↑ Up

Duper---1.0.THM-Prf.s

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

% Computer : n029.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:13 PM UTC 2025

% Result   : Theorem 4.13s 4.27s
% Output   : Proof 4.13s
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.04/0.13  % Problem    : GEO208+1 : TPTP v9.2.0. Released v3.3.0.
% 0.04/0.15  % Command    : duper %s
% 0.15/0.36  % Computer : n029.cluster.edu
% 0.15/0.36  % Model    : x86_64 x86_64
% 0.15/0.36  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.36  % Memory   : 8042.1875MB
% 0.15/0.36  % OS       : Linux 3.10.0-693.el7.x86_64
% 0.15/0.36  % CPULimit   : 300
% 0.15/0.36  % WCLimit    : 300
% 0.15/0.36  % DateTime   : Fri Oct  3 11:51:38 EDT 2025
% 0.15/0.36  % CPUTime    : 
% 4.13/4.27  SZS status Theorem for theBenchmark.p
% 4.13/4.27  SZS output start Proof for theBenchmark.p
% 4.13/4.27  Clause #16 (by assumption #[]): Eq
% 4.13/4.27    (∀ (X Y Z : Iota),
% 4.13/4.27      distinct_lines Y Z → Or (Or (apart_point_and_line X Y) (apart_point_and_line X Z)) (convergent_lines Y Z))
% 4.13/4.27    True
% 4.13/4.27  Clause #17 (by assumption #[]): Eq
% 4.13/4.27    (Not
% 4.13/4.27      (∀ (X Y Z : Iota),
% 4.13/4.27        And (And (Not (apart_point_and_line X Y)) (Not (apart_point_and_line X Z))) (Not (convergent_lines Y Z)) →
% 4.13/4.27          Not (distinct_lines Y Z)))
% 4.13/4.27    True
% 4.13/4.27  Clause #35 (by clausification #[17]): Eq
% 4.13/4.27    (∀ (X Y Z : Iota),
% 4.13/4.27      And (And (Not (apart_point_and_line X Y)) (Not (apart_point_and_line X Z))) (Not (convergent_lines Y Z)) →
% 4.13/4.27        Not (distinct_lines Y Z))
% 4.13/4.27    False
% 4.13/4.27  Clause #36 (by clausification #[35]): ∀ (a : Iota),
% 4.13/4.27    Eq
% 4.13/4.27      (Not
% 4.13/4.27        (∀ (Y Z : Iota),
% 4.13/4.27          And (And (Not (apart_point_and_line (skS.0 0 a) Y)) (Not (apart_point_and_line (skS.0 0 a) Z)))
% 4.13/4.27              (Not (convergent_lines Y Z)) →
% 4.13/4.27            Not (distinct_lines Y Z)))
% 4.13/4.27      True
% 4.13/4.27  Clause #37 (by clausification #[36]): ∀ (a : Iota),
% 4.13/4.27    Eq
% 4.13/4.27      (∀ (Y Z : Iota),
% 4.13/4.27        And (And (Not (apart_point_and_line (skS.0 0 a) Y)) (Not (apart_point_and_line (skS.0 0 a) Z)))
% 4.13/4.27            (Not (convergent_lines Y Z)) →
% 4.13/4.27          Not (distinct_lines Y Z))
% 4.13/4.27      False
% 4.13/4.27  Clause #38 (by clausification #[37]): ∀ (a a_1 : Iota),
% 4.13/4.27    Eq
% 4.13/4.27      (Not
% 4.13/4.27        (∀ (Z : Iota),
% 4.13/4.27          And (And (Not (apart_point_and_line (skS.0 0 a) (skS.0 1 a a_1))) (Not (apart_point_and_line (skS.0 0 a) Z)))
% 4.13/4.27              (Not (convergent_lines (skS.0 1 a a_1) Z)) →
% 4.13/4.27            Not (distinct_lines (skS.0 1 a a_1) Z)))
% 4.13/4.27      True
% 4.13/4.27  Clause #39 (by clausification #[38]): ∀ (a a_1 : Iota),
% 4.13/4.27    Eq
% 4.13/4.27      (∀ (Z : Iota),
% 4.13/4.27        And (And (Not (apart_point_and_line (skS.0 0 a) (skS.0 1 a a_1))) (Not (apart_point_and_line (skS.0 0 a) Z)))
% 4.13/4.27            (Not (convergent_lines (skS.0 1 a a_1) Z)) →
% 4.13/4.27          Not (distinct_lines (skS.0 1 a a_1) Z))
% 4.13/4.27      False
% 4.13/4.27  Clause #40 (by clausification #[39]): ∀ (a a_1 a_2 : Iota),
% 4.13/4.27    Eq
% 4.13/4.27      (Not
% 4.13/4.27        (And
% 4.13/4.27            (And (Not (apart_point_and_line (skS.0 0 a) (skS.0 1 a a_1)))
% 4.13/4.27              (Not (apart_point_and_line (skS.0 0 a) (skS.0 2 a a_1 a_2))))
% 4.13/4.27            (Not (convergent_lines (skS.0 1 a a_1) (skS.0 2 a a_1 a_2))) →
% 4.13/4.27          Not (distinct_lines (skS.0 1 a a_1) (skS.0 2 a a_1 a_2))))
% 4.13/4.27      True
% 4.13/4.27  Clause #41 (by clausification #[40]): ∀ (a a_1 a_2 : Iota),
% 4.13/4.27    Eq
% 4.13/4.27      (And
% 4.13/4.27          (And (Not (apart_point_and_line (skS.0 0 a) (skS.0 1 a a_1)))
% 4.13/4.27            (Not (apart_point_and_line (skS.0 0 a) (skS.0 2 a a_1 a_2))))
% 4.13/4.27          (Not (convergent_lines (skS.0 1 a a_1) (skS.0 2 a a_1 a_2))) →
% 4.13/4.27        Not (distinct_lines (skS.0 1 a a_1) (skS.0 2 a a_1 a_2)))
% 4.13/4.27      False
% 4.13/4.27  Clause #42 (by clausification #[41]): ∀ (a a_1 a_2 : Iota),
% 4.13/4.27    Eq
% 4.13/4.27      (And
% 4.13/4.27        (And (Not (apart_point_and_line (skS.0 0 a) (skS.0 1 a a_1)))
% 4.13/4.27          (Not (apart_point_and_line (skS.0 0 a) (skS.0 2 a a_1 a_2))))
% 4.13/4.27        (Not (convergent_lines (skS.0 1 a a_1) (skS.0 2 a a_1 a_2))))
% 4.13/4.27      True
% 4.13/4.27  Clause #43 (by clausification #[41]): ∀ (a a_1 a_2 : Iota), Eq (Not (distinct_lines (skS.0 1 a a_1) (skS.0 2 a a_1 a_2))) False
% 4.13/4.27  Clause #44 (by clausification #[42]): ∀ (a a_1 a_2 : Iota), Eq (Not (convergent_lines (skS.0 1 a a_1) (skS.0 2 a a_1 a_2))) True
% 4.13/4.27  Clause #45 (by clausification #[42]): ∀ (a a_1 a_2 : Iota),
% 4.13/4.27    Eq
% 4.13/4.27      (And (Not (apart_point_and_line (skS.0 0 a) (skS.0 1 a a_1)))
% 4.13/4.27        (Not (apart_point_and_line (skS.0 0 a) (skS.0 2 a a_1 a_2))))
% 4.13/4.27      True
% 4.13/4.27  Clause #46 (by clausification #[44]): ∀ (a a_1 a_2 : Iota), Eq (convergent_lines (skS.0 1 a a_1) (skS.0 2 a a_1 a_2)) False
% 4.13/4.27  Clause #88 (by clausification #[16]): ∀ (a : Iota),
% 4.13/4.27    Eq
% 4.13/4.27      (∀ (Y Z : Iota),
% 4.13/4.27        distinct_lines Y Z → Or (Or (apart_point_and_line a Y) (apart_point_and_line a Z)) (convergent_lines Y Z))
% 4.13/4.27      True
% 4.13/4.27  Clause #89 (by clausification #[88]): ∀ (a a_1 : Iota),
% 4.13/4.27    Eq
% 4.13/4.27      (∀ (Z : Iota),
% 4.13/4.27        distinct_lines a Z → Or (Or (apart_point_and_line a_1 a) (apart_point_and_line a_1 Z)) (convergent_lines a Z))
% 4.13/4.27      True
% 4.13/4.27  Clause #90 (by clausification #[89]): ∀ (a a_1 a_2 : Iota),
% 4.13/4.27    Eq
% 4.13/4.27      (distinct_lines a a_1 →
% 4.13/4.27        Or (Or (apart_point_and_line a_2 a) (apart_point_and_line a_2 a_1)) (convergent_lines a a_1))
% 4.13/4.29      True
% 4.13/4.29  Clause #91 (by clausification #[90]): ∀ (a a_1 a_2 : Iota),
% 4.13/4.29    Or (Eq (distinct_lines a a_1) False)
% 4.13/4.29      (Eq (Or (Or (apart_point_and_line a_2 a) (apart_point_and_line a_2 a_1)) (convergent_lines a a_1)) True)
% 4.13/4.29  Clause #92 (by clausification #[91]): ∀ (a a_1 a_2 : Iota),
% 4.13/4.29    Or (Eq (distinct_lines a a_1) False)
% 4.13/4.29      (Or (Eq (Or (apart_point_and_line a_2 a) (apart_point_and_line a_2 a_1)) True) (Eq (convergent_lines a a_1) True))
% 4.13/4.29  Clause #93 (by clausification #[92]): ∀ (a a_1 a_2 : Iota),
% 4.13/4.29    Or (Eq (distinct_lines a a_1) False)
% 4.13/4.29      (Or (Eq (convergent_lines a a_1) True)
% 4.13/4.29        (Or (Eq (apart_point_and_line a_2 a) True) (Eq (apart_point_and_line a_2 a_1) True)))
% 4.13/4.29  Clause #103 (by clausification #[43]): ∀ (a a_1 a_2 : Iota), Eq (distinct_lines (skS.0 1 a a_1) (skS.0 2 a a_1 a_2)) True
% 4.13/4.29  Clause #105 (by superposition #[103, 93]): ∀ (a a_1 a_2 a_3 : Iota),
% 4.13/4.29    Or (Eq True False)
% 4.13/4.29      (Or (Eq (convergent_lines (skS.0 1 a a_1) (skS.0 2 a a_1 a_2)) True)
% 4.13/4.29        (Or (Eq (apart_point_and_line a_3 (skS.0 1 a a_1)) True)
% 4.13/4.29          (Eq (apart_point_and_line a_3 (skS.0 2 a a_1 a_2)) True)))
% 4.13/4.29  Clause #121 (by clausification #[45]): ∀ (a a_1 a_2 : Iota), Eq (Not (apart_point_and_line (skS.0 0 a) (skS.0 2 a a_1 a_2))) True
% 4.13/4.29  Clause #122 (by clausification #[45]): ∀ (a a_1 : Iota), Eq (Not (apart_point_and_line (skS.0 0 a) (skS.0 1 a a_1))) True
% 4.13/4.29  Clause #123 (by clausification #[121]): ∀ (a a_1 a_2 : Iota), Eq (apart_point_and_line (skS.0 0 a) (skS.0 2 a a_1 a_2)) False
% 4.13/4.29  Clause #124 (by clausification #[122]): ∀ (a a_1 : Iota), Eq (apart_point_and_line (skS.0 0 a) (skS.0 1 a a_1)) False
% 4.13/4.29  Clause #146 (by clausification #[105]): ∀ (a a_1 a_2 a_3 : Iota),
% 4.13/4.29    Or (Eq (convergent_lines (skS.0 1 a a_1) (skS.0 2 a a_1 a_2)) True)
% 4.13/4.29      (Or (Eq (apart_point_and_line a_3 (skS.0 1 a a_1)) True) (Eq (apart_point_and_line a_3 (skS.0 2 a a_1 a_2)) True))
% 4.13/4.29  Clause #147 (by superposition #[146, 46]): ∀ (a a_1 a_2 a_3 : Iota),
% 4.13/4.29    Or (Eq (apart_point_and_line a (skS.0 1 a_1 a_2)) True)
% 4.13/4.29      (Or (Eq (apart_point_and_line a (skS.0 2 a_1 a_2 a_3)) True) (Eq True False))
% 4.13/4.29  Clause #154 (by clausification #[147]): ∀ (a a_1 a_2 a_3 : Iota),
% 4.13/4.29    Or (Eq (apart_point_and_line a (skS.0 1 a_1 a_2)) True) (Eq (apart_point_and_line a (skS.0 2 a_1 a_2 a_3)) True)
% 4.13/4.29  Clause #155 (by superposition #[154, 123]): ∀ (a a_1 : Iota), Or (Eq (apart_point_and_line (skS.0 0 a) (skS.0 1 a a_1)) True) (Eq True False)
% 4.13/4.29  Clause #158 (by clausification #[155]): ∀ (a a_1 : Iota), Eq (apart_point_and_line (skS.0 0 a) (skS.0 1 a a_1)) True
% 4.13/4.29  Clause #159 (by superposition #[158, 124]): Eq True False
% 4.13/4.29  Clause #162 (by clausification #[159]): False
% 4.13/4.29  SZS output end Proof for theBenchmark.p
%------------------------------------------------------------------------------