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