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