%------------------------------------------------------------------------------
% File : CSI_E---1.1
% Problem : MGT054+1 : TPTP v9.3.0. Released v2.4.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:35 AM UTC 2026
% Result : Theorem 0.23s 0.54s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : MGT054+1 : TPTP v9.3.0. Released v2.4.0.
% 0.00/0.02 % Command : java -jar mcs_scs.jar %d %s
% 0.08/0.34 % Computer : n013.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:24:35 UTC 2026
% 0.08/0.34 % CPUTime :
% 0.12/0.46 start to proof:theBenchmark.p
% 0.23/0.54 % Version : CSI_E---1.1
% 0.23/0.54 % Problem : theBenchmark.p
% 0.23/0.54 % Proof found!
% 0.23/0.54 % SZS status Theorem for theBenchmark.p
% 0.23/0.54 % SZS output start Proof
% 0.23/0.54 fof(theorem_5, conjecture, ![X1, X5, X6, X7]:(((((((organization(X1)&~(has_endowment(X1)))&age(X1,X5)=zero)&smaller_or_equal(age(X1,X6),sigma))&greater(age(X1,X7),sigma))&greater(sigma,zero))=>greater(hazard_of_mortality(X1,X7),hazard_of_mortality(X1,X6)))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', theorem_5)).
% 0.23/0.54 fof(assumption_15, axiom, ![X1, X5, X4]:(((organization(X1)&age(X1,X5)=zero)=>(greater(age(X1,X4),sigma)<=>dissimilar(X1,X5,X4)))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', assumption_15)).
% 0.23/0.54 fof(definition_2, axiom, ![X1, X5, X4]:((dissimilar(X1,X5,X4)<=>(organization(X1)&~((is_aligned(X1,X5)<=>is_aligned(X1,X4)))))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', definition_2)).
% 0.23/0.54 fof(definition_smaller_or_equal, axiom, ![X1, X2]:((smaller_or_equal(X1,X2)<=>(smaller(X1,X2)|X1=X2))), file('/export/starexec/sandbox/benchmark/Axioms/MGT001+0.ax', definition_smaller_or_equal)).
% 0.23/0.54 fof(assumption_13, axiom, ![X1, X4]:(((organization(X1)&age(X1,X4)=zero)=>is_aligned(X1,X4))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', assumption_13)).
% 0.23/0.54 fof(definition_smaller, axiom, ![X1, X2]:((smaller(X1,X2)<=>greater(X2,X1))), file('/export/starexec/sandbox/benchmark/Axioms/MGT001+0.ax', definition_smaller)).
% 0.23/0.54 fof(meaning_postulate_greater_strict, axiom, ![X1, X2]:(~((greater(X1,X2)&greater(X2,X1)))), file('/export/starexec/sandbox/benchmark/Axioms/MGT001+0.ax', meaning_postulate_greater_strict)).
% 0.23/0.54 fof(assumption_16, axiom, ![X1, X5, X4]:(((((organization(X1)&~(has_immunity(X1,X5)))&~(has_immunity(X1,X4)))&greater(capability(X1,X4),capability(X1,X5)))=>greater(hazard_of_mortality(X1,X5),hazard_of_mortality(X1,X4)))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', assumption_16)).
% 0.23/0.54 fof(assumption_3, axiom, ![X1, X5, X4]:((((organization(X1)&has_immunity(X1,X5))&~(has_immunity(X1,X4)))=>greater(hazard_of_mortality(X1,X4),hazard_of_mortality(X1,X5)))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', assumption_3)).
% 0.23/0.54 fof(assumption_14, axiom, ![X1, X5, X4]:((((organization(X1)&is_aligned(X1,X5))&~(is_aligned(X1,X4)))=>greater(capability(X1,X5),capability(X1,X4)))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', assumption_14)).
% 0.23/0.54 fof(assumption_1, axiom, ![X1, X4]:(((organization(X1)&~(has_endowment(X1)))=>~(has_immunity(X1,X4)))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', assumption_1)).
% 0.23/0.54 fof(c_0_11, negated_conjecture, ~(![X1, X5, X6, X7]:(((((((organization(X1)&~has_endowment(X1))&age(X1,X5)=zero)&smaller_or_equal(age(X1,X6),sigma))&greater(age(X1,X7),sigma))&greater(sigma,zero))=>greater(hazard_of_mortality(X1,X7),hazard_of_mortality(X1,X6))))), inference(fof_simplification,[status(thm)],[inference(assume_negation,[status(cth)],[theorem_5])])).
% 0.23/0.54 fof(c_0_12, plain, ![X34, X35, X36]:(((~greater(age(X34,X36),sigma)|dissimilar(X34,X35,X36)|(~organization(X34)|age(X34,X35)!=zero))&(~dissimilar(X34,X35,X36)|greater(age(X34,X36),sigma)|(~organization(X34)|age(X34,X35)!=zero)))), inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[assumption_15])])])])).
% 0.23/0.54 fof(c_0_13, plain, ![X26, X27, X28]:((((organization(X26)|~dissimilar(X26,X27,X28))&((~is_aligned(X26,X27)|~is_aligned(X26,X28)|~dissimilar(X26,X27,X28))&(is_aligned(X26,X27)|is_aligned(X26,X28)|~dissimilar(X26,X27,X28))))&((~is_aligned(X26,X27)|is_aligned(X26,X28)|~organization(X26)|dissimilar(X26,X27,X28))&(~is_aligned(X26,X28)|is_aligned(X26,X27)|~organization(X26)|dissimilar(X26,X27,X28))))), inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[definition_2])])])])).
% 0.23/0.54 fof(c_0_14, plain, ![X8, X9]:(((~smaller_or_equal(X8,X9)|(smaller(X8,X9)|X8=X9))&((~smaller(X8,X9)|smaller_or_equal(X8,X9))&(X8!=X9|smaller_or_equal(X8,X9))))), inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[definition_smaller_or_equal])])])])).
% 0.23/0.54 fof(c_0_15, negated_conjecture, ((((((organization(esk1_0)&~has_endowment(esk1_0))&age(esk1_0,esk2_0)=zero)&smaller_or_equal(age(esk1_0,esk3_0),sigma))&greater(age(esk1_0,esk4_0),sigma))&greater(sigma,zero))&~greater(hazard_of_mortality(esk1_0,esk4_0),hazard_of_mortality(esk1_0,esk3_0))), inference(fof_nnf,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_11])])])])).
% 0.23/0.54 cnf(c_0_16, plain, (greater(age(X1,X3),sigma)|~dissimilar(X1,X2,X3)|~organization(X1)|age(X1,X2)!=zero), inference(split_conjunct,[status(thm)],[c_0_12])).
% 0.23/0.54 cnf(c_0_17, plain, (organization(X1)|~dissimilar(X1,X2,X3)), inference(split_conjunct,[status(thm)],[c_0_13])).
% 0.23/0.54 fof(c_0_18, plain, ![X29, X30]:((~organization(X29)|age(X29,X30)!=zero|is_aligned(X29,X30))), inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[assumption_13])])])).
% 0.23/0.54 fof(c_0_19, plain, ![X12, X13]:(((~smaller(X12,X13)|greater(X13,X12))&(~greater(X13,X12)|smaller(X12,X13)))), inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[definition_smaller])])])).
% 0.23/0.54 cnf(c_0_20, plain, (smaller(X1,X2)|X1=X2|~smaller_or_equal(X1,X2)), inference(split_conjunct,[status(thm)],[c_0_14])).
% 0.23/0.54 cnf(c_0_21, negated_conjecture, (smaller_or_equal(age(esk1_0,esk3_0),sigma)), inference(split_conjunct,[status(thm)],[c_0_15])).
% 0.23/0.54 cnf(c_0_22, plain, (greater(age(X1,X2),sigma)|age(X1,X3)!=zero|~dissimilar(X1,X3,X2)), inference(csr,[status(thm)],[c_0_16, c_0_17])).
% 0.23/0.54 cnf(c_0_23, plain, (is_aligned(X1,X3)|dissimilar(X1,X2,X3)|~is_aligned(X1,X2)|~organization(X1)), inference(split_conjunct,[status(thm)],[c_0_13])).
% 0.23/0.54 cnf(c_0_24, plain, (is_aligned(X1,X2)|~organization(X1)|age(X1,X2)!=zero), inference(split_conjunct,[status(thm)],[c_0_18])).
% 0.23/0.54 fof(c_0_25, plain, ![X14, X15]:((~greater(X14,X15)|~greater(X15,X14))), inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[meaning_postulate_greater_strict])])])).
% 0.23/0.54 cnf(c_0_26, plain, (greater(X2,X1)|~smaller(X1,X2)), inference(split_conjunct,[status(thm)],[c_0_19])).
% 0.23/0.54 cnf(c_0_27, negated_conjecture, (age(esk1_0,esk3_0)=sigma|smaller(age(esk1_0,esk3_0),sigma)), inference(spm,[status(thm)],[c_0_20, c_0_21])).
% 0.23/0.54 fof(c_0_28, plain, ![X1, X5, X4]:(((((organization(X1)&~has_immunity(X1,X5))&~has_immunity(X1,X4))&greater(capability(X1,X4),capability(X1,X5)))=>greater(hazard_of_mortality(X1,X5),hazard_of_mortality(X1,X4)))), inference(fof_simplification,[status(thm)],[assumption_16])).
% 0.23/0.54 fof(c_0_29, plain, ![X1, X5, X4]:((((organization(X1)&has_immunity(X1,X5))&~has_immunity(X1,X4))=>greater(hazard_of_mortality(X1,X4),hazard_of_mortality(X1,X5)))), inference(fof_simplification,[status(thm)],[assumption_3])).
% 0.23/0.54 cnf(c_0_30, plain, (is_aligned(X1,X2)|greater(age(X1,X2),sigma)|age(X1,X3)!=zero|~organization(X1)), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_22, c_0_23]), c_0_24])).
% 0.23/0.54 cnf(c_0_31, negated_conjecture, (age(esk1_0,esk2_0)=zero), inference(split_conjunct,[status(thm)],[c_0_15])).
% 0.23/0.54 cnf(c_0_32, negated_conjecture, (organization(esk1_0)), inference(split_conjunct,[status(thm)],[c_0_15])).
% 0.23/0.54 cnf(c_0_33, plain, (~greater(X1,X2)|~greater(X2,X1)), inference(split_conjunct,[status(thm)],[c_0_25])).
% 0.23/0.54 cnf(c_0_34, negated_conjecture, (age(esk1_0,esk3_0)=sigma|greater(sigma,age(esk1_0,esk3_0))), inference(spm,[status(thm)],[c_0_26, c_0_27])).
% 0.23/0.54 fof(c_0_35, plain, ![X37, X38, X39]:((~organization(X37)|has_immunity(X37,X38)|has_immunity(X37,X39)|~greater(capability(X37,X39),capability(X37,X38))|greater(hazard_of_mortality(X37,X38),hazard_of_mortality(X37,X39)))), inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_28])])])).
% 0.23/0.54 fof(c_0_36, plain, ![X23, X24, X25]:((~organization(X23)|~has_immunity(X23,X24)|has_immunity(X23,X25)|greater(hazard_of_mortality(X23,X25),hazard_of_mortality(X23,X24)))), inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_29])])])).
% 0.23/0.54 fof(c_0_37, plain, ![X1, X5, X4]:((((organization(X1)&is_aligned(X1,X5))&~is_aligned(X1,X4))=>greater(capability(X1,X5),capability(X1,X4)))), inference(fof_simplification,[status(thm)],[assumption_14])).
% 0.23/0.54 cnf(c_0_38, negated_conjecture, (is_aligned(esk1_0,X1)|greater(age(esk1_0,X1),sigma)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_30, c_0_31]), c_0_32])])).
% 0.23/0.54 cnf(c_0_39, negated_conjecture, (age(esk1_0,esk3_0)=sigma|~greater(age(esk1_0,esk3_0),sigma)), inference(spm,[status(thm)],[c_0_33, c_0_34])).
% 0.23/0.54 cnf(c_0_40, plain, (~is_aligned(X1,X2)|~is_aligned(X1,X3)|~dissimilar(X1,X2,X3)), inference(split_conjunct,[status(thm)],[c_0_13])).
% 0.23/0.54 cnf(c_0_41, plain, (dissimilar(X1,X3,X2)|~greater(age(X1,X2),sigma)|~organization(X1)|age(X1,X3)!=zero), inference(split_conjunct,[status(thm)],[c_0_12])).
% 0.23/0.54 cnf(c_0_42, plain, (has_immunity(X1,X2)|has_immunity(X1,X3)|greater(hazard_of_mortality(X1,X2),hazard_of_mortality(X1,X3))|~organization(X1)|~greater(capability(X1,X3),capability(X1,X2))), inference(split_conjunct,[status(thm)],[c_0_35])).
% 0.23/0.54 cnf(c_0_43, plain, (has_immunity(X1,X3)|greater(hazard_of_mortality(X1,X3),hazard_of_mortality(X1,X2))|~organization(X1)|~has_immunity(X1,X2)), inference(split_conjunct,[status(thm)],[c_0_36])).
% 0.23/0.54 fof(c_0_44, plain, ![X31, X32, X33]:((~organization(X31)|~is_aligned(X31,X32)|is_aligned(X31,X33)|greater(capability(X31,X32),capability(X31,X33)))), inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_37])])])).
% 0.23/0.54 cnf(c_0_45, negated_conjecture, (is_aligned(esk1_0,X1)|~greater(sigma,age(esk1_0,X1))), inference(spm,[status(thm)],[c_0_33, c_0_38])).
% 0.23/0.54 cnf(c_0_46, negated_conjecture, (age(esk1_0,esk3_0)=sigma|is_aligned(esk1_0,esk3_0)), inference(spm,[status(thm)],[c_0_39, c_0_38])).
% 0.23/0.54 cnf(c_0_47, plain, (age(X1,X2)!=zero|~is_aligned(X1,X3)|~organization(X1)|~greater(age(X1,X3),sigma)), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_40, c_0_41]), c_0_24])).
% 0.23/0.54 cnf(c_0_48, negated_conjecture, (greater(age(esk1_0,esk4_0),sigma)), inference(split_conjunct,[status(thm)],[c_0_15])).
% 0.23/0.54 fof(c_0_49, plain, ![X1, X4]:(((organization(X1)&~has_endowment(X1))=>~has_immunity(X1,X4))), inference(fof_simplification,[status(thm)],[assumption_1])).
% 0.23/0.54 cnf(c_0_50, plain, (has_immunity(X1,X2)|greater(hazard_of_mortality(X1,X2),hazard_of_mortality(X1,X3))|~organization(X1)|~greater(capability(X1,X3),capability(X1,X2))), inference(csr,[status(thm)],[c_0_42, c_0_43])).
% 0.23/0.54 cnf(c_0_51, plain, (is_aligned(X1,X3)|greater(capability(X1,X2),capability(X1,X3))|~organization(X1)|~is_aligned(X1,X2)), inference(split_conjunct,[status(thm)],[c_0_44])).
% 0.23/0.54 cnf(c_0_52, negated_conjecture, (is_aligned(esk1_0,esk3_0)|~greater(sigma,sigma)), inference(spm,[status(thm)],[c_0_45, c_0_46])).
% 0.23/0.54 cnf(c_0_53, negated_conjecture, (age(esk1_0,X1)!=zero|~is_aligned(esk1_0,esk4_0)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_47, c_0_48]), c_0_32])])).
% 0.23/0.54 fof(c_0_54, plain, ![X21, X22]:((~organization(X21)|has_endowment(X21)|~has_immunity(X21,X22))), inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_49])])])).
% 0.23/0.54 cnf(c_0_55, negated_conjecture, (~greater(hazard_of_mortality(esk1_0,esk4_0),hazard_of_mortality(esk1_0,esk3_0))), inference(split_conjunct,[status(thm)],[c_0_15])).
% 0.23/0.54 cnf(c_0_56, plain, (is_aligned(X1,X2)|has_immunity(X1,X2)|greater(hazard_of_mortality(X1,X2),hazard_of_mortality(X1,X3))|~is_aligned(X1,X3)|~organization(X1)), inference(spm,[status(thm)],[c_0_50, c_0_51])).
% 0.23/0.54 cnf(c_0_57, negated_conjecture, (is_aligned(esk1_0,esk3_0)), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_38, c_0_46]), c_0_52])).
% 0.23/0.54 cnf(c_0_58, negated_conjecture, (~is_aligned(esk1_0,esk4_0)), inference(spm,[status(thm)],[c_0_53, c_0_31])).
% 0.23/0.54 cnf(c_0_59, plain, (has_endowment(X1)|~organization(X1)|~has_immunity(X1,X2)), inference(split_conjunct,[status(thm)],[c_0_54])).
% 0.23/0.54 cnf(c_0_60, negated_conjecture, (has_immunity(esk1_0,esk4_0)), inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_55, c_0_56]), c_0_57]), c_0_32])]), c_0_58])).
% 0.23/0.54 cnf(c_0_61, negated_conjecture, (~has_endowment(esk1_0)), inference(split_conjunct,[status(thm)],[c_0_15])).
% 0.23/0.54 cnf(c_0_62, negated_conjecture, ($false), inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_59, c_0_60]), c_0_32])]), c_0_61]), ['proof']).
% 0.23/0.54 % SZS output end Proof
% 0.23/0.54 % User time : 0.013 s
% 0.23/0.54 % System time : 0.006 s
% 0.23/0.54 % Total time : 0.019 s
% 0.23/0.54 % User time : 0.052 s
% 0.23/0.54 % System time : 0.018 s
% 0.23/0.54 % Total time : 0.070 s
% 0.23/0.54
%------------------------------------------------------------------------------