- : unit = () - : 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] active(__(X1,X2)) -> __(active(X1),X2) [32] active(__(X1,X2)) -> __(X1,active(X2)) [33] active(U11(X)) -> U11(active(X)) [34] active(U21(X1,X2)) -> U21(active(X1),X2) [35] active(U22(X)) -> U22(active(X)) [36] active(U31(X)) -> U31(active(X)) [37] active(U41(X1,X2)) -> U41(active(X1),X2) [38] active(U42(X)) -> U42(active(X)) [39] active(U51(X1,X2)) -> U51(active(X1),X2) [40] active(U52(X)) -> U52(active(X)) [41] active(U61(X)) -> U61(active(X)) [42] active(U71(X1,X2)) -> U71(active(X1),X2) [43] active(U72(X)) -> U72(active(X)) [44] active(U81(X)) -> U81(active(X)) [45] __(mark(X1),X2) -> mark(__(X1,X2)) [46] __(X1,mark(X2)) -> mark(__(X1,X2)) [47] U11(mark(X)) -> mark(U11(X)) [48] U21(mark(X1),X2) -> mark(U21(X1,X2)) [49] U22(mark(X)) -> mark(U22(X)) [50] U31(mark(X)) -> mark(U31(X)) [51] U41(mark(X1),X2) -> mark(U41(X1,X2)) [52] U42(mark(X)) -> mark(U42(X)) [53] U51(mark(X1),X2) -> mark(U51(X1,X2)) [54] U52(mark(X)) -> mark(U52(X)) [55] U61(mark(X)) -> mark(U61(X)) [56] U71(mark(X1),X2) -> mark(U71(X1,X2)) [57] U72(mark(X)) -> mark(U72(X)) [58] U81(mark(X)) -> mark(U81(X)) [59] proper(__(X1,X2)) -> __(proper(X1),proper(X2)) [60] proper(nil) -> ok(nil) [61] proper(U11(X)) -> U11(proper(X)) [62] proper(tt) -> ok(tt) [63] proper(U21(X1,X2)) -> U21(proper(X1),proper(X2)) [64] proper(U22(X)) -> U22(proper(X)) [65] proper(isList(X)) -> isList(proper(X)) [66] proper(U31(X)) -> U31(proper(X)) [67] proper(U41(X1,X2)) -> U41(proper(X1),proper(X2)) [68] proper(U42(X)) -> U42(proper(X)) [69] proper(isNeList(X)) -> isNeList(proper(X)) [70] proper(U51(X1,X2)) -> U51(proper(X1),proper(X2)) [71] proper(U52(X)) -> U52(proper(X)) [72] proper(U61(X)) -> U61(proper(X)) [73] proper(U71(X1,X2)) -> U71(proper(X1),proper(X2)) [74] proper(U72(X)) -> U72(proper(X)) [75] proper(isPal(X)) -> isPal(proper(X)) [76] proper(U81(X)) -> U81(proper(X)) [77] proper(isQid(X)) -> isQid(proper(X)) [78] proper(isNePal(X)) -> isNePal(proper(X)) [79] proper(a) -> ok(a) [80] proper(e) -> ok(e) [81] proper(i) -> ok(i) [82] proper(o) -> ok(o) [83] proper(u) -> ok(u) [84] __(ok(X1),ok(X2)) -> ok(__(X1,X2)) [85] U11(ok(X)) -> ok(U11(X)) [86] U21(ok(X1),ok(X2)) -> ok(U21(X1,X2)) [87] U22(ok(X)) -> ok(U22(X)) [88] isList(ok(X)) -> ok(isList(X)) [89] U31(ok(X)) -> ok(U31(X)) [90] U41(ok(X1),ok(X2)) -> ok(U41(X1,X2)) [91] U42(ok(X)) -> ok(U42(X)) [92] isNeList(ok(X)) -> ok(isNeList(X)) [93] U51(ok(X1),ok(X2)) -> ok(U51(X1,X2)) [94] U52(ok(X)) -> ok(U52(X)) [95] U61(ok(X)) -> ok(U61(X)) [96] U71(ok(X1),ok(X2)) -> ok(U71(X1,X2)) [97] U72(ok(X)) -> ok(U72(X)) [98] isPal(ok(X)) -> ok(isPal(X)) [99] U81(ok(X)) -> ok(U81(X)) [100] isQid(ok(X)) -> ok(isQid(X)) [101] isNePal(ok(X)) -> ok(isNePal(X)) [102] top(mark(X)) -> top(proper(X)) [103] top(ok(X)) -> top(active(X)) Sub problem: guided: DP termination of: END GUIDED APPLY CRITERIA (Graph splitting) Found 21 components: { --> --> --> --> } { --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> } { --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> } { --> } { --> } { --> } { --> } { --> } { --> --> --> --> --> --> --> --> --> } { --> --> --> --> } { --> --> --> --> } { --> --> --> --> } { --> --> --> --> } { --> --> --> --> } { --> --> --> --> } { --> --> --> --> } { --> --> --> --> } { --> --> --> --> } { --> --> --> --> } { --> --> --> --> } { --> --> --> --> } APPLY CRITERIA (Subterm criterion) APPLY CRITERIA (Choosing graph) Trying to solve the following constraints: { __(mark(X1),X2) >= mark(__(X1,X2)) ; __(ok(X1),ok(X2)) >= ok(__(X1,X2)) ; __(X1,mark(X2)) >= mark(__(X1,X2)) ; active(__(__(X,Y),Z)) >= mark(__(X,__(Y,Z))) ; active(__(nil,X)) >= mark(X) ; active(__(X,nil)) >= mark(X) ; active(__(X1,X2)) >= __(active(X1),X2) ; active(__(X1,X2)) >= __(X1,active(X2)) ; active(U11(tt)) >= mark(tt) ; active(U11(X)) >= U11(active(X)) ; active(U22(tt)) >= mark(tt) ; active(U22(X)) >= U22(active(X)) ; 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(U21(X1,X2)) >= U21(active(X1),X2) ; active(U31(tt)) >= mark(tt) ; active(U31(X)) >= U31(active(X)) ; active(U42(tt)) >= mark(tt) ; active(U42(X)) >= U42(active(X)) ; 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(U41(X1,X2)) >= U41(active(X1),X2) ; active(U52(tt)) >= mark(tt) ; active(U52(X)) >= U52(active(X)) ; active(U51(tt,V2)) >= mark(U52(isList(V2))) ; active(U51(X1,X2)) >= U51(active(X1),X2) ; active(U61(tt)) >= mark(tt) ; active(U61(X)) >= U61(active(X)) ; active(U72(tt)) >= mark(tt) ; active(U72(X)) >= U72(active(X)) ; active(isPal(nil)) >= mark(tt) ; active(isPal(V)) >= mark(U81(isNePal(V))) ; active(U71(tt,P)) >= mark(U72(isPal(P))) ; active(U71(X1,X2)) >= U71(active(X1),X2) ; active(U81(tt)) >= mark(tt) ; active(U81(X)) >= U81(active(X)) ; 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)) >= mark(U11(X)) ; U11(ok(X)) >= ok(U11(X)) ; U22(mark(X)) >= mark(U22(X)) ; U22(ok(X)) >= ok(U22(X)) ; isList(ok(X)) >= ok(isList(X)) ; U21(mark(X1),X2) >= mark(U21(X1,X2)) ; U21(ok(X1),ok(X2)) >= ok(U21(X1,X2)) ; U31(mark(X)) >= mark(U31(X)) ; U31(ok(X)) >= ok(U31(X)) ; U42(mark(X)) >= mark(U42(X)) ; U42(ok(X)) >= ok(U42(X)) ; isNeList(ok(X)) >= ok(isNeList(X)) ; U41(mark(X1),X2) >= mark(U41(X1,X2)) ; U41(ok(X1),ok(X2)) >= ok(U41(X1,X2)) ; U52(mark(X)) >= mark(U52(X)) ; U52(ok(X)) >= ok(U52(X)) ; U51(mark(X1),X2) >= mark(U51(X1,X2)) ; U51(ok(X1),ok(X2)) >= ok(U51(X1,X2)) ; U61(mark(X)) >= mark(U61(X)) ; U61(ok(X)) >= ok(U61(X)) ; U72(mark(X)) >= mark(U72(X)) ; U72(ok(X)) >= ok(U72(X)) ; isPal(ok(X)) >= ok(isPal(X)) ; U71(mark(X1),X2) >= mark(U71(X1,X2)) ; U71(ok(X1),ok(X2)) >= ok(U71(X1,X2)) ; U81(mark(X)) >= mark(U81(X)) ; U81(ok(X)) >= ok(U81(X)) ; isQid(ok(X)) >= ok(isQid(X)) ; isNePal(ok(X)) >= ok(isNePal(X)) ; proper(__(X1,X2)) >= __(proper(X1),proper(X2)) ; proper(nil) >= ok(nil) ; proper(tt) >= ok(tt) ; proper(U11(X)) >= U11(proper(X)) ; proper(U22(X)) >= U22(proper(X)) ; proper(isList(X)) >= isList(proper(X)) ; proper(U21(X1,X2)) >= U21(proper(X1),proper(X2)) ; proper(U31(X)) >= U31(proper(X)) ; proper(U42(X)) >= U42(proper(X)) ; proper(isNeList(X)) >= isNeList(proper(X)) ; proper(U41(X1,X2)) >= U41(proper(X1),proper(X2)) ; proper(U52(X)) >= U52(proper(X)) ; proper(U51(X1,X2)) >= U51(proper(X1),proper(X2)) ; proper(U61(X)) >= U61(proper(X)) ; proper(U72(X)) >= U72(proper(X)) ; proper(isPal(X)) >= isPal(proper(X)) ; proper(U71(X1,X2)) >= U71(proper(X1),proper(X2)) ; proper(U81(X)) >= U81(proper(X)) ; proper(isQid(X)) >= isQid(proper(X)) ; proper(isNePal(X)) >= isNePal(proper(X)) ; proper(a) >= ok(a) ; proper(e) >= ok(e) ; proper(i) >= ok(i) ; proper(o) >= ok(o) ; proper(u) >= ok(u) ; top(mark(X)) >= top(proper(X)) ; top(ok(X)) >= top(active(X)) ; Marked_top(mark(X)) >= Marked_top(proper(X)) ; Marked_top(ok(X)) >= Marked_top(active(X)) ; } + Disjunctions:{ { Marked_top(mark(X)) > Marked_top(proper(X)) ; } { Marked_top(ok(X)) > Marked_top(active(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: __(mark(X1),X2) >= mark(__(X1,X2)) constraint: __(ok(X1),ok(X2)) >= ok(__(X1,X2)) constraint: __(X1,mark(X2)) >= mark(__(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(__(X1,X2)) >= __(active(X1),X2) constraint: active(__(X1,X2)) >= __(X1,active(X2)) constraint: active(U11(tt)) >= mark(tt) constraint: active(U11(X)) >= U11(active(X)) constraint: active(U22(tt)) >= mark(tt) constraint: active(U22(X)) >= U22(active(X)) 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(U21(X1,X2)) >= U21(active(X1),X2) constraint: active(U31(tt)) >= mark(tt) constraint: active(U31(X)) >= U31(active(X)) constraint: active(U42(tt)) >= mark(tt) constraint: active(U42(X)) >= U42(active(X)) 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(U41(X1,X2)) >= U41(active(X1),X2) constraint: active(U52(tt)) >= mark(tt) constraint: active(U52(X)) >= U52(active(X)) constraint: active(U51(tt,V2)) >= mark(U52(isList(V2))) constraint: active(U51(X1,X2)) >= U51(active(X1),X2) constraint: active(U61(tt)) >= mark(tt) constraint: active(U61(X)) >= U61(active(X)) constraint: active(U72(tt)) >= mark(tt) constraint: active(U72(X)) >= U72(active(X)) 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(U71(X1,X2)) >= U71(active(X1),X2) constraint: active(U81(tt)) >= mark(tt) constraint: active(U81(X)) >= U81(active(X)) 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)) >= mark(U11(X)) constraint: U11(ok(X)) >= ok(U11(X)) constraint: U22(mark(X)) >= mark(U22(X)) constraint: U22(ok(X)) >= ok(U22(X)) constraint: isList(ok(X)) >= ok(isList(X)) constraint: U21(mark(X1),X2) >= mark(U21(X1,X2)) constraint: U21(ok(X1),ok(X2)) >= ok(U21(X1,X2)) constraint: U31(mark(X)) >= mark(U31(X)) constraint: U31(ok(X)) >= ok(U31(X)) constraint: U42(mark(X)) >= mark(U42(X)) constraint: U42(ok(X)) >= ok(U42(X)) constraint: isNeList(ok(X)) >= ok(isNeList(X)) constraint: U41(mark(X1),X2) >= mark(U41(X1,X2)) constraint: U41(ok(X1),ok(X2)) >= ok(U41(X1,X2)) constraint: U52(mark(X)) >= mark(U52(X)) constraint: U52(ok(X)) >= ok(U52(X)) constraint: U51(mark(X1),X2) >= mark(U51(X1,X2)) constraint: U51(ok(X1),ok(X2)) >= ok(U51(X1,X2)) constraint: U61(mark(X)) >= mark(U61(X)) constraint: U61(ok(X)) >= ok(U61(X)) constraint: U72(mark(X)) >= mark(U72(X)) constraint: U72(ok(X)) >= ok(U72(X)) constraint: isPal(ok(X)) >= ok(isPal(X)) constraint: U71(mark(X1),X2) >= mark(U71(X1,X2)) constraint: U71(ok(X1),ok(X2)) >= ok(U71(X1,X2)) constraint: U81(mark(X)) >= mark(U81(X)) constraint: U81(ok(X)) >= ok(U81(X)) constraint: isQid(ok(X)) >= ok(isQid(X)) constraint: isNePal(ok(X)) >= ok(isNePal(X)) constraint: proper(__(X1,X2)) >= __(proper(X1),proper(X2)) constraint: proper(nil) >= ok(nil) constraint: proper(tt) >= ok(tt) constraint: proper(U11(X)) >= U11(proper(X)) constraint: proper(U22(X)) >= U22(proper(X)) constraint: proper(isList(X)) >= isList(proper(X)) constraint: proper(U21(X1,X2)) >= U21(proper(X1),proper(X2)) constraint: proper(U31(X)) >= U31(proper(X)) constraint: proper(U42(X)) >= U42(proper(X)) constraint: proper(isNeList(X)) >= isNeList(proper(X)) constraint: proper(U41(X1,X2)) >= U41(proper(X1),proper(X2)) constraint: proper(U52(X)) >= U52(proper(X)) constraint: proper(U51(X1,X2)) >= U51(proper(X1),proper(X2)) constraint: proper(U61(X)) >= U61(proper(X)) constraint: proper(U72(X)) >= U72(proper(X)) constraint: proper(isPal(X)) >= isPal(proper(X)) constraint: proper(U71(X1,X2)) >= U71(proper(X1),proper(X2)) constraint: proper(U81(X)) >= U81(proper(X)) constraint: proper(isQid(X)) >= isQid(proper(X)) constraint: proper(isNePal(X)) >= isNePal(proper(X)) constraint: proper(a) >= ok(a) constraint: proper(e) >= ok(e) constraint: proper(i) >= ok(i) constraint: proper(o) >= ok(o) constraint: proper(u) >= ok(u) constraint: top(mark(X)) >= top(proper(X)) constraint: top(ok(X)) >= top(active(X)) constraint: Marked_top(mark(X)) >= Marked_top(proper(X)) constraint: Marked_top(ok(X)) >= Marked_top(active(X)) APPLY CRITERIA (Subterm criterion) ST: Marked_proper -> 1 APPLY CRITERIA (Subterm criterion) ST: Marked_active -> 1 APPLY CRITERIA (Subterm criterion) ST: Marked_isPal -> 1 APPLY CRITERIA (Subterm criterion) ST: Marked_isList -> 1 APPLY CRITERIA (Subterm criterion) ST: Marked_isNeList -> 1 APPLY CRITERIA (Subterm criterion) ST: Marked_isQid -> 1 APPLY CRITERIA (Subterm criterion) ST: Marked_isNePal -> 1 APPLY CRITERIA (Subterm criterion) ST: Marked___ -> 2 APPLY CRITERIA (Subterm criterion) ST: Marked_U11 -> 1 APPLY CRITERIA (Subterm criterion) ST: Marked_U21 -> 2 APPLY CRITERIA (Subterm criterion) ST: Marked_U22 -> 1 APPLY CRITERIA (Subterm criterion) ST: Marked_U31 -> 1 APPLY CRITERIA (Subterm criterion) ST: Marked_U41 -> 2 APPLY CRITERIA (Subterm criterion) ST: Marked_U42 -> 1 APPLY CRITERIA (Subterm criterion) ST: Marked_U51 -> 2 APPLY CRITERIA (Subterm criterion) ST: Marked_U52 -> 1 APPLY CRITERIA (Subterm criterion) ST: Marked_U61 -> 1 APPLY CRITERIA (Subterm criterion) ST: Marked_U71 -> 2 APPLY CRITERIA (Subterm criterion) ST: Marked_U72 -> 1 APPLY CRITERIA (Subterm criterion) ST: Marked_U81 -> 1 APPLY CRITERIA (Graph splitting) Found 1 components: { --> } APPLY CRITERIA (Subterm criterion) APPLY CRITERIA (Choosing graph) Trying to solve the following constraints: { __(mark(X1),X2) >= mark(__(X1,X2)) ; __(ok(X1),ok(X2)) >= ok(__(X1,X2)) ; __(X1,mark(X2)) >= mark(__(X1,X2)) ; active(__(__(X,Y),Z)) >= mark(__(X,__(Y,Z))) ; active(__(nil,X)) >= mark(X) ; active(__(X,nil)) >= mark(X) ; active(__(X1,X2)) >= __(active(X1),X2) ; active(__(X1,X2)) >= __(X1,active(X2)) ; active(U11(tt)) >= mark(tt) ; active(U11(X)) >= U11(active(X)) ; active(U22(tt)) >= mark(tt) ; active(U22(X)) >= U22(active(X)) ; 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(U21(X1,X2)) >= U21(active(X1),X2) ; active(U31(tt)) >= mark(tt) ; active(U31(X)) >= U31(active(X)) ; active(U42(tt)) >= mark(tt) ; active(U42(X)) >= U42(active(X)) ; 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(U41(X1,X2)) >= U41(active(X1),X2) ; active(U52(tt)) >= mark(tt) ; active(U52(X)) >= U52(active(X)) ; active(U51(tt,V2)) >= mark(U52(isList(V2))) ; active(U51(X1,X2)) >= U51(active(X1),X2) ; active(U61(tt)) >= mark(tt) ; active(U61(X)) >= U61(active(X)) ; active(U72(tt)) >= mark(tt) ; active(U72(X)) >= U72(active(X)) ; active(isPal(nil)) >= mark(tt) ; active(isPal(V)) >= mark(U81(isNePal(V))) ; active(U71(tt,P)) >= mark(U72(isPal(P))) ; active(U71(X1,X2)) >= U71(active(X1),X2) ; active(U81(tt)) >= mark(tt) ; active(U81(X)) >= U81(active(X)) ; 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)) >= mark(U11(X)) ; U11(ok(X)) >= ok(U11(X)) ; U22(mark(X)) >= mark(U22(X)) ; U22(ok(X)) >= ok(U22(X)) ; isList(ok(X)) >= ok(isList(X)) ; U21(mark(X1),X2) >= mark(U21(X1,X2)) ; U21(ok(X1),ok(X2)) >= ok(U21(X1,X2)) ; U31(mark(X)) >= mark(U31(X)) ; U31(ok(X)) >= ok(U31(X)) ; U42(mark(X)) >= mark(U42(X)) ; U42(ok(X)) >= ok(U42(X)) ; isNeList(ok(X)) >= ok(isNeList(X)) ; U41(mark(X1),X2) >= mark(U41(X1,X2)) ; U41(ok(X1),ok(X2)) >= ok(U41(X1,X2)) ; U52(mark(X)) >= mark(U52(X)) ; U52(ok(X)) >= ok(U52(X)) ; U51(mark(X1),X2) >= mark(U51(X1,X2)) ; U51(ok(X1),ok(X2)) >= ok(U51(X1,X2)) ; U61(mark(X)) >= mark(U61(X)) ; U61(ok(X)) >= ok(U61(X)) ; U72(mark(X)) >= mark(U72(X)) ; U72(ok(X)) >= ok(U72(X)) ; isPal(ok(X)) >= ok(isPal(X)) ; U71(mark(X1),X2) >= mark(U71(X1,X2)) ; U71(ok(X1),ok(X2)) >= ok(U71(X1,X2)) ; U81(mark(X)) >= mark(U81(X)) ; U81(ok(X)) >= ok(U81(X)) ; isQid(ok(X)) >= ok(isQid(X)) ; isNePal(ok(X)) >= ok(isNePal(X)) ; proper(__(X1,X2)) >= __(proper(X1),proper(X2)) ; proper(nil) >= ok(nil) ; proper(tt) >= ok(tt) ; proper(U11(X)) >= U11(proper(X)) ; proper(U22(X)) >= U22(proper(X)) ; proper(isList(X)) >= isList(proper(X)) ; proper(U21(X1,X2)) >= U21(proper(X1),proper(X2)) ; proper(U31(X)) >= U31(proper(X)) ; proper(U42(X)) >= U42(proper(X)) ; proper(isNeList(X)) >= isNeList(proper(X)) ; proper(U41(X1,X2)) >= U41(proper(X1),proper(X2)) ; proper(U52(X)) >= U52(proper(X)) ; proper(U51(X1,X2)) >= U51(proper(X1),proper(X2)) ; proper(U61(X)) >= U61(proper(X)) ; proper(U72(X)) >= U72(proper(X)) ; proper(isPal(X)) >= isPal(proper(X)) ; proper(U71(X1,X2)) >= U71(proper(X1),proper(X2)) ; proper(U81(X)) >= U81(proper(X)) ; proper(isQid(X)) >= isQid(proper(X)) ; proper(isNePal(X)) >= isNePal(proper(X)) ; proper(a) >= ok(a) ; proper(e) >= ok(e) ; proper(i) >= ok(i) ; proper(o) >= ok(o) ; proper(u) >= ok(u) ; top(mark(X)) >= top(proper(X)) ; top(ok(X)) >= top(active(X)) ; Marked_top(ok(X)) >= Marked_top(active(X)) ; } + Disjunctions:{ { Marked_top(ok(X)) > Marked_top(active(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: __(mark(X1),X2) >= mark(__(X1,X2)) constraint: __(ok(X1),ok(X2)) >= ok(__(X1,X2)) constraint: __(X1,mark(X2)) >= mark(__(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(__(X1,X2)) >= __(active(X1),X2) constraint: active(__(X1,X2)) >= __(X1,active(X2)) constraint: active(U11(tt)) >= mark(tt) constraint: active(U11(X)) >= U11(active(X)) constraint: active(U22(tt)) >= mark(tt) constraint: active(U22(X)) >= U22(active(X)) 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(U21(X1,X2)) >= U21(active(X1),X2) constraint: active(U31(tt)) >= mark(tt) constraint: active(U31(X)) >= U31(active(X)) constraint: active(U42(tt)) >= mark(tt) constraint: active(U42(X)) >= U42(active(X)) 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(U41(X1,X2)) >= U41(active(X1),X2) constraint: active(U52(tt)) >= mark(tt) constraint: active(U52(X)) >= U52(active(X)) constraint: active(U51(tt,V2)) >= mark(U52(isList(V2))) constraint: active(U51(X1,X2)) >= U51(active(X1),X2) constraint: active(U61(tt)) >= mark(tt) constraint: active(U61(X)) >= U61(active(X)) constraint: active(U72(tt)) >= mark(tt) constraint: active(U72(X)) >= U72(active(X)) 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(U71(X1,X2)) >= U71(active(X1),X2) constraint: active(U81(tt)) >= mark(tt) constraint: active(U81(X)) >= U81(active(X)) 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)) >= mark(U11(X)) constraint: U11(ok(X)) >= ok(U11(X)) constraint: U22(mark(X)) >= mark(U22(X)) constraint: U22(ok(X)) >= ok(U22(X)) constraint: isList(ok(X)) >= ok(isList(X)) constraint: U21(mark(X1),X2) >= mark(U21(X1,X2)) constraint: U21(ok(X1),ok(X2)) >= ok(U21(X1,X2)) constraint: U31(mark(X)) >= mark(U31(X)) constraint: U31(ok(X)) >= ok(U31(X)) constraint: U42(mark(X)) >= mark(U42(X)) constraint: U42(ok(X)) >= ok(U42(X)) constraint: isNeList(ok(X)) >= ok(isNeList(X)) constraint: U41(mark(X1),X2) >= mark(U41(X1,X2)) constraint: U41(ok(X1),ok(X2)) >= ok(U41(X1,X2)) constraint: U52(mark(X)) >= mark(U52(X)) constraint: U52(ok(X)) >= ok(U52(X)) constraint: U51(mark(X1),X2) >= mark(U51(X1,X2)) constraint: U51(ok(X1),ok(X2)) >= ok(U51(X1,X2)) constraint: U61(mark(X)) >= mark(U61(X)) constraint: U61(ok(X)) >= ok(U61(X)) constraint: U72(mark(X)) >= mark(U72(X)) constraint: U72(ok(X)) >= ok(U72(X)) constraint: isPal(ok(X)) >= ok(isPal(X)) constraint: U71(mark(X1),X2) >= mark(U71(X1,X2)) constraint: U71(ok(X1),ok(X2)) >= ok(U71(X1,X2)) constraint: U81(mark(X)) >= mark(U81(X)) constraint: U81(ok(X)) >= ok(U81(X)) constraint: isQid(ok(X)) >= ok(isQid(X)) constraint: isNePal(ok(X)) >= ok(isNePal(X)) constraint: proper(__(X1,X2)) >= __(proper(X1),proper(X2)) constraint: proper(nil) >= ok(nil) constraint: proper(tt) >= ok(tt) constraint: proper(U11(X)) >= U11(proper(X)) constraint: proper(U22(X)) >= U22(proper(X)) constraint: proper(isList(X)) >= isList(proper(X)) constraint: proper(U21(X1,X2)) >= U21(proper(X1),proper(X2)) constraint: proper(U31(X)) >= U31(proper(X)) constraint: proper(U42(X)) >= U42(proper(X)) constraint: proper(isNeList(X)) >= isNeList(proper(X)) constraint: proper(U41(X1,X2)) >= U41(proper(X1),proper(X2)) constraint: proper(U52(X)) >= U52(proper(X)) constraint: proper(U51(X1,X2)) >= U51(proper(X1),proper(X2)) constraint: proper(U61(X)) >= U61(proper(X)) constraint: proper(U72(X)) >= U72(proper(X)) constraint: proper(isPal(X)) >= isPal(proper(X)) constraint: proper(U71(X1,X2)) >= U71(proper(X1),proper(X2)) constraint: proper(U81(X)) >= U81(proper(X)) constraint: proper(isQid(X)) >= isQid(proper(X)) constraint: proper(isNePal(X)) >= isNePal(proper(X)) constraint: proper(a) >= ok(a) constraint: proper(e) >= ok(e) constraint: proper(i) >= ok(i) constraint: proper(o) >= ok(o) constraint: proper(u) >= ok(u) constraint: top(mark(X)) >= top(proper(X)) constraint: top(ok(X)) >= top(active(X)) constraint: Marked_top(ok(X)) >= Marked_top(active(X)) 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: 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 1 components: { --> } APPLY CRITERIA (Subterm criterion) ST: Marked___ -> 1 APPLY CRITERIA (Graph splitting) Found 0 components: APPLY CRITERIA (Graph splitting) Found 0 components: APPLY CRITERIA (Graph splitting) Found 1 components: { --> } APPLY CRITERIA (Subterm criterion) ST: Marked_U21 -> 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 1 components: { --> } APPLY CRITERIA (Subterm criterion) ST: Marked_U41 -> 1 APPLY CRITERIA (Graph splitting) Found 0 components: APPLY CRITERIA (Graph splitting) Found 0 components: APPLY CRITERIA (Graph splitting) Found 1 components: { --> } APPLY CRITERIA (Subterm criterion) ST: Marked_U51 -> 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 1 components: { --> } APPLY CRITERIA (Subterm criterion) ST: Marked_U71 -> 1 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] 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] active(__(X1,X2)) -> __(active(X1),X2) [32] active(__(X1,X2)) -> __(X1,active(X2)) [33] active(U11(X)) -> U11(active(X)) [34] active(U21(X1,X2)) -> U21(active(X1),X2) [35] active(U22(X)) -> U22(active(X)) [36] active(U31(X)) -> U31(active(X)) [37] active(U41(X1,X2)) -> U41(active(X1),X2) [38] active(U42(X)) -> U42(active(X)) [39] active(U51(X1,X2)) -> U51(active(X1),X2) [40] active(U52(X)) -> U52(active(X)) [41] active(U61(X)) -> U61(active(X)) [42] active(U71(X1,X2)) -> U71(active(X1),X2) [43] active(U72(X)) -> U72(active(X)) [44] active(U81(X)) -> U81(active(X)) [45] __(mark(X1),X2) -> mark(__(X1,X2)) [46] __(X1,mark(X2)) -> mark(__(X1,X2)) [47] U11(mark(X)) -> mark(U11(X)) [48] U21(mark(X1),X2) -> mark(U21(X1,X2)) [49] U22(mark(X)) -> mark(U22(X)) [50] U31(mark(X)) -> mark(U31(X)) [51] U41(mark(X1),X2) -> mark(U41(X1,X2)) [52] U42(mark(X)) -> mark(U42(X)) [53] U51(mark(X1),X2) -> mark(U51(X1,X2)) [54] U52(mark(X)) -> mark(U52(X)) [55] U61(mark(X)) -> mark(U61(X)) [56] U71(mark(X1),X2) -> mark(U71(X1,X2)) [57] U72(mark(X)) -> mark(U72(X)) [58] U81(mark(X)) -> mark(U81(X)) [59] proper(__(X1,X2)) -> __(proper(X1),proper(X2)) [60] proper(nil) -> ok(nil) [61] proper(U11(X)) -> U11(proper(X)) [62] proper(tt) -> ok(tt) [63] proper(U21(X1,X2)) -> U21(proper(X1),proper(X2)) [64] proper(U22(X)) -> U22(proper(X)) [65] proper(isList(X)) -> isList(proper(X)) [66] proper(U31(X)) -> U31(proper(X)) [67] proper(U41(X1,X2)) -> U41(proper(X1),proper(X2)) [68] proper(U42(X)) -> U42(proper(X)) [69] proper(isNeList(X)) -> isNeList(proper(X)) [70] proper(U51(X1,X2)) -> U51(proper(X1),proper(X2)) [71] proper(U52(X)) -> U52(proper(X)) [72] proper(U61(X)) -> U61(proper(X)) [73] proper(U71(X1,X2)) -> U71(proper(X1),proper(X2)) [74] proper(U72(X)) -> U72(proper(X)) [75] proper(isPal(X)) -> isPal(proper(X)) [76] proper(U81(X)) -> U81(proper(X)) [77] proper(isQid(X)) -> isQid(proper(X)) [78] proper(isNePal(X)) -> isNePal(proper(X)) [79] proper(a) -> ok(a) [80] proper(e) -> ok(e) [81] proper(i) -> ok(i) [82] proper(o) -> ok(o) [83] proper(u) -> ok(u) [84] __(ok(X1),ok(X2)) -> ok(__(X1,X2)) [85] U11(ok(X)) -> ok(U11(X)) [86] U21(ok(X1),ok(X2)) -> ok(U21(X1,X2)) [87] U22(ok(X)) -> ok(U22(X)) [88] isList(ok(X)) -> ok(isList(X)) [89] U31(ok(X)) -> ok(U31(X)) [90] U41(ok(X1),ok(X2)) -> ok(U41(X1,X2)) [91] U42(ok(X)) -> ok(U42(X)) [92] isNeList(ok(X)) -> ok(isNeList(X)) [93] U51(ok(X1),ok(X2)) -> ok(U51(X1,X2)) [94] U52(ok(X)) -> ok(U52(X)) [95] U61(ok(X)) -> ok(U61(X)) [96] U71(ok(X1),ok(X2)) -> ok(U71(X1,X2)) [97] U72(ok(X)) -> ok(U72(X)) [98] isPal(ok(X)) -> ok(isPal(X)) [99] U81(ok(X)) -> ok(U81(X)) [100] isQid(ok(X)) -> ok(isQid(X)) [101] isNePal(ok(X)) -> ok(isNePal(X)) [102] top(mark(X)) -> top(proper(X)) [103] top(ok(X)) -> top(active(X)) , CRITERION: MDP [ { DP termination of: , CRITERION: SG [ { DP termination of: , CRITERION: CG using polynomial interpretation = [ mark ] (X0) = 1*X0 + 1; [ U72 ] (X0) = 1*X0 + 1; [ U21 ] (X0,X1) = 3*X1 + 2*X0 + 3; [ i ] () = 3; [ tt ] () = 2; [ isQid ] (X0) = 1*X0; [ U41 ] (X0,X1) = 3*X1 + 2*X0 + 2; [ ok ] (X0) = 1*X0; [ active ] (X0) = 1*X0; [ U71 ] (X0,X1) = 3*X1 + 3*X0; [ U42 ] (X0) = 1*X0 + 1; [ u ] () = 3; [ U22 ] (X0) = 1*X0 + 3; [ a ] () = 3; [ U51 ] (X0,X1) = 3*X1 + 3*X0 + 2; [ Marked_top ] (X0) = 1*X0; [ __ ] (X0,X1) = 1*X1 + 3*X0 + 3; [ isPal ] (X0) = 2*X0 + 3; [ U31 ] (X0) = 2*X0; [ o ] () = 3; [ U11 ] (X0) = 1*X0 + 1; [ isNePal ] (X0) = 2*X0 + 1; [ U52 ] (X0) = 1*X0 + 2; [ top ] (X0) = 0; [ nil ] () = 0; [ U81 ] (X0) = 1*X0 + 1; [ isNeList ] (X0) = 3*X0 + 1; [ proper ] (X0) = 1*X0; [ isList ] (X0) = 3*X0 + 3; [ e ] () = 3; [ U61 ] (X0) = 2*X0; removing [ { DP termination of: , CRITERION: SG [ { DP termination of: , CRITERION: ORD [ Solution found: polynomial interpretation = [ mark ] (X0) = 2 + 0; [ U72 ] (X0) = 2*X0 + 0; [ U21 ] (X0,X1) = 1*X0 + 1*X1 + 0; [ i ] () = 2 + 0; [ tt ] () = 2 + 0; [ isQid ] (X0) = 2*X0 + 0; [ U41 ] (X0,X1) = 2 + 2*X1 + 0; [ ok ] (X0) = 2 + 2*X0 + 0; [ active ] (X0) = 1*X0 + 0; [ U71 ] (X0,X1) = 2 + 2*X1 + 0; [ U42 ] (X0) = 2 + 3*X0 + 0; [ u ] () = 2 + 0; [ U22 ] (X0) = 2*X0 + 0; [ a ] () = 2 + 0; [ U51 ] (X0,X1) = 2*X0 + 2*X1 + 0; [ Marked_top ] (X0) = 3*X0 + 0; [ __ ] (X0,X1) = 1 + 2*X0 + 2*X1 + 0; [ isPal ] (X0) = 2 + 3*X0 + 0; [ U31 ] (X0) = 2*X0 + 0; [ o ] () = 3 + 0; [ U11 ] (X0) = 2 + 3*X0 + 0; [ isNePal ] (X0) = 2 + 2*X0 + 0; [ U52 ] (X0) = 2 + 3*X0 + 0; [ top ] (X0) = 0; [ nil ] () = 2 + 0; [ U81 ] (X0) = 2 + 3*X0 + 0; [ isNeList ] (X0) = 3 + 3*X0 + 0; [ proper ] (X0) = 3*X0 + 0; [ isList ] (X0) = 2 + 2*X0 + 0; [ e ] () = 2 + 0; [ U61 ] (X0) = 2*X0 + 0; ]} ]} ]} { DP termination of: , CRITERION: ST [ { 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 [ ]} ]} { DP termination of: , CRITERION: ST [ { 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 [ ]} ]} { DP termination of: , CRITERION: ST [ { 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 [ ]} ]} ]} ]} { DP termination of: , CRITERION: ST [ { 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 [ ]} ]} ]} ]} { DP termination of: , CRITERION: ST [ { 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 [ { DP termination of: , CRITERION: ST [ { 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 [ { DP termination of: , CRITERION: ST [ { 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 [ ]} ]} { DP termination of: , CRITERION: ST [ { 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 [ ]} ]} { DP termination of: , CRITERION: ST [ { DP termination of: , CRITERION: SG [ ]} ]} ]} ]} Cime worked for 1.229991 seconds (real time) Cime Exit Status: 0