%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : PLA054_4 : TPTP v9.2.0. Released v8.2.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n001.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 07:58:04 PM UTC 2025 % Result : Theorem 4.02s 4.21s % Output : Proof 4.16s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.04/0.12 % Problem : PLA054_4 : TPTP v9.2.0. Released v8.2.0. % 0.13/0.14 % Command : duper %s % 0.14/0.35 % Computer : n001.cluster.edu % 0.14/0.35 % Model : x86_64 x86_64 % 0.14/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.14/0.35 % Memory : 8042.1875MB % 0.14/0.35 % OS : Linux 3.10.0-693.el7.x86_64 % 0.14/0.35 % CPULimit : 300 % 0.14/0.35 % WCLimit : 300 % 0.14/0.35 % DateTime : Thu Oct 2 08:57:53 EDT 2025 % 0.21/0.35 % CPUTime : % 4.02/4.21 SZS status Theorem for theBenchmark.p % 4.02/4.21 SZS output start Proof for theBenchmark.p % 4.02/4.21 Clause #0 (by assumption #[]): Eq (∀ (W : «$ki_world»), «$ki_accessible» W W) True % 4.02/4.21 Clause #2 (by assumption #[]): Eq (∀ (W : «$ki_world») (X : Iota), «$ki_exists_in_world_$i» W X) True % 4.02/4.21 Clause #4 (by assumption #[]): Eq % 4.02/4.21 (∀ (W : «$ki_world»), % 4.02/4.21 «$ki_accessible» «$ki_local_world» W → % 4.02/4.21 ∀ (S : Iota), % 4.02/4.21 «$ki_exists_in_world_$i» W S → % 4.02/4.21 ∀ (V : Iota), % 4.02/4.21 «$ki_exists_in_world_$i» W V → % 4.02/4.21 Exists fun O => % 4.02/4.21 And % 4.02/4.21 (And («$ki_exists_in_world_$i» W O) % 4.02/4.21 (∀ (W0 : «$ki_world»), % 4.02/4.21 «$ki_accessible» W W0 → % 4.02/4.21 And (And (closed W0 S) (combo W0 S V)) (h W0 O) → % 4.02/4.21 ∀ (W1 : «$ki_world»), «$ki_accessible» W0 W1 → open W1 S)) % 4.02/4.21 (∀ (W0 : «$ki_world»), % 4.02/4.21 «$ki_accessible» W W0 → % 4.02/4.21 And (And (closed W0 S) (Not (combo W0 S V))) (h W0 o) → % 4.02/4.21 ∀ (W1 : «$ki_world»), «$ki_accessible» W0 W1 → closed W1 S)) % 4.02/4.21 True % 4.02/4.21 Clause #5 (by assumption #[]): Eq (∀ (W : «$ki_world»), «$ki_accessible» «$ki_local_world» W → closed W d) True % 4.02/4.21 Clause #7 (by assumption #[]): Eq % 4.02/4.21 (∀ (W : «$ki_world»), % 4.02/4.21 «$ki_accessible» «$ki_local_world» W → % 4.02/4.21 ∀ (S : Iota), «$ki_exists_in_world_$i» W S → Not (And (open W S) (closed W S))) % 4.02/4.21 True % 4.02/4.21 Clause #9 (by assumption #[]): Eq % 4.02/4.21 (Not % 4.02/4.21 (∀ (W : «$ki_world»), % 4.02/4.21 «$ki_accessible» «$ki_local_world» W → % 4.02/4.21 Exists fun V => % 4.02/4.21 And («$ki_exists_in_world_$i» W V) % 4.02/4.21 (Exists fun O => % 4.02/4.21 And («$ki_exists_in_world_$i» W O) % 4.02/4.21 ((∀ (W0 : «$ki_world»), «$ki_accessible» W W0 → And (combo W0 d V) (h W0 O)) → % 4.02/4.21 ∀ (W0 : «$ki_world»), «$ki_accessible» W W0 → open W0 d)))) % 4.02/4.21 True % 4.02/4.21 Clause #10 (by clausification #[0]): ∀ (a : «$ki_world»), Eq («$ki_accessible» a a) True % 4.02/4.21 Clause #11 (by clausification #[5]): ∀ (a : «$ki_world»), Eq («$ki_accessible» «$ki_local_world» a → closed a d) True % 4.02/4.21 Clause #12 (by clausification #[11]): ∀ (a : «$ki_world»), Or (Eq («$ki_accessible» «$ki_local_world» a) False) (Eq (closed a d) True) % 4.02/4.21 Clause #15 (by clausification #[2]): ∀ (a : «$ki_world»), Eq (∀ (X : Iota), «$ki_exists_in_world_$i» a X) True % 4.02/4.21 Clause #16 (by clausification #[15]): ∀ (a : «$ki_world») (a_1 : Iota), Eq («$ki_exists_in_world_$i» a a_1) True % 4.02/4.21 Clause #27 (by clausification #[7]): ∀ (a : «$ki_world»), % 4.02/4.21 Eq % 4.02/4.21 («$ki_accessible» «$ki_local_world» a → % 4.02/4.21 ∀ (S : Iota), «$ki_exists_in_world_$i» a S → Not (And (open a S) (closed a S))) % 4.02/4.21 True % 4.02/4.21 Clause #28 (by clausification #[27]): ∀ (a : «$ki_world»), % 4.02/4.21 Or (Eq («$ki_accessible» «$ki_local_world» a) False) % 4.02/4.21 (Eq (∀ (S : Iota), «$ki_exists_in_world_$i» a S → Not (And (open a S) (closed a S))) True) % 4.02/4.21 Clause #29 (by clausification #[28]): ∀ (a : «$ki_world») (a_1 : Iota), % 4.02/4.21 Or (Eq («$ki_accessible» «$ki_local_world» a) False) % 4.02/4.21 (Eq («$ki_exists_in_world_$i» a a_1 → Not (And (open a a_1) (closed a a_1))) True) % 4.02/4.21 Clause #30 (by clausification #[29]): ∀ (a : «$ki_world») (a_1 : Iota), % 4.02/4.21 Or (Eq («$ki_accessible» «$ki_local_world» a) False) % 4.02/4.21 (Or (Eq («$ki_exists_in_world_$i» a a_1) False) (Eq (Not (And (open a a_1) (closed a a_1))) True)) % 4.02/4.21 Clause #31 (by clausification #[30]): ∀ (a : «$ki_world») (a_1 : Iota), % 4.02/4.21 Or (Eq («$ki_accessible» «$ki_local_world» a) False) % 4.02/4.21 (Or (Eq («$ki_exists_in_world_$i» a a_1) False) (Eq (And (open a a_1) (closed a a_1)) False)) % 4.02/4.21 Clause #32 (by clausification #[31]): ∀ (a : «$ki_world») (a_1 : Iota), % 4.02/4.21 Or (Eq («$ki_accessible» «$ki_local_world» a) False) % 4.02/4.21 (Or (Eq («$ki_exists_in_world_$i» a a_1) False) (Or (Eq (open a a_1) False) (Eq (closed a a_1) False))) % 4.02/4.21 Clause #33 (by forward demodulation #[32, 16]): ∀ (a : «$ki_world») (a_1 : Iota), % 4.02/4.21 Or (Eq («$ki_accessible» «$ki_local_world» a) False) % 4.02/4.23 (Or (Eq True False) (Or (Eq (open a a_1) False) (Eq (closed a a_1) False))) % 4.02/4.23 Clause #34 (by clausification #[33]): ∀ (a : «$ki_world») (a_1 : Iota), % 4.02/4.23 Or (Eq («$ki_accessible» «$ki_local_world» a) False) (Or (Eq (open a a_1) False) (Eq (closed a a_1) False)) % 4.02/4.23 Clause #47 (by clausification #[4]): ∀ (a : «$ki_world»), % 4.02/4.23 Eq % 4.02/4.23 («$ki_accessible» «$ki_local_world» a → % 4.02/4.23 ∀ (S : Iota), % 4.02/4.23 «$ki_exists_in_world_$i» a S → % 4.02/4.23 ∀ (V : Iota), % 4.02/4.23 «$ki_exists_in_world_$i» a V → % 4.02/4.23 Exists fun O => % 4.02/4.23 And % 4.02/4.23 (And («$ki_exists_in_world_$i» a O) % 4.02/4.23 (∀ (W0 : «$ki_world»), % 4.02/4.23 «$ki_accessible» a W0 → % 4.02/4.23 And (And (closed W0 S) (combo W0 S V)) (h W0 O) → % 4.02/4.23 ∀ (W1 : «$ki_world»), «$ki_accessible» W0 W1 → open W1 S)) % 4.02/4.23 (∀ (W0 : «$ki_world»), % 4.02/4.23 «$ki_accessible» a W0 → % 4.02/4.23 And (And (closed W0 S) (Not (combo W0 S V))) (h W0 o) → % 4.02/4.23 ∀ (W1 : «$ki_world»), «$ki_accessible» W0 W1 → closed W1 S)) % 4.02/4.23 True % 4.02/4.23 Clause #48 (by clausification #[47]): ∀ (a : «$ki_world»), % 4.02/4.23 Or (Eq («$ki_accessible» «$ki_local_world» a) False) % 4.02/4.23 (Eq % 4.02/4.23 (∀ (S : Iota), % 4.02/4.23 «$ki_exists_in_world_$i» a S → % 4.02/4.23 ∀ (V : Iota), % 4.02/4.23 «$ki_exists_in_world_$i» a V → % 4.02/4.23 Exists fun O => % 4.02/4.23 And % 4.02/4.23 (And («$ki_exists_in_world_$i» a O) % 4.02/4.23 (∀ (W0 : «$ki_world»), % 4.02/4.23 «$ki_accessible» a W0 → % 4.02/4.23 And (And (closed W0 S) (combo W0 S V)) (h W0 O) → % 4.02/4.23 ∀ (W1 : «$ki_world»), «$ki_accessible» W0 W1 → open W1 S)) % 4.02/4.23 (∀ (W0 : «$ki_world»), % 4.02/4.23 «$ki_accessible» a W0 → % 4.02/4.23 And (And (closed W0 S) (Not (combo W0 S V))) (h W0 o) → % 4.02/4.23 ∀ (W1 : «$ki_world»), «$ki_accessible» W0 W1 → closed W1 S)) % 4.02/4.23 True) % 4.02/4.23 Clause #49 (by clausification #[48]): ∀ (a : «$ki_world») (a_1 : Iota), % 4.02/4.23 Or (Eq («$ki_accessible» «$ki_local_world» a) False) % 4.02/4.23 (Eq % 4.02/4.23 («$ki_exists_in_world_$i» a a_1 → % 4.02/4.23 ∀ (V : Iota), % 4.02/4.23 «$ki_exists_in_world_$i» a V → % 4.02/4.23 Exists fun O => % 4.02/4.23 And % 4.02/4.23 (And («$ki_exists_in_world_$i» a O) % 4.02/4.23 (∀ (W0 : «$ki_world»), % 4.02/4.23 «$ki_accessible» a W0 → % 4.02/4.23 And (And (closed W0 a_1) (combo W0 a_1 V)) (h W0 O) → % 4.02/4.23 ∀ (W1 : «$ki_world»), «$ki_accessible» W0 W1 → open W1 a_1)) % 4.02/4.23 (∀ (W0 : «$ki_world»), % 4.02/4.23 «$ki_accessible» a W0 → % 4.02/4.23 And (And (closed W0 a_1) (Not (combo W0 a_1 V))) (h W0 o) → % 4.02/4.23 ∀ (W1 : «$ki_world»), «$ki_accessible» W0 W1 → closed W1 a_1)) % 4.02/4.23 True) % 4.02/4.23 Clause #50 (by clausification #[49]): ∀ (a : «$ki_world») (a_1 : Iota), % 4.02/4.23 Or (Eq («$ki_accessible» «$ki_local_world» a) False) % 4.02/4.23 (Or (Eq («$ki_exists_in_world_$i» a a_1) False) % 4.02/4.23 (Eq % 4.02/4.23 (∀ (V : Iota), % 4.02/4.23 «$ki_exists_in_world_$i» a V → % 4.02/4.23 Exists fun O => % 4.02/4.23 And % 4.02/4.23 (And («$ki_exists_in_world_$i» a O) % 4.02/4.23 (∀ (W0 : «$ki_world»), % 4.02/4.23 «$ki_accessible» a W0 → % 4.02/4.23 And (And (closed W0 a_1) (combo W0 a_1 V)) (h W0 O) → % 4.02/4.23 ∀ (W1 : «$ki_world»), «$ki_accessible» W0 W1 → open W1 a_1)) % 4.02/4.23 (∀ (W0 : «$ki_world»), % 4.02/4.23 «$ki_accessible» a W0 → % 4.02/4.23 And (And (closed W0 a_1) (Not (combo W0 a_1 V))) (h W0 o) → % 4.02/4.23 ∀ (W1 : «$ki_world»), «$ki_accessible» W0 W1 → closed W1 a_1)) % 4.02/4.23 True)) % 4.02/4.23 Clause #51 (by clausification #[50]): ∀ (a : «$ki_world») (a_1 a_2 : Iota), % 4.02/4.23 Or (Eq («$ki_accessible» «$ki_local_world» a) False) % 4.02/4.23 (Or (Eq («$ki_exists_in_world_$i» a a_1) False) % 4.08/4.24 (Eq % 4.08/4.24 («$ki_exists_in_world_$i» a a_2 → % 4.08/4.24 Exists fun O => % 4.08/4.24 And % 4.08/4.24 (And («$ki_exists_in_world_$i» a O) % 4.08/4.24 (∀ (W0 : «$ki_world»), % 4.08/4.24 «$ki_accessible» a W0 → % 4.08/4.24 And (And (closed W0 a_1) (combo W0 a_1 a_2)) (h W0 O) → % 4.08/4.24 ∀ (W1 : «$ki_world»), «$ki_accessible» W0 W1 → open W1 a_1)) % 4.08/4.24 (∀ (W0 : «$ki_world»), % 4.08/4.24 «$ki_accessible» a W0 → % 4.08/4.24 And (And (closed W0 a_1) (Not (combo W0 a_1 a_2))) (h W0 o) → % 4.08/4.24 ∀ (W1 : «$ki_world»), «$ki_accessible» W0 W1 → closed W1 a_1)) % 4.08/4.24 True)) % 4.08/4.24 Clause #52 (by clausification #[51]): ∀ (a : «$ki_world») (a_1 a_2 : Iota), % 4.08/4.24 Or (Eq («$ki_accessible» «$ki_local_world» a) False) % 4.08/4.24 (Or (Eq («$ki_exists_in_world_$i» a a_1) False) % 4.08/4.24 (Or (Eq («$ki_exists_in_world_$i» a a_2) False) % 4.08/4.24 (Eq % 4.08/4.24 (Exists fun O => % 4.08/4.24 And % 4.08/4.24 (And («$ki_exists_in_world_$i» a O) % 4.08/4.24 (∀ (W0 : «$ki_world»), % 4.08/4.24 «$ki_accessible» a W0 → % 4.08/4.24 And (And (closed W0 a_1) (combo W0 a_1 a_2)) (h W0 O) → % 4.08/4.24 ∀ (W1 : «$ki_world»), «$ki_accessible» W0 W1 → open W1 a_1)) % 4.08/4.24 (∀ (W0 : «$ki_world»), % 4.08/4.24 «$ki_accessible» a W0 → % 4.08/4.24 And (And (closed W0 a_1) (Not (combo W0 a_1 a_2))) (h W0 o) → % 4.08/4.24 ∀ (W1 : «$ki_world»), «$ki_accessible» W0 W1 → closed W1 a_1)) % 4.08/4.24 True))) % 4.08/4.24 Clause #53 (by clausification #[52]): ∀ (a : «$ki_world») (a_1 a_2 a_3 : Iota), % 4.08/4.24 Or (Eq («$ki_accessible» «$ki_local_world» a) False) % 4.08/4.24 (Or (Eq («$ki_exists_in_world_$i» a a_1) False) % 4.08/4.24 (Or (Eq («$ki_exists_in_world_$i» a a_2) False) % 4.08/4.24 (Eq % 4.08/4.24 (And % 4.08/4.24 (And («$ki_exists_in_world_$i» a (skS.0 2 a a_1 a_2 a_3)) % 4.08/4.24 (∀ (W0 : «$ki_world»), % 4.08/4.24 «$ki_accessible» a W0 → % 4.08/4.24 And (And (closed W0 a_1) (combo W0 a_1 a_2)) (h W0 (skS.0 2 a a_1 a_2 a_3)) → % 4.08/4.24 ∀ (W1 : «$ki_world»), «$ki_accessible» W0 W1 → open W1 a_1)) % 4.08/4.24 (∀ (W0 : «$ki_world»), % 4.08/4.24 «$ki_accessible» a W0 → % 4.08/4.24 And (And (closed W0 a_1) (Not (combo W0 a_1 a_2))) (h W0 o) → % 4.08/4.24 ∀ (W1 : «$ki_world»), «$ki_accessible» W0 W1 → closed W1 a_1)) % 4.08/4.24 True))) % 4.08/4.24 Clause #55 (by clausification #[53]): ∀ (a : «$ki_world») (a_1 a_2 a_3 : Iota), % 4.08/4.24 Or (Eq («$ki_accessible» «$ki_local_world» a) False) % 4.08/4.24 (Or (Eq («$ki_exists_in_world_$i» a a_1) False) % 4.08/4.24 (Or (Eq («$ki_exists_in_world_$i» a a_2) False) % 4.08/4.24 (Eq % 4.08/4.24 (And («$ki_exists_in_world_$i» a (skS.0 2 a a_1 a_2 a_3)) % 4.08/4.24 (∀ (W0 : «$ki_world»), % 4.08/4.24 «$ki_accessible» a W0 → % 4.08/4.24 And (And (closed W0 a_1) (combo W0 a_1 a_2)) (h W0 (skS.0 2 a a_1 a_2 a_3)) → % 4.08/4.24 ∀ (W1 : «$ki_world»), «$ki_accessible» W0 W1 → open W1 a_1)) % 4.08/4.24 True))) % 4.08/4.24 Clause #66 (by clausification #[9]): Eq % 4.08/4.24 (∀ (W : «$ki_world»), % 4.08/4.24 «$ki_accessible» «$ki_local_world» W → % 4.08/4.24 Exists fun V => % 4.08/4.24 And («$ki_exists_in_world_$i» W V) % 4.08/4.24 (Exists fun O => % 4.08/4.24 And («$ki_exists_in_world_$i» W O) % 4.08/4.24 ((∀ (W0 : «$ki_world»), «$ki_accessible» W W0 → And (combo W0 d V) (h W0 O)) → % 4.08/4.24 ∀ (W0 : «$ki_world»), «$ki_accessible» W W0 → open W0 d))) % 4.08/4.24 False % 4.08/4.24 Clause #67 (by clausification #[66]): ∀ (a : «$ki_world»), % 4.08/4.24 Eq % 4.08/4.24 (Not % 4.08/4.24 («$ki_accessible» «$ki_local_world» (skS.0 3 a) → % 4.08/4.24 Exists fun V => % 4.08/4.24 And («$ki_exists_in_world_$i» (skS.0 3 a) V) % 4.08/4.24 (Exists fun O => % 4.08/4.24 And («$ki_exists_in_world_$i» (skS.0 3 a) O) % 4.08/4.24 ((∀ (W0 : «$ki_world»), «$ki_accessible» (skS.0 3 a) W0 → And (combo W0 d V) (h W0 O)) → % 4.08/4.24 ∀ (W0 : «$ki_world»), «$ki_accessible» (skS.0 3 a) W0 → open W0 d)))) % 4.08/4.24 True % 4.08/4.24 Clause #68 (by clausification #[67]): ∀ (a : «$ki_world»), % 4.10/4.26 Eq % 4.10/4.26 («$ki_accessible» «$ki_local_world» (skS.0 3 a) → % 4.10/4.26 Exists fun V => % 4.10/4.26 And («$ki_exists_in_world_$i» (skS.0 3 a) V) % 4.10/4.26 (Exists fun O => % 4.10/4.26 And («$ki_exists_in_world_$i» (skS.0 3 a) O) % 4.10/4.26 ((∀ (W0 : «$ki_world»), «$ki_accessible» (skS.0 3 a) W0 → And (combo W0 d V) (h W0 O)) → % 4.10/4.26 ∀ (W0 : «$ki_world»), «$ki_accessible» (skS.0 3 a) W0 → open W0 d))) % 4.10/4.26 False % 4.10/4.26 Clause #69 (by clausification #[68]): ∀ (a : «$ki_world»), Eq («$ki_accessible» «$ki_local_world» (skS.0 3 a)) True % 4.10/4.26 Clause #70 (by clausification #[68]): ∀ (a : «$ki_world»), % 4.10/4.26 Eq % 4.10/4.26 (Exists fun V => % 4.10/4.26 And («$ki_exists_in_world_$i» (skS.0 3 a) V) % 4.10/4.26 (Exists fun O => % 4.10/4.26 And («$ki_exists_in_world_$i» (skS.0 3 a) O) % 4.10/4.26 ((∀ (W0 : «$ki_world»), «$ki_accessible» (skS.0 3 a) W0 → And (combo W0 d V) (h W0 O)) → % 4.10/4.26 ∀ (W0 : «$ki_world»), «$ki_accessible» (skS.0 3 a) W0 → open W0 d))) % 4.10/4.26 False % 4.10/4.26 Clause #71 (by superposition #[69, 12]): ∀ (a : «$ki_world»), Or (Eq True False) (Eq (closed (skS.0 3 a) d) True) % 4.10/4.26 Clause #72 (by superposition #[69, 34]): ∀ (a : «$ki_world») (a_1 : Iota), % 4.10/4.26 Or (Eq True False) (Or (Eq (open (skS.0 3 a) a_1) False) (Eq (closed (skS.0 3 a) a_1) False)) % 4.10/4.26 Clause #76 (by clausification #[71]): ∀ (a : «$ki_world»), Eq (closed (skS.0 3 a) d) True % 4.10/4.26 Clause #79 (by clausification #[55]): ∀ (a : «$ki_world») (a_1 a_2 a_3 : Iota), % 4.10/4.26 Or (Eq («$ki_accessible» «$ki_local_world» a) False) % 4.10/4.26 (Or (Eq («$ki_exists_in_world_$i» a a_1) False) % 4.10/4.26 (Or (Eq («$ki_exists_in_world_$i» a a_2) False) % 4.10/4.26 (Eq % 4.10/4.26 (∀ (W0 : «$ki_world»), % 4.10/4.26 «$ki_accessible» a W0 → % 4.10/4.26 And (And (closed W0 a_1) (combo W0 a_1 a_2)) (h W0 (skS.0 2 a a_1 a_2 a_3)) → % 4.10/4.26 ∀ (W1 : «$ki_world»), «$ki_accessible» W0 W1 → open W1 a_1) % 4.10/4.26 True))) % 4.10/4.26 Clause #81 (by clausification #[79]): ∀ (a : «$ki_world») (a_1 a_2 : Iota) (a_3 : «$ki_world») (a_4 : Iota), % 4.10/4.26 Or (Eq («$ki_accessible» «$ki_local_world» a) False) % 4.10/4.26 (Or (Eq («$ki_exists_in_world_$i» a a_1) False) % 4.10/4.26 (Or (Eq («$ki_exists_in_world_$i» a a_2) False) % 4.10/4.26 (Eq % 4.10/4.26 («$ki_accessible» a a_3 → % 4.10/4.26 And (And (closed a_3 a_1) (combo a_3 a_1 a_2)) (h a_3 (skS.0 2 a a_1 a_2 a_4)) → % 4.10/4.26 ∀ (W1 : «$ki_world»), «$ki_accessible» a_3 W1 → open W1 a_1) % 4.10/4.26 True))) % 4.10/4.26 Clause #82 (by clausification #[81]): ∀ (a : «$ki_world») (a_1 a_2 : Iota) (a_3 : «$ki_world») (a_4 : Iota), % 4.10/4.26 Or (Eq («$ki_accessible» «$ki_local_world» a) False) % 4.10/4.26 (Or (Eq («$ki_exists_in_world_$i» a a_1) False) % 4.10/4.26 (Or (Eq («$ki_exists_in_world_$i» a a_2) False) % 4.10/4.26 (Or (Eq («$ki_accessible» a a_3) False) % 4.10/4.26 (Eq % 4.10/4.26 (And (And (closed a_3 a_1) (combo a_3 a_1 a_2)) (h a_3 (skS.0 2 a a_1 a_2 a_4)) → % 4.10/4.26 ∀ (W1 : «$ki_world»), «$ki_accessible» a_3 W1 → open W1 a_1) % 4.10/4.26 True)))) % 4.10/4.26 Clause #83 (by clausification #[82]): ∀ (a : «$ki_world») (a_1 a_2 : Iota) (a_3 : «$ki_world») (a_4 : Iota), % 4.10/4.26 Or (Eq («$ki_accessible» «$ki_local_world» a) False) % 4.10/4.26 (Or (Eq («$ki_exists_in_world_$i» a a_1) False) % 4.10/4.26 (Or (Eq («$ki_exists_in_world_$i» a a_2) False) % 4.10/4.26 (Or (Eq («$ki_accessible» a a_3) False) % 4.10/4.26 (Or (Eq (And (And (closed a_3 a_1) (combo a_3 a_1 a_2)) (h a_3 (skS.0 2 a a_1 a_2 a_4))) False) % 4.10/4.26 (Eq (∀ (W1 : «$ki_world»), «$ki_accessible» a_3 W1 → open W1 a_1) True))))) % 4.10/4.26 Clause #84 (by clausification #[83]): ∀ (a : «$ki_world») (a_1 a_2 : Iota) (a_3 : «$ki_world») (a_4 : Iota), % 4.10/4.26 Or (Eq («$ki_accessible» «$ki_local_world» a) False) % 4.10/4.26 (Or (Eq («$ki_exists_in_world_$i» a a_1) False) % 4.10/4.26 (Or (Eq («$ki_exists_in_world_$i» a a_2) False) % 4.10/4.26 (Or (Eq («$ki_accessible» a a_3) False) % 4.10/4.26 (Or (Eq (∀ (W1 : «$ki_world»), «$ki_accessible» a_3 W1 → open W1 a_1) True) % 4.10/4.26 (Or (Eq (And (closed a_3 a_1) (combo a_3 a_1 a_2)) False) (Eq (h a_3 (skS.0 2 a a_1 a_2 a_4)) False)))))) % 4.10/4.28 Clause #85 (by clausification #[84]): ∀ (a : «$ki_world») (a_1 a_2 : Iota) (a_3 : «$ki_world») (a_4 : Iota) (a_5 : «$ki_world»), % 4.10/4.28 Or (Eq («$ki_accessible» «$ki_local_world» a) False) % 4.10/4.28 (Or (Eq («$ki_exists_in_world_$i» a a_1) False) % 4.10/4.28 (Or (Eq («$ki_exists_in_world_$i» a a_2) False) % 4.10/4.28 (Or (Eq («$ki_accessible» a a_3) False) % 4.10/4.28 (Or (Eq (And (closed a_3 a_1) (combo a_3 a_1 a_2)) False) % 4.10/4.28 (Or (Eq (h a_3 (skS.0 2 a a_1 a_2 a_4)) False) (Eq («$ki_accessible» a_3 a_5 → open a_5 a_1) True)))))) % 4.10/4.28 Clause #86 (by clausification #[85]): ∀ (a : «$ki_world») (a_1 a_2 : Iota) (a_3 : «$ki_world») (a_4 : Iota) (a_5 : «$ki_world»), % 4.10/4.28 Or (Eq («$ki_accessible» «$ki_local_world» a) False) % 4.10/4.28 (Or (Eq («$ki_exists_in_world_$i» a a_1) False) % 4.10/4.28 (Or (Eq («$ki_exists_in_world_$i» a a_2) False) % 4.10/4.28 (Or (Eq («$ki_accessible» a a_3) False) % 4.10/4.28 (Or (Eq (h a_3 (skS.0 2 a a_1 a_2 a_4)) False) % 4.10/4.28 (Or (Eq («$ki_accessible» a_3 a_5 → open a_5 a_1) True) % 4.10/4.28 (Or (Eq (closed a_3 a_1) False) (Eq (combo a_3 a_1 a_2) False))))))) % 4.10/4.28 Clause #87 (by clausification #[86]): ∀ (a : «$ki_world») (a_1 a_2 : Iota) (a_3 : «$ki_world») (a_4 : Iota) (a_5 : «$ki_world»), % 4.10/4.28 Or (Eq («$ki_accessible» «$ki_local_world» a) False) % 4.10/4.28 (Or (Eq («$ki_exists_in_world_$i» a a_1) False) % 4.10/4.28 (Or (Eq («$ki_exists_in_world_$i» a a_2) False) % 4.10/4.28 (Or (Eq («$ki_accessible» a a_3) False) % 4.10/4.28 (Or (Eq (h a_3 (skS.0 2 a a_1 a_2 a_4)) False) % 4.10/4.28 (Or (Eq (closed a_3 a_1) False) % 4.10/4.28 (Or (Eq (combo a_3 a_1 a_2) False) % 4.10/4.28 (Or (Eq («$ki_accessible» a_3 a_5) False) (Eq (open a_5 a_1) True)))))))) % 4.10/4.28 Clause #88 (by forward demodulation #[87, 16]): ∀ (a : «$ki_world») (a_1 : Iota) (a_2 : «$ki_world») (a_3 a_4 : Iota) (a_5 : «$ki_world»), % 4.10/4.28 Or (Eq («$ki_accessible» «$ki_local_world» a) False) % 4.10/4.28 (Or (Eq True False) % 4.10/4.28 (Or (Eq («$ki_exists_in_world_$i» a a_1) False) % 4.10/4.28 (Or (Eq («$ki_accessible» a a_2) False) % 4.10/4.28 (Or (Eq (h a_2 (skS.0 2 a a_3 a_1 a_4)) False) % 4.10/4.28 (Or (Eq (closed a_2 a_3) False) % 4.10/4.28 (Or (Eq (combo a_2 a_3 a_1) False) % 4.10/4.28 (Or (Eq («$ki_accessible» a_2 a_5) False) (Eq (open a_5 a_3) True)))))))) % 4.10/4.28 Clause #89 (by clausification #[88]): ∀ (a : «$ki_world») (a_1 : Iota) (a_2 : «$ki_world») (a_3 a_4 : Iota) (a_5 : «$ki_world»), % 4.10/4.28 Or (Eq («$ki_accessible» «$ki_local_world» a) False) % 4.10/4.28 (Or (Eq («$ki_exists_in_world_$i» a a_1) False) % 4.10/4.28 (Or (Eq («$ki_accessible» a a_2) False) % 4.10/4.28 (Or (Eq (h a_2 (skS.0 2 a a_3 a_1 a_4)) False) % 4.10/4.28 (Or (Eq (closed a_2 a_3) False) % 4.10/4.28 (Or (Eq (combo a_2 a_3 a_1) False) (Or (Eq («$ki_accessible» a_2 a_5) False) (Eq (open a_5 a_3) True))))))) % 4.10/4.28 Clause #90 (by forward demodulation #[89, 16]): ∀ (a a_1 : «$ki_world») (a_2 a_3 a_4 : Iota) (a_5 : «$ki_world»), % 4.10/4.28 Or (Eq («$ki_accessible» «$ki_local_world» a) False) % 4.10/4.28 (Or (Eq True False) % 4.10/4.28 (Or (Eq («$ki_accessible» a a_1) False) % 4.10/4.28 (Or (Eq (h a_1 (skS.0 2 a a_2 a_3 a_4)) False) % 4.10/4.28 (Or (Eq (closed a_1 a_2) False) % 4.10/4.28 (Or (Eq (combo a_1 a_2 a_3) False) (Or (Eq («$ki_accessible» a_1 a_5) False) (Eq (open a_5 a_2) True))))))) % 4.10/4.28 Clause #91 (by clausification #[90]): ∀ (a a_1 : «$ki_world») (a_2 a_3 a_4 : Iota) (a_5 : «$ki_world»), % 4.10/4.28 Or (Eq («$ki_accessible» «$ki_local_world» a) False) % 4.10/4.28 (Or (Eq («$ki_accessible» a a_1) False) % 4.10/4.28 (Or (Eq (h a_1 (skS.0 2 a a_2 a_3 a_4)) False) % 4.10/4.28 (Or (Eq (closed a_1 a_2) False) % 4.10/4.28 (Or (Eq (combo a_1 a_2 a_3) False) (Or (Eq («$ki_accessible» a_1 a_5) False) (Eq (open a_5 a_2) True)))))) % 4.10/4.28 Clause #93 (by superposition #[91, 10]): ∀ (a : «$ki_world») (a_1 a_2 a_3 : Iota) (a_4 : «$ki_world»), % 4.10/4.28 Or (Eq («$ki_accessible» «$ki_local_world» a) False) % 4.10/4.28 (Or (Eq (h a (skS.0 2 «$ki_local_world» a_1 a_2 a_3)) False) % 4.10/4.28 (Or (Eq (closed a a_1) False) % 4.10/4.28 (Or (Eq (combo a a_1 a_2) False) % 4.10/4.28 (Or (Eq («$ki_accessible» a a_4) False) (Or (Eq (open a_4 a_1) True) (Eq False True)))))) % 4.10/4.30 Clause #95 (by clausification #[72]): ∀ (a : «$ki_world») (a_1 : Iota), Or (Eq (open (skS.0 3 a) a_1) False) (Eq (closed (skS.0 3 a) a_1) False) % 4.10/4.30 Clause #100 (by clausification #[70]): ∀ (a : «$ki_world») (a_1 : Iota), % 4.10/4.30 Eq % 4.10/4.30 (And («$ki_exists_in_world_$i» (skS.0 3 a) a_1) % 4.10/4.30 (Exists fun O => % 4.10/4.30 And («$ki_exists_in_world_$i» (skS.0 3 a) O) % 4.10/4.30 ((∀ (W0 : «$ki_world»), «$ki_accessible» (skS.0 3 a) W0 → And (combo W0 d a_1) (h W0 O)) → % 4.10/4.30 ∀ (W0 : «$ki_world»), «$ki_accessible» (skS.0 3 a) W0 → open W0 d))) % 4.10/4.30 False % 4.10/4.30 Clause #101 (by clausification #[100]): ∀ (a : «$ki_world») (a_1 : Iota), % 4.10/4.30 Or (Eq («$ki_exists_in_world_$i» (skS.0 3 a) a_1) False) % 4.10/4.30 (Eq % 4.10/4.30 (Exists fun O => % 4.10/4.30 And («$ki_exists_in_world_$i» (skS.0 3 a) O) % 4.10/4.30 ((∀ (W0 : «$ki_world»), «$ki_accessible» (skS.0 3 a) W0 → And (combo W0 d a_1) (h W0 O)) → % 4.10/4.30 ∀ (W0 : «$ki_world»), «$ki_accessible» (skS.0 3 a) W0 → open W0 d)) % 4.10/4.30 False) % 4.10/4.30 Clause #102 (by clausification #[101]): ∀ (a : «$ki_world») (a_1 a_2 : Iota), % 4.10/4.30 Or (Eq («$ki_exists_in_world_$i» (skS.0 3 a) a_1) False) % 4.10/4.30 (Eq % 4.10/4.30 (And («$ki_exists_in_world_$i» (skS.0 3 a) a_2) % 4.10/4.30 ((∀ (W0 : «$ki_world»), «$ki_accessible» (skS.0 3 a) W0 → And (combo W0 d a_1) (h W0 a_2)) → % 4.10/4.30 ∀ (W0 : «$ki_world»), «$ki_accessible» (skS.0 3 a) W0 → open W0 d)) % 4.10/4.30 False) % 4.10/4.30 Clause #103 (by clausification #[102]): ∀ (a : «$ki_world») (a_1 a_2 : Iota), % 4.10/4.30 Or (Eq («$ki_exists_in_world_$i» (skS.0 3 a) a_1) False) % 4.10/4.30 (Or (Eq («$ki_exists_in_world_$i» (skS.0 3 a) a_2) False) % 4.10/4.30 (Eq % 4.10/4.30 ((∀ (W0 : «$ki_world»), «$ki_accessible» (skS.0 3 a) W0 → And (combo W0 d a_1) (h W0 a_2)) → % 4.10/4.30 ∀ (W0 : «$ki_world»), «$ki_accessible» (skS.0 3 a) W0 → open W0 d) % 4.10/4.30 False)) % 4.10/4.30 Clause #104 (by clausification #[103]): ∀ (a : «$ki_world») (a_1 a_2 : Iota), % 4.10/4.30 Or (Eq («$ki_exists_in_world_$i» (skS.0 3 a) a_1) False) % 4.10/4.30 (Or (Eq («$ki_exists_in_world_$i» (skS.0 3 a) a_2) False) % 4.10/4.30 (Eq (∀ (W0 : «$ki_world»), «$ki_accessible» (skS.0 3 a) W0 → And (combo W0 d a_1) (h W0 a_2)) True)) % 4.10/4.30 Clause #106 (by clausification #[104]): ∀ (a : «$ki_world») (a_1 a_2 : Iota) (a_3 : «$ki_world»), % 4.10/4.30 Or (Eq («$ki_exists_in_world_$i» (skS.0 3 a) a_1) False) % 4.10/4.30 (Or (Eq («$ki_exists_in_world_$i» (skS.0 3 a) a_2) False) % 4.10/4.30 (Eq («$ki_accessible» (skS.0 3 a) a_3 → And (combo a_3 d a_1) (h a_3 a_2)) True)) % 4.10/4.30 Clause #107 (by clausification #[106]): ∀ (a : «$ki_world») (a_1 a_2 : Iota) (a_3 : «$ki_world»), % 4.10/4.30 Or (Eq («$ki_exists_in_world_$i» (skS.0 3 a) a_1) False) % 4.10/4.30 (Or (Eq («$ki_exists_in_world_$i» (skS.0 3 a) a_2) False) % 4.10/4.30 (Or (Eq («$ki_accessible» (skS.0 3 a) a_3) False) (Eq (And (combo a_3 d a_1) (h a_3 a_2)) True))) % 4.10/4.30 Clause #108 (by clausification #[107]): ∀ (a : «$ki_world») (a_1 a_2 : Iota) (a_3 : «$ki_world»), % 4.10/4.30 Or (Eq («$ki_exists_in_world_$i» (skS.0 3 a) a_1) False) % 4.10/4.30 (Or (Eq («$ki_exists_in_world_$i» (skS.0 3 a) a_2) False) % 4.10/4.30 (Or (Eq («$ki_accessible» (skS.0 3 a) a_3) False) (Eq (h a_3 a_2) True))) % 4.10/4.30 Clause #109 (by clausification #[107]): ∀ (a : «$ki_world») (a_1 a_2 : Iota) (a_3 : «$ki_world»), % 4.10/4.30 Or (Eq («$ki_exists_in_world_$i» (skS.0 3 a) a_1) False) % 4.10/4.30 (Or (Eq («$ki_exists_in_world_$i» (skS.0 3 a) a_2) False) % 4.10/4.30 (Or (Eq («$ki_accessible» (skS.0 3 a) a_3) False) (Eq (combo a_3 d a_1) True))) % 4.10/4.30 Clause #110 (by superposition #[108, 16]): ∀ (a : «$ki_world») (a_1 : Iota) (a_2 : «$ki_world»), % 4.10/4.30 Or (Eq («$ki_exists_in_world_$i» (skS.0 3 a) a_1) False) % 4.10/4.30 (Or (Eq («$ki_accessible» (skS.0 3 a) a_2) False) (Or (Eq (h a_2 a_1) True) (Eq False True))) % 4.10/4.30 Clause #119 (by clausification #[110]): ∀ (a : «$ki_world») (a_1 : Iota) (a_2 : «$ki_world»), % 4.10/4.30 Or (Eq («$ki_exists_in_world_$i» (skS.0 3 a) a_1) False) % 4.10/4.30 (Or (Eq («$ki_accessible» (skS.0 3 a) a_2) False) (Eq (h a_2 a_1) True)) % 4.10/4.30 Clause #120 (by superposition #[119, 16]): ∀ (a a_1 : «$ki_world») (a_2 : Iota), % 4.16/4.32 Or (Eq («$ki_accessible» (skS.0 3 a) a_1) False) (Or (Eq (h a_1 a_2) True) (Eq False True)) % 4.16/4.32 Clause #121 (by clausification #[120]): ∀ (a a_1 : «$ki_world») (a_2 : Iota), Or (Eq («$ki_accessible» (skS.0 3 a) a_1) False) (Eq (h a_1 a_2) True) % 4.16/4.32 Clause #122 (by superposition #[121, 10]): ∀ (a : «$ki_world») (a_1 : Iota), Or (Eq (h (skS.0 3 a) a_1) True) (Eq False True) % 4.16/4.32 Clause #123 (by clausification #[122]): ∀ (a : «$ki_world») (a_1 : Iota), Eq (h (skS.0 3 a) a_1) True % 4.16/4.32 Clause #155 (by clausification #[93]): ∀ (a : «$ki_world») (a_1 a_2 a_3 : Iota) (a_4 : «$ki_world»), % 4.16/4.32 Or (Eq («$ki_accessible» «$ki_local_world» a) False) % 4.16/4.32 (Or (Eq (h a (skS.0 2 «$ki_local_world» a_1 a_2 a_3)) False) % 4.16/4.32 (Or (Eq (closed a a_1) False) % 4.16/4.32 (Or (Eq (combo a a_1 a_2) False) (Or (Eq («$ki_accessible» a a_4) False) (Eq (open a_4 a_1) True))))) % 4.16/4.32 Clause #156 (by superposition #[155, 69]): ∀ (a : «$ki_world») (a_1 a_2 a_3 : Iota) (a_4 : «$ki_world»), % 4.16/4.32 Or (Eq (h (skS.0 3 a) (skS.0 2 «$ki_local_world» a_1 a_2 a_3)) False) % 4.16/4.32 (Or (Eq (closed (skS.0 3 a) a_1) False) % 4.16/4.32 (Or (Eq (combo (skS.0 3 a) a_1 a_2) False) % 4.16/4.32 (Or (Eq («$ki_accessible» (skS.0 3 a) a_4) False) (Or (Eq (open a_4 a_1) True) (Eq False True))))) % 4.16/4.32 Clause #163 (by superposition #[109, 16]): ∀ (a : «$ki_world») (a_1 : Iota) (a_2 : «$ki_world») (a_3 : Iota), % 4.16/4.32 Or (Eq («$ki_exists_in_world_$i» (skS.0 3 a) a_1) False) % 4.16/4.32 (Or (Eq («$ki_accessible» (skS.0 3 a) a_2) False) (Or (Eq (combo a_2 d a_3) True) (Eq False True))) % 4.16/4.32 Clause #164 (by clausification #[163]): ∀ (a : «$ki_world») (a_1 : Iota) (a_2 : «$ki_world») (a_3 : Iota), % 4.16/4.32 Or (Eq («$ki_exists_in_world_$i» (skS.0 3 a) a_1) False) % 4.16/4.32 (Or (Eq («$ki_accessible» (skS.0 3 a) a_2) False) (Eq (combo a_2 d a_3) True)) % 4.16/4.32 Clause #165 (by superposition #[164, 16]): ∀ (a a_1 : «$ki_world») (a_2 : Iota), % 4.16/4.32 Or (Eq («$ki_accessible» (skS.0 3 a) a_1) False) (Or (Eq (combo a_1 d a_2) True) (Eq False True)) % 4.16/4.32 Clause #170 (by clausification #[165]): ∀ (a a_1 : «$ki_world») (a_2 : Iota), Or (Eq («$ki_accessible» (skS.0 3 a) a_1) False) (Eq (combo a_1 d a_2) True) % 4.16/4.32 Clause #172 (by superposition #[170, 10]): ∀ (a : «$ki_world») (a_1 : Iota), Or (Eq (combo (skS.0 3 a) d a_1) True) (Eq False True) % 4.16/4.32 Clause #173 (by clausification #[172]): ∀ (a : «$ki_world») (a_1 : Iota), Eq (combo (skS.0 3 a) d a_1) True % 4.16/4.32 Clause #193 (by clausification #[156]): ∀ (a : «$ki_world») (a_1 a_2 a_3 : Iota) (a_4 : «$ki_world»), % 4.16/4.32 Or (Eq (h (skS.0 3 a) (skS.0 2 «$ki_local_world» a_1 a_2 a_3)) False) % 4.16/4.32 (Or (Eq (closed (skS.0 3 a) a_1) False) % 4.16/4.32 (Or (Eq (combo (skS.0 3 a) a_1 a_2) False) % 4.16/4.32 (Or (Eq («$ki_accessible» (skS.0 3 a) a_4) False) (Eq (open a_4 a_1) True)))) % 4.16/4.32 Clause #194 (by superposition #[193, 123]): ∀ (a : «$ki_world») (a_1 a_2 : Iota) (a_3 : «$ki_world»), % 4.16/4.32 Or (Eq (closed (skS.0 3 a) a_1) False) % 4.16/4.32 (Or (Eq (combo (skS.0 3 a) a_1 a_2) False) % 4.16/4.32 (Or (Eq («$ki_accessible» (skS.0 3 a) a_3) False) (Or (Eq (open a_3 a_1) True) (Eq False True)))) % 4.16/4.32 Clause #195 (by clausification #[194]): ∀ (a : «$ki_world») (a_1 a_2 : Iota) (a_3 : «$ki_world»), % 4.16/4.32 Or (Eq (closed (skS.0 3 a) a_1) False) % 4.16/4.32 (Or (Eq (combo (skS.0 3 a) a_1 a_2) False) % 4.16/4.32 (Or (Eq («$ki_accessible» (skS.0 3 a) a_3) False) (Eq (open a_3 a_1) True))) % 4.16/4.32 Clause #196 (by superposition #[195, 76]): ∀ (a : «$ki_world») (a_1 : Iota) (a_2 : «$ki_world»), % 4.16/4.32 Or (Eq (combo (skS.0 3 a) d a_1) False) % 4.16/4.32 (Or (Eq («$ki_accessible» (skS.0 3 a) a_2) False) (Or (Eq (open a_2 d) True) (Eq False True))) % 4.16/4.32 Clause #197 (by clausification #[196]): ∀ (a : «$ki_world») (a_1 : Iota) (a_2 : «$ki_world»), % 4.16/4.32 Or (Eq (combo (skS.0 3 a) d a_1) False) (Or (Eq («$ki_accessible» (skS.0 3 a) a_2) False) (Eq (open a_2 d) True)) % 4.16/4.32 Clause #198 (by superposition #[197, 173]): ∀ (a a_1 : «$ki_world»), Or (Eq («$ki_accessible» (skS.0 3 a) a_1) False) (Or (Eq (open a_1 d) True) (Eq False True)) % 4.16/4.32 Clause #201 (by clausification #[198]): ∀ (a a_1 : «$ki_world»), Or (Eq («$ki_accessible» (skS.0 3 a) a_1) False) (Eq (open a_1 d) True) % 4.16/4.32 Clause #203 (by superposition #[201, 10]): ∀ (a : «$ki_world»), Or (Eq (open (skS.0 3 a) d) True) (Eq False True) % 4.16/4.32 Clause #204 (by clausification #[203]): ∀ (a : «$ki_world»), Eq (open (skS.0 3 a) d) True % 4.16/4.32 Clause #205 (by superposition #[204, 95]): ∀ (a : «$ki_world»), Or (Eq True False) (Eq (closed (skS.0 3 a) d) False) % 4.16/4.32 Clause #206 (by clausification #[205]): ∀ (a : «$ki_world»), Eq (closed (skS.0 3 a) d) False % 4.16/4.32 Clause #207 (by superposition #[206, 76]): Eq False True % 4.16/4.32 Clause #208 (by clausification #[207]): False % 4.16/4.32 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------