%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : SET642+3 : TPTP v9.2.0. Released v2.2.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n029.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:20 PM UTC 2025 % Result : Theorem 115.02s 115.26s % Output : Proof 115.17s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.10/0.12 % Problem : SET642+3 : TPTP v9.2.0. Released v2.2.0. % 0.10/0.13 % Command : duper %s % 0.13/0.34 % Computer : n029.cluster.edu % 0.13/0.34 % Model : x86_64 x86_64 % 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.34 % Memory : 8042.1875MB % 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.34 % CPULimit : 300 % 0.13/0.34 % WCLimit : 300 % 0.13/0.34 % DateTime : Thu Oct 2 13:52:08 EDT 2025 % 0.13/0.34 % CPUTime : % 115.02/115.26 SZS status Theorem for theBenchmark.p % 115.02/115.26 SZS output start Proof for theBenchmark.p % 115.02/115.26 Clause #0 (by assumption #[]): Eq % 115.02/115.26 (∀ (B : Iota), % 115.02/115.26 ilf_type B set_type → % 115.02/115.26 ∀ (C : Iota), % 115.02/115.26 ilf_type C set_type → % 115.02/115.26 ∀ (D : Iota), % 115.02/115.26 ilf_type D set_type → % 115.02/115.26 ∀ (E : Iota), ilf_type E (relation_type C D) → subset B E → subset B (cross_product C D)) % 115.02/115.26 True % 115.02/115.26 Clause #1 (by assumption #[]): Eq % 115.02/115.26 (∀ (B : Iota), % 115.02/115.26 ilf_type B set_type → % 115.02/115.26 ∀ (C : Iota), % 115.02/115.26 ilf_type C set_type → % 115.02/115.26 ∀ (D : Iota), ilf_type D set_type → subset B (cross_product C D) → ilf_type B (relation_type C D)) % 115.02/115.26 True % 115.02/115.26 Clause #18 (by assumption #[]): Eq (∀ (B : Iota), ilf_type B set_type) True % 115.02/115.26 Clause #19 (by assumption #[]): Eq % 115.02/115.26 (Not % 115.02/115.26 (∀ (B : Iota), % 115.02/115.26 ilf_type B set_type → % 115.02/115.26 ∀ (C : Iota), % 115.02/115.26 ilf_type C set_type → % 115.02/115.26 ∀ (D : Iota), % 115.02/115.26 ilf_type D set_type → % 115.02/115.26 ∀ (E : Iota), ilf_type E (relation_type C D) → subset B E → ilf_type B (relation_type C D))) % 115.02/115.26 True % 115.02/115.26 Clause #20 (by clausification #[18]): ∀ (a : Iota), Eq (ilf_type a set_type) True % 115.02/115.26 Clause #44 (by clausification #[0]): ∀ (a : Iota), % 115.02/115.26 Eq % 115.02/115.26 (ilf_type a set_type → % 115.02/115.26 ∀ (C : Iota), % 115.02/115.26 ilf_type C set_type → % 115.02/115.26 ∀ (D : Iota), % 115.02/115.26 ilf_type D set_type → % 115.02/115.26 ∀ (E : Iota), ilf_type E (relation_type C D) → subset a E → subset a (cross_product C D)) % 115.02/115.26 True % 115.02/115.26 Clause #45 (by clausification #[44]): ∀ (a : Iota), % 115.02/115.26 Or (Eq (ilf_type a set_type) False) % 115.02/115.26 (Eq % 115.02/115.26 (∀ (C : Iota), % 115.02/115.26 ilf_type C set_type → % 115.02/115.26 ∀ (D : Iota), % 115.02/115.26 ilf_type D set_type → % 115.02/115.26 ∀ (E : Iota), ilf_type E (relation_type C D) → subset a E → subset a (cross_product C D)) % 115.02/115.26 True) % 115.02/115.26 Clause #46 (by clausification #[45]): ∀ (a a_1 : Iota), % 115.02/115.26 Or (Eq (ilf_type a set_type) False) % 115.02/115.26 (Eq % 115.02/115.26 (ilf_type a_1 set_type → % 115.02/115.26 ∀ (D : Iota), % 115.02/115.26 ilf_type D set_type → % 115.02/115.26 ∀ (E : Iota), ilf_type E (relation_type a_1 D) → subset a E → subset a (cross_product a_1 D)) % 115.02/115.26 True) % 115.02/115.26 Clause #47 (by clausification #[46]): ∀ (a a_1 : Iota), % 115.02/115.26 Or (Eq (ilf_type a set_type) False) % 115.02/115.26 (Or (Eq (ilf_type a_1 set_type) False) % 115.02/115.26 (Eq % 115.02/115.26 (∀ (D : Iota), % 115.02/115.26 ilf_type D set_type → % 115.02/115.26 ∀ (E : Iota), ilf_type E (relation_type a_1 D) → subset a E → subset a (cross_product a_1 D)) % 115.02/115.26 True)) % 115.02/115.26 Clause #48 (by clausification #[47]): ∀ (a a_1 a_2 : Iota), % 115.02/115.26 Or (Eq (ilf_type a set_type) False) % 115.02/115.26 (Or (Eq (ilf_type a_1 set_type) False) % 115.02/115.26 (Eq % 115.02/115.26 (ilf_type a_2 set_type → % 115.02/115.26 ∀ (E : Iota), ilf_type E (relation_type a_1 a_2) → subset a E → subset a (cross_product a_1 a_2)) % 115.02/115.26 True)) % 115.02/115.26 Clause #49 (by clausification #[48]): ∀ (a a_1 a_2 : Iota), % 115.02/115.26 Or (Eq (ilf_type a set_type) False) % 115.02/115.26 (Or (Eq (ilf_type a_1 set_type) False) % 115.02/115.26 (Or (Eq (ilf_type a_2 set_type) False) % 115.02/115.26 (Eq (∀ (E : Iota), ilf_type E (relation_type a_1 a_2) → subset a E → subset a (cross_product a_1 a_2)) True))) % 115.02/115.26 Clause #50 (by clausification #[49]): ∀ (a a_1 a_2 a_3 : Iota), % 115.02/115.26 Or (Eq (ilf_type a set_type) False) % 115.02/115.26 (Or (Eq (ilf_type a_1 set_type) False) % 115.02/115.26 (Or (Eq (ilf_type a_2 set_type) False) % 115.02/115.26 (Eq (ilf_type a_3 (relation_type a_1 a_2) → subset a a_3 → subset a (cross_product a_1 a_2)) True))) % 115.02/115.26 Clause #51 (by clausification #[50]): ∀ (a a_1 a_2 a_3 : Iota), % 115.02/115.26 Or (Eq (ilf_type a set_type) False) % 115.02/115.26 (Or (Eq (ilf_type a_1 set_type) False) % 115.02/115.26 (Or (Eq (ilf_type a_2 set_type) False) % 115.02/115.26 (Or (Eq (ilf_type a_3 (relation_type a_1 a_2)) False) % 115.02/115.26 (Eq (subset a a_3 → subset a (cross_product a_1 a_2)) True)))) % 115.02/115.26 Clause #52 (by clausification #[51]): ∀ (a a_1 a_2 a_3 : Iota), % 115.02/115.26 Or (Eq (ilf_type a set_type) False) % 115.02/115.26 (Or (Eq (ilf_type a_1 set_type) False) % 115.02/115.26 (Or (Eq (ilf_type a_2 set_type) False) % 115.02/115.26 (Or (Eq (ilf_type a_3 (relation_type a_1 a_2)) False) % 115.02/115.26 (Or (Eq (subset a a_3) False) (Eq (subset a (cross_product a_1 a_2)) True))))) % 115.02/115.26 Clause #53 (by forward demodulation #[52, 20]): ∀ (a a_1 a_2 a_3 : Iota), % 115.02/115.28 Or (Eq True False) % 115.02/115.28 (Or (Eq (ilf_type a set_type) False) % 115.02/115.28 (Or (Eq (ilf_type a_1 set_type) False) % 115.02/115.28 (Or (Eq (ilf_type a_2 (relation_type a a_1)) False) % 115.02/115.28 (Or (Eq (subset a_3 a_2) False) (Eq (subset a_3 (cross_product a a_1)) True))))) % 115.02/115.28 Clause #54 (by clausification #[53]): ∀ (a a_1 a_2 a_3 : Iota), % 115.02/115.28 Or (Eq (ilf_type a set_type) False) % 115.02/115.28 (Or (Eq (ilf_type a_1 set_type) False) % 115.02/115.28 (Or (Eq (ilf_type a_2 (relation_type a a_1)) False) % 115.02/115.28 (Or (Eq (subset a_3 a_2) False) (Eq (subset a_3 (cross_product a a_1)) True)))) % 115.02/115.28 Clause #55 (by forward demodulation #[54, 20]): ∀ (a a_1 a_2 a_3 : Iota), % 115.02/115.28 Or (Eq True False) % 115.02/115.28 (Or (Eq (ilf_type a set_type) False) % 115.02/115.28 (Or (Eq (ilf_type a_1 (relation_type a_2 a)) False) % 115.02/115.28 (Or (Eq (subset a_3 a_1) False) (Eq (subset a_3 (cross_product a_2 a)) True)))) % 115.02/115.28 Clause #56 (by clausification #[55]): ∀ (a a_1 a_2 a_3 : Iota), % 115.02/115.28 Or (Eq (ilf_type a set_type) False) % 115.02/115.28 (Or (Eq (ilf_type a_1 (relation_type a_2 a)) False) % 115.02/115.28 (Or (Eq (subset a_3 a_1) False) (Eq (subset a_3 (cross_product a_2 a)) True))) % 115.02/115.28 Clause #57 (by forward demodulation #[56, 20]): ∀ (a a_1 a_2 a_3 : Iota), % 115.02/115.28 Or (Eq True False) % 115.02/115.28 (Or (Eq (ilf_type a (relation_type a_1 a_2)) False) % 115.02/115.28 (Or (Eq (subset a_3 a) False) (Eq (subset a_3 (cross_product a_1 a_2)) True))) % 115.02/115.28 Clause #58 (by clausification #[57]): ∀ (a a_1 a_2 a_3 : Iota), % 115.02/115.28 Or (Eq (ilf_type a (relation_type a_1 a_2)) False) % 115.02/115.28 (Or (Eq (subset a_3 a) False) (Eq (subset a_3 (cross_product a_1 a_2)) True)) % 115.02/115.28 Clause #98 (by clausification #[1]): ∀ (a : Iota), % 115.02/115.28 Eq % 115.02/115.28 (ilf_type a set_type → % 115.02/115.28 ∀ (C : Iota), % 115.02/115.28 ilf_type C set_type → % 115.02/115.28 ∀ (D : Iota), ilf_type D set_type → subset a (cross_product C D) → ilf_type a (relation_type C D)) % 115.02/115.28 True % 115.02/115.28 Clause #99 (by clausification #[98]): ∀ (a : Iota), % 115.02/115.28 Or (Eq (ilf_type a set_type) False) % 115.02/115.28 (Eq % 115.02/115.28 (∀ (C : Iota), % 115.02/115.28 ilf_type C set_type → % 115.02/115.28 ∀ (D : Iota), ilf_type D set_type → subset a (cross_product C D) → ilf_type a (relation_type C D)) % 115.02/115.28 True) % 115.02/115.28 Clause #100 (by clausification #[99]): ∀ (a a_1 : Iota), % 115.02/115.28 Or (Eq (ilf_type a set_type) False) % 115.02/115.28 (Eq % 115.02/115.28 (ilf_type a_1 set_type → % 115.02/115.28 ∀ (D : Iota), ilf_type D set_type → subset a (cross_product a_1 D) → ilf_type a (relation_type a_1 D)) % 115.02/115.28 True) % 115.02/115.28 Clause #101 (by clausification #[100]): ∀ (a a_1 : Iota), % 115.02/115.28 Or (Eq (ilf_type a set_type) False) % 115.02/115.28 (Or (Eq (ilf_type a_1 set_type) False) % 115.02/115.28 (Eq (∀ (D : Iota), ilf_type D set_type → subset a (cross_product a_1 D) → ilf_type a (relation_type a_1 D)) True)) % 115.02/115.28 Clause #102 (by clausification #[101]): ∀ (a a_1 a_2 : Iota), % 115.02/115.28 Or (Eq (ilf_type a set_type) False) % 115.02/115.28 (Or (Eq (ilf_type a_1 set_type) False) % 115.02/115.28 (Eq (ilf_type a_2 set_type → subset a (cross_product a_1 a_2) → ilf_type a (relation_type a_1 a_2)) True)) % 115.02/115.28 Clause #103 (by clausification #[102]): ∀ (a a_1 a_2 : Iota), % 115.02/115.28 Or (Eq (ilf_type a set_type) False) % 115.02/115.28 (Or (Eq (ilf_type a_1 set_type) False) % 115.02/115.28 (Or (Eq (ilf_type a_2 set_type) False) % 115.02/115.28 (Eq (subset a (cross_product a_1 a_2) → ilf_type a (relation_type a_1 a_2)) True))) % 115.02/115.28 Clause #104 (by clausification #[103]): ∀ (a a_1 a_2 : Iota), % 115.02/115.28 Or (Eq (ilf_type a set_type) False) % 115.02/115.28 (Or (Eq (ilf_type a_1 set_type) False) % 115.02/115.28 (Or (Eq (ilf_type a_2 set_type) False) % 115.02/115.28 (Or (Eq (subset a (cross_product a_1 a_2)) False) (Eq (ilf_type a (relation_type a_1 a_2)) True)))) % 115.02/115.28 Clause #105 (by forward demodulation #[104, 20]): ∀ (a a_1 a_2 : Iota), % 115.02/115.28 Or (Eq True False) % 115.02/115.28 (Or (Eq (ilf_type a set_type) False) % 115.02/115.28 (Or (Eq (ilf_type a_1 set_type) False) % 115.02/115.28 (Or (Eq (subset a_2 (cross_product a a_1)) False) (Eq (ilf_type a_2 (relation_type a a_1)) True)))) % 115.02/115.28 Clause #106 (by clausification #[105]): ∀ (a a_1 a_2 : Iota), % 115.02/115.28 Or (Eq (ilf_type a set_type) False) % 115.02/115.28 (Or (Eq (ilf_type a_1 set_type) False) % 115.02/115.28 (Or (Eq (subset a_2 (cross_product a a_1)) False) (Eq (ilf_type a_2 (relation_type a a_1)) True))) % 115.02/115.28 Clause #107 (by forward demodulation #[106, 20]): ∀ (a a_1 a_2 : Iota), % 115.02/115.30 Or (Eq True False) % 115.02/115.30 (Or (Eq (ilf_type a set_type) False) % 115.02/115.30 (Or (Eq (subset a_1 (cross_product a_2 a)) False) (Eq (ilf_type a_1 (relation_type a_2 a)) True))) % 115.02/115.30 Clause #108 (by clausification #[107]): ∀ (a a_1 a_2 : Iota), % 115.02/115.30 Or (Eq (ilf_type a set_type) False) % 115.02/115.30 (Or (Eq (subset a_1 (cross_product a_2 a)) False) (Eq (ilf_type a_1 (relation_type a_2 a)) True)) % 115.02/115.30 Clause #109 (by forward demodulation #[108, 20]): ∀ (a a_1 a_2 : Iota), % 115.02/115.30 Or (Eq True False) (Or (Eq (subset a (cross_product a_1 a_2)) False) (Eq (ilf_type a (relation_type a_1 a_2)) True)) % 115.02/115.30 Clause #110 (by clausification #[109]): ∀ (a a_1 a_2 : Iota), Or (Eq (subset a (cross_product a_1 a_2)) False) (Eq (ilf_type a (relation_type a_1 a_2)) True) % 115.02/115.30 Clause #197 (by clausification #[19]): Eq % 115.02/115.30 (∀ (B : Iota), % 115.02/115.30 ilf_type B set_type → % 115.02/115.30 ∀ (C : Iota), % 115.02/115.30 ilf_type C set_type → % 115.02/115.30 ∀ (D : Iota), % 115.02/115.30 ilf_type D set_type → % 115.02/115.30 ∀ (E : Iota), ilf_type E (relation_type C D) → subset B E → ilf_type B (relation_type C D)) % 115.02/115.30 False % 115.02/115.30 Clause #198 (by clausification #[197]): ∀ (a : Iota), % 115.02/115.30 Eq % 115.02/115.30 (Not % 115.02/115.30 (ilf_type (skS.0 5 a) set_type → % 115.02/115.30 ∀ (C : Iota), % 115.02/115.30 ilf_type C set_type → % 115.02/115.30 ∀ (D : Iota), % 115.02/115.30 ilf_type D set_type → % 115.02/115.30 ∀ (E : Iota), % 115.02/115.30 ilf_type E (relation_type C D) → subset (skS.0 5 a) E → ilf_type (skS.0 5 a) (relation_type C D))) % 115.02/115.30 True % 115.02/115.30 Clause #199 (by clausification #[198]): ∀ (a : Iota), % 115.02/115.30 Eq % 115.02/115.30 (ilf_type (skS.0 5 a) set_type → % 115.02/115.30 ∀ (C : Iota), % 115.02/115.30 ilf_type C set_type → % 115.02/115.30 ∀ (D : Iota), % 115.02/115.30 ilf_type D set_type → % 115.02/115.30 ∀ (E : Iota), % 115.02/115.30 ilf_type E (relation_type C D) → subset (skS.0 5 a) E → ilf_type (skS.0 5 a) (relation_type C D)) % 115.02/115.30 False % 115.02/115.30 Clause #201 (by clausification #[199]): ∀ (a : Iota), % 115.02/115.30 Eq % 115.02/115.30 (∀ (C : Iota), % 115.02/115.30 ilf_type C set_type → % 115.02/115.30 ∀ (D : Iota), % 115.02/115.30 ilf_type D set_type → % 115.02/115.30 ∀ (E : Iota), % 115.02/115.30 ilf_type E (relation_type C D) → subset (skS.0 5 a) E → ilf_type (skS.0 5 a) (relation_type C D)) % 115.02/115.30 False % 115.02/115.30 Clause #219 (by clausification #[201]): ∀ (a a_1 : Iota), % 115.02/115.30 Eq % 115.02/115.30 (Not % 115.02/115.30 (ilf_type (skS.0 7 a a_1) set_type → % 115.02/115.30 ∀ (D : Iota), % 115.02/115.30 ilf_type D set_type → % 115.02/115.30 ∀ (E : Iota), % 115.02/115.30 ilf_type E (relation_type (skS.0 7 a a_1) D) → % 115.02/115.30 subset (skS.0 5 a) E → ilf_type (skS.0 5 a) (relation_type (skS.0 7 a a_1) D))) % 115.02/115.30 True % 115.02/115.30 Clause #220 (by clausification #[219]): ∀ (a a_1 : Iota), % 115.02/115.30 Eq % 115.02/115.30 (ilf_type (skS.0 7 a a_1) set_type → % 115.02/115.30 ∀ (D : Iota), % 115.02/115.30 ilf_type D set_type → % 115.02/115.30 ∀ (E : Iota), % 115.02/115.30 ilf_type E (relation_type (skS.0 7 a a_1) D) → % 115.02/115.30 subset (skS.0 5 a) E → ilf_type (skS.0 5 a) (relation_type (skS.0 7 a a_1) D)) % 115.02/115.30 False % 115.02/115.30 Clause #222 (by clausification #[220]): ∀ (a a_1 : Iota), % 115.02/115.30 Eq % 115.02/115.30 (∀ (D : Iota), % 115.02/115.30 ilf_type D set_type → % 115.02/115.30 ∀ (E : Iota), % 115.02/115.30 ilf_type E (relation_type (skS.0 7 a a_1) D) → % 115.02/115.30 subset (skS.0 5 a) E → ilf_type (skS.0 5 a) (relation_type (skS.0 7 a a_1) D)) % 115.02/115.30 False % 115.02/115.30 Clause #368 (by clausification #[222]): ∀ (a a_1 a_2 : Iota), % 115.02/115.30 Eq % 115.02/115.30 (Not % 115.02/115.30 (ilf_type (skS.0 9 a a_1 a_2) set_type → % 115.02/115.30 ∀ (E : Iota), % 115.02/115.30 ilf_type E (relation_type (skS.0 7 a a_1) (skS.0 9 a a_1 a_2)) → % 115.02/115.30 subset (skS.0 5 a) E → ilf_type (skS.0 5 a) (relation_type (skS.0 7 a a_1) (skS.0 9 a a_1 a_2)))) % 115.02/115.30 True % 115.02/115.30 Clause #369 (by clausification #[368]): ∀ (a a_1 a_2 : Iota), % 115.02/115.30 Eq % 115.02/115.30 (ilf_type (skS.0 9 a a_1 a_2) set_type → % 115.02/115.30 ∀ (E : Iota), % 115.02/115.30 ilf_type E (relation_type (skS.0 7 a a_1) (skS.0 9 a a_1 a_2)) → % 115.02/115.30 subset (skS.0 5 a) E → ilf_type (skS.0 5 a) (relation_type (skS.0 7 a a_1) (skS.0 9 a a_1 a_2))) % 115.02/115.30 False % 115.02/115.30 Clause #371 (by clausification #[369]): ∀ (a a_1 a_2 : Iota), % 115.02/115.30 Eq % 115.02/115.30 (∀ (E : Iota), % 115.02/115.30 ilf_type E (relation_type (skS.0 7 a a_1) (skS.0 9 a a_1 a_2)) → % 115.02/115.30 subset (skS.0 5 a) E → ilf_type (skS.0 5 a) (relation_type (skS.0 7 a a_1) (skS.0 9 a a_1 a_2))) % 115.17/115.39 False % 115.17/115.39 Clause #700 (by clausification #[371]): ∀ (a a_1 a_2 a_3 : Iota), % 115.17/115.39 Eq % 115.17/115.39 (Not % 115.17/115.39 (ilf_type (skS.0 12 a a_1 a_2 a_3) (relation_type (skS.0 7 a a_1) (skS.0 9 a a_1 a_2)) → % 115.17/115.39 subset (skS.0 5 a) (skS.0 12 a a_1 a_2 a_3) → % 115.17/115.39 ilf_type (skS.0 5 a) (relation_type (skS.0 7 a a_1) (skS.0 9 a a_1 a_2)))) % 115.17/115.39 True % 115.17/115.39 Clause #701 (by clausification #[700]): ∀ (a a_1 a_2 a_3 : Iota), % 115.17/115.39 Eq % 115.17/115.39 (ilf_type (skS.0 12 a a_1 a_2 a_3) (relation_type (skS.0 7 a a_1) (skS.0 9 a a_1 a_2)) → % 115.17/115.39 subset (skS.0 5 a) (skS.0 12 a a_1 a_2 a_3) → % 115.17/115.39 ilf_type (skS.0 5 a) (relation_type (skS.0 7 a a_1) (skS.0 9 a a_1 a_2))) % 115.17/115.39 False % 115.17/115.39 Clause #702 (by clausification #[701]): ∀ (a a_1 a_2 a_3 : Iota), % 115.17/115.39 Eq (ilf_type (skS.0 12 a a_1 a_2 a_3) (relation_type (skS.0 7 a a_1) (skS.0 9 a a_1 a_2))) True % 115.17/115.39 Clause #703 (by clausification #[701]): ∀ (a a_1 a_2 a_3 : Iota), % 115.17/115.39 Eq % 115.17/115.39 (subset (skS.0 5 a) (skS.0 12 a a_1 a_2 a_3) → % 115.17/115.39 ilf_type (skS.0 5 a) (relation_type (skS.0 7 a a_1) (skS.0 9 a a_1 a_2))) % 115.17/115.39 False % 115.17/115.39 Clause #704 (by superposition #[702, 58]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 115.17/115.39 Or (Eq True False) % 115.17/115.39 (Or (Eq (subset a (skS.0 12 a_1 a_2 a_3 a_4)) False) % 115.17/115.39 (Eq (subset a (cross_product (skS.0 7 a_1 a_2) (skS.0 9 a_1 a_2 a_3))) True)) % 115.17/115.39 Clause #923 (by clausification #[703]): ∀ (a a_1 a_2 a_3 : Iota), Eq (subset (skS.0 5 a) (skS.0 12 a a_1 a_2 a_3)) True % 115.17/115.39 Clause #924 (by clausification #[703]): ∀ (a a_1 a_2 : Iota), Eq (ilf_type (skS.0 5 a) (relation_type (skS.0 7 a a_1) (skS.0 9 a a_1 a_2))) False % 115.17/115.39 Clause #9095 (by clausification #[704]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 115.17/115.39 Or (Eq (subset a (skS.0 12 a_1 a_2 a_3 a_4)) False) % 115.17/115.39 (Eq (subset a (cross_product (skS.0 7 a_1 a_2) (skS.0 9 a_1 a_2 a_3))) True) % 115.17/115.39 Clause #9096 (by superposition #[9095, 923]): ∀ (a a_1 a_2 : Iota), % 115.17/115.39 Or (Eq (subset (skS.0 5 a) (cross_product (skS.0 7 a a_1) (skS.0 9 a a_1 a_2))) True) (Eq False True) % 115.17/115.39 Clause #9105 (by clausification #[9096]): ∀ (a a_1 a_2 : Iota), Eq (subset (skS.0 5 a) (cross_product (skS.0 7 a a_1) (skS.0 9 a a_1 a_2))) True % 115.17/115.39 Clause #9106 (by superposition #[9105, 110]): ∀ (a a_1 a_2 : Iota), % 115.17/115.39 Or (Eq True False) (Eq (ilf_type (skS.0 5 a) (relation_type (skS.0 7 a a_1) (skS.0 9 a a_1 a_2))) True) % 115.17/115.39 Clause #9108 (by clausification #[9106]): ∀ (a a_1 a_2 : Iota), Eq (ilf_type (skS.0 5 a) (relation_type (skS.0 7 a a_1) (skS.0 9 a a_1 a_2))) True % 115.17/115.39 Clause #9109 (by superposition #[9108, 924]): Eq True False % 115.17/115.39 Clause #9112 (by clausification #[9109]): False % 115.17/115.39 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------