%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : SET666+3 : TPTP v9.2.0. Released v2.2.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n020.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:00:22 PM UTC 2025 % Result : Theorem 7.13s 7.30s % Output : Proof 7.23s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.13 % Problem : SET666+3 : TPTP v9.2.0. Released v2.2.0. % 0.07/0.14 % Command : duper %s % 0.14/0.35 % Computer : n020.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 14:14:38 EDT 2025 % 0.14/0.35 % CPUTime : % 7.13/7.30 SZS status Theorem for theBenchmark.p % 7.13/7.30 SZS output start Proof for theBenchmark.p % 7.13/7.30 Clause #0 (by assumption #[]): Eq % 7.13/7.30 (∀ (B : Iota), % 7.13/7.30 ilf_type B set_type → % 7.13/7.30 ∀ (C : Iota), % 7.13/7.30 ilf_type C set_type → % 7.13/7.30 And (∀ (D : Iota), ilf_type D (subset_type (cross_product B C)) → ilf_type D (relation_type B C)) % 7.13/7.30 (∀ (E : Iota), ilf_type E (relation_type B C) → ilf_type E (subset_type (cross_product B C)))) % 7.13/7.30 True % 7.13/7.30 Clause #2 (by assumption #[]): Eq (∀ (B : Iota), ilf_type B set_type → subset (identity_relation_of B) (cross_product B B)) True % 7.13/7.30 Clause #5 (by assumption #[]): Eq % 7.13/7.30 (∀ (B : Iota), % 7.13/7.30 ilf_type B set_type → % 7.13/7.30 ∀ (C : Iota), % 7.13/7.30 ilf_type C set_type → Iff (ilf_type C (identity_relation_of_type B)) (ilf_type C (relation_type B B))) % 7.13/7.30 True % 7.13/7.30 Clause #11 (by assumption #[]): Eq % 7.13/7.30 (∀ (B : Iota), % 7.13/7.30 ilf_type B set_type → % 7.13/7.30 ∀ (C : Iota), ilf_type C set_type → Iff (ilf_type C (subset_type B)) (ilf_type C (member_type (power_set B)))) % 7.13/7.30 True % 7.13/7.30 Clause #13 (by assumption #[]): Eq % 7.13/7.30 (∀ (B : Iota), % 7.13/7.30 ilf_type B set_type → % 7.13/7.30 ∀ (C : Iota), % 7.13/7.30 ilf_type C set_type → Iff (subset B C) (∀ (D : Iota), ilf_type D set_type → member D B → member D C)) % 7.13/7.30 True % 7.13/7.30 Clause #15 (by assumption #[]): Eq % 7.13/7.30 (∀ (B : Iota), % 7.13/7.30 ilf_type B set_type → % 7.13/7.30 ∀ (C : Iota), % 7.13/7.30 ilf_type C set_type → % 7.13/7.30 Iff (member B (power_set C)) (∀ (D : Iota), ilf_type D set_type → member D B → member D C)) % 7.13/7.30 True % 7.13/7.30 Clause #16 (by assumption #[]): Eq (∀ (B : Iota), ilf_type B set_type → And (Not (empty (power_set B))) (ilf_type (power_set B) set_type)) True % 7.13/7.30 Clause #17 (by assumption #[]): Eq % 7.13/7.30 (∀ (B : Iota), % 7.13/7.30 ilf_type B set_type → % 7.13/7.30 ∀ (C : Iota), And (Not (empty C)) (ilf_type C set_type) → Iff (ilf_type B (member_type C)) (member B C)) % 7.13/7.30 True % 7.13/7.30 Clause #23 (by assumption #[]): Eq (∀ (B : Iota), ilf_type B set_type) True % 7.13/7.30 Clause #24 (by assumption #[]): Eq (Not (∀ (B : Iota), ilf_type B set_type → ilf_type (identity_relation_of B) (identity_relation_of_type B))) True % 7.13/7.30 Clause #25 (by clausification #[23]): ∀ (a : Iota), Eq (ilf_type a set_type) True % 7.13/7.30 Clause #38 (by clausification #[0]): ∀ (a : Iota), % 7.13/7.30 Eq % 7.13/7.30 (ilf_type a set_type → % 7.13/7.30 ∀ (C : Iota), % 7.13/7.30 ilf_type C set_type → % 7.13/7.30 And (∀ (D : Iota), ilf_type D (subset_type (cross_product a C)) → ilf_type D (relation_type a C)) % 7.13/7.30 (∀ (E : Iota), ilf_type E (relation_type a C) → ilf_type E (subset_type (cross_product a C)))) % 7.13/7.30 True % 7.13/7.30 Clause #39 (by clausification #[38]): ∀ (a : Iota), % 7.13/7.30 Or (Eq (ilf_type a set_type) False) % 7.13/7.30 (Eq % 7.13/7.30 (∀ (C : Iota), % 7.13/7.30 ilf_type C set_type → % 7.13/7.30 And (∀ (D : Iota), ilf_type D (subset_type (cross_product a C)) → ilf_type D (relation_type a C)) % 7.13/7.30 (∀ (E : Iota), ilf_type E (relation_type a C) → ilf_type E (subset_type (cross_product a C)))) % 7.13/7.30 True) % 7.13/7.30 Clause #40 (by clausification #[39]): ∀ (a a_1 : Iota), % 7.13/7.30 Or (Eq (ilf_type a set_type) False) % 7.13/7.30 (Eq % 7.13/7.30 (ilf_type a_1 set_type → % 7.13/7.30 And (∀ (D : Iota), ilf_type D (subset_type (cross_product a a_1)) → ilf_type D (relation_type a a_1)) % 7.13/7.30 (∀ (E : Iota), ilf_type E (relation_type a a_1) → ilf_type E (subset_type (cross_product a a_1)))) % 7.13/7.30 True) % 7.13/7.30 Clause #41 (by clausification #[40]): ∀ (a a_1 : Iota), % 7.13/7.30 Or (Eq (ilf_type a set_type) False) % 7.13/7.30 (Or (Eq (ilf_type a_1 set_type) False) % 7.13/7.30 (Eq % 7.13/7.30 (And (∀ (D : Iota), ilf_type D (subset_type (cross_product a a_1)) → ilf_type D (relation_type a a_1)) % 7.13/7.30 (∀ (E : Iota), ilf_type E (relation_type a a_1) → ilf_type E (subset_type (cross_product a a_1)))) % 7.13/7.30 True)) % 7.13/7.30 Clause #43 (by clausification #[41]): ∀ (a a_1 : Iota), % 7.13/7.30 Or (Eq (ilf_type a set_type) False) % 7.13/7.30 (Or (Eq (ilf_type a_1 set_type) False) % 7.13/7.30 (Eq (∀ (D : Iota), ilf_type D (subset_type (cross_product a a_1)) → ilf_type D (relation_type a a_1)) True)) % 7.13/7.30 Clause #50 (by clausification #[2]): ∀ (a : Iota), Eq (ilf_type a set_type → subset (identity_relation_of a) (cross_product a a)) True % 7.13/7.30 Clause #51 (by clausification #[50]): ∀ (a : Iota), Or (Eq (ilf_type a set_type) False) (Eq (subset (identity_relation_of a) (cross_product a a)) True) % 7.13/7.33 Clause #52 (by forward demodulation #[51, 25]): ∀ (a : Iota), Or (Eq True False) (Eq (subset (identity_relation_of a) (cross_product a a)) True) % 7.13/7.33 Clause #53 (by clausification #[52]): ∀ (a : Iota), Eq (subset (identity_relation_of a) (cross_product a a)) True % 7.13/7.33 Clause #54 (by clausification #[24]): Eq (∀ (B : Iota), ilf_type B set_type → ilf_type (identity_relation_of B) (identity_relation_of_type B)) False % 7.13/7.33 Clause #55 (by clausification #[54]): ∀ (a : Iota), % 7.13/7.33 Eq % 7.13/7.33 (Not % 7.13/7.33 (ilf_type (skS.0 1 a) set_type → % 7.13/7.33 ilf_type (identity_relation_of (skS.0 1 a)) (identity_relation_of_type (skS.0 1 a)))) % 7.13/7.33 True % 7.13/7.33 Clause #56 (by clausification #[55]): ∀ (a : Iota), % 7.13/7.33 Eq % 7.13/7.33 (ilf_type (skS.0 1 a) set_type → % 7.13/7.33 ilf_type (identity_relation_of (skS.0 1 a)) (identity_relation_of_type (skS.0 1 a))) % 7.13/7.33 False % 7.13/7.33 Clause #58 (by clausification #[56]): ∀ (a : Iota), Eq (ilf_type (identity_relation_of (skS.0 1 a)) (identity_relation_of_type (skS.0 1 a))) False % 7.13/7.33 Clause #123 (by clausification #[16]): ∀ (a : Iota), Eq (ilf_type a set_type → And (Not (empty (power_set a))) (ilf_type (power_set a) set_type)) True % 7.13/7.33 Clause #124 (by clausification #[123]): ∀ (a : Iota), % 7.13/7.33 Or (Eq (ilf_type a set_type) False) (Eq (And (Not (empty (power_set a))) (ilf_type (power_set a) set_type)) True) % 7.13/7.33 Clause #126 (by clausification #[124]): ∀ (a : Iota), Or (Eq (ilf_type a set_type) False) (Eq (Not (empty (power_set a))) True) % 7.13/7.33 Clause #145 (by clausification #[126]): ∀ (a : Iota), Or (Eq (ilf_type a set_type) False) (Eq (empty (power_set a)) False) % 7.13/7.33 Clause #146 (by forward demodulation #[145, 25]): ∀ (a : Iota), Or (Eq True False) (Eq (empty (power_set a)) False) % 7.13/7.33 Clause #147 (by clausification #[146]): ∀ (a : Iota), Eq (empty (power_set a)) False % 7.13/7.33 Clause #148 (by clausification #[17]): ∀ (a : Iota), % 7.13/7.33 Eq % 7.13/7.33 (ilf_type a set_type → % 7.13/7.33 ∀ (C : Iota), And (Not (empty C)) (ilf_type C set_type) → Iff (ilf_type a (member_type C)) (member a C)) % 7.13/7.33 True % 7.13/7.33 Clause #149 (by clausification #[148]): ∀ (a : Iota), % 7.13/7.33 Or (Eq (ilf_type a set_type) False) % 7.13/7.33 (Eq (∀ (C : Iota), And (Not (empty C)) (ilf_type C set_type) → Iff (ilf_type a (member_type C)) (member a C)) True) % 7.13/7.33 Clause #150 (by clausification #[149]): ∀ (a a_1 : Iota), % 7.13/7.33 Or (Eq (ilf_type a set_type) False) % 7.13/7.33 (Eq (And (Not (empty a_1)) (ilf_type a_1 set_type) → Iff (ilf_type a (member_type a_1)) (member a a_1)) True) % 7.13/7.33 Clause #151 (by clausification #[150]): ∀ (a a_1 : Iota), % 7.13/7.33 Or (Eq (ilf_type a set_type) False) % 7.13/7.33 (Or (Eq (And (Not (empty a_1)) (ilf_type a_1 set_type)) False) % 7.13/7.33 (Eq (Iff (ilf_type a (member_type a_1)) (member a a_1)) True)) % 7.13/7.33 Clause #152 (by clausification #[151]): ∀ (a a_1 : Iota), % 7.13/7.33 Or (Eq (ilf_type a set_type) False) % 7.13/7.33 (Or (Eq (Iff (ilf_type a (member_type a_1)) (member a a_1)) True) % 7.13/7.33 (Or (Eq (Not (empty a_1)) False) (Eq (ilf_type a_1 set_type) False))) % 7.13/7.33 Clause #153 (by clausification #[152]): ∀ (a a_1 : Iota), % 7.13/7.33 Or (Eq (ilf_type a set_type) False) % 7.13/7.33 (Or (Eq (Not (empty a_1)) False) % 7.13/7.33 (Or (Eq (ilf_type a_1 set_type) False) (Or (Eq (ilf_type a (member_type a_1)) True) (Eq (member a a_1) False)))) % 7.13/7.33 Clause #155 (by clausification #[153]): ∀ (a a_1 : Iota), % 7.13/7.33 Or (Eq (ilf_type a set_type) False) % 7.13/7.33 (Or (Eq (ilf_type a_1 set_type) False) % 7.13/7.33 (Or (Eq (ilf_type a (member_type a_1)) True) (Or (Eq (member a a_1) False) (Eq (empty a_1) True)))) % 7.13/7.33 Clause #156 (by forward demodulation #[155, 25]): ∀ (a a_1 : Iota), % 7.13/7.33 Or (Eq True False) % 7.13/7.33 (Or (Eq (ilf_type a set_type) False) % 7.13/7.33 (Or (Eq (ilf_type a_1 (member_type a)) True) (Or (Eq (member a_1 a) False) (Eq (empty a) True)))) % 7.13/7.33 Clause #157 (by clausification #[156]): ∀ (a a_1 : Iota), % 7.13/7.33 Or (Eq (ilf_type a set_type) False) % 7.13/7.33 (Or (Eq (ilf_type a_1 (member_type a)) True) (Or (Eq (member a_1 a) False) (Eq (empty a) True))) % 7.13/7.33 Clause #158 (by forward demodulation #[157, 25]): ∀ (a a_1 : Iota), % 7.13/7.33 Or (Eq True False) (Or (Eq (ilf_type a (member_type a_1)) True) (Or (Eq (member a a_1) False) (Eq (empty a_1) True))) % 7.13/7.35 Clause #159 (by clausification #[158]): ∀ (a a_1 : Iota), Or (Eq (ilf_type a (member_type a_1)) True) (Or (Eq (member a a_1) False) (Eq (empty a_1) True)) % 7.13/7.35 Clause #177 (by clausification #[5]): ∀ (a : Iota), % 7.13/7.35 Eq % 7.13/7.35 (ilf_type a set_type → % 7.13/7.35 ∀ (C : Iota), % 7.13/7.35 ilf_type C set_type → Iff (ilf_type C (identity_relation_of_type a)) (ilf_type C (relation_type a a))) % 7.13/7.35 True % 7.13/7.35 Clause #178 (by clausification #[177]): ∀ (a : Iota), % 7.13/7.35 Or (Eq (ilf_type a set_type) False) % 7.13/7.35 (Eq % 7.13/7.35 (∀ (C : Iota), % 7.13/7.35 ilf_type C set_type → Iff (ilf_type C (identity_relation_of_type a)) (ilf_type C (relation_type a a))) % 7.13/7.35 True) % 7.13/7.35 Clause #179 (by clausification #[178]): ∀ (a a_1 : Iota), % 7.13/7.35 Or (Eq (ilf_type a set_type) False) % 7.13/7.35 (Eq (ilf_type a_1 set_type → Iff (ilf_type a_1 (identity_relation_of_type a)) (ilf_type a_1 (relation_type a a))) % 7.13/7.35 True) % 7.13/7.35 Clause #180 (by clausification #[179]): ∀ (a a_1 : Iota), % 7.13/7.35 Or (Eq (ilf_type a set_type) False) % 7.13/7.35 (Or (Eq (ilf_type a_1 set_type) False) % 7.13/7.35 (Eq (Iff (ilf_type a_1 (identity_relation_of_type a)) (ilf_type a_1 (relation_type a a))) True)) % 7.13/7.35 Clause #181 (by clausification #[180]): ∀ (a a_1 : Iota), % 7.13/7.35 Or (Eq (ilf_type a set_type) False) % 7.13/7.35 (Or (Eq (ilf_type a_1 set_type) False) % 7.13/7.35 (Or (Eq (ilf_type a_1 (identity_relation_of_type a)) True) (Eq (ilf_type a_1 (relation_type a a)) False))) % 7.13/7.35 Clause #183 (by forward demodulation #[181, 25]): ∀ (a a_1 : Iota), % 7.13/7.35 Or (Eq True False) % 7.13/7.35 (Or (Eq (ilf_type a set_type) False) % 7.13/7.35 (Or (Eq (ilf_type a (identity_relation_of_type a_1)) True) (Eq (ilf_type a (relation_type a_1 a_1)) False))) % 7.13/7.35 Clause #184 (by clausification #[183]): ∀ (a a_1 : Iota), % 7.13/7.35 Or (Eq (ilf_type a set_type) False) % 7.13/7.35 (Or (Eq (ilf_type a (identity_relation_of_type a_1)) True) (Eq (ilf_type a (relation_type a_1 a_1)) False)) % 7.13/7.35 Clause #185 (by forward demodulation #[184, 25]): ∀ (a a_1 : Iota), % 7.13/7.35 Or (Eq True False) % 7.13/7.35 (Or (Eq (ilf_type a (identity_relation_of_type a_1)) True) (Eq (ilf_type a (relation_type a_1 a_1)) False)) % 7.13/7.35 Clause #186 (by clausification #[185]): ∀ (a a_1 : Iota), % 7.13/7.35 Or (Eq (ilf_type a (identity_relation_of_type a_1)) True) (Eq (ilf_type a (relation_type a_1 a_1)) False) % 7.13/7.35 Clause #198 (by clausification #[11]): ∀ (a : Iota), % 7.13/7.35 Eq % 7.13/7.35 (ilf_type a set_type → % 7.13/7.35 ∀ (C : Iota), ilf_type C set_type → Iff (ilf_type C (subset_type a)) (ilf_type C (member_type (power_set a)))) % 7.13/7.35 True % 7.13/7.35 Clause #199 (by clausification #[198]): ∀ (a : Iota), % 7.13/7.35 Or (Eq (ilf_type a set_type) False) % 7.13/7.35 (Eq (∀ (C : Iota), ilf_type C set_type → Iff (ilf_type C (subset_type a)) (ilf_type C (member_type (power_set a)))) % 7.13/7.35 True) % 7.13/7.35 Clause #200 (by clausification #[199]): ∀ (a a_1 : Iota), % 7.13/7.35 Or (Eq (ilf_type a set_type) False) % 7.13/7.35 (Eq (ilf_type a_1 set_type → Iff (ilf_type a_1 (subset_type a)) (ilf_type a_1 (member_type (power_set a)))) True) % 7.13/7.35 Clause #201 (by clausification #[200]): ∀ (a a_1 : Iota), % 7.13/7.35 Or (Eq (ilf_type a set_type) False) % 7.13/7.35 (Or (Eq (ilf_type a_1 set_type) False) % 7.13/7.35 (Eq (Iff (ilf_type a_1 (subset_type a)) (ilf_type a_1 (member_type (power_set a)))) True)) % 7.13/7.35 Clause #202 (by clausification #[201]): ∀ (a a_1 : Iota), % 7.13/7.35 Or (Eq (ilf_type a set_type) False) % 7.13/7.35 (Or (Eq (ilf_type a_1 set_type) False) % 7.13/7.35 (Or (Eq (ilf_type a_1 (subset_type a)) True) (Eq (ilf_type a_1 (member_type (power_set a))) False))) % 7.13/7.35 Clause #204 (by forward demodulation #[202, 25]): ∀ (a a_1 : Iota), % 7.13/7.35 Or (Eq True False) % 7.13/7.35 (Or (Eq (ilf_type a set_type) False) % 7.13/7.35 (Or (Eq (ilf_type a (subset_type a_1)) True) (Eq (ilf_type a (member_type (power_set a_1))) False))) % 7.13/7.35 Clause #205 (by clausification #[204]): ∀ (a a_1 : Iota), % 7.13/7.35 Or (Eq (ilf_type a set_type) False) % 7.13/7.35 (Or (Eq (ilf_type a (subset_type a_1)) True) (Eq (ilf_type a (member_type (power_set a_1))) False)) % 7.13/7.35 Clause #206 (by forward demodulation #[205, 25]): ∀ (a a_1 : Iota), % 7.13/7.35 Or (Eq True False) (Or (Eq (ilf_type a (subset_type a_1)) True) (Eq (ilf_type a (member_type (power_set a_1))) False)) % 7.13/7.35 Clause #207 (by clausification #[206]): ∀ (a a_1 : Iota), Or (Eq (ilf_type a (subset_type a_1)) True) (Eq (ilf_type a (member_type (power_set a_1))) False) % 7.21/7.37 Clause #211 (by clausification #[13]): ∀ (a : Iota), % 7.21/7.37 Eq % 7.21/7.37 (ilf_type a set_type → % 7.21/7.37 ∀ (C : Iota), % 7.21/7.37 ilf_type C set_type → Iff (subset a C) (∀ (D : Iota), ilf_type D set_type → member D a → member D C)) % 7.21/7.37 True % 7.21/7.37 Clause #212 (by clausification #[211]): ∀ (a : Iota), % 7.21/7.37 Or (Eq (ilf_type a set_type) False) % 7.21/7.37 (Eq % 7.21/7.37 (∀ (C : Iota), % 7.21/7.37 ilf_type C set_type → Iff (subset a C) (∀ (D : Iota), ilf_type D set_type → member D a → member D C)) % 7.21/7.37 True) % 7.21/7.37 Clause #213 (by clausification #[212]): ∀ (a a_1 : Iota), % 7.21/7.37 Or (Eq (ilf_type a set_type) False) % 7.21/7.37 (Eq (ilf_type a_1 set_type → Iff (subset a a_1) (∀ (D : Iota), ilf_type D set_type → member D a → member D a_1)) % 7.21/7.37 True) % 7.21/7.37 Clause #214 (by clausification #[213]): ∀ (a a_1 : Iota), % 7.21/7.37 Or (Eq (ilf_type a set_type) False) % 7.21/7.37 (Or (Eq (ilf_type a_1 set_type) False) % 7.21/7.37 (Eq (Iff (subset a a_1) (∀ (D : Iota), ilf_type D set_type → member D a → member D a_1)) True)) % 7.21/7.37 Clause #216 (by clausification #[214]): ∀ (a a_1 : Iota), % 7.21/7.37 Or (Eq (ilf_type a set_type) False) % 7.21/7.37 (Or (Eq (ilf_type a_1 set_type) False) % 7.21/7.37 (Or (Eq (subset a a_1) False) (Eq (∀ (D : Iota), ilf_type D set_type → member D a → member D a_1) True))) % 7.21/7.37 Clause #225 (by clausification #[43]): ∀ (a a_1 a_2 : Iota), % 7.21/7.37 Or (Eq (ilf_type a set_type) False) % 7.21/7.37 (Or (Eq (ilf_type a_1 set_type) False) % 7.21/7.37 (Eq (ilf_type a_2 (subset_type (cross_product a a_1)) → ilf_type a_2 (relation_type a a_1)) True)) % 7.21/7.37 Clause #226 (by clausification #[225]): ∀ (a a_1 a_2 : Iota), % 7.21/7.37 Or (Eq (ilf_type a set_type) False) % 7.21/7.37 (Or (Eq (ilf_type a_1 set_type) False) % 7.21/7.37 (Or (Eq (ilf_type a_2 (subset_type (cross_product a a_1))) False) (Eq (ilf_type a_2 (relation_type a a_1)) True))) % 7.21/7.37 Clause #227 (by forward demodulation #[226, 25]): ∀ (a a_1 a_2 : Iota), % 7.21/7.37 Or (Eq True False) % 7.21/7.37 (Or (Eq (ilf_type a set_type) False) % 7.21/7.37 (Or (Eq (ilf_type a_1 (subset_type (cross_product a_2 a))) False) (Eq (ilf_type a_1 (relation_type a_2 a)) True))) % 7.21/7.37 Clause #228 (by clausification #[227]): ∀ (a a_1 a_2 : Iota), % 7.21/7.37 Or (Eq (ilf_type a set_type) False) % 7.21/7.37 (Or (Eq (ilf_type a_1 (subset_type (cross_product a_2 a))) False) (Eq (ilf_type a_1 (relation_type a_2 a)) True)) % 7.21/7.37 Clause #229 (by forward demodulation #[228, 25]): ∀ (a a_1 a_2 : Iota), % 7.21/7.37 Or (Eq True False) % 7.21/7.37 (Or (Eq (ilf_type a (subset_type (cross_product a_1 a_2))) False) (Eq (ilf_type a (relation_type a_1 a_2)) True)) % 7.21/7.37 Clause #230 (by clausification #[229]): ∀ (a a_1 a_2 : Iota), % 7.21/7.37 Or (Eq (ilf_type a (subset_type (cross_product a_1 a_2))) False) (Eq (ilf_type a (relation_type a_1 a_2)) True) % 7.21/7.37 Clause #232 (by clausification #[15]): ∀ (a : Iota), % 7.21/7.37 Eq % 7.21/7.37 (ilf_type a set_type → % 7.21/7.37 ∀ (C : Iota), % 7.21/7.37 ilf_type C set_type → % 7.21/7.37 Iff (member a (power_set C)) (∀ (D : Iota), ilf_type D set_type → member D a → member D C)) % 7.21/7.37 True % 7.21/7.37 Clause #233 (by clausification #[232]): ∀ (a : Iota), % 7.21/7.37 Or (Eq (ilf_type a set_type) False) % 7.21/7.37 (Eq % 7.21/7.37 (∀ (C : Iota), % 7.21/7.37 ilf_type C set_type → % 7.21/7.37 Iff (member a (power_set C)) (∀ (D : Iota), ilf_type D set_type → member D a → member D C)) % 7.21/7.37 True) % 7.21/7.37 Clause #234 (by clausification #[233]): ∀ (a a_1 : Iota), % 7.21/7.37 Or (Eq (ilf_type a set_type) False) % 7.21/7.37 (Eq % 7.21/7.37 (ilf_type a_1 set_type → % 7.21/7.37 Iff (member a (power_set a_1)) (∀ (D : Iota), ilf_type D set_type → member D a → member D a_1)) % 7.21/7.37 True) % 7.21/7.37 Clause #235 (by clausification #[234]): ∀ (a a_1 : Iota), % 7.21/7.37 Or (Eq (ilf_type a set_type) False) % 7.21/7.37 (Or (Eq (ilf_type a_1 set_type) False) % 7.21/7.37 (Eq (Iff (member a (power_set a_1)) (∀ (D : Iota), ilf_type D set_type → member D a → member D a_1)) True)) % 7.21/7.37 Clause #236 (by clausification #[235]): ∀ (a a_1 : Iota), % 7.21/7.37 Or (Eq (ilf_type a set_type) False) % 7.21/7.37 (Or (Eq (ilf_type a_1 set_type) False) % 7.21/7.37 (Or (Eq (member a (power_set a_1)) True) % 7.21/7.37 (Eq (∀ (D : Iota), ilf_type D set_type → member D a → member D a_1) False))) % 7.21/7.37 Clause #238 (by clausification #[236]): ∀ (a a_1 a_2 : Iota), % 7.23/7.39 Or (Eq (ilf_type a set_type) False) % 7.23/7.39 (Or (Eq (ilf_type a_1 set_type) False) % 7.23/7.39 (Or (Eq (member a (power_set a_1)) True) % 7.23/7.39 (Eq % 7.23/7.39 (Not (ilf_type (skS.0 8 a a_1 a_2) set_type → member (skS.0 8 a a_1 a_2) a → member (skS.0 8 a a_1 a_2) a_1)) % 7.23/7.39 True))) % 7.23/7.39 Clause #239 (by clausification #[238]): ∀ (a a_1 a_2 : Iota), % 7.23/7.39 Or (Eq (ilf_type a set_type) False) % 7.23/7.39 (Or (Eq (ilf_type a_1 set_type) False) % 7.23/7.39 (Or (Eq (member a (power_set a_1)) True) % 7.23/7.39 (Eq (ilf_type (skS.0 8 a a_1 a_2) set_type → member (skS.0 8 a a_1 a_2) a → member (skS.0 8 a a_1 a_2) a_1) % 7.23/7.39 False))) % 7.23/7.39 Clause #241 (by clausification #[239]): ∀ (a a_1 a_2 : Iota), % 7.23/7.39 Or (Eq (ilf_type a set_type) False) % 7.23/7.39 (Or (Eq (ilf_type a_1 set_type) False) % 7.23/7.39 (Or (Eq (member a (power_set a_1)) True) % 7.23/7.39 (Eq (member (skS.0 8 a a_1 a_2) a → member (skS.0 8 a a_1 a_2) a_1) False))) % 7.23/7.39 Clause #334 (by clausification #[216]): ∀ (a a_1 a_2 : Iota), % 7.23/7.39 Or (Eq (ilf_type a set_type) False) % 7.23/7.39 (Or (Eq (ilf_type a_1 set_type) False) % 7.23/7.39 (Or (Eq (subset a a_1) False) (Eq (ilf_type a_2 set_type → member a_2 a → member a_2 a_1) True))) % 7.23/7.39 Clause #335 (by clausification #[334]): ∀ (a a_1 a_2 : Iota), % 7.23/7.39 Or (Eq (ilf_type a set_type) False) % 7.23/7.39 (Or (Eq (ilf_type a_1 set_type) False) % 7.23/7.39 (Or (Eq (subset a a_1) False) (Or (Eq (ilf_type a_2 set_type) False) (Eq (member a_2 a → member a_2 a_1) True)))) % 7.23/7.39 Clause #336 (by clausification #[335]): ∀ (a a_1 a_2 : Iota), % 7.23/7.39 Or (Eq (ilf_type a set_type) False) % 7.23/7.39 (Or (Eq (ilf_type a_1 set_type) False) % 7.23/7.39 (Or (Eq (subset a a_1) False) % 7.23/7.39 (Or (Eq (ilf_type a_2 set_type) False) (Or (Eq (member a_2 a) False) (Eq (member a_2 a_1) True))))) % 7.23/7.39 Clause #337 (by forward demodulation #[336, 25]): ∀ (a a_1 a_2 : Iota), % 7.23/7.39 Or (Eq True False) % 7.23/7.39 (Or (Eq (ilf_type a set_type) False) % 7.23/7.39 (Or (Eq (subset a_1 a) False) % 7.23/7.39 (Or (Eq (ilf_type a_2 set_type) False) (Or (Eq (member a_2 a_1) False) (Eq (member a_2 a) True))))) % 7.23/7.39 Clause #338 (by clausification #[337]): ∀ (a a_1 a_2 : Iota), % 7.23/7.39 Or (Eq (ilf_type a set_type) False) % 7.23/7.39 (Or (Eq (subset a_1 a) False) % 7.23/7.39 (Or (Eq (ilf_type a_2 set_type) False) (Or (Eq (member a_2 a_1) False) (Eq (member a_2 a) True)))) % 7.23/7.39 Clause #339 (by forward demodulation #[338, 25]): ∀ (a a_1 a_2 : Iota), % 7.23/7.39 Or (Eq True False) % 7.23/7.39 (Or (Eq (subset a a_1) False) % 7.23/7.39 (Or (Eq (ilf_type a_2 set_type) False) (Or (Eq (member a_2 a) False) (Eq (member a_2 a_1) True)))) % 7.23/7.39 Clause #340 (by clausification #[339]): ∀ (a a_1 a_2 : Iota), % 7.23/7.39 Or (Eq (subset a a_1) False) % 7.23/7.39 (Or (Eq (ilf_type a_2 set_type) False) (Or (Eq (member a_2 a) False) (Eq (member a_2 a_1) True))) % 7.23/7.39 Clause #341 (by forward demodulation #[340, 25]): ∀ (a a_1 a_2 : Iota), % 7.23/7.39 Or (Eq (subset a a_1) False) (Or (Eq True False) (Or (Eq (member a_2 a) False) (Eq (member a_2 a_1) True))) % 7.23/7.39 Clause #342 (by clausification #[341]): ∀ (a a_1 a_2 : Iota), Or (Eq (subset a a_1) False) (Or (Eq (member a_2 a) False) (Eq (member a_2 a_1) True)) % 7.23/7.39 Clause #343 (by superposition #[342, 53]): ∀ (a a_1 : Iota), % 7.23/7.39 Or (Eq (member a (identity_relation_of a_1)) False) (Or (Eq (member a (cross_product a_1 a_1)) True) (Eq False True)) % 7.23/7.39 Clause #346 (by clausification #[343]): ∀ (a a_1 : Iota), Or (Eq (member a (identity_relation_of a_1)) False) (Eq (member a (cross_product a_1 a_1)) True) % 7.23/7.39 Clause #397 (by clausification #[241]): ∀ (a a_1 a_2 : Iota), % 7.23/7.39 Or (Eq (ilf_type a set_type) False) % 7.23/7.39 (Or (Eq (ilf_type a_1 set_type) False) % 7.23/7.39 (Or (Eq (member a (power_set a_1)) True) (Eq (member (skS.0 8 a a_1 a_2) a) True))) % 7.23/7.39 Clause #398 (by clausification #[241]): ∀ (a a_1 a_2 : Iota), % 7.23/7.39 Or (Eq (ilf_type a set_type) False) % 7.23/7.39 (Or (Eq (ilf_type a_1 set_type) False) % 7.23/7.39 (Or (Eq (member a (power_set a_1)) True) (Eq (member (skS.0 8 a a_1 a_2) a_1) False))) % 7.23/7.39 Clause #399 (by forward demodulation #[397, 25]): ∀ (a a_1 a_2 : Iota), % 7.23/7.39 Or (Eq True False) % 7.23/7.39 (Or (Eq (ilf_type a set_type) False) % 7.23/7.39 (Or (Eq (member a_1 (power_set a)) True) (Eq (member (skS.0 8 a_1 a a_2) a_1) True))) % 7.23/7.39 Clause #400 (by clausification #[399]): ∀ (a a_1 a_2 : Iota), % 7.23/7.41 Or (Eq (ilf_type a set_type) False) % 7.23/7.41 (Or (Eq (member a_1 (power_set a)) True) (Eq (member (skS.0 8 a_1 a a_2) a_1) True)) % 7.23/7.41 Clause #401 (by forward demodulation #[400, 25]): ∀ (a a_1 a_2 : Iota), % 7.23/7.41 Or (Eq True False) (Or (Eq (member a (power_set a_1)) True) (Eq (member (skS.0 8 a a_1 a_2) a) True)) % 7.23/7.41 Clause #402 (by clausification #[401]): ∀ (a a_1 a_2 : Iota), Or (Eq (member a (power_set a_1)) True) (Eq (member (skS.0 8 a a_1 a_2) a) True) % 7.23/7.41 Clause #403 (by superposition #[402, 346]): ∀ (a a_1 a_2 : Iota), % 7.23/7.41 Or (Eq (member (identity_relation_of a) (power_set a_1)) True) % 7.23/7.41 (Or (Eq True False) (Eq (member (skS.0 8 (identity_relation_of a) a_1 a_2) (cross_product a a)) True)) % 7.23/7.41 Clause #578 (by clausification #[403]): ∀ (a a_1 a_2 : Iota), % 7.23/7.41 Or (Eq (member (identity_relation_of a) (power_set a_1)) True) % 7.23/7.41 (Eq (member (skS.0 8 (identity_relation_of a) a_1 a_2) (cross_product a a)) True) % 7.23/7.41 Clause #683 (by forward demodulation #[398, 25]): ∀ (a a_1 a_2 : Iota), % 7.23/7.41 Or (Eq True False) % 7.23/7.41 (Or (Eq (ilf_type a set_type) False) % 7.23/7.41 (Or (Eq (member a_1 (power_set a)) True) (Eq (member (skS.0 8 a_1 a a_2) a) False))) % 7.23/7.41 Clause #684 (by clausification #[683]): ∀ (a a_1 a_2 : Iota), % 7.23/7.41 Or (Eq (ilf_type a set_type) False) % 7.23/7.41 (Or (Eq (member a_1 (power_set a)) True) (Eq (member (skS.0 8 a_1 a a_2) a) False)) % 7.23/7.41 Clause #685 (by forward demodulation #[684, 25]): ∀ (a a_1 a_2 : Iota), % 7.23/7.41 Or (Eq True False) (Or (Eq (member a (power_set a_1)) True) (Eq (member (skS.0 8 a a_1 a_2) a_1) False)) % 7.23/7.41 Clause #686 (by clausification #[685]): ∀ (a a_1 a_2 : Iota), Or (Eq (member a (power_set a_1)) True) (Eq (member (skS.0 8 a a_1 a_2) a_1) False) % 7.23/7.41 Clause #687 (by superposition #[686, 578]): ∀ (a : Iota), % 7.23/7.41 Or (Eq (member (identity_relation_of a) (power_set (cross_product a a))) True) % 7.23/7.41 (Or (Eq (member (identity_relation_of a) (power_set (cross_product a a))) True) (Eq False True)) % 7.23/7.41 Clause #763 (by clausification #[687]): ∀ (a : Iota), % 7.23/7.41 Or (Eq (member (identity_relation_of a) (power_set (cross_product a a))) True) % 7.23/7.41 (Eq (member (identity_relation_of a) (power_set (cross_product a a))) True) % 7.23/7.41 Clause #764 (by eliminate duplicate literals #[763]): ∀ (a : Iota), Eq (member (identity_relation_of a) (power_set (cross_product a a))) True % 7.23/7.41 Clause #767 (by superposition #[764, 159]): ∀ (a : Iota), % 7.23/7.41 Or (Eq (ilf_type (identity_relation_of a) (member_type (power_set (cross_product a a)))) True) % 7.23/7.41 (Or (Eq True False) (Eq (empty (power_set (cross_product a a))) True)) % 7.23/7.41 Clause #786 (by clausification #[767]): ∀ (a : Iota), % 7.23/7.41 Or (Eq (ilf_type (identity_relation_of a) (member_type (power_set (cross_product a a)))) True) % 7.23/7.41 (Eq (empty (power_set (cross_product a a))) True) % 7.23/7.41 Clause #787 (by forward demodulation #[786, 147]): ∀ (a : Iota), % 7.23/7.41 Or (Eq (ilf_type (identity_relation_of a) (member_type (power_set (cross_product a a)))) True) (Eq False True) % 7.23/7.41 Clause #788 (by clausification #[787]): ∀ (a : Iota), Eq (ilf_type (identity_relation_of a) (member_type (power_set (cross_product a a)))) True % 7.23/7.41 Clause #789 (by superposition #[788, 207]): ∀ (a : Iota), Or (Eq (ilf_type (identity_relation_of a) (subset_type (cross_product a a))) True) (Eq True False) % 7.23/7.41 Clause #791 (by clausification #[789]): ∀ (a : Iota), Eq (ilf_type (identity_relation_of a) (subset_type (cross_product a a))) True % 7.23/7.41 Clause #793 (by superposition #[791, 230]): ∀ (a : Iota), Or (Eq True False) (Eq (ilf_type (identity_relation_of a) (relation_type a a)) True) % 7.23/7.41 Clause #808 (by clausification #[793]): ∀ (a : Iota), Eq (ilf_type (identity_relation_of a) (relation_type a a)) True % 7.23/7.41 Clause #810 (by superposition #[808, 186]): ∀ (a : Iota), Or (Eq (ilf_type (identity_relation_of a) (identity_relation_of_type a)) True) (Eq True False) % 7.23/7.41 Clause #811 (by clausification #[810]): ∀ (a : Iota), Eq (ilf_type (identity_relation_of a) (identity_relation_of_type a)) True % 7.23/7.41 Clause #812 (by superposition #[811, 58]): Eq True False % 7.23/7.41 Clause #813 (by clausification #[812]): False % 7.23/7.41 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------