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