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