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