%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : MGT057-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 : n003.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:22 AM UTC 2026
% Result : Unsatisfiable 0.54s 0.73s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : MGT057-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.05/0.32 % Computer : n003.cluster.edu
% 0.05/0.32 % Model : x86_64 x86_64
% 0.05/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.05/0.32 % Memory : 8046.5625MB
% 0.05/0.32 % OS : Linux 6.8.0-71-generic
% 0.05/0.32 % CPULimit : 300
% 0.05/0.32 % WCLimit : 300
% 0.05/0.32 % DateTime : Mon Sep 7 13:32:09 UTC 2026
% 0.05/0.32 % CPUTime :
% 0.24/0.49 start to proof:theBenchmark
% 0.54/0.72 %-------------------------------------------
% 0.54/0.72 % File :CSE---1.7
% 0.54/0.72 % Problem :theBenchmark
% 0.54/0.72 % Transform :cnf
% 0.54/0.72 % Format :tptp:raw
% 0.54/0.72 % Command :java -jar mcs_scs.jar %d %s
% 0.54/0.72
% 0.54/0.72 % Result :Theorem 0.258473s
% 0.54/0.72 % Output :CNFRefutation 0.258473s
% 0.54/0.72 %-------------------------------------------
% 0.54/0.73 %--------------------------------------------------------------------------
% 0.54/0.73 % File : MGT057-1 : TPTP v9.3.0. Released v2.4.0.
% 0.54/0.73 % Domain : Management (Organisation Theory)
% 0.54/0.73 % Problem : Conditions for a constant then increasing hazard of mortality
% 0.54/0.73 % Version : [Han98] axioms.
% 0.54/0.73 % English : In a drifting environment, an endowed organization's hazard of
% 0.54/0.73 % mortality is constant during the period of immunity; beyond the
% 0.54/0.73 % period of immunity, the hazard rises with age.
% 0.54/0.73
% 0.54/0.73 % Refs : [Kam00] Kamps (2000), Email to G. Sutcliffe
% 0.54/0.73 % : [CH00] Carroll & Hannan (2000), The Demography of Corporation
% 0.54/0.73 % : [Han98] Hannan (1998), Rethinking Age Dependence in Organizati
% 0.54/0.73 % Source : [TPTP]
% 0.54/0.73 % Names :
% 0.54/0.73
% 0.54/0.73 % Status : Unsatisfiable
% 0.54/0.73 % 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.00 v5.5.0, 0.10 v5.4.0, 0.15 v5.3.0, 0.11 v5.2.0, 0.06 v5.0.0, 0.00 v4.0.1, 0.09 v4.0.0, 0.00 v3.3.0, 0.07 v3.2.0, 0.08 v3.1.0, 0.09 v2.7.0, 0.08 v2.6.0, 0.00 v2.5.0, 0.11 v2.4.0
% 0.54/0.73 % Syntax : Number of clauses : 27 ( 6 unt; 8 nHn; 25 RR)
% 0.54/0.73 % Number of literals : 66 ( 8 equ; 31 neg)
% 0.54/0.73 % Maximal clause size : 4 ( 2 avg)
% 0.54/0.73 % Maximal term depth : 3 ( 1 avg)
% 0.54/0.73 % Number of predicates : 8 ( 7 usr; 0 prp; 1-2 aty)
% 0.54/0.73 % Number of functors : 9 ( 9 usr; 6 con; 0-2 aty)
% 0.54/0.73 % Number of variables : 38 ( 0 sgn)
% 0.54/0.73 % SPC : CNF_UNS_RFO_SEQ_NHN
% 0.54/0.73
% 0.54/0.73 % Comments : See MGT042+1.p for the mnemonic names.
% 0.54/0.73 % : Created with tptp2X -f tptp -t clausify:otter MGT057+1.p
% 0.54/0.73 %--------------------------------------------------------------------------
% 0.54/0.73 include('Axioms/MGT001-0.ax').
% 0.54/0.73 %--------------------------------------------------------------------------
% 0.54/0.73 cnf(definition_1_31,axiom,
% 0.54/0.73 ( ~ has_endowment(A)
% 0.54/0.73 | organization(A) ) ).
% 0.54/0.73
% 0.54/0.73 cnf(definition_1_32,axiom,
% 0.54/0.73 ( ~ has_endowment(A)
% 0.54/0.73 | ~ smaller_or_equal(age(A,B),eta)
% 0.54/0.73 | has_immunity(A,B) ) ).
% 0.54/0.73
% 0.54/0.73 cnf(definition_1_33,axiom,
% 0.54/0.73 ( ~ has_endowment(A)
% 0.54/0.73 | ~ greater(age(A,B),eta)
% 0.54/0.73 | ~ has_immunity(A,B) ) ).
% 0.54/0.73
% 0.54/0.73 cnf(definition_1_34,axiom,
% 0.54/0.73 ( ~ organization(A)
% 0.54/0.73 | smaller_or_equal(age(A,sk1(A)),eta)
% 0.54/0.73 | greater(age(A,sk1(A)),eta)
% 0.54/0.73 | has_endowment(A) ) ).
% 0.54/0.73
% 0.54/0.73 cnf(definition_1_35,axiom,
% 0.54/0.73 ( ~ organization(A)
% 0.54/0.73 | smaller_or_equal(age(A,sk1(A)),eta)
% 0.54/0.73 | has_immunity(A,sk1(A))
% 0.54/0.73 | has_endowment(A) ) ).
% 0.54/0.73
% 0.54/0.73 cnf(definition_1_36,axiom,
% 0.54/0.73 ( ~ organization(A)
% 0.54/0.73 | ~ has_immunity(A,sk1(A))
% 0.54/0.73 | greater(age(A,sk1(A)),eta)
% 0.54/0.73 | has_endowment(A) ) ).
% 0.54/0.73
% 0.54/0.73 cnf(definition_1_37,axiom,
% 0.54/0.73 ( ~ organization(A)
% 0.54/0.73 | ~ has_immunity(A,sk1(A))
% 0.54/0.73 | has_immunity(A,sk1(A))
% 0.54/0.73 | has_endowment(A) ) ).
% 0.54/0.73
% 0.54/0.73 cnf(assumption_2_38,axiom,
% 0.54/0.73 ( ~ organization(A)
% 0.54/0.73 | ~ has_immunity(A,B)
% 0.54/0.73 | ~ has_immunity(A,C)
% 0.54/0.73 | hazard_of_mortality(A,B) = hazard_of_mortality(A,C) ) ).
% 0.54/0.73
% 0.54/0.73 cnf(assumption_3_39,axiom,
% 0.54/0.73 ( ~ organization(A)
% 0.54/0.73 | ~ has_immunity(A,B)
% 0.54/0.73 | has_immunity(A,C)
% 0.54/0.73 | greater(hazard_of_mortality(A,C),hazard_of_mortality(A,B)) ) ).
% 0.54/0.73
% 0.54/0.73 cnf(theorem_6_40,negated_conjecture,
% 0.54/0.73 organization(sk2) ).
% 0.54/0.73
% 0.54/0.73 cnf(theorem_6_41,negated_conjecture,
% 0.54/0.73 has_endowment(sk2) ).
% 0.54/0.73
% 0.54/0.73 cnf(theorem_6_42,negated_conjecture,
% 0.54/0.73 age(sk2,sk3) = zero ).
% 0.54/0.73
% 0.54/0.73 cnf(theorem_6_43,negated_conjecture,
% 0.54/0.73 smaller_or_equal(age(sk2,sk4),eta) ).
% 0.54/0.73
% 0.54/0.73 cnf(theorem_6_44,negated_conjecture,
% 0.54/0.73 greater(age(sk2,sk5),eta) ).
% 0.54/0.73
% 0.54/0.73 cnf(theorem_6_45,negated_conjecture,
% 0.54/0.73 greater(eta,zero) ).
% 0.54/0.73
% 0.54/0.73 cnf(theorem_6_46,negated_conjecture,
% 0.54/0.73 ( ~ greater(hazard_of_mortality(sk2,sk5),hazard_of_mortality(sk2,sk4))
% 0.54/0.73 | hazard_of_mortality(sk2,sk4) != hazard_of_mortality(sk2,sk3) ) ).
% 0.54/0.73
% 0.54/0.73 %--------------------------------------------------------------------------
% 0.54/0.73 %-------------------------------------------
% 0.54/0.73 % Proof found
% 0.54/0.73 % SZS status Theorem for theBenchmark
% 0.54/0.73 % SZS output start Proof
% 0.54/0.73 %ClaNum:46(EqnAxiom:20)
% 0.54/0.73 %VarNum:100(SingletonVarNum:37)
% 0.54/0.73 %MaxLitNum:4
% 0.54/0.73 %MaxfuncDepth:2
% 0.54/0.73 %SharedTerms:20
% 0.54/0.73 %goalClause: 21 22 23 24 25 26 46
% 0.54/0.73 %singleGoalClaCount:6
% 0.54/0.73 [21]P1(a1)
% 0.54/0.73 [22]P4(a1)
% 0.54/0.73 [24]P2(a3,a7)
% 0.54/0.73 [23]E(f2(a1,a6),a7)
% 0.54/0.73 [25]P6(f2(a1,a8),a3)
% 0.54/0.73 [26]P2(f2(a1,a9),a3)
% 0.54/0.73 [46]~P2(f4(a1,a9),f4(a1,a8))+~E(f4(a1,a8),f4(a1,a6))
% 0.54/0.73 [27]~P1(x271)+P4(x271)
% 0.54/0.73 [28]~E(x281,x282)+P6(x281,x282)
% 0.54/0.73 [29]~E(x291,x292)+P3(x291,x292)
% 0.54/0.73 [31]~P7(x311,x312)+P6(x311,x312)
% 0.54/0.73 [32]~P2(x322,x321)+P7(x321,x322)
% 0.54/0.73 [33]~P2(x331,x332)+P3(x331,x332)
% 0.54/0.73 [34]~P7(x342,x341)+P2(x341,x342)
% 0.54/0.73 [37]~P2(x372,x371)+~P2(x371,x372)
% 0.54/0.73 [30]P7(x301,x302)+P2(x301,x302)+E(x301,x302)
% 0.54/0.73 [35]P7(x351,x352)+~P6(x351,x352)+E(x351,x352)
% 0.54/0.73 [36]P2(x361,x362)+~P3(x361,x362)+E(x361,x362)
% 0.54/0.73 [40]~P1(x401)+P5(x401,x402)+~P6(f2(x401,x402),a3)
% 0.54/0.73 [42]~P1(x421)+~P5(x421,x422)+~P2(f2(x421,x422),a3)
% 0.54/0.73 [38]~P2(x381,x383)+P2(x381,x382)+~P2(x383,x382)
% 0.54/0.73 [41]~P4(x411)+P1(x411)+P5(x411,f5(x411))+P6(f2(x411,f5(x411)),a3)
% 0.54/0.73 [43]~P4(x431)+P1(x431)+~P5(x431,f5(x431))+P2(f2(x431,f5(x431)),a3)
% 0.54/0.73 [45]~P4(x451)+P1(x451)+P6(f2(x451,f5(x451)),a3)+P2(f2(x451,f5(x451)),a3)
% 0.54/0.74 [39]~P4(x391)+~P5(x391,x393)+~P5(x391,x392)+E(f4(x391,x392),f4(x391,x393))
% 0.54/0.74 [44]~P4(x441)+~P5(x441,x443)+P5(x441,x442)+P2(f4(x441,x442),f4(x441,x443))
% 0.54/0.74 %EqnAxiom
% 0.54/0.74 [1]E(x11,x11)
% 0.54/0.74 [2]E(x22,x21)+~E(x21,x22)
% 0.54/0.74 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 0.54/0.74 [4]~E(x41,x42)+E(f2(x41,x43),f2(x42,x43))
% 0.54/0.74 [5]~E(x51,x52)+E(f2(x53,x51),f2(x53,x52))
% 0.54/0.74 [6]~E(x61,x62)+E(f4(x61,x63),f4(x62,x63))
% 0.54/0.74 [7]~E(x71,x72)+E(f4(x73,x71),f4(x73,x72))
% 0.54/0.74 [8]~E(x81,x82)+E(f5(x81),f5(x82))
% 0.54/0.74 [9]~P1(x91)+P1(x92)+~E(x91,x92)
% 0.54/0.74 [10]~P4(x101)+P4(x102)+~E(x101,x102)
% 0.54/0.74 [11]P2(x112,x113)+~E(x111,x112)+~P2(x111,x113)
% 0.54/0.74 [12]P2(x123,x122)+~E(x121,x122)+~P2(x123,x121)
% 0.54/0.74 [13]P6(x132,x133)+~E(x131,x132)+~P6(x131,x133)
% 0.54/0.74 [14]P6(x143,x142)+~E(x141,x142)+~P6(x143,x141)
% 0.54/0.74 [15]P5(x152,x153)+~E(x151,x152)+~P5(x151,x153)
% 0.54/0.74 [16]P5(x163,x162)+~E(x161,x162)+~P5(x163,x161)
% 0.54/0.74 [17]P7(x172,x173)+~E(x171,x172)+~P7(x171,x173)
% 0.54/0.74 [18]P7(x183,x182)+~E(x181,x182)+~P7(x183,x181)
% 0.54/0.74 [19]P3(x192,x193)+~E(x191,x192)+~P3(x191,x193)
% 0.54/0.74 [20]P3(x203,x202)+~E(x201,x202)+~P3(x203,x201)
% 0.54/0.74
% 0.54/0.74 %-------------------------------------------
% 0.54/0.74 cnf(49,plain,
% 0.54/0.74 (~P2(a7,a3)),
% 0.54/0.74 inference(scs_inference,[],[24,37])).
% 0.54/0.74 cnf(51,plain,
% 0.54/0.74 (E(a7,f2(a1,a6))),
% 0.54/0.74 inference(scs_inference,[],[24,23,37,2])).
% 0.54/0.74 cnf(52,plain,
% 0.54/0.74 (P5(a1,a8)),
% 0.54/0.74 inference(scs_inference,[],[21,24,23,25,37,2,40])).
% 0.54/0.74 cnf(54,plain,
% 0.54/0.74 (~P5(a1,a9)),
% 0.54/0.74 inference(scs_inference,[],[21,24,23,25,26,37,2,40,42])).
% 0.54/0.74 cnf(56,plain,
% 0.54/0.74 (P2(f2(a1,a9),a7)),
% 0.54/0.74 inference(scs_inference,[],[21,24,23,25,26,37,2,40,42,38])).
% 0.54/0.74 cnf(59,plain,
% 0.54/0.74 (P2(a3,f2(a1,a6))),
% 0.54/0.74 inference(scs_inference,[],[21,24,23,25,26,37,2,40,42,38,11,12])).
% 0.54/0.74 cnf(81,plain,
% 0.54/0.74 (~P2(a3,f2(a1,a9))),
% 0.54/0.74 inference(scs_inference,[],[26,37])).
% 0.54/0.74 cnf(83,plain,
% 0.54/0.74 (~P2(a7,f2(a1,a9))),
% 0.54/0.74 inference(scs_inference,[],[26,49,37,38])).
% 0.54/0.74 cnf(85,plain,
% 0.54/0.74 (~E(a7,f2(a1,a9))),
% 0.54/0.74 inference(scs_inference,[],[24,26,49,37,38,12])).
% 0.54/0.74 cnf(101,plain,
% 0.54/0.74 (~P2(f2(a1,a6),a3)),
% 0.54/0.74 inference(scs_inference,[],[83,59,34,37])).
% 0.54/0.74 cnf(103,plain,
% 0.54/0.74 (P2(f2(a1,a9),f2(a1,a6))),
% 0.54/0.74 inference(scs_inference,[],[26,83,59,34,37,38])).
% 0.54/0.74 cnf(105,plain,
% 0.54/0.74 (P7(a7,f2(a1,a9))),
% 0.54/0.74 inference(scs_inference,[],[26,85,83,59,34,37,38,30])).
% 0.54/0.74 cnf(109,plain,
% 0.54/0.74 (P7(f2(a1,a6),f2(a1,a9))),
% 0.54/0.74 inference(scs_inference,[],[26,51,81,85,83,59,34,37,38,30,12,5,17])).
% 0.54/0.74 cnf(111,plain,
% 0.54/0.74 (P2(x1111,a7)+~E(a3,x1111)),
% 0.54/0.74 inference(scs_inference,[],[26,24,51,81,85,83,59,34,37,38,30,12,5,17,18,11])).
% 0.54/0.74 cnf(114,plain,
% 0.54/0.74 (P6(f2(a1,a8),x1141)+~E(a3,x1141)),
% 0.54/0.74 inference(scs_inference,[],[25,26,24,51,81,85,83,59,34,37,38,30,12,5,17,18,11,9,13,14])).
% 0.54/0.74 cnf(122,plain,
% 0.54/0.74 (~P2(f2(a1,a6),f2(a1,a9))),
% 0.54/0.74 inference(scs_inference,[],[103,101,34,37])).
% 0.54/0.74 cnf(126,plain,
% 0.54/0.74 (E(a7,a3)+P7(f2(a1,a6),a3)),
% 0.54/0.74 inference(scs_inference,[],[51,103,101,34,37,30,3])).
% 0.54/0.74 cnf(136,plain,
% 0.54/0.74 (P2(x1361,f2(a1,a6))+~E(a3,x1361)),
% 0.54/0.74 inference(scs_inference,[],[59,56,109,122,34,38,18,11])).
% 0.54/0.74 cnf(156,plain,
% 0.54/0.74 (P2(f4(a1,a9),f4(a1,a8))),
% 0.54/0.74 inference(scs_inference,[],[21,52,54,27,44])).
% 0.54/0.74 cnf(157,plain,
% 0.54/0.74 (~E(f4(a1,a8),f4(a1,a6))),
% 0.54/0.74 inference(scs_inference,[],[156,46])).
% 0.54/0.74 cnf(169,plain,
% 0.54/0.74 (P6(f2(a1,a6),f2(a1,a9))),
% 0.54/0.74 inference(scs_inference,[],[105,51,31,13])).
% 0.54/0.74 cnf(172,plain,
% 0.54/0.74 (~P5(a1,a6)),
% 0.54/0.74 inference(scs_inference,[],[22,23,157,52,169,7,13,39])).
% 0.54/0.74 cnf(199,plain,
% 0.54/0.74 (P3(x1991,a3)+~E(f2(a1,a9),x1991)),
% 0.54/0.74 inference(scs_inference,[],[26,33,19])).
% 0.54/0.74 cnf(200,plain,
% 0.54/0.74 (P3(f2(a1,a9),a3)),
% 0.54/0.74 inference(equality_inference,[],[199])).
% 0.54/0.74 cnf(201,plain,
% 0.54/0.74 (P3(f2(a1,a9),x2011)+~E(a3,x2011)),
% 0.54/0.74 inference(scs_inference,[],[200,20])).
% 0.54/0.74 cnf(215,plain,
% 0.54/0.74 (P6(f2(a1,a6),a3)+E(a7,a3)),
% 0.54/0.74 inference(scs_inference,[],[126,31])).
% 0.54/0.74 cnf(221,plain,
% 0.54/0.74 (E(a3,a7)+P6(f2(a1,a6),a3)),
% 0.54/0.74 inference(scs_inference,[],[215,2])).
% 0.54/0.74 cnf(223,plain,
% 0.54/0.74 (E(a3,a7)),
% 0.54/0.74 inference(scs_inference,[],[21,172,221,40])).
% 0.54/0.74 cnf(229,plain,
% 0.54/0.74 ($false),
% 0.54/0.74 inference(scs_inference,[],[223,111,114,136,201,2,37]),
% 0.54/0.74 ['proof']).
% 0.54/0.74 % SZS output end Proof
% 0.54/0.74 % Total time :0.258473s
%------------------------------------------------------------------------------