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