%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : MGT065+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 : n010.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:23 AM UTC 2026
% Result : Theorem 182.27s 182.31s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : MGT065+1 : TPTP v9.3.0. Released v2.4.0.
% 0.00/0.02 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% 0.06/0.34 % Computer : n010.cluster.edu
% 0.06/0.34 % Model : x86_64 x86_64
% 0.06/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.06/0.34 % Memory : 8046.5625MB
% 0.06/0.34 % OS : Linux 6.8.0-71-generic
% 0.06/0.34 % CPULimit : 300
% 0.06/0.34 % WCLimit : 300
% 0.06/0.34 % DateTime : Mon Sep 7 13:45:41 UTC 2026
% 0.06/0.34 % CPUTime :
% 0.23/0.50 start to proof:theBenchmark
% 182.16/182.29 %-------------------------------------------
% 182.16/182.29 % File :CSE---1.7
% 182.16/182.29 % Problem :theBenchmark
% 182.16/182.29 % Transform :cnf
% 182.16/182.29 % Format :tptp:raw
% 182.16/182.29 % Command :java -jar mcs_scs.jar %d %s
% 182.16/182.29
% 182.16/182.29 % Result :Theorem 181.786973s
% 182.16/182.29 % Output :CNFRefutation 181.786973s
% 182.16/182.29 %-------------------------------------------
% 182.16/182.30 %--------------------------------------------------------------------------
% 182.16/182.30 % File : MGT065+1 : TPTP v9.3.0. Released v2.4.0.
% 182.16/182.30 % Domain : Management (Organisation Theory)
% 182.16/182.30 % Problem : Long-run hazard of mortality
% 182.16/182.30 % Version : [Han98] axioms.
% 182.16/182.30 % English : The long-run hazard of mortality for an endowed organization with
% 182.16/182.30 % either a fragile or a robust position in a drifting environment
% 182.16/182.30 % exceeds the hazard near founding.
% 182.16/182.30
% 182.16/182.30 % Refs : [Kam00] Kamps (2000), Email to G. Sutcliffe
% 182.16/182.30 % : [CH00] Carroll & Hannan (2000), The Demography of Corporation
% 182.16/182.30 % : [Han98] Hannan (1998), Rethinking Age Dependence in Organizati
% 182.16/182.30 % Source : [Kam00]
% 182.27/182.30 % Names : THEOREM 11 [Han98]
% 182.27/182.30
% 182.27/182.30 % Status : Theorem
% 182.27/182.30 % Rating : 0.17 v9.3.0, 0.30 v9.1.0, 0.24 v9.0.0, 0.31 v8.2.0, 0.28 v8.1.0, 0.25 v7.5.0, 0.28 v7.4.0, 0.23 v7.3.0, 0.31 v7.2.0, 0.28 v7.1.0, 0.26 v7.0.0, 0.17 v6.4.0, 0.23 v6.3.0, 0.25 v6.2.0, 0.28 v6.1.0, 0.33 v6.0.0, 0.26 v5.5.0, 0.33 v5.4.0, 0.39 v5.3.0, 0.41 v5.2.0, 0.30 v5.1.0, 0.29 v4.1.0, 0.35 v4.0.0, 0.33 v3.7.0, 0.25 v3.5.0, 0.21 v3.4.0, 0.26 v3.3.0, 0.29 v3.2.0, 0.36 v3.1.0, 0.44 v2.7.0, 0.33 v2.6.0, 0.50 v2.5.0, 0.33 v2.4.0
% 182.27/182.30 % Syntax : Number of formulae : 17 ( 5 unt; 0 def)
% 182.27/182.30 % Number of atoms : 70 ( 12 equ)
% 182.27/182.30 % Maximal formula atoms : 16 ( 4 avg)
% 182.27/182.30 % Number of connectives : 61 ( 8 ~; 5 |; 28 &)
% 182.27/182.30 % ( 7 <=>; 13 =>; 0 <=; 0 <~>)
% 182.27/182.30 % Maximal formula depth : 18 ( 5 avg)
% 182.27/182.30 % Maximal term depth : 2 ( 1 avg)
% 182.27/182.30 % Number of predicates : 13 ( 12 usr; 0 prp; 1-3 aty)
% 182.27/182.30 % Number of functors : 11 ( 11 usr; 9 con; 0-2 aty)
% 182.27/182.30 % Number of variables : 29 ( 29 !; 0 ?)
% 182.27/182.30 % SPC : FOF_THM_RFO_SEQ
% 182.27/182.30
% 182.27/182.30 % Comments : See MGT042+1.p for the mnemonic names.
% 182.27/182.30 %--------------------------------------------------------------------------
% 182.27/182.30 include('Axioms/MGT001+0.ax').
% 182.27/182.30 %--------------------------------------------------------------------------
% 182.27/182.30 %----Problem Axioms
% 182.27/182.30 %----An endowment provides an immunity that lasts until an
% 182.27/182.30 %----organization's age exceeds `eta'.
% 182.27/182.30 fof(definition_1,axiom,
% 182.27/182.30 ! [X] :
% 182.27/182.30 ( has_endowment(X)
% 182.27/182.30 <=> ! [T] :
% 182.27/182.30 ( organization(X)
% 182.27/182.30 & ( smaller_or_equal(age(X,T),eta)
% 182.27/182.30 => has_immunity(X,T) )
% 182.27/182.30 & ( greater(age(X,T),eta)
% 182.27/182.30 => ~ has_immunity(X,T) ) ) ) ).
% 182.27/182.30
% 182.27/182.30 %----Two states of the environment are dissimilar for an organization
% 182.27/182.30 %----if and only if the organization cannot be aligned to both.
% 182.27/182.30 %----
% 182.27/182.30 %----Added quantification over X.
% 182.27/182.30 fof(definition_2,axiom,
% 182.27/182.30 ! [X,T0,T] :
% 182.27/182.30 ( dissimilar(X,T0,T)
% 182.27/182.30 <=> ( organization(X)
% 182.27/182.30 & ~ ( is_aligned(X,T0)
% 182.27/182.30 <=> is_aligned(X,T) ) ) ) ).
% 182.27/182.30
% 182.27/182.30 %----An organization is aligned with the state of the environment at
% 182.27/182.30 %----its time of founding.
% 182.27/182.30 fof(assumption_13,axiom,
% 182.27/182.30 ! [X,T] :
% 182.27/182.30 ( ( organization(X)
% 182.27/182.30 & age(X,T) = zero )
% 182.27/182.30 => is_aligned(X,T) ) ).
% 182.27/182.30
% 182.27/182.30 %----Environmental drift: the environments at times separated by more
% 182.27/182.30 %----than `sigma' are dissimilar.
% 182.27/182.30 fof(assumption_15,axiom,
% 182.27/182.30 ! [X,T0,T] :
% 182.27/182.30 ( ( organization(X)
% 182.27/182.30 & age(X,T0) = zero )
% 182.27/182.30 => ( greater(age(X,T),sigma)
% 182.27/182.30 <=> dissimilar(X,T0,T) ) ) ).
% 182.27/182.30
% 182.27/182.30 %----An organization's immunity. alignment of capability with the
% 182.27/182.30 %----current state of the environment and positional advantage jointly
% 182.27/182.30 %----affect the hazard of mortality with the following ordinal scaling:
% 182.27/182.30 fof(assumption_17,axiom,
% 182.27/182.30 ! [X,T] :
% 182.27/182.30 ( organization(X)
% 182.27/182.30 => ( ( has_immunity(X,T)
% 182.27/182.30 => hazard_of_mortality(X,T) = very_low )
% 182.27/182.30 & ( ~ has_immunity(X,T)
% 182.27/182.30 => ( ( ( is_aligned(X,T)
% 182.27/182.30 & positional_advantage(X,T) )
% 182.27/182.30 => hazard_of_mortality(X,T) = low )
% 182.27/182.30 & ( ( ~ is_aligned(X,T)
% 182.27/182.30 & positional_advantage(X,T) )
% 182.27/182.30 => hazard_of_mortality(X,T) = mod1 )
% 182.27/182.30 & ( ( is_aligned(X,T)
% 182.27/182.30 & ~ positional_advantage(X,T) )
% 182.27/182.30 => hazard_of_mortality(X,T) = mod2 )
% 182.27/182.30 & ( ( ~ is_aligned(X,T)
% 182.27/182.30 & ~ positional_advantage(X,T) )
% 182.27/182.30 => hazard_of_mortality(X,T) = high ) ) ) ) ) ).
% 182.27/182.30
% 182.27/182.30 %----The levels of hazard of mortality are ordered:
% 182.27/182.30 %----
% 182.27/182.31 %----Split over 5 separate formulas because TPTP gives an error on top
% 182.27/182.31 %----level occurrences of `&'.
% 182.27/182.31 fof(assumption_18a,axiom,
% 182.27/182.31 greater(high,mod1) ).
% 182.27/182.31
% 182.27/182.31 fof(assumption_18b,axiom,
% 182.27/182.31 greater(mod1,low) ).
% 182.27/182.31
% 182.27/182.31 fof(assumption_18c,axiom,
% 182.27/182.31 greater(low,very_low) ).
% 182.27/182.31
% 182.27/182.31 fof(assumption_18d,axiom,
% 182.27/182.31 greater(high,mod2) ).
% 182.27/182.31
% 182.27/182.31 fof(assumption_18e,axiom,
% 182.27/182.31 greater(mod2,low) ).
% 182.27/182.31
% 182.27/182.31 %----Problem theorems
% 182.27/182.31 %----The long-run hazard of mortality for an endowed organization with
% 182.27/182.31 %----either a fragile or a robust position in a drifting environment
% 182.27/182.31 %----exceeds the hazard near founding.
% 182.27/182.31 %----From D1, D2, A13, A15, A17, A18 (text says D1,2,4 and A1,2,13-15,17-19;
% 182.27/182.31 %----also needs D<, D<=, MP>str, MP>com, MP>tra).
% 182.27/182.31 %----
% 182.27/182.31 %----Expanding (age(X,T1) <= min(eta,sigma,tau)) and
% 182.27/182.31 %----expanding (age(X,T1) > max(eta,sigma,tau));
% 182.27/182.31 %----Text says RB(x) & FG(x) which contradicts lemma 10; changed to |.
% 182.27/182.31 %----added (hazard_of_mortality(X,T1) = hazard_of_mortality(X,T0)).
% 182.27/182.31 fof(theorem_11,conjecture,
% 182.27/182.31 ! [X,T0,T1,T2] :
% 182.27/182.31 ( ( organization(X)
% 182.27/182.31 & ( robust_position(X)
% 182.27/182.31 | fragile_position(X) )
% 182.27/182.31 & has_endowment(X)
% 182.27/182.31 & age(X,T0) = zero
% 182.27/182.31 & greater(sigma,zero)
% 182.27/182.31 & greater(tau,zero)
% 182.27/182.31 & greater(eta,zero)
% 182.27/182.31 & smaller_or_equal(age(X,T1),sigma)
% 182.27/182.31 & smaller_or_equal(age(X,T1),tau)
% 182.27/182.31 & smaller_or_equal(age(X,T1),eta)
% 182.27/182.31 & greater(age(X,T2),sigma)
% 182.27/182.31 & greater(age(X,T2),tau)
% 182.27/182.31 & greater(age(X,T2),eta) )
% 182.27/182.31 => ( greater(hazard_of_mortality(X,T2),hazard_of_mortality(X,T1))
% 182.27/182.31 & hazard_of_mortality(X,T1) = hazard_of_mortality(X,T0) ) ) ).
% 182.27/182.31
% 182.27/182.31 %--------------------------------------------------------------------------
% 182.27/182.31 %-------------------------------------------
% 182.27/182.31 % Proof found
% 182.27/182.31 % SZS status Theorem for theBenchmark
% 182.27/182.31 % SZS output start Proof
% 182.27/182.31 %ClaNum:83(EqnAxiom:32)
% 182.27/182.31 %VarNum:185(SingletonVarNum:67)
% 182.27/182.31 %MaxLitNum:4
% 182.27/182.31 %MaxfuncDepth:2
% 182.27/182.31 %SharedTerms:40
% 182.27/182.31 %goalClause: 33 34 35 36 37 43 44 45 46 47 48 49 50 80
% 182.27/182.31 %singleGoalClaCount:12
% 182.27/182.31 [33]P1(a1)
% 182.27/182.31 [34]P7(a1)
% 182.27/182.31 [36]P2(a7,a6)
% 182.27/182.31 [37]P2(a10,a6)
% 182.27/182.31 [38]P2(a11,a16)
% 182.27/182.31 [39]P2(a14,a11)
% 182.27/182.31 [40]P2(a15,a11)
% 182.27/182.31 [41]P2(a12,a14)
% 182.27/182.31 [42]P2(a12,a15)
% 182.27/182.31 [43]P2(a17,a6)
% 182.27/182.31 [35]E(f2(a1,a5),a6)
% 182.27/182.31 [44]P10(f2(a1,a8),a7)
% 182.27/182.31 [45]P10(f2(a1,a8),a10)
% 182.27/182.31 [46]P10(f2(a1,a8),a17)
% 182.27/182.31 [47]P2(f2(a1,a9),a7)
% 182.27/182.31 [48]P2(f2(a1,a9),a10)
% 182.27/182.31 [49]P2(f2(a1,a9),a17)
% 182.27/182.31 [50]P11(a1)+P3(a1)
% 182.27/182.31 [80]~P2(f13(a1,a9),f13(a1,a8))+~E(f13(a1,a8),f13(a1,a5))
% 182.27/182.31 [51]~P1(x511)+P7(x511)
% 182.27/182.31 [52]~E(x521,x522)+P10(x521,x522)
% 182.27/182.31 [53]~E(x531,x532)+P6(x531,x532)
% 182.27/182.31 [56]~P13(x561,x562)+P10(x561,x562)
% 182.27/182.31 [57]~P2(x572,x571)+P13(x571,x572)
% 182.27/182.31 [58]~P2(x581,x582)+P6(x581,x582)
% 182.27/182.31 [59]~P13(x592,x591)+P2(x591,x592)
% 182.27/182.31 [64]~P2(x642,x641)+~P2(x641,x642)
% 182.27/182.31 [73]P7(x731)+~P5(x731,x732,x733)
% 182.27/182.31 [54]P13(x541,x542)+P2(x541,x542)+E(x541,x542)
% 182.27/182.31 [55]P4(x551,x552)+~P7(x551)+P8(x551,x552)
% 182.27/182.31 [60]P13(x601,x602)+~P10(x601,x602)+E(x601,x602)
% 182.27/182.31 [61]P2(x611,x612)+~P6(x611,x612)+E(x611,x612)
% 182.27/182.31 [62]~P7(x621)+~P8(x621,x622)+E(f13(x621,x622),a16)
% 182.27/182.31 [63]~P7(x631)+P9(x631,x632)+~E(f2(x631,x632),a6)
% 182.27/182.31 [70]~P1(x701)+P8(x701,x702)+~P10(f2(x701,x702),a7)
% 182.27/182.31 [74]~P1(x741)+~P8(x741,x742)+~P2(f2(x741,x742),a7)
% 182.27/182.31 [65]~P2(x651,x653)+P2(x651,x652)+~P2(x653,x652)
% 182.27/182.31 [79]~P5(x791,x793,x792)+P9(x791,x792)+P9(x791,x793)
% 182.27/182.31 [81]~P5(x811,x813,x812)+~P9(x811,x812)+~P9(x811,x813)
% 182.27/182.31 [66]~P7(x661)+P1(x661)+P8(x661,f3(x661))+~P8(x661,f4(x661))
% 182.27/182.31 [72]~P7(x721)+P1(x721)+P8(x721,f3(x721))+P10(f2(x721,f4(x721)),a7)
% 182.27/182.31 [75]~P7(x751)+P1(x751)+~P8(x751,f4(x751))+P2(f2(x751,f3(x751)),a7)
% 182.27/182.31 [78]~P7(x781)+P1(x781)+P10(f2(x781,f4(x781)),a7)+P2(f2(x781,f3(x781)),a7)
% 182.27/182.31 [67]P9(x671,x672)+P12(x671,x672)+~P4(x671,x672)+E(f13(x671,x672),a12)
% 182.27/182.31 [68]P9(x681,x682)+~P12(x681,x682)+~P4(x681,x682)+E(f13(x681,x682),a14)
% 182.27/182.31 [69]P12(x691,x692)+~P9(x691,x692)+~P4(x691,x692)+E(f13(x691,x692),a15)
% 182.27/182.31 [71]~P9(x711,x712)+~P12(x711,x712)+~P4(x711,x712)+E(f13(x711,x712),a11)
% 182.27/182.31 [76]~P7(x761)+~P9(x761,x763)+P9(x761,x762)+P5(x761,x762,x763)
% 182.27/182.31 [77]~P7(x771)+~P9(x771,x773)+P9(x771,x772)+P5(x771,x773,x772)
% 182.27/182.31 [82]~P7(x821)+P5(x821,x822,x823)+~E(f2(x821,x822),a6)+~P2(f2(x821,x823),a10)
% 182.27/182.31 [83]~P7(x831)+~P5(x831,x833,x832)+P2(f2(x831,x832),a10)+~E(f2(x831,x833),a6)
% 182.27/182.31 %EqnAxiom
% 182.27/182.31 [1]E(x11,x11)
% 182.27/182.31 [2]E(x22,x21)+~E(x21,x22)
% 182.27/182.31 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 182.27/182.31 [4]~E(x41,x42)+E(f2(x41,x43),f2(x42,x43))
% 182.27/182.31 [5]~E(x51,x52)+E(f2(x53,x51),f2(x53,x52))
% 182.27/182.31 [6]~E(x61,x62)+E(f13(x61,x63),f13(x62,x63))
% 182.27/182.31 [7]~E(x71,x72)+E(f13(x73,x71),f13(x73,x72))
% 182.27/182.31 [8]~E(x81,x82)+E(f4(x81),f4(x82))
% 182.27/182.31 [9]~E(x91,x92)+E(f3(x91),f3(x92))
% 182.27/182.31 [10]~P1(x101)+P1(x102)+~E(x101,x102)
% 182.27/182.31 [11]~P7(x111)+P7(x112)+~E(x111,x112)
% 182.27/182.31 [12]P2(x122,x123)+~E(x121,x122)+~P2(x121,x123)
% 182.27/182.31 [13]P2(x133,x132)+~E(x131,x132)+~P2(x133,x131)
% 182.27/182.31 [14]P9(x142,x143)+~E(x141,x142)+~P9(x141,x143)
% 182.27/182.31 [15]P9(x153,x152)+~E(x151,x152)+~P9(x153,x151)
% 182.27/182.31 [16]P12(x162,x163)+~E(x161,x162)+~P12(x161,x163)
% 182.27/182.31 [17]P12(x173,x172)+~E(x171,x172)+~P12(x173,x171)
% 182.27/182.31 [18]P5(x182,x183,x184)+~E(x181,x182)+~P5(x181,x183,x184)
% 182.27/182.31 [19]P5(x193,x192,x194)+~E(x191,x192)+~P5(x193,x191,x194)
% 182.27/182.31 [20]P5(x203,x204,x202)+~E(x201,x202)+~P5(x203,x204,x201)
% 182.27/182.31 [21]P8(x212,x213)+~E(x211,x212)+~P8(x211,x213)
% 182.27/182.31 [22]P8(x223,x222)+~E(x221,x222)+~P8(x223,x221)
% 182.27/182.31 [23]P4(x232,x233)+~E(x231,x232)+~P4(x231,x233)
% 182.27/182.31 [24]P4(x243,x242)+~E(x241,x242)+~P4(x243,x241)
% 182.27/182.31 [25]P10(x252,x253)+~E(x251,x252)+~P10(x251,x253)
% 182.27/182.31 [26]P10(x263,x262)+~E(x261,x262)+~P10(x263,x261)
% 182.27/182.31 [27]P13(x272,x273)+~E(x271,x272)+~P13(x271,x273)
% 182.27/182.31 [28]P13(x283,x282)+~E(x281,x282)+~P13(x283,x281)
% 182.27/182.31 [29]P6(x292,x293)+~E(x291,x292)+~P6(x291,x293)
% 182.27/182.31 [30]P6(x303,x302)+~E(x301,x302)+~P6(x303,x301)
% 182.27/182.31 [31]~P11(x311)+P11(x312)+~E(x311,x312)
% 182.27/182.31 [32]~P3(x321)+P3(x322)+~E(x321,x322)
% 182.27/182.31
% 182.27/182.31 %-------------------------------------------
% 182.27/182.32 cnf(84,plain,
% 182.27/182.32 (P10(x841,x841)),
% 182.27/182.32 inference(equality_inference,[],[52])).
% 182.27/182.32 cnf(85,plain,
% 182.27/182.32 (P6(x851,x851)),
% 182.27/182.32 inference(equality_inference,[],[53])).
% 182.27/182.32 cnf(86,plain,
% 182.27/182.32 (E(a6,f2(a1,a5))),
% 182.27/182.32 inference(scs_inference,[],[35,2])).
% 182.27/182.32 cnf(89,plain,
% 182.27/182.32 (P9(a1,a5)),
% 182.27/182.32 inference(scs_inference,[],[34,36,35,2,64,63])).
% 182.27/182.32 cnf(91,plain,
% 182.27/182.32 (P8(a1,a8)),
% 182.27/182.32 inference(scs_inference,[],[33,34,36,35,44,2,64,63,70])).
% 182.27/182.32 cnf(93,plain,
% 182.27/182.32 (~P8(a1,a9)),
% 182.27/182.32 inference(scs_inference,[],[33,34,36,35,44,47,2,64,63,70,74])).
% 182.27/182.32 cnf(96,plain,
% 182.27/182.32 (P2(a7,f2(a1,a5))),
% 182.27/182.32 inference(scs_inference,[],[33,34,36,35,44,47,2,64,63,70,74,12,13])).
% 182.27/182.32 cnf(101,plain,
% 182.27/182.32 (~E(a8,a9)),
% 182.27/182.32 inference(scs_inference,[],[33,34,36,35,44,47,2,64,63,70,74,12,13,65,81,22])).
% 182.27/182.32 cnf(103,plain,
% 182.27/182.32 (P10(x1031,x1031)),
% 182.27/182.32 inference(rename_variables,[],[84])).
% 182.27/182.32 cnf(107,plain,
% 182.27/182.32 (P6(x1071,x1071)),
% 182.27/182.32 inference(rename_variables,[],[85])).
% 182.27/182.32 cnf(110,plain,
% 182.27/182.32 (P5(a1,a5,a9)),
% 182.27/182.32 inference(scs_inference,[],[33,34,36,48,35,44,47,84,103,85,107,2,64,63,70,74,12,13,65,81,22,25,26,29,30,82])).
% 182.27/182.32 cnf(112,plain,
% 182.27/182.32 (~P13(a7,a6)),
% 182.27/182.32 inference(scs_inference,[],[33,34,36,48,35,44,47,84,103,85,107,2,64,63,70,74,12,13,65,81,22,25,26,29,30,82,59])).
% 182.27/182.32 cnf(114,plain,
% 182.27/182.32 (P4(a1,a9)),
% 182.27/182.32 inference(scs_inference,[],[33,34,36,48,35,44,47,84,103,85,107,2,64,63,70,74,12,13,65,81,22,25,26,29,30,82,59,55])).
% 182.27/182.32 cnf(116,plain,
% 182.27/182.32 (~E(f2(a1,a9),f2(a1,a5))),
% 182.27/182.32 inference(scs_inference,[],[33,34,36,48,35,44,47,84,103,85,107,2,64,63,70,74,12,13,65,81,22,25,26,29,30,82,59,55,3])).
% 182.27/182.32 cnf(118,plain,
% 182.27/182.32 (~E(a9,a5)),
% 182.27/182.32 inference(scs_inference,[],[33,34,36,48,35,44,47,84,103,85,107,2,64,63,70,74,12,13,65,81,22,25,26,29,30,82,59,55,3,10,20])).
% 182.27/182.32 cnf(130,plain,
% 182.27/182.32 (~P2(a6,f2(a1,a9))),
% 182.27/182.32 inference(scs_inference,[],[37,48,64,65])).
% 182.27/182.32 cnf(132,plain,
% 182.27/182.32 (P2(a10,f2(a1,a5))),
% 182.27/182.32 inference(scs_inference,[],[37,48,86,64,65,13])).
% 182.27/182.32 cnf(148,plain,
% 182.27/182.32 (~P2(a7,f2(a1,a9))),
% 182.27/182.32 inference(scs_inference,[],[47,130,59,64])).
% 182.27/182.32 cnf(152,plain,
% 182.27/182.32 (P2(a17,f2(a1,a5))),
% 182.27/182.32 inference(scs_inference,[],[47,43,86,96,130,59,64,65,13])).
% 182.27/182.32 cnf(162,plain,
% 182.27/182.32 (~P2(a10,f2(a1,a9))),
% 182.27/182.32 inference(scs_inference,[],[48,148,59,64])).
% 182.27/182.32 cnf(164,plain,
% 182.27/182.32 (P2(a14,a16)),
% 182.27/182.32 inference(scs_inference,[],[48,148,38,39,59,64,65])).
% 182.27/182.32 cnf(166,plain,
% 182.27/182.32 (~E(a6,f2(a1,a9))),
% 182.27/182.32 inference(scs_inference,[],[48,37,148,38,39,59,64,65,13])).
% 182.27/182.32 cnf(168,plain,
% 182.27/182.32 (P13(a6,f2(a1,a9))),
% 182.27/182.32 inference(scs_inference,[],[48,37,86,148,38,39,130,59,64,65,13,32,54])).
% 182.27/182.32 cnf(175,plain,
% 182.27/182.32 (~P2(a17,f2(a1,a9))),
% 182.27/182.32 inference(scs_inference,[],[49,162,59,64])).
% 182.27/182.32 cnf(178,plain,
% 182.27/182.32 (P2(a12,a11)),
% 182.27/182.32 inference(scs_inference,[],[49,86,162,168,40,42,59,64,27,65])).
% 182.27/182.32 cnf(180,plain,
% 182.27/182.32 (~E(f2(a1,a5),f2(a1,a9))),
% 182.27/182.32 inference(scs_inference,[],[49,86,152,162,168,40,42,59,64,27,65,13])).
% 182.27/182.32 cnf(194,plain,
% 182.27/182.32 (~P2(a6,a17)),
% 182.27/182.32 inference(scs_inference,[],[43,175,59,64])).
% 182.27/182.32 cnf(196,plain,
% 182.27/182.32 (P2(a12,a16)),
% 182.27/182.32 inference(scs_inference,[],[43,175,41,164,59,64,65])).
% 182.27/182.32 cnf(208,plain,
% 182.27/182.32 (~P13(a17,a6)),
% 182.27/182.32 inference(scs_inference,[],[194,59])).
% 182.27/182.32 cnf(210,plain,
% 182.27/182.32 (~P2(f2(a1,a5),a17)),
% 182.27/182.32 inference(scs_inference,[],[152,194,59,64])).
% 182.27/182.32 cnf(221,plain,
% 182.27/182.32 (~P2(f2(a1,a5),a10)),
% 182.27/182.32 inference(scs_inference,[],[132,210,59,64])).
% 182.27/182.32 cnf(230,plain,
% 182.27/182.32 (~P2(f2(a1,a5),a7)),
% 182.27/182.32 inference(scs_inference,[],[96,221,59,64])).
% 182.27/182.32 cnf(232,plain,
% 182.27/182.32 (~P2(f2(a1,a5),f2(a1,a9))),
% 182.27/182.32 inference(scs_inference,[],[48,96,221,59,64,65])).
% 182.27/182.33 cnf(241,plain,
% 182.27/182.33 (~P13(f2(a1,a9),f2(a1,a5))),
% 182.27/182.33 inference(scs_inference,[],[232,59])).
% 182.27/182.33 cnf(243,plain,
% 182.27/182.33 (~P2(a16,a14)),
% 182.27/182.33 inference(scs_inference,[],[164,232,59,64])).
% 182.27/182.33 cnf(245,plain,
% 182.27/182.33 (~P2(a16,a12)),
% 182.27/182.33 inference(scs_inference,[],[164,232,41,59,64,65])).
% 182.27/182.33 cnf(247,plain,
% 182.27/182.33 (~E(a12,a16)),
% 182.27/182.33 inference(scs_inference,[],[164,232,41,59,64,65,12])).
% 182.27/182.33 cnf(258,plain,
% 182.27/182.33 (~P2(a16,a11)),
% 182.27/182.33 inference(scs_inference,[],[38,230,59,64])).
% 182.27/182.33 cnf(260,plain,
% 182.27/182.33 (~E(a14,a16)),
% 182.27/182.33 inference(scs_inference,[],[38,39,230,59,64,12])).
% 182.27/182.33 cnf(267,plain,
% 182.27/182.33 (~P13(a12,a16)),
% 182.27/182.33 inference(scs_inference,[],[245,59])).
% 182.27/182.33 cnf(269,plain,
% 182.27/182.33 (~P2(a11,a15)),
% 182.27/182.33 inference(scs_inference,[],[40,245,59,64])).
% 182.27/182.33 cnf(271,plain,
% 182.27/182.33 (P2(a15,a16)),
% 182.27/182.33 inference(scs_inference,[],[40,38,245,59,64,65])).
% 182.27/182.33 cnf(273,plain,
% 182.27/182.33 (~E(a16,a15)),
% 182.27/182.33 inference(scs_inference,[],[40,38,245,59,64,65,13])).
% 182.27/182.33 cnf(274,plain,
% 182.27/182.33 (~E(a15,a16)),
% 182.27/182.33 inference(scs_inference,[],[40,38,245,258,59,64,65,13,12])).
% 182.27/182.33 cnf(275,plain,
% 182.27/182.33 (E(a16,a12)+P13(a16,a12)),
% 182.27/182.33 inference(scs_inference,[],[40,38,245,258,59,64,65,13,12,54])).
% 182.27/182.33 cnf(278,plain,
% 182.27/182.33 (~P13(a14,a16)),
% 182.27/182.33 inference(scs_inference,[],[243,59])).
% 182.27/182.33 cnf(280,plain,
% 182.27/182.33 (~P2(a11,a14)),
% 182.27/182.33 inference(scs_inference,[],[39,243,59,64])).
% 182.27/182.33 cnf(282,plain,
% 182.27/182.33 (~P2(a11,a12)),
% 182.27/182.33 inference(scs_inference,[],[39,243,269,42,59,64,65])).
% 182.27/182.33 cnf(285,plain,
% 182.27/182.33 (E(a16,a14)+P13(a16,a14)),
% 182.27/182.33 inference(scs_inference,[],[39,243,269,42,59,64,65,12,54])).
% 182.27/182.33 cnf(293,plain,
% 182.27/182.33 (~P2(a14,a12)),
% 182.27/182.33 inference(scs_inference,[],[41,280,59,64])).
% 182.27/182.33 cnf(295,plain,
% 182.27/182.33 (~E(a16,a12)),
% 182.27/182.33 inference(scs_inference,[],[164,41,280,59,64,13])).
% 182.27/182.33 cnf(296,plain,
% 182.27/182.33 (P13(a16,a12)),
% 182.27/182.33 inference(scs_inference,[],[164,41,280,59,64,13,275])).
% 182.27/182.33 cnf(304,plain,
% 182.27/182.33 (~P2(a15,a12)),
% 182.27/182.33 inference(scs_inference,[],[42,282,59,64])).
% 182.27/182.33 cnf(306,plain,
% 182.27/182.33 (~E(a11,a12)),
% 182.27/182.33 inference(scs_inference,[],[39,42,282,293,59,64,13])).
% 182.27/182.33 cnf(307,plain,
% 182.27/182.33 (P13(a11,a12)),
% 182.27/182.33 inference(scs_inference,[],[39,42,282,293,59,64,13,54])).
% 182.27/182.33 cnf(321,plain,
% 182.27/182.33 (~P2(a16,a15)),
% 182.27/182.33 inference(scs_inference,[],[271,304,59,64])).
% 182.27/182.33 cnf(332,plain,
% 182.27/182.33 (~P13(a15,a16)),
% 182.27/182.33 inference(scs_inference,[],[321,59])).
% 182.27/182.33 cnf(343,plain,
% 182.27/182.33 (~P13(a11,a16)),
% 182.27/182.33 inference(scs_inference,[],[258,59])).
% 182.27/182.33 cnf(372,plain,
% 182.27/182.33 (~E(a6,a17)+~E(a17,a6)),
% 182.27/182.33 inference(scs_inference,[],[43,194,12,13])).
% 182.27/182.33 cnf(436,plain,
% 182.27/182.33 (P13(a16,a14)),
% 182.27/182.33 inference(scs_inference,[],[38,280,13,285])).
% 182.27/182.33 cnf(441,plain,
% 182.27/182.33 (E(f13(a1,a8),a16)),
% 182.27/182.33 inference(scs_inference,[],[33,91,51,62])).
% 182.27/182.33 cnf(442,plain,
% 182.27/182.33 (E(a16,f13(a1,a8))),
% 182.27/182.33 inference(scs_inference,[],[441,2])).
% 182.27/182.33 cnf(443,plain,
% 182.27/182.33 (~E(a15,f13(a1,a8))),
% 182.27/182.33 inference(scs_inference,[],[274,441,2,3])).
% 182.27/182.33 cnf(445,plain,
% 182.27/182.33 (P2(a12,f13(a1,a8))),
% 182.27/182.33 inference(scs_inference,[],[274,441,196,296,2,3,27,13])).
% 182.27/182.33 cnf(446,plain,
% 182.27/182.33 (~P2(f13(a1,a8),a12)),
% 182.27/182.33 inference(scs_inference,[],[274,441,196,296,2,3,27,13,64])).
% 182.27/182.33 cnf(448,plain,
% 182.27/182.33 (~P2(x4481,a12)+P2(x4481,f13(a1,a8))),
% 182.27/182.33 inference(scs_inference,[],[274,441,196,296,2,3,27,13,64,65])).
% 182.27/182.33 cnf(450,plain,
% 182.27/182.33 (~P13(a12,f13(a1,a8))),
% 182.27/182.33 inference(scs_inference,[],[274,441,196,296,2,3,27,13,64,65,59])).
% 182.27/182.33 cnf(458,plain,
% 182.27/182.33 (~E(a12,f13(a1,a8))),
% 182.27/182.33 inference(scs_inference,[],[247,441,3])).
% 182.27/182.33 cnf(506,plain,
% 182.27/182.33 (P2(x5061,f13(a1,a8))+~E(a12,x5061)),
% 182.27/182.33 inference(scs_inference,[],[445,12])).
% 182.27/182.33 cnf(605,plain,
% 182.27/182.33 (~E(a6,a17)),
% 182.27/182.33 inference(scs_inference,[],[372,2])).
% 182.27/182.33 cnf(622,plain,
% 182.27/182.33 (~E(a14,f13(a1,a8))),
% 182.27/182.33 inference(scs_inference,[],[441,260,3])).
% 182.27/182.33 cnf(708,plain,
% 182.27/182.33 (P6(x7081,x7081)),
% 182.27/182.33 inference(rename_variables,[],[85])).
% 182.27/182.33 cnf(709,plain,
% 182.27/182.33 (P6(a16,f13(a1,a8))),
% 182.27/182.33 inference(scs_inference,[],[441,85,708,30,29])).
% 182.27/182.33 cnf(998,plain,
% 182.27/182.33 (~E(f13(a1,a5),f13(a1,a8))+~P2(f13(a1,a9),f13(a1,a8))),
% 182.27/182.33 inference(scs_inference,[],[80,2])).
% 182.27/182.33 cnf(1273,plain,
% 182.27/182.33 (E(f2(a16,x12731),f2(f13(a1,a8),x12731))),
% 182.27/182.33 inference(scs_inference,[],[441,2,4])).
% 182.27/182.33 cnf(1274,plain,
% 182.27/182.33 (E(f2(f13(a1,a8),x12741),f2(a16,x12741))),
% 182.27/182.33 inference(scs_inference,[],[1273,2])).
% 182.27/182.33 cnf(1292,plain,
% 182.27/182.33 (E(f2(a6,x12921),f2(f2(a1,a5),x12921))),
% 182.27/182.33 inference(scs_inference,[],[35,2,4])).
% 182.27/182.33 cnf(1293,plain,
% 182.27/182.33 (E(f2(f2(a1,a5),x12931),f2(a6,x12931))),
% 182.27/182.33 inference(scs_inference,[],[1292,2])).
% 182.27/182.33 cnf(1319,plain,
% 182.27/182.33 (E(f2(f2(f2(a1,a5),x13191),x13192),f2(f2(a6,x13191),x13192))),
% 182.27/182.33 inference(scs_inference,[],[1292,2,4])).
% 182.27/182.33 cnf(1328,plain,
% 182.27/182.33 (E(f2(x13281,f2(f2(a1,a5),x13282)),f2(x13281,f2(a6,x13282)))),
% 182.27/182.33 inference(scs_inference,[],[1292,2,5])).
% 182.27/182.33 cnf(1329,plain,
% 182.27/182.33 (E(f13(f2(a6,x13291),x13292),f13(f2(f2(a1,a5),x13291),x13292))),
% 182.27/182.33 inference(scs_inference,[],[1293,2,6])).
% 182.27/182.33 cnf(1330,plain,
% 182.27/182.33 (E(f13(x13301,a6),f13(x13301,f2(a1,a5)))),
% 182.27/182.33 inference(scs_inference,[],[35,2,7])).
% 182.27/182.33 cnf(1331,plain,
% 182.27/182.33 (E(f13(x13311,f2(a1,a5)),f13(x13311,a6))),
% 182.27/182.33 inference(scs_inference,[],[1330,2])).
% 182.27/182.33 cnf(1357,plain,
% 182.27/182.33 (E(f13(a6,x13571),f13(f2(a1,a5),x13571))),
% 182.27/182.33 inference(scs_inference,[],[35,2,6])).
% 182.27/182.33 cnf(1358,plain,
% 182.27/182.33 (E(f13(f2(a1,a5),x13581),f13(a6,x13581))),
% 182.27/182.33 inference(scs_inference,[],[1357,2])).
% 182.27/182.33 cnf(1359,plain,
% 182.27/182.33 (E(f13(a6,f2(a1,a5)),f13(f2(a1,a5),a6))),
% 182.27/182.33 inference(scs_inference,[],[1331,1357,2,3])).
% 182.27/182.33 cnf(1370,plain,
% 182.27/182.33 (E(f13(a6,a6),f13(f2(a1,a5),f2(a1,a5)))),
% 182.27/182.33 inference(scs_inference,[],[1330,1359,1357,2,3])).
% 182.27/182.33 cnf(1473,plain,
% 182.27/182.33 (P6(f13(a6,x14731),f13(f2(a1,a5),x14731))),
% 182.27/182.33 inference(scs_inference,[],[1357,85,30])).
% 182.27/182.33 cnf(1474,plain,
% 182.27/182.33 (P6(x14741,x14741)),
% 182.27/182.33 inference(rename_variables,[],[85])).
% 182.27/182.33 cnf(1475,plain,
% 182.27/182.33 (P6(f13(f2(a1,a5),x14751),f13(a6,x14751))),
% 182.27/182.33 inference(scs_inference,[],[1357,85,1474,30,29])).
% 182.27/182.33 cnf(1478,plain,
% 182.27/182.33 (P10(x14781,x14781)),
% 182.27/182.33 inference(rename_variables,[],[84])).
% 182.27/182.33 cnf(1479,plain,
% 182.27/182.33 (P10(f13(f2(a1,a5),x14791),f13(a6,x14791))),
% 182.27/182.33 inference(scs_inference,[],[1357,85,1474,84,1478,30,29,26,25])).
% 182.27/182.33 cnf(1642,plain,
% 182.27/182.33 (E(f13(x16421,f13(f2(a1,a5),f2(a1,a5))),f13(x16421,f13(a6,a6)))),
% 182.27/182.33 inference(scs_inference,[],[1370,2,7])).
% 182.27/182.33 cnf(1644,plain,
% 182.27/182.33 (E(f3(a6),f3(f2(a1,a5)))),
% 182.27/182.33 inference(scs_inference,[],[35,2,9])).
% 182.27/182.33 cnf(1671,plain,
% 182.27/182.33 (E(f2(f3(f2(a1,a5)),x16711),f2(f3(a6),x16711))),
% 182.27/182.33 inference(scs_inference,[],[1644,2,4])).
% 182.27/182.33 cnf(1673,plain,
% 182.27/182.33 (E(f2(x16731,a6),f2(x16731,f2(a1,a5)))),
% 182.27/182.33 inference(scs_inference,[],[35,2,5])).
% 182.27/182.33 cnf(1785,plain,
% 182.27/182.33 (E(f2(a6,a6),f2(f2(a1,a5),f2(a1,a5)))),
% 182.27/182.33 inference(scs_inference,[],[1673,1292,3])).
% 182.27/182.33 cnf(2018,plain,
% 182.27/182.33 (E(f3(a16),f3(f13(a1,a8)))),
% 182.27/182.33 inference(scs_inference,[],[436,178,442,56,58,8,9])).
% 182.27/182.33 cnf(2019,plain,
% 182.27/182.33 (E(f13(a16,x20191),f13(f13(a1,a8),x20191))),
% 182.27/182.33 inference(scs_inference,[],[436,178,442,56,58,8,9,6])).
% 182.27/182.33 cnf(2020,plain,
% 182.27/182.33 (E(f13(x20201,a16),f13(x20201,f13(a1,a8)))),
% 182.27/182.33 inference(scs_inference,[],[436,178,442,56,58,8,9,6,7])).
% 182.27/182.33 cnf(2021,plain,
% 182.27/182.33 (P13(f2(a1,a5),a10)),
% 182.27/182.33 inference(scs_inference,[],[436,178,132,442,56,58,8,9,6,7,57])).
% 182.27/182.33 cnf(2023,plain,
% 182.27/182.33 (E(f2(x20231,a16),f2(x20231,f13(a1,a8)))),
% 182.27/182.33 inference(scs_inference,[],[436,178,132,442,56,58,8,9,6,7,57,5])).
% 182.27/182.33 cnf(2025,plain,
% 182.27/182.33 (~P2(f2(a1,a8),a7)),
% 182.27/182.33 inference(scs_inference,[],[101,436,178,132,33,442,91,56,58,8,9,6,7,57,5,2,74])).
% 182.27/182.33 cnf(2027,plain,
% 182.27/182.33 (~P9(a1,a9)),
% 182.27/182.33 inference(scs_inference,[],[101,436,178,132,33,442,91,110,89,56,58,8,9,6,7,57,5,2,74,81])).
% 182.27/182.33 cnf(2035,plain,
% 182.27/182.33 (~E(f13(a1,a8),a12)),
% 182.27/182.33 inference(scs_inference,[],[101,295,458,450,321,436,273,178,132,33,93,442,91,110,89,56,58,8,9,6,7,57,5,2,74,81,70,60,61,3])).
% 182.27/182.33 cnf(2036,plain,
% 182.27/182.33 (~P13(a15,f13(a1,a8))),
% 182.27/182.33 inference(scs_inference,[],[101,295,458,450,332,321,436,273,178,132,33,93,442,91,441,110,89,56,58,8,9,6,7,57,5,2,74,81,70,60,61,3,28])).
% 182.27/182.33 cnf(2041,plain,
% 182.27/182.33 (P10(x20411,x20411)),
% 182.27/182.33 inference(rename_variables,[],[84])).
% 182.27/182.33 cnf(2044,plain,
% 182.27/182.33 (P2(a15,f13(a1,a8))),
% 182.27/182.33 inference(scs_inference,[],[101,295,458,450,332,709,321,436,273,178,271,132,84,2041,33,93,442,91,441,110,89,56,58,8,9,6,7,57,5,2,74,81,70,60,61,3,28,30,29,12,26,25,13])).
% 182.27/182.33 cnf(2053,plain,
% 182.27/182.34 (P2(a14,f13(a1,a8))),
% 182.27/182.34 inference(scs_inference,[],[34,101,295,458,450,332,1785,709,321,436,273,178,271,132,84,2041,33,93,442,91,441,110,89,56,58,8,9,6,7,57,5,2,74,81,70,60,61,3,28,30,29,12,26,25,13,76,52,53,17,27,59])).
% 182.27/182.34 cnf(2055,plain,
% 182.27/182.34 (~P2(f13(a1,a8),a14)),
% 182.27/182.34 inference(scs_inference,[],[34,101,295,458,450,332,1785,709,321,436,273,178,271,132,84,2041,33,93,442,91,441,110,89,56,58,8,9,6,7,57,5,2,74,81,70,60,61,3,28,30,29,12,26,25,13,76,52,53,17,27,59,64])).
% 182.27/182.34 cnf(2061,plain,
% 182.27/182.34 (P10(f13(x20611,a16),f13(x20611,f13(a1,a8)))),
% 182.27/182.34 inference(scs_inference,[],[2020,52])).
% 182.27/182.34 cnf(2063,plain,
% 182.27/182.34 (P13(f13(a1,a8),a15)),
% 182.27/182.34 inference(scs_inference,[],[2044,2020,52,57])).
% 182.27/182.34 cnf(2071,plain,
% 182.27/182.34 (E(f3(f13(a1,a8)),f3(a16))),
% 182.27/182.34 inference(scs_inference,[],[2021,2044,2020,441,52,57,53,56,58,9])).
% 182.27/182.34 cnf(2072,plain,
% 182.27/182.34 (E(f13(f13(a1,a8),x20721),f13(a16,x20721))),
% 182.27/182.34 inference(scs_inference,[],[2021,2044,2020,441,52,57,53,56,58,9,6])).
% 182.27/182.34 cnf(2073,plain,
% 182.27/182.34 (E(f13(x20731,f13(a1,a8)),f13(x20731,a16))),
% 182.27/182.34 inference(scs_inference,[],[2021,2044,2020,441,52,57,53,56,58,9,6,7])).
% 182.27/182.34 cnf(2074,plain,
% 182.27/182.34 (E(f4(f13(a1,a8)),f4(a16))),
% 182.27/182.34 inference(scs_inference,[],[2021,2044,2020,441,52,57,53,56,58,9,6,7,8])).
% 182.27/182.34 cnf(2075,plain,
% 182.27/182.34 (E(f2(x20751,f13(a1,a8)),f2(x20751,a16))),
% 182.27/182.34 inference(scs_inference,[],[2021,2044,2020,441,52,57,53,56,58,9,6,7,8,5])).
% 182.27/182.34 cnf(2076,plain,
% 182.27/182.34 (~E(a17,a6)),
% 182.27/182.34 inference(scs_inference,[],[605,2021,2044,2020,441,52,57,53,56,58,9,6,7,8,5,2])).
% 182.27/182.34 cnf(2077,plain,
% 182.27/182.34 (~P10(a15,f13(a1,a8))),
% 182.27/182.34 inference(scs_inference,[],[605,443,2021,2044,2036,2020,441,52,57,53,56,58,9,6,7,8,5,2,60])).
% 182.27/182.34 cnf(2081,plain,
% 182.27/182.34 (E(f13(a16,a16),f13(f13(a1,a8),f13(a1,a8)))),
% 182.27/182.34 inference(scs_inference,[],[306,605,443,2021,2044,2036,2020,2019,282,441,52,57,53,56,58,9,6,7,8,5,2,60,61,3])).
% 182.27/182.34 cnf(2082,plain,
% 182.27/182.34 (E(f13(x20821,a16),f13(x20821,f13(a1,a8)))),
% 182.27/182.34 inference(rename_variables,[],[2020])).
% 182.27/182.34 cnf(2084,plain,
% 182.27/182.34 (~P13(a14,f13(a1,a8))),
% 182.27/182.34 inference(scs_inference,[],[306,605,443,2021,2044,2036,2020,278,2019,282,441,52,57,53,56,58,9,6,7,8,5,2,60,61,3,28])).
% 182.27/182.34 cnf(2088,plain,
% 182.27/182.34 (E(f13(x20881,a16),f13(x20881,f13(a1,a8)))),
% 182.27/182.34 inference(rename_variables,[],[2020])).
% 182.27/182.34 cnf(2097,plain,
% 182.27/182.34 (~P2(f2(a1,a8),f2(a1,a9))),
% 182.27/182.34 inference(scs_inference,[],[118,306,605,443,2021,2044,2036,2025,2020,2082,2088,2018,278,1475,1479,2019,282,84,85,441,47,52,57,53,56,58,9,6,7,8,5,2,60,61,3,28,30,29,26,25,54,65])).
% 182.27/182.34 cnf(2108,plain,
% 182.27/182.34 (P10(f13(f13(a1,a8),x21081),f13(a16,x21081))),
% 182.27/182.34 inference(scs_inference,[],[2063,2072,56,52])).
% 182.27/182.34 cnf(2112,plain,
% 182.27/182.34 (P13(f2(a1,a5),a7)),
% 182.27/182.34 inference(scs_inference,[],[2063,2072,2053,96,56,52,58,57])).
% 182.27/182.34 cnf(2114,plain,
% 182.27/182.34 (P6(f13(f13(a1,a8),x21141),f13(a16,x21141))),
% 182.27/182.34 inference(scs_inference,[],[2063,2072,2053,96,56,52,58,57,53])).
% 182.27/182.34 cnf(2118,plain,
% 182.27/182.34 (~P10(a14,f13(a1,a8))),
% 182.27/182.34 inference(scs_inference,[],[622,2063,2084,2072,2053,96,86,56,52,58,57,53,8,2,60])).
% 182.27/182.34 cnf(2126,plain,
% 182.27/182.34 (~P10(a15,a16)),
% 182.27/182.34 inference(scs_inference,[],[622,2063,2077,2084,2072,2073,2053,2055,96,442,86,56,52,58,57,53,8,2,60,61,3,29,26])).
% 182.27/182.34 cnf(2140,plain,
% 182.27/182.34 (P10(f2(a1,a5),a7)),
% 182.27/182.34 inference(scs_inference,[],[2112,56])).
% 182.27/182.34 cnf(2142,plain,
% 182.27/182.34 (P13(a11,a15)),
% 182.27/182.34 inference(scs_inference,[],[2112,40,56,57])).
% 182.27/182.34 cnf(2150,plain,
% 182.27/182.34 (E(f4(f2(a1,a5)),f4(a6))),
% 182.27/182.34 inference(scs_inference,[],[2112,2071,271,40,35,56,57,52,53,58,8])).
% 182.27/182.34 cnf(2174,plain,
% 182.27/182.34 (P6(f13(a16,a16),f13(f13(a1,a8),f13(a1,a8)))),
% 182.27/182.34 inference(scs_inference,[],[2081,53])).
% 182.27/182.34 cnf(2180,plain,
% 182.27/182.34 (P13(a11,a14)),
% 182.27/182.34 inference(scs_inference,[],[2142,2081,152,39,53,56,58,57])).
% 182.27/182.34 cnf(2188,plain,
% 182.27/182.34 (E(f2(f13(a1,a8),f13(a1,a8)),f2(a16,a16))),
% 182.27/182.34 inference(scs_inference,[],[2142,2150,2081,2035,267,446,2075,247,152,39,1274,53,56,58,57,52,60,61,3])).
% 182.27/182.34 cnf(2191,plain,
% 182.27/182.34 (~P6(a16,a12)),
% 182.27/182.34 inference(scs_inference,[],[2142,2150,2081,2035,267,446,2075,247,152,39,1274,442,53,56,58,57,52,60,61,3,29])).
% 182.27/182.34 cnf(2198,plain,
% 182.27/182.34 (P13(a6,a7)),
% 182.27/182.34 inference(scs_inference,[],[2188,36,53,57])).
% 182.27/182.34 cnf(2206,plain,
% 182.27/182.34 (~P10(a17,a6)),
% 182.27/182.34 inference(scs_inference,[],[2180,2188,2076,208,132,36,53,57,56,52,58,60])).
% 182.27/182.34 cnf(2208,plain,
% 182.27/182.34 (~P6(a6,a17)),
% 182.27/182.34 inference(scs_inference,[],[2180,2188,2076,605,208,132,36,194,53,57,56,52,58,60,61])).
% 182.27/182.34 cnf(2210,plain,
% 182.27/182.34 (E(f2(a6,a16),f2(f2(a1,a5),f13(a1,a8)))),
% 182.27/182.34 inference(scs_inference,[],[2180,2188,2076,2023,605,208,132,36,1292,194,53,57,56,52,58,60,61,3])).
% 182.27/182.34 cnf(2231,plain,
% 182.27/182.34 (P13(a6,a10)),
% 182.27/182.34 inference(scs_inference,[],[2210,37,52,53,57])).
% 182.27/182.34 cnf(2241,plain,
% 182.27/182.34 (E(f13(a16,a6),f13(f13(a1,a8),f2(a1,a5)))),
% 182.27/182.34 inference(scs_inference,[],[2198,2210,241,232,2019,180,116,96,37,1330,52,53,57,58,56,60,61,3])).
% 182.27/182.34 cnf(2248,plain,
% 182.27/182.34 (~E(f2(a1,a9),f2(a1,a8))),
% 182.27/182.34 inference(scs_inference,[],[2198,2208,2114,2210,241,2025,232,2073,2019,180,116,96,37,1330,47,35,52,53,57,58,56,60,61,3,30,29,12])).
% 182.27/182.34 cnf(2250,plain,
% 182.27/182.34 (~E(f2(a1,a8),f2(a1,a9))),
% 182.27/182.34 inference(scs_inference,[],[2198,2206,2208,2114,2210,241,2025,232,2073,2019,180,116,96,37,1330,47,35,52,53,57,58,56,60,61,3,30,29,12,26,2])).
% 182.27/182.34 cnf(2265,plain,
% 182.27/182.34 (P13(a17,f2(a1,a9))),
% 182.27/182.34 inference(scs_inference,[],[2231,2241,40,49,58,52,53,56,57])).
% 182.27/182.34 cnf(2286,plain,
% 182.27/182.34 (P6(a14,a11)),
% 182.27/182.34 inference(scs_inference,[],[2265,2074,39,53,52,56,58])).
% 182.27/182.34 cnf(2288,plain,
% 182.27/182.34 (P13(a15,a12)),
% 182.27/182.34 inference(scs_inference,[],[2265,2074,39,42,53,52,56,58,57])).
% 182.27/182.34 cnf(2290,plain,
% 182.27/182.34 (P13(f2(a1,a8),f2(a1,a9))),
% 182.27/182.34 inference(scs_inference,[],[2265,2074,2250,2097,39,42,53,52,56,58,57,54])).
% 182.27/182.34 cnf(2294,plain,
% 182.27/182.34 (P2(f2(a1,a9),f2(a1,a8))),
% 182.27/182.34 inference(scs_inference,[],[2265,2074,2250,166,2097,130,39,42,53,52,56,58,57,54,61,59])).
% 182.27/182.34 cnf(2308,plain,
% 182.27/182.34 (P6(f2(x23081,a16),f2(x23081,f13(a1,a8)))),
% 182.27/182.34 inference(scs_inference,[],[2288,2294,2081,2023,56,52,58,53])).
% 182.27/182.34 cnf(2310,plain,
% 182.27/182.34 (P13(a14,a12)),
% 182.27/182.34 inference(scs_inference,[],[2288,2294,2081,2023,41,56,52,58,53,57])).
% 182.27/182.34 cnf(2312,plain,
% 182.27/182.34 (E(f2(a16,a16),f2(f13(a1,a8),f13(a1,a8)))),
% 182.27/182.34 inference(scs_inference,[],[2288,2294,2081,2023,41,1273,56,52,58,53,57,3])).
% 182.27/182.34 cnf(2333,plain,
% 182.27/182.34 (P13(a16,a11)),
% 182.27/182.34 inference(scs_inference,[],[2310,2312,164,38,58,52,53,56,57])).
% 182.27/182.34 cnf(2337,plain,
% 182.27/182.34 (~P10(f2(a1,a9),f2(a1,a8))+P13(f2(a1,a9),f2(a1,a8))),
% 182.27/182.34 inference(scs_inference,[],[2310,2312,2174,2248,2073,164,38,58,52,53,56,57,30,60])).
% 182.27/182.34 cnf(2349,plain,
% 182.27/182.34 (P6(f2(x23491,f13(a1,a8)),f2(x23491,a16))),
% 182.27/182.34 inference(scs_inference,[],[2075,53])).
% 182.27/182.34 cnf(2355,plain,
% 182.27/182.34 (P10(f2(x23551,f13(a1,a8)),f2(x23551,a16))),
% 182.27/182.34 inference(scs_inference,[],[2333,2075,36,53,56,58,52])).
% 182.27/182.34 cnf(2360,plain,
% 182.27/182.34 (P2(a11,f13(a1,a8))),
% 182.27/182.34 inference(scs_inference,[],[2333,2075,36,48,442,53,56,58,52,57,27,59])).
% 182.27/182.34 cnf(2381,plain,
% 182.27/182.34 (P10(f13(a16,x23811),f13(f13(a1,a8),x23811))),
% 182.27/182.34 inference(scs_inference,[],[2360,2019,58,52])).
% 182.27/182.34 cnf(2425,plain,
% 182.27/182.34 (P10(f13(x24251,f13(a1,a8)),f13(x24251,a16))),
% 182.27/182.34 inference(scs_inference,[],[2073,43,58,52])).
% 182.27/182.34 cnf(2427,plain,
% 182.27/182.34 (P6(f13(x24271,f13(a1,a8)),f13(x24271,a16))),
% 182.27/182.34 inference(scs_inference,[],[2073,43,58,52,53])).
% 182.27/182.34 cnf(2781,plain,
% 182.27/182.34 (~P13(x27811,f13(a1,a8))+~E(x27811,a14)),
% 182.27/182.34 inference(scs_inference,[],[2084,27])).
% 182.27/182.34 cnf(2852,plain,
% 182.27/182.34 (~P2(f13(a1,a8),x28521)+~E(x28521,a14)),
% 182.27/182.34 inference(scs_inference,[],[2055,13])).
% 182.27/182.34 cnf(2988,plain,
% 182.27/182.34 (~P13(x29881,a16)+~E(x29881,a14)),
% 182.27/182.34 inference(scs_inference,[],[278,27])).
% 182.27/182.34 cnf(3122,plain,
% 182.27/182.34 (~P2(a16,x31221)+~E(x31221,a14)),
% 182.27/182.34 inference(scs_inference,[],[243,13])).
% 182.27/182.34 cnf(3525,plain,
% 182.27/182.34 (~E(a7,x35251)+~P13(x35251,a6)),
% 182.27/182.34 inference(scs_inference,[],[112,27,2])).
% 182.27/182.34 cnf(3796,plain,
% 182.27/182.34 (P12(a1,a9)+E(f13(a1,a9),a12)),
% 182.27/182.34 inference(scs_inference,[],[2027,114,67])).
% 182.27/182.34 cnf(3798,plain,
% 182.27/182.34 (E(f13(a1,a9),a14)+E(f13(a1,a9),a12)),
% 182.27/182.34 inference(scs_inference,[],[2027,114,67,68])).
% 182.27/182.34 cnf(3800,plain,
% 182.27/182.34 (~P2(f13(a1,a8),f13(a1,a9))+E(f13(a1,a9),a12)),
% 182.27/182.34 inference(scs_inference,[],[2027,114,67,68,2852])).
% 182.27/182.34 cnf(3801,plain,
% 182.27/182.34 (~P13(f13(a1,a9),f13(a1,a8))+E(f13(a1,a9),a12)),
% 182.27/182.34 inference(scs_inference,[],[2027,114,67,68,2852,2781])).
% 182.27/182.34 cnf(3802,plain,
% 182.27/182.34 (~P13(f13(a1,a9),a16)+E(f13(a1,a9),a12)),
% 182.27/182.34 inference(scs_inference,[],[2027,114,67,68,2852,2781,2988])).
% 182.27/182.34 cnf(3803,plain,
% 182.27/182.34 (~P2(a16,f13(a1,a9))+E(f13(a1,a9),a12)),
% 182.27/182.34 inference(scs_inference,[],[2027,114,67,68,2852,2781,2988,3122])).
% 182.27/182.34 cnf(3804,plain,
% 182.27/182.34 (P6(f13(a1,a9),a14)+E(f13(a1,a9),a12)),
% 182.27/182.34 inference(scs_inference,[],[2027,114,67,68,2852,2781,2988,3122,53])).
% 182.27/182.34 cnf(3806,plain,
% 182.27/182.34 (P10(f13(a1,a9),a14)+E(f13(a1,a9),a12)),
% 182.27/182.34 inference(scs_inference,[],[2027,114,67,68,2852,2781,2988,3122,53,52])).
% 182.27/182.34 cnf(3808,plain,
% 182.27/182.34 (E(f13(f13(a1,a9),x38081),f13(a14,x38081))+E(f13(a1,a9),a12)),
% 182.27/182.34 inference(scs_inference,[],[2027,114,67,68,2852,2781,2988,3122,53,52,6])).
% 182.27/182.34 cnf(3809,plain,
% 182.27/182.34 (E(f3(f13(a1,a9)),f3(a14))+E(f13(a1,a9),a12)),
% 182.27/182.34 inference(scs_inference,[],[2027,114,67,68,2852,2781,2988,3122,53,52,6,9])).
% 182.27/182.34 cnf(3810,plain,
% 182.27/182.34 (E(f2(f13(a1,a9),x38101),f2(a14,x38101))+E(f13(a1,a9),a12)),
% 182.27/182.34 inference(scs_inference,[],[2027,114,67,68,2852,2781,2988,3122,53,52,6,9,4])).
% 182.27/182.34 cnf(3811,plain,
% 182.27/182.34 (E(f13(x38111,f13(a1,a9)),f13(x38111,a14))+E(f13(a1,a9),a12)),
% 182.27/182.34 inference(scs_inference,[],[2027,114,67,68,2852,2781,2988,3122,53,52,6,9,4,7])).
% 182.27/182.34 cnf(3812,plain,
% 182.27/182.34 (E(f4(f13(a1,a9)),f4(a14))+E(f13(a1,a9),a12)),
% 182.27/182.34 inference(scs_inference,[],[2027,114,67,68,2852,2781,2988,3122,53,52,6,9,4,7,8])).
% 182.27/182.34 cnf(3813,plain,
% 182.27/182.34 (E(f2(x38131,f13(a1,a9)),f2(x38131,a14))+E(f13(a1,a9),a12)),
% 182.27/182.34 inference(scs_inference,[],[2027,114,67,68,2852,2781,2988,3122,53,52,6,9,4,7,8,5])).
% 182.27/182.34 cnf(3814,plain,
% 182.27/182.34 (~P10(f13(a1,a9),f13(a1,a8))+E(f13(a1,a9),a12)),
% 182.27/182.34 inference(scs_inference,[],[2027,2118,114,67,68,2852,2781,2988,3122,53,52,6,9,4,7,8,5,25])).
% 182.27/182.34 cnf(3815,plain,
% 182.27/182.34 (P6(a14,f13(a1,a9))+E(f13(a1,a9),a12)),
% 182.27/182.34 inference(scs_inference,[],[2027,2118,85,114,67,68,2852,2781,2988,3122,53,52,6,9,4,7,8,5,25,29])).
% 182.27/182.34 cnf(3908,plain,
% 182.27/182.34 (E(a7,a6)+~P10(a7,a6)),
% 182.27/182.34 inference(scs_inference,[],[2072,112,1331,3,53,52,60])).
% 182.27/182.34 cnf(4462,plain,
% 182.27/182.34 (E(f13(x44621,f13(f2(a1,a5),f2(a1,a5))),f13(x44621,f13(a6,a6)))),
% 182.27/182.34 inference(rename_variables,[],[1642])).
% 182.27/182.34 cnf(4463,plain,
% 182.27/182.34 (P6(f13(a6,x44631),f13(f2(a1,a5),x44631))),
% 182.27/182.34 inference(rename_variables,[],[1473])).
% 182.27/182.34 cnf(4465,plain,
% 182.27/182.34 (E(f13(x44651,f13(f2(a1,a5),f2(a1,a5))),f13(x44651,f13(a6,a6)))),
% 182.27/182.34 inference(rename_variables,[],[1642])).
% 182.27/182.34 cnf(4466,plain,
% 182.27/182.34 (P10(f13(a16,x44661),f13(f13(a1,a8),x44661))),
% 182.27/182.34 inference(rename_variables,[],[2381])).
% 182.27/182.34 cnf(4467,plain,
% 182.27/182.34 (P10(f13(a16,f13(a6,a6)),f13(f13(a1,a8),f13(f2(a1,a5),f2(a1,a5))))),
% 182.27/182.34 inference(scs_inference,[],[2381,4466,1642,4462,4465,1473,53,52,6,4,9,7,8,5,30,26,25])).
% 182.27/182.34 cnf(4468,plain,
% 182.27/182.34 (E(f13(x44681,f13(f2(a1,a5),f2(a1,a5))),f13(x44681,f13(a6,a6)))),
% 182.27/182.34 inference(rename_variables,[],[1642])).
% 182.27/182.34 cnf(4470,plain,
% 182.27/182.34 (P6(f13(a6,f13(a6,a6)),f13(f2(a1,a5),f13(f2(a1,a5),f2(a1,a5))))),
% 182.27/182.34 inference(scs_inference,[],[2381,4466,1642,4462,4465,4468,1473,4463,53,52,6,4,9,7,8,5,30,26,25,29])).
% 182.27/182.34 cnf(4478,plain,
% 182.27/182.34 (P6(f2(f2(f2(a1,a5),x44781),x44782),f2(f2(a6,x44781),x44782))),
% 182.27/182.34 inference(scs_inference,[],[1319,53])).
% 182.27/182.34 cnf(4499,plain,
% 182.27/182.34 (P8(a1,a5)),
% 182.27/182.34 inference(scs_inference,[],[33,1273,2019,2097,2355,2427,2140,59,2337,26,30,70])).
% 182.27/182.34 cnf(4525,plain,
% 182.27/182.34 (E(f2(a16,f13(a1,a8)),f2(f13(a1,a8),a16))),
% 182.27/182.34 inference(scs_inference,[],[1330,1273,2019,2075,1319,2025,2425,2114,2,59,26,30,3])).
% 182.27/182.34 cnf(4545,plain,
% 182.27/182.34 (E(f13(a16,f13(a1,a8)),f13(f13(a1,a8),a16))),
% 182.27/182.34 inference(scs_inference,[],[1330,1273,2019,2073,1642,2108,2349,2,26,30,3])).
% 182.27/182.34 cnf(4557,plain,
% 182.27/182.34 (E(f13(f2(f2(a1,a5),x45571),x45572),f13(f2(a6,x45571),x45572))),
% 182.27/182.34 inference(scs_inference,[],[1329,2])).
% 182.27/182.34 cnf(4584,plain,
% 182.27/182.34 (E(f13(a16,f13(f2(a1,a5),f2(a1,a5))),f13(f13(a1,a8),f13(a6,a6)))),
% 182.27/182.34 inference(scs_inference,[],[2019,1673,2072,1642,4478,4545,4467,2,26,30,3])).
% 182.27/182.34 cnf(4586,plain,
% 182.27/182.34 (E(f13(a16,x45861),f13(f13(a1,a8),x45861))),
% 182.27/182.34 inference(rename_variables,[],[2019])).
% 182.27/182.34 cnf(4593,plain,
% 182.27/182.34 (P2(x45931,f13(a1,a8))+~E(a11,x45931)),
% 182.27/182.34 inference(scs_inference,[],[1273,2019,4586,1673,2072,1642,2360,4478,4545,2061,4467,2308,2,26,30,3,25,29,12])).
% 182.27/182.34 cnf(4607,plain,
% 182.27/182.34 (P6(f13(f2(a1,a5),f13(a6,a6)),f13(f2(a1,a5),f13(f2(a1,a5),f2(a1,a5))))),
% 182.27/182.34 inference(scs_inference,[],[1330,1357,1358,1329,4525,4470,2,30,3,29])).
% 182.27/182.34 cnf(4615,plain,
% 182.27/182.34 (~E(a7,a6)),
% 182.27/182.34 inference(scs_inference,[],[1330,2019,2072,1357,1358,112,1329,2198,4467,4525,4470,2,30,3,29,25,28,26,27,3525])).
% 182.27/182.34 cnf(4618,plain,
% 182.27/182.34 (~P10(a7,a6)),
% 182.27/182.34 inference(scs_inference,[],[4615,3908])).
% 182.27/182.34 cnf(4627,plain,
% 182.27/182.34 (P2(x46271,f13(a1,a8))+~E(a15,x46271)),
% 182.27/182.34 inference(scs_inference,[],[1330,1358,2044,2140,2290,4584,4557,4607,2,30,3,26,28,12])).
% 182.27/182.34 cnf(4646,plain,
% 182.27/182.34 (P2(x46461,f13(a1,a8))+~E(a14,x46461)),
% 182.27/182.34 inference(scs_inference,[],[1673,2053,1328,1671,2286,2,3,30,12])).
% 182.27/182.34 cnf(5470,plain,
% 182.27/182.34 (E(f13(a1,a5),a16)),
% 182.27/182.34 inference(scs_inference,[],[34,4499,62])).
% 182.27/182.34 cnf(5481,plain,
% 182.27/182.34 (E(f2(x54811,f13(a1,a5)),f2(x54811,a16))),
% 182.27/182.34 inference(scs_inference,[],[34,4499,62,53,52,6,4,9,7,8,5])).
% 182.27/182.34 cnf(5484,plain,
% 182.27/182.34 (~P13(a11,f13(a1,a5))),
% 182.27/182.34 inference(scs_inference,[],[34,84,343,4499,4618,62,53,52,6,4,9,7,8,5,25,28])).
% 182.27/182.34 cnf(5504,plain,
% 182.27/182.34 (~P2(f13(a1,a5),a11)),
% 182.27/182.34 inference(scs_inference,[],[5470,5481,258,52,53,12])).
% 182.27/182.34 cnf(5508,plain,
% 182.27/182.34 (E(f13(a1,a5),f13(a1,a8))),
% 182.27/182.34 inference(scs_inference,[],[84,5470,5481,5484,258,307,442,52,53,12,25,28,3])).
% 182.27/182.34 cnf(5511,plain,
% 182.27/182.34 (~P10(a15,f13(a1,a5))),
% 182.27/182.34 inference(scs_inference,[],[84,5470,5481,5484,2126,2191,258,307,442,52,53,12,25,28,3,2,29,26])).
% 182.27/182.34 cnf(5512,plain,
% 182.27/182.34 (~P2(f13(a1,a9),f13(a1,a8))),
% 182.27/182.34 inference(scs_inference,[],[84,5470,5481,5484,2126,2191,258,307,442,52,53,12,25,28,3,2,29,26,998])).
% 182.27/182.34 cnf(5513,plain,
% 182.27/182.34 (~E(a12,f13(a1,a9))),
% 182.27/182.34 inference(scs_inference,[],[84,5470,5481,5484,2126,2191,258,307,442,52,53,12,25,28,3,2,29,26,998,506])).
% 182.27/182.34 cnf(5514,plain,
% 182.27/182.34 (~P2(f13(a1,a9),a12)),
% 182.27/182.34 inference(scs_inference,[],[84,5470,5481,5484,2126,2191,258,307,442,52,53,12,25,28,3,2,29,26,998,506,448])).
% 182.27/182.34 cnf(5520,plain,
% 182.27/182.34 (E(f13(x55201,f13(a1,a5)),f13(x55201,f13(a1,a8)))),
% 182.27/182.34 inference(scs_inference,[],[84,5470,5481,5484,101,2126,2191,258,307,442,52,53,12,25,28,3,2,29,26,998,506,448,54,9,4,7])).
% 182.27/182.34 cnf(5546,plain,
% 182.27/182.35 (P10(x55461,x55461)),
% 182.27/182.35 inference(rename_variables,[],[84])).
% 182.27/182.35 cnf(5548,plain,
% 182.27/182.35 (~E(f13(a1,a9),a12)),
% 182.27/182.35 inference(scs_inference,[],[84,40,5520,5508,5513,5504,5511,5512,5470,260,4593,4646,4627,52,53,65,13,5,25,3,2])).
% 182.27/182.35 cnf(5554,plain,
% 182.27/182.35 (~P10(f13(a1,a9),f13(a1,a8))),
% 182.27/182.35 inference(scs_inference,[],[84,5546,85,40,5520,5508,5513,5504,5511,5512,5470,260,4593,4646,4627,52,53,65,13,5,25,3,2,29,26,3815,3814])).
% 182.27/182.35 cnf(5570,plain,
% 182.27/182.35 (E(f13(a1,a9),f13(a1,a8))),
% 182.27/182.35 inference(scs_inference,[],[84,5546,85,35,40,5520,5508,5513,5504,5511,5512,5470,260,4593,4646,4627,52,53,65,13,5,25,3,2,29,26,3815,3814,3813,3812,3811,3810,3809,3808,3806,3804,3803,3802,3801,3800,3798,3796,15,54])).
% 182.27/182.35 cnf(5597,plain,
% 182.27/182.35 ($false),
% 182.27/182.35 inference(scs_inference,[],[5554,5570,5514,5548,54,61,59,53,52]),
% 182.27/182.35 ['proof']).
% 182.27/182.35 % SZS output end Proof
% 182.27/182.35 % Total time :181.786973s
%------------------------------------------------------------------------------