%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : GEO176+2 : TPTP v9.2.0. Released v3.3.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n011.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:48:07 PM UTC 2025 % Result : Theorem 57.08s 57.33s % Output : Proof 57.11s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.11/0.12 % Problem : GEO176+2 : TPTP v9.2.0. Released v3.3.0. % 0.11/0.13 % Command : duper %s % 0.12/0.34 % Computer : n011.cluster.edu % 0.12/0.34 % Model : x86_64 x86_64 % 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.34 % Memory : 8042.1875MB % 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.34 % CPULimit : 300 % 0.12/0.34 % WCLimit : 300 % 0.12/0.34 % DateTime : Fri Oct 3 11:22:53 EDT 2025 % 0.12/0.35 % CPUTime : % 57.08/57.33 SZS status Theorem for theBenchmark.p % 57.08/57.33 SZS output start Proof for theBenchmark.p % 57.08/57.33 Clause #7 (by assumption #[]): Eq % 57.08/57.33 (∀ (X Y Z : Iota), % 57.08/57.33 convergent_lines X Y → % 57.08/57.33 Or (apart_point_and_line Z X) (apart_point_and_line Z Y) → distinct_points Z (intersection_point X Y)) % 57.08/57.33 True % 57.08/57.33 Clause #12 (by assumption #[]): Eq % 57.08/57.33 (Not % 57.08/57.33 (∀ (X Y U V : Iota), % 57.08/57.33 And (And (distinct_points X Y) (convergent_lines U V)) % 57.08/57.33 (Or (apart_point_and_line X U) (apart_point_and_line X V)) → % 57.08/57.33 distinct_points X (intersection_point U V))) % 57.08/57.33 True % 57.08/57.33 Clause #22 (by clausification #[7]): ∀ (a : Iota), % 57.08/57.33 Eq % 57.08/57.33 (∀ (Y Z : Iota), % 57.08/57.33 convergent_lines a Y → % 57.08/57.33 Or (apart_point_and_line Z a) (apart_point_and_line Z Y) → distinct_points Z (intersection_point a Y)) % 57.08/57.33 True % 57.08/57.33 Clause #23 (by clausification #[22]): ∀ (a a_1 : Iota), % 57.08/57.33 Eq % 57.08/57.33 (∀ (Z : Iota), % 57.08/57.33 convergent_lines a a_1 → % 57.08/57.33 Or (apart_point_and_line Z a) (apart_point_and_line Z a_1) → distinct_points Z (intersection_point a a_1)) % 57.08/57.33 True % 57.08/57.33 Clause #24 (by clausification #[23]): ∀ (a a_1 a_2 : Iota), % 57.08/57.33 Eq % 57.08/57.33 (convergent_lines a a_1 → % 57.08/57.33 Or (apart_point_and_line a_2 a) (apart_point_and_line a_2 a_1) → distinct_points a_2 (intersection_point a a_1)) % 57.08/57.33 True % 57.08/57.33 Clause #25 (by clausification #[24]): ∀ (a a_1 a_2 : Iota), % 57.08/57.33 Or (Eq (convergent_lines a a_1) False) % 57.08/57.33 (Eq % 57.08/57.33 (Or (apart_point_and_line a_2 a) (apart_point_and_line a_2 a_1) → distinct_points a_2 (intersection_point a a_1)) % 57.08/57.33 True) % 57.08/57.33 Clause #26 (by clausification #[25]): ∀ (a a_1 a_2 : Iota), % 57.08/57.33 Or (Eq (convergent_lines a a_1) False) % 57.08/57.33 (Or (Eq (Or (apart_point_and_line a_2 a) (apart_point_and_line a_2 a_1)) False) % 57.08/57.33 (Eq (distinct_points a_2 (intersection_point a a_1)) True)) % 57.08/57.33 Clause #27 (by clausification #[26]): ∀ (a a_1 a_2 : Iota), % 57.08/57.33 Or (Eq (convergent_lines a a_1) False) % 57.08/57.33 (Or (Eq (distinct_points a_2 (intersection_point a a_1)) True) (Eq (apart_point_and_line a_2 a_1) False)) % 57.08/57.33 Clause #28 (by clausification #[26]): ∀ (a a_1 a_2 : Iota), % 57.08/57.33 Or (Eq (convergent_lines a a_1) False) % 57.08/57.33 (Or (Eq (distinct_points a_2 (intersection_point a a_1)) True) (Eq (apart_point_and_line a_2 a) False)) % 57.08/57.33 Clause #54 (by clausification #[12]): Eq % 57.08/57.33 (∀ (X Y U V : Iota), % 57.08/57.33 And (And (distinct_points X Y) (convergent_lines U V)) (Or (apart_point_and_line X U) (apart_point_and_line X V)) → % 57.08/57.33 distinct_points X (intersection_point U V)) % 57.08/57.33 False % 57.08/57.33 Clause #55 (by clausification #[54]): ∀ (a : Iota), % 57.08/57.33 Eq % 57.08/57.33 (Not % 57.08/57.33 (∀ (Y U V : Iota), % 57.08/57.33 And (And (distinct_points (skS.0 0 a) Y) (convergent_lines U V)) % 57.08/57.33 (Or (apart_point_and_line (skS.0 0 a) U) (apart_point_and_line (skS.0 0 a) V)) → % 57.08/57.33 distinct_points (skS.0 0 a) (intersection_point U V))) % 57.08/57.33 True % 57.08/57.33 Clause #56 (by clausification #[55]): ∀ (a : Iota), % 57.08/57.33 Eq % 57.08/57.33 (∀ (Y U V : Iota), % 57.08/57.33 And (And (distinct_points (skS.0 0 a) Y) (convergent_lines U V)) % 57.08/57.33 (Or (apart_point_and_line (skS.0 0 a) U) (apart_point_and_line (skS.0 0 a) V)) → % 57.08/57.33 distinct_points (skS.0 0 a) (intersection_point U V)) % 57.08/57.33 False % 57.08/57.33 Clause #57 (by clausification #[56]): ∀ (a a_1 : Iota), % 57.08/57.33 Eq % 57.08/57.33 (Not % 57.08/57.33 (∀ (U V : Iota), % 57.08/57.33 And (And (distinct_points (skS.0 0 a) (skS.0 1 a a_1)) (convergent_lines U V)) % 57.08/57.33 (Or (apart_point_and_line (skS.0 0 a) U) (apart_point_and_line (skS.0 0 a) V)) → % 57.08/57.33 distinct_points (skS.0 0 a) (intersection_point U V))) % 57.08/57.33 True % 57.08/57.33 Clause #58 (by clausification #[57]): ∀ (a a_1 : Iota), % 57.08/57.33 Eq % 57.08/57.33 (∀ (U V : Iota), % 57.08/57.33 And (And (distinct_points (skS.0 0 a) (skS.0 1 a a_1)) (convergent_lines U V)) % 57.08/57.33 (Or (apart_point_and_line (skS.0 0 a) U) (apart_point_and_line (skS.0 0 a) V)) → % 57.08/57.33 distinct_points (skS.0 0 a) (intersection_point U V)) % 57.08/57.33 False % 57.08/57.33 Clause #59 (by clausification #[58]): ∀ (a a_1 a_2 : Iota), % 57.08/57.33 Eq % 57.08/57.33 (Not % 57.08/57.33 (∀ (V : Iota), % 57.08/57.33 And (And (distinct_points (skS.0 0 a) (skS.0 1 a a_1)) (convergent_lines (skS.0 2 a a_1 a_2) V)) % 57.08/57.33 (Or (apart_point_and_line (skS.0 0 a) (skS.0 2 a a_1 a_2)) (apart_point_and_line (skS.0 0 a) V)) → % 57.08/57.33 distinct_points (skS.0 0 a) (intersection_point (skS.0 2 a a_1 a_2) V))) % 57.11/57.35 True % 57.11/57.35 Clause #60 (by clausification #[59]): ∀ (a a_1 a_2 : Iota), % 57.11/57.35 Eq % 57.11/57.35 (∀ (V : Iota), % 57.11/57.35 And (And (distinct_points (skS.0 0 a) (skS.0 1 a a_1)) (convergent_lines (skS.0 2 a a_1 a_2) V)) % 57.11/57.35 (Or (apart_point_and_line (skS.0 0 a) (skS.0 2 a a_1 a_2)) (apart_point_and_line (skS.0 0 a) V)) → % 57.11/57.35 distinct_points (skS.0 0 a) (intersection_point (skS.0 2 a a_1 a_2) V)) % 57.11/57.35 False % 57.11/57.35 Clause #61 (by clausification #[60]): ∀ (a a_1 a_2 a_3 : Iota), % 57.11/57.35 Eq % 57.11/57.35 (Not % 57.11/57.35 (And % 57.11/57.35 (And (distinct_points (skS.0 0 a) (skS.0 1 a a_1)) % 57.11/57.35 (convergent_lines (skS.0 2 a a_1 a_2) (skS.0 3 a a_1 a_2 a_3))) % 57.11/57.35 (Or (apart_point_and_line (skS.0 0 a) (skS.0 2 a a_1 a_2)) % 57.11/57.35 (apart_point_and_line (skS.0 0 a) (skS.0 3 a a_1 a_2 a_3))) → % 57.11/57.35 distinct_points (skS.0 0 a) (intersection_point (skS.0 2 a a_1 a_2) (skS.0 3 a a_1 a_2 a_3)))) % 57.11/57.35 True % 57.11/57.35 Clause #62 (by clausification #[61]): ∀ (a a_1 a_2 a_3 : Iota), % 57.11/57.35 Eq % 57.11/57.35 (And % 57.11/57.35 (And (distinct_points (skS.0 0 a) (skS.0 1 a a_1)) % 57.11/57.35 (convergent_lines (skS.0 2 a a_1 a_2) (skS.0 3 a a_1 a_2 a_3))) % 57.11/57.35 (Or (apart_point_and_line (skS.0 0 a) (skS.0 2 a a_1 a_2)) % 57.11/57.35 (apart_point_and_line (skS.0 0 a) (skS.0 3 a a_1 a_2 a_3))) → % 57.11/57.35 distinct_points (skS.0 0 a) (intersection_point (skS.0 2 a a_1 a_2) (skS.0 3 a a_1 a_2 a_3))) % 57.11/57.35 False % 57.11/57.35 Clause #63 (by clausification #[62]): ∀ (a a_1 a_2 a_3 : Iota), % 57.11/57.35 Eq % 57.11/57.35 (And % 57.11/57.35 (And (distinct_points (skS.0 0 a) (skS.0 1 a a_1)) (convergent_lines (skS.0 2 a a_1 a_2) (skS.0 3 a a_1 a_2 a_3))) % 57.11/57.35 (Or (apart_point_and_line (skS.0 0 a) (skS.0 2 a a_1 a_2)) % 57.11/57.35 (apart_point_and_line (skS.0 0 a) (skS.0 3 a a_1 a_2 a_3)))) % 57.11/57.35 True % 57.11/57.35 Clause #64 (by clausification #[62]): ∀ (a a_1 a_2 a_3 : Iota), % 57.11/57.35 Eq (distinct_points (skS.0 0 a) (intersection_point (skS.0 2 a a_1 a_2) (skS.0 3 a a_1 a_2 a_3))) False % 57.11/57.35 Clause #65 (by clausification #[63]): ∀ (a a_1 a_2 a_3 : Iota), % 57.11/57.35 Eq % 57.11/57.35 (Or (apart_point_and_line (skS.0 0 a) (skS.0 2 a a_1 a_2)) % 57.11/57.35 (apart_point_and_line (skS.0 0 a) (skS.0 3 a a_1 a_2 a_3))) % 57.11/57.35 True % 57.11/57.35 Clause #66 (by clausification #[63]): ∀ (a a_1 a_2 a_3 : Iota), % 57.11/57.35 Eq (And (distinct_points (skS.0 0 a) (skS.0 1 a a_1)) (convergent_lines (skS.0 2 a a_1 a_2) (skS.0 3 a a_1 a_2 a_3))) % 57.11/57.35 True % 57.11/57.35 Clause #67 (by clausification #[65]): ∀ (a a_1 a_2 a_3 : Iota), % 57.11/57.35 Or (Eq (apart_point_and_line (skS.0 0 a) (skS.0 2 a a_1 a_2)) True) % 57.11/57.35 (Eq (apart_point_and_line (skS.0 0 a) (skS.0 3 a a_1 a_2 a_3)) True) % 57.11/57.35 Clause #86 (by clausification #[66]): ∀ (a a_1 a_2 a_3 : Iota), Eq (convergent_lines (skS.0 2 a a_1 a_2) (skS.0 3 a a_1 a_2 a_3)) True % 57.11/57.35 Clause #89 (by superposition #[86, 27]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 57.11/57.35 Or (Eq True False) % 57.11/57.35 (Or (Eq (distinct_points a (intersection_point (skS.0 2 a_1 a_2 a_3) (skS.0 3 a_1 a_2 a_3 a_4))) True) % 57.11/57.35 (Eq (apart_point_and_line a (skS.0 3 a_1 a_2 a_3 a_4)) False)) % 57.11/57.35 Clause #91 (by superposition #[86, 28]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 57.11/57.35 Or (Eq True False) % 57.11/57.35 (Or (Eq (distinct_points a (intersection_point (skS.0 2 a_1 a_2 a_3) (skS.0 3 a_1 a_2 a_3 a_4))) True) % 57.11/57.35 (Eq (apart_point_and_line a (skS.0 2 a_1 a_2 a_3)) False)) % 57.11/57.35 Clause #141 (by clausification #[89]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 57.11/57.35 Or (Eq (distinct_points a (intersection_point (skS.0 2 a_1 a_2 a_3) (skS.0 3 a_1 a_2 a_3 a_4))) True) % 57.11/57.35 (Eq (apart_point_and_line a (skS.0 3 a_1 a_2 a_3 a_4)) False) % 57.11/57.35 Clause #142 (by superposition #[141, 67]): ∀ (a a_1 a_2 a_3 : Iota), % 57.11/57.35 Or (Eq (distinct_points (skS.0 0 a) (intersection_point (skS.0 2 a a_1 a_2) (skS.0 3 a a_1 a_2 a_3))) True) % 57.11/57.35 (Or (Eq (apart_point_and_line (skS.0 0 a) (skS.0 2 a a_1 a_2)) True) (Eq False True)) % 57.11/57.35 Clause #217 (by clausification #[91]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 57.11/57.35 Or (Eq (distinct_points a (intersection_point (skS.0 2 a_1 a_2 a_3) (skS.0 3 a_1 a_2 a_3 a_4))) True) % 57.11/57.35 (Eq (apart_point_and_line a (skS.0 2 a_1 a_2 a_3)) False) % 57.11/57.35 Clause #1076 (by clausification #[142]): ∀ (a a_1 a_2 a_3 : Iota), % 57.11/57.35 Or (Eq (distinct_points (skS.0 0 a) (intersection_point (skS.0 2 a a_1 a_2) (skS.0 3 a a_1 a_2 a_3))) True) % 57.11/57.41 (Eq (apart_point_and_line (skS.0 0 a) (skS.0 2 a a_1 a_2)) True) % 57.11/57.41 Clause #1077 (by superposition #[1076, 64]): ∀ (a a_1 a_2 : Iota), Or (Eq (apart_point_and_line (skS.0 0 a) (skS.0 2 a a_1 a_2)) True) (Eq True False) % 57.11/57.41 Clause #1082 (by clausification #[1077]): ∀ (a a_1 a_2 : Iota), Eq (apart_point_and_line (skS.0 0 a) (skS.0 2 a a_1 a_2)) True % 57.11/57.41 Clause #1085 (by superposition #[1082, 217]): ∀ (a a_1 a_2 a_3 : Iota), % 57.11/57.41 Or (Eq (distinct_points (skS.0 0 a) (intersection_point (skS.0 2 a a_1 a_2) (skS.0 3 a a_1 a_2 a_3))) True) % 57.11/57.41 (Eq True False) % 57.11/57.41 Clause #5285 (by clausification #[1085]): ∀ (a a_1 a_2 a_3 : Iota), % 57.11/57.41 Eq (distinct_points (skS.0 0 a) (intersection_point (skS.0 2 a a_1 a_2) (skS.0 3 a a_1 a_2 a_3))) True % 57.11/57.41 Clause #5286 (by superposition #[5285, 64]): Eq True False % 57.11/57.41 Clause #5291 (by clausification #[5286]): False % 57.11/57.41 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------