%------------------------------------------------------------------------------
% File : CSI_E---1.1
% Problem : MGT073+1 : TPTP v9.3.0. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar mcs_scs.jar %d %s
% Computer : n017.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 0.24s 0.53s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : MGT073+1 : TPTP v9.3.0. Released v9.3.0.
% 0.00/0.03 % Command : java -jar mcs_scs.jar %d %s
% 0.06/0.34 % Computer : n017.cluster.edu
% 0.06/0.34 % Model : x86_64 x86_64
% 0.06/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.06/0.34 % Memory : 8046.5625MB
% 0.06/0.34 % OS : Linux 6.8.0-71-generic
% 0.06/0.34 % CPULimit : 300
% 0.06/0.34 % WCLimit : 300
% 0.06/0.34 % DateTime : Mon Sep 7 13:52:54 UTC 2026
% 0.06/0.34 % CPUTime :
% 0.24/0.46 start to proof:theBenchmark.p
% 0.24/0.53 % Version : CSI_E---1.1
% 0.24/0.53 % Problem : theBenchmark.p
% 0.24/0.53 % Proof found!
% 0.24/0.53 % SZS status Theorem for theBenchmark.p
% 0.24/0.53 % SZS output start Proof
% 0.24/0.53 fof(no_false_compatible, conjecture, ?[X1]:((in_closed(X1,n0,n10)&in_closed(X1,n5,n10))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', no_false_compatible)).
% 0.24/0.53 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)).
% 0.24/0.53 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)).
% 0.24/0.53 fof(order_0_5, hypothesis, less(n0,n5), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', order_0_5)).
% 0.24/0.53 fof(order_5_10, hypothesis, less(n5,n10), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', order_5_10)).
% 0.24/0.53 fof(c_0_5, negated_conjecture, ~(?[X1]:((in_closed(X1,n0,n10)&in_closed(X1,n5,n10)))), inference(assume_negation,[status(cth)],[no_false_compatible])).
% 0.24/0.53 fof(c_0_6, negated_conjecture, ![X26]:((~in_closed(X26,n0,n10)|~in_closed(X26,n5,n10))), inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_5])])])).
% 0.24/0.53 fof(c_0_7, plain, ![X53, X54, X55]:((((leq(X54,X53)|~in_closed(X53,X54,X55))&(leq(X53,X55)|~in_closed(X53,X54,X55)))&(~leq(X54,X53)|~leq(X53,X55)|in_closed(X53,X54,X55)))), inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[in_closed])])])])).
% 0.24/0.53 cnf(c_0_8, negated_conjecture, (~in_closed(X1,n0,n10)|~in_closed(X1,n5,n10)), inference(split_conjunct,[status(thm)],[c_0_6])).
% 0.24/0.53 cnf(c_0_9, plain, (in_closed(X2,X1,X3)|~leq(X1,X2)|~leq(X2,X3)), inference(split_conjunct,[status(thm)],[c_0_7])).
% 0.24/0.53 cnf(c_0_10, plain, (leq(X1,X2)|~in_closed(X1,X3,X2)), inference(split_conjunct,[status(thm)],[c_0_7])).
% 0.24/0.53 fof(c_0_11, plain, ![X33, X34]:(((~leq(X33,X34)|(less(X33,X34)|X33=X34))&((~less(X33,X34)|leq(X33,X34))&(X33!=X34|leq(X33,X34))))), inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[leq_def])])])])).
% 0.24/0.53 cnf(c_0_12, negated_conjecture, (~in_closed(X1,n5,n10)|~leq(n0,X1)), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_8, c_0_9]), c_0_10])).
% 0.24/0.53 cnf(c_0_13, plain, (leq(X1,X2)|~less(X1,X2)), inference(split_conjunct,[status(thm)],[c_0_11])).
% 0.24/0.53 cnf(c_0_14, hypothesis, (less(n0,n5)), inference(split_conjunct,[status(thm)],[order_0_5])).
% 0.24/0.53 cnf(c_0_15, hypothesis, (less(n5,n10)), inference(split_conjunct,[status(thm)],[order_5_10])).
% 0.24/0.53 cnf(c_0_16, plain, (leq(X1,X2)|X1!=X2), inference(split_conjunct,[status(thm)],[c_0_11])).
% 0.24/0.53 cnf(c_0_17, negated_conjecture, (~leq(n0,X1)|~leq(X1,n10)|~leq(n5,X1)), inference(spm,[status(thm)],[c_0_12, c_0_9])).
% 0.24/0.53 cnf(c_0_18, hypothesis, (leq(n0,n5)), inference(spm,[status(thm)],[c_0_13, c_0_14])).
% 0.24/0.53 cnf(c_0_19, hypothesis, (leq(n5,n10)), inference(spm,[status(thm)],[c_0_13, c_0_15])).
% 0.24/0.53 cnf(c_0_20, plain, (leq(X1,X1)), inference(er,[status(thm)],[c_0_16])).
% 0.24/0.53 cnf(c_0_21, hypothesis, ($false), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_17, c_0_18]), c_0_19]), c_0_20])]), ['proof']).
% 0.24/0.53 % SZS output end Proof
% 0.24/0.53 % User time : 0.008 s
% 0.24/0.53 % System time : 0.001 s
% 0.24/0.53 % Total time : 0.009 s
% 0.24/0.53 % User time : 0.011 s
% 0.24/0.53 % System time : 0.004 s
% 0.24/0.53 % Total time : 0.015 s
% 0.24/0.53
%------------------------------------------------------------------------------