- : unit = () h : heuristic = - : unit = () APPLY CRITERIA (Marked dependency pairs) TRS termination of: [1] pairNs -> cons(0,n__incr(n__oddNs)) [2] oddNs -> incr(pairNs) [3] incr(cons(X,XS)) -> cons(s(X),n__incr(activate(XS))) [4] take(0,XS) -> nil [5] take(s(N),cons(X,XS)) -> cons(X,n__take(N,activate(XS))) [6] zip(nil,XS) -> nil [7] zip(X,nil) -> nil [8] zip(cons(X,XS),cons(Y,YS)) -> cons(pair(X,Y),n__zip(activate(XS),activate(YS))) [9] tail(cons(X,XS)) -> activate(XS) [10] repItems(nil) -> nil [11] repItems(cons(X,XS)) -> cons(X,n__cons(X,n__repItems(activate(XS)))) [12] incr(X) -> n__incr(X) [13] oddNs -> n__oddNs [14] take(X1,X2) -> n__take(X1,X2) [15] zip(X1,X2) -> n__zip(X1,X2) [16] cons(X1,X2) -> n__cons(X1,X2) [17] repItems(X) -> n__repItems(X) [18] activate(n__incr(X)) -> incr(activate(X)) [19] activate(n__oddNs) -> oddNs [20] activate(n__take(X1,X2)) -> take(activate(X1),activate(X2)) [21] activate(n__zip(X1,X2)) -> zip(activate(X1),activate(X2)) [22] activate(n__cons(X1,X2)) -> cons(activate(X1),X2) [23] activate(n__repItems(X)) -> repItems(activate(X)) [24] activate(X) -> 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: { cons(X1,X2) >= n__cons(X1,X2) ; pairNs >= cons(0,n__incr(n__oddNs)) ; incr(cons(X,XS)) >= cons(s(X),n__incr(activate(XS))) ; incr(X) >= n__incr(X) ; oddNs >= n__oddNs ; oddNs >= incr(pairNs) ; activate(n__incr(X)) >= incr(activate(X)) ; activate(n__oddNs) >= oddNs ; activate(n__take(X1,X2)) >= take(activate(X1),activate(X2)) ; activate(n__zip(X1,X2)) >= zip(activate(X1),activate(X2)) ; activate(n__cons(X1,X2)) >= cons(activate(X1),X2) ; activate(n__repItems(X)) >= repItems(activate(X)) ; activate(X) >= X ; take(0,XS) >= nil ; take(s(N),cons(X,XS)) >= cons(X,n__take(N,activate(XS))) ; take(X1,X2) >= n__take(X1,X2) ; zip(cons(X,XS),cons(Y,YS)) >= cons(pair(X,Y), n__zip(activate(XS),activate(YS))) ; zip(nil,XS) >= nil ; zip(X,nil) >= nil ; zip(X1,X2) >= n__zip(X1,X2) ; tail(cons(X,XS)) >= activate(XS) ; repItems(cons(X,XS)) >= cons(X,n__cons(X,n__repItems(activate(XS)))) ; repItems(nil) >= nil ; repItems(X) >= n__repItems(X) ; Marked_activate(n__incr(X)) >= Marked_activate(X) ; Marked_activate(n__incr(X)) >= Marked_incr(activate(X)) ; Marked_activate(n__oddNs) >= Marked_oddNs ; Marked_activate(n__take(X1,X2)) >= Marked_activate(X1) ; Marked_activate(n__take(X1,X2)) >= Marked_activate(X2) ; Marked_activate(n__take(X1,X2)) >= Marked_take(activate(X1),activate(X2)) ; Marked_activate(n__zip(X1,X2)) >= Marked_activate(X1) ; Marked_activate(n__zip(X1,X2)) >= Marked_activate(X2) ; Marked_activate(n__zip(X1,X2)) >= Marked_zip(activate(X1),activate(X2)) ; Marked_activate(n__cons(X1,X2)) >= Marked_activate(X1) ; Marked_activate(n__repItems(X)) >= Marked_activate(X) ; Marked_activate(n__repItems(X)) >= Marked_repItems(activate(X)) ; Marked_repItems(cons(X,XS)) >= Marked_activate(XS) ; Marked_zip(cons(X,XS),cons(Y,YS)) >= Marked_activate(XS) ; Marked_zip(cons(X,XS),cons(Y,YS)) >= Marked_activate(YS) ; Marked_take(s(N),cons(X,XS)) >= Marked_activate(XS) ; Marked_oddNs >= Marked_incr(pairNs) ; Marked_incr(cons(X,XS)) >= Marked_activate(XS) ; } + Disjunctions:{ { Marked_activate(n__incr(X)) > Marked_activate(X) ; } { Marked_activate(n__incr(X)) > Marked_incr(activate(X)) ; } { Marked_activate(n__oddNs) > Marked_oddNs ; } { Marked_activate(n__take(X1,X2)) > Marked_activate(X1) ; } { Marked_activate(n__take(X1,X2)) > Marked_activate(X2) ; } { Marked_activate(n__take(X1,X2)) > Marked_take(activate(X1),activate(X2)) ; } { Marked_activate(n__zip(X1,X2)) > Marked_activate(X1) ; } { Marked_activate(n__zip(X1,X2)) > Marked_activate(X2) ; } { Marked_activate(n__zip(X1,X2)) > Marked_zip(activate(X1),activate(X2)) ; } { Marked_activate(n__cons(X1,X2)) > Marked_activate(X1) ; } { Marked_activate(n__repItems(X)) > Marked_activate(X) ; } { Marked_activate(n__repItems(X)) > Marked_repItems(activate(X)) ; } { Marked_repItems(cons(X,XS)) > Marked_activate(XS) ; } { Marked_zip(cons(X,XS),cons(Y,YS)) > Marked_activate(XS) ; } { Marked_zip(cons(X,XS),cons(Y,YS)) > Marked_activate(YS) ; } { Marked_take(s(N),cons(X,XS)) > Marked_activate(XS) ; } { Marked_oddNs > Marked_incr(pairNs) ; } { Marked_incr(cons(X,XS)) > Marked_activate(XS) ; } } === 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: pairNs >= cons(0,n__incr(n__oddNs)) constraint: incr(cons(X,XS)) >= cons(s(X),n__incr(activate(XS))) constraint: incr(X) >= n__incr(X) constraint: oddNs >= n__oddNs constraint: oddNs >= incr(pairNs) constraint: activate(n__incr(X)) >= incr(activate(X)) constraint: activate(n__oddNs) >= oddNs constraint: activate(n__take(X1,X2)) >= take(activate(X1),activate(X2)) constraint: activate(n__zip(X1,X2)) >= zip(activate(X1),activate(X2)) constraint: activate(n__cons(X1,X2)) >= cons(activate(X1),X2) constraint: activate(n__repItems(X)) >= repItems(activate(X)) constraint: activate(X) >= X constraint: take(0,XS) >= nil constraint: take(s(N),cons(X,XS)) >= cons(X,n__take(N,activate(XS))) constraint: take(X1,X2) >= n__take(X1,X2) constraint: zip(cons(X,XS),cons(Y,YS)) >= cons(pair(X,Y), n__zip(activate(XS),activate(YS))) constraint: zip(nil,XS) >= nil constraint: zip(X,nil) >= nil constraint: zip(X1,X2) >= n__zip(X1,X2) constraint: tail(cons(X,XS)) >= activate(XS) constraint: repItems(cons(X,XS)) >= cons(X, n__cons(X,n__repItems(activate(XS)))) constraint: repItems(nil) >= nil constraint: repItems(X) >= n__repItems(X) constraint: Marked_activate(n__incr(X)) >= Marked_activate(X) constraint: Marked_activate(n__incr(X)) >= Marked_incr(activate(X)) constraint: Marked_activate(n__oddNs) >= Marked_oddNs constraint: Marked_activate(n__take(X1,X2)) >= Marked_activate(X1) constraint: Marked_activate(n__take(X1,X2)) >= Marked_activate(X2) constraint: Marked_activate(n__take(X1,X2)) >= Marked_take(activate(X1), activate(X2)) constraint: Marked_activate(n__zip(X1,X2)) >= Marked_activate(X1) constraint: Marked_activate(n__zip(X1,X2)) >= Marked_activate(X2) constraint: Marked_activate(n__zip(X1,X2)) >= Marked_zip(activate(X1), activate(X2)) constraint: Marked_activate(n__cons(X1,X2)) >= Marked_activate(X1) constraint: Marked_activate(n__repItems(X)) >= Marked_activate(X) constraint: Marked_activate(n__repItems(X)) >= Marked_repItems(activate(X)) constraint: Marked_repItems(cons(X,XS)) >= Marked_activate(XS) constraint: Marked_zip(cons(X,XS),cons(Y,YS)) >= Marked_activate(XS) constraint: Marked_zip(cons(X,XS),cons(Y,YS)) >= Marked_activate(YS) constraint: Marked_take(s(N),cons(X,XS)) >= Marked_activate(XS) constraint: Marked_oddNs >= Marked_incr(pairNs) constraint: Marked_incr(cons(X,XS)) >= Marked_activate(XS) APPLY CRITERIA (Graph splitting) Found 1 components: { --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> -->