%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : MGT042+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 : n009.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 6.34s 6.51s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : MGT042+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.06/0.32 % Computer : n009.cluster.edu
% 0.06/0.32 % Model : x86_64 x86_64
% 0.06/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.06/0.32 % Memory : 8046.5625MB
% 0.06/0.32 % OS : Linux 6.8.0-71-generic
% 0.06/0.32 % CPULimit : 300
% 0.06/0.32 % WCLimit : 300
% 0.06/0.32 % DateTime : Mon Sep 7 13:03:52 UTC 2026
% 0.06/0.32 % CPUTime :
% 0.25/0.48 start to proof:theBenchmark
% 6.34/6.50 %-------------------------------------------
% 6.34/6.50 % File :CSE---1.7
% 6.34/6.50 % Problem :theBenchmark
% 6.34/6.50 % Transform :cnf
% 6.34/6.50 % Format :tptp:raw
% 6.34/6.50 % Command :java -jar mcs_scs.jar %d %s
% 6.34/6.50
% 6.34/6.50 % Result :Theorem 6.020284s
% 6.34/6.50 % Output :CNFRefutation 6.020284s
% 6.34/6.50 %-------------------------------------------
% 6.34/6.50 %--------------------------------------------------------------------------
% 6.34/6.50 % File : MGT042+1 : TPTP v9.3.0. Released v2.4.0.
% 6.34/6.50 % Domain : Management (Organisation Theory)
% 6.34/6.50 % Problem : Conditions for a lower hazard of mortality
% 6.34/6.50 % Version : [Han98] axioms.
% 6.34/6.50 % English : When an organization lacks immunity, increased collective
% 6.34/6.50 % knowledge and superior external ties lower its hazard of
% 6.34/6.50 % mortality when internal friction does not increase.
% 6.34/6.50
% 6.34/6.50 % Refs : [Kam00] Kamps (2000), Email to G. Sutcliffe
% 6.34/6.50 % : [CH00] Carroll & Hannan (2000), The Demography of Corporation
% 6.34/6.50 % : [Han98] Hannan (1998), Rethinking Age Dependence in Organizati
% 6.34/6.50 % Source : [Kam00]
% 6.34/6.50 % Names : LEMMA 1 [Han98]
% 6.34/6.50
% 6.34/6.50 % Status : Theorem
% 6.34/6.50 % Rating : 0.17 v9.3.0, 0.24 v9.1.0, 0.18 v9.0.0, 0.28 v8.2.0, 0.22 v8.1.0, 0.19 v7.5.0, 0.22 v7.4.0, 0.20 v7.3.0, 0.24 v7.2.0, 0.21 v7.1.0, 0.17 v7.0.0, 0.27 v6.4.0, 0.31 v6.3.0, 0.29 v6.2.0, 0.32 v6.1.0, 0.40 v6.0.0, 0.26 v5.5.0, 0.37 v5.4.0, 0.43 v5.3.0, 0.56 v5.2.0, 0.45 v5.1.0, 0.43 v5.0.0, 0.42 v4.1.0, 0.35 v4.0.1, 0.30 v4.0.0, 0.29 v3.7.0, 0.30 v3.5.0, 0.26 v3.4.0, 0.47 v3.3.0, 0.50 v3.2.0, 0.64 v3.1.0, 0.78 v2.7.0, 0.67 v2.6.0, 0.83 v2.4.0
% 6.34/6.50 % Syntax : Number of formulae : 10 ( 0 unt; 0 def)
% 6.34/6.50 % Number of atoms : 54 ( 11 equ)
% 6.34/6.50 % Maximal formula atoms : 12 ( 5 avg)
% 6.34/6.50 % Number of connectives : 49 ( 5 ~; 4 |; 22 &)
% 6.34/6.50 % ( 3 <=>; 15 =>; 0 <=; 0 <~>)
% 6.34/6.50 % Maximal formula depth : 9 ( 6 avg)
% 6.34/6.50 % Maximal term depth : 2 ( 1 avg)
% 6.34/6.50 % Number of predicates : 7 ( 6 usr; 0 prp; 1-2 aty)
% 6.34/6.50 % Number of functors : 6 ( 6 usr; 0 con; 2-2 aty)
% 6.34/6.50 % Number of variables : 25 ( 25 !; 0 ?)
% 6.34/6.51 % SPC : FOF_THM_RFO_SEQ
% 6.34/6.51
% 6.34/6.51 % Comments : The original text uses mnemonic names:
% 6.34/6.51 % Original: C/F/P: Arity: New name:
% 6.34/6.51 % zero-symbol c 0 zero
% 6.34/6.51 % eta-symbol c 0 eta
% 6.34/6.51 % sigma-symbol c 0 sigma
% 6.34/6.51 % tau-symbol c 0 tau
% 6.34/6.51 % very_low c 0 very_low
% 6.34/6.51 % low c 0 low
% 6.34/6.51 % mod1 c 0 mod1
% 6.34/6.51 % mod2 c 0 mod2
% 6.34/6.51 % high c 0 high
% 6.34/6.51 % A f 2 age
% 6.34/6.51 % H f 2 hazard_of_mortality
% 6.34/6.51 % C f 2 capability
% 6.34/6.51 % P f 2 position
% 6.34/6.51 % K f 2 stock_of_knowledge
% 6.34/6.51 % T f 2 external_ties
% 6.34/6.51 % F f 2 internal_friction
% 6.34/6.51 % O p 1 organization
% 6.34/6.51 % EN p 1 has_endowment
% 6.34/6.51 % IM p 2 has_immunity
% 6.34/6.51 % DS p 3 dissimilar
% 6.34/6.51 % AL p 2 is_aligned
% 6.34/6.51 % PA p 2 positional_advantage
% 6.34/6.51 % FG p 1 fragile_position
% 6.34/6.51 % RB p 1 robust_position
% 6.34/6.51 %--------------------------------------------------------------------------
% 6.34/6.51 include('Axioms/MGT001+0.ax').
% 6.34/6.51 %--------------------------------------------------------------------------
% 6.34/6.51 %----Problem Axioms
% 6.34/6.51 %----When an organization lacks immunity, superior capability and
% 6.34/6.51 %----position imply a lower hazard of mortality.
% 6.34/6.51 fof(assumption_4,axiom,
% 6.34/6.51 ! [X,T0,T] :
% 6.34/6.51 ( ( organization(X)
% 6.34/6.51 & ~ has_immunity(X,T0)
% 6.34/6.51 & ~ has_immunity(X,T) )
% 6.34/6.51 => ( ( ( greater(capability(X,T),capability(X,T0))
% 6.34/6.51 & greater_or_equal(position(X,T),position(X,T0)) )
% 6.34/6.51 => smaller(hazard_of_mortality(X,T),hazard_of_mortality(X,T0)) )
% 6.34/6.51 & ( ( greater_or_equal(capability(X,T),capability(X,T0))
% 6.34/6.51 & greater(position(X,T),position(X,T0)) )
% 6.34/6.51 => smaller(hazard_of_mortality(X,T),hazard_of_mortality(X,T0)) )
% 6.34/6.51 & ( ( capability(X,T) = capability(X,T0)
% 6.34/6.51 & position(X,T) = position(X,T0) )
% 6.34/6.51 => hazard_of_mortality(X,T) = hazard_of_mortality(X,T0) ) ) ) ).
% 6.34/6.51
% 6.34/6.51 %----Increased knowledge elevates an organization's capability; and
% 6.34/6.51 %----increased accumulation of organizational internal frictions
% 6.34/6.51 %----diminishes its capability.
% 6.34/6.51 fof(assumption_5,axiom,
% 6.34/6.51 ! [X,T0,T] :
% 6.34/6.51 ( organization(X)
% 6.34/6.51 => ( ( ( greater(stock_of_knowledge(X,T),stock_of_knowledge(X,T0))
% 6.34/6.51 & smaller_or_equal(internal_friction(X,T),internal_friction(X,T0)) )
% 6.34/6.51 => greater(capability(X,T),capability(X,T0)) )
% 6.34/6.51 & ( ( smaller_or_equal(stock_of_knowledge(X,T),stock_of_knowledge(X,T0))
% 6.34/6.51 & greater(internal_friction(X,T),internal_friction(X,T0)) )
% 6.34/6.51 => smaller(capability(X,T),capability(X,T0)) )
% 6.34/6.51 & ( ( stock_of_knowledge(X,T) = stock_of_knowledge(X,T0)
% 6.34/6.51 & internal_friction(X,T) = internal_friction(X,T0) )
% 6.34/6.51 => capability(X,T) = capability(X,T0) ) ) ) ).
% 6.34/6.51
% 6.34/6.51 %----Improved ties with external actors enhance an organization's position.
% 6.34/6.51 fof(assumption_6,axiom,
% 6.34/6.51 ! [X,T0,T] :
% 6.34/6.51 ( organization(X)
% 6.34/6.51 => ( ( greater(external_ties(X,T),external_ties(X,T0))
% 6.34/6.51 => greater(position(X,T),position(X,T0)) )
% 6.34/6.51 & ( external_ties(X,T) = external_ties(X,T0)
% 6.34/6.51 => position(X,T) = position(X,T0) ) ) ) ).
% 6.34/6.51
% 6.34/6.51 %----Problem theorems
% 6.34/6.51 %----When an organization lacks immunity, increased collective
% 6.34/6.51 %----knowledge and superior external ties lower its hazard of
% 6.34/6.51 %----mortality when internal friction does not increase.
% 6.34/6.51 %----From A4, A5, and A6 (text says A1-6; also needs D<, D>=, D<=).
% 6.34/6.51 fof(lemma_1,conjecture,
% 6.34/6.51 ! [X,T0,T] :
% 6.34/6.51 ( ( organization(X)
% 6.34/6.51 & ~ has_immunity(X,T0)
% 6.34/6.51 & ~ has_immunity(X,T) )
% 6.34/6.51 => ( ( ( greater(stock_of_knowledge(X,T),stock_of_knowledge(X,T0))
% 6.34/6.51 & smaller_or_equal(internal_friction(X,T),internal_friction(X,T0))
% 6.34/6.51 & greater_or_equal(external_ties(X,T),external_ties(X,T0)) )
% 6.34/6.51 => smaller(hazard_of_mortality(X,T),hazard_of_mortality(X,T0)) )
% 6.34/6.51 & ( ( greater_or_equal(stock_of_knowledge(X,T),stock_of_knowledge(X,T0))
% 6.34/6.51 & smaller_or_equal(internal_friction(X,T),internal_friction(X,T0))
% 6.34/6.51 & greater(external_ties(X,T),external_ties(X,T0)) )
% 6.34/6.51 => smaller(hazard_of_mortality(X,T),hazard_of_mortality(X,T0)) ) ) ) ).
% 6.34/6.51
% 6.34/6.51 %--------------------------------------------------------------------------
% 6.34/6.51 %-------------------------------------------
% 6.34/6.51 % Proof found
% 6.34/6.51 % SZS status Theorem for theBenchmark
% 6.34/6.51 % SZS output start Proof
% 6.34/6.51 %ClaNum:72(EqnAxiom:32)
% 6.34/6.51 %VarNum:172(SingletonVarNum:53)
% 6.34/6.51 %MaxLitNum:4
% 6.34/6.51 %MaxfuncDepth:1
% 6.34/6.51 %SharedTerms:20
% 6.34/6.51 %goalClause: 33 34 35 36 37 56 57 58 59
% 6.34/6.51 %singleGoalClaCount:5
% 6.34/6.51 [33]P1(a1)
% 6.34/6.51 [35]~P2(a1,a4)
% 6.34/6.51 [36]~P2(a1,a3)
% 6.34/6.51 [34]P7(f5(a1,a3),f5(a1,a4))
% 6.34/6.51 [37]~P8(f6(a1,a3),f6(a1,a4))
% 6.34/6.51 [56]P3(f9(a1,a3),f9(a1,a4))+P3(f7(a1,a3),f7(a1,a4))
% 6.34/6.51 [57]P4(f9(a1,a3),f9(a1,a4))+P3(f9(a1,a3),f9(a1,a4))
% 6.34/6.51 [58]P4(f7(a1,a3),f7(a1,a4))+P3(f7(a1,a3),f7(a1,a4))
% 6.34/6.51 [59]P4(f9(a1,a3),f9(a1,a4))+P4(f7(a1,a3),f7(a1,a4))
% 6.34/6.51 [38]~E(x381,x382)+P7(x381,x382)
% 6.34/6.51 [39]~E(x391,x392)+P3(x391,x392)
% 6.34/6.51 [41]~P8(x411,x412)+P7(x411,x412)
% 6.34/6.51 [42]~P4(x422,x421)+P8(x421,x422)
% 6.34/6.51 [43]~P4(x431,x432)+P3(x431,x432)
% 6.34/6.51 [44]~P8(x442,x441)+P4(x441,x442)
% 6.34/6.51 [47]~P4(x472,x471)+~P4(x471,x472)
% 6.34/6.51 [49]~P1(x491)+P5(x491,x492,x493)
% 6.34/6.51 [40]P8(x401,x402)+P4(x401,x402)+E(x401,x402)
% 6.34/6.51 [45]P8(x451,x452)+~P7(x451,x452)+E(x451,x452)
% 6.34/6.51 [46]P4(x461,x462)+~P3(x461,x462)+E(x461,x462)
% 6.34/6.51 [48]~P4(x481,x483)+P4(x481,x482)+~P4(x483,x482)
% 6.34/6.51 [50]~P1(x501)+~E(f7(x501,x502),f7(x501,x503))+E(f8(x501,x502),f8(x501,x503))
% 6.34/6.51 [66]~P1(x661)+~P4(f7(x661,x662),f7(x661,x663))+P4(f8(x661,x662),f8(x661,x663))
% 6.34/6.51 [51]P6(x511,x513,x512)+~P1(x511)+P2(x511,x512)+P2(x511,x513)
% 6.34/6.51 [67]~P5(x671,x673,x672)+~E(f9(x671,x672),f9(x671,x673))+~E(f5(x671,x672),f5(x671,x673))+E(f2(x671,x672),f2(x671,x673))
% 6.34/6.51 [68]~P6(x681,x683,x682)+~E(f2(x681,x682),f2(x681,x683))+~E(f8(x681,x682),f8(x681,x683))+E(f6(x681,x682),f6(x681,x683))
% 6.34/6.51 [69]~P5(x691,x693,x692)+~P7(f9(x691,x692),f9(x691,x693))+~P4(f5(x691,x692),f5(x691,x693))+P8(f2(x691,x692),f2(x691,x693))
% 6.34/6.51 [70]~P6(x701,x703,x702)+~P3(f2(x701,x702),f2(x701,x703))+~P4(f8(x701,x702),f8(x701,x703))+P8(f6(x701,x702),f6(x701,x703))
% 6.34/6.51 [71]~P6(x711,x713,x712)+~P3(f8(x711,x712),f8(x711,x713))+~P4(f2(x711,x712),f2(x711,x713))+P8(f6(x711,x712),f6(x711,x713))
% 6.34/6.51 [72]~P5(x721,x723,x722)+~P7(f5(x721,x722),f5(x721,x723))+~P4(f9(x721,x722),f9(x721,x723))+P4(f2(x721,x722),f2(x721,x723))
% 6.34/6.51 %EqnAxiom
% 6.34/6.51 [1]E(x11,x11)
% 6.34/6.51 [2]E(x22,x21)+~E(x21,x22)
% 6.34/6.51 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 6.34/6.51 [4]~E(x41,x42)+E(f5(x41,x43),f5(x42,x43))
% 6.34/6.51 [5]~E(x51,x52)+E(f5(x53,x51),f5(x53,x52))
% 6.34/6.51 [6]~E(x61,x62)+E(f9(x61,x63),f9(x62,x63))
% 6.34/6.51 [7]~E(x71,x72)+E(f9(x73,x71),f9(x73,x72))
% 6.34/6.51 [8]~E(x81,x82)+E(f6(x81,x83),f6(x82,x83))
% 6.34/6.51 [9]~E(x91,x92)+E(f6(x93,x91),f6(x93,x92))
% 6.34/6.51 [10]~E(x101,x102)+E(f7(x101,x103),f7(x102,x103))
% 6.34/6.51 [11]~E(x111,x112)+E(f7(x113,x111),f7(x113,x112))
% 6.34/6.51 [12]~E(x121,x122)+E(f8(x121,x123),f8(x122,x123))
% 6.34/6.51 [13]~E(x131,x132)+E(f8(x133,x131),f8(x133,x132))
% 6.34/6.51 [14]~E(x141,x142)+E(f2(x141,x143),f2(x142,x143))
% 6.34/6.51 [15]~E(x151,x152)+E(f2(x153,x151),f2(x153,x152))
% 6.34/6.51 [16]~P1(x161)+P1(x162)+~E(x161,x162)
% 6.34/6.51 [17]P7(x172,x173)+~E(x171,x172)+~P7(x171,x173)
% 6.34/6.51 [18]P7(x183,x182)+~E(x181,x182)+~P7(x183,x181)
% 6.34/6.51 [19]P2(x192,x193)+~E(x191,x192)+~P2(x191,x193)
% 6.34/6.51 [20]P2(x203,x202)+~E(x201,x202)+~P2(x203,x201)
% 6.34/6.51 [21]P8(x212,x213)+~E(x211,x212)+~P8(x211,x213)
% 6.34/6.51 [22]P8(x223,x222)+~E(x221,x222)+~P8(x223,x221)
% 6.34/6.51 [23]P4(x232,x233)+~E(x231,x232)+~P4(x231,x233)
% 6.34/6.51 [24]P4(x243,x242)+~E(x241,x242)+~P4(x243,x241)
% 6.34/6.51 [25]P3(x252,x253)+~E(x251,x252)+~P3(x251,x253)
% 6.34/6.51 [26]P3(x263,x262)+~E(x261,x262)+~P3(x263,x261)
% 6.34/6.51 [27]P5(x272,x273,x274)+~E(x271,x272)+~P5(x271,x273,x274)
% 6.34/6.51 [28]P5(x283,x282,x284)+~E(x281,x282)+~P5(x283,x281,x284)
% 6.34/6.51 [29]P5(x293,x294,x292)+~E(x291,x292)+~P5(x293,x294,x291)
% 6.34/6.51 [30]P6(x302,x303,x304)+~E(x301,x302)+~P6(x301,x303,x304)
% 6.34/6.51 [31]P6(x313,x312,x314)+~E(x311,x312)+~P6(x313,x311,x314)
% 6.34/6.51 [32]P6(x323,x324,x322)+~E(x321,x322)+~P6(x323,x324,x321)
% 6.34/6.51
% 6.34/6.51 %-------------------------------------------
% 6.34/6.51 cnf(73,plain,
% 6.34/6.51 (P7(x731,x731)),
% 6.34/6.51 inference(equality_inference,[],[38])).
% 6.34/6.51 cnf(74,plain,
% 6.34/6.51 (P3(x741,x741)),
% 6.34/6.51 inference(equality_inference,[],[39])).
% 6.34/6.51 cnf(76,plain,
% 6.34/6.51 (P5(a1,x761,x762)),
% 6.34/6.51 inference(scs_inference,[],[33,49])).
% 6.34/6.52 cnf(78,plain,
% 6.34/6.52 (~P4(f6(a1,a4),f6(a1,a3))),
% 6.34/6.52 inference(scs_inference,[],[33,37,49,42])).
% 6.34/6.52 cnf(80,plain,
% 6.34/6.52 (P6(a1,a4,a4)),
% 6.34/6.52 inference(scs_inference,[],[33,35,37,49,42,51])).
% 6.34/6.52 cnf(82,plain,
% 6.34/6.52 (E(f5(a1,a3),f5(a1,a4))+P8(f5(a1,a3),f5(a1,a4))),
% 6.34/6.52 inference(scs_inference,[],[33,35,34,37,49,42,51,45])).
% 6.34/6.52 cnf(87,plain,
% 6.34/6.52 (P3(x871,x871)),
% 6.34/6.52 inference(rename_variables,[],[74])).
% 6.34/6.52 cnf(90,plain,
% 6.34/6.52 (E(f5(a1,a4),f5(a1,a3))+P8(f5(a1,a3),f5(a1,a4))),
% 6.34/6.52 inference(scs_inference,[],[33,35,34,37,73,74,87,49,42,51,45,17,25,26,2])).
% 6.34/6.52 cnf(120,plain,
% 6.34/6.52 (P7(x1201,x1202)+~E(x1202,x1201)),
% 6.34/6.52 inference(scs_inference,[],[73,17])).
% 6.34/6.52 cnf(126,plain,
% 6.34/6.52 (P4(f2(a1,a3),f2(a1,a4))+P4(f7(a1,a3),f7(a1,a4))),
% 6.34/6.52 inference(scs_inference,[],[34,76,72,59])).
% 6.34/6.52 cnf(135,plain,
% 6.34/6.52 (~P4(f2(a1,a3),f2(a1,a4))+~P6(a1,a4,a3)+~P4(f8(a1,a3),f8(a1,a4))),
% 6.34/6.52 inference(scs_inference,[],[37,43,70])).
% 6.34/6.52 cnf(165,plain,
% 6.34/6.52 (P4(f5(a1,a4),f5(a1,a3))+E(f5(a1,a3),f5(a1,a4))),
% 6.34/6.52 inference(scs_inference,[],[82,44])).
% 6.34/6.52 cnf(169,plain,
% 6.34/6.52 (P4(f5(a1,a4),f5(a1,a3))+E(f5(a1,a4),f5(a1,a3))),
% 6.34/6.52 inference(scs_inference,[],[90,44])).
% 6.34/6.52 cnf(180,plain,
% 6.34/6.52 (~P4(f5(a1,a3),f5(a1,a4))+E(f5(a1,a4),f5(a1,a3))),
% 6.34/6.52 inference(scs_inference,[],[169,47])).
% 6.34/6.52 cnf(195,plain,
% 6.34/6.52 (~P4(f5(a1,a3),f5(a1,a4))+~E(f9(a1,a4),f9(a1,a3))+E(f2(a1,a4),f2(a1,a3))),
% 6.34/6.52 inference(scs_inference,[],[76,180,67])).
% 6.34/6.52 cnf(218,plain,
% 6.34/6.52 (~E(a1,x2181)+P4(f8(x2181,x2182),f8(x2181,x2183))+~P4(f7(x2181,x2182),f7(x2181,x2183))),
% 6.34/6.52 inference(scs_inference,[],[33,66,16])).
% 6.34/6.52 cnf(219,plain,
% 6.34/6.52 (~P4(f7(a1,x2191),f7(a1,x2192))+P4(f8(a1,x2191),f8(a1,x2192))),
% 6.34/6.52 inference(equality_inference,[],[218])).
% 6.34/6.52 cnf(220,plain,
% 6.34/6.52 (~P4(f7(a1,x2201),f7(a1,x2201))),
% 6.34/6.52 inference(scs_inference,[],[219,47])).
% 6.34/6.52 cnf(221,plain,
% 6.34/6.52 (~P8(f7(a1,x2211),f7(a1,x2211))),
% 6.34/6.52 inference(scs_inference,[],[220,44])).
% 6.34/6.52 cnf(223,plain,
% 6.34/6.52 (~P4(f8(a1,a3),f8(a1,a4))+~P4(f9(a1,a3),f9(a1,a4))+~P6(a1,a4,a3)),
% 6.34/6.52 inference(scs_inference,[],[34,76,135,72])).
% 6.34/6.52 cnf(224,plain,
% 6.34/6.52 (~P8(f9(a1,a4),f9(a1,a3))+~P4(f8(a1,a3),f8(a1,a4))+~P6(a1,a4,a3)),
% 6.34/6.52 inference(scs_inference,[],[223,44])).
% 6.34/6.52 cnf(225,plain,
% 6.34/6.52 (~P8(f9(a1,a4),f9(a1,a3))+~P4(f8(a1,a3),f8(a1,a4))),
% 6.34/6.52 inference(scs_inference,[],[33,36,35,224,51])).
% 6.34/6.52 cnf(226,plain,
% 6.34/6.52 (~P4(f9(a1,a3),f9(a1,a4))+~P4(f8(a1,a3),f8(a1,a4))),
% 6.34/6.52 inference(scs_inference,[],[225,42])).
% 6.34/6.52 cnf(243,plain,
% 6.34/6.52 (E(f2(a1,a3),f2(a1,a4))+~E(f9(a1,a4),f9(a1,a3))+~P4(f5(a1,a3),f5(a1,a4))),
% 6.34/6.52 inference(scs_inference,[],[2,195])).
% 6.34/6.52 cnf(260,plain,
% 6.34/6.52 (E(f2(a1,x2601),f2(a1,x2602))+~E(f9(a1,x2602),f9(a1,x2601))+~E(f5(a1,x2602),f5(a1,x2601))),
% 6.34/6.52 inference(scs_inference,[],[76,2,67])).
% 6.34/6.52 cnf(318,plain,
% 6.34/6.52 (~E(a4,x3181)+~P2(a1,x3181)),
% 6.34/6.52 inference(scs_inference,[],[35,2,20])).
% 6.34/6.52 cnf(322,plain,
% 6.34/6.52 (~E(f5(a1,x3221),f5(a1,x3222))+~E(f9(a1,x3222),f9(a1,x3221))+E(f2(a1,x3222),f2(a1,x3221))),
% 6.34/6.52 inference(scs_inference,[],[76,2,67])).
% 6.34/6.52 cnf(332,plain,
% 6.34/6.52 (~E(f7(a1,x3321),x3322)+~P8(x3322,f7(a1,x3321))),
% 6.34/6.52 inference(scs_inference,[],[221,2,21])).
% 6.34/6.52 cnf(354,plain,
% 6.34/6.52 (~E(f8(a1,a3),f8(a1,a4))+~P6(a1,a4,a3)+~P4(f2(a1,a3),f2(a1,a4))),
% 6.34/6.52 inference(scs_inference,[],[37,39,71])).
% 6.34/6.52 cnf(355,plain,
% 6.34/6.52 (~P4(f2(a1,a3),f2(a1,a4))+~P6(a1,a4,a3)+~E(f7(a1,a3),f7(a1,a4))),
% 6.34/6.52 inference(scs_inference,[],[33,354,50])).
% 6.34/6.52 cnf(388,plain,
% 6.34/6.52 (P3(f2(a1,a3),f2(a1,a4))+~E(f9(a1,a4),f9(a1,a3))+~P4(f5(a1,a3),f5(a1,a4))),
% 6.34/6.52 inference(scs_inference,[],[39,243])).
% 6.34/6.52 cnf(389,plain,
% 6.34/6.52 (~E(f9(a1,a3),f9(a1,a4))+P3(f2(a1,a3),f2(a1,a4))+~P4(f5(a1,a3),f5(a1,a4))),
% 6.34/6.52 inference(scs_inference,[],[388,2])).
% 6.34/6.52 cnf(502,plain,
% 6.34/6.52 (P7(x5021,x5022)+~P4(x5022,x5021)),
% 6.34/6.52 inference(scs_inference,[],[42,41])).
% 6.34/6.52 cnf(520,plain,
% 6.34/6.52 (P8(f8(a1,x5201),f8(a1,x5202))+~P4(f7(a1,x5202),f7(a1,x5201))),
% 6.34/6.52 inference(scs_inference,[],[42,219])).
% 6.34/6.52 cnf(542,plain,
% 6.34/6.52 (P3(x5421,x5422)+~P8(x5422,x5421)),
% 6.34/6.52 inference(scs_inference,[],[43,44])).
% 6.34/6.52 cnf(545,plain,
% 6.34/6.52 (P3(f9(a1,a3),f9(a1,a4))),
% 6.34/6.52 inference(scs_inference,[],[43,57])).
% 6.34/6.52 cnf(546,plain,
% 6.34/6.52 (E(f9(a1,a3),f9(a1,a4))+P4(f9(a1,a3),f9(a1,a4))),
% 6.34/6.52 inference(scs_inference,[],[545,46])).
% 6.34/6.52 cnf(548,plain,
% 6.34/6.52 (E(f9(a1,a3),f9(a1,a4))+P4(f2(a1,a3),f2(a1,a4))),
% 6.34/6.52 inference(scs_inference,[],[34,545,76,46,72])).
% 6.34/6.52 cnf(590,plain,
% 6.34/6.52 (P4(f2(a1,a3),f2(a1,a4))+P3(f2(a1,a3),f2(a1,a4))+~P4(f5(a1,a3),f5(a1,a4))),
% 6.34/6.52 inference(scs_inference,[],[548,389])).
% 6.34/6.52 cnf(594,plain,
% 6.34/6.52 (P8(f2(a1,a4),f2(a1,a3))+P3(f2(a1,a3),f2(a1,a4))+~P4(f5(a1,a3),f5(a1,a4))),
% 6.34/6.52 inference(scs_inference,[],[590,42])).
% 6.34/6.52 cnf(597,plain,
% 6.34/6.52 (P3(f2(a1,a3),f2(a1,a4))+~P4(f5(a1,a3),f5(a1,a4))),
% 6.34/6.52 inference(scs_inference,[],[594,542])).
% 6.34/6.52 cnf(601,plain,
% 6.34/6.52 (P3(f7(a1,a3),f7(a1,a4))),
% 6.34/6.52 inference(scs_inference,[],[43,58])).
% 6.34/6.52 cnf(604,plain,
% 6.34/6.52 (E(f7(a1,a3),f7(a1,a4))+P8(f8(a1,a4),f8(a1,a3))),
% 6.34/6.52 inference(scs_inference,[],[601,46,520])).
% 6.34/6.52 cnf(682,plain,
% 6.34/6.52 (~P4(x6821,x6822)+~P8(x6821,x6822)),
% 6.34/6.52 inference(scs_inference,[],[44,47])).
% 6.34/6.52 cnf(706,plain,
% 6.34/6.52 (~P8(f8(a1,a4),f8(a1,a4))+P8(f6(a1,a4),f6(a1,a4))),
% 6.34/6.52 inference(scs_inference,[],[74,80,44,70])).
% 6.34/6.52 cnf(709,plain,
% 6.34/6.52 (P4(f6(a1,a4),f6(a1,a4))+~P8(f8(a1,a4),f8(a1,a4))),
% 6.34/6.52 inference(scs_inference,[],[44,706])).
% 6.34/6.52 cnf(710,plain,
% 6.34/6.52 (~P8(f8(a1,a4),f8(a1,a4))),
% 6.34/6.52 inference(scs_inference,[],[709,47])).
% 6.34/6.52 cnf(713,plain,
% 6.34/6.52 (~P6(a1,a4,a3)+~P3(f2(a1,a3),f2(a1,a4))+~P4(f8(a1,a3),f8(a1,a4))),
% 6.34/6.52 inference(scs_inference,[],[78,44,70])).
% 6.34/6.52 cnf(714,plain,
% 6.34/6.52 (~P3(f2(a1,a3),f2(a1,a4))+~P4(f8(a1,a3),f8(a1,a4))),
% 6.34/6.52 inference(scs_inference,[],[33,36,35,713,51])).
% 6.34/6.52 cnf(715,plain,
% 6.34/6.52 (~E(f2(a1,a3),f2(a1,a4))+~P4(f8(a1,a3),f8(a1,a4))),
% 6.34/6.52 inference(scs_inference,[],[714,39])).
% 6.34/6.52 cnf(716,plain,
% 6.34/6.52 (~E(f2(a1,a4),f2(a1,a3))+~P4(f8(a1,a3),f8(a1,a4))),
% 6.34/6.52 inference(scs_inference,[],[715,2])).
% 6.34/6.52 cnf(739,plain,
% 6.34/6.52 (P4(f8(a1,a3),f8(a1,a4))+E(f7(a1,a3),f7(a1,a4))),
% 6.34/6.52 inference(scs_inference,[],[44,604])).
% 6.34/6.52 cnf(788,plain,
% 6.34/6.52 (P7(f9(a1,a4),f9(a1,a3))+P4(f9(a1,a3),f9(a1,a4))),
% 6.34/6.52 inference(scs_inference,[],[545,120,46])).
% 6.34/6.52 cnf(814,plain,
% 6.34/6.52 (P6(a1,x8141,a3)+~E(a4,x8141)),
% 6.34/6.52 inference(scs_inference,[],[33,36,318,51])).
% 6.34/6.52 cnf(815,plain,
% 6.34/6.52 (P6(a1,a4,a3)),
% 6.34/6.52 inference(equality_inference,[],[814])).
% 6.34/6.52 cnf(816,plain,
% 6.34/6.52 (~P4(f2(a1,a3),f2(a1,a4))+~P4(f8(a1,a3),f8(a1,a4))),
% 6.34/6.52 inference(scs_inference,[],[815,135])).
% 6.34/6.52 cnf(818,plain,
% 6.34/6.52 (~P4(f2(a1,a3),f2(a1,a4))+~E(f7(a1,a3),f7(a1,a4))),
% 6.34/6.52 inference(scs_inference,[],[815,355])).
% 6.34/6.52 cnf(830,plain,
% 6.34/6.52 (~P8(f2(a1,a4),f2(a1,a3))+~P4(f8(a1,a3),f8(a1,a4))),
% 6.34/6.52 inference(scs_inference,[],[816,44])).
% 6.34/6.52 cnf(832,plain,
% 6.34/6.52 (P4(f7(a1,a3),f7(a1,a4))+~E(f7(a1,a3),f7(a1,a4))),
% 6.34/6.52 inference(scs_inference,[],[818,126])).
% 6.34/6.52 cnf(837,plain,
% 6.34/6.52 (P8(f7(a1,a4),f7(a1,a3))+~E(f7(a1,a3),f7(a1,a4))),
% 6.34/6.52 inference(scs_inference,[],[832,42])).
% 6.34/6.52 cnf(842,plain,
% 6.34/6.52 (~E(f7(a1,a3),f7(a1,a4))),
% 6.34/6.52 inference(scs_inference,[],[837,332])).
% 6.34/6.52 cnf(844,plain,
% 6.34/6.52 (P8(f8(a1,a4),f8(a1,a3))),
% 6.34/6.52 inference(scs_inference,[],[842,604])).
% 6.34/6.52 cnf(853,plain,
% 6.34/6.52 (P4(f8(a1,a3),f8(a1,a4))),
% 6.34/6.52 inference(scs_inference,[],[842,739])).
% 6.34/6.52 cnf(859,plain,
% 6.34/6.52 (~P4(f9(a1,a3),f9(a1,a4))),
% 6.34/6.52 inference(scs_inference,[],[853,226])).
% 6.34/6.52 cnf(863,plain,
% 6.34/6.52 (~P3(f2(a1,a3),f2(a1,a4))),
% 6.34/6.52 inference(scs_inference,[],[853,714])).
% 6.34/6.52 cnf(864,plain,
% 6.34/6.52 (~E(f2(a1,a3),f2(a1,a4))),
% 6.34/6.52 inference(scs_inference,[],[853,715])).
% 6.34/6.52 cnf(865,plain,
% 6.34/6.52 (~E(f2(a1,a4),f2(a1,a3))),
% 6.34/6.52 inference(scs_inference,[],[853,716])).
% 6.34/6.52 cnf(867,plain,
% 6.34/6.52 (~P4(f2(a1,a3),f2(a1,a4))),
% 6.34/6.52 inference(scs_inference,[],[853,816])).
% 6.34/6.52 cnf(869,plain,
% 6.34/6.52 (~P8(f2(a1,a4),f2(a1,a3))),
% 6.34/6.52 inference(scs_inference,[],[853,830])).
% 6.34/6.52 cnf(908,plain,
% 6.34/6.52 (E(f9(a1,a3),f9(a1,a4))),
% 6.34/6.52 inference(scs_inference,[],[859,546])).
% 6.34/6.52 cnf(913,plain,
% 6.34/6.52 (~P4(f5(a1,a3),f5(a1,a4))),
% 6.34/6.52 inference(scs_inference,[],[863,597])).
% 6.34/6.52 cnf(926,plain,
% 6.34/6.52 (P7(f9(a1,a4),f9(a1,a3))),
% 6.34/6.52 inference(scs_inference,[],[859,788])).
% 6.34/6.52 cnf(940,plain,
% 6.34/6.52 (P4(f2(a1,a4),f2(a1,a3))),
% 6.34/6.52 inference(scs_inference,[],[710,844,864,865,867,682,44,22,40,542,21,46])).
% 6.34/6.52 cnf(994,plain,
% 6.34/6.52 ($false),
% 6.34/6.52 inference(scs_inference,[],[76,73,864,865,869,908,926,940,913,2,502,44,260,322,18,69,165]),
% 6.34/6.52 ['proof']).
% 6.34/6.52 % SZS output end Proof
% 6.34/6.52 % Total time :6.020284s
%------------------------------------------------------------------------------