8.68/3.06	YES
8.68/3.06	
8.68/3.06	Proof:
8.68/3.06	This system is confluent.
8.68/3.06	By \cite{SMI95}, Corollary 4.7 or 5.3.
8.68/3.06	This system is oriented.
8.68/3.06	This system is of type 3 or smaller.
8.68/3.06	This system is right-stable.
8.68/3.06	This system is properly oriented.
8.68/3.06	This is an overlay system.
8.68/3.06	This system is left-linear.
8.68/3.08	All 2 critical pairs are trivial or infeasible.
8.68/3.08	Overlap: (rule1: f(z, x') -> h(s(z)) <= c(h(z)) = c(a), rule2: f(y', z') -> g(s(y')) <= c(g(y')) = c(a), pos: ε, mgu: {(z,y'), (x',z')})
8.68/3.08	CP: g(s(y')) = h(s(y')) <= c(h(y')) = c(a), c(g(y')) = c(a)
8.68/3.09	This critical pair is infeasible.
8.68/3.09	This critical pair is conditional.
8.68/3.09	This critical pair has some non-trivial conditions.
8.68/3.09	Call external tool:
8.68/3.09	./waldmeister
8.68/3.09	Input:
8.68/3.09	  f(x, y) -> g(s(x)) <= c(g(x)) = c(a)
8.68/3.09	  f(x, y) -> h(s(x)) <= c(h(x)) = c(a)
8.68/3.09	  g(s(x)) -> x
8.68/3.09	  h(s(x)) -> x
8.68/3.09	
8.68/3.09	By Waldmeister.
8.68/3.09	Overlap: (rule1: f(z, x') -> g(s(z)) <= c(g(z)) = c(a), rule2: f(y', z') -> h(s(y')) <= c(h(y')) = c(a), pos: ε, mgu: {(z,y'), (x',z')})
8.68/3.09	CP: h(s(y')) = g(s(y')) <= c(g(y')) = c(a), c(h(y')) = c(a)
8.68/3.09	This critical pair is infeasible.
8.68/3.09	This critical pair is conditional.
8.68/3.09	This critical pair has some non-trivial conditions.
8.68/3.09	Call external tool:
8.68/3.09	./waldmeister
8.68/3.09	Input:
8.68/3.09	  f(x, y) -> g(s(x)) <= c(g(x)) = c(a)
8.68/3.09	  f(x, y) -> h(s(x)) <= c(h(x)) = c(a)
8.68/3.09	  g(s(x)) -> x
8.68/3.09	  h(s(x)) -> x
8.68/3.09	
8.68/3.09	By Waldmeister.
8.68/3.09	
9.39/3.22	EOF