%------------------------------------------------------------------------------
% File : CSE_E---1.7
% Problem : GEO003-1 : TPTP v9.2.1. Bugfixed v2.5.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 : n025.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:18:56 PM UTC 2026
% Result : Unsatisfiable 0.25s 1.61s
% Output : CNFRefutation 0.25s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.11 % Problem : GEO003-1 : TPTP v9.2.1. Bugfixed v2.5.0.
% 0.00/0.11 % 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.32 % Computer : n025.cluster.edu
% 0.15/0.32 % Model : x86_64 x86_64
% 0.15/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.32 % Memory : 8042.1875MB
% 0.15/0.32 % OS : Linux 3.10.0-693.el7.x86_64
% 0.15/0.32 % CPULimit : 300
% 0.15/0.32 % WCLimit : 300
% 0.15/0.32 % DateTime : Mon May 4 17:35:58 EDT 2026
% 0.15/0.33 % CPUTime :
% 0.15/0.34 % start to proof: theBenchmark
% 0.25/1.61 % Version : CSE_E---1.7
% 0.25/1.61 % Problem : theBenchmark.p
% 0.25/1.61 % SZS status Unsatisfiable for theBenchmark.p
% 0.25/1.61 % SZS output start CNFRefutation
% 0.25/1.61 cnf(continuity1, axiom, (equidistant(X1,X6,X1,continuous(X2,X6,X4,X3,X5,X1))|~equidistant(X1,X2,X1,X3)|~equidistant(X1,X4,X1,X5)|~between(X1,X2,X4)|~between(X2,X6,X4)), file('/export/starexec/sandbox/benchmark/Axioms/GEO001-0.ax', continuity1)).
% 0.25/1.61 cnf(continuity2, axiom, (between(X3,continuous(X2,X6,X4,X3,X5,X1),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/GEO001-0.ax', continuity2)).
% 0.25/1.61 cnf(euclid3, axiom, (X1=X2|between(euclid1(X3,X1,X4,X5,X2),X3,euclid2(X3,X1,X4,X5,X2))|~between(X1,X2,X3)|~between(X4,X2,X5)), file('/export/starexec/sandbox/benchmark/Axioms/GEO001-0.ax', euclid3)).
% 0.25/1.61 cnf(euclid2, axiom, (X1=X2|between(X1,X4,euclid2(X3,X1,X4,X5,X2))|~between(X1,X2,X3)|~between(X4,X2,X5)), file('/export/starexec/sandbox/benchmark/Axioms/GEO001-0.ax', euclid2)).
% 0.25/1.61 cnf(euclid1, axiom, (X1=X2|between(X1,X5,euclid1(X3,X1,X4,X5,X2))|~between(X1,X2,X3)|~between(X4,X2,X5)), file('/export/starexec/sandbox/benchmark/Axioms/GEO001-0.ax', euclid1)).
% 0.25/1.61 cnf(outer_pasch1, axiom, (between(X1,outer_pasch(X2,X1,X4,X5,X3),X4)|~between(X1,X2,X3)|~between(X4,X3,X5)), file('/export/starexec/sandbox/benchmark/Axioms/GEO001-0.ax', outer_pasch1)).
% 0.25/1.61 cnf(outer_pasch2, axiom, (between(X5,X2,outer_pasch(X2,X1,X4,X5,X3))|~between(X1,X2,X3)|~between(X4,X3,X5)), file('/export/starexec/sandbox/benchmark/Axioms/GEO001-0.ax', outer_pasch2)).
% 0.25/1.61 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/GEO001-0.ax', outer_five_segment)).
% 0.25/1.61 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/GEO001-0.ax', upper_dimension)).
% 0.25/1.61 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/GEO001-0.ax', transitivity_for_equidistance)).
% 0.25/1.61 cnf(segment_construction2, axiom, (equidistant(X1,extension(X2,X1,X3,X4),X3,X4)), file('/export/starexec/sandbox/benchmark/Axioms/GEO001-0.ax', segment_construction2)).
% 0.25/1.61 cnf(segment_construction1, axiom, (between(X1,X2,extension(X1,X2,X3,X4))), file('/export/starexec/sandbox/benchmark/Axioms/GEO001-0.ax', segment_construction1)).
% 0.25/1.61 cnf(identity_for_equidistance, axiom, (X1=X2|~equidistant(X1,X2,X3,X3)), file('/export/starexec/sandbox/benchmark/Axioms/GEO001-0.ax', identity_for_equidistance)).
% 0.25/1.61 cnf(connectivity_for_betweeness, axiom, (X1=X2|between(X1,X3,X4)|between(X1,X4,X3)|~between(X1,X2,X3)|~between(X1,X2,X4)), file('/export/starexec/sandbox/benchmark/Axioms/GEO001-0.ax', connectivity_for_betweeness)).
% 0.25/1.61 cnf(reflexivity_for_equidistance, axiom, (equidistant(X1,X2,X2,X1)), file('/export/starexec/sandbox/benchmark/Axioms/GEO001-0.ax', reflexivity_for_equidistance)).
% 0.25/1.61 cnf(transitivity_for_betweeness, axiom, (between(X1,X2,X4)|~between(X1,X2,X3)|~between(X2,X4,X3)), file('/export/starexec/sandbox/benchmark/Axioms/GEO001-0.ax', transitivity_for_betweeness)).
% 0.25/1.61 cnf(identity_for_betweeness, axiom, (X1=X2|~between(X1,X2,X1)), file('/export/starexec/sandbox/benchmark/Axioms/GEO001-0.ax', identity_for_betweeness)).
% 0.25/1.61 cnf(prove_b_between_a_and_b, negated_conjecture, (~between(a,b,b)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', prove_b_between_a_and_b)).
% 0.25/1.61 cnf(lower_dimension3, axiom, (~between(lower_dimension_point_3,lower_dimension_point_1,lower_dimension_point_2)), file('/export/starexec/sandbox/benchmark/Axioms/GEO001-0.ax', lower_dimension3)).
% 0.25/1.61 cnf(lower_dimension2, axiom, (~between(lower_dimension_point_2,lower_dimension_point_3,lower_dimension_point_1)), file('/export/starexec/sandbox/benchmark/Axioms/GEO001-0.ax', lower_dimension2)).
% 0.25/1.61 cnf(lower_dimension1, axiom, (~between(lower_dimension_point_1,lower_dimension_point_2,lower_dimension_point_3)), file('/export/starexec/sandbox/benchmark/Axioms/GEO001-0.ax', lower_dimension1)).
% 0.25/1.61 cnf(i_0_21, axiom, (equidistant(X1,X6,X1,continuous(X2,X6,X4,X3,X5,X1))|~equidistant(X1,X2,X1,X3)|~equidistant(X1,X4,X1,X5)|~between(X1,X2,X4)|~between(X2,X6,X4)), continuity1, ['final']).
% 0.25/1.61 cnf(i_0_22, axiom, (between(X3,continuous(X2,X6,X4,X3,X5,X1),X5)|~equidistant(X1,X2,X1,X3)|~equidistant(X1,X4,X1,X5)|~between(X1,X2,X4)|~between(X2,X6,X4)), continuity2, ['final']).
% 0.25/1.61 cnf(i_0_23, axiom, (X1=X2|between(euclid1(X3,X1,X4,X5,X2),X3,euclid2(X3,X1,X4,X5,X2))|~between(X1,X2,X3)|~between(X4,X2,X5)), euclid3, ['final']).
% 0.25/1.61 cnf(i_0_24, axiom, (X1=X2|between(X1,X4,euclid2(X3,X1,X4,X5,X2))|~between(X1,X2,X3)|~between(X4,X2,X5)), euclid2, ['final']).
% 0.25/1.61 cnf(i_0_25, axiom, (X1=X2|between(X1,X5,euclid1(X3,X1,X4,X5,X2))|~between(X1,X2,X3)|~between(X4,X2,X5)), euclid1, ['final']).
% 0.25/1.61 cnf(i_0_26, axiom, (between(X1,outer_pasch(X2,X1,X4,X5,X3),X4)|~between(X1,X2,X3)|~between(X4,X3,X5)), outer_pasch1, ['final']).
% 0.25/1.61 cnf(i_0_27, axiom, (between(X5,X2,outer_pasch(X2,X1,X4,X5,X3))|~between(X1,X2,X3)|~between(X4,X3,X5)), outer_pasch2, ['final']).
% 0.25/1.61 cnf(i_0_28, 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']).
% 0.25/1.61 cnf(i_0_29, 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']).
% 0.25/1.61 cnf(i_0_30, axiom, (equidistant(X3,X4,X5,X6)|~equidistant(X1,X2,X3,X4)|~equidistant(X1,X2,X5,X6)), transitivity_for_equidistance, ['final']).
% 0.25/1.61 cnf(i_0_31, axiom, (equidistant(X1,extension(X2,X1,X3,X4),X3,X4)), segment_construction2, ['final']).
% 0.25/1.61 cnf(i_0_32, axiom, (between(X1,X2,extension(X1,X2,X3,X4))), segment_construction1, ['final']).
% 0.25/1.61 cnf(i_0_33, axiom, (X1=X2|~equidistant(X1,X2,X3,X3)), identity_for_equidistance, ['final']).
% 0.25/1.61 cnf(i_0_34, axiom, (X1=X2|between(X1,X3,X4)|between(X1,X4,X3)|~between(X1,X2,X3)|~between(X1,X2,X4)), connectivity_for_betweeness, ['final']).
% 0.25/1.61 cnf(i_0_35, axiom, (equidistant(X1,X2,X2,X1)), reflexivity_for_equidistance, ['final']).
% 0.25/1.61 cnf(i_0_36, axiom, (between(X1,X2,X4)|~between(X1,X2,X3)|~between(X2,X4,X3)), transitivity_for_betweeness, ['final']).
% 0.25/1.61 cnf(i_0_37, axiom, (X1=X2|~between(X1,X2,X1)), identity_for_betweeness, ['final']).
% 0.25/1.61 cnf(i_0_38, negated_conjecture, (~between(a,b,b)), prove_b_between_a_and_b, ['final']).
% 0.25/1.61 cnf(i_0_39, axiom, (~between(lower_dimension_point_3,lower_dimension_point_1,lower_dimension_point_2)), lower_dimension3, ['final']).
% 0.25/1.61 cnf(i_0_40, axiom, (~between(lower_dimension_point_2,lower_dimension_point_3,lower_dimension_point_1)), lower_dimension2, ['final']).
% 0.25/1.61 cnf(i_0_41, axiom, (~between(lower_dimension_point_1,lower_dimension_point_2,lower_dimension_point_3)), lower_dimension1, ['final']).
% 0.25/1.61 cnf(i_0_42, axiom, (X1=X1)).
% 0.25/1.61 cnf(i_0_43, axiom, (X1=X2|X2!=X1)).
% 0.25/1.61 cnf(i_0_44, axiom, (X1=X2|X1!=X3|X3!=X2)).
% 0.25/1.61 cnf(i_0_45, axiom, (X1!=X2|~equidistant(X1,X3,X4,X5)|equidistant(X2,X3,X4,X5))).
% 0.25/1.61 cnf(i_0_46, axiom, (X1!=X2|~equidistant(X3,X1,X4,X5)|equidistant(X3,X2,X4,X5))).
% 0.25/1.61 cnf(i_0_47, axiom, (X1!=X2|~equidistant(X3,X4,X1,X5)|equidistant(X3,X4,X2,X5))).
% 0.25/1.61 cnf(i_0_48, axiom, (X1!=X2|~equidistant(X3,X4,X5,X1)|equidistant(X3,X4,X5,X2))).
% 0.25/1.61 cnf(i_0_49, axiom, (X1!=X2|~between(X1,X3,X4)|between(X2,X3,X4))).
% 0.25/1.61 cnf(i_0_50, axiom, (X1!=X2|~between(X3,X1,X4)|between(X3,X2,X4))).
% 0.25/1.61 cnf(i_0_51, axiom, (X1!=X2|~between(X3,X4,X1)|between(X3,X4,X2))).
% 0.25/1.66 cnf(i_0_42, axiom, (X1=X1)).
% 0.25/1.66 cnf(i_0_43, axiom, (X1=X2|X2!=X1)).
% 0.25/1.66 cnf(i_0_44, axiom, (X1=X2|X1!=X3|X3!=X2)).
% 0.25/1.66 cnf(i_0_45, axiom, (X1!=X2|~equidistant(X1,X3,X4,X5)|equidistant(X2,X3,X4,X5))).
% 0.25/1.66 cnf(i_0_46, axiom, (X1!=X2|~equidistant(X3,X1,X4,X5)|equidistant(X3,X2,X4,X5))).
% 0.25/1.66 cnf(i_0_47, axiom, (X1!=X2|~equidistant(X3,X4,X1,X5)|equidistant(X3,X4,X2,X5))).
% 0.25/1.66 cnf(i_0_48, axiom, (X1!=X2|~equidistant(X3,X4,X5,X1)|equidistant(X3,X4,X5,X2))).
% 0.25/1.66 cnf(i_0_49, axiom, (X1!=X2|~between(X1,X3,X4)|between(X2,X3,X4))).
% 0.25/1.66 cnf(i_0_50, axiom, (X1!=X2|~between(X3,X1,X4)|between(X3,X2,X4))).
% 0.25/1.66 cnf(i_0_51, axiom, (X1!=X2|~between(X3,X4,X1)|between(X3,X4,X2))).
% 0.25/1.66 cnf(i_0_52, plain, (X1=extension(X2,X1,X3,X3)), inference(scs_inference,[],[i_0_31,i_0_33])).
% 0.25/1.66 cnf(i_0_53, plain, (equidistant(X1,extension(X2,X1,X3,X4),X3,X4)), inference(rename_variables,[],[i_0_31])).
% 0.25/1.66 cnf(i_0_54, plain, (~equidistant(X1,X2,X3,X3)|X1=X2), inference(rename_variables,[],[i_0_33])).
% 0.25/1.66 cnf(i_0_55, plain, (extension(X1,X2,X3,X3)=X2), inference(scs_inference,[],[i_0_31,i_0_33,i_0_43])).
% 0.25/1.66 cnf(i_0_56, plain, (~between(a,b,extension(b,b,X1,X2))), inference(scs_inference,[],[i_0_38,i_0_31,i_0_32,i_0_33,i_0_43,i_0_36])).
% 0.25/1.66 cnf(i_0_57, plain, (between(X1,X2,extension(X1,X2,X3,X4))), inference(rename_variables,[],[i_0_32])).
% 0.25/1.66 cnf(i_0_58, plain, (~between(X1,X2,X3)|between(X4,X1,X2)|~between(X4,X1,X3)), inference(rename_variables,[],[i_0_36])).
% 0.25/1.66 cnf(i_0_59, plain, (~between(extension(X1,a,X2,X2),b,b)), inference(scs_inference,[],[i_0_38,i_0_31,i_0_32,i_0_33,i_0_43,i_0_36,i_0_49])).
% 0.25/1.66 cnf(i_0_60, plain, (equidistant(X1,X2,X1,X2)), inference(scs_inference,[],[i_0_38,i_0_35,i_0_31,i_0_32,i_0_33,i_0_43,i_0_36,i_0_49,i_0_30])).
% 0.25/1.66 cnf(i_0_61, plain, (~equidistant(X1,X2,X3,X4)|equidistant(X5,X6,X3,X4)|~equidistant(X1,X2,X5,X6)), inference(rename_variables,[],[i_0_30])).
% 0.25/1.66 cnf(i_0_62, plain, (extension(a,b,X1,X2)!=b), inference(scs_inference,[],[i_0_38,i_0_35,i_0_31,i_0_32,i_0_57,i_0_33,i_0_43,i_0_36,i_0_49,i_0_30,i_0_51])).
% 0.25/1.66 cnf(i_0_63, plain, (between(X1,X2,extension(X1,X2,X3,X4))), inference(rename_variables,[],[i_0_32])).
% 0.25/1.66 cnf(i_0_64, plain, (X1!=b|~between(a,X1,b)), inference(scs_inference,[],[i_0_38,i_0_35,i_0_31,i_0_32,i_0_57,i_0_33,i_0_43,i_0_36,i_0_49,i_0_30,i_0_51,i_0_50])).
% 0.25/1.66 cnf(i_0_65, plain, (between(X1,X2,X3)|~between(X1,X4,X3)|~between(X1,X4,X2)|X1=X4|between(X1,X3,X2)), inference(rename_variables,[],[i_0_34])).
% 0.25/1.66 cnf(i_0_66, plain, (equidistant(X1,X2,X2,X1)), inference(rename_variables,[],[i_0_35])).
% 0.25/1.66 cnf(i_0_67, plain, (equidistant(X1,extension(X2,X1,X3,X4),X3,X4)), inference(rename_variables,[],[i_0_31])).
% 0.25/1.66 cnf(i_0_68, plain, (between(X1,X2,extension(X1,X2,X3,X4))), inference(rename_variables,[],[i_0_32])).
% 0.25/1.66 cnf(i_0_69, plain, (between(X1,X2,extension(X1,X2,X3,X4))), inference(rename_variables,[],[i_0_32])).
% 0.25/1.66 cnf(i_0_70, plain, (a=continuous(a,a,extension(a,a,a,b),a,b,a)|~between(a,lower_dimension_point_3,b)), inference(scs_inference,[],[i_0_38,i_0_35,i_0_31,i_0_53,i_0_32,i_0_57,i_0_63,i_0_39,i_0_33,i_0_43,i_0_36,i_0_49,i_0_30,i_0_51,i_0_50,i_0_65,i_0_22])).
% 0.25/1.66 cnf(i_0_71, plain, (~between(a,b,b)), inference(equality_inference,[],[64])).
% 0.25/1.67 cnf(i_0_72,plain, ($false), inference(scs_inference,[],[i_0+55, i_0_62]), ['proof']).
% 0.25/1.67 % SZS output end CNFRefutation
% 0.25/1.67 % Total time : 1.270s
%------------------------------------------------------------------------------