%------------------------------------------------------------------------------
% File : CSE_E---1.7
% Problem : GEO112+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 : n003.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:20 PM UTC 2026
% Result : Theorem 38.94s 26.08s
% Output : CNFRefutation 40.46s
% Verified :
% SZS Type : ERROR: Analysing output (Could not find formula named 53)
% Comments :
%------------------------------------------------------------------------------
fof(theorem_3_8_2,conjecture,
! [X1,X3,X5,X7] :
( between_c(X1,X3,X5,X7)
=> between_c(X1,X7,X5,X3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',theorem_3_8_2) ).
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(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(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(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(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(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(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(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(c3,axiom,
! [X1] :
? [X3] : inner_point(X3,X1),
file('/export/starexec/sandbox/benchmark/Axioms/GEO004+0.ax',c3) ).
fof(i_0_18,negated_conjecture,
~ ! [X1,X3,X5,X7] :
( between_c(X1,X3,X5,X7)
=> between_c(X1,X7,X5,X3) ),
inference(assume_negation,[status(cth)],[theorem_3_8_2]) ).
fof(i_0_19,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_20,plain,
! [X144,X145,X146,X147,X149,X150,X151,X152,X153] :
( ( X145 != X147
| ~ between_c(X144,X145,X146,X147) )
& ( part_of(esk14_4(X144,X145,X146,X147),X144)
| ~ between_c(X144,X145,X146,X147) )
& ( end_point(X145,esk14_4(X144,X145,X146,X147))
| ~ between_c(X144,X145,X146,X147) )
& ( end_point(X147,esk14_4(X144,X145,X146,X147))
| ~ between_c(X144,X145,X146,X147) )
& ( inner_point(X146,esk14_4(X144,X145,X146,X147))
| ~ between_c(X144,X145,X146,X147) )
& ( X150 = X152
| ~ part_of(X153,X149)
| ~ end_point(X150,X153)
| ~ end_point(X152,X153)
| ~ inner_point(X151,X153)
| between_c(X149,X150,X151,X152) ) ),
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_21,plain,
! [X96,X97,X98,X99,X100,X101,X102] :
( ( incident_c(X96,X97)
| ~ meet(X96,X97,X98) )
& ( incident_c(X96,X98)
| ~ meet(X96,X97,X98) )
& ( end_point(X99,X97)
| ~ incident_c(X99,X97)
| ~ incident_c(X99,X98)
| ~ meet(X96,X97,X98) )
& ( end_point(X99,X98)
| ~ incident_c(X99,X97)
| ~ incident_c(X99,X98)
| ~ meet(X96,X97,X98) )
& ( incident_c(esk5_3(X100,X101,X102),X101)
| ~ incident_c(X100,X101)
| ~ incident_c(X100,X102)
| meet(X100,X101,X102) )
& ( incident_c(esk5_3(X100,X101,X102),X102)
| ~ incident_c(X100,X101)
| ~ incident_c(X100,X102)
| meet(X100,X101,X102) )
& ( ~ end_point(esk5_3(X100,X101,X102),X101)
| ~ end_point(esk5_3(X100,X101,X102),X102)
| ~ incident_c(X100,X101)
| ~ incident_c(X100,X102)
| meet(X100,X101,X102) ) ),
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_22,plain,
! [X77,X78,X79,X80,X81,X82,X83,X84] :
( ( ~ incident_c(X80,X77)
| incident_c(X80,X78)
| incident_c(X80,X79)
| X77 != sum(X78,X79) )
& ( ~ incident_c(X81,X78)
| incident_c(X81,X77)
| X77 != sum(X78,X79) )
& ( ~ incident_c(X81,X79)
| incident_c(X81,X77)
| X77 != sum(X78,X79) )
& ( ~ incident_c(esk2_3(X82,X83,X84),X83)
| ~ incident_c(esk2_3(X82,X83,X84),X82)
| X82 = sum(X83,X84) )
& ( ~ incident_c(esk2_3(X82,X83,X84),X84)
| ~ incident_c(esk2_3(X82,X83,X84),X82)
| X82 = sum(X83,X84) )
& ( incident_c(esk2_3(X82,X83,X84),X82)
| incident_c(esk2_3(X82,X83,X84),X83)
| incident_c(esk2_3(X82,X83,X84),X84)
| X82 = sum(X83,X84) ) ),
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_23,negated_conjecture,
( between_c(esk15_0,esk16_0,esk17_0,esk18_0)
& ~ between_c(esk15_0,esk18_0,esk17_0,esk16_0) ),
inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[i_0_18])])]) ).
fof(i_0_24,plain,
! [X114,X115,X116,X117,X118] :
( ~ part_of(X115,X114)
| ~ part_of(X116,X114)
| ~ part_of(X117,X114)
| ~ end_point(X118,X115)
| ~ end_point(X118,X116)
| ~ end_point(X118,X117)
| part_of(X116,X117)
| part_of(X117,X116)
| part_of(X115,X116)
| part_of(X116,X115)
| part_of(X115,X117)
| part_of(X117,X115) ),
inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c2])])]) ).
fof(i_0_25,plain,
! [X132,X133,X134,X135,X136] :
( ~ closed(X132)
| ~ meet(X135,X133,X134)
| X132 != sum(X133,X134)
| ~ end_point(X136,X133)
| meet(X136,X133,X134) ),
inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c7])])]) ).
fof(i_0_26,plain,
! [X86,X87,X88,X89,X90,X91] :
( ( incident_c(X86,X87)
| ~ end_point(X86,X87) )
& ( ~ part_of(X88,X87)
| ~ part_of(X89,X87)
| ~ incident_c(X86,X88)
| ~ incident_c(X86,X89)
| part_of(X88,X89)
| part_of(X89,X88)
| ~ end_point(X86,X87) )
& ( part_of(esk3_2(X90,X91),X91)
| ~ incident_c(X90,X91)
| end_point(X90,X91) )
& ( part_of(esk4_2(X90,X91),X91)
| ~ incident_c(X90,X91)
| end_point(X90,X91) )
& ( incident_c(X90,esk3_2(X90,X91))
| ~ incident_c(X90,X91)
| end_point(X90,X91) )
& ( incident_c(X90,esk4_2(X90,X91))
| ~ incident_c(X90,X91)
| end_point(X90,X91) )
& ( ~ part_of(esk3_2(X90,X91),esk4_2(X90,X91))
| ~ incident_c(X90,X91)
| end_point(X90,X91) )
& ( ~ part_of(esk4_2(X90,X91),esk3_2(X90,X91))
| ~ incident_c(X90,X91)
| end_point(X90,X91) ) ),
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_27,plain,
! [X121,X122] :
( ( meet(X122,esk9_2(X121,X122),esk10_2(X121,X122))
| ~ inner_point(X122,X121) )
& ( X121 = sum(esk9_2(X121,X122),esk10_2(X121,X122))
| ~ inner_point(X122,X121) ) ),
inference(distribute,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c4])])])]) ).
fof(i_0_28,plain,
! [X141,X142] :
( ( ~ incident_c(esk13_2(X141,X142),X141)
| ~ incident_c(esk13_2(X141,X142),X142)
| X141 = X142 )
& ( incident_c(esk13_2(X141,X142),X141)
| incident_c(esk13_2(X141,X142),X142)
| X141 = X142 ) ),
inference(distribute,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c9])])])]) ).
fof(i_0_29,plain,
! [X137,X138,X139] :
( ~ meet(X139,X137,X138)
| esk12_2(X137,X138) = sum(X137,X138) ),
inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c8])])])]) ).
fof(i_0_30,plain,
! [X71,X72,X73,X74,X75] :
( ( ~ part_of(X72,X71)
| ~ incident_c(X73,X72)
| incident_c(X73,X71) )
& ( incident_c(esk1_2(X74,X75),X75)
| part_of(X75,X74) )
& ( ~ incident_c(esk1_2(X74,X75),X74)
| part_of(X75,X74) ) ),
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_31,plain,
! [X125,X126,X127,X128] :
( ~ end_point(X126,X125)
| ~ end_point(X127,X125)
| ~ end_point(X128,X125)
| X126 = X127
| X126 = X128
| X127 = X128 ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c5])]) ).
fof(i_0_32,plain,
! [X129,X130] :
( ( end_point(esk11_2(X129,X130),X129)
| ~ end_point(X130,X129) )
& ( X130 != esk11_2(X129,X130)
| ~ end_point(X130,X129) ) ),
inference(distribute,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c6])])])]) ).
fof(i_0_33,plain,
! [X94,X95] :
( ( incident_c(X94,X95)
| ~ inner_point(X94,X95) )
& ( ~ end_point(X94,X95)
| ~ inner_point(X94,X95) )
& ( ~ incident_c(X94,X95)
| end_point(X94,X95)
| inner_point(X94,X95) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[i_0_19])])]) ).
fof(i_0_34,plain,
! [X104,X105,X106] :
( ( ~ closed(X104)
| ~ end_point(X105,X104) )
& ( end_point(esk6_1(X106),X106)
| closed(X106) ) ),
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_35,plain,
! [X112,X113] :
( ~ part_of(X113,X112)
| X113 = X112
| open(X113) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c1])]) ).
fof(i_0_36,plain,
! [X108,X110,X111] :
( ( ~ open(X108)
| end_point(esk7_1(X108),X108) )
& ( ~ end_point(X111,X110)
| open(X110) ) ),
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_37,plain,
! [X119] : inner_point(esk8_1(X119),X119),
inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[c3])]) ).
cnf(i_0_38,plain,
( part_of(esk14_4(X1,X2,X3,X4),X1)
| ~ between_c(X1,X2,X3,X4) ),
inference(split_conjunct,[status(thm)],[i_0_20]),
[final] ).
cnf(i_0_39,plain,
( inner_point(X1,esk14_4(X2,X3,X1,X4))
| ~ between_c(X2,X3,X1,X4) ),
inference(split_conjunct,[status(thm)],[i_0_20]),
[final] ).
cnf(i_0_40,plain,
( end_point(X1,esk14_4(X2,X1,X3,X4))
| ~ between_c(X2,X1,X3,X4) ),
inference(split_conjunct,[status(thm)],[i_0_20]),
[final] ).
cnf(i_0_41,plain,
( end_point(X1,esk14_4(X2,X3,X4,X1))
| ~ between_c(X2,X3,X4,X1) ),
inference(split_conjunct,[status(thm)],[i_0_20]),
[final] ).
cnf(i_0_42,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_21]),
[final] ).
cnf(i_0_43,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_22]),
[final] ).
cnf(i_0_44,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_22]),
[final] ).
cnf(i_0_45,plain,
( X1 != X2
| ~ between_c(X3,X1,X4,X2) ),
inference(split_conjunct,[status(thm)],[i_0_20]),
[final] ).
cnf(i_0_46,negated_conjecture,
~ between_c(esk15_0,esk18_0,esk17_0,esk16_0),
inference(split_conjunct,[status(thm)],[i_0_23]),
[final] ).
cnf(i_0_47,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_22]),
[final] ).
cnf(i_0_48,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_20]),
[final] ).
cnf(i_0_49,negated_conjecture,
between_c(esk15_0,esk16_0,esk17_0,esk18_0),
inference(split_conjunct,[status(thm)],[i_0_23]),
[final] ).
cnf(i_0_50,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_24]),
[final] ).
cnf(i_0_51,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_21]),
[final] ).
cnf(i_0_52,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_21]),
[final] ).
cnf(i_0_53,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_25]),
[final] ).
cnf(i_0_54,plain,
( end_point(X1,X2)
| ~ incident_c(X1,X2)
| ~ incident_c(X1,X3)
| ~ meet(X4,X2,X3) ),
inference(split_conjunct,[status(thm)],[i_0_21]),
[final] ).
cnf(i_0_55,plain,
( end_point(X1,X2)
| ~ incident_c(X1,X3)
| ~ incident_c(X1,X2)
| ~ meet(X4,X3,X2) ),
inference(split_conjunct,[status(thm)],[i_0_21]),
[final] ).
cnf(i_0_56,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_26]),
[final] ).
cnf(i_0_57,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_26]),
[final] ).
cnf(i_0_58,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_26]),
[final] ).
cnf(i_0_59,plain,
( meet(X1,esk9_2(X2,X1),esk10_2(X2,X1))
| ~ inner_point(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_27]),
[final] ).
cnf(i_0_60,plain,
( X1 = X2
| ~ incident_c(esk13_2(X1,X2),X1)
| ~ incident_c(esk13_2(X1,X2),X2) ),
inference(split_conjunct,[status(thm)],[i_0_28]),
[final] ).
cnf(i_0_61,plain,
( esk12_2(X2,X3) = sum(X2,X3)
| ~ meet(X1,X2,X3) ),
inference(split_conjunct,[status(thm)],[i_0_29]),
[final] ).
cnf(i_0_62,plain,
( incident_c(X1,X2)
| ~ meet(X1,X2,X3) ),
inference(split_conjunct,[status(thm)],[i_0_21]),
[final] ).
cnf(i_0_63,plain,
( incident_c(X1,X2)
| ~ meet(X1,X3,X2) ),
inference(split_conjunct,[status(thm)],[i_0_21]),
[final] ).
cnf(i_0_64,plain,
( X1 = sum(esk9_2(X1,X2),esk10_2(X1,X2))
| ~ inner_point(X2,X1) ),
inference(split_conjunct,[status(thm)],[i_0_27]),
[final] ).
cnf(i_0_65,plain,
( incident_c(esk13_2(X1,X2),X1)
| incident_c(esk13_2(X1,X2),X2)
| X1 = X2 ),
inference(split_conjunct,[status(thm)],[i_0_28]),
[final] ).
cnf(i_0_66,plain,
( part_of(X2,X1)
| ~ incident_c(esk1_2(X1,X2),X1) ),
inference(split_conjunct,[status(thm)],[i_0_30]),
[final] ).
cnf(i_0_67,plain,
( part_of(esk4_2(X1,X2),X2)
| end_point(X1,X2)
| ~ incident_c(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_26]),
[final] ).
cnf(i_0_68,plain,
( part_of(esk3_2(X1,X2),X2)
| end_point(X1,X2)
| ~ incident_c(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_26]),
[final] ).
cnf(i_0_69,plain,
( incident_c(X1,esk4_2(X1,X2))
| end_point(X1,X2)
| ~ incident_c(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_26]),
[final] ).
cnf(i_0_70,plain,
( incident_c(X1,esk3_2(X1,X2))
| end_point(X1,X2)
| ~ incident_c(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_26]),
[final] ).
cnf(i_0_71,plain,
( incident_c(X1,X3)
| incident_c(X1,X4)
| ~ incident_c(X1,X2)
| X2 != sum(X3,X4) ),
inference(split_conjunct,[status(thm)],[i_0_22]),
[final] ).
cnf(i_0_72,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_31]),
[final] ).
cnf(i_0_73,plain,
( end_point(esk11_2(X1,X2),X1)
| ~ end_point(X2,X1) ),
inference(split_conjunct,[status(thm)],[i_0_32]),
[final] ).
cnf(i_0_74,plain,
( incident_c(X1,X3)
| ~ incident_c(X1,X2)
| X3 != sum(X2,X4) ),
inference(split_conjunct,[status(thm)],[i_0_22]),
[final] ).
cnf(i_0_75,plain,
( incident_c(X1,X3)
| ~ incident_c(X1,X2)
| X3 != sum(X4,X2) ),
inference(split_conjunct,[status(thm)],[i_0_22]),
[final] ).
cnf(i_0_76,plain,
( incident_c(X3,X2)
| ~ part_of(X1,X2)
| ~ incident_c(X3,X1) ),
inference(split_conjunct,[status(thm)],[i_0_30]),
[final] ).
cnf(i_0_77,plain,
( incident_c(esk1_2(X1,X2),X2)
| part_of(X2,X1) ),
inference(split_conjunct,[status(thm)],[i_0_30]),
[final] ).
cnf(i_0_78,plain,
( end_point(X1,X2)
| inner_point(X1,X2)
| ~ incident_c(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_33]),
[final] ).
cnf(i_0_79,plain,
( X1 != esk11_2(X2,X1)
| ~ end_point(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_32]),
[final] ).
cnf(i_0_80,plain,
( ~ end_point(X1,X2)
| ~ inner_point(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_33]),
[final] ).
cnf(i_0_81,plain,
( incident_c(X1,X2)
| ~ inner_point(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_33]),
[final] ).
cnf(i_0_82,plain,
( incident_c(X1,X2)
| ~ end_point(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_26]),
[final] ).
cnf(i_0_83,plain,
( ~ closed(X1)
| ~ end_point(X2,X1) ),
inference(split_conjunct,[status(thm)],[i_0_34]),
[final] ).
cnf(i_0_84,plain,
( X1 = X2
| open(X1)
| ~ part_of(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_35]),
[final] ).
cnf(i_0_85,plain,
( end_point(esk7_1(X1),X1)
| ~ open(X1) ),
inference(split_conjunct,[status(thm)],[i_0_36]),
[final] ).
cnf(i_0_86,plain,
( open(X2)
| ~ end_point(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_36]),
[final] ).
cnf(i_0_87,plain,
( end_point(esk6_1(X1),X1)
| closed(X1) ),
inference(split_conjunct,[status(thm)],[i_0_34]),
[final] ).
cnf(i_0_88,plain,
inner_point(esk8_1(X1),X1),
inference(split_conjunct,[status(thm)],[i_0_37]),
[final] ).
cnf(i_0_89,axiom,
X1 = X1 ).
cnf(i_0_90,axiom,
( X1 = X2
| X2 != X1 ) ).
cnf(i_0_91,axiom,
( X1 = X2
| X1 != X3
| X3 != X2 ) ).
cnf(i_0_92,axiom,
( X1 != X2
| esk12_2(X1,X3) = esk12_2(X2,X3) ) ).
cnf(i_0_93,axiom,
( X1 != X2
| esk12_2(X3,X1) = esk12_2(X3,X2) ) ).
cnf(i_0_94,axiom,
( X1 != X2
| esk11_2(X1,X3) = esk11_2(X2,X3) ) ).
cnf(i_0_95,axiom,
( X1 != X2
| esk11_2(X3,X1) = esk11_2(X3,X2) ) ).
cnf(i_0_96,axiom,
( X1 != X2
| sum(X1,X3) = sum(X2,X3) ) ).
cnf(i_0_97,axiom,
( X1 != X2
| sum(X3,X1) = sum(X3,X2) ) ).
cnf(i_0_98,axiom,
( X1 != X2
| ~ part_of(X1,X3)
| part_of(X2,X3) ) ).
cnf(i_0_99,axiom,
( X1 != X2
| ~ part_of(X3,X1)
| part_of(X3,X2) ) ).
cnf(i_0_100,axiom,
( X1 != X2
| ~ between_c(X1,X3,X4,X5)
| between_c(X2,X3,X4,X5) ) ).
cnf(i_0_101,axiom,
( X1 != X2
| ~ between_c(X3,X1,X4,X5)
| between_c(X3,X2,X4,X5) ) ).
cnf(i_0_102,axiom,
( X1 != X2
| ~ between_c(X3,X4,X1,X5)
| between_c(X3,X4,X2,X5) ) ).
cnf(i_0_103,axiom,
( X1 != X2
| ~ between_c(X3,X4,X5,X1)
| between_c(X3,X4,X5,X2) ) ).
cnf(i_0_104,axiom,
( X1 != X2
| ~ inner_point(X1,X3)
| inner_point(X2,X3) ) ).
cnf(i_0_105,axiom,
( X1 != X2
| ~ inner_point(X3,X1)
| inner_point(X3,X2) ) ).
cnf(i_0_106,axiom,
( X1 != X2
| ~ end_point(X1,X3)
| end_point(X2,X3) ) ).
cnf(i_0_107,axiom,
( X1 != X2
| ~ end_point(X3,X1)
| end_point(X3,X2) ) ).
cnf(i_0_108,axiom,
( X1 != X2
| ~ meet(X1,X3,X4)
| meet(X2,X3,X4) ) ).
cnf(i_0_109,axiom,
( X1 != X2
| ~ meet(X3,X1,X4)
| meet(X3,X2,X4) ) ).
cnf(i_0_110,axiom,
( X1 != X2
| ~ meet(X3,X4,X1)
| meet(X3,X4,X2) ) ).
cnf(i_0_111,axiom,
( X1 != X2
| ~ incident_c(X1,X3)
| incident_c(X2,X3) ) ).
cnf(i_0_112,axiom,
( X1 != X2
| ~ incident_c(X3,X1)
| incident_c(X3,X2) ) ).
cnf(i_0_113,axiom,
( X1 != X2
| ~ closed(X1)
| closed(X2) ) ).
cnf(i_0_114,axiom,
( X1 != X2
| ~ open(X1)
| open(X2) ) ).
cnf(i_0_89_001,axiom,
X1 = X1 ).
cnf(i_0_90_002,axiom,
( X1 = X2
| X2 != X1 ) ).
cnf(i_0_91_003,axiom,
( X1 = X2
| X1 != X3
| X3 != X2 ) ).
cnf(i_0_92_004,axiom,
( X1 != X2
| esk12_2(X1,X3) = esk12_2(X2,X3) ) ).
cnf(i_0_93_005,axiom,
( X1 != X2
| esk12_2(X3,X1) = esk12_2(X3,X2) ) ).
cnf(i_0_94_006,axiom,
( X1 != X2
| esk11_2(X1,X3) = esk11_2(X2,X3) ) ).
cnf(i_0_95_007,axiom,
( X1 != X2
| esk11_2(X3,X1) = esk11_2(X3,X2) ) ).
cnf(i_0_96_008,axiom,
( X1 != X2
| sum(X1,X3) = sum(X2,X3) ) ).
cnf(i_0_97_009,axiom,
( X1 != X2
| sum(X3,X1) = sum(X3,X2) ) ).
cnf(i_0_98_010,axiom,
( X1 != X2
| ~ part_of(X1,X3)
| part_of(X2,X3) ) ).
cnf(i_0_99_011,axiom,
( X1 != X2
| ~ part_of(X3,X1)
| part_of(X3,X2) ) ).
cnf(i_0_100_012,axiom,
( X1 != X2
| ~ between_c(X1,X3,X4,X5)
| between_c(X2,X3,X4,X5) ) ).
cnf(i_0_101_013,axiom,
( X1 != X2
| ~ between_c(X3,X1,X4,X5)
| between_c(X3,X2,X4,X5) ) ).
cnf(i_0_102_014,axiom,
( X1 != X2
| ~ between_c(X3,X4,X1,X5)
| between_c(X3,X4,X2,X5) ) ).
cnf(i_0_103_015,axiom,
( X1 != X2
| ~ between_c(X3,X4,X5,X1)
| between_c(X3,X4,X5,X2) ) ).
cnf(i_0_104_016,axiom,
( X1 != X2
| ~ inner_point(X1,X3)
| inner_point(X2,X3) ) ).
cnf(i_0_105_017,axiom,
( X1 != X2
| ~ inner_point(X3,X1)
| inner_point(X3,X2) ) ).
cnf(i_0_106_018,axiom,
( X1 != X2
| ~ end_point(X1,X3)
| end_point(X2,X3) ) ).
cnf(i_0_107_019,axiom,
( X1 != X2
| ~ end_point(X3,X1)
| end_point(X3,X2) ) ).
cnf(i_0_108_020,axiom,
( X1 != X2
| ~ meet(X1,X3,X4)
| meet(X2,X3,X4) ) ).
cnf(i_0_109_021,axiom,
( X1 != X2
| ~ meet(X3,X1,X4)
| meet(X3,X2,X4) ) ).
cnf(i_0_110_022,axiom,
( X1 != X2
| ~ meet(X3,X4,X1)
| meet(X3,X4,X2) ) ).
cnf(i_0_111_023,axiom,
( X1 != X2
| ~ incident_c(X1,X3)
| incident_c(X2,X3) ) ).
cnf(i_0_112_024,axiom,
( X1 != X2
| ~ incident_c(X3,X1)
| incident_c(X3,X2) ) ).
cnf(i_0_113_025,axiom,
( X1 != X2
| ~ closed(X1)
| closed(X2) ) ).
cnf(i_0_114_026,axiom,
( X1 != X2
| ~ open(X1)
| open(X2) ) ).
cnf(i_0_115,plain,
~ between_c(X1,X2,X3,X2),
inference(equality_inference,[],[45]) ).
cnf(i_0_116,plain,
( ~ end_point(X1,X2)
| meet(X1,X2,X3)
| ~ meet(X4,X2,X3)
| ~ closed(sum(X2,X3)) ),
inference(equality_inference,[],[53]) ).
cnf(i_0_117,plain,
( incident_c(X1,X2)
| incident_c(X1,X3)
| ~ incident_c(X1,sum(X2,X3)) ),
inference(equality_inference,[],[71]) ).
cnf(i_0_118,plain,
( incident_c(X1,sum(X2,X3))
| ~ incident_c(X1,X2) ),
inference(equality_inference,[],[74]) ).
cnf(i_0_119,plain,
( incident_c(X1,sum(X2,X3))
| ~ incident_c(X1,X3) ),
inference(equality_inference,[],[75]) ).
cnf(i_0_120,plain,
~ end_point(esk8_1(X1),X1),
inference(scs_inference,[],[i_0_88,i_0_80]) ).
cnf(i_0_121,plain,
( ~ inner_point(X1,X2)
| ~ end_point(X1,X2) ),
inference(rename_variables,[],[i_0_80]) ).
cnf(i_0_122,plain,
incident_c(esk8_1(X1),X1),
inference(scs_inference,[],[i_0_88,i_0_80,i_0_81]) ).
cnf(i_0_123,plain,
( ~ inner_point(X1,X2)
| incident_c(X1,X2) ),
inference(rename_variables,[],[i_0_81]) ).
cnf(i_0_124,plain,
incident_c(esk8_1(X1),sum(X1,X2)),
inference(scs_inference,[],[i_0_88,i_0_80,i_0_81,i_0_118]) ).
cnf(i_0_125,plain,
( ~ incident_c(X1,X2)
| incident_c(X1,sum(X2,X3)) ),
inference(rename_variables,[],[i_0_118]) ).
cnf(i_0_126,plain,
incident_c(esk8_1(X1),sum(X2,X1)),
inference(scs_inference,[],[i_0_88,i_0_80,i_0_81,i_0_118,i_0_119]) ).
cnf(i_0_127,plain,
( ~ incident_c(X1,X2)
| incident_c(X1,sum(X3,X2)) ),
inference(rename_variables,[],[i_0_119]) ).
cnf(i_0_128,plain,
esk16_0 != esk18_0,
inference(scs_inference,[],[i_0_49,i_0_115,i_0_88,i_0_80,i_0_81,i_0_118,i_0_119,i_0_101]) ).
cnf(i_0_129,plain,
~ between_c(X1,X2,X3,X2),
inference(rename_variables,[],[i_0_115]) ).
cnf(i_0_130,plain,
esk18_0 != esk16_0,
inference(scs_inference,[],[i_0_49,i_0_115,i_0_129,i_0_88,i_0_80,i_0_81,i_0_118,i_0_119,i_0_101,i_0_103]) ).
cnf(i_0_131,plain,
~ between_c(X1,X2,X3,X2),
inference(rename_variables,[],[i_0_115]) ).
cnf(i_0_132,plain,
~ meet(X1,X2,X2),
inference(scs_inference,[],[i_0_49,i_0_115,i_0_129,i_0_88,i_0_80,i_0_81,i_0_118,i_0_119,i_0_101,i_0_103,i_0_54]) ).
cnf(i_0_133,plain,
( ~ incident_c(X1,X2)
| end_point(X1,X2)
| ~ meet(X3,X2,X4)
| ~ incident_c(X1,X4) ),
inference(rename_variables,[],[i_0_54]) ).
cnf(i_0_134,plain,
( X1 != esk15_0
| ~ between_c(X1,esk18_0,esk17_0,esk16_0) ),
inference(scs_inference,[],[i_0_46,i_0_49,i_0_115,i_0_129,i_0_88,i_0_80,i_0_81,i_0_118,i_0_119,i_0_101,i_0_103,i_0_54,i_0_100]) ).
cnf(i_0_135,plain,
( X1 != esk17_0
| ~ between_c(esk15_0,esk18_0,X1,esk16_0) ),
inference(scs_inference,[],[i_0_46,i_0_49,i_0_115,i_0_129,i_0_88,i_0_80,i_0_81,i_0_118,i_0_119,i_0_101,i_0_103,i_0_54,i_0_100,i_0_102]) ).
cnf(i_0_136,plain,
( incident_c(esk8_1(X1),X2)
| ~ part_of(X1,X2) ),
inference(scs_inference,[],[i_0_46,i_0_49,i_0_115,i_0_129,i_0_88,i_0_80,i_0_81,i_0_118,i_0_119,i_0_101,i_0_103,i_0_54,i_0_100,i_0_102,i_0_76]) ).
cnf(i_0_137,plain,
( ~ incident_c(X1,X2)
| incident_c(X1,X3)
| ~ part_of(X2,X3) ),
inference(rename_variables,[],[i_0_76]) ).
cnf(i_0_138,plain,
( incident_c(esk8_1(sum(X1,X2)),X1)
| incident_c(esk8_1(sum(X1,X2)),X2) ),
inference(scs_inference,[],[i_0_46,i_0_49,i_0_115,i_0_129,i_0_88,i_0_80,i_0_81,i_0_118,i_0_119,i_0_101,i_0_103,i_0_54,i_0_100,i_0_102,i_0_76,i_0_117]) ).
cnf(i_0_139,plain,
( ~ incident_c(X1,sum(X2,X3))
| incident_c(X1,X2)
| incident_c(X1,X3) ),
inference(rename_variables,[],[i_0_117]) ).
cnf(i_0_140,plain,
( X1 != esk8_1(sum(X2,X3))
| ~ end_point(X1,sum(X2,X3)) ),
inference(scs_inference,[],[i_0_46,i_0_49,i_0_115,i_0_129,i_0_88,i_0_80,i_0_81,i_0_118,i_0_119,i_0_101,i_0_103,i_0_54,i_0_100,i_0_102,i_0_76,i_0_117,i_0_106]) ).
cnf(i_0_141,plain,
( X1 != sum(X2,X3)
| ~ end_point(esk8_1(sum(X2,X3)),X1) ),
inference(scs_inference,[],[i_0_46,i_0_49,i_0_115,i_0_129,i_0_88,i_0_80,i_0_81,i_0_118,i_0_119,i_0_101,i_0_103,i_0_54,i_0_100,i_0_102,i_0_76,i_0_117,i_0_106,i_0_107]) ).
cnf(i_0_142,plain,
~ between_c(esk15_0,esk18_0,esk17_0,esk16_0),
inference(equality_inference,[],[134]) ).
cnf(i_0_143,plain,
~ between_c(esk15_0,esk18_0,esk17_0,esk16_0),
inference(equality_inference,[],[135]) ).
cnf(i_0_144,plain,
~ end_point(esk8_1(sum(X1,X2)),sum(X1,X2)),
inference(equality_inference,[],[140]) ).
cnf(i_0_145,plain,
~ end_point(esk8_1(sum(X1,X2)),sum(X1,X2)),
inference(equality_inference,[],[141]) ).
cnf(i_0_146,plain,
incident_c(esk8_1(X1),sum(sum(X1,X2),X3)),
inference(scs_inference,[],[i_0_124,i_0_118]) ).
cnf(i_0_147,plain,
( ~ incident_c(X1,X2)
| incident_c(X1,sum(X2,X3)) ),
inference(rename_variables,[],[i_0_118]) ).
cnf(i_0_148,plain,
incident_c(esk8_1(X1),sum(X2,sum(X1,X3))),
inference(scs_inference,[],[i_0_124,i_0_118,i_0_119]) ).
cnf(i_0_149,plain,
( ~ incident_c(X1,X2)
| incident_c(X1,sum(X3,X2)) ),
inference(rename_variables,[],[i_0_119]) ).
cnf(i_0_150,plain,
( X1 != X2
| ~ meet(X3,X1,X2) ),
inference(scs_inference,[],[i_0_132,i_0_124,i_0_118,i_0_119,i_0_109]) ).
cnf(i_0_151,plain,
( ~ meet(X1,X2,X3)
| ~ meet(X4,esk12_2(X2,X3),sum(X2,X3)) ),
inference(scs_inference,[],[i_0_132,i_0_124,i_0_118,i_0_119,i_0_109,i_0_61]) ).
cnf(i_0_152,plain,
~ meet(X1,X2,X2),
inference(rename_variables,[],[i_0_132]) ).
cnf(i_0_153,plain,
( ~ incident_c(X1,X2)
| incident_c(X1,X3)
| ~ part_of(X2,X3) ),
inference(rename_variables,[],[i_0_76]) ).
cnf(i_0_154,plain,
incident_c(esk8_1(X1),X1),
inference(rename_variables,[],[i_0_122]) ).
cnf(i_0_156,plain,
~ meet(X1,X2,X2),
inference(equality_inference,[],[150]) ).
cnf(i_0_157,plain,
incident_c(esk8_1(X1),sum(sum(X2,X1),X3)),
inference(scs_inference,[],[i_0_126,i_0_118]) ).
cnf(i_0_158,plain,
( ~ incident_c(X1,X2)
| incident_c(X1,sum(X2,X3)) ),
inference(rename_variables,[],[i_0_118]) ).
cnf(i_0_159,plain,
incident_c(esk8_1(X1),sum(X2,sum(X3,X1))),
inference(scs_inference,[],[i_0_126,i_0_118,i_0_119]) ).
cnf(i_0_160,plain,
( ~ incident_c(X1,X2)
| incident_c(X1,sum(X3,X2)) ),
inference(rename_variables,[],[i_0_119]) ).
cnf(i_0_161,plain,
( incident_c(esk8_1(X1),X2)
| ~ part_of(sum(X3,X1),X2) ),
inference(scs_inference,[],[i_0_126,i_0_118,i_0_119,i_0_76]) ).
cnf(i_0_162,plain,
( ~ incident_c(X1,X2)
| incident_c(X1,X3)
| ~ part_of(X2,X3) ),
inference(rename_variables,[],[i_0_76]) ).
cnf(i_0_164,plain,
( X1 != X2
| ~ meet(X3,X2,X1) ),
inference(scs_inference,[],[i_0_132,i_0_110]) ).
cnf(i_0_165,plain,
( X1 = sum(esk9_2(X1,X2),esk10_2(X1,X2))
| ~ inner_point(X2,X1) ),
inference(rename_variables,[],[i_0_64]) ).
cnf(i_0_166,plain,
incident_c(esk8_1(X1),X1),
inference(rename_variables,[],[i_0_122]) ).
cnf(i_0_167,plain,
~ meet(X1,X2,X2),
inference(rename_variables,[],[i_0_132]) ).
cnf(i_0_169,plain,
~ meet(X1,X2,X2),
inference(equality_inference,[],[164]) ).
cnf(i_0_170,plain,
( incident_c(esk8_1(X1),X2)
| ~ part_of(sum(sum(X1,X3),X4),X2) ),
inference(scs_inference,[],[i_0_146,i_0_76]) ).
cnf(i_0_171,plain,
( ~ incident_c(X1,X2)
| incident_c(X1,X3)
| ~ part_of(X2,X3) ),
inference(rename_variables,[],[i_0_76]) ).
cnf(i_0_172,plain,
( incident_c(esk8_1(X1),sum(X2,X3))
| ~ part_of(sum(sum(X1,X4),X5),X2) ),
inference(scs_inference,[],[i_0_146,i_0_76,i_0_118]) ).
cnf(i_0_173,plain,
( ~ incident_c(X1,X2)
| incident_c(X1,sum(X2,X3)) ),
inference(rename_variables,[],[i_0_118]) ).
cnf(i_0_174,plain,
( incident_c(esk8_1(X1),sum(X2,X3))
| ~ part_of(sum(sum(X1,X4),X5),X3) ),
inference(scs_inference,[],[i_0_146,i_0_76,i_0_118,i_0_119]) ).
cnf(i_0_175,plain,
( ~ incident_c(X1,X2)
| incident_c(X1,sum(X3,X2)) ),
inference(rename_variables,[],[i_0_119]) ).
cnf(i_0_176,plain,
incident_c(esk8_1(X1),X1),
inference(rename_variables,[],[i_0_122]) ).
cnf(i_0_177,plain,
( X1 != X2
| ~ part_of(sum(sum(X3,X4),X5),X6)
| ~ end_point(esk8_1(X2),X1) ),
inference(scs_inference,[],[i_0_46,i_0_122,i_0_146,i_0_120,i_0_76,i_0_118,i_0_119,i_0_107]) ).
cnf(i_0_178,plain,
( ~ end_point(esk8_1(X1),X1)
| ~ part_of(sum(sum(X2,X3),X4),X5) ),
inference(equality_inference,[],[177]) ).
cnf(i_0_179,plain,
( incident_c(esk8_1(X1),X2)
| ~ part_of(sum(X1,X3),X2) ),
inference(scs_inference,[],[i_0_124,i_0_76]) ).
cnf(i_0_180,plain,
( ~ incident_c(X1,X2)
| incident_c(X1,X3)
| ~ part_of(X2,X3) ),
inference(rename_variables,[],[i_0_76]) ).
cnf(i_0_181,plain,
( incident_c(esk8_1(X1),sum(X2,X3))
| ~ part_of(sum(X1,X4),X2) ),
inference(scs_inference,[],[i_0_124,i_0_76,i_0_118]) ).
cnf(i_0_182,plain,
( ~ incident_c(X1,X2)
| incident_c(X1,sum(X2,X3)) ),
inference(rename_variables,[],[i_0_118]) ).
cnf(i_0_183,plain,
( incident_c(esk8_1(X1),sum(X2,X3))
| ~ part_of(sum(X1,X4),X3) ),
inference(scs_inference,[],[i_0_124,i_0_76,i_0_118,i_0_119]) ).
cnf(i_0_184,plain,
( ~ incident_c(X1,X2)
| incident_c(X1,sum(X3,X2)) ),
inference(rename_variables,[],[i_0_119]) ).
cnf(i_0_185,plain,
incident_c(esk8_1(X1),X1),
inference(rename_variables,[],[i_0_122]) ).
cnf(i_0_186,plain,
( X1 != esk18_0
| ~ between_c(esk15_0,X1,esk17_0,esk16_0)
| ~ part_of(sum(X2,X3),X4) ),
inference(scs_inference,[],[i_0_46,i_0_122,i_0_124,i_0_132,i_0_76,i_0_118,i_0_119,i_0_101]) ).
cnf(i_0_187,plain,
( ~ part_of(sum(X1,X2),X3)
| ~ between_c(esk15_0,esk18_0,esk17_0,esk16_0) ),
inference(equality_inference,[],[186]) ).
cnf(i_0_188,plain,
( X1 != esk16_0
| ~ between_c(esk15_0,esk18_0,esk17_0,X1) ),
inference(scs_inference,[],[i_0_46,i_0_103]) ).
cnf(i_0_189,plain,
( incident_c(esk8_1(X1),X2)
| ~ part_of(sum(X3,sum(X1,X4)),X2) ),
inference(scs_inference,[],[i_0_46,i_0_148,i_0_103,i_0_76]) ).
cnf(i_0_190,plain,
( ~ incident_c(X1,X2)
| incident_c(X1,X3)
| ~ part_of(X2,X3) ),
inference(rename_variables,[],[i_0_76]) ).
cnf(i_0_191,plain,
( X1 != esk8_1(X2)
| ~ end_point(X1,X2) ),
inference(scs_inference,[],[i_0_46,i_0_148,i_0_120,i_0_103,i_0_76,i_0_106]) ).
cnf(i_0_192,plain,
( X1 != X2
| ~ end_point(esk8_1(X2),X1) ),
inference(scs_inference,[],[i_0_46,i_0_148,i_0_120,i_0_103,i_0_76,i_0_106,i_0_107]) ).
cnf(i_0_193,plain,
( X1 != esk18_0
| ~ between_c(esk15_0,X1,esk17_0,esk16_0) ),
inference(scs_inference,[],[i_0_46,i_0_148,i_0_120,i_0_103,i_0_76,i_0_106,i_0_107,i_0_101]) ).
cnf(i_0_194,plain,
~ between_c(esk15_0,esk18_0,esk17_0,esk16_0),
inference(equality_inference,[],[188]) ).
cnf(i_0_195,plain,
~ end_point(esk8_1(X1),X1),
inference(equality_inference,[],[191]) ).
cnf(i_0_196,plain,
~ end_point(esk8_1(X1),X1),
inference(equality_inference,[],[192]) ).
cnf(i_0_197,plain,
~ between_c(esk15_0,esk18_0,esk17_0,esk16_0),
inference(equality_inference,[],[193]) ).
cnf(i_0_198,plain,
( incident_c(esk8_1(X1),X2)
| ~ part_of(sum(sum(X3,X1),X4),X2) ),
inference(scs_inference,[],[i_0_157,i_0_76]) ).
cnf(i_0_199,plain,
( ~ incident_c(X1,X2)
| incident_c(X1,X3)
| ~ part_of(X2,X3) ),
inference(rename_variables,[],[i_0_76]) ).
cnf(i_0_200,plain,
( incident_c(esk8_1(X1),sum(X2,X3))
| ~ part_of(sum(sum(X4,X1),X5),X2) ),
inference(scs_inference,[],[i_0_157,i_0_76,i_0_118]) ).
cnf(i_0_201,plain,
( ~ incident_c(X1,X2)
| incident_c(X1,sum(X2,X3)) ),
inference(rename_variables,[],[i_0_118]) ).
cnf(i_0_202,plain,
( incident_c(esk8_1(X1),sum(X2,X3))
| ~ part_of(sum(sum(X4,X1),X5),X3) ),
inference(scs_inference,[],[i_0_157,i_0_76,i_0_118,i_0_119]) ).
cnf(i_0_203,plain,
( ~ incident_c(X1,X2)
| incident_c(X1,sum(X3,X2)) ),
inference(rename_variables,[],[i_0_119]) ).
cnf(i_0_204,plain,
incident_c(esk8_1(X1),X1),
inference(rename_variables,[],[i_0_122]) ).
cnf(i_0_206,plain,
( incident_c(esk8_1(X1),X2)
| ~ part_of(sum(X3,sum(X4,X1)),X2) ),
inference(scs_inference,[],[i_0_159,i_0_76]) ).
cnf(i_0_207,plain,
( ~ incident_c(X1,X2)
| incident_c(X1,X3)
| ~ part_of(X2,X3) ),
inference(rename_variables,[],[i_0_76]) ).
cnf(i_0_208,plain,
( incident_c(esk8_1(X1),sum(X2,X3))
| ~ part_of(sum(X4,sum(X5,X1)),X2) ),
inference(scs_inference,[],[i_0_159,i_0_76,i_0_118]) ).
cnf(i_0_209,plain,
( ~ incident_c(X1,X2)
| incident_c(X1,sum(X2,X3)) ),
inference(rename_variables,[],[i_0_118]) ).
cnf(i_0_210,plain,
( incident_c(esk8_1(X1),sum(X2,X3))
| ~ part_of(sum(X4,sum(X5,X1)),X3) ),
inference(scs_inference,[],[i_0_159,i_0_76,i_0_118,i_0_119]) ).
cnf(i_0_211,plain,
( ~ incident_c(X1,X2)
| incident_c(X1,sum(X3,X2)) ),
inference(rename_variables,[],[i_0_119]) ).
cnf(i_0_212,plain,
incident_c(esk8_1(X1),X1),
inference(rename_variables,[],[i_0_122]) ).
cnf(i_0_214,plain,
~ meet(X1,sum(X2,X3),X2),
inference(scs_inference,[],[i_0_124,i_0_122,i_0_120,i_0_55]) ).
cnf(i_0_215,plain,
incident_c(esk8_1(X1),X1),
inference(rename_variables,[],[i_0_122]) ).
cnf(i_0_216,plain,
~ end_point(esk8_1(X1),X1),
inference(rename_variables,[],[i_0_120]) ).
cnf(i_0_217,plain,
( ~ incident_c(X1,X2)
| end_point(X1,X2)
| ~ meet(X3,X4,X2)
| ~ incident_c(X1,X4) ),
inference(rename_variables,[],[i_0_55]) ).
cnf(i_0_218,plain,
~ meet(X1,X2,sum(X2,X3)),
inference(scs_inference,[],[i_0_124,i_0_122,i_0_215,i_0_120,i_0_216,i_0_55,i_0_54]) ).
cnf(i_0_219,plain,
incident_c(esk8_1(X1),X1),
inference(rename_variables,[],[i_0_122]) ).
cnf(i_0_220,plain,
~ end_point(esk8_1(X1),X1),
inference(rename_variables,[],[i_0_120]) ).
cnf(i_0_221,plain,
( ~ incident_c(X1,X2)
| end_point(X1,X2)
| ~ meet(X3,X2,X4)
| ~ incident_c(X1,X4) ),
inference(rename_variables,[],[i_0_54]) ).
cnf(i_0_222,plain,
( X1 != sum(X2,X3)
| ~ meet(X4,X1,X2) ),
inference(scs_inference,[],[i_0_124,i_0_122,i_0_215,i_0_120,i_0_216,i_0_55,i_0_54,i_0_109]) ).
cnf(i_0_223,plain,
( meet(X1,esk9_2(X2,X1),esk10_2(X2,X1))
| ~ inner_point(X1,X2) ),
inference(rename_variables,[],[i_0_59]) ).
cnf(i_0_224,plain,
incident_c(esk8_1(X1),sum(X1,X2)),
inference(rename_variables,[],[i_0_124]) ).
cnf(i_0_226,plain,
~ meet(X1,sum(X2,X3),X2),
inference(equality_inference,[],[222]) ).
cnf(i_0_227,plain,
~ meet(X1,sum(X2,X3),X3),
inference(scs_inference,[],[i_0_126,i_0_122,i_0_120,i_0_55]) ).
cnf(i_0_228,plain,
incident_c(esk8_1(X1),X1),
inference(rename_variables,[],[i_0_122]) ).
cnf(i_0_229,plain,
~ end_point(esk8_1(X1),X1),
inference(rename_variables,[],[i_0_120]) ).
cnf(i_0_230,plain,
( ~ incident_c(X1,X2)
| end_point(X1,X2)
| ~ meet(X3,X4,X2)
| ~ incident_c(X1,X4) ),
inference(rename_variables,[],[i_0_55]) ).
cnf(i_0_231,plain,
~ meet(X1,X2,sum(X3,X2)),
inference(scs_inference,[],[i_0_126,i_0_122,i_0_228,i_0_120,i_0_229,i_0_55,i_0_54]) ).
cnf(i_0_232,plain,
incident_c(esk8_1(X1),X1),
inference(rename_variables,[],[i_0_122]) ).
cnf(i_0_233,plain,
~ end_point(esk8_1(X1),X1),
inference(rename_variables,[],[i_0_120]) ).
cnf(i_0_234,plain,
( ~ incident_c(X1,X2)
| end_point(X1,X2)
| ~ meet(X3,X2,X4)
| ~ incident_c(X1,X4) ),
inference(rename_variables,[],[i_0_54]) ).
cnf(i_0_235,plain,
( X1 != X2
| ~ meet(X3,X1,sum(X2,X4)) ),
inference(scs_inference,[],[i_0_126,i_0_122,i_0_228,i_0_120,i_0_229,i_0_218,i_0_55,i_0_54,i_0_109]) ).
cnf(i_0_236,plain,
( X1 != X2
| ~ meet(X3,esk12_2(X1,X4),sum(esk12_2(X2,X4),X5)) ),
inference(scs_inference,[],[i_0_126,i_0_122,i_0_228,i_0_120,i_0_229,i_0_218,i_0_55,i_0_54,i_0_109,i_0_92]) ).
cnf(i_0_237,plain,
( X1 = sum(esk9_2(X1,X2),esk10_2(X1,X2))
| ~ inner_point(X2,X1) ),
inference(rename_variables,[],[i_0_64]) ).
cnf(i_0_239,plain,
~ meet(X1,X2,sum(X2,X3)),
inference(equality_inference,[],[235]) ).
cnf(i_0_240,plain,
~ meet(X1,esk12_2(X2,X3),sum(esk12_2(X2,X3),X4)),
inference(equality_inference,[],[236]) ).
cnf(i_0_241,plain,
( X1 != sum(X2,X3)
| ~ meet(X4,X1,X3) ),
inference(scs_inference,[],[i_0_227,i_0_109]) ).
cnf(i_0_242,plain,
( meet(X1,esk9_2(X2,X1),esk10_2(X2,X1))
| ~ inner_point(X1,X2) ),
inference(rename_variables,[],[i_0_59]) ).
cnf(i_0_244,plain,
~ meet(X1,sum(X2,X3),X3),
inference(equality_inference,[],[241]) ).
cnf(i_0_245,plain,
( X1 != X2
| ~ meet(X3,X1,sum(X4,X2)) ),
inference(scs_inference,[],[i_0_231,i_0_109]) ).
cnf(i_0_246,plain,
( X1 != X2
| ~ meet(X3,esk12_2(X4,X1),sum(X5,esk12_2(X4,X2))) ),
inference(scs_inference,[],[i_0_231,i_0_109,i_0_93]) ).
cnf(i_0_247,plain,
( X1 = sum(esk9_2(X1,X2),esk10_2(X1,X2))
| ~ inner_point(X2,X1) ),
inference(rename_variables,[],[i_0_64]) ).
cnf(i_0_249,plain,
~ meet(X1,X2,sum(X3,X2)),
inference(equality_inference,[],[245]) ).
cnf(i_0_250,plain,
~ meet(X1,esk12_2(X2,X3),sum(X4,esk12_2(X2,X3))),
inference(equality_inference,[],[246]) ).
cnf(i_0_251,plain,
( X1 != X2
| ~ meet(X3,sum(X2,X4),X1) ),
inference(scs_inference,[],[i_0_214,i_0_110]) ).
cnf(i_0_252,plain,
( X1 != X2
| ~ meet(X3,sum(esk11_2(X2,X4),X5),esk11_2(X1,X4)) ),
inference(scs_inference,[],[i_0_214,i_0_110,i_0_94]) ).
cnf(i_0_253,plain,
( X1 = sum(esk9_2(X1,X2),esk10_2(X1,X2))
| ~ inner_point(X2,X1) ),
inference(rename_variables,[],[i_0_64]) ).
cnf(i_0_255,plain,
~ meet(X1,sum(X2,X3),X2),
inference(equality_inference,[],[251]) ).
cnf(i_0_256,plain,
~ meet(X1,sum(esk11_2(X2,X3),X4),esk11_2(X2,X3)),
inference(equality_inference,[],[252]) ).
cnf(i_0_257,plain,
( X1 != sum(X2,X3)
| ~ meet(X4,X2,X1) ),
inference(scs_inference,[],[i_0_218,i_0_110]) ).
cnf(i_0_258,plain,
( meet(X1,esk9_2(X2,X1),esk10_2(X2,X1))
| ~ inner_point(X1,X2) ),
inference(rename_variables,[],[i_0_59]) ).
cnf(i_0_259,plain,
incident_c(esk8_1(X1),X1),
inference(rename_variables,[],[i_0_122]) ).
cnf(i_0_261,plain,
~ meet(X1,X2,sum(X2,X3)),
inference(equality_inference,[],[257]) ).
cnf(i_0_262,plain,
( X1 != X2
| ~ meet(X3,sum(X4,X2),X1) ),
inference(scs_inference,[],[i_0_227,i_0_110]) ).
cnf(i_0_263,plain,
( X1 != X2
| ~ meet(X3,sum(X4,esk11_2(X5,X2)),esk11_2(X5,X1)) ),
inference(scs_inference,[],[i_0_227,i_0_110,i_0_95]) ).
cnf(i_0_264,plain,
( X1 = sum(esk9_2(X1,X2),esk10_2(X1,X2))
| ~ inner_point(X2,X1) ),
inference(rename_variables,[],[i_0_64]) ).
cnf(i_0_265,plain,
incident_c(esk8_1(X1),X1),
inference(rename_variables,[],[i_0_122]) ).
cnf(i_0_267,plain,
~ meet(X1,sum(X2,X3),X3),
inference(equality_inference,[],[262]) ).
cnf(i_0_268,plain,
~ meet(X1,sum(X2,esk11_2(X3,X4)),esk11_2(X3,X4)),
inference(equality_inference,[],[263]) ).
cnf(i_0_269,plain,
( X1 != sum(X2,X3)
| ~ meet(X4,X3,X1) ),
inference(scs_inference,[],[i_0_231,i_0_110]) ).
cnf(i_0_270,plain,
( meet(X1,esk9_2(X2,X1),esk10_2(X2,X1))
| ~ inner_point(X1,X2) ),
inference(rename_variables,[],[i_0_59]) ).
cnf(i_0_271,plain,
incident_c(esk8_1(X1),X1),
inference(rename_variables,[],[i_0_122]) ).
cnf(i_0_273,plain,
~ meet(X1,X2,sum(X3,X2)),
inference(equality_inference,[],[269]) ).
cnf(i_0_274,plain,
~ meet(X1,sum(sum(X2,X3),X4),X2),
inference(scs_inference,[],[i_0_146,i_0_122,i_0_120,i_0_55]) ).
cnf(i_0_275,plain,
incident_c(esk8_1(X1),X1),
inference(rename_variables,[],[i_0_122]) ).
cnf(i_0_276,plain,
~ end_point(esk8_1(X1),X1),
inference(rename_variables,[],[i_0_120]) ).
cnf(i_0_277,plain,
( ~ incident_c(X1,X2)
| end_point(X1,X2)
| ~ meet(X3,X4,X2)
| ~ incident_c(X1,X4) ),
inference(rename_variables,[],[i_0_55]) ).
cnf(i_0_278,plain,
~ meet(X1,X2,sum(sum(X2,X3),X4)),
inference(scs_inference,[],[i_0_146,i_0_122,i_0_275,i_0_120,i_0_276,i_0_55,i_0_54]) ).
cnf(i_0_279,plain,
incident_c(esk8_1(X1),X1),
inference(rename_variables,[],[i_0_122]) ).
cnf(i_0_280,plain,
~ end_point(esk8_1(X1),X1),
inference(rename_variables,[],[i_0_120]) ).
cnf(i_0_281,plain,
( ~ incident_c(X1,X2)
| end_point(X1,X2)
| ~ meet(X3,X2,X4)
| ~ incident_c(X1,X4) ),
inference(rename_variables,[],[i_0_54]) ).
cnf(i_0_282,plain,
( X1 != sum(sum(X2,X3),X4)
| ~ meet(X5,X1,X2) ),
inference(scs_inference,[],[i_0_146,i_0_122,i_0_275,i_0_120,i_0_276,i_0_55,i_0_54,i_0_109]) ).
cnf(i_0_283,plain,
( meet(X1,esk9_2(X2,X1),esk10_2(X2,X1))
| ~ inner_point(X1,X2) ),
inference(rename_variables,[],[i_0_59]) ).
cnf(i_0_284,plain,
incident_c(esk8_1(X1),sum(sum(X1,X2),X3)),
inference(rename_variables,[],[i_0_146]) ).
cnf(i_0_286,plain,
~ meet(X1,sum(sum(X2,X3),X4),X2),
inference(equality_inference,[],[282]) ).
cnf(i_0_287,plain,
( X1 != X2
| ~ meet(X3,X1,sum(sum(X2,X4),X5)) ),
inference(scs_inference,[],[i_0_278,i_0_109]) ).
cnf(i_0_288,plain,
( X1 != X2
| ~ meet(X3,sum(sum(X2,X4),X5),X1) ),
inference(scs_inference,[],[i_0_274,i_0_278,i_0_109,i_0_110]) ).
cnf(i_0_289,plain,
( X1 = sum(X2,X3)
| incident_c(esk2_3(X1,X2,X3),X1)
| incident_c(esk2_3(X1,X2,X3),X2)
| incident_c(esk2_3(X1,X2,X3),X3) ),
inference(rename_variables,[],[i_0_47]) ).
cnf(i_0_291,plain,
~ meet(X1,X2,sum(sum(X2,X3),X4)),
inference(equality_inference,[],[287]) ).
cnf(i_0_292,plain,
~ meet(X1,sum(sum(X2,X3),X4),X2),
inference(equality_inference,[],[288]) ).
cnf(i_0_293,plain,
( X1 != sum(sum(X2,X3),X4)
| ~ meet(X5,X2,X1) ),
inference(scs_inference,[],[i_0_278,i_0_110]) ).
cnf(i_0_294,plain,
( meet(X1,esk9_2(X2,X1),esk10_2(X2,X1))
| ~ inner_point(X1,X2) ),
inference(rename_variables,[],[i_0_59]) ).
cnf(i_0_296,plain,
~ meet(X1,X2,sum(sum(X2,X3),X4)),
inference(equality_inference,[],[293]) ).
cnf(i_0_297,plain,
~ meet(X1,sum(X2,sum(X3,X4)),X3),
inference(scs_inference,[],[i_0_148,i_0_122,i_0_120,i_0_55]) ).
cnf(i_0_298,plain,
incident_c(esk8_1(X1),X1),
inference(rename_variables,[],[i_0_122]) ).
cnf(i_0_299,plain,
~ end_point(esk8_1(X1),X1),
inference(rename_variables,[],[i_0_120]) ).
cnf(i_0_300,plain,
( ~ incident_c(X1,X2)
| end_point(X1,X2)
| ~ meet(X3,X4,X2)
| ~ incident_c(X1,X4) ),
inference(rename_variables,[],[i_0_55]) ).
cnf(i_0_301,plain,
~ meet(X1,X2,sum(X3,sum(X2,X4))),
inference(scs_inference,[],[i_0_148,i_0_122,i_0_298,i_0_120,i_0_299,i_0_55,i_0_54]) ).
cnf(i_0_302,plain,
incident_c(esk8_1(X1),X1),
inference(rename_variables,[],[i_0_122]) ).
cnf(i_0_303,plain,
~ end_point(esk8_1(X1),X1),
inference(rename_variables,[],[i_0_120]) ).
cnf(i_0_304,plain,
( ~ incident_c(X1,X2)
| end_point(X1,X2)
| ~ meet(X3,X2,X4)
| ~ incident_c(X1,X4) ),
inference(rename_variables,[],[i_0_54]) ).
cnf(i_0_305,plain,
( X1 != sum(X2,sum(X3,X4))
| ~ meet(X5,X1,X3) ),
inference(scs_inference,[],[i_0_148,i_0_122,i_0_298,i_0_120,i_0_299,i_0_55,i_0_54,i_0_109]) ).
cnf(i_0_306,plain,
( meet(X1,esk9_2(X2,X1),esk10_2(X2,X1))
| ~ inner_point(X1,X2) ),
inference(rename_variables,[],[i_0_59]) ).
cnf(i_0_307,plain,
incident_c(esk8_1(X1),sum(X2,sum(X1,X3))),
inference(rename_variables,[],[i_0_148]) ).
cnf(i_0_309,plain,
~ meet(X1,sum(X2,sum(X3,X4)),X3),
inference(equality_inference,[],[305]) ).
cnf(i_0_310,plain,
( X1 != X2
| ~ meet(X3,X1,sum(X4,sum(X2,X5))) ),
inference(scs_inference,[],[i_0_301,i_0_109]) ).
cnf(i_0_311,plain,
( X1 != X2
| ~ meet(X3,sum(X4,sum(X2,X5)),X1) ),
inference(scs_inference,[],[i_0_297,i_0_301,i_0_109,i_0_110]) ).
cnf(i_0_312,plain,
( X1 = sum(X2,X3)
| incident_c(esk2_3(X1,X2,X3),X1)
| incident_c(esk2_3(X1,X2,X3),X2)
| incident_c(esk2_3(X1,X2,X3),X3) ),
inference(rename_variables,[],[i_0_47]) ).
cnf(i_0_314,plain,
~ meet(X1,X2,sum(X3,sum(X2,X4))),
inference(equality_inference,[],[310]) ).
cnf(i_0_315,plain,
~ meet(X1,sum(X2,sum(X3,X4)),X3),
inference(equality_inference,[],[311]) ).
cnf(i_0_316,plain,
( X1 != sum(X2,sum(X3,X4))
| ~ meet(X5,X3,X1) ),
inference(scs_inference,[],[i_0_301,i_0_110]) ).
cnf(i_0_317,plain,
( meet(X1,esk9_2(X2,X1),esk10_2(X2,X1))
| ~ inner_point(X1,X2) ),
inference(rename_variables,[],[i_0_59]) ).
cnf(i_0_319,plain,
~ meet(X1,X2,sum(X3,sum(X2,X4))),
inference(equality_inference,[],[316]) ).
cnf(i_0_320,plain,
~ meet(X1,sum(sum(X2,X3),X4),X3),
inference(scs_inference,[],[i_0_157,i_0_122,i_0_120,i_0_55]) ).
cnf(i_0_321,plain,
incident_c(esk8_1(X1),X1),
inference(rename_variables,[],[i_0_122]) ).
cnf(i_0_322,plain,
~ end_point(esk8_1(X1),X1),
inference(rename_variables,[],[i_0_120]) ).
cnf(i_0_323,plain,
( ~ incident_c(X1,X2)
| end_point(X1,X2)
| ~ meet(X3,X4,X2)
| ~ incident_c(X1,X4) ),
inference(rename_variables,[],[i_0_55]) ).
cnf(i_0_324,plain,
~ meet(X1,X2,sum(sum(X3,X2),X4)),
inference(scs_inference,[],[i_0_157,i_0_122,i_0_321,i_0_120,i_0_322,i_0_55,i_0_54]) ).
cnf(i_0_325,plain,
incident_c(esk8_1(X1),X1),
inference(rename_variables,[],[i_0_122]) ).
cnf(i_0_326,plain,
~ end_point(esk8_1(X1),X1),
inference(rename_variables,[],[i_0_120]) ).
cnf(i_0_327,plain,
( ~ incident_c(X1,X2)
| end_point(X1,X2)
| ~ meet(X3,X2,X4)
| ~ incident_c(X1,X4) ),
inference(rename_variables,[],[i_0_54]) ).
cnf(i_0_328,plain,
( X1 != sum(sum(X2,X3),X4)
| ~ meet(X5,X1,X3) ),
inference(scs_inference,[],[i_0_157,i_0_122,i_0_321,i_0_120,i_0_322,i_0_55,i_0_54,i_0_109]) ).
cnf(i_0_329,plain,
( meet(X1,esk9_2(X2,X1),esk10_2(X2,X1))
| ~ inner_point(X1,X2) ),
inference(rename_variables,[],[i_0_59]) ).
cnf(i_0_330,plain,
incident_c(esk8_1(X1),sum(sum(X2,X1),X3)),
inference(rename_variables,[],[i_0_157]) ).
cnf(i_0_332,plain,
~ meet(X1,sum(sum(X2,X3),X4),X3),
inference(equality_inference,[],[328]) ).
cnf(i_0_333,plain,
( X1 != X2
| ~ meet(X3,X1,sum(sum(X4,X2),X5)) ),
inference(scs_inference,[],[i_0_324,i_0_109]) ).
cnf(i_0_334,plain,
( X1 != X2
| ~ meet(X3,sum(sum(X4,X2),X5),X1) ),
inference(scs_inference,[],[i_0_320,i_0_324,i_0_109,i_0_110]) ).
cnf(i_0_335,plain,
( X1 = sum(X2,X3)
| incident_c(esk2_3(X1,X2,X3),X1)
| incident_c(esk2_3(X1,X2,X3),X2)
| incident_c(esk2_3(X1,X2,X3),X3) ),
inference(rename_variables,[],[i_0_47]) ).
cnf(i_0_337,plain,
~ meet(X1,X2,sum(sum(X3,X2),X4)),
inference(equality_inference,[],[333]) ).
cnf(i_0_338,plain,
~ meet(X1,sum(sum(X2,X3),X4),X3),
inference(equality_inference,[],[334]) ).
cnf(i_0_339,plain,
( X1 != sum(sum(X2,X3),X4)
| ~ meet(X5,X3,X1) ),
inference(scs_inference,[],[i_0_324,i_0_110]) ).
cnf(i_0_340,plain,
( meet(X1,esk9_2(X2,X1),esk10_2(X2,X1))
| ~ inner_point(X1,X2) ),
inference(rename_variables,[],[i_0_59]) ).
cnf(i_0_342,plain,
~ meet(X1,X2,sum(sum(X3,X2),X4)),
inference(equality_inference,[],[339]) ).
cnf(i_0_343,plain,
~ meet(X1,sum(X2,sum(X3,X4)),X4),
inference(scs_inference,[],[i_0_159,i_0_122,i_0_120,i_0_55]) ).
cnf(i_0_344,plain,
incident_c(esk8_1(X1),X1),
inference(rename_variables,[],[i_0_122]) ).
cnf(i_0_345,plain,
~ end_point(esk8_1(X1),X1),
inference(rename_variables,[],[i_0_120]) ).
cnf(i_0_346,plain,
( ~ incident_c(X1,X2)
| end_point(X1,X2)
| ~ meet(X3,X4,X2)
| ~ incident_c(X1,X4) ),
inference(rename_variables,[],[i_0_55]) ).
cnf(i_0_347,plain,
~ meet(X1,X2,sum(X3,sum(X4,X2))),
inference(scs_inference,[],[i_0_159,i_0_122,i_0_344,i_0_120,i_0_345,i_0_55,i_0_54]) ).
cnf(i_0_348,plain,
incident_c(esk8_1(X1),X1),
inference(rename_variables,[],[i_0_122]) ).
cnf(i_0_349,plain,
~ end_point(esk8_1(X1),X1),
inference(rename_variables,[],[i_0_120]) ).
cnf(i_0_350,plain,
( ~ incident_c(X1,X2)
| end_point(X1,X2)
| ~ meet(X3,X2,X4)
| ~ incident_c(X1,X4) ),
inference(rename_variables,[],[i_0_54]) ).
cnf(i_0_351,plain,
( X1 != sum(X2,sum(X3,X4))
| ~ meet(X5,X1,X4) ),
inference(scs_inference,[],[i_0_159,i_0_122,i_0_344,i_0_120,i_0_345,i_0_55,i_0_54,i_0_109]) ).
cnf(i_0_352,plain,
( meet(X1,esk9_2(X2,X1),esk10_2(X2,X1))
| ~ inner_point(X1,X2) ),
inference(rename_variables,[],[i_0_59]) ).
cnf(i_0_353,plain,
incident_c(esk8_1(X1),sum(X2,sum(X3,X1))),
inference(rename_variables,[],[i_0_159]) ).
cnf(i_0_355,plain,
~ meet(X1,sum(X2,sum(X3,X4)),X4),
inference(equality_inference,[],[351]) ).
cnf(i_0_356,plain,
( X1 != X2
| ~ meet(X3,X1,sum(X4,sum(X5,X2))) ),
inference(scs_inference,[],[i_0_347,i_0_109]) ).
cnf(i_0_357,plain,
( X1 != X2
| ~ meet(X3,sum(X4,sum(X5,X2)),X1) ),
inference(scs_inference,[],[i_0_343,i_0_347,i_0_109,i_0_110]) ).
cnf(i_0_358,plain,
( X1 = sum(X2,X3)
| incident_c(esk2_3(X1,X2,X3),X1)
| incident_c(esk2_3(X1,X2,X3),X2)
| incident_c(esk2_3(X1,X2,X3),X3) ),
inference(rename_variables,[],[i_0_47]) ).
cnf(i_0_360,plain,
~ meet(X1,X2,sum(X3,sum(X4,X2))),
inference(equality_inference,[],[356]) ).
cnf(i_0_361,plain,
~ meet(X1,sum(X2,sum(X3,X4)),X4),
inference(equality_inference,[],[357]) ).
cnf(i_0_362,plain,
( X1 != sum(X2,sum(X3,X4))
| ~ meet(X5,X4,X1) ),
inference(scs_inference,[],[i_0_347,i_0_110]) ).
cnf(i_0_363,plain,
( meet(X1,esk9_2(X2,X1),esk10_2(X2,X1))
| ~ inner_point(X1,X2) ),
inference(rename_variables,[],[i_0_59]) ).
cnf(i_0_365,plain,
~ meet(X1,X2,sum(X3,sum(X4,X2))),
inference(equality_inference,[],[362]) ).
cnf(i_0_366,plain,
part_of(esk14_4(esk15_0,esk16_0,esk17_0,esk18_0),esk15_0),
inference(scs_inference,[],[i_0_49,i_0_38]) ).
cnf(i_0_367,plain,
( ~ between_c(X1,X2,X3,X4)
| part_of(esk14_4(X1,X2,X3,X4),X1) ),
inference(rename_variables,[],[i_0_38]) ).
cnf(i_0_368,plain,
inner_point(esk17_0,esk14_4(esk15_0,esk16_0,esk17_0,esk18_0)),
inference(scs_inference,[],[i_0_49,i_0_38,i_0_39]) ).
cnf(i_0_369,plain,
( ~ between_c(X1,X2,X3,X4)
| inner_point(X3,esk14_4(X1,X2,X3,X4)) ),
inference(rename_variables,[],[i_0_39]) ).
cnf(i_0_370,plain,
end_point(esk16_0,esk14_4(esk15_0,esk16_0,esk17_0,esk18_0)),
inference(scs_inference,[],[i_0_49,i_0_38,i_0_39,i_0_40]) ).
cnf(i_0_371,plain,
( ~ between_c(X1,X2,X3,X4)
| end_point(X2,esk14_4(X1,X2,X3,X4)) ),
inference(rename_variables,[],[i_0_40]) ).
cnf(i_0_372,plain,
end_point(esk18_0,esk14_4(esk15_0,esk16_0,esk17_0,esk18_0)),
inference(scs_inference,[],[i_0_49,i_0_38,i_0_39,i_0_40,i_0_41]) ).
cnf(i_0_373,plain,
( ~ between_c(X1,X2,X3,X4)
| end_point(X4,esk14_4(X1,X2,X3,X4)) ),
inference(rename_variables,[],[i_0_41]) ).
cnf(i_0_374,plain,
~ inner_point(esk16_0,esk14_4(esk15_0,esk16_0,esk17_0,esk18_0)),
inference(scs_inference,[],[i_0_49,i_0_38,i_0_39,i_0_40,i_0_41,i_0_80]) ).
cnf(i_0_375,plain,
( ~ end_point(X1,X2)
| ~ inner_point(X1,X2) ),
inference(rename_variables,[],[i_0_80]) ).
cnf(i_0_376,plain,
meet(esk8_1(X1),esk9_2(X1,esk8_1(X1)),esk10_2(X1,esk8_1(X1))),
inference(scs_inference,[],[i_0_49,i_0_88,i_0_38,i_0_39,i_0_40,i_0_41,i_0_80,i_0_59]) ).
cnf(i_0_377,plain,
( ~ inner_point(X1,X2)
| meet(X1,esk9_2(X2,X1),esk10_2(X2,X1)) ),
inference(rename_variables,[],[i_0_59]) ).
cnf(i_0_378,plain,
part_of(esk4_2(esk8_1(X1),X1),X1),
inference(scs_inference,[],[i_0_49,i_0_122,i_0_88,i_0_120,i_0_38,i_0_39,i_0_40,i_0_41,i_0_80,i_0_59,i_0_67]) ).
cnf(i_0_379,plain,
~ end_point(esk8_1(X1),X1),
inference(rename_variables,[],[i_0_120]) ).
cnf(i_0_380,plain,
( end_point(X1,X2)
| ~ incident_c(X1,X2)
| part_of(esk4_2(X1,X2),X2) ),
inference(rename_variables,[],[i_0_67]) ).
cnf(i_0_381,plain,
part_of(esk3_2(esk8_1(X1),X1),X1),
inference(scs_inference,[],[i_0_49,i_0_122,i_0_88,i_0_120,i_0_379,i_0_38,i_0_39,i_0_40,i_0_41,i_0_80,i_0_59,i_0_67,i_0_68]) ).
cnf(i_0_382,plain,
~ end_point(esk8_1(X1),X1),
inference(rename_variables,[],[i_0_120]) ).
cnf(i_0_383,plain,
( end_point(X1,X2)
| ~ incident_c(X1,X2)
| part_of(esk3_2(X1,X2),X2) ),
inference(rename_variables,[],[i_0_68]) ).
cnf(i_0_384,plain,
incident_c(esk8_1(X1),esk4_2(esk8_1(X1),X1)),
inference(scs_inference,[],[i_0_49,i_0_122,i_0_88,i_0_120,i_0_379,i_0_382,i_0_38,i_0_39,i_0_40,i_0_41,i_0_80,i_0_59,i_0_67,i_0_68,i_0_69]) ).
cnf(i_0_385,plain,
~ end_point(esk8_1(X1),X1),
inference(rename_variables,[],[i_0_120]) ).
cnf(i_0_386,plain,
( end_point(X1,X2)
| ~ incident_c(X1,X2)
| incident_c(X1,esk4_2(X1,X2)) ),
inference(rename_variables,[],[i_0_69]) ).
cnf(i_0_387,plain,
incident_c(esk8_1(X1),esk3_2(esk8_1(X1),X1)),
inference(scs_inference,[],[i_0_49,i_0_122,i_0_88,i_0_120,i_0_379,i_0_382,i_0_385,i_0_38,i_0_39,i_0_40,i_0_41,i_0_80,i_0_59,i_0_67,i_0_68,i_0_69,i_0_70]) ).
cnf(i_0_388,plain,
~ end_point(esk8_1(X1),X1),
inference(rename_variables,[],[i_0_120]) ).
cnf(i_0_389,plain,
( end_point(X1,X2)
| ~ incident_c(X1,X2)
| incident_c(X1,esk3_2(X1,X2)) ),
inference(rename_variables,[],[i_0_70]) ).
cnf(i_0_390,plain,
~ part_of(esk4_2(esk8_1(X1),X1),esk3_2(esk8_1(X1),X1)),
inference(scs_inference,[],[i_0_49,i_0_122,i_0_88,i_0_120,i_0_379,i_0_382,i_0_385,i_0_388,i_0_38,i_0_39,i_0_40,i_0_41,i_0_80,i_0_59,i_0_67,i_0_68,i_0_69,i_0_70,i_0_57]) ).
cnf(i_0_391,plain,
incident_c(esk8_1(X1),X1),
inference(rename_variables,[],[i_0_122]) ).
cnf(i_0_392,plain,
( ~ incident_c(X1,X2)
| end_point(X1,X2)
| ~ part_of(esk4_2(X1,X2),esk3_2(X1,X2)) ),
inference(rename_variables,[],[i_0_57]) ).
cnf(i_0_393,plain,
~ part_of(esk3_2(esk8_1(X1),X1),esk4_2(esk8_1(X1),X1)),
inference(scs_inference,[],[i_0_49,i_0_122,i_0_391,i_0_88,i_0_120,i_0_379,i_0_382,i_0_385,i_0_388,i_0_38,i_0_39,i_0_40,i_0_41,i_0_80,i_0_59,i_0_67,i_0_68,i_0_69,i_0_70,i_0_57,i_0_58]) ).
cnf(i_0_394,plain,
incident_c(esk8_1(X1),X1),
inference(rename_variables,[],[i_0_122]) ).
cnf(i_0_395,plain,
( ~ incident_c(X1,X2)
| end_point(X1,X2)
| ~ part_of(esk3_2(X1,X2),esk4_2(X1,X2)) ),
inference(rename_variables,[],[i_0_58]) ).
cnf(i_0_396,plain,
between_c(esk15_0,esk18_0,esk8_1(esk14_4(esk15_0,esk16_0,esk17_0,esk18_0)),esk16_0),
inference(scs_inference,[],[i_0_49,i_0_130,i_0_122,i_0_391,i_0_88,i_0_120,i_0_379,i_0_382,i_0_385,i_0_388,i_0_38,i_0_39,i_0_40,i_0_41,i_0_80,i_0_59,i_0_67,i_0_68,i_0_69,i_0_70,i_0_57,i_0_58,i_0_48]) ).
cnf(i_0_397,plain,
inner_point(esk8_1(X1),X1),
inference(rename_variables,[],[i_0_88]) ).
cnf(i_0_398,plain,
( ~ end_point(X1,X2)
| ~ inner_point(X3,X2)
| X4 = X1
| between_c(X5,X4,X3,X1)
| ~ part_of(X2,X5)
| ~ end_point(X4,X2) ),
inference(rename_variables,[],[i_0_48]) ).
cnf(i_0_399,plain,
~ closed(esk14_4(esk15_0,esk16_0,esk17_0,esk18_0)),
inference(scs_inference,[],[i_0_49,i_0_130,i_0_122,i_0_391,i_0_88,i_0_120,i_0_379,i_0_382,i_0_385,i_0_388,i_0_38,i_0_39,i_0_40,i_0_41,i_0_80,i_0_59,i_0_67,i_0_68,i_0_69,i_0_70,i_0_57,i_0_58,i_0_48,i_0_83]) ).
cnf(i_0_400,plain,
( ~ end_point(X1,X2)
| ~ closed(X2) ),
inference(rename_variables,[],[i_0_83]) ).
cnf(i_0_401,plain,
open(esk14_4(esk15_0,esk16_0,esk17_0,esk18_0)),
inference(scs_inference,[],[i_0_49,i_0_130,i_0_122,i_0_391,i_0_88,i_0_120,i_0_379,i_0_382,i_0_385,i_0_388,i_0_38,i_0_39,i_0_40,i_0_41,i_0_80,i_0_59,i_0_67,i_0_68,i_0_69,i_0_70,i_0_57,i_0_58,i_0_48,i_0_83,i_0_86]) ).
cnf(i_0_402,plain,
( ~ end_point(X1,X2)
| open(X2) ),
inference(rename_variables,[],[i_0_86]) ).
cnf(i_0_403,plain,
end_point(esk7_1(esk14_4(esk15_0,esk16_0,esk17_0,esk18_0)),esk14_4(esk15_0,esk16_0,esk17_0,esk18_0)),
inference(scs_inference,[],[i_0_49,i_0_130,i_0_122,i_0_391,i_0_88,i_0_120,i_0_379,i_0_382,i_0_385,i_0_388,i_0_38,i_0_39,i_0_40,i_0_41,i_0_80,i_0_59,i_0_67,i_0_68,i_0_69,i_0_70,i_0_57,i_0_58,i_0_48,i_0_83,i_0_86,i_0_85]) ).
cnf(i_0_404,plain,
( ~ open(X1)
| end_point(esk7_1(X1),X1) ),
inference(rename_variables,[],[i_0_85]) ).
cnf(i_0_405,plain,
end_point(esk6_1(esk14_4(esk15_0,esk16_0,esk17_0,esk18_0)),esk14_4(esk15_0,esk16_0,esk17_0,esk18_0)),
inference(scs_inference,[],[i_0_49,i_0_130,i_0_122,i_0_391,i_0_88,i_0_120,i_0_379,i_0_382,i_0_385,i_0_388,i_0_38,i_0_39,i_0_40,i_0_41,i_0_80,i_0_59,i_0_67,i_0_68,i_0_69,i_0_70,i_0_57,i_0_58,i_0_48,i_0_83,i_0_86,i_0_85,i_0_87]) ).
cnf(i_0_406,plain,
( closed(X1)
| end_point(esk6_1(X1),X1) ),
inference(rename_variables,[],[i_0_87]) ).
cnf(i_0_407,plain,
end_point(esk11_2(esk14_4(esk15_0,esk16_0,esk17_0,esk18_0),esk16_0),esk14_4(esk15_0,esk16_0,esk17_0,esk18_0)),
inference(scs_inference,[],[i_0_49,i_0_130,i_0_122,i_0_391,i_0_88,i_0_120,i_0_379,i_0_382,i_0_385,i_0_388,i_0_38,i_0_39,i_0_40,i_0_41,i_0_80,i_0_59,i_0_67,i_0_68,i_0_69,i_0_70,i_0_57,i_0_58,i_0_48,i_0_83,i_0_86,i_0_85,i_0_87,i_0_73]) ).
cnf(i_0_408,plain,
( ~ end_point(X1,X2)
| end_point(esk11_2(X2,X1),X2) ),
inference(rename_variables,[],[i_0_73]) ).
cnf(i_0_409,plain,
esk16_0 != esk11_2(esk14_4(esk15_0,esk16_0,esk17_0,esk18_0),esk16_0),
inference(scs_inference,[],[i_0_49,i_0_130,i_0_122,i_0_391,i_0_88,i_0_120,i_0_379,i_0_382,i_0_385,i_0_388,i_0_38,i_0_39,i_0_40,i_0_41,i_0_80,i_0_59,i_0_67,i_0_68,i_0_69,i_0_70,i_0_57,i_0_58,i_0_48,i_0_83,i_0_86,i_0_85,i_0_87,i_0_73,i_0_79]) ).
cnf(i_0_410,plain,
( ~ end_point(X1,X2)
| X1 != esk11_2(X2,X1) ),
inference(rename_variables,[],[i_0_79]) ).
cnf(i_0_411,plain,
( part_of(X1,esk15_0)
| esk14_4(esk15_0,esk16_0,esk17_0,esk18_0) != X1 ),
inference(scs_inference,[],[i_0_49,i_0_130,i_0_122,i_0_391,i_0_88,i_0_120,i_0_379,i_0_382,i_0_385,i_0_388,i_0_38,i_0_39,i_0_40,i_0_41,i_0_80,i_0_59,i_0_67,i_0_68,i_0_69,i_0_70,i_0_57,i_0_58,i_0_48,i_0_83,i_0_86,i_0_85,i_0_87,i_0_73,i_0_79,i_0_98]) ).
cnf(i_0_412,plain,
X1 != esk3_2(esk8_1(X1),X1),
inference(scs_inference,[],[i_0_49,i_0_130,i_0_122,i_0_391,i_0_88,i_0_120,i_0_379,i_0_382,i_0_385,i_0_388,i_0_38,i_0_39,i_0_40,i_0_41,i_0_80,i_0_59,i_0_67,i_0_68,i_0_69,i_0_70,i_0_57,i_0_58,i_0_48,i_0_83,i_0_86,i_0_85,i_0_87,i_0_73,i_0_79,i_0_98,i_0_99]) ).
cnf(i_0_413,plain,
esk8_1(esk14_4(esk15_0,esk16_0,esk17_0,esk18_0)) != esk16_0,
inference(scs_inference,[],[i_0_49,i_0_130,i_0_122,i_0_391,i_0_88,i_0_397,i_0_120,i_0_379,i_0_382,i_0_385,i_0_388,i_0_38,i_0_39,i_0_40,i_0_41,i_0_80,i_0_59,i_0_67,i_0_68,i_0_69,i_0_70,i_0_57,i_0_58,i_0_48,i_0_83,i_0_86,i_0_85,i_0_87,i_0_73,i_0_79,i_0_98,i_0_99,i_0_104]) ).
cnf(i_0_414,plain,
inner_point(esk8_1(X1),X1),
inference(rename_variables,[],[i_0_88]) ).
cnf(i_0_415,plain,
incident_c(esk8_1(esk14_4(esk15_0,esk16_0,esk17_0,esk18_0)),esk15_0),
inference(scs_inference,[],[i_0_49,i_0_130,i_0_122,i_0_391,i_0_394,i_0_88,i_0_397,i_0_120,i_0_379,i_0_382,i_0_385,i_0_388,i_0_38,i_0_39,i_0_40,i_0_41,i_0_80,i_0_59,i_0_67,i_0_68,i_0_69,i_0_70,i_0_57,i_0_58,i_0_48,i_0_83,i_0_86,i_0_85,i_0_87,i_0_73,i_0_79,i_0_98,i_0_99,i_0_104,i_0_76]) ).
cnf(i_0_416,plain,
incident_c(esk8_1(X1),X1),
inference(rename_variables,[],[i_0_122]) ).
cnf(i_0_417,plain,
( ~ part_of(X1,X2)
| incident_c(X3,X2)
| ~ incident_c(X3,X1) ),
inference(rename_variables,[],[i_0_76]) ).
cnf(i_0_418,plain,
esk8_1(esk14_4(esk15_0,esk16_0,esk17_0,esk18_0)) != esk17_0,
inference(scs_inference,[],[i_0_46,i_0_49,i_0_130,i_0_122,i_0_391,i_0_394,i_0_88,i_0_397,i_0_120,i_0_379,i_0_382,i_0_385,i_0_388,i_0_38,i_0_39,i_0_40,i_0_41,i_0_80,i_0_59,i_0_67,i_0_68,i_0_69,i_0_70,i_0_57,i_0_58,i_0_48,i_0_83,i_0_86,i_0_85,i_0_87,i_0_73,i_0_79,i_0_98,i_0_99,i_0_104,i_0_76,i_0_102]) ).
cnf(i_0_419,plain,
esk16_0 != esk8_1(esk14_4(esk15_0,esk16_0,esk17_0,esk18_0)),
inference(scs_inference,[],[i_0_46,i_0_49,i_0_130,i_0_122,i_0_391,i_0_394,i_0_88,i_0_397,i_0_120,i_0_379,i_0_382,i_0_385,i_0_388,i_0_38,i_0_39,i_0_40,i_0_41,i_0_80,i_0_59,i_0_67,i_0_68,i_0_69,i_0_70,i_0_57,i_0_58,i_0_48,i_0_83,i_0_86,i_0_85,i_0_87,i_0_73,i_0_79,i_0_98,i_0_99,i_0_104,i_0_76,i_0_102,i_0_106]) ).
cnf(i_0_420,plain,
~ end_point(esk8_1(X1),X1),
inference(rename_variables,[],[i_0_120]) ).
cnf(i_0_421,plain,
incident_c(esk5_3(esk8_1(X1),sum(X2,X1),sum(X2,X1)),sum(X2,X1)),
inference(scs_inference,[],[i_0_46,i_0_49,i_0_130,i_0_126,i_0_122,i_0_391,i_0_394,i_0_88,i_0_397,i_0_120,i_0_379,i_0_382,i_0_385,i_0_388,i_0_132,i_0_38,i_0_39,i_0_40,i_0_41,i_0_80,i_0_59,i_0_67,i_0_68,i_0_69,i_0_70,i_0_57,i_0_58,i_0_48,i_0_83,i_0_86,i_0_85,i_0_87,i_0_73,i_0_79,i_0_98,i_0_99,i_0_104,i_0_76,i_0_102,i_0_106,i_0_51]) ).
cnf(i_0_422,plain,
~ meet(X1,X2,X2),
inference(rename_variables,[],[i_0_132]) ).
cnf(i_0_423,plain,
( ~ incident_c(X1,X2)
| ~ incident_c(X1,X3)
| meet(X1,X2,X3)
| incident_c(esk5_3(X1,X2,X3),X2) ),
inference(rename_variables,[],[i_0_51]) ).
cnf(i_0_424,plain,
incident_c(esk5_3(esk8_1(X1),sum(X1,X2),sum(X1,X2)),sum(X1,X2)),
inference(scs_inference,[],[i_0_46,i_0_49,i_0_130,i_0_126,i_0_124,i_0_122,i_0_391,i_0_394,i_0_88,i_0_397,i_0_120,i_0_379,i_0_382,i_0_385,i_0_388,i_0_132,i_0_422,i_0_38,i_0_39,i_0_40,i_0_41,i_0_80,i_0_59,i_0_67,i_0_68,i_0_69,i_0_70,i_0_57,i_0_58,i_0_48,i_0_83,i_0_86,i_0_85,i_0_87,i_0_73,i_0_79,i_0_98,i_0_99,i_0_104,i_0_76,i_0_102,i_0_106,i_0_51,i_0_52]) ).
cnf(i_0_425,plain,
~ meet(X1,X2,X2),
inference(rename_variables,[],[i_0_132]) ).
cnf(i_0_426,plain,
( ~ incident_c(X1,X2)
| ~ incident_c(X1,X3)
| meet(X1,X2,X3)
| incident_c(esk5_3(X1,X2,X3),X3) ),
inference(rename_variables,[],[i_0_52]) ).
cnf(i_0_427,plain,
~ end_point(esk5_3(esk8_1(X1),sum(X2,X1),sum(X2,X1)),sum(X2,X1)),
inference(scs_inference,[],[i_0_46,i_0_49,i_0_130,i_0_126,i_0_124,i_0_122,i_0_391,i_0_394,i_0_88,i_0_397,i_0_120,i_0_379,i_0_382,i_0_385,i_0_388,i_0_132,i_0_422,i_0_425,i_0_38,i_0_39,i_0_40,i_0_41,i_0_80,i_0_59,i_0_67,i_0_68,i_0_69,i_0_70,i_0_57,i_0_58,i_0_48,i_0_83,i_0_86,i_0_85,i_0_87,i_0_73,i_0_79,i_0_98,i_0_99,i_0_104,i_0_76,i_0_102,i_0_106,i_0_51,i_0_52,i_0_42]) ).
cnf(i_0_428,plain,
~ meet(X1,X2,X2),
inference(rename_variables,[],[i_0_132]) ).
cnf(i_0_429,plain,
( ~ incident_c(X1,X2)
| ~ incident_c(X1,X3)
| meet(X1,X2,X3)
| ~ end_point(esk5_3(X1,X2,X3),X3)
| ~ end_point(esk5_3(X1,X2,X3),X2) ),
inference(rename_variables,[],[i_0_42]) ).
cnf(i_0_430,plain,
esk18_0 = esk11_2(esk14_4(esk15_0,esk16_0,esk17_0,esk18_0),esk16_0),
inference(scs_inference,[],[i_0_46,i_0_49,i_0_128,i_0_130,i_0_126,i_0_124,i_0_122,i_0_391,i_0_394,i_0_88,i_0_397,i_0_120,i_0_379,i_0_382,i_0_385,i_0_388,i_0_132,i_0_422,i_0_425,i_0_38,i_0_39,i_0_40,i_0_41,i_0_80,i_0_59,i_0_67,i_0_68,i_0_69,i_0_70,i_0_57,i_0_58,i_0_48,i_0_83,i_0_86,i_0_85,i_0_87,i_0_73,i_0_79,i_0_98,i_0_99,i_0_104,i_0_76,i_0_102,i_0_106,i_0_51,i_0_52,i_0_42,i_0_72]) ).
cnf(i_0_431,plain,
( ~ end_point(X1,X2)
| X3 = X4
| X3 = X1
| ~ end_point(X3,X2)
| ~ end_point(X4,X2)
| X4 = X1 ),
inference(rename_variables,[],[i_0_72]) ).
cnf(i_0_432,plain,
esk11_2(esk14_4(esk15_0,esk16_0,esk17_0,esk18_0),esk16_0) != esk16_0,
inference(scs_inference,[],[i_0_46,i_0_49,i_0_128,i_0_130,i_0_126,i_0_124,i_0_122,i_0_391,i_0_394,i_0_88,i_0_397,i_0_120,i_0_379,i_0_382,i_0_385,i_0_388,i_0_132,i_0_422,i_0_425,i_0_38,i_0_39,i_0_40,i_0_41,i_0_80,i_0_59,i_0_67,i_0_68,i_0_69,i_0_70,i_0_57,i_0_58,i_0_48,i_0_83,i_0_86,i_0_85,i_0_87,i_0_73,i_0_79,i_0_98,i_0_99,i_0_104,i_0_76,i_0_102,i_0_106,i_0_51,i_0_52,i_0_42,i_0_72,i_0_90]) ).
cnf(i_0_433,plain,
( incident_c(esk8_1(X1),esk15_0)
| esk14_4(esk15_0,esk16_0,esk17_0,esk18_0) != sum(X2,X1) ),
inference(scs_inference,[],[i_0_46,i_0_49,i_0_128,i_0_130,i_0_126,i_0_124,i_0_122,i_0_391,i_0_394,i_0_88,i_0_397,i_0_120,i_0_379,i_0_382,i_0_385,i_0_388,i_0_132,i_0_422,i_0_425,i_0_38,i_0_39,i_0_40,i_0_41,i_0_80,i_0_59,i_0_67,i_0_68,i_0_69,i_0_70,i_0_57,i_0_58,i_0_48,i_0_83,i_0_86,i_0_85,i_0_87,i_0_73,i_0_79,i_0_98,i_0_99,i_0_104,i_0_76,i_0_102,i_0_106,i_0_51,i_0_52,i_0_42,i_0_72,i_0_90,i_0_161]) ).
cnf(i_0_434,plain,
( ~ part_of(sum(X1,X2),X3)
| incident_c(esk8_1(X2),X3) ),
inference(rename_variables,[],[i_0_161]) ).
cnf(i_0_435,plain,
( incident_c(esk8_1(X1),esk15_0)
| esk14_4(esk15_0,esk16_0,esk17_0,esk18_0) != sum(X1,X2) ),
inference(scs_inference,[],[i_0_46,i_0_49,i_0_128,i_0_130,i_0_126,i_0_124,i_0_122,i_0_391,i_0_394,i_0_88,i_0_397,i_0_120,i_0_379,i_0_382,i_0_385,i_0_388,i_0_132,i_0_422,i_0_425,i_0_38,i_0_39,i_0_40,i_0_41,i_0_80,i_0_59,i_0_67,i_0_68,i_0_69,i_0_70,i_0_57,i_0_58,i_0_48,i_0_83,i_0_86,i_0_85,i_0_87,i_0_73,i_0_79,i_0_98,i_0_99,i_0_104,i_0_76,i_0_102,i_0_106,i_0_51,i_0_52,i_0_42,i_0_72,i_0_90,i_0_161,i_0_179]) ).
cnf(i_0_436,plain,
( ~ part_of(sum(X1,X2),X3)
| incident_c(esk8_1(X1),X3) ),
inference(rename_variables,[],[i_0_179]) ).
cnf(i_0_437,plain,
( incident_c(esk8_1(X1),esk15_0)
| esk14_4(esk15_0,esk16_0,esk17_0,esk18_0) != sum(sum(X1,X2),X3) ),
inference(scs_inference,[],[i_0_46,i_0_49,i_0_128,i_0_130,i_0_126,i_0_124,i_0_122,i_0_391,i_0_394,i_0_88,i_0_397,i_0_120,i_0_379,i_0_382,i_0_385,i_0_388,i_0_132,i_0_422,i_0_425,i_0_38,i_0_39,i_0_40,i_0_41,i_0_80,i_0_59,i_0_67,i_0_68,i_0_69,i_0_70,i_0_57,i_0_58,i_0_48,i_0_83,i_0_86,i_0_85,i_0_87,i_0_73,i_0_79,i_0_98,i_0_99,i_0_104,i_0_76,i_0_102,i_0_106,i_0_51,i_0_52,i_0_42,i_0_72,i_0_90,i_0_161,i_0_179,i_0_170]) ).
cnf(i_0_438,plain,
( ~ part_of(sum(sum(X1,X2),X3),X4)
| incident_c(esk8_1(X1),X4) ),
inference(rename_variables,[],[i_0_170]) ).
cnf(i_0_439,plain,
( incident_c(esk8_1(sum(X1,X2)),sum(esk15_0,X3))
| esk14_4(esk15_0,esk16_0,esk17_0,esk18_0) != sum(sum(X1,X2),X4) ),
inference(scs_inference,[],[i_0_46,i_0_49,i_0_128,i_0_130,i_0_126,i_0_124,i_0_122,i_0_391,i_0_394,i_0_88,i_0_397,i_0_120,i_0_379,i_0_382,i_0_385,i_0_388,i_0_132,i_0_422,i_0_425,i_0_38,i_0_39,i_0_40,i_0_41,i_0_80,i_0_59,i_0_67,i_0_68,i_0_69,i_0_70,i_0_57,i_0_58,i_0_48,i_0_83,i_0_86,i_0_85,i_0_87,i_0_73,i_0_79,i_0_98,i_0_99,i_0_104,i_0_76,i_0_102,i_0_106,i_0_51,i_0_52,i_0_42,i_0_72,i_0_90,i_0_161,i_0_179,i_0_170,i_0_181]) ).
cnf(i_0_440,plain,
( ~ part_of(sum(X1,X2),X3)
| incident_c(esk8_1(X1),sum(X3,X4)) ),
inference(rename_variables,[],[i_0_181]) ).
cnf(i_0_441,plain,
( incident_c(esk8_1(sum(X1,X2)),sum(X3,esk15_0))
| esk14_4(esk15_0,esk16_0,esk17_0,esk18_0) != sum(sum(X1,X2),X4) ),
inference(scs_inference,[],[i_0_46,i_0_49,i_0_128,i_0_130,i_0_126,i_0_124,i_0_122,i_0_391,i_0_394,i_0_88,i_0_397,i_0_120,i_0_379,i_0_382,i_0_385,i_0_388,i_0_132,i_0_422,i_0_425,i_0_38,i_0_39,i_0_40,i_0_41,i_0_80,i_0_59,i_0_67,i_0_68,i_0_69,i_0_70,i_0_57,i_0_58,i_0_48,i_0_83,i_0_86,i_0_85,i_0_87,i_0_73,i_0_79,i_0_98,i_0_99,i_0_104,i_0_76,i_0_102,i_0_106,i_0_51,i_0_52,i_0_42,i_0_72,i_0_90,i_0_161,i_0_179,i_0_170,i_0_181,i_0_183]) ).
cnf(i_0_442,plain,
( ~ part_of(sum(X1,X2),X3)
| incident_c(esk8_1(X1),sum(X4,X3)) ),
inference(rename_variables,[],[i_0_183]) ).
cnf(i_0_443,plain,
( incident_c(esk8_1(X1),esk15_0)
| esk14_4(esk15_0,esk16_0,esk17_0,esk18_0) != sum(sum(X2,X3),sum(X1,X4)) ),
inference(scs_inference,[],[i_0_46,i_0_49,i_0_128,i_0_130,i_0_126,i_0_124,i_0_122,i_0_391,i_0_394,i_0_88,i_0_397,i_0_120,i_0_379,i_0_382,i_0_385,i_0_388,i_0_132,i_0_422,i_0_425,i_0_38,i_0_39,i_0_40,i_0_41,i_0_80,i_0_59,i_0_67,i_0_68,i_0_69,i_0_70,i_0_57,i_0_58,i_0_48,i_0_83,i_0_86,i_0_85,i_0_87,i_0_73,i_0_79,i_0_98,i_0_99,i_0_104,i_0_76,i_0_102,i_0_106,i_0_51,i_0_52,i_0_42,i_0_72,i_0_90,i_0_161,i_0_179,i_0_170,i_0_181,i_0_183,i_0_189]) ).
cnf(i_0_444,plain,
( ~ part_of(sum(X1,sum(X2,X3)),X4)
| incident_c(esk8_1(X2),X4) ),
inference(rename_variables,[],[i_0_189]) ).
cnf(i_0_445,plain,
( incident_c(esk8_1(X1),esk15_0)
| esk14_4(esk15_0,esk16_0,esk17_0,esk18_0) != sum(sum(X2,X1),sum(X3,X4)) ),
inference(scs_inference,[],[i_0_46,i_0_49,i_0_128,i_0_130,i_0_126,i_0_124,i_0_122,i_0_391,i_0_394,i_0_88,i_0_397,i_0_120,i_0_379,i_0_382,i_0_385,i_0_388,i_0_132,i_0_422,i_0_425,i_0_38,i_0_39,i_0_40,i_0_41,i_0_80,i_0_59,i_0_67,i_0_68,i_0_69,i_0_70,i_0_57,i_0_58,i_0_48,i_0_83,i_0_86,i_0_85,i_0_87,i_0_73,i_0_79,i_0_98,i_0_99,i_0_104,i_0_76,i_0_102,i_0_106,i_0_51,i_0_52,i_0_42,i_0_72,i_0_90,i_0_161,i_0_179,i_0_170,i_0_181,i_0_183,i_0_189,i_0_198]) ).
cnf(i_0_446,plain,
( ~ part_of(sum(sum(X1,X2),X3),X4)
| incident_c(esk8_1(X2),X4) ),
inference(rename_variables,[],[i_0_198]) ).
cnf(i_0_447,plain,
( incident_c(esk8_1(X1),esk15_0)
| esk14_4(esk15_0,esk16_0,esk17_0,esk18_0) != sum(sum(X2,X3),sum(X4,X1)) ),
inference(scs_inference,[],[i_0_46,i_0_49,i_0_128,i_0_130,i_0_126,i_0_124,i_0_122,i_0_391,i_0_394,i_0_88,i_0_397,i_0_120,i_0_379,i_0_382,i_0_385,i_0_388,i_0_132,i_0_422,i_0_425,i_0_38,i_0_39,i_0_40,i_0_41,i_0_80,i_0_59,i_0_67,i_0_68,i_0_69,i_0_70,i_0_57,i_0_58,i_0_48,i_0_83,i_0_86,i_0_85,i_0_87,i_0_73,i_0_79,i_0_98,i_0_99,i_0_104,i_0_76,i_0_102,i_0_106,i_0_51,i_0_52,i_0_42,i_0_72,i_0_90,i_0_161,i_0_179,i_0_170,i_0_181,i_0_183,i_0_189,i_0_198,i_0_206]) ).
cnf(i_0_448,plain,
( ~ part_of(sum(X1,sum(X2,X3)),X4)
| incident_c(esk8_1(X3),X4) ),
inference(rename_variables,[],[i_0_206]) ).
cnf(i_0_449,plain,
( incident_c(esk8_1(X1),sum(esk15_0,X2))
| esk14_4(esk15_0,esk16_0,esk17_0,esk18_0) != sum(sum(X1,X3),sum(X4,X5)) ),
inference(scs_inference,[],[i_0_46,i_0_49,i_0_128,i_0_130,i_0_126,i_0_124,i_0_122,i_0_391,i_0_394,i_0_88,i_0_397,i_0_120,i_0_379,i_0_382,i_0_385,i_0_388,i_0_132,i_0_422,i_0_425,i_0_38,i_0_39,i_0_40,i_0_41,i_0_80,i_0_59,i_0_67,i_0_68,i_0_69,i_0_70,i_0_57,i_0_58,i_0_48,i_0_83,i_0_86,i_0_85,i_0_87,i_0_73,i_0_79,i_0_98,i_0_99,i_0_104,i_0_76,i_0_102,i_0_106,i_0_51,i_0_52,i_0_42,i_0_72,i_0_90,i_0_161,i_0_179,i_0_170,i_0_181,i_0_183,i_0_189,i_0_198,i_0_206,i_0_172]) ).
cnf(i_0_450,plain,
( ~ part_of(sum(sum(X1,X2),X3),X4)
| incident_c(esk8_1(X1),sum(X4,X5)) ),
inference(rename_variables,[],[i_0_172]) ).
cnf(i_0_451,plain,
( incident_c(esk8_1(X1),sum(X2,esk15_0))
| esk14_4(esk15_0,esk16_0,esk17_0,esk18_0) != sum(sum(X1,X3),sum(X4,X5)) ),
inference(scs_inference,[],[i_0_46,i_0_49,i_0_128,i_0_130,i_0_126,i_0_124,i_0_122,i_0_391,i_0_394,i_0_88,i_0_397,i_0_120,i_0_379,i_0_382,i_0_385,i_0_388,i_0_132,i_0_422,i_0_425,i_0_38,i_0_39,i_0_40,i_0_41,i_0_80,i_0_59,i_0_67,i_0_68,i_0_69,i_0_70,i_0_57,i_0_58,i_0_48,i_0_83,i_0_86,i_0_85,i_0_87,i_0_73,i_0_79,i_0_98,i_0_99,i_0_104,i_0_76,i_0_102,i_0_106,i_0_51,i_0_52,i_0_42,i_0_72,i_0_90,i_0_161,i_0_179,i_0_170,i_0_181,i_0_183,i_0_189,i_0_198,i_0_206,i_0_172,i_0_174]) ).
cnf(i_0_452,plain,
( ~ part_of(sum(sum(X1,X2),X3),X4)
| incident_c(esk8_1(X1),sum(X5,X4)) ),
inference(rename_variables,[],[i_0_174]) ).
cnf(i_0_453,plain,
( incident_c(esk8_1(X1),sum(esk15_0,X2))
| esk14_4(esk15_0,esk16_0,esk17_0,esk18_0) != sum(sum(X3,X1),sum(X4,X5)) ),
inference(scs_inference,[],[i_0_46,i_0_49,i_0_128,i_0_130,i_0_126,i_0_124,i_0_122,i_0_391,i_0_394,i_0_88,i_0_397,i_0_120,i_0_379,i_0_382,i_0_385,i_0_388,i_0_132,i_0_422,i_0_425,i_0_38,i_0_39,i_0_40,i_0_41,i_0_80,i_0_59,i_0_67,i_0_68,i_0_69,i_0_70,i_0_57,i_0_58,i_0_48,i_0_83,i_0_86,i_0_85,i_0_87,i_0_73,i_0_79,i_0_98,i_0_99,i_0_104,i_0_76,i_0_102,i_0_106,i_0_51,i_0_52,i_0_42,i_0_72,i_0_90,i_0_161,i_0_179,i_0_170,i_0_181,i_0_183,i_0_189,i_0_198,i_0_206,i_0_172,i_0_174,i_0_200]) ).
cnf(i_0_454,plain,
( ~ part_of(sum(sum(X1,X2),X3),X4)
| incident_c(esk8_1(X2),sum(X4,X5)) ),
inference(rename_variables,[],[i_0_200]) ).
cnf(i_0_455,plain,
( incident_c(esk8_1(X1),sum(X2,esk15_0))
| esk14_4(esk15_0,esk16_0,esk17_0,esk18_0) != sum(sum(X3,X1),sum(X4,X5)) ),
inference(scs_inference,[],[i_0_46,i_0_49,i_0_128,i_0_130,i_0_126,i_0_124,i_0_122,i_0_391,i_0_394,i_0_88,i_0_397,i_0_120,i_0_379,i_0_382,i_0_385,i_0_388,i_0_132,i_0_422,i_0_425,i_0_38,i_0_39,i_0_40,i_0_41,i_0_80,i_0_59,i_0_67,i_0_68,i_0_69,i_0_70,i_0_57,i_0_58,i_0_48,i_0_83,i_0_86,i_0_85,i_0_87,i_0_73,i_0_79,i_0_98,i_0_99,i_0_104,i_0_76,i_0_102,i_0_106,i_0_51,i_0_52,i_0_42,i_0_72,i_0_90,i_0_161,i_0_179,i_0_170,i_0_181,i_0_183,i_0_189,i_0_198,i_0_206,i_0_172,i_0_174,i_0_200,i_0_202]) ).
cnf(i_0_456,plain,
( ~ part_of(sum(sum(X1,X2),X3),X4)
| incident_c(esk8_1(X2),sum(X5,X4)) ),
inference(rename_variables,[],[i_0_202]) ).
cnf(i_0_457,plain,
( incident_c(esk8_1(X1),sum(esk15_0,X2))
| esk14_4(esk15_0,esk16_0,esk17_0,esk18_0) != sum(sum(X3,X4),sum(X5,X1)) ),
inference(scs_inference,[],[i_0_46,i_0_49,i_0_128,i_0_130,i_0_126,i_0_124,i_0_122,i_0_391,i_0_394,i_0_88,i_0_397,i_0_120,i_0_379,i_0_382,i_0_385,i_0_388,i_0_132,i_0_422,i_0_425,i_0_38,i_0_39,i_0_40,i_0_41,i_0_80,i_0_59,i_0_67,i_0_68,i_0_69,i_0_70,i_0_57,i_0_58,i_0_48,i_0_83,i_0_86,i_0_85,i_0_87,i_0_73,i_0_79,i_0_98,i_0_99,i_0_104,i_0_76,i_0_102,i_0_106,i_0_51,i_0_52,i_0_42,i_0_72,i_0_90,i_0_161,i_0_179,i_0_170,i_0_181,i_0_183,i_0_189,i_0_198,i_0_206,i_0_172,i_0_174,i_0_200,i_0_202,i_0_208]) ).
cnf(i_0_458,plain,
( ~ part_of(sum(X1,sum(X2,X3)),X4)
| incident_c(esk8_1(X3),sum(X4,X5)) ),
inference(rename_variables,[],[i_0_208]) ).
cnf(i_0_459,plain,
( incident_c(esk8_1(X1),sum(X2,esk15_0))
| esk14_4(esk15_0,esk16_0,esk17_0,esk18_0) != sum(sum(X3,X4),sum(X5,X1)) ),
inference(scs_inference,[],[i_0_46,i_0_49,i_0_128,i_0_130,i_0_126,i_0_124,i_0_122,i_0_391,i_0_394,i_0_88,i_0_397,i_0_120,i_0_379,i_0_382,i_0_385,i_0_388,i_0_132,i_0_422,i_0_425,i_0_38,i_0_39,i_0_40,i_0_41,i_0_80,i_0_59,i_0_67,i_0_68,i_0_69,i_0_70,i_0_57,i_0_58,i_0_48,i_0_83,i_0_86,i_0_85,i_0_87,i_0_73,i_0_79,i_0_98,i_0_99,i_0_104,i_0_76,i_0_102,i_0_106,i_0_51,i_0_52,i_0_42,i_0_72,i_0_90,i_0_161,i_0_179,i_0_170,i_0_181,i_0_183,i_0_189,i_0_198,i_0_206,i_0_172,i_0_174,i_0_200,i_0_202,i_0_208,i_0_210]) ).
cnf(i_0_460,plain,
( ~ part_of(sum(X1,sum(X2,X3)),X4)
| incident_c(esk8_1(X3),sum(X5,X4)) ),
inference(rename_variables,[],[i_0_210]) ).
cnf(i_0_461,plain,
( X1 != esk18_0
| esk14_4(esk15_0,esk16_0,esk17_0,esk18_0) != sum(sum(X2,X3),sum(X4,X5))
| esk16_0 != X1 ),
inference(scs_inference,[],[i_0_46,i_0_49,i_0_128,i_0_130,i_0_126,i_0_124,i_0_122,i_0_391,i_0_394,i_0_88,i_0_397,i_0_120,i_0_379,i_0_382,i_0_385,i_0_388,i_0_132,i_0_422,i_0_425,i_0_38,i_0_39,i_0_40,i_0_41,i_0_80,i_0_59,i_0_67,i_0_68,i_0_69,i_0_70,i_0_57,i_0_58,i_0_48,i_0_83,i_0_86,i_0_85,i_0_87,i_0_73,i_0_79,i_0_98,i_0_99,i_0_104,i_0_76,i_0_102,i_0_106,i_0_51,i_0_52,i_0_42,i_0_72,i_0_90,i_0_161,i_0_179,i_0_170,i_0_181,i_0_183,i_0_189,i_0_198,i_0_206,i_0_172,i_0_174,i_0_200,i_0_202,i_0_208,i_0_210,i_0_91]) ).
cnf(i_0_462,plain,
part_of(esk14_4(esk15_0,esk16_0,esk17_0,esk18_0),esk15_0),
inference(equality_inference,[],[411]) ).
cnf(i_0_463,plain,
incident_c(esk8_1(X1),esk9_2(X1,esk8_1(X1))),
inference(scs_inference,[],[i_0_376,i_0_62]) ).
cnf(i_0_464,plain,
( ~ meet(X1,X2,X3)
| incident_c(X1,X2) ),
inference(rename_variables,[],[i_0_62]) ).
cnf(i_0_465,plain,
incident_c(esk8_1(X1),esk10_2(X1,esk8_1(X1))),
inference(scs_inference,[],[i_0_376,i_0_62,i_0_63]) ).
cnf(i_0_466,plain,
( ~ meet(X1,X2,X3)
| incident_c(X1,X3) ),
inference(rename_variables,[],[i_0_63]) ).
cnf(i_0_467,plain,
esk9_2(X1,esk8_1(X1)) != esk10_2(X1,esk8_1(X1)),
inference(scs_inference,[],[i_0_376,i_0_62,i_0_63,i_0_150]) ).
cnf(i_0_468,plain,
esk10_2(X1,esk8_1(X1)) != esk9_2(X1,esk8_1(X1)),
inference(scs_inference,[],[i_0_376,i_0_62,i_0_63,i_0_150,i_0_164]) ).
cnf(i_0_469,plain,
end_point(esk11_2(esk14_4(esk15_0,esk16_0,esk17_0,esk18_0),esk18_0),esk14_4(esk15_0,esk16_0,esk17_0,esk18_0)),
inference(scs_inference,[],[i_0_372,i_0_376,i_0_62,i_0_63,i_0_150,i_0_164,i_0_73]) ).
cnf(i_0_470,plain,
( ~ end_point(X1,X2)
| end_point(esk11_2(X2,X1),X2) ),
inference(rename_variables,[],[i_0_73]) ).
cnf(i_0_471,plain,
esk18_0 != esk11_2(esk14_4(esk15_0,esk16_0,esk17_0,esk18_0),esk18_0),
inference(scs_inference,[],[i_0_372,i_0_376,i_0_62,i_0_63,i_0_150,i_0_164,i_0_73,i_0_79]) ).
cnf(i_0_472,plain,
( ~ end_point(X1,X2)
| X1 != esk11_2(X2,X1) ),
inference(rename_variables,[],[i_0_79]) ).
cnf(i_0_473,plain,
~ inner_point(esk18_0,esk14_4(esk15_0,esk16_0,esk17_0,esk18_0)),
inference(scs_inference,[],[i_0_372,i_0_376,i_0_62,i_0_63,i_0_150,i_0_164,i_0_73,i_0_79,i_0_80]) ).
cnf(i_0_474,plain,
( ~ end_point(X1,X2)
| ~ inner_point(X1,X2) ),
inference(rename_variables,[],[i_0_80]) ).
cnf(i_0_475,plain,
esk3_2(esk8_1(X1),X1) != X1,
inference(scs_inference,[],[i_0_372,i_0_412,i_0_376,i_0_62,i_0_63,i_0_150,i_0_164,i_0_73,i_0_79,i_0_80,i_0_90]) ).
cnf(i_0_476,plain,
meet(esk17_0,esk9_2(esk14_4(esk15_0,esk16_0,esk17_0,esk18_0),esk17_0),esk10_2(esk14_4(esk15_0,esk16_0,esk17_0,esk18_0),esk17_0)),
inference(scs_inference,[],[i_0_372,i_0_368,i_0_412,i_0_376,i_0_62,i_0_63,i_0_150,i_0_164,i_0_73,i_0_79,i_0_80,i_0_90,i_0_59]) ).
cnf(i_0_477,plain,
( ~ inner_point(X1,X2)
| meet(X1,esk9_2(X2,X1),esk10_2(X2,X1)) ),
inference(rename_variables,[],[i_0_59]) ).
cnf(i_0_478,plain,
inner_point(esk8_1(esk18_0),esk11_2(esk14_4(esk15_0,esk16_0,esk17_0,esk18_0),esk16_0)),
inference(scs_inference,[],[i_0_372,i_0_368,i_0_412,i_0_430,i_0_376,i_0_88,i_0_62,i_0_63,i_0_150,i_0_164,i_0_73,i_0_79,i_0_80,i_0_90,i_0_59,i_0_105]) ).
cnf(i_0_479,plain,
inner_point(esk8_1(X1),X1),
inference(rename_variables,[],[i_0_88]) ).
cnf(i_0_480,plain,
incident_c(esk8_1(esk18_0),esk11_2(esk14_4(esk15_0,esk16_0,esk17_0,esk18_0),esk16_0)),
inference(scs_inference,[],[i_0_372,i_0_368,i_0_412,i_0_430,i_0_376,i_0_88,i_0_122,i_0_62,i_0_63,i_0_150,i_0_164,i_0_73,i_0_79,i_0_80,i_0_90,i_0_59,i_0_105,i_0_112]) ).
cnf(i_0_481,plain,
incident_c(esk8_1(X1),X1),
inference(rename_variables,[],[i_0_122]) ).
cnf(i_0_482,plain,
open(esk3_2(esk8_1(X1),X1)),
inference(scs_inference,[],[i_0_372,i_0_368,i_0_381,i_0_412,i_0_430,i_0_376,i_0_88,i_0_122,i_0_62,i_0_63,i_0_150,i_0_164,i_0_73,i_0_79,i_0_80,i_0_90,i_0_59,i_0_105,i_0_112,i_0_84]) ).
cnf(i_0_483,plain,
part_of(esk3_2(esk8_1(X1),X1),X1),
inference(rename_variables,[],[i_0_381]) ).
cnf(i_0_484,plain,
( ~ part_of(X1,X2)
| X1 = X2
| open(X1) ),
inference(rename_variables,[],[i_0_84]) ).
cnf(i_0_485,plain,
inner_point(esk5_3(esk8_1(X1),sum(X2,X1),sum(X2,X1)),sum(X2,X1)),
inference(scs_inference,[],[i_0_372,i_0_368,i_0_421,i_0_427,i_0_381,i_0_412,i_0_430,i_0_376,i_0_88,i_0_122,i_0_62,i_0_63,i_0_150,i_0_164,i_0_73,i_0_79,i_0_80,i_0_90,i_0_59,i_0_105,i_0_112,i_0_84,i_0_78]) ).
cnf(i_0_486,plain,
incident_c(esk5_3(esk8_1(X1),sum(X2,X1),sum(X2,X1)),sum(X2,X1)),
inference(rename_variables,[],[i_0_421]) ).
cnf(i_0_487,plain,
( ~ incident_c(X1,X2)
| end_point(X1,X2)
| inner_point(X1,X2) ),
inference(rename_variables,[],[i_0_78]) ).
cnf(i_0_488,plain,
part_of(esk4_2(esk5_3(esk8_1(X1),sum(X2,X1),sum(X2,X1)),sum(X2,X1)),sum(X2,X1)),
inference(scs_inference,[],[i_0_372,i_0_368,i_0_421,i_0_486,i_0_427,i_0_381,i_0_412,i_0_430,i_0_376,i_0_88,i_0_122,i_0_62,i_0_63,i_0_150,i_0_164,i_0_73,i_0_79,i_0_80,i_0_90,i_0_59,i_0_105,i_0_112,i_0_84,i_0_78,i_0_67]) ).
cnf(i_0_489,plain,
incident_c(esk5_3(esk8_1(X1),sum(X2,X1),sum(X2,X1)),sum(X2,X1)),
inference(rename_variables,[],[i_0_421]) ).
cnf(i_0_490,plain,
( ~ incident_c(X1,X2)
| end_point(X1,X2)
| part_of(esk4_2(X1,X2),X2) ),
inference(rename_variables,[],[i_0_67]) ).
cnf(i_0_491,plain,
part_of(esk3_2(esk5_3(esk8_1(X1),sum(X2,X1),sum(X2,X1)),sum(X2,X1)),sum(X2,X1)),
inference(scs_inference,[],[i_0_372,i_0_368,i_0_421,i_0_486,i_0_489,i_0_427,i_0_381,i_0_412,i_0_430,i_0_376,i_0_88,i_0_122,i_0_62,i_0_63,i_0_150,i_0_164,i_0_73,i_0_79,i_0_80,i_0_90,i_0_59,i_0_105,i_0_112,i_0_84,i_0_78,i_0_67,i_0_68]) ).
cnf(i_0_492,plain,
incident_c(esk5_3(esk8_1(X1),sum(X2,X1),sum(X2,X1)),sum(X2,X1)),
inference(rename_variables,[],[i_0_421]) ).
cnf(i_0_493,plain,
( ~ incident_c(X1,X2)
| end_point(X1,X2)
| part_of(esk3_2(X1,X2),X2) ),
inference(rename_variables,[],[i_0_68]) ).
cnf(i_0_494,plain,
esk11_2(esk14_4(esk15_0,esk16_0,esk17_0,esk18_0),esk16_0) != esk3_2(esk8_1(esk18_0),esk18_0),
inference(scs_inference,[],[i_0_372,i_0_368,i_0_421,i_0_486,i_0_489,i_0_427,i_0_381,i_0_412,i_0_430,i_0_376,i_0_88,i_0_122,i_0_62,i_0_63,i_0_150,i_0_164,i_0_73,i_0_79,i_0_80,i_0_90,i_0_59,i_0_105,i_0_112,i_0_84,i_0_78,i_0_67,i_0_68,i_0_91]) ).
cnf(i_0_495,plain,
X1 != esk3_2(esk8_1(X1),X1),
inference(rename_variables,[],[i_0_412]) ).
cnf(i_0_496,plain,
part_of(esk4_2(esk8_1(esk18_0),esk18_0),esk11_2(esk14_4(esk15_0,esk16_0,esk17_0,esk18_0),esk16_0)),
inference(scs_inference,[],[i_0_372,i_0_368,i_0_421,i_0_486,i_0_489,i_0_427,i_0_378,i_0_381,i_0_412,i_0_430,i_0_376,i_0_88,i_0_122,i_0_62,i_0_63,i_0_150,i_0_164,i_0_73,i_0_79,i_0_80,i_0_90,i_0_59,i_0_105,i_0_112,i_0_84,i_0_78,i_0_67,i_0_68,i_0_91,i_0_99]) ).
cnf(i_0_497,plain,
part_of(esk4_2(esk8_1(X1),X1),X1),
inference(rename_variables,[],[i_0_378]) ).
cnf(i_0_498,plain,
between_c(esk15_0,esk11_2(esk14_4(esk15_0,esk16_0,esk17_0,esk18_0),esk16_0),esk8_1(esk14_4(esk15_0,esk16_0,esk17_0,esk18_0)),esk16_0),
inference(scs_inference,[],[i_0_372,i_0_368,i_0_421,i_0_486,i_0_489,i_0_427,i_0_378,i_0_381,i_0_412,i_0_430,i_0_396,i_0_376,i_0_88,i_0_122,i_0_62,i_0_63,i_0_150,i_0_164,i_0_73,i_0_79,i_0_80,i_0_90,i_0_59,i_0_105,i_0_112,i_0_84,i_0_78,i_0_67,i_0_68,i_0_91,i_0_99,i_0_101]) ).
cnf(i_0_499,plain,
between_c(esk15_0,esk16_0,esk17_0,esk11_2(esk14_4(esk15_0,esk16_0,esk17_0,esk18_0),esk16_0)),
inference(scs_inference,[],[i_0_372,i_0_368,i_0_421,i_0_486,i_0_489,i_0_427,i_0_378,i_0_381,i_0_412,i_0_430,i_0_396,i_0_376,i_0_49,i_0_88,i_0_122,i_0_62,i_0_63,i_0_150,i_0_164,i_0_73,i_0_79,i_0_80,i_0_90,i_0_59,i_0_105,i_0_112,i_0_84,i_0_78,i_0_67,i_0_68,i_0_91,i_0_99,i_0_101,i_0_103]) ).
cnf(i_0_500,plain,
~ meet(X1,esk4_2(esk8_1(X2),X2),X2),
inference(scs_inference,[],[i_0_372,i_0_368,i_0_421,i_0_486,i_0_489,i_0_427,i_0_378,i_0_381,i_0_384,i_0_412,i_0_430,i_0_396,i_0_376,i_0_49,i_0_88,i_0_122,i_0_481,i_0_120,i_0_62,i_0_63,i_0_150,i_0_164,i_0_73,i_0_79,i_0_80,i_0_90,i_0_59,i_0_105,i_0_112,i_0_84,i_0_78,i_0_67,i_0_68,i_0_91,i_0_99,i_0_101,i_0_103,i_0_55]) ).
cnf(i_0_501,plain,
incident_c(esk8_1(X1),esk4_2(esk8_1(X1),X1)),
inference(rename_variables,[],[i_0_384]) ).
cnf(i_0_502,plain,
~ end_point(esk8_1(X1),X1),
inference(rename_variables,[],[i_0_120]) ).
cnf(i_0_503,plain,
( ~ incident_c(X1,X2)
| end_point(X1,X3)
| ~ meet(X4,X2,X3)
| ~ incident_c(X1,X3) ),
inference(rename_variables,[],[i_0_55]) ).
cnf(i_0_504,plain,
~ meet(X1,X2,esk4_2(esk8_1(X2),X2)),
inference(scs_inference,[],[i_0_372,i_0_368,i_0_421,i_0_486,i_0_489,i_0_427,i_0_378,i_0_381,i_0_384,i_0_501,i_0_412,i_0_430,i_0_396,i_0_376,i_0_49,i_0_88,i_0_122,i_0_481,i_0_120,i_0_502,i_0_62,i_0_63,i_0_150,i_0_164,i_0_73,i_0_79,i_0_80,i_0_90,i_0_59,i_0_105,i_0_112,i_0_84,i_0_78,i_0_67,i_0_68,i_0_91,i_0_99,i_0_101,i_0_103,i_0_55,i_0_54]) ).
cnf(i_0_505,plain,
incident_c(esk8_1(X1),esk4_2(esk8_1(X1),X1)),
inference(rename_variables,[],[i_0_384]) ).
cnf(i_0_506,plain,
~ end_point(esk8_1(X1),X1),
inference(rename_variables,[],[i_0_120]) ).
cnf(i_0_507,plain,
( ~ incident_c(X1,X2)
| end_point(X1,X3)
| ~ meet(X4,X3,X2)
| ~ incident_c(X1,X3) ),
inference(rename_variables,[],[i_0_54]) ).
cnf(i_0_508,plain,
( incident_c(X1,sum(X2,X3))
| esk5_3(esk8_1(X3),sum(X2,X3),sum(X2,X3)) != X1 ),
inference(scs_inference,[],[i_0_372,i_0_368,i_0_421,i_0_486,i_0_489,i_0_492,i_0_427,i_0_378,i_0_381,i_0_384,i_0_501,i_0_412,i_0_430,i_0_396,i_0_376,i_0_49,i_0_88,i_0_122,i_0_481,i_0_120,i_0_502,i_0_62,i_0_63,i_0_150,i_0_164,i_0_73,i_0_79,i_0_80,i_0_90,i_0_59,i_0_105,i_0_112,i_0_84,i_0_78,i_0_67,i_0_68,i_0_91,i_0_99,i_0_101,i_0_103,i_0_55,i_0_54,i_0_111]) ).
cnf(i_0_509,plain,
~ end_point(esk5_3(esk5_3(esk8_1(X1),sum(X2,X1),sum(X2,X1)),sum(X2,X1),sum(X2,X1)),sum(X2,X1)),
inference(scs_inference,[],[i_0_372,i_0_368,i_0_421,i_0_486,i_0_489,i_0_492,i_0_427,i_0_378,i_0_381,i_0_384,i_0_501,i_0_412,i_0_430,i_0_396,i_0_376,i_0_49,i_0_88,i_0_122,i_0_481,i_0_120,i_0_502,i_0_132,i_0_62,i_0_63,i_0_150,i_0_164,i_0_73,i_0_79,i_0_80,i_0_90,i_0_59,i_0_105,i_0_112,i_0_84,i_0_78,i_0_67,i_0_68,i_0_91,i_0_99,i_0_101,i_0_103,i_0_55,i_0_54,i_0_111,i_0_42]) ).
cnf(i_0_510,plain,
~ meet(X1,X2,X2),
inference(rename_variables,[],[i_0_132]) ).
cnf(i_0_511,plain,
( meet(X1,X2,X3)
| ~ end_point(esk5_3(X1,X2,X3),X3)
| ~ incident_c(X1,X3)
| ~ incident_c(X1,X2)
| ~ end_point(esk5_3(X1,X2,X3),X2) ),
inference(rename_variables,[],[i_0_42]) ).
cnf(i_0_512,plain,
between_c(esk15_0,esk11_2(esk14_4(esk15_0,esk16_0,esk17_0,esk18_0),esk16_0),esk17_0,esk16_0),
inference(scs_inference,[],[i_0_366,i_0_372,i_0_370,i_0_368,i_0_421,i_0_486,i_0_489,i_0_492,i_0_427,i_0_407,i_0_378,i_0_381,i_0_384,i_0_501,i_0_412,i_0_432,i_0_430,i_0_396,i_0_376,i_0_49,i_0_88,i_0_122,i_0_481,i_0_120,i_0_502,i_0_132,i_0_62,i_0_63,i_0_150,i_0_164,i_0_73,i_0_79,i_0_80,i_0_90,i_0_59,i_0_105,i_0_112,i_0_84,i_0_78,i_0_67,i_0_68,i_0_91,i_0_99,i_0_101,i_0_103,i_0_55,i_0_54,i_0_111,i_0_42,i_0_48]) ).
cnf(i_0_513,plain,
( X1 = X2
| between_c(X3,X1,X4,X2)
| ~ part_of(X5,X3)
| ~ inner_point(X4,X5)
| ~ end_point(X2,X5)
| ~ end_point(X1,X5) ),
inference(rename_variables,[],[i_0_48]) ).
cnf(i_0_514,plain,
esk11_2(esk14_4(esk15_0,esk16_0,esk17_0,esk18_0),esk16_0) = esk18_0,
inference(scs_inference,[],[i_0_366,i_0_372,i_0_370,i_0_368,i_0_421,i_0_486,i_0_489,i_0_492,i_0_427,i_0_407,i_0_378,i_0_381,i_0_384,i_0_501,i_0_412,i_0_432,i_0_430,i_0_396,i_0_376,i_0_130,i_0_49,i_0_88,i_0_122,i_0_481,i_0_120,i_0_502,i_0_132,i_0_62,i_0_63,i_0_150,i_0_164,i_0_73,i_0_79,i_0_80,i_0_90,i_0_59,i_0_105,i_0_112,i_0_84,i_0_78,i_0_67,i_0_68,i_0_91,i_0_99,i_0_101,i_0_103,i_0_55,i_0_54,i_0_111,i_0_42,i_0_48,i_0_72]) ).
cnf(i_0_515,plain,
( X1 = X2
| ~ end_point(X1,X3)
| ~ end_point(X4,X3)
| X1 = X4
| ~ end_point(X2,X3)
| X4 = X2 ),
inference(rename_variables,[],[i_0_72]) ).
cnf(i_0_516,plain,
part_of(esk14_4(esk15_0,esk16_0,esk17_0,esk18_0),esk14_4(esk15_0,esk16_0,esk17_0,esk18_0)),
inference(scs_inference,[],[i_0_366,i_0_372,i_0_370,i_0_368,i_0_421,i_0_486,i_0_489,i_0_492,i_0_427,i_0_407,i_0_378,i_0_381,i_0_384,i_0_501,i_0_412,i_0_432,i_0_430,i_0_396,i_0_376,i_0_130,i_0_49,i_0_88,i_0_122,i_0_481,i_0_120,i_0_502,i_0_132,i_0_62,i_0_63,i_0_150,i_0_164,i_0_73,i_0_79,i_0_80,i_0_90,i_0_59,i_0_105,i_0_112,i_0_84,i_0_78,i_0_67,i_0_68,i_0_91,i_0_99,i_0_101,i_0_103,i_0_55,i_0_54,i_0_111,i_0_42,i_0_48,i_0_72,i_0_50]) ).
cnf(i_0_517,plain,
( ~ part_of(X1,X2)
| ~ part_of(X3,X2)
| ~ end_point(X4,X1)
| ~ end_point(X4,X3)
| part_of(X1,X3)
| part_of(X5,X1)
| ~ part_of(X5,X2)
| ~ end_point(X4,X5)
| part_of(X3,X5)
| part_of(X5,X3)
| part_of(X1,X5)
| part_of(X3,X1) ),
inference(rename_variables,[],[i_0_50]) ).
cnf(i_0_518,plain,
~ end_point(esk8_1(esk18_0),esk11_2(esk14_4(esk15_0,esk16_0,esk17_0,esk18_0),esk16_0)),
inference(scs_inference,[],[i_0_366,i_0_372,i_0_370,i_0_368,i_0_421,i_0_486,i_0_489,i_0_492,i_0_427,i_0_407,i_0_378,i_0_381,i_0_384,i_0_501,i_0_412,i_0_432,i_0_430,i_0_396,i_0_376,i_0_130,i_0_49,i_0_88,i_0_122,i_0_481,i_0_120,i_0_502,i_0_132,i_0_62,i_0_63,i_0_150,i_0_164,i_0_73,i_0_79,i_0_80,i_0_90,i_0_59,i_0_105,i_0_112,i_0_84,i_0_78,i_0_67,i_0_68,i_0_91,i_0_99,i_0_101,i_0_103,i_0_55,i_0_54,i_0_111,i_0_42,i_0_48,i_0_72,i_0_50,i_0_192]) ).
cnf(i_0_519,plain,
( ~ closed(X1)
| X1 != esk14_4(esk15_0,esk16_0,esk17_0,esk18_0) ),
inference(scs_inference,[],[i_0_399,i_0_366,i_0_372,i_0_370,i_0_368,i_0_421,i_0_486,i_0_489,i_0_492,i_0_427,i_0_407,i_0_378,i_0_381,i_0_384,i_0_501,i_0_412,i_0_432,i_0_430,i_0_396,i_0_376,i_0_130,i_0_49,i_0_88,i_0_122,i_0_481,i_0_120,i_0_502,i_0_132,i_0_62,i_0_63,i_0_150,i_0_164,i_0_73,i_0_79,i_0_80,i_0_90,i_0_59,i_0_105,i_0_112,i_0_84,i_0_78,i_0_67,i_0_68,i_0_91,i_0_99,i_0_101,i_0_103,i_0_55,i_0_54,i_0_111,i_0_42,i_0_48,i_0_72,i_0_50,i_0_192,i_0_193,i_0_113]) ).
cnf(i_0_520,plain,
incident_c(esk5_3(esk8_1(X1),sum(X2,X1),sum(X2,X1)),sum(X2,X1)),
inference(equality_inference,[],[508]) ).
cnf(i_0_521,plain,
~ closed(esk14_4(esk15_0,esk16_0,esk17_0,esk18_0)),
inference(equality_inference,[],[519]) ).
cnf(i_0_522,plain,
incident_c(esk17_0,esk9_2(esk14_4(esk15_0,esk16_0,esk17_0,esk18_0),esk17_0)),
inference(scs_inference,[],[i_0_476,i_0_62]) ).
cnf(i_0_523,plain,
( ~ meet(X1,X2,X3)
| incident_c(X1,X2) ),
inference(rename_variables,[],[i_0_62]) ).
cnf(i_0_524,plain,
incident_c(esk17_0,esk10_2(esk14_4(esk15_0,esk16_0,esk17_0,esk18_0),esk17_0)),
inference(scs_inference,[],[i_0_476,i_0_62,i_0_63]) ).
cnf(i_0_525,plain,
( ~ meet(X1,X2,X3)
| incident_c(X1,X3) ),
inference(rename_variables,[],[i_0_63]) ).
cnf(i_0_526,plain,
esk9_2(esk14_4(esk15_0,esk16_0,esk17_0,esk18_0),esk17_0) != esk10_2(esk14_4(esk15_0,esk16_0,esk17_0,esk18_0),esk17_0),
inference(scs_inference,[],[i_0_476,i_0_62,i_0_63,i_0_150]) ).
cnf(i_0_527,plain,
esk10_2(esk14_4(esk15_0,esk16_0,esk17_0,esk18_0),esk17_0) != esk9_2(esk14_4(esk15_0,esk16_0,esk17_0,esk18_0),esk17_0),
inference(scs_inference,[],[i_0_476,i_0_62,i_0_63,i_0_150,i_0_164]) ).
cnf(i_0_528,plain,
$false,
inference(scs_inference,[],[i_0_514,i_0_512,i_0_476,i_0_62,i_0_63,i_0_150,i_0_164,i_0_193]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.20 % Problem : GEO112+1 : TPTP v9.2.1. Released v2.4.0.
% 0.03/0.20 % 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.12/0.43 % Computer : n003.cluster.edu
% 0.12/0.43 % Model : x86_64 x86_64
% 0.12/0.43 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.43 % Memory : 8042.1875MB
% 0.12/0.43 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.43 % CPULimit : 300
% 0.12/0.43 % WCLimit : 300
% 0.12/0.43 % DateTime : Mon May 4 17:41:41 EDT 2026
% 0.14/0.45 % CPUTime :
% 0.14/0.46 % start to proof: theBenchmark
% 38.94/26.08 % Version : CSE_E---1.7
% 38.94/26.08 % Problem : theBenchmark.p
% 38.94/26.08 % SZS status Theorem for theBenchmark.p
% 38.94/26.08 % SZS output start CNFRefutation
% See solution above
% 40.46/26.89 % Total time : 25.620s
%------------------------------------------------------------------------------