4.96/2.22	MAYBE
4.96/2.22	
4.96/2.22	Proof:
4.96/2.22	ConCon could not decide confluence of the system.
4.96/2.22	Removed infeasible rules from system R.
4.96/2.22	\cite{ALS94}, Theorem 4.1 does not apply.
4.96/2.22	This system is of type 3 or smaller.
4.96/2.22	This system is strongly deterministic.
4.96/2.22	This system is quasi-decreasing.
4.96/2.22	By \cite{O02}, p. 214, Proposition 7.2.50.
4.96/2.22	This system is of type 3 or smaller.
4.96/2.22	This system is deterministic.
4.96/2.22	System R transformed to U(R).
4.96/2.22	This system is terminating.
4.96/2.22	Call external tool:
4.96/2.22	./ttt2.sh
4.96/2.22	Input:
4.96/2.22	(VAR x y)
4.96/2.22	(RULES
4.96/2.22	  gcd(add(x, y), y) -> gcd(x, y)
4.96/2.22	  gcd(y, add(x, y)) -> gcd(x, y)
4.96/2.22	  gcd(x, 0) -> x
4.96/2.22	  gcd(0, x) -> x
4.96/2.22	  add(0, y) -> y
4.96/2.22	  add(s(x), y) -> s(add(x, y))
4.96/2.22	)
4.96/2.22	
4.96/2.22	 Matrix Interpretation Processor: dim=1
4.96/2.22	  
4.96/2.22	  interpretation:
4.96/2.22	   [s](x0) = x0,
4.96/2.22	   
4.96/2.22	   [0] = 5,
4.96/2.22	   
4.96/2.22	   [gcd](x0, x1) = 2x0 + 2x1 + 1,
4.96/2.22	   
4.96/2.22	   [add](x0, x1) = 4x0 + x1 + 5
4.96/2.22	  orientation:
4.96/2.22	   gcd(add(x,y),y) = 8x + 4y + 11 >= 2x + 2y + 1 = gcd(x,y)
4.96/2.22	   
4.96/2.22	   gcd(y,add(x,y)) = 8x + 4y + 11 >= 2x + 2y + 1 = gcd(x,y)
4.96/2.22	   
4.96/2.22	   gcd(x,0()) = 2x + 11 >= x = x
4.96/2.22	   
4.96/2.22	   gcd(0(),x) = 2x + 11 >= x = x
4.96/2.22	   
4.96/2.22	   add(0(),y) = y + 25 >= y = y
4.96/2.22	   
4.96/2.22	   add(s(x),y) = 4x + y + 5 >= 4x + y + 5 = s(add(x,y))
4.96/2.22	  problem:
4.96/2.22	   add(s(x),y) -> s(add(x,y))
4.96/2.22	  Matrix Interpretation Processor: dim=3
4.96/2.22	   
4.96/2.22	   interpretation:
4.96/2.22	                   [0]
4.96/2.22	    [s](x0) = x0 + [1]
4.96/2.22	                   [1],
4.96/2.22	    
4.96/2.22	                    [1 1 0]     [1 0 0]  
4.96/2.22	    [add](x0, x1) = [0 0 1]x0 + [0 0 0]x1
4.96/2.22	                    [0 1 0]     [0 0 0]  
4.96/2.22	   orientation:
4.96/2.22	                  [1 1 0]    [1 0 0]    [1]    [1 1 0]    [1 0 0]    [0]              
4.96/2.22	    add(s(x),y) = [0 0 1]x + [0 0 0]y + [1] >= [0 0 1]x + [0 0 0]y + [1] = s(add(x,y))
4.96/2.22	                  [0 1 0]    [0 0 0]    [1]    [0 1 0]    [0 0 0]    [1]              
4.96/2.22	   problem:
4.96/2.22	    
4.96/2.22	   Qed
4.96/2.22	ConCon could not decide whether all 10 critical pairs are joinable or not.
4.96/2.22	Overlap: (rule1: gcd(add(z, x'), x') -> gcd(z, x'), rule2: add(0, x) -> x, pos: 1, mgu: {(z,0), (x',x)})
4.96/2.22	CP: gcd(x, x) = gcd(0, x)
4.96/2.22	ConCon could not decide context-joinability of this critical pair.
4.96/2.22	
5.17/2.25	EOF