- : unit = () h : heuristic = - : unit = () APPLY CRITERIA (Marked dependency pairs) TRS termination of: [1] app(app(apply,f_1),x) -> app(f_1,x) [2] app(id,x) -> x [3] app(app(app(uncurry,f_2),x),y) -> app(app(f_2,x),y) [4] app(app(app(swap,f_2),y),x) -> app(app(f_2,x),y) [5] app(app(app(compose,g_1),f_1),x) -> app(g_1,app(f_1,x)) [6] app(app(const,x),y) -> x [7] app(listify,x) -> app(app(cons,x),nil) [8] app(app(app(app(fold,f_3),g_2),x),nil) -> x [9] app(app(app(app(fold,f_3),g_2),x),app(app(cons,z),t)) -> app(app(f_3,app(g_2,z)),app(app(app(app(fold,f_3),g_2),x),t)) [10] app(sum,l) -> app(app(app(app(fold,add),id),0),l) [11] app(app(uncurry,app(app(fold,cons),id)),nil) -> id [12] append -> app(app(compose,app(app(swap,fold),cons)),id) [13] reverse -> app(app(uncurry,app(app(fold,app(swap,append)),listify)),nil) [14] length -> app(app(uncurry,app(app(fold,add),app(cons,1))),0) 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(app(fold,f_3),g_2),x),app(app(cons,z),t)) >= app(app(f_3, app(g_2,z)), app(app(app( app( fold, f_3), g_2), x),t)) ; app(app(app(app(fold,f_3),g_2),x),nil) >= x ; app(app(app(uncurry,f_2),x),y) >= app(app(f_2,x),y) ; app(app(app(swap,f_2),y),x) >= app(app(f_2,x),y) ; app(app(app(compose,g_1),f_1),x) >= app(g_1,app(f_1,x)) ; app(app(apply,f_1),x) >= app(f_1,x) ; app(app(uncurry,app(app(fold,cons),id)),nil) >= id ; app(app(const,x),y) >= x ; app(id,x) >= x ; app(listify,x) >= app(app(cons,x),nil) ; app(sum,l) >= app(app(app(app(fold,add),id),0),l) ; append >= app(app(compose,app(app(swap,fold),cons)),id) ; reverse >= app(app(uncurry,app(app(fold,app(swap,append)),listify)),nil) ; length >= app(app(uncurry,app(app(fold,add),app(cons,1))),0) ; Marked_app(app(app(app(fold,f_3),g_2),x),app(app(cons,z),t)) >= Marked_app( app( app( app( fold, f_3), g_2), x), t) ; Marked_app(app(app(app(fold,f_3),g_2),x),app(app(cons,z),t)) >= Marked_app( app( f_3, app(g_2,z)), app( app( app( app( fold, f_3), g_2), x), t)) ; Marked_app(app(app(app(fold,f_3),g_2),x),app(app(cons,z),t)) >= Marked_app( f_3, app(g_2,z)) ; Marked_app(app(app(app(fold,f_3),g_2),x),app(app(cons,z),t)) >= Marked_app( g_2, z) ; Marked_app(app(app(uncurry,f_2),x),y) >= Marked_app(app(f_2,x),y) ; Marked_app(app(app(uncurry,f_2),x),y) >= Marked_app(f_2,x) ; Marked_app(app(app(swap,f_2),y),x) >= Marked_app(app(f_2,x),y) ; Marked_app(app(app(swap,f_2),y),x) >= Marked_app(f_2,x) ; Marked_app(app(app(compose,g_1),f_1),x) >= Marked_app(f_1,x) ; Marked_app(app(app(compose,g_1),f_1),x) >= Marked_app(g_1,app(f_1,x)) ; Marked_app(app(apply,f_1),x) >= Marked_app(f_1,x) ; Marked_app(listify,x) >= Marked_app(app(cons,x),nil) ; Marked_app(sum,l) >= Marked_app(app(app(app(fold,add),id),0),l) ; Marked_app(sum,l) >= Marked_app(app(app(fold,add),id),0) ; Marked_app(sum,l) >= Marked_app(app(fold,add),id) ; } + Disjunctions:{ { Marked_app(app(app(app(fold,f_3),g_2),x),app(app(cons,z),t)) > Marked_app( app( app( app( fold, f_3), g_2), x), t) ; } { Marked_app(app(app(app(fold,f_3),g_2),x),app(app(cons,z),t)) > Marked_app( app( f_3, app(g_2,z)), app( app( app( app( fold, f_3), g_2), x), t)) ; } { Marked_app(app(app(app(fold,f_3),g_2),x),app(app(cons,z),t)) > Marked_app( f_3, app(g_2,z)) ; } { Marked_app(app(app(app(fold,f_3),g_2),x),app(app(cons,z),t)) > Marked_app( g_2, z) ; } { Marked_app(app(app(uncurry,f_2),x),y) > Marked_app(app(f_2,x),y) ; } { Marked_app(app(app(uncurry,f_2),x),y) > Marked_app(f_2,x) ; } { Marked_app(app(app(swap,f_2),y),x) > Marked_app(app(f_2,x),y) ; } { Marked_app(app(app(swap,f_2),y),x) > Marked_app(f_2,x) ; } { Marked_app(app(app(compose,g_1),f_1),x) > Marked_app(f_1,x) ; } { Marked_app(app(app(compose,g_1),f_1),x) > Marked_app(g_1,app(f_1,x)) ; } { Marked_app(app(apply,f_1),x) > Marked_app(f_1,x) ; } { Marked_app(listify,x) > Marked_app(app(cons,x),nil) ; } { Marked_app(sum,l) > Marked_app(app(app(app(fold,add),id),0),l) ; } { Marked_app(sum,l) > Marked_app(app(app(fold,add),id),0) ; } { Marked_app(sum,l) > Marked_app(app(fold,add),id) ; } } === 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 === === TIMER virtual : 25.000000 === Search parameters: AFS type: 2 ; time limit: 25.. === STOPING TIMER virtual === === TIMER virtual : 25.000000 === Search parameters: AFS type: 2 ; time limit: 25.. === STOPING TIMER virtual === === TIMER virtual : 25.000000 === Search parameters: AFS type: 2 ; time limit: 25.. === STOPING TIMER virtual === === TIMER virtual : 25.000000 === Search parameters: AFS type: 2 ; time limit: 25.. === STOPING TIMER virtual === === TIMER virtual : 25.000000 === Search parameters: AFS type: 2 ; time limit: 25.. === STOPING TIMER virtual === === TIMER virtual : 25.000000 === Search parameters: AFS type: 2 ; time limit: 25.. === STOPING TIMER virtual === === TIMER virtual : 25.000000 === Search parameters: AFS type: 2 ; time limit: 25.. === STOPING TIMER virtual === === TIMER virtual : 25.000000 === Search parameters: AFS type: 2 ; time limit: 25.. === STOPING TIMER virtual === === TIMER virtual : 25.000000 === Search parameters: AFS type: 2 ; time limit: 25.. === STOPING TIMER virtual === === TIMER virtual : 25.000000 === Search parameters: AFS type: 2 ; time limit: 25.. === STOPING TIMER virtual === === TIMER virtual : 25.000000 === Search parameters: AFS type: 2 ; time limit: 25.. === STOPING TIMER virtual === === TIMER virtual : 25.000000 === Search parameters: AFS type: 2 ; time limit: 25.. === STOPING TIMER virtual === === TIMER virtual : 25.000000 === Search parameters: AFS type: 2 ; time limit: 25.. === STOPING TIMER virtual === === TIMER virtual : 25.000000 === Search parameters: AFS type: 2 ; time limit: 25.. === STOPING TIMER virtual === === 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 solver returned === STOPING TIMER real === === STOPING TIMER virtual === No solution found 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 timeout reached === 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 88.717655 seconds (real time) Cime Exit Status: 0