%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : LCL950_17 : TPTP v9.3.1. Released v8.2.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n026.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8046.5625MB % OS : Linux 6.8.0-71-generic % CPULimit : 300s % WCLimit : 300s % DateTime : Mon Sep 7 11:36:55 AM UTC 2026 % Result : Theorem 9.80s 10.03s % Output : Proof 10.47s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : LCL950_17 : TPTP v9.3.1. Released v8.2.0. % 0.00/0.05 % Command : duper %s % 0.11/0.36 % Computer : n026.cluster.edu % 0.11/0.36 % Model : x86_64 x86_64 % 0.11/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.11/0.36 % Memory : 8046.5625MB % 0.11/0.36 % OS : Linux 6.8.0-71-generic % 0.11/0.36 % CPULimit : 300 % 0.11/0.36 % WCLimit : 300 % 0.11/0.36 % DateTime : Sat Sep 5 17:19:26 UTC 2026 % 0.11/0.37 % CPUTime : % 9.80/10.03 SZS status Theorem for theBenchmark.p % 9.80/10.03 SZS output start Proof for theBenchmark.p % 9.80/10.03 Clause #0 (by assumption #[]): Eq (∀ (W V : «$ki_world»), «$ki_accessible» W V) True % 9.80/10.03 Clause #1 (by assumption #[]): Eq (∀ (W : «$ki_world») (X : Iota), «$ki_exists_in_world_$i» W X) True % 9.80/10.03 Clause #3 (by assumption #[]): Eq % 9.80/10.03 (∀ (W : «$ki_world»), % 9.80/10.03 «$ki_accessible» «$ki_local_world» W → % 9.80/10.03 ∀ (B : Iota), % 9.80/10.03 «$ki_exists_in_world_$i» W B → % 9.80/10.03 ∀ (W0 : «$ki_world»), % 9.80/10.03 «$ki_accessible» W W0 → % 9.80/10.03 ∀ (C : Iota), % 9.80/10.03 «$ki_exists_in_world_$i» W0 C → % 9.80/10.03 And % 9.80/10.03 (∀ (W1 : «$ki_world»), % 9.80/10.03 «$ki_accessible» W0 W1 → % 9.80/10.03 (∀ (W2 : «$ki_world»), «$ki_accessible» W1 W2 → intersect W2 B C) → % 9.80/10.03 Exists fun D => % 9.80/10.03 And % 9.80/10.03 (And («$ki_exists_in_world_$i» W1 D) % 9.80/10.03 (∀ (W2 : «$ki_world»), «$ki_accessible» W1 W2 → member W2 D B)) % 9.80/10.03 (∀ (W2 : «$ki_world»), «$ki_accessible» W1 W2 → member W2 D C)) % 9.80/10.03 (∀ (W1 : «$ki_world»), % 9.80/10.03 «$ki_accessible» W0 W1 → % 9.80/10.03 (Exists fun D => % 9.80/10.03 And % 9.80/10.03 (And («$ki_exists_in_world_$i» W1 D) % 9.80/10.03 (∀ (W2 : «$ki_world»), «$ki_accessible» W1 W2 → member W2 D B)) % 9.80/10.03 (∀ (W2 : «$ki_world»), «$ki_accessible» W1 W2 → member W2 D C)) → % 9.80/10.03 ∀ (W2 : «$ki_world»), «$ki_accessible» W1 W2 → intersect W2 B C)) % 9.80/10.03 True % 9.80/10.03 Clause #4 (by assumption #[]): Eq % 9.80/10.03 (∀ (W : «$ki_world»), % 9.80/10.03 «$ki_accessible» «$ki_local_world» W → % 9.80/10.03 ∀ (B : Iota), % 9.80/10.03 «$ki_exists_in_world_$i» W B → % 9.80/10.03 ∀ (W0 : «$ki_world»), % 9.80/10.03 «$ki_accessible» W W0 → % 9.80/10.03 ∀ (C : Iota), % 9.80/10.03 «$ki_exists_in_world_$i» W0 C → % 9.80/10.03 ∀ (W1 : «$ki_world»), % 9.80/10.03 «$ki_accessible» W0 W1 → % 9.80/10.03 (∀ (W2 : «$ki_world»), «$ki_accessible» W1 W2 → intersect W2 B C) → % 9.80/10.03 ∀ (W2 : «$ki_world»), «$ki_accessible» W1 W2 → intersect W2 C B) % 9.80/10.03 True % 9.80/10.03 Clause #5 (by assumption #[]): Eq % 9.80/10.03 (Not % 9.80/10.03 (∀ (W : «$ki_world»), % 9.80/10.03 «$ki_accessible» «$ki_local_world» W → % 9.80/10.03 ∀ (B : Iota), % 9.80/10.03 «$ki_exists_in_world_$i» W B → % 9.80/10.03 ∀ (W0 : «$ki_world»), % 9.80/10.03 «$ki_accessible» W W0 → % 9.80/10.03 ∀ (C : Iota), % 9.80/10.03 «$ki_exists_in_world_$i» W0 C → % 9.80/10.03 ∀ (W1 : «$ki_world»), % 9.80/10.03 «$ki_accessible» W0 W1 → % 9.80/10.03 ∀ (D : Iota), % 9.80/10.03 «$ki_exists_in_world_$i» W1 D → % 9.80/10.03 ∀ (W2 : «$ki_world»), % 9.80/10.03 «$ki_accessible» W1 W2 → % 9.80/10.03 And (∀ (W3 : «$ki_world»), «$ki_accessible» W2 W3 → member W3 B C) % 9.80/10.03 (∀ (W3 : «$ki_world»), «$ki_accessible» W2 W3 → member W3 B D) → % 9.80/10.03 ∀ (W3 : «$ki_world»), «$ki_accessible» W2 W3 → intersect W3 C D)) % 9.80/10.03 True % 9.80/10.03 Clause #6 (by clausification #[1]): ∀ (a : «$ki_world»), Eq (∀ (X : Iota), «$ki_exists_in_world_$i» a X) True % 9.80/10.03 Clause #7 (by clausification #[6]): ∀ (a : «$ki_world») (a_1 : Iota), Eq («$ki_exists_in_world_$i» a a_1) True % 9.80/10.03 Clause #8 (by clausification #[0]): ∀ (a : «$ki_world»), Eq (∀ (V : «$ki_world»), «$ki_accessible» a V) True % 9.80/10.03 Clause #9 (by clausification #[8]): ∀ (a a_1 : «$ki_world»), Eq («$ki_accessible» a a_1) True % 9.80/10.03 Clause #13 (by clausification #[4]): ∀ (a : «$ki_world»), % 9.80/10.03 Eq % 9.80/10.03 («$ki_accessible» «$ki_local_world» a → % 9.80/10.03 ∀ (B : Iota), % 9.80/10.03 «$ki_exists_in_world_$i» a B → % 9.80/10.03 ∀ (W0 : «$ki_world»), % 9.80/10.03 «$ki_accessible» a W0 → % 9.80/10.03 ∀ (C : Iota), % 9.80/10.06 «$ki_exists_in_world_$i» W0 C → % 9.80/10.06 ∀ (W1 : «$ki_world»), % 9.80/10.06 «$ki_accessible» W0 W1 → % 9.80/10.06 (∀ (W2 : «$ki_world»), «$ki_accessible» W1 W2 → intersect W2 B C) → % 9.80/10.06 ∀ (W2 : «$ki_world»), «$ki_accessible» W1 W2 → intersect W2 C B) % 9.80/10.06 True % 9.80/10.06 Clause #14 (by clausification #[13]): ∀ (a : «$ki_world»), % 9.80/10.06 Or (Eq («$ki_accessible» «$ki_local_world» a) False) % 9.80/10.06 (Eq % 9.80/10.06 (∀ (B : Iota), % 9.80/10.06 «$ki_exists_in_world_$i» a B → % 9.80/10.06 ∀ (W0 : «$ki_world»), % 9.80/10.06 «$ki_accessible» a W0 → % 9.80/10.06 ∀ (C : Iota), % 9.80/10.06 «$ki_exists_in_world_$i» W0 C → % 9.80/10.06 ∀ (W1 : «$ki_world»), % 9.80/10.06 «$ki_accessible» W0 W1 → % 9.80/10.06 (∀ (W2 : «$ki_world»), «$ki_accessible» W1 W2 → intersect W2 B C) → % 9.80/10.06 ∀ (W2 : «$ki_world»), «$ki_accessible» W1 W2 → intersect W2 C B) % 9.80/10.06 True) % 9.80/10.06 Clause #15 (by clausification #[14]): ∀ (a : «$ki_world») (a_1 : Iota), % 9.80/10.06 Or (Eq («$ki_accessible» «$ki_local_world» a) False) % 9.80/10.06 (Eq % 9.80/10.06 («$ki_exists_in_world_$i» a a_1 → % 9.80/10.06 ∀ (W0 : «$ki_world»), % 9.80/10.06 «$ki_accessible» a W0 → % 9.80/10.06 ∀ (C : Iota), % 9.80/10.06 «$ki_exists_in_world_$i» W0 C → % 9.80/10.06 ∀ (W1 : «$ki_world»), % 9.80/10.06 «$ki_accessible» W0 W1 → % 9.80/10.06 (∀ (W2 : «$ki_world»), «$ki_accessible» W1 W2 → intersect W2 a_1 C) → % 9.80/10.06 ∀ (W2 : «$ki_world»), «$ki_accessible» W1 W2 → intersect W2 C a_1) % 9.80/10.06 True) % 9.80/10.06 Clause #16 (by clausification #[15]): ∀ (a : «$ki_world») (a_1 : Iota), % 9.80/10.06 Or (Eq («$ki_accessible» «$ki_local_world» a) False) % 9.80/10.06 (Or (Eq («$ki_exists_in_world_$i» a a_1) False) % 9.80/10.06 (Eq % 9.80/10.06 (∀ (W0 : «$ki_world»), % 9.80/10.06 «$ki_accessible» a W0 → % 9.80/10.06 ∀ (C : Iota), % 9.80/10.06 «$ki_exists_in_world_$i» W0 C → % 9.80/10.06 ∀ (W1 : «$ki_world»), % 9.80/10.06 «$ki_accessible» W0 W1 → % 9.80/10.06 (∀ (W2 : «$ki_world»), «$ki_accessible» W1 W2 → intersect W2 a_1 C) → % 9.80/10.06 ∀ (W2 : «$ki_world»), «$ki_accessible» W1 W2 → intersect W2 C a_1) % 9.80/10.06 True)) % 9.80/10.06 Clause #17 (by clausification #[16]): ∀ (a : «$ki_world») (a_1 : Iota) (a_2 : «$ki_world»), % 9.80/10.06 Or (Eq («$ki_accessible» «$ki_local_world» a) False) % 9.80/10.06 (Or (Eq («$ki_exists_in_world_$i» a a_1) False) % 9.80/10.06 (Eq % 9.80/10.06 («$ki_accessible» a a_2 → % 9.80/10.06 ∀ (C : Iota), % 9.80/10.06 «$ki_exists_in_world_$i» a_2 C → % 9.80/10.06 ∀ (W1 : «$ki_world»), % 9.80/10.06 «$ki_accessible» a_2 W1 → % 9.80/10.06 (∀ (W2 : «$ki_world»), «$ki_accessible» W1 W2 → intersect W2 a_1 C) → % 9.80/10.06 ∀ (W2 : «$ki_world»), «$ki_accessible» W1 W2 → intersect W2 C a_1) % 9.80/10.06 True)) % 9.80/10.06 Clause #18 (by clausification #[17]): ∀ (a : «$ki_world») (a_1 : Iota) (a_2 : «$ki_world»), % 9.80/10.06 Or (Eq («$ki_accessible» «$ki_local_world» a) False) % 9.80/10.06 (Or (Eq («$ki_exists_in_world_$i» a a_1) False) % 9.80/10.06 (Or (Eq («$ki_accessible» a a_2) False) % 9.80/10.06 (Eq % 9.80/10.06 (∀ (C : Iota), % 9.80/10.06 «$ki_exists_in_world_$i» a_2 C → % 9.80/10.06 ∀ (W1 : «$ki_world»), % 9.80/10.06 «$ki_accessible» a_2 W1 → % 9.80/10.06 (∀ (W2 : «$ki_world»), «$ki_accessible» W1 W2 → intersect W2 a_1 C) → % 9.80/10.06 ∀ (W2 : «$ki_world»), «$ki_accessible» W1 W2 → intersect W2 C a_1) % 9.80/10.06 True))) % 9.80/10.06 Clause #19 (by clausification #[18]): ∀ (a : «$ki_world») (a_1 : Iota) (a_2 : «$ki_world») (a_3 : Iota), % 9.80/10.06 Or (Eq («$ki_accessible» «$ki_local_world» a) False) % 9.80/10.06 (Or (Eq («$ki_exists_in_world_$i» a a_1) False) % 9.80/10.06 (Or (Eq («$ki_accessible» a a_2) False) % 9.80/10.06 (Eq % 9.80/10.06 («$ki_exists_in_world_$i» a_2 a_3 → % 9.80/10.06 ∀ (W1 : «$ki_world»), % 9.80/10.06 «$ki_accessible» a_2 W1 → % 9.80/10.06 (∀ (W2 : «$ki_world»), «$ki_accessible» W1 W2 → intersect W2 a_1 a_3) → % 9.80/10.10 ∀ (W2 : «$ki_world»), «$ki_accessible» W1 W2 → intersect W2 a_3 a_1) % 9.80/10.10 True))) % 9.80/10.10 Clause #20 (by clausification #[19]): ∀ (a : «$ki_world») (a_1 : Iota) (a_2 : «$ki_world») (a_3 : Iota), % 9.80/10.10 Or (Eq («$ki_accessible» «$ki_local_world» a) False) % 9.80/10.10 (Or (Eq («$ki_exists_in_world_$i» a a_1) False) % 9.80/10.10 (Or (Eq («$ki_accessible» a a_2) False) % 9.80/10.10 (Or (Eq («$ki_exists_in_world_$i» a_2 a_3) False) % 9.80/10.10 (Eq % 9.80/10.10 (∀ (W1 : «$ki_world»), % 9.80/10.10 «$ki_accessible» a_2 W1 → % 9.80/10.10 (∀ (W2 : «$ki_world»), «$ki_accessible» W1 W2 → intersect W2 a_1 a_3) → % 9.80/10.10 ∀ (W2 : «$ki_world»), «$ki_accessible» W1 W2 → intersect W2 a_3 a_1) % 9.80/10.10 True)))) % 9.80/10.10 Clause #21 (by clausification #[20]): ∀ (a : «$ki_world») (a_1 : Iota) (a_2 : «$ki_world») (a_3 : Iota) (a_4 : «$ki_world»), % 9.80/10.10 Or (Eq («$ki_accessible» «$ki_local_world» a) False) % 9.80/10.10 (Or (Eq («$ki_exists_in_world_$i» a a_1) False) % 9.80/10.10 (Or (Eq («$ki_accessible» a a_2) False) % 9.80/10.10 (Or (Eq («$ki_exists_in_world_$i» a_2 a_3) False) % 9.80/10.10 (Eq % 9.80/10.10 («$ki_accessible» a_2 a_4 → % 9.80/10.10 (∀ (W2 : «$ki_world»), «$ki_accessible» a_4 W2 → intersect W2 a_1 a_3) → % 9.80/10.10 ∀ (W2 : «$ki_world»), «$ki_accessible» a_4 W2 → intersect W2 a_3 a_1) % 9.80/10.10 True)))) % 9.80/10.10 Clause #22 (by clausification #[21]): ∀ (a : «$ki_world») (a_1 : Iota) (a_2 : «$ki_world») (a_3 : Iota) (a_4 : «$ki_world»), % 9.80/10.10 Or (Eq («$ki_accessible» «$ki_local_world» a) False) % 9.80/10.10 (Or (Eq («$ki_exists_in_world_$i» a a_1) False) % 9.80/10.10 (Or (Eq («$ki_accessible» a a_2) False) % 9.80/10.10 (Or (Eq («$ki_exists_in_world_$i» a_2 a_3) False) % 9.80/10.10 (Or (Eq («$ki_accessible» a_2 a_4) False) % 9.80/10.10 (Eq % 9.80/10.10 ((∀ (W2 : «$ki_world»), «$ki_accessible» a_4 W2 → intersect W2 a_1 a_3) → % 9.80/10.10 ∀ (W2 : «$ki_world»), «$ki_accessible» a_4 W2 → intersect W2 a_3 a_1) % 9.80/10.10 True))))) % 9.80/10.10 Clause #23 (by clausification #[22]): ∀ (a : «$ki_world») (a_1 : Iota) (a_2 : «$ki_world») (a_3 : Iota) (a_4 : «$ki_world»), % 9.80/10.10 Or (Eq («$ki_accessible» «$ki_local_world» a) False) % 9.80/10.10 (Or (Eq («$ki_exists_in_world_$i» a a_1) False) % 9.80/10.10 (Or (Eq («$ki_accessible» a a_2) False) % 9.80/10.10 (Or (Eq («$ki_exists_in_world_$i» a_2 a_3) False) % 9.80/10.10 (Or (Eq («$ki_accessible» a_2 a_4) False) % 9.80/10.10 (Or (Eq (∀ (W2 : «$ki_world»), «$ki_accessible» a_4 W2 → intersect W2 a_1 a_3) False) % 9.80/10.10 (Eq (∀ (W2 : «$ki_world»), «$ki_accessible» a_4 W2 → intersect W2 a_3 a_1) True)))))) % 9.80/10.10 Clause #24 (by clausification #[23]): ∀ (a : «$ki_world») (a_1 : Iota) (a_2 : «$ki_world») (a_3 : Iota) (a_4 a_5 : «$ki_world»), % 9.80/10.10 Or (Eq («$ki_accessible» «$ki_local_world» a) False) % 9.80/10.10 (Or (Eq («$ki_exists_in_world_$i» a a_1) False) % 9.80/10.10 (Or (Eq («$ki_accessible» a a_2) False) % 9.80/10.10 (Or (Eq («$ki_exists_in_world_$i» a_2 a_3) False) % 9.80/10.10 (Or (Eq («$ki_accessible» a_2 a_4) False) % 9.80/10.10 (Or (Eq (∀ (W2 : «$ki_world»), «$ki_accessible» a_4 W2 → intersect W2 a_3 a_1) True) % 9.80/10.10 (Eq (Not («$ki_accessible» a_4 (skS.0 1 a_4 a_1 a_3 a_5) → intersect (skS.0 1 a_4 a_1 a_3 a_5) a_1 a_3)) % 9.80/10.10 True)))))) % 9.80/10.10 Clause #25 (by clausification #[24]): ∀ (a : «$ki_world») (a_1 : Iota) (a_2 : «$ki_world») (a_3 : Iota) (a_4 a_5 a_6 : «$ki_world»), % 9.80/10.10 Or (Eq («$ki_accessible» «$ki_local_world» a) False) % 9.80/10.10 (Or (Eq («$ki_exists_in_world_$i» a a_1) False) % 9.80/10.10 (Or (Eq («$ki_accessible» a a_2) False) % 9.80/10.10 (Or (Eq («$ki_exists_in_world_$i» a_2 a_3) False) % 9.80/10.10 (Or (Eq («$ki_accessible» a_2 a_4) False) % 9.80/10.10 (Or % 9.80/10.10 (Eq (Not («$ki_accessible» a_4 (skS.0 1 a_4 a_1 a_3 a_5) → intersect (skS.0 1 a_4 a_1 a_3 a_5) a_1 a_3)) % 9.80/10.10 True) % 9.80/10.10 (Eq («$ki_accessible» a_4 a_6 → intersect a_6 a_3 a_1) True)))))) % 9.80/10.10 Clause #26 (by clausification #[25]): ∀ (a : «$ki_world») (a_1 : Iota) (a_2 : «$ki_world») (a_3 : Iota) (a_4 a_5 a_6 : «$ki_world»), % 9.90/10.14 Or (Eq («$ki_accessible» «$ki_local_world» a) False) % 9.90/10.14 (Or (Eq («$ki_exists_in_world_$i» a a_1) False) % 9.90/10.14 (Or (Eq («$ki_accessible» a a_2) False) % 9.90/10.14 (Or (Eq («$ki_exists_in_world_$i» a_2 a_3) False) % 9.90/10.14 (Or (Eq («$ki_accessible» a_2 a_4) False) % 9.90/10.14 (Or (Eq («$ki_accessible» a_4 a_5 → intersect a_5 a_3 a_1) True) % 9.90/10.14 (Eq («$ki_accessible» a_4 (skS.0 1 a_4 a_1 a_3 a_6) → intersect (skS.0 1 a_4 a_1 a_3 a_6) a_1 a_3) % 9.90/10.14 False)))))) % 9.90/10.14 Clause #27 (by clausification #[26]): ∀ (a : «$ki_world») (a_1 : Iota) (a_2 : «$ki_world») (a_3 : Iota) (a_4 a_5 a_6 : «$ki_world»), % 9.90/10.14 Or (Eq («$ki_accessible» «$ki_local_world» a) False) % 9.90/10.14 (Or (Eq («$ki_exists_in_world_$i» a a_1) False) % 9.90/10.14 (Or (Eq («$ki_accessible» a a_2) False) % 9.90/10.14 (Or (Eq («$ki_exists_in_world_$i» a_2 a_3) False) % 9.90/10.14 (Or (Eq («$ki_accessible» a_2 a_4) False) % 9.90/10.14 (Or % 9.90/10.14 (Eq («$ki_accessible» a_4 (skS.0 1 a_4 a_1 a_3 a_5) → intersect (skS.0 1 a_4 a_1 a_3 a_5) a_1 a_3) False) % 9.90/10.14 (Or (Eq («$ki_accessible» a_4 a_6) False) (Eq (intersect a_6 a_3 a_1) True))))))) % 9.90/10.14 Clause #29 (by clausification #[27]): ∀ (a : «$ki_world») (a_1 : Iota) (a_2 : «$ki_world») (a_3 : Iota) (a_4 a_5 a_6 : «$ki_world»), % 9.90/10.14 Or (Eq («$ki_accessible» «$ki_local_world» a) False) % 9.90/10.14 (Or (Eq («$ki_exists_in_world_$i» a a_1) False) % 9.90/10.14 (Or (Eq («$ki_accessible» a a_2) False) % 9.90/10.14 (Or (Eq («$ki_exists_in_world_$i» a_2 a_3) False) % 9.90/10.14 (Or (Eq («$ki_accessible» a_2 a_4) False) % 9.90/10.14 (Or (Eq («$ki_accessible» a_4 a_5) False) % 9.90/10.14 (Or (Eq (intersect a_5 a_3 a_1) True) (Eq (intersect (skS.0 1 a_4 a_1 a_3 a_6) a_1 a_3) False))))))) % 9.90/10.14 Clause #32 (by clausification #[5]): Eq % 9.90/10.14 (∀ (W : «$ki_world»), % 9.90/10.14 «$ki_accessible» «$ki_local_world» W → % 9.90/10.14 ∀ (B : Iota), % 9.90/10.14 «$ki_exists_in_world_$i» W B → % 9.90/10.14 ∀ (W0 : «$ki_world»), % 9.90/10.14 «$ki_accessible» W W0 → % 9.90/10.14 ∀ (C : Iota), % 9.90/10.14 «$ki_exists_in_world_$i» W0 C → % 9.90/10.14 ∀ (W1 : «$ki_world»), % 9.90/10.14 «$ki_accessible» W0 W1 → % 9.90/10.14 ∀ (D : Iota), % 9.90/10.14 «$ki_exists_in_world_$i» W1 D → % 9.90/10.14 ∀ (W2 : «$ki_world»), % 9.90/10.14 «$ki_accessible» W1 W2 → % 9.90/10.14 And (∀ (W3 : «$ki_world»), «$ki_accessible» W2 W3 → member W3 B C) % 9.90/10.14 (∀ (W3 : «$ki_world»), «$ki_accessible» W2 W3 → member W3 B D) → % 9.90/10.14 ∀ (W3 : «$ki_world»), «$ki_accessible» W2 W3 → intersect W3 C D) % 9.90/10.14 False % 9.90/10.14 Clause #33 (by clausification #[32]): ∀ (a : «$ki_world»), % 9.90/10.14 Eq % 9.90/10.14 (Not % 9.90/10.14 («$ki_accessible» «$ki_local_world» (skS.0 2 a) → % 9.90/10.14 ∀ (B : Iota), % 9.90/10.14 «$ki_exists_in_world_$i» (skS.0 2 a) B → % 9.90/10.14 ∀ (W0 : «$ki_world»), % 9.90/10.14 «$ki_accessible» (skS.0 2 a) W0 → % 9.90/10.14 ∀ (C : Iota), % 9.90/10.14 «$ki_exists_in_world_$i» W0 C → % 9.90/10.14 ∀ (W1 : «$ki_world»), % 9.90/10.14 «$ki_accessible» W0 W1 → % 9.90/10.14 ∀ (D : Iota), % 9.90/10.14 «$ki_exists_in_world_$i» W1 D → % 9.90/10.14 ∀ (W2 : «$ki_world»), % 9.90/10.14 «$ki_accessible» W1 W2 → % 9.90/10.14 And (∀ (W3 : «$ki_world»), «$ki_accessible» W2 W3 → member W3 B C) % 9.90/10.14 (∀ (W3 : «$ki_world»), «$ki_accessible» W2 W3 → member W3 B D) → % 9.90/10.14 ∀ (W3 : «$ki_world»), «$ki_accessible» W2 W3 → intersect W3 C D)) % 9.90/10.14 True % 9.90/10.14 Clause #34 (by clausification #[33]): ∀ (a : «$ki_world»), % 9.90/10.14 Eq % 9.90/10.14 («$ki_accessible» «$ki_local_world» (skS.0 2 a) → % 9.90/10.14 ∀ (B : Iota), % 9.90/10.14 «$ki_exists_in_world_$i» (skS.0 2 a) B → % 9.90/10.14 ∀ (W0 : «$ki_world»), % 9.90/10.14 «$ki_accessible» (skS.0 2 a) W0 → % 9.90/10.14 ∀ (C : Iota), % 9.90/10.14 «$ki_exists_in_world_$i» W0 C → % 9.90/10.16 ∀ (W1 : «$ki_world»), % 9.90/10.16 «$ki_accessible» W0 W1 → % 9.90/10.16 ∀ (D : Iota), % 9.90/10.16 «$ki_exists_in_world_$i» W1 D → % 9.90/10.16 ∀ (W2 : «$ki_world»), % 9.90/10.16 «$ki_accessible» W1 W2 → % 9.90/10.16 And (∀ (W3 : «$ki_world»), «$ki_accessible» W2 W3 → member W3 B C) % 9.90/10.16 (∀ (W3 : «$ki_world»), «$ki_accessible» W2 W3 → member W3 B D) → % 9.90/10.16 ∀ (W3 : «$ki_world»), «$ki_accessible» W2 W3 → intersect W3 C D) % 9.90/10.16 False % 9.90/10.16 Clause #36 (by clausification #[34]): ∀ (a : «$ki_world»), % 9.90/10.16 Eq % 9.90/10.16 (∀ (B : Iota), % 9.90/10.16 «$ki_exists_in_world_$i» (skS.0 2 a) B → % 9.90/10.16 ∀ (W0 : «$ki_world»), % 9.90/10.16 «$ki_accessible» (skS.0 2 a) W0 → % 9.90/10.16 ∀ (C : Iota), % 9.90/10.16 «$ki_exists_in_world_$i» W0 C → % 9.90/10.16 ∀ (W1 : «$ki_world»), % 9.90/10.16 «$ki_accessible» W0 W1 → % 9.90/10.16 ∀ (D : Iota), % 9.90/10.16 «$ki_exists_in_world_$i» W1 D → % 9.90/10.16 ∀ (W2 : «$ki_world»), % 9.90/10.16 «$ki_accessible» W1 W2 → % 9.90/10.16 And (∀ (W3 : «$ki_world»), «$ki_accessible» W2 W3 → member W3 B C) % 9.90/10.16 (∀ (W3 : «$ki_world»), «$ki_accessible» W2 W3 → member W3 B D) → % 9.90/10.16 ∀ (W3 : «$ki_world»), «$ki_accessible» W2 W3 → intersect W3 C D) % 9.90/10.16 False % 9.90/10.16 Clause #37 (by clausification #[3]): ∀ (a : «$ki_world»), % 9.90/10.16 Eq % 9.90/10.16 («$ki_accessible» «$ki_local_world» a → % 9.90/10.16 ∀ (B : Iota), % 9.90/10.16 «$ki_exists_in_world_$i» a B → % 9.90/10.16 ∀ (W0 : «$ki_world»), % 9.90/10.16 «$ki_accessible» a W0 → % 9.90/10.16 ∀ (C : Iota), % 9.90/10.16 «$ki_exists_in_world_$i» W0 C → % 9.90/10.16 And % 9.90/10.16 (∀ (W1 : «$ki_world»), % 9.90/10.16 «$ki_accessible» W0 W1 → % 9.90/10.16 (∀ (W2 : «$ki_world»), «$ki_accessible» W1 W2 → intersect W2 B C) → % 9.90/10.16 Exists fun D => % 9.90/10.16 And % 9.90/10.16 (And («$ki_exists_in_world_$i» W1 D) % 9.90/10.16 (∀ (W2 : «$ki_world»), «$ki_accessible» W1 W2 → member W2 D B)) % 9.90/10.16 (∀ (W2 : «$ki_world»), «$ki_accessible» W1 W2 → member W2 D C)) % 9.90/10.16 (∀ (W1 : «$ki_world»), % 9.90/10.16 «$ki_accessible» W0 W1 → % 9.90/10.16 (Exists fun D => % 9.90/10.16 And % 9.90/10.16 (And («$ki_exists_in_world_$i» W1 D) % 9.90/10.16 (∀ (W2 : «$ki_world»), «$ki_accessible» W1 W2 → member W2 D B)) % 9.90/10.16 (∀ (W2 : «$ki_world»), «$ki_accessible» W1 W2 → member W2 D C)) → % 9.90/10.16 ∀ (W2 : «$ki_world»), «$ki_accessible» W1 W2 → intersect W2 B C)) % 9.90/10.16 True % 9.90/10.16 Clause #38 (by clausification #[37]): ∀ (a : «$ki_world»), % 9.90/10.16 Or (Eq («$ki_accessible» «$ki_local_world» a) False) % 9.90/10.16 (Eq % 9.90/10.16 (∀ (B : Iota), % 9.90/10.16 «$ki_exists_in_world_$i» a B → % 9.90/10.16 ∀ (W0 : «$ki_world»), % 9.90/10.16 «$ki_accessible» a W0 → % 9.90/10.16 ∀ (C : Iota), % 9.90/10.16 «$ki_exists_in_world_$i» W0 C → % 9.90/10.16 And % 9.90/10.16 (∀ (W1 : «$ki_world»), % 9.90/10.16 «$ki_accessible» W0 W1 → % 9.90/10.16 (∀ (W2 : «$ki_world»), «$ki_accessible» W1 W2 → intersect W2 B C) → % 9.90/10.16 Exists fun D => % 9.90/10.16 And % 9.90/10.16 (And («$ki_exists_in_world_$i» W1 D) % 9.90/10.16 (∀ (W2 : «$ki_world»), «$ki_accessible» W1 W2 → member W2 D B)) % 9.90/10.16 (∀ (W2 : «$ki_world»), «$ki_accessible» W1 W2 → member W2 D C)) % 9.90/10.16 (∀ (W1 : «$ki_world»), % 9.90/10.16 «$ki_accessible» W0 W1 → % 9.90/10.16 (Exists fun D => % 9.90/10.19 And % 9.90/10.19 (And («$ki_exists_in_world_$i» W1 D) % 9.90/10.19 (∀ (W2 : «$ki_world»), «$ki_accessible» W1 W2 → member W2 D B)) % 9.90/10.19 (∀ (W2 : «$ki_world»), «$ki_accessible» W1 W2 → member W2 D C)) → % 9.90/10.19 ∀ (W2 : «$ki_world»), «$ki_accessible» W1 W2 → intersect W2 B C)) % 9.90/10.19 True) % 9.90/10.19 Clause #39 (by clausification #[38]): ∀ (a : «$ki_world») (a_1 : Iota), % 9.90/10.19 Or (Eq («$ki_accessible» «$ki_local_world» a) False) % 9.90/10.19 (Eq % 9.90/10.19 («$ki_exists_in_world_$i» a a_1 → % 9.90/10.19 ∀ (W0 : «$ki_world»), % 9.90/10.19 «$ki_accessible» a W0 → % 9.90/10.19 ∀ (C : Iota), % 9.90/10.19 «$ki_exists_in_world_$i» W0 C → % 9.90/10.19 And % 9.90/10.19 (∀ (W1 : «$ki_world»), % 9.90/10.19 «$ki_accessible» W0 W1 → % 9.90/10.19 (∀ (W2 : «$ki_world»), «$ki_accessible» W1 W2 → intersect W2 a_1 C) → % 9.90/10.19 Exists fun D => % 9.90/10.19 And % 9.90/10.19 (And («$ki_exists_in_world_$i» W1 D) % 9.90/10.19 (∀ (W2 : «$ki_world»), «$ki_accessible» W1 W2 → member W2 D a_1)) % 9.90/10.19 (∀ (W2 : «$ki_world»), «$ki_accessible» W1 W2 → member W2 D C)) % 9.90/10.19 (∀ (W1 : «$ki_world»), % 9.90/10.19 «$ki_accessible» W0 W1 → % 9.90/10.19 (Exists fun D => % 9.90/10.19 And % 9.90/10.19 (And («$ki_exists_in_world_$i» W1 D) % 9.90/10.19 (∀ (W2 : «$ki_world»), «$ki_accessible» W1 W2 → member W2 D a_1)) % 9.90/10.19 (∀ (W2 : «$ki_world»), «$ki_accessible» W1 W2 → member W2 D C)) → % 9.90/10.19 ∀ (W2 : «$ki_world»), «$ki_accessible» W1 W2 → intersect W2 a_1 C)) % 9.90/10.19 True) % 9.90/10.19 Clause #40 (by clausification #[39]): ∀ (a : «$ki_world») (a_1 : Iota), % 9.90/10.19 Or (Eq («$ki_accessible» «$ki_local_world» a) False) % 9.90/10.19 (Or (Eq («$ki_exists_in_world_$i» a a_1) False) % 9.90/10.19 (Eq % 9.90/10.19 (∀ (W0 : «$ki_world»), % 9.90/10.19 «$ki_accessible» a W0 → % 9.90/10.19 ∀ (C : Iota), % 9.90/10.19 «$ki_exists_in_world_$i» W0 C → % 9.90/10.19 And % 9.90/10.19 (∀ (W1 : «$ki_world»), % 9.90/10.19 «$ki_accessible» W0 W1 → % 9.90/10.19 (∀ (W2 : «$ki_world»), «$ki_accessible» W1 W2 → intersect W2 a_1 C) → % 9.90/10.19 Exists fun D => % 9.90/10.19 And % 9.90/10.19 (And («$ki_exists_in_world_$i» W1 D) % 9.90/10.19 (∀ (W2 : «$ki_world»), «$ki_accessible» W1 W2 → member W2 D a_1)) % 9.90/10.19 (∀ (W2 : «$ki_world»), «$ki_accessible» W1 W2 → member W2 D C)) % 9.90/10.19 (∀ (W1 : «$ki_world»), % 9.90/10.19 «$ki_accessible» W0 W1 → % 9.90/10.19 (Exists fun D => % 9.90/10.19 And % 9.90/10.19 (And («$ki_exists_in_world_$i» W1 D) % 9.90/10.19 (∀ (W2 : «$ki_world»), «$ki_accessible» W1 W2 → member W2 D a_1)) % 9.90/10.19 (∀ (W2 : «$ki_world»), «$ki_accessible» W1 W2 → member W2 D C)) → % 9.90/10.19 ∀ (W2 : «$ki_world»), «$ki_accessible» W1 W2 → intersect W2 a_1 C)) % 9.90/10.19 True)) % 9.90/10.19 Clause #41 (by clausification #[40]): ∀ (a : «$ki_world») (a_1 : Iota) (a_2 : «$ki_world»), % 9.90/10.19 Or (Eq («$ki_accessible» «$ki_local_world» a) False) % 9.90/10.19 (Or (Eq («$ki_exists_in_world_$i» a a_1) False) % 9.90/10.19 (Eq % 9.90/10.19 («$ki_accessible» a a_2 → % 9.90/10.19 ∀ (C : Iota), % 9.90/10.19 «$ki_exists_in_world_$i» a_2 C → % 9.90/10.19 And % 9.90/10.19 (∀ (W1 : «$ki_world»), % 9.90/10.19 «$ki_accessible» a_2 W1 → % 9.90/10.19 (∀ (W2 : «$ki_world»), «$ki_accessible» W1 W2 → intersect W2 a_1 C) → % 9.90/10.19 Exists fun D => % 9.90/10.19 And % 9.90/10.19 (And («$ki_exists_in_world_$i» W1 D) % 9.90/10.19 (∀ (W2 : «$ki_world»), «$ki_accessible» W1 W2 → member W2 D a_1)) % 9.97/10.22 (∀ (W2 : «$ki_world»), «$ki_accessible» W1 W2 → member W2 D C)) % 9.97/10.22 (∀ (W1 : «$ki_world»), % 9.97/10.22 «$ki_accessible» a_2 W1 → % 9.97/10.22 (Exists fun D => % 9.97/10.22 And % 9.97/10.22 (And («$ki_exists_in_world_$i» W1 D) % 9.97/10.22 (∀ (W2 : «$ki_world»), «$ki_accessible» W1 W2 → member W2 D a_1)) % 9.97/10.22 (∀ (W2 : «$ki_world»), «$ki_accessible» W1 W2 → member W2 D C)) → % 9.97/10.22 ∀ (W2 : «$ki_world»), «$ki_accessible» W1 W2 → intersect W2 a_1 C)) % 9.97/10.22 True)) % 9.97/10.22 Clause #42 (by clausification #[41]): ∀ (a : «$ki_world») (a_1 : Iota) (a_2 : «$ki_world»), % 9.97/10.22 Or (Eq («$ki_accessible» «$ki_local_world» a) False) % 9.97/10.22 (Or (Eq («$ki_exists_in_world_$i» a a_1) False) % 9.97/10.22 (Or (Eq («$ki_accessible» a a_2) False) % 9.97/10.22 (Eq % 9.97/10.22 (∀ (C : Iota), % 9.97/10.22 «$ki_exists_in_world_$i» a_2 C → % 9.97/10.22 And % 9.97/10.22 (∀ (W1 : «$ki_world»), % 9.97/10.22 «$ki_accessible» a_2 W1 → % 9.97/10.22 (∀ (W2 : «$ki_world»), «$ki_accessible» W1 W2 → intersect W2 a_1 C) → % 9.97/10.22 Exists fun D => % 9.97/10.22 And % 9.97/10.22 (And («$ki_exists_in_world_$i» W1 D) % 9.97/10.22 (∀ (W2 : «$ki_world»), «$ki_accessible» W1 W2 → member W2 D a_1)) % 9.97/10.22 (∀ (W2 : «$ki_world»), «$ki_accessible» W1 W2 → member W2 D C)) % 9.97/10.22 (∀ (W1 : «$ki_world»), % 9.97/10.22 «$ki_accessible» a_2 W1 → % 9.97/10.22 (Exists fun D => % 9.97/10.22 And % 9.97/10.22 (And («$ki_exists_in_world_$i» W1 D) % 9.97/10.22 (∀ (W2 : «$ki_world»), «$ki_accessible» W1 W2 → member W2 D a_1)) % 9.97/10.22 (∀ (W2 : «$ki_world»), «$ki_accessible» W1 W2 → member W2 D C)) → % 9.97/10.22 ∀ (W2 : «$ki_world»), «$ki_accessible» W1 W2 → intersect W2 a_1 C)) % 9.97/10.22 True))) % 9.97/10.22 Clause #43 (by clausification #[42]): ∀ (a : «$ki_world») (a_1 : Iota) (a_2 : «$ki_world») (a_3 : Iota), % 9.97/10.22 Or (Eq («$ki_accessible» «$ki_local_world» a) False) % 9.97/10.22 (Or (Eq («$ki_exists_in_world_$i» a a_1) False) % 9.97/10.22 (Or (Eq («$ki_accessible» a a_2) False) % 9.97/10.22 (Eq % 9.97/10.22 («$ki_exists_in_world_$i» a_2 a_3 → % 9.97/10.22 And % 9.97/10.22 (∀ (W1 : «$ki_world»), % 9.97/10.22 «$ki_accessible» a_2 W1 → % 9.97/10.22 (∀ (W2 : «$ki_world»), «$ki_accessible» W1 W2 → intersect W2 a_1 a_3) → % 9.97/10.22 Exists fun D => % 9.97/10.22 And % 9.97/10.22 (And («$ki_exists_in_world_$i» W1 D) % 9.97/10.22 (∀ (W2 : «$ki_world»), «$ki_accessible» W1 W2 → member W2 D a_1)) % 9.97/10.22 (∀ (W2 : «$ki_world»), «$ki_accessible» W1 W2 → member W2 D a_3)) % 9.97/10.22 (∀ (W1 : «$ki_world»), % 9.97/10.22 «$ki_accessible» a_2 W1 → % 9.97/10.22 (Exists fun D => % 9.97/10.22 And % 9.97/10.22 (And («$ki_exists_in_world_$i» W1 D) % 9.97/10.22 (∀ (W2 : «$ki_world»), «$ki_accessible» W1 W2 → member W2 D a_1)) % 9.97/10.22 (∀ (W2 : «$ki_world»), «$ki_accessible» W1 W2 → member W2 D a_3)) → % 9.97/10.22 ∀ (W2 : «$ki_world»), «$ki_accessible» W1 W2 → intersect W2 a_1 a_3)) % 9.97/10.22 True))) % 9.97/10.22 Clause #44 (by clausification #[43]): ∀ (a : «$ki_world») (a_1 : Iota) (a_2 : «$ki_world») (a_3 : Iota), % 9.97/10.22 Or (Eq («$ki_accessible» «$ki_local_world» a) False) % 9.97/10.22 (Or (Eq («$ki_exists_in_world_$i» a a_1) False) % 9.97/10.22 (Or (Eq («$ki_accessible» a a_2) False) % 9.97/10.22 (Or (Eq («$ki_exists_in_world_$i» a_2 a_3) False) % 9.97/10.22 (Eq % 9.97/10.22 (And % 9.97/10.22 (∀ (W1 : «$ki_world»), % 9.97/10.22 «$ki_accessible» a_2 W1 → % 9.97/10.22 (∀ (W2 : «$ki_world»), «$ki_accessible» W1 W2 → intersect W2 a_1 a_3) → % 9.97/10.22 Exists fun D => % 9.97/10.22 And % 9.97/10.22 (And («$ki_exists_in_world_$i» W1 D) % 9.97/10.25 (∀ (W2 : «$ki_world»), «$ki_accessible» W1 W2 → member W2 D a_1)) % 9.97/10.25 (∀ (W2 : «$ki_world»), «$ki_accessible» W1 W2 → member W2 D a_3)) % 9.97/10.25 (∀ (W1 : «$ki_world»), % 9.97/10.25 «$ki_accessible» a_2 W1 → % 9.97/10.25 (Exists fun D => % 9.97/10.25 And % 9.97/10.25 (And («$ki_exists_in_world_$i» W1 D) % 9.97/10.25 (∀ (W2 : «$ki_world»), «$ki_accessible» W1 W2 → member W2 D a_1)) % 9.97/10.25 (∀ (W2 : «$ki_world»), «$ki_accessible» W1 W2 → member W2 D a_3)) → % 9.97/10.25 ∀ (W2 : «$ki_world»), «$ki_accessible» W1 W2 → intersect W2 a_1 a_3)) % 9.97/10.25 True)))) % 9.97/10.25 Clause #45 (by clausification #[44]): ∀ (a : «$ki_world») (a_1 : Iota) (a_2 : «$ki_world») (a_3 : Iota), % 9.97/10.25 Or (Eq («$ki_accessible» «$ki_local_world» a) False) % 9.97/10.25 (Or (Eq («$ki_exists_in_world_$i» a a_1) False) % 9.97/10.25 (Or (Eq («$ki_accessible» a a_2) False) % 9.97/10.25 (Or (Eq («$ki_exists_in_world_$i» a_2 a_3) False) % 9.97/10.25 (Eq % 9.97/10.25 (∀ (W1 : «$ki_world»), % 9.97/10.25 «$ki_accessible» a_2 W1 → % 9.97/10.25 (Exists fun D => % 9.97/10.25 And % 9.97/10.25 (And («$ki_exists_in_world_$i» W1 D) % 9.97/10.25 (∀ (W2 : «$ki_world»), «$ki_accessible» W1 W2 → member W2 D a_1)) % 9.97/10.25 (∀ (W2 : «$ki_world»), «$ki_accessible» W1 W2 → member W2 D a_3)) → % 9.97/10.25 ∀ (W2 : «$ki_world»), «$ki_accessible» W1 W2 → intersect W2 a_1 a_3) % 9.97/10.25 True)))) % 9.97/10.25 Clause #47 (by clausification #[45]): ∀ (a : «$ki_world») (a_1 : Iota) (a_2 : «$ki_world») (a_3 : Iota) (a_4 : «$ki_world»), % 9.97/10.25 Or (Eq («$ki_accessible» «$ki_local_world» a) False) % 9.97/10.25 (Or (Eq («$ki_exists_in_world_$i» a a_1) False) % 9.97/10.25 (Or (Eq («$ki_accessible» a a_2) False) % 9.97/10.25 (Or (Eq («$ki_exists_in_world_$i» a_2 a_3) False) % 9.97/10.25 (Eq % 9.97/10.25 («$ki_accessible» a_2 a_4 → % 9.97/10.25 (Exists fun D => % 9.97/10.25 And % 9.97/10.25 (And («$ki_exists_in_world_$i» a_4 D) % 9.97/10.25 (∀ (W2 : «$ki_world»), «$ki_accessible» a_4 W2 → member W2 D a_1)) % 9.97/10.25 (∀ (W2 : «$ki_world»), «$ki_accessible» a_4 W2 → member W2 D a_3)) → % 9.97/10.25 ∀ (W2 : «$ki_world»), «$ki_accessible» a_4 W2 → intersect W2 a_1 a_3) % 9.97/10.25 True)))) % 9.97/10.25 Clause #48 (by clausification #[47]): ∀ (a : «$ki_world») (a_1 : Iota) (a_2 : «$ki_world») (a_3 : Iota) (a_4 : «$ki_world»), % 9.97/10.25 Or (Eq («$ki_accessible» «$ki_local_world» a) False) % 9.97/10.25 (Or (Eq («$ki_exists_in_world_$i» a a_1) False) % 9.97/10.25 (Or (Eq («$ki_accessible» a a_2) False) % 9.97/10.25 (Or (Eq («$ki_exists_in_world_$i» a_2 a_3) False) % 9.97/10.25 (Or (Eq («$ki_accessible» a_2 a_4) False) % 9.97/10.25 (Eq % 9.97/10.25 ((Exists fun D => % 9.97/10.25 And % 9.97/10.25 (And («$ki_exists_in_world_$i» a_4 D) % 9.97/10.25 (∀ (W2 : «$ki_world»), «$ki_accessible» a_4 W2 → member W2 D a_1)) % 9.97/10.25 (∀ (W2 : «$ki_world»), «$ki_accessible» a_4 W2 → member W2 D a_3)) → % 9.97/10.25 ∀ (W2 : «$ki_world»), «$ki_accessible» a_4 W2 → intersect W2 a_1 a_3) % 9.97/10.25 True))))) % 9.97/10.25 Clause #49 (by clausification #[48]): ∀ (a : «$ki_world») (a_1 : Iota) (a_2 : «$ki_world») (a_3 : Iota) (a_4 : «$ki_world»), % 9.97/10.25 Or (Eq («$ki_accessible» «$ki_local_world» a) False) % 9.97/10.25 (Or (Eq («$ki_exists_in_world_$i» a a_1) False) % 9.97/10.25 (Or (Eq («$ki_accessible» a a_2) False) % 9.97/10.25 (Or (Eq («$ki_exists_in_world_$i» a_2 a_3) False) % 9.97/10.25 (Or (Eq («$ki_accessible» a_2 a_4) False) % 9.97/10.25 (Or % 9.97/10.25 (Eq % 9.97/10.25 (Exists fun D => % 9.97/10.25 And % 9.97/10.25 (And («$ki_exists_in_world_$i» a_4 D) % 9.97/10.25 (∀ (W2 : «$ki_world»), «$ki_accessible» a_4 W2 → member W2 D a_1)) % 9.97/10.25 (∀ (W2 : «$ki_world»), «$ki_accessible» a_4 W2 → member W2 D a_3)) % 9.97/10.25 False) % 9.97/10.29 (Eq (∀ (W2 : «$ki_world»), «$ki_accessible» a_4 W2 → intersect W2 a_1 a_3) True)))))) % 9.97/10.29 Clause #50 (by clausification #[49]): ∀ (a : «$ki_world») (a_1 : Iota) (a_2 : «$ki_world») (a_3 : Iota) (a_4 : «$ki_world») (a_5 : Iota), % 9.97/10.29 Or (Eq («$ki_accessible» «$ki_local_world» a) False) % 9.97/10.29 (Or (Eq («$ki_exists_in_world_$i» a a_1) False) % 9.97/10.29 (Or (Eq («$ki_accessible» a a_2) False) % 9.97/10.29 (Or (Eq («$ki_exists_in_world_$i» a_2 a_3) False) % 9.97/10.29 (Or (Eq («$ki_accessible» a_2 a_4) False) % 9.97/10.29 (Or (Eq (∀ (W2 : «$ki_world»), «$ki_accessible» a_4 W2 → intersect W2 a_1 a_3) True) % 9.97/10.29 (Eq % 9.97/10.29 (And % 9.97/10.29 (And («$ki_exists_in_world_$i» a_4 a_5) % 9.97/10.29 (∀ (W2 : «$ki_world»), «$ki_accessible» a_4 W2 → member W2 a_5 a_1)) % 9.97/10.29 (∀ (W2 : «$ki_world»), «$ki_accessible» a_4 W2 → member W2 a_5 a_3)) % 9.97/10.29 False)))))) % 9.97/10.29 Clause #51 (by clausification #[50]): ∀ (a : «$ki_world») (a_1 : Iota) (a_2 : «$ki_world») (a_3 : Iota) (a_4 : «$ki_world») (a_5 : Iota) (a_6 : «$ki_world»), % 9.97/10.29 Or (Eq («$ki_accessible» «$ki_local_world» a) False) % 9.97/10.29 (Or (Eq («$ki_exists_in_world_$i» a a_1) False) % 9.97/10.29 (Or (Eq («$ki_accessible» a a_2) False) % 9.97/10.29 (Or (Eq («$ki_exists_in_world_$i» a_2 a_3) False) % 9.97/10.29 (Or (Eq («$ki_accessible» a_2 a_4) False) % 9.97/10.29 (Or % 9.97/10.29 (Eq % 9.97/10.29 (And % 9.97/10.29 (And («$ki_exists_in_world_$i» a_4 a_5) % 9.97/10.29 (∀ (W2 : «$ki_world»), «$ki_accessible» a_4 W2 → member W2 a_5 a_1)) % 9.97/10.29 (∀ (W2 : «$ki_world»), «$ki_accessible» a_4 W2 → member W2 a_5 a_3)) % 9.97/10.29 False) % 9.97/10.29 (Eq («$ki_accessible» a_4 a_6 → intersect a_6 a_1 a_3) True)))))) % 9.97/10.29 Clause #52 (by clausification #[51]): ∀ (a : «$ki_world») (a_1 : Iota) (a_2 : «$ki_world») (a_3 : Iota) (a_4 a_5 : «$ki_world») (a_6 : Iota), % 9.97/10.29 Or (Eq («$ki_accessible» «$ki_local_world» a) False) % 9.97/10.29 (Or (Eq («$ki_exists_in_world_$i» a a_1) False) % 9.97/10.29 (Or (Eq («$ki_accessible» a a_2) False) % 9.97/10.29 (Or (Eq («$ki_exists_in_world_$i» a_2 a_3) False) % 9.97/10.29 (Or (Eq («$ki_accessible» a_2 a_4) False) % 9.97/10.29 (Or (Eq («$ki_accessible» a_4 a_5 → intersect a_5 a_1 a_3) True) % 9.97/10.29 (Or % 9.97/10.29 (Eq % 9.97/10.29 (And («$ki_exists_in_world_$i» a_4 a_6) % 9.97/10.29 (∀ (W2 : «$ki_world»), «$ki_accessible» a_4 W2 → member W2 a_6 a_1)) % 9.97/10.29 False) % 9.97/10.29 (Eq (∀ (W2 : «$ki_world»), «$ki_accessible» a_4 W2 → member W2 a_6 a_3) False))))))) % 9.97/10.29 Clause #53 (by clausification #[52]): ∀ (a : «$ki_world») (a_1 : Iota) (a_2 : «$ki_world») (a_3 : Iota) (a_4 : «$ki_world») (a_5 : Iota) (a_6 : «$ki_world»), % 9.97/10.29 Or (Eq («$ki_accessible» «$ki_local_world» a) False) % 9.97/10.29 (Or (Eq («$ki_exists_in_world_$i» a a_1) False) % 9.97/10.29 (Or (Eq («$ki_accessible» a a_2) False) % 9.97/10.29 (Or (Eq («$ki_exists_in_world_$i» a_2 a_3) False) % 9.97/10.29 (Or (Eq («$ki_accessible» a_2 a_4) False) % 9.97/10.29 (Or % 9.97/10.29 (Eq % 9.97/10.29 (And («$ki_exists_in_world_$i» a_4 a_5) % 9.97/10.29 (∀ (W2 : «$ki_world»), «$ki_accessible» a_4 W2 → member W2 a_5 a_1)) % 9.97/10.29 False) % 9.97/10.29 (Or (Eq (∀ (W2 : «$ki_world»), «$ki_accessible» a_4 W2 → member W2 a_5 a_3) False) % 9.97/10.29 (Or (Eq («$ki_accessible» a_4 a_6) False) (Eq (intersect a_6 a_1 a_3) True)))))))) % 9.97/10.29 Clause #54 (by clausification #[53]): ∀ (a : «$ki_world») (a_1 : Iota) (a_2 : «$ki_world») (a_3 : Iota) (a_4 : «$ki_world») (a_5 : Iota) (a_6 : «$ki_world»), % 9.97/10.29 Or (Eq («$ki_accessible» «$ki_local_world» a) False) % 9.97/10.29 (Or (Eq («$ki_exists_in_world_$i» a a_1) False) % 9.97/10.29 (Or (Eq («$ki_accessible» a a_2) False) % 9.97/10.29 (Or (Eq («$ki_exists_in_world_$i» a_2 a_3) False) % 9.97/10.29 (Or (Eq («$ki_accessible» a_2 a_4) False) % 9.97/10.29 (Or (Eq (∀ (W2 : «$ki_world»), «$ki_accessible» a_4 W2 → member W2 a_5 a_3) False) % 9.97/10.29 (Or (Eq («$ki_accessible» a_4 a_6) False) % 10.07/10.33 (Or (Eq (intersect a_6 a_1 a_3) True) % 10.07/10.33 (Or (Eq («$ki_exists_in_world_$i» a_4 a_5) False) % 10.07/10.33 (Eq (∀ (W2 : «$ki_world»), «$ki_accessible» a_4 W2 → member W2 a_5 a_1) False))))))))) % 10.07/10.33 Clause #55 (by clausification #[54]): ∀ (a : «$ki_world») (a_1 : Iota) (a_2 : «$ki_world») (a_3 : Iota) (a_4 a_5 : «$ki_world») (a_6 : Iota) % 10.07/10.33 (a_7 : «$ki_world»), % 10.07/10.33 Or (Eq («$ki_accessible» «$ki_local_world» a) False) % 10.07/10.33 (Or (Eq («$ki_exists_in_world_$i» a a_1) False) % 10.07/10.33 (Or (Eq («$ki_accessible» a a_2) False) % 10.07/10.33 (Or (Eq («$ki_exists_in_world_$i» a_2 a_3) False) % 10.07/10.33 (Or (Eq («$ki_accessible» a_2 a_4) False) % 10.07/10.33 (Or (Eq («$ki_accessible» a_4 a_5) False) % 10.07/10.33 (Or (Eq (intersect a_5 a_1 a_3) True) % 10.07/10.33 (Or (Eq («$ki_exists_in_world_$i» a_4 a_6) False) % 10.07/10.33 (Or (Eq (∀ (W2 : «$ki_world»), «$ki_accessible» a_4 W2 → member W2 a_6 a_1) False) % 10.07/10.33 (Eq % 10.07/10.33 (Not («$ki_accessible» a_4 (skS.0 3 a_4 a_6 a_3 a_7) → member (skS.0 3 a_4 a_6 a_3 a_7) a_6 a_3)) % 10.07/10.33 True))))))))) % 10.07/10.33 Clause #56 (by clausification #[55]): ∀ (a : «$ki_world») (a_1 : Iota) (a_2 : «$ki_world») (a_3 : Iota) (a_4 a_5 : «$ki_world») (a_6 : Iota) % 10.07/10.33 (a_7 a_8 : «$ki_world»), % 10.07/10.33 Or (Eq («$ki_accessible» «$ki_local_world» a) False) % 10.07/10.33 (Or (Eq («$ki_exists_in_world_$i» a a_1) False) % 10.07/10.33 (Or (Eq («$ki_accessible» a a_2) False) % 10.07/10.33 (Or (Eq («$ki_exists_in_world_$i» a_2 a_3) False) % 10.07/10.33 (Or (Eq («$ki_accessible» a_2 a_4) False) % 10.07/10.33 (Or (Eq («$ki_accessible» a_4 a_5) False) % 10.07/10.33 (Or (Eq (intersect a_5 a_1 a_3) True) % 10.07/10.33 (Or (Eq («$ki_exists_in_world_$i» a_4 a_6) False) % 10.07/10.33 (Or % 10.07/10.33 (Eq % 10.07/10.33 (Not («$ki_accessible» a_4 (skS.0 3 a_4 a_6 a_3 a_7) → member (skS.0 3 a_4 a_6 a_3 a_7) a_6 a_3)) % 10.07/10.33 True) % 10.07/10.33 (Eq % 10.07/10.33 (Not («$ki_accessible» a_4 (skS.0 4 a_4 a_6 a_1 a_8) → member (skS.0 4 a_4 a_6 a_1 a_8) a_6 a_1)) % 10.07/10.33 True))))))))) % 10.07/10.33 Clause #57 (by clausification #[56]): ∀ (a : «$ki_world») (a_1 : Iota) (a_2 : «$ki_world») (a_3 : Iota) (a_4 a_5 : «$ki_world») (a_6 : Iota) % 10.07/10.33 (a_7 a_8 : «$ki_world»), % 10.07/10.33 Or (Eq («$ki_accessible» «$ki_local_world» a) False) % 10.07/10.33 (Or (Eq («$ki_exists_in_world_$i» a a_1) False) % 10.07/10.33 (Or (Eq («$ki_accessible» a a_2) False) % 10.07/10.33 (Or (Eq («$ki_exists_in_world_$i» a_2 a_3) False) % 10.07/10.33 (Or (Eq («$ki_accessible» a_2 a_4) False) % 10.07/10.33 (Or (Eq («$ki_accessible» a_4 a_5) False) % 10.07/10.33 (Or (Eq (intersect a_5 a_1 a_3) True) % 10.07/10.33 (Or (Eq («$ki_exists_in_world_$i» a_4 a_6) False) % 10.07/10.33 (Or % 10.07/10.33 (Eq % 10.07/10.33 (Not («$ki_accessible» a_4 (skS.0 4 a_4 a_6 a_1 a_7) → member (skS.0 4 a_4 a_6 a_1 a_7) a_6 a_1)) % 10.07/10.33 True) % 10.07/10.33 (Eq («$ki_accessible» a_4 (skS.0 3 a_4 a_6 a_3 a_8) → member (skS.0 3 a_4 a_6 a_3 a_8) a_6 a_3) % 10.07/10.33 False))))))))) % 10.07/10.33 Clause #58 (by clausification #[57]): ∀ (a : «$ki_world») (a_1 : Iota) (a_2 : «$ki_world») (a_3 : Iota) (a_4 a_5 : «$ki_world») (a_6 : Iota) % 10.07/10.33 (a_7 a_8 : «$ki_world»), % 10.07/10.33 Or (Eq («$ki_accessible» «$ki_local_world» a) False) % 10.07/10.33 (Or (Eq («$ki_exists_in_world_$i» a a_1) False) % 10.07/10.33 (Or (Eq («$ki_accessible» a a_2) False) % 10.07/10.33 (Or (Eq («$ki_exists_in_world_$i» a_2 a_3) False) % 10.07/10.33 (Or (Eq («$ki_accessible» a_2 a_4) False) % 10.07/10.33 (Or (Eq («$ki_accessible» a_4 a_5) False) % 10.07/10.33 (Or (Eq (intersect a_5 a_1 a_3) True) % 10.07/10.33 (Or (Eq («$ki_exists_in_world_$i» a_4 a_6) False) % 10.07/10.33 (Or % 10.07/10.33 (Eq («$ki_accessible» a_4 (skS.0 3 a_4 a_6 a_3 a_7) → member (skS.0 3 a_4 a_6 a_3 a_7) a_6 a_3) % 10.07/10.33 False) % 10.07/10.33 (Eq («$ki_accessible» a_4 (skS.0 4 a_4 a_6 a_1 a_8) → member (skS.0 4 a_4 a_6 a_1 a_8) a_6 a_1) % 10.07/10.37 False))))))))) % 10.07/10.37 Clause #60 (by clausification #[58]): ∀ (a : «$ki_world») (a_1 : Iota) (a_2 : «$ki_world») (a_3 : Iota) (a_4 a_5 : «$ki_world») (a_6 : Iota) % 10.07/10.37 (a_7 a_8 : «$ki_world»), % 10.07/10.37 Or (Eq («$ki_accessible» «$ki_local_world» a) False) % 10.07/10.37 (Or (Eq («$ki_exists_in_world_$i» a a_1) False) % 10.07/10.37 (Or (Eq («$ki_accessible» a a_2) False) % 10.07/10.37 (Or (Eq («$ki_exists_in_world_$i» a_2 a_3) False) % 10.07/10.37 (Or (Eq («$ki_accessible» a_2 a_4) False) % 10.07/10.37 (Or (Eq («$ki_accessible» a_4 a_5) False) % 10.07/10.37 (Or (Eq (intersect a_5 a_1 a_3) True) % 10.07/10.37 (Or (Eq («$ki_exists_in_world_$i» a_4 a_6) False) % 10.07/10.37 (Or % 10.07/10.37 (Eq («$ki_accessible» a_4 (skS.0 4 a_4 a_6 a_1 a_7) → member (skS.0 4 a_4 a_6 a_1 a_7) a_6 a_1) % 10.07/10.37 False) % 10.07/10.37 (Eq (member (skS.0 3 a_4 a_6 a_3 a_8) a_6 a_3) False))))))))) % 10.07/10.37 Clause #67 (by clausification #[36]): ∀ (a : «$ki_world») (a_1 : Iota), % 10.07/10.37 Eq % 10.07/10.37 (Not % 10.07/10.37 («$ki_exists_in_world_$i» (skS.0 2 a) (skS.0 5 a a_1) → % 10.07/10.37 ∀ (W0 : «$ki_world»), % 10.07/10.37 «$ki_accessible» (skS.0 2 a) W0 → % 10.07/10.37 ∀ (C : Iota), % 10.07/10.37 «$ki_exists_in_world_$i» W0 C → % 10.07/10.37 ∀ (W1 : «$ki_world»), % 10.07/10.37 «$ki_accessible» W0 W1 → % 10.07/10.37 ∀ (D : Iota), % 10.07/10.37 «$ki_exists_in_world_$i» W1 D → % 10.07/10.37 ∀ (W2 : «$ki_world»), % 10.07/10.37 «$ki_accessible» W1 W2 → % 10.07/10.37 And (∀ (W3 : «$ki_world»), «$ki_accessible» W2 W3 → member W3 (skS.0 5 a a_1) C) % 10.07/10.37 (∀ (W3 : «$ki_world»), «$ki_accessible» W2 W3 → member W3 (skS.0 5 a a_1) D) → % 10.07/10.37 ∀ (W3 : «$ki_world»), «$ki_accessible» W2 W3 → intersect W3 C D)) % 10.07/10.37 True % 10.07/10.37 Clause #68 (by clausification #[67]): ∀ (a : «$ki_world») (a_1 : Iota), % 10.07/10.37 Eq % 10.07/10.37 («$ki_exists_in_world_$i» (skS.0 2 a) (skS.0 5 a a_1) → % 10.07/10.37 ∀ (W0 : «$ki_world»), % 10.07/10.37 «$ki_accessible» (skS.0 2 a) W0 → % 10.07/10.37 ∀ (C : Iota), % 10.07/10.37 «$ki_exists_in_world_$i» W0 C → % 10.07/10.37 ∀ (W1 : «$ki_world»), % 10.07/10.37 «$ki_accessible» W0 W1 → % 10.07/10.37 ∀ (D : Iota), % 10.07/10.37 «$ki_exists_in_world_$i» W1 D → % 10.07/10.37 ∀ (W2 : «$ki_world»), % 10.07/10.37 «$ki_accessible» W1 W2 → % 10.07/10.37 And (∀ (W3 : «$ki_world»), «$ki_accessible» W2 W3 → member W3 (skS.0 5 a a_1) C) % 10.07/10.37 (∀ (W3 : «$ki_world»), «$ki_accessible» W2 W3 → member W3 (skS.0 5 a a_1) D) → % 10.07/10.37 ∀ (W3 : «$ki_world»), «$ki_accessible» W2 W3 → intersect W3 C D) % 10.07/10.37 False % 10.07/10.37 Clause #70 (by clausification #[68]): ∀ (a : «$ki_world») (a_1 : Iota), % 10.07/10.37 Eq % 10.07/10.37 (∀ (W0 : «$ki_world»), % 10.07/10.37 «$ki_accessible» (skS.0 2 a) W0 → % 10.07/10.37 ∀ (C : Iota), % 10.07/10.37 «$ki_exists_in_world_$i» W0 C → % 10.07/10.37 ∀ (W1 : «$ki_world»), % 10.07/10.37 «$ki_accessible» W0 W1 → % 10.07/10.37 ∀ (D : Iota), % 10.07/10.37 «$ki_exists_in_world_$i» W1 D → % 10.07/10.37 ∀ (W2 : «$ki_world»), % 10.07/10.37 «$ki_accessible» W1 W2 → % 10.07/10.37 And (∀ (W3 : «$ki_world»), «$ki_accessible» W2 W3 → member W3 (skS.0 5 a a_1) C) % 10.07/10.37 (∀ (W3 : «$ki_world»), «$ki_accessible» W2 W3 → member W3 (skS.0 5 a a_1) D) → % 10.07/10.37 ∀ (W3 : «$ki_world»), «$ki_accessible» W2 W3 → intersect W3 C D) % 10.07/10.37 False % 10.07/10.37 Clause #71 (by clausification #[70]): ∀ (a : «$ki_world») (a_1 : Iota) (a_2 : «$ki_world»), % 10.07/10.37 Eq % 10.07/10.37 (Not % 10.07/10.37 («$ki_accessible» (skS.0 2 a) (skS.0 6 a a_1 a_2) → % 10.07/10.37 ∀ (C : Iota), % 10.07/10.37 «$ki_exists_in_world_$i» (skS.0 6 a a_1 a_2) C → % 10.07/10.37 ∀ (W1 : «$ki_world»), % 10.07/10.37 «$ki_accessible» (skS.0 6 a a_1 a_2) W1 → % 10.07/10.37 ∀ (D : Iota), % 10.07/10.37 «$ki_exists_in_world_$i» W1 D → % 10.07/10.37 ∀ (W2 : «$ki_world»), % 10.17/10.41 «$ki_accessible» W1 W2 → % 10.17/10.41 And (∀ (W3 : «$ki_world»), «$ki_accessible» W2 W3 → member W3 (skS.0 5 a a_1) C) % 10.17/10.41 (∀ (W3 : «$ki_world»), «$ki_accessible» W2 W3 → member W3 (skS.0 5 a a_1) D) → % 10.17/10.41 ∀ (W3 : «$ki_world»), «$ki_accessible» W2 W3 → intersect W3 C D)) % 10.17/10.41 True % 10.17/10.41 Clause #72 (by clausification #[71]): ∀ (a : «$ki_world») (a_1 : Iota) (a_2 : «$ki_world»), % 10.17/10.41 Eq % 10.17/10.41 («$ki_accessible» (skS.0 2 a) (skS.0 6 a a_1 a_2) → % 10.17/10.41 ∀ (C : Iota), % 10.17/10.41 «$ki_exists_in_world_$i» (skS.0 6 a a_1 a_2) C → % 10.17/10.41 ∀ (W1 : «$ki_world»), % 10.17/10.41 «$ki_accessible» (skS.0 6 a a_1 a_2) W1 → % 10.17/10.41 ∀ (D : Iota), % 10.17/10.41 «$ki_exists_in_world_$i» W1 D → % 10.17/10.41 ∀ (W2 : «$ki_world»), % 10.17/10.41 «$ki_accessible» W1 W2 → % 10.17/10.41 And (∀ (W3 : «$ki_world»), «$ki_accessible» W2 W3 → member W3 (skS.0 5 a a_1) C) % 10.17/10.41 (∀ (W3 : «$ki_world»), «$ki_accessible» W2 W3 → member W3 (skS.0 5 a a_1) D) → % 10.17/10.41 ∀ (W3 : «$ki_world»), «$ki_accessible» W2 W3 → intersect W3 C D) % 10.17/10.41 False % 10.17/10.41 Clause #74 (by clausification #[72]): ∀ (a : «$ki_world») (a_1 : Iota) (a_2 : «$ki_world»), % 10.17/10.41 Eq % 10.17/10.41 (∀ (C : Iota), % 10.17/10.41 «$ki_exists_in_world_$i» (skS.0 6 a a_1 a_2) C → % 10.17/10.41 ∀ (W1 : «$ki_world»), % 10.17/10.41 «$ki_accessible» (skS.0 6 a a_1 a_2) W1 → % 10.17/10.41 ∀ (D : Iota), % 10.17/10.41 «$ki_exists_in_world_$i» W1 D → % 10.17/10.41 ∀ (W2 : «$ki_world»), % 10.17/10.41 «$ki_accessible» W1 W2 → % 10.17/10.41 And (∀ (W3 : «$ki_world»), «$ki_accessible» W2 W3 → member W3 (skS.0 5 a a_1) C) % 10.17/10.41 (∀ (W3 : «$ki_world»), «$ki_accessible» W2 W3 → member W3 (skS.0 5 a a_1) D) → % 10.17/10.41 ∀ (W3 : «$ki_world»), «$ki_accessible» W2 W3 → intersect W3 C D) % 10.17/10.41 False % 10.17/10.41 Clause #75 (by clausification #[74]): ∀ (a : «$ki_world») (a_1 : Iota) (a_2 : «$ki_world») (a_3 : Iota), % 10.17/10.41 Eq % 10.17/10.41 (Not % 10.17/10.41 («$ki_exists_in_world_$i» (skS.0 6 a a_1 a_2) (skS.0 7 a a_1 a_2 a_3) → % 10.17/10.41 ∀ (W1 : «$ki_world»), % 10.17/10.41 «$ki_accessible» (skS.0 6 a a_1 a_2) W1 → % 10.17/10.41 ∀ (D : Iota), % 10.17/10.41 «$ki_exists_in_world_$i» W1 D → % 10.17/10.41 ∀ (W2 : «$ki_world»), % 10.17/10.41 «$ki_accessible» W1 W2 → % 10.17/10.41 And % 10.17/10.41 (∀ (W3 : «$ki_world»), % 10.17/10.41 «$ki_accessible» W2 W3 → member W3 (skS.0 5 a a_1) (skS.0 7 a a_1 a_2 a_3)) % 10.17/10.41 (∀ (W3 : «$ki_world»), «$ki_accessible» W2 W3 → member W3 (skS.0 5 a a_1) D) → % 10.17/10.41 ∀ (W3 : «$ki_world»), «$ki_accessible» W2 W3 → intersect W3 (skS.0 7 a a_1 a_2 a_3) D)) % 10.17/10.41 True % 10.17/10.41 Clause #76 (by clausification #[75]): ∀ (a : «$ki_world») (a_1 : Iota) (a_2 : «$ki_world») (a_3 : Iota), % 10.17/10.41 Eq % 10.17/10.41 («$ki_exists_in_world_$i» (skS.0 6 a a_1 a_2) (skS.0 7 a a_1 a_2 a_3) → % 10.17/10.41 ∀ (W1 : «$ki_world»), % 10.17/10.41 «$ki_accessible» (skS.0 6 a a_1 a_2) W1 → % 10.17/10.41 ∀ (D : Iota), % 10.17/10.41 «$ki_exists_in_world_$i» W1 D → % 10.17/10.41 ∀ (W2 : «$ki_world»), % 10.17/10.41 «$ki_accessible» W1 W2 → % 10.17/10.41 And (∀ (W3 : «$ki_world»), «$ki_accessible» W2 W3 → member W3 (skS.0 5 a a_1) (skS.0 7 a a_1 a_2 a_3)) % 10.17/10.41 (∀ (W3 : «$ki_world»), «$ki_accessible» W2 W3 → member W3 (skS.0 5 a a_1) D) → % 10.17/10.41 ∀ (W3 : «$ki_world»), «$ki_accessible» W2 W3 → intersect W3 (skS.0 7 a a_1 a_2 a_3) D) % 10.17/10.41 False % 10.17/10.41 Clause #78 (by clausification #[76]): ∀ (a : «$ki_world») (a_1 : Iota) (a_2 : «$ki_world») (a_3 : Iota), % 10.17/10.41 Eq % 10.17/10.41 (∀ (W1 : «$ki_world»), % 10.17/10.41 «$ki_accessible» (skS.0 6 a a_1 a_2) W1 → % 10.17/10.41 ∀ (D : Iota), % 10.17/10.41 «$ki_exists_in_world_$i» W1 D → % 10.17/10.41 ∀ (W2 : «$ki_world»), % 10.17/10.41 «$ki_accessible» W1 W2 → % 10.17/10.41 And (∀ (W3 : «$ki_world»), «$ki_accessible» W2 W3 → member W3 (skS.0 5 a a_1) (skS.0 7 a a_1 a_2 a_3)) % 10.17/10.45 (∀ (W3 : «$ki_world»), «$ki_accessible» W2 W3 → member W3 (skS.0 5 a a_1) D) → % 10.17/10.45 ∀ (W3 : «$ki_world»), «$ki_accessible» W2 W3 → intersect W3 (skS.0 7 a a_1 a_2 a_3) D) % 10.17/10.45 False % 10.17/10.45 Clause #79 (by clausification #[78]): ∀ (a : «$ki_world») (a_1 : Iota) (a_2 : «$ki_world») (a_3 : Iota) (a_4 : «$ki_world»), % 10.17/10.45 Eq % 10.17/10.45 (Not % 10.17/10.45 («$ki_accessible» (skS.0 6 a a_1 a_2) (skS.0 8 a a_1 a_2 a_3 a_4) → % 10.17/10.45 ∀ (D : Iota), % 10.17/10.45 «$ki_exists_in_world_$i» (skS.0 8 a a_1 a_2 a_3 a_4) D → % 10.17/10.45 ∀ (W2 : «$ki_world»), % 10.17/10.45 «$ki_accessible» (skS.0 8 a a_1 a_2 a_3 a_4) W2 → % 10.17/10.45 And (∀ (W3 : «$ki_world»), «$ki_accessible» W2 W3 → member W3 (skS.0 5 a a_1) (skS.0 7 a a_1 a_2 a_3)) % 10.17/10.45 (∀ (W3 : «$ki_world»), «$ki_accessible» W2 W3 → member W3 (skS.0 5 a a_1) D) → % 10.17/10.45 ∀ (W3 : «$ki_world»), «$ki_accessible» W2 W3 → intersect W3 (skS.0 7 a a_1 a_2 a_3) D)) % 10.17/10.45 True % 10.17/10.45 Clause #80 (by clausification #[79]): ∀ (a : «$ki_world») (a_1 : Iota) (a_2 : «$ki_world») (a_3 : Iota) (a_4 : «$ki_world»), % 10.17/10.45 Eq % 10.17/10.45 («$ki_accessible» (skS.0 6 a a_1 a_2) (skS.0 8 a a_1 a_2 a_3 a_4) → % 10.17/10.45 ∀ (D : Iota), % 10.17/10.45 «$ki_exists_in_world_$i» (skS.0 8 a a_1 a_2 a_3 a_4) D → % 10.17/10.45 ∀ (W2 : «$ki_world»), % 10.17/10.45 «$ki_accessible» (skS.0 8 a a_1 a_2 a_3 a_4) W2 → % 10.17/10.45 And (∀ (W3 : «$ki_world»), «$ki_accessible» W2 W3 → member W3 (skS.0 5 a a_1) (skS.0 7 a a_1 a_2 a_3)) % 10.17/10.45 (∀ (W3 : «$ki_world»), «$ki_accessible» W2 W3 → member W3 (skS.0 5 a a_1) D) → % 10.17/10.45 ∀ (W3 : «$ki_world»), «$ki_accessible» W2 W3 → intersect W3 (skS.0 7 a a_1 a_2 a_3) D) % 10.17/10.45 False % 10.17/10.45 Clause #82 (by clausification #[80]): ∀ (a : «$ki_world») (a_1 : Iota) (a_2 : «$ki_world») (a_3 : Iota) (a_4 : «$ki_world»), % 10.17/10.45 Eq % 10.17/10.45 (∀ (D : Iota), % 10.17/10.45 «$ki_exists_in_world_$i» (skS.0 8 a a_1 a_2 a_3 a_4) D → % 10.17/10.45 ∀ (W2 : «$ki_world»), % 10.17/10.45 «$ki_accessible» (skS.0 8 a a_1 a_2 a_3 a_4) W2 → % 10.17/10.45 And (∀ (W3 : «$ki_world»), «$ki_accessible» W2 W3 → member W3 (skS.0 5 a a_1) (skS.0 7 a a_1 a_2 a_3)) % 10.17/10.45 (∀ (W3 : «$ki_world»), «$ki_accessible» W2 W3 → member W3 (skS.0 5 a a_1) D) → % 10.17/10.45 ∀ (W3 : «$ki_world»), «$ki_accessible» W2 W3 → intersect W3 (skS.0 7 a a_1 a_2 a_3) D) % 10.17/10.45 False % 10.17/10.45 Clause #83 (by clausification #[82]): ∀ (a : «$ki_world») (a_1 : Iota) (a_2 : «$ki_world») (a_3 : Iota) (a_4 : «$ki_world») (a_5 : Iota), % 10.17/10.45 Eq % 10.17/10.45 (Not % 10.17/10.45 («$ki_exists_in_world_$i» (skS.0 8 a a_1 a_2 a_3 a_4) (skS.0 9 a a_1 a_2 a_3 a_4 a_5) → % 10.17/10.45 ∀ (W2 : «$ki_world»), % 10.17/10.45 «$ki_accessible» (skS.0 8 a a_1 a_2 a_3 a_4) W2 → % 10.17/10.45 And (∀ (W3 : «$ki_world»), «$ki_accessible» W2 W3 → member W3 (skS.0 5 a a_1) (skS.0 7 a a_1 a_2 a_3)) % 10.17/10.45 (∀ (W3 : «$ki_world»), % 10.17/10.45 «$ki_accessible» W2 W3 → member W3 (skS.0 5 a a_1) (skS.0 9 a a_1 a_2 a_3 a_4 a_5)) → % 10.17/10.45 ∀ (W3 : «$ki_world»), % 10.17/10.45 «$ki_accessible» W2 W3 → intersect W3 (skS.0 7 a a_1 a_2 a_3) (skS.0 9 a a_1 a_2 a_3 a_4 a_5))) % 10.17/10.45 True % 10.17/10.45 Clause #84 (by clausification #[83]): ∀ (a : «$ki_world») (a_1 : Iota) (a_2 : «$ki_world») (a_3 : Iota) (a_4 : «$ki_world») (a_5 : Iota), % 10.17/10.45 Eq % 10.17/10.45 («$ki_exists_in_world_$i» (skS.0 8 a a_1 a_2 a_3 a_4) (skS.0 9 a a_1 a_2 a_3 a_4 a_5) → % 10.17/10.45 ∀ (W2 : «$ki_world»), % 10.17/10.45 «$ki_accessible» (skS.0 8 a a_1 a_2 a_3 a_4) W2 → % 10.17/10.45 And (∀ (W3 : «$ki_world»), «$ki_accessible» W2 W3 → member W3 (skS.0 5 a a_1) (skS.0 7 a a_1 a_2 a_3)) % 10.17/10.45 (∀ (W3 : «$ki_world»), % 10.17/10.45 «$ki_accessible» W2 W3 → member W3 (skS.0 5 a a_1) (skS.0 9 a a_1 a_2 a_3 a_4 a_5)) → % 10.17/10.45 ∀ (W3 : «$ki_world»), % 10.17/10.45 «$ki_accessible» W2 W3 → intersect W3 (skS.0 7 a a_1 a_2 a_3) (skS.0 9 a a_1 a_2 a_3 a_4 a_5)) % 10.27/10.50 False % 10.27/10.50 Clause #86 (by clausification #[84]): ∀ (a : «$ki_world») (a_1 : Iota) (a_2 : «$ki_world») (a_3 : Iota) (a_4 : «$ki_world») (a_5 : Iota), % 10.27/10.50 Eq % 10.27/10.50 (∀ (W2 : «$ki_world»), % 10.27/10.50 «$ki_accessible» (skS.0 8 a a_1 a_2 a_3 a_4) W2 → % 10.27/10.50 And (∀ (W3 : «$ki_world»), «$ki_accessible» W2 W3 → member W3 (skS.0 5 a a_1) (skS.0 7 a a_1 a_2 a_3)) % 10.27/10.50 (∀ (W3 : «$ki_world»), «$ki_accessible» W2 W3 → member W3 (skS.0 5 a a_1) (skS.0 9 a a_1 a_2 a_3 a_4 a_5)) → % 10.27/10.50 ∀ (W3 : «$ki_world»), % 10.27/10.50 «$ki_accessible» W2 W3 → intersect W3 (skS.0 7 a a_1 a_2 a_3) (skS.0 9 a a_1 a_2 a_3 a_4 a_5)) % 10.27/10.50 False % 10.27/10.50 Clause #87 (by forward demodulation #[29, 9]): ∀ (a : «$ki_world») (a_1 : Iota) (a_2 : «$ki_world») (a_3 : Iota) (a_4 a_5 a_6 : «$ki_world»), % 10.27/10.50 Or (Eq True False) % 10.27/10.50 (Or (Eq («$ki_exists_in_world_$i» a a_1) False) % 10.27/10.50 (Or (Eq («$ki_accessible» a a_2) False) % 10.27/10.50 (Or (Eq («$ki_exists_in_world_$i» a_2 a_3) False) % 10.27/10.50 (Or (Eq («$ki_accessible» a_2 a_4) False) % 10.27/10.50 (Or (Eq («$ki_accessible» a_4 a_5) False) % 10.27/10.50 (Or (Eq (intersect a_5 a_3 a_1) True) (Eq (intersect (skS.0 1 a_4 a_1 a_3 a_6) a_1 a_3) False))))))) % 10.27/10.50 Clause #88 (by clausification #[87]): ∀ (a : «$ki_world») (a_1 : Iota) (a_2 : «$ki_world») (a_3 : Iota) (a_4 a_5 a_6 : «$ki_world»), % 10.27/10.50 Or (Eq («$ki_exists_in_world_$i» a a_1) False) % 10.27/10.50 (Or (Eq («$ki_accessible» a a_2) False) % 10.27/10.50 (Or (Eq («$ki_exists_in_world_$i» a_2 a_3) False) % 10.27/10.50 (Or (Eq («$ki_accessible» a_2 a_4) False) % 10.27/10.50 (Or (Eq («$ki_accessible» a_4 a_5) False) % 10.27/10.50 (Or (Eq (intersect a_5 a_3 a_1) True) (Eq (intersect (skS.0 1 a_4 a_1 a_3 a_6) a_1 a_3) False)))))) % 10.27/10.50 Clause #89 (by superposition #[88, 7]): ∀ (a a_1 : «$ki_world») (a_2 : Iota) (a_3 a_4 : «$ki_world») (a_5 : Iota) (a_6 : «$ki_world»), % 10.27/10.50 Or (Eq («$ki_accessible» a a_1) False) % 10.27/10.50 (Or (Eq («$ki_exists_in_world_$i» a_1 a_2) False) % 10.27/10.50 (Or (Eq («$ki_accessible» a_1 a_3) False) % 10.27/10.50 (Or (Eq («$ki_accessible» a_3 a_4) False) % 10.27/10.50 (Or (Eq (intersect a_4 a_2 a_5) True) % 10.27/10.50 (Or (Eq (intersect (skS.0 1 a_3 a_5 a_2 a_6) a_5 a_2) False) (Eq False True)))))) % 10.27/10.50 Clause #90 (by clausification #[86]): ∀ (a : «$ki_world») (a_1 : Iota) (a_2 : «$ki_world») (a_3 : Iota) (a_4 : «$ki_world») (a_5 : Iota) (a_6 : «$ki_world»), % 10.27/10.50 Eq % 10.27/10.50 (Not % 10.27/10.50 («$ki_accessible» (skS.0 8 a a_1 a_2 a_3 a_4) (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6) → % 10.27/10.50 And % 10.27/10.50 (∀ (W3 : «$ki_world»), % 10.27/10.50 «$ki_accessible» (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6) W3 → % 10.27/10.50 member W3 (skS.0 5 a a_1) (skS.0 7 a a_1 a_2 a_3)) % 10.27/10.50 (∀ (W3 : «$ki_world»), % 10.27/10.50 «$ki_accessible» (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6) W3 → % 10.27/10.50 member W3 (skS.0 5 a a_1) (skS.0 9 a a_1 a_2 a_3 a_4 a_5)) → % 10.27/10.50 ∀ (W3 : «$ki_world»), % 10.27/10.50 «$ki_accessible» (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6) W3 → % 10.27/10.50 intersect W3 (skS.0 7 a a_1 a_2 a_3) (skS.0 9 a a_1 a_2 a_3 a_4 a_5))) % 10.27/10.50 True % 10.27/10.50 Clause #91 (by clausification #[90]): ∀ (a : «$ki_world») (a_1 : Iota) (a_2 : «$ki_world») (a_3 : Iota) (a_4 : «$ki_world») (a_5 : Iota) (a_6 : «$ki_world»), % 10.27/10.50 Eq % 10.27/10.50 («$ki_accessible» (skS.0 8 a a_1 a_2 a_3 a_4) (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6) → % 10.27/10.50 And % 10.27/10.50 (∀ (W3 : «$ki_world»), % 10.27/10.50 «$ki_accessible» (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6) W3 → % 10.27/10.50 member W3 (skS.0 5 a a_1) (skS.0 7 a a_1 a_2 a_3)) % 10.27/10.50 (∀ (W3 : «$ki_world»), % 10.27/10.50 «$ki_accessible» (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6) W3 → % 10.27/10.50 member W3 (skS.0 5 a a_1) (skS.0 9 a a_1 a_2 a_3 a_4 a_5)) → % 10.27/10.50 ∀ (W3 : «$ki_world»), % 10.27/10.50 «$ki_accessible» (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6) W3 → % 10.27/10.50 intersect W3 (skS.0 7 a a_1 a_2 a_3) (skS.0 9 a a_1 a_2 a_3 a_4 a_5)) % 10.27/10.50 False % 10.27/10.50 Clause #93 (by clausification #[91]): ∀ (a : «$ki_world») (a_1 : Iota) (a_2 : «$ki_world») (a_3 : Iota) (a_4 : «$ki_world») (a_5 : Iota) (a_6 : «$ki_world»), % 10.27/10.54 Eq % 10.27/10.54 (And % 10.27/10.54 (∀ (W3 : «$ki_world»), % 10.27/10.54 «$ki_accessible» (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6) W3 → member W3 (skS.0 5 a a_1) (skS.0 7 a a_1 a_2 a_3)) % 10.27/10.54 (∀ (W3 : «$ki_world»), % 10.27/10.54 «$ki_accessible» (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6) W3 → % 10.27/10.54 member W3 (skS.0 5 a a_1) (skS.0 9 a a_1 a_2 a_3 a_4 a_5)) → % 10.27/10.54 ∀ (W3 : «$ki_world»), % 10.27/10.54 «$ki_accessible» (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6) W3 → % 10.27/10.54 intersect W3 (skS.0 7 a a_1 a_2 a_3) (skS.0 9 a a_1 a_2 a_3 a_4 a_5)) % 10.27/10.54 False % 10.27/10.54 Clause #94 (by clausification #[93]): ∀ (a : «$ki_world») (a_1 : Iota) (a_2 : «$ki_world») (a_3 : Iota) (a_4 : «$ki_world») (a_5 : Iota) (a_6 : «$ki_world»), % 10.27/10.54 Eq % 10.27/10.54 (And % 10.27/10.54 (∀ (W3 : «$ki_world»), % 10.27/10.54 «$ki_accessible» (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6) W3 → member W3 (skS.0 5 a a_1) (skS.0 7 a a_1 a_2 a_3)) % 10.27/10.54 (∀ (W3 : «$ki_world»), % 10.27/10.54 «$ki_accessible» (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6) W3 → % 10.27/10.54 member W3 (skS.0 5 a a_1) (skS.0 9 a a_1 a_2 a_3 a_4 a_5))) % 10.27/10.54 True % 10.27/10.54 Clause #95 (by clausification #[93]): ∀ (a : «$ki_world») (a_1 : Iota) (a_2 : «$ki_world») (a_3 : Iota) (a_4 : «$ki_world») (a_5 : Iota) (a_6 : «$ki_world»), % 10.27/10.54 Eq % 10.27/10.54 (∀ (W3 : «$ki_world»), % 10.27/10.54 «$ki_accessible» (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6) W3 → % 10.27/10.54 intersect W3 (skS.0 7 a a_1 a_2 a_3) (skS.0 9 a a_1 a_2 a_3 a_4 a_5)) % 10.27/10.54 False % 10.27/10.54 Clause #96 (by clausification #[94]): ∀ (a : «$ki_world») (a_1 : Iota) (a_2 : «$ki_world») (a_3 : Iota) (a_4 : «$ki_world») (a_5 : Iota) (a_6 : «$ki_world»), % 10.27/10.54 Eq % 10.27/10.54 (∀ (W3 : «$ki_world»), % 10.27/10.54 «$ki_accessible» (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6) W3 → % 10.27/10.54 member W3 (skS.0 5 a a_1) (skS.0 9 a a_1 a_2 a_3 a_4 a_5)) % 10.27/10.54 True % 10.27/10.54 Clause #97 (by clausification #[94]): ∀ (a : «$ki_world») (a_1 : Iota) (a_2 : «$ki_world») (a_3 : Iota) (a_4 : «$ki_world») (a_5 : Iota) (a_6 : «$ki_world»), % 10.27/10.54 Eq % 10.27/10.54 (∀ (W3 : «$ki_world»), % 10.27/10.54 «$ki_accessible» (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6) W3 → member W3 (skS.0 5 a a_1) (skS.0 7 a a_1 a_2 a_3)) % 10.27/10.54 True % 10.27/10.54 Clause #98 (by clausification #[96]): ∀ (a : «$ki_world») (a_1 : Iota) (a_2 : «$ki_world») (a_3 : Iota) (a_4 : «$ki_world») (a_5 : Iota) % 10.27/10.54 (a_6 a_7 : «$ki_world»), % 10.27/10.54 Eq % 10.27/10.54 («$ki_accessible» (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6) a_7 → % 10.27/10.54 member a_7 (skS.0 5 a a_1) (skS.0 9 a a_1 a_2 a_3 a_4 a_5)) % 10.27/10.54 True % 10.27/10.54 Clause #99 (by clausification #[98]): ∀ (a : «$ki_world») (a_1 : Iota) (a_2 : «$ki_world») (a_3 : Iota) (a_4 : «$ki_world») (a_5 : Iota) % 10.27/10.54 (a_6 a_7 : «$ki_world»), % 10.27/10.54 Or (Eq («$ki_accessible» (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6) a_7) False) % 10.27/10.54 (Eq (member a_7 (skS.0 5 a a_1) (skS.0 9 a a_1 a_2 a_3 a_4 a_5)) True) % 10.27/10.54 Clause #100 (by superposition #[99, 9]): ∀ (a a_1 : «$ki_world») (a_2 : Iota) (a_3 : «$ki_world») (a_4 : Iota) (a_5 : «$ki_world») (a_6 : Iota), % 10.27/10.54 Or (Eq (member a (skS.0 5 a_1 a_2) (skS.0 9 a_1 a_2 a_3 a_4 a_5 a_6)) True) (Eq False True) % 10.27/10.54 Clause #101 (by clausification #[97]): ∀ (a : «$ki_world») (a_1 : Iota) (a_2 : «$ki_world») (a_3 : Iota) (a_4 : «$ki_world») (a_5 : Iota) % 10.27/10.54 (a_6 a_7 : «$ki_world»), % 10.27/10.54 Eq («$ki_accessible» (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6) a_7 → member a_7 (skS.0 5 a a_1) (skS.0 7 a a_1 a_2 a_3)) % 10.27/10.54 True % 10.27/10.54 Clause #102 (by clausification #[101]): ∀ (a : «$ki_world») (a_1 : Iota) (a_2 : «$ki_world») (a_3 : Iota) (a_4 : «$ki_world») (a_5 : Iota) % 10.27/10.54 (a_6 a_7 : «$ki_world»), % 10.27/10.54 Or (Eq («$ki_accessible» (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6) a_7) False) % 10.27/10.54 (Eq (member a_7 (skS.0 5 a a_1) (skS.0 7 a a_1 a_2 a_3)) True) % 10.27/10.54 Clause #103 (by superposition #[102, 9]): ∀ (a a_1 : «$ki_world») (a_2 : Iota) (a_3 : «$ki_world») (a_4 : Iota), % 10.27/10.54 Or (Eq (member a (skS.0 5 a_1 a_2) (skS.0 7 a_1 a_2 a_3 a_4)) True) (Eq False True) % 10.27/10.54 Clause #104 (by clausification #[103]): ∀ (a a_1 : «$ki_world») (a_2 : Iota) (a_3 : «$ki_world») (a_4 : Iota), % 10.27/10.54 Eq (member a (skS.0 5 a_1 a_2) (skS.0 7 a_1 a_2 a_3 a_4)) True % 10.27/10.54 Clause #105 (by clausification #[100]): ∀ (a a_1 : «$ki_world») (a_2 : Iota) (a_3 : «$ki_world») (a_4 : Iota) (a_5 : «$ki_world») (a_6 : Iota), % 10.27/10.60 Eq (member a (skS.0 5 a_1 a_2) (skS.0 9 a_1 a_2 a_3 a_4 a_5 a_6)) True % 10.27/10.60 Clause #122 (by clausification #[95]): ∀ (a : «$ki_world») (a_1 : Iota) (a_2 : «$ki_world») (a_3 : Iota) (a_4 : «$ki_world») (a_5 : Iota) % 10.27/10.60 (a_6 a_7 : «$ki_world»), % 10.27/10.60 Eq % 10.27/10.60 (Not % 10.27/10.60 («$ki_accessible» (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 13 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) → % 10.27/10.60 intersect (skS.0 13 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 7 a a_1 a_2 a_3) (skS.0 9 a a_1 a_2 a_3 a_4 a_5))) % 10.27/10.60 True % 10.27/10.60 Clause #123 (by clausification #[122]): ∀ (a : «$ki_world») (a_1 : Iota) (a_2 : «$ki_world») (a_3 : Iota) (a_4 : «$ki_world») (a_5 : Iota) % 10.27/10.60 (a_6 a_7 : «$ki_world»), % 10.27/10.60 Eq % 10.27/10.60 («$ki_accessible» (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 13 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) → % 10.27/10.60 intersect (skS.0 13 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 7 a a_1 a_2 a_3) (skS.0 9 a a_1 a_2 a_3 a_4 a_5)) % 10.27/10.60 False % 10.27/10.60 Clause #125 (by clausification #[123]): ∀ (a : «$ki_world») (a_1 : Iota) (a_2 : «$ki_world») (a_3 : Iota) (a_4 : «$ki_world») (a_5 : Iota) % 10.27/10.60 (a_6 a_7 : «$ki_world»), % 10.27/10.60 Eq (intersect (skS.0 13 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 7 a a_1 a_2 a_3) (skS.0 9 a a_1 a_2 a_3 a_4 a_5)) False % 10.27/10.60 Clause #126 (by clausification #[89]): ∀ (a a_1 : «$ki_world») (a_2 : Iota) (a_3 a_4 : «$ki_world») (a_5 : Iota) (a_6 : «$ki_world»), % 10.27/10.60 Or (Eq («$ki_accessible» a a_1) False) % 10.27/10.60 (Or (Eq («$ki_exists_in_world_$i» a_1 a_2) False) % 10.27/10.60 (Or (Eq («$ki_accessible» a_1 a_3) False) % 10.27/10.60 (Or (Eq («$ki_accessible» a_3 a_4) False) % 10.27/10.60 (Or (Eq (intersect a_4 a_2 a_5) True) (Eq (intersect (skS.0 1 a_3 a_5 a_2 a_6) a_5 a_2) False))))) % 10.27/10.60 Clause #127 (by superposition #[126, 9]): ∀ (a : «$ki_world») (a_1 : Iota) (a_2 a_3 : «$ki_world») (a_4 : Iota) (a_5 : «$ki_world»), % 10.27/10.60 Or (Eq («$ki_exists_in_world_$i» a a_1) False) % 10.27/10.60 (Or (Eq («$ki_accessible» a a_2) False) % 10.27/10.60 (Or (Eq («$ki_accessible» a_2 a_3) False) % 10.27/10.60 (Or (Eq (intersect a_3 a_1 a_4) True) % 10.27/10.60 (Or (Eq (intersect (skS.0 1 a_2 a_4 a_1 a_5) a_4 a_1) False) (Eq False True))))) % 10.27/10.60 Clause #128 (by clausification #[127]): ∀ (a : «$ki_world») (a_1 : Iota) (a_2 a_3 : «$ki_world») (a_4 : Iota) (a_5 : «$ki_world»), % 10.27/10.60 Or (Eq («$ki_exists_in_world_$i» a a_1) False) % 10.27/10.60 (Or (Eq («$ki_accessible» a a_2) False) % 10.27/10.60 (Or (Eq («$ki_accessible» a_2 a_3) False) % 10.27/10.60 (Or (Eq (intersect a_3 a_1 a_4) True) (Eq (intersect (skS.0 1 a_2 a_4 a_1 a_5) a_4 a_1) False)))) % 10.27/10.60 Clause #129 (by superposition #[128, 7]): ∀ (a a_1 a_2 : «$ki_world») (a_3 a_4 : Iota) (a_5 : «$ki_world»), % 10.27/10.60 Or (Eq («$ki_accessible» a a_1) False) % 10.27/10.60 (Or (Eq («$ki_accessible» a_1 a_2) False) % 10.27/10.60 (Or (Eq (intersect a_2 a_3 a_4) True) % 10.27/10.60 (Or (Eq (intersect (skS.0 1 a_1 a_4 a_3 a_5) a_4 a_3) False) (Eq False True)))) % 10.27/10.60 Clause #130 (by clausification #[129]): ∀ (a a_1 a_2 : «$ki_world») (a_3 a_4 : Iota) (a_5 : «$ki_world»), % 10.27/10.60 Or (Eq («$ki_accessible» a a_1) False) % 10.27/10.60 (Or (Eq («$ki_accessible» a_1 a_2) False) % 10.27/10.60 (Or (Eq (intersect a_2 a_3 a_4) True) (Eq (intersect (skS.0 1 a_1 a_4 a_3 a_5) a_4 a_3) False))) % 10.27/10.60 Clause #131 (by superposition #[130, 9]): ∀ (a a_1 : «$ki_world») (a_2 a_3 : Iota) (a_4 : «$ki_world»), % 10.27/10.60 Or (Eq («$ki_accessible» a a_1) False) % 10.27/10.60 (Or (Eq (intersect a_1 a_2 a_3) True) (Or (Eq (intersect (skS.0 1 a a_3 a_2 a_4) a_3 a_2) False) (Eq False True))) % 10.27/10.60 Clause #132 (by clausification #[131]): ∀ (a a_1 : «$ki_world») (a_2 a_3 : Iota) (a_4 : «$ki_world»), % 10.27/10.60 Or (Eq («$ki_accessible» a a_1) False) % 10.27/10.60 (Or (Eq (intersect a_1 a_2 a_3) True) (Eq (intersect (skS.0 1 a a_3 a_2 a_4) a_3 a_2) False)) % 10.27/10.60 Clause #133 (by superposition #[132, 9]): ∀ (a : «$ki_world») (a_1 a_2 : Iota) (a_3 a_4 : «$ki_world»), % 10.27/10.60 Or (Eq (intersect a a_1 a_2) True) (Or (Eq (intersect (skS.0 1 a_3 a_2 a_1 a_4) a_2 a_1) False) (Eq False True)) % 10.27/10.60 Clause #135 (by clausification #[60]): ∀ (a : «$ki_world») (a_1 : Iota) (a_2 : «$ki_world») (a_3 : Iota) (a_4 a_5 : «$ki_world») (a_6 : Iota) % 10.37/10.64 (a_7 a_8 : «$ki_world»), % 10.37/10.64 Or (Eq («$ki_accessible» «$ki_local_world» a) False) % 10.37/10.64 (Or (Eq («$ki_exists_in_world_$i» a a_1) False) % 10.37/10.64 (Or (Eq («$ki_accessible» a a_2) False) % 10.37/10.64 (Or (Eq («$ki_exists_in_world_$i» a_2 a_3) False) % 10.37/10.64 (Or (Eq («$ki_accessible» a_2 a_4) False) % 10.37/10.64 (Or (Eq («$ki_accessible» a_4 a_5) False) % 10.37/10.64 (Or (Eq (intersect a_5 a_1 a_3) True) % 10.37/10.64 (Or (Eq («$ki_exists_in_world_$i» a_4 a_6) False) % 10.37/10.64 (Or (Eq (member (skS.0 3 a_4 a_6 a_3 a_7) a_6 a_3) False) % 10.37/10.64 (Eq (member (skS.0 4 a_4 a_6 a_1 a_8) a_6 a_1) False))))))))) % 10.37/10.64 Clause #140 (by clausification #[133]): ∀ (a : «$ki_world») (a_1 a_2 : Iota) (a_3 a_4 : «$ki_world»), % 10.37/10.64 Or (Eq (intersect a a_1 a_2) True) (Eq (intersect (skS.0 1 a_3 a_2 a_1 a_4) a_2 a_1) False) % 10.37/10.64 Clause #159 (by forward demodulation #[135, 9]): ∀ (a : «$ki_world») (a_1 : Iota) (a_2 : «$ki_world») (a_3 : Iota) (a_4 a_5 : «$ki_world») (a_6 : Iota) % 10.37/10.64 (a_7 a_8 : «$ki_world»), % 10.37/10.64 Or (Eq True False) % 10.37/10.64 (Or (Eq («$ki_exists_in_world_$i» a a_1) False) % 10.37/10.64 (Or (Eq («$ki_accessible» a a_2) False) % 10.37/10.64 (Or (Eq («$ki_exists_in_world_$i» a_2 a_3) False) % 10.37/10.64 (Or (Eq («$ki_accessible» a_2 a_4) False) % 10.37/10.64 (Or (Eq («$ki_accessible» a_4 a_5) False) % 10.37/10.64 (Or (Eq (intersect a_5 a_1 a_3) True) % 10.37/10.64 (Or (Eq («$ki_exists_in_world_$i» a_4 a_6) False) % 10.37/10.64 (Or (Eq (member (skS.0 3 a_4 a_6 a_3 a_7) a_6 a_3) False) % 10.37/10.64 (Eq (member (skS.0 4 a_4 a_6 a_1 a_8) a_6 a_1) False))))))))) % 10.37/10.64 Clause #160 (by clausification #[159]): ∀ (a : «$ki_world») (a_1 : Iota) (a_2 : «$ki_world») (a_3 : Iota) (a_4 a_5 : «$ki_world») (a_6 : Iota) % 10.37/10.64 (a_7 a_8 : «$ki_world»), % 10.37/10.64 Or (Eq («$ki_exists_in_world_$i» a a_1) False) % 10.37/10.64 (Or (Eq («$ki_accessible» a a_2) False) % 10.37/10.64 (Or (Eq («$ki_exists_in_world_$i» a_2 a_3) False) % 10.37/10.64 (Or (Eq («$ki_accessible» a_2 a_4) False) % 10.37/10.64 (Or (Eq («$ki_accessible» a_4 a_5) False) % 10.37/10.64 (Or (Eq (intersect a_5 a_1 a_3) True) % 10.37/10.64 (Or (Eq («$ki_exists_in_world_$i» a_4 a_6) False) % 10.37/10.64 (Or (Eq (member (skS.0 3 a_4 a_6 a_3 a_7) a_6 a_3) False) % 10.37/10.64 (Eq (member (skS.0 4 a_4 a_6 a_1 a_8) a_6 a_1) False)))))))) % 10.37/10.64 Clause #161 (by forward demodulation #[160, 7]): ∀ (a : «$ki_world») (a_1 : Iota) (a_2 : «$ki_world») (a_3 : Iota) (a_4 a_5 : «$ki_world») (a_6 : Iota) % 10.37/10.64 (a_7 a_8 : «$ki_world»), % 10.37/10.64 Or (Eq («$ki_exists_in_world_$i» a a_1) False) % 10.37/10.64 (Or (Eq («$ki_accessible» a a_2) False) % 10.37/10.64 (Or (Eq («$ki_exists_in_world_$i» a_2 a_3) False) % 10.37/10.64 (Or (Eq («$ki_accessible» a_2 a_4) False) % 10.37/10.64 (Or (Eq («$ki_accessible» a_4 a_5) False) % 10.37/10.64 (Or (Eq (intersect a_5 a_1 a_3) True) % 10.37/10.64 (Or (Eq True False) % 10.37/10.64 (Or (Eq (member (skS.0 3 a_4 a_6 a_3 a_7) a_6 a_3) False) % 10.37/10.64 (Eq (member (skS.0 4 a_4 a_6 a_1 a_8) a_6 a_1) False)))))))) % 10.37/10.64 Clause #162 (by clausification #[161]): ∀ (a : «$ki_world») (a_1 : Iota) (a_2 : «$ki_world») (a_3 : Iota) (a_4 a_5 : «$ki_world») (a_6 : Iota) % 10.37/10.64 (a_7 a_8 : «$ki_world»), % 10.37/10.64 Or (Eq («$ki_exists_in_world_$i» a a_1) False) % 10.37/10.64 (Or (Eq («$ki_accessible» a a_2) False) % 10.37/10.64 (Or (Eq («$ki_exists_in_world_$i» a_2 a_3) False) % 10.37/10.64 (Or (Eq («$ki_accessible» a_2 a_4) False) % 10.37/10.64 (Or (Eq («$ki_accessible» a_4 a_5) False) % 10.37/10.64 (Or (Eq (intersect a_5 a_1 a_3) True) % 10.37/10.64 (Or (Eq (member (skS.0 3 a_4 a_6 a_3 a_7) a_6 a_3) False) % 10.37/10.64 (Eq (member (skS.0 4 a_4 a_6 a_1 a_8) a_6 a_1) False))))))) % 10.37/10.64 Clause #163 (by superposition #[162, 7]): ∀ (a a_1 : «$ki_world») (a_2 : Iota) (a_3 a_4 : «$ki_world») (a_5 a_6 : Iota) (a_7 a_8 : «$ki_world»), % 10.37/10.64 Or (Eq («$ki_accessible» a a_1) False) % 10.37/10.64 (Or (Eq («$ki_exists_in_world_$i» a_1 a_2) False) % 10.37/10.64 (Or (Eq («$ki_accessible» a_1 a_3) False) % 10.37/10.64 (Or (Eq («$ki_accessible» a_3 a_4) False) % 10.37/10.64 (Or (Eq (intersect a_4 a_5 a_2) True) % 10.37/10.64 (Or (Eq (member (skS.0 3 a_3 a_6 a_2 a_7) a_6 a_2) False) % 10.37/10.69 (Or (Eq (member (skS.0 4 a_3 a_6 a_5 a_8) a_6 a_5) False) (Eq False True))))))) % 10.37/10.69 Clause #164 (by clausification #[163]): ∀ (a a_1 : «$ki_world») (a_2 : Iota) (a_3 a_4 : «$ki_world») (a_5 a_6 : Iota) (a_7 a_8 : «$ki_world»), % 10.37/10.69 Or (Eq («$ki_accessible» a a_1) False) % 10.37/10.69 (Or (Eq («$ki_exists_in_world_$i» a_1 a_2) False) % 10.37/10.69 (Or (Eq («$ki_accessible» a_1 a_3) False) % 10.37/10.69 (Or (Eq («$ki_accessible» a_3 a_4) False) % 10.37/10.69 (Or (Eq (intersect a_4 a_5 a_2) True) % 10.37/10.69 (Or (Eq (member (skS.0 3 a_3 a_6 a_2 a_7) a_6 a_2) False) % 10.37/10.69 (Eq (member (skS.0 4 a_3 a_6 a_5 a_8) a_6 a_5) False)))))) % 10.37/10.69 Clause #165 (by superposition #[164, 9]): ∀ (a : «$ki_world») (a_1 : Iota) (a_2 a_3 : «$ki_world») (a_4 a_5 : Iota) (a_6 a_7 : «$ki_world»), % 10.37/10.69 Or (Eq («$ki_exists_in_world_$i» a a_1) False) % 10.37/10.69 (Or (Eq («$ki_accessible» a a_2) False) % 10.37/10.69 (Or (Eq («$ki_accessible» a_2 a_3) False) % 10.37/10.69 (Or (Eq (intersect a_3 a_4 a_1) True) % 10.37/10.69 (Or (Eq (member (skS.0 3 a_2 a_5 a_1 a_6) a_5 a_1) False) % 10.37/10.69 (Or (Eq (member (skS.0 4 a_2 a_5 a_4 a_7) a_5 a_4) False) (Eq False True)))))) % 10.37/10.69 Clause #166 (by clausification #[165]): ∀ (a : «$ki_world») (a_1 : Iota) (a_2 a_3 : «$ki_world») (a_4 a_5 : Iota) (a_6 a_7 : «$ki_world»), % 10.37/10.69 Or (Eq («$ki_exists_in_world_$i» a a_1) False) % 10.37/10.69 (Or (Eq («$ki_accessible» a a_2) False) % 10.37/10.69 (Or (Eq («$ki_accessible» a_2 a_3) False) % 10.37/10.69 (Or (Eq (intersect a_3 a_4 a_1) True) % 10.37/10.69 (Or (Eq (member (skS.0 3 a_2 a_5 a_1 a_6) a_5 a_1) False) % 10.37/10.69 (Eq (member (skS.0 4 a_2 a_5 a_4 a_7) a_5 a_4) False))))) % 10.37/10.69 Clause #167 (by superposition #[166, 7]): ∀ (a a_1 a_2 : «$ki_world») (a_3 a_4 a_5 : Iota) (a_6 a_7 : «$ki_world»), % 10.37/10.69 Or (Eq («$ki_accessible» a a_1) False) % 10.37/10.69 (Or (Eq («$ki_accessible» a_1 a_2) False) % 10.37/10.69 (Or (Eq (intersect a_2 a_3 a_4) True) % 10.37/10.69 (Or (Eq (member (skS.0 3 a_1 a_5 a_4 a_6) a_5 a_4) False) % 10.37/10.69 (Or (Eq (member (skS.0 4 a_1 a_5 a_3 a_7) a_5 a_3) False) (Eq False True))))) % 10.37/10.69 Clause #178 (by clausification #[167]): ∀ (a a_1 a_2 : «$ki_world») (a_3 a_4 a_5 : Iota) (a_6 a_7 : «$ki_world»), % 10.37/10.69 Or (Eq («$ki_accessible» a a_1) False) % 10.37/10.69 (Or (Eq («$ki_accessible» a_1 a_2) False) % 10.37/10.69 (Or (Eq (intersect a_2 a_3 a_4) True) % 10.37/10.69 (Or (Eq (member (skS.0 3 a_1 a_5 a_4 a_6) a_5 a_4) False) % 10.37/10.69 (Eq (member (skS.0 4 a_1 a_5 a_3 a_7) a_5 a_3) False)))) % 10.37/10.69 Clause #179 (by superposition #[178, 9]): ∀ (a a_1 : «$ki_world») (a_2 a_3 a_4 : Iota) (a_5 a_6 : «$ki_world»), % 10.37/10.69 Or (Eq («$ki_accessible» a a_1) False) % 10.37/10.69 (Or (Eq (intersect a_1 a_2 a_3) True) % 10.37/10.69 (Or (Eq (member (skS.0 3 a a_4 a_3 a_5) a_4 a_3) False) % 10.37/10.69 (Or (Eq (member (skS.0 4 a a_4 a_2 a_6) a_4 a_2) False) (Eq False True)))) % 10.37/10.69 Clause #180 (by clausification #[179]): ∀ (a a_1 : «$ki_world») (a_2 a_3 a_4 : Iota) (a_5 a_6 : «$ki_world»), % 10.37/10.69 Or (Eq («$ki_accessible» a a_1) False) % 10.37/10.69 (Or (Eq (intersect a_1 a_2 a_3) True) % 10.37/10.69 (Or (Eq (member (skS.0 3 a a_4 a_3 a_5) a_4 a_3) False) (Eq (member (skS.0 4 a a_4 a_2 a_6) a_4 a_2) False))) % 10.37/10.69 Clause #181 (by superposition #[180, 9]): ∀ (a : «$ki_world») (a_1 a_2 : Iota) (a_3 : «$ki_world») (a_4 : Iota) (a_5 a_6 : «$ki_world»), % 10.37/10.69 Or (Eq (intersect a a_1 a_2) True) % 10.37/10.69 (Or (Eq (member (skS.0 3 a_3 a_4 a_2 a_5) a_4 a_2) False) % 10.37/10.69 (Or (Eq (member (skS.0 4 a_3 a_4 a_1 a_6) a_4 a_1) False) (Eq False True))) % 10.37/10.69 Clause #182 (by clausification #[181]): ∀ (a : «$ki_world») (a_1 a_2 : Iota) (a_3 : «$ki_world») (a_4 : Iota) (a_5 a_6 : «$ki_world»), % 10.37/10.69 Or (Eq (intersect a a_1 a_2) True) % 10.37/10.69 (Or (Eq (member (skS.0 3 a_3 a_4 a_2 a_5) a_4 a_2) False) (Eq (member (skS.0 4 a_3 a_4 a_1 a_6) a_4 a_1) False)) % 10.37/10.69 Clause #183 (by superposition #[182, 104]): ∀ (a : «$ki_world») (a_1 : Iota) (a_2 : «$ki_world») (a_3 : Iota) (a_4 : «$ki_world») (a_5 : Iota) % 10.37/10.69 (a_6 a_7 : «$ki_world»), % 10.37/10.69 Or (Eq (intersect a a_1 (skS.0 7 a_2 a_3 a_4 a_5)) True) % 10.37/10.69 (Or (Eq (member (skS.0 4 a_6 (skS.0 5 a_2 a_3) a_1 a_7) (skS.0 5 a_2 a_3) a_1) False) (Eq False True)) % 10.37/10.69 Clause #185 (by clausification #[183]): ∀ (a : «$ki_world») (a_1 : Iota) (a_2 : «$ki_world») (a_3 : Iota) (a_4 : «$ki_world») (a_5 : Iota) % 10.47/10.71 (a_6 a_7 : «$ki_world»), % 10.47/10.71 Or (Eq (intersect a a_1 (skS.0 7 a_2 a_3 a_4 a_5)) True) % 10.47/10.71 (Eq (member (skS.0 4 a_6 (skS.0 5 a_2 a_3) a_1 a_7) (skS.0 5 a_2 a_3) a_1) False) % 10.47/10.71 Clause #187 (by superposition #[185, 105]): ∀ (a a_1 : «$ki_world») (a_2 : Iota) (a_3 : «$ki_world») (a_4 : Iota) (a_5 : «$ki_world») (a_6 : Iota) % 10.47/10.71 (a_7 : «$ki_world») (a_8 : Iota), % 10.47/10.71 Or (Eq (intersect a (skS.0 9 a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 7 a_1 a_2 a_7 a_8)) True) (Eq False True) % 10.47/10.71 Clause #200 (by clausification #[187]): ∀ (a a_1 : «$ki_world») (a_2 : Iota) (a_3 : «$ki_world») (a_4 : Iota) (a_5 : «$ki_world») (a_6 : Iota) % 10.47/10.71 (a_7 : «$ki_world») (a_8 : Iota), Eq (intersect a (skS.0 9 a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 7 a_1 a_2 a_7 a_8)) True % 10.47/10.71 Clause #201 (by superposition #[200, 140]): ∀ (a a_1 : «$ki_world») (a_2 : Iota) (a_3 : «$ki_world») (a_4 : Iota) (a_5 : «$ki_world») (a_6 : Iota) % 10.47/10.71 (a_7 : «$ki_world») (a_8 : Iota), % 10.47/10.71 Or (Eq (intersect a (skS.0 7 a_1 a_2 a_3 a_4) (skS.0 9 a_1 a_2 a_5 a_6 a_7 a_8)) True) (Eq True False) % 10.47/10.71 Clause #203 (by clausification #[201]): ∀ (a a_1 : «$ki_world») (a_2 : Iota) (a_3 : «$ki_world») (a_4 : Iota) (a_5 : «$ki_world») (a_6 : Iota) % 10.47/10.71 (a_7 : «$ki_world») (a_8 : Iota), Eq (intersect a (skS.0 7 a_1 a_2 a_3 a_4) (skS.0 9 a_1 a_2 a_5 a_6 a_7 a_8)) True % 10.47/10.71 Clause #204 (by superposition #[203, 125]): Eq True False % 10.47/10.71 Clause #207 (by clausification #[204]): False % 10.47/10.71 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------