- : unit = () h : heuristic = - : unit = () APPLY CRITERIA (Marked dependency pairs) TRS termination of: [1] a__U11(tt,V1,V2) -> a__U12(a__isNat(V1),V2) [2] a__U12(tt,V2) -> a__U13(a__isNat(V2)) [3] a__U13(tt) -> tt [4] a__U21(tt,V1) -> a__U22(a__isNat(V1)) [5] a__U22(tt) -> tt [6] a__U31(tt,V1,V2) -> a__U32(a__isNat(V1),V2) [7] a__U32(tt,V2) -> a__U33(a__isNat(V2)) [8] a__U33(tt) -> tt [9] a__U41(tt,N) -> mark(N) [10] a__U51(tt,M,N) -> s(a__plus(mark(N),mark(M))) [11] a__U61(tt) -> 0 [12] a__U71(tt,M,N) -> a__plus(a__x(mark(N),mark(M)),mark(N)) [13] a__and(tt,X) -> mark(X) [14] a__isNat(0) -> tt [15] a__isNat(plus(V1,V2)) -> a__U11(a__and(a__isNatKind(V1),isNatKind(V2)),V1,V2) [16] a__isNat(s(V1)) -> a__U21(a__isNatKind(V1),V1) [17] a__isNat(x(V1,V2)) -> a__U31(a__and(a__isNatKind(V1),isNatKind(V2)),V1,V2) [18] a__isNatKind(0) -> tt [19] a__isNatKind(plus(V1,V2)) -> a__and(a__isNatKind(V1),isNatKind(V2)) [20] a__isNatKind(s(V1)) -> a__isNatKind(V1) [21] a__isNatKind(x(V1,V2)) -> a__and(a__isNatKind(V1),isNatKind(V2)) [22] a__plus(N,0) -> a__U41(a__and(a__isNat(N),isNatKind(N)),N) [23] a__plus(N,s(M)) -> a__U51(a__and(a__and(a__isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N))), M,N) [24] a__x(N,0) -> a__U61(a__and(a__isNat(N),isNatKind(N))) [25] a__x(N,s(M)) -> a__U71(a__and(a__and(a__isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N))), M,N) [26] mark(U11(X1,X2,X3)) -> a__U11(mark(X1),X2,X3) [27] mark(U12(X1,X2)) -> a__U12(mark(X1),X2) [28] mark(isNat(X)) -> a__isNat(X) [29] mark(U13(X)) -> a__U13(mark(X)) [30] mark(U21(X1,X2)) -> a__U21(mark(X1),X2) [31] mark(U22(X)) -> a__U22(mark(X)) [32] mark(U31(X1,X2,X3)) -> a__U31(mark(X1),X2,X3) [33] mark(U32(X1,X2)) -> a__U32(mark(X1),X2) [34] mark(U33(X)) -> a__U33(mark(X)) [35] mark(U41(X1,X2)) -> a__U41(mark(X1),X2) [36] mark(U51(X1,X2,X3)) -> a__U51(mark(X1),X2,X3) [37] mark(plus(X1,X2)) -> a__plus(mark(X1),mark(X2)) [38] mark(U61(X)) -> a__U61(mark(X)) [39] mark(U71(X1,X2,X3)) -> a__U71(mark(X1),X2,X3) [40] mark(x(X1,X2)) -> a__x(mark(X1),mark(X2)) [41] mark(and(X1,X2)) -> a__and(mark(X1),X2) [42] mark(isNatKind(X)) -> a__isNatKind(X) [43] mark(tt) -> tt [44] mark(s(X)) -> s(mark(X)) [45] mark(0) -> 0 [46] a__U11(X1,X2,X3) -> U11(X1,X2,X3) [47] a__U12(X1,X2) -> U12(X1,X2) [48] a__isNat(X) -> isNat(X) [49] a__U13(X) -> U13(X) [50] a__U21(X1,X2) -> U21(X1,X2) [51] a__U22(X) -> U22(X) [52] a__U31(X1,X2,X3) -> U31(X1,X2,X3) [53] a__U32(X1,X2) -> U32(X1,X2) [54] a__U33(X) -> U33(X) [55] a__U41(X1,X2) -> U41(X1,X2) [56] a__U51(X1,X2,X3) -> U51(X1,X2,X3) [57] a__plus(X1,X2) -> plus(X1,X2) [58] a__U61(X) -> U61(X) [59] a__U71(X1,X2,X3) -> U71(X1,X2,X3) [60] a__x(X1,X2) -> x(X1,X2) [61] a__and(X1,X2) -> and(X1,X2) [62] a__isNatKind(X) -> isNatKind(X) Sub problem: guided: DP termination of: END GUIDED APPLY CRITERIA (Graph splitting) Found 1 components: { --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> } APPLY CRITERIA (Choosing graph) Trying to solve the following constraints: { a__U12(tt,V2) >= a__U13(a__isNat(V2)) ; a__U12(X1,X2) >= U12(X1,X2) ; a__isNat(s(V1)) >= a__U21(a__isNatKind(V1),V1) ; a__isNat(0) >= tt ; a__isNat(plus(V1,V2)) >= a__U11(a__and(a__isNatKind(V1),isNatKind(V2)),V1,V2) ; a__isNat(x(V1,V2)) >= a__U31(a__and(a__isNatKind(V1),isNatKind(V2)),V1,V2) ; a__isNat(X) >= isNat(X) ; a__U11(tt,V1,V2) >= a__U12(a__isNat(V1),V2) ; a__U11(X1,X2,X3) >= U11(X1,X2,X3) ; a__U13(tt) >= tt ; a__U13(X) >= U13(X) ; a__U22(tt) >= tt ; a__U22(X) >= U22(X) ; a__U21(tt,V1) >= a__U22(a__isNat(V1)) ; a__U21(X1,X2) >= U21(X1,X2) ; a__U32(tt,V2) >= a__U33(a__isNat(V2)) ; a__U32(X1,X2) >= U32(X1,X2) ; a__U31(tt,V1,V2) >= a__U32(a__isNat(V1),V2) ; a__U31(X1,X2,X3) >= U31(X1,X2,X3) ; a__U33(tt) >= tt ; a__U33(X) >= U33(X) ; mark(tt) >= tt ; mark(s(X)) >= s(mark(X)) ; mark(0) >= 0 ; mark(isNatKind(X)) >= a__isNatKind(X) ; mark(plus(X1,X2)) >= a__plus(mark(X1),mark(X2)) ; mark(x(X1,X2)) >= a__x(mark(X1),mark(X2)) ; mark(and(X1,X2)) >= a__and(mark(X1),X2) ; mark(isNat(X)) >= a__isNat(X) ; mark(U11(X1,X2,X3)) >= a__U11(mark(X1),X2,X3) ; mark(U12(X1,X2)) >= a__U12(mark(X1),X2) ; mark(U13(X)) >= a__U13(mark(X)) ; mark(U21(X1,X2)) >= a__U21(mark(X1),X2) ; mark(U22(X)) >= a__U22(mark(X)) ; mark(U31(X1,X2,X3)) >= a__U31(mark(X1),X2,X3) ; mark(U32(X1,X2)) >= a__U32(mark(X1),X2) ; mark(U33(X)) >= a__U33(mark(X)) ; mark(U41(X1,X2)) >= a__U41(mark(X1),X2) ; mark(U51(X1,X2,X3)) >= a__U51(mark(X1),X2,X3) ; mark(U61(X)) >= a__U61(mark(X)) ; mark(U71(X1,X2,X3)) >= a__U71(mark(X1),X2,X3) ; a__U41(tt,N) >= mark(N) ; a__U41(X1,X2) >= U41(X1,X2) ; a__plus(N,s(M)) >= a__U51(a__and(a__and(a__isNat(M),isNatKind(M)), and(isNat(N),isNatKind(N))),M,N) ; a__plus(N,0) >= a__U41(a__and(a__isNat(N),isNatKind(N)),N) ; a__plus(X1,X2) >= plus(X1,X2) ; a__U51(tt,M,N) >= s(a__plus(mark(N),mark(M))) ; a__U51(X1,X2,X3) >= U51(X1,X2,X3) ; a__U61(tt) >= 0 ; a__U61(X) >= U61(X) ; a__x(N,s(M)) >= a__U71(a__and(a__and(a__isNat(M),isNatKind(M)), and(isNat(N),isNatKind(N))),M,N) ; a__x(N,0) >= a__U61(a__and(a__isNat(N),isNatKind(N))) ; a__x(X1,X2) >= x(X1,X2) ; a__U71(tt,M,N) >= a__plus(a__x(mark(N),mark(M)),mark(N)) ; a__U71(X1,X2,X3) >= U71(X1,X2,X3) ; a__and(tt,X) >= mark(X) ; a__and(X1,X2) >= and(X1,X2) ; a__isNatKind(s(V1)) >= a__isNatKind(V1) ; a__isNatKind(0) >= tt ; a__isNatKind(plus(V1,V2)) >= a__and(a__isNatKind(V1),isNatKind(V2)) ; a__isNatKind(x(V1,V2)) >= a__and(a__isNatKind(V1),isNatKind(V2)) ; a__isNatKind(X) >= isNatKind(X) ; Marked_a__isNatKind(s(V1)) >= Marked_a__isNatKind(V1) ; Marked_a__isNatKind(plus(V1,V2)) >= Marked_a__isNatKind(V1) ; Marked_a__isNatKind(plus(V1,V2)) >= Marked_a__and(a__isNatKind(V1), isNatKind(V2)) ; Marked_a__isNatKind(x(V1,V2)) >= Marked_a__isNatKind(V1) ; Marked_a__isNatKind(x(V1,V2)) >= Marked_a__and(a__isNatKind(V1), isNatKind(V2)) ; Marked_a__and(tt,X) >= Marked_mark(X) ; Marked_a__x(N,s(M)) >= Marked_a__and(a__isNat(M),isNatKind(M)) ; Marked_a__x(N,s(M)) >= Marked_a__and(a__and(a__isNat(M),isNatKind(M)), and(isNat(N),isNatKind(N))) ; Marked_a__x(N,s(M)) >= Marked_a__U71(a__and(a__and(a__isNat(M),isNatKind(M)), and(isNat(N),isNatKind(N))),M, N) ; Marked_a__x(N,s(M)) >= Marked_a__isNat(M) ; Marked_a__x(N,0) >= Marked_a__and(a__isNat(N),isNatKind(N)) ; Marked_a__x(N,0) >= Marked_a__isNat(N) ; Marked_a__U71(tt,M,N) >= Marked_a__x(mark(N),mark(M)) ; Marked_a__U71(tt,M,N) >= Marked_a__plus(a__x(mark(N),mark(M)),mark(N)) ; Marked_a__U71(tt,M,N) >= Marked_mark(N) ; Marked_a__U71(tt,M,N) >= Marked_mark(M) ; Marked_a__plus(N,s(M)) >= Marked_a__and(a__isNat(M),isNatKind(M)) ; Marked_a__plus(N,s(M)) >= Marked_a__and(a__and(a__isNat(M),isNatKind(M)), and(isNat(N),isNatKind(N))) ; Marked_a__plus(N,s(M)) >= Marked_a__U51(a__and(a__and(a__isNat(M), isNatKind(M)), and(isNat(N),isNatKind(N))), M,N) ; Marked_a__plus(N,s(M)) >= Marked_a__isNat(M) ; Marked_a__plus(N,0) >= Marked_a__and(a__isNat(N),isNatKind(N)) ; Marked_a__plus(N,0) >= Marked_a__U41(a__and(a__isNat(N),isNatKind(N)),N) ; Marked_a__plus(N,0) >= Marked_a__isNat(N) ; Marked_a__U51(tt,M,N) >= Marked_a__plus(mark(N),mark(M)) ; Marked_a__U51(tt,M,N) >= Marked_mark(N) ; Marked_a__U51(tt,M,N) >= Marked_mark(M) ; Marked_a__U41(tt,N) >= Marked_mark(N) ; Marked_a__U32(tt,V2) >= Marked_a__isNat(V2) ; Marked_a__U31(tt,V1,V2) >= Marked_a__U32(a__isNat(V1),V2) ; Marked_a__U31(tt,V1,V2) >= Marked_a__isNat(V1) ; Marked_a__U21(tt,V1) >= Marked_a__isNat(V1) ; Marked_a__isNat(s(V1)) >= Marked_a__isNatKind(V1) ; Marked_a__isNat(s(V1)) >= Marked_a__U21(a__isNatKind(V1),V1) ; Marked_a__isNat(plus(V1,V2)) >= Marked_a__isNatKind(V1) ; Marked_a__isNat(plus(V1,V2)) >= Marked_a__and(a__isNatKind(V1),isNatKind(V2)) ; Marked_a__isNat(plus(V1,V2)) >= Marked_a__U11(a__and(a__isNatKind(V1), isNatKind(V2)),V1,V2) ; Marked_a__isNat(x(V1,V2)) >= Marked_a__isNatKind(V1) ; Marked_a__isNat(x(V1,V2)) >= Marked_a__and(a__isNatKind(V1),isNatKind(V2)) ; Marked_a__isNat(x(V1,V2)) >= Marked_a__U31(a__and(a__isNatKind(V1), isNatKind(V2)),V1,V2) ; Marked_a__U12(tt,V2) >= Marked_a__isNat(V2) ; Marked_a__U11(tt,V1,V2) >= Marked_a__isNat(V1) ; Marked_a__U11(tt,V1,V2) >= Marked_a__U12(a__isNat(V1),V2) ; Marked_mark(s(X)) >= Marked_mark(X) ; Marked_mark(isNatKind(X)) >= Marked_a__isNatKind(X) ; Marked_mark(plus(X1,X2)) >= Marked_a__plus(mark(X1),mark(X2)) ; Marked_mark(plus(X1,X2)) >= Marked_mark(X1) ; Marked_mark(plus(X1,X2)) >= Marked_mark(X2) ; Marked_mark(x(X1,X2)) >= Marked_a__x(mark(X1),mark(X2)) ; Marked_mark(x(X1,X2)) >= Marked_mark(X1) ; Marked_mark(x(X1,X2)) >= Marked_mark(X2) ; Marked_mark(and(X1,X2)) >= Marked_a__and(mark(X1),X2) ; Marked_mark(and(X1,X2)) >= Marked_mark(X1) ; Marked_mark(isNat(X)) >= Marked_a__isNat(X) ; Marked_mark(U11(X1,X2,X3)) >= Marked_a__U11(mark(X1),X2,X3) ; Marked_mark(U11(X1,X2,X3)) >= Marked_mark(X1) ; Marked_mark(U12(X1,X2)) >= Marked_a__U12(mark(X1),X2) ; Marked_mark(U12(X1,X2)) >= Marked_mark(X1) ; Marked_mark(U13(X)) >= Marked_mark(X) ; Marked_mark(U21(X1,X2)) >= Marked_a__U21(mark(X1),X2) ; Marked_mark(U21(X1,X2)) >= Marked_mark(X1) ; Marked_mark(U22(X)) >= Marked_mark(X) ; Marked_mark(U31(X1,X2,X3)) >= Marked_a__U31(mark(X1),X2,X3) ; Marked_mark(U31(X1,X2,X3)) >= Marked_mark(X1) ; Marked_mark(U32(X1,X2)) >= Marked_a__U32(mark(X1),X2) ; Marked_mark(U32(X1,X2)) >= Marked_mark(X1) ; Marked_mark(U33(X)) >= Marked_mark(X) ; Marked_mark(U41(X1,X2)) >= Marked_a__U41(mark(X1),X2) ; Marked_mark(U41(X1,X2)) >= Marked_mark(X1) ; Marked_mark(U51(X1,X2,X3)) >= Marked_a__U51(mark(X1),X2,X3) ; Marked_mark(U51(X1,X2,X3)) >= Marked_mark(X1) ; Marked_mark(U61(X)) >= Marked_mark(X) ; Marked_mark(U71(X1,X2,X3)) >= Marked_a__U71(mark(X1),X2,X3) ; Marked_mark(U71(X1,X2,X3)) >= Marked_mark(X1) ; } + Disjunctions:{ { Marked_a__isNatKind(s(V1)) > Marked_a__isNatKind(V1) ; } { Marked_a__isNatKind(plus(V1,V2)) > Marked_a__isNatKind(V1) ; } { Marked_a__isNatKind(plus(V1,V2)) > Marked_a__and(a__isNatKind(V1), isNatKind(V2)) ; } { Marked_a__isNatKind(x(V1,V2)) > Marked_a__isNatKind(V1) ; } { Marked_a__isNatKind(x(V1,V2)) > Marked_a__and(a__isNatKind(V1),isNatKind(V2)) ; } { Marked_a__and(tt,X) > Marked_mark(X) ; } { Marked_a__x(N,s(M)) > Marked_a__and(a__isNat(M),isNatKind(M)) ; } { Marked_a__x(N,s(M)) > Marked_a__and(a__and(a__isNat(M),isNatKind(M)), and(isNat(N),isNatKind(N))) ; } { Marked_a__x(N,s(M)) > Marked_a__U71(a__and(a__and(a__isNat(M),isNatKind(M)), and(isNat(N),isNatKind(N))),M, N) ; } { Marked_a__x(N,s(M)) > Marked_a__isNat(M) ; } { Marked_a__x(N,0) > Marked_a__and(a__isNat(N),isNatKind(N)) ; } { Marked_a__x(N,0) > Marked_a__isNat(N) ; } { Marked_a__U71(tt,M,N) > Marked_a__x(mark(N),mark(M)) ; } { Marked_a__U71(tt,M,N) > Marked_a__plus(a__x(mark(N),mark(M)),mark(N)) ; } { Marked_a__U71(tt,M,N) > Marked_mark(N) ; } { Marked_a__U71(tt,M,N) > Marked_mark(M) ; } { Marked_a__plus(N,s(M)) > Marked_a__and(a__isNat(M),isNatKind(M)) ; } { Marked_a__plus(N,s(M)) > Marked_a__and(a__and(a__isNat(M),isNatKind(M)), and(isNat(N),isNatKind(N))) ; } { Marked_a__plus(N,s(M)) > Marked_a__U51(a__and(a__and(a__isNat(M), isNatKind(M)), and(isNat(N),isNatKind(N))), M,N) ; } { Marked_a__plus(N,s(M)) > Marked_a__isNat(M) ; } { Marked_a__plus(N,0) > Marked_a__and(a__isNat(N),isNatKind(N)) ; } { Marked_a__plus(N,0) > Marked_a__U41(a__and(a__isNat(N),isNatKind(N)),N) ; } { Marked_a__plus(N,0) > Marked_a__isNat(N) ; } { Marked_a__U51(tt,M,N) > Marked_a__plus(mark(N),mark(M)) ; } { Marked_a__U51(tt,M,N) > Marked_mark(N) ; } { Marked_a__U51(tt,M,N) > Marked_mark(M) ; } { Marked_a__U41(tt,N) > Marked_mark(N) ; } { Marked_a__U32(tt,V2) > Marked_a__isNat(V2) ; } { Marked_a__U31(tt,V1,V2) > Marked_a__U32(a__isNat(V1),V2) ; } { Marked_a__U31(tt,V1,V2) > Marked_a__isNat(V1) ; } { Marked_a__U21(tt,V1) > Marked_a__isNat(V1) ; } { Marked_a__isNat(s(V1)) > Marked_a__isNatKind(V1) ; } { Marked_a__isNat(s(V1)) > Marked_a__U21(a__isNatKind(V1),V1) ; } { Marked_a__isNat(plus(V1,V2)) > Marked_a__isNatKind(V1) ; } { Marked_a__isNat(plus(V1,V2)) > Marked_a__and(a__isNatKind(V1),isNatKind(V2)) ; } { Marked_a__isNat(plus(V1,V2)) > Marked_a__U11(a__and(a__isNatKind(V1), isNatKind(V2)),V1,V2) ; } { Marked_a__isNat(x(V1,V2)) > Marked_a__isNatKind(V1) ; } { Marked_a__isNat(x(V1,V2)) > Marked_a__and(a__isNatKind(V1),isNatKind(V2)) ; } { Marked_a__isNat(x(V1,V2)) > Marked_a__U31(a__and(a__isNatKind(V1), isNatKind(V2)),V1,V2) ; } { Marked_a__U12(tt,V2) > Marked_a__isNat(V2) ; } { Marked_a__U11(tt,V1,V2) > Marked_a__isNat(V1) ; } { Marked_a__U11(tt,V1,V2) > Marked_a__U12(a__isNat(V1),V2) ; } { Marked_mark(s(X)) > Marked_mark(X) ; } { Marked_mark(isNatKind(X)) > Marked_a__isNatKind(X) ; } { Marked_mark(plus(X1,X2)) > Marked_a__plus(mark(X1),mark(X2)) ; } { Marked_mark(plus(X1,X2)) > Marked_mark(X1) ; } { Marked_mark(plus(X1,X2)) > Marked_mark(X2) ; } { Marked_mark(x(X1,X2)) > Marked_a__x(mark(X1),mark(X2)) ; } { Marked_mark(x(X1,X2)) > Marked_mark(X1) ; } { Marked_mark(x(X1,X2)) > Marked_mark(X2) ; } { Marked_mark(and(X1,X2)) > Marked_a__and(mark(X1),X2) ; } { Marked_mark(and(X1,X2)) > Marked_mark(X1) ; } { Marked_mark(isNat(X)) > Marked_a__isNat(X) ; } { Marked_mark(U11(X1,X2,X3)) > Marked_a__U11(mark(X1),X2,X3) ; } { Marked_mark(U11(X1,X2,X3)) > Marked_mark(X1) ; } { Marked_mark(U12(X1,X2)) > Marked_a__U12(mark(X1),X2) ; } { Marked_mark(U12(X1,X2)) > Marked_mark(X1) ; } { Marked_mark(U13(X)) > Marked_mark(X) ; } { Marked_mark(U21(X1,X2)) > Marked_a__U21(mark(X1),X2) ; } { Marked_mark(U21(X1,X2)) > Marked_mark(X1) ; } { Marked_mark(U22(X)) > Marked_mark(X) ; } { Marked_mark(U31(X1,X2,X3)) > Marked_a__U31(mark(X1),X2,X3) ; } { Marked_mark(U31(X1,X2,X3)) > Marked_mark(X1) ; } { Marked_mark(U32(X1,X2)) > Marked_a__U32(mark(X1),X2) ; } { Marked_mark(U32(X1,X2)) > Marked_mark(X1) ; } { Marked_mark(U33(X)) > Marked_mark(X) ; } { Marked_mark(U41(X1,X2)) > Marked_a__U41(mark(X1),X2) ; } { Marked_mark(U41(X1,X2)) > Marked_mark(X1) ; } { Marked_mark(U51(X1,X2,X3)) > Marked_a__U51(mark(X1),X2,X3) ; } { Marked_mark(U51(X1,X2,X3)) > Marked_mark(X1) ; } { Marked_mark(U61(X)) > Marked_mark(X) ; } { Marked_mark(U71(X1,X2,X3)) > Marked_a__U71(mark(X1),X2,X3) ; } { Marked_mark(U71(X1,X2,X3)) > Marked_mark(X1) ; } } === TIMER virtual : 10.000000 === Entering poly_solver Starting Sat solver initialization Calling Sat solver... === STOPING TIMER virtual === === TIMER real : 10.000000 === === STOPING TIMER real === Sat solver returned === STOPING TIMER real === === STOPING TIMER virtual === No solution found for these parameters. Entering rpo_solver === TIMER virtual : 25.000000 === Search parameters: AFS type: 2 ; time limit: 25.. === STOPING TIMER virtual === Time out for these parameters. === TIMER virtual : 15.000000 === Entering poly_solver Starting Sat solver initialization Calling Sat solver... === STOPING TIMER virtual === === TIMER real : 15.000000 === === STOPING TIMER real === Sat timeout reached === STOPING TIMER virtual === Time out for these parameters. === TIMER virtual : 50.000000 === trying sub matrices of size: 1 Matrix interpretation constraints generated. Search parameters: LINEAR MATRIX 3x3 (strict=1x1) ; time limit: 50.. Termination constraints generated. Starting Sat solver initialization Calling Sat solver... === STOPING TIMER virtual === === TIMER real : 50.000000 === === STOPING TIMER real === Sat solver returned === STOPING TIMER real === === STOPING TIMER virtual === No solution found for these parameters. No solution found for these constraints. APPLY CRITERIA (ID_CRIT) NOT SOLVED No proof found Cime worked for 113.524854 seconds (real time) Cime Exit Status: 0