MAYBE 1068.91/297.07 MAYBE 1068.91/297.07 1068.91/297.07 We are left with following problem, upon which TcT provides the 1068.91/297.07 certificate MAYBE. 1068.91/297.07 1068.91/297.07 Strict Trs: 1068.91/297.07 { f(x, Cons(x', xs)) -> 1068.91/297.07 f(f[Ite][False][Ite](lt0(x, Cons(Nil(), Nil())), x, Cons(x', xs)), 1068.91/297.07 f[Ite][False][Ite](lt0(x, Cons(Nil(), Nil())), x, Cons(x', xs))) 1068.91/297.07 , f(x, Nil()) -> 1068.91/297.07 Cons(Nil(), 1068.91/297.07 Cons(Nil(), 1068.91/297.07 Cons(Nil(), 1068.91/297.07 Cons(Nil(), 1068.91/297.07 Cons(Nil(), 1068.91/297.07 Cons(Nil(), 1068.91/297.07 Cons(Nil(), 1068.91/297.07 Cons(Nil(), 1068.91/297.07 Cons(Nil(), 1068.91/297.07 Cons(Nil(), 1068.91/297.07 Cons(Nil(), 1068.91/297.07 Cons(Nil(), 1068.91/297.07 Cons(Nil(), 1068.91/297.07 Cons(Nil(), 1068.91/297.07 Cons(Nil(), 1068.91/297.07 Cons(Nil(), 1068.91/297.07 Cons(Nil(), 1068.91/297.07 Cons(Nil(), 1068.91/297.07 Cons(Nil(), 1068.91/297.07 Cons(Nil(), 1068.91/297.07 Cons(Nil(), 1068.91/297.07 Cons(Nil(), 1068.91/297.07 Cons(Nil(), 1068.91/297.07 Cons(Nil(), 1068.91/297.07 Cons(Nil(), 1068.91/297.07 Cons(Nil(), 1068.91/297.07 Cons(Nil(), 1068.91/297.07 Cons(Nil(), 1068.91/297.07 Cons(Nil(), 1068.91/297.07 Cons(Nil(), 1068.91/297.07 Cons(Nil(), 1068.91/297.07 Cons(Nil(), 1068.91/297.07 Cons(Nil(), 1068.91/297.07 Cons(Nil(), 1068.91/297.07 Cons(Nil(), 1068.91/297.07 Cons(Nil(), 1068.91/297.07 Cons(Nil(), 1068.91/297.07 Cons(Nil(), 1068.91/297.07 Cons(Nil(), 1068.91/297.07 Cons(Nil(), 1068.91/297.07 Cons(Nil(), 1068.91/297.07 Cons(Nil(), 1068.91/297.07 Nil())))))))))))))))))))))))))))))))))))))))))) 1068.91/297.07 , lt0(x, Nil()) -> False() 1068.91/297.07 , lt0(Cons(x', xs'), Cons(x, xs)) -> lt0(xs', xs) 1068.91/297.07 , number42() -> 1068.91/297.07 Cons(Nil(), 1068.91/297.07 Cons(Nil(), 1068.91/297.07 Cons(Nil(), 1068.91/297.07 Cons(Nil(), 1068.91/297.07 Cons(Nil(), 1068.91/297.07 Cons(Nil(), 1068.91/297.07 Cons(Nil(), 1068.91/297.07 Cons(Nil(), 1068.91/297.07 Cons(Nil(), 1068.91/297.07 Cons(Nil(), 1068.91/297.07 Cons(Nil(), 1068.91/297.07 Cons(Nil(), 1068.91/297.07 Cons(Nil(), 1068.91/297.07 Cons(Nil(), 1068.91/297.07 Cons(Nil(), 1068.91/297.07 Cons(Nil(), 1068.91/297.07 Cons(Nil(), 1068.91/297.07 Cons(Nil(), 1068.91/297.07 Cons(Nil(), 1068.91/297.07 Cons(Nil(), 1068.91/297.07 Cons(Nil(), 1068.91/297.07 Cons(Nil(), 1068.91/297.07 Cons(Nil(), 1068.91/297.07 Cons(Nil(), 1068.91/297.07 Cons(Nil(), 1068.91/297.07 Cons(Nil(), 1068.91/297.07 Cons(Nil(), 1068.91/297.07 Cons(Nil(), 1068.91/297.07 Cons(Nil(), 1068.91/297.08 Cons(Nil(), 1068.91/297.08 Cons(Nil(), 1068.91/297.08 Cons(Nil(), 1068.91/297.08 Cons(Nil(), 1068.91/297.08 Cons(Nil(), 1068.91/297.08 Cons(Nil(), 1068.91/297.08 Cons(Nil(), 1068.91/297.08 Cons(Nil(), 1068.91/297.08 Cons(Nil(), 1068.91/297.08 Cons(Nil(), 1068.91/297.08 Cons(Nil(), 1068.91/297.08 Cons(Nil(), 1068.91/297.08 Cons(Nil(), 1068.91/297.08 Nil())))))))))))))))))))))))))))))))))))))))))) 1068.91/297.08 , goal(x, y) -> Cons(f(x, y), Cons(g(x, y), Nil())) 1068.91/297.08 , g(x, Cons(x', xs)) -> 1068.91/297.08 g[Ite][False][Ite](lt0(x, Cons(Nil(), Nil())), x, Cons(x', xs)) 1068.91/297.08 , g(x, Nil()) -> 1068.91/297.08 Cons(Nil(), 1068.91/297.08 Cons(Nil(), 1068.91/297.08 Cons(Nil(), 1068.91/297.08 Cons(Nil(), 1068.91/297.08 Cons(Nil(), 1068.91/297.08 Cons(Nil(), 1068.91/297.08 Cons(Nil(), 1068.91/297.08 Cons(Nil(), 1068.91/297.08 Cons(Nil(), 1068.91/297.08 Cons(Nil(), 1068.91/297.08 Cons(Nil(), 1068.91/297.08 Cons(Nil(), 1068.91/297.08 Cons(Nil(), 1068.91/297.08 Cons(Nil(), 1068.91/297.08 Cons(Nil(), 1068.91/297.08 Cons(Nil(), 1068.91/297.08 Cons(Nil(), 1068.91/297.08 Cons(Nil(), 1068.91/297.08 Cons(Nil(), 1068.91/297.08 Cons(Nil(), 1068.91/297.08 Cons(Nil(), 1068.91/297.08 Cons(Nil(), 1068.91/297.08 Cons(Nil(), 1068.91/297.08 Cons(Nil(), 1068.91/297.08 Cons(Nil(), 1068.91/297.08 Cons(Nil(), 1068.91/297.08 Cons(Nil(), 1068.91/297.08 Cons(Nil(), 1068.91/297.08 Cons(Nil(), 1068.91/297.08 Cons(Nil(), 1068.91/297.08 Cons(Nil(), 1068.91/297.08 Cons(Nil(), 1068.91/297.08 Cons(Nil(), 1068.91/297.08 Cons(Nil(), 1068.91/297.08 Cons(Nil(), 1068.91/297.08 Cons(Nil(), 1068.91/297.08 Cons(Nil(), 1068.91/297.08 Cons(Nil(), 1068.91/297.08 Cons(Nil(), 1068.91/297.08 Cons(Nil(), 1068.91/297.08 Cons(Nil(), 1068.91/297.08 Cons(Nil(), 1068.91/297.08 Nil())))))))))))))))))))))))))))))))))))))))))) } 1068.91/297.08 Weak Trs: 1068.91/297.08 { f[Ite][False][Ite](True(), x, y) -> x 1068.91/297.08 , f[Ite][False][Ite](True(), x', Cons(x, xs)) -> xs 1068.91/297.08 , f[Ite][False][Ite](False(), x, y) -> Cons(Cons(Nil(), Nil()), y) 1068.91/297.08 , f[Ite][False][Ite](False(), Cons(x, xs), y) -> xs 1068.91/297.08 , g[Ite][False][Ite](True(), x', Cons(x, xs)) -> g(x', xs) 1068.91/297.08 , g[Ite][False][Ite](False(), Cons(x, xs), y) -> 1068.91/297.08 g(xs, Cons(Cons(Nil(), Nil()), y)) } 1068.91/297.08 Obligation: 1068.91/297.08 innermost runtime complexity 1068.91/297.08 Answer: 1068.91/297.08 MAYBE 1068.91/297.08 1068.91/297.08 None of the processors succeeded. 1068.91/297.08 1068.91/297.08 Details of failed attempt(s): 1068.91/297.08 ----------------------------- 1068.91/297.08 1) 'empty' failed due to the following reason: 1068.91/297.08 1068.91/297.08 Empty strict component of the problem is NOT empty. 1068.91/297.08 1068.91/297.08 2) 'Best' failed due to the following reason: 1068.91/297.08 1068.91/297.08 None of the processors succeeded. 1068.91/297.08 1068.91/297.08 Details of failed attempt(s): 1068.91/297.08 ----------------------------- 1068.91/297.08 1) 'With Problem ... (timeout of 297 seconds)' failed due to the 1068.91/297.08 following reason: 1068.91/297.08 1068.91/297.08 Computation stopped due to timeout after 297.0 seconds. 1068.91/297.08 1068.91/297.08 2) 'Best' failed due to the following reason: 1068.91/297.08 1068.91/297.08 None of the processors succeeded. 1068.91/297.08 1068.91/297.08 Details of failed attempt(s): 1068.91/297.08 ----------------------------- 1068.91/297.08 1) 'With Problem ... (timeout of 148 seconds) (timeout of 297 1068.91/297.08 seconds)' failed due to the following reason: 1068.91/297.08 1068.91/297.08 Computation stopped due to timeout after 148.0 seconds. 1068.91/297.08 1068.91/297.08 2) 'Best' failed due to the following reason: 1068.91/297.08 1068.91/297.08 None of the processors succeeded. 1068.91/297.08 1068.91/297.08 Details of failed attempt(s): 1068.91/297.08 ----------------------------- 1068.91/297.08 1) 'Polynomial Path Order (PS) (timeout of 297 seconds)' failed due 1068.91/297.08 to the following reason: 1068.91/297.08 1068.91/297.08 The input cannot be shown compatible 1068.91/297.08 1068.91/297.08 2) 'bsearch-popstar (timeout of 297 seconds)' failed due to the 1068.91/297.08 following reason: 1068.91/297.08 1068.91/297.08 The input cannot be shown compatible 1068.91/297.08 1068.91/297.08 1068.91/297.08 3) 'Fastest (timeout of 24 seconds) (timeout of 297 seconds)' 1068.91/297.08 failed due to the following reason: 1068.91/297.08 1068.91/297.08 None of the processors succeeded. 1068.91/297.08 1068.91/297.08 Details of failed attempt(s): 1068.91/297.08 ----------------------------- 1068.91/297.08 1) 'Bounds with minimal-enrichment and initial automaton 'match'' 1068.91/297.08 failed due to the following reason: 1068.91/297.08 1068.91/297.08 match-boundness of the problem could not be verified. 1068.91/297.08 1068.91/297.08 2) 'Bounds with perSymbol-enrichment and initial automaton 'match'' 1068.91/297.08 failed due to the following reason: 1068.91/297.08 1068.91/297.08 match-boundness of the problem could not be verified. 1068.91/297.08 1068.91/297.08 1068.91/297.08 1068.91/297.08 1068.91/297.08 1068.91/297.08 Arrrr.. 1069.71/297.63 EOF