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