0.003/0.003	NO
0.003/0.003	
0.003/0.003	Problem 1:
0.003/0.003	
0.003/0.003	
0.003/0.003	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
0.003/0.003	Confluence Problem:
0.003/0.003	(VAR vNonEmpty v w y z xs xs' ys')
0.003/0.003	(REPLACEMENT-MAP
0.003/0.003	(ssp 1, 2)
0.003/0.003	(sub 1, 2)
0.003/0.003	(0)
0.003/0.003	(cons 1, 2)
0.003/0.003	(fSNonEmpty)
0.003/0.003	(nil)
0.003/0.003	(s 1)
0.003/0.003	)
0.003/0.003	(RULES
0.003/0.003	ssp(cons(y,ys'),v) -> cons(y,xs') | sub(v,y) ->* w, ssp(ys',w) ->* xs'
0.003/0.003	ssp(cons(y,ys'),v) -> xs | ssp(ys',v) ->* xs
0.003/0.003	ssp(nil,0) -> nil
0.003/0.003	sub(s(v),s(w)) -> z | sub(v,w) ->* z
0.003/0.003	sub(z,0) -> z
0.003/0.003	)
0.003/0.003	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
0.003/0.003	
0.003/0.003	
0.003/0.003	Problem 1:
0.003/0.003	
0.003/0.003	Inlining of Conditions Processor [STERN17]:
0.003/0.003	
0.003/0.003	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
0.003/0.003	Confluence Problem:
0.003/0.003	(VAR vNonEmpty v w y z xs xs' ys')
0.003/0.003	(REPLACEMENT-MAP
0.003/0.003	(ssp 1, 2)
0.003/0.003	(sub 1, 2)
0.003/0.003	(0)
0.003/0.003	(cons 1, 2)
0.003/0.003	(fSNonEmpty)
0.003/0.003	(nil)
0.003/0.003	(s 1)
0.003/0.003	)
0.003/0.003	(RULES
0.003/0.003	ssp(cons(y,ys'),v) -> ssp(ys',v)
0.003/0.003	ssp(cons(y,ys'),v) -> cons(y,ssp(ys',sub(v,y)))
0.003/0.003	ssp(nil,0) -> nil
0.003/0.003	sub(s(v),s(w)) -> sub(v,w)
0.003/0.003	sub(z,0) -> z
0.003/0.003	)
0.003/0.003	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
0.003/0.003	
0.003/0.003	
0.003/0.003	Problem 1:
0.003/0.003	
0.003/0.003	Clean CTRS Processor:
0.003/0.003	
0.003/0.003	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
0.003/0.003	Confluence Problem:
0.003/0.003	(VAR v w y z ys')
0.003/0.003	(REPLACEMENT-MAP
0.003/0.003	(ssp 1, 2)
0.003/0.003	(sub 1, 2)
0.003/0.003	(0)
0.003/0.003	(cons 1, 2)
0.003/0.003	(fSNonEmpty)
0.003/0.003	(nil)
0.003/0.003	(s 1)
0.003/0.003	)
0.003/0.003	(RULES
0.003/0.003	ssp(cons(y,ys'),v) -> ssp(ys',v)
0.003/0.003	ssp(cons(y,ys'),v) -> cons(y,ssp(ys',sub(v,y)))
0.003/0.003	ssp(nil,0) -> nil
0.003/0.003	sub(s(v),s(w)) -> sub(v,w)
0.003/0.003	sub(z,0) -> z
0.003/0.003	)
0.003/0.003	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
0.003/0.003	
0.003/0.003	CRule InfChecker Info:
0.003/0.003	ssp(cons(y,ys'),v) -> ssp(ys',v)
0.003/0.003	Rule remains
0.003/0.003	Proof:
0.003/0.003	NO_CONDS
0.003/0.003	
0.003/0.003	CRule InfChecker Info:
0.003/0.003	ssp(cons(y,ys'),v) -> cons(y,ssp(ys',sub(v,y)))
0.003/0.003	Rule remains
0.003/0.003	Proof:
0.003/0.003	NO_CONDS
0.003/0.003	
0.003/0.003	CRule InfChecker Info:
0.003/0.003	ssp(nil,0) -> nil
0.003/0.003	Rule remains
0.003/0.003	Proof:
0.003/0.003	NO_CONDS
0.003/0.003	
0.003/0.003	CRule InfChecker Info:
0.003/0.003	sub(s(v),s(w)) -> sub(v,w)
0.003/0.003	Rule remains
0.003/0.003	Proof:
0.003/0.003	NO_CONDS
0.003/0.003	
0.003/0.003	CRule InfChecker Info:
0.003/0.003	sub(z,0) -> z
0.003/0.003	Rule remains
0.003/0.003	Proof:
0.003/0.003	NO_CONDS
0.003/0.003	
0.003/0.003	Problem 1:
0.003/0.003	
0.003/0.003	Transform No Conds CTRS Processor:
0.003/0.003	
0.003/0.003	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
0.003/0.003	Confluence Problem:
0.003/0.003	(VAR v w y z ys')
0.003/0.003	(REPLACEMENT-MAP
0.003/0.003	(ssp 1, 2)
0.003/0.003	(sub 1, 2)
0.003/0.003	(0)
0.003/0.003	(cons 1, 2)
0.003/0.003	(fSNonEmpty)
0.003/0.003	(nil)
0.003/0.003	(s 1)
0.003/0.003	)
0.003/0.003	(RULES
0.003/0.003	ssp(cons(y,ys'),v) -> ssp(ys',v)
0.003/0.003	ssp(cons(y,ys'),v) -> cons(y,ssp(ys',sub(v,y)))
0.003/0.003	ssp(nil,0) -> nil
0.003/0.003	sub(s(v),s(w)) -> sub(v,w)
0.003/0.003	sub(z,0) -> z
0.003/0.003	)
0.003/0.003	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
0.003/0.003	Resulting R:
0.003/0.003	(VAR v w y z ys')
0.003/0.003	(STRATEGY CONTEXTSENSITIVE
0.003/0.003	(ssp 1 2)
0.003/0.003	(sub 1 2)
0.003/0.003	(0)
0.003/0.003	(cons 1 2)
0.003/0.003	(fSNonEmpty)
0.003/0.003	(nil)
0.003/0.003	(s 1)
0.003/0.003	)
0.003/0.003	(RULES
0.003/0.003	ssp(cons(y,ys'),v) -> ssp(ys',v)
0.003/0.003	ssp(cons(y,ys'),v) -> cons(y,ssp(ys',sub(v,y)))
0.003/0.003	ssp(nil,0) -> nil
0.003/0.003	sub(s(v),s(w)) -> sub(v,w)
0.003/0.003	sub(z,0) -> z
0.003/0.003	)
0.003/0.003	
0.003/0.003	Problem 1:
0.003/0.003	
0.003/0.003	CleanTRS Processor:
0.003/0.003	
0.003/0.003	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
0.003/0.003	Confluence Problem:
0.003/0.003	(VAR v w y z ys')
0.003/0.003	(REPLACEMENT-MAP
0.003/0.003	(ssp 1, 2)
0.003/0.003	(sub 1, 2)
0.003/0.003	(0)
0.003/0.003	(cons 1, 2)
0.003/0.003	(fSNonEmpty)
0.003/0.003	(nil)
0.003/0.003	(s 1)
0.003/0.003	)
0.003/0.003	(RULES
0.003/0.003	ssp(cons(y,ys'),v) -> ssp(ys',v)
0.003/0.003	ssp(cons(y,ys'),v) -> cons(y,ssp(ys',sub(v,y)))
0.003/0.003	ssp(nil,0) -> nil
0.003/0.003	sub(s(v),s(w)) -> sub(v,w)
0.003/0.003	sub(z,0) -> z
0.003/0.003	)
0.003/0.003	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
0.003/0.003	
0.003/0.003	
0.003/0.003	Problem 1:
0.003/0.003	
0.003/0.003	Modular Confluence Combinations Decomposition Processor:
0.003/0.003	
0.003/0.003	No usable combinations
0.003/0.003	
0.003/0.003	Problem 1:
0.003/0.003	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
0.003/0.003	Confluence Problem:
0.003/0.003	(VAR v w y z ys')
0.003/0.003	(REPLACEMENT-MAP
0.003/0.003	(ssp 1, 2)
0.003/0.003	(sub 1, 2)
0.003/0.003	(0)
0.003/0.003	(cons 1, 2)
0.003/0.003	(fSNonEmpty)
0.003/0.003	(nil)
0.003/0.003	(s 1)
0.003/0.003	)
0.003/0.003	(RULES
0.003/0.003	ssp(cons(y,ys'),v) -> ssp(ys',v)
0.003/0.003	ssp(cons(y,ys'),v) -> cons(y,ssp(ys',sub(v,y)))
0.003/0.003	ssp(nil,0) -> nil
0.003/0.003	sub(s(v),s(w)) -> sub(v,w)
0.003/0.003	sub(z,0) -> z
0.003/0.003	)
0.003/0.003	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
0.003/0.003	
0.003/0.003	Huet Levy Processor:
0.003/0.003	-> Rules:
0.003/0.003	 ssp(cons(y,ys'),v) -> ssp(ys',v)
0.003/0.003	 ssp(cons(y,ys'),v) -> cons(y,ssp(ys',sub(v,y)))
0.003/0.003	 ssp(nil,0) -> nil
0.003/0.003	 sub(s(v),s(w)) -> sub(v,w)
0.003/0.003	 sub(z,0) -> z
0.003/0.003	-> Vars:
0.003/0.003	 v, y, ys', v, y, ys', v, w, z
0.003/0.003	
0.003/0.003	-> Rlps:
0.003/0.003	 (rule: ssp(cons(y,ys'),v) -> ssp(ys',v), id: 1, possubterms: ssp(cons(y,ys'),v)->[], cons(y,ys')->[1])
0.003/0.003	 (rule: ssp(cons(y,ys'),v) -> cons(y,ssp(ys',sub(v,y))), id: 2, possubterms: ssp(cons(y,ys'),v)->[], cons(y,ys')->[1])
0.003/0.003	 (rule: ssp(nil,0) -> nil, id: 3, possubterms: ssp(nil,0)->[], nil->[1], 0->[2])
0.003/0.003	 (rule: sub(s(v),s(w)) -> sub(v,w), id: 4, possubterms: sub(s(v),s(w))->[], s(v)->[1], s(w)->[2])
0.003/0.003	 (rule: sub(z,0) -> z, id: 5, possubterms: sub(z,0)->[], 0->[2])
0.003/0.003	
0.003/0.003	-> Unifications:
0.003/0.003	(R2 unifies with R1 at p: [], l: ssp(cons(y,ys'),v), lp: ssp(cons(y,ys'),v), sig: {v -> v',y -> y',ys' -> ys''}, l': ssp(cons(y',ys''),v'), r: cons(y,ssp(ys',sub(v,y))), r': ssp(ys'',v'))
0.003/0.003	
0.003/0.003	-> Critical pairs info:
0.003/0.003	<ssp(ys'',v'),cons(y',ssp(ys'',sub(v',y')))>   =>  Not trivial, Overlay, NW0, N1
0.003/0.003	
0.003/0.003	-> Problem conclusions:
0.003/0.003	 Left linear, Not right linear, Not linear
0.003/0.003	 Not weakly orthogonal, Not almost orthogonal, Not orthogonal
0.003/0.003	 Not Huet-Levy confluent, Not Newman confluent
0.003/0.003	 R is a TRS
0.003/0.003	
0.003/0.003	
0.003/0.003	Problem 1:
0.003/0.003	Different Normal CP Terms Processor:
0.003/0.003	<ssp(ys'',v'),cons(y',ssp(ys'',sub(v',y')))>   =>  Not trivial, Overlay, NW0, N1, Normal and not trivial cp
0.003/0.003	
0.003/0.003	The problem is not joinable.
0.003/0.003	0.01user 0.00system 0:00.03elapsed 54%CPU (0avgtext+0avgdata 10604maxresident)k
0.003/0.003	8inputs+0outputs (0major+1619minor)pagefaults 0swaps