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