cnf(a_equals_x_5,negated_conjecture, ( equalish(a,x) )). cnf(add_equals_c_6,negated_conjecture, ( equalish(add(a,b),c) )). cnf(add_not_equal_to_c_7,negated_conjecture, ( ~ equalish(add(x,b),c) )).