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