|
Side change of a term in an equation by multiplication, part 2
cnf(a_not_equal_to_additive_identity_3,negated_conjecture,
( ~ equalish(a,additive_identity) )).
cnf(multiplicative_identity_equals_multiply_4,negated_conjecture,
( equalish(multiplicative_identity,multiply(b,multiplicative_inverse(a))) )).
cnf(a_not_equal_to_b_5,negated_conjecture,
( ~ equalish(a,b) )).
$false(by EP 1.1)
$false(by Vampire 11.0)
Copyright 2009 Inference Web group.
All Rights Reserved.
