|
Unknown
cnf(a_times_b,negated_conjecture,
( product(a,b,additive_identity) )).
cnf(a_not_additive_identity,negated_conjecture,
( a != additive_identity )).
cnf(prove_b_is_additive_identity,negated_conjecture,
( b != additive_identity )).
$false(by Vampire 11.0)
$false(by SPASS 3.5)
$false(by SOS 2.0)
$false(by SNARK 20080805r018b)
$false(by Otter 3.3)
$false(by EP 1.1)
Copyright 2010 Inference Web group.
All Rights Reserved.
