cnf(add_equals_add_4,negated_conjecture, ( equalish(add(a,c),add(b,c)) )). cnf(a_not_equal_to_b_5,negated_conjecture, ( ~ equalish(a,b) )).