MAYBE 493.88/297.12 MAYBE 493.88/297.12 493.88/297.12 We are left with following problem, upon which TcT provides the 493.88/297.12 certificate MAYBE. 493.88/297.12 493.88/297.12 Strict Trs: 493.88/297.12 { gt(s(x), s(y)) -> gt(x, y) 493.88/297.12 , gt(s(x), 0()) -> true() 493.88/297.12 , gt(0(), y) -> false() 493.88/297.12 , divides(x, y) -> div(x, y, y) 493.88/297.12 , div(s(x), s(y), z) -> div(x, y, z) 493.88/297.12 , div(s(x), 0(), s(z)) -> div(s(x), s(z), s(z)) 493.88/297.12 , div(0(), s(x), z) -> false() 493.88/297.12 , div(0(), 0(), z) -> true() 493.88/297.12 , prime(x) -> test(x, s(s(0()))) 493.88/297.12 , test(x, y) -> if1(gt(x, y), x, y) 493.88/297.12 , if1(true(), x, y) -> if2(divides(x, y), x, y) 493.88/297.12 , if1(false(), x, y) -> true() 493.88/297.12 , if2(true(), x, y) -> false() 493.88/297.12 , if2(false(), x, y) -> test(x, s(y)) } 493.88/297.12 Obligation: 493.88/297.12 innermost runtime complexity 493.88/297.12 Answer: 493.88/297.12 MAYBE 493.88/297.12 493.88/297.12 None of the processors succeeded. 493.88/297.12 493.88/297.12 Details of failed attempt(s): 493.88/297.12 ----------------------------- 493.88/297.12 1) 'empty' failed due to the following reason: 493.88/297.12 493.88/297.12 Empty strict component of the problem is NOT empty. 493.88/297.12 493.88/297.12 2) 'Best' failed due to the following reason: 493.88/297.12 493.88/297.12 None of the processors succeeded. 493.88/297.12 493.88/297.12 Details of failed attempt(s): 493.88/297.12 ----------------------------- 493.88/297.12 1) 'With Problem ... (timeout of 297 seconds)' failed due to the 493.88/297.12 following reason: 493.88/297.12 493.88/297.12 Computation stopped due to timeout after 297.0 seconds. 493.88/297.12 493.88/297.12 2) 'Best' failed due to the following reason: 493.88/297.12 493.88/297.12 None of the processors succeeded. 493.88/297.12 493.88/297.12 Details of failed attempt(s): 493.88/297.12 ----------------------------- 493.88/297.12 1) 'With Problem ... (timeout of 148 seconds) (timeout of 297 493.88/297.12 seconds)' failed due to the following reason: 493.88/297.12 493.88/297.12 The weightgap principle applies (using the following nonconstant 493.88/297.12 growth matrix-interpretation) 493.88/297.12 493.88/297.12 The following argument positions are usable: 493.88/297.12 Uargs(if1) = {1}, Uargs(if2) = {1} 493.88/297.12 493.88/297.12 TcT has computed the following matrix interpretation satisfying 493.88/297.12 not(EDA) and not(IDA(1)). 493.88/297.12 493.88/297.12 [gt](x1, x2) = [4] 493.88/297.12 493.88/297.12 [s](x1) = [7] 493.88/297.12 493.88/297.12 [0] = [7] 493.88/297.12 493.88/297.12 [true] = [0] 493.88/297.12 493.88/297.12 [false] = [0] 493.88/297.12 493.88/297.12 [divides](x1, x2) = [0] 493.88/297.12 493.88/297.12 [div](x1, x2, x3) = [0] 493.88/297.12 493.88/297.12 [prime](x1) = [1] x1 + [7] 493.88/297.12 493.88/297.12 [test](x1, x2) = [1] x1 + [0] 493.88/297.12 493.88/297.12 [if1](x1, x2, x3) = [1] x1 + [1] x2 + [0] 493.88/297.12 493.88/297.12 [if2](x1, x2, x3) = [1] x1 + [1] x2 + [0] 493.88/297.12 493.88/297.12 The order satisfies the following ordering constraints: 493.88/297.12 493.88/297.12 [gt(s(x), s(y))] = [4] 493.88/297.13 >= [4] 493.88/297.13 = [gt(x, y)] 493.88/297.13 493.88/297.13 [gt(s(x), 0())] = [4] 493.88/297.13 > [0] 493.88/297.13 = [true()] 493.88/297.13 493.88/297.13 [gt(0(), y)] = [4] 493.88/297.13 > [0] 493.88/297.13 = [false()] 493.88/297.13 493.88/297.13 [divides(x, y)] = [0] 493.88/297.13 >= [0] 493.88/297.13 = [div(x, y, y)] 493.88/297.13 493.88/297.13 [div(s(x), s(y), z)] = [0] 493.88/297.13 >= [0] 493.88/297.13 = [div(x, y, z)] 493.88/297.13 493.88/297.13 [div(s(x), 0(), s(z))] = [0] 493.88/297.13 >= [0] 493.88/297.13 = [div(s(x), s(z), s(z))] 493.88/297.13 493.88/297.13 [div(0(), s(x), z)] = [0] 493.88/297.13 >= [0] 493.88/297.13 = [false()] 493.88/297.13 493.88/297.13 [div(0(), 0(), z)] = [0] 493.88/297.13 >= [0] 493.88/297.13 = [true()] 493.88/297.13 493.88/297.13 [prime(x)] = [1] x + [7] 493.88/297.13 > [1] x + [0] 493.88/297.13 = [test(x, s(s(0())))] 493.88/297.13 493.88/297.13 [test(x, y)] = [1] x + [0] 493.88/297.13 ? [1] x + [4] 493.88/297.13 = [if1(gt(x, y), x, y)] 493.88/297.13 493.88/297.13 [if1(true(), x, y)] = [1] x + [0] 493.88/297.13 >= [1] x + [0] 493.88/297.13 = [if2(divides(x, y), x, y)] 493.88/297.13 493.88/297.13 [if1(false(), x, y)] = [1] x + [0] 493.88/297.13 >= [0] 493.88/297.13 = [true()] 493.88/297.13 493.88/297.13 [if2(true(), x, y)] = [1] x + [0] 493.88/297.13 >= [0] 493.88/297.13 = [false()] 493.88/297.13 493.88/297.13 [if2(false(), x, y)] = [1] x + [0] 493.88/297.13 >= [1] x + [0] 493.88/297.13 = [test(x, s(y))] 493.88/297.13 493.88/297.13 493.88/297.13 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 493.88/297.13 493.88/297.13 We are left with following problem, upon which TcT provides the 493.88/297.13 certificate MAYBE. 493.88/297.13 493.88/297.13 Strict Trs: 493.88/297.13 { gt(s(x), s(y)) -> gt(x, y) 493.88/297.13 , divides(x, y) -> div(x, y, y) 493.88/297.13 , div(s(x), s(y), z) -> div(x, y, z) 493.88/297.13 , div(s(x), 0(), s(z)) -> div(s(x), s(z), s(z)) 493.88/297.13 , div(0(), s(x), z) -> false() 493.88/297.13 , div(0(), 0(), z) -> true() 493.88/297.13 , test(x, y) -> if1(gt(x, y), x, y) 493.88/297.13 , if1(true(), x, y) -> if2(divides(x, y), x, y) 493.88/297.13 , if1(false(), x, y) -> true() 493.88/297.13 , if2(true(), x, y) -> false() 493.88/297.13 , if2(false(), x, y) -> test(x, s(y)) } 493.88/297.13 Weak Trs: 493.88/297.13 { gt(s(x), 0()) -> true() 493.88/297.13 , gt(0(), y) -> false() 493.88/297.13 , prime(x) -> test(x, s(s(0()))) } 493.88/297.13 Obligation: 493.88/297.13 innermost runtime complexity 493.88/297.13 Answer: 493.88/297.13 MAYBE 493.88/297.13 493.88/297.13 The weightgap principle applies (using the following nonconstant 493.88/297.13 growth matrix-interpretation) 493.88/297.13 493.88/297.13 The following argument positions are usable: 493.88/297.13 Uargs(if1) = {1}, Uargs(if2) = {1} 493.88/297.13 493.88/297.13 TcT has computed the following matrix interpretation satisfying 493.88/297.13 not(EDA) and not(IDA(1)). 493.88/297.13 493.88/297.13 [gt](x1, x2) = [4] 493.88/297.13 493.88/297.13 [s](x1) = [7] 493.88/297.13 493.88/297.13 [0] = [7] 493.88/297.13 493.88/297.13 [true] = [0] 493.88/297.13 493.88/297.13 [false] = [0] 493.88/297.13 493.88/297.13 [divides](x1, x2) = [1] 493.88/297.13 493.88/297.13 [div](x1, x2, x3) = [0] 493.88/297.13 493.88/297.13 [prime](x1) = [1] x1 + [7] 493.88/297.13 493.88/297.13 [test](x1, x2) = [1] x1 + [0] 493.88/297.13 493.88/297.13 [if1](x1, x2, x3) = [1] x1 + [1] x2 + [0] 493.88/297.13 493.88/297.13 [if2](x1, x2, x3) = [1] x1 + [1] x2 + [0] 493.88/297.13 493.88/297.13 The order satisfies the following ordering constraints: 493.88/297.13 493.88/297.13 [gt(s(x), s(y))] = [4] 493.88/297.13 >= [4] 493.88/297.13 = [gt(x, y)] 493.88/297.13 493.88/297.13 [gt(s(x), 0())] = [4] 493.88/297.13 > [0] 493.88/297.13 = [true()] 493.88/297.13 493.88/297.13 [gt(0(), y)] = [4] 493.88/297.13 > [0] 493.88/297.13 = [false()] 493.88/297.13 493.88/297.13 [divides(x, y)] = [1] 493.88/297.13 > [0] 493.88/297.13 = [div(x, y, y)] 493.88/297.13 493.88/297.13 [div(s(x), s(y), z)] = [0] 493.88/297.13 >= [0] 493.88/297.13 = [div(x, y, z)] 493.88/297.13 493.88/297.13 [div(s(x), 0(), s(z))] = [0] 493.88/297.13 >= [0] 493.88/297.13 = [div(s(x), s(z), s(z))] 493.88/297.13 493.88/297.13 [div(0(), s(x), z)] = [0] 493.88/297.13 >= [0] 493.88/297.13 = [false()] 493.88/297.13 493.88/297.13 [div(0(), 0(), z)] = [0] 493.88/297.13 >= [0] 493.88/297.13 = [true()] 493.88/297.13 493.88/297.13 [prime(x)] = [1] x + [7] 493.88/297.13 > [1] x + [0] 493.88/297.13 = [test(x, s(s(0())))] 493.88/297.13 493.88/297.13 [test(x, y)] = [1] x + [0] 493.88/297.13 ? [1] x + [4] 493.88/297.13 = [if1(gt(x, y), x, y)] 493.88/297.13 493.88/297.13 [if1(true(), x, y)] = [1] x + [0] 493.88/297.13 ? [1] x + [1] 493.88/297.13 = [if2(divides(x, y), x, y)] 493.88/297.13 493.88/297.13 [if1(false(), x, y)] = [1] x + [0] 493.88/297.13 >= [0] 493.88/297.13 = [true()] 493.88/297.13 493.88/297.13 [if2(true(), x, y)] = [1] x + [0] 493.88/297.13 >= [0] 493.88/297.13 = [false()] 493.88/297.13 493.88/297.13 [if2(false(), x, y)] = [1] x + [0] 493.88/297.13 >= [1] x + [0] 493.88/297.13 = [test(x, s(y))] 493.88/297.13 493.88/297.13 493.88/297.13 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 493.88/297.13 493.88/297.13 We are left with following problem, upon which TcT provides the 493.88/297.13 certificate MAYBE. 493.88/297.13 493.88/297.13 Strict Trs: 493.88/297.13 { gt(s(x), s(y)) -> gt(x, y) 493.88/297.13 , div(s(x), s(y), z) -> div(x, y, z) 493.88/297.13 , div(s(x), 0(), s(z)) -> div(s(x), s(z), s(z)) 493.88/297.13 , div(0(), s(x), z) -> false() 493.88/297.13 , div(0(), 0(), z) -> true() 493.88/297.13 , test(x, y) -> if1(gt(x, y), x, y) 493.88/297.13 , if1(true(), x, y) -> if2(divides(x, y), x, y) 493.88/297.13 , if1(false(), x, y) -> true() 493.88/297.13 , if2(true(), x, y) -> false() 493.88/297.13 , if2(false(), x, y) -> test(x, s(y)) } 493.88/297.13 Weak Trs: 493.88/297.13 { gt(s(x), 0()) -> true() 493.88/297.13 , gt(0(), y) -> false() 493.88/297.13 , divides(x, y) -> div(x, y, y) 493.88/297.13 , prime(x) -> test(x, s(s(0()))) } 493.88/297.13 Obligation: 493.88/297.13 innermost runtime complexity 493.88/297.13 Answer: 493.88/297.13 MAYBE 493.88/297.13 493.88/297.13 The weightgap principle applies (using the following nonconstant 493.88/297.13 growth matrix-interpretation) 493.88/297.13 493.88/297.13 The following argument positions are usable: 493.88/297.13 Uargs(if1) = {1}, Uargs(if2) = {1} 493.88/297.13 493.88/297.13 TcT has computed the following matrix interpretation satisfying 493.88/297.13 not(EDA) and not(IDA(1)). 493.88/297.13 493.88/297.13 [gt](x1, x2) = [4] 493.88/297.13 493.88/297.13 [s](x1) = [7] 493.88/297.13 493.88/297.13 [0] = [7] 493.88/297.13 493.88/297.13 [true] = [0] 493.88/297.13 493.88/297.13 [false] = [0] 493.88/297.13 493.88/297.13 [divides](x1, x2) = [4] 493.88/297.13 493.88/297.13 [div](x1, x2, x3) = [0] 493.88/297.13 493.88/297.13 [prime](x1) = [1] x1 + [7] 493.88/297.13 493.88/297.13 [test](x1, x2) = [1] x1 + [5] 493.88/297.13 493.88/297.13 [if1](x1, x2, x3) = [1] x1 + [1] x2 + [0] 493.88/297.13 493.88/297.13 [if2](x1, x2, x3) = [1] x1 + [1] x2 + [0] 493.88/297.13 493.88/297.13 The order satisfies the following ordering constraints: 493.88/297.13 493.88/297.13 [gt(s(x), s(y))] = [4] 493.88/297.13 >= [4] 493.88/297.13 = [gt(x, y)] 493.88/297.13 493.88/297.13 [gt(s(x), 0())] = [4] 493.88/297.13 > [0] 493.88/297.13 = [true()] 493.88/297.13 493.88/297.13 [gt(0(), y)] = [4] 493.88/297.13 > [0] 493.88/297.13 = [false()] 493.88/297.13 493.88/297.13 [divides(x, y)] = [4] 493.88/297.13 > [0] 493.88/297.13 = [div(x, y, y)] 493.88/297.13 493.88/297.13 [div(s(x), s(y), z)] = [0] 493.88/297.13 >= [0] 493.88/297.13 = [div(x, y, z)] 493.88/297.13 493.88/297.13 [div(s(x), 0(), s(z))] = [0] 493.88/297.13 >= [0] 493.88/297.13 = [div(s(x), s(z), s(z))] 493.88/297.13 493.88/297.13 [div(0(), s(x), z)] = [0] 493.88/297.13 >= [0] 493.88/297.13 = [false()] 493.88/297.13 493.88/297.13 [div(0(), 0(), z)] = [0] 493.88/297.13 >= [0] 493.88/297.13 = [true()] 493.88/297.13 493.88/297.13 [prime(x)] = [1] x + [7] 493.88/297.13 > [1] x + [5] 493.88/297.13 = [test(x, s(s(0())))] 493.88/297.13 493.88/297.13 [test(x, y)] = [1] x + [5] 493.88/297.13 > [1] x + [4] 493.88/297.13 = [if1(gt(x, y), x, y)] 493.88/297.13 493.88/297.13 [if1(true(), x, y)] = [1] x + [0] 493.88/297.13 ? [1] x + [4] 493.88/297.13 = [if2(divides(x, y), x, y)] 493.88/297.13 493.88/297.13 [if1(false(), x, y)] = [1] x + [0] 493.88/297.13 >= [0] 493.88/297.13 = [true()] 493.88/297.13 493.88/297.13 [if2(true(), x, y)] = [1] x + [0] 493.88/297.13 >= [0] 493.88/297.13 = [false()] 493.88/297.13 493.88/297.13 [if2(false(), x, y)] = [1] x + [0] 493.88/297.13 ? [1] x + [5] 493.88/297.13 = [test(x, s(y))] 493.88/297.13 493.88/297.13 493.88/297.13 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 493.88/297.13 493.88/297.13 We are left with following problem, upon which TcT provides the 493.88/297.13 certificate MAYBE. 493.88/297.13 493.88/297.13 Strict Trs: 493.88/297.13 { gt(s(x), s(y)) -> gt(x, y) 493.88/297.13 , div(s(x), s(y), z) -> div(x, y, z) 493.88/297.13 , div(s(x), 0(), s(z)) -> div(s(x), s(z), s(z)) 493.88/297.13 , div(0(), s(x), z) -> false() 493.88/297.13 , div(0(), 0(), z) -> true() 493.88/297.13 , if1(true(), x, y) -> if2(divides(x, y), x, y) 493.88/297.13 , if1(false(), x, y) -> true() 493.88/297.13 , if2(true(), x, y) -> false() 493.88/297.13 , if2(false(), x, y) -> test(x, s(y)) } 493.88/297.13 Weak Trs: 493.88/297.13 { gt(s(x), 0()) -> true() 493.88/297.13 , gt(0(), y) -> false() 493.88/297.13 , divides(x, y) -> div(x, y, y) 493.88/297.13 , prime(x) -> test(x, s(s(0()))) 493.88/297.13 , test(x, y) -> if1(gt(x, y), x, y) } 493.88/297.13 Obligation: 493.88/297.13 innermost runtime complexity 493.88/297.13 Answer: 493.88/297.13 MAYBE 493.88/297.13 493.88/297.13 The weightgap principle applies (using the following nonconstant 493.88/297.13 growth matrix-interpretation) 493.88/297.13 493.88/297.13 The following argument positions are usable: 493.88/297.13 Uargs(if1) = {1}, Uargs(if2) = {1} 493.88/297.13 493.88/297.13 TcT has computed the following matrix interpretation satisfying 493.88/297.13 not(EDA) and not(IDA(1)). 493.88/297.13 493.88/297.13 [gt](x1, x2) = [1] 493.88/297.13 493.88/297.13 [s](x1) = [7] 493.88/297.13 493.88/297.13 [0] = [7] 493.88/297.13 493.88/297.13 [true] = [0] 493.88/297.13 493.88/297.13 [false] = [1] 493.88/297.13 493.88/297.13 [divides](x1, x2) = [4] 493.88/297.13 493.88/297.13 [div](x1, x2, x3) = [0] 493.88/297.13 493.88/297.13 [prime](x1) = [1] x1 + [7] 493.88/297.13 493.88/297.13 [test](x1, x2) = [1] x1 + [4] 493.88/297.13 493.88/297.13 [if1](x1, x2, x3) = [1] x1 + [1] x2 + [0] 493.88/297.13 493.88/297.13 [if2](x1, x2, x3) = [1] x1 + [1] x2 + [0] 493.88/297.13 493.88/297.13 The order satisfies the following ordering constraints: 493.88/297.13 493.88/297.13 [gt(s(x), s(y))] = [1] 493.88/297.13 >= [1] 493.88/297.13 = [gt(x, y)] 493.88/297.13 493.88/297.13 [gt(s(x), 0())] = [1] 493.88/297.13 > [0] 493.88/297.13 = [true()] 493.88/297.13 493.88/297.13 [gt(0(), y)] = [1] 493.88/297.13 >= [1] 493.88/297.13 = [false()] 493.88/297.13 493.88/297.13 [divides(x, y)] = [4] 493.88/297.13 > [0] 493.88/297.13 = [div(x, y, y)] 493.88/297.13 493.88/297.13 [div(s(x), s(y), z)] = [0] 493.88/297.13 >= [0] 493.88/297.13 = [div(x, y, z)] 493.88/297.13 493.88/297.13 [div(s(x), 0(), s(z))] = [0] 493.88/297.13 >= [0] 493.88/297.13 = [div(s(x), s(z), s(z))] 493.88/297.13 493.88/297.13 [div(0(), s(x), z)] = [0] 493.88/297.13 ? [1] 493.88/297.13 = [false()] 493.88/297.13 493.88/297.13 [div(0(), 0(), z)] = [0] 493.88/297.13 >= [0] 493.88/297.13 = [true()] 493.88/297.13 493.88/297.13 [prime(x)] = [1] x + [7] 493.88/297.13 > [1] x + [4] 493.88/297.13 = [test(x, s(s(0())))] 493.88/297.13 493.88/297.13 [test(x, y)] = [1] x + [4] 493.88/297.13 > [1] x + [1] 493.88/297.13 = [if1(gt(x, y), x, y)] 493.88/297.13 493.88/297.13 [if1(true(), x, y)] = [1] x + [0] 493.88/297.13 ? [1] x + [4] 493.88/297.13 = [if2(divides(x, y), x, y)] 493.88/297.13 493.88/297.13 [if1(false(), x, y)] = [1] x + [1] 493.88/297.13 > [0] 493.88/297.13 = [true()] 493.88/297.13 493.88/297.13 [if2(true(), x, y)] = [1] x + [0] 493.88/297.13 ? [1] 493.88/297.13 = [false()] 493.88/297.13 493.88/297.13 [if2(false(), x, y)] = [1] x + [1] 493.88/297.13 ? [1] x + [4] 493.88/297.13 = [test(x, s(y))] 493.88/297.13 493.88/297.13 493.88/297.13 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 493.88/297.13 493.88/297.13 We are left with following problem, upon which TcT provides the 493.88/297.13 certificate MAYBE. 493.88/297.13 493.88/297.13 Strict Trs: 493.88/297.13 { gt(s(x), s(y)) -> gt(x, y) 493.88/297.13 , div(s(x), s(y), z) -> div(x, y, z) 493.88/297.13 , div(s(x), 0(), s(z)) -> div(s(x), s(z), s(z)) 493.88/297.13 , div(0(), s(x), z) -> false() 493.88/297.13 , div(0(), 0(), z) -> true() 493.88/297.13 , if1(true(), x, y) -> if2(divides(x, y), x, y) 493.88/297.13 , if2(true(), x, y) -> false() 493.88/297.13 , if2(false(), x, y) -> test(x, s(y)) } 493.88/297.13 Weak Trs: 493.88/297.13 { gt(s(x), 0()) -> true() 493.88/297.13 , gt(0(), y) -> false() 493.88/297.13 , divides(x, y) -> div(x, y, y) 493.88/297.13 , prime(x) -> test(x, s(s(0()))) 493.88/297.13 , test(x, y) -> if1(gt(x, y), x, y) 493.88/297.13 , if1(false(), x, y) -> true() } 493.88/297.13 Obligation: 493.88/297.13 innermost runtime complexity 493.88/297.13 Answer: 493.88/297.13 MAYBE 493.88/297.13 493.88/297.13 The weightgap principle applies (using the following nonconstant 493.88/297.13 growth matrix-interpretation) 493.88/297.13 493.88/297.13 The following argument positions are usable: 493.88/297.13 Uargs(if1) = {1}, Uargs(if2) = {1} 493.88/297.13 493.88/297.13 TcT has computed the following matrix interpretation satisfying 493.88/297.13 not(EDA) and not(IDA(1)). 493.88/297.13 493.88/297.13 [gt](x1, x2) = [0] 493.88/297.13 493.88/297.13 [s](x1) = [3] 493.88/297.13 493.88/297.13 [0] = [7] 493.88/297.13 493.88/297.13 [true] = [0] 493.88/297.13 493.88/297.13 [false] = [0] 493.88/297.13 493.88/297.13 [divides](x1, x2) = [4] 493.88/297.13 493.88/297.13 [div](x1, x2, x3) = [4] 493.88/297.13 493.88/297.13 [prime](x1) = [1] x1 + [7] 493.88/297.13 493.88/297.13 [test](x1, x2) = [1] x1 + [4] 493.88/297.13 493.88/297.13 [if1](x1, x2, x3) = [1] x1 + [1] x2 + [0] 493.88/297.13 493.88/297.13 [if2](x1, x2, x3) = [1] x1 + [1] x2 + [0] 493.88/297.13 493.88/297.13 The order satisfies the following ordering constraints: 493.88/297.13 493.88/297.13 [gt(s(x), s(y))] = [0] 493.88/297.13 >= [0] 493.88/297.13 = [gt(x, y)] 493.88/297.13 493.88/297.13 [gt(s(x), 0())] = [0] 493.88/297.13 >= [0] 493.88/297.13 = [true()] 493.88/297.13 493.88/297.13 [gt(0(), y)] = [0] 493.88/297.13 >= [0] 493.88/297.13 = [false()] 493.88/297.13 493.88/297.13 [divides(x, y)] = [4] 493.88/297.13 >= [4] 493.88/297.13 = [div(x, y, y)] 493.88/297.13 493.88/297.13 [div(s(x), s(y), z)] = [4] 493.88/297.13 >= [4] 493.88/297.13 = [div(x, y, z)] 493.88/297.13 493.88/297.13 [div(s(x), 0(), s(z))] = [4] 493.88/297.13 >= [4] 493.88/297.13 = [div(s(x), s(z), s(z))] 493.88/297.13 493.88/297.13 [div(0(), s(x), z)] = [4] 493.88/297.13 > [0] 493.88/297.13 = [false()] 493.88/297.13 493.88/297.13 [div(0(), 0(), z)] = [4] 493.88/297.13 > [0] 493.88/297.13 = [true()] 493.88/297.13 493.88/297.13 [prime(x)] = [1] x + [7] 493.88/297.13 > [1] x + [4] 493.88/297.13 = [test(x, s(s(0())))] 493.88/297.13 493.88/297.13 [test(x, y)] = [1] x + [4] 493.88/297.13 > [1] x + [0] 493.88/297.13 = [if1(gt(x, y), x, y)] 493.88/297.13 493.88/297.13 [if1(true(), x, y)] = [1] x + [0] 493.88/297.13 ? [1] x + [4] 493.88/297.13 = [if2(divides(x, y), x, y)] 493.88/297.13 493.88/297.13 [if1(false(), x, y)] = [1] x + [0] 493.88/297.13 >= [0] 493.88/297.13 = [true()] 493.88/297.13 493.88/297.13 [if2(true(), x, y)] = [1] x + [0] 493.88/297.13 >= [0] 493.88/297.13 = [false()] 493.88/297.13 493.88/297.13 [if2(false(), x, y)] = [1] x + [0] 493.88/297.13 ? [1] x + [4] 493.88/297.13 = [test(x, s(y))] 493.88/297.13 493.88/297.13 493.88/297.13 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 493.88/297.13 493.88/297.13 We are left with following problem, upon which TcT provides the 493.88/297.13 certificate MAYBE. 493.88/297.13 493.88/297.13 Strict Trs: 493.88/297.13 { gt(s(x), s(y)) -> gt(x, y) 493.88/297.13 , div(s(x), s(y), z) -> div(x, y, z) 493.88/297.13 , div(s(x), 0(), s(z)) -> div(s(x), s(z), s(z)) 493.88/297.13 , if1(true(), x, y) -> if2(divides(x, y), x, y) 493.88/297.13 , if2(true(), x, y) -> false() 493.88/297.13 , if2(false(), x, y) -> test(x, s(y)) } 493.88/297.13 Weak Trs: 493.88/297.13 { gt(s(x), 0()) -> true() 493.88/297.13 , gt(0(), y) -> false() 493.88/297.13 , divides(x, y) -> div(x, y, y) 493.88/297.13 , div(0(), s(x), z) -> false() 493.88/297.13 , div(0(), 0(), z) -> true() 493.88/297.13 , prime(x) -> test(x, s(s(0()))) 493.88/297.13 , test(x, y) -> if1(gt(x, y), x, y) 493.88/297.13 , if1(false(), x, y) -> true() } 493.88/297.13 Obligation: 493.88/297.13 innermost runtime complexity 493.88/297.13 Answer: 493.88/297.13 MAYBE 493.88/297.13 493.88/297.13 The weightgap principle applies (using the following nonconstant 493.88/297.13 growth matrix-interpretation) 493.88/297.13 493.88/297.13 The following argument positions are usable: 493.88/297.13 Uargs(if1) = {1}, Uargs(if2) = {1} 493.88/297.13 493.88/297.13 TcT has computed the following matrix interpretation satisfying 493.88/297.13 not(EDA) and not(IDA(1)). 493.88/297.13 493.88/297.13 [gt](x1, x2) = [2] 493.88/297.13 493.88/297.13 [s](x1) = [7] 493.88/297.13 493.88/297.13 [0] = [7] 493.88/297.13 493.88/297.13 [true] = [0] 493.88/297.13 493.88/297.13 [false] = [0] 493.88/297.13 493.88/297.13 [divides](x1, x2) = [0] 493.88/297.13 493.88/297.13 [div](x1, x2, x3) = [0] 493.88/297.13 493.88/297.13 [prime](x1) = [1] x1 + [7] 493.88/297.13 493.88/297.13 [test](x1, x2) = [4] 493.88/297.13 493.88/297.13 [if1](x1, x2, x3) = [1] x1 + [2] 493.88/297.13 493.88/297.13 [if2](x1, x2, x3) = [1] x1 + [0] 493.88/297.13 493.88/297.13 The order satisfies the following ordering constraints: 493.88/297.13 493.88/297.13 [gt(s(x), s(y))] = [2] 493.88/297.13 >= [2] 493.88/297.13 = [gt(x, y)] 493.88/297.13 493.88/297.13 [gt(s(x), 0())] = [2] 493.88/297.13 > [0] 493.88/297.13 = [true()] 493.88/297.13 493.88/297.13 [gt(0(), y)] = [2] 493.88/297.13 > [0] 493.88/297.13 = [false()] 493.88/297.13 493.88/297.13 [divides(x, y)] = [0] 493.88/297.13 >= [0] 493.88/297.13 = [div(x, y, y)] 493.88/297.13 493.88/297.13 [div(s(x), s(y), z)] = [0] 493.88/297.13 >= [0] 493.88/297.13 = [div(x, y, z)] 493.88/297.13 493.88/297.13 [div(s(x), 0(), s(z))] = [0] 493.88/297.13 >= [0] 493.88/297.13 = [div(s(x), s(z), s(z))] 493.88/297.13 493.88/297.13 [div(0(), s(x), z)] = [0] 493.88/297.13 >= [0] 493.88/297.13 = [false()] 493.88/297.13 493.88/297.13 [div(0(), 0(), z)] = [0] 493.88/297.13 >= [0] 493.88/297.13 = [true()] 493.88/297.13 493.88/297.13 [prime(x)] = [1] x + [7] 493.88/297.13 > [4] 493.88/297.13 = [test(x, s(s(0())))] 493.88/297.13 493.88/297.13 [test(x, y)] = [4] 493.88/297.13 >= [4] 493.88/297.13 = [if1(gt(x, y), x, y)] 493.88/297.13 493.88/297.13 [if1(true(), x, y)] = [2] 493.88/297.13 > [0] 493.88/297.13 = [if2(divides(x, y), x, y)] 493.88/297.13 493.88/297.13 [if1(false(), x, y)] = [2] 493.88/297.13 > [0] 493.88/297.13 = [true()] 493.88/297.13 493.88/297.13 [if2(true(), x, y)] = [0] 493.88/297.13 >= [0] 493.88/297.13 = [false()] 493.88/297.13 493.88/297.13 [if2(false(), x, y)] = [0] 493.88/297.13 ? [4] 493.88/297.13 = [test(x, s(y))] 493.88/297.13 493.88/297.13 493.88/297.13 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 493.88/297.13 493.88/297.13 We are left with following problem, upon which TcT provides the 493.88/297.13 certificate MAYBE. 493.88/297.13 493.88/297.13 Strict Trs: 493.88/297.13 { gt(s(x), s(y)) -> gt(x, y) 493.88/297.13 , div(s(x), s(y), z) -> div(x, y, z) 493.88/297.13 , div(s(x), 0(), s(z)) -> div(s(x), s(z), s(z)) 493.88/297.13 , if2(true(), x, y) -> false() 493.88/297.13 , if2(false(), x, y) -> test(x, s(y)) } 493.88/297.13 Weak Trs: 493.88/297.13 { gt(s(x), 0()) -> true() 493.88/297.13 , gt(0(), y) -> false() 493.88/297.13 , divides(x, y) -> div(x, y, y) 493.88/297.13 , div(0(), s(x), z) -> false() 493.88/297.13 , div(0(), 0(), z) -> true() 493.88/297.13 , prime(x) -> test(x, s(s(0()))) 493.88/297.13 , test(x, y) -> if1(gt(x, y), x, y) 493.88/297.13 , if1(true(), x, y) -> if2(divides(x, y), x, y) 493.88/297.13 , if1(false(), x, y) -> true() } 493.88/297.13 Obligation: 493.88/297.13 innermost runtime complexity 493.88/297.13 Answer: 493.88/297.13 MAYBE 493.88/297.13 493.88/297.13 The weightgap principle applies (using the following nonconstant 493.88/297.13 growth matrix-interpretation) 493.88/297.13 493.88/297.13 The following argument positions are usable: 493.88/297.13 Uargs(if1) = {1}, Uargs(if2) = {1} 493.88/297.13 493.88/297.13 TcT has computed the following matrix interpretation satisfying 493.88/297.13 not(EDA) and not(IDA(1)). 493.88/297.13 493.88/297.13 [gt](x1, x2) = [1] 493.88/297.13 493.88/297.13 [s](x1) = [7] 493.88/297.13 493.88/297.13 [0] = [7] 493.88/297.13 493.88/297.13 [true] = [1] 493.88/297.13 493.88/297.13 [false] = [0] 493.88/297.13 493.88/297.13 [divides](x1, x2) = [1] 493.88/297.13 493.88/297.13 [div](x1, x2, x3) = [1] 493.88/297.13 493.88/297.13 [prime](x1) = [1] x1 + [7] 493.88/297.13 493.88/297.13 [test](x1, x2) = [1] x1 + [5] 493.88/297.13 493.88/297.13 [if1](x1, x2, x3) = [1] x1 + [1] x2 + [4] 493.88/297.13 493.88/297.13 [if2](x1, x2, x3) = [1] x1 + [1] x2 + [0] 493.88/297.13 493.88/297.13 The order satisfies the following ordering constraints: 493.88/297.13 493.88/297.13 [gt(s(x), s(y))] = [1] 493.88/297.13 >= [1] 493.88/297.13 = [gt(x, y)] 493.88/297.13 493.88/297.13 [gt(s(x), 0())] = [1] 493.88/297.13 >= [1] 493.88/297.13 = [true()] 493.88/297.13 493.88/297.13 [gt(0(), y)] = [1] 493.88/297.13 > [0] 493.88/297.13 = [false()] 493.88/297.13 493.88/297.13 [divides(x, y)] = [1] 493.88/297.13 >= [1] 493.88/297.13 = [div(x, y, y)] 493.88/297.13 493.88/297.13 [div(s(x), s(y), z)] = [1] 493.88/297.13 >= [1] 493.88/297.13 = [div(x, y, z)] 493.88/297.13 493.88/297.13 [div(s(x), 0(), s(z))] = [1] 493.88/297.13 >= [1] 493.88/297.13 = [div(s(x), s(z), s(z))] 493.88/297.13 493.88/297.13 [div(0(), s(x), z)] = [1] 493.88/297.13 > [0] 493.88/297.13 = [false()] 493.88/297.13 493.88/297.13 [div(0(), 0(), z)] = [1] 493.88/297.13 >= [1] 493.88/297.13 = [true()] 493.88/297.13 493.88/297.13 [prime(x)] = [1] x + [7] 493.88/297.13 > [1] x + [5] 493.88/297.13 = [test(x, s(s(0())))] 493.88/297.13 493.88/297.13 [test(x, y)] = [1] x + [5] 493.88/297.13 >= [1] x + [5] 493.88/297.13 = [if1(gt(x, y), x, y)] 493.88/297.13 493.88/297.13 [if1(true(), x, y)] = [1] x + [5] 493.88/297.13 > [1] x + [1] 493.88/297.13 = [if2(divides(x, y), x, y)] 493.88/297.13 493.88/297.13 [if1(false(), x, y)] = [1] x + [4] 493.88/297.13 > [1] 493.88/297.13 = [true()] 493.88/297.13 493.88/297.13 [if2(true(), x, y)] = [1] x + [1] 493.88/297.13 > [0] 493.88/297.13 = [false()] 493.88/297.13 493.88/297.13 [if2(false(), x, y)] = [1] x + [0] 493.88/297.13 ? [1] x + [5] 493.88/297.13 = [test(x, s(y))] 493.88/297.13 493.88/297.13 493.88/297.13 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 493.88/297.13 493.88/297.13 We are left with following problem, upon which TcT provides the 493.88/297.13 certificate MAYBE. 493.88/297.13 493.88/297.13 Strict Trs: 493.88/297.13 { gt(s(x), s(y)) -> gt(x, y) 493.88/297.13 , div(s(x), s(y), z) -> div(x, y, z) 493.88/297.13 , div(s(x), 0(), s(z)) -> div(s(x), s(z), s(z)) 493.88/297.13 , if2(false(), x, y) -> test(x, s(y)) } 493.88/297.13 Weak Trs: 493.88/297.13 { gt(s(x), 0()) -> true() 493.88/297.13 , gt(0(), y) -> false() 493.88/297.13 , divides(x, y) -> div(x, y, y) 493.88/297.13 , div(0(), s(x), z) -> false() 493.88/297.13 , div(0(), 0(), z) -> true() 493.88/297.13 , prime(x) -> test(x, s(s(0()))) 493.88/297.13 , test(x, y) -> if1(gt(x, y), x, y) 493.88/297.13 , if1(true(), x, y) -> if2(divides(x, y), x, y) 493.88/297.13 , if1(false(), x, y) -> true() 493.88/297.13 , if2(true(), x, y) -> false() } 493.88/297.13 Obligation: 493.88/297.13 innermost runtime complexity 493.88/297.13 Answer: 493.88/297.13 MAYBE 493.88/297.13 493.88/297.13 None of the processors succeeded. 493.88/297.13 493.88/297.13 Details of failed attempt(s): 493.88/297.13 ----------------------------- 493.88/297.13 1) 'empty' failed due to the following reason: 493.88/297.13 493.88/297.13 Empty strict component of the problem is NOT empty. 493.88/297.13 493.88/297.13 2) 'With Problem ...' failed due to the following reason: 493.88/297.13 493.88/297.13 None of the processors succeeded. 493.88/297.13 493.88/297.13 Details of failed attempt(s): 493.88/297.13 ----------------------------- 493.88/297.13 1) 'empty' failed due to the following reason: 493.88/297.13 493.88/297.13 Empty strict component of the problem is NOT empty. 493.88/297.13 493.88/297.13 2) 'Fastest' failed due to the following reason: 493.88/297.13 493.88/297.13 None of the processors succeeded. 493.88/297.13 493.88/297.13 Details of failed attempt(s): 493.88/297.13 ----------------------------- 493.88/297.13 1) 'With Problem ...' failed due to the following reason: 493.88/297.13 493.88/297.13 None of the processors succeeded. 493.88/297.13 493.88/297.13 Details of failed attempt(s): 493.88/297.13 ----------------------------- 493.88/297.13 1) 'empty' failed due to the following reason: 493.88/297.13 493.88/297.13 Empty strict component of the problem is NOT empty. 493.88/297.13 493.88/297.13 2) 'With Problem ...' failed due to the following reason: 493.88/297.13 493.88/297.13 The weightgap principle applies (using the following nonconstant 493.88/297.13 growth matrix-interpretation) 493.88/297.13 493.88/297.13 The following argument positions are usable: 493.88/297.13 Uargs(if1) = {1}, Uargs(if2) = {1} 493.88/297.13 493.88/297.13 TcT has computed the following matrix interpretation satisfying 493.88/297.13 not(EDA) and not(IDA(1)). 493.88/297.13 493.88/297.13 [gt](x1, x2) = [0 0] x2 + [0] 493.88/297.13 [0 1] [0] 493.88/297.13 493.88/297.13 [s](x1) = [0] 493.88/297.13 [0] 493.88/297.13 493.88/297.13 [0] = [0] 493.88/297.13 [2] 493.88/297.13 493.88/297.13 [true] = [0] 493.88/297.13 [2] 493.88/297.13 493.88/297.13 [false] = [0] 493.88/297.13 [0] 493.88/297.13 493.88/297.13 [divides](x1, x2) = [0] 493.88/297.13 [4] 493.88/297.13 493.88/297.13 [div](x1, x2, x3) = [0] 493.88/297.13 [4] 493.88/297.13 493.88/297.13 [prime](x1) = [7] 493.88/297.13 [7] 493.88/297.13 493.88/297.13 [test](x1, x2) = [0 1] x2 + [6] 493.88/297.13 [0 0] [4] 493.88/297.13 493.88/297.13 [if1](x1, x2, x3) = [1 1] x1 + [6] 493.88/297.13 [0 0] [4] 493.88/297.13 493.88/297.13 [if2](x1, x2, x3) = [1 0] x1 + [7] 493.88/297.13 [0 0] [4] 493.88/297.13 493.88/297.13 The order satisfies the following ordering constraints: 493.88/297.13 493.88/297.13 [gt(s(x), s(y))] = [0] 493.88/297.13 [0] 493.88/297.13 ? [0 0] y + [0] 493.88/297.13 [0 1] [0] 493.88/297.13 = [gt(x, y)] 493.88/297.13 493.88/297.14 [gt(s(x), 0())] = [0] 493.88/297.14 [2] 493.88/297.14 >= [0] 493.88/297.14 [2] 493.88/297.14 = [true()] 493.88/297.14 493.88/297.14 [gt(0(), y)] = [0 0] y + [0] 493.88/297.14 [0 1] [0] 493.88/297.14 >= [0] 493.88/297.14 [0] 493.88/297.14 = [false()] 493.88/297.14 493.88/297.14 [divides(x, y)] = [0] 493.88/297.14 [4] 493.88/297.14 >= [0] 493.88/297.14 [4] 493.88/297.14 = [div(x, y, y)] 493.88/297.14 493.88/297.14 [div(s(x), s(y), z)] = [0] 493.88/297.14 [4] 493.88/297.14 >= [0] 493.88/297.14 [4] 493.88/297.14 = [div(x, y, z)] 493.88/297.14 493.88/297.14 [div(s(x), 0(), s(z))] = [0] 493.88/297.14 [4] 493.88/297.14 >= [0] 493.88/297.14 [4] 493.88/297.14 = [div(s(x), s(z), s(z))] 493.88/297.14 493.88/297.14 [div(0(), s(x), z)] = [0] 493.88/297.14 [4] 493.88/297.14 >= [0] 493.88/297.14 [0] 493.88/297.14 = [false()] 493.88/297.14 493.88/297.14 [div(0(), 0(), z)] = [0] 493.88/297.14 [4] 493.88/297.14 >= [0] 493.88/297.14 [2] 493.88/297.14 = [true()] 493.88/297.14 493.88/297.14 [prime(x)] = [7] 493.88/297.14 [7] 493.88/297.14 > [6] 493.88/297.14 [4] 493.88/297.14 = [test(x, s(s(0())))] 493.88/297.14 493.88/297.14 [test(x, y)] = [0 1] y + [6] 493.88/297.14 [0 0] [4] 493.88/297.14 >= [0 1] y + [6] 493.88/297.14 [0 0] [4] 493.88/297.14 = [if1(gt(x, y), x, y)] 493.88/297.14 493.88/297.14 [if1(true(), x, y)] = [8] 493.88/297.14 [4] 493.88/297.14 > [7] 493.88/297.14 [4] 493.88/297.14 = [if2(divides(x, y), x, y)] 493.88/297.14 493.88/297.14 [if1(false(), x, y)] = [6] 493.88/297.14 [4] 493.88/297.14 > [0] 493.88/297.14 [2] 493.88/297.14 = [true()] 493.88/297.14 493.88/297.14 [if2(true(), x, y)] = [7] 493.88/297.14 [4] 493.88/297.14 > [0] 493.88/297.14 [0] 493.88/297.14 = [false()] 493.88/297.14 493.88/297.14 [if2(false(), x, y)] = [7] 493.88/297.14 [4] 493.88/297.14 > [6] 493.88/297.14 [4] 493.88/297.14 = [test(x, s(y))] 493.88/297.14 493.88/297.14 493.88/297.14 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 493.88/297.14 493.88/297.14 We are left with following problem, upon which TcT provides the 493.88/297.14 certificate MAYBE. 493.88/297.14 493.88/297.14 Strict Trs: 493.88/297.14 { gt(s(x), s(y)) -> gt(x, y) 493.88/297.14 , div(s(x), s(y), z) -> div(x, y, z) 493.88/297.14 , div(s(x), 0(), s(z)) -> div(s(x), s(z), s(z)) } 493.88/297.14 Weak Trs: 493.88/297.14 { gt(s(x), 0()) -> true() 493.88/297.14 , gt(0(), y) -> false() 493.88/297.14 , divides(x, y) -> div(x, y, y) 493.88/297.14 , div(0(), s(x), z) -> false() 493.88/297.14 , div(0(), 0(), z) -> true() 493.88/297.14 , prime(x) -> test(x, s(s(0()))) 493.88/297.14 , test(x, y) -> if1(gt(x, y), x, y) 493.88/297.14 , if1(true(), x, y) -> if2(divides(x, y), x, y) 493.88/297.14 , if1(false(), x, y) -> true() 493.88/297.14 , if2(true(), x, y) -> false() 493.88/297.14 , if2(false(), x, y) -> test(x, s(y)) } 493.88/297.14 Obligation: 493.88/297.14 innermost runtime complexity 493.88/297.14 Answer: 493.88/297.14 MAYBE 493.88/297.14 493.88/297.14 None of the processors succeeded. 493.88/297.14 493.88/297.14 Details of failed attempt(s): 493.88/297.14 ----------------------------- 493.88/297.14 1) 'empty' failed due to the following reason: 493.88/297.14 493.88/297.14 Empty strict component of the problem is NOT empty. 493.88/297.14 493.88/297.14 2) 'With Problem ...' failed due to the following reason: 493.88/297.14 493.88/297.14 None of the processors succeeded. 493.88/297.14 493.88/297.14 Details of failed attempt(s): 493.88/297.14 ----------------------------- 493.88/297.14 1) 'empty' failed due to the following reason: 493.88/297.14 493.88/297.14 Empty strict component of the problem is NOT empty. 493.88/297.14 493.88/297.14 2) 'With Problem ...' failed due to the following reason: 493.88/297.14 493.88/297.14 Empty strict component of the problem is NOT empty. 493.88/297.14 493.88/297.14 493.88/297.14 493.88/297.14 493.88/297.14 2) 'With Problem ...' failed due to the following reason: 493.88/297.14 493.88/297.14 None of the processors succeeded. 493.88/297.14 493.88/297.14 Details of failed attempt(s): 493.88/297.14 ----------------------------- 493.88/297.14 1) 'empty' failed due to the following reason: 493.88/297.14 493.88/297.14 Empty strict component of the problem is NOT empty. 493.88/297.14 493.88/297.14 2) 'With Problem ...' failed due to the following reason: 493.88/297.14 493.88/297.14 Empty strict component of the problem is NOT empty. 493.88/297.14 493.88/297.14 493.88/297.14 493.88/297.14 493.88/297.14 493.88/297.14 2) 'Best' failed due to the following reason: 493.88/297.14 493.88/297.14 None of the processors succeeded. 493.88/297.14 493.88/297.14 Details of failed attempt(s): 493.88/297.14 ----------------------------- 493.88/297.14 1) 'bsearch-popstar (timeout of 297 seconds)' failed due to the 493.88/297.14 following reason: 493.88/297.14 493.88/297.14 The input cannot be shown compatible 493.88/297.14 493.88/297.14 2) 'Polynomial Path Order (PS) (timeout of 297 seconds)' failed due 493.88/297.14 to the following reason: 493.88/297.14 493.88/297.14 The input cannot be shown compatible 493.88/297.14 493.88/297.14 493.88/297.14 3) 'Fastest (timeout of 24 seconds) (timeout of 297 seconds)' 493.88/297.14 failed due to the following reason: 493.88/297.14 493.88/297.14 None of the processors succeeded. 493.88/297.14 493.88/297.14 Details of failed attempt(s): 493.88/297.14 ----------------------------- 493.88/297.14 1) 'Bounds with minimal-enrichment and initial automaton 'match'' 493.88/297.14 failed due to the following reason: 493.88/297.14 493.88/297.14 match-boundness of the problem could not be verified. 493.88/297.14 493.88/297.14 2) 'Bounds with perSymbol-enrichment and initial automaton 'match'' 493.88/297.14 failed due to the following reason: 493.88/297.14 493.88/297.14 match-boundness of the problem could not be verified. 493.88/297.14 493.88/297.14 493.88/297.14 493.88/297.14 493.88/297.14 493.88/297.14 Arrrr.. 493.88/297.17 EOF