%------------------------------------------------------------------------------
% File : CSI_E---1.1
% Problem : MGT058-1 : TPTP v9.3.0. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar mcs_scs.jar %d %s
% Computer : n015.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:35 AM UTC 2026
% Result : Unsatisfiable 0.25s 0.53s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : MGT058-1 : TPTP v9.3.0. Released v2.4.0.
% 0.00/0.03 % Command : java -jar mcs_scs.jar %d %s
% 0.08/0.34 % Computer : n015.cluster.edu
% 0.08/0.34 % Model : x86_64 x86_64
% 0.08/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.34 % Memory : 8046.5625MB
% 0.08/0.34 % OS : Linux 6.8.0-71-generic
% 0.08/0.34 % CPULimit : 300
% 0.08/0.34 % WCLimit : 300
% 0.08/0.34 % DateTime : Mon Sep 7 13:35:00 UTC 2026
% 0.08/0.34 % CPUTime :
% 0.13/0.46 start to proof:theBenchmark.p
% 0.25/0.53 % Version : CSI_E---1.1
% 0.25/0.53 % Problem : theBenchmark.p
% 0.25/0.53 % Proof found!
% 0.25/0.53 # SZS status Unsatisfiable
% 0.25/0.53 % SZS output start Proof
% 0.25/0.53 cnf(definition_greater_or_equal_4, axiom, (greater(X1,X2)|X1=X2|~greater_or_equal(X1,X2)), file('/export/starexec/sandbox2/benchmark/Axioms/MGT001-0.ax', definition_greater_or_equal_4)).
% 0.25/0.53 cnf(definition_smaller_8, axiom, (smaller(X2,X1)|~greater(X1,X2)), file('/export/starexec/sandbox2/benchmark/Axioms/MGT001-0.ax', definition_smaller_8)).
% 0.25/0.53 cnf(lemma_10_44, negated_conjecture, (greater_or_equal(sigma,zero)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', lemma_10_44)).
% 0.25/0.53 cnf(definition_3_30, axiom, (positional_advantage(X1,X2)|~fragile_position(X1)|~smaller_or_equal(age(X1,X2),sigma)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', definition_3_30)).
% 0.25/0.53 cnf(definition_smaller_or_equal_2, axiom, (smaller_or_equal(X1,X2)|~smaller(X1,X2)), file('/export/starexec/sandbox2/benchmark/Axioms/MGT001-0.ax', definition_smaller_or_equal_2)).
% 0.25/0.53 cnf(lemma_10_43, negated_conjecture, (age(sk3,sk4)=zero), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', lemma_10_43)).
% 0.25/0.53 cnf(lemma_10_46, negated_conjecture, (fragile_position(sk3)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', lemma_10_46)).
% 0.25/0.53 cnf(lemma_10_45, negated_conjecture, (greater_or_equal(tau,zero)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', lemma_10_45)).
% 0.25/0.53 cnf(definition_4_36, axiom, (~robust_position(X1)|~smaller_or_equal(age(X1,X2),tau)|~positional_advantage(X1,X2)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', definition_4_36)).
% 0.25/0.53 cnf(lemma_10_47, negated_conjecture, (robust_position(sk3)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', lemma_10_47)).
% 0.25/0.53 cnf(definition_smaller_or_equal_3, axiom, (smaller_or_equal(X1,X2)|X1!=X2), file('/export/starexec/sandbox2/benchmark/Axioms/MGT001-0.ax', definition_smaller_or_equal_3)).
% 0.25/0.53 cnf(c_0_11, plain, (greater(X1,X2)|X1=X2|~greater_or_equal(X1,X2)), inference(fof_simplification,[status(thm)],[definition_greater_or_equal_4])).
% 0.25/0.53 cnf(c_0_12, plain, (smaller(X2,X1)|~greater(X1,X2)), inference(fof_simplification,[status(thm)],[definition_smaller_8])).
% 0.25/0.53 cnf(c_0_13, plain, (greater(X1,X2)|X1=X2|~greater_or_equal(X1,X2)), c_0_11).
% 0.25/0.53 cnf(c_0_14, negated_conjecture, (greater_or_equal(sigma,zero)), lemma_10_44).
% 0.25/0.53 cnf(c_0_15, plain, (positional_advantage(X1,X2)|~fragile_position(X1)|~smaller_or_equal(age(X1,X2),sigma)), inference(fof_simplification,[status(thm)],[definition_3_30])).
% 0.25/0.53 cnf(c_0_16, plain, (smaller_or_equal(X1,X2)|~smaller(X1,X2)), inference(fof_simplification,[status(thm)],[definition_smaller_or_equal_2])).
% 0.25/0.53 cnf(c_0_17, plain, (smaller(X2,X1)|~greater(X1,X2)), c_0_12).
% 0.25/0.53 cnf(c_0_18, negated_conjecture, (zero=sigma|greater(sigma,zero)), inference(spm,[status(thm)],[c_0_13, c_0_14])).
% 0.25/0.53 cnf(c_0_19, plain, (positional_advantage(X1,X2)|~fragile_position(X1)|~smaller_or_equal(age(X1,X2),sigma)), c_0_15).
% 0.25/0.53 cnf(c_0_20, negated_conjecture, (age(sk3,sk4)=zero), lemma_10_43).
% 0.25/0.53 cnf(c_0_21, negated_conjecture, (fragile_position(sk3)), lemma_10_46).
% 0.25/0.53 cnf(c_0_22, plain, (smaller_or_equal(X1,X2)|~smaller(X1,X2)), c_0_16).
% 0.25/0.53 cnf(c_0_23, negated_conjecture, (zero=sigma|smaller(zero,sigma)), inference(spm,[status(thm)],[c_0_17, c_0_18])).
% 0.25/0.53 cnf(c_0_24, negated_conjecture, (greater_or_equal(tau,zero)), lemma_10_45).
% 0.25/0.53 cnf(c_0_25, plain, (~robust_position(X1)|~smaller_or_equal(age(X1,X2),tau)|~positional_advantage(X1,X2)), inference(fof_simplification,[status(thm)],[definition_4_36])).
% 0.25/0.53 cnf(c_0_26, negated_conjecture, (positional_advantage(sk3,sk4)|~smaller_or_equal(zero,sigma)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_19, c_0_20]), c_0_21])])).
% 0.25/0.53 cnf(c_0_27, negated_conjecture, (zero=sigma|smaller_or_equal(zero,sigma)), inference(spm,[status(thm)],[c_0_22, c_0_23])).
% 0.25/0.53 cnf(c_0_28, negated_conjecture, (zero=tau|greater(tau,zero)), inference(spm,[status(thm)],[c_0_13, c_0_24])).
% 0.25/0.53 cnf(c_0_29, plain, (~robust_position(X1)|~smaller_or_equal(age(X1,X2),tau)|~positional_advantage(X1,X2)), c_0_25).
% 0.25/0.53 cnf(c_0_30, negated_conjecture, (zero=sigma|positional_advantage(sk3,sk4)), inference(spm,[status(thm)],[c_0_26, c_0_27])).
% 0.25/0.53 cnf(c_0_31, negated_conjecture, (robust_position(sk3)), lemma_10_47).
% 0.25/0.53 cnf(c_0_32, negated_conjecture, (zero=tau|smaller(zero,tau)), inference(spm,[status(thm)],[c_0_17, c_0_28])).
% 0.25/0.53 cnf(c_0_33, plain, (smaller_or_equal(X1,X2)|X1!=X2), inference(fof_simplification,[status(thm)],[definition_smaller_or_equal_3])).
% 0.25/0.53 cnf(c_0_34, negated_conjecture, (zero=sigma|~smaller_or_equal(zero,tau)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_29, c_0_30]), c_0_31]), c_0_20])])).
% 0.25/0.53 cnf(c_0_35, negated_conjecture, (zero=tau|smaller_or_equal(zero,tau)), inference(spm,[status(thm)],[c_0_22, c_0_32])).
% 0.25/0.53 cnf(c_0_36, plain, (smaller_or_equal(X1,X2)|X1!=X2), c_0_33).
% 0.25/0.53 cnf(c_0_37, negated_conjecture, (zero=tau|zero=sigma), inference(spm,[status(thm)],[c_0_34, c_0_35])).
% 0.25/0.53 cnf(c_0_38, plain, (smaller_or_equal(X1,X1)), inference(er,[status(thm)],[c_0_36])).
% 0.25/0.53 cnf(c_0_39, negated_conjecture, (zero=sigma|tau!=sigma), inference(ef,[status(thm)],[c_0_37])).
% 0.25/0.53 cnf(c_0_40, negated_conjecture, (zero=sigma), inference(csr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_34, c_0_37]), c_0_38])]), c_0_39])).
% 0.25/0.53 cnf(c_0_41, negated_conjecture, (positional_advantage(sk3,sk4)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_26, c_0_40]), c_0_38])])).
% 0.25/0.53 cnf(c_0_42, negated_conjecture, (~smaller_or_equal(sigma,tau)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_29, c_0_41]), c_0_31]), c_0_20]), c_0_40])])).
% 0.25/0.53 cnf(c_0_43, negated_conjecture, (tau=sigma), inference(sr,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_35, c_0_40]), c_0_40]), c_0_42])).
% 0.25/0.53 cnf(c_0_44, negated_conjecture, ($false), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_42, c_0_43]), c_0_38])]), ['proof']).
% 0.25/0.53 % SZS output end Proof
% 0.25/0.53 % User time : 0.006 s
% 0.25/0.53 % System time : 0.002 s
% 0.25/0.53 % Total time : 0.009 s
% 0.25/0.53 % User time : 0.007 s
% 0.25/0.53 % System time : 0.006 s
% 0.25/0.53 % Total time : 0.014 s
% 0.25/0.53
%------------------------------------------------------------------------------