%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : MGT056+1 : TPTP v9.3.0. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% Computer : n006.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 2.45s 2.60s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : MGT056+1 : TPTP v9.3.0. Released v2.4.0.
% 0.00/0.03 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% 0.08/0.34 % Computer : n006.cluster.edu
% 0.08/0.34 % Model : x86_64 x86_64
% 0.08/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.34 % Memory : 8046.5625MB
% 0.08/0.34 % OS : Linux 6.8.0-71-generic
% 0.08/0.34 % CPULimit : 300
% 0.08/0.34 % WCLimit : 300
% 0.08/0.34 % DateTime : Mon Sep 7 13:28:01 UTC 2026
% 0.08/0.35 % CPUTime :
% 0.24/0.50 start to proof:theBenchmark
% 2.34/2.59 %-------------------------------------------
% 2.34/2.59 % File :CSE---1.7
% 2.34/2.59 % Problem :theBenchmark
% 2.34/2.59 % Transform :cnf
% 2.34/2.59 % Format :tptp:raw
% 2.34/2.59 % Command :java -jar mcs_scs.jar %d %s
% 2.34/2.59
% 2.34/2.59 % Result :Theorem 2.099866s
% 2.34/2.59 % Output :CNFRefutation 2.099866s
% 2.34/2.59 %-------------------------------------------
% 2.34/2.59 %--------------------------------------------------------------------------
% 2.34/2.59 % File : MGT056+1 : TPTP v9.3.0. Released v2.4.0.
% 2.34/2.59 % Domain : Management (Organisation Theory)
% 2.34/2.59 % Problem : Conditions for a constant then jumping hazard of mortality 2
% 2.34/2.59 % Version : [Han98] axioms.
% 2.34/2.59 % English : When (`eta' >= `sigma') in a drifting environment, an endowed
% 2.34/2.59 % organization's hazard of mortality remains constant until age
% 2.34/2.59 % `eta' and then jumps to a higher level in a drifting environment.
% 2.34/2.59
% 2.34/2.59 % Refs : [Kam00] Kamps (2000), Email to G. Sutcliffe
% 2.34/2.59 % : [CH00] Carroll & Hannan (2000), The Demography of Corporation
% 2.34/2.59 % : [Han98] Hannan (1998), Rethinking Age Dependence in Organizati
% 2.34/2.59 % Source : [Kam00]
% 2.34/2.59 % Names : LEMMA 9 [Han98]
% 2.34/2.59
% 2.34/2.59 % Status : Theorem
% 2.34/2.59 % Rating : 0.13 v9.3.0, 0.18 v9.1.0, 0.15 v9.0.0, 0.19 v8.2.0, 0.17 v8.1.0, 0.14 v7.5.0, 0.16 v7.4.0, 0.13 v7.3.0, 0.21 v7.2.0, 0.17 v7.1.0, 0.13 v7.0.0, 0.10 v6.4.0, 0.15 v6.3.0, 0.17 v6.2.0, 0.20 v6.0.0, 0.13 v5.5.0, 0.22 v5.4.0, 0.25 v5.3.0, 0.30 v5.2.0, 0.20 v5.1.0, 0.19 v5.0.0, 0.17 v4.0.1, 0.22 v4.0.0, 0.21 v3.7.0, 0.10 v3.5.0, 0.11 v3.3.0, 0.07 v3.2.0, 0.18 v3.1.0, 0.11 v2.7.0, 0.17 v2.6.0, 0.33 v2.5.0, 0.17 v2.4.0
% 2.34/2.59 % Syntax : Number of formulae : 10 ( 0 unt; 0 def)
% 2.34/2.59 % Number of atoms : 39 ( 6 equ)
% 2.34/2.59 % Maximal formula atoms : 9 ( 3 avg)
% 2.34/2.59 % Number of connectives : 32 ( 3 ~; 4 |; 15 &)
% 2.34/2.59 % ( 4 <=>; 6 =>; 0 <=; 0 <~>)
% 2.34/2.59 % Maximal formula depth : 12 ( 7 avg)
% 2.34/2.59 % Maximal term depth : 2 ( 1 avg)
% 2.34/2.59 % Number of predicates : 8 ( 7 usr; 0 prp; 1-2 aty)
% 2.34/2.59 % Number of functors : 5 ( 5 usr; 3 con; 0-2 aty)
% 2.34/2.59 % Number of variables : 25 ( 25 !; 0 ?)
% 2.34/2.59 % SPC : FOF_THM_RFO_SEQ
% 2.34/2.59
% 2.34/2.59 % Comments : See MGT042+1.p for the mnemonic names.
% 2.34/2.59 %--------------------------------------------------------------------------
% 2.34/2.59 include('Axioms/MGT001+0.ax').
% 2.34/2.59 %--------------------------------------------------------------------------
% 2.34/2.59 %----Problem Axioms
% 2.34/2.59 %----An endowment provides an immunity that lasts until an
% 2.34/2.60 %----organization's age exceeds `eta'.
% 2.34/2.60 fof(definition_1,axiom,
% 2.34/2.60 ! [X] :
% 2.34/2.60 ( has_endowment(X)
% 2.34/2.60 <=> ! [T] :
% 2.34/2.60 ( organization(X)
% 2.34/2.60 & ( smaller_or_equal(age(X,T),eta)
% 2.34/2.60 => has_immunity(X,T) )
% 2.34/2.60 & ( greater(age(X,T),eta)
% 2.34/2.60 => ~ has_immunity(X,T) ) ) ) ).
% 2.34/2.60
% 2.34/2.60 %----An organization's hazard of mortality is constant during periods
% 2.34/2.60 %----in which it has immunity.
% 2.34/2.60 fof(assumption_2,axiom,
% 2.34/2.60 ! [X,T0,T] :
% 2.34/2.60 ( ( organization(X)
% 2.34/2.60 & has_immunity(X,T0)
% 2.34/2.60 & has_immunity(X,T) )
% 2.34/2.60 => hazard_of_mortality(X,T0) = hazard_of_mortality(X,T) ) ).
% 2.34/2.60
% 2.34/2.60 %----An organization's hazard of mortality is lower during periods in
% 2.34/2.60 %----which it has immunity than in periods in which it does not.
% 2.34/2.60 fof(assumption_3,axiom,
% 2.34/2.60 ! [X,T0,T] :
% 2.34/2.60 ( ( organization(X)
% 2.34/2.60 & has_immunity(X,T0)
% 2.34/2.60 & ~ has_immunity(X,T) )
% 2.34/2.60 => greater(hazard_of_mortality(X,T),hazard_of_mortality(X,T0)) ) ).
% 2.34/2.60
% 2.34/2.60 %----Problem theorems
% 2.34/2.60 %----When (`eta' >= `sigma') in a drifting environment, an endowed
% 2.34/2.60 %----organization's hazard of mortality remains constant until age
% 2.34/2.60 %----`eta' and then jumps to a higher level in a drifting environment.
% 2.34/2.60 %----From D1, A2, A3 (text says D1-2, A1-3, 13-16; also needs D<, D<=, D>=,
% 2.34/2.60 %----MP>str, MP>com, MP>tra).
% 2.34/2.60 fof(lemma_9,conjecture,
% 2.34/2.60 ! [X,T0,T1,T2] :
% 2.34/2.60 ( ( organization(X)
% 2.34/2.60 & has_endowment(X)
% 2.34/2.60 & age(X,T0) = zero
% 2.34/2.60 & smaller_or_equal(age(X,T1),eta)
% 2.34/2.60 & greater(age(X,T2),eta)
% 2.34/2.60 & greater_or_equal(eta,sigma)
% 2.34/2.60 & greater(sigma,zero) )
% 2.34/2.60 => ( greater(hazard_of_mortality(X,T2),hazard_of_mortality(X,T1))
% 2.34/2.60 & hazard_of_mortality(X,T1) = hazard_of_mortality(X,T0) ) ) ).
% 2.45/2.60
% 2.45/2.60 %--------------------------------------------------------------------------
% 2.45/2.60 %-------------------------------------------
% 2.45/2.60 % Proof found
% 2.45/2.60 % SZS status Theorem for theBenchmark
% 2.45/2.60 % SZS output start Proof
% 2.45/2.60 %ClaNum:49(EqnAxiom:21)
% 2.45/2.60 %VarNum:106(SingletonVarNum:38)
% 2.45/2.60 %MaxLitNum:4
% 2.45/2.60 %MaxfuncDepth:2
% 2.45/2.60 %SharedTerms:22
% 2.45/2.60 %goalClause: 22 23 24 25 26 27 28 49
% 2.45/2.60 %singleGoalClaCount:7
% 2.45/2.60 [22]P1(a1)
% 2.45/2.60 [23]P4(a1)
% 2.45/2.60 [25]P2(a7,a10)
% 2.45/2.60 [26]P3(a10,a6)
% 2.45/2.60 [24]E(f2(a1,a5),a6)
% 2.45/2.60 [27]P6(f2(a1,a8),a7)
% 2.45/2.60 [28]P3(f2(a1,a9),a7)
% 2.45/2.60 [49]~P3(f11(a1,a9),f11(a1,a8))+~E(f11(a1,a8),f11(a1,a5))
% 2.45/2.60 [29]~P1(x291)+P4(x291)
% 2.45/2.60 [30]~E(x301,x302)+P6(x301,x302)
% 2.45/2.60 [31]~E(x311,x312)+P2(x311,x312)
% 2.45/2.60 [33]~P7(x331,x332)+P6(x331,x332)
% 2.45/2.60 [34]~P3(x342,x341)+P7(x341,x342)
% 2.45/2.60 [35]~P3(x351,x352)+P2(x351,x352)
% 2.45/2.60 [36]~P7(x362,x361)+P3(x361,x362)
% 2.45/2.60 [39]~P3(x392,x391)+~P3(x391,x392)
% 2.45/2.60 [32]P7(x321,x322)+P3(x321,x322)+E(x321,x322)
% 2.45/2.60 [37]P7(x371,x372)+~P6(x371,x372)+E(x371,x372)
% 2.45/2.60 [38]P3(x381,x382)+~P2(x381,x382)+E(x381,x382)
% 2.45/2.60 [43]~P1(x431)+P5(x431,x432)+~P6(f2(x431,x432),a7)
% 2.45/2.60 [45]~P1(x451)+~P5(x451,x452)+~P3(f2(x451,x452),a7)
% 2.45/2.60 [40]~P3(x401,x403)+P3(x401,x402)+~P3(x403,x402)
% 2.45/2.60 [41]~P4(x411)+P1(x411)+P5(x411,f3(x411))+~P5(x411,f4(x411))
% 2.45/2.60 [44]~P4(x441)+P1(x441)+P5(x441,f3(x441))+P6(f2(x441,f4(x441)),a7)
% 2.45/2.60 [46]~P4(x461)+P1(x461)+~P5(x461,f4(x461))+P3(f2(x461,f3(x461)),a7)
% 2.45/2.60 [48]~P4(x481)+P1(x481)+P6(f2(x481,f4(x481)),a7)+P3(f2(x481,f3(x481)),a7)
% 2.45/2.60 [42]~P4(x421)+~P5(x421,x423)+~P5(x421,x422)+E(f11(x421,x422),f11(x421,x423))
% 2.45/2.60 [47]~P4(x471)+~P5(x471,x473)+P5(x471,x472)+P3(f11(x471,x472),f11(x471,x473))
% 2.45/2.60 %EqnAxiom
% 2.45/2.60 [1]E(x11,x11)
% 2.45/2.60 [2]E(x22,x21)+~E(x21,x22)
% 2.45/2.60 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 2.45/2.60 [4]~E(x41,x42)+E(f2(x41,x43),f2(x42,x43))
% 2.45/2.60 [5]~E(x51,x52)+E(f2(x53,x51),f2(x53,x52))
% 2.45/2.60 [6]~E(x61,x62)+E(f11(x61,x63),f11(x62,x63))
% 2.45/2.60 [7]~E(x71,x72)+E(f11(x73,x71),f11(x73,x72))
% 2.45/2.60 [8]~E(x81,x82)+E(f4(x81),f4(x82))
% 2.45/2.60 [9]~E(x91,x92)+E(f3(x91),f3(x92))
% 2.45/2.60 [10]~P1(x101)+P1(x102)+~E(x101,x102)
% 2.45/2.60 [11]~P4(x111)+P4(x112)+~E(x111,x112)
% 2.45/2.60 [12]P2(x122,x123)+~E(x121,x122)+~P2(x121,x123)
% 2.45/2.60 [13]P2(x133,x132)+~E(x131,x132)+~P2(x133,x131)
% 2.45/2.60 [14]P3(x142,x143)+~E(x141,x142)+~P3(x141,x143)
% 2.45/2.60 [15]P3(x153,x152)+~E(x151,x152)+~P3(x153,x151)
% 2.45/2.60 [16]P6(x162,x163)+~E(x161,x162)+~P6(x161,x163)
% 2.45/2.60 [17]P6(x173,x172)+~E(x171,x172)+~P6(x173,x171)
% 2.45/2.60 [18]P5(x182,x183)+~E(x181,x182)+~P5(x181,x183)
% 2.45/2.60 [19]P5(x193,x192)+~E(x191,x192)+~P5(x193,x191)
% 2.45/2.60 [20]P7(x202,x203)+~E(x201,x202)+~P7(x201,x203)
% 2.45/2.60 [21]P7(x213,x212)+~E(x211,x212)+~P7(x213,x211)
% 2.45/2.60
% 2.45/2.60 %-------------------------------------------
% 2.45/2.60 cnf(50,plain,
% 2.45/2.60 (P6(x501,x501)),
% 2.45/2.60 inference(equality_inference,[],[30])).
% 2.45/2.60 cnf(51,plain,
% 2.45/2.60 (P2(x511,x511)),
% 2.45/2.60 inference(equality_inference,[],[31])).
% 2.45/2.60 cnf(52,plain,
% 2.45/2.60 (~P3(a6,a10)),
% 2.45/2.60 inference(scs_inference,[],[26,39])).
% 2.45/2.60 cnf(54,plain,
% 2.45/2.60 (E(a6,f2(a1,a5))),
% 2.45/2.60 inference(scs_inference,[],[26,24,39,2])).
% 2.45/2.60 cnf(55,plain,
% 2.45/2.60 (P5(a1,a8)),
% 2.45/2.60 inference(scs_inference,[],[22,26,24,27,39,2,43])).
% 2.45/2.60 cnf(57,plain,
% 2.45/2.60 (~P5(a1,a9)),
% 2.45/2.60 inference(scs_inference,[],[22,26,24,27,28,39,2,43,45])).
% 2.45/2.60 cnf(60,plain,
% 2.45/2.60 (P2(x601,x601)),
% 2.45/2.60 inference(rename_variables,[],[51])).
% 2.45/2.60 cnf(63,plain,
% 2.45/2.60 (P3(a10,f2(a1,a5))),
% 2.45/2.60 inference(scs_inference,[],[22,26,24,27,28,51,60,39,2,43,45,12,13,15])).
% 2.45/2.60 cnf(65,plain,
% 2.45/2.60 (P6(x651,x651)),
% 2.45/2.60 inference(rename_variables,[],[50])).
% 2.45/2.60 cnf(72,plain,
% 2.45/2.60 (E(a6,a10)+P7(a6,a10)),
% 2.45/2.60 inference(scs_inference,[],[22,26,24,27,28,50,65,51,60,39,2,43,45,12,13,15,16,17,19,36,10,32])).
% 2.45/2.60 cnf(76,plain,
% 2.45/2.60 (E(a7,a10)+P3(a7,a10)),
% 2.45/2.60 inference(scs_inference,[],[22,25,26,24,27,28,50,65,51,60,39,2,43,45,12,13,15,16,17,19,36,10,32,37,38])).
% 2.45/2.60 cnf(78,plain,
% 2.45/2.60 (~P3(x781,a10)+P3(x781,a6)),
% 2.45/2.60 inference(scs_inference,[],[22,25,26,24,27,28,50,65,51,60,39,2,43,45,12,13,15,16,17,19,36,10,32,37,38,40])).
% 2.45/2.60 cnf(90,plain,
% 2.45/2.60 (~P3(f2(a1,a5),a10)),
% 2.45/2.60 inference(scs_inference,[],[63,39])).
% 2.45/2.60 cnf(103,plain,
% 2.45/2.60 (P6(f2(a1,a8),x1031)+~E(a7,x1031)),
% 2.45/2.60 inference(scs_inference,[],[27,17])).
% 2.45/2.60 cnf(106,plain,
% 2.45/2.60 (P2(x1061,a10)+~E(a7,x1061)),
% 2.45/2.60 inference(scs_inference,[],[27,24,25,55,17,11,18,12])).
% 2.45/2.60 cnf(120,plain,
% 2.45/2.60 (~P3(x1201,a10)+P3(x1201,f2(a1,a5))),
% 2.45/2.60 inference(scs_inference,[],[63,40])).
% 2.45/2.60 cnf(136,plain,
% 2.45/2.60 (E(a6,a10)+P7(f2(a1,a5),a10)),
% 2.45/2.60 inference(scs_inference,[],[54,90,32,3])).
% 2.45/2.60 cnf(152,plain,
% 2.45/2.60 (P3(f2(a1,a9),x1521)+~E(a7,x1521)),
% 2.45/2.60 inference(scs_inference,[],[28,15])).
% 2.45/2.60 cnf(153,plain,
% 2.45/2.60 (P3(f2(a1,a9),a6)+~E(a7,a10)),
% 2.45/2.60 inference(scs_inference,[],[26,28,15,40])).
% 2.45/2.60 cnf(160,plain,
% 2.45/2.60 (~P3(a10,f2(a1,a9))+~E(a7,a10)),
% 2.45/2.60 inference(scs_inference,[],[26,28,24,52,15,40,14,3,120,5,39])).
% 2.45/2.60 cnf(170,plain,
% 2.45/2.60 (P3(x1701,f2(a1,a5))+~E(a10,x1701)),
% 2.45/2.60 inference(scs_inference,[],[63,14])).
% 2.45/2.60 cnf(174,plain,
% 2.45/2.60 (P6(a7,f2(a1,a9))),
% 2.45/2.60 inference(scs_inference,[],[28,33,34])).
% 2.45/2.60 cnf(175,plain,
% 2.45/2.60 (P6(x1751,f2(a1,a9))+~E(a7,x1751)),
% 2.45/2.60 inference(scs_inference,[],[174,16])).
% 2.45/2.60 cnf(179,plain,
% 2.45/2.60 (P2(x1791,a7)+~E(f2(a1,a9),x1791)),
% 2.45/2.60 inference(scs_inference,[],[28,35,12])).
% 2.45/2.60 cnf(180,plain,
% 2.45/2.60 (P2(f2(a1,a9),a7)),
% 2.45/2.60 inference(equality_inference,[],[179])).
% 2.45/2.60 cnf(181,plain,
% 2.45/2.60 (P2(f2(a1,a9),x1811)+~E(a7,x1811)),
% 2.45/2.60 inference(scs_inference,[],[180,13])).
% 2.45/2.60 cnf(189,plain,
% 2.45/2.60 (P6(a6,a10)+E(a6,a10)),
% 2.45/2.60 inference(scs_inference,[],[72,33])).
% 2.45/2.60 cnf(191,plain,
% 2.45/2.60 (P7(a6,x1911)+~P3(x1911,a10)),
% 2.45/2.61 inference(scs_inference,[],[78,34])).
% 2.45/2.61 cnf(197,plain,
% 2.45/2.61 (~P7(a10,x1971)+P7(a6,x1971)),
% 2.45/2.61 inference(scs_inference,[],[191,36])).
% 2.45/2.61 cnf(199,plain,
% 2.45/2.61 (P6(a6,x1991)+~P7(a10,x1991)),
% 2.45/2.61 inference(scs_inference,[],[197,33])).
% 2.45/2.61 cnf(200,plain,
% 2.45/2.61 (~P3(x2001,a10)+P6(a6,x2001)),
% 2.45/2.61 inference(scs_inference,[],[199,34])).
% 2.45/2.61 cnf(201,plain,
% 2.45/2.61 (P6(f2(a1,a5),x2011)+~P3(x2011,a10)),
% 2.45/2.61 inference(scs_inference,[],[54,200,16])).
% 2.45/2.61 cnf(212,plain,
% 2.45/2.61 (P3(a7,a10)+~P3(a10,f2(a1,a9))),
% 2.45/2.61 inference(scs_inference,[],[160,76])).
% 2.45/2.61 cnf(216,plain,
% 2.45/2.61 (P5(a1,a5)+~P3(a7,a10)),
% 2.45/2.61 inference(scs_inference,[],[22,201,43])).
% 2.45/2.61 cnf(390,plain,
% 2.45/2.61 (P3(f11(a1,a9),f11(a1,a8))),
% 2.45/2.61 inference(scs_inference,[],[22,55,57,29,47])).
% 2.45/2.61 cnf(391,plain,
% 2.45/2.61 (~E(f11(a1,a8),f11(a1,a5))),
% 2.45/2.61 inference(scs_inference,[],[390,49])).
% 2.45/2.61 cnf(407,plain,
% 2.45/2.61 (~P5(a1,a5)),
% 2.45/2.61 inference(scs_inference,[],[391,23,55,42])).
% 2.45/2.61 cnf(415,plain,
% 2.45/2.61 (~P3(a7,a10)),
% 2.45/2.61 inference(scs_inference,[],[407,216])).
% 2.45/2.61 cnf(425,plain,
% 2.45/2.61 (E(a7,a10)),
% 2.45/2.61 inference(scs_inference,[],[415,76])).
% 2.45/2.61 cnf(426,plain,
% 2.45/2.61 (~P3(a10,f2(a1,a9))),
% 2.45/2.61 inference(scs_inference,[],[415,212])).
% 2.45/2.61 cnf(434,plain,
% 2.45/2.61 (P3(f2(a1,a9),a6)),
% 2.45/2.61 inference(scs_inference,[],[425,153])).
% 2.45/2.61 cnf(448,plain,
% 2.45/2.61 (P3(f2(a1,a9),a10)),
% 2.45/2.61 inference(scs_inference,[],[425,103,152])).
% 2.45/2.61 cnf(455,plain,
% 2.45/2.61 (E(a10,a7)),
% 2.45/2.61 inference(scs_inference,[],[425,103,152,175,181,191,201,2])).
% 2.45/2.61 cnf(460,plain,
% 2.45/2.61 (P3(a7,a6)),
% 2.45/2.61 inference(scs_inference,[],[26,24,425,426,434,103,152,175,181,191,201,2,39,16,15,14])).
% 2.45/2.61 cnf(461,plain,
% 2.45/2.61 (P3(a7,f2(a1,a5))),
% 2.45/2.61 inference(scs_inference,[],[26,24,425,426,434,103,152,175,181,191,201,2,39,16,15,14,170])).
% 2.45/2.61 cnf(502,plain,
% 2.45/2.61 (~P3(a6,a7)),
% 2.45/2.61 inference(scs_inference,[],[460,39])).
% 2.45/2.61 cnf(538,plain,
% 2.45/2.61 (E(a6,a7)+P7(a6,a7)),
% 2.45/2.61 inference(scs_inference,[],[502,32])).
% 2.45/2.61 cnf(573,plain,
% 2.45/2.61 (P6(a6,a7)+E(a6,a7)),
% 2.45/2.61 inference(scs_inference,[],[538,33])).
% 2.45/2.61 cnf(577,plain,
% 2.45/2.61 (P6(f2(a1,a5),a7)+E(a6,a7)),
% 2.45/2.61 inference(scs_inference,[],[54,573,16])).
% 2.45/2.61 cnf(591,plain,
% 2.45/2.61 (~E(a6,a10)),
% 2.45/2.61 inference(scs_inference,[],[415,460,15])).
% 2.45/2.61 cnf(594,plain,
% 2.45/2.61 (P7(f2(a1,a5),a10)),
% 2.45/2.61 inference(scs_inference,[],[415,448,460,15,14,72,136])).
% 2.45/2.61 cnf(604,plain,
% 2.45/2.61 (P6(a6,a10)),
% 2.45/2.61 inference(scs_inference,[],[591,189])).
% 2.45/2.61 cnf(606,plain,
% 2.45/2.61 (E(a6,a7)),
% 2.45/2.61 inference(scs_inference,[],[22,407,577,43])).
% 2.45/2.61 cnf(611,plain,
% 2.45/2.61 (P2(a6,a10)),
% 2.45/2.61 inference(scs_inference,[],[415,455,461,594,606,604,2,21,15,17,106])).
% 2.45/2.61 cnf(623,plain,
% 2.45/2.61 ($false),
% 2.45/2.61 inference(scs_inference,[],[52,611,591,38]),
% 2.45/2.61 ['proof']).
% 2.45/2.61 % SZS output end Proof
% 2.45/2.61 % Total time :2.099866s
%------------------------------------------------------------------------------