%------------------------------------------------------------------------------
% File : CSE_E---1.7
% Problem : MGT005+2 : TPTP v9.2.1. Bugfixed v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox2/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox2/solver/bin/cse --final-prover /export/starexec/sandbox2/solver/bin/eprover --proof-time %d --global-time-limit %d
% Computer : n004.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:47:04 PM UTC 2026
% Result : Theorem 56.72s 30.67s
% Output : CNFRefutation 58.27s
% Verified :
% SZS Type : ERROR: Analysing output (Could not find formula named 56)
% Comments :
%------------------------------------------------------------------------------
fof(t4_FOL,hypothesis,
! [X1,X4,X5,X8,X9,X10,X11] :
( ( organization(X1,X8)
& organization(X1,X9)
& reorganization(X1,X10,X11)
& survival_chance(X1,X4,X8)
& survival_chance(X1,X5,X9)
& ~ greater(X10,X8)
& greater(X9,X8)
& ~ greater(X9,X11) )
=> greater(X4,X5) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t4_FOL) ).
fof(t5_plus_FOL,conjecture,
! [X1,X2,X12,X13,X7,X4,X5,X14,X15,X6,X10,X11,X16] :
( ( organization(X1,X10)
& organization(X2,X10)
& organization(X1,X16)
& organization(X2,X16)
& class(X1,X13,X10)
& class(X2,X13,X10)
& survival_chance(X1,X7,X10)
& survival_chance(X2,X7,X10)
& reorganization(X1,X10,X11)
& reorganization(X2,X10,X16)
& reorganization_type(X1,X12,X10)
& reorganization_type(X2,X12,X10)
& reorganization_free(X1,X11,X16)
& survival_chance(X1,X4,X6)
& survival_chance(X2,X5,X6)
& complexity(X1,X14,X10)
& complexity(X2,X15,X10)
& greater(X15,X14)
& ( X6 = X16
=> greater(X4,X5) ) )
=> ( X6 = X11
=> ( greater(X4,X5)
| X4 = X5 ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t5_plus_FOL) ).
fof(a15_FOL,hypothesis,
! [X1,X2,X17,X18,X19,X20,X8,X9] :
( ( greater(X9,X8)
& survival_chance(X1,X17,X8)
& survival_chance(X2,X19,X8)
& survival_chance(X1,X18,X9)
& survival_chance(X2,X20,X9)
& greater(X18,X17)
& greater(X19,X18) )
=> ? [X21,X22,X23] :
( greater(X21,X8)
& greater(X9,X21)
& survival_chance(X1,X22,X21)
& survival_chance(X2,X23,X21)
& X22 = X23 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',a15_FOL) ).
fof(a11_FOL,hypothesis,
! [X1,X2,X12,X13,X7,X4,X5,X14,X15,X10,X11,X16] :
( ( organization(X1,X10)
& organization(X2,X10)
& organization(X1,X11)
& organization(X2,X11)
& class(X1,X13,X10)
& class(X2,X13,X10)
& survival_chance(X1,X7,X10)
& survival_chance(X2,X7,X10)
& reorganization(X1,X10,X11)
& reorganization(X2,X10,X16)
& reorganization_type(X1,X12,X10)
& reorganization_type(X2,X12,X10)
& survival_chance(X1,X4,X11)
& survival_chance(X2,X5,X11)
& complexity(X1,X14,X10)
& complexity(X2,X15,X10)
& greater(X15,X14) )
=> ( greater(X4,X5)
| X4 = X5 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',a11_FOL) ).
fof(a10_FOL,hypothesis,
! [X1,X2,X12,X13,X14,X15,X10,X11,X16] :
( ( organization(X1,X10)
& organization(X2,X10)
& organization(X2,X16)
& class(X1,X13,X10)
& class(X2,X13,X10)
& reorganization(X1,X10,X11)
& reorganization(X2,X10,X16)
& reorganization_type(X1,X12,X10)
& reorganization_type(X2,X12,X10)
& complexity(X1,X14,X10)
& complexity(X2,X15,X10)
& greater(X15,X14) )
=> greater(X16,X11) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',a10_FOL) ).
fof(t3_FOL,hypothesis,
! [X1,X4,X5,X8,X9] :
( ( organization(X1,X8)
& organization(X1,X9)
& reorganization_free(X1,X8,X9)
& survival_chance(X1,X4,X8)
& survival_chance(X1,X5,X9)
& greater(X9,X8) )
=> greater(X5,X4) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t3_FOL) ).
fof(mp14,axiom,
! [X1,X2,X4,X5,X6] :
( ( survival_chance(X1,X4,X6)
& survival_chance(X2,X5,X6) )
=> ( greater(X4,X5)
| X4 = X5
| greater(X5,X4) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mp14) ).
fof(mp13,axiom,
! [X1,X6,X8,X9] :
( ( organization(X1,X8)
& organization(X1,X9)
& greater(X6,X8)
& greater(X9,X6) )
=> organization(X1,X6) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mp13) ).
fof(mp12,axiom,
! [X1,X6] :
( organization(X1,X6)
=> ? [X7] : survival_chance(X1,X7,X6) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mp12) ).
fof(mp7,axiom,
! [X1,X10,X11] :
( reorganization(X1,X10,X11)
=> greater(X11,X10) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mp7) ).
fof(mp11,axiom,
! [X1,X2,X3] :
( ( greater(X1,X2)
& greater(X2,X3) )
=> greater(X1,X3) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mp11) ).
fof(mp6_2,axiom,
! [X1,X2] :
~ ( greater(X1,X2)
& greater(X2,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mp6_2) ).
fof(mp6_1,axiom,
! [X1,X2] :
~ ( greater(X1,X2)
& X1 = X2 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mp6_1) ).
fof(i_0_13,hypothesis,
! [X1,X4,X5,X8,X9,X10,X11] :
( ( organization(X1,X8)
& organization(X1,X9)
& reorganization(X1,X10,X11)
& survival_chance(X1,X4,X8)
& survival_chance(X1,X5,X9)
& ~ greater(X10,X8)
& greater(X9,X8)
& ~ greater(X9,X11) )
=> greater(X4,X5) ),
inference(fof_simplification,[status(thm)],[t4_FOL]) ).
fof(i_0_14,negated_conjecture,
~ ! [X1,X2,X12,X13,X7,X4,X5,X14,X15,X6,X10,X11,X16] :
( ( organization(X1,X10)
& organization(X2,X10)
& organization(X1,X16)
& organization(X2,X16)
& class(X1,X13,X10)
& class(X2,X13,X10)
& survival_chance(X1,X7,X10)
& survival_chance(X2,X7,X10)
& reorganization(X1,X10,X11)
& reorganization(X2,X10,X16)
& reorganization_type(X1,X12,X10)
& reorganization_type(X2,X12,X10)
& reorganization_free(X1,X11,X16)
& survival_chance(X1,X4,X6)
& survival_chance(X2,X5,X6)
& complexity(X1,X14,X10)
& complexity(X2,X15,X10)
& greater(X15,X14)
& ( X6 = X16
=> greater(X4,X5) ) )
=> ( X6 = X11
=> ( greater(X4,X5)
| X4 = X5 ) ) ),
inference(assume_negation,[status(cth)],[t5_plus_FOL]) ).
fof(i_0_15,hypothesis,
! [X158,X159,X160,X161,X162,X163,X164,X165] :
( ( greater(esk2_8(X158,X159,X160,X161,X162,X163,X164,X165),X164)
| ~ greater(X165,X164)
| ~ survival_chance(X158,X160,X164)
| ~ survival_chance(X159,X162,X164)
| ~ survival_chance(X158,X161,X165)
| ~ survival_chance(X159,X163,X165)
| ~ greater(X161,X160)
| ~ greater(X162,X161) )
& ( greater(X165,esk2_8(X158,X159,X160,X161,X162,X163,X164,X165))
| ~ greater(X165,X164)
| ~ survival_chance(X158,X160,X164)
| ~ survival_chance(X159,X162,X164)
| ~ survival_chance(X158,X161,X165)
| ~ survival_chance(X159,X163,X165)
| ~ greater(X161,X160)
| ~ greater(X162,X161) )
& ( survival_chance(X158,esk3_8(X158,X159,X160,X161,X162,X163,X164,X165),esk2_8(X158,X159,X160,X161,X162,X163,X164,X165))
| ~ greater(X165,X164)
| ~ survival_chance(X158,X160,X164)
| ~ survival_chance(X159,X162,X164)
| ~ survival_chance(X158,X161,X165)
| ~ survival_chance(X159,X163,X165)
| ~ greater(X161,X160)
| ~ greater(X162,X161) )
& ( survival_chance(X159,esk4_8(X158,X159,X160,X161,X162,X163,X164,X165),esk2_8(X158,X159,X160,X161,X162,X163,X164,X165))
| ~ greater(X165,X164)
| ~ survival_chance(X158,X160,X164)
| ~ survival_chance(X159,X162,X164)
| ~ survival_chance(X158,X161,X165)
| ~ survival_chance(X159,X163,X165)
| ~ greater(X161,X160)
| ~ greater(X162,X161) )
& ( esk3_8(X158,X159,X160,X161,X162,X163,X164,X165) = esk4_8(X158,X159,X160,X161,X162,X163,X164,X165)
| ~ greater(X165,X164)
| ~ survival_chance(X158,X160,X164)
| ~ survival_chance(X159,X162,X164)
| ~ survival_chance(X158,X161,X165)
| ~ survival_chance(X159,X163,X165)
| ~ greater(X161,X160)
| ~ greater(X162,X161) ) ),
inference(distribute,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[a15_FOL])])])]) ).
fof(i_0_16,hypothesis,
! [X146,X147,X148,X149,X150,X151,X152,X153,X154,X155,X156,X157] :
( ~ organization(X146,X155)
| ~ organization(X147,X155)
| ~ organization(X146,X156)
| ~ organization(X147,X156)
| ~ class(X146,X149,X155)
| ~ class(X147,X149,X155)
| ~ survival_chance(X146,X150,X155)
| ~ survival_chance(X147,X150,X155)
| ~ reorganization(X146,X155,X156)
| ~ reorganization(X147,X155,X157)
| ~ reorganization_type(X146,X148,X155)
| ~ reorganization_type(X147,X148,X155)
| ~ survival_chance(X146,X151,X156)
| ~ survival_chance(X147,X152,X156)
| ~ complexity(X146,X153,X155)
| ~ complexity(X147,X154,X155)
| ~ greater(X154,X153)
| greater(X151,X152)
| X151 = X152 ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[a11_FOL])]) ).
fof(i_0_17,hypothesis,
! [X137,X138,X139,X140,X141,X142,X143,X144,X145] :
( ~ organization(X137,X143)
| ~ organization(X138,X143)
| ~ organization(X138,X145)
| ~ class(X137,X140,X143)
| ~ class(X138,X140,X143)
| ~ reorganization(X137,X143,X144)
| ~ reorganization(X138,X143,X145)
| ~ reorganization_type(X137,X139,X143)
| ~ reorganization_type(X138,X139,X143)
| ~ complexity(X137,X141,X143)
| ~ complexity(X138,X142,X143)
| ~ greater(X142,X141)
| greater(X145,X144) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[a10_FOL])]) ).
fof(i_0_18,hypothesis,
! [X130,X131,X132,X133,X134,X135,X136] :
( ~ organization(X130,X133)
| ~ organization(X130,X134)
| ~ reorganization(X130,X135,X136)
| ~ survival_chance(X130,X131,X133)
| ~ survival_chance(X130,X132,X134)
| greater(X135,X133)
| ~ greater(X134,X133)
| greater(X134,X136)
| greater(X131,X132) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[i_0_13])]) ).
fof(i_0_19,hypothesis,
! [X125,X126,X127,X128,X129] :
( ~ organization(X125,X128)
| ~ organization(X125,X129)
| ~ reorganization_free(X125,X128,X129)
| ~ survival_chance(X125,X126,X128)
| ~ survival_chance(X125,X127,X129)
| ~ greater(X129,X128)
| greater(X127,X126) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[t3_FOL])]) ).
fof(i_0_20,plain,
! [X110,X111,X112,X113,X114] :
( ~ survival_chance(X110,X112,X114)
| ~ survival_chance(X111,X113,X114)
| greater(X112,X113)
| X112 = X113
| greater(X113,X112) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mp14])]) ).
fof(i_0_21,plain,
! [X118,X119,X120,X121] :
( ~ organization(X118,X120)
| ~ organization(X118,X121)
| ~ greater(X119,X120)
| ~ greater(X121,X119)
| organization(X118,X119) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mp13])]) ).
fof(i_0_22,plain,
! [X115,X116] :
( ~ organization(X115,X116)
| survival_chance(X115,esk1_2(X115,X116),X116) ),
inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mp12])])]) ).
fof(i_0_23,plain,
! [X122,X123,X124] :
( ~ reorganization(X122,X123,X124)
| greater(X124,X123) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mp7])]) ).
fof(i_0_24,plain,
! [X107,X108,X109] :
( ~ greater(X107,X108)
| ~ greater(X108,X109)
| greater(X107,X109) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mp11])]) ).
fof(i_0_25,negated_conjecture,
( organization(esk5_0,esk15_0)
& organization(esk6_0,esk15_0)
& organization(esk5_0,esk17_0)
& organization(esk6_0,esk17_0)
& class(esk5_0,esk8_0,esk15_0)
& class(esk6_0,esk8_0,esk15_0)
& survival_chance(esk5_0,esk9_0,esk15_0)
& survival_chance(esk6_0,esk9_0,esk15_0)
& reorganization(esk5_0,esk15_0,esk16_0)
& reorganization(esk6_0,esk15_0,esk17_0)
& reorganization_type(esk5_0,esk7_0,esk15_0)
& reorganization_type(esk6_0,esk7_0,esk15_0)
& reorganization_free(esk5_0,esk16_0,esk17_0)
& survival_chance(esk5_0,esk10_0,esk14_0)
& survival_chance(esk6_0,esk11_0,esk14_0)
& complexity(esk5_0,esk12_0,esk15_0)
& complexity(esk6_0,esk13_0,esk15_0)
& greater(esk13_0,esk12_0)
& ( esk14_0 != esk17_0
| greater(esk10_0,esk11_0) )
& esk14_0 = esk16_0
& ~ greater(esk10_0,esk11_0)
& esk10_0 != esk11_0 ),
inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[i_0_14])])]) ).
fof(i_0_26,plain,
! [X105,X106] :
( ~ greater(X105,X106)
| ~ greater(X106,X105) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mp6_2])]) ).
fof(i_0_27,plain,
! [X103,X104] :
( ~ greater(X103,X104)
| X103 != X104 ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mp6_1])]) ).
cnf(i_0_28,hypothesis,
( survival_chance(X1,esk4_8(X2,X1,X3,X4,X5,X6,X7,X8),esk2_8(X2,X1,X3,X4,X5,X6,X7,X8))
| ~ greater(X8,X7)
| ~ survival_chance(X2,X3,X7)
| ~ survival_chance(X1,X5,X7)
| ~ survival_chance(X2,X4,X8)
| ~ survival_chance(X1,X6,X8)
| ~ greater(X4,X3)
| ~ greater(X5,X4) ),
inference(split_conjunct,[status(thm)],[i_0_15]),
[final] ).
cnf(i_0_29,hypothesis,
( survival_chance(X1,esk3_8(X1,X2,X3,X4,X5,X6,X7,X8),esk2_8(X1,X2,X3,X4,X5,X6,X7,X8))
| ~ greater(X8,X7)
| ~ survival_chance(X1,X3,X7)
| ~ survival_chance(X2,X5,X7)
| ~ survival_chance(X1,X4,X8)
| ~ survival_chance(X2,X6,X8)
| ~ greater(X4,X3)
| ~ greater(X5,X4) ),
inference(split_conjunct,[status(thm)],[i_0_15]),
[final] ).
cnf(i_0_30,hypothesis,
( greater(esk2_8(X1,X2,X3,X4,X5,X6,X7,X8),X7)
| ~ greater(X8,X7)
| ~ survival_chance(X1,X3,X7)
| ~ survival_chance(X2,X5,X7)
| ~ survival_chance(X1,X4,X8)
| ~ survival_chance(X2,X6,X8)
| ~ greater(X4,X3)
| ~ greater(X5,X4) ),
inference(split_conjunct,[status(thm)],[i_0_15]),
[final] ).
cnf(i_0_31,hypothesis,
( greater(X1,esk2_8(X2,X3,X4,X5,X6,X7,X8,X1))
| ~ greater(X1,X8)
| ~ survival_chance(X2,X4,X8)
| ~ survival_chance(X3,X6,X8)
| ~ survival_chance(X2,X5,X1)
| ~ survival_chance(X3,X7,X1)
| ~ greater(X5,X4)
| ~ greater(X6,X5) ),
inference(split_conjunct,[status(thm)],[i_0_15]),
[final] ).
cnf(i_0_32,hypothesis,
( esk3_8(X1,X2,X3,X4,X5,X6,X7,X8) = esk4_8(X1,X2,X3,X4,X5,X6,X7,X8)
| ~ greater(X8,X7)
| ~ survival_chance(X1,X3,X7)
| ~ survival_chance(X2,X5,X7)
| ~ survival_chance(X1,X4,X8)
| ~ survival_chance(X2,X6,X8)
| ~ greater(X4,X3)
| ~ greater(X5,X4) ),
inference(split_conjunct,[status(thm)],[i_0_15]),
[final] ).
cnf(i_0_33,hypothesis,
( greater(X9,X10)
| X9 = X10
| ~ organization(X1,X2)
| ~ organization(X3,X2)
| ~ organization(X1,X4)
| ~ organization(X3,X4)
| ~ class(X1,X5,X2)
| ~ class(X3,X5,X2)
| ~ survival_chance(X1,X6,X2)
| ~ survival_chance(X3,X6,X2)
| ~ reorganization(X1,X2,X4)
| ~ reorganization(X3,X2,X7)
| ~ reorganization_type(X1,X8,X2)
| ~ reorganization_type(X3,X8,X2)
| ~ survival_chance(X1,X9,X4)
| ~ survival_chance(X3,X10,X4)
| ~ complexity(X1,X11,X2)
| ~ complexity(X3,X12,X2)
| ~ greater(X12,X11) ),
inference(split_conjunct,[status(thm)],[i_0_16]),
[final] ).
cnf(i_0_34,hypothesis,
( greater(X4,X6)
| ~ organization(X1,X2)
| ~ organization(X3,X2)
| ~ organization(X3,X4)
| ~ class(X1,X5,X2)
| ~ class(X3,X5,X2)
| ~ reorganization(X1,X2,X6)
| ~ reorganization(X3,X2,X4)
| ~ reorganization_type(X1,X7,X2)
| ~ reorganization_type(X3,X7,X2)
| ~ complexity(X1,X8,X2)
| ~ complexity(X3,X9,X2)
| ~ greater(X9,X8) ),
inference(split_conjunct,[status(thm)],[i_0_17]),
[final] ).
cnf(i_0_35,hypothesis,
( greater(X4,X2)
| greater(X3,X5)
| greater(X6,X7)
| ~ organization(X1,X2)
| ~ organization(X1,X3)
| ~ reorganization(X1,X4,X5)
| ~ survival_chance(X1,X6,X2)
| ~ survival_chance(X1,X7,X3)
| ~ greater(X3,X2) ),
inference(split_conjunct,[status(thm)],[i_0_18]),
[final] ).
cnf(i_0_36,hypothesis,
( greater(X5,X4)
| ~ organization(X1,X2)
| ~ organization(X1,X3)
| ~ reorganization_free(X1,X2,X3)
| ~ survival_chance(X1,X4,X2)
| ~ survival_chance(X1,X5,X3)
| ~ greater(X3,X2) ),
inference(split_conjunct,[status(thm)],[i_0_19]),
[final] ).
cnf(i_0_37,plain,
( greater(X2,X5)
| X2 = X5
| greater(X5,X2)
| ~ survival_chance(X1,X2,X3)
| ~ survival_chance(X4,X5,X3) ),
inference(split_conjunct,[status(thm)],[i_0_20]),
[final] ).
cnf(i_0_38,plain,
( organization(X1,X4)
| ~ organization(X1,X2)
| ~ organization(X1,X3)
| ~ greater(X4,X2)
| ~ greater(X3,X4) ),
inference(split_conjunct,[status(thm)],[i_0_21]),
[final] ).
cnf(i_0_39,plain,
( survival_chance(X1,esk1_2(X1,X2),X2)
| ~ organization(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_22]),
[final] ).
cnf(i_0_40,plain,
( greater(X3,X2)
| ~ reorganization(X1,X2,X3) ),
inference(split_conjunct,[status(thm)],[i_0_23]),
[final] ).
cnf(i_0_41,plain,
( greater(X1,X3)
| ~ greater(X1,X2)
| ~ greater(X2,X3) ),
inference(split_conjunct,[status(thm)],[i_0_24]),
[final] ).
cnf(i_0_42,negated_conjecture,
complexity(esk6_0,esk13_0,esk15_0),
inference(split_conjunct,[status(thm)],[i_0_25]),
[final] ).
cnf(i_0_43,negated_conjecture,
complexity(esk5_0,esk12_0,esk15_0),
inference(split_conjunct,[status(thm)],[i_0_25]),
[final] ).
cnf(i_0_44,negated_conjecture,
reorganization_type(esk6_0,esk7_0,esk15_0),
inference(split_conjunct,[status(thm)],[i_0_25]),
[final] ).
cnf(i_0_45,negated_conjecture,
reorganization_type(esk5_0,esk7_0,esk15_0),
inference(split_conjunct,[status(thm)],[i_0_25]),
[final] ).
cnf(i_0_46,negated_conjecture,
class(esk6_0,esk8_0,esk15_0),
inference(split_conjunct,[status(thm)],[i_0_25]),
[final] ).
cnf(i_0_47,negated_conjecture,
class(esk5_0,esk8_0,esk15_0),
inference(split_conjunct,[status(thm)],[i_0_25]),
[final] ).
cnf(i_0_48,negated_conjecture,
reorganization_free(esk5_0,esk16_0,esk17_0),
inference(split_conjunct,[status(thm)],[i_0_25]),
[final] ).
cnf(i_0_49,negated_conjecture,
reorganization(esk6_0,esk15_0,esk17_0),
inference(split_conjunct,[status(thm)],[i_0_25]),
[final] ).
cnf(i_0_50,negated_conjecture,
reorganization(esk5_0,esk15_0,esk16_0),
inference(split_conjunct,[status(thm)],[i_0_25]),
[final] ).
cnf(i_0_51,negated_conjecture,
survival_chance(esk6_0,esk11_0,esk14_0),
inference(split_conjunct,[status(thm)],[i_0_25]),
[final] ).
cnf(i_0_52,negated_conjecture,
survival_chance(esk6_0,esk9_0,esk15_0),
inference(split_conjunct,[status(thm)],[i_0_25]),
[final] ).
cnf(i_0_53,negated_conjecture,
survival_chance(esk5_0,esk10_0,esk14_0),
inference(split_conjunct,[status(thm)],[i_0_25]),
[final] ).
cnf(i_0_54,negated_conjecture,
survival_chance(esk5_0,esk9_0,esk15_0),
inference(split_conjunct,[status(thm)],[i_0_25]),
[final] ).
cnf(i_0_55,plain,
( ~ greater(X1,X2)
| ~ greater(X2,X1) ),
inference(split_conjunct,[status(thm)],[i_0_26]),
[final] ).
cnf(i_0_56,plain,
( ~ greater(X1,X2)
| X1 != X2 ),
inference(split_conjunct,[status(thm)],[i_0_27]),
[final] ).
cnf(i_0_57,negated_conjecture,
~ greater(esk10_0,esk11_0),
inference(split_conjunct,[status(thm)],[i_0_25]),
[final] ).
cnf(i_0_58,negated_conjecture,
( greater(esk10_0,esk11_0)
| esk14_0 != esk17_0 ),
inference(split_conjunct,[status(thm)],[i_0_25]),
[final] ).
cnf(i_0_59,negated_conjecture,
organization(esk6_0,esk17_0),
inference(split_conjunct,[status(thm)],[i_0_25]),
[final] ).
cnf(i_0_60,negated_conjecture,
organization(esk6_0,esk15_0),
inference(split_conjunct,[status(thm)],[i_0_25]),
[final] ).
cnf(i_0_61,negated_conjecture,
organization(esk5_0,esk17_0),
inference(split_conjunct,[status(thm)],[i_0_25]),
[final] ).
cnf(i_0_62,negated_conjecture,
organization(esk5_0,esk15_0),
inference(split_conjunct,[status(thm)],[i_0_25]),
[final] ).
cnf(i_0_63,negated_conjecture,
greater(esk13_0,esk12_0),
inference(split_conjunct,[status(thm)],[i_0_25]),
[final] ).
cnf(i_0_64,negated_conjecture,
esk10_0 != esk11_0,
inference(split_conjunct,[status(thm)],[i_0_25]),
[final] ).
cnf(i_0_65,negated_conjecture,
esk14_0 = esk16_0,
inference(split_conjunct,[status(thm)],[i_0_25]),
[final] ).
cnf(i_0_66,axiom,
X1 = X1 ).
cnf(i_0_67,axiom,
( X1 = X2
| X2 != X1 ) ).
cnf(i_0_68,axiom,
( X1 = X2
| X1 != X3
| X3 != X2 ) ).
cnf(i_0_69,axiom,
( X1 != X2
| esk4_8(X1,X3,X4,X5,X6,X7,X8,X9) = esk4_8(X2,X3,X4,X5,X6,X7,X8,X9) ) ).
cnf(i_0_70,axiom,
( X1 != X2
| esk4_8(X3,X1,X4,X5,X6,X7,X8,X9) = esk4_8(X3,X2,X4,X5,X6,X7,X8,X9) ) ).
cnf(i_0_71,axiom,
( X1 != X2
| esk4_8(X3,X4,X1,X5,X6,X7,X8,X9) = esk4_8(X3,X4,X2,X5,X6,X7,X8,X9) ) ).
cnf(i_0_72,axiom,
( X1 != X2
| esk4_8(X3,X4,X5,X1,X6,X7,X8,X9) = esk4_8(X3,X4,X5,X2,X6,X7,X8,X9) ) ).
cnf(i_0_73,axiom,
( X1 != X2
| esk4_8(X3,X4,X5,X6,X1,X7,X8,X9) = esk4_8(X3,X4,X5,X6,X2,X7,X8,X9) ) ).
cnf(i_0_74,axiom,
( X1 != X2
| esk4_8(X3,X4,X5,X6,X7,X1,X8,X9) = esk4_8(X3,X4,X5,X6,X7,X2,X8,X9) ) ).
cnf(i_0_75,axiom,
( X1 != X2
| esk4_8(X3,X4,X5,X6,X7,X8,X1,X9) = esk4_8(X3,X4,X5,X6,X7,X8,X2,X9) ) ).
cnf(i_0_76,axiom,
( X1 != X2
| esk4_8(X3,X4,X5,X6,X7,X8,X9,X1) = esk4_8(X3,X4,X5,X6,X7,X8,X9,X2) ) ).
cnf(i_0_77,axiom,
( X1 != X2
| esk3_8(X1,X3,X4,X5,X6,X7,X8,X9) = esk3_8(X2,X3,X4,X5,X6,X7,X8,X9) ) ).
cnf(i_0_78,axiom,
( X1 != X2
| esk3_8(X3,X1,X4,X5,X6,X7,X8,X9) = esk3_8(X3,X2,X4,X5,X6,X7,X8,X9) ) ).
cnf(i_0_79,axiom,
( X1 != X2
| esk3_8(X3,X4,X1,X5,X6,X7,X8,X9) = esk3_8(X3,X4,X2,X5,X6,X7,X8,X9) ) ).
cnf(i_0_80,axiom,
( X1 != X2
| esk3_8(X3,X4,X5,X1,X6,X7,X8,X9) = esk3_8(X3,X4,X5,X2,X6,X7,X8,X9) ) ).
cnf(i_0_81,axiom,
( X1 != X2
| esk3_8(X3,X4,X5,X6,X1,X7,X8,X9) = esk3_8(X3,X4,X5,X6,X2,X7,X8,X9) ) ).
cnf(i_0_82,axiom,
( X1 != X2
| esk3_8(X3,X4,X5,X6,X7,X1,X8,X9) = esk3_8(X3,X4,X5,X6,X7,X2,X8,X9) ) ).
cnf(i_0_83,axiom,
( X1 != X2
| esk3_8(X3,X4,X5,X6,X7,X8,X1,X9) = esk3_8(X3,X4,X5,X6,X7,X8,X2,X9) ) ).
cnf(i_0_84,axiom,
( X1 != X2
| esk3_8(X3,X4,X5,X6,X7,X8,X9,X1) = esk3_8(X3,X4,X5,X6,X7,X8,X9,X2) ) ).
cnf(i_0_85,axiom,
( X1 != X2
| ~ survival_chance(X1,X3,X4)
| survival_chance(X2,X3,X4) ) ).
cnf(i_0_86,axiom,
( X1 != X2
| ~ survival_chance(X3,X1,X4)
| survival_chance(X3,X2,X4) ) ).
cnf(i_0_87,axiom,
( X1 != X2
| ~ survival_chance(X3,X4,X1)
| survival_chance(X3,X4,X2) ) ).
cnf(i_0_88,axiom,
( X1 != X2
| ~ greater(X1,X3)
| greater(X2,X3) ) ).
cnf(i_0_89,axiom,
( X1 != X2
| ~ greater(X3,X1)
| greater(X3,X2) ) ).
cnf(i_0_90,axiom,
( X1 != X2
| ~ organization(X1,X3)
| organization(X2,X3) ) ).
cnf(i_0_91,axiom,
( X1 != X2
| ~ organization(X3,X1)
| organization(X3,X2) ) ).
cnf(i_0_92,axiom,
( X1 != X2
| ~ class(X1,X3,X4)
| class(X2,X3,X4) ) ).
cnf(i_0_93,axiom,
( X1 != X2
| ~ class(X3,X1,X4)
| class(X3,X2,X4) ) ).
cnf(i_0_94,axiom,
( X1 != X2
| ~ class(X3,X4,X1)
| class(X3,X4,X2) ) ).
cnf(i_0_95,axiom,
( X1 != X2
| ~ reorganization(X1,X3,X4)
| reorganization(X2,X3,X4) ) ).
cnf(i_0_96,axiom,
( X1 != X2
| ~ reorganization(X3,X1,X4)
| reorganization(X3,X2,X4) ) ).
cnf(i_0_97,axiom,
( X1 != X2
| ~ reorganization(X3,X4,X1)
| reorganization(X3,X4,X2) ) ).
cnf(i_0_98,axiom,
( X1 != X2
| ~ reorganization_type(X1,X3,X4)
| reorganization_type(X2,X3,X4) ) ).
cnf(i_0_99,axiom,
( X1 != X2
| ~ reorganization_type(X3,X1,X4)
| reorganization_type(X3,X2,X4) ) ).
cnf(i_0_100,axiom,
( X1 != X2
| ~ reorganization_type(X3,X4,X1)
| reorganization_type(X3,X4,X2) ) ).
cnf(i_0_101,axiom,
( X1 != X2
| ~ complexity(X1,X3,X4)
| complexity(X2,X3,X4) ) ).
cnf(i_0_102,axiom,
( X1 != X2
| ~ complexity(X3,X1,X4)
| complexity(X3,X2,X4) ) ).
cnf(i_0_103,axiom,
( X1 != X2
| ~ complexity(X3,X4,X1)
| complexity(X3,X4,X2) ) ).
cnf(i_0_104,axiom,
( X1 != X2
| ~ reorganization_free(X1,X3,X4)
| reorganization_free(X2,X3,X4) ) ).
cnf(i_0_105,axiom,
( X1 != X2
| ~ reorganization_free(X3,X1,X4)
| reorganization_free(X3,X2,X4) ) ).
cnf(i_0_106,axiom,
( X1 != X2
| ~ reorganization_free(X3,X4,X1)
| reorganization_free(X3,X4,X2) ) ).
cnf(i_0_66_001,axiom,
X1 = X1 ).
cnf(i_0_67_002,axiom,
( X1 = X2
| X2 != X1 ) ).
cnf(i_0_68_003,axiom,
( X1 = X2
| X1 != X3
| X3 != X2 ) ).
cnf(i_0_69_004,axiom,
( X1 != X2
| esk4_8(X1,X3,X4,X5,X6,X7,X8,X9) = esk4_8(X2,X3,X4,X5,X6,X7,X8,X9) ) ).
cnf(i_0_70_005,axiom,
( X1 != X2
| esk4_8(X3,X1,X4,X5,X6,X7,X8,X9) = esk4_8(X3,X2,X4,X5,X6,X7,X8,X9) ) ).
cnf(i_0_71_006,axiom,
( X1 != X2
| esk4_8(X3,X4,X1,X5,X6,X7,X8,X9) = esk4_8(X3,X4,X2,X5,X6,X7,X8,X9) ) ).
cnf(i_0_72_007,axiom,
( X1 != X2
| esk4_8(X3,X4,X5,X1,X6,X7,X8,X9) = esk4_8(X3,X4,X5,X2,X6,X7,X8,X9) ) ).
cnf(i_0_73_008,axiom,
( X1 != X2
| esk4_8(X3,X4,X5,X6,X1,X7,X8,X9) = esk4_8(X3,X4,X5,X6,X2,X7,X8,X9) ) ).
cnf(i_0_74_009,axiom,
( X1 != X2
| esk4_8(X3,X4,X5,X6,X7,X1,X8,X9) = esk4_8(X3,X4,X5,X6,X7,X2,X8,X9) ) ).
cnf(i_0_75_010,axiom,
( X1 != X2
| esk4_8(X3,X4,X5,X6,X7,X8,X1,X9) = esk4_8(X3,X4,X5,X6,X7,X8,X2,X9) ) ).
cnf(i_0_76_011,axiom,
( X1 != X2
| esk4_8(X3,X4,X5,X6,X7,X8,X9,X1) = esk4_8(X3,X4,X5,X6,X7,X8,X9,X2) ) ).
cnf(i_0_77_012,axiom,
( X1 != X2
| esk3_8(X1,X3,X4,X5,X6,X7,X8,X9) = esk3_8(X2,X3,X4,X5,X6,X7,X8,X9) ) ).
cnf(i_0_78_013,axiom,
( X1 != X2
| esk3_8(X3,X1,X4,X5,X6,X7,X8,X9) = esk3_8(X3,X2,X4,X5,X6,X7,X8,X9) ) ).
cnf(i_0_79_014,axiom,
( X1 != X2
| esk3_8(X3,X4,X1,X5,X6,X7,X8,X9) = esk3_8(X3,X4,X2,X5,X6,X7,X8,X9) ) ).
cnf(i_0_80_015,axiom,
( X1 != X2
| esk3_8(X3,X4,X5,X1,X6,X7,X8,X9) = esk3_8(X3,X4,X5,X2,X6,X7,X8,X9) ) ).
cnf(i_0_81_016,axiom,
( X1 != X2
| esk3_8(X3,X4,X5,X6,X1,X7,X8,X9) = esk3_8(X3,X4,X5,X6,X2,X7,X8,X9) ) ).
cnf(i_0_82_017,axiom,
( X1 != X2
| esk3_8(X3,X4,X5,X6,X7,X1,X8,X9) = esk3_8(X3,X4,X5,X6,X7,X2,X8,X9) ) ).
cnf(i_0_83_018,axiom,
( X1 != X2
| esk3_8(X3,X4,X5,X6,X7,X8,X1,X9) = esk3_8(X3,X4,X5,X6,X7,X8,X2,X9) ) ).
cnf(i_0_84_019,axiom,
( X1 != X2
| esk3_8(X3,X4,X5,X6,X7,X8,X9,X1) = esk3_8(X3,X4,X5,X6,X7,X8,X9,X2) ) ).
cnf(i_0_85_020,axiom,
( X1 != X2
| ~ survival_chance(X1,X3,X4)
| survival_chance(X2,X3,X4) ) ).
cnf(i_0_86_021,axiom,
( X1 != X2
| ~ survival_chance(X3,X1,X4)
| survival_chance(X3,X2,X4) ) ).
cnf(i_0_87_022,axiom,
( X1 != X2
| ~ survival_chance(X3,X4,X1)
| survival_chance(X3,X4,X2) ) ).
cnf(i_0_88_023,axiom,
( X1 != X2
| ~ greater(X1,X3)
| greater(X2,X3) ) ).
cnf(i_0_89_024,axiom,
( X1 != X2
| ~ greater(X3,X1)
| greater(X3,X2) ) ).
cnf(i_0_90_025,axiom,
( X1 != X2
| ~ organization(X1,X3)
| organization(X2,X3) ) ).
cnf(i_0_91_026,axiom,
( X1 != X2
| ~ organization(X3,X1)
| organization(X3,X2) ) ).
cnf(i_0_92_027,axiom,
( X1 != X2
| ~ class(X1,X3,X4)
| class(X2,X3,X4) ) ).
cnf(i_0_93_028,axiom,
( X1 != X2
| ~ class(X3,X1,X4)
| class(X3,X2,X4) ) ).
cnf(i_0_94_029,axiom,
( X1 != X2
| ~ class(X3,X4,X1)
| class(X3,X4,X2) ) ).
cnf(i_0_95_030,axiom,
( X1 != X2
| ~ reorganization(X1,X3,X4)
| reorganization(X2,X3,X4) ) ).
cnf(i_0_96_031,axiom,
( X1 != X2
| ~ reorganization(X3,X1,X4)
| reorganization(X3,X2,X4) ) ).
cnf(i_0_97_032,axiom,
( X1 != X2
| ~ reorganization(X3,X4,X1)
| reorganization(X3,X4,X2) ) ).
cnf(i_0_98_033,axiom,
( X1 != X2
| ~ reorganization_type(X1,X3,X4)
| reorganization_type(X2,X3,X4) ) ).
cnf(i_0_99_034,axiom,
( X1 != X2
| ~ reorganization_type(X3,X1,X4)
| reorganization_type(X3,X2,X4) ) ).
cnf(i_0_100_035,axiom,
( X1 != X2
| ~ reorganization_type(X3,X4,X1)
| reorganization_type(X3,X4,X2) ) ).
cnf(i_0_101_036,axiom,
( X1 != X2
| ~ complexity(X1,X3,X4)
| complexity(X2,X3,X4) ) ).
cnf(i_0_102_037,axiom,
( X1 != X2
| ~ complexity(X3,X1,X4)
| complexity(X3,X2,X4) ) ).
cnf(i_0_103_038,axiom,
( X1 != X2
| ~ complexity(X3,X4,X1)
| complexity(X3,X4,X2) ) ).
cnf(i_0_104_039,axiom,
( X1 != X2
| ~ reorganization_free(X1,X3,X4)
| reorganization_free(X2,X3,X4) ) ).
cnf(i_0_105_040,axiom,
( X1 != X2
| ~ reorganization_free(X3,X1,X4)
| reorganization_free(X3,X2,X4) ) ).
cnf(i_0_106_041,axiom,
( X1 != X2
| ~ reorganization_free(X3,X4,X1)
| reorganization_free(X3,X4,X2) ) ).
cnf(i_0_107,plain,
~ greater(X1,X1),
inference(equality_inference,[],[56]) ).
cnf(i_0_108,plain,
esk14_0 != esk17_0,
inference(scs_inference,[],[i_0_57,i_0_58]) ).
cnf(i_0_109,plain,
~ reorganization(X1,esk11_0,esk10_0),
inference(scs_inference,[],[i_0_57,i_0_40]) ).
cnf(i_0_110,plain,
( greater(X1,X2)
| ~ reorganization(X3,X2,X1) ),
inference(rename_variables,[],[i_0_40]) ).
cnf(i_0_111,plain,
~ greater(esk12_0,esk13_0),
inference(scs_inference,[],[i_0_57,i_0_63,i_0_40,i_0_55]) ).
cnf(i_0_112,plain,
( ~ greater(X1,X2)
| ~ greater(X2,X1) ),
inference(rename_variables,[],[i_0_55]) ).
cnf(i_0_113,plain,
~ greater(esk14_0,esk16_0),
inference(scs_inference,[],[i_0_57,i_0_63,i_0_65,i_0_40,i_0_55,i_0_56]) ).
cnf(i_0_114,plain,
( X1 != X2
| ~ greater(X1,X2) ),
inference(rename_variables,[],[i_0_56]) ).
cnf(i_0_115,plain,
esk16_0 = esk14_0,
inference(scs_inference,[],[i_0_57,i_0_63,i_0_65,i_0_40,i_0_55,i_0_56,i_0_67]) ).
cnf(i_0_116,plain,
~ greater(esk16_0,esk14_0),
inference(scs_inference,[],[i_0_57,i_0_63,i_0_65,i_0_107,i_0_40,i_0_55,i_0_56,i_0_67,i_0_89]) ).
cnf(i_0_117,plain,
~ greater(X1,X1),
inference(rename_variables,[],[i_0_107]) ).
cnf(i_0_118,plain,
greater(esk11_0,esk10_0),
inference(scs_inference,[],[i_0_51,i_0_53,i_0_57,i_0_63,i_0_64,i_0_65,i_0_107,i_0_40,i_0_55,i_0_56,i_0_67,i_0_89,i_0_37]) ).
cnf(i_0_119,plain,
( X1 = X2
| greater(X2,X1)
| greater(X1,X2)
| ~ survival_chance(X3,X1,X4)
| ~ survival_chance(X5,X2,X4) ),
inference(rename_variables,[],[i_0_37]) ).
cnf(i_0_120,plain,
~ complexity(esk6_0,esk12_0,esk15_0),
inference(scs_inference,[],[i_0_42,i_0_44,i_0_46,i_0_49,i_0_51,i_0_53,i_0_57,i_0_59,i_0_60,i_0_63,i_0_64,i_0_65,i_0_107,i_0_117,i_0_40,i_0_55,i_0_56,i_0_67,i_0_89,i_0_37,i_0_34]) ).
cnf(i_0_121,plain,
~ greater(X1,X1),
inference(rename_variables,[],[i_0_107]) ).
cnf(i_0_122,plain,
( ~ organization(X1,X2)
| ~ class(X1,X3,X4)
| ~ reorganization(X5,X4,X6)
| ~ reorganization(X1,X4,X2)
| ~ reorganization_type(X1,X7,X4)
| ~ greater(X8,X9)
| greater(X2,X6)
| ~ organization(X5,X4)
| ~ class(X5,X3,X4)
| ~ reorganization_type(X5,X7,X4)
| ~ organization(X1,X4)
| ~ complexity(X5,X9,X4)
| ~ complexity(X1,X8,X4) ),
inference(rename_variables,[],[i_0_34]) ).
cnf(i_0_123,plain,
esk5_0 != esk6_0,
inference(scs_inference,[],[i_0_42,i_0_43,i_0_44,i_0_46,i_0_49,i_0_51,i_0_53,i_0_57,i_0_59,i_0_60,i_0_63,i_0_64,i_0_65,i_0_107,i_0_117,i_0_40,i_0_55,i_0_56,i_0_67,i_0_89,i_0_37,i_0_34,i_0_101]) ).
cnf(i_0_124,plain,
( X1 != esk10_0
| ~ greater(X1,esk11_0) ),
inference(scs_inference,[],[i_0_42,i_0_43,i_0_44,i_0_46,i_0_49,i_0_51,i_0_53,i_0_57,i_0_59,i_0_60,i_0_63,i_0_64,i_0_65,i_0_107,i_0_117,i_0_40,i_0_55,i_0_56,i_0_67,i_0_89,i_0_37,i_0_34,i_0_101,i_0_88]) ).
cnf(i_0_125,plain,
esk13_0 != esk12_0,
inference(scs_inference,[],[i_0_42,i_0_43,i_0_44,i_0_46,i_0_49,i_0_51,i_0_53,i_0_57,i_0_59,i_0_60,i_0_63,i_0_64,i_0_65,i_0_107,i_0_117,i_0_40,i_0_55,i_0_56,i_0_67,i_0_89,i_0_37,i_0_34,i_0_101,i_0_88,i_0_102]) ).
cnf(i_0_126,plain,
( X1 != esk11_0
| ~ reorganization(X2,X1,esk10_0) ),
inference(scs_inference,[],[i_0_42,i_0_43,i_0_44,i_0_46,i_0_49,i_0_51,i_0_53,i_0_57,i_0_59,i_0_60,i_0_63,i_0_64,i_0_65,i_0_107,i_0_117,i_0_40,i_0_55,i_0_56,i_0_67,i_0_89,i_0_37,i_0_34,i_0_101,i_0_88,i_0_102,i_0_96]) ).
cnf(i_0_127,plain,
( X1 != esk10_0
| ~ reorganization(X2,esk11_0,X1) ),
inference(scs_inference,[],[i_0_42,i_0_43,i_0_44,i_0_46,i_0_49,i_0_51,i_0_53,i_0_57,i_0_59,i_0_60,i_0_63,i_0_64,i_0_65,i_0_107,i_0_117,i_0_40,i_0_55,i_0_56,i_0_67,i_0_89,i_0_37,i_0_34,i_0_101,i_0_88,i_0_102,i_0_96,i_0_97]) ).
cnf(i_0_128,plain,
( X1 != esk15_0
| ~ complexity(esk6_0,esk12_0,X1) ),
inference(scs_inference,[],[i_0_42,i_0_43,i_0_44,i_0_46,i_0_49,i_0_51,i_0_53,i_0_57,i_0_59,i_0_60,i_0_63,i_0_64,i_0_65,i_0_107,i_0_117,i_0_40,i_0_55,i_0_56,i_0_67,i_0_89,i_0_37,i_0_34,i_0_101,i_0_88,i_0_102,i_0_96,i_0_97,i_0_103]) ).
cnf(i_0_129,plain,
( ~ greater(X1,X2)
| ~ greater(X3,X1)
| organization(X4,X1)
| ~ organization(X4,X2)
| ~ organization(X4,X3) ),
inference(rename_variables,[],[i_0_38]) ).
cnf(i_0_130,plain,
( ~ greater(esk17_0,esk13_0)
| organization(esk6_0,esk13_0)
| ~ organization(esk6_0,esk12_0) ),
inference(scs_inference,[],[i_0_42,i_0_43,i_0_44,i_0_46,i_0_49,i_0_51,i_0_53,i_0_57,i_0_59,i_0_60,i_0_63,i_0_64,i_0_65,i_0_107,i_0_117,i_0_40,i_0_55,i_0_56,i_0_67,i_0_89,i_0_37,i_0_34,i_0_101,i_0_102,i_0_38]) ).
cnf(i_0_131,plain,
~ greater(esk10_0,esk11_0),
inference(equality_inference,[],[124]) ).
cnf(i_0_132,plain,
~ reorganization(X1,esk11_0,esk10_0),
inference(equality_inference,[],[126]) ).
cnf(i_0_133,plain,
~ reorganization(X1,esk11_0,esk10_0),
inference(equality_inference,[],[127]) ).
cnf(i_0_134,plain,
~ complexity(esk6_0,esk12_0,esk15_0),
inference(equality_inference,[],[128]) ).
cnf(i_0_135,plain,
~ reorganization(X1,esk13_0,esk12_0),
inference(scs_inference,[],[i_0_111,i_0_40]) ).
cnf(i_0_136,plain,
( greater(X1,X2)
| ~ reorganization(X3,X2,X1) ),
inference(rename_variables,[],[i_0_40]) ).
cnf(i_0_137,plain,
greater(esk17_0,esk16_0),
inference(scs_inference,[],[i_0_42,i_0_63,i_0_45,i_0_47,i_0_50,i_0_62,i_0_43,i_0_44,i_0_60,i_0_46,i_0_49,i_0_59,i_0_111,i_0_40,i_0_34]) ).
cnf(i_0_138,plain,
( ~ organization(X1,X2)
| ~ class(X1,X3,X4)
| ~ reorganization(X5,X4,X6)
| ~ reorganization(X1,X4,X2)
| ~ reorganization_type(X1,X7,X4)
| ~ greater(X8,X9)
| greater(X2,X6)
| ~ organization(X5,X4)
| ~ class(X5,X3,X4)
| ~ reorganization_type(X5,X7,X4)
| ~ organization(X1,X4)
| ~ complexity(X5,X9,X4)
| ~ complexity(X1,X8,X4) ),
inference(rename_variables,[],[i_0_34]) ).
cnf(i_0_139,plain,
~ greater(esk16_0,esk17_0),
inference(scs_inference,[],[i_0_42,i_0_63,i_0_45,i_0_47,i_0_50,i_0_62,i_0_43,i_0_44,i_0_60,i_0_46,i_0_49,i_0_59,i_0_111,i_0_40,i_0_34,i_0_55]) ).
cnf(i_0_140,plain,
( ~ greater(X1,X2)
| ~ greater(X2,X1) ),
inference(rename_variables,[],[i_0_55]) ).
cnf(i_0_141,plain,
~ greater(esk14_0,esk17_0),
inference(scs_inference,[],[i_0_42,i_0_63,i_0_45,i_0_47,i_0_50,i_0_62,i_0_43,i_0_44,i_0_60,i_0_46,i_0_49,i_0_59,i_0_111,i_0_113,i_0_40,i_0_34,i_0_55,i_0_41]) ).
cnf(i_0_142,plain,
( ~ greater(X1,X2)
| greater(X3,X2)
| ~ greater(X3,X1) ),
inference(rename_variables,[],[i_0_41]) ).
cnf(i_0_143,plain,
( X1 != esk11_0
| ~ greater(esk10_0,X1) ),
inference(scs_inference,[],[i_0_42,i_0_63,i_0_45,i_0_47,i_0_50,i_0_62,i_0_43,i_0_44,i_0_60,i_0_46,i_0_49,i_0_59,i_0_57,i_0_111,i_0_113,i_0_40,i_0_34,i_0_55,i_0_41,i_0_89]) ).
cnf(i_0_144,plain,
~ greater(X1,X1),
inference(rename_variables,[],[i_0_107]) ).
cnf(i_0_145,plain,
~ greater(X1,X1),
inference(rename_variables,[],[i_0_107]) ).
cnf(i_0_146,plain,
( X1 = X2
| greater(X2,X1)
| greater(X1,X2)
| ~ survival_chance(X3,X1,X4)
| ~ survival_chance(X5,X2,X4) ),
inference(rename_variables,[],[i_0_37]) ).
cnf(i_0_147,plain,
~ greater(X1,X1),
inference(rename_variables,[],[i_0_107]) ).
cnf(i_0_148,plain,
~ greater(X1,X1),
inference(rename_variables,[],[i_0_107]) ).
cnf(i_0_150,plain,
~ greater(esk10_0,esk11_0),
inference(equality_inference,[],[143]) ).
cnf(i_0_151,plain,
~ reorganization(X1,esk14_0,esk16_0),
inference(scs_inference,[],[i_0_116,i_0_40]) ).
cnf(i_0_152,plain,
( greater(X1,X2)
| ~ reorganization(X3,X2,X1) ),
inference(rename_variables,[],[i_0_40]) ).
cnf(i_0_153,plain,
~ reorganization(X1,esk16_0,esk16_0),
inference(scs_inference,[],[i_0_115,i_0_116,i_0_40,i_0_96]) ).
cnf(i_0_154,plain,
~ reorganization(X1,esk14_0,esk14_0),
inference(scs_inference,[],[i_0_65,i_0_115,i_0_116,i_0_40,i_0_96,i_0_97]) ).
cnf(i_0_155,plain,
( X1 != esk17_0
| ~ greater(esk16_0,X1) ),
inference(scs_inference,[],[i_0_65,i_0_115,i_0_116,i_0_139,i_0_40,i_0_96,i_0_97,i_0_89]) ).
cnf(i_0_156,plain,
( X1 != esk12_0
| ~ greater(X1,esk13_0) ),
inference(scs_inference,[],[i_0_65,i_0_115,i_0_116,i_0_139,i_0_111,i_0_40,i_0_96,i_0_97,i_0_89,i_0_88]) ).
cnf(i_0_157,plain,
( ~ greater(X1,X2)
| ~ greater(X3,X1)
| organization(X4,X1)
| ~ organization(X4,X2)
| ~ organization(X4,X3) ),
inference(rename_variables,[],[i_0_38]) ).
cnf(i_0_158,plain,
( greater(esk17_0,esk14_0)
| ~ survival_chance(X1,esk14_0,X2)
| ~ survival_chance(X3,esk17_0,X2) ),
inference(scs_inference,[],[i_0_65,i_0_63,i_0_61,i_0_108,i_0_115,i_0_116,i_0_139,i_0_141,i_0_111,i_0_40,i_0_96,i_0_97,i_0_37]) ).
cnf(i_0_159,plain,
~ greater(esk16_0,esk17_0),
inference(equality_inference,[],[155]) ).
cnf(i_0_160,plain,
~ greater(esk12_0,esk13_0),
inference(equality_inference,[],[156]) ).
cnf(i_0_161,plain,
~ reorganization(X1,esk16_0,esk14_0),
inference(scs_inference,[],[i_0_113,i_0_40]) ).
cnf(i_0_162,plain,
( greater(X1,X2)
| ~ reorganization(X3,X2,X1) ),
inference(rename_variables,[],[i_0_40]) ).
cnf(i_0_163,plain,
( X1 != esk13_0
| ~ reorganization(X2,X1,esk12_0) ),
inference(scs_inference,[],[i_0_113,i_0_135,i_0_40,i_0_96]) ).
cnf(i_0_164,plain,
( esk16_0 != esk12_0
| esk15_0 != esk13_0 ),
inference(scs_inference,[],[i_0_50,i_0_113,i_0_135,i_0_40,i_0_96,i_0_97]) ).
cnf(i_0_165,plain,
~ reorganization(X1,esk13_0,esk12_0),
inference(rename_variables,[],[i_0_135]) ).
cnf(i_0_166,plain,
~ greater(X1,X1),
inference(rename_variables,[],[i_0_107]) ).
cnf(i_0_167,plain,
~ greater(X1,X1),
inference(rename_variables,[],[i_0_107]) ).
cnf(i_0_168,plain,
( X1 = X2
| greater(X2,X1)
| greater(X1,X2)
| ~ survival_chance(X3,X1,X4)
| ~ survival_chance(X5,X2,X4) ),
inference(rename_variables,[],[i_0_37]) ).
cnf(i_0_169,plain,
~ greater(X1,X1),
inference(rename_variables,[],[i_0_107]) ).
cnf(i_0_170,plain,
~ greater(X1,X1),
inference(rename_variables,[],[i_0_107]) ).
cnf(i_0_172,plain,
~ reorganization(X1,esk13_0,esk12_0),
inference(equality_inference,[],[163]) ).
cnf(i_0_173,plain,
~ reorganization(X1,X2,X2),
inference(scs_inference,[],[i_0_107,i_0_40]) ).
cnf(i_0_174,plain,
( greater(X1,X2)
| ~ reorganization(X3,X2,X1) ),
inference(rename_variables,[],[i_0_40]) ).
cnf(i_0_175,plain,
( X1 != esk12_0
| ~ reorganization(X2,esk13_0,X1) ),
inference(scs_inference,[],[i_0_107,i_0_135,i_0_40,i_0_97]) ).
cnf(i_0_176,plain,
( X1 != esk17_0
| ~ greater(esk14_0,X1) ),
inference(scs_inference,[],[i_0_107,i_0_141,i_0_135,i_0_40,i_0_97,i_0_89]) ).
cnf(i_0_177,plain,
( ~ greater(X1,X2)
| ~ greater(X3,X1)
| organization(X4,X1)
| ~ organization(X4,X2)
| ~ organization(X4,X3) ),
inference(rename_variables,[],[i_0_38]) ).
cnf(i_0_179,plain,
~ reorganization(X1,esk13_0,esk12_0),
inference(equality_inference,[],[175]) ).
cnf(i_0_180,plain,
~ greater(esk14_0,esk17_0),
inference(equality_inference,[],[176]) ).
cnf(i_0_181,plain,
~ reorganization(X1,esk17_0,esk16_0),
inference(scs_inference,[],[i_0_139,i_0_40]) ).
cnf(i_0_182,plain,
( greater(X1,X2)
| ~ reorganization(X3,X2,X1) ),
inference(rename_variables,[],[i_0_40]) ).
cnf(i_0_183,plain,
esk15_0 != esk17_0,
inference(scs_inference,[],[i_0_50,i_0_139,i_0_40,i_0_96]) ).
cnf(i_0_184,plain,
~ reorganization(esk5_0,esk17_0,esk14_0),
inference(scs_inference,[],[i_0_65,i_0_50,i_0_139,i_0_40,i_0_96,i_0_97]) ).
cnf(i_0_185,plain,
( X1 != esk5_0
| ~ reorganization(X1,esk17_0,esk14_0) ),
inference(scs_inference,[],[i_0_65,i_0_50,i_0_139,i_0_40,i_0_96,i_0_97,i_0_95]) ).
cnf(i_0_186,plain,
( X1 != esk13_0
| ~ greater(esk12_0,X1) ),
inference(scs_inference,[],[i_0_65,i_0_50,i_0_139,i_0_111,i_0_40,i_0_96,i_0_97,i_0_95,i_0_89]) ).
cnf(i_0_187,plain,
( ~ greater(X1,X2)
| ~ greater(X3,X1)
| organization(X4,X1)
| ~ organization(X4,X2)
| ~ organization(X4,X3) ),
inference(rename_variables,[],[i_0_38]) ).
cnf(i_0_189,plain,
~ reorganization(esk5_0,esk17_0,esk14_0),
inference(equality_inference,[],[185]) ).
cnf(i_0_190,plain,
~ greater(esk12_0,esk13_0),
inference(equality_inference,[],[186]) ).
cnf(i_0_191,plain,
~ reorganization(X1,esk17_0,esk14_0),
inference(scs_inference,[],[i_0_141,i_0_40]) ).
cnf(i_0_192,plain,
( greater(X1,X2)
| ~ reorganization(X3,X2,X1) ),
inference(rename_variables,[],[i_0_40]) ).
cnf(i_0_193,plain,
( X1 != esk17_0
| ~ reorganization(esk5_0,X1,esk14_0) ),
inference(scs_inference,[],[i_0_141,i_0_184,i_0_40,i_0_96]) ).
cnf(i_0_194,plain,
( ~ greater(X1,X2)
| ~ greater(X3,X1)
| organization(X4,X1)
| ~ organization(X4,X2)
| ~ organization(X4,X3) ),
inference(rename_variables,[],[i_0_38]) ).
cnf(i_0_196,plain,
~ reorganization(esk5_0,esk17_0,esk14_0),
inference(equality_inference,[],[193]) ).
cnf(i_0_197,plain,
( X1 != esk17_0
| ~ reorganization(X2,X1,esk14_0) ),
inference(scs_inference,[],[i_0_191,i_0_96]) ).
cnf(i_0_198,plain,
( ~ greater(X1,X2)
| ~ greater(X3,X1)
| organization(X4,X1)
| ~ organization(X4,X2)
| ~ organization(X4,X3) ),
inference(rename_variables,[],[i_0_38]) ).
cnf(i_0_200,plain,
~ reorganization(X1,esk17_0,esk14_0),
inference(equality_inference,[],[197]) ).
cnf(i_0_201,plain,
( ~ survival_chance(esk5_0,esk11_0,esk16_0)
| ~ survival_chance(esk5_0,esk10_0,esk17_0)
| ~ organization(esk5_0,esk16_0) ),
inference(scs_inference,[],[i_0_57,i_0_63,i_0_59,i_0_48,i_0_61,i_0_108,i_0_137,i_0_141,i_0_36]) ).
cnf(i_0_2545,plain,
( ~ survival_chance(esk5_0,X1,esk16_0)
| ~ survival_chance(esk5_0,X1,esk17_0)
| ~ organization(esk5_0,esk16_0) ),
inference(scs_inference,[],[i_0_107,i_0_60,i_0_63,i_0_48,i_0_108,i_0_61,i_0_137,i_0_141,i_0_36]) ).
cnf(i_0_2881,plain,
( ~ survival_chance(esk5_0,esk13_0,esk16_0)
| ~ survival_chance(esk5_0,esk12_0,esk17_0)
| ~ organization(esk5_0,esk16_0) ),
inference(scs_inference,[],[i_0_111,i_0_60,i_0_63,i_0_48,i_0_108,i_0_61,i_0_137,i_0_141,i_0_36]) ).
cnf(i_0_2993,plain,
( ~ survival_chance(esk5_0,esk16_0,esk16_0)
| ~ survival_chance(esk5_0,esk14_0,esk17_0)
| ~ organization(esk5_0,esk16_0) ),
inference(scs_inference,[],[i_0_113,i_0_60,i_0_63,i_0_48,i_0_108,i_0_61,i_0_137,i_0_141,i_0_36]) ).
cnf(i_0_3217,plain,
( ~ survival_chance(esk5_0,esk14_0,esk16_0)
| ~ survival_chance(esk5_0,esk16_0,esk17_0)
| ~ organization(esk5_0,esk16_0) ),
inference(scs_inference,[],[i_0_116,i_0_60,i_0_63,i_0_48,i_0_108,i_0_61,i_0_137,i_0_141,i_0_36]) ).
cnf(i_0_3329,plain,
( ~ complexity(esk6_0,esk10_0,esk15_0)
| ~ complexity(esk6_0,esk11_0,esk15_0) ),
inference(scs_inference,[],[i_0_118,i_0_60,i_0_59,i_0_44,i_0_46,i_0_49,i_0_107,i_0_34]) ).
cnf(i_0_3330,plain,
~ greater(X1,X1),
inference(rename_variables,[],[i_0_107]) ).
cnf(i_0_3331,plain,
( ~ organization(X1,X2)
| ~ class(X1,X3,X4)
| ~ reorganization(X5,X4,X6)
| ~ reorganization(X1,X4,X2)
| ~ reorganization_type(X1,X7,X4)
| ~ greater(X8,X9)
| greater(X2,X6)
| ~ organization(X5,X4)
| ~ class(X5,X3,X4)
| ~ reorganization_type(X5,X7,X4)
| ~ organization(X1,X4)
| ~ complexity(X5,X9,X4)
| ~ complexity(X1,X8,X4) ),
inference(rename_variables,[],[i_0_34]) ).
cnf(i_0_3332,plain,
( esk13_0 != esk10_0
| ~ complexity(esk6_0,esk11_0,esk15_0) ),
inference(scs_inference,[],[i_0_118,i_0_60,i_0_59,i_0_44,i_0_46,i_0_42,i_0_49,i_0_107,i_0_34,i_0_102]) ).
cnf(i_0_3557,plain,
( greater(esk6_0,esk5_0)
| greater(esk5_0,esk6_0)
| ~ survival_chance(X1,esk5_0,X2)
| ~ survival_chance(X3,esk6_0,X2) ),
inference(scs_inference,[],[i_0_123,i_0_60,i_0_63,i_0_37]) ).
cnf(i_0_4005,plain,
( ~ survival_chance(esk5_0,esk17_0,esk16_0)
| ~ survival_chance(esk5_0,esk16_0,esk17_0)
| ~ organization(esk5_0,esk16_0) ),
inference(scs_inference,[],[i_0_139,i_0_60,i_0_63,i_0_108,i_0_48,i_0_61,i_0_137,i_0_141,i_0_36]) ).
cnf(i_0_4117,plain,
( ~ survival_chance(esk5_0,esk17_0,esk16_0)
| ~ survival_chance(esk5_0,esk14_0,esk17_0)
| ~ organization(esk5_0,esk16_0) ),
inference(scs_inference,[],[i_0_141,i_0_60,i_0_63,i_0_108,i_0_48,i_0_61,i_0_137,i_0_36]) ).
cnf(i_0_4677,plain,
( greater(esk17_0,esk15_0)
| greater(esk15_0,esk17_0)
| ~ survival_chance(X1,esk15_0,X2)
| ~ survival_chance(X3,esk17_0,X2) ),
inference(scs_inference,[],[i_0_183,i_0_60,i_0_63,i_0_37]) ).
cnf(i_0_4683,plain,
esk4_8(esk16_0,X1,X2,X3,X4,X5,X6,X7) = esk4_8(esk14_0,X1,X2,X3,X4,X5,X6,X7),
inference(scs_inference,[],[i_0_115,i_0_69]) ).
cnf(i_0_4684,plain,
esk4_8(X1,esk16_0,X2,X3,X4,X5,X6,X7) = esk4_8(X1,esk14_0,X2,X3,X4,X5,X6,X7),
inference(scs_inference,[],[i_0_115,i_0_69,i_0_70]) ).
cnf(i_0_4685,plain,
esk4_8(X1,X2,esk16_0,X3,X4,X5,X6,X7) = esk4_8(X1,X2,esk14_0,X3,X4,X5,X6,X7),
inference(scs_inference,[],[i_0_115,i_0_69,i_0_70,i_0_71]) ).
cnf(i_0_4686,plain,
esk4_8(X1,X2,X3,esk16_0,X4,X5,X6,X7) = esk4_8(X1,X2,X3,esk14_0,X4,X5,X6,X7),
inference(scs_inference,[],[i_0_115,i_0_69,i_0_70,i_0_71,i_0_72]) ).
cnf(i_0_4687,plain,
esk4_8(X1,X2,X3,X4,esk16_0,X5,X6,X7) = esk4_8(X1,X2,X3,X4,esk14_0,X5,X6,X7),
inference(scs_inference,[],[i_0_115,i_0_69,i_0_70,i_0_71,i_0_72,i_0_73]) ).
cnf(i_0_4688,plain,
esk4_8(X1,X2,X3,X4,X5,esk16_0,X6,X7) = esk4_8(X1,X2,X3,X4,X5,esk14_0,X6,X7),
inference(scs_inference,[],[i_0_115,i_0_69,i_0_70,i_0_71,i_0_72,i_0_73,i_0_74]) ).
cnf(i_0_4689,plain,
esk4_8(X1,X2,X3,X4,X5,X6,esk16_0,X7) = esk4_8(X1,X2,X3,X4,X5,X6,esk14_0,X7),
inference(scs_inference,[],[i_0_115,i_0_69,i_0_70,i_0_71,i_0_72,i_0_73,i_0_74,i_0_75]) ).
cnf(i_0_4690,plain,
esk4_8(X1,X2,X3,X4,X5,X6,X7,esk16_0) = esk4_8(X1,X2,X3,X4,X5,X6,X7,esk14_0),
inference(scs_inference,[],[i_0_115,i_0_69,i_0_70,i_0_71,i_0_72,i_0_73,i_0_74,i_0_75,i_0_76]) ).
cnf(i_0_4691,plain,
esk3_8(esk16_0,X1,X2,X3,X4,X5,X6,X7) = esk3_8(esk14_0,X1,X2,X3,X4,X5,X6,X7),
inference(scs_inference,[],[i_0_115,i_0_69,i_0_70,i_0_71,i_0_72,i_0_73,i_0_74,i_0_75,i_0_76,i_0_77]) ).
cnf(i_0_4692,plain,
esk3_8(X1,esk16_0,X2,X3,X4,X5,X6,X7) = esk3_8(X1,esk14_0,X2,X3,X4,X5,X6,X7),
inference(scs_inference,[],[i_0_115,i_0_69,i_0_70,i_0_71,i_0_72,i_0_73,i_0_74,i_0_75,i_0_76,i_0_77,i_0_78]) ).
cnf(i_0_4693,plain,
esk3_8(X1,X2,esk16_0,X3,X4,X5,X6,X7) = esk3_8(X1,X2,esk14_0,X3,X4,X5,X6,X7),
inference(scs_inference,[],[i_0_115,i_0_69,i_0_70,i_0_71,i_0_72,i_0_73,i_0_74,i_0_75,i_0_76,i_0_77,i_0_78,i_0_79]) ).
cnf(i_0_4694,plain,
esk3_8(X1,X2,X3,esk16_0,X4,X5,X6,X7) = esk3_8(X1,X2,X3,esk14_0,X4,X5,X6,X7),
inference(scs_inference,[],[i_0_115,i_0_69,i_0_70,i_0_71,i_0_72,i_0_73,i_0_74,i_0_75,i_0_76,i_0_77,i_0_78,i_0_79,i_0_80]) ).
cnf(i_0_4695,plain,
esk3_8(X1,X2,X3,X4,esk16_0,X5,X6,X7) = esk3_8(X1,X2,X3,X4,esk14_0,X5,X6,X7),
inference(scs_inference,[],[i_0_115,i_0_69,i_0_70,i_0_71,i_0_72,i_0_73,i_0_74,i_0_75,i_0_76,i_0_77,i_0_78,i_0_79,i_0_80,i_0_81]) ).
cnf(i_0_4696,plain,
esk3_8(X1,X2,X3,X4,X5,esk16_0,X6,X7) = esk3_8(X1,X2,X3,X4,X5,esk14_0,X6,X7),
inference(scs_inference,[],[i_0_115,i_0_69,i_0_70,i_0_71,i_0_72,i_0_73,i_0_74,i_0_75,i_0_76,i_0_77,i_0_78,i_0_79,i_0_80,i_0_81,i_0_82]) ).
cnf(i_0_4697,plain,
esk3_8(X1,X2,X3,X4,X5,X6,esk16_0,X7) = esk3_8(X1,X2,X3,X4,X5,X6,esk14_0,X7),
inference(scs_inference,[],[i_0_115,i_0_69,i_0_70,i_0_71,i_0_72,i_0_73,i_0_74,i_0_75,i_0_76,i_0_77,i_0_78,i_0_79,i_0_80,i_0_81,i_0_82,i_0_83]) ).
cnf(i_0_4698,plain,
esk3_8(X1,X2,X3,X4,X5,X6,X7,esk16_0) = esk3_8(X1,X2,X3,X4,X5,X6,X7,esk14_0),
inference(scs_inference,[],[i_0_115,i_0_69,i_0_70,i_0_71,i_0_72,i_0_73,i_0_74,i_0_75,i_0_76,i_0_77,i_0_78,i_0_79,i_0_80,i_0_81,i_0_82,i_0_83,i_0_84]) ).
cnf(i_0_4699,plain,
survival_chance(esk6_0,esk1_2(esk6_0,esk15_0),esk15_0),
inference(scs_inference,[],[i_0_115,i_0_60,i_0_69,i_0_70,i_0_71,i_0_72,i_0_73,i_0_74,i_0_75,i_0_76,i_0_77,i_0_78,i_0_79,i_0_80,i_0_81,i_0_82,i_0_83,i_0_84,i_0_39]) ).
cnf(i_0_4700,plain,
( ~ organization(X1,X2)
| survival_chance(X1,esk1_2(X1,X2),X2) ),
inference(rename_variables,[],[i_0_39]) ).
cnf(i_0_4701,plain,
esk11_0 != esk10_0,
inference(scs_inference,[],[i_0_115,i_0_60,i_0_118,i_0_69,i_0_70,i_0_71,i_0_72,i_0_73,i_0_74,i_0_75,i_0_76,i_0_77,i_0_78,i_0_79,i_0_80,i_0_81,i_0_82,i_0_83,i_0_84,i_0_39,i_0_56]) ).
cnf(i_0_4702,plain,
( ~ greater(X1,X2)
| X1 != X2 ),
inference(rename_variables,[],[i_0_56]) ).
cnf(i_0_4703,plain,
esk17_0 != esk15_0,
inference(scs_inference,[],[i_0_115,i_0_183,i_0_60,i_0_118,i_0_69,i_0_70,i_0_71,i_0_72,i_0_73,i_0_74,i_0_75,i_0_76,i_0_77,i_0_78,i_0_79,i_0_80,i_0_81,i_0_82,i_0_83,i_0_84,i_0_39,i_0_56,i_0_67]) ).
cnf(i_0_4704,plain,
greater(esk16_0,esk15_0),
inference(scs_inference,[],[i_0_115,i_0_50,i_0_183,i_0_60,i_0_118,i_0_69,i_0_70,i_0_71,i_0_72,i_0_73,i_0_74,i_0_75,i_0_76,i_0_77,i_0_78,i_0_79,i_0_80,i_0_81,i_0_82,i_0_83,i_0_84,i_0_39,i_0_56,i_0_67,i_0_40]) ).
cnf(i_0_4705,plain,
( ~ reorganization(X1,X2,X3)
| greater(X3,X2) ),
inference(rename_variables,[],[i_0_40]) ).
cnf(i_0_4706,plain,
esk16_0 != esk17_0,
inference(scs_inference,[],[i_0_115,i_0_50,i_0_65,i_0_183,i_0_60,i_0_118,i_0_108,i_0_69,i_0_70,i_0_71,i_0_72,i_0_73,i_0_74,i_0_75,i_0_76,i_0_77,i_0_78,i_0_79,i_0_80,i_0_81,i_0_82,i_0_83,i_0_84,i_0_39,i_0_56,i_0_67,i_0_40,i_0_68]) ).
cnf(i_0_4707,plain,
survival_chance(esk5_0,esk10_0,esk16_0),
inference(scs_inference,[],[i_0_53,i_0_115,i_0_50,i_0_65,i_0_183,i_0_60,i_0_118,i_0_108,i_0_69,i_0_70,i_0_71,i_0_72,i_0_73,i_0_74,i_0_75,i_0_76,i_0_77,i_0_78,i_0_79,i_0_80,i_0_81,i_0_82,i_0_83,i_0_84,i_0_39,i_0_56,i_0_67,i_0_40,i_0_68,i_0_87]) ).
cnf(i_0_4708,plain,
reorganization_free(esk5_0,esk14_0,esk17_0),
inference(scs_inference,[],[i_0_53,i_0_115,i_0_50,i_0_65,i_0_183,i_0_60,i_0_118,i_0_108,i_0_48,i_0_69,i_0_70,i_0_71,i_0_72,i_0_73,i_0_74,i_0_75,i_0_76,i_0_77,i_0_78,i_0_79,i_0_80,i_0_81,i_0_82,i_0_83,i_0_84,i_0_39,i_0_56,i_0_67,i_0_40,i_0_68,i_0_87,i_0_105]) ).
cnf(i_0_4709,plain,
~ greater(esk15_0,esk14_0),
inference(scs_inference,[],[i_0_53,i_0_115,i_0_50,i_0_65,i_0_183,i_0_60,i_0_118,i_0_116,i_0_108,i_0_48,i_0_69,i_0_70,i_0_71,i_0_72,i_0_73,i_0_74,i_0_75,i_0_76,i_0_77,i_0_78,i_0_79,i_0_80,i_0_81,i_0_82,i_0_83,i_0_84,i_0_39,i_0_56,i_0_67,i_0_40,i_0_68,i_0_87,i_0_105,i_0_41]) ).
cnf(i_0_4710,plain,
( greater(X1,X2)
| ~ greater(X1,X3)
| ~ greater(X3,X2) ),
inference(rename_variables,[],[i_0_41]) ).
cnf(i_0_4711,plain,
greater(esk14_0,esk15_0),
inference(scs_inference,[],[i_0_53,i_0_115,i_0_50,i_0_65,i_0_183,i_0_60,i_0_118,i_0_116,i_0_108,i_0_48,i_0_69,i_0_70,i_0_71,i_0_72,i_0_73,i_0_74,i_0_75,i_0_76,i_0_77,i_0_78,i_0_79,i_0_80,i_0_81,i_0_82,i_0_83,i_0_84,i_0_39,i_0_56,i_0_67,i_0_40,i_0_68,i_0_87,i_0_105,i_0_41,i_0_88]) ).
cnf(i_0_4712,plain,
reorganization(esk5_0,esk15_0,esk14_0),
inference(scs_inference,[],[i_0_53,i_0_115,i_0_50,i_0_65,i_0_183,i_0_60,i_0_118,i_0_116,i_0_108,i_0_48,i_0_69,i_0_70,i_0_71,i_0_72,i_0_73,i_0_74,i_0_75,i_0_76,i_0_77,i_0_78,i_0_79,i_0_80,i_0_81,i_0_82,i_0_83,i_0_84,i_0_39,i_0_56,i_0_67,i_0_40,i_0_68,i_0_87,i_0_105,i_0_41,i_0_88,i_0_97]) ).
cnf(i_0_4713,plain,
~ reorganization(X1,esk4_8(esk16_0,X2,X3,X4,X5,X6,X7,X8),esk4_8(esk14_0,X2,X3,X4,X5,X6,X7,X8)),
inference(scs_inference,[],[i_0_173,i_0_53,i_0_115,i_0_50,i_0_65,i_0_183,i_0_60,i_0_118,i_0_116,i_0_108,i_0_48,i_0_69,i_0_70,i_0_71,i_0_72,i_0_73,i_0_74,i_0_75,i_0_76,i_0_77,i_0_78,i_0_79,i_0_80,i_0_81,i_0_82,i_0_83,i_0_84,i_0_39,i_0_56,i_0_67,i_0_40,i_0_68,i_0_87,i_0_105,i_0_41,i_0_88,i_0_97,i_0_96]) ).
cnf(i_0_4714,plain,
~ reorganization(X1,X2,X2),
inference(rename_variables,[],[i_0_173]) ).
cnf(i_0_4715,plain,
greater(esk17_0,esk14_0),
inference(scs_inference,[],[i_0_173,i_0_53,i_0_115,i_0_50,i_0_65,i_0_183,i_0_60,i_0_118,i_0_116,i_0_108,i_0_48,i_0_137,i_0_69,i_0_70,i_0_71,i_0_72,i_0_73,i_0_74,i_0_75,i_0_76,i_0_77,i_0_78,i_0_79,i_0_80,i_0_81,i_0_82,i_0_83,i_0_84,i_0_39,i_0_56,i_0_67,i_0_40,i_0_68,i_0_87,i_0_105,i_0_41,i_0_88,i_0_97,i_0_96,i_0_89]) ).
cnf(i_0_4716,plain,
organization(esk6_0,esk16_0),
inference(scs_inference,[],[i_0_173,i_0_53,i_0_115,i_0_50,i_0_65,i_0_183,i_0_60,i_0_118,i_0_116,i_0_59,i_0_108,i_0_48,i_0_137,i_0_69,i_0_70,i_0_71,i_0_72,i_0_73,i_0_74,i_0_75,i_0_76,i_0_77,i_0_78,i_0_79,i_0_80,i_0_81,i_0_82,i_0_83,i_0_84,i_0_39,i_0_56,i_0_67,i_0_40,i_0_68,i_0_87,i_0_105,i_0_41,i_0_88,i_0_97,i_0_96,i_0_89,i_0_38]) ).
cnf(i_0_4717,plain,
( ~ greater(X1,X2)
| organization(X3,X2)
| ~ organization(X3,X4)
| ~ organization(X3,X1)
| ~ greater(X2,X4) ),
inference(rename_variables,[],[i_0_38]) ).
cnf(i_0_4718,plain,
~ greater(esk15_0,esk16_0),
inference(scs_inference,[],[i_0_173,i_0_53,i_0_115,i_0_50,i_0_65,i_0_183,i_0_60,i_0_118,i_0_116,i_0_59,i_0_108,i_0_48,i_0_137,i_0_69,i_0_70,i_0_71,i_0_72,i_0_73,i_0_74,i_0_75,i_0_76,i_0_77,i_0_78,i_0_79,i_0_80,i_0_81,i_0_82,i_0_83,i_0_84,i_0_39,i_0_56,i_0_67,i_0_40,i_0_68,i_0_87,i_0_105,i_0_41,i_0_88,i_0_97,i_0_96,i_0_89,i_0_38,i_0_55]) ).
cnf(i_0_4719,plain,
( ~ greater(X1,X2)
| ~ greater(X2,X1) ),
inference(rename_variables,[],[i_0_55]) ).
cnf(i_0_4720,plain,
( survival_chance(X1,esk9_0,esk15_0)
| esk6_0 != X1 ),
inference(scs_inference,[],[i_0_173,i_0_52,i_0_53,i_0_115,i_0_50,i_0_65,i_0_183,i_0_60,i_0_118,i_0_116,i_0_59,i_0_108,i_0_48,i_0_137,i_0_69,i_0_70,i_0_71,i_0_72,i_0_73,i_0_74,i_0_75,i_0_76,i_0_77,i_0_78,i_0_79,i_0_80,i_0_81,i_0_82,i_0_83,i_0_84,i_0_39,i_0_56,i_0_67,i_0_40,i_0_68,i_0_87,i_0_105,i_0_41,i_0_88,i_0_97,i_0_96,i_0_89,i_0_38,i_0_55,i_0_85]) ).
cnf(i_0_4721,plain,
organization(esk6_0,esk14_0),
inference(scs_inference,[],[i_0_173,i_0_52,i_0_53,i_0_115,i_0_50,i_0_65,i_0_183,i_0_60,i_0_118,i_0_116,i_0_59,i_0_108,i_0_48,i_0_137,i_0_69,i_0_70,i_0_71,i_0_72,i_0_73,i_0_74,i_0_75,i_0_76,i_0_77,i_0_78,i_0_79,i_0_80,i_0_81,i_0_82,i_0_83,i_0_84,i_0_39,i_0_56,i_0_67,i_0_40,i_0_68,i_0_87,i_0_105,i_0_41,i_0_88,i_0_97,i_0_96,i_0_89,i_0_38,i_0_55,i_0_85,i_0_91]) ).
cnf(i_0_4722,plain,
( survival_chance(X1,esk14_0,X2)
| ~ survival_chance(X1,esk16_0,X2) ),
inference(scs_inference,[],[i_0_173,i_0_52,i_0_53,i_0_115,i_0_50,i_0_65,i_0_183,i_0_60,i_0_118,i_0_116,i_0_59,i_0_108,i_0_48,i_0_137,i_0_69,i_0_70,i_0_71,i_0_72,i_0_73,i_0_74,i_0_75,i_0_76,i_0_77,i_0_78,i_0_79,i_0_80,i_0_81,i_0_82,i_0_83,i_0_84,i_0_39,i_0_56,i_0_67,i_0_40,i_0_68,i_0_87,i_0_105,i_0_41,i_0_88,i_0_97,i_0_96,i_0_89,i_0_38,i_0_55,i_0_85,i_0_91,i_0_86]) ).
cnf(i_0_4723,plain,
survival_chance(esk6_0,esk9_0,esk15_0),
inference(equality_inference,[],[4720]) ).
cnf(i_0_4724,plain,
survival_chance(esk6_0,esk1_2(esk6_0,esk16_0),esk16_0),
inference(scs_inference,[],[i_0_4716,i_0_39]) ).
cnf(i_0_4725,plain,
( ~ organization(X1,X2)
| survival_chance(X1,esk1_2(X1,X2),X2) ),
inference(rename_variables,[],[i_0_39]) ).
cnf(i_0_4726,plain,
esk17_0 != esk14_0,
inference(scs_inference,[],[i_0_4715,i_0_4716,i_0_39,i_0_56]) ).
cnf(i_0_4727,plain,
( ~ greater(X1,X2)
| X1 != X2 ),
inference(rename_variables,[],[i_0_56]) ).
cnf(i_0_4728,plain,
esk4_8(esk14_0,X1,X2,X3,X4,X5,X6,X7) = esk4_8(esk16_0,X1,X2,X3,X4,X5,X6,X7),
inference(scs_inference,[],[i_0_4715,i_0_4716,i_0_65,i_0_39,i_0_56,i_0_69]) ).
cnf(i_0_4729,plain,
esk4_8(X1,esk14_0,X2,X3,X4,X5,X6,X7) = esk4_8(X1,esk16_0,X2,X3,X4,X5,X6,X7),
inference(scs_inference,[],[i_0_4715,i_0_4716,i_0_65,i_0_39,i_0_56,i_0_69,i_0_70]) ).
cnf(i_0_4730,plain,
esk4_8(X1,X2,esk14_0,X3,X4,X5,X6,X7) = esk4_8(X1,X2,esk16_0,X3,X4,X5,X6,X7),
inference(scs_inference,[],[i_0_4715,i_0_4716,i_0_65,i_0_39,i_0_56,i_0_69,i_0_70,i_0_71]) ).
cnf(i_0_4731,plain,
esk4_8(X1,X2,X3,esk14_0,X4,X5,X6,X7) = esk4_8(X1,X2,X3,esk16_0,X4,X5,X6,X7),
inference(scs_inference,[],[i_0_4715,i_0_4716,i_0_65,i_0_39,i_0_56,i_0_69,i_0_70,i_0_71,i_0_72]) ).
cnf(i_0_4732,plain,
esk4_8(X1,X2,X3,X4,esk14_0,X5,X6,X7) = esk4_8(X1,X2,X3,X4,esk16_0,X5,X6,X7),
inference(scs_inference,[],[i_0_4715,i_0_4716,i_0_65,i_0_39,i_0_56,i_0_69,i_0_70,i_0_71,i_0_72,i_0_73]) ).
cnf(i_0_4733,plain,
esk4_8(X1,X2,X3,X4,X5,esk14_0,X6,X7) = esk4_8(X1,X2,X3,X4,X5,esk16_0,X6,X7),
inference(scs_inference,[],[i_0_4715,i_0_4716,i_0_65,i_0_39,i_0_56,i_0_69,i_0_70,i_0_71,i_0_72,i_0_73,i_0_74]) ).
cnf(i_0_4734,plain,
esk4_8(X1,X2,X3,X4,X5,X6,esk14_0,X7) = esk4_8(X1,X2,X3,X4,X5,X6,esk16_0,X7),
inference(scs_inference,[],[i_0_4715,i_0_4716,i_0_65,i_0_39,i_0_56,i_0_69,i_0_70,i_0_71,i_0_72,i_0_73,i_0_74,i_0_75]) ).
cnf(i_0_4735,plain,
esk4_8(X1,X2,X3,X4,X5,X6,X7,esk14_0) = esk4_8(X1,X2,X3,X4,X5,X6,X7,esk16_0),
inference(scs_inference,[],[i_0_4715,i_0_4716,i_0_65,i_0_39,i_0_56,i_0_69,i_0_70,i_0_71,i_0_72,i_0_73,i_0_74,i_0_75,i_0_76]) ).
cnf(i_0_4736,plain,
esk3_8(esk14_0,X1,X2,X3,X4,X5,X6,X7) = esk3_8(esk16_0,X1,X2,X3,X4,X5,X6,X7),
inference(scs_inference,[],[i_0_4715,i_0_4716,i_0_65,i_0_39,i_0_56,i_0_69,i_0_70,i_0_71,i_0_72,i_0_73,i_0_74,i_0_75,i_0_76,i_0_77]) ).
cnf(i_0_4737,plain,
esk3_8(X1,esk14_0,X2,X3,X4,X5,X6,X7) = esk3_8(X1,esk16_0,X2,X3,X4,X5,X6,X7),
inference(scs_inference,[],[i_0_4715,i_0_4716,i_0_65,i_0_39,i_0_56,i_0_69,i_0_70,i_0_71,i_0_72,i_0_73,i_0_74,i_0_75,i_0_76,i_0_77,i_0_78]) ).
cnf(i_0_4738,plain,
esk3_8(X1,X2,esk14_0,X3,X4,X5,X6,X7) = esk3_8(X1,X2,esk16_0,X3,X4,X5,X6,X7),
inference(scs_inference,[],[i_0_4715,i_0_4716,i_0_65,i_0_39,i_0_56,i_0_69,i_0_70,i_0_71,i_0_72,i_0_73,i_0_74,i_0_75,i_0_76,i_0_77,i_0_78,i_0_79]) ).
cnf(i_0_4739,plain,
esk3_8(X1,X2,X3,esk14_0,X4,X5,X6,X7) = esk3_8(X1,X2,X3,esk16_0,X4,X5,X6,X7),
inference(scs_inference,[],[i_0_4715,i_0_4716,i_0_65,i_0_39,i_0_56,i_0_69,i_0_70,i_0_71,i_0_72,i_0_73,i_0_74,i_0_75,i_0_76,i_0_77,i_0_78,i_0_79,i_0_80]) ).
cnf(i_0_4740,plain,
esk3_8(X1,X2,X3,X4,esk14_0,X5,X6,X7) = esk3_8(X1,X2,X3,X4,esk16_0,X5,X6,X7),
inference(scs_inference,[],[i_0_4715,i_0_4716,i_0_65,i_0_39,i_0_56,i_0_69,i_0_70,i_0_71,i_0_72,i_0_73,i_0_74,i_0_75,i_0_76,i_0_77,i_0_78,i_0_79,i_0_80,i_0_81]) ).
cnf(i_0_4741,plain,
esk3_8(X1,X2,X3,X4,X5,esk14_0,X6,X7) = esk3_8(X1,X2,X3,X4,X5,esk16_0,X6,X7),
inference(scs_inference,[],[i_0_4715,i_0_4716,i_0_65,i_0_39,i_0_56,i_0_69,i_0_70,i_0_71,i_0_72,i_0_73,i_0_74,i_0_75,i_0_76,i_0_77,i_0_78,i_0_79,i_0_80,i_0_81,i_0_82]) ).
cnf(i_0_4742,plain,
esk3_8(X1,X2,X3,X4,X5,X6,esk14_0,X7) = esk3_8(X1,X2,X3,X4,X5,X6,esk16_0,X7),
inference(scs_inference,[],[i_0_4715,i_0_4716,i_0_65,i_0_39,i_0_56,i_0_69,i_0_70,i_0_71,i_0_72,i_0_73,i_0_74,i_0_75,i_0_76,i_0_77,i_0_78,i_0_79,i_0_80,i_0_81,i_0_82,i_0_83]) ).
cnf(i_0_4743,plain,
esk3_8(X1,X2,X3,X4,X5,X6,X7,esk14_0) = esk3_8(X1,X2,X3,X4,X5,X6,X7,esk16_0),
inference(scs_inference,[],[i_0_4715,i_0_4716,i_0_65,i_0_39,i_0_56,i_0_69,i_0_70,i_0_71,i_0_72,i_0_73,i_0_74,i_0_75,i_0_76,i_0_77,i_0_78,i_0_79,i_0_80,i_0_81,i_0_82,i_0_83,i_0_84]) ).
cnf(i_0_4744,plain,
esk17_0 != esk16_0,
inference(scs_inference,[],[i_0_4715,i_0_4706,i_0_4716,i_0_65,i_0_39,i_0_56,i_0_69,i_0_70,i_0_71,i_0_72,i_0_73,i_0_74,i_0_75,i_0_76,i_0_77,i_0_78,i_0_79,i_0_80,i_0_81,i_0_82,i_0_83,i_0_84,i_0_67]) ).
cnf(i_0_4745,plain,
greater(esk17_0,esk15_0),
inference(scs_inference,[],[i_0_4715,i_0_4706,i_0_4716,i_0_49,i_0_65,i_0_39,i_0_56,i_0_69,i_0_70,i_0_71,i_0_72,i_0_73,i_0_74,i_0_75,i_0_76,i_0_77,i_0_78,i_0_79,i_0_80,i_0_81,i_0_82,i_0_83,i_0_84,i_0_67,i_0_40]) ).
cnf(i_0_4746,plain,
( ~ reorganization(X1,X2,X3)
| greater(X3,X2) ),
inference(rename_variables,[],[i_0_40]) ).
cnf(i_0_4747,plain,
~ greater(esk15_0,esk17_0),
inference(scs_inference,[],[i_0_4715,i_0_4706,i_0_4716,i_0_49,i_0_65,i_0_107,i_0_39,i_0_56,i_0_69,i_0_70,i_0_71,i_0_72,i_0_73,i_0_74,i_0_75,i_0_76,i_0_77,i_0_78,i_0_79,i_0_80,i_0_81,i_0_82,i_0_83,i_0_84,i_0_67,i_0_40,i_0_41]) ).
cnf(i_0_4748,plain,
~ greater(X1,X1),
inference(rename_variables,[],[i_0_107]) ).
cnf(i_0_4749,plain,
( ~ greater(X1,X2)
| greater(X1,X3)
| ~ greater(X2,X3) ),
inference(rename_variables,[],[i_0_41]) ).
cnf(i_0_4750,plain,
esk4_8(esk16_0,esk16_0,X1,X2,X3,X4,X5,X6) = esk4_8(esk14_0,esk14_0,X1,X2,X3,X4,X5,X6),
inference(scs_inference,[],[i_0_4715,i_0_4706,i_0_4716,i_0_4683,i_0_4684,i_0_49,i_0_65,i_0_107,i_0_39,i_0_56,i_0_69,i_0_70,i_0_71,i_0_72,i_0_73,i_0_74,i_0_75,i_0_76,i_0_77,i_0_78,i_0_79,i_0_80,i_0_81,i_0_82,i_0_83,i_0_84,i_0_67,i_0_40,i_0_41,i_0_68]) ).
cnf(i_0_4751,plain,
esk4_8(esk16_0,X1,X2,X3,X4,X5,X6,X7) = esk4_8(esk14_0,X1,X2,X3,X4,X5,X6,X7),
inference(rename_variables,[],[i_0_4683]) ).
cnf(i_0_4752,plain,
esk4_8(X1,esk16_0,X2,X3,X4,X5,X6,X7) = esk4_8(X1,esk14_0,X2,X3,X4,X5,X6,X7),
inference(rename_variables,[],[i_0_4684]) ).
cnf(i_0_4753,plain,
survival_chance(esk6_0,esk11_0,esk16_0),
inference(scs_inference,[],[i_0_4715,i_0_4706,i_0_4716,i_0_4683,i_0_4684,i_0_51,i_0_49,i_0_65,i_0_107,i_0_39,i_0_56,i_0_69,i_0_70,i_0_71,i_0_72,i_0_73,i_0_74,i_0_75,i_0_76,i_0_77,i_0_78,i_0_79,i_0_80,i_0_81,i_0_82,i_0_83,i_0_84,i_0_67,i_0_40,i_0_41,i_0_68,i_0_87]) ).
cnf(i_0_4754,plain,
esk15_0 != esk16_0,
inference(scs_inference,[],[i_0_4715,i_0_4706,i_0_4712,i_0_4716,i_0_4683,i_0_4684,i_0_161,i_0_51,i_0_49,i_0_65,i_0_107,i_0_39,i_0_56,i_0_69,i_0_70,i_0_71,i_0_72,i_0_73,i_0_74,i_0_75,i_0_76,i_0_77,i_0_78,i_0_79,i_0_80,i_0_81,i_0_82,i_0_83,i_0_84,i_0_67,i_0_40,i_0_41,i_0_68,i_0_87,i_0_96]) ).
cnf(i_0_4755,plain,
~ reorganization(X1,esk16_0,esk14_0),
inference(rename_variables,[],[i_0_161]) ).
cnf(i_0_4756,plain,
esk15_0 != esk14_0,
inference(scs_inference,[],[i_0_4715,i_0_4704,i_0_4706,i_0_4712,i_0_4716,i_0_4683,i_0_4684,i_0_161,i_0_51,i_0_49,i_0_65,i_0_116,i_0_107,i_0_39,i_0_56,i_0_69,i_0_70,i_0_71,i_0_72,i_0_73,i_0_74,i_0_75,i_0_76,i_0_77,i_0_78,i_0_79,i_0_80,i_0_81,i_0_82,i_0_83,i_0_84,i_0_67,i_0_40,i_0_41,i_0_68,i_0_87,i_0_96,i_0_89]) ).
cnf(i_0_4757,plain,
( organization(X1,esk16_0)
| esk6_0 != X1 ),
inference(scs_inference,[],[i_0_4715,i_0_4704,i_0_4706,i_0_4712,i_0_4716,i_0_4683,i_0_4684,i_0_161,i_0_51,i_0_49,i_0_65,i_0_116,i_0_107,i_0_39,i_0_56,i_0_69,i_0_70,i_0_71,i_0_72,i_0_73,i_0_74,i_0_75,i_0_76,i_0_77,i_0_78,i_0_79,i_0_80,i_0_81,i_0_82,i_0_83,i_0_84,i_0_67,i_0_40,i_0_41,i_0_68,i_0_87,i_0_96,i_0_89,i_0_90]) ).
cnf(i_0_4758,plain,
( esk6_0 != esk5_0
| ~ survival_chance(esk5_0,esk10_0,esk17_0) ),
inference(scs_inference,[],[i_0_4715,i_0_4704,i_0_4706,i_0_4707,i_0_4712,i_0_4716,i_0_4683,i_0_4684,i_0_161,i_0_51,i_0_49,i_0_65,i_0_116,i_0_107,i_0_39,i_0_56,i_0_69,i_0_70,i_0_71,i_0_72,i_0_73,i_0_74,i_0_75,i_0_76,i_0_77,i_0_78,i_0_79,i_0_80,i_0_81,i_0_82,i_0_83,i_0_84,i_0_67,i_0_40,i_0_41,i_0_68,i_0_87,i_0_96,i_0_89,i_0_90,i_0_2545]) ).
cnf(i_0_4759,plain,
( ~ organization(esk5_0,esk16_0)
| ~ survival_chance(esk5_0,X1,esk16_0)
| ~ survival_chance(esk5_0,X1,esk17_0) ),
inference(rename_variables,[],[i_0_2545]) ).
cnf(i_0_4760,plain,
( class(esk4_8(esk14_0,X1,X2,X3,X4,X5,X6,X7),X8,X9)
| esk6_0 != esk5_0
| ~ class(esk4_8(esk16_0,X1,X2,X3,X4,X5,X6,X7),X8,X9) ),
inference(scs_inference,[],[i_0_4715,i_0_4704,i_0_4706,i_0_4707,i_0_4712,i_0_4716,i_0_4683,i_0_4751,i_0_4684,i_0_161,i_0_51,i_0_49,i_0_65,i_0_116,i_0_107,i_0_39,i_0_56,i_0_69,i_0_70,i_0_71,i_0_72,i_0_73,i_0_74,i_0_75,i_0_76,i_0_77,i_0_78,i_0_79,i_0_80,i_0_81,i_0_82,i_0_83,i_0_84,i_0_67,i_0_40,i_0_41,i_0_68,i_0_87,i_0_96,i_0_89,i_0_90,i_0_2545,i_0_92]) ).
cnf(i_0_4761,plain,
organization(esk6_0,esk16_0),
inference(equality_inference,[],[4757]) ).
cnf(i_0_4762,plain,
survival_chance(esk6_0,esk1_2(esk6_0,esk14_0),esk14_0),
inference(scs_inference,[],[i_0_4721,i_0_39]) ).
cnf(i_0_4763,plain,
( ~ organization(X1,X2)
| survival_chance(X1,esk1_2(X1,X2),X2) ),
inference(rename_variables,[],[i_0_39]) ).
cnf(i_0_4764,plain,
esk14_0 != esk15_0,
inference(scs_inference,[],[i_0_4721,i_0_4711,i_0_39,i_0_56]) ).
cnf(i_0_4765,plain,
( ~ greater(X1,X2)
| X1 != X2 ),
inference(rename_variables,[],[i_0_56]) ).
cnf(i_0_4766,plain,
esk16_0 != esk15_0,
inference(scs_inference,[],[i_0_4721,i_0_4754,i_0_4711,i_0_39,i_0_56,i_0_67]) ).
cnf(i_0_4767,plain,
~ reorganization(X1,esk4_8(esk16_0,X2,esk16_0,X3,X4,X5,X6,X7),esk4_8(esk14_0,X2,esk14_0,X3,X4,X5,X6,X7)),
inference(scs_inference,[],[i_0_4721,i_0_4754,i_0_4713,i_0_4685,i_0_4711,i_0_39,i_0_56,i_0_67,i_0_96]) ).
cnf(i_0_4768,plain,
esk4_8(X1,X2,esk16_0,X3,X4,X5,X6,X7) = esk4_8(X1,X2,esk14_0,X3,X4,X5,X6,X7),
inference(rename_variables,[],[i_0_4685]) ).
cnf(i_0_4769,plain,
~ reorganization(X1,esk4_8(esk16_0,X2,X3,X4,X5,X6,X7,X8),esk4_8(esk14_0,X2,X3,X4,X5,X6,X7,X8)),
inference(rename_variables,[],[i_0_4713]) ).
cnf(i_0_4770,plain,
~ greater(esk4_8(X1,X2,esk14_0,X3,X4,X5,X6,X7),esk4_8(X1,X2,esk16_0,X3,X4,X5,X6,X7)),
inference(scs_inference,[],[i_0_4721,i_0_4754,i_0_4713,i_0_4685,i_0_4768,i_0_4711,i_0_107,i_0_39,i_0_56,i_0_67,i_0_96,i_0_89]) ).
cnf(i_0_4771,plain,
~ greater(X1,X1),
inference(rename_variables,[],[i_0_107]) ).
cnf(i_0_4772,plain,
( class(esk5_0,X1,esk15_0)
| esk8_0 != X1 ),
inference(scs_inference,[],[i_0_4721,i_0_4754,i_0_4713,i_0_4685,i_0_4768,i_0_4711,i_0_47,i_0_107,i_0_39,i_0_56,i_0_67,i_0_96,i_0_89,i_0_93]) ).
cnf(i_0_4773,plain,
esk4_8(X1,X2,esk16_0,esk16_0,X3,X4,X5,X6) = esk4_8(X1,X2,esk14_0,esk14_0,X3,X4,X5,X6),
inference(scs_inference,[],[i_0_4721,i_0_4754,i_0_4713,i_0_4685,i_0_4768,i_0_4686,i_0_4711,i_0_47,i_0_107,i_0_39,i_0_56,i_0_67,i_0_96,i_0_89,i_0_93,i_0_68]) ).
cnf(i_0_4774,plain,
esk4_8(X1,X2,esk16_0,X3,X4,X5,X6,X7) = esk4_8(X1,X2,esk14_0,X3,X4,X5,X6,X7),
inference(rename_variables,[],[i_0_4685]) ).
cnf(i_0_4775,plain,
esk4_8(X1,X2,X3,esk16_0,X4,X5,X6,X7) = esk4_8(X1,X2,X3,esk14_0,X4,X5,X6,X7),
inference(rename_variables,[],[i_0_4686]) ).
cnf(i_0_4776,plain,
survival_chance(esk6_0,esk1_2(esk6_0,esk16_0),esk14_0),
inference(scs_inference,[],[i_0_4721,i_0_4754,i_0_4713,i_0_4685,i_0_4768,i_0_4686,i_0_4724,i_0_4711,i_0_47,i_0_115,i_0_107,i_0_39,i_0_56,i_0_67,i_0_96,i_0_89,i_0_93,i_0_68,i_0_87]) ).
cnf(i_0_4777,plain,
( class(X1,X2,esk4_8(X3,X4,esk14_0,X5,X6,X7,X8,X9))
| ~ class(X1,X2,esk4_8(X3,X4,esk16_0,X5,X6,X7,X8,X9)) ),
inference(scs_inference,[],[i_0_4721,i_0_4754,i_0_4713,i_0_4685,i_0_4768,i_0_4774,i_0_4686,i_0_4724,i_0_4711,i_0_47,i_0_115,i_0_107,i_0_39,i_0_56,i_0_67,i_0_96,i_0_89,i_0_93,i_0_68,i_0_87,i_0_94]) ).
cnf(i_0_4778,plain,
class(esk5_0,esk8_0,esk15_0),
inference(equality_inference,[],[4772]) ).
cnf(i_0_4779,plain,
survival_chance(esk5_0,esk1_2(esk5_0,esk15_0),esk15_0),
inference(scs_inference,[],[i_0_62,i_0_39]) ).
cnf(i_0_4780,plain,
( ~ organization(X1,X2)
| survival_chance(X1,esk1_2(X1,X2),X2) ),
inference(rename_variables,[],[i_0_39]) ).
cnf(i_0_4781,plain,
esk6_0 != esk5_0,
inference(scs_inference,[],[i_0_123,i_0_62,i_0_39,i_0_67]) ).
cnf(i_0_4782,plain,
survival_chance(esk6_0,esk1_2(esk6_0,esk14_0),esk16_0),
inference(scs_inference,[],[i_0_4762,i_0_65,i_0_123,i_0_62,i_0_39,i_0_67,i_0_87]) ).
cnf(i_0_4783,plain,
esk12_0 != esk13_0,
inference(scs_inference,[],[i_0_4762,i_0_65,i_0_123,i_0_62,i_0_107,i_0_63,i_0_39,i_0_67,i_0_87,i_0_89]) ).
cnf(i_0_4784,plain,
~ greater(X1,X1),
inference(rename_variables,[],[i_0_107]) ).
cnf(i_0_4785,plain,
( reorganization_type(X1,esk7_0,esk15_0)
| esk5_0 != X1 ),
inference(scs_inference,[],[i_0_4762,i_0_45,i_0_65,i_0_123,i_0_62,i_0_107,i_0_63,i_0_39,i_0_67,i_0_87,i_0_89,i_0_98]) ).
cnf(i_0_4786,plain,
( reorganization_type(esk4_8(X1,X2,X3,X4,esk14_0,X5,X6,X7),esk7_0,esk15_0)
| esk5_0 != esk4_8(X1,X2,X3,X4,esk16_0,X5,X6,X7) ),
inference(scs_inference,[],[i_0_4687,i_0_4762,i_0_45,i_0_65,i_0_123,i_0_62,i_0_107,i_0_63,i_0_39,i_0_67,i_0_87,i_0_89,i_0_98,i_0_68]) ).
cnf(i_0_4787,plain,
( reorganization_type(esk4_8(X1,X2,X3,X4,esk14_0,X5,X6,X7),esk7_0,esk15_0)
| reorganization_type(X8,esk4_8(X1,X2,X3,X4,esk14_0,X5,X6,X7),X9)
| ~ reorganization_type(X8,esk4_8(X1,X2,X3,X4,esk16_0,X5,X6,X7),X9) ),
inference(scs_inference,[],[i_0_4687,i_0_4762,i_0_45,i_0_65,i_0_123,i_0_62,i_0_107,i_0_63,i_0_39,i_0_67,i_0_87,i_0_89,i_0_98,i_0_68,i_0_99]) ).
cnf(i_0_4788,plain,
reorganization_type(esk5_0,esk7_0,esk15_0),
inference(equality_inference,[],[4785]) ).
cnf(i_0_4789,plain,
survival_chance(esk6_0,esk1_2(esk6_0,esk17_0),esk17_0),
inference(scs_inference,[],[i_0_59,i_0_39]) ).
cnf(i_0_4790,plain,
( ~ organization(X1,X2)
| survival_chance(X1,esk1_2(X1,X2),X2) ),
inference(rename_variables,[],[i_0_39]) ).
cnf(i_0_4791,plain,
esk4_8(X1,X2,X3,X4,X5,esk16_0,esk16_0,X6) = esk4_8(X1,X2,X3,X4,X5,esk14_0,esk14_0,X6),
inference(scs_inference,[],[i_0_4688,i_0_4689,i_0_59,i_0_39,i_0_68]) ).
cnf(i_0_4792,plain,
esk4_8(X1,X2,X3,X4,X5,esk16_0,X6,X7) = esk4_8(X1,X2,X3,X4,X5,esk14_0,X6,X7),
inference(rename_variables,[],[i_0_4688]) ).
cnf(i_0_4793,plain,
esk4_8(X1,X2,X3,X4,X5,X6,esk16_0,X7) = esk4_8(X1,X2,X3,X4,X5,X6,esk14_0,X7),
inference(rename_variables,[],[i_0_4689]) ).
cnf(i_0_4794,plain,
~ greater(esk4_8(X1,X2,esk14_0,X3,X4,esk14_0,X5,X6),esk4_8(X1,X2,esk16_0,X3,X4,esk16_0,X5,X6)),
inference(scs_inference,[],[i_0_4688,i_0_4792,i_0_4689,i_0_4770,i_0_59,i_0_39,i_0_68,i_0_89]) ).
cnf(i_0_4795,plain,
esk4_8(X1,X2,X3,X4,X5,esk16_0,X6,X7) = esk4_8(X1,X2,X3,X4,X5,esk14_0,X6,X7),
inference(rename_variables,[],[i_0_4688]) ).
cnf(i_0_4796,plain,
~ greater(esk4_8(X1,X2,esk14_0,X3,X4,X5,X6,X7),esk4_8(X1,X2,esk16_0,X3,X4,X5,X6,X7)),
inference(rename_variables,[],[i_0_4770]) ).
cnf(i_0_4797,plain,
greater(esk1_2(esk6_0,esk15_0),esk1_2(esk6_0,esk16_0)),
inference(scs_inference,[],[i_0_4688,i_0_4792,i_0_4689,i_0_4770,i_0_4699,i_0_4776,i_0_4721,i_0_4711,i_0_49,i_0_60,i_0_107,i_0_59,i_0_141,i_0_39,i_0_68,i_0_89,i_0_35]) ).
cnf(i_0_4798,plain,
~ greater(X1,X1),
inference(rename_variables,[],[i_0_107]) ).
cnf(i_0_4799,plain,
( ~ greater(X1,X2)
| ~ survival_chance(X3,X4,X1)
| ~ survival_chance(X3,X5,X2)
| ~ reorganization(X3,X6,X7)
| greater(X6,X2)
| greater(X1,X7)
| greater(X5,X4)
| ~ organization(X3,X2)
| ~ organization(X3,X1) ),
inference(rename_variables,[],[i_0_35]) ).
cnf(i_0_4800,plain,
~ greater(esk1_2(esk6_0,esk16_0),esk1_2(esk6_0,esk15_0)),
inference(scs_inference,[],[i_0_4688,i_0_4792,i_0_4689,i_0_4770,i_0_4699,i_0_4776,i_0_4721,i_0_4711,i_0_49,i_0_60,i_0_107,i_0_59,i_0_141,i_0_39,i_0_68,i_0_89,i_0_35,i_0_55]) ).
cnf(i_0_4801,plain,
( ~ greater(X1,X2)
| ~ greater(X2,X1) ),
inference(rename_variables,[],[i_0_55]) ).
cnf(i_0_4802,plain,
esk1_2(esk6_0,esk15_0) != esk1_2(esk6_0,esk16_0),
inference(scs_inference,[],[i_0_4688,i_0_4792,i_0_4689,i_0_4770,i_0_4699,i_0_4776,i_0_4721,i_0_4711,i_0_49,i_0_60,i_0_107,i_0_59,i_0_141,i_0_39,i_0_68,i_0_89,i_0_35,i_0_55,i_0_56]) ).
cnf(i_0_4803,plain,
( ~ greater(X1,X2)
| X1 != X2 ),
inference(rename_variables,[],[i_0_56]) ).
cnf(i_0_4804,plain,
esk1_2(esk6_0,esk16_0) != esk1_2(esk6_0,esk15_0),
inference(scs_inference,[],[i_0_4688,i_0_4792,i_0_4689,i_0_4770,i_0_4699,i_0_4776,i_0_4721,i_0_4711,i_0_49,i_0_60,i_0_107,i_0_59,i_0_141,i_0_39,i_0_68,i_0_89,i_0_35,i_0_55,i_0_56,i_0_67]) ).
cnf(i_0_4805,plain,
( reorganization_type(esk5_0,esk7_0,X1)
| esk15_0 != X1 ),
inference(scs_inference,[],[i_0_4688,i_0_4792,i_0_4689,i_0_4770,i_0_4699,i_0_4776,i_0_4721,i_0_4711,i_0_45,i_0_49,i_0_60,i_0_107,i_0_59,i_0_141,i_0_39,i_0_68,i_0_89,i_0_35,i_0_55,i_0_56,i_0_67,i_0_100]) ).
cnf(i_0_4806,plain,
( reorganization_free(esk4_8(X1,X2,X3,X4,X5,esk14_0,X6,X7),X8,X9)
| ~ reorganization_free(esk4_8(X1,X2,X3,X4,X5,esk16_0,X6,X7),X8,X9) ),
inference(scs_inference,[],[i_0_4688,i_0_4792,i_0_4795,i_0_4689,i_0_4770,i_0_4699,i_0_4776,i_0_4721,i_0_4711,i_0_45,i_0_49,i_0_60,i_0_107,i_0_59,i_0_141,i_0_39,i_0_68,i_0_89,i_0_35,i_0_55,i_0_56,i_0_67,i_0_100,i_0_104]) ).
cnf(i_0_4807,plain,
reorganization_type(esk5_0,esk7_0,esk15_0),
inference(equality_inference,[],[4805]) ).
cnf(i_0_4808,plain,
survival_chance(esk5_0,esk1_2(esk5_0,esk17_0),esk17_0),
inference(scs_inference,[],[i_0_61,i_0_39]) ).
cnf(i_0_4809,plain,
( ~ organization(X1,X2)
| survival_chance(X1,esk1_2(X1,X2),X2) ),
inference(rename_variables,[],[i_0_39]) ).
cnf(i_0_4810,plain,
( reorganization_free(esk5_0,esk14_0,X1)
| esk17_0 != X1 ),
inference(scs_inference,[],[i_0_4708,i_0_61,i_0_39,i_0_106]) ).
cnf(i_0_4811,plain,
( reorganization_free(esk5_0,esk14_0,esk4_8(X1,X2,X3,X4,X5,X6,X7,esk14_0))
| esk17_0 != esk4_8(X1,X2,X3,X4,X5,X6,X7,esk16_0) ),
inference(scs_inference,[],[i_0_4690,i_0_4708,i_0_61,i_0_39,i_0_106,i_0_68]) ).
cnf(i_0_4812,plain,
( esk4_8(X1,X2,X3,X4,X5,X6,X7,esk14_0) != esk17_0
| reorganization_free(esk5_0,esk14_0,esk4_8(X1,X2,X3,X4,X5,X6,X7,esk14_0)) ),
inference(scs_inference,[],[i_0_4690,i_0_4708,i_0_61,i_0_39,i_0_106,i_0_68,i_0_67]) ).
cnf(i_0_4813,plain,
( ~ survival_chance(esk5_0,X1,esk16_0)
| ~ organization(esk5_0,esk16_0)
| ~ survival_chance(esk5_0,X1,esk17_0) ),
inference(rename_variables,[],[i_0_2545]) ).
cnf(i_0_4814,plain,
( reorganization_free(esk5_0,esk14_0,esk4_8(X1,X2,X3,X4,X5,X6,X7,esk14_0))
| ~ organization(esk5_0,esk16_0)
| ~ survival_chance(esk5_0,esk10_0,esk17_0) ),
inference(scs_inference,[],[i_0_4690,i_0_4708,i_0_4707,i_0_61,i_0_39,i_0_106,i_0_68,i_0_67,i_0_2545]) ).
cnf(i_0_4815,plain,
reorganization_free(esk5_0,esk14_0,esk17_0),
inference(equality_inference,[],[4810]) ).
cnf(i_0_4816,plain,
esk3_8(esk16_0,esk16_0,X1,X2,X3,X4,X5,X6) = esk3_8(esk14_0,esk14_0,X1,X2,X3,X4,X5,X6),
inference(scs_inference,[],[i_0_4691,i_0_4692,i_0_68]) ).
cnf(i_0_4817,plain,
esk3_8(esk16_0,X1,X2,X3,X4,X5,X6,X7) = esk3_8(esk14_0,X1,X2,X3,X4,X5,X6,X7),
inference(rename_variables,[],[i_0_4691]) ).
cnf(i_0_4818,plain,
esk3_8(X1,esk16_0,X2,X3,X4,X5,X6,X7) = esk3_8(X1,esk14_0,X2,X3,X4,X5,X6,X7),
inference(rename_variables,[],[i_0_4692]) ).
cnf(i_0_4819,plain,
~ greater(esk3_8(esk16_0,X1,X2,X3,X4,X5,X6,X7),esk3_8(esk14_0,X1,X2,X3,X4,X5,X6,X7)),
inference(scs_inference,[],[i_0_4691,i_0_4817,i_0_4692,i_0_107,i_0_68,i_0_88]) ).
cnf(i_0_4820,plain,
~ greater(X1,X1),
inference(rename_variables,[],[i_0_107]) ).
cnf(i_0_4821,plain,
~ reorganization(X1,esk3_8(esk14_0,X2,X3,X4,X5,X6,X7,X8),esk3_8(esk16_0,X2,X3,X4,X5,X6,X7,X8)),
inference(scs_inference,[],[i_0_4691,i_0_4817,i_0_4692,i_0_173,i_0_107,i_0_68,i_0_88,i_0_97]) ).
cnf(i_0_4822,plain,
~ reorganization(X1,X2,X2),
inference(rename_variables,[],[i_0_173]) ).
cnf(i_0_4823,plain,
( survival_chance(esk3_8(esk14_0,X1,X2,X3,X4,X5,X6,X7),X8,X9)
| ~ survival_chance(esk3_8(esk16_0,X1,X2,X3,X4,X5,X6,X7),X8,X9) ),
inference(scs_inference,[],[i_0_4691,i_0_4817,i_0_4692,i_0_173,i_0_107,i_0_68,i_0_88,i_0_97,i_0_85]) ).
cnf(i_0_4824,plain,
( survival_chance(esk3_8(esk14_0,X1,X2,X3,X4,X5,X6,X7),X8,esk3_8(esk14_0,X1,X2,X3,X4,X5,X6,X7))
| ~ survival_chance(esk3_8(esk16_0,X1,X2,X3,X4,X5,X6,X7),X8,esk3_8(esk16_0,X1,X2,X3,X4,X5,X6,X7)) ),
inference(scs_inference,[],[i_0_4691,i_0_4817,i_0_4692,i_0_173,i_0_107,i_0_68,i_0_88,i_0_97,i_0_85,i_0_87]) ).
cnf(i_0_4825,plain,
( ~ reorganization_free(esk6_0,esk15_0,esk16_0)
| survival_chance(esk3_8(esk14_0,X1,X2,X3,X4,X5,X6,X7),X8,esk3_8(esk14_0,X1,X2,X3,X4,X5,X6,X7)) ),
inference(scs_inference,[],[i_0_4800,i_0_4691,i_0_4817,i_0_4692,i_0_4699,i_0_4724,i_0_173,i_0_4704,i_0_4716,i_0_60,i_0_107,i_0_68,i_0_88,i_0_97,i_0_85,i_0_87,i_0_36]) ).
cnf(i_0_4826,plain,
( ~ survival_chance(X1,X2,X3)
| ~ greater(X3,X4)
| greater(X2,X5)
| ~ organization(X1,X4)
| ~ organization(X1,X3)
| ~ survival_chance(X1,X5,X4)
| ~ reorganization_free(X1,X4,X3) ),
inference(rename_variables,[],[i_0_36]) ).
cnf(i_0_4827,plain,
( survival_chance(esk3_8(esk14_0,X1,X2,X3,X4,X5,X6,X7),esk14_0,esk3_8(esk14_0,X1,X2,X3,X4,X5,X6,X7))
| ~ survival_chance(esk3_8(esk16_0,X1,X2,X3,X4,X5,X6,X7),esk16_0,esk3_8(esk14_0,X1,X2,X3,X4,X5,X6,X7)) ),
inference(scs_inference,[],[i_0_4800,i_0_4691,i_0_4817,i_0_4692,i_0_4699,i_0_4724,i_0_173,i_0_4704,i_0_4716,i_0_60,i_0_107,i_0_68,i_0_88,i_0_97,i_0_85,i_0_87,i_0_36,i_0_4722]) ).
cnf(i_0_4828,plain,
( survival_chance(esk3_8(esk14_0,X1,X2,X3,X4,X5,X6,X7),esk14_0,esk3_8(esk14_0,X1,X2,X3,X4,X5,X6,X7))
| survival_chance(X8,esk3_8(esk14_0,X1,X2,X3,X4,X5,X6,X7),X9)
| ~ survival_chance(X8,esk3_8(esk16_0,X1,X2,X3,X4,X5,X6,X7),X9) ),
inference(scs_inference,[],[i_0_4800,i_0_4691,i_0_4817,i_0_4692,i_0_4699,i_0_4724,i_0_173,i_0_4704,i_0_4716,i_0_60,i_0_107,i_0_68,i_0_88,i_0_97,i_0_85,i_0_87,i_0_36,i_0_4722,i_0_86]) ).
cnf(i_0_4829,plain,
( organization(esk3_8(X1,X2,esk14_0,X3,X4,X5,X6,X7),X8)
| ~ organization(esk3_8(X1,X2,esk16_0,X3,X4,X5,X6,X7),X8) ),
inference(scs_inference,[],[i_0_4693,i_0_90]) ).
cnf(i_0_4830,plain,
( organization(esk3_8(X1,X2,esk14_0,X3,X4,X5,X6,X7),esk3_8(X1,X2,esk14_0,X3,X4,X5,X6,X7))
| ~ organization(esk3_8(X1,X2,esk16_0,X3,X4,X5,X6,X7),esk3_8(X1,X2,esk16_0,X3,X4,X5,X6,X7)) ),
inference(scs_inference,[],[i_0_4693,i_0_90,i_0_91]) ).
cnf(i_0_4831,plain,
( organization(esk3_8(X1,X2,esk14_0,X3,X4,X5,X6,X7),esk3_8(X1,X2,esk14_0,X3,X4,X5,X6,X7))
| class(esk3_8(X1,X2,esk14_0,X3,X4,X5,X6,X7),X8,X9)
| ~ class(esk3_8(X1,X2,esk16_0,X3,X4,X5,X6,X7),X8,X9) ),
inference(scs_inference,[],[i_0_4693,i_0_90,i_0_91,i_0_92]) ).
cnf(i_0_4832,plain,
~ reorganization(X1,esk3_8(esk14_0,X2,X3,esk16_0,X4,X5,X6,X7),esk3_8(esk16_0,X2,X3,esk14_0,X4,X5,X6,X7)),
inference(scs_inference,[],[i_0_4821,i_0_4694,i_0_96]) ).
cnf(i_0_4833,plain,
esk3_8(X1,X2,X3,esk16_0,X4,X5,X6,X7) = esk3_8(X1,X2,X3,esk14_0,X4,X5,X6,X7),
inference(rename_variables,[],[i_0_4694]) ).
cnf(i_0_4834,plain,
~ reorganization(X1,esk3_8(esk14_0,X2,X3,X4,X5,X6,X7,X8),esk3_8(esk16_0,X2,X3,X4,X5,X6,X7,X8)),
inference(rename_variables,[],[i_0_4821]) ).
cnf(i_0_4835,plain,
greater(esk1_2(esk6_0,esk14_0),esk1_2(esk6_0,esk17_0)),
inference(scs_inference,[],[i_0_4709,i_0_4789,i_0_4821,i_0_4694,i_0_4762,i_0_4715,i_0_4721,i_0_49,i_0_107,i_0_59,i_0_96,i_0_35]) ).
cnf(i_0_4836,plain,
~ greater(X1,X1),
inference(rename_variables,[],[i_0_107]) ).
cnf(i_0_4837,plain,
( ~ organization(X1,X2)
| ~ reorganization(X1,X3,X4)
| ~ survival_chance(X1,X5,X2)
| ~ survival_chance(X1,X6,X7)
| greater(X3,X2)
| greater(X7,X4)
| greater(X5,X6)
| ~ greater(X7,X2)
| ~ organization(X1,X7) ),
inference(rename_variables,[],[i_0_35]) ).
cnf(i_0_4838,plain,
~ greater(esk1_2(esk6_0,esk17_0),esk1_2(esk6_0,esk14_0)),
inference(scs_inference,[],[i_0_4709,i_0_4789,i_0_4821,i_0_4694,i_0_4762,i_0_4715,i_0_4721,i_0_49,i_0_107,i_0_59,i_0_96,i_0_35,i_0_55]) ).
cnf(i_0_4839,plain,
( ~ greater(X1,X2)
| ~ greater(X2,X1) ),
inference(rename_variables,[],[i_0_55]) ).
cnf(i_0_4840,plain,
esk1_2(esk6_0,esk14_0) != esk1_2(esk6_0,esk17_0),
inference(scs_inference,[],[i_0_4709,i_0_4789,i_0_4821,i_0_4694,i_0_4762,i_0_4715,i_0_4721,i_0_49,i_0_107,i_0_59,i_0_96,i_0_35,i_0_55,i_0_56]) ).
cnf(i_0_4841,plain,
( ~ greater(X1,X2)
| X1 != X2 ),
inference(rename_variables,[],[i_0_56]) ).
cnf(i_0_4842,plain,
esk1_2(esk6_0,esk17_0) != esk1_2(esk6_0,esk14_0),
inference(scs_inference,[],[i_0_4709,i_0_4789,i_0_4821,i_0_4694,i_0_4762,i_0_4715,i_0_4721,i_0_49,i_0_107,i_0_59,i_0_96,i_0_35,i_0_55,i_0_56,i_0_67]) ).
cnf(i_0_4843,plain,
( class(X1,esk3_8(X2,X3,X4,esk14_0,X5,X6,X7,X8),X9)
| ~ class(X1,esk3_8(X2,X3,X4,esk16_0,X5,X6,X7,X8),X9) ),
inference(scs_inference,[],[i_0_4709,i_0_4789,i_0_4821,i_0_4694,i_0_4833,i_0_4762,i_0_4715,i_0_4721,i_0_49,i_0_107,i_0_59,i_0_96,i_0_35,i_0_55,i_0_56,i_0_67,i_0_93]) ).
cnf(i_0_4844,plain,
~ reorganization(esk6_0,esk15_0,esk14_0),
inference(scs_inference,[],[i_0_42,i_0_4709,i_0_4789,i_0_4821,i_0_4694,i_0_4833,i_0_4762,i_0_4715,i_0_47,i_0_4721,i_0_43,i_0_45,i_0_44,i_0_46,i_0_50,i_0_49,i_0_60,i_0_113,i_0_62,i_0_107,i_0_59,i_0_63,i_0_96,i_0_35,i_0_55,i_0_56,i_0_67,i_0_93,i_0_34]) ).
cnf(i_0_4845,plain,
( greater(X1,X2)
| ~ class(X3,X4,X5)
| ~ organization(X3,X5)
| ~ reorganization_type(X3,X6,X5)
| ~ organization(X7,X5)
| ~ complexity(X3,X8,X5)
| ~ complexity(X7,X9,X5)
| ~ class(X7,X4,X5)
| ~ reorganization(X3,X5,X2)
| ~ reorganization(X7,X5,X1)
| ~ reorganization_type(X7,X6,X5)
| ~ greater(X9,X8)
| ~ organization(X7,X1) ),
inference(rename_variables,[],[i_0_34]) ).
cnf(i_0_4846,plain,
( class(X1,esk3_8(X2,X3,X4,esk14_0,X5,X6,X7,X8),esk4_8(X9,X10,esk14_0,X11,X12,X13,X14,X15))
| ~ class(X1,esk3_8(X2,X3,X4,esk16_0,X5,X6,X7,X8),esk4_8(X9,X10,esk16_0,X11,X12,X13,X14,X15)) ),
inference(scs_inference,[],[i_0_42,i_0_4709,i_0_4789,i_0_4821,i_0_4694,i_0_4833,i_0_4762,i_0_4715,i_0_47,i_0_4721,i_0_43,i_0_45,i_0_44,i_0_46,i_0_50,i_0_49,i_0_60,i_0_113,i_0_62,i_0_107,i_0_59,i_0_63,i_0_96,i_0_35,i_0_55,i_0_56,i_0_67,i_0_93,i_0_34,i_0_4777]) ).
cnf(i_0_4847,plain,
( class(esk3_8(X1,X2,esk14_0,X3,X4,X5,X6,X7),esk3_8(X8,X9,X10,esk14_0,X11,X12,X13,X14),esk4_8(X15,X16,esk14_0,X17,X18,X19,X20,X21))
| ~ class(esk3_8(X1,X2,esk16_0,X3,X4,X5,X6,X7),esk3_8(X8,X9,X10,esk16_0,X11,X12,X13,X14),esk4_8(X15,X16,esk14_0,X17,X18,X19,X20,X21))
| organization(esk3_8(X1,X2,esk14_0,X3,X4,X5,X6,X7),esk3_8(X1,X2,esk14_0,X3,X4,X5,X6,X7)) ),
inference(scs_inference,[],[i_0_42,i_0_4709,i_0_4789,i_0_4821,i_0_4694,i_0_4833,i_0_4762,i_0_4715,i_0_47,i_0_4721,i_0_43,i_0_45,i_0_44,i_0_46,i_0_50,i_0_49,i_0_60,i_0_113,i_0_62,i_0_107,i_0_59,i_0_63,i_0_96,i_0_35,i_0_55,i_0_56,i_0_67,i_0_93,i_0_34,i_0_4777,i_0_4831]) ).
cnf(i_0_4848,plain,
~ reorganization_free(esk6_0,esk16_0,esk17_0),
inference(scs_inference,[],[i_0_4838,i_0_4782,i_0_4789,i_0_4716,i_0_59,i_0_137,i_0_36]) ).
cnf(i_0_4849,plain,
( ~ greater(X1,X2)
| ~ survival_chance(X3,X4,X2)
| greater(X5,X4)
| ~ organization(X3,X2)
| ~ organization(X3,X1)
| ~ survival_chance(X3,X5,X1)
| ~ reorganization_free(X3,X2,X1) ),
inference(rename_variables,[],[i_0_36]) ).
cnf(i_0_4850,plain,
( ~ organization(esk5_0,esk16_0)
| ~ survival_chance(esk5_0,esk10_0,esk17_0) ),
inference(scs_inference,[],[i_0_4838,i_0_4782,i_0_4789,i_0_4707,i_0_4716,i_0_59,i_0_137,i_0_36,i_0_2545]) ).
cnf(i_0_4851,plain,
( ~ survival_chance(esk5_0,X1,esk16_0)
| ~ organization(esk5_0,esk16_0)
| ~ survival_chance(esk5_0,X1,esk17_0) ),
inference(rename_variables,[],[i_0_2545]) ).
cnf(i_0_4852,plain,
( class(X1,X2,esk3_8(X3,X4,X5,X6,esk14_0,X7,X8,X9))
| ~ class(X1,X2,esk3_8(X3,X4,X5,X6,esk16_0,X7,X8,X9)) ),
inference(scs_inference,[],[i_0_4838,i_0_4695,i_0_4782,i_0_4789,i_0_4707,i_0_4716,i_0_59,i_0_137,i_0_36,i_0_2545,i_0_94]) ).
cnf(i_0_4853,plain,
~ greater(esk3_8(esk16_0,X1,X2,X3,X4,esk14_0,X5,X6),esk3_8(esk14_0,X1,X2,X3,X4,esk16_0,X5,X6)),
inference(scs_inference,[],[i_0_4696,i_0_4819,i_0_89]) ).
cnf(i_0_4854,plain,
esk3_8(X1,X2,X3,X4,X5,esk16_0,X6,X7) = esk3_8(X1,X2,X3,X4,X5,esk14_0,X6,X7),
inference(rename_variables,[],[i_0_4696]) ).
cnf(i_0_4855,plain,
~ greater(esk3_8(esk16_0,X1,X2,X3,X4,X5,X6,X7),esk3_8(esk14_0,X1,X2,X3,X4,X5,X6,X7)),
inference(rename_variables,[],[i_0_4819]) ).
cnf(i_0_4856,plain,
~ reorganization_free(esk6_0,esk15_0,esk14_0),
inference(scs_inference,[],[i_0_4696,i_0_4819,i_0_4800,i_0_4776,i_0_4699,i_0_4711,i_0_4721,i_0_60,i_0_89,i_0_36]) ).
cnf(i_0_4857,plain,
( ~ survival_chance(X1,X2,X3)
| greater(X4,X2)
| ~ organization(X1,X3)
| ~ organization(X1,X5)
| ~ survival_chance(X1,X4,X5)
| ~ greater(X5,X3)
| ~ reorganization_free(X1,X3,X5) ),
inference(rename_variables,[],[i_0_36]) ).
cnf(i_0_4858,plain,
( reorganization_type(esk3_8(X1,X2,X3,X4,X5,esk14_0,X6,X7),X8,X9)
| ~ reorganization_type(esk3_8(X1,X2,X3,X4,X5,esk16_0,X6,X7),X8,X9) ),
inference(scs_inference,[],[i_0_4696,i_0_4854,i_0_4819,i_0_4800,i_0_4776,i_0_4699,i_0_4711,i_0_4721,i_0_60,i_0_89,i_0_36,i_0_98]) ).
cnf(i_0_4859,plain,
( reorganization_type(esk3_8(X1,X2,X3,X4,X5,esk14_0,X6,X7),X8,esk3_8(X1,X2,X3,X4,X5,esk14_0,X6,X7))
| ~ reorganization_type(esk3_8(X1,X2,X3,X4,X5,esk16_0,X6,X7),X8,esk3_8(X1,X2,X3,X4,X5,esk16_0,X6,X7)) ),
inference(scs_inference,[],[i_0_4696,i_0_4854,i_0_4819,i_0_4800,i_0_4776,i_0_4699,i_0_4711,i_0_4721,i_0_60,i_0_89,i_0_36,i_0_98,i_0_100]) ).
cnf(i_0_4860,plain,
( reorganization_type(esk3_8(X1,X2,X3,X4,X5,esk14_0,X6,X7),X8,esk3_8(X1,X2,X3,X4,X5,esk14_0,X6,X7))
| ~ reorganization_free(esk6_0,esk15_0,esk16_0) ),
inference(scs_inference,[],[i_0_4696,i_0_4854,i_0_4819,i_0_4800,i_0_4776,i_0_4699,i_0_4711,i_0_4721,i_0_115,i_0_60,i_0_89,i_0_36,i_0_98,i_0_100,i_0_106]) ).
cnf(i_0_4861,plain,
( reorganization_type(esk3_8(X1,X2,X3,X4,X5,esk14_0,X6,X7),esk3_8(X1,X2,X3,X4,X5,esk14_0,X6,X7),esk3_8(X1,X2,X3,X4,X5,esk14_0,X6,X7))
| ~ reorganization_type(esk3_8(X1,X2,X3,X4,X5,esk16_0,X6,X7),esk3_8(X1,X2,X3,X4,X5,esk16_0,X6,X7),esk3_8(X1,X2,X3,X4,X5,esk14_0,X6,X7)) ),
inference(scs_inference,[],[i_0_4696,i_0_4854,i_0_4819,i_0_4800,i_0_4776,i_0_4699,i_0_4711,i_0_4721,i_0_115,i_0_60,i_0_89,i_0_36,i_0_98,i_0_100,i_0_106,i_0_99]) ).
cnf(i_0_4862,plain,
( reorganization_type(esk3_8(X1,X2,X3,X4,X5,esk14_0,X6,X7),esk3_8(X1,X2,X3,X4,X5,esk14_0,X6,X7),esk3_8(X1,X2,X3,X4,X5,esk14_0,X6,X7))
| reorganization_free(esk3_8(X1,X2,X3,X4,X5,esk14_0,X6,X7),X8,X9)
| ~ reorganization_free(esk3_8(X1,X2,X3,X4,X5,esk16_0,X6,X7),X8,X9) ),
inference(scs_inference,[],[i_0_4696,i_0_4854,i_0_4819,i_0_4800,i_0_4776,i_0_4699,i_0_4711,i_0_4721,i_0_115,i_0_60,i_0_89,i_0_36,i_0_98,i_0_100,i_0_106,i_0_99,i_0_104]) ).
cnf(i_0_4863,plain,
esk3_8(X1,X2,X3,X4,X5,X6,esk16_0,esk16_0) = esk3_8(X1,X2,X3,X4,X5,X6,esk14_0,esk14_0),
inference(scs_inference,[],[i_0_4697,i_0_4698,i_0_68]) ).
cnf(i_0_4864,plain,
esk3_8(X1,X2,X3,X4,X5,X6,esk16_0,X7) = esk3_8(X1,X2,X3,X4,X5,X6,esk14_0,X7),
inference(rename_variables,[],[i_0_4697]) ).
cnf(i_0_4865,plain,
esk3_8(X1,X2,X3,X4,X5,X6,X7,esk16_0) = esk3_8(X1,X2,X3,X4,X5,X6,X7,esk14_0),
inference(rename_variables,[],[i_0_4698]) ).
cnf(i_0_4866,plain,
( survival_chance(X1,esk1_2(esk5_0,esk15_0),esk15_0)
| esk5_0 != X1 ),
inference(scs_inference,[],[i_0_4779,i_0_4697,i_0_4698,i_0_68,i_0_85]) ).
cnf(i_0_4867,plain,
( X1 != esk5_0
| survival_chance(X1,esk1_2(esk5_0,esk15_0),esk15_0) ),
inference(scs_inference,[],[i_0_4779,i_0_4697,i_0_4698,i_0_68,i_0_85,i_0_67]) ).
cnf(i_0_4868,plain,
( survival_chance(X1,esk1_2(esk5_0,esk15_0),esk15_0)
| reorganization_free(X2,esk3_8(X3,X4,X5,X6,X7,X8,esk14_0,X9),X10)
| ~ reorganization_free(X2,esk3_8(X3,X4,X5,X6,X7,X8,esk16_0,X9),X10) ),
inference(scs_inference,[],[i_0_4779,i_0_4697,i_0_4864,i_0_4698,i_0_68,i_0_85,i_0_67,i_0_105]) ).
cnf(i_0_4869,plain,
survival_chance(esk5_0,esk1_2(esk5_0,esk15_0),esk15_0),
inference(equality_inference,[],[4866]) ).
cnf(i_0_4870,plain,
survival_chance(esk5_0,esk1_2(esk5_0,esk15_0),esk15_0),
inference(equality_inference,[],[4867]) ).
cnf(i_0_4871,plain,
~ greater(esk4_8(esk14_0,X1,esk14_0,X2,X3,esk14_0,X4,X5),esk4_8(esk16_0,X1,esk16_0,X2,X3,esk16_0,X4,X5)),
inference(scs_inference,[],[i_0_4728,i_0_4794,i_0_88]) ).
cnf(i_0_4872,plain,
esk4_8(esk14_0,X1,X2,X3,X4,X5,X6,X7) = esk4_8(esk16_0,X1,X2,X3,X4,X5,X6,X7),
inference(rename_variables,[],[i_0_4728]) ).
cnf(i_0_4873,plain,
~ greater(esk4_8(X1,X2,esk14_0,X3,X4,esk14_0,X5,X6),esk4_8(X1,X2,esk16_0,X3,X4,esk16_0,X5,X6)),
inference(rename_variables,[],[i_0_4794]) ).
cnf(i_0_4874,plain,
~ reorganization(X1,esk4_8(esk16_0,esk16_0,esk16_0,X2,X3,X4,X5,X6),esk4_8(esk14_0,esk14_0,esk14_0,X2,X3,X4,X5,X6)),
inference(scs_inference,[],[i_0_4728,i_0_4729,i_0_4767,i_0_4794,i_0_88,i_0_97]) ).
cnf(i_0_4875,plain,
esk4_8(X1,esk14_0,X2,X3,X4,X5,X6,X7) = esk4_8(X1,esk16_0,X2,X3,X4,X5,X6,X7),
inference(rename_variables,[],[i_0_4729]) ).
cnf(i_0_4876,plain,
~ reorganization(X1,esk4_8(esk16_0,X2,esk16_0,X3,X4,X5,X6,X7),esk4_8(esk14_0,X2,esk14_0,X3,X4,X5,X6,X7)),
inference(rename_variables,[],[i_0_4767]) ).
cnf(i_0_4877,plain,
( survival_chance(esk5_0,X1,esk17_0)
| esk1_2(esk5_0,esk17_0) != X1 ),
inference(scs_inference,[],[i_0_4808,i_0_4728,i_0_4729,i_0_4767,i_0_4794,i_0_88,i_0_97,i_0_86]) ).
cnf(i_0_4878,plain,
( esk1_2(esk5_0,esk17_0) != esk16_0
| survival_chance(esk5_0,esk14_0,esk17_0) ),
inference(scs_inference,[],[i_0_4808,i_0_4728,i_0_4729,i_0_4767,i_0_4794,i_0_88,i_0_97,i_0_86,i_0_4722]) ).
cnf(i_0_4879,plain,
( greater(X1,X2)
| ~ greater(X1,X3)
| ~ greater(X3,X2) ),
inference(rename_variables,[],[i_0_41]) ).
cnf(i_0_4880,plain,
( ~ greater(X1,esk17_0)
| esk1_2(esk5_0,esk17_0) != esk16_0
| ~ greater(esk15_0,X1) ),
inference(scs_inference,[],[i_0_4747,i_0_4808,i_0_4728,i_0_4729,i_0_4767,i_0_4794,i_0_88,i_0_97,i_0_86,i_0_4722,i_0_41]) ).
cnf(i_0_4881,plain,
survival_chance(esk5_0,esk1_2(esk5_0,esk17_0),esk17_0),
inference(equality_inference,[],[4877]) ).
cnf(i_0_4882,plain,
( organization(X1,esk14_0)
| esk6_0 != X1 ),
inference(scs_inference,[],[i_0_4721,i_0_90]) ).
cnf(i_0_4883,plain,
( organization(esk4_8(X1,X2,esk16_0,X3,X4,X5,X6,X7),esk14_0)
| esk6_0 != esk4_8(X1,X2,esk14_0,X3,X4,X5,X6,X7) ),
inference(scs_inference,[],[i_0_4730,i_0_4721,i_0_90,i_0_68]) ).
cnf(i_0_4884,plain,
( esk4_8(X1,X2,esk16_0,X3,X4,X5,X6,X7) != esk6_0
| organization(esk4_8(X1,X2,esk16_0,X3,X4,X5,X6,X7),esk14_0) ),
inference(scs_inference,[],[i_0_4730,i_0_4721,i_0_90,i_0_68,i_0_67]) ).
cnf(i_0_4885,plain,
( ~ survival_chance(esk5_0,X1,esk16_0)
| ~ organization(esk5_0,esk16_0)
| ~ survival_chance(esk5_0,X1,esk17_0) ),
inference(rename_variables,[],[i_0_2545]) ).
cnf(i_0_4887,plain,
organization(esk6_0,esk14_0),
inference(equality_inference,[],[4882]) ).
cnf(i_0_4888,plain,
esk4_8(X1,X2,X3,esk14_0,esk14_0,X4,X5,X6) = esk4_8(X1,X2,X3,esk16_0,esk16_0,X4,X5,X6),
inference(scs_inference,[],[i_0_4731,i_0_4732,i_0_68]) ).
cnf(i_0_4889,plain,
esk4_8(X1,X2,X3,esk14_0,X4,X5,X6,X7) = esk4_8(X1,X2,X3,esk16_0,X4,X5,X6,X7),
inference(rename_variables,[],[i_0_4731]) ).
cnf(i_0_4890,plain,
esk4_8(X1,X2,X3,X4,esk14_0,X5,X6,X7) = esk4_8(X1,X2,X3,X4,esk16_0,X5,X6,X7),
inference(rename_variables,[],[i_0_4732]) ).
cnf(i_0_4891,plain,
~ reorganization(X1,esk4_8(esk16_0,esk16_0,esk16_0,esk14_0,X2,X3,X4,X5),esk4_8(esk14_0,esk14_0,esk14_0,esk16_0,X2,X3,X4,X5)),
inference(scs_inference,[],[i_0_4731,i_0_4889,i_0_4732,i_0_4874,i_0_68,i_0_96]) ).
cnf(i_0_4892,plain,
esk4_8(X1,X2,X3,esk14_0,X4,X5,X6,X7) = esk4_8(X1,X2,X3,esk16_0,X4,X5,X6,X7),
inference(rename_variables,[],[i_0_4731]) ).
cnf(i_0_4893,plain,
~ reorganization(X1,esk4_8(esk16_0,esk16_0,esk16_0,X2,X3,X4,X5,X6),esk4_8(esk14_0,esk14_0,esk14_0,X2,X3,X4,X5,X6)),
inference(rename_variables,[],[i_0_4874]) ).
cnf(i_0_4894,plain,
( class(X1,esk8_0,esk15_0)
| esk5_0 != X1 ),
inference(scs_inference,[],[i_0_4731,i_0_4889,i_0_4732,i_0_4874,i_0_47,i_0_68,i_0_96,i_0_92]) ).
cnf(i_0_4895,plain,
( X1 != esk5_0
| class(X1,esk8_0,esk15_0) ),
inference(scs_inference,[],[i_0_4731,i_0_4889,i_0_4732,i_0_4874,i_0_47,i_0_68,i_0_96,i_0_92,i_0_67]) ).
cnf(i_0_4896,plain,
( class(X1,esk8_0,esk15_0)
| class(X2,esk4_8(X3,X4,X5,esk16_0,X6,X7,X8,X9),X10)
| ~ class(X2,esk4_8(X3,X4,X5,esk14_0,X6,X7,X8,X9),X10) ),
inference(scs_inference,[],[i_0_4731,i_0_4889,i_0_4892,i_0_4732,i_0_4874,i_0_47,i_0_68,i_0_96,i_0_92,i_0_67,i_0_93]) ).
cnf(i_0_4897,plain,
class(esk5_0,esk8_0,esk15_0),
inference(equality_inference,[],[4894]) ).
cnf(i_0_4898,plain,
class(esk5_0,esk8_0,esk15_0),
inference(equality_inference,[],[4895]) ).
cnf(i_0_4899,plain,
( class(esk5_0,esk8_0,X1)
| esk15_0 != X1 ),
inference(scs_inference,[],[i_0_47,i_0_94]) ).
cnf(i_0_4900,plain,
( class(esk5_0,esk8_0,esk4_8(X1,X2,X3,X4,X5,esk16_0,X6,X7))
| esk15_0 != esk4_8(X1,X2,X3,X4,X5,esk14_0,X6,X7) ),
inference(scs_inference,[],[i_0_4733,i_0_47,i_0_94,i_0_68]) ).
cnf(i_0_4901,plain,
( esk4_8(X1,X2,X3,X4,X5,esk16_0,X6,X7) != esk15_0
| class(esk5_0,esk8_0,esk4_8(X1,X2,X3,X4,X5,esk16_0,X6,X7)) ),
inference(scs_inference,[],[i_0_4733,i_0_47,i_0_94,i_0_68,i_0_67]) ).
cnf(i_0_4902,plain,
( class(esk5_0,esk8_0,esk4_8(X1,X2,X3,X4,X5,esk16_0,X6,X7))
| reorganization_type(esk4_8(X1,X2,X3,X4,X5,esk16_0,X6,X7),X8,X9)
| ~ reorganization_type(esk4_8(X1,X2,X3,X4,X5,esk14_0,X6,X7),X8,X9) ),
inference(scs_inference,[],[i_0_4733,i_0_47,i_0_94,i_0_68,i_0_67,i_0_98]) ).
cnf(i_0_4903,plain,
class(esk5_0,esk8_0,esk15_0),
inference(equality_inference,[],[4899]) ).
cnf(i_0_4904,plain,
~ reorganization_free(esk6_0,esk15_0,esk16_0),
inference(scs_inference,[],[i_0_4856,i_0_115,i_0_106]) ).
cnf(i_0_4905,plain,
esk4_8(X1,X2,X3,X4,X5,X6,esk14_0,esk14_0) = esk4_8(X1,X2,X3,X4,X5,X6,esk16_0,esk16_0),
inference(scs_inference,[],[i_0_4856,i_0_4734,i_0_4735,i_0_115,i_0_106,i_0_68]) ).
cnf(i_0_4906,plain,
esk4_8(X1,X2,X3,X4,X5,X6,esk14_0,X7) = esk4_8(X1,X2,X3,X4,X5,X6,esk16_0,X7),
inference(rename_variables,[],[i_0_4734]) ).
cnf(i_0_4907,plain,
esk4_8(X1,X2,X3,X4,X5,X6,X7,esk14_0) = esk4_8(X1,X2,X3,X4,X5,X6,X7,esk16_0),
inference(rename_variables,[],[i_0_4735]) ).
cnf(i_0_4908,plain,
~ greater(esk4_8(esk14_0,X1,esk14_0,X2,X3,esk14_0,esk16_0,X4),esk4_8(esk16_0,X1,esk16_0,X2,X3,esk16_0,esk14_0,X4)),
inference(scs_inference,[],[i_0_4856,i_0_4734,i_0_4906,i_0_4735,i_0_4871,i_0_115,i_0_106,i_0_68,i_0_89]) ).
cnf(i_0_4909,plain,
esk4_8(X1,X2,X3,X4,X5,X6,esk14_0,X7) = esk4_8(X1,X2,X3,X4,X5,X6,esk16_0,X7),
inference(rename_variables,[],[i_0_4734]) ).
cnf(i_0_4910,plain,
~ greater(esk4_8(esk14_0,X1,esk14_0,X2,X3,esk14_0,X4,X5),esk4_8(esk16_0,X1,esk16_0,X2,X3,esk16_0,X4,X5)),
inference(rename_variables,[],[i_0_4871]) ).
cnf(i_0_4911,plain,
( reorganization_type(esk5_0,X1,esk15_0)
| esk7_0 != X1 ),
inference(scs_inference,[],[i_0_4856,i_0_4734,i_0_4906,i_0_4735,i_0_4871,i_0_45,i_0_115,i_0_106,i_0_68,i_0_89,i_0_99]) ).
cnf(i_0_4912,plain,
~ organization(esk5_0,esk16_0),
inference(scs_inference,[],[i_0_42,i_0_4856,i_0_4734,i_0_4906,i_0_4735,i_0_4871,i_0_4753,i_0_64,i_0_52,i_0_54,i_0_43,i_0_45,i_0_44,i_0_4707,i_0_4716,i_0_47,i_0_46,i_0_50,i_0_49,i_0_115,i_0_60,i_0_62,i_0_57,i_0_63,i_0_106,i_0_68,i_0_89,i_0_99,i_0_33]) ).
cnf(i_0_4913,plain,
( ~ reorganization_type(X1,X2,X3)
| ~ complexity(X1,X4,X3)
| ~ complexity(X5,X6,X3)
| ~ organization(X5,X7)
| ~ class(X5,X8,X3)
| ~ survival_chance(X5,X9,X3)
| ~ reorganization(X1,X3,X7)
| ~ reorganization_type(X5,X2,X3)
| ~ survival_chance(X1,X10,X7)
| ~ survival_chance(X5,X11,X7)
| ~ greater(X6,X4)
| greater(X10,X11)
| ~ organization(X1,X3)
| ~ class(X1,X8,X3)
| ~ organization(X5,X3)
| ~ survival_chance(X1,X9,X3)
| ~ reorganization(X5,X3,X12)
| ~ organization(X1,X7)
| X10 = X11 ),
inference(rename_variables,[],[i_0_33]) ).
cnf(i_0_4914,plain,
( esk7_0 != esk4_8(X1,X2,X3,X4,esk16_0,X5,X6,X7)
| reorganization_type(esk5_0,esk4_8(X1,X2,X3,X4,esk14_0,X5,X6,X7),esk15_0)
| reorganization_type(esk4_8(X1,X2,X3,X4,esk14_0,X5,X6,X7),esk7_0,esk15_0) ),
inference(scs_inference,[],[i_0_42,i_0_4856,i_0_4734,i_0_4906,i_0_4735,i_0_4871,i_0_4753,i_0_64,i_0_52,i_0_54,i_0_43,i_0_45,i_0_44,i_0_4707,i_0_4716,i_0_47,i_0_46,i_0_50,i_0_49,i_0_115,i_0_60,i_0_62,i_0_57,i_0_63,i_0_106,i_0_68,i_0_89,i_0_99,i_0_33,i_0_4787]) ).
cnf(i_0_4915,plain,
reorganization_type(esk5_0,esk7_0,esk15_0),
inference(equality_inference,[],[4911]) ).
cnf(i_0_4916,plain,
( reorganization_type(esk6_0,esk7_0,X1)
| esk15_0 != X1 ),
inference(scs_inference,[],[i_0_44,i_0_100]) ).
cnf(i_0_4917,plain,
( reorganization_type(esk6_0,esk7_0,esk3_8(esk16_0,X1,X2,X3,X4,X5,X6,X7))
| esk15_0 != esk3_8(esk14_0,X1,X2,X3,X4,X5,X6,X7) ),
inference(scs_inference,[],[i_0_4736,i_0_44,i_0_100,i_0_68]) ).
cnf(i_0_4918,plain,
( esk3_8(esk16_0,X1,X2,X3,X4,X5,X6,X7) != esk15_0
| reorganization_type(esk6_0,esk7_0,esk3_8(esk16_0,X1,X2,X3,X4,X5,X6,X7)) ),
inference(scs_inference,[],[i_0_4736,i_0_44,i_0_100,i_0_68,i_0_67]) ).
cnf(i_0_4919,plain,
( greater(X1,X2)
| ~ greater(X1,X3)
| ~ greater(X3,X2) ),
inference(rename_variables,[],[i_0_41]) ).
cnf(i_0_4920,plain,
( reorganization_type(esk6_0,esk7_0,esk3_8(esk16_0,X1,X2,X3,X4,X5,X6,X7))
| ~ greater(X8,esk3_8(esk14_0,X9,X10,X11,X12,esk16_0,X13,X14))
| ~ greater(esk3_8(esk16_0,X9,X10,X11,X12,esk14_0,X13,X14),X8) ),
inference(scs_inference,[],[i_0_4736,i_0_4853,i_0_44,i_0_100,i_0_68,i_0_67,i_0_41]) ).
cnf(i_0_4921,plain,
reorganization_type(esk6_0,esk7_0,esk15_0),
inference(equality_inference,[],[4916]) ).
cnf(i_0_4922,plain,
~ greater(esk3_8(esk16_0,esk14_0,X1,X2,X3,X4,X5,X6),esk3_8(esk14_0,esk16_0,X1,X2,X3,X4,X5,X6)),
inference(scs_inference,[],[i_0_4737,i_0_4819,i_0_88]) ).
cnf(i_0_4923,plain,
esk3_8(X1,esk14_0,X2,X3,X4,X5,X6,X7) = esk3_8(X1,esk16_0,X2,X3,X4,X5,X6,X7),
inference(rename_variables,[],[i_0_4737]) ).
cnf(i_0_4924,plain,
~ greater(esk3_8(esk16_0,X1,X2,X3,X4,X5,X6,X7),esk3_8(esk14_0,X1,X2,X3,X4,X5,X6,X7)),
inference(rename_variables,[],[i_0_4819]) ).
cnf(i_0_4925,plain,
~ reorganization(X1,esk3_8(esk14_0,esk16_0,X2,esk16_0,X3,X4,X5,X6),esk3_8(esk16_0,esk14_0,X2,esk14_0,X3,X4,X5,X6)),
inference(scs_inference,[],[i_0_4737,i_0_4923,i_0_4832,i_0_4819,i_0_88,i_0_97]) ).
cnf(i_0_4926,plain,
esk3_8(X1,esk14_0,X2,X3,X4,X5,X6,X7) = esk3_8(X1,esk16_0,X2,X3,X4,X5,X6,X7),
inference(rename_variables,[],[i_0_4737]) ).
cnf(i_0_4927,plain,
~ reorganization(X1,esk3_8(esk14_0,X2,X3,esk16_0,X4,X5,X6,X7),esk3_8(esk16_0,X2,X3,esk14_0,X4,X5,X6,X7)),
inference(rename_variables,[],[i_0_4832]) ).
cnf(i_0_4928,plain,
esk3_8(X1,esk14_0,esk14_0,X2,X3,X4,X5,X6) = esk3_8(X1,esk16_0,esk16_0,X2,X3,X4,X5,X6),
inference(scs_inference,[],[i_0_4737,i_0_4923,i_0_4926,i_0_4738,i_0_4832,i_0_4819,i_0_88,i_0_97,i_0_68]) ).
cnf(i_0_4929,plain,
esk3_8(X1,esk14_0,X2,X3,X4,X5,X6,X7) = esk3_8(X1,esk16_0,X2,X3,X4,X5,X6,X7),
inference(rename_variables,[],[i_0_4737]) ).
cnf(i_0_4930,plain,
esk3_8(X1,X2,esk14_0,X3,X4,X5,X6,X7) = esk3_8(X1,X2,esk16_0,X3,X4,X5,X6,X7),
inference(rename_variables,[],[i_0_4738]) ).
cnf(i_0_4931,plain,
$false,
inference(scs_inference,[],[i_0_4737,i_0_4923,i_0_4926,i_0_4738,i_0_4832,i_0_4912,i_0_4819,i_0_4704,i_0_62,i_0_61,i_0_137,i_0_88,i_0_97,i_0_68,i_0_38]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.11 % Problem : MGT005+2 : TPTP v9.2.1. Bugfixed v3.2.0.
% 0.00/0.11 % Command : /export/starexec/sandbox2/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox2/solver/bin/cse --final-prover /export/starexec/sandbox2/solver/bin/eprover --proof-time %d --global-time-limit %d
% 0.14/0.32 % Computer : n004.cluster.edu
% 0.14/0.32 % Model : x86_64 x86_64
% 0.14/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.32 % Memory : 8042.1875MB
% 0.14/0.32 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.32 % CPULimit : 300
% 0.14/0.32 % WCLimit : 300
% 0.14/0.32 % DateTime : Mon May 4 23:25:47 EDT 2026
% 0.14/0.33 % CPUTime :
% 0.14/0.34 % start to proof: theBenchmark
% 56.72/30.67 % Version : CSE_E---1.7
% 56.72/30.67 % Problem : theBenchmark.p
% 56.72/30.67 % SZS status Theorem for theBenchmark.p
% 56.72/30.67 % SZS output start CNFRefutation
% See solution above
% 58.27/31.47 % Total time : 30.333s
%------------------------------------------------------------------------------