|
The resulting equation of the summation of two equations
cnf(a_equals_b_6,negated_conjecture,
( equalish(a,b) )).
cnf(c_equals_d_7,negated_conjecture,
( equalish(c,d) )).
cnf(add_equals_u_8,negated_conjecture,
( equalish(add(a,c),u) )).
cnf(add_not_equal_to_u_9,negated_conjecture,
( ~ equalish(add(d,b),u) )).
$false(by EP 1.1)
$false(by SPASS 3.5)
Copyright 2009 Inference Web group.
All Rights Reserved.
