0.00/0.52	YES
0.00/0.52	system: plus(0(), y) -> y ; plus(s(x), y) -> plus(x, s(y)) ; f(x, y) -> z <= plus(x, y) ->* plus(z, z')
0.00/0.52	CTRS is orthogonal, properly oriented and right stable, hence level-confluent
0.00/0.53	EOF