%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : MGT043-1 : TPTP v9.3.0. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% Computer : n031.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 0.58s 0.73s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : MGT043-1 : TPTP v9.3.0. Released v2.4.0.
% 0.00/0.03 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% 0.10/0.35 % Computer : n031.cluster.edu
% 0.10/0.35 % Model : x86_64 x86_64
% 0.10/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.35 % Memory : 8046.5625MB
% 0.10/0.35 % OS : Linux 6.8.0-71-generic
% 0.10/0.35 % CPULimit : 300
% 0.10/0.35 % WCLimit : 300
% 0.10/0.35 % DateTime : Mon Sep 7 13:09:26 UTC 2026
% 0.10/0.35 % CPUTime :
% 0.26/0.56 start to proof:theBenchmark
% 0.58/0.71 %-------------------------------------------
% 0.58/0.72 % File :CSE---1.7
% 0.58/0.72 % Problem :theBenchmark
% 0.58/0.72 % Transform :cnf
% 0.58/0.72 % Format :tptp:raw
% 0.58/0.72 % Command :java -jar mcs_scs.jar %d %s
% 0.58/0.72
% 0.58/0.72 % Result :Theorem 0.181239s
% 0.58/0.72 % Output :CNFRefutation 0.181239s
% 0.58/0.72 %-------------------------------------------
% 0.58/0.72 %--------------------------------------------------------------------------
% 0.58/0.72 % File : MGT043-1 : TPTP v9.3.0. Released v2.4.0.
% 0.58/0.72 % Domain : Management (Organisation Theory)
% 0.58/0.72 % Problem : Conditions for a higher hazard of mortality
% 0.58/0.72 % Version : [Han98] axioms.
% 0.58/0.72 % English : When an organization lacks immunity, the growth of internal
% 0.58/0.72 % friction elevates its hazard of mortality when its knowledge and
% 0.58/0.72 % the quality of its ties are constant.
% 0.58/0.72
% 0.58/0.72 % Refs : [Kam00] Kamps (2000), Email to G. Sutcliffe
% 0.58/0.72 % : [CH00] Carroll & Hannan (2000), The Demography of Corporation
% 0.58/0.72 % : [Han98] Hannan (1998), Rethinking Age Dependence in Organizati
% 0.58/0.72 % Source : [TPTP]
% 0.58/0.72 % Names :
% 0.58/0.72
% 0.58/0.72 % Status : Unsatisfiable
% 0.58/0.72 % Rating : 0.08 v9.3.0, 0.05 v9.0.0, 0.10 v8.1.0, 0.00 v7.5.0, 0.05 v7.4.0, 0.06 v7.3.0, 0.08 v7.1.0, 0.00 v7.0.0, 0.07 v6.4.0, 0.00 v6.1.0, 0.07 v6.0.0, 0.10 v5.5.0, 0.20 v5.4.0, 0.25 v5.3.0, 0.28 v5.2.0, 0.19 v5.1.0, 0.24 v5.0.0, 0.29 v4.1.0, 0.23 v4.0.1, 0.00 v3.4.0, 0.08 v3.3.0, 0.21 v3.2.0, 0.23 v3.1.0, 0.27 v2.7.0, 0.25 v2.6.0, 0.44 v2.4.0
% 0.58/0.72 % Syntax : Number of clauses : 26 ( 7 unt; 6 nHn; 25 RR)
% 0.58/0.72 % Number of literals : 69 ( 15 equ; 37 neg)
% 0.58/0.72 % Maximal clause size : 6 ( 2 avg)
% 0.58/0.72 % Maximal term depth : 2 ( 1 avg)
% 0.58/0.72 % Number of predicates : 7 ( 6 usr; 0 prp; 1-2 aty)
% 0.58/0.72 % Number of functors : 9 ( 9 usr; 3 con; 0-2 aty)
% 0.58/0.72 % Number of variables : 47 ( 0 sgn)
% 0.58/0.72 % SPC : CNF_UNS_RFO_SEQ_NHN
% 0.58/0.72
% 0.58/0.72 % Comments : See MGT042+1.p for the mnemonic names.
% 0.58/0.72 % : Created with tptp2X -f tptp -t clausify:otter MGT043+1.p
% 0.58/0.72 %--------------------------------------------------------------------------
% 0.58/0.72 include('Axioms/MGT001-0.ax').
% 0.58/0.72 %--------------------------------------------------------------------------
% 0.58/0.72 cnf(assumption_4_38,axiom,
% 0.58/0.72 ( ~ organization(A)
% 0.58/0.72 | has_immunity(A,B)
% 0.58/0.72 | has_immunity(A,C)
% 0.58/0.72 | ~ greater(capability(A,C),capability(A,B))
% 0.58/0.72 | ~ greater_or_equal(position(A,C),position(A,B))
% 0.58/0.72 | smaller(hazard_of_mortality(A,C),hazard_of_mortality(A,B)) ) ).
% 0.58/0.72
% 0.58/0.72 cnf(assumption_4_39,axiom,
% 0.58/0.72 ( ~ organization(A)
% 0.58/0.72 | has_immunity(A,B)
% 0.58/0.72 | has_immunity(A,C)
% 0.58/0.72 | ~ greater_or_equal(capability(A,C),capability(A,B))
% 0.58/0.72 | ~ greater(position(A,C),position(A,B))
% 0.58/0.72 | smaller(hazard_of_mortality(A,C),hazard_of_mortality(A,B)) ) ).
% 0.58/0.72
% 0.58/0.72 cnf(assumption_4_40,axiom,
% 0.58/0.72 ( ~ organization(A)
% 0.58/0.72 | has_immunity(A,B)
% 0.58/0.72 | has_immunity(A,C)
% 0.58/0.72 | capability(A,C) != capability(A,B)
% 0.58/0.72 | position(A,C) != position(A,B)
% 0.58/0.72 | hazard_of_mortality(A,C) = hazard_of_mortality(A,B) ) ).
% 0.58/0.72
% 0.58/0.72 cnf(assumption_5_41,axiom,
% 0.58/0.72 ( ~ organization(A)
% 0.58/0.72 | ~ greater(stock_of_knowledge(A,B),stock_of_knowledge(A,C))
% 0.58/0.72 | ~ smaller_or_equal(internal_friction(A,B),internal_friction(A,C))
% 0.58/0.72 | greater(capability(A,B),capability(A,C)) ) ).
% 0.58/0.72
% 0.58/0.72 cnf(assumption_5_42,axiom,
% 0.58/0.72 ( ~ organization(A)
% 0.58/0.72 | ~ smaller_or_equal(stock_of_knowledge(A,B),stock_of_knowledge(A,C))
% 0.58/0.72 | ~ greater(internal_friction(A,B),internal_friction(A,C))
% 0.58/0.72 | smaller(capability(A,B),capability(A,C)) ) ).
% 0.58/0.72
% 0.58/0.72 cnf(assumption_5_43,axiom,
% 0.58/0.72 ( ~ organization(A)
% 0.58/0.72 | stock_of_knowledge(A,B) != stock_of_knowledge(A,C)
% 0.58/0.72 | internal_friction(A,B) != internal_friction(A,C)
% 0.58/0.72 | capability(A,B) = capability(A,C) ) ).
% 0.58/0.72
% 0.58/0.72 cnf(assumption_6_44,axiom,
% 0.58/0.72 ( ~ organization(A)
% 0.58/0.72 | ~ greater(external_ties(A,B),external_ties(A,C))
% 0.58/0.72 | greater(position(A,B),position(A,C)) ) ).
% 0.58/0.72
% 0.58/0.72 cnf(assumption_6_45,axiom,
% 0.58/0.72 ( ~ organization(A)
% 0.58/0.72 | external_ties(A,B) != external_ties(A,C)
% 0.58/0.72 | position(A,B) = position(A,C) ) ).
% 0.58/0.72
% 0.58/0.72 cnf(lemma_2_46,negated_conjecture,
% 0.58/0.72 organization(sk1) ).
% 0.58/0.72
% 0.58/0.72 cnf(lemma_2_47,negated_conjecture,
% 0.58/0.72 ~ has_immunity(sk1,sk2) ).
% 0.58/0.72
% 0.58/0.72 cnf(lemma_2_48,negated_conjecture,
% 0.58/0.72 ~ has_immunity(sk1,sk3) ).
% 0.58/0.72
% 0.58/0.72 cnf(lemma_2_49,negated_conjecture,
% 0.58/0.72 stock_of_knowledge(sk1,sk3) = stock_of_knowledge(sk1,sk2) ).
% 0.58/0.72
% 0.58/0.72 cnf(lemma_2_50,negated_conjecture,
% 0.58/0.72 greater(internal_friction(sk1,sk3),internal_friction(sk1,sk2)) ).
% 0.58/0.73
% 0.58/0.73 cnf(lemma_2_51,negated_conjecture,
% 0.58/0.73 external_ties(sk1,sk2) = external_ties(sk1,sk3) ).
% 0.58/0.73
% 0.58/0.73 cnf(lemma_2_52,negated_conjecture,
% 0.58/0.73 ~ greater(hazard_of_mortality(sk1,sk3),hazard_of_mortality(sk1,sk2)) ).
% 0.58/0.73
% 0.58/0.73 %--------------------------------------------------------------------------
% 0.58/0.73 %-------------------------------------------
% 0.58/0.73 % Proof found
% 0.58/0.73 % SZS status Theorem for theBenchmark
% 0.58/0.73 % SZS output start Proof
% 0.58/0.73 %ClaNum:52(EqnAxiom:26)
% 0.58/0.73 %VarNum:160(SingletonVarNum:47)
% 0.58/0.73 %MaxLitNum:6
% 0.58/0.73 %MaxfuncDepth:1
% 0.58/0.73 %SharedTerms:18
% 0.58/0.73 %goalClause: 27 28 29 30 31 32 33
% 0.58/0.73 %singleGoalClaCount:7
% 0.58/0.73 [27]P1(a1)
% 0.58/0.73 [31]~P3(a1,a7)
% 0.58/0.73 [32]~P3(a1,a9)
% 0.58/0.73 [28]E(f8(a1,a7),f8(a1,a9))
% 0.58/0.73 [29]E(f2(a1,a7),f2(a1,a9))
% 0.58/0.73 [30]P2(f4(a1,a9),f4(a1,a7))
% 0.58/0.73 [33]~P2(f5(a1,a9),f5(a1,a7))
% 0.58/0.73 [34]~E(x341,x342)+P5(x341,x342)
% 0.58/0.73 [35]~E(x351,x352)+P4(x351,x352)
% 0.58/0.73 [37]~P6(x371,x372)+P5(x371,x372)
% 0.58/0.73 [38]~P2(x382,x381)+P6(x381,x382)
% 0.58/0.73 [39]~P2(x391,x392)+P4(x391,x392)
% 0.58/0.73 [40]~P6(x402,x401)+P2(x401,x402)
% 0.58/0.73 [43]~P2(x432,x431)+~P2(x431,x432)
% 0.58/0.73 [36]P6(x361,x362)+P2(x361,x362)+E(x361,x362)
% 0.58/0.73 [41]P6(x411,x412)+~P5(x411,x412)+E(x411,x412)
% 0.58/0.73 [42]P2(x421,x422)+~P4(x421,x422)+E(x421,x422)
% 0.58/0.73 [44]~P2(x441,x443)+P2(x441,x442)+~P2(x443,x442)
% 0.58/0.73 [45]~P1(x451)+~E(f2(x451,x452),f2(x451,x453))+E(f6(x451,x452),f6(x451,x453))
% 0.58/0.73 [48]~P1(x481)+~P2(f2(x481,x482),f2(x481,x483))+P2(f6(x481,x482),f6(x481,x483))
% 0.58/0.73 [46]~P1(x461)+~E(f8(x461,x462),f8(x461,x463))+~E(f4(x461,x462),f4(x461,x463))+E(f3(x461,x462),f3(x461,x463))
% 0.58/0.73 [49]~P1(x491)+~P5(f8(x491,x492),f8(x491,x493))+~P2(f4(x491,x492),f4(x491,x493))+P6(f3(x491,x492),f3(x491,x493))
% 0.58/0.73 [50]~P1(x501)+~P5(f4(x501,x502),f4(x501,x503))+~P2(f8(x501,x502),f8(x501,x503))+P2(f3(x501,x502),f3(x501,x503))
% 0.58/0.73 [47]P3(x471,x473)+P3(x471,x472)+~P1(x471)+~E(f3(x471,x472),f3(x471,x473))+~E(f6(x471,x472),f6(x471,x473))+E(f5(x471,x472),f5(x471,x473))
% 0.58/0.73 [51]~P1(x511)+P3(x511,x512)+P3(x511,x513)+P6(f5(x511,x512),f5(x511,x513))+~P4(f3(x511,x512),f3(x511,x513))+~P2(f6(x511,x512),f6(x511,x513))
% 0.58/0.73 [52]~P1(x521)+P3(x521,x522)+P3(x521,x523)+P6(f5(x521,x522),f5(x521,x523))+~P4(f6(x521,x522),f6(x521,x523))+~P2(f3(x521,x522),f3(x521,x523))
% 0.58/0.73 %EqnAxiom
% 0.58/0.73 [1]E(x11,x11)
% 0.58/0.73 [2]E(x22,x21)+~E(x21,x22)
% 0.58/0.73 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 0.58/0.73 [4]~E(x41,x42)+E(f8(x41,x43),f8(x42,x43))
% 0.58/0.73 [5]~E(x51,x52)+E(f8(x53,x51),f8(x53,x52))
% 0.58/0.73 [6]~E(x61,x62)+E(f3(x61,x63),f3(x62,x63))
% 0.58/0.73 [7]~E(x71,x72)+E(f3(x73,x71),f3(x73,x72))
% 0.58/0.73 [8]~E(x81,x82)+E(f2(x81,x83),f2(x82,x83))
% 0.58/0.73 [9]~E(x91,x92)+E(f2(x93,x91),f2(x93,x92))
% 0.58/0.73 [10]~E(x101,x102)+E(f4(x101,x103),f4(x102,x103))
% 0.58/0.73 [11]~E(x111,x112)+E(f4(x113,x111),f4(x113,x112))
% 0.58/0.73 [12]~E(x121,x122)+E(f6(x121,x123),f6(x122,x123))
% 0.58/0.73 [13]~E(x131,x132)+E(f6(x133,x131),f6(x133,x132))
% 0.58/0.73 [14]~E(x141,x142)+E(f5(x141,x143),f5(x142,x143))
% 0.58/0.73 [15]~E(x151,x152)+E(f5(x153,x151),f5(x153,x152))
% 0.58/0.73 [16]~P1(x161)+P1(x162)+~E(x161,x162)
% 0.58/0.73 [17]P2(x172,x173)+~E(x171,x172)+~P2(x171,x173)
% 0.58/0.73 [18]P2(x183,x182)+~E(x181,x182)+~P2(x183,x181)
% 0.58/0.73 [19]P3(x192,x193)+~E(x191,x192)+~P3(x191,x193)
% 0.58/0.73 [20]P3(x203,x202)+~E(x201,x202)+~P3(x203,x201)
% 0.58/0.73 [21]P4(x212,x213)+~E(x211,x212)+~P4(x211,x213)
% 0.58/0.73 [22]P4(x223,x222)+~E(x221,x222)+~P4(x223,x221)
% 0.58/0.73 [23]P5(x232,x233)+~E(x231,x232)+~P5(x231,x233)
% 0.58/0.73 [24]P5(x243,x242)+~E(x241,x242)+~P5(x243,x241)
% 0.58/0.73 [25]P6(x252,x253)+~E(x251,x252)+~P6(x251,x253)
% 0.58/0.73 [26]P6(x263,x262)+~E(x261,x262)+~P6(x263,x261)
% 0.58/0.73
% 0.58/0.73 %-------------------------------------------
% 0.58/0.73 cnf(53,plain,
% 0.58/0.73 (P5(x531,x531)),
% 0.58/0.73 inference(equality_inference,[],[34])).
% 0.58/0.73 cnf(54,plain,
% 0.58/0.73 (P4(x541,x541)),
% 0.58/0.73 inference(equality_inference,[],[35])).
% 0.58/0.73 cnf(56,plain,
% 0.58/0.73 (~P6(f5(a1,a7),f5(a1,a9))),
% 0.58/0.73 inference(scs_inference,[],[33,40])).
% 0.58/0.73 cnf(60,plain,
% 0.58/0.73 (E(f8(a1,a9),f8(a1,a7))),
% 0.58/0.73 inference(scs_inference,[],[28,30,33,40,43,2])).
% 0.58/0.73 cnf(62,plain,
% 0.58/0.73 (P4(x621,x621)),
% 0.58/0.73 inference(rename_variables,[],[54])).
% 0.58/0.73 cnf(66,plain,
% 0.58/0.73 (P5(x661,x661)),
% 0.58/0.73 inference(rename_variables,[],[53])).
% 0.58/0.73 cnf(69,plain,
% 0.58/0.73 (P6(f3(a1,a9),f3(a1,a7))),
% 0.58/0.73 inference(scs_inference,[],[27,28,30,33,53,66,54,62,40,43,2,21,22,23,24,49])).
% 0.58/0.73 cnf(115,plain,
% 0.58/0.73 (~P4(f6(a1,a7),f6(a1,a9))+~P2(f3(a1,a7),f3(a1,a9))),
% 0.58/0.73 inference(scs_inference,[],[27,31,32,56,60,16,52])).
% 0.58/0.73 cnf(156,plain,
% 0.58/0.73 (~P4(f6(a1,a7),f6(a1,a9))),
% 0.58/0.73 inference(scs_inference,[],[69,115,40])).
% 0.58/0.73 cnf(164,plain,
% 0.58/0.73 ($false),
% 0.58/0.73 inference(scs_inference,[],[29,27,156,35,39,13,40,45]),
% 0.58/0.73 ['proof']).
% 0.58/0.73 % SZS output end Proof
% 0.58/0.73 % Total time :0.181239s
%------------------------------------------------------------------------------