1.54/1.08	NO
1.54/1.08	
1.54/1.08	Proof:
1.54/1.08	This system is not confluent.
1.54/1.08	For the unconditional CP gcd(x', x') = gcd(0, x') the left- and right-hand sides are not joinable wrt R_u.
1.54/1.08	Call external tool:
1.54/1.08	./csi.sh
1.54/1.08	Input:
1.54/1.08	  gcd(add(x, y), y) -> gcd(x, y)
1.54/1.08	  gcd(y, add(x, y)) -> gcd(x, y)
1.54/1.08	  gcd(x, 0) -> x
1.54/1.08	  gcd(0, x) -> x
1.54/1.08	  gcd(x, y) -> gcd(y, x)
1.54/1.08	  add(0, y) -> y
1.54/1.08	  add(s(x), y) -> s(add(x, y))
1.54/1.08	
1.54/1.08	 Nonconfluence Processor:
1.54/1.08	  terms: gcd(x'(),x'()) *<- gcd(x'(),x'()) ->* gcd(0(),x'())
1.54/1.08	  Qed
1.54/1.08	  
1.54/1.08	  first automaton:
1.54/1.08	   final states: {1}
1.54/1.08	   transitions:
1.54/1.08	    gcd(3,11) -> 1*
1.54/1.08	    gcd(11,2) -> 1*
1.54/1.08	    gcd(2,3) -> 1*
1.54/1.08	    gcd(2,11) -> 1*
1.54/1.08	    gcd(3,2) -> 1*
1.54/1.08	    gcd(11,3) -> 1*
1.54/1.08	    gcd(11,11) -> 1*
1.54/1.08	    x'() -> 11*,3,2
1.54/1.08	  
1.54/1.08	  second automaton:
1.54/1.08	   final states: {32,4}
1.54/1.08	   transitions:
1.54/1.08	    gcd(6,32) -> 4*
1.54/1.08	    gcd(5,6) -> 4*
1.54/1.08	    gcd(6,5) -> 4*
1.54/1.08	    gcd(32,6) -> 4*
1.54/1.08	    0() -> 6*
1.54/1.08	    x'() -> 32*,4,5
1.54/1.08	    5 -> 4*
1.54/1.08	    32 -> 4*
1.54/1.08	
3.37/1.47	EOF