%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : SWV373+1 : TPTP v8.2.0. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% Computer : n025.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Mon Jun 24 16:47:01 EDT 2024
% Result : Theorem 73.23s 73.28s
% Output : CNFRefutation 73.40s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : SWV373+1 : TPTP v8.2.0. Released v3.3.0.
% 0.07/0.12 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% 0.12/0.33 % Computer : n025.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 300
% 0.12/0.33 % DateTime : Thu Jun 20 17:37:09 EDT 2024
% 0.12/0.33 % CPUTime :
% 0.19/0.57 start to proof:theBenchmark
% 73.23/73.26 %-------------------------------------------
% 73.23/73.26 % File :CSE---1.7
% 73.23/73.26 % Problem :theBenchmark
% 73.23/73.26 % Transform :cnf
% 73.23/73.26 % Format :tptp:raw
% 73.23/73.26 % Command :java -jar mcs_scs.jar %d %s
% 73.23/73.26
% 73.23/73.26 % Result :Theorem 72.640000s
% 73.23/73.26 % Output :CNFRefutation 72.640000s
% 73.23/73.26 %-------------------------------------------
% 73.23/73.28 %------------------------------------------------------------------------------
% 73.23/73.28 % File : SWV373+1 : TPTP v8.2.0. Released v3.3.0.
% 73.23/73.28 % Domain : Software Verification
% 73.23/73.28 % Problem : Priority queue checker: lemma_not_contains_min_not_ok
% 73.23/73.28 % Version : [dNP05] axioms.
% 73.23/73.28 % English :
% 73.23/73.28
% 73.23/73.28 % Refs : [Pis06] Piskac (2006), Email to Geoff Sutcliffe
% 73.23/73.28 % : [dNP05] de Nivelle & Piskac (2005), Verification of an Off-Lin
% 73.23/73.28 % Source : [Pis06]
% 73.23/73.28 % Names : cpq_l009 [Pis06]
% 73.23/73.28
% 73.23/73.28 % Status : Theorem
% 73.23/73.28 % Rating : 0.17 v8.1.0, 0.19 v7.5.0, 0.22 v7.4.0, 0.10 v7.3.0, 0.14 v7.2.0, 0.10 v7.1.0, 0.13 v7.0.0, 0.10 v6.4.0, 0.15 v6.3.0, 0.17 v6.2.0, 0.24 v6.1.0, 0.27 v6.0.0, 0.17 v5.5.0, 0.19 v5.4.0, 0.25 v5.3.0, 0.37 v5.2.0, 0.30 v5.1.0, 0.29 v5.0.0, 0.25 v4.1.0, 0.22 v4.0.0, 0.25 v3.7.0, 0.20 v3.5.0, 0.21 v3.4.0, 0.26 v3.3.0
% 73.23/73.28 % Syntax : Number of formulae : 43 ( 16 unt; 0 def)
% 73.23/73.28 % Number of atoms : 88 ( 30 equ)
% 73.23/73.28 % Maximal formula atoms : 4 ( 2 avg)
% 73.23/73.28 % Number of connectives : 61 ( 16 ~; 3 |; 14 &)
% 73.23/73.28 % ( 7 <=>; 21 =>; 0 <=; 0 <~>)
% 73.23/73.28 % Maximal formula depth : 9 ( 5 avg)
% 73.23/73.28 % Maximal term depth : 4 ( 1 avg)
% 73.23/73.28 % Number of predicates : 11 ( 9 usr; 1 prp; 0-3 aty)
% 73.23/73.28 % Number of functors : 18 ( 18 usr; 3 con; 0-3 aty)
% 73.23/73.28 % Number of variables : 123 ( 123 !; 0 ?)
% 73.23/73.28 % SPC : FOF_THM_RFO_SEQ
% 73.23/73.28
% 73.23/73.28 % Comments :
% 73.23/73.28 %------------------------------------------------------------------------------
% 73.23/73.28 %----Include the axioms about priority queues and checked priority queues
% 73.23/73.28 include('Axioms/SWV007+0.ax').
% 73.23/73.28 include('Axioms/SWV007+2.ax').
% 73.23/73.28 include('Axioms/SWV007+3.ax').
% 73.23/73.28 %------------------------------------------------------------------------------
% 73.23/73.28 %----lemma_ok_find_min (cpq_l010.p)
% 73.23/73.28 fof(l9_l10,lemma,
% 73.23/73.28 ! [U,V,W] :
% 73.23/73.28 ( ok(findmin_cpq_eff(triple(U,V,W)))
% 73.23/73.28 => ( V != create_slb
% 73.23/73.28 & contains_slb(V,findmin_pqp_res(U))
% 73.23/73.28 & less_than(lookup_slb(V,findmin_pqp_res(U)),findmin_pqp_res(U)) ) ) ).
% 73.23/73.28
% 73.23/73.28 %----lemma_not_contains_min_not_ok (conjecture)
% 73.23/73.28 fof(l9_co,conjecture,
% 73.23/73.28 ! [U,V,W] :
% 73.23/73.28 ( ~ contains_cpq(triple(U,V,W),findmin_cpq_res(triple(U,V,W)))
% 73.23/73.28 => ~ ok(findmin_cpq_eff(triple(U,V,W))) ) ).
% 73.23/73.28
% 73.23/73.28 %------------------------------------------------------------------------------
% 73.23/73.28 %-------------------------------------------
% 73.23/73.28 % Proof found
% 73.23/73.28 % SZS status Theorem for theBenchmark
% 73.23/73.28 % SZS output start Proof
% 73.27/73.29 %ClaNum:96(EqnAxiom:43)
% 73.27/73.29 %VarNum:314(SingletonVarNum:156)
% 73.27/73.29 %MaxLitNum:4
% 73.27/73.29 %MaxfuncDepth:3
% 73.27/73.29 %SharedTerms:12
% 73.27/73.29 %goalClause: 54 60
% 73.27/73.29 %singleGoalClaCount:2
% 73.27/73.29 [56]~P2(a1)
% 73.27/73.29 [54]P7(f8(f19(a9,a10,a11)))
% 73.27/73.29 [60]~P5(f19(a9,a10,a11),f7(f19(a9,a10,a11)))
% 73.27/73.29 [45]P1(a2,x451)
% 73.27/73.29 [46]P1(x461,x461)
% 73.27/73.29 [47]P6(x471,x471)
% 73.27/73.30 [57]~P4(a1,x571)
% 73.27/73.30 [44]E(f4(a1,x441),a1)
% 73.27/73.30 [58]~P8(a1,x581,x582)
% 73.27/73.30 [52]P3(f19(x521,a1,x522))
% 73.27/73.30 [59]~P7(f19(x591,x592,a3))
% 73.27/73.30 [51]E(f7(f19(x511,a1,x512)),a2)
% 73.27/73.30 [53]E(f8(f19(x531,a1,x532)),f19(x531,a1,a3))
% 73.27/73.30 [48]P2(f6(x481,f5(x482,x483)))
% 73.27/73.30 [49]E(f16(f6(x491,f5(x492,x493)),x492),x491)
% 73.27/73.30 [50]E(f15(f6(x501,f5(x502,x503)),x502),x503)
% 73.27/73.30 [55]E(f19(f12(x551,x552),f6(x553,f5(x552,a2)),x554),f13(f19(x551,x553,x554),x552))
% 73.27/73.30 [61]P1(x612,x611)+P1(x611,x612)
% 73.27/73.30 [62]~P9(x621,x622)+P1(x621,x622)
% 73.27/73.30 [64]~P9(x642,x641)+~P1(x641,x642)
% 73.27/73.30 [63]~P6(x631,x632)+P6(x631,f8(x632))
% 73.27/73.30 [69]~P6(x691,x692)+P6(x691,f17(f8(x692),f7(x692)))
% 73.27/73.30 [67]~P6(x671,x672)+P6(x671,f13(x672,x673))
% 73.27/73.30 [68]~P6(x681,x682)+P6(x681,f17(x682,x683))
% 73.27/73.30 [71]E(x711,a3)+P7(f19(x712,x713,x711))
% 73.27/73.30 [73]E(x731,a1)+E(f7(f19(x732,x731,x733)),f14(x732))
% 73.27/73.30 [91]~E(x911,a1)+~P7(f8(f19(x912,x911,x913)))
% 73.27/73.30 [92]P4(x921,f14(x922))+~P7(f8(f19(x922,x921,x923)))
% 73.27/73.30 [93]P1(f15(x931,f14(x932)),f14(x932))+~P7(f8(f19(x932,x931,x933)))
% 73.27/73.30 [76]~P4(x762,x764)+P5(f19(x761,x762,x763),x764)
% 73.27/73.30 [82]P4(x821,x822)+~P5(f19(x823,x821,x824),x822)
% 73.27/73.30 [70]~E(x702,x704)+P4(f6(x701,f5(x702,x703)),x704)
% 73.27/73.30 [72]~P4(x721,x724)+P4(f6(x721,f5(x722,x723)),x724)
% 73.27/73.30 [81]P4(x812,x814)+E(f17(f19(x811,x812,x813),x814),f19(x811,x812,a3))
% 73.27/73.30 [78]~P1(x782,x784)+E(f6(f4(x781,x782),f5(x783,x784)),f4(f6(x781,f5(x783,x784)),x782))
% 73.27/73.30 [79]~P9(x793,x794)+E(f4(f6(x791,f5(x792,x793)),x794),f6(f4(x791,x794),f5(x792,x794)))
% 73.27/73.30 [83]~P8(x831,x834,x835)+P8(f6(x831,f5(x832,x833)),x834,x835)
% 73.27/73.30 [94]~P9(x941,x942)+~P3(f19(x943,f6(x944,f5(x941,x942)),x945))
% 73.27/73.30 [65]P9(x652,x651)+~P1(x652,x651)+P1(x651,x652)
% 73.27/73.30 [66]~P1(x661,x663)+P1(x661,x662)+~P1(x663,x662)
% 73.27/73.30 [84]P4(x841,f14(x842))+E(x841,a1)+E(f8(f19(x842,x841,x843)),f19(x842,f4(x841,f14(x842)),a3))
% 73.27/73.30 [77]E(x771,x772)+P4(x773,x772)+~P4(f6(x773,f5(x771,x774)),x772)
% 73.27/73.30 [87]~P4(x872,x874)+~P9(x874,f15(x872,x874))+E(f17(f19(x871,x872,x873),x874),f19(f18(x871,x874),f16(x872,x874),a3))
% 73.27/73.30 [88]~P4(x883,x882)+~P1(f15(x883,x882),x882)+E(f19(f18(x881,x882),f16(x883,x882),x884),f17(f19(x881,x883,x884),x882))
% 73.27/73.30 [74]~P4(x743,x742)+E(x741,x742)+E(f15(f6(x743,f5(x741,x744)),x742),f15(x743,x742))
% 73.27/73.30 [80]~P4(x803,x802)+E(x801,x802)+E(f16(f6(x803,f5(x801,x804)),x802),f6(f16(x803,x802),f5(x801,x804)))
% 73.27/73.30 [75]~E(x753,x755)+~E(x752,x754)+P8(f6(x751,f5(x752,x753)),x754,x755)
% 73.27/73.30 [85]E(x851,x852)+P8(x853,x854,x852)+~P8(f6(x853,f5(x855,x851)),x854,x852)
% 73.27/73.30 [86]E(x861,x862)+P8(x863,x862,x864)+~P8(f6(x863,f5(x861,x865)),x862,x864)
% 73.27/73.30 [95]~P1(x954,x953)+~P3(f19(x951,x952,x955))+P3(f19(x951,f6(x952,f5(x953,x954)),x955))
% 73.27/73.30 [96]~P1(x964,x965)+P3(f19(x961,x962,x963))+~P3(f19(x961,f6(x962,f5(x965,x964)),x963))
% 73.27/73.30 [89]~P4(x891,f14(x892))+E(x891,a1)+~P9(f14(x892),f15(x891,f14(x892)))+E(f8(f19(x892,x891,x893)),f19(x892,f4(x891,f14(x892)),a3))
% 73.27/73.30 [90]~P4(x901,f14(x902))+E(x901,a1)+~P1(f15(x901,f14(x902)),f14(x902))+E(f19(x902,f4(x901,f14(x902)),x903),f8(f19(x902,x901,x903)))
% 73.27/73.30 %EqnAxiom
% 73.27/73.30 [1]E(x11,x11)
% 73.27/73.30 [2]E(x22,x21)+~E(x21,x22)
% 73.27/73.30 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 73.27/73.30 [4]~E(x41,x42)+E(f4(x41,x43),f4(x42,x43))
% 73.27/73.30 [5]~E(x51,x52)+E(f4(x53,x51),f4(x53,x52))
% 73.27/73.30 [6]~E(x61,x62)+E(f5(x61,x63),f5(x62,x63))
% 73.27/73.30 [7]~E(x71,x72)+E(f5(x73,x71),f5(x73,x72))
% 73.27/73.30 [8]~E(x81,x82)+E(f6(x81,x83),f6(x82,x83))
% 73.27/73.30 [9]~E(x91,x92)+E(f6(x93,x91),f6(x93,x92))
% 73.27/73.30 [10]~E(x101,x102)+E(f19(x101,x103,x104),f19(x102,x103,x104))
% 73.27/73.30 [11]~E(x111,x112)+E(f19(x113,x111,x114),f19(x113,x112,x114))
% 73.27/73.30 [12]~E(x121,x122)+E(f19(x123,x124,x121),f19(x123,x124,x122))
% 73.27/73.30 [13]~E(x131,x132)+E(f16(x131,x133),f16(x132,x133))
% 73.27/73.30 [14]~E(x141,x142)+E(f16(x143,x141),f16(x143,x142))
% 73.27/73.30 [15]~E(x151,x152)+E(f15(x151,x153),f15(x152,x153))
% 73.27/73.30 [16]~E(x161,x162)+E(f15(x163,x161),f15(x163,x162))
% 73.27/73.30 [17]~E(x171,x172)+E(f14(x171),f14(x172))
% 73.27/73.30 [18]~E(x181,x182)+E(f17(x181,x183),f17(x182,x183))
% 73.27/73.30 [19]~E(x191,x192)+E(f17(x193,x191),f17(x193,x192))
% 73.27/73.30 [20]~E(x201,x202)+E(f8(x201),f8(x202))
% 73.27/73.30 [21]~E(x211,x212)+E(f18(x211,x213),f18(x212,x213))
% 73.27/73.30 [22]~E(x221,x222)+E(f18(x223,x221),f18(x223,x222))
% 73.27/73.30 [23]~E(x231,x232)+E(f7(x231),f7(x232))
% 73.27/73.30 [24]~E(x241,x242)+E(f13(x241,x243),f13(x242,x243))
% 73.27/73.30 [25]~E(x251,x252)+E(f13(x253,x251),f13(x253,x252))
% 73.27/73.30 [26]~E(x261,x262)+E(f12(x261,x263),f12(x262,x263))
% 73.27/73.30 [27]~E(x271,x272)+E(f12(x273,x271),f12(x273,x272))
% 73.27/73.30 [28]P1(x282,x283)+~E(x281,x282)+~P1(x281,x283)
% 73.27/73.30 [29]P1(x293,x292)+~E(x291,x292)+~P1(x293,x291)
% 73.27/73.30 [30]~P3(x301)+P3(x302)+~E(x301,x302)
% 73.27/73.30 [31]P6(x312,x313)+~E(x311,x312)+~P6(x311,x313)
% 73.27/73.30 [32]P6(x323,x322)+~E(x321,x322)+~P6(x323,x321)
% 73.27/73.30 [33]~P2(x331)+P2(x332)+~E(x331,x332)
% 73.27/73.30 [34]P4(x342,x343)+~E(x341,x342)+~P4(x341,x343)
% 73.27/73.30 [35]P4(x353,x352)+~E(x351,x352)+~P4(x353,x351)
% 73.27/73.30 [36]~P7(x361)+P7(x362)+~E(x361,x362)
% 73.27/73.30 [37]P9(x372,x373)+~E(x371,x372)+~P9(x371,x373)
% 73.27/73.30 [38]P9(x383,x382)+~E(x381,x382)+~P9(x383,x381)
% 73.27/73.30 [39]P5(x392,x393)+~E(x391,x392)+~P5(x391,x393)
% 73.27/73.30 [40]P5(x403,x402)+~E(x401,x402)+~P5(x403,x401)
% 73.27/73.30 [41]P8(x412,x413,x414)+~E(x411,x412)+~P8(x411,x413,x414)
% 73.27/73.30 [42]P8(x423,x422,x424)+~E(x421,x422)+~P8(x423,x421,x424)
% 73.27/73.30 [43]P8(x433,x434,x432)+~E(x431,x432)+~P8(x433,x434,x431)
% 73.27/73.30
% 73.27/73.30 %-------------------------------------------
% 73.27/73.31 cnf(97,plain,
% 73.27/73.31 (P4(f6(x972,f5(x971,x973)),x971)),
% 73.27/73.31 inference(equality_inference,[],[70])).
% 73.27/73.31 cnf(98,plain,
% 73.27/73.31 (~P7(f8(f19(x981,a1,x982)))),
% 73.27/73.31 inference(equality_inference,[],[91])).
% 73.27/73.31 cnf(99,plain,
% 73.27/73.31 (~E(a10,a1)),
% 73.27/73.31 inference(scs_inference,[],[54,91])).
% 73.27/73.31 cnf(101,plain,
% 73.27/73.31 (~P4(a10,f7(f19(a9,a10,a11)))),
% 73.27/73.31 inference(scs_inference,[],[54,60,91,76])).
% 73.27/73.31 cnf(103,plain,
% 73.27/73.31 (P4(a10,f14(a9))),
% 73.27/73.31 inference(scs_inference,[],[54,60,91,76,92])).
% 73.27/73.31 cnf(105,plain,
% 73.27/73.31 (P1(f15(a10,f14(a9)),f14(a9))),
% 73.27/73.31 inference(scs_inference,[],[54,60,91,76,92,93])).
% 73.27/73.31 cnf(109,plain,
% 73.27/73.32 (E(a1,f4(a1,x1091))),
% 73.27/73.32 inference(scs_inference,[],[54,60,44,46,91,76,92,93,64,2])).
% 73.27/73.32 cnf(110,plain,
% 73.27/73.32 (~P7(f16(f6(f8(f19(x1101,a1,x1102)),f5(x1103,x1104)),x1103))),
% 73.27/73.32 inference(scs_inference,[],[54,60,98,44,49,46,91,76,92,93,64,2,36])).
% 73.27/73.32 cnf(112,plain,
% 73.27/73.32 (~E(a10,f4(a1,x1121))),
% 73.27/73.32 inference(scs_inference,[],[54,60,98,44,49,46,91,76,92,93,64,2,36,3])).
% 73.27/73.32 cnf(113,plain,
% 73.27/73.32 (P1(a1,f4(a1,x1131))),
% 73.27/73.32 inference(scs_inference,[],[54,60,98,44,49,46,91,76,92,93,64,2,36,3,28])).
% 73.27/73.32 cnf(114,plain,
% 73.27/73.32 (P1(x1141,x1141)),
% 73.27/73.32 inference(rename_variables,[],[46])).
% 73.27/73.32 cnf(115,plain,
% 73.27/73.32 (P1(f4(a1,x1151),a1)),
% 73.27/73.32 inference(scs_inference,[],[54,60,98,44,49,46,114,91,76,92,93,64,2,36,3,28,29])).
% 73.27/73.32 cnf(117,plain,
% 73.27/73.32 (~E(f6(x1171,f5(x1172,x1173)),a1)),
% 73.27/73.32 inference(scs_inference,[],[54,60,98,44,97,57,49,46,114,91,76,92,93,64,2,36,3,28,29,34])).
% 73.27/73.32 cnf(118,plain,
% 73.27/73.32 (P4(f6(x1181,f5(x1182,x1183)),x1182)),
% 73.27/73.32 inference(rename_variables,[],[97])).
% 73.27/73.32 cnf(119,plain,
% 73.27/73.32 (P4(f6(x1191,f5(f4(a1,x1192),x1193)),a1)),
% 73.27/73.32 inference(scs_inference,[],[54,60,98,44,97,118,57,49,46,114,91,76,92,93,64,2,36,3,28,29,34,35])).
% 73.27/73.32 cnf(121,plain,
% 73.27/73.32 (P6(a1,f4(a1,x1211))),
% 73.27/73.32 inference(scs_inference,[],[54,60,98,44,97,118,57,49,46,114,47,91,76,92,93,64,2,36,3,28,29,34,35,31])).
% 73.27/73.32 cnf(122,plain,
% 73.27/73.32 (P6(x1221,x1221)),
% 73.27/73.32 inference(rename_variables,[],[47])).
% 73.27/73.32 cnf(123,plain,
% 73.27/73.32 (P6(f4(a1,x1231),a1)),
% 73.27/73.32 inference(scs_inference,[],[54,60,98,44,97,118,57,49,46,114,47,122,91,76,92,93,64,2,36,3,28,29,34,35,31,32])).
% 73.27/73.32 cnf(125,plain,
% 73.27/73.32 (~P2(f4(a1,x1251))),
% 73.27/73.32 inference(scs_inference,[],[54,60,98,44,97,118,57,49,46,114,47,122,56,91,76,92,93,64,2,36,3,28,29,34,35,31,32,33])).
% 73.27/73.32 cnf(129,plain,
% 73.27/73.32 (~P9(f14(a9),f15(a10,f14(a9)))),
% 73.27/73.32 inference(scs_inference,[],[105,64])).
% 73.27/73.32 cnf(131,plain,
% 73.27/73.32 (E(f19(x1311,a1,a3),f8(f19(x1311,a1,x1312)))),
% 73.27/73.32 inference(scs_inference,[],[105,53,64,2])).
% 73.27/73.32 cnf(132,plain,
% 73.27/73.32 (P1(f4(a1,x1321),f4(a1,x1322))),
% 73.27/73.32 inference(scs_inference,[],[105,113,115,53,64,2,66])).
% 73.27/73.32 cnf(134,plain,
% 73.27/73.32 (P3(f8(f19(x1341,a1,x1342)))),
% 73.27/73.32 inference(scs_inference,[],[105,113,115,53,52,64,2,66,30])).
% 73.27/73.32 cnf(136,plain,
% 73.27/73.32 (P6(f4(a1,x1361),f4(a1,x1362))),
% 73.27/73.32 inference(scs_inference,[],[105,109,113,115,53,123,52,64,2,66,30,32])).
% 73.27/73.32 cnf(139,plain,
% 73.27/73.32 (~E(a10,f15(f6(x1391,f5(x1392,a1)),x1392))),
% 73.27/73.32 inference(scs_inference,[],[99,105,109,113,115,53,50,49,125,123,52,64,2,66,30,32,33,3])).
% 73.27/73.32 cnf(141,plain,
% 73.27/73.32 (~E(f14(a9),f7(f19(a9,a10,a11)))),
% 73.27/73.32 inference(scs_inference,[],[99,105,101,103,109,113,115,53,50,49,125,123,52,64,2,66,30,32,33,3,35])).
% 73.27/73.32 cnf(146,plain,
% 73.27/73.32 (P1(f15(a10,f14(a9)),x1461)+~E(f14(a9),x1461)),
% 73.27/73.32 inference(scs_inference,[],[99,105,101,103,44,109,113,115,53,50,49,125,123,52,64,2,66,30,32,33,3,35,65,28,36,29])).
% 73.27/73.32 cnf(152,plain,
% 73.27/73.32 (~P7(f13(f19(x1521,x1522,a3),x1523))),
% 73.27/73.32 inference(scs_inference,[],[113,59,55,64,2,36])).
% 73.27/73.32 cnf(154,plain,
% 73.27/73.32 (P4(f6(x1541,f5(f4(a1,x1542),x1543)),f4(a1,x1544))),
% 73.27/73.32 inference(scs_inference,[],[119,113,59,55,109,64,2,36,35])).
% 73.27/73.32 cnf(155,plain,
% 73.27/73.32 (E(f8(f19(x1551,a1,x1552)),f8(f19(x1551,a1,x1553)))),
% 73.27/73.32 inference(scs_inference,[],[119,113,53,131,59,55,109,64,2,36,35,3])).
% 73.27/73.32 cnf(157,plain,
% 73.27/73.32 (E(f4(a1,x1571),f4(a1,x1572))),
% 73.27/73.32 inference(scs_inference,[],[119,113,53,131,59,55,57,109,64,2,36,35,3,77])).
% 73.27/73.32 cnf(168,plain,
% 73.27/73.32 (E(a2,f7(f19(x1681,a1,x1682)))),
% 73.27/73.32 inference(scs_inference,[],[115,51,64,2])).
% 73.27/73.32 cnf(169,plain,
% 73.27/73.32 (P1(f7(f19(x1691,a1,x1692)),x1693)),
% 73.27/73.32 inference(scs_inference,[],[115,51,45,64,2,28])).
% 73.27/73.32 cnf(170,plain,
% 73.27/73.32 (~E(a10,f16(f6(a1,f5(x1701,x1702)),x1701))),
% 73.27/73.32 inference(scs_inference,[],[99,115,51,49,45,64,2,28,3])).
% 73.27/73.32 cnf(178,plain,
% 73.27/73.32 (E(x1781,f15(f6(x1782,f5(x1783,x1781)),x1783))),
% 73.27/73.32 inference(scs_inference,[],[132,50,64,2])).
% 73.27/73.32 cnf(179,plain,
% 73.27/73.32 (E(f15(f6(x1791,f5(x1792,a2)),x1792),f7(f19(x1793,a1,x1794)))),
% 73.27/73.32 inference(scs_inference,[],[132,168,50,64,2,3])).
% 73.27/73.32 cnf(188,plain,
% 73.27/73.32 (P1(f15(f6(x1881,f5(x1882,a2)),x1882),x1883)),
% 73.27/73.32 inference(scs_inference,[],[169,178,179,45,64,2,28])).
% 73.27/73.32 cnf(196,plain,
% 73.27/73.32 (E(x1961,f16(f6(x1961,f5(x1962,x1963)),x1962))),
% 73.27/73.32 inference(scs_inference,[],[188,49,64,2])).
% 73.27/73.32 cnf(198,plain,
% 73.27/73.32 (E(f8(f19(x1981,a1,x1982)),f16(f6(f8(f19(x1981,a1,x1983)),f5(x1984,x1985)),x1984))),
% 73.27/73.32 inference(scs_inference,[],[155,188,49,134,64,2,30,3])).
% 73.27/73.32 cnf(205,plain,
% 73.27/73.32 (P1(f15(a10,f14(a9)),f16(f6(f14(a9),f5(x2051,x2052)),x2051))),
% 73.27/73.32 inference(scs_inference,[],[196,146])).
% 73.27/73.32 cnf(206,plain,
% 73.27/73.32 (E(x2061,f16(f6(x2061,f5(x2062,x2063)),x2062))),
% 73.27/73.32 inference(rename_variables,[],[196])).
% 73.27/73.32 cnf(209,plain,
% 73.27/73.32 (E(f16(f6(f8(f19(x2091,a1,x2092)),f5(x2093,x2094)),x2093),f8(f19(x2091,a1,x2095)))),
% 73.27/73.32 inference(scs_inference,[],[196,198,45,146,64,2])).
% 73.27/73.32 cnf(210,plain,
% 73.27/73.32 (P1(f16(f6(f15(a10,f14(a9)),f5(x2101,x2102)),x2101),f14(a9))),
% 73.27/73.32 inference(scs_inference,[],[105,196,206,198,45,146,64,2,28])).
% 73.27/73.32 cnf(211,plain,
% 73.27/73.32 (E(x2111,f16(f6(x2111,f5(x2112,x2113)),x2112))),
% 73.27/73.32 inference(rename_variables,[],[196])).
% 73.27/73.32 cnf(212,plain,
% 73.27/73.32 (P2(f16(f6(f6(x2121,f5(x2122,x2123)),f5(x2124,x2125)),x2124))),
% 73.27/73.32 inference(scs_inference,[],[105,196,206,211,198,45,48,146,64,2,28,33])).
% 73.27/73.32 cnf(219,plain,
% 73.27/73.32 (~P9(f16(f6(f14(a9),f5(x2191,x2192)),x2191),f15(a10,f14(a9)))),
% 73.27/73.32 inference(scs_inference,[],[205,64])).
% 73.27/73.32 cnf(223,plain,
% 73.27/73.32 (E(f16(f6(f8(f19(x2231,a1,x2232)),f5(x2233,x2234)),x2233),f19(x2231,a1,a3))),
% 73.27/73.32 inference(scs_inference,[],[131,198,205,64,3,2])).
% 73.27/73.32 cnf(231,plain,
% 73.27/73.32 (~P9(f14(a9),f16(f6(f15(a10,f14(a9)),f5(x2311,x2312)),x2311))),
% 73.27/73.32 inference(scs_inference,[],[210,64])).
% 73.27/73.32 cnf(235,plain,
% 73.27/73.32 (E(f16(f6(a2,f5(x2351,x2352)),x2351),f7(f19(x2353,a1,x2354)))),
% 73.27/73.32 inference(scs_inference,[],[169,210,49,196,168,64,28,3])).
% 73.27/73.32 cnf(341,plain,
% 73.27/73.32 (E(f14(a1),f14(f4(a1,x3411)))),
% 73.27/73.32 inference(scs_inference,[],[44,17,2])).
% 73.27/73.32 cnf(342,plain,
% 73.27/73.32 (E(f14(f4(a1,x3421)),f14(a1))),
% 73.27/73.32 inference(scs_inference,[],[341,2])).
% 73.27/73.32 cnf(343,plain,
% 73.27/73.32 (E(f16(f6(f14(a1),f5(x3431,x3432)),x3431),f14(f4(a1,x3433)))),
% 73.27/73.32 inference(scs_inference,[],[49,341,2,3])).
% 73.27/73.32 cnf(348,plain,
% 73.27/73.32 (E(f8(f4(f4(a1,x3481),x3482)),f8(f4(a1,x3482)))),
% 73.27/73.32 inference(scs_inference,[],[44,20,4])).
% 73.27/73.32 cnf(349,plain,
% 73.27/73.32 (E(f8(f4(a1,x3491)),f8(f4(f4(a1,x3492),x3491)))),
% 73.27/73.32 inference(scs_inference,[],[348,2])).
% 73.27/73.32 cnf(350,plain,
% 73.27/73.32 (E(f16(f6(f14(f4(a1,x3501)),f5(x3502,x3503)),x3502),f14(a1))),
% 73.27/73.32 inference(scs_inference,[],[49,348,342,2,3])).
% 73.27/73.32 cnf(355,plain,
% 73.27/73.32 (E(f7(f4(x3551,f4(a1,x3552))),f7(f4(x3551,a1)))),
% 73.27/73.32 inference(scs_inference,[],[44,23,5])).
% 73.27/73.32 cnf(356,plain,
% 73.27/73.32 (E(f7(f4(x3561,a1)),f7(f4(x3561,f4(a1,x3562))))),
% 73.27/73.32 inference(scs_inference,[],[355,2])).
% 73.27/73.32 cnf(365,plain,
% 73.27/73.32 (P8(f6(x3651,f5(a3,a3)),a3,a3)),
% 73.27/73.32 inference(scs_inference,[],[59,71,75])).
% 73.27/73.32 cnf(367,plain,
% 73.27/73.32 (P8(f6(x3671,f5(a3,a3)),f16(f6(a3,f5(x3672,x3673)),x3672),a3)),
% 73.27/73.32 inference(scs_inference,[],[196,350,365,2,42])).
% 73.27/73.32 cnf(423,plain,
% 73.27/73.32 (P6(x4231,f16(f6(x4231,f5(x4232,x4233)),x4232))),
% 73.27/73.32 inference(scs_inference,[],[49,47,31])).
% 73.27/73.32 cnf(424,plain,
% 73.27/73.32 (P6(x4241,x4241)),
% 73.27/73.32 inference(rename_variables,[],[47])).
% 73.27/73.32 cnf(425,plain,
% 73.27/73.32 (P6(f16(f6(x4251,f5(x4252,x4253)),x4252),x4251)),
% 73.27/73.32 inference(scs_inference,[],[49,47,424,31,32])).
% 73.27/73.32 cnf(427,plain,
% 73.27/73.32 (P1(f16(f6(x4271,f5(x4272,x4273)),x4272),x4271)),
% 73.27/73.32 inference(scs_inference,[],[49,46,47,424,31,32,29])).
% 73.27/73.32 cnf(428,plain,
% 73.27/73.32 (P1(x4281,x4281)),
% 73.27/73.32 inference(rename_variables,[],[46])).
% 73.27/73.32 cnf(429,plain,
% 73.27/73.32 (P1(x4291,f16(f6(x4291,f5(x4292,x4293)),x4292))),
% 73.27/73.32 inference(scs_inference,[],[49,46,428,47,424,31,32,29,28])).
% 73.27/73.32 cnf(431,plain,
% 73.27/73.32 (E(f16(f6(f19(x4311,a1,a3),f5(x4312,x4313)),x4312),f8(f19(x4311,a1,x4314)))),
% 73.27/73.32 inference(scs_inference,[],[49,131,46,428,47,424,31,32,29,28,3])).
% 73.27/73.32 cnf(433,plain,
% 73.27/73.32 (~P7(f16(f6(f19(x4331,a1,a3),f5(x4332,x4333)),x4332))),
% 73.27/73.32 inference(scs_inference,[],[49,98,131,46,428,47,424,31,32,29,28,3,36])).
% 73.27/73.32 cnf(434,plain,
% 73.27/73.32 (E(f8(f19(x4341,a1,x4342)),f16(f6(f19(x4341,a1,a3),f5(x4343,x4344)),x4343))),
% 73.27/73.32 inference(scs_inference,[],[49,98,131,46,428,47,424,31,32,29,28,3,36,2])).
% 73.27/73.32 cnf(454,plain,
% 73.27/73.32 (P6(f7(f19(x4541,a1,x4542)),a2)),
% 73.27/73.32 inference(scs_inference,[],[235,425,31])).
% 73.27/73.32 cnf(475,plain,
% 73.27/73.32 (P6(x4751,f15(f6(x4752,f5(x4753,x4751)),x4753))),
% 73.27/73.32 inference(scs_inference,[],[50,47,31])).
% 73.27/73.32 cnf(476,plain,
% 73.27/73.32 (P6(x4761,x4761)),
% 73.27/73.32 inference(rename_variables,[],[47])).
% 73.27/73.32 cnf(477,plain,
% 73.27/73.32 (P6(f15(f6(x4771,f5(x4772,x4773)),x4772),x4773)),
% 73.27/73.32 inference(scs_inference,[],[50,47,476,31,32])).
% 73.27/73.32 cnf(482,plain,
% 73.27/73.32 (P6(f16(f6(f7(f19(x4821,a1,x4822)),f5(x4823,x4824)),x4823),a2)),
% 73.27/73.32 inference(scs_inference,[],[51,423,425,31,32])).
% 73.27/73.32 cnf(487,plain,
% 73.27/73.32 (P6(a1,f16(f6(f4(a1,x4871),f5(x4872,x4873)),x4872))),
% 73.27/73.32 inference(scs_inference,[],[44,423,31])).
% 73.27/73.32 cnf(489,plain,
% 73.27/73.32 (P6(f16(f6(f4(a1,x4891),f5(x4892,x4893)),x4892),a1)),
% 73.27/73.32 inference(scs_inference,[],[44,423,425,31,32])).
% 73.27/73.32 cnf(491,plain,
% 73.27/73.32 (P1(f16(f6(f4(a1,x4911),f5(x4912,x4913)),x4912),a1)),
% 73.27/73.32 inference(scs_inference,[],[44,427,423,425,31,32,29])).
% 73.27/73.32 cnf(493,plain,
% 73.27/73.32 (P1(a1,f16(f6(f4(a1,x4931),f5(x4932,x4933)),x4932))),
% 73.27/73.32 inference(scs_inference,[],[44,429,427,423,425,31,32,29,28])).
% 73.27/73.32 cnf(495,plain,
% 73.27/73.32 (E(f14(f4(a1,x4951)),f14(f4(a1,x4952)))),
% 73.27/73.32 inference(scs_inference,[],[44,342,341,429,427,423,425,31,32,29,28,3])).
% 73.27/73.32 cnf(502,plain,
% 73.27/73.32 (~P5(f19(x5021,a10,x5022),f7(f19(a9,a10,a11)))),
% 73.27/73.32 inference(scs_inference,[],[60,82,76])).
% 73.27/73.32 cnf(507,plain,
% 73.27/73.32 (P6(f16(f6(f8(f19(x5071,a1,x5072)),f5(x5073,x5074)),x5073),f19(x5071,a1,a3))),
% 73.27/73.32 inference(scs_inference,[],[53,493,423,425,64,31,32])).
% 73.27/73.32 cnf(509,plain,
% 73.27/73.32 (P1(f16(f6(f8(f19(x5091,a1,x5092)),f5(x5093,x5094)),x5093),f19(x5091,a1,a3))),
% 73.27/73.32 inference(scs_inference,[],[53,427,493,423,425,64,31,32,29])).
% 73.27/73.32 cnf(511,plain,
% 73.27/73.32 (P1(f19(x5111,a1,a3),f16(f6(f8(f19(x5111,a1,x5112)),f5(x5113,x5114)),x5113))),
% 73.27/73.32 inference(scs_inference,[],[53,429,427,493,423,425,64,31,32,29,28])).
% 73.27/73.32 cnf(518,plain,
% 73.27/73.32 (E(f5(f19(x5181,a1,a3),x5182),f5(f8(f19(x5181,a1,x5183)),x5182))),
% 73.27/73.32 inference(scs_inference,[],[53,6,2])).
% 73.27/73.32 cnf(521,plain,
% 73.27/73.32 (E(f5(f8(f19(x5211,a1,x5212)),x5213),f5(f19(x5211,a1,a3),x5213))),
% 73.27/73.32 inference(scs_inference,[],[518,509,64,2])).
% 73.27/73.32 cnf(522,plain,
% 73.27/73.32 (P6(f8(f19(x5221,a1,x5222)),f19(x5221,a1,a3))),
% 73.27/73.32 inference(scs_inference,[],[209,518,509,507,64,2,31])).
% 73.27/73.32 cnf(523,plain,
% 73.27/73.32 (P6(f16(f6(f8(f19(x5231,a1,x5232)),f5(x5233,x5234)),x5233),f19(x5231,a1,a3))),
% 73.27/73.32 inference(rename_variables,[],[507])).
% 73.27/73.32 cnf(526,plain,
% 73.27/73.32 (P1(f16(f6(f4(a1,x5261),f5(x5262,x5263)),x5262),f4(a1,x5264))),
% 73.27/73.32 inference(scs_inference,[],[109,131,209,491,518,509,507,523,64,2,31,32,29])).
% 73.27/73.32 cnf(551,plain,
% 73.27/73.32 (P6(f16(f6(f4(a1,x5511),f5(x5512,x5513)),x5512),f4(a1,x5514))),
% 73.27/73.32 inference(scs_inference,[],[109,526,487,489,64,31,32])).
% 73.27/73.32 cnf(552,plain,
% 73.27/73.32 (P1(f19(x5521,a1,a3),f8(f19(x5521,a1,x5522)))),
% 73.27/73.32 inference(scs_inference,[],[109,209,511,526,487,489,64,31,32,29])).
% 73.27/73.32 cnf(571,plain,
% 73.27/73.32 (~P9(f8(f19(x5711,a1,x5712)),f19(x5711,a1,a3))),
% 73.27/73.32 inference(scs_inference,[],[552,64])).
% 73.27/73.32 cnf(592,plain,
% 73.27/73.32 (E(f12(x5921,x5922),f12(x5921,a1))+E(f7(f19(x5923,x5922,x5924)),f14(x5923))),
% 73.27/73.32 inference(scs_inference,[],[27,73])).
% 73.27/73.32 cnf(597,plain,
% 73.27/73.32 (~P2(f15(f6(x5971,f5(x5972,a1)),x5972))),
% 73.27/73.32 inference(scs_inference,[],[56,50,33])).
% 73.27/73.32 cnf(611,plain,
% 73.27/73.32 (P4(f6(x6111,f5(a1,x6112)),f4(a1,x6113))),
% 73.27/73.32 inference(scs_inference,[],[109,97,35])).
% 73.27/73.32 cnf(615,plain,
% 73.27/73.32 (P6(f16(f6(a1,f5(x6151,x6152)),x6151),f4(a1,x6153))),
% 73.27/73.32 inference(scs_inference,[],[109,97,423,425,35,31,32])).
% 73.27/73.32 cnf(617,plain,
% 73.27/73.32 (P1(f16(f6(a1,f5(x6171,x6172)),x6171),f4(a1,x6173))),
% 73.27/73.32 inference(scs_inference,[],[109,97,427,423,425,35,31,32,29])).
% 73.27/73.32 cnf(619,plain,
% 73.27/73.32 (P1(f4(a1,x6191),f16(f6(a1,f5(x6192,x6193)),x6192))),
% 73.27/73.32 inference(scs_inference,[],[109,97,429,427,423,425,35,31,32,29,28])).
% 73.27/73.32 cnf(628,plain,
% 73.27/73.32 (P6(f15(f6(x6281,f5(x6282,a1)),x6282),f4(a1,x6283))),
% 73.27/73.32 inference(scs_inference,[],[109,619,475,477,64,31,32])).
% 73.27/73.32 cnf(640,plain,
% 73.27/73.32 (~E(a10,f16(f6(f4(a1,x6401),f5(x6402,x6403)),x6402))),
% 73.27/73.32 inference(scs_inference,[],[112,49,3])).
% 73.27/73.32 cnf(644,plain,
% 73.27/73.32 (~E(f6(x6441,f5(x6442,x6443)),f4(a1,x6444))),
% 73.27/73.32 inference(scs_inference,[],[117,44,3])).
% 73.27/73.32 cnf(646,plain,
% 73.27/73.32 (~E(f6(x6461,f5(x6462,x6463)),f15(f6(x6464,f5(x6465,a1)),x6465))),
% 73.27/73.32 inference(scs_inference,[],[117,50,3])).
% 73.27/73.32 cnf(648,plain,
% 73.27/73.32 (~E(f6(x6481,f5(x6482,x6483)),f16(f6(a1,f5(x6484,x6485)),x6484))),
% 73.27/73.32 inference(scs_inference,[],[117,49,3])).
% 73.27/73.32 cnf(652,plain,
% 73.27/73.32 (E(f17(f19(x6521,a10,x6522),f7(f19(a9,a10,a11))),f19(x6521,a10,a3))),
% 73.27/73.32 inference(scs_inference,[],[502,81,76])).
% 73.27/73.32 cnf(654,plain,
% 73.27/73.32 (~P7(f17(f19(x6541,a10,x6542),f7(f19(a9,a10,a11))))),
% 73.27/73.32 inference(scs_inference,[],[652,59,2,36])).
% 73.27/73.32 cnf(676,plain,
% 73.27/73.32 (P4(f6(x6761,f5(f19(x6762,a1,a3),x6763)),f8(f19(x6762,a1,x6764)))),
% 73.27/73.32 inference(scs_inference,[],[131,97,35])).
% 73.27/73.32 cnf(682,plain,
% 73.27/73.32 (P1(f16(f6(f19(x6821,a1,a3),f5(x6822,x6823)),x6822),f8(f19(x6821,a1,x6824)))),
% 73.27/73.32 inference(scs_inference,[],[131,97,427,423,425,35,31,32,29])).
% 73.27/73.32 cnf(684,plain,
% 73.27/73.32 (P1(f8(f19(x6841,a1,x6842)),f16(f6(f19(x6841,a1,a3),f5(x6843,x6844)),x6843))),
% 73.27/73.32 inference(scs_inference,[],[131,97,429,427,423,425,35,31,32,29,28])).
% 73.27/73.32 cnf(695,plain,
% 73.27/73.32 (~E(f14(a9),f16(f6(f7(f19(a9,a10,a11)),f5(x6951,x6952)),x6951))),
% 73.27/73.32 inference(scs_inference,[],[141,49,3])).
% 73.27/73.32 cnf(704,plain,
% 73.27/73.32 (P4(f6(x7041,f5(a2,x7042)),f7(f19(x7043,a1,x7044)))),
% 73.27/73.32 inference(scs_inference,[],[168,97,35])).
% 73.27/73.32 cnf(716,plain,
% 73.27/73.32 (P8(f6(x7161,f5(a3,a3)),f15(f6(x7162,f5(x7163,a3)),x7163),a3)),
% 73.27/73.32 inference(scs_inference,[],[178,365,42])).
% 73.27/73.32 cnf(717,plain,
% 73.27/73.32 (E(x7171,f15(f6(x7172,f5(x7173,x7171)),x7173))),
% 73.27/73.32 inference(rename_variables,[],[178])).
% 73.27/73.32 cnf(718,plain,
% 73.27/73.32 (P8(f6(x7181,f5(a3,a3)),a3,f15(f6(x7182,f5(x7183,a3)),x7183))),
% 73.27/73.32 inference(scs_inference,[],[178,717,365,42,43])).
% 73.27/73.32 cnf(719,plain,
% 73.27/73.32 (E(x7191,f15(f6(x7192,f5(x7193,x7191)),x7193))),
% 73.27/73.32 inference(rename_variables,[],[178])).
% 73.27/73.32 cnf(720,plain,
% 73.27/73.32 (P4(f6(x7201,f5(x7202,x7203)),f15(f6(x7204,f5(x7205,x7202)),x7205))),
% 73.27/73.32 inference(scs_inference,[],[178,717,719,97,365,42,43,35])).
% 73.27/73.32 cnf(727,plain,
% 73.27/73.32 (P4(f6(x7271,f5(x7272,x7273)),f16(f6(x7272,f5(x7274,x7275)),x7274))),
% 73.27/73.32 inference(scs_inference,[],[196,97,35])).
% 73.27/73.33 cnf(730,plain,
% 73.27/73.33 (P4(f6(x7301,f5(a1,x7302)),f16(f6(f4(a1,x7303),f5(x7304,x7305)),x7304))),
% 73.27/73.33 inference(scs_inference,[],[196,611,35])).
% 73.27/73.33 cnf(732,plain,
% 73.27/73.33 (E(a1,f16(f6(f4(a1,x7321),f5(x7322,x7323)),x7322))),
% 73.27/73.33 inference(scs_inference,[],[196,611,57,35,77])).
% 73.27/73.33 cnf(744,plain,
% 73.27/73.33 (E(f16(f6(f4(a1,x7441),f5(x7442,x7443)),x7442),a1)),
% 73.27/73.33 inference(scs_inference,[],[732,2])).
% 73.27/73.33 cnf(745,plain,
% 73.27/73.33 (P4(f6(x7451,f5(a2,x7452)),f16(f6(f7(f19(x7453,a1,x7454)),f5(x7455,x7456)),x7455))),
% 73.27/73.33 inference(scs_inference,[],[196,704,732,2,35])).
% 73.27/73.33 cnf(753,plain,
% 73.27/73.33 (E(f12(x7531,a10),f12(x7531,a1))),
% 73.27/73.33 inference(scs_inference,[],[141,592,2])).
% 73.27/73.33 cnf(754,plain,
% 73.27/73.33 (E(f12(x7541,a1),f12(x7541,a10))),
% 73.27/73.33 inference(scs_inference,[],[753,2])).
% 73.27/73.33 cnf(785,plain,
% 73.27/73.33 (P4(f6(x7851,f5(f14(a1),x7852)),f14(f4(a1,x7853)))),
% 73.27/73.33 inference(scs_inference,[],[341,97,35])).
% 73.27/73.33 cnf(789,plain,
% 73.27/73.33 (P6(f16(f6(f14(a1),f5(x7891,x7892)),x7891),f14(f4(a1,x7893)))),
% 73.27/73.33 inference(scs_inference,[],[341,97,423,425,35,31,32])).
% 73.27/73.33 cnf(793,plain,
% 73.27/73.33 (P1(f14(f4(a1,x7931)),f16(f6(f14(a1),f5(x7932,x7933)),x7932))),
% 73.27/73.33 inference(scs_inference,[],[341,97,427,429,423,425,35,31,32,29,28])).
% 73.27/73.33 cnf(803,plain,
% 73.27/73.33 (P1(f14(f4(a1,x8031)),f14(f4(a1,x8032)))),
% 73.27/73.33 inference(scs_inference,[],[341,343,793,789,47,64,31,32,29])).
% 73.27/73.33 cnf(805,plain,
% 73.27/73.33 (P1(f14(f4(a1,x8051)),f14(a1))),
% 73.27/73.33 inference(scs_inference,[],[341,343,793,789,46,47,64,31,32,29,28])).
% 73.27/73.33 cnf(812,plain,
% 73.27/73.33 (P6(f14(f4(a1,x8121)),f14(a1))),
% 73.27/73.33 inference(scs_inference,[],[341,803,47,64,31])).
% 73.27/73.33 cnf(814,plain,
% 73.27/73.33 (P1(f14(a1),f14(f4(a1,x8141)))),
% 73.27/73.33 inference(scs_inference,[],[341,803,46,47,64,31,29])).
% 73.27/73.33 cnf(816,plain,
% 73.27/73.33 (~P9(f14(a1),f14(f4(a1,x8161)))),
% 73.27/73.33 inference(scs_inference,[],[805,64])).
% 73.27/73.33 cnf(819,plain,
% 73.27/73.33 (~P9(f14(f4(a1,x8191)),f14(a1))),
% 73.27/73.33 inference(scs_inference,[],[814,64])).
% 73.27/73.33 cnf(899,plain,
% 73.27/73.33 (P6(f5(f8(f19(x8991,a1,x8992)),x8993),f5(f19(x8991,a1,a3),x8993))),
% 73.27/73.33 inference(scs_inference,[],[518,47,31])).
% 73.27/73.33 cnf(900,plain,
% 73.27/73.33 (P6(x9001,x9001)),
% 73.27/73.33 inference(rename_variables,[],[47])).
% 73.27/73.33 cnf(901,plain,
% 73.27/73.33 (P6(f5(f19(x9011,a1,a3),x9012),f5(f8(f19(x9011,a1,x9013)),x9012))),
% 73.27/73.33 inference(scs_inference,[],[518,47,900,31,32])).
% 73.27/73.33 cnf(903,plain,
% 73.27/73.33 (P1(f5(f8(f19(x9031,a1,x9032)),x9033),f5(f19(x9031,a1,a3),x9033))),
% 73.27/73.33 inference(scs_inference,[],[518,46,47,900,31,32,28])).
% 73.27/73.33 cnf(904,plain,
% 73.27/73.33 (P1(x9041,x9041)),
% 73.27/73.33 inference(rename_variables,[],[46])).
% 73.27/73.33 cnf(905,plain,
% 73.27/73.33 (P1(f5(f19(x9051,a1,a3),x9052),f5(f8(f19(x9051,a1,x9053)),x9052))),
% 73.27/73.33 inference(scs_inference,[],[518,46,904,47,900,31,32,28,29])).
% 73.27/73.33 cnf(925,plain,
% 73.27/73.33 (E(f4(a1,x9251),f4(f4(a1,x9252),x9251))),
% 73.27/73.33 inference(scs_inference,[],[44,2,4])).
% 73.27/73.33 cnf(926,plain,
% 73.27/73.33 (E(f4(f4(a1,x9261),x9262),f4(a1,x9262))),
% 73.27/73.33 inference(scs_inference,[],[925,2])).
% 73.27/73.33 cnf(927,plain,
% 73.27/73.33 (E(a1,f4(f4(a1,x9271),x9272))),
% 73.27/73.33 inference(scs_inference,[],[109,925,2,3])).
% 73.27/73.33 cnf(933,plain,
% 73.27/73.33 (E(f4(f4(a1,x9331),x9332),a1)),
% 73.27/73.33 inference(scs_inference,[],[927,2])).
% 73.27/73.33 cnf(934,plain,
% 73.27/73.33 (~E(f6(x9341,f5(x9342,x9343)),f4(f4(a1,x9344),x9345))),
% 73.27/73.33 inference(scs_inference,[],[926,927,644,2,3])).
% 73.27/73.33 cnf(944,plain,
% 73.27/73.33 (~E(a10,f4(f4(a1,x9441),x9442))),
% 73.27/73.33 inference(scs_inference,[],[99,933,3])).
% 73.27/73.33 cnf(956,plain,
% 73.27/73.33 (~E(f6(x9561,f5(x9562,x9563)),f16(f6(f4(a1,x9564),f5(x9565,x9566)),x9565))),
% 73.27/73.33 inference(scs_inference,[],[644,49,3])).
% 73.27/73.33 cnf(961,plain,
% 73.27/73.33 (P6(x9611,x9611)),
% 73.27/73.33 inference(rename_variables,[],[47])).
% 73.27/73.33 cnf(962,plain,
% 73.27/73.33 (P6(f17(f19(x9621,a10,x9622),f7(f19(a9,a10,a11))),f19(x9621,a10,a3))),
% 73.27/73.33 inference(scs_inference,[],[652,47,961,31,32])).
% 73.27/73.33 cnf(964,plain,
% 73.27/73.33 (P1(f19(x9641,a10,a3),f17(f19(x9641,a10,x9642),f7(f19(a9,a10,a11))))),
% 73.27/73.33 inference(scs_inference,[],[652,46,47,961,31,32,28])).
% 73.34/73.33 cnf(971,plain,
% 73.34/73.33 (~P9(f17(f19(x9711,a10,x9712),f7(f19(a9,a10,a11))),f19(x9711,a10,a3))),
% 73.34/73.33 inference(scs_inference,[],[964,64])).
% 73.34/73.33 cnf(979,plain,
% 73.34/73.33 (E(f4(x9791,a1),f4(x9791,f4(a1,x9792)))),
% 73.34/73.33 inference(scs_inference,[],[44,2,5])).
% 73.34/73.33 cnf(980,plain,
% 73.34/73.33 (E(f4(x9801,f4(a1,x9802)),f4(x9801,a1))),
% 73.34/73.33 inference(scs_inference,[],[979,2])).
% 73.34/73.33 cnf(992,plain,
% 73.34/73.33 (E(f5(a1,x9921),f5(f4(a1,x9922),x9921))),
% 73.34/73.33 inference(scs_inference,[],[44,2,6])).
% 73.34/73.33 cnf(993,plain,
% 73.34/73.33 (E(f5(f4(a1,x9931),x9932),f5(a1,x9932))),
% 73.34/73.33 inference(scs_inference,[],[992,2])).
% 73.34/73.33 cnf(1003,plain,
% 73.34/73.33 (P4(f6(x10031,f5(f12(x10032,a10),x10033)),f12(x10032,a1))),
% 73.34/73.33 inference(scs_inference,[],[753,97,35])).
% 73.34/73.33 cnf(1005,plain,
% 73.34/73.33 (P6(f12(x10051,a1),f16(f6(f12(x10051,a10),f5(x10052,x10053)),x10052))),
% 73.34/73.33 inference(scs_inference,[],[753,97,423,35,31])).
% 73.34/73.33 cnf(1007,plain,
% 73.34/73.33 (P6(f16(f6(f12(x10071,a10),f5(x10072,x10073)),x10072),f12(x10071,a1))),
% 73.34/73.33 inference(scs_inference,[],[753,97,423,425,35,31,32])).
% 73.34/73.33 cnf(1009,plain,
% 73.34/73.33 (P1(f12(x10091,a1),f16(f6(f12(x10091,a10),f5(x10092,x10093)),x10092))),
% 73.34/73.33 inference(scs_inference,[],[753,429,97,423,425,35,31,32,28])).
% 73.34/73.33 cnf(1011,plain,
% 73.34/73.33 (P1(f16(f6(f12(x10111,a10),f5(x10112,x10113)),x10112),f12(x10111,a1))),
% 73.34/73.33 inference(scs_inference,[],[753,427,429,97,423,425,35,31,32,28,29])).
% 73.34/73.33 cnf(1017,plain,
% 73.34/73.33 (P6(f12(x10171,a10),f12(x10171,a1))),
% 73.34/73.33 inference(scs_inference,[],[49,1011,1007,64,31])).
% 73.34/73.33 cnf(1019,plain,
% 73.34/73.33 (E(f16(f6(x10191,f5(x10192,x10193)),x10192),x10191)),
% 73.34/73.33 inference(rename_variables,[],[49])).
% 73.34/73.33 cnf(1020,plain,
% 73.34/73.33 (P6(f12(x10201,a1),f12(x10201,a10))),
% 73.34/73.33 inference(scs_inference,[],[49,1019,1011,1007,1005,64,31,32])).
% 73.34/73.33 cnf(1022,plain,
% 73.34/73.33 (E(f16(f6(x10221,f5(x10222,x10223)),x10222),x10221)),
% 73.34/73.33 inference(rename_variables,[],[49])).
% 73.34/73.33 cnf(1023,plain,
% 73.34/73.33 (P1(f12(x10231,a10),f12(x10231,a1))),
% 73.34/73.33 inference(scs_inference,[],[49,1019,1022,1011,1007,1005,64,31,32,28])).
% 73.34/73.33 cnf(1025,plain,
% 73.34/73.33 (E(f16(f6(x10251,f5(x10252,x10253)),x10252),x10251)),
% 73.34/73.33 inference(rename_variables,[],[49])).
% 73.34/73.33 cnf(1026,plain,
% 73.34/73.33 (P1(f12(x10261,a1),f12(x10261,a10))),
% 73.34/73.33 inference(scs_inference,[],[49,1019,1022,1025,1011,1009,1007,1005,64,31,32,28,29])).
% 73.34/73.33 cnf(1029,plain,
% 73.34/73.33 (E(f4(f12(x10291,a1),x10292),f4(f12(x10291,a10),x10292))),
% 73.34/73.33 inference(scs_inference,[],[753,2,4])).
% 73.34/73.33 cnf(1030,plain,
% 73.34/73.33 (~P9(f12(x10301,a1),f12(x10301,a10))),
% 73.34/73.33 inference(scs_inference,[],[1023,64])).
% 73.34/73.33 cnf(1032,plain,
% 73.34/73.33 (E(f4(f12(x10321,a10),x10322),f4(f12(x10321,a1),x10322))),
% 73.34/73.33 inference(scs_inference,[],[1029,1023,64,2])).
% 73.34/73.33 cnf(1040,plain,
% 73.34/73.33 (~P9(f12(x10401,a10),f12(x10401,a1))),
% 73.34/73.33 inference(scs_inference,[],[1026,64])).
% 73.34/73.33 cnf(1065,plain,
% 73.34/73.33 (P4(f6(x10651,f5(f12(x10652,a1),x10653)),f12(x10652,a10))),
% 73.34/73.33 inference(scs_inference,[],[754,97,35])).
% 73.34/73.33 cnf(1069,plain,
% 73.34/73.33 (P6(f16(f6(f12(x10691,a1),f5(x10692,x10693)),x10692),f12(x10691,a10))),
% 73.34/73.33 inference(scs_inference,[],[754,97,423,425,35,31,32])).
% 73.34/73.33 cnf(1071,plain,
% 73.34/73.33 (P1(f16(f6(f12(x10711,a1),f5(x10712,x10713)),x10712),f12(x10711,a10))),
% 73.34/73.33 inference(scs_inference,[],[754,427,97,423,425,35,31,32,29])).
% 73.34/73.33 cnf(1073,plain,
% 73.34/73.33 (P1(f12(x10731,a10),f16(f6(f12(x10731,a1),f5(x10732,x10733)),x10732))),
% 73.34/73.33 inference(scs_inference,[],[754,427,429,97,423,425,35,31,32,29,28])).
% 73.34/73.33 cnf(1097,plain,
% 73.34/73.33 (E(f5(x10971,a1),f5(x10971,f4(a1,x10972)))),
% 73.34/73.33 inference(scs_inference,[],[44,2,7])).
% 73.34/73.33 cnf(1098,plain,
% 73.34/73.33 (E(f5(x10981,f4(a1,x10982)),f5(x10981,a1))),
% 73.34/73.33 inference(scs_inference,[],[1097,2])).
% 73.34/73.33 cnf(1099,plain,
% 73.34/73.33 (E(f5(f8(f19(x10991,a1,x10992)),a1),f5(f19(x10991,a1,a3),f4(a1,x10993)))),
% 73.34/73.33 inference(scs_inference,[],[521,1097,2,3])).
% 73.34/73.33 cnf(1110,plain,
% 73.34/73.33 (E(f5(f19(x11101,a1,a3),a1),f5(f8(f19(x11101,a1,x11102)),f4(a1,x11103)))),
% 73.34/73.33 inference(scs_inference,[],[518,1099,1097,2,3])).
% 73.34/73.33 cnf(1120,plain,
% 73.34/73.33 (E(f5(f8(f19(x11201,a1,x11202)),a1),f5(f8(f19(x11201,a1,x11203)),f4(a1,x11204)))),
% 73.34/73.33 inference(scs_inference,[],[521,1110,2,3])).
% 73.34/73.33 cnf(1224,plain,
% 73.34/73.33 (P4(f6(x12241,f5(f4(a1,x12242),x12243)),f4(f4(a1,x12244),x12245))),
% 73.34/73.33 inference(scs_inference,[],[925,154,35])).
% 73.34/73.33 cnf(1228,plain,
% 73.34/73.33 (P6(f4(f4(a1,x12281),x12282),a1)),
% 73.34/73.33 inference(scs_inference,[],[925,154,123,121,35,32,31])).
% 73.34/73.33 cnf(1232,plain,
% 73.34/73.33 (P1(f4(f4(a1,x12321),x12322),a1)),
% 73.34/73.33 inference(scs_inference,[],[925,113,154,115,123,121,35,32,31,29,28])).
% 73.34/73.33 cnf(1236,plain,
% 73.34/73.33 (E(f4(a1,x12361),f4(f4(a1,x12362),x12363))),
% 73.34/73.33 inference(scs_inference,[],[925,113,154,115,57,123,121,35,32,31,29,28,64,77])).
% 73.34/73.33 cnf(1239,plain,
% 73.34/73.33 (E(f4(f4(a1,x12391),x12392),f4(a1,x12393))),
% 73.34/73.33 inference(scs_inference,[],[925,113,154,115,57,123,121,35,32,31,29,28,64,77,2])).
% 73.34/73.33 cnf(1244,plain,
% 73.34/73.33 (P4(f6(x12441,f5(a1,x12442)),f4(f4(a1,x12443),x12444))),
% 73.34/73.33 inference(scs_inference,[],[927,97,1232,64,35])).
% 73.34/73.33 cnf(1247,plain,
% 73.34/73.33 (P6(f4(f4(a1,x12471),x12472),f4(a1,x12473))),
% 73.34/73.33 inference(scs_inference,[],[927,97,1232,123,121,64,35,32,31])).
% 73.34/73.33 cnf(1300,plain,
% 73.34/73.33 (P6(f16(f6(f4(f4(a1,x13001),x13002),f5(x13003,x13004)),x13003),a1)),
% 73.34/73.33 inference(scs_inference,[],[933,425,32])).
% 73.34/73.33 cnf(1302,plain,
% 73.34/73.33 (P6(a1,f16(f6(f4(f4(a1,x13021),x13022),f5(x13023,x13024)),x13023))),
% 73.34/73.33 inference(scs_inference,[],[933,423,425,32,31])).
% 73.34/73.33 cnf(1304,plain,
% 73.34/73.33 (P1(f16(f6(f4(f4(a1,x13041),x13042),f5(x13043,x13044)),x13043),a1)),
% 73.34/73.33 inference(scs_inference,[],[933,427,423,425,32,31,29])).
% 73.34/73.33 cnf(1306,plain,
% 73.34/73.33 (P1(a1,f16(f6(f4(f4(a1,x13061),x13062),f5(x13063,x13064)),x13063))),
% 73.34/73.33 inference(scs_inference,[],[933,427,429,423,425,32,31,29,28])).
% 73.34/73.33 cnf(1315,plain,
% 73.34/73.33 (P1(f4(a1,x13151),f16(f6(f4(f4(a1,x13152),x13153),f5(x13154,x13155)),x13154))),
% 73.34/73.33 inference(scs_inference,[],[109,1304,1306,1300,1302,64,32,31,29,28])).
% 73.34/73.33 cnf(1320,plain,
% 73.34/73.33 (~E(f6(x13201,f5(x13202,x13203)),f16(f6(f4(f4(a1,x13204),x13205),f5(x13206,x13207)),x13206))),
% 73.34/73.33 inference(scs_inference,[],[934,49,3])).
% 73.34/73.33 cnf(1323,plain,
% 73.34/73.33 (~E(a10,f16(f6(f4(f4(a1,x13231),x13232),f5(x13233,x13234)),x13233))),
% 73.34/73.33 inference(scs_inference,[],[944,49,3])).
% 73.34/73.33 cnf(1329,plain,
% 73.34/73.33 (P4(f6(x13291,f5(f4(x13292,a1),x13293)),f4(x13292,f4(a1,x13294)))),
% 73.34/73.33 inference(scs_inference,[],[979,97,35])).
% 73.34/73.33 cnf(1331,plain,
% 73.34/73.33 (P6(f16(f6(f4(x13311,a1),f5(x13312,x13313)),x13312),f4(x13311,f4(a1,x13314)))),
% 73.34/73.33 inference(scs_inference,[],[979,97,425,35,32])).
% 73.34/73.33 cnf(1333,plain,
% 73.34/73.33 (P6(f4(x13331,f4(a1,x13332)),f16(f6(f4(x13331,a1),f5(x13333,x13334)),x13333))),
% 73.34/73.33 inference(scs_inference,[],[979,97,423,425,35,32,31])).
% 73.34/73.33 cnf(1335,plain,
% 73.34/73.33 (E(f4(f12(x13351,a10),a1),f4(f12(x13351,a1),f4(a1,x13352)))),
% 73.34/73.33 inference(scs_inference,[],[979,1032,97,423,425,35,32,31,3])).
% 73.34/73.33 cnf(1337,plain,
% 73.34/73.33 (E(f4(x13371,a1),f4(x13371,f4(a1,x13372)))),
% 73.34/73.33 inference(rename_variables,[],[979])).
% 73.34/73.33 cnf(1338,plain,
% 73.34/73.33 (P1(f16(f6(f4(x13381,a1),f5(x13382,x13383)),x13382),f4(x13381,f4(a1,x13384)))),
% 73.34/73.33 inference(scs_inference,[],[979,1337,1032,427,97,423,425,35,32,31,3,29])).
% 73.34/73.33 cnf(1340,plain,
% 73.34/73.33 (P1(f4(x13401,f4(a1,x13402)),f16(f6(f4(x13401,a1),f5(x13403,x13404)),x13403))),
% 73.34/73.33 inference(scs_inference,[],[979,1337,1032,427,429,97,423,425,35,32,31,3,29,28])).
% 73.34/73.33 cnf(1344,plain,
% 73.34/73.33 (E(f4(f12(x13441,a1),f4(a1,x13442)),f4(f12(x13441,a10),a1))),
% 73.34/73.33 inference(scs_inference,[],[979,1337,1032,427,429,97,423,425,35,32,31,3,29,28,64,2])).
% 73.34/73.33 cnf(1353,plain,
% 73.34/73.33 (P6(f4(x13531,a1),f4(x13531,f4(a1,x13532)))),
% 73.34/73.33 inference(scs_inference,[],[979,1340,47,64,32])).
% 73.34/73.33 cnf(1354,plain,
% 73.34/73.33 (P6(x13541,x13541)),
% 73.34/73.33 inference(rename_variables,[],[47])).
% 73.34/73.33 cnf(1355,plain,
% 73.34/73.33 (P6(f4(x13551,f4(a1,x13552)),f4(x13551,a1))),
% 73.34/73.33 inference(scs_inference,[],[979,1340,47,1354,64,32,31])).
% 73.34/73.33 cnf(1357,plain,
% 73.34/73.33 (E(f4(f12(x13571,a1),a1),f4(f12(x13571,a10),f4(a1,x13572)))),
% 73.34/73.33 inference(scs_inference,[],[979,1029,1340,47,1354,64,32,31,3])).
% 73.34/73.33 cnf(1359,plain,
% 73.34/73.33 (E(f4(x13591,a1),f4(x13591,f4(a1,x13592)))),
% 73.34/73.33 inference(rename_variables,[],[979])).
% 73.34/73.33 cnf(1360,plain,
% 73.34/73.33 (P1(f4(x13601,a1),f4(x13601,f4(a1,x13602)))),
% 73.34/73.33 inference(scs_inference,[],[979,1359,1029,1340,46,47,1354,64,32,31,3,29])).
% 73.34/73.33 cnf(1361,plain,
% 73.34/73.33 (P1(x13611,x13611)),
% 73.34/73.33 inference(rename_variables,[],[46])).
% 73.34/73.33 cnf(1362,plain,
% 73.34/73.33 (P1(f4(x13621,f4(a1,x13622)),f4(x13621,a1))),
% 73.34/73.33 inference(scs_inference,[],[979,1359,1029,1340,46,1361,47,1354,64,32,31,3,29,28])).
% 73.34/73.33 cnf(1364,plain,
% 73.34/73.33 (E(f4(f12(x13641,a10),f4(a1,x13642)),f4(f12(x13641,a1),a1))),
% 73.34/73.33 inference(scs_inference,[],[979,1359,1029,1340,46,1361,47,1354,64,32,31,3,29,28,2])).
% 73.34/73.33 cnf(1366,plain,
% 73.34/73.33 (~P9(f4(x13661,a1),f4(x13661,f4(a1,x13662)))),
% 73.34/73.33 inference(scs_inference,[],[1362,64])).
% 73.34/73.33 cnf(1368,plain,
% 73.34/73.33 (P6(f4(x13681,f4(a1,x13682)),f4(x13681,f4(a1,x13683)))),
% 73.34/73.33 inference(scs_inference,[],[979,1362,1355,64,32])).
% 73.34/73.33 cnf(1370,plain,
% 73.34/73.33 (P1(f4(x13701,f4(a1,x13702)),f4(x13701,f4(a1,x13703)))),
% 73.34/73.33 inference(scs_inference,[],[979,1362,1355,64,32,29])).
% 73.34/73.33 cnf(1377,plain,
% 73.34/73.33 (~P9(f4(x13771,f4(a1,x13772)),f4(x13771,a1))),
% 73.34/73.33 inference(scs_inference,[],[1360,64])).
% 73.34/73.33 cnf(1380,plain,
% 73.34/73.33 (~P9(f4(x13801,f4(a1,x13802)),f4(x13801,f4(a1,x13803)))),
% 73.34/73.33 inference(scs_inference,[],[1370,64])).
% 73.34/73.33 cnf(1384,plain,
% 73.34/73.33 (P6(f4(x13841,a1),f16(f6(f4(x13841,f4(a1,x13842)),f5(x13843,x13844)),x13843))),
% 73.34/73.33 inference(scs_inference,[],[980,423,31])).
% 73.34/73.33 cnf(1386,plain,
% 73.34/73.33 (P6(f16(f6(f4(x13861,f4(a1,x13862)),f5(x13863,x13864)),x13863),f4(x13861,a1))),
% 73.34/73.33 inference(scs_inference,[],[980,423,425,31,32])).
% 73.34/73.33 cnf(1388,plain,
% 73.34/73.33 (E(f4(f12(x13881,a10),f4(a1,x13882)),f4(f12(x13881,a1),f4(a1,x13883)))),
% 73.34/73.33 inference(scs_inference,[],[980,1335,423,425,31,32,3])).
% 73.34/73.33 cnf(1389,plain,
% 73.34/73.33 (E(f4(x13891,f4(a1,x13892)),f4(x13891,a1))),
% 73.34/73.33 inference(rename_variables,[],[980])).
% 73.34/73.33 cnf(1390,plain,
% 73.34/73.33 (P1(f16(f6(f4(x13901,f4(a1,x13902)),f5(x13903,x13904)),x13903),f4(x13901,a1))),
% 73.34/73.33 inference(scs_inference,[],[980,1389,427,1335,423,425,31,32,3,29])).
% 73.34/73.33 cnf(1392,plain,
% 73.34/73.33 (P1(f4(x13921,a1),f16(f6(f4(x13921,f4(a1,x13922)),f5(x13923,x13924)),x13923))),
% 73.34/73.33 inference(scs_inference,[],[980,1389,427,429,1335,423,425,31,32,3,29,28])).
% 73.34/73.33 cnf(1396,plain,
% 73.34/73.33 (E(f4(f12(x13961,a1),f4(a1,x13962)),f4(f12(x13961,a10),f4(a1,x13963)))),
% 73.34/73.33 inference(scs_inference,[],[980,1389,427,429,1335,423,425,31,32,3,29,28,64,2])).
% 73.34/73.33 cnf(1407,plain,
% 73.34/73.33 (P4(f6(x14071,f5(f5(a1,x14072),x14073)),f5(f4(a1,x14074),x14072))),
% 73.34/73.33 inference(scs_inference,[],[992,97,35])).
% 73.34/73.33 cnf(1409,plain,
% 73.34/73.33 (P6(f5(f4(a1,x14091),x14092),f16(f6(f5(a1,x14092),f5(x14093,x14094)),x14093))),
% 73.34/73.33 inference(scs_inference,[],[992,97,423,35,31])).
% 73.34/73.33 cnf(1411,plain,
% 73.34/73.33 (P6(f16(f6(f5(a1,x14111),f5(x14112,x14113)),x14112),f5(f4(a1,x14114),x14111))),
% 73.34/73.33 inference(scs_inference,[],[992,97,423,425,35,31,32])).
% 73.34/73.33 cnf(1413,plain,
% 73.34/73.33 (E(f5(a1,f4(a1,x14131)),f5(f4(a1,x14132),a1))),
% 73.34/73.33 inference(scs_inference,[],[992,1098,97,423,425,35,31,32,3])).
% 73.34/73.33 cnf(1415,plain,
% 73.34/73.33 (E(f5(a1,x14151),f5(f4(a1,x14152),x14151))),
% 73.34/73.33 inference(rename_variables,[],[992])).
% 73.34/73.33 cnf(1416,plain,
% 73.34/73.33 (P1(f16(f6(f5(a1,x14161),f5(x14162,x14163)),x14162),f5(f4(a1,x14164),x14161))),
% 73.34/73.33 inference(scs_inference,[],[992,1415,1098,427,97,423,425,35,31,32,3,29])).
% 73.34/73.33 cnf(1418,plain,
% 73.34/73.33 (P1(f5(f4(a1,x14181),x14182),f16(f6(f5(a1,x14182),f5(x14183,x14184)),x14183))),
% 73.34/73.33 inference(scs_inference,[],[992,1415,1098,427,429,97,423,425,35,31,32,3,29,28])).
% 73.34/73.33 cnf(1422,plain,
% 73.34/73.33 (E(f5(f4(a1,x14221),a1),f5(a1,f4(a1,x14222)))),
% 73.34/73.33 inference(scs_inference,[],[992,1415,1098,427,429,97,423,425,35,31,32,3,29,28,64,2])).
% 73.34/73.33 cnf(1430,plain,
% 73.34/73.33 (P6(f5(f4(a1,x14301),x14302),f5(a1,x14302))),
% 73.34/73.33 inference(scs_inference,[],[992,1418,47,64,31])).
% 73.34/73.33 cnf(1431,plain,
% 73.34/73.33 (P6(x14311,x14311)),
% 73.34/73.33 inference(rename_variables,[],[47])).
% 73.34/73.33 cnf(1432,plain,
% 73.34/73.33 (P6(f5(a1,x14321),f5(f4(a1,x14322),x14321))),
% 73.34/73.33 inference(scs_inference,[],[992,1418,47,1431,64,31,32])).
% 73.34/73.33 cnf(1434,plain,
% 73.34/73.33 (E(f5(a1,a1),f5(f4(a1,x14341),f4(a1,x14342)))),
% 73.34/73.33 inference(scs_inference,[],[992,1097,1418,47,1431,64,31,32,3])).
% 73.34/73.33 cnf(1436,plain,
% 73.34/73.33 (E(f5(a1,x14361),f5(f4(a1,x14362),x14361))),
% 73.34/73.33 inference(rename_variables,[],[992])).
% 73.34/73.33 cnf(1437,plain,
% 73.34/73.33 (P1(f5(a1,x14371),f5(f4(a1,x14372),x14371))),
% 73.34/73.33 inference(scs_inference,[],[992,1436,1097,1418,46,47,1431,64,31,32,3,29])).
% 73.34/73.33 cnf(1438,plain,
% 73.34/73.33 (P1(x14381,x14381)),
% 73.34/73.33 inference(rename_variables,[],[46])).
% 73.34/73.33 cnf(1439,plain,
% 73.34/73.33 (P1(f5(f4(a1,x14391),x14392),f5(a1,x14392))),
% 73.34/73.33 inference(scs_inference,[],[992,1436,1097,1418,46,1438,47,1431,64,31,32,3,29,28])).
% 73.34/73.33 cnf(1441,plain,
% 73.34/73.33 (E(f5(f4(a1,x14411),f4(a1,x14412)),f5(a1,a1))),
% 73.34/73.33 inference(scs_inference,[],[992,1436,1097,1418,46,1438,47,1431,64,31,32,3,29,28,2])).
% 73.34/73.33 cnf(1447,plain,
% 73.34/73.33 (~P9(f5(a1,x14471),f5(f4(a1,x14472),x14471))),
% 73.34/73.33 inference(scs_inference,[],[1439,64])).
% 73.34/73.33 cnf(1449,plain,
% 73.34/73.33 (P6(f5(f4(a1,x14491),x14492),f5(f4(a1,x14493),x14492))),
% 73.34/73.33 inference(scs_inference,[],[992,1439,1432,64,31])).
% 73.34/73.33 cnf(1451,plain,
% 73.34/73.33 (P1(f5(f4(a1,x14511),x14512),f5(f4(a1,x14513),x14512))),
% 73.34/73.33 inference(scs_inference,[],[992,1439,1432,64,31,29])).
% 73.34/73.33 cnf(1456,plain,
% 73.34/73.33 (~P9(f5(f4(a1,x14561),x14562),f5(a1,x14562))),
% 73.34/73.33 inference(scs_inference,[],[1437,64])).
% 73.34/73.33 cnf(1458,plain,
% 73.34/73.33 (~P9(f5(f4(a1,x14581),x14582),f5(f4(a1,x14583),x14582))),
% 73.34/73.33 inference(scs_inference,[],[1451,64])).
% 73.34/73.33 cnf(1461,plain,
% 73.34/73.33 (P6(f16(f6(f5(f4(a1,x14611),x14612),f5(x14613,x14614)),x14613),f5(a1,x14612))),
% 73.34/73.33 inference(scs_inference,[],[993,425,32])).
% 73.34/73.33 cnf(1463,plain,
% 73.34/73.33 (P6(f5(a1,x14631),f16(f6(f5(f4(a1,x14632),x14631),f5(x14633,x14634)),x14633))),
% 73.34/73.33 inference(scs_inference,[],[993,423,425,32,31])).
% 73.34/73.33 cnf(1465,plain,
% 73.34/73.33 (E(f5(f4(a1,x14651),x14652),f5(f4(a1,x14653),x14652))),
% 73.34/73.33 inference(scs_inference,[],[993,992,423,425,32,31,3])).
% 73.34/73.33 cnf(1467,plain,
% 73.34/73.33 (P1(f16(f6(f5(f4(a1,x14671),x14672),f5(x14673,x14674)),x14673),f5(a1,x14672))),
% 73.34/73.33 inference(scs_inference,[],[993,992,427,423,425,32,31,3,29])).
% 73.34/73.33 cnf(1469,plain,
% 73.34/73.33 (P1(f5(a1,x14691),f16(f6(f5(f4(a1,x14692),x14691),f5(x14693,x14694)),x14693))),
% 73.34/73.33 inference(scs_inference,[],[993,992,427,429,423,425,32,31,3,29,28])).
% 73.34/73.33 cnf(1479,plain,
% 73.34/73.33 (P6(f16(f6(f5(f4(a1,x14791),x14792),f5(x14793,x14794)),x14793),f5(f4(a1,x14795),x14792))),
% 73.34/73.33 inference(scs_inference,[],[992,1469,1461,64,32])).
% 73.34/73.33 cnf(1481,plain,
% 73.34/73.33 (P6(f5(f4(a1,x14811),x14812),f16(f6(f5(f4(a1,x14813),x14812),f5(x14814,x14815)),x14814))),
% 73.34/73.33 inference(scs_inference,[],[992,1469,1461,1463,64,32,31])).
% 73.34/73.33 cnf(1483,plain,
% 73.34/73.33 (E(f5(f4(a1,x14831),f4(a1,x14832)),f5(f4(a1,x14833),a1))),
% 73.34/73.33 inference(scs_inference,[],[993,992,1413,1469,1461,1463,64,32,31,3])).
% 73.34/73.33 cnf(1487,plain,
% 73.34/73.33 (P1(f16(f6(f5(f4(a1,x14871),x14872),f5(x14873,x14874)),x14873),f5(f4(a1,x14875),x14872))),
% 73.34/73.33 inference(scs_inference,[],[993,992,1413,1467,1469,1461,1463,64,32,31,3,28,29])).
% 73.34/73.33 cnf(1489,plain,
% 73.34/73.33 (E(f5(f4(a1,x14891),a1),f5(f4(a1,x14892),f4(a1,x14893)))),
% 73.34/73.33 inference(scs_inference,[],[993,992,1413,1467,1469,1461,1463,64,32,31,3,28,29,2])).
% 73.34/73.33 cnf(1509,plain,
% 73.34/73.33 (E(f4(f12(x15091,a1),f4(a1,x15092)),f4(f12(x15091,a1),f4(a1,x15093)))),
% 73.34/73.33 inference(scs_inference,[],[1029,1388,423,425,32,31,3])).
% 73.34/73.33 cnf(1511,plain,
% 73.34/73.33 (E(f4(f12(x15111,a1),x15112),f4(f12(x15111,a10),x15112))),
% 73.34/73.33 inference(rename_variables,[],[1029])).
% 73.34/73.33 cnf(1514,plain,
% 73.34/73.33 (P1(f16(f6(f4(f12(x15141,a1),x15142),f5(x15143,x15144)),x15143),f4(f12(x15141,a10),x15142))),
% 73.34/73.33 inference(scs_inference,[],[1029,1511,427,429,1388,423,425,32,31,3,28,29])).
% 73.34/73.33 cnf(1523,plain,
% 73.34/73.33 (E(f4(f12(x15231,a1),x15232),f4(f12(x15231,a10),x15232))),
% 73.34/73.33 inference(rename_variables,[],[1029])).
% 73.34/73.33 cnf(1526,plain,
% 73.34/73.33 (E(f4(f12(x15261,a1),x15262),f4(f12(x15261,a10),x15262))),
% 73.34/73.33 inference(rename_variables,[],[1029])).
% 73.34/73.33 cnf(1527,plain,
% 73.34/73.33 (P1(f16(f6(f4(f12(x15271,a1),a1),f5(x15272,x15273)),x15272),f4(f12(x15271,a10),f4(a1,x15274)))),
% 73.34/73.33 inference(scs_inference,[],[1029,1523,1526,1338,1514,1331,1333,64,32,31,29])).
% 73.34/73.33 cnf(1529,plain,
% 73.34/73.33 (E(f4(f12(x15291,a1),x15292),f4(f12(x15291,a10),x15292))),
% 73.34/73.33 inference(rename_variables,[],[1029])).
% 73.34/73.33 cnf(1530,plain,
% 73.34/73.33 (P1(f4(f12(x15301,a10),f4(a1,x15302)),f16(f6(f4(f12(x15301,a1),a1),f5(x15303,x15304)),x15303))),
% 73.34/73.33 inference(scs_inference,[],[1029,1523,1526,1529,1338,1340,1514,1331,1333,64,32,31,29,28])).
% 73.34/73.33 cnf(1536,plain,
% 73.34/73.33 (P6(f4(x15361,a1),f4(x15361,f4(a1,x15362)))),
% 73.34/73.33 inference(rename_variables,[],[1353])).
% 73.34/73.33 cnf(1537,plain,
% 73.34/73.33 (E(f4(f12(x15371,a1),x15372),f4(f12(x15371,a10),x15372))),
% 73.34/73.33 inference(rename_variables,[],[1029])).
% 73.34/73.33 cnf(1540,plain,
% 73.34/73.33 (E(f4(f12(x15401,a1),x15402),f4(f12(x15401,a10),x15402))),
% 73.34/73.33 inference(rename_variables,[],[1029])).
% 73.34/73.33 cnf(1542,plain,
% 73.34/73.33 (P1(f4(x15421,a1),f4(x15421,f4(a1,x15422)))),
% 73.34/73.33 inference(rename_variables,[],[1360])).
% 73.34/73.33 cnf(1543,plain,
% 73.34/73.33 (E(f4(f12(x15431,a1),x15432),f4(f12(x15431,a10),x15432))),
% 73.34/73.33 inference(rename_variables,[],[1029])).
% 73.34/73.33 cnf(1544,plain,
% 73.34/73.33 (P1(f4(f12(x15441,a1),a1),f4(f12(x15441,a10),f4(a1,x15442)))),
% 73.34/73.33 inference(scs_inference,[],[1029,1537,1540,1543,1360,1542,1527,1353,1536,64,32,31,28,29])).
% 73.34/73.33 cnf(1553,plain,
% 73.34/73.33 (P6(f4(x15531,f4(a1,x15532)),f4(x15531,f4(a1,x15533)))),
% 73.34/73.33 inference(rename_variables,[],[1368])).
% 73.34/73.33 cnf(1554,plain,
% 73.34/73.33 (E(f4(f12(x15541,a1),x15542),f4(f12(x15541,a10),x15542))),
% 73.34/73.33 inference(rename_variables,[],[1029])).
% 73.34/73.33 cnf(1557,plain,
% 73.34/73.33 (E(f4(f12(x15571,a1),x15572),f4(f12(x15571,a10),x15572))),
% 73.34/73.33 inference(rename_variables,[],[1029])).
% 73.34/73.33 cnf(1558,plain,
% 73.34/73.33 (P1(f4(f12(x15581,a10),a1),f16(f6(f4(f12(x15581,a1),f4(a1,x15582)),f5(x15583,x15584)),x15583))),
% 73.34/73.33 inference(scs_inference,[],[1029,1554,1557,1392,1530,1368,1553,64,32,31,28])).
% 73.34/73.33 cnf(1560,plain,
% 73.34/73.33 (E(f4(f12(x15601,a1),x15602),f4(f12(x15601,a10),x15602))),
% 73.34/73.33 inference(rename_variables,[],[1029])).
% 73.34/73.33 cnf(1561,plain,
% 73.34/73.33 (P1(f16(f6(f4(f12(x15611,a1),f4(a1,x15612)),f5(x15613,x15614)),x15613),f4(f12(x15611,a10),a1))),
% 73.34/73.33 inference(scs_inference,[],[1029,1554,1557,1560,1390,1392,1530,1368,1553,64,32,31,28,29])).
% 73.34/73.33 cnf(1584,plain,
% 73.34/73.33 (P6(f16(f6(f4(f12(x15841,a1),f4(a1,x15842)),f5(x15843,x15844)),x15843),f4(f12(x15841,a10),a1))),
% 73.34/73.33 inference(scs_inference,[],[1029,1544,1386,64,32])).
% 73.34/73.33 cnf(1586,plain,
% 73.34/73.33 (E(f4(f12(x15861,a1),x15862),f4(f12(x15861,a10),x15862))),
% 73.34/73.33 inference(rename_variables,[],[1029])).
% 73.34/73.33 cnf(1587,plain,
% 73.34/73.33 (P6(f4(f12(x15871,a10),a1),f16(f6(f4(f12(x15871,a1),f4(a1,x15872)),f5(x15873,x15874)),x15873))),
% 73.34/73.33 inference(scs_inference,[],[1029,1586,1544,1386,1384,64,32,31])).
% 73.34/73.33 cnf(1600,plain,
% 73.34/73.33 (P6(x16001,x16001)),
% 73.34/73.33 inference(rename_variables,[],[47])).
% 73.34/73.33 cnf(1603,plain,
% 73.34/73.33 (P1(f4(f12(x16031,a10),x16032),f4(f12(x16031,a1),x16032))),
% 73.34/73.33 inference(scs_inference,[],[1029,1561,46,47,1600,64,32,31,28])).
% 73.34/73.33 cnf(1604,plain,
% 73.34/73.33 (P1(x16041,x16041)),
% 73.34/73.33 inference(rename_variables,[],[46])).
% 73.34/73.33 cnf(1605,plain,
% 73.34/73.33 (P1(f4(f12(x16051,a1),x16052),f4(f12(x16051,a10),x16052))),
% 73.34/73.33 inference(scs_inference,[],[1029,1561,46,1604,47,1600,64,32,31,28,29])).
% 73.34/73.33 cnf(1613,plain,
% 73.34/73.33 (~P9(f4(f12(x16131,a1),x16132),f4(f12(x16131,a10),x16132))),
% 73.34/73.33 inference(scs_inference,[],[1603,64])).
% 73.34/73.33 cnf(1615,plain,
% 73.34/73.33 (~P9(f4(f12(x16151,a10),x16152),f4(f12(x16151,a1),x16152))),
% 73.34/73.33 inference(scs_inference,[],[1605,64])).
% 73.34/73.33 cnf(1625,plain,
% 73.34/73.33 (E(f4(f12(x16251,a10),f4(a1,x16252)),f4(f12(x16251,a10),f4(a1,x16253)))),
% 73.34/73.33 inference(scs_inference,[],[1032,1396,423,425,32,31,3])).
% 73.34/73.33 cnf(1669,plain,
% 73.34/73.33 (E(f6(a1,x16691),f6(f4(a1,x16692),x16691))),
% 73.34/73.33 inference(scs_inference,[],[44,2,8])).
% 73.34/73.33 cnf(1670,plain,
% 73.34/73.33 (E(f6(f4(a1,x16701),x16702),f6(a1,x16702))),
% 73.34/73.33 inference(scs_inference,[],[1669,2])).
% 73.34/73.33 cnf(1682,plain,
% 73.34/73.33 (P4(f6(x16821,f5(f5(x16822,a1),x16823)),f5(x16822,f4(a1,x16824)))),
% 73.34/73.33 inference(scs_inference,[],[1097,97,35])).
% 73.34/73.33 cnf(1690,plain,
% 73.34/73.33 (P1(f16(f6(f5(x16901,a1),f5(x16902,x16903)),x16902),f5(x16901,f4(a1,x16904)))),
% 73.34/73.33 inference(scs_inference,[],[1097,427,429,97,423,425,35,32,31,28,29])).
% 73.34/73.33 cnf(1697,plain,
% 73.34/73.33 (P4(f6(x16971,f5(f5(a1,a1),x16972)),f5(f4(a1,x16973),f4(a1,x16974)))),
% 73.34/73.33 inference(scs_inference,[],[1097,1407,1690,64,35])).
% 73.34/73.33 cnf(1699,plain,
% 73.34/73.33 (E(f5(x16991,a1),f5(x16991,f4(a1,x16992)))),
% 73.34/73.33 inference(rename_variables,[],[1097])).
% 73.34/73.33 cnf(1700,plain,
% 73.34/73.33 (P6(f5(f8(f19(x17001,a1,x17002)),a1),f5(f19(x17001,a1,a3),f4(a1,x17003)))),
% 73.34/73.33 inference(scs_inference,[],[1097,1699,1407,1690,899,64,35,32])).
% 73.34/73.33 cnf(1701,plain,
% 73.34/73.33 (P6(f5(f8(f19(x17011,a1,x17012)),x17013),f5(f19(x17011,a1,a3),x17013))),
% 73.34/73.33 inference(rename_variables,[],[899])).
% 73.34/73.33 cnf(1702,plain,
% 73.34/73.33 (E(f5(x17021,a1),f5(x17021,f4(a1,x17022)))),
% 73.34/73.33 inference(rename_variables,[],[1097])).
% 73.34/73.33 cnf(1705,plain,
% 73.34/73.33 (E(f5(x17051,a1),f5(x17051,f4(a1,x17052)))),
% 73.34/73.33 inference(rename_variables,[],[1097])).
% 73.34/73.33 cnf(1706,plain,
% 73.34/73.33 (P1(f5(f8(f19(x17061,a1,x17062)),f4(a1,x17063)),f5(f19(x17061,a1,a3),a1))),
% 73.34/73.33 inference(scs_inference,[],[1097,1699,1702,1705,903,1407,1690,899,1701,64,35,32,31,28])).
% 73.34/73.33 cnf(1707,plain,
% 73.34/73.33 (P1(f5(f8(f19(x17071,a1,x17072)),x17073),f5(f19(x17071,a1,a3),x17073))),
% 73.34/73.33 inference(rename_variables,[],[903])).
% 73.34/73.33 cnf(1708,plain,
% 73.34/73.33 (E(f5(x17081,a1),f5(x17081,f4(a1,x17082)))),
% 73.34/73.33 inference(rename_variables,[],[1097])).
% 73.34/73.33 cnf(1709,plain,
% 73.34/73.33 (P1(f5(f8(f19(x17091,a1,x17092)),a1),f5(f19(x17091,a1,a3),f4(a1,x17093)))),
% 73.34/73.33 inference(scs_inference,[],[1097,1699,1702,1705,1708,903,1707,1407,1690,899,1701,64,35,32,31,28,29])).
% 73.34/73.33 cnf(1718,plain,
% 73.34/73.33 (P6(f5(f19(x17181,a1,a3),x17182),f5(f8(f19(x17181,a1,x17183)),x17182))),
% 73.34/73.33 inference(rename_variables,[],[901])).
% 73.34/73.33 cnf(1719,plain,
% 73.34/73.33 (E(f5(x17191,a1),f5(x17191,f4(a1,x17192)))),
% 73.34/73.33 inference(rename_variables,[],[1097])).
% 73.34/73.33 cnf(1722,plain,
% 73.34/73.33 (E(f5(x17221,a1),f5(x17221,f4(a1,x17222)))),
% 73.34/73.33 inference(rename_variables,[],[1097])).
% 73.34/73.33 cnf(1724,plain,
% 73.34/73.33 (P1(f5(f19(x17241,a1,a3),x17242),f5(f8(f19(x17241,a1,x17243)),x17242))),
% 73.34/73.33 inference(rename_variables,[],[905])).
% 73.34/73.33 cnf(1725,plain,
% 73.34/73.33 (E(f5(x17251,a1),f5(x17251,f4(a1,x17252)))),
% 73.34/73.33 inference(rename_variables,[],[1097])).
% 73.34/73.33 cnf(1726,plain,
% 73.34/73.34 (P1(f5(f19(x17261,a1,a3),a1),f5(f8(f19(x17261,a1,x17262)),f4(a1,x17263)))),
% 73.34/73.34 inference(scs_inference,[],[1097,1719,1722,1725,905,1724,1706,901,1718,64,32,31,28,29])).
% 73.34/73.34 cnf(1732,plain,
% 73.34/73.34 (P6(f5(f4(a1,x17321),x17322),f5(a1,x17322))),
% 73.34/73.34 inference(rename_variables,[],[1430])).
% 73.34/73.34 cnf(1733,plain,
% 73.34/73.34 (E(f5(x17331,a1),f5(x17331,f4(a1,x17332)))),
% 73.34/73.34 inference(rename_variables,[],[1097])).
% 73.34/73.34 cnf(1734,plain,
% 73.34/73.34 (P6(f5(f4(a1,x17341),f4(a1,x17342)),f5(a1,a1))),
% 73.34/73.34 inference(scs_inference,[],[1097,1733,1709,1430,1732,64,32,31])).
% 73.34/73.34 cnf(1736,plain,
% 73.34/73.34 (E(f5(x17361,a1),f5(x17361,f4(a1,x17362)))),
% 73.34/73.34 inference(rename_variables,[],[1097])).
% 73.34/73.34 cnf(1737,plain,
% 73.34/73.34 (P1(f5(a1,f4(a1,x17371)),f5(f4(a1,x17372),a1))),
% 73.34/73.34 inference(scs_inference,[],[1097,1733,1736,1437,1709,1430,1732,64,32,31,28])).
% 73.34/73.34 cnf(1738,plain,
% 73.34/73.34 (P1(f5(a1,x17381),f5(f4(a1,x17382),x17381))),
% 73.34/73.34 inference(rename_variables,[],[1437])).
% 73.34/73.34 cnf(1739,plain,
% 73.34/73.34 (E(f5(x17391,a1),f5(x17391,f4(a1,x17392)))),
% 73.34/73.34 inference(rename_variables,[],[1097])).
% 73.34/73.34 cnf(1740,plain,
% 73.34/73.34 (P1(f5(a1,a1),f5(f4(a1,x17401),f4(a1,x17402)))),
% 73.34/73.34 inference(scs_inference,[],[1097,1733,1736,1739,1437,1738,1709,1430,1732,64,32,31,28,29])).
% 73.34/73.34 cnf(1745,plain,
% 73.34/73.34 (~P9(f5(f8(f19(x17451,a1,x17452)),f4(a1,x17453)),f5(f19(x17451,a1,a3),a1))),
% 73.34/73.34 inference(scs_inference,[],[1726,64])).
% 73.34/73.34 cnf(1748,plain,
% 73.34/73.34 (P6(f5(f4(a1,x17481),x17482),f5(f4(a1,x17483),x17482))),
% 73.34/73.34 inference(rename_variables,[],[1449])).
% 73.34/73.34 cnf(1749,plain,
% 73.34/73.34 (E(f5(x17491,a1),f5(x17491,f4(a1,x17492)))),
% 73.34/73.34 inference(rename_variables,[],[1097])).
% 73.34/73.34 cnf(1750,plain,
% 73.34/73.34 (P6(f5(f4(a1,x17501),f4(a1,x17502)),f5(f4(a1,x17503),a1))),
% 73.34/73.34 inference(scs_inference,[],[1097,1749,1726,1449,1748,64,32,31])).
% 73.34/73.34 cnf(1752,plain,
% 73.34/73.34 (E(f5(x17521,a1),f5(x17521,f4(a1,x17522)))),
% 73.34/73.34 inference(rename_variables,[],[1097])).
% 73.34/73.34 cnf(1753,plain,
% 73.34/73.34 (P1(f5(f4(a1,x17531),f4(a1,x17532)),f5(a1,a1))),
% 73.34/73.34 inference(scs_inference,[],[1097,1749,1752,1439,1726,1449,1748,64,32,31,28])).
% 73.34/73.34 cnf(1763,plain,
% 73.34/73.34 (P6(f5(a1,x17631),f5(f4(a1,x17632),x17631))),
% 73.34/73.34 inference(rename_variables,[],[1432])).
% 73.34/73.34 cnf(1764,plain,
% 73.34/73.34 (E(f5(x17641,a1),f5(x17641,f4(a1,x17642)))),
% 73.34/73.34 inference(rename_variables,[],[1097])).
% 73.34/73.34 cnf(1767,plain,
% 73.34/73.34 (E(f5(x17671,a1),f5(x17671,f4(a1,x17672)))),
% 73.34/73.34 inference(rename_variables,[],[1097])).
% 73.34/73.34 cnf(1770,plain,
% 73.34/73.34 (E(f5(x17701,a1),f5(x17701,f4(a1,x17702)))),
% 73.34/73.34 inference(rename_variables,[],[1097])).
% 73.34/73.34 cnf(1771,plain,
% 73.34/73.34 (P1(f16(f6(f5(a1,a1),f5(x17711,x17712)),x17711),f5(f4(a1,x17713),f4(a1,x17714)))),
% 73.34/73.34 inference(scs_inference,[],[1097,1764,1767,1770,1416,1418,1740,1432,1763,64,32,31,28,29])).
% 73.34/73.34 cnf(1779,plain,
% 73.34/73.34 (E(f5(x17791,a1),f5(x17791,f4(a1,x17792)))),
% 73.34/73.34 inference(rename_variables,[],[1097])).
% 73.34/73.34 cnf(1782,plain,
% 73.34/73.34 (E(f5(x17821,a1),f5(x17821,f4(a1,x17822)))),
% 73.34/73.34 inference(rename_variables,[],[1097])).
% 73.34/73.34 cnf(1783,plain,
% 73.34/73.34 (P1(f5(f4(a1,x17831),f4(a1,x17832)),f5(f4(a1,x17833),a1))),
% 73.34/73.34 inference(scs_inference,[],[1097,1779,1782,1451,1737,1411,1481,64,32,31,28])).
% 73.34/73.34 cnf(1812,plain,
% 73.34/73.34 (E(f5(x18121,a1),f5(x18121,f4(a1,x18122)))),
% 73.34/73.34 inference(rename_variables,[],[1097])).
% 73.34/73.34 cnf(1815,plain,
% 73.34/73.34 (E(f5(x18151,a1),f5(x18151,f4(a1,x18152)))),
% 73.34/73.34 inference(rename_variables,[],[1097])).
% 73.34/73.34 cnf(1816,plain,
% 73.34/73.34 (P1(f5(f4(a1,x18161),a1),f5(f4(a1,x18162),f4(a1,x18163)))),
% 73.34/73.34 inference(scs_inference,[],[1097,1812,1815,1451,1771,1461,1463,64,32,31,29])).
% 73.34/73.34 cnf(1818,plain,
% 73.34/73.34 (E(f5(x18181,a1),f5(x18181,f4(a1,x18182)))),
% 73.34/73.34 inference(rename_variables,[],[1097])).
% 73.34/73.34 cnf(1819,plain,
% 73.34/73.34 (P1(f5(a1,f4(a1,x18191)),f16(f6(f5(f4(a1,x18192),a1),f5(x18193,x18194)),x18193))),
% 73.34/73.34 inference(scs_inference,[],[1097,1812,1815,1818,1451,1469,1771,1461,1463,64,32,31,29,28])).
% 73.34/73.34 cnf(1822,plain,
% 73.34/73.34 (E(f4(f5(x18221,f4(a1,x18222)),x18223),f4(f5(x18221,a1),x18223))),
% 73.34/73.34 inference(scs_inference,[],[1097,2,4])).
% 73.34/73.34 cnf(1823,plain,
% 73.34/73.34 (E(f4(f5(x18231,a1),x18232),f4(f5(x18231,f4(a1,x18233)),x18232))),
% 73.34/73.34 inference(scs_inference,[],[1822,2])).
% 73.34/73.34 cnf(1828,plain,
% 73.34/73.34 (P6(f5(a1,f4(a1,x18281)),f5(a1,a1))),
% 73.34/73.34 inference(scs_inference,[],[1097,993,1783,1822,1734,2,64,32,31])).
% 73.34/73.34 cnf(1861,plain,
% 73.34/73.34 (E(f5(x18611,a1),f5(x18611,f4(a1,x18612)))),
% 73.34/73.34 inference(rename_variables,[],[1097])).
% 73.34/73.34 cnf(1863,plain,
% 73.34/73.34 (E(f5(x18631,a1),f5(x18631,f4(a1,x18632)))),
% 73.34/73.34 inference(rename_variables,[],[1097])).
% 73.34/73.34 cnf(1866,plain,
% 73.34/73.34 (P1(f5(f19(x18661,a1,a3),f4(a1,x18662)),f5(f19(x18661,a1,a3),a1))),
% 73.34/73.34 inference(scs_inference,[],[1097,1861,1863,521,1706,1783,1753,1828,1700,64,32,31,29,28])).
% 73.34/73.34 cnf(1915,plain,
% 73.34/73.34 (E(f5(x19151,a1),f5(x19151,f4(a1,x19152)))),
% 73.34/73.34 inference(rename_variables,[],[1097])).
% 73.34/73.34 cnf(1916,plain,
% 73.34/73.34 (P6(f5(x19161,f4(a1,x19162)),f5(x19161,a1))),
% 73.34/73.34 inference(scs_inference,[],[1097,1915,1866,1750,47,64,32,31])).
% 73.34/73.34 cnf(1919,plain,
% 73.34/73.34 (E(f5(x19191,a1),f5(x19191,f4(a1,x19192)))),
% 73.34/73.34 inference(rename_variables,[],[1097])).
% 73.34/73.34 cnf(1920,plain,
% 73.34/73.34 (P1(f5(x19201,a1),f5(x19201,f4(a1,x19202)))),
% 73.34/73.34 inference(scs_inference,[],[1097,1915,1919,1866,1726,1750,46,47,64,32,31,28,29])).
% 73.34/73.34 cnf(1934,plain,
% 73.34/73.34 (P1(f5(x19341,f4(a1,x19342)),f5(x19341,f4(a1,x19343)))),
% 73.34/73.34 inference(scs_inference,[],[1097,518,1816,1920,1700,64,32,28])).
% 73.34/73.34 cnf(1940,plain,
% 73.34/73.34 (P1(f5(x19401,f4(a1,x19402)),f5(x19401,a1))),
% 73.34/73.34 inference(scs_inference,[],[1097,1819,46,47,64,32,28])).
% 73.34/73.34 cnf(1950,plain,
% 73.34/73.34 (~P9(f5(x19501,f4(a1,x19502)),f5(x19501,f4(a1,x19503)))),
% 73.34/73.34 inference(scs_inference,[],[1934,64])).
% 73.34/73.34 cnf(1959,plain,
% 73.34/73.34 (~P9(f5(x19591,a1),f5(x19591,f4(a1,x19592)))),
% 73.34/73.34 inference(scs_inference,[],[1940,64])).
% 73.34/73.34 cnf(1965,plain,
% 73.34/73.34 (~P9(f5(x19651,f4(a1,x19652)),f5(x19651,a1))),
% 73.34/73.34 inference(scs_inference,[],[1920,64])).
% 73.34/73.34 cnf(1968,plain,
% 73.34/73.34 (E(f5(f8(f19(x19681,a1,x19682)),f4(a1,x19683)),f5(f19(x19681,a1,a3),f4(a1,x19684)))),
% 73.34/73.34 inference(scs_inference,[],[1098,1099,3])).
% 73.34/73.34 cnf(1969,plain,
% 73.34/73.34 (E(f5(x19691,f4(a1,x19692)),f5(x19691,a1))),
% 73.34/73.34 inference(rename_variables,[],[1098])).
% 73.34/73.34 cnf(1970,plain,
% 73.34/73.34 (P6(f16(f6(f5(x19701,f4(a1,x19702)),f5(x19703,x19704)),x19703),f5(x19701,a1))),
% 73.34/73.34 inference(scs_inference,[],[1098,1969,1099,425,3,32])).
% 73.34/73.34 cnf(1972,plain,
% 73.34/73.34 (P6(f5(x19721,a1),f16(f6(f5(x19721,f4(a1,x19722)),f5(x19723,x19724)),x19723))),
% 73.34/73.34 inference(scs_inference,[],[1098,1969,1099,423,425,3,32,31])).
% 73.34/73.34 cnf(1974,plain,
% 73.34/73.34 (P1(f16(f6(f5(x19741,f4(a1,x19742)),f5(x19743,x19744)),x19743),f5(x19741,a1))),
% 73.34/73.34 inference(scs_inference,[],[1098,1969,1099,427,423,425,3,32,31,29])).
% 73.34/73.34 cnf(1976,plain,
% 73.34/73.34 (P1(f5(x19761,a1),f16(f6(f5(x19761,f4(a1,x19762)),f5(x19763,x19764)),x19763))),
% 73.34/73.34 inference(scs_inference,[],[1098,1969,1099,427,429,423,425,3,32,31,29,28])).
% 73.34/73.34 cnf(1978,plain,
% 73.34/73.34 (E(f5(f19(x19781,a1,a3),f4(a1,x19782)),f5(f8(f19(x19781,a1,x19783)),f4(a1,x19784)))),
% 73.34/73.34 inference(scs_inference,[],[1098,1969,1099,427,429,423,425,3,32,31,29,28,2])).
% 73.34/73.34 cnf(1985,plain,
% 73.34/73.34 (E(f5(x19851,f4(a1,x19852)),f5(x19851,a1))),
% 73.34/73.34 inference(rename_variables,[],[1098])).
% 73.34/73.34 cnf(1988,plain,
% 73.34/73.34 (E(f5(x19881,f4(a1,x19882)),f5(x19881,a1))),
% 73.34/73.34 inference(rename_variables,[],[1098])).
% 73.34/73.34 cnf(1991,plain,
% 73.34/73.34 (E(f5(x19911,f4(a1,x19912)),f5(x19911,a1))),
% 73.34/73.34 inference(rename_variables,[],[1098])).
% 73.34/73.34 cnf(1992,plain,
% 73.34/73.34 (P1(f16(f6(f5(a1,f4(a1,x19921)),f5(x19922,x19923)),x19922),f5(f4(a1,x19924),a1))),
% 73.34/73.34 inference(scs_inference,[],[1098,1985,1988,1991,1120,1416,1976,1411,1481,64,3,32,31,29])).
% 73.34/73.34 cnf(1994,plain,
% 73.34/73.34 (E(f5(x19941,f4(a1,x19942)),f5(x19941,a1))),
% 73.34/73.34 inference(rename_variables,[],[1098])).
% 73.34/73.34 cnf(1995,plain,
% 73.34/73.34 (P1(f5(f4(a1,x19951),a1),f16(f6(f5(a1,f4(a1,x19952)),f5(x19953,x19954)),x19953))),
% 73.34/73.34 inference(scs_inference,[],[1098,1985,1988,1991,1994,1120,1416,1418,1976,1411,1481,64,3,32,31,29,28])).
% 73.34/73.34 cnf(2004,plain,
% 73.34/73.34 (E(f5(x20041,f4(a1,x20042)),f5(x20041,a1))),
% 73.34/73.34 inference(rename_variables,[],[1098])).
% 73.34/73.34 cnf(2007,plain,
% 73.34/73.34 (E(f5(x20071,f4(a1,x20072)),f5(x20071,a1))),
% 73.34/73.34 inference(rename_variables,[],[1098])).
% 73.34/73.34 cnf(2008,plain,
% 73.34/73.34 (P1(f16(f6(f5(f4(a1,x20081),f4(a1,x20082)),f5(x20083,x20084)),x20083),f5(f4(a1,x20085),a1))),
% 73.34/73.34 inference(scs_inference,[],[1098,2004,2007,1097,1487,1992,1479,1409,64,3,32,31,29])).
% 73.34/73.34 cnf(2018,plain,
% 73.34/73.34 (E(f5(f4(a1,x20181),f4(a1,x20182)),f5(a1,f4(a1,x20183)))),
% 73.34/73.34 inference(scs_inference,[],[1098,1422,1995,64,3])).
% 73.34/73.34 cnf(2019,plain,
% 73.34/73.34 (E(f5(x20191,f4(a1,x20192)),f5(x20191,a1))),
% 73.34/73.34 inference(rename_variables,[],[1098])).
% 73.34/73.34 cnf(2022,plain,
% 73.34/73.34 (E(f5(x20221,f4(a1,x20222)),f5(x20221,a1))),
% 73.34/73.34 inference(rename_variables,[],[1098])).
% 73.34/73.34 cnf(2025,plain,
% 73.34/73.34 (E(f5(x20251,f4(a1,x20252)),f5(x20251,a1))),
% 73.34/73.34 inference(rename_variables,[],[1098])).
% 73.34/73.34 cnf(2028,plain,
% 73.34/73.34 (E(f5(x20281,f4(a1,x20282)),f5(x20281,a1))),
% 73.34/73.34 inference(rename_variables,[],[1098])).
% 73.34/73.34 cnf(2032,plain,
% 73.34/73.34 (E(f5(a1,f4(a1,x20321)),f5(f4(a1,x20322),f4(a1,x20323)))),
% 73.34/73.34 inference(scs_inference,[],[1098,2019,2022,2025,2028,1422,1467,1469,1995,1461,1463,64,3,32,31,29,28,2])).
% 73.34/73.34 cnf(2038,plain,
% 73.34/73.34 (E(f5(f4(a1,x20381),f4(a1,x20382)),f5(f4(a1,x20383),f4(a1,x20384)))),
% 73.34/73.34 inference(scs_inference,[],[1098,1489,2008,64,3])).
% 73.34/73.34 cnf(2076,plain,
% 73.34/73.34 (E(f6(x20761,a1),f6(x20761,f4(a1,x20762)))),
% 73.34/73.34 inference(scs_inference,[],[44,2,9])).
% 73.34/73.34 cnf(2077,plain,
% 73.34/73.34 (E(f6(x20771,f4(a1,x20772)),f6(x20771,a1))),
% 73.34/73.34 inference(scs_inference,[],[2076,2])).
% 73.34/73.34 cnf(2141,plain,
% 73.34/73.34 (E(f19(a1,x21411,x21412),f19(f4(a1,x21413),x21411,x21412))),
% 73.34/73.34 inference(scs_inference,[],[44,2,10])).
% 73.34/73.34 cnf(2142,plain,
% 73.34/73.34 (E(f19(f4(a1,x21421),x21422,x21423),f19(a1,x21422,x21423))),
% 73.34/73.34 inference(scs_inference,[],[2141,2])).
% 73.34/73.34 cnf(2143,plain,
% 73.34/73.34 (E(f17(f19(a1,a10,x21431),f7(f19(a9,a10,a11))),f19(f4(a1,x21432),a10,a3))),
% 73.34/73.34 inference(scs_inference,[],[652,2141,2,3])).
% 73.34/73.34 cnf(2154,plain,
% 73.34/73.34 (E(f17(f19(f4(a1,x21541),a10,x21542),f7(f19(a9,a10,a11))),f19(a1,a10,a3))),
% 73.34/73.34 inference(scs_inference,[],[652,2142,2143,2,3])).
% 73.34/73.34 cnf(2160,plain,
% 73.34/73.34 (E(f19(a1,a10,a3),f17(f19(f4(a1,x21601),a10,x21602),f7(f19(a9,a10,a11))))),
% 73.34/73.34 inference(scs_inference,[],[2154,2])).
% 73.34/73.34 cnf(2202,plain,
% 73.34/73.34 (E(f4(f5(x22021,a1),a1),f4(f5(x22021,f4(a1,x22022)),f4(a1,x22023)))),
% 73.34/73.34 inference(scs_inference,[],[979,1823,3])).
% 73.34/73.34 cnf(2205,plain,
% 73.34/73.34 (E(f4(f5(x22051,f4(a1,x22052)),f4(a1,x22053)),f4(f5(x22051,a1),a1))),
% 73.34/73.34 inference(scs_inference,[],[979,1823,3,2])).
% 73.34/73.34 cnf(2214,plain,
% 73.34/73.34 (E(f4(f5(x22141,a1),f4(a1,x22142)),f4(f5(x22141,f4(a1,x22143)),f4(a1,x22144)))),
% 73.34/73.34 inference(scs_inference,[],[980,2202,3])).
% 73.34/73.34 cnf(2248,plain,
% 73.34/73.34 (P6(f16(f6(f4(f12(x22481,a10),f4(a1,x22482)),f5(x22483,x22484)),x22483),f4(f12(x22481,a1),f4(a1,x22485)))),
% 73.34/73.34 inference(scs_inference,[],[1335,1386,32])).
% 73.34/73.34 cnf(2254,plain,
% 73.34/73.34 (P1(f16(f6(f4(f12(x22541,a10),f4(a1,x22542)),f5(x22543,x22544)),x22543),f4(f12(x22541,a1),f4(a1,x22545)))),
% 73.34/73.34 inference(scs_inference,[],[1335,1390,1392,1386,1384,32,31,28,29])).
% 73.34/73.34 cnf(2260,plain,
% 73.34/73.34 (P6(f16(f6(f4(f12(x22601,a1),f4(a1,x22602)),f5(x22603,x22604)),x22603),f4(f12(x22601,a1),f4(a1,x22605)))),
% 73.34/73.34 inference(scs_inference,[],[1335,2254,1584,64,32])).
% 73.34/73.34 cnf(2262,plain,
% 73.34/73.34 (P6(f4(f12(x22621,a1),f4(a1,x22622)),f16(f6(f4(f12(x22621,a1),f4(a1,x22623)),f5(x22624,x22625)),x22624))),
% 73.34/73.34 inference(scs_inference,[],[1335,2254,1584,1587,64,32,31])).
% 73.34/73.34 cnf(2264,plain,
% 73.34/73.34 (P1(f4(f12(x22641,a1),f4(a1,x22642)),f16(f6(f4(f12(x22641,a1),f4(a1,x22643)),f5(x22644,x22645)),x22644))),
% 73.34/73.34 inference(scs_inference,[],[1335,1558,2254,1584,1587,64,32,31,28])).
% 73.34/73.34 cnf(2266,plain,
% 73.34/73.34 (P1(f16(f6(f4(f12(x22661,a1),f4(a1,x22662)),f5(x22663,x22664)),x22663),f4(f12(x22661,a1),f4(a1,x22665)))),
% 73.34/73.34 inference(scs_inference,[],[1335,1561,1558,2254,1584,1587,64,32,31,28,29])).
% 73.34/73.34 cnf(2273,plain,
% 73.34/73.34 (E(f4(f12(x22731,a1),x22732),f4(f12(x22731,a10),x22732))),
% 73.34/73.34 inference(rename_variables,[],[1029])).
% 73.34/73.34 cnf(2276,plain,
% 73.34/73.34 (E(f4(f12(x22761,a1),x22762),f4(f12(x22761,a10),x22762))),
% 73.34/73.34 inference(rename_variables,[],[1029])).
% 73.34/73.34 cnf(2277,plain,
% 73.34/73.34 (P1(f4(f12(x22771,a10),f4(a1,x22772)),f16(f6(f4(f12(x22771,a1),f4(a1,x22773)),f5(x22774,x22775)),x22774))),
% 73.34/73.34 inference(scs_inference,[],[1029,2273,2276,2266,2264,2260,2262,64,32,31,28])).
% 73.34/73.34 cnf(2279,plain,
% 73.34/73.34 (E(f4(f12(x22791,a1),x22792),f4(f12(x22791,a10),x22792))),
% 73.34/73.34 inference(rename_variables,[],[1029])).
% 73.34/73.34 cnf(2280,plain,
% 73.34/73.34 (P1(f16(f6(f4(f12(x22801,a1),f4(a1,x22802)),f5(x22803,x22804)),x22803),f4(f12(x22801,a10),f4(a1,x22805)))),
% 73.34/73.34 inference(scs_inference,[],[1029,2273,2276,2279,2266,2264,2260,2262,64,32,31,28,29])).
% 73.34/73.34 cnf(2286,plain,
% 73.34/73.34 (P6(f16(f6(f4(f12(x22861,a10),f4(a1,x22862)),f5(x22863,x22864)),x22863),f4(f12(x22861,a10),f4(a1,x22865)))),
% 73.34/73.34 inference(scs_inference,[],[1029,2280,2248,64,32])).
% 73.34/73.34 cnf(2307,plain,
% 73.34/73.34 (~E(f6(x23071,f5(f7(f19(a9,a10,a11)),x23072)),a10)),
% 73.34/73.34 inference(scs_inference,[],[101,178,97,2277,146,64,34])).
% 73.34/73.34 cnf(2310,plain,
% 73.34/73.34 (E(x23101,f16(f6(x23101,f5(x23102,x23103)),x23102))),
% 73.34/73.34 inference(rename_variables,[],[196])).
% 73.34/73.34 cnf(2315,plain,
% 73.34/73.34 (E(f8(f4(f4(a1,x23151),x23152)),f8(f4(f4(a1,x23153),x23152)))),
% 73.34/73.34 inference(scs_inference,[],[101,349,348,198,196,2310,178,676,97,2277,367,146,64,34,42,43,35,3])).
% 73.34/73.34 cnf(2334,plain,
% 73.34/73.34 (P6(f16(f6(f5(x23341,f4(a1,x23342)),f5(x23343,x23344)),x23343),f8(f5(x23341,a1)))),
% 73.34/73.34 inference(scs_inference,[],[1970,63])).
% 73.34/73.34 cnf(2336,plain,
% 73.34/73.34 (P6(f16(f6(f5(x23361,f4(a1,x23362)),f5(x23363,x23364)),x23363),f13(f5(x23361,a1),x23365))),
% 73.34/73.34 inference(scs_inference,[],[1970,63,67])).
% 73.34/73.34 cnf(2338,plain,
% 73.34/73.34 (P6(f16(f6(f5(x23381,f4(a1,x23382)),f5(x23383,x23384)),x23383),f17(f5(x23381,a1),x23385))),
% 73.34/73.34 inference(scs_inference,[],[1970,63,67,68])).
% 73.34/73.34 cnf(2340,plain,
% 73.34/73.34 (~P5(f19(x23401,a1,x23402),x23403)),
% 73.34/73.34 inference(scs_inference,[],[1970,57,63,67,68,82])).
% 73.34/73.34 cnf(2347,plain,
% 73.34/73.34 (P4(f6(f6(x23471,f5(f5(x23472,a1),x23473)),f5(x23474,x23475)),f5(x23472,f4(a1,x23476)))),
% 73.34/73.34 inference(scs_inference,[],[1970,1682,2214,2038,57,63,67,68,82,17,20,23,70,72])).
% 73.34/73.34 cnf(2369,plain,
% 73.34/73.34 (P8(f6(f6(x23691,f5(a3,a3)),f5(x23692,x23693)),f15(f6(x23694,f5(x23695,a3)),x23695),a3)),
% 73.34/73.34 inference(scs_inference,[],[1970,1247,1682,2214,716,2038,57,63,67,68,82,17,20,23,70,72,4,5,6,7,8,9,13,14,15,16,18,19,21,22,24,25,26,27,69,83])).
% 73.34/73.34 cnf(2374,plain,
% 73.34/73.34 (E(f7(f19(x23741,f6(x23742,f5(x23743,x23744)),x23745)),f14(x23741))),
% 73.34/73.34 inference(scs_inference,[],[1970,1247,1682,2214,716,2038,117,57,63,67,68,82,17,20,23,70,72,4,5,6,7,8,9,13,14,15,16,18,19,21,22,24,25,26,27,69,83,10,11,12,73])).
% 73.34/73.34 cnf(2376,plain,
% 73.34/73.34 (E(f17(f19(x23761,a1,x23762),x23763),f19(x23761,a1,a3))),
% 73.34/73.34 inference(scs_inference,[],[1970,1247,1682,2214,716,2038,117,57,63,67,68,82,17,20,23,70,72,4,5,6,7,8,9,13,14,15,16,18,19,21,22,24,25,26,27,69,83,10,11,12,73,81])).
% 73.34/73.34 cnf(2378,plain,
% 73.34/73.34 (E(f6(f4(x23781,f4(a1,x23782)),f5(x23783,a1)),f4(f6(x23781,f5(x23783,a1)),f4(a1,x23782)))),
% 73.34/73.34 inference(scs_inference,[],[1970,1247,1682,2214,716,2038,117,115,57,63,67,68,82,17,20,23,70,72,4,5,6,7,8,9,13,14,15,16,18,19,21,22,24,25,26,27,69,83,10,11,12,73,81,78])).
% 73.34/73.34 cnf(2384,plain,
% 73.34/73.34 (~E(f15(f6(x23841,f5(x23842,a1)),x23842),a10)),
% 73.34/73.34 inference(scs_inference,[],[139,1970,1247,1682,2214,716,2038,117,115,57,933,63,67,68,82,17,20,23,70,72,4,5,6,7,8,9,13,14,15,16,18,19,21,22,24,25,26,27,69,83,10,11,12,73,81,78,76,91,2])).
% 73.34/73.34 cnf(2386,plain,
% 73.34/73.34 (E(f4(f5(x23861,a1),f4(a1,x23862)),f4(f5(x23861,f4(a1,x23863)),f4(a1,x23864)))),
% 73.34/73.34 inference(rename_variables,[],[2214])).
% 73.34/73.34 cnf(2388,plain,
% 73.34/73.34 (~P5(f19(x23881,a10,x23882),f16(f6(f7(f19(a9,a10,a11)),f5(x23883,x23884)),x23883))),
% 73.34/73.34 inference(scs_inference,[],[1366,139,1970,1247,1682,2214,716,2038,117,502,115,57,933,49,63,67,68,82,17,20,23,70,72,4,5,6,7,8,9,13,14,15,16,18,19,21,22,24,25,26,27,69,83,10,11,12,73,81,78,76,91,2,38,40])).
% 73.34/73.34 cnf(2389,plain,
% 73.34/73.34 (E(f16(f6(x23891,f5(x23892,x23893)),x23892),x23891)),
% 73.34/73.34 inference(rename_variables,[],[49])).
% 73.34/73.34 cnf(2393,plain,
% 73.34/73.34 (P4(f6(x23931,f5(a1,x23932)),f4(a1,x23933))),
% 73.34/73.34 inference(rename_variables,[],[611])).
% 73.34/73.34 cnf(2398,plain,
% 73.34/73.34 (E(f19(f18(x23981,f14(a9)),f16(a10,f14(a9)),x23982),f17(f19(x23981,a10,x23982),f14(a9)))),
% 73.34/73.34 inference(scs_inference,[],[1366,139,1970,1247,1682,2214,716,2038,1239,112,611,2393,103,117,502,115,57,933,49,105,63,67,68,82,17,20,23,70,72,4,5,6,7,8,9,13,14,15,16,18,19,21,22,24,25,26,27,69,83,10,11,12,73,81,78,76,91,2,38,40,75,74,80,88])).
% 73.34/73.34 cnf(2400,plain,
% 73.34/73.34 (~P8(f16(f6(f4(a1,x24001),f5(x24002,x24003)),x24002),x24004,x24005)),
% 73.34/73.34 inference(scs_inference,[],[1366,139,1970,1247,1682,2214,716,2038,1239,58,112,611,2393,103,744,117,502,115,57,933,49,105,63,67,68,82,17,20,23,70,72,4,5,6,7,8,9,13,14,15,16,18,19,21,22,24,25,26,27,69,83,10,11,12,73,81,78,76,91,2,38,40,75,74,80,88,41])).
% 73.34/73.34 cnf(2404,plain,
% 73.34/73.34 (~P4(f6(a1,f5(a10,x24041)),f15(f6(x24042,f5(x24043,a1)),x24043))),
% 73.34/73.34 inference(scs_inference,[],[1366,139,1970,1247,1682,2214,1071,716,2038,1239,58,112,1073,611,2393,103,744,117,502,115,57,933,49,105,63,67,68,82,17,20,23,70,72,4,5,6,7,8,9,13,14,15,16,18,19,21,22,24,25,26,27,69,83,10,11,12,73,81,78,76,91,2,38,40,75,74,80,88,41,66,77])).
% 73.34/73.34 cnf(2405,plain,
% 73.34/73.34 (~P4(a1,x24051)),
% 73.34/73.34 inference(rename_variables,[],[57])).
% 73.34/73.34 cnf(2407,plain,
% 73.34/73.34 (~P4(f16(f6(f4(a1,x24071),f5(x24072,x24073)),x24072),x24074)),
% 73.34/73.34 inference(scs_inference,[],[1366,139,1970,1247,1682,2214,1071,716,2038,1239,58,112,1073,611,2393,103,744,117,502,115,57,2405,933,49,105,63,67,68,82,17,20,23,70,72,4,5,6,7,8,9,13,14,15,16,18,19,21,22,24,25,26,27,69,83,10,11,12,73,81,78,76,91,2,38,40,75,74,80,88,41,66,77,34])).
% 73.34/73.34 cnf(2408,plain,
% 73.34/73.34 (~P4(a10,f16(f6(f7(f19(a9,a10,a11)),f5(x24081,x24082)),x24081))),
% 73.34/73.34 inference(scs_inference,[],[1366,139,1970,1247,1682,2214,1071,716,2038,1239,58,112,1073,611,2393,103,744,101,117,502,115,57,2405,933,49,2389,105,63,67,68,82,17,20,23,70,72,4,5,6,7,8,9,13,14,15,16,18,19,21,22,24,25,26,27,69,83,10,11,12,73,81,78,76,91,2,38,40,75,74,80,88,41,66,77,34,35])).
% 73.34/73.34 cnf(2410,plain,
% 73.34/73.34 (~P8(f6(a1,f5(x24101,a10)),x24102,f15(f6(x24103,f5(x24104,a1)),x24104))),
% 73.34/73.34 inference(scs_inference,[],[1366,139,1970,1247,1682,2214,1071,716,2038,1239,58,112,1073,611,2393,103,744,101,117,502,115,57,2405,933,49,2389,105,63,67,68,82,17,20,23,70,72,4,5,6,7,8,9,13,14,15,16,18,19,21,22,24,25,26,27,69,83,10,11,12,73,81,78,76,91,2,38,40,75,74,80,88,41,66,77,34,35,85])).
% 73.34/73.34 cnf(2411,plain,
% 73.34/73.34 (~P8(a1,x24111,x24112)),
% 73.34/73.34 inference(rename_variables,[],[58])).
% 73.34/73.34 cnf(2413,plain,
% 73.34/73.34 (~P8(f6(a1,f5(a10,x24131)),f15(f6(x24132,f5(x24133,a1)),x24133),x24134)),
% 73.34/73.34 inference(scs_inference,[],[1366,139,1970,1247,1682,2214,1071,716,2038,1239,58,2411,112,1073,611,2393,103,744,101,117,502,115,57,2405,933,49,2389,105,63,67,68,82,17,20,23,70,72,4,5,6,7,8,9,13,14,15,16,18,19,21,22,24,25,26,27,69,83,10,11,12,73,81,78,76,91,2,38,40,75,74,80,88,41,66,77,34,35,85,86])).
% 73.34/73.34 cnf(2418,plain,
% 73.34/73.34 (~E(f8(f19(a9,a10,a11)),f13(f19(x24181,x24182,a3),x24183))),
% 73.34/73.34 inference(scs_inference,[],[54,152,1366,139,1970,1247,1682,2214,1071,716,2038,1239,431,58,2411,112,1073,611,2393,103,434,744,101,117,502,115,57,2405,933,49,2389,105,63,67,68,82,17,20,23,70,72,4,5,6,7,8,9,13,14,15,16,18,19,21,22,24,25,26,27,69,83,10,11,12,73,81,78,76,91,2,38,40,75,74,80,88,41,66,77,34,35,85,86,3,36])).
% 73.34/73.34 cnf(2420,plain,
% 73.34/73.34 (E(f19(a9,f4(a10,f14(a9)),x24201),f8(f19(a9,a10,x24201)))),
% 73.34/73.34 inference(scs_inference,[],[54,152,1366,597,139,1970,1247,1682,2214,1071,716,2038,1239,431,58,2411,112,212,1073,611,2393,103,434,744,101,117,502,115,57,2405,933,99,49,2389,105,63,67,68,82,17,20,23,70,72,4,5,6,7,8,9,13,14,15,16,18,19,21,22,24,25,26,27,69,83,10,11,12,73,81,78,76,91,2,38,40,75,74,80,88,41,66,77,34,35,85,86,3,36,33,90])).
% 73.34/73.34 cnf(2423,plain,
% 73.34/73.34 (P6(f4(f5(x24231,a1),f4(a1,x24232)),f4(f5(x24231,f4(a1,x24233)),f4(a1,x24234)))),
% 73.34/73.34 inference(scs_inference,[],[54,152,1366,597,139,1970,2315,1247,1682,2214,2386,1071,716,2038,1239,431,58,2411,112,212,1368,1073,611,2393,103,434,744,101,117,502,115,57,2405,933,99,49,2389,105,63,67,68,82,17,20,23,70,72,4,5,6,7,8,9,13,14,15,16,18,19,21,22,24,25,26,27,69,83,10,11,12,73,81,78,76,91,2,38,40,75,74,80,88,41,66,77,34,35,85,86,3,36,33,90,39,32])).
% 73.34/73.34 cnf(2424,plain,
% 73.34/73.34 (E(f4(f5(x24241,a1),f4(a1,x24242)),f4(f5(x24241,f4(a1,x24243)),f4(a1,x24244)))),
% 73.34/73.34 inference(rename_variables,[],[2214])).
% 73.34/73.34 cnf(2425,plain,
% 73.34/73.34 (P6(f4(x24251,f4(a1,x24252)),f4(x24251,f4(a1,x24253)))),
% 73.34/73.34 inference(rename_variables,[],[1368])).
% 73.34/73.34 cnf(2426,plain,
% 73.34/73.34 (P6(f4(f5(x24261,f4(a1,x24262)),f4(a1,x24263)),f4(f5(x24261,a1),f4(a1,x24264)))),
% 73.34/73.34 inference(scs_inference,[],[54,152,1366,597,139,1970,2315,1247,1682,2214,2386,2424,1071,716,2038,1239,431,58,2411,112,212,1368,2425,1073,611,2393,103,434,744,101,117,502,115,57,2405,933,99,49,2389,105,63,67,68,82,17,20,23,70,72,4,5,6,7,8,9,13,14,15,16,18,19,21,22,24,25,26,27,69,83,10,11,12,73,81,78,76,91,2,38,40,75,74,80,88,41,66,77,34,35,85,86,3,36,33,90,39,32,31])).
% 73.34/73.34 cnf(2447,plain,
% 73.34/73.34 (P8(f6(f6(f6(x24471,f5(a3,a3)),f5(x24472,x24473)),f5(x24474,x24475)),f15(f6(x24476,f5(x24477,a3)),x24477),a3)),
% 73.34/73.34 inference(scs_inference,[],[2423,2407,2408,2369,45,78,63,67,81,82,83])).
% 73.34/73.34 cnf(2451,plain,
% 73.34/73.34 (E(f7(f19(x24511,a10,x24512)),f14(x24511))),
% 73.34/73.34 inference(scs_inference,[],[2376,2423,2407,2408,2369,45,99,78,63,67,81,82,83,22,23,73])).
% 73.34/73.34 cnf(2453,plain,
% 73.34/73.34 (E(f15(x24531,f17(f19(x24532,a1,x24533),x24534)),f15(x24531,f19(x24532,a1,a3)))),
% 73.34/73.34 inference(scs_inference,[],[2376,2423,2407,2408,2369,45,99,78,63,67,81,82,83,22,23,73,16])).
% 73.34/73.34 cnf(2456,plain,
% 73.34/73.34 (E(f19(f17(f19(x24561,a1,x24562),x24563),x24564,x24565),f19(f19(x24561,a1,a3),x24564,x24565))),
% 73.34/73.34 inference(scs_inference,[],[2376,2423,2407,2408,2369,45,99,78,63,67,81,82,83,22,23,73,16,25,21,10])).
% 73.34/73.34 cnf(2459,plain,
% 73.34/73.34 (E(f17(f17(f19(x24591,a1,x24592),x24593),x24594),f17(f19(x24591,a1,a3),x24594))),
% 73.34/73.34 inference(scs_inference,[],[2376,2423,2407,2408,2369,1069,45,99,78,63,67,81,82,83,22,23,73,16,25,21,10,69,18])).
% 73.34/73.34 cnf(2462,plain,
% 73.34/73.34 (P4(f6(f6(f6(x24621,f5(f5(x24622,a1),x24623)),f5(x24624,x24625)),f5(x24626,x24627)),f5(x24622,f4(a1,x24628)))),
% 73.34/73.34 inference(scs_inference,[],[2376,2423,2407,2408,2347,2369,1069,45,99,78,63,67,81,82,83,22,23,73,16,25,21,10,69,18,76,72])).
% 73.34/73.34 cnf(2464,plain,
% 73.34/73.34 (E(f16(x24641,f17(f19(x24642,a1,x24643),x24644)),f16(x24641,f19(x24642,a1,a3)))),
% 73.34/73.34 inference(scs_inference,[],[2376,2423,2407,2408,2347,2369,1069,45,99,78,63,67,81,82,83,22,23,73,16,25,21,10,69,18,76,72,14])).
% 73.34/73.34 cnf(2466,plain,
% 73.34/73.34 (P6(f4(f5(x24661,a1),f4(a1,x24662)),f17(f4(f5(x24661,f4(a1,x24663)),f4(a1,x24664)),x24665))),
% 73.34/73.34 inference(scs_inference,[],[2376,2423,2407,2408,2347,2369,1069,45,99,78,63,67,81,82,83,22,23,73,16,25,21,10,69,18,76,72,14,13,68])).
% 73.34/73.34 cnf(2468,plain,
% 73.34/73.34 (P4(f6(x24681,f5(f17(f19(x24682,a1,x24683),x24684),x24685)),f19(x24682,a1,a3))),
% 73.34/73.34 inference(scs_inference,[],[2376,2423,2407,2408,2347,2369,1069,45,99,78,63,67,81,82,83,22,23,73,16,25,21,10,69,18,76,72,14,13,68,70])).
% 73.34/73.34 cnf(2471,plain,
% 73.34/73.34 (E(f19(x24711,f17(f19(x24712,a1,x24713),x24714),x24715),f19(x24711,f19(x24712,a1,a3),x24715))),
% 73.34/73.34 inference(scs_inference,[],[2376,2423,2407,2408,2347,2369,1069,45,99,78,63,67,81,82,83,22,23,73,16,25,21,10,69,18,76,72,14,13,68,70,27,11])).
% 73.34/73.34 cnf(2476,plain,
% 73.34/73.34 (E(f5(x24761,f17(f19(x24762,a1,x24763),x24764)),f5(x24761,f19(x24762,a1,a3)))),
% 73.34/73.34 inference(scs_inference,[],[2376,2423,2407,2408,2347,2369,1069,45,99,78,63,67,81,82,83,22,23,73,16,25,21,10,69,18,76,72,14,13,68,70,27,11,15,17,20,9,7])).
% 73.34/73.34 cnf(2480,plain,
% 73.34/73.34 (E(f12(f17(f19(x24801,a1,x24802),x24803),x24804),f12(f19(x24801,a1,a3),x24804))),
% 73.34/73.34 inference(scs_inference,[],[2376,2423,2407,2408,2347,2369,1069,45,99,78,63,67,81,82,83,22,23,73,16,25,21,10,69,18,76,72,14,13,68,70,27,11,15,17,20,9,7,24,5,12,26])).
% 73.34/73.34 cnf(2482,plain,
% 73.34/73.34 (E(f4(f17(f19(x24821,a1,x24822),x24823),x24824),f4(f19(x24821,a1,a3),x24824))),
% 73.34/73.34 inference(scs_inference,[],[2376,2423,2407,2408,2347,2369,1069,45,99,78,63,67,81,82,83,22,23,73,16,25,21,10,69,18,76,72,14,13,68,70,27,11,15,17,20,9,7,24,5,12,26,8,4])).
% 73.34/73.34 cnf(2484,plain,
% 73.34/73.34 (E(f5(f17(f19(x24841,a1,x24842),x24843),x24844),f5(f19(x24841,a1,a3),x24844))),
% 73.34/73.34 inference(scs_inference,[],[2376,2423,2407,2408,2347,2369,1069,45,99,78,63,67,81,82,83,22,23,73,16,25,21,10,69,18,76,72,14,13,68,70,27,11,15,17,20,9,7,24,5,12,26,8,4,19,6])).
% 73.34/73.34 cnf(2485,plain,
% 73.34/73.34 (~P7(f8(f19(x24851,f4(a1,x24852),x24853)))),
% 73.34/73.34 inference(scs_inference,[],[2376,2423,2407,2408,2347,2369,1069,45,99,44,78,63,67,81,82,83,22,23,73,16,25,21,10,69,18,76,72,14,13,68,70,27,11,15,17,20,9,7,24,5,12,26,8,4,19,6,91])).
% 73.34/73.34 cnf(2487,plain,
% 73.34/73.34 (~E(f13(f19(x24871,x24872,a3),x24873),f8(f19(a9,a10,a11)))),
% 73.34/73.34 inference(scs_inference,[],[2376,2418,2423,2407,2408,2347,2369,1069,45,99,44,78,63,67,81,82,83,22,23,73,16,25,21,10,69,18,76,72,14,13,68,70,27,11,15,17,20,9,7,24,5,12,26,8,4,19,6,91,2])).
% 73.34/73.34 cnf(2490,plain,
% 73.34/73.34 (~P8(f6(f4(a1,x24901),f5(x24902,a10)),x24903,f15(f6(x24904,f5(x24905,a1)),x24905))),
% 73.34/73.34 inference(scs_inference,[],[2376,129,2418,2423,2407,2410,2408,2347,2369,2374,1069,1670,45,99,44,78,63,67,81,82,83,22,23,73,16,25,21,10,69,18,76,72,14,13,68,70,27,11,15,17,20,9,7,24,5,12,26,8,4,19,6,91,2,37,41])).
% 73.34/73.34 cnf(2491,plain,
% 73.34/73.34 (E(f6(f4(a1,x24911),x24912),f6(a1,x24912))),
% 73.34/73.34 inference(rename_variables,[],[1670])).
% 73.34/73.34 cnf(2496,plain,
% 73.34/73.34 (~P5(f17(f19(x24961,a1,x24962),x24963),x24964)),
% 73.34/73.34 inference(scs_inference,[],[2340,2376,129,2418,2423,2407,219,2410,2408,2347,2369,2374,1069,1670,45,99,49,44,78,63,67,81,82,83,22,23,73,16,25,21,10,69,18,76,72,14,13,68,70,27,11,15,17,20,9,7,24,5,12,26,8,4,19,6,91,2,37,41,75,38,39])).
% 73.34/73.34 cnf(2501,plain,
% 73.34/73.34 (~P4(f6(f4(a1,x25011),f5(a10,x25012)),f15(f6(x25013,f5(x25014,a1)),x25014))),
% 73.34/73.34 inference(scs_inference,[],[2340,2376,129,2418,2423,2407,219,2410,2404,695,2408,2347,2369,2374,1069,1670,2491,45,99,49,44,78,63,67,81,82,83,22,23,73,16,25,21,10,69,18,76,72,14,13,68,70,27,11,15,17,20,9,7,24,5,12,26,8,4,19,6,91,2,37,41,75,38,39,77,34])).
% 73.34/73.34 cnf(2503,plain,
% 73.34/73.34 (~P8(f6(a1,f5(x25031,f8(f19(a9,a10,a11)))),x25032,f13(f19(x25033,x25034,a3),x25035))),
% 73.34/73.34 inference(scs_inference,[],[2340,2376,129,2418,2423,2407,219,2410,2404,695,2408,2347,2369,2374,1069,1670,2491,58,45,99,49,44,78,63,67,81,82,83,22,23,73,16,25,21,10,69,18,76,72,14,13,68,70,27,11,15,17,20,9,7,24,5,12,26,8,4,19,6,91,2,37,41,75,38,39,77,34,85])).
% 73.34/73.34 cnf(2504,plain,
% 73.34/73.34 (~P8(a1,x25041,x25042)),
% 73.34/73.34 inference(rename_variables,[],[58])).
% 73.34/73.34 cnf(2506,plain,
% 73.34/73.34 (~P8(f6(a1,f5(f8(f19(a9,a10,a11)),x25061)),f13(f19(x25062,x25063,a3),x25064),x25065)),
% 73.34/73.34 inference(scs_inference,[],[2340,2376,129,2418,2423,2407,219,2410,2404,695,2408,2347,2369,2374,1069,1670,2491,58,2504,45,99,49,44,78,63,67,81,82,83,22,23,73,16,25,21,10,69,18,76,72,14,13,68,70,27,11,15,17,20,9,7,24,5,12,26,8,4,19,6,91,2,37,41,75,38,39,77,34,85,86])).
% 73.34/73.34 cnf(2509,plain,
% 73.34/73.34 (~E(f15(f6(x25091,f5(x25092,a10)),x25092),f16(f6(f4(a1,x25093),f5(x25094,x25095)),x25094))),
% 73.34/73.34 inference(scs_inference,[],[2340,2376,129,2418,2423,2407,640,219,2410,2404,695,2408,2347,2369,2374,1069,1670,2491,58,2504,178,45,99,49,44,78,63,67,81,82,83,22,23,73,16,25,21,10,69,18,76,72,14,13,68,70,27,11,15,17,20,9,7,24,5,12,26,8,4,19,6,91,2,37,41,75,38,39,77,34,85,86,3])).
% 73.34/73.34 cnf(2511,plain,
% 73.34/73.34 (~E(f8(f19(a9,a10,a11)),f16(f6(f19(x25111,a1,a3),f5(x25112,x25113)),x25112))),
% 73.40/73.34 inference(scs_inference,[],[54,2340,2376,129,2418,2423,2407,433,640,219,2410,2404,695,2408,2347,2369,2374,1069,1670,2491,58,2504,178,45,99,49,44,78,63,67,81,82,83,22,23,73,16,25,21,10,69,18,76,72,14,13,68,70,27,11,15,17,20,9,7,24,5,12,26,8,4,19,6,91,2,37,41,75,38,39,77,34,85,86,3,36])).
% 73.40/73.34 cnf(2512,plain,
% 73.40/73.34 (P3(f19(x25121,f6(a1,f5(f12(x25122,a10),f12(x25122,a1))),x25123))),
% 73.40/73.34 inference(scs_inference,[],[54,2340,2376,129,2418,2423,2407,433,640,219,2410,2404,695,2408,2347,2369,2374,1069,1026,1670,2491,58,2504,178,52,45,99,49,44,78,63,67,81,82,83,22,23,73,16,25,21,10,69,18,76,72,14,13,68,70,27,11,15,17,20,9,7,24,5,12,26,8,4,19,6,91,2,37,41,75,38,39,77,34,85,86,3,36,95])).
% 73.40/73.34 cnf(2519,plain,
% 73.40/73.34 (E(f6(f4(x25191,x25192),f5(x25193,x25192)),f4(f6(x25191,f5(x25193,x25192)),x25192))),
% 73.40/73.34 inference(scs_inference,[],[46,78])).
% 73.40/73.34 cnf(2564,plain,
% 73.40/73.34 (~P9(f7(f19(a9,a10,x25641)),f16(f6(f15(a10,f14(a9)),f5(x25642,x25643)),x25642))),
% 73.40/73.34 inference(scs_inference,[],[2426,170,2501,231,2468,2447,962,1697,2018,2451,46,78,63,82,22,83,68,76,67,72,11,13,69,27,17,70,18,10,14,19,23,25,16,5,6,9,21,24,4,15,12,8,20,7,26,2,37])).
% 73.40/73.34 cnf(2566,plain,
% 73.40/73.34 (P8(f6(x25661,f5(f4(a1,x25662),f4(a1,x25662))),f4(a1,x25663),f4(a1,x25663))),
% 73.40/73.34 inference(scs_inference,[],[2426,170,2501,231,2468,2447,962,1697,2018,157,2451,46,78,63,82,22,83,68,76,67,72,11,13,69,27,17,70,18,10,14,19,23,25,16,5,6,9,21,24,4,15,12,8,20,7,26,2,37,75])).
% 73.40/73.34 cnf(2568,plain,
% 73.40/73.34 (~P8(f16(f6(f4(a1,x25681),f5(f19(x25682,a1,a3),x25683)),f17(f19(x25682,a1,x25684),x25685)),x25686,x25687)),
% 73.40/73.34 inference(scs_inference,[],[2426,2400,170,2464,2501,231,2468,2447,962,1697,2018,157,2451,46,78,63,82,22,83,68,76,67,72,11,13,69,27,17,70,18,10,14,19,23,25,16,5,6,9,21,24,4,15,12,8,20,7,26,2,37,75,41])).
% 73.40/73.34 cnf(2569,plain,
% 73.40/73.34 (E(f16(x25691,f17(f19(x25692,a1,x25693),x25694)),f16(x25691,f19(x25692,a1,a3)))),
% 73.40/73.34 inference(rename_variables,[],[2464])).
% 73.40/73.34 cnf(2570,plain,
% 73.40/73.34 (~P8(f16(f6(f4(a1,x25701),f5(x25702,x25703)),x25702),x25704,x25705)),
% 73.40/73.34 inference(rename_variables,[],[2400])).
% 73.40/73.34 cnf(2574,plain,
% 73.40/73.34 (~P9(f8(f19(f19(x25741,a1,a3),a1,x25742)),f19(f17(f19(x25741,a1,x25743),x25744),a1,a3))),
% 73.40/73.34 inference(scs_inference,[],[2496,2426,2400,170,2456,2459,2464,2501,231,2468,2447,571,962,1697,2018,157,2451,46,78,63,82,22,83,68,76,67,72,11,13,69,27,17,70,18,10,14,19,23,25,16,5,6,9,21,24,4,15,12,8,20,7,26,2,37,75,41,39,38])).
% 73.40/73.34 cnf(2575,plain,
% 73.40/73.34 (E(f19(f17(f19(x25751,a1,x25752),x25753),x25754,x25755),f19(f19(x25751,a1,a3),x25754,x25755))),
% 73.40/73.34 inference(rename_variables,[],[2456])).
% 73.40/73.34 cnf(2578,plain,
% 73.40/73.34 (~P4(f16(f6(f4(a1,x25781),f5(x25782,x25783)),x25782),x25784)),
% 73.40/73.34 inference(rename_variables,[],[2407])).
% 73.40/73.34 cnf(2580,plain,
% 73.40/73.34 (~P8(f6(a1,f5(a10,x25801)),f15(f6(x25802,f5(f19(x25803,a1,a3),a1)),f17(f19(x25803,a1,x25804),x25805)),x25806)),
% 73.40/73.34 inference(scs_inference,[],[2496,2426,2400,170,2456,2453,2459,2464,2501,2413,231,2468,2447,571,962,1697,2018,157,2451,2407,46,78,63,82,22,83,68,76,67,72,11,13,69,27,17,70,18,10,14,19,23,25,16,5,6,9,21,24,4,15,12,8,20,7,26,2,37,75,41,39,38,77,42])).
% 73.40/73.34 cnf(2582,plain,
% 73.40/73.34 (E(f15(x25821,f17(f19(x25822,a1,x25823),x25824)),f15(x25821,f19(x25822,a1,a3)))),
% 73.40/73.34 inference(rename_variables,[],[2453])).
% 73.40/73.34 cnf(2585,plain,
% 73.40/73.34 (E(f15(x25851,f17(f19(x25852,a1,x25853),x25854)),f15(x25851,f19(x25852,a1,a3)))),
% 73.40/73.34 inference(rename_variables,[],[2453])).
% 73.40/73.34 cnf(2586,plain,
% 73.40/73.34 (~P4(f16(f6(f4(a1,x25861),f5(f19(x25862,a1,a3),x25863)),f17(f19(x25862,a1,x25864),x25865)),x25866)),
% 73.40/73.34 inference(scs_inference,[],[2496,2426,2400,170,2456,2453,2582,2459,2464,2569,2490,2501,2413,231,2468,2447,571,962,1697,2018,157,2451,2407,2578,46,78,63,82,22,83,68,76,67,72,11,13,69,27,17,70,18,10,14,19,23,25,16,5,6,9,21,24,4,15,12,8,20,7,26,2,37,75,41,39,38,77,42,43,34])).
% 73.40/73.34 cnf(2589,plain,
% 73.40/73.34 (~P4(f6(f4(a1,x25891),f5(a10,x25892)),f15(f6(x25893,f5(f19(x25894,a1,a3),a1)),f17(f19(x25894,a1,x25895),x25896)))),
% 73.40/73.34 inference(scs_inference,[],[2496,2426,2400,170,2456,2453,2582,2585,2459,2464,2569,2490,2501,2413,231,2468,2447,571,962,1697,2018,157,2451,2407,2578,46,78,63,82,22,83,68,76,67,72,11,13,69,27,17,70,18,10,14,19,23,25,16,5,6,9,21,24,4,15,12,8,20,7,26,2,37,75,41,39,38,77,42,43,34,35])).
% 73.40/73.34 cnf(2593,plain,
% 73.40/73.34 (~P8(f16(f6(f4(a1,x25931),f5(x25932,x25933)),x25932),x25934,x25935)),
% 73.40/73.34 inference(rename_variables,[],[2400])).
% 73.40/73.34 cnf(2601,plain,
% 73.40/73.34 (~E(f8(f19(a9,a10,a11)),f8(f19(x26011,f4(a1,x26012),x26013)))),
% 73.40/73.34 inference(scs_inference,[],[54,2496,2426,2400,2570,2593,2485,170,2456,2575,2471,2453,2582,2585,2459,2464,2569,2490,2501,2413,231,2468,2447,571,962,1697,2018,157,2451,2407,2578,46,78,63,82,22,83,68,76,67,72,11,13,69,27,17,70,18,10,14,19,23,25,16,5,6,9,21,24,4,15,12,8,20,7,26,2,37,75,41,39,38,77,42,43,34,35,85,86,3,36])).
% 73.40/73.34 cnf(2610,plain,
% 73.40/73.34 (P8(f6(f6(x26101,f5(f4(a1,x26102),f4(a1,x26102))),f5(x26103,x26104)),f4(a1,x26105),f4(a1,x26105))),
% 73.40/73.34 inference(scs_inference,[],[2566,1972,1329,63,76,83])).
% 73.40/73.34 cnf(2623,plain,
% 73.40/73.34 (P6(f12(x26231,a10),f17(f8(f12(x26231,a1)),f7(f12(x26231,a1))))),
% 73.40/73.34 inference(scs_inference,[],[2566,1972,2462,1017,1329,2032,2404,63,76,83,68,82,22,72,67,70,69])).
% 73.40/73.34 cnf(2640,plain,
% 73.40/73.34 (E(f5(f5(a1,f4(a1,x26401)),x26402),f5(f5(f4(a1,x26403),f4(a1,x26404)),x26402))),
% 73.40/73.34 inference(scs_inference,[],[2566,1972,2462,1017,1329,2032,2404,63,76,83,68,82,22,72,67,70,69,5,19,16,23,10,9,18,13,27,11,14,12,17,24,15,6])).
% 73.40/73.34 cnf(2645,plain,
% 73.40/73.34 (E(f5(x26451,f5(a1,f4(a1,x26452))),f5(x26451,f5(f4(a1,x26453),f4(a1,x26454))))),
% 73.40/73.34 inference(scs_inference,[],[2566,1972,2462,1017,1329,2032,2404,63,76,83,68,82,22,72,67,70,69,5,19,16,23,10,9,18,13,27,11,14,12,17,24,15,6,25,8,26,21,7])).
% 73.40/73.34 cnf(2649,plain,
% 73.40/73.34 (~P9(f12(f17(f19(x26491,a1,x26492),x26493),a1),f12(f19(x26491,a1,a3),a10))),
% 73.40/73.34 inference(scs_inference,[],[2566,2480,646,1972,2462,1030,1017,1329,2032,2404,63,76,83,68,82,22,72,67,70,69,5,19,16,23,10,9,18,13,27,11,14,12,17,24,15,6,25,8,26,21,7,4,20,2,37])).
% 73.40/73.34 cnf(2650,plain,
% 73.40/73.34 (~P9(f12(x26501,a1),f12(x26501,a10))),
% 73.40/73.34 inference(rename_variables,[],[1030])).
% 73.40/73.34 cnf(2651,plain,
% 73.40/73.34 (E(f12(f17(f19(x26511,a1,x26512),x26513),x26514),f12(f19(x26511,a1,a3),x26514))),
% 73.40/73.34 inference(rename_variables,[],[2480])).
% 73.40/73.34 cnf(2656,plain,
% 73.40/73.34 (~P9(f12(f19(x26561,a1,a3),a1),f12(f17(f19(x26561,a1,x26562),x26563),a10))),
% 73.40/73.34 inference(scs_inference,[],[2566,2480,2651,646,1972,2462,2503,1030,2650,1017,1329,2032,2404,2142,1670,63,76,83,68,82,22,72,67,70,69,5,19,16,23,10,9,18,13,27,11,14,12,17,24,15,6,25,8,26,21,7,4,20,2,37,41,75,38])).
% 73.40/73.34 cnf(2659,plain,
% 73.40/73.34 (~P4(f6(a10,f5(f14(a9),x26591)),f7(f19(a9,a10,a11)))),
% 73.40/73.34 inference(scs_inference,[],[2566,2480,2651,646,1972,2462,2503,1030,2650,1017,1329,2032,2404,2142,141,101,1670,63,76,83,68,82,22,72,67,70,69,5,19,16,23,10,9,18,13,27,11,14,12,17,24,15,6,25,8,26,21,7,4,20,2,37,41,75,38,77])).
% 73.40/73.34 cnf(2664,plain,
% 73.40/73.34 (~P8(f6(a1,f5(x26641,f13(f19(x26642,x26643,a3),x26644))),x26645,f8(f19(a9,a10,a11)))),
% 73.40/73.34 inference(scs_inference,[],[2487,2566,2480,2651,646,1972,2462,2503,2589,1030,2650,1017,1329,2032,2404,2142,141,101,1670,1669,58,63,76,83,68,82,22,72,67,70,69,5,19,16,23,10,9,18,13,27,11,14,12,17,24,15,6,25,8,26,21,7,4,20,2,37,41,75,38,77,34,85])).
% 73.40/73.34 cnf(2665,plain,
% 73.40/73.34 (~P8(a1,x26651,x26652)),
% 73.40/73.34 inference(rename_variables,[],[58])).
% 73.40/73.34 cnf(2667,plain,
% 73.40/73.34 (~P8(f6(a1,f5(f13(f19(x26671,x26672,a3),x26673),x26674)),f8(f19(a9,a10,a11)),x26675)),
% 73.40/73.34 inference(scs_inference,[],[2487,2566,2480,2651,646,1972,2462,2503,2589,1030,2650,1017,1329,2032,2404,2142,141,101,1670,1669,58,2665,63,76,83,68,82,22,72,67,70,69,5,19,16,23,10,9,18,13,27,11,14,12,17,24,15,6,25,8,26,21,7,4,20,2,37,41,75,38,77,34,85,86])).
% 73.40/73.34 cnf(2672,plain,
% 73.40/73.34 (~E(f8(f19(a9,a10,a11)),f17(f19(x26721,a10,x26722),f7(f19(a9,a10,a11))))),
% 73.40/73.34 inference(scs_inference,[],[54,2487,2566,654,2480,2651,646,1972,1323,2462,2503,2589,1030,2650,1017,1329,2032,2404,2142,141,101,1670,1669,58,2665,178,63,76,83,68,82,22,72,67,70,69,5,19,16,23,10,9,18,13,27,11,14,12,17,24,15,6,25,8,26,21,7,4,20,2,37,41,75,38,77,34,85,86,3,36])).
% 73.40/73.34 cnf(2677,plain,
% 73.40/73.34 (P8(f6(f6(f6(x26771,f5(f4(a1,x26772),f4(a1,x26772))),f5(x26773,x26774)),f5(x26775,x26776)),f4(a1,x26777),f4(a1,x26777))),
% 73.40/73.34 inference(scs_inference,[],[2610,2623,1244,76,63,83])).
% 73.40/73.34 cnf(2679,plain,
% 73.40/73.34 (P4(f6(f6(x26791,f5(a1,x26792)),f5(x26793,x26794)),f4(f4(a1,x26795),x26796))),
% 73.40/73.34 inference(scs_inference,[],[2610,2623,1244,76,63,83,72])).
% 73.40/73.34 cnf(2690,plain,
% 73.40/73.34 (P6(f12(x26901,a1),f17(f8(f12(x26901,a10)),f7(f12(x26901,a10))))),
% 73.40/73.34 inference(scs_inference,[],[2610,2659,2623,1020,1244,1968,1625,76,63,83,72,68,67,82,22,70,69])).
% 73.40/73.34 cnf(2695,plain,
% 73.40/73.34 (E(f6(x26951,f5(f8(f19(x26952,a1,x26953)),f4(a1,x26954))),f6(x26951,f5(f19(x26952,a1,a3),f4(a1,x26955))))),
% 73.40/73.34 inference(scs_inference,[],[2610,2659,2623,1020,1244,1968,1625,76,63,83,72,68,67,82,22,70,69,19,18,12,9])).
% 73.40/73.34 cnf(2702,plain,
% 73.40/73.34 (E(f7(f5(f8(f19(x27021,a1,x27022)),f4(a1,x27023))),f7(f5(f19(x27021,a1,a3),f4(a1,x27024))))),
% 73.40/73.34 inference(scs_inference,[],[2610,2659,2623,1020,1244,1968,1625,76,63,83,72,68,67,82,22,70,69,19,18,12,9,16,27,5,13,10,8,23])).
% 73.40/73.34 cnf(2704,plain,
% 73.40/73.34 (E(f5(f5(f8(f19(x27041,a1,x27042)),f4(a1,x27043)),x27044),f5(f5(f19(x27041,a1,a3),f4(a1,x27045)),x27044))),
% 73.40/73.34 inference(scs_inference,[],[2610,2659,2623,1020,1244,1968,1625,76,63,83,72,68,67,82,22,70,69,19,18,12,9,16,27,5,13,10,8,23,25,6])).
% 73.40/73.34 cnf(2709,plain,
% 73.40/73.34 (E(f14(f5(f8(f19(x27091,a1,x27092)),f4(a1,x27093))),f14(f5(f19(x27091,a1,a3),f4(a1,x27094))))),
% 73.40/73.34 inference(scs_inference,[],[2610,2659,2623,1020,1244,1968,1625,76,63,83,72,68,67,82,22,70,69,19,18,12,9,16,27,5,13,10,8,23,25,6,14,15,24,11,17])).
% 73.40/73.34 cnf(2714,plain,
% 73.40/73.34 (E(f8(f5(f8(f19(x27141,a1,x27142)),f4(a1,x27143))),f8(f5(f19(x27141,a1,a3),f4(a1,x27144))))),
% 73.40/73.34 inference(scs_inference,[],[2610,2659,2623,1020,1244,1968,1625,76,63,83,72,68,67,82,22,70,69,19,18,12,9,16,27,5,13,10,8,23,25,6,14,15,24,11,17,4,21,7,26,20])).
% 73.40/73.34 cnf(2716,plain,
% 73.40/73.34 (~P9(f12(f17(f19(x27161,a1,x27162),x27163),a1),f12(f17(f19(x27161,a1,x27164),x27165),a10))),
% 73.40/73.34 inference(scs_inference,[],[2610,2659,956,2623,2656,1020,1244,1968,1625,2480,76,63,83,72,68,67,82,22,70,69,19,18,12,9,16,27,5,13,10,8,23,25,6,14,15,24,11,17,4,21,7,26,20,2,37])).
% 73.40/73.34 cnf(2718,plain,
% 73.40/73.34 (P8(f6(x27181,f5(f5(a1,a1),f5(a1,a1))),f5(f4(a1,x27182),f4(a1,x27183)),f5(f4(a1,x27182),f4(a1,x27183)))),
% 73.40/73.34 inference(scs_inference,[],[2610,2659,956,2623,2656,1020,1244,1968,1625,2480,1434,76,63,83,72,68,67,82,22,70,69,19,18,12,9,16,27,5,13,10,8,23,25,6,14,15,24,11,17,4,21,7,26,20,2,37,75])).
% 73.40/73.34 cnf(2725,plain,
% 73.40/73.34 (~P9(f5(f4(a1,x27251),f19(x27252,a1,a3)),f5(a1,f17(f19(x27252,a1,x27253),x27254)))),
% 73.40/73.34 inference(scs_inference,[],[2610,2476,2659,956,2623,2656,2586,2506,1456,1020,1244,1968,1625,2480,1434,112,1670,76,63,83,72,68,67,82,22,70,69,19,18,12,9,16,27,5,13,10,8,23,25,6,14,15,24,11,17,4,21,7,26,20,2,37,75,41,77,38])).
% 73.40/73.34 cnf(2728,plain,
% 73.40/73.34 (~P4(f4(f4(a1,x27281),x27282),x27283)),
% 73.40/73.34 inference(scs_inference,[],[2610,2476,2659,956,2623,2656,2586,2506,1456,1020,1244,1968,1625,2480,1434,112,1670,57,933,76,63,83,72,68,67,82,22,70,69,19,18,12,9,16,27,5,13,10,8,23,25,6,14,15,24,11,17,4,21,7,26,20,2,37,75,41,77,38,34])).
% 73.40/73.34 cnf(2729,plain,
% 73.40/73.34 (~P8(f6(f16(f6(f4(a1,x27291),f5(f19(x27292,a1,a3),x27293)),f17(f19(x27292,a1,x27294),x27295)),f5(x27296,a10)),x27297,f4(a1,x27298))),
% 73.40/73.34 inference(scs_inference,[],[2610,2476,2659,956,2623,2656,2568,2586,2506,1456,1020,1244,1968,1625,2480,1434,112,1670,57,933,76,63,83,72,68,67,82,22,70,69,19,18,12,9,16,27,5,13,10,8,23,25,6,14,15,24,11,17,4,21,7,26,20,2,37,75,41,77,38,34,85])).
% 73.40/73.34 cnf(2730,plain,
% 73.40/73.34 (~P8(f16(f6(f4(a1,x27301),f5(f19(x27302,a1,a3),x27303)),f17(f19(x27302,a1,x27304),x27305)),x27306,x27307)),
% 73.40/73.34 inference(rename_variables,[],[2568])).
% 73.40/73.34 cnf(2732,plain,
% 73.40/73.34 (~P8(f6(f16(f6(f4(a1,x27321),f5(f19(x27322,a1,a3),x27323)),f17(f19(x27322,a1,x27324),x27325)),f5(a10,x27326)),f4(a1,x27327),x27328)),
% 73.40/73.34 inference(scs_inference,[],[2610,2476,2659,956,2623,2656,2568,2730,2586,2506,1456,1020,1244,1968,1625,2480,1434,112,1670,57,933,76,63,83,72,68,67,82,22,70,69,19,18,12,9,16,27,5,13,10,8,23,25,6,14,15,24,11,17,4,21,7,26,20,2,37,75,41,77,38,34,85,86])).
% 73.40/73.34 cnf(2750,plain,
% 73.40/73.34 (P4(f6(f6(f6(x27501,f5(a1,x27502)),f5(x27503,x27504)),f5(x27505,x27506)),f4(f4(a1,x27507),x27508))),
% 73.40/73.34 inference(scs_inference,[],[2679,2690,2677,63,76,83,72])).
% 73.40/73.34 cnf(2769,plain,
% 73.40/73.34 (E(f6(x27691,f5(f19(x27692,a1,a3),f4(a1,x27693))),f6(x27691,f5(f8(f19(x27692,a1,x27694)),f4(a1,x27695))))),
% 73.40/73.34 inference(scs_inference,[],[2728,2679,2690,2677,812,1978,1509,63,76,83,72,82,67,68,22,70,69,18,5,12,27,25,19,9])).
% 73.40/73.34 cnf(2774,plain,
% 73.40/73.34 (E(f14(f5(f19(x27741,a1,a3),f4(a1,x27742))),f14(f5(f8(f19(x27741,a1,x27743)),f4(a1,x27744))))),
% 73.40/73.34 inference(scs_inference,[],[2728,2679,2690,2677,812,1978,1509,63,76,83,72,82,67,68,22,70,69,18,5,12,27,25,19,9,13,16,10,11,17])).
% 73.40/73.34 cnf(2778,plain,
% 73.40/73.34 (E(f7(f5(f19(x27781,a1,a3),f4(a1,x27782))),f7(f5(f8(f19(x27781,a1,x27783)),f4(a1,x27784))))),
% 73.40/73.34 inference(scs_inference,[],[2728,2679,2690,2677,812,1978,1509,63,76,83,72,82,67,68,22,70,69,18,5,12,27,25,19,9,13,16,10,11,17,24,15,14,23])).
% 73.40/73.34 cnf(2779,plain,
% 73.40/73.34 (E(f5(f5(f19(x27791,a1,a3),f4(a1,x27792)),x27793),f5(f5(f8(f19(x27791,a1,x27794)),f4(a1,x27795)),x27793))),
% 73.40/73.34 inference(scs_inference,[],[2728,2679,2690,2677,812,1978,1509,63,76,83,72,82,67,68,22,70,69,18,5,12,27,25,19,9,13,16,10,11,17,24,15,14,23,6])).
% 73.40/73.34 cnf(2785,plain,
% 73.40/73.34 (E(f8(f5(f19(x27851,a1,a3),f4(a1,x27852))),f8(f5(f8(f19(x27851,a1,x27853)),f4(a1,x27854))))),
% 73.40/73.34 inference(scs_inference,[],[2728,2679,2690,2677,812,1978,1509,63,76,83,72,82,67,68,22,70,69,18,5,12,27,25,19,9,13,16,10,11,17,24,15,14,23,6,8,21,26,4,7,20])).
% 73.40/73.34 cnf(2790,plain,
% 73.40/73.34 (~P9(f12(f17(f19(x27901,a1,x27902),x27903),a10),f12(f19(x27901,a1,a3),a10))),
% 73.40/73.34 inference(scs_inference,[],[2728,2679,2649,648,2690,2677,812,682,1978,1509,684,753,63,76,83,72,82,67,68,22,70,69,18,5,12,27,25,19,9,13,16,10,11,17,24,15,14,23,6,8,21,26,4,7,20,2,66,37])).
% 73.40/73.34 cnf(2800,plain,
% 73.40/73.34 (~P9(f5(f4(a1,x28001),f19(x28002,a1,a3)),f5(f4(a1,x28003),f17(f19(x28002,a1,x28004),x28005)))),
% 73.40/73.34 inference(scs_inference,[],[2728,2679,2649,648,2690,2725,2677,2729,2664,812,682,1978,1509,2659,684,2451,141,1670,993,753,109,63,76,83,72,82,67,68,22,70,69,18,5,12,27,25,19,9,13,16,10,11,17,24,15,14,23,6,8,21,26,4,7,20,2,66,37,75,77,43,41,38])).
% 73.40/73.34 cnf(2804,plain,
% 73.40/73.34 (P6(f4(f19(x28041,a1,a3),a1),f4(f17(f19(x28041,a1,x28042),x28043),f4(a1,x28044)))),
% 73.40/73.34 inference(scs_inference,[],[2728,2679,2482,2649,648,2690,2725,2677,2729,2664,812,682,1978,1509,2659,1353,684,2451,141,1670,993,753,109,49,63,76,83,72,82,67,68,22,70,69,18,5,12,27,25,19,9,13,16,10,11,17,24,15,14,23,6,8,21,26,4,7,20,2,66,37,75,77,43,41,38,34,31])).
% 73.40/73.34 cnf(2805,plain,
% 73.40/73.34 (E(f4(f17(f19(x28051,a1,x28052),x28053),x28054),f4(f19(x28051,a1,a3),x28054))),
% 73.40/73.34 inference(rename_variables,[],[2482])).
% 73.40/73.34 cnf(2806,plain,
% 73.40/73.34 (P6(f4(x28061,a1),f4(x28061,f4(a1,x28062)))),
% 73.40/73.34 inference(rename_variables,[],[1353])).
% 73.40/73.34 cnf(2807,plain,
% 73.40/73.34 (P6(f4(f17(f19(x28071,a1,x28072),x28073),a1),f4(f19(x28071,a1,a3),f4(a1,x28074)))),
% 73.40/73.34 inference(scs_inference,[],[2728,2679,2482,2805,2649,648,2690,2725,2677,2729,2664,812,682,1978,1509,2659,1353,2806,684,2451,141,1670,993,753,109,49,63,76,83,72,82,67,68,22,70,69,18,5,12,27,25,19,9,13,16,10,11,17,24,15,14,23,6,8,21,26,4,7,20,2,66,37,75,77,43,41,38,34,31,32])).
% 73.40/73.34 cnf(2808,plain,
% 73.40/73.34 (E(f4(f17(f19(x28081,a1,x28082),x28083),x28084),f4(f19(x28081,a1,a3),x28084))),
% 73.40/73.34 inference(rename_variables,[],[2482])).
% 73.40/73.34 cnf(2810,plain,
% 73.40/73.34 (~E(f15(f6(x28101,f5(x28102,a10)),x28102),f4(f4(a1,x28103),x28104))),
% 73.40/73.34 inference(scs_inference,[],[2728,2679,2482,2805,2649,648,2690,2725,2677,2729,2664,812,682,1978,1509,944,2659,1353,2806,684,2451,141,1670,178,993,753,109,49,63,76,83,72,82,67,68,22,70,69,18,5,12,27,25,19,9,13,16,10,11,17,24,15,14,23,6,8,21,26,4,7,20,2,66,37,75,77,43,41,38,34,31,32,3])).
% 73.40/73.34 cnf(2812,plain,
% 73.40/73.34 (~E(f8(f19(a9,a10,a11)),f16(f6(f8(f19(x28121,a1,x28122)),f5(x28123,x28124)),x28123))),
% 73.40/73.34 inference(scs_inference,[],[54,2728,2679,2482,2805,2649,648,2690,2725,2677,2729,2664,812,682,1978,1509,944,2659,110,1353,2806,684,2451,141,1670,178,993,753,109,49,63,76,83,72,82,67,68,22,70,69,18,5,12,27,25,19,9,13,16,10,11,17,24,15,14,23,6,8,21,26,4,7,20,2,66,37,75,77,43,41,38,34,31,32,3,36])).
% 73.40/73.34 cnf(2816,plain,
% 73.40/73.34 (P1(f16(f6(f5(f17(f19(x28161,a1,x28162),x28163),f4(a1,x28164)),f5(x28165,x28166)),x28165),f5(f19(x28161,a1,a3),a1))),
% 73.40/73.34 inference(scs_inference,[],[54,2728,2679,2482,2805,2808,2484,2649,648,2690,2725,2677,2729,2664,1974,812,682,1978,1509,944,2659,110,1353,2806,684,2451,1360,141,1670,178,993,753,109,49,63,76,83,72,82,67,68,22,70,69,18,5,12,27,25,19,9,13,16,10,11,17,24,15,14,23,6,8,21,26,4,7,20,2,66,37,75,77,43,41,38,34,31,32,3,36,28,29])).
% 73.40/73.34 cnf(2821,plain,
% 73.40/73.34 (P3(f19(x28211,f6(f6(a1,f5(f12(x28212,a10),f12(x28212,a1))),f5(x28213,a2)),x28214))),
% 73.40/73.34 inference(scs_inference,[],[54,2728,2679,2482,2805,2808,2484,2649,648,2690,2725,2677,2512,2729,2664,1974,812,682,1978,1509,944,2659,110,1353,2806,684,2451,1360,141,103,1670,178,45,993,753,109,49,63,76,83,72,82,67,68,22,70,69,18,5,12,27,25,19,9,13,16,10,11,17,24,15,14,23,6,8,21,26,4,7,20,2,66,37,75,77,43,41,38,34,31,32,3,36,28,29,74,95])).
% 73.40/73.34 cnf(2830,plain,
% 73.40/73.34 (P8(f6(f6(x28301,f5(f5(a1,a1),f5(a1,a1))),f5(x28302,x28303)),f5(f4(a1,x28304),f4(a1,x28305)),f5(f4(a1,x28304),f4(a1,x28305)))),
% 73.40/73.34 inference(scs_inference,[],[2804,2750,2718,76,63,83])).
% 73.40/73.34 cnf(2834,plain,
% 73.40/73.34 (P4(f6(f6(f6(f6(x28341,f5(a1,x28342)),f5(x28343,x28344)),f5(x28345,x28346)),f5(x28347,x28348)),f4(f4(a1,x28349),x283410))),
% 73.40/73.34 inference(scs_inference,[],[2804,2750,2718,76,63,83,68,72])).
% 73.40/73.34 cnf(2853,plain,
% 73.40/73.34 (E(f5(f5(f4(a1,x28531),x28532),x28533),f5(f5(f4(a1,x28534),x28532),x28533))),
% 73.40/73.34 inference(scs_inference,[],[2804,2750,2718,628,1465,76,63,83,68,72,67,69,70,22,5,19,12,18,17,9,25,27,16,13,6])).
% 73.40/73.34 cnf(2871,plain,
% 73.40/73.34 (~P9(f5(f4(a1,x28711),f17(f19(x28712,a1,x28713),x28714)),f5(f4(a1,x28715),f17(f19(x28712,a1,x28716),x28717)))),
% 73.40/73.34 inference(scs_inference,[],[2804,2750,2810,2800,2718,2732,628,1465,2476,1441,109,76,63,83,68,72,67,69,70,22,5,19,12,18,17,9,25,27,16,13,6,8,23,11,14,15,10,24,26,7,21,4,20,2,42,75,37])).
% 73.40/73.34 cnf(2873,plain,
% 73.40/73.34 (~P4(f6(f4(f4(a1,x28731),x28732),f5(a10,x28733)),f16(f6(f4(a1,x28734),f5(x28735,x28736)),x28735))),
% 73.40/73.34 inference(scs_inference,[],[2804,2750,2810,2800,2718,2732,628,1465,2728,640,2476,1441,109,76,63,83,68,72,67,69,70,22,5,19,12,18,17,9,25,27,16,13,6,8,23,11,14,15,10,24,26,7,21,4,20,2,42,75,37,77])).
% 73.40/73.34 cnf(2874,plain,
% 73.40/73.34 (~P4(f4(f4(a1,x28741),x28742),x28743)),
% 73.40/73.34 inference(rename_variables,[],[2728])).
% 73.40/73.34 cnf(2876,plain,
% 73.40/73.34 (P8(f4(f6(x28761,f5(f5(a1,a1),f5(a1,a1))),f5(a1,a1)),f5(f4(a1,x28762),f4(a1,x28763)),f5(f4(a1,x28762),f4(a1,x28763)))),
% 73.40/73.34 inference(scs_inference,[],[2804,2750,2810,2800,2718,2732,2519,628,1465,2728,640,2476,1441,109,76,63,83,68,72,67,69,70,22,5,19,12,18,17,9,25,27,16,13,6,8,23,11,14,15,10,24,26,7,21,4,20,2,42,75,37,77,41])).
% 73.40/73.34 cnf(2879,plain,
% 73.40/73.34 (~P9(f5(f5(f8(f19(x28791,a1,x28792)),f4(a1,x28793)),f4(a1,x28794)),f5(f5(f19(x28791,a1,a3),f4(a1,x28795)),a1))),
% 73.40/73.34 inference(scs_inference,[],[2804,2750,2810,2800,2718,2732,2779,1965,2519,628,1465,2728,640,2476,1441,109,76,63,83,68,72,67,69,70,22,5,19,12,18,17,9,25,27,16,13,6,8,23,11,14,15,10,24,26,7,21,4,20,2,42,75,37,77,41,38])).
% 73.40/73.34 cnf(2882,plain,
% 73.40/73.34 (~P4(f4(a1,x28821),x28822)),
% 73.40/73.34 inference(scs_inference,[],[2804,2750,2810,2800,2718,2732,2779,1965,2519,628,1465,2728,2874,640,2476,1441,1236,109,76,63,83,68,72,67,69,70,22,5,19,12,18,17,9,25,27,16,13,6,8,23,11,14,15,10,24,26,7,21,4,20,2,42,75,37,77,41,38,34])).
% 73.40/73.34 cnf(2886,plain,
% 73.40/73.34 (E(f17(f19(x28861,f4(a1,x28862),x28863),x28864),f19(x28861,f4(a1,x28862),a3))),
% 73.40/73.34 inference(scs_inference,[],[2804,2750,2810,2800,2718,2732,2779,2774,1965,2519,2709,628,1465,2728,2874,640,2476,1441,1236,109,76,63,83,68,72,67,69,70,22,5,19,12,18,17,9,25,27,16,13,6,8,23,11,14,15,10,24,26,7,21,4,20,2,42,75,37,77,41,38,34,3,81])).
% 73.40/73.34 cnf(2888,plain,
% 73.40/73.34 (~P5(f19(x28881,f6(f4(f4(a1,x28882),x28883),f5(a10,x28884)),x28885),f16(f6(f4(a1,x28886),f5(x28887,x28888)),x28887))),
% 73.40/73.34 inference(scs_inference,[],[2804,2750,2810,2800,2718,2732,2779,2774,1965,2519,2709,628,1465,2728,2874,640,2476,1441,1236,109,76,63,83,68,72,67,69,70,22,5,19,12,18,17,9,25,27,16,13,6,8,23,11,14,15,10,24,26,7,21,4,20,2,42,75,37,77,41,38,34,3,81,82])).
% 73.40/73.34 cnf(2902,plain,
% 73.40/73.34 (P4(f6(f6(f6(f6(f6(x29021,f5(a1,x29022)),f5(x29023,x29024)),f5(x29025,x29026)),f5(x29027,x29028)),f5(x29029,x290210)),f4(f4(a1,x290211),x290212))),
% 73.40/73.34 inference(scs_inference,[],[2807,2834,2876,76,83,63,68,72])).
% 73.40/73.34 cnf(2917,plain,
% 73.40/73.34 (E(f6(x29171,f5(f4(a1,x29172),f4(a1,x29173))),f6(x29171,f5(f4(a1,x29174),a1)))),
% 73.40/73.34 inference(scs_inference,[],[2882,2807,2834,2876,551,1483,76,83,63,68,72,82,67,69,70,5,22,25,18,12,9])).
% 73.40/73.34 cnf(2927,plain,
% 73.40/73.34 (E(f5(f5(f4(a1,x29271),f4(a1,x29272)),x29273),f5(f5(f4(a1,x29274),a1),x29273))),
% 73.40/73.34 inference(scs_inference,[],[2882,2807,2834,2876,551,1483,76,83,63,68,72,82,67,69,70,5,22,25,18,12,9,19,23,27,11,24,17,15,13,16,6])).
% 73.40/73.34 cnf(2940,plain,
% 73.40/73.34 (~P9(f5(a1,f17(f19(x29401,a1,x29402),x29403)),f5(f4(a1,x29404),f17(f19(x29401,a1,x29405),x29406)))),
% 73.40/73.34 inference(scs_inference,[],[2882,2886,2807,2511,2834,2876,2871,551,1483,732,992,76,83,63,68,72,82,67,69,70,5,22,25,18,12,9,19,23,27,11,24,17,15,13,16,6,8,7,10,26,14,21,4,20,2,39,75,37])).
% 73.40/73.34 cnf(2950,plain,
% 73.40/73.34 (~E(f15(f6(x29501,f5(x29502,f14(a9))),x29502),f7(f19(a9,a10,a11)))),
% 73.40/73.34 inference(scs_inference,[],[2882,2886,2807,2790,2511,2834,2876,2871,2667,551,1483,2408,2480,732,141,1670,178,992,49,76,83,63,68,72,82,67,69,70,5,22,25,18,12,9,19,23,27,11,24,17,15,13,16,6,8,7,10,26,14,21,4,20,2,39,75,37,41,34,38,3])).
% 73.40/73.34 cnf(2952,plain,
% 73.40/73.34 (~E(f8(f19(a9,a10,a11)),f8(f19(x29521,a1,x29522)))),
% 73.40/73.34 inference(scs_inference,[],[54,2882,2886,2807,2790,2511,2834,2876,2871,2667,551,1483,98,2408,2480,732,141,1670,178,992,49,76,83,63,68,72,82,67,69,70,5,22,25,18,12,9,19,23,27,11,24,17,15,13,16,6,8,7,10,26,14,21,4,20,2,39,75,37,41,34,38,3,36])).
% 73.40/73.34 cnf(2968,plain,
% 73.40/73.34 (P4(f6(x29681,f5(f4(f4(a1,x29682),x29683),x29684)),f4(a1,x29685))),
% 73.40/73.34 inference(scs_inference,[],[2336,2902,2830,522,1224,1239,76,63,83,68,72,67,69,70])).
% 73.40/73.34 cnf(2971,plain,
% 73.40/73.34 (E(f17(f4(f5(x29711,f4(a1,x29712)),f4(a1,x29713)),x29714),f17(f4(f5(x29711,a1),a1),x29714))),
% 73.40/73.34 inference(scs_inference,[],[2336,2902,2830,522,1224,2205,1239,76,63,83,68,72,67,69,70,5,18])).
% 73.40/73.34 cnf(2976,plain,
% 73.40/73.34 (E(f7(f4(f5(x29761,f4(a1,x29762)),f4(a1,x29763))),f7(f4(f5(x29761,a1),a1)))),
% 73.40/73.34 inference(scs_inference,[],[2336,2902,2830,522,1224,2205,1239,76,63,83,68,72,67,69,70,5,18,19,25,22,15,23])).
% 73.40/73.34 cnf(2994,plain,
% 73.40/73.34 (~E(f8(f19(x29941,a1,x29942)),f8(f19(a9,a10,a11)))),
% 73.40/73.34 inference(scs_inference,[],[2952,2336,2902,2830,522,1224,2205,1239,76,63,83,68,72,67,69,70,5,18,19,25,22,15,23,13,9,7,11,6,12,27,24,17,26,8,10,16,14,21,4,20,2])).
% 73.40/73.34 cnf(2995,plain,
% 73.40/73.34 (~P4(f6(f4(a1,x29951),f5(f8(f19(a9,a10,a11)),x29952)),f8(f19(x29953,a1,x29954)))),
% 73.40/73.34 inference(scs_inference,[],[2952,2336,2902,2830,522,1224,2882,2205,1239,76,63,83,68,72,67,69,70,5,18,19,25,22,15,23,13,9,7,11,6,12,27,24,17,26,8,10,16,14,21,4,20,2,77])).
% 73.40/73.34 cnf(3000,plain,
% 73.40/73.34 (~P5(f16(f6(f8(f19(x30001,a1,x30002)),f5(x30003,x30004)),x30003),x30005)),
% 73.40/73.34 inference(scs_inference,[],[2952,2336,2902,2830,522,1224,2340,2882,2205,1239,223,2077,76,63,83,68,72,67,69,70,5,18,19,25,22,15,23,13,9,7,11,6,12,27,24,17,26,8,10,16,14,21,4,20,2,77,75,39])).
% 73.40/73.34 cnf(3003,plain,
% 73.40/73.34 (~P9(f5(f5(f19(x30031,a1,a3),f4(a1,x30032)),f4(a1,x30033)),f5(f5(f19(x30031,a1,a3),f4(a1,x30034)),a1))),
% 73.40/73.34 inference(scs_inference,[],[2952,2336,2902,2830,2879,522,1224,2779,2340,2882,2205,1239,223,2077,76,63,83,68,72,67,69,70,5,18,19,25,22,15,23,13,9,7,11,6,12,27,24,17,26,8,10,16,14,21,4,20,2,77,75,39,37])).
% 73.40/73.34 cnf(3007,plain,
% 73.40/73.34 (~P9(f5(f5(f4(a1,x30071),x30072),a1),f5(f5(f4(a1,x30073),x30072),f4(a1,x30074)))),
% 73.40/73.34 inference(scs_inference,[],[2952,2336,2902,2830,2853,2879,2580,1959,522,1224,2779,2340,2882,2205,1239,223,2077,1670,76,63,83,68,72,67,69,70,5,18,19,25,22,15,23,13,9,7,11,6,12,27,24,17,26,8,10,16,14,21,4,20,2,77,75,39,37,41,38])).
% 73.40/73.34 cnf(3010,plain,
% 73.40/73.34 (~P8(f6(a1,f5(f8(f19(a9,a10,a11)),x30101)),f8(f19(x30102,a1,x30103)),x30104)),
% 73.40/73.34 inference(scs_inference,[],[2952,2336,2902,2830,2853,2879,2580,1959,522,1224,2779,2340,2882,2205,1239,223,2077,58,1670,76,63,83,68,72,67,69,70,5,18,19,25,22,15,23,13,9,7,11,6,12,27,24,17,26,8,10,16,14,21,4,20,2,77,75,39,37,41,38,86])).
% 73.40/73.34 cnf(3011,plain,
% 73.40/73.34 (~P8(a1,x30111,x30112)),
% 73.40/73.34 inference(rename_variables,[],[58])).
% 73.40/73.34 cnf(3020,plain,
% 73.40/73.34 (~P4(f16(f6(a10,f5(x30201,x30202)),x30201),f7(f19(a9,a10,a11)))),
% 73.40/73.34 inference(scs_inference,[],[2952,2336,2902,2830,2853,2879,2778,2580,1959,2702,522,1224,2779,2340,2882,2205,814,1239,223,2077,101,58,3011,1670,49,76,63,83,68,72,67,69,70,5,18,19,25,22,15,23,13,9,7,11,6,12,27,24,17,26,8,10,16,14,21,4,20,2,77,75,39,37,41,38,86,85,3,96,34])).
% 73.40/73.34 cnf(3033,plain,
% 73.40/73.34 (P8(f6(f6(x30331,f5(a3,a3)),f5(x30332,x30333)),a3,f15(f6(x30334,f5(x30335,a3)),x30335))),
% 73.40/73.34 inference(scs_inference,[],[2338,2968,785,718,76,63,72,83])).
% 73.40/73.34 cnf(3041,plain,
% 73.40/73.34 (P6(f4(a1,x30411),f17(f8(f4(a1,x30412)),f7(f4(a1,x30412))))),
% 73.40/73.34 inference(scs_inference,[],[3020,2338,2968,785,718,136,76,63,72,83,67,68,82,69])).
% 73.40/73.34 cnf(3049,plain,
% 73.40/73.34 (E(f6(x30491,f5(f4(a1,x30492),f4(a1,x30493))),f6(x30491,f5(f4(a1,x30494),f4(a1,x30495))))),
% 73.40/73.34 inference(scs_inference,[],[3020,2338,2968,785,718,136,2038,1489,76,63,72,83,67,68,82,69,70,5,19,18,22,9])).
% 73.40/73.34 cnf(3051,plain,
% 73.40/73.34 (E(f5(x30511,f5(f4(a1,x30512),f4(a1,x30513))),f5(x30511,f5(f4(a1,x30514),f4(a1,x30515))))),
% 73.40/73.34 inference(scs_inference,[],[3020,2338,2968,785,718,136,2038,1489,76,63,72,83,67,68,82,69,70,5,19,18,22,9,11,7])).
% 73.40/73.34 cnf(3070,plain,
% 73.40/73.34 (~P4(f6(f6(f4(f4(a1,x30701),x30702),f5(a10,x30703)),f5(a10,x30704)),f16(f6(f4(a1,x30705),f5(x30706,x30707)),x30706))),
% 73.40/73.34 inference(scs_inference,[],[3020,2601,2338,2968,2873,785,718,136,2038,1489,640,76,63,72,83,67,68,82,69,70,5,19,18,22,9,11,7,27,25,13,8,15,26,12,23,17,4,6,24,21,10,14,16,20,2,77])).
% 73.40/73.34 cnf(3073,plain,
% 73.40/73.34 (P8(f6(x30731,f5(f19(a1,x30732,x30733),f19(a1,x30732,x30733))),f19(f4(a1,x30734),x30732,x30733),f19(f4(a1,x30734),x30732,x30733))),
% 73.40/73.34 inference(scs_inference,[],[3020,2601,2338,2968,2873,785,718,136,2038,1489,640,2141,76,63,72,83,67,68,82,69,70,5,19,18,22,9,11,7,27,25,13,8,15,26,12,23,17,4,6,24,21,10,14,16,20,2,77,75])).
% 73.40/73.34 cnf(3075,plain,
% 73.40/73.34 (~P9(f5(f5(f4(a1,x30751),f4(a1,x30752)),a1),f5(f5(f4(a1,x30753),a1),f4(a1,x30754)))),
% 73.40/73.34 inference(scs_inference,[],[3020,2601,2338,3007,2968,2873,2927,785,718,136,2038,1489,640,2141,76,63,72,83,67,68,82,69,70,5,19,18,22,9,11,7,27,25,13,8,15,26,12,23,17,4,6,24,21,10,14,16,20,2,77,75,37])).
% 73.40/73.34 cnf(3076,plain,
% 73.40/73.34 (~P9(f5(f5(f4(a1,x30761),x30762),a1),f5(f5(f4(a1,x30763),x30762),f4(a1,x30764)))),
% 73.40/73.34 inference(rename_variables,[],[3007])).
% 73.40/73.34 cnf(3077,plain,
% 73.40/73.34 (E(f5(f5(f4(a1,x30771),f4(a1,x30772)),x30773),f5(f5(f4(a1,x30774),a1),x30773))),
% 73.40/73.34 inference(rename_variables,[],[2927])).
% 73.40/73.34 cnf(3086,plain,
% 73.40/73.34 (~E(f15(f6(x30861,f5(x30862,a10)),x30862),f15(f6(x30863,f5(x30864,a1)),x30864))),
% 73.40/73.34 inference(scs_inference,[],[3020,2601,2338,3007,3076,2968,3010,2873,2927,3077,2378,785,718,136,2038,1489,640,139,2141,178,1670,76,63,72,83,67,68,82,69,70,5,19,18,22,9,11,7,27,25,13,8,15,26,12,23,17,4,6,24,21,10,14,16,20,2,77,75,37,41,38,34,3])).
% 73.40/73.34 cnf(3095,plain,
% 73.40/73.34 (P6(f4(f5(x30951,a1),f4(a1,x30952)),f17(f4(f5(x30951,a1),a1),x30953))),
% 73.40/73.34 inference(scs_inference,[],[3020,2601,2338,3007,3076,2466,2564,2968,3010,2971,2873,2821,2927,3077,2378,785,718,136,617,1315,2038,1489,640,139,2141,45,178,1670,76,63,72,83,67,68,82,69,70,5,19,18,22,9,11,7,27,25,13,8,15,26,12,23,17,4,6,24,21,10,14,16,20,2,77,75,37,41,38,34,3,66,95,65,32])).
% 73.40/73.34 cnf(3114,plain,
% 73.40/73.34 (P4(f6(f6(x31141,f5(f12(x31142,a1),x31143)),f5(x31144,x31145)),f12(x31142,a10))),
% 73.40/73.34 inference(scs_inference,[],[3095,1065,63,76,68,67,72])).
% 73.40/73.34 cnf(3116,plain,
% 73.40/73.34 (P8(f6(f6(x31161,f5(f19(a1,x31162,x31163),f19(a1,x31162,x31163))),f5(x31164,x31165)),f19(f4(a1,x31166),x31162,x31163),f19(f4(a1,x31166),x31162,x31163))),
% 73.40/73.34 inference(scs_inference,[],[3095,3073,1065,63,76,68,67,72,83])).
% 73.40/73.34 cnf(3129,plain,
% 73.40/73.34 (E(f12(f4(f12(x31291,a10),f4(a1,x31292)),x31293),f12(f4(f12(x31291,a10),f4(a1,x31294)),x31293))),
% 73.40/73.34 inference(scs_inference,[],[3095,3073,1065,1300,1625,1413,63,76,68,67,72,83,70,69,5,19,22,27,25,18,13,26])).
% 73.40/73.34 cnf(3130,plain,
% 73.40/73.34 (E(f5(x31301,f4(f12(x31302,a10),f4(a1,x31303))),f5(x31301,f4(f12(x31302,a10),f4(a1,x31304))))),
% 73.40/73.34 inference(scs_inference,[],[3095,3073,1065,1300,1625,1413,63,76,68,67,72,83,70,69,5,19,22,27,25,18,13,26,7])).
% 73.40/73.34 cnf(3146,plain,
% 73.40/73.34 (~E(f17(f19(x31461,a10,x31462),f7(f19(a9,a10,a11))),f8(f19(a9,a10,a11)))),
% 73.40/73.34 inference(scs_inference,[],[3095,2672,3073,1065,1300,1625,1413,63,76,68,67,72,83,70,69,5,19,22,27,25,18,13,26,7,9,11,17,15,23,4,14,12,8,10,16,6,21,24,20,2])).
% 73.40/73.34 cnf(3147,plain,
% 73.40/73.34 (~P4(f6(f4(a1,x31471),f5(f8(f19(x31472,a1,x31473)),x31474)),f8(f19(a9,a10,a11)))),
% 73.40/73.34 inference(scs_inference,[],[2994,3095,2672,3073,1065,1300,1625,1413,2882,63,76,68,67,72,83,70,69,5,19,22,27,25,18,13,26,7,9,11,17,15,23,4,14,12,8,10,16,6,21,24,20,2,77])).
% 73.40/73.34 cnf(3150,plain,
% 73.40/73.34 (P8(f6(x31501,f5(f6(x31502,a1),f6(x31502,a1))),f6(x31502,f4(a1,x31503)),f6(x31502,f4(a1,x31503)))),
% 73.40/73.34 inference(scs_inference,[],[2994,3095,2672,3073,1065,1300,1625,1413,2882,2076,63,76,68,67,72,83,70,69,5,19,22,27,25,18,13,26,7,9,11,17,15,23,4,14,12,8,10,16,6,21,24,20,2,77,75])).
% 73.40/73.34 cnf(3152,plain,
% 73.40/73.34 (~P9(f5(f5(a1,f4(a1,x31521)),a1),f5(f5(f4(a1,x31522),a1),f4(a1,x31523)))),
% 73.40/73.34 inference(scs_inference,[],[2994,3095,2672,3073,3075,2640,1065,1300,1625,1413,2882,2076,63,76,68,67,72,83,70,69,5,19,22,27,25,18,13,26,7,9,11,17,15,23,4,14,12,8,10,16,6,21,24,20,2,77,75,37])).
% 73.40/73.34 cnf(3154,plain,
% 73.40/73.34 (P8(f4(f6(x31541,f5(f19(a1,x31542,x31543),f19(a1,x31542,x31543))),f19(a1,x31542,x31543)),f19(f4(a1,x31544),x31542,x31543),f19(f4(a1,x31544),x31542,x31543))),
% 73.40/73.34 inference(scs_inference,[],[2994,3095,2672,3073,3075,2640,1065,2519,1300,1625,1413,2882,2076,63,76,68,67,72,83,70,69,5,19,22,27,25,18,13,26,7,9,11,17,15,23,4,14,12,8,10,16,6,21,24,20,2,77,75,37,41])).
% 73.40/73.34 cnf(3157,plain,
% 73.40/73.34 (~P9(f5(a1,f5(f4(a1,x31571),f4(a1,x31572))),f5(f4(a1,x31573),f5(f4(a1,x31574),f4(a1,x31575))))),
% 73.40/73.34 inference(scs_inference,[],[2994,3095,2672,3073,3075,3051,1447,2640,1065,2519,1300,1625,1413,2882,2076,63,76,68,67,72,83,70,69,5,19,22,27,25,18,13,26,7,9,11,17,15,23,4,14,12,8,10,16,6,21,24,20,2,77,75,37,41,38])).
% 73.40/73.34 cnf(3160,plain,
% 73.40/73.34 (~P4(f6(a1,f5(f8(f19(a9,a10,a11)),x31601)),f8(f19(x31602,a1,x31603)))),
% 73.40/73.34 inference(scs_inference,[],[2994,3095,2672,3073,3075,3051,2995,1447,2640,1065,2519,1300,1625,1413,2882,2076,1669,63,76,68,67,72,83,70,69,5,19,22,27,25,18,13,26,7,9,11,17,15,23,4,14,12,8,10,16,6,21,24,20,2,77,75,37,41,38,34])).
% 73.40/73.34 cnf(3165,plain,
% 73.40/73.34 (~P4(f6(f6(f4(f4(a1,x31651),x31652),f5(a10,x31653)),f5(a10,x31654)),a1)),
% 73.40/73.34 inference(scs_inference,[],[2994,3095,2672,3073,3075,3051,3070,2995,1447,2785,2640,2714,1065,2519,1300,1625,1413,2882,732,2076,1669,63,76,68,67,72,83,70,69,5,19,22,27,25,18,13,26,7,9,11,17,15,23,4,14,12,8,10,16,6,21,24,20,2,77,75,37,41,38,34,3,35])).
% 73.40/73.34 cnf(3177,plain,
% 73.40/73.34 (P4(f6(f6(f6(x31771,f5(f12(x31772,a1),x31773)),f5(x31774,x31775)),f5(x31776,x31777)),f12(x31772,a10))),
% 73.40/73.34 inference(scs_inference,[],[3114,3041,3150,76,63,68,67,83,72])).
% 73.40/73.34 cnf(3179,plain,
% 73.40/73.34 (~P5(f19(x31791,f6(f6(f4(f4(a1,x31792),x31793),f5(a10,x31794)),f5(a10,x31795)),x31796),a1)),
% 73.40/73.34 inference(scs_inference,[],[3165,3114,3041,3150,76,63,68,67,83,72,82])).
% 73.40/73.34 cnf(3210,plain,
% 73.40/73.34 (~P4(f6(f6(f6(f4(f4(a1,x32101),x32102),f5(a10,x32103)),f5(a10,x32104)),f5(a10,x32105)),a1)),
% 73.40/73.34 inference(scs_inference,[],[3165,3114,3041,3150,1320,1916,1509,1357,99,76,63,68,67,83,72,82,70,69,19,5,27,22,13,18,26,11,17,7,23,25,14,9,15,4,16,24,12,21,8,10,6,20,2,77])).
% 73.40/73.34 cnf(3212,plain,
% 73.40/73.34 (P8(f6(x32121,f5(f4(a1,x32122),f4(a1,x32122))),f4(f4(a1,x32123),x32124),f4(f4(a1,x32123),x32124))),
% 73.40/73.34 inference(scs_inference,[],[3165,3114,3041,3150,1320,1916,1509,1357,1236,99,76,63,68,67,83,72,82,70,69,19,5,27,22,13,18,26,11,17,7,23,25,14,9,15,4,16,24,12,21,8,10,6,20,2,77,75])).
% 73.40/73.34 cnf(3217,plain,
% 73.40/73.34 (~P8(f6(f4(a1,x32171),f5(a10,x32172)),f15(f6(x32173,f5(x32174,a1)),x32174),x32175)),
% 73.40/73.34 inference(scs_inference,[],[3165,3114,3041,3150,1320,3129,1040,2413,1916,1509,1357,1236,1670,99,76,63,68,67,83,72,82,70,69,19,5,27,22,13,18,26,11,17,7,23,25,14,9,15,4,16,24,12,21,8,10,6,20,2,77,75,37,41])).
% 73.40/73.34 cnf(3219,plain,
% 73.40/73.34 (~P4(f6(f4(a1,x32191),f5(f19(x32192,a1,a3),f4(a1,x32193))),f8(f19(a9,a10,a11)))),
% 73.40/73.34 inference(scs_inference,[],[3165,3114,3041,3150,1320,3129,3147,1040,2769,2413,1916,1509,1357,1236,1670,99,76,63,68,67,83,72,82,70,69,19,5,27,22,13,18,26,11,17,7,23,25,14,9,15,4,16,24,12,21,8,10,6,20,2,77,75,37,41,34])).
% 73.40/73.34 cnf(3222,plain,
% 73.40/73.34 (~P9(f5(f5(f19(x32221,a1,a3),f4(a1,x32222)),f4(a1,x32223)),f5(f5(f8(f19(x32221,a1,x32224)),f4(a1,x32225)),a1))),
% 73.40/73.34 inference(scs_inference,[],[3165,3114,3041,3150,1320,3003,3129,3147,1040,2769,2704,2413,1916,1509,1357,1236,1670,99,76,63,68,67,83,72,82,70,69,19,5,27,22,13,18,26,11,17,7,23,25,14,9,15,4,16,24,12,21,8,10,6,20,2,77,75,37,41,34,38])).
% 73.40/73.34 cnf(3226,plain,
% 73.40/73.34 (~E(f19(a1,a10,a3),f8(f19(a9,a10,a11)))),
% 73.40/73.34 inference(scs_inference,[],[3165,3114,3146,3041,3150,1320,3003,3129,3147,1040,2769,2704,2413,1916,1509,1357,2154,744,1236,1670,99,76,63,68,67,83,72,82,70,69,19,5,27,22,13,18,26,11,17,7,23,25,14,9,15,4,16,24,12,21,8,10,6,20,2,77,75,37,41,34,38,35,3])).
% 73.40/73.34 cnf(3228,plain,
% 73.40/73.35 (~E(f8(f19(a9,a10,a11)),f19(x32281,x32282,a3))),
% 73.40/73.35 inference(scs_inference,[],[54,3165,3114,3146,3041,3150,1320,3003,3129,3147,1040,2769,2704,2413,1916,1509,1357,2154,59,744,1236,1670,99,76,63,68,67,83,72,82,70,69,19,5,27,22,13,18,26,11,17,7,23,25,14,9,15,4,16,24,12,21,8,10,6,20,2,77,75,37,41,34,38,35,3,36])).
% 73.40/73.35 cnf(3239,plain,
% 73.40/73.35 (P4(f6(f6(f6(f6(x32391,f5(f12(x32392,a1),x32393)),f5(x32394,x32395)),f5(x32396,x32397)),f5(x32398,x32399)),f12(x32392,a10))),
% 73.40/73.35 inference(scs_inference,[],[3177,3212,2286,76,67,63,68,83,72])).
% 73.40/73.35 cnf(3271,plain,
% 73.40/73.35 (~E(f19(x32711,x32712,a3),f8(f19(a9,a10,a11)))),
% 73.40/73.35 inference(scs_inference,[],[3228,3219,3177,3212,2286,1430,1364,76,67,63,68,83,72,82,69,70,19,5,22,27,13,26,17,18,7,11,25,23,24,14,9,4,15,21,16,12,8,6,10,20,2])).
% 73.40/73.35 cnf(3274,plain,
% 73.40/73.35 (P8(f6(x32741,f5(f6(a1,x32742),f6(a1,x32742))),f6(f4(a1,x32743),x32742),f6(f4(a1,x32743),x32742))),
% 73.40/73.35 inference(scs_inference,[],[3228,3226,3219,3177,3212,2286,1430,1364,1669,76,67,63,68,83,72,82,69,70,19,5,22,27,13,26,17,18,7,11,25,23,24,14,9,4,15,21,16,12,8,6,10,20,2,77,75])).
% 73.40/73.35 cnf(3278,plain,
% 73.40/73.35 (P8(f6(x32781,f5(f4(a1,x32782),f4(a1,x32783))),f4(f4(a1,x32784),x32785),f4(f4(a1,x32784),x32785))),
% 73.40/73.35 inference(scs_inference,[],[3228,3226,3219,3177,3212,2286,3049,3157,2645,1430,1364,1669,76,67,63,68,83,72,82,69,70,19,5,22,27,13,26,17,18,7,11,25,23,24,14,9,4,15,21,16,12,8,6,10,20,2,77,75,37,41])).
% 73.40/73.35 cnf(3285,plain,
% 73.40/73.35 (~P4(f6(f4(a1,x32851),f5(f19(x32852,a1,a3),f4(a1,x32853))),f19(a9,f4(a10,f14(a9)),a11))),
% 73.40/73.35 inference(scs_inference,[],[3228,3226,3219,3210,3177,3212,2286,3130,3049,3157,1458,2645,2420,1430,1364,1669,49,76,67,63,68,83,72,82,69,70,19,5,22,27,13,26,17,18,7,11,25,23,24,14,9,4,15,21,16,12,8,6,10,20,2,77,75,37,41,34,38,35])).
% 73.40/73.35 cnf(3288,plain,
% 73.40/73.35 (~P8(f6(f4(a1,x32881),f5(a10,x32882)),f15(f6(x32883,f5(x32884,a1)),x32884),x32885)),
% 73.40/73.35 inference(rename_variables,[],[3217])).
% 73.40/73.35 cnf(3290,plain,
% 73.40/73.35 (~P8(f6(f6(f4(a1,x32901),f5(a10,x32902)),f5(a10,x32903)),f15(f6(x32904,f5(x32905,a1)),x32905),x32906)),
% 73.40/73.35 inference(scs_inference,[],[3228,3226,3219,3210,3217,3288,3177,3212,2286,3130,3049,3157,1458,2645,2420,1430,1364,944,139,1669,49,76,67,63,68,83,72,82,69,70,19,5,22,27,13,26,17,18,7,11,25,23,24,14,9,4,15,21,16,12,8,6,10,20,2,77,75,37,41,34,38,35,85,86])).
% 73.40/73.35 cnf(3297,plain,
% 73.40/73.35 (~P8(f6(f4(a1,x32971),f5(a10,x32972)),a1,x32973)),
% 73.40/73.35 inference(scs_inference,[],[3228,3226,3219,3210,3217,3288,3177,3212,2286,3130,3049,3157,1458,2976,2645,2420,1430,552,1364,944,356,139,1669,178,49,76,67,63,68,83,72,82,69,70,19,5,22,27,13,26,17,18,7,11,25,23,24,14,9,4,15,21,16,12,8,6,10,20,2,77,75,37,41,34,38,35,85,86,3,96,42])).
% 73.40/73.35 cnf(3322,plain,
% 73.40/73.35 (P6(f4(f4(a1,x33221),x33222),f17(f8(a1),f7(a1)))),
% 73.40/73.35 inference(scs_inference,[],[3274,2334,3239,1003,3210,1228,76,68,83,63,67,72,82,69])).
% 73.40/73.35 cnf(3342,plain,
% 73.40/73.35 (E(f4(f4(f12(x33421,a1),f4(a1,x33422)),x33423),f4(f4(f12(x33421,a10),a1),x33423))),
% 73.40/73.35 inference(scs_inference,[],[3274,2334,3239,1003,3210,1228,1344,76,68,83,63,67,72,82,69,70,19,5,13,22,27,7,26,17,18,11,9,23,21,15,14,24,4])).
% 73.40/73.35 cnf(3345,plain,
% 73.40/73.35 (E(f19(x33451,x33452,f4(f12(x33453,a1),f4(a1,x33454))),f19(x33451,x33452,f4(f12(x33453,a10),a1)))),
% 73.40/73.35 inference(scs_inference,[],[3274,2334,3239,1003,3210,1228,1344,76,68,83,63,67,72,82,69,70,19,5,13,22,27,7,26,17,18,11,9,23,21,15,14,24,4,16,25,12])).
% 73.40/73.35 cnf(3352,plain,
% 73.40/73.35 (~P8(f6(f4(a1,x33521),f5(a10,x33522)),f16(f6(f4(a1,x33523),f5(x33524,x33525)),x33524),x33526)),
% 73.40/73.35 inference(scs_inference,[],[3297,3274,2334,2812,3179,3239,1003,3210,1228,1344,744,933,76,68,83,63,67,72,82,69,70,19,5,13,22,27,7,26,17,18,11,9,23,21,15,14,24,4,16,25,12,6,8,10,20,2,40,42])).
% 73.40/73.35 cnf(3358,plain,
% 73.40/73.35 (~P8(f6(a1,f5(a10,x33581)),a1,x33582)),
% 73.40/73.35 inference(scs_inference,[],[3297,3274,2334,2812,3179,3239,3222,1003,3210,2704,1228,1344,744,1669,980,933,76,68,83,63,67,72,82,69,70,19,5,13,22,27,7,26,17,18,11,9,23,21,15,14,24,4,16,25,12,6,8,10,20,2,40,42,75,37,41])).
% 73.40/73.35 cnf(3359,plain,
% 73.40/73.35 (~P8(f6(f4(a1,x33591),f5(a10,x33592)),a1,x33593)),
% 73.40/73.35 inference(rename_variables,[],[3297])).
% 73.40/73.35 cnf(3361,plain,
% 73.40/73.35 (~P4(f6(f4(a1,x33611),f5(f8(f19(x33612,a1,x33613)),f4(a1,x33614))),f19(a9,f4(a10,f14(a9)),a11))),
% 73.40/73.35 inference(scs_inference,[],[3297,3274,2334,2812,3179,3239,3285,3222,2695,1003,3210,2704,1228,1344,744,1669,980,933,76,68,83,63,67,72,82,69,70,19,5,13,22,27,7,26,17,18,11,9,23,21,15,14,24,4,16,25,12,6,8,10,20,2,40,42,75,37,41,34])).
% 73.40/73.35 cnf(3363,plain,
% 73.40/73.35 (~P9(f5(a1,f17(f19(x33631,a1,x33632),x33633)),f5(a1,f17(f19(x33631,a1,x33634),x33635)))),
% 73.40/73.35 inference(scs_inference,[],[3297,3274,2334,2812,3179,3239,3285,2940,3222,2695,1003,3210,2704,1228,1344,744,1669,980,933,992,76,68,83,63,67,72,82,69,70,19,5,13,22,27,7,26,17,18,11,9,23,21,15,14,24,4,16,25,12,6,8,10,20,2,40,42,75,37,41,34,38])).
% 73.40/73.35 cnf(3371,plain,
% 73.40/73.35 (~E(f15(f6(x33711,f5(x33712,a10)),x33712),f16(f6(a1,f5(x33713,x33714)),x33713))),
% 73.40/73.35 inference(scs_inference,[],[3271,3297,3359,3274,2334,2812,3179,3239,3285,2940,3222,2695,1003,3210,2704,1228,1344,170,117,744,1669,980,178,933,992,76,68,83,63,67,72,82,69,70,19,5,13,22,27,7,26,17,18,11,9,23,21,15,14,24,4,16,25,12,6,8,10,20,2,40,42,75,37,41,34,38,86,85,3])).
% 73.40/73.35 cnf(3394,plain,
% 73.40/73.35 (P6(f4(f4(a1,x33941),x33942),f17(f17(f8(a1),f7(a1)),x33943))),
% 73.40/73.35 inference(scs_inference,[],[3322,745,76,68])).
% 73.40/73.35 cnf(3398,plain,
% 73.40/73.35 (P6(f4(f4(a1,x33981),x33982),f8(f17(f8(a1),f7(a1))))),
% 73.40/73.35 inference(scs_inference,[],[3322,3278,745,76,68,83,63])).
% 73.40/73.35 cnf(3400,plain,
% 73.40/73.35 (P6(f4(f4(a1,x34001),x34002),f13(f17(f8(a1),f7(a1)),x34003))),
% 73.40/73.35 inference(scs_inference,[],[3322,3278,745,76,68,83,63,67])).
% 73.40/73.35 cnf(3402,plain,
% 73.40/73.35 (P4(f6(f6(x34021,f5(a2,x34022)),f5(x34023,x34024)),f16(f6(f7(f19(x34025,a1,x34026)),f5(x34027,x34028)),x34027))),
% 73.40/73.35 inference(scs_inference,[],[3322,3278,745,76,68,83,63,67,72])).
% 73.40/73.35 cnf(3408,plain,
% 73.40/73.35 (E(f17(x34081,f4(a1,x34082)),f17(x34081,f4(a1,x34083)))),
% 73.40/73.35 inference(scs_inference,[],[3322,3278,745,1007,157,495,76,68,83,63,67,72,69,70,19])).
% 73.40/73.35 cnf(3409,plain,
% 73.40/73.35 (E(f4(x34091,f4(a1,x34092)),f4(x34091,f4(a1,x34093)))),
% 73.40/73.35 inference(scs_inference,[],[3322,3278,745,1007,157,495,76,68,83,63,67,72,69,70,19,5])).
% 73.40/73.35 cnf(3410,plain,
% 73.40/73.35 (E(f16(f4(a1,x34101),x34102),f16(f4(a1,x34103),x34102))),
% 73.40/73.35 inference(scs_inference,[],[3322,3278,745,1007,157,495,76,68,83,63,67,72,69,70,19,5,13])).
% 73.40/73.35 cnf(3411,plain,
% 73.40/73.35 (E(f12(x34111,f4(a1,x34112)),f12(x34111,f4(a1,x34113)))),
% 73.40/73.35 inference(scs_inference,[],[3322,3278,745,1007,157,495,76,68,83,63,67,72,69,70,19,5,13,27])).
% 73.40/73.35 cnf(3412,plain,
% 73.40/73.35 (E(f18(x34121,f4(a1,x34122)),f18(x34121,f4(a1,x34123)))),
% 73.40/73.35 inference(scs_inference,[],[3322,3278,745,1007,157,495,76,68,83,63,67,72,69,70,19,5,13,27,22])).
% 73.40/73.35 cnf(3416,plain,
% 73.40/73.35 (E(f19(x34161,f4(a1,x34162),x34163),f19(x34161,f4(a1,x34164),x34163))),
% 73.40/73.35 inference(scs_inference,[],[3322,3278,745,1007,157,495,76,68,83,63,67,72,69,70,19,5,13,27,22,7,17,21,11])).
% 73.40/73.35 cnf(3419,plain,
% 73.40/73.35 (E(f16(x34191,f4(a1,x34192)),f16(x34191,f4(a1,x34193)))),
% 73.40/73.35 inference(scs_inference,[],[3322,3278,745,1007,157,495,76,68,83,63,67,72,69,70,19,5,13,27,22,7,17,21,11,15,18,14])).
% 73.40/73.35 cnf(3422,plain,
% 73.40/73.35 (E(f15(x34221,f4(a1,x34222)),f15(x34221,f4(a1,x34223)))),
% 73.40/73.35 inference(scs_inference,[],[3322,3278,745,1007,157,495,76,68,83,63,67,72,69,70,19,5,13,27,22,7,17,21,11,15,18,14,23,26,16])).
% 73.40/73.35 cnf(3428,plain,
% 73.40/73.35 (E(f19(x34281,x34282,f4(a1,x34283)),f19(x34281,x34282,f4(a1,x34284)))),
% 73.40/73.35 inference(scs_inference,[],[3322,3278,745,1007,157,495,76,68,83,63,67,72,69,70,19,5,13,27,22,7,17,21,11,15,18,14,23,26,16,9,24,4,25,6,12])).
% 73.40/73.35 cnf(3431,plain,
% 73.40/73.35 (E(f19(f4(a1,x34311),x34312,x34313),f19(f4(a1,x34314),x34312,x34313))),
% 73.40/73.35 inference(scs_inference,[],[3322,3278,745,1007,157,495,76,68,83,63,67,72,69,70,19,5,13,27,22,7,17,21,11,15,18,14,23,26,16,9,24,4,25,6,12,20,8,10])).
% 73.40/73.35 cnf(3435,plain,
% 73.40/73.35 (~P8(f6(f4(a1,x34351),f5(a10,x34352)),f16(f6(f4(a1,x34353),f5(x34354,x34355)),x34354),x34356)),
% 73.40/73.35 inference(rename_variables,[],[3352])).
% 73.40/73.35 cnf(3436,plain,
% 73.40/73.35 (P8(f6(x34361,f5(f12(x34362,a1),f12(x34362,a1))),f12(x34362,a10),f12(x34362,a10))),
% 73.40/73.35 inference(scs_inference,[],[3322,3352,3278,3086,745,1007,157,495,2464,754,76,68,83,63,67,72,69,70,19,5,13,27,22,7,17,21,11,15,18,14,23,26,16,9,24,4,25,6,12,20,8,10,2,42,75])).
% 73.40/73.35 cnf(3440,plain,
% 73.40/73.35 (P8(f6(x34401,f5(f4(a1,x34402),a1)),f4(f4(a1,x34403),x34404),f4(f4(a1,x34403),x34404))),
% 73.40/73.35 inference(scs_inference,[],[3322,3352,3278,3086,2574,2917,745,1007,431,157,495,2464,754,76,68,83,63,67,72,69,70,19,5,13,27,22,7,17,21,11,15,18,14,23,26,16,9,24,4,25,6,12,20,8,10,2,42,75,37,41])).
% 73.40/73.35 cnf(3444,plain,
% 73.40/73.35 (~P9(f4(f4(f12(x34441,a10),a1),f4(a1,x34442)),f4(f4(f12(x34441,a1),f4(a1,x34443)),a1))),
% 73.40/73.35 inference(scs_inference,[],[3322,3352,3278,3086,3342,2574,1377,2917,745,1007,431,157,495,2464,2408,754,50,76,68,83,63,67,72,69,70,19,5,13,27,22,7,17,21,11,15,18,14,23,26,16,9,24,4,25,6,12,20,8,10,2,42,75,37,41,34,38])).
% 73.40/73.35 cnf(3447,plain,
% 73.40/73.35 (~P8(f6(f6(f4(a1,x34471),f5(a10,x34472)),f5(a10,x34473)),f16(f6(f4(a1,x34474),f5(x34475,x34476)),x34475),x34477)),
% 73.40/73.35 inference(scs_inference,[],[3322,3352,3435,3278,3086,3342,2574,1377,2917,745,1007,431,157,495,2464,640,2408,754,50,76,68,83,63,67,72,69,70,19,5,13,27,22,7,17,21,11,15,18,14,23,26,16,9,24,4,25,6,12,20,8,10,2,42,75,37,41,34,38,86])).
% 73.40/73.35 cnf(3461,plain,
% 73.40/73.35 (P8(f6(f6(x34611,f5(f12(x34612,a1),f12(x34612,a1))),f5(x34613,x34614)),f12(x34612,a10),f12(x34612,a10))),
% 73.40/73.35 inference(scs_inference,[],[3436,3394,3402,730,76,68,72,83])).
% 73.40/73.35 cnf(3498,plain,
% 73.40/73.35 (E(f16(x34981,f4(a1,x34982)),f16(x34981,f4(a1,x34983)))),
% 73.40/73.35 inference(rename_variables,[],[3419])).
% 73.40/73.35 cnf(3499,plain,
% 73.40/73.35 (~P5(f16(f6(f8(f19(x34991,a1,x34992)),f5(f4(a1,x34993),x34994)),f4(a1,x34995)),x34996)),
% 73.40/73.35 inference(scs_inference,[],[3416,3419,3498,3436,3394,3402,2509,2388,730,3000,615,76,68,72,83,67,63,69,70,19,5,27,13,7,17,11,14,22,15,16,23,9,18,21,25,26,4,24,12,6,20,8,10,2,40,39])).
% 73.40/73.35 cnf(3501,plain,
% 73.40/73.35 (E(f16(x35011,f4(a1,x35012)),f16(x35011,f4(a1,x35013)))),
% 73.40/73.35 inference(rename_variables,[],[3419])).
% 73.40/73.35 cnf(3502,plain,
% 73.40/73.35 (~P8(f6(f6(f4(a1,x35021),f5(a10,x35022)),f5(a10,x35023)),f15(f6(x35024,f5(f4(a1,x35025),a1)),f4(a1,x35026)),x35027)),
% 73.40/73.35 inference(scs_inference,[],[3416,3419,3498,3422,3436,3394,3290,3402,2509,2388,730,3000,615,76,68,72,83,67,63,69,70,19,5,27,13,7,17,11,14,22,15,16,23,9,18,21,25,26,4,24,12,6,20,8,10,2,40,39,42])).
% 73.40/73.35 cnf(3504,plain,
% 73.40/73.35 (E(f15(x35041,f4(a1,x35042)),f15(x35041,f4(a1,x35043)))),
% 73.40/73.35 inference(rename_variables,[],[3422])).
% 73.40/73.35 cnf(3509,plain,
% 73.40/73.35 (~P8(f16(f6(f4(a1,x35091),f5(f4(a1,x35092),x35093)),f4(a1,x35094)),x35095,x35096)),
% 73.40/73.35 inference(scs_inference,[],[3416,3419,3498,3501,3422,3436,3394,3290,3402,2509,3363,2388,730,3000,2400,615,51,993,76,68,72,83,67,63,69,70,19,5,27,13,7,17,11,14,22,15,16,23,9,18,21,25,26,4,24,12,6,20,8,10,2,40,39,42,75,37,41])).
% 73.40/73.35 cnf(3511,plain,
% 73.40/73.35 (E(f16(x35111,f4(a1,x35112)),f16(x35111,f4(a1,x35113)))),
% 73.40/73.35 inference(rename_variables,[],[3419])).
% 73.40/73.35 cnf(3512,plain,
% 73.40/73.35 (~P4(f6(a1,f5(f8(f19(x35121,a1,x35122)),f4(a1,x35123))),f19(a9,f4(a10,f14(a9)),a11))),
% 73.40/73.35 inference(scs_inference,[],[3416,3419,3498,3501,3422,3436,3394,3290,3402,2509,3363,3361,2388,730,3000,2400,615,1669,51,993,76,68,72,83,67,63,69,70,19,5,27,13,7,17,11,14,22,15,16,23,9,18,21,25,26,4,24,12,6,20,8,10,2,40,39,42,75,37,41,34])).
% 73.40/73.35 cnf(3514,plain,
% 73.40/73.35 (~P9(f12(f17(f19(x35141,a1,x35142),x35143),a1),f12(f17(f19(x35141,a1,x35144),x35145),a1))),
% 73.40/73.35 inference(scs_inference,[],[3416,3419,3498,3501,3422,3436,3394,3290,3402,2509,2716,3363,3361,2388,730,3000,2400,615,1669,754,51,993,76,68,72,83,67,63,69,70,19,5,27,13,7,17,11,14,22,15,16,23,9,18,21,25,26,4,24,12,6,20,8,10,2,40,39,42,75,37,41,34,38])).
% 73.40/73.35 cnf(3521,plain,
% 73.40/73.35 (~E(f15(f6(x35211,f5(f4(a1,x35212),a1)),f4(a1,x35213)),a10)),
% 73.40/73.35 inference(scs_inference,[],[3416,3419,3498,3501,3511,3422,3504,3436,2384,3394,3290,3402,2509,2716,3363,3361,2388,730,3358,3070,3000,2400,615,117,1669,754,51,993,76,68,72,83,67,63,69,70,19,5,27,13,7,17,11,14,22,15,16,23,9,18,21,25,26,4,24,12,6,20,8,10,2,40,39,42,75,37,41,34,38,35,86,3])).
% 73.40/73.35 cnf(3531,plain,
% 73.40/73.35 (P4(f6(f6(x35311,f5(x35312,x35313)),f5(x35314,x35315)),f15(f6(x35316,f5(x35317,x35312)),x35317))),
% 73.40/73.35 inference(scs_inference,[],[3400,720,76,68,72])).
% 73.40/73.35 cnf(3533,plain,
% 73.40/73.35 (P8(f6(f6(f6(x35331,f5(f12(x35332,a1),f12(x35332,a1))),f5(x35333,x35334)),f5(x35335,x35336)),f12(x35332,a10),f12(x35332,a10))),
% 73.40/73.35 inference(scs_inference,[],[3461,3400,720,76,68,72,83])).
% 73.40/73.35 cnf(3547,plain,
% 73.40/73.35 (E(f5(x35471,f19(x35472,x35473,f4(a1,x35474))),f5(x35471,f19(x35472,x35473,f4(a1,x35475))))),
% 73.40/73.35 inference(scs_inference,[],[3428,3461,3400,720,482,76,68,72,83,67,63,69,70,19,13,27,5,7])).
% 73.40/73.35 cnf(3559,plain,
% 73.40/73.35 (E(f4(f19(x35591,x35592,f4(a1,x35593)),x35594),f4(f19(x35591,x35592,f4(a1,x35595)),x35594))),
% 73.40/73.35 inference(scs_inference,[],[3428,3461,3400,720,482,76,68,72,83,67,63,69,70,19,13,27,5,7,22,15,11,18,21,14,17,25,23,16,9,4])).
% 73.40/73.35 cnf(3567,plain,
% 73.40/73.35 (~E(a10,f15(f6(x35671,f5(f4(a1,x35672),a1)),f4(a1,x35673)))),
% 73.40/73.35 inference(scs_inference,[],[3428,3461,3521,3400,720,482,76,68,72,83,67,63,69,70,19,13,27,5,7,22,15,11,18,21,14,17,25,23,16,9,4,26,6,12,24,8,20,10,2])).
% 73.40/73.35 cnf(3581,plain,
% 73.40/73.35 (~P9(f17(f19(f4(a1,x35811),a10,x35812),f7(f19(a9,a10,a11))),f19(f4(a1,x35813),a10,a3))),
% 73.40/73.35 inference(scs_inference,[],[3428,3431,3461,3521,3400,3499,3440,3444,3512,971,720,3342,2769,2378,482,198,1670,76,68,72,83,67,63,69,70,19,13,27,5,7,22,15,11,18,21,14,17,25,23,16,9,4,26,6,12,24,8,20,10,2,39,75,41,37,34,38])).
% 73.40/73.35 cnf(3582,plain,
% 73.40/73.35 (E(f19(f4(a1,x35821),x35822,x35823),f19(f4(a1,x35824),x35822,x35823))),
% 73.40/73.35 inference(rename_variables,[],[3431])).
% 73.40/73.35 cnf(3584,plain,
% 73.40/73.35 (~P4(f6(a1,f5(f8(f19(a9,a10,a11)),x35841)),f19(x35842,a1,a3))),
% 73.40/73.35 inference(scs_inference,[],[3428,3431,3461,3521,3400,3499,3440,3444,3160,3512,971,720,3342,2769,2378,482,198,1670,131,76,68,72,83,67,63,69,70,19,13,27,5,7,22,15,11,18,21,14,17,25,23,16,9,4,26,6,12,24,8,20,10,2,39,75,41,37,34,38,35])).
% 73.40/73.35 cnf(3594,plain,
% 73.40/73.35 (~P8(f6(a1,f5(a10,x35941)),f16(f6(f4(a1,x35942),f5(x35943,x35944)),x35943),x35945)),
% 73.40/73.35 inference(scs_inference,[],[3428,3431,3582,3461,3509,3521,3400,3499,3440,3444,3345,3160,3512,971,720,3342,2769,2378,482,132,3358,944,198,744,1670,131,76,68,72,83,67,63,69,70,19,13,27,5,7,22,15,11,18,21,14,17,25,23,16,9,4,26,6,12,24,8,20,10,2,39,75,41,37,34,38,35,86,3,96,42])).
% 73.40/73.35 cnf(3602,plain,
% 73.40/73.35 (P4(f6(f6(f6(x36021,f5(x36022,x36023)),f5(x36024,x36025)),f5(x36026,x36027)),f15(f6(x36028,f5(x36029,x36022)),x36029))),
% 73.40/73.35 inference(scs_inference,[],[3398,3531,68,72])).
% 73.40/73.35 cnf(3612,plain,
% 73.40/73.35 (P6(f7(f19(x36121,a1,x36122)),f17(f8(a2),f7(a2)))),
% 73.40/73.35 inference(scs_inference,[],[3398,3533,3531,454,68,72,83,76,67,63,69])).
% 73.40/73.35 cnf(3617,plain,
% 73.40/73.35 (E(f4(x36171,f17(x36172,f4(a1,x36173))),f4(x36171,f17(x36172,f4(a1,x36174))))),
% 73.40/73.35 inference(scs_inference,[],[3398,3533,3531,3408,454,68,72,83,76,67,63,69,70,19,5])).
% 73.40/73.35 cnf(3634,plain,
% 73.40/73.35 (E(f4(f17(x36341,f4(a1,x36342)),x36343),f4(f17(x36341,f4(a1,x36344)),x36343))),
% 73.40/73.35 inference(scs_inference,[],[3398,3533,3531,3408,454,68,72,83,76,67,63,69,70,19,5,13,27,7,18,15,21,11,22,23,16,17,14,9,25,26,24,4])).
% 73.40/73.35 cnf(3636,plain,
% 73.40/73.35 (E(f5(f17(x36361,f4(a1,x36362)),x36363),f5(f17(x36361,f4(a1,x36364)),x36363))),
% 73.40/73.35 inference(scs_inference,[],[3398,3533,3531,3408,454,68,72,83,76,67,63,69,70,19,5,13,27,7,18,15,21,11,22,23,16,17,14,9,25,26,24,4,12,6])).
% 73.40/73.35 cnf(3649,plain,
% 73.40/73.35 (E(f6(f4(a1,x36491),x36492),f6(a1,x36492))),
% 73.40/73.35 inference(rename_variables,[],[1670])).
% 73.40/73.35 cnf(3656,plain,
% 73.40/73.35 (~E(a10,f15(f6(x36561,f5(f4(a1,x36562),a1)),f4(a1,x36563)))),
% 73.40/73.35 inference(rename_variables,[],[3567])).
% 73.40/73.35 cnf(3667,plain,
% 73.40/73.35 (~P4(f6(f6(f4(a1,x36671),f5(a10,x36672)),f5(a10,x36673)),f15(f6(x36674,f5(f4(a1,x36675),a1)),f4(a1,x36676)))),
% 73.40/73.35 inference(scs_inference,[],[3567,3656,3398,3594,3533,3531,3584,3371,3514,819,3502,3408,3419,3422,2490,2374,454,2501,342,178,1670,3649,753,68,72,83,76,67,63,69,70,19,5,13,27,7,18,15,21,11,22,23,16,17,14,9,25,26,24,4,12,6,20,8,10,2,75,42,37,41,34,38,85,86,3,77,35])).
% 73.40/73.35 cnf(3668,plain,
% 73.40/73.35 (E(f15(x36681,f4(a1,x36682)),f15(x36681,f4(a1,x36683)))),
% 73.40/73.35 inference(rename_variables,[],[3422])).
% 73.40/73.35 cnf(3679,plain,
% 73.40/73.35 (P6(f4(f19(x36791,x36792,f4(a1,x36793)),f4(a1,x36794)),f4(f19(x36791,x36792,f4(a1,x36795)),f4(a1,x36796)))),
% 73.40/73.35 inference(scs_inference,[],[3567,3656,3398,3594,3533,3152,3531,3584,2816,3547,3559,3371,3514,819,3502,3408,3419,3422,3668,2490,2374,1976,899,454,2501,1368,342,178,1670,3649,753,68,72,83,76,67,63,69,70,19,5,13,27,7,18,15,21,11,22,23,16,17,14,9,25,26,24,4,12,6,20,8,10,2,75,42,37,41,34,38,85,86,3,77,35,66,43,65,32,31])).
% 73.40/73.35 cnf(3735,plain,
% 73.40/73.35 (~P9(f19(a1,a10,a3),f19(f4(a1,x37351),a10,a3))),
% 73.40/73.35 inference(scs_inference,[],[3612,3581,3033,3667,3602,2307,3409,727,3567,1734,2160,1098,72,68,76,83,67,63,69,70,19,7,5,27,18,13,15,21,11,14,17,22,23,16,9,25,24,26,4,12,6,8,20,10,2,77,75,37])).
% 73.40/73.35 cnf(3738,plain,
% 73.40/73.35 (~P4(f16(f6(f6(f6(f4(f4(a1,x37381),x37382),f5(a10,x37383)),f5(a10,x37384)),f5(x37385,x37386)),x37385),a1)),
% 73.40/73.35 inference(scs_inference,[],[3612,3581,3033,3667,3602,2307,3409,727,3567,3165,1734,2160,58,1098,933,49,72,68,76,83,67,63,69,70,19,7,5,27,18,13,15,21,11,14,17,22,23,16,9,25,24,26,4,12,6,8,20,10,2,77,75,37,41,34])).
% 73.40/73.35 cnf(3743,plain,
% 73.40/73.35 (~P4(f6(f6(f4(a1,x37431),f5(a10,x37432)),f5(a10,x37433)),a1)),
% 73.40/73.35 inference(scs_inference,[],[3612,3581,3033,3667,3602,3634,2307,1380,3409,727,3567,3165,1734,2160,58,1098,178,933,49,72,68,76,83,67,63,69,70,19,7,5,27,18,13,15,21,11,14,17,22,23,16,9,25,24,26,4,12,6,8,20,10,2,77,75,37,41,34,38,35])).
% 73.40/73.35 cnf(3761,plain,
% 73.40/73.35 (P4(f6(f6(x37611,f5(f5(a1,a1),x37612)),f5(x37613,x37614)),f5(f4(a1,x37615),f4(a1,x37616)))),
% 73.40/73.35 inference(scs_inference,[],[1697,72])).
% 73.40/73.35 cnf(3771,plain,
% 73.40/73.35 (P6(f15(f6(x37711,f5(x37712,x37713)),x37712),f17(f8(x37713),f7(x37713)))),
% 73.40/73.35 inference(scs_inference,[],[3679,3116,1697,1407,477,72,76,68,83,67,69])).
% 73.40/73.35 cnf(3801,plain,
% 73.40/73.35 (~E(f7(f19(a9,a10,a11)),f15(f6(x38011,f5(x38012,f14(a9))),x38012))),
% 73.40/73.35 inference(scs_inference,[],[3679,3116,2950,3410,1697,1407,477,72,76,68,83,67,69,63,70,19,27,5,18,7,13,15,21,11,17,22,23,14,9,16,24,12,26,25,4,6,8,20,10,2])).
% 73.40/73.35 cnf(3812,plain,
% 73.40/73.35 (~P4(f6(f6(f4(a1,x38121),f5(a10,x38122)),f5(a10,x38123)),f16(f6(f4(a1,x38124),f5(x38125,x38126)),x38125))),
% 73.40/73.35 inference(scs_inference,[],[3743,3679,3116,3617,3738,2950,816,1613,3410,1697,1407,2374,3419,477,744,993,72,76,68,83,67,69,63,70,19,27,5,18,7,13,15,21,11,17,22,23,14,9,16,24,12,26,25,4,6,8,20,10,2,75,37,34,38,35])).
% 73.40/73.35 cnf(3813,plain,
% 73.40/73.35 (~E(f15(f6(x38131,f5(x38132,a10)),x38132),f4(a1,x38133))),
% 73.40/73.35 inference(scs_inference,[],[3743,3679,3116,3617,3738,2950,816,1613,3410,1697,1407,2374,3419,477,112,744,178,993,72,76,68,83,67,69,63,70,19,27,5,18,7,13,15,21,11,17,22,23,14,9,16,24,12,26,25,4,6,8,20,10,2,75,37,34,38,35,3])).
% 73.40/73.35 cnf(3815,plain,
% 73.40/73.35 (~P4(f6(f6(f6(f4(a1,x38151),f5(a10,x38152)),f5(a10,x38153)),f5(a10,x38154)),a1)),
% 73.40/73.35 inference(scs_inference,[],[3743,3679,3116,3617,3738,2950,816,1613,3410,1697,1407,2374,3419,477,112,744,178,993,99,72,76,68,83,67,69,63,70,19,27,5,18,7,13,15,21,11,17,22,23,14,9,16,24,12,26,25,4,6,8,20,10,2,75,37,34,38,35,3,77])).
% 73.40/73.35 cnf(3821,plain,
% 73.40/73.35 (P4(f6(f6(f6(x38211,f5(f5(a1,a1),x38212)),f5(x38213,x38214)),f5(x38215,x38216)),f5(f4(a1,x38217),f4(a1,x38218)))),
% 73.40/73.35 inference(scs_inference,[],[3761,76,72])).
% 73.40/73.35 cnf(3829,plain,
% 73.40/73.35 (P6(f16(f6(f4(a1,x38291),f5(x38292,x38293)),x38292),f17(f8(a1),f7(a1)))),
% 73.40/73.35 inference(scs_inference,[],[3771,3761,3154,489,76,72,68,83,67,69])).
% 73.40/73.35 cnf(3838,plain,
% 73.40/73.35 (E(f4(x38381,f12(x38382,f4(a1,x38383))),f4(x38381,f12(x38382,f4(a1,x38384))))),
% 73.40/73.35 inference(scs_inference,[],[3771,3761,3154,3411,489,76,72,68,83,67,69,63,70,19,27,18,5])).
% 73.40/73.35 cnf(3860,plain,
% 73.40/73.35 (P8(f6(x38601,f5(f19(x38602,a1,a3),f19(x38602,a1,a3))),f8(f19(x38602,a1,x38603)),f8(f19(x38602,a1,x38603)))),
% 73.40/73.35 inference(scs_inference,[],[3813,3771,3761,3154,3411,489,131,76,72,68,83,67,69,63,70,19,27,18,5,13,7,11,15,21,23,22,17,14,16,12,24,25,9,4,26,6,8,20,10,2,75])).
% 73.40/73.35 cnf(3864,plain,
% 73.40/73.35 (~P4(f15(f6(x38641,f5(x38642,a10)),x38642),f7(f19(a9,a10,a11)))),
% 73.40/73.35 inference(scs_inference,[],[3735,3813,3771,3761,3154,3411,2142,489,101,131,50,76,72,68,83,67,69,63,70,19,27,18,5,13,7,11,15,21,23,22,17,14,16,12,24,25,9,4,26,6,8,20,10,2,75,37,34])).
% 73.40/73.35 cnf(3872,plain,
% 73.40/73.35 (~E(f17(f19(x38721,a10,a3),f14(a9)),f8(f19(a9,a10,a11)))),
% 73.40/73.35 inference(scs_inference,[],[3735,3813,3771,3761,3812,3154,3636,1950,3411,2398,3271,2142,489,3419,101,131,50,76,72,68,83,67,69,63,70,19,27,18,5,13,7,11,15,21,23,22,17,14,16,12,24,25,9,4,26,6,8,20,10,2,75,37,34,38,35,3])).
% 73.40/73.35 cnf(3947,plain,
% 73.40/73.35 ($false),
% 73.40/73.35 inference(scs_inference,[],[3872,3815,3829,3864,3860,3447,3821,3838,2888,3801,1615,1745,3412,2484,676,2453,2451,2882,1355,732,944,58,744,178,933,76,72,83,68,67,69,63,70,19,27,18,5,13,7,11,21,23,15,22,16,17,14,24,12,25,6,9,26,4,8,20,10,2,40,77,75,37,34,38,86,85,35,3]),
% 73.40/73.35 ['proof']).
% 73.40/73.35 % SZS output end Proof
% 73.40/73.35 % Total time :72.640000s
%------------------------------------------------------------------------------