%------------------------------------------------------------------------------
% File : ConnectPP---0.7.2
% Problem : GEO024-2 : TPTP v9.3.1. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox2/solver/bin/connect++ --verbosity 1 --no-colour --tptp-proof --schedule default --timeout 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n003.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Sep 24 08:39:16 AM UTC 2026
% Result : Unsatisfiable 2.36s 2.68s
% Output : Proof 2.46s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(reflexivity_for_equidistance,axiom,
equidistant(X,Y,Y,X),
file('GEO002-0.ax',reflexivity_for_equidistance) ).
cnf(transitivity_for_equidistance,axiom,
( equidistant(Z,V,V2,W)
| ~ equidistant(X,Y,V2,W)
| ~ equidistant(X,Y,Z,V) ),
file('GEO002-0.ax',transitivity_for_equidistance) ).
cnf(identity_for_equidistance,axiom,
( X = Y
| ~ equidistant(X,Y,Z,Z) ),
file('GEO002-0.ax',identity_for_equidistance) ).
cnf(segment_construction1,axiom,
between(X,Y,extension(X,Y,W,V)),
file('GEO002-0.ax',segment_construction1) ).
cnf(segment_construction2,axiom,
equidistant(Y,extension(X,Y,W,V),W,V),
file('GEO002-0.ax',segment_construction2) ).
cnf(outer_five_segment,axiom,
( equidistant(Z,V,Z1,V1)
| X = Y
| ~ between(X1,Y1,Z1)
| ~ between(X,Y,Z)
| ~ equidistant(Y,V,Y1,V1)
| ~ equidistant(X,V,X1,V1)
| ~ equidistant(Y,Z,Y1,Z1)
| ~ equidistant(X,Y,X1,Y1) ),
file('GEO002-0.ax',outer_five_segment) ).
cnf(identity_for_betweeness,axiom,
( X = Y
| ~ between(X,Y,X) ),
file('GEO002-0.ax',identity_for_betweeness) ).
cnf(inner_pasch1,axiom,
( between(V,inner_pasch(U,V,W,X,Y),Y)
| ~ between(Y,X,W)
| ~ between(U,V,W) ),
file('GEO002-0.ax',inner_pasch1) ).
cnf(inner_pasch2,axiom,
( between(X,inner_pasch(U,V,W,X,Y),U)
| ~ between(Y,X,W)
| ~ between(U,V,W) ),
file('GEO002-0.ax',inner_pasch2) ).
cnf(lower_dimension1,axiom,
~ between(lower_dimension_point_1,lower_dimension_point_2,lower_dimension_point_3),
file('GEO002-0.ax',lower_dimension1) ).
cnf(lower_dimension2,axiom,
~ between(lower_dimension_point_2,lower_dimension_point_3,lower_dimension_point_1),
file('GEO002-0.ax',lower_dimension2) ).
cnf(lower_dimension3,axiom,
~ between(lower_dimension_point_3,lower_dimension_point_1,lower_dimension_point_2),
file('GEO002-0.ax',lower_dimension3) ).
cnf(upper_dimension,axiom,
( W = V
| between(Z,X,Y)
| between(Y,Z,X)
| between(X,Y,Z)
| ~ equidistant(Z,W,Z,V)
| ~ equidistant(Y,W,Y,V)
| ~ equidistant(X,W,X,V) ),
file('GEO002-0.ax',upper_dimension) ).
cnf(euclid1,axiom,
( between(U,V,euclid1(U,V,W,X,Y))
| U = W
| ~ between(V,W,X)
| ~ between(U,W,Y) ),
file('GEO002-0.ax',euclid1) ).
cnf(euclid2,axiom,
( between(U,X,euclid2(U,V,W,X,Y))
| U = W
| ~ between(V,W,X)
| ~ between(U,W,Y) ),
file('GEO002-0.ax',euclid2) ).
cnf(euclid3,axiom,
( between(euclid1(U,V,W,X,Y),Y,euclid2(U,V,W,X,Y))
| U = W
| ~ between(V,W,X)
| ~ between(U,W,Y) ),
file('GEO002-0.ax',euclid3) ).
cnf(continuity1,axiom,
( between(V1,continuous(U,V,V1,W,X,X1),X1)
| ~ between(V,W,X)
| ~ between(U,V,X)
| ~ equidistant(U,X,U,X1)
| ~ equidistant(U,V,U,V1) ),
file('GEO002-0.ax',continuity1) ).
cnf(continuity2,axiom,
( equidistant(U,W,U,continuous(U,V,V1,W,X,X1))
| ~ between(V,W,X)
| ~ between(U,V,X)
| ~ equidistant(U,X,U,X1)
| ~ equidistant(U,V,U,V1) ),
file('GEO002-0.ax',continuity2) ).
cnf(prove_congruence,negated_conjecture,
~ equidistant(u,u,v,v),
file('theBenchmark.p',prove_congruence) ).
cnf(equality_1,axiom,
Eq_x_0 = Eq_x_0,
theory(equality,[reflexivity]) ).
cnf(equality_2,axiom,
( Eq_x_1 = Eq_x_0
| Eq_x_0 != Eq_x_1 ),
theory(equality,[symmetry]) ).
cnf(equality_3,axiom,
( Eq_x_0 = Eq_x_2
| Eq_x_1 != Eq_x_2
| Eq_x_0 != Eq_x_1 ),
theory(equality,[transitivity]) ).
cnf(equality_4,axiom,
( extension(Eq_x_0,Eq_x_1,Eq_x_2,Eq_x_3) = extension(Eq_y_0,Eq_y_1,Eq_y_2,Eq_y_3)
| Eq_x_3 != Eq_y_3
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_5,axiom,
( inner_pasch(Eq_x_0,Eq_x_1,Eq_x_2,Eq_x_3,Eq_x_4) = inner_pasch(Eq_y_0,Eq_y_1,Eq_y_2,Eq_y_3,Eq_y_4)
| Eq_x_4 != Eq_y_4
| Eq_x_3 != Eq_y_3
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_6,axiom,
( euclid1(Eq_x_0,Eq_x_1,Eq_x_2,Eq_x_3,Eq_x_4) = euclid1(Eq_y_0,Eq_y_1,Eq_y_2,Eq_y_3,Eq_y_4)
| Eq_x_4 != Eq_y_4
| Eq_x_3 != Eq_y_3
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_7,axiom,
( euclid2(Eq_x_0,Eq_x_1,Eq_x_2,Eq_x_3,Eq_x_4) = euclid2(Eq_y_0,Eq_y_1,Eq_y_2,Eq_y_3,Eq_y_4)
| Eq_x_4 != Eq_y_4
| Eq_x_3 != Eq_y_3
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_8,axiom,
( continuous(Eq_x_0,Eq_x_1,Eq_x_2,Eq_x_3,Eq_x_4,Eq_x_5) = continuous(Eq_y_0,Eq_y_1,Eq_y_2,Eq_y_3,Eq_y_4,Eq_y_5)
| Eq_x_5 != Eq_y_5
| Eq_x_4 != Eq_y_4
| Eq_x_3 != Eq_y_3
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_9,axiom,
( equidistant(Eq_y_0,Eq_y_1,Eq_y_2,Eq_y_3)
| ~ equidistant(Eq_x_0,Eq_x_1,Eq_x_2,Eq_x_3)
| Eq_x_3 != Eq_y_3
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_10,axiom,
( between(Eq_y_0,Eq_y_1,Eq_y_2)
| ~ between(Eq_x_0,Eq_x_1,Eq_x_2)
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(sat_proved,plain,
$false,
inference(cadical,[status(thm)],[]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GEO024-2 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.03 This is a CNF_UNS_RFO_SEQ_NHN problem
% 0.00/0.04 % Command : /export/starexec/sandbox2/solver/bin/connect++ --verbosity 1 --no-colour --tptp-proof --schedule default --timeout 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.10/0.36 % Computer : n003.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Sat Sep 19 07:10:13 UTC 2026
% 0.10/0.37 % CPUTime :
% 2.36/2.68 % SZS status Unsatisfiable for theBenchmark
% 2.36/2.68 % SZS output start Proof for theBenchmark
% See solution above
%------------------------------------------------------------------------------