|
If a is not 0, then the multiplicative inverse of a is not 0
cnf(a_not_equal_to_additive_identity_2,negated_conjecture,
( ~ equalish(a,additive_identity) )).
cnf(multiplicative_inverse_equals_additive_identity_3,negated_conjecture,
( equalish(multiplicative_inverse(a),additive_identity) )).
$false(by Vampire 11.0)
Copyright 2010 Inference Web group.
All Rights Reserved.
