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