5.51/2.22	MAYBE
5.51/2.23	
5.51/2.23	Proof:
5.51/2.23	ConCon could not decide confluence of the system.
5.51/2.23	\cite{ALS94}, Theorem 4.1 does not apply.
5.51/2.23	This system is of type 3 or smaller.
5.51/2.23	This system is strongly deterministic.
5.51/2.23	This system is quasi-decreasing.
5.51/2.23	By \cite{A14}, Theorem 11.5.9.
5.51/2.23	This system is of type 3 or smaller.
5.51/2.23	This system is deterministic.
5.51/2.23	System R transformed to V(R) + Emb.
5.51/2.23	This system is terminating.
5.51/2.23	Call external tool:
5.51/2.23	./ttt2.sh
5.51/2.23	Input:
5.51/2.23	(VAR x)
5.51/2.23	(RULES
5.51/2.23	  f(g(x)) -> x
5.51/2.23	  g(s(x)) -> g(x)
5.51/2.23	  s(x) -> x
5.51/2.23	  g(x) -> x
5.51/2.23	  f(x) -> x
5.51/2.23	)
5.51/2.23	
5.51/2.23	 KBO Processor:
5.51/2.23	  weight function:
5.51/2.23	   w0 = 1
5.51/2.23	   w(s) = w(g) = 1
5.51/2.23	   w(f) = 0
5.51/2.23	  precedence:
5.51/2.23	   f > s ~ g
5.51/2.23	  problem:
5.51/2.23	   
5.51/2.23	  Qed
5.51/2.23	This critical pair is conditional.
5.51/2.23	This critical pair has some non-trivial conditions.
5.51/2.23	ConCon could not decide whether all 1 critical pairs are joinable or not.
5.51/2.23	Overlap: (rule1: f(g(y)) -> y <= y = s(0), rule2: g(s(z)) -> g(z), pos: 1, mgu: {(y,s(z))})
5.51/2.23	CP: f(g(z)) = s(z) <= s(z) = s(0)
5.51/2.23	ConCon could not decide infeasibility of this critical pair.
5.51/2.23	don't know if infeasible
5.51/2.23	
5.51/2.25	EOF