5.70/2.33	MAYBE
5.70/2.33	
5.70/2.33	Proof:
5.70/2.33	ConCon could not decide confluence of the system.
5.70/2.33	Inlined conditions in System R.
5.70/2.33	\cite{ALS94}, Theorem 4.1 does not apply.
5.70/2.33	This system is of type 3 or smaller.
5.70/2.33	This system is strongly deterministic.
5.70/2.33	This system is quasi-decreasing.
5.70/2.33	By \cite{O02}, p. 214, Proposition 7.2.50.
5.70/2.33	This system is of type 3 or smaller.
5.70/2.33	This system is deterministic.
5.70/2.33	System R transformed to U(R).
5.70/2.34	This system is terminating.
5.70/2.34	Call external tool:
5.70/2.34	./ttt2.sh
5.70/2.34	Input:
5.70/2.34	(VAR x z)
5.70/2.34	(RULES
5.70/2.34	  pin(a) -> pout(b)
5.70/2.34	  pin(b) -> pout(c)
5.70/2.34	  tc(x) -> x
5.70/2.34	  ?1(pout(z), x) -> tc(z)
5.70/2.34	  tc(x) -> ?1(pin(x), x)
5.70/2.34	)
5.70/2.34	
5.70/2.34	 Matrix Interpretation Processor: dim=1
5.70/2.34	  
5.70/2.34	  interpretation:
5.70/2.34	   [?1](x0, x1) = x0 + x1,
5.70/2.34	   
5.70/2.34	   [tc](x0) = 7x0 + 1,
5.70/2.34	   
5.70/2.34	   [c] = 0,
5.70/2.34	   
5.70/2.34	   [pout](x0) = 7x0 + 1,
5.70/2.34	   
5.70/2.34	   [b] = 1,
5.70/2.34	   
5.70/2.34	   [pin](x0) = 5x0,
5.70/2.34	   
5.70/2.34	   [a] = 4
5.70/2.34	  orientation:
5.70/2.34	   pin(a()) = 20 >= 8 = pout(b())
5.70/2.34	   
5.70/2.34	   pin(b()) = 5 >= 1 = pout(c())
5.70/2.34	   
5.70/2.34	   tc(x) = 7x + 1 >= x = x
5.70/2.34	   
5.70/2.34	   ?1(pout(z),x) = x + 7z + 1 >= 7z + 1 = tc(z)
5.70/2.34	   
5.70/2.34	   tc(x) = 7x + 1 >= 6x = ?1(pin(x),x)
5.70/2.34	  problem:
5.70/2.34	   ?1(pout(z),x) -> tc(z)
5.70/2.34	  Matrix Interpretation Processor: dim=3
5.70/2.34	   
5.70/2.34	   interpretation:
5.70/2.34	                   [1 0 0]     [1 0 0]     [1]
5.70/2.34	    [?1](x0, x1) = [0 0 0]x0 + [0 0 0]x1 + [0]
5.70/2.34	                   [0 1 0]     [0 0 0]     [0],
5.70/2.34	    
5.70/2.34	               [1 0 0]  
5.70/2.34	    [tc](x0) = [0 0 0]x0
5.70/2.34	               [0 1 0]  ,
5.70/2.34	    
5.70/2.34	                 [1 0 0]  
5.70/2.34	    [pout](x0) = [0 1 0]x0
5.70/2.34	                 [0 0 0]  
5.70/2.34	   orientation:
5.70/2.34	                    [1 0 0]    [1 0 0]    [1]    [1 0 0]         
5.70/2.34	    ?1(pout(z),x) = [0 0 0]x + [0 0 0]z + [0] >= [0 0 0]z = tc(z)
5.70/2.34	                    [0 0 0]    [0 1 0]    [0]    [0 1 0]         
5.70/2.34	   problem:
5.70/2.34	    
5.70/2.34	   Qed
5.70/2.34	This critical pair is conditional.
5.70/2.34	This critical pair has some non-trivial conditions.
5.70/2.34	ConCon could not decide whether all 2 critical pairs are joinable or not.
5.70/2.34	Overlap: (rule1: tc(y) -> tc(x') <= pin(y) = pout(x'), rule2: tc(z) -> z, pos: ε, mgu: {(y,z)})
5.70/2.34	CP: z = tc(x') <= pin(z) = pout(x')
5.70/2.34	ConCon could not decide infeasibility of this critical pair.
5.70/2.34	'tcap_{R_u}(pout(x'))' and 'pin(z)' are unifiable.
5.70/2.34	
5.70/2.36	EOF