- : unit = () - : unit = () h : heuristic = - : unit = () APPLY CRITERIA (Marked dependency pairs) TRS termination of: [1] app'(app'(eq,0),0) -> true [2] app'(app'(eq,0),app'(s,x)) -> false [3] app'(app'(eq,app'(s,x)),0) -> false [4] app'(app'(eq,app'(s,x)),app'(s,y)) -> app'(app'(eq,x),y) [5] app'(app'(le,0),y) -> true [6] app'(app'(le,app'(s,x)),0) -> false [7] app'(app'(le,app'(s,x)),app'(s,y)) -> app'(app'(le,x),y) [8] app'(app'(app,nil),y) -> y [9] app'(app'(app,app'(app'(add,n),x)),y) -> app'(app'(add,n),app'(app'(app,x),y)) [10] app'(min,app'(app'(add,n),nil)) -> n [11] app'(min,app'(app'(add,n),app'(app'(add,m),x))) -> app'(app'(if_min,app'(app'(le,n),m)),app'(app'(add,n),app'(app'(add,m),x))) [12] app'(app'(if_min,true),app'(app'(add,n),app'(app'(add,m),x))) -> app'(min,app'(app'(add,n),x)) [13] app'(app'(if_min,false),app'(app'(add,n),app'(app'(add,m),x))) -> app'(min,app'(app'(add,m),x)) [14] app'(app'(rm,n),nil) -> nil [15] app'(app'(rm,n),app'(app'(add,m),x)) -> app'(app'(app'(if_rm,app'(app'(eq,n),m)),n),app'(app'(add,m),x)) [16] app'(app'(app'(if_rm,true),n),app'(app'(add,m),x)) -> app'(app'(rm,n),x) [17] app'(app'(app'(if_rm,false),n),app'(app'(add,m),x)) -> app'(app'(add,m),app'(app'(rm,n),x)) [18] app'(app'(minsort,nil),nil) -> nil [19] app'(app'(minsort,app'(app'(add,n),x)),y) -> app'(app'(app'(if_minsort,app'(app'(eq,n),app'(min,app'(app'(add,n),x)))), app'(app'(add,n),x)),y) [20] app'(app'(app'(if_minsort,true),app'(app'(add,n),x)),y) -> app'(app'(add,n),app'(app'(minsort,app'(app'(app,app'(app'(rm,n),x)),y)),nil)) [21] app'(app'(app'(if_minsort,false),app'(app'(add,n),x)),y) -> app'(app'(minsort,x),app'(app'(add,n),y)) [22] app'(app'(map,f),nil) -> nil [23] app'(app'(map,f),app'(app'(add,x),xs)) -> app'(app'(add,app'(f,x)),app'(app'(map,f),xs)) [24] app'(app'(filter,f),nil) -> nil [25] app'(app'(filter,f),app'(app'(add,x),xs)) -> app'(app'(app'(app'(filter2,app'(f,x)),f),x),xs) [26] app'(app'(app'(app'(filter2,true),f),x),xs) -> app'(app'(add,x),app'(app'(filter,f),xs)) [27] app'(app'(app'(app'(filter2,false),f),x),xs) -> app'(app'(filter,f),xs) 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: { app'(app'(app'(app'(filter2,true),f),x),xs) >= app'(app'(add,x), app'(app'(filter,f),xs)) ; app'(app'(app'(app'(filter2,false),f),x),xs) >= app'(app'(filter,f),xs) ; app'(app'(app'(if_rm,true),n),app'(app'(add,m),x)) >= app'(app'(rm,n),x) ; app'(app'(app'(if_rm,false),n),app'(app'(add,m),x)) >= app'(app'(add,m), app'(app'(rm,n),x)) ; app'(app'(app'(if_minsort,true),app'(app'(add,n),x)),y) >= app'(app'(add,n), app'(app'( minsort, app'( app'( app, app'( app'( rm, n), x)), y)), nil)) ; app'(app'(app'(if_minsort,false),app'(app'(add,n),x)),y) >= app'(app'( minsort, x), app'(app'(add,n), y)) ; app'(app'(eq,app'(s,x)),app'(s,y)) >= app'(app'(eq,x),y) ; app'(app'(eq,app'(s,x)),0) >= false ; app'(app'(eq,0),app'(s,x)) >= false ; app'(app'(eq,0),0) >= true ; app'(app'(le,app'(s,x)),app'(s,y)) >= app'(app'(le,x),y) ; app'(app'(le,app'(s,x)),0) >= false ; app'(app'(le,0),y) >= true ; app'(app'(app,app'(app'(add,n),x)),y) >= app'(app'(add,n), app'(app'(app,x),y)) ; app'(app'(app,nil),y) >= y ; app'(app'(if_min,true),app'(app'(add,n),app'(app'(add,m),x))) >= app'( min, app'( app'( add, n), x)) ; app'(app'(if_min,false),app'(app'(add,n),app'(app'(add,m),x))) >= app'( min, app'( app'( add, m), x)) ; app'(app'(rm,n),app'(app'(add,m),x)) >= app'(app'(app'(if_rm, app'(app'(eq,n),m)), n),app'(app'(add,m),x)) ; app'(app'(rm,n),nil) >= nil ; app'(app'(minsort,app'(app'(add,n),x)),y) >= app'(app'(app'(if_minsort, app'(app'(eq,n), app'(min, app'(app'(add,n),x))) ), app'(app'(add,n),x)), y) ; app'(app'(minsort,nil),nil) >= nil ; app'(app'(map,f),app'(app'(add,x),xs)) >= app'(app'(add,app'(f,x)), app'(app'(map,f),xs)) ; app'(app'(map,f),nil) >= nil ; app'(app'(filter,f),app'(app'(add,x),xs)) >= app'(app'(app'(app'(filter2, app'(f,x)), f),x),xs) ; app'(app'(filter,f),nil) >= nil ; app'(min,app'(app'(add,n),app'(app'(add,m),x))) >= app'(app'(if_min, app'(app'(le,n),m)), app'(app'(add,n), app'(app'(add,m),x))) ; app'(min,app'(app'(add,n),nil)) >= n ; Marked_app'(app'(app'(app'(filter2,true),f),x),xs) >= Marked_app'(app'(add,x), app'(app'(filter,f), xs)) ; Marked_app'(app'(app'(app'(filter2,true),f),x),xs) >= Marked_app'(app'( filter, f), xs) ; Marked_app'(app'(app'(app'(filter2,false),f),x),xs) >= Marked_app'( app'(filter, f),xs) ; Marked_app'(app'(app'(if_rm,true),n),app'(app'(add,m),x)) >= Marked_app'( app'( rm,n), x) ; Marked_app'(app'(app'(if_rm,false),n),app'(app'(add,m),x)) >= Marked_app'( app'( add, m), app'( app'( rm, n), x)) ; Marked_app'(app'(app'(if_rm,false),n),app'(app'(add,m),x)) >= Marked_app'( app'( rm, n), x) ; Marked_app'(app'(app'(if_minsort,true),app'(app'(add,n),x)),y) >= Marked_app'( app'( app, app'( app'( rm, n), x)), y) ; Marked_app'(app'(app'(if_minsort,true),app'(app'(add,n),x)),y) >= Marked_app'( app'( add, n), app'( app'( minsort, app'( app'( app, app'( app'( rm, n), x)), y)), nil)) ; Marked_app'(app'(app'(if_minsort,true),app'(app'(add,n),x)),y) >= Marked_app'( app'( rm, n), x) ; Marked_app'(app'(app'(if_minsort,true),app'(app'(add,n),x)),y) >= Marked_app'( app'( minsort, app'( app'( app, app'( app'( rm, n), x)), y)), nil) ; Marked_app'(app'(app'(if_minsort,false),app'(app'(add,n),x)),y) >= Marked_app'(app'(add,n),y) ; Marked_app'(app'(app'(if_minsort,false),app'(app'(add,n),x)),y) >= Marked_app'(app'(minsort,x),app'(app'(add,n),y)) ; Marked_app'(app'(eq,app'(s,x)),app'(s,y)) >= Marked_app'(app'(eq,x),y) ; Marked_app'(app'(le,app'(s,x)),app'(s,y)) >= Marked_app'(app'(le,x),y) ; Marked_app'(app'(app,app'(app'(add,n),x)),y) >= Marked_app'(app'(app,x),y) ; Marked_app'(app'(app,app'(app'(add,n),x)),y) >= Marked_app'(app'(add,n), app'(app'(app,x),y)) ; Marked_app'(app'(if_min,true),app'(app'(add,n),app'(app'(add,m),x))) >= Marked_app'(app'(add,n),x) ; Marked_app'(app'(if_min,true),app'(app'(add,n),app'(app'(add,m),x))) >= Marked_app'(min,app'(app'(add,n),x)) ; Marked_app'(app'(if_min,false),app'(app'(add,n),app'(app'(add,m),x))) >= Marked_app'(min,app'(app'(add,m),x)) ; Marked_app'(app'(rm,n),app'(app'(add,m),x)) >= Marked_app'(app'(app'( if_rm, app'( app'( eq, n), m)), n), app'(app'(add,m),x)) ; Marked_app'(app'(rm,n),app'(app'(add,m),x)) >= Marked_app'(app'(eq,n),m) ; Marked_app'(app'(rm,n),app'(app'(add,m),x)) >= Marked_app'(app'(if_rm, app'(app'(eq,n), m)),n) ; Marked_app'(app'(minsort,app'(app'(add,n),x)),y) >= Marked_app'(app'( app'( if_minsort, app'( app'( eq, n), app'( min, app'( app'( add, n), x)))), app'( app'( add, n), x)), y) ; Marked_app'(app'(minsort,app'(app'(add,n),x)),y) >= Marked_app'(app'(eq,n), app'(min, app'(app'(add,n),x))) ; Marked_app'(app'(minsort,app'(app'(add,n),x)),y) >= Marked_app'(app'( if_minsort, app'( app'( eq, n), app'( min, app'( app'( add, n), x)))), app'(app'(add,n),x)) ; Marked_app'(app'(minsort,app'(app'(add,n),x)),y) >= Marked_app'(min, app'(app'(add,n),x)) ; Marked_app'(app'(map,f),app'(app'(add,x),xs)) >= Marked_app'(app'(add, app'(f,x)), app'(app'(map,f),xs)) ; Marked_app'(app'(map,f),app'(app'(add,x),xs)) >= Marked_app'(app'(map,f),xs) ; Marked_app'(app'(map,f),app'(app'(add,x),xs)) >= Marked_app'(f,x) ; Marked_app'(app'(filter,f),app'(app'(add,x),xs)) >= Marked_app'(app'( app'( app'( filter2, app'(f,x)), f), x), xs) ; Marked_app'(app'(filter,f),app'(app'(add,x),xs)) >= Marked_app'(app'( app'( filter2, app'(f,x)), f), x) ; Marked_app'(app'(filter,f),app'(app'(add,x),xs)) >= Marked_app'(app'( filter2, app'(f,x)), f) ; Marked_app'(app'(filter,f),app'(app'(add,x),xs)) >= Marked_app'(f,x) ; Marked_app'(min,app'(app'(add,n),app'(app'(add,m),x))) >= Marked_app'( app'(le, n),m) ; Marked_app'(min,app'(app'(add,n),app'(app'(add,m),x))) >= Marked_app'( app'(if_min, app'(app'(le,n), m)), app'(app'(add,n), app'(app'(add,m), x))) ; } + Disjunctions:{ { Marked_app'(app'(app'(app'(filter2,true),f),x),xs) > Marked_app'(app'(add,x), app'(app'(filter,f),xs)) ; } { Marked_app'(app'(app'(app'(filter2,true),f),x),xs) > Marked_app'(app'( filter, f), xs) ; } { Marked_app'(app'(app'(app'(filter2,false),f),x),xs) > Marked_app'(app'( filter, f), xs) ; } { Marked_app'(app'(app'(if_rm,true),n),app'(app'(add,m),x)) > Marked_app'( app'(rm, n),x) ; } { Marked_app'(app'(app'(if_rm,false),n),app'(app'(add,m),x)) > Marked_app'( app'( add, m), app'( app'(rm,n), x)) ; } { Marked_app'(app'(app'(if_rm,false),n),app'(app'(add,m),x)) > Marked_app'( app'( rm,n), x) ; } { Marked_app'(app'(app'(if_minsort,true),app'(app'(add,n),x)),y) > Marked_app'( app'( app, app'( app'( rm, n), x)), y) ; } { Marked_app'(app'(app'(if_minsort,true),app'(app'(add,n),x)),y) > Marked_app'( app'( add, n), app'( app'( minsort, app'( app'( app, app'( app'( rm, n), x)), y)), nil)) ; } { Marked_app'(app'(app'(if_minsort,true),app'(app'(add,n),x)),y) > Marked_app'( app'( rm, n), x) ; } { Marked_app'(app'(app'(if_minsort,true),app'(app'(add,n),x)),y) > Marked_app'( app'( minsort, app'( app'( app, app'( app'( rm, n), x)), y)), nil) ; } { Marked_app'(app'(app'(if_minsort,false),app'(app'(add,n),x)),y) > Marked_app'( app'( add, n), y) ; } { Marked_app'(app'(app'(if_minsort,false),app'(app'(add,n),x)),y) > Marked_app'( app'( minsort, x), app'( app'( add, n), y)) ; } { Marked_app'(app'(eq,app'(s,x)),app'(s,y)) > Marked_app'(app'(eq,x),y) ; } { Marked_app'(app'(le,app'(s,x)),app'(s,y)) > Marked_app'(app'(le,x),y) ; } { Marked_app'(app'(app,app'(app'(add,n),x)),y) > Marked_app'(app'(app,x),y) ; } { Marked_app'(app'(app,app'(app'(add,n),x)),y) > Marked_app'(app'(add,n), app'(app'(app,x),y)) ; } { Marked_app'(app'(if_min,true),app'(app'(add,n),app'(app'(add,m),x))) > Marked_app'(app'(add,n),x) ; } { Marked_app'(app'(if_min,true),app'(app'(add,n),app'(app'(add,m),x))) > Marked_app'(min,app'(app'(add,n),x)) ; } { Marked_app'(app'(if_min,false),app'(app'(add,n),app'(app'(add,m),x))) > Marked_app'(min,app'(app'(add,m),x)) ; } { Marked_app'(app'(rm,n),app'(app'(add,m),x)) > Marked_app'(app'(app'( if_rm, app'( app'( eq, n), m)), n), app'(app'(add,m),x)) ; } { Marked_app'(app'(rm,n),app'(app'(add,m),x)) > Marked_app'(app'(eq,n),m) ; } { Marked_app'(app'(rm,n),app'(app'(add,m),x)) > Marked_app'(app'(if_rm, app'(app'(eq,n),m)), n) ; } { Marked_app'(app'(minsort,app'(app'(add,n),x)),y) > Marked_app'(app'( app'( if_minsort, app'( app'( eq, n), app'( min, app'( app'( add, n), x)))), app'( app'( add, n), x)), y) ; } { Marked_app'(app'(minsort,app'(app'(add,n),x)),y) > Marked_app'(app'(eq,n), app'(min, app'(app'(add,n),x))) ; } { Marked_app'(app'(minsort,app'(app'(add,n),x)),y) > Marked_app'(app'( if_minsort, app'( app'( eq, n), app'( min, app'( app'( add, n), x)))), app'(app'(add,n),x)) ; } { Marked_app'(app'(minsort,app'(app'(add,n),x)),y) > Marked_app'(min, app'(app'(add,n),x)) ; } { Marked_app'(app'(map,f),app'(app'(add,x),xs)) > Marked_app'(app'(add, app'(f,x)), app'(app'(map,f),xs)) ; } { Marked_app'(app'(map,f),app'(app'(add,x),xs)) > Marked_app'(app'(map,f),xs) ; } { Marked_app'(app'(map,f),app'(app'(add,x),xs)) > Marked_app'(f,x) ; } { Marked_app'(app'(filter,f),app'(app'(add,x),xs)) > Marked_app'(app'( app'( app'( filter2, app'(f,x)), f), x), xs) ; } { Marked_app'(app'(filter,f),app'(app'(add,x),xs)) > Marked_app'(app'( app'( filter2, app'(f,x)), f), x) ; } { Marked_app'(app'(filter,f),app'(app'(add,x),xs)) > Marked_app'(app'( filter2, app'(f,x)), f) ; } { Marked_app'(app'(filter,f),app'(app'(add,x),xs)) > Marked_app'(f,x) ; } { Marked_app'(min,app'(app'(add,n),app'(app'(add,m),x))) > Marked_app'( app'(le,n), m) ; } { Marked_app'(min,app'(app'(add,n),app'(app'(add,m),x))) > Marked_app'( app'(if_min, app'(app'(le,n),m)), app'(app'(add,n), app'(app'(add,m), 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 === 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 : 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 : 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 === 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 === STOPING TIMER virtual === No solution found for these parameters. No solution found for these constraints. APPLY CRITERIA (Simple graph) Found the following constraints: { app'(app'(app'(app'(filter2,true),f),x),xs) >= app'(app'(add,x), app'(app'(filter,f),xs)) ; app'(app'(app'(app'(filter2,false),f),x),xs) >= app'(app'(filter,f),xs) ; app'(app'(app'(if_rm,true),n),app'(app'(add,m),x)) >= app'(app'(rm,n),x) ; app'(app'(app'(if_rm,false),n),app'(app'(add,m),x)) >= app'(app'(add,m), app'(app'(rm,n),x)) ; app'(app'(app'(if_minsort,true),app'(app'(add,n),x)),y) >= app'(app'(add,n), app'(app'( minsort, app'( app'( app, app'( app'( rm, n), x)), y)), nil)) ; app'(app'(app'(if_minsort,false),app'(app'(add,n),x)),y) >= app'(app'( minsort, x), app'(app'(add,n), y)) ; app'(app'(eq,app'(s,x)),app'(s,y)) >= app'(app'(eq,x),y) ; app'(app'(eq,app'(s,x)),0) >= false ; app'(app'(eq,0),app'(s,x)) >= false ; app'(app'(eq,0),0) >= true ; app'(app'(le,app'(s,x)),app'(s,y)) >= app'(app'(le,x),y) ; app'(app'(le,app'(s,x)),0) >= false ; app'(app'(le,0),y) >= true ; app'(app'(app,app'(app'(add,n),x)),y) >= app'(app'(add,n), app'(app'(app,x),y)) ; app'(app'(app,nil),y) >= y ; app'(app'(if_min,true),app'(app'(add,n),app'(app'(add,m),x))) >= app'( min, app'( app'( add, n), x)) ; app'(app'(if_min,false),app'(app'(add,n),app'(app'(add,m),x))) >= app'( min, app'( app'( add, m), x)) ; app'(app'(rm,n),app'(app'(add,m),x)) >= app'(app'(app'(if_rm, app'(app'(eq,n),m)), n),app'(app'(add,m),x)) ; app'(app'(rm,n),nil) >= nil ; app'(app'(minsort,app'(app'(add,n),x)),y) >= app'(app'(app'(if_minsort, app'(app'(eq,n), app'(min, app'(app'(add,n),x))) ), app'(app'(add,n),x)), y) ; app'(app'(minsort,nil),nil) >= nil ; app'(app'(map,f),app'(app'(add,x),xs)) >= app'(app'(add,app'(f,x)), app'(app'(map,f),xs)) ; app'(app'(map,f),nil) >= nil ; app'(app'(filter,f),app'(app'(add,x),xs)) >= app'(app'(app'(app'(filter2, app'(f,x)), f),x),xs) ; app'(app'(filter,f),nil) >= nil ; app'(min,app'(app'(add,n),app'(app'(add,m),x))) >= app'(app'(if_min, app'(app'(le,n),m)), app'(app'(add,n), app'(app'(add,m),x))) ; app'(min,app'(app'(add,n),nil)) >= n ; Marked_app'(app'(app'(app'(filter2,true),f),x),xs) > Marked_app'(app'(add,x), app'(app'(filter,f),xs)) ; Marked_app'(app'(app'(app'(filter2,true),f),x),xs) > Marked_app'(app'( filter, f), xs) ; Marked_app'(app'(app'(app'(filter2,false),f),x),xs) > Marked_app'(app'( filter, f), xs) ; Marked_app'(app'(app'(if_rm,true),n),app'(app'(add,m),x)) > Marked_app'( app'(rm, n),x) ; Marked_app'(app'(app'(if_rm,false),n),app'(app'(add,m),x)) > Marked_app'( app'( add, m), app'( app'(rm,n), x)) ; Marked_app'(app'(app'(if_rm,false),n),app'(app'(add,m),x)) > Marked_app'( app'( rm,n), x) ; Marked_app'(app'(app'(if_minsort,true),app'(app'(add,n),x)),y) > Marked_app'( app'( app, app'( app'( rm, n), x)), y) ; Marked_app'(app'(app'(if_minsort,true),app'(app'(add,n),x)),y) > Marked_app'( app'( add, n), app'( app'( minsort, app'( app'( app, app'( app'( rm, n), x)), y)), nil)) ; Marked_app'(app'(app'(if_minsort,true),app'(app'(add,n),x)),y) > Marked_app'( app'( rm, n), x) ; Marked_app'(app'(app'(if_minsort,true),app'(app'(add,n),x)),y) > Marked_app'( app'( minsort, app'( app'( app, app'( app'( rm, n), x)), y)), nil) ; Marked_app'(app'(app'(if_minsort,false),app'(app'(add,n),x)),y) > Marked_app'( app'( add, n), y) ; Marked_app'(app'(app'(if_minsort,false),app'(app'(add,n),x)),y) > Marked_app'( app'( minsort, x), app'( app'( add, n), y)) ; Marked_app'(app'(eq,app'(s,x)),app'(s,y)) > Marked_app'(app'(eq,x),y) ; Marked_app'(app'(le,app'(s,x)),app'(s,y)) > Marked_app'(app'(le,x),y) ; Marked_app'(app'(app,app'(app'(add,n),x)),y) > Marked_app'(app'(app,x),y) ; Marked_app'(app'(app,app'(app'(add,n),x)),y) > Marked_app'(app'(add,n), app'(app'(app,x),y)) ; Marked_app'(app'(if_min,true),app'(app'(add,n),app'(app'(add,m),x))) > Marked_app'(app'(add,n),x) ; Marked_app'(app'(if_min,true),app'(app'(add,n),app'(app'(add,m),x))) > Marked_app'(min,app'(app'(add,n),x)) ; Marked_app'(app'(if_min,false),app'(app'(add,n),app'(app'(add,m),x))) > Marked_app'(min,app'(app'(add,m),x)) ; Marked_app'(app'(rm,n),app'(app'(add,m),x)) > Marked_app'(app'(app'( if_rm, app'( app'( eq, n), m)), n), app'(app'(add,m),x)) ; Marked_app'(app'(rm,n),app'(app'(add,m),x)) > Marked_app'(app'(eq,n),m) ; Marked_app'(app'(rm,n),app'(app'(add,m),x)) > Marked_app'(app'(if_rm, app'(app'(eq,n),m)), n) ; Marked_app'(app'(minsort,app'(app'(add,n),x)),y) > Marked_app'(app'( app'( if_minsort, app'( app'( eq, n), app'( min, app'( app'( add, n), x)))), app'( app'( add, n), x)), y) ; Marked_app'(app'(minsort,app'(app'(add,n),x)),y) > Marked_app'(app'(eq,n), app'(min, app'(app'(add,n),x))) ; Marked_app'(app'(minsort,app'(app'(add,n),x)),y) > Marked_app'(app'( if_minsort, app'( app'( eq, n), app'( min, app'( app'( add, n), x)))), app'(app'(add,n),x)) ; Marked_app'(app'(minsort,app'(app'(add,n),x)),y) >= Marked_app'(min, app'(app'(add,n),x)) ; Marked_app'(app'(map,f),app'(app'(add,x),xs)) > Marked_app'(app'(add, app'(f,x)), app'(app'(map,f),xs)) ; Marked_app'(app'(map,f),app'(app'(add,x),xs)) > Marked_app'(app'(map,f),xs) ; Marked_app'(app'(map,f),app'(app'(add,x),xs)) > Marked_app'(f,x) ; Marked_app'(app'(filter,f),app'(app'(add,x),xs)) > Marked_app'(app'( app'( app'( filter2, app'(f,x)), f), x), xs) ; Marked_app'(app'(filter,f),app'(app'(add,x),xs)) > Marked_app'(app'( app'( filter2, app'(f,x)), f), x) ; Marked_app'(app'(filter,f),app'(app'(add,x),xs)) > Marked_app'(app'( filter2, app'(f,x)), f) ; Marked_app'(app'(filter,f),app'(app'(add,x),xs)) > Marked_app'(f,x) ; Marked_app'(min,app'(app'(add,n),app'(app'(add,m),x))) > Marked_app'( app'(le,n), m) ; Marked_app'(min,app'(app'(add,n),app'(app'(add,m),x))) > Marked_app'( app'(if_min, app'(app'(le,n),m)), app'(app'(add,n), app'(app'(add,m), x))) ; } APPLY CRITERIA (SOLVE_ORD) Trying to solve the following constraints: { app'(app'(app'(app'(filter2,true),f),x),xs) >= app'(app'(add,x), app'(app'(filter,f),xs)) ; app'(app'(app'(app'(filter2,false),f),x),xs) >= app'(app'(filter,f),xs) ; app'(app'(app'(if_rm,true),n),app'(app'(add,m),x)) >= app'(app'(rm,n),x) ; app'(app'(app'(if_rm,false),n),app'(app'(add,m),x)) >= app'(app'(add,m), app'(app'(rm,n),x)) ; app'(app'(app'(if_minsort,true),app'(app'(add,n),x)),y) >= app'(app'(add,n), app'(app'( minsort, app'( app'( app, app'( app'( rm, n), x)), y)), nil)) ; app'(app'(app'(if_minsort,false),app'(app'(add,n),x)),y) >= app'(app'( minsort, x), app'(app'(add,n), y)) ; app'(app'(eq,app'(s,x)),app'(s,y)) >= app'(app'(eq,x),y) ; app'(app'(eq,app'(s,x)),0) >= false ; app'(app'(eq,0),app'(s,x)) >= false ; app'(app'(eq,0),0) >= true ; app'(app'(le,app'(s,x)),app'(s,y)) >= app'(app'(le,x),y) ; app'(app'(le,app'(s,x)),0) >= false ; app'(app'(le,0),y) >= true ; app'(app'(app,app'(app'(add,n),x)),y) >= app'(app'(add,n), app'(app'(app,x),y)) ; app'(app'(app,nil),y) >= y ; app'(app'(if_min,true),app'(app'(add,n),app'(app'(add,m),x))) >= app'( min, app'( app'( add, n), x)) ; app'(app'(if_min,false),app'(app'(add,n),app'(app'(add,m),x))) >= app'( min, app'( app'( add, m), x)) ; app'(app'(rm,n),app'(app'(add,m),x)) >= app'(app'(app'(if_rm, app'(app'(eq,n),m)), n),app'(app'(add,m),x)) ; app'(app'(rm,n),nil) >= nil ; app'(app'(minsort,app'(app'(add,n),x)),y) >= app'(app'(app'(if_minsort, app'(app'(eq,n), app'(min, app'(app'(add,n),x))) ), app'(app'(add,n),x)), y) ; app'(app'(minsort,nil),nil) >= nil ; app'(app'(map,f),app'(app'(add,x),xs)) >= app'(app'(add,app'(f,x)), app'(app'(map,f),xs)) ; app'(app'(map,f),nil) >= nil ; app'(app'(filter,f),app'(app'(add,x),xs)) >= app'(app'(app'(app'(filter2, app'(f,x)), f),x),xs) ; app'(app'(filter,f),nil) >= nil ; app'(min,app'(app'(add,n),app'(app'(add,m),x))) >= app'(app'(if_min, app'(app'(le,n),m)), app'(app'(add,n), app'(app'(add,m),x))) ; app'(min,app'(app'(add,n),nil)) >= n ; Marked_app'(app'(app'(app'(filter2,true),f),x),xs) > Marked_app'(app'(add,x), app'(app'(filter,f),xs)) ; Marked_app'(app'(app'(app'(filter2,true),f),x),xs) > Marked_app'(app'( filter, f), xs) ; Marked_app'(app'(app'(app'(filter2,false),f),x),xs) > Marked_app'(app'( filter, f), xs) ; Marked_app'(app'(app'(if_rm,true),n),app'(app'(add,m),x)) > Marked_app'( app'(rm, n),x) ; Marked_app'(app'(app'(if_rm,false),n),app'(app'(add,m),x)) > Marked_app'( app'( add, m), app'( app'(rm,n), x)) ; Marked_app'(app'(app'(if_rm,false),n),app'(app'(add,m),x)) > Marked_app'( app'( rm,n), x) ; Marked_app'(app'(app'(if_minsort,true),app'(app'(add,n),x)),y) > Marked_app'( app'( app, app'( app'( rm, n), x)), y) ; Marked_app'(app'(app'(if_minsort,true),app'(app'(add,n),x)),y) > Marked_app'( app'( add, n), app'( app'( minsort, app'( app'( app, app'( app'( rm, n), x)), y)), nil)) ; Marked_app'(app'(app'(if_minsort,true),app'(app'(add,n),x)),y) > Marked_app'( app'( rm, n), x) ; Marked_app'(app'(app'(if_minsort,true),app'(app'(add,n),x)),y) > Marked_app'( app'( minsort, app'( app'( app, app'( app'( rm, n), x)), y)), nil) ; Marked_app'(app'(app'(if_minsort,false),app'(app'(add,n),x)),y) > Marked_app'( app'( add, n), y) ; Marked_app'(app'(app'(if_minsort,false),app'(app'(add,n),x)),y) > Marked_app'( app'( minsort, x), app'( app'( add, n), y)) ; Marked_app'(app'(eq,app'(s,x)),app'(s,y)) > Marked_app'(app'(eq,x),y) ; Marked_app'(app'(le,app'(s,x)),app'(s,y)) > Marked_app'(app'(le,x),y) ; Marked_app'(app'(app,app'(app'(add,n),x)),y) > Marked_app'(app'(app,x),y) ; Marked_app'(app'(app,app'(app'(add,n),x)),y) > Marked_app'(app'(add,n), app'(app'(app,x),y)) ; Marked_app'(app'(if_min,true),app'(app'(add,n),app'(app'(add,m),x))) > Marked_app'(app'(add,n),x) ; Marked_app'(app'(if_min,true),app'(app'(add,n),app'(app'(add,m),x))) > Marked_app'(min,app'(app'(add,n),x)) ; Marked_app'(app'(if_min,false),app'(app'(add,n),app'(app'(add,m),x))) > Marked_app'(min,app'(app'(add,m),x)) ; Marked_app'(app'(rm,n),app'(app'(add,m),x)) > Marked_app'(app'(app'( if_rm, app'( app'( eq, n), m)), n), app'(app'(add,m),x)) ; Marked_app'(app'(rm,n),app'(app'(add,m),x)) > Marked_app'(app'(eq,n),m) ; Marked_app'(app'(rm,n),app'(app'(add,m),x)) > Marked_app'(app'(if_rm, app'(app'(eq,n),m)), n) ; Marked_app'(app'(minsort,app'(app'(add,n),x)),y) > Marked_app'(app'( app'( if_minsort, app'( app'( eq, n), app'( min, app'( app'( add, n), x)))), app'( app'( add, n), x)), y) ; Marked_app'(app'(minsort,app'(app'(add,n),x)),y) > Marked_app'(app'(eq,n), app'(min, app'(app'(add,n),x))) ; Marked_app'(app'(minsort,app'(app'(add,n),x)),y) > Marked_app'(app'( if_minsort, app'( app'( eq, n), app'( min, app'( app'(