%------------------------------------------------------------------------------
% File : CSI_E---1.1
% Problem : MGT068+1 : TPTP v9.3.0. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar mcs_scs.jar %d %s
% Computer : n013.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:37 AM UTC 2026
% Result : Theorem 35.19s 5.94s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : MGT068+1 : TPTP v9.3.0. Released v9.3.0.
% 0.00/0.03 % Command : java -jar mcs_scs.jar %d %s
% 0.09/0.37 % Computer : n013.cluster.edu
% 0.09/0.37 % Model : x86_64 x86_64
% 0.09/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.37 % Memory : 8046.5625MB
% 0.09/0.37 % OS : Linux 6.8.0-71-generic
% 0.09/0.37 % CPULimit : 300
% 0.09/0.37 % WCLimit : 300
% 0.09/0.37 % DateTime : Mon Sep 7 13:52:20 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.21/0.49 start to proof:theBenchmark.p
% 35.19/5.94 % Version : CSI_E---1.1
% 35.19/5.94 % Problem : theBenchmark.p
% 35.19/5.94 % Proof found!
% 35.19/5.94 % SZS status Theorem for theBenchmark.p
% 35.19/5.94 % SZS output start Proof
% 35.19/5.94 fof(axis_subsumes_def, axiom, ![X6, X7, X8, X9]:((axis_subsumes(X6,X7,X8,X9)<=>![X1]:((in_closed(X1,X6,X7)=>in_closed(X1,X8,X9))))), file('/export/starexec/sandbox2/benchmark/Axioms/MGT002+2.ax', axis_subsumes_def)).
% 35.19/5.94 fof(in_closed, axiom, ![X1, X4, X5]:((in_closed(X1,X4,X5)<=>(leq(X4,X1)&leq(X1,X5)))), file('/export/starexec/sandbox2/benchmark/Axioms/MGT002+2.ax', in_closed)).
% 35.19/5.94 fof(axis_compatible_def, axiom, ![X6, X7, X8, X9]:((axis_compatible(X6,X7,X8,X9)<=>?[X1]:((in_closed(X1,X6,X7)&in_closed(X1,X8,X9))))), file('/export/starexec/sandbox2/benchmark/Axioms/MGT002+2.ax', axis_compatible_def)).
% 35.19/5.94 fof(h_sup_ub, hypothesis, ![X1]:(leq(X1,nsup)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', h_sup_ub)).
% 35.19/5.94 fof(irreflexive, axiom, ![X1]:(~(less(X1,X1))), file('/export/starexec/sandbox2/benchmark/Axioms/MGT002+0.ax', irreflexive)).
% 35.19/5.94 fof(less_leq_trans, axiom, ![X1, X2, X3]:(((less(X1,X2)&leq(X2,X3))=>less(X1,X3))), file('/export/starexec/sandbox2/benchmark/Axioms/MGT002+0.ax', less_leq_trans)).
% 35.19/5.94 fof(leq_less_trans, axiom, ![X1, X2, X3]:(((leq(X1,X2)&less(X2,X3))=>less(X1,X3))), file('/export/starexec/sandbox2/benchmark/Axioms/MGT002+0.ax', leq_less_trans)).
% 35.19/5.94 fof(axis_conflict_def, axiom, ![X6, X7, X8, X9]:((axis_conflict(X6,X7,X8,X9)<=>~(?[X1]:((in_closed(X1,X6,X7)&in_closed(X1,X8,X9)))))), file('/export/starexec/sandbox2/benchmark/Axioms/MGT002+2.ax', axis_conflict_def)).
% 35.19/5.94 fof(hard_chain, conjecture, (((((axis_conflict(n0,n3,n10,n20)&?[X3]:((less(n5,X3)&less(X3,n10))))&~(disjoint(n5,nsup,o,c,ninf,n10,c,o)))&completion_conflict(n5,n10,ninf,nsup))&completion_compatible(n5,ninf,nsup))&box_verdict(conflict,unknown)=conflict), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', hard_chain)).
% 35.19/5.94 fof(h_inf_lb, hypothesis, ![X1]:(leq(ninf,X1)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', h_inf_lb)).
% 35.19/5.94 fof(dense, axiom, ![X1, X2]:((less(X1,X2)=>?[X3]:((less(X1,X3)&less(X3,X2))))), file('/export/starexec/sandbox2/benchmark/Axioms/MGT002+1.ax', dense)).
% 35.19/5.94 fof(disjoint_def, axiom, ![X24, X25, X26, X27, X28, X29, X30, X31]:((disjoint(X24,X25,X26,X27,X28,X29,X30,X31)<=>(prec(X25,X28,X27,X30)|prec(X29,X24,X31,X26)))), file('/export/starexec/sandbox2/benchmark/Axioms/MGT002+5.ax', disjoint_def)).
% 35.19/5.94 fof(h_5_10, hypothesis, less(n5,n10), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', h_5_10)).
% 35.19/5.94 fof(leq_def, axiom, ![X1, X2]:((leq(X1,X2)<=>(less(X1,X2)|X1=X2))), file('/export/starexec/sandbox2/benchmark/Axioms/MGT002+0.ax', leq_def)).
% 35.19/5.94 fof(sharpness_conflict, axiom, ![X15, X10, X13, X14]:(((((leq(X13,X15)&leq(X15,X14))&less(X15,X10))&leq(X10,X14))=>completion_conflict(X15,X10,X13,X14))), file('/export/starexec/sandbox2/benchmark/Axioms/MGT002+4.ax', sharpness_conflict)).
% 35.19/5.94 fof(leq_antisym, axiom, ![X1, X2]:(((leq(X1,X2)&leq(X2,X1))=>X1=X2)), file('/export/starexec/sandbox2/benchmark/Axioms/MGT002+0.ax', leq_antisym)).
% 35.19/5.94 fof(completion_compat, axiom, ![X10, X13, X14]:(((leq(X13,X10)&leq(X10,X14))=>completion_compatible(X10,X13,X14))), file('/export/starexec/sandbox2/benchmark/Axioms/MGT002+4.ax', completion_compat)).
% 35.19/5.94 fof(prec_oo, axiom, ![X15, X23]:((prec(X15,X23,o,o)<=>leq(X15,X23))), file('/export/starexec/sandbox2/benchmark/Axioms/MGT002+5.ax', prec_oo)).
% 35.19/5.94 fof(prec_cc, axiom, ![X15, X23]:((prec(X15,X23,c,c)<=>less(X15,X23))), file('/export/starexec/sandbox2/benchmark/Axioms/MGT002+5.ax', prec_cc)).
% 35.19/5.94 fof(transitive, axiom, ![X1, X2, X3]:(((less(X1,X2)&less(X2,X3))=>less(X1,X3))), file('/export/starexec/sandbox2/benchmark/Axioms/MGT002+0.ax', transitive)).
% 35.19/5.94 fof(box_conflict, axiom, ![X11, X12]:((((is_verdict(X11)&is_verdict(X12))&(X11=conflict|X12=conflict))=>box_verdict(X11,X12)=conflict)), file('/export/starexec/sandbox2/benchmark/Axioms/MGT002+2.ax', box_conflict)).
% 35.19/5.94 fof(h_3_5, hypothesis, less(n3,n5), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', h_3_5)).
% 35.19/5.94 fof(conflict_is_verdict, axiom, is_verdict(conflict), file('/export/starexec/sandbox2/benchmark/Axioms/MGT002+2.ax', conflict_is_verdict)).
% 35.19/5.94 fof(unknown_is_verdict, axiom, is_verdict(unknown), file('/export/starexec/sandbox2/benchmark/Axioms/MGT002+2.ax', unknown_is_verdict)).
% 35.19/5.94 fof(c_0_24, plain, ![X88, X89, X90, X91, X92, X93, X94, X95, X96]:(((~axis_subsumes(X88,X89,X90,X91)|(~in_closed(X92,X88,X89)|in_closed(X92,X90,X91)))&((in_closed(esk4_4(X93,X94,X95,X96),X93,X94)|axis_subsumes(X93,X94,X95,X96))&(~in_closed(esk4_4(X93,X94,X95,X96),X95,X96)|axis_subsumes(X93,X94,X95,X96))))), inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(fof_nnf,[status(thm)],[axis_subsumes_def])])])])])])])).
% 35.19/5.94 fof(c_0_25, plain, ![X56, X57, X58]:((((leq(X57,X56)|~in_closed(X56,X57,X58))&(leq(X56,X58)|~in_closed(X56,X57,X58)))&(~leq(X57,X56)|~leq(X56,X58)|in_closed(X56,X57,X58)))), inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[in_closed])])])])).
% 35.19/5.94 fof(c_0_26, plain, ![X78, X79, X80, X81, X83, X84, X85, X86, X87]:((((in_closed(esk3_4(X78,X79,X80,X81),X78,X79)|~axis_compatible(X78,X79,X80,X81))&(in_closed(esk3_4(X78,X79,X80,X81),X80,X81)|~axis_compatible(X78,X79,X80,X81)))&(~in_closed(X87,X83,X84)|~in_closed(X87,X85,X86)|axis_compatible(X83,X84,X85,X86)))), inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(fof_nnf,[status(thm)],[axis_compatible_def])])])])])])])).
% 35.19/5.94 cnf(c_0_27, plain, (axis_subsumes(X1,X2,X3,X4)|~in_closed(esk4_4(X1,X2,X3,X4),X3,X4)), inference(split_conjunct,[status(thm)],[c_0_24])).
% 35.19/5.94 cnf(c_0_28, plain, (in_closed(X2,X1,X3)|~leq(X1,X2)|~leq(X2,X3)), inference(split_conjunct,[status(thm)],[c_0_25])).
% 35.19/5.94 fof(c_0_29, hypothesis, ![X151]:(leq(X151,nsup)), inference(variable_rename,[status(thm)],[h_sup_ub])).
% 35.19/5.94 fof(c_0_30, plain, ![X1]:(~less(X1,X1)), inference(fof_simplification,[status(thm)],[irreflexive])).
% 35.19/5.94 fof(c_0_31, plain, ![X47, X48, X49]:((~less(X47,X48)|~leq(X48,X49)|less(X47,X49))), inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[less_leq_trans])])])).
% 35.19/5.94 cnf(c_0_32, plain, (leq(X1,X2)|~in_closed(X2,X1,X3)), inference(split_conjunct,[status(thm)],[c_0_25])).
% 35.19/5.94 cnf(c_0_33, plain, (in_closed(esk3_4(X1,X2,X3,X4),X3,X4)|~axis_compatible(X1,X2,X3,X4)), inference(split_conjunct,[status(thm)],[c_0_26])).
% 35.19/5.94 cnf(c_0_34, plain, (axis_subsumes(X1,X2,X3,X4)|~leq(esk4_4(X1,X2,X3,X4),X4)|~leq(X3,esk4_4(X1,X2,X3,X4))), inference(spm,[status(thm)],[c_0_27, c_0_28])).
% 35.19/5.94 cnf(c_0_35, hypothesis, (leq(X1,nsup)), inference(split_conjunct,[status(thm)],[c_0_29])).
% 35.19/5.94 cnf(c_0_36, plain, (in_closed(esk4_4(X1,X2,X3,X4),X1,X2)|axis_subsumes(X1,X2,X3,X4)), inference(split_conjunct,[status(thm)],[c_0_24])).
% 35.19/5.94 fof(c_0_37, plain, ![X32]:(~less(X32,X32)), inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[c_0_30])])).
% 35.19/5.94 cnf(c_0_38, plain, (less(X1,X3)|~less(X1,X2)|~leq(X2,X3)), inference(split_conjunct,[status(thm)],[c_0_31])).
% 35.19/5.94 cnf(c_0_39, plain, (leq(X1,esk3_4(X2,X3,X1,X4))|~axis_compatible(X2,X3,X1,X4)), inference(spm,[status(thm)],[c_0_32, c_0_33])).
% 35.19/5.94 fof(c_0_40, plain, ![X44, X45, X46]:((~leq(X44,X45)|~less(X45,X46)|less(X44,X46))), inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[leq_less_trans])])])).
% 35.19/5.94 cnf(c_0_41, plain, (leq(X1,X2)|~in_closed(X1,X3,X2)), inference(split_conjunct,[status(thm)],[c_0_25])).
% 35.19/5.94 fof(c_0_42, plain, ![X68, X69, X70, X71, X72, X73, X74, X75, X76]:(((~axis_conflict(X68,X69,X70,X71)|(~in_closed(X72,X68,X69)|~in_closed(X72,X70,X71)))&((in_closed(esk2_4(X73,X74,X75,X76),X73,X74)|axis_conflict(X73,X74,X75,X76))&(in_closed(esk2_4(X73,X74,X75,X76),X75,X76)|axis_conflict(X73,X74,X75,X76))))), inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(fof_nnf,[status(thm)],[axis_conflict_def])])])])])])])).
% 35.19/5.94 cnf(c_0_43, hypothesis, (axis_subsumes(X1,X2,X3,nsup)|~leq(X3,esk4_4(X1,X2,X3,nsup))), inference(spm,[status(thm)],[c_0_34, c_0_35])).
% 35.19/5.94 cnf(c_0_44, plain, (axis_subsumes(X1,X2,X3,X4)|leq(X1,esk4_4(X1,X2,X3,X4))), inference(spm,[status(thm)],[c_0_32, c_0_36])).
% 35.19/5.94 fof(c_0_45, negated_conjecture, ~((((((axis_conflict(n0,n3,n10,n20)&?[X3]:((less(n5,X3)&less(X3,n10))))&~disjoint(n5,nsup,o,c,ninf,n10,c,o))&completion_conflict(n5,n10,ninf,nsup))&completion_compatible(n5,ninf,nsup))&box_verdict(conflict,unknown)=conflict)), inference(fof_simplification,[status(thm)],[inference(assume_negation,[status(cth)],[hard_chain])])).
% 35.19/5.94 cnf(c_0_46, plain, (~less(X1,X1)), inference(split_conjunct,[status(thm)],[c_0_37])).
% 35.19/5.94 cnf(c_0_47, plain, (less(X1,esk3_4(X2,X3,X4,X5))|~axis_compatible(X2,X3,X4,X5)|~less(X1,X4)), inference(spm,[status(thm)],[c_0_38, c_0_39])).
% 35.19/5.94 cnf(c_0_48, plain, (less(X1,X3)|~leq(X1,X2)|~less(X2,X3)), inference(split_conjunct,[status(thm)],[c_0_40])).
% 35.19/5.94 cnf(c_0_49, plain, (leq(esk3_4(X1,X2,X3,X4),X4)|~axis_compatible(X1,X2,X3,X4)), inference(spm,[status(thm)],[c_0_41, c_0_33])).
% 35.19/5.94 cnf(c_0_50, plain, (axis_compatible(X2,X3,X4,X5)|~in_closed(X1,X2,X3)|~in_closed(X1,X4,X5)), inference(split_conjunct,[status(thm)],[c_0_26])).
% 35.19/5.94 cnf(c_0_51, plain, (in_closed(esk2_4(X1,X2,X3,X4),X3,X4)|axis_conflict(X1,X2,X3,X4)), inference(split_conjunct,[status(thm)],[c_0_42])).
% 35.19/5.94 fof(c_0_52, hypothesis, ![X150]:(leq(ninf,X150)), inference(variable_rename,[status(thm)],[h_inf_lb])).
% 35.19/5.94 cnf(c_0_53, plain, (in_closed(X5,X3,X4)|~axis_subsumes(X1,X2,X3,X4)|~in_closed(X5,X1,X2)), inference(split_conjunct,[status(thm)],[c_0_24])).
% 35.19/5.94 cnf(c_0_54, hypothesis, (axis_subsumes(X1,X2,X1,nsup)), inference(spm,[status(thm)],[c_0_43, c_0_44])).
% 35.19/5.94 fof(c_0_55, negated_conjecture, ![X152]:((~axis_conflict(n0,n3,n10,n20)|(~less(n5,X152)|~less(X152,n10))|disjoint(n5,nsup,o,c,ninf,n10,c,o)|~completion_conflict(n5,n10,ninf,nsup)|~completion_compatible(n5,ninf,nsup)|box_verdict(conflict,unknown)!=conflict)), inference(fof_nnf,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_45])])])])).
% 35.19/5.94 fof(c_0_56, plain, ![X53, X54]:(((less(X53,esk1_2(X53,X54))|~less(X53,X54))&(less(esk1_2(X53,X54),X54)|~less(X53,X54)))), inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[dense])])])])])).
% 35.19/5.94 cnf(c_0_57, plain, (in_closed(esk3_4(X1,X2,X3,X4),X1,X2)|~axis_compatible(X1,X2,X3,X4)), inference(split_conjunct,[status(thm)],[c_0_26])).
% 35.19/5.94 cnf(c_0_58, plain, (~axis_compatible(X1,X2,X3,X4)|~less(esk3_4(X1,X2,X3,X4),X3)), inference(spm,[status(thm)],[c_0_46, c_0_47])).
% 35.19/5.94 cnf(c_0_59, plain, (less(esk3_4(X1,X2,X3,X4),X5)|~axis_compatible(X1,X2,X3,X4)|~less(X4,X5)), inference(spm,[status(thm)],[c_0_48, c_0_49])).
% 35.19/5.94 cnf(c_0_60, plain, (axis_compatible(X1,X2,X3,X4)|axis_conflict(X5,X6,X3,X4)|~in_closed(esk2_4(X5,X6,X3,X4),X1,X2)), inference(spm,[status(thm)],[c_0_50, c_0_51])).
% 35.19/5.94 cnf(c_0_61, hypothesis, (leq(ninf,X1)), inference(split_conjunct,[status(thm)],[c_0_52])).
% 35.19/5.94 cnf(c_0_62, hypothesis, (in_closed(X1,X2,nsup)|~in_closed(X1,X2,X3)), inference(spm,[status(thm)],[c_0_53, c_0_54])).
% 35.19/5.94 cnf(c_0_63, negated_conjecture, (disjoint(n5,nsup,o,c,ninf,n10,c,o)|~axis_conflict(n0,n3,n10,n20)|~less(n5,X1)|~less(X1,n10)|~completion_conflict(n5,n10,ninf,nsup)|~completion_compatible(n5,ninf,nsup)|box_verdict(conflict,unknown)!=conflict), inference(split_conjunct,[status(thm)],[c_0_55])).
% 35.19/5.94 cnf(c_0_64, plain, (less(esk1_2(X1,X2),X2)|~less(X1,X2)), inference(split_conjunct,[status(thm)],[c_0_56])).
% 35.19/5.94 cnf(c_0_65, plain, (leq(esk3_4(X1,X2,X3,X4),X2)|~axis_compatible(X1,X2,X3,X4)), inference(spm,[status(thm)],[c_0_41, c_0_57])).
% 35.19/5.94 cnf(c_0_66, plain, (~axis_compatible(X1,X2,X3,X4)|~less(X4,X3)), inference(spm,[status(thm)],[c_0_58, c_0_59])).
% 35.19/5.94 cnf(c_0_67, plain, (axis_compatible(X1,X2,X1,X2)|axis_conflict(X3,X4,X1,X2)), inference(spm,[status(thm)],[c_0_60, c_0_51])).
% 35.19/5.94 cnf(c_0_68, hypothesis, (axis_subsumes(X1,X2,ninf,nsup)), inference(spm,[status(thm)],[c_0_43, c_0_61])).
% 35.19/5.94 cnf(c_0_69, hypothesis, (in_closed(X1,X2,nsup)|~leq(X1,X3)|~leq(X2,X1)), inference(spm,[status(thm)],[c_0_62, c_0_28])).
% 35.19/5.94 fof(c_0_70, plain, ![X142, X143, X144, X145, X146, X147, X148, X149]:(((~disjoint(X142,X143,X144,X145,X146,X147,X148,X149)|(prec(X143,X146,X145,X148)|prec(X147,X142,X149,X144)))&((~prec(X143,X146,X145,X148)|disjoint(X142,X143,X144,X145,X146,X147,X148,X149))&(~prec(X147,X142,X149,X144)|disjoint(X142,X143,X144,X145,X146,X147,X148,X149))))), inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[disjoint_def])])])])).
% 35.19/5.94 cnf(c_0_71, negated_conjecture, (disjoint(n5,nsup,o,c,ninf,n10,c,o)|box_verdict(conflict,unknown)!=conflict|~completion_conflict(n5,n10,ninf,nsup)|~completion_compatible(n5,ninf,nsup)|~axis_conflict(n0,n3,n10,n20)|~less(n5,esk1_2(X1,n10))|~less(X1,n10)), inference(spm,[status(thm)],[c_0_63, c_0_64])).
% 35.19/5.94 cnf(c_0_72, plain, (less(X1,esk1_2(X1,X2))|~less(X1,X2)), inference(split_conjunct,[status(thm)],[c_0_56])).
% 35.19/5.94 cnf(c_0_73, hypothesis, (less(n5,n10)), inference(split_conjunct,[status(thm)],[h_5_10])).
% 35.19/5.94 cnf(c_0_74, plain, (less(esk3_4(X1,X2,X3,X4),X5)|~axis_compatible(X1,X2,X3,X4)|~less(X2,X5)), inference(spm,[status(thm)],[c_0_48, c_0_65])).
% 35.19/5.94 cnf(c_0_75, plain, (in_closed(esk2_4(X1,X2,X3,X4),X1,X2)|axis_conflict(X1,X2,X3,X4)), inference(split_conjunct,[status(thm)],[c_0_42])).
% 35.19/5.94 cnf(c_0_76, plain, (~axis_conflict(X1,X2,X3,X4)|~in_closed(X5,X1,X2)|~in_closed(X5,X3,X4)), inference(split_conjunct,[status(thm)],[c_0_42])).
% 35.19/5.94 cnf(c_0_77, plain, (axis_conflict(X1,X2,X3,X4)|~less(X4,X3)), inference(spm,[status(thm)],[c_0_66, c_0_67])).
% 35.19/5.94 cnf(c_0_78, hypothesis, (in_closed(X1,ninf,nsup)|~in_closed(X1,X2,X3)), inference(spm,[status(thm)],[c_0_53, c_0_68])).
% 35.19/5.94 cnf(c_0_79, hypothesis, (in_closed(X1,X2,nsup)|~leq(X2,X1)), inference(spm,[status(thm)],[c_0_69, c_0_35])).
% 35.19/5.94 cnf(c_0_80, plain, (prec(X2,X5,X4,X7)|prec(X6,X1,X8,X3)|~disjoint(X1,X2,X3,X4,X5,X6,X7,X8)), inference(split_conjunct,[status(thm)],[c_0_70])).
% 35.19/5.94 cnf(c_0_81, negated_conjecture, (disjoint(n5,nsup,o,c,ninf,n10,c,o)|box_verdict(conflict,unknown)!=conflict|~completion_conflict(n5,n10,ninf,nsup)|~completion_compatible(n5,ninf,nsup)|~axis_conflict(n0,n3,n10,n20)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_71, c_0_72]), c_0_73])])).
% 35.19/5.94 cnf(c_0_82, plain, (~axis_compatible(X1,X2,X3,X4)|~less(X2,X3)), inference(spm,[status(thm)],[c_0_58, c_0_74])).
% 35.19/5.94 cnf(c_0_83, plain, (axis_compatible(X1,X2,X3,X4)|axis_conflict(X1,X2,X3,X4)), inference(spm,[status(thm)],[c_0_60, c_0_75])).
% 35.19/5.94 cnf(c_0_84, plain, (~in_closed(X1,X2,X3)|~in_closed(X1,X4,X5)|~less(X3,X2)), inference(spm,[status(thm)],[c_0_76, c_0_77])).
% 35.19/5.94 cnf(c_0_85, hypothesis, (in_closed(X1,ninf,nsup)|~leq(X2,X1)), inference(spm,[status(thm)],[c_0_78, c_0_79])).
% 35.19/5.94 fof(c_0_86, plain, ![X38, X39]:(((~leq(X38,X39)|(less(X38,X39)|X38=X39))&((~less(X38,X39)|leq(X38,X39))&(X38!=X39|leq(X38,X39))))), inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[leq_def])])])])).
% 35.19/5.94 cnf(c_0_87, negated_conjecture, (prec(nsup,ninf,c,c)|prec(n10,n5,o,o)|box_verdict(conflict,unknown)!=conflict|~completion_conflict(n5,n10,ninf,nsup)|~completion_compatible(n5,ninf,nsup)|~axis_conflict(n0,n3,n10,n20)), inference(spm,[status(thm)],[c_0_80, c_0_81])).
% 35.19/5.94 cnf(c_0_88, plain, (axis_conflict(X1,X2,X3,X4)|~less(X2,X3)), inference(spm,[status(thm)],[c_0_82, c_0_83])).
% 35.19/5.94 fof(c_0_89, plain, ![X118, X119, X120, X121]:((~leq(X120,X118)|~leq(X118,X121)|~less(X118,X119)|~leq(X119,X121)|completion_conflict(X118,X119,X120,X121))), inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[sharpness_conflict])])])).
% 35.19/5.94 cnf(c_0_90, plain, (~in_closed(X1,X2,X3)|~leq(X1,X4)|~leq(X5,X1)|~less(X4,X5)), inference(spm,[status(thm)],[c_0_84, c_0_28])).
% 35.19/5.94 cnf(c_0_91, hypothesis, (in_closed(X1,ninf,nsup)), inference(spm,[status(thm)],[c_0_85, c_0_61])).
% 35.19/5.94 cnf(c_0_92, plain, (leq(X1,X2)|X1!=X2), inference(split_conjunct,[status(thm)],[c_0_86])).
% 35.19/5.94 fof(c_0_93, plain, ![X40, X41]:((~leq(X40,X41)|~leq(X41,X40)|X40=X41)), inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[leq_antisym])])])).
% 35.19/5.94 cnf(c_0_94, negated_conjecture, (prec(n10,n5,o,o)|prec(nsup,ninf,c,c)|box_verdict(conflict,unknown)!=conflict|~completion_conflict(n5,n10,ninf,nsup)|~completion_compatible(n5,ninf,nsup)|~less(n3,n10)), inference(spm,[status(thm)],[c_0_87, c_0_88])).
% 35.19/5.94 cnf(c_0_95, plain, (completion_conflict(X2,X4,X1,X3)|~leq(X1,X2)|~leq(X2,X3)|~less(X2,X4)|~leq(X4,X3)), inference(split_conjunct,[status(thm)],[c_0_89])).
% 35.19/5.94 fof(c_0_96, plain, ![X107, X108, X109]:((~leq(X108,X107)|~leq(X107,X109)|completion_compatible(X107,X108,X109))), inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[completion_compat])])])).
% 35.19/5.94 cnf(c_0_97, hypothesis, (~leq(X1,X2)|~leq(X3,X1)|~less(X2,X3)), inference(spm,[status(thm)],[c_0_90, c_0_91])).
% 35.19/5.94 cnf(c_0_98, plain, (leq(X1,X1)), inference(er,[status(thm)],[c_0_92])).
% 35.19/5.94 cnf(c_0_99, plain, (X1=X2|~leq(X1,X2)|~leq(X2,X1)), inference(split_conjunct,[status(thm)],[c_0_93])).
% 35.19/5.94 cnf(c_0_100, plain, (leq(X1,X2)|~less(X1,X2)), inference(split_conjunct,[status(thm)],[c_0_86])).
% 35.19/5.94 fof(c_0_101, plain, ![X140, X141]:(((~prec(X140,X141,o,o)|leq(X140,X141))&(~leq(X140,X141)|prec(X140,X141,o,o)))), inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[prec_oo])])])).
% 35.19/5.94 cnf(c_0_102, negated_conjecture, (prec(nsup,ninf,c,c)|prec(n10,n5,o,o)|box_verdict(conflict,unknown)!=conflict|~completion_compatible(n5,ninf,nsup)|~less(n3,n10)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_94, c_0_95]), c_0_35]), c_0_35]), c_0_61]), c_0_73])])).
% 35.19/5.94 cnf(c_0_103, plain, (completion_compatible(X2,X1,X3)|~leq(X1,X2)|~leq(X2,X3)), inference(split_conjunct,[status(thm)],[c_0_96])).
% 35.19/5.94 cnf(c_0_104, hypothesis, (~leq(X1,X2)|~less(X2,X1)), inference(spm,[status(thm)],[c_0_97, c_0_98])).
% 35.19/5.94 cnf(c_0_105, hypothesis, (X1=ninf|~leq(X1,ninf)), inference(spm,[status(thm)],[c_0_99, c_0_61])).
% 35.19/5.94 cnf(c_0_106, plain, (leq(esk1_2(X1,X2),X2)|~less(X1,X2)), inference(spm,[status(thm)],[c_0_100, c_0_64])).
% 35.19/5.94 fof(c_0_107, plain, ![X134, X135]:(((~prec(X134,X135,c,c)|less(X134,X135))&(~less(X134,X135)|prec(X134,X135,c,c)))), inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[prec_cc])])])).
% 35.19/5.94 cnf(c_0_108, plain, (leq(X1,X2)|~prec(X1,X2,o,o)), inference(split_conjunct,[status(thm)],[c_0_101])).
% 35.19/5.94 cnf(c_0_109, negated_conjecture, (prec(n10,n5,o,o)|prec(nsup,ninf,c,c)|box_verdict(conflict,unknown)!=conflict|~less(n3,n10)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_102, c_0_103]), c_0_35]), c_0_61])])).
% 35.19/5.94 cnf(c_0_110, hypothesis, (~leq(n10,n5)), inference(spm,[status(thm)],[c_0_104, c_0_73])).
% 35.19/5.94 cnf(c_0_111, hypothesis, (esk1_2(X1,ninf)=ninf|~less(X1,ninf)), inference(spm,[status(thm)],[c_0_105, c_0_106])).
% 35.19/5.94 fof(c_0_112, plain, ![X33, X34, X35]:((~less(X33,X34)|~less(X34,X35)|less(X33,X35))), inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[transitive])])])).
% 35.19/5.94 cnf(c_0_113, plain, (less(X1,X2)|~prec(X1,X2,c,c)), inference(split_conjunct,[status(thm)],[c_0_107])).
% 35.19/5.94 cnf(c_0_114, negated_conjecture, (prec(nsup,ninf,c,c)|box_verdict(conflict,unknown)!=conflict|~less(n3,n10)), inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_108, c_0_109]), c_0_110])).
% 35.19/5.94 cnf(c_0_115, hypothesis, (~less(X1,ninf)), inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_64, c_0_111]), c_0_46])).
% 35.19/5.94 cnf(c_0_116, plain, (less(X1,X3)|~less(X1,X2)|~less(X2,X3)), inference(split_conjunct,[status(thm)],[c_0_112])).
% 35.19/5.94 fof(c_0_117, plain, ![X99, X100]:(((X99!=conflict|(~is_verdict(X99)|~is_verdict(X100))|box_verdict(X99,X100)=conflict)&(X100!=conflict|(~is_verdict(X99)|~is_verdict(X100))|box_verdict(X99,X100)=conflict))), inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[box_conflict])])])])).
% 35.19/5.94 cnf(c_0_118, negated_conjecture, (box_verdict(conflict,unknown)!=conflict|~less(n3,n10)), inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_113, c_0_114]), c_0_115])).
% 35.19/5.94 cnf(c_0_119, hypothesis, (less(X1,n10)|~less(X1,n5)), inference(spm,[status(thm)],[c_0_116, c_0_73])).
% 35.19/5.94 cnf(c_0_120, hypothesis, (less(n3,n5)), inference(split_conjunct,[status(thm)],[h_3_5])).
% 35.19/5.94 cnf(c_0_121, plain, (box_verdict(X1,X2)=conflict|X1!=conflict|~is_verdict(X1)|~is_verdict(X2)), inference(split_conjunct,[status(thm)],[c_0_117])).
% 35.19/5.94 cnf(c_0_122, plain, (is_verdict(conflict)), inference(split_conjunct,[status(thm)],[conflict_is_verdict])).
% 35.19/5.94 cnf(c_0_123, hypothesis, (box_verdict(conflict,unknown)!=conflict), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_118, c_0_119]), c_0_120])])).
% 35.19/5.94 cnf(c_0_124, plain, (box_verdict(conflict,X1)=conflict|~is_verdict(X1)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(er,[status(thm)],[c_0_121]), c_0_122])])).
% 35.19/5.94 cnf(c_0_125, plain, (is_verdict(unknown)), inference(split_conjunct,[status(thm)],[unknown_is_verdict])).
% 35.19/5.94 cnf(c_0_126, hypothesis, ($false), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_123, c_0_124]), c_0_125])]), ['proof']).
% 35.19/5.94 % SZS output end Proof
% 35.19/5.94 % User time : 4.953 s
% 35.19/5.94 % System time : 0.144 s
% 35.19/5.94 % Total time : 5.097 s
% 35.19/5.94 % User time : 23.971 s
% 35.19/5.94 % System time : 0.430 s
% 35.19/5.94 % Total time : 24.401 s
% 35.19/5.94
%------------------------------------------------------------------------------