%------------------------------------------------------------------------------
% 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 : n002.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 : Theorem 0.86s 1.13s
% 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.08/0.34 % Computer : n002.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:08:22 UTC 2026
% 0.08/0.34 % CPUTime :
% 0.14/0.47 start to proof:theBenchmark
% 0.86/1.11 %-------------------------------------------
% 0.86/1.11 % File :CSE---1.7
% 0.86/1.12 % Problem :theBenchmark
% 0.86/1.12 % Transform :cnf
% 0.86/1.12 % Format :tptp:raw
% 0.86/1.12 % Command :java -jar mcs_scs.jar %d %s
% 0.86/1.12
% 0.86/1.12 % Result :Theorem 0.637572s
% 0.86/1.12 % Output :CNFRefutation 0.637572s
% 0.86/1.12 %-------------------------------------------
% 0.86/1.12 %--------------------------------------------------------------------------
% 0.86/1.12 % File : MGT043+1 : TPTP v9.3.0. Released v2.4.0.
% 0.86/1.12 % Domain : Management (Organisation Theory)
% 0.86/1.12 % Problem : Conditions for a higher hazard of mortality
% 0.86/1.12 % Version : [Han98] axioms.
% 0.86/1.12 % English : When an organization lacks immunity, the growth of internal
% 0.86/1.12 % friction elevates its hazard of mortality when its knowledge and
% 0.86/1.12 % the quality of its ties are constant.
% 0.86/1.12
% 0.86/1.12 % Refs : [Kam00] Kamps (2000), Email to G. Sutcliffe
% 0.86/1.12 % : [CH00] Carroll & Hannan (2000), The Demography of Corporation
% 0.86/1.12 % : [Han98] Hannan (1998), Rethinking Age Dependence in Organizati
% 0.86/1.12 % Source : [Kam00]
% 0.86/1.12 % Names : LEMMA 2 [Han98]
% 0.86/1.12
% 0.86/1.12 % Status : Theorem
% 0.86/1.12 % Rating : 0.13 v9.3.0, 0.12 v9.1.0, 0.09 v9.0.0, 0.11 v8.2.0, 0.08 v8.1.0, 0.06 v7.4.0, 0.10 v7.3.0, 0.07 v7.2.0, 0.03 v7.1.0, 0.04 v7.0.0, 0.03 v6.4.0, 0.08 v6.3.0, 0.12 v6.2.0, 0.20 v6.1.0, 0.23 v6.0.0, 0.13 v5.5.0, 0.19 v5.4.0, 0.21 v5.3.0, 0.30 v5.2.0, 0.20 v5.1.0, 0.24 v5.0.0, 0.17 v4.1.0, 0.13 v4.0.0, 0.12 v3.7.0, 0.15 v3.5.0, 0.16 v3.3.0, 0.21 v3.2.0, 0.27 v3.1.0, 0.44 v2.7.0, 0.50 v2.6.0, 0.33 v2.4.0
% 0.86/1.12 % Syntax : Number of formulae : 10 ( 0 unt; 0 def)
% 0.86/1.12 % Number of atoms : 50 ( 13 equ)
% 0.86/1.12 % Maximal formula atoms : 12 ( 5 avg)
% 0.86/1.12 % Number of connectives : 45 ( 5 ~; 4 |; 20 &)
% 0.86/1.12 % ( 3 <=>; 13 =>; 0 <=; 0 <~>)
% 0.86/1.12 % Maximal formula depth : 10 ( 7 avg)
% 0.86/1.12 % Maximal term depth : 2 ( 1 avg)
% 0.86/1.12 % Number of predicates : 7 ( 6 usr; 0 prp; 1-2 aty)
% 0.86/1.12 % Number of functors : 6 ( 6 usr; 0 con; 2-2 aty)
% 0.86/1.12 % Number of variables : 25 ( 25 !; 0 ?)
% 0.86/1.12 % SPC : FOF_THM_RFO_SEQ
% 0.86/1.12
% 0.86/1.12 % Comments : See MGT042+1.p for the mnemonic names.
% 0.86/1.12 %--------------------------------------------------------------------------
% 0.86/1.12 include('Axioms/MGT001+0.ax').
% 0.86/1.12 %--------------------------------------------------------------------------
% 0.86/1.12 %----Problem Axioms
% 0.86/1.12 %----When an organization lacks immunity, superior capability and
% 0.86/1.12 %----position imply a lower hazard of mortality.
% 0.86/1.12 fof(assumption_4,axiom,
% 0.86/1.12 ! [X,T0,T] :
% 0.86/1.12 ( ( organization(X)
% 0.86/1.12 & ~ has_immunity(X,T0)
% 0.86/1.12 & ~ has_immunity(X,T) )
% 0.86/1.12 => ( ( ( greater(capability(X,T),capability(X,T0))
% 0.86/1.12 & greater_or_equal(position(X,T),position(X,T0)) )
% 0.86/1.12 => smaller(hazard_of_mortality(X,T),hazard_of_mortality(X,T0)) )
% 0.86/1.12 & ( ( greater_or_equal(capability(X,T),capability(X,T0))
% 0.86/1.12 & greater(position(X,T),position(X,T0)) )
% 0.86/1.12 => smaller(hazard_of_mortality(X,T),hazard_of_mortality(X,T0)) )
% 0.86/1.12 & ( ( capability(X,T) = capability(X,T0)
% 0.86/1.12 & position(X,T) = position(X,T0) )
% 0.86/1.12 => hazard_of_mortality(X,T) = hazard_of_mortality(X,T0) ) ) ) ).
% 0.86/1.12
% 0.86/1.12 %----Increased knowledge elevates an organization's capability; and
% 0.86/1.12 %----increased accumulation of organizational internal frictions
% 0.86/1.12 %----diminishes its capability.
% 0.86/1.12 fof(assumption_5,axiom,
% 0.86/1.12 ! [X,T0,T] :
% 0.86/1.12 ( organization(X)
% 0.86/1.12 => ( ( ( greater(stock_of_knowledge(X,T),stock_of_knowledge(X,T0))
% 0.86/1.12 & smaller_or_equal(internal_friction(X,T),internal_friction(X,T0)) )
% 0.86/1.12 => greater(capability(X,T),capability(X,T0)) )
% 0.86/1.12 & ( ( smaller_or_equal(stock_of_knowledge(X,T),stock_of_knowledge(X,T0))
% 0.86/1.12 & greater(internal_friction(X,T),internal_friction(X,T0)) )
% 0.86/1.12 => smaller(capability(X,T),capability(X,T0)) )
% 0.86/1.12 & ( ( stock_of_knowledge(X,T) = stock_of_knowledge(X,T0)
% 0.86/1.12 & internal_friction(X,T) = internal_friction(X,T0) )
% 0.86/1.12 => capability(X,T) = capability(X,T0) ) ) ) ).
% 0.86/1.12
% 0.86/1.12 %----Improved ties with external actors enhance an organization's position.
% 0.86/1.12 fof(assumption_6,axiom,
% 0.86/1.12 ! [X,T0,T] :
% 0.86/1.12 ( organization(X)
% 0.86/1.12 => ( ( greater(external_ties(X,T),external_ties(X,T0))
% 0.86/1.12 => greater(position(X,T),position(X,T0)) )
% 0.86/1.12 & ( external_ties(X,T) = external_ties(X,T0)
% 0.86/1.12 => position(X,T) = position(X,T0) ) ) ) ).
% 0.86/1.12
% 0.86/1.12 %----Problem theorems
% 0.86/1.12 %----When an organization lacks immunity, the growth of internal
% 0.86/1.12 %----friction elevates its hazard of mortality when its knowledge and
% 0.86/1.12 %----the quality of its ties are constant.
% 0.86/1.12 %----From A4, A5, and A6 (text says A1-6; also needs D<, D>=, D<=,
% 0.86/1.12 %----MP>str, MP>com, MP>tra).
% 0.86/1.12 fof(lemma_2,conjecture,
% 0.86/1.12 ! [X,T0,T] :
% 0.86/1.12 ( ( organization(X)
% 0.86/1.12 & ~ has_immunity(X,T0)
% 0.86/1.12 & ~ has_immunity(X,T)
% 0.86/1.12 & stock_of_knowledge(X,T) = stock_of_knowledge(X,T0)
% 0.86/1.12 & greater(internal_friction(X,T),internal_friction(X,T0))
% 0.86/1.12 & external_ties(X,T0) = external_ties(X,T) )
% 0.86/1.13 => greater(hazard_of_mortality(X,T),hazard_of_mortality(X,T0)) ) ).
% 0.86/1.13
% 0.86/1.13 %--------------------------------------------------------------------------
% 0.86/1.13 %-------------------------------------------
% 0.86/1.13 % Proof found
% 0.86/1.13 % SZS status Theorem for theBenchmark
% 0.86/1.13 % SZS output start Proof
% 0.86/1.13 %ClaNum:60(EqnAxiom:32)
% 0.86/1.13 %VarNum:172(SingletonVarNum:53)
% 0.86/1.13 %MaxLitNum:4
% 0.86/1.13 %MaxfuncDepth:1
% 0.86/1.13 %SharedTerms:18
% 0.86/1.13 %goalClause: 33 34 35 36 37 38 39
% 0.86/1.13 %singleGoalClaCount:7
% 0.86/1.13 [33]P1(a1)
% 0.86/1.13 [37]~P5(a1,a3)
% 0.86/1.13 [38]~P5(a1,a5)
% 0.86/1.13 [34]E(f4(a1,a3),f4(a1,a5))
% 0.86/1.13 [35]E(f6(a1,a3),f6(a1,a5))
% 0.86/1.13 [36]P2(f7(a1,a5),f7(a1,a3))
% 0.86/1.13 [39]~P2(f8(a1,a5),f8(a1,a3))
% 0.86/1.13 [40]~E(x401,x402)+P7(x401,x402)
% 0.86/1.13 [41]~E(x411,x412)+P6(x411,x412)
% 0.86/1.13 [43]~P8(x431,x432)+P7(x431,x432)
% 0.86/1.13 [44]~P2(x442,x441)+P8(x441,x442)
% 0.86/1.13 [45]~P2(x451,x452)+P6(x451,x452)
% 0.86/1.13 [46]~P8(x462,x461)+P2(x461,x462)
% 0.86/1.13 [49]~P2(x492,x491)+~P2(x491,x492)
% 0.86/1.13 [51]~P1(x511)+P3(x511,x512,x513)
% 0.86/1.13 [42]P8(x421,x422)+P2(x421,x422)+E(x421,x422)
% 0.86/1.13 [47]P8(x471,x472)+~P7(x471,x472)+E(x471,x472)
% 0.86/1.13 [48]P2(x481,x482)+~P6(x481,x482)+E(x481,x482)
% 0.86/1.13 [50]~P2(x501,x503)+P2(x501,x502)+~P2(x503,x502)
% 0.86/1.13 [52]~P1(x521)+~E(f6(x521,x522),f6(x521,x523))+E(f9(x521,x522),f9(x521,x523))
% 0.86/1.13 [54]~P1(x541)+~P2(f6(x541,x542),f6(x541,x543))+P2(f9(x541,x542),f9(x541,x543))
% 0.86/1.13 [53]P4(x531,x533,x532)+~P1(x531)+P5(x531,x532)+P5(x531,x533)
% 0.86/1.13 [55]~P3(x551,x553,x552)+~E(f4(x551,x552),f4(x551,x553))+~E(f7(x551,x552),f7(x551,x553))+E(f2(x551,x552),f2(x551,x553))
% 0.86/1.13 [56]~P4(x561,x563,x562)+~E(f2(x561,x562),f2(x561,x563))+~E(f9(x561,x562),f9(x561,x563))+E(f8(x561,x562),f8(x561,x563))
% 0.86/1.13 [57]~P3(x571,x573,x572)+~P7(f4(x571,x572),f4(x571,x573))+~P2(f7(x571,x572),f7(x571,x573))+P8(f2(x571,x572),f2(x571,x573))
% 0.86/1.13 [58]~P4(x581,x583,x582)+~P6(f2(x581,x582),f2(x581,x583))+~P2(f9(x581,x582),f9(x581,x583))+P8(f8(x581,x582),f8(x581,x583))
% 0.86/1.13 [59]~P4(x591,x593,x592)+~P6(f9(x591,x592),f9(x591,x593))+~P2(f2(x591,x592),f2(x591,x593))+P8(f8(x591,x592),f8(x591,x593))
% 0.99/1.13 [60]~P3(x601,x603,x602)+~P7(f7(x601,x602),f7(x601,x603))+~P2(f4(x601,x602),f4(x601,x603))+P2(f2(x601,x602),f2(x601,x603))
% 0.99/1.13 %EqnAxiom
% 0.99/1.13 [1]E(x11,x11)
% 0.99/1.13 [2]E(x22,x21)+~E(x21,x22)
% 0.99/1.13 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 0.99/1.13 [4]~E(x41,x42)+E(f4(x41,x43),f4(x42,x43))
% 0.99/1.13 [5]~E(x51,x52)+E(f4(x53,x51),f4(x53,x52))
% 0.99/1.13 [6]~E(x61,x62)+E(f7(x61,x63),f7(x62,x63))
% 0.99/1.13 [7]~E(x71,x72)+E(f7(x73,x71),f7(x73,x72))
% 0.99/1.13 [8]~E(x81,x82)+E(f6(x81,x83),f6(x82,x83))
% 0.99/1.13 [9]~E(x91,x92)+E(f6(x93,x91),f6(x93,x92))
% 0.99/1.13 [10]~E(x101,x102)+E(f2(x101,x103),f2(x102,x103))
% 0.99/1.13 [11]~E(x111,x112)+E(f2(x113,x111),f2(x113,x112))
% 0.99/1.13 [12]~E(x121,x122)+E(f9(x121,x123),f9(x122,x123))
% 0.99/1.13 [13]~E(x131,x132)+E(f9(x133,x131),f9(x133,x132))
% 0.99/1.13 [14]~E(x141,x142)+E(f8(x141,x143),f8(x142,x143))
% 0.99/1.13 [15]~E(x151,x152)+E(f8(x153,x151),f8(x153,x152))
% 0.99/1.13 [16]~P1(x161)+P1(x162)+~E(x161,x162)
% 0.99/1.13 [17]P2(x172,x173)+~E(x171,x172)+~P2(x171,x173)
% 0.99/1.13 [18]P2(x183,x182)+~E(x181,x182)+~P2(x183,x181)
% 0.99/1.13 [19]P5(x192,x193)+~E(x191,x192)+~P5(x191,x193)
% 0.99/1.13 [20]P5(x203,x202)+~E(x201,x202)+~P5(x203,x201)
% 0.99/1.13 [21]P4(x212,x213,x214)+~E(x211,x212)+~P4(x211,x213,x214)
% 0.99/1.13 [22]P4(x223,x222,x224)+~E(x221,x222)+~P4(x223,x221,x224)
% 0.99/1.13 [23]P4(x233,x234,x232)+~E(x231,x232)+~P4(x233,x234,x231)
% 0.99/1.13 [24]P6(x242,x243)+~E(x241,x242)+~P6(x241,x243)
% 0.99/1.13 [25]P6(x253,x252)+~E(x251,x252)+~P6(x253,x251)
% 0.99/1.13 [26]P7(x262,x263)+~E(x261,x262)+~P7(x261,x263)
% 0.99/1.13 [27]P7(x273,x272)+~E(x271,x272)+~P7(x273,x271)
% 0.99/1.13 [28]P3(x282,x283,x284)+~E(x281,x282)+~P3(x281,x283,x284)
% 0.99/1.13 [29]P3(x293,x292,x294)+~E(x291,x292)+~P3(x293,x291,x294)
% 0.99/1.13 [30]P3(x303,x304,x302)+~E(x301,x302)+~P3(x303,x304,x301)
% 0.99/1.13 [31]P8(x312,x313)+~E(x311,x312)+~P8(x311,x313)
% 0.99/1.13 [32]P8(x323,x322)+~E(x321,x322)+~P8(x323,x321)
% 0.99/1.13
% 0.99/1.13 %-------------------------------------------
% 0.99/1.13 cnf(61,plain,
% 0.99/1.13 (P7(x611,x611)),
% 0.99/1.13 inference(equality_inference,[],[40])).
% 0.99/1.13 cnf(62,plain,
% 0.99/1.13 (P6(x621,x621)),
% 0.99/1.13 inference(equality_inference,[],[41])).
% 0.99/1.13 cnf(67,plain,
% 0.99/1.13 (~P8(f8(a1,a3),f8(a1,a5))),
% 0.99/1.13 inference(scs_inference,[],[33,34,39,51,2,46])).
% 0.99/1.13 cnf(72,plain,
% 0.99/1.13 (P6(x721,x721)),
% 0.99/1.13 inference(rename_variables,[],[62])).
% 0.99/1.13 cnf(76,plain,
% 0.99/1.13 (P7(x761,x761)),
% 0.99/1.13 inference(rename_variables,[],[61])).
% 0.99/1.13 cnf(81,plain,
% 0.99/1.13 (P8(f2(a1,a5),f2(a1,a3))),
% 0.99/1.13 inference(scs_inference,[],[33,37,34,36,39,61,76,62,72,51,2,46,49,24,25,26,27,53,57])).
% 0.99/1.13 cnf(267,plain,
% 0.99/1.13 (E(f9(a1,a5),f9(a1,a3))),
% 0.99/1.13 inference(scs_inference,[],[35,33,2,52])).
% 0.99/1.13 cnf(322,plain,
% 0.99/1.13 (P6(x3221,x3221)),
% 0.99/1.13 inference(rename_variables,[],[62])).
% 0.99/1.13 cnf(326,plain,
% 0.99/1.13 (P7(x3261,x3261)),
% 0.99/1.13 inference(rename_variables,[],[61])).
% 0.99/1.13 cnf(329,plain,
% 0.99/1.13 (~P4(a1,a5,a3)+~P2(f2(a1,a3),f2(a1,a5))),
% 0.99/1.13 inference(scs_inference,[],[267,62,322,61,326,67,24,25,27,26,59])).
% 0.99/1.13 cnf(338,plain,
% 0.99/1.13 (~P4(a1,a5,a3)),
% 0.99/1.13 inference(scs_inference,[],[81,329,46])).
% 0.99/1.13 cnf(381,plain,
% 0.99/1.13 ($false),
% 0.99/1.13 inference(scs_inference,[],[33,38,37,338,53]),
% 0.99/1.13 ['proof']).
% 0.99/1.13 % SZS output end Proof
% 0.99/1.13 % Total time :0.637572s
%------------------------------------------------------------------------------