GM06dGnd
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) (not (= a b)) (not (= a c)) (not (= a d)) (not (= b c)) (not (= b d)) (not (= c d))
Conclusion:
(and (or (R a b) (R b a) (exists ?Z (and (R a ?Z) (R ?Z b))) (exists ?Z (and (R b ?Z) (R ?Z a)))) (or (R a c) (R c a) (exists ?Z (and (R a ?Z) (R ?Z c))) (exists ?Z (and (R c ?Z) (R ?Z a)))) (or (R a d) (R d a) (exists ?Z (and (R a ?Z) (R ?Z d))) (exists ?Z (and (R d ?Z) (R ?Z a)))) (or (R b c) (R c b) (exists ?Z (and (R b ?Z) (R ?Z c))) (exists ?Z (and (R v ?Z) (R ?Z b)))) (or (R b d) (R d b) (exists ?Z (and (R b ?Z) (R ?Z d))) (exists ?Z (and (R d ?Z) (R ?Z b)))) (or (R c d) (R d c) (exists ?Z (and (R c ?Z) (R ?Z d))) (exists ?Z (and (R d ?Z) (R ?Z c)))))