%------------------------------------------------------------------------------
% File : CSE_E---1.7
% Problem : GEO028-3 : TPTP v9.2.1. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox/solver/bin/cse --final-prover /export/starexec/sandbox/solver/bin/eprover --proof-time %d --global-time-limit %d
% Computer : n028.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 133.11s 92.76s
% Output : CNFRefutation 138.43s
% Verified :
% SZS Type : ERROR: Analysing output (Could not find formula named c_0_42)
% Comments :
%------------------------------------------------------------------------------
cnf(r2_2,axiom,
equidistant(X1,reflection(X2,X1),X2,X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',r2_2) ).
cnf(reflection,axiom,
reflection(X1,X2) = extension(X1,X2,X1,X2),
file('/export/starexec/sandbox/benchmark/Axioms/GEO002-2.ax',reflection) ).
cnf(r2_1,axiom,
between(X1,X2,reflection(X1,X2)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',r2_1) ).
cnf(r4,axiom,
( X2 = X1
| X1 != reflection(X2,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',r4) ).
cnf(r3_1,axiom,
( X2 = reflection(X1,X2)
| X1 != X2 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',r3_1) ).
cnf(r3_2,axiom,
X1 = reflection(X1,X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',r3_2) ).
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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/benchmark/Axioms/GEO002-0.ax',upper_dimension) ).
cnf(d8,axiom,
( equidistant(X1,X5,X3,X6)
| ~ equidistant(X1,X2,X3,X4)
| ~ equidistant(X2,X5,X4,X6)
| ~ between(X1,X2,X5)
| ~ between(X3,X4,X6) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d8) ).
cnf(d5,axiom,
( equidistant(X1,X2,X5,X6)
| ~ equidistant(X1,X2,X3,X4)
| ~ equidistant(X3,X4,X5,X6) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d5) ).
cnf(transitivity_for_equidistance,axiom,
( equidistant(X3,X4,X5,X6)
| ~ equidistant(X1,X2,X3,X4)
| ~ equidistant(X1,X2,X5,X6) ),
file('/export/starexec/sandbox/benchmark/Axioms/GEO002-0.ax',transitivity_for_equidistance) ).
cnf(prove_equal_extensions,negated_conjecture,
extension(u,v,w,x) != extension(u,v,y,z),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_equal_extensions) ).
cnf(segment_construction2,axiom,
equidistant(X1,extension(X2,X1,X3,X4),X3,X4),
file('/export/starexec/sandbox/benchmark/Axioms/GEO002-0.ax',segment_construction2) ).
cnf(d4_1,axiom,
( equidistant(X1,X2,X4,X3)
| ~ equidistant(X1,X2,X3,X4) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d4_1) ).
cnf(d3,axiom,
( equidistant(X2,X1,X3,X4)
| ~ equidistant(X1,X2,X3,X4) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d3) ).
cnf(d4_2,axiom,
( equidistant(X2,X1,X4,X3)
| ~ equidistant(X1,X2,X3,X4) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d4_2) ).
cnf(d2,axiom,
( equidistant(X3,X4,X1,X2)
| ~ equidistant(X1,X2,X3,X4) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d2) ).
cnf(d4_3,axiom,
( equidistant(X3,X4,X2,X1)
| ~ equidistant(X1,X2,X3,X4) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d4_3) ).
cnf(d4_4,axiom,
( equidistant(X4,X3,X1,X2)
| ~ equidistant(X1,X2,X3,X4) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d4_4) ).
cnf(d4_5,axiom,
( equidistant(X4,X3,X2,X1)
| ~ equidistant(X1,X2,X3,X4) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d4_5) ).
cnf(d9,axiom,
( X1 = X2
| X3 = X4
| ~ between(X1,X2,X3)
| ~ between(X1,X2,X4)
| ~ equidistant(X2,X3,X2,X4) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d9) ).
cnf(segment_construction1,axiom,
between(X1,X2,extension(X1,X2,X3,X4)),
file('/export/starexec/sandbox/benchmark/Axioms/GEO002-0.ax',segment_construction1) ).
cnf(b0,axiom,
( between(X2,X3,X1)
| X1 != extension(X2,X3,X4,X5) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',b0) ).
cnf(identity_for_equidistance,axiom,
( X1 = X2
| ~ equidistant(X1,X2,X3,X3) ),
file('/export/starexec/sandbox/benchmark/Axioms/GEO002-0.ax',identity_for_equidistance) ).
cnf(e1,axiom,
X1 = extension(X2,X1,X3,X3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e1) ).
cnf(d7,axiom,
equidistant(X1,X1,X2,X2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d7) ).
cnf(d1,axiom,
equidistant(X1,X2,X1,X2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d1) ).
cnf(reflexivity_for_equidistance,axiom,
equidistant(X1,X2,X2,X1),
file('/export/starexec/sandbox/benchmark/Axioms/GEO002-0.ax',reflexivity_for_equidistance) ).
cnf(w_to_x_equals_y_to_z,hypothesis,
equidistant(w,x,y,z),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',w_to_x_equals_y_to_z) ).
cnf(identity_for_betweeness,axiom,
( X1 = X2
| ~ between(X1,X2,X1) ),
file('/export/starexec/sandbox/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/sandbox/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/sandbox/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/sandbox/benchmark/Axioms/GEO002-0.ax',lower_dimension1) ).
cnf(u_not_v,hypothesis,
u != v,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',u_not_v) ).
cnf(i_0_41,axiom,
equidistant(X1,reflection(X2,X1),X2,X1),
r2_2 ).
cnf(i_0_42,axiom,
reflection(X1,X2) = extension(X1,X2,X1,X2),
reflection ).
cnf(i_0_43,axiom,
between(X1,X2,reflection(X1,X2)),
r2_1 ).
cnf(i_0_44,axiom,
( X2 = X1
| X1 != reflection(X2,X1) ),
r4 ).
cnf(i_0_45,axiom,
( X2 = reflection(X1,X2)
| X1 != X2 ),
r3_1 ).
cnf(i_0_46,axiom,
X1 = reflection(X1,X1),
r3_2 ).
cnf(i_0_47,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_48,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_49,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_50,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_51,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_52,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_53,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_54,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_55,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_56,axiom,
( equidistant(X1,X5,X3,X6)
| ~ equidistant(X1,X2,X3,X4)
| ~ equidistant(X2,X5,X4,X6)
| ~ between(X1,X2,X5)
| ~ between(X3,X4,X6) ),
d8,
[final] ).
cnf(i_0_57,axiom,
( equidistant(X1,X2,X5,X6)
| ~ equidistant(X1,X2,X3,X4)
| ~ equidistant(X3,X4,X5,X6) ),
d5,
[final] ).
cnf(i_0_58,axiom,
( equidistant(X3,X4,X5,X6)
| ~ equidistant(X1,X2,X3,X4)
| ~ equidistant(X1,X2,X5,X6) ),
transitivity_for_equidistance,
[final] ).
cnf(i_0_59,negated_conjecture,
extension(u,v,w,x) != extension(u,v,y,z),
prove_equal_extensions,
[final] ).
cnf(i_0_60,plain,
equidistant(X1,extension(X2,X1,X2,X1),X2,X1),
inference(rw,[status(thm)],[i_0_41,c_0_42]),
[final] ).
cnf(i_0_61,axiom,
equidistant(X1,extension(X2,X1,X3,X4),X3,X4),
segment_construction2,
[final] ).
cnf(i_0_62,axiom,
( equidistant(X1,X2,X4,X3)
| ~ equidistant(X1,X2,X3,X4) ),
d4_1,
[final] ).
cnf(i_0_63,axiom,
( equidistant(X2,X1,X3,X4)
| ~ equidistant(X1,X2,X3,X4) ),
d3,
[final] ).
cnf(i_0_64,axiom,
( equidistant(X2,X1,X4,X3)
| ~ equidistant(X1,X2,X3,X4) ),
d4_2,
[final] ).
cnf(i_0_65,axiom,
( equidistant(X3,X4,X1,X2)
| ~ equidistant(X1,X2,X3,X4) ),
d2,
[final] ).
cnf(i_0_66,axiom,
( equidistant(X3,X4,X2,X1)
| ~ equidistant(X1,X2,X3,X4) ),
d4_3,
[final] ).
cnf(i_0_67,axiom,
( equidistant(X4,X3,X1,X2)
| ~ equidistant(X1,X2,X3,X4) ),
d4_4,
[final] ).
cnf(i_0_68,axiom,
( equidistant(X4,X3,X2,X1)
| ~ equidistant(X1,X2,X3,X4) ),
d4_5,
[final] ).
cnf(i_0_69,axiom,
( X1 = X2
| X3 = X4
| ~ between(X1,X2,X3)
| ~ between(X1,X2,X4)
| ~ equidistant(X2,X3,X2,X4) ),
d9,
[final] ).
cnf(i_0_70,plain,
between(X1,X2,extension(X1,X2,X1,X2)),
inference(rw,[status(thm)],[i_0_43,c_0_42]),
[final] ).
cnf(i_0_71,axiom,
between(X1,X2,extension(X1,X2,X3,X4)),
segment_construction1,
[final] ).
cnf(i_0_72,axiom,
( between(X2,X3,X1)
| X1 != extension(X2,X3,X4,X5) ),
b0,
[final] ).
cnf(i_0_73,plain,
( X1 = X2
| X1 != extension(X2,X1,X2,X1) ),
inference(rw,[status(thm)],[i_0_44,c_0_42]),
[final] ).
cnf(i_0_74,axiom,
( X1 = X2
| ~ equidistant(X1,X2,X3,X3) ),
identity_for_equidistance,
[final] ).
cnf(i_0_75,plain,
( X2 = extension(X1,X2,X1,X2)
| X1 != X2 ),
inference(rw,[status(thm)],[i_0_45,c_0_42]),
[final] ).
cnf(i_0_76,plain,
X1 = extension(X1,X1,X1,X1),
inference(rw,[status(thm)],[i_0_46,c_0_42]),
[final] ).
cnf(i_0_77,axiom,
X1 = extension(X2,X1,X3,X3),
e1,
[final] ).
cnf(i_0_78,axiom,
equidistant(X1,X1,X2,X2),
d7,
[final] ).
cnf(i_0_79,axiom,
equidistant(X1,X2,X1,X2),
d1,
[final] ).
cnf(i_0_80,axiom,
equidistant(X1,X2,X2,X1),
reflexivity_for_equidistance,
[final] ).
cnf(i_0_81,hypothesis,
equidistant(w,x,y,z),
w_to_x_equals_y_to_z,
[final] ).
cnf(i_0_82,axiom,
( X1 = X2
| ~ between(X1,X2,X1) ),
identity_for_betweeness,
[final] ).
cnf(i_0_83,axiom,
~ between(lower_dimension_point_3,lower_dimension_point_1,lower_dimension_point_2),
lower_dimension3,
[final] ).
cnf(i_0_84,axiom,
~ between(lower_dimension_point_2,lower_dimension_point_3,lower_dimension_point_1),
lower_dimension2,
[final] ).
cnf(i_0_85,axiom,
~ between(lower_dimension_point_1,lower_dimension_point_2,lower_dimension_point_3),
lower_dimension1,
[final] ).
cnf(i_0_86,hypothesis,
u != v,
u_not_v,
[final] ).
cnf(i_0_87,axiom,
X1 = X1 ).
cnf(i_0_88,axiom,
( X1 = X2
| X2 != X1 ) ).
cnf(i_0_89,axiom,
( X1 = X2
| X1 != X3
| X3 != X2 ) ).
cnf(i_0_90,axiom,
( X1 != X2
| extension(X1,X3,X4,X5) = extension(X2,X3,X4,X5) ) ).
cnf(i_0_91,axiom,
( X1 != X2
| extension(X3,X1,X4,X5) = extension(X3,X2,X4,X5) ) ).
cnf(i_0_92,axiom,
( X1 != X2
| extension(X3,X4,X1,X5) = extension(X3,X4,X2,X5) ) ).
cnf(i_0_93,axiom,
( X1 != X2
| extension(X3,X4,X5,X1) = extension(X3,X4,X5,X2) ) ).
cnf(i_0_94,axiom,
( X1 != X2
| ~ equidistant(X1,X3,X4,X5)
| equidistant(X2,X3,X4,X5) ) ).
cnf(i_0_95,axiom,
( X1 != X2
| ~ equidistant(X3,X1,X4,X5)
| equidistant(X3,X2,X4,X5) ) ).
cnf(i_0_96,axiom,
( X1 != X2
| ~ equidistant(X3,X4,X1,X5)
| equidistant(X3,X4,X2,X5) ) ).
cnf(i_0_97,axiom,
( X1 != X2
| ~ equidistant(X3,X4,X5,X1)
| equidistant(X3,X4,X5,X2) ) ).
cnf(i_0_98,axiom,
( X1 != X2
| ~ between(X1,X3,X4)
| between(X2,X3,X4) ) ).
cnf(i_0_99,axiom,
( X1 != X2
| ~ between(X3,X1,X4)
| between(X3,X2,X4) ) ).
cnf(i_0_100,axiom,
( X1 != X2
| ~ between(X3,X4,X1)
| between(X3,X4,X2) ) ).
cnf(i_0_3253,plain,
equidistant(extension(X1,X1,X1,X1),extension(X2,X1,X3,X1),X3,extension(X1,X1,X1,X1)),
inference(rename_variables,[],[i_0_1726]) ).
cnf(i_0_3255,plain,
extension(X1,u,X2,X2) != v,
inference(scs_inference,[],[i_0_59,i_0_136,i_0_151,i_0_86,i_0_1726,i_0_1003,i_0_3247,i_0_77,i_0_3245,i_0_3251,i_0_85,i_0_82,i_0_73,i_0_72,i_0_74,i_0_65,i_0_68,i_0_64,i_0_88,i_0_95,i_0_97,i_0_94,i_0_96,i_0_57,i_0_89]) ).
cnf(i_0_3257,plain,
between(extension(X1,X1,X1,X1),extension(X2,X1,X3,X3),extension(X1,X1,X1,X1)),
inference(scs_inference,[],[i_0_59,i_0_136,i_0_151,i_0_86,i_0_1726,i_0_1628,i_0_1003,i_0_3247,i_0_1020,i_0_77,i_0_3245,i_0_3251,i_0_85,i_0_82,i_0_73,i_0_72,i_0_74,i_0_65,i_0_68,i_0_64,i_0_88,i_0_95,i_0_97,i_0_94,i_0_96,i_0_57,i_0_89,i_0_98]) ).
cnf(i_0_3259,plain,
between(extension(X1,X2,X3,X3),extension(X1,X2,X3,X3),extension(X4,X2,X5,X5)),
inference(scs_inference,[],[i_0_59,i_0_136,i_0_151,i_0_86,i_0_1726,i_0_1628,i_0_1003,i_0_3247,i_0_3249,i_0_1020,i_0_77,i_0_3245,i_0_3251,i_0_85,i_0_82,i_0_73,i_0_72,i_0_74,i_0_65,i_0_68,i_0_64,i_0_88,i_0_95,i_0_97,i_0_94,i_0_96,i_0_57,i_0_89,i_0_98,i_0_100]) ).
cnf(i_0_3261,plain,
~ equidistant(X1,extension(X1,X1,X1,X1),extension(u,v,y,z),extension(u,v,w,x)),
inference(scs_inference,[],[i_0_59,i_0_136,i_0_151,i_0_86,i_0_1726,i_0_1628,i_0_1003,i_0_3247,i_0_3249,i_0_1020,i_0_77,i_0_3245,i_0_3251,i_0_85,i_0_82,i_0_73,i_0_72,i_0_74,i_0_65,i_0_68,i_0_64,i_0_88,i_0_95,i_0_97,i_0_94,i_0_96,i_0_57,i_0_89,i_0_98,i_0_100,i_0_62]) ).
cnf(i_0_3263,plain,
~ equidistant(extension(X1,X1,X1,X1),X1,extension(u,v,w,x),extension(u,v,y,z)),
inference(scs_inference,[],[i_0_59,i_0_136,i_0_151,i_0_86,i_0_1726,i_0_1628,i_0_1003,i_0_3247,i_0_3249,i_0_1020,i_0_77,i_0_3245,i_0_3251,i_0_85,i_0_82,i_0_73,i_0_72,i_0_74,i_0_65,i_0_68,i_0_64,i_0_88,i_0_95,i_0_97,i_0_94,i_0_96,i_0_57,i_0_89,i_0_98,i_0_100,i_0_62,i_0_63]) ).
cnf(i_0_3265,plain,
~ equidistant(extension(u,v,w,x),extension(u,v,y,z),extension(X1,X1,X1,X1),X1),
inference(scs_inference,[],[i_0_59,i_0_136,i_0_151,i_0_86,i_0_1726,i_0_1628,i_0_1003,i_0_3247,i_0_3249,i_0_1020,i_0_77,i_0_3245,i_0_3251,i_0_85,i_0_82,i_0_73,i_0_72,i_0_74,i_0_65,i_0_68,i_0_64,i_0_88,i_0_95,i_0_97,i_0_94,i_0_96,i_0_57,i_0_89,i_0_98,i_0_100,i_0_62,i_0_63,i_0_67]) ).
cnf(i_0_3267,plain,
~ equidistant(extension(u,v,y,z),extension(u,v,w,x),X1,extension(X1,X1,X1,X1)),
inference(scs_inference,[],[i_0_59,i_0_136,i_0_151,i_0_86,i_0_1726,i_0_1628,i_0_1003,i_0_3247,i_0_3249,i_0_1020,i_0_77,i_0_3245,i_0_3251,i_0_85,i_0_82,i_0_73,i_0_72,i_0_74,i_0_65,i_0_68,i_0_64,i_0_88,i_0_95,i_0_97,i_0_94,i_0_96,i_0_57,i_0_89,i_0_98,i_0_100,i_0_62,i_0_63,i_0_67,i_0_66]) ).
cnf(i_0_3273,plain,
between(X1,extension(X2,X2,X2,X2),extension(X3,X2,X4,X4)),
inference(rename_variables,[],[i_0_1720]) ).
cnf(i_0_4077,plain,
equidistant(X1,extension(X2,X2,X2,X2),extension(X2,X2,X2,X2),extension(X3,X2,X1,X2)),
inference(rename_variables,[],[i_0_1728]) ).
cnf(i_0_4118,plain,
equidistant(X1,extension(X2,X2,X2,X2),extension(X3,X2,X1,X2),extension(X2,X2,X2,X2)),
inference(rename_variables,[],[i_0_1732]) ).
cnf(i_0_1822,plain,
extension(extension(X1,X1,X1,X1),X1,X2,X2) = extension(X3,X1,X1,X1),
inference(scs_inference,[],[i_0_1630,i_0_1791,i_0_1266,i_0_1781,i_0_72,i_0_63,i_0_65,i_0_64,i_0_68,i_0_66,i_0_67,i_0_62,i_0_88]) ).
cnf(i_0_1844,plain,
equidistant(extension(X1,X2,X3,X2),extension(extension(X2,X2,X2,X2),X2,X4,X4),X3,X2),
inference(scs_inference,[],[i_0_1112,i_0_1832,i_0_1835,i_0_1630,i_0_1791,i_0_467,i_0_968,i_0_1828,i_0_118,i_0_479,i_0_104,i_0_985,i_0_701,i_0_281,i_0_1831,i_0_283,i_0_970,i_0_1266,i_0_1781,i_0_1720,i_0_71,i_0_72,i_0_63,i_0_65,i_0_64,i_0_68,i_0_66,i_0_67,i_0_62,i_0_88,i_0_58,i_0_57,i_0_98,i_0_99,i_0_100,i_0_69,i_0_56]) ).
cnf(i_0_1918,plain,
equidistant(X1,extension(X2,X1,extension(X3,X4,X5,X6),X4),X6,extension(X5,X5,X5,X5)),
inference(scs_inference,[],[i_0_1507,i_0_1775,i_0_1230,i_0_63,i_0_65,i_0_64,i_0_68,i_0_66,i_0_67,i_0_62]) ).
cnf(i_0_1920,plain,
equidistant(X1,X2,extension(X3,extension(X4,X4,X4,X4),X5,X5),extension(X6,X4,X1,X2)),
inference(scs_inference,[],[i_0_968,i_0_1227,i_0_1507,i_0_1775,i_0_1230,i_0_63,i_0_65,i_0_64,i_0_68,i_0_66,i_0_67,i_0_62,i_0_58]) ).
cnf(i_0_1923,plain,
equidistant(extension(X1,X2,extension(X3,X4,X5,X5),X4),extension(X2,X2,X2,X2),X6,X6),
inference(scs_inference,[],[i_0_968,i_0_255,i_0_1227,i_0_1507,i_0_1775,i_0_1230,i_0_63,i_0_65,i_0_64,i_0_68,i_0_66,i_0_67,i_0_62,i_0_58,i_0_57]) ).
cnf(i_0_2189,plain,
equidistant(X1,extension(X2,X2,X2,X2),extension(X2,X2,X2,X2),extension(X3,X2,X2,X1)),
inference(rename_variables,[],[i_0_1769]) ).
cnf(i_0_2259,plain,
equidistant(X1,extension(X2,X2,X2,X2),extension(X3,X2,X2,X1),extension(X2,X2,X2,X2)),
inference(rename_variables,[],[i_0_1773]) ).
cnf(i_0_2369,plain,
equidistant(extension(X1,X1,X1,X1),X2,extension(X3,X1,X1,X2),extension(X1,X1,X1,X1)),
inference(rename_variables,[],[i_0_1765]) ).
cnf(i_0_2375,plain,
between(X1,X2,extension(X3,extension(X2,X2,X2,X2),extension(X4,X4,X4,X4),X4)),
inference(rename_variables,[],[i_0_1761]) ).
cnf(i_0_2457,plain,
equidistant(extension(X1,extension(X2,X2,X2,X2),X3,X3),extension(X4,X2,X5,X6),X6,X5),
inference(scs_inference,[],[i_0_1778,i_0_65]) ).
cnf(i_0_2511,plain,
equidistant(extension(X1,X1,X1,X1),X2,extension(X1,X1,X1,X1),extension(X3,X1,X1,X2)),
inference(rename_variables,[],[i_0_1771]) ).
cnf(i_0_2862,plain,
equidistant(extension(X1,X1,X1,X1),X2,extension(X3,X1,X1,X2),extension(X1,X1,X1,X1)),
inference(rename_variables,[],[i_0_1765]) ).
cnf(i_0_2874,plain,
equidistant(extension(X1,X1,X1,X1),X2,extension(X3,X1,X1,X2),extension(X1,X1,X1,X1)),
inference(rename_variables,[],[i_0_1765]) ).
cnf(i_0_2894,plain,
equidistant(extension(X1,X1,X1,X1),X2,extension(X1,X1,X1,X1),extension(X3,X1,X1,X2)),
inference(rename_variables,[],[i_0_1771]) ).
cnf(i_0_2902,plain,
between(X1,X2,extension(X3,extension(X2,X2,X2,X2),extension(X4,X4,X4,X4),X4)),
inference(rename_variables,[],[i_0_1761]) ).
cnf(i_0_2906,plain,
equidistant(extension(X1,X1,X1,X1),X2,extension(X1,X1,X1,X1),extension(X3,X1,X1,X2)),
inference(rename_variables,[],[i_0_1771]) ).
cnf(i_0_2910,plain,
equidistant(extension(X1,X1,X1,X1),X2,extension(X1,X1,X1,X1),extension(X3,X1,X1,X2)),
inference(rename_variables,[],[i_0_1771]) ).
cnf(i_0_2974,plain,
between(X1,X2,extension(X3,extension(X2,X2,X2,X2),extension(X4,X4,X4,X4),X4)),
inference(rename_variables,[],[i_0_1761]) ).
cnf(i_0_3036,plain,
equidistant(extension(X1,X1,X1,X1),X2,extension(X3,X1,X1,X2),extension(X1,X1,X1,X1)),
inference(rename_variables,[],[i_0_1765]) ).
cnf(i_0_3048,plain,
equidistant(extension(X1,X1,X1,X1),extension(X2,X1,X1,X3),extension(X1,X1,X1,X1),X3),
inference(rename_variables,[],[i_0_1763]) ).
cnf(i_0_3073,plain,
equidistant(extension(X1,X1,X1,X1),X2,extension(X1,X1,X1,X1),extension(X3,X1,X1,X2)),
inference(rename_variables,[],[i_0_1771]) ).
cnf(i_0_3084,plain,
equidistant(extension(X1,X1,X1,X1),X2,extension(X1,X1,X1,X1),extension(X3,X1,X1,X2)),
inference(rename_variables,[],[i_0_1771]) ).
cnf(i_0_3088,plain,
equidistant(extension(X1,X1,X1,X1),X2,extension(X1,X1,X1,X1),extension(X3,X1,X1,X2)),
inference(rename_variables,[],[i_0_1771]) ).
cnf(i_0_3151,plain,
between(X1,X2,extension(X3,extension(X2,X2,X2,X2),extension(X4,X4,X4,X4),X4)),
inference(rename_variables,[],[i_0_1761]) ).
cnf(i_0_3217,plain,
between(X1,X2,extension(X3,extension(X2,X2,X2,X2),extension(X4,X4,X4,X4),X4)),
inference(rename_variables,[],[i_0_1761]) ).
cnf(i_0_3286,plain,
~ equidistant(extension(u,v,w,x),extension(u,v,y,z),X1,extension(X1,X1,X1,X1)),
inference(scs_inference,[],[i_0_3252,i_0_3243,i_0_504,i_0_671,i_0_83,i_0_82,i_0_73,i_0_72,i_0_74,i_0_65]) ).
cnf(i_0_3288,plain,
~ equidistant(extension(u,v,y,z),extension(u,v,w,x),extension(X1,X1,X1,X1),X1),
inference(scs_inference,[],[i_0_3252,i_0_3243,i_0_504,i_0_671,i_0_83,i_0_82,i_0_73,i_0_72,i_0_74,i_0_65,i_0_68]) ).
cnf(i_0_3290,plain,
~ equidistant(extension(X1,X1,X1,X1),X1,extension(u,v,y,z),extension(u,v,w,x)),
inference(scs_inference,[],[i_0_3252,i_0_3243,i_0_504,i_0_671,i_0_83,i_0_82,i_0_73,i_0_72,i_0_74,i_0_65,i_0_68,i_0_64]) ).
cnf(i_0_3310,plain,
~ equidistant(X1,extension(X1,X1,X1,X1),extension(u,v,y,z),extension(u,v,w,x)),
inference(rename_variables,[],[i_0_3261]) ).
cnf(i_0_3311,plain,
equidistant(extension(X1,X1,X1,X1),extension(X2,X1,X3,X1),X3,extension(X4,X1,X5,X5)),
inference(rename_variables,[],[i_0_3246]) ).
cnf(i_0_3314,plain,
equidistant(extension(X1,X1,X1,X1),extension(X2,X1,X3,X1),X3,extension(X4,X1,X5,X5)),
inference(rename_variables,[],[i_0_3246]) ).
cnf(i_0_3372,plain,
equidistant(extension(X1,X2,X3,X3),extension(X4,X2,X5,X2),X5,extension(X2,X2,X2,X2)),
inference(rename_variables,[],[i_0_3248]) ).
cnf(i_0_3907,plain,
equidistant(extension(X1,X1,X1,X1),extension(X2,X1,X3,X1),X3,extension(X4,X1,X5,X5)),
inference(rename_variables,[],[i_0_3246]) ).
cnf(i_0_4305,plain,
equidistant(extension(X1,X2,X3,X3),extension(X4,X2,X5,X2),X5,extension(X2,X2,X2,X2)),
inference(rename_variables,[],[i_0_3248]) ).
cnf(i_0_4503,plain,
equidistant(extension(X1,X1,X1,X1),extension(X2,X1,X3,X1),X3,extension(X4,X1,X5,X5)),
inference(rename_variables,[],[i_0_3246]) ).
cnf(i_0_1892,plain,
equidistant(extension(X1,X2,X3,X4),X2,X4,extension(X5,X3,X2,X2)),
inference(scs_inference,[],[i_0_1158,i_0_1885,i_0_1888,i_0_1839,i_0_467,i_0_962,i_0_1881,i_0_253,i_0_985,i_0_1008,i_0_324,i_0_1884,i_0_898,i_0_970,i_0_1460,i_0_1823,i_0_63,i_0_65,i_0_64,i_0_68,i_0_66,i_0_67,i_0_62,i_0_88,i_0_58,i_0_57,i_0_98,i_0_99,i_0_100,i_0_56]) ).
cnf(i_0_1965,plain,
equidistant(X1,X2,extension(X3,X3,X3,X3),extension(X4,X3,extension(X5,X3,X2,X1),X3)),
inference(scs_inference,[],[i_0_962,i_0_1936,i_0_1728,i_0_63,i_0_65,i_0_64,i_0_68,i_0_66,i_0_67,i_0_62,i_0_58]) ).
cnf(i_0_1968,plain,
equidistant(extension(X1,X2,X3,extension(X4,X3,X5,X5)),extension(X2,X2,X2,X2),X6,X6),
inference(scs_inference,[],[i_0_962,i_0_255,i_0_1936,i_0_1728,i_0_63,i_0_65,i_0_64,i_0_68,i_0_66,i_0_67,i_0_62,i_0_58,i_0_57]) ).
cnf(i_0_1981,plain,
equidistant(extension(X1,X2,X2,X3),X2,X3,extension(X4,X2,X5,X5)),
inference(scs_inference,[],[i_0_1158,i_0_1974,i_0_1977,i_0_467,i_0_962,i_0_1970,i_0_253,i_0_255,i_0_1234,i_0_494,i_0_1084,i_0_279,i_0_1936,i_0_1728,i_0_63,i_0_65,i_0_64,i_0_68,i_0_66,i_0_67,i_0_62,i_0_58,i_0_57,i_0_98,i_0_99,i_0_100,i_0_56]) ).
cnf(i_0_2089,plain,
equidistant(X1,extension(X2,X1,extension(X3,X4,X5,X6),X4),X6,extension(X5,X5,X5,X5)),
inference(rename_variables,[],[i_0_1918]) ).
cnf(i_0_2459,plain,
equidistant(extension(X1,X1,X1,X1),extension(X2,X1,extension(X3,X4,X5,X5),X4),X6,X6),
inference(scs_inference,[],[i_0_1778,i_0_1923,i_0_65,i_0_63]) ).
cnf(i_0_2461,plain,
equidistant(extension(X1,X1,X1,X1),extension(X2,X1,extension(X3,X4,X5,X6),X4),X6,X5),
inference(scs_inference,[],[i_0_1699,i_0_1778,i_0_1923,i_0_65,i_0_63,i_0_64]) ).
cnf(i_0_2463,plain,
equidistant(X1,X2,extension(X3,X3,X3,X3),extension(X4,X3,extension(X5,X6,X2,X1),X6)),
inference(scs_inference,[],[i_0_1699,i_0_1778,i_0_1923,i_0_65,i_0_63,i_0_64,i_0_68]) ).
cnf(i_0_2465,plain,
equidistant(X1,X2,extension(X3,X4,extension(X5,X6,X2,X1),X6),extension(X4,X4,X4,X4)),
inference(scs_inference,[],[i_0_1699,i_0_1778,i_0_1923,i_0_65,i_0_63,i_0_64,i_0_68,i_0_67]) ).
cnf(i_0_2467,plain,
equidistant(extension(X1,extension(X2,X2,X2,X2),X3,X3),extension(X4,X2,X5,X6),X5,X6),
inference(scs_inference,[],[i_0_1699,i_0_1778,i_0_1923,i_0_65,i_0_63,i_0_64,i_0_68,i_0_67,i_0_66]) ).
cnf(i_0_2010,plain,
equidistant(X1,X1,extension(X2,X2,X2,X2),extension(X3,X2,X2,X2)),
inference(scs_inference,[],[i_0_815,i_0_1820,i_0_1916,i_0_1892,i_0_63,i_0_65,i_0_64,i_0_68,i_0_66,i_0_67,i_0_62,i_0_58]) ).
cnf(i_0_2011,plain,
equidistant(extension(X1,X2,X3,X4),X2,X4,extension(X5,X3,X2,X2)),
inference(rename_variables,[],[i_0_1892]) ).
cnf(i_0_2082,plain,
equidistant(extension(X1,X2,X2,X3),X2,X3,extension(X4,X2,X5,X5)),
inference(rename_variables,[],[i_0_1981]) ).
cnf(i_0_4580,plain,
equidistant(extension(X1,X2,X3,X4),X2,X4,extension(X5,X3,X2,X2)),
inference(rename_variables,[],[i_0_1892]) ).
cnf(i_0_4665,plain,
equidistant(extension(X1,X2,X2,X3),X2,X3,extension(X4,X2,X5,X5)),
inference(rename_variables,[],[i_0_1981]) ).
cnf(i_0_2046,plain,
equidistant(X1,X1,extension(X2,X3,X4,X4),extension(X3,X3,X3,X3)),
inference(scs_inference,[],[i_0_854,i_0_1078,i_0_2017,i_0_63,i_0_65,i_0_64,i_0_68,i_0_66,i_0_67,i_0_62,i_0_58]) ).
cnf(i_0_2049,plain,
equidistant(extension(X1,X2,X3,X3),extension(X2,X2,X2,X2),X4,X4),
inference(scs_inference,[],[i_0_968,i_0_854,i_0_1078,i_0_78,i_0_2017,i_0_63,i_0_65,i_0_64,i_0_68,i_0_66,i_0_67,i_0_62,i_0_58,i_0_57]) ).
cnf(i_0_2069,plain,
equidistant(extension(X1,X1,X1,X1),extension(X2,X1,X1,X1),X3,X3),
inference(scs_inference,[],[i_0_2010,i_0_2053,i_0_63,i_0_65]) ).
cnf(i_0_2081,plain,
equidistant(X1,X1,extension(X2,X2,X2,X2),extension(X3,X2,X4,X4)),
inference(scs_inference,[],[i_0_815,i_0_2010,i_0_1908,i_0_2053,i_0_1981,i_0_63,i_0_65,i_0_64,i_0_68,i_0_66,i_0_67,i_0_62,i_0_58]) ).
cnf(i_0_2084,plain,
equidistant(extension(X1,X2,X3,extension(X4,X5,X6,X6)),extension(X2,X2,X2,X2),X3,X5),
inference(scs_inference,[],[i_0_968,i_0_815,i_0_1138,i_0_2010,i_0_1908,i_0_2053,i_0_1981,i_0_63,i_0_65,i_0_64,i_0_68,i_0_66,i_0_67,i_0_62,i_0_58,i_0_57]) ).
cnf(i_0_3533,plain,
equidistant(X1,X1,extension(X2,X3,X4,X4),extension(X3,X3,X3,X3)),
inference(rename_variables,[],[i_0_2046]) ).
cnf(i_0_2116,plain,
equidistant(X1,X2,extension(X3,X3,X3,X3),extension(X4,extension(X5,X3,X1,X2),X6,X6)),
inference(scs_inference,[],[i_0_968,i_0_2088,i_0_1491,i_0_65,i_0_63,i_0_64,i_0_68,i_0_66,i_0_67,i_0_62,i_0_58]) ).
cnf(i_0_2119,plain,
equidistant(extension(X1,X2,X3,X4),extension(X2,X2,X2,X2),X3,extension(X5,X4,X6,X6)),
inference(scs_inference,[],[i_0_968,i_0_1187,i_0_2088,i_0_1491,i_0_65,i_0_63,i_0_64,i_0_68,i_0_66,i_0_67,i_0_62,i_0_58,i_0_57]) ).
cnf(i_0_2139,plain,
equidistant(extension(X1,X1,X1,X1),extension(X2,X1,X3,X3),X4,X4),
inference(scs_inference,[],[i_0_2071,i_0_2049,i_0_65,i_0_63]) ).
cnf(i_0_2145,plain,
equidistant(X1,extension(X2,X1,X3,X3),X4,extension(extension(X5,X4,X1,X1),X4,X6,X6)),
inference(scs_inference,[],[i_0_2071,i_0_2075,i_0_2049,i_0_1317,i_0_65,i_0_63,i_0_64,i_0_68,i_0_66]) ).
cnf(i_0_2147,plain,
equidistant(extension(X1,X1,X1,X1),extension(X2,X1,extension(X3,X4,X5,X6),X4),X5,X6),
inference(scs_inference,[],[i_0_2071,i_0_2075,i_0_2049,i_0_1056,i_0_1317,i_0_65,i_0_63,i_0_64,i_0_68,i_0_66,i_0_67]) ).
cnf(i_0_2149,plain,
equidistant(extension(extension(X1,X2,X3,X3),X2,X4,X4),X2,extension(X5,X3,X6,X6),X3),
inference(scs_inference,[],[i_0_2071,i_0_2075,i_0_2049,i_0_1056,i_0_1317,i_0_65,i_0_63,i_0_64,i_0_68,i_0_66,i_0_67,i_0_62]) ).
cnf(i_0_2151,plain,
equidistant(X1,X2,extension(X3,X4,extension(X5,X4,X2,X1),X4),extension(X4,X4,X4,X4)),
inference(scs_inference,[],[i_0_962,i_0_1732,i_0_2071,i_0_2075,i_0_2049,i_0_1056,i_0_1317,i_0_65,i_0_63,i_0_64,i_0_68,i_0_66,i_0_67,i_0_62,i_0_58]) ).
cnf(i_0_3587,plain,
equidistant(X1,X1,extension(X2,X2,X2,X2),extension(X3,X2,X4,X4)),
inference(rename_variables,[],[i_0_2081]) ).
cnf(i_0_2188,plain,
equidistant(X1,X2,extension(X3,X3,X3,X3),extension(X4,X3,X3,extension(X5,X3,X2,X1))),
inference(scs_inference,[],[i_0_962,i_0_2158,i_0_1769,i_0_65,i_0_63,i_0_64,i_0_68,i_0_66,i_0_67,i_0_62,i_0_58]) ).
cnf(i_0_2191,plain,
equidistant(extension(X1,X2,extension(X3,X4,X5,X5),X6),extension(X2,X2,X2,X2),X6,X4),
inference(scs_inference,[],[i_0_962,i_0_1138,i_0_2158,i_0_1769,i_0_65,i_0_63,i_0_64,i_0_68,i_0_66,i_0_67,i_0_62,i_0_58,i_0_57]) ).
cnf(i_0_2288,plain,
equidistant(extension(X1,X1,X1,X1),extension(X2,X1,extension(X3,X1,X4,X5),X1),X5,X4),
inference(scs_inference,[],[i_0_2151,i_0_1092,i_0_1552,i_0_1651,i_0_1734,i_0_65,i_0_63,i_0_64,i_0_68,i_0_66,i_0_67]) ).
cnf(i_0_2290,plain,
equidistant(extension(X1,X2,X3,extension(X4,X5,X6,X6)),extension(X2,X2,X2,X2),X5,X3),
inference(scs_inference,[],[i_0_2151,i_0_1092,i_0_1552,i_0_1651,i_0_1734,i_0_2084,i_0_65,i_0_63,i_0_64,i_0_68,i_0_66,i_0_67,i_0_62]) ).
cnf(i_0_2292,plain,
equidistant(X1,X1,X2,extension(X3,X2,extension(X4,X4,X4,X4),X4)),
inference(scs_inference,[],[i_0_968,i_0_2151,i_0_1092,i_0_1552,i_0_1651,i_0_1734,i_0_2084,i_0_1080,i_0_65,i_0_63,i_0_64,i_0_68,i_0_66,i_0_67,i_0_62,i_0_58]) ).
cnf(i_0_3409,plain,
equidistant(extension(X1,X2,X3,X4),extension(X2,X2,X2,X2),X3,extension(X5,X4,X6,X6)),
inference(rename_variables,[],[i_0_2119]) ).
cnf(i_0_3617,plain,
equidistant(extension(X1,X1,X1,X1),extension(X2,X1,X3,X3),X4,X4),
inference(rename_variables,[],[i_0_2139]) ).
cnf(i_0_3621,plain,
equidistant(extension(X1,X1,X1,X1),extension(X2,X1,X3,X3),X4,X4),
inference(rename_variables,[],[i_0_2139]) ).
cnf(i_0_3626,plain,
equidistant(extension(X1,X1,X1,X1),extension(X2,X1,X3,X3),X4,X4),
inference(rename_variables,[],[i_0_2139]) ).
cnf(i_0_3994,plain,
equidistant(extension(X1,X2,X3,X4),extension(X2,X2,X2,X2),X3,extension(X5,X4,X6,X6)),
inference(rename_variables,[],[i_0_2119]) ).
cnf(i_0_4632,plain,
equidistant(extension(X1,X2,X3,X4),extension(X2,X2,X2,X2),X3,extension(X5,X4,X6,X6)),
inference(rename_variables,[],[i_0_2119]) ).
cnf(i_0_2223,plain,
equidistant(X1,X2,extension(X3,extension(X4,X5,X1,X2),X6,X6),extension(X5,X5,X5,X5)),
inference(scs_inference,[],[i_0_968,i_0_2195,i_0_1495,i_0_65,i_0_63,i_0_64,i_0_68,i_0_66,i_0_67,i_0_62,i_0_58]) ).
cnf(i_0_2329,plain,
equidistant(X1,X1,extension(X2,X3,extension(X4,X4,X4,X4),X4),X3),
inference(scs_inference,[],[i_0_968,i_0_2296,i_0_1086,i_0_65,i_0_63,i_0_64,i_0_68,i_0_67,i_0_66,i_0_62,i_0_58]) ).
cnf(i_0_2337,plain,
equidistant(X1,X1,X2,extension(X3,X2,extension(X4,X4,X4,X4),X4)),
inference(rename_variables,[],[i_0_2292]) ).
cnf(i_0_2469,plain,
equidistant(extension(X1,X2,extension(X3,X4,X5,X5),X6),extension(X2,X2,X2,X2),X4,X6),
inference(scs_inference,[],[i_0_1699,i_0_1778,i_0_1923,i_0_2191,i_0_65,i_0_63,i_0_64,i_0_68,i_0_67,i_0_66,i_0_62]) ).
cnf(i_0_2471,plain,
equidistant(X1,X2,extension(X3,X4,X5,extension(X6,X5,X2,X1)),X4),
inference(scs_inference,[],[i_0_962,i_0_1010,i_0_1699,i_0_1778,i_0_1923,i_0_2191,i_0_65,i_0_63,i_0_64,i_0_68,i_0_67,i_0_66,i_0_62,i_0_58]) ).
cnf(i_0_3079,plain,
equidistant(X1,X1,X2,extension(X3,X2,extension(X4,X4,X4,X4),X4)),
inference(rename_variables,[],[i_0_2292]) ).
cnf(i_0_2258,plain,
equidistant(X1,X2,extension(X3,X4,X4,extension(X5,X4,X2,X1)),extension(X4,X4,X4,X4)),
inference(scs_inference,[],[i_0_962,i_0_1773,i_0_2226,i_0_65,i_0_63,i_0_64,i_0_68,i_0_66,i_0_67,i_0_62,i_0_58]) ).
cnf(i_0_2261,plain,
equidistant(extension(X1,X2,X3,X4),extension(X2,X2,X2,X2),X4,extension(X5,X3,X6,X6)),
inference(scs_inference,[],[i_0_962,i_0_1187,i_0_1773,i_0_2226,i_0_65,i_0_63,i_0_64,i_0_68,i_0_66,i_0_67,i_0_62,i_0_58,i_0_57]) ).
cnf(i_0_2365,plain,
equidistant(X1,X2,X3,extension(X4,X3,extension(X5,X6,X1,X2),X6)),
inference(scs_inference,[],[i_0_968,i_0_2333,i_0_1088,i_0_65,i_0_63,i_0_64,i_0_68,i_0_67,i_0_66,i_0_62,i_0_58]) ).
cnf(i_0_2507,plain,
equidistant(X1,X2,X3,extension(X4,X3,X5,extension(X6,X5,X2,X1))),
inference(scs_inference,[],[i_0_962,i_0_2474,i_0_1016,i_0_65,i_0_63,i_0_64,i_0_68,i_0_67,i_0_66,i_0_62,i_0_58]) ).
cnf(i_0_2401,plain,
equidistant(X1,X2,X1,extension(X3,X2,extension(X4,X4,X4,X4),X4)),
inference(scs_inference,[],[i_0_968,i_0_2368,i_0_2336,i_0_65,i_0_63,i_0_64,i_0_68,i_0_67,i_0_66,i_0_62,i_0_58]) ).
cnf(i_0_2408,plain,
equidistant(extension(X1,X2,X3,X3),X2,X3,extension(X4,X3,X5,extension(X6,X5,X2,X2))),
inference(scs_inference,[],[i_0_467,i_0_968,i_0_2406,i_0_1008,i_0_2368,i_0_2336,i_0_1044,i_0_1580,i_0_65,i_0_63,i_0_64,i_0_68,i_0_67,i_0_66,i_0_62,i_0_58,i_0_57,i_0_56]) ).
cnf(i_0_2543,plain,
equidistant(X1,X2,extension(X3,X4,extension(X5,X6,X2,X1),X6),X4),
inference(scs_inference,[],[i_0_962,i_0_2510,i_0_1082,i_0_65,i_0_63,i_0_64,i_0_68,i_0_67,i_0_66,i_0_62,i_0_58]) ).
cnf(i_0_3669,plain,
equidistant(extension(X1,X2,X3,X4),extension(X2,X2,X2,X2),X4,extension(X5,X3,X6,X6)),
inference(rename_variables,[],[i_0_2261]) ).
cnf(i_0_4218,plain,
equidistant(extension(X1,X2,X3,X4),extension(X2,X2,X2,X2),X4,extension(X5,X3,X6,X6)),
inference(rename_variables,[],[i_0_2261]) ).
cnf(i_0_4685,plain,
equidistant(extension(X1,X2,X3,X4),extension(X2,X2,X2,X2),X4,extension(X5,X3,X6,X6)),
inference(rename_variables,[],[i_0_2261]) ).
cnf(i_0_2440,plain,
equidistant(extension(X1,X2,X3,X4),extension(X2,X2,X2,X2),extension(X5,X4,X6,X6),X3),
inference(scs_inference,[],[i_0_968,i_0_1227,i_0_2404,i_0_779,i_0_65,i_0_63,i_0_64,i_0_68,i_0_67,i_0_66,i_0_62,i_0_58,i_0_57]) ).
cnf(i_0_2443,plain,
equidistant(extension(X1,X2,X3,X4),X2,X3,extension(X5,X4,extension(X2,X2,X2,X2),X2)),
inference(scs_inference,[],[i_0_467,i_0_968,i_0_1227,i_0_297,i_0_2404,i_0_779,i_0_110,i_0_65,i_0_63,i_0_64,i_0_68,i_0_67,i_0_66,i_0_62,i_0_58,i_0_57,i_0_56]) ).
cnf(i_0_2612,plain,
equidistant(X1,X2,X3,extension(X4,extension(X3,X3,X3,X3),X2,X1)),
inference(scs_inference,[],[i_0_962,i_0_2549,i_0_1548,i_0_65,i_0_63,i_0_64,i_0_68,i_0_67,i_0_66,i_0_62,i_0_58]) ).
cnf(i_0_2478,plain,
equidistant(extension(X1,X2,X2,X3),X2,X3,extension(X4,X2,extension(X2,X2,X2,X2),X2)),
inference(scs_inference,[],[i_0_467,i_0_962,i_0_2476,i_0_1730,i_0_297,i_0_1010,i_0_1699,i_0_1778,i_0_1923,i_0_2191,i_0_2443,i_0_65,i_0_63,i_0_64,i_0_68,i_0_67,i_0_66,i_0_62,i_0_58,i_0_57,i_0_56]) ).
cnf(i_0_2479,plain,
equidistant(extension(X1,X2,X3,X4),X2,X3,extension(X5,X4,extension(X2,X2,X2,X2),X2)),
inference(rename_variables,[],[i_0_2443]) ).
cnf(i_0_2648,plain,
equidistant(X1,X2,X2,extension(X3,extension(X1,X1,X1,X1),X4,X4)),
inference(scs_inference,[],[i_0_825,i_0_2616,i_0_2600,i_0_65,i_0_63,i_0_64,i_0_68,i_0_67,i_0_66,i_0_62,i_0_58]) ).
cnf(i_0_2657,plain,
equidistant(X1,X2,X3,extension(X4,extension(X3,X3,X3,X3),X2,X1)),
inference(rename_variables,[],[i_0_2612]) ).
cnf(i_0_3415,plain,
equidistant(extension(X1,X2,X3,X4),extension(X2,X2,X2,X2),extension(X5,X4,X6,X6),X3),
inference(rename_variables,[],[i_0_2440]) ).
cnf(i_0_4387,plain,
equidistant(extension(X1,X2,X3,X4),extension(X2,X2,X2,X2),extension(X5,X4,X6,X6),X3),
inference(rename_variables,[],[i_0_2440]) ).
cnf(i_0_2578,plain,
equidistant(X1,X1,extension(X2,X2,X2,X2),extension(X3,X2,extension(X2,X2,X2,X2),X2)),
inference(scs_inference,[],[i_0_815,i_0_2546,i_0_2478,i_0_65,i_0_63,i_0_64,i_0_68,i_0_67,i_0_66,i_0_62,i_0_58]) ).
cnf(i_0_2579,plain,
equidistant(extension(X1,X2,X2,X3),X2,X3,extension(X4,X2,extension(X2,X2,X2,X2),X2)),
inference(rename_variables,[],[i_0_2478]) ).
cnf(i_0_2685,plain,
equidistant(X1,extension(X2,X2,X2,X2),extension(X3,X2,X4,X4),X1),
inference(scs_inference,[],[i_0_930,i_0_2602,i_0_2619,i_0_65,i_0_63,i_0_64,i_0_68,i_0_67,i_0_66,i_0_62,i_0_58]) ).
cnf(i_0_2689,plain,
equidistant(extension(X1,X2,X3,X4),extension(X2,X2,X2,X2),extension(X5,X3,X6,X6),X4),
inference(scs_inference,[],[i_0_962,i_0_930,i_0_1227,i_0_2602,i_0_2619,i_0_65,i_0_63,i_0_64,i_0_68,i_0_67,i_0_66,i_0_62,i_0_58,i_0_57]) ).
cnf(i_0_2725,plain,
equidistant(extension(X1,X2,w,x),extension(X2,X2,X2,X2),y,z),
inference(scs_inference,[],[i_0_968,i_0_2723,i_0_81,i_0_2692,i_0_2606,i_0_65,i_0_63,i_0_64,i_0_68,i_0_67,i_0_66,i_0_62,i_0_58,i_0_57]) ).
cnf(i_0_2758,plain,
equidistant(X1,extension(X2,X2,X2,X2),extension(X3,X2,X4,X4),X1),
inference(rename_variables,[],[i_0_2685]) ).
cnf(i_0_3584,plain,
equidistant(extension(X1,X2,X3,X4),extension(X2,X2,X2,X2),extension(X5,X3,X6,X6),X4),
inference(rename_variables,[],[i_0_2689]) ).
cnf(i_0_4447,plain,
equidistant(extension(X1,X2,X3,X4),extension(X2,X2,X2,X2),extension(X5,X3,X6,X6),X4),
inference(rename_variables,[],[i_0_2689]) ).
cnf(i_0_4855,plain,
equidistant(X1,extension(X2,X2,X2,X2),extension(X3,X2,X4,X4),X1),
inference(rename_variables,[],[i_0_2685]) ).
cnf(i_0_4859,plain,
equidistant(X1,extension(X2,X2,X2,X2),extension(X3,X2,X4,X4),X1),
inference(rename_variables,[],[i_0_2685]) ).
cnf(i_0_2757,plain,
equidistant(X1,X2,extension(X3,X4,X5,X5),extension(X6,X4,X1,X2)),
inference(scs_inference,[],[i_0_968,i_0_2721,i_0_2581,i_0_2652,i_0_2685,i_0_65,i_0_63,i_0_64,i_0_68,i_0_67,i_0_66,i_0_62,i_0_58]) ).
cnf(i_0_2966,plain,
equidistant(X1,X2,extension(X3,X4,X5,X5),extension(X6,X4,X1,X2)),
inference(rename_variables,[],[i_0_2757]) ).
cnf(i_0_3269,plain,
~ equidistant(extension(X1,X2,X3,X3),extension(X2,X2,X2,X2),extension(u,v,w,x),extension(u,v,y,z)),
inference(scs_inference,[],[i_0_59,i_0_136,i_0_151,i_0_86,i_0_1726,i_0_1628,i_0_2753,i_0_1003,i_0_3247,i_0_3249,i_0_1020,i_0_77,i_0_3245,i_0_3251,i_0_85,i_0_82,i_0_73,i_0_72,i_0_74,i_0_65,i_0_68,i_0_64,i_0_88,i_0_95,i_0_97,i_0_94,i_0_96,i_0_57,i_0_89,i_0_98,i_0_100,i_0_62,i_0_63,i_0_67,i_0_66,i_0_58]) ).
cnf(i_0_3272,plain,
between(X1,extension(X2,X3,X4,X4),extension(X5,X3,X6,X6)),
inference(scs_inference,[],[i_0_59,i_0_136,i_0_151,i_0_86,i_0_1726,i_0_1628,i_0_2753,i_0_1003,i_0_3247,i_0_3249,i_0_3260,i_0_1020,i_0_77,i_0_3245,i_0_3251,i_0_1720,i_0_85,i_0_82,i_0_73,i_0_72,i_0_74,i_0_65,i_0_68,i_0_64,i_0_88,i_0_95,i_0_97,i_0_94,i_0_96,i_0_57,i_0_89,i_0_98,i_0_100,i_0_62,i_0_63,i_0_67,i_0_66,i_0_58,i_0_99]) ).
cnf(i_0_4083,plain,
equidistant(X1,X2,extension(X3,X4,X5,X5),extension(X6,X4,X1,X2)),
inference(rename_variables,[],[i_0_2757]) ).
cnf(i_0_4084,plain,
equidistant(X1,X2,extension(X3,X4,X5,X5),extension(X6,X4,X1,X2)),
inference(rename_variables,[],[i_0_2757]) ).
cnf(i_0_2825,plain,
equidistant(extension(X1,X1,X1,X1),extension(X2,X1,X1,X1),extension(X3,X1,X4,X4),X1),
inference(scs_inference,[],[i_0_1730,i_0_1078,i_0_2792,i_0_65,i_0_64,i_0_68,i_0_63,i_0_62,i_0_67,i_0_66,i_0_58]) ).
cnf(i_0_3292,plain,
~ equidistant(extension(X1,X2,X3,X3),extension(X2,X2,X2,X2),extension(u,v,y,z),extension(u,v,w,x)),
inference(scs_inference,[],[i_0_3252,i_0_3269,i_0_3243,i_0_504,i_0_671,i_0_83,i_0_82,i_0_73,i_0_72,i_0_74,i_0_65,i_0_68,i_0_64,i_0_62]) ).
cnf(i_0_3294,plain,
~ equidistant(extension(X1,X1,X1,X1),extension(X2,X1,X3,X3),extension(u,v,w,x),extension(u,v,y,z)),
inference(scs_inference,[],[i_0_3252,i_0_3269,i_0_3243,i_0_504,i_0_671,i_0_83,i_0_82,i_0_73,i_0_72,i_0_74,i_0_65,i_0_68,i_0_64,i_0_62,i_0_63]) ).
cnf(i_0_3296,plain,
~ equidistant(extension(u,v,w,x),extension(u,v,y,z),extension(X1,X1,X1,X1),extension(X2,X1,X3,X3)),
inference(scs_inference,[],[i_0_3252,i_0_3269,i_0_3243,i_0_504,i_0_671,i_0_83,i_0_82,i_0_73,i_0_72,i_0_74,i_0_65,i_0_68,i_0_64,i_0_62,i_0_63,i_0_67]) ).
cnf(i_0_3298,plain,
~ equidistant(extension(u,v,y,z),extension(u,v,w,x),extension(X1,X2,X3,X3),extension(X2,X2,X2,X2)),
inference(scs_inference,[],[i_0_3252,i_0_3269,i_0_3243,i_0_504,i_0_671,i_0_83,i_0_82,i_0_73,i_0_72,i_0_74,i_0_65,i_0_68,i_0_64,i_0_62,i_0_63,i_0_67,i_0_66]) ).
cnf(i_0_3300,plain,
lower_dimension_point_1 != extension(X1,lower_dimension_point_2,X2,X2),
inference(scs_inference,[],[i_0_3252,i_0_3269,i_0_3243,i_0_504,i_0_671,i_0_83,i_0_82,i_0_73,i_0_72,i_0_74,i_0_65,i_0_68,i_0_64,i_0_62,i_0_63,i_0_67,i_0_66,i_0_88]) ).
cnf(i_0_3301,plain,
equidistant(z,y,x,extension(X1,w,X2,X2)),
inference(scs_inference,[],[i_0_141,i_0_3252,i_0_3269,i_0_3243,i_0_504,i_0_671,i_0_77,i_0_83,i_0_82,i_0_73,i_0_72,i_0_74,i_0_65,i_0_68,i_0_64,i_0_62,i_0_63,i_0_67,i_0_66,i_0_88,i_0_97]) ).
cnf(i_0_3303,plain,
equidistant(z,extension(X1,y,X2,X2),x,w),
inference(scs_inference,[],[i_0_141,i_0_3252,i_0_3269,i_0_3243,i_0_504,i_0_671,i_0_77,i_0_3302,i_0_83,i_0_82,i_0_73,i_0_72,i_0_74,i_0_65,i_0_68,i_0_64,i_0_62,i_0_63,i_0_67,i_0_66,i_0_88,i_0_97,i_0_95]) ).
cnf(i_0_3305,plain,
equidistant(extension(X1,z,X2,X2),y,x,w),
inference(scs_inference,[],[i_0_141,i_0_3252,i_0_3269,i_0_3243,i_0_504,i_0_671,i_0_77,i_0_3302,i_0_3304,i_0_83,i_0_82,i_0_73,i_0_72,i_0_74,i_0_65,i_0_68,i_0_64,i_0_62,i_0_63,i_0_67,i_0_66,i_0_88,i_0_97,i_0_95,i_0_94]) ).
cnf(i_0_3307,plain,
equidistant(z,y,extension(X1,x,X2,X2),w),
inference(scs_inference,[],[i_0_141,i_0_3252,i_0_3269,i_0_3243,i_0_504,i_0_671,i_0_77,i_0_3302,i_0_3304,i_0_3306,i_0_83,i_0_82,i_0_73,i_0_72,i_0_74,i_0_65,i_0_68,i_0_64,i_0_62,i_0_63,i_0_67,i_0_66,i_0_88,i_0_97,i_0_95,i_0_94,i_0_96]) ).
cnf(i_0_3309,plain,
~ equidistant(extension(X1,X1,X1,X1),extension(X2,X1,X1,X1),extension(u,v,y,z),extension(u,v,w,x)),
inference(scs_inference,[],[i_0_141,i_0_3246,i_0_3252,i_0_3261,i_0_3269,i_0_3243,i_0_504,i_0_671,i_0_77,i_0_3302,i_0_3304,i_0_3306,i_0_83,i_0_82,i_0_73,i_0_72,i_0_74,i_0_65,i_0_68,i_0_64,i_0_62,i_0_63,i_0_67,i_0_66,i_0_88,i_0_97,i_0_95,i_0_94,i_0_96,i_0_58]) ).
cnf(i_0_3313,plain,
~ equidistant(X1,extension(X2,X1,X3,X3),extension(u,v,w,x),extension(u,v,y,z)),
inference(scs_inference,[],[i_0_141,i_0_3246,i_0_3311,i_0_3252,i_0_3261,i_0_3269,i_0_3243,i_0_504,i_0_671,i_0_77,i_0_3302,i_0_3304,i_0_3306,i_0_83,i_0_82,i_0_73,i_0_72,i_0_74,i_0_65,i_0_68,i_0_64,i_0_62,i_0_63,i_0_67,i_0_66,i_0_88,i_0_97,i_0_95,i_0_94,i_0_96,i_0_58,i_0_57]) ).
cnf(i_0_3315,plain,
~ equidistant(extension(X1,X2,X3,X3),extension(X2,X2,X2,X2),extension(u,v,w,x),extension(u,v,y,z)),
inference(rename_variables,[],[i_0_3269]) ).
cnf(i_0_3317,plain,
equidistant(z,extension(y,y,y,y),x,extension(x,w,y,y)),
inference(scs_inference,[],[i_0_141,i_0_3246,i_0_3311,i_0_3252,i_0_3261,i_0_3269,i_0_3243,i_0_504,i_0_671,i_0_1016,i_0_77,i_0_3302,i_0_3304,i_0_3306,i_0_71,i_0_83,i_0_253,i_0_82,i_0_73,i_0_72,i_0_74,i_0_65,i_0_68,i_0_64,i_0_62,i_0_63,i_0_67,i_0_66,i_0_88,i_0_97,i_0_95,i_0_94,i_0_96,i_0_58,i_0_57,i_0_56]) ).
cnf(i_0_3369,plain,
between(X1,extension(X2,X3,X4,X4),extension(X5,X3,X6,X6)),
inference(rename_variables,[],[i_0_3272]) ).
cnf(i_0_3413,plain,
between(X1,extension(X2,X3,X4,X4),extension(X5,X3,X6,X6)),
inference(rename_variables,[],[i_0_3272]) ).
cnf(i_0_3484,plain,
between(X1,extension(X2,X3,X4,X4),extension(X5,X3,X6,X6)),
inference(rename_variables,[],[i_0_3272]) ).
cnf(i_0_3531,plain,
between(X1,extension(X2,X3,X4,X4),extension(X5,X3,X6,X6)),
inference(rename_variables,[],[i_0_3272]) ).
cnf(i_0_3583,plain,
between(X1,extension(X2,X3,X4,X4),extension(X5,X3,X6,X6)),
inference(rename_variables,[],[i_0_3272]) ).
cnf(i_0_3589,plain,
between(X1,extension(X2,X3,X4,X4),extension(X5,X3,X6,X6)),
inference(rename_variables,[],[i_0_3272]) ).
cnf(i_0_3590,plain,
between(X1,extension(X2,X3,X4,X4),extension(X5,X3,X6,X6)),
inference(rename_variables,[],[i_0_3272]) ).
cnf(i_0_3678,plain,
between(X1,extension(X2,X3,X4,X4),extension(X5,X3,X6,X6)),
inference(rename_variables,[],[i_0_3272]) ).
cnf(i_0_3684,plain,
between(X1,extension(X2,X3,X4,X4),extension(X5,X3,X6,X6)),
inference(rename_variables,[],[i_0_3272]) ).
cnf(i_0_3732,plain,
between(X1,extension(X2,X3,X4,X4),extension(X5,X3,X6,X6)),
inference(rename_variables,[],[i_0_3272]) ).
cnf(i_0_3777,plain,
between(X1,extension(X2,X3,X4,X4),extension(X5,X3,X6,X6)),
inference(rename_variables,[],[i_0_3272]) ).
cnf(i_0_3823,plain,
between(X1,extension(X2,X3,X4,X4),extension(X5,X3,X6,X6)),
inference(rename_variables,[],[i_0_3272]) ).
cnf(i_0_3905,plain,
between(X1,extension(X2,X3,X4,X4),extension(X5,X3,X6,X6)),
inference(rename_variables,[],[i_0_3272]) ).
cnf(i_0_3956,plain,
between(X1,extension(X2,X3,X4,X4),extension(X5,X3,X6,X6)),
inference(rename_variables,[],[i_0_3272]) ).
cnf(i_0_3993,plain,
between(X1,extension(X2,X3,X4,X4),extension(X5,X3,X6,X6)),
inference(rename_variables,[],[i_0_3272]) ).
cnf(i_0_4000,plain,
between(X1,extension(X2,X3,X4,X4),extension(X5,X3,X6,X6)),
inference(rename_variables,[],[i_0_3272]) ).
cnf(i_0_4036,plain,
between(X1,extension(X2,X3,X4,X4),extension(X5,X3,X6,X6)),
inference(rename_variables,[],[i_0_3272]) ).
cnf(i_0_4044,plain,
between(X1,extension(X2,X3,X4,X4),extension(X5,X3,X6,X6)),
inference(rename_variables,[],[i_0_3272]) ).
cnf(i_0_4119,plain,
between(X1,extension(X2,X3,X4,X4),extension(X5,X3,X6,X6)),
inference(rename_variables,[],[i_0_3272]) ).
cnf(i_0_4169,plain,
between(X1,extension(X2,X3,X4,X4),extension(X5,X3,X6,X6)),
inference(rename_variables,[],[i_0_3272]) ).
cnf(i_0_4170,plain,
between(X1,extension(X2,X3,X4,X4),extension(X5,X3,X6,X6)),
inference(rename_variables,[],[i_0_3272]) ).
cnf(i_0_4208,plain,
between(X1,extension(X2,X3,X4,X4),extension(X5,X3,X6,X6)),
inference(rename_variables,[],[i_0_3272]) ).
cnf(i_0_4214,plain,
between(X1,extension(X2,X3,X4,X4),extension(X5,X3,X6,X6)),
inference(rename_variables,[],[i_0_3272]) ).
cnf(i_0_4263,plain,
between(X1,extension(X2,X3,X4,X4),extension(X5,X3,X6,X6)),
inference(rename_variables,[],[i_0_3272]) ).
cnf(i_0_4269,plain,
between(X1,extension(X2,X3,X4,X4),extension(X5,X3,X6,X6)),
inference(rename_variables,[],[i_0_3272]) ).
cnf(i_0_4316,plain,
between(X1,extension(X2,X3,X4,X4),extension(X5,X3,X6,X6)),
inference(rename_variables,[],[i_0_3272]) ).
cnf(i_0_4321,plain,
between(X1,extension(X2,X3,X4,X4),extension(X5,X3,X6,X6)),
inference(rename_variables,[],[i_0_3272]) ).
cnf(i_0_4361,plain,
extension(X1,X2,X3,X3) = extension(X4,X2,X5,X5),
inference(scs_inference,[],[i_0_3272,i_0_82]) ).
cnf(i_0_4362,plain,
between(X1,extension(X2,X3,X4,X4),extension(X5,X3,X6,X6)),
inference(rename_variables,[],[i_0_3272]) ).
cnf(i_0_4453,plain,
between(X1,extension(X2,X3,X4,X4),extension(X5,X3,X6,X6)),
inference(rename_variables,[],[i_0_3272]) ).
cnf(i_0_4501,plain,
between(X1,extension(X2,X3,X4,X4),extension(X5,X3,X6,X6)),
inference(rename_variables,[],[i_0_3272]) ).
cnf(i_0_4547,plain,
between(X1,extension(X2,X3,X4,X4),extension(X5,X3,X6,X6)),
inference(rename_variables,[],[i_0_3272]) ).
cnf(i_0_4551,plain,
between(X1,extension(X2,X3,X4,X4),extension(X5,X3,X6,X6)),
inference(rename_variables,[],[i_0_3272]) ).
cnf(i_0_4588,plain,
between(X1,extension(X2,X3,X4,X4),extension(X5,X3,X6,X6)),
inference(rename_variables,[],[i_0_3272]) ).
cnf(i_0_4631,plain,
between(X1,extension(X2,X3,X4,X4),extension(X5,X3,X6,X6)),
inference(rename_variables,[],[i_0_3272]) ).
cnf(i_0_4674,plain,
between(X1,extension(X2,X3,X4,X4),extension(X5,X3,X6,X6)),
inference(rename_variables,[],[i_0_3272]) ).
cnf(i_0_4684,plain,
between(X1,extension(X2,X3,X4,X4),extension(X5,X3,X6,X6)),
inference(rename_variables,[],[i_0_3272]) ).
cnf(i_0_4726,plain,
between(X1,extension(X2,X3,X4,X4),extension(X5,X3,X6,X6)),
inference(rename_variables,[],[i_0_3272]) ).
cnf(i_0_2864,plain,
equidistant(extension(X1,X2,x,w),extension(X2,X2,X2,X2),y,z),
inference(scs_inference,[],[i_0_962,i_0_1765,i_0_81,i_0_2829,i_0_515,i_0_65,i_0_64,i_0_68,i_0_63,i_0_62,i_0_67,i_0_66,i_0_58,i_0_57]) ).
cnf(i_0_3326,plain,
~ equidistant(v,extension(u,v,w,x),v,extension(u,v,y,z)),
inference(scs_inference,[],[i_0_71,i_0_3322]) ).
cnf(i_0_3330,plain,
u != extension(v,u,v,u),
inference(scs_inference,[],[i_0_3231,i_0_86,i_0_71,i_0_3322,i_0_82,i_0_73]) ).
cnf(i_0_3332,plain,
lower_dimension_point_1 != extension(lower_dimension_point_2,lower_dimension_point_3,X1,X2),
inference(scs_inference,[],[i_0_3231,i_0_86,i_0_71,i_0_84,i_0_3322,i_0_82,i_0_73,i_0_72]) ).
cnf(i_0_3336,plain,
~ equidistant(extension(u,v,y,z),extension(u,v,w,x),extension(X1,X1,X1,X1),extension(X2,X1,X1,X1)),
inference(scs_inference,[],[i_0_3309,i_0_3231,i_0_86,i_0_71,i_0_84,i_0_3322,i_0_82,i_0_73,i_0_72,i_0_74,i_0_65]) ).
cnf(i_0_3338,plain,
~ equidistant(extension(u,v,w,x),extension(u,v,y,z),extension(X1,X2,X2,X2),extension(X2,X2,X2,X2)),
inference(scs_inference,[],[i_0_3309,i_0_3231,i_0_86,i_0_71,i_0_84,i_0_3322,i_0_82,i_0_73,i_0_72,i_0_74,i_0_65,i_0_68]) ).
cnf(i_0_3340,plain,
~ equidistant(extension(X1,X2,X3,X3),X2,extension(u,v,y,z),extension(u,v,w,x)),
inference(scs_inference,[],[i_0_3309,i_0_3313,i_0_3231,i_0_86,i_0_71,i_0_84,i_0_3322,i_0_82,i_0_73,i_0_72,i_0_74,i_0_65,i_0_68,i_0_64]) ).
cnf(i_0_3342,plain,
~ equidistant(extension(X1,X1,X1,X1),extension(X2,X1,X3,X3),extension(u,v,y,z),extension(u,v,w,x)),
inference(scs_inference,[],[i_0_3309,i_0_3294,i_0_3313,i_0_3231,i_0_86,i_0_71,i_0_84,i_0_3322,i_0_82,i_0_73,i_0_72,i_0_74,i_0_65,i_0_68,i_0_64,i_0_62]) ).
cnf(i_0_3344,plain,
~ equidistant(extension(u,v,y,z),extension(u,v,w,x),extension(X1,X1,X1,X1),extension(X2,X1,X3,X3)),
inference(scs_inference,[],[i_0_3309,i_0_3294,i_0_3296,i_0_3313,i_0_3231,i_0_86,i_0_71,i_0_84,i_0_3322,i_0_82,i_0_73,i_0_72,i_0_74,i_0_65,i_0_68,i_0_64,i_0_62,i_0_63]) ).
cnf(i_0_3346,plain,
~ equidistant(extension(u,v,w,x),extension(u,v,y,z),extension(X1,X2,X3,X3),extension(X2,X2,X2,X2)),
inference(scs_inference,[],[i_0_3309,i_0_3294,i_0_3296,i_0_3313,i_0_3231,i_0_86,i_0_71,i_0_84,i_0_3322,i_0_82,i_0_73,i_0_72,i_0_74,i_0_65,i_0_68,i_0_64,i_0_62,i_0_63,i_0_67]) ).
cnf(i_0_3348,plain,
~ equidistant(extension(u,v,y,z),extension(u,v,w,x),X1,extension(X2,X1,X3,X3)),
inference(scs_inference,[],[i_0_3309,i_0_3294,i_0_3296,i_0_3313,i_0_3231,i_0_86,i_0_71,i_0_84,i_0_3322,i_0_82,i_0_73,i_0_72,i_0_74,i_0_65,i_0_68,i_0_64,i_0_62,i_0_63,i_0_67,i_0_66]) ).
cnf(i_0_3529,plain,
equidistant(z,y,x,extension(X1,w,X2,X2)),
inference(rename_variables,[],[i_0_3301]) ).
cnf(i_0_3991,plain,
equidistant(z,extension(X1,y,X2,X2),x,w),
inference(rename_variables,[],[i_0_3303]) ).
cnf(i_0_4450,plain,
extension(X1,X2,X3,X3) = extension(X4,X2,X5,X5),
inference(rename_variables,[],[i_0_4361]) ).
cnf(i_0_4491,plain,
extension(X1,X2,X3,X3) = extension(X4,X2,X5,X5),
inference(rename_variables,[],[i_0_4361]) ).
cnf(i_0_4542,plain,
extension(X1,X2,X3,X3) = extension(X4,X2,X5,X5),
inference(rename_variables,[],[i_0_4361]) ).
cnf(i_0_4574,plain,
extension(X1,X2,X3,X3) = extension(X4,X2,X5,X5),
inference(rename_variables,[],[i_0_4361]) ).
cnf(i_0_4616,plain,
extension(X1,X2,X3,X3) = extension(X4,X2,X5,X5),
inference(rename_variables,[],[i_0_4361]) ).
cnf(i_0_4658,plain,
extension(X1,X2,X3,X3) = extension(X4,X2,X5,X5),
inference(rename_variables,[],[i_0_4361]) ).
cnf(i_0_4671,plain,
extension(X1,X2,X3,X3) = extension(X4,X2,X5,X5),
inference(rename_variables,[],[i_0_4361]) ).
cnf(i_0_4708,plain,
extension(X1,X2,X3,X3) = extension(X4,X2,X5,X5),
inference(rename_variables,[],[i_0_4361]) ).
cnf(i_0_4710,plain,
extension(X1,X2,X3,X3) = extension(X4,X2,X5,X5),
inference(rename_variables,[],[i_0_4361]) ).
cnf(i_0_2892,plain,
equidistant(extension(X1,X1,X1,X1),extension(X2,X1,X1,X1),X1,extension(X3,X1,X4,X4)),
inference(scs_inference,[],[i_0_1771,i_0_1084,i_0_2860,i_0_65,i_0_64,i_0_68,i_0_63,i_0_62,i_0_67,i_0_66,i_0_58]) ).
cnf(i_0_3382,plain,
~ equidistant(v,extension(u,v,y,z),v,extension(u,v,w,x)),
inference(scs_inference,[],[i_0_3326,i_0_3280,i_0_1145,i_0_82,i_0_72,i_0_74,i_0_65]) ).
cnf(i_0_3384,plain,
~ equidistant(extension(u,v,y,z),v,extension(u,v,w,x),v),
inference(scs_inference,[],[i_0_3326,i_0_3280,i_0_1145,i_0_82,i_0_72,i_0_74,i_0_65,i_0_68]) ).
cnf(i_0_3386,plain,
~ equidistant(extension(u,v,w,x),v,extension(u,v,y,z),v),
inference(scs_inference,[],[i_0_3326,i_0_3280,i_0_1145,i_0_82,i_0_72,i_0_74,i_0_65,i_0_68,i_0_64]) ).
cnf(i_0_3388,plain,
~ equidistant(v,extension(u,v,w,x),extension(u,v,y,z),v),
inference(scs_inference,[],[i_0_3326,i_0_3280,i_0_1145,i_0_82,i_0_72,i_0_74,i_0_65,i_0_68,i_0_64,i_0_62]) ).
cnf(i_0_3390,plain,
~ equidistant(extension(u,v,w,x),v,v,extension(u,v,y,z)),
inference(scs_inference,[],[i_0_3326,i_0_3280,i_0_1145,i_0_82,i_0_72,i_0_74,i_0_65,i_0_68,i_0_64,i_0_62,i_0_63]) ).
cnf(i_0_3392,plain,
~ equidistant(v,extension(u,v,y,z),extension(u,v,w,x),v),
inference(scs_inference,[],[i_0_3326,i_0_3280,i_0_1145,i_0_82,i_0_72,i_0_74,i_0_65,i_0_68,i_0_64,i_0_62,i_0_63,i_0_67]) ).
cnf(i_0_3394,plain,
~ equidistant(extension(u,v,y,z),v,v,extension(u,v,w,x)),
inference(scs_inference,[],[i_0_3326,i_0_3280,i_0_1145,i_0_82,i_0_72,i_0_74,i_0_65,i_0_68,i_0_64,i_0_62,i_0_63,i_0_67,i_0_66]) ).
cnf(i_0_3397,plain,
equidistant(x,w,y,extension(X1,z,X2,X2)),
inference(scs_inference,[],[i_0_143,i_0_3326,i_0_3280,i_0_77,i_0_1145,i_0_82,i_0_72,i_0_74,i_0_65,i_0_68,i_0_64,i_0_62,i_0_63,i_0_67,i_0_66,i_0_88,i_0_97]) ).
cnf(i_0_3399,plain,
equidistant(x,extension(X1,w,X2,X2),y,z),
inference(scs_inference,[],[i_0_143,i_0_3326,i_0_3280,i_0_77,i_0_3398,i_0_1145,i_0_82,i_0_72,i_0_74,i_0_65,i_0_68,i_0_64,i_0_62,i_0_63,i_0_67,i_0_66,i_0_88,i_0_97,i_0_95]) ).
cnf(i_0_3401,plain,
equidistant(extension(X1,x,X2,X2),w,y,z),
inference(scs_inference,[],[i_0_143,i_0_3326,i_0_3280,i_0_77,i_0_3398,i_0_3400,i_0_1145,i_0_82,i_0_72,i_0_74,i_0_65,i_0_68,i_0_64,i_0_62,i_0_63,i_0_67,i_0_66,i_0_88,i_0_97,i_0_95,i_0_94]) ).
cnf(i_0_3403,plain,
equidistant(x,w,extension(X1,y,X2,X2),z),
inference(scs_inference,[],[i_0_143,i_0_3326,i_0_3280,i_0_77,i_0_3398,i_0_3400,i_0_3402,i_0_1145,i_0_82,i_0_72,i_0_74,i_0_65,i_0_68,i_0_64,i_0_62,i_0_63,i_0_67,i_0_66,i_0_88,i_0_97,i_0_95,i_0_94,i_0_96]) ).
cnf(i_0_3405,plain,
~ equidistant(extension(u,v,w,x),extension(X1,v,X2,X2),v,extension(u,v,y,z)),
inference(scs_inference,[],[i_0_143,i_0_1454,i_0_3326,i_0_3280,i_0_77,i_0_3398,i_0_3400,i_0_3402,i_0_1145,i_0_82,i_0_72,i_0_74,i_0_65,i_0_68,i_0_64,i_0_62,i_0_63,i_0_67,i_0_66,i_0_88,i_0_97,i_0_95,i_0_94,i_0_96,i_0_58]) ).
cnf(i_0_3408,plain,
~ equidistant(X1,extension(X2,X1,X3,X3),extension(u,v,y,z),extension(u,v,w,x)),
inference(scs_inference,[],[i_0_143,i_0_2119,i_0_1454,i_0_3326,i_0_3292,i_0_3280,i_0_77,i_0_3398,i_0_3400,i_0_3402,i_0_1145,i_0_82,i_0_72,i_0_74,i_0_65,i_0_68,i_0_64,i_0_62,i_0_63,i_0_67,i_0_66,i_0_88,i_0_97,i_0_95,i_0_94,i_0_96,i_0_58,i_0_57]) ).
cnf(i_0_3411,plain,
equidistant(extension(X1,X2,X3,X4),extension(X2,X2,X2,X2),extension(X5,X2,X4,X3),X2),
inference(scs_inference,[],[i_0_143,i_0_2796,i_0_2119,i_0_2440,i_0_1454,i_0_3326,i_0_3292,i_0_3280,i_0_3272,i_0_77,i_0_3398,i_0_3400,i_0_3402,i_0_1145,i_0_467,i_0_82,i_0_72,i_0_74,i_0_65,i_0_68,i_0_64,i_0_62,i_0_63,i_0_67,i_0_66,i_0_88,i_0_97,i_0_95,i_0_94,i_0_96,i_0_58,i_0_57,i_0_56]) ).
cnf(i_0_3434,plain,
~ between(u,extension(v,u,v,u),u),
inference(scs_inference,[],[i_0_3330,i_0_82]) ).
cnf(i_0_3438,plain,
~ equidistant(u,extension(v,u,v,u),X1,X1),
inference(scs_inference,[],[i_0_3330,i_0_166,i_0_82,i_0_72,i_0_74]) ).
cnf(i_0_3469,plain,
~ equidistant(X1,extension(X2,X1,X3,X3),extension(u,v,y,z),extension(u,v,w,x)),
inference(rename_variables,[],[i_0_3408]) ).
cnf(i_0_3520,plain,
equidistant(extension(X1,X2,X3,X4),extension(X2,X2,X2,X2),extension(X5,X2,X4,X3),X2),
inference(rename_variables,[],[i_0_3411]) ).
cnf(i_0_4205,plain,
equidistant(extension(X1,X2,X3,X4),extension(X2,X2,X2,X2),extension(X5,X2,X4,X3),X2),
inference(rename_variables,[],[i_0_3411]) ).
cnf(i_0_4452,plain,
equidistant(x,w,y,extension(X1,z,X2,X2)),
inference(rename_variables,[],[i_0_3397]) ).
cnf(i_0_3106,plain,
equidistant(extension(X1,X1,X1,X1),extension(X2,X1,X3,X4),X4,extension(X3,X3,X3,X3)),
inference(scs_inference,[],[i_0_1722,i_0_3075,i_0_2073,i_0_65,i_0_64,i_0_68,i_0_63,i_0_62,i_0_67,i_0_66,i_0_58]) ).
cnf(i_0_3127,plain,
equidistant(X1,extension(X2,X2,X2,X2),extension(X3,X3,X3,X3),extension(X4,X3,X2,X1)),
inference(scs_inference,[],[i_0_3106,i_0_65]) ).
cnf(i_0_3131,plain,
equidistant(extension(X1,X1,X1,X1),X2,extension(X3,X4,X1,X2),extension(X4,X4,X4,X4)),
inference(scs_inference,[],[i_0_3106,i_0_3110,i_0_65,i_0_64,i_0_68]) ).
cnf(i_0_3135,plain,
equidistant(extension(X1,X1,X1,X1),extension(X2,X1,X3,X4),extension(X3,X3,X3,X3),X4),
inference(scs_inference,[],[i_0_3106,i_0_3110,i_0_65,i_0_64,i_0_68,i_0_63,i_0_62]) ).
cnf(i_0_3137,plain,
equidistant(extension(X1,X1,X1,X1),X2,extension(X3,X3,X3,X3),extension(X4,X3,X1,X2)),
inference(scs_inference,[],[i_0_3106,i_0_3110,i_0_65,i_0_64,i_0_68,i_0_63,i_0_62,i_0_67]) ).
cnf(i_0_3139,plain,
equidistant(X1,extension(X2,X2,X2,X2),extension(X3,X4,X2,X1),extension(X4,X4,X4,X4)),
inference(scs_inference,[],[i_0_3106,i_0_3110,i_0_65,i_0_64,i_0_68,i_0_63,i_0_62,i_0_67,i_0_66]) ).
cnf(i_0_3178,plain,
equidistant(X1,extension(X2,X2,X2,X2),extension(X3,X3,X3,X3),extension(X4,X3,X2,X1)),
inference(rename_variables,[],[i_0_3127]) ).
cnf(i_0_3211,plain,
equidistant(extension(X1,X1,X1,X1),X2,extension(X3,X4,X1,X2),extension(X4,X4,X4,X4)),
inference(rename_variables,[],[i_0_3131]) ).
cnf(i_0_3275,plain,
equidistant(extension(X1,X1,X1,X1),X2,extension(X3,X3,X3,X3),extension(X4,X3,X1,X2)),
inference(rename_variables,[],[i_0_3137]) ).
cnf(i_0_3351,plain,
equidistant(X1,extension(X2,X2,X2,X2),extension(X3,X4,X2,X1),extension(X5,X4,X6,X6)),
inference(scs_inference,[],[i_0_3139,i_0_3309,i_0_3294,i_0_3296,i_0_3313,i_0_3231,i_0_86,i_0_1003,i_0_71,i_0_84,i_0_3322,i_0_82,i_0_73,i_0_72,i_0_74,i_0_65,i_0_68,i_0_64,i_0_62,i_0_63,i_0_67,i_0_66,i_0_88,i_0_97]) ).
cnf(i_0_3353,plain,
equidistant(X1,extension(X2,X3,X4,X4),extension(X5,X6,X3,X1),extension(X6,X6,X6,X6)),
inference(scs_inference,[],[i_0_3139,i_0_3309,i_0_3294,i_0_3296,i_0_3313,i_0_3231,i_0_86,i_0_1003,i_0_3352,i_0_71,i_0_84,i_0_3322,i_0_82,i_0_73,i_0_72,i_0_74,i_0_65,i_0_68,i_0_64,i_0_62,i_0_63,i_0_67,i_0_66,i_0_88,i_0_97,i_0_95]) ).
cnf(i_0_3355,plain,
equidistant(extension(X1,z,X2,X2),y,w,x),
inference(scs_inference,[],[i_0_153,i_0_3139,i_0_3309,i_0_3294,i_0_3296,i_0_3313,i_0_3231,i_0_86,i_0_1003,i_0_3352,i_0_77,i_0_71,i_0_84,i_0_3322,i_0_82,i_0_73,i_0_72,i_0_74,i_0_65,i_0_68,i_0_64,i_0_62,i_0_63,i_0_67,i_0_66,i_0_88,i_0_97,i_0_95,i_0_94]) ).
cnf(i_0_3357,plain,
equidistant(z,y,extension(X1,w,X2,X2),x),
inference(scs_inference,[],[i_0_153,i_0_3139,i_0_3309,i_0_3294,i_0_3296,i_0_3313,i_0_3231,i_0_86,i_0_1003,i_0_3352,i_0_77,i_0_3356,i_0_71,i_0_84,i_0_3322,i_0_82,i_0_73,i_0_72,i_0_74,i_0_65,i_0_68,i_0_64,i_0_62,i_0_63,i_0_67,i_0_66,i_0_88,i_0_97,i_0_95,i_0_94,i_0_96]) ).
cnf(i_0_3359,plain,
~ equidistant(extension(X1,X2,X3,X3),X2,extension(u,v,w,x),extension(u,v,y,z)),
inference(scs_inference,[],[i_0_153,i_0_3139,i_0_3309,i_0_3294,i_0_3296,i_0_3313,i_0_3231,i_0_1080,i_0_86,i_0_1003,i_0_3352,i_0_77,i_0_3356,i_0_71,i_0_84,i_0_3322,i_0_82,i_0_73,i_0_72,i_0_74,i_0_65,i_0_68,i_0_64,i_0_62,i_0_63,i_0_67,i_0_66,i_0_88,i_0_97,i_0_95,i_0_94,i_0_96,i_0_58]) ).
cnf(i_0_3362,plain,
~ equidistant(extension(X1,X2,lower_dimension_point_2,lower_dimension_point_1),X2,X3,X3),
inference(scs_inference,[],[i_0_153,i_0_3139,i_0_1014,i_0_3309,i_0_3294,i_0_3296,i_0_3313,i_0_3284,i_0_3231,i_0_1080,i_0_86,i_0_1003,i_0_3352,i_0_77,i_0_3356,i_0_71,i_0_84,i_0_3322,i_0_82,i_0_73,i_0_72,i_0_74,i_0_65,i_0_68,i_0_64,i_0_62,i_0_63,i_0_67,i_0_66,i_0_88,i_0_97,i_0_95,i_0_94,i_0_96,i_0_58,i_0_57]) ).
cnf(i_0_3370,plain,
equidistant(extension(X1,X1,X1,X1),X2,extension(X3,X4,X1,X2),extension(X4,X4,X4,X4)),
inference(rename_variables,[],[i_0_3131]) ).
cnf(i_0_3680,plain,
equidistant(extension(X1,X1,X1,X1),extension(X2,X1,X3,X4),extension(X3,X3,X3,X3),X4),
inference(rename_variables,[],[i_0_3135]) ).
cnf(i_0_3825,plain,
equidistant(extension(X1,X1,X1,X1),X2,extension(X3,X3,X3,X3),extension(X4,X3,X1,X2)),
inference(rename_variables,[],[i_0_3137]) ).
cnf(i_0_4123,plain,
equidistant(X1,extension(X2,X2,X2,X2),extension(X3,X3,X3,X3),extension(X4,X3,X2,X1)),
inference(rename_variables,[],[i_0_3127]) ).
cnf(i_0_4278,plain,
equidistant(extension(X1,X1,X1,X1),extension(X2,X1,X3,X4),extension(X3,X3,X3,X3),X4),
inference(rename_variables,[],[i_0_3135]) ).
cnf(i_0_4420,plain,
equidistant(extension(X1,X1,X1,X1),X2,extension(X3,X3,X3,X3),extension(X4,X3,X1,X2)),
inference(rename_variables,[],[i_0_3137]) ).
cnf(i_0_4509,plain,
equidistant(X1,extension(X2,X2,X2,X2),extension(X3,X3,X3,X3),extension(X4,X3,X2,X1)),
inference(rename_variables,[],[i_0_3127]) ).
cnf(i_0_4677,plain,
equidistant(extension(X1,X1,X1,X1),X2,extension(X3,X4,X1,X2),extension(X4,X4,X4,X4)),
inference(rename_variables,[],[i_0_3131]) ).
cnf(i_0_4766,plain,
equidistant(extension(X1,X1,X1,X1),extension(X2,X1,X3,X4),extension(X3,X3,X3,X3),X4),
inference(rename_variables,[],[i_0_3135]) ).
cnf(i_0_3206,plain,
equidistant(X1,X1,X1,extension(X2,extension(X1,X1,X1,X1),X1,extension(X1,X1,X1,X1))),
inference(scs_inference,[],[i_0_968,i_0_3177,i_0_3173,i_0_65,i_0_68,i_0_64,i_0_62,i_0_63,i_0_67,i_0_66,i_0_58]) ).
cnf(i_0_3419,plain,
~ equidistant(extension(X1,X2,lower_dimension_point_2,lower_dimension_point_1),X2,X3,X3),
inference(rename_variables,[],[i_0_3362]) ).
cnf(i_0_3454,plain,
extension(v,u,v,u) != u,
inference(scs_inference,[],[i_0_3330,i_0_3366,i_0_166,i_0_82,i_0_72,i_0_74,i_0_65,i_0_68,i_0_64,i_0_62,i_0_63,i_0_67,i_0_66,i_0_88]) ).
cnf(i_0_3465,plain,
~ equidistant(lower_dimension_point_2,lower_dimension_point_1,X1,X1),
inference(scs_inference,[],[i_0_2991,i_0_3457,i_0_3460,i_0_3330,i_0_3366,i_0_3334,i_0_114,i_0_1003,i_0_3456,i_0_3459,i_0_3462,i_0_166,i_0_82,i_0_72,i_0_74,i_0_65,i_0_68,i_0_64,i_0_62,i_0_63,i_0_67,i_0_66,i_0_88,i_0_97,i_0_95,i_0_94,i_0_96,i_0_58]) ).
cnf(i_0_3468,plain,
~ equidistant(extension(X1,X2,X3,X3),extension(X4,X2,X5,X5),extension(u,v,y,z),extension(u,v,w,x)),
inference(scs_inference,[],[i_0_2991,i_0_3457,i_0_3460,i_0_3351,i_0_3330,i_0_3366,i_0_3334,i_0_3408,i_0_114,i_0_1003,i_0_3456,i_0_3459,i_0_3462,i_0_166,i_0_82,i_0_72,i_0_74,i_0_65,i_0_68,i_0_64,i_0_62,i_0_63,i_0_67,i_0_66,i_0_88,i_0_97,i_0_95,i_0_94,i_0_96,i_0_58,i_0_57]) ).
cnf(i_0_3470,plain,
equidistant(X1,extension(X2,X2,X2,X2),extension(X3,X4,X2,X1),extension(X5,X4,X6,X6)),
inference(rename_variables,[],[i_0_3351]) ).
cnf(i_0_3472,plain,
extension(X1,u,X2,X2) != extension(v,u,v,u),
inference(scs_inference,[],[i_0_2991,i_0_3457,i_0_3460,i_0_3351,i_0_3330,i_0_3366,i_0_3334,i_0_3408,i_0_114,i_0_1003,i_0_3456,i_0_3459,i_0_3462,i_0_77,i_0_166,i_0_82,i_0_72,i_0_74,i_0_65,i_0_68,i_0_64,i_0_62,i_0_63,i_0_67,i_0_66,i_0_88,i_0_97,i_0_95,i_0_94,i_0_96,i_0_58,i_0_57,i_0_89]) ).
cnf(i_0_3474,plain,
equidistant(x,extension(x,w,X1,X1),z,extension(X2,y,w,w)),
inference(scs_inference,[],[i_0_145,i_0_2991,i_0_3457,i_0_3460,i_0_3351,i_0_3330,i_0_3366,i_0_3334,i_0_3408,i_0_114,i_0_1088,i_0_1003,i_0_3456,i_0_3459,i_0_3462,i_0_77,i_0_71,i_0_166,i_0_253,i_0_82,i_0_72,i_0_74,i_0_65,i_0_68,i_0_64,i_0_62,i_0_63,i_0_67,i_0_66,i_0_88,i_0_97,i_0_95,i_0_94,i_0_96,i_0_58,i_0_57,i_0_89,i_0_56]) ).
cnf(i_0_3482,plain,
equidistant(X1,extension(X2,X3,X4,X4),extension(X5,X6,X3,X1),extension(X6,X6,X6,X6)),
inference(rename_variables,[],[i_0_3353]) ).
cnf(i_0_3483,plain,
equidistant(X1,extension(X2,X2,X2,X2),extension(X3,X4,X2,X1),extension(X5,X4,X6,X6)),
inference(rename_variables,[],[i_0_3351]) ).
cnf(i_0_3532,plain,
~ equidistant(extension(X1,X2,lower_dimension_point_2,lower_dimension_point_1),X2,X3,X3),
inference(rename_variables,[],[i_0_3362]) ).
cnf(i_0_4043,plain,
equidistant(X1,extension(X2,X2,X2,X2),extension(X3,X4,X2,X1),extension(X5,X4,X6,X6)),
inference(rename_variables,[],[i_0_3351]) ).
cnf(i_0_4200,plain,
equidistant(X1,extension(X2,X3,X4,X4),extension(X5,X6,X3,X1),extension(X6,X6,X6,X6)),
inference(rename_variables,[],[i_0_3353]) ).
cnf(i_0_4455,plain,
equidistant(X1,extension(X2,X3,X4,X4),extension(X5,X6,X3,X1),extension(X6,X6,X6,X6)),
inference(rename_variables,[],[i_0_3353]) ).
cnf(i_0_4553,plain,
~ equidistant(extension(X1,X2,lower_dimension_point_2,lower_dimension_point_1),X2,X3,X3),
inference(rename_variables,[],[i_0_3362]) ).
cnf(i_0_3488,plain,
~ between(extension(X1,u,X2,X2),extension(v,u,v,u),extension(X1,u,X2,X2)),
inference(scs_inference,[],[i_0_3472,i_0_82]) ).
cnf(i_0_3490,plain,
~ equidistant(extension(X1,u,X2,X2),extension(v,u,v,u),X3,X3),
inference(scs_inference,[],[i_0_3472,i_0_82,i_0_74]) ).
cnf(i_0_3492,plain,
~ equidistant(X1,X1,lower_dimension_point_2,lower_dimension_point_1),
inference(scs_inference,[],[i_0_3465,i_0_3472,i_0_82,i_0_74,i_0_65]) ).
cnf(i_0_3494,plain,
~ equidistant(X1,X1,lower_dimension_point_1,lower_dimension_point_2),
inference(scs_inference,[],[i_0_3465,i_0_3472,i_0_82,i_0_74,i_0_65,i_0_68]) ).
cnf(i_0_3496,plain,
~ equidistant(lower_dimension_point_1,lower_dimension_point_2,X1,X1),
inference(scs_inference,[],[i_0_3465,i_0_3472,i_0_82,i_0_74,i_0_65,i_0_68,i_0_64]) ).
cnf(i_0_3498,plain,
~ equidistant(extension(u,v,y,z),extension(u,v,w,x),extension(X1,X2,X3,X3),X2),
inference(scs_inference,[],[i_0_3465,i_0_3472,i_0_3348,i_0_82,i_0_74,i_0_65,i_0_68,i_0_64,i_0_62]) ).
cnf(i_0_3500,plain,
~ equidistant(extension(v,u,v,u),u,X1,X1),
inference(scs_inference,[],[i_0_3465,i_0_3472,i_0_3438,i_0_3348,i_0_82,i_0_74,i_0_65,i_0_68,i_0_64,i_0_62,i_0_63]) ).
cnf(i_0_3506,plain,
extension(v,u,v,u) != extension(X1,u,X2,X2),
inference(scs_inference,[],[i_0_3465,i_0_3472,i_0_3380,i_0_3438,i_0_3348,i_0_82,i_0_74,i_0_65,i_0_68,i_0_64,i_0_62,i_0_63,i_0_67,i_0_66,i_0_88]) ).
cnf(i_0_3507,plain,
equidistant(y,z,w,extension(X1,x,X2,X2)),
inference(scs_inference,[],[i_0_147,i_0_3465,i_0_3472,i_0_3380,i_0_3438,i_0_3348,i_0_77,i_0_82,i_0_74,i_0_65,i_0_68,i_0_64,i_0_62,i_0_63,i_0_67,i_0_66,i_0_88,i_0_97]) ).
cnf(i_0_3509,plain,
equidistant(y,extension(X1,z,X2,X2),w,x),
inference(scs_inference,[],[i_0_147,i_0_3465,i_0_3472,i_0_3380,i_0_3438,i_0_3348,i_0_77,i_0_3508,i_0_82,i_0_74,i_0_65,i_0_68,i_0_64,i_0_62,i_0_63,i_0_67,i_0_66,i_0_88,i_0_97,i_0_95]) ).
cnf(i_0_3511,plain,
equidistant(extension(X1,y,X2,X2),z,w,x),
inference(scs_inference,[],[i_0_147,i_0_3465,i_0_3472,i_0_3380,i_0_3438,i_0_3348,i_0_77,i_0_3508,i_0_3510,i_0_82,i_0_74,i_0_65,i_0_68,i_0_64,i_0_62,i_0_63,i_0_67,i_0_66,i_0_88,i_0_97,i_0_95,i_0_94]) ).
cnf(i_0_3513,plain,
equidistant(y,z,extension(X1,w,X2,X2),x),
inference(scs_inference,[],[i_0_147,i_0_3465,i_0_3472,i_0_3380,i_0_3438,i_0_3348,i_0_77,i_0_3508,i_0_3510,i_0_3512,i_0_82,i_0_74,i_0_65,i_0_68,i_0_64,i_0_62,i_0_63,i_0_67,i_0_66,i_0_88,i_0_97,i_0_95,i_0_94,i_0_96]) ).
cnf(i_0_3523,plain,
equidistant(y,extension(z,z,z,z),w,extension(w,x,z,z)),
inference(scs_inference,[],[i_0_147,i_0_3465,i_0_3455,i_0_3411,i_0_3472,i_0_3440,i_0_3516,i_0_3380,i_0_3438,i_0_3348,i_0_1016,i_0_77,i_0_3508,i_0_3510,i_0_3512,i_0_71,i_0_253,i_0_82,i_0_74,i_0_65,i_0_68,i_0_64,i_0_62,i_0_63,i_0_67,i_0_66,i_0_88,i_0_97,i_0_95,i_0_94,i_0_96,i_0_58,i_0_57,i_0_56]) ).
cnf(i_0_3546,plain,
~ between(extension(v,u,v,u),extension(X1,u,X2,X2),extension(v,u,v,u)),
inference(scs_inference,[],[i_0_3506,i_0_82]) ).
cnf(i_0_3548,plain,
~ equidistant(extension(v,u,v,u),extension(X1,u,X2,X2),X3,X3),
inference(scs_inference,[],[i_0_3506,i_0_82,i_0_74]) ).
cnf(i_0_3564,plain,
v != extension(X1,u,X2,X2),
inference(scs_inference,[],[i_0_3515,i_0_3506,i_0_3255,i_0_82,i_0_74,i_0_65,i_0_68,i_0_64,i_0_62,i_0_63,i_0_67,i_0_66,i_0_88]) ).
cnf(i_0_3574,plain,
~ equidistant(X1,X1,lower_dimension_point_2,lower_dimension_point_1),
inference(rename_variables,[],[i_0_3492]) ).
cnf(i_0_3577,plain,
~ equidistant(X1,X1,lower_dimension_point_1,lower_dimension_point_2),
inference(rename_variables,[],[i_0_3494]) ).
cnf(i_0_3581,plain,
~ equidistant(X1,X1,lower_dimension_point_2,lower_dimension_point_1),
inference(rename_variables,[],[i_0_3492]) ).
cnf(i_0_3601,plain,
~ equidistant(X1,X1,extension(X2,u,X3,X3),extension(v,u,v,u)),
inference(scs_inference,[],[i_0_3490,i_0_3350,i_0_82,i_0_74,i_0_65]) ).
cnf(i_0_3603,plain,
~ equidistant(X1,X1,extension(v,u,v,u),extension(X2,u,X3,X3)),
inference(scs_inference,[],[i_0_3490,i_0_3350,i_0_82,i_0_74,i_0_65,i_0_68]) ).
cnf(i_0_3605,plain,
~ equidistant(extension(u,v,w,x),extension(u,v,y,z),X1,extension(X2,X1,X3,X3)),
inference(scs_inference,[],[i_0_3490,i_0_3498,i_0_3350,i_0_82,i_0_74,i_0_65,i_0_68,i_0_64]) ).
cnf(i_0_3607,plain,
~ equidistant(extension(X1,X2,X3,X3),extension(X4,X2,X5,X5),extension(u,v,w,x),extension(u,v,y,z)),
inference(scs_inference,[],[i_0_3490,i_0_3498,i_0_3468,i_0_3350,i_0_82,i_0_74,i_0_65,i_0_68,i_0_64,i_0_62]) ).
cnf(i_0_3609,plain,
~ equidistant(extension(u,v,w,x),extension(u,v,y,z),extension(X1,X2,X3,X3),X2),
inference(scs_inference,[],[i_0_3490,i_0_3498,i_0_3468,i_0_3350,i_0_82,i_0_74,i_0_65,i_0_68,i_0_64,i_0_62,i_0_63]) ).
cnf(i_0_3611,plain,
~ equidistant(X1,X1,u,extension(v,u,v,u)),
inference(scs_inference,[],[i_0_3490,i_0_3500,i_0_3498,i_0_3468,i_0_3350,i_0_82,i_0_74,i_0_65,i_0_68,i_0_64,i_0_62,i_0_63,i_0_67]) ).
cnf(i_0_3613,plain,
~ equidistant(X1,X1,extension(v,u,v,u),u),
inference(scs_inference,[],[i_0_3490,i_0_3500,i_0_3498,i_0_3468,i_0_3350,i_0_82,i_0_74,i_0_65,i_0_68,i_0_64,i_0_62,i_0_63,i_0_67,i_0_66]) ).
cnf(i_0_3615,plain,
extension(lower_dimension_point_2,lower_dimension_point_3,X1,X2) != lower_dimension_point_1,
inference(scs_inference,[],[i_0_3490,i_0_3500,i_0_3498,i_0_3468,i_0_3350,i_0_3332,i_0_82,i_0_74,i_0_65,i_0_68,i_0_64,i_0_62,i_0_63,i_0_67,i_0_66,i_0_88]) ).
cnf(i_0_3618,plain,
equidistant(extension(X1,x,X2,X2),extension(x,w,X3,X3),z,extension(X4,y,w,w)),
inference(scs_inference,[],[i_0_2139,i_0_3490,i_0_3500,i_0_3498,i_0_3468,i_0_3350,i_0_3474,i_0_3332,i_0_1020,i_0_77,i_0_82,i_0_74,i_0_65,i_0_68,i_0_64,i_0_62,i_0_63,i_0_67,i_0_66,i_0_88,i_0_97,i_0_94]) ).
cnf(i_0_3622,plain,
~ equidistant(extension(X1,lower_dimension_point_1,X2,X2),lower_dimension_point_2,X3,X3),
inference(scs_inference,[],[i_0_3496,i_0_2139,i_0_3617,i_0_1493,i_0_3490,i_0_3500,i_0_3498,i_0_3468,i_0_3350,i_0_3474,i_0_3332,i_0_1020,i_0_77,i_0_82,i_0_74,i_0_65,i_0_68,i_0_64,i_0_62,i_0_63,i_0_67,i_0_66,i_0_88,i_0_97,i_0_94,i_0_96,i_0_58]) ).
cnf(i_0_4217,plain,
extension(v,u,v,u) != extension(X1,u,X2,X2),
inference(rename_variables,[],[i_0_3506]) ).
cnf(i_0_4583,plain,
equidistant(y,extension(X1,z,X2,X2),w,x),
inference(rename_variables,[],[i_0_3509]) ).
cnf(i_0_3639,plain,
~ equidistant(v,extension(X1,u,X2,X2),X3,X3),
inference(scs_inference,[],[i_0_3396,i_0_3564,i_0_82,i_0_74]) ).
cnf(i_0_3668,plain,
~ equidistant(extension(v,u,v,u),extension(X1,u,X2,X2),X3,X3),
inference(rename_variables,[],[i_0_3548]) ).
cnf(i_0_3673,plain,
extension(lower_dimension_point_2,lower_dimension_point_3,X1,X2) != lower_dimension_point_1,
inference(rename_variables,[],[i_0_3615]) ).
cnf(i_0_3683,plain,
v != extension(X1,u,X2,X2),
inference(rename_variables,[],[i_0_3564]) ).
cnf(i_0_3766,plain,
~ equidistant(X1,X1,extension(X2,u,X3,X3),extension(v,u,v,u)),
inference(rename_variables,[],[i_0_3601]) ).
cnf(i_0_3806,plain,
equidistant(extension(X1,x,X2,X2),extension(x,w,X3,X3),z,extension(X4,y,w,w)),
inference(rename_variables,[],[i_0_3618]) ).
cnf(i_0_3809,plain,
equidistant(extension(X1,x,X2,X2),extension(x,w,X3,X3),z,extension(X4,y,w,w)),
inference(rename_variables,[],[i_0_3618]) ).
cnf(i_0_3942,plain,
~ equidistant(X1,X1,extension(v,u,v,u),extension(X2,u,X3,X3)),
inference(rename_variables,[],[i_0_3603]) ).
cnf(i_0_3945,plain,
~ equidistant(X1,X1,extension(v,u,v,u),extension(X2,u,X3,X3)),
inference(rename_variables,[],[i_0_3603]) ).
cnf(i_0_4835,plain,
extension(lower_dimension_point_2,lower_dimension_point_3,X1,X2) != lower_dimension_point_1,
inference(rename_variables,[],[i_0_3615]) ).
cnf(i_0_3649,plain,
~ equidistant(lower_dimension_point_2,extension(X1,lower_dimension_point_1,X2,X2),X3,X3),
inference(scs_inference,[],[i_0_3625,i_0_3622,i_0_3580,i_0_3396,i_0_3564,i_0_82,i_0_74,i_0_65,i_0_68,i_0_64,i_0_62,i_0_63]) ).
cnf(i_0_3656,plain,
equidistant(extension(X1,X2,X3,X3),X2,extension(X4,X4,X4,X4),extension(X5,X4,X6,X6)),
inference(scs_inference,[],[i_0_3586,i_0_3625,i_0_3599,i_0_3622,i_0_3580,i_0_3396,i_0_3564,i_0_3436,i_0_103,i_0_82,i_0_74,i_0_65,i_0_68,i_0_64,i_0_62,i_0_63,i_0_67,i_0_66,i_0_88,i_0_95]) ).
cnf(i_0_3658,plain,
equidistant(extension(X1,X2,X3,X3),extension(X2,X2,X2,X2),extension(X4,X4,X4,X4),X4),
inference(scs_inference,[],[i_0_3586,i_0_3625,i_0_3599,i_0_3622,i_0_3580,i_0_3396,i_0_3564,i_0_3436,i_0_103,i_0_3657,i_0_82,i_0_74,i_0_65,i_0_68,i_0_64,i_0_62,i_0_63,i_0_67,i_0_66,i_0_88,i_0_95,i_0_97]) ).
cnf(i_0_3660,plain,
equidistant(extension(X1,X2,X3,X3),extension(X2,X2,X2,X2),X4,extension(X5,X4,X6,X6)),
inference(scs_inference,[],[i_0_3586,i_0_3625,i_0_3599,i_0_3622,i_0_3580,i_0_3396,i_0_3564,i_0_3436,i_0_103,i_0_3657,i_0_3659,i_0_82,i_0_74,i_0_65,i_0_68,i_0_64,i_0_62,i_0_63,i_0_67,i_0_66,i_0_88,i_0_95,i_0_97,i_0_96]) ).
cnf(i_0_3662,plain,
equidistant(X1,extension(X1,X1,X1,X1),extension(X2,X2,X2,X2),extension(X3,X2,X4,X4)),
inference(scs_inference,[],[i_0_3586,i_0_3625,i_0_3599,i_0_3622,i_0_3580,i_0_3396,i_0_3564,i_0_3436,i_0_103,i_0_3657,i_0_3659,i_0_3661,i_0_82,i_0_74,i_0_65,i_0_68,i_0_64,i_0_62,i_0_63,i_0_67,i_0_66,i_0_88,i_0_95,i_0_97,i_0_96,i_0_94]) ).
cnf(i_0_3667,plain,
~ equidistant(u,extension(X1,v,X2,X2),X3,X3),
inference(scs_inference,[],[i_0_3586,i_0_3568,i_0_2261,i_0_3556,i_0_3548,i_0_3625,i_0_3599,i_0_3622,i_0_3580,i_0_3396,i_0_3564,i_0_3436,i_0_103,i_0_3657,i_0_3659,i_0_3661,i_0_82,i_0_74,i_0_65,i_0_68,i_0_64,i_0_62,i_0_63,i_0_67,i_0_66,i_0_88,i_0_95,i_0_97,i_0_96,i_0_94,i_0_58,i_0_57]) ).
cnf(i_0_3671,plain,
lower_dimension_point_3 != lower_dimension_point_1,
inference(scs_inference,[],[i_0_3586,i_0_3568,i_0_2261,i_0_3556,i_0_3548,i_0_3625,i_0_3599,i_0_3622,i_0_3580,i_0_3396,i_0_3564,i_0_3615,i_0_3436,i_0_103,i_0_3657,i_0_3659,i_0_3661,i_0_3663,i_0_82,i_0_74,i_0_65,i_0_68,i_0_64,i_0_62,i_0_63,i_0_67,i_0_66,i_0_88,i_0_95,i_0_97,i_0_96,i_0_94,i_0_58,i_0_57,i_0_89]) ).
cnf(i_0_3676,plain,
equidistant(extension(X1,X2,X3,X3),extension(X4,X2,X5,X5),extension(X5,X5,X5,X5),X5),
inference(scs_inference,[],[i_0_3586,i_0_3568,i_0_2261,i_0_3556,i_0_3548,i_0_3625,i_0_3599,i_0_3622,i_0_3580,i_0_3396,i_0_3564,i_0_3615,i_0_3135,i_0_3436,i_0_103,i_0_3657,i_0_3659,i_0_3661,i_0_3663,i_0_3272,i_0_467,i_0_82,i_0_74,i_0_65,i_0_68,i_0_64,i_0_62,i_0_63,i_0_67,i_0_66,i_0_88,i_0_95,i_0_97,i_0_96,i_0_94,i_0_58,i_0_57,i_0_89,i_0_73,i_0_56]) ).
cnf(c_0_3396,plain,
equidistant(X1,X2,extension(X3,X4,X5,X5),extension(X6,X4,X1,X2)),
i_0_2757 ).
cnf(c_0_3397,axiom,
X1 = extension(X2,X1,X3,X3),
i_0_77 ).
cnf(c_0_3398,axiom,
( equidistant(X1,X2,X3,X4)
| ~ equidistant(X1,X2,X5,X6)
| ~ equidistant(X5,X6,X3,X4) ),
i_0_57 ).
cnf(c_0_3399,plain,
equidistant(X1,X2,X3,extension(X4,X3,X1,X2)),
inference(rw,[status(thm)],[c_0_3396,c_0_3397]) ).
cnf(c_0_3400,plain,
equidistant(extension(X1,X2,w,x),extension(X2,X2,X2,X2),y,z),
i_0_2725 ).
cnf(c_0_3401,plain,
~ equidistant(extension(u,v,w,x),v,v,extension(u,v,y,z)),
i_0_3390 ).
cnf(c_0_3402,plain,
( equidistant(X1,X2,X3,extension(X4,X3,X5,X6))
| ~ equidistant(X1,X2,X5,X6) ),
inference(spm,[status(thm)],[c_0_3398,c_0_3399]) ).
cnf(c_0_3403,plain,
equidistant(extension(X1,X2,w,x),X2,y,z),
inference(rw,[status(thm)],[c_0_3400,c_0_3397]) ).
cnf(c_0_3404,plain,
$false,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_3401,c_0_3402]),c_0_3403])]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : GEO028-3 : TPTP v9.2.1. Released v1.0.0.
% 0.00/0.12 % Command : /export/starexec/sandbox/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox/solver/bin/cse --final-prover /export/starexec/sandbox/solver/bin/eprover --proof-time %d --global-time-limit %d
% 0.15/0.33 % Computer : n028.cluster.edu
% 0.15/0.33 % Model : x86_64 x86_64
% 0.15/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.33 % Memory : 8042.1875MB
% 0.15/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.15/0.33 % CPULimit : 300
% 0.15/0.33 % WCLimit : 300
% 0.15/0.33 % DateTime : Mon May 4 17:37:46 EDT 2026
% 0.15/0.33 % CPUTime :
% 0.15/0.34 % start to proof: theBenchmark
% 133.11/92.76 % Version : CSE_E---1.7
% 133.11/92.76 % Problem : theBenchmark.p
% 133.11/92.76 % SZS status Unsatisfiable for theBenchmark.p
% 133.11/92.76 % SZS output start CNFRefutation
% See solution above
% 138.43/98.10 % Total time : 92.379s
%------------------------------------------------------------------------------