- : unit = () - : unit = () h : heuristic = - : unit = () APPLY CRITERIA (Marked dependency pairs) TRS termination of: [1] active(U11(tt,V1,V2)) -> mark(U12(isNatKind(V1),V1,V2)) [2] active(U12(tt,V1,V2)) -> mark(U13(isNatKind(V2),V1,V2)) [3] active(U13(tt,V1,V2)) -> mark(U14(isNatKind(V2),V1,V2)) [4] active(U14(tt,V1,V2)) -> mark(U15(isNat(V1),V2)) [5] active(U15(tt,V2)) -> mark(U16(isNat(V2))) [6] active(U16(tt)) -> mark(tt) [7] active(U21(tt,V1)) -> mark(U22(isNatKind(V1),V1)) [8] active(U22(tt,V1)) -> mark(U23(isNat(V1))) [9] active(U23(tt)) -> mark(tt) [10] active(U31(tt,V2)) -> mark(U32(isNatKind(V2))) [11] active(U32(tt)) -> mark(tt) [12] active(U41(tt)) -> mark(tt) [13] active(U51(tt,N)) -> mark(U52(isNatKind(N),N)) [14] active(U52(tt,N)) -> mark(N) [15] active(U61(tt,M,N)) -> mark(U62(isNatKind(M),M,N)) [16] active(U62(tt,M,N)) -> mark(U63(isNat(N),M,N)) [17] active(U63(tt,M,N)) -> mark(U64(isNatKind(N),M,N)) [18] active(U64(tt,M,N)) -> mark(s(plus(N,M))) [19] active(isNat(0)) -> mark(tt) [20] active(isNat(plus(V1,V2))) -> mark(U11(isNatKind(V1),V1,V2)) [21] active(isNat(s(V1))) -> mark(U21(isNatKind(V1),V1)) [22] active(isNatKind(0)) -> mark(tt) [23] active(isNatKind(plus(V1,V2))) -> mark(U31(isNatKind(V1),V2)) [24] active(isNatKind(s(V1))) -> mark(U41(isNatKind(V1))) [25] active(plus(N,0)) -> mark(U51(isNat(N),N)) [26] active(plus(N,s(M))) -> mark(U61(isNat(M),M,N)) [27] mark(U11(X1,X2,X3)) -> active(U11(mark(X1),X2,X3)) [28] mark(tt) -> active(tt) [29] mark(U12(X1,X2,X3)) -> active(U12(mark(X1),X2,X3)) [30] mark(isNatKind(X)) -> active(isNatKind(X)) [31] mark(U13(X1,X2,X3)) -> active(U13(mark(X1),X2,X3)) [32] mark(U14(X1,X2,X3)) -> active(U14(mark(X1),X2,X3)) [33] mark(U15(X1,X2)) -> active(U15(mark(X1),X2)) [34] mark(isNat(X)) -> active(isNat(X)) [35] mark(U16(X)) -> active(U16(mark(X))) [36] mark(U21(X1,X2)) -> active(U21(mark(X1),X2)) [37] mark(U22(X1,X2)) -> active(U22(mark(X1),X2)) [38] mark(U23(X)) -> active(U23(mark(X))) [39] mark(U31(X1,X2)) -> active(U31(mark(X1),X2)) [40] mark(U32(X)) -> active(U32(mark(X))) [41] mark(U41(X)) -> active(U41(mark(X))) [42] mark(U51(X1,X2)) -> active(U51(mark(X1),X2)) [43] mark(U52(X1,X2)) -> active(U52(mark(X1),X2)) [44] mark(U61(X1,X2,X3)) -> active(U61(mark(X1),X2,X3)) [45] mark(U62(X1,X2,X3)) -> active(U62(mark(X1),X2,X3)) [46] mark(U63(X1,X2,X3)) -> active(U63(mark(X1),X2,X3)) [47] mark(U64(X1,X2,X3)) -> active(U64(mark(X1),X2,X3)) [48] mark(s(X)) -> active(s(mark(X))) [49] mark(plus(X1,X2)) -> active(plus(mark(X1),mark(X2))) [50] mark(0) -> active(0) [51] U11(mark(X1),X2,X3) -> U11(X1,X2,X3) [52] U11(X1,mark(X2),X3) -> U11(X1,X2,X3) [53] U11(X1,X2,mark(X3)) -> U11(X1,X2,X3) [54] U11(active(X1),X2,X3) -> U11(X1,X2,X3) [55] U11(X1,active(X2),X3) -> U11(X1,X2,X3) [56] U11(X1,X2,active(X3)) -> U11(X1,X2,X3) [57] U12(mark(X1),X2,X3) -> U12(X1,X2,X3) [58] U12(X1,mark(X2),X3) -> U12(X1,X2,X3) [59] U12(X1,X2,mark(X3)) -> U12(X1,X2,X3) [60] U12(active(X1),X2,X3) -> U12(X1,X2,X3) [61] U12(X1,active(X2),X3) -> U12(X1,X2,X3) [62] U12(X1,X2,active(X3)) -> U12(X1,X2,X3) [63] isNatKind(mark(X)) -> isNatKind(X) [64] isNatKind(active(X)) -> isNatKind(X) [65] U13(mark(X1),X2,X3) -> U13(X1,X2,X3) [66] U13(X1,mark(X2),X3) -> U13(X1,X2,X3) [67] U13(X1,X2,mark(X3)) -> U13(X1,X2,X3) [68] U13(active(X1),X2,X3) -> U13(X1,X2,X3) [69] U13(X1,active(X2),X3) -> U13(X1,X2,X3) [70] U13(X1,X2,active(X3)) -> U13(X1,X2,X3) [71] U14(mark(X1),X2,X3) -> U14(X1,X2,X3) [72] U14(X1,mark(X2),X3) -> U14(X1,X2,X3) [73] U14(X1,X2,mark(X3)) -> U14(X1,X2,X3) [74] U14(active(X1),X2,X3) -> U14(X1,X2,X3) [75] U14(X1,active(X2),X3) -> U14(X1,X2,X3) [76] U14(X1,X2,active(X3)) -> U14(X1,X2,X3) [77] U15(mark(X1),X2) -> U15(X1,X2) [78] U15(X1,mark(X2)) -> U15(X1,X2) [79] U15(active(X1),X2) -> U15(X1,X2) [80] U15(X1,active(X2)) -> U15(X1,X2) [81] isNat(mark(X)) -> isNat(X) [82] isNat(active(X)) -> isNat(X) [83] U16(mark(X)) -> U16(X) [84] U16(active(X)) -> U16(X) [85] U21(mark(X1),X2) -> U21(X1,X2) [86] U21(X1,mark(X2)) -> U21(X1,X2) [87] U21(active(X1),X2) -> U21(X1,X2) [88] U21(X1,active(X2)) -> U21(X1,X2) [89] U22(mark(X1),X2) -> U22(X1,X2) [90] U22(X1,mark(X2)) -> U22(X1,X2) [91] U22(active(X1),X2) -> U22(X1,X2) [92] U22(X1,active(X2)) -> U22(X1,X2) [93] U23(mark(X)) -> U23(X) [94] U23(active(X)) -> U23(X) [95] U31(mark(X1),X2) -> U31(X1,X2) [96] U31(X1,mark(X2)) -> U31(X1,X2) [97] U31(active(X1),X2) -> U31(X1,X2) [98] U31(X1,active(X2)) -> U31(X1,X2) [99] U32(mark(X)) -> U32(X) [100] U32(active(X)) -> U32(X) [101] U41(mark(X)) -> U41(X) [102] U41(active(X)) -> U41(X) [103] U51(mark(X1),X2) -> U51(X1,X2) [104] U51(X1,mark(X2)) -> U51(X1,X2) [105] U51(active(X1),X2) -> U51(X1,X2) [106] U51(X1,active(X2)) -> U51(X1,X2) [107] U52(mark(X1),X2) -> U52(X1,X2) [108] U52(X1,mark(X2)) -> U52(X1,X2) [109] U52(active(X1),X2) -> U52(X1,X2) [110] U52(X1,active(X2)) -> U52(X1,X2) [111] U61(mark(X1),X2,X3) -> U61(X1,X2,X3) [112] U61(X1,mark(X2),X3) -> U61(X1,X2,X3) [113] U61(X1,X2,mark(X3)) -> U61(X1,X2,X3) [114] U61(active(X1),X2,X3) -> U61(X1,X2,X3) [115] U61(X1,active(X2),X3) -> U61(X1,X2,X3) [116] U61(X1,X2,active(X3)) -> U61(X1,X2,X3) [117] U62(mark(X1),X2,X3) -> U62(X1,X2,X3) [118] U62(X1,mark(X2),X3) -> U62(X1,X2,X3) [119] U62(X1,X2,mark(X3)) -> U62(X1,X2,X3) [120] U62(active(X1),X2,X3) -> U62(X1,X2,X3) [121] U62(X1,active(X2),X3) -> U62(X1,X2,X3) [122] U62(X1,X2,active(X3)) -> U62(X1,X2,X3) [123] U63(mark(X1),X2,X3) -> U63(X1,X2,X3) [124] U63(X1,mark(X2),X3) -> U63(X1,X2,X3) [125] U63(X1,X2,mark(X3)) -> U63(X1,X2,X3) [126] U63(active(X1),X2,X3) -> U63(X1,X2,X3) [127] U63(X1,active(X2),X3) -> U63(X1,X2,X3) [128] U63(X1,X2,active(X3)) -> U63(X1,X2,X3) [129] U64(mark(X1),X2,X3) -> U64(X1,X2,X3) [130] U64(X1,mark(X2),X3) -> U64(X1,X2,X3) [131] U64(X1,X2,mark(X3)) -> U64(X1,X2,X3) [132] U64(active(X1),X2,X3) -> U64(X1,X2,X3) [133] U64(X1,active(X2),X3) -> U64(X1,X2,X3) [134] U64(X1,X2,active(X3)) -> U64(X1,X2,X3) [135] s(mark(X)) -> s(X) [136] s(active(X)) -> s(X) [137] plus(mark(X1),X2) -> plus(X1,X2) [138] plus(X1,mark(X2)) -> plus(X1,X2) [139] plus(active(X1),X2) -> plus(X1,X2) [140] plus(X1,active(X2)) -> plus(X1,X2) Sub problem: guided: DP termination of: END GUIDED APPLY CRITERIA (Graph splitting) Found 23 components: { --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> } { --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> } { --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> } { --> --> --> --> } { --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> } { --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> } { --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> } { --> --> --> --> } { --> --> --> --> } { --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> } { --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> } { --> --> --> --> } { --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> } { --> --> --> --> } { --> --> --> --> } { --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> } { --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> } { --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> } { --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> } { --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> } { --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> } { --> --> --> --> } { --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> } APPLY CRITERIA (Subterm criterion) APPLY CRITERIA (Choosing graph) Trying to solve the following constraints: { mark(U12(X1,X2,X3)) >= active(U12(mark(X1),X2,X3)) ; mark(isNatKind(X)) >= active(isNatKind(X)) ; mark(U11(X1,X2,X3)) >= active(U11(mark(X1),X2,X3)) ; mark(tt) >= active(tt) ; mark(U13(X1,X2,X3)) >= active(U13(mark(X1),X2,X3)) ; mark(U14(X1,X2,X3)) >= active(U14(mark(X1),X2,X3)) ; mark(U15(X1,X2)) >= active(U15(mark(X1),X2)) ; mark(isNat(X)) >= active(isNat(X)) ; mark(U16(X)) >= active(U16(mark(X))) ; mark(U22(X1,X2)) >= active(U22(mark(X1),X2)) ; mark(U21(X1,X2)) >= active(U21(mark(X1),X2)) ; mark(U23(X)) >= active(U23(mark(X))) ; mark(U32(X)) >= active(U32(mark(X))) ; mark(U31(X1,X2)) >= active(U31(mark(X1),X2)) ; mark(U41(X)) >= active(U41(mark(X))) ; mark(U52(X1,X2)) >= active(U52(mark(X1),X2)) ; mark(U51(X1,X2)) >= active(U51(mark(X1),X2)) ; mark(U62(X1,X2,X3)) >= active(U62(mark(X1),X2,X3)) ; mark(U61(X1,X2,X3)) >= active(U61(mark(X1),X2,X3)) ; mark(U63(X1,X2,X3)) >= active(U63(mark(X1),X2,X3)) ; mark(U64(X1,X2,X3)) >= active(U64(mark(X1),X2,X3)) ; mark(s(X)) >= active(s(mark(X))) ; mark(plus(X1,X2)) >= active(plus(mark(X1),mark(X2))) ; mark(0) >= active(0) ; U12(mark(X1),X2,X3) >= U12(X1,X2,X3) ; U12(active(X1),X2,X3) >= U12(X1,X2,X3) ; U12(X1,mark(X2),X3) >= U12(X1,X2,X3) ; U12(X1,active(X2),X3) >= U12(X1,X2,X3) ; U12(X1,X2,mark(X3)) >= U12(X1,X2,X3) ; U12(X1,X2,active(X3)) >= U12(X1,X2,X3) ; isNatKind(mark(X)) >= isNatKind(X) ; isNatKind(active(X)) >= isNatKind(X) ; active(U12(tt,V1,V2)) >= mark(U13(isNatKind(V2),V1,V2)) ; active(isNatKind(s(V1))) >= mark(U41(isNatKind(V1))) ; active(isNatKind(plus(V1,V2))) >= mark(U31(isNatKind(V1),V2)) ; active(isNatKind(0)) >= mark(tt) ; active(U11(tt,V1,V2)) >= mark(U12(isNatKind(V1),V1,V2)) ; active(U13(tt,V1,V2)) >= mark(U14(isNatKind(V2),V1,V2)) ; active(U14(tt,V1,V2)) >= mark(U15(isNat(V1),V2)) ; active(U15(tt,V2)) >= mark(U16(isNat(V2))) ; active(isNat(s(V1))) >= mark(U21(isNatKind(V1),V1)) ; active(isNat(plus(V1,V2))) >= mark(U11(isNatKind(V1),V1,V2)) ; active(isNat(0)) >= mark(tt) ; active(U16(tt)) >= mark(tt) ; active(U22(tt,V1)) >= mark(U23(isNat(V1))) ; active(U21(tt,V1)) >= mark(U22(isNatKind(V1),V1)) ; active(U23(tt)) >= mark(tt) ; active(U32(tt)) >= mark(tt) ; active(U31(tt,V2)) >= mark(U32(isNatKind(V2))) ; active(U41(tt)) >= mark(tt) ; active(U52(tt,N)) >= mark(N) ; active(U51(tt,N)) >= mark(U52(isNatKind(N),N)) ; active(U62(tt,M,N)) >= mark(U63(isNat(N),M,N)) ; active(U61(tt,M,N)) >= mark(U62(isNatKind(M),M,N)) ; active(U63(tt,M,N)) >= mark(U64(isNatKind(N),M,N)) ; active(U64(tt,M,N)) >= mark(s(plus(N,M))) ; active(plus(N,s(M))) >= mark(U61(isNat(M),M,N)) ; active(plus(N,0)) >= mark(U51(isNat(N),N)) ; U11(mark(X1),X2,X3) >= U11(X1,X2,X3) ; U11(active(X1),X2,X3) >= U11(X1,X2,X3) ; U11(X1,mark(X2),X3) >= U11(X1,X2,X3) ; U11(X1,active(X2),X3) >= U11(X1,X2,X3) ; U11(X1,X2,mark(X3)) >= U11(X1,X2,X3) ; U11(X1,X2,active(X3)) >= U11(X1,X2,X3) ; U13(mark(X1),X2,X3) >= U13(X1,X2,X3) ; U13(active(X1),X2,X3) >= U13(X1,X2,X3) ; U13(X1,mark(X2),X3) >= U13(X1,X2,X3) ; U13(X1,active(X2),X3) >= U13(X1,X2,X3) ; U13(X1,X2,mark(X3)) >= U13(X1,X2,X3) ; U13(X1,X2,active(X3)) >= U13(X1,X2,X3) ; U14(mark(X1),X2,X3) >= U14(X1,X2,X3) ; U14(active(X1),X2,X3) >= U14(X1,X2,X3) ; U14(X1,mark(X2),X3) >= U14(X1,X2,X3) ; U14(X1,active(X2),X3) >= U14(X1,X2,X3) ; U14(X1,X2,mark(X3)) >= U14(X1,X2,X3) ; U14(X1,X2,active(X3)) >= U14(X1,X2,X3) ; U15(mark(X1),X2) >= U15(X1,X2) ; U15(active(X1),X2) >= U15(X1,X2) ; U15(X1,mark(X2)) >= U15(X1,X2) ; U15(X1,active(X2)) >= U15(X1,X2) ; isNat(mark(X)) >= isNat(X) ; isNat(active(X)) >= isNat(X) ; U16(mark(X)) >= U16(X) ; U16(active(X)) >= U16(X) ; U22(mark(X1),X2) >= U22(X1,X2) ; U22(active(X1),X2) >= U22(X1,X2) ; U22(X1,mark(X2)) >= U22(X1,X2) ; U22(X1,active(X2)) >= U22(X1,X2) ; 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) ; U23(mark(X)) >= U23(X) ; U23(active(X)) >= U23(X) ; U32(mark(X)) >= U32(X) ; U32(active(X)) >= U32(X) ; U31(mark(X1),X2) >= U31(X1,X2) ; U31(active(X1),X2) >= U31(X1,X2) ; U31(X1,mark(X2)) >= U31(X1,X2) ; U31(X1,active(X2)) >= U31(X1,X2) ; U41(mark(X)) >= U41(X) ; U41(active(X)) >= U41(X) ; U52(mark(X1),X2) >= U52(X1,X2) ; U52(active(X1),X2) >= U52(X1,X2) ; U52(X1,mark(X2)) >= U52(X1,X2) ; U52(X1,active(X2)) >= U52(X1,X2) ; 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) ; U62(mark(X1),X2,X3) >= U62(X1,X2,X3) ; U62(active(X1),X2,X3) >= U62(X1,X2,X3) ; U62(X1,mark(X2),X3) >= U62(X1,X2,X3) ; U62(X1,active(X2),X3) >= U62(X1,X2,X3) ; U62(X1,X2,mark(X3)) >= U62(X1,X2,X3) ; U62(X1,X2,active(X3)) >= U62(X1,X2,X3) ; U61(mark(X1),X2,X3) >= U61(X1,X2,X3) ; U61(active(X1),X2,X3) >= U61(X1,X2,X3) ; U61(X1,mark(X2),X3) >= U61(X1,X2,X3) ; U61(X1,active(X2),X3) >= U61(X1,X2,X3) ; U61(X1,X2,mark(X3)) >= U61(X1,X2,X3) ; U61(X1,X2,active(X3)) >= U61(X1,X2,X3) ; U63(mark(X1),X2,X3) >= U63(X1,X2,X3) ; U63(active(X1),X2,X3) >= U63(X1,X2,X3) ; U63(X1,mark(X2),X3) >= U63(X1,X2,X3) ; U63(X1,active(X2),X3) >= U63(X1,X2,X3) ; U63(X1,X2,mark(X3)) >= U63(X1,X2,X3) ; U63(X1,X2,active(X3)) >= U63(X1,X2,X3) ; U64(mark(X1),X2,X3) >= U64(X1,X2,X3) ; U64(active(X1),X2,X3) >= U64(X1,X2,X3) ; U64(X1,mark(X2),X3) >= U64(X1,X2,X3) ; U64(X1,active(X2),X3) >= U64(X1,X2,X3) ; U64(X1,X2,mark(X3)) >= U64(X1,X2,X3) ; U64(X1,X2,active(X3)) >= U64(X1,X2,X3) ; s(mark(X)) >= s(X) ; s(active(X)) >= s(X) ; plus(mark(X1),X2) >= plus(X1,X2) ; plus(active(X1),X2) >= plus(X1,X2) ; plus(X1,mark(X2)) >= plus(X1,X2) ; plus(X1,active(X2)) >= plus(X1,X2) ; Marked_mark(U12(X1,X2,X3)) >= Marked_mark(X1) ; Marked_mark(U12(X1,X2,X3)) >= Marked_active(U12(mark(X1),X2,X3)) ; Marked_mark(isNatKind(X)) >= Marked_active(isNatKind(X)) ; Marked_mark(U11(X1,X2,X3)) >= Marked_mark(X1) ; Marked_mark(U11(X1,X2,X3)) >= Marked_active(U11(mark(X1),X2,X3)) ; Marked_mark(U13(X1,X2,X3)) >= Marked_mark(X1) ; Marked_mark(U13(X1,X2,X3)) >= Marked_active(U13(mark(X1),X2,X3)) ; Marked_mark(U14(X1,X2,X3)) >= Marked_mark(X1) ; Marked_mark(U14(X1,X2,X3)) >= Marked_active(U14(mark(X1),X2,X3)) ; Marked_mark(U15(X1,X2)) >= Marked_mark(X1) ; Marked_mark(U15(X1,X2)) >= Marked_active(U15(mark(X1),X2)) ; Marked_mark(isNat(X)) >= Marked_active(isNat(X)) ; Marked_mark(U16(X)) >= Marked_mark(X) ; Marked_mark(U16(X)) >= Marked_active(U16(mark(X))) ; Marked_mark(U22(X1,X2)) >= Marked_mark(X1) ; Marked_mark(U22(X1,X2)) >= Marked_active(U22(mark(X1),X2)) ; Marked_mark(U21(X1,X2)) >= Marked_mark(X1) ; Marked_mark(U21(X1,X2)) >= Marked_active(U21(mark(X1),X2)) ; Marked_mark(U23(X)) >= Marked_mark(X) ; Marked_mark(U23(X)) >= Marked_active(U23(mark(X))) ; Marked_mark(U32(X)) >= Marked_mark(X) ; Marked_mark(U32(X)) >= Marked_active(U32(mark(X))) ; Marked_mark(U31(X1,X2)) >= Marked_mark(X1) ; Marked_mark(U31(X1,X2)) >= Marked_active(U31(mark(X1),X2)) ; Marked_mark(U41(X)) >= Marked_mark(X) ; Marked_mark(U41(X)) >= Marked_active(U41(mark(X))) ; Marked_mark(U52(X1,X2)) >= Marked_mark(X1) ; Marked_mark(U52(X1,X2)) >= Marked_active(U52(mark(X1),X2)) ; Marked_mark(U51(X1,X2)) >= Marked_mark(X1) ; Marked_mark(U51(X1,X2)) >= Marked_active(U51(mark(X1),X2)) ; Marked_mark(U62(X1,X2,X3)) >= Marked_mark(X1) ; Marked_mark(U62(X1,X2,X3)) >= Marked_active(U62(mark(X1),X2,X3)) ; Marked_mark(U61(X1,X2,X3)) >= Marked_mark(X1) ; Marked_mark(U61(X1,X2,X3)) >= Marked_active(U61(mark(X1),X2,X3)) ; Marked_mark(U63(X1,X2,X3)) >= Marked_mark(X1) ; Marked_mark(U63(X1,X2,X3)) >= Marked_active(U63(mark(X1),X2,X3)) ; Marked_mark(U64(X1,X2,X3)) >= Marked_mark(X1) ; Marked_mark(U64(X1,X2,X3)) >= Marked_active(U64(mark(X1),X2,X3)) ; Marked_mark(s(X)) >= Marked_mark(X) ; Marked_mark(s(X)) >= Marked_active(s(mark(X))) ; Marked_mark(plus(X1,X2)) >= Marked_mark(X1) ; Marked_mark(plus(X1,X2)) >= Marked_mark(X2) ; Marked_mark(plus(X1,X2)) >= Marked_active(plus(mark(X1),mark(X2))) ; Marked_active(U12(tt,V1,V2)) >= Marked_mark(U13(isNatKind(V2),V1,V2)) ; Marked_active(isNatKind(s(V1))) >= Marked_mark(U41(isNatKind(V1))) ; Marked_active(isNatKind(plus(V1,V2))) >= Marked_mark(U31(isNatKind(V1),V2)) ; Marked_active(U11(tt,V1,V2)) >= Marked_mark(U12(isNatKind(V1),V1,V2)) ; Marked_active(U13(tt,V1,V2)) >= Marked_mark(U14(isNatKind(V2),V1,V2)) ; Marked_active(U14(tt,V1,V2)) >= Marked_mark(U15(isNat(V1),V2)) ; Marked_active(U15(tt,V2)) >= Marked_mark(U16(isNat(V2))) ; Marked_active(isNat(s(V1))) >= Marked_mark(U21(isNatKind(V1),V1)) ; Marked_active(isNat(plus(V1,V2))) >= Marked_mark(U11(isNatKind(V1),V1,V2)) ; Marked_active(U22(tt,V1)) >= Marked_mark(U23(isNat(V1))) ; Marked_active(U21(tt,V1)) >= Marked_mark(U22(isNatKind(V1),V1)) ; Marked_active(U31(tt,V2)) >= Marked_mark(U32(isNatKind(V2))) ; Marked_active(U52(tt,N)) >= Marked_mark(N) ; Marked_active(U51(tt,N)) >= Marked_mark(U52(isNatKind(N),N)) ; Marked_active(U62(tt,M,N)) >= Marked_mark(U63(isNat(N),M,N)) ; Marked_active(U61(tt,M,N)) >= Marked_mark(U62(isNatKind(M),M,N)) ; Marked_active(U63(tt,M,N)) >= Marked_mark(U64(isNatKind(N),M,N)) ; Marked_active(U64(tt,M,N)) >= Marked_mark(s(plus(N,M))) ; Marked_active(plus(N,s(M))) >= Marked_mark(U61(isNat(M),M,N)) ; Marked_active(plus(N,0)) >= Marked_mark(U51(isNat(N),N)) ; } + Disjunctions:{ { Marked_mark(U12(X1,X2,X3)) > Marked_mark(X1) ; } { Marked_mark(U12(X1,X2,X3)) > Marked_active(U12(mark(X1),X2,X3)) ; } { Marked_mark(isNatKind(X)) > Marked_active(isNatKind(X)) ; } { Marked_mark(U11(X1,X2,X3)) > Marked_mark(X1) ; } { Marked_mark(U11(X1,X2,X3)) > Marked_active(U11(mark(X1),X2,X3)) ; } { Marked_mark(U13(X1,X2,X3)) > Marked_mark(X1) ; } { Marked_mark(U13(X1,X2,X3)) > Marked_active(U13(mark(X1),X2,X3)) ; } { Marked_mark(U14(X1,X2,X3)) > Marked_mark(X1) ; } { Marked_mark(U14(X1,X2,X3)) > Marked_active(U14(mark(X1),X2,X3)) ; } { Marked_mark(U15(X1,X2)) > Marked_mark(X1) ; } { Marked_mark(U15(X1,X2)) > Marked_active(U15(mark(X1),X2)) ; } { Marked_mark(isNat(X)) > Marked_active(isNat(X)) ; } { Marked_mark(U16(X)) > Marked_mark(X) ; } { Marked_mark(U16(X)) > Marked_active(U16(mark(X))) ; } { Marked_mark(U22(X1,X2)) > Marked_mark(X1) ; } { Marked_mark(U22(X1,X2)) > Marked_active(U22(mark(X1),X2)) ; } { Marked_mark(U21(X1,X2)) > Marked_mark(X1) ; } { Marked_mark(U21(X1,X2)) > Marked_active(U21(mark(X1),X2)) ; } { Marked_mark(U23(X)) > Marked_mark(X) ; } { Marked_mark(U23(X)) > Marked_active(U23(mark(X))) ; } { Marked_mark(U32(X)) > Marked_mark(X) ; } { Marked_mark(U32(X)) > Marked_active(U32(mark(X))) ; } { Marked_mark(U31(X1,X2)) > Marked_mark(X1) ; } { Marked_mark(U31(X1,X2)) > Marked_active(U31(mark(X1),X2)) ; } { Marked_mark(U41(X)) > Marked_mark(X) ; } { Marked_mark(U41(X)) > Marked_active(U41(mark(X))) ; } { Marked_mark(U52(X1,X2)) > Marked_mark(X1) ; } { Marked_mark(U52(X1,X2)) > Marked_active(U52(mark(X1),X2)) ; } { Marked_mark(U51(X1,X2)) > Marked_mark(X1) ; } { Marked_mark(U51(X1,X2)) > Marked_active(U51(mark(X1),X2)) ; } { Marked_mark(U62(X1,X2,X3)) > Marked_mark(X1) ; } { Marked_mark(U62(X1,X2,X3)) > Marked_active(U62(mark(X1),X2,X3)) ; } { Marked_mark(U61(X1,X2,X3)) > Marked_mark(X1) ; } { Marked_mark(U61(X1,X2,X3)) > Marked_active(U61(mark(X1),X2,X3)) ; } { Marked_mark(U63(X1,X2,X3)) > Marked_mark(X1) ; } { Marked_mark(U63(X1,X2,X3)) > Marked_active(U63(mark(X1),X2,X3)) ; } { Marked_mark(U64(X1,X2,X3)) > Marked_mark(X1) ; } { Marked_mark(U64(X1,X2,X3)) > Marked_active(U64(mark(X1),X2,X3)) ; } { Marked_mark(s(X)) > Marked_mark(X) ; } { Marked_mark(s(X)) > Marked_active(s(mark(X))) ; } { Marked_mark(plus(X1,X2)) > Marked_mark(X1) ; } { Marked_mark(plus(X1,X2)) > Marked_mark(X2) ; } { Marked_mark(plus(X1,X2)) > Marked_active(plus(mark(X1),mark(X2))) ; } { Marked_active(U12(tt,V1,V2)) > Marked_mark(U13(isNatKind(V2),V1,V2)) ; } { Marked_active(isNatKind(s(V1))) > Marked_mark(U41(isNatKind(V1))) ; } { Marked_active(isNatKind(plus(V1,V2))) > Marked_mark(U31(isNatKind(V1),V2)) ; } { Marked_active(U11(tt,V1,V2)) > Marked_mark(U12(isNatKind(V1),V1,V2)) ; } { Marked_active(U13(tt,V1,V2)) > Marked_mark(U14(isNatKind(V2),V1,V2)) ; } { Marked_active(U14(tt,V1,V2)) > Marked_mark(U15(isNat(V1),V2)) ; } { Marked_active(U15(tt,V2)) > Marked_mark(U16(isNat(V2))) ; } { Marked_active(isNat(s(V1))) > Marked_mark(U21(isNatKind(V1),V1)) ; } { Marked_active(isNat(plus(V1,V2))) > Marked_mark(U11(isNatKind(V1),V1,V2)) ; } { Marked_active(U22(tt,V1)) > Marked_mark(U23(isNat(V1))) ; } { Marked_active(U21(tt,V1)) > Marked_mark(U22(isNatKind(V1),V1)) ; } { Marked_active(U31(tt,V2)) > Marked_mark(U32(isNatKind(V2))) ; } { Marked_active(U52(tt,N)) > Marked_mark(N) ; } { Marked_active(U51(tt,N)) > Marked_mark(U52(isNatKind(N),N)) ; } { Marked_active(U62(tt,M,N)) > Marked_mark(U63(isNat(N),M,N)) ; } { Marked_active(U61(tt,M,N)) > Marked_mark(U62(isNatKind(M),M,N)) ; } { Marked_active(U63(tt,M,N)) > Marked_mark(U64(isNatKind(N),M,N)) ; } { Marked_active(U64(tt,M,N)) > Marked_mark(s(plus(N,M))) ; } { Marked_active(plus(N,s(M))) > Marked_mark(U61(isNat(M),M,N)) ; } { Marked_active(plus(N,0)) > Marked_mark(U51(isNat(N),N)) ; } } === 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(U12(X1,X2,X3)) >= active(U12(mark(X1),X2,X3)) constraint: mark(isNatKind(X)) >= active(isNatKind(X)) constraint: mark(U11(X1,X2,X3)) >= active(U11(mark(X1),X2,X3)) constraint: mark(tt) >= active(tt) constraint: mark(U13(X1,X2,X3)) >= active(U13(mark(X1),X2,X3)) constraint: mark(U14(X1,X2,X3)) >= active(U14(mark(X1),X2,X3)) constraint: mark(U15(X1,X2)) >= active(U15(mark(X1),X2)) constraint: mark(isNat(X)) >= active(isNat(X)) constraint: mark(U16(X)) >= active(U16(mark(X))) constraint: mark(U22(X1,X2)) >= active(U22(mark(X1),X2)) constraint: mark(U21(X1,X2)) >= active(U21(mark(X1),X2)) constraint: mark(U23(X)) >= active(U23(mark(X))) constraint: mark(U32(X)) >= active(U32(mark(X))) constraint: mark(U31(X1,X2)) >= active(U31(mark(X1),X2)) constraint: mark(U41(X)) >= active(U41(mark(X))) constraint: mark(U52(X1,X2)) >= active(U52(mark(X1),X2)) constraint: mark(U51(X1,X2)) >= active(U51(mark(X1),X2)) constraint: mark(U62(X1,X2,X3)) >= active(U62(mark(X1),X2,X3)) constraint: mark(U61(X1,X2,X3)) >= active(U61(mark(X1),X2,X3)) constraint: mark(U63(X1,X2,X3)) >= active(U63(mark(X1),X2,X3)) constraint: mark(U64(X1,X2,X3)) >= active(U64(mark(X1),X2,X3)) constraint: mark(s(X)) >= active(s(mark(X))) constraint: mark(plus(X1,X2)) >= active(plus(mark(X1),mark(X2))) constraint: mark(0) >= active(0) constraint: U12(mark(X1),X2,X3) >= U12(X1,X2,X3) constraint: U12(active(X1),X2,X3) >= U12(X1,X2,X3) constraint: U12(X1,mark(X2),X3) >= U12(X1,X2,X3) constraint: U12(X1,active(X2),X3) >= U12(X1,X2,X3) constraint: U12(X1,X2,mark(X3)) >= U12(X1,X2,X3) constraint: U12(X1,X2,active(X3)) >= U12(X1,X2,X3) constraint: isNatKind(mark(X)) >= isNatKind(X) constraint: isNatKind(active(X)) >= isNatKind(X) constraint: active(U12(tt,V1,V2)) >= mark(U13(isNatKind(V2),V1,V2)) constraint: active(isNatKind(s(V1))) >= mark(U41(isNatKind(V1))) constraint: active(isNatKind(plus(V1,V2))) >= mark(U31(isNatKind(V1),V2)) constraint: active(isNatKind(0)) >= mark(tt) constraint: active(U11(tt,V1,V2)) >= mark(U12(isNatKind(V1),V1,V2)) constraint: active(U13(tt,V1,V2)) >= mark(U14(isNatKind(V2),V1,V2)) constraint: active(U14(tt,V1,V2)) >= mark(U15(isNat(V1),V2)) constraint: active(U15(tt,V2)) >= mark(U16(isNat(V2))) constraint: active(isNat(s(V1))) >= mark(U21(isNatKind(V1),V1)) constraint: active(isNat(plus(V1,V2))) >= mark(U11(isNatKind(V1),V1,V2)) constraint: active(isNat(0)) >= mark(tt) constraint: active(U16(tt)) >= mark(tt) constraint: active(U22(tt,V1)) >= mark(U23(isNat(V1))) constraint: active(U21(tt,V1)) >= mark(U22(isNatKind(V1),V1)) constraint: active(U23(tt)) >= mark(tt) constraint: active(U32(tt)) >= mark(tt) constraint: active(U31(tt,V2)) >= mark(U32(isNatKind(V2))) constraint: active(U41(tt)) >= mark(tt) constraint: active(U52(tt,N)) >= mark(N) constraint: active(U51(tt,N)) >= mark(U52(isNatKind(N),N)) constraint: active(U62(tt,M,N)) >= mark(U63(isNat(N),M,N)) constraint: active(U61(tt,M,N)) >= mark(U62(isNatKind(M),M,N)) constraint: active(U63(tt,M,N)) >= mark(U64(isNatKind(N),M,N)) constraint: active(U64(tt,M,N)) >= mark(s(plus(N,M))) constraint: active(plus(N,s(M))) >= mark(U61(isNat(M),M,N)) constraint: active(plus(N,0)) >= mark(U51(isNat(N),N)) constraint: U11(mark(X1),X2,X3) >= U11(X1,X2,X3) constraint: U11(active(X1),X2,X3) >= U11(X1,X2,X3) constraint: U11(X1,mark(X2),X3) >= U11(X1,X2,X3) constraint: U11(X1,active(X2),X3) >= U11(X1,X2,X3) constraint: U11(X1,X2,mark(X3)) >= U11(X1,X2,X3) constraint: U11(X1,X2,active(X3)) >= U11(X1,X2,X3) constraint: U13(mark(X1),X2,X3) >= U13(X1,X2,X3) constraint: U13(active(X1),X2,X3) >= U13(X1,X2,X3) constraint: U13(X1,mark(X2),X3) >= U13(X1,X2,X3) constraint: U13(X1,active(X2),X3) >= U13(X1,X2,X3) constraint: U13(X1,X2,mark(X3)) >= U13(X1,X2,X3) constraint: U13(X1,X2,active(X3)) >= U13(X1,X2,X3) constraint: U14(mark(X1),X2,X3) >= U14(X1,X2,X3) constraint: U14(active(X1),X2,X3) >= U14(X1,X2,X3) constraint: U14(X1,mark(X2),X3) >= U14(X1,X2,X3) constraint: U14(X1,active(X2),X3) >= U14(X1,X2,X3) constraint: U14(X1,X2,mark(X3)) >= U14(X1,X2,X3) constraint: U14(X1,X2,active(X3)) >= U14(X1,X2,X3) constraint: U15(mark(X1),X2) >= U15(X1,X2) constraint: U15(active(X1),X2) >= U15(X1,X2) constraint: U15(X1,mark(X2)) >= U15(X1,X2) constraint: U15(X1,active(X2)) >= U15(X1,X2) constraint: isNat(mark(X)) >= isNat(X) constraint: isNat(active(X)) >= isNat(X) constraint: U16(mark(X)) >= U16(X) constraint: U16(active(X)) >= U16(X) constraint: U22(mark(X1),X2) >= U22(X1,X2) constraint: U22(active(X1),X2) >= U22(X1,X2) constraint: U22(X1,mark(X2)) >= U22(X1,X2) constraint: U22(X1,active(X2)) >= U22(X1,X2) 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: U23(mark(X)) >= U23(X) constraint: U23(active(X)) >= U23(X) constraint: U32(mark(X)) >= U32(X) constraint: U32(active(X)) >= U32(X) constraint: U31(mark(X1),X2) >= U31(X1,X2) constraint: U31(active(X1),X2) >= U31(X1,X2) constraint: U31(X1,mark(X2)) >= U31(X1,X2) constraint: U31(X1,active(X2)) >= U31(X1,X2) constraint: U41(mark(X)) >= U41(X) constraint: U41(active(X)) >= U41(X) constraint: U52(mark(X1),X2) >= U52(X1,X2) constraint: U52(active(X1),X2) >= U52(X1,X2) constraint: U52(X1,mark(X2)) >= U52(X1,X2) constraint: U52(X1,active(X2)) >= U52(X1,X2) 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: U62(mark(X1),X2,X3) >= U62(X1,X2,X3) constraint: U62(active(X1),X2,X3) >= U62(X1,X2,X3) constraint: U62(X1,mark(X2),X3) >= U62(X1,X2,X3) constraint: U62(X1,active(X2),X3) >= U62(X1,X2,X3) constraint: U62(X1,X2,mark(X3)) >= U62(X1,X2,X3) constraint: U62(X1,X2,active(X3)) >= U62(X1,X2,X3) constraint: U61(mark(X1),X2,X3) >= U61(X1,X2,X3) constraint: U61(active(X1),X2,X3) >= U61(X1,X2,X3) constraint: U61(X1,mark(X2),X3) >= U61(X1,X2,X3) constraint: U61(X1,active(X2),X3) >= U61(X1,X2,X3) constraint: U61(X1,X2,mark(X3)) >= U61(X1,X2,X3) constraint: U61(X1,X2,active(X3)) >= U61(X1,X2,X3) constraint: U63(mark(X1),X2,X3) >= U63(X1,X2,X3) constraint: U63(active(X1),X2,X3) >= U63(X1,X2,X3) constraint: U63(X1,mark(X2),X3) >= U63(X1,X2,X3) constraint: U63(X1,active(X2),X3) >= U63(X1,X2,X3) constraint: U63(X1,X2,mark(X3)) >= U63(X1,X2,X3) constraint: U63(X1,X2,active(X3)) >= U63(X1,X2,X3) constraint: U64(mark(X1),X2,X3) >= U64(X1,X2,X3) constraint: U64(active(X1),X2,X3) >= U64(X1,X2,X3) constraint: U64(X1,mark(X2),X3) >= U64(X1,X2,X3) constraint: U64(X1,active(X2),X3) >= U64(X1,X2,X3) constraint: U64(X1,X2,mark(X3)) >= U64(X1,X2,X3) constraint: U64(X1,X2,active(X3)) >= U64(X1,X2,X3) constraint: s(mark(X)) >= s(X) constraint: s(active(X)) >= s(X) constraint: plus(mark(X1),X2) >= plus(X1,X2) constraint: plus(active(X1),X2) >= plus(X1,X2) constraint: plus(X1,mark(X2)) >= plus(X1,X2) constraint: plus(X1,active(X2)) >= plus(X1,X2) constraint: Marked_mark(U12(X1,X2,X3)) >= Marked_mark(X1) constraint: Marked_mark(U12(X1,X2,X3)) >= Marked_active(U12(mark(X1),X2,X3)) constraint: Marked_mark(isNatKind(X)) >= Marked_active(isNatKind(X)) constraint: Marked_mark(U11(X1,X2,X3)) >= Marked_mark(X1) constraint: Marked_mark(U11(X1,X2,X3)) >= Marked_active(U11(mark(X1),X2,X3)) constraint: Marked_mark(U13(X1,X2,X3)) >= Marked_mark(X1) constraint: Marked_mark(U13(X1,X2,X3)) >= Marked_active(U13(mark(X1),X2,X3)) constraint: Marked_mark(U14(X1,X2,X3)) >= Marked_mark(X1) constraint: Marked_mark(U14(X1,X2,X3)) >= Marked_active(U14(mark(X1),X2,X3)) constraint: Marked_mark(U15(X1,X2)) >= Marked_mark(X1) constraint: Marked_mark(U15(X1,X2)) >= Marked_active(U15(mark(X1),X2)) constraint: Marked_mark(isNat(X)) >= Marked_active(isNat(X)) constraint: Marked_mark(U16(X)) >= Marked_mark(X) constraint: Marked_mark(U16(X)) >= Marked_active(U16(mark(X))) constraint: Marked_mark(U22(X1,X2)) >= Marked_mark(X1) constraint: Marked_mark(U22(X1,X2)) >= Marked_active(U22(mark(X1),X2)) constraint: Marked_mark(U21(X1,X2)) >= Marked_mark(X1) constraint: Marked_mark(U21(X1,X2)) >= Marked_active(U21(mark(X1),X2)) constraint: Marked_mark(U23(X)) >= Marked_mark(X) constraint: Marked_mark(U23(X)) >= Marked_active(U23(mark(X))) constraint: Marked_mark(U32(X)) >= Marked_mark(X) constraint: Marked_mark(U32(X)) >= Marked_active(U32(mark(X))) constraint: Marked_mark(U31(X1,X2)) >= Marked_mark(X1) constraint: Marked_mark(U31(X1,X2)) >= Marked_active(U31(mark(X1),X2)) constraint: Marked_mark(U41(X)) >= Marked_mark(X) constraint: Marked_mark(U41(X)) >= Marked_active(U41(mark(X))) constraint: Marked_mark(U52(X1,X2)) >= Marked_mark(X1) constraint: Marked_mark(U52(X1,X2)) >= Marked_active(U52(mark(X1),X2)) constraint: Marked_mark(U51(X1,X2)) >= Marked_mark(X1) constraint: Marked_mark(U51(X1,X2)) >= Marked_active(U51(mark(X1),X2)) constraint: Marked_mark(U62(X1,X2,X3)) >= Marked_mark(X1) constraint: Marked_mark(U62(X1,X2,X3)) >= Marked_active(U62(mark(X1),X2,X3)) constraint: Marked_mark(U61(X1,X2,X3)) >= Marked_mark(X1) constraint: Marked_mark(U61(X1,X2,X3)) >= Marked_active(U61(mark(X1),X2,X3)) constraint: Marked_mark(U63(X1,X2,X3)) >= Marked_mark(X1) constraint: Marked_mark(U63(X1,X2,X3)) >= Marked_active(U63(mark(X1),X2,X3)) constraint: Marked_mark(U64(X1,X2,X3)) >= Marked_mark(X1) constraint: Marked_mark(U64(X1,X2,X3)) >= Marked_active(U64(mark(X1),X2,X3)) constraint: Marked_mark(s(X)) >= Marked_mark(X) constraint: Marked_mark(s(X)) >= Marked_active(s(mark(X))) constraint: Marked_mark(plus(X1,X2)) >= Marked_mark(X1) constraint: Marked_mark(plus(X1,X2)) >= Marked_mark(X2) constraint: Marked_mark(plus(X1,X2)) >= Marked_active(plus(mark(X1),mark(X2))) constraint: Marked_active(U12(tt,V1,V2)) >= Marked_mark(U13(isNatKind(V2), V1,V2)) constraint: Marked_active(isNatKind(s(V1))) >= Marked_mark(U41(isNatKind(V1))) constraint: Marked_active(isNatKind(plus(V1,V2))) >= Marked_mark(U31( isNatKind( V1), V2)) constraint: Marked_active(U11(tt,V1,V2)) >= Marked_mark(U12(isNatKind(V1), V1,V2)) constraint: Marked_active(U13(tt,V1,V2)) >= Marked_mark(U14(isNatKind(V2), V1,V2)) constraint: Marked_active(U14(tt,V1,V2)) >= Marked_mark(U15(isNat(V1),V2)) constraint: Marked_active(U15(tt,V2)) >= Marked_mark(U16(isNat(V2))) constraint: Marked_active(isNat(s(V1))) >= Marked_mark(U21(isNatKind(V1),V1)) constraint: Marked_active(isNat(plus(V1,V2))) >= Marked_mark(U11(isNatKind(V1), V1,V2)) constraint: Marked_active(U22(tt,V1)) >= Marked_mark(U23(isNat(V1))) constraint: Marked_active(U21(tt,V1)) >= Marked_mark(U22(isNatKind(V1),V1)) constraint: Marked_active(U31(tt,V2)) >= Marked_mark(U32(isNatKind(V2))) constraint: Marked_active(U52(tt,N)) >= Marked_mark(N) constraint: Marked_active(U51(tt,N)) >= Marked_mark(U52(isNatKind(N),N)) constraint: Marked_active(U62(tt,M,N)) >= Marked_mark(U63(isNat(N),M,N)) constraint: Marked_active(U61(tt,M,N)) >= Marked_mark(U62(isNatKind(M),M,N)) constraint: Marked_active(U63(tt,M,N)) >= Marked_mark(U64(isNatKind(N),M,N)) constraint: Marked_active(U64(tt,M,N)) >= Marked_mark(s(plus(N,M))) constraint: Marked_active(plus(N,s(M))) >= Marked_mark(U61(isNat(M),M,N)) constraint: Marked_active(plus(N,0)) >= Marked_mark(U51(isNat(N),N)) APPLY CRITERIA (Subterm criterion) ST: Marked_U11 -> 3 APPLY CRITERIA (Subterm criterion) ST: Marked_U12 -> 3 APPLY CRITERIA (Subterm criterion) ST: Marked_isNatKind -> 1 APPLY CRITERIA (Subterm criterion) ST: Marked_U13 -> 3 APPLY CRITERIA (Subterm criterion) ST: Marked_U14 -> 3 APPLY CRITERIA (Subterm criterion) ST: Marked_U15 -> 2 APPLY CRITERIA (Subterm criterion) ST: Marked_isNat -> 1 APPLY CRITERIA (Subterm criterion) ST: Marked_U16 -> 1 APPLY CRITERIA (Subterm criterion) ST: Marked_U21 -> 2 APPLY CRITERIA (Subterm criterion) ST: Marked_U22 -> 2 APPLY CRITERIA (Subterm criterion) ST: Marked_U23 -> 1 APPLY CRITERIA (Subterm criterion) ST: Marked_U31 -> 2 APPLY CRITERIA (Subterm criterion) ST: Marked_U32 -> 1 APPLY CRITERIA (Subterm criterion) ST: Marked_U41 -> 1 APPLY CRITERIA (Subterm criterion) ST: Marked_U51 -> 2 APPLY CRITERIA (Subterm criterion) ST: Marked_U52 -> 2 APPLY CRITERIA (Subterm criterion) ST: Marked_U61 -> 3 APPLY CRITERIA (Subterm criterion) ST: Marked_U62 -> 3 APPLY CRITERIA (Subterm criterion) ST: Marked_U63 -> 3 APPLY CRITERIA (Subterm criterion) ST: Marked_U64 -> 3 APPLY CRITERIA (Subterm criterion) ST: Marked_s -> 1 APPLY CRITERIA (Subterm criterion) ST: Marked_plus -> 2 APPLY CRITERIA (Graph splitting) Found 1 components: { --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> } APPLY CRITERIA (Subterm criterion) APPLY CRITERIA (Choosing graph) Trying to solve the following constraints: { mark(U12(X1,X2,X3)) >= active(U12(mark(X1),X2,X3)) ; mark(isNatKind(X)) >= active(isNatKind(X)) ; mark(U11(X1,X2,X3)) >= active(U11(mark(X1),X2,X3)) ; mark(tt) >= active(tt) ; mark(U13(X1,X2,X3)) >= active(U13(mark(X1),X2,X3)) ; mark(U14(X1,X2,X3)) >= active(U14(mark(X1),X2,X3)) ; mark(U15(X1,X2)) >= active(U15(mark(X1),X2)) ; mark(isNat(X)) >= active(isNat(X)) ; mark(U16(X)) >= active(U16(mark(X))) ; mark(U22(X1,X2)) >= active(U22(mark(X1),X2)) ; mark(U21(X1,X2)) >= active(U21(mark(X1),X2)) ; mark(U23(X)) >= active(U23(mark(X))) ; mark(U32(X)) >= active(U32(mark(X))) ; mark(U31(X1,X2)) >= active(U31(mark(X1),X2)) ; mark(U41(X)) >= active(U41(mark(X))) ; mark(U52(X1,X2)) >= active(U52(mark(X1),X2)) ; mark(U51(X1,X2)) >= active(U51(mark(X1),X2)) ; mark(U62(X1,X2,X3)) >= active(U62(mark(X1),X2,X3)) ; mark(U61(X1,X2,X3)) >= active(U61(mark(X1),X2,X3)) ; mark(U63(X1,X2,X3)) >= active(U63(mark(X1),X2,X3)) ; mark(U64(X1,X2,X3)) >= active(U64(mark(X1),X2,X3)) ; mark(s(X)) >= active(s(mark(X))) ; mark(plus(X1,X2)) >= active(plus(mark(X1),mark(X2))) ; mark(0) >= active(0) ; U12(mark(X1),X2,X3) >= U12(X1,X2,X3) ; U12(active(X1),X2,X3) >= U12(X1,X2,X3) ; U12(X1,mark(X2),X3) >= U12(X1,X2,X3) ; U12(X1,active(X2),X3) >= U12(X1,X2,X3) ; U12(X1,X2,mark(X3)) >= U12(X1,X2,X3) ; U12(X1,X2,active(X3)) >= U12(X1,X2,X3) ; isNatKind(mark(X)) >= isNatKind(X) ; isNatKind(active(X)) >= isNatKind(X) ; active(U12(tt,V1,V2)) >= mark(U13(isNatKind(V2),V1,V2)) ; active(isNatKind(s(V1))) >= mark(U41(isNatKind(V1))) ; active(isNatKind(plus(V1,V2))) >= mark(U31(isNatKind(V1),V2)) ; active(isNatKind(0)) >= mark(tt) ; active(U11(tt,V1,V2)) >= mark(U12(isNatKind(V1),V1,V2)) ; active(U13(tt,V1,V2)) >= mark(U14(isNatKind(V2),V1,V2)) ; active(U14(tt,V1,V2)) >= mark(U15(isNat(V1),V2)) ; active(U15(tt,V2)) >= mark(U16(isNat(V2))) ; active(isNat(s(V1))) >= mark(U21(isNatKind(V1),V1)) ; active(isNat(plus(V1,V2))) >= mark(U11(isNatKind(V1),V1,V2)) ; active(isNat(0)) >= mark(tt) ; active(U16(tt)) >= mark(tt) ; active(U22(tt,V1)) >= mark(U23(isNat(V1))) ; active(U21(tt,V1)) >= mark(U22(isNatKind(V1),V1)) ; active(U23(tt)) >= mark(tt) ; active(U32(tt)) >= mark(tt) ; active(U31(tt,V2)) >= mark(U32(isNatKind(V2))) ; active(U41(tt)) >= mark(tt) ; active(U52(tt,N)) >= mark(N) ; active(U51(tt,N)) >= mark(U52(isNatKind(N),N)) ; active(U62(tt,M,N)) >= mark(U63(isNat(N),M,N)) ; active(U61(tt,M,N)) >= mark(U62(isNatKind(M),M,N)) ; active(U63(tt,M,N)) >= mark(U64(isNatKind(N),M,N)) ; active(U64(tt,M,N)) >= mark(s(plus(N,M))) ; active(plus(N,s(M))) >= mark(U61(isNat(M),M,N)) ; active(plus(N,0)) >= mark(U51(isNat(N),N)) ; U11(mark(X1),X2,X3) >= U11(X1,X2,X3) ; U11(active(X1),X2,X3) >= U11(X1,X2,X3) ; U11(X1,mark(X2),X3) >= U11(X1,X2,X3) ; U11(X1,active(X2),X3) >= U11(X1,X2,X3) ; U11(X1,X2,mark(X3)) >= U11(X1,X2,X3) ; U11(X1,X2,active(X3)) >= U11(X1,X2,X3) ; U13(mark(X1),X2,X3) >= U13(X1,X2,X3) ; U13(active(X1),X2,X3) >= U13(X1,X2,X3) ; U13(X1,mark(X2),X3) >= U13(X1,X2,X3) ; U13(X1,active(X2),X3) >= U13(X1,X2,X3) ; U13(X1,X2,mark(X3)) >= U13(X1,X2,X3) ; U13(X1,X2,active(X3)) >= U13(X1,X2,X3) ; U14(mark(X1),X2,X3) >= U14(X1,X2,X3) ; U14(active(X1),X2,X3) >= U14(X1,X2,X3) ; U14(X1,mark(X2),X3) >= U14(X1,X2,X3) ; U14(X1,active(X2),X3) >= U14(X1,X2,X3) ; U14(X1,X2,mark(X3)) >= U14(X1,X2,X3) ; U14(X1,X2,active(X3)) >= U14(X1,X2,X3) ; U15(mark(X1),X2) >= U15(X1,X2) ; U15(active(X1),X2) >= U15(X1,X2) ; U15(X1,mark(X2)) >= U15(X1,X2) ; U15(X1,active(X2)) >= U15(X1,X2) ; isNat(mark(X)) >= isNat(X) ; isNat(active(X)) >= isNat(X) ; U16(mark(X)) >= U16(X) ; U16(active(X)) >= U16(X) ; U22(mark(X1),X2) >= U22(X1,X2) ; U22(active(X1),X2) >= U22(X1,X2) ; U22(X1,mark(X2)) >= U22(X1,X2) ; U22(X1,active(X2)) >= U22(X1,X2) ; 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) ; U23(mark(X)) >= U23(X) ; U23(active(X)) >= U23(X) ; U32(mark(X)) >= U32(X) ; U32(active(X)) >= U32(X) ; U31(mark(X1),X2) >= U31(X1,X2) ; U31(active(X1),X2) >= U31(X1,X2) ; U31(X1,mark(X2)) >= U31(X1,X2) ; U31(X1,active(X2)) >= U31(X1,X2) ; U41(mark(X)) >= U41(X) ; U41(active(X)) >= U41(X) ; U52(mark(X1),X2) >= U52(X1,X2) ; U52(active(X1),X2) >= U52(X1,X2) ; U52(X1,mark(X2)) >= U52(X1,X2) ; U52(X1,active(X2)) >= U52(X1,X2) ; 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) ; U62(mark(X1),X2,X3) >= U62(X1,X2,X3) ; U62(active(X1),X2,X3) >= U62(X1,X2,X3) ; U62(X1,mark(X2),X3) >= U62(X1,X2,X3) ; U62(X1,active(X2),X3) >= U62(X1,X2,X3) ; U62(X1,X2,mark(X3)) >= U62(X1,X2,X3) ; U62(X1,X2,active(X3)) >= U62(X1,X2,X3) ; U61(mark(X1),X2,X3) >= U61(X1,X2,X3) ; U61(active(X1),X2,X3) >= U61(X1,X2,X3) ; U61(X1,mark(X2),X3) >= U61(X1,X2,X3) ; U61(X1,active(X2),X3) >= U61(X1,X2,X3) ; U61(X1,X2,mark(X3)) >= U61(X1,X2,X3) ; U61(X1,X2,active(X3)) >= U61(X1,X2,X3) ; U63(mark(X1),X2,X3) >= U63(X1,X2,X3) ; U63(active(X1),X2,X3) >= U63(X1,X2,X3) ; U63(X1,mark(X2),X3) >= U63(X1,X2,X3) ; U63(X1,active(X2),X3) >= U63(X1,X2,X3) ; U63(X1,X2,mark(X3)) >= U63(X1,X2,X3) ; U63(X1,X2,active(X3)) >= U63(X1,X2,X3) ; U64(mark(X1),X2,X3) >= U64(X1,X2,X3) ; U64(active(X1),X2,X3) >= U64(X1,X2,X3) ; U64(X1,mark(X2),X3) >= U64(X1,X2,X3) ; U64(X1,active(X2),X3) >= U64(X1,X2,X3) ; U64(X1,X2,mark(X3)) >= U64(X1,X2,X3) ; U64(X1,X2,active(X3)) >= U64(X1,X2,X3) ; s(mark(X)) >= s(X) ; s(active(X)) >= s(X) ; plus(mark(X1),X2) >= plus(X1,X2) ; plus(active(X1),X2) >= plus(X1,X2) ; plus(X1,mark(X2)) >= plus(X1,X2) ; plus(X1,active(X2)) >= plus(X1,X2) ; Marked_mark(U12(X1,X2,X3)) >= Marked_mark(X1) ; Marked_mark(U12(X1,X2,X3)) >= Marked_active(U12(mark(X1),X2,X3)) ; Marked_mark(isNatKind(X)) >= Marked_active(isNatKind(X)) ; Marked_mark(U11(X1,X2,X3)) >= Marked_mark(X1) ; Marked_mark(U11(X1,X2,X3)) >= Marked_active(U11(mark(X1),X2,X3)) ; Marked_mark(U13(X1,X2,X3)) >= Marked_mark(X1) ; Marked_mark(U13(X1,X2,X3)) >= Marked_active(U13(mark(X1),X2,X3)) ; Marked_mark(U14(X1,X2,X3)) >= Marked_mark(X1) ; Marked_mark(U14(X1,X2,X3)) >= Marked_active(U14(mark(X1),X2,X3)) ; Marked_mark(U15(X1,X2)) >= Marked_mark(X1) ; Marked_mark(U15(X1,X2)) >= Marked_active(U15(mark(X1),X2)) ; Marked_mark(isNat(X)) >= Marked_active(isNat(X)) ; Marked_mark(U16(X)) >= Marked_mark(X) ; Marked_mark(U16(X)) >= Marked_active(U16(mark(X))) ; Marked_mark(U22(X1,X2)) >= Marked_mark(X1) ; Marked_mark(U22(X1,X2)) >= Marked_active(U22(mark(X1),X2)) ; Marked_mark(U21(X1,X2)) >= Marked_mark(X1) ; Marked_mark(U21(X1,X2)) >= Marked_active(U21(mark(X1),X2)) ; Marked_mark(U23(X)) >= Marked_mark(X) ; Marked_mark(U23(X)) >= Marked_active(U23(mark(X))) ; Marked_mark(U32(X)) >= Marked_mark(X) ; Marked_mark(U32(X)) >= Marked_active(U32(mark(X))) ; Marked_mark(U31(X1,X2)) >= Marked_mark(X1) ; Marked_mark(U31(X1,X2)) >= Marked_active(U31(mark(X1),X2)) ; Marked_mark(U41(X)) >= Marked_mark(X) ; Marked_mark(U41(X)) >= Marked_active(U41(mark(X))) ; Marked_mark(U52(X1,X2)) >= Marked_mark(X1) ; Marked_mark(U52(X1,X2)) >= Marked_active(U52(mark(X1),X2)) ; Marked_mark(U51(X1,X2)) >= Marked_mark(X1) ; Marked_mark(U51(X1,X2)) >= Marked_active(U51(mark(X1),X2)) ; Marked_mark(U62(X1,X2,X3)) >= Marked_mark(X1) ; Marked_mark(U62(X1,X2,X3)) >= Marked_active(U62(mark(X1),X2,X3)) ; Marked_mark(U61(X1,X2,X3)) >= Marked_mark(X1) ; Marked_mark(U61(X1,X2,X3)) >= Marked_active(U61(mark(X1),X2,X3)) ; Marked_mark(U63(X1,X2,X3)) >= Marked_mark(X1) ; Marked_mark(U63(X1,X2,X3)) >= Marked_active(U63(mark(X1),X2,X3)) ; Marked_mark(U64(X1,X2,X3)) >= Marked_mark(X1) ; Marked_mark(U64(X1,X2,X3)) >= Marked_active(U64(mark(X1),X2,X3)) ; Marked_mark(s(X)) >= Marked_mark(X) ; Marked_mark(s(X)) >= Marked_active(s(mark(X))) ; Marked_mark(plus(X1,X2)) >= Marked_mark(X1) ; Marked_mark(plus(X1,X2)) >= Marked_mark(X2) ; Marked_mark(plus(X1,X2)) >= Marked_active(plus(mark(X1),mark(X2))) ; Marked_active(U12(tt,V1,V2)) >= Marked_mark(U13(isNatKind(V2),V1,V2)) ; Marked_active(isNatKind(s(V1))) >= Marked_mark(U41(isNatKind(V1))) ; Marked_active(isNatKind(plus(V1,V2))) >= Marked_mark(U31(isNatKind(V1),V2)) ; Marked_active(U11(tt,V1,V2)) >= Marked_mark(U12(isNatKind(V1),V1,V2)) ; Marked_active(U13(tt,V1,V2)) >= Marked_mark(U14(isNatKind(V2),V1,V2)) ; Marked_active(U14(tt,V1,V2)) >= Marked_mark(U15(isNat(V1),V2)) ; Marked_active(U15(tt,V2)) >= Marked_mark(U16(isNat(V2))) ; Marked_active(isNat(s(V1))) >= Marked_mark(U21(isNatKind(V1),V1)) ; Marked_active(isNat(plus(V1,V2))) >= Marked_mark(U11(isNatKind(V1),V1,V2)) ; Marked_active(U22(tt,V1)) >= Marked_mark(U23(isNat(V1))) ; Marked_active(U21(tt,V1)) >= Marked_mark(U22(isNatKind(V1),V1)) ; Marked_active(U31(tt,V2)) >= Marked_mark(U32(isNatKind(V2))) ; Marked_active(U52(tt,N)) >= Marked_mark(N) ; Marked_active(U51(tt,N)) >= Marked_mark(U52(isNatKind(N),N)) ; Marked_active(U62(tt,M,N)) >= Marked_mark(U63(isNat(N),M,N)) ; Marked_active(U61(tt,M,N)) >= Marked_mark(U62(isNatKind(M),M,N)) ; Marked_active(U63(tt,M,N)) >= Marked_mark(U64(isNatKind(N),M,N)) ; Marked_active(U64(tt,M,N)) >= Marked_mark(s(plus(N,M))) ; Marked_active(plus(N,s(M))) >= Marked_mark(U61(isNat(M),M,N)) ; } + Disjunctions:{ { Marked_mark(U12(X1,X2,X3)) > Marked_mark(X1) ; } { Marked_mark(U12(X1,X2,X3)) > Marked_active(U12(mark(X1),X2,X3)) ; } { Marked_mark(isNatKind(X)) > Marked_active(isNatKind(X)) ; } { Marked_mark(U11(X1,X2,X3)) > Marked_mark(X1) ; } { Marked_mark(U11(X1,X2,X3)) > Marked_active(U11(mark(X1),X2,X3)) ; } { Marked_mark(U13(X1,X2,X3)) > Marked_mark(X1) ; } { Marked_mark(U13(X1,X2,X3)) > Marked_active(U13(mark(X1),X2,X3)) ; } { Marked_mark(U14(X1,X2,X3)) > Marked_mark(X1) ; } { Marked_mark(U14(X1,X2,X3)) > Marked_active(U14(mark(X1),X2,X3)) ; } { Marked_mark(U15(X1,X2)) > Marked_mark(X1) ; } { Marked_mark(U15(X1,X2)) > Marked_active(U15(mark(X1),X2)) ; } { Marked_mark(isNat(X)) > Marked_active(isNat(X)) ; } { Marked_mark(U16(X)) > Marked_mark(X) ; } { Marked_mark(U16(X)) > Marked_active(U16(mark(X))) ; } { Marked_mark(U22(X1,X2)) > Marked_mark(X1) ; } { Marked_mark(U22(X1,X2)) > Marked_active(U22(mark(X1),X2)) ; } { Marked_mark(U21(X1,X2)) > Marked_mark(X1) ; } { Marked_mark(U21(X1,X2)) > Marked_active(U21(mark(X1),X2)) ; } { Marked_mark(U23(X)) > Marked_mark(X) ; } { Marked_mark(U23(X)) > Marked_active(U23(mark(X))) ; } { Marked_mark(U32(X)) > Marked_mark(X) ; } { Marked_mark(U32(X)) > Marked_active(U32(mark(X))) ; } { Marked_mark(U31(X1,X2)) > Marked_mark(X1) ; } { Marked_mark(U31(X1,X2)) > Marked_active(U31(mark(X1),X2)) ; } { Marked_mark(U41(X)) > Marked_mark(X) ; } { Marked_mark(U41(X)) > Marked_active(U41(mark(X))) ; } { Marked_mark(U52(X1,X2)) > Marked_mark(X1) ; } { Marked_mark(U52(X1,X2)) > Marked_active(U52(mark(X1),X2)) ; } { Marked_mark(U51(X1,X2)) > Marked_mark(X1) ; } { Marked_mark(U51(X1,X2)) > Marked_active(U51(mark(X1),X2)) ; } { Marked_mark(U62(X1,X2,X3)) > Marked_mark(X1) ; } { Marked_mark(U62(X1,X2,X3)) > Marked_active(U62(mark(X1),X2,X3)) ; } { Marked_mark(U61(X1,X2,X3)) > Marked_mark(X1) ; } { Marked_mark(U61(X1,X2,X3)) > Marked_active(U61(mark(X1),X2,X3)) ; } { Marked_mark(U63(X1,X2,X3)) > Marked_mark(X1) ; } { Marked_mark(U63(X1,X2,X3)) > Marked_active(U63(mark(X1),X2,X3)) ; } { Marked_mark(U64(X1,X2,X3)) > Marked_mark(X1) ; } { Marked_mark(U64(X1,X2,X3)) > Marked_active(U64(mark(X1),X2,X3)) ; } { Marked_mark(s(X)) > Marked_mark(X) ; } { Marked_mark(s(X)) > Marked_active(s(mark(X))) ; } { Marked_mark(plus(X1,X2)) > Marked_mark(X1) ; } { Marked_mark(plus(X1,X2)) > Marked_mark(X2) ; } { Marked_mark(plus(X1,X2)) > Marked_active(plus(mark(X1),mark(X2))) ; } { Marked_active(U12(tt,V1,V2)) > Marked_mark(U13(isNatKind(V2),V1,V2)) ; } { Marked_active(isNatKind(s(V1))) > Marked_mark(U41(isNatKind(V1))) ; } { Marked_active(isNatKind(plus(V1,V2))) > Marked_mark(U31(isNatKind(V1),V2)) ; } { Marked_active(U11(tt,V1,V2)) > Marked_mark(U12(isNatKind(V1),V1,V2)) ; } { Marked_active(U13(tt,V1,V2)) > Marked_mark(U14(isNatKind(V2),V1,V2)) ; } { Marked_active(U14(tt,V1,V2)) > Marked_mark(U15(isNat(V1),V2)) ; } { Marked_active(U15(tt,V2)) > Marked_mark(U16(isNat(V2))) ; } { Marked_active(isNat(s(V1))) > Marked_mark(U21(isNatKind(V1),V1)) ; } { Marked_active(isNat(plus(V1,V2))) > Marked_mark(U11(isNatKind(V1),V1,V2)) ; } { Marked_active(U22(tt,V1)) > Marked_mark(U23(isNat(V1))) ; } { Marked_active(U21(tt,V1)) > Marked_mark(U22(isNatKind(V1),V1)) ; } { Marked_active(U31(tt,V2)) > Marked_mark(U32(isNatKind(V2))) ; } { Marked_active(U52(tt,N)) > Marked_mark(N) ; } { Marked_active(U51(tt,N)) > Marked_mark(U52(isNatKind(N),N)) ; } { Marked_active(U62(tt,M,N)) > Marked_mark(U63(isNat(N),M,N)) ; } { Marked_active(U61(tt,M,N)) > Marked_mark(U62(isNatKind(M),M,N)) ; } { Marked_active(U63(tt,M,N)) > Marked_mark(U64(isNatKind(N),M,N)) ; } { Marked_active(U64(tt,M,N)) > Marked_mark(s(plus(N,M))) ; } { Marked_active(plus(N,s(M))) > Marked_mark(U61(isNat(M),M,N)) ; } } === 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(U12(X1,X2,X3)) >= active(U12(mark(X1),X2,X3)) constraint: mark(isNatKind(X)) >= active(isNatKind(X)) constraint: mark(U11(X1,X2,X3)) >= active(U11(mark(X1),X2,X3)) constraint: mark(tt) >= active(tt) constraint: mark(U13(X1,X2,X3)) >= active(U13(mark(X1),X2,X3)) constraint: mark(U14(X1,X2,X3)) >= active(U14(mark(X1),X2,X3)) constraint: mark(U15(X1,X2)) >= active(U15(mark(X1),X2)) constraint: mark(isNat(X)) >= active(isNat(X)) constraint: mark(U16(X)) >= active(U16(mark(X))) constraint: mark(U22(X1,X2)) >= active(U22(mark(X1),X2)) constraint: mark(U21(X1,X2)) >= active(U21(mark(X1),X2)) constraint: mark(U23(X)) >= active(U23(mark(X))) constraint: mark(U32(X)) >= active(U32(mark(X))) constraint: mark(U31(X1,X2)) >= active(U31(mark(X1),X2)) constraint: mark(U41(X)) >= active(U41(mark(X))) constraint: mark(U52(X1,X2)) >= active(U52(mark(X1),X2)) constraint: mark(U51(X1,X2)) >= active(U51(mark(X1),X2)) constraint: mark(U62(X1,X2,X3)) >= active(U62(mark(X1),X2,X3)) constraint: mark(U61(X1,X2,X3)) >= active(U61(mark(X1),X2,X3)) constraint: mark(U63(X1,X2,X3)) >= active(U63(mark(X1),X2,X3)) constraint: mark(U64(X1,X2,X3)) >= active(U64(mark(X1),X2,X3)) constraint: mark(s(X)) >= active(s(mark(X))) constraint: mark(plus(X1,X2)) >= active(plus(mark(X1),mark(X2))) constraint: mark(0) >= active(0) constraint: U12(mark(X1),X2,X3) >= U12(X1,X2,X3) constraint: U12(active(X1),X2,X3) >= U12(X1,X2,X3) constraint: U12(X1,mark(X2),X3) >= U12(X1,X2,X3) constraint: U12(X1,active(X2),X3) >= U12(X1,X2,X3) constraint: U12(X1,X2,mark(X3)) >= U12(X1,X2,X3) constraint: U12(X1,X2,active(X3)) >= U12(X1,X2,X3) constraint: isNatKind(mark(X)) >= isNatKind(X) constraint: isNatKind(active(X)) >= isNatKind(X) constraint: active(U12(tt,V1,V2)) >= mark(U13(isNatKind(V2),V1,V2)) constraint: active(isNatKind(s(V1))) >= mark(U41(isNatKind(V1))) constraint: active(isNatKind(plus(V1,V2))) >= mark(U31(isNatKind(V1),V2)) constraint: active(isNatKind(0)) >= mark(tt) constraint: active(U11(tt,V1,V2)) >= mark(U12(isNatKind(V1),V1,V2)) constraint: active(U13(tt,V1,V2)) >= mark(U14(isNatKind(V2),V1,V2)) constraint: active(U14(tt,V1,V2)) >= mark(U15(isNat(V1),V2)) constraint: active(U15(tt,V2)) >= mark(U16(isNat(V2))) constraint: active(isNat(s(V1))) >= mark(U21(isNatKind(V1),V1)) constraint: active(isNat(plus(V1,V2))) >= mark(U11(isNatKind(V1),V1,V2)) constraint: active(isNat(0)) >= mark(tt) constraint: active(U16(tt)) >= mark(tt) constraint: active(U22(tt,V1)) >= mark(U23(isNat(V1))) constraint: active(U21(tt,V1)) >= mark(U22(isNatKind(V1),V1)) constraint: active(U23(tt)) >= mark(tt) constraint: active(U32(tt)) >= mark(tt) constraint: active(U31(tt,V2)) >= mark(U32(isNatKind(V2))) constraint: active(U41(tt)) >= mark(tt) constraint: active(U52(tt,N)) >= mark(N) constraint: active(U51(tt,N)) >= mark(U52(isNatKind(N),N)) constraint: active(U62(tt,M,N)) >= mark(U63(isNat(N),M,N)) constraint: active(U61(tt,M,N)) >= mark(U62(isNatKind(M),M,N)) constraint: active(U63(tt,M,N)) >= mark(U64(isNatKind(N),M,N)) constraint: active(U64(tt,M,N)) >= mark(s(plus(N,M))) constraint: active(plus(N,s(M))) >= mark(U61(isNat(M),M,N)) constraint: active(plus(N,0)) >= mark(U51(isNat(N),N)) constraint: U11(mark(X1),X2,X3) >= U11(X1,X2,X3) constraint: U11(active(X1),X2,X3) >= U11(X1,X2,X3) constraint: U11(X1,mark(X2),X3) >= U11(X1,X2,X3) constraint: U11(X1,active(X2),X3) >= U11(X1,X2,X3) constraint: U11(X1,X2,mark(X3)) >= U11(X1,X2,X3) constraint: U11(X1,X2,active(X3)) >= U11(X1,X2,X3) constraint: U13(mark(X1),X2,X3) >= U13(X1,X2,X3) constraint: U13(active(X1),X2,X3) >= U13(X1,X2,X3) constraint: U13(X1,mark(X2),X3) >= U13(X1,X2,X3) constraint: U13(X1,active(X2),X3) >= U13(X1,X2,X3) constraint: U13(X1,X2,mark(X3)) >= U13(X1,X2,X3) constraint: U13(X1,X2,active(X3)) >= U13(X1,X2,X3) constraint: U14(mark(X1),X2,X3) >= U14(X1,X2,X3) constraint: U14(active(X1),X2,X3) >= U14(X1,X2,X3) constraint: U14(X1,mark(X2),X3) >= U14(X1,X2,X3) constraint: U14(X1,active(X2),X3) >= U14(X1,X2,X3) constraint: U14(X1,X2,mark(X3)) >= U14(X1,X2,X3) constraint: U14(X1,X2,active(X3)) >= U14(X1,X2,X3) constraint: U15(mark(X1),X2) >= U15(X1,X2) constraint: U15(active(X1),X2) >= U15(X1,X2) constraint: U15(X1,mark(X2)) >= U15(X1,X2) constraint: U15(X1,active(X2)) >= U15(X1,X2) constraint: isNat(mark(X)) >= isNat(X) constraint: isNat(active(X)) >= isNat(X) constraint: U16(mark(X)) >= U16(X) constraint: U16(active(X)) >= U16(X) constraint: U22(mark(X1),X2) >= U22(X1,X2) constraint: U22(active(X1),X2) >= U22(X1,X2) constraint: U22(X1,mark(X2)) >= U22(X1,X2) constraint: U22(X1,active(X2)) >= U22(X1,X2) 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: U23(mark(X)) >= U23(X) constraint: U23(active(X)) >= U23(X) constraint: U32(mark(X)) >= U32(X) constraint: U32(active(X)) >= U32(X) constraint: U31(mark(X1),X2) >= U31(X1,X2) constraint: U31(active(X1),X2) >= U31(X1,X2) constraint: U31(X1,mark(X2)) >= U31(X1,X2) constraint: U31(X1,active(X2)) >= U31(X1,X2) constraint: U41(mark(X)) >= U41(X) constraint: U41(active(X)) >= U41(X) constraint: U52(mark(X1),X2) >= U52(X1,X2) constraint: U52(active(X1),X2) >= U52(X1,X2) constraint: U52(X1,mark(X2)) >= U52(X1,X2) constraint: U52(X1,active(X2)) >= U52(X1,X2) 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: U62(mark(X1),X2,X3) >= U62(X1,X2,X3) constraint: U62(active(X1),X2,X3) >= U62(X1,X2,X3) constraint: U62(X1,mark(X2),X3) >= U62(X1,X2,X3) constraint: U62(X1,active(X2),X3) >= U62(X1,X2,X3) constraint: U62(X1,X2,mark(X3)) >= U62(X1,X2,X3) constraint: U62(X1,X2,active(X3)) >= U62(X1,X2,X3) constraint: U61(mark(X1),X2,X3) >= U61(X1,X2,X3) constraint: U61(active(X1),X2,X3) >= U61(X1,X2,X3) constraint: U61(X1,mark(X2),X3) >= U61(X1,X2,X3) constraint: U61(X1,active(X2),X3) >= U61(X1,X2,X3) constraint: U61(X1,X2,mark(X3)) >= U61(X1,X2,X3) constraint: U61(X1,X2,active(X3)) >= U61(X1,X2,X3) constraint: U63(mark(X1),X2,X3) >= U63(X1,X2,X3) constraint: U63(active(X1),X2,X3) >= U63(X1,X2,X3) constraint: U63(X1,mark(X2),X3) >= U63(X1,X2,X3) constraint: U63(X1,active(X2),X3) >= U63(X1,X2,X3) constraint: U63(X1,X2,mark(X3)) >= U63(X1,X2,X3) constraint: U63(X1,X2,active(X3)) >= U63(X1,X2,X3) constraint: U64(mark(X1),X2,X3) >= U64(X1,X2,X3) constraint: U64(active(X1),X2,X3) >= U64(X1,X2,X3) constraint: U64(X1,mark(X2),X3) >= U64(X1,X2,X3) constraint: U64(X1,active(X2),X3) >= U64(X1,X2,X3) constraint: U64(X1,X2,mark(X3)) >= U64(X1,X2,X3) constraint: U64(X1,X2,active(X3)) >= U64(X1,X2,X3) constraint: s(mark(X)) >= s(X) constraint: s(active(X)) >= s(X) constraint: plus(mark(X1),X2) >= plus(X1,X2) constraint: plus(active(X1),X2) >= plus(X1,X2) constraint: plus(X1,mark(X2)) >= plus(X1,X2) constraint: plus(X1,active(X2)) >= plus(X1,X2) constraint: Marked_mark(U12(X1,X2,X3)) >= Marked_mark(X1) constraint: Marked_mark(U12(X1,X2,X3)) >= Marked_active(U12(mark(X1),X2,X3)) constraint: Marked_mark(isNatKind(X)) >= Marked_active(isNatKind(X)) constraint: Marked_mark(U11(X1,X2,X3)) >= Marked_mark(X1) constraint: Marked_mark(U11(X1,X2,X3)) >= Marked_active(U11(mark(X1),X2,X3)) constraint: Marked_mark(U13(X1,X2,X3)) >= Marked_mark(X1) constraint: Marked_mark(U13(X1,X2,X3)) >= Marked_active(U13(mark(X1),X2,X3)) constraint: Marked_mark(U14(X1,X2,X3)) >= Marked_mark(X1) constraint: Marked_mark(U14(X1,X2,X3)) >= Marked_active(U14(mark(X1),X2,X3)) constraint: Marked_mark(U15(X1,X2)) >= Marked_mark(X1) constraint: Marked_mark(U15(X1,X2)) >= Marked_active(U15(mark(X1),X2)) constraint: Marked_mark(isNat(X)) >= Marked_active(isNat(X)) constraint: Marked_mark(U16(X)) >= Marked_mark(X) constraint: Marked_mark(U16(X)) >= Marked_active(U16(mark(X))) constraint: Marked_mark(U22(X1,X2)) >= Marked_mark(X1) constraint: Marked_mark(U22(X1,X2)) >= Marked_active(U22(mark(X1),X2)) constraint: Marked_mark(U21(X1,X2)) >= Marked_mark(X1) constraint: Marked_mark(U21(X1,X2)) >= Marked_active(U21(mark(X1),X2)) constraint: Marked_mark(U23(X)) >= Marked_mark(X) constraint: Marked_mark(U23(X)) >= Marked_active(U23(mark(X))) constraint: Marked_mark(U32(X)) >= Marked_mark(X) constraint: Marked_mark(U32(X)) >= Marked_active(U32(mark(X))) constraint: Marked_mark(U31(X1,X2)) >= Marked_mark(X1) constraint: Marked_mark(U31(X1,X2)) >= Marked_active(U31(mark(X1),X2)) constraint: Marked_mark(U41(X)) >= Marked_mark(X) constraint: Marked_mark(U41(X)) >= Marked_active(U41(mark(X))) constraint: Marked_mark(U52(X1,X2)) >= Marked_mark(X1) constraint: Marked_mark(U52(X1,X2)) >= Marked_active(U52(mark(X1),X2)) constraint: Marked_mark(U51(X1,X2)) >= Marked_mark(X1) constraint: Marked_mark(U51(X1,X2)) >= Marked_active(U51(mark(X1),X2)) constraint: Marked_mark(U62(X1,X2,X3)) >= Marked_mark(X1) constraint: Marked_mark(U62(X1,X2,X3)) >= Marked_active(U62(mark(X1),X2,X3)) constraint: Marked_mark(U61(X1,X2,X3)) >= Marked_mark(X1) constraint: Marked_mark(U61(X1,X2,X3)) >= Marked_active(U61(mark(X1),X2,X3)) constraint: Marked_mark(U63(X1,X2,X3)) >= Marked_mark(X1) constraint: Marked_mark(U63(X1,X2,X3)) >= Marked_active(U63(mark(X1),X2,X3)) constraint: Marked_mark(U64(X1,X2,X3)) >= Marked_mark(X1) constraint: Marked_mark(U64(X1,X2,X3)) >= Marked_active(U64(mark(X1),X2,X3)) constraint: Marked_mark(s(X)) >= Marked_mark(X) constraint: Marked_mark(s(X)) >= Marked_active(s(mark(X))) constraint: Marked_mark(plus(X1,X2)) >= Marked_mark(X1) constraint: Marked_mark(plus(X1,X2)) >= Marked_mark(X2) constraint: Marked_mark(plus(X1,X2)) >= Marked_active(plus(mark(X1),mark(X2))) constraint: Marked_active(U12(tt,V1,V2)) >= Marked_mark(U13(isNatKind(V2), V1,V2)) constraint: Marked_active(isNatKind(s(V1))) >= Marked_mark(U41(isNatKind(V1))) constraint: Marked_active(isNatKind(plus(V1,V2))) >= Marked_mark(U31( isNatKind( V1), V2)) constraint: Marked_active(U11(tt,V1,V2)) >= Marked_mark(U12(isNatKind(V1), V1,V2)) constraint: Marked_active(U13(tt,V1,V2)) >= Marked_mark(U14(isNatKind(V2), V1,V2)) constraint: Marked_active(U14(tt,V1,V2)) >= Marked_mark(U15(isNat(V1),V2)) constraint: Marked_active(U15(tt,V2)) >= Marked_mark(U16(isNat(V2))) constraint: Marked_active(isNat(s(V1))) >= Marked_mark(U21(isNatKind(V1),V1)) constraint: Marked_active(isNat(plus(V1,V2))) >= Marked_mark(U11(isNatKind(V1), V1,V2)) constraint: Marked_active(U22(tt,V1)) >= Marked_mark(U23(isNat(V1))) constraint: Marked_active(U21(tt,V1)) >= Marked_mark(U22(isNatKind(V1),V1)) constraint: Marked_active(U31(tt,V2)) >= Marked_mark(U32(isNatKind(V2))) constraint: Marked_active(U52(tt,N)) >= Marked_mark(N) constraint: Marked_active(U51(tt,N)) >= Marked_mark(U52(isNatKind(N),N)) constraint: Marked_active(U62(tt,M,N)) >= Marked_mark(U63(isNat(N),M,N)) constraint: Marked_active(U61(tt,M,N)) >= Marked_mark(U62(isNatKind(M),M,N)) constraint: Marked_active(U63(tt,M,N)) >= Marked_mark(U64(isNatKind(N),M,N)) constraint: Marked_active(U64(tt,M,N)) >= Marked_mark(s(plus(N,M))) constraint: Marked_active(plus(N,s(M))) >= Marked_mark(U61(isNat(M),M,N)) APPLY CRITERIA (Graph splitting) Found 1 components: { --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> } APPLY CRITERIA (Subterm criterion) APPLY CRITERIA (Choosing graph) Trying to solve the following constraints: { mark(U12(X1,X2,X3)) >= active(U12(mark(X1),X2,X3)) ; mark(isNatKind(X)) >= active(isNatKind(X)) ; mark(U11(X1,X2,X3)) >= active(U11(mark(X1),X2,X3)) ; mark(tt) >= active(tt) ; mark(U13(X1,X2,X3)) >= active(U13(mark(X1),X2,X3)) ; mark(U14(X1,X2,X3)) >= active(U14(mark(X1),X2,X3)) ; mark(U15(X1,X2)) >= active(U15(mark(X1),X2)) ; mark(isNat(X)) >= active(isNat(X)) ; mark(U16(X)) >= active(U16(mark(X))) ; mark(U22(X1,X2)) >= active(U22(mark(X1),X2)) ; mark(U21(X1,X2)) >= active(U21(mark(X1),X2)) ; mark(U23(X)) >= active(U23(mark(X))) ; mark(U32(X)) >= active(U32(mark(X))) ; mark(U31(X1,X2)) >= active(U31(mark(X1),X2)) ; mark(U41(X)) >= active(U41(mark(X))) ; mark(U52(X1,X2)) >= active(U52(mark(X1),X2)) ; mark(U51(X1,X2)) >= active(U51(mark(X1),X2)) ; mark(U62(X1,X2,X3)) >= active(U62(mark(X1),X2,X3)) ; mark(U61(X1,X2,X3)) >= active(U61(mark(X1),X2,X3)) ; mark(U63(X1,X2,X3)) >= active(U63(mark(X1),X2,X3)) ; mark(U64(X1,X2,X3)) >= active(U64(mark(X1),X2,X3)) ; mark(s(X)) >= active(s(mark(X))) ; mark(plus(X1,X2)) >= active(plus(mark(X1),mark(X2))) ; mark(0) >= active(0) ; U12(mark(X1),X2,X3) >= U12(X1,X2,X3) ; U12(active(X1),X2,X3) >= U12(X1,X2,X3) ; U12(X1,mark(X2),X3) >= U12(X1,X2,X3) ; U12(X1,active(X2),X3) >= U12(X1,X2,X3) ; U12(X1,X2,mark(X3)) >= U12(X1,X2,X3) ; U12(X1,X2,active(X3)) >= U12(X1,X2,X3) ; isNatKind(mark(X)) >= isNatKind(X) ; isNatKind(active(X)) >= isNatKind(X) ; active(U12(tt,V1,V2)) >= mark(U13(isNatKind(V2),V1,V2)) ; active(isNatKind(s(V1))) >= mark(U41(isNatKind(V1))) ; active(isNatKind(plus(V1,V2))) >= mark(U31(isNatKind(V1),V2)) ; active(isNatKind(0)) >= mark(tt) ; active(U11(tt,V1,V2)) >= mark(U12(isNatKind(V1),V1,V2)) ; active(U13(tt,V1,V2)) >= mark(U14(isNatKind(V2),V1,V2)) ; active(U14(tt,V1,V2)) >= mark(U15(isNat(V1),V2)) ; active(U15(tt,V2)) >= mark(U16(isNat(V2))) ; active(isNat(s(V1))) >= mark(U21(isNatKind(V1),V1)) ; active(isNat(plus(V1,V2))) >= mark(U11(isNatKind(V1),V1,V2)) ; active(isNat(0)) >= mark(tt) ; active(U16(tt)) >= mark(tt) ; active(U22(tt,V1)) >= mark(U23(isNat(V1))) ; active(U21(tt,V1)) >= mark(U22(isNatKind(V1),V1)) ; active(U23(tt)) >= mark(tt) ; active(U32(tt)) >= mark(tt) ; active(U31(tt,V2)) >= mark(U32(isNatKind(V2))) ; active(U41(tt)) >= mark(tt) ; active(U52(tt,N)) >= mark(N) ; active(U51(tt,N)) >= mark(U52(isNatKind(N),N)) ; active(U62(tt,M,N)) >= mark(U63(isNat(N),M,N)) ; active(U61(tt,M,N)) >= mark(U62(isNatKind(M),M,N)) ; active(U63(tt,M,N)) >= mark(U64(isNatKind(N),M,N)) ; active(U64(tt,M,N)) >= mark(s(plus(N,M))) ; active(plus(N,s(M))) >= mark(U61(isNat(M),M,N)) ; active(plus(N,0)) >= mark(U51(isNat(N),N)) ; U11(mark(X1),X2,X3) >= U11(X1,X2,X3) ; U11(active(X1),X2,X3) >= U11(X1,X2,X3) ; U11(X1,mark(X2),X3) >= U11(X1,X2,X3) ; U11(X1,active(X2),X3) >= U11(X1,X2,X3) ; U11(X1,X2,mark(X3)) >= U11(X1,X2,X3) ; U11(X1,X2,active(X3)) >= U11(X1,X2,X3) ; U13(mark(X1),X2,X3) >= U13(X1,X2,X3) ; U13(active(X1),X2,X3) >= U13(X1,X2,X3) ; U13(X1,mark(X2),X3) >= U13(X1,X2,X3) ; U13(X1,active(X2),X3) >= U13(X1,X2,X3) ; U13(X1,X2,mark(X3)) >= U13(X1,X2,X3) ; U13(X1,X2,active(X3)) >= U13(X1,X2,X3) ; U14(mark(X1),X2,X3) >= U14(X1,X2,X3) ; U14(active(X1),X2,X3) >= U14(X1,X2,X3) ; U14(X1,mark(X2),X3) >= U14(X1,X2,X3) ; U14(X1,active(X2),X3) >= U14(X1,X2,X3) ; U14(X1,X2,mark(X3)) >= U14(X1,X2,X3) ; U14(X1,X2,active(X3)) >= U14(X1,X2,X3) ; U15(mark(X1),X2) >= U15(X1,X2) ; U15(active(X1),X2) >= U15(X1,X2) ; U15(X1,mark(X2)) >= U15(X1,X2) ; U15(X1,active(X2)) >= U15(X1,X2) ; isNat(mark(X)) >= isNat(X) ; isNat(active(X)) >= isNat(X) ; U16(mark(X)) >= U16(X) ; U16(active(X)) >= U16(X) ; U22(mark(X1),X2) >= U22(X1,X2) ; U22(active(X1),X2) >= U22(X1,X2) ; U22(X1,mark(X2)) >= U22(X1,X2) ; U22(X1,active(X2)) >= U22(X1,X2) ; 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) ; U23(mark(X)) >= U23(X) ; U23(active(X)) >= U23(X) ; U32(mark(X)) >= U32(X) ; U32(active(X)) >= U32(X) ; U31(mark(X1),X2) >= U31(X1,X2) ; U31(active(X1),X2) >= U31(X1,X2) ; U31(X1,mark(X2)) >= U31(X1,X2) ; U31(X1,active(X2)) >= U31(X1,X2) ; U41(mark(X)) >= U41(X) ; U41(active(X)) >= U41(X) ; U52(mark(X1),X2) >= U52(X1,X2) ; U52(active(X1),X2) >= U52(X1,X2) ; U52(X1,mark(X2)) >= U52(X1,X2) ; U52(X1,active(X2)) >= U52(X1,X2) ; 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) ; U62(mark(X1),X2,X3) >= U62(X1,X2,X3) ; U62(active(X1),X2,X3) >= U62(X1,X2,X3) ; U62(X1,mark(X2),X3) >= U62(X1,X2,X3) ; U62(X1,active(X2),X3) >= U62(X1,X2,X3) ; U62(X1,X2,mark(X3)) >= U62(X1,X2,X3) ; U62(X1,X2,active(X3)) >= U62(X1,X2,X3) ; U61(mark(X1),X2,X3) >= U61(X1,X2,X3) ; U61(active(X1),X2,X3) >= U61(X1,X2,X3) ; U61(X1,mark(X2),X3) >= U61(X1,X2,X3) ; U61(X1,active(X2),X3) >= U61(X1,X2,X3) ; U61(X1,X2,mark(X3)) >= U61(X1,X2,X3) ; U61(X1,X2,active(X3)) >= U61(X1,X2,X3) ; U63(mark(X1),X2,X3) >= U63(X1,X2,X3) ; U63(active(X1),X2,X3) >= U63(X1,X2,X3) ; U63(X1,mark(X2),X3) >= U63(X1,X2,X3) ; U63(X1,active(X2),X3) >= U63(X1,X2,X3) ; U63(X1,X2,mark(X3)) >= U63(X1,X2,X3) ; U63(X1,X2,active(X3)) >= U63(X1,X2,X3) ; U64(mark(X1),X2,X3) >= U64(X1,X2,X3) ; U64(active(X1),X2,X3) >= U64(X1,X2,X3) ; U64(X1,mark(X2),X3) >= U64(X1,X2,X3) ; U64(X1,active(X2),X3) >= U64(X1,X2,X3) ; U64(X1,X2,mark(X3)) >= U64(X1,X2,X3) ; U64(X1,X2,active(X3)) >= U64(X1,X2,X3) ; s(mark(X)) >= s(X) ; s(active(X)) >= s(X) ; plus(mark(X1),X2) >= plus(X1,X2) ; plus(active(X1),X2) >= plus(X1,X2) ; plus(X1,mark(X2)) >= plus(X1,X2) ; plus(X1,active(X2)) >= plus(X1,X2) ; Marked_mark(U12(X1,X2,X3)) >= Marked_mark(X1) ; Marked_mark(U12(X1,X2,X3)) >= Marked_active(U12(mark(X1),X2,X3)) ; Marked_mark(isNatKind(X)) >= Marked_active(isNatKind(X)) ; Marked_mark(U11(X1,X2,X3)) >= Marked_mark(X1) ; Marked_mark(U11(X1,X2,X3)) >= Marked_active(U11(mark(X1),X2,X3)) ; Marked_mark(U13(X1,X2,X3)) >= Marked_mark(X1) ; Marked_mark(U13(X1,X2,X3)) >= Marked_active(U13(mark(X1),X2,X3)) ; Marked_mark(U14(X1,X2,X3)) >= Marked_mark(X1) ; Marked_mark(U14(X1,X2,X3)) >= Marked_active(U14(mark(X1),X2,X3)) ; Marked_mark(U15(X1,X2)) >= Marked_mark(X1) ; Marked_mark(U15(X1,X2)) >= Marked_active(U15(mark(X1),X2)) ; Marked_mark(isNat(X)) >= Marked_active(isNat(X)) ; Marked_mark(U16(X)) >= Marked_mark(X) ; Marked_mark(U22(X1,X2)) >= Marked_mark(X1) ; Marked_mark(U22(X1,X2)) >= Marked_active(U22(mark(X1),X2)) ; Marked_mark(U21(X1,X2)) >= Marked_mark(X1) ; Marked_mark(U21(X1,X2)) >= Marked_active(U21(mark(X1),X2)) ; Marked_mark(U23(X)) >= Marked_mark(X) ; Marked_mark(U32(X)) >= Marked_mark(X) ; Marked_mark(U31(X1,X2)) >= Marked_mark(X1) ; Marked_mark(U31(X1,X2)) >= Marked_active(U31(mark(X1),X2)) ; Marked_mark(U41(X)) >= Marked_mark(X) ; Marked_mark(U52(X1,X2)) >= Marked_mark(X1) ; Marked_mark(U52(X1,X2)) >= Marked_active(U52(mark(X1),X2)) ; Marked_mark(U51(X1,X2)) >= Marked_mark(X1) ; Marked_mark(U51(X1,X2)) >= Marked_active(U51(mark(X1),X2)) ; Marked_mark(U62(X1,X2,X3)) >= Marked_mark(X1) ; Marked_mark(U62(X1,X2,X3)) >= Marked_active(U62(mark(X1),X2,X3)) ; Marked_mark(U61(X1,X2,X3)) >= Marked_mark(X1) ; Marked_mark(U61(X1,X2,X3)) >= Marked_active(U61(mark(X1),X2,X3)) ; Marked_mark(U63(X1,X2,X3)) >= Marked_mark(X1) ; Marked_mark(U63(X1,X2,X3)) >= Marked_active(U63(mark(X1),X2,X3)) ; Marked_mark(U64(X1,X2,X3)) >= Marked_mark(X1) ; Marked_mark(U64(X1,X2,X3)) >= Marked_active(U64(mark(X1),X2,X3)) ; Marked_mark(s(X)) >= Marked_mark(X) ; Marked_mark(plus(X1,X2)) >= Marked_mark(X1) ; Marked_mark(plus(X1,X2)) >= Marked_mark(X2) ; Marked_mark(plus(X1,X2)) >= Marked_active(plus(mark(X1),mark(X2))) ; Marked_active(U12(tt,V1,V2)) >= Marked_mark(U13(isNatKind(V2),V1,V2)) ; Marked_active(isNatKind(s(V1))) >= Marked_mark(U41(isNatKind(V1))) ; Marked_active(isNatKind(plus(V1,V2))) >= Marked_mark(U31(isNatKind(V1),V2)) ; Marked_active(U11(tt,V1,V2)) >= Marked_mark(U12(isNatKind(V1),V1,V2)) ; Marked_active(U13(tt,V1,V2)) >= Marked_mark(U14(isNatKind(V2),V1,V2)) ; Marked_active(U14(tt,V1,V2)) >= Marked_mark(U15(isNat(V1),V2)) ; Marked_active(U15(tt,V2)) >= Marked_mark(U16(isNat(V2))) ; Marked_active(isNat(s(V1))) >= Marked_mark(U21(isNatKind(V1),V1)) ; Marked_active(isNat(plus(V1,V2))) >= Marked_mark(U11(isNatKind(V1),V1,V2)) ; Marked_active(U22(tt,V1)) >= Marked_mark(U23(isNat(V1))) ; Marked_active(U21(tt,V1)) >= Marked_mark(U22(isNatKind(V1),V1)) ; Marked_active(U31(tt,V2)) >= Marked_mark(U32(isNatKind(V2))) ; Marked_active(U52(tt,N)) >= Marked_mark(N) ; Marked_active(U51(tt,N)) >= Marked_mark(U52(isNatKind(N),N)) ; Marked_active(U62(tt,M,N)) >= Marked_mark(U63(isNat(N),M,N)) ; Marked_active(U61(tt,M,N)) >= Marked_mark(U62(isNatKind(M),M,N)) ; Marked_active(U63(tt,M,N)) >= Marked_mark(U64(isNatKind(N),M,N)) ; Marked_active(U64(tt,M,N)) >= Marked_mark(s(plus(N,M))) ; Marked_active(plus(N,s(M))) >= Marked_mark(U61(isNat(M),M,N)) ; } + Disjunctions:{ { Marked_mark(U12(X1,X2,X3)) > Marked_mark(X1) ; } { Marked_mark(U12(X1,X2,X3)) > Marked_active(U12(mark(X1),X2,X3)) ; } { Marked_mark(isNatKind(X)) > Marked_active(isNatKind(X)) ; } { Marked_mark(U11(X1,X2,X3)) > Marked_mark(X1) ; } { Marked_mark(U11(X1,X2,X3)) > Marked_active(U11(mark(X1),X2,X3)) ; } { Marked_mark(U13(X1,X2,X3)) > Marked_mark(X1) ; } { Marked_mark(U13(X1,X2,X3)) > Marked_active(U13(mark(X1),X2,X3)) ; } { Marked_mark(U14(X1,X2,X3)) > Marked_mark(X1) ; } { Marked_mark(U14(X1,X2,X3)) > Marked_active(U14(mark(X1),X2,X3)) ; } { Marked_mark(U15(X1,X2)) > Marked_mark(X1) ; } { Marked_mark(U15(X1,X2)) > Marked_active(U15(mark(X1),X2)) ; } { Marked_mark(isNat(X)) > Marked_active(isNat(X)) ; } { Marked_mark(U16(X)) > Marked_mark(X) ; } { Marked_mark(U22(X1,X2)) > Marked_mark(X1) ; } { Marked_mark(U22(X1,X2)) > Marked_active(U22(mark(X1),X2)) ; } { Marked_mark(U21(X1,X2)) > Marked_mark(X1) ; } { Marked_mark(U21(X1,X2)) > Marked_active(U21(mark(X1),X2)) ; } { Marked_mark(U23(X)) > Marked_mark(X) ; } { Marked_mark(U32(X)) > Marked_mark(X) ; } { Marked_mark(U31(X1,X2)) > Marked_mark(X1) ; } { Marked_mark(U31(X1,X2)) > Marked_active(U31(mark(X1),X2)) ; } { Marked_mark(U41(X)) > Marked_mark(X) ; } { Marked_mark(U52(X1,X2)) > Marked_mark(X1) ; } { Marked_mark(U52(X1,X2)) > Marked_active(U52(mark(X1),X2)) ; } { Marked_mark(U51(X1,X2)) > Marked_mark(X1) ; } { Marked_mark(U51(X1,X2)) > Marked_active(U51(mark(X1),X2)) ; } { Marked_mark(U62(X1,X2,X3)) > Marked_mark(X1) ; } { Marked_mark(U62(X1,X2,X3)) > Marked_active(U62(mark(X1),X2,X3)) ; } { Marked_mark(U61(X1,X2,X3)) > Marked_mark(X1) ; } { Marked_mark(U61(X1,X2,X3)) > Marked_active(U61(mark(X1),X2,X3)) ; } { Marked_mark(U63(X1,X2,X3)) > Marked_mark(X1) ; } { Marked_mark(U63(X1,X2,X3)) > Marked_active(U63(mark(X1),X2,X3)) ; } { Marked_mark(U64(X1,X2,X3)) > Marked_mark(X1) ; } { Marked_mark(U64(X1,X2,X3)) > Marked_active(U64(mark(X1),X2,X3)) ; } { Marked_mark(s(X)) > Marked_mark(X) ; } { Marked_mark(plus(X1,X2)) > Marked_mark(X1) ; } { Marked_mark(plus(X1,X2)) > Marked_mark(X2) ; } { Marked_mark(plus(X1,X2)) > Marked_active(plus(mark(X1),mark(X2))) ; } { Marked_active(U12(tt,V1,V2)) > Marked_mark(U13(isNatKind(V2),V1,V2)) ; } { Marked_active(isNatKind(s(V1))) > Marked_mark(U41(isNatKind(V1))) ; } { Marked_active(isNatKind(plus(V1,V2))) > Marked_mark(U31(isNatKind(V1),V2)) ; } { Marked_active(U11(tt,V1,V2)) > Marked_mark(U12(isNatKind(V1),V1,V2)) ; } { Marked_active(U13(tt,V1,V2)) > Marked_mark(U14(isNatKind(V2),V1,V2)) ; } { Marked_active(U14(tt,V1,V2)) > Marked_mark(U15(isNat(V1),V2)) ; } { Marked_active(U15(tt,V2)) > Marked_mark(U16(isNat(V2))) ; } { Marked_active(isNat(s(V1))) > Marked_mark(U21(isNatKind(V1),V1)) ; } { Marked_active(isNat(plus(V1,V2))) > Marked_mark(U11(isNatKind(V1),V1,V2)) ; } { Marked_active(U22(tt,V1)) > Marked_mark(U23(isNat(V1))) ; } { Marked_active(U21(tt,V1)) > Marked_mark(U22(isNatKind(V1),V1)) ; } { Marked_active(U31(tt,V2)) > Marked_mark(U32(isNatKind(V2))) ; } { Marked_active(U52(tt,N)) > Marked_mark(N) ; } { Marked_active(U51(tt,N)) > Marked_mark(U52(isNatKind(N),N)) ; } { Marked_active(U62(tt,M,N)) > Marked_mark(U63(isNat(N),M,N)) ; } { Marked_active(U61(tt,M,N)) > Marked_mark(U62(isNatKind(M),M,N)) ; } { Marked_active(U63(tt,M,N)) > Marked_mark(U64(isNatKind(N),M,N)) ; } { Marked_active(U64(tt,M,N)) > Marked_mark(s(plus(N,M))) ; } { Marked_active(plus(N,s(M))) > Marked_mark(U61(isNat(M),M,N)) ; } } === 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(U12(X1,X2,X3)) >= active(U12(mark(X1),X2,X3)) constraint: mark(isNatKind(X)) >= active(isNatKind(X)) constraint: mark(U11(X1,X2,X3)) >= active(U11(mark(X1),X2,X3)) constraint: mark(tt) >= active(tt) constraint: mark(U13(X1,X2,X3)) >= active(U13(mark(X1),X2,X3)) constraint: mark(U14(X1,X2,X3)) >= active(U14(mark(X1),X2,X3)) constraint: mark(U15(X1,X2)) >= active(U15(mark(X1),X2)) constraint: mark(isNat(X)) >= active(isNat(X)) constraint: mark(U16(X)) >= active(U16(mark(X))) constraint: mark(U22(X1,X2)) >= active(U22(mark(X1),X2)) constraint: mark(U21(X1,X2)) >= active(U21(mark(X1),X2)) constraint: mark(U23(X)) >= active(U23(mark(X))) constraint: mark(U32(X)) >= active(U32(mark(X))) constraint: mark(U31(X1,X2)) >= active(U31(mark(X1),X2)) constraint: mark(U41(X)) >= active(U41(mark(X))) constraint: mark(U52(X1,X2)) >= active(U52(mark(X1),X2)) constraint: mark(U51(X1,X2)) >= active(U51(mark(X1),X2)) constraint: mark(U62(X1,X2,X3)) >= active(U62(mark(X1),X2,X3)) constraint: mark(U61(X1,X2,X3)) >= active(U61(mark(X1),X2,X3)) constraint: mark(U63(X1,X2,X3)) >= active(U63(mark(X1),X2,X3)) constraint: mark(U64(X1,X2,X3)) >= active(U64(mark(X1),X2,X3)) constraint: mark(s(X)) >= active(s(mark(X))) constraint: mark(plus(X1,X2)) >= active(plus(mark(X1),mark(X2))) constraint: mark(0) >= active(0) constraint: U12(mark(X1),X2,X3) >= U12(X1,X2,X3) constraint: U12(active(X1),X2,X3) >= U12(X1,X2,X3) constraint: U12(X1,mark(X2),X3) >= U12(X1,X2,X3) constraint: U12(X1,active(X2),X3) >= U12(X1,X2,X3) constraint: U12(X1,X2,mark(X3)) >= U12(X1,X2,X3) constraint: U12(X1,X2,active(X3)) >= U12(X1,X2,X3) constraint: isNatKind(mark(X)) >= isNatKind(X) constraint: isNatKind(active(X)) >= isNatKind(X) constraint: active(U12(tt,V1,V2)) >= mark(U13(isNatKind(V2),V1,V2)) constraint: active(isNatKind(s(V1))) >= mark(U41(isNatKind(V1))) constraint: active(isNatKind(plus(V1,V2))) >= mark(U31(isNatKind(V1),V2)) constraint: active(isNatKind(0)) >= mark(tt) constraint: active(U11(tt,V1,V2)) >= mark(U12(isNatKind(V1),V1,V2)) constraint: active(U13(tt,V1,V2)) >= mark(U14(isNatKind(V2),V1,V2)) constraint: active(U14(tt,V1,V2)) >= mark(U15(isNat(V1),V2)) constraint: active(U15(tt,V2)) >= mark(U16(isNat(V2))) constraint: active(isNat(s(V1))) >= mark(U21(isNatKind(V1),V1)) constraint: active(isNat(plus(V1,V2))) >= mark(U11(isNatKind(V1),V1,V2)) constraint: active(isNat(0)) >= mark(tt) constraint: active(U16(tt)) >= mark(tt) constraint: active(U22(tt,V1)) >= mark(U23(isNat(V1))) constraint: active(U21(tt,V1)) >= mark(U22(isNatKind(V1),V1)) constraint: active(U23(tt)) >= mark(tt) constraint: active(U32(tt)) >= mark(tt) constraint: active(U31(tt,V2)) >= mark(U32(isNatKind(V2))) constraint: active(U41(tt)) >= mark(tt) constraint: active(U52(tt,N)) >= mark(N) constraint: active(U51(tt,N)) >= mark(U52(isNatKind(N),N)) constraint: active(U62(tt,M,N)) >= mark(U63(isNat(N),M,N)) constraint: active(U61(tt,M,N)) >= mark(U62(isNatKind(M),M,N)) constraint: active(U63(tt,M,N)) >= mark(U64(isNatKind(N),M,N)) constraint: active(U64(tt,M,N)) >= mark(s(plus(N,M))) constraint: active(plus(N,s(M))) >= mark(U61(isNat(M),M,N)) constraint: active(plus(N,0)) >= mark(U51(isNat(N),N)) constraint: U11(mark(X1),X2,X3) >= U11(X1,X2,X3) constraint: U11(active(X1),X2,X3) >= U11(X1,X2,X3) constraint: U11(X1,mark(X2),X3) >= U11(X1,X2,X3) constraint: U11(X1,active(X2),X3) >= U11(X1,X2,X3) constraint: U11(X1,X2,mark(X3)) >= U11(X1,X2,X3) constraint: U11(X1,X2,active(X3)) >= U11(X1,X2,X3) constraint: U13(mark(X1),X2,X3) >= U13(X1,X2,X3) constraint: U13(active(X1),X2,X3) >= U13(X1,X2,X3) constraint: U13(X1,mark(X2),X3) >= U13(X1,X2,X3) constraint: U13(X1,active(X2),X3) >= U13(X1,X2,X3) constraint: U13(X1,X2,mark(X3)) >= U13(X1,X2,X3) constraint: U13(X1,X2,active(X3)) >= U13(X1,X2,X3) constraint: U14(mark(X1),X2,X3) >= U14(X1,X2,X3) constraint: U14(active(X1),X2,X3) >= U14(X1,X2,X3) constraint: U14(X1,mark(X2),X3) >= U14(X1,X2,X3) constraint: U14(X1,active(X2),X3) >= U14(X1,X2,X3) constraint: U14(X1,X2,mark(X3)) >= U14(X1,X2,X3) constraint: U14(X1,X2,active(X3)) >= U14(X1,X2,X3) constraint: U15(mark(X1),X2) >= U15(X1,X2) constraint: U15(active(X1),X2) >= U15(X1,X2) constraint: U15(X1,mark(X2)) >= U15(X1,X2) constraint: U15(X1,active(X2)) >= U15(X1,X2) constraint: isNat(mark(X)) >= isNat(X) constraint: isNat(active(X)) >= isNat(X) constraint: U16(mark(X)) >= U16(X) constraint: U16(active(X)) >= U16(X) constraint: U22(mark(X1),X2) >= U22(X1,X2) constraint: U22(active(X1),X2) >= U22(X1,X2) constraint: U22(X1,mark(X2)) >= U22(X1,X2) constraint: U22(X1,active(X2)) >= U22(X1,X2) 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: U23(mark(X)) >= U23(X) constraint: U23(active(X)) >= U23(X) constraint: U32(mark(X)) >= U32(X) constraint: U32(active(X)) >= U32(X) constraint: U31(mark(X1),X2) >= U31(X1,X2) constraint: U31(active(X1),X2) >= U31(X1,X2) constraint: U31(X1,mark(X2)) >= U31(X1,X2) constraint: U31(X1,active(X2)) >= U31(X1,X2) constraint: U41(mark(X)) >= U41(X) constraint: U41(active(X)) >= U41(X) constraint: U52(mark(X1),X2) >= U52(X1,X2) constraint: U52(active(X1),X2) >= U52(X1,X2) constraint: U52(X1,mark(X2)) >= U52(X1,X2) constraint: U52(X1,active(X2)) >= U52(X1,X2) 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: U62(mark(X1),X2,X3) >= U62(X1,X2,X3) constraint: U62(active(X1),X2,X3) >= U62(X1,X2,X3) constraint: U62(X1,mark(X2),X3) >= U62(X1,X2,X3) constraint: U62(X1,active(X2),X3) >= U62(X1,X2,X3) constraint: U62(X1,X2,mark(X3)) >= U62(X1,X2,X3) constraint: U62(X1,X2,active(X3)) >= U62(X1,X2,X3) constraint: U61(mark(X1),X2,X3) >= U61(X1,X2,X3) constraint: U61(active(X1),X2,X3) >= U61(X1,X2,X3) constraint: U61(X1,mark(X2),X3) >= U61(X1,X2,X3) constraint: U61(X1,active(X2),X3) >= U61(X1,X2,X3) constraint: U61(X1,X2,mark(X3)) >= U61(X1,X2,X3) constraint: U61(X1,X2,active(X3)) >= U61(X1,X2,X3) constraint: U63(mark(X1),X2,X3) >= U63(X1,X2,X3) constraint: U63(active(X1),X2,X3) >= U63(X1,X2,X3) constraint: U63(X1,mark(X2),X3) >= U63(X1,X2,X3) constraint: U63(X1,active(X2),X3) >= U63(X1,X2,X3) constraint: U63(X1,X2,mark(X3)) >= U63(X1,X2,X3) constraint: U63(X1,X2,active(X3)) >= U63(X1,X2,X3) constraint: U64(mark(X1),X2,X3) >= U64(X1,X2,X3) constraint: U64(active(X1),X2,X3) >= U64(X1,X2,X3) constraint: U64(X1,mark(X2),X3) >= U64(X1,X2,X3) constraint: U64(X1,active(X2),X3) >= U64(X1,X2,X3) constraint: U64(X1,X2,mark(X3)) >= U64(X1,X2,X3) constraint: U64(X1,X2,active(X3)) >= U64(X1,X2,X3) constraint: s(mark(X)) >= s(X) constraint: s(active(X)) >= s(X) constraint: plus(mark(X1),X2) >= plus(X1,X2) constraint: plus(active(X1),X2) >= plus(X1,X2) constraint: plus(X1,mark(X2)) >= plus(X1,X2) constraint: plus(X1,active(X2)) >= plus(X1,X2) constraint: Marked_mark(U12(X1,X2,X3)) >= Marked_mark(X1) constraint: Marked_mark(U12(X1,X2,X3)) >= Marked_active(U12(mark(X1),X2,X3)) constraint: Marked_mark(isNatKind(X)) >= Marked_active(isNatKind(X)) constraint: Marked_mark(U11(X1,X2,X3)) >= Marked_mark(X1) constraint: Marked_mark(U11(X1,X2,X3)) >= Marked_active(U11(mark(X1),X2,X3)) constraint: Marked_mark(U13(X1,X2,X3)) >= Marked_mark(X1) constraint: Marked_mark(U13(X1,X2,X3)) >= Marked_active(U13(mark(X1),X2,X3)) constraint: Marked_mark(U14(X1,X2,X3)) >= Marked_mark(X1) constraint: Marked_mark(U14(X1,X2,X3)) >= Marked_active(U14(mark(X1),X2,X3)) constraint: Marked_mark(U15(X1,X2)) >= Marked_mark(X1) constraint: Marked_mark(U15(X1,X2)) >= Marked_active(U15(mark(X1),X2)) constraint: Marked_mark(isNat(X)) >= Marked_active(isNat(X)) constraint: Marked_mark(U16(X)) >= Marked_mark(X) constraint: Marked_mark(U22(X1,X2)) >= Marked_mark(X1) constraint: Marked_mark(U22(X1,X2)) >= Marked_active(U22(mark(X1),X2)) constraint: Marked_mark(U21(X1,X2)) >= Marked_mark(X1) constraint: Marked_mark(U21(X1,X2)) >= Marked_active(U21(mark(X1),X2)) constraint: Marked_mark(U23(X)) >= Marked_mark(X) constraint: Marked_mark(U32(X)) >= Marked_mark(X) constraint: Marked_mark(U31(X1,X2)) >= Marked_mark(X1) constraint: Marked_mark(U31(X1,X2)) >= Marked_active(U31(mark(X1),X2)) constraint: Marked_mark(U41(X)) >= Marked_mark(X) constraint: Marked_mark(U52(X1,X2)) >= Marked_mark(X1) constraint: Marked_mark(U52(X1,X2)) >= Marked_active(U52(mark(X1),X2)) constraint: Marked_mark(U51(X1,X2)) >= Marked_mark(X1) constraint: Marked_mark(U51(X1,X2)) >= Marked_active(U51(mark(X1),X2)) constraint: Marked_mark(U62(X1,X2,X3)) >= Marked_mark(X1) constraint: Marked_mark(U62(X1,X2,X3)) >= Marked_active(U62(mark(X1),X2,X3)) constraint: Marked_mark(U61(X1,X2,X3)) >= Marked_mark(X1) constraint: Marked_mark(U61(X1,X2,X3)) >= Marked_active(U61(mark(X1),X2,X3)) constraint: Marked_mark(U63(X1,X2,X3)) >= Marked_mark(X1) constraint: Marked_mark(U63(X1,X2,X3)) >= Marked_active(U63(mark(X1),X2,X3)) constraint: Marked_mark(U64(X1,X2,X3)) >= Marked_mark(X1) constraint: Marked_mark(U64(X1,X2,X3)) >= Marked_active(U64(mark(X1),X2,X3)) constraint: Marked_mark(s(X)) >= Marked_mark(X) constraint: Marked_mark(plus(X1,X2)) >= Marked_mark(X1) constraint: Marked_mark(plus(X1,X2)) >= Marked_mark(X2) constraint: Marked_mark(plus(X1,X2)) >= Marked_active(plus(mark(X1),mark(X2))) constraint: Marked_active(U12(tt,V1,V2)) >= Marked_mark(U13(isNatKind(V2), V1,V2)) constraint: Marked_active(isNatKind(s(V1))) >= Marked_mark(U41(isNatKind(V1))) constraint: Marked_active(isNatKind(plus(V1,V2))) >= Marked_mark(U31( isNatKind( V1), V2)) constraint: Marked_active(U11(tt,V1,V2)) >= Marked_mark(U12(isNatKind(V1), V1,V2)) constraint: Marked_active(U13(tt,V1,V2)) >= Marked_mark(U14(isNatKind(V2), V1,V2)) constraint: Marked_active(U14(tt,V1,V2)) >= Marked_mark(U15(isNat(V1),V2)) constraint: Marked_active(U15(tt,V2)) >= Marked_mark(U16(isNat(V2))) constraint: Marked_active(isNat(s(V1))) >= Marked_mark(U21(isNatKind(V1),V1)) constraint: Marked_active(isNat(plus(V1,V2))) >= Marked_mark(U11(isNatKind(V1), V1,V2)) constraint: Marked_active(U22(tt,V1)) >= Marked_mark(U23(isNat(V1))) constraint: Marked_active(U21(tt,V1)) >= Marked_mark(U22(isNatKind(V1),V1)) constraint: Marked_active(U31(tt,V2)) >= Marked_mark(U32(isNatKind(V2))) constraint: Marked_active(U52(tt,N)) >= Marked_mark(N) constraint: Marked_active(U51(tt,N)) >= Marked_mark(U52(isNatKind(N),N)) constraint: Marked_active(U62(tt,M,N)) >= Marked_mark(U63(isNat(N),M,N)) constraint: Marked_active(U61(tt,M,N)) >= Marked_mark(U62(isNatKind(M),M,N)) constraint: Marked_active(U63(tt,M,N)) >= Marked_mark(U64(isNatKind(N),M,N)) constraint: Marked_active(U64(tt,M,N)) >= Marked_mark(s(plus(N,M))) constraint: Marked_active(plus(N,s(M))) >= Marked_mark(U61(isNat(M),M,N)) APPLY CRITERIA (Graph splitting) Found 1 components: { --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> -->