0.00/0.64	NO
0.00/0.64	
0.00/0.64	Problem:
0.00/0.64	gcd(z, y) -> gcd(x, y) <= iadd(z) = tp2(x, y)
0.00/0.64	gcd(y, z) -> gcd(x, y) <= iadd(z) = tp2(x, y)
0.00/0.64	gcd(x, 0()) -> x
0.00/0.64	gcd(0(), x) -> x
0.00/0.64	iadd(y) -> tp2(0(), y)
0.00/0.64	iadd(s(z)) -> tp2(s(x), y) <= iadd(z) = tp2(x, y)
0.00/0.64	iadd(add(x, y)) -> tp2(x, y)
0.00/0.64	
0.00/0.64	Proof:
0.00/0.64	This system is not confluent.
0.00/0.64	This system is oriented.
0.00/0.64	For the unconditional CP tp2(x, y) = tp2(0(), add(x, y)) the left- and right-hand sides are two different normal forms wrt R_u.
0.00/0.64	
0.00/0.96	EOF