MAYBE 824.25/297.03 MAYBE 824.25/297.03 824.25/297.03 We are left with following problem, upon which TcT provides the 824.25/297.03 certificate MAYBE. 824.25/297.03 824.25/297.03 Strict Trs: 824.25/297.03 { ack(Cons(x', xs'), Cons(x, xs)) -> 824.25/297.03 ack(xs', ack(Cons(x', xs'), xs)) 824.25/297.03 , ack(Cons(x, xs), Nil()) -> ack(xs, Cons(Nil(), Nil())) 824.25/297.03 , ack(Nil(), n) -> Cons(Cons(Nil(), Nil()), n) 824.25/297.03 , goal(m, n) -> ack(m, n) } 824.25/297.03 Obligation: 824.25/297.03 innermost runtime complexity 824.25/297.03 Answer: 824.25/297.03 MAYBE 824.25/297.03 824.25/297.03 None of the processors succeeded. 824.25/297.03 824.25/297.03 Details of failed attempt(s): 824.25/297.03 ----------------------------- 824.25/297.03 1) 'empty' failed due to the following reason: 824.25/297.03 824.25/297.03 Empty strict component of the problem is NOT empty. 824.25/297.03 824.25/297.03 2) 'Best' failed due to the following reason: 824.25/297.03 824.25/297.03 None of the processors succeeded. 824.25/297.03 824.25/297.03 Details of failed attempt(s): 824.25/297.03 ----------------------------- 824.25/297.03 1) 'With Problem ... (timeout of 297 seconds)' failed due to the 824.25/297.03 following reason: 824.25/297.03 824.25/297.03 Computation stopped due to timeout after 297.0 seconds. 824.25/297.03 824.25/297.03 2) 'Best' failed due to the following reason: 824.25/297.03 824.25/297.03 None of the processors succeeded. 824.25/297.03 824.25/297.03 Details of failed attempt(s): 824.25/297.03 ----------------------------- 824.25/297.03 1) 'With Problem ... (timeout of 148 seconds) (timeout of 297 824.25/297.03 seconds)' failed due to the following reason: 824.25/297.03 824.25/297.03 The weightgap principle applies (using the following nonconstant 824.25/297.03 growth matrix-interpretation) 824.25/297.03 824.25/297.03 The following argument positions are usable: 824.25/297.03 Uargs(ack) = {2} 824.25/297.03 824.25/297.03 TcT has computed the following matrix interpretation satisfying 824.25/297.03 not(EDA) and not(IDA(1)). 824.25/297.03 824.25/297.03 [ack](x1, x2) = [1] x2 + [0] 824.25/297.03 824.25/297.03 [Cons](x1, x2) = [1] x2 + [0] 824.25/297.03 824.25/297.03 [Nil] = [0] 824.25/297.03 824.25/297.03 [goal](x1, x2) = [1] x1 + [1] x2 + [7] 824.25/297.03 824.25/297.03 The order satisfies the following ordering constraints: 824.25/297.03 824.25/297.03 [ack(Cons(x', xs'), Cons(x, xs))] = [1] xs + [0] 824.25/297.03 >= [1] xs + [0] 824.25/297.03 = [ack(xs', ack(Cons(x', xs'), xs))] 824.25/297.03 824.25/297.03 [ack(Cons(x, xs), Nil())] = [0] 824.25/297.03 >= [0] 824.25/297.03 = [ack(xs, Cons(Nil(), Nil()))] 824.25/297.03 824.25/297.03 [ack(Nil(), n)] = [1] n + [0] 824.25/297.03 >= [1] n + [0] 824.25/297.03 = [Cons(Cons(Nil(), Nil()), n)] 824.25/297.03 824.25/297.03 [goal(m, n)] = [1] n + [1] m + [7] 824.25/297.03 > [1] n + [0] 824.25/297.03 = [ack(m, n)] 824.25/297.03 824.25/297.03 824.25/297.03 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 824.25/297.03 824.25/297.03 We are left with following problem, upon which TcT provides the 824.25/297.03 certificate MAYBE. 824.25/297.03 824.25/297.03 Strict Trs: 824.25/297.03 { ack(Cons(x', xs'), Cons(x, xs)) -> 824.25/297.03 ack(xs', ack(Cons(x', xs'), xs)) 824.25/297.03 , ack(Cons(x, xs), Nil()) -> ack(xs, Cons(Nil(), Nil())) 824.25/297.03 , ack(Nil(), n) -> Cons(Cons(Nil(), Nil()), n) } 824.25/297.03 Weak Trs: { goal(m, n) -> ack(m, n) } 824.25/297.03 Obligation: 824.25/297.03 innermost runtime complexity 824.25/297.03 Answer: 824.25/297.03 MAYBE 824.25/297.03 824.25/297.03 The weightgap principle applies (using the following nonconstant 824.25/297.03 growth matrix-interpretation) 824.25/297.03 824.25/297.03 The following argument positions are usable: 824.25/297.03 Uargs(ack) = {2} 824.25/297.03 824.25/297.03 TcT has computed the following matrix interpretation satisfying 824.25/297.03 not(EDA) and not(IDA(1)). 824.25/297.03 824.25/297.03 [ack](x1, x2) = [1] x2 + [4] 824.25/297.03 824.25/297.03 [Cons](x1, x2) = [1] x2 + [0] 824.25/297.03 824.25/297.03 [Nil] = [0] 824.25/297.03 824.25/297.03 [goal](x1, x2) = [1] x1 + [1] x2 + [7] 824.25/297.03 824.25/297.03 The order satisfies the following ordering constraints: 824.25/297.03 824.25/297.03 [ack(Cons(x', xs'), Cons(x, xs))] = [1] xs + [4] 824.25/297.03 ? [1] xs + [8] 824.25/297.03 = [ack(xs', ack(Cons(x', xs'), xs))] 824.25/297.03 824.25/297.03 [ack(Cons(x, xs), Nil())] = [4] 824.25/297.03 >= [4] 824.25/297.03 = [ack(xs, Cons(Nil(), Nil()))] 824.25/297.03 824.25/297.03 [ack(Nil(), n)] = [1] n + [4] 824.25/297.03 > [1] n + [0] 824.25/297.03 = [Cons(Cons(Nil(), Nil()), n)] 824.25/297.03 824.25/297.03 [goal(m, n)] = [1] n + [1] m + [7] 824.25/297.03 > [1] n + [4] 824.25/297.03 = [ack(m, n)] 824.25/297.03 824.25/297.03 824.25/297.03 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 824.25/297.03 824.25/297.03 We are left with following problem, upon which TcT provides the 824.25/297.03 certificate MAYBE. 824.25/297.03 824.25/297.03 Strict Trs: 824.25/297.03 { ack(Cons(x', xs'), Cons(x, xs)) -> 824.25/297.03 ack(xs', ack(Cons(x', xs'), xs)) 824.25/297.03 , ack(Cons(x, xs), Nil()) -> ack(xs, Cons(Nil(), Nil())) } 824.25/297.03 Weak Trs: 824.25/297.03 { ack(Nil(), n) -> Cons(Cons(Nil(), Nil()), n) 824.25/297.03 , goal(m, n) -> ack(m, n) } 824.25/297.03 Obligation: 824.25/297.03 innermost runtime complexity 824.25/297.03 Answer: 824.25/297.03 MAYBE 824.25/297.03 824.25/297.03 None of the processors succeeded. 824.25/297.03 824.25/297.03 Details of failed attempt(s): 824.25/297.03 ----------------------------- 824.25/297.03 1) 'empty' failed due to the following reason: 824.25/297.03 824.25/297.03 Empty strict component of the problem is NOT empty. 824.25/297.03 824.25/297.03 2) 'With Problem ...' failed due to the following reason: 824.25/297.03 824.25/297.03 None of the processors succeeded. 824.25/297.03 824.25/297.03 Details of failed attempt(s): 824.25/297.03 ----------------------------- 824.25/297.03 1) 'empty' failed due to the following reason: 824.25/297.03 824.25/297.03 Empty strict component of the problem is NOT empty. 824.25/297.03 824.25/297.03 2) 'Fastest' failed due to the following reason: 824.25/297.03 824.25/297.03 None of the processors succeeded. 824.25/297.03 824.25/297.03 Details of failed attempt(s): 824.25/297.03 ----------------------------- 824.25/297.03 1) 'With Problem ...' failed due to the following reason: 824.25/297.03 824.25/297.03 None of the processors succeeded. 824.25/297.03 824.25/297.03 Details of failed attempt(s): 824.25/297.03 ----------------------------- 824.25/297.03 1) 'empty' failed due to the following reason: 824.25/297.03 824.25/297.03 Empty strict component of the problem is NOT empty. 824.25/297.03 824.25/297.03 2) 'With Problem ...' failed due to the following reason: 824.25/297.03 824.25/297.03 Empty strict component of the problem is NOT empty. 824.25/297.03 824.25/297.03 824.25/297.03 2) 'With Problem ...' failed due to the following reason: 824.25/297.03 824.25/297.03 None of the processors succeeded. 824.25/297.03 824.25/297.03 Details of failed attempt(s): 824.25/297.03 ----------------------------- 824.25/297.03 1) 'empty' failed due to the following reason: 824.25/297.03 824.25/297.03 Empty strict component of the problem is NOT empty. 824.25/297.03 824.25/297.03 2) 'With Problem ...' failed due to the following reason: 824.25/297.03 824.25/297.03 None of the processors succeeded. 824.25/297.03 824.25/297.03 Details of failed attempt(s): 824.25/297.03 ----------------------------- 824.25/297.03 1) 'empty' failed due to the following reason: 824.25/297.03 824.25/297.03 Empty strict component of the problem is NOT empty. 824.25/297.03 824.25/297.03 2) 'With Problem ...' failed due to the following reason: 824.25/297.03 824.25/297.03 None of the processors succeeded. 824.25/297.03 824.25/297.03 Details of failed attempt(s): 824.25/297.03 ----------------------------- 824.25/297.03 1) 'empty' failed due to the following reason: 824.25/297.03 824.25/297.03 Empty strict component of the problem is NOT empty. 824.25/297.03 824.25/297.03 2) 'With Problem ...' failed due to the following reason: 824.25/297.03 824.25/297.03 Empty strict component of the problem is NOT empty. 824.25/297.03 824.25/297.03 824.25/297.03 824.25/297.03 824.25/297.03 824.25/297.03 824.25/297.03 824.25/297.03 2) 'Best' failed due to the following reason: 824.25/297.03 824.25/297.03 None of the processors succeeded. 824.25/297.03 824.25/297.03 Details of failed attempt(s): 824.25/297.03 ----------------------------- 824.25/297.03 1) 'bsearch-popstar (timeout of 297 seconds)' failed due to the 824.25/297.03 following reason: 824.25/297.03 824.25/297.03 The input cannot be shown compatible 824.25/297.03 824.25/297.03 2) 'Polynomial Path Order (PS) (timeout of 297 seconds)' failed due 824.25/297.03 to the following reason: 824.25/297.03 824.25/297.03 The input cannot be shown compatible 824.25/297.03 824.25/297.03 824.25/297.03 3) 'Fastest (timeout of 24 seconds) (timeout of 297 seconds)' 824.25/297.03 failed due to the following reason: 824.25/297.03 824.25/297.03 None of the processors succeeded. 824.25/297.03 824.25/297.03 Details of failed attempt(s): 824.25/297.03 ----------------------------- 824.25/297.03 1) 'Bounds with minimal-enrichment and initial automaton 'match'' 824.25/297.03 failed due to the following reason: 824.25/297.03 824.25/297.03 match-boundness of the problem could not be verified. 824.25/297.03 824.25/297.03 2) 'Bounds with perSymbol-enrichment and initial automaton 'match'' 824.25/297.03 failed due to the following reason: 824.25/297.03 824.25/297.03 match-boundness of the problem could not be verified. 824.25/297.03 824.25/297.03 824.25/297.03 824.25/297.03 824.25/297.03 824.25/297.03 Arrrr.. 824.58/297.36 EOF