MAYBE 364.50/191.63 MAYBE 364.50/191.63 364.50/191.63 We are left with following problem, upon which TcT provides the 364.50/191.63 certificate MAYBE. 364.50/191.63 364.50/191.63 Strict Trs: 364.50/191.63 { sub(0(), 0()) -> 0() 364.50/191.63 , sub(0(), s(x)) -> 0() 364.50/191.63 , sub(s(x), 0()) -> s(x) 364.50/191.63 , sub(s(x), s(y)) -> sub(x, y) 364.50/191.63 , zero(nil()) -> zero2(0(), nil()) 364.50/191.63 , zero(cons(x, xs)) -> zero2(sub(x, x), cons(x, xs)) 364.50/191.63 , zero2(0(), nil()) -> nil() 364.50/191.63 , zero2(0(), cons(x, xs)) -> cons(sub(x, x), zero(xs)) 364.50/191.63 , zero2(s(y), nil()) -> zero(nil()) 364.50/191.63 , zero2(s(y), cons(x, xs)) -> zero(cons(x, xs)) } 364.50/191.63 Obligation: 364.50/191.63 runtime complexity 364.50/191.63 Answer: 364.50/191.63 MAYBE 364.50/191.63 364.50/191.63 None of the processors succeeded. 364.50/191.63 364.50/191.63 Details of failed attempt(s): 364.50/191.63 ----------------------------- 364.50/191.63 1) 'Best' failed due to the following reason: 364.50/191.63 364.50/191.63 None of the processors succeeded. 364.50/191.63 364.50/191.63 Details of failed attempt(s): 364.50/191.63 ----------------------------- 364.50/191.63 1) 'With Problem ... (timeout of 148 seconds) (timeout of 297 364.50/191.63 seconds)' failed due to the following reason: 364.50/191.63 364.50/191.63 The weightgap principle applies (using the following nonconstant 364.50/191.63 growth matrix-interpretation) 364.50/191.63 364.50/191.63 The following argument positions are usable: 364.50/191.63 Uargs(zero2) = {1}, Uargs(cons) = {1, 2} 364.50/191.63 364.50/191.63 TcT has computed the following matrix interpretation satisfying 364.50/191.63 not(EDA) and not(IDA(1)). 364.50/191.63 364.50/191.63 [sub](x1, x2) = [1] 364.50/191.63 364.50/191.63 [0] = [0] 364.50/191.63 364.50/191.63 [s](x1) = [0] 364.50/191.63 364.50/191.63 [zero](x1) = [0] 364.50/191.63 364.50/191.63 [nil] = [5] 364.50/191.63 364.50/191.63 [zero2](x1, x2) = [1] x1 + [0] 364.50/191.63 364.50/191.63 [cons](x1, x2) = [1] x1 + [1] x2 + [0] 364.50/191.63 364.50/191.63 The order satisfies the following ordering constraints: 364.50/191.63 364.50/191.63 [sub(0(), 0())] = [1] 364.50/191.63 > [0] 364.50/191.63 = [0()] 364.50/191.63 364.50/191.63 [sub(0(), s(x))] = [1] 364.50/191.63 > [0] 364.50/191.63 = [0()] 364.50/191.63 364.50/191.63 [sub(s(x), 0())] = [1] 364.50/191.63 > [0] 364.50/191.63 = [s(x)] 364.50/191.63 364.50/191.63 [sub(s(x), s(y))] = [1] 364.50/191.63 >= [1] 364.50/191.63 = [sub(x, y)] 364.50/191.63 364.50/191.63 [zero(nil())] = [0] 364.50/191.63 >= [0] 364.50/191.63 = [zero2(0(), nil())] 364.50/191.63 364.50/191.63 [zero(cons(x, xs))] = [0] 364.50/191.63 ? [1] 364.50/191.63 = [zero2(sub(x, x), cons(x, xs))] 364.50/191.63 364.50/191.63 [zero2(0(), nil())] = [0] 364.50/191.63 ? [5] 364.50/191.63 = [nil()] 364.50/191.63 364.50/191.63 [zero2(0(), cons(x, xs))] = [0] 364.50/191.63 ? [1] 364.50/191.63 = [cons(sub(x, x), zero(xs))] 364.50/191.63 364.50/191.63 [zero2(s(y), nil())] = [0] 364.50/191.63 >= [0] 364.50/191.63 = [zero(nil())] 364.50/191.63 364.50/191.63 [zero2(s(y), cons(x, xs))] = [0] 364.50/191.63 >= [0] 364.50/191.63 = [zero(cons(x, xs))] 364.50/191.63 364.50/191.63 364.50/191.63 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 364.50/191.63 364.50/191.63 We are left with following problem, upon which TcT provides the 364.50/191.63 certificate MAYBE. 364.50/191.63 364.50/191.63 Strict Trs: 364.50/191.63 { sub(s(x), s(y)) -> sub(x, y) 364.50/191.63 , zero(nil()) -> zero2(0(), nil()) 364.50/191.63 , zero(cons(x, xs)) -> zero2(sub(x, x), cons(x, xs)) 364.50/191.63 , zero2(0(), nil()) -> nil() 364.50/191.63 , zero2(0(), cons(x, xs)) -> cons(sub(x, x), zero(xs)) 364.50/191.63 , zero2(s(y), nil()) -> zero(nil()) 364.50/191.63 , zero2(s(y), cons(x, xs)) -> zero(cons(x, xs)) } 364.50/191.63 Weak Trs: 364.50/191.63 { sub(0(), 0()) -> 0() 364.50/191.63 , sub(0(), s(x)) -> 0() 364.50/191.63 , sub(s(x), 0()) -> s(x) } 364.50/191.63 Obligation: 364.50/191.63 runtime complexity 364.50/191.63 Answer: 364.50/191.63 MAYBE 364.50/191.63 364.50/191.63 The weightgap principle applies (using the following nonconstant 364.50/191.63 growth matrix-interpretation) 364.50/191.63 364.50/191.63 The following argument positions are usable: 364.50/191.63 Uargs(zero2) = {1}, Uargs(cons) = {1, 2} 364.50/191.63 364.50/191.63 TcT has computed the following matrix interpretation satisfying 364.50/191.63 not(EDA) and not(IDA(1)). 364.50/191.63 364.50/191.63 [sub](x1, x2) = [4] 364.50/191.63 364.50/191.63 [0] = [1] 364.50/191.63 364.50/191.63 [s](x1) = [0] 364.50/191.63 364.50/191.63 [zero](x1) = [0] 364.50/191.63 364.50/191.63 [nil] = [0] 364.50/191.63 364.50/191.63 [zero2](x1, x2) = [1] x1 + [0] 364.50/191.63 364.50/191.63 [cons](x1, x2) = [1] x1 + [1] x2 + [0] 364.50/191.63 364.50/191.63 The order satisfies the following ordering constraints: 364.50/191.63 364.50/191.63 [sub(0(), 0())] = [4] 364.50/191.63 > [1] 364.50/191.63 = [0()] 364.50/191.63 364.50/191.63 [sub(0(), s(x))] = [4] 364.50/191.63 > [1] 364.50/191.63 = [0()] 364.50/191.63 364.50/191.63 [sub(s(x), 0())] = [4] 364.50/191.63 > [0] 364.50/191.63 = [s(x)] 364.50/191.63 364.50/191.63 [sub(s(x), s(y))] = [4] 364.50/191.63 >= [4] 364.50/191.63 = [sub(x, y)] 364.50/191.63 364.50/191.63 [zero(nil())] = [0] 364.50/191.63 ? [1] 364.50/191.63 = [zero2(0(), nil())] 364.50/191.63 364.50/191.63 [zero(cons(x, xs))] = [0] 364.50/191.63 ? [4] 364.50/191.63 = [zero2(sub(x, x), cons(x, xs))] 364.50/191.63 364.50/191.63 [zero2(0(), nil())] = [1] 364.50/191.63 > [0] 364.50/191.63 = [nil()] 364.50/191.63 364.50/191.63 [zero2(0(), cons(x, xs))] = [1] 364.50/191.63 ? [4] 364.50/191.63 = [cons(sub(x, x), zero(xs))] 364.50/191.63 364.50/191.63 [zero2(s(y), nil())] = [0] 364.50/191.63 >= [0] 364.50/191.63 = [zero(nil())] 364.50/191.63 364.50/191.63 [zero2(s(y), cons(x, xs))] = [0] 364.50/191.63 >= [0] 364.50/191.63 = [zero(cons(x, xs))] 364.50/191.63 364.50/191.63 364.50/191.63 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 364.50/191.63 364.50/191.63 We are left with following problem, upon which TcT provides the 364.50/191.63 certificate MAYBE. 364.50/191.63 364.50/191.63 Strict Trs: 364.50/191.63 { sub(s(x), s(y)) -> sub(x, y) 364.50/191.63 , zero(nil()) -> zero2(0(), nil()) 364.50/191.63 , zero(cons(x, xs)) -> zero2(sub(x, x), cons(x, xs)) 364.50/191.63 , zero2(0(), cons(x, xs)) -> cons(sub(x, x), zero(xs)) 364.50/191.63 , zero2(s(y), nil()) -> zero(nil()) 364.50/191.63 , zero2(s(y), cons(x, xs)) -> zero(cons(x, xs)) } 364.50/191.63 Weak Trs: 364.50/191.63 { sub(0(), 0()) -> 0() 364.50/191.63 , sub(0(), s(x)) -> 0() 364.50/191.63 , sub(s(x), 0()) -> s(x) 364.50/191.63 , zero2(0(), nil()) -> nil() } 364.50/191.63 Obligation: 364.50/191.63 runtime complexity 364.50/191.63 Answer: 364.50/191.63 MAYBE 364.50/191.63 364.50/191.63 The weightgap principle applies (using the following nonconstant 364.50/191.63 growth matrix-interpretation) 364.50/191.63 364.50/191.63 The following argument positions are usable: 364.50/191.63 Uargs(zero2) = {1}, Uargs(cons) = {1, 2} 364.50/191.63 364.50/191.63 TcT has computed the following matrix interpretation satisfying 364.50/191.63 not(EDA) and not(IDA(1)). 364.50/191.63 364.50/191.63 [sub](x1, x2) = [1] 364.50/191.63 364.50/191.63 [0] = [0] 364.50/191.63 364.50/191.63 [s](x1) = [1] 364.50/191.63 364.50/191.63 [zero](x1) = [0] 364.50/191.63 364.50/191.63 [nil] = [0] 364.50/191.63 364.50/191.63 [zero2](x1, x2) = [1] x1 + [0] 364.50/191.63 364.50/191.63 [cons](x1, x2) = [1] x1 + [1] x2 + [0] 364.50/191.63 364.50/191.63 The order satisfies the following ordering constraints: 364.50/191.63 364.50/191.63 [sub(0(), 0())] = [1] 364.50/191.63 > [0] 364.50/191.63 = [0()] 364.50/191.63 364.50/191.63 [sub(0(), s(x))] = [1] 364.50/191.63 > [0] 364.50/191.63 = [0()] 364.50/191.63 364.50/191.63 [sub(s(x), 0())] = [1] 364.50/191.63 >= [1] 364.50/191.63 = [s(x)] 364.50/191.63 364.50/191.63 [sub(s(x), s(y))] = [1] 364.50/191.63 >= [1] 364.50/191.63 = [sub(x, y)] 364.50/191.63 364.50/191.63 [zero(nil())] = [0] 364.50/191.63 >= [0] 364.50/191.63 = [zero2(0(), nil())] 364.50/191.63 364.50/191.63 [zero(cons(x, xs))] = [0] 364.50/191.63 ? [1] 364.50/191.63 = [zero2(sub(x, x), cons(x, xs))] 364.50/191.63 364.50/191.63 [zero2(0(), nil())] = [0] 364.50/191.63 >= [0] 364.50/191.63 = [nil()] 364.50/191.63 364.50/191.63 [zero2(0(), cons(x, xs))] = [0] 364.50/191.63 ? [1] 364.50/191.63 = [cons(sub(x, x), zero(xs))] 364.50/191.63 364.50/191.63 [zero2(s(y), nil())] = [1] 364.50/191.63 > [0] 364.50/191.63 = [zero(nil())] 364.50/191.63 364.50/191.63 [zero2(s(y), cons(x, xs))] = [1] 364.50/191.63 > [0] 364.50/191.63 = [zero(cons(x, xs))] 364.50/191.63 364.50/191.63 364.50/191.63 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 364.50/191.63 364.50/191.63 We are left with following problem, upon which TcT provides the 364.50/191.63 certificate MAYBE. 364.50/191.63 364.50/191.63 Strict Trs: 364.50/191.63 { sub(s(x), s(y)) -> sub(x, y) 364.50/191.63 , zero(nil()) -> zero2(0(), nil()) 364.50/191.63 , zero(cons(x, xs)) -> zero2(sub(x, x), cons(x, xs)) 364.50/191.63 , zero2(0(), cons(x, xs)) -> cons(sub(x, x), zero(xs)) } 364.50/191.63 Weak Trs: 364.50/191.63 { sub(0(), 0()) -> 0() 364.50/191.63 , sub(0(), s(x)) -> 0() 364.50/191.63 , sub(s(x), 0()) -> s(x) 364.50/191.63 , zero2(0(), nil()) -> nil() 364.50/191.63 , zero2(s(y), nil()) -> zero(nil()) 364.50/191.63 , zero2(s(y), cons(x, xs)) -> zero(cons(x, xs)) } 364.50/191.63 Obligation: 364.50/191.63 runtime complexity 364.50/191.63 Answer: 364.50/191.63 MAYBE 364.50/191.63 364.50/191.63 The weightgap principle applies (using the following nonconstant 364.50/191.63 growth matrix-interpretation) 364.50/191.63 364.50/191.63 The following argument positions are usable: 364.50/191.63 Uargs(zero2) = {1}, Uargs(cons) = {1, 2} 364.50/191.63 364.50/191.63 TcT has computed the following matrix interpretation satisfying 364.50/191.63 not(EDA) and not(IDA(1)). 364.50/191.63 364.50/191.63 [sub](x1, x2) = [0] 364.50/191.63 364.50/191.63 [0] = [0] 364.50/191.63 364.50/191.63 [s](x1) = [0] 364.50/191.63 364.50/191.63 [zero](x1) = [0] 364.50/191.63 364.50/191.63 [nil] = [1] 364.50/191.63 364.50/191.63 [zero2](x1, x2) = [1] x1 + [1] 364.50/191.63 364.50/191.63 [cons](x1, x2) = [1] x1 + [1] x2 + [0] 364.50/191.63 364.50/191.63 The order satisfies the following ordering constraints: 364.50/191.63 364.50/191.63 [sub(0(), 0())] = [0] 364.50/191.63 >= [0] 364.50/191.63 = [0()] 364.50/191.63 364.50/191.63 [sub(0(), s(x))] = [0] 364.50/191.63 >= [0] 364.50/191.63 = [0()] 364.50/191.63 364.50/191.63 [sub(s(x), 0())] = [0] 364.50/191.63 >= [0] 364.50/191.63 = [s(x)] 364.50/191.63 364.50/191.63 [sub(s(x), s(y))] = [0] 364.50/191.63 >= [0] 364.50/191.63 = [sub(x, y)] 364.50/191.63 364.50/191.63 [zero(nil())] = [0] 364.50/191.63 ? [1] 364.50/191.63 = [zero2(0(), nil())] 364.50/191.63 364.50/191.63 [zero(cons(x, xs))] = [0] 364.50/191.63 ? [1] 364.50/191.63 = [zero2(sub(x, x), cons(x, xs))] 364.50/191.63 364.50/191.63 [zero2(0(), nil())] = [1] 364.50/191.63 >= [1] 364.50/191.63 = [nil()] 364.50/191.63 364.50/191.63 [zero2(0(), cons(x, xs))] = [1] 364.50/191.63 > [0] 364.50/191.63 = [cons(sub(x, x), zero(xs))] 364.50/191.63 364.50/191.63 [zero2(s(y), nil())] = [1] 364.50/191.63 > [0] 364.50/191.63 = [zero(nil())] 364.50/191.63 364.50/191.63 [zero2(s(y), cons(x, xs))] = [1] 364.50/191.63 > [0] 364.50/191.63 = [zero(cons(x, xs))] 364.50/191.63 364.50/191.63 364.50/191.63 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 364.50/191.63 364.50/191.63 We are left with following problem, upon which TcT provides the 364.50/191.63 certificate MAYBE. 364.50/191.63 364.50/191.63 Strict Trs: 364.50/191.63 { sub(s(x), s(y)) -> sub(x, y) 364.50/191.63 , zero(nil()) -> zero2(0(), nil()) 364.50/191.63 , zero(cons(x, xs)) -> zero2(sub(x, x), cons(x, xs)) } 364.50/191.63 Weak Trs: 364.50/191.63 { sub(0(), 0()) -> 0() 364.50/191.63 , sub(0(), s(x)) -> 0() 364.50/191.63 , sub(s(x), 0()) -> s(x) 364.50/191.63 , zero2(0(), nil()) -> nil() 364.50/191.63 , zero2(0(), cons(x, xs)) -> cons(sub(x, x), zero(xs)) 364.50/191.63 , zero2(s(y), nil()) -> zero(nil()) 364.50/191.63 , zero2(s(y), cons(x, xs)) -> zero(cons(x, xs)) } 364.50/191.63 Obligation: 364.50/191.63 runtime complexity 364.50/191.63 Answer: 364.50/191.63 MAYBE 364.50/191.63 364.50/191.63 We use the processor 'matrix interpretation of dimension 1' to 364.50/191.63 orient following rules strictly. 364.50/191.63 364.50/191.63 Trs: { zero(nil()) -> zero2(0(), nil()) } 364.50/191.63 364.50/191.63 The induced complexity on above rules (modulo remaining rules) is 364.50/191.63 YES(?,O(n^1)) . These rules are moved into the corresponding weak 364.50/191.63 component(s). 364.50/191.63 364.50/191.63 Sub-proof: 364.50/191.63 ---------- 364.50/191.63 The following argument positions are usable: 364.50/191.63 Uargs(zero2) = {1}, Uargs(cons) = {1, 2} 364.50/191.63 364.50/191.63 TcT has computed the following constructor-based matrix 364.50/191.63 interpretation satisfying not(EDA). 364.50/191.63 364.50/191.63 [sub](x1, x2) = [1] 364.50/191.63 364.50/191.63 [0] = [0] 364.50/191.63 364.50/191.63 [s](x1) = [1] 364.50/191.63 364.50/191.63 [zero](x1) = [2] x1 + [4] 364.50/191.63 364.50/191.63 [nil] = [0] 364.50/191.63 364.50/191.63 [zero2](x1, x2) = [2] x1 + [2] x2 + [2] 364.50/191.63 364.50/191.63 [cons](x1, x2) = [1] x1 + [1] x2 + [4] 364.50/191.63 364.50/191.63 The order satisfies the following ordering constraints: 364.50/191.63 364.50/191.63 [sub(0(), 0())] = [1] 364.50/191.63 > [0] 364.50/191.63 = [0()] 364.50/191.63 364.50/191.63 [sub(0(), s(x))] = [1] 364.50/191.63 > [0] 364.50/191.63 = [0()] 364.50/191.63 364.50/191.63 [sub(s(x), 0())] = [1] 364.50/191.63 >= [1] 364.50/191.63 = [s(x)] 364.50/191.63 364.50/191.63 [sub(s(x), s(y))] = [1] 364.50/191.63 >= [1] 364.50/191.63 = [sub(x, y)] 364.50/191.63 364.50/191.63 [zero(nil())] = [4] 364.50/191.63 > [2] 364.50/191.63 = [zero2(0(), nil())] 364.50/191.63 364.50/191.63 [zero(cons(x, xs))] = [2] x + [2] xs + [12] 364.50/191.63 >= [2] x + [2] xs + [12] 364.50/191.63 = [zero2(sub(x, x), cons(x, xs))] 364.50/191.63 364.50/191.63 [zero2(0(), nil())] = [2] 364.50/191.63 > [0] 364.50/191.63 = [nil()] 364.50/191.63 364.50/191.63 [zero2(0(), cons(x, xs))] = [2] x + [2] xs + [10] 364.50/191.63 > [2] xs + [9] 364.50/191.63 = [cons(sub(x, x), zero(xs))] 364.50/191.63 364.50/191.63 [zero2(s(y), nil())] = [4] 364.50/191.63 >= [4] 364.50/191.63 = [zero(nil())] 364.50/191.63 364.50/191.63 [zero2(s(y), cons(x, xs))] = [2] x + [2] xs + [12] 364.50/191.63 >= [2] x + [2] xs + [12] 364.50/191.63 = [zero(cons(x, xs))] 364.50/191.63 364.50/191.63 364.50/191.63 We return to the main proof. 364.50/191.63 364.50/191.63 We are left with following problem, upon which TcT provides the 364.50/191.63 certificate MAYBE. 364.50/191.63 364.50/191.63 Strict Trs: 364.50/191.63 { sub(s(x), s(y)) -> sub(x, y) 364.50/191.63 , zero(cons(x, xs)) -> zero2(sub(x, x), cons(x, xs)) } 364.50/191.63 Weak Trs: 364.50/191.63 { sub(0(), 0()) -> 0() 364.50/191.63 , sub(0(), s(x)) -> 0() 364.50/191.63 , sub(s(x), 0()) -> s(x) 364.50/191.63 , zero(nil()) -> zero2(0(), nil()) 364.50/191.63 , zero2(0(), nil()) -> nil() 364.50/191.63 , zero2(0(), cons(x, xs)) -> cons(sub(x, x), zero(xs)) 364.50/191.63 , zero2(s(y), nil()) -> zero(nil()) 364.50/191.63 , zero2(s(y), cons(x, xs)) -> zero(cons(x, xs)) } 364.50/191.63 Obligation: 364.50/191.63 runtime complexity 364.50/191.63 Answer: 364.50/191.63 MAYBE 364.50/191.63 364.50/191.63 None of the processors succeeded. 364.50/191.63 364.50/191.63 Details of failed attempt(s): 364.50/191.63 ----------------------------- 364.50/191.63 1) 'empty' failed due to the following reason: 364.50/191.63 364.50/191.63 Empty strict component of the problem is NOT empty. 364.50/191.63 364.50/191.63 2) 'With Problem ...' failed due to the following reason: 364.50/191.63 364.50/191.63 None of the processors succeeded. 364.50/191.63 364.50/191.63 Details of failed attempt(s): 364.50/191.63 ----------------------------- 364.50/191.63 1) 'empty' failed due to the following reason: 364.50/191.63 364.50/191.63 Empty strict component of the problem is NOT empty. 364.50/191.63 364.50/191.63 2) 'Fastest' failed due to the following reason: 364.50/191.63 364.50/191.63 None of the processors succeeded. 364.50/191.63 364.50/191.63 Details of failed attempt(s): 364.50/191.63 ----------------------------- 364.50/191.63 1) 'With Problem ...' failed due to the following reason: 364.50/191.63 364.50/191.63 None of the processors succeeded. 364.50/191.63 364.50/191.63 Details of failed attempt(s): 364.50/191.63 ----------------------------- 364.50/191.63 1) 'empty' failed due to the following reason: 364.50/191.63 364.50/191.63 Empty strict component of the problem is NOT empty. 364.50/191.63 364.50/191.63 2) 'With Problem ...' failed due to the following reason: 364.50/191.63 364.50/191.63 None of the processors succeeded. 364.50/191.63 364.50/191.63 Details of failed attempt(s): 364.50/191.63 ----------------------------- 364.50/191.63 1) 'empty' failed due to the following reason: 364.50/191.63 364.50/191.63 Empty strict component of the problem is NOT empty. 364.50/191.63 364.50/191.63 2) 'With Problem ...' failed due to the following reason: 364.50/191.63 364.50/191.63 None of the processors succeeded. 364.50/191.63 364.50/191.63 Details of failed attempt(s): 364.50/191.63 ----------------------------- 364.50/191.63 1) 'empty' failed due to the following reason: 364.50/191.63 364.50/191.63 Empty strict component of the problem is NOT empty. 364.50/191.63 364.50/191.63 2) 'With Problem ...' failed due to the following reason: 364.50/191.63 364.50/191.63 Empty strict component of the problem is NOT empty. 364.50/191.63 364.50/191.63 364.50/191.63 364.50/191.63 364.50/191.63 2) 'With Problem ...' failed due to the following reason: 364.50/191.63 364.50/191.63 None of the processors succeeded. 364.50/191.63 364.50/191.63 Details of failed attempt(s): 364.50/191.63 ----------------------------- 364.50/191.63 1) 'empty' failed due to the following reason: 364.50/191.63 364.50/191.63 Empty strict component of the problem is NOT empty. 364.50/191.63 364.50/191.63 2) 'With Problem ...' failed due to the following reason: 364.50/191.63 364.50/191.63 Empty strict component of the problem is NOT empty. 364.50/191.63 364.50/191.63 364.50/191.63 364.50/191.63 364.50/191.63 364.50/191.63 2) 'Best' failed due to the following reason: 364.50/191.63 364.50/191.63 None of the processors succeeded. 364.50/191.63 364.50/191.63 Details of failed attempt(s): 364.50/191.63 ----------------------------- 364.50/191.63 1) 'bsearch-popstar (timeout of 297 seconds)' failed due to the 364.50/191.63 following reason: 364.50/191.63 364.50/191.63 The processor is inapplicable, reason: 364.50/191.63 Processor only applicable for innermost runtime complexity analysis 364.50/191.63 364.50/191.63 2) 'Polynomial Path Order (PS) (timeout of 297 seconds)' failed due 364.50/191.63 to the following reason: 364.50/191.63 364.50/191.63 The processor is inapplicable, reason: 364.50/191.63 Processor only applicable for innermost runtime complexity analysis 364.50/191.63 364.50/191.63 364.50/191.63 3) 'Fastest (timeout of 24 seconds) (timeout of 297 seconds)' 364.50/191.63 failed due to the following reason: 364.50/191.63 364.50/191.63 None of the processors succeeded. 364.50/191.63 364.50/191.63 Details of failed attempt(s): 364.50/191.63 ----------------------------- 364.50/191.63 1) 'Bounds with perSymbol-enrichment and initial automaton 'match'' 364.50/191.63 failed due to the following reason: 364.50/191.63 364.50/191.63 match-boundness of the problem could not be verified. 364.50/191.63 364.50/191.63 2) 'Bounds with minimal-enrichment and initial automaton 'match'' 364.50/191.63 failed due to the following reason: 364.50/191.63 364.50/191.63 match-boundness of the problem could not be verified. 364.50/191.63 364.50/191.63 364.50/191.63 364.50/191.63 2) 'Weak Dependency Pairs (timeout of 297 seconds)' failed due to 364.50/191.63 the following reason: 364.50/191.63 364.50/191.63 We add the following weak dependency pairs: 364.50/191.63 364.50/191.63 Strict DPs: 364.50/191.63 { sub^#(0(), 0()) -> c_1() 364.50/191.63 , sub^#(0(), s(x)) -> c_2() 364.50/191.63 , sub^#(s(x), 0()) -> c_3(x) 364.50/191.63 , sub^#(s(x), s(y)) -> c_4(sub^#(x, y)) 364.50/191.63 , zero^#(nil()) -> c_5(zero2^#(0(), nil())) 364.50/191.63 , zero^#(cons(x, xs)) -> c_6(zero2^#(sub(x, x), cons(x, xs))) 364.50/191.63 , zero2^#(0(), nil()) -> c_7() 364.50/191.63 , zero2^#(0(), cons(x, xs)) -> c_8(sub^#(x, x), zero^#(xs)) 364.50/191.63 , zero2^#(s(y), nil()) -> c_9(zero^#(nil())) 364.50/191.63 , zero2^#(s(y), cons(x, xs)) -> c_10(zero^#(cons(x, xs))) } 364.50/191.63 364.50/191.63 and mark the set of starting terms. 364.50/191.63 364.50/191.63 We are left with following problem, upon which TcT provides the 364.50/191.63 certificate MAYBE. 364.50/191.63 364.50/191.63 Strict DPs: 364.50/191.63 { sub^#(0(), 0()) -> c_1() 364.50/191.63 , sub^#(0(), s(x)) -> c_2() 364.50/191.63 , sub^#(s(x), 0()) -> c_3(x) 364.50/191.63 , sub^#(s(x), s(y)) -> c_4(sub^#(x, y)) 364.50/191.63 , zero^#(nil()) -> c_5(zero2^#(0(), nil())) 364.50/191.63 , zero^#(cons(x, xs)) -> c_6(zero2^#(sub(x, x), cons(x, xs))) 364.50/191.63 , zero2^#(0(), nil()) -> c_7() 364.50/191.63 , zero2^#(0(), cons(x, xs)) -> c_8(sub^#(x, x), zero^#(xs)) 364.50/191.63 , zero2^#(s(y), nil()) -> c_9(zero^#(nil())) 364.50/191.63 , zero2^#(s(y), cons(x, xs)) -> c_10(zero^#(cons(x, xs))) } 364.50/191.63 Strict Trs: 364.50/191.63 { sub(0(), 0()) -> 0() 364.50/191.63 , sub(0(), s(x)) -> 0() 364.50/191.63 , sub(s(x), 0()) -> s(x) 364.50/191.63 , sub(s(x), s(y)) -> sub(x, y) 364.50/191.63 , zero(nil()) -> zero2(0(), nil()) 364.50/191.63 , zero(cons(x, xs)) -> zero2(sub(x, x), cons(x, xs)) 364.50/191.63 , zero2(0(), nil()) -> nil() 364.50/191.63 , zero2(0(), cons(x, xs)) -> cons(sub(x, x), zero(xs)) 364.50/191.63 , zero2(s(y), nil()) -> zero(nil()) 364.50/191.63 , zero2(s(y), cons(x, xs)) -> zero(cons(x, xs)) } 364.50/191.63 Obligation: 364.50/191.63 runtime complexity 364.50/191.63 Answer: 364.50/191.63 MAYBE 364.50/191.63 364.50/191.63 We estimate the number of application of {1,2,7} by applications of 364.50/191.63 Pre({1,2,7}) = {3,4,5,8}. Here rules are labeled as follows: 364.50/191.63 364.50/191.63 DPs: 364.50/191.63 { 1: sub^#(0(), 0()) -> c_1() 364.50/191.63 , 2: sub^#(0(), s(x)) -> c_2() 364.50/191.63 , 3: sub^#(s(x), 0()) -> c_3(x) 364.50/191.63 , 4: sub^#(s(x), s(y)) -> c_4(sub^#(x, y)) 364.50/191.63 , 5: zero^#(nil()) -> c_5(zero2^#(0(), nil())) 364.50/191.63 , 6: zero^#(cons(x, xs)) -> c_6(zero2^#(sub(x, x), cons(x, xs))) 364.50/191.63 , 7: zero2^#(0(), nil()) -> c_7() 364.50/191.63 , 8: zero2^#(0(), cons(x, xs)) -> c_8(sub^#(x, x), zero^#(xs)) 364.50/191.63 , 9: zero2^#(s(y), nil()) -> c_9(zero^#(nil())) 364.50/191.63 , 10: zero2^#(s(y), cons(x, xs)) -> c_10(zero^#(cons(x, xs))) } 364.50/191.63 364.50/191.63 We are left with following problem, upon which TcT provides the 364.50/191.63 certificate MAYBE. 364.50/191.63 364.50/191.63 Strict DPs: 364.50/191.63 { sub^#(s(x), 0()) -> c_3(x) 364.50/191.63 , sub^#(s(x), s(y)) -> c_4(sub^#(x, y)) 364.50/191.63 , zero^#(nil()) -> c_5(zero2^#(0(), nil())) 364.50/191.63 , zero^#(cons(x, xs)) -> c_6(zero2^#(sub(x, x), cons(x, xs))) 364.50/191.63 , zero2^#(0(), cons(x, xs)) -> c_8(sub^#(x, x), zero^#(xs)) 364.50/191.63 , zero2^#(s(y), nil()) -> c_9(zero^#(nil())) 364.50/191.63 , zero2^#(s(y), cons(x, xs)) -> c_10(zero^#(cons(x, xs))) } 364.50/191.63 Strict Trs: 364.50/191.63 { sub(0(), 0()) -> 0() 364.50/191.63 , sub(0(), s(x)) -> 0() 364.50/191.63 , sub(s(x), 0()) -> s(x) 364.50/191.63 , sub(s(x), s(y)) -> sub(x, y) 364.50/191.63 , zero(nil()) -> zero2(0(), nil()) 364.50/191.63 , zero(cons(x, xs)) -> zero2(sub(x, x), cons(x, xs)) 364.50/191.63 , zero2(0(), nil()) -> nil() 364.50/191.63 , zero2(0(), cons(x, xs)) -> cons(sub(x, x), zero(xs)) 364.50/191.63 , zero2(s(y), nil()) -> zero(nil()) 364.50/191.63 , zero2(s(y), cons(x, xs)) -> zero(cons(x, xs)) } 364.50/191.63 Weak DPs: 364.50/191.63 { sub^#(0(), 0()) -> c_1() 364.50/191.63 , sub^#(0(), s(x)) -> c_2() 364.50/191.63 , zero2^#(0(), nil()) -> c_7() } 364.50/191.63 Obligation: 364.50/191.63 runtime complexity 364.50/191.63 Answer: 364.50/191.63 MAYBE 364.50/191.63 364.50/191.63 We estimate the number of application of {3} by applications of 364.50/191.63 Pre({3}) = {1,5,6}. Here rules are labeled as follows: 364.50/191.63 364.50/191.63 DPs: 364.50/191.63 { 1: sub^#(s(x), 0()) -> c_3(x) 364.50/191.63 , 2: sub^#(s(x), s(y)) -> c_4(sub^#(x, y)) 364.50/191.63 , 3: zero^#(nil()) -> c_5(zero2^#(0(), nil())) 364.50/191.63 , 4: zero^#(cons(x, xs)) -> c_6(zero2^#(sub(x, x), cons(x, xs))) 364.50/191.64 , 5: zero2^#(0(), cons(x, xs)) -> c_8(sub^#(x, x), zero^#(xs)) 364.50/191.64 , 6: zero2^#(s(y), nil()) -> c_9(zero^#(nil())) 364.50/191.64 , 7: zero2^#(s(y), cons(x, xs)) -> c_10(zero^#(cons(x, xs))) 364.50/191.64 , 8: sub^#(0(), 0()) -> c_1() 364.50/191.64 , 9: sub^#(0(), s(x)) -> c_2() 364.50/191.64 , 10: zero2^#(0(), nil()) -> c_7() } 364.50/191.64 364.50/191.64 We are left with following problem, upon which TcT provides the 364.50/191.64 certificate MAYBE. 364.50/191.64 364.50/191.64 Strict DPs: 364.50/191.64 { sub^#(s(x), 0()) -> c_3(x) 364.50/191.64 , sub^#(s(x), s(y)) -> c_4(sub^#(x, y)) 364.50/191.64 , zero^#(cons(x, xs)) -> c_6(zero2^#(sub(x, x), cons(x, xs))) 364.50/191.64 , zero2^#(0(), cons(x, xs)) -> c_8(sub^#(x, x), zero^#(xs)) 364.50/191.64 , zero2^#(s(y), nil()) -> c_9(zero^#(nil())) 364.50/191.64 , zero2^#(s(y), cons(x, xs)) -> c_10(zero^#(cons(x, xs))) } 364.50/191.64 Strict Trs: 364.50/191.64 { sub(0(), 0()) -> 0() 364.50/191.64 , sub(0(), s(x)) -> 0() 364.50/191.64 , sub(s(x), 0()) -> s(x) 364.50/191.64 , sub(s(x), s(y)) -> sub(x, y) 364.50/191.64 , zero(nil()) -> zero2(0(), nil()) 364.50/191.64 , zero(cons(x, xs)) -> zero2(sub(x, x), cons(x, xs)) 364.50/191.64 , zero2(0(), nil()) -> nil() 364.50/191.64 , zero2(0(), cons(x, xs)) -> cons(sub(x, x), zero(xs)) 364.50/191.64 , zero2(s(y), nil()) -> zero(nil()) 364.50/191.64 , zero2(s(y), cons(x, xs)) -> zero(cons(x, xs)) } 364.50/191.64 Weak DPs: 364.50/191.64 { sub^#(0(), 0()) -> c_1() 364.50/191.64 , sub^#(0(), s(x)) -> c_2() 364.50/191.64 , zero^#(nil()) -> c_5(zero2^#(0(), nil())) 364.50/191.64 , zero2^#(0(), nil()) -> c_7() } 364.50/191.64 Obligation: 364.50/191.64 runtime complexity 364.50/191.64 Answer: 364.50/191.64 MAYBE 364.50/191.64 364.50/191.64 We estimate the number of application of {5} by applications of 364.50/191.64 Pre({5}) = {1}. Here rules are labeled as follows: 364.50/191.64 364.50/191.64 DPs: 364.50/191.64 { 1: sub^#(s(x), 0()) -> c_3(x) 364.50/191.64 , 2: sub^#(s(x), s(y)) -> c_4(sub^#(x, y)) 364.50/191.64 , 3: zero^#(cons(x, xs)) -> c_6(zero2^#(sub(x, x), cons(x, xs))) 364.50/191.64 , 4: zero2^#(0(), cons(x, xs)) -> c_8(sub^#(x, x), zero^#(xs)) 364.50/191.64 , 5: zero2^#(s(y), nil()) -> c_9(zero^#(nil())) 364.50/191.64 , 6: zero2^#(s(y), cons(x, xs)) -> c_10(zero^#(cons(x, xs))) 364.50/191.64 , 7: sub^#(0(), 0()) -> c_1() 364.50/191.64 , 8: sub^#(0(), s(x)) -> c_2() 364.50/191.64 , 9: zero^#(nil()) -> c_5(zero2^#(0(), nil())) 364.50/191.64 , 10: zero2^#(0(), nil()) -> c_7() } 364.50/191.64 364.50/191.64 We are left with following problem, upon which TcT provides the 364.50/191.64 certificate MAYBE. 364.50/191.64 364.50/191.64 Strict DPs: 364.50/191.64 { sub^#(s(x), 0()) -> c_3(x) 364.50/191.64 , sub^#(s(x), s(y)) -> c_4(sub^#(x, y)) 364.50/191.64 , zero^#(cons(x, xs)) -> c_6(zero2^#(sub(x, x), cons(x, xs))) 364.50/191.64 , zero2^#(0(), cons(x, xs)) -> c_8(sub^#(x, x), zero^#(xs)) 364.50/191.64 , zero2^#(s(y), cons(x, xs)) -> c_10(zero^#(cons(x, xs))) } 364.50/191.64 Strict Trs: 364.50/191.64 { sub(0(), 0()) -> 0() 364.50/191.64 , sub(0(), s(x)) -> 0() 364.50/191.64 , sub(s(x), 0()) -> s(x) 364.50/191.64 , sub(s(x), s(y)) -> sub(x, y) 364.50/191.64 , zero(nil()) -> zero2(0(), nil()) 364.50/191.64 , zero(cons(x, xs)) -> zero2(sub(x, x), cons(x, xs)) 364.50/191.64 , zero2(0(), nil()) -> nil() 364.50/191.64 , zero2(0(), cons(x, xs)) -> cons(sub(x, x), zero(xs)) 364.50/191.64 , zero2(s(y), nil()) -> zero(nil()) 364.50/191.64 , zero2(s(y), cons(x, xs)) -> zero(cons(x, xs)) } 364.50/191.64 Weak DPs: 364.50/191.64 { sub^#(0(), 0()) -> c_1() 364.50/191.64 , sub^#(0(), s(x)) -> c_2() 364.50/191.64 , zero^#(nil()) -> c_5(zero2^#(0(), nil())) 364.50/191.64 , zero2^#(0(), nil()) -> c_7() 364.50/191.64 , zero2^#(s(y), nil()) -> c_9(zero^#(nil())) } 364.50/191.64 Obligation: 364.50/191.64 runtime complexity 364.50/191.64 Answer: 364.50/191.64 MAYBE 364.50/191.64 364.50/191.64 Empty strict component of the problem is NOT empty. 364.50/191.64 364.50/191.64 364.50/191.64 Arrrr.. 364.72/191.86 EOF