%------------------------------------------------------------------------------
% File : CSE_E---1.7
% Problem : GEO031-2 : TPTP v9.2.1. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox2/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox2/solver/bin/cse --final-prover /export/starexec/sandbox2/solver/bin/eprover --proof-time %d --global-time-limit %d
% Computer : n011.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 : Tue May 5 04:19:04 PM UTC 2026
% Result : Unsatisfiable 96.90s 80.02s
% Output : CNFRefutation 98.90s
% Verified :
% SZS Type : Refutation
% Derivation depth : 5
% Number of leaves : 35
% Syntax : Number of clauses : 227 ( 192 unt; 10 nHn; 61 RR)
% Number of literals : 323 ( 28 equ; 93 neg)
% Maximal clause size : 8 ( 1 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 4 ( 2 usr; 1 prp; 0-4 aty)
% Number of functors : 16 ( 16 usr; 11 con; 0-6 aty)
% Number of variables : 779 ( 155 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(continuity2,axiom,
( equidistant(X1,X6,X1,continuous(X1,X2,X3,X6,X4,X5))
| ~ equidistant(X1,X2,X1,X3)
| ~ equidistant(X1,X4,X1,X5)
| ~ between(X1,X2,X4)
| ~ between(X2,X6,X4) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO002-0.ax',continuity2) ).
cnf(continuity1,axiom,
( between(X3,continuous(X1,X2,X3,X6,X4,X5),X5)
| ~ equidistant(X1,X2,X1,X3)
| ~ equidistant(X1,X4,X1,X5)
| ~ between(X1,X2,X4)
| ~ between(X2,X6,X4) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO002-0.ax',continuity1) ).
cnf(euclid3,axiom,
( X1 = X2
| between(euclid1(X1,X4,X2,X5,X3),X3,euclid2(X1,X4,X2,X5,X3))
| ~ between(X1,X2,X3)
| ~ between(X4,X2,X5) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO002-0.ax',euclid3) ).
cnf(euclid1,axiom,
( X1 = X2
| between(X1,X4,euclid1(X1,X4,X2,X5,X3))
| ~ between(X1,X2,X3)
| ~ between(X4,X2,X5) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO002-0.ax',euclid1) ).
cnf(euclid2,axiom,
( X1 = X2
| between(X1,X5,euclid2(X1,X4,X2,X5,X3))
| ~ between(X1,X2,X3)
| ~ between(X4,X2,X5) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO002-0.ax',euclid2) ).
cnf(inner_pasch1,axiom,
( between(X2,inner_pasch(X1,X2,X3,X5,X4),X4)
| ~ between(X1,X2,X3)
| ~ between(X4,X5,X3) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO002-0.ax',inner_pasch1) ).
cnf(inner_pasch2,axiom,
( between(X5,inner_pasch(X1,X2,X3,X5,X4),X1)
| ~ between(X1,X2,X3)
| ~ between(X4,X5,X3) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO002-0.ax',inner_pasch2) ).
cnf(outer_five_segment,axiom,
( X1 = X2
| equidistant(X5,X7,X6,X8)
| ~ equidistant(X1,X2,X3,X4)
| ~ equidistant(X2,X5,X4,X6)
| ~ equidistant(X1,X7,X3,X8)
| ~ equidistant(X2,X7,X4,X8)
| ~ between(X1,X2,X5)
| ~ between(X3,X4,X6) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO002-0.ax',outer_five_segment) ).
cnf(upper_dimension,axiom,
( between(X1,X4,X5)
| between(X4,X5,X1)
| between(X5,X1,X4)
| X2 = X3
| ~ equidistant(X1,X2,X1,X3)
| ~ equidistant(X4,X2,X4,X3)
| ~ equidistant(X5,X2,X5,X3) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO002-0.ax',upper_dimension) ).
cnf(transitivity_for_equidistance,axiom,
( equidistant(X3,X4,X5,X6)
| ~ equidistant(X1,X2,X3,X4)
| ~ equidistant(X1,X2,X5,X6) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO002-0.ax',transitivity_for_equidistance) ).
cnf(segment_construction2,axiom,
equidistant(X1,extension(X2,X1,X3,X4),X3,X4),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO002-0.ax',segment_construction2) ).
cnf(segment_construction1,axiom,
between(X1,X2,extension(X1,X2,X3,X4)),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO002-0.ax',segment_construction1) ).
cnf(identity_for_equidistance,axiom,
( X1 = X2
| ~ equidistant(X1,X2,X3,X3) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO002-0.ax',identity_for_equidistance) ).
cnf(prove_v_to_x_equals_v1_to_x1,negated_conjecture,
~ equidistant(v,x,v1,x1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_v_to_x_equals_v1_to_x1) ).
cnf(reflexivity_for_equidistance,axiom,
equidistant(X1,X2,X2,X1),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO002-0.ax',reflexivity_for_equidistance) ).
cnf(w_to_x_equals_w1_to_x1,hypothesis,
equidistant(w,x,w1,x1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',w_to_x_equals_w1_to_x1) ).
cnf(u_to_x_equals_u1_to_x1,hypothesis,
equidistant(u,x,u1,x1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u_to_x_equals_u1_to_x1) ).
cnf(u_to_w_equals_u1_to_w1,hypothesis,
equidistant(u,w,u1,w1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u_to_w_equals_u1_to_w1) ).
cnf(u_to_v_equals_u1_to_v1,hypothesis,
equidistant(u,v,u1,v1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u_to_v_equals_u1_to_v1) ).
cnf(identity_for_betweeness,axiom,
( X1 = X2
| ~ between(X1,X2,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO002-0.ax',identity_for_betweeness) ).
cnf(lower_dimension3,axiom,
~ between(lower_dimension_point_3,lower_dimension_point_1,lower_dimension_point_2),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO002-0.ax',lower_dimension3) ).
cnf(lower_dimension2,axiom,
~ between(lower_dimension_point_2,lower_dimension_point_3,lower_dimension_point_1),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO002-0.ax',lower_dimension2) ).
cnf(lower_dimension1,axiom,
~ between(lower_dimension_point_1,lower_dimension_point_2,lower_dimension_point_3),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO002-0.ax',lower_dimension1) ).
cnf(v1_between_u1_and_w1,hypothesis,
between(u1,v1,w1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',v1_between_u1_and_w1) ).
cnf(v_between_u_and_w,hypothesis,
between(u,v,w),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',v_between_u_and_w) ).
cnf(i_0_25,axiom,
( equidistant(X1,X6,X1,continuous(X1,X2,X3,X6,X4,X5))
| ~ equidistant(X1,X2,X1,X3)
| ~ equidistant(X1,X4,X1,X5)
| ~ between(X1,X2,X4)
| ~ between(X2,X6,X4) ),
continuity2,
[final] ).
cnf(i_0_26,axiom,
( between(X3,continuous(X1,X2,X3,X6,X4,X5),X5)
| ~ equidistant(X1,X2,X1,X3)
| ~ equidistant(X1,X4,X1,X5)
| ~ between(X1,X2,X4)
| ~ between(X2,X6,X4) ),
continuity1,
[final] ).
cnf(i_0_27,axiom,
( X1 = X2
| between(euclid1(X1,X4,X2,X5,X3),X3,euclid2(X1,X4,X2,X5,X3))
| ~ between(X1,X2,X3)
| ~ between(X4,X2,X5) ),
euclid3,
[final] ).
cnf(i_0_28,axiom,
( X1 = X2
| between(X1,X4,euclid1(X1,X4,X2,X5,X3))
| ~ between(X1,X2,X3)
| ~ between(X4,X2,X5) ),
euclid1,
[final] ).
cnf(i_0_29,axiom,
( X1 = X2
| between(X1,X5,euclid2(X1,X4,X2,X5,X3))
| ~ between(X1,X2,X3)
| ~ between(X4,X2,X5) ),
euclid2,
[final] ).
cnf(i_0_30,axiom,
( between(X2,inner_pasch(X1,X2,X3,X5,X4),X4)
| ~ between(X1,X2,X3)
| ~ between(X4,X5,X3) ),
inner_pasch1,
[final] ).
cnf(i_0_31,axiom,
( between(X5,inner_pasch(X1,X2,X3,X5,X4),X1)
| ~ between(X1,X2,X3)
| ~ between(X4,X5,X3) ),
inner_pasch2,
[final] ).
cnf(i_0_32,axiom,
( X1 = X2
| equidistant(X5,X7,X6,X8)
| ~ equidistant(X1,X2,X3,X4)
| ~ equidistant(X2,X5,X4,X6)
| ~ equidistant(X1,X7,X3,X8)
| ~ equidistant(X2,X7,X4,X8)
| ~ between(X1,X2,X5)
| ~ between(X3,X4,X6) ),
outer_five_segment,
[final] ).
cnf(i_0_33,axiom,
( between(X1,X4,X5)
| between(X4,X5,X1)
| between(X5,X1,X4)
| X2 = X3
| ~ equidistant(X1,X2,X1,X3)
| ~ equidistant(X4,X2,X4,X3)
| ~ equidistant(X5,X2,X5,X3) ),
upper_dimension,
[final] ).
cnf(i_0_34,axiom,
( equidistant(X3,X4,X5,X6)
| ~ equidistant(X1,X2,X3,X4)
| ~ equidistant(X1,X2,X5,X6) ),
transitivity_for_equidistance,
[final] ).
cnf(i_0_35,axiom,
equidistant(X1,extension(X2,X1,X3,X4),X3,X4),
segment_construction2,
[final] ).
cnf(i_0_36,axiom,
between(X1,X2,extension(X1,X2,X3,X4)),
segment_construction1,
[final] ).
cnf(i_0_37,axiom,
( X1 = X2
| ~ equidistant(X1,X2,X3,X3) ),
identity_for_equidistance,
[final] ).
cnf(i_0_38,negated_conjecture,
~ equidistant(v,x,v1,x1),
prove_v_to_x_equals_v1_to_x1,
[final] ).
cnf(i_0_39,axiom,
equidistant(X1,X2,X2,X1),
reflexivity_for_equidistance,
[final] ).
cnf(i_0_40,hypothesis,
equidistant(w,x,w1,x1),
w_to_x_equals_w1_to_x1,
[final] ).
cnf(i_0_41,hypothesis,
equidistant(u,x,u1,x1),
u_to_x_equals_u1_to_x1,
[final] ).
cnf(i_0_42,hypothesis,
equidistant(u,w,u1,w1),
u_to_w_equals_u1_to_w1,
[final] ).
cnf(i_0_43,hypothesis,
equidistant(u,v,u1,v1),
u_to_v_equals_u1_to_v1,
[final] ).
cnf(i_0_44,axiom,
( X1 = X2
| ~ between(X1,X2,X1) ),
identity_for_betweeness,
[final] ).
cnf(i_0_45,axiom,
~ between(lower_dimension_point_3,lower_dimension_point_1,lower_dimension_point_2),
lower_dimension3,
[final] ).
cnf(i_0_46,axiom,
~ between(lower_dimension_point_2,lower_dimension_point_3,lower_dimension_point_1),
lower_dimension2,
[final] ).
cnf(i_0_47,axiom,
~ between(lower_dimension_point_1,lower_dimension_point_2,lower_dimension_point_3),
lower_dimension1,
[final] ).
cnf(i_0_48,hypothesis,
between(u1,v1,w1),
v1_between_u1_and_w1,
[final] ).
cnf(i_0_49,hypothesis,
between(u,v,w),
v_between_u_and_w,
[final] ).
cnf(i_0_50,axiom,
X1 = X1 ).
cnf(i_0_51,axiom,
( X1 = X2
| X2 != X1 ) ).
cnf(i_0_52,axiom,
( X1 = X2
| X1 != X3
| X3 != X2 ) ).
cnf(i_0_53,axiom,
( X1 != X2
| ~ equidistant(X1,X3,X4,X5)
| equidistant(X2,X3,X4,X5) ) ).
cnf(i_0_54,axiom,
( X1 != X2
| ~ equidistant(X3,X1,X4,X5)
| equidistant(X3,X2,X4,X5) ) ).
cnf(i_0_55,axiom,
( X1 != X2
| ~ equidistant(X3,X4,X1,X5)
| equidistant(X3,X4,X2,X5) ) ).
cnf(i_0_56,axiom,
( X1 != X2
| ~ equidistant(X3,X4,X5,X1)
| equidistant(X3,X4,X5,X2) ) ).
cnf(i_0_57,axiom,
( X1 != X2
| ~ between(X1,X3,X4)
| between(X2,X3,X4) ) ).
cnf(i_0_58,axiom,
( X1 != X2
| ~ between(X3,X1,X4)
| between(X3,X2,X4) ) ).
cnf(i_0_59,axiom,
( X1 != X2
| ~ between(X3,X4,X1)
| between(X3,X4,X2) ) ).
cnf(i_0_60,plain,
X1 = extension(X2,X1,X3,X3),
inference(scs_inference,[],[i_0_35,i_0_37]) ).
cnf(i_0_61,plain,
equidistant(X1,extension(X2,X1,X3,X4),X3,X4),
inference(rename_variables,[],[i_0_35]) ).
cnf(i_0_63,plain,
~ equidistant(X1,v1,v,x),
inference(scs_inference,[],[i_0_38,i_0_39,i_0_35,i_0_37,i_0_34]) ).
cnf(i_0_64,plain,
equidistant(X1,X2,X2,X1),
inference(rename_variables,[],[i_0_39]) ).
cnf(i_0_67,plain,
equidistant(X1,extension(X2,X1,X3,X4),X3,X4),
inference(rename_variables,[],[i_0_35]) ).
cnf(i_0_69,plain,
between(X1,X2,extension(X1,X2,X3,X4)),
inference(rename_variables,[],[i_0_36]) ).
cnf(i_0_74,plain,
equidistant(X1,X2,X2,X1),
inference(rename_variables,[],[i_0_39]) ).
cnf(i_0_75,plain,
between(X1,X2,extension(X1,X2,X3,X4)),
inference(rename_variables,[],[i_0_36]) ).
cnf(i_0_76,plain,
between(X1,X2,extension(X1,X2,X3,X4)),
inference(rename_variables,[],[i_0_36]) ).
cnf(i_0_78,plain,
between(X1,X2,extension(X1,X2,X3,X4)),
inference(rename_variables,[],[i_0_36]) ).
cnf(i_0_99,plain,
equidistant(u1,X1,u1,X1),
inference(scs_inference,[],[i_0_41,i_0_34]) ).
cnf(i_0_115,plain,
equidistant(u1,w1,u1,w1),
inference(scs_inference,[],[i_0_42,i_0_34]) ).
cnf(i_0_131,plain,
equidistant(u1,v1,u1,v1),
inference(scs_inference,[],[i_0_43,i_0_34]) ).
cnf(i_0_147,plain,
~ equidistant(X1,extension(X2,X1,v1,X3),v,x),
inference(scs_inference,[],[i_0_38,i_0_35,i_0_34]) ).
cnf(i_0_148,plain,
equidistant(X1,extension(X2,X1,X3,X4),X3,X4),
inference(rename_variables,[],[i_0_35]) ).
cnf(i_0_449,plain,
equidistant(X1,extension(X2,X1,X3,X4),X3,X4),
inference(rename_variables,[],[i_0_35]) ).
cnf(i_0_463,plain,
equidistant(X1,extension(X2,X1,X3,X4),X3,X4),
inference(rename_variables,[],[i_0_35]) ).
cnf(i_0_477,plain,
equidistant(X1,extension(X2,X1,X3,X4),X3,X4),
inference(rename_variables,[],[i_0_35]) ).
cnf(i_0_489,plain,
equidistant(X1,extension(X2,X1,X3,X4),X3,X4),
inference(rename_variables,[],[i_0_35]) ).
cnf(i_0_502,plain,
equidistant(X1,extension(X2,X1,X3,X4),X3,X4),
inference(rename_variables,[],[i_0_35]) ).
cnf(i_0_506,plain,
equidistant(X1,extension(X2,X1,X3,X4),X3,X4),
inference(rename_variables,[],[i_0_35]) ).
cnf(i_0_510,plain,
equidistant(X1,extension(X2,X1,X3,X4),X3,X4),
inference(rename_variables,[],[i_0_35]) ).
cnf(i_0_514,plain,
equidistant(X1,extension(X2,X1,X3,X4),X3,X4),
inference(rename_variables,[],[i_0_35]) ).
cnf(i_0_518,plain,
equidistant(X1,extension(X2,X1,X3,X4),X3,X4),
inference(rename_variables,[],[i_0_35]) ).
cnf(i_0_522,plain,
equidistant(X1,extension(X2,X1,X3,X4),X3,X4),
inference(rename_variables,[],[i_0_35]) ).
cnf(i_0_526,plain,
equidistant(X1,extension(X2,X1,X3,X4),X3,X4),
inference(rename_variables,[],[i_0_35]) ).
cnf(i_0_530,plain,
equidistant(X1,extension(X2,X1,X3,X4),X3,X4),
inference(rename_variables,[],[i_0_35]) ).
cnf(i_0_534,plain,
equidistant(X1,extension(X2,X1,X3,X4),X3,X4),
inference(rename_variables,[],[i_0_35]) ).
cnf(i_0_538,plain,
equidistant(X1,extension(X2,X1,X3,X4),X3,X4),
inference(rename_variables,[],[i_0_35]) ).
cnf(i_0_542,plain,
equidistant(X1,extension(X2,X1,X3,X4),X3,X4),
inference(rename_variables,[],[i_0_35]) ).
cnf(i_0_546,plain,
equidistant(X1,extension(X2,X1,X3,X4),X3,X4),
inference(rename_variables,[],[i_0_35]) ).
cnf(i_0_550,plain,
equidistant(X1,extension(X2,X1,X3,X4),X3,X4),
inference(rename_variables,[],[i_0_35]) ).
cnf(i_0_554,plain,
equidistant(X1,extension(X2,X1,X3,X4),X3,X4),
inference(rename_variables,[],[i_0_35]) ).
cnf(i_0_558,plain,
equidistant(X1,extension(X2,X1,X3,X4),X3,X4),
inference(rename_variables,[],[i_0_35]) ).
cnf(i_0_562,plain,
equidistant(X1,extension(X2,X1,X3,X4),X3,X4),
inference(rename_variables,[],[i_0_35]) ).
cnf(i_0_566,plain,
equidistant(X1,extension(X2,X1,X3,X4),X3,X4),
inference(rename_variables,[],[i_0_35]) ).
cnf(i_0_570,plain,
equidistant(X1,extension(X2,X1,X3,X4),X3,X4),
inference(rename_variables,[],[i_0_35]) ).
cnf(i_0_574,plain,
equidistant(X1,extension(X2,X1,X3,X4),X3,X4),
inference(rename_variables,[],[i_0_35]) ).
cnf(i_0_578,plain,
equidistant(X1,extension(X2,X1,X3,X4),X3,X4),
inference(rename_variables,[],[i_0_35]) ).
cnf(i_0_582,plain,
equidistant(X1,extension(X2,X1,X3,X4),X3,X4),
inference(rename_variables,[],[i_0_35]) ).
cnf(i_0_586,plain,
equidistant(X1,extension(X2,X1,X3,X4),X3,X4),
inference(rename_variables,[],[i_0_35]) ).
cnf(i_0_590,plain,
equidistant(X1,extension(X2,X1,X3,X4),X3,X4),
inference(rename_variables,[],[i_0_35]) ).
cnf(i_0_594,plain,
equidistant(X1,extension(X2,X1,X3,X4),X3,X4),
inference(rename_variables,[],[i_0_35]) ).
cnf(i_0_598,plain,
equidistant(X1,extension(X2,X1,X3,X4),X3,X4),
inference(rename_variables,[],[i_0_35]) ).
cnf(i_0_602,plain,
equidistant(X1,extension(X2,X1,X3,X4),X3,X4),
inference(rename_variables,[],[i_0_35]) ).
cnf(i_0_606,plain,
equidistant(X1,extension(X2,X1,X3,X4),X3,X4),
inference(rename_variables,[],[i_0_35]) ).
cnf(i_0_610,plain,
equidistant(X1,extension(X2,X1,X3,X4),X3,X4),
inference(rename_variables,[],[i_0_35]) ).
cnf(i_0_614,plain,
equidistant(X1,extension(X2,X1,X3,X4),X3,X4),
inference(rename_variables,[],[i_0_35]) ).
cnf(i_0_618,plain,
equidistant(X1,extension(X2,X1,X3,X4),X3,X4),
inference(rename_variables,[],[i_0_35]) ).
cnf(i_0_622,plain,
equidistant(X1,extension(X2,X1,X3,X4),X3,X4),
inference(rename_variables,[],[i_0_35]) ).
cnf(i_0_626,plain,
equidistant(X1,extension(X2,X1,X3,X4),X3,X4),
inference(rename_variables,[],[i_0_35]) ).
cnf(i_0_630,plain,
equidistant(X1,extension(X2,X1,X3,X4),X3,X4),
inference(rename_variables,[],[i_0_35]) ).
cnf(i_0_634,plain,
equidistant(X1,extension(X2,X1,X3,X4),X3,X4),
inference(rename_variables,[],[i_0_35]) ).
cnf(i_0_638,plain,
equidistant(X1,extension(X2,X1,X3,X4),X3,X4),
inference(rename_variables,[],[i_0_35]) ).
cnf(i_0_642,plain,
equidistant(X1,extension(X2,X1,X3,X4),X3,X4),
inference(rename_variables,[],[i_0_35]) ).
cnf(i_0_646,plain,
equidistant(X1,extension(X2,X1,X3,X4),X3,X4),
inference(rename_variables,[],[i_0_35]) ).
cnf(i_0_650,plain,
equidistant(X1,extension(X2,X1,X3,X4),X3,X4),
inference(rename_variables,[],[i_0_35]) ).
cnf(i_0_654,plain,
equidistant(X1,extension(X2,X1,X3,X4),X3,X4),
inference(rename_variables,[],[i_0_35]) ).
cnf(i_0_658,plain,
equidistant(X1,extension(X2,X1,X3,X4),X3,X4),
inference(rename_variables,[],[i_0_35]) ).
cnf(i_0_662,plain,
equidistant(X1,extension(X2,X1,X3,X4),X3,X4),
inference(rename_variables,[],[i_0_35]) ).
cnf(i_0_666,plain,
equidistant(X1,extension(X2,X1,X3,X4),X3,X4),
inference(rename_variables,[],[i_0_35]) ).
cnf(i_0_670,plain,
equidistant(X1,extension(X2,X1,X3,X4),X3,X4),
inference(rename_variables,[],[i_0_35]) ).
cnf(i_0_674,plain,
equidistant(X1,extension(X2,X1,X3,X4),X3,X4),
inference(rename_variables,[],[i_0_35]) ).
cnf(i_0_678,plain,
equidistant(X1,extension(X2,X1,X3,X4),X3,X4),
inference(rename_variables,[],[i_0_35]) ).
cnf(i_0_682,plain,
equidistant(X1,extension(X2,X1,X3,X4),X3,X4),
inference(rename_variables,[],[i_0_35]) ).
cnf(i_0_686,plain,
equidistant(X1,extension(X2,X1,X3,X4),X3,X4),
inference(rename_variables,[],[i_0_35]) ).
cnf(i_0_690,plain,
equidistant(X1,extension(X2,X1,X3,X4),X3,X4),
inference(rename_variables,[],[i_0_35]) ).
cnf(i_0_694,plain,
equidistant(X1,extension(X2,X1,X3,X4),X3,X4),
inference(rename_variables,[],[i_0_35]) ).
cnf(i_0_698,plain,
equidistant(X1,extension(X2,X1,X3,X4),X3,X4),
inference(rename_variables,[],[i_0_35]) ).
cnf(i_0_702,plain,
equidistant(X1,extension(X2,X1,X3,X4),X3,X4),
inference(rename_variables,[],[i_0_35]) ).
cnf(i_0_706,plain,
equidistant(X1,extension(X2,X1,X3,X4),X3,X4),
inference(rename_variables,[],[i_0_35]) ).
cnf(i_0_710,plain,
equidistant(X1,extension(X2,X1,X3,X4),X3,X4),
inference(rename_variables,[],[i_0_35]) ).
cnf(i_0_714,plain,
equidistant(X1,extension(X2,X1,X3,X4),X3,X4),
inference(rename_variables,[],[i_0_35]) ).
cnf(i_0_718,plain,
equidistant(X1,extension(X2,X1,X3,X4),X3,X4),
inference(rename_variables,[],[i_0_35]) ).
cnf(i_0_722,plain,
equidistant(X1,extension(X2,X1,X3,X4),X3,X4),
inference(rename_variables,[],[i_0_35]) ).
cnf(i_0_726,plain,
equidistant(X1,extension(X2,X1,X3,X4),X3,X4),
inference(rename_variables,[],[i_0_35]) ).
cnf(i_0_730,plain,
equidistant(X1,extension(X2,X1,X3,X4),X3,X4),
inference(rename_variables,[],[i_0_35]) ).
cnf(i_0_734,plain,
equidistant(X1,extension(X2,X1,X3,X4),X3,X4),
inference(rename_variables,[],[i_0_35]) ).
cnf(i_0_738,plain,
equidistant(X1,extension(X2,X1,X3,X4),X3,X4),
inference(rename_variables,[],[i_0_35]) ).
cnf(i_0_742,plain,
equidistant(X1,extension(X2,X1,X3,X4),X3,X4),
inference(rename_variables,[],[i_0_35]) ).
cnf(i_0_746,plain,
equidistant(X1,extension(X2,X1,X3,X4),X3,X4),
inference(rename_variables,[],[i_0_35]) ).
cnf(i_0_750,plain,
equidistant(X1,extension(X2,X1,X3,X4),X3,X4),
inference(rename_variables,[],[i_0_35]) ).
cnf(i_0_754,plain,
equidistant(X1,extension(X2,X1,X3,X4),X3,X4),
inference(rename_variables,[],[i_0_35]) ).
cnf(i_0_758,plain,
equidistant(X1,extension(X2,X1,X3,X4),X3,X4),
inference(rename_variables,[],[i_0_35]) ).
cnf(i_0_762,plain,
equidistant(X1,extension(X2,X1,X3,X4),X3,X4),
inference(rename_variables,[],[i_0_35]) ).
cnf(i_0_766,plain,
equidistant(X1,extension(X2,X1,X3,X4),X3,X4),
inference(rename_variables,[],[i_0_35]) ).
cnf(i_0_770,plain,
equidistant(X1,extension(X2,X1,X3,X4),X3,X4),
inference(rename_variables,[],[i_0_35]) ).
cnf(i_0_774,plain,
equidistant(X1,extension(X2,X1,X3,X4),X3,X4),
inference(rename_variables,[],[i_0_35]) ).
cnf(i_0_778,plain,
equidistant(X1,extension(X2,X1,X3,X4),X3,X4),
inference(rename_variables,[],[i_0_35]) ).
cnf(i_0_782,plain,
equidistant(X1,extension(X2,X1,X3,X4),X3,X4),
inference(rename_variables,[],[i_0_35]) ).
cnf(i_0_786,plain,
equidistant(X1,extension(X2,X1,X3,X4),X3,X4),
inference(rename_variables,[],[i_0_35]) ).
cnf(i_0_790,plain,
equidistant(X1,extension(X2,X1,X3,X4),X3,X4),
inference(rename_variables,[],[i_0_35]) ).
cnf(i_0_794,plain,
equidistant(X1,extension(X2,X1,X3,X4),X3,X4),
inference(rename_variables,[],[i_0_35]) ).
cnf(i_0_798,plain,
equidistant(X1,extension(X2,X1,X3,X4),X3,X4),
inference(rename_variables,[],[i_0_35]) ).
cnf(i_0_802,plain,
equidistant(X1,extension(X2,X1,X3,X4),X3,X4),
inference(rename_variables,[],[i_0_35]) ).
cnf(i_0_806,plain,
equidistant(X1,extension(X2,X1,X3,X4),X3,X4),
inference(rename_variables,[],[i_0_35]) ).
cnf(i_0_810,plain,
equidistant(X1,extension(X2,X1,X3,X4),X3,X4),
inference(rename_variables,[],[i_0_35]) ).
cnf(i_0_814,plain,
equidistant(X1,extension(X2,X1,X3,X4),X3,X4),
inference(rename_variables,[],[i_0_35]) ).
cnf(i_0_818,plain,
equidistant(X1,extension(X2,X1,X3,X4),X3,X4),
inference(rename_variables,[],[i_0_35]) ).
cnf(i_0_822,plain,
equidistant(X1,extension(X2,X1,X3,X4),X3,X4),
inference(rename_variables,[],[i_0_35]) ).
cnf(i_0_826,plain,
equidistant(X1,extension(X2,X1,X3,X4),X3,X4),
inference(rename_variables,[],[i_0_35]) ).
cnf(i_0_830,plain,
equidistant(X1,extension(X2,X1,X3,X4),X3,X4),
inference(rename_variables,[],[i_0_35]) ).
cnf(i_0_834,plain,
equidistant(X1,extension(X2,X1,X3,X4),X3,X4),
inference(rename_variables,[],[i_0_35]) ).
cnf(i_0_838,plain,
equidistant(X1,extension(X2,X1,X3,X4),X3,X4),
inference(rename_variables,[],[i_0_35]) ).
cnf(i_0_842,plain,
equidistant(X1,extension(X2,X1,X3,X4),X3,X4),
inference(rename_variables,[],[i_0_35]) ).
cnf(i_0_846,plain,
equidistant(X1,extension(X2,X1,X3,X4),X3,X4),
inference(rename_variables,[],[i_0_35]) ).
cnf(i_0_850,plain,
equidistant(X1,extension(X2,X1,X3,X4),X3,X4),
inference(rename_variables,[],[i_0_35]) ).
cnf(i_0_854,plain,
equidistant(X1,extension(X2,X1,X3,X4),X3,X4),
inference(rename_variables,[],[i_0_35]) ).
cnf(i_0_858,plain,
equidistant(X1,extension(X2,X1,X3,X4),X3,X4),
inference(rename_variables,[],[i_0_35]) ).
cnf(i_0_862,plain,
equidistant(X1,extension(X2,X1,X3,X4),X3,X4),
inference(rename_variables,[],[i_0_35]) ).
cnf(i_0_866,plain,
equidistant(X1,extension(X2,X1,X3,X4),X3,X4),
inference(rename_variables,[],[i_0_35]) ).
cnf(i_0_870,plain,
equidistant(X1,extension(X2,X1,X3,X4),X3,X4),
inference(rename_variables,[],[i_0_35]) ).
cnf(i_0_874,plain,
equidistant(X1,extension(X2,X1,X3,X4),X3,X4),
inference(rename_variables,[],[i_0_35]) ).
cnf(i_0_878,plain,
equidistant(X1,extension(X2,X1,X3,X4),X3,X4),
inference(rename_variables,[],[i_0_35]) ).
cnf(i_0_882,plain,
equidistant(X1,extension(X2,X1,X3,X4),X3,X4),
inference(rename_variables,[],[i_0_35]) ).
cnf(i_0_886,plain,
equidistant(X1,extension(X2,X1,X3,X4),X3,X4),
inference(rename_variables,[],[i_0_35]) ).
cnf(i_0_890,plain,
equidistant(X1,extension(X2,X1,X3,X4),X3,X4),
inference(rename_variables,[],[i_0_35]) ).
cnf(i_0_894,plain,
equidistant(X1,extension(X2,X1,X3,X4),X3,X4),
inference(rename_variables,[],[i_0_35]) ).
cnf(i_0_898,plain,
equidistant(X1,extension(X2,X1,X3,X4),X3,X4),
inference(rename_variables,[],[i_0_35]) ).
cnf(i_0_902,plain,
equidistant(X1,extension(X2,X1,X3,X4),X3,X4),
inference(rename_variables,[],[i_0_35]) ).
cnf(i_0_906,plain,
equidistant(X1,extension(X2,X1,X3,X4),X3,X4),
inference(rename_variables,[],[i_0_35]) ).
cnf(i_0_910,plain,
equidistant(X1,extension(X2,X1,X3,X4),X3,X4),
inference(rename_variables,[],[i_0_35]) ).
cnf(i_0_914,plain,
equidistant(X1,extension(X2,X1,X3,X4),X3,X4),
inference(rename_variables,[],[i_0_35]) ).
cnf(i_0_918,plain,
equidistant(X1,extension(X2,X1,X3,X4),X3,X4),
inference(rename_variables,[],[i_0_35]) ).
cnf(i_0_922,plain,
equidistant(X1,extension(X2,X1,X3,X4),X3,X4),
inference(rename_variables,[],[i_0_35]) ).
cnf(i_0_926,plain,
equidistant(X1,extension(X2,X1,X3,X4),X3,X4),
inference(rename_variables,[],[i_0_35]) ).
cnf(i_0_930,plain,
equidistant(X1,extension(X2,X1,X3,X4),X3,X4),
inference(rename_variables,[],[i_0_35]) ).
cnf(i_0_942,plain,
equidistant(X1,X2,X2,X1),
inference(rename_variables,[],[i_0_39]) ).
cnf(i_0_964,plain,
equidistant(X1,extension(X2,X1,X3,X4),X3,X4),
inference(rename_variables,[],[i_0_35]) ).
cnf(i_0_965,plain,
equidistant(X1,extension(X2,X1,X3,X4),X3,X4),
inference(rename_variables,[],[i_0_35]) ).
cnf(i_0_966,plain,
equidistant(X1,extension(X2,X1,X3,X4),X3,X4),
inference(rename_variables,[],[i_0_35]) ).
cnf(i_0_998,plain,
equidistant(X1,X2,X2,X1),
inference(rename_variables,[],[i_0_39]) ).
cnf(i_0_999,plain,
equidistant(X1,X2,X2,X1),
inference(rename_variables,[],[i_0_39]) ).
cnf(i_0_1002,plain,
equidistant(X1,X2,X2,X1),
inference(rename_variables,[],[i_0_39]) ).
cnf(i_0_1003,plain,
equidistant(X1,X2,X2,X1),
inference(rename_variables,[],[i_0_39]) ).
cnf(i_0_1013,plain,
equidistant(X1,X2,X2,X1),
inference(rename_variables,[],[i_0_39]) ).
cnf(i_0_1057,plain,
between(X1,X2,extension(X1,X2,X3,X4)),
inference(rename_variables,[],[i_0_36]) ).
cnf(i_0_1059,plain,
equidistant(X1,X2,X2,X1),
inference(rename_variables,[],[i_0_39]) ).
cnf(i_0_1060,plain,
equidistant(X1,X2,X2,X1),
inference(rename_variables,[],[i_0_39]) ).
cnf(i_0_1062,plain,
between(X1,X2,extension(X1,X2,X3,X4)),
inference(rename_variables,[],[i_0_36]) ).
cnf(i_0_1071,plain,
equidistant(X1,X2,X2,X1),
inference(rename_variables,[],[i_0_39]) ).
cnf(i_0_1088,plain,
equidistant(X1,X2,X2,X1),
inference(rename_variables,[],[i_0_39]) ).
cnf(i_0_1112,plain,
equidistant(X1,X2,X2,X1),
inference(rename_variables,[],[i_0_39]) ).
cnf(i_0_1120,plain,
equidistant(X1,X2,X2,X1),
inference(rename_variables,[],[i_0_39]) ).
cnf(i_0_1129,plain,
equidistant(X1,extension(X2,X1,X3,X4),X3,X4),
inference(rename_variables,[],[i_0_35]) ).
cnf(i_0_1144,plain,
equidistant(X1,X2,X2,X1),
inference(rename_variables,[],[i_0_39]) ).
cnf(i_0_1156,plain,
equidistant(X1,X2,X2,X1),
inference(rename_variables,[],[i_0_39]) ).
cnf(i_0_1173,plain,
equidistant(X1,X2,X2,X1),
inference(rename_variables,[],[i_0_39]) ).
cnf(i_0_1181,plain,
equidistant(X1,X2,X2,X1),
inference(rename_variables,[],[i_0_39]) ).
cnf(i_0_1223,plain,
between(X1,X2,extension(X1,X2,X3,X4)),
inference(rename_variables,[],[i_0_36]) ).
cnf(i_0_1231,plain,
equidistant(X1,X2,X2,X1),
inference(rename_variables,[],[i_0_39]) ).
cnf(i_0_1239,plain,
equidistant(X1,X2,X2,X1),
inference(rename_variables,[],[i_0_39]) ).
cnf(i_0_1249,plain,
between(X1,X2,extension(X1,X2,X3,X4)),
inference(rename_variables,[],[i_0_36]) ).
cnf(i_0_1259,plain,
between(X1,X2,extension(X1,X2,X3,X4)),
inference(rename_variables,[],[i_0_36]) ).
cnf(i_0_1264,plain,
equidistant(X1,X2,X2,X1),
inference(rename_variables,[],[i_0_39]) ).
cnf(i_0_1267,plain,
equidistant(X1,X2,X2,X1),
inference(rename_variables,[],[i_0_39]) ).
cnf(i_0_1291,plain,
between(X1,X2,extension(X1,X2,X3,X4)),
inference(rename_variables,[],[i_0_36]) ).
cnf(i_0_1307,plain,
equidistant(X1,X2,X2,X1),
inference(rename_variables,[],[i_0_39]) ).
cnf(i_0_1316,plain,
equidistant(X1,X2,X2,X1),
inference(rename_variables,[],[i_0_39]) ).
cnf(i_0_1338,plain,
between(X1,X2,extension(X1,X2,X3,X4)),
inference(rename_variables,[],[i_0_36]) ).
cnf(c_0_68,axiom,
( equidistant(X1,X2,X3,X4)
| ~ equidistant(X5,X6,X1,X2)
| ~ equidistant(X5,X6,X3,X4) ),
i_0_34 ).
cnf(c_0_69,axiom,
equidistant(X1,extension(X2,X1,X3,X4),X3,X4),
i_0_35 ).
cnf(c_0_70,plain,
( equidistant(X1,X2,X3,X4)
| ~ equidistant(X5,extension(X6,X5,X3,X4),X1,X2) ),
inference(spm,[status(thm)],[c_0_68,c_0_69]) ).
cnf(c_0_71,axiom,
equidistant(X1,X2,X2,X1),
i_0_39 ).
cnf(c_0_72,plain,
~ equidistant(X1,v1,v,x),
i_0_63 ).
cnf(c_0_73,plain,
equidistant(extension(X1,X2,X3,X4),X2,X3,X4),
inference(spm,[status(thm)],[c_0_70,c_0_71]) ).
cnf(c_0_74,plain,
$false,
inference(spm,[status(thm)],[c_0_72,c_0_73]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : GEO031-2 : TPTP v9.2.1. Released v1.0.0.
% 0.00/0.12 % Command : /export/starexec/sandbox2/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox2/solver/bin/cse --final-prover /export/starexec/sandbox2/solver/bin/eprover --proof-time %d --global-time-limit %d
% 0.16/0.33 % Computer : n011.cluster.edu
% 0.16/0.33 % Model : x86_64 x86_64
% 0.16/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.33 % Memory : 8042.1875MB
% 0.16/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.16/0.33 % CPULimit : 300
% 0.16/0.33 % WCLimit : 300
% 0.16/0.33 % DateTime : Mon May 4 17:37:02 EDT 2026
% 0.16/0.33 % CPUTime :
% 0.16/0.34 % start to proof: theBenchmark
% 96.90/80.02 % Version : CSE_E---1.7
% 96.90/80.02 % Problem : theBenchmark.p
% 96.90/80.02 % SZS status Unsatisfiable for theBenchmark.p
% 96.90/80.02 % SZS output start CNFRefutation
% See solution above
% 98.90/82.03 % Total time : 79.668s
%------------------------------------------------------------------------------