G ((n0 → X n1) ∧
(n1 → X n1)) ∧
n0 ∧
¬ n1 ∧
G ¬ (n0 ∧
n1) ∧
¬ R#t1_x#T_x#T ∧
¬ R#t1_x#T_s#T ∧
¬ R#t1_s#T_x#T ∧
¬ R#t1_s#T_s#T ∧
G (((n0 ∧
X n1) → ((X R#t1_x#T_x#T ↔ (R#t1_x#T_x#T ∨
(O#t1_x#T ∧
choice0_x#T_x#T))) ∧
(X R#t1_x#T_s#T ↔ (R#t1_x#T_s#T ∨
(O#t1_s#T ∧
choice0_x#T_s#T))) ∧
(X R#t1_s#T_x#T ↔ (R#t1_s#T_x#T ∨
(O#t1_x#T ∧
choice0_s#T_x#T))) ∧
(X R#t1_s#T_s#T ↔ (R#t1_s#T_s#T ∨
(O#t1_s#T ∧
choice0_s#T_s#T))))) ∧
((n1 ∧
X n1) → ((X R#t1_x#T_x#T ↔ R#t1_x#T_x#T) ∧
(X R#t1_x#T_s#T ↔ R#t1_x#T_s#T) ∧
(X R#t1_s#T_x#T ↔ R#t1_s#T_x#T) ∧
(X R#t1_s#T_s#T ↔ R#t1_s#T_s#T)))) ∧
¬ R#t2_x#T_x#T ∧
¬ R#t2_x#T_s#T ∧
¬ R#t2_s#T_x#T ∧
¬ R#t2_s#T_s#T ∧
G (((n0 ∧
X n1) → ((X R#t2_x#T_x#T ↔ (R#t2_x#T_x#T ∨
(O#t2_x#T ∧
choice0_x#T_x#T))) ∧
(X R#t2_x#T_s#T ↔ (R#t2_x#T_s#T ∨
(O#t2_s#T ∧
choice0_x#T_s#T))) ∧
(X R#t2_s#T_x#T ↔ (R#t2_s#T_x#T ∨
(O#t2_x#T ∧
choice0_s#T_x#T))) ∧
(X R#t2_s#T_s#T ↔ (R#t2_s#T_s#T ∨
(O#t2_s#T ∧
choice0_s#T_s#T))))) ∧
((n1 ∧
X n1) → ((X R#t2_x#T_x#T ↔ R#t2_x#T_x#T) ∧
(X R#t2_x#T_s#T ↔ R#t2_x#T_s#T) ∧
(X R#t2_s#T_x#T ↔ R#t2_s#T_x#T) ∧
(X R#t2_s#T_s#T ↔ R#t2_s#T_s#T)))) ∧
True ∧
F ¬ (R#t1_x#T_s#T ↔ R#t2_x#T_s#T)