%------------------------------------------------------------------------------
% 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 : n007.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 1.98s 2.20s
% 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.08/0.35 % Computer : n007.cluster.edu
% 0.08/0.35 % Model : x86_64 x86_64
% 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35 % Memory : 8046.5625MB
% 0.08/0.35 % OS : Linux 6.8.0-71-generic
% 0.08/0.35 % CPULimit : 300
% 0.08/0.35 % WCLimit : 300
% 0.08/0.35 % DateTime : Mon Sep 7 13:08:11 UTC 2026
% 0.08/0.35 % CPUTime :
% 0.24/0.51 start to proof:theBenchmark
% 1.98/2.18 %-------------------------------------------
% 1.98/2.18 % File :CSE---1.7
% 1.98/2.18 % Problem :theBenchmark
% 1.98/2.18 % Transform :cnf
% 1.98/2.18 % Format :tptp:raw
% 1.98/2.18 % Command :java -jar mcs_scs.jar %d %s
% 1.98/2.18
% 1.98/2.18 % Result :Theorem 1.685869s
% 1.98/2.19 % Output :CNFRefutation 1.685869s
% 1.98/2.19 %-------------------------------------------
% 1.98/2.19 %--------------------------------------------------------------------------
% 1.98/2.19 % File : MGT046+1 : TPTP v9.3.0. Released v2.4.0.
% 1.98/2.19 % Domain : Management (Organisation Theory)
% 1.98/2.19 % Problem : Unendowed organization's hazard of mortality declines with age
% 1.98/2.19 % Version : [Han98] axioms.
% 1.98/2.19 % English : An unendowed organization's hazard of mortality declines
% 1.98/2.19 % monotonically with its age.
% 1.98/2.19
% 1.98/2.19 % Refs : [Kam00] Kamps (2000), Email to G. Sutcliffe
% 1.98/2.19 % : [CH00] Carroll & Hannan (2000), The Demography of Corporation
% 1.98/2.19 % : [Han98] Hannan (1998), Rethinking Age Dependence in Organizati
% 1.98/2.19 % Source : [Kam00]
% 1.98/2.19 % Names : THEOREM 1 [Han98]
% 1.98/2.19
% 1.98/2.19 % Status : Theorem
% 1.98/2.19 % Rating : 0.13 v9.3.0, 0.15 v9.1.0, 0.12 v9.0.0, 0.14 v8.2.0, 0.08 v7.5.0, 0.09 v7.4.0, 0.10 v7.3.0, 0.07 v7.2.0, 0.03 v7.1.0, 0.00 v7.0.0, 0.07 v6.4.0, 0.08 v6.2.0, 0.12 v6.1.0, 0.17 v6.0.0, 0.13 v5.5.0, 0.11 v5.4.0, 0.14 v5.3.0, 0.22 v5.2.0, 0.10 v5.0.0, 0.12 v4.1.0, 0.09 v4.0.0, 0.08 v3.7.0, 0.10 v3.5.0, 0.11 v3.4.0, 0.16 v3.3.0, 0.21 v3.2.0, 0.27 v3.1.0, 0.22 v2.7.0, 0.17 v2.4.0
% 1.98/2.19 % Syntax : Number of formulae : 14 ( 0 unt; 0 def)
% 1.98/2.19 % Number of atoms : 58 ( 12 equ)
% 1.98/2.19 % Maximal formula atoms : 12 ( 4 avg)
% 1.98/2.19 % Number of connectives : 50 ( 6 ~; 4 |; 20 &)
% 1.98/2.19 % ( 3 <=>; 17 =>; 0 <=; 0 <~>)
% 1.98/2.19 % Maximal formula depth : 9 ( 6 avg)
% 1.98/2.19 % Maximal term depth : 2 ( 1 avg)
% 1.98/2.19 % Number of predicates : 8 ( 7 usr; 0 prp; 1-2 aty)
% 1.98/2.19 % Number of functors : 7 ( 7 usr; 0 con; 2-2 aty)
% 1.98/2.19 % Number of variables : 36 ( 36 !; 0 ?)
% 1.98/2.19 % SPC : FOF_THM_RFO_SEQ
% 1.98/2.19
% 1.98/2.19 % Comments : See MGT042+1.p for the mnemonic names.
% 1.98/2.19 %--------------------------------------------------------------------------
% 1.98/2.19 include('Axioms/MGT001+0.ax').
% 1.98/2.19 %--------------------------------------------------------------------------
% 1.98/2.19 %----Problem Axioms
% 1.98/2.19 %----An unendowed organization never possesses immunity.
% 1.98/2.19 fof(assumption_1,axiom,
% 1.98/2.19 ! [X,T] :
% 1.98/2.19 ( ( organization(X)
% 1.98/2.19 & ~ has_endowment(X) )
% 1.98/2.19 => ~ has_immunity(X,T) ) ).
% 1.98/2.19
% 1.98/2.19 %----When an organization lacks immunity, superior capability and
% 1.98/2.19 %----position imply a lower hazard of mortality.
% 1.98/2.19 fof(assumption_4,axiom,
% 1.98/2.19 ! [X,T0,T] :
% 1.98/2.19 ( ( organization(X)
% 1.98/2.19 & ~ has_immunity(X,T0)
% 1.98/2.19 & ~ has_immunity(X,T) )
% 1.98/2.19 => ( ( ( greater(capability(X,T),capability(X,T0))
% 1.98/2.19 & greater_or_equal(position(X,T),position(X,T0)) )
% 1.98/2.19 => smaller(hazard_of_mortality(X,T),hazard_of_mortality(X,T0)) )
% 1.98/2.19 & ( ( greater_or_equal(capability(X,T),capability(X,T0))
% 1.98/2.19 & greater(position(X,T),position(X,T0)) )
% 1.98/2.19 => smaller(hazard_of_mortality(X,T),hazard_of_mortality(X,T0)) )
% 1.98/2.19 & ( ( capability(X,T) = capability(X,T0)
% 1.98/2.19 & position(X,T) = position(X,T0) )
% 1.98/2.19 => hazard_of_mortality(X,T) = hazard_of_mortality(X,T0) ) ) ) ).
% 1.98/2.19
% 1.98/2.19 %----Increased knowledge elevates an organization's capability; and
% 1.98/2.19 %----increased accumulation of organizational internal frictions
% 1.98/2.19 %----diminishes its capability.
% 1.98/2.19 fof(assumption_5,axiom,
% 1.98/2.19 ! [X,T0,T] :
% 1.98/2.19 ( organization(X)
% 1.98/2.19 => ( ( ( greater(stock_of_knowledge(X,T),stock_of_knowledge(X,T0))
% 1.98/2.19 & smaller_or_equal(internal_friction(X,T),internal_friction(X,T0)) )
% 1.98/2.19 => greater(capability(X,T),capability(X,T0)) )
% 1.98/2.19 & ( ( smaller_or_equal(stock_of_knowledge(X,T),stock_of_knowledge(X,T0))
% 1.98/2.19 & greater(internal_friction(X,T),internal_friction(X,T0)) )
% 1.98/2.19 => smaller(capability(X,T),capability(X,T0)) )
% 1.98/2.19 & ( ( stock_of_knowledge(X,T) = stock_of_knowledge(X,T0)
% 1.98/2.19 & internal_friction(X,T) = internal_friction(X,T0) )
% 1.98/2.19 => capability(X,T) = capability(X,T0) ) ) ) ).
% 1.98/2.19
% 1.98/2.19 %----Improved ties with external actors enhance an organization's position.
% 1.98/2.19 fof(assumption_6,axiom,
% 1.98/2.19 ! [X,T0,T] :
% 1.98/2.19 ( organization(X)
% 1.98/2.19 => ( ( greater(external_ties(X,T),external_ties(X,T0))
% 1.98/2.19 => greater(position(X,T),position(X,T0)) )
% 1.98/2.19 & ( external_ties(X,T) = external_ties(X,T0)
% 1.98/2.19 => position(X,T) = position(X,T0) ) ) ) ).
% 1.98/2.19
% 1.98/2.19 %----Case: liability of Newness (Ass. 7-9).
% 1.98/2.19 %----
% 1.98/2.19 %----An organization's stock of knowledge increases monotonically with
% 1.98/2.19 %----its age.
% 1.98/2.19 fof(assumption_7,axiom,
% 1.98/2.19 ! [X,T0,T] :
% 1.98/2.19 ( ( organization(X)
% 1.98/2.19 & greater(age(X,T),age(X,T0)) )
% 1.98/2.19 => greater(stock_of_knowledge(X,T),stock_of_knowledge(X,T0)) ) ).
% 1.98/2.19
% 1.98/2.19 %----The quality of an organization's external ties increases
% 1.98/2.19 %----monotonically with its age.
% 1.98/2.19 fof(assumption_8,axiom,
% 1.98/2.19 ! [X,T0,T] :
% 1.98/2.19 ( ( organization(X)
% 1.98/2.19 & greater(age(X,T),age(X,T0)) )
% 1.98/2.19 => greater(external_ties(X,T),external_ties(X,T0)) ) ).
% 1.98/2.19
% 1.98/2.19 %----The quality of an organization's internal friction does not vary
% 1.98/2.19 %----with its age.
% 1.98/2.19 fof(assumption_9,axiom,
% 1.98/2.19 ! [X,T0,T] :
% 1.98/2.19 ( organization(X)
% 1.98/2.19 => internal_friction(X,T) = internal_friction(X,T0) ) ).
% 1.98/2.19
% 1.98/2.19 %----Problem theorems
% 1.98/2.19 %----The liability-of-newness theorem (Stinchcombe 1965): an unendowed
% 1.98/2.19 %----organization's hazard of mortality declines monotonically with
% 1.98/2.20 %----its age.
% 1.98/2.20 %----From A1 and A4-9 (text says D1, A1-4, L1-2; also needs D<=, D>=).
% 1.98/2.20 fof(theorem_1,conjecture,
% 1.98/2.20 ! [X,T0,T] :
% 1.98/2.20 ( ( organization(X)
% 1.98/2.20 & ~ has_endowment(X)
% 1.98/2.20 & greater(age(X,T),age(X,T0)) )
% 1.98/2.20 => smaller(hazard_of_mortality(X,T),hazard_of_mortality(X,T0)) ) ).
% 1.98/2.20
% 1.98/2.20 %--------------------------------------------------------------------------
% 1.98/2.20 %-------------------------------------------
% 1.98/2.20 % Proof found
% 1.98/2.20 % SZS status Theorem for theBenchmark
% 1.98/2.20 % SZS output start Proof
% 1.98/2.20 %ClaNum:64(EqnAxiom:35)
% 1.98/2.20 %VarNum:199(SingletonVarNum:64)
% 1.98/2.20 %MaxLitNum:4
% 1.98/2.20 %MaxfuncDepth:1
% 1.98/2.20 %SharedTerms:11
% 1.98/2.20 %goalClause: 36 37 38 39
% 1.98/2.20 %singleGoalClaCount:4
% 1.98/2.20 [36]P1(a1)
% 1.98/2.20 [38]~P5(a1)
% 1.98/2.20 [37]P2(f2(a1,a4),f2(a1,a5))
% 1.98/2.20 [39]~P8(f6(a1,a4),f6(a1,a5))
% 1.98/2.20 [40]~E(x401,x402)+P9(x401,x402)
% 1.98/2.20 [41]~E(x411,x412)+P6(x411,x412)
% 1.98/2.20 [45]~P8(x451,x452)+P9(x451,x452)
% 1.98/2.20 [46]~P2(x462,x461)+P8(x461,x462)
% 1.98/2.20 [47]~P2(x471,x472)+P6(x471,x472)
% 1.98/2.20 [48]~P8(x482,x481)+P2(x481,x482)
% 1.98/2.20 [51]~P2(x512,x511)+~P2(x511,x512)
% 1.98/2.20 [53]~P1(x531)+P3(x531,x532,x533)
% 1.98/2.20 [44]~P1(x441)+E(f8(x441,x442),f8(x441,x443))
% 0.35/2.20 [42]P8(x421,x422)+P2(x421,x422)+E(x421,x422)
% 0.35/2.20 [43]~P1(x431)+P5(x431)+~P7(x431,x432)
% 0.35/2.20 [49]P8(x491,x492)+~P9(x491,x492)+E(x491,x492)
% 0.35/2.20 [50]P2(x501,x502)+~P6(x501,x502)+E(x501,x502)
% 0.35/2.20 [52]~P2(x521,x523)+P2(x521,x522)+~P2(x523,x522)
% 0.35/2.20 [54]~P1(x541)+~E(f7(x541,x542),f7(x541,x543))+E(f9(x541,x542),f9(x541,x543))
% 0.35/2.20 [56]~P1(x561)+~P2(f7(x561,x562),f7(x561,x563))+P2(f9(x561,x562),f9(x561,x563))
% 0.35/2.20 [57]~P1(x571)+~P2(f2(x571,x572),f2(x571,x573))+P2(f10(x571,x572),f10(x571,x573))
% 0.35/2.20 [58]~P1(x581)+~P2(f2(x581,x582),f2(x581,x583))+P2(f7(x581,x582),f7(x581,x583))
% 0.35/2.20 [55]P4(x551,x552,x553)+~P1(x551)+P7(x551,x552)+P7(x551,x553)
% 0.35/2.20 [59]~P3(x591,x592,x593)+~E(f10(x591,x592),f10(x591,x593))+~E(f8(x591,x592),f8(x591,x593))+E(f3(x591,x592),f3(x591,x593))
% 0.35/2.20 [60]~P4(x601,x602,x603)+~E(f3(x601,x602),f3(x601,x603))+~E(f9(x601,x602),f9(x601,x603))+E(f6(x601,x602),f6(x601,x603))
% 0.35/2.20 [61]~P3(x611,x612,x613)+~P9(f10(x611,x612),f10(x611,x613))+~P2(f8(x611,x612),f8(x611,x613))+P8(f3(x611,x612),f3(x611,x613))
% 0.35/2.20 [62]~P4(x621,x622,x623)+~P6(f3(x621,x622),f3(x621,x623))+~P2(f9(x621,x622),f9(x621,x623))+P8(f6(x621,x622),f6(x621,x623))
% 0.35/2.20 [63]~P4(x631,x632,x633)+~P6(f9(x631,x632),f9(x631,x633))+~P2(f3(x631,x632),f3(x631,x633))+P8(f6(x631,x632),f6(x631,x633))
% 0.35/2.20 [64]~P3(x641,x642,x643)+~P9(f8(x641,x642),f8(x641,x643))+~P2(f10(x641,x642),f10(x641,x643))+P2(f3(x641,x642),f3(x641,x643))
% 0.35/2.20 %EqnAxiom
% 0.35/2.20 [1]E(x11,x11)
% 0.35/2.20 [2]E(x22,x21)+~E(x21,x22)
% 0.35/2.20 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 0.35/2.20 [4]~E(x41,x42)+E(f2(x41,x43),f2(x42,x43))
% 0.35/2.20 [5]~E(x51,x52)+E(f2(x53,x51),f2(x53,x52))
% 0.35/2.20 [6]~E(x61,x62)+E(f10(x61,x63),f10(x62,x63))
% 0.35/2.20 [7]~E(x71,x72)+E(f10(x73,x71),f10(x73,x72))
% 0.35/2.20 [8]~E(x81,x82)+E(f6(x81,x83),f6(x82,x83))
% 0.35/2.20 [9]~E(x91,x92)+E(f6(x93,x91),f6(x93,x92))
% 0.35/2.20 [10]~E(x101,x102)+E(f9(x101,x103),f9(x102,x103))
% 0.35/2.20 [11]~E(x111,x112)+E(f9(x113,x111),f9(x113,x112))
% 0.35/2.20 [12]~E(x121,x122)+E(f8(x121,x123),f8(x122,x123))
% 0.35/2.20 [13]~E(x131,x132)+E(f8(x133,x131),f8(x133,x132))
% 0.35/2.20 [14]~E(x141,x142)+E(f3(x141,x143),f3(x142,x143))
% 0.35/2.20 [15]~E(x151,x152)+E(f3(x153,x151),f3(x153,x152))
% 0.35/2.20 [16]~E(x161,x162)+E(f7(x161,x163),f7(x162,x163))
% 0.35/2.20 [17]~E(x171,x172)+E(f7(x173,x171),f7(x173,x172))
% 0.35/2.20 [18]~P1(x181)+P1(x182)+~E(x181,x182)
% 0.35/2.20 [19]P2(x192,x193)+~E(x191,x192)+~P2(x191,x193)
% 0.35/2.20 [20]P2(x203,x202)+~E(x201,x202)+~P2(x203,x201)
% 0.35/2.20 [21]~P5(x211)+P5(x212)+~E(x211,x212)
% 0.35/2.20 [22]P8(x222,x223)+~E(x221,x222)+~P8(x221,x223)
% 0.35/2.20 [23]P8(x233,x232)+~E(x231,x232)+~P8(x233,x231)
% 0.35/2.20 [24]P9(x242,x243)+~E(x241,x242)+~P9(x241,x243)
% 0.35/2.20 [25]P9(x253,x252)+~E(x251,x252)+~P9(x253,x251)
% 0.35/2.20 [26]P6(x262,x263)+~E(x261,x262)+~P6(x261,x263)
% 0.35/2.20 [27]P6(x273,x272)+~E(x271,x272)+~P6(x273,x271)
% 0.35/2.20 [28]P7(x282,x283)+~E(x281,x282)+~P7(x281,x283)
% 0.35/2.20 [29]P7(x293,x292)+~E(x291,x292)+~P7(x293,x291)
% 0.35/2.20 [30]P4(x302,x303,x304)+~E(x301,x302)+~P4(x301,x303,x304)
% 0.35/2.20 [31]P4(x313,x312,x314)+~E(x311,x312)+~P4(x313,x311,x314)
% 0.35/2.20 [32]P4(x323,x324,x322)+~E(x321,x322)+~P4(x323,x324,x321)
% 0.35/2.20 [33]P3(x332,x333,x334)+~E(x331,x332)+~P3(x331,x333,x334)
% 0.35/2.20 [34]P3(x343,x342,x344)+~E(x341,x342)+~P3(x343,x341,x344)
% 0.35/2.20 [35]P3(x353,x354,x352)+~E(x351,x352)+~P3(x353,x354,x351)
% 0.35/2.20
% 0.35/2.20 %-------------------------------------------
% 0.35/2.20 cnf(65,plain,
% 0.35/2.20 (P9(x651,x651)),
% 0.35/2.20 inference(equality_inference,[],[40])).
% 0.35/2.20 cnf(66,plain,
% 0.35/2.20 (P6(x661,x661)),
% 0.35/2.20 inference(equality_inference,[],[41])).
% 0.35/2.20 cnf(68,plain,
% 0.35/2.20 (P3(a1,x681,x682)),
% 0.35/2.20 inference(scs_inference,[],[36,53])).
% 0.35/2.20 cnf(74,plain,
% 0.35/2.20 (~P7(a1,x741)),
% 0.35/2.20 inference(scs_inference,[],[36,38,37,39,53,46,51,43])).
% 0.35/2.20 cnf(76,plain,
% 0.35/2.20 (P4(a1,x761,x761)),
% 0.35/2.20 inference(scs_inference,[],[36,38,37,39,53,46,51,43,55])).
% 0.35/2.20 cnf(109,plain,
% 0.35/2.20 (P6(x1091,x1092)+~E(x1092,x1091)),
% 0.35/2.20 inference(scs_inference,[],[66,26])).
% 0.35/2.20 cnf(113,plain,
% 0.35/2.20 (P9(x1131,x1132)+~E(x1132,x1131)),
% 0.35/2.20 inference(scs_inference,[],[37,76,66,65,26,31,52,24])).
% 0.35/2.20 cnf(137,plain,
% 0.35/2.20 (~E(a1,x1371)+E(f8(x1371,x1372),f8(x1371,x1373))),
% 0.35/2.20 inference(scs_inference,[],[36,44,18])).
% 0.35/2.20 cnf(138,plain,
% 0.35/2.20 (E(f8(a1,x1381),f8(a1,x1382))),
% 0.35/2.20 inference(equality_inference,[],[137])).
% 0.35/2.20 cnf(140,plain,
% 0.35/2.20 (P9(f8(a1,x1401),f8(a1,x1402))),
% 0.35/2.20 inference(scs_inference,[],[138,109,113])).
% 0.35/2.20 cnf(141,plain,
% 0.35/2.20 (P4(a1,f8(a1,x1411),f8(a1,x1412))),
% 0.35/2.20 inference(scs_inference,[],[76,138,109,113,32])).
% 0.35/2.20 cnf(165,plain,
% 0.35/2.20 (~P2(f10(a1,x1651),f10(a1,x1652))+P2(f3(a1,x1651),f3(a1,x1652))),
% 0.35/2.20 inference(scs_inference,[],[68,140,141,30,64])).
% 0.35/2.20 cnf(256,plain,
% 0.35/2.20 (P2(f7(a1,a4),f7(a1,a5))),
% 0.35/2.20 inference(scs_inference,[],[37,36,58,18])).
% 0.35/2.20 cnf(481,plain,
% 0.35/2.20 (P6(f9(a1,a4),f9(a1,a5))),
% 0.35/2.20 inference(scs_inference,[],[256,36,47,56])).
% 0.35/2.20 cnf(532,plain,
% 0.35/2.20 (~P4(a1,a4,a5)+~P2(f3(a1,a4),f3(a1,a5))),
% 0.35/2.20 inference(scs_inference,[],[39,481,63])).
% 0.35/2.20 cnf(548,plain,
% 0.35/2.20 (P7(a1,a5)+~P2(f3(a1,a4),f3(a1,a5))),
% 0.35/2.20 inference(scs_inference,[],[36,74,532,55])).
% 0.35/2.20 cnf(555,plain,
% 0.35/2.20 ($false),
% 0.35/2.20 inference(scs_inference,[],[37,36,74,548,165,48,57]),
% 0.35/2.20 ['proof']).
% 0.35/2.20 % SZS output end Proof
% 0.35/2.20 % Total time :1.685869s
%------------------------------------------------------------------------------