- : unit = () - : unit = () h : heuristic = - : unit = () APPLY CRITERIA (Marked dependency pairs) TRS termination of: [1] a____(__(X,Y),Z) -> a____(mark(X),a____(mark(Y),mark(Z))) [2] a____(X,nil) -> mark(X) [3] a____(nil,X) -> mark(X) [4] a__U11(tt,V) -> a__U12(a__isPalListKind(V),V) [5] a__U12(tt,V) -> a__U13(a__isNeList(V)) [6] a__U13(tt) -> tt [7] a__U21(tt,V1,V2) -> a__U22(a__isPalListKind(V1),V1,V2) [8] a__U22(tt,V1,V2) -> a__U23(a__isPalListKind(V2),V1,V2) [9] a__U23(tt,V1,V2) -> a__U24(a__isPalListKind(V2),V1,V2) [10] a__U24(tt,V1,V2) -> a__U25(a__isList(V1),V2) [11] a__U25(tt,V2) -> a__U26(a__isList(V2)) [12] a__U26(tt) -> tt [13] a__U31(tt,V) -> a__U32(a__isPalListKind(V),V) [14] a__U32(tt,V) -> a__U33(a__isQid(V)) [15] a__U33(tt) -> tt [16] a__U41(tt,V1,V2) -> a__U42(a__isPalListKind(V1),V1,V2) [17] a__U42(tt,V1,V2) -> a__U43(a__isPalListKind(V2),V1,V2) [18] a__U43(tt,V1,V2) -> a__U44(a__isPalListKind(V2),V1,V2) [19] a__U44(tt,V1,V2) -> a__U45(a__isList(V1),V2) [20] a__U45(tt,V2) -> a__U46(a__isNeList(V2)) [21] a__U46(tt) -> tt [22] a__U51(tt,V1,V2) -> a__U52(a__isPalListKind(V1),V1,V2) [23] a__U52(tt,V1,V2) -> a__U53(a__isPalListKind(V2),V1,V2) [24] a__U53(tt,V1,V2) -> a__U54(a__isPalListKind(V2),V1,V2) [25] a__U54(tt,V1,V2) -> a__U55(a__isNeList(V1),V2) [26] a__U55(tt,V2) -> a__U56(a__isList(V2)) [27] a__U56(tt) -> tt [28] a__U61(tt,V) -> a__U62(a__isPalListKind(V),V) [29] a__U62(tt,V) -> a__U63(a__isQid(V)) [30] a__U63(tt) -> tt [31] a__U71(tt,I,P) -> a__U72(a__isPalListKind(I),P) [32] a__U72(tt,P) -> a__U73(a__isPal(P),P) [33] a__U73(tt,P) -> a__U74(a__isPalListKind(P)) [34] a__U74(tt) -> tt [35] a__U81(tt,V) -> a__U82(a__isPalListKind(V),V) [36] a__U82(tt,V) -> a__U83(a__isNePal(V)) [37] a__U83(tt) -> tt [38] a__U91(tt,V2) -> a__U92(a__isPalListKind(V2)) [39] a__U92(tt) -> tt [40] a__isList(V) -> a__U11(a__isPalListKind(V),V) [41] a__isList(nil) -> tt [42] a__isList(__(V1,V2)) -> a__U21(a__isPalListKind(V1),V1,V2) [43] a__isNeList(V) -> a__U31(a__isPalListKind(V),V) [44] a__isNeList(__(V1,V2)) -> a__U41(a__isPalListKind(V1),V1,V2) [45] a__isNeList(__(V1,V2)) -> a__U51(a__isPalListKind(V1),V1,V2) [46] a__isNePal(V) -> a__U61(a__isPalListKind(V),V) [47] a__isNePal(__(I,__(P,I))) -> a__U71(a__isQid(I),I,P) [48] a__isPal(V) -> a__U81(a__isPalListKind(V),V) [49] a__isPal(nil) -> tt [50] a__isPalListKind(a) -> tt [51] a__isPalListKind(e) -> tt [52] a__isPalListKind(i) -> tt [53] a__isPalListKind(nil) -> tt [54] a__isPalListKind(o) -> tt [55] a__isPalListKind(u) -> tt [56] a__isPalListKind(__(V1,V2)) -> a__U91(a__isPalListKind(V1),V2) [57] a__isQid(a) -> tt [58] a__isQid(e) -> tt [59] a__isQid(i) -> tt [60] a__isQid(o) -> tt [61] a__isQid(u) -> tt [62] mark(__(X1,X2)) -> a____(mark(X1),mark(X2)) [63] mark(U11(X1,X2)) -> a__U11(mark(X1),X2) [64] mark(U12(X1,X2)) -> a__U12(mark(X1),X2) [65] mark(isPalListKind(X)) -> a__isPalListKind(X) [66] mark(U13(X)) -> a__U13(mark(X)) [67] mark(isNeList(X)) -> a__isNeList(X) [68] mark(U21(X1,X2,X3)) -> a__U21(mark(X1),X2,X3) [69] mark(U22(X1,X2,X3)) -> a__U22(mark(X1),X2,X3) [70] mark(U23(X1,X2,X3)) -> a__U23(mark(X1),X2,X3) [71] mark(U24(X1,X2,X3)) -> a__U24(mark(X1),X2,X3) [72] mark(U25(X1,X2)) -> a__U25(mark(X1),X2) [73] mark(isList(X)) -> a__isList(X) [74] mark(U26(X)) -> a__U26(mark(X)) [75] mark(U31(X1,X2)) -> a__U31(mark(X1),X2) [76] mark(U32(X1,X2)) -> a__U32(mark(X1),X2) [77] mark(U33(X)) -> a__U33(mark(X)) [78] mark(isQid(X)) -> a__isQid(X) [79] mark(U41(X1,X2,X3)) -> a__U41(mark(X1),X2,X3) [80] mark(U42(X1,X2,X3)) -> a__U42(mark(X1),X2,X3) [81] mark(U43(X1,X2,X3)) -> a__U43(mark(X1),X2,X3) [82] mark(U44(X1,X2,X3)) -> a__U44(mark(X1),X2,X3) [83] mark(U45(X1,X2)) -> a__U45(mark(X1),X2) [84] mark(U46(X)) -> a__U46(mark(X)) [85] mark(U51(X1,X2,X3)) -> a__U51(mark(X1),X2,X3) [86] mark(U52(X1,X2,X3)) -> a__U52(mark(X1),X2,X3) [87] mark(U53(X1,X2,X3)) -> a__U53(mark(X1),X2,X3) [88] mark(U54(X1,X2,X3)) -> a__U54(mark(X1),X2,X3) [89] mark(U55(X1,X2)) -> a__U55(mark(X1),X2) [90] mark(U56(X)) -> a__U56(mark(X)) [91] mark(U61(X1,X2)) -> a__U61(mark(X1),X2) [92] mark(U62(X1,X2)) -> a__U62(mark(X1),X2) [93] mark(U63(X)) -> a__U63(mark(X)) [94] mark(U71(X1,X2,X3)) -> a__U71(mark(X1),X2,X3) [95] mark(U72(X1,X2)) -> a__U72(mark(X1),X2) [96] mark(U73(X1,X2)) -> a__U73(mark(X1),X2) [97] mark(isPal(X)) -> a__isPal(X) [98] mark(U74(X)) -> a__U74(mark(X)) [99] mark(U81(X1,X2)) -> a__U81(mark(X1),X2) [100] mark(U82(X1,X2)) -> a__U82(mark(X1),X2) [101] mark(U83(X)) -> a__U83(mark(X)) [102] mark(isNePal(X)) -> a__isNePal(X) [103] mark(U91(X1,X2)) -> a__U91(mark(X1),X2) [104] mark(U92(X)) -> a__U92(mark(X)) [105] mark(nil) -> nil [106] mark(tt) -> tt [107] mark(a) -> a [108] mark(e) -> e [109] mark(i) -> i [110] mark(o) -> o [111] mark(u) -> u [112] a____(X1,X2) -> __(X1,X2) [113] a__U11(X1,X2) -> U11(X1,X2) [114] a__U12(X1,X2) -> U12(X1,X2) [115] a__isPalListKind(X) -> isPalListKind(X) [116] a__U13(X) -> U13(X) [117] a__isNeList(X) -> isNeList(X) [118] a__U21(X1,X2,X3) -> U21(X1,X2,X3) [119] a__U22(X1,X2,X3) -> U22(X1,X2,X3) [120] a__U23(X1,X2,X3) -> U23(X1,X2,X3) [121] a__U24(X1,X2,X3) -> U24(X1,X2,X3) [122] a__U25(X1,X2) -> U25(X1,X2) [123] a__isList(X) -> isList(X) [124] a__U26(X) -> U26(X) [125] a__U31(X1,X2) -> U31(X1,X2) [126] a__U32(X1,X2) -> U32(X1,X2) [127] a__U33(X) -> U33(X) [128] a__isQid(X) -> isQid(X) [129] a__U41(X1,X2,X3) -> U41(X1,X2,X3) [130] a__U42(X1,X2,X3) -> U42(X1,X2,X3) [131] a__U43(X1,X2,X3) -> U43(X1,X2,X3) [132] a__U44(X1,X2,X3) -> U44(X1,X2,X3) [133] a__U45(X1,X2) -> U45(X1,X2) [134] a__U46(X) -> U46(X) [135] a__U51(X1,X2,X3) -> U51(X1,X2,X3) [136] a__U52(X1,X2,X3) -> U52(X1,X2,X3) [137] a__U53(X1,X2,X3) -> U53(X1,X2,X3) [138] a__U54(X1,X2,X3) -> U54(X1,X2,X3) [139] a__U55(X1,X2) -> U55(X1,X2) [140] a__U56(X) -> U56(X) [141] a__U61(X1,X2) -> U61(X1,X2) [142] a__U62(X1,X2) -> U62(X1,X2) [143] a__U63(X) -> U63(X) [144] a__U71(X1,X2,X3) -> U71(X1,X2,X3) [145] a__U72(X1,X2) -> U72(X1,X2) [146] a__U73(X1,X2) -> U73(X1,X2) [147] a__isPal(X) -> isPal(X) [148] a__U74(X) -> U74(X) [149] a__U81(X1,X2) -> U81(X1,X2) [150] a__U82(X1,X2) -> U82(X1,X2) [151] a__U83(X) -> U83(X) [152] a__isNePal(X) -> isNePal(X) [153] a__U91(X1,X2) -> U91(X1,X2) [154] a__U92(X) -> U92(X) Sub problem: guided: DP termination of: END GUIDED APPLY CRITERIA (Graph splitting) Found 4 components: { --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> } { --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> } { --> --> --> --> --> --> } { --> --> --> --> --> } APPLY CRITERIA (Subterm criterion) APPLY CRITERIA (Choosing graph) Trying to solve the following constraints: { a____(__(X,Y),Z) >= a____(mark(X),a____(mark(Y),mark(Z))) ; a____(nil,X) >= mark(X) ; a____(X,nil) >= mark(X) ; a____(X1,X2) >= __(X1,X2) ; mark(__(X1,X2)) >= a____(mark(X1),mark(X2)) ; mark(nil) >= nil ; mark(tt) >= tt ; mark(a) >= a ; mark(e) >= e ; mark(i) >= i ; mark(o) >= o ; mark(u) >= u ; mark(U11(X1,X2)) >= a__U11(mark(X1),X2) ; mark(U12(X1,X2)) >= a__U12(mark(X1),X2) ; mark(isPalListKind(X)) >= a__isPalListKind(X) ; mark(U13(X)) >= a__U13(mark(X)) ; mark(isNeList(X)) >= a__isNeList(X) ; mark(U21(X1,X2,X3)) >= a__U21(mark(X1),X2,X3) ; mark(U22(X1,X2,X3)) >= a__U22(mark(X1),X2,X3) ; mark(U23(X1,X2,X3)) >= a__U23(mark(X1),X2,X3) ; mark(U24(X1,X2,X3)) >= a__U24(mark(X1),X2,X3) ; mark(U25(X1,X2)) >= a__U25(mark(X1),X2) ; mark(isList(X)) >= a__isList(X) ; mark(U26(X)) >= a__U26(mark(X)) ; mark(U31(X1,X2)) >= a__U31(mark(X1),X2) ; mark(U32(X1,X2)) >= a__U32(mark(X1),X2) ; mark(U33(X)) >= a__U33(mark(X)) ; mark(isQid(X)) >= a__isQid(X) ; mark(U41(X1,X2,X3)) >= a__U41(mark(X1),X2,X3) ; mark(U42(X1,X2,X3)) >= a__U42(mark(X1),X2,X3) ; mark(U43(X1,X2,X3)) >= a__U43(mark(X1),X2,X3) ; mark(U44(X1,X2,X3)) >= a__U44(mark(X1),X2,X3) ; mark(U45(X1,X2)) >= a__U45(mark(X1),X2) ; mark(U46(X)) >= a__U46(mark(X)) ; mark(U51(X1,X2,X3)) >= a__U51(mark(X1),X2,X3) ; mark(U52(X1,X2,X3)) >= a__U52(mark(X1),X2,X3) ; mark(U53(X1,X2,X3)) >= a__U53(mark(X1),X2,X3) ; mark(U54(X1,X2,X3)) >= a__U54(mark(X1),X2,X3) ; mark(U55(X1,X2)) >= a__U55(mark(X1),X2) ; mark(U56(X)) >= a__U56(mark(X)) ; mark(U61(X1,X2)) >= a__U61(mark(X1),X2) ; mark(U62(X1,X2)) >= a__U62(mark(X1),X2) ; mark(U63(X)) >= a__U63(mark(X)) ; mark(U71(X1,X2,X3)) >= a__U71(mark(X1),X2,X3) ; mark(U72(X1,X2)) >= a__U72(mark(X1),X2) ; mark(U73(X1,X2)) >= a__U73(mark(X1),X2) ; mark(isPal(X)) >= a__isPal(X) ; mark(U74(X)) >= a__U74(mark(X)) ; mark(U81(X1,X2)) >= a__U81(mark(X1),X2) ; mark(U82(X1,X2)) >= a__U82(mark(X1),X2) ; mark(U83(X)) >= a__U83(mark(X)) ; mark(isNePal(X)) >= a__isNePal(X) ; mark(U91(X1,X2)) >= a__U91(mark(X1),X2) ; mark(U92(X)) >= a__U92(mark(X)) ; a__U12(tt,V) >= a__U13(a__isNeList(V)) ; a__U12(X1,X2) >= U12(X1,X2) ; a__isPalListKind(__(V1,V2)) >= a__U91(a__isPalListKind(V1),V2) ; a__isPalListKind(nil) >= tt ; a__isPalListKind(a) >= tt ; a__isPalListKind(e) >= tt ; a__isPalListKind(i) >= tt ; a__isPalListKind(o) >= tt ; a__isPalListKind(u) >= tt ; a__isPalListKind(X) >= isPalListKind(X) ; a__U11(tt,V) >= a__U12(a__isPalListKind(V),V) ; a__U11(X1,X2) >= U11(X1,X2) ; a__U13(tt) >= tt ; a__U13(X) >= U13(X) ; a__isNeList(__(V1,V2)) >= a__U41(a__isPalListKind(V1),V1,V2) ; a__isNeList(__(V1,V2)) >= a__U51(a__isPalListKind(V1),V1,V2) ; a__isNeList(X) >= isNeList(X) ; a__isNeList(V) >= a__U31(a__isPalListKind(V),V) ; a__U22(tt,V1,V2) >= a__U23(a__isPalListKind(V2),V1,V2) ; a__U22(X1,X2,X3) >= U22(X1,X2,X3) ; a__U21(tt,V1,V2) >= a__U22(a__isPalListKind(V1),V1,V2) ; a__U21(X1,X2,X3) >= U21(X1,X2,X3) ; a__U23(tt,V1,V2) >= a__U24(a__isPalListKind(V2),V1,V2) ; a__U23(X1,X2,X3) >= U23(X1,X2,X3) ; a__U24(tt,V1,V2) >= a__U25(a__isList(V1),V2) ; a__U24(X1,X2,X3) >= U24(X1,X2,X3) ; a__U25(tt,V2) >= a__U26(a__isList(V2)) ; a__U25(X1,X2) >= U25(X1,X2) ; a__isList(__(V1,V2)) >= a__U21(a__isPalListKind(V1),V1,V2) ; a__isList(nil) >= tt ; a__isList(X) >= isList(X) ; a__isList(V) >= a__U11(a__isPalListKind(V),V) ; a__U26(tt) >= tt ; a__U26(X) >= U26(X) ; a__U32(tt,V) >= a__U33(a__isQid(V)) ; a__U32(X1,X2) >= U32(X1,X2) ; a__U31(tt,V) >= a__U32(a__isPalListKind(V),V) ; a__U31(X1,X2) >= U31(X1,X2) ; a__U33(tt) >= tt ; a__U33(X) >= U33(X) ; a__isQid(a) >= tt ; a__isQid(e) >= tt ; a__isQid(i) >= tt ; a__isQid(o) >= tt ; a__isQid(u) >= tt ; a__isQid(X) >= isQid(X) ; a__U42(tt,V1,V2) >= a__U43(a__isPalListKind(V2),V1,V2) ; a__U42(X1,X2,X3) >= U42(X1,X2,X3) ; a__U41(tt,V1,V2) >= a__U42(a__isPalListKind(V1),V1,V2) ; a__U41(X1,X2,X3) >= U41(X1,X2,X3) ; a__U43(tt,V1,V2) >= a__U44(a__isPalListKind(V2),V1,V2) ; a__U43(X1,X2,X3) >= U43(X1,X2,X3) ; a__U44(tt,V1,V2) >= a__U45(a__isList(V1),V2) ; a__U44(X1,X2,X3) >= U44(X1,X2,X3) ; a__U45(tt,V2) >= a__U46(a__isNeList(V2)) ; a__U45(X1,X2) >= U45(X1,X2) ; a__U46(tt) >= tt ; a__U46(X) >= U46(X) ; a__U52(tt,V1,V2) >= a__U53(a__isPalListKind(V2),V1,V2) ; a__U52(X1,X2,X3) >= U52(X1,X2,X3) ; a__U51(tt,V1,V2) >= a__U52(a__isPalListKind(V1),V1,V2) ; a__U51(X1,X2,X3) >= U51(X1,X2,X3) ; a__U53(tt,V1,V2) >= a__U54(a__isPalListKind(V2),V1,V2) ; a__U53(X1,X2,X3) >= U53(X1,X2,X3) ; a__U54(tt,V1,V2) >= a__U55(a__isNeList(V1),V2) ; a__U54(X1,X2,X3) >= U54(X1,X2,X3) ; a__U55(tt,V2) >= a__U56(a__isList(V2)) ; a__U55(X1,X2) >= U55(X1,X2) ; a__U56(tt) >= tt ; a__U56(X) >= U56(X) ; a__U62(tt,V) >= a__U63(a__isQid(V)) ; a__U62(X1,X2) >= U62(X1,X2) ; a__U61(tt,V) >= a__U62(a__isPalListKind(V),V) ; a__U61(X1,X2) >= U61(X1,X2) ; a__U63(tt) >= tt ; a__U63(X) >= U63(X) ; a__U72(tt,P) >= a__U73(a__isPal(P),P) ; a__U72(X1,X2) >= U72(X1,X2) ; a__U71(tt,I,P) >= a__U72(a__isPalListKind(I),P) ; a__U71(X1,X2,X3) >= U71(X1,X2,X3) ; a__U73(tt,P) >= a__U74(a__isPalListKind(P)) ; a__U73(X1,X2) >= U73(X1,X2) ; a__isPal(nil) >= tt ; a__isPal(X) >= isPal(X) ; a__isPal(V) >= a__U81(a__isPalListKind(V),V) ; a__U74(tt) >= tt ; a__U74(X) >= U74(X) ; a__U82(tt,V) >= a__U83(a__isNePal(V)) ; a__U82(X1,X2) >= U82(X1,X2) ; a__U81(tt,V) >= a__U82(a__isPalListKind(V),V) ; a__U81(X1,X2) >= U81(X1,X2) ; a__U83(tt) >= tt ; a__U83(X) >= U83(X) ; a__isNePal(__(I,__(P,I))) >= a__U71(a__isQid(I),I,P) ; a__isNePal(X) >= isNePal(X) ; a__isNePal(V) >= a__U61(a__isPalListKind(V),V) ; a__U92(tt) >= tt ; a__U92(X) >= U92(X) ; a__U91(tt,V2) >= a__U92(a__isPalListKind(V2)) ; a__U91(X1,X2) >= U91(X1,X2) ; Marked_a____(__(X,Y),Z) >= Marked_a____(mark(X),a____(mark(Y),mark(Z))) ; Marked_a____(__(X,Y),Z) >= Marked_a____(mark(Y),mark(Z)) ; Marked_a____(__(X,Y),Z) >= Marked_mark(X) ; Marked_a____(__(X,Y),Z) >= Marked_mark(Y) ; Marked_a____(__(X,Y),Z) >= Marked_mark(Z) ; Marked_a____(nil,X) >= Marked_mark(X) ; Marked_a____(X,nil) >= Marked_mark(X) ; Marked_mark(__(X1,X2)) >= Marked_a____(mark(X1),mark(X2)) ; Marked_mark(__(X1,X2)) >= Marked_mark(X1) ; Marked_mark(__(X1,X2)) >= Marked_mark(X2) ; Marked_mark(U11(X1,X2)) >= Marked_mark(X1) ; Marked_mark(U12(X1,X2)) >= Marked_mark(X1) ; Marked_mark(U13(X)) >= Marked_mark(X) ; Marked_mark(U21(X1,X2,X3)) >= Marked_mark(X1) ; Marked_mark(U22(X1,X2,X3)) >= Marked_mark(X1) ; Marked_mark(U23(X1,X2,X3)) >= Marked_mark(X1) ; Marked_mark(U24(X1,X2,X3)) >= Marked_mark(X1) ; Marked_mark(U25(X1,X2)) >= Marked_mark(X1) ; Marked_mark(U26(X)) >= Marked_mark(X) ; Marked_mark(U31(X1,X2)) >= Marked_mark(X1) ; Marked_mark(U32(X1,X2)) >= Marked_mark(X1) ; Marked_mark(U33(X)) >= Marked_mark(X) ; Marked_mark(U41(X1,X2,X3)) >= Marked_mark(X1) ; Marked_mark(U42(X1,X2,X3)) >= Marked_mark(X1) ; Marked_mark(U43(X1,X2,X3)) >= Marked_mark(X1) ; Marked_mark(U44(X1,X2,X3)) >= Marked_mark(X1) ; Marked_mark(U45(X1,X2)) >= Marked_mark(X1) ; Marked_mark(U46(X)) >= Marked_mark(X) ; Marked_mark(U51(X1,X2,X3)) >= Marked_mark(X1) ; Marked_mark(U52(X1,X2,X3)) >= Marked_mark(X1) ; Marked_mark(U53(X1,X2,X3)) >= Marked_mark(X1) ; Marked_mark(U54(X1,X2,X3)) >= Marked_mark(X1) ; Marked_mark(U55(X1,X2)) >= Marked_mark(X1) ; Marked_mark(U56(X)) >= Marked_mark(X) ; Marked_mark(U61(X1,X2)) >= Marked_mark(X1) ; Marked_mark(U62(X1,X2)) >= Marked_mark(X1) ; Marked_mark(U63(X)) >= Marked_mark(X) ; Marked_mark(U71(X1,X2,X3)) >= Marked_mark(X1) ; Marked_mark(U72(X1,X2)) >= Marked_mark(X1) ; Marked_mark(U73(X1,X2)) >= Marked_mark(X1) ; Marked_mark(U74(X)) >= Marked_mark(X) ; Marked_mark(U81(X1,X2)) >= Marked_mark(X1) ; Marked_mark(U82(X1,X2)) >= Marked_mark(X1) ; Marked_mark(U83(X)) >= Marked_mark(X) ; Marked_mark(U91(X1,X2)) >= Marked_mark(X1) ; Marked_mark(U92(X)) >= Marked_mark(X) ; } + Disjunctions:{ { Marked_a____(__(X,Y),Z) > Marked_a____(mark(X),a____(mark(Y),mark(Z))) ; } { Marked_a____(__(X,Y),Z) > Marked_a____(mark(Y),mark(Z)) ; } { Marked_a____(__(X,Y),Z) > Marked_mark(X) ; } { Marked_a____(__(X,Y),Z) > Marked_mark(Y) ; } { Marked_a____(__(X,Y),Z) > Marked_mark(Z) ; } { Marked_a____(nil,X) > Marked_mark(X) ; } { Marked_a____(X,nil) > Marked_mark(X) ; } { Marked_mark(__(X1,X2)) > Marked_a____(mark(X1),mark(X2)) ; } { Marked_mark(__(X1,X2)) > Marked_mark(X1) ; } { Marked_mark(__(X1,X2)) > Marked_mark(X2) ; } { Marked_mark(U11(X1,X2)) > Marked_mark(X1) ; } { Marked_mark(U12(X1,X2)) > Marked_mark(X1) ; } { Marked_mark(U13(X)) > Marked_mark(X) ; } { Marked_mark(U21(X1,X2,X3)) > Marked_mark(X1) ; } { Marked_mark(U22(X1,X2,X3)) > Marked_mark(X1) ; } { Marked_mark(U23(X1,X2,X3)) > Marked_mark(X1) ; } { Marked_mark(U24(X1,X2,X3)) > Marked_mark(X1) ; } { Marked_mark(U25(X1,X2)) > Marked_mark(X1) ; } { Marked_mark(U26(X)) > Marked_mark(X) ; } { Marked_mark(U31(X1,X2)) > Marked_mark(X1) ; } { Marked_mark(U32(X1,X2)) > Marked_mark(X1) ; } { Marked_mark(U33(X)) > Marked_mark(X) ; } { Marked_mark(U41(X1,X2,X3)) > Marked_mark(X1) ; } { Marked_mark(U42(X1,X2,X3)) > Marked_mark(X1) ; } { Marked_mark(U43(X1,X2,X3)) > Marked_mark(X1) ; } { Marked_mark(U44(X1,X2,X3)) > Marked_mark(X1) ; } { Marked_mark(U45(X1,X2)) > Marked_mark(X1) ; } { Marked_mark(U46(X)) > Marked_mark(X) ; } { Marked_mark(U51(X1,X2,X3)) > Marked_mark(X1) ; } { Marked_mark(U52(X1,X2,X3)) > Marked_mark(X1) ; } { Marked_mark(U53(X1,X2,X3)) > Marked_mark(X1) ; } { Marked_mark(U54(X1,X2,X3)) > Marked_mark(X1) ; } { Marked_mark(U55(X1,X2)) > Marked_mark(X1) ; } { Marked_mark(U56(X)) > Marked_mark(X) ; } { Marked_mark(U61(X1,X2)) > Marked_mark(X1) ; } { Marked_mark(U62(X1,X2)) > Marked_mark(X1) ; } { Marked_mark(U63(X)) > Marked_mark(X) ; } { Marked_mark(U71(X1,X2,X3)) > Marked_mark(X1) ; } { Marked_mark(U72(X1,X2)) > Marked_mark(X1) ; } { Marked_mark(U73(X1,X2)) > Marked_mark(X1) ; } { Marked_mark(U74(X)) > Marked_mark(X) ; } { Marked_mark(U81(X1,X2)) > Marked_mark(X1) ; } { Marked_mark(U82(X1,X2)) > Marked_mark(X1) ; } { Marked_mark(U83(X)) > Marked_mark(X) ; } { Marked_mark(U91(X1,X2)) > Marked_mark(X1) ; } { Marked_mark(U92(X)) > Marked_mark(X) ; } } === TIMER virtual : 10.000000 === Entering poly_solver Starting Sat solver initialization Calling Sat solver... === STOPING TIMER virtual === === TIMER real : 10.000000 === === STOPING TIMER real === Sat solver returned Sat solver result read === STOPING TIMER real === === STOPING TIMER virtual === constraint: a____(__(X,Y),Z) >= a____(mark(X),a____(mark(Y),mark(Z))) constraint: a____(nil,X) >= mark(X) constraint: a____(X,nil) >= mark(X) constraint: a____(X1,X2) >= __(X1,X2) constraint: mark(__(X1,X2)) >= a____(mark(X1),mark(X2)) constraint: mark(nil) >= nil constraint: mark(tt) >= tt constraint: mark(a) >= a constraint: mark(e) >= e constraint: mark(i) >= i constraint: mark(o) >= o constraint: mark(u) >= u constraint: mark(U11(X1,X2)) >= a__U11(mark(X1),X2) constraint: mark(U12(X1,X2)) >= a__U12(mark(X1),X2) constraint: mark(isPalListKind(X)) >= a__isPalListKind(X) constraint: mark(U13(X)) >= a__U13(mark(X)) constraint: mark(isNeList(X)) >= a__isNeList(X) constraint: mark(U21(X1,X2,X3)) >= a__U21(mark(X1),X2,X3) constraint: mark(U22(X1,X2,X3)) >= a__U22(mark(X1),X2,X3) constraint: mark(U23(X1,X2,X3)) >= a__U23(mark(X1),X2,X3) constraint: mark(U24(X1,X2,X3)) >= a__U24(mark(X1),X2,X3) constraint: mark(U25(X1,X2)) >= a__U25(mark(X1),X2) constraint: mark(isList(X)) >= a__isList(X) constraint: mark(U26(X)) >= a__U26(mark(X)) constraint: mark(U31(X1,X2)) >= a__U31(mark(X1),X2) constraint: mark(U32(X1,X2)) >= a__U32(mark(X1),X2) constraint: mark(U33(X)) >= a__U33(mark(X)) constraint: mark(isQid(X)) >= a__isQid(X) constraint: mark(U41(X1,X2,X3)) >= a__U41(mark(X1),X2,X3) constraint: mark(U42(X1,X2,X3)) >= a__U42(mark(X1),X2,X3) constraint: mark(U43(X1,X2,X3)) >= a__U43(mark(X1),X2,X3) constraint: mark(U44(X1,X2,X3)) >= a__U44(mark(X1),X2,X3) constraint: mark(U45(X1,X2)) >= a__U45(mark(X1),X2) constraint: mark(U46(X)) >= a__U46(mark(X)) constraint: mark(U51(X1,X2,X3)) >= a__U51(mark(X1),X2,X3) constraint: mark(U52(X1,X2,X3)) >= a__U52(mark(X1),X2,X3) constraint: mark(U53(X1,X2,X3)) >= a__U53(mark(X1),X2,X3) constraint: mark(U54(X1,X2,X3)) >= a__U54(mark(X1),X2,X3) constraint: mark(U55(X1,X2)) >= a__U55(mark(X1),X2) constraint: mark(U56(X)) >= a__U56(mark(X)) constraint: mark(U61(X1,X2)) >= a__U61(mark(X1),X2) constraint: mark(U62(X1,X2)) >= a__U62(mark(X1),X2) constraint: mark(U63(X)) >= a__U63(mark(X)) constraint: mark(U71(X1,X2,X3)) >= a__U71(mark(X1),X2,X3) constraint: mark(U72(X1,X2)) >= a__U72(mark(X1),X2) constraint: mark(U73(X1,X2)) >= a__U73(mark(X1),X2) constraint: mark(isPal(X)) >= a__isPal(X) constraint: mark(U74(X)) >= a__U74(mark(X)) constraint: mark(U81(X1,X2)) >= a__U81(mark(X1),X2) constraint: mark(U82(X1,X2)) >= a__U82(mark(X1),X2) constraint: mark(U83(X)) >= a__U83(mark(X)) constraint: mark(isNePal(X)) >= a__isNePal(X) constraint: mark(U91(X1,X2)) >= a__U91(mark(X1),X2) constraint: mark(U92(X)) >= a__U92(mark(X)) constraint: a__U12(tt,V) >= a__U13(a__isNeList(V)) constraint: a__U12(X1,X2) >= U12(X1,X2) constraint: a__isPalListKind(__(V1,V2)) >= a__U91(a__isPalListKind(V1),V2) constraint: a__isPalListKind(nil) >= tt constraint: a__isPalListKind(a) >= tt constraint: a__isPalListKind(e) >= tt constraint: a__isPalListKind(i) >= tt constraint: a__isPalListKind(o) >= tt constraint: a__isPalListKind(u) >= tt constraint: a__isPalListKind(X) >= isPalListKind(X) constraint: a__U11(tt,V) >= a__U12(a__isPalListKind(V),V) constraint: a__U11(X1,X2) >= U11(X1,X2) constraint: a__U13(tt) >= tt constraint: a__U13(X) >= U13(X) constraint: a__isNeList(__(V1,V2)) >= a__U41(a__isPalListKind(V1),V1,V2) constraint: a__isNeList(__(V1,V2)) >= a__U51(a__isPalListKind(V1),V1,V2) constraint: a__isNeList(X) >= isNeList(X) constraint: a__isNeList(V) >= a__U31(a__isPalListKind(V),V) constraint: a__U22(tt,V1,V2) >= a__U23(a__isPalListKind(V2),V1,V2) constraint: a__U22(X1,X2,X3) >= U22(X1,X2,X3) constraint: a__U21(tt,V1,V2) >= a__U22(a__isPalListKind(V1),V1,V2) constraint: a__U21(X1,X2,X3) >= U21(X1,X2,X3) constraint: a__U23(tt,V1,V2) >= a__U24(a__isPalListKind(V2),V1,V2) constraint: a__U23(X1,X2,X3) >= U23(X1,X2,X3) constraint: a__U24(tt,V1,V2) >= a__U25(a__isList(V1),V2) constraint: a__U24(X1,X2,X3) >= U24(X1,X2,X3) constraint: a__U25(tt,V2) >= a__U26(a__isList(V2)) constraint: a__U25(X1,X2) >= U25(X1,X2) constraint: a__isList(__(V1,V2)) >= a__U21(a__isPalListKind(V1),V1,V2) constraint: a__isList(nil) >= tt constraint: a__isList(X) >= isList(X) constraint: a__isList(V) >= a__U11(a__isPalListKind(V),V) constraint: a__U26(tt) >= tt constraint: a__U26(X) >= U26(X) constraint: a__U32(tt,V) >= a__U33(a__isQid(V)) constraint: a__U32(X1,X2) >= U32(X1,X2) constraint: a__U31(tt,V) >= a__U32(a__isPalListKind(V),V) constraint: a__U31(X1,X2) >= U31(X1,X2) constraint: a__U33(tt) >= tt constraint: a__U33(X) >= U33(X) constraint: a__isQid(a) >= tt constraint: a__isQid(e) >= tt constraint: a__isQid(i) >= tt constraint: a__isQid(o) >= tt constraint: a__isQid(u) >= tt constraint: a__isQid(X) >= isQid(X) constraint: a__U42(tt,V1,V2) >= a__U43(a__isPalListKind(V2),V1,V2) constraint: a__U42(X1,X2,X3) >= U42(X1,X2,X3) constraint: a__U41(tt,V1,V2) >= a__U42(a__isPalListKind(V1),V1,V2) constraint: a__U41(X1,X2,X3) >= U41(X1,X2,X3) constraint: a__U43(tt,V1,V2) >= a__U44(a__isPalListKind(V2),V1,V2) constraint: a__U43(X1,X2,X3) >= U43(X1,X2,X3) constraint: a__U44(tt,V1,V2) >= a__U45(a__isList(V1),V2) constraint: a__U44(X1,X2,X3) >= U44(X1,X2,X3) constraint: a__U45(tt,V2) >= a__U46(a__isNeList(V2)) constraint: a__U45(X1,X2) >= U45(X1,X2) constraint: a__U46(tt) >= tt constraint: a__U46(X) >= U46(X) constraint: a__U52(tt,V1,V2) >= a__U53(a__isPalListKind(V2),V1,V2) constraint: a__U52(X1,X2,X3) >= U52(X1,X2,X3) constraint: a__U51(tt,V1,V2) >= a__U52(a__isPalListKind(V1),V1,V2) constraint: a__U51(X1,X2,X3) >= U51(X1,X2,X3) constraint: a__U53(tt,V1,V2) >= a__U54(a__isPalListKind(V2),V1,V2) constraint: a__U53(X1,X2,X3) >= U53(X1,X2,X3) constraint: a__U54(tt,V1,V2) >= a__U55(a__isNeList(V1),V2) constraint: a__U54(X1,X2,X3) >= U54(X1,X2,X3) constraint: a__U55(tt,V2) >= a__U56(a__isList(V2)) constraint: a__U55(X1,X2) >= U55(X1,X2) constraint: a__U56(tt) >= tt constraint: a__U56(X) >= U56(X) constraint: a__U62(tt,V) >= a__U63(a__isQid(V)) constraint: a__U62(X1,X2) >= U62(X1,X2) constraint: a__U61(tt,V) >= a__U62(a__isPalListKind(V),V) constraint: a__U61(X1,X2) >= U61(X1,X2) constraint: a__U63(tt) >= tt constraint: a__U63(X) >= U63(X) constraint: a__U72(tt,P) >= a__U73(a__isPal(P),P) constraint: a__U72(X1,X2) >= U72(X1,X2) constraint: a__U71(tt,I,P) >= a__U72(a__isPalListKind(I),P) constraint: a__U71(X1,X2,X3) >= U71(X1,X2,X3) constraint: a__U73(tt,P) >= a__U74(a__isPalListKind(P)) constraint: a__U73(X1,X2) >= U73(X1,X2) constraint: a__isPal(nil) >= tt constraint: a__isPal(X) >= isPal(X) constraint: a__isPal(V) >= a__U81(a__isPalListKind(V),V) constraint: a__U74(tt) >= tt constraint: a__U74(X) >= U74(X) constraint: a__U82(tt,V) >= a__U83(a__isNePal(V)) constraint: a__U82(X1,X2) >= U82(X1,X2) constraint: a__U81(tt,V) >= a__U82(a__isPalListKind(V),V) constraint: a__U81(X1,X2) >= U81(X1,X2) constraint: a__U83(tt) >= tt constraint: a__U83(X) >= U83(X) constraint: a__isNePal(__(I,__(P,I))) >= a__U71(a__isQid(I),I,P) constraint: a__isNePal(X) >= isNePal(X) constraint: a__isNePal(V) >= a__U61(a__isPalListKind(V),V) constraint: a__U92(tt) >= tt constraint: a__U92(X) >= U92(X) constraint: a__U91(tt,V2) >= a__U92(a__isPalListKind(V2)) constraint: a__U91(X1,X2) >= U91(X1,X2) constraint: Marked_a____(__(X,Y),Z) >= Marked_a____(mark(X), a____(mark(Y),mark(Z))) constraint: Marked_a____(__(X,Y),Z) >= Marked_a____(mark(Y),mark(Z)) constraint: Marked_a____(__(X,Y),Z) >= Marked_mark(X) constraint: Marked_a____(__(X,Y),Z) >= Marked_mark(Y) constraint: Marked_a____(__(X,Y),Z) >= Marked_mark(Z) constraint: Marked_a____(nil,X) >= Marked_mark(X) constraint: Marked_a____(X,nil) >= Marked_mark(X) constraint: Marked_mark(__(X1,X2)) >= Marked_a____(mark(X1),mark(X2)) constraint: Marked_mark(__(X1,X2)) >= Marked_mark(X1) constraint: Marked_mark(__(X1,X2)) >= Marked_mark(X2) constraint: Marked_mark(U11(X1,X2)) >= Marked_mark(X1) constraint: Marked_mark(U12(X1,X2)) >= Marked_mark(X1) constraint: Marked_mark(U13(X)) >= Marked_mark(X) constraint: Marked_mark(U21(X1,X2,X3)) >= Marked_mark(X1) constraint: Marked_mark(U22(X1,X2,X3)) >= Marked_mark(X1) constraint: Marked_mark(U23(X1,X2,X3)) >= Marked_mark(X1) constraint: Marked_mark(U24(X1,X2,X3)) >= Marked_mark(X1) constraint: Marked_mark(U25(X1,X2)) >= Marked_mark(X1) constraint: Marked_mark(U26(X)) >= Marked_mark(X) constraint: Marked_mark(U31(X1,X2)) >= Marked_mark(X1) constraint: Marked_mark(U32(X1,X2)) >= Marked_mark(X1) constraint: Marked_mark(U33(X)) >= Marked_mark(X) constraint: Marked_mark(U41(X1,X2,X3)) >= Marked_mark(X1) constraint: Marked_mark(U42(X1,X2,X3)) >= Marked_mark(X1) constraint: Marked_mark(U43(X1,X2,X3)) >= Marked_mark(X1) constraint: Marked_mark(U44(X1,X2,X3)) >= Marked_mark(X1) constraint: Marked_mark(U45(X1,X2)) >= Marked_mark(X1) constraint: Marked_mark(U46(X)) >= Marked_mark(X) constraint: Marked_mark(U51(X1,X2,X3)) >= Marked_mark(X1) constraint: Marked_mark(U52(X1,X2,X3)) >= Marked_mark(X1) constraint: Marked_mark(U53(X1,X2,X3)) >= Marked_mark(X1) constraint: Marked_mark(U54(X1,X2,X3)) >= Marked_mark(X1) constraint: Marked_mark(U55(X1,X2)) >= Marked_mark(X1) constraint: Marked_mark(U56(X)) >= Marked_mark(X) constraint: Marked_mark(U61(X1,X2)) >= Marked_mark(X1) constraint: Marked_mark(U62(X1,X2)) >= Marked_mark(X1) constraint: Marked_mark(U63(X)) >= Marked_mark(X) constraint: Marked_mark(U71(X1,X2,X3)) >= Marked_mark(X1) constraint: Marked_mark(U72(X1,X2)) >= Marked_mark(X1) constraint: Marked_mark(U73(X1,X2)) >= Marked_mark(X1) constraint: Marked_mark(U74(X)) >= Marked_mark(X) constraint: Marked_mark(U81(X1,X2)) >= Marked_mark(X1) constraint: Marked_mark(U82(X1,X2)) >= Marked_mark(X1) constraint: Marked_mark(U83(X)) >= Marked_mark(X) constraint: Marked_mark(U91(X1,X2)) >= Marked_mark(X1) constraint: Marked_mark(U92(X)) >= Marked_mark(X) APPLY CRITERIA (Subterm criterion) APPLY CRITERIA (Choosing graph) Trying to solve the following constraints: { a____(__(X,Y),Z) >= a____(mark(X),a____(mark(Y),mark(Z))) ; a____(nil,X) >= mark(X) ; a____(X,nil) >= mark(X) ; a____(X1,X2) >= __(X1,X2) ; mark(__(X1,X2)) >= a____(mark(X1),mark(X2)) ; mark(nil) >= nil ; mark(tt) >= tt ; mark(a) >= a ; mark(e) >= e ; mark(i) >= i ; mark(o) >= o ; mark(u) >= u ; mark(U11(X1,X2)) >= a__U11(mark(X1),X2) ; mark(U12(X1,X2)) >= a__U12(mark(X1),X2) ; mark(isPalListKind(X)) >= a__isPalListKind(X) ; mark(U13(X)) >= a__U13(mark(X)) ; mark(isNeList(X)) >= a__isNeList(X) ; mark(U21(X1,X2,X3)) >= a__U21(mark(X1),X2,X3) ; mark(U22(X1,X2,X3)) >= a__U22(mark(X1),X2,X3) ; mark(U23(X1,X2,X3)) >= a__U23(mark(X1),X2,X3) ; mark(U24(X1,X2,X3)) >= a__U24(mark(X1),X2,X3) ; mark(U25(X1,X2)) >= a__U25(mark(X1),X2) ; mark(isList(X)) >= a__isList(X) ; mark(U26(X)) >= a__U26(mark(X)) ; mark(U31(X1,X2)) >= a__U31(mark(X1),X2) ; mark(U32(X1,X2)) >= a__U32(mark(X1),X2) ; mark(U33(X)) >= a__U33(mark(X)) ; mark(isQid(X)) >= a__isQid(X) ; mark(U41(X1,X2,X3)) >= a__U41(mark(X1),X2,X3) ; mark(U42(X1,X2,X3)) >= a__U42(mark(X1),X2,X3) ; mark(U43(X1,X2,X3)) >= a__U43(mark(X1),X2,X3) ; mark(U44(X1,X2,X3)) >= a__U44(mark(X1),X2,X3) ; mark(U45(X1,X2)) >= a__U45(mark(X1),X2) ; mark(U46(X)) >= a__U46(mark(X)) ; mark(U51(X1,X2,X3)) >= a__U51(mark(X1),X2,X3) ; mark(U52(X1,X2,X3)) >= a__U52(mark(X1),X2,X3) ; mark(U53(X1,X2,X3)) >= a__U53(mark(X1),X2,X3) ; mark(U54(X1,X2,X3)) >= a__U54(mark(X1),X2,X3) ; mark(U55(X1,X2)) >= a__U55(mark(X1),X2) ; mark(U56(X)) >= a__U56(mark(X)) ; mark(U61(X1,X2)) >= a__U61(mark(X1),X2) ; mark(U62(X1,X2)) >= a__U62(mark(X1),X2) ; mark(U63(X)) >= a__U63(mark(X)) ; mark(U71(X1,X2,X3)) >= a__U71(mark(X1),X2,X3) ; mark(U72(X1,X2)) >= a__U72(mark(X1),X2) ; mark(U73(X1,X2)) >= a__U73(mark(X1),X2) ; mark(isPal(X)) >= a__isPal(X) ; mark(U74(X)) >= a__U74(mark(X)) ; mark(U81(X1,X2)) >= a__U81(mark(X1),X2) ; mark(U82(X1,X2)) >= a__U82(mark(X1),X2) ; mark(U83(X)) >= a__U83(mark(X)) ; mark(isNePal(X)) >= a__isNePal(X) ; mark(U91(X1,X2)) >= a__U91(mark(X1),X2) ; mark(U92(X)) >= a__U92(mark(X)) ; a__U12(tt,V) >= a__U13(a__isNeList(V)) ; a__U12(X1,X2) >= U12(X1,X2) ; a__isPalListKind(__(V1,V2)) >= a__U91(a__isPalListKind(V1),V2) ; a__isPalListKind(nil) >= tt ; a__isPalListKind(a) >= tt ; a__isPalListKind(e) >= tt ; a__isPalListKind(i) >= tt ; a__isPalListKind(o) >= tt ; a__isPalListKind(u) >= tt ; a__isPalListKind(X) >= isPalListKind(X) ; a__U11(tt,V) >= a__U12(a__isPalListKind(V),V) ; a__U11(X1,X2) >= U11(X1,X2) ; a__U13(tt) >= tt ; a__U13(X) >= U13(X) ; a__isNeList(__(V1,V2)) >= a__U41(a__isPalListKind(V1),V1,V2) ; a__isNeList(__(V1,V2)) >= a__U51(a__isPalListKind(V1),V1,V2) ; a__isNeList(X) >= isNeList(X) ; a__isNeList(V) >= a__U31(a__isPalListKind(V),V) ; a__U22(tt,V1,V2) >= a__U23(a__isPalListKind(V2),V1,V2) ; a__U22(X1,X2,X3) >= U22(X1,X2,X3) ; a__U21(tt,V1,V2) >= a__U22(a__isPalListKind(V1),V1,V2) ; a__U21(X1,X2,X3) >= U21(X1,X2,X3) ; a__U23(tt,V1,V2) >= a__U24(a__isPalListKind(V2),V1,V2) ; a__U23(X1,X2,X3) >= U23(X1,X2,X3) ; a__U24(tt,V1,V2) >= a__U25(a__isList(V1),V2) ; a__U24(X1,X2,X3) >= U24(X1,X2,X3) ; a__U25(tt,V2) >= a__U26(a__isList(V2)) ; a__U25(X1,X2) >= U25(X1,X2) ; a__isList(__(V1,V2)) >= a__U21(a__isPalListKind(V1),V1,V2) ; a__isList(nil) >= tt ; a__isList(X) >= isList(X) ; a__isList(V) >= a__U11(a__isPalListKind(V),V) ; a__U26(tt) >= tt ; a__U26(X) >= U26(X) ; a__U32(tt,V) >= a__U33(a__isQid(V)) ; a__U32(X1,X2) >= U32(X1,X2) ; a__U31(tt,V) >= a__U32(a__isPalListKind(V),V) ; a__U31(X1,X2) >= U31(X1,X2) ; a__U33(tt) >= tt ; a__U33(X) >= U33(X) ; a__isQid(a) >= tt ; a__isQid(e) >= tt ; a__isQid(i) >= tt ; a__isQid(o) >= tt ; a__isQid(u) >= tt ; a__isQid(X) >= isQid(X) ; a__U42(tt,V1,V2) >= a__U43(a__isPalListKind(V2),V1,V2) ; a__U42(X1,X2,X3) >= U42(X1,X2,X3) ; a__U41(tt,V1,V2) >= a__U42(a__isPalListKind(V1),V1,V2) ; a__U41(X1,X2,X3) >= U41(X1,X2,X3) ; a__U43(tt,V1,V2) >= a__U44(a__isPalListKind(V2),V1,V2) ; a__U43(X1,X2,X3) >= U43(X1,X2,X3) ; a__U44(tt,V1,V2) >= a__U45(a__isList(V1),V2) ; a__U44(X1,X2,X3) >= U44(X1,X2,X3) ; a__U45(tt,V2) >= a__U46(a__isNeList(V2)) ; a__U45(X1,X2) >= U45(X1,X2) ; a__U46(tt) >= tt ; a__U46(X) >= U46(X) ; a__U52(tt,V1,V2) >= a__U53(a__isPalListKind(V2),V1,V2) ; a__U52(X1,X2,X3) >= U52(X1,X2,X3) ; a__U51(tt,V1,V2) >= a__U52(a__isPalListKind(V1),V1,V2) ; a__U51(X1,X2,X3) >= U51(X1,X2,X3) ; a__U53(tt,V1,V2) >= a__U54(a__isPalListKind(V2),V1,V2) ; a__U53(X1,X2,X3) >= U53(X1,X2,X3) ; a__U54(tt,V1,V2) >= a__U55(a__isNeList(V1),V2) ; a__U54(X1,X2,X3) >= U54(X1,X2,X3) ; a__U55(tt,V2) >= a__U56(a__isList(V2)) ; a__U55(X1,X2) >= U55(X1,X2) ; a__U56(tt) >= tt ; a__U56(X) >= U56(X) ; a__U62(tt,V) >= a__U63(a__isQid(V)) ; a__U62(X1,X2) >= U62(X1,X2) ; a__U61(tt,V) >= a__U62(a__isPalListKind(V),V) ; a__U61(X1,X2) >= U61(X1,X2) ; a__U63(tt) >= tt ; a__U63(X) >= U63(X) ; a__U72(tt,P) >= a__U73(a__isPal(P),P) ; a__U72(X1,X2) >= U72(X1,X2) ; a__U71(tt,I,P) >= a__U72(a__isPalListKind(I),P) ; a__U71(X1,X2,X3) >= U71(X1,X2,X3) ; a__U73(tt,P) >= a__U74(a__isPalListKind(P)) ; a__U73(X1,X2) >= U73(X1,X2) ; a__isPal(nil) >= tt ; a__isPal(X) >= isPal(X) ; a__isPal(V) >= a__U81(a__isPalListKind(V),V) ; a__U74(tt) >= tt ; a__U74(X) >= U74(X) ; a__U82(tt,V) >= a__U83(a__isNePal(V)) ; a__U82(X1,X2) >= U82(X1,X2) ; a__U81(tt,V) >= a__U82(a__isPalListKind(V),V) ; a__U81(X1,X2) >= U81(X1,X2) ; a__U83(tt) >= tt ; a__U83(X) >= U83(X) ; a__isNePal(__(I,__(P,I))) >= a__U71(a__isQid(I),I,P) ; a__isNePal(X) >= isNePal(X) ; a__isNePal(V) >= a__U61(a__isPalListKind(V),V) ; a__U92(tt) >= tt ; a__U92(X) >= U92(X) ; a__U91(tt,V2) >= a__U92(a__isPalListKind(V2)) ; a__U91(X1,X2) >= U91(X1,X2) ; Marked_a__U55(tt,V2) >= Marked_a__isList(V2) ; Marked_a__U54(tt,V1,V2) >= Marked_a__U55(a__isNeList(V1),V2) ; Marked_a__U54(tt,V1,V2) >= Marked_a__isNeList(V1) ; Marked_a__U53(tt,V1,V2) >= Marked_a__U54(a__isPalListKind(V2),V1,V2) ; Marked_a__U52(tt,V1,V2) >= Marked_a__U53(a__isPalListKind(V2),V1,V2) ; Marked_a__U51(tt,V1,V2) >= Marked_a__U52(a__isPalListKind(V1),V1,V2) ; Marked_a__U45(tt,V2) >= Marked_a__isNeList(V2) ; Marked_a__U44(tt,V1,V2) >= Marked_a__U45(a__isList(V1),V2) ; Marked_a__U44(tt,V1,V2) >= Marked_a__isList(V1) ; Marked_a__U43(tt,V1,V2) >= Marked_a__U44(a__isPalListKind(V2),V1,V2) ; Marked_a__U42(tt,V1,V2) >= Marked_a__U43(a__isPalListKind(V2),V1,V2) ; Marked_a__U41(tt,V1,V2) >= Marked_a__U42(a__isPalListKind(V1),V1,V2) ; Marked_a__isList(__(V1,V2)) >= Marked_a__U21(a__isPalListKind(V1),V1,V2) ; Marked_a__isList(V) >= Marked_a__U11(a__isPalListKind(V),V) ; Marked_a__U25(tt,V2) >= Marked_a__isList(V2) ; Marked_a__U24(tt,V1,V2) >= Marked_a__isList(V1) ; Marked_a__U24(tt,V1,V2) >= Marked_a__U25(a__isList(V1),V2) ; Marked_a__U23(tt,V1,V2) >= Marked_a__U24(a__isPalListKind(V2),V1,V2) ; Marked_a__U22(tt,V1,V2) >= Marked_a__U23(a__isPalListKind(V2),V1,V2) ; Marked_a__U21(tt,V1,V2) >= Marked_a__U22(a__isPalListKind(V1),V1,V2) ; Marked_a__isNeList(__(V1,V2)) >= Marked_a__U51(a__isPalListKind(V1),V1,V2) ; Marked_a__isNeList(__(V1,V2)) >= Marked_a__U41(a__isPalListKind(V1),V1,V2) ; Marked_a__U12(tt,V) >= Marked_a__isNeList(V) ; Marked_a__U11(tt,V) >= Marked_a__U12(a__isPalListKind(V),V) ; } + Disjunctions:{ { Marked_a__U55(tt,V2) > Marked_a__isList(V2) ; } { Marked_a__U54(tt,V1,V2) > Marked_a__U55(a__isNeList(V1),V2) ; } { Marked_a__U54(tt,V1,V2) > Marked_a__isNeList(V1) ; } { Marked_a__U53(tt,V1,V2) > Marked_a__U54(a__isPalListKind(V2),V1,V2) ; } { Marked_a__U52(tt,V1,V2) > Marked_a__U53(a__isPalListKind(V2),V1,V2) ; } { Marked_a__U51(tt,V1,V2) > Marked_a__U52(a__isPalListKind(V1),V1,V2) ; } { Marked_a__U45(tt,V2) > Marked_a__isNeList(V2) ; } { Marked_a__U44(tt,V1,V2) > Marked_a__U45(a__isList(V1),V2) ; } { Marked_a__U44(tt,V1,V2) > Marked_a__isList(V1) ; } { Marked_a__U43(tt,V1,V2) > Marked_a__U44(a__isPalListKind(V2),V1,V2) ; } { Marked_a__U42(tt,V1,V2) > Marked_a__U43(a__isPalListKind(V2),V1,V2) ; } { Marked_a__U41(tt,V1,V2) > Marked_a__U42(a__isPalListKind(V1),V1,V2) ; } { Marked_a__isList(__(V1,V2)) > Marked_a__U21(a__isPalListKind(V1),V1,V2) ; } { Marked_a__isList(V) > Marked_a__U11(a__isPalListKind(V),V) ; } { Marked_a__U25(tt,V2) > Marked_a__isList(V2) ; } { Marked_a__U24(tt,V1,V2) > Marked_a__isList(V1) ; } { Marked_a__U24(tt,V1,V2) > Marked_a__U25(a__isList(V1),V2) ; } { Marked_a__U23(tt,V1,V2) > Marked_a__U24(a__isPalListKind(V2),V1,V2) ; } { Marked_a__U22(tt,V1,V2) > Marked_a__U23(a__isPalListKind(V2),V1,V2) ; } { Marked_a__U21(tt,V1,V2) > Marked_a__U22(a__isPalListKind(V1),V1,V2) ; } { Marked_a__isNeList(__(V1,V2)) > Marked_a__U51(a__isPalListKind(V1),V1,V2) ; } { Marked_a__isNeList(__(V1,V2)) > Marked_a__U41(a__isPalListKind(V1),V1,V2) ; } { Marked_a__U12(tt,V) > Marked_a__isNeList(V) ; } { Marked_a__U11(tt,V) > Marked_a__U12(a__isPalListKind(V),V) ; } } === TIMER virtual : 10.000000 === Entering poly_solver Starting Sat solver initialization Calling Sat solver... === STOPING TIMER virtual === === TIMER real : 10.000000 === === STOPING TIMER real === Sat solver returned Sat solver result read === STOPING TIMER real === === STOPING TIMER virtual === constraint: a____(__(X,Y),Z) >= a____(mark(X),a____(mark(Y),mark(Z))) constraint: a____(nil,X) >= mark(X) constraint: a____(X,nil) >= mark(X) constraint: a____(X1,X2) >= __(X1,X2) constraint: mark(__(X1,X2)) >= a____(mark(X1),mark(X2)) constraint: mark(nil) >= nil constraint: mark(tt) >= tt constraint: mark(a) >= a constraint: mark(e) >= e constraint: mark(i) >= i constraint: mark(o) >= o constraint: mark(u) >= u constraint: mark(U11(X1,X2)) >= a__U11(mark(X1),X2) constraint: mark(U12(X1,X2)) >= a__U12(mark(X1),X2) constraint: mark(isPalListKind(X)) >= a__isPalListKind(X) constraint: mark(U13(X)) >= a__U13(mark(X)) constraint: mark(isNeList(X)) >= a__isNeList(X) constraint: mark(U21(X1,X2,X3)) >= a__U21(mark(X1),X2,X3) constraint: mark(U22(X1,X2,X3)) >= a__U22(mark(X1),X2,X3) constraint: mark(U23(X1,X2,X3)) >= a__U23(mark(X1),X2,X3) constraint: mark(U24(X1,X2,X3)) >= a__U24(mark(X1),X2,X3) constraint: mark(U25(X1,X2)) >= a__U25(mark(X1),X2) constraint: mark(isList(X)) >= a__isList(X) constraint: mark(U26(X)) >= a__U26(mark(X)) constraint: mark(U31(X1,X2)) >= a__U31(mark(X1),X2) constraint: mark(U32(X1,X2)) >= a__U32(mark(X1),X2) constraint: mark(U33(X)) >= a__U33(mark(X)) constraint: mark(isQid(X)) >= a__isQid(X) constraint: mark(U41(X1,X2,X3)) >= a__U41(mark(X1),X2,X3) constraint: mark(U42(X1,X2,X3)) >= a__U42(mark(X1),X2,X3) constraint: mark(U43(X1,X2,X3)) >= a__U43(mark(X1),X2,X3) constraint: mark(U44(X1,X2,X3)) >= a__U44(mark(X1),X2,X3) constraint: mark(U45(X1,X2)) >= a__U45(mark(X1),X2) constraint: mark(U46(X)) >= a__U46(mark(X)) constraint: mark(U51(X1,X2,X3)) >= a__U51(mark(X1),X2,X3) constraint: mark(U52(X1,X2,X3)) >= a__U52(mark(X1),X2,X3) constraint: mark(U53(X1,X2,X3)) >= a__U53(mark(X1),X2,X3) constraint: mark(U54(X1,X2,X3)) >= a__U54(mark(X1),X2,X3) constraint: mark(U55(X1,X2)) >= a__U55(mark(X1),X2) constraint: mark(U56(X)) >= a__U56(mark(X)) constraint: mark(U61(X1,X2)) >= a__U61(mark(X1),X2) constraint: mark(U62(X1,X2)) >= a__U62(mark(X1),X2) constraint: mark(U63(X)) >= a__U63(mark(X)) constraint: mark(U71(X1,X2,X3)) >= a__U71(mark(X1),X2,X3) constraint: mark(U72(X1,X2)) >= a__U72(mark(X1),X2) constraint: mark(U73(X1,X2)) >= a__U73(mark(X1),X2) constraint: mark(isPal(X)) >= a__isPal(X) constraint: mark(U74(X)) >= a__U74(mark(X)) constraint: mark(U81(X1,X2)) >= a__U81(mark(X1),X2) constraint: mark(U82(X1,X2)) >= a__U82(mark(X1),X2) constraint: mark(U83(X)) >= a__U83(mark(X)) constraint: mark(isNePal(X)) >= a__isNePal(X) constraint: mark(U91(X1,X2)) >= a__U91(mark(X1),X2) constraint: mark(U92(X)) >= a__U92(mark(X)) constraint: a__U12(tt,V) >= a__U13(a__isNeList(V)) constraint: a__U12(X1,X2) >= U12(X1,X2) constraint: a__isPalListKind(__(V1,V2)) >= a__U91(a__isPalListKind(V1),V2) constraint: a__isPalListKind(nil) >= tt constraint: a__isPalListKind(a) >= tt constraint: a__isPalListKind(e) >= tt constraint: a__isPalListKind(i) >= tt constraint: a__isPalListKind(o) >= tt constraint: a__isPalListKind(u) >= tt constraint: a__isPalListKind(X) >= isPalListKind(X) constraint: a__U11(tt,V) >= a__U12(a__isPalListKind(V),V) constraint: a__U11(X1,X2) >= U11(X1,X2) constraint: a__U13(tt) >= tt constraint: a__U13(X) >= U13(X) constraint: a__isNeList(__(V1,V2)) >= a__U41(a__isPalListKind(V1),V1,V2) constraint: a__isNeList(__(V1,V2)) >= a__U51(a__isPalListKind(V1),V1,V2) constraint: a__isNeList(X) >= isNeList(X) constraint: a__isNeList(V) >= a__U31(a__isPalListKind(V),V) constraint: a__U22(tt,V1,V2) >= a__U23(a__isPalListKind(V2),V1,V2) constraint: a__U22(X1,X2,X3) >= U22(X1,X2,X3) constraint: a__U21(tt,V1,V2) >= a__U22(a__isPalListKind(V1),V1,V2) constraint: a__U21(X1,X2,X3) >= U21(X1,X2,X3) constraint: a__U23(tt,V1,V2) >= a__U24(a__isPalListKind(V2),V1,V2) constraint: a__U23(X1,X2,X3) >= U23(X1,X2,X3) constraint: a__U24(tt,V1,V2) >= a__U25(a__isList(V1),V2) constraint: a__U24(X1,X2,X3) >= U24(X1,X2,X3) constraint: a__U25(tt,V2) >= a__U26(a__isList(V2)) constraint: a__U25(X1,X2) >= U25(X1,X2) constraint: a__isList(__(V1,V2)) >= a__U21(a__isPalListKind(V1),V1,V2) constraint: a__isList(nil) >= tt constraint: a__isList(X) >= isList(X) constraint: a__isList(V) >= a__U11(a__isPalListKind(V),V) constraint: a__U26(tt) >= tt constraint: a__U26(X) >= U26(X) constraint: a__U32(tt,V) >= a__U33(a__isQid(V)) constraint: a__U32(X1,X2) >= U32(X1,X2) constraint: a__U31(tt,V) >= a__U32(a__isPalListKind(V),V) constraint: a__U31(X1,X2) >= U31(X1,X2) constraint: a__U33(tt) >= tt constraint: a__U33(X) >= U33(X) constraint: a__isQid(a) >= tt constraint: a__isQid(e) >= tt constraint: a__isQid(i) >= tt constraint: a__isQid(o) >= tt constraint: a__isQid(u) >= tt constraint: a__isQid(X) >= isQid(X) constraint: a__U42(tt,V1,V2) >= a__U43(a__isPalListKind(V2),V1,V2) constraint: a__U42(X1,X2,X3) >= U42(X1,X2,X3) constraint: a__U41(tt,V1,V2) >= a__U42(a__isPalListKind(V1),V1,V2) constraint: a__U41(X1,X2,X3) >= U41(X1,X2,X3) constraint: a__U43(tt,V1,V2) >= a__U44(a__isPalListKind(V2),V1,V2) constraint: a__U43(X1,X2,X3) >= U43(X1,X2,X3) constraint: a__U44(tt,V1,V2) >= a__U45(a__isList(V1),V2) constraint: a__U44(X1,X2,X3) >= U44(X1,X2,X3) constraint: a__U45(tt,V2) >= a__U46(a__isNeList(V2)) constraint: a__U45(X1,X2) >= U45(X1,X2) constraint: a__U46(tt) >= tt constraint: a__U46(X) >= U46(X) constraint: a__U52(tt,V1,V2) >= a__U53(a__isPalListKind(V2),V1,V2) constraint: a__U52(X1,X2,X3) >= U52(X1,X2,X3) constraint: a__U51(tt,V1,V2) >= a__U52(a__isPalListKind(V1),V1,V2) constraint: a__U51(X1,X2,X3) >= U51(X1,X2,X3) constraint: a__U53(tt,V1,V2) >= a__U54(a__isPalListKind(V2),V1,V2) constraint: a__U53(X1,X2,X3) >= U53(X1,X2,X3) constraint: a__U54(tt,V1,V2) >= a__U55(a__isNeList(V1),V2) constraint: a__U54(X1,X2,X3) >= U54(X1,X2,X3) constraint: a__U55(tt,V2) >= a__U56(a__isList(V2)) constraint: a__U55(X1,X2) >= U55(X1,X2) constraint: a__U56(tt) >= tt constraint: a__U56(X) >= U56(X) constraint: a__U62(tt,V) >= a__U63(a__isQid(V)) constraint: a__U62(X1,X2) >= U62(X1,X2) constraint: a__U61(tt,V) >= a__U62(a__isPalListKind(V),V) constraint: a__U61(X1,X2) >= U61(X1,X2) constraint: a__U63(tt) >= tt constraint: a__U63(X) >= U63(X) constraint: a__U72(tt,P) >= a__U73(a__isPal(P),P) constraint: a__U72(X1,X2) >= U72(X1,X2) constraint: a__U71(tt,I,P) >= a__U72(a__isPalListKind(I),P) constraint: a__U71(X1,X2,X3) >= U71(X1,X2,X3) constraint: a__U73(tt,P) >= a__U74(a__isPalListKind(P)) constraint: a__U73(X1,X2) >= U73(X1,X2) constraint: a__isPal(nil) >= tt constraint: a__isPal(X) >= isPal(X) constraint: a__isPal(V) >= a__U81(a__isPalListKind(V),V) constraint: a__U74(tt) >= tt constraint: a__U74(X) >= U74(X) constraint: a__U82(tt,V) >= a__U83(a__isNePal(V)) constraint: a__U82(X1,X2) >= U82(X1,X2) constraint: a__U81(tt,V) >= a__U82(a__isPalListKind(V),V) constraint: a__U81(X1,X2) >= U81(X1,X2) constraint: a__U83(tt) >= tt constraint: a__U83(X) >= U83(X) constraint: a__isNePal(__(I,__(P,I))) >= a__U71(a__isQid(I),I,P) constraint: a__isNePal(X) >= isNePal(X) constraint: a__isNePal(V) >= a__U61(a__isPalListKind(V),V) constraint: a__U92(tt) >= tt constraint: a__U92(X) >= U92(X) constraint: a__U91(tt,V2) >= a__U92(a__isPalListKind(V2)) constraint: a__U91(X1,X2) >= U91(X1,X2) constraint: Marked_a__U55(tt,V2) >= Marked_a__isList(V2) constraint: Marked_a__U54(tt,V1,V2) >= Marked_a__U55(a__isNeList(V1),V2) constraint: Marked_a__U54(tt,V1,V2) >= Marked_a__isNeList(V1) constraint: Marked_a__U53(tt,V1,V2) >= Marked_a__U54(a__isPalListKind(V2), V1,V2) constraint: Marked_a__U52(tt,V1,V2) >= Marked_a__U53(a__isPalListKind(V2), V1,V2) constraint: Marked_a__U51(tt,V1,V2) >= Marked_a__U52(a__isPalListKind(V1), V1,V2) constraint: Marked_a__U45(tt,V2) >= Marked_a__isNeList(V2) constraint: Marked_a__U44(tt,V1,V2) >= Marked_a__U45(a__isList(V1),V2) constraint: Marked_a__U44(tt,V1,V2) >= Marked_a__isList(V1) constraint: Marked_a__U43(tt,V1,V2) >= Marked_a__U44(a__isPalListKind(V2), V1,V2) constraint: Marked_a__U42(tt,V1,V2) >= Marked_a__U43(a__isPalListKind(V2), V1,V2) constraint: Marked_a__U41(tt,V1,V2) >= Marked_a__U42(a__isPalListKind(V1), V1,V2) constraint: Marked_a__isList(__(V1,V2)) >= Marked_a__U21(a__isPalListKind(V1), V1,V2) constraint: Marked_a__isList(V) >= Marked_a__U11(a__isPalListKind(V),V) constraint: Marked_a__U25(tt,V2) >= Marked_a__isList(V2) constraint: Marked_a__U24(tt,V1,V2) >= Marked_a__isList(V1) constraint: Marked_a__U24(tt,V1,V2) >= Marked_a__U25(a__isList(V1),V2) constraint: Marked_a__U23(tt,V1,V2) >= Marked_a__U24(a__isPalListKind(V2), V1,V2) constraint: Marked_a__U22(tt,V1,V2) >= Marked_a__U23(a__isPalListKind(V2), V1,V2) constraint: Marked_a__U21(tt,V1,V2) >= Marked_a__U22(a__isPalListKind(V1), V1,V2) constraint: Marked_a__isNeList(__(V1,V2)) >= Marked_a__U51(a__isPalListKind(V1), V1,V2) constraint: Marked_a__isNeList(__(V1,V2)) >= Marked_a__U41(a__isPalListKind(V1), V1,V2) constraint: Marked_a__U12(tt,V) >= Marked_a__isNeList(V) constraint: Marked_a__U11(tt,V) >= Marked_a__U12(a__isPalListKind(V),V) APPLY CRITERIA (Subterm criterion) ST: Marked_a__isNePal -> 1 Marked_a__U82 -> 2 Marked_a__U81 -> 2 Marked_a__isPal -> 1 Marked_a__U72 -> 2 Marked_a__U71 -> 3 APPLY CRITERIA (Subterm criterion) ST: Marked_a__isPalListKind -> 1 Marked_a__U91 -> 2 APPLY CRITERIA (Graph splitting) Found 1 components: { --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> } APPLY CRITERIA (Subterm criterion) APPLY CRITERIA (Choosing graph) Trying to solve the following constraints: { a____(__(X,Y),Z) >= a____(mark(X),a____(mark(Y),mark(Z))) ; a____(nil,X) >= mark(X) ; a____(X,nil) >= mark(X) ; a____(X1,X2) >= __(X1,X2) ; mark(__(X1,X2)) >= a____(mark(X1),mark(X2)) ; mark(nil) >= nil ; mark(tt) >= tt ; mark(a) >= a ; mark(e) >= e ; mark(i) >= i ; mark(o) >= o ; mark(u) >= u ; mark(U11(X1,X2)) >= a__U11(mark(X1),X2) ; mark(U12(X1,X2)) >= a__U12(mark(X1),X2) ; mark(isPalListKind(X)) >= a__isPalListKind(X) ; mark(U13(X)) >= a__U13(mark(X)) ; mark(isNeList(X)) >= a__isNeList(X) ; mark(U21(X1,X2,X3)) >= a__U21(mark(X1),X2,X3) ; mark(U22(X1,X2,X3)) >= a__U22(mark(X1),X2,X3) ; mark(U23(X1,X2,X3)) >= a__U23(mark(X1),X2,X3) ; mark(U24(X1,X2,X3)) >= a__U24(mark(X1),X2,X3) ; mark(U25(X1,X2)) >= a__U25(mark(X1),X2) ; mark(isList(X)) >= a__isList(X) ; mark(U26(X)) >= a__U26(mark(X)) ; mark(U31(X1,X2)) >= a__U31(mark(X1),X2) ; mark(U32(X1,X2)) >= a__U32(mark(X1),X2) ; mark(U33(X)) >= a__U33(mark(X)) ; mark(isQid(X)) >= a__isQid(X) ; mark(U41(X1,X2,X3)) >= a__U41(mark(X1),X2,X3) ; mark(U42(X1,X2,X3)) >= a__U42(mark(X1),X2,X3) ; mark(U43(X1,X2,X3)) >= a__U43(mark(X1),X2,X3) ; mark(U44(X1,X2,X3)) >= a__U44(mark(X1),X2,X3) ; mark(U45(X1,X2)) >= a__U45(mark(X1),X2) ; mark(U46(X)) >= a__U46(mark(X)) ; mark(U51(X1,X2,X3)) >= a__U51(mark(X1),X2,X3) ; mark(U52(X1,X2,X3)) >= a__U52(mark(X1),X2,X3) ; mark(U53(X1,X2,X3)) >= a__U53(mark(X1),X2,X3) ; mark(U54(X1,X2,X3)) >= a__U54(mark(X1),X2,X3) ; mark(U55(X1,X2)) >= a__U55(mark(X1),X2) ; mark(U56(X)) >= a__U56(mark(X)) ; mark(U61(X1,X2)) >= a__U61(mark(X1),X2) ; mark(U62(X1,X2)) >= a__U62(mark(X1),X2) ; mark(U63(X)) >= a__U63(mark(X)) ; mark(U71(X1,X2,X3)) >= a__U71(mark(X1),X2,X3) ; mark(U72(X1,X2)) >= a__U72(mark(X1),X2) ; mark(U73(X1,X2)) >= a__U73(mark(X1),X2) ; mark(isPal(X)) >= a__isPal(X) ; mark(U74(X)) >= a__U74(mark(X)) ; mark(U81(X1,X2)) >= a__U81(mark(X1),X2) ; mark(U82(X1,X2)) >= a__U82(mark(X1),X2) ; mark(U83(X)) >= a__U83(mark(X)) ; mark(isNePal(X)) >= a__isNePal(X) ; mark(U91(X1,X2)) >= a__U91(mark(X1),X2) ; mark(U92(X)) >= a__U92(mark(X)) ; a__U12(tt,V) >= a__U13(a__isNeList(V)) ; a__U12(X1,X2) >= U12(X1,X2) ; a__isPalListKind(__(V1,V2)) >= a__U91(a__isPalListKind(V1),V2) ; a__isPalListKind(nil) >= tt ; a__isPalListKind(a) >= tt ; a__isPalListKind(e) >= tt ; a__isPalListKind(i) >= tt ; a__isPalListKind(o) >= tt ; a__isPalListKind(u) >= tt ; a__isPalListKind(X) >= isPalListKind(X) ; a__U11(tt,V) >= a__U12(a__isPalListKind(V),V) ; a__U11(X1,X2) >= U11(X1,X2) ; a__U13(tt) >= tt ; a__U13(X) >= U13(X) ; a__isNeList(__(V1,V2)) >= a__U41(a__isPalListKind(V1),V1,V2) ; a__isNeList(__(V1,V2)) >= a__U51(a__isPalListKind(V1),V1,V2) ; a__isNeList(X) >= isNeList(X) ; a__isNeList(V) >= a__U31(a__isPalListKind(V),V) ; a__U22(tt,V1,V2) >= a__U23(a__isPalListKind(V2),V1,V2) ; a__U22(X1,X2,X3) >= U22(X1,X2,X3) ; a__U21(tt,V1,V2) >= a__U22(a__isPalListKind(V1),V1,V2) ; a__U21(X1,X2,X3) >= U21(X1,X2,X3) ; a__U23(tt,V1,V2) >= a__U24(a__isPalListKind(V2),V1,V2) ; a__U23(X1,X2,X3) >= U23(X1,X2,X3) ; a__U24(tt,V1,V2) >= a__U25(a__isList(V1),V2) ; a__U24(X1,X2,X3) >= U24(X1,X2,X3) ; a__U25(tt,V2) >= a__U26(a__isList(V2)) ; a__U25(X1,X2) >= U25(X1,X2) ; a__isList(__(V1,V2)) >= a__U21(a__isPalListKind(V1),V1,V2) ; a__isList(nil) >= tt ; a__isList(X) >= isList(X) ; a__isList(V) >= a__U11(a__isPalListKind(V),V) ; a__U26(tt) >= tt ; a__U26(X) >= U26(X) ; a__U32(tt,V) >= a__U33(a__isQid(V)) ; a__U32(X1,X2) >= U32(X1,X2) ; a__U31(tt,V) >= a__U32(a__isPalListKind(V),V) ; a__U31(X1,X2) >= U31(X1,X2) ; a__U33(tt) >= tt ; a__U33(X) >= U33(X) ; a__isQid(a) >= tt ; a__isQid(e) >= tt ; a__isQid(i) >= tt ; a__isQid(o) >= tt ; a__isQid(u) >= tt ; a__isQid(X) >= isQid(X) ; a__U42(tt,V1,V2) >= a__U43(a__isPalListKind(V2),V1,V2) ; a__U42(X1,X2,X3) >= U42(X1,X2,X3) ; a__U41(tt,V1,V2) >= a__U42(a__isPalListKind(V1),V1,V2) ; a__U41(X1,X2,X3) >= U41(X1,X2,X3) ; a__U43(tt,V1,V2) >= a__U44(a__isPalListKind(V2),V1,V2) ; a__U43(X1,X2,X3) >= U43(X1,X2,X3) ; a__U44(tt,V1,V2) >= a__U45(a__isList(V1),V2) ; a__U44(X1,X2,X3) >= U44(X1,X2,X3) ; a__U45(tt,V2) >= a__U46(a__isNeList(V2)) ; a__U45(X1,X2) >= U45(X1,X2) ; a__U46(tt) >= tt ; a__U46(X) >= U46(X) ; a__U52(tt,V1,V2) >= a__U53(a__isPalListKind(V2),V1,V2) ; a__U52(X1,X2,X3) >= U52(X1,X2,X3) ; a__U51(tt,V1,V2) >= a__U52(a__isPalListKind(V1),V1,V2) ; a__U51(X1,X2,X3) >= U51(X1,X2,X3) ; a__U53(tt,V1,V2) >= a__U54(a__isPalListKind(V2),V1,V2) ; a__U53(X1,X2,X3) >= U53(X1,X2,X3) ; a__U54(tt,V1,V2) >= a__U55(a__isNeList(V1),V2) ; a__U54(X1,X2,X3) >= U54(X1,X2,X3) ; a__U55(tt,V2) >= a__U56(a__isList(V2)) ; a__U55(X1,X2) >= U55(X1,X2) ; a__U56(tt) >= tt ; a__U56(X) >= U56(X) ; a__U62(tt,V) >= a__U63(a__isQid(V)) ; a__U62(X1,X2) >= U62(X1,X2) ; a__U61(tt,V) >= a__U62(a__isPalListKind(V),V) ; a__U61(X1,X2) >= U61(X1,X2) ; a__U63(tt) >= tt ; a__U63(X) >= U63(X) ; a__U72(tt,P) >= a__U73(a__isPal(P),P) ; a__U72(X1,X2) >= U72(X1,X2) ; a__U71(tt,I,P) >= a__U72(a__isPalListKind(I),P) ; a__U71(X1,X2,X3) >= U71(X1,X2,X3) ; a__U73(tt,P) >= a__U74(a__isPalListKind(P)) ; a__U73(X1,X2) >= U73(X1,X2) ; a__isPal(nil) >= tt ; a__isPal(X) >= isPal(X) ; a__isPal(V) >= a__U81(a__isPalListKind(V),V) ; a__U74(tt) >= tt ; a__U74(X) >= U74(X) ; a__U82(tt,V) >= a__U83(a__isNePal(V)) ; a__U82(X1,X2) >= U82(X1,X2) ; a__U81(tt,V) >= a__U82(a__isPalListKind(V),V) ; a__U81(X1,X2) >= U81(X1,X2) ; a__U83(tt) >= tt ; a__U83(X) >= U83(X) ; a__isNePal(__(I,__(P,I))) >= a__U71(a__isQid(I),I,P) ; a__isNePal(X) >= isNePal(X) ; a__isNePal(V) >= a__U61(a__isPalListKind(V),V) ; a__U92(tt) >= tt ; a__U92(X) >= U92(X) ; a__U91(tt,V2) >= a__U92(a__isPalListKind(V2)) ; a__U91(X1,X2) >= U91(X1,X2) ; Marked_a____(__(X,Y),Z) >= Marked_a____(mark(X),a____(mark(Y),mark(Z))) ; Marked_a____(__(X,Y),Z) >= Marked_a____(mark(Y),mark(Z)) ; Marked_a____(__(X,Y),Z) >= Marked_mark(X) ; Marked_a____(__(X,Y),Z) >= Marked_mark(Y) ; Marked_a____(__(X,Y),Z) >= Marked_mark(Z) ; Marked_mark(__(X1,X2)) >= Marked_a____(mark(X1),mark(X2)) ; Marked_mark(__(X1,X2)) >= Marked_mark(X1) ; Marked_mark(__(X1,X2)) >= Marked_mark(X2) ; Marked_mark(U11(X1,X2)) >= Marked_mark(X1) ; Marked_mark(U12(X1,X2)) >= Marked_mark(X1) ; Marked_mark(U13(X)) >= Marked_mark(X) ; Marked_mark(U21(X1,X2,X3)) >= Marked_mark(X1) ; Marked_mark(U22(X1,X2,X3)) >= Marked_mark(X1) ; Marked_mark(U23(X1,X2,X3)) >= Marked_mark(X1) ; Marked_mark(U24(X1,X2,X3)) >= Marked_mark(X1) ; Marked_mark(U25(X1,X2)) >= Marked_mark(X1) ; Marked_mark(U26(X)) >= Marked_mark(X) ; Marked_mark(U31(X1,X2)) >= Marked_mark(X1) ; Marked_mark(U32(X1,X2)) >= Marked_mark(X1) ; Marked_mark(U33(X)) >= Marked_mark(X) ; Marked_mark(U41(X1,X2,X3)) >= Marked_mark(X1) ; Marked_mark(U42(X1,X2,X3)) >= Marked_mark(X1) ; Marked_mark(U43(X1,X2,X3)) >= Marked_mark(X1) ; Marked_mark(U44(X1,X2,X3)) >= Marked_mark(X1) ; Marked_mark(U45(X1,X2)) >= Marked_mark(X1) ; Marked_mark(U46(X)) >= Marked_mark(X) ; Marked_mark(U51(X1,X2,X3)) >= Marked_mark(X1) ; Marked_mark(U52(X1,X2,X3)) >= Marked_mark(X1) ; Marked_mark(U53(X1,X2,X3)) >= Marked_mark(X1) ; Marked_mark(U54(X1,X2,X3)) >= Marked_mark(X1) ; Marked_mark(U55(X1,X2)) >= Marked_mark(X1) ; Marked_mark(U56(X)) >= Marked_mark(X) ; Marked_mark(U61(X1,X2)) >= Marked_mark(X1) ; Marked_mark(U62(X1,X2)) >= Marked_mark(X1) ; Marked_mark(U63(X)) >= Marked_mark(X) ; Marked_mark(U71(X1,X2,X3)) >= Marked_mark(X1) ; Marked_mark(U72(X1,X2)) >= Marked_mark(X1) ; Marked_mark(U73(X1,X2)) >= Marked_mark(X1) ; Marked_mark(U74(X)) >= Marked_mark(X) ; Marked_mark(U81(X1,X2)) >= Marked_mark(X1) ; Marked_mark(U82(X1,X2)) >= Marked_mark(X1) ; Marked_mark(U83(X)) >= Marked_mark(X) ; Marked_mark(U91(X1,X2)) >= Marked_mark(X1) ; Marked_mark(U92(X)) >= Marked_mark(X) ; } + Disjunctions:{ { Marked_a____(__(X,Y),Z) > Marked_a____(mark(X),a____(mark(Y),mark(Z))) ; } { Marked_a____(__(X,Y),Z) > Marked_a____(mark(Y),mark(Z)) ; } { Marked_a____(__(X,Y),Z) > Marked_mark(X) ; } { Marked_a____(__(X,Y),Z) > Marked_mark(Y) ; } { Marked_a____(__(X,Y),Z) > Marked_mark(Z) ; } { Marked_mark(__(X1,X2)) > Marked_a____(mark(X1),mark(X2)) ; } { Marked_mark(__(X1,X2)) > Marked_mark(X1) ; } { Marked_mark(__(X1,X2)) > Marked_mark(X2) ; } { Marked_mark(U11(X1,X2)) > Marked_mark(X1) ; } { Marked_mark(U12(X1,X2)) > Marked_mark(X1) ; } { Marked_mark(U13(X)) > Marked_mark(X) ; } { Marked_mark(U21(X1,X2,X3)) > Marked_mark(X1) ; } { Marked_mark(U22(X1,X2,X3)) > Marked_mark(X1) ; } { Marked_mark(U23(X1,X2,X3)) > Marked_mark(X1) ; } { Marked_mark(U24(X1,X2,X3)) > Marked_mark(X1) ; } { Marked_mark(U25(X1,X2)) > Marked_mark(X1) ; } { Marked_mark(U26(X)) > Marked_mark(X) ; } { Marked_mark(U31(X1,X2)) > Marked_mark(X1) ; } { Marked_mark(U32(X1,X2)) > Marked_mark(X1) ; } { Marked_mark(U33(X)) > Marked_mark(X) ; } { Marked_mark(U41(X1,X2,X3)) > Marked_mark(X1) ; } { Marked_mark(U42(X1,X2,X3)) > Marked_mark(X1) ; } { Marked_mark(U43(X1,X2,X3)) > Marked_mark(X1) ; } { Marked_mark(U44(X1,X2,X3)) > Marked_mark(X1) ; } { Marked_mark(U45(X1,X2)) > Marked_mark(X1) ; } { Marked_mark(U46(X)) > Marked_mark(X) ; } { Marked_mark(U51(X1,X2,X3)) > Marked_mark(X1) ; } { Marked_mark(U52(X1,X2,X3)) > Marked_mark(X1) ; } { Marked_mark(U53(X1,X2,X3)) > Marked_mark(X1) ; } { Marked_mark(U54(X1,X2,X3)) > Marked_mark(X1) ; } { Marked_mark(U55(X1,X2)) > Marked_mark(X1) ; } { Marked_mark(U56(X)) > Marked_mark(X) ; } { Marked_mark(U61(X1,X2)) > Marked_mark(X1) ; } { Marked_mark(U62(X1,X2)) > Marked_mark(X1) ; } { Marked_mark(U63(X)) > Marked_mark(X) ; } { Marked_mark(U71(X1,X2,X3)) > Marked_mark(X1) ; } { Marked_mark(U72(X1,X2)) > Marked_mark(X1) ; } { Marked_mark(U73(X1,X2)) > Marked_mark(X1) ; } { Marked_mark(U74(X)) > Marked_mark(X) ; } { Marked_mark(U81(X1,X2)) > Marked_mark(X1) ; } { Marked_mark(U82(X1,X2)) > Marked_mark(X1) ; } { Marked_mark(U83(X)) > Marked_mark(X) ; } { Marked_mark(U91(X1,X2)) > Marked_mark(X1) ; } { Marked_mark(U92(X)) > Marked_mark(X) ; } } === TIMER virtual : 10.000000 === Entering poly_solver Starting Sat solver initialization Calling Sat solver... === STOPING TIMER virtual === === TIMER real : 10.000000 === === STOPING TIMER real === Sat solver returned Sat solver result read === STOPING TIMER real === === STOPING TIMER virtual === constraint: a____(__(X,Y),Z) >= a____(mark(X),a____(mark(Y),mark(Z))) constraint: a____(nil,X) >= mark(X) constraint: a____(X,nil) >= mark(X) constraint: a____(X1,X2) >= __(X1,X2) constraint: mark(__(X1,X2)) >= a____(mark(X1),mark(X2)) constraint: mark(nil) >= nil constraint: mark(tt) >= tt constraint: mark(a) >= a constraint: mark(e) >= e constraint: mark(i) >= i constraint: mark(o) >= o constraint: mark(u) >= u constraint: mark(U11(X1,X2)) >= a__U11(mark(X1),X2) constraint: mark(U12(X1,X2)) >= a__U12(mark(X1),X2) constraint: mark(isPalListKind(X)) >= a__isPalListKind(X) constraint: mark(U13(X)) >= a__U13(mark(X)) constraint: mark(isNeList(X)) >= a__isNeList(X) constraint: mark(U21(X1,X2,X3)) >= a__U21(mark(X1),X2,X3) constraint: mark(U22(X1,X2,X3)) >= a__U22(mark(X1),X2,X3) constraint: mark(U23(X1,X2,X3)) >= a__U23(mark(X1),X2,X3) constraint: mark(U24(X1,X2,X3)) >= a__U24(mark(X1),X2,X3) constraint: mark(U25(X1,X2)) >= a__U25(mark(X1),X2) constraint: mark(isList(X)) >= a__isList(X) constraint: mark(U26(X)) >= a__U26(mark(X)) constraint: mark(U31(X1,X2)) >= a__U31(mark(X1),X2) constraint: mark(U32(X1,X2)) >= a__U32(mark(X1),X2) constraint: mark(U33(X)) >= a__U33(mark(X)) constraint: mark(isQid(X)) >= a__isQid(X) constraint: mark(U41(X1,X2,X3)) >= a__U41(mark(X1),X2,X3) constraint: mark(U42(X1,X2,X3)) >= a__U42(mark(X1),X2,X3) constraint: mark(U43(X1,X2,X3)) >= a__U43(mark(X1),X2,X3) constraint: mark(U44(X1,X2,X3)) >= a__U44(mark(X1),X2,X3) constraint: mark(U45(X1,X2)) >= a__U45(mark(X1),X2) constraint: mark(U46(X)) >= a__U46(mark(X)) constraint: mark(U51(X1,X2,X3)) >= a__U51(mark(X1),X2,X3) constraint: mark(U52(X1,X2,X3)) >= a__U52(mark(X1),X2,X3) constraint: mark(U53(X1,X2,X3)) >= a__U53(mark(X1),X2,X3) constraint: mark(U54(X1,X2,X3)) >= a__U54(mark(X1),X2,X3) constraint: mark(U55(X1,X2)) >= a__U55(mark(X1),X2) constraint: mark(U56(X)) >= a__U56(mark(X)) constraint: mark(U61(X1,X2)) >= a__U61(mark(X1),X2) constraint: mark(U62(X1,X2)) >= a__U62(mark(X1),X2) constraint: mark(U63(X)) >= a__U63(mark(X)) constraint: mark(U71(X1,X2,X3)) >= a__U71(mark(X1),X2,X3) constraint: mark(U72(X1,X2)) >= a__U72(mark(X1),X2) constraint: mark(U73(X1,X2)) >= a__U73(mark(X1),X2) constraint: mark(isPal(X)) >= a__isPal(X) constraint: mark(U74(X)) >= a__U74(mark(X)) constraint: mark(U81(X1,X2)) >= a__U81(mark(X1),X2) constraint: mark(U82(X1,X2)) >= a__U82(mark(X1),X2) constraint: mark(U83(X)) >= a__U83(mark(X)) constraint: mark(isNePal(X)) >= a__isNePal(X) constraint: mark(U91(X1,X2)) >= a__U91(mark(X1),X2) constraint: mark(U92(X)) >= a__U92(mark(X)) constraint: a__U12(tt,V) >= a__U13(a__isNeList(V)) constraint: a__U12(X1,X2) >= U12(X1,X2) constraint: a__isPalListKind(__(V1,V2)) >= a__U91(a__isPalListKind(V1),V2) constraint: a__isPalListKind(nil) >= tt constraint: a__isPalListKind(a) >= tt constraint: a__isPalListKind(e) >= tt constraint: a__isPalListKind(i) >= tt constraint: a__isPalListKind(o) >= tt constraint: a__isPalListKind(u) >= tt constraint: a__isPalListKind(X) >= isPalListKind(X) constraint: a__U11(tt,V) >= a__U12(a__isPalListKind(V),V) constraint: a__U11(X1,X2) >= U11(X1,X2) constraint: a__U13(tt) >= tt constraint: a__U13(X) >= U13(X) constraint: a__isNeList(__(V1,V2)) >= a__U41(a__isPalListKind(V1),V1,V2) constraint: a__isNeList(__(V1,V2)) >= a__U51(a__isPalListKind(V1),V1,V2) constraint: a__isNeList(X) >= isNeList(X) constraint: a__isNeList(V) >= a__U31(a__isPalListKind(V),V) constraint: a__U22(tt,V1,V2) >= a__U23(a__isPalListKind(V2),V1,V2) constraint: a__U22(X1,X2,X3) >= U22(X1,X2,X3) constraint: a__U21(tt,V1,V2) >= a__U22(a__isPalListKind(V1),V1,V2) constraint: a__U21(X1,X2,X3) >= U21(X1,X2,X3) constraint: a__U23(tt,V1,V2) >= a__U24(a__isPalListKind(V2),V1,V2) constraint: a__U23(X1,X2,X3) >= U23(X1,X2,X3) constraint: a__U24(tt,V1,V2) >= a__U25(a__isList(V1),V2) constraint: a__U24(X1,X2,X3) >= U24(X1,X2,X3) constraint: a__U25(tt,V2) >= a__U26(a__isList(V2)) constraint: a__U25(X1,X2) >= U25(X1,X2) constraint: a__isList(__(V1,V2)) >= a__U21(a__isPalListKind(V1),V1,V2) constraint: a__isList(nil) >= tt constraint: a__isList(X) >= isList(X) constraint: a__isList(V) >= a__U11(a__isPalListKind(V),V) constraint: a__U26(tt) >= tt constraint: a__U26(X) >= U26(X) constraint: a__U32(tt,V) >= a__U33(a__isQid(V)) constraint: a__U32(X1,X2) >= U32(X1,X2) constraint: a__U31(tt,V) >= a__U32(a__isPalListKind(V),V) constraint: a__U31(X1,X2) >= U31(X1,X2) constraint: a__U33(tt) >= tt constraint: a__U33(X) >= U33(X) constraint: a__isQid(a) >= tt constraint: a__isQid(e) >= tt constraint: a__isQid(i) >= tt constraint: a__isQid(o) >= tt constraint: a__isQid(u) >= tt constraint: a__isQid(X) >= isQid(X) constraint: a__U42(tt,V1,V2) >= a__U43(a__isPalListKind(V2),V1,V2) constraint: a__U42(X1,X2,X3) >= U42(X1,X2,X3) constraint: a__U41(tt,V1,V2) >= a__U42(a__isPalListKind(V1),V1,V2) constraint: a__U41(X1,X2,X3) >= U41(X1,X2,X3) constraint: a__U43(tt,V1,V2) >= a__U44(a__isPalListKind(V2),V1,V2) constraint: a__U43(X1,X2,X3) >= U43(X1,X2,X3) constraint: a__U44(tt,V1,V2) >= a__U45(a__isList(V1),V2) constraint: a__U44(X1,X2,X3) >= U44(X1,X2,X3) constraint: a__U45(tt,V2) >= a__U46(a__isNeList(V2)) constraint: a__U45(X1,X2) >= U45(X1,X2) constraint: a__U46(tt) >= tt constraint: a__U46(X) >= U46(X) constraint: a__U52(tt,V1,V2) >= a__U53(a__isPalListKind(V2),V1,V2) constraint: a__U52(X1,X2,X3) >= U52(X1,X2,X3) constraint: a__U51(tt,V1,V2) >= a__U52(a__isPalListKind(V1),V1,V2) constraint: a__U51(X1,X2,X3) >= U51(X1,X2,X3) constraint: a__U53(tt,V1,V2) >= a__U54(a__isPalListKind(V2),V1,V2) constraint: a__U53(X1,X2,X3) >= U53(X1,X2,X3) constraint: a__U54(tt,V1,V2) >= a__U55(a__isNeList(V1),V2) constraint: a__U54(X1,X2,X3) >= U54(X1,X2,X3) constraint: a__U55(tt,V2) >= a__U56(a__isList(V2)) constraint: a__U55(X1,X2) >= U55(X1,X2) constraint: a__U56(tt) >= tt constraint: a__U56(X) >= U56(X) constraint: a__U62(tt,V) >= a__U63(a__isQid(V)) constraint: a__U62(X1,X2) >= U62(X1,X2) constraint: a__U61(tt,V) >= a__U62(a__isPalListKind(V),V) constraint: a__U61(X1,X2) >= U61(X1,X2) constraint: a__U63(tt) >= tt constraint: a__U63(X) >= U63(X) constraint: a__U72(tt,P) >= a__U73(a__isPal(P),P) constraint: a__U72(X1,X2) >= U72(X1,X2) constraint: a__U71(tt,I,P) >= a__U72(a__isPalListKind(I),P) constraint: a__U71(X1,X2,X3) >= U71(X1,X2,X3) constraint: a__U73(tt,P) >= a__U74(a__isPalListKind(P)) constraint: a__U73(X1,X2) >= U73(X1,X2) constraint: a__isPal(nil) >= tt constraint: a__isPal(X) >= isPal(X) constraint: a__isPal(V) >= a__U81(a__isPalListKind(V),V) constraint: a__U74(tt) >= tt constraint: a__U74(X) >= U74(X) constraint: a__U82(tt,V) >= a__U83(a__isNePal(V)) constraint: a__U82(X1,X2) >= U82(X1,X2) constraint: a__U81(tt,V) >= a__U82(a__isPalListKind(V),V) constraint: a__U81(X1,X2) >= U81(X1,X2) constraint: a__U83(tt) >= tt constraint: a__U83(X) >= U83(X) constraint: a__isNePal(__(I,__(P,I))) >= a__U71(a__isQid(I),I,P) constraint: a__isNePal(X) >= isNePal(X) constraint: a__isNePal(V) >= a__U61(a__isPalListKind(V),V) constraint: a__U92(tt) >= tt constraint: a__U92(X) >= U92(X) constraint: a__U91(tt,V2) >= a__U92(a__isPalListKind(V2)) constraint: a__U91(X1,X2) >= U91(X1,X2) constraint: Marked_a____(__(X,Y),Z) >= Marked_a____(mark(X), a____(mark(Y),mark(Z))) constraint: Marked_a____(__(X,Y),Z) >= Marked_a____(mark(Y),mark(Z)) constraint: Marked_a____(__(X,Y),Z) >= Marked_mark(X) constraint: Marked_a____(__(X,Y),Z) >= Marked_mark(Y) constraint: Marked_a____(__(X,Y),Z) >= Marked_mark(Z) constraint: Marked_mark(__(X1,X2)) >= Marked_a____(mark(X1),mark(X2)) constraint: Marked_mark(__(X1,X2)) >= Marked_mark(X1) constraint: Marked_mark(__(X1,X2)) >= Marked_mark(X2) constraint: Marked_mark(U11(X1,X2)) >= Marked_mark(X1) constraint: Marked_mark(U12(X1,X2)) >= Marked_mark(X1) constraint: Marked_mark(U13(X)) >= Marked_mark(X) constraint: Marked_mark(U21(X1,X2,X3)) >= Marked_mark(X1) constraint: Marked_mark(U22(X1,X2,X3)) >= Marked_mark(X1) constraint: Marked_mark(U23(X1,X2,X3)) >= Marked_mark(X1) constraint: Marked_mark(U24(X1,X2,X3)) >= Marked_mark(X1) constraint: Marked_mark(U25(X1,X2)) >= Marked_mark(X1) constraint: Marked_mark(U26(X)) >= Marked_mark(X) constraint: Marked_mark(U31(X1,X2)) >= Marked_mark(X1) constraint: Marked_mark(U32(X1,X2)) >= Marked_mark(X1) constraint: Marked_mark(U33(X)) >= Marked_mark(X) constraint: Marked_mark(U41(X1,X2,X3)) >= Marked_mark(X1) constraint: Marked_mark(U42(X1,X2,X3)) >= Marked_mark(X1) constraint: Marked_mark(U43(X1,X2,X3)) >= Marked_mark(X1) constraint: Marked_mark(U44(X1,X2,X3)) >= Marked_mark(X1) constraint: Marked_mark(U45(X1,X2)) >= Marked_mark(X1) constraint: Marked_mark(U46(X)) >= Marked_mark(X) constraint: Marked_mark(U51(X1,X2,X3)) >= Marked_mark(X1) constraint: Marked_mark(U52(X1,X2,X3)) >= Marked_mark(X1) constraint: Marked_mark(U53(X1,X2,X3)) >= Marked_mark(X1) constraint: Marked_mark(U54(X1,X2,X3)) >= Marked_mark(X1) constraint: Marked_mark(U55(X1,X2)) >= Marked_mark(X1) constraint: Marked_mark(U56(X)) >= Marked_mark(X) constraint: Marked_mark(U61(X1,X2)) >= Marked_mark(X1) constraint: Marked_mark(U62(X1,X2)) >= Marked_mark(X1) constraint: Marked_mark(U63(X)) >= Marked_mark(X) constraint: Marked_mark(U71(X1,X2,X3)) >= Marked_mark(X1) constraint: Marked_mark(U72(X1,X2)) >= Marked_mark(X1) constraint: Marked_mark(U73(X1,X2)) >= Marked_mark(X1) constraint: Marked_mark(U74(X)) >= Marked_mark(X) constraint: Marked_mark(U81(X1,X2)) >= Marked_mark(X1) constraint: Marked_mark(U82(X1,X2)) >= Marked_mark(X1) constraint: Marked_mark(U83(X)) >= Marked_mark(X) constraint: Marked_mark(U91(X1,X2)) >= Marked_mark(X1) constraint: Marked_mark(U92(X)) >= Marked_mark(X) APPLY CRITERIA (Graph splitting) Found 2 components: { --> } { --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> } APPLY CRITERIA (Subterm criterion) APPLY CRITERIA (Choosing graph) Trying to solve the following constraints: { a____(__(X,Y),Z) >= a____(mark(X),a____(mark(Y),mark(Z))) ; a____(nil,X) >= mark(X) ; a____(X,nil) >= mark(X) ; a____(X1,X2) >= __(X1,X2) ; mark(__(X1,X2)) >= a____(mark(X1),mark(X2)) ; mark(nil) >= nil ; mark(tt) >= tt ; mark(a) >= a ; mark(e) >= e ; mark(i) >= i ; mark(o) >= o ; mark(u) >= u ; mark(U11(X1,X2)) >= a__U11(mark(X1),X2) ; mark(U12(X1,X2)) >= a__U12(mark(X1),X2) ; mark(isPalListKind(X)) >= a__isPalListKind(X) ; mark(U13(X)) >= a__U13(mark(X)) ; mark(isNeList(X)) >= a__isNeList(X) ; mark(U21(X1,X2,X3)) >= a__U21(mark(X1),X2,X3) ; mark(U22(X1,X2,X3)) >= a__U22(mark(X1),X2,X3) ; mark(U23(X1,X2,X3)) >= a__U23(mark(X1),X2,X3) ; mark(U24(X1,X2,X3)) >= a__U24(mark(X1),X2,X3) ; mark(U25(X1,X2)) >= a__U25(mark(X1),X2) ; mark(isList(X)) >= a__isList(X) ; mark(U26(X)) >= a__U26(mark(X)) ; mark(U31(X1,X2)) >= a__U31(mark(X1),X2) ; mark(U32(X1,X2)) >= a__U32(mark(X1),X2) ; mark(U33(X)) >= a__U33(mark(X)) ; mark(isQid(X)) >= a__isQid(X) ; mark(U41(X1,X2,X3)) >= a__U41(mark(X1),X2,X3) ; mark(U42(X1,X2,X3)) >= a__U42(mark(X1),X2,X3) ; mark(U43(X1,X2,X3)) >= a__U43(mark(X1),X2,X3) ; mark(U44(X1,X2,X3)) >= a__U44(mark(X1),X2,X3) ; mark(U45(X1,X2)) >= a__U45(mark(X1),X2) ; mark(U46(X)) >= a__U46(mark(X)) ; mark(U51(X1,X2,X3)) >= a__U51(mark(X1),X2,X3) ; mark(U52(X1,X2,X3)) >= a__U52(mark(X1),X2,X3) ; mark(U53(X1,X2,X3)) >= a__U53(mark(X1),X2,X3) ; mark(U54(X1,X2,X3)) >= a__U54(mark(X1),X2,X3) ; mark(U55(X1,X2)) >= a__U55(mark(X1),X2) ; mark(U56(X)) >= a__U56(mark(X)) ; mark(U61(X1,X2)) >= a__U61(mark(X1),X2) ; mark(U62(X1,X2)) >= a__U62(mark(X1),X2) ; mark(U63(X)) >= a__U63(mark(X)) ; mark(U71(X1,X2,X3)) >= a__U71(mark(X1),X2,X3) ; mark(U72(X1,X2)) >= a__U72(mark(X1),X2) ; mark(U73(X1,X2)) >= a__U73(mark(X1),X2) ; mark(isPal(X)) >= a__isPal(X) ; mark(U74(X)) >= a__U74(mark(X)) ; mark(U81(X1,X2)) >= a__U81(mark(X1),X2) ; mark(U82(X1,X2)) >= a__U82(mark(X1),X2) ; mark(U83(X)) >= a__U83(mark(X)) ; mark(isNePal(X)) >= a__isNePal(X) ; mark(U91(X1,X2)) >= a__U91(mark(X1),X2) ; mark(U92(X)) >= a__U92(mark(X)) ; a__U12(tt,V) >= a__U13(a__isNeList(V)) ; a__U12(X1,X2) >= U12(X1,X2) ; a__isPalListKind(__(V1,V2)) >= a__U91(a__isPalListKind(V1),V2) ; a__isPalListKind(nil) >= tt ; a__isPalListKind(a) >= tt ; a__isPalListKind(e) >= tt ; a__isPalListKind(i) >= tt ; a__isPalListKind(o) >= tt ; a__isPalListKind(u) >= tt ; a__isPalListKind(X) >= isPalListKind(X) ; a__U11(tt,V) >= a__U12(a__isPalListKind(V),V) ; a__U11(X1,X2) >= U11(X1,X2) ; a__U13(tt) >= tt ; a__U13(X) >= U13(X) ; a__isNeList(__(V1,V2)) >= a__U41(a__isPalListKind(V1),V1,V2) ; a__isNeList(__(V1,V2)) >= a__U51(a__isPalListKind(V1),V1,V2) ; a__isNeList(X) >= isNeList(X) ; a__isNeList(V) >= a__U31(a__isPalListKind(V),V) ; a__U22(tt,V1,V2) >= a__U23(a__isPalListKind(V2),V1,V2) ; a__U22(X1,X2,X3) >= U22(X1,X2,X3) ; a__U21(tt,V1,V2) >= a__U22(a__isPalListKind(V1),V1,V2) ; a__U21(X1,X2,X3) >= U21(X1,X2,X3) ; a__U23(tt,V1,V2) >= a__U24(a__isPalListKind(V2),V1,V2) ; a__U23(X1,X2,X3) >= U23(X1,X2,X3) ; a__U24(tt,V1,V2) >= a__U25(a__isList(V1),V2) ; a__U24(X1,X2,X3) >= U24(X1,X2,X3) ; a__U25(tt,V2) >= a__U26(a__isList(V2)) ; a__U25(X1,X2) >= U25(X1,X2) ; a__isList(__(V1,V2)) >= a__U21(a__isPalListKind(V1),V1,V2) ; a__isList(nil) >= tt ; a__isList(X) >= isList(X) ; a__isList(V) >= a__U11(a__isPalListKind(V),V) ; a__U26(tt) >= tt ; a__U26(X) >= U26(X) ; a__U32(tt,V) >= a__U33(a__isQid(V)) ; a__U32(X1,X2) >= U32(X1,X2) ; a__U31(tt,V) >= a__U32(a__isPalListKind(V),V) ; a__U31(X1,X2) >= U31(X1,X2) ; a__U33(tt) >= tt ; a__U33(X) >= U33(X) ; a__isQid(a) >= tt ; a__isQid(e) >= tt ; a__isQid(i) >= tt ; a__isQid(o) >= tt ; a__isQid(u) >= tt ; a__isQid(X) >= isQid(X) ; a__U42(tt,V1,V2) >= a__U43(a__isPalListKind(V2),V1,V2) ; a__U42(X1,X2,X3) >= U42(X1,X2,X3) ; a__U41(tt,V1,V2) >= a__U42(a__isPalListKind(V1),V1,V2) ; a__U41(X1,X2,X3) >= U41(X1,X2,X3) ; a__U43(tt,V1,V2) >= a__U44(a__isPalListKind(V2),V1,V2) ; a__U43(X1,X2,X3) >= U43(X1,X2,X3) ; a__U44(tt,V1,V2) >= a__U45(a__isList(V1),V2) ; a__U44(X1,X2,X3) >= U44(X1,X2,X3) ; a__U45(tt,V2) >= a__U46(a__isNeList(V2)) ; a__U45(X1,X2) >= U45(X1,X2) ; a__U46(tt) >= tt ; a__U46(X) >= U46(X) ; a__U52(tt,V1,V2) >= a__U53(a__isPalListKind(V2),V1,V2) ; a__U52(X1,X2,X3) >= U52(X1,X2,X3) ; a__U51(tt,V1,V2) >= a__U52(a__isPalListKind(V1),V1,V2) ; a__U51(X1,X2,X3) >= U51(X1,X2,X3) ; a__U53(tt,V1,V2) >= a__U54(a__isPalListKind(V2),V1,V2) ; a__U53(X1,X2,X3) >= U53(X1,X2,X3) ; a__U54(tt,V1,V2) >= a__U55(a__isNeList(V1),V2) ; a__U54(X1,X2,X3) >= U54(X1,X2,X3) ; a__U55(tt,V2) >= a__U56(a__isList(V2)) ; a__U55(X1,X2) >= U55(X1,X2) ; a__U56(tt) >= tt ; a__U56(X) >= U56(X) ; a__U62(tt,V) >= a__U63(a__isQid(V)) ; a__U62(X1,X2) >= U62(X1,X2) ; a__U61(tt,V) >= a__U62(a__isPalListKind(V),V) ; a__U61(X1,X2) >= U61(X1,X2) ; a__U63(tt) >= tt ; a__U63(X) >= U63(X) ; a__U72(tt,P) >= a__U73(a__isPal(P),P) ; a__U72(X1,X2) >= U72(X1,X2) ; a__U71(tt,I,P) >= a__U72(a__isPalListKind(I),P) ; a__U71(X1,X2,X3) >= U71(X1,X2,X3) ; a__U73(tt,P) >= a__U74(a__isPalListKind(P)) ; a__U73(X1,X2) >= U73(X1,X2) ; a__isPal(nil) >= tt ; a__isPal(X) >= isPal(X) ; a__isPal(V) >= a__U81(a__isPalListKind(V),V) ; a__U74(tt) >= tt ; a__U74(X) >= U74(X) ; a__U82(tt,V) >= a__U83(a__isNePal(V)) ; a__U82(X1,X2) >= U82(X1,X2) ; a__U81(tt,V) >= a__U82(a__isPalListKind(V),V) ; a__U81(X1,X2) >= U81(X1,X2) ; a__U83(tt) >= tt ; a__U83(X) >= U83(X) ; a__isNePal(__(I,__(P,I))) >= a__U71(a__isQid(I),I,P) ; a__isNePal(X) >= isNePal(X) ; a__isNePal(V) >= a__U61(a__isPalListKind(V),V) ; a__U92(tt) >= tt ; a__U92(X) >= U92(X) ; a__U91(tt,V2) >= a__U92(a__isPalListKind(V2)) ; a__U91(X1,X2) >= U91(X1,X2) ; Marked_a____(__(X,Y),Z) >= Marked_a____(mark(X),a____(mark(Y),mark(Z))) ; } + Disjunctions:{ { Marked_a____(__(X,Y),Z) > Marked_a____(mark(X),a____(mark(Y),mark(Z))) ; } } === TIMER virtual : 10.000000 === Entering poly_solver Starting Sat solver initialization Calling Sat solver... === STOPING TIMER virtual === === TIMER real : 10.000000 === === STOPING TIMER real === Sat solver returned Sat solver result read === STOPING TIMER real === === STOPING TIMER virtual === constraint: a____(__(X,Y),Z) >= a____(mark(X),a____(mark(Y),mark(Z))) constraint: a____(nil,X) >= mark(X) constraint: a____(X,nil) >= mark(X) constraint: a____(X1,X2) >= __(X1,X2) constraint: mark(__(X1,X2)) >= a____(mark(X1),mark(X2)) constraint: mark(nil) >= nil constraint: mark(tt) >= tt constraint: mark(a) >= a constraint: mark(e) >= e constraint: mark(i) >= i constraint: mark(o) >= o constraint: mark(u) >= u constraint: mark(U11(X1,X2)) >= a__U11(mark(X1),X2) constraint: mark(U12(X1,X2)) >= a__U12(mark(X1),X2) constraint: mark(isPalListKind(X)) >= a__isPalListKind(X) constraint: mark(U13(X)) >= a__U13(mark(X)) constraint: mark(isNeList(X)) >= a__isNeList(X) constraint: mark(U21(X1,X2,X3)) >= a__U21(mark(X1),X2,X3) constraint: mark(U22(X1,X2,X3)) >= a__U22(mark(X1),X2,X3) constraint: mark(U23(X1,X2,X3)) >= a__U23(mark(X1),X2,X3) constraint: mark(U24(X1,X2,X3)) >= a__U24(mark(X1),X2,X3) constraint: mark(U25(X1,X2)) >= a__U25(mark(X1),X2) constraint: mark(isList(X)) >= a__isList(X) constraint: mark(U26(X)) >= a__U26(mark(X)) constraint: mark(U31(X1,X2)) >= a__U31(mark(X1),X2) constraint: mark(U32(X1,X2)) >= a__U32(mark(X1),X2) constraint: mark(U33(X)) >= a__U33(mark(X)) constraint: mark(isQid(X)) >= a__isQid(X) constraint: mark(U41(X1,X2,X3)) >= a__U41(mark(X1),X2,X3) constraint: mark(U42(X1,X2,X3)) >= a__U42(mark(X1),X2,X3) constraint: mark(U43(X1,X2,X3)) >= a__U43(mark(X1),X2,X3) constraint: mark(U44(X1,X2,X3)) >= a__U44(mark(X1),X2,X3) constraint: mark(U45(X1,X2)) >= a__U45(mark(X1),X2) constraint: mark(U46(X)) >= a__U46(mark(X)) constraint: mark(U51(X1,X2,X3)) >= a__U51(mark(X1),X2,X3) constraint: mark(U52(X1,X2,X3)) >= a__U52(mark(X1),X2,X3) constraint: mark(U53(X1,X2,X3)) >= a__U53(mark(X1),X2,X3) constraint: mark(U54(X1,X2,X3)) >= a__U54(mark(X1),X2,X3) constraint: mark(U55(X1,X2)) >= a__U55(mark(X1),X2) constraint: mark(U56(X)) >= a__U56(mark(X)) constraint: mark(U61(X1,X2)) >= a__U61(mark(X1),X2) constraint: mark(U62(X1,X2)) >= a__U62(mark(X1),X2) constraint: mark(U63(X)) >= a__U63(mark(X)) constraint: mark(U71(X1,X2,X3)) >= a__U71(mark(X1),X2,X3) constraint: mark(U72(X1,X2)) >= a__U72(mark(X1),X2) constraint: mark(U73(X1,X2)) >= a__U73(mark(X1),X2) constraint: mark(isPal(X)) >= a__isPal(X) constraint: mark(U74(X)) >= a__U74(mark(X)) constraint: mark(U81(X1,X2)) >= a__U81(mark(X1),X2) constraint: mark(U82(X1,X2)) >= a__U82(mark(X1),X2) constraint: mark(U83(X)) >= a__U83(mark(X)) constraint: mark(isNePal(X)) >= a__isNePal(X) constraint: mark(U91(X1,X2)) >= a__U91(mark(X1),X2) constraint: mark(U92(X)) >= a__U92(mark(X)) constraint: a__U12(tt,V) >= a__U13(a__isNeList(V)) constraint: a__U12(X1,X2) >= U12(X1,X2) constraint: a__isPalListKind(__(V1,V2)) >= a__U91(a__isPalListKind(V1),V2) constraint: a__isPalListKind(nil) >= tt constraint: a__isPalListKind(a) >= tt constraint: a__isPalListKind(e) >= tt constraint: a__isPalListKind(i) >= tt constraint: a__isPalListKind(o) >= tt constraint: a__isPalListKind(u) >= tt constraint: a__isPalListKind(X) >= isPalListKind(X) constraint: a__U11(tt,V) >= a__U12(a__isPalListKind(V),V) constraint: a__U11(X1,X2) >= U11(X1,X2) constraint: a__U13(tt) >= tt constraint: a__U13(X) >= U13(X) constraint: a__isNeList(__(V1,V2)) >= a__U41(a__isPalListKind(V1),V1,V2) constraint: a__isNeList(__(V1,V2)) >= a__U51(a__isPalListKind(V1),V1,V2) constraint: a__isNeList(X) >= isNeList(X) constraint: a__isNeList(V) >= a__U31(a__isPalListKind(V),V) constraint: a__U22(tt,V1,V2) >= a__U23(a__isPalListKind(V2),V1,V2) constraint: a__U22(X1,X2,X3) >= U22(X1,X2,X3) constraint: a__U21(tt,V1,V2) >= a__U22(a__isPalListKind(V1),V1,V2) constraint: a__U21(X1,X2,X3) >= U21(X1,X2,X3) constraint: a__U23(tt,V1,V2) >= a__U24(a__isPalListKind(V2),V1,V2) constraint: a__U23(X1,X2,X3) >= U23(X1,X2,X3) constraint: a__U24(tt,V1,V2) >= a__U25(a__isList(V1),V2) constraint: a__U24(X1,X2,X3) >= U24(X1,X2,X3) constraint: a__U25(tt,V2) >= a__U26(a__isList(V2)) constraint: a__U25(X1,X2) >= U25(X1,X2) constraint: a__isList(__(V1,V2)) >= a__U21(a__isPalListKind(V1),V1,V2) constraint: a__isList(nil) >= tt constraint: a__isList(X) >= isList(X) constraint: a__isList(V) >= a__U11(a__isPalListKind(V),V) constraint: a__U26(tt) >= tt constraint: a__U26(X) >= U26(X) constraint: a__U32(tt,V) >= a__U33(a__isQid(V)) constraint: a__U32(X1,X2) >= U32(X1,X2) constraint: a__U31(tt,V) >= a__U32(a__isPalListKind(V),V) constraint: a__U31(X1,X2) >= U31(X1,X2) constraint: a__U33(tt) >= tt constraint: a__U33(X) >= U33(X) constraint: a__isQid(a) >= tt constraint: a__isQid(e) >= tt constraint: a__isQid(i) >= tt constraint: a__isQid(o) >= tt constraint: a__isQid(u) >= tt constraint: a__isQid(X) >= isQid(X) constraint: a__U42(tt,V1,V2) >= a__U43(a__isPalListKind(V2),V1,V2) constraint: a__U42(X1,X2,X3) >= U42(X1,X2,X3) constraint: a__U41(tt,V1,V2) >= a__U42(a__isPalListKind(V1),V1,V2) constraint: a__U41(X1,X2,X3) >= U41(X1,X2,X3) constraint: a__U43(tt,V1,V2) >= a__U44(a__isPalListKind(V2),V1,V2) constraint: a__U43(X1,X2,X3) >= U43(X1,X2,X3) constraint: a__U44(tt,V1,V2) >= a__U45(a__isList(V1),V2) constraint: a__U44(X1,X2,X3) >= U44(X1,X2,X3) constraint: a__U45(tt,V2) >= a__U46(a__isNeList(V2)) constraint: a__U45(X1,X2) >= U45(X1,X2) constraint: a__U46(tt) >= tt constraint: a__U46(X) >= U46(X) constraint: a__U52(tt,V1,V2) >= a__U53(a__isPalListKind(V2),V1,V2) constraint: a__U52(X1,X2,X3) >= U52(X1,X2,X3) constraint: a__U51(tt,V1,V2) >= a__U52(a__isPalListKind(V1),V1,V2) constraint: a__U51(X1,X2,X3) >= U51(X1,X2,X3) constraint: a__U53(tt,V1,V2) >= a__U54(a__isPalListKind(V2),V1,V2) constraint: a__U53(X1,X2,X3) >= U53(X1,X2,X3) constraint: a__U54(tt,V1,V2) >= a__U55(a__isNeList(V1),V2) constraint: a__U54(X1,X2,X3) >= U54(X1,X2,X3) constraint: a__U55(tt,V2) >= a__U56(a__isList(V2)) constraint: a__U55(X1,X2) >= U55(X1,X2) constraint: a__U56(tt) >= tt constraint: a__U56(X) >= U56(X) constraint: a__U62(tt,V) >= a__U63(a__isQid(V)) constraint: a__U62(X1,X2) >= U62(X1,X2) constraint: a__U61(tt,V) >= a__U62(a__isPalListKind(V),V) constraint: a__U61(X1,X2) >= U61(X1,X2) constraint: a__U63(tt) >= tt constraint: a__U63(X) >= U63(X) constraint: a__U72(tt,P) >= a__U73(a__isPal(P),P) constraint: a__U72(X1,X2) >= U72(X1,X2) constraint: a__U71(tt,I,P) >= a__U72(a__isPalListKind(I),P) constraint: a__U71(X1,X2,X3) >= U71(X1,X2,X3) constraint: a__U73(tt,P) >= a__U74(a__isPalListKind(P)) constraint: a__U73(X1,X2) >= U73(X1,X2) constraint: a__isPal(nil) >= tt constraint: a__isPal(X) >= isPal(X) constraint: a__isPal(V) >= a__U81(a__isPalListKind(V),V) constraint: a__U74(tt) >= tt constraint: a__U74(X) >= U74(X) constraint: a__U82(tt,V) >= a__U83(a__isNePal(V)) constraint: a__U82(X1,X2) >= U82(X1,X2) constraint: a__U81(tt,V) >= a__U82(a__isPalListKind(V),V) constraint: a__U81(X1,X2) >= U81(X1,X2) constraint: a__U83(tt) >= tt constraint: a__U83(X) >= U83(X) constraint: a__isNePal(__(I,__(P,I))) >= a__U71(a__isQid(I),I,P) constraint: a__isNePal(X) >= isNePal(X) constraint: a__isNePal(V) >= a__U61(a__isPalListKind(V),V) constraint: a__U92(tt) >= tt constraint: a__U92(X) >= U92(X) constraint: a__U91(tt,V2) >= a__U92(a__isPalListKind(V2)) constraint: a__U91(X1,X2) >= U91(X1,X2) constraint: Marked_a____(__(X,Y),Z) >= Marked_a____(mark(X), a____(mark(Y),mark(Z))) APPLY CRITERIA (Subterm criterion) ST: Marked_mark -> 1 APPLY CRITERIA (Graph splitting) Found 0 components: APPLY CRITERIA (Graph splitting) Found 0 components: APPLY CRITERIA (Graph splitting) Found 0 components: APPLY CRITERIA (Graph splitting) Found 0 components: APPLY CRITERIA (Graph splitting) Found 0 components: SOLVED { TRS termination of: [1] a____(__(X,Y),Z) -> a____(mark(X),a____(mark(Y),mark(Z))) [2] a____(X,nil) -> mark(X) [3] a____(nil,X) -> mark(X) [4] a__U11(tt,V) -> a__U12(a__isPalListKind(V),V) [5] a__U12(tt,V) -> a__U13(a__isNeList(V)) [6] a__U13(tt) -> tt [7] a__U21(tt,V1,V2) -> a__U22(a__isPalListKind(V1),V1,V2) [8] a__U22(tt,V1,V2) -> a__U23(a__isPalListKind(V2),V1,V2) [9] a__U23(tt,V1,V2) -> a__U24(a__isPalListKind(V2),V1,V2) [10] a__U24(tt,V1,V2) -> a__U25(a__isList(V1),V2) [11] a__U25(tt,V2) -> a__U26(a__isList(V2)) [12] a__U26(tt) -> tt [13] a__U31(tt,V) -> a__U32(a__isPalListKind(V),V) [14] a__U32(tt,V) -> a__U33(a__isQid(V)) [15] a__U33(tt) -> tt [16] a__U41(tt,V1,V2) -> a__U42(a__isPalListKind(V1),V1,V2) [17] a__U42(tt,V1,V2) -> a__U43(a__isPalListKind(V2),V1,V2) [18] a__U43(tt,V1,V2) -> a__U44(a__isPalListKind(V2),V1,V2) [19] a__U44(tt,V1,V2) -> a__U45(a__isList(V1),V2) [20] a__U45(tt,V2) -> a__U46(a__isNeList(V2)) [21] a__U46(tt) -> tt [22] a__U51(tt,V1,V2) -> a__U52(a__isPalListKind(V1),V1,V2) [23] a__U52(tt,V1,V2) -> a__U53(a__isPalListKind(V2),V1,V2) [24] a__U53(tt,V1,V2) -> a__U54(a__isPalListKind(V2),V1,V2) [25] a__U54(tt,V1,V2) -> a__U55(a__isNeList(V1),V2) [26] a__U55(tt,V2) -> a__U56(a__isList(V2)) [27] a__U56(tt) -> tt [28] a__U61(tt,V) -> a__U62(a__isPalListKind(V),V) [29] a__U62(tt,V) -> a__U63(a__isQid(V)) [30] a__U63(tt) -> tt [31] a__U71(tt,I,P) -> a__U72(a__isPalListKind(I),P) [32] a__U72(tt,P) -> a__U73(a__isPal(P),P) [33] a__U73(tt,P) -> a__U74(a__isPalListKind(P)) [34] a__U74(tt) -> tt [35] a__U81(tt,V) -> a__U82(a__isPalListKind(V),V) [36] a__U82(tt,V) -> a__U83(a__isNePal(V)) [37] a__U83(tt) -> tt [38] a__U91(tt,V2) -> a__U92(a__isPalListKind(V2)) [39] a__U92(tt) -> tt [40] a__isList(V) -> a__U11(a__isPalListKind(V),V) [41] a__isList(nil) -> tt [42] a__isList(__(V1,V2)) -> a__U21(a__isPalListKind(V1),V1,V2) [43] a__isNeList(V) -> a__U31(a__isPalListKind(V),V) [44] a__isNeList(__(V1,V2)) -> a__U41(a__isPalListKind(V1),V1,V2) [45] a__isNeList(__(V1,V2)) -> a__U51(a__isPalListKind(V1),V1,V2) [46] a__isNePal(V) -> a__U61(a__isPalListKind(V),V) [47] a__isNePal(__(I,__(P,I))) -> a__U71(a__isQid(I),I,P) [48] a__isPal(V) -> a__U81(a__isPalListKind(V),V) [49] a__isPal(nil) -> tt [50] a__isPalListKind(a) -> tt [51] a__isPalListKind(e) -> tt [52] a__isPalListKind(i) -> tt [53] a__isPalListKind(nil) -> tt [54] a__isPalListKind(o) -> tt [55] a__isPalListKind(u) -> tt [56] a__isPalListKind(__(V1,V2)) -> a__U91(a__isPalListKind(V1),V2) [57] a__isQid(a) -> tt [58] a__isQid(e) -> tt [59] a__isQid(i) -> tt [60] a__isQid(o) -> tt [61] a__isQid(u) -> tt [62] mark(__(X1,X2)) -> a____(mark(X1),mark(X2)) [63] mark(U11(X1,X2)) -> a__U11(mark(X1),X2) [64] mark(U12(X1,X2)) -> a__U12(mark(X1),X2) [65] mark(isPalListKind(X)) -> a__isPalListKind(X) [66] mark(U13(X)) -> a__U13(mark(X)) [67] mark(isNeList(X)) -> a__isNeList(X) [68] mark(U21(X1,X2,X3)) -> a__U21(mark(X1),X2,X3) [69] mark(U22(X1,X2,X3)) -> a__U22(mark(X1),X2,X3) [70] mark(U23(X1,X2,X3)) -> a__U23(mark(X1),X2,X3) [71] mark(U24(X1,X2,X3)) -> a__U24(mark(X1),X2,X3) [72] mark(U25(X1,X2)) -> a__U25(mark(X1),X2) [73] mark(isList(X)) -> a__isList(X) [74] mark(U26(X)) -> a__U26(mark(X)) [75] mark(U31(X1,X2)) -> a__U31(mark(X1),X2) [76] mark(U32(X1,X2)) -> a__U32(mark(X1),X2) [77] mark(U33(X)) -> a__U33(mark(X)) [78] mark(isQid(X)) -> a__isQid(X) [79] mark(U41(X1,X2,X3)) -> a__U41(mark(X1),X2,X3) [80] mark(U42(X1,X2,X3)) -> a__U42(mark(X1),X2,X3) [81] mark(U43(X1,X2,X3)) -> a__U43(mark(X1),X2,X3) [82] mark(U44(X1,X2,X3)) -> a__U44(mark(X1),X2,X3) [83] mark(U45(X1,X2)) -> a__U45(mark(X1),X2) [84] mark(U46(X)) -> a__U46(mark(X)) [85] mark(U51(X1,X2,X3)) -> a__U51(mark(X1),X2,X3) [86] mark(U52(X1,X2,X3)) -> a__U52(mark(X1),X2,X3) [87] mark(U53(X1,X2,X3)) -> a__U53(mark(X1),X2,X3) [88] mark(U54(X1,X2,X3)) -> a__U54(mark(X1),X2,X3) [89] mark(U55(X1,X2)) -> a__U55(mark(X1),X2) [90] mark(U56(X)) -> a__U56(mark(X)) [91] mark(U61(X1,X2)) -> a__U61(mark(X1),X2) [92] mark(U62(X1,X2)) -> a__U62(mark(X1),X2) [93] mark(U63(X)) -> a__U63(mark(X)) [94] mark(U71(X1,X2,X3)) -> a__U71(mark(X1),X2,X3) [95] mark(U72(X1,X2)) -> a__U72(mark(X1),X2) [96] mark(U73(X1,X2)) -> a__U73(mark(X1),X2) [97] mark(isPal(X)) -> a__isPal(X) [98] mark(U74(X)) -> a__U74(mark(X)) [99] mark(U81(X1,X2)) -> a__U81(mark(X1),X2) [100] mark(U82(X1,X2)) -> a__U82(mark(X1),X2) [101] mark(U83(X)) -> a__U83(mark(X)) [102] mark(isNePal(X)) -> a__isNePal(X) [103] mark(U91(X1,X2)) -> a__U91(mark(X1),X2) [104] mark(U92(X)) -> a__U92(mark(X)) [105] mark(nil) -> nil [106] mark(tt) -> tt [107] mark(a) -> a [108] mark(e) -> e [109] mark(i) -> i [110] mark(o) -> o [111] mark(u) -> u [112] a____(X1,X2) -> __(X1,X2) [113] a__U11(X1,X2) -> U11(X1,X2) [114] a__U12(X1,X2) -> U12(X1,X2) [115] a__isPalListKind(X) -> isPalListKind(X) [116] a__U13(X) -> U13(X) [117] a__isNeList(X) -> isNeList(X) [118] a__U21(X1,X2,X3) -> U21(X1,X2,X3) [119] a__U22(X1,X2,X3) -> U22(X1,X2,X3) [120] a__U23(X1,X2,X3) -> U23(X1,X2,X3) [121] a__U24(X1,X2,X3) -> U24(X1,X2,X3) [122] a__U25(X1,X2) -> U25(X1,X2) [123] a__isList(X) -> isList(X) [124] a__U26(X) -> U26(X) [125] a__U31(X1,X2) -> U31(X1,X2) [126] a__U32(X1,X2) -> U32(X1,X2) [127] a__U33(X) -> U33(X) [128] a__isQid(X) -> isQid(X) [129] a__U41(X1,X2,X3) -> U41(X1,X2,X3) [130] a__U42(X1,X2,X3) -> U42(X1,X2,X3) [131] a__U43(X1,X2,X3) -> U43(X1,X2,X3) [132] a__U44(X1,X2,X3) -> U44(X1,X2,X3) [133] a__U45(X1,X2) -> U45(X1,X2) [134] a__U46(X) -> U46(X) [135] a__U51(X1,X2,X3) -> U51(X1,X2,X3) [136] a__U52(X1,X2,X3) -> U52(X1,X2,X3) [137] a__U53(X1,X2,X3) -> U53(X1,X2,X3) [138] a__U54(X1,X2,X3) -> U54(X1,X2,X3) [139] a__U55(X1,X2) -> U55(X1,X2) [140] a__U56(X) -> U56(X) [141] a__U61(X1,X2) -> U61(X1,X2) [142] a__U62(X1,X2) -> U62(X1,X2) [143] a__U63(X) -> U63(X) [144] a__U71(X1,X2,X3) -> U71(X1,X2,X3) [145] a__U72(X1,X2) -> U72(X1,X2) [146] a__U73(X1,X2) -> U73(X1,X2) [147] a__isPal(X) -> isPal(X) [148] a__U74(X) -> U74(X) [149] a__U81(X1,X2) -> U81(X1,X2) [150] a__U82(X1,X2) -> U82(X1,X2) [151] a__U83(X) -> U83(X) [152] a__isNePal(X) -> isNePal(X) [153] a__U91(X1,X2) -> U91(X1,X2) [154] a__U92(X) -> U92(X) , CRITERION: MDP [ { DP termination of: , CRITERION: SG [ { DP termination of: , CRITERION: CG using polynomial interpretation = [ a____ ] (X0,X1) = 1*X1 + 1*X0; [ U31 ] (X0,X1) = 1*X0; [ a__U56 ] (X0) = 2*X0; [ a__U26 ] (X0) = 2*X0; [ U61 ] (X0,X1) = 2*X0; [ e ] () = 0; [ a__U13 ] (X0) = 1*X0; [ Marked_a____ ] (X0,X1) = 2*X1 + 2*X0; [ U45 ] (X0,X1) = 2*X0; [ a__U74 ] (X0) = 1*X0; [ a__U44 ] (X0,X1,X2) = 2*X0; [ U81 ] (X0,X1) = 1*X0; [ isNeList ] (X0) = 0; [ a__U12 ] (X0,X1) = 1*X0; [ U41 ] (X0,X1,X2) = 2*X0; [ a__U72 ] (X0,X1) = 1*X0; [ a__isQid ] (X0) = 0; [ U72 ] (X0,X1) = 1*X0; [ U11 ] (X0,X1) = 2*X0; [ a__U23 ] (X0,X1,X2) = 1*X0; [ U53 ] (X0,X1,X2) = 1*X0; [ a__isNePal ] (X0) = 0; [ a__U51 ] (X0,X1,X2) = 2*X0; [ U91 ] (X0,X1) = 1*X0; [ U24 ] (X0,X1,X2) = 1*X0; [ __ ] (X0,X1) = 1*X1 + 1*X0; [ U33 ] (X0) = 1*X0; [ a__U61 ] (X0,X1) = 2*X0; [ a__U31 ] (X0,X1) = 1*X0; [ U63 ] (X0) = 1*X0; [ o ] () = 0; [ a__U22 ] (X0,X1,X2) = 1*X0; [ U51 ] (X0,X1,X2) = 2*X0; [ a__U81 ] (X0,X1) = 1*X0; [ a__U46 ] (X0) = 1*X0; [ U83 ] (X0) = 1*X0; [ U22 ] (X0,X1,X2) = 1*X0; [ a__U11 ] (X0,X1) = 2*X0; [ U43 ] (X0,X1,X2) = 2*X0; [ a__U73 ] (X0,X1) = 2*X0; [ a__U41 ] (X0,X1,X2) = 2*X0; [ isPal ] (X0) = 0; [ isPalListKind ] (X0) = 0; [ a__U25 ] (X0,X1) = 1*X0; [ U55 ] (X0,X1) = 1*X0; [ a__U91 ] (X0,X1) = 1*X0; [ a__U54 ] (X0,X1,X2) = 1*X0; [ isList ] (X0) = 0; [ mark ] (X0) = 1*X0; [ U32 ] (X0,X1) = 1*X0; [ a__U62 ] (X0,X1) = 1*X0; [ a__U32 ] (X0,X1) = 1*X0; [ U62 ] (X0,X1) = 1*X0; [ i ] () = 0; [ a__isNeList ] (X0) = 0; [ Marked_mark ] (X0) = 2*X0; [ U46 ] (X0) = 1*X0; [ a__U82 ] (X0,X1) = 2*X0; [ a__U45 ] (X0,X1) = 2*X0; [ U82 ] (X0,X1) = 2*X0; [ U21 ] (X0,X1,X2) = 2*X0; [ a__isPalListKind ] (X0) = 0; [ U42 ] (X0,X1,X2) = 1*X0; [ a__U71 ] (X0,X1,X2) = 1*X0; [ a__U42 ] (X0,X1,X2) = 1*X0; [ U73 ] (X0,X1) = 2*X0; [ U12 ] (X0,X1) = 1*X0; [ a__U24 ] (X0,X1,X2) = 1*X0; [ U54 ] (X0,X1,X2) = 1*X0; [ a__U92 ] (X0) = 2*X0; [ a__U53 ] (X0,X1,X2) = 1*X0; [ U92 ] (X0) = 2*X0; [ U25 ] (X0,X1) = 1*X0; [ nil ] () = 2; [ isQid ] (X0) = 0; [ a__U63 ] (X0) = 1*X0; [ a__U33 ] (X0) = 1*X0; [ U71 ] (X0,X1,X2) = 1*X0; [ u ] () = 0; [ a__U21 ] (X0,X1,X2) = 2*X0; [ U52 ] (X0,X1,X2) = 1*X0; [ a__U83 ] (X0) = 1*X0; [ a__U52 ] (X0,X1,X2) = 1*X0; [ isNePal ] (X0) = 0; [ U23 ] (X0,X1,X2) = 1*X0; [ tt ] () = 0; [ U44 ] (X0,X1,X2) = 2*X0; [ a__isPal ] (X0) = 0; [ a__U43 ] (X0,X1,X2) = 2*X0; [ U74 ] (X0) = 1*X0; [ U13 ] (X0) = 1*X0; [ a__isList ] (X0) = 0; [ U56 ] (X0) = 2*X0; [ a ] () = 0; [ a__U55 ] (X0,X1) = 1*X0; [ U26 ] (X0) = 2*X0; removing [ { DP termination of: , CRITERION: SG [ { DP termination of: , CRITERION: CG using polynomial interpretation = [ a____ ] (X0,X1) = 1*X1 + 1*X0 + 2; [ U31 ] (X0,X1) = 1*X0; [ a__U56 ] (X0) = 2*X0; [ a__U26 ] (X0) = 2*X0; [ U61 ] (X0,X1) = 1*X0; [ e ] () = 0; [ a__U13 ] (X0) = 2*X0; [ Marked_a____ ] (X0,X1) = 1*X1 + 1*X0; [ U45 ] (X0,X1) = 1*X0; [ a__U74 ] (X0) = 1*X0; [ a__U44 ] (X0,X1,X2) = 2*X0; [ U81 ] (X0,X1) = 2*X0; [ isNeList ] (X0) = 0; [ a__U12 ] (X0,X1) = 1*X0; [ U41 ] (X0,X1,X2) = 1*X0; [ a__U72 ] (X0,X1) = 2*X0; [ a__isQid ] (X0) = 0; [ U72 ] (X0,X1) = 2*X0; [ U11 ] (X0,X1) = 1*X0; [ a__U23 ] (X0,X1,X2) = 1*X0; [ U53 ] (X0,X1,X2) = 1*X0; [ a__isNePal ] (X0) = 0; [ a__U51 ] (X0,X1,X2) = 1*X0; [ U91 ] (X0,X1) = 2*X0; [ U24 ] (X0,X1,X2) = 1*X0; [ __ ] (X0,X1) = 1*X1 + 1*X0 + 2; [ U33 ] (X0) = 1*X0; [ a__U61 ] (X0,X1) = 1*X0; [ a__U31 ] (X0,X1) = 1*X0; [ U63 ] (X0) = 2*X0; [ o ] () = 0; [ a__U22 ] (X0,X1,X2) = 1*X0; [ U51 ] (X0,X1,X2) = 1*X0; [ a__U81 ] (X0,X1) = 2*X0; [ a__U46 ] (X0) = 1*X0; [ U83 ] (X0) = 1*X0; [ U22 ] (X0,X1,X2) = 1*X0; [ a__U11 ] (X0,X1) = 1*X0; [ U43 ] (X0,X1,X2) = 2*X0; [ a__U73 ] (X0,X1) = 1*X0; [ a__U41 ] (X0,X1,X2) = 1*X0; [ isPal ] (X0) = 0; [ isPalListKind ] (X0) = 0; [ a__U25 ] (X0,X1) = 2*X0; [ U55 ] (X0,X1) = 2*X0; [ a__U91 ] (X0,X1) = 2*X0; [ a__U54 ] (X0,X1,X2) = 1*X0; [ isList ] (X0) = 0; [ mark ] (X0) = 1*X0; [ U32 ] (X0,X1) = 2*X0; [ a__U62 ] (X0,X1) = 1*X0; [ a__U32 ] (X0,X1) = 2*X0; [ U62 ] (X0,X1) = 1*X0; [ i ] () = 0; [ a__isNeList ] (X0) = 0; [ Marked_mark ] (X0) = 1*X0; [ U46 ] (X0) = 1*X0; [ a__U82 ] (X0,X1) = 1*X0; [ a__U45 ] (X0,X1) = 1*X0; [ U82 ] (X0,X1) = 1*X0; [ U21 ] (X0,X1,X2) = 1*X0; [ a__isPalListKind ] (X0) = 0; [ U42 ] (X0,X1,X2) = 1*X0; [ a__U71 ] (X0,X1,X2) = 2*X0; [ a__U42 ] (X0,X1,X2) = 1*X0; [ U73 ] (X0,X1) = 1*X0; [ U12 ] (X0,X1) = 1*X0; [ a__U24 ] (X0,X1,X2) = 1*X0; [ U54 ] (X0,X1,X2) = 1*X0; [ a__U92 ] (X0) = 1*X0; [ a__U53 ] (X0,X1,X2) = 1*X0; [ U92 ] (X0) = 1*X0; [ U25 ] (X0,X1) = 2*X0; [ nil ] () = 0; [ isQid ] (X0) = 0; [ a__U63 ] (X0) = 2*X0; [ a__U33 ] (X0) = 1*X0; [ U71 ] (X0,X1,X2) = 2*X0; [ u ] () = 0; [ a__U21 ] (X0,X1,X2) = 1*X0; [ U52 ] (X0,X1,X2) = 2*X0; [ a__U83 ] (X0) = 1*X0; [ a__U52 ] (X0,X1,X2) = 2*X0; [ isNePal ] (X0) = 0; [ U23 ] (X0,X1,X2) = 1*X0; [ tt ] () = 0; [ U44 ] (X0,X1,X2) = 2*X0; [ a__isPal ] (X0) = 0; [ a__U43 ] (X0,X1,X2) = 2*X0; [ U74 ] (X0) = 1*X0; [ U13 ] (X0) = 2*X0; [ a__isList ] (X0) = 0; [ U56 ] (X0) = 2*X0; [ a ] () = 0; [ a__U55 ] (X0,X1) = 2*X0; [ U26 ] (X0) = 2*X0; removing < Marked_a____(__(X,Y),Z),Marked_mark(Z)>< Marked_mark(__(X1,X2)),Marked_mark(X1)> [ { DP termination of: , CRITERION: SG [ { DP termination of: , CRITERION: ORD [ Solution found: polynomial interpretation = [ a____ ] (X0,X1) = 1 + 1*X0 + 1*X1 + 0; [ U31 ] (X0,X1) = 0; [ a__U56 ] (X0) = 0; [ a__U26 ] (X0) = 0; [ U61 ] (X0,X1) = 0; [ e ] () = 0; [ a__U13 ] (X0) = 0; [ Marked_a____ ] (X0,X1) = 1*X0 + 0; [ U45 ] (X0,X1) = 0; [ a__U74 ] (X0) = 0; [ a__U44 ] (X0,X1,X2) = 0; [ U81 ] (X0,X1) = 0; [ isNeList ] (X0) = 2*X0 + 0; [ a__U12 ] (X0,X1) = 0; [ U41 ] (X0,X1,X2) = 0; [ a__U72 ] (X0,X1) = 0; [ a__isQid ] (X0) = 0; [ U72 ] (X0,X1) = 0; [ U11 ] (X0,X1) = 0; [ a__U23 ] (X0,X1,X2) = 0; [ U53 ] (X0,X1,X2) = 0; [ a__isNePal ] (X0) = 2*X0 + 0; [ a__U51 ] (X0,X1,X2) = 0; [ U91 ] (X0,X1) = 2*X1 + 0; [ U24 ] (X0,X1,X2) = 0; [ __ ] (X0,X1) = 1 + 1*X0 + 1*X1 + 0; [ U33 ] (X0) = 0; [ a__U61 ] (X0,X1) = 0; [ a__U31 ] (X0,X1) = 0; [ U63 ] (X0) = 0; [ o ] () = 0; [ a__U22 ] (X0,X1,X2) = 0; [ U51 ] (X0,X1,X2) = 0; [ a__U81 ] (X0,X1) = 0; [ a__U46 ] (X0) = 0; [ U83 ] (X0) = 0; [ U22 ] (X0,X1,X2) = 0; [ a__U11 ] (X0,X1) = 0; [ U43 ] (X0,X1,X2) = 0; [ a__U73 ] (X0,X1) = 0; [ a__U41 ] (X0,X1,X2) = 0; [ isPal ] (X0) = 0; [ isPalListKind ] (X0) = 2*X0 + 0; [ a__U25 ] (X0,X1) = 0; [ U55 ] (X0,X1) = 0; [ a__U91 ] (X0,X1) = 2*X1 + 0; [ a__U54 ] (X0,X1,X2) = 0; [ isList ] (X0) = 0; [ mark ] (X0) = 1*X0 + 0; [ U32 ] (X0,X1) = 0; [ a__U62 ] (X0,X1) = 0; [ a__U32 ] (X0,X1) = 0; [ U62 ] (X0,X1) = 0; [ i ] () = 0; [ a__isNeList ] (X0) = 2*X0 + 0; [ U46 ] (X0) = 0; [ a__U82 ] (X0,X1) = 0; [ a__U45 ] (X0,X1) = 0; [ U82 ] (X0,X1) = 0; [ U21 ] (X0,X1,X2) = 0; [ a__isPalListKind ] (X0) = 2*X0 + 0; [ U42 ] (X0,X1,X2) = 0; [ a__U71 ] (X0,X1,X2) = 2*X1 + 2*X2 + 0; [ a__U42 ] (X0,X1,X2) = 0; [ U73 ] (X0,X1) = 0; [ U12 ] (X0,X1) = 0; [ a__U24 ] (X0,X1,X2) = 0; [ U54 ] (X0,X1,X2) = 0; [ a__U92 ] (X0) = 0; [ a__U53 ] (X0,X1,X2) = 0; [ U92 ] (X0) = 0; [ U25 ] (X0,X1) = 0; [ nil ] () = 0; [ isQid ] (X0) = 0; [ a__U63 ] (X0) = 0; [ a__U33 ] (X0) = 0; [ U71 ] (X0,X1,X2) = 2*X1 + 2*X2 + 0; [ u ] () = 0; [ a__U21 ] (X0,X1,X2) = 0; [ U52 ] (X0,X1,X2) = 0; [ a__U83 ] (X0) = 0; [ a__U52 ] (X0,X1,X2) = 0; [ isNePal ] (X0) = 2*X0 + 0; [ U23 ] (X0,X1,X2) = 0; [ tt ] () = 0; [ U44 ] (X0,X1,X2) = 0; [ a__isPal ] (X0) = 0; [ a__U43 ] (X0,X1,X2) = 0; [ U74 ] (X0) = 0; [ U13 ] (X0) = 0; [ a__isList ] (X0) = 0; [ U56 ] (X0) = 0; [ a ] () = 0; [ a__U55 ] (X0,X1) = 0; [ U26 ] (X0) = 0; ]} { DP termination of: , CRITERION: ST [ { DP termination of: , CRITERION: SG [ ]} ]} ]} ]} ]} ]} { DP termination of: , CRITERION: CG using polynomial interpretation = [ a____ ] (X0,X1) = 1*X1 + 2*X0 + 2; [ Marked_a__U23 ] (X0,X1,X2) = 1*X2 + 1*X1; [ U31 ] (X0,X1) = 0; [ a__U56 ] (X0) = 0; [ a__U26 ] (X0) = 0; [ U61 ] (X0,X1) = 0; [ e ] () = 0; [ Marked_a__U52 ] (X0,X1,X2) = 1*X2 + 1*X1 + 1; [ a__U13 ] (X0) = 0; [ U45 ] (X0,X1) = 0; [ a__U74 ] (X0) = 0; [ a__U44 ] (X0,X1,X2) = 0; [ U81 ] (X0,X1) = 0; [ isNeList ] (X0) = 0; [ a__U12 ] (X0,X1) = 0; [ U41 ] (X0,X1,X2) = 0; [ a__U72 ] (X0,X1) = 0; [ a__isQid ] (X0) = 0; [ U72 ] (X0,X1) = 0; [ U11 ] (X0,X1) = 0; [ Marked_a__U44 ] (X0,X1,X2) = 1*X2 + 1*X1; [ a__U23 ] (X0,X1,X2) = 0; [ U53 ] (X0,X1,X2) = 0; [ a__isNePal ] (X0) = 0; [ a__U51 ] (X0,X1,X2) = 0; [ U91 ] (X0,X1) = 0; [ U24 ] (X0,X1,X2) = 0; [ __ ] (X0,X1) = 1*X1 + 2*X0 + 2; [ Marked_a__U21 ] (X0,X1,X2) = 1*X2 + 1*X1; [ U33 ] (X0) = 0; [ a__U61 ] (X0,X1) = 0; [ a__U31 ] (X0,X1) = 0; [ U63 ] (X0) = 0; [ o ] () = 0; [ a__U22 ] (X0,X1,X2) = 0; [ U51 ] (X0,X1,X2) = 0; [ a__U81 ] (X0,X1) = 0; [ a__U46 ] (X0) = 0; [ U83 ] (X0) = 0; [ U22 ] (X0,X1,X2) = 0; [ a__U11 ] (X0,X1) = 0; [ Marked_a__U12 ] (X0,X1) = 1*X1; [ U43 ] (X0,X1,X2) = 0; [ a__U73 ] (X0,X1) = 0; [ a__U41 ] (X0,X1,X2) = 0; [ isPal ] (X0) = 0; [ isPalListKind ] (X0) = 0; [ Marked_a__U42 ] (X0,X1,X2) = 1*X2 + 1*X1 + 1; [ a__U25 ] (X0,X1) = 0; [ U55 ] (X0,X1) = 0; [ a__U91 ] (X0,X1) = 0; [ Marked_a__U54 ] (X0,X1,X2) = 1*X2 + 1*X1 + 1; [ a__U54 ] (X0,X1,X2) = 0; [ isList ] (X0) = 1*X0; [ Marked_a__U25 ] (X0,X1) = 1*X1; [ mark ] (X0) = 1*X0; [ Marked_a__U22 ] (X0,X1,X2) = 1*X2 + 1*X1; [ U32 ] (X0,X1) = 0; [ a__U62 ] (X0,X1) = 0; [ a__U32 ] (X0,X1) = 0; [ U62 ] (X0,X1) = 0; [ i ] () = 0; [ Marked_a__U51 ] (X0,X1,X2) = 1*X2 + 1*X1 + 1; [ a__isNeList ] (X0) = 0; [ U46 ] (X0) = 0; [ a__U82 ] (X0,X1) = 0; [ a__U45 ] (X0,X1) = 0; [ U82 ] (X0,X1) = 0; [ U21 ] (X0,X1,X2) = 2; [ a__isPalListKind ] (X0) = 0; [ U42 ] (X0,X1,X2) = 0; [ a__U71 ] (X0,X1,X2) = 0; [ a__U42 ] (X0,X1,X2) = 0; [ U73 ] (X0,X1) = 0; [ U12 ] (X0,X1) = 0; [ Marked_a__U43 ] (X0,X1,X2) = 1*X2 + 1*X1 + 1; [ a__U24 ] (X0,X1,X2) = 0; [ U54 ] (X0,X1,X2) = 0; [ a__U92 ] (X0) = 0; [ Marked_a__U55 ] (X0,X1) = 1*X1; [ a__U53 ] (X0,X1,X2) = 0; [ U92 ] (X0) = 0; [ U25 ] (X0,X1) = 0; [ Marked_a__isList ] (X0) = 1*X0; [ nil ] () = 0; [ Marked_a__isNeList ] (X0) = 1*X0; [ isQid ] (X0) = 0; [ a__U63 ] (X0) = 0; [ a__U33 ] (X0) = 0; [ U71 ] (X0,X1,X2) = 0; [ u ] () = 0; [ Marked_a__U45 ] (X0,X1) = 1*X1; [ a__U21 ] (X0,X1,X2) = 2; [ U52 ] (X0,X1,X2) = 0; [ a__U83 ] (X0) = 0; [ a__U52 ] (X0,X1,X2) = 0; [ isNePal ] (X0) = 0; [ U23 ] (X0,X1,X2) = 0; [ tt ] () = 0; [ Marked_a__U11 ] (X0,X1) = 1*X1; [ U44 ] (X0,X1,X2) = 0; [ a__isPal ] (X0) = 0; [ a__U43 ] (X0,X1,X2) = 0; [ U74 ] (X0) = 0; [ U13 ] (X0) = 0; [ Marked_a__U41 ] (X0,X1,X2) = 1*X2 + 1*X1 + 1; [ a__isList ] (X0) = 1*X0; [ U56 ] (X0) = 0; [ a ] () = 0; [ Marked_a__U53 ] (X0,X1,X2) = 1*X2 + 1*X1 + 1; [ a__U55 ] (X0,X1) = 0; [ U26 ] (X0) = 0; [ Marked_a__U24 ] (X0,X1,X2) = 1*X2 + 1*X1; removing < Marked_a__U54(tt,V1,V2),Marked_a__U55(a__isNeList(V1),V2)> [ { DP termination of: , CRITERION: SG [ ]} ]} { DP termination of: , CRITERION: ST [ { DP termination of: , CRITERION: SG [ ]} ]} { DP termination of: , CRITERION: ST [ { DP termination of: , CRITERION: SG [ ]} ]} ]} ]} Cime worked for 2.639781 seconds (real time) Cime Exit Status: 0