%------------------------------------------------------------------------------
% File : CSI_E---1.1
% Problem : MGT005+2 : TPTP v9.3.0. Bugfixed v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar mcs_scs.jar %d %s
% Computer : n005.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 8 06:04:27 AM UTC 2026
% Result : Theorem 249.41s 36.89s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : MGT005+2 : TPTP v9.3.0. Bugfixed v3.2.0.
% 0.00/0.02 % Command : java -jar mcs_scs.jar %d %s
% 0.08/0.33 % Computer : n005.cluster.edu
% 0.08/0.33 % Model : x86_64 x86_64
% 0.08/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.33 % Memory : 8046.5625MB
% 0.08/0.33 % OS : Linux 6.8.0-71-generic
% 0.08/0.33 % CPULimit : 300
% 0.08/0.33 % WCLimit : 300
% 0.08/0.33 % DateTime : Mon Sep 7 11:39:50 UTC 2026
% 0.08/0.33 % CPUTime :
% 0.13/0.45 start to proof:theBenchmark.p
% 249.41/36.89 % Version : CSI_E---1.1
% 249.41/36.89 % Problem : theBenchmark.p
% 249.41/36.89 % Proof found!
% 249.41/36.89 % SZS status Theorem for theBenchmark.p
% 249.41/36.89 % SZS output start Proof
% 249.41/36.89 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)).
% 249.41/36.89 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)).
% 249.41/36.89 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)).
% 249.41/36.89 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)).
% 249.41/36.89 fof(mp7, axiom, ![X1, X10, X11]:((reorganization(X1,X10,X11)=>greater(X11,X10))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', mp7)).
% 249.41/36.89 fof(c_0_5, 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])).
% 249.41/36.89 fof(c_0_6, hypothesis, ![X67, X68, X69, X70, X71, X72, X73, X74, X75, X76, X77, X78]:((~organization(X67,X76)|~organization(X68,X76)|~organization(X67,X77)|~organization(X68,X77)|~class(X67,X70,X76)|~class(X68,X70,X76)|~survival_chance(X67,X71,X76)|~survival_chance(X68,X71,X76)|~reorganization(X67,X76,X77)|~reorganization(X68,X76,X78)|~reorganization_type(X67,X69,X76)|~reorganization_type(X68,X69,X76)|~survival_chance(X67,X72,X77)|~survival_chance(X68,X73,X77)|~complexity(X67,X74,X76)|~complexity(X68,X75,X76)|~greater(X75,X74)|(greater(X72,X73)|X72=X73))), inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[a11_FOL])])])).
% 249.41/36.89 fof(c_0_7, 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(fof_nnf,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_5])])])])).
% 249.41/36.89 fof(c_0_8, hypothesis, ![X58, X59, X60, X61, X62, X63, X64, X65, X66]:((~organization(X58,X64)|~organization(X59,X64)|~organization(X59,X66)|~class(X58,X61,X64)|~class(X59,X61,X64)|~reorganization(X58,X64,X65)|~reorganization(X59,X64,X66)|~reorganization_type(X58,X60,X64)|~reorganization_type(X59,X60,X64)|~complexity(X58,X62,X64)|~complexity(X59,X63,X64)|~greater(X63,X62)|greater(X66,X65))), inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[a10_FOL])])])).
% 249.41/36.89 cnf(c_0_9, 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)],[c_0_6])).
% 249.41/36.89 cnf(c_0_10, negated_conjecture, (complexity(esk6_0,esk13_0,esk15_0)), inference(split_conjunct,[status(thm)],[c_0_7])).
% 249.41/36.89 cnf(c_0_11, negated_conjecture, (organization(esk6_0,esk15_0)), inference(split_conjunct,[status(thm)],[c_0_7])).
% 249.41/36.89 cnf(c_0_12, 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)],[c_0_8])).
% 249.41/36.89 cnf(c_0_13, negated_conjecture, (X1=X2|greater(X1,X2)|~complexity(X3,X4,esk15_0)|~reorganization_type(esk6_0,X5,esk15_0)|~reorganization_type(X3,X5,esk15_0)|~class(esk6_0,X6,esk15_0)|~class(X3,X6,esk15_0)|~reorganization(esk6_0,esk15_0,X7)|~reorganization(X3,esk15_0,X8)|~organization(esk6_0,X8)|~organization(X3,esk15_0)|~organization(X3,X8)|~survival_chance(esk6_0,X9,esk15_0)|~survival_chance(esk6_0,X2,X8)|~survival_chance(X3,X9,esk15_0)|~survival_chance(X3,X1,X8)|~greater(esk13_0,X4)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_9, c_0_10]), c_0_11])])).
% 249.41/36.89 cnf(c_0_14, negated_conjecture, (reorganization_type(esk6_0,esk7_0,esk15_0)), inference(split_conjunct,[status(thm)],[c_0_7])).
% 249.41/36.89 cnf(c_0_15, negated_conjecture, (greater(X1,X2)|~complexity(X3,X4,esk15_0)|~reorganization_type(esk6_0,X5,esk15_0)|~reorganization_type(X3,X5,esk15_0)|~class(esk6_0,X6,esk15_0)|~class(X3,X6,esk15_0)|~reorganization(esk6_0,esk15_0,X1)|~reorganization(X3,esk15_0,X2)|~organization(esk6_0,X1)|~organization(X3,esk15_0)|~greater(esk13_0,X4)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_12, c_0_10]), c_0_11])])).
% 249.41/36.89 cnf(c_0_16, negated_conjecture, (X1=X2|greater(X1,X2)|~complexity(X3,X4,esk15_0)|~reorganization_type(X3,esk7_0,esk15_0)|~class(esk6_0,X5,esk15_0)|~class(X3,X5,esk15_0)|~reorganization(esk6_0,esk15_0,X6)|~reorganization(X3,esk15_0,X7)|~organization(esk6_0,X7)|~organization(X3,esk15_0)|~organization(X3,X7)|~survival_chance(esk6_0,X8,esk15_0)|~survival_chance(esk6_0,X2,X7)|~survival_chance(X3,X8,esk15_0)|~survival_chance(X3,X1,X7)|~greater(esk13_0,X4)), inference(spm,[status(thm)],[c_0_13, c_0_14])).
% 249.41/36.89 cnf(c_0_17, negated_conjecture, (reorganization_type(esk5_0,esk7_0,esk15_0)), inference(split_conjunct,[status(thm)],[c_0_7])).
% 249.41/36.89 cnf(c_0_18, negated_conjecture, (organization(esk5_0,esk15_0)), inference(split_conjunct,[status(thm)],[c_0_7])).
% 249.41/36.89 cnf(c_0_19, negated_conjecture, (greater(X1,X2)|~complexity(X3,X4,esk15_0)|~reorganization_type(X3,esk7_0,esk15_0)|~class(esk6_0,X5,esk15_0)|~class(X3,X5,esk15_0)|~reorganization(esk6_0,esk15_0,X1)|~reorganization(X3,esk15_0,X2)|~organization(esk6_0,X1)|~organization(X3,esk15_0)|~greater(esk13_0,X4)), inference(spm,[status(thm)],[c_0_15, c_0_14])).
% 249.41/36.89 cnf(c_0_20, negated_conjecture, (X1=X2|greater(X1,X2)|~complexity(esk5_0,X3,esk15_0)|~class(esk6_0,X4,esk15_0)|~class(esk5_0,X4,esk15_0)|~reorganization(esk6_0,esk15_0,X5)|~reorganization(esk5_0,esk15_0,X6)|~organization(esk6_0,X6)|~organization(esk5_0,X6)|~survival_chance(esk6_0,X7,esk15_0)|~survival_chance(esk5_0,X7,esk15_0)|~survival_chance(esk6_0,X2,X6)|~survival_chance(esk5_0,X1,X6)|~greater(esk13_0,X3)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_16, c_0_17]), c_0_18])])).
% 249.41/36.89 cnf(c_0_21, negated_conjecture, (complexity(esk5_0,esk12_0,esk15_0)), inference(split_conjunct,[status(thm)],[c_0_7])).
% 249.41/36.89 cnf(c_0_22, negated_conjecture, (greater(esk13_0,esk12_0)), inference(split_conjunct,[status(thm)],[c_0_7])).
% 249.41/36.89 cnf(c_0_23, negated_conjecture, (greater(X1,X2)|~complexity(esk5_0,X3,esk15_0)|~class(esk6_0,X4,esk15_0)|~class(esk5_0,X4,esk15_0)|~reorganization(esk6_0,esk15_0,X1)|~reorganization(esk5_0,esk15_0,X2)|~organization(esk6_0,X1)|~greater(esk13_0,X3)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_19, c_0_17]), c_0_18])])).
% 249.41/36.89 cnf(c_0_24, negated_conjecture, (X1=X2|greater(X1,X2)|~class(esk6_0,X3,esk15_0)|~class(esk5_0,X3,esk15_0)|~reorganization(esk6_0,esk15_0,X4)|~reorganization(esk5_0,esk15_0,X5)|~organization(esk6_0,X5)|~organization(esk5_0,X5)|~survival_chance(esk6_0,X6,esk15_0)|~survival_chance(esk5_0,X6,esk15_0)|~survival_chance(esk6_0,X2,X5)|~survival_chance(esk5_0,X1,X5)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_20, c_0_21]), c_0_22])])).
% 249.41/36.89 cnf(c_0_25, negated_conjecture, (class(esk6_0,esk8_0,esk15_0)), inference(split_conjunct,[status(thm)],[c_0_7])).
% 249.41/36.89 cnf(c_0_26, negated_conjecture, (class(esk5_0,esk8_0,esk15_0)), inference(split_conjunct,[status(thm)],[c_0_7])).
% 249.41/36.89 fof(c_0_27, plain, ![X39, X40, X41, X42]:((~organization(X39,X41)|~organization(X39,X42)|~greater(X40,X41)|~greater(X42,X40)|organization(X39,X40))), inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mp13])])])).
% 249.41/36.89 cnf(c_0_28, negated_conjecture, (greater(X1,X2)|~class(esk6_0,X3,esk15_0)|~class(esk5_0,X3,esk15_0)|~reorganization(esk6_0,esk15_0,X1)|~reorganization(esk5_0,esk15_0,X2)|~organization(esk6_0,X1)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_23, c_0_21]), c_0_22])])).
% 249.41/36.89 cnf(c_0_29, negated_conjecture, (X1=X2|greater(X1,X2)|~reorganization(esk6_0,esk15_0,X3)|~reorganization(esk5_0,esk15_0,X4)|~organization(esk6_0,X4)|~organization(esk5_0,X4)|~survival_chance(esk6_0,X5,esk15_0)|~survival_chance(esk5_0,X5,esk15_0)|~survival_chance(esk6_0,X2,X4)|~survival_chance(esk5_0,X1,X4)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_24, c_0_25]), c_0_26])])).
% 249.41/36.89 cnf(c_0_30, negated_conjecture, (reorganization(esk6_0,esk15_0,esk17_0)), inference(split_conjunct,[status(thm)],[c_0_7])).
% 249.41/36.89 cnf(c_0_31, negated_conjecture, (reorganization(esk5_0,esk15_0,esk16_0)), inference(split_conjunct,[status(thm)],[c_0_7])).
% 249.41/36.89 cnf(c_0_32, negated_conjecture, (esk14_0=esk16_0), inference(split_conjunct,[status(thm)],[c_0_7])).
% 249.41/36.89 cnf(c_0_33, plain, (organization(X1,X4)|~organization(X1,X2)|~organization(X1,X3)|~greater(X4,X2)|~greater(X3,X4)), inference(split_conjunct,[status(thm)],[c_0_27])).
% 249.41/36.89 cnf(c_0_34, negated_conjecture, (organization(esk6_0,esk17_0)), inference(split_conjunct,[status(thm)],[c_0_7])).
% 249.41/36.89 cnf(c_0_35, negated_conjecture, (greater(X1,X2)|~reorganization(esk6_0,esk15_0,X1)|~reorganization(esk5_0,esk15_0,X2)|~organization(esk6_0,X1)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_28, c_0_25]), c_0_26])])).
% 249.41/36.89 fof(c_0_36, plain, ![X43, X44, X45]:((~reorganization(X43,X44,X45)|greater(X45,X44))), inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mp7])])])).
% 249.41/36.89 cnf(c_0_37, negated_conjecture, (X1=X2|greater(X1,X2)|~reorganization(esk5_0,esk15_0,X3)|~organization(esk6_0,X3)|~organization(esk5_0,X3)|~survival_chance(esk6_0,X4,esk15_0)|~survival_chance(esk5_0,X4,esk15_0)|~survival_chance(esk6_0,X2,X3)|~survival_chance(esk5_0,X1,X3)), inference(spm,[status(thm)],[c_0_29, c_0_30])).
% 249.41/36.89 cnf(c_0_38, negated_conjecture, (reorganization(esk5_0,esk15_0,esk14_0)), inference(rw,[status(thm)],[c_0_31, c_0_32])).
% 249.41/36.89 cnf(c_0_39, negated_conjecture, (organization(esk6_0,X1)|~organization(esk6_0,X2)|~greater(esk17_0,X1)|~greater(X1,X2)), inference(spm,[status(thm)],[c_0_33, c_0_34])).
% 249.41/36.89 cnf(c_0_40, negated_conjecture, (greater(esk17_0,X1)|~reorganization(esk5_0,esk15_0,X1)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_35, c_0_30]), c_0_34])])).
% 249.41/36.89 cnf(c_0_41, plain, (greater(X3,X2)|~reorganization(X1,X2,X3)), inference(split_conjunct,[status(thm)],[c_0_36])).
% 249.41/36.89 cnf(c_0_42, negated_conjecture, (organization(esk5_0,esk17_0)), inference(split_conjunct,[status(thm)],[c_0_7])).
% 249.41/36.89 cnf(c_0_43, negated_conjecture, (X1=X2|greater(X1,X2)|~organization(esk6_0,esk14_0)|~organization(esk5_0,esk14_0)|~survival_chance(esk6_0,X3,esk15_0)|~survival_chance(esk5_0,X3,esk15_0)|~survival_chance(esk6_0,X2,esk14_0)|~survival_chance(esk5_0,X1,esk14_0)), inference(spm,[status(thm)],[c_0_37, c_0_38])).
% 249.41/36.89 cnf(c_0_44, negated_conjecture, (organization(esk6_0,X1)|~greater(esk17_0,X1)|~greater(X1,esk15_0)), inference(spm,[status(thm)],[c_0_39, c_0_11])).
% 249.41/36.89 cnf(c_0_45, negated_conjecture, (greater(esk17_0,esk14_0)), inference(spm,[status(thm)],[c_0_40, c_0_38])).
% 249.41/36.89 cnf(c_0_46, negated_conjecture, (greater(esk14_0,esk15_0)), inference(spm,[status(thm)],[c_0_41, c_0_38])).
% 249.41/36.89 cnf(c_0_47, negated_conjecture, (organization(esk5_0,X1)|~organization(esk5_0,X2)|~greater(esk17_0,X1)|~greater(X1,X2)), inference(spm,[status(thm)],[c_0_33, c_0_42])).
% 249.41/36.89 cnf(c_0_48, negated_conjecture, (X1=X2|greater(X1,X2)|~organization(esk5_0,esk14_0)|~survival_chance(esk6_0,X3,esk15_0)|~survival_chance(esk5_0,X3,esk15_0)|~survival_chance(esk6_0,X2,esk14_0)|~survival_chance(esk5_0,X1,esk14_0)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_43, c_0_44]), c_0_45]), c_0_46])])).
% 249.41/36.89 cnf(c_0_49, negated_conjecture, (organization(esk5_0,X1)|~greater(esk17_0,X1)|~greater(X1,esk15_0)), inference(spm,[status(thm)],[c_0_47, c_0_18])).
% 249.41/36.89 cnf(c_0_50, negated_conjecture, (X1=X2|greater(X1,X2)|~survival_chance(esk6_0,X3,esk15_0)|~survival_chance(esk5_0,X3,esk15_0)|~survival_chance(esk6_0,X2,esk14_0)|~survival_chance(esk5_0,X1,esk14_0)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_48, c_0_49]), c_0_45]), c_0_46])])).
% 249.41/36.89 cnf(c_0_51, negated_conjecture, (survival_chance(esk6_0,esk9_0,esk15_0)), inference(split_conjunct,[status(thm)],[c_0_7])).
% 249.41/36.89 cnf(c_0_52, negated_conjecture, (survival_chance(esk5_0,esk9_0,esk15_0)), inference(split_conjunct,[status(thm)],[c_0_7])).
% 249.41/36.89 cnf(c_0_53, negated_conjecture, (X1=X2|greater(X1,X2)|~survival_chance(esk6_0,X2,esk14_0)|~survival_chance(esk5_0,X1,esk14_0)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_50, c_0_51]), c_0_52])])).
% 249.41/36.89 cnf(c_0_54, negated_conjecture, (survival_chance(esk6_0,esk11_0,esk14_0)), inference(split_conjunct,[status(thm)],[c_0_7])).
% 249.41/36.89 cnf(c_0_55, negated_conjecture, (X1=esk11_0|greater(X1,esk11_0)|~survival_chance(esk5_0,X1,esk14_0)), inference(spm,[status(thm)],[c_0_53, c_0_54])).
% 249.41/36.89 cnf(c_0_56, negated_conjecture, (survival_chance(esk5_0,esk10_0,esk14_0)), inference(split_conjunct,[status(thm)],[c_0_7])).
% 249.41/36.89 cnf(c_0_57, negated_conjecture, (esk10_0!=esk11_0), inference(split_conjunct,[status(thm)],[c_0_7])).
% 249.41/36.89 cnf(c_0_58, negated_conjecture, (~greater(esk10_0,esk11_0)), inference(split_conjunct,[status(thm)],[c_0_7])).
% 249.41/36.89 cnf(c_0_59, negated_conjecture, ($false), inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_55, c_0_56]), c_0_57]), c_0_58]), ['proof']).
% 249.41/36.89 % SZS output end Proof
% 249.41/36.89 % User time : 35.558 s
% 249.41/36.89 % System time : 0.139 s
% 249.41/36.89 % Total time : 35.697 s
% 249.41/36.89 % User time : 176.899 s
% 249.41/36.89 % System time : 0.979 s
% 249.41/36.89 % Total time : 177.878 s
% 249.41/36.89
%------------------------------------------------------------------------------