101.77/30.87	MAYBE
101.77/30.87	(UNSUPPORTED)
101.77/30.87	ConCon could not decide confluence of the system.
101.77/30.87	\cite{ALS94}, Theorem 4.1 does not apply.
101.77/30.87	This system is of type 3 or smaller.
101.77/30.87	This system is absolutely deterministic.
101.77/30.87	The external tool could not decide termination of the system.
101.77/30.87	Call external tool:
101.77/30.87	./ttt2.sh
101.77/30.87	Input:
101.77/30.87	(VAR x y n z)
101.77/30.87	(RULES
101.77/30.87	  mult(s(x), y) -> add(mult(x, y), y)
101.77/30.87	  add(s(x), y) -> s(add(x, y))
101.77/30.87	  lte(s(x), 0) -> false
101.77/30.87	  minus(0, s(y)) -> 0
101.77/30.87	  div(0, s(x)) -> 0
101.77/30.87	  mod(x, s(y)) -> U1(lte(s(y), x), x, y)
101.77/30.87	  U1(false, x, y) -> x
101.77/30.87	  div(s(x), s(y)) -> U2(lte(s(x), y), x, y)
101.77/30.87	  U2(false, x, y) -> s(div(minus(x, y), s(y)))
101.77/30.87	  mod(x, s(y)) -> U1(lte(s(y), x), x, y)
101.77/30.87	  U1(true, x, y) -> mod(minus(x, s(y)), s(y))
101.77/30.87	  minus(s(x), s(y)) -> minus(x, y)
101.77/30.87	  div(s(x), s(y)) -> U2(lte(s(x), y), x, y)
101.77/30.87	  U2(true, x, y) -> 0
101.77/30.87	  mult(0, y) -> 0
101.77/30.87	  power(x, 0) -> s(0)
101.77/30.87	  mod(x, 0) -> x
101.77/30.87	  lte(s(x), s(y)) -> lte(x, y)
101.77/30.87	  add(0, x) -> x
101.77/30.87	  mod(0, y) -> 0
101.77/30.87	  power(x, n) -> U3(mod(n, s(s(0))), x, n)
101.77/30.87	  U3(0, x, n) -> mult(mult(power(x, div(n, s(s(0)))), power(x, div(n, s(s(0))))), s(0))
101.77/30.87	  power(x, n) -> U3(mod(n, s(s(0))), x, n)
101.77/30.87	  U3(s(z), x, n) -> mult(mult(power(x, div(n, s(s(0)))), power(x, div(n, s(s(0))))), x)
101.77/30.87	  minus(x, 0) -> x
101.77/30.87	  lte(0, y) -> true
101.77/30.87	)
101.77/30.87	
101.83/30.87	EOF