- : unit = () - : unit = () h : heuristic = - : unit = () APPLY CRITERIA (Marked dependency pairs) TRS termination of: [1] zeros -> cons(0,n__zeros) [2] U11(tt,L) -> s(length(activate(L))) [3] and(tt,X) -> activate(X) [4] isNat(n__0) -> tt [5] isNat(n__length(V1)) -> isNatList(activate(V1)) [6] isNat(n__s(V1)) -> isNat(activate(V1)) [7] isNatIList(V) -> isNatList(activate(V)) [8] isNatIList(n__zeros) -> tt [9] isNatIList(n__cons(V1,V2)) -> and(isNat(activate(V1)),n__isNatIList(activate(V2))) [10] isNatList(n__nil) -> tt [11] isNatList(n__cons(V1,V2)) -> and(isNat(activate(V1)),n__isNatList(activate(V2))) [12] length(nil) -> 0 [13] length(cons(N,L)) -> U11(and(isNatList(activate(L)),n__isNat(N)),activate(L)) [14] zeros -> n__zeros [15] 0 -> n__0 [16] length(X) -> n__length(X) [17] s(X) -> n__s(X) [18] cons(X1,X2) -> n__cons(X1,X2) [19] isNatIList(X) -> n__isNatIList(X) [20] nil -> n__nil [21] isNatList(X) -> n__isNatList(X) [22] isNat(X) -> n__isNat(X) [23] activate(n__zeros) -> zeros [24] activate(n__0) -> 0 [25] activate(n__length(X)) -> length(activate(X)) [26] activate(n__s(X)) -> s(activate(X)) [27] activate(n__cons(X1,X2)) -> cons(activate(X1),X2) [28] activate(n__isNatIList(X)) -> isNatIList(X) [29] activate(n__nil) -> nil [30] activate(n__isNatList(X)) -> isNatList(X) [31] activate(n__isNat(X)) -> isNat(X) [32] activate(X) -> X Sub problem: guided: DP termination of: END GUIDED APPLY CRITERIA (Graph splitting) Found 1 components: { --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> } APPLY CRITERIA (Subterm criterion) APPLY CRITERIA (Choosing graph) Trying to solve the following constraints: { cons(X1,X2) >= n__cons(X1,X2) ; 0 >= n__0 ; zeros >= cons(0,n__zeros) ; zeros >= n__zeros ; s(X) >= n__s(X) ; length(cons(N,L)) >= U11(and(isNatList(activate(L)),n__isNat(N)),activate(L)) ; length(nil) >= 0 ; length(X) >= n__length(X) ; activate(n__zeros) >= zeros ; activate(n__0) >= 0 ; activate(n__length(X)) >= length(activate(X)) ; activate(n__s(X)) >= s(activate(X)) ; activate(n__isNatIList(X)) >= isNatIList(X) ; activate(n__cons(X1,X2)) >= cons(activate(X1),X2) ; activate(n__nil) >= nil ; activate(n__isNatList(X)) >= isNatList(X) ; activate(n__isNat(X)) >= isNat(X) ; activate(X) >= X ; U11(tt,L) >= s(length(activate(L))) ; and(tt,X) >= activate(X) ; isNat(n__0) >= tt ; isNat(n__length(V1)) >= isNatList(activate(V1)) ; isNat(n__s(V1)) >= isNat(activate(V1)) ; isNat(X) >= n__isNat(X) ; isNatList(n__cons(V1,V2)) >= and(isNat(activate(V1)), n__isNatList(activate(V2))) ; isNatList(n__nil) >= tt ; isNatList(X) >= n__isNatList(X) ; isNatIList(n__zeros) >= tt ; isNatIList(n__cons(V1,V2)) >= and(isNat(activate(V1)), n__isNatIList(activate(V2))) ; isNatIList(X) >= n__isNatIList(X) ; isNatIList(V) >= isNatList(activate(V)) ; nil >= n__nil ; Marked_activate(n__length(X)) >= Marked_activate(X) ; Marked_activate(n__length(X)) >= Marked_length(activate(X)) ; Marked_activate(n__s(X)) >= Marked_activate(X) ; Marked_activate(n__isNatIList(X)) >= Marked_isNatIList(X) ; Marked_activate(n__cons(X1,X2)) >= Marked_activate(X1) ; Marked_activate(n__isNatList(X)) >= Marked_isNatList(X) ; Marked_activate(n__isNat(X)) >= Marked_isNat(X) ; Marked_isNat(n__length(V1)) >= Marked_activate(V1) ; Marked_isNat(n__length(V1)) >= Marked_isNatList(activate(V1)) ; Marked_isNat(n__s(V1)) >= Marked_activate(V1) ; Marked_isNat(n__s(V1)) >= Marked_isNat(activate(V1)) ; Marked_isNatList(n__cons(V1,V2)) >= Marked_activate(V1) ; Marked_isNatList(n__cons(V1,V2)) >= Marked_activate(V2) ; Marked_isNatList(n__cons(V1,V2)) >= Marked_isNat(activate(V1)) ; Marked_isNatList(n__cons(V1,V2)) >= Marked_and(isNat(activate(V1)), n__isNatList(activate(V2))) ; Marked_isNatIList(n__cons(V1,V2)) >= Marked_activate(V1) ; Marked_isNatIList(n__cons(V1,V2)) >= Marked_activate(V2) ; Marked_isNatIList(n__cons(V1,V2)) >= Marked_isNat(activate(V1)) ; Marked_isNatIList(n__cons(V1,V2)) >= Marked_and(isNat(activate(V1)), n__isNatIList(activate(V2))) ; Marked_isNatIList(V) >= Marked_activate(V) ; Marked_isNatIList(V) >= Marked_isNatList(activate(V)) ; Marked_length(cons(N,L)) >= Marked_activate(L) ; Marked_length(cons(N,L)) >= Marked_isNatList(activate(L)) ; Marked_length(cons(N,L)) >= Marked_U11(and(isNatList(activate(L)), n__isNat(N)),activate(L)) ; Marked_length(cons(N,L)) >= Marked_and(isNatList(activate(L)),n__isNat(N)) ; Marked_U11(tt,L) >= Marked_activate(L) ; Marked_U11(tt,L) >= Marked_length(activate(L)) ; Marked_and(tt,X) >= Marked_activate(X) ; } + Disjunctions:{ { Marked_activate(n__length(X)) > Marked_activate(X) ; } { Marked_activate(n__length(X)) > Marked_length(activate(X)) ; } { Marked_activate(n__s(X)) > Marked_activate(X) ; } { Marked_activate(n__isNatIList(X)) > Marked_isNatIList(X) ; } { Marked_activate(n__cons(X1,X2)) > Marked_activate(X1) ; } { Marked_activate(n__isNatList(X)) > Marked_isNatList(X) ; } { Marked_activate(n__isNat(X)) > Marked_isNat(X) ; } { Marked_isNat(n__length(V1)) > Marked_activate(V1) ; } { Marked_isNat(n__length(V1)) > Marked_isNatList(activate(V1)) ; } { Marked_isNat(n__s(V1)) > Marked_activate(V1) ; } { Marked_isNat(n__s(V1)) > Marked_isNat(activate(V1)) ; } { Marked_isNatList(n__cons(V1,V2)) > Marked_activate(V1) ; } { Marked_isNatList(n__cons(V1,V2)) > Marked_activate(V2) ; } { Marked_isNatList(n__cons(V1,V2)) > Marked_isNat(activate(V1)) ; } { Marked_isNatList(n__cons(V1,V2)) > Marked_and(isNat(activate(V1)), n__isNatList(activate(V2))) ; } { Marked_isNatIList(n__cons(V1,V2)) > Marked_activate(V1) ; } { Marked_isNatIList(n__cons(V1,V2)) > Marked_activate(V2) ; } { Marked_isNatIList(n__cons(V1,V2)) > Marked_isNat(activate(V1)) ; } { Marked_isNatIList(n__cons(V1,V2)) > Marked_and(isNat(activate(V1)), n__isNatIList(activate(V2))) ; } { Marked_isNatIList(V) > Marked_activate(V) ; } { Marked_isNatIList(V) > Marked_isNatList(activate(V)) ; } { Marked_length(cons(N,L)) > Marked_activate(L) ; } { Marked_length(cons(N,L)) > Marked_isNatList(activate(L)) ; } { Marked_length(cons(N,L)) > Marked_U11(and(isNatList(activate(L)),n__isNat(N)), activate(L)) ; } { Marked_length(cons(N,L)) > Marked_and(isNatList(activate(L)),n__isNat(N)) ; } { Marked_U11(tt,L) > Marked_activate(L) ; } { Marked_U11(tt,L) > Marked_length(activate(L)) ; } { Marked_and(tt,X) > Marked_activate(X) ; } } === TIMER virtual : 10.000000 === Entering poly_solver Starting Sat solver initialization Calling Sat solver... === STOPING TIMER virtual === === TIMER real : 10.000000 === === STOPING TIMER real === Sat solver returned Sat solver result read === STOPING TIMER real === === STOPING TIMER virtual === constraint: cons(X1,X2) >= n__cons(X1,X2) constraint: 0 >= n__0 constraint: zeros >= cons(0,n__zeros) constraint: zeros >= n__zeros constraint: s(X) >= n__s(X) constraint: length(cons(N,L)) >= U11(and(isNatList(activate(L)),n__isNat(N)), activate(L)) constraint: length(nil) >= 0 constraint: length(X) >= n__length(X) constraint: activate(n__zeros) >= zeros constraint: activate(n__0) >= 0 constraint: activate(n__length(X)) >= length(activate(X)) constraint: activate(n__s(X)) >= s(activate(X)) constraint: activate(n__isNatIList(X)) >= isNatIList(X) constraint: activate(n__cons(X1,X2)) >= cons(activate(X1),X2) constraint: activate(n__nil) >= nil constraint: activate(n__isNatList(X)) >= isNatList(X) constraint: activate(n__isNat(X)) >= isNat(X) constraint: activate(X) >= X constraint: U11(tt,L) >= s(length(activate(L))) constraint: and(tt,X) >= activate(X) constraint: isNat(n__0) >= tt constraint: isNat(n__length(V1)) >= isNatList(activate(V1)) constraint: isNat(n__s(V1)) >= isNat(activate(V1)) constraint: isNat(X) >= n__isNat(X) constraint: isNatList(n__cons(V1,V2)) >= and(isNat(activate(V1)), n__isNatList(activate(V2))) constraint: isNatList(n__nil) >= tt constraint: isNatList(X) >= n__isNatList(X) constraint: isNatIList(n__zeros) >= tt constraint: isNatIList(n__cons(V1,V2)) >= and(isNat(activate(V1)), n__isNatIList(activate(V2))) constraint: isNatIList(X) >= n__isNatIList(X) constraint: isNatIList(V) >= isNatList(activate(V)) constraint: nil >= n__nil constraint: Marked_activate(n__length(X)) >= Marked_activate(X) constraint: Marked_activate(n__length(X)) >= Marked_length(activate(X)) constraint: Marked_activate(n__s(X)) >= Marked_activate(X) constraint: Marked_activate(n__isNatIList(X)) >= Marked_isNatIList(X) constraint: Marked_activate(n__cons(X1,X2)) >= Marked_activate(X1) constraint: Marked_activate(n__isNatList(X)) >= Marked_isNatList(X) constraint: Marked_activate(n__isNat(X)) >= Marked_isNat(X) constraint: Marked_isNat(n__length(V1)) >= Marked_activate(V1) constraint: Marked_isNat(n__length(V1)) >= Marked_isNatList(activate(V1)) constraint: Marked_isNat(n__s(V1)) >= Marked_activate(V1) constraint: Marked_isNat(n__s(V1)) >= Marked_isNat(activate(V1)) constraint: Marked_isNatList(n__cons(V1,V2)) >= Marked_activate(V1) constraint: Marked_isNatList(n__cons(V1,V2)) >= Marked_activate(V2) constraint: Marked_isNatList(n__cons(V1,V2)) >= Marked_isNat(activate(V1)) constraint: Marked_isNatList(n__cons(V1,V2)) >= Marked_and(isNat(activate(V1)), n__isNatList(activate(V2))) constraint: Marked_isNatIList(n__cons(V1,V2)) >= Marked_activate(V1) constraint: Marked_isNatIList(n__cons(V1,V2)) >= Marked_activate(V2) constraint: Marked_isNatIList(n__cons(V1,V2)) >= Marked_isNat(activate(V1)) constraint: Marked_isNatIList(n__cons(V1,V2)) >= Marked_and(isNat(activate(V1)), n__isNatIList(activate(V2))) constraint: Marked_isNatIList(V) >= Marked_activate(V) constraint: Marked_isNatIList(V) >= Marked_isNatList(activate(V)) constraint: Marked_length(cons(N,L)) >= Marked_activate(L) constraint: Marked_length(cons(N,L)) >= Marked_isNatList(activate(L)) constraint: Marked_length(cons(N,L)) >= Marked_U11(and(isNatList(activate(L)), n__isNat(N)),activate(L)) constraint: Marked_length(cons(N,L)) >= Marked_and(isNatList(activate(L)), n__isNat(N)) constraint: Marked_U11(tt,L) >= Marked_activate(L) constraint: Marked_U11(tt,L) >= Marked_length(activate(L)) constraint: Marked_and(tt,X) >= Marked_activate(X) APPLY CRITERIA (Graph splitting) Found 2 components: { --> --> } { --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> -->