MAYBE 428.60/297.08 MAYBE 428.60/297.08 428.60/297.08 We are left with following problem, upon which TcT provides the 428.60/297.08 certificate MAYBE. 428.60/297.08 428.60/297.08 Strict Trs: 428.60/297.08 { sub(0(), 0()) -> 0() 428.60/297.08 , sub(0(), s(x)) -> 0() 428.60/297.08 , sub(s(x), 0()) -> s(x) 428.60/297.08 , sub(s(x), s(y)) -> sub(x, y) 428.60/297.08 , zero(nil()) -> zero2(0(), nil()) 428.60/297.08 , zero(cons(x, xs)) -> zero2(sub(x, x), cons(x, xs)) 428.60/297.08 , zero2(0(), nil()) -> nil() 428.60/297.08 , zero2(0(), cons(x, xs)) -> cons(sub(x, x), zero(xs)) 428.60/297.08 , zero2(s(y), nil()) -> zero(nil()) 428.60/297.08 , zero2(s(y), cons(x, xs)) -> zero(cons(x, xs)) } 428.60/297.08 Obligation: 428.60/297.08 innermost runtime complexity 428.60/297.08 Answer: 428.60/297.08 MAYBE 428.60/297.08 428.60/297.08 None of the processors succeeded. 428.60/297.08 428.60/297.08 Details of failed attempt(s): 428.60/297.08 ----------------------------- 428.60/297.08 1) 'empty' failed due to the following reason: 428.60/297.08 428.60/297.08 Empty strict component of the problem is NOT empty. 428.60/297.08 428.60/297.08 2) 'Best' failed due to the following reason: 428.60/297.08 428.60/297.08 None of the processors succeeded. 428.60/297.08 428.60/297.08 Details of failed attempt(s): 428.60/297.08 ----------------------------- 428.60/297.08 1) 'With Problem ... (timeout of 297 seconds)' failed due to the 428.60/297.08 following reason: 428.60/297.08 428.60/297.08 Computation stopped due to timeout after 297.0 seconds. 428.60/297.08 428.60/297.08 2) 'Best' failed due to the following reason: 428.60/297.08 428.60/297.08 None of the processors succeeded. 428.60/297.08 428.60/297.08 Details of failed attempt(s): 428.60/297.08 ----------------------------- 428.60/297.08 1) 'With Problem ... (timeout of 148 seconds) (timeout of 297 428.60/297.08 seconds)' failed due to the following reason: 428.60/297.08 428.60/297.08 The weightgap principle applies (using the following nonconstant 428.60/297.08 growth matrix-interpretation) 428.60/297.08 428.60/297.08 The following argument positions are usable: 428.60/297.08 Uargs(zero2) = {1}, Uargs(cons) = {1, 2} 428.60/297.08 428.60/297.08 TcT has computed the following matrix interpretation satisfying 428.60/297.08 not(EDA) and not(IDA(1)). 428.60/297.08 428.60/297.08 [sub](x1, x2) = [1] 428.60/297.08 428.60/297.08 [0] = [0] 428.60/297.08 428.60/297.08 [s](x1) = [0] 428.60/297.08 428.60/297.08 [zero](x1) = [0] 428.60/297.08 428.60/297.08 [nil] = [5] 428.60/297.08 428.60/297.08 [zero2](x1, x2) = [1] x1 + [0] 428.60/297.08 428.60/297.08 [cons](x1, x2) = [1] x1 + [1] x2 + [0] 428.60/297.08 428.60/297.08 The order satisfies the following ordering constraints: 428.60/297.08 428.60/297.08 [sub(0(), 0())] = [1] 428.60/297.08 > [0] 428.60/297.08 = [0()] 428.60/297.08 428.60/297.08 [sub(0(), s(x))] = [1] 428.60/297.08 > [0] 428.60/297.08 = [0()] 428.60/297.08 428.60/297.08 [sub(s(x), 0())] = [1] 428.60/297.08 > [0] 428.60/297.08 = [s(x)] 428.60/297.08 428.60/297.08 [sub(s(x), s(y))] = [1] 428.60/297.08 >= [1] 428.60/297.08 = [sub(x, y)] 428.60/297.08 428.60/297.08 [zero(nil())] = [0] 428.60/297.08 >= [0] 428.60/297.08 = [zero2(0(), nil())] 428.60/297.08 428.60/297.08 [zero(cons(x, xs))] = [0] 428.60/297.08 ? [1] 428.60/297.08 = [zero2(sub(x, x), cons(x, xs))] 428.60/297.08 428.60/297.08 [zero2(0(), nil())] = [0] 428.60/297.08 ? [5] 428.60/297.08 = [nil()] 428.60/297.08 428.60/297.08 [zero2(0(), cons(x, xs))] = [0] 428.60/297.08 ? [1] 428.60/297.08 = [cons(sub(x, x), zero(xs))] 428.60/297.08 428.60/297.08 [zero2(s(y), nil())] = [0] 428.60/297.08 >= [0] 428.60/297.08 = [zero(nil())] 428.60/297.08 428.60/297.08 [zero2(s(y), cons(x, xs))] = [0] 428.60/297.08 >= [0] 428.60/297.08 = [zero(cons(x, xs))] 428.60/297.08 428.60/297.08 428.60/297.08 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 428.60/297.08 428.60/297.08 We are left with following problem, upon which TcT provides the 428.60/297.08 certificate MAYBE. 428.60/297.08 428.60/297.08 Strict Trs: 428.60/297.08 { sub(s(x), s(y)) -> sub(x, y) 428.60/297.08 , zero(nil()) -> zero2(0(), nil()) 428.60/297.08 , zero(cons(x, xs)) -> zero2(sub(x, x), cons(x, xs)) 428.60/297.08 , zero2(0(), nil()) -> nil() 428.60/297.08 , zero2(0(), cons(x, xs)) -> cons(sub(x, x), zero(xs)) 428.60/297.08 , zero2(s(y), nil()) -> zero(nil()) 428.60/297.08 , zero2(s(y), cons(x, xs)) -> zero(cons(x, xs)) } 428.60/297.08 Weak Trs: 428.60/297.08 { sub(0(), 0()) -> 0() 428.60/297.08 , sub(0(), s(x)) -> 0() 428.60/297.08 , sub(s(x), 0()) -> s(x) } 428.60/297.08 Obligation: 428.60/297.08 innermost runtime complexity 428.60/297.08 Answer: 428.60/297.08 MAYBE 428.60/297.08 428.60/297.08 The weightgap principle applies (using the following nonconstant 428.60/297.08 growth matrix-interpretation) 428.60/297.08 428.60/297.08 The following argument positions are usable: 428.60/297.08 Uargs(zero2) = {1}, Uargs(cons) = {1, 2} 428.60/297.08 428.60/297.08 TcT has computed the following matrix interpretation satisfying 428.60/297.08 not(EDA) and not(IDA(1)). 428.60/297.08 428.60/297.08 [sub](x1, x2) = [4] 428.60/297.08 428.60/297.08 [0] = [1] 428.60/297.08 428.60/297.08 [s](x1) = [0] 428.60/297.08 428.60/297.08 [zero](x1) = [0] 428.60/297.08 428.60/297.08 [nil] = [0] 428.60/297.08 428.60/297.08 [zero2](x1, x2) = [1] x1 + [0] 428.60/297.08 428.60/297.08 [cons](x1, x2) = [1] x1 + [1] x2 + [0] 428.60/297.08 428.60/297.08 The order satisfies the following ordering constraints: 428.60/297.08 428.60/297.08 [sub(0(), 0())] = [4] 428.60/297.08 > [1] 428.60/297.08 = [0()] 428.60/297.08 428.60/297.08 [sub(0(), s(x))] = [4] 428.60/297.08 > [1] 428.60/297.08 = [0()] 428.60/297.08 428.60/297.08 [sub(s(x), 0())] = [4] 428.60/297.08 > [0] 428.60/297.08 = [s(x)] 428.60/297.08 428.60/297.08 [sub(s(x), s(y))] = [4] 428.60/297.08 >= [4] 428.60/297.08 = [sub(x, y)] 428.60/297.08 428.60/297.08 [zero(nil())] = [0] 428.60/297.08 ? [1] 428.60/297.08 = [zero2(0(), nil())] 428.60/297.08 428.60/297.08 [zero(cons(x, xs))] = [0] 428.60/297.08 ? [4] 428.60/297.08 = [zero2(sub(x, x), cons(x, xs))] 428.60/297.08 428.60/297.08 [zero2(0(), nil())] = [1] 428.60/297.08 > [0] 428.60/297.08 = [nil()] 428.60/297.08 428.60/297.08 [zero2(0(), cons(x, xs))] = [1] 428.60/297.08 ? [4] 428.60/297.08 = [cons(sub(x, x), zero(xs))] 428.60/297.08 428.60/297.08 [zero2(s(y), nil())] = [0] 428.60/297.08 >= [0] 428.60/297.08 = [zero(nil())] 428.60/297.08 428.60/297.08 [zero2(s(y), cons(x, xs))] = [0] 428.60/297.08 >= [0] 428.60/297.08 = [zero(cons(x, xs))] 428.60/297.08 428.60/297.08 428.60/297.08 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 428.60/297.08 428.60/297.08 We are left with following problem, upon which TcT provides the 428.60/297.08 certificate MAYBE. 428.60/297.08 428.60/297.08 Strict Trs: 428.60/297.08 { sub(s(x), s(y)) -> sub(x, y) 428.60/297.08 , zero(nil()) -> zero2(0(), nil()) 428.60/297.08 , zero(cons(x, xs)) -> zero2(sub(x, x), cons(x, xs)) 428.60/297.08 , zero2(0(), cons(x, xs)) -> cons(sub(x, x), zero(xs)) 428.60/297.08 , zero2(s(y), nil()) -> zero(nil()) 428.60/297.08 , zero2(s(y), cons(x, xs)) -> zero(cons(x, xs)) } 428.60/297.08 Weak Trs: 428.60/297.08 { sub(0(), 0()) -> 0() 428.60/297.08 , sub(0(), s(x)) -> 0() 428.60/297.08 , sub(s(x), 0()) -> s(x) 428.60/297.08 , zero2(0(), nil()) -> nil() } 428.60/297.08 Obligation: 428.60/297.08 innermost runtime complexity 428.60/297.08 Answer: 428.60/297.08 MAYBE 428.60/297.08 428.60/297.08 The weightgap principle applies (using the following nonconstant 428.60/297.08 growth matrix-interpretation) 428.60/297.08 428.60/297.08 The following argument positions are usable: 428.60/297.08 Uargs(zero2) = {1}, Uargs(cons) = {1, 2} 428.60/297.08 428.60/297.08 TcT has computed the following matrix interpretation satisfying 428.60/297.08 not(EDA) and not(IDA(1)). 428.60/297.08 428.60/297.08 [sub](x1, x2) = [1] 428.60/297.08 428.60/297.08 [0] = [0] 428.60/297.08 428.60/297.08 [s](x1) = [1] 428.60/297.08 428.60/297.08 [zero](x1) = [0] 428.60/297.08 428.60/297.08 [nil] = [0] 428.60/297.08 428.60/297.08 [zero2](x1, x2) = [1] x1 + [0] 428.60/297.08 428.60/297.08 [cons](x1, x2) = [1] x1 + [1] x2 + [0] 428.60/297.08 428.60/297.08 The order satisfies the following ordering constraints: 428.60/297.08 428.60/297.08 [sub(0(), 0())] = [1] 428.60/297.08 > [0] 428.60/297.08 = [0()] 428.60/297.08 428.60/297.08 [sub(0(), s(x))] = [1] 428.60/297.08 > [0] 428.60/297.08 = [0()] 428.60/297.08 428.60/297.08 [sub(s(x), 0())] = [1] 428.60/297.08 >= [1] 428.60/297.08 = [s(x)] 428.60/297.08 428.60/297.08 [sub(s(x), s(y))] = [1] 428.60/297.08 >= [1] 428.60/297.08 = [sub(x, y)] 428.60/297.08 428.60/297.08 [zero(nil())] = [0] 428.60/297.08 >= [0] 428.60/297.08 = [zero2(0(), nil())] 428.60/297.08 428.60/297.08 [zero(cons(x, xs))] = [0] 428.60/297.08 ? [1] 428.60/297.08 = [zero2(sub(x, x), cons(x, xs))] 428.60/297.08 428.60/297.08 [zero2(0(), nil())] = [0] 428.60/297.08 >= [0] 428.60/297.08 = [nil()] 428.60/297.08 428.60/297.08 [zero2(0(), cons(x, xs))] = [0] 428.60/297.08 ? [1] 428.60/297.08 = [cons(sub(x, x), zero(xs))] 428.60/297.08 428.60/297.08 [zero2(s(y), nil())] = [1] 428.60/297.08 > [0] 428.60/297.08 = [zero(nil())] 428.60/297.08 428.60/297.08 [zero2(s(y), cons(x, xs))] = [1] 428.60/297.08 > [0] 428.60/297.08 = [zero(cons(x, xs))] 428.60/297.08 428.60/297.08 428.60/297.08 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 428.60/297.08 428.60/297.08 We are left with following problem, upon which TcT provides the 428.60/297.08 certificate MAYBE. 428.60/297.08 428.60/297.08 Strict Trs: 428.60/297.08 { sub(s(x), s(y)) -> sub(x, y) 428.60/297.08 , zero(nil()) -> zero2(0(), nil()) 428.60/297.08 , zero(cons(x, xs)) -> zero2(sub(x, x), cons(x, xs)) 428.60/297.08 , zero2(0(), cons(x, xs)) -> cons(sub(x, x), zero(xs)) } 428.60/297.08 Weak Trs: 428.60/297.08 { sub(0(), 0()) -> 0() 428.60/297.08 , sub(0(), s(x)) -> 0() 428.60/297.08 , sub(s(x), 0()) -> s(x) 428.60/297.08 , zero2(0(), nil()) -> nil() 428.60/297.08 , zero2(s(y), nil()) -> zero(nil()) 428.60/297.08 , zero2(s(y), cons(x, xs)) -> zero(cons(x, xs)) } 428.60/297.08 Obligation: 428.60/297.08 innermost runtime complexity 428.60/297.08 Answer: 428.60/297.08 MAYBE 428.60/297.08 428.60/297.08 The weightgap principle applies (using the following nonconstant 428.60/297.08 growth matrix-interpretation) 428.60/297.08 428.60/297.08 The following argument positions are usable: 428.60/297.08 Uargs(zero2) = {1}, Uargs(cons) = {1, 2} 428.60/297.08 428.60/297.08 TcT has computed the following matrix interpretation satisfying 428.60/297.08 not(EDA) and not(IDA(1)). 428.60/297.08 428.60/297.08 [sub](x1, x2) = [0] 428.60/297.08 428.60/297.08 [0] = [0] 428.60/297.08 428.60/297.08 [s](x1) = [0] 428.60/297.08 428.60/297.08 [zero](x1) = [0] 428.60/297.08 428.60/297.08 [nil] = [1] 428.60/297.08 428.60/297.08 [zero2](x1, x2) = [1] x1 + [1] 428.60/297.08 428.60/297.08 [cons](x1, x2) = [1] x1 + [1] x2 + [0] 428.60/297.08 428.60/297.08 The order satisfies the following ordering constraints: 428.60/297.08 428.60/297.08 [sub(0(), 0())] = [0] 428.60/297.08 >= [0] 428.60/297.08 = [0()] 428.60/297.08 428.60/297.08 [sub(0(), s(x))] = [0] 428.60/297.08 >= [0] 428.60/297.08 = [0()] 428.60/297.08 428.60/297.08 [sub(s(x), 0())] = [0] 428.60/297.08 >= [0] 428.60/297.08 = [s(x)] 428.60/297.08 428.60/297.08 [sub(s(x), s(y))] = [0] 428.60/297.08 >= [0] 428.60/297.08 = [sub(x, y)] 428.60/297.08 428.60/297.08 [zero(nil())] = [0] 428.60/297.08 ? [1] 428.60/297.08 = [zero2(0(), nil())] 428.60/297.08 428.60/297.08 [zero(cons(x, xs))] = [0] 428.60/297.08 ? [1] 428.60/297.08 = [zero2(sub(x, x), cons(x, xs))] 428.60/297.08 428.60/297.08 [zero2(0(), nil())] = [1] 428.60/297.08 >= [1] 428.60/297.08 = [nil()] 428.60/297.08 428.60/297.08 [zero2(0(), cons(x, xs))] = [1] 428.60/297.08 > [0] 428.60/297.08 = [cons(sub(x, x), zero(xs))] 428.60/297.08 428.60/297.08 [zero2(s(y), nil())] = [1] 428.60/297.08 > [0] 428.60/297.08 = [zero(nil())] 428.60/297.08 428.60/297.08 [zero2(s(y), cons(x, xs))] = [1] 428.60/297.08 > [0] 428.60/297.08 = [zero(cons(x, xs))] 428.60/297.08 428.60/297.08 428.60/297.08 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 428.60/297.08 428.60/297.08 We are left with following problem, upon which TcT provides the 428.60/297.08 certificate MAYBE. 428.60/297.08 428.60/297.08 Strict Trs: 428.60/297.08 { sub(s(x), s(y)) -> sub(x, y) 428.60/297.08 , zero(nil()) -> zero2(0(), nil()) 428.60/297.08 , zero(cons(x, xs)) -> zero2(sub(x, x), cons(x, xs)) } 428.60/297.08 Weak Trs: 428.60/297.08 { sub(0(), 0()) -> 0() 428.60/297.08 , sub(0(), s(x)) -> 0() 428.60/297.08 , sub(s(x), 0()) -> s(x) 428.60/297.08 , zero2(0(), nil()) -> nil() 428.60/297.08 , zero2(0(), cons(x, xs)) -> cons(sub(x, x), zero(xs)) 428.60/297.08 , zero2(s(y), nil()) -> zero(nil()) 428.60/297.08 , zero2(s(y), cons(x, xs)) -> zero(cons(x, xs)) } 428.60/297.08 Obligation: 428.60/297.08 innermost runtime complexity 428.60/297.08 Answer: 428.60/297.08 MAYBE 428.60/297.08 428.60/297.08 We use the processor 'matrix interpretation of dimension 1' to 428.60/297.08 orient following rules strictly. 428.60/297.08 428.60/297.08 Trs: { zero(nil()) -> zero2(0(), nil()) } 428.60/297.08 428.60/297.08 The induced complexity on above rules (modulo remaining rules) is 428.60/297.08 YES(?,O(n^1)) . These rules are moved into the corresponding weak 428.60/297.08 component(s). 428.60/297.08 428.60/297.08 Sub-proof: 428.60/297.08 ---------- 428.60/297.08 The following argument positions are usable: 428.60/297.08 Uargs(zero2) = {1}, Uargs(cons) = {1, 2} 428.60/297.08 428.60/297.08 TcT has computed the following constructor-based matrix 428.60/297.08 interpretation satisfying not(EDA). 428.60/297.08 428.60/297.08 [sub](x1, x2) = [1] 428.60/297.08 428.60/297.08 [0] = [0] 428.60/297.08 428.60/297.08 [s](x1) = [1] 428.60/297.08 428.60/297.08 [zero](x1) = [2] x1 + [4] 428.60/297.08 428.60/297.08 [nil] = [0] 428.60/297.08 428.60/297.08 [zero2](x1, x2) = [2] x1 + [2] x2 + [2] 428.60/297.08 428.60/297.08 [cons](x1, x2) = [1] x1 + [1] x2 + [4] 428.60/297.08 428.60/297.08 The order satisfies the following ordering constraints: 428.60/297.08 428.60/297.08 [sub(0(), 0())] = [1] 428.60/297.08 > [0] 428.60/297.08 = [0()] 428.60/297.08 428.60/297.08 [sub(0(), s(x))] = [1] 428.60/297.08 > [0] 428.60/297.08 = [0()] 428.60/297.08 428.60/297.08 [sub(s(x), 0())] = [1] 428.60/297.08 >= [1] 428.60/297.08 = [s(x)] 428.60/297.08 428.60/297.08 [sub(s(x), s(y))] = [1] 428.60/297.08 >= [1] 428.60/297.08 = [sub(x, y)] 428.60/297.08 428.60/297.08 [zero(nil())] = [4] 428.60/297.08 > [2] 428.60/297.08 = [zero2(0(), nil())] 428.60/297.08 428.60/297.08 [zero(cons(x, xs))] = [2] x + [2] xs + [12] 428.60/297.08 >= [2] x + [2] xs + [12] 428.60/297.08 = [zero2(sub(x, x), cons(x, xs))] 428.60/297.08 428.60/297.08 [zero2(0(), nil())] = [2] 428.60/297.08 > [0] 428.60/297.08 = [nil()] 428.60/297.09 428.60/297.09 [zero2(0(), cons(x, xs))] = [2] x + [2] xs + [10] 428.60/297.09 > [2] xs + [9] 428.60/297.09 = [cons(sub(x, x), zero(xs))] 428.60/297.09 428.60/297.09 [zero2(s(y), nil())] = [4] 428.60/297.09 >= [4] 428.60/297.09 = [zero(nil())] 428.60/297.09 428.60/297.09 [zero2(s(y), cons(x, xs))] = [2] x + [2] xs + [12] 428.60/297.09 >= [2] x + [2] xs + [12] 428.60/297.09 = [zero(cons(x, xs))] 428.60/297.09 428.60/297.09 428.60/297.09 We return to the main proof. 428.60/297.09 428.60/297.09 We are left with following problem, upon which TcT provides the 428.60/297.09 certificate MAYBE. 428.60/297.09 428.60/297.09 Strict Trs: 428.60/297.09 { sub(s(x), s(y)) -> sub(x, y) 428.60/297.09 , zero(cons(x, xs)) -> zero2(sub(x, x), cons(x, xs)) } 428.60/297.09 Weak Trs: 428.60/297.09 { sub(0(), 0()) -> 0() 428.60/297.09 , sub(0(), s(x)) -> 0() 428.60/297.09 , sub(s(x), 0()) -> s(x) 428.60/297.09 , zero(nil()) -> zero2(0(), nil()) 428.60/297.09 , zero2(0(), nil()) -> nil() 428.60/297.09 , zero2(0(), cons(x, xs)) -> cons(sub(x, x), zero(xs)) 428.60/297.09 , zero2(s(y), nil()) -> zero(nil()) 428.60/297.09 , zero2(s(y), cons(x, xs)) -> zero(cons(x, xs)) } 428.60/297.09 Obligation: 428.60/297.09 innermost runtime complexity 428.60/297.09 Answer: 428.60/297.09 MAYBE 428.60/297.09 428.60/297.09 None of the processors succeeded. 428.60/297.09 428.60/297.09 Details of failed attempt(s): 428.60/297.09 ----------------------------- 428.60/297.09 1) 'empty' failed due to the following reason: 428.60/297.09 428.60/297.09 Empty strict component of the problem is NOT empty. 428.60/297.09 428.60/297.09 2) 'With Problem ...' failed due to the following reason: 428.60/297.09 428.60/297.09 None of the processors succeeded. 428.60/297.09 428.60/297.09 Details of failed attempt(s): 428.60/297.09 ----------------------------- 428.60/297.09 1) 'empty' failed due to the following reason: 428.60/297.09 428.60/297.09 Empty strict component of the problem is NOT empty. 428.60/297.09 428.60/297.09 2) 'Fastest' failed due to the following reason: 428.60/297.09 428.60/297.09 None of the processors succeeded. 428.60/297.09 428.60/297.09 Details of failed attempt(s): 428.60/297.09 ----------------------------- 428.60/297.09 1) 'With Problem ...' failed due to the following reason: 428.60/297.09 428.60/297.09 None of the processors succeeded. 428.60/297.09 428.60/297.09 Details of failed attempt(s): 428.60/297.09 ----------------------------- 428.60/297.09 1) 'empty' failed due to the following reason: 428.60/297.09 428.60/297.09 Empty strict component of the problem is NOT empty. 428.60/297.09 428.60/297.09 2) 'With Problem ...' failed due to the following reason: 428.60/297.09 428.60/297.09 None of the processors succeeded. 428.60/297.09 428.60/297.09 Details of failed attempt(s): 428.60/297.09 ----------------------------- 428.60/297.09 1) 'empty' failed due to the following reason: 428.60/297.09 428.60/297.09 Empty strict component of the problem is NOT empty. 428.60/297.09 428.60/297.09 2) 'With Problem ...' failed due to the following reason: 428.60/297.09 428.60/297.09 None of the processors succeeded. 428.60/297.09 428.60/297.09 Details of failed attempt(s): 428.60/297.09 ----------------------------- 428.60/297.09 1) 'empty' failed due to the following reason: 428.60/297.09 428.60/297.09 Empty strict component of the problem is NOT empty. 428.60/297.09 428.60/297.09 2) 'With Problem ...' failed due to the following reason: 428.60/297.09 428.60/297.09 Empty strict component of the problem is NOT empty. 428.60/297.09 428.60/297.09 428.60/297.09 428.60/297.09 428.60/297.09 2) 'With Problem ...' failed due to the following reason: 428.60/297.09 428.60/297.09 None of the processors succeeded. 428.60/297.09 428.60/297.09 Details of failed attempt(s): 428.60/297.09 ----------------------------- 428.60/297.09 1) 'empty' failed due to the following reason: 428.60/297.09 428.60/297.09 Empty strict component of the problem is NOT empty. 428.60/297.09 428.60/297.09 2) 'With Problem ...' failed due to the following reason: 428.60/297.09 428.60/297.09 Empty strict component of the problem is NOT empty. 428.60/297.09 428.60/297.09 428.60/297.09 428.60/297.09 428.60/297.09 428.60/297.09 2) 'Best' failed due to the following reason: 428.60/297.09 428.60/297.09 None of the processors succeeded. 428.60/297.09 428.60/297.09 Details of failed attempt(s): 428.60/297.09 ----------------------------- 428.60/297.09 1) 'bsearch-popstar (timeout of 297 seconds)' failed due to the 428.60/297.09 following reason: 428.60/297.09 428.60/297.09 The input cannot be shown compatible 428.60/297.09 428.60/297.09 2) 'Polynomial Path Order (PS) (timeout of 297 seconds)' failed due 428.60/297.09 to the following reason: 428.60/297.09 428.60/297.09 The input cannot be shown compatible 428.60/297.09 428.60/297.09 428.60/297.09 3) 'Fastest (timeout of 24 seconds) (timeout of 297 seconds)' 428.60/297.09 failed due to the following reason: 428.60/297.09 428.60/297.09 None of the processors succeeded. 428.60/297.09 428.60/297.09 Details of failed attempt(s): 428.60/297.09 ----------------------------- 428.60/297.09 1) 'Bounds with minimal-enrichment and initial automaton 'match'' 428.60/297.09 failed due to the following reason: 428.60/297.09 428.60/297.09 match-boundness of the problem could not be verified. 428.60/297.09 428.60/297.09 2) 'Bounds with perSymbol-enrichment and initial automaton 'match'' 428.60/297.09 failed due to the following reason: 428.60/297.09 428.60/297.09 match-boundness of the problem could not be verified. 428.60/297.09 428.60/297.09 428.60/297.09 428.60/297.09 428.60/297.09 428.60/297.09 Arrrr.. 428.93/297.10 EOF