4.11/1.91	MAYBE
4.11/1.91	
4.11/1.91	Proof:
4.11/1.91	ConCon could not decide confluence of the system.
4.11/1.91	Inlined conditions in System R.
4.11/1.91	\cite{ALS94}, Theorem 4.1 does not apply.
4.11/1.91	This system is of type 3 or smaller.
4.11/1.91	This system is strongly deterministic.
4.11/1.91	This system is quasi-decreasing.
4.11/1.91	By \cite{O02}, p. 214, Proposition 7.2.50.
4.11/1.91	This system is of type 3 or smaller.
4.11/1.91	This system is deterministic.
4.11/1.91	System R transformed to optimized U(R).
4.11/1.91	This system is terminating.
4.11/1.91	Call external tool:
4.11/1.91	./ttt2.sh
4.11/1.91	Input:
4.11/1.91	(VAR z w v y ys')
4.11/1.91	(RULES
4.11/1.91	  ssp(cons(y, ys'), v) -> ssp(ys', v)
4.11/1.91	  ssp(cons(y, ys'), v) -> cons(y, ssp(ys', sub(v, y)))
4.11/1.91	  sub(z, 0) -> z
4.11/1.91	  ssp(nil, 0) -> nil
4.11/1.91	  sub(s(v), s(w)) -> sub(v, w)
4.11/1.91	)
4.11/1.91	
4.11/1.91	 Matrix Interpretation Processor: dim=1
4.11/1.91	  
4.11/1.91	  interpretation:
4.11/1.91	   [s](x0) = 4x0 + 4,
4.11/1.91	   
4.11/1.91	   [nil] = 4,
4.11/1.91	   
4.11/1.91	   [0] = 1,
4.11/1.91	   
4.11/1.91	   [sub](x0, x1) = x0 + 2x1 + 1,
4.11/1.91	   
4.11/1.91	   [ssp](x0, x1) = 3x0 + 2x1,
4.11/1.91	   
4.11/1.91	   [cons](x0, x1) = 2x0 + x1 + 2
4.11/1.91	  orientation:
4.11/1.91	   ssp(cons(y,ys'),v) = 2v + 6y + 3ys' + 6 >= 2v + 3ys' = ssp(ys',v)
4.11/1.91	   
4.11/1.91	   ssp(cons(y,ys'),v) = 2v + 6y + 3ys' + 6 >= 2v + 6y + 3ys' + 4 = cons(y,ssp(ys',sub(v,y)))
4.11/1.91	   
4.11/1.91	   sub(z,0()) = z + 3 >= z = z
4.11/1.91	   
4.11/1.91	   ssp(nil(),0()) = 14 >= 4 = nil()
4.11/1.91	   
4.11/1.91	   sub(s(v),s(w)) = 4v + 8w + 13 >= v + 2w + 1 = sub(v,w)
4.11/1.91	  problem:
4.11/1.91	   
4.11/1.91	  Qed
4.11/1.91	ConCon could not decide whether all 2 critical pairs are joinable or not.
4.11/1.91	Overlap: (rule1: ssp(cons(z, x'), x) -> cons(z, ssp(x', sub(x, z))), rule2: ssp(cons(z', $1), y') -> ssp($1, y'), pos: ε, mgu: {(z,z'), (x',$1), (x,y')})
4.11/1.91	CP: ssp($1, y') = cons(z', ssp($1, sub(y', z')))
4.11/1.91	ConCon could not decide unfeasibility of this critical pair.
4.11/1.91	
4.19/1.97	EOF