:- 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).