 |
 |
 |
 |
 |
Proof Style | Sentence Format | Lens Magnitude | Lens Width |  |
|
Elimination of an additive term/inverse term - pair
cnf(add_not_equal_to_a_3,negated_conjecture,
( ~ equalish(add(a,add(b,additive_inverse(b))),a) )).
$false(by SPASS 3.5)
$false(by EP 1.1)
Copyright 2010 Inference Web group.
All Rights Reserved.
