MAYBE 220.96/95.23 MAYBE 220.96/95.23 220.96/95.23 We are left with following problem, upon which TcT provides the 220.96/95.23 certificate MAYBE. 220.96/95.23 220.96/95.23 Strict Trs: 220.96/95.23 { gt(s(x), s(y)) -> gt(x, y) 220.96/95.23 , gt(s(x), 0()) -> true() 220.96/95.23 , gt(0(), y) -> false() 220.96/95.23 , divides(x, y) -> div(x, y, y) 220.96/95.23 , div(s(x), s(y), z) -> div(x, y, z) 220.96/95.23 , div(s(x), 0(), s(z)) -> div(s(x), s(z), s(z)) 220.96/95.23 , div(0(), s(x), z) -> false() 220.96/95.23 , div(0(), 0(), z) -> true() 220.96/95.23 , prime(x) -> test(x, s(s(0()))) 220.96/95.23 , test(x, y) -> if1(gt(x, y), x, y) 220.96/95.23 , if1(true(), x, y) -> if2(divides(x, y), x, y) 220.96/95.23 , if1(false(), x, y) -> true() 220.96/95.23 , if2(true(), x, y) -> false() 220.96/95.23 , if2(false(), x, y) -> test(x, s(y)) } 220.96/95.23 Obligation: 220.96/95.23 runtime complexity 220.96/95.23 Answer: 220.96/95.23 MAYBE 220.96/95.23 220.96/95.23 None of the processors succeeded. 220.96/95.23 220.96/95.23 Details of failed attempt(s): 220.96/95.23 ----------------------------- 220.96/95.23 1) 'Best' failed due to the following reason: 220.96/95.23 220.96/95.23 None of the processors succeeded. 220.96/95.23 220.96/95.23 Details of failed attempt(s): 220.96/95.23 ----------------------------- 220.96/95.23 1) 'With Problem ... (timeout of 148 seconds) (timeout of 297 220.96/95.23 seconds)' failed due to the following reason: 220.96/95.23 220.96/95.23 The weightgap principle applies (using the following nonconstant 220.96/95.23 growth matrix-interpretation) 220.96/95.23 220.96/95.23 The following argument positions are usable: 220.96/95.23 Uargs(if1) = {1}, Uargs(if2) = {1} 220.96/95.23 220.96/95.23 TcT has computed the following matrix interpretation satisfying 220.96/95.23 not(EDA) and not(IDA(1)). 220.96/95.23 220.96/95.23 [gt](x1, x2) = [4] 220.96/95.23 220.96/95.23 [s](x1) = [7] 220.96/95.23 220.96/95.23 [0] = [7] 220.96/95.23 220.96/95.23 [true] = [0] 220.96/95.23 220.96/95.23 [false] = [0] 220.96/95.23 220.96/95.23 [divides](x1, x2) = [0] 220.96/95.23 220.96/95.23 [div](x1, x2, x3) = [0] 220.96/95.23 220.96/95.23 [prime](x1) = [1] x1 + [7] 220.96/95.23 220.96/95.23 [test](x1, x2) = [1] x1 + [0] 220.96/95.23 220.96/95.23 [if1](x1, x2, x3) = [1] x1 + [1] x2 + [0] 220.96/95.23 220.96/95.23 [if2](x1, x2, x3) = [1] x1 + [1] x2 + [0] 220.96/95.23 220.96/95.23 The order satisfies the following ordering constraints: 220.96/95.23 220.96/95.23 [gt(s(x), s(y))] = [4] 220.96/95.23 >= [4] 220.96/95.23 = [gt(x, y)] 220.96/95.23 220.96/95.23 [gt(s(x), 0())] = [4] 220.96/95.23 > [0] 220.96/95.23 = [true()] 220.96/95.23 220.96/95.23 [gt(0(), y)] = [4] 220.96/95.23 > [0] 220.96/95.23 = [false()] 220.96/95.23 220.96/95.23 [divides(x, y)] = [0] 220.96/95.23 >= [0] 220.96/95.23 = [div(x, y, y)] 220.96/95.23 220.96/95.23 [div(s(x), s(y), z)] = [0] 220.96/95.23 >= [0] 220.96/95.23 = [div(x, y, z)] 220.96/95.23 220.96/95.23 [div(s(x), 0(), s(z))] = [0] 220.96/95.23 >= [0] 220.96/95.23 = [div(s(x), s(z), s(z))] 220.96/95.23 220.96/95.23 [div(0(), s(x), z)] = [0] 220.96/95.23 >= [0] 220.96/95.23 = [false()] 220.96/95.23 220.96/95.23 [div(0(), 0(), z)] = [0] 220.96/95.23 >= [0] 220.96/95.23 = [true()] 220.96/95.23 220.96/95.23 [prime(x)] = [1] x + [7] 220.96/95.23 > [1] x + [0] 220.96/95.23 = [test(x, s(s(0())))] 220.96/95.23 220.96/95.23 [test(x, y)] = [1] x + [0] 220.96/95.23 ? [1] x + [4] 220.96/95.23 = [if1(gt(x, y), x, y)] 220.96/95.23 220.96/95.23 [if1(true(), x, y)] = [1] x + [0] 220.96/95.23 >= [1] x + [0] 220.96/95.23 = [if2(divides(x, y), x, y)] 220.96/95.23 220.96/95.23 [if1(false(), x, y)] = [1] x + [0] 220.96/95.23 >= [0] 220.96/95.23 = [true()] 220.96/95.23 220.96/95.23 [if2(true(), x, y)] = [1] x + [0] 220.96/95.23 >= [0] 220.96/95.23 = [false()] 220.96/95.23 220.96/95.23 [if2(false(), x, y)] = [1] x + [0] 220.96/95.23 >= [1] x + [0] 220.96/95.23 = [test(x, s(y))] 220.96/95.23 220.96/95.23 220.96/95.23 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 220.96/95.23 220.96/95.23 We are left with following problem, upon which TcT provides the 220.96/95.23 certificate MAYBE. 220.96/95.23 220.96/95.23 Strict Trs: 220.96/95.23 { gt(s(x), s(y)) -> gt(x, y) 220.96/95.23 , divides(x, y) -> div(x, y, y) 220.96/95.23 , div(s(x), s(y), z) -> div(x, y, z) 220.96/95.23 , div(s(x), 0(), s(z)) -> div(s(x), s(z), s(z)) 220.96/95.23 , div(0(), s(x), z) -> false() 220.96/95.23 , div(0(), 0(), z) -> true() 220.96/95.23 , test(x, y) -> if1(gt(x, y), x, y) 220.96/95.23 , if1(true(), x, y) -> if2(divides(x, y), x, y) 220.96/95.23 , if1(false(), x, y) -> true() 220.96/95.23 , if2(true(), x, y) -> false() 220.96/95.23 , if2(false(), x, y) -> test(x, s(y)) } 220.96/95.23 Weak Trs: 220.96/95.23 { gt(s(x), 0()) -> true() 220.96/95.23 , gt(0(), y) -> false() 220.96/95.23 , prime(x) -> test(x, s(s(0()))) } 220.96/95.23 Obligation: 220.96/95.23 runtime complexity 220.96/95.23 Answer: 220.96/95.23 MAYBE 220.96/95.23 220.96/95.23 The weightgap principle applies (using the following nonconstant 220.96/95.23 growth matrix-interpretation) 220.96/95.23 220.96/95.23 The following argument positions are usable: 220.96/95.23 Uargs(if1) = {1}, Uargs(if2) = {1} 220.96/95.23 220.96/95.23 TcT has computed the following matrix interpretation satisfying 220.96/95.23 not(EDA) and not(IDA(1)). 220.96/95.23 220.96/95.23 [gt](x1, x2) = [4] 220.96/95.23 220.96/95.23 [s](x1) = [7] 220.96/95.23 220.96/95.23 [0] = [7] 220.96/95.23 220.96/95.23 [true] = [0] 220.96/95.23 220.96/95.23 [false] = [0] 220.96/95.23 220.96/95.23 [divides](x1, x2) = [1] 220.96/95.23 220.96/95.23 [div](x1, x2, x3) = [0] 220.96/95.23 220.96/95.23 [prime](x1) = [1] x1 + [7] 220.96/95.23 220.96/95.23 [test](x1, x2) = [1] x1 + [0] 220.96/95.23 220.96/95.23 [if1](x1, x2, x3) = [1] x1 + [1] x2 + [0] 220.96/95.23 220.96/95.23 [if2](x1, x2, x3) = [1] x1 + [1] x2 + [0] 220.96/95.23 220.96/95.23 The order satisfies the following ordering constraints: 220.96/95.23 220.96/95.23 [gt(s(x), s(y))] = [4] 220.96/95.23 >= [4] 220.96/95.23 = [gt(x, y)] 220.96/95.23 220.96/95.23 [gt(s(x), 0())] = [4] 220.96/95.23 > [0] 220.96/95.23 = [true()] 220.96/95.23 220.96/95.23 [gt(0(), y)] = [4] 220.96/95.23 > [0] 220.96/95.23 = [false()] 220.96/95.23 220.96/95.23 [divides(x, y)] = [1] 220.96/95.23 > [0] 220.96/95.23 = [div(x, y, y)] 220.96/95.23 220.96/95.23 [div(s(x), s(y), z)] = [0] 220.96/95.23 >= [0] 220.96/95.23 = [div(x, y, z)] 220.96/95.23 220.96/95.23 [div(s(x), 0(), s(z))] = [0] 220.96/95.23 >= [0] 220.96/95.23 = [div(s(x), s(z), s(z))] 220.96/95.23 220.96/95.23 [div(0(), s(x), z)] = [0] 220.96/95.23 >= [0] 220.96/95.23 = [false()] 220.96/95.23 220.96/95.23 [div(0(), 0(), z)] = [0] 220.96/95.23 >= [0] 220.96/95.23 = [true()] 220.96/95.23 220.96/95.23 [prime(x)] = [1] x + [7] 220.96/95.23 > [1] x + [0] 220.96/95.23 = [test(x, s(s(0())))] 220.96/95.23 220.96/95.23 [test(x, y)] = [1] x + [0] 220.96/95.23 ? [1] x + [4] 220.96/95.23 = [if1(gt(x, y), x, y)] 220.96/95.23 220.96/95.23 [if1(true(), x, y)] = [1] x + [0] 220.96/95.23 ? [1] x + [1] 220.96/95.23 = [if2(divides(x, y), x, y)] 220.96/95.23 220.96/95.23 [if1(false(), x, y)] = [1] x + [0] 220.96/95.23 >= [0] 220.96/95.23 = [true()] 220.96/95.23 220.96/95.23 [if2(true(), x, y)] = [1] x + [0] 220.96/95.23 >= [0] 220.96/95.23 = [false()] 220.96/95.23 220.96/95.23 [if2(false(), x, y)] = [1] x + [0] 220.96/95.23 >= [1] x + [0] 220.96/95.23 = [test(x, s(y))] 220.96/95.23 220.96/95.23 220.96/95.23 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 220.96/95.23 220.96/95.23 We are left with following problem, upon which TcT provides the 220.96/95.23 certificate MAYBE. 220.96/95.23 220.96/95.23 Strict Trs: 220.96/95.23 { gt(s(x), s(y)) -> gt(x, y) 220.96/95.23 , div(s(x), s(y), z) -> div(x, y, z) 220.96/95.23 , div(s(x), 0(), s(z)) -> div(s(x), s(z), s(z)) 220.96/95.23 , div(0(), s(x), z) -> false() 220.96/95.23 , div(0(), 0(), z) -> true() 220.96/95.23 , test(x, y) -> if1(gt(x, y), x, y) 220.96/95.23 , if1(true(), x, y) -> if2(divides(x, y), x, y) 220.96/95.23 , if1(false(), x, y) -> true() 220.96/95.23 , if2(true(), x, y) -> false() 220.96/95.23 , if2(false(), x, y) -> test(x, s(y)) } 220.96/95.23 Weak Trs: 220.96/95.23 { gt(s(x), 0()) -> true() 220.96/95.23 , gt(0(), y) -> false() 220.96/95.23 , divides(x, y) -> div(x, y, y) 220.96/95.23 , prime(x) -> test(x, s(s(0()))) } 220.96/95.23 Obligation: 220.96/95.23 runtime complexity 220.96/95.23 Answer: 220.96/95.23 MAYBE 220.96/95.23 220.96/95.23 The weightgap principle applies (using the following nonconstant 220.96/95.23 growth matrix-interpretation) 220.96/95.23 220.96/95.23 The following argument positions are usable: 220.96/95.23 Uargs(if1) = {1}, Uargs(if2) = {1} 220.96/95.23 220.96/95.23 TcT has computed the following matrix interpretation satisfying 220.96/95.23 not(EDA) and not(IDA(1)). 220.96/95.23 220.96/95.23 [gt](x1, x2) = [4] 220.96/95.23 220.96/95.23 [s](x1) = [7] 220.96/95.23 220.96/95.23 [0] = [7] 220.96/95.23 220.96/95.23 [true] = [0] 220.96/95.23 220.96/95.23 [false] = [0] 220.96/95.23 220.96/95.23 [divides](x1, x2) = [4] 220.96/95.23 220.96/95.23 [div](x1, x2, x3) = [0] 220.96/95.23 220.96/95.23 [prime](x1) = [1] x1 + [7] 220.96/95.23 220.96/95.23 [test](x1, x2) = [1] x1 + [5] 220.96/95.23 220.96/95.23 [if1](x1, x2, x3) = [1] x1 + [1] x2 + [0] 220.96/95.23 220.96/95.23 [if2](x1, x2, x3) = [1] x1 + [1] x2 + [0] 220.96/95.23 220.96/95.23 The order satisfies the following ordering constraints: 220.96/95.23 220.96/95.23 [gt(s(x), s(y))] = [4] 220.96/95.23 >= [4] 220.96/95.23 = [gt(x, y)] 220.96/95.23 220.96/95.23 [gt(s(x), 0())] = [4] 220.96/95.23 > [0] 220.96/95.23 = [true()] 220.96/95.23 220.96/95.23 [gt(0(), y)] = [4] 220.96/95.23 > [0] 220.96/95.23 = [false()] 220.96/95.23 220.96/95.23 [divides(x, y)] = [4] 220.96/95.23 > [0] 220.96/95.23 = [div(x, y, y)] 220.96/95.23 220.96/95.23 [div(s(x), s(y), z)] = [0] 220.96/95.23 >= [0] 220.96/95.23 = [div(x, y, z)] 220.96/95.23 220.96/95.23 [div(s(x), 0(), s(z))] = [0] 220.96/95.23 >= [0] 220.96/95.23 = [div(s(x), s(z), s(z))] 220.96/95.23 220.96/95.23 [div(0(), s(x), z)] = [0] 220.96/95.23 >= [0] 220.96/95.23 = [false()] 220.96/95.23 220.96/95.23 [div(0(), 0(), z)] = [0] 220.96/95.23 >= [0] 220.96/95.23 = [true()] 220.96/95.23 220.96/95.23 [prime(x)] = [1] x + [7] 220.96/95.23 > [1] x + [5] 220.96/95.23 = [test(x, s(s(0())))] 220.96/95.23 220.96/95.23 [test(x, y)] = [1] x + [5] 220.96/95.23 > [1] x + [4] 220.96/95.23 = [if1(gt(x, y), x, y)] 220.96/95.23 220.96/95.23 [if1(true(), x, y)] = [1] x + [0] 220.96/95.23 ? [1] x + [4] 220.96/95.23 = [if2(divides(x, y), x, y)] 220.96/95.23 220.96/95.23 [if1(false(), x, y)] = [1] x + [0] 220.96/95.23 >= [0] 220.96/95.23 = [true()] 220.96/95.23 220.96/95.23 [if2(true(), x, y)] = [1] x + [0] 220.96/95.23 >= [0] 220.96/95.23 = [false()] 220.96/95.23 220.96/95.23 [if2(false(), x, y)] = [1] x + [0] 220.96/95.23 ? [1] x + [5] 220.96/95.23 = [test(x, s(y))] 220.96/95.23 220.96/95.23 220.96/95.23 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 220.96/95.23 220.96/95.23 We are left with following problem, upon which TcT provides the 220.96/95.23 certificate MAYBE. 220.96/95.23 220.96/95.23 Strict Trs: 220.96/95.23 { gt(s(x), s(y)) -> gt(x, y) 220.96/95.23 , div(s(x), s(y), z) -> div(x, y, z) 220.96/95.23 , div(s(x), 0(), s(z)) -> div(s(x), s(z), s(z)) 220.96/95.23 , div(0(), s(x), z) -> false() 220.96/95.23 , div(0(), 0(), z) -> true() 220.96/95.23 , if1(true(), x, y) -> if2(divides(x, y), x, y) 220.96/95.23 , if1(false(), x, y) -> true() 220.96/95.23 , if2(true(), x, y) -> false() 220.96/95.23 , if2(false(), x, y) -> test(x, s(y)) } 220.96/95.23 Weak Trs: 220.96/95.23 { gt(s(x), 0()) -> true() 220.96/95.23 , gt(0(), y) -> false() 220.96/95.23 , divides(x, y) -> div(x, y, y) 220.96/95.23 , prime(x) -> test(x, s(s(0()))) 220.96/95.23 , test(x, y) -> if1(gt(x, y), x, y) } 220.96/95.23 Obligation: 220.96/95.23 runtime complexity 220.96/95.23 Answer: 220.96/95.23 MAYBE 220.96/95.23 220.96/95.23 The weightgap principle applies (using the following nonconstant 220.96/95.23 growth matrix-interpretation) 220.96/95.23 220.96/95.23 The following argument positions are usable: 220.96/95.23 Uargs(if1) = {1}, Uargs(if2) = {1} 220.96/95.23 220.96/95.23 TcT has computed the following matrix interpretation satisfying 220.96/95.23 not(EDA) and not(IDA(1)). 220.96/95.23 220.96/95.23 [gt](x1, x2) = [1] 220.96/95.23 220.96/95.23 [s](x1) = [7] 220.96/95.23 220.96/95.23 [0] = [7] 220.96/95.23 220.96/95.23 [true] = [0] 220.96/95.23 220.96/95.23 [false] = [1] 220.96/95.23 220.96/95.23 [divides](x1, x2) = [4] 220.96/95.23 220.96/95.23 [div](x1, x2, x3) = [0] 220.96/95.23 220.96/95.23 [prime](x1) = [1] x1 + [7] 220.96/95.23 220.96/95.23 [test](x1, x2) = [1] x1 + [4] 220.96/95.23 220.96/95.23 [if1](x1, x2, x3) = [1] x1 + [1] x2 + [0] 220.96/95.23 220.96/95.23 [if2](x1, x2, x3) = [1] x1 + [1] x2 + [0] 220.96/95.23 220.96/95.23 The order satisfies the following ordering constraints: 220.96/95.23 220.96/95.23 [gt(s(x), s(y))] = [1] 220.96/95.23 >= [1] 220.96/95.23 = [gt(x, y)] 220.96/95.23 220.96/95.23 [gt(s(x), 0())] = [1] 220.96/95.23 > [0] 220.96/95.23 = [true()] 220.96/95.23 220.96/95.23 [gt(0(), y)] = [1] 220.96/95.23 >= [1] 220.96/95.23 = [false()] 220.96/95.23 220.96/95.23 [divides(x, y)] = [4] 220.96/95.23 > [0] 220.96/95.23 = [div(x, y, y)] 220.96/95.23 220.96/95.23 [div(s(x), s(y), z)] = [0] 220.96/95.23 >= [0] 220.96/95.23 = [div(x, y, z)] 220.96/95.23 220.96/95.23 [div(s(x), 0(), s(z))] = [0] 220.96/95.23 >= [0] 220.96/95.23 = [div(s(x), s(z), s(z))] 220.96/95.23 220.96/95.23 [div(0(), s(x), z)] = [0] 220.96/95.23 ? [1] 220.96/95.23 = [false()] 220.96/95.23 220.96/95.23 [div(0(), 0(), z)] = [0] 220.96/95.23 >= [0] 220.96/95.23 = [true()] 220.96/95.23 220.96/95.23 [prime(x)] = [1] x + [7] 220.96/95.23 > [1] x + [4] 220.96/95.23 = [test(x, s(s(0())))] 220.96/95.23 220.96/95.23 [test(x, y)] = [1] x + [4] 220.96/95.23 > [1] x + [1] 220.96/95.23 = [if1(gt(x, y), x, y)] 220.96/95.23 220.96/95.23 [if1(true(), x, y)] = [1] x + [0] 220.96/95.23 ? [1] x + [4] 220.96/95.23 = [if2(divides(x, y), x, y)] 220.96/95.23 220.96/95.23 [if1(false(), x, y)] = [1] x + [1] 220.96/95.23 > [0] 220.96/95.23 = [true()] 220.96/95.23 220.96/95.23 [if2(true(), x, y)] = [1] x + [0] 220.96/95.23 ? [1] 220.96/95.23 = [false()] 220.96/95.23 220.96/95.23 [if2(false(), x, y)] = [1] x + [1] 220.96/95.23 ? [1] x + [4] 220.96/95.23 = [test(x, s(y))] 220.96/95.23 220.96/95.23 220.96/95.23 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 220.96/95.23 220.96/95.23 We are left with following problem, upon which TcT provides the 220.96/95.23 certificate MAYBE. 220.96/95.23 220.96/95.23 Strict Trs: 220.96/95.23 { gt(s(x), s(y)) -> gt(x, y) 220.96/95.23 , div(s(x), s(y), z) -> div(x, y, z) 220.96/95.23 , div(s(x), 0(), s(z)) -> div(s(x), s(z), s(z)) 220.96/95.23 , div(0(), s(x), z) -> false() 220.96/95.23 , div(0(), 0(), z) -> true() 220.96/95.23 , if1(true(), x, y) -> if2(divides(x, y), x, y) 220.96/95.23 , if2(true(), x, y) -> false() 220.96/95.23 , if2(false(), x, y) -> test(x, s(y)) } 220.96/95.23 Weak Trs: 220.96/95.23 { gt(s(x), 0()) -> true() 220.96/95.23 , gt(0(), y) -> false() 220.96/95.23 , divides(x, y) -> div(x, y, y) 220.96/95.23 , prime(x) -> test(x, s(s(0()))) 220.96/95.23 , test(x, y) -> if1(gt(x, y), x, y) 220.96/95.23 , if1(false(), x, y) -> true() } 220.96/95.23 Obligation: 220.96/95.23 runtime complexity 220.96/95.23 Answer: 220.96/95.23 MAYBE 220.96/95.23 220.96/95.23 The weightgap principle applies (using the following nonconstant 220.96/95.23 growth matrix-interpretation) 220.96/95.23 220.96/95.24 The following argument positions are usable: 220.96/95.24 Uargs(if1) = {1}, Uargs(if2) = {1} 220.96/95.24 220.96/95.24 TcT has computed the following matrix interpretation satisfying 220.96/95.24 not(EDA) and not(IDA(1)). 220.96/95.24 220.96/95.24 [gt](x1, x2) = [0] 220.96/95.24 220.96/95.24 [s](x1) = [3] 220.96/95.24 220.96/95.24 [0] = [7] 220.96/95.24 220.96/95.24 [true] = [0] 220.96/95.24 220.96/95.24 [false] = [0] 220.96/95.24 220.96/95.24 [divides](x1, x2) = [4] 220.96/95.24 220.96/95.24 [div](x1, x2, x3) = [4] 220.96/95.24 220.96/95.24 [prime](x1) = [1] x1 + [7] 220.96/95.24 220.96/95.24 [test](x1, x2) = [1] x1 + [4] 220.96/95.24 220.96/95.24 [if1](x1, x2, x3) = [1] x1 + [1] x2 + [0] 220.96/95.24 220.96/95.24 [if2](x1, x2, x3) = [1] x1 + [1] x2 + [0] 220.96/95.24 220.96/95.24 The order satisfies the following ordering constraints: 220.96/95.24 220.96/95.24 [gt(s(x), s(y))] = [0] 220.96/95.24 >= [0] 220.96/95.24 = [gt(x, y)] 220.96/95.24 220.96/95.24 [gt(s(x), 0())] = [0] 220.96/95.24 >= [0] 220.96/95.24 = [true()] 220.96/95.24 220.96/95.24 [gt(0(), y)] = [0] 220.96/95.24 >= [0] 220.96/95.24 = [false()] 220.96/95.24 220.96/95.24 [divides(x, y)] = [4] 220.96/95.24 >= [4] 220.96/95.24 = [div(x, y, y)] 220.96/95.24 220.96/95.24 [div(s(x), s(y), z)] = [4] 220.96/95.24 >= [4] 220.96/95.24 = [div(x, y, z)] 220.96/95.24 220.96/95.24 [div(s(x), 0(), s(z))] = [4] 220.96/95.24 >= [4] 220.96/95.24 = [div(s(x), s(z), s(z))] 220.96/95.24 220.96/95.24 [div(0(), s(x), z)] = [4] 220.96/95.24 > [0] 220.96/95.24 = [false()] 220.96/95.24 220.96/95.24 [div(0(), 0(), z)] = [4] 220.96/95.24 > [0] 220.96/95.24 = [true()] 220.96/95.24 220.96/95.24 [prime(x)] = [1] x + [7] 220.96/95.24 > [1] x + [4] 220.96/95.24 = [test(x, s(s(0())))] 220.96/95.24 220.96/95.24 [test(x, y)] = [1] x + [4] 220.96/95.24 > [1] x + [0] 220.96/95.24 = [if1(gt(x, y), x, y)] 220.96/95.24 220.96/95.24 [if1(true(), x, y)] = [1] x + [0] 220.96/95.24 ? [1] x + [4] 220.96/95.24 = [if2(divides(x, y), x, y)] 220.96/95.24 220.96/95.24 [if1(false(), x, y)] = [1] x + [0] 220.96/95.24 >= [0] 220.96/95.24 = [true()] 220.96/95.24 220.96/95.24 [if2(true(), x, y)] = [1] x + [0] 220.96/95.24 >= [0] 220.96/95.24 = [false()] 220.96/95.24 220.96/95.24 [if2(false(), x, y)] = [1] x + [0] 220.96/95.24 ? [1] x + [4] 220.96/95.24 = [test(x, s(y))] 220.96/95.24 220.96/95.24 220.96/95.24 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 220.96/95.24 220.96/95.24 We are left with following problem, upon which TcT provides the 220.96/95.24 certificate MAYBE. 220.96/95.24 220.96/95.24 Strict Trs: 220.96/95.24 { gt(s(x), s(y)) -> gt(x, y) 220.96/95.24 , div(s(x), s(y), z) -> div(x, y, z) 220.96/95.24 , div(s(x), 0(), s(z)) -> div(s(x), s(z), s(z)) 220.96/95.24 , if1(true(), x, y) -> if2(divides(x, y), x, y) 220.96/95.24 , if2(true(), x, y) -> false() 220.96/95.24 , if2(false(), x, y) -> test(x, s(y)) } 220.96/95.24 Weak Trs: 220.96/95.24 { gt(s(x), 0()) -> true() 220.96/95.24 , gt(0(), y) -> false() 220.96/95.24 , divides(x, y) -> div(x, y, y) 220.96/95.24 , div(0(), s(x), z) -> false() 220.96/95.24 , div(0(), 0(), z) -> true() 220.96/95.24 , prime(x) -> test(x, s(s(0()))) 220.96/95.24 , test(x, y) -> if1(gt(x, y), x, y) 220.96/95.24 , if1(false(), x, y) -> true() } 220.96/95.24 Obligation: 220.96/95.24 runtime complexity 220.96/95.24 Answer: 220.96/95.24 MAYBE 220.96/95.24 220.96/95.24 The weightgap principle applies (using the following nonconstant 220.96/95.24 growth matrix-interpretation) 220.96/95.24 220.96/95.24 The following argument positions are usable: 220.96/95.24 Uargs(if1) = {1}, Uargs(if2) = {1} 220.96/95.24 220.96/95.24 TcT has computed the following matrix interpretation satisfying 220.96/95.24 not(EDA) and not(IDA(1)). 220.96/95.24 220.96/95.24 [gt](x1, x2) = [2] 220.96/95.24 220.96/95.24 [s](x1) = [7] 220.96/95.24 220.96/95.24 [0] = [7] 220.96/95.24 220.96/95.24 [true] = [0] 220.96/95.24 220.96/95.24 [false] = [0] 220.96/95.24 220.96/95.24 [divides](x1, x2) = [0] 220.96/95.24 220.96/95.24 [div](x1, x2, x3) = [0] 220.96/95.24 220.96/95.24 [prime](x1) = [1] x1 + [7] 220.96/95.24 220.96/95.24 [test](x1, x2) = [4] 220.96/95.24 220.96/95.24 [if1](x1, x2, x3) = [1] x1 + [2] 220.96/95.24 220.96/95.24 [if2](x1, x2, x3) = [1] x1 + [0] 220.96/95.24 220.96/95.24 The order satisfies the following ordering constraints: 220.96/95.24 220.96/95.24 [gt(s(x), s(y))] = [2] 220.96/95.24 >= [2] 220.96/95.24 = [gt(x, y)] 220.96/95.24 220.96/95.24 [gt(s(x), 0())] = [2] 220.96/95.24 > [0] 220.96/95.24 = [true()] 220.96/95.24 220.96/95.24 [gt(0(), y)] = [2] 220.96/95.24 > [0] 220.96/95.24 = [false()] 220.96/95.24 220.96/95.24 [divides(x, y)] = [0] 220.96/95.24 >= [0] 220.96/95.24 = [div(x, y, y)] 220.96/95.24 220.96/95.24 [div(s(x), s(y), z)] = [0] 220.96/95.24 >= [0] 220.96/95.24 = [div(x, y, z)] 220.96/95.24 220.96/95.24 [div(s(x), 0(), s(z))] = [0] 220.96/95.24 >= [0] 220.96/95.24 = [div(s(x), s(z), s(z))] 220.96/95.24 220.96/95.24 [div(0(), s(x), z)] = [0] 220.96/95.24 >= [0] 220.96/95.24 = [false()] 220.96/95.24 220.96/95.24 [div(0(), 0(), z)] = [0] 220.96/95.24 >= [0] 220.96/95.24 = [true()] 220.96/95.24 220.96/95.24 [prime(x)] = [1] x + [7] 220.96/95.24 > [4] 220.96/95.24 = [test(x, s(s(0())))] 220.96/95.24 220.96/95.24 [test(x, y)] = [4] 220.96/95.24 >= [4] 220.96/95.24 = [if1(gt(x, y), x, y)] 220.96/95.24 220.96/95.24 [if1(true(), x, y)] = [2] 220.96/95.24 > [0] 220.96/95.24 = [if2(divides(x, y), x, y)] 220.96/95.24 220.96/95.24 [if1(false(), x, y)] = [2] 220.96/95.24 > [0] 220.96/95.24 = [true()] 220.96/95.24 220.96/95.24 [if2(true(), x, y)] = [0] 220.96/95.24 >= [0] 220.96/95.24 = [false()] 220.96/95.24 220.96/95.24 [if2(false(), x, y)] = [0] 220.96/95.24 ? [4] 220.96/95.24 = [test(x, s(y))] 220.96/95.24 220.96/95.24 220.96/95.24 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 220.96/95.24 220.96/95.24 We are left with following problem, upon which TcT provides the 220.96/95.24 certificate MAYBE. 220.96/95.24 220.96/95.24 Strict Trs: 220.96/95.24 { gt(s(x), s(y)) -> gt(x, y) 220.96/95.24 , div(s(x), s(y), z) -> div(x, y, z) 220.96/95.24 , div(s(x), 0(), s(z)) -> div(s(x), s(z), s(z)) 220.96/95.24 , if2(true(), x, y) -> false() 220.96/95.24 , if2(false(), x, y) -> test(x, s(y)) } 220.96/95.24 Weak Trs: 220.96/95.24 { gt(s(x), 0()) -> true() 220.96/95.24 , gt(0(), y) -> false() 220.96/95.24 , divides(x, y) -> div(x, y, y) 220.96/95.24 , div(0(), s(x), z) -> false() 220.96/95.24 , div(0(), 0(), z) -> true() 220.96/95.24 , prime(x) -> test(x, s(s(0()))) 220.96/95.24 , test(x, y) -> if1(gt(x, y), x, y) 220.96/95.24 , if1(true(), x, y) -> if2(divides(x, y), x, y) 220.96/95.24 , if1(false(), x, y) -> true() } 220.96/95.24 Obligation: 220.96/95.24 runtime complexity 220.96/95.24 Answer: 220.96/95.24 MAYBE 220.96/95.24 220.96/95.24 The weightgap principle applies (using the following nonconstant 220.96/95.24 growth matrix-interpretation) 220.96/95.24 220.96/95.24 The following argument positions are usable: 220.96/95.24 Uargs(if1) = {1}, Uargs(if2) = {1} 220.96/95.24 220.96/95.24 TcT has computed the following matrix interpretation satisfying 220.96/95.24 not(EDA) and not(IDA(1)). 220.96/95.24 220.96/95.24 [gt](x1, x2) = [1] 220.96/95.24 220.96/95.24 [s](x1) = [7] 220.96/95.24 220.96/95.24 [0] = [7] 220.96/95.24 220.96/95.24 [true] = [1] 220.96/95.24 220.96/95.24 [false] = [0] 220.96/95.24 220.96/95.24 [divides](x1, x2) = [1] 220.96/95.24 220.96/95.24 [div](x1, x2, x3) = [1] 220.96/95.24 220.96/95.24 [prime](x1) = [1] x1 + [7] 220.96/95.24 220.96/95.24 [test](x1, x2) = [1] x1 + [5] 220.96/95.24 220.96/95.24 [if1](x1, x2, x3) = [1] x1 + [1] x2 + [4] 220.96/95.24 220.96/95.24 [if2](x1, x2, x3) = [1] x1 + [1] x2 + [0] 220.96/95.24 220.96/95.24 The order satisfies the following ordering constraints: 220.96/95.24 220.96/95.24 [gt(s(x), s(y))] = [1] 220.96/95.24 >= [1] 220.96/95.24 = [gt(x, y)] 220.96/95.24 220.96/95.24 [gt(s(x), 0())] = [1] 220.96/95.24 >= [1] 220.96/95.24 = [true()] 220.96/95.24 220.96/95.24 [gt(0(), y)] = [1] 220.96/95.24 > [0] 220.96/95.24 = [false()] 220.96/95.24 220.96/95.24 [divides(x, y)] = [1] 220.96/95.24 >= [1] 220.96/95.24 = [div(x, y, y)] 220.96/95.24 220.96/95.24 [div(s(x), s(y), z)] = [1] 220.96/95.24 >= [1] 220.96/95.24 = [div(x, y, z)] 220.96/95.24 220.96/95.24 [div(s(x), 0(), s(z))] = [1] 220.96/95.24 >= [1] 220.96/95.24 = [div(s(x), s(z), s(z))] 220.96/95.24 220.96/95.24 [div(0(), s(x), z)] = [1] 220.96/95.24 > [0] 220.96/95.24 = [false()] 220.96/95.24 220.96/95.24 [div(0(), 0(), z)] = [1] 220.96/95.24 >= [1] 220.96/95.24 = [true()] 220.96/95.24 220.96/95.24 [prime(x)] = [1] x + [7] 220.96/95.24 > [1] x + [5] 220.96/95.24 = [test(x, s(s(0())))] 220.96/95.24 220.96/95.24 [test(x, y)] = [1] x + [5] 220.96/95.24 >= [1] x + [5] 220.96/95.24 = [if1(gt(x, y), x, y)] 220.96/95.24 220.96/95.24 [if1(true(), x, y)] = [1] x + [5] 220.96/95.24 > [1] x + [1] 220.96/95.24 = [if2(divides(x, y), x, y)] 220.96/95.24 220.96/95.24 [if1(false(), x, y)] = [1] x + [4] 220.96/95.24 > [1] 220.96/95.24 = [true()] 220.96/95.24 220.96/95.24 [if2(true(), x, y)] = [1] x + [1] 220.96/95.24 > [0] 220.96/95.24 = [false()] 220.96/95.24 220.96/95.24 [if2(false(), x, y)] = [1] x + [0] 220.96/95.24 ? [1] x + [5] 220.96/95.24 = [test(x, s(y))] 220.96/95.24 220.96/95.24 220.96/95.24 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 220.96/95.24 220.96/95.24 We are left with following problem, upon which TcT provides the 220.96/95.24 certificate MAYBE. 220.96/95.24 220.96/95.24 Strict Trs: 220.96/95.24 { gt(s(x), s(y)) -> gt(x, y) 220.96/95.24 , div(s(x), s(y), z) -> div(x, y, z) 220.96/95.24 , div(s(x), 0(), s(z)) -> div(s(x), s(z), s(z)) 220.96/95.24 , if2(false(), x, y) -> test(x, s(y)) } 220.96/95.24 Weak Trs: 220.96/95.24 { gt(s(x), 0()) -> true() 220.96/95.24 , gt(0(), y) -> false() 220.96/95.24 , divides(x, y) -> div(x, y, y) 220.96/95.24 , div(0(), s(x), z) -> false() 220.96/95.24 , div(0(), 0(), z) -> true() 220.96/95.24 , prime(x) -> test(x, s(s(0()))) 220.96/95.24 , test(x, y) -> if1(gt(x, y), x, y) 220.96/95.24 , if1(true(), x, y) -> if2(divides(x, y), x, y) 220.96/95.24 , if1(false(), x, y) -> true() 220.96/95.24 , if2(true(), x, y) -> false() } 220.96/95.24 Obligation: 220.96/95.24 runtime complexity 220.96/95.24 Answer: 220.96/95.24 MAYBE 220.96/95.24 220.96/95.24 None of the processors succeeded. 220.96/95.24 220.96/95.24 Details of failed attempt(s): 220.96/95.24 ----------------------------- 220.96/95.24 1) 'empty' failed due to the following reason: 220.96/95.24 220.96/95.24 Empty strict component of the problem is NOT empty. 220.96/95.24 220.96/95.24 2) 'With Problem ...' failed due to the following reason: 220.96/95.24 220.96/95.24 None of the processors succeeded. 220.96/95.24 220.96/95.24 Details of failed attempt(s): 220.96/95.24 ----------------------------- 220.96/95.24 1) 'empty' failed due to the following reason: 220.96/95.24 220.96/95.24 Empty strict component of the problem is NOT empty. 220.96/95.24 220.96/95.24 2) 'Fastest' failed due to the following reason: 220.96/95.24 220.96/95.24 None of the processors succeeded. 220.96/95.24 220.96/95.24 Details of failed attempt(s): 220.96/95.24 ----------------------------- 220.96/95.24 1) 'With Problem ...' failed due to the following reason: 220.96/95.24 220.96/95.24 None of the processors succeeded. 220.96/95.24 220.96/95.24 Details of failed attempt(s): 220.96/95.24 ----------------------------- 220.96/95.24 1) 'empty' failed due to the following reason: 220.96/95.24 220.96/95.24 Empty strict component of the problem is NOT empty. 220.96/95.24 220.96/95.24 2) 'With Problem ...' failed due to the following reason: 220.96/95.24 220.96/95.24 The weightgap principle applies (using the following nonconstant 220.96/95.24 growth matrix-interpretation) 220.96/95.24 220.96/95.24 The following argument positions are usable: 220.96/95.24 Uargs(if1) = {1}, Uargs(if2) = {1} 220.96/95.24 220.96/95.24 TcT has computed the following matrix interpretation satisfying 220.96/95.24 not(EDA) and not(IDA(1)). 220.96/95.24 220.96/95.24 [gt](x1, x2) = [0 0] x2 + [0] 220.96/95.24 [0 1] [0] 220.96/95.24 220.96/95.24 [s](x1) = [0] 220.96/95.24 [0] 220.96/95.24 220.96/95.24 [0] = [0] 220.96/95.24 [2] 220.96/95.24 220.96/95.24 [true] = [0] 220.96/95.24 [2] 220.96/95.24 220.96/95.24 [false] = [0] 220.96/95.24 [0] 220.96/95.24 220.96/95.24 [divides](x1, x2) = [0] 220.96/95.24 [4] 220.96/95.24 220.96/95.24 [div](x1, x2, x3) = [0] 220.96/95.24 [4] 220.96/95.24 220.96/95.24 [prime](x1) = [7] 220.96/95.24 [7] 220.96/95.24 220.96/95.24 [test](x1, x2) = [0 1] x2 + [6] 220.96/95.24 [0 0] [4] 220.96/95.24 220.96/95.24 [if1](x1, x2, x3) = [1 1] x1 + [6] 220.96/95.24 [0 0] [4] 220.96/95.24 220.96/95.24 [if2](x1, x2, x3) = [1 0] x1 + [7] 220.96/95.24 [0 0] [4] 220.96/95.24 220.96/95.24 The order satisfies the following ordering constraints: 220.96/95.24 220.96/95.24 [gt(s(x), s(y))] = [0] 220.96/95.24 [0] 220.96/95.24 ? [0 0] y + [0] 220.96/95.24 [0 1] [0] 220.96/95.24 = [gt(x, y)] 220.96/95.24 220.96/95.24 [gt(s(x), 0())] = [0] 220.96/95.24 [2] 220.96/95.24 >= [0] 220.96/95.24 [2] 220.96/95.24 = [true()] 220.96/95.24 220.96/95.24 [gt(0(), y)] = [0 0] y + [0] 220.96/95.24 [0 1] [0] 220.96/95.24 >= [0] 220.96/95.24 [0] 220.96/95.24 = [false()] 220.96/95.24 220.96/95.24 [divides(x, y)] = [0] 220.96/95.24 [4] 220.96/95.24 >= [0] 220.96/95.24 [4] 220.96/95.24 = [div(x, y, y)] 220.96/95.24 220.96/95.24 [div(s(x), s(y), z)] = [0] 220.96/95.24 [4] 220.96/95.24 >= [0] 220.96/95.24 [4] 220.96/95.24 = [div(x, y, z)] 220.96/95.24 220.96/95.24 [div(s(x), 0(), s(z))] = [0] 220.96/95.24 [4] 220.96/95.24 >= [0] 220.96/95.24 [4] 220.96/95.24 = [div(s(x), s(z), s(z))] 220.96/95.24 220.96/95.24 [div(0(), s(x), z)] = [0] 220.96/95.24 [4] 220.96/95.24 >= [0] 220.96/95.24 [0] 220.96/95.24 = [false()] 220.96/95.24 220.96/95.24 [div(0(), 0(), z)] = [0] 220.96/95.24 [4] 220.96/95.24 >= [0] 220.96/95.24 [2] 220.96/95.24 = [true()] 220.96/95.24 220.96/95.24 [prime(x)] = [7] 220.96/95.24 [7] 220.96/95.24 > [6] 220.96/95.24 [4] 220.96/95.24 = [test(x, s(s(0())))] 220.96/95.24 220.96/95.24 [test(x, y)] = [0 1] y + [6] 220.96/95.24 [0 0] [4] 220.96/95.24 >= [0 1] y + [6] 220.96/95.24 [0 0] [4] 220.96/95.24 = [if1(gt(x, y), x, y)] 220.96/95.24 220.96/95.24 [if1(true(), x, y)] = [8] 220.96/95.24 [4] 220.96/95.24 > [7] 220.96/95.24 [4] 220.96/95.24 = [if2(divides(x, y), x, y)] 220.96/95.24 220.96/95.24 [if1(false(), x, y)] = [6] 220.96/95.24 [4] 220.96/95.24 > [0] 220.96/95.24 [2] 220.96/95.24 = [true()] 220.96/95.24 220.96/95.24 [if2(true(), x, y)] = [7] 220.96/95.24 [4] 220.96/95.24 > [0] 220.96/95.24 [0] 220.96/95.24 = [false()] 220.96/95.24 220.96/95.24 [if2(false(), x, y)] = [7] 220.96/95.24 [4] 220.96/95.24 > [6] 220.96/95.24 [4] 220.96/95.24 = [test(x, s(y))] 220.96/95.24 220.96/95.24 220.96/95.24 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 220.96/95.24 220.96/95.24 We are left with following problem, upon which TcT provides the 220.96/95.24 certificate MAYBE. 220.96/95.24 220.96/95.24 Strict Trs: 220.96/95.24 { gt(s(x), s(y)) -> gt(x, y) 220.96/95.24 , div(s(x), s(y), z) -> div(x, y, z) 220.96/95.24 , div(s(x), 0(), s(z)) -> div(s(x), s(z), s(z)) } 220.96/95.24 Weak Trs: 220.96/95.24 { gt(s(x), 0()) -> true() 220.96/95.24 , gt(0(), y) -> false() 220.96/95.24 , divides(x, y) -> div(x, y, y) 220.96/95.24 , div(0(), s(x), z) -> false() 220.96/95.24 , div(0(), 0(), z) -> true() 220.96/95.24 , prime(x) -> test(x, s(s(0()))) 220.96/95.24 , test(x, y) -> if1(gt(x, y), x, y) 220.96/95.24 , if1(true(), x, y) -> if2(divides(x, y), x, y) 220.96/95.24 , if1(false(), x, y) -> true() 220.96/95.24 , if2(true(), x, y) -> false() 220.96/95.24 , if2(false(), x, y) -> test(x, s(y)) } 220.96/95.24 Obligation: 220.96/95.24 runtime complexity 220.96/95.24 Answer: 220.96/95.24 MAYBE 220.96/95.24 220.96/95.24 None of the processors succeeded. 220.96/95.24 220.96/95.24 Details of failed attempt(s): 220.96/95.24 ----------------------------- 220.96/95.24 1) 'empty' failed due to the following reason: 220.96/95.24 220.96/95.24 Empty strict component of the problem is NOT empty. 220.96/95.24 220.96/95.24 2) 'With Problem ...' failed due to the following reason: 220.96/95.24 220.96/95.24 None of the processors succeeded. 220.96/95.24 220.96/95.24 Details of failed attempt(s): 220.96/95.24 ----------------------------- 220.96/95.24 1) 'empty' failed due to the following reason: 220.96/95.24 220.96/95.24 Empty strict component of the problem is NOT empty. 220.96/95.24 220.96/95.24 2) 'With Problem ...' failed due to the following reason: 220.96/95.24 220.96/95.24 Empty strict component of the problem is NOT empty. 220.96/95.24 220.96/95.24 220.96/95.24 220.96/95.24 220.96/95.24 2) 'With Problem ...' failed due to the following reason: 220.96/95.24 220.96/95.24 None of the processors succeeded. 220.96/95.24 220.96/95.24 Details of failed attempt(s): 220.96/95.24 ----------------------------- 220.96/95.24 1) 'empty' failed due to the following reason: 220.96/95.24 220.96/95.24 Empty strict component of the problem is NOT empty. 220.96/95.24 220.96/95.24 2) 'With Problem ...' failed due to the following reason: 220.96/95.24 220.96/95.24 Empty strict component of the problem is NOT empty. 220.96/95.24 220.96/95.24 220.96/95.24 220.96/95.24 220.96/95.24 220.96/95.24 2) 'Fastest (timeout of 24 seconds) (timeout of 297 seconds)' 220.96/95.24 failed due to the following reason: 220.96/95.24 220.96/95.24 None of the processors succeeded. 220.96/95.24 220.96/95.24 Details of failed attempt(s): 220.96/95.24 ----------------------------- 220.96/95.24 1) 'Bounds with perSymbol-enrichment and initial automaton 'match'' 220.96/95.24 failed due to the following reason: 220.96/95.24 220.96/95.24 match-boundness of the problem could not be verified. 220.96/95.24 220.96/95.24 2) 'Bounds with minimal-enrichment and initial automaton 'match'' 220.96/95.24 failed due to the following reason: 220.96/95.24 220.96/95.24 match-boundness of the problem could not be verified. 220.96/95.24 220.96/95.24 220.96/95.24 3) 'Best' failed due to the following reason: 220.96/95.24 220.96/95.24 None of the processors succeeded. 220.96/95.24 220.96/95.24 Details of failed attempt(s): 220.96/95.24 ----------------------------- 220.96/95.24 1) 'Polynomial Path Order (PS) (timeout of 297 seconds)' failed due 220.96/95.24 to the following reason: 220.96/95.24 220.96/95.24 The processor is inapplicable, reason: 220.96/95.24 Processor only applicable for innermost runtime complexity analysis 220.96/95.24 220.96/95.24 2) 'bsearch-popstar (timeout of 297 seconds)' failed due to the 220.96/95.24 following reason: 220.96/95.24 220.96/95.24 The processor is inapplicable, reason: 220.96/95.24 Processor only applicable for innermost runtime complexity analysis 220.96/95.24 220.96/95.24 220.96/95.24 220.96/95.24 2) 'Weak Dependency Pairs (timeout of 297 seconds)' failed due to 220.96/95.24 the following reason: 220.96/95.24 220.96/95.24 We add the following weak dependency pairs: 220.96/95.24 220.96/95.24 Strict DPs: 220.96/95.24 { gt^#(s(x), s(y)) -> c_1(gt^#(x, y)) 220.96/95.24 , gt^#(s(x), 0()) -> c_2() 220.96/95.24 , gt^#(0(), y) -> c_3() 220.96/95.24 , divides^#(x, y) -> c_4(div^#(x, y, y)) 220.96/95.24 , div^#(s(x), s(y), z) -> c_5(div^#(x, y, z)) 220.96/95.24 , div^#(s(x), 0(), s(z)) -> c_6(div^#(s(x), s(z), s(z))) 220.96/95.24 , div^#(0(), s(x), z) -> c_7() 220.96/95.24 , div^#(0(), 0(), z) -> c_8() 220.96/95.24 , prime^#(x) -> c_9(test^#(x, s(s(0())))) 220.96/95.24 , test^#(x, y) -> c_10(if1^#(gt(x, y), x, y)) 220.96/95.24 , if1^#(true(), x, y) -> c_11(if2^#(divides(x, y), x, y)) 220.96/95.24 , if1^#(false(), x, y) -> c_12() 220.96/95.24 , if2^#(true(), x, y) -> c_13() 220.96/95.24 , if2^#(false(), x, y) -> c_14(test^#(x, s(y))) } 220.96/95.24 220.96/95.24 and mark the set of starting terms. 220.96/95.24 220.96/95.24 We are left with following problem, upon which TcT provides the 220.96/95.24 certificate MAYBE. 220.96/95.24 220.96/95.24 Strict DPs: 220.96/95.24 { gt^#(s(x), s(y)) -> c_1(gt^#(x, y)) 220.96/95.24 , gt^#(s(x), 0()) -> c_2() 220.96/95.24 , gt^#(0(), y) -> c_3() 220.96/95.24 , divides^#(x, y) -> c_4(div^#(x, y, y)) 220.96/95.24 , div^#(s(x), s(y), z) -> c_5(div^#(x, y, z)) 220.96/95.24 , div^#(s(x), 0(), s(z)) -> c_6(div^#(s(x), s(z), s(z))) 220.96/95.24 , div^#(0(), s(x), z) -> c_7() 220.96/95.24 , div^#(0(), 0(), z) -> c_8() 220.96/95.24 , prime^#(x) -> c_9(test^#(x, s(s(0())))) 220.96/95.24 , test^#(x, y) -> c_10(if1^#(gt(x, y), x, y)) 220.96/95.24 , if1^#(true(), x, y) -> c_11(if2^#(divides(x, y), x, y)) 220.96/95.24 , if1^#(false(), x, y) -> c_12() 220.96/95.24 , if2^#(true(), x, y) -> c_13() 220.96/95.24 , if2^#(false(), x, y) -> c_14(test^#(x, s(y))) } 220.96/95.24 Strict Trs: 220.96/95.24 { gt(s(x), s(y)) -> gt(x, y) 220.96/95.24 , gt(s(x), 0()) -> true() 220.96/95.24 , gt(0(), y) -> false() 220.96/95.24 , divides(x, y) -> div(x, y, y) 220.96/95.24 , div(s(x), s(y), z) -> div(x, y, z) 220.96/95.24 , div(s(x), 0(), s(z)) -> div(s(x), s(z), s(z)) 220.96/95.24 , div(0(), s(x), z) -> false() 220.96/95.24 , div(0(), 0(), z) -> true() 220.96/95.24 , prime(x) -> test(x, s(s(0()))) 220.96/95.24 , test(x, y) -> if1(gt(x, y), x, y) 220.96/95.24 , if1(true(), x, y) -> if2(divides(x, y), x, y) 220.96/95.24 , if1(false(), x, y) -> true() 220.96/95.24 , if2(true(), x, y) -> false() 220.96/95.24 , if2(false(), x, y) -> test(x, s(y)) } 220.96/95.24 Obligation: 220.96/95.24 runtime complexity 220.96/95.24 Answer: 220.96/95.24 MAYBE 220.96/95.24 220.96/95.24 We estimate the number of application of {2,3,7,8,12,13} by 220.96/95.24 applications of Pre({2,3,7,8,12,13}) = {1,4,5,10,11}. Here rules 220.96/95.24 are labeled as follows: 220.96/95.24 220.96/95.24 DPs: 220.96/95.24 { 1: gt^#(s(x), s(y)) -> c_1(gt^#(x, y)) 220.96/95.24 , 2: gt^#(s(x), 0()) -> c_2() 220.96/95.24 , 3: gt^#(0(), y) -> c_3() 220.96/95.24 , 4: divides^#(x, y) -> c_4(div^#(x, y, y)) 220.96/95.24 , 5: div^#(s(x), s(y), z) -> c_5(div^#(x, y, z)) 220.96/95.24 , 6: div^#(s(x), 0(), s(z)) -> c_6(div^#(s(x), s(z), s(z))) 220.96/95.24 , 7: div^#(0(), s(x), z) -> c_7() 220.96/95.24 , 8: div^#(0(), 0(), z) -> c_8() 220.96/95.24 , 9: prime^#(x) -> c_9(test^#(x, s(s(0())))) 220.96/95.24 , 10: test^#(x, y) -> c_10(if1^#(gt(x, y), x, y)) 220.96/95.24 , 11: if1^#(true(), x, y) -> c_11(if2^#(divides(x, y), x, y)) 220.96/95.24 , 12: if1^#(false(), x, y) -> c_12() 220.96/95.24 , 13: if2^#(true(), x, y) -> c_13() 220.96/95.24 , 14: if2^#(false(), x, y) -> c_14(test^#(x, s(y))) } 220.96/95.24 220.96/95.24 We are left with following problem, upon which TcT provides the 220.96/95.24 certificate MAYBE. 220.96/95.24 220.96/95.24 Strict DPs: 220.96/95.24 { gt^#(s(x), s(y)) -> c_1(gt^#(x, y)) 220.96/95.24 , divides^#(x, y) -> c_4(div^#(x, y, y)) 220.96/95.24 , div^#(s(x), s(y), z) -> c_5(div^#(x, y, z)) 220.96/95.24 , div^#(s(x), 0(), s(z)) -> c_6(div^#(s(x), s(z), s(z))) 220.96/95.24 , prime^#(x) -> c_9(test^#(x, s(s(0())))) 220.96/95.25 , test^#(x, y) -> c_10(if1^#(gt(x, y), x, y)) 220.96/95.25 , if1^#(true(), x, y) -> c_11(if2^#(divides(x, y), x, y)) 220.96/95.25 , if2^#(false(), x, y) -> c_14(test^#(x, s(y))) } 220.96/95.25 Strict Trs: 220.96/95.25 { gt(s(x), s(y)) -> gt(x, y) 220.96/95.25 , gt(s(x), 0()) -> true() 220.96/95.25 , gt(0(), y) -> false() 220.96/95.25 , divides(x, y) -> div(x, y, y) 220.96/95.25 , div(s(x), s(y), z) -> div(x, y, z) 220.96/95.25 , div(s(x), 0(), s(z)) -> div(s(x), s(z), s(z)) 220.96/95.25 , div(0(), s(x), z) -> false() 220.96/95.25 , div(0(), 0(), z) -> true() 220.96/95.25 , prime(x) -> test(x, s(s(0()))) 220.96/95.25 , test(x, y) -> if1(gt(x, y), x, y) 220.96/95.25 , if1(true(), x, y) -> if2(divides(x, y), x, y) 220.96/95.25 , if1(false(), x, y) -> true() 220.96/95.25 , if2(true(), x, y) -> false() 220.96/95.25 , if2(false(), x, y) -> test(x, s(y)) } 220.96/95.25 Weak DPs: 220.96/95.25 { gt^#(s(x), 0()) -> c_2() 220.96/95.25 , gt^#(0(), y) -> c_3() 220.96/95.25 , div^#(0(), s(x), z) -> c_7() 220.96/95.25 , div^#(0(), 0(), z) -> c_8() 220.96/95.25 , if1^#(false(), x, y) -> c_12() 220.96/95.25 , if2^#(true(), x, y) -> c_13() } 220.96/95.25 Obligation: 220.96/95.25 runtime complexity 220.96/95.25 Answer: 220.96/95.25 MAYBE 220.96/95.25 220.96/95.25 Empty strict component of the problem is NOT empty. 220.96/95.25 220.96/95.25 220.96/95.25 Arrrr.. 221.20/95.41 EOF