MAYBE 920.72/297.13 MAYBE 920.72/297.13 920.72/297.13 We are left with following problem, upon which TcT provides the 920.72/297.13 certificate MAYBE. 920.72/297.13 920.72/297.13 Strict Trs: 920.72/297.13 { active(zeros()) -> mark(cons(0(), zeros())) 920.72/297.13 , active(cons(X1, X2)) -> cons(active(X1), X2) 920.72/297.13 , active(tail(X)) -> tail(active(X)) 920.72/297.13 , active(tail(cons(X, XS))) -> mark(XS) 920.72/297.13 , cons(mark(X1), X2) -> mark(cons(X1, X2)) 920.72/297.13 , cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)) 920.72/297.13 , tail(mark(X)) -> mark(tail(X)) 920.72/297.13 , tail(ok(X)) -> ok(tail(X)) 920.72/297.13 , proper(zeros()) -> ok(zeros()) 920.72/297.13 , proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)) 920.72/297.13 , proper(0()) -> ok(0()) 920.72/297.13 , proper(tail(X)) -> tail(proper(X)) 920.72/297.13 , top(mark(X)) -> top(proper(X)) 920.72/297.13 , top(ok(X)) -> top(active(X)) } 920.72/297.13 Obligation: 920.72/297.13 derivational complexity 920.72/297.13 Answer: 920.72/297.13 MAYBE 920.72/297.13 920.72/297.13 None of the processors succeeded. 920.72/297.13 920.72/297.13 Details of failed attempt(s): 920.72/297.13 ----------------------------- 920.72/297.13 1) 'Inspecting Problem... (timeout of 297 seconds)' failed due to 920.72/297.13 the following reason: 920.72/297.13 920.72/297.13 Computation stopped due to timeout after 297.0 seconds. 920.72/297.13 920.72/297.13 2) 'Fastest (timeout of 60 seconds)' failed due to the following 920.72/297.13 reason: 920.72/297.13 920.72/297.13 Computation stopped due to timeout after 60.0 seconds. 920.72/297.13 920.72/297.13 3) 'iteProgress (timeout of 297 seconds)' failed due to the 920.72/297.13 following reason: 920.72/297.13 920.72/297.13 Fail 920.72/297.13 920.72/297.13 4) 'bsearch-matrix (timeout of 297 seconds)' failed due to the 920.72/297.13 following reason: 920.72/297.13 920.72/297.13 The input cannot be shown compatible 920.72/297.13 920.72/297.13 920.72/297.13 Arrrr.. 920.72/297.16 EOF