%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : TOP028+1 : TPTP v9.2.0. Released v3.4.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n008.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 300s % DateTime : Fri Oct 3 08:09:54 PM UTC 2025 % Result : Theorem 29.56s 29.77s % Output : Proof 29.72s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : TOP028+1 : TPTP v9.2.0. Released v3.4.0. % 0.07/0.13 % Command : duper %s % 0.13/0.35 % Computer : n008.cluster.edu % 0.13/0.35 % Model : x86_64 x86_64 % 0.13/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.35 % Memory : 8042.1875MB % 0.13/0.35 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.35 % CPULimit : 300 % 0.13/0.35 % WCLimit : 300 % 0.13/0.35 % DateTime : Fri Oct 3 01:55:08 EDT 2025 % 0.13/0.35 % CPUTime : % 29.56/29.77 SZS status Theorem for theBenchmark.p % 29.56/29.77 SZS output start Proof for theBenchmark.p % 29.56/29.77 Clause #0 (by assumption #[]): Eq % 29.56/29.77 (Not % 29.56/29.77 (∀ (A : Iota), % 29.56/29.77 And (And (Not (v3_struct_0 A)) (v2_pre_topc A)) (l1_pre_topc A) → % 29.56/29.77 Exists fun B => And (m1_subset_1 B (k1_zfmisc_1 (u1_struct_0 A))) (v1_tsp_2 B A))) % 29.56/29.77 True % 29.56/29.77 Clause #38 (by assumption #[]): Eq (∀ (A : Iota), Exists fun B => And (m1_subset_1 B (k1_zfmisc_1 A)) (v1_xboole_0 B)) True % 29.56/29.77 Clause #48 (by assumption #[]): Eq % 29.56/29.77 (∀ (A : Iota), % 29.56/29.77 And (Not (v3_struct_0 A)) (l1_pre_topc A) → % 29.56/29.77 ∀ (B : Iota), m1_subset_1 B (k1_zfmisc_1 (u1_struct_0 A)) → v3_tex_2 B A → v1_tsp_1 B A) % 29.56/29.77 True % 29.56/29.77 Clause #51 (by assumption #[]): Eq % 29.56/29.77 (∀ (A : Iota), % 29.56/29.77 And (And (Not (v3_struct_0 A)) (v2_pre_topc A)) (l1_pre_topc A) → % 29.56/29.77 ∀ (B : Iota), And (v1_xboole_0 B) (m1_subset_1 B (k1_zfmisc_1 (u1_struct_0 A))) → v3_tex_2 B A) % 29.56/29.77 True % 29.56/29.77 Clause #55 (by assumption #[]): Eq (∀ (A : Iota), v1_xboole_0 A → Eq A k1_xboole_0) True % 29.56/29.77 Clause #58 (by assumption #[]): Eq % 29.56/29.77 (∀ (A : Iota), % 29.56/29.77 And (And (Not (v3_struct_0 A)) (v2_pre_topc A)) (l1_pre_topc A) → % 29.56/29.77 ∀ (B : Iota), % 29.56/29.77 m1_subset_1 B (k1_zfmisc_1 (u1_struct_0 A)) → % 29.56/29.77 Not % 29.56/29.77 (And (v1_tsp_1 B A) % 29.56/29.77 (∀ (C : Iota), m1_subset_1 C (k1_zfmisc_1 (u1_struct_0 A)) → Not (And (r1_tarski B C) (v1_tsp_2 C A))))) % 29.56/29.77 True % 29.56/29.77 Clause #67 (by clausification #[0]): Eq % 29.56/29.77 (∀ (A : Iota), % 29.56/29.77 And (And (Not (v3_struct_0 A)) (v2_pre_topc A)) (l1_pre_topc A) → % 29.56/29.77 Exists fun B => And (m1_subset_1 B (k1_zfmisc_1 (u1_struct_0 A))) (v1_tsp_2 B A)) % 29.56/29.77 False % 29.56/29.77 Clause #68 (by clausification #[67]): ∀ (a : Iota), % 29.56/29.77 Eq % 29.56/29.77 (Not % 29.56/29.77 (And (And (Not (v3_struct_0 (skS.0 0 a))) (v2_pre_topc (skS.0 0 a))) (l1_pre_topc (skS.0 0 a)) → % 29.56/29.77 Exists fun B => And (m1_subset_1 B (k1_zfmisc_1 (u1_struct_0 (skS.0 0 a)))) (v1_tsp_2 B (skS.0 0 a)))) % 29.56/29.77 True % 29.56/29.77 Clause #69 (by clausification #[68]): ∀ (a : Iota), % 29.56/29.77 Eq % 29.56/29.77 (And (And (Not (v3_struct_0 (skS.0 0 a))) (v2_pre_topc (skS.0 0 a))) (l1_pre_topc (skS.0 0 a)) → % 29.56/29.77 Exists fun B => And (m1_subset_1 B (k1_zfmisc_1 (u1_struct_0 (skS.0 0 a)))) (v1_tsp_2 B (skS.0 0 a))) % 29.56/29.77 False % 29.56/29.77 Clause #70 (by clausification #[69]): ∀ (a : Iota), Eq (And (And (Not (v3_struct_0 (skS.0 0 a))) (v2_pre_topc (skS.0 0 a))) (l1_pre_topc (skS.0 0 a))) True % 29.56/29.77 Clause #71 (by clausification #[69]): ∀ (a : Iota), % 29.56/29.77 Eq (Exists fun B => And (m1_subset_1 B (k1_zfmisc_1 (u1_struct_0 (skS.0 0 a)))) (v1_tsp_2 B (skS.0 0 a))) False % 29.56/29.77 Clause #72 (by clausification #[70]): ∀ (a : Iota), Eq (l1_pre_topc (skS.0 0 a)) True % 29.56/29.77 Clause #73 (by clausification #[70]): ∀ (a : Iota), Eq (And (Not (v3_struct_0 (skS.0 0 a))) (v2_pre_topc (skS.0 0 a))) True % 29.56/29.77 Clause #96 (by clausification #[55]): ∀ (a : Iota), Eq (v1_xboole_0 a → Eq a k1_xboole_0) True % 29.56/29.77 Clause #97 (by clausification #[96]): ∀ (a : Iota), Or (Eq (v1_xboole_0 a) False) (Eq (Eq a k1_xboole_0) True) % 29.56/29.77 Clause #98 (by clausification #[97]): ∀ (a : Iota), Or (Eq (v1_xboole_0 a) False) (Eq a k1_xboole_0) % 29.56/29.77 Clause #123 (by clausification #[51]): ∀ (a : Iota), % 29.56/29.77 Eq % 29.56/29.77 (And (And (Not (v3_struct_0 a)) (v2_pre_topc a)) (l1_pre_topc a) → % 29.56/29.77 ∀ (B : Iota), And (v1_xboole_0 B) (m1_subset_1 B (k1_zfmisc_1 (u1_struct_0 a))) → v3_tex_2 B a) % 29.56/29.77 True % 29.56/29.77 Clause #124 (by clausification #[123]): ∀ (a : Iota), % 29.56/29.77 Or (Eq (And (And (Not (v3_struct_0 a)) (v2_pre_topc a)) (l1_pre_topc a)) False) % 29.56/29.77 (Eq (∀ (B : Iota), And (v1_xboole_0 B) (m1_subset_1 B (k1_zfmisc_1 (u1_struct_0 a))) → v3_tex_2 B a) True) % 29.56/29.77 Clause #125 (by clausification #[124]): ∀ (a : Iota), % 29.56/29.77 Or (Eq (∀ (B : Iota), And (v1_xboole_0 B) (m1_subset_1 B (k1_zfmisc_1 (u1_struct_0 a))) → v3_tex_2 B a) True) % 29.56/29.77 (Or (Eq (And (Not (v3_struct_0 a)) (v2_pre_topc a)) False) (Eq (l1_pre_topc a) False)) % 29.56/29.77 Clause #126 (by clausification #[125]): ∀ (a a_1 : Iota), % 29.56/29.77 Or (Eq (And (Not (v3_struct_0 a)) (v2_pre_topc a)) False) % 29.56/29.77 (Or (Eq (l1_pre_topc a) False) % 29.56/29.77 (Eq (And (v1_xboole_0 a_1) (m1_subset_1 a_1 (k1_zfmisc_1 (u1_struct_0 a))) → v3_tex_2 a_1 a) True)) % 29.56/29.77 Clause #127 (by clausification #[126]): ∀ (a a_1 : Iota), % 29.56/29.79 Or (Eq (l1_pre_topc a) False) % 29.56/29.79 (Or (Eq (And (v1_xboole_0 a_1) (m1_subset_1 a_1 (k1_zfmisc_1 (u1_struct_0 a))) → v3_tex_2 a_1 a) True) % 29.56/29.79 (Or (Eq (Not (v3_struct_0 a)) False) (Eq (v2_pre_topc a) False))) % 29.56/29.79 Clause #128 (by clausification #[127]): ∀ (a a_1 : Iota), % 29.56/29.79 Or (Eq (l1_pre_topc a) False) % 29.56/29.79 (Or (Eq (Not (v3_struct_0 a)) False) % 29.56/29.79 (Or (Eq (v2_pre_topc a) False) % 29.56/29.79 (Or (Eq (And (v1_xboole_0 a_1) (m1_subset_1 a_1 (k1_zfmisc_1 (u1_struct_0 a)))) False) % 29.56/29.79 (Eq (v3_tex_2 a_1 a) True)))) % 29.56/29.79 Clause #129 (by clausification #[128]): ∀ (a a_1 : Iota), % 29.56/29.79 Or (Eq (l1_pre_topc a) False) % 29.56/29.79 (Or (Eq (v2_pre_topc a) False) % 29.56/29.79 (Or (Eq (And (v1_xboole_0 a_1) (m1_subset_1 a_1 (k1_zfmisc_1 (u1_struct_0 a)))) False) % 29.56/29.79 (Or (Eq (v3_tex_2 a_1 a) True) (Eq (v3_struct_0 a) True)))) % 29.56/29.79 Clause #130 (by clausification #[129]): ∀ (a a_1 : Iota), % 29.56/29.79 Or (Eq (l1_pre_topc a) False) % 29.56/29.79 (Or (Eq (v2_pre_topc a) False) % 29.56/29.79 (Or (Eq (v3_tex_2 a_1 a) True) % 29.56/29.79 (Or (Eq (v3_struct_0 a) True) % 29.56/29.79 (Or (Eq (v1_xboole_0 a_1) False) (Eq (m1_subset_1 a_1 (k1_zfmisc_1 (u1_struct_0 a))) False))))) % 29.56/29.79 Clause #131 (by superposition #[130, 72]): ∀ (a a_1 : Iota), % 29.56/29.79 Or (Eq (v2_pre_topc (skS.0 0 a)) False) % 29.56/29.79 (Or (Eq (v3_tex_2 a_1 (skS.0 0 a)) True) % 29.56/29.79 (Or (Eq (v3_struct_0 (skS.0 0 a)) True) % 29.56/29.79 (Or (Eq (v1_xboole_0 a_1) False) % 29.56/29.79 (Or (Eq (m1_subset_1 a_1 (k1_zfmisc_1 (u1_struct_0 (skS.0 0 a)))) False) (Eq False True))))) % 29.56/29.79 Clause #161 (by clausification #[48]): ∀ (a : Iota), % 29.56/29.79 Eq % 29.56/29.79 (And (Not (v3_struct_0 a)) (l1_pre_topc a) → % 29.56/29.79 ∀ (B : Iota), m1_subset_1 B (k1_zfmisc_1 (u1_struct_0 a)) → v3_tex_2 B a → v1_tsp_1 B a) % 29.56/29.79 True % 29.56/29.79 Clause #162 (by clausification #[161]): ∀ (a : Iota), % 29.56/29.79 Or (Eq (And (Not (v3_struct_0 a)) (l1_pre_topc a)) False) % 29.56/29.79 (Eq (∀ (B : Iota), m1_subset_1 B (k1_zfmisc_1 (u1_struct_0 a)) → v3_tex_2 B a → v1_tsp_1 B a) True) % 29.56/29.79 Clause #163 (by clausification #[162]): ∀ (a : Iota), % 29.56/29.79 Or (Eq (∀ (B : Iota), m1_subset_1 B (k1_zfmisc_1 (u1_struct_0 a)) → v3_tex_2 B a → v1_tsp_1 B a) True) % 29.56/29.79 (Or (Eq (Not (v3_struct_0 a)) False) (Eq (l1_pre_topc a) False)) % 29.56/29.79 Clause #164 (by clausification #[163]): ∀ (a a_1 : Iota), % 29.56/29.79 Or (Eq (Not (v3_struct_0 a)) False) % 29.56/29.79 (Or (Eq (l1_pre_topc a) False) % 29.56/29.79 (Eq (m1_subset_1 a_1 (k1_zfmisc_1 (u1_struct_0 a)) → v3_tex_2 a_1 a → v1_tsp_1 a_1 a) True)) % 29.56/29.79 Clause #165 (by clausification #[164]): ∀ (a a_1 : Iota), % 29.56/29.79 Or (Eq (l1_pre_topc a) False) % 29.56/29.79 (Or (Eq (m1_subset_1 a_1 (k1_zfmisc_1 (u1_struct_0 a)) → v3_tex_2 a_1 a → v1_tsp_1 a_1 a) True) % 29.56/29.79 (Eq (v3_struct_0 a) True)) % 29.56/29.79 Clause #166 (by clausification #[165]): ∀ (a a_1 : Iota), % 29.56/29.79 Or (Eq (l1_pre_topc a) False) % 29.56/29.79 (Or (Eq (v3_struct_0 a) True) % 29.56/29.79 (Or (Eq (m1_subset_1 a_1 (k1_zfmisc_1 (u1_struct_0 a))) False) (Eq (v3_tex_2 a_1 a → v1_tsp_1 a_1 a) True))) % 29.56/29.79 Clause #167 (by clausification #[166]): ∀ (a a_1 : Iota), % 29.56/29.79 Or (Eq (l1_pre_topc a) False) % 29.56/29.79 (Or (Eq (v3_struct_0 a) True) % 29.56/29.79 (Or (Eq (m1_subset_1 a_1 (k1_zfmisc_1 (u1_struct_0 a))) False) % 29.56/29.79 (Or (Eq (v3_tex_2 a_1 a) False) (Eq (v1_tsp_1 a_1 a) True)))) % 29.56/29.79 Clause #168 (by superposition #[167, 72]): ∀ (a a_1 : Iota), % 29.56/29.79 Or (Eq (v3_struct_0 (skS.0 0 a)) True) % 29.56/29.79 (Or (Eq (m1_subset_1 a_1 (k1_zfmisc_1 (u1_struct_0 (skS.0 0 a)))) False) % 29.56/29.79 (Or (Eq (v3_tex_2 a_1 (skS.0 0 a)) False) (Or (Eq (v1_tsp_1 a_1 (skS.0 0 a)) True) (Eq False True)))) % 29.56/29.79 Clause #238 (by clausification #[38]): ∀ (a : Iota), Eq (Exists fun B => And (m1_subset_1 B (k1_zfmisc_1 a)) (v1_xboole_0 B)) True % 29.56/29.79 Clause #239 (by clausification #[238]): ∀ (a a_1 : Iota), Eq (And (m1_subset_1 (skS.0 5 a a_1) (k1_zfmisc_1 a)) (v1_xboole_0 (skS.0 5 a a_1))) True % 29.56/29.79 Clause #240 (by clausification #[239]): ∀ (a a_1 : Iota), Eq (v1_xboole_0 (skS.0 5 a a_1)) True % 29.56/29.79 Clause #241 (by clausification #[239]): ∀ (a a_1 : Iota), Eq (m1_subset_1 (skS.0 5 a a_1) (k1_zfmisc_1 a)) True % 29.56/29.79 Clause #242 (by superposition #[240, 98]): ∀ (a a_1 : Iota), Or (Eq True False) (Eq (skS.0 5 a a_1) k1_xboole_0) % 29.56/29.79 Clause #244 (by clausification #[242]): ∀ (a a_1 : Iota), Eq (skS.0 5 a a_1) k1_xboole_0 % 29.63/29.81 Clause #245 (by backward demodulation #[244, 240]): Eq (v1_xboole_0 k1_xboole_0) True % 29.63/29.81 Clause #314 (by forward demodulation #[241, 244]): ∀ (a : Iota), Eq (m1_subset_1 k1_xboole_0 (k1_zfmisc_1 a)) True % 29.63/29.81 Clause #633 (by clausification #[58]): ∀ (a : Iota), % 29.63/29.81 Eq % 29.63/29.81 (And (And (Not (v3_struct_0 a)) (v2_pre_topc a)) (l1_pre_topc a) → % 29.63/29.81 ∀ (B : Iota), % 29.63/29.81 m1_subset_1 B (k1_zfmisc_1 (u1_struct_0 a)) → % 29.63/29.81 Not % 29.63/29.81 (And (v1_tsp_1 B a) % 29.63/29.81 (∀ (C : Iota), m1_subset_1 C (k1_zfmisc_1 (u1_struct_0 a)) → Not (And (r1_tarski B C) (v1_tsp_2 C a))))) % 29.63/29.81 True % 29.63/29.81 Clause #634 (by clausification #[633]): ∀ (a : Iota), % 29.63/29.81 Or (Eq (And (And (Not (v3_struct_0 a)) (v2_pre_topc a)) (l1_pre_topc a)) False) % 29.63/29.81 (Eq % 29.63/29.81 (∀ (B : Iota), % 29.63/29.81 m1_subset_1 B (k1_zfmisc_1 (u1_struct_0 a)) → % 29.63/29.81 Not % 29.63/29.81 (And (v1_tsp_1 B a) % 29.63/29.81 (∀ (C : Iota), m1_subset_1 C (k1_zfmisc_1 (u1_struct_0 a)) → Not (And (r1_tarski B C) (v1_tsp_2 C a))))) % 29.63/29.81 True) % 29.63/29.81 Clause #635 (by clausification #[634]): ∀ (a : Iota), % 29.63/29.81 Or % 29.63/29.81 (Eq % 29.63/29.81 (∀ (B : Iota), % 29.63/29.81 m1_subset_1 B (k1_zfmisc_1 (u1_struct_0 a)) → % 29.63/29.81 Not % 29.63/29.81 (And (v1_tsp_1 B a) % 29.63/29.81 (∀ (C : Iota), m1_subset_1 C (k1_zfmisc_1 (u1_struct_0 a)) → Not (And (r1_tarski B C) (v1_tsp_2 C a))))) % 29.63/29.81 True) % 29.63/29.81 (Or (Eq (And (Not (v3_struct_0 a)) (v2_pre_topc a)) False) (Eq (l1_pre_topc a) False)) % 29.63/29.81 Clause #636 (by clausification #[635]): ∀ (a a_1 : Iota), % 29.63/29.81 Or (Eq (And (Not (v3_struct_0 a)) (v2_pre_topc a)) False) % 29.63/29.81 (Or (Eq (l1_pre_topc a) False) % 29.63/29.81 (Eq % 29.63/29.81 (m1_subset_1 a_1 (k1_zfmisc_1 (u1_struct_0 a)) → % 29.63/29.81 Not % 29.63/29.81 (And (v1_tsp_1 a_1 a) % 29.63/29.81 (∀ (C : Iota), m1_subset_1 C (k1_zfmisc_1 (u1_struct_0 a)) → Not (And (r1_tarski a_1 C) (v1_tsp_2 C a))))) % 29.63/29.81 True)) % 29.63/29.81 Clause #637 (by clausification #[636]): ∀ (a a_1 : Iota), % 29.63/29.81 Or (Eq (l1_pre_topc a) False) % 29.63/29.81 (Or % 29.63/29.81 (Eq % 29.63/29.81 (m1_subset_1 a_1 (k1_zfmisc_1 (u1_struct_0 a)) → % 29.63/29.81 Not % 29.63/29.81 (And (v1_tsp_1 a_1 a) % 29.63/29.81 (∀ (C : Iota), m1_subset_1 C (k1_zfmisc_1 (u1_struct_0 a)) → Not (And (r1_tarski a_1 C) (v1_tsp_2 C a))))) % 29.63/29.81 True) % 29.63/29.81 (Or (Eq (Not (v3_struct_0 a)) False) (Eq (v2_pre_topc a) False))) % 29.63/29.81 Clause #638 (by clausification #[637]): ∀ (a a_1 : Iota), % 29.63/29.81 Or (Eq (l1_pre_topc a) False) % 29.63/29.81 (Or (Eq (Not (v3_struct_0 a)) False) % 29.63/29.81 (Or (Eq (v2_pre_topc a) False) % 29.63/29.81 (Or (Eq (m1_subset_1 a_1 (k1_zfmisc_1 (u1_struct_0 a))) False) % 29.63/29.81 (Eq % 29.63/29.81 (Not % 29.63/29.81 (And (v1_tsp_1 a_1 a) % 29.63/29.81 (∀ (C : Iota), % 29.63/29.81 m1_subset_1 C (k1_zfmisc_1 (u1_struct_0 a)) → Not (And (r1_tarski a_1 C) (v1_tsp_2 C a))))) % 29.63/29.81 True)))) % 29.63/29.81 Clause #639 (by clausification #[638]): ∀ (a a_1 : Iota), % 29.63/29.81 Or (Eq (l1_pre_topc a) False) % 29.63/29.81 (Or (Eq (v2_pre_topc a) False) % 29.63/29.81 (Or (Eq (m1_subset_1 a_1 (k1_zfmisc_1 (u1_struct_0 a))) False) % 29.63/29.81 (Or % 29.63/29.81 (Eq % 29.63/29.81 (Not % 29.63/29.81 (And (v1_tsp_1 a_1 a) % 29.63/29.81 (∀ (C : Iota), % 29.63/29.81 m1_subset_1 C (k1_zfmisc_1 (u1_struct_0 a)) → Not (And (r1_tarski a_1 C) (v1_tsp_2 C a))))) % 29.63/29.81 True) % 29.63/29.81 (Eq (v3_struct_0 a) True)))) % 29.63/29.81 Clause #640 (by clausification #[639]): ∀ (a a_1 : Iota), % 29.63/29.81 Or (Eq (l1_pre_topc a) False) % 29.63/29.81 (Or (Eq (v2_pre_topc a) False) % 29.63/29.81 (Or (Eq (m1_subset_1 a_1 (k1_zfmisc_1 (u1_struct_0 a))) False) % 29.63/29.81 (Or (Eq (v3_struct_0 a) True) % 29.63/29.81 (Eq % 29.63/29.81 (And (v1_tsp_1 a_1 a) % 29.63/29.81 (∀ (C : Iota), m1_subset_1 C (k1_zfmisc_1 (u1_struct_0 a)) → Not (And (r1_tarski a_1 C) (v1_tsp_2 C a)))) % 29.63/29.81 False)))) % 29.63/29.81 Clause #641 (by clausification #[640]): ∀ (a a_1 : Iota), % 29.63/29.81 Or (Eq (l1_pre_topc a) False) % 29.63/29.81 (Or (Eq (v2_pre_topc a) False) % 29.63/29.81 (Or (Eq (m1_subset_1 a_1 (k1_zfmisc_1 (u1_struct_0 a))) False) % 29.63/29.81 (Or (Eq (v3_struct_0 a) True) % 29.63/29.81 (Or (Eq (v1_tsp_1 a_1 a) False) % 29.63/29.81 (Eq (∀ (C : Iota), m1_subset_1 C (k1_zfmisc_1 (u1_struct_0 a)) → Not (And (r1_tarski a_1 C) (v1_tsp_2 C a))) % 29.63/29.81 False))))) % 29.63/29.81 Clause #642 (by clausification #[641]): ∀ (a a_1 a_2 : Iota), % 29.63/29.83 Or (Eq (l1_pre_topc a) False) % 29.63/29.83 (Or (Eq (v2_pre_topc a) False) % 29.63/29.83 (Or (Eq (m1_subset_1 a_1 (k1_zfmisc_1 (u1_struct_0 a))) False) % 29.63/29.83 (Or (Eq (v3_struct_0 a) True) % 29.63/29.83 (Or (Eq (v1_tsp_1 a_1 a) False) % 29.63/29.83 (Eq % 29.63/29.83 (Not % 29.63/29.83 (m1_subset_1 (skS.0 16 a a_1 a_2) (k1_zfmisc_1 (u1_struct_0 a)) → % 29.63/29.83 Not (And (r1_tarski a_1 (skS.0 16 a a_1 a_2)) (v1_tsp_2 (skS.0 16 a a_1 a_2) a)))) % 29.63/29.83 True))))) % 29.63/29.83 Clause #643 (by clausification #[642]): ∀ (a a_1 a_2 : Iota), % 29.63/29.83 Or (Eq (l1_pre_topc a) False) % 29.63/29.83 (Or (Eq (v2_pre_topc a) False) % 29.63/29.83 (Or (Eq (m1_subset_1 a_1 (k1_zfmisc_1 (u1_struct_0 a))) False) % 29.63/29.83 (Or (Eq (v3_struct_0 a) True) % 29.63/29.83 (Or (Eq (v1_tsp_1 a_1 a) False) % 29.63/29.83 (Eq % 29.63/29.83 (m1_subset_1 (skS.0 16 a a_1 a_2) (k1_zfmisc_1 (u1_struct_0 a)) → % 29.63/29.83 Not (And (r1_tarski a_1 (skS.0 16 a a_1 a_2)) (v1_tsp_2 (skS.0 16 a a_1 a_2) a))) % 29.63/29.83 False))))) % 29.63/29.83 Clause #644 (by clausification #[643]): ∀ (a a_1 a_2 : Iota), % 29.63/29.83 Or (Eq (l1_pre_topc a) False) % 29.63/29.83 (Or (Eq (v2_pre_topc a) False) % 29.63/29.83 (Or (Eq (m1_subset_1 a_1 (k1_zfmisc_1 (u1_struct_0 a))) False) % 29.63/29.83 (Or (Eq (v3_struct_0 a) True) % 29.63/29.83 (Or (Eq (v1_tsp_1 a_1 a) False) (Eq (m1_subset_1 (skS.0 16 a a_1 a_2) (k1_zfmisc_1 (u1_struct_0 a))) True))))) % 29.63/29.83 Clause #645 (by clausification #[643]): ∀ (a a_1 a_2 : Iota), % 29.63/29.83 Or (Eq (l1_pre_topc a) False) % 29.63/29.83 (Or (Eq (v2_pre_topc a) False) % 29.63/29.83 (Or (Eq (m1_subset_1 a_1 (k1_zfmisc_1 (u1_struct_0 a))) False) % 29.63/29.83 (Or (Eq (v3_struct_0 a) True) % 29.63/29.83 (Or (Eq (v1_tsp_1 a_1 a) False) % 29.63/29.83 (Eq (Not (And (r1_tarski a_1 (skS.0 16 a a_1 a_2)) (v1_tsp_2 (skS.0 16 a a_1 a_2) a))) False))))) % 29.63/29.83 Clause #646 (by superposition #[644, 72]): ∀ (a a_1 a_2 : Iota), % 29.63/29.83 Or (Eq (v2_pre_topc (skS.0 0 a)) False) % 29.63/29.83 (Or (Eq (m1_subset_1 a_1 (k1_zfmisc_1 (u1_struct_0 (skS.0 0 a)))) False) % 29.63/29.83 (Or (Eq (v3_struct_0 (skS.0 0 a)) True) % 29.63/29.83 (Or (Eq (v1_tsp_1 a_1 (skS.0 0 a)) False) % 29.63/29.83 (Or (Eq (m1_subset_1 (skS.0 16 (skS.0 0 a) a_1 a_2) (k1_zfmisc_1 (u1_struct_0 (skS.0 0 a)))) True) % 29.63/29.83 (Eq False True))))) % 29.63/29.83 Clause #650 (by clausification #[71]): ∀ (a a_1 : Iota), Eq (And (m1_subset_1 a (k1_zfmisc_1 (u1_struct_0 (skS.0 0 a_1)))) (v1_tsp_2 a (skS.0 0 a_1))) False % 29.63/29.83 Clause #651 (by clausification #[650]): ∀ (a a_1 : Iota), % 29.63/29.83 Or (Eq (m1_subset_1 a (k1_zfmisc_1 (u1_struct_0 (skS.0 0 a_1)))) False) (Eq (v1_tsp_2 a (skS.0 0 a_1)) False) % 29.63/29.83 Clause #665 (by clausification #[73]): ∀ (a : Iota), Eq (v2_pre_topc (skS.0 0 a)) True % 29.63/29.83 Clause #666 (by clausification #[73]): ∀ (a : Iota), Eq (Not (v3_struct_0 (skS.0 0 a))) True % 29.63/29.83 Clause #676 (by clausification #[666]): ∀ (a : Iota), Eq (v3_struct_0 (skS.0 0 a)) False % 29.63/29.83 Clause #692 (by clausification #[131]): ∀ (a a_1 : Iota), % 29.63/29.83 Or (Eq (v2_pre_topc (skS.0 0 a)) False) % 29.63/29.83 (Or (Eq (v3_tex_2 a_1 (skS.0 0 a)) True) % 29.63/29.83 (Or (Eq (v3_struct_0 (skS.0 0 a)) True) % 29.63/29.83 (Or (Eq (v1_xboole_0 a_1) False) (Eq (m1_subset_1 a_1 (k1_zfmisc_1 (u1_struct_0 (skS.0 0 a)))) False)))) % 29.63/29.83 Clause #693 (by forward demodulation #[692, 665]): ∀ (a a_1 : Iota), % 29.63/29.83 Or (Eq True False) % 29.63/29.83 (Or (Eq (v3_tex_2 a (skS.0 0 a_1)) True) % 29.63/29.83 (Or (Eq (v3_struct_0 (skS.0 0 a_1)) True) % 29.63/29.83 (Or (Eq (v1_xboole_0 a) False) (Eq (m1_subset_1 a (k1_zfmisc_1 (u1_struct_0 (skS.0 0 a_1)))) False)))) % 29.63/29.83 Clause #694 (by clausification #[693]): ∀ (a a_1 : Iota), % 29.63/29.83 Or (Eq (v3_tex_2 a (skS.0 0 a_1)) True) % 29.63/29.83 (Or (Eq (v3_struct_0 (skS.0 0 a_1)) True) % 29.63/29.83 (Or (Eq (v1_xboole_0 a) False) (Eq (m1_subset_1 a (k1_zfmisc_1 (u1_struct_0 (skS.0 0 a_1)))) False))) % 29.63/29.83 Clause #695 (by forward demodulation #[694, 676]): ∀ (a a_1 : Iota), % 29.63/29.83 Or (Eq (v3_tex_2 a (skS.0 0 a_1)) True) % 29.63/29.83 (Or (Eq False True) % 29.63/29.83 (Or (Eq (v1_xboole_0 a) False) (Eq (m1_subset_1 a (k1_zfmisc_1 (u1_struct_0 (skS.0 0 a_1)))) False))) % 29.63/29.83 Clause #696 (by clausification #[695]): ∀ (a a_1 : Iota), % 29.63/29.83 Or (Eq (v3_tex_2 a (skS.0 0 a_1)) True) % 29.63/29.83 (Or (Eq (v1_xboole_0 a) False) (Eq (m1_subset_1 a (k1_zfmisc_1 (u1_struct_0 (skS.0 0 a_1)))) False)) % 29.63/29.83 Clause #697 (by superposition #[696, 245]): ∀ (a : Iota), % 29.63/29.86 Or (Eq (v3_tex_2 k1_xboole_0 (skS.0 0 a)) True) % 29.63/29.86 (Or (Eq (m1_subset_1 k1_xboole_0 (k1_zfmisc_1 (u1_struct_0 (skS.0 0 a)))) False) (Eq False True)) % 29.63/29.86 Clause #750 (by clausification #[168]): ∀ (a a_1 : Iota), % 29.63/29.86 Or (Eq (v3_struct_0 (skS.0 0 a)) True) % 29.63/29.86 (Or (Eq (m1_subset_1 a_1 (k1_zfmisc_1 (u1_struct_0 (skS.0 0 a)))) False) % 29.63/29.86 (Or (Eq (v3_tex_2 a_1 (skS.0 0 a)) False) (Eq (v1_tsp_1 a_1 (skS.0 0 a)) True))) % 29.63/29.86 Clause #751 (by forward demodulation #[750, 676]): ∀ (a a_1 : Iota), % 29.63/29.86 Or (Eq False True) % 29.63/29.86 (Or (Eq (m1_subset_1 a (k1_zfmisc_1 (u1_struct_0 (skS.0 0 a_1)))) False) % 29.63/29.86 (Or (Eq (v3_tex_2 a (skS.0 0 a_1)) False) (Eq (v1_tsp_1 a (skS.0 0 a_1)) True))) % 29.63/29.86 Clause #752 (by clausification #[751]): ∀ (a a_1 : Iota), % 29.63/29.86 Or (Eq (m1_subset_1 a (k1_zfmisc_1 (u1_struct_0 (skS.0 0 a_1)))) False) % 29.63/29.86 (Or (Eq (v3_tex_2 a (skS.0 0 a_1)) False) (Eq (v1_tsp_1 a (skS.0 0 a_1)) True)) % 29.63/29.86 Clause #753 (by superposition #[752, 314]): ∀ (a : Iota), % 29.63/29.86 Or (Eq (v3_tex_2 k1_xboole_0 (skS.0 0 a)) False) (Or (Eq (v1_tsp_1 k1_xboole_0 (skS.0 0 a)) True) (Eq False True)) % 29.63/29.86 Clause #1230 (by clausification #[645]): ∀ (a a_1 a_2 : Iota), % 29.63/29.86 Or (Eq (l1_pre_topc a) False) % 29.63/29.86 (Or (Eq (v2_pre_topc a) False) % 29.63/29.86 (Or (Eq (m1_subset_1 a_1 (k1_zfmisc_1 (u1_struct_0 a))) False) % 29.63/29.86 (Or (Eq (v3_struct_0 a) True) % 29.63/29.86 (Or (Eq (v1_tsp_1 a_1 a) False) % 29.63/29.86 (Eq (And (r1_tarski a_1 (skS.0 16 a a_1 a_2)) (v1_tsp_2 (skS.0 16 a a_1 a_2) a)) True))))) % 29.63/29.86 Clause #1231 (by clausification #[1230]): ∀ (a a_1 a_2 : Iota), % 29.63/29.86 Or (Eq (l1_pre_topc a) False) % 29.63/29.86 (Or (Eq (v2_pre_topc a) False) % 29.63/29.86 (Or (Eq (m1_subset_1 a_1 (k1_zfmisc_1 (u1_struct_0 a))) False) % 29.63/29.86 (Or (Eq (v3_struct_0 a) True) (Or (Eq (v1_tsp_1 a_1 a) False) (Eq (v1_tsp_2 (skS.0 16 a a_1 a_2) a) True))))) % 29.63/29.86 Clause #1233 (by superposition #[1231, 72]): ∀ (a a_1 a_2 : Iota), % 29.63/29.86 Or (Eq (v2_pre_topc (skS.0 0 a)) False) % 29.63/29.86 (Or (Eq (m1_subset_1 a_1 (k1_zfmisc_1 (u1_struct_0 (skS.0 0 a)))) False) % 29.63/29.86 (Or (Eq (v3_struct_0 (skS.0 0 a)) True) % 29.63/29.86 (Or (Eq (v1_tsp_1 a_1 (skS.0 0 a)) False) % 29.63/29.86 (Or (Eq (v1_tsp_2 (skS.0 16 (skS.0 0 a) a_1 a_2) (skS.0 0 a)) True) (Eq False True))))) % 29.63/29.86 Clause #1236 (by clausification #[753]): ∀ (a : Iota), Or (Eq (v3_tex_2 k1_xboole_0 (skS.0 0 a)) False) (Eq (v1_tsp_1 k1_xboole_0 (skS.0 0 a)) True) % 29.63/29.86 Clause #1242 (by clausification #[646]): ∀ (a a_1 a_2 : Iota), % 29.63/29.86 Or (Eq (v2_pre_topc (skS.0 0 a)) False) % 29.63/29.86 (Or (Eq (m1_subset_1 a_1 (k1_zfmisc_1 (u1_struct_0 (skS.0 0 a)))) False) % 29.63/29.86 (Or (Eq (v3_struct_0 (skS.0 0 a)) True) % 29.63/29.86 (Or (Eq (v1_tsp_1 a_1 (skS.0 0 a)) False) % 29.63/29.86 (Eq (m1_subset_1 (skS.0 16 (skS.0 0 a) a_1 a_2) (k1_zfmisc_1 (u1_struct_0 (skS.0 0 a)))) True)))) % 29.63/29.86 Clause #1243 (by forward demodulation #[1242, 665]): ∀ (a a_1 a_2 : Iota), % 29.63/29.86 Or (Eq True False) % 29.63/29.86 (Or (Eq (m1_subset_1 a (k1_zfmisc_1 (u1_struct_0 (skS.0 0 a_1)))) False) % 29.63/29.86 (Or (Eq (v3_struct_0 (skS.0 0 a_1)) True) % 29.63/29.86 (Or (Eq (v1_tsp_1 a (skS.0 0 a_1)) False) % 29.63/29.86 (Eq (m1_subset_1 (skS.0 16 (skS.0 0 a_1) a a_2) (k1_zfmisc_1 (u1_struct_0 (skS.0 0 a_1)))) True)))) % 29.63/29.86 Clause #1244 (by clausification #[1243]): ∀ (a a_1 a_2 : Iota), % 29.63/29.86 Or (Eq (m1_subset_1 a (k1_zfmisc_1 (u1_struct_0 (skS.0 0 a_1)))) False) % 29.63/29.86 (Or (Eq (v3_struct_0 (skS.0 0 a_1)) True) % 29.63/29.86 (Or (Eq (v1_tsp_1 a (skS.0 0 a_1)) False) % 29.63/29.86 (Eq (m1_subset_1 (skS.0 16 (skS.0 0 a_1) a a_2) (k1_zfmisc_1 (u1_struct_0 (skS.0 0 a_1)))) True))) % 29.63/29.86 Clause #1245 (by forward demodulation #[1244, 676]): ∀ (a a_1 a_2 : Iota), % 29.63/29.86 Or (Eq (m1_subset_1 a (k1_zfmisc_1 (u1_struct_0 (skS.0 0 a_1)))) False) % 29.63/29.86 (Or (Eq False True) % 29.63/29.86 (Or (Eq (v1_tsp_1 a (skS.0 0 a_1)) False) % 29.63/29.86 (Eq (m1_subset_1 (skS.0 16 (skS.0 0 a_1) a a_2) (k1_zfmisc_1 (u1_struct_0 (skS.0 0 a_1)))) True))) % 29.63/29.86 Clause #1246 (by clausification #[1245]): ∀ (a a_1 a_2 : Iota), % 29.63/29.86 Or (Eq (m1_subset_1 a (k1_zfmisc_1 (u1_struct_0 (skS.0 0 a_1)))) False) % 29.63/29.86 (Or (Eq (v1_tsp_1 a (skS.0 0 a_1)) False) % 29.63/29.86 (Eq (m1_subset_1 (skS.0 16 (skS.0 0 a_1) a a_2) (k1_zfmisc_1 (u1_struct_0 (skS.0 0 a_1)))) True)) % 29.63/29.86 Clause #1247 (by superposition #[1246, 314]): ∀ (a a_1 : Iota), % 29.72/29.88 Or (Eq (v1_tsp_1 k1_xboole_0 (skS.0 0 a)) False) % 29.72/29.88 (Or (Eq (m1_subset_1 (skS.0 16 (skS.0 0 a) k1_xboole_0 a_1) (k1_zfmisc_1 (u1_struct_0 (skS.0 0 a)))) True) % 29.72/29.88 (Eq False True)) % 29.72/29.88 Clause #1309 (by clausification #[697]): ∀ (a : Iota), % 29.72/29.88 Or (Eq (v3_tex_2 k1_xboole_0 (skS.0 0 a)) True) % 29.72/29.88 (Eq (m1_subset_1 k1_xboole_0 (k1_zfmisc_1 (u1_struct_0 (skS.0 0 a)))) False) % 29.72/29.88 Clause #1310 (by superposition #[1309, 314]): ∀ (a : Iota), Or (Eq (v3_tex_2 k1_xboole_0 (skS.0 0 a)) True) (Eq False True) % 29.72/29.88 Clause #1311 (by clausification #[1310]): ∀ (a : Iota), Eq (v3_tex_2 k1_xboole_0 (skS.0 0 a)) True % 29.72/29.88 Clause #1312 (by backward demodulation #[1311, 1236]): ∀ (a : Iota), Or (Eq True False) (Eq (v1_tsp_1 k1_xboole_0 (skS.0 0 a)) True) % 29.72/29.88 Clause #1314 (by clausification #[1312]): ∀ (a : Iota), Eq (v1_tsp_1 k1_xboole_0 (skS.0 0 a)) True % 29.72/29.88 Clause #2095 (by clausification #[1233]): ∀ (a a_1 a_2 : Iota), % 29.72/29.88 Or (Eq (v2_pre_topc (skS.0 0 a)) False) % 29.72/29.88 (Or (Eq (m1_subset_1 a_1 (k1_zfmisc_1 (u1_struct_0 (skS.0 0 a)))) False) % 29.72/29.88 (Or (Eq (v3_struct_0 (skS.0 0 a)) True) % 29.72/29.88 (Or (Eq (v1_tsp_1 a_1 (skS.0 0 a)) False) (Eq (v1_tsp_2 (skS.0 16 (skS.0 0 a) a_1 a_2) (skS.0 0 a)) True)))) % 29.72/29.88 Clause #2096 (by forward demodulation #[2095, 665]): ∀ (a a_1 a_2 : Iota), % 29.72/29.88 Or (Eq True False) % 29.72/29.88 (Or (Eq (m1_subset_1 a (k1_zfmisc_1 (u1_struct_0 (skS.0 0 a_1)))) False) % 29.72/29.88 (Or (Eq (v3_struct_0 (skS.0 0 a_1)) True) % 29.72/29.88 (Or (Eq (v1_tsp_1 a (skS.0 0 a_1)) False) (Eq (v1_tsp_2 (skS.0 16 (skS.0 0 a_1) a a_2) (skS.0 0 a_1)) True)))) % 29.72/29.88 Clause #2097 (by clausification #[2096]): ∀ (a a_1 a_2 : Iota), % 29.72/29.88 Or (Eq (m1_subset_1 a (k1_zfmisc_1 (u1_struct_0 (skS.0 0 a_1)))) False) % 29.72/29.88 (Or (Eq (v3_struct_0 (skS.0 0 a_1)) True) % 29.72/29.88 (Or (Eq (v1_tsp_1 a (skS.0 0 a_1)) False) (Eq (v1_tsp_2 (skS.0 16 (skS.0 0 a_1) a a_2) (skS.0 0 a_1)) True))) % 29.72/29.88 Clause #2098 (by forward demodulation #[2097, 676]): ∀ (a a_1 a_2 : Iota), % 29.72/29.88 Or (Eq (m1_subset_1 a (k1_zfmisc_1 (u1_struct_0 (skS.0 0 a_1)))) False) % 29.72/29.88 (Or (Eq False True) % 29.72/29.88 (Or (Eq (v1_tsp_1 a (skS.0 0 a_1)) False) (Eq (v1_tsp_2 (skS.0 16 (skS.0 0 a_1) a a_2) (skS.0 0 a_1)) True))) % 29.72/29.88 Clause #2099 (by clausification #[2098]): ∀ (a a_1 a_2 : Iota), % 29.72/29.88 Or (Eq (m1_subset_1 a (k1_zfmisc_1 (u1_struct_0 (skS.0 0 a_1)))) False) % 29.72/29.88 (Or (Eq (v1_tsp_1 a (skS.0 0 a_1)) False) (Eq (v1_tsp_2 (skS.0 16 (skS.0 0 a_1) a a_2) (skS.0 0 a_1)) True)) % 29.72/29.88 Clause #2100 (by superposition #[2099, 314]): ∀ (a a_1 : Iota), % 29.72/29.88 Or (Eq (v1_tsp_1 k1_xboole_0 (skS.0 0 a)) False) % 29.72/29.88 (Or (Eq (v1_tsp_2 (skS.0 16 (skS.0 0 a) k1_xboole_0 a_1) (skS.0 0 a)) True) (Eq False True)) % 29.72/29.88 Clause #2434 (by clausification #[1247]): ∀ (a a_1 : Iota), % 29.72/29.88 Or (Eq (v1_tsp_1 k1_xboole_0 (skS.0 0 a)) False) % 29.72/29.88 (Eq (m1_subset_1 (skS.0 16 (skS.0 0 a) k1_xboole_0 a_1) (k1_zfmisc_1 (u1_struct_0 (skS.0 0 a)))) True) % 29.72/29.88 Clause #2435 (by forward demodulation #[2434, 1314]): ∀ (a a_1 : Iota), % 29.72/29.88 Or (Eq True False) % 29.72/29.88 (Eq (m1_subset_1 (skS.0 16 (skS.0 0 a) k1_xboole_0 a_1) (k1_zfmisc_1 (u1_struct_0 (skS.0 0 a)))) True) % 29.72/29.88 Clause #2436 (by clausification #[2435]): ∀ (a a_1 : Iota), Eq (m1_subset_1 (skS.0 16 (skS.0 0 a) k1_xboole_0 a_1) (k1_zfmisc_1 (u1_struct_0 (skS.0 0 a)))) True % 29.72/29.88 Clause #2438 (by superposition #[2436, 651]): ∀ (a a_1 : Iota), Or (Eq True False) (Eq (v1_tsp_2 (skS.0 16 (skS.0 0 a) k1_xboole_0 a_1) (skS.0 0 a)) False) % 29.72/29.88 Clause #2450 (by clausification #[2438]): ∀ (a a_1 : Iota), Eq (v1_tsp_2 (skS.0 16 (skS.0 0 a) k1_xboole_0 a_1) (skS.0 0 a)) False % 29.72/29.88 Clause #2741 (by clausification #[2100]): ∀ (a a_1 : Iota), % 29.72/29.88 Or (Eq (v1_tsp_1 k1_xboole_0 (skS.0 0 a)) False) % 29.72/29.88 (Eq (v1_tsp_2 (skS.0 16 (skS.0 0 a) k1_xboole_0 a_1) (skS.0 0 a)) True) % 29.72/29.88 Clause #2742 (by forward demodulation #[2741, 1314]): ∀ (a a_1 : Iota), Or (Eq True False) (Eq (v1_tsp_2 (skS.0 16 (skS.0 0 a) k1_xboole_0 a_1) (skS.0 0 a)) True) % 29.72/29.88 Clause #2743 (by clausification #[2742]): ∀ (a a_1 : Iota), Eq (v1_tsp_2 (skS.0 16 (skS.0 0 a) k1_xboole_0 a_1) (skS.0 0 a)) True % 29.72/29.88 Clause #2744 (by superposition #[2743, 2450]): Eq True False % 29.72/29.88 Clause #2745 (by clausification #[2744]): False % 29.72/29.89 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------