16.43/4.81	MAYBE
16.43/4.81	
16.43/4.81	Proof:
16.43/4.81	ConCon could not decide confluence of the system.
16.43/4.81	\cite{ALS94}, Theorem 4.1 does not apply.
16.43/4.81	This system is of type 3 or smaller.
16.43/4.81	This system is strongly deterministic.
16.43/4.81	This system is quasi-decreasing.
16.43/4.81	By \cite{O02}, p. 214, Proposition 7.2.50.
16.43/4.81	This system is of type 3 or smaller.
16.43/4.81	This system is deterministic.
16.43/4.81	System R transformed to U(R).
16.43/4.81	This system is terminating.
16.43/4.81	Call external tool:
16.43/4.81	./ttt2.sh
16.43/4.81	Input:
16.43/4.81	  ?1(pair(z1, z2), x, y, rest) -> cons(z1, cons(z2, rest))
16.43/4.81	  cons(x, cons(y, rest)) -> ?1(orient(x, y), x, y, rest)
16.43/4.81	  cons(x, cons(x, rest)) -> cons(x, rest)
16.43/4.81	  ?2(pair(z1, z2), x, y) -> pair(s(z1), s(z2))
16.43/4.81	  orient(s(x), s(y)) -> ?2(orient(x, y), x, y)
16.43/4.81	  orient(s(x), 0) -> pair(0, s(x))
16.43/4.81	
16.43/4.81	 DP Processor:
16.43/4.81	  DPs:
16.43/4.81	   ?1#(pair(z1,z2),x,y,rest) -> cons#(z2,rest)
16.43/4.81	   ?1#(pair(z1,z2),x,y,rest) -> cons#(z1,cons(z2,rest))
16.43/4.81	   cons#(x,cons(y,rest)) -> orient#(x,y)
16.43/4.81	   cons#(x,cons(y,rest)) -> ?1#(orient(x,y),x,y,rest)
16.43/4.81	   orient#(s(x),s(y)) -> orient#(x,y)
16.43/4.81	   orient#(s(x),s(y)) -> ?2#(orient(x,y),x,y)
16.43/4.81	  TRS:
16.43/4.81	   ?1(pair(z1,z2),x,y,rest) -> cons(z1,cons(z2,rest))
16.43/4.81	   cons(x,cons(y,rest)) -> ?1(orient(x,y),x,y,rest)
16.43/4.81	   cons(x,cons(x,rest)) -> cons(x,rest)
16.43/4.81	   ?2(pair(z1,z2),x,y) -> pair(s(z1),s(z2))
16.43/4.81	   orient(s(x),s(y)) -> ?2(orient(x,y),x,y)
16.43/4.81	   orient(s(x),0()) -> pair(0(),s(x))
16.43/4.81	  TDG Processor:
16.43/4.81	   DPs:
16.43/4.81	    ?1#(pair(z1,z2),x,y,rest) -> cons#(z2,rest)
16.43/4.81	    ?1#(pair(z1,z2),x,y,rest) -> cons#(z1,cons(z2,rest))
16.43/4.81	    cons#(x,cons(y,rest)) -> orient#(x,y)
16.43/4.81	    cons#(x,cons(y,rest)) -> ?1#(orient(x,y),x,y,rest)
16.43/4.81	    orient#(s(x),s(y)) -> orient#(x,y)
16.43/4.81	    orient#(s(x),s(y)) -> ?2#(orient(x,y),x,y)
16.43/4.81	   TRS:
16.43/4.81	    ?1(pair(z1,z2),x,y,rest) -> cons(z1,cons(z2,rest))
16.43/4.81	    cons(x,cons(y,rest)) -> ?1(orient(x,y),x,y,rest)
16.43/4.81	    cons(x,cons(x,rest)) -> cons(x,rest)
16.43/4.81	    ?2(pair(z1,z2),x,y) -> pair(s(z1),s(z2))
16.43/4.81	    orient(s(x),s(y)) -> ?2(orient(x,y),x,y)
16.43/4.81	    orient(s(x),0()) -> pair(0(),s(x))
16.43/4.81	   graph:
16.43/4.81	    orient#(s(x),s(y)) -> orient#(x,y) ->
16.43/4.81	    orient#(s(x),s(y)) -> ?2#(orient(x,y),x,y)
16.43/4.81	    orient#(s(x),s(y)) -> orient#(x,y) ->
16.43/4.81	    orient#(s(x),s(y)) -> orient#(x,y)
16.43/4.81	    cons#(x,cons(y,rest)) -> orient#(x,y) ->
16.43/4.81	    orient#(s(x),s(y)) -> ?2#(orient(x,y),x,y)
16.43/4.81	    cons#(x,cons(y,rest)) -> orient#(x,y) ->
16.43/4.81	    orient#(s(x),s(y)) -> orient#(x,y)
16.43/4.81	    cons#(x,cons(y,rest)) -> ?1#(orient(x,y),x,y,rest) ->
16.43/4.81	    ?1#(pair(z1,z2),x,y,rest) -> cons#(z1,cons(z2,rest))
16.43/4.81	    cons#(x,cons(y,rest)) -> ?1#(orient(x,y),x,y,rest) ->
16.43/4.81	    ?1#(pair(z1,z2),x,y,rest) -> cons#(z2,rest)
16.43/4.81	    ?1#(pair(z1,z2),x,y,rest) -> cons#(z1,cons(z2,rest)) ->
16.43/4.81	    cons#(x,cons(y,rest)) -> ?1#(orient(x,y),x,y,rest)
16.43/4.81	    ?1#(pair(z1,z2),x,y,rest) -> cons#(z1,cons(z2,rest)) ->
16.43/4.81	    cons#(x,cons(y,rest)) -> orient#(x,y)
16.43/4.81	    ?1#(pair(z1,z2),x,y,rest) -> cons#(z2,rest) ->
16.43/4.81	    cons#(x,cons(y,rest)) -> ?1#(orient(x,y),x,y,rest)
16.43/4.81	    ?1#(pair(z1,z2),x,y,rest) -> cons#(z2,rest) -> cons#(x,cons(y,rest)) -> orient#(x,y)
16.43/4.81	   SCC Processor:
16.43/4.82	    #sccs: 2
16.43/4.82	    #rules: 4
16.43/4.82	    #arcs: 10/36
16.43/4.82	    DPs:
16.43/4.82	     cons#(x,cons(y,rest)) -> ?1#(orient(x,y),x,y,rest)
16.43/4.82	     ?1#(pair(z1,z2),x,y,rest) -> cons#(z2,rest)
16.43/4.82	     ?1#(pair(z1,z2),x,y,rest) -> cons#(z1,cons(z2,rest))
16.43/4.82	    TRS:
16.43/4.82	     ?1(pair(z1,z2),x,y,rest) -> cons(z1,cons(z2,rest))
16.43/4.82	     cons(x,cons(y,rest)) -> ?1(orient(x,y),x,y,rest)
16.43/4.82	     cons(x,cons(x,rest)) -> cons(x,rest)
16.43/4.82	     ?2(pair(z1,z2),x,y) -> pair(s(z1),s(z2))
16.43/4.82	     orient(s(x),s(y)) -> ?2(orient(x,y),x,y)
16.43/4.82	     orient(s(x),0()) -> pair(0(),s(x))
16.43/4.82	    Subterm Criterion Processor:
16.43/4.82	     simple projection:
16.43/4.82	      pi(pair) = [0,1]
16.43/4.82	      pi(?1) = [0,3]
16.43/4.82	      pi(cons) = [0,1]
16.43/4.82	      pi(orient) = [0,1]
16.43/4.82	      pi(?2) = 0
16.43/4.82	      pi(s) = 0
16.43/4.82	      pi(?1#) = [0,3]
16.43/4.82	      pi(cons#) = [0,1]
16.43/4.82	     problem:
16.43/4.82	      DPs:
16.43/4.82	       cons#(x,cons(y,rest)) -> ?1#(orient(x,y),x,y,rest)
16.43/4.82	       ?1#(pair(z1,z2),x,y,rest) -> cons#(z1,cons(z2,rest))
16.43/4.82	      TRS:
16.43/4.82	       ?1(pair(z1,z2),x,y,rest) -> cons(z1,cons(z2,rest))
16.43/4.82	       cons(x,cons(y,rest)) -> ?1(orient(x,y),x,y,rest)
16.43/4.82	       cons(x,cons(x,rest)) -> cons(x,rest)
16.43/4.82	       ?2(pair(z1,z2),x,y) -> pair(s(z1),s(z2))
16.43/4.82	       orient(s(x),s(y)) -> ?2(orient(x,y),x,y)
16.43/4.82	       orient(s(x),0()) -> pair(0(),s(x))
16.43/4.82	     Arctic Interpretation Processor:
16.43/4.82	      dimension: 1
16.43/4.82	      usable rules:
16.43/4.82	       ?2(pair(z1,z2),x,y) -> pair(s(z1),s(z2))
16.43/4.82	       orient(s(x),s(y)) -> ?2(orient(x,y),x,y)
16.43/4.82	       orient(s(x),0()) -> pair(0(),s(x))
16.43/4.82	      interpretation:
16.43/4.82	       [cons#](x0, x1) = x0 + 1,
16.43/4.82	       
16.43/4.82	       [?1#](x0, x1, x2, x3) = x0 + x1 + 0,
16.43/4.82	       
16.43/4.82	       [0] = 2,
16.43/4.82	       
16.43/4.82	       [s](x0) = 5x0 + 6,
16.43/4.82	       
16.43/4.82	       [?2](x0, x1, x2) = 5x0 + 4x1 + 0,
16.43/4.82	       
16.43/4.82	       [orient](x0, x1) = x0 + 1,
16.43/4.82	       
16.43/4.82	       [cons](x0, x1) = 1x0 + 1x1,
16.43/4.82	       
16.43/4.82	       [?1](x0, x1, x2, x3) = x0 + 11x1 + 2x2 + 2x3 + 0,
16.43/4.82	       
16.43/4.82	       [pair](x0, x1) = 1x0 + x1 + 2
16.43/4.82	      orientation:
16.43/4.82	       cons#(x,cons(y,rest)) = x + 1 >= x + 1 = ?1#(orient(x,y),x,y,rest)
16.43/4.82	       
16.43/4.82	       ?1#(pair(z1,z2),x,y,rest) = x + 1z1 + z2 + 2 >= z1 + 1 = cons#(z1,cons(z2,rest))
16.43/4.82	       
16.43/4.82	       ?1(pair(z1,z2),x,y,rest) = 2rest + 11x + 2y + 1z1 + z2 + 2 >= 2rest + 1z1 + 2z2 = cons(z1,cons(z2,rest))
16.43/4.82	       
16.43/4.82	       cons(x,cons(y,rest)) = 2rest + 1x + 2y >= 2rest + 11x + 2y + 1 = ?1(orient(x,y),x,y,rest)
16.43/4.82	       
16.43/4.82	       cons(x,cons(x,rest)) = 2rest + 2x >= 1rest + 1x = cons(x,rest)
16.43/4.82	       
16.43/4.82	       ?2(pair(z1,z2),x,y) = 4x + 6z1 + 5z2 + 7 >= 6z1 + 5z2 + 7 = pair(s(z1),s(z2))
16.43/4.82	       
16.43/4.82	       orient(s(x),s(y)) = 5x + 6 >= 5x + 6 = ?2(orient(x,y),x,y)
16.43/4.82	       
16.43/4.82	       orient(s(x),0()) = 5x + 6 >= 5x + 6 = pair(0(),s(x))
16.43/4.82	      problem:
16.43/4.82	       DPs:
16.43/4.82	        cons#(x,cons(y,rest)) -> ?1#(orient(x,y),x,y,rest)
16.43/4.82	       TRS:
16.43/4.82	        ?1(pair(z1,z2),x,y,rest) -> cons(z1,cons(z2,rest))
16.43/4.82	        cons(x,cons(y,rest)) -> ?1(orient(x,y),x,y,rest)
16.43/4.82	        cons(x,cons(x,rest)) -> cons(x,rest)
16.43/4.82	        ?2(pair(z1,z2),x,y) -> pair(s(z1),s(z2))
16.43/4.82	        orient(s(x),s(y)) -> ?2(orient(x,y),x,y)
16.43/4.82	        orient(s(x),0()) -> pair(0(),s(x))
16.43/4.82	      Restore Modifier:
16.43/4.82	       DPs:
16.43/4.82	        cons#(x,cons(y,rest)) -> ?1#(orient(x,y),x,y,rest)
16.43/4.82	       TRS:
16.43/4.82	        ?1(pair(z1,z2),x,y,rest) -> cons(z1,cons(z2,rest))
16.43/4.82	        cons(x,cons(y,rest)) -> ?1(orient(x,y),x,y,rest)
16.43/4.82	        cons(x,cons(x,rest)) -> cons(x,rest)
16.43/4.82	        ?2(pair(z1,z2),x,y) -> pair(s(z1),s(z2))
16.43/4.82	        orient(s(x),s(y)) -> ?2(orient(x,y),x,y)
16.43/4.82	        orient(s(x),0()) -> pair(0(),s(x))
16.43/4.82	       SCC Processor:
16.43/4.82	        #sccs: 0
16.43/4.82	        #rules: 0
16.43/4.82	        #arcs: 4/1
16.43/4.82	        
16.43/4.82	    
16.43/4.82	    DPs:
16.43/4.82	     orient#(s(x),s(y)) -> orient#(x,y)
16.43/4.82	    TRS:
16.43/4.82	     ?1(pair(z1,z2),x,y,rest) -> cons(z1,cons(z2,rest))
16.43/4.82	     cons(x,cons(y,rest)) -> ?1(orient(x,y),x,y,rest)
16.43/4.82	     cons(x,cons(x,rest)) -> cons(x,rest)
16.43/4.82	     ?2(pair(z1,z2),x,y) -> pair(s(z1),s(z2))
16.43/4.83	     orient(s(x),s(y)) -> ?2(orient(x,y),x,y)
16.43/4.83	     orient(s(x),0()) -> pair(0(),s(x))
16.43/4.83	    Subterm Criterion Processor:
16.43/4.83	     simple projection:
16.43/4.83	      pi(orient#) = 0
16.43/4.83	     problem:
16.43/4.83	      DPs:
16.43/4.83	       
16.43/4.83	      TRS:
16.43/4.83	       ?1(pair(z1,z2),x,y,rest) -> cons(z1,cons(z2,rest))
16.43/4.83	       cons(x,cons(y,rest)) -> ?1(orient(x,y),x,y,rest)
16.43/4.83	       cons(x,cons(x,rest)) -> cons(x,rest)
16.43/4.83	       ?2(pair(z1,z2),x,y) -> pair(s(z1),s(z2))
16.43/4.83	       orient(s(x),s(y)) -> ?2(orient(x,y),x,y)
16.43/4.83	       orient(s(x),0()) -> pair(0(),s(x))
16.43/4.83	     Qed
16.43/4.83	This critical pair is conditional.
16.43/4.83	This critical pair has some non-trivial conditions.
16.43/4.83	ConCon could not decide whether all 6 critical pairs are joinable or not.
16.43/4.83	Overlap: (rule1: cons(x', cons($1, z')) -> cons(y', cons(z, z')) <= orient(x', $1) = pair(y', z), rule2: cons($2, cons($2, y)) -> cons($2, y), pos: 2, mgu: {($2,$1), (z',cons($1, y))})
16.43/4.83	CP: cons(x', cons($1, y)) = cons(y', cons(z, cons($1, y))) <= orient(x', $1) = pair(y', z)
16.43/4.83	ConCon could not decide infeasibility of this critical pair.
16.43/4.83	'\Sigma(orient(x', $1)) \cap (->^*_R)[\Sigma(REN(pair(y', z)))]' is not empty.
16.43/4.83	
16.43/4.88	EOF