MAYBE 1139.12/297.11 MAYBE 1139.12/297.11 1139.12/297.11 We are left with following problem, upon which TcT provides the 1139.12/297.11 certificate MAYBE. 1139.12/297.11 1139.12/297.11 Strict Trs: 1139.12/297.11 { active(zeros()) -> mark(cons(0(), zeros())) 1139.12/297.11 , active(U11(tt(), L)) -> mark(U12(tt(), L)) 1139.12/297.11 , active(U12(tt(), L)) -> mark(s(length(L))) 1139.12/297.11 , active(length(cons(N, L))) -> mark(U11(tt(), L)) 1139.12/297.11 , active(length(nil())) -> mark(0()) 1139.12/297.11 , mark(zeros()) -> active(zeros()) 1139.12/297.11 , mark(cons(X1, X2)) -> active(cons(mark(X1), X2)) 1139.12/297.11 , mark(0()) -> active(0()) 1139.12/297.11 , mark(U11(X1, X2)) -> active(U11(mark(X1), X2)) 1139.12/297.11 , mark(tt()) -> active(tt()) 1139.12/297.11 , mark(U12(X1, X2)) -> active(U12(mark(X1), X2)) 1139.12/297.11 , mark(s(X)) -> active(s(mark(X))) 1139.12/297.11 , mark(length(X)) -> active(length(mark(X))) 1139.12/297.11 , mark(nil()) -> active(nil()) 1139.12/297.11 , cons(X1, active(X2)) -> cons(X1, X2) 1139.12/297.11 , cons(X1, mark(X2)) -> cons(X1, X2) 1139.12/297.11 , cons(active(X1), X2) -> cons(X1, X2) 1139.12/297.11 , cons(mark(X1), X2) -> cons(X1, X2) 1139.12/297.11 , U11(X1, active(X2)) -> U11(X1, X2) 1139.12/297.11 , U11(X1, mark(X2)) -> U11(X1, X2) 1139.12/297.11 , U11(active(X1), X2) -> U11(X1, X2) 1139.12/297.11 , U11(mark(X1), X2) -> U11(X1, X2) 1139.12/297.11 , U12(X1, active(X2)) -> U12(X1, X2) 1139.12/297.12 , U12(X1, mark(X2)) -> U12(X1, X2) 1139.12/297.12 , U12(active(X1), X2) -> U12(X1, X2) 1139.12/297.12 , U12(mark(X1), X2) -> U12(X1, X2) 1139.12/297.12 , s(active(X)) -> s(X) 1139.12/297.12 , s(mark(X)) -> s(X) 1139.12/297.12 , length(active(X)) -> length(X) 1139.12/297.12 , length(mark(X)) -> length(X) } 1139.12/297.12 Obligation: 1139.12/297.12 derivational complexity 1139.12/297.12 Answer: 1139.12/297.12 MAYBE 1139.12/297.12 1139.12/297.12 None of the processors succeeded. 1139.12/297.12 1139.12/297.12 Details of failed attempt(s): 1139.12/297.12 ----------------------------- 1139.12/297.12 1) 'Inspecting Problem... (timeout of 297 seconds)' failed due to 1139.12/297.12 the following reason: 1139.12/297.12 1139.12/297.12 Computation stopped due to timeout after 297.0 seconds. 1139.12/297.12 1139.12/297.12 2) 'iteProgress (timeout of 297 seconds)' failed due to the 1139.12/297.12 following reason: 1139.12/297.12 1139.12/297.12 Fail 1139.12/297.12 1139.12/297.12 3) 'Fastest (timeout of 60 seconds)' failed due to the following 1139.12/297.12 reason: 1139.12/297.12 1139.12/297.12 Computation stopped due to timeout after 60.0 seconds. 1139.12/297.12 1139.12/297.12 4) 'bsearch-matrix (timeout of 297 seconds)' failed due to the 1139.12/297.12 following reason: 1139.12/297.12 1139.12/297.12 The input cannot be shown compatible 1139.12/297.12 1139.12/297.12 1139.12/297.12 Arrrr.. 1139.29/297.21 EOF