-
Andrei Paskevich authored
In presence of conjectures, TPTP requires us to prove their conjunction, but no conjectures means |- false. This is awkward, and most provers treat conjectures disjunctively, as in a sequent. We follow TPTP here.
27466653
In presence of conjectures, TPTP requires us to prove their conjunction, but no conjectures means |- false. This is awkward, and most provers treat conjectures disjunctively, as in a sequent. We follow TPTP here.