%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : MGT061+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 : n017.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:22 AM UTC 2026
% Result : Theorem 132.13s 132.28s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : MGT061+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.35 % Computer : n017.cluster.edu
% 0.08/0.35 % Model : x86_64 x86_64
% 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35 % Memory : 8046.5625MB
% 0.08/0.35 % OS : Linux 6.8.0-71-generic
% 0.08/0.35 % CPULimit : 300
% 0.08/0.35 % WCLimit : 300
% 0.08/0.35 % DateTime : Mon Sep 7 13:31:09 UTC 2026
% 0.08/0.35 % CPUTime :
% 0.13/0.45 start to proof:theBenchmark
% 132.13/132.27 %-------------------------------------------
% 132.13/132.27 % File :CSE---1.7
% 132.13/132.27 % Problem :theBenchmark
% 132.13/132.27 % Transform :cnf
% 132.13/132.27 % Format :tptp:raw
% 132.13/132.27 % Command :java -jar mcs_scs.jar %d %s
% 132.13/132.27
% 132.13/132.27 % Result :Theorem 131.795701s
% 132.13/132.27 % Output :CNFRefutation 131.795701s
% 132.13/132.27 %-------------------------------------------
% 132.13/132.27 %--------------------------------------------------------------------------
% 132.13/132.27 % File : MGT061+1 : TPTP v9.3.0. Released v2.4.0.
% 132.13/132.27 % Domain : Management (Organisation Theory)
% 132.13/132.27 % Problem : Conditions for an in reasing hazard of mortality
% 132.13/132.27 % Version : [Han98] axioms.
% 132.13/132.27 % English : The hazard of mortality increases with age for an unendowed
% 132.13/132.27 % organization with a fragile position in drifting environments.
% 132.13/132.27
% 132.13/132.27 % Refs : [Kam00] Kamps (2000), Email to G. Sutcliffe
% 132.13/132.27 % : [CH00] Carroll & Hannan (2000), The Demography of Corporation
% 132.13/132.27 % : [Han98] Hannan (1998), Rethinking Age Dependence in Organizati
% 132.13/132.27 % Source : [Kam00]
% 132.13/132.27 % Names : THEOREM 7 [Han98]
% 132.13/132.27
% 132.13/132.27 % Status : Theorem
% 132.13/132.27 % 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.13 v7.3.0, 0.21 v7.2.0, 0.17 v6.4.0, 0.19 v6.3.0, 0.21 v6.2.0, 0.20 v6.1.0, 0.30 v6.0.0, 0.35 v5.5.0, 0.33 v5.4.0, 0.36 v5.3.0, 0.44 v5.2.0, 0.25 v5.1.0, 0.24 v5.0.0, 0.29 v4.1.0, 0.30 v4.0.0, 0.29 v3.7.0, 0.20 v3.5.0, 0.16 v3.3.0, 0.14 v3.2.0, 0.27 v3.1.0, 0.33 v2.7.0, 0.17 v2.6.0, 0.33 v2.4.0
% 132.13/132.27 % Syntax : Number of formulae : 18 ( 5 unt; 0 def)
% 132.13/132.27 % Number of atoms : 65 ( 12 equ)
% 132.13/132.27 % Maximal formula atoms : 16 ( 3 avg)
% 132.13/132.27 % Number of connectives : 58 ( 11 ~; 4 |; 22 &)
% 132.13/132.27 % ( 7 <=>; 14 =>; 0 <=; 0 <~>)
% 132.13/132.27 % Maximal formula depth : 12 ( 5 avg)
% 132.13/132.27 % Maximal term depth : 2 ( 1 avg)
% 132.13/132.27 % Number of predicates : 12 ( 11 usr; 0 prp; 1-3 aty)
% 132.13/132.27 % Number of functors : 9 ( 9 usr; 7 con; 0-2 aty)
% 132.13/132.27 % Number of variables : 31 ( 31 !; 0 ?)
% 132.13/132.27 % SPC : FOF_THM_RFO_SEQ
% 132.13/132.27
% 132.13/132.27 % Comments : See MGT042+1.p for the mnemonic names.
% 132.13/132.27 %--------------------------------------------------------------------------
% 132.13/132.27 include('Axioms/MGT001+0.ax').
% 132.13/132.27 %--------------------------------------------------------------------------
% 132.13/132.27 %----Problem Axioms
% 132.13/132.27 %----An unendowed organization never possesses immunity.
% 132.13/132.27 fof(assumption_1,axiom,
% 132.13/132.27 ! [X,T] :
% 132.13/132.27 ( ( organization(X)
% 132.13/132.27 & ~ has_endowment(X) )
% 132.13/132.27 => ~ has_immunity(X,T) ) ).
% 132.13/132.27
% 132.13/132.27 %----Two states of the environment are dissimilar for an organization
% 132.13/132.27 %----if and only if the organization cannot be aligned to both.
% 132.13/132.27 %----
% 132.13/132.27 %----Added quantification over X.
% 132.13/132.27 fof(definition_2,axiom,
% 132.13/132.27 ! [X,T0,T] :
% 132.13/132.27 ( dissimilar(X,T0,T)
% 132.13/132.27 <=> ( organization(X)
% 132.13/132.27 & ~ ( is_aligned(X,T0)
% 132.13/132.27 <=> is_aligned(X,T) ) ) ) ).
% 132.13/132.27
% 132.13/132.27 %----An organization is aligned with the state of the environment at
% 132.13/132.27 %----its time of founding.
% 132.13/132.27 fof(assumption_13,axiom,
% 132.13/132.27 ! [X,T] :
% 132.13/132.27 ( ( organization(X)
% 132.13/132.27 & age(X,T) = zero )
% 132.13/132.27 => is_aligned(X,T) ) ).
% 132.13/132.27
% 132.13/132.27 %----Environmental drift: the environments at times separated by more
% 132.13/132.27 %----than `sigma' are dissimilar.
% 132.13/132.27 fof(assumption_15,axiom,
% 132.13/132.27 ! [X,T0,T] :
% 132.13/132.27 ( ( organization(X)
% 132.13/132.27 & age(X,T0) = zero )
% 132.13/132.27 => ( greater(age(X,T),sigma)
% 132.13/132.27 <=> dissimilar(X,T0,T) ) ) ).
% 132.13/132.27
% 132.13/132.27 %--- Case: Fragile and robust positions in drifting environments.
% 132.13/132.27 %--- Retracting A16!
% 132.13/132.27 %----
% 132.13/132.27 %----An organization's position is fragile if and only if it does not
% 132.13/132.27 %----provide advantage after age `sigma'.
% 132.13/132.27 %----
% 132.13/132.27 %----Added case: ( smaller_or_equal(age(X,T),sigma)
% 132.13/132.28 %---- => positional_advantage(X,T) )
% 132.13/132.28 fof(definition_3,axiom,
% 132.13/132.28 ! [X] :
% 132.13/132.28 ( fragile_position(X)
% 132.13/132.28 <=> ! [T] :
% 132.13/132.28 ( ( smaller_or_equal(age(X,T),sigma)
% 132.13/132.28 => positional_advantage(X,T) )
% 132.13/132.28 & ( greater(age(X,T),sigma)
% 132.13/132.28 => ~ positional_advantage(X,T) ) ) ) ).
% 132.13/132.28
% 132.13/132.28 %----An organization's immunity. alignment of capability with the
% 132.13/132.28 %----current state of the environment and positional advantage jointly
% 132.13/132.28 %----affect the hazard of mortality with the following ordinal scaling:
% 132.13/132.28 fof(assumption_17,axiom,
% 132.13/132.28 ! [X,T] :
% 132.13/132.28 ( organization(X)
% 132.13/132.28 => ( ( has_immunity(X,T)
% 132.13/132.28 => hazard_of_mortality(X,T) = very_low )
% 132.13/132.28 & ( ~ has_immunity(X,T)
% 132.13/132.28 => ( ( ( is_aligned(X,T)
% 132.13/132.28 & positional_advantage(X,T) )
% 132.13/132.28 => hazard_of_mortality(X,T) = low )
% 132.13/132.28 & ( ( ~ is_aligned(X,T)
% 132.13/132.28 & positional_advantage(X,T) )
% 132.13/132.28 => hazard_of_mortality(X,T) = mod1 )
% 132.13/132.28 & ( ( is_aligned(X,T)
% 132.13/132.28 & ~ positional_advantage(X,T) )
% 132.13/132.28 => hazard_of_mortality(X,T) = mod2 )
% 132.13/132.28 & ( ( ~ is_aligned(X,T)
% 132.13/132.28 & ~ positional_advantage(X,T) )
% 132.13/132.28 => hazard_of_mortality(X,T) = high ) ) ) ) ) ).
% 132.13/132.28
% 132.13/132.28 %----The levels of hazard of mortality are ordered:
% 132.13/132.28 %----
% 132.13/132.28 %----Split over 5 separate formulas because TPTP gives an error on top
% 132.13/132.28 %----level occurrences of `&'.
% 132.13/132.28 fof(assumption_18a,axiom,
% 132.13/132.28 greater(high,mod1) ).
% 132.13/132.28
% 132.13/132.28 fof(assumption_18b,axiom,
% 132.13/132.28 greater(mod1,low) ).
% 132.13/132.28
% 132.13/132.28 fof(assumption_18c,axiom,
% 132.13/132.28 greater(low,very_low) ).
% 132.13/132.28
% 132.13/132.28 fof(assumption_18d,axiom,
% 132.13/132.28 greater(high,mod2) ).
% 132.13/132.28
% 132.13/132.28 fof(assumption_18e,axiom,
% 132.13/132.28 greater(mod2,low) ).
% 132.13/132.28
% 132.13/132.28 %----Problem theorems
% 132.13/132.28 %----Fragile position without endowment: The hazard of mortality
% 132.13/132.28 %----increases with age for an unendowed organization with a fragile
% 132.13/132.28 %----position in drifting environments.
% 132.13/132.28 %----From D2, D3 and A1, A13, A15, A17, A18 (text says D1,2 and A1,2,13-15,
% 132.13/132.28 %----A17-19; also needs D<=, MP>com, MP>tra).
% 132.13/132.28 %----
% 132.13/132.28 %----Added (hazard_of_mortality(X,T1) = hazard_of_mortality(X,T0)).
% 132.13/132.28 fof(theorem_7,conjecture,
% 132.13/132.28 ! [X,T0,T1,T2] :
% 132.13/132.28 ( ( organization(X)
% 132.13/132.28 & fragile_position(X)
% 132.13/132.28 & ~ has_endowment(X)
% 132.13/132.28 & age(X,T0) = zero
% 132.13/132.28 & greater(sigma,zero)
% 132.13/132.28 & smaller_or_equal(age(X,T1),sigma)
% 132.13/132.28 & greater(age(X,T2),sigma) )
% 132.13/132.28 => ( greater(hazard_of_mortality(X,T2),hazard_of_mortality(X,T1))
% 132.13/132.28 & hazard_of_mortality(X,T1) = hazard_of_mortality(X,T0) ) ) ).
% 132.13/132.28
% 132.13/132.28 %--------------------------------------------------------------------------
% 132.13/132.28 %-------------------------------------------
% 132.13/132.28 % Proof found
% 132.13/132.28 % SZS status Theorem for theBenchmark
% 132.13/132.28 % SZS output start Proof
% 132.13/132.28 %ClaNum:76(EqnAxiom:31)
% 132.13/132.28 %VarNum:183(SingletonVarNum:68)
% 132.13/132.28 %MaxLitNum:4
% 132.13/132.28 %MaxfuncDepth:2
% 132.13/132.28 %SharedTerms:31
% 132.13/132.28 %goalClause: 32 33 34 35 41 42 43 73
% 132.13/132.28 %singleGoalClaCount:7
% 132.13/132.28 [32]P1(a1)
% 132.13/132.28 [33]P2(a1)
% 132.13/132.28 [35]P5(a7,a6)
% 132.13/132.28 [36]P5(a8,a15)
% 132.13/132.28 [37]P5(a13,a8)
% 132.13/132.28 [38]P5(a14,a8)
% 132.13/132.28 [39]P5(a9,a13)
% 132.13/132.28 [40]P5(a9,a14)
% 132.13/132.28 [43]~P6(a1)
% 132.13/132.28 [34]E(f2(a1,a5),a6)
% 132.13/132.28 [41]P10(f2(a1,a10),a7)
% 132.13/132.28 [42]P5(f2(a1,a11),a7)
% 132.13/132.28 [73]~P5(f12(a1,a11),f12(a1,a10))+~E(f12(a1,a10),f12(a1,a5))
% 132.13/132.28 [44]~E(x441,x442)+P10(x441,x442)
% 132.13/132.28 [45]~E(x451,x452)+P7(x451,x452)
% 132.13/132.28 [49]~P11(x491,x492)+P10(x491,x492)
% 132.13/132.28 [50]~P5(x502,x501)+P11(x501,x502)
% 132.13/132.28 [51]~P5(x511,x512)+P7(x511,x512)
% 132.13/132.28 [52]~P11(x522,x521)+P5(x521,x522)
% 132.13/132.28 [57]~P5(x572,x571)+~P5(x571,x572)
% 132.13/132.28 [67]P1(x671)+~P4(x671,x672,x673)
% 132.13/132.28 [58]P2(x581)+P12(x581,f3(x581))+~P12(x581,f4(x581))
% 132.13/132.28 [63]P2(x631)+P12(x631,f3(x631))+P10(f2(x631,f4(x631)),a7)
% 132.13/132.28 [66]P2(x661)+~P12(x661,f4(x661))+P5(f2(x661,f3(x661)),a7)
% 132.13/132.28 [71]P2(x711)+P10(f2(x711,f4(x711)),a7)+P5(f2(x711,f3(x711)),a7)
% 132.13/132.28 [46]P11(x461,x462)+P5(x461,x462)+E(x461,x462)
% 132.13/132.28 [47]~P1(x471)+P6(x471)+~P8(x471,x472)
% 132.13/132.28 [48]P3(x481,x482)+~P1(x481)+P8(x481,x482)
% 132.13/132.28 [53]P11(x531,x532)+~P10(x531,x532)+E(x531,x532)
% 132.13/132.28 [54]P5(x541,x542)+~P7(x541,x542)+E(x541,x542)
% 132.13/132.28 [55]~P1(x551)+~P8(x551,x552)+E(f12(x551,x552),a15)
% 132.13/132.28 [56]~P1(x561)+P9(x561,x562)+~E(f2(x561,x562),a6)
% 132.13/132.28 [64]~P2(x641)+P12(x641,x642)+~P10(f2(x641,x642),a7)
% 132.13/132.28 [68]~P2(x681)+~P12(x681,x682)+~P5(f2(x681,x682),a7)
% 132.13/132.28 [59]~P5(x591,x593)+P5(x591,x592)+~P5(x593,x592)
% 132.13/132.28 [72]~P4(x721,x723,x722)+P9(x721,x722)+P9(x721,x723)
% 132.13/132.28 [74]~P4(x741,x743,x742)+~P9(x741,x742)+~P9(x741,x743)
% 132.13/132.28 [60]P9(x601,x602)+P12(x601,x602)+~P3(x601,x602)+E(f12(x601,x602),a9)
% 132.13/132.28 [61]P9(x611,x612)+~P12(x611,x612)+~P3(x611,x612)+E(f12(x611,x612),a13)
% 132.13/132.28 [62]P12(x621,x622)+~P9(x621,x622)+~P3(x621,x622)+E(f12(x621,x622),a14)
% 132.13/132.28 [65]~P9(x651,x652)+~P12(x651,x652)+~P3(x651,x652)+E(f12(x651,x652),a8)
% 132.13/132.28 [69]~P1(x691)+~P9(x691,x693)+P9(x691,x692)+P4(x691,x692,x693)
% 132.13/132.28 [70]~P1(x701)+~P9(x701,x703)+P9(x701,x702)+P4(x701,x703,x702)
% 132.13/132.28 [75]~P1(x751)+P4(x751,x752,x753)+~E(f2(x751,x752),a6)+~P5(f2(x751,x753),a7)
% 132.13/132.28 [76]~P1(x761)+~P4(x761,x763,x762)+P5(f2(x761,x762),a7)+~E(f2(x761,x763),a6)
% 132.13/132.28 %EqnAxiom
% 132.13/132.28 [1]E(x11,x11)
% 132.13/132.28 [2]E(x22,x21)+~E(x21,x22)
% 132.13/132.28 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 132.13/132.28 [4]~E(x41,x42)+E(f2(x41,x43),f2(x42,x43))
% 132.13/132.28 [5]~E(x51,x52)+E(f2(x53,x51),f2(x53,x52))
% 132.13/132.28 [6]~E(x61,x62)+E(f12(x61,x63),f12(x62,x63))
% 132.13/132.28 [7]~E(x71,x72)+E(f12(x73,x71),f12(x73,x72))
% 132.13/132.28 [8]~E(x81,x82)+E(f4(x81),f4(x82))
% 132.13/132.28 [9]~E(x91,x92)+E(f3(x91),f3(x92))
% 132.13/132.28 [10]~P1(x101)+P1(x102)+~E(x101,x102)
% 132.13/132.28 [11]~P2(x111)+P2(x112)+~E(x111,x112)
% 132.13/132.28 [12]P5(x122,x123)+~E(x121,x122)+~P5(x121,x123)
% 132.13/132.28 [13]P5(x133,x132)+~E(x131,x132)+~P5(x133,x131)
% 132.13/132.28 [14]P10(x142,x143)+~E(x141,x142)+~P10(x141,x143)
% 132.13/132.28 [15]P10(x153,x152)+~E(x151,x152)+~P10(x153,x151)
% 132.13/132.28 [16]P9(x162,x163)+~E(x161,x162)+~P9(x161,x163)
% 132.13/132.28 [17]P9(x173,x172)+~E(x171,x172)+~P9(x173,x171)
% 132.13/132.28 [18]P12(x182,x183)+~E(x181,x182)+~P12(x181,x183)
% 132.13/132.28 [19]P12(x193,x192)+~E(x191,x192)+~P12(x193,x191)
% 132.13/132.28 [20]P4(x202,x203,x204)+~E(x201,x202)+~P4(x201,x203,x204)
% 132.13/132.28 [21]P4(x213,x212,x214)+~E(x211,x212)+~P4(x213,x211,x214)
% 132.13/132.28 [22]P4(x223,x224,x222)+~E(x221,x222)+~P4(x223,x224,x221)
% 132.13/132.28 [23]P3(x232,x233)+~E(x231,x232)+~P3(x231,x233)
% 132.13/132.28 [24]P3(x243,x242)+~E(x241,x242)+~P3(x243,x241)
% 132.13/132.28 [25]P7(x252,x253)+~E(x251,x252)+~P7(x251,x253)
% 132.13/132.28 [26]P7(x263,x262)+~E(x261,x262)+~P7(x263,x261)
% 132.13/132.28 [27]P11(x272,x273)+~E(x271,x272)+~P11(x271,x273)
% 132.13/132.28 [28]P11(x283,x282)+~E(x281,x282)+~P11(x283,x281)
% 132.13/132.28 [29]~P6(x291)+P6(x292)+~E(x291,x292)
% 132.13/132.28 [30]P8(x302,x303)+~E(x301,x302)+~P8(x301,x303)
% 132.13/132.28 [31]P8(x313,x312)+~E(x311,x312)+~P8(x313,x311)
% 132.13/132.28
% 132.13/132.28 %-------------------------------------------
% 132.13/132.29 cnf(77,plain,
% 132.13/132.29 (P10(x771,x771)),
% 132.13/132.29 inference(equality_inference,[],[44])).
% 132.13/132.29 cnf(78,plain,
% 132.13/132.29 (P7(x781,x781)),
% 132.13/132.29 inference(equality_inference,[],[45])).
% 132.13/132.29 cnf(79,plain,
% 132.13/132.29 (E(a6,f2(a1,a5))),
% 132.13/132.29 inference(scs_inference,[],[34,2])).
% 132.13/132.29 cnf(80,plain,
% 132.13/132.29 (~P5(a6,a7)),
% 132.13/132.29 inference(scs_inference,[],[35,34,2,57])).
% 132.13/132.29 cnf(84,plain,
% 132.13/132.29 (P3(a1,x841)),
% 132.13/132.29 inference(scs_inference,[],[32,35,43,34,2,57,47,48])).
% 132.13/132.29 cnf(86,plain,
% 132.13/132.29 (P9(a1,a5)),
% 132.13/132.29 inference(scs_inference,[],[32,35,43,34,2,57,47,48,56])).
% 132.13/132.29 cnf(88,plain,
% 132.13/132.29 (P12(a1,a10)),
% 132.13/132.29 inference(scs_inference,[],[32,33,35,43,34,41,2,57,47,48,56,64])).
% 132.13/132.29 cnf(90,plain,
% 132.13/132.29 (~P12(a1,a11)),
% 132.13/132.29 inference(scs_inference,[],[32,33,35,43,34,41,42,2,57,47,48,56,64,68])).
% 132.13/132.29 cnf(92,plain,
% 132.13/132.29 (~E(f2(a1,a11),a6)),
% 132.13/132.29 inference(scs_inference,[],[32,33,35,43,34,41,42,2,57,47,48,56,64,68,12])).
% 132.13/132.29 cnf(93,plain,
% 132.13/132.29 (P5(a7,f2(a1,a5))),
% 132.13/132.29 inference(scs_inference,[],[32,33,35,43,34,41,42,2,57,47,48,56,64,68,12,13])).
% 132.13/132.29 cnf(94,plain,
% 132.13/132.29 (P5(f2(a1,a11),a6)),
% 132.13/132.29 inference(scs_inference,[],[32,33,35,43,34,41,42,2,57,47,48,56,64,68,12,13,59])).
% 132.13/132.29 cnf(99,plain,
% 132.13/132.29 (P10(x991,x991)),
% 132.13/132.29 inference(rename_variables,[],[77])).
% 132.13/132.29 cnf(102,plain,
% 132.13/132.29 (~E(a10,a11)),
% 132.13/132.29 inference(scs_inference,[],[32,33,35,43,34,41,42,77,99,2,57,47,48,56,64,68,12,13,59,74,14,15,19])).
% 132.13/132.29 cnf(104,plain,
% 132.13/132.29 (P7(x1041,x1041)),
% 132.13/132.29 inference(rename_variables,[],[78])).
% 132.13/132.29 cnf(107,plain,
% 132.13/132.29 (P4(a1,a5,a11)),
% 132.13/132.29 inference(scs_inference,[],[32,33,35,43,34,41,42,77,99,78,104,2,57,47,48,56,64,68,12,13,59,74,14,15,19,25,26,75])).
% 132.13/132.29 cnf(111,plain,
% 132.13/132.29 (~E(f2(a1,a11),f2(a1,a5))),
% 132.13/132.29 inference(scs_inference,[],[32,33,35,43,34,41,42,77,99,78,104,2,57,47,48,56,64,68,12,13,59,74,14,15,19,25,26,75,52,3])).
% 132.13/132.29 cnf(118,plain,
% 132.13/132.29 (~P5(a7,f2(a1,a11))),
% 132.13/132.29 inference(scs_inference,[],[42,57])).
% 132.13/132.29 cnf(121,plain,
% 132.13/132.29 (~P5(a6,f2(a1,a11))),
% 132.13/132.29 inference(scs_inference,[],[35,42,80,57,13,59])).
% 132.13/132.29 cnf(123,plain,
% 132.13/132.29 (~P11(f2(a1,a11),a7)),
% 132.13/132.29 inference(scs_inference,[],[35,42,80,57,13,59,52])).
% 132.13/132.29 cnf(126,plain,
% 132.13/132.29 (P11(a6,f2(a1,a11))),
% 132.13/132.29 inference(scs_inference,[],[35,42,86,80,57,13,59,52,17,46])).
% 132.13/132.29 cnf(131,plain,
% 132.13/132.29 (~P11(f2(a1,a11),a6)),
% 132.13/132.29 inference(scs_inference,[],[121,52])).
% 132.13/132.29 cnf(133,plain,
% 132.13/132.29 (~P5(f2(a1,a5),a7)),
% 132.13/132.29 inference(scs_inference,[],[93,121,52,57])).
% 132.13/132.29 cnf(136,plain,
% 132.13/132.29 (P5(f2(a1,a11),f2(a1,a5))),
% 132.13/132.29 inference(scs_inference,[],[42,79,93,121,126,52,57,27,59])).
% 132.13/132.29 cnf(145,plain,
% 132.13/132.29 (~P5(f2(a1,a5),f2(a1,a11))),
% 132.13/132.29 inference(scs_inference,[],[136,133,52,57])).
% 132.13/132.29 cnf(147,plain,
% 132.13/132.29 (P5(a13,a15)),
% 132.13/132.29 inference(scs_inference,[],[136,133,36,37,52,57,59])).
% 132.13/132.29 cnf(156,plain,
% 132.13/132.29 (~P11(f2(a1,a11),f2(a1,a5))),
% 132.13/132.29 inference(scs_inference,[],[145,52])).
% 132.13/132.29 cnf(158,plain,
% 132.13/132.29 (~P5(a8,a14)),
% 132.13/132.29 inference(scs_inference,[],[145,38,52,57])).
% 132.13/132.29 cnf(160,plain,
% 132.13/132.29 (P5(a9,a8)),
% 132.13/132.29 inference(scs_inference,[],[145,38,40,52,57,59])).
% 132.13/132.29 cnf(162,plain,
% 132.13/132.29 (~E(a9,a8)),
% 132.13/132.29 inference(scs_inference,[],[145,38,40,52,57,59,12])).
% 132.13/132.29 cnf(163,plain,
% 132.13/132.29 (~E(a15,a14)),
% 132.13/132.29 inference(scs_inference,[],[145,38,40,36,52,57,59,12,13])).
% 132.13/132.29 cnf(164,plain,
% 132.13/132.29 (E(f2(a1,a10),a7)+P11(f2(a1,a10),a7)),
% 132.13/132.29 inference(scs_inference,[],[41,145,38,40,36,52,57,59,12,13,53])).
% 132.13/132.29 cnf(169,plain,
% 132.13/132.29 (~P11(a14,a8)),
% 132.13/132.29 inference(scs_inference,[],[158,52])).
% 132.13/132.29 cnf(171,plain,
% 132.13/132.29 (~P5(a13,a9)),
% 132.13/132.29 inference(scs_inference,[],[39,158,52,57])).
% 132.13/132.29 cnf(173,plain,
% 132.13/132.29 (P5(a9,a15)),
% 132.13/132.29 inference(scs_inference,[],[39,147,158,52,57,59])).
% 132.13/132.29 cnf(175,plain,
% 132.13/132.29 (~E(a15,a9)),
% 132.13/132.29 inference(scs_inference,[],[39,147,158,52,57,59,13])).
% 132.13/132.29 cnf(186,plain,
% 132.13/132.29 (~P5(a14,a9)),
% 132.13/132.29 inference(scs_inference,[],[40,171,52,57])).
% 132.13/132.29 cnf(188,plain,
% 132.13/132.29 (~P5(a8,a9)),
% 132.13/132.29 inference(scs_inference,[],[40,171,158,52,57,59])).
% 132.13/132.29 cnf(190,plain,
% 132.13/132.29 (~E(a8,a9)),
% 132.13/132.29 inference(scs_inference,[],[40,171,158,37,52,57,59,13])).
% 132.13/132.29 cnf(192,plain,
% 132.13/132.29 (E(f2(a1,a11),a7)+~E(f2(a1,a10),f2(a1,a11))),
% 132.13/132.29 inference(scs_inference,[],[41,123,40,171,158,37,52,57,59,13,14,53])).
% 132.13/132.29 cnf(197,plain,
% 132.13/132.29 (E(a7,f2(a1,a11))+~E(f2(a1,a10),f2(a1,a11))),
% 132.13/132.29 inference(scs_inference,[],[41,123,126,40,171,158,37,52,57,59,13,14,53,46,28,2])).
% 132.13/132.29 cnf(203,plain,
% 132.13/132.29 (~P11(a9,a14)),
% 132.13/132.29 inference(scs_inference,[],[186,52])).
% 132.13/132.29 cnf(205,plain,
% 132.13/132.29 (~P5(a15,a9)),
% 132.13/132.29 inference(scs_inference,[],[173,186,52,57])).
% 132.13/132.29 cnf(207,plain,
% 132.13/132.29 (P11(a8,a9)),
% 132.13/132.29 inference(scs_inference,[],[173,186,188,190,52,57,46])).
% 132.13/132.29 cnf(217,plain,
% 132.13/132.29 (~P11(a9,a15)),
% 132.13/132.29 inference(scs_inference,[],[205,52])).
% 132.13/132.29 cnf(219,plain,
% 132.13/132.29 (~P5(a15,a8)),
% 132.13/132.29 inference(scs_inference,[],[36,205,52,57])).
% 132.13/132.29 cnf(223,plain,
% 132.13/132.29 (~E(a13,a15)),
% 132.13/132.29 inference(scs_inference,[],[36,37,175,205,52,57,46,12])).
% 132.13/132.29 cnf(230,plain,
% 132.13/132.29 (P11(x2301,a9)+~E(a8,x2301)),
% 132.13/132.29 inference(scs_inference,[],[34,86,88,126,94,36,37,175,207,205,52,57,46,12,18,11,16,28,59,27])).
% 132.13/132.29 cnf(235,plain,
% 132.13/132.29 (~P11(a8,a15)),
% 132.13/132.29 inference(scs_inference,[],[219,52])).
% 132.13/132.29 cnf(237,plain,
% 132.13/132.29 (~P5(a15,a13)),
% 132.13/132.29 inference(scs_inference,[],[147,219,52,57])).
% 132.13/132.29 cnf(239,plain,
% 132.13/132.29 (P5(a14,a15)),
% 132.13/132.29 inference(scs_inference,[],[147,38,36,219,52,57,59])).
% 132.13/132.29 cnf(241,plain,
% 132.13/132.29 (~E(a14,a15)),
% 132.13/132.29 inference(scs_inference,[],[147,38,36,219,52,57,59,12])).
% 132.13/132.29 cnf(242,plain,
% 132.13/132.29 (~E(a9,a15)),
% 132.13/132.29 inference(scs_inference,[],[147,38,36,219,207,52,57,59,12,28])).
% 132.13/132.29 cnf(249,plain,
% 132.13/132.29 (~P11(a13,a15)),
% 132.13/132.29 inference(scs_inference,[],[237,52])).
% 132.13/132.29 cnf(251,plain,
% 132.13/132.29 (~P5(a8,a13)),
% 132.13/132.29 inference(scs_inference,[],[37,237,52,57])).
% 132.13/132.29 cnf(258,plain,
% 132.13/132.29 (~P11(a13,a8)),
% 132.13/132.29 inference(scs_inference,[],[251,52])).
% 132.13/132.29 cnf(260,plain,
% 132.13/132.29 (~P5(a15,a14)),
% 132.13/132.29 inference(scs_inference,[],[239,251,52,57])).
% 132.13/132.29 cnf(264,plain,
% 132.13/132.29 (~E(a15,a13)),
% 132.13/132.29 inference(scs_inference,[],[36,239,163,251,52,57,46,13])).
% 132.13/132.29 cnf(275,plain,
% 132.13/132.29 (~P11(a14,a15)),
% 132.13/132.29 inference(scs_inference,[],[260,52])).
% 132.13/132.29 cnf(283,plain,
% 132.13/132.29 (~P11(a9,a8)),
% 132.13/132.29 inference(scs_inference,[],[188,52])).
% 132.13/132.29 cnf(303,plain,
% 132.13/132.29 (P10(f2(a1,a5),f2(a1,a11))),
% 132.13/132.29 inference(scs_inference,[],[126,79,49,14])).
% 132.13/132.29 cnf(304,plain,
% 132.13/132.29 (P10(a6,f2(a1,a11))),
% 132.13/132.29 inference(scs_inference,[],[34,303,14])).
% 132.13/132.29 cnf(335,plain,
% 132.13/132.29 (E(a8,a13)+P11(a8,a13)),
% 132.13/132.29 inference(scs_inference,[],[147,251,304,15,12,46])).
% 132.13/132.29 cnf(347,plain,
% 132.13/132.29 (P5(x3471,a15)+~E(a8,x3471)),
% 132.13/132.29 inference(scs_inference,[],[36,12])).
% 132.13/132.29 cnf(387,plain,
% 132.13/132.29 (P5(a9,x3871)+~E(a8,x3871)),
% 132.13/132.29 inference(scs_inference,[],[160,13])).
% 132.13/132.29 cnf(512,plain,
% 132.13/132.29 (E(f12(f2(x5121,f2(a1,a5)),x5122),f12(f2(x5121,a6),x5122))),
% 132.13/132.29 inference(scs_inference,[],[34,6,5])).
% 132.13/132.29 cnf(514,plain,
% 132.13/132.29 (P11(f2(a1,a10),a7)+E(f2(f2(a1,a10),x5141),f2(a7,x5141))),
% 132.13/132.29 inference(scs_inference,[],[164,4])).
% 132.13/132.29 cnf(579,plain,
% 132.13/132.29 (~E(a10,a5)+~P5(f12(a1,a11),f12(a1,a10))),
% 132.13/132.29 inference(scs_inference,[],[73,7])).
% 132.13/132.29 cnf(580,plain,
% 132.13/132.29 (~E(a5,a10)+~P5(f12(a1,a11),f12(a1,a10))),
% 132.13/132.29 inference(scs_inference,[],[579,2])).
% 132.13/132.29 cnf(582,plain,
% 132.13/132.29 (P5(a7,f2(a1,a10))+E(f2(f2(a1,a10),x5821),f2(a7,x5821))),
% 132.13/132.29 inference(scs_inference,[],[514,52])).
% 132.13/132.29 cnf(584,plain,
% 132.13/132.29 (P7(f2(f2(a1,a10),x5841),f2(a7,x5841))+P5(a7,f2(a1,a10))),
% 132.13/132.29 inference(scs_inference,[],[582,45])).
% 132.13/132.29 cnf(587,plain,
% 132.13/132.29 (P7(x5871,f2(a7,x5872))+~E(f2(f2(a1,a10),x5872),x5871)+P5(a7,f2(a1,a10))),
% 132.13/132.29 inference(scs_inference,[],[584,25])).
% 132.13/132.29 cnf(779,plain,
% 132.13/132.29 (E(f2(a6,x7791),f2(f2(a1,a5),x7791))),
% 132.13/132.29 inference(scs_inference,[],[34,2,4])).
% 132.13/132.29 cnf(780,plain,
% 132.13/132.29 (E(f2(f2(a1,a5),x7801),f2(a6,x7801))),
% 132.13/132.29 inference(scs_inference,[],[779,2])).
% 132.13/132.29 cnf(825,plain,
% 132.13/132.29 (E(f2(x8251,a6),f2(x8251,f2(a1,a5)))),
% 132.13/132.29 inference(scs_inference,[],[34,2,5])).
% 132.13/132.29 cnf(826,plain,
% 132.13/132.29 (E(f2(x8261,f2(a1,a5)),f2(x8261,a6))),
% 132.13/132.29 inference(scs_inference,[],[825,2])).
% 132.13/132.29 cnf(827,plain,
% 132.13/132.29 (E(f2(f2(a1,a5),a6),f2(a6,f2(a1,a5)))),
% 132.13/132.29 inference(scs_inference,[],[780,825,2,3])).
% 132.13/132.29 cnf(838,plain,
% 132.13/132.29 (E(f2(f2(a1,a5),f2(a1,a5)),f2(a6,a6))),
% 132.13/132.29 inference(scs_inference,[],[780,826,827,2,3])).
% 132.13/132.29 cnf(847,plain,
% 132.13/132.29 (E(f2(a6,a6),f2(f2(a1,a5),f2(a1,a5)))),
% 132.13/132.29 inference(scs_inference,[],[838,2])).
% 132.13/132.29 cnf(908,plain,
% 132.13/132.29 (P10(f2(a6,x9081),f2(f2(a1,a5),x9081))),
% 132.13/132.29 inference(scs_inference,[],[779,78,77,25,15])).
% 132.13/132.29 cnf(919,plain,
% 132.13/132.29 (P10(f2(x9191,a6),f2(x9191,f2(a1,a5)))),
% 132.13/132.29 inference(scs_inference,[],[825,78,77,25,15])).
% 132.13/132.29 cnf(1006,plain,
% 132.13/132.29 (E(f12(a6,x10061),f12(f2(a1,a5),x10061))),
% 132.13/132.29 inference(scs_inference,[],[34,2,6])).
% 132.13/132.29 cnf(1007,plain,
% 132.13/132.29 (E(f12(f2(a1,a5),x10071),f12(a6,x10071))),
% 132.13/132.29 inference(scs_inference,[],[1006,2])).
% 132.13/132.29 cnf(1081,plain,
% 132.13/132.29 (E(f2(x10811,f2(f2(a1,a5),f2(a1,a5))),f2(x10811,f2(a6,a6)))),
% 132.13/132.29 inference(scs_inference,[],[847,2,5])).
% 132.13/132.29 cnf(1082,plain,
% 132.13/132.29 (E(f12(x10821,a6),f12(x10821,f2(a1,a5)))),
% 132.13/132.29 inference(scs_inference,[],[34,2,7])).
% 132.13/132.29 cnf(1083,plain,
% 132.13/132.29 (E(f12(x10831,f2(a1,a5)),f12(x10831,a6))),
% 132.13/132.29 inference(scs_inference,[],[1082,2])).
% 132.13/132.29 cnf(1084,plain,
% 132.13/132.29 (E(f12(f2(a1,a5),a6),f12(a6,f2(a1,a5)))),
% 132.13/132.29 inference(scs_inference,[],[1007,1082,2,3])).
% 132.13/132.29 cnf(1096,plain,
% 132.13/132.29 (E(f12(f2(a1,a5),f2(a1,a5)),f12(a6,a6))),
% 132.13/132.29 inference(scs_inference,[],[1007,1083,1084,2,3])).
% 132.13/132.29 cnf(1106,plain,
% 132.13/132.29 (E(f12(a6,a6),f12(f2(a1,a5),f2(a1,a5)))),
% 132.13/132.29 inference(scs_inference,[],[1096,2])).
% 132.13/132.29 cnf(1212,plain,
% 132.13/132.29 (P7(f12(f2(a1,a5),x12121),f12(a6,x12121))),
% 132.13/132.29 inference(scs_inference,[],[1006,78,25])).
% 132.13/132.29 cnf(1500,plain,
% 132.13/132.29 (~P7(f2(a1,a5),f2(a1,a11))),
% 132.13/132.29 inference(scs_inference,[],[111,145,2,54])).
% 132.13/132.29 cnf(1501,plain,
% 132.13/132.29 (E(a9,f12(a1,a11))+P9(a1,a11)),
% 132.13/132.29 inference(scs_inference,[],[84,90,2,60])).
% 132.13/132.29 cnf(1516,plain,
% 132.13/132.29 (E(a8,f12(a1,a10))+~P9(a1,a10)),
% 132.13/132.29 inference(scs_inference,[],[88,84,2,65])).
% 132.13/132.29 cnf(1517,plain,
% 132.13/132.29 (E(f2(a8,x15171),f2(f12(a1,a10),x15171))+~P9(a1,a10)),
% 132.13/132.29 inference(scs_inference,[],[1516,4])).
% 132.13/132.29 cnf(1519,plain,
% 132.13/132.29 (~E(f2(a1,a11),a7)),
% 132.13/132.29 inference(scs_inference,[],[33,90,44,64])).
% 132.13/132.29 cnf(1520,plain,
% 132.13/132.29 (~E(f2(a1,a10),f2(a1,a11))),
% 132.13/132.29 inference(scs_inference,[],[1519,192])).
% 132.13/132.29 cnf(1521,plain,
% 132.13/132.29 (P10(f2(a1,a5),a7)+P11(f2(a1,a5),a7)),
% 132.13/132.29 inference(scs_inference,[],[133,44,46])).
% 132.13/132.29 cnf(1522,plain,
% 132.13/132.29 (P10(f2(a1,a5),a7)),
% 132.13/132.29 inference(scs_inference,[],[1521,49])).
% 132.13/132.29 cnf(1523,plain,
% 132.13/132.29 (P12(a1,a5)),
% 132.13/132.29 inference(scs_inference,[],[33,1522,64])).
% 132.13/132.29 cnf(1530,plain,
% 132.13/132.29 (P10(f12(a1,a11),a9)+P9(a1,a11)),
% 132.13/132.29 inference(scs_inference,[],[84,90,44,60])).
% 132.13/132.29 cnf(1558,plain,
% 132.13/132.29 (P7(f12(a1,a11),a9)+P9(a1,a11)),
% 132.13/132.29 inference(scs_inference,[],[84,90,45,60])).
% 132.13/132.29 cnf(1607,plain,
% 132.13/132.29 (P10(x16071,a9)+~E(a8,x16071)),
% 132.13/132.29 inference(scs_inference,[],[49,230])).
% 132.13/132.29 cnf(1651,plain,
% 132.13/132.29 (P10(a8,a13)+E(a8,a13)),
% 132.13/132.29 inference(scs_inference,[],[49,335])).
% 132.13/132.29 cnf(1652,plain,
% 132.13/132.29 (P10(a8,a13)),
% 132.13/132.29 inference(scs_inference,[],[77,1651,15])).
% 132.13/132.29 cnf(1653,plain,
% 132.13/132.29 (P10(x16531,a13)+~E(a8,x16531)),
% 132.13/132.29 inference(scs_inference,[],[1652,14])).
% 132.13/132.29 cnf(2061,plain,
% 132.13/132.29 (~P5(f2(a1,a10),a7)),
% 132.13/132.29 inference(scs_inference,[],[33,1520,239,38,88,51,50,2,68])).
% 132.13/132.29 cnf(2063,plain,
% 132.13/132.29 (~P9(a1,a11)),
% 132.13/132.29 inference(scs_inference,[],[33,1520,239,38,88,107,86,51,50,2,68,74])).
% 132.13/132.29 cnf(2072,plain,
% 132.13/132.29 (E(f12(a1,a5),a8)),
% 132.13/132.29 inference(scs_inference,[],[33,1520,1500,283,1523,162,260,239,163,38,90,88,84,79,107,86,51,50,2,68,74,64,54,53,25,65])).
% 132.13/132.29 cnf(2073,plain,
% 132.13/132.29 (P3(a1,x20731)),
% 132.13/132.29 inference(rename_variables,[],[84])).
% 132.13/132.29 cnf(2075,plain,
% 132.13/132.29 (E(f12(a1,a11),a9)),
% 132.13/132.29 inference(scs_inference,[],[33,1520,1500,283,1523,162,260,239,163,38,90,88,84,2073,79,107,86,51,50,2,68,74,64,54,53,25,65,60])).
% 132.13/132.29 cnf(2085,plain,
% 132.13/132.29 (E(f3(f12(a1,a5)),f3(a8))),
% 132.13/132.29 inference(scs_inference,[],[33,1520,1500,283,1523,162,260,239,163,38,90,88,84,2073,79,107,32,86,51,50,2,68,74,64,54,53,25,65,60,69,44,49,8,9])).
% 132.13/132.29 cnf(2086,plain,
% 132.13/132.29 (E(f2(f12(a1,a5),x20861),f2(a8,x20861))),
% 132.13/132.29 inference(scs_inference,[],[33,1520,1500,283,1523,162,260,239,163,38,90,88,84,2073,79,107,32,86,51,50,2,68,74,64,54,53,25,65,60,69,44,49,8,9,4])).
% 132.13/132.29 cnf(2087,plain,
% 132.13/132.29 (E(f12(f12(a1,a5),x20871),f12(a8,x20871))),
% 132.13/132.29 inference(scs_inference,[],[33,1520,1500,283,1523,162,260,239,163,38,90,88,84,2073,79,107,32,86,51,50,2,68,74,64,54,53,25,65,60,69,44,49,8,9,4,6])).
% 132.13/132.29 cnf(2088,plain,
% 132.13/132.29 (E(f12(x20881,f12(a1,a5)),f12(x20881,a8))),
% 132.13/132.29 inference(scs_inference,[],[33,1520,1500,283,1523,162,260,239,163,38,90,88,84,2073,79,107,32,86,51,50,2,68,74,64,54,53,25,65,60,69,44,49,8,9,4,6,7])).
% 132.13/132.29 cnf(2093,plain,
% 132.13/132.29 (E(f2(x20931,f12(a1,a5)),f2(x20931,a8))),
% 132.13/132.29 inference(scs_inference,[],[33,1520,1500,283,1523,162,260,239,163,38,90,88,84,2073,79,107,32,86,51,50,2,68,74,64,54,53,25,65,60,69,44,49,8,9,4,6,7,1530,1558,45,5])).
% 132.13/132.29 cnf(2094,plain,
% 132.13/132.29 (E(a9,f12(a1,a11))),
% 132.13/132.29 inference(scs_inference,[],[33,1520,1500,283,1523,162,260,239,163,38,90,88,84,2073,79,107,32,86,51,50,2,68,74,64,54,53,25,65,60,69,44,49,8,9,4,6,7,1530,1558,45,5,1501])).
% 132.13/132.29 cnf(2099,plain,
% 132.13/132.29 (~P5(f12(a1,a5),a9)),
% 132.13/132.29 inference(scs_inference,[],[33,1520,1500,283,1523,162,260,188,1106,239,163,38,826,90,88,84,2073,79,107,32,86,51,50,2,68,74,64,54,53,25,65,60,69,44,49,8,9,4,6,7,1530,1558,45,5,1501,30,28,3,12])).
% 132.13/132.29 cnf(2100,plain,
% 132.13/132.29 (~P11(f12(a1,a11),a8)),
% 132.13/132.29 inference(scs_inference,[],[33,1520,1500,283,1523,162,260,188,1106,239,163,38,826,90,88,84,2073,79,107,32,86,51,50,2,68,74,64,54,53,25,65,60,69,44,49,8,9,4,6,7,1530,1558,45,5,1501,30,28,3,12,27])).
% 132.13/132.29 cnf(2102,plain,
% 132.13/132.29 (~P5(a8,f12(a1,a11))),
% 132.13/132.29 inference(scs_inference,[],[33,1520,1500,283,1523,162,260,188,1106,239,163,38,826,90,88,84,2073,79,107,32,86,51,50,2,68,74,64,54,53,25,65,60,69,44,49,8,9,4,6,7,1530,1558,45,5,1501,30,28,3,12,27,14,13])).
% 132.13/132.29 cnf(2103,plain,
% 132.13/132.29 (~P10(a9,f12(a1,a5))),
% 132.13/132.29 inference(scs_inference,[],[33,1520,1500,283,1523,162,260,188,1106,239,163,38,826,90,88,84,2073,79,107,32,86,51,50,2,68,74,64,54,53,25,65,60,69,44,49,8,9,4,6,7,1530,1558,45,5,1501,30,28,3,12,27,14,13,15])).
% 132.13/132.29 cnf(2114,plain,
% 132.13/132.29 (P7(a9,f12(a1,a11))),
% 132.13/132.29 inference(scs_inference,[],[2094,45])).
% 132.13/132.29 cnf(2118,plain,
% 132.13/132.29 (E(f12(x21181,f12(a1,a11)),f12(x21181,a9))),
% 132.13/132.29 inference(scs_inference,[],[2075,2094,37,45,50,7])).
% 132.13/132.29 cnf(2121,plain,
% 132.13/132.29 (P10(a9,f12(a1,a11))),
% 132.13/132.29 inference(scs_inference,[],[2075,2094,37,45,50,7,51,44])).
% 132.13/132.29 cnf(2124,plain,
% 132.13/132.29 (E(f12(f12(a1,a11),x21241),f12(a9,x21241))),
% 132.13/132.29 inference(scs_inference,[],[2075,2094,37,45,50,7,51,44,8,6])).
% 132.13/132.29 cnf(2125,plain,
% 132.13/132.29 (E(f2(f12(a1,a11),x21251),f2(a9,x21251))),
% 132.13/132.29 inference(scs_inference,[],[2075,2094,37,45,50,7,51,44,8,6,4])).
% 132.13/132.29 cnf(2127,plain,
% 132.13/132.29 (E(f2(x21271,f12(a1,a11)),f2(x21271,a9))),
% 132.13/132.29 inference(scs_inference,[],[2075,2094,37,45,50,7,51,44,8,6,4,9,5])).
% 132.13/132.29 cnf(2128,plain,
% 132.13/132.29 (~E(a7,f2(a1,a11))),
% 132.13/132.29 inference(scs_inference,[],[2075,2094,1519,37,45,50,7,51,44,8,6,4,9,5,2])).
% 132.13/132.29 cnf(2135,plain,
% 132.13/132.29 (~P11(f12(a1,a11),f12(a1,a5))),
% 132.13/132.29 inference(scs_inference,[],[241,2075,2094,2100,2102,275,1519,2072,175,205,37,36,45,50,7,51,44,8,6,4,9,5,2,59,54,53,28])).
% 132.13/132.29 cnf(2136,plain,
% 132.13/132.29 (~E(f12(a1,a11),a15)),
% 132.13/132.29 inference(scs_inference,[],[241,242,2075,2094,2100,2102,275,1519,2072,175,205,37,36,45,50,7,51,44,8,6,4,9,5,2,59,54,53,28,3])).
% 132.13/132.29 cnf(2137,plain,
% 132.13/132.29 (P5(f12(a1,a11),a13)),
% 132.13/132.29 inference(scs_inference,[],[241,242,2075,2094,2100,2102,275,1519,2072,175,205,37,39,36,45,50,7,51,44,8,6,4,9,5,2,59,54,53,28,3,12])).
% 132.13/132.29 cnf(2140,plain,
% 132.13/132.29 (P10(f2(a6,a8),f2(f2(a1,a5),f12(a1,a5)))),
% 132.13/132.29 inference(scs_inference,[],[241,242,2075,2094,2100,2102,2093,275,1519,2072,908,175,235,205,37,39,36,45,50,7,51,44,8,6,4,9,5,2,59,54,53,28,3,12,27,26,14])).
% 132.13/132.29 cnf(2143,plain,
% 132.13/132.29 (~P5(f12(a1,a5),f12(a1,a11))),
% 132.13/132.29 inference(scs_inference,[],[241,242,2075,2094,2099,2100,2102,2093,275,1519,2072,908,175,235,205,37,39,36,45,50,7,51,44,8,6,4,9,5,2,59,54,53,28,3,12,27,26,14,13])).
% 132.13/132.29 cnf(2153,plain,
% 132.13/132.30 (~E(f2(a1,a10),f2(a1,a11))),
% 132.13/132.30 inference(scs_inference,[],[2128,197])).
% 132.13/132.30 cnf(2158,plain,
% 132.13/132.30 (P7(f12(x21581,f12(a1,a11)),f12(x21581,a9))),
% 132.13/132.30 inference(scs_inference,[],[2137,2118,50,51,45])).
% 132.13/132.30 cnf(2161,plain,
% 132.13/132.30 (P10(f12(x21611,f12(a1,a11)),f12(x21611,a9))),
% 132.13/132.30 inference(scs_inference,[],[2137,2118,2094,50,51,45,8,44])).
% 132.13/132.30 cnf(2163,plain,
% 132.13/132.30 (E(f12(x21631,a9),f12(x21631,f12(a1,a11)))),
% 132.13/132.30 inference(scs_inference,[],[2137,2118,2094,50,51,45,8,44,7])).
% 132.13/132.30 cnf(2164,plain,
% 132.13/132.30 (E(f2(a9,x21641),f2(f12(a1,a11),x21641))),
% 132.13/132.30 inference(scs_inference,[],[2137,2118,2094,50,51,45,8,44,7,4])).
% 132.13/132.30 cnf(2166,plain,
% 132.13/132.30 (E(f12(a9,x21661),f12(f12(a1,a11),x21661))),
% 132.13/132.30 inference(scs_inference,[],[2137,2118,2094,50,51,45,8,44,7,4,9,6])).
% 132.13/132.30 cnf(2167,plain,
% 132.13/132.30 (E(f2(x21671,a9),f2(x21671,f12(a1,a11)))),
% 132.13/132.30 inference(scs_inference,[],[2137,2118,2094,50,51,45,8,44,7,4,9,6,5])).
% 132.13/132.30 cnf(2169,plain,
% 132.13/132.30 (~P5(f2(a1,a10),f2(a1,a11))),
% 132.13/132.30 inference(scs_inference,[],[2136,2137,2061,2118,2094,42,50,51,45,8,44,7,4,9,6,5,2,59])).
% 132.13/132.30 cnf(2176,plain,
% 132.13/132.30 (E(f12(f12(a1,a11),f12(a1,a11)),f12(a9,a9))),
% 132.13/132.30 inference(scs_inference,[],[2128,2136,2137,2061,2118,2124,258,156,2072,118,2094,111,42,50,51,45,8,44,7,4,9,6,5,2,59,54,53,28,3])).
% 132.13/132.30 cnf(2177,plain,
% 132.13/132.30 (E(f12(x21771,f12(a1,a11)),f12(x21771,a9))),
% 132.13/132.30 inference(rename_variables,[],[2118])).
% 132.13/132.30 cnf(2186,plain,
% 132.13/132.30 (~E(f12(a1,a11),f12(a1,a5))),
% 132.13/132.30 inference(scs_inference,[],[2128,2136,2103,2121,2137,2061,2118,2177,2124,258,203,156,1212,2072,251,118,2094,2075,186,111,42,50,51,45,8,44,7,4,9,6,5,2,59,54,53,28,3,12,27,26,14,13,15])).
% 132.13/132.30 cnf(2189,plain,
% 132.13/132.30 (P5(f12(a1,a11),f12(a1,a5))),
% 132.13/132.30 inference(scs_inference,[],[2135,2128,2136,2103,2121,2137,2061,2118,2177,2124,258,203,156,1212,2072,251,118,2094,2075,186,111,42,50,51,45,8,44,7,4,9,6,5,2,59,54,53,28,3,12,27,26,14,13,15,587,46])).
% 132.13/132.30 cnf(2205,plain,
% 132.13/132.30 (P5(f12(a1,a11),a8)),
% 132.13/132.30 inference(scs_inference,[],[2189,2186,2176,2137,37,51,50,45,44,2,59])).
% 132.13/132.30 cnf(2212,plain,
% 132.13/132.30 (E(f2(a9,a9),f2(f12(a1,a11),f12(a1,a11)))),
% 132.13/132.30 inference(scs_inference,[],[2143,2189,2186,2176,2164,2167,223,249,169,2137,2072,37,51,50,45,44,2,59,54,53,28,3])).
% 132.13/132.30 cnf(2213,plain,
% 132.13/132.30 (E(f2(a9,x22131),f2(f12(a1,a11),x22131))),
% 132.13/132.30 inference(rename_variables,[],[2164])).
% 132.13/132.30 cnf(2215,plain,
% 132.13/132.30 (P5(a9,f12(a1,a5))),
% 132.13/132.30 inference(scs_inference,[],[2143,2189,2186,2176,2164,2167,223,249,169,2137,2072,37,2075,51,50,45,44,2,59,54,53,28,3,12])).
% 132.13/132.30 cnf(2216,plain,
% 132.13/132.30 (~E(a9,f12(a1,a5))),
% 132.13/132.30 inference(scs_inference,[],[2143,2189,2186,2114,2176,2164,2167,223,249,169,2137,2072,37,2075,51,50,45,44,2,59,54,53,28,3,12,25])).
% 132.13/132.30 cnf(2227,plain,
% 132.13/132.30 (P11(f2(a1,a10),f2(a1,a11))),
% 132.13/132.30 inference(scs_inference,[],[2153,2143,2189,2186,2169,2114,2161,2176,2164,2213,2167,919,223,249,169,2137,2072,37,2094,219,2075,51,50,45,44,2,59,54,53,28,3,12,25,26,14,13,15,49,30,46])).
% 132.13/132.30 cnf(2237,plain,
% 132.13/132.30 (P11(f12(a1,a5),a9)),
% 132.13/132.30 inference(scs_inference,[],[2227,2215,49,51,50])).
% 132.13/132.30 cnf(2243,plain,
% 132.13/132.30 (P5(f2(a1,a11),f2(a1,a10))),
% 132.13/132.30 inference(scs_inference,[],[2227,2215,2212,49,51,50,44,45,52])).
% 132.13/132.30 cnf(2250,plain,
% 132.13/132.30 (E(f12(a9,a9),f12(f12(a1,a11),f12(a1,a11)))),
% 132.13/132.30 inference(scs_inference,[],[2227,2215,2216,2212,2163,2166,131,264,237,92,49,51,50,44,45,52,2,54,53,3])).
% 132.13/132.30 cnf(2272,plain,
% 132.13/132.30 (P11(a8,f12(a1,a11))),
% 132.13/132.30 inference(scs_inference,[],[2237,2243,2250,2205,49,51,44,45,50])).
% 132.13/132.30 cnf(2279,plain,
% 132.13/132.30 (E(f12(f12(a1,a5),f12(a1,a5)),f12(a8,a8))),
% 132.13/132.30 inference(scs_inference,[],[2237,2243,2250,2205,2087,2088,242,2153,2169,217,102,49,51,44,45,50,2,54,53,3])).
% 132.13/132.30 cnf(2301,plain,
% 132.13/132.30 (E(f2(f12(a1,a11),f12(a1,a5)),f2(a9,a8))),
% 132.13/132.30 inference(scs_inference,[],[2272,2279,2125,2205,2093,190,188,93,49,51,45,44,50,54,3])).
% 132.13/132.30 cnf(2314,plain,
% 132.13/132.30 (P11(a15,a8)),
% 132.13/132.30 inference(scs_inference,[],[2301,36,44,50])).
% 132.13/132.30 cnf(2436,plain,
% 132.13/132.30 (P10(f12(f12(a1,a5),x24361),f12(a8,x24361))),
% 132.13/132.30 inference(scs_inference,[],[2087,44])).
% 132.13/132.30 cnf(2438,plain,
% 132.13/132.30 (P7(f12(f12(a1,a5),x24381),f12(a8,x24381))),
% 132.13/132.30 inference(scs_inference,[],[2087,44,45])).
% 132.13/132.30 cnf(2473,plain,
% 132.13/132.30 (P10(f12(x24731,f12(a1,a5)),f12(x24731,a8))),
% 132.13/132.30 inference(scs_inference,[],[2088,44])).
% 132.13/132.30 cnf(2483,plain,
% 132.13/132.30 (P10(f2(x24831,f12(a1,a5)),f2(x24831,a8))),
% 132.13/132.30 inference(scs_inference,[],[2093,44])).
% 132.13/132.30 cnf(2485,plain,
% 132.13/132.30 (P7(f2(x24851,f12(a1,a5)),f2(x24851,a8))),
% 132.13/132.30 inference(scs_inference,[],[2093,44,45])).
% 132.13/132.30 cnf(2519,plain,
% 132.13/132.30 (P7(f2(f12(a1,a11),x25191),f2(a9,x25191))),
% 132.13/132.30 inference(scs_inference,[],[2125,44,45])).
% 132.13/132.30 cnf(2562,plain,
% 132.13/132.30 (P10(f2(f12(a1,a5),x25621),f2(a8,x25621))),
% 132.13/132.30 inference(scs_inference,[],[2086,44])).
% 132.13/132.30 cnf(2598,plain,
% 132.13/132.30 (P7(f2(f12(a1,a5),x25981),f2(a8,x25981))),
% 132.13/132.30 inference(scs_inference,[],[2086,45])).
% 132.13/132.30 cnf(4390,plain,
% 132.13/132.30 (P10(f2(x43901,f2(f2(a1,a5),f2(a1,a5))),f2(x43901,f2(a6,a6)))),
% 132.13/132.30 inference(scs_inference,[],[1081,6,8,9,4,7,44])).
% 132.13/132.30 cnf(4393,plain,
% 132.13/132.30 (P7(f2(x43931,f2(f2(a1,a5),f2(a1,a5))),f2(x43931,f2(a6,a6)))),
% 132.13/132.30 inference(scs_inference,[],[1081,6,8,9,4,7,44,5,45])).
% 132.13/132.30 cnf(4396,plain,
% 132.13/132.30 (E(f2(x43961,f2(f2(a1,a5),f2(a1,a5))),f2(x43961,f2(a6,a6)))),
% 132.13/132.30 inference(rename_variables,[],[1081])).
% 132.13/132.30 cnf(4397,plain,
% 132.13/132.30 (P7(f2(f12(a1,a5),x43971),f2(a8,x43971))),
% 132.27/132.30 inference(rename_variables,[],[2598])).
% 132.27/132.30 cnf(4399,plain,
% 132.27/132.30 (E(f2(x43991,f2(f2(a1,a5),f2(a1,a5))),f2(x43991,f2(a6,a6)))),
% 132.27/132.30 inference(rename_variables,[],[1081])).
% 132.27/132.30 cnf(4402,plain,
% 132.27/132.30 (E(f2(x44021,f2(f2(a1,a5),f2(a1,a5))),f2(x44021,f2(a6,a6)))),
% 132.27/132.30 inference(rename_variables,[],[1081])).
% 132.27/132.30 cnf(4403,plain,
% 132.27/132.30 (P10(f2(f12(a1,a5),x44031),f2(a8,x44031))),
% 132.27/132.30 inference(rename_variables,[],[2562])).
% 132.27/132.30 cnf(4404,plain,
% 132.27/132.30 (P10(f2(f12(a1,a5),f2(f2(a1,a5),f2(a1,a5))),f2(a8,f2(a6,a6)))),
% 132.27/132.30 inference(scs_inference,[],[2562,4403,2598,4397,1081,4396,4399,4402,6,8,9,4,7,44,5,45,26,25,14,15])).
% 132.27/132.30 cnf(4438,plain,
% 132.27/132.30 (E(f12(x44381,a6),f12(x44381,f2(a1,a5)))),
% 132.27/132.30 inference(rename_variables,[],[1082])).
% 132.27/132.30 cnf(4442,plain,
% 132.27/132.30 (E(f12(f2(a1,a5),x44421),f12(a6,x44421))),
% 132.27/132.30 inference(rename_variables,[],[1007])).
% 132.27/132.30 cnf(4455,plain,
% 132.27/132.30 (P9(a1,a10)),
% 132.27/132.30 inference(scs_inference,[],[32,34,86,779,1007,4442,2072,1082,4438,2127,2061,2063,2161,2436,2140,2158,2438,2314,2,52,1653,347,3,15,28,14,25,26,72,76,53,70])).
% 132.27/132.30 cnf(4463,plain,
% 132.27/132.30 (E(a8,f12(a1,a10))),
% 132.27/132.30 inference(scs_inference,[],[4455,1516])).
% 132.27/132.30 cnf(4464,plain,
% 132.27/132.30 (E(f2(a8,x44641),f2(f12(a1,a10),x44641))),
% 132.27/132.30 inference(scs_inference,[],[4455,1517])).
% 132.27/132.30 cnf(4499,plain,
% 132.27/132.30 (P5(a9,f12(a1,a10))),
% 132.27/132.30 inference(scs_inference,[],[512,4463,2,347,1607,387])).
% 132.27/132.30 cnf(4507,plain,
% 132.27/132.30 (E(f2(a6,x45071),f2(f2(a1,a5),x45071))),
% 132.27/132.30 inference(rename_variables,[],[779])).
% 132.27/132.30 cnf(4513,plain,
% 132.27/132.30 (P7(f2(f12(a1,a11),a8),f2(a9,f12(a1,a5)))),
% 132.27/132.30 inference(scs_inference,[],[779,1007,2094,1082,2093,512,2519,2473,2483,2314,2272,4463,2,347,1607,387,230,3,27,15,28,12,14,25])).
% 132.27/132.30 cnf(4525,plain,
% 132.27/132.30 (~E(f12(a1,a10),f12(a1,a5))),
% 132.27/132.30 inference(scs_inference,[],[779,4507,1007,2094,1082,2093,512,2485,2519,2473,2483,2314,2272,4463,2,347,1607,387,230,3,27,15,28,12,14,25,26,57,52,579,580,73])).
% 132.27/132.30 cnf(4567,plain,
% 132.27/132.30 (E(f2(a6,x45671),f2(f2(a1,a5),x45671))),
% 132.27/132.30 inference(rename_variables,[],[779])).
% 132.27/132.30 cnf(4571,plain,
% 132.27/132.30 (P10(f2(f12(a1,a5),a8),f2(a8,f12(a1,a5)))),
% 132.27/132.30 inference(scs_inference,[],[779,4567,2093,2085,1081,2562,4390,4499,57,2,52,3,15,14])).
% 132.27/132.30 cnf(4632,plain,
% 132.27/132.30 (E(f12(a1,a5),f12(a1,a10))),
% 132.27/132.30 inference(scs_inference,[],[779,2072,2125,4463,2086,4571,4393,4464,4404,4513,2,15,14,25,26,3])).
% 132.27/132.30 cnf(5179,plain,
% 132.27/132.30 ($false),
% 132.27/132.30 inference(scs_inference,[],[4632,4525,2]),
% 132.27/132.30 ['proof']).
% 132.27/132.30 % SZS output end Proof
% 132.27/132.30 % Total time :131.795701s
%------------------------------------------------------------------------------