16.04/4.85	MAYBE
16.04/4.85	
16.04/4.85	Problem:
16.04/4.85	ssp'(xs, 0()) -> nil()
16.04/4.85	ssp'(cons(y', ws), v) -> cons(y', ys') <= sub(v, y') = w, ssp'(ws, w) = ys'
16.04/4.85	ssp'(cons(x', xs'), v) -> cons(y', ys') <= get(xs') = tp2(y', zs), sub(v, y') = w, ssp'(cons(x', zs), w) = ys'
16.04/4.85	sub(z, 0()) -> z
16.04/4.85	sub(s(v), s(w)) -> z <= sub(v, w) = z
16.04/4.85	get(cons(y, ys)) -> tp2(y, ys)
16.04/4.85	get(cons(x', xs')) -> tp2(y, cons(x', zs)) <= get(xs') = tp2(y, zs)
16.04/4.85	
16.04/4.85	Proof:
16.04/4.85	ConCon could not decide confluence of the system.
16.04/4.85	\cite{SMI95}, Corollary 4.7 or 5.3 do not apply.
16.04/4.85	Some of the 8 critical pairs are not trivial and  ConCon could not decide whether those all are infeasible.
16.04/4.85	CP: nil() = cons(y', $4) <= get($6) = tp2(y', x'), sub(0(), y') = $5, ssp'(cons($3, x'), $5) = $4:
16.04/4.85	ConCon could not decide infeasibility of this critical pair.
16.04/4.85	'\Sigma(conds(tp2(y', x'), $5, $4)) \cap (->^*_R^-1)[\Sigma(REN(conds(get($6), sub(0(), y'), ssp'(cons($3, x'), $5))))]' is not empty.
16.04/4.85	'\Sigma(conds(get($6), sub(0(), y'), ssp'(cons($3, x'), $5))) \cap (->^*_R)[\Sigma(REN(conds(tp2(y', x'), $5, $4)))]' is not empty.
16.04/4.85	'\Sigma(conds(tp2(y', x'), $5)) \cap (->^*_R^-1)[\Sigma(REN(conds(get($6), sub(0(), y'))))]' is not empty.
16.04/4.85	'\Sigma(conds(get($6), sub(0(), y'))) \cap (->^*_R)[\Sigma(REN(conds(tp2(y', x'), $5)))]' is not empty.
16.04/4.85	'\Sigma(conds($5, $4)) \cap (->^*_R^-1)[\Sigma(REN(conds(sub(0(), y'), ssp'(cons($3, x'), $5))))]' is not empty.
16.04/4.85	'\Sigma(conds(sub(0(), y'), ssp'(cons($3, x'), $5))) \cap (->^*_R)[\Sigma(REN(conds($5, $4)))]' is not empty.
16.04/4.85	'\Sigma(conds(tp2(y', x'), $4)) \cap (->^*_R^-1)[\Sigma(REN(conds(get($6), ssp'(cons($3, x'), $5))))]' is not empty.
16.04/4.85	'\Sigma(conds(get($6), ssp'(cons($3, x'), $5))) \cap (->^*_R)[\Sigma(REN(conds(tp2(y', x'), $4)))]' is not empty.
16.04/4.85	'\Sigma($4) \cap (->^*_R^-1)[\Sigma(REN(ssp'(cons($3, x'), $5)))]' is not empty.
16.04/4.85	'\Sigma(ssp'(cons($3, x'), $5)) \cap (->^*_R)[\Sigma(REN($4))]' is not empty.
16.04/4.86	'\Sigma($5) \cap (->^*_R^-1)[\Sigma(REN(sub(0(), y')))]' is not empty.
16.04/4.86	'\Sigma(sub(0(), y')) \cap (->^*_R)[\Sigma(REN($5))]' is not empty.
16.04/4.86	'\Sigma(tp2(y', x')) \cap (->^*_R^-1)[\Sigma(REN(get($6)))]' is not empty.
16.04/4.86	'\Sigma(get($6)) \cap (->^*_R)[\Sigma(REN(tp2(y', x')))]' is not empty.
16.04/4.86	
16.91/4.99	EOF