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)