2.80/1.24	MAYBE
2.80/1.24	
2.80/1.24	Proof:
2.80/1.24	ConCon could not decide confluence of the system.
2.80/1.24	\cite{ALS94}, Theorem 4.1 does not apply.
2.80/1.24	This system is of type 3 or smaller.
2.80/1.25	This system is strongly deterministic.
2.80/1.25	This system is quasi-decreasing.
2.80/1.25	By \cite{O02}, p. 214, Proposition 7.2.50.
2.80/1.25	This system is of type 3 or smaller.
2.80/1.25	This system is deterministic.
2.80/1.25	System R transformed to optimized U(R).
2.80/1.25	This system is terminating.
2.80/1.25	Call external tool:
2.80/1.25	./ttt2.sh
2.80/1.25	Input:
2.80/1.25	  p(q(x)) -> p(r(x))
2.80/1.25	  q(h(x)) -> r(x)
2.80/1.25	  r(x) -> ?1(s(x), x)
2.80/1.25	  ?1(0, x) -> r(h(x))
2.80/1.25	  s(x) -> 1
2.80/1.25	
2.80/1.25	 DP Processor:
2.80/1.25	  DPs:
2.80/1.25	   p#(q(x)) -> r#(x)
2.80/1.25	   p#(q(x)) -> p#(r(x))
2.80/1.25	   q#(h(x)) -> r#(x)
2.80/1.25	   r#(x) -> s#(x)
2.80/1.25	   r#(x) -> ?1#(s(x),x)
2.80/1.25	   ?1#(0(),x) -> r#(h(x))
2.80/1.25	  TRS:
2.80/1.25	   p(q(x)) -> p(r(x))
2.80/1.25	   q(h(x)) -> r(x)
2.80/1.25	   r(x) -> ?1(s(x),x)
2.80/1.25	   ?1(0(),x) -> r(h(x))
2.80/1.25	   s(x) -> 1()
2.80/1.25	  TDG Processor:
2.80/1.25	   DPs:
2.80/1.25	    p#(q(x)) -> r#(x)
2.80/1.25	    p#(q(x)) -> p#(r(x))
2.80/1.25	    q#(h(x)) -> r#(x)
2.80/1.25	    r#(x) -> s#(x)
2.80/1.25	    r#(x) -> ?1#(s(x),x)
2.80/1.25	    ?1#(0(),x) -> r#(h(x))
2.80/1.25	   TRS:
2.80/1.25	    p(q(x)) -> p(r(x))
2.80/1.25	    q(h(x)) -> r(x)
2.80/1.25	    r(x) -> ?1(s(x),x)
2.80/1.25	    ?1(0(),x) -> r(h(x))
2.80/1.25	    s(x) -> 1()
2.80/1.25	   graph:
2.80/1.25	    ?1#(0(),x) -> r#(h(x)) -> r#(x) -> ?1#(s(x),x)
2.80/1.25	    ?1#(0(),x) -> r#(h(x)) -> r#(x) -> s#(x)
2.80/1.25	    q#(h(x)) -> r#(x) -> r#(x) -> ?1#(s(x),x)
2.80/1.25	    q#(h(x)) -> r#(x) -> r#(x) -> s#(x)
2.80/1.25	    r#(x) -> ?1#(s(x),x) -> ?1#(0(),x) -> r#(h(x))
2.80/1.25	    p#(q(x)) -> r#(x) -> r#(x) -> ?1#(s(x),x)
2.80/1.25	    p#(q(x)) -> r#(x) -> r#(x) -> s#(x)
2.80/1.25	    p#(q(x)) -> p#(r(x)) -> p#(q(x)) -> p#(r(x))
2.80/1.25	    p#(q(x)) -> p#(r(x)) -> p#(q(x)) -> r#(x)
2.80/1.25	   SCC Processor:
2.80/1.25	    #sccs: 2
2.80/1.25	    #rules: 3
2.80/1.25	    #arcs: 9/36
2.80/1.25	    DPs:
2.80/1.25	     p#(q(x)) -> p#(r(x))
2.80/1.25	    TRS:
2.80/1.25	     p(q(x)) -> p(r(x))
2.80/1.25	     q(h(x)) -> r(x)
2.80/1.25	     r(x) -> ?1(s(x),x)
2.80/1.25	     ?1(0(),x) -> r(h(x))
2.80/1.25	     s(x) -> 1()
2.80/1.25	    EDG Processor:
2.80/1.25	     DPs:
2.80/1.25	      p#(q(x)) -> p#(r(x))
2.80/1.25	     TRS:
2.80/1.25	      p(q(x)) -> p(r(x))
2.80/1.25	      q(h(x)) -> r(x)
2.80/1.25	      r(x) -> ?1(s(x),x)
2.80/1.25	      ?1(0(),x) -> r(h(x))
2.80/1.25	      s(x) -> 1()
2.80/1.25	     graph:
2.80/1.25	      
2.80/1.25	     SCC Processor:
2.80/1.25	      #sccs: 0
2.80/1.25	      #rules: 0
2.80/1.25	      #arcs: 0/1
2.80/1.25	      
2.80/1.25	    
2.80/1.25	    DPs:
2.80/1.25	     ?1#(0(),x) -> r#(h(x))
2.80/1.25	     r#(x) -> ?1#(s(x),x)
2.80/1.25	    TRS:
2.80/1.25	     p(q(x)) -> p(r(x))
2.80/1.25	     q(h(x)) -> r(x)
2.80/1.25	     r(x) -> ?1(s(x),x)
2.80/1.25	     ?1(0(),x) -> r(h(x))
2.80/1.25	     s(x) -> 1()
2.80/1.25	    EDG Processor:
2.80/1.25	     DPs:
2.80/1.25	      ?1#(0(),x) -> r#(h(x))
2.80/1.25	      r#(x) -> ?1#(s(x),x)
2.80/1.25	     TRS:
2.80/1.25	      p(q(x)) -> p(r(x))
2.80/1.25	      q(h(x)) -> r(x)
2.80/1.25	      r(x) -> ?1(s(x),x)
2.80/1.25	      ?1(0(),x) -> r(h(x))
2.80/1.25	      s(x) -> 1()
2.80/1.25	     graph:
2.80/1.25	      ?1#(0(),x) -> r#(h(x)) -> r#(x) -> ?1#(s(x),x)
2.80/1.25	     SCC Processor:
2.80/1.25	      #sccs: 0
2.80/1.25	      #rules: 0
2.80/1.25	      #arcs: 1/4
2.80/1.25	      
2.80/1.25	This critical pair is not trivial.
2.80/1.25	
2.80/1.28	EOF