%------------------------------------------------------------------------------
% File : CSE_E---1.7
% Problem : GEO117+1 : TPTP v9.2.1. Released v2.4.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 : 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.34s 1.62s
% Output : CNFRefutation 0.34s
% 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/sandbox/benchmark/Axioms/GEO004+0.ax',inner_point_defn) ).
fof(theorem_4_4,conjecture,
! [X9,X3] : ~ ordered_by(X9,X3,X3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',theorem_4_4) ).
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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/benchmark/Axioms/GEO004+0.ax',c9) ).
fof(c8,axiom,
! [X2,X4] :
( ? [X3] : meet(X3,X2,X4)
=> ? [X1] : X1 = sum(X2,X4) ),
file('/export/starexec/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/benchmark/Axioms/GEO004+2.ax',o2) ).
fof(closed_defn,axiom,
! [X1] :
( closed(X1)
<=> ~ ? [X3] : end_point(X3,X1) ),
file('/export/starexec/sandbox/benchmark/Axioms/GEO004+0.ax',closed_defn) ).
fof(c1,axiom,
! [X1,X2] :
( ( part_of(X2,X1)
& X2 != X1 )
=> open(X2) ),
file('/export/starexec/sandbox/benchmark/Axioms/GEO004+0.ax',c1) ).
fof(open_defn,axiom,
! [X1] :
( open(X1)
<=> ? [X3] : end_point(X3,X1) ),
file('/export/starexec/sandbox/benchmark/Axioms/GEO004+0.ax',open_defn) ).
fof(o4,axiom,
! [X9] :
? [X3] : start_point(X3,X9),
file('/export/starexec/sandbox/benchmark/Axioms/GEO004+2.ax',o4) ).
fof(c3,axiom,
! [X1] :
? [X3] : inner_point(X3,X1),
file('/export/starexec/sandbox/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] : ~ ordered_by(X9,X3,X3),
inference(fof_simplification,[status(thm)],[inference(assume_negation,[status(cth)],[theorem_4_4])]) ).
fof(i_0_30,plain,
! [X214,X215,X216,X217,X219,X220,X221,X222,X223,X224,X225] :
( ( ~ incident_o(X219,X217)
| incident_c(X219,esk18_4(X214,X215,X216,X217))
| ~ between_o(X217,X214,X215,X216) )
& ( ~ incident_c(X220,esk18_4(X214,X215,X216,X217))
| incident_o(X220,X217)
| ~ between_o(X217,X214,X215,X216) )
& ( between_c(esk18_4(X214,X215,X216,X217),X214,X215,X216)
| ~ between_o(X217,X214,X215,X216) )
& ( ~ incident_o(esk19_5(X221,X222,X223,X224,X225),X224)
| ~ incident_c(esk19_5(X221,X222,X223,X224,X225),X225)
| ~ between_c(X225,X221,X222,X223)
| between_o(X224,X221,X222,X223) )
& ( incident_o(esk19_5(X221,X222,X223,X224,X225),X224)
| incident_c(esk19_5(X221,X222,X223,X224,X225),X225)
| ~ between_c(X225,X221,X222,X223)
| between_o(X224,X221,X222,X223) ) ),
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,
! [X181,X182,X183,X184,X186,X187,X188,X189,X190] :
( ( X182 != X184
| ~ between_c(X181,X182,X183,X184) )
& ( part_of(esk14_4(X181,X182,X183,X184),X181)
| ~ between_c(X181,X182,X183,X184) )
& ( end_point(X182,esk14_4(X181,X182,X183,X184))
| ~ between_c(X181,X182,X183,X184) )
& ( end_point(X184,esk14_4(X181,X182,X183,X184))
| ~ between_c(X181,X182,X183,X184) )
& ( inner_point(X183,esk14_4(X181,X182,X183,X184))
| ~ between_c(X181,X182,X183,X184) )
& ( X187 = X189
| ~ part_of(X190,X186)
| ~ end_point(X187,X190)
| ~ end_point(X189,X190)
| ~ inner_point(X188,X190)
| between_c(X186,X187,X188,X189) ) ),
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,
! [X191,X192,X193,X194] :
( ( ordered_by(X191,X194,X193)
| ordered_by(X191,X192,X193)
| ~ between_o(X191,X192,X193,X194) )
& ( ordered_by(X191,X193,X192)
| ordered_by(X191,X192,X193)
| ~ between_o(X191,X192,X193,X194) )
& ( ordered_by(X191,X194,X193)
| ordered_by(X191,X193,X194)
| ~ between_o(X191,X192,X193,X194) )
& ( ordered_by(X191,X193,X192)
| ordered_by(X191,X193,X194)
| ~ between_o(X191,X192,X193,X194) )
& ( ~ ordered_by(X191,X192,X193)
| ~ ordered_by(X191,X193,X194)
| between_o(X191,X192,X193,X194) )
& ( ~ ordered_by(X191,X194,X193)
| ~ ordered_by(X191,X193,X192)
| between_o(X191,X192,X193,X194) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[between_o_defn])])]) ).
fof(i_0_33,plain,
! [X133,X134,X135,X136,X137,X138,X139] :
( ( incident_c(X133,X134)
| ~ meet(X133,X134,X135) )
& ( incident_c(X133,X135)
| ~ meet(X133,X134,X135) )
& ( end_point(X136,X134)
| ~ incident_c(X136,X134)
| ~ incident_c(X136,X135)
| ~ meet(X133,X134,X135) )
& ( end_point(X136,X135)
| ~ incident_c(X136,X134)
| ~ incident_c(X136,X135)
| ~ meet(X133,X134,X135) )
& ( incident_c(esk5_3(X137,X138,X139),X138)
| ~ incident_c(X137,X138)
| ~ incident_c(X137,X139)
| meet(X137,X138,X139) )
& ( incident_c(esk5_3(X137,X138,X139),X139)
| ~ incident_c(X137,X138)
| ~ incident_c(X137,X139)
| meet(X137,X138,X139) )
& ( ~ end_point(esk5_3(X137,X138,X139),X138)
| ~ end_point(esk5_3(X137,X138,X139),X139)
| ~ incident_c(X137,X138)
| ~ incident_c(X137,X139)
| meet(X137,X138,X139) ) ),
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,
! [X114,X115,X116,X117,X118,X119,X120,X121] :
( ( ~ incident_c(X117,X114)
| incident_c(X117,X115)
| incident_c(X117,X116)
| X114 != sum(X115,X116) )
& ( ~ incident_c(X118,X115)
| incident_c(X118,X114)
| X114 != sum(X115,X116) )
& ( ~ incident_c(X118,X116)
| incident_c(X118,X114)
| X114 != sum(X115,X116) )
& ( ~ incident_c(esk2_3(X119,X120,X121),X120)
| ~ incident_c(esk2_3(X119,X120,X121),X119)
| X119 = sum(X120,X121) )
& ( ~ incident_c(esk2_3(X119,X120,X121),X121)
| ~ incident_c(esk2_3(X119,X120,X121),X119)
| X119 = sum(X120,X121) )
& ( incident_c(esk2_3(X119,X120,X121),X119)
| incident_c(esk2_3(X119,X120,X121),X120)
| incident_c(esk2_3(X119,X120,X121),X121)
| X119 = sum(X120,X121) ) ),
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,
! [X235,X236] :
( ( ~ ordered_by(X235,esk22_2(X235,X236),esk23_2(X235,X236))
| ~ ordered_by(X236,esk22_2(X235,X236),esk23_2(X235,X236))
| X235 = X236 )
& ( ordered_by(X235,esk22_2(X235,X236),esk23_2(X235,X236))
| ordered_by(X236,esk22_2(X235,X236),esk23_2(X235,X236))
| X235 = X236 ) ),
inference(distribute,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[o6])])])]) ).
fof(i_0_36,plain,
! [X229,X230,X231,X233,X234] :
( ( ~ incident_o(X233,esk21_3(X229,X230,X231))
| incident_c(X233,X231)
| ~ open(X231)
| X229 = X230
| ~ incident_c(X229,X231)
| ~ incident_c(X230,X231) )
& ( ~ incident_c(X234,X231)
| incident_o(X234,esk21_3(X229,X230,X231))
| ~ open(X231)
| X229 = X230
| ~ incident_c(X229,X231)
| ~ incident_c(X230,X231) )
& ( ordered_by(esk21_3(X229,X230,X231),X229,X230)
| ~ open(X231)
| X229 = X230
| ~ incident_c(X229,X231)
| ~ incident_c(X230,X231) ) ),
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,
! [X151,X152,X153,X154,X155] :
( ~ part_of(X152,X151)
| ~ part_of(X153,X151)
| ~ part_of(X154,X151)
| ~ end_point(X155,X152)
| ~ end_point(X155,X153)
| ~ end_point(X155,X154)
| part_of(X153,X154)
| part_of(X154,X153)
| part_of(X152,X153)
| part_of(X153,X152)
| part_of(X152,X154)
| part_of(X154,X152) ),
inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c2])])]) ).
fof(i_0_38,plain,
! [X169,X170,X171,X172,X173] :
( ~ closed(X169)
| ~ meet(X172,X170,X171)
| X169 != sum(X170,X171)
| ~ end_point(X173,X170)
| meet(X173,X170,X171) ),
inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c7])])]) ).
fof(i_0_39,plain,
! [X201,X202,X203,X204,X205] :
( ( incident_o(X201,X202)
| ~ finish_point(X201,X202) )
& ( X201 = X203
| ~ incident_o(X203,X202)
| ordered_by(X202,X203,X201)
| ~ finish_point(X201,X202) )
& ( X204 != esk16_2(X204,X205)
| ~ incident_o(X204,X205)
| finish_point(X204,X205) )
& ( incident_o(esk16_2(X204,X205),X205)
| ~ incident_o(X204,X205)
| finish_point(X204,X205) )
& ( ~ ordered_by(X205,esk16_2(X204,X205),X204)
| ~ incident_o(X204,X205)
| finish_point(X204,X205) ) ),
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,
! [X195,X196,X197,X198,X199] :
( ( incident_o(X195,X196)
| ~ start_point(X195,X196) )
& ( X195 = X197
| ~ incident_o(X197,X196)
| ordered_by(X196,X195,X197)
| ~ start_point(X195,X196) )
& ( X198 != esk15_2(X198,X199)
| ~ incident_o(X198,X199)
| start_point(X198,X199) )
& ( incident_o(esk15_2(X198,X199),X199)
| ~ incident_o(X198,X199)
| start_point(X198,X199) )
& ( ~ ordered_by(X199,X198,esk15_2(X198,X199))
| ~ incident_o(X198,X199)
| start_point(X198,X199) ) ),
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,
! [X123,X124,X125,X126,X127,X128] :
( ( incident_c(X123,X124)
| ~ end_point(X123,X124) )
& ( ~ part_of(X125,X124)
| ~ part_of(X126,X124)
| ~ incident_c(X123,X125)
| ~ incident_c(X123,X126)
| part_of(X125,X126)
| part_of(X126,X125)
| ~ end_point(X123,X124) )
& ( part_of(esk3_2(X127,X128),X128)
| ~ incident_c(X127,X128)
| end_point(X127,X128) )
& ( part_of(esk4_2(X127,X128),X128)
| ~ incident_c(X127,X128)
| end_point(X127,X128) )
& ( incident_c(X127,esk3_2(X127,X128))
| ~ incident_c(X127,X128)
| end_point(X127,X128) )
& ( incident_c(X127,esk4_2(X127,X128))
| ~ incident_c(X127,X128)
| end_point(X127,X128) )
& ( ~ part_of(esk3_2(X127,X128),esk4_2(X127,X128))
| ~ incident_c(X127,X128)
| end_point(X127,X128) )
& ( ~ part_of(esk4_2(X127,X128),esk3_2(X127,X128))
| ~ incident_c(X127,X128)
| end_point(X127,X128) ) ),
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,
! [X239,X240,X241,X242,X243,X244] :
( ( ~ incident_o(X241,X240)
| incident_c(X241,X239)
| X239 != underlying_curve(X240) )
& ( ~ incident_c(X242,X239)
| incident_o(X242,X240)
| X239 != underlying_curve(X240) )
& ( ~ incident_o(esk24_2(X243,X244),X244)
| ~ incident_c(esk24_2(X243,X244),X243)
| X243 = underlying_curve(X244) )
& ( incident_o(esk24_2(X243,X244),X244)
| incident_c(esk24_2(X243,X244),X243)
| X243 = underlying_curve(X244) ) ),
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,
! [X158,X159] :
( ( meet(X159,esk9_2(X158,X159),esk10_2(X158,X159))
| ~ inner_point(X159,X158) )
& ( X158 = sum(esk9_2(X158,X159),esk10_2(X158,X159))
| ~ inner_point(X159,X158) ) ),
inference(distribute,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c4])])])]) ).
fof(i_0_44,plain,
! [X178,X179] :
( ( ~ incident_c(esk13_2(X178,X179),X178)
| ~ incident_c(esk13_2(X178,X179),X179)
| X178 = X179 )
& ( incident_c(esk13_2(X178,X179),X178)
| incident_c(esk13_2(X178,X179),X179)
| X178 = X179 ) ),
inference(distribute,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c9])])])]) ).
fof(i_0_45,plain,
! [X174,X175,X176] :
( ~ meet(X176,X174,X175)
| esk12_2(X174,X175) = sum(X174,X175) ),
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,
! [X207,X208,X209] :
( ( incident_o(X208,X207)
| ~ ordered_by(X207,X208,X209) )
& ( incident_o(X209,X207)
| ~ ordered_by(X207,X208,X209) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[o1])])]) ).
fof(i_0_47,plain,
! [X108,X109,X110,X111,X112] :
( ( ~ part_of(X109,X108)
| ~ incident_c(X110,X109)
| incident_c(X110,X108) )
& ( incident_c(esk1_2(X111,X112),X112)
| part_of(X112,X111) )
& ( ~ incident_c(esk1_2(X111,X112),X111)
| part_of(X112,X111) ) ),
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,
! [X162,X163,X164,X165] :
( ~ end_point(X163,X162)
| ~ end_point(X164,X162)
| ~ end_point(X165,X162)
| X163 = X164
| X163 = X165
| X164 = X165 ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c5])]) ).
fof(i_0_49,plain,
! [X166,X167] :
( ( end_point(esk11_2(X166,X167),X166)
| ~ end_point(X167,X166) )
& ( X167 != esk11_2(X166,X167)
| ~ end_point(X167,X166) ) ),
inference(distribute,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c6])])])]) ).
fof(i_0_50,plain,
! [X131,X132] :
( ( incident_c(X131,X132)
| ~ inner_point(X131,X132) )
& ( ~ end_point(X131,X132)
| ~ inner_point(X131,X132) )
& ( ~ incident_c(X131,X132)
| end_point(X131,X132)
| inner_point(X131,X132) ) ),
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,esk26_0),
inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[i_0_29])])]) ).
fof(i_0_52,plain,
! [X210,X212,X213] :
( open(esk17_1(X210))
& ( ~ incident_o(X212,X210)
| incident_c(X212,esk17_1(X210)) )
& ( ~ incident_c(X213,esk17_1(X210))
| incident_o(X213,X210) ) ),
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,
! [X141,X142,X143] :
( ( ~ closed(X141)
| ~ end_point(X142,X141) )
& ( end_point(esk6_1(X143),X143)
| closed(X143) ) ),
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,
! [X149,X150] :
( ~ part_of(X150,X149)
| X150 = X149
| open(X150) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c1])]) ).
fof(i_0_55,plain,
! [X145,X147,X148] :
( ( ~ open(X145)
| end_point(esk7_1(X145),X145) )
& ( ~ end_point(X148,X147)
| open(X147) ) ),
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,
! [X227] : start_point(esk20_1(X227),X227),
inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[o4])]) ).
fof(i_0_57,plain,
! [X156] : inner_point(esk8_1(X156),X156),
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,esk26_0,esk26_0),
inference(split_conjunct,[status(thm)],[i_0_51]),
[final] ).
cnf(i_0_126,plain,
( incident_o(X1,X2)
| ~ incident_c(X1,esk17_1(X2)) ),
inference(split_conjunct,[status(thm)],[i_0_52]),
[final] ).
cnf(i_0_127,plain,
( X1 != esk11_2(X2,X1)
| ~ end_point(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_49]),
[final] ).
cnf(i_0_128,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_129,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_130,plain,
( ~ end_point(X1,X2)
| ~ inner_point(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_50]),
[final] ).
cnf(i_0_131,plain,
( incident_c(X1,esk17_1(X2))
| ~ incident_o(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_52]),
[final] ).
cnf(i_0_132,plain,
( incident_o(X1,X2)
| ~ finish_point(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_39]),
[final] ).
cnf(i_0_133,plain,
( incident_o(X1,X2)
| ~ start_point(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_40]),
[final] ).
cnf(i_0_134,plain,
( incident_c(X1,X2)
| ~ inner_point(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_50]),
[final] ).
cnf(i_0_135,plain,
( incident_c(X1,X2)
| ~ end_point(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_41]),
[final] ).
cnf(i_0_136,plain,
( ~ closed(X1)
| ~ end_point(X2,X1) ),
inference(split_conjunct,[status(thm)],[i_0_53]),
[final] ).
cnf(i_0_137,plain,
( X1 = X2
| open(X1)
| ~ part_of(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_54]),
[final] ).
cnf(i_0_138,plain,
( end_point(esk7_1(X1),X1)
| ~ open(X1) ),
inference(split_conjunct,[status(thm)],[i_0_55]),
[final] ).
cnf(i_0_139,plain,
( open(X2)
| ~ end_point(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_55]),
[final] ).
cnf(i_0_140,plain,
( end_point(esk6_1(X1),X1)
| closed(X1) ),
inference(split_conjunct,[status(thm)],[i_0_53]),
[final] ).
cnf(i_0_141,plain,
start_point(esk20_1(X1),X1),
inference(split_conjunct,[status(thm)],[i_0_56]),
[final] ).
cnf(i_0_142,plain,
inner_point(esk8_1(X1),X1),
inference(split_conjunct,[status(thm)],[i_0_57]),
[final] ).
cnf(i_0_143,plain,
open(esk17_1(X1)),
inference(split_conjunct,[status(thm)],[i_0_52]),
[final] ).
cnf(i_0_144,axiom,
X1 = X1 ).
cnf(i_0_145,axiom,
( X1 = X2
| X2 != X1 ) ).
cnf(i_0_146,axiom,
( X1 = X2
| X1 != X3
| X3 != X2 ) ).
cnf(i_0_147,axiom,
( X1 != X2
| esk16_2(X1,X3) = esk16_2(X2,X3) ) ).
cnf(i_0_148,axiom,
( X1 != X2
| esk16_2(X3,X1) = esk16_2(X3,X2) ) ).
cnf(i_0_149,axiom,
( X1 != X2
| esk15_2(X1,X3) = esk15_2(X2,X3) ) ).
cnf(i_0_150,axiom,
( X1 != X2
| esk15_2(X3,X1) = esk15_2(X3,X2) ) ).
cnf(i_0_151,axiom,
( X1 != X2
| underlying_curve(X1) = underlying_curve(X2) ) ).
cnf(i_0_152,axiom,
( X1 != X2
| esk12_2(X1,X3) = esk12_2(X2,X3) ) ).
cnf(i_0_153,axiom,
( X1 != X2
| esk12_2(X3,X1) = esk12_2(X3,X2) ) ).
cnf(i_0_154,axiom,
( X1 != X2
| esk11_2(X1,X3) = esk11_2(X2,X3) ) ).
cnf(i_0_155,axiom,
( X1 != X2
| esk11_2(X3,X1) = esk11_2(X3,X2) ) ).
cnf(i_0_156,axiom,
( X1 != X2
| sum(X1,X3) = sum(X2,X3) ) ).
cnf(i_0_157,axiom,
( X1 != X2
| sum(X3,X1) = sum(X3,X2) ) ).
cnf(i_0_158,axiom,
( X1 != X2
| ~ between_o(X1,X3,X4,X5)
| between_o(X2,X3,X4,X5) ) ).
cnf(i_0_159,axiom,
( X1 != X2
| ~ between_o(X3,X1,X4,X5)
| between_o(X3,X2,X4,X5) ) ).
cnf(i_0_160,axiom,
( X1 != X2
| ~ between_o(X3,X4,X1,X5)
| between_o(X3,X4,X2,X5) ) ).
cnf(i_0_161,axiom,
( X1 != X2
| ~ between_o(X3,X4,X5,X1)
| between_o(X3,X4,X5,X2) ) ).
cnf(i_0_162,axiom,
( X1 != X2
| ~ open(X1)
| open(X2) ) ).
cnf(i_0_163,axiom,
( X1 != X2
| ~ closed(X1)
| closed(X2) ) ).
cnf(i_0_164,axiom,
( X1 != X2
| ~ finish_point(X1,X3)
| finish_point(X2,X3) ) ).
cnf(i_0_165,axiom,
( X1 != X2
| ~ finish_point(X3,X1)
| finish_point(X3,X2) ) ).
cnf(i_0_166,axiom,
( X1 != X2
| ~ start_point(X1,X3)
| start_point(X2,X3) ) ).
cnf(i_0_167,axiom,
( X1 != X2
| ~ start_point(X3,X1)
| start_point(X3,X2) ) ).
cnf(i_0_168,axiom,
( X1 != X2
| ~ incident_o(X1,X3)
| incident_o(X2,X3) ) ).
cnf(i_0_169,axiom,
( X1 != X2
| ~ incident_o(X3,X1)
| incident_o(X3,X2) ) ).
cnf(i_0_170,axiom,
( X1 != X2
| ~ incident_c(X1,X3)
| incident_c(X2,X3) ) ).
cnf(i_0_171,axiom,
( X1 != X2
| ~ incident_c(X3,X1)
| incident_c(X3,X2) ) ).
cnf(i_0_172,axiom,
( X1 != X2
| ~ between_c(X1,X3,X4,X5)
| between_c(X2,X3,X4,X5) ) ).
cnf(i_0_173,axiom,
( X1 != X2
| ~ between_c(X3,X1,X4,X5)
| between_c(X3,X2,X4,X5) ) ).
cnf(i_0_174,axiom,
( X1 != X2
| ~ between_c(X3,X4,X1,X5)
| between_c(X3,X4,X2,X5) ) ).
cnf(i_0_175,axiom,
( X1 != X2
| ~ between_c(X3,X4,X5,X1)
| between_c(X3,X4,X5,X2) ) ).
cnf(i_0_176,axiom,
( X1 != X2
| ~ part_of(X1,X3)
| part_of(X2,X3) ) ).
cnf(i_0_177,axiom,
( X1 != X2
| ~ part_of(X3,X1)
| part_of(X3,X2) ) ).
cnf(i_0_178,axiom,
( X1 != X2
| ~ inner_point(X1,X3)
| inner_point(X2,X3) ) ).
cnf(i_0_179,axiom,
( X1 != X2
| ~ inner_point(X3,X1)
| inner_point(X3,X2) ) ).
cnf(i_0_180,axiom,
( X1 != X2
| ~ end_point(X1,X3)
| end_point(X2,X3) ) ).
cnf(i_0_181,axiom,
( X1 != X2
| ~ end_point(X3,X1)
| end_point(X3,X2) ) ).
cnf(i_0_182,axiom,
( X1 != X2
| ~ ordered_by(X1,X3,X4)
| ordered_by(X2,X3,X4) ) ).
cnf(i_0_183,axiom,
( X1 != X2
| ~ ordered_by(X3,X1,X4)
| ordered_by(X3,X2,X4) ) ).
cnf(i_0_184,axiom,
( X1 != X2
| ~ ordered_by(X3,X4,X1)
| ordered_by(X3,X4,X2) ) ).
cnf(i_0_185,axiom,
( X1 != X2
| ~ meet(X1,X3,X4)
| meet(X2,X3,X4) ) ).
cnf(i_0_186,axiom,
( X1 != X2
| ~ meet(X3,X1,X4)
| meet(X3,X2,X4) ) ).
cnf(i_0_187,axiom,
( X1 != X2
| ~ meet(X3,X4,X1)
| meet(X3,X4,X2) ) ).
cnf(i_0_144_001,axiom,
X1 = X1 ).
cnf(i_0_145_002,axiom,
( X1 = X2
| X2 != X1 ) ).
cnf(i_0_146_003,axiom,
( X1 = X2
| X1 != X3
| X3 != X2 ) ).
cnf(i_0_147_004,axiom,
( X1 != X2
| esk16_2(X1,X3) = esk16_2(X2,X3) ) ).
cnf(i_0_148_005,axiom,
( X1 != X2
| esk16_2(X3,X1) = esk16_2(X3,X2) ) ).
cnf(i_0_149_006,axiom,
( X1 != X2
| esk15_2(X1,X3) = esk15_2(X2,X3) ) ).
cnf(i_0_150_007,axiom,
( X1 != X2
| esk15_2(X3,X1) = esk15_2(X3,X2) ) ).
cnf(i_0_151_008,axiom,
( X1 != X2
| underlying_curve(X1) = underlying_curve(X2) ) ).
cnf(i_0_152_009,axiom,
( X1 != X2
| esk12_2(X1,X3) = esk12_2(X2,X3) ) ).
cnf(i_0_153_010,axiom,
( X1 != X2
| esk12_2(X3,X1) = esk12_2(X3,X2) ) ).
cnf(i_0_154_011,axiom,
( X1 != X2
| esk11_2(X1,X3) = esk11_2(X2,X3) ) ).
cnf(i_0_155_012,axiom,
( X1 != X2
| esk11_2(X3,X1) = esk11_2(X3,X2) ) ).
cnf(i_0_156_013,axiom,
( X1 != X2
| sum(X1,X3) = sum(X2,X3) ) ).
cnf(i_0_157_014,axiom,
( X1 != X2
| sum(X3,X1) = sum(X3,X2) ) ).
cnf(i_0_158_015,axiom,
( X1 != X2
| ~ between_o(X1,X3,X4,X5)
| between_o(X2,X3,X4,X5) ) ).
cnf(i_0_159_016,axiom,
( X1 != X2
| ~ between_o(X3,X1,X4,X5)
| between_o(X3,X2,X4,X5) ) ).
cnf(i_0_160_017,axiom,
( X1 != X2
| ~ between_o(X3,X4,X1,X5)
| between_o(X3,X4,X2,X5) ) ).
cnf(i_0_161_018,axiom,
( X1 != X2
| ~ between_o(X3,X4,X5,X1)
| between_o(X3,X4,X5,X2) ) ).
cnf(i_0_162_019,axiom,
( X1 != X2
| ~ open(X1)
| open(X2) ) ).
cnf(i_0_163_020,axiom,
( X1 != X2
| ~ closed(X1)
| closed(X2) ) ).
cnf(i_0_164_021,axiom,
( X1 != X2
| ~ finish_point(X1,X3)
| finish_point(X2,X3) ) ).
cnf(i_0_165_022,axiom,
( X1 != X2
| ~ finish_point(X3,X1)
| finish_point(X3,X2) ) ).
cnf(i_0_166_023,axiom,
( X1 != X2
| ~ start_point(X1,X3)
| start_point(X2,X3) ) ).
cnf(i_0_167_024,axiom,
( X1 != X2
| ~ start_point(X3,X1)
| start_point(X3,X2) ) ).
cnf(i_0_168_025,axiom,
( X1 != X2
| ~ incident_o(X1,X3)
| incident_o(X2,X3) ) ).
cnf(i_0_169_026,axiom,
( X1 != X2
| ~ incident_o(X3,X1)
| incident_o(X3,X2) ) ).
cnf(i_0_170_027,axiom,
( X1 != X2
| ~ incident_c(X1,X3)
| incident_c(X2,X3) ) ).
cnf(i_0_171_028,axiom,
( X1 != X2
| ~ incident_c(X3,X1)
| incident_c(X3,X2) ) ).
cnf(i_0_172_029,axiom,
( X1 != X2
| ~ between_c(X1,X3,X4,X5)
| between_c(X2,X3,X4,X5) ) ).
cnf(i_0_173_030,axiom,
( X1 != X2
| ~ between_c(X3,X1,X4,X5)
| between_c(X3,X2,X4,X5) ) ).
cnf(i_0_174_031,axiom,
( X1 != X2
| ~ between_c(X3,X4,X1,X5)
| between_c(X3,X4,X2,X5) ) ).
cnf(i_0_175_032,axiom,
( X1 != X2
| ~ between_c(X3,X4,X5,X1)
| between_c(X3,X4,X5,X2) ) ).
cnf(i_0_176_033,axiom,
( X1 != X2
| ~ part_of(X1,X3)
| part_of(X2,X3) ) ).
cnf(i_0_177_034,axiom,
( X1 != X2
| ~ part_of(X3,X1)
| part_of(X3,X2) ) ).
cnf(i_0_178_035,axiom,
( X1 != X2
| ~ inner_point(X1,X3)
| inner_point(X2,X3) ) ).
cnf(i_0_179_036,axiom,
( X1 != X2
| ~ inner_point(X3,X1)
| inner_point(X3,X2) ) ).
cnf(i_0_180_037,axiom,
( X1 != X2
| ~ end_point(X1,X3)
| end_point(X2,X3) ) ).
cnf(i_0_181_038,axiom,
( X1 != X2
| ~ end_point(X3,X1)
| end_point(X3,X2) ) ).
cnf(i_0_182_039,axiom,
( X1 != X2
| ~ ordered_by(X1,X3,X4)
| ordered_by(X2,X3,X4) ) ).
cnf(i_0_183_040,axiom,
( X1 != X2
| ~ ordered_by(X3,X1,X4)
| ordered_by(X3,X2,X4) ) ).
cnf(i_0_184_041,axiom,
( X1 != X2
| ~ ordered_by(X3,X4,X1)
| ordered_by(X3,X4,X2) ) ).
cnf(i_0_185_042,axiom,
( X1 != X2
| ~ meet(X1,X3,X4)
| meet(X2,X3,X4) ) ).
cnf(i_0_186_043,axiom,
( X1 != X2
| ~ meet(X3,X1,X4)
| meet(X3,X2,X4) ) ).
cnf(i_0_187_044,axiom,
( X1 != X2
| ~ meet(X3,X4,X1)
| meet(X3,X4,X2) ) ).
cnf(i_0_188,plain,
~ between_c(X1,X2,X3,X2),
inference(equality_inference,[],[76]) ).
cnf(i_0_189,plain,
( ~ end_point(X1,X2)
| meet(X1,X2,X3)
| ~ meet(X4,X2,X3)
| ~ closed(sum(X2,X3)) ),
inference(equality_inference,[],[87]) ).
cnf(i_0_190,plain,
( incident_c(X1,X2)
| incident_c(X1,X3)
| ~ incident_c(X1,sum(X2,X3)) ),
inference(equality_inference,[],[115]) ).
cnf(i_0_191,plain,
( incident_c(X1,sum(X2,X3))
| ~ incident_c(X1,X2) ),
inference(equality_inference,[],[120]) ).
cnf(i_0_192,plain,
( incident_c(X1,sum(X2,X3))
| ~ incident_c(X1,X3) ),
inference(equality_inference,[],[121]) ).
cnf(i_0_193,plain,
( incident_o(X1,X2)
| ~ incident_c(X1,underlying_curve(X2)) ),
inference(equality_inference,[],[128]) ).
cnf(i_0_194,plain,
( incident_c(X1,underlying_curve(X2))
| ~ incident_o(X1,X2) ),
inference(equality_inference,[],[129]) ).
cnf(i_0_195,plain,
~ between_o(X1,X2,X3,X2),
inference(scs_inference,[],[i_0_188,i_0_61]) ).
cnf(i_0_196,plain,
~ between_c(X1,X2,X3,X2),
inference(rename_variables,[],[i_0_188]) ).
cnf(i_0_197,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_198,plain,
incident_c(esk8_1(X1),X1),
inference(scs_inference,[],[i_0_188,i_0_142,i_0_61,i_0_134]) ).
cnf(i_0_199,plain,
( ~ inner_point(X1,X2)
| incident_c(X1,X2) ),
inference(rename_variables,[],[i_0_134]) ).
cnf(i_0_200,plain,
incident_c(esk8_1(X1),sum(X1,X2)),
inference(scs_inference,[],[i_0_188,i_0_142,i_0_61,i_0_134,i_0_191]) ).
cnf(i_0_201,plain,
( ~ incident_c(X1,X2)
| incident_c(X1,sum(X2,X3)) ),
inference(rename_variables,[],[i_0_191]) ).
cnf(i_0_202,plain,
incident_c(esk8_1(X1),sum(X2,X1)),
inference(scs_inference,[],[i_0_188,i_0_142,i_0_61,i_0_134,i_0_191,i_0_192]) ).
cnf(i_0_203,plain,
( ~ incident_c(X1,X2)
| incident_c(X1,sum(X3,X2)) ),
inference(rename_variables,[],[i_0_192]) ).
cnf(i_0_204,plain,
incident_o(esk8_1(esk17_1(X1)),X1),
inference(scs_inference,[],[i_0_188,i_0_142,i_0_61,i_0_134,i_0_191,i_0_192,i_0_126]) ).
cnf(i_0_205,plain,
( ~ incident_c(X1,esk17_1(X2))
| incident_o(X1,X2) ),
inference(rename_variables,[],[i_0_126]) ).
cnf(i_0_206,plain,
~ end_point(esk8_1(esk17_1(X1)),esk17_1(X1)),
inference(scs_inference,[],[i_0_188,i_0_142,i_0_61,i_0_134,i_0_191,i_0_192,i_0_126,i_0_130]) ).
cnf(i_0_207,plain,
inner_point(esk8_1(X1),X1),
inference(rename_variables,[],[i_0_142]) ).
cnf(i_0_208,plain,
( ~ inner_point(X1,X2)
| ~ end_point(X1,X2) ),
inference(rename_variables,[],[i_0_130]) ).
cnf(i_0_209,plain,
incident_o(esk20_1(X1),X1),
inference(scs_inference,[],[i_0_188,i_0_141,i_0_142,i_0_61,i_0_134,i_0_191,i_0_192,i_0_126,i_0_130,i_0_133]) ).
cnf(i_0_210,plain,
( ~ start_point(X1,X2)
| incident_o(X1,X2) ),
inference(rename_variables,[],[i_0_133]) ).
cnf(i_0_211,plain,
$false,
inference(scs_inference,[],[i_0_125,i_0_188,i_0_141,i_0_142,i_0_61,i_0_134,i_0_191,i_0_192,i_0_126,i_0_130,i_0_133,i_0_72]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.12/0.13 % Problem : GEO117+1 : TPTP v9.2.1. Released v2.4.0.
% 0.12/0.13 % 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.34 % Computer : n006.cluster.edu
% 0.15/0.34 % Model : x86_64 x86_64
% 0.15/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.34 % Memory : 8042.1875MB
% 0.15/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.15/0.34 % CPULimit : 300
% 0.15/0.34 % WCLimit : 300
% 0.15/0.34 % DateTime : Mon May 4 17:43:16 EDT 2026
% 0.15/0.34 % CPUTime :
% 0.15/0.35 % start to proof: theBenchmark
% 0.34/1.62 % Version : CSE_E---1.7
% 0.34/1.62 % Problem : theBenchmark.p
% 0.34/1.62 % SZS status Theorem for theBenchmark.p
% 0.34/1.62 % SZS output start CNFRefutation
% See solution above
% 0.34/1.68 % Total time : 1.273s
%------------------------------------------------------------------------------