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