Modify bks-1 to avoid existentials

[alanruttenberg]

Former

(forall (o)
 (if (exists (t) (instance-of o role t))
  (forall (u)
   (if (exists (t) (instance-of o u t))
    (forall (t) (iff (instance-of o role t) (instance-of o u t)))))))

Replacement

(forall (o u t1 t2)
 (if (and (instance-of o role t1) (instance-of o u t2))
  (and (instance-of o role t2) (instance-of o u t1))))

They are logically equivalent. This avoids skolemization in Werner's prover. Credit Werner Ceusters.

[wceusters]

Actually, it is not an issue of skolemization here, but the introduction of a redundant literal in the CNF generated out of bks-1, but also that a reasoner can deal with. The main advantage of the alternative is the readability. It requires, at least for me :-), less brain power to understand the alternative than the original, so thanks.