:- true pred bst_member(_1,_2)
         : ( num(_1), bin_tree(_2) )
        => ( num(_1), bin_tree(_2), depth(_2,_A) )
         + cost(ub,steps,3*2**(_A+1)+4*_A+14).

:- true pred 'bst_member$pre'(_1)
         : bin_tree(_1)
        => ( bin_tree(_1), depth(_1,_A) )
         + cost(ub,steps,3*2**(_A+1)+3*_A+9).

:- true pred 'bst_member$cls'(E,T)
         : ( num(E), bin_tree(T) )
        => ( num(E), bin_tree(T), depth(T,_A) )
         + cost(ub,steps,_A+4).

:- true pred bst_member_i(E,_A)
         : ( num(E), bin_tree(_A) )
        => ( num(E), bin_tree(_A), depth(_A,_B) )
         + cost(ub,steps,_B+3).

:- true pred bst(_A)
         : bin_tree(_A)
        => ( bin_tree(_A), depth(_A,_B) )
         + cost(ub,steps,3*2**(_B+1)+3*_B+6).

:- true pred min_(_A,_1)
         : ( bin_tree(_A), var(_1) )
        => ( bin_tree(_A), num(_1), depth(_A,_B) )
         + cost(ub,steps,_B+3).

:- true pred max_(_A,_1)
         : ( bin_tree(_A), var(_1) )
        => ( bin_tree(_A), num(_1), depth(_A,_B) )
         + cost(ub,steps,_B+3).

:- true pred bst_(_A,_1,_2)
         : ( bin_tree(_A), num(_1), num(_2) )
        => ( bin_tree(_A), num(_1), num(_2), depth(_A,_B) )
         + cost(ub,steps,2**(_B+2)-1.0).