%------------------------------------------------------------------------------
% File : CSE_E---1.7
% Problem : GEO003-2 : 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 : n027.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.21s 1.81s
% Output : CNFRefutation 0.21s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.10/0.26 % Problem : GEO003-2 : TPTP v9.2.1. Released v1.0.0.
% 0.10/0.26 % 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.13/0.50 % Computer : n027.cluster.edu
% 0.13/0.50 % Model : x86_64 x86_64
% 0.13/0.50 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.50 % Memory : 8042.1875MB
% 0.13/0.50 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.50 % CPULimit : 300
% 0.13/0.50 % WCLimit : 300
% 0.13/0.50 % DateTime : Mon May 4 17:36:05 EDT 2026
% 0.13/0.50 % CPUTime :
% 0.13/0.51 % start to proof: theBenchmark
% 0.21/1.81 % Version : CSE_E---1.7
% 0.21/1.81 % Problem : theBenchmark.p
% 0.21/1.81 % SZS status Unsatisfiable for theBenchmark.p
% 0.21/1.81 % SZS output start CNFRefutation
% 0.21/1.81 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)).
% 0.21/1.81 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)).
% 0.21/1.81 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)).
% 0.21/1.81 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)).
% 0.21/1.81 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)).
% 0.21/1.81 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)).
% 0.21/1.81 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)).
% 0.21/1.81 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)).
% 0.21/1.81 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)).
% 0.21/1.81 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)).
% 0.21/1.81 cnf(segment_construction2, axiom, (equidistant(X1,extension(X2,X1,X3,X4),X3,X4)), file('/export/starexec/sandbox/benchmark/Axioms/GEO002-0.ax', segment_construction2)).
% 0.21/1.81 cnf(segment_construction1, axiom, (between(X1,X2,extension(X1,X2,X3,X4))), file('/export/starexec/sandbox/benchmark/Axioms/GEO002-0.ax', segment_construction1)).
% 0.21/1.81 cnf(identity_for_equidistance, axiom, (X1=X2|~equidistant(X1,X2,X3,X3)), file('/export/starexec/sandbox/benchmark/Axioms/GEO002-0.ax', identity_for_equidistance)).
% 0.21/1.81 cnf(reflexivity_for_equidistance, axiom, (equidistant(X1,X2,X2,X1)), file('/export/starexec/sandbox/benchmark/Axioms/GEO002-0.ax', reflexivity_for_equidistance)).
% 0.21/1.81 cnf(identity_for_betweeness, axiom, (X1=X2|~between(X1,X2,X1)), file('/export/starexec/sandbox/benchmark/Axioms/GEO002-0.ax', identity_for_betweeness)).
% 0.21/1.81 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.21/1.81 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)).
% 0.21/1.81 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)).
% 0.21/1.81 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)).
% 0.21/1.81 cnf(i_0_19, 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']).
% 0.21/1.81 cnf(i_0_20, 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']).
% 0.21/1.81 cnf(i_0_21, 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']).
% 0.21/1.81 cnf(i_0_22, axiom, (X1=X2|between(X1,X4,euclid1(X1,X4,X2,X5,X3))|~between(X1,X2,X3)|~between(X4,X2,X5)), euclid1, ['final']).
% 0.21/1.81 cnf(i_0_23, axiom, (X1=X2|between(X1,X5,euclid2(X1,X4,X2,X5,X3))|~between(X1,X2,X3)|~between(X4,X2,X5)), euclid2, ['final']).
% 0.21/1.81 cnf(i_0_24, axiom, (between(X2,inner_pasch(X1,X2,X3,X5,X4),X4)|~between(X1,X2,X3)|~between(X4,X5,X3)), inner_pasch1, ['final']).
% 0.21/1.81 cnf(i_0_25, axiom, (between(X5,inner_pasch(X1,X2,X3,X5,X4),X1)|~between(X1,X2,X3)|~between(X4,X5,X3)), inner_pasch2, ['final']).
% 0.21/1.81 cnf(i_0_26, 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.21/1.81 cnf(i_0_27, 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.21/1.81 cnf(i_0_28, axiom, (equidistant(X3,X4,X5,X6)|~equidistant(X1,X2,X3,X4)|~equidistant(X1,X2,X5,X6)), transitivity_for_equidistance, ['final']).
% 0.21/1.81 cnf(i_0_29, axiom, (equidistant(X1,extension(X2,X1,X3,X4),X3,X4)), segment_construction2, ['final']).
% 0.21/1.81 cnf(i_0_30, axiom, (between(X1,X2,extension(X1,X2,X3,X4))), segment_construction1, ['final']).
% 0.21/1.81 cnf(i_0_31, axiom, (X1=X2|~equidistant(X1,X2,X3,X3)), identity_for_equidistance, ['final']).
% 0.21/1.81 cnf(i_0_32, axiom, (equidistant(X1,X2,X2,X1)), reflexivity_for_equidistance, ['final']).
% 0.21/1.81 cnf(i_0_33, axiom, (X1=X2|~between(X1,X2,X1)), identity_for_betweeness, ['final']).
% 0.21/1.81 cnf(i_0_34, negated_conjecture, (~between(a,b,b)), prove_b_between_a_and_b, ['final']).
% 0.21/1.81 cnf(i_0_35, axiom, (~between(lower_dimension_point_3,lower_dimension_point_1,lower_dimension_point_2)), lower_dimension3, ['final']).
% 0.21/1.81 cnf(i_0_36, axiom, (~between(lower_dimension_point_2,lower_dimension_point_3,lower_dimension_point_1)), lower_dimension2, ['final']).
% 0.21/1.81 cnf(i_0_37, axiom, (~between(lower_dimension_point_1,lower_dimension_point_2,lower_dimension_point_3)), lower_dimension1, ['final']).
% 0.21/1.81 cnf(i_0_38, axiom, (X1=X1)).
% 0.21/1.81 cnf(i_0_39, axiom, (X1=X2|X2!=X1)).
% 0.21/1.81 cnf(i_0_40, axiom, (X1=X2|X1!=X3|X3!=X2)).
% 0.21/1.81 cnf(i_0_41, axiom, (X1!=X2|~equidistant(X1,X3,X4,X5)|equidistant(X2,X3,X4,X5))).
% 0.21/1.81 cnf(i_0_42, axiom, (X1!=X2|~equidistant(X3,X1,X4,X5)|equidistant(X3,X2,X4,X5))).
% 0.21/1.81 cnf(i_0_43, axiom, (X1!=X2|~equidistant(X3,X4,X1,X5)|equidistant(X3,X4,X2,X5))).
% 0.21/1.81 cnf(i_0_44, axiom, (X1!=X2|~equidistant(X3,X4,X5,X1)|equidistant(X3,X4,X5,X2))).
% 0.21/1.81 cnf(i_0_45, axiom, (X1!=X2|~between(X1,X3,X4)|between(X2,X3,X4))).
% 0.21/1.81 cnf(i_0_46, axiom, (X1!=X2|~between(X3,X1,X4)|between(X3,X2,X4))).
% 0.21/1.81 cnf(i_0_47, axiom, (X1!=X2|~between(X3,X4,X1)|between(X3,X4,X2))).
% 0.21/1.84 cnf(i_0_38, axiom, (X1=X1)).
% 0.21/1.84 cnf(i_0_39, axiom, (X1=X2|X2!=X1)).
% 0.21/1.84 cnf(i_0_40, axiom, (X1=X2|X1!=X3|X3!=X2)).
% 0.21/1.84 cnf(i_0_41, axiom, (X1!=X2|~equidistant(X1,X3,X4,X5)|equidistant(X2,X3,X4,X5))).
% 0.21/1.84 cnf(i_0_42, axiom, (X1!=X2|~equidistant(X3,X1,X4,X5)|equidistant(X3,X2,X4,X5))).
% 0.21/1.84 cnf(i_0_43, axiom, (X1!=X2|~equidistant(X3,X4,X1,X5)|equidistant(X3,X4,X2,X5))).
% 0.21/1.84 cnf(i_0_44, axiom, (X1!=X2|~equidistant(X3,X4,X5,X1)|equidistant(X3,X4,X5,X2))).
% 0.21/1.84 cnf(i_0_45, axiom, (X1!=X2|~between(X1,X3,X4)|between(X2,X3,X4))).
% 0.21/1.84 cnf(i_0_46, axiom, (X1!=X2|~between(X3,X1,X4)|between(X3,X2,X4))).
% 0.21/1.84 cnf(i_0_47, axiom, (X1!=X2|~between(X3,X4,X1)|between(X3,X4,X2))).
% 0.21/1.84 cnf(i_0_48, plain, (X1=extension(X2,X1,X3,X3)), inference(scs_inference,[],[i_0_29,i_0_31])).
% 0.21/1.84 cnf(i_0_49, plain, (equidistant(X1,extension(X2,X1,X3,X4),X3,X4)), inference(rename_variables,[],[i_0_29])).
% 0.21/1.84 cnf(i_0_50, plain, (~equidistant(X1,X2,X3,X3)|X1=X2), inference(rename_variables,[],[i_0_31])).
% 0.21/1.84 cnf(i_0_51, plain, (extension(X1,X2,X3,X3)=X2), inference(scs_inference,[],[i_0_29,i_0_31,i_0_39])).
% 0.21/1.84 cnf(i_0_52, plain, (~between(extension(X1,a,X2,X2),b,b)), inference(scs_inference,[],[i_0_34,i_0_29,i_0_31,i_0_39,i_0_45])).
% 0.21/1.84 cnf(i_0_53, plain, (equidistant(X1,X2,X1,X2)), inference(scs_inference,[],[i_0_34,i_0_32,i_0_29,i_0_31,i_0_39,i_0_45,i_0_28])).
% 0.21/1.84 cnf(i_0_54, plain, (~equidistant(X1,X2,X3,X4)|equidistant(X5,X6,X3,X4)|~equidistant(X1,X2,X5,X6)), inference(rename_variables,[],[i_0_28])).
% 0.21/1.84 cnf(i_0_55, plain, (extension(a,b,X1,X2)!=b), inference(scs_inference,[],[i_0_34,i_0_32,i_0_29,i_0_30,i_0_31,i_0_39,i_0_45,i_0_28,i_0_47])).
% 0.21/1.84 cnf(i_0_56, plain, (between(X1,X2,extension(X1,X2,X3,X4))), inference(rename_variables,[],[i_0_30])).
% 0.21/1.84 cnf(i_0_57, plain, (X1!=b|~between(a,X1,b)), inference(scs_inference,[],[i_0_34,i_0_32,i_0_29,i_0_30,i_0_31,i_0_39,i_0_45,i_0_28,i_0_47,i_0_46])).
% 0.21/1.84 cnf(i_0_58, plain, (equidistant(X1,X2,X2,X1)), inference(rename_variables,[],[i_0_32])).
% 0.21/1.84 cnf(i_0_59, plain, (equidistant(X1,X2,X2,X1)), inference(rename_variables,[],[i_0_32])).
% 0.21/1.84 cnf(i_0_60, plain, (equidistant(X1,X2,X2,X1)), inference(rename_variables,[],[i_0_32])).
% 0.21/1.84 cnf(i_0_61, plain, (between(X1,X2,extension(X1,X2,X3,X4))), inference(rename_variables,[],[i_0_30])).
% 0.21/1.84 cnf(i_0_62, plain, (~equidistant(X1,X2,X3,X4)|~equidistant(X5,X6,X7,X8)|~equidistant(X1,X6,X3,X8)|~between(X5,X1,X2)|~between(X7,X3,X4)|X5=X1|equidistant(X2,X6,X4,X8)|~equidistant(X5,X1,X7,X3)), inference(rename_variables,[],[i_0_26])).
% 0.21/1.84 cnf(i_0_64, plain, (~between(a,b,b)), inference(equality_inference,[],[57])).
% 0.21/1.84 cnf(i_0_65,plain, ($false), inference(scs_inference,[],[i_0+51, i_0_55]), ['proof']).
% 0.21/1.84 % SZS output end CNFRefutation
% 0.21/1.84 % Total time : 1.284s
%------------------------------------------------------------------------------