:- true pred ord_insert(_A,_B,_C)
         : ( num(_A), list(_B,num), var(_C) )
        => ( num(_A), list(_B,num), rt4(_C), length(_B,_D) )
         + cost(ub,steps,3.0*(_D+1)**2+10.0*_D+11.0).

:- true pred sorted(_A)
         : list(_A,num)
        => ( list(_A,num), length(_A,_B) )
         + cost(ub,steps,2*_B+1).

:- true pred sorted([_A|_B])
         : ( num(_A), list(_B,num) )
        => ( num(_A), list(_B,num), length(_B,_C) )
         + cost(ub,steps,2*_C+3).

:- true pred sorted(_A)
         : rt4(_A)
        => ( list(_A,num), length(_A,_B) )
         + cost(ub,steps,2*_B+1).

:- true pred sorted([_A])
         : num(_A)
        => num(_A)
         + cost(ub,steps,3).

:- true pred sorted([])
         + cost(ub,steps,1).

:- true pred head(_A,X)
         : ( list(_A,num), var(X) )
        => ( rt4(_A), num(X) )
         + cost(ub,steps,1).

:- true pred head(_A,X)
         : ( rt0(_A), var(X) )
        => ( rt4(_A), num(X) )
         + cost(ub,steps,1).

:- regtype rt4/1.

rt4([A|B]) :-
        num(A),
        list(B,num).

:- regtype rt0/1.

rt0([]).