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