↑ Up

Duper---1.0.THM-Prf.s

View TPTP
Problem Process solution in
SystemOnTSTP Download .tgz 
%------------------------------------------------------------------------------
% File     : Duper---1.0
% Problem  : GEO225+2 : TPTP v9.2.0. Released v3.3.0.
% Transfm  : none
% Format   : tptp:raw
% Command  : duper %s

% Computer : n018.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:17 PM UTC 2025

% Result   : Theorem 9.63s 9.82s
% Output   : Proof 9.63s
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.12/0.12  % Problem    : GEO225+2 : TPTP v9.2.0. Released v3.3.0.
% 0.12/0.14  % Command    : duper %s
% 0.14/0.35  % Computer : n018.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:47:53 EDT 2025
% 0.14/0.35  % CPUTime    : 
% 9.63/9.82  SZS status Theorem for theBenchmark.p
% 9.63/9.82  SZS output start Proof for theBenchmark.p
% 9.63/9.82  Clause #0 (by assumption #[]): Eq (∀ (X : Iota), Not (distinct_points X X)) True
% 9.63/9.82  Clause #6 (by assumption #[]): Eq
% 9.63/9.82    (∀ (X Y Z : Iota),
% 9.63/9.82      distinct_points X Y →
% 9.63/9.82        apart_point_and_line Z (line_connecting X Y) → And (distinct_points Z X) (distinct_points Z Y))
% 9.63/9.82    True
% 9.63/9.82  Clause #16 (by assumption #[]): Eq
% 9.63/9.82    (Not
% 9.63/9.82      (∀ (A B : Iota),
% 9.63/9.82        And (And (point A) (point B)) (distinct_points A B) →
% 9.63/9.82          Exists fun X => line X → And (Not (apart_point_and_line A X)) (Not (apart_point_and_line B X))))
% 9.63/9.82    True
% 9.63/9.82  Clause #21 (by clausification #[0]): ∀ (a : Iota), Eq (Not (distinct_points a a)) True
% 9.63/9.82  Clause #22 (by clausification #[21]): ∀ (a : Iota), Eq (distinct_points a a) False
% 9.63/9.82  Clause #76 (by clausification #[6]): ∀ (a : Iota),
% 9.63/9.82    Eq
% 9.63/9.82      (∀ (Y Z : Iota),
% 9.63/9.82        distinct_points a Y →
% 9.63/9.82          apart_point_and_line Z (line_connecting a Y) → And (distinct_points Z a) (distinct_points Z Y))
% 9.63/9.82      True
% 9.63/9.82  Clause #77 (by clausification #[76]): ∀ (a a_1 : Iota),
% 9.63/9.82    Eq
% 9.63/9.82      (∀ (Z : Iota),
% 9.63/9.82        distinct_points a a_1 →
% 9.63/9.82          apart_point_and_line Z (line_connecting a a_1) → And (distinct_points Z a) (distinct_points Z a_1))
% 9.63/9.82      True
% 9.63/9.82  Clause #78 (by clausification #[77]): ∀ (a a_1 a_2 : Iota),
% 9.63/9.82    Eq
% 9.63/9.82      (distinct_points a a_1 →
% 9.63/9.82        apart_point_and_line a_2 (line_connecting a a_1) → And (distinct_points a_2 a) (distinct_points a_2 a_1))
% 9.63/9.82      True
% 9.63/9.82  Clause #79 (by clausification #[78]): ∀ (a a_1 a_2 : Iota),
% 9.63/9.82    Or (Eq (distinct_points a a_1) False)
% 9.63/9.82      (Eq (apart_point_and_line a_2 (line_connecting a a_1) → And (distinct_points a_2 a) (distinct_points a_2 a_1)) True)
% 9.63/9.82  Clause #80 (by clausification #[79]): ∀ (a a_1 a_2 : Iota),
% 9.63/9.82    Or (Eq (distinct_points a a_1) False)
% 9.63/9.82      (Or (Eq (apart_point_and_line a_2 (line_connecting a a_1)) False)
% 9.63/9.82        (Eq (And (distinct_points a_2 a) (distinct_points a_2 a_1)) True))
% 9.63/9.82  Clause #81 (by clausification #[80]): ∀ (a a_1 a_2 : Iota),
% 9.63/9.82    Or (Eq (distinct_points a a_1) False)
% 9.63/9.82      (Or (Eq (apart_point_and_line a_2 (line_connecting a a_1)) False) (Eq (distinct_points a_2 a_1) True))
% 9.63/9.82  Clause #82 (by clausification #[80]): ∀ (a a_1 a_2 : Iota),
% 9.63/9.82    Or (Eq (distinct_points a a_1) False)
% 9.63/9.82      (Or (Eq (apart_point_and_line a_2 (line_connecting a a_1)) False) (Eq (distinct_points a_2 a) True))
% 9.63/9.82  Clause #92 (by clausification #[16]): Eq
% 9.63/9.82    (∀ (A B : Iota),
% 9.63/9.82      And (And (point A) (point B)) (distinct_points A B) →
% 9.63/9.82        Exists fun X => line X → And (Not (apart_point_and_line A X)) (Not (apart_point_and_line B X)))
% 9.63/9.82    False
% 9.63/9.82  Clause #93 (by clausification #[92]): ∀ (a : Iota),
% 9.63/9.82    Eq
% 9.63/9.82      (Not
% 9.63/9.82        (∀ (B : Iota),
% 9.63/9.82          And (And (point (skS.0 0 a)) (point B)) (distinct_points (skS.0 0 a) B) →
% 9.63/9.82            Exists fun X => line X → And (Not (apart_point_and_line (skS.0 0 a) X)) (Not (apart_point_and_line B X))))
% 9.63/9.82      True
% 9.63/9.82  Clause #94 (by clausification #[93]): ∀ (a : Iota),
% 9.63/9.82    Eq
% 9.63/9.82      (∀ (B : Iota),
% 9.63/9.82        And (And (point (skS.0 0 a)) (point B)) (distinct_points (skS.0 0 a) B) →
% 9.63/9.82          Exists fun X => line X → And (Not (apart_point_and_line (skS.0 0 a) X)) (Not (apart_point_and_line B X)))
% 9.63/9.82      False
% 9.63/9.82  Clause #95 (by clausification #[94]): ∀ (a a_1 : Iota),
% 9.63/9.82    Eq
% 9.63/9.82      (Not
% 9.63/9.82        (And (And (point (skS.0 0 a)) (point (skS.0 1 a a_1))) (distinct_points (skS.0 0 a) (skS.0 1 a a_1)) →
% 9.63/9.82          Exists fun X =>
% 9.63/9.82            line X → And (Not (apart_point_and_line (skS.0 0 a) X)) (Not (apart_point_and_line (skS.0 1 a a_1) X))))
% 9.63/9.82      True
% 9.63/9.82  Clause #96 (by clausification #[95]): ∀ (a a_1 : Iota),
% 9.63/9.82    Eq
% 9.63/9.82      (And (And (point (skS.0 0 a)) (point (skS.0 1 a a_1))) (distinct_points (skS.0 0 a) (skS.0 1 a a_1)) →
% 9.63/9.82        Exists fun X =>
% 9.63/9.82          line X → And (Not (apart_point_and_line (skS.0 0 a) X)) (Not (apart_point_and_line (skS.0 1 a a_1) X)))
% 9.63/9.82      False
% 9.63/9.82  Clause #97 (by clausification #[96]): ∀ (a a_1 : Iota),
% 9.63/9.82    Eq (And (And (point (skS.0 0 a)) (point (skS.0 1 a a_1))) (distinct_points (skS.0 0 a) (skS.0 1 a a_1))) True
% 9.63/9.82  Clause #98 (by clausification #[96]): ∀ (a a_1 : Iota),
% 9.63/9.82    Eq
% 9.63/9.82      (Exists fun X =>
% 9.63/9.82        line X → And (Not (apart_point_and_line (skS.0 0 a) X)) (Not (apart_point_and_line (skS.0 1 a a_1) X)))
% 9.63/9.84      False
% 9.63/9.84  Clause #99 (by clausification #[97]): ∀ (a a_1 : Iota), Eq (distinct_points (skS.0 0 a) (skS.0 1 a a_1)) True
% 9.63/9.84  Clause #103 (by superposition #[99, 81]): ∀ (a a_1 a_2 : Iota),
% 9.63/9.84    Or (Eq True False)
% 9.63/9.84      (Or (Eq (apart_point_and_line a (line_connecting (skS.0 0 a_1) (skS.0 1 a_1 a_2))) False)
% 9.63/9.84        (Eq (distinct_points a (skS.0 1 a_1 a_2)) True))
% 9.63/9.84  Clause #104 (by superposition #[99, 82]): ∀ (a a_1 a_2 : Iota),
% 9.63/9.84    Or (Eq True False)
% 9.63/9.84      (Or (Eq (apart_point_and_line a (line_connecting (skS.0 0 a_1) (skS.0 1 a_1 a_2))) False)
% 9.63/9.84        (Eq (distinct_points a (skS.0 0 a_1)) True))
% 9.63/9.84  Clause #115 (by clausification #[98]): ∀ (a a_1 a_2 : Iota),
% 9.63/9.84    Eq (line a → And (Not (apart_point_and_line (skS.0 0 a_1) a)) (Not (apart_point_and_line (skS.0 1 a_1 a_2) a))) False
% 9.63/9.84  Clause #117 (by clausification #[115]): ∀ (a a_1 a_2 : Iota),
% 9.63/9.84    Eq (And (Not (apart_point_and_line (skS.0 0 a) a_1)) (Not (apart_point_and_line (skS.0 1 a a_2) a_1))) False
% 9.63/9.84  Clause #126 (by clausification #[117]): ∀ (a a_1 a_2 : Iota),
% 9.63/9.84    Or (Eq (Not (apart_point_and_line (skS.0 0 a) a_1)) False) (Eq (Not (apart_point_and_line (skS.0 1 a a_2) a_1)) False)
% 9.63/9.84  Clause #127 (by clausification #[126]): ∀ (a a_1 a_2 : Iota),
% 9.63/9.84    Or (Eq (Not (apart_point_and_line (skS.0 1 a a_1) a_2)) False) (Eq (apart_point_and_line (skS.0 0 a) a_2) True)
% 9.63/9.84  Clause #128 (by clausification #[127]): ∀ (a a_1 a_2 : Iota),
% 9.63/9.84    Or (Eq (apart_point_and_line (skS.0 0 a) a_1) True) (Eq (apart_point_and_line (skS.0 1 a a_2) a_1) True)
% 9.63/9.84  Clause #166 (by clausification #[103]): ∀ (a a_1 a_2 : Iota),
% 9.63/9.84    Or (Eq (apart_point_and_line a (line_connecting (skS.0 0 a_1) (skS.0 1 a_1 a_2))) False)
% 9.63/9.84      (Eq (distinct_points a (skS.0 1 a_1 a_2)) True)
% 9.63/9.84  Clause #167 (by superposition #[166, 128]): ∀ (a a_1 a_2 a_3 : Iota),
% 9.63/9.84    Or (Eq (distinct_points (skS.0 1 a a_1) (skS.0 1 a_2 a_3)) True)
% 9.63/9.84      (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) (Eq False True))
% 9.63/9.84  Clause #207 (by clausification #[104]): ∀ (a a_1 a_2 : Iota),
% 9.63/9.84    Or (Eq (apart_point_and_line a (line_connecting (skS.0 0 a_1) (skS.0 1 a_1 a_2))) False)
% 9.63/9.84      (Eq (distinct_points a (skS.0 0 a_1)) True)
% 9.63/9.84  Clause #1176 (by clausification #[167]): ∀ (a a_1 a_2 a_3 : Iota),
% 9.63/9.84    Or (Eq (distinct_points (skS.0 1 a a_1) (skS.0 1 a_2 a_3)) True)
% 9.63/9.84      (Eq (apart_point_and_line (skS.0 0 a) (line_connecting (skS.0 0 a_2) (skS.0 1 a_2 a_3))) True)
% 9.63/9.84  Clause #1177 (by superposition #[1176, 22]): ∀ (a a_1 : Iota),
% 9.63/9.84    Or (Eq (apart_point_and_line (skS.0 0 a) (line_connecting (skS.0 0 a) (skS.0 1 a a_1))) True) (Eq True False)
% 9.63/9.84  Clause #1192 (by clausification #[1177]): ∀ (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))) True
% 9.63/9.84  Clause #1195 (by superposition #[1192, 207]): ∀ (a : Iota), Or (Eq True False) (Eq (distinct_points (skS.0 0 a) (skS.0 0 a)) True)
% 9.63/9.84  Clause #1203 (by clausification #[1195]): ∀ (a : Iota), Eq (distinct_points (skS.0 0 a) (skS.0 0 a)) True
% 9.63/9.84  Clause #1204 (by superposition #[1203, 22]): Eq True False
% 9.63/9.84  Clause #1208 (by clausification #[1204]): False
% 9.63/9.84  SZS output end Proof for theBenchmark.p
%------------------------------------------------------------------------------