GM08a
Premises:
(forall (?X ?Y ?Z) (=> (and (R ?X ?Y) (R ?X ?Z)) (= ?Y ?Z))) (forall (?X ?Y ?Z) (=> (and (R ?Y ?X) (R ?Z ?X)) (= ?Y ?Z))) (forall ?X (not (R ?X ?X))) (R a b) (R b c) (R c d) (R d a) (P a) (P b) (not (P c)) (not (P d)) (not (= a b)) (not (= a c)) (not (= a d)) (not (= b c)) (not (= b d)) (not (= c d))
Conclusion:
(exists ?X (and (P ?X) (forall ?Y (=> (R ?X ?Y) (P ?Y)))))