cnf(additive_inverse_equals_additive_inverse_3,negated_conjecture, ( equalish(additive_inverse(a),additive_inverse(b)) )). cnf(a_not_equal_to_b_4,negated_conjecture, ( ~ equalish(a,b) )).