%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : GEO220+2 : TPTP v9.2.0. Released v3.3.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n015.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:16 PM UTC 2025 % Result : Theorem 4.37s 4.56s % Output : Proof 4.40s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.06/0.12 % Problem : GEO220+2 : TPTP v9.2.0. Released v3.3.0. % 0.06/0.13 % Command : duper %s % 0.13/0.34 % Computer : n015.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 : Fri Oct 3 12:32:23 EDT 2025 % 0.13/0.35 % CPUTime : % 4.37/4.56 SZS status Theorem for theBenchmark.p % 4.37/4.56 SZS output start Proof for theBenchmark.p % 4.37/4.56 Clause #14 (by assumption #[]): Eq (∀ (L M N : Iota), And (Not (unorthogonal_lines L M)) (Not (unorthogonal_lines L N)) → Not (convergent_lines M N)) % 4.37/4.56 True % 4.37/4.56 Clause #15 (by assumption #[]): Eq % 4.37/4.56 (Not % 4.37/4.56 (∀ (L M N : Iota), And (Not (unorthogonal_lines L M)) (Not (unorthogonal_lines L N)) → Not (convergent_lines M N))) % 4.37/4.56 True % 4.37/4.56 Clause #25 (by clausification #[14]): ∀ (a : Iota), % 4.37/4.56 Eq (∀ (M N : Iota), And (Not (unorthogonal_lines a M)) (Not (unorthogonal_lines a N)) → Not (convergent_lines M N)) % 4.37/4.56 True % 4.37/4.56 Clause #26 (by clausification #[25]): ∀ (a a_1 : Iota), % 4.37/4.56 Eq (∀ (N : Iota), And (Not (unorthogonal_lines a a_1)) (Not (unorthogonal_lines a N)) → Not (convergent_lines a_1 N)) % 4.37/4.56 True % 4.37/4.56 Clause #27 (by clausification #[26]): ∀ (a a_1 a_2 : Iota), % 4.37/4.56 Eq (And (Not (unorthogonal_lines a a_1)) (Not (unorthogonal_lines a a_2)) → Not (convergent_lines a_1 a_2)) True % 4.37/4.56 Clause #28 (by clausification #[27]): ∀ (a a_1 a_2 : Iota), % 4.37/4.56 Or (Eq (And (Not (unorthogonal_lines a a_1)) (Not (unorthogonal_lines a a_2))) False) % 4.37/4.56 (Eq (Not (convergent_lines a_1 a_2)) True) % 4.37/4.56 Clause #29 (by clausification #[28]): ∀ (a a_1 a_2 : Iota), % 4.37/4.56 Or (Eq (Not (convergent_lines a a_1)) True) % 4.37/4.56 (Or (Eq (Not (unorthogonal_lines a_2 a)) False) (Eq (Not (unorthogonal_lines a_2 a_1)) False)) % 4.37/4.56 Clause #30 (by clausification #[29]): ∀ (a a_1 a_2 : Iota), % 4.37/4.56 Or (Eq (Not (unorthogonal_lines a a_1)) False) % 4.37/4.56 (Or (Eq (Not (unorthogonal_lines a a_2)) False) (Eq (convergent_lines a_1 a_2) False)) % 4.37/4.56 Clause #31 (by clausification #[30]): ∀ (a a_1 a_2 : Iota), % 4.37/4.56 Or (Eq (Not (unorthogonal_lines a a_1)) False) % 4.37/4.56 (Or (Eq (convergent_lines a_2 a_1) False) (Eq (unorthogonal_lines a a_2) True)) % 4.37/4.56 Clause #32 (by clausification #[31]): ∀ (a a_1 a_2 : Iota), % 4.37/4.56 Or (Eq (convergent_lines a a_1) False) % 4.37/4.56 (Or (Eq (unorthogonal_lines a_2 a) True) (Eq (unorthogonal_lines a_2 a_1) True)) % 4.37/4.56 Clause #38 (by clausification #[15]): Eq (∀ (L M N : Iota), And (Not (unorthogonal_lines L M)) (Not (unorthogonal_lines L N)) → Not (convergent_lines M N)) % 4.37/4.56 False % 4.37/4.56 Clause #39 (by clausification #[38]): ∀ (a : Iota), % 4.37/4.56 Eq % 4.37/4.56 (Not % 4.37/4.56 (∀ (M N : Iota), % 4.37/4.56 And (Not (unorthogonal_lines (skS.0 0 a) M)) (Not (unorthogonal_lines (skS.0 0 a) N)) → % 4.37/4.56 Not (convergent_lines M N))) % 4.37/4.56 True % 4.37/4.56 Clause #40 (by clausification #[39]): ∀ (a : Iota), % 4.37/4.56 Eq % 4.37/4.56 (∀ (M N : Iota), % 4.37/4.56 And (Not (unorthogonal_lines (skS.0 0 a) M)) (Not (unorthogonal_lines (skS.0 0 a) N)) → % 4.37/4.56 Not (convergent_lines M N)) % 4.37/4.56 False % 4.37/4.56 Clause #41 (by clausification #[40]): ∀ (a a_1 : Iota), % 4.37/4.56 Eq % 4.37/4.56 (Not % 4.37/4.56 (∀ (N : Iota), % 4.37/4.56 And (Not (unorthogonal_lines (skS.0 0 a) (skS.0 1 a a_1))) (Not (unorthogonal_lines (skS.0 0 a) N)) → % 4.37/4.56 Not (convergent_lines (skS.0 1 a a_1) N))) % 4.37/4.56 True % 4.37/4.56 Clause #42 (by clausification #[41]): ∀ (a a_1 : Iota), % 4.37/4.56 Eq % 4.37/4.56 (∀ (N : Iota), % 4.37/4.56 And (Not (unorthogonal_lines (skS.0 0 a) (skS.0 1 a a_1))) (Not (unorthogonal_lines (skS.0 0 a) N)) → % 4.37/4.56 Not (convergent_lines (skS.0 1 a a_1) N)) % 4.37/4.56 False % 4.37/4.56 Clause #43 (by clausification #[42]): ∀ (a a_1 a_2 : Iota), % 4.37/4.56 Eq % 4.37/4.56 (Not % 4.37/4.56 (And (Not (unorthogonal_lines (skS.0 0 a) (skS.0 1 a a_1))) % 4.37/4.56 (Not (unorthogonal_lines (skS.0 0 a) (skS.0 2 a a_1 a_2))) → % 4.37/4.56 Not (convergent_lines (skS.0 1 a a_1) (skS.0 2 a a_1 a_2)))) % 4.37/4.56 True % 4.37/4.56 Clause #44 (by clausification #[43]): ∀ (a a_1 a_2 : Iota), % 4.37/4.56 Eq % 4.37/4.56 (And (Not (unorthogonal_lines (skS.0 0 a) (skS.0 1 a a_1))) % 4.37/4.56 (Not (unorthogonal_lines (skS.0 0 a) (skS.0 2 a a_1 a_2))) → % 4.37/4.56 Not (convergent_lines (skS.0 1 a a_1) (skS.0 2 a a_1 a_2))) % 4.37/4.56 False % 4.37/4.56 Clause #45 (by clausification #[44]): ∀ (a a_1 a_2 : Iota), % 4.37/4.56 Eq % 4.37/4.56 (And (Not (unorthogonal_lines (skS.0 0 a) (skS.0 1 a a_1))) % 4.37/4.56 (Not (unorthogonal_lines (skS.0 0 a) (skS.0 2 a a_1 a_2)))) % 4.37/4.56 True % 4.37/4.56 Clause #46 (by clausification #[44]): ∀ (a a_1 a_2 : Iota), Eq (Not (convergent_lines (skS.0 1 a a_1) (skS.0 2 a a_1 a_2))) False % 4.37/4.56 Clause #47 (by clausification #[45]): ∀ (a a_1 a_2 : Iota), Eq (Not (unorthogonal_lines (skS.0 0 a) (skS.0 2 a a_1 a_2))) True % 4.40/4.57 Clause #48 (by clausification #[45]): ∀ (a a_1 : Iota), Eq (Not (unorthogonal_lines (skS.0 0 a) (skS.0 1 a a_1))) True % 4.40/4.57 Clause #49 (by clausification #[47]): ∀ (a a_1 a_2 : Iota), Eq (unorthogonal_lines (skS.0 0 a) (skS.0 2 a a_1 a_2)) False % 4.40/4.57 Clause #114 (by clausification #[48]): ∀ (a a_1 : Iota), Eq (unorthogonal_lines (skS.0 0 a) (skS.0 1 a a_1)) False % 4.40/4.57 Clause #132 (by clausification #[46]): ∀ (a a_1 a_2 : Iota), Eq (convergent_lines (skS.0 1 a a_1) (skS.0 2 a a_1 a_2)) True % 4.40/4.57 Clause #134 (by superposition #[132, 32]): ∀ (a a_1 a_2 a_3 : Iota), % 4.40/4.57 Or (Eq True False) % 4.40/4.57 (Or (Eq (unorthogonal_lines a (skS.0 1 a_1 a_2)) True) (Eq (unorthogonal_lines a (skS.0 2 a_1 a_2 a_3)) True)) % 4.40/4.57 Clause #211 (by clausification #[134]): ∀ (a a_1 a_2 a_3 : Iota), % 4.40/4.57 Or (Eq (unorthogonal_lines a (skS.0 1 a_1 a_2)) True) (Eq (unorthogonal_lines a (skS.0 2 a_1 a_2 a_3)) True) % 4.40/4.57 Clause #212 (by superposition #[211, 49]): ∀ (a a_1 : Iota), Or (Eq (unorthogonal_lines (skS.0 0 a) (skS.0 1 a a_1)) True) (Eq True False) % 4.40/4.57 Clause #213 (by clausification #[212]): ∀ (a a_1 : Iota), Eq (unorthogonal_lines (skS.0 0 a) (skS.0 1 a a_1)) True % 4.40/4.57 Clause #214 (by superposition #[213, 114]): Eq True False % 4.40/4.57 Clause #215 (by clausification #[214]): False % 4.40/4.57 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------