- : unit = () h : heuristic = - : unit = () APPLY CRITERIA (Marked dependency pairs) TRS termination of: [1] active(__(__(X,Y),Z)) -> mark(__(X,__(Y,Z))) [2] active(__(X,nil)) -> mark(X) [3] active(__(nil,X)) -> mark(X) [4] active(U11(tt)) -> mark(tt) [5] active(U21(tt,V2)) -> mark(U22(isList(V2))) [6] active(U22(tt)) -> mark(tt) [7] active(U31(tt)) -> mark(tt) [8] active(U41(tt,V2)) -> mark(U42(isNeList(V2))) [9] active(U42(tt)) -> mark(tt) [10] active(U51(tt,V2)) -> mark(U52(isList(V2))) [11] active(U52(tt)) -> mark(tt) [12] active(U61(tt)) -> mark(tt) [13] active(U71(tt,P)) -> mark(U72(isPal(P))) [14] active(U72(tt)) -> mark(tt) [15] active(U81(tt)) -> mark(tt) [16] active(isList(V)) -> mark(U11(isNeList(V))) [17] active(isList(nil)) -> mark(tt) [18] active(isList(__(V1,V2))) -> mark(U21(isList(V1),V2)) [19] active(isNeList(V)) -> mark(U31(isQid(V))) [20] active(isNeList(__(V1,V2))) -> mark(U41(isList(V1),V2)) [21] active(isNeList(__(V1,V2))) -> mark(U51(isNeList(V1),V2)) [22] active(isNePal(V)) -> mark(U61(isQid(V))) [23] active(isNePal(__(I,__(P,I)))) -> mark(U71(isQid(I),P)) [24] active(isPal(V)) -> mark(U81(isNePal(V))) [25] active(isPal(nil)) -> mark(tt) [26] active(isQid(a)) -> mark(tt) [27] active(isQid(e)) -> mark(tt) [28] active(isQid(i)) -> mark(tt) [29] active(isQid(o)) -> mark(tt) [30] active(isQid(u)) -> mark(tt) [31] mark(__(X1,X2)) -> active(__(mark(X1),mark(X2))) [32] mark(nil) -> active(nil) [33] mark(U11(X)) -> active(U11(mark(X))) [34] mark(tt) -> active(tt) [35] mark(U21(X1,X2)) -> active(U21(mark(X1),X2)) [36] mark(U22(X)) -> active(U22(mark(X))) [37] mark(isList(X)) -> active(isList(X)) [38] mark(U31(X)) -> active(U31(mark(X))) [39] mark(U41(X1,X2)) -> active(U41(mark(X1),X2)) [40] mark(U42(X)) -> active(U42(mark(X))) [41] mark(isNeList(X)) -> active(isNeList(X)) [42] mark(U51(X1,X2)) -> active(U51(mark(X1),X2)) [43] mark(U52(X)) -> active(U52(mark(X))) [44] mark(U61(X)) -> active(U61(mark(X))) [45] mark(U71(X1,X2)) -> active(U71(mark(X1),X2)) [46] mark(U72(X)) -> active(U72(mark(X))) [47] mark(isPal(X)) -> active(isPal(X)) [48] mark(U81(X)) -> active(U81(mark(X))) [49] mark(isQid(X)) -> active(isQid(X)) [50] mark(isNePal(X)) -> active(isNePal(X)) [51] mark(a) -> active(a) [52] mark(e) -> active(e) [53] mark(i) -> active(i) [54] mark(o) -> active(o) [55] mark(u) -> active(u) [56] __(mark(X1),X2) -> __(X1,X2) [57] __(X1,mark(X2)) -> __(X1,X2) [58] __(active(X1),X2) -> __(X1,X2) [59] __(X1,active(X2)) -> __(X1,X2) [60] U11(mark(X)) -> U11(X) [61] U11(active(X)) -> U11(X) [62] U21(mark(X1),X2) -> U21(X1,X2) [63] U21(X1,mark(X2)) -> U21(X1,X2) [64] U21(active(X1),X2) -> U21(X1,X2) [65] U21(X1,active(X2)) -> U21(X1,X2) [66] U22(mark(X)) -> U22(X) [67] U22(active(X)) -> U22(X) [68] isList(mark(X)) -> isList(X) [69] isList(active(X)) -> isList(X) [70] U31(mark(X)) -> U31(X) [71] U31(active(X)) -> U31(X) [72] U41(mark(X1),X2) -> U41(X1,X2) [73] U41(X1,mark(X2)) -> U41(X1,X2) [74] U41(active(X1),X2) -> U41(X1,X2) [75] U41(X1,active(X2)) -> U41(X1,X2) [76] U42(mark(X)) -> U42(X) [77] U42(active(X)) -> U42(X) [78] isNeList(mark(X)) -> isNeList(X) [79] isNeList(active(X)) -> isNeList(X) [80] U51(mark(X1),X2) -> U51(X1,X2) [81] U51(X1,mark(X2)) -> U51(X1,X2) [82] U51(active(X1),X2) -> U51(X1,X2) [83] U51(X1,active(X2)) -> U51(X1,X2) [84] U52(mark(X)) -> U52(X) [85] U52(active(X)) -> U52(X) [86] U61(mark(X)) -> U61(X) [87] U61(active(X)) -> U61(X) [88] U71(mark(X1),X2) -> U71(X1,X2) [89] U71(X1,mark(X2)) -> U71(X1,X2) [90] U71(active(X1),X2) -> U71(X1,X2) [91] U71(X1,active(X2)) -> U71(X1,X2) [92] U72(mark(X)) -> U72(X) [93] U72(active(X)) -> U72(X) [94] isPal(mark(X)) -> isPal(X) [95] isPal(active(X)) -> isPal(X) [96] U81(mark(X)) -> U81(X) [97] U81(active(X)) -> U81(X) [98] isQid(mark(X)) -> isQid(X) [99] isQid(active(X)) -> isQid(X) [100] isNePal(mark(X)) -> isNePal(X) [101] isNePal(active(X)) -> isNePal(X) Sub problem: guided: DP termination of: END GUIDED APPLY CRITERIA (Graph splitting) Found 19 components: { --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> } { --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> } { --> --> --> --> } { --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> } { --> --> --> --> } { --> --> --> --> } { --> --> --> --> } { --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> } { --> --> --> --> } { --> --> --> --> } { --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> } { --> --> --> --> } { --> --> --> --> } { --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> } { --> --> --> --> } { --> --> --> --> } { --> --> --> --> } { --> --> --> --> } { --> --> --> --> } APPLY CRITERIA (Choosing graph) Trying to solve the following constraints: { mark(__(X1,X2)) >= active(__(mark(X1),mark(X2))) ; mark(nil) >= active(nil) ; mark(tt) >= active(tt) ; mark(U11(X)) >= active(U11(mark(X))) ; mark(U22(X)) >= active(U22(mark(X))) ; mark(isList(X)) >= active(isList(X)) ; mark(U21(X1,X2)) >= active(U21(mark(X1),X2)) ; mark(U31(X)) >= active(U31(mark(X))) ; mark(U42(X)) >= active(U42(mark(X))) ; mark(isNeList(X)) >= active(isNeList(X)) ; mark(U41(X1,X2)) >= active(U41(mark(X1),X2)) ; mark(U52(X)) >= active(U52(mark(X))) ; mark(U51(X1,X2)) >= active(U51(mark(X1),X2)) ; mark(U61(X)) >= active(U61(mark(X))) ; mark(U72(X)) >= active(U72(mark(X))) ; mark(isPal(X)) >= active(isPal(X)) ; mark(U71(X1,X2)) >= active(U71(mark(X1),X2)) ; mark(U81(X)) >= active(U81(mark(X))) ; mark(isQid(X)) >= active(isQid(X)) ; mark(isNePal(X)) >= active(isNePal(X)) ; mark(a) >= active(a) ; mark(e) >= active(e) ; mark(i) >= active(i) ; mark(o) >= active(o) ; mark(u) >= active(u) ; __(mark(X1),X2) >= __(X1,X2) ; __(active(X1),X2) >= __(X1,X2) ; __(X1,mark(X2)) >= __(X1,X2) ; __(X1,active(X2)) >= __(X1,X2) ; active(__(__(X,Y),Z)) >= mark(__(X,__(Y,Z))) ; active(__(nil,X)) >= mark(X) ; active(__(X,nil)) >= mark(X) ; active(U11(tt)) >= mark(tt) ; active(U22(tt)) >= mark(tt) ; active(isList(__(V1,V2))) >= mark(U21(isList(V1),V2)) ; active(isList(nil)) >= mark(tt) ; active(isList(V)) >= mark(U11(isNeList(V))) ; active(U21(tt,V2)) >= mark(U22(isList(V2))) ; active(U31(tt)) >= mark(tt) ; active(U42(tt)) >= mark(tt) ; active(isNeList(__(V1,V2))) >= mark(U41(isList(V1),V2)) ; active(isNeList(__(V1,V2))) >= mark(U51(isNeList(V1),V2)) ; active(isNeList(V)) >= mark(U31(isQid(V))) ; active(U41(tt,V2)) >= mark(U42(isNeList(V2))) ; active(U52(tt)) >= mark(tt) ; active(U51(tt,V2)) >= mark(U52(isList(V2))) ; active(U61(tt)) >= mark(tt) ; active(U72(tt)) >= mark(tt) ; active(isPal(nil)) >= mark(tt) ; active(isPal(V)) >= mark(U81(isNePal(V))) ; active(U71(tt,P)) >= mark(U72(isPal(P))) ; active(U81(tt)) >= mark(tt) ; active(isQid(a)) >= mark(tt) ; active(isQid(e)) >= mark(tt) ; active(isQid(i)) >= mark(tt) ; active(isQid(o)) >= mark(tt) ; active(isQid(u)) >= mark(tt) ; active(isNePal(__(I,__(P,I)))) >= mark(U71(isQid(I),P)) ; active(isNePal(V)) >= mark(U61(isQid(V))) ; U11(mark(X)) >= U11(X) ; U11(active(X)) >= U11(X) ; U22(mark(X)) >= U22(X) ; U22(active(X)) >= U22(X) ; isList(mark(X)) >= isList(X) ; isList(active(X)) >= isList(X) ; U21(mark(X1),X2) >= U21(X1,X2) ; U21(active(X1),X2) >= U21(X1,X2) ; U21(X1,mark(X2)) >= U21(X1,X2) ; U21(X1,active(X2)) >= U21(X1,X2) ; U31(mark(X)) >= U31(X) ; U31(active(X)) >= U31(X) ; U42(mark(X)) >= U42(X) ; U42(active(X)) >= U42(X) ; isNeList(mark(X)) >= isNeList(X) ; isNeList(active(X)) >= isNeList(X) ; U41(mark(X1),X2) >= U41(X1,X2) ; U41(active(X1),X2) >= U41(X1,X2) ; U41(X1,mark(X2)) >= U41(X1,X2) ; U41(X1,active(X2)) >= U41(X1,X2) ; U52(mark(X)) >= U52(X) ; U52(active(X)) >= U52(X) ; U51(mark(X1),X2) >= U51(X1,X2) ; U51(active(X1),X2) >= U51(X1,X2) ; U51(X1,mark(X2)) >= U51(X1,X2) ; U51(X1,active(X2)) >= U51(X1,X2) ; U61(mark(X)) >= U61(X) ; U61(active(X)) >= U61(X) ; U72(mark(X)) >= U72(X) ; U72(active(X)) >= U72(X) ; isPal(mark(X)) >= isPal(X) ; isPal(active(X)) >= isPal(X) ; U71(mark(X1),X2) >= U71(X1,X2) ; U71(active(X1),X2) >= U71(X1,X2) ; U71(X1,mark(X2)) >= U71(X1,X2) ; U71(X1,active(X2)) >= U71(X1,X2) ; U81(mark(X)) >= U81(X) ; U81(active(X)) >= U81(X) ; isQid(mark(X)) >= isQid(X) ; isQid(active(X)) >= isQid(X) ; isNePal(mark(X)) >= isNePal(X) ; isNePal(active(X)) >= isNePal(X) ; Marked_mark(__(X1,X2)) >= Marked_mark(X1) ; Marked_mark(__(X1,X2)) >= Marked_mark(X2) ; Marked_mark(__(X1,X2)) >= Marked_active(__(mark(X1),mark(X2))) ; Marked_mark(U11(X)) >= Marked_mark(X) ; Marked_mark(U11(X)) >= Marked_active(U11(mark(X))) ; Marked_mark(U22(X)) >= Marked_mark(X) ; Marked_mark(U22(X)) >= Marked_active(U22(mark(X))) ; Marked_mark(isList(X)) >= Marked_active(isList(X)) ; Marked_mark(U21(X1,X2)) >= Marked_mark(X1) ; Marked_mark(U21(X1,X2)) >= Marked_active(U21(mark(X1),X2)) ; Marked_mark(U31(X)) >= Marked_mark(X) ; Marked_mark(U31(X)) >= Marked_active(U31(mark(X))) ; Marked_mark(U42(X)) >= Marked_mark(X) ; Marked_mark(U42(X)) >= Marked_active(U42(mark(X))) ; Marked_mark(isNeList(X)) >= Marked_active(isNeList(X)) ; Marked_mark(U41(X1,X2)) >= Marked_mark(X1) ; Marked_mark(U41(X1,X2)) >= Marked_active(U41(mark(X1),X2)) ; Marked_mark(U52(X)) >= Marked_mark(X) ; Marked_mark(U52(X)) >= Marked_active(U52(mark(X))) ; Marked_mark(U51(X1,X2)) >= Marked_mark(X1) ; Marked_mark(U51(X1,X2)) >= Marked_active(U51(mark(X1),X2)) ; Marked_mark(U61(X)) >= Marked_mark(X) ; Marked_mark(U61(X)) >= Marked_active(U61(mark(X))) ; Marked_mark(U72(X)) >= Marked_mark(X) ; Marked_mark(U72(X)) >= Marked_active(U72(mark(X))) ; Marked_mark(isPal(X)) >= Marked_active(isPal(X)) ; Marked_mark(U71(X1,X2)) >= Marked_mark(X1) ; Marked_mark(U71(X1,X2)) >= Marked_active(U71(mark(X1),X2)) ; Marked_mark(U81(X)) >= Marked_mark(X) ; Marked_mark(U81(X)) >= Marked_active(U81(mark(X))) ; Marked_mark(isQid(X)) >= Marked_active(isQid(X)) ; Marked_mark(isNePal(X)) >= Marked_active(isNePal(X)) ; Marked_active(__(__(X,Y),Z)) >= Marked_mark(__(X,__(Y,Z))) ; Marked_active(__(nil,X)) >= Marked_mark(X) ; Marked_active(__(X,nil)) >= Marked_mark(X) ; Marked_active(isList(__(V1,V2))) >= Marked_mark(U21(isList(V1),V2)) ; Marked_active(isList(V)) >= Marked_mark(U11(isNeList(V))) ; Marked_active(U21(tt,V2)) >= Marked_mark(U22(isList(V2))) ; Marked_active(isNeList(__(V1,V2))) >= Marked_mark(U41(isList(V1),V2)) ; Marked_active(isNeList(__(V1,V2))) >= Marked_mark(U51(isNeList(V1),V2)) ; Marked_active(isNeList(V)) >= Marked_mark(U31(isQid(V))) ; Marked_active(U41(tt,V2)) >= Marked_mark(U42(isNeList(V2))) ; Marked_active(U51(tt,V2)) >= Marked_mark(U52(isList(V2))) ; Marked_active(isPal(V)) >= Marked_mark(U81(isNePal(V))) ; Marked_active(U71(tt,P)) >= Marked_mark(U72(isPal(P))) ; Marked_active(isNePal(__(I,__(P,I)))) >= Marked_mark(U71(isQid(I),P)) ; Marked_active(isNePal(V)) >= Marked_mark(U61(isQid(V))) ; } + Disjunctions:{ { Marked_mark(__(X1,X2)) > Marked_mark(X1) ; } { Marked_mark(__(X1,X2)) > Marked_mark(X2) ; } { Marked_mark(__(X1,X2)) > Marked_active(__(mark(X1),mark(X2))) ; } { Marked_mark(U11(X)) > Marked_mark(X) ; } { Marked_mark(U11(X)) > Marked_active(U11(mark(X))) ; } { Marked_mark(U22(X)) > Marked_mark(X) ; } { Marked_mark(U22(X)) > Marked_active(U22(mark(X))) ; } { Marked_mark(isList(X)) > Marked_active(isList(X)) ; } { Marked_mark(U21(X1,X2)) > Marked_mark(X1) ; } { Marked_mark(U21(X1,X2)) > Marked_active(U21(mark(X1),X2)) ; } { Marked_mark(U31(X)) > Marked_mark(X) ; } { Marked_mark(U31(X)) > Marked_active(U31(mark(X))) ; } { Marked_mark(U42(X)) > Marked_mark(X) ; } { Marked_mark(U42(X)) > Marked_active(U42(mark(X))) ; } { Marked_mark(isNeList(X)) > Marked_active(isNeList(X)) ; } { Marked_mark(U41(X1,X2)) > Marked_mark(X1) ; } { Marked_mark(U41(X1,X2)) > Marked_active(U41(mark(X1),X2)) ; } { Marked_mark(U52(X)) > Marked_mark(X) ; } { Marked_mark(U52(X)) > Marked_active(U52(mark(X))) ; } { Marked_mark(U51(X1,X2)) > Marked_mark(X1) ; } { Marked_mark(U51(X1,X2)) > Marked_active(U51(mark(X1),X2)) ; } { Marked_mark(U61(X)) > Marked_mark(X) ; } { Marked_mark(U61(X)) > Marked_active(U61(mark(X))) ; } { Marked_mark(U72(X)) > Marked_mark(X) ; } { Marked_mark(U72(X)) > Marked_active(U72(mark(X))) ; } { Marked_mark(isPal(X)) > Marked_active(isPal(X)) ; } { Marked_mark(U71(X1,X2)) > Marked_mark(X1) ; } { Marked_mark(U71(X1,X2)) > Marked_active(U71(mark(X1),X2)) ; } { Marked_mark(U81(X)) > Marked_mark(X) ; } { Marked_mark(U81(X)) > Marked_active(U81(mark(X))) ; } { Marked_mark(isQid(X)) > Marked_active(isQid(X)) ; } { Marked_mark(isNePal(X)) > Marked_active(isNePal(X)) ; } { Marked_active(__(__(X,Y),Z)) > Marked_mark(__(X,__(Y,Z))) ; } { Marked_active(__(nil,X)) > Marked_mark(X) ; } { Marked_active(__(X,nil)) > Marked_mark(X) ; } { Marked_active(isList(__(V1,V2))) > Marked_mark(U21(isList(V1),V2)) ; } { Marked_active(isList(V)) > Marked_mark(U11(isNeList(V))) ; } { Marked_active(U21(tt,V2)) > Marked_mark(U22(isList(V2))) ; } { Marked_active(isNeList(__(V1,V2))) > Marked_mark(U41(isList(V1),V2)) ; } { Marked_active(isNeList(__(V1,V2))) > Marked_mark(U51(isNeList(V1),V2)) ; } { Marked_active(isNeList(V)) > Marked_mark(U31(isQid(V))) ; } { Marked_active(U41(tt,V2)) > Marked_mark(U42(isNeList(V2))) ; } { Marked_active(U51(tt,V2)) > Marked_mark(U52(isList(V2))) ; } { Marked_active(isPal(V)) > Marked_mark(U81(isNePal(V))) ; } { Marked_active(U71(tt,P)) > Marked_mark(U72(isPal(P))) ; } { Marked_active(isNePal(__(I,__(P,I)))) > Marked_mark(U71(isQid(I),P)) ; } { Marked_active(isNePal(V)) > Marked_mark(U61(isQid(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: mark(__(X1,X2)) >= active(__(mark(X1),mark(X2))) constraint: mark(nil) >= active(nil) constraint: mark(tt) >= active(tt) constraint: mark(U11(X)) >= active(U11(mark(X))) constraint: mark(U22(X)) >= active(U22(mark(X))) constraint: mark(isList(X)) >= active(isList(X)) constraint: mark(U21(X1,X2)) >= active(U21(mark(X1),X2)) constraint: mark(U31(X)) >= active(U31(mark(X))) constraint: mark(U42(X)) >= active(U42(mark(X))) constraint: mark(isNeList(X)) >= active(isNeList(X)) constraint: mark(U41(X1,X2)) >= active(U41(mark(X1),X2)) constraint: mark(U52(X)) >= active(U52(mark(X))) constraint: mark(U51(X1,X2)) >= active(U51(mark(X1),X2)) constraint: mark(U61(X)) >= active(U61(mark(X))) constraint: mark(U72(X)) >= active(U72(mark(X))) constraint: mark(isPal(X)) >= active(isPal(X)) constraint: mark(U71(X1,X2)) >= active(U71(mark(X1),X2)) constraint: mark(U81(X)) >= active(U81(mark(X))) constraint: mark(isQid(X)) >= active(isQid(X)) constraint: mark(isNePal(X)) >= active(isNePal(X)) constraint: mark(a) >= active(a) constraint: mark(e) >= active(e) constraint: mark(i) >= active(i) constraint: mark(o) >= active(o) constraint: mark(u) >= active(u) constraint: __(mark(X1),X2) >= __(X1,X2) constraint: __(active(X1),X2) >= __(X1,X2) constraint: __(X1,mark(X2)) >= __(X1,X2) constraint: __(X1,active(X2)) >= __(X1,X2) constraint: active(__(__(X,Y),Z)) >= mark(__(X,__(Y,Z))) constraint: active(__(nil,X)) >= mark(X) constraint: active(__(X,nil)) >= mark(X) constraint: active(U11(tt)) >= mark(tt) constraint: active(U22(tt)) >= mark(tt) constraint: active(isList(__(V1,V2))) >= mark(U21(isList(V1),V2)) constraint: active(isList(nil)) >= mark(tt) constraint: active(isList(V)) >= mark(U11(isNeList(V))) constraint: active(U21(tt,V2)) >= mark(U22(isList(V2))) constraint: active(U31(tt)) >= mark(tt) constraint: active(U42(tt)) >= mark(tt) constraint: active(isNeList(__(V1,V2))) >= mark(U41(isList(V1),V2)) constraint: active(isNeList(__(V1,V2))) >= mark(U51(isNeList(V1),V2)) constraint: active(isNeList(V)) >= mark(U31(isQid(V))) constraint: active(U41(tt,V2)) >= mark(U42(isNeList(V2))) constraint: active(U52(tt)) >= mark(tt) constraint: active(U51(tt,V2)) >= mark(U52(isList(V2))) constraint: active(U61(tt)) >= mark(tt) constraint: active(U72(tt)) >= mark(tt) constraint: active(isPal(nil)) >= mark(tt) constraint: active(isPal(V)) >= mark(U81(isNePal(V))) constraint: active(U71(tt,P)) >= mark(U72(isPal(P))) constraint: active(U81(tt)) >= mark(tt) constraint: active(isQid(a)) >= mark(tt) constraint: active(isQid(e)) >= mark(tt) constraint: active(isQid(i)) >= mark(tt) constraint: active(isQid(o)) >= mark(tt) constraint: active(isQid(u)) >= mark(tt) constraint: active(isNePal(__(I,__(P,I)))) >= mark(U71(isQid(I),P)) constraint: active(isNePal(V)) >= mark(U61(isQid(V))) constraint: U11(mark(X)) >= U11(X) constraint: U11(active(X)) >= U11(X) constraint: U22(mark(X)) >= U22(X) constraint: U22(active(X)) >= U22(X) constraint: isList(mark(X)) >= isList(X) constraint: isList(active(X)) >= isList(X) constraint: U21(mark(X1),X2) >= U21(X1,X2) constraint: U21(active(X1),X2) >= U21(X1,X2) constraint: U21(X1,mark(X2)) >= U21(X1,X2) constraint: U21(X1,active(X2)) >= U21(X1,X2) constraint: U31(mark(X)) >= U31(X) constraint: U31(active(X)) >= U31(X) constraint: U42(mark(X)) >= U42(X) constraint: U42(active(X)) >= U42(X) constraint: isNeList(mark(X)) >= isNeList(X) constraint: isNeList(active(X)) >= isNeList(X) constraint: U41(mark(X1),X2) >= U41(X1,X2) constraint: U41(active(X1),X2) >= U41(X1,X2) constraint: U41(X1,mark(X2)) >= U41(X1,X2) constraint: U41(X1,active(X2)) >= U41(X1,X2) constraint: U52(mark(X)) >= U52(X) constraint: U52(active(X)) >= U52(X) constraint: U51(mark(X1),X2) >= U51(X1,X2) constraint: U51(active(X1),X2) >= U51(X1,X2) constraint: U51(X1,mark(X2)) >= U51(X1,X2) constraint: U51(X1,active(X2)) >= U51(X1,X2) constraint: U61(mark(X)) >= U61(X) constraint: U61(active(X)) >= U61(X) constraint: U72(mark(X)) >= U72(X) constraint: U72(active(X)) >= U72(X) constraint: isPal(mark(X)) >= isPal(X) constraint: isPal(active(X)) >= isPal(X) constraint: U71(mark(X1),X2) >= U71(X1,X2) constraint: U71(active(X1),X2) >= U71(X1,X2) constraint: U71(X1,mark(X2)) >= U71(X1,X2) constraint: U71(X1,active(X2)) >= U71(X1,X2) constraint: U81(mark(X)) >= U81(X) constraint: U81(active(X)) >= U81(X) constraint: isQid(mark(X)) >= isQid(X) constraint: isQid(active(X)) >= isQid(X) constraint: isNePal(mark(X)) >= isNePal(X) constraint: isNePal(active(X)) >= isNePal(X) constraint: Marked_mark(__(X1,X2)) >= Marked_mark(X1) constraint: Marked_mark(__(X1,X2)) >= Marked_mark(X2) constraint: Marked_mark(__(X1,X2)) >= Marked_active(__(mark(X1),mark(X2))) constraint: Marked_mark(U11(X)) >= Marked_mark(X) constraint: Marked_mark(U11(X)) >= Marked_active(U11(mark(X))) constraint: Marked_mark(U22(X)) >= Marked_mark(X) constraint: Marked_mark(U22(X)) >= Marked_active(U22(mark(X))) constraint: Marked_mark(isList(X)) >= Marked_active(isList(X)) constraint: Marked_mark(U21(X1,X2)) >= Marked_mark(X1) constraint: Marked_mark(U21(X1,X2)) >= Marked_active(U21(mark(X1),X2)) constraint: Marked_mark(U31(X)) >= Marked_mark(X) constraint: Marked_mark(U31(X)) >= Marked_active(U31(mark(X))) constraint: Marked_mark(U42(X)) >= Marked_mark(X) constraint: Marked_mark(U42(X)) >= Marked_active(U42(mark(X))) constraint: Marked_mark(isNeList(X)) >= Marked_active(isNeList(X)) constraint: Marked_mark(U41(X1,X2)) >= Marked_mark(X1) constraint: Marked_mark(U41(X1,X2)) >= Marked_active(U41(mark(X1),X2)) constraint: Marked_mark(U52(X)) >= Marked_mark(X) constraint: Marked_mark(U52(X)) >= Marked_active(U52(mark(X))) constraint: Marked_mark(U51(X1,X2)) >= Marked_mark(X1) constraint: Marked_mark(U51(X1,X2)) >= Marked_active(U51(mark(X1),X2)) constraint: Marked_mark(U61(X)) >= Marked_mark(X) constraint: Marked_mark(U61(X)) >= Marked_active(U61(mark(X))) constraint: Marked_mark(U72(X)) >= Marked_mark(X) constraint: Marked_mark(U72(X)) >= Marked_active(U72(mark(X))) constraint: Marked_mark(isPal(X)) >= Marked_active(isPal(X)) constraint: Marked_mark(U71(X1,X2)) >= Marked_mark(X1) constraint: Marked_mark(U71(X1,X2)) >= Marked_active(U71(mark(X1),X2)) constraint: Marked_mark(U81(X)) >= Marked_mark(X) constraint: Marked_mark(U81(X)) >= Marked_active(U81(mark(X))) constraint: Marked_mark(isQid(X)) >= Marked_active(isQid(X)) constraint: Marked_mark(isNePal(X)) >= Marked_active(isNePal(X)) constraint: Marked_active(__(__(X,Y),Z)) >= Marked_mark(__(X,__(Y,Z))) constraint: Marked_active(__(nil,X)) >= Marked_mark(X) constraint: Marked_active(__(X,nil)) >= Marked_mark(X) constraint: Marked_active(isList(__(V1,V2))) >= Marked_mark(U21(isList(V1),V2)) constraint: Marked_active(isList(V)) >= Marked_mark(U11(isNeList(V))) constraint: Marked_active(U21(tt,V2)) >= Marked_mark(U22(isList(V2))) constraint: Marked_active(isNeList(__(V1,V2))) >= Marked_mark(U41(isList(V1), V2)) constraint: Marked_active(isNeList(__(V1,V2))) >= Marked_mark(U51(isNeList(V1), V2)) constraint: Marked_active(isNeList(V)) >= Marked_mark(U31(isQid(V))) constraint: Marked_active(U41(tt,V2)) >= Marked_mark(U42(isNeList(V2))) constraint: Marked_active(U51(tt,V2)) >= Marked_mark(U52(isList(V2))) constraint: Marked_active(isPal(V)) >= Marked_mark(U81(isNePal(V))) constraint: Marked_active(U71(tt,P)) >= Marked_mark(U72(isPal(P))) constraint: Marked_active(isNePal(__(I,__(P,I)))) >= Marked_mark(U71( isQid(I), P)) constraint: Marked_active(isNePal(V)) >= Marked_mark(U61(isQid(V))) APPLY CRITERIA (Choosing graph) Trying to solve the following constraints: { mark(__(X1,X2)) >= active(__(mark(X1),mark(X2))) ; mark(nil) >= active(nil) ; mark(tt) >= active(tt) ; mark(U11(X)) >= active(U11(mark(X))) ; mark(U22(X)) >= active(U22(mark(X))) ; mark(isList(X)) >= active(isList(X)) ; mark(U21(X1,X2)) >= active(U21(mark(X1),X2)) ; mark(U31(X)) >= active(U31(mark(X))) ; mark(U42(X)) >= active(U42(mark(X))) ; mark(isNeList(X)) >= active(isNeList(X)) ; mark(U41(X1,X2)) >= active(U41(mark(X1),X2)) ; mark(U52(X)) >= active(U52(mark(X))) ; mark(U51(X1,X2)) >= active(U51(mark(X1),X2)) ; mark(U61(X)) >= active(U61(mark(X))) ; mark(U72(X)) >= active(U72(mark(X))) ; mark(isPal(X)) >= active(isPal(X)) ; mark(U71(X1,X2)) >= active(U71(mark(X1),X2)) ; mark(U81(X)) >= active(U81(mark(X))) ; mark(isQid(X)) >= active(isQid(X)) ; mark(isNePal(X)) >= active(isNePal(X)) ; mark(a) >= active(a) ; mark(e) >= active(e) ; mark(i) >= active(i) ; mark(o) >= active(o) ; mark(u) >= active(u) ; __(mark(X1),X2) >= __(X1,X2) ; __(active(X1),X2) >= __(X1,X2) ; __(X1,mark(X2)) >= __(X1,X2) ; __(X1,active(X2)) >= __(X1,X2) ; active(__(__(X,Y),Z)) >= mark(__(X,__(Y,Z))) ; active(__(nil,X)) >= mark(X) ; active(__(X,nil)) >= mark(X) ; active(U11(tt)) >= mark(tt) ; active(U22(tt)) >= mark(tt) ; active(isList(__(V1,V2))) >= mark(U21(isList(V1),V2)) ; active(isList(nil)) >= mark(tt) ; active(isList(V)) >= mark(U11(isNeList(V))) ; active(U21(tt,V2)) >= mark(U22(isList(V2))) ; active(U31(tt)) >= mark(tt) ; active(U42(tt)) >= mark(tt) ; active(isNeList(__(V1,V2))) >= mark(U41(isList(V1),V2)) ; active(isNeList(__(V1,V2))) >= mark(U51(isNeList(V1),V2)) ; active(isNeList(V)) >= mark(U31(isQid(V))) ; active(U41(tt,V2)) >= mark(U42(isNeList(V2))) ; active(U52(tt)) >= mark(tt) ; active(U51(tt,V2)) >= mark(U52(isList(V2))) ; active(U61(tt)) >= mark(tt) ; active(U72(tt)) >= mark(tt) ; active(isPal(nil)) >= mark(tt) ; active(isPal(V)) >= mark(U81(isNePal(V))) ; active(U71(tt,P)) >= mark(U72(isPal(P))) ; active(U81(tt)) >= mark(tt) ; active(isQid(a)) >= mark(tt) ; active(isQid(e)) >= mark(tt) ; active(isQid(i)) >= mark(tt) ; active(isQid(o)) >= mark(tt) ; active(isQid(u)) >= mark(tt) ; active(isNePal(__(I,__(P,I)))) >= mark(U71(isQid(I),P)) ; active(isNePal(V)) >= mark(U61(isQid(V))) ; U11(mark(X)) >= U11(X) ; U11(active(X)) >= U11(X) ; U22(mark(X)) >= U22(X) ; U22(active(X)) >= U22(X) ; isList(mark(X)) >= isList(X) ; isList(active(X)) >= isList(X) ; U21(mark(X1),X2) >= U21(X1,X2) ; U21(active(X1),X2) >= U21(X1,X2) ; U21(X1,mark(X2)) >= U21(X1,X2) ; U21(X1,active(X2)) >= U21(X1,X2) ; U31(mark(X)) >= U31(X) ; U31(active(X)) >= U31(X) ; U42(mark(X)) >= U42(X) ; U42(active(X)) >= U42(X) ; isNeList(mark(X)) >= isNeList(X) ; isNeList(active(X)) >= isNeList(X) ; U41(mark(X1),X2) >= U41(X1,X2) ; U41(active(X1),X2) >= U41(X1,X2) ; U41(X1,mark(X2)) >= U41(X1,X2) ; U41(X1,active(X2)) >= U41(X1,X2) ; U52(mark(X)) >= U52(X) ; U52(active(X)) >= U52(X) ; U51(mark(X1),X2) >= U51(X1,X2) ; U51(active(X1),X2) >= U51(X1,X2) ; U51(X1,mark(X2)) >= U51(X1,X2) ; U51(X1,active(X2)) >= U51(X1,X2) ; U61(mark(X)) >= U61(X) ; U61(active(X)) >= U61(X) ; U72(mark(X)) >= U72(X) ; U72(active(X)) >= U72(X) ; isPal(mark(X)) >= isPal(X) ; isPal(active(X)) >= isPal(X) ; U71(mark(X1),X2) >= U71(X1,X2) ; U71(active(X1),X2) >= U71(X1,X2) ; U71(X1,mark(X2)) >= U71(X1,X2) ; U71(X1,active(X2)) >= U71(X1,X2) ; U81(mark(X)) >= U81(X) ; U81(active(X)) >= U81(X) ; isQid(mark(X)) >= isQid(X) ; isQid(active(X)) >= isQid(X) ; isNePal(mark(X)) >= isNePal(X) ; isNePal(active(X)) >= isNePal(X) ; Marked___(mark(X1),X2) >= Marked___(X1,X2) ; Marked___(active(X1),X2) >= Marked___(X1,X2) ; Marked___(X1,mark(X2)) >= Marked___(X1,X2) ; Marked___(X1,active(X2)) >= Marked___(X1,X2) ; } + Disjunctions:{ { Marked___(mark(X1),X2) > Marked___(X1,X2) ; } { Marked___(active(X1),X2) > Marked___(X1,X2) ; } { Marked___(X1,mark(X2)) > Marked___(X1,X2) ; } { Marked___(X1,active(X2)) > Marked___(X1,X2) ; } } === 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 === STOPING TIMER real === === STOPING TIMER virtual === No solution found for these parameters. Entering rpo_solver === TIMER virtual : 25.000000 === Search parameters: AFS type: 2 ; time limit: 25.. === STOPING TIMER virtual === Time out for these parameters. === TIMER virtual : 15.000000 === Entering poly_solver Starting Sat solver initialization Calling Sat solver... === STOPING TIMER virtual === === TIMER real : 15.000000 === === STOPING TIMER real === Sat solver returned === STOPING TIMER real === === STOPING TIMER virtual === No solution found for these parameters. === TIMER virtual : 50.000000 === trying sub matrices of size: 1 Matrix interpretation constraints generated. Search parameters: LINEAR MATRIX 3x3 (strict=1x1) ; time limit: 50.. Termination constraints generated. Starting Sat solver initialization Calling Sat solver... === STOPING TIMER virtual === === TIMER real : 50.000000 === === STOPING TIMER real === Sat solver returned === STOPING TIMER real === === STOPING TIMER virtual === No solution found for these parameters. No solution found for these constraints. APPLY CRITERIA (ID_CRIT) NOT SOLVED No proof found Cime worked for 41.276377 seconds (real time) Cime Exit Status: 0