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