%------------------------------------------------------------------------------
% File : ConnectPP---0.7.2
% Problem : GEO034-3 : TPTP v9.3.1. Bugfixed v1.2.1.
% 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 : n015.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:18 AM UTC 2026
% Result : Unsatisfiable 222.25s 222.53s
% Output : Proof 225.75s
% 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(reflection,axiom,
reflection(U,V) = extension(U,V,U,V),
file('GEO002-2.ax',reflection) ).
cnf(d1,axiom,
equidistant(U,V,U,V),
file('theBenchmark.p',d1) ).
cnf(d2,axiom,
( equidistant(W,X,U,V)
| ~ equidistant(U,V,W,X) ),
file('theBenchmark.p',d2) ).
cnf(d3,axiom,
( equidistant(V,U,W,X)
| ~ equidistant(U,V,W,X) ),
file('theBenchmark.p',d3) ).
cnf(d4_1,axiom,
( equidistant(U,V,X,W)
| ~ equidistant(U,V,W,X) ),
file('theBenchmark.p',d4_1) ).
cnf(d4_2,axiom,
( equidistant(V,U,X,W)
| ~ equidistant(U,V,W,X) ),
file('theBenchmark.p',d4_2) ).
cnf(d4_3,axiom,
( equidistant(W,X,V,U)
| ~ equidistant(U,V,W,X) ),
file('theBenchmark.p',d4_3) ).
cnf(d4_4,axiom,
( equidistant(X,W,U,V)
| ~ equidistant(U,V,W,X) ),
file('theBenchmark.p',d4_4) ).
cnf(d4_5,axiom,
( equidistant(X,W,V,U)
| ~ equidistant(U,V,W,X) ),
file('theBenchmark.p',d4_5) ).
cnf(d5,axiom,
( equidistant(U,V,Y,Z)
| ~ equidistant(W,X,Y,Z)
| ~ equidistant(U,V,W,X) ),
file('theBenchmark.p',d5) ).
cnf(e1,axiom,
V = extension(U,V,W,W),
file('theBenchmark.p',e1) ).
cnf(b0,axiom,
( between(U,V,Y)
| Y != extension(U,V,W,X) ),
file('theBenchmark.p',b0) ).
cnf(r2_1,axiom,
between(U,V,reflection(U,V)),
file('theBenchmark.p',r2_1) ).
cnf(r2_2,axiom,
equidistant(V,reflection(U,V),U,V),
file('theBenchmark.p',r2_2) ).
cnf(r3_1,axiom,
( V = reflection(U,V)
| U != V ),
file('theBenchmark.p',r3_1) ).
cnf(r3_2,axiom,
U = reflection(U,U),
file('theBenchmark.p',r3_2) ).
cnf(r4,axiom,
( U = V
| V != reflection(U,V) ),
file('theBenchmark.p',r4) ).
cnf(d7,axiom,
equidistant(U,U,V,V),
file('theBenchmark.p',d7) ).
cnf(d8,axiom,
( equidistant(U,W,U1,W1)
| ~ between(U1,V1,W1)
| ~ between(U,V,W)
| ~ equidistant(V,W,V1,W1)
| ~ equidistant(U,V,U1,V1) ),
file('theBenchmark.p',d8) ).
cnf(d9,axiom,
( W = X
| U = V
| ~ equidistant(V,W,V,X)
| ~ between(U,V,X)
| ~ between(U,V,W) ),
file('theBenchmark.p',d9) ).
cnf(d10_1,axiom,
( W = extension(U,V,V,W)
| U = V
| ~ between(U,V,W) ),
file('theBenchmark.p',d10_1) ).
cnf(d10_2,axiom,
( U = V
| extension(U,V,W,X) = extension(U,V,Y,Z)
| ~ equidistant(W,X,Y,Z) ),
file('theBenchmark.p',d10_2) ).
cnf(d10_3,axiom,
( U = V
| extension(U,V,U,V) = extension(U,V,V,U) ),
file('theBenchmark.p',d10_3) ).
cnf(r5,axiom,
equidistant(V,U,V,reflection(reflection(U,V),V)),
file('theBenchmark.p',r5) ).
cnf(r6,axiom,
U = reflection(reflection(U,V),V),
file('theBenchmark.p',r6) ).
cnf(t3,axiom,
between(U,V,V),
file('theBenchmark.p',t3) ).
cnf(b1,axiom,
( between(V,W,X)
| U != X
| ~ between(U,W,X) ),
file('theBenchmark.p',b1) ).
cnf(t1,axiom,
( between(W,V,U)
| ~ between(U,V,W) ),
file('theBenchmark.p',t1) ).
cnf(t2,axiom,
between(U,U,V),
file('theBenchmark.p',t2) ).
cnf(b2,axiom,
( U = V
| ~ between(V,U,W)
| ~ between(U,V,W) ),
file('theBenchmark.p',b2) ).
cnf(b3,axiom,
( V = W
| ~ between(U,W,V)
| ~ between(U,V,W) ),
file('theBenchmark.p',b3) ).
cnf(t6_1,axiom,
( V = W
| U = V
| ~ between(V,U,W)
| ~ between(U,V,W) ),
file('theBenchmark.p',t6_1) ).
cnf(t6_2,axiom,
( V = W
| U = V
| ~ between(U,W,V)
| ~ between(U,V,W) ),
file('theBenchmark.p',t6_2) ).
cnf(b4,axiom,
( between(U,V,W)
| ~ between(V,W,X)
| ~ between(U,V,W) ),
file('theBenchmark.p',b4) ).
cnf(b5,axiom,
( between(V,W,X)
| ~ between(U,W,X)
| ~ between(U,V,W) ),
file('theBenchmark.p',b5) ).
cnf(b6,axiom,
( V = W
| between(U,W,X)
| ~ between(V,W,X)
| ~ between(U,V,W) ),
file('theBenchmark.p',b6) ).
cnf(b7,axiom,
( V = W
| between(U,V,X)
| ~ between(V,W,X)
| ~ between(U,V,W) ),
file('theBenchmark.p',b7) ).
cnf(b8,axiom,
( between(U,W,X)
| ~ between(V,W,X)
| ~ between(U,V,X) ),
file('theBenchmark.p',b8) ).
cnf(b9,axiom,
( between(U,V,X)
| ~ between(U,W,X)
| ~ between(U,V,W) ),
file('theBenchmark.p',b9) ).
cnf(e2_1,axiom,
lower_dimension_point_1 != lower_dimension_point_2,
file('theBenchmark.p',e2_1) ).
cnf(e2_2,axiom,
lower_dimension_point_2 != lower_dimension_point_3,
file('theBenchmark.p',e2_2) ).
cnf(e2_3,axiom,
lower_dimension_point_1 != lower_dimension_point_3,
file('theBenchmark.p',e2_3) ).
cnf(e3_1,axiom,
V != extension(U,V,lower_dimension_point_1,lower_dimension_point_2),
file('theBenchmark.p',e3_1) ).
cnf(e3_2,axiom,
equidistant(V,extension(U,V,lower_dimension_point_1,lower_dimension_point_2),X,extension(W,X,lower_dimension_point_1,lower_dimension_point_2)),
file('theBenchmark.p',e3_2) ).
cnf(e3_3,axiom,
between(U,V,extension(U,V,lower_dimension_point_1,lower_dimension_point_2)),
file('theBenchmark.p',e3_3) ).
cnf(b10,axiom,
( between(V,inner_pasch(V1,inner_pasch(U,X,U1,V1,W),U,V,W),V1)
| between(X,inner_pasch(V1,inner_pasch(U,X,U1,V1,W),U,V,W),W)
| ~ between(U,X,U1)
| ~ between(U1,V1,W)
| ~ between(U,V,W) ),
file('theBenchmark.p',b10) ).
cnf(d11,axiom,
( W = W1
| U = V
| ~ equidistant(V,W,V,W1)
| ~ equidistant(U,W,U,W1)
| ~ between(U,V,W) ),
file('theBenchmark.p',d11) ).
cnf(d12,axiom,
( equidistant(V,X,V1,X1)
| ~ between(U1,V1,W1)
| ~ between(U,V,W)
| ~ equidistant(W,X,W1,X1)
| ~ equidistant(U,X,U1,X1)
| ~ equidistant(U,W,U1,W1)
| ~ equidistant(U,V,U1,V1) ),
file('theBenchmark.p',d12) ).
cnf(d13,axiom,
( equidistant(V,W,V1,W1)
| ~ equidistant(U,W,U1,W1)
| ~ equidistant(U,V,U1,V1)
| ~ between(U1,V1,W1)
| ~ between(U,V,W) ),
file('theBenchmark.p',d13) ).
cnf(d14,axiom,
( equidistant(V,X,V1,X1)
| ~ between(U1,V1,W1)
| ~ between(U,V,W)
| ~ equidistant(W,X,W1,X1)
| ~ equidistant(U,X,U1,X1)
| ~ equidistant(V,W,V1,W1)
| ~ equidistant(U,V,U1,V1) ),
file('theBenchmark.p',d14) ).
cnf(v_between_u_and_w,hypothesis,
between(u,v,w),
file('theBenchmark.p',v_between_u_and_w) ).
cnf(u_to_v_equals_u_to_x,hypothesis,
equidistant(u,v,u,x),
file('theBenchmark.p',u_to_v_equals_u_to_x) ).
cnf(w_to_v_equals_w_to_x,hypothesis,
equidistant(w,v,w,x),
file('theBenchmark.p',w_to_v_equals_w_to_x) ).
cnf(prove_v_is_x,negated_conjecture,
v != x,
file('theBenchmark.p',prove_v_is_x) ).
cnf(b4_true,plain,
$true,
inference(clause_is_true,[status(thm)],[b4]) ).
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,
( reflection(Eq_x_0,Eq_x_1) = reflection(Eq_y_0,Eq_y_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_10,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_11,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.02 % Problem : GEO034-3 : TPTP v9.3.1. Bugfixed v1.2.1.
% 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.37 % Computer : n015.cluster.edu
% 0.10/0.37 % Model : x86_64 x86_64
% 0.10/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.37 % Memory : 8046.5625MB
% 0.10/0.37 % OS : Linux 6.8.0-71-generic
% 0.10/0.37 % CPULimit : 300
% 0.10/0.37 % WCLimit : 300
% 0.10/0.37 % DateTime : Sat Sep 19 07:20:03 UTC 2026
% 0.10/0.38 % CPUTime :
% 222.25/222.53 % SZS status Unsatisfiable for theBenchmark
% 222.25/222.53 % SZS output start Proof for theBenchmark
% See solution above
%------------------------------------------------------------------------------