0.00/0.00	MAYBE
0.00/0.00	
0.00/0.00	Succeeded in reading "/export/starexec/sandbox2/benchmark/theBenchmark.trs".
0.00/0.00	    (CONDITIONTYPE ORIENTED)
0.00/0.00	    (VAR x y q n z x4 x1 x2 x3)
0.00/0.00	    (RULES
0.00/0.00	      add(0,x) -> x
0.00/0.00	      add(s(x),y) -> s(add(x,y))
0.00/0.00	      mult(0,y) -> 0
0.00/0.00	      mult(s(x),y) -> add(mult(x,y),y)
0.00/0.00	      lte(0,y) -> true
0.00/0.00	      lte(s(x),0) -> false
0.00/0.00	      lte(s(x),s(y)) -> lte(x,y)
0.00/0.00	      minus(0,s(y)) -> 0
0.00/0.00	      minus(x,0) -> x
0.00/0.00	      minus(s(x),s(y)) -> minus(x,y)
0.00/0.00	      mod(0,y) -> 0
0.00/0.00	      mod(x,0) -> x
0.00/0.00	      mod(x,s(y)) -> mod(minus(x,s(y)),s(y)) | lte(s(y),x) == true
0.00/0.00	      mod(x,s(y)) -> x | lte(s(y),x) == false
0.00/0.00	      div(0,s(x)) -> 0
0.00/0.00	      div(s(x),s(y)) -> 0 | lte(s(x),y) == true
0.00/0.00	      div(s(x),s(y)) -> s(q) | lte(s(x),y) == false, div(minus(x,y),s(y)) == q
0.00/0.00	      power(x,0) -> s(0)
0.00/0.00	      power(x,n) -> mult(mult(y,y),s(0)) | mod(n,s(s(0))) == 0, power(x,div(n,s(s(0)))) == y
0.00/0.00	      power(x,n) -> mult(mult(y,y),x) | mod(n,s(s(0))) == s(z), power(x,div(n,s(s(0)))) == y
0.00/0.00	    )
0.00/0.00	    (COMMENT COPS 499)
0.00/0.00	    (COMMENT submitted by: Naoki Nishida)
0.00/0.00	
0.00/0.00	No "->="-rules.
0.00/0.00	
0.00/0.00	Decomposed conditions and removed infeasible rules if possible.
0.00/0.00	    (CONDITIONTYPE ORIENTED)
0.00/0.00	    (VAR x y q n z x4 x1 x2 x3)
0.00/0.00	    (RULES
0.00/0.00	      add(0,x) -> x
0.00/0.00	      add(s(x),y) -> s(add(x,y))
0.00/0.00	      mult(0,y) -> 0
0.00/0.00	      mult(s(x),y) -> add(mult(x,y),y)
0.00/0.00	      lte(0,y) -> true
0.00/0.00	      lte(s(x),0) -> false
0.00/0.00	      lte(s(x),s(y)) -> lte(x,y)
0.00/0.00	      minus(0,s(y)) -> 0
0.00/0.00	      minus(x,0) -> x
0.00/0.00	      minus(s(x),s(y)) -> minus(x,y)
0.00/0.00	      mod(0,y) -> 0
0.00/0.00	      mod(x,0) -> x
0.00/0.00	      mod(x,s(y)) -> mod(minus(x,s(y)),s(y)) | lte(s(y),x) == true
0.00/0.00	      mod(x,s(y)) -> x | lte(s(y),x) == false
0.00/0.00	      div(0,s(x)) -> 0
0.00/0.00	      div(s(x),s(y)) -> 0 | lte(s(x),y) == true
0.00/0.00	      div(s(x),s(y)) -> s(q) | lte(s(x),y) == false, div(minus(x,y),s(y)) == q
0.00/0.00	      power(x,0) -> s(0)
0.00/0.00	      power(x,n) -> mult(mult(y,y),s(0)) | mod(n,s(s(0))) == 0, power(x,div(n,s(s(0)))) == y
0.00/0.00	      power(x,n) -> mult(mult(y,y),x) | mod(n,s(s(0))) == s(z), power(x,div(n,s(s(0)))) == y
0.00/0.00	    )
0.00/0.00	    (COMMENT COPS 499)
0.00/0.00	    (COMMENT submitted by: Naoki Nishida)
0.00/0.00	
0.00/0.00	(VAR x4 x1 y x2 x3)
0.00/0.00	(CONDITION 
0.00/0.00	mod(x3,s(s(0))) == 0, power(x2,div(x3,s(s(0)))) == y, mod(x3,s(s(0))) == s(x1), power(x2,div(x3,s(s(0)))) == x4
0.00/0.00	)
0.00/0.00	
0.00/0.00	Optimized the infeasibility problem if possible.
0.00/0.00	
0.00/0.00	(VAR x4 x1 y x2 x3)
0.00/0.00	(CONDITION 
0.00/0.00	mod(x3,s(s(0))) == 0, power(x2,div(x3,s(s(0)))) == y, mod(x3,s(s(0))) == s(x1), power(x2,div(x3,s(s(0)))) == x4
0.00/0.00	)
0.00/0.00	
0.00/0.00	This is not ultra-RL and deterministic.
0.00/0.00	
0.00/0.00	
0.00/0.00	MAYBE
0.00/0.00	EOF