Los001
Premises:
(forall (?X ?Y ?Z) (=> (and (P ?X ?Y) (P ?Y ?Z)) (P ?X ?Z))) (forall (?X ?Y ?Z) (=> (and (Q ?X ?Y) (Q ?Y ?Z)) (Q ?X ?Z))) (forall (?X ?Y) (=> (Q ?X ?Y) (Q ?Y ?X))) (forall (?X ?Y) (or (P ?X ?Y) (Q ?X ?Y)))
Conclusion:
(or (forall (?X ?Y) (P ?X ?Y)) (forall (?X ?Y) (Q ?X ?Y)))
Proof Trace