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