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