MAYBE 896.74/297.08 MAYBE 896.74/297.08 896.74/297.08 We are left with following problem, upon which TcT provides the 896.74/297.08 certificate MAYBE. 896.74/297.08 896.74/297.08 Strict Trs: 896.74/297.08 { active(__(X1, X2)) -> __(X1, active(X2)) 896.74/297.08 , active(__(X1, X2)) -> __(active(X1), X2) 896.74/297.08 , active(__(X, nil())) -> mark(X) 896.74/297.08 , active(__(__(X, Y), Z)) -> mark(__(X, __(Y, Z))) 896.74/297.08 , active(__(nil(), X)) -> mark(X) 896.74/297.08 , active(U11(X1, X2)) -> U11(active(X1), X2) 896.74/297.08 , active(U11(tt(), V)) -> mark(U12(isNeList(V))) 896.74/297.08 , active(U12(X)) -> U12(active(X)) 896.74/297.08 , active(U12(tt())) -> mark(tt()) 896.74/297.08 , active(isNeList(V)) -> mark(U31(isPalListKind(V), V)) 896.74/297.08 , active(isNeList(__(V1, V2))) -> 896.74/297.08 mark(U41(and(isPalListKind(V1), isPalListKind(V2)), V1, V2)) 896.74/297.08 , active(isNeList(__(V1, V2))) -> 896.74/297.08 mark(U51(and(isPalListKind(V1), isPalListKind(V2)), V1, V2)) 896.74/297.08 , active(U21(X1, X2, X3)) -> U21(active(X1), X2, X3) 896.74/297.08 , active(U21(tt(), V1, V2)) -> mark(U22(isList(V1), V2)) 896.74/297.08 , active(U22(X1, X2)) -> U22(active(X1), X2) 896.74/297.08 , active(U22(tt(), V2)) -> mark(U23(isList(V2))) 896.74/297.08 , active(isList(V)) -> mark(U11(isPalListKind(V), V)) 896.74/297.08 , active(isList(__(V1, V2))) -> 896.74/297.08 mark(U21(and(isPalListKind(V1), isPalListKind(V2)), V1, V2)) 896.74/297.08 , active(isList(nil())) -> mark(tt()) 896.74/297.08 , active(U23(X)) -> U23(active(X)) 896.74/297.08 , active(U23(tt())) -> mark(tt()) 896.74/297.08 , active(U31(X1, X2)) -> U31(active(X1), X2) 896.74/297.08 , active(U31(tt(), V)) -> mark(U32(isQid(V))) 896.74/297.08 , active(U32(X)) -> U32(active(X)) 896.74/297.08 , active(U32(tt())) -> mark(tt()) 896.74/297.08 , active(isQid(a())) -> mark(tt()) 896.74/297.08 , active(isQid(e())) -> mark(tt()) 896.74/297.08 , active(isQid(i())) -> mark(tt()) 896.74/297.08 , active(isQid(o())) -> mark(tt()) 896.74/297.08 , active(isQid(u())) -> mark(tt()) 896.74/297.08 , active(U41(X1, X2, X3)) -> U41(active(X1), X2, X3) 896.74/297.08 , active(U41(tt(), V1, V2)) -> mark(U42(isList(V1), V2)) 896.74/297.08 , active(U42(X1, X2)) -> U42(active(X1), X2) 896.74/297.08 , active(U42(tt(), V2)) -> mark(U43(isNeList(V2))) 896.74/297.08 , active(U43(X)) -> U43(active(X)) 896.74/297.08 , active(U43(tt())) -> mark(tt()) 896.74/297.08 , active(U51(X1, X2, X3)) -> U51(active(X1), X2, X3) 896.74/297.08 , active(U51(tt(), V1, V2)) -> mark(U52(isNeList(V1), V2)) 896.74/297.08 , active(U52(X1, X2)) -> U52(active(X1), X2) 896.74/297.08 , active(U52(tt(), V2)) -> mark(U53(isList(V2))) 896.74/297.08 , active(U53(X)) -> U53(active(X)) 896.74/297.08 , active(U53(tt())) -> mark(tt()) 896.74/297.08 , active(U61(X1, X2)) -> U61(active(X1), X2) 896.74/297.08 , active(U61(tt(), V)) -> mark(U62(isQid(V))) 896.74/297.08 , active(U62(X)) -> U62(active(X)) 896.74/297.08 , active(U62(tt())) -> mark(tt()) 896.74/297.08 , active(U71(X1, X2)) -> U71(active(X1), X2) 896.74/297.08 , active(U71(tt(), V)) -> mark(U72(isNePal(V))) 896.74/297.08 , active(U72(X)) -> U72(active(X)) 896.74/297.08 , active(U72(tt())) -> mark(tt()) 896.74/297.08 , active(isNePal(V)) -> mark(U61(isPalListKind(V), V)) 896.74/297.08 , active(isNePal(__(I, __(P, I)))) -> 896.74/297.08 mark(and(and(isQid(I), isPalListKind(I)), 896.74/297.08 and(isPal(P), isPalListKind(P)))) 896.74/297.08 , active(and(X1, X2)) -> and(active(X1), X2) 896.74/297.08 , active(and(tt(), X)) -> mark(X) 896.74/297.08 , active(isPalListKind(__(V1, V2))) -> 896.74/297.08 mark(and(isPalListKind(V1), isPalListKind(V2))) 896.74/297.08 , active(isPalListKind(nil())) -> mark(tt()) 896.74/297.08 , active(isPalListKind(a())) -> mark(tt()) 896.74/297.08 , active(isPalListKind(e())) -> mark(tt()) 896.74/297.08 , active(isPalListKind(i())) -> mark(tt()) 896.74/297.08 , active(isPalListKind(o())) -> mark(tt()) 896.74/297.08 , active(isPalListKind(u())) -> mark(tt()) 896.74/297.08 , active(isPal(V)) -> mark(U71(isPalListKind(V), V)) 896.74/297.08 , active(isPal(nil())) -> mark(tt()) 896.74/297.08 , __(X1, mark(X2)) -> mark(__(X1, X2)) 896.74/297.08 , __(mark(X1), X2) -> mark(__(X1, X2)) 896.74/297.08 , __(ok(X1), ok(X2)) -> ok(__(X1, X2)) 896.74/297.08 , U11(mark(X1), X2) -> mark(U11(X1, X2)) 896.74/297.08 , U11(ok(X1), ok(X2)) -> ok(U11(X1, X2)) 896.74/297.08 , U12(mark(X)) -> mark(U12(X)) 896.74/297.08 , U12(ok(X)) -> ok(U12(X)) 896.74/297.08 , isNeList(ok(X)) -> ok(isNeList(X)) 896.74/297.08 , U21(mark(X1), X2, X3) -> mark(U21(X1, X2, X3)) 896.74/297.08 , U21(ok(X1), ok(X2), ok(X3)) -> ok(U21(X1, X2, X3)) 896.74/297.08 , U22(mark(X1), X2) -> mark(U22(X1, X2)) 896.74/297.08 , U22(ok(X1), ok(X2)) -> ok(U22(X1, X2)) 896.74/297.08 , isList(ok(X)) -> ok(isList(X)) 896.74/297.08 , U23(mark(X)) -> mark(U23(X)) 896.74/297.08 , U23(ok(X)) -> ok(U23(X)) 896.74/297.08 , U31(mark(X1), X2) -> mark(U31(X1, X2)) 896.74/297.08 , U31(ok(X1), ok(X2)) -> ok(U31(X1, X2)) 896.74/297.08 , U32(mark(X)) -> mark(U32(X)) 896.74/297.08 , U32(ok(X)) -> ok(U32(X)) 896.74/297.08 , isQid(ok(X)) -> ok(isQid(X)) 896.74/297.08 , U41(mark(X1), X2, X3) -> mark(U41(X1, X2, X3)) 896.74/297.08 , U41(ok(X1), ok(X2), ok(X3)) -> ok(U41(X1, X2, X3)) 896.74/297.08 , U42(mark(X1), X2) -> mark(U42(X1, X2)) 896.74/297.08 , U42(ok(X1), ok(X2)) -> ok(U42(X1, X2)) 896.74/297.08 , U43(mark(X)) -> mark(U43(X)) 896.74/297.08 , U43(ok(X)) -> ok(U43(X)) 896.74/297.08 , U51(mark(X1), X2, X3) -> mark(U51(X1, X2, X3)) 896.74/297.08 , U51(ok(X1), ok(X2), ok(X3)) -> ok(U51(X1, X2, X3)) 896.74/297.08 , U52(mark(X1), X2) -> mark(U52(X1, X2)) 896.74/297.08 , U52(ok(X1), ok(X2)) -> ok(U52(X1, X2)) 896.74/297.08 , U53(mark(X)) -> mark(U53(X)) 896.74/297.08 , U53(ok(X)) -> ok(U53(X)) 896.74/297.08 , U61(mark(X1), X2) -> mark(U61(X1, X2)) 896.74/297.08 , U61(ok(X1), ok(X2)) -> ok(U61(X1, X2)) 896.74/297.08 , U62(mark(X)) -> mark(U62(X)) 896.74/297.08 , U62(ok(X)) -> ok(U62(X)) 896.74/297.08 , U71(mark(X1), X2) -> mark(U71(X1, X2)) 896.74/297.08 , U71(ok(X1), ok(X2)) -> ok(U71(X1, X2)) 896.74/297.08 , U72(mark(X)) -> mark(U72(X)) 896.74/297.08 , U72(ok(X)) -> ok(U72(X)) 896.74/297.08 , isNePal(ok(X)) -> ok(isNePal(X)) 896.74/297.08 , and(mark(X1), X2) -> mark(and(X1, X2)) 896.74/297.08 , and(ok(X1), ok(X2)) -> ok(and(X1, X2)) 896.74/297.08 , isPalListKind(ok(X)) -> ok(isPalListKind(X)) 896.74/297.08 , isPal(ok(X)) -> ok(isPal(X)) 896.74/297.08 , proper(__(X1, X2)) -> __(proper(X1), proper(X2)) 896.74/297.08 , proper(nil()) -> ok(nil()) 896.74/297.08 , proper(U11(X1, X2)) -> U11(proper(X1), proper(X2)) 896.74/297.08 , proper(tt()) -> ok(tt()) 896.74/297.08 , proper(U12(X)) -> U12(proper(X)) 896.74/297.08 , proper(isNeList(X)) -> isNeList(proper(X)) 896.74/297.08 , proper(U21(X1, X2, X3)) -> 896.74/297.08 U21(proper(X1), proper(X2), proper(X3)) 896.74/297.08 , proper(U22(X1, X2)) -> U22(proper(X1), proper(X2)) 896.74/297.08 , proper(isList(X)) -> isList(proper(X)) 896.74/297.08 , proper(U23(X)) -> U23(proper(X)) 896.74/297.08 , proper(U31(X1, X2)) -> U31(proper(X1), proper(X2)) 896.74/297.08 , proper(U32(X)) -> U32(proper(X)) 896.74/297.08 , proper(isQid(X)) -> isQid(proper(X)) 896.74/297.08 , proper(U41(X1, X2, X3)) -> 896.74/297.08 U41(proper(X1), proper(X2), proper(X3)) 896.74/297.08 , proper(U42(X1, X2)) -> U42(proper(X1), proper(X2)) 896.74/297.08 , proper(U43(X)) -> U43(proper(X)) 896.74/297.08 , proper(U51(X1, X2, X3)) -> 896.74/297.08 U51(proper(X1), proper(X2), proper(X3)) 896.74/297.08 , proper(U52(X1, X2)) -> U52(proper(X1), proper(X2)) 896.74/297.08 , proper(U53(X)) -> U53(proper(X)) 896.74/297.08 , proper(U61(X1, X2)) -> U61(proper(X1), proper(X2)) 896.74/297.08 , proper(U62(X)) -> U62(proper(X)) 896.74/297.08 , proper(U71(X1, X2)) -> U71(proper(X1), proper(X2)) 896.74/297.08 , proper(U72(X)) -> U72(proper(X)) 896.74/297.08 , proper(isNePal(X)) -> isNePal(proper(X)) 896.74/297.08 , proper(and(X1, X2)) -> and(proper(X1), proper(X2)) 896.74/297.08 , proper(isPalListKind(X)) -> isPalListKind(proper(X)) 896.74/297.08 , proper(isPal(X)) -> isPal(proper(X)) 896.74/297.08 , proper(a()) -> ok(a()) 896.74/297.08 , proper(e()) -> ok(e()) 896.74/297.08 , proper(i()) -> ok(i()) 896.74/297.08 , proper(o()) -> ok(o()) 896.74/297.08 , proper(u()) -> ok(u()) 896.74/297.08 , top(mark(X)) -> top(proper(X)) 896.74/297.08 , top(ok(X)) -> top(active(X)) } 896.74/297.08 Obligation: 896.74/297.08 runtime complexity 896.74/297.08 Answer: 896.74/297.08 MAYBE 896.74/297.08 896.74/297.08 None of the processors succeeded. 896.74/297.08 896.74/297.08 Details of failed attempt(s): 896.74/297.08 ----------------------------- 896.74/297.08 1) 'With Problem ... (timeout of 297 seconds)' failed due to the 896.74/297.08 following reason: 896.74/297.08 896.74/297.08 Computation stopped due to timeout after 297.0 seconds. 896.74/297.08 896.74/297.08 2) 'Best' failed due to the following reason: 896.74/297.08 896.74/297.08 None of the processors succeeded. 896.74/297.08 896.74/297.08 Details of failed attempt(s): 896.74/297.08 ----------------------------- 896.74/297.08 1) 'With Problem ... (timeout of 148 seconds) (timeout of 297 896.74/297.08 seconds)' failed due to the following reason: 896.74/297.08 896.74/297.08 Computation stopped due to timeout after 148.0 seconds. 896.74/297.08 896.74/297.08 2) 'Best' failed due to the following reason: 896.74/297.08 896.74/297.08 None of the processors succeeded. 896.74/297.08 896.74/297.08 Details of failed attempt(s): 896.74/297.08 ----------------------------- 896.74/297.08 1) 'bsearch-popstar (timeout of 297 seconds)' failed due to the 896.74/297.08 following reason: 896.74/297.08 896.74/297.08 The processor is inapplicable, reason: 896.74/297.08 Processor only applicable for innermost runtime complexity analysis 896.74/297.08 896.74/297.08 2) 'Polynomial Path Order (PS) (timeout of 297 seconds)' failed due 896.74/297.08 to the following reason: 896.74/297.08 896.74/297.08 The processor is inapplicable, reason: 896.74/297.08 Processor only applicable for innermost runtime complexity analysis 896.74/297.08 896.74/297.08 896.74/297.08 3) 'Fastest (timeout of 24 seconds) (timeout of 297 seconds)' 896.74/297.08 failed due to the following reason: 896.74/297.08 896.74/297.08 None of the processors succeeded. 896.74/297.08 896.74/297.08 Details of failed attempt(s): 896.74/297.08 ----------------------------- 896.74/297.08 1) 'Bounds with minimal-enrichment and initial automaton 'match'' 896.74/297.09 failed due to the following reason: 896.74/297.09 896.74/297.09 match-boundness of the problem could not be verified. 896.74/297.09 896.74/297.09 2) 'Bounds with perSymbol-enrichment and initial automaton 'match'' 896.74/297.09 failed due to the following reason: 896.74/297.09 896.74/297.09 match-boundness of the problem could not be verified. 896.74/297.09 896.74/297.09 896.74/297.09 896.74/297.09 3) 'Weak Dependency Pairs (timeout of 297 seconds)' failed due to 896.74/297.09 the following reason: 896.74/297.09 896.74/297.09 We add the following weak dependency pairs: 896.74/297.09 896.74/297.09 Strict DPs: 896.74/297.09 { active^#(__(X1, X2)) -> c_1(__^#(X1, active(X2))) 896.74/297.09 , active^#(__(X1, X2)) -> c_2(__^#(active(X1), X2)) 896.74/297.09 , active^#(__(X, nil())) -> c_3(X) 896.74/297.09 , active^#(__(__(X, Y), Z)) -> c_4(__^#(X, __(Y, Z))) 896.74/297.09 , active^#(__(nil(), X)) -> c_5(X) 896.74/297.09 , active^#(U11(X1, X2)) -> c_6(U11^#(active(X1), X2)) 896.74/297.09 , active^#(U11(tt(), V)) -> c_7(U12^#(isNeList(V))) 896.74/297.09 , active^#(U12(X)) -> c_8(U12^#(active(X))) 896.74/297.09 , active^#(U12(tt())) -> c_9() 896.74/297.09 , active^#(isNeList(V)) -> c_10(U31^#(isPalListKind(V), V)) 896.74/297.09 , active^#(isNeList(__(V1, V2))) -> 896.74/297.09 c_11(U41^#(and(isPalListKind(V1), isPalListKind(V2)), V1, V2)) 896.74/297.09 , active^#(isNeList(__(V1, V2))) -> 896.74/297.09 c_12(U51^#(and(isPalListKind(V1), isPalListKind(V2)), V1, V2)) 896.74/297.09 , active^#(U21(X1, X2, X3)) -> c_13(U21^#(active(X1), X2, X3)) 896.74/297.09 , active^#(U21(tt(), V1, V2)) -> c_14(U22^#(isList(V1), V2)) 896.74/297.09 , active^#(U22(X1, X2)) -> c_15(U22^#(active(X1), X2)) 896.74/297.09 , active^#(U22(tt(), V2)) -> c_16(U23^#(isList(V2))) 896.74/297.09 , active^#(isList(V)) -> c_17(U11^#(isPalListKind(V), V)) 896.74/297.09 , active^#(isList(__(V1, V2))) -> 896.74/297.09 c_18(U21^#(and(isPalListKind(V1), isPalListKind(V2)), V1, V2)) 896.74/297.09 , active^#(isList(nil())) -> c_19() 896.74/297.09 , active^#(U23(X)) -> c_20(U23^#(active(X))) 896.74/297.09 , active^#(U23(tt())) -> c_21() 896.74/297.09 , active^#(U31(X1, X2)) -> c_22(U31^#(active(X1), X2)) 896.74/297.09 , active^#(U31(tt(), V)) -> c_23(U32^#(isQid(V))) 896.74/297.09 , active^#(U32(X)) -> c_24(U32^#(active(X))) 896.74/297.09 , active^#(U32(tt())) -> c_25() 896.74/297.09 , active^#(isQid(a())) -> c_26() 896.74/297.09 , active^#(isQid(e())) -> c_27() 896.74/297.09 , active^#(isQid(i())) -> c_28() 896.74/297.09 , active^#(isQid(o())) -> c_29() 896.74/297.09 , active^#(isQid(u())) -> c_30() 896.74/297.09 , active^#(U41(X1, X2, X3)) -> c_31(U41^#(active(X1), X2, X3)) 896.74/297.09 , active^#(U41(tt(), V1, V2)) -> c_32(U42^#(isList(V1), V2)) 896.74/297.09 , active^#(U42(X1, X2)) -> c_33(U42^#(active(X1), X2)) 896.74/297.09 , active^#(U42(tt(), V2)) -> c_34(U43^#(isNeList(V2))) 896.74/297.09 , active^#(U43(X)) -> c_35(U43^#(active(X))) 896.74/297.09 , active^#(U43(tt())) -> c_36() 896.74/297.09 , active^#(U51(X1, X2, X3)) -> c_37(U51^#(active(X1), X2, X3)) 896.74/297.09 , active^#(U51(tt(), V1, V2)) -> c_38(U52^#(isNeList(V1), V2)) 896.74/297.09 , active^#(U52(X1, X2)) -> c_39(U52^#(active(X1), X2)) 896.74/297.09 , active^#(U52(tt(), V2)) -> c_40(U53^#(isList(V2))) 896.74/297.09 , active^#(U53(X)) -> c_41(U53^#(active(X))) 896.74/297.09 , active^#(U53(tt())) -> c_42() 896.74/297.09 , active^#(U61(X1, X2)) -> c_43(U61^#(active(X1), X2)) 896.74/297.09 , active^#(U61(tt(), V)) -> c_44(U62^#(isQid(V))) 896.74/297.09 , active^#(U62(X)) -> c_45(U62^#(active(X))) 896.74/297.09 , active^#(U62(tt())) -> c_46() 896.74/297.09 , active^#(U71(X1, X2)) -> c_47(U71^#(active(X1), X2)) 896.74/297.09 , active^#(U71(tt(), V)) -> c_48(U72^#(isNePal(V))) 896.74/297.09 , active^#(U72(X)) -> c_49(U72^#(active(X))) 896.74/297.09 , active^#(U72(tt())) -> c_50() 896.74/297.09 , active^#(isNePal(V)) -> c_51(U61^#(isPalListKind(V), V)) 896.74/297.09 , active^#(isNePal(__(I, __(P, I)))) -> 896.74/297.09 c_52(and^#(and(isQid(I), isPalListKind(I)), 896.74/297.09 and(isPal(P), isPalListKind(P)))) 896.74/297.09 , active^#(and(X1, X2)) -> c_53(and^#(active(X1), X2)) 896.74/297.09 , active^#(and(tt(), X)) -> c_54(X) 896.74/297.09 , active^#(isPalListKind(__(V1, V2))) -> 896.74/297.09 c_55(and^#(isPalListKind(V1), isPalListKind(V2))) 896.74/297.09 , active^#(isPalListKind(nil())) -> c_56() 896.74/297.09 , active^#(isPalListKind(a())) -> c_57() 896.74/297.09 , active^#(isPalListKind(e())) -> c_58() 896.74/297.09 , active^#(isPalListKind(i())) -> c_59() 896.74/297.09 , active^#(isPalListKind(o())) -> c_60() 896.74/297.09 , active^#(isPalListKind(u())) -> c_61() 896.74/297.09 , active^#(isPal(V)) -> c_62(U71^#(isPalListKind(V), V)) 896.74/297.09 , active^#(isPal(nil())) -> c_63() 896.74/297.09 , __^#(X1, mark(X2)) -> c_64(__^#(X1, X2)) 896.74/297.09 , __^#(mark(X1), X2) -> c_65(__^#(X1, X2)) 896.74/297.09 , __^#(ok(X1), ok(X2)) -> c_66(__^#(X1, X2)) 896.74/297.09 , U11^#(mark(X1), X2) -> c_67(U11^#(X1, X2)) 896.74/297.09 , U11^#(ok(X1), ok(X2)) -> c_68(U11^#(X1, X2)) 896.74/297.09 , U12^#(mark(X)) -> c_69(U12^#(X)) 896.74/297.09 , U12^#(ok(X)) -> c_70(U12^#(X)) 896.74/297.09 , U31^#(mark(X1), X2) -> c_79(U31^#(X1, X2)) 896.74/297.09 , U31^#(ok(X1), ok(X2)) -> c_80(U31^#(X1, X2)) 896.74/297.09 , U41^#(mark(X1), X2, X3) -> c_84(U41^#(X1, X2, X3)) 896.74/297.09 , U41^#(ok(X1), ok(X2), ok(X3)) -> c_85(U41^#(X1, X2, X3)) 896.74/297.09 , U51^#(mark(X1), X2, X3) -> c_90(U51^#(X1, X2, X3)) 896.74/297.09 , U51^#(ok(X1), ok(X2), ok(X3)) -> c_91(U51^#(X1, X2, X3)) 896.74/297.09 , U21^#(mark(X1), X2, X3) -> c_72(U21^#(X1, X2, X3)) 896.74/297.09 , U21^#(ok(X1), ok(X2), ok(X3)) -> c_73(U21^#(X1, X2, X3)) 896.74/297.09 , U22^#(mark(X1), X2) -> c_74(U22^#(X1, X2)) 896.74/297.09 , U22^#(ok(X1), ok(X2)) -> c_75(U22^#(X1, X2)) 896.74/297.09 , U23^#(mark(X)) -> c_77(U23^#(X)) 896.74/297.09 , U23^#(ok(X)) -> c_78(U23^#(X)) 896.74/297.09 , U32^#(mark(X)) -> c_81(U32^#(X)) 896.74/297.09 , U32^#(ok(X)) -> c_82(U32^#(X)) 896.74/297.09 , U42^#(mark(X1), X2) -> c_86(U42^#(X1, X2)) 896.74/297.09 , U42^#(ok(X1), ok(X2)) -> c_87(U42^#(X1, X2)) 896.74/297.09 , U43^#(mark(X)) -> c_88(U43^#(X)) 896.74/297.09 , U43^#(ok(X)) -> c_89(U43^#(X)) 896.74/297.09 , U52^#(mark(X1), X2) -> c_92(U52^#(X1, X2)) 896.74/297.09 , U52^#(ok(X1), ok(X2)) -> c_93(U52^#(X1, X2)) 896.74/297.09 , U53^#(mark(X)) -> c_94(U53^#(X)) 896.74/297.09 , U53^#(ok(X)) -> c_95(U53^#(X)) 896.74/297.09 , U61^#(mark(X1), X2) -> c_96(U61^#(X1, X2)) 896.74/297.09 , U61^#(ok(X1), ok(X2)) -> c_97(U61^#(X1, X2)) 896.74/297.09 , U62^#(mark(X)) -> c_98(U62^#(X)) 896.74/297.09 , U62^#(ok(X)) -> c_99(U62^#(X)) 896.74/297.09 , U71^#(mark(X1), X2) -> c_100(U71^#(X1, X2)) 896.74/297.09 , U71^#(ok(X1), ok(X2)) -> c_101(U71^#(X1, X2)) 896.74/297.09 , U72^#(mark(X)) -> c_102(U72^#(X)) 896.74/297.09 , U72^#(ok(X)) -> c_103(U72^#(X)) 896.74/297.09 , and^#(mark(X1), X2) -> c_105(and^#(X1, X2)) 896.74/297.09 , and^#(ok(X1), ok(X2)) -> c_106(and^#(X1, X2)) 896.74/297.09 , isNeList^#(ok(X)) -> c_71(isNeList^#(X)) 896.74/297.09 , isList^#(ok(X)) -> c_76(isList^#(X)) 896.74/297.09 , isQid^#(ok(X)) -> c_83(isQid^#(X)) 896.74/297.09 , isNePal^#(ok(X)) -> c_104(isNePal^#(X)) 896.74/297.09 , isPalListKind^#(ok(X)) -> c_107(isPalListKind^#(X)) 896.74/297.09 , isPal^#(ok(X)) -> c_108(isPal^#(X)) 896.74/297.09 , proper^#(__(X1, X2)) -> c_109(__^#(proper(X1), proper(X2))) 896.74/297.09 , proper^#(nil()) -> c_110() 896.74/297.09 , proper^#(U11(X1, X2)) -> c_111(U11^#(proper(X1), proper(X2))) 896.74/297.09 , proper^#(tt()) -> c_112() 896.74/297.09 , proper^#(U12(X)) -> c_113(U12^#(proper(X))) 896.74/297.09 , proper^#(isNeList(X)) -> c_114(isNeList^#(proper(X))) 896.74/297.09 , proper^#(U21(X1, X2, X3)) -> 896.74/297.09 c_115(U21^#(proper(X1), proper(X2), proper(X3))) 896.74/297.09 , proper^#(U22(X1, X2)) -> c_116(U22^#(proper(X1), proper(X2))) 896.74/297.09 , proper^#(isList(X)) -> c_117(isList^#(proper(X))) 896.74/297.09 , proper^#(U23(X)) -> c_118(U23^#(proper(X))) 896.74/297.09 , proper^#(U31(X1, X2)) -> c_119(U31^#(proper(X1), proper(X2))) 896.74/297.09 , proper^#(U32(X)) -> c_120(U32^#(proper(X))) 896.74/297.09 , proper^#(isQid(X)) -> c_121(isQid^#(proper(X))) 896.74/297.09 , proper^#(U41(X1, X2, X3)) -> 896.74/297.09 c_122(U41^#(proper(X1), proper(X2), proper(X3))) 896.74/297.09 , proper^#(U42(X1, X2)) -> c_123(U42^#(proper(X1), proper(X2))) 896.74/297.09 , proper^#(U43(X)) -> c_124(U43^#(proper(X))) 896.74/297.09 , proper^#(U51(X1, X2, X3)) -> 896.74/297.09 c_125(U51^#(proper(X1), proper(X2), proper(X3))) 896.74/297.09 , proper^#(U52(X1, X2)) -> c_126(U52^#(proper(X1), proper(X2))) 896.74/297.09 , proper^#(U53(X)) -> c_127(U53^#(proper(X))) 896.74/297.09 , proper^#(U61(X1, X2)) -> c_128(U61^#(proper(X1), proper(X2))) 896.74/297.09 , proper^#(U62(X)) -> c_129(U62^#(proper(X))) 896.74/297.09 , proper^#(U71(X1, X2)) -> c_130(U71^#(proper(X1), proper(X2))) 896.74/297.09 , proper^#(U72(X)) -> c_131(U72^#(proper(X))) 896.74/297.09 , proper^#(isNePal(X)) -> c_132(isNePal^#(proper(X))) 896.74/297.09 , proper^#(and(X1, X2)) -> c_133(and^#(proper(X1), proper(X2))) 896.74/297.09 , proper^#(isPalListKind(X)) -> c_134(isPalListKind^#(proper(X))) 896.74/297.09 , proper^#(isPal(X)) -> c_135(isPal^#(proper(X))) 896.74/297.09 , proper^#(a()) -> c_136() 896.74/297.09 , proper^#(e()) -> c_137() 896.74/297.09 , proper^#(i()) -> c_138() 896.74/297.09 , proper^#(o()) -> c_139() 896.74/297.09 , proper^#(u()) -> c_140() 896.74/297.09 , top^#(mark(X)) -> c_141(top^#(proper(X))) 896.74/297.09 , top^#(ok(X)) -> c_142(top^#(active(X))) } 896.74/297.09 896.74/297.09 and mark the set of starting terms. 896.74/297.09 896.74/297.09 We are left with following problem, upon which TcT provides the 896.74/297.09 certificate MAYBE. 896.74/297.09 896.74/297.09 Strict DPs: 896.74/297.09 { active^#(__(X1, X2)) -> c_1(__^#(X1, active(X2))) 896.74/297.09 , active^#(__(X1, X2)) -> c_2(__^#(active(X1), X2)) 896.74/297.09 , active^#(__(X, nil())) -> c_3(X) 896.74/297.09 , active^#(__(__(X, Y), Z)) -> c_4(__^#(X, __(Y, Z))) 896.74/297.09 , active^#(__(nil(), X)) -> c_5(X) 896.74/297.09 , active^#(U11(X1, X2)) -> c_6(U11^#(active(X1), X2)) 896.74/297.09 , active^#(U11(tt(), V)) -> c_7(U12^#(isNeList(V))) 896.74/297.09 , active^#(U12(X)) -> c_8(U12^#(active(X))) 896.74/297.09 , active^#(U12(tt())) -> c_9() 896.74/297.09 , active^#(isNeList(V)) -> c_10(U31^#(isPalListKind(V), V)) 896.74/297.09 , active^#(isNeList(__(V1, V2))) -> 896.74/297.09 c_11(U41^#(and(isPalListKind(V1), isPalListKind(V2)), V1, V2)) 896.74/297.09 , active^#(isNeList(__(V1, V2))) -> 896.74/297.09 c_12(U51^#(and(isPalListKind(V1), isPalListKind(V2)), V1, V2)) 896.74/297.09 , active^#(U21(X1, X2, X3)) -> c_13(U21^#(active(X1), X2, X3)) 896.74/297.09 , active^#(U21(tt(), V1, V2)) -> c_14(U22^#(isList(V1), V2)) 896.74/297.09 , active^#(U22(X1, X2)) -> c_15(U22^#(active(X1), X2)) 896.74/297.09 , active^#(U22(tt(), V2)) -> c_16(U23^#(isList(V2))) 896.74/297.09 , active^#(isList(V)) -> c_17(U11^#(isPalListKind(V), V)) 896.74/297.09 , active^#(isList(__(V1, V2))) -> 896.74/297.09 c_18(U21^#(and(isPalListKind(V1), isPalListKind(V2)), V1, V2)) 896.74/297.09 , active^#(isList(nil())) -> c_19() 896.74/297.09 , active^#(U23(X)) -> c_20(U23^#(active(X))) 896.74/297.09 , active^#(U23(tt())) -> c_21() 896.74/297.09 , active^#(U31(X1, X2)) -> c_22(U31^#(active(X1), X2)) 896.74/297.09 , active^#(U31(tt(), V)) -> c_23(U32^#(isQid(V))) 896.74/297.09 , active^#(U32(X)) -> c_24(U32^#(active(X))) 896.74/297.09 , active^#(U32(tt())) -> c_25() 896.74/297.09 , active^#(isQid(a())) -> c_26() 896.74/297.09 , active^#(isQid(e())) -> c_27() 896.74/297.09 , active^#(isQid(i())) -> c_28() 896.74/297.09 , active^#(isQid(o())) -> c_29() 896.74/297.09 , active^#(isQid(u())) -> c_30() 896.74/297.09 , active^#(U41(X1, X2, X3)) -> c_31(U41^#(active(X1), X2, X3)) 896.74/297.09 , active^#(U41(tt(), V1, V2)) -> c_32(U42^#(isList(V1), V2)) 896.74/297.09 , active^#(U42(X1, X2)) -> c_33(U42^#(active(X1), X2)) 896.74/297.09 , active^#(U42(tt(), V2)) -> c_34(U43^#(isNeList(V2))) 896.74/297.09 , active^#(U43(X)) -> c_35(U43^#(active(X))) 896.74/297.09 , active^#(U43(tt())) -> c_36() 896.74/297.09 , active^#(U51(X1, X2, X3)) -> c_37(U51^#(active(X1), X2, X3)) 896.74/297.09 , active^#(U51(tt(), V1, V2)) -> c_38(U52^#(isNeList(V1), V2)) 896.74/297.09 , active^#(U52(X1, X2)) -> c_39(U52^#(active(X1), X2)) 896.74/297.09 , active^#(U52(tt(), V2)) -> c_40(U53^#(isList(V2))) 896.74/297.09 , active^#(U53(X)) -> c_41(U53^#(active(X))) 896.74/297.09 , active^#(U53(tt())) -> c_42() 896.74/297.09 , active^#(U61(X1, X2)) -> c_43(U61^#(active(X1), X2)) 896.74/297.09 , active^#(U61(tt(), V)) -> c_44(U62^#(isQid(V))) 896.74/297.09 , active^#(U62(X)) -> c_45(U62^#(active(X))) 896.74/297.09 , active^#(U62(tt())) -> c_46() 896.74/297.09 , active^#(U71(X1, X2)) -> c_47(U71^#(active(X1), X2)) 896.74/297.09 , active^#(U71(tt(), V)) -> c_48(U72^#(isNePal(V))) 896.74/297.09 , active^#(U72(X)) -> c_49(U72^#(active(X))) 896.74/297.09 , active^#(U72(tt())) -> c_50() 896.74/297.09 , active^#(isNePal(V)) -> c_51(U61^#(isPalListKind(V), V)) 896.74/297.09 , active^#(isNePal(__(I, __(P, I)))) -> 896.74/297.09 c_52(and^#(and(isQid(I), isPalListKind(I)), 896.74/297.09 and(isPal(P), isPalListKind(P)))) 896.74/297.09 , active^#(and(X1, X2)) -> c_53(and^#(active(X1), X2)) 896.74/297.09 , active^#(and(tt(), X)) -> c_54(X) 896.74/297.09 , active^#(isPalListKind(__(V1, V2))) -> 896.74/297.09 c_55(and^#(isPalListKind(V1), isPalListKind(V2))) 896.74/297.09 , active^#(isPalListKind(nil())) -> c_56() 896.74/297.09 , active^#(isPalListKind(a())) -> c_57() 896.74/297.09 , active^#(isPalListKind(e())) -> c_58() 896.74/297.09 , active^#(isPalListKind(i())) -> c_59() 896.74/297.09 , active^#(isPalListKind(o())) -> c_60() 896.74/297.09 , active^#(isPalListKind(u())) -> c_61() 896.74/297.09 , active^#(isPal(V)) -> c_62(U71^#(isPalListKind(V), V)) 896.74/297.09 , active^#(isPal(nil())) -> c_63() 896.74/297.09 , __^#(X1, mark(X2)) -> c_64(__^#(X1, X2)) 896.74/297.09 , __^#(mark(X1), X2) -> c_65(__^#(X1, X2)) 896.74/297.09 , __^#(ok(X1), ok(X2)) -> c_66(__^#(X1, X2)) 896.74/297.09 , U11^#(mark(X1), X2) -> c_67(U11^#(X1, X2)) 896.74/297.09 , U11^#(ok(X1), ok(X2)) -> c_68(U11^#(X1, X2)) 896.74/297.09 , U12^#(mark(X)) -> c_69(U12^#(X)) 896.74/297.09 , U12^#(ok(X)) -> c_70(U12^#(X)) 896.74/297.09 , U31^#(mark(X1), X2) -> c_79(U31^#(X1, X2)) 896.74/297.09 , U31^#(ok(X1), ok(X2)) -> c_80(U31^#(X1, X2)) 896.74/297.09 , U41^#(mark(X1), X2, X3) -> c_84(U41^#(X1, X2, X3)) 896.74/297.09 , U41^#(ok(X1), ok(X2), ok(X3)) -> c_85(U41^#(X1, X2, X3)) 896.74/297.09 , U51^#(mark(X1), X2, X3) -> c_90(U51^#(X1, X2, X3)) 896.74/297.09 , U51^#(ok(X1), ok(X2), ok(X3)) -> c_91(U51^#(X1, X2, X3)) 896.74/297.09 , U21^#(mark(X1), X2, X3) -> c_72(U21^#(X1, X2, X3)) 896.74/297.09 , U21^#(ok(X1), ok(X2), ok(X3)) -> c_73(U21^#(X1, X2, X3)) 896.74/297.09 , U22^#(mark(X1), X2) -> c_74(U22^#(X1, X2)) 896.74/297.09 , U22^#(ok(X1), ok(X2)) -> c_75(U22^#(X1, X2)) 896.74/297.09 , U23^#(mark(X)) -> c_77(U23^#(X)) 896.74/297.09 , U23^#(ok(X)) -> c_78(U23^#(X)) 896.74/297.09 , U32^#(mark(X)) -> c_81(U32^#(X)) 896.74/297.09 , U32^#(ok(X)) -> c_82(U32^#(X)) 896.74/297.09 , U42^#(mark(X1), X2) -> c_86(U42^#(X1, X2)) 896.74/297.09 , U42^#(ok(X1), ok(X2)) -> c_87(U42^#(X1, X2)) 896.74/297.09 , U43^#(mark(X)) -> c_88(U43^#(X)) 896.74/297.09 , U43^#(ok(X)) -> c_89(U43^#(X)) 896.74/297.09 , U52^#(mark(X1), X2) -> c_92(U52^#(X1, X2)) 896.74/297.09 , U52^#(ok(X1), ok(X2)) -> c_93(U52^#(X1, X2)) 896.74/297.09 , U53^#(mark(X)) -> c_94(U53^#(X)) 896.74/297.09 , U53^#(ok(X)) -> c_95(U53^#(X)) 896.74/297.09 , U61^#(mark(X1), X2) -> c_96(U61^#(X1, X2)) 896.74/297.09 , U61^#(ok(X1), ok(X2)) -> c_97(U61^#(X1, X2)) 896.74/297.09 , U62^#(mark(X)) -> c_98(U62^#(X)) 896.74/297.09 , U62^#(ok(X)) -> c_99(U62^#(X)) 896.74/297.09 , U71^#(mark(X1), X2) -> c_100(U71^#(X1, X2)) 896.74/297.09 , U71^#(ok(X1), ok(X2)) -> c_101(U71^#(X1, X2)) 896.74/297.09 , U72^#(mark(X)) -> c_102(U72^#(X)) 896.74/297.09 , U72^#(ok(X)) -> c_103(U72^#(X)) 896.74/297.09 , and^#(mark(X1), X2) -> c_105(and^#(X1, X2)) 896.74/297.09 , and^#(ok(X1), ok(X2)) -> c_106(and^#(X1, X2)) 896.74/297.09 , isNeList^#(ok(X)) -> c_71(isNeList^#(X)) 896.74/297.09 , isList^#(ok(X)) -> c_76(isList^#(X)) 896.74/297.09 , isQid^#(ok(X)) -> c_83(isQid^#(X)) 896.74/297.09 , isNePal^#(ok(X)) -> c_104(isNePal^#(X)) 896.74/297.09 , isPalListKind^#(ok(X)) -> c_107(isPalListKind^#(X)) 896.74/297.09 , isPal^#(ok(X)) -> c_108(isPal^#(X)) 896.74/297.09 , proper^#(__(X1, X2)) -> c_109(__^#(proper(X1), proper(X2))) 896.74/297.09 , proper^#(nil()) -> c_110() 896.74/297.09 , proper^#(U11(X1, X2)) -> c_111(U11^#(proper(X1), proper(X2))) 896.74/297.09 , proper^#(tt()) -> c_112() 896.74/297.09 , proper^#(U12(X)) -> c_113(U12^#(proper(X))) 896.74/297.09 , proper^#(isNeList(X)) -> c_114(isNeList^#(proper(X))) 896.74/297.09 , proper^#(U21(X1, X2, X3)) -> 896.74/297.09 c_115(U21^#(proper(X1), proper(X2), proper(X3))) 896.74/297.09 , proper^#(U22(X1, X2)) -> c_116(U22^#(proper(X1), proper(X2))) 896.74/297.09 , proper^#(isList(X)) -> c_117(isList^#(proper(X))) 896.74/297.09 , proper^#(U23(X)) -> c_118(U23^#(proper(X))) 896.74/297.09 , proper^#(U31(X1, X2)) -> c_119(U31^#(proper(X1), proper(X2))) 896.74/297.09 , proper^#(U32(X)) -> c_120(U32^#(proper(X))) 896.74/297.09 , proper^#(isQid(X)) -> c_121(isQid^#(proper(X))) 896.74/297.09 , proper^#(U41(X1, X2, X3)) -> 896.74/297.09 c_122(U41^#(proper(X1), proper(X2), proper(X3))) 896.74/297.09 , proper^#(U42(X1, X2)) -> c_123(U42^#(proper(X1), proper(X2))) 896.74/297.09 , proper^#(U43(X)) -> c_124(U43^#(proper(X))) 896.74/297.09 , proper^#(U51(X1, X2, X3)) -> 896.74/297.09 c_125(U51^#(proper(X1), proper(X2), proper(X3))) 896.74/297.09 , proper^#(U52(X1, X2)) -> c_126(U52^#(proper(X1), proper(X2))) 896.74/297.09 , proper^#(U53(X)) -> c_127(U53^#(proper(X))) 896.74/297.09 , proper^#(U61(X1, X2)) -> c_128(U61^#(proper(X1), proper(X2))) 896.74/297.09 , proper^#(U62(X)) -> c_129(U62^#(proper(X))) 896.74/297.09 , proper^#(U71(X1, X2)) -> c_130(U71^#(proper(X1), proper(X2))) 896.74/297.09 , proper^#(U72(X)) -> c_131(U72^#(proper(X))) 896.74/297.09 , proper^#(isNePal(X)) -> c_132(isNePal^#(proper(X))) 896.74/297.09 , proper^#(and(X1, X2)) -> c_133(and^#(proper(X1), proper(X2))) 896.74/297.09 , proper^#(isPalListKind(X)) -> c_134(isPalListKind^#(proper(X))) 896.74/297.09 , proper^#(isPal(X)) -> c_135(isPal^#(proper(X))) 896.74/297.09 , proper^#(a()) -> c_136() 896.74/297.09 , proper^#(e()) -> c_137() 896.74/297.09 , proper^#(i()) -> c_138() 896.74/297.09 , proper^#(o()) -> c_139() 896.74/297.09 , proper^#(u()) -> c_140() 896.74/297.09 , top^#(mark(X)) -> c_141(top^#(proper(X))) 896.74/297.09 , top^#(ok(X)) -> c_142(top^#(active(X))) } 896.74/297.09 Strict Trs: 896.74/297.09 { active(__(X1, X2)) -> __(X1, active(X2)) 896.74/297.09 , active(__(X1, X2)) -> __(active(X1), X2) 896.74/297.09 , active(__(X, nil())) -> mark(X) 896.74/297.09 , active(__(__(X, Y), Z)) -> mark(__(X, __(Y, Z))) 897.06/297.10 , active(__(nil(), X)) -> mark(X) 897.06/297.10 , active(U11(X1, X2)) -> U11(active(X1), X2) 897.06/297.10 , active(U11(tt(), V)) -> mark(U12(isNeList(V))) 897.06/297.10 , active(U12(X)) -> U12(active(X)) 897.06/297.10 , active(U12(tt())) -> mark(tt()) 897.06/297.10 , active(isNeList(V)) -> mark(U31(isPalListKind(V), V)) 897.06/297.10 , active(isNeList(__(V1, V2))) -> 897.06/297.10 mark(U41(and(isPalListKind(V1), isPalListKind(V2)), V1, V2)) 897.06/297.10 , active(isNeList(__(V1, V2))) -> 897.06/297.10 mark(U51(and(isPalListKind(V1), isPalListKind(V2)), V1, V2)) 897.06/297.10 , active(U21(X1, X2, X3)) -> U21(active(X1), X2, X3) 897.06/297.10 , active(U21(tt(), V1, V2)) -> mark(U22(isList(V1), V2)) 897.06/297.10 , active(U22(X1, X2)) -> U22(active(X1), X2) 897.06/297.10 , active(U22(tt(), V2)) -> mark(U23(isList(V2))) 897.06/297.10 , active(isList(V)) -> mark(U11(isPalListKind(V), V)) 897.06/297.10 , active(isList(__(V1, V2))) -> 897.06/297.10 mark(U21(and(isPalListKind(V1), isPalListKind(V2)), V1, V2)) 897.06/297.10 , active(isList(nil())) -> mark(tt()) 897.06/297.10 , active(U23(X)) -> U23(active(X)) 897.06/297.10 , active(U23(tt())) -> mark(tt()) 897.06/297.10 , active(U31(X1, X2)) -> U31(active(X1), X2) 897.06/297.10 , active(U31(tt(), V)) -> mark(U32(isQid(V))) 897.06/297.10 , active(U32(X)) -> U32(active(X)) 897.06/297.10 , active(U32(tt())) -> mark(tt()) 897.06/297.10 , active(isQid(a())) -> mark(tt()) 897.06/297.10 , active(isQid(e())) -> mark(tt()) 897.06/297.10 , active(isQid(i())) -> mark(tt()) 897.06/297.10 , active(isQid(o())) -> mark(tt()) 897.06/297.10 , active(isQid(u())) -> mark(tt()) 897.06/297.10 , active(U41(X1, X2, X3)) -> U41(active(X1), X2, X3) 897.06/297.10 , active(U41(tt(), V1, V2)) -> mark(U42(isList(V1), V2)) 897.06/297.10 , active(U42(X1, X2)) -> U42(active(X1), X2) 897.06/297.10 , active(U42(tt(), V2)) -> mark(U43(isNeList(V2))) 897.06/297.10 , active(U43(X)) -> U43(active(X)) 897.06/297.10 , active(U43(tt())) -> mark(tt()) 897.06/297.10 , active(U51(X1, X2, X3)) -> U51(active(X1), X2, X3) 897.06/297.10 , active(U51(tt(), V1, V2)) -> mark(U52(isNeList(V1), V2)) 897.06/297.10 , active(U52(X1, X2)) -> U52(active(X1), X2) 897.06/297.10 , active(U52(tt(), V2)) -> mark(U53(isList(V2))) 897.06/297.10 , active(U53(X)) -> U53(active(X)) 897.06/297.10 , active(U53(tt())) -> mark(tt()) 897.06/297.10 , active(U61(X1, X2)) -> U61(active(X1), X2) 897.06/297.10 , active(U61(tt(), V)) -> mark(U62(isQid(V))) 897.06/297.10 , active(U62(X)) -> U62(active(X)) 897.06/297.10 , active(U62(tt())) -> mark(tt()) 897.06/297.10 , active(U71(X1, X2)) -> U71(active(X1), X2) 897.06/297.10 , active(U71(tt(), V)) -> mark(U72(isNePal(V))) 897.06/297.10 , active(U72(X)) -> U72(active(X)) 897.06/297.10 , active(U72(tt())) -> mark(tt()) 897.06/297.10 , active(isNePal(V)) -> mark(U61(isPalListKind(V), V)) 897.06/297.10 , active(isNePal(__(I, __(P, I)))) -> 897.06/297.10 mark(and(and(isQid(I), isPalListKind(I)), 897.06/297.10 and(isPal(P), isPalListKind(P)))) 897.06/297.10 , active(and(X1, X2)) -> and(active(X1), X2) 897.06/297.10 , active(and(tt(), X)) -> mark(X) 897.06/297.10 , active(isPalListKind(__(V1, V2))) -> 897.06/297.10 mark(and(isPalListKind(V1), isPalListKind(V2))) 897.06/297.10 , active(isPalListKind(nil())) -> mark(tt()) 897.06/297.10 , active(isPalListKind(a())) -> mark(tt()) 897.06/297.10 , active(isPalListKind(e())) -> mark(tt()) 897.06/297.10 , active(isPalListKind(i())) -> mark(tt()) 897.06/297.10 , active(isPalListKind(o())) -> mark(tt()) 897.06/297.10 , active(isPalListKind(u())) -> mark(tt()) 897.06/297.10 , active(isPal(V)) -> mark(U71(isPalListKind(V), V)) 897.06/297.10 , active(isPal(nil())) -> mark(tt()) 897.06/297.10 , __(X1, mark(X2)) -> mark(__(X1, X2)) 897.06/297.10 , __(mark(X1), X2) -> mark(__(X1, X2)) 897.06/297.10 , __(ok(X1), ok(X2)) -> ok(__(X1, X2)) 897.06/297.10 , U11(mark(X1), X2) -> mark(U11(X1, X2)) 897.06/297.10 , U11(ok(X1), ok(X2)) -> ok(U11(X1, X2)) 897.06/297.10 , U12(mark(X)) -> mark(U12(X)) 897.06/297.10 , U12(ok(X)) -> ok(U12(X)) 897.06/297.10 , isNeList(ok(X)) -> ok(isNeList(X)) 897.06/297.10 , U21(mark(X1), X2, X3) -> mark(U21(X1, X2, X3)) 897.06/297.10 , U21(ok(X1), ok(X2), ok(X3)) -> ok(U21(X1, X2, X3)) 897.06/297.10 , U22(mark(X1), X2) -> mark(U22(X1, X2)) 897.06/297.10 , U22(ok(X1), ok(X2)) -> ok(U22(X1, X2)) 897.06/297.10 , isList(ok(X)) -> ok(isList(X)) 897.06/297.10 , U23(mark(X)) -> mark(U23(X)) 897.06/297.10 , U23(ok(X)) -> ok(U23(X)) 897.06/297.10 , U31(mark(X1), X2) -> mark(U31(X1, X2)) 897.06/297.10 , U31(ok(X1), ok(X2)) -> ok(U31(X1, X2)) 897.06/297.10 , U32(mark(X)) -> mark(U32(X)) 897.06/297.10 , U32(ok(X)) -> ok(U32(X)) 897.06/297.10 , isQid(ok(X)) -> ok(isQid(X)) 897.06/297.10 , U41(mark(X1), X2, X3) -> mark(U41(X1, X2, X3)) 897.06/297.10 , U41(ok(X1), ok(X2), ok(X3)) -> ok(U41(X1, X2, X3)) 897.06/297.10 , U42(mark(X1), X2) -> mark(U42(X1, X2)) 897.06/297.10 , U42(ok(X1), ok(X2)) -> ok(U42(X1, X2)) 897.06/297.10 , U43(mark(X)) -> mark(U43(X)) 897.06/297.10 , U43(ok(X)) -> ok(U43(X)) 897.06/297.10 , U51(mark(X1), X2, X3) -> mark(U51(X1, X2, X3)) 897.06/297.10 , U51(ok(X1), ok(X2), ok(X3)) -> ok(U51(X1, X2, X3)) 897.06/297.10 , U52(mark(X1), X2) -> mark(U52(X1, X2)) 897.06/297.10 , U52(ok(X1), ok(X2)) -> ok(U52(X1, X2)) 897.06/297.10 , U53(mark(X)) -> mark(U53(X)) 897.06/297.10 , U53(ok(X)) -> ok(U53(X)) 897.06/297.10 , U61(mark(X1), X2) -> mark(U61(X1, X2)) 897.06/297.10 , U61(ok(X1), ok(X2)) -> ok(U61(X1, X2)) 897.06/297.10 , U62(mark(X)) -> mark(U62(X)) 897.06/297.10 , U62(ok(X)) -> ok(U62(X)) 897.06/297.10 , U71(mark(X1), X2) -> mark(U71(X1, X2)) 897.06/297.10 , U71(ok(X1), ok(X2)) -> ok(U71(X1, X2)) 897.06/297.10 , U72(mark(X)) -> mark(U72(X)) 897.06/297.10 , U72(ok(X)) -> ok(U72(X)) 897.06/297.10 , isNePal(ok(X)) -> ok(isNePal(X)) 897.06/297.10 , and(mark(X1), X2) -> mark(and(X1, X2)) 897.06/297.10 , and(ok(X1), ok(X2)) -> ok(and(X1, X2)) 897.06/297.10 , isPalListKind(ok(X)) -> ok(isPalListKind(X)) 897.06/297.10 , isPal(ok(X)) -> ok(isPal(X)) 897.06/297.10 , proper(__(X1, X2)) -> __(proper(X1), proper(X2)) 897.06/297.10 , proper(nil()) -> ok(nil()) 897.06/297.10 , proper(U11(X1, X2)) -> U11(proper(X1), proper(X2)) 897.06/297.10 , proper(tt()) -> ok(tt()) 897.06/297.10 , proper(U12(X)) -> U12(proper(X)) 897.06/297.10 , proper(isNeList(X)) -> isNeList(proper(X)) 897.06/297.10 , proper(U21(X1, X2, X3)) -> 897.06/297.10 U21(proper(X1), proper(X2), proper(X3)) 897.06/297.10 , proper(U22(X1, X2)) -> U22(proper(X1), proper(X2)) 897.06/297.10 , proper(isList(X)) -> isList(proper(X)) 897.06/297.10 , proper(U23(X)) -> U23(proper(X)) 897.06/297.10 , proper(U31(X1, X2)) -> U31(proper(X1), proper(X2)) 897.06/297.10 , proper(U32(X)) -> U32(proper(X)) 897.06/297.10 , proper(isQid(X)) -> isQid(proper(X)) 897.06/297.10 , proper(U41(X1, X2, X3)) -> 897.06/297.10 U41(proper(X1), proper(X2), proper(X3)) 897.06/297.10 , proper(U42(X1, X2)) -> U42(proper(X1), proper(X2)) 897.06/297.10 , proper(U43(X)) -> U43(proper(X)) 897.06/297.10 , proper(U51(X1, X2, X3)) -> 897.06/297.10 U51(proper(X1), proper(X2), proper(X3)) 897.06/297.10 , proper(U52(X1, X2)) -> U52(proper(X1), proper(X2)) 897.06/297.10 , proper(U53(X)) -> U53(proper(X)) 897.06/297.10 , proper(U61(X1, X2)) -> U61(proper(X1), proper(X2)) 897.06/297.10 , proper(U62(X)) -> U62(proper(X)) 897.06/297.10 , proper(U71(X1, X2)) -> U71(proper(X1), proper(X2)) 897.06/297.10 , proper(U72(X)) -> U72(proper(X)) 897.06/297.10 , proper(isNePal(X)) -> isNePal(proper(X)) 897.06/297.10 , proper(and(X1, X2)) -> and(proper(X1), proper(X2)) 897.06/297.10 , proper(isPalListKind(X)) -> isPalListKind(proper(X)) 897.06/297.10 , proper(isPal(X)) -> isPal(proper(X)) 897.06/297.10 , proper(a()) -> ok(a()) 897.06/297.10 , proper(e()) -> ok(e()) 897.06/297.10 , proper(i()) -> ok(i()) 897.06/297.10 , proper(o()) -> ok(o()) 897.06/297.10 , proper(u()) -> ok(u()) 897.06/297.10 , top(mark(X)) -> top(proper(X)) 897.06/297.10 , top(ok(X)) -> top(active(X)) } 897.06/297.10 Obligation: 897.06/297.10 runtime complexity 897.06/297.10 Answer: 897.06/297.10 MAYBE 897.06/297.10 897.06/297.10 Consider the dependency graph: 897.06/297.10 897.06/297.10 1: active^#(__(X1, X2)) -> c_1(__^#(X1, active(X2))) 897.06/297.10 -->_1 __^#(ok(X1), ok(X2)) -> c_66(__^#(X1, X2)) :66 897.06/297.10 -->_1 __^#(mark(X1), X2) -> c_65(__^#(X1, X2)) :65 897.06/297.10 -->_1 __^#(X1, mark(X2)) -> c_64(__^#(X1, X2)) :64 897.06/297.10 897.06/297.10 2: active^#(__(X1, X2)) -> c_2(__^#(active(X1), X2)) 897.06/297.10 -->_1 __^#(ok(X1), ok(X2)) -> c_66(__^#(X1, X2)) :66 897.06/297.10 -->_1 __^#(mark(X1), X2) -> c_65(__^#(X1, X2)) :65 897.06/297.10 -->_1 __^#(X1, mark(X2)) -> c_64(__^#(X1, X2)) :64 897.06/297.10 897.06/297.10 3: active^#(__(X, nil())) -> c_3(X) 897.06/297.10 -->_1 top^#(ok(X)) -> c_142(top^#(active(X))) :142 897.06/297.10 -->_1 top^#(mark(X)) -> c_141(top^#(proper(X))) :141 897.06/297.10 -->_1 proper^#(isPal(X)) -> c_135(isPal^#(proper(X))) :135 897.06/297.10 -->_1 proper^#(isPalListKind(X)) -> 897.06/297.10 c_134(isPalListKind^#(proper(X))) :134 897.06/297.10 -->_1 proper^#(and(X1, X2)) -> 897.06/297.10 c_133(and^#(proper(X1), proper(X2))) :133 897.06/297.10 -->_1 proper^#(isNePal(X)) -> c_132(isNePal^#(proper(X))) :132 897.06/297.10 -->_1 proper^#(U72(X)) -> c_131(U72^#(proper(X))) :131 897.06/297.10 -->_1 proper^#(U71(X1, X2)) -> 897.06/297.10 c_130(U71^#(proper(X1), proper(X2))) :130 897.06/297.10 -->_1 proper^#(U62(X)) -> c_129(U62^#(proper(X))) :129 897.06/297.10 -->_1 proper^#(U61(X1, X2)) -> 897.06/297.10 c_128(U61^#(proper(X1), proper(X2))) :128 897.06/297.11 -->_1 proper^#(U53(X)) -> c_127(U53^#(proper(X))) :127 897.06/297.11 -->_1 proper^#(U52(X1, X2)) -> 897.06/297.11 c_126(U52^#(proper(X1), proper(X2))) :126 897.06/297.11 -->_1 proper^#(U51(X1, X2, X3)) -> 897.06/297.11 c_125(U51^#(proper(X1), proper(X2), proper(X3))) :125 897.06/297.11 -->_1 proper^#(U43(X)) -> c_124(U43^#(proper(X))) :124 897.06/297.11 -->_1 proper^#(U42(X1, X2)) -> 897.06/297.11 c_123(U42^#(proper(X1), proper(X2))) :123 897.06/297.11 -->_1 proper^#(U41(X1, X2, X3)) -> 897.06/297.11 c_122(U41^#(proper(X1), proper(X2), proper(X3))) :122 897.06/297.11 -->_1 proper^#(isQid(X)) -> c_121(isQid^#(proper(X))) :121 897.06/297.11 -->_1 proper^#(U32(X)) -> c_120(U32^#(proper(X))) :120 897.06/297.11 -->_1 proper^#(U31(X1, X2)) -> 897.06/297.11 c_119(U31^#(proper(X1), proper(X2))) :119 897.06/297.11 -->_1 proper^#(U23(X)) -> c_118(U23^#(proper(X))) :118 897.06/297.11 -->_1 proper^#(isList(X)) -> c_117(isList^#(proper(X))) :117 897.06/297.11 -->_1 proper^#(U22(X1, X2)) -> 897.06/297.11 c_116(U22^#(proper(X1), proper(X2))) :116 897.06/297.11 -->_1 proper^#(U21(X1, X2, X3)) -> 897.06/297.11 c_115(U21^#(proper(X1), proper(X2), proper(X3))) :115 897.06/297.11 -->_1 proper^#(isNeList(X)) -> c_114(isNeList^#(proper(X))) :114 897.06/297.11 -->_1 proper^#(U12(X)) -> c_113(U12^#(proper(X))) :113 897.06/297.11 -->_1 proper^#(U11(X1, X2)) -> 897.06/297.11 c_111(U11^#(proper(X1), proper(X2))) :111 897.06/297.11 -->_1 proper^#(__(X1, X2)) -> 897.06/297.11 c_109(__^#(proper(X1), proper(X2))) :109 897.06/297.11 -->_1 isPal^#(ok(X)) -> c_108(isPal^#(X)) :108 897.06/297.11 -->_1 isPalListKind^#(ok(X)) -> c_107(isPalListKind^#(X)) :107 897.06/297.11 -->_1 isNePal^#(ok(X)) -> c_104(isNePal^#(X)) :106 897.06/297.11 -->_1 isQid^#(ok(X)) -> c_83(isQid^#(X)) :105 897.06/297.11 -->_1 isList^#(ok(X)) -> c_76(isList^#(X)) :104 897.06/297.11 -->_1 isNeList^#(ok(X)) -> c_71(isNeList^#(X)) :103 897.06/297.11 -->_1 and^#(ok(X1), ok(X2)) -> c_106(and^#(X1, X2)) :102 897.06/297.11 -->_1 and^#(mark(X1), X2) -> c_105(and^#(X1, X2)) :101 897.06/297.11 -->_1 U72^#(ok(X)) -> c_103(U72^#(X)) :100 897.06/297.11 -->_1 U72^#(mark(X)) -> c_102(U72^#(X)) :99 897.06/297.11 -->_1 U71^#(ok(X1), ok(X2)) -> c_101(U71^#(X1, X2)) :98 897.06/297.11 -->_1 U71^#(mark(X1), X2) -> c_100(U71^#(X1, X2)) :97 897.06/297.11 -->_1 U62^#(ok(X)) -> c_99(U62^#(X)) :96 897.06/297.11 -->_1 U62^#(mark(X)) -> c_98(U62^#(X)) :95 897.06/297.11 -->_1 U61^#(ok(X1), ok(X2)) -> c_97(U61^#(X1, X2)) :94 897.06/297.11 -->_1 U61^#(mark(X1), X2) -> c_96(U61^#(X1, X2)) :93 897.06/297.11 -->_1 U53^#(ok(X)) -> c_95(U53^#(X)) :92 897.06/297.11 -->_1 U53^#(mark(X)) -> c_94(U53^#(X)) :91 897.06/297.11 -->_1 U52^#(ok(X1), ok(X2)) -> c_93(U52^#(X1, X2)) :90 897.06/297.11 -->_1 U52^#(mark(X1), X2) -> c_92(U52^#(X1, X2)) :89 897.06/297.11 -->_1 U43^#(ok(X)) -> c_89(U43^#(X)) :88 897.06/297.11 -->_1 U43^#(mark(X)) -> c_88(U43^#(X)) :87 897.06/297.11 -->_1 U42^#(ok(X1), ok(X2)) -> c_87(U42^#(X1, X2)) :86 897.06/297.11 -->_1 U42^#(mark(X1), X2) -> c_86(U42^#(X1, X2)) :85 897.06/297.11 -->_1 U32^#(ok(X)) -> c_82(U32^#(X)) :84 897.06/297.11 -->_1 U32^#(mark(X)) -> c_81(U32^#(X)) :83 897.06/297.11 -->_1 U23^#(ok(X)) -> c_78(U23^#(X)) :82 897.06/297.11 -->_1 U23^#(mark(X)) -> c_77(U23^#(X)) :81 897.06/297.11 -->_1 U22^#(ok(X1), ok(X2)) -> c_75(U22^#(X1, X2)) :80 897.06/297.11 -->_1 U22^#(mark(X1), X2) -> c_74(U22^#(X1, X2)) :79 897.06/297.11 -->_1 U21^#(ok(X1), ok(X2), ok(X3)) -> c_73(U21^#(X1, X2, X3)) :78 897.06/297.11 -->_1 U21^#(mark(X1), X2, X3) -> c_72(U21^#(X1, X2, X3)) :77 897.06/297.11 -->_1 U51^#(ok(X1), ok(X2), ok(X3)) -> c_91(U51^#(X1, X2, X3)) :76 897.06/297.11 -->_1 U51^#(mark(X1), X2, X3) -> c_90(U51^#(X1, X2, X3)) :75 897.06/297.11 -->_1 U41^#(ok(X1), ok(X2), ok(X3)) -> c_85(U41^#(X1, X2, X3)) :74 897.06/297.11 -->_1 U41^#(mark(X1), X2, X3) -> c_84(U41^#(X1, X2, X3)) :73 897.06/297.11 -->_1 U31^#(ok(X1), ok(X2)) -> c_80(U31^#(X1, X2)) :72 897.06/297.11 -->_1 U31^#(mark(X1), X2) -> c_79(U31^#(X1, X2)) :71 897.06/297.11 -->_1 U12^#(ok(X)) -> c_70(U12^#(X)) :70 897.06/297.11 -->_1 U12^#(mark(X)) -> c_69(U12^#(X)) :69 897.06/297.11 -->_1 U11^#(ok(X1), ok(X2)) -> c_68(U11^#(X1, X2)) :68 897.06/297.11 -->_1 U11^#(mark(X1), X2) -> c_67(U11^#(X1, X2)) :67 897.06/297.11 -->_1 __^#(ok(X1), ok(X2)) -> c_66(__^#(X1, X2)) :66 897.06/297.11 -->_1 __^#(mark(X1), X2) -> c_65(__^#(X1, X2)) :65 897.06/297.11 -->_1 __^#(X1, mark(X2)) -> c_64(__^#(X1, X2)) :64 897.06/297.11 -->_1 active^#(isPal(V)) -> c_62(U71^#(isPalListKind(V), V)) :62 897.06/297.11 -->_1 active^#(isPalListKind(__(V1, V2))) -> 897.06/297.11 c_55(and^#(isPalListKind(V1), isPalListKind(V2))) :55 897.06/297.11 -->_1 active^#(and(tt(), X)) -> c_54(X) :54 897.06/297.11 -->_1 active^#(and(X1, X2)) -> c_53(and^#(active(X1), X2)) :53 897.06/297.11 -->_1 active^#(isNePal(__(I, __(P, I)))) -> 897.06/297.11 c_52(and^#(and(isQid(I), isPalListKind(I)), 897.06/297.11 and(isPal(P), isPalListKind(P)))) :52 897.06/297.11 -->_1 active^#(isNePal(V)) -> c_51(U61^#(isPalListKind(V), V)) :51 897.06/297.11 -->_1 active^#(U72(X)) -> c_49(U72^#(active(X))) :49 897.06/297.11 -->_1 active^#(U71(tt(), V)) -> c_48(U72^#(isNePal(V))) :48 897.06/297.11 -->_1 active^#(U71(X1, X2)) -> c_47(U71^#(active(X1), X2)) :47 897.06/297.11 -->_1 active^#(U62(X)) -> c_45(U62^#(active(X))) :45 897.06/297.11 -->_1 active^#(U61(tt(), V)) -> c_44(U62^#(isQid(V))) :44 897.06/297.11 -->_1 active^#(U61(X1, X2)) -> c_43(U61^#(active(X1), X2)) :43 897.06/297.11 -->_1 active^#(U53(X)) -> c_41(U53^#(active(X))) :41 897.06/297.11 -->_1 active^#(U52(tt(), V2)) -> c_40(U53^#(isList(V2))) :40 897.06/297.11 -->_1 active^#(U52(X1, X2)) -> c_39(U52^#(active(X1), X2)) :39 897.06/297.11 -->_1 active^#(U51(tt(), V1, V2)) -> 897.06/297.11 c_38(U52^#(isNeList(V1), V2)) :38 897.06/297.11 -->_1 active^#(U51(X1, X2, X3)) -> 897.06/297.11 c_37(U51^#(active(X1), X2, X3)) :37 897.06/297.11 -->_1 active^#(U43(X)) -> c_35(U43^#(active(X))) :35 897.06/297.11 -->_1 active^#(U42(tt(), V2)) -> c_34(U43^#(isNeList(V2))) :34 897.06/297.11 -->_1 active^#(U42(X1, X2)) -> c_33(U42^#(active(X1), X2)) :33 897.06/297.11 -->_1 active^#(U41(tt(), V1, V2)) -> 897.06/297.11 c_32(U42^#(isList(V1), V2)) :32 897.06/297.11 -->_1 active^#(U41(X1, X2, X3)) -> 897.06/297.11 c_31(U41^#(active(X1), X2, X3)) :31 897.06/297.11 -->_1 active^#(U32(X)) -> c_24(U32^#(active(X))) :24 897.06/297.11 -->_1 active^#(U31(tt(), V)) -> c_23(U32^#(isQid(V))) :23 897.06/297.11 -->_1 active^#(U31(X1, X2)) -> c_22(U31^#(active(X1), X2)) :22 897.06/297.11 -->_1 active^#(U23(X)) -> c_20(U23^#(active(X))) :20 897.06/297.11 -->_1 active^#(isList(__(V1, V2))) -> 897.06/297.11 c_18(U21^#(and(isPalListKind(V1), isPalListKind(V2)), V1, V2)) :18 897.06/297.11 -->_1 active^#(isList(V)) -> c_17(U11^#(isPalListKind(V), V)) :17 897.06/297.11 -->_1 active^#(U22(tt(), V2)) -> c_16(U23^#(isList(V2))) :16 897.06/297.11 -->_1 active^#(U22(X1, X2)) -> c_15(U22^#(active(X1), X2)) :15 897.06/297.11 -->_1 active^#(U21(tt(), V1, V2)) -> 897.06/297.11 c_14(U22^#(isList(V1), V2)) :14 897.06/297.11 -->_1 active^#(U21(X1, X2, X3)) -> 897.06/297.11 c_13(U21^#(active(X1), X2, X3)) :13 897.06/297.11 -->_1 active^#(isNeList(__(V1, V2))) -> 897.06/297.11 c_12(U51^#(and(isPalListKind(V1), isPalListKind(V2)), V1, V2)) :12 897.06/297.11 -->_1 active^#(isNeList(__(V1, V2))) -> 897.06/297.11 c_11(U41^#(and(isPalListKind(V1), isPalListKind(V2)), V1, V2)) :11 897.06/297.11 -->_1 active^#(isNeList(V)) -> c_10(U31^#(isPalListKind(V), V)) :10 897.06/297.11 -->_1 active^#(U12(X)) -> c_8(U12^#(active(X))) :8 897.06/297.11 -->_1 active^#(U11(tt(), V)) -> c_7(U12^#(isNeList(V))) :7 897.06/297.11 -->_1 active^#(U11(X1, X2)) -> c_6(U11^#(active(X1), X2)) :6 897.06/297.11 -->_1 active^#(__(nil(), X)) -> c_5(X) :5 897.06/297.11 -->_1 active^#(__(__(X, Y), Z)) -> c_4(__^#(X, __(Y, Z))) :4 897.06/297.11 -->_1 proper^#(u()) -> c_140() :140 897.06/297.11 -->_1 proper^#(o()) -> c_139() :139 897.06/297.11 -->_1 proper^#(i()) -> c_138() :138 897.06/297.11 -->_1 proper^#(e()) -> c_137() :137 897.06/297.11 -->_1 proper^#(a()) -> c_136() :136 897.06/297.11 -->_1 proper^#(tt()) -> c_112() :112 897.06/297.11 -->_1 proper^#(nil()) -> c_110() :110 897.06/297.11 -->_1 active^#(isPal(nil())) -> c_63() :63 897.06/297.11 -->_1 active^#(isPalListKind(u())) -> c_61() :61 897.06/297.11 -->_1 active^#(isPalListKind(o())) -> c_60() :60 897.06/297.11 -->_1 active^#(isPalListKind(i())) -> c_59() :59 897.06/297.11 -->_1 active^#(isPalListKind(e())) -> c_58() :58 897.06/297.11 -->_1 active^#(isPalListKind(a())) -> c_57() :57 897.06/297.11 -->_1 active^#(isPalListKind(nil())) -> c_56() :56 897.06/297.11 -->_1 active^#(U72(tt())) -> c_50() :50 897.06/297.11 -->_1 active^#(U62(tt())) -> c_46() :46 897.06/297.11 -->_1 active^#(U53(tt())) -> c_42() :42 897.06/297.11 -->_1 active^#(U43(tt())) -> c_36() :36 897.06/297.11 -->_1 active^#(isQid(u())) -> c_30() :30 897.06/297.11 -->_1 active^#(isQid(o())) -> c_29() :29 897.06/297.11 -->_1 active^#(isQid(i())) -> c_28() :28 897.06/297.11 -->_1 active^#(isQid(e())) -> c_27() :27 897.06/297.11 -->_1 active^#(isQid(a())) -> c_26() :26 897.06/297.11 -->_1 active^#(U32(tt())) -> c_25() :25 897.06/297.11 -->_1 active^#(U23(tt())) -> c_21() :21 897.06/297.11 -->_1 active^#(isList(nil())) -> c_19() :19 897.06/297.11 -->_1 active^#(U12(tt())) -> c_9() :9 897.06/297.11 -->_1 active^#(__(X, nil())) -> c_3(X) :3 897.06/297.11 -->_1 active^#(__(X1, X2)) -> c_2(__^#(active(X1), X2)) :2 897.06/297.11 -->_1 active^#(__(X1, X2)) -> c_1(__^#(X1, active(X2))) :1 897.06/297.11 897.06/297.11 4: active^#(__(__(X, Y), Z)) -> c_4(__^#(X, __(Y, Z))) 897.06/297.11 -->_1 __^#(ok(X1), ok(X2)) -> c_66(__^#(X1, X2)) :66 897.06/297.11 -->_1 __^#(mark(X1), X2) -> c_65(__^#(X1, X2)) :65 897.06/297.11 -->_1 __^#(X1, mark(X2)) -> c_64(__^#(X1, X2)) :64 897.06/297.11 897.06/297.11 5: active^#(__(nil(), X)) -> c_5(X) 897.06/297.11 -->_1 top^#(ok(X)) -> c_142(top^#(active(X))) :142 897.06/297.11 -->_1 top^#(mark(X)) -> c_141(top^#(proper(X))) :141 897.06/297.11 -->_1 proper^#(isPal(X)) -> c_135(isPal^#(proper(X))) :135 897.06/297.11 -->_1 proper^#(isPalListKind(X)) -> 897.06/297.11 c_134(isPalListKind^#(proper(X))) :134 897.06/297.11 -->_1 proper^#(and(X1, X2)) -> 897.06/297.11 c_133(and^#(proper(X1), proper(X2))) :133 897.06/297.11 -->_1 proper^#(isNePal(X)) -> c_132(isNePal^#(proper(X))) :132 897.06/297.11 -->_1 proper^#(U72(X)) -> c_131(U72^#(proper(X))) :131 897.06/297.11 -->_1 proper^#(U71(X1, X2)) -> 897.06/297.11 c_130(U71^#(proper(X1), proper(X2))) :130 897.06/297.11 -->_1 proper^#(U62(X)) -> c_129(U62^#(proper(X))) :129 897.06/297.11 -->_1 proper^#(U61(X1, X2)) -> 897.06/297.11 c_128(U61^#(proper(X1), proper(X2))) :128 897.06/297.11 -->_1 proper^#(U53(X)) -> c_127(U53^#(proper(X))) :127 897.06/297.11 -->_1 proper^#(U52(X1, X2)) -> 897.06/297.11 c_126(U52^#(proper(X1), proper(X2))) :126 897.06/297.11 -->_1 proper^#(U51(X1, X2, X3)) -> 897.06/297.11 c_125(U51^#(proper(X1), proper(X2), proper(X3))) :125 897.06/297.11 -->_1 proper^#(U43(X)) -> c_124(U43^#(proper(X))) :124 897.06/297.11 -->_1 proper^#(U42(X1, X2)) -> 897.06/297.11 c_123(U42^#(proper(X1), proper(X2))) :123 897.06/297.11 -->_1 proper^#(U41(X1, X2, X3)) -> 897.06/297.11 c_122(U41^#(proper(X1), proper(X2), proper(X3))) :122 897.06/297.11 -->_1 proper^#(isQid(X)) -> c_121(isQid^#(proper(X))) :121 897.06/297.11 -->_1 proper^#(U32(X)) -> c_120(U32^#(proper(X))) :120 897.06/297.11 -->_1 proper^#(U31(X1, X2)) -> 897.06/297.11 c_119(U31^#(proper(X1), proper(X2))) :119 897.06/297.11 -->_1 proper^#(U23(X)) -> c_118(U23^#(proper(X))) :118 897.06/297.11 -->_1 proper^#(isList(X)) -> c_117(isList^#(proper(X))) :117 897.06/297.11 -->_1 proper^#(U22(X1, X2)) -> 897.06/297.11 c_116(U22^#(proper(X1), proper(X2))) :116 897.06/297.11 -->_1 proper^#(U21(X1, X2, X3)) -> 897.06/297.11 c_115(U21^#(proper(X1), proper(X2), proper(X3))) :115 897.06/297.11 -->_1 proper^#(isNeList(X)) -> c_114(isNeList^#(proper(X))) :114 897.06/297.11 -->_1 proper^#(U12(X)) -> c_113(U12^#(proper(X))) :113 897.06/297.11 -->_1 proper^#(U11(X1, X2)) -> 897.06/297.11 c_111(U11^#(proper(X1), proper(X2))) :111 897.06/297.11 -->_1 proper^#(__(X1, X2)) -> 897.06/297.11 c_109(__^#(proper(X1), proper(X2))) :109 897.06/297.11 -->_1 isPal^#(ok(X)) -> c_108(isPal^#(X)) :108 897.06/297.11 -->_1 isPalListKind^#(ok(X)) -> c_107(isPalListKind^#(X)) :107 897.06/297.11 -->_1 isNePal^#(ok(X)) -> c_104(isNePal^#(X)) :106 897.06/297.11 -->_1 isQid^#(ok(X)) -> c_83(isQid^#(X)) :105 897.06/297.11 -->_1 isList^#(ok(X)) -> c_76(isList^#(X)) :104 897.06/297.11 -->_1 isNeList^#(ok(X)) -> c_71(isNeList^#(X)) :103 897.06/297.11 -->_1 and^#(ok(X1), ok(X2)) -> c_106(and^#(X1, X2)) :102 897.06/297.11 -->_1 and^#(mark(X1), X2) -> c_105(and^#(X1, X2)) :101 897.06/297.11 -->_1 U72^#(ok(X)) -> c_103(U72^#(X)) :100 897.06/297.11 -->_1 U72^#(mark(X)) -> c_102(U72^#(X)) :99 897.06/297.11 -->_1 U71^#(ok(X1), ok(X2)) -> c_101(U71^#(X1, X2)) :98 897.06/297.11 -->_1 U71^#(mark(X1), X2) -> c_100(U71^#(X1, X2)) :97 897.06/297.11 -->_1 U62^#(ok(X)) -> c_99(U62^#(X)) :96 897.06/297.11 -->_1 U62^#(mark(X)) -> c_98(U62^#(X)) :95 897.06/297.11 -->_1 U61^#(ok(X1), ok(X2)) -> c_97(U61^#(X1, X2)) :94 897.06/297.11 -->_1 U61^#(mark(X1), X2) -> c_96(U61^#(X1, X2)) :93 897.06/297.11 -->_1 U53^#(ok(X)) -> c_95(U53^#(X)) :92 897.06/297.11 -->_1 U53^#(mark(X)) -> c_94(U53^#(X)) :91 897.06/297.11 -->_1 U52^#(ok(X1), ok(X2)) -> c_93(U52^#(X1, X2)) :90 897.06/297.11 -->_1 U52^#(mark(X1), X2) -> c_92(U52^#(X1, X2)) :89 897.06/297.11 -->_1 U43^#(ok(X)) -> c_89(U43^#(X)) :88 897.06/297.11 -->_1 U43^#(mark(X)) -> c_88(U43^#(X)) :87 897.06/297.11 -->_1 U42^#(ok(X1), ok(X2)) -> c_87(U42^#(X1, X2)) :86 897.06/297.11 -->_1 U42^#(mark(X1), X2) -> c_86(U42^#(X1, X2)) :85 897.06/297.11 -->_1 U32^#(ok(X)) -> c_82(U32^#(X)) :84 897.06/297.11 -->_1 U32^#(mark(X)) -> c_81(U32^#(X)) :83 897.06/297.11 -->_1 U23^#(ok(X)) -> c_78(U23^#(X)) :82 897.06/297.11 -->_1 U23^#(mark(X)) -> c_77(U23^#(X)) :81 897.06/297.11 -->_1 U22^#(ok(X1), ok(X2)) -> c_75(U22^#(X1, X2)) :80 897.06/297.11 -->_1 U22^#(mark(X1), X2) -> c_74(U22^#(X1, X2)) :79 897.06/297.11 -->_1 U21^#(ok(X1), ok(X2), ok(X3)) -> c_73(U21^#(X1, X2, X3)) :78 897.06/297.11 -->_1 U21^#(mark(X1), X2, X3) -> c_72(U21^#(X1, X2, X3)) :77 897.06/297.11 -->_1 U51^#(ok(X1), ok(X2), ok(X3)) -> c_91(U51^#(X1, X2, X3)) :76 897.06/297.11 -->_1 U51^#(mark(X1), X2, X3) -> c_90(U51^#(X1, X2, X3)) :75 897.06/297.11 -->_1 U41^#(ok(X1), ok(X2), ok(X3)) -> c_85(U41^#(X1, X2, X3)) :74 897.06/297.11 -->_1 U41^#(mark(X1), X2, X3) -> c_84(U41^#(X1, X2, X3)) :73 897.06/297.11 -->_1 U31^#(ok(X1), ok(X2)) -> c_80(U31^#(X1, X2)) :72 897.06/297.11 -->_1 U31^#(mark(X1), X2) -> c_79(U31^#(X1, X2)) :71 897.06/297.11 -->_1 U12^#(ok(X)) -> c_70(U12^#(X)) :70 897.06/297.11 -->_1 U12^#(mark(X)) -> c_69(U12^#(X)) :69 897.06/297.11 -->_1 U11^#(ok(X1), ok(X2)) -> c_68(U11^#(X1, X2)) :68 897.06/297.11 -->_1 U11^#(mark(X1), X2) -> c_67(U11^#(X1, X2)) :67 897.06/297.11 -->_1 __^#(ok(X1), ok(X2)) -> c_66(__^#(X1, X2)) :66 897.06/297.11 -->_1 __^#(mark(X1), X2) -> c_65(__^#(X1, X2)) :65 897.06/297.11 -->_1 __^#(X1, mark(X2)) -> c_64(__^#(X1, X2)) :64 897.06/297.11 -->_1 active^#(isPal(V)) -> c_62(U71^#(isPalListKind(V), V)) :62 897.06/297.11 -->_1 active^#(isPalListKind(__(V1, V2))) -> 897.06/297.11 c_55(and^#(isPalListKind(V1), isPalListKind(V2))) :55 897.06/297.11 -->_1 active^#(and(tt(), X)) -> c_54(X) :54 897.06/297.11 -->_1 active^#(and(X1, X2)) -> c_53(and^#(active(X1), X2)) :53 897.06/297.11 -->_1 active^#(isNePal(__(I, __(P, I)))) -> 897.06/297.11 c_52(and^#(and(isQid(I), isPalListKind(I)), 897.06/297.11 and(isPal(P), isPalListKind(P)))) :52 897.06/297.11 -->_1 active^#(isNePal(V)) -> c_51(U61^#(isPalListKind(V), V)) :51 897.06/297.11 -->_1 active^#(U72(X)) -> c_49(U72^#(active(X))) :49 897.06/297.11 -->_1 active^#(U71(tt(), V)) -> c_48(U72^#(isNePal(V))) :48 897.06/297.11 -->_1 active^#(U71(X1, X2)) -> c_47(U71^#(active(X1), X2)) :47 897.06/297.11 -->_1 active^#(U62(X)) -> c_45(U62^#(active(X))) :45 897.06/297.11 -->_1 active^#(U61(tt(), V)) -> c_44(U62^#(isQid(V))) :44 897.06/297.11 -->_1 active^#(U61(X1, X2)) -> c_43(U61^#(active(X1), X2)) :43 897.06/297.11 -->_1 active^#(U53(X)) -> c_41(U53^#(active(X))) :41 897.06/297.11 -->_1 active^#(U52(tt(), V2)) -> c_40(U53^#(isList(V2))) :40 897.06/297.11 -->_1 active^#(U52(X1, X2)) -> c_39(U52^#(active(X1), X2)) :39 897.06/297.11 -->_1 active^#(U51(tt(), V1, V2)) -> 897.06/297.11 c_38(U52^#(isNeList(V1), V2)) :38 897.06/297.11 -->_1 active^#(U51(X1, X2, X3)) -> 897.06/297.11 c_37(U51^#(active(X1), X2, X3)) :37 897.06/297.11 -->_1 active^#(U43(X)) -> c_35(U43^#(active(X))) :35 897.06/297.11 -->_1 active^#(U42(tt(), V2)) -> c_34(U43^#(isNeList(V2))) :34 897.06/297.11 -->_1 active^#(U42(X1, X2)) -> c_33(U42^#(active(X1), X2)) :33 897.06/297.11 -->_1 active^#(U41(tt(), V1, V2)) -> 897.06/297.11 c_32(U42^#(isList(V1), V2)) :32 897.06/297.11 -->_1 active^#(U41(X1, X2, X3)) -> 897.06/297.11 c_31(U41^#(active(X1), X2, X3)) :31 897.06/297.11 -->_1 active^#(U32(X)) -> c_24(U32^#(active(X))) :24 897.06/297.11 -->_1 active^#(U31(tt(), V)) -> c_23(U32^#(isQid(V))) :23 897.06/297.11 -->_1 active^#(U31(X1, X2)) -> c_22(U31^#(active(X1), X2)) :22 897.06/297.11 -->_1 active^#(U23(X)) -> c_20(U23^#(active(X))) :20 897.06/297.11 -->_1 active^#(isList(__(V1, V2))) -> 897.06/297.11 c_18(U21^#(and(isPalListKind(V1), isPalListKind(V2)), V1, V2)) :18 897.06/297.11 -->_1 active^#(isList(V)) -> c_17(U11^#(isPalListKind(V), V)) :17 897.06/297.11 -->_1 active^#(U22(tt(), V2)) -> c_16(U23^#(isList(V2))) :16 897.06/297.12 -->_1 active^#(U22(X1, X2)) -> c_15(U22^#(active(X1), X2)) :15 897.06/297.12 -->_1 active^#(U21(tt(), V1, V2)) -> 897.06/297.12 c_14(U22^#(isList(V1), V2)) :14 897.06/297.12 -->_1 active^#(U21(X1, X2, X3)) -> 897.06/297.12 c_13(U21^#(active(X1), X2, X3)) :13 897.06/297.12 -->_1 active^#(isNeList(__(V1, V2))) -> 897.06/297.12 c_12(U51^#(and(isPalListKind(V1), isPalListKind(V2)), V1, V2)) :12 897.06/297.12 -->_1 active^#(isNeList(__(V1, V2))) -> 897.06/297.12 c_11(U41^#(and(isPalListKind(V1), isPalListKind(V2)), V1, V2)) :11 897.06/297.12 -->_1 active^#(isNeList(V)) -> c_10(U31^#(isPalListKind(V), V)) :10 897.06/297.12 -->_1 active^#(U12(X)) -> c_8(U12^#(active(X))) :8 897.06/297.12 -->_1 active^#(U11(tt(), V)) -> c_7(U12^#(isNeList(V))) :7 897.06/297.12 -->_1 active^#(U11(X1, X2)) -> c_6(U11^#(active(X1), X2)) :6 897.06/297.12 -->_1 proper^#(u()) -> c_140() :140 897.06/297.12 -->_1 proper^#(o()) -> c_139() :139 897.06/297.12 -->_1 proper^#(i()) -> c_138() :138 897.06/297.12 -->_1 proper^#(e()) -> c_137() :137 897.06/297.12 -->_1 proper^#(a()) -> c_136() :136 897.06/297.12 -->_1 proper^#(tt()) -> c_112() :112 897.06/297.12 -->_1 proper^#(nil()) -> c_110() :110 897.06/297.12 -->_1 active^#(isPal(nil())) -> c_63() :63 897.06/297.12 -->_1 active^#(isPalListKind(u())) -> c_61() :61 897.06/297.12 -->_1 active^#(isPalListKind(o())) -> c_60() :60 897.06/297.12 -->_1 active^#(isPalListKind(i())) -> c_59() :59 897.06/297.12 -->_1 active^#(isPalListKind(e())) -> c_58() :58 897.06/297.12 -->_1 active^#(isPalListKind(a())) -> c_57() :57 897.06/297.12 -->_1 active^#(isPalListKind(nil())) -> c_56() :56 897.06/297.12 -->_1 active^#(U72(tt())) -> c_50() :50 897.06/297.12 -->_1 active^#(U62(tt())) -> c_46() :46 897.06/297.12 -->_1 active^#(U53(tt())) -> c_42() :42 897.06/297.12 -->_1 active^#(U43(tt())) -> c_36() :36 897.06/297.12 -->_1 active^#(isQid(u())) -> c_30() :30 897.06/297.12 -->_1 active^#(isQid(o())) -> c_29() :29 897.06/297.12 -->_1 active^#(isQid(i())) -> c_28() :28 897.06/297.12 -->_1 active^#(isQid(e())) -> c_27() :27 897.06/297.12 -->_1 active^#(isQid(a())) -> c_26() :26 897.06/297.12 -->_1 active^#(U32(tt())) -> c_25() :25 897.06/297.12 -->_1 active^#(U23(tt())) -> c_21() :21 897.06/297.12 -->_1 active^#(isList(nil())) -> c_19() :19 897.06/297.12 -->_1 active^#(U12(tt())) -> c_9() :9 897.06/297.12 -->_1 active^#(__(nil(), X)) -> c_5(X) :5 897.06/297.12 -->_1 active^#(__(__(X, Y), Z)) -> c_4(__^#(X, __(Y, Z))) :4 897.06/297.12 -->_1 active^#(__(X, nil())) -> c_3(X) :3 897.06/297.12 -->_1 active^#(__(X1, X2)) -> c_2(__^#(active(X1), X2)) :2 897.06/297.12 -->_1 active^#(__(X1, X2)) -> c_1(__^#(X1, active(X2))) :1 897.06/297.12 897.06/297.12 6: active^#(U11(X1, X2)) -> c_6(U11^#(active(X1), X2)) 897.06/297.12 -->_1 U11^#(ok(X1), ok(X2)) -> c_68(U11^#(X1, X2)) :68 897.06/297.12 -->_1 U11^#(mark(X1), X2) -> c_67(U11^#(X1, X2)) :67 897.06/297.12 897.06/297.12 7: active^#(U11(tt(), V)) -> c_7(U12^#(isNeList(V))) 897.06/297.12 -->_1 U12^#(ok(X)) -> c_70(U12^#(X)) :70 897.06/297.12 -->_1 U12^#(mark(X)) -> c_69(U12^#(X)) :69 897.06/297.12 897.06/297.12 8: active^#(U12(X)) -> c_8(U12^#(active(X))) 897.06/297.12 -->_1 U12^#(ok(X)) -> c_70(U12^#(X)) :70 897.06/297.12 -->_1 U12^#(mark(X)) -> c_69(U12^#(X)) :69 897.06/297.12 897.06/297.12 9: active^#(U12(tt())) -> c_9() 897.06/297.12 897.06/297.12 10: active^#(isNeList(V)) -> c_10(U31^#(isPalListKind(V), V)) 897.06/297.12 -->_1 U31^#(ok(X1), ok(X2)) -> c_80(U31^#(X1, X2)) :72 897.06/297.12 -->_1 U31^#(mark(X1), X2) -> c_79(U31^#(X1, X2)) :71 897.06/297.12 897.06/297.12 11: active^#(isNeList(__(V1, V2))) -> 897.06/297.12 c_11(U41^#(and(isPalListKind(V1), isPalListKind(V2)), V1, V2)) 897.06/297.12 -->_1 U41^#(ok(X1), ok(X2), ok(X3)) -> c_85(U41^#(X1, X2, X3)) :74 897.06/297.12 -->_1 U41^#(mark(X1), X2, X3) -> c_84(U41^#(X1, X2, X3)) :73 897.06/297.12 897.06/297.12 12: active^#(isNeList(__(V1, V2))) -> 897.06/297.12 c_12(U51^#(and(isPalListKind(V1), isPalListKind(V2)), V1, V2)) 897.06/297.12 -->_1 U51^#(ok(X1), ok(X2), ok(X3)) -> c_91(U51^#(X1, X2, X3)) :76 897.06/297.12 -->_1 U51^#(mark(X1), X2, X3) -> c_90(U51^#(X1, X2, X3)) :75 897.06/297.12 897.06/297.12 13: active^#(U21(X1, X2, X3)) -> c_13(U21^#(active(X1), X2, X3)) 897.06/297.12 -->_1 U21^#(ok(X1), ok(X2), ok(X3)) -> c_73(U21^#(X1, X2, X3)) :78 897.06/297.12 -->_1 U21^#(mark(X1), X2, X3) -> c_72(U21^#(X1, X2, X3)) :77 897.06/297.12 897.06/297.12 14: active^#(U21(tt(), V1, V2)) -> c_14(U22^#(isList(V1), V2)) 897.06/297.12 -->_1 U22^#(ok(X1), ok(X2)) -> c_75(U22^#(X1, X2)) :80 897.06/297.12 -->_1 U22^#(mark(X1), X2) -> c_74(U22^#(X1, X2)) :79 897.06/297.12 897.06/297.12 15: active^#(U22(X1, X2)) -> c_15(U22^#(active(X1), X2)) 897.06/297.12 -->_1 U22^#(ok(X1), ok(X2)) -> c_75(U22^#(X1, X2)) :80 897.06/297.12 -->_1 U22^#(mark(X1), X2) -> c_74(U22^#(X1, X2)) :79 897.06/297.12 897.06/297.12 16: active^#(U22(tt(), V2)) -> c_16(U23^#(isList(V2))) 897.06/297.12 -->_1 U23^#(ok(X)) -> c_78(U23^#(X)) :82 897.06/297.12 -->_1 U23^#(mark(X)) -> c_77(U23^#(X)) :81 897.06/297.12 897.06/297.12 17: active^#(isList(V)) -> c_17(U11^#(isPalListKind(V), V)) 897.06/297.12 -->_1 U11^#(ok(X1), ok(X2)) -> c_68(U11^#(X1, X2)) :68 897.06/297.12 -->_1 U11^#(mark(X1), X2) -> c_67(U11^#(X1, X2)) :67 897.06/297.12 897.06/297.12 18: active^#(isList(__(V1, V2))) -> 897.06/297.12 c_18(U21^#(and(isPalListKind(V1), isPalListKind(V2)), V1, V2)) 897.06/297.12 -->_1 U21^#(ok(X1), ok(X2), ok(X3)) -> c_73(U21^#(X1, X2, X3)) :78 897.06/297.12 -->_1 U21^#(mark(X1), X2, X3) -> c_72(U21^#(X1, X2, X3)) :77 897.06/297.12 897.06/297.12 19: active^#(isList(nil())) -> c_19() 897.06/297.12 897.06/297.12 20: active^#(U23(X)) -> c_20(U23^#(active(X))) 897.06/297.12 -->_1 U23^#(ok(X)) -> c_78(U23^#(X)) :82 897.06/297.12 -->_1 U23^#(mark(X)) -> c_77(U23^#(X)) :81 897.06/297.12 897.06/297.12 21: active^#(U23(tt())) -> c_21() 897.06/297.12 897.06/297.12 22: active^#(U31(X1, X2)) -> c_22(U31^#(active(X1), X2)) 897.06/297.12 -->_1 U31^#(ok(X1), ok(X2)) -> c_80(U31^#(X1, X2)) :72 897.06/297.12 -->_1 U31^#(mark(X1), X2) -> c_79(U31^#(X1, X2)) :71 897.06/297.12 897.06/297.12 23: active^#(U31(tt(), V)) -> c_23(U32^#(isQid(V))) 897.06/297.12 -->_1 U32^#(ok(X)) -> c_82(U32^#(X)) :84 897.06/297.12 -->_1 U32^#(mark(X)) -> c_81(U32^#(X)) :83 897.06/297.12 897.06/297.12 24: active^#(U32(X)) -> c_24(U32^#(active(X))) 897.06/297.12 -->_1 U32^#(ok(X)) -> c_82(U32^#(X)) :84 897.06/297.12 -->_1 U32^#(mark(X)) -> c_81(U32^#(X)) :83 897.06/297.12 897.06/297.12 25: active^#(U32(tt())) -> c_25() 897.06/297.12 897.06/297.12 26: active^#(isQid(a())) -> c_26() 897.06/297.12 897.06/297.12 27: active^#(isQid(e())) -> c_27() 897.06/297.12 897.06/297.12 28: active^#(isQid(i())) -> c_28() 897.06/297.12 897.06/297.12 29: active^#(isQid(o())) -> c_29() 897.06/297.12 897.06/297.12 30: active^#(isQid(u())) -> c_30() 897.06/297.12 897.06/297.12 31: active^#(U41(X1, X2, X3)) -> c_31(U41^#(active(X1), X2, X3)) 897.06/297.12 -->_1 U41^#(ok(X1), ok(X2), ok(X3)) -> c_85(U41^#(X1, X2, X3)) :74 897.06/297.12 -->_1 U41^#(mark(X1), X2, X3) -> c_84(U41^#(X1, X2, X3)) :73 897.06/297.12 897.06/297.12 32: active^#(U41(tt(), V1, V2)) -> c_32(U42^#(isList(V1), V2)) 897.06/297.12 -->_1 U42^#(ok(X1), ok(X2)) -> c_87(U42^#(X1, X2)) :86 897.06/297.12 -->_1 U42^#(mark(X1), X2) -> c_86(U42^#(X1, X2)) :85 897.06/297.12 897.06/297.12 33: active^#(U42(X1, X2)) -> c_33(U42^#(active(X1), X2)) 897.06/297.12 -->_1 U42^#(ok(X1), ok(X2)) -> c_87(U42^#(X1, X2)) :86 897.06/297.12 -->_1 U42^#(mark(X1), X2) -> c_86(U42^#(X1, X2)) :85 897.06/297.12 897.06/297.12 34: active^#(U42(tt(), V2)) -> c_34(U43^#(isNeList(V2))) 897.06/297.12 -->_1 U43^#(ok(X)) -> c_89(U43^#(X)) :88 897.06/297.12 -->_1 U43^#(mark(X)) -> c_88(U43^#(X)) :87 897.06/297.12 897.06/297.12 35: active^#(U43(X)) -> c_35(U43^#(active(X))) 897.06/297.12 -->_1 U43^#(ok(X)) -> c_89(U43^#(X)) :88 897.06/297.12 -->_1 U43^#(mark(X)) -> c_88(U43^#(X)) :87 897.06/297.12 897.06/297.12 36: active^#(U43(tt())) -> c_36() 897.06/297.12 897.06/297.12 37: active^#(U51(X1, X2, X3)) -> c_37(U51^#(active(X1), X2, X3)) 897.06/297.12 -->_1 U51^#(ok(X1), ok(X2), ok(X3)) -> c_91(U51^#(X1, X2, X3)) :76 897.06/297.12 -->_1 U51^#(mark(X1), X2, X3) -> c_90(U51^#(X1, X2, X3)) :75 897.06/297.12 897.06/297.12 38: active^#(U51(tt(), V1, V2)) -> c_38(U52^#(isNeList(V1), V2)) 897.06/297.12 -->_1 U52^#(ok(X1), ok(X2)) -> c_93(U52^#(X1, X2)) :90 897.06/297.12 -->_1 U52^#(mark(X1), X2) -> c_92(U52^#(X1, X2)) :89 897.06/297.12 897.06/297.12 39: active^#(U52(X1, X2)) -> c_39(U52^#(active(X1), X2)) 897.06/297.12 -->_1 U52^#(ok(X1), ok(X2)) -> c_93(U52^#(X1, X2)) :90 897.06/297.12 -->_1 U52^#(mark(X1), X2) -> c_92(U52^#(X1, X2)) :89 897.06/297.12 897.06/297.12 40: active^#(U52(tt(), V2)) -> c_40(U53^#(isList(V2))) 897.06/297.12 -->_1 U53^#(ok(X)) -> c_95(U53^#(X)) :92 897.06/297.12 -->_1 U53^#(mark(X)) -> c_94(U53^#(X)) :91 897.06/297.12 897.06/297.12 41: active^#(U53(X)) -> c_41(U53^#(active(X))) 897.06/297.12 -->_1 U53^#(ok(X)) -> c_95(U53^#(X)) :92 897.06/297.12 -->_1 U53^#(mark(X)) -> c_94(U53^#(X)) :91 897.06/297.12 897.06/297.12 42: active^#(U53(tt())) -> c_42() 897.06/297.12 897.06/297.12 43: active^#(U61(X1, X2)) -> c_43(U61^#(active(X1), X2)) 897.06/297.12 -->_1 U61^#(ok(X1), ok(X2)) -> c_97(U61^#(X1, X2)) :94 897.06/297.13 -->_1 U61^#(mark(X1), X2) -> c_96(U61^#(X1, X2)) :93 897.06/297.13 897.06/297.13 44: active^#(U61(tt(), V)) -> c_44(U62^#(isQid(V))) 897.06/297.13 -->_1 U62^#(ok(X)) -> c_99(U62^#(X)) :96 897.06/297.13 -->_1 U62^#(mark(X)) -> c_98(U62^#(X)) :95 897.06/297.13 897.06/297.13 45: active^#(U62(X)) -> c_45(U62^#(active(X))) 897.06/297.13 -->_1 U62^#(ok(X)) -> c_99(U62^#(X)) :96 897.06/297.13 -->_1 U62^#(mark(X)) -> c_98(U62^#(X)) :95 897.06/297.13 897.06/297.13 46: active^#(U62(tt())) -> c_46() 897.06/297.13 897.06/297.13 47: active^#(U71(X1, X2)) -> c_47(U71^#(active(X1), X2)) 897.06/297.13 -->_1 U71^#(ok(X1), ok(X2)) -> c_101(U71^#(X1, X2)) :98 897.06/297.13 -->_1 U71^#(mark(X1), X2) -> c_100(U71^#(X1, X2)) :97 897.06/297.13 897.06/297.13 48: active^#(U71(tt(), V)) -> c_48(U72^#(isNePal(V))) 897.06/297.13 -->_1 U72^#(ok(X)) -> c_103(U72^#(X)) :100 897.06/297.13 -->_1 U72^#(mark(X)) -> c_102(U72^#(X)) :99 897.06/297.13 897.06/297.13 49: active^#(U72(X)) -> c_49(U72^#(active(X))) 897.06/297.13 -->_1 U72^#(ok(X)) -> c_103(U72^#(X)) :100 897.06/297.13 -->_1 U72^#(mark(X)) -> c_102(U72^#(X)) :99 897.06/297.13 897.06/297.13 50: active^#(U72(tt())) -> c_50() 897.06/297.13 897.06/297.13 51: active^#(isNePal(V)) -> c_51(U61^#(isPalListKind(V), V)) 897.06/297.13 -->_1 U61^#(ok(X1), ok(X2)) -> c_97(U61^#(X1, X2)) :94 897.06/297.13 -->_1 U61^#(mark(X1), X2) -> c_96(U61^#(X1, X2)) :93 897.06/297.13 897.06/297.13 52: active^#(isNePal(__(I, __(P, I)))) -> 897.06/297.13 c_52(and^#(and(isQid(I), isPalListKind(I)), 897.06/297.13 and(isPal(P), isPalListKind(P)))) 897.06/297.13 -->_1 and^#(ok(X1), ok(X2)) -> c_106(and^#(X1, X2)) :102 897.06/297.13 -->_1 and^#(mark(X1), X2) -> c_105(and^#(X1, X2)) :101 897.06/297.13 897.06/297.13 53: active^#(and(X1, X2)) -> c_53(and^#(active(X1), X2)) 897.06/297.13 -->_1 and^#(ok(X1), ok(X2)) -> c_106(and^#(X1, X2)) :102 897.06/297.13 -->_1 and^#(mark(X1), X2) -> c_105(and^#(X1, X2)) :101 897.06/297.13 897.06/297.13 54: active^#(and(tt(), X)) -> c_54(X) 897.06/297.13 -->_1 top^#(ok(X)) -> c_142(top^#(active(X))) :142 897.06/297.13 -->_1 top^#(mark(X)) -> c_141(top^#(proper(X))) :141 897.06/297.13 -->_1 proper^#(isPal(X)) -> c_135(isPal^#(proper(X))) :135 897.06/297.13 -->_1 proper^#(isPalListKind(X)) -> 897.06/297.13 c_134(isPalListKind^#(proper(X))) :134 897.06/297.13 -->_1 proper^#(and(X1, X2)) -> 897.06/297.13 c_133(and^#(proper(X1), proper(X2))) :133 897.06/297.13 -->_1 proper^#(isNePal(X)) -> c_132(isNePal^#(proper(X))) :132 897.06/297.13 -->_1 proper^#(U72(X)) -> c_131(U72^#(proper(X))) :131 897.06/297.13 -->_1 proper^#(U71(X1, X2)) -> 897.06/297.13 c_130(U71^#(proper(X1), proper(X2))) :130 897.06/297.13 -->_1 proper^#(U62(X)) -> c_129(U62^#(proper(X))) :129 897.06/297.13 -->_1 proper^#(U61(X1, X2)) -> 897.06/297.13 c_128(U61^#(proper(X1), proper(X2))) :128 897.06/297.13 -->_1 proper^#(U53(X)) -> c_127(U53^#(proper(X))) :127 897.06/297.13 -->_1 proper^#(U52(X1, X2)) -> 897.06/297.13 c_126(U52^#(proper(X1), proper(X2))) :126 897.06/297.13 -->_1 proper^#(U51(X1, X2, X3)) -> 897.06/297.13 c_125(U51^#(proper(X1), proper(X2), proper(X3))) :125 897.06/297.13 -->_1 proper^#(U43(X)) -> c_124(U43^#(proper(X))) :124 897.06/297.13 -->_1 proper^#(U42(X1, X2)) -> 897.06/297.13 c_123(U42^#(proper(X1), proper(X2))) :123 897.06/297.13 -->_1 proper^#(U41(X1, X2, X3)) -> 897.06/297.13 c_122(U41^#(proper(X1), proper(X2), proper(X3))) :122 897.06/297.13 -->_1 proper^#(isQid(X)) -> c_121(isQid^#(proper(X))) :121 897.06/297.13 -->_1 proper^#(U32(X)) -> c_120(U32^#(proper(X))) :120 897.06/297.13 -->_1 proper^#(U31(X1, X2)) -> 897.06/297.13 c_119(U31^#(proper(X1), proper(X2))) :119 897.06/297.13 -->_1 proper^#(U23(X)) -> c_118(U23^#(proper(X))) :118 897.06/297.13 -->_1 proper^#(isList(X)) -> c_117(isList^#(proper(X))) :117 897.06/297.13 -->_1 proper^#(U22(X1, X2)) -> 897.06/297.13 c_116(U22^#(proper(X1), proper(X2))) :116 897.06/297.13 -->_1 proper^#(U21(X1, X2, X3)) -> 897.06/297.13 c_115(U21^#(proper(X1), proper(X2), proper(X3))) :115 897.06/297.13 -->_1 proper^#(isNeList(X)) -> c_114(isNeList^#(proper(X))) :114 897.06/297.13 -->_1 proper^#(U12(X)) -> c_113(U12^#(proper(X))) :113 897.06/297.13 -->_1 proper^#(U11(X1, X2)) -> 897.06/297.13 c_111(U11^#(proper(X1), proper(X2))) :111 897.06/297.13 -->_1 proper^#(__(X1, X2)) -> 897.06/297.13 c_109(__^#(proper(X1), proper(X2))) :109 897.06/297.13 -->_1 isPal^#(ok(X)) -> c_108(isPal^#(X)) :108 897.06/297.13 -->_1 isPalListKind^#(ok(X)) -> c_107(isPalListKind^#(X)) :107 897.06/297.13 -->_1 isNePal^#(ok(X)) -> c_104(isNePal^#(X)) :106 897.06/297.13 -->_1 isQid^#(ok(X)) -> c_83(isQid^#(X)) :105 897.06/297.13 -->_1 isList^#(ok(X)) -> c_76(isList^#(X)) :104 897.06/297.13 -->_1 isNeList^#(ok(X)) -> c_71(isNeList^#(X)) :103 897.06/297.13 -->_1 and^#(ok(X1), ok(X2)) -> c_106(and^#(X1, X2)) :102 897.06/297.13 -->_1 and^#(mark(X1), X2) -> c_105(and^#(X1, X2)) :101 897.06/297.13 -->_1 U72^#(ok(X)) -> c_103(U72^#(X)) :100 897.06/297.13 -->_1 U72^#(mark(X)) -> c_102(U72^#(X)) :99 897.06/297.13 -->_1 U71^#(ok(X1), ok(X2)) -> c_101(U71^#(X1, X2)) :98 897.06/297.13 -->_1 U71^#(mark(X1), X2) -> c_100(U71^#(X1, X2)) :97 897.06/297.13 -->_1 U62^#(ok(X)) -> c_99(U62^#(X)) :96 897.06/297.13 -->_1 U62^#(mark(X)) -> c_98(U62^#(X)) :95 897.06/297.13 -->_1 U61^#(ok(X1), ok(X2)) -> c_97(U61^#(X1, X2)) :94 897.06/297.13 -->_1 U61^#(mark(X1), X2) -> c_96(U61^#(X1, X2)) :93 897.06/297.13 -->_1 U53^#(ok(X)) -> c_95(U53^#(X)) :92 897.06/297.13 -->_1 U53^#(mark(X)) -> c_94(U53^#(X)) :91 897.06/297.13 -->_1 U52^#(ok(X1), ok(X2)) -> c_93(U52^#(X1, X2)) :90 897.06/297.13 -->_1 U52^#(mark(X1), X2) -> c_92(U52^#(X1, X2)) :89 897.06/297.13 -->_1 U43^#(ok(X)) -> c_89(U43^#(X)) :88 897.06/297.13 -->_1 U43^#(mark(X)) -> c_88(U43^#(X)) :87 897.06/297.13 -->_1 U42^#(ok(X1), ok(X2)) -> c_87(U42^#(X1, X2)) :86 897.06/297.13 -->_1 U42^#(mark(X1), X2) -> c_86(U42^#(X1, X2)) :85 897.06/297.13 -->_1 U32^#(ok(X)) -> c_82(U32^#(X)) :84 897.06/297.13 -->_1 U32^#(mark(X)) -> c_81(U32^#(X)) :83 897.06/297.13 -->_1 U23^#(ok(X)) -> c_78(U23^#(X)) :82 897.06/297.13 -->_1 U23^#(mark(X)) -> c_77(U23^#(X)) :81 897.06/297.13 -->_1 U22^#(ok(X1), ok(X2)) -> c_75(U22^#(X1, X2)) :80 897.06/297.13 -->_1 U22^#(mark(X1), X2) -> c_74(U22^#(X1, X2)) :79 897.06/297.13 -->_1 U21^#(ok(X1), ok(X2), ok(X3)) -> c_73(U21^#(X1, X2, X3)) :78 897.06/297.13 -->_1 U21^#(mark(X1), X2, X3) -> c_72(U21^#(X1, X2, X3)) :77 897.06/297.13 -->_1 U51^#(ok(X1), ok(X2), ok(X3)) -> c_91(U51^#(X1, X2, X3)) :76 897.06/297.13 -->_1 U51^#(mark(X1), X2, X3) -> c_90(U51^#(X1, X2, X3)) :75 897.06/297.13 -->_1 U41^#(ok(X1), ok(X2), ok(X3)) -> c_85(U41^#(X1, X2, X3)) :74 897.06/297.13 -->_1 U41^#(mark(X1), X2, X3) -> c_84(U41^#(X1, X2, X3)) :73 897.06/297.13 -->_1 U31^#(ok(X1), ok(X2)) -> c_80(U31^#(X1, X2)) :72 897.06/297.13 -->_1 U31^#(mark(X1), X2) -> c_79(U31^#(X1, X2)) :71 897.06/297.13 -->_1 U12^#(ok(X)) -> c_70(U12^#(X)) :70 897.06/297.13 -->_1 U12^#(mark(X)) -> c_69(U12^#(X)) :69 897.06/297.13 -->_1 U11^#(ok(X1), ok(X2)) -> c_68(U11^#(X1, X2)) :68 897.06/297.13 -->_1 U11^#(mark(X1), X2) -> c_67(U11^#(X1, X2)) :67 897.06/297.13 -->_1 __^#(ok(X1), ok(X2)) -> c_66(__^#(X1, X2)) :66 897.06/297.13 -->_1 __^#(mark(X1), X2) -> c_65(__^#(X1, X2)) :65 897.06/297.13 -->_1 __^#(X1, mark(X2)) -> c_64(__^#(X1, X2)) :64 897.06/297.13 -->_1 active^#(isPal(V)) -> c_62(U71^#(isPalListKind(V), V)) :62 897.06/297.13 -->_1 active^#(isPalListKind(__(V1, V2))) -> 897.06/297.13 c_55(and^#(isPalListKind(V1), isPalListKind(V2))) :55 897.06/297.13 -->_1 proper^#(u()) -> c_140() :140 897.06/297.13 -->_1 proper^#(o()) -> c_139() :139 897.06/297.13 -->_1 proper^#(i()) -> c_138() :138 897.06/297.13 -->_1 proper^#(e()) -> c_137() :137 897.06/297.13 -->_1 proper^#(a()) -> c_136() :136 897.06/297.13 -->_1 proper^#(tt()) -> c_112() :112 897.06/297.13 -->_1 proper^#(nil()) -> c_110() :110 897.06/297.13 -->_1 active^#(isPal(nil())) -> c_63() :63 897.06/297.13 -->_1 active^#(isPalListKind(u())) -> c_61() :61 897.06/297.13 -->_1 active^#(isPalListKind(o())) -> c_60() :60 897.06/297.13 -->_1 active^#(isPalListKind(i())) -> c_59() :59 897.06/297.13 -->_1 active^#(isPalListKind(e())) -> c_58() :58 897.06/297.13 -->_1 active^#(isPalListKind(a())) -> c_57() :57 897.06/297.13 -->_1 active^#(isPalListKind(nil())) -> c_56() :56 897.06/297.13 -->_1 active^#(and(tt(), X)) -> c_54(X) :54 897.06/297.13 -->_1 active^#(and(X1, X2)) -> c_53(and^#(active(X1), X2)) :53 897.06/297.13 -->_1 active^#(isNePal(__(I, __(P, I)))) -> 897.06/297.13 c_52(and^#(and(isQid(I), isPalListKind(I)), 897.06/297.13 and(isPal(P), isPalListKind(P)))) :52 897.06/297.13 -->_1 active^#(isNePal(V)) -> c_51(U61^#(isPalListKind(V), V)) :51 897.06/297.13 -->_1 active^#(U72(tt())) -> c_50() :50 897.06/297.13 -->_1 active^#(U72(X)) -> c_49(U72^#(active(X))) :49 897.06/297.13 -->_1 active^#(U71(tt(), V)) -> c_48(U72^#(isNePal(V))) :48 897.06/297.13 -->_1 active^#(U71(X1, X2)) -> c_47(U71^#(active(X1), X2)) :47 897.06/297.13 -->_1 active^#(U62(tt())) -> c_46() :46 897.06/297.13 -->_1 active^#(U62(X)) -> c_45(U62^#(active(X))) :45 897.06/297.13 -->_1 active^#(U61(tt(), V)) -> c_44(U62^#(isQid(V))) :44 897.06/297.13 -->_1 active^#(U61(X1, X2)) -> c_43(U61^#(active(X1), X2)) :43 897.06/297.13 -->_1 active^#(U53(tt())) -> c_42() :42 897.06/297.13 -->_1 active^#(U53(X)) -> c_41(U53^#(active(X))) :41 897.06/297.13 -->_1 active^#(U52(tt(), V2)) -> c_40(U53^#(isList(V2))) :40 897.06/297.13 -->_1 active^#(U52(X1, X2)) -> c_39(U52^#(active(X1), X2)) :39 897.06/297.13 -->_1 active^#(U51(tt(), V1, V2)) -> 897.06/297.13 c_38(U52^#(isNeList(V1), V2)) :38 897.06/297.13 -->_1 active^#(U51(X1, X2, X3)) -> 897.06/297.13 c_37(U51^#(active(X1), X2, X3)) :37 897.06/297.13 -->_1 active^#(U43(tt())) -> c_36() :36 897.06/297.13 -->_1 active^#(U43(X)) -> c_35(U43^#(active(X))) :35 897.06/297.13 -->_1 active^#(U42(tt(), V2)) -> c_34(U43^#(isNeList(V2))) :34 897.06/297.13 -->_1 active^#(U42(X1, X2)) -> c_33(U42^#(active(X1), X2)) :33 897.06/297.13 -->_1 active^#(U41(tt(), V1, V2)) -> 897.06/297.13 c_32(U42^#(isList(V1), V2)) :32 897.06/297.13 -->_1 active^#(U41(X1, X2, X3)) -> 897.06/297.13 c_31(U41^#(active(X1), X2, X3)) :31 897.06/297.13 -->_1 active^#(isQid(u())) -> c_30() :30 897.06/297.13 -->_1 active^#(isQid(o())) -> c_29() :29 897.06/297.13 -->_1 active^#(isQid(i())) -> c_28() :28 897.06/297.13 -->_1 active^#(isQid(e())) -> c_27() :27 897.06/297.13 -->_1 active^#(isQid(a())) -> c_26() :26 897.06/297.13 -->_1 active^#(U32(tt())) -> c_25() :25 897.06/297.13 -->_1 active^#(U32(X)) -> c_24(U32^#(active(X))) :24 897.06/297.13 -->_1 active^#(U31(tt(), V)) -> c_23(U32^#(isQid(V))) :23 897.06/297.13 -->_1 active^#(U31(X1, X2)) -> c_22(U31^#(active(X1), X2)) :22 897.06/297.13 -->_1 active^#(U23(tt())) -> c_21() :21 897.06/297.13 -->_1 active^#(U23(X)) -> c_20(U23^#(active(X))) :20 897.06/297.13 -->_1 active^#(isList(nil())) -> c_19() :19 897.06/297.13 -->_1 active^#(isList(__(V1, V2))) -> 897.06/297.13 c_18(U21^#(and(isPalListKind(V1), isPalListKind(V2)), V1, V2)) :18 897.06/297.13 -->_1 active^#(isList(V)) -> c_17(U11^#(isPalListKind(V), V)) :17 897.06/297.13 -->_1 active^#(U22(tt(), V2)) -> c_16(U23^#(isList(V2))) :16 897.06/297.13 -->_1 active^#(U22(X1, X2)) -> c_15(U22^#(active(X1), X2)) :15 897.06/297.13 -->_1 active^#(U21(tt(), V1, V2)) -> 897.06/297.13 c_14(U22^#(isList(V1), V2)) :14 897.06/297.13 -->_1 active^#(U21(X1, X2, X3)) -> 897.06/297.13 c_13(U21^#(active(X1), X2, X3)) :13 897.06/297.13 -->_1 active^#(isNeList(__(V1, V2))) -> 897.06/297.13 c_12(U51^#(and(isPalListKind(V1), isPalListKind(V2)), V1, V2)) :12 897.06/297.13 -->_1 active^#(isNeList(__(V1, V2))) -> 897.06/297.13 c_11(U41^#(and(isPalListKind(V1), isPalListKind(V2)), V1, V2)) :11 897.06/297.13 -->_1 active^#(isNeList(V)) -> c_10(U31^#(isPalListKind(V), V)) :10 897.06/297.13 -->_1 active^#(U12(tt())) -> c_9() :9 897.06/297.13 -->_1 active^#(U12(X)) -> c_8(U12^#(active(X))) :8 897.06/297.13 -->_1 active^#(U11(tt(), V)) -> c_7(U12^#(isNeList(V))) :7 897.06/297.13 -->_1 active^#(U11(X1, X2)) -> c_6(U11^#(active(X1), X2)) :6 897.06/297.13 -->_1 active^#(__(nil(), X)) -> c_5(X) :5 897.06/297.13 -->_1 active^#(__(__(X, Y), Z)) -> c_4(__^#(X, __(Y, Z))) :4 897.06/297.13 -->_1 active^#(__(X, nil())) -> c_3(X) :3 897.06/297.13 -->_1 active^#(__(X1, X2)) -> c_2(__^#(active(X1), X2)) :2 897.06/297.13 -->_1 active^#(__(X1, X2)) -> c_1(__^#(X1, active(X2))) :1 897.06/297.13 897.06/297.13 55: active^#(isPalListKind(__(V1, V2))) -> 897.06/297.13 c_55(and^#(isPalListKind(V1), isPalListKind(V2))) 897.06/297.13 -->_1 and^#(ok(X1), ok(X2)) -> c_106(and^#(X1, X2)) :102 897.06/297.13 -->_1 and^#(mark(X1), X2) -> c_105(and^#(X1, X2)) :101 897.06/297.13 897.06/297.13 56: active^#(isPalListKind(nil())) -> c_56() 897.06/297.13 897.06/297.13 57: active^#(isPalListKind(a())) -> c_57() 897.06/297.13 897.06/297.13 58: active^#(isPalListKind(e())) -> c_58() 897.06/297.13 897.06/297.13 59: active^#(isPalListKind(i())) -> c_59() 897.06/297.13 897.06/297.13 60: active^#(isPalListKind(o())) -> c_60() 897.06/297.13 897.06/297.13 61: active^#(isPalListKind(u())) -> c_61() 897.06/297.13 897.06/297.13 62: active^#(isPal(V)) -> c_62(U71^#(isPalListKind(V), V)) 897.06/297.13 -->_1 U71^#(ok(X1), ok(X2)) -> c_101(U71^#(X1, X2)) :98 897.06/297.13 -->_1 U71^#(mark(X1), X2) -> c_100(U71^#(X1, X2)) :97 897.06/297.13 897.06/297.13 63: active^#(isPal(nil())) -> c_63() 897.06/297.13 897.06/297.13 64: __^#(X1, mark(X2)) -> c_64(__^#(X1, X2)) 897.06/297.13 -->_1 __^#(ok(X1), ok(X2)) -> c_66(__^#(X1, X2)) :66 897.06/297.13 -->_1 __^#(mark(X1), X2) -> c_65(__^#(X1, X2)) :65 897.06/297.13 -->_1 __^#(X1, mark(X2)) -> c_64(__^#(X1, X2)) :64 897.06/297.13 897.06/297.13 65: __^#(mark(X1), X2) -> c_65(__^#(X1, X2)) 897.06/297.13 -->_1 __^#(ok(X1), ok(X2)) -> c_66(__^#(X1, X2)) :66 897.06/297.13 -->_1 __^#(mark(X1), X2) -> c_65(__^#(X1, X2)) :65 897.06/297.13 -->_1 __^#(X1, mark(X2)) -> c_64(__^#(X1, X2)) :64 897.06/297.13 897.06/297.13 66: __^#(ok(X1), ok(X2)) -> c_66(__^#(X1, X2)) 897.06/297.13 -->_1 __^#(ok(X1), ok(X2)) -> c_66(__^#(X1, X2)) :66 897.06/297.13 -->_1 __^#(mark(X1), X2) -> c_65(__^#(X1, X2)) :65 897.06/297.13 -->_1 __^#(X1, mark(X2)) -> c_64(__^#(X1, X2)) :64 897.06/297.13 897.06/297.13 67: U11^#(mark(X1), X2) -> c_67(U11^#(X1, X2)) 897.06/297.13 -->_1 U11^#(ok(X1), ok(X2)) -> c_68(U11^#(X1, X2)) :68 897.06/297.13 -->_1 U11^#(mark(X1), X2) -> c_67(U11^#(X1, X2)) :67 897.06/297.13 897.06/297.13 68: U11^#(ok(X1), ok(X2)) -> c_68(U11^#(X1, X2)) 897.06/297.13 -->_1 U11^#(ok(X1), ok(X2)) -> c_68(U11^#(X1, X2)) :68 897.06/297.13 -->_1 U11^#(mark(X1), X2) -> c_67(U11^#(X1, X2)) :67 897.06/297.13 897.06/297.13 69: U12^#(mark(X)) -> c_69(U12^#(X)) 897.06/297.13 -->_1 U12^#(ok(X)) -> c_70(U12^#(X)) :70 897.06/297.13 -->_1 U12^#(mark(X)) -> c_69(U12^#(X)) :69 897.06/297.13 897.06/297.13 70: U12^#(ok(X)) -> c_70(U12^#(X)) 897.06/297.13 -->_1 U12^#(ok(X)) -> c_70(U12^#(X)) :70 897.06/297.13 -->_1 U12^#(mark(X)) -> c_69(U12^#(X)) :69 897.06/297.13 897.06/297.13 71: U31^#(mark(X1), X2) -> c_79(U31^#(X1, X2)) 897.06/297.13 -->_1 U31^#(ok(X1), ok(X2)) -> c_80(U31^#(X1, X2)) :72 897.06/297.13 -->_1 U31^#(mark(X1), X2) -> c_79(U31^#(X1, X2)) :71 897.06/297.13 897.06/297.13 72: U31^#(ok(X1), ok(X2)) -> c_80(U31^#(X1, X2)) 897.06/297.13 -->_1 U31^#(ok(X1), ok(X2)) -> c_80(U31^#(X1, X2)) :72 897.06/297.13 -->_1 U31^#(mark(X1), X2) -> c_79(U31^#(X1, X2)) :71 897.06/297.13 897.06/297.13 73: U41^#(mark(X1), X2, X3) -> c_84(U41^#(X1, X2, X3)) 897.06/297.13 -->_1 U41^#(ok(X1), ok(X2), ok(X3)) -> c_85(U41^#(X1, X2, X3)) :74 897.06/297.13 -->_1 U41^#(mark(X1), X2, X3) -> c_84(U41^#(X1, X2, X3)) :73 897.06/297.13 897.06/297.13 74: U41^#(ok(X1), ok(X2), ok(X3)) -> c_85(U41^#(X1, X2, X3)) 897.06/297.13 -->_1 U41^#(ok(X1), ok(X2), ok(X3)) -> c_85(U41^#(X1, X2, X3)) :74 897.06/297.13 -->_1 U41^#(mark(X1), X2, X3) -> c_84(U41^#(X1, X2, X3)) :73 897.06/297.13 897.06/297.13 75: U51^#(mark(X1), X2, X3) -> c_90(U51^#(X1, X2, X3)) 897.06/297.13 -->_1 U51^#(ok(X1), ok(X2), ok(X3)) -> c_91(U51^#(X1, X2, X3)) :76 897.06/297.13 -->_1 U51^#(mark(X1), X2, X3) -> c_90(U51^#(X1, X2, X3)) :75 897.06/297.13 897.06/297.13 76: U51^#(ok(X1), ok(X2), ok(X3)) -> c_91(U51^#(X1, X2, X3)) 897.06/297.13 -->_1 U51^#(ok(X1), ok(X2), ok(X3)) -> c_91(U51^#(X1, X2, X3)) :76 897.06/297.13 -->_1 U51^#(mark(X1), X2, X3) -> c_90(U51^#(X1, X2, X3)) :75 897.06/297.13 897.06/297.13 77: U21^#(mark(X1), X2, X3) -> c_72(U21^#(X1, X2, X3)) 897.06/297.13 -->_1 U21^#(ok(X1), ok(X2), ok(X3)) -> c_73(U21^#(X1, X2, X3)) :78 897.06/297.13 -->_1 U21^#(mark(X1), X2, X3) -> c_72(U21^#(X1, X2, X3)) :77 897.06/297.13 897.06/297.13 78: U21^#(ok(X1), ok(X2), ok(X3)) -> c_73(U21^#(X1, X2, X3)) 897.06/297.13 -->_1 U21^#(ok(X1), ok(X2), ok(X3)) -> c_73(U21^#(X1, X2, X3)) :78 897.06/297.13 -->_1 U21^#(mark(X1), X2, X3) -> c_72(U21^#(X1, X2, X3)) :77 897.06/297.13 897.06/297.13 79: U22^#(mark(X1), X2) -> c_74(U22^#(X1, X2)) 897.06/297.13 -->_1 U22^#(ok(X1), ok(X2)) -> c_75(U22^#(X1, X2)) :80 897.06/297.13 -->_1 U22^#(mark(X1), X2) -> c_74(U22^#(X1, X2)) :79 897.06/297.13 897.06/297.13 80: U22^#(ok(X1), ok(X2)) -> c_75(U22^#(X1, X2)) 897.06/297.13 -->_1 U22^#(ok(X1), ok(X2)) -> c_75(U22^#(X1, X2)) :80 897.06/297.13 -->_1 U22^#(mark(X1), X2) -> c_74(U22^#(X1, X2)) :79 897.06/297.13 897.06/297.13 81: U23^#(mark(X)) -> c_77(U23^#(X)) 897.06/297.13 -->_1 U23^#(ok(X)) -> c_78(U23^#(X)) :82 897.06/297.13 -->_1 U23^#(mark(X)) -> c_77(U23^#(X)) :81 897.06/297.13 897.06/297.13 82: U23^#(ok(X)) -> c_78(U23^#(X)) 897.06/297.13 -->_1 U23^#(ok(X)) -> c_78(U23^#(X)) :82 897.06/297.13 -->_1 U23^#(mark(X)) -> c_77(U23^#(X)) :81 897.06/297.13 897.06/297.13 83: U32^#(mark(X)) -> c_81(U32^#(X)) 897.06/297.13 -->_1 U32^#(ok(X)) -> c_82(U32^#(X)) :84 897.06/297.13 -->_1 U32^#(mark(X)) -> c_81(U32^#(X)) :83 897.06/297.13 897.06/297.13 84: U32^#(ok(X)) -> c_82(U32^#(X)) 897.06/297.13 -->_1 U32^#(ok(X)) -> c_82(U32^#(X)) :84 897.06/297.13 -->_1 U32^#(mark(X)) -> c_81(U32^#(X)) :83 897.06/297.13 897.06/297.13 85: U42^#(mark(X1), X2) -> c_86(U42^#(X1, X2)) 897.06/297.13 -->_1 U42^#(ok(X1), ok(X2)) -> c_87(U42^#(X1, X2)) :86 897.06/297.13 -->_1 U42^#(mark(X1), X2) -> c_86(U42^#(X1, X2)) :85 897.06/297.14 897.06/297.14 86: U42^#(ok(X1), ok(X2)) -> c_87(U42^#(X1, X2)) 897.06/297.14 -->_1 U42^#(ok(X1), ok(X2)) -> c_87(U42^#(X1, X2)) :86 897.06/297.14 -->_1 U42^#(mark(X1), X2) -> c_86(U42^#(X1, X2)) :85 897.06/297.14 897.06/297.14 87: U43^#(mark(X)) -> c_88(U43^#(X)) 897.06/297.14 -->_1 U43^#(ok(X)) -> c_89(U43^#(X)) :88 897.06/297.14 -->_1 U43^#(mark(X)) -> c_88(U43^#(X)) :87 897.06/297.14 897.06/297.14 88: U43^#(ok(X)) -> c_89(U43^#(X)) 897.06/297.14 -->_1 U43^#(ok(X)) -> c_89(U43^#(X)) :88 897.06/297.14 -->_1 U43^#(mark(X)) -> c_88(U43^#(X)) :87 897.06/297.14 897.06/297.14 89: U52^#(mark(X1), X2) -> c_92(U52^#(X1, X2)) 897.06/297.14 -->_1 U52^#(ok(X1), ok(X2)) -> c_93(U52^#(X1, X2)) :90 897.06/297.14 -->_1 U52^#(mark(X1), X2) -> c_92(U52^#(X1, X2)) :89 897.06/297.14 897.06/297.14 90: U52^#(ok(X1), ok(X2)) -> c_93(U52^#(X1, X2)) 897.06/297.14 -->_1 U52^#(ok(X1), ok(X2)) -> c_93(U52^#(X1, X2)) :90 897.06/297.14 -->_1 U52^#(mark(X1), X2) -> c_92(U52^#(X1, X2)) :89 897.06/297.14 897.06/297.14 91: U53^#(mark(X)) -> c_94(U53^#(X)) 897.06/297.14 -->_1 U53^#(ok(X)) -> c_95(U53^#(X)) :92 897.06/297.14 -->_1 U53^#(mark(X)) -> c_94(U53^#(X)) :91 897.06/297.14 897.06/297.14 92: U53^#(ok(X)) -> c_95(U53^#(X)) 897.06/297.14 -->_1 U53^#(ok(X)) -> c_95(U53^#(X)) :92 897.06/297.14 -->_1 U53^#(mark(X)) -> c_94(U53^#(X)) :91 897.06/297.14 897.06/297.14 93: U61^#(mark(X1), X2) -> c_96(U61^#(X1, X2)) 897.06/297.14 -->_1 U61^#(ok(X1), ok(X2)) -> c_97(U61^#(X1, X2)) :94 897.06/297.14 -->_1 U61^#(mark(X1), X2) -> c_96(U61^#(X1, X2)) :93 897.06/297.14 897.06/297.14 94: U61^#(ok(X1), ok(X2)) -> c_97(U61^#(X1, X2)) 897.06/297.14 -->_1 U61^#(ok(X1), ok(X2)) -> c_97(U61^#(X1, X2)) :94 897.06/297.14 -->_1 U61^#(mark(X1), X2) -> c_96(U61^#(X1, X2)) :93 897.06/297.14 897.06/297.14 95: U62^#(mark(X)) -> c_98(U62^#(X)) 897.06/297.14 -->_1 U62^#(ok(X)) -> c_99(U62^#(X)) :96 897.06/297.14 -->_1 U62^#(mark(X)) -> c_98(U62^#(X)) :95 897.06/297.14 897.06/297.14 96: U62^#(ok(X)) -> c_99(U62^#(X)) 897.06/297.14 -->_1 U62^#(ok(X)) -> c_99(U62^#(X)) :96 897.06/297.14 -->_1 U62^#(mark(X)) -> c_98(U62^#(X)) :95 897.06/297.14 897.06/297.14 97: U71^#(mark(X1), X2) -> c_100(U71^#(X1, X2)) 897.06/297.14 -->_1 U71^#(ok(X1), ok(X2)) -> c_101(U71^#(X1, X2)) :98 897.06/297.14 -->_1 U71^#(mark(X1), X2) -> c_100(U71^#(X1, X2)) :97 897.06/297.14 897.06/297.14 98: U71^#(ok(X1), ok(X2)) -> c_101(U71^#(X1, X2)) 897.06/297.14 -->_1 U71^#(ok(X1), ok(X2)) -> c_101(U71^#(X1, X2)) :98 897.06/297.14 -->_1 U71^#(mark(X1), X2) -> c_100(U71^#(X1, X2)) :97 897.06/297.14 897.06/297.14 99: U72^#(mark(X)) -> c_102(U72^#(X)) 897.06/297.14 -->_1 U72^#(ok(X)) -> c_103(U72^#(X)) :100 897.06/297.14 -->_1 U72^#(mark(X)) -> c_102(U72^#(X)) :99 897.06/297.14 897.06/297.14 100: U72^#(ok(X)) -> c_103(U72^#(X)) 897.06/297.14 -->_1 U72^#(ok(X)) -> c_103(U72^#(X)) :100 897.06/297.14 -->_1 U72^#(mark(X)) -> c_102(U72^#(X)) :99 897.06/297.14 897.06/297.14 101: and^#(mark(X1), X2) -> c_105(and^#(X1, X2)) 897.06/297.14 -->_1 and^#(ok(X1), ok(X2)) -> c_106(and^#(X1, X2)) :102 897.06/297.14 -->_1 and^#(mark(X1), X2) -> c_105(and^#(X1, X2)) :101 897.06/297.14 897.06/297.14 102: and^#(ok(X1), ok(X2)) -> c_106(and^#(X1, X2)) 897.06/297.14 -->_1 and^#(ok(X1), ok(X2)) -> c_106(and^#(X1, X2)) :102 897.06/297.14 -->_1 and^#(mark(X1), X2) -> c_105(and^#(X1, X2)) :101 897.06/297.14 897.06/297.14 103: isNeList^#(ok(X)) -> c_71(isNeList^#(X)) 897.06/297.14 -->_1 isNeList^#(ok(X)) -> c_71(isNeList^#(X)) :103 897.06/297.14 897.06/297.14 104: isList^#(ok(X)) -> c_76(isList^#(X)) 897.06/297.14 -->_1 isList^#(ok(X)) -> c_76(isList^#(X)) :104 897.06/297.14 897.06/297.14 105: isQid^#(ok(X)) -> c_83(isQid^#(X)) 897.06/297.14 -->_1 isQid^#(ok(X)) -> c_83(isQid^#(X)) :105 897.06/297.14 897.06/297.14 106: isNePal^#(ok(X)) -> c_104(isNePal^#(X)) 897.06/297.14 -->_1 isNePal^#(ok(X)) -> c_104(isNePal^#(X)) :106 897.06/297.14 897.06/297.14 107: isPalListKind^#(ok(X)) -> c_107(isPalListKind^#(X)) 897.06/297.14 -->_1 isPalListKind^#(ok(X)) -> c_107(isPalListKind^#(X)) :107 897.06/297.14 897.06/297.14 108: isPal^#(ok(X)) -> c_108(isPal^#(X)) 897.06/297.14 -->_1 isPal^#(ok(X)) -> c_108(isPal^#(X)) :108 897.06/297.14 897.06/297.14 109: proper^#(__(X1, X2)) -> c_109(__^#(proper(X1), proper(X2))) 897.06/297.14 -->_1 __^#(ok(X1), ok(X2)) -> c_66(__^#(X1, X2)) :66 897.06/297.14 -->_1 __^#(mark(X1), X2) -> c_65(__^#(X1, X2)) :65 897.06/297.14 -->_1 __^#(X1, mark(X2)) -> c_64(__^#(X1, X2)) :64 897.06/297.14 897.06/297.14 110: proper^#(nil()) -> c_110() 897.06/297.14 897.06/297.14 111: proper^#(U11(X1, X2)) -> c_111(U11^#(proper(X1), proper(X2))) 897.06/297.14 -->_1 U11^#(ok(X1), ok(X2)) -> c_68(U11^#(X1, X2)) :68 897.06/297.14 -->_1 U11^#(mark(X1), X2) -> c_67(U11^#(X1, X2)) :67 897.06/297.14 897.06/297.14 112: proper^#(tt()) -> c_112() 897.06/297.14 897.06/297.14 113: proper^#(U12(X)) -> c_113(U12^#(proper(X))) 897.06/297.14 -->_1 U12^#(ok(X)) -> c_70(U12^#(X)) :70 897.06/297.14 -->_1 U12^#(mark(X)) -> c_69(U12^#(X)) :69 897.06/297.14 897.06/297.14 114: proper^#(isNeList(X)) -> c_114(isNeList^#(proper(X))) 897.06/297.14 -->_1 isNeList^#(ok(X)) -> c_71(isNeList^#(X)) :103 897.06/297.14 897.06/297.14 115: proper^#(U21(X1, X2, X3)) -> 897.06/297.14 c_115(U21^#(proper(X1), proper(X2), proper(X3))) 897.06/297.14 -->_1 U21^#(ok(X1), ok(X2), ok(X3)) -> c_73(U21^#(X1, X2, X3)) :78 897.06/297.14 -->_1 U21^#(mark(X1), X2, X3) -> c_72(U21^#(X1, X2, X3)) :77 897.06/297.14 897.06/297.14 116: proper^#(U22(X1, X2)) -> c_116(U22^#(proper(X1), proper(X2))) 897.06/297.14 -->_1 U22^#(ok(X1), ok(X2)) -> c_75(U22^#(X1, X2)) :80 897.06/297.14 -->_1 U22^#(mark(X1), X2) -> c_74(U22^#(X1, X2)) :79 897.06/297.14 897.06/297.14 117: proper^#(isList(X)) -> c_117(isList^#(proper(X))) 897.06/297.14 -->_1 isList^#(ok(X)) -> c_76(isList^#(X)) :104 897.06/297.14 897.06/297.14 118: proper^#(U23(X)) -> c_118(U23^#(proper(X))) 897.06/297.14 -->_1 U23^#(ok(X)) -> c_78(U23^#(X)) :82 897.06/297.14 -->_1 U23^#(mark(X)) -> c_77(U23^#(X)) :81 897.06/297.14 897.06/297.14 119: proper^#(U31(X1, X2)) -> c_119(U31^#(proper(X1), proper(X2))) 897.06/297.14 -->_1 U31^#(ok(X1), ok(X2)) -> c_80(U31^#(X1, X2)) :72 897.06/297.14 -->_1 U31^#(mark(X1), X2) -> c_79(U31^#(X1, X2)) :71 897.06/297.14 897.06/297.14 120: proper^#(U32(X)) -> c_120(U32^#(proper(X))) 897.06/297.14 -->_1 U32^#(ok(X)) -> c_82(U32^#(X)) :84 897.06/297.14 -->_1 U32^#(mark(X)) -> c_81(U32^#(X)) :83 897.06/297.14 897.06/297.14 121: proper^#(isQid(X)) -> c_121(isQid^#(proper(X))) 897.06/297.14 -->_1 isQid^#(ok(X)) -> c_83(isQid^#(X)) :105 897.06/297.14 897.06/297.14 122: proper^#(U41(X1, X2, X3)) -> 897.06/297.14 c_122(U41^#(proper(X1), proper(X2), proper(X3))) 897.06/297.14 -->_1 U41^#(ok(X1), ok(X2), ok(X3)) -> c_85(U41^#(X1, X2, X3)) :74 897.06/297.14 -->_1 U41^#(mark(X1), X2, X3) -> c_84(U41^#(X1, X2, X3)) :73 897.06/297.14 897.06/297.14 123: proper^#(U42(X1, X2)) -> c_123(U42^#(proper(X1), proper(X2))) 897.06/297.14 -->_1 U42^#(ok(X1), ok(X2)) -> c_87(U42^#(X1, X2)) :86 897.06/297.14 -->_1 U42^#(mark(X1), X2) -> c_86(U42^#(X1, X2)) :85 897.06/297.14 897.06/297.14 124: proper^#(U43(X)) -> c_124(U43^#(proper(X))) 897.06/297.14 -->_1 U43^#(ok(X)) -> c_89(U43^#(X)) :88 897.06/297.14 -->_1 U43^#(mark(X)) -> c_88(U43^#(X)) :87 897.06/297.14 897.06/297.14 125: proper^#(U51(X1, X2, X3)) -> 897.06/297.14 c_125(U51^#(proper(X1), proper(X2), proper(X3))) 897.06/297.14 -->_1 U51^#(ok(X1), ok(X2), ok(X3)) -> c_91(U51^#(X1, X2, X3)) :76 897.06/297.14 -->_1 U51^#(mark(X1), X2, X3) -> c_90(U51^#(X1, X2, X3)) :75 897.06/297.14 897.06/297.14 126: proper^#(U52(X1, X2)) -> c_126(U52^#(proper(X1), proper(X2))) 897.06/297.14 -->_1 U52^#(ok(X1), ok(X2)) -> c_93(U52^#(X1, X2)) :90 897.06/297.14 -->_1 U52^#(mark(X1), X2) -> c_92(U52^#(X1, X2)) :89 897.06/297.14 897.06/297.14 127: proper^#(U53(X)) -> c_127(U53^#(proper(X))) 897.06/297.14 -->_1 U53^#(ok(X)) -> c_95(U53^#(X)) :92 897.06/297.14 -->_1 U53^#(mark(X)) -> c_94(U53^#(X)) :91 897.06/297.14 897.06/297.14 128: proper^#(U61(X1, X2)) -> c_128(U61^#(proper(X1), proper(X2))) 897.06/297.14 -->_1 U61^#(ok(X1), ok(X2)) -> c_97(U61^#(X1, X2)) :94 897.06/297.14 -->_1 U61^#(mark(X1), X2) -> c_96(U61^#(X1, X2)) :93 897.06/297.14 897.06/297.14 129: proper^#(U62(X)) -> c_129(U62^#(proper(X))) 897.06/297.14 -->_1 U62^#(ok(X)) -> c_99(U62^#(X)) :96 897.06/297.14 -->_1 U62^#(mark(X)) -> c_98(U62^#(X)) :95 897.06/297.14 897.06/297.14 130: proper^#(U71(X1, X2)) -> c_130(U71^#(proper(X1), proper(X2))) 897.06/297.14 -->_1 U71^#(ok(X1), ok(X2)) -> c_101(U71^#(X1, X2)) :98 897.06/297.14 -->_1 U71^#(mark(X1), X2) -> c_100(U71^#(X1, X2)) :97 897.06/297.14 897.06/297.14 131: proper^#(U72(X)) -> c_131(U72^#(proper(X))) 897.06/297.14 -->_1 U72^#(ok(X)) -> c_103(U72^#(X)) :100 897.06/297.14 -->_1 U72^#(mark(X)) -> c_102(U72^#(X)) :99 897.06/297.14 897.06/297.14 132: proper^#(isNePal(X)) -> c_132(isNePal^#(proper(X))) 897.06/297.14 -->_1 isNePal^#(ok(X)) -> c_104(isNePal^#(X)) :106 897.06/297.14 897.06/297.14 133: proper^#(and(X1, X2)) -> c_133(and^#(proper(X1), proper(X2))) 897.06/297.14 -->_1 and^#(ok(X1), ok(X2)) -> c_106(and^#(X1, X2)) :102 897.06/297.14 -->_1 and^#(mark(X1), X2) -> c_105(and^#(X1, X2)) :101 897.06/297.14 897.06/297.14 134: proper^#(isPalListKind(X)) -> 897.06/297.14 c_134(isPalListKind^#(proper(X))) 897.06/297.14 -->_1 isPalListKind^#(ok(X)) -> c_107(isPalListKind^#(X)) :107 897.06/297.14 897.06/297.14 135: proper^#(isPal(X)) -> c_135(isPal^#(proper(X))) 897.06/297.14 -->_1 isPal^#(ok(X)) -> c_108(isPal^#(X)) :108 897.06/297.14 897.06/297.14 136: proper^#(a()) -> c_136() 897.06/297.14 897.06/297.14 137: proper^#(e()) -> c_137() 897.06/297.14 897.06/297.14 138: proper^#(i()) -> c_138() 897.06/297.14 897.06/297.14 139: proper^#(o()) -> c_139() 897.06/297.14 897.06/297.14 140: proper^#(u()) -> c_140() 897.06/297.14 897.06/297.14 141: top^#(mark(X)) -> c_141(top^#(proper(X))) 897.06/297.14 -->_1 top^#(ok(X)) -> c_142(top^#(active(X))) :142 897.06/297.14 -->_1 top^#(mark(X)) -> c_141(top^#(proper(X))) :141 897.06/297.14 897.06/297.14 142: top^#(ok(X)) -> c_142(top^#(active(X))) 897.06/297.14 -->_1 top^#(ok(X)) -> c_142(top^#(active(X))) :142 897.06/297.14 -->_1 top^#(mark(X)) -> c_141(top^#(proper(X))) :141 897.06/297.14 897.06/297.14 897.06/297.14 Only the nodes 897.06/297.14 {64,66,65,67,68,69,70,71,72,73,74,75,76,77,78,79,80,81,82,83,84,85,86,87,88,89,90,91,92,93,94,95,96,97,98,99,100,101,102,103,104,105,106,107,108,110,112,136,137,138,139,140,141,142} 897.06/297.14 are reachable from nodes 897.06/297.14 {64,65,66,67,68,69,70,71,72,73,74,75,76,77,78,79,80,81,82,83,84,85,86,87,88,89,90,91,92,93,94,95,96,97,98,99,100,101,102,103,104,105,106,107,108,110,112,136,137,138,139,140,141,142} 897.06/297.14 that start derivation from marked basic terms. The nodes not 897.06/297.14 reachable are removed from the problem. 897.06/297.14 897.06/297.14 We are left with following problem, upon which TcT provides the 897.06/297.14 certificate MAYBE. 897.06/297.14 897.06/297.14 Strict DPs: 897.06/297.14 { __^#(X1, mark(X2)) -> c_64(__^#(X1, X2)) 897.06/297.14 , __^#(mark(X1), X2) -> c_65(__^#(X1, X2)) 897.06/297.14 , __^#(ok(X1), ok(X2)) -> c_66(__^#(X1, X2)) 897.06/297.14 , U11^#(mark(X1), X2) -> c_67(U11^#(X1, X2)) 897.06/297.14 , U11^#(ok(X1), ok(X2)) -> c_68(U11^#(X1, X2)) 897.06/297.14 , U12^#(mark(X)) -> c_69(U12^#(X)) 897.06/297.14 , U12^#(ok(X)) -> c_70(U12^#(X)) 897.06/297.14 , U31^#(mark(X1), X2) -> c_79(U31^#(X1, X2)) 897.06/297.14 , U31^#(ok(X1), ok(X2)) -> c_80(U31^#(X1, X2)) 897.06/297.14 , U41^#(mark(X1), X2, X3) -> c_84(U41^#(X1, X2, X3)) 897.06/297.14 , U41^#(ok(X1), ok(X2), ok(X3)) -> c_85(U41^#(X1, X2, X3)) 897.06/297.14 , U51^#(mark(X1), X2, X3) -> c_90(U51^#(X1, X2, X3)) 897.06/297.14 , U51^#(ok(X1), ok(X2), ok(X3)) -> c_91(U51^#(X1, X2, X3)) 897.06/297.14 , U21^#(mark(X1), X2, X3) -> c_72(U21^#(X1, X2, X3)) 897.06/297.14 , U21^#(ok(X1), ok(X2), ok(X3)) -> c_73(U21^#(X1, X2, X3)) 897.06/297.14 , U22^#(mark(X1), X2) -> c_74(U22^#(X1, X2)) 897.06/297.14 , U22^#(ok(X1), ok(X2)) -> c_75(U22^#(X1, X2)) 897.06/297.14 , U23^#(mark(X)) -> c_77(U23^#(X)) 897.06/297.14 , U23^#(ok(X)) -> c_78(U23^#(X)) 897.06/297.14 , U32^#(mark(X)) -> c_81(U32^#(X)) 897.06/297.14 , U32^#(ok(X)) -> c_82(U32^#(X)) 897.06/297.14 , U42^#(mark(X1), X2) -> c_86(U42^#(X1, X2)) 897.06/297.14 , U42^#(ok(X1), ok(X2)) -> c_87(U42^#(X1, X2)) 897.06/297.14 , U43^#(mark(X)) -> c_88(U43^#(X)) 897.06/297.14 , U43^#(ok(X)) -> c_89(U43^#(X)) 897.06/297.14 , U52^#(mark(X1), X2) -> c_92(U52^#(X1, X2)) 897.06/297.14 , U52^#(ok(X1), ok(X2)) -> c_93(U52^#(X1, X2)) 897.06/297.14 , U53^#(mark(X)) -> c_94(U53^#(X)) 897.06/297.14 , U53^#(ok(X)) -> c_95(U53^#(X)) 897.06/297.14 , U61^#(mark(X1), X2) -> c_96(U61^#(X1, X2)) 897.06/297.14 , U61^#(ok(X1), ok(X2)) -> c_97(U61^#(X1, X2)) 897.06/297.14 , U62^#(mark(X)) -> c_98(U62^#(X)) 897.06/297.14 , U62^#(ok(X)) -> c_99(U62^#(X)) 897.06/297.14 , U71^#(mark(X1), X2) -> c_100(U71^#(X1, X2)) 897.06/297.14 , U71^#(ok(X1), ok(X2)) -> c_101(U71^#(X1, X2)) 897.06/297.14 , U72^#(mark(X)) -> c_102(U72^#(X)) 897.06/297.14 , U72^#(ok(X)) -> c_103(U72^#(X)) 897.06/297.14 , and^#(mark(X1), X2) -> c_105(and^#(X1, X2)) 897.06/297.14 , and^#(ok(X1), ok(X2)) -> c_106(and^#(X1, X2)) 897.06/297.14 , isNeList^#(ok(X)) -> c_71(isNeList^#(X)) 897.06/297.14 , isList^#(ok(X)) -> c_76(isList^#(X)) 897.06/297.14 , isQid^#(ok(X)) -> c_83(isQid^#(X)) 897.06/297.14 , isNePal^#(ok(X)) -> c_104(isNePal^#(X)) 897.06/297.14 , isPalListKind^#(ok(X)) -> c_107(isPalListKind^#(X)) 897.06/297.14 , isPal^#(ok(X)) -> c_108(isPal^#(X)) 897.06/297.14 , proper^#(nil()) -> c_110() 897.06/297.14 , proper^#(tt()) -> c_112() 897.06/297.14 , proper^#(a()) -> c_136() 897.06/297.14 , proper^#(e()) -> c_137() 897.06/297.14 , proper^#(i()) -> c_138() 897.06/297.14 , proper^#(o()) -> c_139() 897.06/297.14 , proper^#(u()) -> c_140() 897.06/297.14 , top^#(mark(X)) -> c_141(top^#(proper(X))) 897.06/297.14 , top^#(ok(X)) -> c_142(top^#(active(X))) } 897.06/297.14 Strict Trs: 897.06/297.14 { active(__(X1, X2)) -> __(X1, active(X2)) 897.06/297.14 , active(__(X1, X2)) -> __(active(X1), X2) 897.06/297.14 , active(__(X, nil())) -> mark(X) 897.06/297.14 , active(__(__(X, Y), Z)) -> mark(__(X, __(Y, Z))) 897.06/297.14 , active(__(nil(), X)) -> mark(X) 897.06/297.14 , active(U11(X1, X2)) -> U11(active(X1), X2) 897.06/297.14 , active(U11(tt(), V)) -> mark(U12(isNeList(V))) 897.06/297.14 , active(U12(X)) -> U12(active(X)) 897.06/297.14 , active(U12(tt())) -> mark(tt()) 897.06/297.14 , active(isNeList(V)) -> mark(U31(isPalListKind(V), V)) 897.06/297.14 , active(isNeList(__(V1, V2))) -> 897.06/297.14 mark(U41(and(isPalListKind(V1), isPalListKind(V2)), V1, V2)) 897.06/297.14 , active(isNeList(__(V1, V2))) -> 897.06/297.14 mark(U51(and(isPalListKind(V1), isPalListKind(V2)), V1, V2)) 897.06/297.14 , active(U21(X1, X2, X3)) -> U21(active(X1), X2, X3) 897.06/297.14 , active(U21(tt(), V1, V2)) -> mark(U22(isList(V1), V2)) 897.06/297.14 , active(U22(X1, X2)) -> U22(active(X1), X2) 897.06/297.14 , active(U22(tt(), V2)) -> mark(U23(isList(V2))) 897.06/297.14 , active(isList(V)) -> mark(U11(isPalListKind(V), V)) 897.06/297.14 , active(isList(__(V1, V2))) -> 897.06/297.14 mark(U21(and(isPalListKind(V1), isPalListKind(V2)), V1, V2)) 897.06/297.14 , active(isList(nil())) -> mark(tt()) 897.06/297.14 , active(U23(X)) -> U23(active(X)) 897.06/297.14 , active(U23(tt())) -> mark(tt()) 897.06/297.14 , active(U31(X1, X2)) -> U31(active(X1), X2) 897.06/297.14 , active(U31(tt(), V)) -> mark(U32(isQid(V))) 897.06/297.14 , active(U32(X)) -> U32(active(X)) 897.06/297.14 , active(U32(tt())) -> mark(tt()) 897.06/297.14 , active(isQid(a())) -> mark(tt()) 897.06/297.14 , active(isQid(e())) -> mark(tt()) 897.06/297.14 , active(isQid(i())) -> mark(tt()) 897.06/297.14 , active(isQid(o())) -> mark(tt()) 897.06/297.14 , active(isQid(u())) -> mark(tt()) 897.06/297.14 , active(U41(X1, X2, X3)) -> U41(active(X1), X2, X3) 897.06/297.14 , active(U41(tt(), V1, V2)) -> mark(U42(isList(V1), V2)) 897.06/297.14 , active(U42(X1, X2)) -> U42(active(X1), X2) 897.06/297.14 , active(U42(tt(), V2)) -> mark(U43(isNeList(V2))) 897.06/297.14 , active(U43(X)) -> U43(active(X)) 897.06/297.14 , active(U43(tt())) -> mark(tt()) 897.06/297.14 , active(U51(X1, X2, X3)) -> U51(active(X1), X2, X3) 897.06/297.14 , active(U51(tt(), V1, V2)) -> mark(U52(isNeList(V1), V2)) 897.06/297.14 , active(U52(X1, X2)) -> U52(active(X1), X2) 897.06/297.14 , active(U52(tt(), V2)) -> mark(U53(isList(V2))) 897.06/297.14 , active(U53(X)) -> U53(active(X)) 897.06/297.14 , active(U53(tt())) -> mark(tt()) 897.06/297.14 , active(U61(X1, X2)) -> U61(active(X1), X2) 897.06/297.14 , active(U61(tt(), V)) -> mark(U62(isQid(V))) 897.06/297.14 , active(U62(X)) -> U62(active(X)) 897.06/297.14 , active(U62(tt())) -> mark(tt()) 897.06/297.14 , active(U71(X1, X2)) -> U71(active(X1), X2) 897.06/297.14 , active(U71(tt(), V)) -> mark(U72(isNePal(V))) 897.06/297.14 , active(U72(X)) -> U72(active(X)) 897.06/297.14 , active(U72(tt())) -> mark(tt()) 897.06/297.14 , active(isNePal(V)) -> mark(U61(isPalListKind(V), V)) 897.06/297.14 , active(isNePal(__(I, __(P, I)))) -> 897.06/297.14 mark(and(and(isQid(I), isPalListKind(I)), 897.06/297.14 and(isPal(P), isPalListKind(P)))) 897.06/297.14 , active(and(X1, X2)) -> and(active(X1), X2) 897.06/297.14 , active(and(tt(), X)) -> mark(X) 897.06/297.14 , active(isPalListKind(__(V1, V2))) -> 897.06/297.14 mark(and(isPalListKind(V1), isPalListKind(V2))) 897.06/297.14 , active(isPalListKind(nil())) -> mark(tt()) 897.06/297.14 , active(isPalListKind(a())) -> mark(tt()) 897.06/297.14 , active(isPalListKind(e())) -> mark(tt()) 897.06/297.14 , active(isPalListKind(i())) -> mark(tt()) 897.06/297.14 , active(isPalListKind(o())) -> mark(tt()) 897.06/297.14 , active(isPalListKind(u())) -> mark(tt()) 897.06/297.14 , active(isPal(V)) -> mark(U71(isPalListKind(V), V)) 897.06/297.14 , active(isPal(nil())) -> mark(tt()) 897.06/297.14 , __(X1, mark(X2)) -> mark(__(X1, X2)) 897.06/297.14 , __(mark(X1), X2) -> mark(__(X1, X2)) 897.06/297.14 , __(ok(X1), ok(X2)) -> ok(__(X1, X2)) 897.06/297.14 , U11(mark(X1), X2) -> mark(U11(X1, X2)) 897.06/297.14 , U11(ok(X1), ok(X2)) -> ok(U11(X1, X2)) 897.06/297.14 , U12(mark(X)) -> mark(U12(X)) 897.06/297.14 , U12(ok(X)) -> ok(U12(X)) 897.06/297.14 , isNeList(ok(X)) -> ok(isNeList(X)) 897.06/297.14 , U21(mark(X1), X2, X3) -> mark(U21(X1, X2, X3)) 897.06/297.14 , U21(ok(X1), ok(X2), ok(X3)) -> ok(U21(X1, X2, X3)) 897.06/297.14 , U22(mark(X1), X2) -> mark(U22(X1, X2)) 897.06/297.14 , U22(ok(X1), ok(X2)) -> ok(U22(X1, X2)) 897.06/297.14 , isList(ok(X)) -> ok(isList(X)) 897.06/297.14 , U23(mark(X)) -> mark(U23(X)) 897.06/297.14 , U23(ok(X)) -> ok(U23(X)) 897.06/297.14 , U31(mark(X1), X2) -> mark(U31(X1, X2)) 897.06/297.14 , U31(ok(X1), ok(X2)) -> ok(U31(X1, X2)) 897.06/297.14 , U32(mark(X)) -> mark(U32(X)) 897.06/297.14 , U32(ok(X)) -> ok(U32(X)) 897.06/297.14 , isQid(ok(X)) -> ok(isQid(X)) 897.06/297.14 , U41(mark(X1), X2, X3) -> mark(U41(X1, X2, X3)) 897.06/297.14 , U41(ok(X1), ok(X2), ok(X3)) -> ok(U41(X1, X2, X3)) 897.06/297.15 , U42(mark(X1), X2) -> mark(U42(X1, X2)) 897.06/297.15 , U42(ok(X1), ok(X2)) -> ok(U42(X1, X2)) 897.06/297.15 , U43(mark(X)) -> mark(U43(X)) 897.06/297.15 , U43(ok(X)) -> ok(U43(X)) 897.06/297.15 , U51(mark(X1), X2, X3) -> mark(U51(X1, X2, X3)) 897.06/297.15 , U51(ok(X1), ok(X2), ok(X3)) -> ok(U51(X1, X2, X3)) 897.06/297.15 , U52(mark(X1), X2) -> mark(U52(X1, X2)) 897.06/297.15 , U52(ok(X1), ok(X2)) -> ok(U52(X1, X2)) 897.06/297.15 , U53(mark(X)) -> mark(U53(X)) 897.06/297.15 , U53(ok(X)) -> ok(U53(X)) 897.06/297.15 , U61(mark(X1), X2) -> mark(U61(X1, X2)) 897.06/297.15 , U61(ok(X1), ok(X2)) -> ok(U61(X1, X2)) 897.06/297.15 , U62(mark(X)) -> mark(U62(X)) 897.06/297.15 , U62(ok(X)) -> ok(U62(X)) 897.06/297.15 , U71(mark(X1), X2) -> mark(U71(X1, X2)) 897.06/297.15 , U71(ok(X1), ok(X2)) -> ok(U71(X1, X2)) 897.06/297.15 , U72(mark(X)) -> mark(U72(X)) 897.06/297.15 , U72(ok(X)) -> ok(U72(X)) 897.06/297.15 , isNePal(ok(X)) -> ok(isNePal(X)) 897.06/297.15 , and(mark(X1), X2) -> mark(and(X1, X2)) 897.06/297.15 , and(ok(X1), ok(X2)) -> ok(and(X1, X2)) 897.06/297.15 , isPalListKind(ok(X)) -> ok(isPalListKind(X)) 897.06/297.15 , isPal(ok(X)) -> ok(isPal(X)) 897.06/297.15 , proper(__(X1, X2)) -> __(proper(X1), proper(X2)) 897.06/297.15 , proper(nil()) -> ok(nil()) 897.06/297.15 , proper(U11(X1, X2)) -> U11(proper(X1), proper(X2)) 897.06/297.15 , proper(tt()) -> ok(tt()) 897.06/297.15 , proper(U12(X)) -> U12(proper(X)) 897.06/297.15 , proper(isNeList(X)) -> isNeList(proper(X)) 897.06/297.15 , proper(U21(X1, X2, X3)) -> 897.06/297.15 U21(proper(X1), proper(X2), proper(X3)) 897.06/297.15 , proper(U22(X1, X2)) -> U22(proper(X1), proper(X2)) 897.06/297.15 , proper(isList(X)) -> isList(proper(X)) 897.06/297.15 , proper(U23(X)) -> U23(proper(X)) 897.06/297.15 , proper(U31(X1, X2)) -> U31(proper(X1), proper(X2)) 897.06/297.15 , proper(U32(X)) -> U32(proper(X)) 897.06/297.15 , proper(isQid(X)) -> isQid(proper(X)) 897.06/297.15 , proper(U41(X1, X2, X3)) -> 897.06/297.15 U41(proper(X1), proper(X2), proper(X3)) 897.06/297.15 , proper(U42(X1, X2)) -> U42(proper(X1), proper(X2)) 897.06/297.15 , proper(U43(X)) -> U43(proper(X)) 897.06/297.15 , proper(U51(X1, X2, X3)) -> 897.06/297.15 U51(proper(X1), proper(X2), proper(X3)) 897.06/297.15 , proper(U52(X1, X2)) -> U52(proper(X1), proper(X2)) 897.06/297.15 , proper(U53(X)) -> U53(proper(X)) 897.06/297.15 , proper(U61(X1, X2)) -> U61(proper(X1), proper(X2)) 897.06/297.15 , proper(U62(X)) -> U62(proper(X)) 897.06/297.15 , proper(U71(X1, X2)) -> U71(proper(X1), proper(X2)) 897.06/297.15 , proper(U72(X)) -> U72(proper(X)) 897.06/297.15 , proper(isNePal(X)) -> isNePal(proper(X)) 897.06/297.15 , proper(and(X1, X2)) -> and(proper(X1), proper(X2)) 897.06/297.15 , proper(isPalListKind(X)) -> isPalListKind(proper(X)) 897.06/297.15 , proper(isPal(X)) -> isPal(proper(X)) 897.06/297.15 , proper(a()) -> ok(a()) 897.06/297.15 , proper(e()) -> ok(e()) 897.06/297.15 , proper(i()) -> ok(i()) 897.06/297.15 , proper(o()) -> ok(o()) 897.06/297.15 , proper(u()) -> ok(u()) 897.06/297.15 , top(mark(X)) -> top(proper(X)) 897.06/297.15 , top(ok(X)) -> top(active(X)) } 897.06/297.15 Obligation: 897.06/297.15 runtime complexity 897.06/297.15 Answer: 897.06/297.15 MAYBE 897.06/297.15 897.06/297.15 We estimate the number of application of {46,47,48,49,50,51,52} by 897.06/297.15 applications of Pre({46,47,48,49,50,51,52}) = {}. Here rules are 897.06/297.15 labeled as follows: 897.06/297.15 897.06/297.15 DPs: 897.06/297.15 { 1: __^#(X1, mark(X2)) -> c_64(__^#(X1, X2)) 897.06/297.15 , 2: __^#(mark(X1), X2) -> c_65(__^#(X1, X2)) 897.06/297.15 , 3: __^#(ok(X1), ok(X2)) -> c_66(__^#(X1, X2)) 897.06/297.15 , 4: U11^#(mark(X1), X2) -> c_67(U11^#(X1, X2)) 897.06/297.15 , 5: U11^#(ok(X1), ok(X2)) -> c_68(U11^#(X1, X2)) 897.06/297.15 , 6: U12^#(mark(X)) -> c_69(U12^#(X)) 897.06/297.15 , 7: U12^#(ok(X)) -> c_70(U12^#(X)) 897.06/297.15 , 8: U31^#(mark(X1), X2) -> c_79(U31^#(X1, X2)) 897.06/297.15 , 9: U31^#(ok(X1), ok(X2)) -> c_80(U31^#(X1, X2)) 897.06/297.15 , 10: U41^#(mark(X1), X2, X3) -> c_84(U41^#(X1, X2, X3)) 897.06/297.15 , 11: U41^#(ok(X1), ok(X2), ok(X3)) -> c_85(U41^#(X1, X2, X3)) 897.06/297.15 , 12: U51^#(mark(X1), X2, X3) -> c_90(U51^#(X1, X2, X3)) 897.06/297.15 , 13: U51^#(ok(X1), ok(X2), ok(X3)) -> c_91(U51^#(X1, X2, X3)) 897.06/297.15 , 14: U21^#(mark(X1), X2, X3) -> c_72(U21^#(X1, X2, X3)) 897.06/297.15 , 15: U21^#(ok(X1), ok(X2), ok(X3)) -> c_73(U21^#(X1, X2, X3)) 897.06/297.15 , 16: U22^#(mark(X1), X2) -> c_74(U22^#(X1, X2)) 897.06/297.15 , 17: U22^#(ok(X1), ok(X2)) -> c_75(U22^#(X1, X2)) 897.06/297.15 , 18: U23^#(mark(X)) -> c_77(U23^#(X)) 897.06/297.15 , 19: U23^#(ok(X)) -> c_78(U23^#(X)) 897.06/297.15 , 20: U32^#(mark(X)) -> c_81(U32^#(X)) 897.06/297.15 , 21: U32^#(ok(X)) -> c_82(U32^#(X)) 897.06/297.15 , 22: U42^#(mark(X1), X2) -> c_86(U42^#(X1, X2)) 897.06/297.15 , 23: U42^#(ok(X1), ok(X2)) -> c_87(U42^#(X1, X2)) 897.06/297.15 , 24: U43^#(mark(X)) -> c_88(U43^#(X)) 897.06/297.15 , 25: U43^#(ok(X)) -> c_89(U43^#(X)) 897.06/297.15 , 26: U52^#(mark(X1), X2) -> c_92(U52^#(X1, X2)) 897.06/297.15 , 27: U52^#(ok(X1), ok(X2)) -> c_93(U52^#(X1, X2)) 897.06/297.15 , 28: U53^#(mark(X)) -> c_94(U53^#(X)) 897.06/297.15 , 29: U53^#(ok(X)) -> c_95(U53^#(X)) 897.06/297.15 , 30: U61^#(mark(X1), X2) -> c_96(U61^#(X1, X2)) 897.06/297.15 , 31: U61^#(ok(X1), ok(X2)) -> c_97(U61^#(X1, X2)) 897.06/297.15 , 32: U62^#(mark(X)) -> c_98(U62^#(X)) 897.06/297.15 , 33: U62^#(ok(X)) -> c_99(U62^#(X)) 897.06/297.15 , 34: U71^#(mark(X1), X2) -> c_100(U71^#(X1, X2)) 897.06/297.15 , 35: U71^#(ok(X1), ok(X2)) -> c_101(U71^#(X1, X2)) 897.06/297.15 , 36: U72^#(mark(X)) -> c_102(U72^#(X)) 897.06/297.15 , 37: U72^#(ok(X)) -> c_103(U72^#(X)) 897.06/297.15 , 38: and^#(mark(X1), X2) -> c_105(and^#(X1, X2)) 897.06/297.15 , 39: and^#(ok(X1), ok(X2)) -> c_106(and^#(X1, X2)) 897.06/297.15 , 40: isNeList^#(ok(X)) -> c_71(isNeList^#(X)) 897.06/297.15 , 41: isList^#(ok(X)) -> c_76(isList^#(X)) 897.06/297.15 , 42: isQid^#(ok(X)) -> c_83(isQid^#(X)) 897.06/297.15 , 43: isNePal^#(ok(X)) -> c_104(isNePal^#(X)) 897.06/297.15 , 44: isPalListKind^#(ok(X)) -> c_107(isPalListKind^#(X)) 897.06/297.15 , 45: isPal^#(ok(X)) -> c_108(isPal^#(X)) 897.06/297.15 , 46: proper^#(nil()) -> c_110() 897.06/297.15 , 47: proper^#(tt()) -> c_112() 897.06/297.15 , 48: proper^#(a()) -> c_136() 897.06/297.15 , 49: proper^#(e()) -> c_137() 897.06/297.15 , 50: proper^#(i()) -> c_138() 897.06/297.15 , 51: proper^#(o()) -> c_139() 897.06/297.15 , 52: proper^#(u()) -> c_140() 897.06/297.15 , 53: top^#(mark(X)) -> c_141(top^#(proper(X))) 897.06/297.15 , 54: top^#(ok(X)) -> c_142(top^#(active(X))) } 897.06/297.15 897.06/297.15 We are left with following problem, upon which TcT provides the 897.06/297.15 certificate MAYBE. 897.06/297.15 897.06/297.15 Strict DPs: 897.06/297.15 { __^#(X1, mark(X2)) -> c_64(__^#(X1, X2)) 897.06/297.15 , __^#(mark(X1), X2) -> c_65(__^#(X1, X2)) 897.06/297.15 , __^#(ok(X1), ok(X2)) -> c_66(__^#(X1, X2)) 897.06/297.15 , U11^#(mark(X1), X2) -> c_67(U11^#(X1, X2)) 897.06/297.15 , U11^#(ok(X1), ok(X2)) -> c_68(U11^#(X1, X2)) 897.06/297.15 , U12^#(mark(X)) -> c_69(U12^#(X)) 897.06/297.15 , U12^#(ok(X)) -> c_70(U12^#(X)) 897.06/297.15 , U31^#(mark(X1), X2) -> c_79(U31^#(X1, X2)) 897.06/297.15 , U31^#(ok(X1), ok(X2)) -> c_80(U31^#(X1, X2)) 897.06/297.15 , U41^#(mark(X1), X2, X3) -> c_84(U41^#(X1, X2, X3)) 897.06/297.15 , U41^#(ok(X1), ok(X2), ok(X3)) -> c_85(U41^#(X1, X2, X3)) 897.06/297.15 , U51^#(mark(X1), X2, X3) -> c_90(U51^#(X1, X2, X3)) 897.06/297.15 , U51^#(ok(X1), ok(X2), ok(X3)) -> c_91(U51^#(X1, X2, X3)) 897.06/297.15 , U21^#(mark(X1), X2, X3) -> c_72(U21^#(X1, X2, X3)) 897.06/297.15 , U21^#(ok(X1), ok(X2), ok(X3)) -> c_73(U21^#(X1, X2, X3)) 897.06/297.15 , U22^#(mark(X1), X2) -> c_74(U22^#(X1, X2)) 897.06/297.15 , U22^#(ok(X1), ok(X2)) -> c_75(U22^#(X1, X2)) 897.06/297.15 , U23^#(mark(X)) -> c_77(U23^#(X)) 897.06/297.15 , U23^#(ok(X)) -> c_78(U23^#(X)) 897.06/297.15 , U32^#(mark(X)) -> c_81(U32^#(X)) 897.06/297.15 , U32^#(ok(X)) -> c_82(U32^#(X)) 897.06/297.15 , U42^#(mark(X1), X2) -> c_86(U42^#(X1, X2)) 897.06/297.15 , U42^#(ok(X1), ok(X2)) -> c_87(U42^#(X1, X2)) 897.06/297.15 , U43^#(mark(X)) -> c_88(U43^#(X)) 897.06/297.15 , U43^#(ok(X)) -> c_89(U43^#(X)) 897.06/297.15 , U52^#(mark(X1), X2) -> c_92(U52^#(X1, X2)) 897.06/297.15 , U52^#(ok(X1), ok(X2)) -> c_93(U52^#(X1, X2)) 897.06/297.15 , U53^#(mark(X)) -> c_94(U53^#(X)) 897.06/297.15 , U53^#(ok(X)) -> c_95(U53^#(X)) 897.06/297.15 , U61^#(mark(X1), X2) -> c_96(U61^#(X1, X2)) 897.06/297.15 , U61^#(ok(X1), ok(X2)) -> c_97(U61^#(X1, X2)) 897.06/297.15 , U62^#(mark(X)) -> c_98(U62^#(X)) 897.06/297.15 , U62^#(ok(X)) -> c_99(U62^#(X)) 897.06/297.15 , U71^#(mark(X1), X2) -> c_100(U71^#(X1, X2)) 897.06/297.15 , U71^#(ok(X1), ok(X2)) -> c_101(U71^#(X1, X2)) 897.06/297.15 , U72^#(mark(X)) -> c_102(U72^#(X)) 897.06/297.15 , U72^#(ok(X)) -> c_103(U72^#(X)) 897.06/297.15 , and^#(mark(X1), X2) -> c_105(and^#(X1, X2)) 897.06/297.15 , and^#(ok(X1), ok(X2)) -> c_106(and^#(X1, X2)) 897.06/297.15 , isNeList^#(ok(X)) -> c_71(isNeList^#(X)) 897.06/297.15 , isList^#(ok(X)) -> c_76(isList^#(X)) 897.06/297.15 , isQid^#(ok(X)) -> c_83(isQid^#(X)) 897.06/297.15 , isNePal^#(ok(X)) -> c_104(isNePal^#(X)) 897.06/297.15 , isPalListKind^#(ok(X)) -> c_107(isPalListKind^#(X)) 897.06/297.15 , isPal^#(ok(X)) -> c_108(isPal^#(X)) 897.06/297.15 , top^#(mark(X)) -> c_141(top^#(proper(X))) 897.06/297.15 , top^#(ok(X)) -> c_142(top^#(active(X))) } 897.06/297.15 Strict Trs: 897.06/297.15 { active(__(X1, X2)) -> __(X1, active(X2)) 897.06/297.15 , active(__(X1, X2)) -> __(active(X1), X2) 897.06/297.15 , active(__(X, nil())) -> mark(X) 897.06/297.15 , active(__(__(X, Y), Z)) -> mark(__(X, __(Y, Z))) 897.06/297.15 , active(__(nil(), X)) -> mark(X) 897.06/297.15 , active(U11(X1, X2)) -> U11(active(X1), X2) 897.06/297.15 , active(U11(tt(), V)) -> mark(U12(isNeList(V))) 897.06/297.15 , active(U12(X)) -> U12(active(X)) 897.06/297.15 , active(U12(tt())) -> mark(tt()) 897.06/297.15 , active(isNeList(V)) -> mark(U31(isPalListKind(V), V)) 897.06/297.15 , active(isNeList(__(V1, V2))) -> 897.06/297.15 mark(U41(and(isPalListKind(V1), isPalListKind(V2)), V1, V2)) 897.06/297.15 , active(isNeList(__(V1, V2))) -> 897.06/297.15 mark(U51(and(isPalListKind(V1), isPalListKind(V2)), V1, V2)) 897.06/297.15 , active(U21(X1, X2, X3)) -> U21(active(X1), X2, X3) 897.06/297.15 , active(U21(tt(), V1, V2)) -> mark(U22(isList(V1), V2)) 897.06/297.15 , active(U22(X1, X2)) -> U22(active(X1), X2) 897.06/297.15 , active(U22(tt(), V2)) -> mark(U23(isList(V2))) 897.06/297.15 , active(isList(V)) -> mark(U11(isPalListKind(V), V)) 897.06/297.15 , active(isList(__(V1, V2))) -> 897.06/297.15 mark(U21(and(isPalListKind(V1), isPalListKind(V2)), V1, V2)) 897.06/297.15 , active(isList(nil())) -> mark(tt()) 897.06/297.15 , active(U23(X)) -> U23(active(X)) 897.06/297.15 , active(U23(tt())) -> mark(tt()) 897.06/297.15 , active(U31(X1, X2)) -> U31(active(X1), X2) 897.06/297.15 , active(U31(tt(), V)) -> mark(U32(isQid(V))) 897.06/297.15 , active(U32(X)) -> U32(active(X)) 897.06/297.15 , active(U32(tt())) -> mark(tt()) 897.06/297.15 , active(isQid(a())) -> mark(tt()) 897.06/297.15 , active(isQid(e())) -> mark(tt()) 897.06/297.15 , active(isQid(i())) -> mark(tt()) 897.06/297.15 , active(isQid(o())) -> mark(tt()) 897.06/297.15 , active(isQid(u())) -> mark(tt()) 897.06/297.15 , active(U41(X1, X2, X3)) -> U41(active(X1), X2, X3) 897.06/297.15 , active(U41(tt(), V1, V2)) -> mark(U42(isList(V1), V2)) 897.06/297.15 , active(U42(X1, X2)) -> U42(active(X1), X2) 897.06/297.15 , active(U42(tt(), V2)) -> mark(U43(isNeList(V2))) 897.06/297.15 , active(U43(X)) -> U43(active(X)) 897.06/297.15 , active(U43(tt())) -> mark(tt()) 897.06/297.15 , active(U51(X1, X2, X3)) -> U51(active(X1), X2, X3) 897.06/297.15 , active(U51(tt(), V1, V2)) -> mark(U52(isNeList(V1), V2)) 897.06/297.15 , active(U52(X1, X2)) -> U52(active(X1), X2) 897.06/297.15 , active(U52(tt(), V2)) -> mark(U53(isList(V2))) 897.06/297.15 , active(U53(X)) -> U53(active(X)) 897.06/297.15 , active(U53(tt())) -> mark(tt()) 897.06/297.15 , active(U61(X1, X2)) -> U61(active(X1), X2) 897.06/297.15 , active(U61(tt(), V)) -> mark(U62(isQid(V))) 897.06/297.15 , active(U62(X)) -> U62(active(X)) 897.06/297.15 , active(U62(tt())) -> mark(tt()) 897.06/297.15 , active(U71(X1, X2)) -> U71(active(X1), X2) 897.06/297.15 , active(U71(tt(), V)) -> mark(U72(isNePal(V))) 897.06/297.15 , active(U72(X)) -> U72(active(X)) 897.06/297.15 , active(U72(tt())) -> mark(tt()) 897.06/297.15 , active(isNePal(V)) -> mark(U61(isPalListKind(V), V)) 897.06/297.15 , active(isNePal(__(I, __(P, I)))) -> 897.06/297.15 mark(and(and(isQid(I), isPalListKind(I)), 897.06/297.15 and(isPal(P), isPalListKind(P)))) 897.06/297.15 , active(and(X1, X2)) -> and(active(X1), X2) 897.06/297.15 , active(and(tt(), X)) -> mark(X) 897.06/297.15 , active(isPalListKind(__(V1, V2))) -> 897.06/297.15 mark(and(isPalListKind(V1), isPalListKind(V2))) 897.06/297.15 , active(isPalListKind(nil())) -> mark(tt()) 897.06/297.15 , active(isPalListKind(a())) -> mark(tt()) 897.06/297.15 , active(isPalListKind(e())) -> mark(tt()) 897.06/297.15 , active(isPalListKind(i())) -> mark(tt()) 897.06/297.15 , active(isPalListKind(o())) -> mark(tt()) 897.06/297.15 , active(isPalListKind(u())) -> mark(tt()) 897.06/297.15 , active(isPal(V)) -> mark(U71(isPalListKind(V), V)) 897.06/297.15 , active(isPal(nil())) -> mark(tt()) 897.06/297.15 , __(X1, mark(X2)) -> mark(__(X1, X2)) 897.06/297.15 , __(mark(X1), X2) -> mark(__(X1, X2)) 897.06/297.15 , __(ok(X1), ok(X2)) -> ok(__(X1, X2)) 897.06/297.15 , U11(mark(X1), X2) -> mark(U11(X1, X2)) 897.06/297.15 , U11(ok(X1), ok(X2)) -> ok(U11(X1, X2)) 897.06/297.15 , U12(mark(X)) -> mark(U12(X)) 897.06/297.15 , U12(ok(X)) -> ok(U12(X)) 897.06/297.15 , isNeList(ok(X)) -> ok(isNeList(X)) 897.06/297.15 , U21(mark(X1), X2, X3) -> mark(U21(X1, X2, X3)) 897.06/297.15 , U21(ok(X1), ok(X2), ok(X3)) -> ok(U21(X1, X2, X3)) 897.06/297.15 , U22(mark(X1), X2) -> mark(U22(X1, X2)) 897.06/297.15 , U22(ok(X1), ok(X2)) -> ok(U22(X1, X2)) 897.06/297.15 , isList(ok(X)) -> ok(isList(X)) 897.06/297.15 , U23(mark(X)) -> mark(U23(X)) 897.06/297.15 , U23(ok(X)) -> ok(U23(X)) 897.06/297.15 , U31(mark(X1), X2) -> mark(U31(X1, X2)) 897.06/297.15 , U31(ok(X1), ok(X2)) -> ok(U31(X1, X2)) 897.06/297.15 , U32(mark(X)) -> mark(U32(X)) 897.06/297.15 , U32(ok(X)) -> ok(U32(X)) 897.06/297.15 , isQid(ok(X)) -> ok(isQid(X)) 897.06/297.15 , U41(mark(X1), X2, X3) -> mark(U41(X1, X2, X3)) 897.06/297.15 , U41(ok(X1), ok(X2), ok(X3)) -> ok(U41(X1, X2, X3)) 897.06/297.15 , U42(mark(X1), X2) -> mark(U42(X1, X2)) 897.06/297.15 , U42(ok(X1), ok(X2)) -> ok(U42(X1, X2)) 897.06/297.15 , U43(mark(X)) -> mark(U43(X)) 897.06/297.15 , U43(ok(X)) -> ok(U43(X)) 897.06/297.15 , U51(mark(X1), X2, X3) -> mark(U51(X1, X2, X3)) 897.06/297.15 , U51(ok(X1), ok(X2), ok(X3)) -> ok(U51(X1, X2, X3)) 897.06/297.15 , U52(mark(X1), X2) -> mark(U52(X1, X2)) 897.06/297.15 , U52(ok(X1), ok(X2)) -> ok(U52(X1, X2)) 897.06/297.15 , U53(mark(X)) -> mark(U53(X)) 897.06/297.15 , U53(ok(X)) -> ok(U53(X)) 897.06/297.15 , U61(mark(X1), X2) -> mark(U61(X1, X2)) 897.06/297.15 , U61(ok(X1), ok(X2)) -> ok(U61(X1, X2)) 897.06/297.15 , U62(mark(X)) -> mark(U62(X)) 897.06/297.15 , U62(ok(X)) -> ok(U62(X)) 897.06/297.15 , U71(mark(X1), X2) -> mark(U71(X1, X2)) 897.06/297.15 , U71(ok(X1), ok(X2)) -> ok(U71(X1, X2)) 897.06/297.15 , U72(mark(X)) -> mark(U72(X)) 897.06/297.15 , U72(ok(X)) -> ok(U72(X)) 897.06/297.15 , isNePal(ok(X)) -> ok(isNePal(X)) 897.06/297.15 , and(mark(X1), X2) -> mark(and(X1, X2)) 897.06/297.15 , and(ok(X1), ok(X2)) -> ok(and(X1, X2)) 897.06/297.15 , isPalListKind(ok(X)) -> ok(isPalListKind(X)) 897.06/297.15 , isPal(ok(X)) -> ok(isPal(X)) 897.06/297.15 , proper(__(X1, X2)) -> __(proper(X1), proper(X2)) 897.06/297.15 , proper(nil()) -> ok(nil()) 897.06/297.15 , proper(U11(X1, X2)) -> U11(proper(X1), proper(X2)) 897.06/297.15 , proper(tt()) -> ok(tt()) 897.06/297.15 , proper(U12(X)) -> U12(proper(X)) 897.06/297.15 , proper(isNeList(X)) -> isNeList(proper(X)) 897.06/297.15 , proper(U21(X1, X2, X3)) -> 897.06/297.15 U21(proper(X1), proper(X2), proper(X3)) 897.06/297.15 , proper(U22(X1, X2)) -> U22(proper(X1), proper(X2)) 897.06/297.15 , proper(isList(X)) -> isList(proper(X)) 897.06/297.15 , proper(U23(X)) -> U23(proper(X)) 897.06/297.15 , proper(U31(X1, X2)) -> U31(proper(X1), proper(X2)) 897.06/297.15 , proper(U32(X)) -> U32(proper(X)) 897.06/297.15 , proper(isQid(X)) -> isQid(proper(X)) 897.06/297.15 , proper(U41(X1, X2, X3)) -> 897.06/297.15 U41(proper(X1), proper(X2), proper(X3)) 897.06/297.15 , proper(U42(X1, X2)) -> U42(proper(X1), proper(X2)) 897.06/297.15 , proper(U43(X)) -> U43(proper(X)) 897.06/297.15 , proper(U51(X1, X2, X3)) -> 897.06/297.15 U51(proper(X1), proper(X2), proper(X3)) 897.06/297.15 , proper(U52(X1, X2)) -> U52(proper(X1), proper(X2)) 897.06/297.15 , proper(U53(X)) -> U53(proper(X)) 897.06/297.15 , proper(U61(X1, X2)) -> U61(proper(X1), proper(X2)) 897.06/297.15 , proper(U62(X)) -> U62(proper(X)) 897.06/297.15 , proper(U71(X1, X2)) -> U71(proper(X1), proper(X2)) 897.06/297.15 , proper(U72(X)) -> U72(proper(X)) 897.06/297.15 , proper(isNePal(X)) -> isNePal(proper(X)) 897.06/297.15 , proper(and(X1, X2)) -> and(proper(X1), proper(X2)) 897.06/297.15 , proper(isPalListKind(X)) -> isPalListKind(proper(X)) 897.06/297.15 , proper(isPal(X)) -> isPal(proper(X)) 897.06/297.15 , proper(a()) -> ok(a()) 897.06/297.15 , proper(e()) -> ok(e()) 897.06/297.15 , proper(i()) -> ok(i()) 897.06/297.15 , proper(o()) -> ok(o()) 897.06/297.15 , proper(u()) -> ok(u()) 897.06/297.15 , top(mark(X)) -> top(proper(X)) 897.06/297.15 , top(ok(X)) -> top(active(X)) } 897.06/297.15 Weak DPs: 897.06/297.15 { proper^#(nil()) -> c_110() 897.06/297.15 , proper^#(tt()) -> c_112() 897.06/297.15 , proper^#(a()) -> c_136() 897.06/297.15 , proper^#(e()) -> c_137() 897.06/297.15 , proper^#(i()) -> c_138() 897.06/297.15 , proper^#(o()) -> c_139() 897.06/297.15 , proper^#(u()) -> c_140() } 897.06/297.15 Obligation: 897.06/297.15 runtime complexity 897.06/297.15 Answer: 897.06/297.15 MAYBE 897.06/297.15 897.06/297.15 Empty strict component of the problem is NOT empty. 897.06/297.15 897.06/297.15 897.06/297.15 Arrrr.. 897.24/297.21 EOF