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