%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : GEO245+3 : TPTP v9.2.0. Released v4.0.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:21 PM UTC 2025 % Result : Theorem 7.21s 7.43s % Output : Proof 7.21s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.09/0.12 % Problem : GEO245+3 : TPTP v9.2.0. Released v4.0.0. % 0.09/0.13 % Command : duper %s % 0.11/0.33 % Computer : n011.cluster.edu % 0.11/0.33 % Model : x86_64 x86_64 % 0.11/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.11/0.33 % Memory : 8042.1875MB % 0.11/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.11/0.33 % CPULimit : 300 % 0.11/0.33 % WCLimit : 300 % 0.11/0.33 % DateTime : Fri Oct 3 11:25:38 EDT 2025 % 0.11/0.33 % CPUTime : % 7.21/7.43 SZS status Theorem for theBenchmark.p % 7.21/7.43 SZS output start Proof for theBenchmark.p % 7.21/7.43 Clause #19 (by assumption #[]): Eq (∀ (A L : Iota), Not (Or (left_apart_point A L) (left_apart_point A (reverse_line L)))) True % 7.21/7.43 Clause #36 (by assumption #[]): Eq % 7.21/7.43 (Not % 7.21/7.43 (∀ (A B C : Iota), % 7.21/7.43 distinct_points A B → left_apart_point C (line_connecting A B) → right_apart_point B (line_connecting A C))) % 7.21/7.43 True % 7.21/7.43 Clause #163 (by clausification #[19]): ∀ (a : Iota), Eq (∀ (L : Iota), Not (Or (left_apart_point a L) (left_apart_point a (reverse_line L)))) True % 7.21/7.43 Clause #164 (by clausification #[163]): ∀ (a a_1 : Iota), Eq (Not (Or (left_apart_point a a_1) (left_apart_point a (reverse_line a_1)))) True % 7.21/7.43 Clause #165 (by clausification #[164]): ∀ (a a_1 : Iota), Eq (Or (left_apart_point a a_1) (left_apart_point a (reverse_line a_1))) False % 7.21/7.43 Clause #167 (by clausification #[165]): ∀ (a a_1 : Iota), Eq (left_apart_point a a_1) False % 7.21/7.43 Clause #258 (by clausification #[36]): Eq % 7.21/7.43 (∀ (A B C : Iota), % 7.21/7.43 distinct_points A B → left_apart_point C (line_connecting A B) → right_apart_point B (line_connecting A C)) % 7.21/7.43 False % 7.21/7.43 Clause #259 (by clausification #[258]): ∀ (a : Iota), % 7.21/7.43 Eq % 7.21/7.43 (Not % 7.21/7.43 (∀ (B C : Iota), % 7.21/7.43 distinct_points (skS.0 0 a) B → % 7.21/7.43 left_apart_point C (line_connecting (skS.0 0 a) B) → right_apart_point B (line_connecting (skS.0 0 a) C))) % 7.21/7.43 True % 7.21/7.43 Clause #260 (by clausification #[259]): ∀ (a : Iota), % 7.21/7.43 Eq % 7.21/7.43 (∀ (B C : Iota), % 7.21/7.43 distinct_points (skS.0 0 a) B → % 7.21/7.43 left_apart_point C (line_connecting (skS.0 0 a) B) → right_apart_point B (line_connecting (skS.0 0 a) C)) % 7.21/7.43 False % 7.21/7.43 Clause #261 (by clausification #[260]): ∀ (a a_1 : Iota), % 7.21/7.43 Eq % 7.21/7.43 (Not % 7.21/7.43 (∀ (C : Iota), % 7.21/7.43 distinct_points (skS.0 0 a) (skS.0 1 a a_1) → % 7.21/7.43 left_apart_point C (line_connecting (skS.0 0 a) (skS.0 1 a a_1)) → % 7.21/7.43 right_apart_point (skS.0 1 a a_1) (line_connecting (skS.0 0 a) C))) % 7.21/7.43 True % 7.21/7.43 Clause #262 (by clausification #[261]): ∀ (a a_1 : Iota), % 7.21/7.43 Eq % 7.21/7.43 (∀ (C : Iota), % 7.21/7.43 distinct_points (skS.0 0 a) (skS.0 1 a a_1) → % 7.21/7.43 left_apart_point C (line_connecting (skS.0 0 a) (skS.0 1 a a_1)) → % 7.21/7.43 right_apart_point (skS.0 1 a a_1) (line_connecting (skS.0 0 a) C)) % 7.21/7.43 False % 7.21/7.43 Clause #263 (by clausification #[262]): ∀ (a a_1 a_2 : Iota), % 7.21/7.43 Eq % 7.21/7.43 (Not % 7.21/7.43 (distinct_points (skS.0 0 a) (skS.0 1 a a_1) → % 7.21/7.43 left_apart_point (skS.0 2 a a_1 a_2) (line_connecting (skS.0 0 a) (skS.0 1 a a_1)) → % 7.21/7.43 right_apart_point (skS.0 1 a a_1) (line_connecting (skS.0 0 a) (skS.0 2 a a_1 a_2)))) % 7.21/7.43 True % 7.21/7.43 Clause #264 (by clausification #[263]): ∀ (a a_1 a_2 : Iota), % 7.21/7.43 Eq % 7.21/7.43 (distinct_points (skS.0 0 a) (skS.0 1 a a_1) → % 7.21/7.43 left_apart_point (skS.0 2 a a_1 a_2) (line_connecting (skS.0 0 a) (skS.0 1 a a_1)) → % 7.21/7.43 right_apart_point (skS.0 1 a a_1) (line_connecting (skS.0 0 a) (skS.0 2 a a_1 a_2))) % 7.21/7.43 False % 7.21/7.43 Clause #266 (by clausification #[264]): ∀ (a a_1 a_2 : Iota), % 7.21/7.43 Eq % 7.21/7.43 (left_apart_point (skS.0 2 a a_1 a_2) (line_connecting (skS.0 0 a) (skS.0 1 a a_1)) → % 7.21/7.43 right_apart_point (skS.0 1 a a_1) (line_connecting (skS.0 0 a) (skS.0 2 a a_1 a_2))) % 7.21/7.43 False % 7.21/7.43 Clause #1053 (by clausification #[266]): ∀ (a a_1 a_2 : Iota), Eq (left_apart_point (skS.0 2 a a_1 a_2) (line_connecting (skS.0 0 a) (skS.0 1 a a_1))) True % 7.21/7.43 Clause #1055 (by superposition #[1053, 167]): Eq True False % 7.21/7.43 Clause #1056 (by clausification #[1055]): False % 7.21/7.43 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------