GM08bGnd
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:
(and (or (not (P a)) (exists (?X ?Y) (and (R a ?X) (R ?X ?Y) (not (P ?Y))))) (or (not (P b)) (exists (?X ?Y) (and (R b ?X) (R ?X ?Y) (not (P ?Y))))) (or (not (P c)) (exists (?X ?Y) (and (R c ?X) (R ?X ?Y) (not (P ?Y))))) (or (not (P d)) (exists (?X ?Y) (and (R d ?X) (R ?X ?Y) (not (P ?Y))))))