%------------------------------------------------------------------------------
% File : CSE_E---1.7
% Problem : GEO118+1 : TPTP v9.2.1. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox2/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox2/solver/bin/cse --final-prover /export/starexec/sandbox2/solver/bin/eprover --proof-time %d --global-time-limit %d
% Computer : n006.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:21 PM UTC 2026
% Result : Theorem 0.32s 1.62s
% Output : CNFRefutation 0.32s
% Verified :
% SZS Type : ERROR: Analysing output (Could not find formula named 87)
% Comments :
%------------------------------------------------------------------------------
fof(inner_point_defn,axiom,
! [X3,X1] :
( inner_point(X3,X1)
<=> ( incident_c(X3,X1)
& ~ end_point(X3,X1) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO004+0.ax',inner_point_defn) ).
fof(theorem_4_5,conjecture,
! [X9,X3,X5] :
( ordered_by(X9,X3,X5)
=> ~ ordered_by(X9,X5,X3) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',theorem_4_5) ).
fof(o3,axiom,
! [X3,X5,X7,X9] :
( between_o(X9,X3,X5,X7)
<=> ? [X1] :
( ! [X3] :
( incident_o(X3,X9)
<=> incident_c(X3,X1) )
& between_c(X1,X3,X5,X7) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO004+2.ax',o3) ).
fof(between_c_defn,axiom,
! [X1,X3,X5,X7] :
( between_c(X1,X3,X5,X7)
<=> ( X3 != X7
& ? [X8] :
( part_of(X8,X1)
& end_point(X3,X8)
& end_point(X7,X8)
& inner_point(X5,X8) ) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO004+1.ax',between_c_defn) ).
fof(between_o_defn,axiom,
! [X9,X3,X5,X7] :
( between_o(X9,X3,X5,X7)
<=> ( ( ordered_by(X9,X3,X5)
& ordered_by(X9,X5,X7) )
| ( ordered_by(X9,X7,X5)
& ordered_by(X9,X5,X3) ) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO004+2.ax',between_o_defn) ).
fof(meet_defn,axiom,
! [X3,X1,X2] :
( meet(X3,X1,X2)
<=> ( incident_c(X3,X1)
& incident_c(X3,X2)
& ! [X5] :
( ( incident_c(X5,X1)
& incident_c(X5,X2) )
=> ( end_point(X5,X1)
& end_point(X5,X2) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO004+0.ax',meet_defn) ).
fof(sum_defn,axiom,
! [X1,X2,X4] :
( X1 = sum(X2,X4)
<=> ! [X5] :
( incident_c(X5,X1)
<=> ( incident_c(X5,X2)
| incident_c(X5,X4) ) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO004+0.ax',sum_defn) ).
fof(o6,axiom,
! [X10,X11] :
( ! [X3,X5] :
( ordered_by(X10,X3,X5)
<=> ordered_by(X11,X3,X5) )
=> X10 = X11 ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO004+2.ax',o6) ).
fof(o5,axiom,
! [X3,X5,X1] :
( ( open(X1)
& X3 != X5
& incident_c(X3,X1)
& incident_c(X5,X1) )
=> ? [X9] :
( ! [X7] :
( incident_o(X7,X9)
<=> incident_c(X7,X1) )
& ordered_by(X9,X3,X5) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO004+2.ax',o5) ).
fof(c2,axiom,
! [X1,X2,X4,X6] :
( ( part_of(X2,X1)
& part_of(X4,X1)
& part_of(X6,X1)
& ? [X3] :
( end_point(X3,X2)
& end_point(X3,X4)
& end_point(X3,X6) ) )
=> ( part_of(X4,X6)
| part_of(X6,X4)
| part_of(X2,X4)
| part_of(X4,X2)
| part_of(X2,X6)
| part_of(X6,X2) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO004+0.ax',c2) ).
fof(c7,axiom,
! [X1,X2,X4,X3] :
( ( closed(X1)
& meet(X3,X2,X4)
& X1 = sum(X2,X4) )
=> ! [X5] :
( end_point(X5,X2)
=> meet(X5,X2,X4) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO004+0.ax',c7) ).
fof(finish_point_defn,axiom,
! [X3,X9] :
( finish_point(X3,X9)
<=> ( incident_o(X3,X9)
& ! [X5] :
( ( X3 != X5
& incident_o(X5,X9) )
=> ordered_by(X9,X5,X3) ) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO004+2.ax',finish_point_defn) ).
fof(start_point_defn,axiom,
! [X3,X9] :
( start_point(X3,X9)
<=> ( incident_o(X3,X9)
& ! [X5] :
( ( X3 != X5
& incident_o(X5,X9) )
=> ordered_by(X9,X3,X5) ) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO004+2.ax',start_point_defn) ).
fof(end_point_defn,axiom,
! [X3,X1] :
( end_point(X3,X1)
<=> ( incident_c(X3,X1)
& ! [X2,X4] :
( ( part_of(X2,X1)
& part_of(X4,X1)
& incident_c(X3,X2)
& incident_c(X3,X4) )
=> ( part_of(X2,X4)
| part_of(X4,X2) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO004+0.ax',end_point_defn) ).
fof(underlying_curve_defn,axiom,
! [X1,X9] :
( X1 = underlying_curve(X9)
<=> ! [X3] :
( incident_o(X3,X9)
<=> incident_c(X3,X1) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO004+2.ax',underlying_curve_defn) ).
fof(c4,axiom,
! [X1,X3] :
( inner_point(X3,X1)
=> ? [X2,X4] :
( meet(X3,X2,X4)
& X1 = sum(X2,X4) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO004+0.ax',c4) ).
fof(c9,axiom,
! [X1,X2] :
( ! [X3] :
( incident_c(X3,X1)
<=> incident_c(X3,X2) )
=> X1 = X2 ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO004+0.ax',c9) ).
fof(c8,axiom,
! [X2,X4] :
( ? [X3] : meet(X3,X2,X4)
=> ? [X1] : X1 = sum(X2,X4) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO004+0.ax',c8) ).
fof(o1,axiom,
! [X9,X3,X5] :
( ordered_by(X9,X3,X5)
=> ( incident_o(X3,X9)
& incident_o(X5,X9) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO004+2.ax',o1) ).
fof(part_of_defn,axiom,
! [X1,X2] :
( part_of(X2,X1)
<=> ! [X3] :
( incident_c(X3,X2)
=> incident_c(X3,X1) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO004+0.ax',part_of_defn) ).
fof(c5,axiom,
! [X1,X3,X5,X7] :
( ( end_point(X3,X1)
& end_point(X5,X1)
& end_point(X7,X1) )
=> ( X3 = X5
| X3 = X7
| X5 = X7 ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO004+0.ax',c5) ).
fof(c6,axiom,
! [X1,X3] :
( end_point(X3,X1)
=> ? [X5] :
( end_point(X5,X1)
& X3 != X5 ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO004+0.ax',c6) ).
fof(o2,axiom,
! [X9] :
? [X1] :
( open(X1)
& ! [X3] :
( incident_o(X3,X9)
<=> incident_c(X3,X1) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO004+2.ax',o2) ).
fof(closed_defn,axiom,
! [X1] :
( closed(X1)
<=> ~ ? [X3] : end_point(X3,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO004+0.ax',closed_defn) ).
fof(c1,axiom,
! [X1,X2] :
( ( part_of(X2,X1)
& X2 != X1 )
=> open(X2) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO004+0.ax',c1) ).
fof(open_defn,axiom,
! [X1] :
( open(X1)
<=> ? [X3] : end_point(X3,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO004+0.ax',open_defn) ).
fof(o4,axiom,
! [X9] :
? [X3] : start_point(X3,X9),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO004+2.ax',o4) ).
fof(c3,axiom,
! [X1] :
? [X3] : inner_point(X3,X1),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO004+0.ax',c3) ).
fof(i_0_28,plain,
! [X3,X1] :
( inner_point(X3,X1)
<=> ( incident_c(X3,X1)
& ~ end_point(X3,X1) ) ),
inference(fof_simplification,[status(thm)],[inner_point_defn]) ).
fof(i_0_29,negated_conjecture,
~ ! [X9,X3,X5] :
( ordered_by(X9,X3,X5)
=> ~ ordered_by(X9,X5,X3) ),
inference(fof_simplification,[status(thm)],[inference(assume_negation,[status(cth)],[theorem_4_5])]) ).
fof(i_0_30,plain,
! [X215,X216,X217,X218,X220,X221,X222,X223,X224,X225,X226] :
( ( ~ incident_o(X220,X218)
| incident_c(X220,esk18_4(X215,X216,X217,X218))
| ~ between_o(X218,X215,X216,X217) )
& ( ~ incident_c(X221,esk18_4(X215,X216,X217,X218))
| incident_o(X221,X218)
| ~ between_o(X218,X215,X216,X217) )
& ( between_c(esk18_4(X215,X216,X217,X218),X215,X216,X217)
| ~ between_o(X218,X215,X216,X217) )
& ( ~ incident_o(esk19_5(X222,X223,X224,X225,X226),X225)
| ~ incident_c(esk19_5(X222,X223,X224,X225,X226),X226)
| ~ between_c(X226,X222,X223,X224)
| between_o(X225,X222,X223,X224) )
& ( incident_o(esk19_5(X222,X223,X224,X225,X226),X225)
| incident_c(esk19_5(X222,X223,X224,X225,X226),X226)
| ~ between_c(X226,X222,X223,X224)
| between_o(X225,X222,X223,X224) ) ),
inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(fof_nnf,[status(thm)],[o3])])])])])]) ).
fof(i_0_31,plain,
! [X182,X183,X184,X185,X187,X188,X189,X190,X191] :
( ( X183 != X185
| ~ between_c(X182,X183,X184,X185) )
& ( part_of(esk14_4(X182,X183,X184,X185),X182)
| ~ between_c(X182,X183,X184,X185) )
& ( end_point(X183,esk14_4(X182,X183,X184,X185))
| ~ between_c(X182,X183,X184,X185) )
& ( end_point(X185,esk14_4(X182,X183,X184,X185))
| ~ between_c(X182,X183,X184,X185) )
& ( inner_point(X184,esk14_4(X182,X183,X184,X185))
| ~ between_c(X182,X183,X184,X185) )
& ( X188 = X190
| ~ part_of(X191,X187)
| ~ end_point(X188,X191)
| ~ end_point(X190,X191)
| ~ inner_point(X189,X191)
| between_c(X187,X188,X189,X190) ) ),
inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(fof_nnf,[status(thm)],[between_c_defn])])])])])]) ).
fof(i_0_32,plain,
! [X192,X193,X194,X195] :
( ( ordered_by(X192,X195,X194)
| ordered_by(X192,X193,X194)
| ~ between_o(X192,X193,X194,X195) )
& ( ordered_by(X192,X194,X193)
| ordered_by(X192,X193,X194)
| ~ between_o(X192,X193,X194,X195) )
& ( ordered_by(X192,X195,X194)
| ordered_by(X192,X194,X195)
| ~ between_o(X192,X193,X194,X195) )
& ( ordered_by(X192,X194,X193)
| ordered_by(X192,X194,X195)
| ~ between_o(X192,X193,X194,X195) )
& ( ~ ordered_by(X192,X193,X194)
| ~ ordered_by(X192,X194,X195)
| between_o(X192,X193,X194,X195) )
& ( ~ ordered_by(X192,X195,X194)
| ~ ordered_by(X192,X194,X193)
| between_o(X192,X193,X194,X195) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[between_o_defn])])]) ).
fof(i_0_33,plain,
! [X134,X135,X136,X137,X138,X139,X140] :
( ( incident_c(X134,X135)
| ~ meet(X134,X135,X136) )
& ( incident_c(X134,X136)
| ~ meet(X134,X135,X136) )
& ( end_point(X137,X135)
| ~ incident_c(X137,X135)
| ~ incident_c(X137,X136)
| ~ meet(X134,X135,X136) )
& ( end_point(X137,X136)
| ~ incident_c(X137,X135)
| ~ incident_c(X137,X136)
| ~ meet(X134,X135,X136) )
& ( incident_c(esk5_3(X138,X139,X140),X139)
| ~ incident_c(X138,X139)
| ~ incident_c(X138,X140)
| meet(X138,X139,X140) )
& ( incident_c(esk5_3(X138,X139,X140),X140)
| ~ incident_c(X138,X139)
| ~ incident_c(X138,X140)
| meet(X138,X139,X140) )
& ( ~ end_point(esk5_3(X138,X139,X140),X139)
| ~ end_point(esk5_3(X138,X139,X140),X140)
| ~ incident_c(X138,X139)
| ~ incident_c(X138,X140)
| meet(X138,X139,X140) ) ),
inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(fof_nnf,[status(thm)],[meet_defn])])])])])]) ).
fof(i_0_34,plain,
! [X115,X116,X117,X118,X119,X120,X121,X122] :
( ( ~ incident_c(X118,X115)
| incident_c(X118,X116)
| incident_c(X118,X117)
| X115 != sum(X116,X117) )
& ( ~ incident_c(X119,X116)
| incident_c(X119,X115)
| X115 != sum(X116,X117) )
& ( ~ incident_c(X119,X117)
| incident_c(X119,X115)
| X115 != sum(X116,X117) )
& ( ~ incident_c(esk2_3(X120,X121,X122),X121)
| ~ incident_c(esk2_3(X120,X121,X122),X120)
| X120 = sum(X121,X122) )
& ( ~ incident_c(esk2_3(X120,X121,X122),X122)
| ~ incident_c(esk2_3(X120,X121,X122),X120)
| X120 = sum(X121,X122) )
& ( incident_c(esk2_3(X120,X121,X122),X120)
| incident_c(esk2_3(X120,X121,X122),X121)
| incident_c(esk2_3(X120,X121,X122),X122)
| X120 = sum(X121,X122) ) ),
inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(fof_nnf,[status(thm)],[sum_defn])])])])])]) ).
fof(i_0_35,plain,
! [X236,X237] :
( ( ~ ordered_by(X236,esk22_2(X236,X237),esk23_2(X236,X237))
| ~ ordered_by(X237,esk22_2(X236,X237),esk23_2(X236,X237))
| X236 = X237 )
& ( ordered_by(X236,esk22_2(X236,X237),esk23_2(X236,X237))
| ordered_by(X237,esk22_2(X236,X237),esk23_2(X236,X237))
| X236 = X237 ) ),
inference(distribute,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[o6])])])]) ).
fof(i_0_36,plain,
! [X230,X231,X232,X234,X235] :
( ( ~ incident_o(X234,esk21_3(X230,X231,X232))
| incident_c(X234,X232)
| ~ open(X232)
| X230 = X231
| ~ incident_c(X230,X232)
| ~ incident_c(X231,X232) )
& ( ~ incident_c(X235,X232)
| incident_o(X235,esk21_3(X230,X231,X232))
| ~ open(X232)
| X230 = X231
| ~ incident_c(X230,X232)
| ~ incident_c(X231,X232) )
& ( ordered_by(esk21_3(X230,X231,X232),X230,X231)
| ~ open(X232)
| X230 = X231
| ~ incident_c(X230,X232)
| ~ incident_c(X231,X232) ) ),
inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(fof_nnf,[status(thm)],[o5])])])])])]) ).
fof(i_0_37,plain,
! [X152,X153,X154,X155,X156] :
( ~ part_of(X153,X152)
| ~ part_of(X154,X152)
| ~ part_of(X155,X152)
| ~ end_point(X156,X153)
| ~ end_point(X156,X154)
| ~ end_point(X156,X155)
| part_of(X154,X155)
| part_of(X155,X154)
| part_of(X153,X154)
| part_of(X154,X153)
| part_of(X153,X155)
| part_of(X155,X153) ),
inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c2])])]) ).
fof(i_0_38,plain,
! [X170,X171,X172,X173,X174] :
( ~ closed(X170)
| ~ meet(X173,X171,X172)
| X170 != sum(X171,X172)
| ~ end_point(X174,X171)
| meet(X174,X171,X172) ),
inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c7])])]) ).
fof(i_0_39,plain,
! [X202,X203,X204,X205,X206] :
( ( incident_o(X202,X203)
| ~ finish_point(X202,X203) )
& ( X202 = X204
| ~ incident_o(X204,X203)
| ordered_by(X203,X204,X202)
| ~ finish_point(X202,X203) )
& ( X205 != esk16_2(X205,X206)
| ~ incident_o(X205,X206)
| finish_point(X205,X206) )
& ( incident_o(esk16_2(X205,X206),X206)
| ~ incident_o(X205,X206)
| finish_point(X205,X206) )
& ( ~ ordered_by(X206,esk16_2(X205,X206),X205)
| ~ incident_o(X205,X206)
| finish_point(X205,X206) ) ),
inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(fof_nnf,[status(thm)],[finish_point_defn])])])])])]) ).
fof(i_0_40,plain,
! [X196,X197,X198,X199,X200] :
( ( incident_o(X196,X197)
| ~ start_point(X196,X197) )
& ( X196 = X198
| ~ incident_o(X198,X197)
| ordered_by(X197,X196,X198)
| ~ start_point(X196,X197) )
& ( X199 != esk15_2(X199,X200)
| ~ incident_o(X199,X200)
| start_point(X199,X200) )
& ( incident_o(esk15_2(X199,X200),X200)
| ~ incident_o(X199,X200)
| start_point(X199,X200) )
& ( ~ ordered_by(X200,X199,esk15_2(X199,X200))
| ~ incident_o(X199,X200)
| start_point(X199,X200) ) ),
inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(fof_nnf,[status(thm)],[start_point_defn])])])])])]) ).
fof(i_0_41,plain,
! [X124,X125,X126,X127,X128,X129] :
( ( incident_c(X124,X125)
| ~ end_point(X124,X125) )
& ( ~ part_of(X126,X125)
| ~ part_of(X127,X125)
| ~ incident_c(X124,X126)
| ~ incident_c(X124,X127)
| part_of(X126,X127)
| part_of(X127,X126)
| ~ end_point(X124,X125) )
& ( part_of(esk3_2(X128,X129),X129)
| ~ incident_c(X128,X129)
| end_point(X128,X129) )
& ( part_of(esk4_2(X128,X129),X129)
| ~ incident_c(X128,X129)
| end_point(X128,X129) )
& ( incident_c(X128,esk3_2(X128,X129))
| ~ incident_c(X128,X129)
| end_point(X128,X129) )
& ( incident_c(X128,esk4_2(X128,X129))
| ~ incident_c(X128,X129)
| end_point(X128,X129) )
& ( ~ part_of(esk3_2(X128,X129),esk4_2(X128,X129))
| ~ incident_c(X128,X129)
| end_point(X128,X129) )
& ( ~ part_of(esk4_2(X128,X129),esk3_2(X128,X129))
| ~ incident_c(X128,X129)
| end_point(X128,X129) ) ),
inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(fof_nnf,[status(thm)],[end_point_defn])])])])])]) ).
fof(i_0_42,plain,
! [X240,X241,X242,X243,X244,X245] :
( ( ~ incident_o(X242,X241)
| incident_c(X242,X240)
| X240 != underlying_curve(X241) )
& ( ~ incident_c(X243,X240)
| incident_o(X243,X241)
| X240 != underlying_curve(X241) )
& ( ~ incident_o(esk24_2(X244,X245),X245)
| ~ incident_c(esk24_2(X244,X245),X244)
| X244 = underlying_curve(X245) )
& ( incident_o(esk24_2(X244,X245),X245)
| incident_c(esk24_2(X244,X245),X244)
| X244 = underlying_curve(X245) ) ),
inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(fof_nnf,[status(thm)],[underlying_curve_defn])])])])])]) ).
fof(i_0_43,plain,
! [X159,X160] :
( ( meet(X160,esk9_2(X159,X160),esk10_2(X159,X160))
| ~ inner_point(X160,X159) )
& ( X159 = sum(esk9_2(X159,X160),esk10_2(X159,X160))
| ~ inner_point(X160,X159) ) ),
inference(distribute,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c4])])])]) ).
fof(i_0_44,plain,
! [X179,X180] :
( ( ~ incident_c(esk13_2(X179,X180),X179)
| ~ incident_c(esk13_2(X179,X180),X180)
| X179 = X180 )
& ( incident_c(esk13_2(X179,X180),X179)
| incident_c(esk13_2(X179,X180),X180)
| X179 = X180 ) ),
inference(distribute,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c9])])])]) ).
fof(i_0_45,plain,
! [X175,X176,X177] :
( ~ meet(X177,X175,X176)
| esk12_2(X175,X176) = sum(X175,X176) ),
inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c8])])])]) ).
fof(i_0_46,plain,
! [X208,X209,X210] :
( ( incident_o(X209,X208)
| ~ ordered_by(X208,X209,X210) )
& ( incident_o(X210,X208)
| ~ ordered_by(X208,X209,X210) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[o1])])]) ).
fof(i_0_47,plain,
! [X109,X110,X111,X112,X113] :
( ( ~ part_of(X110,X109)
| ~ incident_c(X111,X110)
| incident_c(X111,X109) )
& ( incident_c(esk1_2(X112,X113),X113)
| part_of(X113,X112) )
& ( ~ incident_c(esk1_2(X112,X113),X112)
| part_of(X113,X112) ) ),
inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(fof_nnf,[status(thm)],[part_of_defn])])])])])]) ).
fof(i_0_48,plain,
! [X163,X164,X165,X166] :
( ~ end_point(X164,X163)
| ~ end_point(X165,X163)
| ~ end_point(X166,X163)
| X164 = X165
| X164 = X166
| X165 = X166 ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c5])]) ).
fof(i_0_49,plain,
! [X167,X168] :
( ( end_point(esk11_2(X167,X168),X167)
| ~ end_point(X168,X167) )
& ( X168 != esk11_2(X167,X168)
| ~ end_point(X168,X167) ) ),
inference(distribute,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c6])])])]) ).
fof(i_0_50,plain,
! [X132,X133] :
( ( incident_c(X132,X133)
| ~ inner_point(X132,X133) )
& ( ~ end_point(X132,X133)
| ~ inner_point(X132,X133) )
& ( ~ incident_c(X132,X133)
| end_point(X132,X133)
| inner_point(X132,X133) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[i_0_28])])]) ).
fof(i_0_51,negated_conjecture,
( ordered_by(esk25_0,esk26_0,esk27_0)
& ordered_by(esk25_0,esk27_0,esk26_0) ),
inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[i_0_29])])]) ).
fof(i_0_52,plain,
! [X211,X213,X214] :
( open(esk17_1(X211))
& ( ~ incident_o(X213,X211)
| incident_c(X213,esk17_1(X211)) )
& ( ~ incident_c(X214,esk17_1(X211))
| incident_o(X214,X211) ) ),
inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(fof_nnf,[status(thm)],[o2])])])])]) ).
fof(i_0_53,plain,
! [X142,X143,X144] :
( ( ~ closed(X142)
| ~ end_point(X143,X142) )
& ( end_point(esk6_1(X144),X144)
| closed(X144) ) ),
inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(fof_nnf,[status(thm)],[closed_defn])])])])]) ).
fof(i_0_54,plain,
! [X150,X151] :
( ~ part_of(X151,X150)
| X151 = X150
| open(X151) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c1])]) ).
fof(i_0_55,plain,
! [X146,X148,X149] :
( ( ~ open(X146)
| end_point(esk7_1(X146),X146) )
& ( ~ end_point(X149,X148)
| open(X148) ) ),
inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(fof_nnf,[status(thm)],[open_defn])])])])]) ).
fof(i_0_56,plain,
! [X228] : start_point(esk20_1(X228),X228),
inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[o4])]) ).
fof(i_0_57,plain,
! [X157] : inner_point(esk8_1(X157),X157),
inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[c3])]) ).
cnf(i_0_58,plain,
( between_o(X4,X1,X2,X3)
| ~ incident_o(esk19_5(X1,X2,X3,X4,X5),X4)
| ~ incident_c(esk19_5(X1,X2,X3,X4,X5),X5)
| ~ between_c(X5,X1,X2,X3) ),
inference(split_conjunct,[status(thm)],[i_0_30]),
[final] ).
cnf(i_0_59,plain,
( incident_o(esk19_5(X1,X2,X3,X4,X5),X4)
| incident_c(esk19_5(X1,X2,X3,X4,X5),X5)
| between_o(X4,X1,X2,X3)
| ~ between_c(X5,X1,X2,X3) ),
inference(split_conjunct,[status(thm)],[i_0_30]),
[final] ).
cnf(i_0_60,plain,
( incident_o(X1,X5)
| ~ incident_c(X1,esk18_4(X2,X3,X4,X5))
| ~ between_o(X5,X2,X3,X4) ),
inference(split_conjunct,[status(thm)],[i_0_30]),
[final] ).
cnf(i_0_61,plain,
( between_c(esk18_4(X1,X2,X3,X4),X1,X2,X3)
| ~ between_o(X4,X1,X2,X3) ),
inference(split_conjunct,[status(thm)],[i_0_30]),
[final] ).
cnf(i_0_62,plain,
( incident_c(X1,esk18_4(X3,X4,X5,X2))
| ~ incident_o(X1,X2)
| ~ between_o(X2,X3,X4,X5) ),
inference(split_conjunct,[status(thm)],[i_0_30]),
[final] ).
cnf(i_0_63,plain,
( part_of(esk14_4(X1,X2,X3,X4),X1)
| ~ between_c(X1,X2,X3,X4) ),
inference(split_conjunct,[status(thm)],[i_0_31]),
[final] ).
cnf(i_0_64,plain,
( inner_point(X1,esk14_4(X2,X3,X1,X4))
| ~ between_c(X2,X3,X1,X4) ),
inference(split_conjunct,[status(thm)],[i_0_31]),
[final] ).
cnf(i_0_65,plain,
( end_point(X1,esk14_4(X2,X1,X3,X4))
| ~ between_c(X2,X1,X3,X4) ),
inference(split_conjunct,[status(thm)],[i_0_31]),
[final] ).
cnf(i_0_66,plain,
( end_point(X1,esk14_4(X2,X3,X4,X1))
| ~ between_c(X2,X3,X4,X1) ),
inference(split_conjunct,[status(thm)],[i_0_31]),
[final] ).
cnf(i_0_67,plain,
( ordered_by(X1,X2,X3)
| ordered_by(X1,X2,X4)
| ~ between_o(X1,X3,X2,X4) ),
inference(split_conjunct,[status(thm)],[i_0_32]),
[final] ).
cnf(i_0_68,plain,
( ordered_by(X1,X2,X3)
| ordered_by(X1,X3,X2)
| ~ between_o(X1,X3,X2,X4) ),
inference(split_conjunct,[status(thm)],[i_0_32]),
[final] ).
cnf(i_0_69,plain,
( ordered_by(X1,X2,X3)
| ordered_by(X1,X3,X2)
| ~ between_o(X1,X4,X3,X2) ),
inference(split_conjunct,[status(thm)],[i_0_32]),
[final] ).
cnf(i_0_70,plain,
( ordered_by(X1,X2,X3)
| ordered_by(X1,X4,X3)
| ~ between_o(X1,X4,X3,X2) ),
inference(split_conjunct,[status(thm)],[i_0_32]),
[final] ).
cnf(i_0_71,plain,
( meet(X1,X2,X3)
| ~ end_point(esk5_3(X1,X2,X3),X2)
| ~ end_point(esk5_3(X1,X2,X3),X3)
| ~ incident_c(X1,X2)
| ~ incident_c(X1,X3) ),
inference(split_conjunct,[status(thm)],[i_0_33]),
[final] ).
cnf(i_0_72,plain,
( between_o(X1,X2,X3,X4)
| ~ ordered_by(X1,X2,X3)
| ~ ordered_by(X1,X3,X4) ),
inference(split_conjunct,[status(thm)],[i_0_32]),
[final] ).
cnf(i_0_73,plain,
( between_o(X1,X4,X3,X2)
| ~ ordered_by(X1,X2,X3)
| ~ ordered_by(X1,X3,X4) ),
inference(split_conjunct,[status(thm)],[i_0_32]),
[final] ).
cnf(i_0_74,plain,
( X1 = sum(X2,X3)
| ~ incident_c(esk2_3(X1,X2,X3),X2)
| ~ incident_c(esk2_3(X1,X2,X3),X1) ),
inference(split_conjunct,[status(thm)],[i_0_34]),
[final] ).
cnf(i_0_75,plain,
( X1 = sum(X2,X3)
| ~ incident_c(esk2_3(X1,X2,X3),X3)
| ~ incident_c(esk2_3(X1,X2,X3),X1) ),
inference(split_conjunct,[status(thm)],[i_0_34]),
[final] ).
cnf(i_0_76,plain,
( X1 != X2
| ~ between_c(X3,X1,X4,X2) ),
inference(split_conjunct,[status(thm)],[i_0_31]),
[final] ).
cnf(i_0_77,plain,
( incident_c(esk2_3(X1,X2,X3),X1)
| incident_c(esk2_3(X1,X2,X3),X2)
| incident_c(esk2_3(X1,X2,X3),X3)
| X1 = sum(X2,X3) ),
inference(split_conjunct,[status(thm)],[i_0_34]),
[final] ).
cnf(i_0_78,plain,
( X1 = X2
| between_c(X4,X1,X5,X2)
| ~ part_of(X3,X4)
| ~ end_point(X1,X3)
| ~ end_point(X2,X3)
| ~ inner_point(X5,X3) ),
inference(split_conjunct,[status(thm)],[i_0_31]),
[final] ).
cnf(i_0_79,plain,
( X1 = X2
| ~ ordered_by(X1,esk22_2(X1,X2),esk23_2(X1,X2))
| ~ ordered_by(X2,esk22_2(X1,X2),esk23_2(X1,X2)) ),
inference(split_conjunct,[status(thm)],[i_0_35]),
[final] ).
cnf(i_0_80,plain,
( incident_c(X1,X4)
| X2 = X3
| ~ incident_o(X1,esk21_3(X2,X3,X4))
| ~ open(X4)
| ~ incident_c(X2,X4)
| ~ incident_c(X3,X4) ),
inference(split_conjunct,[status(thm)],[i_0_36]),
[final] ).
cnf(i_0_81,plain,
( part_of(X3,X4)
| part_of(X4,X3)
| part_of(X1,X3)
| part_of(X3,X1)
| part_of(X1,X4)
| part_of(X4,X1)
| ~ part_of(X1,X2)
| ~ part_of(X3,X2)
| ~ part_of(X4,X2)
| ~ end_point(X5,X1)
| ~ end_point(X5,X3)
| ~ end_point(X5,X4) ),
inference(split_conjunct,[status(thm)],[i_0_37]),
[final] ).
cnf(i_0_82,plain,
( incident_c(esk5_3(X1,X2,X3),X2)
| meet(X1,X2,X3)
| ~ incident_c(X1,X2)
| ~ incident_c(X1,X3) ),
inference(split_conjunct,[status(thm)],[i_0_33]),
[final] ).
cnf(i_0_83,plain,
( incident_c(esk5_3(X1,X2,X3),X3)
| meet(X1,X2,X3)
| ~ incident_c(X1,X2)
| ~ incident_c(X1,X3) ),
inference(split_conjunct,[status(thm)],[i_0_33]),
[final] ).
cnf(i_0_84,plain,
( ordered_by(esk21_3(X1,X2,X3),X1,X2)
| X1 = X2
| ~ open(X3)
| ~ incident_c(X1,X3)
| ~ incident_c(X2,X3) ),
inference(split_conjunct,[status(thm)],[i_0_36]),
[final] ).
cnf(i_0_85,plain,
( ordered_by(X1,esk22_2(X1,X2),esk23_2(X1,X2))
| ordered_by(X2,esk22_2(X1,X2),esk23_2(X1,X2))
| X1 = X2 ),
inference(split_conjunct,[status(thm)],[i_0_35]),
[final] ).
cnf(i_0_86,plain,
( incident_o(X1,esk21_3(X3,X4,X2))
| X3 = X4
| ~ incident_c(X1,X2)
| ~ open(X2)
| ~ incident_c(X3,X2)
| ~ incident_c(X4,X2) ),
inference(split_conjunct,[status(thm)],[i_0_36]),
[final] ).
cnf(i_0_87,plain,
( meet(X5,X3,X4)
| ~ closed(X1)
| ~ meet(X2,X3,X4)
| X1 != sum(X3,X4)
| ~ end_point(X5,X3) ),
inference(split_conjunct,[status(thm)],[i_0_38]),
[final] ).
cnf(i_0_88,plain,
( finish_point(X2,X1)
| ~ ordered_by(X1,esk16_2(X2,X1),X2)
| ~ incident_o(X2,X1) ),
inference(split_conjunct,[status(thm)],[i_0_39]),
[final] ).
cnf(i_0_89,plain,
( start_point(X2,X1)
| ~ ordered_by(X1,X2,esk15_2(X2,X1))
| ~ incident_o(X2,X1) ),
inference(split_conjunct,[status(thm)],[i_0_40]),
[final] ).
cnf(i_0_90,plain,
( end_point(X1,X2)
| ~ incident_c(X1,X2)
| ~ incident_c(X1,X3)
| ~ meet(X4,X2,X3) ),
inference(split_conjunct,[status(thm)],[i_0_33]),
[final] ).
cnf(i_0_91,plain,
( end_point(X1,X2)
| ~ incident_c(X1,X3)
| ~ incident_c(X1,X2)
| ~ meet(X4,X3,X2) ),
inference(split_conjunct,[status(thm)],[i_0_33]),
[final] ).
cnf(i_0_92,plain,
( part_of(X1,X3)
| part_of(X3,X1)
| ~ part_of(X1,X2)
| ~ part_of(X3,X2)
| ~ incident_c(X4,X1)
| ~ incident_c(X4,X3)
| ~ end_point(X4,X2) ),
inference(split_conjunct,[status(thm)],[i_0_41]),
[final] ).
cnf(i_0_93,plain,
( end_point(X1,X2)
| ~ part_of(esk4_2(X1,X2),esk3_2(X1,X2))
| ~ incident_c(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_41]),
[final] ).
cnf(i_0_94,plain,
( end_point(X1,X2)
| ~ part_of(esk3_2(X1,X2),esk4_2(X1,X2))
| ~ incident_c(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_41]),
[final] ).
cnf(i_0_95,plain,
( X1 = underlying_curve(X2)
| ~ incident_o(esk24_2(X1,X2),X2)
| ~ incident_c(esk24_2(X1,X2),X1) ),
inference(split_conjunct,[status(thm)],[i_0_42]),
[final] ).
cnf(i_0_96,plain,
( meet(X1,esk9_2(X2,X1),esk10_2(X2,X1))
| ~ inner_point(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_43]),
[final] ).
cnf(i_0_97,plain,
( X1 = X2
| ~ incident_c(esk13_2(X1,X2),X1)
| ~ incident_c(esk13_2(X1,X2),X2) ),
inference(split_conjunct,[status(thm)],[i_0_44]),
[final] ).
cnf(i_0_98,plain,
( esk12_2(X2,X3) = sum(X2,X3)
| ~ meet(X1,X2,X3) ),
inference(split_conjunct,[status(thm)],[i_0_45]),
[final] ).
cnf(i_0_99,plain,
( X1 = X2
| ordered_by(X3,X1,X2)
| ~ incident_o(X2,X3)
| ~ start_point(X1,X3) ),
inference(split_conjunct,[status(thm)],[i_0_40]),
[final] ).
cnf(i_0_100,plain,
( X1 = X2
| ordered_by(X3,X2,X1)
| ~ incident_o(X2,X3)
| ~ finish_point(X1,X3) ),
inference(split_conjunct,[status(thm)],[i_0_39]),
[final] ).
cnf(i_0_101,plain,
( incident_o(X1,X2)
| ~ ordered_by(X2,X1,X3) ),
inference(split_conjunct,[status(thm)],[i_0_46]),
[final] ).
cnf(i_0_102,plain,
( incident_o(X1,X2)
| ~ ordered_by(X2,X3,X1) ),
inference(split_conjunct,[status(thm)],[i_0_46]),
[final] ).
cnf(i_0_103,plain,
( incident_c(X1,X2)
| ~ meet(X1,X2,X3) ),
inference(split_conjunct,[status(thm)],[i_0_33]),
[final] ).
cnf(i_0_104,plain,
( incident_c(X1,X2)
| ~ meet(X1,X3,X2) ),
inference(split_conjunct,[status(thm)],[i_0_33]),
[final] ).
cnf(i_0_105,plain,
( X1 = sum(esk9_2(X1,X2),esk10_2(X1,X2))
| ~ inner_point(X2,X1) ),
inference(split_conjunct,[status(thm)],[i_0_43]),
[final] ).
cnf(i_0_106,plain,
( incident_o(esk24_2(X1,X2),X2)
| incident_c(esk24_2(X1,X2),X1)
| X1 = underlying_curve(X2) ),
inference(split_conjunct,[status(thm)],[i_0_42]),
[final] ).
cnf(i_0_107,plain,
( incident_c(esk13_2(X1,X2),X1)
| incident_c(esk13_2(X1,X2),X2)
| X1 = X2 ),
inference(split_conjunct,[status(thm)],[i_0_44]),
[final] ).
cnf(i_0_108,plain,
( part_of(X2,X1)
| ~ incident_c(esk1_2(X1,X2),X1) ),
inference(split_conjunct,[status(thm)],[i_0_47]),
[final] ).
cnf(i_0_109,plain,
( incident_o(esk16_2(X1,X2),X2)
| finish_point(X1,X2)
| ~ incident_o(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_39]),
[final] ).
cnf(i_0_110,plain,
( incident_o(esk15_2(X1,X2),X2)
| start_point(X1,X2)
| ~ incident_o(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_40]),
[final] ).
cnf(i_0_111,plain,
( part_of(esk4_2(X1,X2),X2)
| end_point(X1,X2)
| ~ incident_c(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_41]),
[final] ).
cnf(i_0_112,plain,
( part_of(esk3_2(X1,X2),X2)
| end_point(X1,X2)
| ~ incident_c(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_41]),
[final] ).
cnf(i_0_113,plain,
( incident_c(X1,esk4_2(X1,X2))
| end_point(X1,X2)
| ~ incident_c(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_41]),
[final] ).
cnf(i_0_114,plain,
( incident_c(X1,esk3_2(X1,X2))
| end_point(X1,X2)
| ~ incident_c(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_41]),
[final] ).
cnf(i_0_115,plain,
( incident_c(X1,X3)
| incident_c(X1,X4)
| ~ incident_c(X1,X2)
| X2 != sum(X3,X4) ),
inference(split_conjunct,[status(thm)],[i_0_34]),
[final] ).
cnf(i_0_116,plain,
( X1 = X3
| X1 = X4
| X3 = X4
| ~ end_point(X1,X2)
| ~ end_point(X3,X2)
| ~ end_point(X4,X2) ),
inference(split_conjunct,[status(thm)],[i_0_48]),
[final] ).
cnf(i_0_117,plain,
( end_point(esk11_2(X1,X2),X1)
| ~ end_point(X2,X1) ),
inference(split_conjunct,[status(thm)],[i_0_49]),
[final] ).
cnf(i_0_118,plain,
( finish_point(X1,X2)
| X1 != esk16_2(X1,X2)
| ~ incident_o(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_39]),
[final] ).
cnf(i_0_119,plain,
( start_point(X1,X2)
| X1 != esk15_2(X1,X2)
| ~ incident_o(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_40]),
[final] ).
cnf(i_0_120,plain,
( incident_c(X1,X3)
| ~ incident_c(X1,X2)
| X3 != sum(X2,X4) ),
inference(split_conjunct,[status(thm)],[i_0_34]),
[final] ).
cnf(i_0_121,plain,
( incident_c(X1,X3)
| ~ incident_c(X1,X2)
| X3 != sum(X4,X2) ),
inference(split_conjunct,[status(thm)],[i_0_34]),
[final] ).
cnf(i_0_122,plain,
( incident_c(X3,X2)
| ~ part_of(X1,X2)
| ~ incident_c(X3,X1) ),
inference(split_conjunct,[status(thm)],[i_0_47]),
[final] ).
cnf(i_0_123,plain,
( incident_c(esk1_2(X1,X2),X2)
| part_of(X2,X1) ),
inference(split_conjunct,[status(thm)],[i_0_47]),
[final] ).
cnf(i_0_124,plain,
( end_point(X1,X2)
| inner_point(X1,X2)
| ~ incident_c(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_50]),
[final] ).
cnf(i_0_125,negated_conjecture,
ordered_by(esk25_0,esk27_0,esk26_0),
inference(split_conjunct,[status(thm)],[i_0_51]),
[final] ).
cnf(i_0_126,negated_conjecture,
ordered_by(esk25_0,esk26_0,esk27_0),
inference(split_conjunct,[status(thm)],[i_0_51]),
[final] ).
cnf(i_0_127,plain,
( incident_o(X1,X2)
| ~ incident_c(X1,esk17_1(X2)) ),
inference(split_conjunct,[status(thm)],[i_0_52]),
[final] ).
cnf(i_0_128,plain,
( X1 != esk11_2(X2,X1)
| ~ end_point(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_49]),
[final] ).
cnf(i_0_129,plain,
( incident_o(X1,X3)
| ~ incident_c(X1,X2)
| X2 != underlying_curve(X3) ),
inference(split_conjunct,[status(thm)],[i_0_42]),
[final] ).
cnf(i_0_130,plain,
( incident_c(X1,X3)
| ~ incident_o(X1,X2)
| X3 != underlying_curve(X2) ),
inference(split_conjunct,[status(thm)],[i_0_42]),
[final] ).
cnf(i_0_131,plain,
( ~ end_point(X1,X2)
| ~ inner_point(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_50]),
[final] ).
cnf(i_0_132,plain,
( incident_c(X1,esk17_1(X2))
| ~ incident_o(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_52]),
[final] ).
cnf(i_0_133,plain,
( incident_o(X1,X2)
| ~ finish_point(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_39]),
[final] ).
cnf(i_0_134,plain,
( incident_o(X1,X2)
| ~ start_point(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_40]),
[final] ).
cnf(i_0_135,plain,
( incident_c(X1,X2)
| ~ inner_point(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_50]),
[final] ).
cnf(i_0_136,plain,
( incident_c(X1,X2)
| ~ end_point(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_41]),
[final] ).
cnf(i_0_137,plain,
( ~ closed(X1)
| ~ end_point(X2,X1) ),
inference(split_conjunct,[status(thm)],[i_0_53]),
[final] ).
cnf(i_0_138,plain,
( X1 = X2
| open(X1)
| ~ part_of(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_54]),
[final] ).
cnf(i_0_139,plain,
( end_point(esk7_1(X1),X1)
| ~ open(X1) ),
inference(split_conjunct,[status(thm)],[i_0_55]),
[final] ).
cnf(i_0_140,plain,
( open(X2)
| ~ end_point(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_55]),
[final] ).
cnf(i_0_141,plain,
( end_point(esk6_1(X1),X1)
| closed(X1) ),
inference(split_conjunct,[status(thm)],[i_0_53]),
[final] ).
cnf(i_0_142,plain,
start_point(esk20_1(X1),X1),
inference(split_conjunct,[status(thm)],[i_0_56]),
[final] ).
cnf(i_0_143,plain,
inner_point(esk8_1(X1),X1),
inference(split_conjunct,[status(thm)],[i_0_57]),
[final] ).
cnf(i_0_144,plain,
open(esk17_1(X1)),
inference(split_conjunct,[status(thm)],[i_0_52]),
[final] ).
cnf(i_0_145,axiom,
X1 = X1 ).
cnf(i_0_146,axiom,
( X1 = X2
| X2 != X1 ) ).
cnf(i_0_147,axiom,
( X1 = X2
| X1 != X3
| X3 != X2 ) ).
cnf(i_0_148,axiom,
( X1 != X2
| esk16_2(X1,X3) = esk16_2(X2,X3) ) ).
cnf(i_0_149,axiom,
( X1 != X2
| esk16_2(X3,X1) = esk16_2(X3,X2) ) ).
cnf(i_0_150,axiom,
( X1 != X2
| esk15_2(X1,X3) = esk15_2(X2,X3) ) ).
cnf(i_0_151,axiom,
( X1 != X2
| esk15_2(X3,X1) = esk15_2(X3,X2) ) ).
cnf(i_0_152,axiom,
( X1 != X2
| underlying_curve(X1) = underlying_curve(X2) ) ).
cnf(i_0_153,axiom,
( X1 != X2
| esk12_2(X1,X3) = esk12_2(X2,X3) ) ).
cnf(i_0_154,axiom,
( X1 != X2
| esk12_2(X3,X1) = esk12_2(X3,X2) ) ).
cnf(i_0_155,axiom,
( X1 != X2
| esk11_2(X1,X3) = esk11_2(X2,X3) ) ).
cnf(i_0_156,axiom,
( X1 != X2
| esk11_2(X3,X1) = esk11_2(X3,X2) ) ).
cnf(i_0_157,axiom,
( X1 != X2
| sum(X1,X3) = sum(X2,X3) ) ).
cnf(i_0_158,axiom,
( X1 != X2
| sum(X3,X1) = sum(X3,X2) ) ).
cnf(i_0_159,axiom,
( X1 != X2
| ~ between_o(X1,X3,X4,X5)
| between_o(X2,X3,X4,X5) ) ).
cnf(i_0_160,axiom,
( X1 != X2
| ~ between_o(X3,X1,X4,X5)
| between_o(X3,X2,X4,X5) ) ).
cnf(i_0_161,axiom,
( X1 != X2
| ~ between_o(X3,X4,X1,X5)
| between_o(X3,X4,X2,X5) ) ).
cnf(i_0_162,axiom,
( X1 != X2
| ~ between_o(X3,X4,X5,X1)
| between_o(X3,X4,X5,X2) ) ).
cnf(i_0_163,axiom,
( X1 != X2
| ~ open(X1)
| open(X2) ) ).
cnf(i_0_164,axiom,
( X1 != X2
| ~ closed(X1)
| closed(X2) ) ).
cnf(i_0_165,axiom,
( X1 != X2
| ~ finish_point(X1,X3)
| finish_point(X2,X3) ) ).
cnf(i_0_166,axiom,
( X1 != X2
| ~ finish_point(X3,X1)
| finish_point(X3,X2) ) ).
cnf(i_0_167,axiom,
( X1 != X2
| ~ start_point(X1,X3)
| start_point(X2,X3) ) ).
cnf(i_0_168,axiom,
( X1 != X2
| ~ start_point(X3,X1)
| start_point(X3,X2) ) ).
cnf(i_0_169,axiom,
( X1 != X2
| ~ incident_o(X1,X3)
| incident_o(X2,X3) ) ).
cnf(i_0_170,axiom,
( X1 != X2
| ~ incident_o(X3,X1)
| incident_o(X3,X2) ) ).
cnf(i_0_171,axiom,
( X1 != X2
| ~ incident_c(X1,X3)
| incident_c(X2,X3) ) ).
cnf(i_0_172,axiom,
( X1 != X2
| ~ incident_c(X3,X1)
| incident_c(X3,X2) ) ).
cnf(i_0_173,axiom,
( X1 != X2
| ~ between_c(X1,X3,X4,X5)
| between_c(X2,X3,X4,X5) ) ).
cnf(i_0_174,axiom,
( X1 != X2
| ~ between_c(X3,X1,X4,X5)
| between_c(X3,X2,X4,X5) ) ).
cnf(i_0_175,axiom,
( X1 != X2
| ~ between_c(X3,X4,X1,X5)
| between_c(X3,X4,X2,X5) ) ).
cnf(i_0_176,axiom,
( X1 != X2
| ~ between_c(X3,X4,X5,X1)
| between_c(X3,X4,X5,X2) ) ).
cnf(i_0_177,axiom,
( X1 != X2
| ~ part_of(X1,X3)
| part_of(X2,X3) ) ).
cnf(i_0_178,axiom,
( X1 != X2
| ~ part_of(X3,X1)
| part_of(X3,X2) ) ).
cnf(i_0_179,axiom,
( X1 != X2
| ~ inner_point(X1,X3)
| inner_point(X2,X3) ) ).
cnf(i_0_180,axiom,
( X1 != X2
| ~ inner_point(X3,X1)
| inner_point(X3,X2) ) ).
cnf(i_0_181,axiom,
( X1 != X2
| ~ end_point(X1,X3)
| end_point(X2,X3) ) ).
cnf(i_0_182,axiom,
( X1 != X2
| ~ end_point(X3,X1)
| end_point(X3,X2) ) ).
cnf(i_0_183,axiom,
( X1 != X2
| ~ ordered_by(X1,X3,X4)
| ordered_by(X2,X3,X4) ) ).
cnf(i_0_184,axiom,
( X1 != X2
| ~ ordered_by(X3,X1,X4)
| ordered_by(X3,X2,X4) ) ).
cnf(i_0_185,axiom,
( X1 != X2
| ~ ordered_by(X3,X4,X1)
| ordered_by(X3,X4,X2) ) ).
cnf(i_0_186,axiom,
( X1 != X2
| ~ meet(X1,X3,X4)
| meet(X2,X3,X4) ) ).
cnf(i_0_187,axiom,
( X1 != X2
| ~ meet(X3,X1,X4)
| meet(X3,X2,X4) ) ).
cnf(i_0_188,axiom,
( X1 != X2
| ~ meet(X3,X4,X1)
| meet(X3,X4,X2) ) ).
cnf(i_0_145_001,axiom,
X1 = X1 ).
cnf(i_0_146_002,axiom,
( X1 = X2
| X2 != X1 ) ).
cnf(i_0_147_003,axiom,
( X1 = X2
| X1 != X3
| X3 != X2 ) ).
cnf(i_0_148_004,axiom,
( X1 != X2
| esk16_2(X1,X3) = esk16_2(X2,X3) ) ).
cnf(i_0_149_005,axiom,
( X1 != X2
| esk16_2(X3,X1) = esk16_2(X3,X2) ) ).
cnf(i_0_150_006,axiom,
( X1 != X2
| esk15_2(X1,X3) = esk15_2(X2,X3) ) ).
cnf(i_0_151_007,axiom,
( X1 != X2
| esk15_2(X3,X1) = esk15_2(X3,X2) ) ).
cnf(i_0_152_008,axiom,
( X1 != X2
| underlying_curve(X1) = underlying_curve(X2) ) ).
cnf(i_0_153_009,axiom,
( X1 != X2
| esk12_2(X1,X3) = esk12_2(X2,X3) ) ).
cnf(i_0_154_010,axiom,
( X1 != X2
| esk12_2(X3,X1) = esk12_2(X3,X2) ) ).
cnf(i_0_155_011,axiom,
( X1 != X2
| esk11_2(X1,X3) = esk11_2(X2,X3) ) ).
cnf(i_0_156_012,axiom,
( X1 != X2
| esk11_2(X3,X1) = esk11_2(X3,X2) ) ).
cnf(i_0_157_013,axiom,
( X1 != X2
| sum(X1,X3) = sum(X2,X3) ) ).
cnf(i_0_158_014,axiom,
( X1 != X2
| sum(X3,X1) = sum(X3,X2) ) ).
cnf(i_0_159_015,axiom,
( X1 != X2
| ~ between_o(X1,X3,X4,X5)
| between_o(X2,X3,X4,X5) ) ).
cnf(i_0_160_016,axiom,
( X1 != X2
| ~ between_o(X3,X1,X4,X5)
| between_o(X3,X2,X4,X5) ) ).
cnf(i_0_161_017,axiom,
( X1 != X2
| ~ between_o(X3,X4,X1,X5)
| between_o(X3,X4,X2,X5) ) ).
cnf(i_0_162_018,axiom,
( X1 != X2
| ~ between_o(X3,X4,X5,X1)
| between_o(X3,X4,X5,X2) ) ).
cnf(i_0_163_019,axiom,
( X1 != X2
| ~ open(X1)
| open(X2) ) ).
cnf(i_0_164_020,axiom,
( X1 != X2
| ~ closed(X1)
| closed(X2) ) ).
cnf(i_0_165_021,axiom,
( X1 != X2
| ~ finish_point(X1,X3)
| finish_point(X2,X3) ) ).
cnf(i_0_166_022,axiom,
( X1 != X2
| ~ finish_point(X3,X1)
| finish_point(X3,X2) ) ).
cnf(i_0_167_023,axiom,
( X1 != X2
| ~ start_point(X1,X3)
| start_point(X2,X3) ) ).
cnf(i_0_168_024,axiom,
( X1 != X2
| ~ start_point(X3,X1)
| start_point(X3,X2) ) ).
cnf(i_0_169_025,axiom,
( X1 != X2
| ~ incident_o(X1,X3)
| incident_o(X2,X3) ) ).
cnf(i_0_170_026,axiom,
( X1 != X2
| ~ incident_o(X3,X1)
| incident_o(X3,X2) ) ).
cnf(i_0_171_027,axiom,
( X1 != X2
| ~ incident_c(X1,X3)
| incident_c(X2,X3) ) ).
cnf(i_0_172_028,axiom,
( X1 != X2
| ~ incident_c(X3,X1)
| incident_c(X3,X2) ) ).
cnf(i_0_173_029,axiom,
( X1 != X2
| ~ between_c(X1,X3,X4,X5)
| between_c(X2,X3,X4,X5) ) ).
cnf(i_0_174_030,axiom,
( X1 != X2
| ~ between_c(X3,X1,X4,X5)
| between_c(X3,X2,X4,X5) ) ).
cnf(i_0_175_031,axiom,
( X1 != X2
| ~ between_c(X3,X4,X1,X5)
| between_c(X3,X4,X2,X5) ) ).
cnf(i_0_176_032,axiom,
( X1 != X2
| ~ between_c(X3,X4,X5,X1)
| between_c(X3,X4,X5,X2) ) ).
cnf(i_0_177_033,axiom,
( X1 != X2
| ~ part_of(X1,X3)
| part_of(X2,X3) ) ).
cnf(i_0_178_034,axiom,
( X1 != X2
| ~ part_of(X3,X1)
| part_of(X3,X2) ) ).
cnf(i_0_179_035,axiom,
( X1 != X2
| ~ inner_point(X1,X3)
| inner_point(X2,X3) ) ).
cnf(i_0_180_036,axiom,
( X1 != X2
| ~ inner_point(X3,X1)
| inner_point(X3,X2) ) ).
cnf(i_0_181_037,axiom,
( X1 != X2
| ~ end_point(X1,X3)
| end_point(X2,X3) ) ).
cnf(i_0_182_038,axiom,
( X1 != X2
| ~ end_point(X3,X1)
| end_point(X3,X2) ) ).
cnf(i_0_183_039,axiom,
( X1 != X2
| ~ ordered_by(X1,X3,X4)
| ordered_by(X2,X3,X4) ) ).
cnf(i_0_184_040,axiom,
( X1 != X2
| ~ ordered_by(X3,X1,X4)
| ordered_by(X3,X2,X4) ) ).
cnf(i_0_185_041,axiom,
( X1 != X2
| ~ ordered_by(X3,X4,X1)
| ordered_by(X3,X4,X2) ) ).
cnf(i_0_186_042,axiom,
( X1 != X2
| ~ meet(X1,X3,X4)
| meet(X2,X3,X4) ) ).
cnf(i_0_187_043,axiom,
( X1 != X2
| ~ meet(X3,X1,X4)
| meet(X3,X2,X4) ) ).
cnf(i_0_188_044,axiom,
( X1 != X2
| ~ meet(X3,X4,X1)
| meet(X3,X4,X2) ) ).
cnf(i_0_189,plain,
~ between_c(X1,X2,X3,X2),
inference(equality_inference,[],[76]) ).
cnf(i_0_190,plain,
( ~ end_point(X1,X2)
| meet(X1,X2,X3)
| ~ meet(X4,X2,X3)
| ~ closed(sum(X2,X3)) ),
inference(equality_inference,[],[87]) ).
cnf(i_0_191,plain,
( incident_c(X1,X2)
| incident_c(X1,X3)
| ~ incident_c(X1,sum(X2,X3)) ),
inference(equality_inference,[],[115]) ).
cnf(i_0_192,plain,
( incident_c(X1,sum(X2,X3))
| ~ incident_c(X1,X2) ),
inference(equality_inference,[],[120]) ).
cnf(i_0_193,plain,
( incident_c(X1,sum(X2,X3))
| ~ incident_c(X1,X3) ),
inference(equality_inference,[],[121]) ).
cnf(i_0_194,plain,
( incident_o(X1,X2)
| ~ incident_c(X1,underlying_curve(X2)) ),
inference(equality_inference,[],[129]) ).
cnf(i_0_195,plain,
( incident_c(X1,underlying_curve(X2))
| ~ incident_o(X1,X2) ),
inference(equality_inference,[],[130]) ).
cnf(i_0_196,plain,
~ between_o(X1,X2,X3,X2),
inference(scs_inference,[],[i_0_189,i_0_61]) ).
cnf(i_0_197,plain,
~ between_c(X1,X2,X3,X2),
inference(rename_variables,[],[i_0_189]) ).
cnf(i_0_198,plain,
( between_c(esk18_4(X1,X2,X3,X4),X1,X2,X3)
| ~ between_o(X4,X1,X2,X3) ),
inference(rename_variables,[],[i_0_61]) ).
cnf(i_0_199,plain,
incident_c(esk8_1(X1),X1),
inference(scs_inference,[],[i_0_189,i_0_143,i_0_61,i_0_135]) ).
cnf(i_0_200,plain,
( ~ inner_point(X1,X2)
| incident_c(X1,X2) ),
inference(rename_variables,[],[i_0_135]) ).
cnf(i_0_201,plain,
incident_c(esk8_1(X1),sum(X1,X2)),
inference(scs_inference,[],[i_0_189,i_0_143,i_0_61,i_0_135,i_0_192]) ).
cnf(i_0_202,plain,
( ~ incident_c(X1,X2)
| incident_c(X1,sum(X2,X3)) ),
inference(rename_variables,[],[i_0_192]) ).
cnf(i_0_203,plain,
incident_c(esk8_1(X1),sum(X2,X1)),
inference(scs_inference,[],[i_0_189,i_0_143,i_0_61,i_0_135,i_0_192,i_0_193]) ).
cnf(i_0_204,plain,
( ~ incident_c(X1,X2)
| incident_c(X1,sum(X3,X2)) ),
inference(rename_variables,[],[i_0_193]) ).
cnf(i_0_205,plain,
incident_o(esk8_1(esk17_1(X1)),X1),
inference(scs_inference,[],[i_0_189,i_0_143,i_0_61,i_0_135,i_0_192,i_0_193,i_0_127]) ).
cnf(i_0_206,plain,
( ~ incident_c(X1,esk17_1(X2))
| incident_o(X1,X2) ),
inference(rename_variables,[],[i_0_127]) ).
cnf(i_0_207,plain,
~ end_point(esk8_1(esk17_1(X1)),esk17_1(X1)),
inference(scs_inference,[],[i_0_189,i_0_143,i_0_61,i_0_135,i_0_192,i_0_193,i_0_127,i_0_131]) ).
cnf(i_0_208,plain,
inner_point(esk8_1(X1),X1),
inference(rename_variables,[],[i_0_143]) ).
cnf(i_0_209,plain,
( ~ inner_point(X1,X2)
| ~ end_point(X1,X2) ),
inference(rename_variables,[],[i_0_131]) ).
cnf(i_0_210,plain,
incident_o(esk20_1(X1),X1),
inference(scs_inference,[],[i_0_189,i_0_142,i_0_143,i_0_61,i_0_135,i_0_192,i_0_193,i_0_127,i_0_131,i_0_134]) ).
cnf(i_0_211,plain,
( ~ start_point(X1,X2)
| incident_o(X1,X2) ),
inference(rename_variables,[],[i_0_134]) ).
cnf(i_0_212,plain,
$false,
inference(scs_inference,[],[i_0_125,i_0_126,i_0_189,i_0_142,i_0_143,i_0_61,i_0_135,i_0_192,i_0_193,i_0_127,i_0_131,i_0_134,i_0_72]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : GEO118+1 : TPTP v9.2.1. Released v2.4.0.
% 0.00/0.12 % Command : /export/starexec/sandbox2/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox2/solver/bin/cse --final-prover /export/starexec/sandbox2/solver/bin/eprover --proof-time %d --global-time-limit %d
% 0.14/0.33 % Computer : n006.cluster.edu
% 0.14/0.33 % Model : x86_64 x86_64
% 0.14/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.33 % Memory : 8042.1875MB
% 0.14/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.33 % CPULimit : 300
% 0.14/0.33 % WCLimit : 300
% 0.14/0.33 % DateTime : Mon May 4 17:43:16 EDT 2026
% 0.14/0.33 % CPUTime :
% 0.14/0.35 % start to proof: theBenchmark
% 0.32/1.62 % Version : CSE_E---1.7
% 0.32/1.62 % Problem : theBenchmark.p
% 0.32/1.62 % SZS status Theorem for theBenchmark.p
% 0.32/1.62 % SZS output start CNFRefutation
% See solution above
% 0.32/1.68 % Total time : 1.272s
%------------------------------------------------------------------------------