0.00/0.01 MAYBE 0.00/0.01 0.00/0.01 0.00/0.01 Succeeded in reading "/export/starexec/sandbox/benchmark/theBenchmark.trs". 0.00/0.01 (CONDITIONTYPE ORIENTED) 0.00/0.01 (VAR x y q n n\' z) 0.00/0.01 (RULES 0.00/0.01 add(0,x) -> x 0.00/0.01 add(s(x),y) -> s(add(x,y)) 0.00/0.01 mult(0,y) -> 0 0.00/0.01 mult(s(x),y) -> add(mult(x,y),y) 0.00/0.01 lte(0,y) -> true 0.00/0.01 lte(s(x),0) -> false 0.00/0.01 lte(s(x),s(y)) -> lte(x,y) 0.00/0.01 minus(0,s(y)) -> 0 0.00/0.01 minus(x,0) -> x 0.00/0.01 minus(s(x),s(y)) -> minus(x,y) 0.00/0.01 mod(0,y) -> 0 0.00/0.01 mod(x,0) -> x 0.00/0.01 mod(x,s(y)) -> mod(minus(x,s(y)),s(y)) | lte(s(y),x) == true 0.00/0.01 mod(x,s(y)) -> x | lte(s(y),x) == false 0.00/0.01 div(0,s(x)) -> 0 0.00/0.01 div(s(x),s(y)) -> 0 | lte(s(x),y) == true 0.00/0.01 div(s(x),s(y)) -> s(q) | lte(s(x),y) == false, div(minus(x,y),s(y)) == q 0.00/0.01 power(x,0) -> s(0) 0.00/0.01 power(x,n) -> mult(mult(y,y),s(0)) | n == s(n\'), mod(n,s(s(0))) == 0, power(x,div(n,s(s(0)))) == y 0.00/0.01 power(x,n) -> mult(mult(y,y),x) | n == s(n\'), mod(n,s(s(0))) == s(z), power(x,div(n,s(s(0)))) == y 0.00/0.01 ) 0.00/0.01 (COMMENT doi:10.4230/LIPIcs.FSCD.2016.10 [91] derived from Figure 1 , with modified conditions in last two rules to conform to Haskell's evaluation strategy; cf. Cops #499 submitted by: Thomas Sternagel) 0.00/0.01 0.00/0.01 No "->="-rules. 0.00/0.01 0.00/0.01 Decomposed conditions if possible. 0.00/0.01 (CONDITIONTYPE ORIENTED) 0.00/0.01 (VAR x y q n n\' z) 0.00/0.01 (RULES 0.00/0.01 add(0,x) -> x 0.00/0.01 add(s(x),y) -> s(add(x,y)) 0.00/0.01 mult(0,y) -> 0 0.00/0.01 mult(s(x),y) -> add(mult(x,y),y) 0.00/0.01 lte(0,y) -> true 0.00/0.01 lte(s(x),0) -> false 0.00/0.01 lte(s(x),s(y)) -> lte(x,y) 0.00/0.01 minus(0,s(y)) -> 0 0.00/0.01 minus(x,0) -> x 0.00/0.01 minus(s(x),s(y)) -> minus(x,y) 0.00/0.01 mod(0,y) -> 0 0.00/0.01 mod(x,0) -> x 0.00/0.01 mod(x,s(y)) -> mod(minus(x,s(y)),s(y)) | lte(s(y),x) == true 0.00/0.01 mod(x,s(y)) -> x | lte(s(y),x) == false 0.00/0.01 div(0,s(x)) -> 0 0.00/0.01 div(s(x),s(y)) -> 0 | lte(s(x),y) == true 0.00/0.01 div(s(x),s(y)) -> s(q) | lte(s(x),y) == false, div(minus(x,y),s(y)) == q 0.00/0.01 power(x,0) -> s(0) 0.00/0.01 power(x,n) -> mult(mult(y,y),s(0)) | n == s(n\'), mod(n,s(s(0))) == 0, power(x,div(n,s(s(0)))) == y 0.00/0.01 power(x,n) -> mult(mult(y,y),x) | n == s(n\'), mod(n,s(s(0))) == s(z), power(x,div(n,s(s(0)))) == y 0.00/0.01 ) 0.00/0.01 (COMMENT doi:10.4230/LIPIcs.FSCD.2016.10 [91] derived from Figure 1 , with modified conditions in last two rules to conform to Haskell's evaluation strategy; cf. Cops #499 submitted by: Thomas Sternagel) 0.00/0.01 0.00/0.01 Removed infeasible rules as much as possible. 0.00/0.01 (CONDITIONTYPE ORIENTED) 0.00/0.01 (VAR x y q n n\' z) 0.00/0.01 (RULES 0.00/0.01 add(0,x) -> x 0.00/0.01 add(s(x),y) -> s(add(x,y)) 0.00/0.01 mult(0,y) -> 0 0.00/0.01 mult(s(x),y) -> add(mult(x,y),y) 0.00/0.01 lte(0,y) -> true 0.00/0.01 lte(s(x),0) -> false 0.00/0.01 lte(s(x),s(y)) -> lte(x,y) 0.00/0.01 minus(0,s(y)) -> 0 0.00/0.01 minus(x,0) -> x 0.00/0.01 minus(s(x),s(y)) -> minus(x,y) 0.00/0.01 mod(0,y) -> 0 0.00/0.01 mod(x,0) -> x 0.00/0.01 mod(x,s(y)) -> mod(minus(x,s(y)),s(y)) | lte(s(y),x) == true 0.00/0.01 mod(x,s(y)) -> x | lte(s(y),x) == false 0.00/0.01 div(0,s(x)) -> 0 0.00/0.01 div(s(x),s(y)) -> 0 | lte(s(x),y) == true 0.00/0.01 div(s(x),s(y)) -> s(q) | lte(s(x),y) == false, div(minus(x,y),s(y)) == q 0.00/0.01 power(x,0) -> s(0) 0.00/0.01 power(x,n) -> mult(mult(y,y),s(0)) | n == s(n\'), mod(n,s(s(0))) == 0, power(x,div(n,s(s(0)))) == y 0.00/0.01 power(x,n) -> mult(mult(y,y),x) | n == s(n\'), mod(n,s(s(0))) == s(z), power(x,div(n,s(s(0)))) == y 0.00/0.01 ) 0.00/0.01 (COMMENT doi:10.4230/LIPIcs.FSCD.2016.10 [91] derived from Figure 1 , with modified conditions in last two rules to conform to Haskell's evaluation strategy; cf. Cops #499 submitted by: Thomas Sternagel) 0.00/0.01 0.00/0.01 Try to disprove confluence of the following (C)TRS: 0.00/0.01 (CONDITIONTYPE ORIENTED) 0.00/0.01 (VAR x y q n n\' z) 0.00/0.01 (RULES 0.00/0.01 add(0,x) -> x 0.00/0.01 add(s(x),y) -> s(add(x,y)) 0.00/0.01 mult(0,y) -> 0 0.00/0.01 mult(s(x),y) -> add(mult(x,y),y) 0.00/0.01 lte(0,y) -> true 0.00/0.01 lte(s(x),0) -> false 0.00/0.01 lte(s(x),s(y)) -> lte(x,y) 0.00/0.01 minus(0,s(y)) -> 0 0.00/0.01 minus(x,0) -> x 0.00/0.01 minus(s(x),s(y)) -> minus(x,y) 0.00/0.01 mod(0,y) -> 0 0.00/0.01 mod(x,0) -> x 0.00/0.01 mod(x,s(y)) -> mod(minus(x,s(y)),s(y)) | lte(s(y),x) == true 0.00/0.01 mod(x,s(y)) -> x | lte(s(y),x) == false 0.00/0.01 div(0,s(x)) -> 0 0.00/0.01 div(s(x),s(y)) -> 0 | lte(s(x),y) == true 0.00/0.01 div(s(x),s(y)) -> s(q) | lte(s(x),y) == false, div(minus(x,y),s(y)) == q 0.00/0.01 power(x,0) -> s(0) 0.00/0.01 power(x,n) -> mult(mult(y,y),s(0)) | n == s(n\'), mod(n,s(s(0))) == 0, power(x,div(n,s(s(0)))) == y 0.00/0.01 power(x,n) -> mult(mult(y,y),x) | n == s(n\'), mod(n,s(s(0))) == s(z), power(x,div(n,s(s(0)))) == y 0.00/0.01 ) 0.00/0.01 (COMMENT doi:10.4230/LIPIcs.FSCD.2016.10 [91] derived from Figure 1 , with modified conditions in last two rules to conform to Haskell's evaluation strategy; cf. Cops #499 submitted by: Thomas Sternagel) 0.00/0.01 0.00/0.01 Failed either to apply SR and U for normal 1CTRSs to the above CTRS or to prove confluence of any converted TRSs. 0.00/0.01 0.00/0.01 Try to apply SR and U for 3DCTRSs to the above CTRS. 0.00/0.01 0.00/0.01 Succeeded in applying U for 3DCTRSs to the above CTRS. 0.00/0.01 U(R) = 0.00/0.01 (VAR x1 x2 x3 x4 x5) 0.00/0.01 (RULES 0.00/0.01 add(0,x1) -> x1 0.00/0.01 add(s(x1),x2) -> s(add(x1,x2)) 0.00/0.01 mult(0,x1) -> 0 0.00/0.01 mult(s(x1),x2) -> add(mult(x1,x2),x2) 0.00/0.01 lte(0,x1) -> true 0.00/0.01 lte(s(x1),0) -> false 0.00/0.01 lte(s(x1),s(x2)) -> lte(x1,x2) 0.00/0.01 minus(0,s(x1)) -> 0 0.00/0.01 minus(x1,0) -> x1 0.00/0.01 minus(s(x1),s(x2)) -> minus(x1,x2) 0.00/0.01 mod(0,x1) -> 0 0.00/0.01 mod(x1,0) -> x1 0.00/0.01 mod(x1,s(x2)) -> u1(lte(s(x2),x1),x1,x2) 0.00/0.01 u1(true,x1,x2) -> mod(minus(x1,s(x2)),s(x2)) 0.00/0.01 u1(false,x1,x2) -> x1 0.00/0.01 div(0,s(x1)) -> 0 0.00/0.01 div(s(x1),s(x2)) -> u2(lte(s(x1),x2),x1,x2) 0.00/0.01 u2(true,x1,x2) -> 0 0.00/0.01 u2(false,x1,x2) -> u3(div(minus(x1,x2),s(x2)),x1,x2) 0.00/0.01 u3(x3,x1,x2) -> s(x3) 0.00/0.01 power(x1,0) -> s(0) 0.00/0.01 power(x1,x2) -> u4(x2,x1,x2) 0.00/0.01 u4(s(x3),x1,x2) -> u5(mod(x2,s(s(0))),x3,x1,x2) 0.00/0.01 u5(0,x3,x1,x2) -> u7(power(x1,div(x2,s(s(0)))),x3,x1,x2) 0.00/0.01 u7(x4,x3,x1,x2) -> mult(mult(x4,x4),s(0)) 0.00/0.01 u5(s(x4),x3,x1,x2) -> u6(power(x1,div(x2,s(s(0)))),x4,x3,x1,x2) 0.00/0.01 u6(x5,x4,x3,x1,x2) -> mult(mult(x5,x5),x1) 0.00/0.01 ) 0.00/0.01 0.00/0.01 U for 3DCTRSs is sound for the above CTRS. 0.00/0.01 0.00/0.01 Failed to prove confluence of U(R). 0.00/0.01 0.00/0.01 Try to prove operational termination of R, i.e., termination of U(R). 0.00/0.01 0.00/0.01 Failed to prove operational termination of R. 0.00/0.01 0.00/0.01 MAYBE 0.00/0.01 EOF