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