cnf(a_times_b,negated_conjecture, ( product(a,b,additive_identity) )). cnf(a_not_additive_identity,negated_conjecture, ( a != additive_identity )). cnf(prove_b_is_additive_identity,negated_conjecture, ( b != additive_identity )).