 |
 |
 |
 |
 |
Proof Style | Sentence Format | Lens Magnitude | Lens Width |  |
|
A theorem in the lattice structure of Wajsberg algebras
cnf(antecedent,negated_conjecture,
( ordered(x,implies(y,z))
| ordered(y,implies(x,z)) )).
cnf(prove_wajsberg_theorem,negated_conjecture,
( ~ ordered(x,implies(y,z))
| ~ ordered(y,implies(x,z)) )).
$false(by Vampire 11.0)
$false(by Metis 2.2)
$false(by EP 1.1)
Copyright 2010 Inference Web group.
All Rights Reserved.
