3.80/1.85	MAYBE
3.80/1.85	
3.80/1.85	Proof:
3.80/1.85	ConCon could not decide confluence of the system.
3.80/1.85	Removed infeasible rules from system R.
3.80/1.85	\cite{ALS94}, Theorem 4.1 does not apply.
3.80/1.85	This system is of type 3 or smaller.
3.80/1.85	This system is strongly deterministic.
3.80/1.85	This system is quasi-decreasing.
3.80/1.85	By \cite{O02}, p. 214, Proposition 7.2.50.
3.80/1.85	This system is of type 3 or smaller.
3.80/1.85	This system is deterministic.
3.80/1.85	System R transformed to optimized U(R).
3.80/1.85	This system is terminating.
3.80/1.85	Call external tool:
3.80/1.85	./ttt2.sh
3.80/1.85	Input:
3.80/1.85	(VAR x)
3.80/1.85	(RULES
3.80/1.85	  p(q(x)) -> p(r(x))
3.80/1.85	  q(h(x)) -> r(x)
3.80/1.85	  s(x) -> 1
3.80/1.85	)
3.80/1.85	
3.80/1.85	 Matrix Interpretation Processor: dim=3
3.80/1.85	  
3.80/1.85	  interpretation:
3.80/1.85	         [0]
3.80/1.85	   [1] = [0]
3.80/1.85	         [0],
3.80/1.85	   
3.80/1.85	             [1 0 0]  
3.80/1.85	   [s](x0) = [0 0 0]x0
3.80/1.85	             [0 0 0]  ,
3.80/1.85	   
3.80/1.85	             [1 0 0]  
3.80/1.85	   [h](x0) = [0 0 0]x0
3.80/1.85	             [0 1 1]  ,
3.80/1.85	   
3.80/1.85	             [1 0 0]  
3.80/1.85	   [r](x0) = [0 0 0]x0
3.80/1.85	             [0 1 1]  ,
3.80/1.85	   
3.80/1.85	             [1 0 1]  
3.80/1.85	   [p](x0) = [0 0 0]x0
3.80/1.85	             [0 0 0]  ,
3.80/1.85	   
3.80/1.85	             [1 0 0]     [1]
3.80/1.85	   [q](x0) = [0 0 0]x0 + [0]
3.80/1.85	             [0 1 1]     [0]
3.80/1.85	  orientation:
3.80/1.85	             [1 1 1]    [1]    [1 1 1]           
3.80/1.85	   p(q(x)) = [0 0 0]x + [0] >= [0 0 0]x = p(r(x))
3.80/1.85	             [0 0 0]    [0]    [0 0 0]           
3.80/1.85	   
3.80/1.85	             [1 0 0]    [1]    [1 0 0]        
3.80/1.85	   q(h(x)) = [0 0 0]x + [0] >= [0 0 0]x = r(x)
3.80/1.85	             [0 1 1]    [0]    [0 1 1]        
3.80/1.85	   
3.80/1.85	          [1 0 0]     [0]      
3.80/1.85	   s(x) = [0 0 0]x >= [0] = 1()
3.80/1.85	          [0 0 0]     [0]      
3.80/1.85	  problem:
3.80/1.85	   s(x) -> 1()
3.80/1.85	  Matrix Interpretation Processor: dim=3
3.80/1.85	   
3.80/1.85	   interpretation:
3.80/1.85	          [0]
3.80/1.85	    [1] = [0]
3.80/1.86	          [0],
3.80/1.86	    
3.80/1.86	              [1 0 0]     [1]
3.80/1.86	    [s](x0) = [0 0 0]x0 + [0]
3.80/1.86	              [0 0 0]     [0]
3.80/1.86	   orientation:
3.80/1.86	           [1 0 0]    [1]    [0]      
3.80/1.86	    s(x) = [0 0 0]x + [0] >= [0] = 1()
3.80/1.86	           [0 0 0]    [0]    [0]      
3.80/1.86	   problem:
3.80/1.86	    
3.80/1.86	   Qed
3.80/1.86	ConCon could not decide whether all 1 critical pairs are joinable or not.
3.80/1.86	Overlap: (rule1: p(q(y)) -> p(r(y)), rule2: q(h(z)) -> r(z), pos: 1, mgu: {(y,h(z))})
3.80/1.86	CP: p(r(z)) = p(r(h(z)))
3.80/1.86	ConCon could not decide context-joinability of this critical pair.
3.80/1.86	
3.80/1.88	EOF