cnf(add_not_equal_to_a_3,negated_conjecture, ( ~ equalish(add(a,add(b,additive_inverse(b))),a) )).