MAYBE 1161.77/297.04 MAYBE 1161.77/297.04 1161.77/297.04 We are left with following problem, upon which TcT provides the 1161.77/297.04 certificate MAYBE. 1161.77/297.04 1161.77/297.04 Strict Trs: 1161.77/297.04 { a(l, x, s(y), h()) -> a(l, x, y, s(h())) 1161.77/297.04 , a(l, x, s(y), s(z)) -> a(l, x, y, a(l, x, s(y), z)) 1161.77/297.04 , a(l, s(x), h(), z) -> a(l, x, z, z) 1161.77/297.04 , a(h(), h(), h(), x) -> s(x) 1161.77/297.04 , a(s(l), h(), h(), z) -> a(l, z, h(), z) 1161.77/297.04 , s(h()) -> 1() 1161.77/297.04 , +(x, h()) -> x 1161.77/297.04 , +(h(), x) -> x 1161.77/297.04 , +(s(x), s(y)) -> s(s(+(x, y))) 1161.77/297.04 , +(+(x, y), z) -> +(x, +(y, z)) 1161.77/297.04 , app(l, nil()) -> l 1161.77/297.04 , app(nil(), k) -> k 1161.77/297.04 , app(cons(x, l), k) -> cons(x, app(l, k)) 1161.77/297.04 , sum(cons(x, nil())) -> cons(x, nil()) 1161.77/297.04 , sum(cons(x, cons(y, l))) -> sum(cons(a(x, y, h(), h()), l)) } 1161.77/297.04 Obligation: 1161.77/297.04 innermost runtime complexity 1161.77/297.04 Answer: 1161.77/297.04 MAYBE 1161.77/297.04 1161.77/297.04 None of the processors succeeded. 1161.77/297.04 1161.77/297.04 Details of failed attempt(s): 1161.77/297.04 ----------------------------- 1161.77/297.04 1) 'empty' failed due to the following reason: 1161.77/297.04 1161.77/297.04 Empty strict component of the problem is NOT empty. 1161.77/297.04 1161.77/297.04 2) 'Best' failed due to the following reason: 1161.77/297.04 1161.77/297.04 None of the processors succeeded. 1161.77/297.04 1161.77/297.04 Details of failed attempt(s): 1161.77/297.04 ----------------------------- 1161.77/297.04 1) 'With Problem ... (timeout of 297 seconds)' failed due to the 1161.77/297.04 following reason: 1161.77/297.04 1161.77/297.04 Computation stopped due to timeout after 297.0 seconds. 1161.77/297.04 1161.77/297.04 2) 'Best' failed due to the following reason: 1161.77/297.04 1161.77/297.04 None of the processors succeeded. 1161.77/297.04 1161.77/297.04 Details of failed attempt(s): 1161.77/297.04 ----------------------------- 1161.77/297.04 1) 'With Problem ... (timeout of 148 seconds) (timeout of 297 1161.77/297.04 seconds)' failed due to the following reason: 1161.77/297.04 1161.77/297.04 Computation stopped due to timeout after 148.0 seconds. 1161.77/297.04 1161.77/297.04 2) 'Best' failed due to the following reason: 1161.77/297.04 1161.77/297.04 None of the processors succeeded. 1161.77/297.04 1161.77/297.04 Details of failed attempt(s): 1161.77/297.04 ----------------------------- 1161.77/297.04 1) 'bsearch-popstar (timeout of 297 seconds)' failed due to the 1161.77/297.04 following reason: 1161.77/297.04 1161.77/297.04 The input cannot be shown compatible 1161.77/297.04 1161.77/297.04 2) 'Polynomial Path Order (PS) (timeout of 297 seconds)' failed due 1161.77/297.04 to the following reason: 1161.77/297.04 1161.77/297.04 The input cannot be shown compatible 1161.77/297.04 1161.77/297.04 1161.77/297.04 3) 'Fastest (timeout of 24 seconds) (timeout of 297 seconds)' 1161.77/297.04 failed due to the following reason: 1161.77/297.04 1161.77/297.04 None of the processors succeeded. 1161.77/297.04 1161.77/297.04 Details of failed attempt(s): 1161.77/297.04 ----------------------------- 1161.77/297.04 1) 'Bounds with perSymbol-enrichment and initial automaton 'match'' 1161.77/297.04 failed due to the following reason: 1161.77/297.04 1161.77/297.04 match-boundness of the problem could not be verified. 1161.77/297.04 1161.77/297.04 2) 'Bounds with minimal-enrichment and initial automaton 'match'' 1161.77/297.04 failed due to the following reason: 1161.77/297.04 1161.77/297.04 match-boundness of the problem could not be verified. 1161.77/297.04 1161.77/297.04 1161.77/297.04 1161.77/297.04 1161.77/297.04 1161.77/297.04 Arrrr.. 1163.41/297.84 EOF