:- true pred ord_insert(_1,_2,_3) : ( num(_1), list(_2,num), var(_3) ) => ( num(_1), list(_2,num), rt3(_3), length(_2,_A) ) + cost(ub,steps,3*_A+6). :- true pred 'ord_insert$pre'(_1) : list(_1,num) => ( list(_1,num), length(_1,_A) ) + cost(ub,steps,2*_A+2). :- true pred 'ord_insert$cls'(A,B,C) : ( num(A), list(B,num), var(C) ) => ( num(A), list(B,num), rt3(C), length(B,_A) ) + cost(ub,steps,_A+3). :- true pred ord_insert_i(X,_A,_B) : ( num(X), list(_A,num), var(_B) ) => ( num(X), list(_A,num), rt3(_B), length(_A,_C) ) + cost(ub,steps,_C+2). :- regtype rt3/1. rt3([A|B]) :- num(A), list(B,num). :- true pred sorted(_A) : list(_A,num) => ( list(_A,num), length(_A,_B) ) + cost(ub,steps,2*_B+1). :- true pred sorted(_A) : rt3(_A) => ( list(_A,num), length(_A,_B) ) + cost(ub,steps,2*_B+1). :- true pred head(_A,X) : ( list(_A,num), var(X) ) => ( rt3(_A), num(X) ) + cost(ub,steps,1).