cnf(a_not_equal_to_additive_identity_3,negated_conjecture, ( ~ equalish(a,additive_identity) )). cnf(multiplicative_identity_equals_multiply_4,negated_conjecture, ( equalish(multiplicative_identity,multiply(b,multiplicative_inverse(a))) )). cnf(a_not_equal_to_b_5,negated_conjecture, ( ~ equalish(a,b) )).