%------------------------------------------------------------------------------
% 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 : n003.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.51s
% 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.05/0.32 % Computer : n003.cluster.edu
% 0.05/0.32 % Model : x86_64 x86_64
% 0.05/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.05/0.32 % Memory : 8046.5625MB
% 0.05/0.32 % OS : Linux 6.8.0-71-generic
% 0.05/0.32 % CPULimit : 300
% 0.05/0.32 % WCLimit : 300
% 0.05/0.32 % DateTime : Mon Sep 7 13:26:54 UTC 2026
% 0.05/0.33 % CPUTime :
% 0.12/0.45 start to proof:theBenchmark.p
% 0.25/0.51 % Version : CSI_E---1.1
% 0.25/0.51 % Problem : theBenchmark.p
% 0.25/0.51 % Proof found!
% 0.25/0.51 # SZS status Unsatisfiable
% 0.25/0.51 % SZS output start Proof
% 0.25/0.51 cnf(assumption_15_50, axiom, (greater(age(X1,X3),sigma)|~organization(X1)|age(X1,X2)!=zero|~dissimilar(X1,X2,X3)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', assumption_15_50)).
% 0.25/0.51 cnf(definition_2_40, axiom, (organization(X1)|~dissimilar(X1,X2,X3)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', definition_2_40)).
% 0.25/0.51 cnf(definition_smaller_or_equal_1, axiom, (smaller(X1,X2)|X1=X2|~smaller_or_equal(X1,X2)), file('/export/starexec/sandbox/benchmark/Axioms/MGT001-0.ax', definition_smaller_or_equal_1)).
% 0.25/0.51 cnf(definition_2_44, axiom, (is_aligned(X1,X3)|dissimilar(X1,X2,X3)|~organization(X1)|~is_aligned(X1,X2)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', definition_2_44)).
% 0.25/0.51 cnf(assumption_13_47, axiom, (is_aligned(X1,X2)|~organization(X1)|age(X1,X2)!=zero), file('/export/starexec/sandbox/benchmark/theBenchmark.p', assumption_13_47)).
% 0.25/0.51 cnf(definition_smaller_7, axiom, (greater(X2,X1)|~smaller(X1,X2)), file('/export/starexec/sandbox/benchmark/Axioms/MGT001-0.ax', definition_smaller_7)).
% 0.25/0.51 cnf(theorem_5_55, negated_conjecture, (smaller_or_equal(age(sk1,sk3),sigma)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', theorem_5_55)).
% 0.25/0.51 cnf(meaning_postulate_greater_strict_9, axiom, (~greater(X1,X2)|~greater(X2,X1)), file('/export/starexec/sandbox/benchmark/Axioms/MGT001-0.ax', meaning_postulate_greater_strict_9)).
% 0.25/0.51 cnf(theorem_5_54, negated_conjecture, (age(sk1,sk2)=zero), file('/export/starexec/sandbox/benchmark/theBenchmark.p', theorem_5_54)).
% 0.25/0.51 cnf(theorem_5_52, negated_conjecture, (organization(sk1)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', theorem_5_52)).
% 0.25/0.51 cnf(definition_2_42, axiom, (~dissimilar(X1,X2,X3)|~is_aligned(X1,X2)|~is_aligned(X1,X3)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', definition_2_42)).
% 0.25/0.51 cnf(assumption_15_49, axiom, (dissimilar(X1,X2,X3)|~organization(X1)|age(X1,X2)!=zero|~greater(age(X1,X3),sigma)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', assumption_15_49)).
% 0.25/0.51 cnf(assumption_16_51, axiom, (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))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', assumption_16_51)).
% 0.25/0.51 cnf(assumption_3_39, axiom, (has_immunity(X1,X3)|greater(hazard_of_mortality(X1,X3),hazard_of_mortality(X1,X2))|~organization(X1)|~has_immunity(X1,X2)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', assumption_3_39)).
% 0.25/0.51 cnf(assumption_14_48, axiom, (is_aligned(X1,X3)|greater(capability(X1,X2),capability(X1,X3))|~organization(X1)|~is_aligned(X1,X2)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', assumption_14_48)).
% 0.25/0.51 cnf(theorem_5_56, negated_conjecture, (greater(age(sk1,sk4),sigma)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', theorem_5_56)).
% 0.25/0.51 cnf(theorem_5_58, negated_conjecture, (~greater(hazard_of_mortality(sk1,sk4),hazard_of_mortality(sk1,sk3))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', theorem_5_58)).
% 0.25/0.51 cnf(assumption_1_38, axiom, (has_endowment(X1)|~organization(X1)|~has_immunity(X1,X2)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', assumption_1_38)).
% 0.25/0.51 cnf(theorem_5_53, negated_conjecture, (~has_endowment(sk1)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', theorem_5_53)).
% 0.25/0.51 cnf(c_0_19, plain, (greater(age(X1,X3),sigma)|~organization(X1)|age(X1,X2)!=zero|~dissimilar(X1,X2,X3)), inference(fof_simplification,[status(thm)],[assumption_15_50])).
% 0.25/0.51 cnf(c_0_20, plain, (organization(X1)|~dissimilar(X1,X2,X3)), inference(fof_simplification,[status(thm)],[definition_2_40])).
% 0.25/0.51 cnf(c_0_21, plain, (smaller(X1,X2)|X1=X2|~smaller_or_equal(X1,X2)), inference(fof_simplification,[status(thm)],[definition_smaller_or_equal_1])).
% 0.25/0.51 cnf(c_0_22, plain, (greater(age(X1,X3),sigma)|~organization(X1)|age(X1,X2)!=zero|~dissimilar(X1,X2,X3)), c_0_19).
% 0.25/0.51 cnf(c_0_23, plain, (organization(X1)|~dissimilar(X1,X2,X3)), c_0_20).
% 0.25/0.51 cnf(c_0_24, plain, (is_aligned(X1,X3)|dissimilar(X1,X2,X3)|~organization(X1)|~is_aligned(X1,X2)), inference(fof_simplification,[status(thm)],[definition_2_44])).
% 0.25/0.51 cnf(c_0_25, plain, (is_aligned(X1,X2)|~organization(X1)|age(X1,X2)!=zero), inference(fof_simplification,[status(thm)],[assumption_13_47])).
% 0.25/0.51 cnf(c_0_26, plain, (greater(X2,X1)|~smaller(X1,X2)), inference(fof_simplification,[status(thm)],[definition_smaller_7])).
% 0.25/0.51 cnf(c_0_27, plain, (smaller(X1,X2)|X1=X2|~smaller_or_equal(X1,X2)), c_0_21).
% 0.25/0.51 cnf(c_0_28, negated_conjecture, (smaller_or_equal(age(sk1,sk3),sigma)), theorem_5_55).
% 0.25/0.51 cnf(c_0_29, plain, (greater(age(X1,X2),sigma)|age(X1,X3)!=zero|~dissimilar(X1,X3,X2)), inference(csr,[status(thm)],[c_0_22, c_0_23])).
% 0.25/0.51 cnf(c_0_30, plain, (is_aligned(X1,X3)|dissimilar(X1,X2,X3)|~organization(X1)|~is_aligned(X1,X2)), c_0_24).
% 0.25/0.51 cnf(c_0_31, plain, (is_aligned(X1,X2)|~organization(X1)|age(X1,X2)!=zero), c_0_25).
% 0.25/0.51 cnf(c_0_32, plain, (~greater(X1,X2)|~greater(X2,X1)), inference(fof_simplification,[status(thm)],[meaning_postulate_greater_strict_9])).
% 0.25/0.51 cnf(c_0_33, plain, (greater(X2,X1)|~smaller(X1,X2)), c_0_26).
% 0.25/0.51 cnf(c_0_34, negated_conjecture, (age(sk1,sk3)=sigma|smaller(age(sk1,sk3),sigma)), inference(spm,[status(thm)],[c_0_27, c_0_28])).
% 0.25/0.51 cnf(c_0_35, 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_29, c_0_30]), c_0_31])).
% 0.25/0.51 cnf(c_0_36, negated_conjecture, (age(sk1,sk2)=zero), theorem_5_54).
% 0.25/0.51 cnf(c_0_37, negated_conjecture, (organization(sk1)), theorem_5_52).
% 0.25/0.51 cnf(c_0_38, plain, (~greater(X1,X2)|~greater(X2,X1)), c_0_32).
% 0.25/0.51 cnf(c_0_39, negated_conjecture, (age(sk1,sk3)=sigma|greater(sigma,age(sk1,sk3))), inference(spm,[status(thm)],[c_0_33, c_0_34])).
% 0.25/0.51 cnf(c_0_40, plain, (~dissimilar(X1,X2,X3)|~is_aligned(X1,X2)|~is_aligned(X1,X3)), inference(fof_simplification,[status(thm)],[definition_2_42])).
% 0.25/0.51 cnf(c_0_41, plain, (dissimilar(X1,X2,X3)|~organization(X1)|age(X1,X2)!=zero|~greater(age(X1,X3),sigma)), inference(fof_simplification,[status(thm)],[assumption_15_49])).
% 0.25/0.51 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(fof_simplification,[status(thm)],[assumption_16_51])).
% 0.25/0.51 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(fof_simplification,[status(thm)],[assumption_3_39])).
% 0.25/0.51 cnf(c_0_44, negated_conjecture, (is_aligned(sk1,X1)|greater(age(sk1,X1),sigma)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_35, c_0_36]), c_0_37])])).
% 0.25/0.51 cnf(c_0_45, negated_conjecture, (age(sk1,sk3)=sigma|~greater(age(sk1,sk3),sigma)), inference(spm,[status(thm)],[c_0_38, c_0_39])).
% 0.25/0.51 cnf(c_0_46, plain, (~dissimilar(X1,X2,X3)|~is_aligned(X1,X2)|~is_aligned(X1,X3)), c_0_40).
% 0.25/0.51 cnf(c_0_47, plain, (dissimilar(X1,X2,X3)|~organization(X1)|age(X1,X2)!=zero|~greater(age(X1,X3),sigma)), c_0_41).
% 0.25/0.51 cnf(c_0_48, 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))), c_0_42).
% 0.25/0.51 cnf(c_0_49, plain, (has_immunity(X1,X3)|greater(hazard_of_mortality(X1,X3),hazard_of_mortality(X1,X2))|~organization(X1)|~has_immunity(X1,X2)), c_0_43).
% 0.25/0.51 cnf(c_0_50, plain, (is_aligned(X1,X3)|greater(capability(X1,X2),capability(X1,X3))|~organization(X1)|~is_aligned(X1,X2)), inference(fof_simplification,[status(thm)],[assumption_14_48])).
% 0.25/0.51 cnf(c_0_51, negated_conjecture, (is_aligned(sk1,X1)|~greater(sigma,age(sk1,X1))), inference(spm,[status(thm)],[c_0_38, c_0_44])).
% 0.25/0.51 cnf(c_0_52, negated_conjecture, (age(sk1,sk3)=sigma|is_aligned(sk1,sk3)), inference(spm,[status(thm)],[c_0_45, c_0_44])).
% 0.25/0.51 cnf(c_0_53, 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_46, c_0_47]), c_0_31])).
% 0.25/0.51 cnf(c_0_54, negated_conjecture, (greater(age(sk1,sk4),sigma)), theorem_5_56).
% 0.25/0.51 cnf(c_0_55, negated_conjecture, (~greater(hazard_of_mortality(sk1,sk4),hazard_of_mortality(sk1,sk3))), inference(fof_simplification,[status(thm)],[theorem_5_58])).
% 0.25/0.51 cnf(c_0_56, 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_48, c_0_49])).
% 0.25/0.51 cnf(c_0_57, plain, (is_aligned(X1,X3)|greater(capability(X1,X2),capability(X1,X3))|~organization(X1)|~is_aligned(X1,X2)), c_0_50).
% 0.25/0.51 cnf(c_0_58, negated_conjecture, (is_aligned(sk1,sk3)|~greater(sigma,sigma)), inference(spm,[status(thm)],[c_0_51, c_0_52])).
% 0.25/0.51 cnf(c_0_59, negated_conjecture, (age(sk1,X1)!=zero|~is_aligned(sk1,sk4)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_53, c_0_54]), c_0_37])])).
% 0.25/0.51 cnf(c_0_60, plain, (has_endowment(X1)|~organization(X1)|~has_immunity(X1,X2)), inference(fof_simplification,[status(thm)],[assumption_1_38])).
% 0.25/0.51 cnf(c_0_61, negated_conjecture, (~greater(hazard_of_mortality(sk1,sk4),hazard_of_mortality(sk1,sk3))), c_0_55).
% 0.25/0.51 cnf(c_0_62, 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_56, c_0_57])).
% 0.25/0.51 cnf(c_0_63, negated_conjecture, (is_aligned(sk1,sk3)), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_44, c_0_52]), c_0_58])).
% 0.25/0.51 cnf(c_0_64, negated_conjecture, (~is_aligned(sk1,sk4)), inference(spm,[status(thm)],[c_0_59, c_0_36])).
% 0.25/0.51 cnf(c_0_65, negated_conjecture, (~has_endowment(sk1)), inference(fof_simplification,[status(thm)],[theorem_5_53])).
% 0.25/0.51 cnf(c_0_66, plain, (has_endowment(X1)|~organization(X1)|~has_immunity(X1,X2)), c_0_60).
% 0.25/0.51 cnf(c_0_67, negated_conjecture, (has_immunity(sk1,sk4)), inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_61, c_0_62]), c_0_63]), c_0_37])]), c_0_64])).
% 0.25/0.51 cnf(c_0_68, negated_conjecture, (~has_endowment(sk1)), c_0_65).
% 0.25/0.51 cnf(c_0_69, negated_conjecture, ($false), inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_66, c_0_67]), c_0_37])]), c_0_68]), ['proof']).
% 0.25/0.51 % SZS output end Proof
% 0.25/0.51 % User time : 0.014 s
% 0.25/0.51 % System time : 0.002 s
% 0.25/0.51 % Total time : 0.015 s
% 0.25/0.51 % User time : 0.015 s
% 0.25/0.51 % System time : 0.006 s
% 0.25/0.51 % Total time : 0.021 s
% 0.25/0.51
%------------------------------------------------------------------------------