%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : GEO200+1 : TPTP v9.2.0. Released v3.3.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n027.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:12 PM UTC 2025 % Result : Theorem 74.15s 74.46s % Output : Proof 74.37s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.12/0.13 % Problem : GEO200+1 : TPTP v9.2.0. Released v3.3.0. % 0.12/0.14 % Command : duper %s % 0.14/0.35 % Computer : n027.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 : Fri Oct 3 12:07:38 EDT 2025 % 0.14/0.35 % CPUTime : % 74.15/74.46 SZS status Theorem for theBenchmark.p % 74.15/74.46 SZS output start Proof for theBenchmark.p % 74.15/74.46 Clause #0 (by assumption #[]): Eq (∀ (X : Iota), Not (distinct_points X X)) True % 74.15/74.46 Clause #3 (by assumption #[]): Eq (∀ (X Y Z : Iota), distinct_points X Y → Or (distinct_points X Z) (distinct_points Y Z)) True % 74.15/74.46 Clause #6 (by assumption #[]): Eq (∀ (X Y : Iota), distinct_points X Y → Not (apart_point_and_line X (line_connecting X Y))) True % 74.15/74.46 Clause #7 (by assumption #[]): Eq (∀ (X Y : Iota), distinct_points X Y → Not (apart_point_and_line Y (line_connecting X Y))) True % 74.15/74.46 Clause #10 (by assumption #[]): Eq % 74.15/74.46 (∀ (X Y U V : Iota), % 74.15/74.46 And (distinct_points X Y) (distinct_lines U V) → % 74.15/74.46 Or (Or (Or (apart_point_and_line X U) (apart_point_and_line X V)) (apart_point_and_line Y U)) % 74.15/74.46 (apart_point_and_line Y V)) % 74.15/74.46 True % 74.15/74.46 Clause #14 (by assumption #[]): Eq (Not (∀ (X Y : Iota), distinct_points X Y → Not (distinct_lines (line_connecting X Y) (line_connecting Y X)))) True % 74.15/74.46 Clause #19 (by clausification #[0]): ∀ (a : Iota), Eq (Not (distinct_points a a)) True % 74.15/74.46 Clause #20 (by clausification #[19]): ∀ (a : Iota), Eq (distinct_points a a) False % 74.15/74.46 Clause #21 (by clausification #[7]): ∀ (a : Iota), Eq (∀ (Y : Iota), distinct_points a Y → Not (apart_point_and_line Y (line_connecting a Y))) True % 74.15/74.46 Clause #22 (by clausification #[21]): ∀ (a a_1 : Iota), Eq (distinct_points a a_1 → Not (apart_point_and_line a_1 (line_connecting a a_1))) True % 74.15/74.46 Clause #23 (by clausification #[22]): ∀ (a a_1 : Iota), % 74.15/74.46 Or (Eq (distinct_points a a_1) False) (Eq (Not (apart_point_and_line a_1 (line_connecting a a_1))) True) % 74.15/74.46 Clause #24 (by clausification #[23]): ∀ (a a_1 : Iota), Or (Eq (distinct_points a a_1) False) (Eq (apart_point_and_line a_1 (line_connecting a a_1)) False) % 74.15/74.46 Clause #25 (by clausification #[6]): ∀ (a : Iota), Eq (∀ (Y : Iota), distinct_points a Y → Not (apart_point_and_line a (line_connecting a Y))) True % 74.15/74.46 Clause #26 (by clausification #[25]): ∀ (a a_1 : Iota), Eq (distinct_points a a_1 → Not (apart_point_and_line a (line_connecting a a_1))) True % 74.15/74.46 Clause #27 (by clausification #[26]): ∀ (a a_1 : Iota), Or (Eq (distinct_points a a_1) False) (Eq (Not (apart_point_and_line a (line_connecting a a_1))) True) % 74.15/74.46 Clause #28 (by clausification #[27]): ∀ (a a_1 : Iota), Or (Eq (distinct_points a a_1) False) (Eq (apart_point_and_line a (line_connecting a a_1)) False) % 74.15/74.46 Clause #29 (by clausification #[3]): ∀ (a : Iota), Eq (∀ (Y Z : Iota), distinct_points a Y → Or (distinct_points a Z) (distinct_points Y Z)) True % 74.15/74.46 Clause #30 (by clausification #[29]): ∀ (a a_1 : Iota), Eq (∀ (Z : Iota), distinct_points a a_1 → Or (distinct_points a Z) (distinct_points a_1 Z)) True % 74.15/74.46 Clause #31 (by clausification #[30]): ∀ (a a_1 a_2 : Iota), Eq (distinct_points a a_1 → Or (distinct_points a a_2) (distinct_points a_1 a_2)) True % 74.15/74.46 Clause #32 (by clausification #[31]): ∀ (a a_1 a_2 : Iota), % 74.15/74.46 Or (Eq (distinct_points a a_1) False) (Eq (Or (distinct_points a a_2) (distinct_points a_1 a_2)) True) % 74.15/74.46 Clause #33 (by clausification #[32]): ∀ (a a_1 a_2 : Iota), % 74.15/74.46 Or (Eq (distinct_points a a_1) False) (Or (Eq (distinct_points a a_2) True) (Eq (distinct_points a_1 a_2) True)) % 74.15/74.46 Clause #67 (by clausification #[14]): Eq (∀ (X Y : Iota), distinct_points X Y → Not (distinct_lines (line_connecting X Y) (line_connecting Y X))) False % 74.15/74.46 Clause #68 (by clausification #[67]): ∀ (a : Iota), % 74.15/74.46 Eq % 74.15/74.46 (Not % 74.15/74.46 (∀ (Y : Iota), % 74.15/74.46 distinct_points (skS.0 0 a) Y → % 74.15/74.46 Not (distinct_lines (line_connecting (skS.0 0 a) Y) (line_connecting Y (skS.0 0 a))))) % 74.15/74.46 True % 74.15/74.46 Clause #69 (by clausification #[68]): ∀ (a : Iota), % 74.15/74.46 Eq % 74.15/74.46 (∀ (Y : Iota), % 74.15/74.46 distinct_points (skS.0 0 a) Y → % 74.15/74.46 Not (distinct_lines (line_connecting (skS.0 0 a) Y) (line_connecting Y (skS.0 0 a)))) % 74.15/74.46 False % 74.15/74.46 Clause #70 (by clausification #[69]): ∀ (a a_1 : Iota), % 74.15/74.46 Eq % 74.15/74.46 (Not % 74.15/74.46 (distinct_points (skS.0 0 a) (skS.0 1 a a_1) → % 74.15/74.46 Not % 74.15/74.46 (distinct_lines (line_connecting (skS.0 0 a) (skS.0 1 a a_1)) (line_connecting (skS.0 1 a a_1) (skS.0 0 a))))) % 74.15/74.46 True % 74.15/74.46 Clause #71 (by clausification #[70]): ∀ (a a_1 : Iota), % 74.15/74.48 Eq % 74.15/74.48 (distinct_points (skS.0 0 a) (skS.0 1 a a_1) → % 74.15/74.48 Not (distinct_lines (line_connecting (skS.0 0 a) (skS.0 1 a a_1)) (line_connecting (skS.0 1 a a_1) (skS.0 0 a)))) % 74.15/74.48 False % 74.15/74.48 Clause #72 (by clausification #[71]): ∀ (a a_1 : Iota), Eq (distinct_points (skS.0 0 a) (skS.0 1 a a_1)) True % 74.15/74.48 Clause #73 (by clausification #[71]): ∀ (a a_1 : Iota), % 74.15/74.48 Eq (Not (distinct_lines (line_connecting (skS.0 0 a) (skS.0 1 a a_1)) (line_connecting (skS.0 1 a a_1) (skS.0 0 a)))) % 74.15/74.48 False % 74.15/74.48 Clause #74 (by superposition #[72, 24]): ∀ (a a_1 : Iota), % 74.15/74.48 Or (Eq True False) (Eq (apart_point_and_line (skS.0 1 a a_1) (line_connecting (skS.0 0 a) (skS.0 1 a a_1))) False) % 74.15/74.48 Clause #75 (by superposition #[72, 28]): ∀ (a a_1 : Iota), % 74.15/74.48 Or (Eq True False) (Eq (apart_point_and_line (skS.0 0 a) (line_connecting (skS.0 0 a) (skS.0 1 a a_1))) False) % 74.15/74.48 Clause #76 (by superposition #[72, 33]): ∀ (a a_1 a_2 : Iota), % 74.15/74.48 Or (Eq True False) (Or (Eq (distinct_points (skS.0 0 a) a_1) True) (Eq (distinct_points (skS.0 1 a a_2) a_1) True)) % 74.15/74.48 Clause #77 (by clausification #[10]): ∀ (a : Iota), % 74.15/74.48 Eq % 74.15/74.48 (∀ (Y U V : Iota), % 74.15/74.48 And (distinct_points a Y) (distinct_lines U V) → % 74.15/74.48 Or (Or (Or (apart_point_and_line a U) (apart_point_and_line a V)) (apart_point_and_line Y U)) % 74.15/74.48 (apart_point_and_line Y V)) % 74.15/74.48 True % 74.15/74.48 Clause #78 (by clausification #[77]): ∀ (a a_1 : Iota), % 74.15/74.48 Eq % 74.15/74.48 (∀ (U V : Iota), % 74.15/74.48 And (distinct_points a a_1) (distinct_lines U V) → % 74.15/74.48 Or (Or (Or (apart_point_and_line a U) (apart_point_and_line a V)) (apart_point_and_line a_1 U)) % 74.15/74.48 (apart_point_and_line a_1 V)) % 74.15/74.48 True % 74.15/74.48 Clause #79 (by clausification #[78]): ∀ (a a_1 a_2 : Iota), % 74.15/74.48 Eq % 74.15/74.48 (∀ (V : Iota), % 74.15/74.48 And (distinct_points a a_1) (distinct_lines a_2 V) → % 74.15/74.48 Or (Or (Or (apart_point_and_line a a_2) (apart_point_and_line a V)) (apart_point_and_line a_1 a_2)) % 74.15/74.48 (apart_point_and_line a_1 V)) % 74.15/74.48 True % 74.15/74.48 Clause #80 (by clausification #[79]): ∀ (a a_1 a_2 a_3 : Iota), % 74.15/74.48 Eq % 74.15/74.48 (And (distinct_points a a_1) (distinct_lines a_2 a_3) → % 74.15/74.48 Or (Or (Or (apart_point_and_line a a_2) (apart_point_and_line a a_3)) (apart_point_and_line a_1 a_2)) % 74.15/74.48 (apart_point_and_line a_1 a_3)) % 74.15/74.48 True % 74.15/74.48 Clause #81 (by clausification #[80]): ∀ (a a_1 a_2 a_3 : Iota), % 74.15/74.48 Or (Eq (And (distinct_points a a_1) (distinct_lines a_2 a_3)) False) % 74.15/74.48 (Eq % 74.15/74.48 (Or (Or (Or (apart_point_and_line a a_2) (apart_point_and_line a a_3)) (apart_point_and_line a_1 a_2)) % 74.15/74.48 (apart_point_and_line a_1 a_3)) % 74.15/74.48 True) % 74.15/74.48 Clause #82 (by clausification #[81]): ∀ (a a_1 a_2 a_3 : Iota), % 74.15/74.48 Or % 74.15/74.48 (Eq % 74.15/74.48 (Or (Or (Or (apart_point_and_line a a_1) (apart_point_and_line a a_2)) (apart_point_and_line a_3 a_1)) % 74.15/74.48 (apart_point_and_line a_3 a_2)) % 74.15/74.48 True) % 74.15/74.48 (Or (Eq (distinct_points a a_3) False) (Eq (distinct_lines a_1 a_2) False)) % 74.15/74.48 Clause #83 (by clausification #[82]): ∀ (a a_1 a_2 a_3 : Iota), % 74.15/74.48 Or (Eq (distinct_points a a_1) False) % 74.15/74.48 (Or (Eq (distinct_lines a_2 a_3) False) % 74.15/74.48 (Or (Eq (Or (Or (apart_point_and_line a a_2) (apart_point_and_line a a_3)) (apart_point_and_line a_1 a_2)) True) % 74.24/74.48 (Eq (apart_point_and_line a_1 a_3) True))) % 74.24/74.48 Clause #84 (by clausification #[83]): ∀ (a a_1 a_2 a_3 : Iota), % 74.24/74.48 Or (Eq (distinct_points a a_1) False) % 74.24/74.48 (Or (Eq (distinct_lines a_2 a_3) False) % 74.24/74.48 (Or (Eq (apart_point_and_line a_1 a_3) True) % 74.24/74.48 (Or (Eq (Or (apart_point_and_line a a_2) (apart_point_and_line a a_3)) True) % 74.24/74.48 (Eq (apart_point_and_line a_1 a_2) True)))) % 74.24/74.48 Clause #85 (by clausification #[84]): ∀ (a a_1 a_2 a_3 : Iota), % 74.24/74.48 Or (Eq (distinct_points a a_1) False) % 74.24/74.48 (Or (Eq (distinct_lines a_2 a_3) False) % 74.24/74.48 (Or (Eq (apart_point_and_line a_1 a_3) True) % 74.24/74.48 (Or (Eq (apart_point_and_line a_1 a_2) True) % 74.24/74.48 (Or (Eq (apart_point_and_line a a_2) True) (Eq (apart_point_and_line a a_3) True))))) % 74.24/74.48 Clause #86 (by superposition #[85, 72]): ∀ (a a_1 a_2 a_3 : Iota), % 74.24/74.48 Or (Eq (distinct_lines a a_1) False) % 74.24/74.48 (Or (Eq (apart_point_and_line (skS.0 1 a_2 a_3) a_1) True) % 74.24/74.48 (Or (Eq (apart_point_and_line (skS.0 1 a_2 a_3) a) True) % 74.25/74.50 (Or (Eq (apart_point_and_line (skS.0 0 a_2) a) True) % 74.25/74.50 (Or (Eq (apart_point_and_line (skS.0 0 a_2) a_1) True) (Eq False True))))) % 74.25/74.50 Clause #87 (by clausification #[76]): ∀ (a a_1 a_2 : Iota), Or (Eq (distinct_points (skS.0 0 a) a_1) True) (Eq (distinct_points (skS.0 1 a a_2) a_1) True) % 74.25/74.50 Clause #90 (by superposition #[87, 28]): ∀ (a a_1 a_2 : Iota), % 74.25/74.50 Or (Eq (distinct_points (skS.0 0 a) a_1) True) % 74.25/74.50 (Or (Eq True False) (Eq (apart_point_and_line (skS.0 1 a a_2) (line_connecting (skS.0 1 a a_2) a_1)) False)) % 74.25/74.50 Clause #91 (by superposition #[87, 33]): ∀ (a a_1 a_2 a_3 : Iota), % 74.25/74.50 Or (Eq (distinct_points (skS.0 0 a) a_1) True) % 74.25/74.50 (Or (Eq True False) (Or (Eq (distinct_points (skS.0 1 a a_2) a_3) True) (Eq (distinct_points a_1 a_3) True))) % 74.25/74.50 Clause #93 (by clausification #[73]): ∀ (a a_1 : Iota), % 74.25/74.50 Eq (distinct_lines (line_connecting (skS.0 0 a) (skS.0 1 a a_1)) (line_connecting (skS.0 1 a a_1) (skS.0 0 a))) True % 74.25/74.50 Clause #96 (by clausification #[75]): ∀ (a a_1 : Iota), Eq (apart_point_and_line (skS.0 0 a) (line_connecting (skS.0 0 a) (skS.0 1 a a_1))) False % 74.25/74.50 Clause #97 (by clausification #[91]): ∀ (a a_1 a_2 a_3 : Iota), % 74.25/74.50 Or (Eq (distinct_points (skS.0 0 a) a_1) True) % 74.25/74.50 (Or (Eq (distinct_points (skS.0 1 a a_2) a_3) True) (Eq (distinct_points a_1 a_3) True)) % 74.25/74.50 Clause #111 (by superposition #[97, 33]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 74.25/74.50 Or (Eq (distinct_points (skS.0 0 a) a_1) True) % 74.25/74.50 (Or (Eq (distinct_points (skS.0 1 a a_2) a_3) True) % 74.25/74.50 (Or (Eq True False) (Or (Eq (distinct_points a_1 a_4) True) (Eq (distinct_points a_3 a_4) True)))) % 74.25/74.50 Clause #119 (by clausification #[74]): ∀ (a a_1 : Iota), Eq (apart_point_and_line (skS.0 1 a a_1) (line_connecting (skS.0 0 a) (skS.0 1 a a_1))) False % 74.25/74.50 Clause #125 (by clausification #[86]): ∀ (a a_1 a_2 a_3 : Iota), % 74.25/74.50 Or (Eq (distinct_lines a a_1) False) % 74.25/74.50 (Or (Eq (apart_point_and_line (skS.0 1 a_2 a_3) a_1) True) % 74.25/74.50 (Or (Eq (apart_point_and_line (skS.0 1 a_2 a_3) a) True) % 74.25/74.50 (Or (Eq (apart_point_and_line (skS.0 0 a_2) a) True) (Eq (apart_point_and_line (skS.0 0 a_2) a_1) True)))) % 74.25/74.50 Clause #126 (by superposition #[125, 93]): ∀ (a a_1 a_2 a_3 : Iota), % 74.25/74.50 Or (Eq (apart_point_and_line (skS.0 1 a a_1) (line_connecting (skS.0 1 a_2 a_3) (skS.0 0 a_2))) True) % 74.25/74.50 (Or (Eq (apart_point_and_line (skS.0 1 a a_1) (line_connecting (skS.0 0 a_2) (skS.0 1 a_2 a_3))) True) % 74.25/74.50 (Or (Eq (apart_point_and_line (skS.0 0 a) (line_connecting (skS.0 0 a_2) (skS.0 1 a_2 a_3))) True) % 74.25/74.50 (Or (Eq (apart_point_and_line (skS.0 0 a) (line_connecting (skS.0 1 a_2 a_3) (skS.0 0 a_2))) True) % 74.25/74.50 (Eq False True)))) % 74.25/74.50 Clause #133 (by clausification #[111]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 74.25/74.50 Or (Eq (distinct_points (skS.0 0 a) a_1) True) % 74.25/74.50 (Or (Eq (distinct_points (skS.0 1 a a_2) a_3) True) % 74.25/74.50 (Or (Eq (distinct_points a_1 a_4) True) (Eq (distinct_points a_3 a_4) True))) % 74.25/74.50 Clause #144 (by superposition #[133, 20]): ∀ (a a_1 a_2 a_3 : Iota), % 74.25/74.50 Or (Eq (distinct_points (skS.0 0 a) a_1) True) % 74.25/74.50 (Or (Eq (distinct_points (skS.0 1 a a_2) a_3) True) (Or (Eq (distinct_points a_3 a_1) True) (Eq True False))) % 74.25/74.50 Clause #163 (by clausification #[90]): ∀ (a a_1 a_2 : Iota), % 74.25/74.50 Or (Eq (distinct_points (skS.0 0 a) a_1) True) % 74.25/74.50 (Eq (apart_point_and_line (skS.0 1 a a_2) (line_connecting (skS.0 1 a a_2) a_1)) False) % 74.25/74.50 Clause #164 (by clausification #[144]): ∀ (a a_1 a_2 a_3 : Iota), % 74.25/74.50 Or (Eq (distinct_points (skS.0 0 a) a_1) True) % 74.25/74.50 (Or (Eq (distinct_points (skS.0 1 a a_2) a_3) True) (Eq (distinct_points a_3 a_1) True)) % 74.25/74.50 Clause #165 (by superposition #[164, 20]): ∀ (a a_1 a_2 : Iota), % 74.25/74.50 Or (Eq (distinct_points (skS.0 1 a a_1) a_2) True) (Or (Eq (distinct_points a_2 (skS.0 0 a)) True) (Eq True False)) % 74.25/74.50 Clause #180 (by clausification #[165]): ∀ (a a_1 a_2 : Iota), Or (Eq (distinct_points (skS.0 1 a a_1) a_2) True) (Eq (distinct_points a_2 (skS.0 0 a)) True) % 74.25/74.50 Clause #181 (by superposition #[180, 20]): ∀ (a a_1 : Iota), Or (Eq (distinct_points (skS.0 1 a a_1) (skS.0 0 a)) True) (Eq True False) % 74.25/74.50 Clause #186 (by clausification #[181]): ∀ (a a_1 : Iota), Eq (distinct_points (skS.0 1 a a_1) (skS.0 0 a)) True % 74.37/74.61 Clause #187 (by superposition #[186, 24]): ∀ (a a_1 : Iota), % 74.37/74.61 Or (Eq True False) (Eq (apart_point_and_line (skS.0 0 a) (line_connecting (skS.0 1 a a_1) (skS.0 0 a))) False) % 74.37/74.61 Clause #194 (by clausification #[187]): ∀ (a a_1 : Iota), Eq (apart_point_and_line (skS.0 0 a) (line_connecting (skS.0 1 a a_1) (skS.0 0 a))) False % 74.37/74.61 Clause #414 (by clausification #[126]): ∀ (a a_1 a_2 a_3 : Iota), % 74.37/74.61 Or (Eq (apart_point_and_line (skS.0 1 a a_1) (line_connecting (skS.0 1 a_2 a_3) (skS.0 0 a_2))) True) % 74.37/74.61 (Or (Eq (apart_point_and_line (skS.0 1 a a_1) (line_connecting (skS.0 0 a_2) (skS.0 1 a_2 a_3))) True) % 74.37/74.61 (Or (Eq (apart_point_and_line (skS.0 0 a) (line_connecting (skS.0 0 a_2) (skS.0 1 a_2 a_3))) True) % 74.37/74.61 (Eq (apart_point_and_line (skS.0 0 a) (line_connecting (skS.0 1 a_2 a_3) (skS.0 0 a_2))) True))) % 74.37/74.61 Clause #415 (by superposition #[414, 163]): ∀ (a a_1 : Iota), % 74.37/74.61 Or (Eq (apart_point_and_line (skS.0 1 a a_1) (line_connecting (skS.0 0 a) (skS.0 1 a a_1))) True) % 74.37/74.61 (Or (Eq (apart_point_and_line (skS.0 0 a) (line_connecting (skS.0 0 a) (skS.0 1 a a_1))) True) % 74.37/74.61 (Or (Eq (apart_point_and_line (skS.0 0 a) (line_connecting (skS.0 1 a a_1) (skS.0 0 a))) True) % 74.37/74.61 (Or (Eq (distinct_points (skS.0 0 a) (skS.0 0 a)) True) (Eq True False)))) % 74.37/74.61 Clause #5968 (by clausification #[415]): ∀ (a a_1 : Iota), % 74.37/74.61 Or (Eq (apart_point_and_line (skS.0 1 a a_1) (line_connecting (skS.0 0 a) (skS.0 1 a a_1))) True) % 74.37/74.61 (Or (Eq (apart_point_and_line (skS.0 0 a) (line_connecting (skS.0 0 a) (skS.0 1 a a_1))) True) % 74.37/74.61 (Or (Eq (apart_point_and_line (skS.0 0 a) (line_connecting (skS.0 1 a a_1) (skS.0 0 a))) True) % 74.37/74.61 (Eq (distinct_points (skS.0 0 a) (skS.0 0 a)) True))) % 74.37/74.61 Clause #5969 (by forward demodulation #[5968, 96]): ∀ (a a_1 : Iota), % 74.37/74.61 Or (Eq (apart_point_and_line (skS.0 1 a a_1) (line_connecting (skS.0 0 a) (skS.0 1 a a_1))) True) % 74.37/74.61 (Or (Eq False True) % 74.37/74.61 (Or (Eq (apart_point_and_line (skS.0 0 a) (line_connecting (skS.0 1 a a_1) (skS.0 0 a))) True) % 74.37/74.61 (Eq (distinct_points (skS.0 0 a) (skS.0 0 a)) True))) % 74.37/74.61 Clause #5970 (by clausification #[5969]): ∀ (a a_1 : Iota), % 74.37/74.61 Or (Eq (apart_point_and_line (skS.0 1 a a_1) (line_connecting (skS.0 0 a) (skS.0 1 a a_1))) True) % 74.37/74.61 (Or (Eq (apart_point_and_line (skS.0 0 a) (line_connecting (skS.0 1 a a_1) (skS.0 0 a))) True) % 74.37/74.61 (Eq (distinct_points (skS.0 0 a) (skS.0 0 a)) True)) % 74.37/74.61 Clause #5971 (by forward demodulation #[5970, 194]): ∀ (a a_1 : Iota), % 74.37/74.61 Or (Eq (apart_point_and_line (skS.0 1 a a_1) (line_connecting (skS.0 0 a) (skS.0 1 a a_1))) True) % 74.37/74.61 (Or (Eq False True) (Eq (distinct_points (skS.0 0 a) (skS.0 0 a)) True)) % 74.37/74.61 Clause #5972 (by clausification #[5971]): ∀ (a a_1 : Iota), % 74.37/74.61 Or (Eq (apart_point_and_line (skS.0 1 a a_1) (line_connecting (skS.0 0 a) (skS.0 1 a a_1))) True) % 74.37/74.61 (Eq (distinct_points (skS.0 0 a) (skS.0 0 a)) True) % 74.37/74.61 Clause #5973 (by forward demodulation #[5972, 20]): ∀ (a a_1 : Iota), % 74.37/74.61 Or (Eq (apart_point_and_line (skS.0 1 a a_1) (line_connecting (skS.0 0 a) (skS.0 1 a a_1))) True) (Eq False True) % 74.37/74.61 Clause #5974 (by clausification #[5973]): ∀ (a a_1 : Iota), Eq (apart_point_and_line (skS.0 1 a a_1) (line_connecting (skS.0 0 a) (skS.0 1 a a_1))) True % 74.37/74.61 Clause #5975 (by superposition #[5974, 119]): Eq True False % 74.37/74.61 Clause #6027 (by clausification #[5975]): False % 74.37/74.61 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------