%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : MGT054+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 : 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:21 AM UTC 2026
% Result : Theorem 58.54s 58.77s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : MGT054+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.08/0.36 % Computer : n007.cluster.edu
% 0.08/0.36 % Model : x86_64 x86_64
% 0.08/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.36 % Memory : 8046.5625MB
% 0.08/0.36 % OS : Linux 6.8.0-71-generic
% 0.08/0.36 % CPULimit : 300
% 0.08/0.36 % WCLimit : 300
% 0.08/0.36 % DateTime : Mon Sep 7 13:22:41 UTC 2026
% 0.08/0.36 % CPUTime :
% 0.23/0.51 start to proof:theBenchmark
% 58.54/58.76 %-------------------------------------------
% 58.54/58.76 % File :CSE---1.7
% 58.54/58.76 % Problem :theBenchmark
% 58.54/58.76 % Transform :cnf
% 58.54/58.76 % Format :tptp:raw
% 58.54/58.76 % Command :java -jar mcs_scs.jar %d %s
% 58.54/58.76
% 58.54/58.76 % Result :Theorem 58.234874s
% 58.54/58.76 % Output :CNFRefutation 58.234874s
% 58.54/58.76 %-------------------------------------------
% 58.54/58.76 %--------------------------------------------------------------------------
% 58.54/58.76 % File : MGT054+1 : TPTP v9.3.0. Released v2.4.0.
% 58.54/58.76 % Domain : Management (Organisation Theory)
% 58.54/58.76 % Problem : Hazard of mortality increases in a drifting environment
% 58.54/58.76 % Version : [Han98] axioms.
% 58.54/58.76 % English : An unendowed organization's hazard of mortality increases with
% 58.54/58.76 % age in a drifting environment.
% 58.54/58.76
% 58.54/58.76 % Refs : [Kam00] Kamps (2000), Email to G. Sutcliffe
% 58.54/58.76 % : [CH00] Carroll & Hannan (2000), The Demography of Corporation
% 58.54/58.76 % : [Han98] Hannan (1998), Rethinking Age Dependence in Organizati
% 58.54/58.76 % Source : [Kam00]
% 58.54/58.76 % Names : THEOREM 5 [Han98]
% 58.54/58.76
% 58.54/58.76 % Status : Theorem
% 58.54/58.76 % Rating : 0.13 v9.3.0, 0.21 v9.1.0, 0.18 v9.0.0, 0.22 v8.2.0, 0.19 v8.1.0, 0.17 v7.5.0, 0.19 v7.4.0, 0.17 v7.3.0, 0.24 v7.2.0, 0.21 v7.1.0, 0.22 v7.0.0, 0.17 v6.4.0, 0.23 v6.3.0, 0.25 v6.2.0, 0.20 v6.1.0, 0.23 v6.0.0, 0.30 v5.5.0, 0.26 v5.4.0, 0.25 v5.3.0, 0.30 v5.2.0, 0.20 v5.1.0, 0.19 v5.0.0, 0.21 v4.1.0, 0.22 v4.0.1, 0.26 v4.0.0, 0.25 v3.7.0, 0.20 v3.5.0, 0.16 v3.3.0, 0.14 v3.2.0, 0.27 v3.1.0, 0.22 v2.7.0, 0.17 v2.6.0, 0.33 v2.5.0, 0.17 v2.4.0
% 58.54/58.76 % Syntax : Number of formulae : 14 ( 0 unt; 0 def)
% 58.54/58.76 % Number of atoms : 50 ( 6 equ)
% 58.54/58.76 % Maximal formula atoms : 7 ( 3 avg)
% 58.54/58.76 % Number of connectives : 45 ( 9 ~; 4 |; 18 &)
% 58.54/58.76 % ( 6 <=>; 8 =>; 0 <=; 0 <~>)
% 58.54/58.76 % Maximal formula depth : 11 ( 7 avg)
% 58.54/58.76 % Maximal term depth : 2 ( 1 avg)
% 58.54/58.76 % Number of predicates : 10 ( 9 usr; 0 prp; 1-3 aty)
% 58.54/58.76 % Number of functors : 5 ( 5 usr; 2 con; 0-2 aty)
% 58.54/58.76 % Number of variables : 36 ( 36 !; 0 ?)
% 58.54/58.76 % SPC : FOF_THM_RFO_SEQ
% 58.54/58.76
% 58.54/58.76 % Comments : See MGT042+1.p for the mnemonic names.
% 58.54/58.76 %--------------------------------------------------------------------------
% 58.54/58.76 include('Axioms/MGT001+0.ax').
% 58.54/58.76 %--------------------------------------------------------------------------
% 58.54/58.76 %----Problem Axioms
% 58.54/58.76 %----An unendowed organization never possesses immunity.
% 58.54/58.76 fof(assumption_1,axiom,
% 58.54/58.76 ! [X,T] :
% 58.54/58.76 ( ( organization(X)
% 58.54/58.76 & ~ has_endowment(X) )
% 58.54/58.76 => ~ has_immunity(X,T) ) ).
% 58.54/58.76
% 58.54/58.76 %----An organization's hazard of mortality is lower during periods in
% 58.54/58.76 %----which it has immunity than in periods in which it does not.
% 58.54/58.76 fof(assumption_3,axiom,
% 58.54/58.76 ! [X,T0,T] :
% 58.54/58.76 ( ( organization(X)
% 58.54/58.76 & has_immunity(X,T0)
% 58.54/58.76 & ~ has_immunity(X,T) )
% 58.54/58.76 => greater(hazard_of_mortality(X,T),hazard_of_mortality(X,T0)) ) ).
% 58.54/58.76
% 58.54/58.76 %----Two states of the environment are dissimilar for an organization
% 58.54/58.76 %----if and only if the organization cannot be aligned to both.
% 58.54/58.76 %----
% 58.54/58.76 %----Added quantification over X.
% 58.54/58.76 fof(definition_2,axiom,
% 58.54/58.76 ! [X,T0,T] :
% 58.54/58.76 ( dissimilar(X,T0,T)
% 58.54/58.76 <=> ( organization(X)
% 58.54/58.76 & ~ ( is_aligned(X,T0)
% 58.54/58.76 <=> is_aligned(X,T) ) ) ) ).
% 58.54/58.76
% 58.54/58.76 %----An organization is aligned with the state of the environment at
% 58.54/58.76 %----its time of founding.
% 58.54/58.76 fof(assumption_13,axiom,
% 58.54/58.76 ! [X,T] :
% 58.54/58.76 ( ( organization(X)
% 58.54/58.76 & age(X,T) = zero )
% 58.54/58.76 => is_aligned(X,T) ) ).
% 58.54/58.76
% 58.54/58.76 %----An organization's capability is higher in the state of the
% 58.54/58.76 %----environment to which it is aligned.
% 58.54/58.76 %----
% 58.54/58.77 %----Changed dissimilar(X,T0,T) to ~ is_aligned(X,T).
% 58.54/58.77 %----This makes theorem 5,9,10,11 and lemma 8 derivable.
% 58.54/58.77 fof(assumption_14,axiom,
% 58.54/58.77 ! [X,T0,T] :
% 58.54/58.77 ( ( organization(X)
% 58.54/58.77 & is_aligned(X,T0)
% 58.54/58.77 & ~ is_aligned(X,T) )
% 58.54/58.77 => greater(capability(X,T0),capability(X,T)) ) ).
% 58.54/58.77
% 58.54/58.77 %----Environmental drift: the environments at times separated by more
% 58.54/58.77 %----than `sigma' are dissimilar.
% 58.54/58.77 fof(assumption_15,axiom,
% 58.54/58.77 ! [X,T0,T] :
% 58.54/58.77 ( ( organization(X)
% 58.54/58.77 & age(X,T0) = zero )
% 58.54/58.77 => ( greater(age(X,T),sigma)
% 58.54/58.77 <=> dissimilar(X,T0,T) ) ) ).
% 58.54/58.77
% 58.54/58.77 %----Superiority in capability lowers the hazard of mortality when an
% 58.54/58.77 %----organization lacks immunity.
% 58.54/58.77 fof(assumption_16,axiom,
% 58.54/58.77 ! [X,T0,T] :
% 58.54/58.77 ( ( organization(X)
% 58.54/58.77 & ~ has_immunity(X,T0)
% 58.54/58.77 & ~ has_immunity(X,T)
% 58.54/58.77 & greater(capability(X,T),capability(X,T0)) )
% 58.54/58.77 => greater(hazard_of_mortality(X,T0),hazard_of_mortality(X,T)) ) ).
% 58.54/58.77
% 58.54/58.77 %----Problem theorems
% 58.54/58.77 %----The obsolescence theorem for unendowed organizations (Barron et
% 58.54/58.77 %----al. 1994): an unendowed organization's hazard of mortality
% 58.54/58.77 %----increases with age in a drifting environment.
% 58.54/58.77 %----From D2, A1, A3, A13-16 (text says D1-2, A1-3, 13-16; also needs D<,
% 58.54/58.77 %----D<=, MP>str).
% 58.54/58.77 fof(theorem_5,conjecture,
% 58.54/58.77 ! [X,T0,T1,T2] :
% 58.54/58.77 ( ( organization(X)
% 58.54/58.77 & ~ has_endowment(X)
% 58.54/58.77 & age(X,T0) = zero
% 58.54/58.77 & smaller_or_equal(age(X,T1),sigma)
% 58.54/58.77 & greater(age(X,T2),sigma)
% 58.54/58.77 & greater(sigma,zero) )
% 58.54/58.77 => greater(hazard_of_mortality(X,T2),hazard_of_mortality(X,T1)) ) ).
% 58.54/58.77
% 58.54/58.77 %--------------------------------------------------------------------------
% 58.54/58.77 %-------------------------------------------
% 58.54/58.77 % Proof found
% 58.54/58.77 % SZS status Theorem for theBenchmark
% 58.54/58.77 % SZS output start Proof
% 58.54/58.77 %ClaNum:56(EqnAxiom:26)
% 58.54/58.77 %VarNum:142(SingletonVarNum:57)
% 58.54/58.77 %MaxLitNum:5
% 58.54/58.77 %MaxfuncDepth:1
% 58.54/58.77 %SharedTerms:18
% 58.54/58.77 %goalClause: 27 28 29 30 31 32 33
% 58.54/58.77 %singleGoalClaCount:7
% 58.54/58.77 [27]P1(a1)
% 58.54/58.77 [29]P2(a6,a5)
% 58.54/58.77 [32]~P4(a1)
% 58.54/58.77 [28]E(f2(a1,a4),a5)
% 58.54/58.77 [30]P8(f2(a1,a7),a6)
% 58.54/58.77 [31]P2(f2(a1,a8),a6)
% 58.54/58.77 [33]~P2(f9(a1,a8),f9(a1,a7))
% 58.54/58.77 [34]~E(x341,x342)+P8(x341,x342)
% 58.54/58.77 [35]~E(x351,x352)+P5(x351,x352)
% 58.54/58.77 [38]~P9(x381,x382)+P8(x381,x382)
% 58.54/58.77 [39]~P2(x392,x391)+P9(x391,x392)
% 58.54/58.77 [40]~P2(x401,x402)+P5(x401,x402)
% 58.54/58.77 [41]~P9(x412,x411)+P2(x411,x412)
% 58.54/58.77 [45]~P2(x452,x451)+~P2(x451,x452)
% 58.54/58.77 [47]P1(x471)+~P3(x471,x472,x473)
% 58.54/58.77 [36]P9(x361,x362)+P2(x361,x362)+E(x361,x362)
% 58.54/58.77 [37]~P1(x371)+P4(x371)+~P6(x371,x372)
% 58.54/58.77 [42]P9(x421,x422)+~P8(x421,x422)+E(x421,x422)
% 58.54/58.77 [43]P2(x431,x432)+~P5(x431,x432)+E(x431,x432)
% 58.54/58.77 [44]~P1(x441)+P7(x441,x442)+~E(f2(x441,x442),a5)
% 58.54/58.77 [46]~P2(x461,x463)+P2(x461,x462)+~P2(x463,x462)
% 58.54/58.77 [52]~P3(x521,x523,x522)+P7(x521,x522)+P7(x521,x523)
% 58.54/58.77 [53]~P3(x531,x533,x532)+~P7(x531,x532)+~P7(x531,x533)
% 58.54/58.77 [48]~P1(x481)+~P7(x481,x483)+P7(x481,x482)+P3(x481,x482,x483)
% 58.54/58.77 [49]~P1(x491)+~P7(x491,x493)+P7(x491,x492)+P3(x491,x493,x492)
% 58.54/58.77 [50]~P1(x501)+~P6(x501,x503)+P6(x501,x502)+P2(f9(x501,x502),f9(x501,x503))
% 58.54/58.77 [51]~P1(x511)+~P7(x511,x513)+P7(x511,x512)+P2(f3(x511,x513),f3(x511,x512))
% 58.54/58.77 [54]~P1(x541)+P3(x541,x542,x543)+~E(f2(x541,x542),a5)+~P2(f2(x541,x543),a6)
% 58.54/58.77 [55]~P1(x551)+~P3(x551,x553,x552)+P2(f2(x551,x552),a6)+~E(f2(x551,x553),a5)
% 58.54/58.77 [56]~P1(x561)+P6(x561,x562)+P6(x561,x563)+P2(f9(x561,x563),f9(x561,x562))+~P2(f3(x561,x562),f3(x561,x563))
% 58.54/58.77 %EqnAxiom
% 58.54/58.77 [1]E(x11,x11)
% 58.54/58.77 [2]E(x22,x21)+~E(x21,x22)
% 58.54/58.77 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 58.54/58.77 [4]~E(x41,x42)+E(f2(x41,x43),f2(x42,x43))
% 58.54/58.77 [5]~E(x51,x52)+E(f2(x53,x51),f2(x53,x52))
% 58.54/58.77 [6]~E(x61,x62)+E(f3(x61,x63),f3(x62,x63))
% 58.54/58.77 [7]~E(x71,x72)+E(f3(x73,x71),f3(x73,x72))
% 58.54/58.77 [8]~E(x81,x82)+E(f9(x81,x83),f9(x82,x83))
% 58.54/58.77 [9]~E(x91,x92)+E(f9(x93,x91),f9(x93,x92))
% 58.54/58.77 [10]~P1(x101)+P1(x102)+~E(x101,x102)
% 58.54/58.77 [11]P2(x112,x113)+~E(x111,x112)+~P2(x111,x113)
% 58.54/58.77 [12]P2(x123,x122)+~E(x121,x122)+~P2(x123,x121)
% 58.54/58.77 [13]P8(x132,x133)+~E(x131,x132)+~P8(x131,x133)
% 58.54/58.77 [14]P8(x143,x142)+~E(x141,x142)+~P8(x143,x141)
% 58.54/58.77 [15]P3(x152,x153,x154)+~E(x151,x152)+~P3(x151,x153,x154)
% 58.54/58.77 [16]P3(x163,x162,x164)+~E(x161,x162)+~P3(x163,x161,x164)
% 58.54/58.77 [17]P3(x173,x174,x172)+~E(x171,x172)+~P3(x173,x174,x171)
% 58.54/58.77 [18]~P4(x181)+P4(x182)+~E(x181,x182)
% 58.54/58.77 [19]P7(x192,x193)+~E(x191,x192)+~P7(x191,x193)
% 58.54/58.77 [20]P7(x203,x202)+~E(x201,x202)+~P7(x203,x201)
% 58.54/58.77 [21]P6(x212,x213)+~E(x211,x212)+~P6(x211,x213)
% 58.54/58.77 [22]P6(x223,x222)+~E(x221,x222)+~P6(x223,x221)
% 58.54/58.77 [23]P5(x232,x233)+~E(x231,x232)+~P5(x231,x233)
% 58.54/58.77 [24]P5(x243,x242)+~E(x241,x242)+~P5(x243,x241)
% 58.54/58.77 [25]P9(x252,x253)+~E(x251,x252)+~P9(x251,x253)
% 58.54/58.77 [26]P9(x263,x262)+~E(x261,x262)+~P9(x263,x261)
% 58.54/58.77
% 58.54/58.77 %-------------------------------------------
% 58.54/58.77 cnf(57,plain,
% 58.54/58.77 (P8(x571,x571)),
% 58.54/58.77 inference(equality_inference,[],[34])).
% 58.54/58.77 cnf(58,plain,
% 58.54/58.77 (P5(x581,x581)),
% 58.54/58.77 inference(equality_inference,[],[35])).
% 58.54/58.77 cnf(59,plain,
% 58.54/58.77 (E(a5,f2(a1,a4))),
% 58.54/58.77 inference(scs_inference,[],[28,2])).
% 58.54/58.77 cnf(62,plain,
% 58.54/58.77 (~P2(a5,a6)),
% 58.54/58.77 inference(scs_inference,[],[29,33,28,2,41,45])).
% 58.54/58.77 cnf(64,plain,
% 58.54/58.77 (~P6(a1,x641)),
% 58.54/58.77 inference(scs_inference,[],[27,29,32,33,28,2,41,45,37])).
% 58.54/58.77 cnf(66,plain,
% 58.54/58.77 (P7(a1,a4)),
% 58.54/58.77 inference(scs_inference,[],[27,29,32,33,28,2,41,45,37,44])).
% 58.54/58.77 cnf(68,plain,
% 58.54/58.77 (~E(f2(a1,a8),a5)),
% 58.54/58.77 inference(scs_inference,[],[27,29,32,33,28,31,2,41,45,37,44,11])).
% 58.54/58.77 cnf(69,plain,
% 58.54/58.77 (P2(a6,f2(a1,a4))),
% 58.54/58.77 inference(scs_inference,[],[27,29,32,33,28,31,2,41,45,37,44,11,12])).
% 58.54/58.77 cnf(70,plain,
% 58.54/58.77 (P8(a5,f2(a1,a4))),
% 58.54/58.77 inference(scs_inference,[],[27,29,32,33,28,31,57,2,41,45,37,44,11,12,13])).
% 58.54/58.77 cnf(71,plain,
% 58.54/58.77 (P8(x711,x711)),
% 58.54/58.77 inference(rename_variables,[],[57])).
% 58.54/58.77 cnf(74,plain,
% 58.54/58.77 (P2(f2(a1,a8),a5)),
% 58.54/58.77 inference(scs_inference,[],[27,29,32,33,28,31,57,71,2,41,45,37,44,11,12,13,14,46])).
% 58.54/58.77 cnf(79,plain,
% 58.54/58.77 (P5(x791,x791)),
% 58.54/58.77 inference(rename_variables,[],[58])).
% 58.54/58.77 cnf(82,plain,
% 58.54/58.77 (P3(a1,a4,a8)),
% 58.54/58.77 inference(scs_inference,[],[27,29,32,33,28,31,57,71,58,79,2,41,45,37,44,11,12,13,14,46,53,23,24,54])).
% 58.54/58.77 cnf(84,plain,
% 58.54/58.77 (~E(f2(a1,a8),f2(a1,a4))),
% 58.54/58.77 inference(scs_inference,[],[27,29,32,33,28,31,57,71,58,79,2,41,45,37,44,11,12,13,14,46,53,23,24,54,3])).
% 58.54/58.77 cnf(90,plain,
% 58.54/58.77 (~P2(a6,f2(a1,a8))),
% 58.54/58.77 inference(scs_inference,[],[31,45])).
% 58.54/58.77 cnf(92,plain,
% 58.54/58.77 (~P9(a6,a5)),
% 58.54/58.77 inference(scs_inference,[],[31,62,45,41])).
% 58.54/58.77 cnf(94,plain,
% 58.54/58.77 (~P2(a5,f2(a1,a8))),
% 58.54/58.77 inference(scs_inference,[],[31,62,45,41,46])).
% 58.54/58.77 cnf(96,plain,
% 58.54/58.77 (~E(a5,f2(a1,a8))),
% 58.54/58.77 inference(scs_inference,[],[29,31,62,45,41,46,12])).
% 58.54/58.77 cnf(98,plain,
% 58.54/58.77 (P9(a5,f2(a1,a8))),
% 58.54/58.77 inference(scs_inference,[],[29,31,66,62,45,41,46,12,19,36])).
% 58.54/58.77 cnf(108,plain,
% 58.54/58.77 (~P2(f2(a1,a4),a6)),
% 58.54/58.77 inference(scs_inference,[],[69,45])).
% 58.54/58.77 cnf(110,plain,
% 58.54/58.77 (~P9(f2(a1,a8),a6)),
% 58.54/58.77 inference(scs_inference,[],[69,90,45,41])).
% 58.54/58.77 cnf(112,plain,
% 58.54/58.77 (P2(f2(a1,a8),f2(a1,a4))),
% 58.54/58.77 inference(scs_inference,[],[31,69,90,45,41,46])).
% 58.54/58.77 cnf(122,plain,
% 58.54/58.77 (~P2(f2(a1,a4),f2(a1,a8))),
% 58.54/58.77 inference(scs_inference,[],[112,45])).
% 58.54/58.77 cnf(124,plain,
% 58.54/58.77 (~P9(f2(a1,a8),a5)),
% 58.54/58.77 inference(scs_inference,[],[94,112,45,41])).
% 58.54/58.77 cnf(134,plain,
% 58.54/58.77 (~P9(a6,f2(a1,a4))),
% 58.54/58.77 inference(scs_inference,[],[108,41])).
% 58.54/58.77 cnf(141,plain,
% 58.54/58.77 (~P9(f2(a1,a8),f2(a1,a4))),
% 58.54/58.77 inference(scs_inference,[],[122,41])).
% 58.54/58.77 cnf(145,plain,
% 58.54/58.77 (P3(a1,x1451,a8)+~E(a4,x1451)),
% 58.54/58.77 inference(scs_inference,[],[82,74,122,41,46,16])).
% 58.54/58.77 cnf(147,plain,
% 58.54/58.77 (E(f2(a1,a7),a6)+P9(f2(a1,a7),a6)),
% 58.54/58.77 inference(scs_inference,[],[29,30,82,74,122,41,46,16,11,42])).
% 58.54/58.77 cnf(155,plain,
% 58.54/58.77 (E(a6,f2(a1,a4))+P9(f2(a1,a4),a6)),
% 58.54/58.77 inference(scs_inference,[],[59,108,36,3,2])).
% 58.54/58.77 cnf(191,plain,
% 58.54/58.77 (E(f2(a1,a4),a6)+P9(a5,a6)),
% 58.54/58.77 inference(scs_inference,[],[28,62,36,3])).
% 58.54/58.77 cnf(220,plain,
% 58.54/58.77 (P8(f2(a1,a4),f2(a1,a8))),
% 58.54/58.77 inference(scs_inference,[],[98,59,38,13])).
% 58.54/58.77 cnf(221,plain,
% 58.54/58.77 (P8(a5,f2(a1,a8))),
% 58.54/58.77 inference(scs_inference,[],[28,220,13])).
% 58.54/58.77 cnf(225,plain,
% 58.54/58.77 (P6(a1,a8)+~P2(f3(a1,a7),f3(a1,a8))),
% 58.54/58.77 inference(scs_inference,[],[27,28,31,33,64,220,112,13,14,12,11,56])).
% 58.54/58.77 cnf(231,plain,
% 58.54/58.77 (~P2(f3(a1,a7),f3(a1,a8))),
% 58.54/58.77 inference(scs_inference,[],[64,225])).
% 58.54/58.77 cnf(241,plain,
% 58.54/58.77 (~P7(a1,a7)+P7(a1,a8)),
% 58.54/58.77 inference(scs_inference,[],[27,221,231,14,51])).
% 58.54/58.77 cnf(275,plain,
% 58.54/58.77 (P9(a5,x2751)+~E(a6,x2751)+E(f2(a1,a4),a6)),
% 58.54/58.77 inference(scs_inference,[],[191,26])).
% 58.54/58.77 cnf(330,plain,
% 58.54/58.77 (P2(a6,f2(a1,a7))+E(f2(a1,a7),a6)),
% 58.54/58.77 inference(scs_inference,[],[147,41])).
% 58.54/58.77 cnf(361,plain,
% 58.54/58.78 (P5(a6,f2(a1,a7))+P2(a6,f2(a1,a7))),
% 58.54/58.78 inference(scs_inference,[],[58,330,23])).
% 58.54/58.78 cnf(1321,plain,
% 58.54/58.78 (~P8(a6,f2(a1,a4))+E(a6,f2(a1,a4))),
% 58.54/58.78 inference(scs_inference,[],[108,41,42])).
% 58.54/58.78 cnf(1322,plain,
% 58.54/58.78 (E(a6,a5)+~P8(a6,f2(a1,a4))),
% 58.54/58.78 inference(scs_inference,[],[28,1321,3])).
% 58.54/58.78 cnf(1323,plain,
% 58.54/58.78 (P2(a5,a5)+~P8(a6,f2(a1,a4))),
% 58.54/58.78 inference(scs_inference,[],[29,1322,11])).
% 58.54/58.78 cnf(1324,plain,
% 58.54/58.78 (~P8(a6,f2(a1,a4))),
% 58.54/58.78 inference(scs_inference,[],[1323,45])).
% 58.54/58.78 cnf(1328,plain,
% 58.54/58.78 (~E(a5,a6)),
% 58.54/58.78 inference(scs_inference,[],[70,1324,34,155,13])).
% 58.54/58.78 cnf(1335,plain,
% 58.54/58.78 (~E(f2(a1,a4),a6)),
% 58.54/58.78 inference(scs_inference,[],[57,1324,13])).
% 58.54/58.78 cnf(1337,plain,
% 58.54/58.78 (~E(a6,x13371)+P9(a5,x13371)),
% 58.54/58.78 inference(scs_inference,[],[1335,275])).
% 58.54/58.78 cnf(1338,plain,
% 58.54/58.78 (~E(x13381,a6)+P9(a5,x13381)),
% 58.54/58.78 inference(scs_inference,[],[1337,2])).
% 58.54/58.78 cnf(1347,plain,
% 58.54/58.78 (P2(x13471,a5)+~E(x13471,a6)),
% 58.54/58.78 inference(scs_inference,[],[41,1338])).
% 58.54/58.78 cnf(1371,plain,
% 58.54/58.78 (~P5(a5,a6)),
% 58.54/58.78 inference(scs_inference,[],[29,1328,45,43])).
% 58.54/58.78 cnf(1374,plain,
% 58.54/58.78 (~P2(f3(a1,x13741),f3(a1,x13741))),
% 58.54/58.78 inference(scs_inference,[],[27,64,45,56])).
% 58.54/58.78 cnf(1575,plain,
% 58.54/58.78 (P7(a1,a8)+~E(f2(a1,a7),a5)),
% 58.54/58.78 inference(scs_inference,[],[27,241,44])).
% 58.54/58.78 cnf(1576,plain,
% 58.54/58.78 (P3(a1,x15761,a8)+P7(a1,x15761)+~E(f2(a1,a7),a5)),
% 58.54/58.78 inference(scs_inference,[],[27,1575,48])).
% 58.54/58.78 cnf(1577,plain,
% 58.54/58.78 (~E(a5,f2(a1,a7))+P7(a1,x15771)+P3(a1,x15771,a8)),
% 58.54/58.78 inference(scs_inference,[],[1576,2])).
% 58.54/58.78 cnf(1578,plain,
% 58.54/58.78 (~E(f2(a1,a4),f2(a1,a7))+P7(a1,x15781)+P3(a1,x15781,a8)),
% 58.54/58.78 inference(scs_inference,[],[59,1577,3])).
% 58.54/58.78 cnf(1579,plain,
% 58.54/58.78 (~E(f2(a1,a7),f2(a1,a4))+P7(a1,x15791)+P3(a1,x15791,a8)),
% 58.54/58.78 inference(scs_inference,[],[1578,2])).
% 58.54/58.78 cnf(1595,plain,
% 58.54/58.78 (P7(a1,a8)+P3(a1,a4,a7)),
% 58.54/58.78 inference(scs_inference,[],[66,27,241,49])).
% 58.54/58.78 cnf(1641,plain,
% 58.54/58.78 (~P2(a5,x16411)+~E(x16411,a6)),
% 58.54/58.78 inference(scs_inference,[],[1347,45])).
% 58.54/58.78 cnf(1718,plain,
% 58.54/58.78 (P9(f2(a1,a7),a6)+~P2(a5,f2(a1,a7))),
% 58.54/58.78 inference(scs_inference,[],[1641,147])).
% 58.54/58.78 cnf(1719,plain,
% 58.54/58.78 (P2(a6,f2(a1,a7))+~P2(a5,f2(a1,a7))),
% 58.54/58.78 inference(scs_inference,[],[1718,41])).
% 58.54/58.78 cnf(1731,plain,
% 58.54/58.78 (~P7(a1,a8)),
% 58.54/58.78 inference(scs_inference,[],[66,145,53])).
% 58.54/58.78 cnf(1732,plain,
% 58.54/58.78 (~P7(a1,a7)),
% 58.54/58.78 inference(scs_inference,[],[1731,241])).
% 58.54/58.78 cnf(1737,plain,
% 58.54/58.78 (P3(a1,a4,a7)),
% 58.54/58.78 inference(scs_inference,[],[1731,1595])).
% 58.54/58.78 cnf(1750,plain,
% 58.54/58.78 (~E(a5,f2(a1,a7))),
% 58.54/58.78 inference(scs_inference,[],[1731,52,1577])).
% 58.54/58.78 cnf(1754,plain,
% 58.54/58.78 (~E(f2(a1,a7),f2(a1,a4))),
% 58.54/58.78 inference(scs_inference,[],[1731,52,1577,1578,1579])).
% 58.54/58.78 cnf(2169,plain,
% 58.54/58.78 (~P5(f2(a1,a4),a6)),
% 58.54/58.78 inference(scs_inference,[],[28,96,1371,141,94,84,43,42,23])).
% 58.54/58.78 cnf(2170,plain,
% 58.54/58.78 (~P8(a6,a5)),
% 58.54/58.78 inference(scs_inference,[],[28,96,1371,141,94,1324,84,59,43,42,23,14])).
% 58.54/58.78 cnf(2171,plain,
% 58.54/58.78 (P2(f2(a1,a7),a6)),
% 58.54/58.78 inference(scs_inference,[],[28,96,1371,141,94,1737,1324,84,59,27,43,42,23,14,55])).
% 58.54/58.78 cnf(2175,plain,
% 58.54/58.78 (P2(f3(a1,a4),f3(a1,a8))),
% 58.54/58.78 inference(scs_inference,[],[28,96,1371,141,94,1737,1324,84,1731,59,66,27,43,42,23,14,55,48,51])).
% 58.54/58.78 cnf(2179,plain,
% 58.54/58.78 (P9(a6,f2(a1,a7))),
% 58.54/58.78 inference(scs_inference,[],[28,96,1371,141,94,1737,1324,84,1731,59,66,27,43,42,23,14,55,48,51,40,39])).
% 58.54/58.78 cnf(2181,plain,
% 58.54/58.78 (~P2(a6,f2(a1,a7))),
% 58.54/58.78 inference(scs_inference,[],[28,96,1371,141,94,1737,1324,84,1731,59,66,27,43,42,23,14,55,48,51,40,39,45])).
% 58.54/58.78 cnf(2184,plain,
% 58.54/58.78 (~P2(f3(a1,a8),f3(a1,a4))),
% 58.54/58.78 inference(scs_inference,[],[28,96,1371,141,1374,94,1737,1324,84,1731,59,66,27,43,42,23,14,55,48,51,40,39,45,21,46])).
% 58.54/58.78 cnf(2198,plain,
% 58.54/58.78 (E(f2(a1,a7),a6)),
% 58.54/58.78 inference(scs_inference,[],[2181,330])).
% 58.54/58.78 cnf(2199,plain,
% 58.54/58.78 (P5(a6,f2(a1,a7))),
% 58.54/58.78 inference(scs_inference,[],[2181,361])).
% 58.54/58.78 cnf(2206,plain,
% 58.54/58.78 (~P2(a5,f2(a1,a7))),
% 58.54/58.78 inference(scs_inference,[],[2181,1719])).
% 58.54/58.78 cnf(2214,plain,
% 58.54/58.78 (P9(f3(a1,a8),f3(a1,a4))),
% 58.54/58.78 inference(scs_inference,[],[2179,2175,40,38,39])).
% 58.54/58.78 cnf(2220,plain,
% 58.54/58.78 (P2(f2(a1,a7),f2(a1,a4))),
% 58.54/58.78 inference(scs_inference,[],[2171,2206,2179,2175,1750,124,69,68,40,38,39,43,42,46])).
% 58.54/58.78 cnf(2222,plain,
% 58.54/58.78 (~P9(f2(a1,a7),f2(a1,a4))),
% 58.54/58.78 inference(scs_inference,[],[2198,2171,2206,2179,2175,1750,134,124,69,68,40,38,39,43,42,46,25])).
% 58.54/58.78 cnf(2224,plain,
% 58.54/58.78 (~E(f3(a1,a8),f3(a1,a4))),
% 58.54/58.78 inference(scs_inference,[],[28,2198,2171,2206,2179,2175,1750,134,124,1374,69,68,40,38,39,43,42,46,25,11,12])).
% 58.54/58.78 cnf(2229,plain,
% 58.54/58.78 (P2(f3(a1,a4),f3(a1,a7))),
% 58.54/58.78 inference(scs_inference,[],[28,2170,2198,2171,2206,2179,2175,2169,1750,134,124,1374,110,1732,69,68,66,27,40,38,39,43,42,46,25,11,12,26,24,13,51])).
% 58.54/58.78 cnf(2242,plain,
% 58.54/58.78 (P9(f2(a1,a4),f2(a1,a7))),
% 58.54/58.78 inference(scs_inference,[],[2220,2214,38,40,39])).
% 58.54/58.78 cnf(2249,plain,
% 58.54/58.78 (~P2(f2(a1,a7),f2(a1,a7))),
% 58.54/58.78 inference(scs_inference,[],[2220,2222,2184,2224,2214,2181,1754,92,2198,38,40,39,43,42,25,11])).
% 58.54/58.78 cnf(2263,plain,
% 58.54/58.78 (P9(f3(a1,a7),f3(a1,a4))),
% 58.54/58.78 inference(scs_inference,[],[2242,2229,40,38,39])).
% 58.54/58.78 cnf(2274,plain,
% 58.54/58.78 ($false),
% 58.54/58.78 inference(scs_inference,[],[2249,2263,2199,2181,2171,38,43,12]),
% 58.54/58.78 ['proof']).
% 58.54/58.78 % SZS output end Proof
% 58.54/58.78 % Total time :58.234874s
%------------------------------------------------------------------------------