159.59/43.73	MAYBE
159.59/43.73	(UNSUPPORTED)
159.59/43.73	ConCon could not decide confluence of the system.
159.59/43.73	This system is oriented.
159.59/43.73	This system is of type 3 or smaller.
159.59/43.73	This system is right-stable.
159.59/43.73	This system is properly oriented.
159.59/43.73	This is an overlay system.
159.59/43.73	This system is left-linear.
159.59/43.73	This critical pair is not trivial.
159.59/43.73	Overlap: (rule1: mod(z, s(x')) -> mod(minus(z, s(x')), s(x')) <= lte(s(x'), z) = true, rule2: mod(y', s(z')) -> y' <= lte(s(z'), y') = false, pos: ε, mgu: {(y',z), (z',x')})
159.59/43.73	CP: z = mod(minus(z, s(x')), s(x')) <= lte(s(x'), z) = true, lte(s(x'), z) = false
159.59/43.73	This critical pair is infeasible.
159.59/43.73	This critical pair is conditional.
159.59/43.73	This critical pair has some non-trivial conditions.
159.59/43.73	Overlap: (rule1: div(s(x'), s(y')) -> s(z) <= lte(s(x'), y') = false, div(minus(x', y'), s(y')) = z, rule2: div(s(z'), s($1)) -> 0 <= lte(s(z'), $1) = true, pos: ε, mgu: {(z',x'), ($1,y')})
159.59/43.73	CP: 0 = s(z) <= lte(s(x'), y') = false, div(minus(x', y'), s(y')) = z, lte(s(x'), y') = true
159.59/43.73	This critical pair is infeasible.
159.59/43.73	This critical pair is conditional.
159.59/43.73	This critical pair has some non-trivial conditions.
159.59/43.73	Overlap: (rule1: power(y', x') -> mult(mult(z', z'), y') <= mod(x', s(s(0))) = s($1), power(y', div(x', s(s(0)))) = z', rule2: power(y, 0) -> s(0), pos: ε, mgu: {(y,y'), (x',0)})
159.59/43.73	CP: s(0) = mult(mult(z', z'), y') <= mod(0, s(s(0))) = s($1), power(y', div(0, s(s(0)))) = z'
159.59/43.73	This critical pair is infeasible.
159.59/43.73	This critical pair is conditional.
159.59/43.73	This critical pair has some non-trivial conditions.
159.59/43.73	Overlap: (rule1: mod(z, s(x')) -> mod(minus(z, s(x')), s(x')) <= lte(s(x'), z) = true, rule2: mod(0, x) -> 0, pos: ε, mgu: {(z,0), (x,s(x'))})
159.59/43.73	CP: 0 = mod(minus(0, s(x')), s(x')) <= lte(s(x'), 0) = true
159.59/43.73	This critical pair is infeasible.
159.59/43.73	This critical pair is conditional.
159.59/43.73	This critical pair has some non-trivial conditions.
159.59/43.73	This critical pair is conditional.
159.59/43.73	This critical pair has some non-trivial conditions.
159.59/43.73	Some of the 16 critical pairs are not trivial and  ConCon could not decide whether those all are infeasible.
159.59/43.73	Overlap: (rule1: power(y, 0) -> s(0), rule2: power(x', z) -> mult(mult(y', y'), s(0)) <= mod(z, s(s(0))) = 0, power(x', div(z, s(s(0)))) = y', pos: ε, mgu: {(x',y), (z,0)})
159.59/43.73	CP: mult(mult(y', y'), s(0)) = s(0) <= mod(0, s(s(0))) = 0, power(y, div(0, s(s(0)))) = y'
159.59/43.73	ConCon could not decide infeasibility of this critical pair.
159.59/43.73	EOF