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