%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : MGT064+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 : n012.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 259.56s 259.60s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : MGT064+1 : TPTP v9.3.0. Released v2.4.0.
% 0.00/0.01 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% 0.03/0.29 % Computer : n012.cluster.edu
% 0.03/0.29 % Model : x86_64 x86_64
% 0.03/0.29 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.03/0.29 % Memory : 8046.5625MB
% 0.03/0.29 % OS : Linux 6.8.0-71-generic
% 0.03/0.29 % CPULimit : 300
% 0.03/0.29 % WCLimit : 300
% 0.03/0.29 % DateTime : Mon Sep 7 13:42:41 UTC 2026
% 0.03/0.30 % CPUTime :
% 0.08/0.39 start to proof:theBenchmark
% 259.45/259.59 %-------------------------------------------
% 259.45/259.59 % File :CSE---1.7
% 259.45/259.59 % Problem :theBenchmark
% 259.45/259.59 % Transform :cnf
% 259.45/259.59 % Format :tptp:raw
% 259.45/259.59 % Command :java -jar mcs_scs.jar %d %s
% 259.45/259.59
% 259.45/259.59 % Result :Theorem 259.192543s
% 259.45/259.59 % Output :CNFRefutation 259.192543s
% 259.45/259.59 %-------------------------------------------
% 259.45/259.59 %--------------------------------------------------------------------------
% 259.45/259.59 % File : MGT064+1 : TPTP v9.3.0. Released v2.4.0.
% 259.45/259.59 % Domain : Management (Organisation Theory)
% 259.45/259.59 % Problem : Conditions for a decreasing then increasing hazard of mortality
% 259.45/259.59 % Version : [Han98] axioms.
% 259.45/259.59 % English : If advantage can be gained from occupancy of a robust position
% 259.45/259.59 % before environmental drift destroys alignment, then the hazard
% 259.45/259.59 % of mortality for an unendowed organization with a robust
% 259.45/259.59 % position initially decreases with age and then rises with
% 259.45/259.59 % further aging but remains below the initial level.
% 259.45/259.59
% 259.45/259.59 % Refs : [Kam00] Kamps (2000), Email to G. Sutcliffe
% 259.45/259.59 % : [CH00] Carroll & Hannan (2000), The Demography of Corporation
% 259.45/259.59 % : [Han98] Hannan (1998), Rethinking Age Dependence in Organizati
% 259.45/259.59 % Source : [Kam00]
% 259.45/259.59 % Names : THEOREM 10 [Han98]
% 259.45/259.59
% 259.45/259.59 % Status : Theorem
% 259.45/259.59 % Rating : 0.30 v9.3.0, 0.33 v9.1.0, 0.30 v9.0.0, 0.36 v8.2.0, 0.33 v8.1.0, 0.31 v7.5.0, 0.38 v7.4.0, 0.23 v7.3.0, 0.28 v7.2.0, 0.24 v7.1.0, 0.22 v7.0.0, 0.20 v6.4.0, 0.23 v6.3.0, 0.21 v6.2.0, 0.24 v6.1.0, 0.40 v6.0.0, 0.39 v5.5.0, 0.52 v5.4.0, 0.54 v5.3.0, 0.56 v5.2.0, 0.40 v5.1.0, 0.43 v5.0.0, 0.42 v4.1.0, 0.48 v4.0.0, 0.46 v3.7.0, 0.45 v3.5.0, 0.47 v3.4.0, 0.37 v3.3.0, 0.43 v3.2.0, 0.55 v3.1.0, 0.67 v2.6.0, 0.83 v2.4.0
% 259.45/259.59 % Syntax : Number of formulae : 20 ( 6 unt; 0 def)
% 259.45/259.59 % Number of atoms : 77 ( 12 equ)
% 259.45/259.59 % Maximal formula atoms : 16 ( 3 avg)
% 259.45/259.59 % Number of connectives : 69 ( 12 ~; 4 |; 29 &)
% 259.45/259.59 % ( 8 <=>; 16 =>; 0 <=; 0 <~>)
% 259.45/259.59 % Maximal formula depth : 17 ( 5 avg)
% 259.45/259.59 % Maximal term depth : 2 ( 1 avg)
% 259.45/259.59 % Number of predicates : 12 ( 11 usr; 0 prp; 1-3 aty)
% 259.45/259.59 % Number of functors : 11 ( 11 usr; 9 con; 0-2 aty)
% 259.45/259.59 % Number of variables : 34 ( 34 !; 0 ?)
% 259.45/259.59 % SPC : FOF_THM_RFO_SEQ
% 259.45/259.59
% 259.45/259.59 % Comments : See MGT042+1.p for the mnemonic names.
% 259.45/259.59 %--------------------------------------------------------------------------
% 259.45/259.59 include('Axioms/MGT001+0.ax').
% 259.45/259.59 %--------------------------------------------------------------------------
% 259.45/259.59 %----Problem Axioms
% 259.45/259.59 %----An endowment provides an immunity that lasts until an
% 259.45/259.59 %----organization's age exceeds `eta'.
% 259.45/259.59 fof(definition_1,axiom,
% 259.45/259.59 ! [X] :
% 259.45/259.59 ( has_endowment(X)
% 259.45/259.59 <=> ! [T] :
% 259.45/259.59 ( organization(X)
% 259.45/259.59 & ( smaller_or_equal(age(X,T),eta)
% 259.45/259.59 => has_immunity(X,T) )
% 259.45/259.59 & ( greater(age(X,T),eta)
% 259.45/259.59 => ~ has_immunity(X,T) ) ) ) ).
% 259.45/259.59
% 259.45/259.59 %----An unendowed organization never possesses immunity.
% 259.45/259.59 fof(assumption_1,axiom,
% 259.45/259.59 ! [X,T] :
% 259.45/259.59 ( ( organization(X)
% 259.45/259.59 & ~ has_endowment(X) )
% 259.45/259.59 => ~ has_immunity(X,T) ) ).
% 259.45/259.59
% 259.45/259.59 %----Two states of the environment are dissimilar for an organization
% 259.45/259.59 %----if and only if the organization cannot be aligned to both.
% 259.45/259.59 %----
% 259.45/259.59 %----Added quantification over X.
% 259.45/259.59 fof(definition_2,axiom,
% 259.45/259.59 ! [X,T0,T] :
% 259.45/259.59 ( dissimilar(X,T0,T)
% 259.45/259.59 <=> ( organization(X)
% 259.45/259.59 & ~ ( is_aligned(X,T0)
% 259.45/259.59 <=> is_aligned(X,T) ) ) ) ).
% 259.45/259.59
% 259.45/259.59 %----An organization is aligned with the state of the environment at
% 259.45/259.59 %----its time of founding.
% 259.45/259.59 fof(assumption_13,axiom,
% 259.45/259.59 ! [X,T] :
% 259.45/259.60 ( ( organization(X)
% 259.45/259.60 & age(X,T) = zero )
% 259.45/259.60 => is_aligned(X,T) ) ).
% 259.45/259.60
% 259.45/259.60 %----Environmental drift: the environments at times separated by more
% 259.45/259.60 %----than `sigma' are dissimilar.
% 259.45/259.60 fof(assumption_15,axiom,
% 259.45/259.60 ! [X,T0,T] :
% 259.45/259.60 ( ( organization(X)
% 259.45/259.60 & age(X,T0) = zero )
% 259.45/259.60 => ( greater(age(X,T),sigma)
% 259.45/259.60 <=> dissimilar(X,T0,T) ) ) ).
% 259.45/259.60
% 259.45/259.60 %----An organization's position is robust if and only if it provides
% 259.45/259.60 %----positional advantage only after age `tau'.
% 259.45/259.60 %----
% 259.45/259.60 %----Text says fragile_position(X) instead of robust_position(X).
% 259.45/259.60 %----Interchanged ~ positional_advantage(X,T) and positional_advantage(X,T).
% 259.45/259.60 fof(definition_4,axiom,
% 259.45/259.60 ! [X] :
% 259.45/259.60 ( robust_position(X)
% 259.45/259.60 <=> ! [T] :
% 259.45/259.60 ( ( smaller_or_equal(age(X,T),tau)
% 259.45/259.60 => ~ positional_advantage(X,T) )
% 259.45/259.60 & ( greater(age(X,T),tau)
% 259.45/259.60 => positional_advantage(X,T) ) ) ) ).
% 259.45/259.60
% 259.45/259.60 %----An organization's immunity. alignment of capability with the
% 259.45/259.60 %----current state of the environment and positional advantage jointly
% 259.45/259.60 %----affect the hazard of mortality with the following ordinal scaling:
% 259.45/259.60 fof(assumption_17,axiom,
% 259.45/259.60 ! [X,T] :
% 259.45/259.60 ( organization(X)
% 259.45/259.60 => ( ( has_immunity(X,T)
% 259.45/259.60 => hazard_of_mortality(X,T) = very_low )
% 259.45/259.60 & ( ~ has_immunity(X,T)
% 259.45/259.60 => ( ( ( is_aligned(X,T)
% 259.45/259.60 & positional_advantage(X,T) )
% 259.45/259.60 => hazard_of_mortality(X,T) = low )
% 259.56/259.60 & ( ( ~ is_aligned(X,T)
% 259.56/259.60 & positional_advantage(X,T) )
% 259.56/259.60 => hazard_of_mortality(X,T) = mod1 )
% 259.56/259.60 & ( ( is_aligned(X,T)
% 259.56/259.60 & ~ positional_advantage(X,T) )
% 259.56/259.60 => hazard_of_mortality(X,T) = mod2 )
% 259.56/259.60 & ( ( ~ is_aligned(X,T)
% 259.56/259.60 & ~ positional_advantage(X,T) )
% 259.56/259.60 => hazard_of_mortality(X,T) = high ) ) ) ) ) ).
% 259.56/259.60
% 259.56/259.60 %----The levels of hazard of mortality are ordered:
% 259.56/259.60 %----
% 259.56/259.60 %----Split over 5 separate formulas because TPTP gives an error on top
% 259.56/259.60 %----level occurrences of `&'.
% 259.56/259.60 fof(assumption_18a,axiom,
% 259.56/259.60 greater(high,mod1) ).
% 259.56/259.60
% 259.56/259.60 fof(assumption_18b,axiom,
% 259.56/259.60 greater(mod1,low) ).
% 259.56/259.60
% 259.56/259.60 fof(assumption_18c,axiom,
% 259.56/259.60 greater(low,very_low) ).
% 259.56/259.60
% 259.56/259.60 fof(assumption_18d,axiom,
% 259.56/259.60 greater(high,mod2) ).
% 259.56/259.60
% 259.56/259.60 fof(assumption_18e,axiom,
% 259.56/259.60 greater(mod2,low) ).
% 259.56/259.60
% 259.56/259.60 %----Position dominates alignment:
% 259.56/259.60 fof(assumption_19,axiom,
% 259.56/259.60 greater(mod2,mod1) ).
% 259.56/259.60
% 259.56/259.60 %----Problem theorems
% 259.56/259.60 %----Robust position without endowment when (`sigma' > `tau'): If
% 259.56/259.60 %----advantage can be gained from occupancy of a robust position
% 259.56/259.60 %----before environmental drift destroys alignment (`sigma' > `tau'), then
% 259.56/259.60 %----the hazard of mortality for an unendowed organization with a
% 259.56/259.60 %----robust position initially decreases with age and then rises with
% 259.56/259.60 %----further aging but remains below the initial level.
% 259.56/259.60 %----From D2, D4, A1, A13, A15, A17, A18 (text says D1,2,4 and A1,2,13-15,
% 259.56/259.60 %----17-19; also needs D<, D<=, MP>str, MP>com, MP>tra).
% 259.56/259.60 %----
% 259.56/259.60 %----Added (`sigma' > `tau')
% 259.56/259.60 %----and (hazard_of_mortality(X,T1) = hazard_of_mortality(X,T0)).
% 259.56/259.60 %----Changed greater(hazard_of_mortality(X,T3),hazard_of_mortality(X,T1))
% 259.56/259.60 %----to smaller(hazard_of_mortality(X,T3),hazard_of_mortality(X,T1)).
% 259.56/259.60 fof(theorem_10,conjecture,
% 259.56/259.60 ! [X,T0,T1,T2,T3] :
% 259.56/259.60 ( ( organization(X)
% 259.56/259.60 & robust_position(X)
% 259.56/259.60 & ~ has_endowment(X)
% 259.56/259.60 & age(X,T0) = zero
% 259.56/259.60 & greater(sigma,zero)
% 259.56/259.60 & greater(tau,zero)
% 259.56/259.60 & greater(sigma,tau)
% 259.56/259.60 & smaller_or_equal(age(X,T1),tau)
% 259.56/259.60 & greater(age(X,T2),tau)
% 259.56/259.60 & smaller_or_equal(age(X,T2),sigma)
% 259.56/259.60 & greater(age(X,T3),sigma) )
% 259.56/259.60 => ( smaller(hazard_of_mortality(X,T2),hazard_of_mortality(X,T3))
% 259.56/259.60 & smaller(hazard_of_mortality(X,T3),hazard_of_mortality(X,T1))
% 259.56/259.60 & hazard_of_mortality(X,T1) = hazard_of_mortality(X,T0) ) ) ).
% 259.56/259.60
% 259.56/259.60 %--------------------------------------------------------------------------
% 259.56/259.60 %-------------------------------------------
% 259.56/259.60 % Proof found
% 259.56/259.60 % SZS status Theorem for theBenchmark
% 259.56/259.60 % SZS output start Proof
% 259.56/259.60 %ClaNum:90(EqnAxiom:33)
% 259.56/259.60 %VarNum:207(SingletonVarNum:75)
% 259.56/259.60 %MaxLitNum:4
% 259.56/259.60 %MaxfuncDepth:2
% 259.56/259.60 %SharedTerms:42
% 259.56/259.60 %goalClause: 34 35 36 37 38 39 46 47 48 49 50 90
% 259.56/259.60 %singleGoalClaCount:11
% 259.56/259.60 [34]P1(a1)
% 259.56/259.60 [35]P9(a1)
% 259.56/259.60 [37]P2(a9,a8)
% 259.56/259.60 [38]P2(a9,a19)
% 259.56/259.60 [39]P2(a19,a8)
% 259.56/259.60 [40]P2(a10,a20)
% 259.56/259.60 [41]P2(a17,a10)
% 259.56/259.60 [42]P2(a18,a10)
% 259.56/259.60 [43]P2(a18,a17)
% 259.56/259.60 [44]P2(a11,a17)
% 259.56/259.60 [45]P2(a11,a18)
% 259.56/259.60 [50]~P5(a1)
% 259.56/259.60 [36]E(f2(a1,a7),a8)
% 259.56/259.60 [46]P11(f2(a1,a12),a19)
% 259.56/259.60 [47]P11(f2(a1,a13),a9)
% 259.56/259.60 [48]P2(f2(a1,a13),a19)
% 259.56/259.60 [49]P2(f2(a1,a14),a9)
% 259.56/259.60 [51]~P5(x511)+P1(x511)
% 259.56/259.60 [52]~E(x521,x522)+P11(x521,x522)
% 259.56/259.60 [53]~E(x531,x532)+P6(x531,x532)
% 259.56/259.60 [57]~P12(x571,x572)+P11(x571,x572)
% 259.56/259.60 [58]~P2(x582,x581)+P12(x581,x582)
% 259.56/259.60 [59]~P2(x591,x592)+P6(x591,x592)
% 259.56/259.60 [60]~P12(x602,x601)+P2(x601,x602)
% 259.56/259.60 [65]~P2(x652,x651)+~P2(x651,x652)
% 259.56/259.60 [78]P1(x781)+~P4(x781,x782,x783)
% 259.56/259.60 [90]~P12(f15(a1,a14),f15(a1,a12))+~E(f15(a1,a12),f15(a1,a7))+~P12(f15(a1,a13),f15(a1,a14))
% 259.56/259.60 [66]P9(x661)+P10(x661,f3(x661))+~P10(x661,f6(x661))
% 259.56/259.60 [72]P9(x721)+P10(x721,f3(x721))+P2(f2(x721,f6(x721)),a19)
% 259.56/259.60 [77]P9(x771)+~P10(x771,f6(x771))+P11(f2(x771,f3(x771)),a19)
% 259.56/259.60 [84]P9(x841)+P11(f2(x841,f3(x841)),a19)+P2(f2(x841,f6(x841)),a19)
% 259.56/259.60 [54]P12(x541,x542)+P2(x541,x542)+E(x541,x542)
% 259.56/259.60 [55]~P1(x551)+P5(x551)+~P7(x551,x552)
% 259.56/259.60 [56]P3(x561,x562)+~P1(x561)+P7(x561,x562)
% 259.56/259.60 [61]P12(x611,x612)+~P11(x611,x612)+E(x611,x612)
% 259.56/259.60 [62]P2(x621,x622)+~P6(x621,x622)+E(x621,x622)
% 259.56/259.60 [63]~P1(x631)+~P7(x631,x632)+E(f15(x631,x632),a20)
% 259.56/259.60 [64]~P1(x641)+P8(x641,x642)+~E(f2(x641,x642),a8)
% 259.56/259.60 [73]~P5(x731)+P7(x731,x732)+~P11(f2(x731,x732),a16)
% 259.56/259.60 [74]~P9(x741)+P10(x741,x742)+~P2(f2(x741,x742),a19)
% 259.56/259.60 [79]~P5(x791)+~P7(x791,x792)+~P2(f2(x791,x792),a16)
% 259.56/259.60 [80]~P9(x801)+~P10(x801,x802)+~P11(f2(x801,x802),a19)
% 259.56/259.60 [67]~P2(x671,x673)+P2(x671,x672)+~P2(x673,x672)
% 259.56/259.60 [86]~P4(x861,x863,x862)+P8(x861,x862)+P8(x861,x863)
% 259.56/259.60 [87]~P4(x871,x873,x872)+~P8(x871,x872)+~P8(x871,x873)
% 259.56/259.60 [76]~P1(x761)+P5(x761)+P7(x761,f4(x761))+P11(f2(x761,f5(x761)),a16)
% 259.56/259.60 [85]~P1(x851)+P5(x851)+P11(f2(x851,f5(x851)),a16)+P2(f2(x851,f4(x851)),a16)
% 259.56/259.60 [69]P8(x691,x692)+P10(x691,x692)+~P3(x691,x692)+E(f15(x691,x692),a11)
% 259.56/259.60 [70]P8(x701,x702)+~P10(x701,x702)+~P3(x701,x702)+E(f15(x701,x702),a17)
% 259.56/259.60 [71]P10(x711,x712)+~P8(x711,x712)+~P3(x711,x712)+E(f15(x711,x712),a18)
% 259.56/259.60 [75]~P8(x751,x752)+~P10(x751,x752)+~P3(x751,x752)+E(f15(x751,x752),a10)
% 259.56/259.60 [82]~P1(x821)+~P8(x821,x823)+P8(x821,x822)+P4(x821,x822,x823)
% 259.56/259.60 [83]~P1(x831)+~P8(x831,x833)+P8(x831,x832)+P4(x831,x833,x832)
% 259.56/259.60 [88]~P1(x881)+P4(x881,x882,x883)+~E(f2(x881,x882),a8)+~P2(f2(x881,x883),a9)
% 259.56/259.60 [89]~P1(x891)+~P4(x891,x893,x892)+P2(f2(x891,x892),a9)+~E(f2(x891,x893),a8)
% 259.56/259.60 %EqnAxiom
% 259.56/259.60 [1]E(x11,x11)
% 259.56/259.60 [2]E(x22,x21)+~E(x21,x22)
% 259.56/259.60 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 259.56/259.60 [4]~E(x41,x42)+E(f2(x41,x43),f2(x42,x43))
% 259.56/259.60 [5]~E(x51,x52)+E(f2(x53,x51),f2(x53,x52))
% 259.56/259.60 [6]~E(x61,x62)+E(f15(x61,x63),f15(x62,x63))
% 259.56/259.60 [7]~E(x71,x72)+E(f15(x73,x71),f15(x73,x72))
% 259.56/259.60 [8]~E(x81,x82)+E(f4(x81),f4(x82))
% 259.56/259.60 [9]~E(x91,x92)+E(f5(x91),f5(x92))
% 259.56/259.60 [10]~E(x101,x102)+E(f6(x101),f6(x102))
% 259.56/259.60 [11]~E(x111,x112)+E(f3(x111),f3(x112))
% 259.56/259.60 [12]~P1(x121)+P1(x122)+~E(x121,x122)
% 259.56/259.60 [13]~P9(x131)+P9(x132)+~E(x131,x132)
% 259.56/259.60 [14]P2(x142,x143)+~E(x141,x142)+~P2(x141,x143)
% 259.56/259.60 [15]P2(x153,x152)+~E(x151,x152)+~P2(x153,x151)
% 259.56/259.60 [16]P11(x162,x163)+~E(x161,x162)+~P11(x161,x163)
% 259.56/259.60 [17]P11(x173,x172)+~E(x171,x172)+~P11(x173,x171)
% 259.56/259.60 [18]P8(x182,x183)+~E(x181,x182)+~P8(x181,x183)
% 259.56/259.60 [19]P8(x193,x192)+~E(x191,x192)+~P8(x193,x191)
% 259.56/259.60 [20]P10(x202,x203)+~E(x201,x202)+~P10(x201,x203)
% 259.56/259.60 [21]P10(x213,x212)+~E(x211,x212)+~P10(x213,x211)
% 259.56/259.60 [22]P4(x222,x223,x224)+~E(x221,x222)+~P4(x221,x223,x224)
% 259.56/259.60 [23]P4(x233,x232,x234)+~E(x231,x232)+~P4(x233,x231,x234)
% 259.56/259.60 [24]P4(x243,x244,x242)+~E(x241,x242)+~P4(x243,x244,x241)
% 259.56/259.60 [25]P7(x252,x253)+~E(x251,x252)+~P7(x251,x253)
% 259.56/259.60 [26]P7(x263,x262)+~E(x261,x262)+~P7(x263,x261)
% 259.56/259.60 [27]P3(x272,x273)+~E(x271,x272)+~P3(x271,x273)
% 259.56/259.60 [28]P3(x283,x282)+~E(x281,x282)+~P3(x283,x281)
% 259.56/259.60 [29]P6(x292,x293)+~E(x291,x292)+~P6(x291,x293)
% 259.56/259.60 [30]P6(x303,x302)+~E(x301,x302)+~P6(x303,x301)
% 259.56/259.60 [31]~P5(x311)+P5(x312)+~E(x311,x312)
% 259.56/259.60 [32]P12(x322,x323)+~E(x321,x322)+~P12(x321,x323)
% 259.56/259.60 [33]P12(x333,x332)+~E(x331,x332)+~P12(x333,x331)
% 259.56/259.60
% 259.56/259.60 %-------------------------------------------
% 259.56/259.60 cnf(91,plain,
% 259.56/259.60 (P11(x911,x911)),
% 259.56/259.60 inference(equality_inference,[],[52])).
% 259.56/259.60 cnf(92,plain,
% 259.56/259.60 (P6(x921,x921)),
% 259.56/259.60 inference(equality_inference,[],[53])).
% 259.56/259.60 cnf(93,plain,
% 259.56/259.60 (E(a8,f2(a1,a7))),
% 259.56/259.60 inference(scs_inference,[],[36,2])).
% 259.56/259.60 cnf(94,plain,
% 259.56/259.60 (~P2(a8,a9)),
% 259.56/259.60 inference(scs_inference,[],[37,36,2,65])).
% 259.56/259.60 cnf(98,plain,
% 259.56/259.60 (P3(a1,x981)),
% 259.56/259.60 inference(scs_inference,[],[34,37,50,36,2,65,55,56])).
% 259.56/259.60 cnf(100,plain,
% 259.56/259.60 (P8(a1,a7)),
% 259.56/259.60 inference(scs_inference,[],[34,37,50,36,2,65,55,56,64])).
% 259.56/259.60 cnf(102,plain,
% 259.56/259.60 (P10(a1,a13)),
% 259.56/259.60 inference(scs_inference,[],[34,35,37,50,48,36,2,65,55,56,64,74])).
% 259.56/259.60 cnf(104,plain,
% 259.56/259.61 (~P10(a1,a12)),
% 259.56/259.61 inference(scs_inference,[],[34,35,37,50,48,36,46,2,65,55,56,64,74,80])).
% 259.56/259.61 cnf(107,plain,
% 259.56/259.61 (P2(a9,f2(a1,a7))),
% 259.56/259.61 inference(scs_inference,[],[34,35,37,50,48,36,46,49,2,65,55,56,64,74,80,14,15])).
% 259.56/259.61 cnf(108,plain,
% 259.56/259.61 (P2(f2(a1,a14),a8)),
% 259.56/259.61 inference(scs_inference,[],[34,35,37,50,48,36,46,49,2,65,55,56,64,74,80,14,15,67])).
% 259.56/259.61 cnf(113,plain,
% 259.56/259.61 (P11(x1131,x1131)),
% 259.56/259.61 inference(rename_variables,[],[91])).
% 259.56/259.61 cnf(118,plain,
% 259.56/259.61 (P6(x1181,x1181)),
% 259.56/259.61 inference(rename_variables,[],[92])).
% 259.56/259.61 cnf(121,plain,
% 259.56/259.61 (P4(a1,a7,a14)),
% 259.56/259.61 inference(scs_inference,[],[34,35,37,50,48,36,46,49,91,113,92,118,2,65,55,56,64,74,80,14,15,67,87,16,17,21,29,30,88])).
% 259.56/259.61 cnf(123,plain,
% 259.56/259.61 (~P12(a9,a8)),
% 259.56/259.61 inference(scs_inference,[],[34,35,37,50,48,36,46,49,91,113,92,118,2,65,55,56,64,74,80,14,15,67,87,16,17,21,29,30,88,60])).
% 259.56/259.61 cnf(125,plain,
% 259.56/259.61 (~E(f2(a1,a14),f2(a1,a7))),
% 259.56/259.61 inference(scs_inference,[],[34,35,37,50,48,36,46,49,91,113,92,118,2,65,55,56,64,74,80,14,15,67,87,16,17,21,29,30,88,60,3])).
% 259.56/259.61 cnf(134,plain,
% 259.56/259.61 (~P2(a19,a9)),
% 259.56/259.61 inference(scs_inference,[],[38,65])).
% 259.56/259.61 cnf(138,plain,
% 259.56/259.61 (P2(f2(a1,a14),a19)),
% 259.56/259.61 inference(scs_inference,[],[38,49,65,60,67])).
% 259.56/259.61 cnf(140,plain,
% 259.56/259.61 (P10(a1,a14)),
% 259.56/259.61 inference(scs_inference,[],[38,35,49,65,60,67,74])).
% 259.56/259.61 cnf(142,plain,
% 259.56/259.61 (~E(a8,a9)),
% 259.56/259.61 inference(scs_inference,[],[38,39,35,49,65,60,67,74,15])).
% 259.56/259.61 cnf(143,plain,
% 259.56/259.61 (P8(a1,x1431)+~E(a7,x1431)),
% 259.56/259.61 inference(scs_inference,[],[38,39,35,49,100,65,60,67,74,15,19])).
% 259.56/259.61 cnf(150,plain,
% 259.56/259.61 (~P2(a9,f2(a1,a14))),
% 259.56/259.61 inference(scs_inference,[],[49,65])).
% 259.56/259.61 cnf(154,plain,
% 259.56/259.61 (~P2(a19,f2(a1,a14))),
% 259.56/259.61 inference(scs_inference,[],[49,134,65,60,67])).
% 259.56/259.61 cnf(157,plain,
% 259.56/259.61 (P12(a8,a9)),
% 259.56/259.61 inference(scs_inference,[],[49,134,142,94,65,60,67,14,54])).
% 259.56/259.61 cnf(159,plain,
% 259.56/259.61 (~E(a19,f2(a1,a14))),
% 259.56/259.61 inference(scs_inference,[],[49,38,134,142,94,65,60,67,14,54,15])).
% 259.56/259.61 cnf(161,plain,
% 259.56/259.61 (~E(a8,f2(a1,a14))),
% 259.56/259.61 inference(scs_inference,[],[49,38,140,104,134,142,94,65,60,67,14,54,15,21,32])).
% 259.56/259.61 cnf(164,plain,
% 259.56/259.61 (P10(x1641,a13)+~E(a1,x1641)),
% 259.56/259.61 inference(scs_inference,[],[36,49,38,102,140,104,134,142,94,65,60,67,14,54,15,21,32,33,31,20])).
% 259.56/259.61 cnf(170,plain,
% 259.56/259.61 (~P2(a19,f2(a1,a13))),
% 259.56/259.61 inference(scs_inference,[],[48,65])).
% 259.56/259.61 cnf(172,plain,
% 259.56/259.61 (~P12(f2(a1,a14),a19)),
% 259.56/259.61 inference(scs_inference,[],[48,154,65,60])).
% 259.56/259.61 cnf(174,plain,
% 259.56/259.61 (P12(a19,f2(a1,a14))),
% 259.56/259.61 inference(scs_inference,[],[48,154,159,65,60,54])).
% 259.56/259.61 cnf(176,plain,
% 259.56/259.61 (~P2(a8,f2(a1,a14))),
% 259.56/259.61 inference(scs_inference,[],[48,49,154,159,94,65,60,54,67])).
% 259.56/259.61 cnf(181,plain,
% 259.56/259.61 (P8(x1811,a7)+~E(a1,x1811)),
% 259.56/259.61 inference(scs_inference,[],[48,49,121,100,107,150,154,159,94,65,60,54,67,15,5,22,18])).
% 259.56/259.61 cnf(183,plain,
% 259.56/259.61 (P11(x1831,a19)+~E(f2(a1,a12),x1831)),
% 259.56/259.61 inference(scs_inference,[],[46,48,49,121,100,107,150,154,159,94,65,60,54,67,15,5,22,18,23,16])).
% 259.56/259.61 cnf(185,plain,
% 259.56/259.61 (P11(f2(a1,a12),x1851)+~E(a19,x1851)),
% 259.56/259.61 inference(scs_inference,[],[46,48,49,98,121,100,107,150,154,159,94,65,60,54,67,15,5,22,18,23,16,27,17])).
% 259.56/259.61 cnf(192,plain,
% 259.56/259.61 (~P2(a8,a19)),
% 259.56/259.61 inference(scs_inference,[],[39,65])).
% 259.56/259.61 cnf(196,plain,
% 259.56/259.61 (~E(f2(a1,a13),a8)),
% 259.56/259.61 inference(scs_inference,[],[48,39,170,65,60,14])).
% 259.56/259.61 cnf(197,plain,
% 259.56/259.61 (~P2(a8,f2(a1,a13))),
% 259.56/259.61 inference(scs_inference,[],[48,39,170,65,60,14,67])).
% 259.56/259.61 cnf(201,plain,
% 259.56/259.61 (~E(a8,f2(a1,a13))),
% 259.56/259.61 inference(scs_inference,[],[48,39,161,170,176,65,60,14,67,54,15])).
% 259.56/259.61 cnf(212,plain,
% 259.56/259.61 (~P2(f2(a1,a7),a9)),
% 259.56/259.61 inference(scs_inference,[],[107,65])).
% 259.56/259.61 cnf(217,plain,
% 259.56/259.61 (P2(f2(a1,a13),a8)),
% 259.56/259.61 inference(scs_inference,[],[36,48,39,196,107,197,65,60,3,67])).
% 259.56/259.61 cnf(221,plain,
% 259.56/259.61 (~E(a9,a8)),
% 259.56/259.61 inference(scs_inference,[],[36,48,38,39,196,107,197,201,192,65,60,3,67,54,14])).
% 259.56/259.61 cnf(222,plain,
% 259.56/259.61 (P2(f2(a1,a14),f2(a1,a7))),
% 259.56/259.61 inference(scs_inference,[],[36,48,38,39,93,196,107,197,201,108,192,65,60,3,67,54,14,15])).
% 259.56/259.61 cnf(228,plain,
% 259.56/259.61 (E(f2(a1,a13),a9)+P12(f2(a1,a13),a9)),
% 259.56/259.61 inference(scs_inference,[],[36,48,47,38,39,93,140,196,107,197,201,108,192,65,60,3,67,54,14,15,5,13,32,20,16,61])).
% 259.56/259.61 cnf(236,plain,
% 259.56/259.61 (~P2(f2(a1,a7),f2(a1,a14))),
% 259.56/259.61 inference(scs_inference,[],[222,65])).
% 259.56/259.61 cnf(238,plain,
% 259.56/259.61 (~P12(a9,f2(a1,a7))),
% 259.56/259.61 inference(scs_inference,[],[222,212,65,60])).
% 259.56/259.61 cnf(240,plain,
% 259.56/259.61 (P2(a17,a20)),
% 259.56/259.61 inference(scs_inference,[],[222,212,40,41,65,60,67])).
% 259.56/259.61 cnf(242,plain,
% 259.56/259.61 (~E(a9,f2(a1,a7))),
% 259.56/259.61 inference(scs_inference,[],[36,222,221,212,40,41,65,60,67,3])).
% 259.56/259.61 cnf(243,plain,
% 259.56/259.61 (P2(f2(a1,a13),f2(a1,a7))),
% 259.56/259.61 inference(scs_inference,[],[36,93,222,221,217,212,40,41,65,60,67,3,15])).
% 259.56/259.61 cnf(249,plain,
% 259.56/259.61 (~P2(f2(a1,a7),f2(a1,a13))),
% 259.56/259.61 inference(scs_inference,[],[243,65])).
% 259.56/259.61 cnf(253,plain,
% 259.56/259.61 (P2(a11,a10)),
% 259.56/259.61 inference(scs_inference,[],[243,176,42,45,65,60,67])).
% 259.56/259.61 cnf(260,plain,
% 259.56/259.61 (~P2(a17,a18)),
% 259.56/259.61 inference(scs_inference,[],[43,65])).
% 259.56/259.61 cnf(262,plain,
% 259.56/259.61 (~P12(f2(a1,a14),f2(a1,a7))),
% 259.56/259.61 inference(scs_inference,[],[236,43,65,60])).
% 259.56/259.61 cnf(264,plain,
% 259.56/259.61 (P2(a18,a20)),
% 259.56/259.61 inference(scs_inference,[],[236,43,240,65,60,67])).
% 259.56/259.61 cnf(266,plain,
% 259.56/259.61 (~E(a11,a17)),
% 259.56/259.61 inference(scs_inference,[],[236,43,240,45,65,60,67,14])).
% 259.56/259.61 cnf(267,plain,
% 259.56/259.61 (~E(a20,a18)),
% 259.56/259.61 inference(scs_inference,[],[236,43,240,45,65,60,67,14,15])).
% 259.56/259.61 cnf(272,plain,
% 259.56/259.61 (~P2(a17,a11)),
% 259.56/259.61 inference(scs_inference,[],[44,65])).
% 259.56/259.61 cnf(278,plain,
% 259.56/259.61 (~E(a10,a18)),
% 259.56/259.61 inference(scs_inference,[],[249,44,260,264,41,45,65,60,67,15])).
% 259.56/259.61 cnf(279,plain,
% 259.56/259.61 (P12(x2791,f2(a1,a14))+~E(a19,x2791)),
% 259.56/259.61 inference(scs_inference,[],[174,249,44,260,264,41,45,65,60,67,15,32])).
% 259.56/259.61 cnf(286,plain,
% 259.56/259.61 (~P2(a18,a11)),
% 259.56/259.61 inference(scs_inference,[],[45,65])).
% 259.56/259.61 cnf(288,plain,
% 259.56/259.61 (~P12(a11,a17)),
% 259.56/259.61 inference(scs_inference,[],[45,272,65,60])).
% 259.56/259.61 cnf(290,plain,
% 259.56/259.61 (~E(a10,a11)),
% 259.56/259.61 inference(scs_inference,[],[45,272,42,65,60,15])).
% 259.56/259.61 cnf(297,plain,
% 259.56/259.61 (~P2(a10,a17)),
% 259.56/259.61 inference(scs_inference,[],[41,65])).
% 259.56/259.61 cnf(299,plain,
% 259.56/259.61 (~P12(a11,a18)),
% 259.56/259.61 inference(scs_inference,[],[41,286,65,60])).
% 259.56/259.61 cnf(301,plain,
% 259.56/259.61 (~E(a18,a10)),
% 259.56/259.61 inference(scs_inference,[],[41,43,286,65,60,14])).
% 259.56/259.61 cnf(302,plain,
% 259.56/259.61 (~P2(a10,a11)),
% 259.56/259.61 inference(scs_inference,[],[41,43,286,44,65,60,14,67])).
% 259.56/259.61 cnf(304,plain,
% 259.56/259.61 (~E(a20,a11)),
% 259.56/259.61 inference(scs_inference,[],[41,240,43,286,44,272,65,60,14,67,15])).
% 259.56/259.61 cnf(310,plain,
% 259.56/259.61 (~P2(a20,a17)),
% 259.56/259.61 inference(scs_inference,[],[240,65])).
% 259.56/259.61 cnf(312,plain,
% 259.56/259.61 (~P12(a17,a10)),
% 259.56/259.61 inference(scs_inference,[],[240,297,65,60])).
% 259.56/259.61 cnf(316,plain,
% 259.56/259.61 (~E(a11,a10)),
% 259.56/259.61 inference(scs_inference,[],[240,290,297,302,44,65,60,54,14])).
% 259.56/259.61 cnf(317,plain,
% 259.56/259.61 (~E(a20,a17)),
% 259.56/259.61 inference(scs_inference,[],[240,40,290,297,302,44,65,60,54,14,15])).
% 259.56/259.61 cnf(323,plain,
% 259.56/259.61 (~P2(a20,a18)),
% 259.56/259.61 inference(scs_inference,[],[264,65])).
% 259.56/259.61 cnf(325,plain,
% 259.56/259.61 (~P12(a17,a20)),
% 259.56/259.61 inference(scs_inference,[],[264,310,65,60])).
% 259.56/259.61 cnf(327,plain,
% 259.56/259.61 (~P2(a20,a11)),
% 259.56/259.61 inference(scs_inference,[],[264,44,310,65,60,67])).
% 259.56/259.61 cnf(331,plain,
% 259.56/259.61 (~E(a18,a20)),
% 259.56/259.61 inference(scs_inference,[],[264,43,44,310,317,65,60,67,54,14])).
% 259.56/259.61 cnf(332,plain,
% 259.56/259.61 (~E(a17,a11)),
% 259.56/259.61 inference(scs_inference,[],[264,43,44,310,317,286,65,60,67,54,14,15])).
% 259.56/259.61 cnf(339,plain,
% 259.56/259.61 (~P2(a10,a18)),
% 259.56/259.61 inference(scs_inference,[],[42,65])).
% 259.56/259.61 cnf(341,plain,
% 259.56/259.61 (~P12(a18,a20)),
% 259.56/259.61 inference(scs_inference,[],[42,323,65,60])).
% 259.56/259.61 cnf(343,plain,
% 259.56/259.61 (P12(a20,a18)),
% 259.56/259.61 inference(scs_inference,[],[42,267,323,65,60,54])).
% 259.56/259.61 cnf(345,plain,
% 259.56/259.61 (~E(a11,a20)),
% 259.56/259.61 inference(scs_inference,[],[45,42,267,323,65,60,54,14])).
% 259.56/259.61 cnf(353,plain,
% 259.56/259.61 (~P12(a11,a20)),
% 259.56/259.61 inference(scs_inference,[],[40,327,65,60])).
% 259.56/259.61 cnf(357,plain,
% 259.56/259.61 (~E(a17,a20)),
% 259.56/259.61 inference(scs_inference,[],[41,40,304,327,65,60,54,14])).
% 259.56/259.61 cnf(364,plain,
% 259.56/259.61 (P11(f2(a1,a7),a9)),
% 259.56/259.61 inference(scs_inference,[],[157,93,57,16])).
% 259.56/259.61 cnf(365,plain,
% 259.56/259.61 (~P12(a18,a10)),
% 259.56/259.61 inference(scs_inference,[],[339,60])).
% 259.56/259.61 cnf(368,plain,
% 259.56/259.61 (P12(a10,a18)),
% 259.56/259.61 inference(scs_inference,[],[36,278,364,339,60,16,54])).
% 259.56/259.61 cnf(389,plain,
% 259.56/259.61 (~P12(a11,a10)),
% 259.56/259.61 inference(scs_inference,[],[302,60])).
% 259.56/259.61 cnf(403,plain,
% 259.56/259.61 (~P12(a18,a17)),
% 259.56/259.61 inference(scs_inference,[],[260,60])).
% 259.56/259.61 cnf(425,plain,
% 259.56/259.61 (E(a9,a19)+P12(a19,a9)),
% 259.56/259.61 inference(scs_inference,[],[48,134,54,15,185,279,65,2])).
% 259.56/259.61 cnf(446,plain,
% 259.56/259.61 (P12(a20,x4461)+~E(a18,x4461)),
% 259.56/259.61 inference(scs_inference,[],[343,33])).
% 259.56/259.61 cnf(462,plain,
% 259.56/259.61 (E(a17,a10)+P12(a10,a17)),
% 259.56/259.61 inference(scs_inference,[],[297,54,2])).
% 259.56/259.61 cnf(506,plain,
% 259.56/259.61 (P2(x5061,a20)+~E(a18,x5061)),
% 259.56/259.61 inference(scs_inference,[],[264,14])).
% 259.56/259.61 cnf(530,plain,
% 259.56/259.61 (P2(a11,x5301)+~E(a18,x5301)),
% 259.56/259.61 inference(scs_inference,[],[45,15])).
% 259.56/259.61 cnf(573,plain,
% 259.56/259.61 (P11(a10,a17)+E(a17,a10)),
% 259.56/259.61 inference(scs_inference,[],[462,57])).
% 259.56/259.61 cnf(591,plain,
% 259.56/259.61 (P11(a10,x5911)+~E(a17,x5911)+E(a17,a10)),
% 259.56/259.61 inference(scs_inference,[],[573,17])).
% 259.56/259.61 cnf(607,plain,
% 259.56/259.61 (E(f4(f5(f2(a1,a7))),f4(f5(a8)))),
% 259.56/259.61 inference(scs_inference,[],[36,8,9])).
% 259.56/259.61 cnf(938,plain,
% 259.56/259.61 (~E(f15(a1,a7),f15(a1,a12))+~P12(f15(a1,a13),f15(a1,a14))+~P12(f15(a1,a14),f15(a1,a12))),
% 259.56/259.61 inference(scs_inference,[],[90,2])).
% 259.56/259.61 cnf(955,plain,
% 259.56/259.61 (~P3(a1,a13)+P8(a1,a13)+E(f15(a1,a13),a17)),
% 259.56/259.61 inference(scs_inference,[],[98,48,35,70,74])).
% 259.56/259.61 cnf(956,plain,
% 259.56/259.61 (E(f15(a1,a13),a17)+P8(a1,a13)),
% 259.56/259.61 inference(scs_inference,[],[98,955])).
% 259.56/259.61 cnf(961,plain,
% 259.56/259.61 (E(f15(a1,a13),a17)+E(f15(a1,a13),a10)),
% 259.56/259.61 inference(scs_inference,[],[102,98,956,75])).
% 259.56/259.61 cnf(964,plain,
% 259.56/259.61 (E(a10,f15(a1,a13))+E(f15(a1,a13),a17)),
% 259.56/259.61 inference(scs_inference,[],[961,2])).
% 259.56/259.61 cnf(1022,plain,
% 259.56/259.61 (E(f2(a8,x10221),f2(f2(a1,a7),x10221))),
% 259.56/259.61 inference(scs_inference,[],[36,2,4])).
% 259.56/259.61 cnf(1023,plain,
% 259.56/259.61 (E(f2(f2(a1,a7),x10231),f2(a8,x10231))),
% 259.56/259.61 inference(scs_inference,[],[1022,2])).
% 259.56/259.61 cnf(1058,plain,
% 259.56/259.61 (E(f2(x10581,a8),f2(x10581,f2(a1,a7)))),
% 259.56/259.61 inference(scs_inference,[],[36,2,5])).
% 259.56/259.61 cnf(1059,plain,
% 259.56/259.61 (E(f2(x10591,f2(a1,a7)),f2(x10591,a8))),
% 259.56/259.61 inference(scs_inference,[],[1058,2])).
% 259.56/259.61 cnf(1060,plain,
% 259.56/259.61 (E(f2(f2(a1,a7),a8),f2(a8,f2(a1,a7)))),
% 259.56/259.61 inference(scs_inference,[],[1023,1058,2,3])).
% 259.56/259.61 cnf(1070,plain,
% 259.56/259.61 (E(f2(f2(a1,a7),f2(a1,a7)),f2(a8,a8))),
% 259.56/259.61 inference(scs_inference,[],[1023,1059,1060,2,3])).
% 259.56/259.61 cnf(1078,plain,
% 259.56/259.61 (E(f2(a8,a8),f2(f2(a1,a7),f2(a1,a7)))),
% 259.56/259.61 inference(scs_inference,[],[1070,2])).
% 259.56/259.61 cnf(1171,plain,
% 259.56/259.61 (P6(x11711,x11711)),
% 259.56/259.61 inference(rename_variables,[],[92])).
% 259.56/259.61 cnf(1172,plain,
% 259.56/259.61 (P6(f2(x11721,f2(a1,a7)),f2(x11721,a8))),
% 259.56/259.61 inference(scs_inference,[],[1058,92,1171,30,29])).
% 259.56/259.61 cnf(1268,plain,
% 259.56/259.61 (E(f15(a8,x12681),f15(f2(a1,a7),x12681))),
% 259.56/259.61 inference(scs_inference,[],[36,2,6])).
% 259.56/259.61 cnf(1269,plain,
% 259.56/259.61 (E(f15(f2(a1,a7),x12691),f15(a8,x12691))),
% 259.56/259.61 inference(scs_inference,[],[1268,2])).
% 259.56/259.61 cnf(1326,plain,
% 259.56/259.61 (E(f15(x13261,a8),f15(x13261,f2(a1,a7)))),
% 259.56/259.61 inference(scs_inference,[],[36,2,7])).
% 259.56/259.61 cnf(1327,plain,
% 259.56/259.61 (E(f15(x13271,f2(a1,a7)),f15(x13271,a8))),
% 259.56/259.61 inference(scs_inference,[],[1326,2])).
% 259.56/259.61 cnf(1328,plain,
% 259.56/259.61 (E(f15(f2(a1,a7),a8),f15(a8,f2(a1,a7)))),
% 259.56/259.61 inference(scs_inference,[],[1269,1326,2,3])).
% 259.56/259.61 cnf(1339,plain,
% 259.56/259.61 (E(f15(f2(a1,a7),f2(a1,a7)),f15(a8,a8))),
% 259.56/259.61 inference(scs_inference,[],[1269,1327,1328,2,3])).
% 259.56/259.61 cnf(1349,plain,
% 259.56/259.61 (E(f15(a8,a8),f15(f2(a1,a7),f2(a1,a7)))),
% 259.56/259.61 inference(scs_inference,[],[1339,2])).
% 259.56/259.61 cnf(1478,plain,
% 259.56/259.61 (P6(x14781,x14781)),
% 259.56/259.61 inference(rename_variables,[],[92])).
% 259.56/259.61 cnf(1481,plain,
% 259.56/259.61 (P11(f15(a8,x14811),f15(f2(a1,a7),x14811))),
% 259.56/259.61 inference(scs_inference,[],[1268,92,1478,91,30,29,17])).
% 259.56/259.61 cnf(1482,plain,
% 259.56/259.61 (P11(x14821,x14821)),
% 259.56/259.61 inference(rename_variables,[],[91])).
% 259.56/259.61 cnf(1483,plain,
% 259.56/259.61 (P11(f15(f2(a1,a7),x14831),f15(a8,x14831))),
% 259.56/259.61 inference(scs_inference,[],[1268,92,1478,91,1482,30,29,17,16])).
% 259.56/259.61 cnf(1554,plain,
% 259.56/259.61 (E(f4(a8),f4(f2(a1,a7)))),
% 259.56/259.61 inference(scs_inference,[],[36,2,8])).
% 259.56/259.61 cnf(1666,plain,
% 259.56/259.61 (E(f6(a8),f6(f2(a1,a7)))),
% 259.56/259.61 inference(scs_inference,[],[36,2,10])).
% 259.56/259.61 cnf(1667,plain,
% 259.56/259.61 (E(f6(f2(a1,a7)),f6(a8))),
% 259.56/259.61 inference(scs_inference,[],[1666,2])).
% 259.56/259.61 cnf(1727,plain,
% 259.56/259.61 (E(f2(f2(f2(a1,a7),f2(a1,a7)),x17271),f2(f2(a8,a8),x17271))),
% 259.56/259.61 inference(scs_inference,[],[1078,2,4])).
% 259.56/259.61 cnf(1728,plain,
% 259.56/259.61 (E(f3(a8),f3(f2(a1,a7)))),
% 259.56/259.61 inference(scs_inference,[],[36,2,11])).
% 259.56/259.61 cnf(1729,plain,
% 259.56/259.61 (E(f3(f2(a1,a7)),f3(a8))),
% 259.56/259.61 inference(scs_inference,[],[1728,2])).
% 259.56/259.61 cnf(1791,plain,
% 259.56/259.61 (P2(a19,f2(a1,a7))),
% 259.56/259.61 inference(scs_inference,[],[36,39,2,15])).
% 259.56/259.61 cnf(1931,plain,
% 259.56/259.61 (~P11(f2(a1,a14),a19)),
% 259.56/259.61 inference(scs_inference,[],[159,172,2,61])).
% 259.56/259.61 cnf(1932,plain,
% 259.56/259.61 (~E(f2(a1,a12),f2(a1,a14))),
% 259.56/259.61 inference(scs_inference,[],[1931,183])).
% 259.56/259.61 cnf(1934,plain,
% 259.56/259.61 (~E(f2(a1,a14),f2(a1,a12))),
% 259.56/259.61 inference(scs_inference,[],[1931,2,183])).
% 259.56/259.61 cnf(1935,plain,
% 259.56/259.61 (E(a9,f2(a1,a13))+P12(f2(a1,a13),a9)),
% 259.56/259.61 inference(scs_inference,[],[2,228])).
% 259.56/259.61 cnf(1936,plain,
% 259.56/259.61 (P2(a9,f2(a1,a13))+E(a9,f2(a1,a13))),
% 259.56/259.61 inference(scs_inference,[],[1935,60])).
% 259.56/259.61 cnf(1938,plain,
% 259.56/259.61 (~E(f2(a1,a7),f2(a1,a13))),
% 259.56/259.61 inference(scs_inference,[],[170,1791,15])).
% 259.56/259.61 cnf(1942,plain,
% 259.56/259.61 (~P6(f2(a1,a7),f2(a1,a14))),
% 259.56/259.61 inference(scs_inference,[],[125,236,2,62])).
% 259.56/259.61 cnf(1952,plain,
% 259.56/259.61 (E(a17,f15(a1,a13))+P8(a1,a13)),
% 259.56/259.61 inference(scs_inference,[],[102,98,2,70])).
% 259.56/259.61 cnf(1956,plain,
% 259.56/259.61 (E(a18,f15(a1,a7))+P10(a1,a7)),
% 259.56/259.61 inference(scs_inference,[],[100,98,2,71])).
% 259.56/259.61 cnf(1962,plain,
% 259.56/259.61 (~P10(a1,a7)+E(a10,f15(a1,a7))),
% 259.56/259.61 inference(scs_inference,[],[100,98,2,75])).
% 259.56/259.61 cnf(1963,plain,
% 259.56/259.61 (E(a10,f15(a1,a7))+E(a18,f15(a1,a7))),
% 259.56/259.61 inference(scs_inference,[],[1962,1956])).
% 259.56/259.61 cnf(1964,plain,
% 259.56/259.61 (P6(a10,f15(a1,a7))+E(a18,f15(a1,a7))),
% 259.56/259.61 inference(scs_inference,[],[92,1963,30])).
% 259.56/259.61 cnf(1983,plain,
% 259.56/259.61 (P11(f15(a1,a7),a10)+~P10(a1,a7)),
% 259.56/259.61 inference(scs_inference,[],[100,98,52,75])).
% 259.56/259.61 cnf(1984,plain,
% 259.56/259.61 (E(a18,f15(a1,a7))+P11(f15(a1,a7),a10)),
% 259.56/259.61 inference(scs_inference,[],[1983,1956])).
% 259.56/259.61 cnf(1996,plain,
% 259.56/259.61 (P6(f15(a1,a7),a18)+P10(a1,a7)),
% 259.56/259.61 inference(scs_inference,[],[100,98,53,71])).
% 259.56/259.61 cnf(2068,plain,
% 259.56/259.61 (~P6(a8,a9)),
% 259.56/259.61 inference(scs_inference,[],[123,142,58,62])).
% 259.56/259.61 cnf(2308,plain,
% 259.56/259.61 (~E(a7,a12)+E(f15(a1,a12),a18)),
% 259.56/259.61 inference(scs_inference,[],[104,98,143,71])).
% 259.56/259.61 cnf(2309,plain,
% 259.56/259.61 (P6(a18,f15(a1,a12))+~E(a7,a12)),
% 259.56/259.61 inference(scs_inference,[],[92,2308,29])).
% 259.56/259.61 cnf(2310,plain,
% 259.56/259.61 (P6(a18,x23101)+~E(f15(a1,a12),x23101)+~E(a7,a12)),
% 259.56/259.61 inference(scs_inference,[],[2309,30])).
% 259.56/259.61 cnf(2392,plain,
% 259.56/259.61 (~P11(f2(a1,a13),a19)),
% 259.56/259.61 inference(scs_inference,[],[35,164,80])).
% 259.56/259.61 cnf(2393,plain,
% 259.56/259.61 (~E(f2(a1,a12),f2(a1,a13))),
% 259.56/259.61 inference(scs_inference,[],[2392,183])).
% 259.56/259.61 cnf(2395,plain,
% 259.56/259.61 (~E(a9,a19)),
% 259.56/259.61 inference(scs_inference,[],[47,2392,183,5,17])).
% 259.56/259.61 cnf(2396,plain,
% 259.56/259.61 (~E(a19,f2(a1,a13))),
% 259.56/259.61 inference(scs_inference,[],[47,91,2392,183,5,17,16])).
% 259.56/259.61 cnf(2398,plain,
% 259.56/259.61 (P12(a19,a9)),
% 259.56/259.61 inference(scs_inference,[],[47,91,2392,183,5,17,16,425])).
% 259.56/259.61 cnf(2405,plain,
% 259.56/259.61 (~P8(a1,a13)+E(f15(a1,a13),a10)),
% 259.56/259.61 inference(scs_inference,[],[98,164,75])).
% 259.56/259.61 cnf(2406,plain,
% 259.56/259.61 (P6(a10,f15(a1,a13))+~P8(a1,a13)),
% 259.56/259.61 inference(scs_inference,[],[92,2405,29])).
% 259.56/259.61 cnf(2407,plain,
% 259.56/259.61 (P6(a10,x24071)+~E(f15(a1,a13),x24071)+~P8(a1,a13)),
% 259.56/259.61 inference(scs_inference,[],[2406,30])).
% 259.56/259.61 cnf(2411,plain,
% 259.56/259.61 (P10(a1,a7)+E(f15(a1,a7),a18)),
% 259.56/259.61 inference(scs_inference,[],[98,181,71])).
% 259.56/259.61 cnf(2425,plain,
% 259.56/259.61 (~P10(a1,a7)+E(f15(a1,a7),a10)),
% 259.56/259.61 inference(scs_inference,[],[98,181,75])).
% 259.56/259.61 cnf(2426,plain,
% 259.56/259.61 (E(a18,f15(a1,a7))+E(f15(a1,a7),a10)),
% 259.56/259.61 inference(scs_inference,[],[2425,1956])).
% 259.56/259.61 cnf(2628,plain,
% 259.56/259.61 (P12(a10,a17)),
% 259.56/259.61 inference(scs_inference,[],[2398,253,41,57,59,58])).
% 259.56/259.61 cnf(2630,plain,
% 259.56/259.61 (~E(a19,a9)),
% 259.56/259.61 inference(scs_inference,[],[2395,2398,253,41,57,59,58,2])).
% 259.56/259.61 cnf(2631,plain,
% 259.56/259.61 (~P2(f2(a1,a12),a19)),
% 259.56/259.61 inference(scs_inference,[],[35,2395,2398,253,41,104,57,59,58,2,74])).
% 259.56/259.61 cnf(2633,plain,
% 259.56/259.61 (~P8(a1,a14)),
% 259.56/259.61 inference(scs_inference,[],[35,2395,2398,253,41,104,121,100,57,59,58,2,74,87])).
% 259.56/259.61 cnf(2640,plain,
% 259.56/259.61 (E(f15(a1,a14),a17)),
% 259.56/259.61 inference(scs_inference,[],[35,316,2395,2398,1938,2068,389,249,140,253,41,104,98,121,100,36,57,59,58,2,74,87,61,62,29,70])).
% 259.56/259.61 cnf(2645,plain,
% 259.56/259.61 (E(f4(f15(a1,a14)),f4(a17))),
% 259.56/259.61 inference(scs_inference,[],[35,316,2395,2398,1938,2068,389,249,140,253,41,104,98,121,34,100,36,57,59,58,2,74,87,61,62,29,70,82,8])).
% 259.56/259.61 cnf(2647,plain,
% 259.56/259.61 (E(f6(f15(a1,a14)),f6(a17))),
% 259.56/259.61 inference(scs_inference,[],[35,316,2395,2398,1938,2068,389,249,140,253,41,104,98,121,34,100,36,57,59,58,2,74,87,61,62,29,70,82,8,9,10])).
% 259.56/259.61 cnf(2648,plain,
% 259.56/259.61 (E(f3(f15(a1,a14)),f3(a17))),
% 259.56/259.61 inference(scs_inference,[],[35,316,2395,2398,1938,2068,389,249,140,253,41,104,98,121,34,100,36,57,59,58,2,74,87,61,62,29,70,82,8,9,10,11])).
% 259.56/259.61 cnf(2649,plain,
% 259.56/259.61 (E(f15(f15(a1,a14),x26491),f15(a17,x26491))),
% 259.56/259.61 inference(scs_inference,[],[35,316,2395,2398,1938,2068,389,249,140,253,41,104,98,121,34,100,36,57,59,58,2,74,87,61,62,29,70,82,8,9,10,11,6])).
% 259.56/259.61 cnf(2650,plain,
% 259.56/259.61 (E(f15(x26501,f15(a1,a14)),f15(x26501,a17))),
% 259.56/259.61 inference(scs_inference,[],[35,316,2395,2398,1938,2068,389,249,140,253,41,104,98,121,34,100,36,57,59,58,2,74,87,61,62,29,70,82,8,9,10,11,6,7])).
% 259.56/259.61 cnf(2655,plain,
% 259.56/259.61 (E(f2(f15(a1,a14),x26551),f2(a17,x26551))),
% 259.56/259.61 inference(scs_inference,[],[35,316,2395,2398,1938,2068,389,249,140,253,41,104,98,121,34,100,36,57,59,58,2,74,87,61,62,29,70,82,8,9,10,11,6,7,52,53,4])).
% 259.56/259.61 cnf(2656,plain,
% 259.56/259.61 (E(f2(x26561,f15(a1,a14)),f2(x26561,a17))),
% 259.56/259.61 inference(scs_inference,[],[35,316,2395,2398,1938,2068,389,249,140,253,41,104,98,121,34,100,36,57,59,58,2,74,87,61,62,29,70,82,8,9,10,11,6,7,52,53,4,5])).
% 259.56/259.61 cnf(2658,plain,
% 259.56/259.61 (E(f15(f15(a1,a14),f2(a1,a7)),f15(a17,a8))),
% 259.56/259.61 inference(scs_inference,[],[35,316,2395,2398,1938,2068,389,249,140,253,1349,1327,41,104,98,121,34,100,36,57,59,58,2,74,87,61,62,29,70,82,8,9,10,11,6,7,52,53,4,5,25,3])).
% 259.56/259.61 cnf(2660,plain,
% 259.56/259.61 (~P12(a18,f15(a1,a14))),
% 259.56/259.61 inference(scs_inference,[],[35,316,2395,2398,1938,2068,403,389,249,140,253,1349,1327,41,104,98,121,34,100,36,57,59,58,2,74,87,61,62,29,70,82,8,9,10,11,6,7,52,53,4,5,25,3,33])).
% 259.56/259.61 cnf(2662,plain,
% 259.56/259.61 (~P12(f15(a1,a14),a20)),
% 259.56/259.61 inference(scs_inference,[],[35,316,2395,2398,1938,2068,403,389,325,249,140,253,272,1349,1327,41,104,98,121,34,100,36,57,59,58,2,74,87,61,62,29,70,82,8,9,10,11,6,7,52,53,4,5,25,3,33,14,32])).
% 259.56/259.61 cnf(2664,plain,
% 259.56/259.61 (P11(x26641,x26641)),
% 259.56/259.61 inference(rename_variables,[],[91])).
% 259.56/259.61 cnf(2667,plain,
% 259.56/259.61 (~P2(a10,f15(a1,a14))),
% 259.56/259.61 inference(scs_inference,[],[35,316,2395,2398,1938,2068,403,389,325,249,140,253,272,1349,1327,41,297,104,91,2664,98,121,34,100,36,57,59,58,2,74,87,61,62,29,70,82,8,9,10,11,6,7,52,53,4,5,25,3,33,14,32,17,16,15])).
% 259.56/259.61 cnf(2672,plain,
% 259.56/259.61 (P6(a18,a10)),
% 259.56/259.61 inference(scs_inference,[],[42,59])).
% 259.56/259.61 cnf(2674,plain,
% 259.56/259.61 (P6(f2(x26741,f15(a1,a14)),f2(x26741,a17))),
% 259.56/259.61 inference(scs_inference,[],[2656,42,59,53])).
% 259.56/259.61 cnf(2676,plain,
% 259.56/259.61 (P11(f2(x26761,f15(a1,a14)),f2(x26761,a17))),
% 259.56/259.61 inference(scs_inference,[],[2656,42,59,53,52])).
% 259.56/259.61 cnf(2678,plain,
% 259.56/259.61 (P12(f2(a1,a7),a19)),
% 259.56/259.61 inference(scs_inference,[],[2656,42,1791,59,53,52,58])).
% 259.56/259.61 cnf(2682,plain,
% 259.56/259.61 (~E(f2(a1,a13),f2(a1,a12))),
% 259.56/259.61 inference(scs_inference,[],[2628,2393,2656,42,1791,59,53,52,58,57,2])).
% 259.56/259.61 cnf(2683,plain,
% 259.56/259.61 (E(f2(f15(a1,a14),f15(a1,a14)),f2(a17,a17))),
% 259.56/259.61 inference(scs_inference,[],[2628,2393,2656,2655,42,1791,59,53,52,58,57,2,3])).
% 259.56/259.61 cnf(2686,plain,
% 259.56/259.61 (~P11(a18,a10)),
% 259.56/259.61 inference(scs_inference,[],[301,2628,2393,2656,2655,365,42,1791,59,53,52,58,57,2,3,61])).
% 259.56/259.61 cnf(2692,plain,
% 259.56/259.61 (~P12(a11,f15(a1,a14))),
% 259.56/259.61 inference(scs_inference,[],[301,2628,2393,2667,2656,2655,365,288,304,2640,327,42,1791,40,59,53,52,58,57,2,3,61,67,62,33])).
% 259.56/259.61 cnf(2693,plain,
% 259.56/259.61 (~P2(f15(a1,a14),a18)),
% 259.56/259.61 inference(scs_inference,[],[301,2628,2393,2667,2656,2655,365,288,304,2640,327,42,260,1791,40,59,53,52,58,57,2,3,61,67,62,33,14])).
% 259.56/259.61 cnf(2696,plain,
% 259.56/259.61 (~E(a20,f15(a1,a14))),
% 259.56/259.61 inference(scs_inference,[],[301,2628,2393,2667,2656,2655,1942,365,312,288,304,2640,327,42,260,1791,40,93,59,53,52,58,57,2,3,61,67,62,33,14,32,29,15])).
% 259.56/259.61 cnf(2710,plain,
% 259.56/259.61 (P11(f2(a1,a7),a19)),
% 259.56/259.61 inference(scs_inference,[],[2678,2683,107,59,53,52,57])).
% 259.56/259.61 cnf(2712,plain,
% 259.56/259.61 (P12(a17,a18)),
% 259.56/259.61 inference(scs_inference,[],[2678,2683,107,43,59,53,52,57,58])).
% 259.56/259.61 cnf(2715,plain,
% 259.56/259.61 (E(f15(f15(a1,a14),f15(a1,a14)),f15(a17,a17))),
% 259.56/259.61 inference(scs_inference,[],[2678,2696,2683,2650,2649,107,43,59,53,52,57,58,2,3])).
% 259.56/259.61 cnf(2720,plain,
% 259.56/259.61 (~P2(f2(a1,a12),f2(a1,a14))),
% 259.56/259.61 inference(scs_inference,[],[2678,2631,2662,2696,2683,2650,2649,138,107,43,59,53,52,57,58,2,3,61,67])).
% 259.56/259.61 cnf(2722,plain,
% 259.56/259.61 (~P6(a17,a11)),
% 259.56/259.61 inference(scs_inference,[],[332,2678,2631,2662,2696,2683,2650,2649,138,107,272,43,59,53,52,57,58,2,3,61,67,62])).
% 259.56/259.61 cnf(2724,plain,
% 259.56/259.61 (P2(f15(a1,a14),a20)),
% 259.56/259.61 inference(scs_inference,[],[332,2678,2631,2662,2696,2683,2650,2649,138,107,272,43,59,53,52,57,58,2,3,61,67,62,54])).
% 259.56/259.61 cnf(2726,plain,
% 259.56/259.61 (~E(a11,f15(a1,a14))),
% 259.56/259.61 inference(scs_inference,[],[332,2678,2631,2662,2693,2696,2683,2650,2649,138,107,272,43,45,59,53,52,57,58,2,3,61,67,62,54,14])).
% 259.56/259.61 cnf(2730,plain,
% 259.56/259.61 (P12(a8,a19)),
% 259.56/259.61 inference(scs_inference,[],[332,2678,2631,2662,2693,2696,2674,2683,2650,2649,138,107,272,43,45,36,59,53,52,57,58,2,3,61,67,62,54,14,29,25,32])).
% 259.56/259.61 cnf(2740,plain,
% 259.56/259.61 (P12(a20,f15(a1,a14))),
% 259.56/259.61 inference(scs_inference,[],[2724,2715,59,53,52,58])).
% 259.56/259.61 cnf(2745,plain,
% 259.56/259.61 (E(f2(f15(a1,a14),f2(a1,a7)),f2(a17,a8))),
% 259.56/259.61 inference(scs_inference,[],[2712,2724,2726,2715,2655,1059,59,53,52,58,57,2,3])).
% 259.56/259.61 cnf(2748,plain,
% 259.56/259.61 (~P11(a17,a20)),
% 259.56/259.61 inference(scs_inference,[],[357,2712,2724,2726,2715,2655,325,1059,59,53,52,58,57,2,3,61])).
% 259.56/259.61 cnf(2752,plain,
% 259.56/259.61 (P2(a11,f15(a1,a14))),
% 259.56/259.61 inference(scs_inference,[],[357,2712,2720,2692,2724,2726,2715,1932,2655,325,1059,59,53,52,58,57,2,3,61,62,54])).
% 259.56/259.61 cnf(2767,plain,
% 259.56/259.61 (P12(f15(a1,a14),a11)),
% 259.56/259.61 inference(scs_inference,[],[2740,2752,2745,52,59,53,57,58])).
% 259.56/259.61 cnf(2769,plain,
% 259.56/259.61 (E(f2(f2(a1,a7),f15(a1,a14)),f2(a8,a17))),
% 259.56/259.61 inference(scs_inference,[],[2740,2752,2745,2656,1023,52,59,53,57,58,3])).
% 259.56/259.61 cnf(2778,plain,
% 259.56/259.61 (P6(f2(a17,a8),f2(f15(a1,a14),a8))),
% 259.56/259.61 inference(scs_inference,[],[2630,2740,2752,2745,353,1172,345,2720,1932,2656,134,1023,52,59,53,57,58,3,61,62,54,29])).
% 259.56/259.61 cnf(2780,plain,
% 259.56/259.61 (P2(f2(a1,a14),f2(a1,a12))),
% 259.56/259.61 inference(scs_inference,[],[2630,2740,2752,2745,353,1172,345,2720,1932,2656,134,1023,52,59,53,57,58,3,61,62,54,29,60])).
% 259.56/259.61 cnf(2793,plain,
% 259.56/259.61 (P12(a20,a10)),
% 259.56/259.61 inference(scs_inference,[],[2780,2769,2648,40,53,52,59,58])).
% 259.56/259.62 cnf(2797,plain,
% 259.56/259.62 (E(f15(f2(a1,a7),f15(a1,a14)),f15(a8,a17))),
% 259.56/259.62 inference(scs_inference,[],[2780,2767,2769,2648,2650,40,1269,53,52,59,58,57,3])).
% 259.56/259.62 cnf(2818,plain,
% 259.56/259.62 (P12(a18,a11)),
% 259.56/259.62 inference(scs_inference,[],[2793,2797,217,45,59,53,52,57,58])).
% 259.56/259.62 cnf(2826,plain,
% 259.56/259.62 (P11(f15(a8,a17),f15(a8,f15(a1,a14)))),
% 259.56/259.62 inference(scs_inference,[],[2793,2797,2396,262,1483,1481,125,217,170,45,59,53,52,57,58,61,62,17,16])).
% 259.56/259.62 cnf(2839,plain,
% 259.56/259.62 (P12(a9,f2(a1,a14))),
% 259.56/259.62 inference(scs_inference,[],[2647,38,49,52,59,53,58])).
% 259.56/259.62 cnf(2841,plain,
% 259.56/259.62 (P11(a18,a11)),
% 259.56/259.62 inference(scs_inference,[],[2818,2647,38,49,52,59,53,58,57])).
% 259.56/259.62 cnf(2843,plain,
% 259.56/259.62 (~P11(a11,a17)),
% 259.56/259.62 inference(scs_inference,[],[2818,2647,266,288,38,49,52,59,53,58,57,61])).
% 259.56/259.62 cnf(2845,plain,
% 259.56/259.62 (~P6(a10,a18)),
% 259.56/259.62 inference(scs_inference,[],[2818,2647,266,288,278,339,38,49,52,59,53,58,57,61,62])).
% 259.56/259.62 cnf(2865,plain,
% 259.56/259.62 (~P6(a20,a18)),
% 259.56/259.62 inference(scs_inference,[],[2839,2645,2658,238,267,242,323,264,53,52,59,57,61,62])).
% 259.56/259.62 cnf(2880,plain,
% 259.56/259.62 (P6(f15(f15(a1,a14),x28801),f15(a17,x28801))),
% 259.56/259.62 inference(scs_inference,[],[2649,37,59,53])).
% 259.56/259.62 cnf(2911,plain,
% 259.56/259.62 (~P6(a20,a17)),
% 259.56/259.62 inference(scs_inference,[],[2730,2648,2658,317,108,310,52,59,53,57,62])).
% 259.56/259.62 cnf(2944,plain,
% 259.56/259.62 (P6(f15(x29441,f15(a1,a14)),f15(x29441,a17))),
% 259.56/259.62 inference(scs_inference,[],[2650,44,59,53])).
% 259.56/259.62 cnf(2946,plain,
% 259.56/259.62 (P11(f15(x29461,f15(a1,a14)),f15(x29461,a17))),
% 259.56/259.62 inference(scs_inference,[],[2650,44,59,53,52])).
% 259.56/259.62 cnf(2948,plain,
% 259.56/259.62 (P11(a10,a18)),
% 259.56/259.62 inference(scs_inference,[],[368,2650,44,59,53,52,57])).
% 259.56/259.62 cnf(2957,plain,
% 259.56/259.62 (P11(f15(f15(a1,a14),x29571),f15(a17,x29571))),
% 259.56/259.62 inference(scs_inference,[],[2649,52])).
% 259.56/259.62 cnf(2961,plain,
% 259.56/259.62 (P11(a20,a18)),
% 259.56/259.62 inference(scs_inference,[],[343,2649,240,52,59,57])).
% 259.56/259.62 cnf(3009,plain,
% 259.56/259.62 (P6(a11,a18)),
% 259.56/259.62 inference(scs_inference,[],[45,59])).
% 259.56/259.62 cnf(3228,plain,
% 259.56/259.62 (~P2(f2(a1,a12),a9)),
% 259.56/259.62 inference(scs_inference,[],[38,2631,14,2,67])).
% 259.56/259.62 cnf(3437,plain,
% 259.56/259.62 (~E(a17,a18)+~P6(a10,a17)),
% 259.56/259.62 inference(scs_inference,[],[278,297,62,3])).
% 259.56/259.62 cnf(3439,plain,
% 259.56/259.62 (~P12(a10,a10)+~P6(a10,a17)),
% 259.56/259.62 inference(scs_inference,[],[2911,312,278,297,62,3,30,32])).
% 259.56/259.62 cnf(3440,plain,
% 259.56/259.62 (~P11(a10,a20)+~P6(a10,a17)),
% 259.56/259.62 inference(scs_inference,[],[2911,2748,312,278,297,62,3,30,32,16])).
% 259.56/259.62 cnf(3445,plain,
% 259.56/259.62 (P11(f4(a10),f4(a17))+~P6(a10,a17)),
% 259.56/259.62 inference(scs_inference,[],[2911,2748,312,278,297,62,3,30,32,16,8,6,11,10,52])).
% 259.56/259.62 cnf(3639,plain,
% 259.56/259.62 (~P12(a11,x36391)+~E(x36391,a18)),
% 259.56/259.62 inference(scs_inference,[],[299,33])).
% 259.56/259.62 cnf(3801,plain,
% 259.56/259.62 (~P2(f2(a1,a12),f2(a1,a13))),
% 259.56/259.62 inference(scs_inference,[],[48,2631,67])).
% 259.56/259.62 cnf(3924,plain,
% 259.56/259.62 (~P11(f2(a1,a14),f2(a1,a12))+P12(f2(a1,a14),f2(a1,a12))),
% 259.56/259.62 inference(scs_inference,[],[1934,61])).
% 259.56/259.62 cnf(3973,plain,
% 259.56/259.62 (E(a17,a10)+~P11(a17,a10)),
% 259.56/259.62 inference(scs_inference,[],[312,61])).
% 259.56/259.62 cnf(4273,plain,
% 259.56/259.62 (~P2(a20,x42731)+~E(x42731,a18)),
% 259.56/259.62 inference(scs_inference,[],[323,15])).
% 259.56/259.62 cnf(4386,plain,
% 259.56/259.62 (~P2(x43861,a11)+~E(x43861,a18)),
% 259.56/259.62 inference(scs_inference,[],[286,14])).
% 259.56/259.62 cnf(4417,plain,
% 259.56/259.62 (~P12(x44171,a20)+~E(x44171,a18)),
% 259.56/259.62 inference(scs_inference,[],[341,32])).
% 259.56/259.62 cnf(4661,plain,
% 259.56/259.62 (~P8(a1,a12)+E(f15(a1,a12),a18)),
% 259.56/259.62 inference(scs_inference,[],[104,98,71])).
% 259.56/259.62 cnf(4715,plain,
% 259.56/259.62 (P11(f15(a17,a8),f15(f15(a1,a14),f2(a1,a7)))),
% 259.56/259.62 inference(scs_inference,[],[91,2658,16])).
% 259.56/259.62 cnf(4806,plain,
% 259.56/259.62 (P11(f15(a17,a8),f15(f15(a1,a14),a8))),
% 259.56/259.62 inference(scs_inference,[],[92,4715,1667,2645,1327,29,14,17])).
% 259.56/259.62 cnf(4856,plain,
% 259.56/259.62 (P6(f2(a8,a17),f2(f2(a1,a7),f15(a1,a14)))),
% 259.56/259.62 inference(scs_inference,[],[92,2769,29])).
% 259.56/259.62 cnf(5114,plain,
% 259.56/259.62 (~E(x51141,a20)+~E(a18,x51141)),
% 259.56/259.62 inference(scs_inference,[],[331,1554,27,3])).
% 259.56/259.62 cnf(5158,plain,
% 259.56/259.62 (~P11(f2(a1,a13),f2(a1,a12))+P12(f2(a1,a13),f2(a1,a12))),
% 259.56/259.62 inference(scs_inference,[],[2682,61])).
% 259.56/259.62 cnf(5272,plain,
% 259.56/259.62 (~E(x52721,a18)+~E(a20,x52721)),
% 259.56/259.62 inference(scs_inference,[],[267,1729,25,3])).
% 259.56/259.62 cnf(5334,plain,
% 259.56/259.62 (~E(x53341,a10)+~E(a18,x53341)),
% 259.56/259.62 inference(scs_inference,[],[301,2645,27,3])).
% 259.56/259.62 cnf(5638,plain,
% 259.56/259.62 (~E(x56381,a18)+~E(a10,x56381)),
% 259.56/259.62 inference(scs_inference,[],[278,3])).
% 259.56/259.62 cnf(6100,plain,
% 259.56/259.62 (E(f2(f2(f2(a1,a7),f2(a1,a7)),f15(a1,a14)),f2(f2(a8,a8),a17))),
% 259.56/259.62 inference(scs_inference,[],[607,1727,2656,92,52,53,6,11,8,7,9,10,4,5,29,3])).
% 259.56/259.62 cnf(6119,plain,
% 259.56/259.62 (P11(f2(f2(f2(a1,a7),f2(a1,a7)),f15(a1,a14)),f2(f2(a8,a8),a17))),
% 259.56/259.62 inference(scs_inference,[],[6100,52])).
% 259.56/259.62 cnf(6121,plain,
% 259.56/259.62 (P6(f2(f2(f2(a1,a7),f2(a1,a7)),f15(a1,a14)),f2(f2(a8,a8),a17))),
% 259.56/259.62 inference(scs_inference,[],[6100,52,53])).
% 259.56/259.62 cnf(6129,plain,
% 259.56/259.62 (E(f2(f2(f2(f2(a1,a7),f2(a1,a7)),f15(a1,a14)),x61291),f2(f2(f2(a8,a8),a17),x61291))),
% 259.56/259.62 inference(scs_inference,[],[6100,52,53,11,8,6,7,9,10,4])).
% 259.56/259.62 cnf(6151,plain,
% 259.56/259.62 (E(f15(x61511,a8),f15(x61511,f2(a1,a7)))),
% 259.56/259.62 inference(rename_variables,[],[1326])).
% 259.56/259.62 cnf(6155,plain,
% 259.56/259.62 (~P10(a1,a7)),
% 259.56/259.62 inference(scs_inference,[],[35,1326,6151,2647,2631,2880,2957,2710,2,60,17,30,80])).
% 259.56/259.62 cnf(6157,plain,
% 259.56/259.62 (E(f2(a8,f15(a1,a14)),f2(f2(a1,a7),a17))),
% 259.56/259.62 inference(scs_inference,[],[1022,35,1326,6151,2647,2656,2631,2880,2957,2710,2,60,17,30,80,3])).
% 259.56/259.62 cnf(6162,plain,
% 259.56/259.62 (E(f15(f2(a1,a7),x61621),f15(a8,x61621))),
% 259.56/259.62 inference(rename_variables,[],[1269])).
% 259.56/259.62 cnf(6170,plain,
% 259.56/259.62 (P8(a1,a12)),
% 259.56/259.62 inference(scs_inference,[],[34,100,36,1022,1269,6162,35,1326,6151,2647,2656,2631,2633,3228,2880,2944,2946,2957,2710,2,60,17,30,80,3,16,29,86,89,83])).
% 259.56/259.62 cnf(6172,plain,
% 259.56/259.62 (E(f15(a1,a12),a18)),
% 259.56/259.62 inference(scs_inference,[],[34,100,36,1022,1269,6162,35,1326,6151,2647,2656,2631,2633,3228,2880,2944,2946,2957,2710,2,60,17,30,80,3,16,29,86,89,83,4661])).
% 259.56/259.62 cnf(6194,plain,
% 259.56/259.62 (E(a18,f15(a1,a7))),
% 259.56/259.62 inference(scs_inference,[],[6155,1956])).
% 259.56/259.62 cnf(6196,plain,
% 259.56/259.62 (P6(f15(a1,a7),a18)),
% 259.56/259.62 inference(scs_inference,[],[6155,1996])).
% 259.56/259.62 cnf(6197,plain,
% 259.56/259.62 (E(f15(a1,a7),a18)),
% 259.56/259.62 inference(scs_inference,[],[6155,2411])).
% 259.56/259.62 cnf(6198,plain,
% 259.56/259.62 (E(f2(x61981,a17),f2(x61981,f15(a1,a14)))),
% 259.56/259.62 inference(scs_inference,[],[2656,2])).
% 259.56/259.62 cnf(6202,plain,
% 259.56/259.62 (~P12(f15(a1,a12),a20)),
% 259.56/259.62 inference(scs_inference,[],[2656,3801,6172,2,60,3639,4417])).
% 259.56/259.62 cnf(6204,plain,
% 259.56/259.62 (~P2(a20,f15(a1,a12))),
% 259.56/259.62 inference(scs_inference,[],[2656,3801,6172,2,60,3639,4417,4386,4273])).
% 259.56/259.62 cnf(6208,plain,
% 259.56/259.62 (E(f2(a8,x62081),f2(f2(a1,a7),x62081))),
% 259.56/259.62 inference(rename_variables,[],[1022])).
% 259.56/259.62 cnf(6211,plain,
% 259.56/259.62 (E(f2(a8,x62111),f2(f2(a1,a7),x62111))),
% 259.56/259.62 inference(rename_variables,[],[1022])).
% 259.56/259.62 cnf(6212,plain,
% 259.56/259.62 (E(f15(f15(a1,a14),a8),f15(a17,f2(a1,a7)))),
% 259.56/259.62 inference(scs_inference,[],[1022,6208,1326,2656,2649,3801,2674,6172,2676,2,60,3639,4417,4386,4273,5158,17,30,3])).
% 259.56/259.62 cnf(6214,plain,
% 259.56/259.62 (E(f15(x62141,a8),f15(x62141,f2(a1,a7)))),
% 259.56/259.62 inference(rename_variables,[],[1326])).
% 259.56/259.62 cnf(6217,plain,
% 259.56/259.62 (P6(f2(f2(a1,a7),a17),f2(f2(a1,a7),f15(a1,a14)))),
% 259.56/259.62 inference(scs_inference,[],[1022,6208,6211,1326,6214,2656,2649,3801,2674,4856,4715,6172,2676,2,60,3639,4417,4386,4273,5158,17,30,3,16,29])).
% 259.56/259.62 cnf(6240,plain,
% 259.56/259.62 (~P12(f15(a1,a7),a20)),
% 259.56/259.62 inference(scs_inference,[],[2649,2720,6197,2,60,3639,4417])).
% 259.56/259.62 cnf(6244,plain,
% 259.56/259.62 (~E(f15(a1,a7),a20)),
% 259.56/259.62 inference(scs_inference,[],[2649,2720,6197,6194,2,60,3639,4417,4386,4273,506,5114])).
% 259.56/259.62 cnf(6251,plain,
% 259.56/259.62 (~E(a10,f15(a1,a12))),
% 259.56/259.62 inference(scs_inference,[],[2649,2720,278,6172,6197,6194,6198,3009,6119,2,60,3639,4417,4386,4273,506,5114,3924,530,446,17,30,3])).
% 259.56/259.62 cnf(6254,plain,
% 259.56/259.62 (~E(f15(a1,a7),a10)),
% 259.56/259.62 inference(scs_inference,[],[2649,2845,2720,278,6172,2818,6197,6194,6198,3009,6196,2841,6119,2,60,3639,4417,4386,4273,506,5114,3924,530,446,17,30,3,16,32,29])).
% 259.56/259.62 cnf(6263,plain,
% 259.56/259.62 (E(a18,f15(a1,a7))),
% 259.56/259.62 inference(scs_inference,[],[6254,2426])).
% 259.56/259.62 cnf(6272,plain,
% 259.56/259.62 (E(f15(a1,a12),f15(a1,a7))),
% 259.56/259.62 inference(scs_inference,[],[1023,2745,6194,3228,6172,6217,2948,2,60,17,30,3])).
% 259.56/259.62 cnf(6273,plain,
% 259.56/259.62 (P11(f2(f2(f2(a1,a7),f2(a1,a7)),a17),f2(f2(a8,a8),a17))),
% 259.56/259.62 inference(scs_inference,[],[1023,2656,2745,6194,3228,6172,6119,6217,2948,2,60,17,30,3,16])).
% 259.56/259.62 cnf(6287,plain,
% 259.56/259.62 (~P12(f15(a1,a13),f15(a1,a14))+~P12(f15(a1,a14),f15(a1,a12))),
% 259.56/259.62 inference(scs_inference,[],[6272,90])).
% 259.56/259.62 cnf(6289,plain,
% 259.56/259.62 (E(f15(a8,a17),f15(f2(a1,a7),f15(a1,a14)))),
% 259.56/259.62 inference(scs_inference,[],[2797,2])).
% 259.56/259.62 cnf(6291,plain,
% 259.56/259.62 (E(f2(x62911,a17),f2(x62911,f15(a1,a14)))),
% 259.56/259.62 inference(rename_variables,[],[6198])).
% 259.56/259.62 cnf(6293,plain,
% 259.56/259.62 (E(f2(x62931,a17),f2(x62931,f15(a1,a14)))),
% 259.56/259.62 inference(rename_variables,[],[6198])).
% 259.56/259.62 cnf(6297,plain,
% 259.56/259.62 (P11(f15(f2(a1,a7),a17),f15(a8,f15(a1,a14)))),
% 259.56/259.62 inference(scs_inference,[],[1022,1268,2797,6198,6291,6293,6121,2826,6273,2,17,30,3,16])).
% 259.56/259.62 cnf(6306,plain,
% 259.56/259.62 (E(f2(a17,x63061),f2(f15(a1,a14),x63061))),
% 259.56/259.62 inference(scs_inference,[],[2655,2])).
% 259.56/259.62 cnf(6315,plain,
% 259.56/259.62 (P6(f2(f2(f2(a1,a7),f2(a1,a7)),a17),f2(f2(a8,a8),a17))),
% 259.56/259.62 inference(scs_inference,[],[1269,1268,1326,2656,1058,2655,6121,6289,2778,4806,6297,2,17,30,3,16,29])).
% 259.56/259.62 cnf(6329,plain,
% 259.56/259.62 (E(f2(a17,f15(a1,a14)),f2(f15(a1,a14),a17))),
% 259.56/259.62 inference(scs_inference,[],[2656,2658,6194,6198,6306,6315,2961,2,17,30,3])).
% 259.56/259.62 cnf(6344,plain,
% 259.56/259.62 (E(a17,f15(a1,a14))),
% 259.56/259.62 inference(scs_inference,[],[2640,2])).
% 259.56/259.62 cnf(6363,plain,
% 259.56/259.62 (E(f15(x63631,a17),f15(x63631,f15(a1,a14)))),
% 259.56/259.62 inference(scs_inference,[],[2650,2])).
% 259.56/259.62 cnf(6396,plain,
% 259.56/259.62 (E(f15(a17,a17),f15(f15(a1,a14),f15(a1,a14)))),
% 259.56/259.62 inference(scs_inference,[],[2715,2])).
% 259.56/259.62 cnf(6403,plain,
% 259.56/259.62 (~P2(a10,f15(a1,a7))),
% 259.56/259.62 inference(scs_inference,[],[2656,2715,6194,6129,6254,2672,2,3,29,62,65])).
% 259.56/259.62 cnf(6405,plain,
% 259.56/259.62 (~P12(f15(a1,a7),a10)),
% 259.56/259.62 inference(scs_inference,[],[2656,2715,6194,6129,6254,2672,2,3,29,62,65,60])).
% 259.56/259.62 cnf(6438,plain,
% 259.56/259.62 (E(f2(a17,a17),f2(f15(a1,a14),f15(a1,a14)))),
% 259.56/259.62 inference(scs_inference,[],[2683,2])).
% 259.56/259.62 cnf(6470,plain,
% 259.56/259.62 (E(a18,f15(a1,a12))),
% 259.56/259.62 inference(scs_inference,[],[6172,2])).
% 259.56/259.62 cnf(6471,plain,
% 259.56/259.62 (P2(f15(a1,a12),a20)),
% 259.56/259.62 inference(scs_inference,[],[6172,2,506])).
% 259.56/259.62 cnf(6472,plain,
% 259.56/259.62 (~E(f15(a1,a12),a20)),
% 259.56/259.62 inference(scs_inference,[],[6172,2,506,5114])).
% 259.56/259.62 cnf(6473,plain,
% 259.56/259.62 (P2(a11,f15(a1,a12))),
% 259.56/259.62 inference(scs_inference,[],[6172,2,506,5114,530])).
% 259.56/259.62 cnf(6474,plain,
% 259.56/259.62 (P12(a20,f15(a1,a12))),
% 259.56/259.62 inference(scs_inference,[],[6172,2,506,5114,530,446])).
% 259.56/259.62 cnf(6614,plain,
% 259.56/259.62 (E(f2(f2(a1,a7),a17),f2(a8,f15(a1,a14)))),
% 259.56/259.62 inference(scs_inference,[],[6157,2])).
% 259.56/259.62 cnf(6620,plain,
% 259.56/259.62 (E(f15(a17,f2(a1,a7)),f15(f15(a1,a14),a8))),
% 259.56/259.62 inference(scs_inference,[],[6212,2])).
% 259.56/259.62 cnf(6626,plain,
% 259.56/259.62 (E(f2(f15(a1,a14),a17),f2(a17,f15(a1,a14)))),
% 259.56/259.62 inference(scs_inference,[],[6329,2])).
% 259.56/259.62 cnf(6743,plain,
% 259.56/259.62 (E(f15(a1,a7),f15(a1,a12))),
% 259.56/259.62 inference(scs_inference,[],[6272,2])).
% 259.56/259.62 cnf(6749,plain,
% 259.56/259.62 (~P12(f15(a1,a13),f15(a1,a14))+~P12(f15(a1,a14),f15(a1,a12))),
% 259.56/259.62 inference(scs_inference,[],[6743,938])).
% 259.56/259.62 cnf(7449,plain,
% 259.56/259.62 (P12(x74491,f2(a1,a14))+~E(a9,x74491)),
% 259.56/259.62 inference(scs_inference,[],[2839,32])).
% 259.56/259.62 cnf(7476,plain,
% 259.56/259.62 (~E(a10,f15(a1,a7))),
% 259.56/259.62 inference(scs_inference,[],[6197,5272,5638])).
% 259.56/259.62 cnf(7477,plain,
% 259.56/259.62 (~E(f15(a1,a12),a10)),
% 259.56/259.62 inference(scs_inference,[],[6197,6470,5272,5638,5334])).
% 259.56/259.62 cnf(7486,plain,
% 259.56/259.62 (E(f4(f15(a1,a12)),f4(f15(a1,a7)))),
% 259.56/259.62 inference(scs_inference,[],[6614,6620,6474,6272,6471,6197,6470,5272,5638,5334,59,57,53,52,8])).
% 259.56/259.62 cnf(7487,plain,
% 259.56/259.62 (E(f15(f15(a1,a12),x74871),f15(f15(a1,a7),x74871))),
% 259.56/259.62 inference(scs_inference,[],[6614,6620,6474,6272,6471,6197,6470,5272,5638,5334,59,57,53,52,8,6])).
% 259.56/259.62 cnf(7488,plain,
% 259.56/259.62 (E(f3(f15(a1,a12)),f3(f15(a1,a7)))),
% 259.56/259.62 inference(scs_inference,[],[6614,6620,6474,6272,6471,6197,6470,5272,5638,5334,59,57,53,52,8,6,11])).
% 259.56/259.62 cnf(7489,plain,
% 259.56/259.62 (E(f15(x74891,f15(a1,a12)),f15(x74891,f15(a1,a7)))),
% 259.56/259.62 inference(scs_inference,[],[6614,6620,6474,6272,6471,6197,6470,5272,5638,5334,59,57,53,52,8,6,11,7])).
% 259.56/259.62 cnf(7495,plain,
% 259.56/259.62 (P12(f15(a1,a12),a11)),
% 259.56/259.62 inference(scs_inference,[],[34,6614,6620,6474,6170,6272,2633,6471,6473,6197,6470,5272,5638,5334,59,57,53,52,8,6,11,7,9,10,4,83,58])).
% 259.56/259.62 cnf(7499,plain,
% 259.56/259.62 (~P2(a10,f15(a1,a12))),
% 259.56/259.62 inference(scs_inference,[],[34,6403,6614,6620,6474,6170,6272,2633,6471,6473,6197,6470,5272,5638,5334,59,57,53,52,8,6,11,7,9,10,4,83,58,82,15])).
% 259.56/259.62 cnf(7500,plain,
% 259.56/259.62 (P12(a10,f15(a1,a12))),
% 259.56/259.62 inference(scs_inference,[],[34,6251,6403,6614,6620,6474,6170,6272,2633,6471,6473,6197,6470,5272,5638,5334,59,57,53,52,8,6,11,7,9,10,4,83,58,82,15,54])).
% 259.56/259.62 cnf(7503,plain,
% 259.56/259.62 (~P12(f15(a1,a12),a10)),
% 259.56/259.62 inference(scs_inference,[],[34,6251,6405,6403,6614,6620,6474,6170,6272,2633,6471,6473,6197,6470,5272,5638,5334,59,57,53,52,8,6,11,7,9,10,4,83,58,82,15,54,5,32])).
% 259.56/259.62 cnf(7506,plain,
% 259.56/259.62 (~P6(a10,f15(a1,a7))),
% 259.56/259.62 inference(scs_inference,[],[34,6244,6251,6405,6240,6403,6614,6620,6474,6170,6272,2633,6471,6473,6197,6470,5272,5638,5334,59,57,53,52,8,6,11,7,9,10,4,83,58,82,15,54,5,32,61,62])).
% 259.56/259.62 cnf(7508,plain,
% 259.56/259.62 (~E(a20,f15(a1,a12))),
% 259.56/259.62 inference(scs_inference,[],[34,6244,6251,6405,6240,6403,6614,6620,6474,6170,6272,2633,6471,6473,6197,6470,5272,5638,5334,59,57,53,52,8,6,11,7,9,10,4,83,58,82,15,54,5,32,61,62,3])).
% 259.56/259.62 cnf(7513,plain,
% 259.56/259.62 (P11(x75131,x75131)),
% 259.56/259.62 inference(rename_variables,[],[91])).
% 259.56/259.62 cnf(7518,plain,
% 259.56/259.62 (P2(f15(a1,a12),a10)),
% 259.56/259.62 inference(scs_inference,[],[34,91,7513,92,6244,6251,6405,6240,6403,6614,6620,6474,6438,6626,6170,6272,6743,2865,2633,6471,6473,6197,6470,5272,5638,5334,59,57,53,52,8,6,11,7,9,10,4,83,58,82,15,54,5,32,61,62,3,30,29,17,16,2310,60])).
% 259.56/259.62 cnf(7525,plain,
% 259.56/259.62 (E(a18,f15(a1,a7))),
% 259.56/259.62 inference(scs_inference,[],[7476,1963])).
% 259.56/259.62 cnf(7526,plain,
% 259.56/259.62 (E(a18,f15(a1,a7))),
% 259.56/259.62 inference(scs_inference,[],[7506,1964])).
% 259.56/259.62 cnf(7544,plain,
% 259.56/259.62 (~P2(f15(a1,a14),f15(a1,a7))),
% 259.56/259.62 inference(scs_inference,[],[7525,7495,7518,2693,6197,59,52,7,57,9,53,4,11,10,6,8,15])).
% 259.56/259.62 cnf(7546,plain,
% 259.56/259.62 (~P2(a17,f15(a1,a7))),
% 259.56/259.62 inference(scs_inference,[],[7525,7495,7518,2693,6197,6344,59,52,7,57,9,53,4,11,10,6,8,15,5,14])).
% 259.56/259.62 cnf(7549,plain,
% 259.56/259.62 (~P12(f15(a1,a7),f15(a1,a14))),
% 259.56/259.62 inference(scs_inference,[],[7525,7495,7477,7503,7518,2693,2660,6197,6344,59,52,7,57,9,53,4,11,10,6,8,15,5,14,61,32])).
% 259.56/259.62 cnf(7552,plain,
% 259.56/259.62 (E(f15(f15(a1,a12),f15(a1,a12)),f15(f15(a1,a7),f15(a1,a7)))),
% 259.56/259.62 inference(scs_inference,[],[7525,7487,7489,7495,7477,7508,7503,7518,6204,2693,2660,6197,6344,59,52,7,57,9,53,4,11,10,6,8,15,5,14,61,32,62,3])).
% 259.56/259.62 cnf(7557,plain,
% 259.56/259.62 (~P11(f15(a1,a7),a10)),
% 259.56/259.62 inference(scs_inference,[],[92,7525,7486,7487,7489,7495,7477,7508,7503,7518,6204,2693,2660,2686,6197,6344,59,52,7,57,9,53,4,11,10,6,8,15,5,14,61,32,62,3,30,16])).
% 259.56/259.62 cnf(7563,plain,
% 259.56/259.62 (E(a18,f15(a1,a7))),
% 259.56/259.62 inference(scs_inference,[],[7557,1984])).
% 259.56/259.62 cnf(7573,plain,
% 259.56/259.62 (E(f2(f15(a1,a7),x75731),f2(f15(a1,a12),x75731))),
% 259.56/259.62 inference(scs_inference,[],[7552,7500,6743,6473,52,59,57,4])).
% 259.56/259.62 cnf(7578,plain,
% 259.56/259.62 (~P2(f15(a1,a14),f15(a1,a12))),
% 259.56/259.62 inference(scs_inference,[],[7544,7552,7500,6272,6743,6473,52,59,57,4,7,53,8,15])).
% 259.56/259.62 cnf(7582,plain,
% 259.56/259.62 (E(f5(f15(a1,a7)),f5(f15(a1,a12)))),
% 259.56/259.62 inference(scs_inference,[],[7544,7552,7500,6272,6743,6473,52,59,57,4,7,53,8,15,6,10,11,9])).
% 259.56/259.62 cnf(7589,plain,
% 259.56/259.62 (~P12(f15(a1,a7),a17)),
% 259.56/259.62 inference(scs_inference,[],[7544,7549,7552,7499,7500,6472,6251,6202,6272,6743,6473,6344,52,59,57,4,7,53,8,15,6,10,11,9,5,61,32,62,33])).
% 259.56/259.62 cnf(7607,plain,
% 259.56/259.62 (E(f2(f15(a1,a7),x76071),f2(a18,x76071))),
% 259.56/259.62 inference(scs_inference,[],[7573,6197,52,4])).
% 259.56/259.62 cnf(7614,plain,
% 259.56/259.62 (E(f15(x76141,f15(a1,a7)),f15(x76141,a18))),
% 259.56/259.62 inference(scs_inference,[],[7573,6197,52,4,8,53,11,9,10,7])).
% 259.56/259.62 cnf(7615,plain,
% 259.56/259.62 (E(f15(f15(a1,a7),x76151),f15(a18,x76151))),
% 259.56/259.62 inference(scs_inference,[],[7573,6197,52,4,8,53,11,9,10,7,6])).
% 259.56/259.62 cnf(7616,plain,
% 259.56/259.62 (~P2(a17,f15(a1,a12))),
% 259.56/259.62 inference(scs_inference,[],[7578,7573,6197,6344,52,4,8,53,11,9,10,7,6,14])).
% 259.56/259.62 cnf(7617,plain,
% 259.56/259.62 (E(f2(x76171,f15(a1,a7)),f2(x76171,a18))),
% 259.56/259.62 inference(scs_inference,[],[7578,7573,6197,6344,52,4,8,53,11,9,10,7,6,14,5])).
% 259.56/259.62 cnf(7631,plain,
% 259.56/259.62 (E(f2(a18,x76311),f2(f15(a1,a12),x76311))),
% 259.56/259.62 inference(scs_inference,[],[7607,6470,52,53,4])).
% 259.56/259.62 cnf(7636,plain,
% 259.56/259.62 (E(f15(a18,x76361),f15(f15(a1,a12),x76361))),
% 259.56/259.62 inference(scs_inference,[],[7607,6470,52,53,4,8,10,11,7,6])).
% 259.56/259.62 cnf(7638,plain,
% 259.56/259.62 (E(f2(x76381,a18),f2(x76381,f15(a1,a12)))),
% 259.56/259.62 inference(scs_inference,[],[7607,6470,52,53,4,8,10,11,7,6,9,5])).
% 259.56/259.62 cnf(7893,plain,
% 259.56/259.62 (P11(f2(x78931,f15(a1,a7)),f2(x78931,a18))),
% 259.56/259.62 inference(scs_inference,[],[7617,52])).
% 259.56/259.62 cnf(8227,plain,
% 259.56/259.62 (E(f15(a18,f15(a1,a7)),f15(f15(a1,a12),a18))),
% 259.56/259.62 inference(scs_inference,[],[7614,7636,7582,7488,52,53,3])).
% 259.56/259.62 cnf(8326,plain,
% 259.56/259.62 (E(f2(a18,a18),f2(f15(a1,a12),f15(a1,a12)))),
% 259.56/259.62 inference(scs_inference,[],[7638,7631,6396,52,53,3])).
% 259.56/259.62 cnf(8416,plain,
% 259.56/259.62 (E(f2(a18,f15(a1,a7)),f2(f15(a1,a12),f15(a1,a12)))),
% 259.56/259.62 inference(scs_inference,[],[8326,7617,6363,6198,52,53,3])).
% 259.56/259.62 cnf(8437,plain,
% 259.56/259.62 (P2(f15(a1,a14),a10)),
% 259.56/259.62 inference(scs_inference,[],[8416,6344,41,2,14])).
% 259.56/259.62 cnf(8439,plain,
% 259.56/259.62 (P2(a18,f15(a1,a14))),
% 259.56/259.62 inference(scs_inference,[],[8416,6344,2712,41,43,2,14,32,15])).
% 259.56/259.62 cnf(8440,plain,
% 259.56/259.62 (E(f2(f15(a1,a7),f15(a1,a7)),f2(f15(a1,a12),f15(a1,a12)))),
% 259.56/259.62 inference(scs_inference,[],[8416,7607,6344,2712,41,43,2,14,32,15,3])).
% 259.56/259.62 cnf(8457,plain,
% 259.56/259.62 (P2(f15(a1,a7),f15(a1,a14))),
% 259.56/259.62 inference(scs_inference,[],[8439,8440,7563,2,14])).
% 259.56/259.62 cnf(8458,plain,
% 259.56/259.62 (P2(f15(a1,a7),a17)),
% 259.56/259.62 inference(scs_inference,[],[8439,8440,7563,2640,2,14,15])).
% 259.56/259.62 cnf(8459,plain,
% 259.56/259.62 (E(f15(f15(a1,a7),f15(a1,a7)),f15(f15(a1,a12),a18))),
% 259.56/259.62 inference(scs_inference,[],[8439,8440,8227,7615,7563,2640,2,14,15,3])).
% 259.56/259.62 cnf(8477,plain,
% 259.56/259.62 (P2(f15(a1,a12),f15(a1,a14))),
% 259.56/259.62 inference(scs_inference,[],[8457,8459,6743,2,14])).
% 259.56/259.62 cnf(8478,plain,
% 259.56/259.62 (P2(f15(a1,a12),a17)),
% 259.56/259.62 inference(scs_inference,[],[8457,8459,6743,2640,2,14,15])).
% 259.56/259.62 cnf(9737,plain,
% 259.56/259.62 (E(f6(f6(f15(a1,a14))),f6(f6(a17)))),
% 259.56/259.62 inference(scs_inference,[],[2655,2647,4,10])).
% 259.56/259.62 cnf(9816,plain,
% 259.56/259.62 (P12(f15(a1,a14),f15(a1,a12))),
% 259.56/259.62 inference(scs_inference,[],[8477,59,58])).
% 259.56/259.62 cnf(9834,plain,
% 259.56/259.62 (~P12(f15(a1,a13),f15(a1,a14))),
% 259.56/259.62 inference(scs_inference,[],[9816,6287])).
% 259.56/259.62 cnf(9835,plain,
% 259.56/259.62 (~P12(f15(a1,a13),f15(a1,a14))),
% 259.56/259.62 inference(scs_inference,[],[9816,6749])).
% 259.56/259.62 cnf(9840,plain,
% 259.56/259.62 (E(f2(f6(f6(f15(a1,a14))),x98401),f2(f6(f6(a17)),x98401))),
% 259.56/259.62 inference(scs_inference,[],[9737,8478,59,58,4])).
% 259.56/259.62 cnf(9842,plain,
% 259.56/259.62 (E(f15(f6(f6(f15(a1,a14))),x98421),f15(f6(f6(a17)),x98421))),
% 259.56/259.62 inference(scs_inference,[],[9737,8478,59,58,4,10,6])).
% 259.56/259.62 cnf(9878,plain,
% 259.56/259.62 (~P12(f15(a1,a13),a17)),
% 259.56/259.62 inference(scs_inference,[],[9834,9840,8458,8457,2740,6344,59,58,10,4,52,6,11,8,7,9,5,53,32,33])).
% 259.56/259.62 cnf(9879,plain,
% 259.56/259.62 (~E(f15(a1,a13),a20)),
% 259.56/259.62 inference(scs_inference,[],[9834,9840,8458,8457,2740,6344,59,58,10,4,52,6,11,8,7,9,5,53,32,33,2])).
% 259.56/259.62 cnf(9889,plain,
% 259.56/259.62 (P12(a10,f15(a1,a14))),
% 259.56/259.62 inference(scs_inference,[],[8437,58])).
% 259.56/259.62 cnf(9891,plain,
% 259.56/259.62 (E(f2(f15(f6(f6(f15(a1,a14))),x98911),x98912),f2(f15(f6(f6(a17)),x98911),x98912))),
% 259.56/259.62 inference(scs_inference,[],[9842,8437,58,4])).
% 259.56/259.62 cnf(9895,plain,
% 259.56/259.62 (E(f15(x98951,f15(f6(f6(f15(a1,a14))),x98952)),f15(x98951,f15(f6(f6(a17)),x98952)))),
% 259.56/259.62 inference(scs_inference,[],[9842,8437,58,4,10,52,7])).
% 259.56/259.62 cnf(9924,plain,
% 259.56/259.62 (P11(f2(f15(f6(f6(f15(a1,a14))),x99241),x99242),f2(f15(f6(f6(a17)),x99241),x99242))),
% 259.56/259.62 inference(scs_inference,[],[9891,8457,58,4,10,52])).
% 259.56/259.62 cnf(9931,plain,
% 259.56/259.62 (P6(f2(f15(f6(f6(f15(a1,a14))),x99311),x99312),f2(f15(f6(f6(a17)),x99311),x99312))),
% 259.56/259.62 inference(scs_inference,[],[9891,8457,58,4,10,52,6,8,7,11,9,53])).
% 259.56/259.62 cnf(9948,plain,
% 259.56/259.62 (E(f2(f15(x99481,f15(f6(f6(f15(a1,a14))),x99482)),x99483),f2(f15(x99481,f15(f6(f6(a17)),x99482)),x99483))),
% 259.56/259.62 inference(scs_inference,[],[9895,4])).
% 259.56/259.62 cnf(9952,plain,
% 259.56/259.62 (E(f15(f15(x99521,f15(f6(f6(f15(a1,a14))),x99522)),x99523),f15(f15(x99521,f15(f6(f6(a17)),x99522)),x99523))),
% 259.56/259.62 inference(scs_inference,[],[9895,4,52,10,6])).
% 259.56/259.62 cnf(9954,plain,
% 259.56/259.62 (E(f15(x99541,f15(x99542,f15(f6(f6(f15(a1,a14))),x99543))),f15(x99541,f15(x99542,f15(f6(f6(a17)),x99543))))),
% 259.56/259.62 inference(scs_inference,[],[9895,4,52,10,6,8,7])).
% 259.56/259.62 cnf(9980,plain,
% 259.56/259.62 (~E(a10,f15(a1,a13))),
% 259.56/259.62 inference(scs_inference,[],[9835,9948,9889,52,4,10,6,7,8,53,11,9,5,32])).
% 259.56/259.62 cnf(9982,plain,
% 259.56/259.62 (E(f2(f15(x99821,f15(f6(f6(f15(a1,a14))),x99822)),x99823),f2(f15(x99821,f15(f6(f6(a17)),x99822)),x99823))),
% 259.56/259.62 inference(rename_variables,[],[9948])).
% 259.56/259.62 cnf(9987,plain,
% 259.56/259.62 (E(f15(a1,a13),a17)),
% 259.56/259.62 inference(scs_inference,[],[9924,9931,9835,9948,9982,9889,52,4,10,6,7,8,53,11,9,5,32,30,16,964])).
% 259.56/259.62 cnf(9991,plain,
% 259.56/259.62 (~E(a17,a10)),
% 259.56/259.62 inference(scs_inference,[],[9924,9931,9835,9948,9982,9889,52,4,10,6,7,8,53,11,9,5,32,30,16,964,2,2407,3])).
% 259.56/259.62 cnf(9996,plain,
% 259.56/259.62 (~P8(a1,a13)),
% 259.56/259.62 inference(scs_inference,[],[9924,9931,9835,9948,9982,9889,52,4,10,6,7,8,53,11,9,5,32,30,16,964,2,2407,3,3445,3439,3440,3437,2405])).
% 259.56/259.62 cnf(9999,plain,
% 259.56/259.62 (~E(a17,x99991)+P11(a10,x99991)),
% 259.56/259.62 inference(scs_inference,[],[9991,591])).
% 259.56/259.62 cnf(10000,plain,
% 259.56/259.62 (E(a17,f15(a1,a13))),
% 259.56/259.62 inference(scs_inference,[],[9996,1952])).
% 259.56/259.62 cnf(10003,plain,
% 259.56/259.62 (~P11(a17,a10)),
% 259.56/259.62 inference(scs_inference,[],[9991,3973])).
% 259.56/259.62 cnf(10004,plain,
% 259.56/259.62 (P11(f15(f15(x100041,f15(f6(f6(f15(a1,a14))),x100042)),x100043),f15(f15(x100041,f15(f6(f6(a17)),x100042)),x100043))),
% 259.56/259.62 inference(scs_inference,[],[9952,52])).
% 259.56/259.62 cnf(10006,plain,
% 259.56/259.62 (E(f2(f15(a1,a13),x100061),f2(a17,x100061))),
% 259.56/259.62 inference(scs_inference,[],[9987,9952,52,4])).
% 259.56/259.62 cnf(10007,plain,
% 259.56/259.62 (E(f6(f15(a1,a13)),f6(a17))),
% 259.56/259.62 inference(scs_inference,[],[9987,9952,52,4,10])).
% 259.56/259.62 cnf(10022,plain,
% 259.56/259.62 (~P2(a10,f15(a1,a13))),
% 259.56/259.62 inference(scs_inference,[],[9991,9987,9952,9879,325,297,52,4,10,53,7,6,11,8,9,5,2,32,62,61,15])).
% 259.56/259.62 cnf(10023,plain,
% 259.56/259.62 (~P2(f15(a1,a13),f15(a1,a7))),
% 259.56/259.62 inference(scs_inference,[],[9991,9987,9952,9879,7546,325,297,52,4,10,53,7,6,11,8,9,5,2,32,62,61,15,14])).
% 259.56/259.62 cnf(10024,plain,
% 259.56/259.62 (~P12(f15(a1,a13),f15(a1,a13))),
% 259.56/259.62 inference(scs_inference,[],[9991,9987,9952,9879,7546,9878,325,297,52,4,10,53,7,6,11,8,9,5,2,32,62,61,15,14,33])).
% 259.56/259.62 cnf(10031,plain,
% 259.56/259.62 (~E(f15(a1,a13),a11)),
% 259.56/259.62 inference(scs_inference,[],[9991,9987,9952,9954,9879,7546,2911,2722,9878,2843,325,297,91,52,4,10,53,7,6,11,8,9,5,2,32,62,61,15,14,33,3,30,29,17,16])).
% 259.56/259.62 cnf(10040,plain,
% 259.56/259.62 (P12(a10,f15(a1,a13))),
% 259.56/259.62 inference(scs_inference,[],[34,9996,9991,9980,9987,9952,9954,9879,7546,2911,2722,9878,2843,325,297,6170,40,91,52,4,10,53,7,6,11,8,9,5,2,32,62,61,15,14,33,3,30,29,17,16,83,82,67,18,54])).
% 259.56/259.62 cnf(10073,plain,
% 259.56/259.62 (~P12(a17,f15(a1,a13))),
% 259.56/259.62 inference(scs_inference,[],[10024,10040,10031,10006,10000,9999,60,52,4,10,53,7,6,11,8,9,5,2,32])).
% 259.56/259.62 cnf(10080,plain,
% 259.56/259.62 (E(f2(f15(a1,a13),x100801),f2(a17,x100801))),
% 259.56/259.62 inference(rename_variables,[],[10006])).
% 259.56/259.62 cnf(10081,plain,
% 259.56/259.62 (P6(f2(x100811,f2(a1,a7)),f2(x100811,a8))),
% 259.56/259.62 inference(rename_variables,[],[1172])).
% 259.56/259.62 cnf(10083,plain,
% 259.56/259.62 (E(f2(f15(a1,a13),x100831),f2(a17,x100831))),
% 259.56/259.62 inference(rename_variables,[],[10006])).
% 259.56/259.62 cnf(10086,plain,
% 259.56/259.62 (E(f2(f15(a1,a13),x100861),f2(a17,x100861))),
% 259.56/259.62 inference(rename_variables,[],[10006])).
% 259.56/259.62 cnf(10087,plain,
% 259.56/259.62 (P11(f2(x100871,f15(a1,a7)),f2(x100871,a18))),
% 259.56/259.62 inference(rename_variables,[],[7893])).
% 259.56/259.62 cnf(10089,plain,
% 259.56/259.62 (E(f2(f15(a1,a13),x100891),f2(a17,x100891))),
% 259.56/259.62 inference(rename_variables,[],[10006])).
% 259.56/259.62 cnf(10094,plain,
% 259.56/259.62 (P2(a11,f15(a1,a13))),
% 259.56/259.62 inference(scs_inference,[],[10024,10023,10022,10040,10031,10006,10080,10083,10086,10089,10000,7893,10087,6263,9980,1172,10081,288,7616,9987,9999,60,52,4,10,53,7,6,11,8,9,5,2,32,62,15,14,33,30,29,17,16,59,18,54])).
% 259.56/259.62 cnf(10096,plain,
% 259.56/259.62 (P4(a1,a7,a13)),
% 259.56/259.62 inference(scs_inference,[],[34,10024,10023,10022,10040,10031,10006,10080,10083,10086,10089,10000,7893,10087,6263,9980,1172,10081,288,9996,7616,9987,100,9999,60,52,4,10,53,7,6,11,8,9,5,2,32,62,15,14,33,30,29,17,16,59,18,54,83])).
% 259.56/259.62 cnf(10119,plain,
% 259.56/259.62 (E(f15(x101191,f6(f15(a1,a13))),f15(x101191,f6(a17)))),
% 259.56/259.62 inference(scs_inference,[],[10094,10007,59,58,65,52,4,10,53,7])).
% 259.56/259.62 cnf(10128,plain,
% 259.56/259.62 (P2(f2(a1,a13),a9)),
% 259.56/259.62 inference(scs_inference,[],[34,10073,10096,10003,10094,10007,10000,9987,2640,36,59,58,65,52,4,10,53,7,6,11,8,9,5,32,33,16,89])).
% 259.56/259.62 cnf(10142,plain,
% 259.56/259.62 (~P2(a9,f2(a1,a13))),
% 259.56/259.62 inference(scs_inference,[],[10128,59,58,65])).
% 259.56/259.62 cnf(10172,plain,
% 259.56/259.62 (E(a9,f2(a1,a13))),
% 259.56/259.62 inference(scs_inference,[],[10142,1936])).
% 259.56/259.62 cnf(10175,plain,
% 259.56/259.62 (E(f2(f15(x101751,f6(f15(a1,a13))),x101752),f2(f15(x101751,f6(a17)),x101752))),
% 259.56/259.62 inference(scs_inference,[],[10119,52,4])).
% 259.56/259.62 cnf(10185,plain,
% 259.56/259.62 (~P12(f15(a1,a7),f15(a1,a13))),
% 259.56/259.62 inference(scs_inference,[],[10119,7589,9987,52,4,53,10,11,7,6,9,8,5,33])).
% 259.56/259.62 cnf(10203,plain,
% 259.56/259.62 (~P2(f2(a1,a13),f2(a1,a14))),
% 259.56/259.62 inference(scs_inference,[],[10172,7449,60,57,59,65])).
% 259.56/259.62 cnf(10209,plain,
% 259.56/259.62 (E(f2(a9,x102091),f2(f2(a1,a13),x102091))),
% 259.56/259.62 inference(scs_inference,[],[10172,10175,7449,60,57,59,65,52,53,4])).
% 259.56/259.62 cnf(10216,plain,
% 259.56/259.62 (E(f2(x102161,a9),f2(x102161,f2(a1,a13)))),
% 259.56/259.62 inference(scs_inference,[],[10172,10175,7449,60,57,59,65,52,53,4,10,11,7,9,6,8,5])).
% 259.56/259.62 cnf(10217,plain,
% 259.56/259.62 (~P12(a18,f15(a1,a13))),
% 259.56/259.62 inference(scs_inference,[],[10185,10172,10175,7526,7449,60,57,59,65,52,53,4,10,11,7,9,6,8,5,32])).
% 259.56/259.62 cnf(10218,plain,
% 259.56/259.62 (~P2(a9,a9)),
% 259.56/259.62 inference(scs_inference,[],[10185,10172,10175,10142,7526,7449,60,57,59,65,52,53,4,10,11,7,9,6,8,5,32,15])).
% 259.56/259.62 cnf(10239,plain,
% 259.56/259.62 (E(f2(a9,a9),f2(f2(a1,a13),f2(a1,a13)))),
% 259.56/259.62 inference(scs_inference,[],[10217,10203,10209,10216,10128,6172,52,53,4,10,11,7,9,6,8,5,32,15,3])).
% 259.56/259.62 cnf(10259,plain,
% 259.56/259.62 (E(f15(x102591,f2(a9,a9)),f15(x102591,f2(f2(a1,a13),f2(a1,a13))))),
% 259.56/259.62 inference(scs_inference,[],[10239,52,53,4,10,11,7])).
% 259.56/259.62 cnf(10320,plain,
% 259.56/259.62 ($false),
% 259.56/259.62 inference(scs_inference,[],[10004,10259,10218,10128,10172,52,53,4,10,11,7,8,6,9,5,14,16,2]),
% 259.56/259.62 ['proof']).
% 259.56/259.62 % SZS output end Proof
% 259.56/259.62 % Total time :259.192543s
%------------------------------------------------------------------------------