116.14/30.48	MAYBE
116.14/30.48	
116.14/30.48	Proof:
116.14/30.48	ConCon could not decide confluence of the system.
116.14/30.48	\cite{ALS94}, Theorem 4.1 does not apply.
116.14/30.48	This system is of type 3 or smaller.
116.14/30.48	This system is strongly deterministic.
116.14/30.48	This system is of type 3 or smaller.
116.14/30.48	This system is deterministic.
116.14/30.48	ConCon could not decide if this system is quasi-decreasing.
116.14/30.48	\cite{O02}, p. 214, Proposition 7.2.50 does not apply.
116.14/30.48	This system is of type 3 or smaller.
116.14/30.48	This system is deterministic.
116.14/30.48	System R transformed to optimized U(R).
116.14/30.48	The external tool could not decide termination of the system.
116.14/30.48	Call external tool:
116.14/30.48	./ttt2.sh
116.14/30.48	Input:
116.14/30.48	  mult(s(x), y) -> add(mult(x, y), y)
116.14/30.48	  add(s(x), y) -> s(add(x, y))
116.14/30.48	  lte(s(x), 0) -> false
116.14/30.48	  minus(0, s(y)) -> 0
116.14/30.48	  div(s(x), s(y)) -> ?2(lte(s(x), y), x, y)
116.14/30.48	  ?2(false, x, y) -> ?3(div(minus(x, y), s(y)), x, y)
116.14/30.48	  ?3(q, x, y) -> s(q)
116.14/30.48	  div(0, s(x)) -> 0
116.14/30.48	  mod(x, s(y)) -> ?1(lte(s(y), x), x, y)
116.14/30.48	  ?1(false, x, y) -> x
116.14/30.48	  mod(x, s(y)) -> ?1(lte(s(y), x), x, y)
116.14/30.48	  ?1(true, x, y) -> mod(minus(x, s(y)), s(y))
116.14/30.48	  minus(s(x), s(y)) -> minus(x, y)
116.14/30.48	  div(s(x), s(y)) -> ?2(lte(s(x), y), x, y)
116.14/30.48	  ?2(true, x, y) -> 0
116.14/30.48	  power(x, n) -> ?4(mod(n, s(s(0))), x, n)
116.14/30.48	  ?4(s(z), x, n) -> ?6(power(x, div(n, s(s(0)))), x, n, z)
116.14/30.48	  ?6(y, x, n, z) -> mult(mult(y, y), x)
116.14/30.48	  mult(0, y) -> 0
116.14/30.48	  power(x, 0) -> s(0)
116.14/30.48	  mod(x, 0) -> x
116.14/30.48	  lte(s(x), s(y)) -> lte(x, y)
116.14/30.48	  add(0, x) -> x
116.14/30.48	  mod(0, y) -> 0
116.14/30.48	  minus(x, 0) -> x
116.14/30.48	  lte(0, y) -> true
116.14/30.48	  power(x, n) -> ?4(mod(n, s(s(0))), x, n)
116.14/30.48	  ?4(0, x, n) -> ?5(power(x, div(n, s(s(0)))), x, n)
116.14/30.48	  ?5(y, x, n) -> mult(mult(y, y), s(0))
116.14/30.48	
116.14/30.48	
116.76/30.51	EOF