cnf(a_not_equal_to_additive_identity_3,negated_conjecture, ( ~ equalish(a,additive_identity) )). cnf(multiply_equals_a_4,negated_conjecture, ( equalish(multiply(m,a),a) )). cnf(m_not_equal_to_multiplicative_identity_5,negated_conjecture, ( ~ equalish(m,multiplicative_identity) )).