%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : MGT046-1 : TPTP v9.3.0. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% Computer : n014.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:20 AM UTC 2026
% Result : Unsatisfiable 4.56s 4.73s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : MGT046-1 : TPTP v9.3.0. Released v2.4.0.
% 0.00/0.02 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% 0.06/0.33 % Computer : n014.cluster.edu
% 0.06/0.33 % Model : x86_64 x86_64
% 0.06/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.06/0.33 % Memory : 8046.5625MB
% 0.06/0.33 % OS : Linux 6.8.0-71-generic
% 0.06/0.33 % CPULimit : 300
% 0.06/0.33 % WCLimit : 300
% 0.06/0.33 % DateTime : Mon Sep 7 13:11:11 UTC 2026
% 0.06/0.33 % CPUTime :
% 0.25/0.50 start to proof:theBenchmark
% 4.56/4.72 %-------------------------------------------
% 4.56/4.72 % File :CSE---1.7
% 4.56/4.72 % Problem :theBenchmark
% 4.56/4.72 % Transform :cnf
% 4.56/4.72 % Format :tptp:raw
% 4.56/4.72 % Command :java -jar mcs_scs.jar %d %s
% 4.56/4.72
% 4.56/4.72 % Result :Theorem 4.241420s
% 4.56/4.72 % Output :CNFRefutation 4.241420s
% 4.56/4.72 %-------------------------------------------
% 4.56/4.72 %--------------------------------------------------------------------------
% 4.56/4.72 % File : MGT046-1 : TPTP v9.3.0. Released v2.4.0.
% 4.56/4.72 % Domain : Management (Organisation Theory)
% 4.56/4.72 % Problem : Unendowed organization's hazard of mortality declines with age
% 4.56/4.72 % Version : [Han98] axioms.
% 4.56/4.72 % English : An unendowed organization's hazard of mortality declines
% 4.56/4.72 % monotonically with its age.
% 4.56/4.72
% 4.56/4.72 % Refs : [Kam00] Kamps (2000), Email to G. Sutcliffe
% 4.56/4.72 % : [CH00] Carroll & Hannan (2000), The Demography of Corporation
% 4.56/4.72 % : [Han98] Hannan (1998), Rethinking Age Dependence in Organizati
% 4.56/4.72 % Source : [TPTP]
% 4.56/4.72 % Names :
% 4.56/4.72
% 4.56/4.72 % Status : Unsatisfiable
% 4.56/4.72 % Rating : 0.17 v9.3.0, 0.00 v9.0.0, 0.05 v8.1.0, 0.00 v7.0.0, 0.07 v6.4.0, 0.00 v5.5.0, 0.15 v5.4.0, 0.20 v5.3.0, 0.17 v5.2.0, 0.12 v5.0.0, 0.07 v4.1.0, 0.00 v3.3.0, 0.14 v3.2.0, 0.08 v3.1.0, 0.09 v2.7.0, 0.17 v2.6.0, 0.00 v2.5.0, 0.22 v2.4.0
% 4.56/4.72 % Syntax : Number of clauses : 27 ( 4 unt; 6 nHn; 25 RR)
% 4.56/4.72 % Number of literals : 77 ( 14 equ; 43 neg)
% 4.56/4.72 % Maximal clause size : 6 ( 2 avg)
% 4.56/4.73 % Maximal term depth : 2 ( 1 avg)
% 4.56/4.73 % Number of predicates : 8 ( 7 usr; 0 prp; 1-2 aty)
% 4.56/4.73 % Number of functors : 10 ( 10 usr; 3 con; 0-2 aty)
% 4.56/4.73 % Number of variables : 58 ( 3 sgn)
% 4.56/4.73 % SPC : CNF_UNS_RFO_SEQ_NHN
% 4.56/4.73
% 4.56/4.73 % Comments : See MGT042+1.p for the mnemonic names.
% 4.56/4.73 % : Created with tptp2X -f tptp -t clausify:otter MGT046+1.p
% 4.56/4.73 %--------------------------------------------------------------------------
% 4.56/4.73 include('Axioms/MGT001-0.ax').
% 4.56/4.73 %--------------------------------------------------------------------------
% 4.56/4.73 cnf(assumption_1_41,axiom,
% 4.56/4.73 ( ~ organization(A)
% 4.56/4.73 | has_endowment(A)
% 4.56/4.73 | ~ has_immunity(A,B) ) ).
% 4.56/4.73
% 4.56/4.73 cnf(assumption_4_42,axiom,
% 4.56/4.73 ( ~ organization(A)
% 4.56/4.73 | has_immunity(A,B)
% 4.56/4.73 | has_immunity(A,C)
% 4.56/4.73 | ~ greater(capability(A,C),capability(A,B))
% 4.56/4.73 | ~ greater_or_equal(position(A,C),position(A,B))
% 4.56/4.73 | smaller(hazard_of_mortality(A,C),hazard_of_mortality(A,B)) ) ).
% 4.56/4.73
% 4.56/4.73 cnf(assumption_4_43,axiom,
% 4.56/4.73 ( ~ organization(A)
% 4.56/4.73 | has_immunity(A,B)
% 4.56/4.73 | has_immunity(A,C)
% 4.56/4.73 | ~ greater_or_equal(capability(A,C),capability(A,B))
% 4.56/4.73 | ~ greater(position(A,C),position(A,B))
% 4.56/4.73 | smaller(hazard_of_mortality(A,C),hazard_of_mortality(A,B)) ) ).
% 4.56/4.73
% 4.56/4.73 cnf(assumption_4_44,axiom,
% 4.56/4.73 ( ~ organization(A)
% 4.56/4.73 | has_immunity(A,B)
% 4.56/4.73 | has_immunity(A,C)
% 4.56/4.73 | capability(A,C) != capability(A,B)
% 4.56/4.73 | position(A,C) != position(A,B)
% 4.56/4.73 | hazard_of_mortality(A,C) = hazard_of_mortality(A,B) ) ).
% 4.56/4.73
% 4.56/4.73 cnf(assumption_5_45,axiom,
% 4.56/4.73 ( ~ organization(A)
% 4.56/4.73 | ~ greater(stock_of_knowledge(A,B),stock_of_knowledge(A,C))
% 4.56/4.73 | ~ smaller_or_equal(internal_friction(A,B),internal_friction(A,C))
% 4.56/4.73 | greater(capability(A,B),capability(A,C)) ) ).
% 4.56/4.73
% 4.56/4.73 cnf(assumption_5_46,axiom,
% 4.56/4.73 ( ~ organization(A)
% 4.56/4.73 | ~ smaller_or_equal(stock_of_knowledge(A,B),stock_of_knowledge(A,C))
% 4.56/4.73 | ~ greater(internal_friction(A,B),internal_friction(A,C))
% 4.56/4.73 | smaller(capability(A,B),capability(A,C)) ) ).
% 4.56/4.73
% 4.56/4.73 cnf(assumption_5_47,axiom,
% 4.56/4.73 ( ~ organization(A)
% 4.56/4.73 | stock_of_knowledge(A,B) != stock_of_knowledge(A,C)
% 4.56/4.73 | internal_friction(A,B) != internal_friction(A,C)
% 4.56/4.73 | capability(A,B) = capability(A,C) ) ).
% 4.56/4.73
% 4.56/4.73 cnf(assumption_6_48,axiom,
% 4.56/4.73 ( ~ organization(A)
% 4.56/4.73 | ~ greater(external_ties(A,B),external_ties(A,C))
% 4.56/4.73 | greater(position(A,B),position(A,C)) ) ).
% 4.56/4.73
% 4.56/4.73 cnf(assumption_6_49,axiom,
% 4.56/4.73 ( ~ organization(A)
% 4.56/4.73 | external_ties(A,B) != external_ties(A,C)
% 4.56/4.73 | position(A,B) = position(A,C) ) ).
% 4.56/4.73
% 4.56/4.73 cnf(assumption_7_50,axiom,
% 4.56/4.73 ( ~ organization(A)
% 4.56/4.73 | ~ greater(age(A,B),age(A,C))
% 4.56/4.73 | greater(stock_of_knowledge(A,B),stock_of_knowledge(A,C)) ) ).
% 4.56/4.73
% 4.56/4.73 cnf(assumption_8_51,axiom,
% 4.56/4.73 ( ~ organization(A)
% 4.56/4.73 | ~ greater(age(A,B),age(A,C))
% 4.56/4.73 | greater(external_ties(A,B),external_ties(A,C)) ) ).
% 4.56/4.73
% 4.56/4.73 cnf(assumption_9_52,axiom,
% 4.56/4.73 ( ~ organization(A)
% 4.56/4.73 | internal_friction(A,B) = internal_friction(A,C) ) ).
% 4.56/4.73
% 4.56/4.73 cnf(theorem_1_53,negated_conjecture,
% 4.56/4.73 organization(sk1) ).
% 4.56/4.73
% 4.56/4.73 cnf(theorem_1_54,negated_conjecture,
% 4.56/4.73 ~ has_endowment(sk1) ).
% 4.56/4.73
% 4.56/4.73 cnf(theorem_1_55,negated_conjecture,
% 4.56/4.73 greater(age(sk1,sk3),age(sk1,sk2)) ).
% 4.56/4.73
% 4.56/4.73 cnf(theorem_1_56,negated_conjecture,
% 4.56/4.73 ~ smaller(hazard_of_mortality(sk1,sk3),hazard_of_mortality(sk1,sk2)) ).
% 4.56/4.73
% 4.56/4.73 %--------------------------------------------------------------------------
% 4.56/4.73 %-------------------------------------------
% 4.56/4.73 % Proof found
% 4.56/4.73 % SZS status Theorem for theBenchmark
% 4.56/4.73 % SZS output start Proof
% 4.56/4.73 %ClaNum:56(EqnAxiom:29)
% 4.56/4.73 %VarNum:187(SingletonVarNum:58)
% 4.56/4.73 %MaxLitNum:6
% 4.56/4.73 %MaxfuncDepth:1
% 4.56/4.73 %SharedTerms:11
% 4.56/4.73 %goalClause: 30 31 32 33
% 4.56/4.73 %singleGoalClaCount:4
% 4.56/4.73 [30]P1(a1)
% 4.56/4.73 [32]~P3(a1)
% 4.56/4.73 [31]P2(f2(a1,a8),f2(a1,a9))
% 4.56/4.73 [33]~P6(f3(a1,a8),f3(a1,a9))
% 4.56/4.73 [34]~E(x341,x342)+P7(x341,x342)
% 4.56/4.73 [35]~E(x351,x352)+P4(x351,x352)
% 4.56/4.73 [39]~P6(x391,x392)+P7(x391,x392)
% 4.56/4.73 [40]~P2(x402,x401)+P6(x401,x402)
% 4.56/4.73 [41]~P2(x411,x412)+P4(x411,x412)
% 4.56/4.73 [42]~P6(x422,x421)+P2(x421,x422)
% 4.56/4.73 [45]~P2(x452,x451)+~P2(x451,x452)
% 4.56/4.73 [38]~P1(x381)+E(f6(x381,x382),f6(x381,x383))
% 4.56/4.73 [36]P6(x361,x362)+P2(x361,x362)+E(x361,x362)
% 4.56/4.73 [37]~P1(x371)+P3(x371)+~P5(x371,x372)
% 4.56/4.73 [43]P6(x431,x432)+~P7(x431,x432)+E(x431,x432)
% 4.56/4.73 [44]P2(x441,x442)+~P4(x441,x442)+E(x441,x442)
% 4.56/4.73 [46]~P2(x461,x463)+P2(x461,x462)+~P2(x463,x462)
% 4.56/4.73 [47]~P1(x471)+~E(f4(x471,x472),f4(x471,x473))+E(f7(x471,x472),f7(x471,x473))
% 4.56/4.73 [50]~P1(x501)+~P2(f4(x501,x502),f4(x501,x503))+P2(f7(x501,x502),f7(x501,x503))
% 4.56/4.73 [51]~P1(x511)+~P2(f2(x511,x512),f2(x511,x513))+P2(f10(x511,x512),f10(x511,x513))
% 4.56/4.73 [52]~P1(x521)+~P2(f2(x521,x522),f2(x521,x523))+P2(f4(x521,x522),f4(x521,x523))
% 4.56/4.73 [48]~P1(x481)+~E(f10(x481,x482),f10(x481,x483))+~E(f6(x481,x482),f6(x481,x483))+E(f5(x481,x482),f5(x481,x483))
% 4.56/4.73 [53]~P1(x531)+~P7(f10(x531,x532),f10(x531,x533))+~P2(f6(x531,x532),f6(x531,x533))+P6(f5(x531,x532),f5(x531,x533))
% 4.56/4.73 [54]~P1(x541)+~P7(f6(x541,x542),f6(x541,x543))+~P2(f10(x541,x542),f10(x541,x543))+P2(f5(x541,x542),f5(x541,x543))
% 4.56/4.73 [49]P5(x491,x493)+P5(x491,x492)+~P1(x491)+~E(f5(x491,x492),f5(x491,x493))+~E(f7(x491,x492),f7(x491,x493))+E(f3(x491,x492),f3(x491,x493))
% 4.56/4.73 [55]~P1(x551)+P5(x551,x552)+P5(x551,x553)+P6(f3(x551,x552),f3(x551,x553))+~P4(f5(x551,x552),f5(x551,x553))+~P2(f7(x551,x552),f7(x551,x553))
% 4.56/4.73 [56]~P1(x561)+P5(x561,x562)+P5(x561,x563)+P6(f3(x561,x562),f3(x561,x563))+~P4(f7(x561,x562),f7(x561,x563))+~P2(f5(x561,x562),f5(x561,x563))
% 4.56/4.73 %EqnAxiom
% 4.56/4.73 [1]E(x11,x11)
% 4.56/4.73 [2]E(x22,x21)+~E(x21,x22)
% 4.56/4.73 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 4.56/4.73 [4]~E(x41,x42)+E(f2(x41,x43),f2(x42,x43))
% 4.56/4.73 [5]~E(x51,x52)+E(f2(x53,x51),f2(x53,x52))
% 4.56/4.73 [6]~E(x61,x62)+E(f5(x61,x63),f5(x62,x63))
% 4.56/4.73 [7]~E(x71,x72)+E(f5(x73,x71),f5(x73,x72))
% 4.56/4.73 [8]~E(x81,x82)+E(f3(x81,x83),f3(x82,x83))
% 4.56/4.73 [9]~E(x91,x92)+E(f3(x93,x91),f3(x93,x92))
% 4.56/4.73 [10]~E(x101,x102)+E(f6(x101,x103),f6(x102,x103))
% 4.56/4.73 [11]~E(x111,x112)+E(f6(x113,x111),f6(x113,x112))
% 4.56/4.73 [12]~E(x121,x122)+E(f10(x121,x123),f10(x122,x123))
% 4.56/4.73 [13]~E(x131,x132)+E(f10(x133,x131),f10(x133,x132))
% 4.56/4.73 [14]~E(x141,x142)+E(f4(x141,x143),f4(x142,x143))
% 4.56/4.73 [15]~E(x151,x152)+E(f4(x153,x151),f4(x153,x152))
% 4.56/4.73 [16]~E(x161,x162)+E(f7(x161,x163),f7(x162,x163))
% 4.56/4.73 [17]~E(x171,x172)+E(f7(x173,x171),f7(x173,x172))
% 4.56/4.73 [18]~P1(x181)+P1(x182)+~E(x181,x182)
% 4.56/4.73 [19]P2(x192,x193)+~E(x191,x192)+~P2(x191,x193)
% 4.56/4.73 [20]P2(x203,x202)+~E(x201,x202)+~P2(x203,x201)
% 4.56/4.73 [21]~P3(x211)+P3(x212)+~E(x211,x212)
% 4.56/4.73 [22]P6(x222,x223)+~E(x221,x222)+~P6(x221,x223)
% 4.56/4.73 [23]P6(x233,x232)+~E(x231,x232)+~P6(x233,x231)
% 4.56/4.73 [24]P7(x242,x243)+~E(x241,x242)+~P7(x241,x243)
% 4.56/4.73 [25]P7(x253,x252)+~E(x251,x252)+~P7(x253,x251)
% 4.56/4.73 [26]P4(x262,x263)+~E(x261,x262)+~P4(x261,x263)
% 4.56/4.73 [27]P4(x273,x272)+~E(x271,x272)+~P4(x273,x271)
% 4.56/4.73 [28]P5(x282,x283)+~E(x281,x282)+~P5(x281,x283)
% 4.56/4.73 [29]P5(x293,x292)+~E(x291,x292)+~P5(x293,x291)
% 4.56/4.73
% 4.56/4.73 %-------------------------------------------
% 4.56/4.73 cnf(57,plain,
% 4.56/4.73 (P7(x571,x571)),
% 4.56/4.73 inference(equality_inference,[],[34])).
% 4.56/4.73 cnf(58,plain,
% 4.56/4.73 (P4(x581,x581)),
% 4.56/4.73 inference(equality_inference,[],[35])).
% 4.56/4.73 cnf(64,plain,
% 4.56/4.73 (~P5(a1,x641)),
% 4.56/4.74 inference(scs_inference,[],[30,32,31,33,40,45,37])).
% 4.56/4.74 cnf(107,plain,
% 4.56/4.74 (P7(x1071,x1072)+~E(x1072,x1071)),
% 4.56/4.74 inference(scs_inference,[],[57,24])).
% 4.56/4.74 cnf(131,plain,
% 4.56/4.74 (~P5(a1,x1311)),
% 4.56/4.74 inference(rename_variables,[],[64])).
% 4.56/4.74 cnf(133,plain,
% 4.56/4.74 (P5(a1,a9)+~P4(f7(a1,a8),f7(a1,a9))+~P2(f5(a1,a8),f5(a1,a9))),
% 4.56/4.74 inference(scs_inference,[],[30,33,64,131,56])).
% 4.56/4.74 cnf(137,plain,
% 4.56/4.74 (P4(x1371,x1371)),
% 4.56/4.74 inference(rename_variables,[],[58])).
% 4.56/4.74 cnf(138,plain,
% 4.56/4.74 (~E(f7(a1,a8),f7(a1,a9))+~P2(f5(a1,a8),f5(a1,a9))),
% 4.56/4.74 inference(scs_inference,[],[64,58,137,133,26,27])).
% 4.56/4.74 cnf(147,plain,
% 4.56/4.74 (~P2(f5(a1,a8),f5(a1,a9))+~P2(f4(a1,a8),f4(a1,a9))),
% 4.56/4.74 inference(scs_inference,[],[30,64,58,137,133,26,27,41,17,42,47,50])).
% 4.56/4.74 cnf(216,plain,
% 4.56/4.74 (~E(a1,x2161)+E(f6(x2161,x2162),f6(x2161,x2163))),
% 4.56/4.74 inference(scs_inference,[],[30,38,18])).
% 4.56/4.74 cnf(217,plain,
% 4.56/4.74 (E(f6(a1,x2171),f6(a1,x2172))),
% 4.56/4.74 inference(equality_inference,[],[216])).
% 4.56/4.74 cnf(218,plain,
% 4.56/4.74 (P7(f6(a1,x2181),f6(a1,x2182))),
% 4.56/4.74 inference(scs_inference,[],[217,107])).
% 4.56/4.74 cnf(3592,plain,
% 4.56/4.74 (P2(f10(a1,a8),f10(a1,a9))),
% 4.56/4.74 inference(scs_inference,[],[31,30,51,18])).
% 4.56/4.74 cnf(3595,plain,
% 4.56/4.74 (P2(f5(a1,a8),f5(a1,a9))),
% 4.56/4.74 inference(scs_inference,[],[30,3592,218,45,54])).
% 4.56/4.74 cnf(3607,plain,
% 4.56/4.74 (~E(f7(a1,a8),f7(a1,a9))),
% 4.56/4.74 inference(scs_inference,[],[3595,138])).
% 4.56/4.74 cnf(3612,plain,
% 4.56/4.74 (~P2(f4(a1,a8),f4(a1,a9))),
% 4.56/4.74 inference(scs_inference,[],[3595,147])).
% 4.56/4.74 cnf(3627,plain,
% 4.56/4.74 ($false),
% 4.56/4.74 inference(scs_inference,[],[31,30,3612,3607,42,47,52]),
% 4.56/4.74 ['proof']).
% 4.56/4.74 % SZS output end Proof
% 4.56/4.74 % Total time :4.241420s
%------------------------------------------------------------------------------