%------------------------------------------------------------------------------
% 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 : 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 43.05s 43.21s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : MGT050+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.07/0.33 % Computer : n007.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:15:11 UTC 2026
% 0.07/0.33 % CPUTime :
% 0.24/0.50 start to proof:theBenchmark
% 43.05/43.20 %-------------------------------------------
% 43.05/43.20 % File :CSE---1.7
% 43.05/43.20 % Problem :theBenchmark
% 43.05/43.20 % Transform :cnf
% 43.05/43.20 % Format :tptp:raw
% 43.05/43.20 % Command :java -jar mcs_scs.jar %d %s
% 43.05/43.20
% 43.05/43.20 % Result :Theorem 42.712473s
% 43.05/43.20 % Output :CNFRefutation 42.712473s
% 43.05/43.20 %-------------------------------------------
% 43.05/43.20 %--------------------------------------------------------------------------
% 43.05/43.20 % File : MGT050+1 : TPTP v9.3.0. Released v2.4.0.
% 43.05/43.20 % Domain : Management (Organisation Theory)
% 43.05/43.20 % Problem : Unendowed organization's hazard of mortality increases with age
% 43.05/43.20 % Version : [Han98] axioms.
% 43.05/43.20 % English : An unendowed organization's hazard of mortality increases with
% 43.05/43.20 % its age.
% 43.05/43.20
% 43.05/43.20 % Refs : [Kam00] Kamps (2000), Email to G. Sutcliffe
% 43.05/43.20 % : [CH00] Carroll & Hannan (2000), The Demography of Corporation
% 43.05/43.20 % : [Han98] Hannan (1998), Rethinking Age Dependence in Organizati
% 43.05/43.20 % Source : [Kam00]
% 43.05/43.20 % Names : THEOREM 3 [Han98]
% 43.05/43.20
% 43.05/43.20 % Status : Theorem
% 43.05/43.20 % Rating : 0.13 v9.3.0, 0.18 v9.1.0, 0.12 v9.0.0, 0.14 v8.2.0, 0.11 v8.1.0, 0.06 v7.4.0, 0.10 v7.3.0, 0.03 v7.2.0, 0.00 v7.1.0, 0.04 v7.0.0, 0.13 v6.4.0, 0.15 v6.3.0, 0.12 v6.2.0, 0.16 v6.1.0, 0.27 v6.0.0, 0.17 v5.5.0, 0.19 v5.4.0, 0.25 v5.3.0, 0.30 v5.2.0, 0.20 v5.1.0, 0.19 v5.0.0, 0.25 v4.1.0, 0.17 v4.0.1, 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.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
% 43.05/43.20 % Syntax : Number of formulae : 14 ( 0 unt; 0 def)
% 43.05/43.20 % Number of atoms : 57 ( 13 equ)
% 43.05/43.20 % Maximal formula atoms : 12 ( 4 avg)
% 43.05/43.20 % Number of connectives : 49 ( 6 ~; 4 |; 19 &)
% 43.05/43.20 % ( 3 <=>; 17 =>; 0 <=; 0 <~>)
% 43.05/43.20 % Maximal formula depth : 9 ( 6 avg)
% 43.05/43.20 % Maximal term depth : 2 ( 1 avg)
% 43.05/43.20 % Number of predicates : 8 ( 7 usr; 0 prp; 1-2 aty)
% 43.05/43.20 % Number of functors : 7 ( 7 usr; 0 con; 2-2 aty)
% 43.05/43.20 % Number of variables : 36 ( 36 !; 0 ?)
% 43.05/43.20 % SPC : FOF_THM_RFO_SEQ
% 43.05/43.20
% 43.05/43.21 % Comments : See MGT042+1.p for the mnemonic names.
% 43.05/43.21 %--------------------------------------------------------------------------
% 43.05/43.21 include('Axioms/MGT001+0.ax').
% 43.05/43.21 %--------------------------------------------------------------------------
% 43.05/43.21 %----Problem Axioms
% 43.05/43.21 %----An unendowed organization never possesses immunity.
% 43.05/43.21 fof(assumption_1,axiom,
% 43.05/43.21 ! [X,T] :
% 43.05/43.21 ( ( organization(X)
% 43.05/43.21 & ~ has_endowment(X) )
% 43.05/43.21 => ~ has_immunity(X,T) ) ).
% 43.05/43.21
% 43.05/43.21 %----When an organization lacks immunity, superior capability and
% 43.05/43.21 %----position imply a lower hazard of mortality.
% 43.05/43.21 fof(assumption_4,axiom,
% 43.05/43.21 ! [X,T0,T] :
% 43.05/43.21 ( ( organization(X)
% 43.05/43.21 & ~ has_immunity(X,T0)
% 43.05/43.21 & ~ has_immunity(X,T) )
% 43.05/43.21 => ( ( ( greater(capability(X,T),capability(X,T0))
% 43.05/43.21 & greater_or_equal(position(X,T),position(X,T0)) )
% 43.05/43.21 => smaller(hazard_of_mortality(X,T),hazard_of_mortality(X,T0)) )
% 43.05/43.21 & ( ( greater_or_equal(capability(X,T),capability(X,T0))
% 43.05/43.21 & greater(position(X,T),position(X,T0)) )
% 43.05/43.21 => smaller(hazard_of_mortality(X,T),hazard_of_mortality(X,T0)) )
% 43.05/43.21 & ( ( capability(X,T) = capability(X,T0)
% 43.05/43.21 & position(X,T) = position(X,T0) )
% 43.05/43.21 => hazard_of_mortality(X,T) = hazard_of_mortality(X,T0) ) ) ) ).
% 43.05/43.21
% 43.05/43.21 %----Increased knowledge elevates an organization's capability; and
% 43.05/43.21 %----increased accumulation of organizational internal frictions
% 43.05/43.21 %----diminishes its capability.
% 43.05/43.21 fof(assumption_5,axiom,
% 43.05/43.21 ! [X,T0,T] :
% 43.05/43.21 ( organization(X)
% 43.05/43.21 => ( ( ( greater(stock_of_knowledge(X,T),stock_of_knowledge(X,T0))
% 43.05/43.21 & smaller_or_equal(internal_friction(X,T),internal_friction(X,T0)) )
% 43.05/43.21 => greater(capability(X,T),capability(X,T0)) )
% 43.05/43.21 & ( ( smaller_or_equal(stock_of_knowledge(X,T),stock_of_knowledge(X,T0))
% 43.05/43.21 & greater(internal_friction(X,T),internal_friction(X,T0)) )
% 43.05/43.21 => smaller(capability(X,T),capability(X,T0)) )
% 43.05/43.21 & ( ( stock_of_knowledge(X,T) = stock_of_knowledge(X,T0)
% 43.05/43.21 & internal_friction(X,T) = internal_friction(X,T0) )
% 43.05/43.21 => capability(X,T) = capability(X,T0) ) ) ) ).
% 43.05/43.21
% 43.05/43.21 %----Improved ties with external actors enhance an organization's position.
% 43.05/43.21 fof(assumption_6,axiom,
% 43.05/43.21 ! [X,T0,T] :
% 43.05/43.21 ( organization(X)
% 43.05/43.21 => ( ( greater(external_ties(X,T),external_ties(X,T0))
% 43.05/43.21 => greater(position(X,T),position(X,T0)) )
% 43.05/43.21 & ( external_ties(X,T) = external_ties(X,T0)
% 43.05/43.21 => position(X,T) = position(X,T0) ) ) ) ).
% 43.05/43.21
% 43.05/43.21 %----Case: liability of senescence (Ass. 10-12 replacing A7-9)!
% 43.05/43.21 %----
% 43.05/43.21 %----An organization's stock of knowledge does not vary with its age
% 43.05/43.21 %----(contra assumption 7).
% 43.05/43.21 fof(assumption_10,axiom,
% 43.05/43.21 ! [X,T0,T] :
% 43.05/43.21 ( organization(X)
% 43.05/43.21 => stock_of_knowledge(X,T) = stock_of_knowledge(X,T0) ) ).
% 43.05/43.21
% 43.05/43.21 %----The quality of an organization's external ties does not vary with
% 43.05/43.21 %----its age (contra assumption 8).
% 43.05/43.21 fof(assumption_11,axiom,
% 43.05/43.21 ! [X,T0,T] :
% 43.05/43.21 ( organization(X)
% 43.05/43.21 => external_ties(X,T) = external_ties(X,T0) ) ).
% 43.05/43.21
% 43.05/43.21 %----The quality of an organization's internal friction increases
% 43.05/43.21 %----monotonically with its age (contra assumption 9).
% 43.05/43.21 fof(assumption_12,axiom,
% 43.05/43.21 ! [X,T0,T] :
% 43.05/43.21 ( ( organization(X)
% 43.05/43.21 & greater(age(X,T),age(X,T0)) )
% 43.05/43.21 => greater(internal_friction(X,T),internal_friction(X,T0)) ) ).
% 43.05/43.21
% 43.05/43.21 %----Problem theorems
% 43.05/43.21 %----The senescence theorem for unendowed organizations (Barron et
% 43.05/43.21 %----al. 1994): an unendowed organization's hazard of mortality
% 43.05/43.21 %----increases with its age.
% 43.05/43.21 %----From A1, A4-6, and A10-12 (text says D1, A1-4, L5-6; also needs D<,
% 43.05/43.21 %----D<=, D>=).
% 43.05/43.21 fof(theorem_3,conjecture,
% 43.05/43.21 ! [X,T0,T] :
% 43.05/43.21 ( ( organization(X)
% 43.05/43.21 & ~ has_endowment(X)
% 43.05/43.21 & greater(age(X,T),age(X,T0)) )
% 43.05/43.21 => greater(hazard_of_mortality(X,T),hazard_of_mortality(X,T0)) ) ).
% 43.05/43.21
% 43.05/43.21 %--------------------------------------------------------------------------
% 43.05/43.21 %-------------------------------------------
% 43.05/43.21 % Proof found
% 43.05/43.21 % SZS status Theorem for theBenchmark
% 43.05/43.21 % SZS output start Proof
% 43.05/43.21 %ClaNum:64(EqnAxiom:35)
% 43.05/43.21 %VarNum:195(SingletonVarNum:64)
% 43.05/43.21 %MaxLitNum:4
% 43.05/43.21 %MaxfuncDepth:1
% 43.05/43.21 %SharedTerms:11
% 43.05/43.21 %goalClause: 36 37 38 39
% 43.05/43.21 %singleGoalClaCount:4
% 43.05/43.21 [36]P1(a1)
% 43.05/43.21 [38]~P5(a1)
% 43.05/43.21 [37]P2(f2(a1,a4),f2(a1,a5))
% 43.05/43.21 [39]~P2(f6(a1,a4),f6(a1,a5))
% 43.05/43.21 [40]~E(x401,x402)+P8(x401,x402)
% 43.05/43.21 [41]~E(x411,x412)+P6(x411,x412)
% 43.05/43.21 [46]~P9(x461,x462)+P8(x461,x462)
% 43.05/43.21 [47]~P2(x472,x471)+P9(x471,x472)
% 43.05/43.21 [48]~P2(x481,x482)+P6(x481,x482)
% 43.05/43.21 [49]~P9(x492,x491)+P2(x491,x492)
% 43.05/43.21 [52]~P2(x522,x521)+~P2(x521,x522)
% 43.05/43.21 [54]~P1(x541)+P3(x541,x542,x543)
% 43.05/43.21 [44]~P1(x441)+E(f8(x441,x442),f8(x441,x443))
% 43.05/43.21 [45]~P1(x451)+E(f7(x451,x452),f7(x451,x453))
% 43.05/43.21 [42]P9(x421,x422)+P2(x421,x422)+E(x421,x422)
% 43.05/43.21 [43]~P1(x431)+P5(x431)+~P7(x431,x432)
% 43.05/43.21 [50]P9(x501,x502)+~P8(x501,x502)+E(x501,x502)
% 43.05/43.21 [51]P2(x511,x512)+~P6(x511,x512)+E(x511,x512)
% 43.05/43.21 [53]~P2(x531,x533)+P2(x531,x532)+~P2(x533,x532)
% 43.05/43.21 [55]~P1(x551)+~E(f7(x551,x552),f7(x551,x553))+E(f9(x551,x552),f9(x551,x553))
% 43.05/43.21 [57]~P1(x571)+~P2(f7(x571,x572),f7(x571,x573))+P2(f9(x571,x572),f9(x571,x573))
% 43.05/43.21 [58]~P1(x581)+~P2(f2(x581,x582),f2(x581,x583))+P2(f10(x581,x582),f10(x581,x583))
% 43.05/43.21 [56]P4(x561,x562,x563)+~P1(x561)+P7(x561,x562)+P7(x561,x563)
% 43.05/43.21 [59]~P3(x591,x592,x593)+~E(f8(x591,x592),f8(x591,x593))+~E(f10(x591,x592),f10(x591,x593))+E(f3(x591,x592),f3(x591,x593))
% 43.05/43.21 [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))
% 43.05/43.21 [61]~P3(x611,x612,x613)+~P8(f8(x611,x612),f8(x611,x613))+~P2(f10(x611,x612),f10(x611,x613))+P9(f3(x611,x612),f3(x611,x613))
% 43.05/43.21 [62]~P4(x621,x622,x623)+~P6(f3(x621,x622),f3(x621,x623))+~P2(f9(x621,x622),f9(x621,x623))+P9(f6(x621,x622),f6(x621,x623))
% 43.05/43.21 [63]~P4(x631,x632,x633)+~P6(f9(x631,x632),f9(x631,x633))+~P2(f3(x631,x632),f3(x631,x633))+P9(f6(x631,x632),f6(x631,x633))
% 43.05/43.21 [64]~P3(x641,x642,x643)+~P8(f10(x641,x642),f10(x641,x643))+~P2(f8(x641,x642),f8(x641,x643))+P2(f3(x641,x642),f3(x641,x643))
% 43.05/43.21 %EqnAxiom
% 43.05/43.21 [1]E(x11,x11)
% 43.05/43.21 [2]E(x22,x21)+~E(x21,x22)
% 43.05/43.21 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 43.05/43.21 [4]~E(x41,x42)+E(f2(x41,x43),f2(x42,x43))
% 43.05/43.21 [5]~E(x51,x52)+E(f2(x53,x51),f2(x53,x52))
% 43.05/43.21 [6]~E(x61,x62)+E(f8(x61,x63),f8(x62,x63))
% 43.05/43.21 [7]~E(x71,x72)+E(f8(x73,x71),f8(x73,x72))
% 43.05/43.21 [8]~E(x81,x82)+E(f6(x81,x83),f6(x82,x83))
% 43.05/43.21 [9]~E(x91,x92)+E(f6(x93,x91),f6(x93,x92))
% 43.05/43.21 [10]~E(x101,x102)+E(f9(x101,x103),f9(x102,x103))
% 43.05/43.21 [11]~E(x111,x112)+E(f9(x113,x111),f9(x113,x112))
% 43.05/43.21 [12]~E(x121,x122)+E(f10(x121,x123),f10(x122,x123))
% 43.05/43.21 [13]~E(x131,x132)+E(f10(x133,x131),f10(x133,x132))
% 43.05/43.21 [14]~E(x141,x142)+E(f3(x141,x143),f3(x142,x143))
% 43.05/43.21 [15]~E(x151,x152)+E(f3(x153,x151),f3(x153,x152))
% 43.05/43.21 [16]~E(x161,x162)+E(f7(x161,x163),f7(x162,x163))
% 43.05/43.21 [17]~E(x171,x172)+E(f7(x173,x171),f7(x173,x172))
% 43.05/43.21 [18]~P1(x181)+P1(x182)+~E(x181,x182)
% 43.05/43.21 [19]P2(x192,x193)+~E(x191,x192)+~P2(x191,x193)
% 43.05/43.21 [20]P2(x203,x202)+~E(x201,x202)+~P2(x203,x201)
% 43.05/43.21 [21]~P5(x211)+P5(x212)+~E(x211,x212)
% 43.05/43.21 [22]P6(x222,x223)+~E(x221,x222)+~P6(x221,x223)
% 43.05/43.21 [23]P6(x233,x232)+~E(x231,x232)+~P6(x233,x231)
% 43.05/43.21 [24]P8(x242,x243)+~E(x241,x242)+~P8(x241,x243)
% 43.05/43.21 [25]P8(x253,x252)+~E(x251,x252)+~P8(x253,x251)
% 43.05/43.21 [26]P7(x262,x263)+~E(x261,x262)+~P7(x261,x263)
% 43.05/43.21 [27]P7(x273,x272)+~E(x271,x272)+~P7(x273,x271)
% 43.05/43.21 [28]P9(x282,x283)+~E(x281,x282)+~P9(x281,x283)
% 43.05/43.21 [29]P9(x293,x292)+~E(x291,x292)+~P9(x293,x291)
% 43.05/43.21 [30]P4(x302,x303,x304)+~E(x301,x302)+~P4(x301,x303,x304)
% 43.05/43.21 [31]P4(x313,x312,x314)+~E(x311,x312)+~P4(x313,x311,x314)
% 43.05/43.21 [32]P4(x323,x324,x322)+~E(x321,x322)+~P4(x323,x324,x321)
% 43.05/43.21 [33]P3(x332,x333,x334)+~E(x331,x332)+~P3(x331,x333,x334)
% 43.05/43.21 [34]P3(x343,x342,x344)+~E(x341,x342)+~P3(x343,x341,x344)
% 43.05/43.21 [35]P3(x353,x354,x352)+~E(x351,x352)+~P3(x353,x354,x351)
% 43.05/43.21
% 43.05/43.21 %-------------------------------------------
% 43.05/43.21 cnf(65,plain,
% 43.05/43.21 (P8(x651,x651)),
% 43.05/43.21 inference(equality_inference,[],[40])).
% 43.05/43.21 cnf(66,plain,
% 43.05/43.21 (P6(x661,x661)),
% 43.05/43.21 inference(equality_inference,[],[41])).
% 43.05/43.21 cnf(68,plain,
% 43.05/43.21 (P3(a1,x681,x682)),
% 43.05/43.21 inference(scs_inference,[],[36,54])).
% 43.05/43.21 cnf(70,plain,
% 43.05/43.21 (~P9(f6(a1,a5),f6(a1,a4))),
% 43.05/43.21 inference(scs_inference,[],[36,39,54,49])).
% 43.05/43.21 cnf(74,plain,
% 43.05/43.22 (~P7(a1,x741)),
% 43.05/43.22 inference(scs_inference,[],[36,38,37,39,54,49,52,43])).
% 43.05/43.22 cnf(76,plain,
% 43.05/43.22 (P4(a1,x761,x761)),
% 43.05/43.22 inference(scs_inference,[],[36,38,37,39,54,49,52,43,56])).
% 43.05/43.22 cnf(124,plain,
% 43.05/43.22 (P6(x1241,x1242)+~E(x1242,x1241)),
% 43.05/43.22 inference(scs_inference,[],[37,76,66,31,20,19,22])).
% 43.05/43.22 cnf(133,plain,
% 43.05/43.22 (P8(x1331,x1332)+~E(x1332,x1331)),
% 43.05/43.22 inference(scs_inference,[],[65,24])).
% 43.05/43.22 cnf(176,plain,
% 43.05/43.22 (~E(a1,x1761)+E(f8(x1761,x1762),f8(x1761,x1763))),
% 43.05/43.22 inference(scs_inference,[],[36,44,18])).
% 43.05/43.22 cnf(177,plain,
% 43.05/43.22 (E(f8(a1,x1771),f8(a1,x1772))),
% 43.05/43.22 inference(equality_inference,[],[176])).
% 43.05/43.22 cnf(179,plain,
% 43.05/43.22 (P8(f8(a1,x1791),f8(a1,x1792))),
% 43.05/43.22 inference(scs_inference,[],[177,124,133])).
% 43.05/43.22 cnf(180,plain,
% 43.05/43.22 (P4(a1,f8(a1,x1801),f8(a1,x1802))),
% 43.05/43.22 inference(scs_inference,[],[76,177,124,133,31])).
% 43.05/43.22 cnf(214,plain,
% 43.05/43.22 (~P2(f10(a1,x2141),f10(a1,x2142))+P9(f3(a1,x2141),f3(a1,x2142))),
% 43.05/43.22 inference(scs_inference,[],[68,179,180,30,61])).
% 43.05/43.22 cnf(278,plain,
% 43.05/43.22 (P8(f3(a1,x2781),f3(a1,x2782))+~P2(f10(a1,x2781),f10(a1,x2782))),
% 43.05/43.22 inference(scs_inference,[],[214,46])).
% 43.05/43.22 cnf(308,plain,
% 43.05/43.22 (P8(f3(a1,a4),f3(a1,a5))),
% 43.05/43.22 inference(scs_inference,[],[37,36,278,58])).
% 43.05/43.22 cnf(309,plain,
% 43.05/43.22 (E(f3(a1,a4),f3(a1,a5))+P9(f3(a1,a4),f3(a1,a5))),
% 43.05/43.22 inference(scs_inference,[],[308,50])).
% 43.05/43.22 cnf(327,plain,
% 43.05/43.22 (P2(f3(a1,a5),f3(a1,a4))+E(f3(a1,a4),f3(a1,a5))),
% 43.05/43.22 inference(scs_inference,[],[309,49])).
% 43.05/43.22 cnf(401,plain,
% 43.05/43.22 (E(f7(a1,x4011),f7(a1,x4012))),
% 43.05/43.22 inference(scs_inference,[],[36,2,45])).
% 43.05/43.22 cnf(436,plain,
% 43.05/43.22 (E(f9(a1,x4361),f9(a1,x4362))),
% 43.05/43.22 inference(scs_inference,[],[401,36,2,55])).
% 43.05/43.22 cnf(437,plain,
% 43.05/43.22 (P6(f9(a1,x4371),f9(a1,x4372))),
% 43.05/43.22 inference(scs_inference,[],[436,124])).
% 43.05/43.22 cnf(479,plain,
% 43.05/43.22 (E(f3(a1,a5),f3(a1,a4))+~P4(a1,a5,a4)),
% 43.05/43.22 inference(scs_inference,[],[70,437,63,327,49,124,133,2])).
% 43.05/43.22 cnf(517,plain,
% 43.05/43.22 (P7(a1,a4)+E(f3(a1,a5),f3(a1,a4))),
% 43.05/43.22 inference(scs_inference,[],[36,74,479,56])).
% 43.05/43.22 cnf(518,plain,
% 43.05/43.22 (E(f3(a1,a5),f3(a1,a4))),
% 43.05/43.22 inference(scs_inference,[],[74,517])).
% 43.05/43.22 cnf(520,plain,
% 43.05/43.22 (E(f3(a1,a4),f3(a1,a5))),
% 43.05/43.22 inference(scs_inference,[],[74,517,2])).
% 43.05/43.22 cnf(588,plain,
% 43.05/43.22 (~P4(a1,a5,a4)+E(f6(a1,a5),f6(a1,a4))),
% 43.05/43.22 inference(scs_inference,[],[436,518,60])).
% 43.05/43.22 cnf(776,plain,
% 43.05/43.22 (E(f6(a1,a5),f6(a1,a4))+P7(a1,a4)),
% 43.05/43.22 inference(scs_inference,[],[36,74,588,56])).
% 43.05/43.22 cnf(777,plain,
% 43.05/43.22 (E(f6(a1,a5),f6(a1,a4))),
% 43.05/43.22 inference(scs_inference,[],[74,776])).
% 43.05/43.22 cnf(2670,plain,
% 43.05/43.22 (~P9(f10(a1,x26701),f10(a1,x26702))+~P2(f8(a1,x26701),f8(a1,x26702))+P2(f3(a1,x26701),f3(a1,x26702))),
% 43.05/43.22 inference(scs_inference,[],[68,46,64])).
% 43.05/43.22 cnf(2686,plain,
% 43.05/43.22 (~P9(f8(a1,x26861),f8(a1,x26862))+P2(f3(a1,x26862),f3(a1,x26861))+~P9(f10(a1,x26862),f10(a1,x26861))),
% 43.05/43.22 inference(scs_inference,[],[2670,49])).
% 43.05/43.22 cnf(2939,plain,
% 43.05/43.22 (~P2(f6(a1,a5),f6(a1,a5))),
% 43.05/43.22 inference(scs_inference,[],[70,777,47,19])).
% 43.05/43.22 cnf(2942,plain,
% 43.05/43.22 (~P2(f3(a1,a5),f3(a1,a5))),
% 43.05/43.22 inference(scs_inference,[],[76,66,2939,49,63])).
% 43.05/43.22 cnf(2961,plain,
% 43.05/43.22 (~P9(f3(a1,a5),f3(a1,a5))),
% 43.05/43.22 inference(scs_inference,[],[2942,49])).
% 43.05/43.22 cnf(3742,plain,
% 43.05/43.22 (P6(f10(a1,a4),f10(a1,a5))),
% 43.05/43.22 inference(scs_inference,[],[37,36,48,58])).
% 43.05/43.22 cnf(3746,plain,
% 43.05/43.22 (E(f10(a1,a5),f10(a1,a4))+P2(f10(a1,a4),f10(a1,a5))),
% 43.05/43.22 inference(scs_inference,[],[3742,51,133,2])).
% 43.05/43.22 cnf(3813,plain,
% 43.05/43.22 (E(f10(a1,a5),f10(a1,a4))+P9(f3(a1,a4),f3(a1,a5))),
% 43.05/43.22 inference(scs_inference,[],[3746,214])).
% 43.05/43.22 cnf(3878,plain,
% 43.05/43.22 (E(f10(a1,a5),f10(a1,a4))),
% 43.05/43.22 inference(scs_inference,[],[2961,520,3813,28])).
% 43.05/43.22 cnf(3879,plain,
% 43.05/43.22 (E(f10(a1,a4),f10(a1,a5))),
% 43.05/43.22 inference(scs_inference,[],[3878,2])).
% 43.05/43.22 cnf(3896,plain,
% 43.05/43.22 (P8(f10(a1,a5),f10(a1,a4))),
% 43.05/43.22 inference(scs_inference,[],[3879,133])).
% 43.05/43.22 cnf(4096,plain,
% 43.05/43.22 (~P2(f10(a1,a4),f10(a1,a5))),
% 43.05/43.22 inference(scs_inference,[],[68,520,3896,2942,20,64,49,2686,214])).
% 43.05/43.22 cnf(4103,plain,
% 43.05/43.22 ($false),
% 43.05/43.22 inference(scs_inference,[],[37,36,4096,49,58]),
% 43.05/43.22 ['proof']).
% 43.05/43.22 % SZS output end Proof
% 43.05/43.22 % Total time :42.712473s
%------------------------------------------------------------------------------