%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : SYO903_10 : TPTP v9.2.0. Released v8.2.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n013.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 300s % DateTime : Fri Oct 3 08:09:45 PM UTC 2025 % Result : Theorem 7.50s 7.68s % Output : Proof 7.92s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : SYO903_10 : TPTP v9.2.0. Released v8.2.0. % 0.03/0.14 % Command : duper %s % 0.13/0.35 % Computer : n013.cluster.edu % 0.13/0.35 % Model : x86_64 x86_64 % 0.13/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.35 % Memory : 8042.1875MB % 0.13/0.35 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.35 % CPULimit : 300 % 0.13/0.35 % WCLimit : 300 % 0.13/0.35 % DateTime : Fri Oct 3 12:56:08 EDT 2025 % 0.13/0.35 % CPUTime : % 7.50/7.68 SZS status Theorem for theBenchmark.p % 7.50/7.68 SZS output start Proof for theBenchmark.p % 7.50/7.68 Clause #0 (by assumption #[]): Eq (∀ (W : «$ki_world»), «$ki_accessible» W W) True % 7.50/7.68 Clause #5 (by assumption #[]): Eq % 7.50/7.68 (Or % 7.50/7.68 (Or (Or (v1 «$ki_local_world») (v2 «$ki_local_world»)) % 7.50/7.68 (∀ (W : «$ki_world»), «$ki_accessible» «$ki_local_world» W → Not (v3 W))) % 7.50/7.68 (∀ (W : «$ki_world»), «$ki_accessible» «$ki_local_world» W → ∀ (W0 : «$ki_world»), «$ki_accessible» W W0 → v1 W0)) % 7.50/7.68 True % 7.50/7.68 Clause #6 (by assumption #[]): Eq % 7.50/7.68 (Or % 7.50/7.68 (Or (Or (v1 «$ki_local_world») (v3 «$ki_local_world»)) % 7.50/7.68 (∀ (W : «$ki_world»), «$ki_accessible» «$ki_local_world» W → ∀ (W0 : «$ki_world»), «$ki_accessible» W W0 → v3 W0)) % 7.50/7.68 (∀ (W : «$ki_world»), «$ki_accessible» «$ki_local_world» W → ∀ (W0 : «$ki_world»), «$ki_accessible» W W0 → v4 W0)) % 7.50/7.68 True % 7.50/7.68 Clause #8 (by assumption #[]): Eq % 7.50/7.68 (Or (Or (Or (v1 «$ki_local_world») (Not (v2 «$ki_local_world»))) (Not (v4 «$ki_local_world»))) % 7.50/7.68 (∀ (W : «$ki_world»), % 7.50/7.68 «$ki_accessible» «$ki_local_world» W → ∀ (W0 : «$ki_world»), «$ki_accessible» W W0 → Not (v2 W0))) % 7.50/7.68 True % 7.50/7.68 Clause #12 (by assumption #[]): Eq % 7.50/7.68 (Or % 7.50/7.68 (Or (Or (v1 «$ki_local_world») (Not (v4 «$ki_local_world»))) % 7.50/7.68 (∀ (W : «$ki_world»), % 7.50/7.68 «$ki_accessible» «$ki_local_world» W → ∀ (W0 : «$ki_world»), «$ki_accessible» W W0 → Not (v3 W0))) % 7.50/7.68 (∀ (W : «$ki_world»), % 7.50/7.68 «$ki_accessible» «$ki_local_world» W → ∀ (W0 : «$ki_world»), «$ki_accessible» W W0 → Not (v4 W0))) % 7.50/7.68 True % 7.50/7.68 Clause #19 (by assumption #[]): Eq % 7.50/7.68 (Or % 7.50/7.68 (Or (Or (v2 «$ki_local_world») (Not (v3 «$ki_local_world»))) % 7.50/7.68 (∀ (W : «$ki_world»), «$ki_accessible» «$ki_local_world» W → Not (v1 W))) % 7.50/7.68 (∀ (W : «$ki_world»), % 7.50/7.68 «$ki_accessible» «$ki_local_world» W → ∀ (W0 : «$ki_world»), «$ki_accessible» W W0 → Not (v1 W0))) % 7.50/7.68 True % 7.50/7.68 Clause #23 (by assumption #[]): Eq % 7.50/7.68 (Or % 7.50/7.68 (Or (Or (v3 «$ki_local_world») (v4 «$ki_local_world»)) % 7.50/7.68 (∀ (W : «$ki_world»), «$ki_accessible» «$ki_local_world» W → v2 W)) % 7.50/7.68 (∀ (W : «$ki_world»), «$ki_accessible» «$ki_local_world» W → ∀ (W0 : «$ki_world»), «$ki_accessible» W W0 → v1 W0)) % 7.50/7.68 True % 7.50/7.68 Clause #27 (by assumption #[]): Eq % 7.50/7.68 (Or % 7.50/7.68 (Or (Or (v3 «$ki_local_world») (Not (v4 «$ki_local_world»))) % 7.50/7.68 (∀ (W : «$ki_world»), «$ki_accessible» «$ki_local_world» W → ∀ (W0 : «$ki_world»), «$ki_accessible» W W0 → v3 W0)) % 7.50/7.68 (∀ (W : «$ki_world»), % 7.50/7.68 «$ki_accessible» «$ki_local_world» W → ∀ (W0 : «$ki_world»), «$ki_accessible» W W0 → Not (v4 W0))) % 7.50/7.68 True % 7.50/7.68 Clause #30 (by assumption #[]): Eq % 7.50/7.68 (Or % 7.50/7.68 (Or (Or (v4 «$ki_local_world») (Not (v1 «$ki_local_world»))) % 7.50/7.68 (∀ (W : «$ki_world»), «$ki_accessible» «$ki_local_world» W → Not (v1 W))) % 7.50/7.68 (∀ (W : «$ki_world»), «$ki_accessible» «$ki_local_world» W → ∀ (W0 : «$ki_world»), «$ki_accessible» W W0 → v3 W0)) % 7.50/7.68 True % 7.50/7.68 Clause #34 (by assumption #[]): Eq % 7.50/7.68 (Or % 7.50/7.68 (Or (Or (Not (v1 «$ki_local_world»)) (Not (v2 «$ki_local_world»))) % 7.50/7.68 (∀ (W : «$ki_world»), «$ki_accessible» «$ki_local_world» W → v3 W)) % 7.50/7.68 (∀ (W : «$ki_world»), % 7.50/7.68 «$ki_accessible» «$ki_local_world» W → ∀ (W0 : «$ki_world»), «$ki_accessible» W W0 → Not (v1 W0))) % 7.50/7.68 True % 7.50/7.68 Clause #35 (by assumption #[]): Eq % 7.50/7.68 (Or % 7.50/7.68 (Or (Or (Not (v1 «$ki_local_world»)) (Not (v2 «$ki_local_world»))) % 7.50/7.68 (∀ (W : «$ki_world»), «$ki_accessible» «$ki_local_world» W → Not (v4 W))) % 7.50/7.68 (∀ (W : «$ki_world»), % 7.50/7.68 «$ki_accessible» «$ki_local_world» W → ∀ (W0 : «$ki_world»), «$ki_accessible» W W0 → Not (v1 W0))) % 7.50/7.68 True % 7.50/7.68 Clause #36 (by assumption #[]): Eq % 7.50/7.68 (Or % 7.50/7.68 (Or (Or (Not (v1 «$ki_local_world»)) (Not (v3 «$ki_local_world»))) % 7.50/7.68 (∀ (W : «$ki_world»), «$ki_accessible» «$ki_local_world» W → Not (v3 W))) % 7.50/7.68 (∀ (W : «$ki_world»), «$ki_accessible» «$ki_local_world» W → ∀ (W0 : «$ki_world»), «$ki_accessible» W W0 → v4 W0)) % 7.50/7.70 True % 7.50/7.70 Clause #41 (by assumption #[]): Eq % 7.50/7.70 (Or % 7.50/7.70 (Or (Or (Not (v2 «$ki_local_world»)) (Not (v3 «$ki_local_world»))) % 7.50/7.70 (∀ (W : «$ki_world»), «$ki_accessible» «$ki_local_world» W → ∀ (W0 : «$ki_world»), «$ki_accessible» W W0 → v1 W0)) % 7.50/7.70 (∀ (W : «$ki_world»), «$ki_accessible» «$ki_local_world» W → ∀ (W0 : «$ki_world»), «$ki_accessible» W W0 → v4 W0)) % 7.50/7.70 True % 7.50/7.70 Clause #55 (by clausification #[0]): ∀ (a : «$ki_world»), Eq («$ki_accessible» a a) True % 7.50/7.70 Clause #115 (by clausification #[23]): Or % 7.50/7.70 (Eq % 7.50/7.70 (Or (Or (v3 «$ki_local_world») (v4 «$ki_local_world»)) % 7.50/7.70 (∀ (W : «$ki_world»), «$ki_accessible» «$ki_local_world» W → v2 W)) % 7.50/7.70 True) % 7.50/7.70 (Eq (∀ (W : «$ki_world»), «$ki_accessible» «$ki_local_world» W → ∀ (W0 : «$ki_world»), «$ki_accessible» W W0 → v1 W0) % 7.50/7.70 True) % 7.50/7.70 Clause #116 (by clausification #[115]): Or % 7.50/7.70 (Eq (∀ (W : «$ki_world»), «$ki_accessible» «$ki_local_world» W → ∀ (W0 : «$ki_world»), «$ki_accessible» W W0 → v1 W0) % 7.50/7.70 True) % 7.50/7.70 (Or (Eq (Or (v3 «$ki_local_world») (v4 «$ki_local_world»)) True) % 7.50/7.70 (Eq (∀ (W : «$ki_world»), «$ki_accessible» «$ki_local_world» W → v2 W) True)) % 7.50/7.70 Clause #117 (by clausification #[116]): ∀ (a : «$ki_world»), % 7.50/7.70 Or (Eq (Or (v3 «$ki_local_world») (v4 «$ki_local_world»)) True) % 7.50/7.70 (Or (Eq (∀ (W : «$ki_world»), «$ki_accessible» «$ki_local_world» W → v2 W) True) % 7.50/7.70 (Eq («$ki_accessible» «$ki_local_world» a → ∀ (W0 : «$ki_world»), «$ki_accessible» a W0 → v1 W0) True)) % 7.50/7.70 Clause #118 (by clausification #[117]): ∀ (a : «$ki_world»), % 7.50/7.70 Or (Eq (∀ (W : «$ki_world»), «$ki_accessible» «$ki_local_world» W → v2 W) True) % 7.50/7.70 (Or (Eq («$ki_accessible» «$ki_local_world» a → ∀ (W0 : «$ki_world»), «$ki_accessible» a W0 → v1 W0) True) % 7.50/7.70 (Or (Eq (v3 «$ki_local_world») True) (Eq (v4 «$ki_local_world») True))) % 7.50/7.70 Clause #119 (by clausification #[118]): ∀ (a a_1 : «$ki_world»), % 7.50/7.70 Or (Eq («$ki_accessible» «$ki_local_world» a → ∀ (W0 : «$ki_world»), «$ki_accessible» a W0 → v1 W0) True) % 7.50/7.70 (Or (Eq (v3 «$ki_local_world») True) % 7.50/7.70 (Or (Eq (v4 «$ki_local_world») True) (Eq («$ki_accessible» «$ki_local_world» a_1 → v2 a_1) True))) % 7.50/7.70 Clause #120 (by clausification #[119]): ∀ (a a_1 : «$ki_world»), % 7.50/7.70 Or (Eq (v3 «$ki_local_world») True) % 7.50/7.70 (Or (Eq (v4 «$ki_local_world») True) % 7.50/7.70 (Or (Eq («$ki_accessible» «$ki_local_world» a → v2 a) True) % 7.50/7.70 (Or (Eq («$ki_accessible» «$ki_local_world» a_1) False) % 7.50/7.70 (Eq (∀ (W0 : «$ki_world»), «$ki_accessible» a_1 W0 → v1 W0) True)))) % 7.50/7.70 Clause #121 (by clausification #[120]): ∀ (a a_1 : «$ki_world»), % 7.50/7.70 Or (Eq (v3 «$ki_local_world») True) % 7.50/7.70 (Or (Eq (v4 «$ki_local_world») True) % 7.50/7.70 (Or (Eq («$ki_accessible» «$ki_local_world» a) False) % 7.50/7.70 (Or (Eq (∀ (W0 : «$ki_world»), «$ki_accessible» a W0 → v1 W0) True) % 7.50/7.70 (Or (Eq («$ki_accessible» «$ki_local_world» a_1) False) (Eq (v2 a_1) True))))) % 7.50/7.70 Clause #122 (by clausification #[121]): ∀ (a a_1 a_2 : «$ki_world»), % 7.50/7.70 Or (Eq (v3 «$ki_local_world») True) % 7.50/7.70 (Or (Eq (v4 «$ki_local_world») True) % 7.50/7.70 (Or (Eq («$ki_accessible» «$ki_local_world» a) False) % 7.50/7.70 (Or (Eq («$ki_accessible» «$ki_local_world» a_1) False) % 7.50/7.70 (Or (Eq (v2 a_1) True) (Eq («$ki_accessible» a a_2 → v1 a_2) True))))) % 7.50/7.70 Clause #123 (by clausification #[122]): ∀ (a a_1 a_2 : «$ki_world»), % 7.50/7.70 Or (Eq (v3 «$ki_local_world») True) % 7.50/7.70 (Or (Eq (v4 «$ki_local_world») True) % 7.50/7.70 (Or (Eq («$ki_accessible» «$ki_local_world» a) False) % 7.50/7.70 (Or (Eq («$ki_accessible» «$ki_local_world» a_1) False) % 7.50/7.70 (Or (Eq (v2 a_1) True) (Or (Eq («$ki_accessible» a a_2) False) (Eq (v1 a_2) True)))))) % 7.50/7.70 Clause #125 (by superposition #[123, 55]): ∀ (a a_1 : «$ki_world»), % 7.50/7.70 Or (Eq (v3 «$ki_local_world») True) % 7.50/7.70 (Or (Eq (v4 «$ki_local_world») True) % 7.50/7.70 (Or (Eq («$ki_accessible» «$ki_local_world» a) False) % 7.50/7.70 (Or (Eq (v2 a) True) % 7.50/7.70 (Or (Eq («$ki_accessible» «$ki_local_world» a_1) False) (Or (Eq (v1 a_1) True) (Eq False True)))))) % 7.50/7.71 Clause #126 (by clausification #[5]): Or % 7.50/7.71 (Eq % 7.50/7.71 (Or (Or (v1 «$ki_local_world») (v2 «$ki_local_world»)) % 7.50/7.71 (∀ (W : «$ki_world»), «$ki_accessible» «$ki_local_world» W → Not (v3 W))) % 7.50/7.71 True) % 7.50/7.71 (Eq (∀ (W : «$ki_world»), «$ki_accessible» «$ki_local_world» W → ∀ (W0 : «$ki_world»), «$ki_accessible» W W0 → v1 W0) % 7.50/7.71 True) % 7.50/7.71 Clause #127 (by clausification #[126]): Or % 7.50/7.71 (Eq (∀ (W : «$ki_world»), «$ki_accessible» «$ki_local_world» W → ∀ (W0 : «$ki_world»), «$ki_accessible» W W0 → v1 W0) % 7.50/7.71 True) % 7.50/7.71 (Or (Eq (Or (v1 «$ki_local_world») (v2 «$ki_local_world»)) True) % 7.50/7.71 (Eq (∀ (W : «$ki_world»), «$ki_accessible» «$ki_local_world» W → Not (v3 W)) True)) % 7.50/7.71 Clause #128 (by clausification #[127]): ∀ (a : «$ki_world»), % 7.50/7.71 Or (Eq (Or (v1 «$ki_local_world») (v2 «$ki_local_world»)) True) % 7.50/7.71 (Or (Eq (∀ (W : «$ki_world»), «$ki_accessible» «$ki_local_world» W → Not (v3 W)) True) % 7.50/7.71 (Eq («$ki_accessible» «$ki_local_world» a → ∀ (W0 : «$ki_world»), «$ki_accessible» a W0 → v1 W0) True)) % 7.50/7.71 Clause #129 (by clausification #[128]): ∀ (a : «$ki_world»), % 7.50/7.71 Or (Eq (∀ (W : «$ki_world»), «$ki_accessible» «$ki_local_world» W → Not (v3 W)) True) % 7.50/7.71 (Or (Eq («$ki_accessible» «$ki_local_world» a → ∀ (W0 : «$ki_world»), «$ki_accessible» a W0 → v1 W0) True) % 7.50/7.71 (Or (Eq (v1 «$ki_local_world») True) (Eq (v2 «$ki_local_world») True))) % 7.50/7.71 Clause #130 (by clausification #[129]): ∀ (a a_1 : «$ki_world»), % 7.50/7.71 Or (Eq («$ki_accessible» «$ki_local_world» a → ∀ (W0 : «$ki_world»), «$ki_accessible» a W0 → v1 W0) True) % 7.50/7.71 (Or (Eq (v1 «$ki_local_world») True) % 7.50/7.71 (Or (Eq (v2 «$ki_local_world») True) (Eq («$ki_accessible» «$ki_local_world» a_1 → Not (v3 a_1)) True))) % 7.50/7.71 Clause #131 (by clausification #[130]): ∀ (a a_1 : «$ki_world»), % 7.50/7.71 Or (Eq (v1 «$ki_local_world») True) % 7.50/7.71 (Or (Eq (v2 «$ki_local_world») True) % 7.50/7.71 (Or (Eq («$ki_accessible» «$ki_local_world» a → Not (v3 a)) True) % 7.50/7.71 (Or (Eq («$ki_accessible» «$ki_local_world» a_1) False) % 7.50/7.71 (Eq (∀ (W0 : «$ki_world»), «$ki_accessible» a_1 W0 → v1 W0) True)))) % 7.50/7.71 Clause #132 (by clausification #[131]): ∀ (a a_1 : «$ki_world»), % 7.50/7.71 Or (Eq (v1 «$ki_local_world») True) % 7.50/7.71 (Or (Eq (v2 «$ki_local_world») True) % 7.50/7.71 (Or (Eq («$ki_accessible» «$ki_local_world» a) False) % 7.50/7.71 (Or (Eq (∀ (W0 : «$ki_world»), «$ki_accessible» a W0 → v1 W0) True) % 7.50/7.71 (Or (Eq («$ki_accessible» «$ki_local_world» a_1) False) (Eq (Not (v3 a_1)) True))))) % 7.50/7.71 Clause #133 (by clausification #[132]): ∀ (a a_1 a_2 : «$ki_world»), % 7.50/7.71 Or (Eq (v1 «$ki_local_world») True) % 7.50/7.71 (Or (Eq (v2 «$ki_local_world») True) % 7.50/7.71 (Or (Eq («$ki_accessible» «$ki_local_world» a) False) % 7.50/7.71 (Or (Eq («$ki_accessible» «$ki_local_world» a_1) False) % 7.50/7.71 (Or (Eq (Not (v3 a_1)) True) (Eq («$ki_accessible» a a_2 → v1 a_2) True))))) % 7.50/7.71 Clause #134 (by clausification #[133]): ∀ (a a_1 a_2 : «$ki_world»), % 7.50/7.71 Or (Eq (v1 «$ki_local_world») True) % 7.50/7.71 (Or (Eq (v2 «$ki_local_world») True) % 7.50/7.71 (Or (Eq («$ki_accessible» «$ki_local_world» a) False) % 7.50/7.71 (Or (Eq («$ki_accessible» «$ki_local_world» a_1) False) % 7.50/7.71 (Or (Eq («$ki_accessible» a a_2 → v1 a_2) True) (Eq (v3 a_1) False))))) % 7.50/7.71 Clause #135 (by clausification #[134]): ∀ (a a_1 a_2 : «$ki_world»), % 7.50/7.71 Or (Eq (v1 «$ki_local_world») True) % 7.50/7.71 (Or (Eq (v2 «$ki_local_world») True) % 7.50/7.71 (Or (Eq («$ki_accessible» «$ki_local_world» a) False) % 7.50/7.71 (Or (Eq («$ki_accessible» «$ki_local_world» a_1) False) % 7.50/7.71 (Or (Eq (v3 a_1) False) (Or (Eq («$ki_accessible» a a_2) False) (Eq (v1 a_2) True)))))) % 7.50/7.71 Clause #137 (by superposition #[135, 55]): ∀ (a a_1 : «$ki_world»), % 7.50/7.71 Or (Eq (v1 «$ki_local_world») True) % 7.50/7.71 (Or (Eq (v2 «$ki_local_world») True) % 7.50/7.71 (Or (Eq («$ki_accessible» «$ki_local_world» a) False) % 7.50/7.71 (Or (Eq (v3 a) False) % 7.50/7.71 (Or (Eq («$ki_accessible» «$ki_local_world» a_1) False) (Or (Eq (v1 a_1) True) (Eq False True)))))) % 7.56/7.73 Clause #173 (by clausification #[6]): Or % 7.56/7.73 (Eq % 7.56/7.73 (Or (Or (v1 «$ki_local_world») (v3 «$ki_local_world»)) % 7.56/7.73 (∀ (W : «$ki_world»), «$ki_accessible» «$ki_local_world» W → ∀ (W0 : «$ki_world»), «$ki_accessible» W W0 → v3 W0)) % 7.56/7.73 True) % 7.56/7.73 (Eq (∀ (W : «$ki_world»), «$ki_accessible» «$ki_local_world» W → ∀ (W0 : «$ki_world»), «$ki_accessible» W W0 → v4 W0) % 7.56/7.73 True) % 7.56/7.73 Clause #174 (by clausification #[173]): Or % 7.56/7.73 (Eq (∀ (W : «$ki_world»), «$ki_accessible» «$ki_local_world» W → ∀ (W0 : «$ki_world»), «$ki_accessible» W W0 → v4 W0) % 7.56/7.73 True) % 7.56/7.73 (Or (Eq (Or (v1 «$ki_local_world») (v3 «$ki_local_world»)) True) % 7.56/7.73 (Eq % 7.56/7.73 (∀ (W : «$ki_world»), «$ki_accessible» «$ki_local_world» W → ∀ (W0 : «$ki_world»), «$ki_accessible» W W0 → v3 W0) % 7.56/7.73 True)) % 7.56/7.73 Clause #175 (by clausification #[174]): ∀ (a : «$ki_world»), % 7.56/7.73 Or (Eq (Or (v1 «$ki_local_world») (v3 «$ki_local_world»)) True) % 7.56/7.73 (Or % 7.56/7.73 (Eq % 7.56/7.73 (∀ (W : «$ki_world»), % 7.56/7.73 «$ki_accessible» «$ki_local_world» W → ∀ (W0 : «$ki_world»), «$ki_accessible» W W0 → v3 W0) % 7.56/7.73 True) % 7.56/7.73 (Eq («$ki_accessible» «$ki_local_world» a → ∀ (W0 : «$ki_world»), «$ki_accessible» a W0 → v4 W0) True)) % 7.56/7.73 Clause #176 (by clausification #[175]): ∀ (a : «$ki_world»), % 7.56/7.73 Or % 7.56/7.73 (Eq % 7.56/7.73 (∀ (W : «$ki_world»), «$ki_accessible» «$ki_local_world» W → ∀ (W0 : «$ki_world»), «$ki_accessible» W W0 → v3 W0) % 7.56/7.73 True) % 7.56/7.73 (Or (Eq («$ki_accessible» «$ki_local_world» a → ∀ (W0 : «$ki_world»), «$ki_accessible» a W0 → v4 W0) True) % 7.56/7.73 (Or (Eq (v1 «$ki_local_world») True) (Eq (v3 «$ki_local_world») True))) % 7.56/7.73 Clause #177 (by clausification #[176]): ∀ (a a_1 : «$ki_world»), % 7.56/7.73 Or (Eq («$ki_accessible» «$ki_local_world» a → ∀ (W0 : «$ki_world»), «$ki_accessible» a W0 → v4 W0) True) % 7.56/7.73 (Or (Eq (v1 «$ki_local_world») True) % 7.56/7.73 (Or (Eq (v3 «$ki_local_world») True) % 7.56/7.73 (Eq («$ki_accessible» «$ki_local_world» a_1 → ∀ (W0 : «$ki_world»), «$ki_accessible» a_1 W0 → v3 W0) True))) % 7.56/7.73 Clause #178 (by clausification #[177]): ∀ (a a_1 : «$ki_world»), % 7.56/7.73 Or (Eq (v1 «$ki_local_world») True) % 7.56/7.73 (Or (Eq (v3 «$ki_local_world») True) % 7.56/7.73 (Or (Eq («$ki_accessible» «$ki_local_world» a → ∀ (W0 : «$ki_world»), «$ki_accessible» a W0 → v3 W0) True) % 7.56/7.73 (Or (Eq («$ki_accessible» «$ki_local_world» a_1) False) % 7.56/7.73 (Eq (∀ (W0 : «$ki_world»), «$ki_accessible» a_1 W0 → v4 W0) True)))) % 7.56/7.73 Clause #179 (by clausification #[178]): ∀ (a a_1 : «$ki_world»), % 7.56/7.73 Or (Eq (v1 «$ki_local_world») True) % 7.56/7.73 (Or (Eq (v3 «$ki_local_world») True) % 7.56/7.73 (Or (Eq («$ki_accessible» «$ki_local_world» a) False) % 7.56/7.73 (Or (Eq (∀ (W0 : «$ki_world»), «$ki_accessible» a W0 → v4 W0) True) % 7.56/7.73 (Or (Eq («$ki_accessible» «$ki_local_world» a_1) False) % 7.56/7.73 (Eq (∀ (W0 : «$ki_world»), «$ki_accessible» a_1 W0 → v3 W0) True))))) % 7.56/7.73 Clause #180 (by clausification #[179]): ∀ (a a_1 a_2 : «$ki_world»), % 7.56/7.73 Or (Eq (v1 «$ki_local_world») True) % 7.56/7.73 (Or (Eq (v3 «$ki_local_world») True) % 7.56/7.73 (Or (Eq («$ki_accessible» «$ki_local_world» a) False) % 7.56/7.73 (Or (Eq («$ki_accessible» «$ki_local_world» a_1) False) % 7.56/7.73 (Or (Eq (∀ (W0 : «$ki_world»), «$ki_accessible» a_1 W0 → v3 W0) True) % 7.56/7.73 (Eq («$ki_accessible» a a_2 → v4 a_2) True))))) % 7.56/7.73 Clause #181 (by clausification #[180]): ∀ (a a_1 a_2 a_3 : «$ki_world»), % 7.56/7.73 Or (Eq (v1 «$ki_local_world») True) % 7.56/7.73 (Or (Eq (v3 «$ki_local_world») True) % 7.56/7.73 (Or (Eq («$ki_accessible» «$ki_local_world» a) False) % 7.56/7.73 (Or (Eq («$ki_accessible» «$ki_local_world» a_1) False) % 7.56/7.73 (Or (Eq («$ki_accessible» a a_2 → v4 a_2) True) (Eq («$ki_accessible» a_1 a_3 → v3 a_3) True))))) % 7.56/7.73 Clause #182 (by clausification #[181]): ∀ (a a_1 a_2 a_3 : «$ki_world»), % 7.56/7.73 Or (Eq (v1 «$ki_local_world») True) % 7.56/7.73 (Or (Eq (v3 «$ki_local_world») True) % 7.56/7.73 (Or (Eq («$ki_accessible» «$ki_local_world» a) False) % 7.56/7.75 (Or (Eq («$ki_accessible» «$ki_local_world» a_1) False) % 7.56/7.75 (Or (Eq («$ki_accessible» a_1 a_2 → v3 a_2) True) % 7.56/7.75 (Or (Eq («$ki_accessible» a a_3) False) (Eq (v4 a_3) True)))))) % 7.56/7.75 Clause #183 (by clausification #[182]): ∀ (a a_1 a_2 a_3 : «$ki_world»), % 7.56/7.75 Or (Eq (v1 «$ki_local_world») True) % 7.56/7.75 (Or (Eq (v3 «$ki_local_world») True) % 7.56/7.75 (Or (Eq («$ki_accessible» «$ki_local_world» a) False) % 7.56/7.75 (Or (Eq («$ki_accessible» «$ki_local_world» a_1) False) % 7.56/7.75 (Or (Eq («$ki_accessible» a a_2) False) % 7.56/7.75 (Or (Eq (v4 a_2) True) (Or (Eq («$ki_accessible» a_1 a_3) False) (Eq (v3 a_3) True))))))) % 7.56/7.75 Clause #185 (by superposition #[183, 55]): ∀ (a a_1 a_2 : «$ki_world»), % 7.56/7.75 Or (Eq (v1 «$ki_local_world») True) % 7.56/7.75 (Or (Eq (v3 «$ki_local_world») True) % 7.56/7.75 (Or (Eq («$ki_accessible» «$ki_local_world» a) False) % 7.56/7.75 (Or (Eq («$ki_accessible» «$ki_local_world» a_1) False) % 7.56/7.75 (Or (Eq (v4 a_1) True) (Or (Eq («$ki_accessible» a a_2) False) (Or (Eq (v3 a_2) True) (Eq False True))))))) % 7.56/7.75 Clause #186 (by clausification #[8]): Or (Eq (Or (Or (v1 «$ki_local_world») (Not (v2 «$ki_local_world»))) (Not (v4 «$ki_local_world»))) True) % 7.56/7.75 (Eq % 7.56/7.75 (∀ (W : «$ki_world»), % 7.56/7.75 «$ki_accessible» «$ki_local_world» W → ∀ (W0 : «$ki_world»), «$ki_accessible» W W0 → Not (v2 W0)) % 7.56/7.75 True) % 7.56/7.75 Clause #187 (by clausification #[186]): Or % 7.56/7.75 (Eq % 7.56/7.75 (∀ (W : «$ki_world»), % 7.56/7.75 «$ki_accessible» «$ki_local_world» W → ∀ (W0 : «$ki_world»), «$ki_accessible» W W0 → Not (v2 W0)) % 7.56/7.75 True) % 7.56/7.75 (Or (Eq (Or (v1 «$ki_local_world») (Not (v2 «$ki_local_world»))) True) (Eq (Not (v4 «$ki_local_world»)) True)) % 7.56/7.75 Clause #188 (by clausification #[187]): ∀ (a : «$ki_world»), % 7.56/7.75 Or (Eq (Or (v1 «$ki_local_world») (Not (v2 «$ki_local_world»))) True) % 7.56/7.75 (Or (Eq (Not (v4 «$ki_local_world»)) True) % 7.56/7.75 (Eq («$ki_accessible» «$ki_local_world» a → ∀ (W0 : «$ki_world»), «$ki_accessible» a W0 → Not (v2 W0)) True)) % 7.56/7.75 Clause #189 (by clausification #[188]): ∀ (a : «$ki_world»), % 7.56/7.75 Or (Eq (Not (v4 «$ki_local_world»)) True) % 7.56/7.75 (Or (Eq («$ki_accessible» «$ki_local_world» a → ∀ (W0 : «$ki_world»), «$ki_accessible» a W0 → Not (v2 W0)) True) % 7.56/7.75 (Or (Eq (v1 «$ki_local_world») True) (Eq (Not (v2 «$ki_local_world»)) True))) % 7.56/7.75 Clause #190 (by clausification #[189]): ∀ (a : «$ki_world»), % 7.56/7.75 Or (Eq («$ki_accessible» «$ki_local_world» a → ∀ (W0 : «$ki_world»), «$ki_accessible» a W0 → Not (v2 W0)) True) % 7.56/7.75 (Or (Eq (v1 «$ki_local_world») True) (Or (Eq (Not (v2 «$ki_local_world»)) True) (Eq (v4 «$ki_local_world») False))) % 7.56/7.75 Clause #191 (by clausification #[190]): ∀ (a : «$ki_world»), % 7.56/7.75 Or (Eq (v1 «$ki_local_world») True) % 7.56/7.75 (Or (Eq (Not (v2 «$ki_local_world»)) True) % 7.56/7.75 (Or (Eq (v4 «$ki_local_world») False) % 7.56/7.75 (Or (Eq («$ki_accessible» «$ki_local_world» a) False) % 7.56/7.75 (Eq (∀ (W0 : «$ki_world»), «$ki_accessible» a W0 → Not (v2 W0)) True)))) % 7.56/7.75 Clause #192 (by clausification #[191]): ∀ (a : «$ki_world»), % 7.56/7.75 Or (Eq (v1 «$ki_local_world») True) % 7.56/7.75 (Or (Eq (v4 «$ki_local_world») False) % 7.56/7.75 (Or (Eq («$ki_accessible» «$ki_local_world» a) False) % 7.56/7.75 (Or (Eq (∀ (W0 : «$ki_world»), «$ki_accessible» a W0 → Not (v2 W0)) True) (Eq (v2 «$ki_local_world») False)))) % 7.56/7.75 Clause #193 (by clausification #[192]): ∀ (a a_1 : «$ki_world»), % 7.56/7.75 Or (Eq (v1 «$ki_local_world») True) % 7.56/7.75 (Or (Eq (v4 «$ki_local_world») False) % 7.56/7.75 (Or (Eq («$ki_accessible» «$ki_local_world» a) False) % 7.56/7.75 (Or (Eq (v2 «$ki_local_world») False) (Eq («$ki_accessible» a a_1 → Not (v2 a_1)) True)))) % 7.56/7.75 Clause #194 (by clausification #[193]): ∀ (a a_1 : «$ki_world»), % 7.56/7.75 Or (Eq (v1 «$ki_local_world») True) % 7.56/7.75 (Or (Eq (v4 «$ki_local_world») False) % 7.56/7.75 (Or (Eq («$ki_accessible» «$ki_local_world» a) False) % 7.56/7.75 (Or (Eq (v2 «$ki_local_world») False) (Or (Eq («$ki_accessible» a a_1) False) (Eq (Not (v2 a_1)) True))))) % 7.56/7.75 Clause #195 (by clausification #[194]): ∀ (a a_1 : «$ki_world»), % 7.60/7.77 Or (Eq (v1 «$ki_local_world») True) % 7.60/7.77 (Or (Eq (v4 «$ki_local_world») False) % 7.60/7.77 (Or (Eq («$ki_accessible» «$ki_local_world» a) False) % 7.60/7.77 (Or (Eq (v2 «$ki_local_world») False) (Or (Eq («$ki_accessible» a a_1) False) (Eq (v2 a_1) False))))) % 7.60/7.77 Clause #222 (by clausification #[30]): Or % 7.60/7.77 (Eq % 7.60/7.77 (Or (Or (v4 «$ki_local_world») (Not (v1 «$ki_local_world»))) % 7.60/7.77 (∀ (W : «$ki_world»), «$ki_accessible» «$ki_local_world» W → Not (v1 W))) % 7.60/7.77 True) % 7.60/7.77 (Eq (∀ (W : «$ki_world»), «$ki_accessible» «$ki_local_world» W → ∀ (W0 : «$ki_world»), «$ki_accessible» W W0 → v3 W0) % 7.60/7.77 True) % 7.60/7.77 Clause #223 (by clausification #[222]): Or % 7.60/7.77 (Eq (∀ (W : «$ki_world»), «$ki_accessible» «$ki_local_world» W → ∀ (W0 : «$ki_world»), «$ki_accessible» W W0 → v3 W0) % 7.60/7.77 True) % 7.60/7.77 (Or (Eq (Or (v4 «$ki_local_world») (Not (v1 «$ki_local_world»))) True) % 7.60/7.77 (Eq (∀ (W : «$ki_world»), «$ki_accessible» «$ki_local_world» W → Not (v1 W)) True)) % 7.60/7.77 Clause #224 (by clausification #[223]): ∀ (a : «$ki_world»), % 7.60/7.77 Or (Eq (Or (v4 «$ki_local_world») (Not (v1 «$ki_local_world»))) True) % 7.60/7.77 (Or (Eq (∀ (W : «$ki_world»), «$ki_accessible» «$ki_local_world» W → Not (v1 W)) True) % 7.60/7.77 (Eq («$ki_accessible» «$ki_local_world» a → ∀ (W0 : «$ki_world»), «$ki_accessible» a W0 → v3 W0) True)) % 7.60/7.77 Clause #225 (by clausification #[224]): ∀ (a : «$ki_world»), % 7.60/7.77 Or (Eq (∀ (W : «$ki_world»), «$ki_accessible» «$ki_local_world» W → Not (v1 W)) True) % 7.60/7.77 (Or (Eq («$ki_accessible» «$ki_local_world» a → ∀ (W0 : «$ki_world»), «$ki_accessible» a W0 → v3 W0) True) % 7.60/7.77 (Or (Eq (v4 «$ki_local_world») True) (Eq (Not (v1 «$ki_local_world»)) True))) % 7.60/7.77 Clause #226 (by clausification #[225]): ∀ (a a_1 : «$ki_world»), % 7.60/7.77 Or (Eq («$ki_accessible» «$ki_local_world» a → ∀ (W0 : «$ki_world»), «$ki_accessible» a W0 → v3 W0) True) % 7.60/7.77 (Or (Eq (v4 «$ki_local_world») True) % 7.60/7.77 (Or (Eq (Not (v1 «$ki_local_world»)) True) (Eq («$ki_accessible» «$ki_local_world» a_1 → Not (v1 a_1)) True))) % 7.60/7.77 Clause #227 (by clausification #[226]): ∀ (a a_1 : «$ki_world»), % 7.60/7.77 Or (Eq (v4 «$ki_local_world») True) % 7.60/7.77 (Or (Eq (Not (v1 «$ki_local_world»)) True) % 7.60/7.77 (Or (Eq («$ki_accessible» «$ki_local_world» a → Not (v1 a)) True) % 7.60/7.77 (Or (Eq («$ki_accessible» «$ki_local_world» a_1) False) % 7.60/7.77 (Eq (∀ (W0 : «$ki_world»), «$ki_accessible» a_1 W0 → v3 W0) True)))) % 7.60/7.77 Clause #228 (by clausification #[227]): ∀ (a a_1 : «$ki_world»), % 7.60/7.77 Or (Eq (v4 «$ki_local_world») True) % 7.60/7.77 (Or (Eq («$ki_accessible» «$ki_local_world» a → Not (v1 a)) True) % 7.60/7.77 (Or (Eq («$ki_accessible» «$ki_local_world» a_1) False) % 7.60/7.77 (Or (Eq (∀ (W0 : «$ki_world»), «$ki_accessible» a_1 W0 → v3 W0) True) (Eq (v1 «$ki_local_world») False)))) % 7.60/7.77 Clause #229 (by clausification #[228]): ∀ (a a_1 : «$ki_world»), % 7.60/7.77 Or (Eq (v4 «$ki_local_world») True) % 7.60/7.77 (Or (Eq («$ki_accessible» «$ki_local_world» a) False) % 7.60/7.77 (Or (Eq (∀ (W0 : «$ki_world»), «$ki_accessible» a W0 → v3 W0) True) % 7.60/7.77 (Or (Eq (v1 «$ki_local_world») False) % 7.60/7.77 (Or (Eq («$ki_accessible» «$ki_local_world» a_1) False) (Eq (Not (v1 a_1)) True))))) % 7.60/7.77 Clause #230 (by clausification #[229]): ∀ (a a_1 a_2 : «$ki_world»), % 7.60/7.77 Or (Eq (v4 «$ki_local_world») True) % 7.60/7.77 (Or (Eq («$ki_accessible» «$ki_local_world» a) False) % 7.60/7.77 (Or (Eq (v1 «$ki_local_world») False) % 7.60/7.77 (Or (Eq («$ki_accessible» «$ki_local_world» a_1) False) % 7.60/7.77 (Or (Eq (Not (v1 a_1)) True) (Eq («$ki_accessible» a a_2 → v3 a_2) True))))) % 7.60/7.77 Clause #231 (by clausification #[230]): ∀ (a a_1 a_2 : «$ki_world»), % 7.60/7.77 Or (Eq (v4 «$ki_local_world») True) % 7.60/7.77 (Or (Eq («$ki_accessible» «$ki_local_world» a) False) % 7.60/7.77 (Or (Eq (v1 «$ki_local_world») False) % 7.60/7.77 (Or (Eq («$ki_accessible» «$ki_local_world» a_1) False) % 7.60/7.77 (Or (Eq («$ki_accessible» a a_2 → v3 a_2) True) (Eq (v1 a_1) False))))) % 7.60/7.77 Clause #232 (by clausification #[231]): ∀ (a a_1 a_2 : «$ki_world»), % 7.60/7.79 Or (Eq (v4 «$ki_local_world») True) % 7.60/7.79 (Or (Eq («$ki_accessible» «$ki_local_world» a) False) % 7.60/7.79 (Or (Eq (v1 «$ki_local_world») False) % 7.60/7.79 (Or (Eq («$ki_accessible» «$ki_local_world» a_1) False) % 7.60/7.79 (Or (Eq (v1 a_1) False) (Or (Eq («$ki_accessible» a a_2) False) (Eq (v3 a_2) True)))))) % 7.60/7.79 Clause #234 (by superposition #[232, 55]): ∀ (a a_1 : «$ki_world»), % 7.60/7.79 Or (Eq (v4 «$ki_local_world») True) % 7.60/7.79 (Or (Eq (v1 «$ki_local_world») False) % 7.60/7.79 (Or (Eq («$ki_accessible» «$ki_local_world» a) False) % 7.60/7.79 (Or (Eq (v1 a) False) % 7.60/7.79 (Or (Eq («$ki_accessible» «$ki_local_world» a_1) False) (Or (Eq (v3 a_1) True) (Eq False True)))))) % 7.60/7.79 Clause #316 (by clausification #[19]): Or % 7.60/7.79 (Eq % 7.60/7.79 (Or (Or (v2 «$ki_local_world») (Not (v3 «$ki_local_world»))) % 7.60/7.79 (∀ (W : «$ki_world»), «$ki_accessible» «$ki_local_world» W → Not (v1 W))) % 7.60/7.79 True) % 7.60/7.79 (Eq % 7.60/7.79 (∀ (W : «$ki_world»), % 7.60/7.79 «$ki_accessible» «$ki_local_world» W → ∀ (W0 : «$ki_world»), «$ki_accessible» W W0 → Not (v1 W0)) % 7.60/7.79 True) % 7.60/7.79 Clause #317 (by clausification #[316]): Or % 7.60/7.79 (Eq % 7.60/7.79 (∀ (W : «$ki_world»), % 7.60/7.79 «$ki_accessible» «$ki_local_world» W → ∀ (W0 : «$ki_world»), «$ki_accessible» W W0 → Not (v1 W0)) % 7.60/7.79 True) % 7.60/7.79 (Or (Eq (Or (v2 «$ki_local_world») (Not (v3 «$ki_local_world»))) True) % 7.60/7.79 (Eq (∀ (W : «$ki_world»), «$ki_accessible» «$ki_local_world» W → Not (v1 W)) True)) % 7.60/7.79 Clause #318 (by clausification #[317]): ∀ (a : «$ki_world»), % 7.60/7.79 Or (Eq (Or (v2 «$ki_local_world») (Not (v3 «$ki_local_world»))) True) % 7.60/7.79 (Or (Eq (∀ (W : «$ki_world»), «$ki_accessible» «$ki_local_world» W → Not (v1 W)) True) % 7.60/7.79 (Eq («$ki_accessible» «$ki_local_world» a → ∀ (W0 : «$ki_world»), «$ki_accessible» a W0 → Not (v1 W0)) True)) % 7.60/7.79 Clause #319 (by clausification #[318]): ∀ (a : «$ki_world»), % 7.60/7.79 Or (Eq (∀ (W : «$ki_world»), «$ki_accessible» «$ki_local_world» W → Not (v1 W)) True) % 7.60/7.79 (Or (Eq («$ki_accessible» «$ki_local_world» a → ∀ (W0 : «$ki_world»), «$ki_accessible» a W0 → Not (v1 W0)) True) % 7.60/7.79 (Or (Eq (v2 «$ki_local_world») True) (Eq (Not (v3 «$ki_local_world»)) True))) % 7.60/7.79 Clause #320 (by clausification #[319]): ∀ (a a_1 : «$ki_world»), % 7.60/7.79 Or (Eq («$ki_accessible» «$ki_local_world» a → ∀ (W0 : «$ki_world»), «$ki_accessible» a W0 → Not (v1 W0)) True) % 7.60/7.79 (Or (Eq (v2 «$ki_local_world») True) % 7.60/7.79 (Or (Eq (Not (v3 «$ki_local_world»)) True) (Eq («$ki_accessible» «$ki_local_world» a_1 → Not (v1 a_1)) True))) % 7.60/7.79 Clause #321 (by clausification #[320]): ∀ (a a_1 : «$ki_world»), % 7.60/7.79 Or (Eq (v2 «$ki_local_world») True) % 7.60/7.79 (Or (Eq (Not (v3 «$ki_local_world»)) True) % 7.60/7.79 (Or (Eq («$ki_accessible» «$ki_local_world» a → Not (v1 a)) True) % 7.60/7.79 (Or (Eq («$ki_accessible» «$ki_local_world» a_1) False) % 7.60/7.79 (Eq (∀ (W0 : «$ki_world»), «$ki_accessible» a_1 W0 → Not (v1 W0)) True)))) % 7.60/7.79 Clause #322 (by clausification #[321]): ∀ (a a_1 : «$ki_world»), % 7.60/7.79 Or (Eq (v2 «$ki_local_world») True) % 7.60/7.79 (Or (Eq («$ki_accessible» «$ki_local_world» a → Not (v1 a)) True) % 7.60/7.79 (Or (Eq («$ki_accessible» «$ki_local_world» a_1) False) % 7.60/7.79 (Or (Eq (∀ (W0 : «$ki_world»), «$ki_accessible» a_1 W0 → Not (v1 W0)) True) (Eq (v3 «$ki_local_world») False)))) % 7.60/7.79 Clause #323 (by clausification #[322]): ∀ (a a_1 : «$ki_world»), % 7.60/7.79 Or (Eq (v2 «$ki_local_world») True) % 7.60/7.79 (Or (Eq («$ki_accessible» «$ki_local_world» a) False) % 7.60/7.79 (Or (Eq (∀ (W0 : «$ki_world»), «$ki_accessible» a W0 → Not (v1 W0)) True) % 7.60/7.79 (Or (Eq (v3 «$ki_local_world») False) % 7.60/7.79 (Or (Eq («$ki_accessible» «$ki_local_world» a_1) False) (Eq (Not (v1 a_1)) True))))) % 7.60/7.79 Clause #324 (by clausification #[323]): ∀ (a a_1 a_2 : «$ki_world»), % 7.60/7.79 Or (Eq (v2 «$ki_local_world») True) % 7.60/7.79 (Or (Eq («$ki_accessible» «$ki_local_world» a) False) % 7.60/7.79 (Or (Eq (v3 «$ki_local_world») False) % 7.60/7.79 (Or (Eq («$ki_accessible» «$ki_local_world» a_1) False) % 7.60/7.79 (Or (Eq (Not (v1 a_1)) True) (Eq («$ki_accessible» a a_2 → Not (v1 a_2)) True))))) % 7.60/7.80 Clause #325 (by clausification #[324]): ∀ (a a_1 a_2 : «$ki_world»), % 7.60/7.80 Or (Eq (v2 «$ki_local_world») True) % 7.60/7.80 (Or (Eq («$ki_accessible» «$ki_local_world» a) False) % 7.60/7.80 (Or (Eq (v3 «$ki_local_world») False) % 7.60/7.80 (Or (Eq («$ki_accessible» «$ki_local_world» a_1) False) % 7.60/7.80 (Or (Eq («$ki_accessible» a a_2 → Not (v1 a_2)) True) (Eq (v1 a_1) False))))) % 7.60/7.80 Clause #326 (by clausification #[325]): ∀ (a a_1 a_2 : «$ki_world»), % 7.60/7.80 Or (Eq (v2 «$ki_local_world») True) % 7.60/7.80 (Or (Eq («$ki_accessible» «$ki_local_world» a) False) % 7.60/7.80 (Or (Eq (v3 «$ki_local_world») False) % 7.60/7.80 (Or (Eq («$ki_accessible» «$ki_local_world» a_1) False) % 7.60/7.80 (Or (Eq (v1 a_1) False) (Or (Eq («$ki_accessible» a a_2) False) (Eq (Not (v1 a_2)) True)))))) % 7.60/7.80 Clause #327 (by clausification #[326]): ∀ (a a_1 a_2 : «$ki_world»), % 7.60/7.80 Or (Eq (v2 «$ki_local_world») True) % 7.60/7.80 (Or (Eq («$ki_accessible» «$ki_local_world» a) False) % 7.60/7.80 (Or (Eq (v3 «$ki_local_world») False) % 7.60/7.80 (Or (Eq («$ki_accessible» «$ki_local_world» a_1) False) % 7.60/7.80 (Or (Eq (v1 a_1) False) (Or (Eq («$ki_accessible» a a_2) False) (Eq (v1 a_2) False)))))) % 7.60/7.80 Clause #329 (by superposition #[327, 55]): ∀ (a a_1 : «$ki_world»), % 7.60/7.80 Or (Eq (v2 «$ki_local_world») True) % 7.60/7.80 (Or (Eq (v3 «$ki_local_world») False) % 7.60/7.80 (Or (Eq («$ki_accessible» «$ki_local_world» a) False) % 7.60/7.80 (Or (Eq (v1 a) False) % 7.60/7.80 (Or (Eq («$ki_accessible» «$ki_local_world» a_1) False) (Or (Eq (v1 a_1) False) (Eq False True)))))) % 7.60/7.80 Clause #330 (by clausification #[12]): Or % 7.60/7.80 (Eq % 7.60/7.80 (Or (Or (v1 «$ki_local_world») (Not (v4 «$ki_local_world»))) % 7.60/7.80 (∀ (W : «$ki_world»), % 7.60/7.80 «$ki_accessible» «$ki_local_world» W → ∀ (W0 : «$ki_world»), «$ki_accessible» W W0 → Not (v3 W0))) % 7.60/7.80 True) % 7.60/7.80 (Eq % 7.60/7.80 (∀ (W : «$ki_world»), % 7.60/7.80 «$ki_accessible» «$ki_local_world» W → ∀ (W0 : «$ki_world»), «$ki_accessible» W W0 → Not (v4 W0)) % 7.60/7.80 True) % 7.60/7.80 Clause #331 (by clausification #[330]): Or % 7.60/7.80 (Eq % 7.60/7.80 (∀ (W : «$ki_world»), % 7.60/7.80 «$ki_accessible» «$ki_local_world» W → ∀ (W0 : «$ki_world»), «$ki_accessible» W W0 → Not (v4 W0)) % 7.60/7.80 True) % 7.60/7.80 (Or (Eq (Or (v1 «$ki_local_world») (Not (v4 «$ki_local_world»))) True) % 7.60/7.80 (Eq % 7.60/7.80 (∀ (W : «$ki_world»), % 7.60/7.80 «$ki_accessible» «$ki_local_world» W → ∀ (W0 : «$ki_world»), «$ki_accessible» W W0 → Not (v3 W0)) % 7.60/7.80 True)) % 7.60/7.80 Clause #332 (by clausification #[331]): ∀ (a : «$ki_world»), % 7.60/7.80 Or (Eq (Or (v1 «$ki_local_world») (Not (v4 «$ki_local_world»))) True) % 7.60/7.80 (Or % 7.60/7.80 (Eq % 7.60/7.80 (∀ (W : «$ki_world»), % 7.60/7.80 «$ki_accessible» «$ki_local_world» W → ∀ (W0 : «$ki_world»), «$ki_accessible» W W0 → Not (v3 W0)) % 7.60/7.80 True) % 7.60/7.80 (Eq («$ki_accessible» «$ki_local_world» a → ∀ (W0 : «$ki_world»), «$ki_accessible» a W0 → Not (v4 W0)) True)) % 7.60/7.80 Clause #333 (by clausification #[332]): ∀ (a : «$ki_world»), % 7.60/7.80 Or % 7.60/7.80 (Eq % 7.60/7.80 (∀ (W : «$ki_world»), % 7.60/7.80 «$ki_accessible» «$ki_local_world» W → ∀ (W0 : «$ki_world»), «$ki_accessible» W W0 → Not (v3 W0)) % 7.60/7.80 True) % 7.60/7.80 (Or (Eq («$ki_accessible» «$ki_local_world» a → ∀ (W0 : «$ki_world»), «$ki_accessible» a W0 → Not (v4 W0)) True) % 7.60/7.80 (Or (Eq (v1 «$ki_local_world») True) (Eq (Not (v4 «$ki_local_world»)) True))) % 7.60/7.80 Clause #334 (by clausification #[333]): ∀ (a a_1 : «$ki_world»), % 7.60/7.80 Or (Eq («$ki_accessible» «$ki_local_world» a → ∀ (W0 : «$ki_world»), «$ki_accessible» a W0 → Not (v4 W0)) True) % 7.60/7.80 (Or (Eq (v1 «$ki_local_world») True) % 7.60/7.80 (Or (Eq (Not (v4 «$ki_local_world»)) True) % 7.60/7.80 (Eq («$ki_accessible» «$ki_local_world» a_1 → ∀ (W0 : «$ki_world»), «$ki_accessible» a_1 W0 → Not (v3 W0)) % 7.60/7.80 True))) % 7.60/7.80 Clause #335 (by clausification #[334]): ∀ (a a_1 : «$ki_world»), % 7.60/7.80 Or (Eq (v1 «$ki_local_world») True) % 7.60/7.80 (Or (Eq (Not (v4 «$ki_local_world»)) True) % 7.60/7.80 (Or (Eq («$ki_accessible» «$ki_local_world» a → ∀ (W0 : «$ki_world»), «$ki_accessible» a W0 → Not (v3 W0)) True) % 7.60/7.82 (Or (Eq («$ki_accessible» «$ki_local_world» a_1) False) % 7.60/7.82 (Eq (∀ (W0 : «$ki_world»), «$ki_accessible» a_1 W0 → Not (v4 W0)) True)))) % 7.60/7.82 Clause #336 (by clausification #[335]): ∀ (a a_1 : «$ki_world»), % 7.60/7.82 Or (Eq (v1 «$ki_local_world») True) % 7.60/7.82 (Or (Eq («$ki_accessible» «$ki_local_world» a → ∀ (W0 : «$ki_world»), «$ki_accessible» a W0 → Not (v3 W0)) True) % 7.60/7.82 (Or (Eq («$ki_accessible» «$ki_local_world» a_1) False) % 7.60/7.82 (Or (Eq (∀ (W0 : «$ki_world»), «$ki_accessible» a_1 W0 → Not (v4 W0)) True) (Eq (v4 «$ki_local_world») False)))) % 7.60/7.82 Clause #337 (by clausification #[336]): ∀ (a a_1 : «$ki_world»), % 7.60/7.82 Or (Eq (v1 «$ki_local_world») True) % 7.60/7.82 (Or (Eq («$ki_accessible» «$ki_local_world» a) False) % 7.60/7.82 (Or (Eq (∀ (W0 : «$ki_world»), «$ki_accessible» a W0 → Not (v4 W0)) True) % 7.60/7.82 (Or (Eq (v4 «$ki_local_world») False) % 7.60/7.82 (Or (Eq («$ki_accessible» «$ki_local_world» a_1) False) % 7.60/7.82 (Eq (∀ (W0 : «$ki_world»), «$ki_accessible» a_1 W0 → Not (v3 W0)) True))))) % 7.60/7.82 Clause #338 (by clausification #[337]): ∀ (a a_1 a_2 : «$ki_world»), % 7.60/7.82 Or (Eq (v1 «$ki_local_world») True) % 7.60/7.82 (Or (Eq («$ki_accessible» «$ki_local_world» a) False) % 7.60/7.82 (Or (Eq (v4 «$ki_local_world») False) % 7.60/7.82 (Or (Eq («$ki_accessible» «$ki_local_world» a_1) False) % 7.60/7.82 (Or (Eq (∀ (W0 : «$ki_world»), «$ki_accessible» a_1 W0 → Not (v3 W0)) True) % 7.60/7.82 (Eq («$ki_accessible» a a_2 → Not (v4 a_2)) True))))) % 7.60/7.82 Clause #339 (by clausification #[338]): ∀ (a a_1 a_2 a_3 : «$ki_world»), % 7.60/7.82 Or (Eq (v1 «$ki_local_world») True) % 7.60/7.82 (Or (Eq («$ki_accessible» «$ki_local_world» a) False) % 7.60/7.82 (Or (Eq (v4 «$ki_local_world») False) % 7.60/7.82 (Or (Eq («$ki_accessible» «$ki_local_world» a_1) False) % 7.60/7.82 (Or (Eq («$ki_accessible» a a_2 → Not (v4 a_2)) True) (Eq («$ki_accessible» a_1 a_3 → Not (v3 a_3)) True))))) % 7.60/7.82 Clause #340 (by clausification #[339]): ∀ (a a_1 a_2 a_3 : «$ki_world»), % 7.60/7.82 Or (Eq (v1 «$ki_local_world») True) % 7.60/7.82 (Or (Eq («$ki_accessible» «$ki_local_world» a) False) % 7.60/7.82 (Or (Eq (v4 «$ki_local_world») False) % 7.60/7.82 (Or (Eq («$ki_accessible» «$ki_local_world» a_1) False) % 7.60/7.82 (Or (Eq («$ki_accessible» a_1 a_2 → Not (v3 a_2)) True) % 7.60/7.82 (Or (Eq («$ki_accessible» a a_3) False) (Eq (Not (v4 a_3)) True)))))) % 7.60/7.82 Clause #341 (by clausification #[340]): ∀ (a a_1 a_2 a_3 : «$ki_world»), % 7.60/7.82 Or (Eq (v1 «$ki_local_world») True) % 7.60/7.82 (Or (Eq («$ki_accessible» «$ki_local_world» a) False) % 7.60/7.82 (Or (Eq (v4 «$ki_local_world») False) % 7.60/7.82 (Or (Eq («$ki_accessible» «$ki_local_world» a_1) False) % 7.60/7.82 (Or (Eq («$ki_accessible» a a_2) False) % 7.60/7.82 (Or (Eq (Not (v4 a_2)) True) (Or (Eq («$ki_accessible» a_1 a_3) False) (Eq (Not (v3 a_3)) True))))))) % 7.60/7.82 Clause #342 (by clausification #[341]): ∀ (a a_1 a_2 a_3 : «$ki_world»), % 7.60/7.82 Or (Eq (v1 «$ki_local_world») True) % 7.60/7.82 (Or (Eq («$ki_accessible» «$ki_local_world» a) False) % 7.60/7.82 (Or (Eq (v4 «$ki_local_world») False) % 7.60/7.82 (Or (Eq («$ki_accessible» «$ki_local_world» a_1) False) % 7.60/7.82 (Or (Eq («$ki_accessible» a a_2) False) % 7.60/7.82 (Or (Eq («$ki_accessible» a_1 a_3) False) (Or (Eq (Not (v3 a_3)) True) (Eq (v4 a_2) False))))))) % 7.60/7.82 Clause #343 (by clausification #[342]): ∀ (a a_1 a_2 a_3 : «$ki_world»), % 7.60/7.82 Or (Eq (v1 «$ki_local_world») True) % 7.60/7.82 (Or (Eq («$ki_accessible» «$ki_local_world» a) False) % 7.60/7.82 (Or (Eq (v4 «$ki_local_world») False) % 7.60/7.82 (Or (Eq («$ki_accessible» «$ki_local_world» a_1) False) % 7.60/7.82 (Or (Eq («$ki_accessible» a a_2) False) % 7.60/7.82 (Or (Eq («$ki_accessible» a_1 a_3) False) (Or (Eq (v4 a_2) False) (Eq (v3 a_3) False))))))) % 7.60/7.82 Clause #345 (by superposition #[343, 55]): ∀ (a a_1 a_2 : «$ki_world»), % 7.60/7.82 Or (Eq (v1 «$ki_local_world») True) % 7.60/7.82 (Or (Eq (v4 «$ki_local_world») False) % 7.60/7.82 (Or (Eq («$ki_accessible» «$ki_local_world» a) False) % 7.60/7.82 (Or (Eq («$ki_accessible» «$ki_local_world» a_1) False) % 7.67/7.84 (Or (Eq («$ki_accessible» a a_2) False) (Or (Eq (v4 a_1) False) (Or (Eq (v3 a_2) False) (Eq False True))))))) % 7.67/7.84 Clause #374 (by clausification #[36]): Or % 7.67/7.84 (Eq % 7.67/7.84 (Or (Or (Not (v1 «$ki_local_world»)) (Not (v3 «$ki_local_world»))) % 7.67/7.84 (∀ (W : «$ki_world»), «$ki_accessible» «$ki_local_world» W → Not (v3 W))) % 7.67/7.84 True) % 7.67/7.84 (Eq (∀ (W : «$ki_world»), «$ki_accessible» «$ki_local_world» W → ∀ (W0 : «$ki_world»), «$ki_accessible» W W0 → v4 W0) % 7.67/7.84 True) % 7.67/7.84 Clause #375 (by clausification #[374]): Or % 7.67/7.84 (Eq (∀ (W : «$ki_world»), «$ki_accessible» «$ki_local_world» W → ∀ (W0 : «$ki_world»), «$ki_accessible» W W0 → v4 W0) % 7.67/7.84 True) % 7.67/7.84 (Or (Eq (Or (Not (v1 «$ki_local_world»)) (Not (v3 «$ki_local_world»))) True) % 7.67/7.84 (Eq (∀ (W : «$ki_world»), «$ki_accessible» «$ki_local_world» W → Not (v3 W)) True)) % 7.67/7.84 Clause #376 (by clausification #[375]): ∀ (a : «$ki_world»), % 7.67/7.84 Or (Eq (Or (Not (v1 «$ki_local_world»)) (Not (v3 «$ki_local_world»))) True) % 7.67/7.84 (Or (Eq (∀ (W : «$ki_world»), «$ki_accessible» «$ki_local_world» W → Not (v3 W)) True) % 7.67/7.84 (Eq («$ki_accessible» «$ki_local_world» a → ∀ (W0 : «$ki_world»), «$ki_accessible» a W0 → v4 W0) True)) % 7.67/7.84 Clause #377 (by clausification #[376]): ∀ (a : «$ki_world»), % 7.67/7.84 Or (Eq (∀ (W : «$ki_world»), «$ki_accessible» «$ki_local_world» W → Not (v3 W)) True) % 7.67/7.84 (Or (Eq («$ki_accessible» «$ki_local_world» a → ∀ (W0 : «$ki_world»), «$ki_accessible» a W0 → v4 W0) True) % 7.67/7.84 (Or (Eq (Not (v1 «$ki_local_world»)) True) (Eq (Not (v3 «$ki_local_world»)) True))) % 7.67/7.84 Clause #378 (by clausification #[377]): ∀ (a a_1 : «$ki_world»), % 7.67/7.84 Or (Eq («$ki_accessible» «$ki_local_world» a → ∀ (W0 : «$ki_world»), «$ki_accessible» a W0 → v4 W0) True) % 7.67/7.84 (Or (Eq (Not (v1 «$ki_local_world»)) True) % 7.67/7.84 (Or (Eq (Not (v3 «$ki_local_world»)) True) (Eq («$ki_accessible» «$ki_local_world» a_1 → Not (v3 a_1)) True))) % 7.67/7.84 Clause #379 (by clausification #[378]): ∀ (a a_1 : «$ki_world»), % 7.67/7.84 Or (Eq (Not (v1 «$ki_local_world»)) True) % 7.67/7.84 (Or (Eq (Not (v3 «$ki_local_world»)) True) % 7.67/7.84 (Or (Eq («$ki_accessible» «$ki_local_world» a → Not (v3 a)) True) % 7.67/7.84 (Or (Eq («$ki_accessible» «$ki_local_world» a_1) False) % 7.67/7.84 (Eq (∀ (W0 : «$ki_world»), «$ki_accessible» a_1 W0 → v4 W0) True)))) % 7.67/7.84 Clause #380 (by clausification #[379]): ∀ (a a_1 : «$ki_world»), % 7.67/7.84 Or (Eq (Not (v3 «$ki_local_world»)) True) % 7.67/7.84 (Or (Eq («$ki_accessible» «$ki_local_world» a → Not (v3 a)) True) % 7.67/7.84 (Or (Eq («$ki_accessible» «$ki_local_world» a_1) False) % 7.67/7.84 (Or (Eq (∀ (W0 : «$ki_world»), «$ki_accessible» a_1 W0 → v4 W0) True) (Eq (v1 «$ki_local_world») False)))) % 7.67/7.84 Clause #381 (by clausification #[380]): ∀ (a a_1 : «$ki_world»), % 7.67/7.84 Or (Eq («$ki_accessible» «$ki_local_world» a → Not (v3 a)) True) % 7.67/7.84 (Or (Eq («$ki_accessible» «$ki_local_world» a_1) False) % 7.67/7.84 (Or (Eq (∀ (W0 : «$ki_world»), «$ki_accessible» a_1 W0 → v4 W0) True) % 7.67/7.84 (Or (Eq (v1 «$ki_local_world») False) (Eq (v3 «$ki_local_world») False)))) % 7.67/7.84 Clause #382 (by clausification #[381]): ∀ (a a_1 : «$ki_world»), % 7.67/7.84 Or (Eq («$ki_accessible» «$ki_local_world» a) False) % 7.67/7.84 (Or (Eq (∀ (W0 : «$ki_world»), «$ki_accessible» a W0 → v4 W0) True) % 7.67/7.84 (Or (Eq (v1 «$ki_local_world») False) % 7.67/7.84 (Or (Eq (v3 «$ki_local_world») False) % 7.67/7.84 (Or (Eq («$ki_accessible» «$ki_local_world» a_1) False) (Eq (Not (v3 a_1)) True))))) % 7.67/7.84 Clause #383 (by clausification #[382]): ∀ (a a_1 a_2 : «$ki_world»), % 7.67/7.84 Or (Eq («$ki_accessible» «$ki_local_world» a) False) % 7.67/7.84 (Or (Eq (v1 «$ki_local_world») False) % 7.67/7.84 (Or (Eq (v3 «$ki_local_world») False) % 7.67/7.84 (Or (Eq («$ki_accessible» «$ki_local_world» a_1) False) % 7.67/7.84 (Or (Eq (Not (v3 a_1)) True) (Eq («$ki_accessible» a a_2 → v4 a_2) True))))) % 7.67/7.84 Clause #384 (by clausification #[383]): ∀ (a a_1 a_2 : «$ki_world»), % 7.67/7.84 Or (Eq («$ki_accessible» «$ki_local_world» a) False) % 7.67/7.84 (Or (Eq (v1 «$ki_local_world») False) % 7.67/7.86 (Or (Eq (v3 «$ki_local_world») False) % 7.67/7.86 (Or (Eq («$ki_accessible» «$ki_local_world» a_1) False) % 7.67/7.86 (Or (Eq («$ki_accessible» a a_2 → v4 a_2) True) (Eq (v3 a_1) False))))) % 7.67/7.86 Clause #385 (by clausification #[384]): ∀ (a a_1 a_2 : «$ki_world»), % 7.67/7.86 Or (Eq («$ki_accessible» «$ki_local_world» a) False) % 7.67/7.86 (Or (Eq (v1 «$ki_local_world») False) % 7.67/7.86 (Or (Eq (v3 «$ki_local_world») False) % 7.67/7.86 (Or (Eq («$ki_accessible» «$ki_local_world» a_1) False) % 7.67/7.86 (Or (Eq (v3 a_1) False) (Or (Eq («$ki_accessible» a a_2) False) (Eq (v4 a_2) True)))))) % 7.67/7.86 Clause #387 (by superposition #[385, 55]): ∀ (a a_1 : «$ki_world»), % 7.67/7.86 Or (Eq (v1 «$ki_local_world») False) % 7.67/7.86 (Or (Eq (v3 «$ki_local_world») False) % 7.67/7.86 (Or (Eq («$ki_accessible» «$ki_local_world» a) False) % 7.67/7.86 (Or (Eq (v3 a) False) % 7.67/7.86 (Or (Eq («$ki_accessible» «$ki_local_world» a_1) False) (Or (Eq (v4 a_1) True) (Eq False True)))))) % 7.67/7.86 Clause #402 (by clausification #[34]): Or % 7.67/7.86 (Eq % 7.67/7.86 (Or (Or (Not (v1 «$ki_local_world»)) (Not (v2 «$ki_local_world»))) % 7.67/7.86 (∀ (W : «$ki_world»), «$ki_accessible» «$ki_local_world» W → v3 W)) % 7.67/7.86 True) % 7.67/7.86 (Eq % 7.67/7.86 (∀ (W : «$ki_world»), % 7.67/7.86 «$ki_accessible» «$ki_local_world» W → ∀ (W0 : «$ki_world»), «$ki_accessible» W W0 → Not (v1 W0)) % 7.67/7.86 True) % 7.67/7.86 Clause #403 (by clausification #[402]): Or % 7.67/7.86 (Eq % 7.67/7.86 (∀ (W : «$ki_world»), % 7.67/7.86 «$ki_accessible» «$ki_local_world» W → ∀ (W0 : «$ki_world»), «$ki_accessible» W W0 → Not (v1 W0)) % 7.67/7.86 True) % 7.67/7.86 (Or (Eq (Or (Not (v1 «$ki_local_world»)) (Not (v2 «$ki_local_world»))) True) % 7.67/7.86 (Eq (∀ (W : «$ki_world»), «$ki_accessible» «$ki_local_world» W → v3 W) True)) % 7.67/7.86 Clause #404 (by clausification #[403]): ∀ (a : «$ki_world»), % 7.67/7.86 Or (Eq (Or (Not (v1 «$ki_local_world»)) (Not (v2 «$ki_local_world»))) True) % 7.67/7.86 (Or (Eq (∀ (W : «$ki_world»), «$ki_accessible» «$ki_local_world» W → v3 W) True) % 7.67/7.86 (Eq («$ki_accessible» «$ki_local_world» a → ∀ (W0 : «$ki_world»), «$ki_accessible» a W0 → Not (v1 W0)) True)) % 7.67/7.86 Clause #405 (by clausification #[404]): ∀ (a : «$ki_world»), % 7.67/7.86 Or (Eq (∀ (W : «$ki_world»), «$ki_accessible» «$ki_local_world» W → v3 W) True) % 7.67/7.86 (Or (Eq («$ki_accessible» «$ki_local_world» a → ∀ (W0 : «$ki_world»), «$ki_accessible» a W0 → Not (v1 W0)) True) % 7.67/7.86 (Or (Eq (Not (v1 «$ki_local_world»)) True) (Eq (Not (v2 «$ki_local_world»)) True))) % 7.67/7.86 Clause #406 (by clausification #[405]): ∀ (a a_1 : «$ki_world»), % 7.67/7.86 Or (Eq («$ki_accessible» «$ki_local_world» a → ∀ (W0 : «$ki_world»), «$ki_accessible» a W0 → Not (v1 W0)) True) % 7.67/7.86 (Or (Eq (Not (v1 «$ki_local_world»)) True) % 7.67/7.86 (Or (Eq (Not (v2 «$ki_local_world»)) True) (Eq («$ki_accessible» «$ki_local_world» a_1 → v3 a_1) True))) % 7.67/7.86 Clause #407 (by clausification #[406]): ∀ (a a_1 : «$ki_world»), % 7.67/7.86 Or (Eq (Not (v1 «$ki_local_world»)) True) % 7.67/7.86 (Or (Eq (Not (v2 «$ki_local_world»)) True) % 7.67/7.86 (Or (Eq («$ki_accessible» «$ki_local_world» a → v3 a) True) % 7.67/7.86 (Or (Eq («$ki_accessible» «$ki_local_world» a_1) False) % 7.67/7.86 (Eq (∀ (W0 : «$ki_world»), «$ki_accessible» a_1 W0 → Not (v1 W0)) True)))) % 7.67/7.86 Clause #408 (by clausification #[407]): ∀ (a a_1 : «$ki_world»), % 7.67/7.86 Or (Eq (Not (v2 «$ki_local_world»)) True) % 7.67/7.86 (Or (Eq («$ki_accessible» «$ki_local_world» a → v3 a) True) % 7.67/7.86 (Or (Eq («$ki_accessible» «$ki_local_world» a_1) False) % 7.67/7.86 (Or (Eq (∀ (W0 : «$ki_world»), «$ki_accessible» a_1 W0 → Not (v1 W0)) True) (Eq (v1 «$ki_local_world») False)))) % 7.67/7.86 Clause #409 (by clausification #[408]): ∀ (a a_1 : «$ki_world»), % 7.67/7.86 Or (Eq («$ki_accessible» «$ki_local_world» a → v3 a) True) % 7.67/7.86 (Or (Eq («$ki_accessible» «$ki_local_world» a_1) False) % 7.67/7.86 (Or (Eq (∀ (W0 : «$ki_world»), «$ki_accessible» a_1 W0 → Not (v1 W0)) True) % 7.67/7.86 (Or (Eq (v1 «$ki_local_world») False) (Eq (v2 «$ki_local_world») False)))) % 7.67/7.86 Clause #410 (by clausification #[409]): ∀ (a a_1 : «$ki_world»), % 7.67/7.86 Or (Eq («$ki_accessible» «$ki_local_world» a) False) % 7.71/7.88 (Or (Eq (∀ (W0 : «$ki_world»), «$ki_accessible» a W0 → Not (v1 W0)) True) % 7.71/7.88 (Or (Eq (v1 «$ki_local_world») False) % 7.71/7.88 (Or (Eq (v2 «$ki_local_world») False) % 7.71/7.88 (Or (Eq («$ki_accessible» «$ki_local_world» a_1) False) (Eq (v3 a_1) True))))) % 7.71/7.88 Clause #411 (by clausification #[410]): ∀ (a a_1 a_2 : «$ki_world»), % 7.71/7.88 Or (Eq («$ki_accessible» «$ki_local_world» a) False) % 7.71/7.88 (Or (Eq (v1 «$ki_local_world») False) % 7.71/7.88 (Or (Eq (v2 «$ki_local_world») False) % 7.71/7.88 (Or (Eq («$ki_accessible» «$ki_local_world» a_1) False) % 7.71/7.88 (Or (Eq (v3 a_1) True) (Eq («$ki_accessible» a a_2 → Not (v1 a_2)) True))))) % 7.71/7.88 Clause #412 (by clausification #[411]): ∀ (a a_1 a_2 : «$ki_world»), % 7.71/7.88 Or (Eq («$ki_accessible» «$ki_local_world» a) False) % 7.71/7.88 (Or (Eq (v1 «$ki_local_world») False) % 7.71/7.88 (Or (Eq (v2 «$ki_local_world») False) % 7.71/7.88 (Or (Eq («$ki_accessible» «$ki_local_world» a_1) False) % 7.71/7.88 (Or (Eq (v3 a_1) True) (Or (Eq («$ki_accessible» a a_2) False) (Eq (Not (v1 a_2)) True)))))) % 7.71/7.88 Clause #413 (by clausification #[412]): ∀ (a a_1 a_2 : «$ki_world»), % 7.71/7.88 Or (Eq («$ki_accessible» «$ki_local_world» a) False) % 7.71/7.88 (Or (Eq (v1 «$ki_local_world») False) % 7.71/7.88 (Or (Eq (v2 «$ki_local_world») False) % 7.71/7.88 (Or (Eq («$ki_accessible» «$ki_local_world» a_1) False) % 7.71/7.88 (Or (Eq (v3 a_1) True) (Or (Eq («$ki_accessible» a a_2) False) (Eq (v1 a_2) False)))))) % 7.71/7.88 Clause #415 (by superposition #[413, 55]): ∀ (a a_1 : «$ki_world»), % 7.71/7.88 Or (Eq (v1 «$ki_local_world») False) % 7.71/7.88 (Or (Eq (v2 «$ki_local_world») False) % 7.71/7.88 (Or (Eq («$ki_accessible» «$ki_local_world» a) False) % 7.71/7.88 (Or (Eq (v3 a) True) % 7.71/7.88 (Or (Eq («$ki_accessible» «$ki_local_world» a_1) False) (Or (Eq (v1 a_1) False) (Eq False True)))))) % 7.71/7.88 Clause #445 (by clausification #[415]): ∀ (a a_1 : «$ki_world»), % 7.71/7.88 Or (Eq (v1 «$ki_local_world») False) % 7.71/7.88 (Or (Eq (v2 «$ki_local_world») False) % 7.71/7.88 (Or (Eq («$ki_accessible» «$ki_local_world» a) False) % 7.71/7.88 (Or (Eq (v3 a) True) (Or (Eq («$ki_accessible» «$ki_local_world» a_1) False) (Eq (v1 a_1) False))))) % 7.71/7.88 Clause #446 (by clausification #[35]): Or % 7.71/7.88 (Eq % 7.71/7.88 (Or (Or (Not (v1 «$ki_local_world»)) (Not (v2 «$ki_local_world»))) % 7.71/7.88 (∀ (W : «$ki_world»), «$ki_accessible» «$ki_local_world» W → Not (v4 W))) % 7.71/7.88 True) % 7.71/7.88 (Eq % 7.71/7.88 (∀ (W : «$ki_world»), % 7.71/7.88 «$ki_accessible» «$ki_local_world» W → ∀ (W0 : «$ki_world»), «$ki_accessible» W W0 → Not (v1 W0)) % 7.71/7.88 True) % 7.71/7.88 Clause #447 (by clausification #[446]): Or % 7.71/7.88 (Eq % 7.71/7.88 (∀ (W : «$ki_world»), % 7.71/7.88 «$ki_accessible» «$ki_local_world» W → ∀ (W0 : «$ki_world»), «$ki_accessible» W W0 → Not (v1 W0)) % 7.71/7.88 True) % 7.71/7.88 (Or (Eq (Or (Not (v1 «$ki_local_world»)) (Not (v2 «$ki_local_world»))) True) % 7.71/7.88 (Eq (∀ (W : «$ki_world»), «$ki_accessible» «$ki_local_world» W → Not (v4 W)) True)) % 7.71/7.88 Clause #448 (by clausification #[447]): ∀ (a : «$ki_world»), % 7.71/7.88 Or (Eq (Or (Not (v1 «$ki_local_world»)) (Not (v2 «$ki_local_world»))) True) % 7.71/7.88 (Or (Eq (∀ (W : «$ki_world»), «$ki_accessible» «$ki_local_world» W → Not (v4 W)) True) % 7.71/7.88 (Eq («$ki_accessible» «$ki_local_world» a → ∀ (W0 : «$ki_world»), «$ki_accessible» a W0 → Not (v1 W0)) True)) % 7.71/7.88 Clause #449 (by clausification #[448]): ∀ (a : «$ki_world»), % 7.71/7.88 Or (Eq (∀ (W : «$ki_world»), «$ki_accessible» «$ki_local_world» W → Not (v4 W)) True) % 7.71/7.88 (Or (Eq («$ki_accessible» «$ki_local_world» a → ∀ (W0 : «$ki_world»), «$ki_accessible» a W0 → Not (v1 W0)) True) % 7.71/7.88 (Or (Eq (Not (v1 «$ki_local_world»)) True) (Eq (Not (v2 «$ki_local_world»)) True))) % 7.71/7.88 Clause #450 (by clausification #[449]): ∀ (a a_1 : «$ki_world»), % 7.71/7.88 Or (Eq («$ki_accessible» «$ki_local_world» a → ∀ (W0 : «$ki_world»), «$ki_accessible» a W0 → Not (v1 W0)) True) % 7.71/7.88 (Or (Eq (Not (v1 «$ki_local_world»)) True) % 7.71/7.88 (Or (Eq (Not (v2 «$ki_local_world»)) True) (Eq («$ki_accessible» «$ki_local_world» a_1 → Not (v4 a_1)) True))) % 7.71/7.90 Clause #451 (by clausification #[450]): ∀ (a a_1 : «$ki_world»), % 7.71/7.90 Or (Eq (Not (v1 «$ki_local_world»)) True) % 7.71/7.90 (Or (Eq (Not (v2 «$ki_local_world»)) True) % 7.71/7.90 (Or (Eq («$ki_accessible» «$ki_local_world» a → Not (v4 a)) True) % 7.71/7.90 (Or (Eq («$ki_accessible» «$ki_local_world» a_1) False) % 7.71/7.90 (Eq (∀ (W0 : «$ki_world»), «$ki_accessible» a_1 W0 → Not (v1 W0)) True)))) % 7.71/7.90 Clause #452 (by clausification #[451]): ∀ (a a_1 : «$ki_world»), % 7.71/7.90 Or (Eq (Not (v2 «$ki_local_world»)) True) % 7.71/7.90 (Or (Eq («$ki_accessible» «$ki_local_world» a → Not (v4 a)) True) % 7.71/7.90 (Or (Eq («$ki_accessible» «$ki_local_world» a_1) False) % 7.71/7.90 (Or (Eq (∀ (W0 : «$ki_world»), «$ki_accessible» a_1 W0 → Not (v1 W0)) True) (Eq (v1 «$ki_local_world») False)))) % 7.71/7.90 Clause #453 (by clausification #[452]): ∀ (a a_1 : «$ki_world»), % 7.71/7.90 Or (Eq («$ki_accessible» «$ki_local_world» a → Not (v4 a)) True) % 7.71/7.90 (Or (Eq («$ki_accessible» «$ki_local_world» a_1) False) % 7.71/7.90 (Or (Eq (∀ (W0 : «$ki_world»), «$ki_accessible» a_1 W0 → Not (v1 W0)) True) % 7.71/7.90 (Or (Eq (v1 «$ki_local_world») False) (Eq (v2 «$ki_local_world») False)))) % 7.71/7.90 Clause #454 (by clausification #[453]): ∀ (a a_1 : «$ki_world»), % 7.71/7.90 Or (Eq («$ki_accessible» «$ki_local_world» a) False) % 7.71/7.90 (Or (Eq (∀ (W0 : «$ki_world»), «$ki_accessible» a W0 → Not (v1 W0)) True) % 7.71/7.90 (Or (Eq (v1 «$ki_local_world») False) % 7.71/7.90 (Or (Eq (v2 «$ki_local_world») False) % 7.71/7.90 (Or (Eq («$ki_accessible» «$ki_local_world» a_1) False) (Eq (Not (v4 a_1)) True))))) % 7.71/7.90 Clause #455 (by clausification #[454]): ∀ (a a_1 a_2 : «$ki_world»), % 7.71/7.90 Or (Eq («$ki_accessible» «$ki_local_world» a) False) % 7.71/7.90 (Or (Eq (v1 «$ki_local_world») False) % 7.71/7.90 (Or (Eq (v2 «$ki_local_world») False) % 7.71/7.90 (Or (Eq («$ki_accessible» «$ki_local_world» a_1) False) % 7.71/7.90 (Or (Eq (Not (v4 a_1)) True) (Eq («$ki_accessible» a a_2 → Not (v1 a_2)) True))))) % 7.71/7.90 Clause #456 (by clausification #[455]): ∀ (a a_1 a_2 : «$ki_world»), % 7.71/7.90 Or (Eq («$ki_accessible» «$ki_local_world» a) False) % 7.71/7.90 (Or (Eq (v1 «$ki_local_world») False) % 7.71/7.90 (Or (Eq (v2 «$ki_local_world») False) % 7.71/7.90 (Or (Eq («$ki_accessible» «$ki_local_world» a_1) False) % 7.71/7.90 (Or (Eq («$ki_accessible» a a_2 → Not (v1 a_2)) True) (Eq (v4 a_1) False))))) % 7.71/7.90 Clause #457 (by clausification #[456]): ∀ (a a_1 a_2 : «$ki_world»), % 7.71/7.90 Or (Eq («$ki_accessible» «$ki_local_world» a) False) % 7.71/7.90 (Or (Eq (v1 «$ki_local_world») False) % 7.71/7.90 (Or (Eq (v2 «$ki_local_world») False) % 7.71/7.90 (Or (Eq («$ki_accessible» «$ki_local_world» a_1) False) % 7.71/7.90 (Or (Eq (v4 a_1) False) (Or (Eq («$ki_accessible» a a_2) False) (Eq (Not (v1 a_2)) True)))))) % 7.71/7.90 Clause #458 (by clausification #[457]): ∀ (a a_1 a_2 : «$ki_world»), % 7.71/7.90 Or (Eq («$ki_accessible» «$ki_local_world» a) False) % 7.71/7.90 (Or (Eq (v1 «$ki_local_world») False) % 7.71/7.90 (Or (Eq (v2 «$ki_local_world») False) % 7.71/7.90 (Or (Eq («$ki_accessible» «$ki_local_world» a_1) False) % 7.71/7.90 (Or (Eq (v4 a_1) False) (Or (Eq («$ki_accessible» a a_2) False) (Eq (v1 a_2) False)))))) % 7.71/7.90 Clause #460 (by superposition #[458, 55]): ∀ (a a_1 : «$ki_world»), % 7.71/7.90 Or (Eq (v1 «$ki_local_world») False) % 7.71/7.90 (Or (Eq (v2 «$ki_local_world») False) % 7.71/7.90 (Or (Eq («$ki_accessible» «$ki_local_world» a) False) % 7.71/7.90 (Or (Eq (v4 a) False) % 7.71/7.90 (Or (Eq («$ki_accessible» «$ki_local_world» a_1) False) (Or (Eq (v1 a_1) False) (Eq False True)))))) % 7.71/7.90 Clause #461 (by clausification #[460]): ∀ (a a_1 : «$ki_world»), % 7.71/7.90 Or (Eq (v1 «$ki_local_world») False) % 7.71/7.90 (Or (Eq (v2 «$ki_local_world») False) % 7.71/7.90 (Or (Eq («$ki_accessible» «$ki_local_world» a) False) % 7.71/7.90 (Or (Eq (v4 a) False) (Or (Eq («$ki_accessible» «$ki_local_world» a_1) False) (Eq (v1 a_1) False))))) % 7.71/7.90 Clause #462 (by clausification #[329]): ∀ (a a_1 : «$ki_world»), % 7.71/7.90 Or (Eq (v2 «$ki_local_world») True) % 7.71/7.90 (Or (Eq (v3 «$ki_local_world») False) % 7.71/7.90 (Or (Eq («$ki_accessible» «$ki_local_world» a) False) % 7.71/7.90 (Or (Eq (v1 a) False) (Or (Eq («$ki_accessible» «$ki_local_world» a_1) False) (Eq (v1 a_1) False))))) % 7.71/7.92 Clause #565 (by clausification #[137]): ∀ (a a_1 : «$ki_world»), % 7.71/7.92 Or (Eq (v1 «$ki_local_world») True) % 7.71/7.92 (Or (Eq (v2 «$ki_local_world») True) % 7.71/7.92 (Or (Eq («$ki_accessible» «$ki_local_world» a) False) % 7.71/7.92 (Or (Eq (v3 a) False) (Or (Eq («$ki_accessible» «$ki_local_world» a_1) False) (Eq (v1 a_1) True))))) % 7.71/7.92 Clause #567 (by superposition #[565, 55]): ∀ (a : «$ki_world»), % 7.71/7.92 Or (Eq (v1 «$ki_local_world») True) % 7.71/7.92 (Or (Eq (v2 «$ki_local_world») True) % 7.71/7.92 (Or (Eq (v3 «$ki_local_world») False) % 7.71/7.92 (Or (Eq («$ki_accessible» «$ki_local_world» a) False) (Or (Eq (v1 a) True) (Eq False True))))) % 7.71/7.92 Clause #568 (by clausification #[567]): ∀ (a : «$ki_world»), % 7.71/7.92 Or (Eq (v1 «$ki_local_world») True) % 7.71/7.92 (Or (Eq (v2 «$ki_local_world») True) % 7.71/7.92 (Or (Eq (v3 «$ki_local_world») False) (Or (Eq («$ki_accessible» «$ki_local_world» a) False) (Eq (v1 a) True)))) % 7.71/7.92 Clause #571 (by clausification #[234]): ∀ (a a_1 : «$ki_world»), % 7.71/7.92 Or (Eq (v4 «$ki_local_world») True) % 7.71/7.92 (Or (Eq (v1 «$ki_local_world») False) % 7.71/7.92 (Or (Eq («$ki_accessible» «$ki_local_world» a) False) % 7.71/7.92 (Or (Eq (v1 a) False) (Or (Eq («$ki_accessible» «$ki_local_world» a_1) False) (Eq (v3 a_1) True))))) % 7.71/7.92 Clause #591 (by clausification #[125]): ∀ (a a_1 : «$ki_world»), % 7.71/7.92 Or (Eq (v3 «$ki_local_world») True) % 7.71/7.92 (Or (Eq (v4 «$ki_local_world») True) % 7.71/7.92 (Or (Eq («$ki_accessible» «$ki_local_world» a) False) % 7.71/7.92 (Or (Eq (v2 a) True) (Or (Eq («$ki_accessible» «$ki_local_world» a_1) False) (Eq (v1 a_1) True))))) % 7.71/7.92 Clause #593 (by superposition #[591, 55]): ∀ (a : «$ki_world»), % 7.71/7.92 Or (Eq (v3 «$ki_local_world») True) % 7.71/7.92 (Or (Eq (v4 «$ki_local_world») True) % 7.71/7.92 (Or (Eq (v2 «$ki_local_world») True) % 7.71/7.92 (Or (Eq («$ki_accessible» «$ki_local_world» a) False) (Or (Eq (v1 a) True) (Eq False True))))) % 7.71/7.92 Clause #594 (by clausification #[593]): ∀ (a : «$ki_world»), % 7.71/7.92 Or (Eq (v3 «$ki_local_world») True) % 7.71/7.92 (Or (Eq (v4 «$ki_local_world») True) % 7.71/7.92 (Or (Eq (v2 «$ki_local_world») True) (Or (Eq («$ki_accessible» «$ki_local_world» a) False) (Eq (v1 a) True)))) % 7.71/7.92 Clause #596 (by superposition #[594, 55]): Or (Eq (v3 «$ki_local_world») True) % 7.71/7.92 (Or (Eq (v4 «$ki_local_world») True) % 7.71/7.92 (Or (Eq (v2 «$ki_local_world») True) (Or (Eq (v1 «$ki_local_world») True) (Eq False True)))) % 7.71/7.92 Clause #597 (by clausification #[596]): Or (Eq (v3 «$ki_local_world») True) % 7.71/7.92 (Or (Eq (v4 «$ki_local_world») True) (Or (Eq (v2 «$ki_local_world») True) (Eq (v1 «$ki_local_world») True))) % 7.71/7.92 Clause #604 (by superposition #[597, 568]): ∀ (a : «$ki_world»), % 7.71/7.92 Or (Eq (v4 «$ki_local_world») True) % 7.71/7.92 (Or (Eq (v2 «$ki_local_world») True) % 7.71/7.92 (Or (Eq (v1 «$ki_local_world») True) % 7.71/7.92 (Or (Eq (v1 «$ki_local_world») True) % 7.71/7.92 (Or (Eq (v2 «$ki_local_world») True) % 7.71/7.92 (Or (Eq True False) (Or (Eq («$ki_accessible» «$ki_local_world» a) False) (Eq (v1 a) True))))))) % 7.71/7.92 Clause #610 (by clausification #[27]): Or % 7.71/7.92 (Eq % 7.71/7.92 (Or (Or (v3 «$ki_local_world») (Not (v4 «$ki_local_world»))) % 7.71/7.92 (∀ (W : «$ki_world»), «$ki_accessible» «$ki_local_world» W → ∀ (W0 : «$ki_world»), «$ki_accessible» W W0 → v3 W0)) % 7.71/7.92 True) % 7.71/7.92 (Eq % 7.71/7.92 (∀ (W : «$ki_world»), % 7.71/7.92 «$ki_accessible» «$ki_local_world» W → ∀ (W0 : «$ki_world»), «$ki_accessible» W W0 → Not (v4 W0)) % 7.71/7.92 True) % 7.71/7.92 Clause #611 (by clausification #[610]): Or % 7.71/7.92 (Eq % 7.71/7.92 (∀ (W : «$ki_world»), % 7.71/7.92 «$ki_accessible» «$ki_local_world» W → ∀ (W0 : «$ki_world»), «$ki_accessible» W W0 → Not (v4 W0)) % 7.71/7.92 True) % 7.71/7.92 (Or (Eq (Or (v3 «$ki_local_world») (Not (v4 «$ki_local_world»))) True) % 7.71/7.92 (Eq % 7.71/7.92 (∀ (W : «$ki_world»), «$ki_accessible» «$ki_local_world» W → ∀ (W0 : «$ki_world»), «$ki_accessible» W W0 → v3 W0) % 7.71/7.92 True)) % 7.71/7.92 Clause #612 (by clausification #[611]): ∀ (a : «$ki_world»), % 7.71/7.92 Or (Eq (Or (v3 «$ki_local_world») (Not (v4 «$ki_local_world»))) True) % 7.71/7.92 (Or % 7.71/7.92 (Eq % 7.71/7.92 (∀ (W : «$ki_world»), % 7.77/7.93 «$ki_accessible» «$ki_local_world» W → ∀ (W0 : «$ki_world»), «$ki_accessible» W W0 → v3 W0) % 7.77/7.93 True) % 7.77/7.93 (Eq («$ki_accessible» «$ki_local_world» a → ∀ (W0 : «$ki_world»), «$ki_accessible» a W0 → Not (v4 W0)) True)) % 7.77/7.93 Clause #613 (by clausification #[612]): ∀ (a : «$ki_world»), % 7.77/7.93 Or % 7.77/7.93 (Eq % 7.77/7.93 (∀ (W : «$ki_world»), «$ki_accessible» «$ki_local_world» W → ∀ (W0 : «$ki_world»), «$ki_accessible» W W0 → v3 W0) % 7.77/7.93 True) % 7.77/7.93 (Or (Eq («$ki_accessible» «$ki_local_world» a → ∀ (W0 : «$ki_world»), «$ki_accessible» a W0 → Not (v4 W0)) True) % 7.77/7.93 (Or (Eq (v3 «$ki_local_world») True) (Eq (Not (v4 «$ki_local_world»)) True))) % 7.77/7.93 Clause #614 (by clausification #[613]): ∀ (a a_1 : «$ki_world»), % 7.77/7.93 Or (Eq («$ki_accessible» «$ki_local_world» a → ∀ (W0 : «$ki_world»), «$ki_accessible» a W0 → Not (v4 W0)) True) % 7.77/7.93 (Or (Eq (v3 «$ki_local_world») True) % 7.77/7.93 (Or (Eq (Not (v4 «$ki_local_world»)) True) % 7.77/7.93 (Eq («$ki_accessible» «$ki_local_world» a_1 → ∀ (W0 : «$ki_world»), «$ki_accessible» a_1 W0 → v3 W0) True))) % 7.77/7.93 Clause #615 (by clausification #[614]): ∀ (a a_1 : «$ki_world»), % 7.77/7.93 Or (Eq (v3 «$ki_local_world») True) % 7.77/7.93 (Or (Eq (Not (v4 «$ki_local_world»)) True) % 7.77/7.93 (Or (Eq («$ki_accessible» «$ki_local_world» a → ∀ (W0 : «$ki_world»), «$ki_accessible» a W0 → v3 W0) True) % 7.77/7.93 (Or (Eq («$ki_accessible» «$ki_local_world» a_1) False) % 7.77/7.93 (Eq (∀ (W0 : «$ki_world»), «$ki_accessible» a_1 W0 → Not (v4 W0)) True)))) % 7.77/7.93 Clause #616 (by clausification #[615]): ∀ (a a_1 : «$ki_world»), % 7.77/7.93 Or (Eq (v3 «$ki_local_world») True) % 7.77/7.93 (Or (Eq («$ki_accessible» «$ki_local_world» a → ∀ (W0 : «$ki_world»), «$ki_accessible» a W0 → v3 W0) True) % 7.77/7.93 (Or (Eq («$ki_accessible» «$ki_local_world» a_1) False) % 7.77/7.93 (Or (Eq (∀ (W0 : «$ki_world»), «$ki_accessible» a_1 W0 → Not (v4 W0)) True) (Eq (v4 «$ki_local_world») False)))) % 7.77/7.93 Clause #617 (by clausification #[616]): ∀ (a a_1 : «$ki_world»), % 7.77/7.93 Or (Eq (v3 «$ki_local_world») True) % 7.77/7.93 (Or (Eq («$ki_accessible» «$ki_local_world» a) False) % 7.77/7.93 (Or (Eq (∀ (W0 : «$ki_world»), «$ki_accessible» a W0 → Not (v4 W0)) True) % 7.77/7.93 (Or (Eq (v4 «$ki_local_world») False) % 7.77/7.93 (Or (Eq («$ki_accessible» «$ki_local_world» a_1) False) % 7.77/7.93 (Eq (∀ (W0 : «$ki_world»), «$ki_accessible» a_1 W0 → v3 W0) True))))) % 7.77/7.93 Clause #618 (by clausification #[617]): ∀ (a a_1 a_2 : «$ki_world»), % 7.77/7.93 Or (Eq (v3 «$ki_local_world») True) % 7.77/7.93 (Or (Eq («$ki_accessible» «$ki_local_world» a) False) % 7.77/7.93 (Or (Eq (v4 «$ki_local_world») False) % 7.77/7.93 (Or (Eq («$ki_accessible» «$ki_local_world» a_1) False) % 7.77/7.93 (Or (Eq (∀ (W0 : «$ki_world»), «$ki_accessible» a_1 W0 → v3 W0) True) % 7.77/7.93 (Eq («$ki_accessible» a a_2 → Not (v4 a_2)) True))))) % 7.77/7.93 Clause #619 (by clausification #[618]): ∀ (a a_1 a_2 a_3 : «$ki_world»), % 7.77/7.93 Or (Eq (v3 «$ki_local_world») True) % 7.77/7.93 (Or (Eq («$ki_accessible» «$ki_local_world» a) False) % 7.77/7.93 (Or (Eq (v4 «$ki_local_world») False) % 7.77/7.93 (Or (Eq («$ki_accessible» «$ki_local_world» a_1) False) % 7.77/7.93 (Or (Eq («$ki_accessible» a a_2 → Not (v4 a_2)) True) (Eq («$ki_accessible» a_1 a_3 → v3 a_3) True))))) % 7.77/7.93 Clause #620 (by clausification #[619]): ∀ (a a_1 a_2 a_3 : «$ki_world»), % 7.77/7.93 Or (Eq (v3 «$ki_local_world») True) % 7.77/7.93 (Or (Eq («$ki_accessible» «$ki_local_world» a) False) % 7.77/7.93 (Or (Eq (v4 «$ki_local_world») False) % 7.77/7.93 (Or (Eq («$ki_accessible» «$ki_local_world» a_1) False) % 7.77/7.93 (Or (Eq («$ki_accessible» a_1 a_2 → v3 a_2) True) % 7.77/7.93 (Or (Eq («$ki_accessible» a a_3) False) (Eq (Not (v4 a_3)) True)))))) % 7.77/7.93 Clause #621 (by clausification #[620]): ∀ (a a_1 a_2 a_3 : «$ki_world»), % 7.77/7.93 Or (Eq (v3 «$ki_local_world») True) % 7.77/7.93 (Or (Eq («$ki_accessible» «$ki_local_world» a) False) % 7.77/7.93 (Or (Eq (v4 «$ki_local_world») False) % 7.77/7.93 (Or (Eq («$ki_accessible» «$ki_local_world» a_1) False) % 7.77/7.93 (Or (Eq («$ki_accessible» a a_2) False) % 7.77/7.95 (Or (Eq (Not (v4 a_2)) True) (Or (Eq («$ki_accessible» a_1 a_3) False) (Eq (v3 a_3) True))))))) % 7.77/7.95 Clause #622 (by clausification #[621]): ∀ (a a_1 a_2 a_3 : «$ki_world»), % 7.77/7.95 Or (Eq (v3 «$ki_local_world») True) % 7.77/7.95 (Or (Eq («$ki_accessible» «$ki_local_world» a) False) % 7.77/7.95 (Or (Eq (v4 «$ki_local_world») False) % 7.77/7.95 (Or (Eq («$ki_accessible» «$ki_local_world» a_1) False) % 7.77/7.95 (Or (Eq («$ki_accessible» a a_2) False) % 7.77/7.95 (Or (Eq («$ki_accessible» a_1 a_3) False) (Or (Eq (v3 a_3) True) (Eq (v4 a_2) False))))))) % 7.77/7.95 Clause #624 (by superposition #[622, 55]): ∀ (a a_1 a_2 : «$ki_world»), % 7.77/7.95 Or (Eq (v3 «$ki_local_world») True) % 7.77/7.95 (Or (Eq (v4 «$ki_local_world») False) % 7.77/7.95 (Or (Eq («$ki_accessible» «$ki_local_world» a) False) % 7.77/7.95 (Or (Eq («$ki_accessible» «$ki_local_world» a_1) False) % 7.77/7.95 (Or (Eq («$ki_accessible» a a_2) False) (Or (Eq (v3 a_2) True) (Or (Eq (v4 a_1) False) (Eq False True))))))) % 7.77/7.95 Clause #629 (by clausification #[387]): ∀ (a a_1 : «$ki_world»), % 7.77/7.95 Or (Eq (v1 «$ki_local_world») False) % 7.77/7.95 (Or (Eq (v3 «$ki_local_world») False) % 7.77/7.95 (Or (Eq («$ki_accessible» «$ki_local_world» a) False) % 7.77/7.95 (Or (Eq (v3 a) False) (Or (Eq («$ki_accessible» «$ki_local_world» a_1) False) (Eq (v4 a_1) True))))) % 7.77/7.95 Clause #630 (by clausification #[41]): Or % 7.77/7.95 (Eq % 7.77/7.95 (Or (Or (Not (v2 «$ki_local_world»)) (Not (v3 «$ki_local_world»))) % 7.77/7.95 (∀ (W : «$ki_world»), «$ki_accessible» «$ki_local_world» W → ∀ (W0 : «$ki_world»), «$ki_accessible» W W0 → v1 W0)) % 7.77/7.95 True) % 7.77/7.95 (Eq (∀ (W : «$ki_world»), «$ki_accessible» «$ki_local_world» W → ∀ (W0 : «$ki_world»), «$ki_accessible» W W0 → v4 W0) % 7.77/7.95 True) % 7.77/7.95 Clause #631 (by clausification #[630]): Or % 7.77/7.95 (Eq (∀ (W : «$ki_world»), «$ki_accessible» «$ki_local_world» W → ∀ (W0 : «$ki_world»), «$ki_accessible» W W0 → v4 W0) % 7.77/7.95 True) % 7.77/7.95 (Or (Eq (Or (Not (v2 «$ki_local_world»)) (Not (v3 «$ki_local_world»))) True) % 7.77/7.95 (Eq % 7.77/7.95 (∀ (W : «$ki_world»), «$ki_accessible» «$ki_local_world» W → ∀ (W0 : «$ki_world»), «$ki_accessible» W W0 → v1 W0) % 7.77/7.95 True)) % 7.77/7.95 Clause #632 (by clausification #[631]): ∀ (a : «$ki_world»), % 7.77/7.95 Or (Eq (Or (Not (v2 «$ki_local_world»)) (Not (v3 «$ki_local_world»))) True) % 7.77/7.95 (Or % 7.77/7.95 (Eq % 7.77/7.95 (∀ (W : «$ki_world»), % 7.77/7.95 «$ki_accessible» «$ki_local_world» W → ∀ (W0 : «$ki_world»), «$ki_accessible» W W0 → v1 W0) % 7.77/7.95 True) % 7.77/7.95 (Eq («$ki_accessible» «$ki_local_world» a → ∀ (W0 : «$ki_world»), «$ki_accessible» a W0 → v4 W0) True)) % 7.77/7.95 Clause #633 (by clausification #[632]): ∀ (a : «$ki_world»), % 7.77/7.95 Or % 7.77/7.95 (Eq % 7.77/7.95 (∀ (W : «$ki_world»), «$ki_accessible» «$ki_local_world» W → ∀ (W0 : «$ki_world»), «$ki_accessible» W W0 → v1 W0) % 7.77/7.95 True) % 7.77/7.95 (Or (Eq («$ki_accessible» «$ki_local_world» a → ∀ (W0 : «$ki_world»), «$ki_accessible» a W0 → v4 W0) True) % 7.77/7.95 (Or (Eq (Not (v2 «$ki_local_world»)) True) (Eq (Not (v3 «$ki_local_world»)) True))) % 7.77/7.95 Clause #634 (by clausification #[633]): ∀ (a a_1 : «$ki_world»), % 7.77/7.95 Or (Eq («$ki_accessible» «$ki_local_world» a → ∀ (W0 : «$ki_world»), «$ki_accessible» a W0 → v4 W0) True) % 7.77/7.95 (Or (Eq (Not (v2 «$ki_local_world»)) True) % 7.77/7.95 (Or (Eq (Not (v3 «$ki_local_world»)) True) % 7.77/7.95 (Eq («$ki_accessible» «$ki_local_world» a_1 → ∀ (W0 : «$ki_world»), «$ki_accessible» a_1 W0 → v1 W0) True))) % 7.77/7.95 Clause #635 (by clausification #[634]): ∀ (a a_1 : «$ki_world»), % 7.77/7.95 Or (Eq (Not (v2 «$ki_local_world»)) True) % 7.77/7.95 (Or (Eq (Not (v3 «$ki_local_world»)) True) % 7.77/7.95 (Or (Eq («$ki_accessible» «$ki_local_world» a → ∀ (W0 : «$ki_world»), «$ki_accessible» a W0 → v1 W0) True) % 7.77/7.95 (Or (Eq («$ki_accessible» «$ki_local_world» a_1) False) % 7.77/7.95 (Eq (∀ (W0 : «$ki_world»), «$ki_accessible» a_1 W0 → v4 W0) True)))) % 7.77/7.95 Clause #636 (by clausification #[635]): ∀ (a a_1 : «$ki_world»), % 7.77/7.95 Or (Eq (Not (v3 «$ki_local_world»)) True) % 7.77/7.95 (Or (Eq («$ki_accessible» «$ki_local_world» a → ∀ (W0 : «$ki_world»), «$ki_accessible» a W0 → v1 W0) True) % 7.80/7.97 (Or (Eq («$ki_accessible» «$ki_local_world» a_1) False) % 7.80/7.97 (Or (Eq (∀ (W0 : «$ki_world»), «$ki_accessible» a_1 W0 → v4 W0) True) (Eq (v2 «$ki_local_world») False)))) % 7.80/7.97 Clause #637 (by clausification #[636]): ∀ (a a_1 : «$ki_world»), % 7.80/7.97 Or (Eq («$ki_accessible» «$ki_local_world» a → ∀ (W0 : «$ki_world»), «$ki_accessible» a W0 → v1 W0) True) % 7.80/7.97 (Or (Eq («$ki_accessible» «$ki_local_world» a_1) False) % 7.80/7.97 (Or (Eq (∀ (W0 : «$ki_world»), «$ki_accessible» a_1 W0 → v4 W0) True) % 7.80/7.97 (Or (Eq (v2 «$ki_local_world») False) (Eq (v3 «$ki_local_world») False)))) % 7.80/7.97 Clause #638 (by clausification #[637]): ∀ (a a_1 : «$ki_world»), % 7.80/7.97 Or (Eq («$ki_accessible» «$ki_local_world» a) False) % 7.80/7.97 (Or (Eq (∀ (W0 : «$ki_world»), «$ki_accessible» a W0 → v4 W0) True) % 7.80/7.97 (Or (Eq (v2 «$ki_local_world») False) % 7.80/7.97 (Or (Eq (v3 «$ki_local_world») False) % 7.80/7.97 (Or (Eq («$ki_accessible» «$ki_local_world» a_1) False) % 7.80/7.97 (Eq (∀ (W0 : «$ki_world»), «$ki_accessible» a_1 W0 → v1 W0) True))))) % 7.80/7.97 Clause #639 (by clausification #[638]): ∀ (a a_1 a_2 : «$ki_world»), % 7.80/7.97 Or (Eq («$ki_accessible» «$ki_local_world» a) False) % 7.80/7.97 (Or (Eq (v2 «$ki_local_world») False) % 7.80/7.97 (Or (Eq (v3 «$ki_local_world») False) % 7.80/7.97 (Or (Eq («$ki_accessible» «$ki_local_world» a_1) False) % 7.80/7.97 (Or (Eq (∀ (W0 : «$ki_world»), «$ki_accessible» a_1 W0 → v1 W0) True) % 7.80/7.97 (Eq («$ki_accessible» a a_2 → v4 a_2) True))))) % 7.80/7.97 Clause #640 (by clausification #[639]): ∀ (a a_1 a_2 a_3 : «$ki_world»), % 7.80/7.97 Or (Eq («$ki_accessible» «$ki_local_world» a) False) % 7.80/7.97 (Or (Eq (v2 «$ki_local_world») False) % 7.80/7.97 (Or (Eq (v3 «$ki_local_world») False) % 7.80/7.97 (Or (Eq («$ki_accessible» «$ki_local_world» a_1) False) % 7.80/7.97 (Or (Eq («$ki_accessible» a a_2 → v4 a_2) True) (Eq («$ki_accessible» a_1 a_3 → v1 a_3) True))))) % 7.80/7.97 Clause #641 (by clausification #[640]): ∀ (a a_1 a_2 a_3 : «$ki_world»), % 7.80/7.97 Or (Eq («$ki_accessible» «$ki_local_world» a) False) % 7.80/7.97 (Or (Eq (v2 «$ki_local_world») False) % 7.80/7.97 (Or (Eq (v3 «$ki_local_world») False) % 7.80/7.97 (Or (Eq («$ki_accessible» «$ki_local_world» a_1) False) % 7.80/7.97 (Or (Eq («$ki_accessible» a_1 a_2 → v1 a_2) True) % 7.80/7.97 (Or (Eq («$ki_accessible» a a_3) False) (Eq (v4 a_3) True)))))) % 7.80/7.97 Clause #642 (by clausification #[641]): ∀ (a a_1 a_2 a_3 : «$ki_world»), % 7.80/7.97 Or (Eq («$ki_accessible» «$ki_local_world» a) False) % 7.80/7.97 (Or (Eq (v2 «$ki_local_world») False) % 7.80/7.97 (Or (Eq (v3 «$ki_local_world») False) % 7.80/7.97 (Or (Eq («$ki_accessible» «$ki_local_world» a_1) False) % 7.80/7.97 (Or (Eq («$ki_accessible» a a_2) False) % 7.80/7.97 (Or (Eq (v4 a_2) True) (Or (Eq («$ki_accessible» a_1 a_3) False) (Eq (v1 a_3) True))))))) % 7.80/7.97 Clause #644 (by superposition #[642, 55]): ∀ (a a_1 a_2 : «$ki_world»), % 7.80/7.97 Or (Eq (v2 «$ki_local_world») False) % 7.80/7.97 (Or (Eq (v3 «$ki_local_world») False) % 7.80/7.97 (Or (Eq («$ki_accessible» «$ki_local_world» a) False) % 7.80/7.97 (Or (Eq («$ki_accessible» «$ki_local_world» a_1) False) % 7.80/7.97 (Or (Eq (v4 a_1) True) (Or (Eq («$ki_accessible» a a_2) False) (Or (Eq (v1 a_2) True) (Eq False True))))))) % 7.80/7.97 Clause #760 (by clausification #[604]): ∀ (a : «$ki_world»), % 7.80/7.97 Or (Eq (v4 «$ki_local_world») True) % 7.80/7.97 (Or (Eq (v2 «$ki_local_world») True) % 7.80/7.97 (Or (Eq (v1 «$ki_local_world») True) % 7.80/7.97 (Or (Eq (v1 «$ki_local_world») True) % 7.80/7.97 (Or (Eq (v2 «$ki_local_world») True) % 7.80/7.97 (Or (Eq («$ki_accessible» «$ki_local_world» a) False) (Eq (v1 a) True)))))) % 7.80/7.97 Clause #761 (by eliminate duplicate literals #[760]): ∀ (a : «$ki_world»), % 7.80/7.97 Or (Eq (v4 «$ki_local_world») True) % 7.80/7.97 (Or (Eq (v2 «$ki_local_world») True) % 7.80/7.97 (Or (Eq (v1 «$ki_local_world») True) (Or (Eq («$ki_accessible» «$ki_local_world» a) False) (Eq (v1 a) True)))) % 7.80/7.97 Clause #763 (by superposition #[761, 55]): Or (Eq (v4 «$ki_local_world») True) % 7.80/7.97 (Or (Eq (v2 «$ki_local_world») True) % 7.80/7.99 (Or (Eq (v1 «$ki_local_world») True) (Or (Eq (v1 «$ki_local_world») True) (Eq False True)))) % 7.80/7.99 Clause #764 (by clausification #[763]): Or (Eq (v4 «$ki_local_world») True) % 7.80/7.99 (Or (Eq (v2 «$ki_local_world») True) (Or (Eq (v1 «$ki_local_world») True) (Eq (v1 «$ki_local_world») True))) % 7.80/7.99 Clause #765 (by eliminate duplicate literals #[764]): Or (Eq (v4 «$ki_local_world») True) (Or (Eq (v2 «$ki_local_world») True) (Eq (v1 «$ki_local_world») True)) % 7.80/7.99 Clause #769 (by superposition #[765, 571]): ∀ (a a_1 : «$ki_world»), % 7.80/7.99 Or (Eq (v4 «$ki_local_world») True) % 7.80/7.99 (Or (Eq (v2 «$ki_local_world») True) % 7.80/7.99 (Or (Eq (v4 «$ki_local_world») True) % 7.80/7.99 (Or (Eq True False) % 7.80/7.99 (Or (Eq («$ki_accessible» «$ki_local_world» a) False) % 7.80/7.99 (Or (Eq (v1 a) False) (Or (Eq («$ki_accessible» «$ki_local_world» a_1) False) (Eq (v3 a_1) True))))))) % 7.80/7.99 Clause #855 (by clausification #[769]): ∀ (a a_1 : «$ki_world»), % 7.80/7.99 Or (Eq (v4 «$ki_local_world») True) % 7.80/7.99 (Or (Eq (v2 «$ki_local_world») True) % 7.80/7.99 (Or (Eq (v4 «$ki_local_world») True) % 7.80/7.99 (Or (Eq («$ki_accessible» «$ki_local_world» a) False) % 7.80/7.99 (Or (Eq (v1 a) False) (Or (Eq («$ki_accessible» «$ki_local_world» a_1) False) (Eq (v3 a_1) True)))))) % 7.80/7.99 Clause #856 (by eliminate duplicate literals #[855]): ∀ (a a_1 : «$ki_world»), % 7.80/7.99 Or (Eq (v4 «$ki_local_world») True) % 7.80/7.99 (Or (Eq (v2 «$ki_local_world») True) % 7.80/7.99 (Or (Eq («$ki_accessible» «$ki_local_world» a) False) % 7.80/7.99 (Or (Eq (v1 a) False) (Or (Eq («$ki_accessible» «$ki_local_world» a_1) False) (Eq (v3 a_1) True))))) % 7.80/7.99 Clause #858 (by superposition #[856, 55]): ∀ (a : «$ki_world»), % 7.80/7.99 Or (Eq (v4 «$ki_local_world») True) % 7.80/7.99 (Or (Eq (v2 «$ki_local_world») True) % 7.80/7.99 (Or (Eq (v1 «$ki_local_world») False) % 7.80/7.99 (Or (Eq («$ki_accessible» «$ki_local_world» a) False) (Or (Eq (v3 a) True) (Eq False True))))) % 7.80/7.99 Clause #859 (by clausification #[858]): ∀ (a : «$ki_world»), % 7.80/7.99 Or (Eq (v4 «$ki_local_world») True) % 7.80/7.99 (Or (Eq (v2 «$ki_local_world») True) % 7.80/7.99 (Or (Eq (v1 «$ki_local_world») False) (Or (Eq («$ki_accessible» «$ki_local_world» a) False) (Eq (v3 a) True)))) % 7.80/7.99 Clause #860 (by superposition #[859, 765]): ∀ (a : «$ki_world»), % 7.80/7.99 Or (Eq (v4 «$ki_local_world») True) % 7.80/7.99 (Or (Eq (v2 «$ki_local_world») True) % 7.80/7.99 (Or (Eq («$ki_accessible» «$ki_local_world» a) False) % 7.80/7.99 (Or (Eq (v3 a) True) % 7.80/7.99 (Or (Eq (v4 «$ki_local_world») True) (Or (Eq (v2 «$ki_local_world») True) (Eq False True)))))) % 7.80/7.99 Clause #861 (by clausification #[860]): ∀ (a : «$ki_world»), % 7.80/7.99 Or (Eq (v4 «$ki_local_world») True) % 7.80/7.99 (Or (Eq (v2 «$ki_local_world») True) % 7.80/7.99 (Or (Eq («$ki_accessible» «$ki_local_world» a) False) % 7.80/7.99 (Or (Eq (v3 a) True) (Or (Eq (v4 «$ki_local_world») True) (Eq (v2 «$ki_local_world») True))))) % 7.80/7.99 Clause #862 (by eliminate duplicate literals #[861]): ∀ (a : «$ki_world»), % 7.80/7.99 Or (Eq (v4 «$ki_local_world») True) % 7.80/7.99 (Or (Eq (v2 «$ki_local_world») True) (Or (Eq («$ki_accessible» «$ki_local_world» a) False) (Eq (v3 a) True))) % 7.80/7.99 Clause #864 (by superposition #[862, 55]): Or (Eq (v4 «$ki_local_world») True) % 7.80/7.99 (Or (Eq (v2 «$ki_local_world») True) (Or (Eq (v3 «$ki_local_world») True) (Eq False True))) % 7.80/7.99 Clause #865 (by clausification #[864]): Or (Eq (v4 «$ki_local_world») True) (Or (Eq (v2 «$ki_local_world») True) (Eq (v3 «$ki_local_world») True)) % 7.80/7.99 Clause #869 (by superposition #[865, 462]): ∀ (a a_1 : «$ki_world»), % 7.80/7.99 Or (Eq (v4 «$ki_local_world») True) % 7.80/7.99 (Or (Eq (v2 «$ki_local_world») True) % 7.80/7.99 (Or (Eq (v2 «$ki_local_world») True) % 7.80/7.99 (Or (Eq True False) % 7.80/7.99 (Or (Eq («$ki_accessible» «$ki_local_world» a) False) % 7.80/7.99 (Or (Eq (v1 a) False) (Or (Eq («$ki_accessible» «$ki_local_world» a_1) False) (Eq (v1 a_1) False))))))) % 7.80/7.99 Clause #900 (by clausification #[869]): ∀ (a a_1 : «$ki_world»), % 7.80/7.99 Or (Eq (v4 «$ki_local_world») True) % 7.80/7.99 (Or (Eq (v2 «$ki_local_world») True) % 7.80/7.99 (Or (Eq (v2 «$ki_local_world») True) % 7.80/7.99 (Or (Eq («$ki_accessible» «$ki_local_world» a) False) % 7.80/8.01 (Or (Eq (v1 a) False) (Or (Eq («$ki_accessible» «$ki_local_world» a_1) False) (Eq (v1 a_1) False)))))) % 7.80/8.01 Clause #901 (by eliminate duplicate literals #[900]): ∀ (a a_1 : «$ki_world»), % 7.80/8.01 Or (Eq (v4 «$ki_local_world») True) % 7.80/8.01 (Or (Eq (v2 «$ki_local_world») True) % 7.80/8.01 (Or (Eq («$ki_accessible» «$ki_local_world» a) False) % 7.80/8.01 (Or (Eq (v1 a) False) (Or (Eq («$ki_accessible» «$ki_local_world» a_1) False) (Eq (v1 a_1) False))))) % 7.80/8.01 Clause #903 (by superposition #[901, 55]): ∀ (a : «$ki_world»), % 7.80/8.01 Or (Eq (v4 «$ki_local_world») True) % 7.80/8.01 (Or (Eq (v2 «$ki_local_world») True) % 7.80/8.01 (Or (Eq (v1 «$ki_local_world») False) % 7.80/8.01 (Or (Eq («$ki_accessible» «$ki_local_world» a) False) (Or (Eq (v1 a) False) (Eq False True))))) % 7.80/8.01 Clause #907 (by clausification #[903]): ∀ (a : «$ki_world»), % 7.80/8.01 Or (Eq (v4 «$ki_local_world») True) % 7.80/8.01 (Or (Eq (v2 «$ki_local_world») True) % 7.80/8.01 (Or (Eq (v1 «$ki_local_world») False) (Or (Eq («$ki_accessible» «$ki_local_world» a) False) (Eq (v1 a) False)))) % 7.80/8.01 Clause #908 (by superposition #[907, 765]): ∀ (a : «$ki_world»), % 7.80/8.01 Or (Eq (v4 «$ki_local_world») True) % 7.80/8.01 (Or (Eq (v2 «$ki_local_world») True) % 7.80/8.01 (Or (Eq («$ki_accessible» «$ki_local_world» a) False) % 7.80/8.01 (Or (Eq (v1 a) False) % 7.80/8.01 (Or (Eq (v4 «$ki_local_world») True) (Or (Eq (v2 «$ki_local_world») True) (Eq False True)))))) % 7.80/8.01 Clause #909 (by clausification #[908]): ∀ (a : «$ki_world»), % 7.80/8.01 Or (Eq (v4 «$ki_local_world») True) % 7.80/8.01 (Or (Eq (v2 «$ki_local_world») True) % 7.80/8.01 (Or (Eq («$ki_accessible» «$ki_local_world» a) False) % 7.80/8.01 (Or (Eq (v1 a) False) (Or (Eq (v4 «$ki_local_world») True) (Eq (v2 «$ki_local_world») True))))) % 7.80/8.01 Clause #910 (by eliminate duplicate literals #[909]): ∀ (a : «$ki_world»), % 7.80/8.01 Or (Eq (v4 «$ki_local_world») True) % 7.80/8.01 (Or (Eq (v2 «$ki_local_world») True) (Or (Eq («$ki_accessible» «$ki_local_world» a) False) (Eq (v1 a) False))) % 7.80/8.01 Clause #912 (by superposition #[910, 55]): Or (Eq (v4 «$ki_local_world») True) % 7.80/8.01 (Or (Eq (v2 «$ki_local_world») True) (Or (Eq (v1 «$ki_local_world») False) (Eq False True))) % 7.80/8.01 Clause #913 (by clausification #[912]): Or (Eq (v4 «$ki_local_world») True) (Or (Eq (v2 «$ki_local_world») True) (Eq (v1 «$ki_local_world») False)) % 7.80/8.01 Clause #914 (by superposition #[913, 765]): Or (Eq (v4 «$ki_local_world») True) % 7.80/8.01 (Or (Eq (v2 «$ki_local_world») True) % 7.80/8.01 (Or (Eq (v4 «$ki_local_world») True) (Or (Eq (v2 «$ki_local_world») True) (Eq False True)))) % 7.80/8.01 Clause #915 (by clausification #[914]): Or (Eq (v4 «$ki_local_world») True) % 7.80/8.01 (Or (Eq (v2 «$ki_local_world») True) (Or (Eq (v4 «$ki_local_world») True) (Eq (v2 «$ki_local_world») True))) % 7.80/8.01 Clause #916 (by eliminate duplicate literals #[915]): Or (Eq (v4 «$ki_local_world») True) (Eq (v2 «$ki_local_world») True) % 7.80/8.01 Clause #963 (by clausification #[185]): ∀ (a a_1 a_2 : «$ki_world»), % 7.80/8.01 Or (Eq (v1 «$ki_local_world») True) % 7.80/8.01 (Or (Eq (v3 «$ki_local_world») True) % 7.80/8.01 (Or (Eq («$ki_accessible» «$ki_local_world» a) False) % 7.80/8.01 (Or (Eq («$ki_accessible» «$ki_local_world» a_1) False) % 7.80/8.01 (Or (Eq (v4 a_1) True) (Or (Eq («$ki_accessible» a a_2) False) (Eq (v3 a_2) True)))))) % 7.80/8.01 Clause #965 (by superposition #[963, 55]): ∀ (a a_1 : «$ki_world»), % 7.80/8.01 Or (Eq (v1 «$ki_local_world») True) % 7.80/8.01 (Or (Eq (v3 «$ki_local_world») True) % 7.80/8.01 (Or (Eq («$ki_accessible» «$ki_local_world» a) False) % 7.80/8.01 (Or (Eq (v4 a) True) % 7.80/8.01 (Or (Eq («$ki_accessible» «$ki_local_world» a_1) False) (Or (Eq (v3 a_1) True) (Eq False True)))))) % 7.80/8.01 Clause #967 (by clausification #[965]): ∀ (a a_1 : «$ki_world»), % 7.80/8.01 Or (Eq (v1 «$ki_local_world») True) % 7.80/8.01 (Or (Eq (v3 «$ki_local_world») True) % 7.80/8.01 (Or (Eq («$ki_accessible» «$ki_local_world» a) False) % 7.80/8.01 (Or (Eq (v4 a) True) (Or (Eq («$ki_accessible» «$ki_local_world» a_1) False) (Eq (v3 a_1) True))))) % 7.80/8.01 Clause #969 (by superposition #[967, 55]): ∀ (a : «$ki_world»), % 7.80/8.01 Or (Eq (v1 «$ki_local_world») True) % 7.80/8.01 (Or (Eq (v3 «$ki_local_world») True) % 7.80/8.01 (Or (Eq (v4 «$ki_local_world») True) % 7.86/8.03 (Or (Eq («$ki_accessible» «$ki_local_world» a) False) (Or (Eq (v3 a) True) (Eq False True))))) % 7.86/8.03 Clause #970 (by clausification #[969]): ∀ (a : «$ki_world»), % 7.86/8.03 Or (Eq (v1 «$ki_local_world») True) % 7.86/8.03 (Or (Eq (v3 «$ki_local_world») True) % 7.86/8.03 (Or (Eq (v4 «$ki_local_world») True) (Or (Eq («$ki_accessible» «$ki_local_world» a) False) (Eq (v3 a) True)))) % 7.86/8.03 Clause #972 (by superposition #[970, 55]): Or (Eq (v1 «$ki_local_world») True) % 7.86/8.03 (Or (Eq (v3 «$ki_local_world») True) % 7.86/8.03 (Or (Eq (v4 «$ki_local_world») True) (Or (Eq (v3 «$ki_local_world») True) (Eq False True)))) % 7.86/8.03 Clause #973 (by clausification #[972]): Or (Eq (v1 «$ki_local_world») True) % 7.86/8.03 (Or (Eq (v3 «$ki_local_world») True) (Or (Eq (v4 «$ki_local_world») True) (Eq (v3 «$ki_local_world») True))) % 7.86/8.03 Clause #974 (by eliminate duplicate literals #[973]): Or (Eq (v1 «$ki_local_world») True) (Or (Eq (v3 «$ki_local_world») True) (Eq (v4 «$ki_local_world») True)) % 7.86/8.03 Clause #1072 (by clausification #[345]): ∀ (a a_1 a_2 : «$ki_world»), % 7.86/8.03 Or (Eq (v1 «$ki_local_world») True) % 7.86/8.03 (Or (Eq (v4 «$ki_local_world») False) % 7.86/8.03 (Or (Eq («$ki_accessible» «$ki_local_world» a) False) % 7.86/8.03 (Or (Eq («$ki_accessible» «$ki_local_world» a_1) False) % 7.86/8.03 (Or (Eq («$ki_accessible» a a_2) False) (Or (Eq (v4 a_1) False) (Eq (v3 a_2) False)))))) % 7.86/8.03 Clause #1073 (by superposition #[1072, 916]): ∀ (a a_1 a_2 : «$ki_world»), % 7.86/8.03 Or (Eq (v1 «$ki_local_world») True) % 7.86/8.03 (Or (Eq («$ki_accessible» «$ki_local_world» a) False) % 7.86/8.03 (Or (Eq («$ki_accessible» «$ki_local_world» a_1) False) % 7.86/8.03 (Or (Eq («$ki_accessible» a a_2) False) % 7.86/8.03 (Or (Eq (v4 a_1) False) (Or (Eq (v3 a_2) False) (Or (Eq False True) (Eq (v2 «$ki_local_world») True))))))) % 7.86/8.03 Clause #1074 (by clausification #[1073]): ∀ (a a_1 a_2 : «$ki_world»), % 7.86/8.03 Or (Eq (v1 «$ki_local_world») True) % 7.86/8.03 (Or (Eq («$ki_accessible» «$ki_local_world» a) False) % 7.86/8.03 (Or (Eq («$ki_accessible» «$ki_local_world» a_1) False) % 7.86/8.03 (Or (Eq («$ki_accessible» a a_2) False) % 7.86/8.03 (Or (Eq (v4 a_1) False) (Or (Eq (v3 a_2) False) (Eq (v2 «$ki_local_world») True)))))) % 7.86/8.03 Clause #1076 (by superposition #[1074, 55]): ∀ (a a_1 : «$ki_world»), % 7.86/8.03 Or (Eq (v1 «$ki_local_world») True) % 7.86/8.03 (Or (Eq («$ki_accessible» «$ki_local_world» a) False) % 7.86/8.03 (Or (Eq («$ki_accessible» «$ki_local_world» a_1) False) % 7.86/8.03 (Or (Eq (v4 a) False) (Or (Eq (v3 a_1) False) (Or (Eq (v2 «$ki_local_world») True) (Eq False True)))))) % 7.86/8.03 Clause #1077 (by clausification #[1076]): ∀ (a a_1 : «$ki_world»), % 7.86/8.03 Or (Eq (v1 «$ki_local_world») True) % 7.86/8.03 (Or (Eq («$ki_accessible» «$ki_local_world» a) False) % 7.86/8.03 (Or (Eq («$ki_accessible» «$ki_local_world» a_1) False) % 7.86/8.03 (Or (Eq (v4 a) False) (Or (Eq (v3 a_1) False) (Eq (v2 «$ki_local_world») True))))) % 7.86/8.03 Clause #1079 (by superposition #[1077, 55]): ∀ (a : «$ki_world»), % 7.86/8.03 Or (Eq (v1 «$ki_local_world») True) % 7.86/8.03 (Or (Eq («$ki_accessible» «$ki_local_world» a) False) % 7.86/8.03 (Or (Eq (v4 «$ki_local_world») False) % 7.86/8.03 (Or (Eq (v3 a) False) (Or (Eq (v2 «$ki_local_world») True) (Eq False True))))) % 7.86/8.03 Clause #1080 (by clausification #[1079]): ∀ (a : «$ki_world»), % 7.86/8.03 Or (Eq (v1 «$ki_local_world») True) % 7.86/8.03 (Or (Eq («$ki_accessible» «$ki_local_world» a) False) % 7.86/8.03 (Or (Eq (v4 «$ki_local_world») False) (Or (Eq (v3 a) False) (Eq (v2 «$ki_local_world») True)))) % 7.86/8.03 Clause #1082 (by superposition #[1080, 55]): Or (Eq (v1 «$ki_local_world») True) % 7.86/8.03 (Or (Eq (v4 «$ki_local_world») False) % 7.86/8.03 (Or (Eq (v3 «$ki_local_world») False) (Or (Eq (v2 «$ki_local_world») True) (Eq False True)))) % 7.86/8.03 Clause #1086 (by clausification #[1082]): Or (Eq (v1 «$ki_local_world») True) % 7.86/8.03 (Or (Eq (v4 «$ki_local_world») False) (Or (Eq (v3 «$ki_local_world») False) (Eq (v2 «$ki_local_world») True))) % 7.86/8.03 Clause #1087 (by superposition #[1086, 916]): Or (Eq (v1 «$ki_local_world») True) % 7.86/8.03 (Or (Eq (v3 «$ki_local_world») False) % 7.86/8.03 (Or (Eq (v2 «$ki_local_world») True) (Or (Eq False True) (Eq (v2 «$ki_local_world») True)))) % 7.86/8.05 Clause #1088 (by clausification #[1087]): Or (Eq (v1 «$ki_local_world») True) % 7.86/8.05 (Or (Eq (v3 «$ki_local_world») False) (Or (Eq (v2 «$ki_local_world») True) (Eq (v2 «$ki_local_world») True))) % 7.86/8.05 Clause #1089 (by eliminate duplicate literals #[1088]): Or (Eq (v1 «$ki_local_world») True) (Or (Eq (v3 «$ki_local_world») False) (Eq (v2 «$ki_local_world») True)) % 7.86/8.05 Clause #1113 (by clausification #[624]): ∀ (a a_1 a_2 : «$ki_world»), % 7.86/8.05 Or (Eq (v3 «$ki_local_world») True) % 7.86/8.05 (Or (Eq (v4 «$ki_local_world») False) % 7.86/8.05 (Or (Eq («$ki_accessible» «$ki_local_world» a) False) % 7.86/8.05 (Or (Eq («$ki_accessible» «$ki_local_world» a_1) False) % 7.86/8.05 (Or (Eq («$ki_accessible» a a_2) False) (Or (Eq (v3 a_2) True) (Eq (v4 a_1) False)))))) % 7.86/8.05 Clause #1114 (by superposition #[1113, 916]): ∀ (a a_1 a_2 : «$ki_world»), % 7.86/8.05 Or (Eq (v3 «$ki_local_world») True) % 7.86/8.05 (Or (Eq («$ki_accessible» «$ki_local_world» a) False) % 7.86/8.05 (Or (Eq («$ki_accessible» «$ki_local_world» a_1) False) % 7.86/8.05 (Or (Eq («$ki_accessible» a a_2) False) % 7.86/8.05 (Or (Eq (v3 a_2) True) (Or (Eq (v4 a_1) False) (Or (Eq False True) (Eq (v2 «$ki_local_world») True))))))) % 7.86/8.05 Clause #1115 (by clausification #[1114]): ∀ (a a_1 a_2 : «$ki_world»), % 7.86/8.05 Or (Eq (v3 «$ki_local_world») True) % 7.86/8.05 (Or (Eq («$ki_accessible» «$ki_local_world» a) False) % 7.86/8.05 (Or (Eq («$ki_accessible» «$ki_local_world» a_1) False) % 7.86/8.05 (Or (Eq («$ki_accessible» a a_2) False) % 7.86/8.05 (Or (Eq (v3 a_2) True) (Or (Eq (v4 a_1) False) (Eq (v2 «$ki_local_world») True)))))) % 7.86/8.05 Clause #1117 (by superposition #[1115, 55]): ∀ (a a_1 : «$ki_world»), % 7.86/8.05 Or (Eq (v3 «$ki_local_world») True) % 7.86/8.05 (Or (Eq («$ki_accessible» «$ki_local_world» a) False) % 7.86/8.05 (Or (Eq («$ki_accessible» «$ki_local_world» a_1) False) % 7.86/8.05 (Or (Eq (v3 a_1) True) (Or (Eq (v4 a) False) (Or (Eq (v2 «$ki_local_world») True) (Eq False True)))))) % 7.86/8.05 Clause #1118 (by clausification #[1117]): ∀ (a a_1 : «$ki_world»), % 7.86/8.05 Or (Eq (v3 «$ki_local_world») True) % 7.86/8.05 (Or (Eq («$ki_accessible» «$ki_local_world» a) False) % 7.86/8.05 (Or (Eq («$ki_accessible» «$ki_local_world» a_1) False) % 7.86/8.05 (Or (Eq (v3 a_1) True) (Or (Eq (v4 a) False) (Eq (v2 «$ki_local_world») True))))) % 7.86/8.05 Clause #1120 (by superposition #[1118, 55]): ∀ (a : «$ki_world»), % 7.86/8.05 Or (Eq (v3 «$ki_local_world») True) % 7.86/8.05 (Or (Eq («$ki_accessible» «$ki_local_world» a) False) % 7.86/8.05 (Or (Eq (v3 a) True) % 7.86/8.05 (Or (Eq (v4 «$ki_local_world») False) (Or (Eq (v2 «$ki_local_world») True) (Eq False True))))) % 7.86/8.05 Clause #1123 (by clausification #[1120]): ∀ (a : «$ki_world»), % 7.86/8.05 Or (Eq (v3 «$ki_local_world») True) % 7.86/8.05 (Or (Eq («$ki_accessible» «$ki_local_world» a) False) % 7.86/8.05 (Or (Eq (v3 a) True) (Or (Eq (v4 «$ki_local_world») False) (Eq (v2 «$ki_local_world») True)))) % 7.86/8.05 Clause #1125 (by superposition #[1123, 55]): Or (Eq (v3 «$ki_local_world») True) % 7.86/8.05 (Or (Eq (v3 «$ki_local_world») True) % 7.86/8.05 (Or (Eq (v4 «$ki_local_world») False) (Or (Eq (v2 «$ki_local_world») True) (Eq False True)))) % 7.86/8.05 Clause #1126 (by clausification #[1125]): Or (Eq (v3 «$ki_local_world») True) % 7.86/8.05 (Or (Eq (v3 «$ki_local_world») True) (Or (Eq (v4 «$ki_local_world») False) (Eq (v2 «$ki_local_world») True))) % 7.86/8.05 Clause #1127 (by eliminate duplicate literals #[1126]): Or (Eq (v3 «$ki_local_world») True) (Or (Eq (v4 «$ki_local_world») False) (Eq (v2 «$ki_local_world») True)) % 7.86/8.05 Clause #1128 (by superposition #[1127, 916]): Or (Eq (v3 «$ki_local_world») True) % 7.86/8.05 (Or (Eq (v2 «$ki_local_world») True) (Or (Eq False True) (Eq (v2 «$ki_local_world») True))) % 7.86/8.05 Clause #1129 (by clausification #[1128]): Or (Eq (v3 «$ki_local_world») True) (Or (Eq (v2 «$ki_local_world») True) (Eq (v2 «$ki_local_world») True)) % 7.86/8.05 Clause #1130 (by eliminate duplicate literals #[1129]): Or (Eq (v3 «$ki_local_world») True) (Eq (v2 «$ki_local_world») True) % 7.86/8.05 Clause #1131 (by superposition #[1130, 462]): ∀ (a a_1 : «$ki_world»), % 7.86/8.05 Or (Eq (v2 «$ki_local_world») True) % 7.86/8.05 (Or (Eq (v2 «$ki_local_world») True) % 7.86/8.05 (Or (Eq True False) % 7.86/8.07 (Or (Eq («$ki_accessible» «$ki_local_world» a) False) % 7.86/8.07 (Or (Eq (v1 a) False) (Or (Eq («$ki_accessible» «$ki_local_world» a_1) False) (Eq (v1 a_1) False)))))) % 7.86/8.07 Clause #1141 (by superposition #[1130, 1089]): Or (Eq (v2 «$ki_local_world») True) % 7.86/8.07 (Or (Eq (v1 «$ki_local_world») True) (Or (Eq True False) (Eq (v2 «$ki_local_world») True))) % 7.86/8.07 Clause #1143 (by clausification #[1141]): Or (Eq (v2 «$ki_local_world») True) (Or (Eq (v1 «$ki_local_world») True) (Eq (v2 «$ki_local_world») True)) % 7.86/8.07 Clause #1144 (by eliminate duplicate literals #[1143]): Or (Eq (v2 «$ki_local_world») True) (Eq (v1 «$ki_local_world») True) % 7.86/8.07 Clause #1162 (by clausification #[1131]): ∀ (a a_1 : «$ki_world»), % 7.86/8.07 Or (Eq (v2 «$ki_local_world») True) % 7.86/8.07 (Or (Eq (v2 «$ki_local_world») True) % 7.86/8.07 (Or (Eq («$ki_accessible» «$ki_local_world» a) False) % 7.86/8.07 (Or (Eq (v1 a) False) (Or (Eq («$ki_accessible» «$ki_local_world» a_1) False) (Eq (v1 a_1) False))))) % 7.86/8.07 Clause #1163 (by eliminate duplicate literals #[1162]): ∀ (a a_1 : «$ki_world»), % 7.86/8.07 Or (Eq (v2 «$ki_local_world») True) % 7.86/8.07 (Or (Eq («$ki_accessible» «$ki_local_world» a) False) % 7.86/8.07 (Or (Eq (v1 a) False) (Or (Eq («$ki_accessible» «$ki_local_world» a_1) False) (Eq (v1 a_1) False)))) % 7.86/8.07 Clause #1165 (by superposition #[1163, 55]): ∀ (a : «$ki_world»), % 7.86/8.07 Or (Eq (v2 «$ki_local_world») True) % 7.86/8.07 (Or (Eq (v1 «$ki_local_world») False) % 7.86/8.07 (Or (Eq («$ki_accessible» «$ki_local_world» a) False) (Or (Eq (v1 a) False) (Eq False True)))) % 7.86/8.07 Clause #1166 (by clausification #[1165]): ∀ (a : «$ki_world»), % 7.86/8.07 Or (Eq (v2 «$ki_local_world») True) % 7.86/8.07 (Or (Eq (v1 «$ki_local_world») False) (Or (Eq («$ki_accessible» «$ki_local_world» a) False) (Eq (v1 a) False))) % 7.86/8.07 Clause #1167 (by superposition #[1166, 1144]): ∀ (a : «$ki_world»), % 7.86/8.07 Or (Eq (v2 «$ki_local_world») True) % 7.86/8.07 (Or (Eq («$ki_accessible» «$ki_local_world» a) False) % 7.86/8.07 (Or (Eq (v1 a) False) (Or (Eq (v2 «$ki_local_world») True) (Eq False True)))) % 7.86/8.07 Clause #1168 (by clausification #[1167]): ∀ (a : «$ki_world»), % 7.86/8.07 Or (Eq (v2 «$ki_local_world») True) % 7.86/8.07 (Or (Eq («$ki_accessible» «$ki_local_world» a) False) (Or (Eq (v1 a) False) (Eq (v2 «$ki_local_world») True))) % 7.86/8.07 Clause #1169 (by eliminate duplicate literals #[1168]): ∀ (a : «$ki_world»), % 7.86/8.07 Or (Eq (v2 «$ki_local_world») True) (Or (Eq («$ki_accessible» «$ki_local_world» a) False) (Eq (v1 a) False)) % 7.86/8.07 Clause #1171 (by superposition #[1169, 55]): Or (Eq (v2 «$ki_local_world») True) (Or (Eq (v1 «$ki_local_world») False) (Eq False True)) % 7.86/8.07 Clause #1172 (by clausification #[1171]): Or (Eq (v2 «$ki_local_world») True) (Eq (v1 «$ki_local_world») False) % 7.86/8.07 Clause #1173 (by superposition #[1172, 1144]): Or (Eq (v2 «$ki_local_world») True) (Or (Eq (v2 «$ki_local_world») True) (Eq False True)) % 7.86/8.07 Clause #1176 (by clausification #[1173]): Or (Eq (v2 «$ki_local_world») True) (Eq (v2 «$ki_local_world») True) % 7.86/8.07 Clause #1177 (by eliminate duplicate literals #[1176]): Eq (v2 «$ki_local_world») True % 7.86/8.07 Clause #1178 (by backward demodulation #[1177, 195]): ∀ (a a_1 : «$ki_world»), % 7.86/8.07 Or (Eq (v1 «$ki_local_world») True) % 7.86/8.07 (Or (Eq (v4 «$ki_local_world») False) % 7.86/8.07 (Or (Eq («$ki_accessible» «$ki_local_world» a) False) % 7.86/8.07 (Or (Eq True False) (Or (Eq («$ki_accessible» a a_1) False) (Eq (v2 a_1) False))))) % 7.86/8.07 Clause #1183 (by backward demodulation #[1177, 445]): ∀ (a a_1 : «$ki_world»), % 7.86/8.07 Or (Eq (v1 «$ki_local_world») False) % 7.86/8.07 (Or (Eq True False) % 7.86/8.07 (Or (Eq («$ki_accessible» «$ki_local_world» a) False) % 7.86/8.07 (Or (Eq (v3 a) True) (Or (Eq («$ki_accessible» «$ki_local_world» a_1) False) (Eq (v1 a_1) False))))) % 7.86/8.07 Clause #1185 (by backward demodulation #[1177, 461]): ∀ (a a_1 : «$ki_world»), % 7.86/8.07 Or (Eq (v1 «$ki_local_world») False) % 7.86/8.07 (Or (Eq True False) % 7.86/8.07 (Or (Eq («$ki_accessible» «$ki_local_world» a) False) % 7.86/8.07 (Or (Eq (v4 a) False) (Or (Eq («$ki_accessible» «$ki_local_world» a_1) False) (Eq (v1 a_1) False))))) % 7.86/8.07 Clause #1204 (by clausification #[1178]): ∀ (a a_1 : «$ki_world»), % 7.92/8.09 Or (Eq (v1 «$ki_local_world») True) % 7.92/8.09 (Or (Eq (v4 «$ki_local_world») False) % 7.92/8.09 (Or (Eq («$ki_accessible» «$ki_local_world» a) False) % 7.92/8.09 (Or (Eq («$ki_accessible» a a_1) False) (Eq (v2 a_1) False)))) % 7.92/8.09 Clause #1205 (by clausification #[1183]): ∀ (a a_1 : «$ki_world»), % 7.92/8.09 Or (Eq (v1 «$ki_local_world») False) % 7.92/8.09 (Or (Eq («$ki_accessible» «$ki_local_world» a) False) % 7.92/8.09 (Or (Eq (v3 a) True) (Or (Eq («$ki_accessible» «$ki_local_world» a_1) False) (Eq (v1 a_1) False)))) % 7.92/8.09 Clause #1222 (by clausification #[1185]): ∀ (a a_1 : «$ki_world»), % 7.92/8.09 Or (Eq (v1 «$ki_local_world») False) % 7.92/8.09 (Or (Eq («$ki_accessible» «$ki_local_world» a) False) % 7.92/8.09 (Or (Eq (v4 a) False) (Or (Eq («$ki_accessible» «$ki_local_world» a_1) False) (Eq (v1 a_1) False)))) % 7.92/8.09 Clause #1300 (by clausification #[644]): ∀ (a a_1 a_2 : «$ki_world»), % 7.92/8.09 Or (Eq (v2 «$ki_local_world») False) % 7.92/8.09 (Or (Eq (v3 «$ki_local_world») False) % 7.92/8.09 (Or (Eq («$ki_accessible» «$ki_local_world» a) False) % 7.92/8.09 (Or (Eq («$ki_accessible» «$ki_local_world» a_1) False) % 7.92/8.09 (Or (Eq (v4 a_1) True) (Or (Eq («$ki_accessible» a a_2) False) (Eq (v1 a_2) True)))))) % 7.92/8.09 Clause #1301 (by forward demodulation #[1300, 1177]): ∀ (a a_1 a_2 : «$ki_world»), % 7.92/8.09 Or (Eq True False) % 7.92/8.09 (Or (Eq (v3 «$ki_local_world») False) % 7.92/8.09 (Or (Eq («$ki_accessible» «$ki_local_world» a) False) % 7.92/8.09 (Or (Eq («$ki_accessible» «$ki_local_world» a_1) False) % 7.92/8.09 (Or (Eq (v4 a_1) True) (Or (Eq («$ki_accessible» a a_2) False) (Eq (v1 a_2) True)))))) % 7.92/8.09 Clause #1302 (by clausification #[1301]): ∀ (a a_1 a_2 : «$ki_world»), % 7.92/8.09 Or (Eq (v3 «$ki_local_world») False) % 7.92/8.09 (Or (Eq («$ki_accessible» «$ki_local_world» a) False) % 7.92/8.09 (Or (Eq («$ki_accessible» «$ki_local_world» a_1) False) % 7.92/8.09 (Or (Eq (v4 a_1) True) (Or (Eq («$ki_accessible» a a_2) False) (Eq (v1 a_2) True))))) % 7.92/8.09 Clause #1303 (by superposition #[1302, 974]): ∀ (a a_1 a_2 : «$ki_world»), % 7.92/8.09 Or (Eq («$ki_accessible» «$ki_local_world» a) False) % 7.92/8.09 (Or (Eq («$ki_accessible» «$ki_local_world» a_1) False) % 7.92/8.09 (Or (Eq (v4 a_1) True) % 7.92/8.09 (Or (Eq («$ki_accessible» a a_2) False) % 7.92/8.09 (Or (Eq (v1 a_2) True) % 7.92/8.09 (Or (Eq (v1 «$ki_local_world») True) (Or (Eq False True) (Eq (v4 «$ki_local_world») True))))))) % 7.92/8.09 Clause #1304 (by clausification #[1303]): ∀ (a a_1 a_2 : «$ki_world»), % 7.92/8.09 Or (Eq («$ki_accessible» «$ki_local_world» a) False) % 7.92/8.09 (Or (Eq («$ki_accessible» «$ki_local_world» a_1) False) % 7.92/8.09 (Or (Eq (v4 a_1) True) % 7.92/8.09 (Or (Eq («$ki_accessible» a a_2) False) % 7.92/8.09 (Or (Eq (v1 a_2) True) (Or (Eq (v1 «$ki_local_world») True) (Eq (v4 «$ki_local_world») True)))))) % 7.92/8.09 Clause #1306 (by superposition #[1304, 55]): ∀ (a a_1 : «$ki_world»), % 7.92/8.09 Or (Eq («$ki_accessible» «$ki_local_world» a) False) % 7.92/8.09 (Or (Eq (v4 a) True) % 7.92/8.09 (Or (Eq («$ki_accessible» «$ki_local_world» a_1) False) % 7.92/8.09 (Or (Eq (v1 a_1) True) % 7.92/8.09 (Or (Eq (v1 «$ki_local_world») True) (Or (Eq (v4 «$ki_local_world») True) (Eq False True)))))) % 7.92/8.09 Clause #1309 (by clausification #[1306]): ∀ (a a_1 : «$ki_world»), % 7.92/8.09 Or (Eq («$ki_accessible» «$ki_local_world» a) False) % 7.92/8.09 (Or (Eq (v4 a) True) % 7.92/8.09 (Or (Eq («$ki_accessible» «$ki_local_world» a_1) False) % 7.92/8.09 (Or (Eq (v1 a_1) True) (Or (Eq (v1 «$ki_local_world») True) (Eq (v4 «$ki_local_world») True))))) % 7.92/8.09 Clause #1311 (by superposition #[1309, 55]): ∀ (a : «$ki_world»), % 7.92/8.09 Or (Eq (v4 «$ki_local_world») True) % 7.92/8.09 (Or (Eq («$ki_accessible» «$ki_local_world» a) False) % 7.92/8.09 (Or (Eq (v1 a) True) (Or (Eq (v1 «$ki_local_world») True) (Or (Eq (v4 «$ki_local_world») True) (Eq False True))))) % 7.92/8.09 Clause #1312 (by clausification #[1311]): ∀ (a : «$ki_world»), % 7.92/8.09 Or (Eq (v4 «$ki_local_world») True) % 7.92/8.09 (Or (Eq («$ki_accessible» «$ki_local_world» a) False) % 7.92/8.09 (Or (Eq (v1 a) True) (Or (Eq (v1 «$ki_local_world») True) (Eq (v4 «$ki_local_world») True)))) % 7.92/8.09 Clause #1313 (by eliminate duplicate literals #[1312]): ∀ (a : «$ki_world»), % 7.92/8.09 Or (Eq (v4 «$ki_local_world») True) % 7.92/8.11 (Or (Eq («$ki_accessible» «$ki_local_world» a) False) (Or (Eq (v1 a) True) (Eq (v1 «$ki_local_world») True))) % 7.92/8.11 Clause #1315 (by superposition #[1313, 55]): Or (Eq (v4 «$ki_local_world») True) % 7.92/8.11 (Or (Eq (v1 «$ki_local_world») True) (Or (Eq (v1 «$ki_local_world») True) (Eq False True))) % 7.92/8.11 Clause #1316 (by clausification #[1315]): Or (Eq (v4 «$ki_local_world») True) (Or (Eq (v1 «$ki_local_world») True) (Eq (v1 «$ki_local_world») True)) % 7.92/8.11 Clause #1317 (by eliminate duplicate literals #[1316]): Or (Eq (v4 «$ki_local_world») True) (Eq (v1 «$ki_local_world») True) % 7.92/8.11 Clause #1320 (by superposition #[1317, 629]): ∀ (a a_1 : «$ki_world»), % 7.92/8.11 Or (Eq (v4 «$ki_local_world») True) % 7.92/8.11 (Or (Eq True False) % 7.92/8.11 (Or (Eq (v3 «$ki_local_world») False) % 7.92/8.11 (Or (Eq («$ki_accessible» «$ki_local_world» a) False) % 7.92/8.11 (Or (Eq (v3 a) False) (Or (Eq («$ki_accessible» «$ki_local_world» a_1) False) (Eq (v4 a_1) True)))))) % 7.92/8.11 Clause #1328 (by superposition #[1317, 1205]): ∀ (a a_1 : «$ki_world»), % 7.92/8.11 Or (Eq (v4 «$ki_local_world») True) % 7.92/8.11 (Or (Eq True False) % 7.92/8.11 (Or (Eq («$ki_accessible» «$ki_local_world» a) False) % 7.92/8.11 (Or (Eq (v3 a) True) (Or (Eq («$ki_accessible» «$ki_local_world» a_1) False) (Eq (v1 a_1) False))))) % 7.92/8.11 Clause #1339 (by clausification #[1328]): ∀ (a a_1 : «$ki_world»), % 7.92/8.11 Or (Eq (v4 «$ki_local_world») True) % 7.92/8.11 (Or (Eq («$ki_accessible» «$ki_local_world» a) False) % 7.92/8.11 (Or (Eq (v3 a) True) (Or (Eq («$ki_accessible» «$ki_local_world» a_1) False) (Eq (v1 a_1) False)))) % 7.92/8.11 Clause #1341 (by superposition #[1339, 55]): ∀ (a : «$ki_world»), % 7.92/8.11 Or (Eq (v4 «$ki_local_world») True) % 7.92/8.11 (Or (Eq (v3 «$ki_local_world») True) % 7.92/8.11 (Or (Eq («$ki_accessible» «$ki_local_world» a) False) (Or (Eq (v1 a) False) (Eq False True)))) % 7.92/8.11 Clause #1342 (by clausification #[1341]): ∀ (a : «$ki_world»), % 7.92/8.11 Or (Eq (v4 «$ki_local_world») True) % 7.92/8.11 (Or (Eq (v3 «$ki_local_world») True) (Or (Eq («$ki_accessible» «$ki_local_world» a) False) (Eq (v1 a) False))) % 7.92/8.11 Clause #1344 (by superposition #[1342, 55]): Or (Eq (v4 «$ki_local_world») True) % 7.92/8.11 (Or (Eq (v3 «$ki_local_world») True) (Or (Eq (v1 «$ki_local_world») False) (Eq False True))) % 7.92/8.11 Clause #1345 (by clausification #[1344]): Or (Eq (v4 «$ki_local_world») True) (Or (Eq (v3 «$ki_local_world») True) (Eq (v1 «$ki_local_world») False)) % 7.92/8.11 Clause #1346 (by superposition #[1345, 1317]): Or (Eq (v4 «$ki_local_world») True) % 7.92/8.11 (Or (Eq (v3 «$ki_local_world») True) (Or (Eq (v4 «$ki_local_world») True) (Eq False True))) % 7.92/8.11 Clause #1347 (by clausification #[1346]): Or (Eq (v4 «$ki_local_world») True) (Or (Eq (v3 «$ki_local_world») True) (Eq (v4 «$ki_local_world») True)) % 7.92/8.11 Clause #1348 (by eliminate duplicate literals #[1347]): Or (Eq (v4 «$ki_local_world») True) (Eq (v3 «$ki_local_world») True) % 7.92/8.11 Clause #1413 (by clausification #[1320]): ∀ (a a_1 : «$ki_world»), % 7.92/8.11 Or (Eq (v4 «$ki_local_world») True) % 7.92/8.11 (Or (Eq (v3 «$ki_local_world») False) % 7.92/8.11 (Or (Eq («$ki_accessible» «$ki_local_world» a) False) % 7.92/8.11 (Or (Eq (v3 a) False) (Or (Eq («$ki_accessible» «$ki_local_world» a_1) False) (Eq (v4 a_1) True))))) % 7.92/8.11 Clause #1414 (by superposition #[1413, 1348]): ∀ (a a_1 : «$ki_world»), % 7.92/8.11 Or (Eq (v4 «$ki_local_world») True) % 7.92/8.11 (Or (Eq («$ki_accessible» «$ki_local_world» a) False) % 7.92/8.11 (Or (Eq (v3 a) False) % 7.92/8.11 (Or (Eq («$ki_accessible» «$ki_local_world» a_1) False) % 7.92/8.11 (Or (Eq (v4 a_1) True) (Or (Eq (v4 «$ki_local_world») True) (Eq False True)))))) % 7.92/8.11 Clause #1415 (by clausification #[1414]): ∀ (a a_1 : «$ki_world»), % 7.92/8.11 Or (Eq (v4 «$ki_local_world») True) % 7.92/8.11 (Or (Eq («$ki_accessible» «$ki_local_world» a) False) % 7.92/8.11 (Or (Eq (v3 a) False) % 7.92/8.11 (Or (Eq («$ki_accessible» «$ki_local_world» a_1) False) % 7.92/8.11 (Or (Eq (v4 a_1) True) (Eq (v4 «$ki_local_world») True))))) % 7.92/8.11 Clause #1416 (by eliminate duplicate literals #[1415]): ∀ (a a_1 : «$ki_world»), % 7.92/8.11 Or (Eq (v4 «$ki_local_world») True) % 7.92/8.11 (Or (Eq («$ki_accessible» «$ki_local_world» a) False) % 7.92/8.11 (Or (Eq (v3 a) False) (Or (Eq («$ki_accessible» «$ki_local_world» a_1) False) (Eq (v4 a_1) True)))) % 7.92/8.13 Clause #1418 (by superposition #[1416, 55]): ∀ (a : «$ki_world»), % 7.92/8.13 Or (Eq (v4 «$ki_local_world») True) % 7.92/8.13 (Or (Eq (v3 «$ki_local_world») False) % 7.92/8.13 (Or (Eq («$ki_accessible» «$ki_local_world» a) False) (Or (Eq (v4 a) True) (Eq False True)))) % 7.92/8.13 Clause #1419 (by clausification #[1418]): ∀ (a : «$ki_world»), % 7.92/8.13 Or (Eq (v4 «$ki_local_world») True) % 7.92/8.13 (Or (Eq (v3 «$ki_local_world») False) (Or (Eq («$ki_accessible» «$ki_local_world» a) False) (Eq (v4 a) True))) % 7.92/8.13 Clause #1420 (by superposition #[1419, 1348]): ∀ (a : «$ki_world»), % 7.92/8.13 Or (Eq (v4 «$ki_local_world») True) % 7.92/8.13 (Or (Eq («$ki_accessible» «$ki_local_world» a) False) % 7.92/8.13 (Or (Eq (v4 a) True) (Or (Eq (v4 «$ki_local_world») True) (Eq False True)))) % 7.92/8.13 Clause #1422 (by clausification #[1420]): ∀ (a : «$ki_world»), % 7.92/8.13 Or (Eq (v4 «$ki_local_world») True) % 7.92/8.13 (Or (Eq («$ki_accessible» «$ki_local_world» a) False) (Or (Eq (v4 a) True) (Eq (v4 «$ki_local_world») True))) % 7.92/8.13 Clause #1423 (by eliminate duplicate literals #[1422]): ∀ (a : «$ki_world»), % 7.92/8.13 Or (Eq (v4 «$ki_local_world») True) (Or (Eq («$ki_accessible» «$ki_local_world» a) False) (Eq (v4 a) True)) % 7.92/8.13 Clause #1425 (by superposition #[1423, 55]): Or (Eq (v4 «$ki_local_world») True) (Or (Eq (v4 «$ki_local_world») True) (Eq False True)) % 7.92/8.13 Clause #1426 (by clausification #[1425]): Or (Eq (v4 «$ki_local_world») True) (Eq (v4 «$ki_local_world») True) % 7.92/8.13 Clause #1427 (by eliminate duplicate literals #[1426]): Eq (v4 «$ki_local_world») True % 7.92/8.13 Clause #1451 (by backward demodulation #[1427, 1204]): ∀ (a a_1 : «$ki_world»), % 7.92/8.13 Or (Eq (v1 «$ki_local_world») True) % 7.92/8.13 (Or (Eq True False) % 7.92/8.13 (Or (Eq («$ki_accessible» «$ki_local_world» a) False) % 7.92/8.13 (Or (Eq («$ki_accessible» a a_1) False) (Eq (v2 a_1) False)))) % 7.92/8.13 Clause #1470 (by clausification #[1451]): ∀ (a a_1 : «$ki_world»), % 7.92/8.13 Or (Eq (v1 «$ki_local_world») True) % 7.92/8.13 (Or (Eq («$ki_accessible» «$ki_local_world» a) False) (Or (Eq («$ki_accessible» a a_1) False) (Eq (v2 a_1) False))) % 7.92/8.13 Clause #1472 (by superposition #[1470, 55]): ∀ (a : «$ki_world»), % 7.92/8.13 Or (Eq (v1 «$ki_local_world») True) % 7.92/8.13 (Or (Eq («$ki_accessible» «$ki_local_world» a) False) (Or (Eq (v2 a) False) (Eq False True))) % 7.92/8.13 Clause #1473 (by clausification #[1472]): ∀ (a : «$ki_world»), % 7.92/8.13 Or (Eq (v1 «$ki_local_world») True) (Or (Eq («$ki_accessible» «$ki_local_world» a) False) (Eq (v2 a) False)) % 7.92/8.13 Clause #1475 (by superposition #[1473, 55]): Or (Eq (v1 «$ki_local_world») True) (Or (Eq (v2 «$ki_local_world») False) (Eq False True)) % 7.92/8.13 Clause #1476 (by clausification #[1475]): Or (Eq (v1 «$ki_local_world») True) (Eq (v2 «$ki_local_world») False) % 7.92/8.13 Clause #1477 (by forward demodulation #[1476, 1177]): Or (Eq (v1 «$ki_local_world») True) (Eq True False) % 7.92/8.13 Clause #1478 (by clausification #[1477]): Eq (v1 «$ki_local_world») True % 7.92/8.13 Clause #1508 (by backward demodulation #[1478, 1222]): ∀ (a a_1 : «$ki_world»), % 7.92/8.13 Or (Eq True False) % 7.92/8.13 (Or (Eq («$ki_accessible» «$ki_local_world» a) False) % 7.92/8.13 (Or (Eq (v4 a) False) (Or (Eq («$ki_accessible» «$ki_local_world» a_1) False) (Eq (v1 a_1) False)))) % 7.92/8.13 Clause #1547 (by clausification #[1508]): ∀ (a a_1 : «$ki_world»), % 7.92/8.13 Or (Eq («$ki_accessible» «$ki_local_world» a) False) % 7.92/8.13 (Or (Eq (v4 a) False) (Or (Eq («$ki_accessible» «$ki_local_world» a_1) False) (Eq (v1 a_1) False))) % 7.92/8.13 Clause #1549 (by superposition #[1547, 55]): ∀ (a : «$ki_world»), % 7.92/8.13 Or (Eq (v4 «$ki_local_world») False) % 7.92/8.13 (Or (Eq («$ki_accessible» «$ki_local_world» a) False) (Or (Eq (v1 a) False) (Eq False True))) % 7.92/8.13 Clause #1550 (by clausification #[1549]): ∀ (a : «$ki_world»), % 7.92/8.13 Or (Eq (v4 «$ki_local_world») False) (Or (Eq («$ki_accessible» «$ki_local_world» a) False) (Eq (v1 a) False)) % 7.92/8.13 Clause #1551 (by forward demodulation #[1550, 1427]): ∀ (a : «$ki_world»), Or (Eq True False) (Or (Eq («$ki_accessible» «$ki_local_world» a) False) (Eq (v1 a) False)) % 7.92/8.13 Clause #1552 (by clausification #[1551]): ∀ (a : «$ki_world»), Or (Eq («$ki_accessible» «$ki_local_world» a) False) (Eq (v1 a) False) % 7.92/8.14 Clause #1554 (by superposition #[1552, 55]): Or (Eq (v1 «$ki_local_world») False) (Eq False True) % 7.92/8.14 Clause #1555 (by clausification #[1554]): Eq (v1 «$ki_local_world») False % 7.92/8.14 Clause #1556 (by superposition #[1555, 1478]): Eq False True % 7.92/8.14 Clause #1557 (by clausification #[1556]): False % 7.92/8.14 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------