4.61/2.12	MAYBE
4.61/2.12	
4.61/2.12	Proof:
4.61/2.12	ConCon could not decide confluence of the system.
4.61/2.12	\cite{ALS94}, Theorem 4.1 does not apply.
4.61/2.12	This system is of type 3 or smaller.
4.61/2.12	This system is strongly deterministic.
4.61/2.12	This system is quasi-decreasing.
4.61/2.12	By \cite{O02}, p. 214, Proposition 7.2.50.
4.61/2.12	This system is of type 3 or smaller.
4.61/2.12	This system is deterministic.
4.61/2.12	System R transformed to optimized U(R).
4.61/2.12	This system is terminating.
4.61/2.12	Call external tool:
4.61/2.12	./ttt2.sh
4.61/2.12	Input:
4.61/2.12	(VAR x)
4.61/2.12	(RULES
4.61/2.12	  b -> d
4.61/2.12	  h(x, f(x)) -> x
4.61/2.12	  a -> d
4.61/2.12	  g(x, x) -> h(x, x)
4.61/2.12	  b -> c
4.61/2.12	  f(x) -> ?1(x, x)
4.61/2.12	  ?1(c, x) -> x
4.61/2.12	  a -> c
4.61/2.12	)
4.61/2.12	
4.61/2.12	 Matrix Interpretation Processor: dim=1
4.61/2.12	  
4.61/2.12	  interpretation:
4.61/2.12	   [?1](x0, x1) = x0 + x1,
4.61/2.12	   
4.61/2.12	   [c] = 0,
4.61/2.12	   
4.61/2.12	   [g](x0, x1) = x0 + 7x1 + 4,
4.61/2.12	   
4.61/2.12	   [a] = 5,
4.61/2.12	   
4.61/2.12	   [h](x0, x1) = x0 + 3x1 + 1,
4.61/2.12	   
4.61/2.12	   [f](x0) = 2x0 + 4,
4.61/2.12	   
4.61/2.12	   [d] = 0,
4.61/2.12	   
4.61/2.12	   [b] = 5
4.61/2.12	  orientation:
4.61/2.12	   b() = 5 >= 0 = d()
4.61/2.12	   
4.61/2.12	   h(x,f(x)) = 7x + 13 >= x = x
4.61/2.12	   
4.61/2.12	   a() = 5 >= 0 = d()
4.61/2.12	   
4.61/2.13	   g(x,x) = 8x + 4 >= 4x + 1 = h(x,x)
4.61/2.13	   
4.61/2.13	   b() = 5 >= 0 = c()
4.61/2.13	   
4.61/2.13	   f(x) = 2x + 4 >= 2x = ?1(x,x)
4.61/2.13	   
4.61/2.13	   ?1(c(),x) = x >= x = x
4.84/2.13	   
4.84/2.13	   a() = 5 >= 0 = c()
4.84/2.13	  problem:
4.84/2.13	   ?1(c(),x) -> x
4.84/2.13	  Matrix Interpretation Processor: dim=3
4.84/2.13	   
4.84/2.13	   interpretation:
4.84/2.13	                   [1 1 0]       
4.84/2.13	    [?1](x0, x1) = [0 0 0]x0 + x1
4.84/2.13	                   [0 0 0]       ,
4.84/2.13	    
4.84/2.13	          [0]
4.84/2.13	    [c] = [1]
4.84/2.13	          [0]
4.84/2.13	   orientation:
4.84/2.13	                    [1]         
4.84/2.13	    ?1(c(),x) = x + [0] >= x = x
4.84/2.13	                    [0]         
4.84/2.13	   problem:
4.84/2.13	    
4.84/2.13	   Qed
4.84/2.13	This critical pair is conditional.
4.84/2.13	This critical pair has some non-trivial conditions.
4.84/2.13	ConCon could not decide whether all 5 critical pairs are joinable or not.
4.84/2.13	Overlap: (rule1: h(y, f(y)) -> y, rule2: f(z) -> z <= z = c, pos: 2, mgu: {(y,z)})
4.84/2.13	CP: h(z, z) = z <= z = c
4.84/2.13	ConCon could not decide infeasibility of this critical pair.
4.84/2.13	
4.84/2.15	EOF