0.00/0.82	NO
0.00/0.82	
0.00/0.82	Problem:
0.00/0.82	gcd(add(x, y), y) -> gcd(x, y)
0.00/0.82	gcd(y, add(x, y)) -> gcd(x, y)
0.00/0.82	gcd(x, 0()) -> x
0.00/0.82	gcd(0(), x) -> x
0.00/0.82	gcd(x, y) -> gcd(y, x) <= leq(y, x) = false()
0.00/0.82	add(0(), y) -> y
0.00/0.82	add(s(x), y) -> s(add(x, y))
0.00/0.82	
0.00/0.82	Proof:
0.00/0.82	This system is not confluent.
0.00/0.82	This system is oriented.
0.00/0.82	For the unconditional CP add(x, 0()) = gcd(x, 0()) the left- and right-hand sides are not joinable wrt R_u.
0.00/0.82	Call external tool:
0.00/0.82	./csi.sh
0.00/0.82	Input:
0.00/0.82	  gcd(add(x, y), y) -> gcd(x, y)
0.00/0.82	  gcd(y, add(x, y)) -> gcd(x, y)
0.00/0.82	  gcd(x, 0()) -> x
0.00/0.82	  gcd(0(), x) -> x
0.00/0.82	  gcd(x, y) -> gcd(y, x)
0.00/0.82	  add(0(), y) -> y
0.00/0.82	  add(s(x), y) -> s(add(x, y))
0.00/0.82	
0.00/0.82	 Nonconfluence Processor:
0.00/0.82	  terms: add(f4(),0()) *<- add(f4(),0()) ->* gcd(f4(),0())
0.00/0.82	  Qed
0.00/0.82	  
0.00/0.82	  first automaton:
0.00/0.82	   final states: {1}
0.00/0.82	   transitions:
0.00/0.82	    add(3,2) -> 1*
0.00/0.82	    0() -> 2*
0.00/0.82	    f4() -> 3*
0.00/0.82	  
0.00/0.82	  second automaton:
0.00/0.82	   final states: {18,4}
0.00/0.82	   transitions:
0.00/0.82	    gcd(18,5) -> 4*
0.00/0.82	    gcd(5,6) -> 4*
0.00/0.82	    gcd(5,18) -> 4*
0.00/0.82	    gcd(6,5) -> 4*
0.00/0.82	    0() -> 5*
0.00/0.82	    f4() -> 18*,4,6
0.00/0.82	    6 -> 4*
0.00/0.82	    18 -> 4*
0.00/0.82	
2.76/1.19	EOF