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