|
The multiplicative identity is unique
cnf(a_not_equal_to_additive_identity_3,negated_conjecture,
( ~ equalish(a,additive_identity) )).
cnf(multiply_equals_a_4,negated_conjecture,
( equalish(multiply(m,a),a) )).
cnf(m_not_equal_to_multiplicative_identity_5,negated_conjecture,
( ~ equalish(m,multiplicative_identity) )).
$false(by EP 1.1)
$false(by Vampire 11.0)
Copyright 2009 Inference Web group.
All Rights Reserved.
