cnf(add_equals_b_5,negated_conjecture, ( equalish(add(a,u),b) )). cnf(add_equals_b_6,negated_conjecture, ( equalish(add(a,v),b) )). cnf(u_not_equal_to_v_7,negated_conjecture, ( ~ equalish(u,v) )).