48.22/21.35	MAYBE
48.22/21.35	
48.22/21.35	Proof:
48.22/21.35	ConCon could not decide confluence of the system.
48.22/21.35	\cite{ALS94}, Theorem 4.1 does not apply.
48.22/21.35	This system is of type 3 or smaller.
48.22/21.35	This system is strongly deterministic.
48.22/21.35	This system is quasi-decreasing.
48.22/21.35	By \cite{O02}, p. 214, Proposition 7.2.50.
48.22/21.35	This system is of type 3 or smaller.
48.22/21.35	This system is deterministic.
48.22/21.35	System R transformed to U(R).
48.22/21.35	This system is terminating.
48.22/21.35	Call external tool:
48.22/21.35	./ttt2.sh
48.22/21.35	Input:
48.22/21.35	  ssp(nil, 0) -> nil
48.22/21.35	  ?1(xs, y, ys', v) -> xs
48.22/21.35	  ssp(cons(y, ys'), v) -> ?1(ssp(ys', v), y, ys', v)
48.22/21.35	  ?3(xs', y, ys', v, w) -> cons(y, xs')
48.22/21.35	  ?2(w, y, ys', v) -> ?3(ssp(ys', w), y, ys', v, w)
48.22/21.35	  ssp(cons(y, ys'), v) -> ?2(sub(v, y), y, ys', v)
48.22/21.35	  sub(z, 0) -> z
48.22/21.35	  ?4(z, v, w) -> z
48.22/21.35	  sub(s(v), s(w)) -> ?4(sub(v, w), v, w)
48.22/21.35	
48.22/21.35	 DP Processor:
48.22/21.35	  DPs:
48.22/21.35	   ssp#(cons(y,ys'),v) -> ssp#(ys',v)
48.22/21.35	   ssp#(cons(y,ys'),v) -> ?1#(ssp(ys',v),y,ys',v)
48.22/21.35	   ?2#(w,y,ys',v) -> ssp#(ys',w)
48.22/21.35	   ?2#(w,y,ys',v) -> ?3#(ssp(ys',w),y,ys',v,w)
48.22/21.35	   ssp#(cons(y,ys'),v) -> sub#(v,y)
48.22/21.35	   ssp#(cons(y,ys'),v) -> ?2#(sub(v,y),y,ys',v)
48.22/21.35	   sub#(s(v),s(w)) -> sub#(v,w)
48.22/21.35	   sub#(s(v),s(w)) -> ?4#(sub(v,w),v,w)
48.22/21.35	  TRS:
48.22/21.35	   ssp(nil(),0()) -> nil()
48.22/21.35	   ?1(xs,y,ys',v) -> xs
48.22/21.35	   ssp(cons(y,ys'),v) -> ?1(ssp(ys',v),y,ys',v)
48.22/21.35	   ?3(xs',y,ys',v,w) -> cons(y,xs')
48.22/21.35	   ?2(w,y,ys',v) -> ?3(ssp(ys',w),y,ys',v,w)
48.22/21.35	   ssp(cons(y,ys'),v) -> ?2(sub(v,y),y,ys',v)
48.22/21.35	   sub(z,0()) -> z
48.22/21.35	   ?4(z,v,w) -> z
48.22/21.35	   sub(s(v),s(w)) -> ?4(sub(v,w),v,w)
48.22/21.35	  TDG Processor:
48.22/21.35	   DPs:
48.22/21.35	    ssp#(cons(y,ys'),v) -> ssp#(ys',v)
48.22/21.35	    ssp#(cons(y,ys'),v) -> ?1#(ssp(ys',v),y,ys',v)
48.22/21.35	    ?2#(w,y,ys',v) -> ssp#(ys',w)
48.22/21.35	    ?2#(w,y,ys',v) -> ?3#(ssp(ys',w),y,ys',v,w)
48.22/21.35	    ssp#(cons(y,ys'),v) -> sub#(v,y)
48.22/21.35	    ssp#(cons(y,ys'),v) -> ?2#(sub(v,y),y,ys',v)
48.22/21.35	    sub#(s(v),s(w)) -> sub#(v,w)
48.22/21.35	    sub#(s(v),s(w)) -> ?4#(sub(v,w),v,w)
48.22/21.35	   TRS:
48.22/21.35	    ssp(nil(),0()) -> nil()
48.22/21.35	    ?1(xs,y,ys',v) -> xs
48.22/21.35	    ssp(cons(y,ys'),v) -> ?1(ssp(ys',v),y,ys',v)
48.22/21.35	    ?3(xs',y,ys',v,w) -> cons(y,xs')
48.22/21.35	    ?2(w,y,ys',v) -> ?3(ssp(ys',w),y,ys',v,w)
48.22/21.35	    ssp(cons(y,ys'),v) -> ?2(sub(v,y),y,ys',v)
48.22/21.35	    sub(z,0()) -> z
48.22/21.35	    ?4(z,v,w) -> z
48.22/21.35	    sub(s(v),s(w)) -> ?4(sub(v,w),v,w)
48.22/21.35	   graph:
48.22/21.35	    sub#(s(v),s(w)) -> sub#(v,w) ->
48.22/21.35	    sub#(s(v),s(w)) -> ?4#(sub(v,w),v,w)
48.22/21.35	    sub#(s(v),s(w)) -> sub#(v,w) -> sub#(s(v),s(w)) -> sub#(v,w)
48.22/21.35	    ?2#(w,y,ys',v) -> ssp#(ys',w) ->
48.22/21.35	    ssp#(cons(y,ys'),v) -> ?2#(sub(v,y),y,ys',v)
48.22/21.35	    ?2#(w,y,ys',v) -> ssp#(ys',w) -> ssp#(cons(y,ys'),v) -> sub#(v,y)
48.22/21.35	    ?2#(w,y,ys',v) -> ssp#(ys',w) ->
48.22/21.35	    ssp#(cons(y,ys'),v) -> ?1#(ssp(ys',v),y,ys',v)
48.22/21.35	    ?2#(w,y,ys',v) -> ssp#(ys',w) ->
48.22/21.35	    ssp#(cons(y,ys'),v) -> ssp#(ys',v)
48.22/21.35	    ssp#(cons(y,ys'),v) -> sub#(v,y) ->
48.22/21.35	    sub#(s(v),s(w)) -> ?4#(sub(v,w),v,w)
48.22/21.35	    ssp#(cons(y,ys'),v) -> sub#(v,y) ->
48.22/21.35	    sub#(s(v),s(w)) -> sub#(v,w)
48.22/21.35	    ssp#(cons(y,ys'),v) -> ?2#(sub(v,y),y,ys',v) ->
48.22/21.35	    ?2#(w,y,ys',v) -> ?3#(ssp(ys',w),y,ys',v,w)
48.22/21.35	    ssp#(cons(y,ys'),v) -> ?2#(sub(v,y),y,ys',v) ->
48.22/21.35	    ?2#(w,y,ys',v) -> ssp#(ys',w)
48.22/21.35	    ssp#(cons(y,ys'),v) -> ssp#(ys',v) ->
48.22/21.35	    ssp#(cons(y,ys'),v) -> ?2#(sub(v,y),y,ys',v)
48.22/21.35	    ssp#(cons(y,ys'),v) -> ssp#(ys',v) ->
48.22/21.35	    ssp#(cons(y,ys'),v) -> sub#(v,y)
48.22/21.35	    ssp#(cons(y,ys'),v) -> ssp#(ys',v) ->
48.22/21.35	    ssp#(cons(y,ys'),v) -> ?1#(ssp(ys',v),y,ys',v)
48.22/21.35	    ssp#(cons(y,ys'),v) -> ssp#(ys',v) -> ssp#(cons(y,ys'),v) -> ssp#(ys',v)
48.22/21.35	   SCC Processor:
48.22/21.35	    #sccs: 2
48.22/21.35	    #rules: 4
48.22/21.35	    #arcs: 14/64
48.22/21.35	    DPs:
48.22/21.35	     ?2#(w,y,ys',v) -> ssp#(ys',w)
48.22/21.35	     ssp#(cons(y,ys'),v) -> ssp#(ys',v)
48.22/21.35	     ssp#(cons(y,ys'),v) -> ?2#(sub(v,y),y,ys',v)
48.22/21.35	    TRS:
48.22/21.35	     ssp(nil(),0()) -> nil()
48.22/21.35	     ?1(xs,y,ys',v) -> xs
48.22/21.35	     ssp(cons(y,ys'),v) -> ?1(ssp(ys',v),y,ys',v)
48.22/21.35	     ?3(xs',y,ys',v,w) -> cons(y,xs')
48.22/21.35	     ?2(w,y,ys',v) -> ?3(ssp(ys',w),y,ys',v,w)
48.22/21.35	     ssp(cons(y,ys'),v) -> ?2(sub(v,y),y,ys',v)
48.22/21.36	     sub(z,0()) -> z
48.22/21.36	     ?4(z,v,w) -> z
48.22/21.36	     sub(s(v),s(w)) -> ?4(sub(v,w),v,w)
48.22/21.36	    Subterm Criterion Processor:
48.22/21.36	     simple projection:
48.22/21.36	      pi(ssp#) = 0
48.22/21.36	      pi(?2#) = 2
48.22/21.36	     problem:
48.22/21.36	      DPs:
48.22/21.36	       ?2#(w,y,ys',v) -> ssp#(ys',w)
48.22/21.36	      TRS:
48.22/21.36	       ssp(nil(),0()) -> nil()
48.22/21.36	       ?1(xs,y,ys',v) -> xs
48.22/21.36	       ssp(cons(y,ys'),v) -> ?1(ssp(ys',v),y,ys',v)
48.22/21.36	       ?3(xs',y,ys',v,w) -> cons(y,xs')
48.22/21.36	       ?2(w,y,ys',v) -> ?3(ssp(ys',w),y,ys',v,w)
48.22/21.36	       ssp(cons(y,ys'),v) -> ?2(sub(v,y),y,ys',v)
48.22/21.36	       sub(z,0()) -> z
48.22/21.36	       ?4(z,v,w) -> z
48.22/21.36	       sub(s(v),s(w)) -> ?4(sub(v,w),v,w)
48.22/21.36	     SCC Processor:
48.22/21.36	      #sccs: 0
48.22/21.36	      #rules: 0
48.22/21.36	      #arcs: 5/1
48.22/21.36	      
48.22/21.36	    
48.22/21.36	    DPs:
48.22/21.36	     sub#(s(v),s(w)) -> sub#(v,w)
48.22/21.36	    TRS:
48.22/21.36	     ssp(nil(),0()) -> nil()
48.22/21.36	     ?1(xs,y,ys',v) -> xs
48.22/21.36	     ssp(cons(y,ys'),v) -> ?1(ssp(ys',v),y,ys',v)
48.22/21.36	     ?3(xs',y,ys',v,w) -> cons(y,xs')
48.22/21.36	     ?2(w,y,ys',v) -> ?3(ssp(ys',w),y,ys',v,w)
48.22/21.36	     ssp(cons(y,ys'),v) -> ?2(sub(v,y),y,ys',v)
48.22/21.36	     sub(z,0()) -> z
48.22/21.36	     ?4(z,v,w) -> z
48.22/21.36	     sub(s(v),s(w)) -> ?4(sub(v,w),v,w)
48.22/21.36	    Subterm Criterion Processor:
48.22/21.36	     simple projection:
48.22/21.36	      pi(sub#) = 0
48.22/21.36	     problem:
48.22/21.36	      DPs:
48.22/21.36	       
48.22/21.36	      TRS:
48.22/21.36	       ssp(nil(),0()) -> nil()
48.22/21.36	       ?1(xs,y,ys',v) -> xs
48.22/21.36	       ssp(cons(y,ys'),v) -> ?1(ssp(ys',v),y,ys',v)
48.22/21.36	       ?3(xs',y,ys',v,w) -> cons(y,xs')
48.22/21.36	       ?2(w,y,ys',v) -> ?3(ssp(ys',w),y,ys',v,w)
48.22/21.36	       ssp(cons(y,ys'),v) -> ?2(sub(v,y),y,ys',v)
48.22/21.36	       sub(z,0()) -> z
48.22/21.36	       ?4(z,v,w) -> z
48.22/21.36	       sub(s(v),s(w)) -> ?4(sub(v,w),v,w)
48.22/21.36	     Qed
48.22/21.36	This critical pair is conditional.
48.22/21.36	This critical pair has some non-trivial conditions.
48.22/21.36	ConCon could not decide whether all 2 critical pairs are joinable or not.
48.22/21.36	Overlap: (rule1: ssp(cons(y', z), x) -> cons(y', x') <= sub(x, y') = z', ssp(z, z') = x', rule2: ssp(cons($3, $4), $1) -> $2 <= ssp($4, $1) = $2, pos: ε, mgu: {($3,y'), ($4,z), ($1,x)})
48.22/21.36	CP: $2 = cons(y', x') <= sub(x, y') = z', ssp(z, z') = x', ssp(z, x) = $2
48.22/21.36	ConCon could not decide infeasibility of this critical pair.
48.22/21.36	'\Sigma(conds(sub(x, y'), ssp(z, z'), ssp(z, x))) \cap (->^*_R)[\Sigma(REN(conds(z', x', $2)))]' is not empty.
48.22/21.36	'\Sigma(conds(sub(x, y'), ssp(z, x))) \cap (->^*_R)[\Sigma(REN(conds(z', $2)))]' is not empty.
48.22/21.36	'\Sigma(conds(sub(x, y'), ssp(z, z'))) \cap (->^*_R)[\Sigma(REN(conds(z', x')))]' is not empty.
48.22/21.36	'\Sigma(conds(ssp(z, z'), ssp(z, x))) \cap (->^*_R)[\Sigma(REN(conds(x', $2)))]' is not empty.
48.22/21.36	'\Sigma(sub(x, y')) \cap (->^*_R)[\Sigma(REN(z'))]' is not empty.
48.22/21.36	'\Sigma(ssp(z, x)) \cap (->^*_R)[\Sigma(REN($2))]' is not empty.
48.22/21.36	'\Sigma(ssp(z, z')) \cap (->^*_R)[\Sigma(REN(x'))]' is not empty.
48.22/21.36	
48.34/21.39	EOF