- : unit = () h : heuristic = - : unit = () APPLY CRITERIA (Marked dependency pairs) TRS termination of: [1] app(app(app(compose,f),g),x) -> app(g,app(f,x)) [2] app(reverse,l) -> app(app(reverse2,l),nil) [3] app(app(reverse2,nil),l) -> l [4] app(app(reverse2,app(app(cons,x),xs)),l) -> app(app(reverse2,xs),app(app(cons,x),l)) [5] app(hd,app(app(cons,x),xs)) -> x [6] app(tl,app(app(cons,x),xs)) -> xs [7] last -> app(app(compose,hd),reverse) [8] init -> app(app(compose,reverse),app(app(compose,tl),reverse)) 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: { app(app(app(compose,f),g),x) >= app(g,app(f,x)) ; app(app(reverse2,app(app(cons,x),xs)),l) >= app(app(reverse2,xs), app(app(cons,x),l)) ; app(app(reverse2,nil),l) >= l ; app(reverse,l) >= app(app(reverse2,l),nil) ; app(hd,app(app(cons,x),xs)) >= x ; app(tl,app(app(cons,x),xs)) >= xs ; last >= app(app(compose,hd),reverse) ; init >= app(app(compose,reverse),app(app(compose,tl),reverse)) ; Marked_app(app(app(compose,f),g),x) >= Marked_app(f,x) ; Marked_app(app(app(compose,f),g),x) >= Marked_app(g,app(f,x)) ; Marked_app(app(reverse2,app(app(cons,x),xs)),l) >= Marked_app(app(reverse2, xs), app(app(cons,x),l)) ; Marked_app(app(reverse2,app(app(cons,x),xs)),l) >= Marked_app(app(cons,x),l) ; Marked_app(reverse,l) >= Marked_app(app(reverse2,l),nil) ; } + Disjunctions:{ { Marked_app(app(app(compose,f),g),x) > Marked_app(f,x) ; } { Marked_app(app(app(compose,f),g),x) > Marked_app(g,app(f,x)) ; } { Marked_app(app(reverse2,app(app(cons,x),xs)),l) > Marked_app(app(reverse2,xs), app(app(cons,x),l)) ; } { Marked_app(app(reverse2,app(app(cons,x),xs)),l) > Marked_app(app(cons,x),l) ; } { Marked_app(reverse,l) > Marked_app(app(reverse2,l),nil) ; } } === 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: app(app(app(compose,f),g),x) >= app(g,app(f,x)) constraint: app(app(reverse2,app(app(cons,x),xs)),l) >= app(app(reverse2,xs), app(app(cons,x),l)) constraint: app(app(reverse2,nil),l) >= l constraint: app(reverse,l) >= app(app(reverse2,l),nil) constraint: app(hd,app(app(cons,x),xs)) >= x constraint: app(tl,app(app(cons,x),xs)) >= xs constraint: last >= app(app(compose,hd),reverse) constraint: init >= app(app(compose,reverse),app(app(compose,tl),reverse)) constraint: Marked_app(app(app(compose,f),g),x) >= Marked_app(f,x) constraint: Marked_app(app(app(compose,f),g),x) >= Marked_app(g,app(f,x)) constraint: Marked_app(app(reverse2,app(app(cons,x),xs)),l) >= Marked_app( app(reverse2, xs), app(app(cons,x), l)) constraint: Marked_app(app(reverse2,app(app(cons,x),xs)),l) >= Marked_app( app(cons, x),l) constraint: Marked_app(reverse,l) >= Marked_app(app(reverse2,l),nil) APPLY CRITERIA (Graph splitting) Found 1 components: { --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> } APPLY CRITERIA (Choosing graph) Trying to solve the following constraints: { app(app(app(compose,f),g),x) >= app(g,app(f,x)) ; app(app(reverse2,app(app(cons,x),xs)),l) >= app(app(reverse2,xs), app(app(cons,x),l)) ; app(app(reverse2,nil),l) >= l ; app(reverse,l) >= app(app(reverse2,l),nil) ; app(hd,app(app(cons,x),xs)) >= x ; app(tl,app(app(cons,x),xs)) >= xs ; last >= app(app(compose,hd),reverse) ; init >= app(app(compose,reverse),app(app(compose,tl),reverse)) ; Marked_app(app(app(compose,f),g),x) >= Marked_app(f,x) ; Marked_app(app(app(compose,f),g),x) >= Marked_app(g,app(f,x)) ; Marked_app(app(reverse2,app(app(cons,x),xs)),l) >= Marked_app(app(reverse2, xs), app(app(cons,x),l)) ; Marked_app(app(reverse2,app(app(cons,x),xs)),l) >= Marked_app(app(cons,x),l) ; } + Disjunctions:{ { Marked_app(app(app(compose,f),g),x) > Marked_app(f,x) ; } { Marked_app(app(app(compose,f),g),x) > Marked_app(g,app(f,x)) ; } { Marked_app(app(reverse2,app(app(cons,x),xs)),l) > Marked_app(app(reverse2,xs), app(app(cons,x),l)) ; } { Marked_app(app(reverse2,app(app(cons,x),xs)),l) > Marked_app(app(cons,x),l) ; } } === 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: app(app(app(compose,f),g),x) >= app(g,app(f,x)) constraint: app(app(reverse2,app(app(cons,x),xs)),l) >= app(app(reverse2,xs), app(app(cons,x),l)) constraint: app(app(reverse2,nil),l) >= l constraint: app(reverse,l) >= app(app(reverse2,l),nil) constraint: app(hd,app(app(cons,x),xs)) >= x constraint: app(tl,app(app(cons,x),xs)) >= xs constraint: last >= app(app(compose,hd),reverse) constraint: init >= app(app(compose,reverse),app(app(compose,tl),reverse)) constraint: Marked_app(app(app(compose,f),g),x) >= Marked_app(f,x) constraint: Marked_app(app(app(compose,f),g),x) >= Marked_app(g,app(f,x)) constraint: Marked_app(app(reverse2,app(app(cons,x),xs)),l) >= Marked_app( app(reverse2, xs), app(app(cons,x), l)) constraint: Marked_app(app(reverse2,app(app(cons,x),xs)),l) >= Marked_app( app(cons, x),l) APPLY CRITERIA (Graph splitting) Found 1 components: { --> --> --> --> --> --> --> --> --> } APPLY CRITERIA (Choosing graph) Trying to solve the following constraints: { app(app(app(compose,f),g),x) >= app(g,app(f,x)) ; app(app(reverse2,app(app(cons,x),xs)),l) >= app(app(reverse2,xs), app(app(cons,x),l)) ; app(app(reverse2,nil),l) >= l ; app(reverse,l) >= app(app(reverse2,l),nil) ; app(hd,app(app(cons,x),xs)) >= x ; app(tl,app(app(cons,x),xs)) >= xs ; last >= app(app(compose,hd),reverse) ; init >= app(app(compose,reverse),app(app(compose,tl),reverse)) ; Marked_app(app(app(compose,f),g),x) >= Marked_app(f,x) ; Marked_app(app(app(compose,f),g),x) >= Marked_app(g,app(f,x)) ; Marked_app(app(reverse2,app(app(cons,x),xs)),l) >= Marked_app(app(cons,x),l) ; } + Disjunctions:{ { Marked_app(app(app(compose,f),g),x) > Marked_app(f,x) ; } { Marked_app(app(app(compose,f),g),x) > Marked_app(g,app(f,x)) ; } { Marked_app(app(reverse2,app(app(cons,x),xs)),l) > Marked_app(app(cons,x),l) ; } } === 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: app(app(app(compose,f),g),x) >= app(g,app(f,x)) constraint: app(app(reverse2,app(app(cons,x),xs)),l) >= app(app(reverse2,xs), app(app(cons,x),l)) constraint: app(app(reverse2,nil),l) >= l constraint: app(reverse,l) >= app(app(reverse2,l),nil) constraint: app(hd,app(app(cons,x),xs)) >= x constraint: app(tl,app(app(cons,x),xs)) >= xs constraint: last >= app(app(compose,hd),reverse) constraint: init >= app(app(compose,reverse),app(app(compose,tl),reverse)) constraint: Marked_app(app(app(compose,f),g),x) >= Marked_app(f,x) constraint: Marked_app(app(app(compose,f),g),x) >= Marked_app(g,app(f,x)) constraint: Marked_app(app(reverse2,app(app(cons,x),xs)),l) >= Marked_app( app(cons, x),l) APPLY CRITERIA (Graph splitting) Found 1 components: { --> --> --> --> } APPLY CRITERIA (Choosing graph) Trying to solve the following constraints: { app(app(app(compose,f),g),x) >= app(g,app(f,x)) ; app(app(reverse2,app(app(cons,x),xs)),l) >= app(app(reverse2,xs), app(app(cons,x),l)) ; app(app(reverse2,nil),l) >= l ; app(reverse,l) >= app(app(reverse2,l),nil) ; app(hd,app(app(cons,x),xs)) >= x ; app(tl,app(app(cons,x),xs)) >= xs ; last >= app(app(compose,hd),reverse) ; init >= app(app(compose,reverse),app(app(compose,tl),reverse)) ; Marked_app(app(app(compose,f),g),x) >= Marked_app(f,x) ; Marked_app(app(app(compose,f),g),x) >= Marked_app(g,app(f,x)) ; } + Disjunctions:{ { Marked_app(app(app(compose,f),g),x) > Marked_app(f,x) ; } { Marked_app(app(app(compose,f),g),x) > Marked_app(g,app(f,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: app(app(app(compose,f),g),x) >= app(g,app(f,x)) constraint: app(app(reverse2,app(app(cons,x),xs)),l) >= app(app(reverse2,xs), app(app(cons,x),l)) constraint: app(app(reverse2,nil),l) >= l constraint: app(reverse,l) >= app(app(reverse2,l),nil) constraint: app(hd,app(app(cons,x),xs)) >= x constraint: app(tl,app(app(cons,x),xs)) >= xs constraint: last >= app(app(compose,hd),reverse) constraint: init >= app(app(compose,reverse),app(app(compose,tl),reverse)) constraint: Marked_app(app(app(compose,f),g),x) >= Marked_app(f,x) constraint: Marked_app(app(app(compose,f),g),x) >= Marked_app(g,app(f,x)) APPLY CRITERIA (Graph splitting) Found 0 components: SOLVED { TRS termination of: [1] app(app(app(compose,f),g),x) -> app(g,app(f,x)) [2] app(reverse,l) -> app(app(reverse2,l),nil) [3] app(app(reverse2,nil),l) -> l [4] app(app(reverse2,app(app(cons,x),xs)),l) -> app(app(reverse2,xs),app(app(cons,x),l)) [5] app(hd,app(app(cons,x),xs)) -> x [6] app(tl,app(app(cons,x),xs)) -> xs [7] last -> app(app(compose,hd),reverse) [8] init -> app(app(compose,reverse),app(app(compose,tl),reverse)) , CRITERION: MDP [ { DP termination of: , CRITERION: SG [ { DP termination of: , CRITERION: CG using polynomial interpretation = [ app ] (X0,X1) = 1*X1 + 1*X0; [ last ] () = 3; [ reverse ] () = 1; [ reverse2 ] () = 0; [ hd ] () = 1; [ compose ] () = 0; [ init ] () = 3; [ cons ] () = 0; [ nil ] () = 0; [ Marked_app ] (X0,X1) = 2*X1 + 2*X0; [ tl ] () = 0; removing [ { DP termination of: , CRITERION: SG [ { DP termination of: , CRITERION: CG using polynomial interpretation = [ app ] (X0,X1) = 1*X1 + 1*X0; [ last ] () = 1; [ reverse ] () = 0; [ reverse2 ] () = 0; [ hd ] () = 0; [ compose ] () = 0; [ init ] () = 1; [ cons ] () = 2; [ nil ] () = 0; [ Marked_app ] (X0,X1) = 1*X0; [ tl ] () = 0; removing [ { DP termination of: , CRITERION: SG [ { DP termination of: , CRITERION: CG using polynomial interpretation = [ app ] (X0,X1) = 1*X1 + 1*X0; [ last ] () = 3; [ reverse ] () = 1; [ reverse2 ] () = 1; [ hd ] () = 0; [ compose ] () = 0; [ init ] () = 3; [ cons ] () = 2; [ nil ] () = 0; [ Marked_app ] (X0,X1) = 2*X1 + 3*X0; [ tl ] () = 0; removing [ { DP termination of: , CRITERION: SG [ { DP termination of: , CRITERION: ORD [ Solution found: polynomial interpretation = [ app ] (X0,X1) = 1*X0 + 1*X1 + 0; [ last ] () = 3 + 0; [ reverse ] () = 0; [ reverse2 ] () = 0; [ hd ] () = 0; [ compose ] () = 1 + 0; [ init ] () = 3 + 0; [ cons ] () = 3 + 0; [ nil ] () = 0; [ Marked_app ] (X0,X1) = 3*X0 + 3*X1 + 0; [ tl ] () = 0; ]} ]} ]} ]} ]} ]} ]} ]} ]} Cime worked for 0.421093 seconds (real time) Cime Exit Status: 0