8.60/2.75	YES
8.60/2.75	
8.60/2.75	Proof:
8.60/2.75	This system is confluent.
8.60/2.75	By \cite{SMI95}, Corollary 4.7 or 5.3.
8.60/2.75	This system is oriented.
8.60/2.75	This system is of type 3 or smaller.
8.60/2.75	This system is right-stable.
8.60/2.75	This system is properly oriented.
8.60/2.75	This is an overlay system.
8.60/2.75	This system is left-linear.
8.60/2.75	All 4 critical pairs are trivial or infeasible.
8.60/2.75	Overlap: (rule1: div(y', z') -> pair(s(z), x') <= leq(z', y') = true, div(m(y', z'), z') = pair(z, x'), rule2: div($1, $2) -> pair(0, $2) <= greater($2, $1) = true, pos: ε, mgu: {($1,y'), ($2,z')})
8.60/2.75	CP: pair(0, z') = pair(s(z), x') <= leq(z', y') = true, div(m(y', z'), z') = pair(z, x'), greater(z', y') = true
8.60/2.75	This critical pair is infeasible.
8.60/2.75	This critical pair is conditional.
8.60/2.75	This critical pair has some non-trivial conditions.
8.60/2.75	Call external tool:
8.60/2.75	./waldmeister
8.60/2.75	Input:
8.60/2.75	  div(x, y) -> pair(0, y) <= greater(y, x) = true
8.60/2.75	  div(x, y) -> pair(s(q), r) <= leq(y, x) = true, div(m(x, y), y) = pair(q, r)
8.60/2.75	  m(x, 0) -> x
8.60/2.75	  m(0, y) -> 0
8.60/2.75	  m(s(x), s(y)) -> m(x, y)
8.60/2.75	  greater(s(x), s(y)) -> greater(x, y)
8.60/2.75	  greater(s(x), 0) -> true
8.60/2.75	  leq(s(x), s(y)) -> leq(x, y)
8.60/2.75	  leq(0, x) -> true
8.60/2.75	
8.60/2.75	By Waldmeister.
8.60/2.75	Overlap: (rule1: div(z, x') -> pair(0, x') <= greater(x', z) = true, rule2: div($1, $2) -> pair(s(y'), z') <= leq($2, $1) = true, div(m($1, $2), $2) = pair(y', z'), pos: ε, mgu: {($1,z), ($2,x')})
8.60/2.75	CP: pair(s(y'), z') = pair(0, x') <= greater(x', z) = true, leq(x', z) = true, div(m(z, x'), x') = pair(y', z')
8.60/2.75	This critical pair is infeasible.
8.60/2.75	This critical pair is conditional.
8.60/2.75	This critical pair has some non-trivial conditions.
8.60/2.75	Call external tool:
8.60/2.75	./waldmeister
8.60/2.75	Input:
8.60/2.75	  div(x, y) -> pair(0, y) <= greater(y, x) = true
8.60/2.75	  div(x, y) -> pair(s(q), r) <= leq(y, x) = true, div(m(x, y), y) = pair(q, r)
8.60/2.75	  m(x, 0) -> x
8.60/2.75	  m(0, y) -> 0
8.60/2.75	  m(s(x), s(y)) -> m(x, y)
8.60/2.75	  greater(s(x), s(y)) -> greater(x, y)
8.60/2.75	  greater(s(x), 0) -> true
8.60/2.75	  leq(s(x), s(y)) -> leq(x, y)
8.60/2.75	  leq(0, x) -> true
8.60/2.75	
8.60/2.75	By Waldmeister.
8.60/2.75	Overlap: (rule1: m(0, x) -> 0, rule2: m(y, 0) -> y, pos: ε, mgu: {(y,0), (x,0)})
8.60/2.75	CP: 0 = 0
8.60/2.75	This critical pair is trivial.
8.60/2.75	Overlap: (rule1: m(y, 0) -> y, rule2: m(0, x) -> 0, pos: ε, mgu: {(y,0), (x,0)})
8.60/2.75	CP: 0 = 0
8.60/2.75	This critical pair is trivial.
8.60/2.75	
8.94/2.78	EOF