:- true pred nreverse(_1,_2)
         : ( list(_1), var(_2) )
        => ( list(_1), list(_2), length(_1,_A) )
         + cost(ub,steps,0.5*(_A+1)**2+1.5*_A+6.5).

:- true pred 'nreverse$pre'(_1)
         : list(_1)
        => ( list(_1), length(_1,_A) )
         + cost(ub,steps,_A+4).

:- true pred 'nreverse$cls'(A,B)
         : ( list(A), var(B) )
        => ( list(A), list(B), length(A,_A) )
         + cost(ub,steps,0.5*(_A+1)**2+0.5*_A+1.5).

:- true pred nreverse_i(_A,Ys)
         : ( list(_A), var(Ys) )
        => ( list(_A), list(Ys), length(_A,_B) )
         + cost(ub,steps,0.5*(_B+1)**2+0.5*_B+0.5).

:- true pred appendlast(_A,X,_B)
         : ( list(_A), term(X), var(_B) )
        => ( list(_A), term(X), non_empty_list(_B), length(_A,_C) )
         + cost(ub,steps,_C+1).

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