4.83/2.16	MAYBE
4.83/2.16	
4.83/2.16	Proof:
4.83/2.16	ConCon could not decide confluence of the system.
4.83/2.16	\cite{ALS94}, Theorem 4.1 does not apply.
4.83/2.16	This system is of type 3 or smaller.
4.83/2.16	This system is strongly deterministic.
4.83/2.16	This system is quasi-decreasing.
4.83/2.16	By \cite{O02}, p. 214, Proposition 7.2.50.
4.83/2.16	This system is of type 3 or smaller.
4.83/2.16	This system is deterministic.
4.83/2.16	System R transformed to U(R).
4.83/2.16	This system is terminating.
4.83/2.16	Call external tool:
4.83/2.16	./ttt2.sh
4.83/2.16	Input:
4.83/2.16	(VAR x y)
4.83/2.16	(RULES
4.83/2.16	  a -> c
4.83/2.16	  a -> d
4.83/2.16	  b -> c
4.83/2.16	  b -> d
4.83/2.16	  s(c) -> t(k)
4.83/2.16	  s(c) -> t(l)
4.83/2.16	  g(x, x) -> h(x, x)
4.83/2.16	  ?1(t(y), x) -> pair(x, y)
4.83/2.16	  f(x) -> ?1(s(x), x)
4.83/2.16	)
4.83/2.16	
4.83/2.16	 Matrix Interpretation Processor: dim=1
4.83/2.16	  
4.83/2.16	  interpretation:
4.83/2.16	   [f](x0) = 7x0 + 7,
4.83/2.16	   
4.83/2.16	   [pair](x0, x1) = x0 + x1,
4.83/2.16	   
5.12/2.16	   [?1](x0, x1) = 3x0 + 4x1 + 1,
5.12/2.16	   
5.12/2.16	   [h](x0, x1) = x0 + x1,
5.12/2.16	   
5.12/2.16	   [g](x0, x1) = x0 + x1 + 2,
5.12/2.16	   
5.12/2.16	   [l] = 0,
5.12/2.16	   
5.12/2.16	   [t](x0) = x0 + 1,
5.12/2.16	   
5.12/2.16	   [k] = 0,
5.12/2.16	   
5.12/2.16	   [s](x0) = x0 + 2,
5.12/2.16	   
5.12/2.16	   [b] = 5,
5.12/2.16	   
5.12/2.16	   [d] = 5,
5.12/2.16	   
5.12/2.16	   [c] = 0,
5.12/2.16	   
5.12/2.16	   [a] = 5
5.12/2.17	  orientation:
5.12/2.17	   a() = 5 >= 0 = c()
5.12/2.17	   
5.12/2.17	   a() = 5 >= 5 = d()
5.12/2.17	   
5.12/2.17	   b() = 5 >= 0 = c()
5.12/2.17	   
5.12/2.17	   b() = 5 >= 5 = d()
5.12/2.17	   
5.12/2.17	   s(c()) = 2 >= 1 = t(k())
5.12/2.17	   
5.12/2.17	   s(c()) = 2 >= 1 = t(l())
5.12/2.17	   
5.12/2.17	   g(x,x) = 2x + 2 >= 2x = h(x,x)
5.12/2.17	   
5.12/2.17	   ?1(t(y),x) = 4x + 3y + 4 >= x + y = pair(x,y)
5.12/2.17	   
5.12/2.17	   f(x) = 7x + 7 >= 7x + 7 = ?1(s(x),x)
5.12/2.17	  problem:
5.12/2.17	   a() -> d()
5.12/2.17	   b() -> d()
5.12/2.17	   f(x) -> ?1(s(x),x)
5.12/2.17	  Matrix Interpretation Processor: dim=1
5.12/2.17	   
5.12/2.17	   interpretation:
5.12/2.17	    [f](x0) = 2x0 + 1,
5.12/2.17	    
5.12/2.17	    [?1](x0, x1) = x0 + x1,
5.12/2.17	    
5.12/2.17	    [s](x0) = x0,
5.12/2.17	    
5.12/2.17	    [b] = 0,
5.12/2.17	    
5.12/2.17	    [d] = 0,
5.12/2.17	    
5.12/2.17	    [a] = 0
5.12/2.17	   orientation:
5.12/2.17	    a() = 0 >= 0 = d()
5.12/2.17	    
5.12/2.17	    b() = 0 >= 0 = d()
5.12/2.17	    
5.12/2.17	    f(x) = 2x + 1 >= 2x = ?1(s(x),x)
5.12/2.17	   problem:
5.12/2.17	    a() -> d()
5.12/2.17	    b() -> d()
5.12/2.17	   Matrix Interpretation Processor: dim=3
5.12/2.17	    
5.12/2.17	    interpretation:
5.12/2.17	           [1]
5.12/2.17	     [b] = [0]
5.12/2.17	           [0],
5.12/2.17	     
5.12/2.17	           [0]
5.12/2.17	     [d] = [0]
5.12/2.17	           [0],
5.12/2.17	     
5.12/2.17	           [0]
5.12/2.17	     [a] = [0]
5.12/2.17	           [0]
5.12/2.17	    orientation:
5.12/2.17	           [0]    [0]      
5.12/2.17	     a() = [0] >= [0] = d()
5.12/2.17	           [0]    [0]      
5.12/2.17	     
5.12/2.17	           [1]    [0]      
5.12/2.17	     b() = [0] >= [0] = d()
5.12/2.17	           [0]    [0]      
5.12/2.17	    problem:
5.12/2.17	     a() -> d()
5.12/2.17	    Matrix Interpretation Processor: dim=3
5.12/2.17	     
5.12/2.17	     interpretation:
5.12/2.17	            [0]
5.12/2.17	      [d] = [0]
5.12/2.17	            [0],
5.12/2.17	      
5.12/2.17	            [1]
5.12/2.17	      [a] = [0]
5.12/2.17	            [1]
5.12/2.17	     orientation:
5.12/2.17	            [1]    [0]      
5.12/2.17	      a() = [0] >= [0] = d()
5.12/2.17	            [1]    [0]      
5.12/2.17	     problem:
5.12/2.17	      
5.12/2.17	     Qed
5.12/2.17	ConCon could not decide whether all 6 critical pairs are joinable or not.
5.12/2.17	Overlap: (rule1: s(c) -> t(k), rule2: s(c) -> t(l), pos: ε, mgu: {})
5.12/2.17	CP: t(l) = t(k)
5.12/2.17	ConCon could not decide context-joinability of this critical pair.
5.12/2.17	
5.15/2.20	EOF