%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : SWV377+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 : n001.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:02 EDT 2024
% Result : Theorem 117.71s 117.87s
% Output : CNFRefutation 117.83s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.10/0.10 % Problem : SWV377+1 : TPTP v8.2.0. Released v3.3.0.
% 0.10/0.10 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% 0.10/0.31 % Computer : n001.cluster.edu
% 0.10/0.31 % Model : x86_64 x86_64
% 0.10/0.31 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.31 % Memory : 8042.1875MB
% 0.10/0.31 % OS : Linux 3.10.0-693.el7.x86_64
% 0.10/0.31 % CPULimit : 300
% 0.10/0.31 % WCLimit : 300
% 0.10/0.31 % DateTime : Thu Jun 20 13:40:39 EDT 2024
% 0.10/0.31 % CPUTime :
% 0.16/0.54 start to proof:theBenchmark
% 117.71/117.86 %-------------------------------------------
% 117.71/117.86 % File :CSE---1.7
% 117.71/117.86 % Problem :theBenchmark
% 117.71/117.86 % Transform :cnf
% 117.71/117.86 % Format :tptp:raw
% 117.71/117.86 % Command :java -jar mcs_scs.jar %d %s
% 117.71/117.86
% 117.71/117.86 % Result :Theorem 117.180000s
% 117.71/117.86 % Output :CNFRefutation 117.180000s
% 117.71/117.86 %-------------------------------------------
% 117.71/117.87 %------------------------------------------------------------------------------
% 117.71/117.87 % File : SWV377+1 : TPTP v8.2.0. Released v3.3.0.
% 117.71/117.87 % Domain : Software Verification
% 117.71/117.87 % Problem : Priority queue checker: lemma_not_ok_persistence_induction step 1
% 117.71/117.87 % Version : [dNP05] axioms.
% 117.71/117.87 % English :
% 117.71/117.87
% 117.71/117.87 % Refs : [Pis06] Piskac (2006), Email to Geoff Sutcliffe
% 117.71/117.87 % : [dNP05] de Nivelle & Piskac (2005), Verification of an Off-Lin
% 117.71/117.87 % Source : [Pis06]
% 117.71/117.87 % Names : cpq_l013 [Pis06]
% 117.71/117.87
% 117.71/117.87 % Status : Theorem
% 117.71/117.87 % Rating : 0.22 v8.2.0, 0.19 v8.1.0, 0.22 v7.5.0, 0.25 v7.4.0, 0.17 v7.3.0, 0.21 v7.1.0, 0.17 v7.0.0, 0.20 v6.4.0, 0.27 v6.3.0, 0.25 v6.2.0, 0.28 v6.1.0, 0.27 v6.0.0, 0.22 v5.5.0, 0.30 v5.4.0, 0.36 v5.3.0, 0.33 v5.2.0, 0.25 v5.1.0, 0.24 v5.0.0, 0.21 v4.1.0, 0.22 v4.0.1, 0.30 v4.0.0, 0.33 v3.7.0, 0.30 v3.5.0, 0.26 v3.4.0, 0.21 v3.3.0
% 117.71/117.87 % Syntax : Number of formulae : 42 ( 16 unt; 0 def)
% 117.71/117.87 % Number of atoms : 84 ( 29 equ)
% 117.71/117.87 % Maximal formula atoms : 4 ( 2 avg)
% 117.71/117.87 % Number of connectives : 57 ( 15 ~; 3 |; 12 &)
% 117.71/117.87 % ( 7 <=>; 20 =>; 0 <=; 0 <~>)
% 117.71/117.87 % Maximal formula depth : 9 ( 5 avg)
% 117.71/117.87 % Maximal term depth : 4 ( 1 avg)
% 117.71/117.87 % Number of predicates : 11 ( 9 usr; 1 prp; 0-3 aty)
% 117.71/117.87 % Number of functors : 18 ( 18 usr; 3 con; 0-3 aty)
% 117.71/117.87 % Number of variables : 121 ( 121 !; 0 ?)
% 117.71/117.87 % SPC : FOF_THM_RFO_SEQ
% 117.71/117.87
% 117.71/117.87 % Comments :
% 117.71/117.87 %------------------------------------------------------------------------------
% 117.71/117.87 %----Include the axioms about priority queues and checked priority queues
% 117.71/117.87 include('Axioms/SWV007+0.ax').
% 117.71/117.87 include('Axioms/SWV007+2.ax').
% 117.71/117.87 include('Axioms/SWV007+3.ax').
% 117.71/117.87 %------------------------------------------------------------------------------
% 117.71/117.87 %----goal: fof(l12_l13, lemma, (! [U,V,W] : (~(ok(triple(U,V,W))) =>
% 117.71/117.87 %---- ~(ok(im_succ_cpq(triple(U,V,W))))))).
% 117.71/117.87
% 117.71/117.87 %----step1: insert (conjecture)
% 117.71/117.87 fof(l13_co,conjecture,
% 117.71/117.87 ! [U,V,W,X] :
% 117.71/117.87 ( ~ ok(triple(U,V,W))
% 117.71/117.87 => ~ ok(insert_cpq(triple(U,V,W),X)) ) ).
% 117.71/117.87
% 117.71/117.87 %------------------------------------------------------------------------------
% 117.71/117.87 %-------------------------------------------
% 117.71/117.87 % Proof found
% 117.71/117.87 % SZS status Theorem for theBenchmark
% 117.71/117.87 % SZS output start Proof
% 117.71/117.88 %ClaNum:93(EqnAxiom:43)
% 117.71/117.88 %VarNum:299(SingletonVarNum:147)
% 117.71/117.88 %MaxLitNum:4
% 117.71/117.88 %MaxfuncDepth:3
% 117.71/117.88 %SharedTerms:12
% 117.71/117.88 %goalClause: 54 59
% 117.71/117.88 %singleGoalClaCount:2
% 117.71/117.88 [56]~P2(a1)
% 117.71/117.88 [59]~P7(f20(a9,a10,a11))
% 117.71/117.88 [54]P7(f13(f20(a9,a10,a11),a12))
% 117.71/117.88 [45]P1(a2,x451)
% 117.71/117.88 [46]P1(x461,x461)
% 117.71/117.88 [47]P6(x471,x471)
% 117.71/117.88 [57]~P4(a1,x571)
% 117.71/117.88 [44]E(f4(a1,x441),a1)
% 117.71/117.88 [58]~P8(a1,x581,x582)
% 117.71/117.88 [52]P3(f20(x521,a1,x522))
% 117.71/117.88 [60]~P7(f20(x601,x602,a3))
% 117.71/117.88 [51]E(f7(f20(x511,a1,x512)),a2)
% 117.71/117.88 [53]E(f8(f20(x531,a1,x532)),f20(x531,a1,a3))
% 117.71/117.88 [48]P2(f6(x481,f5(x482,x483)))
% 117.71/117.88 [49]E(f17(f6(x491,f5(x492,x493)),x492),x491)
% 117.71/117.88 [50]E(f16(f6(x501,f5(x502,x503)),x502),x503)
% 117.71/117.88 [55]E(f20(f15(x551,x552),f6(x553,f5(x552,a2)),x554),f13(f20(x551,x553,x554),x552))
% 117.71/117.88 [61]P1(x612,x611)+P1(x611,x612)
% 117.71/117.88 [62]~P9(x621,x622)+P1(x621,x622)
% 117.71/117.88 [64]~P9(x642,x641)+~P1(x641,x642)
% 117.71/117.88 [63]~P6(x631,x632)+P6(x631,f8(x632))
% 117.71/117.88 [69]~P6(x691,x692)+P6(x691,f18(f8(x692),f7(x692)))
% 117.71/117.88 [67]~P6(x671,x672)+P6(x671,f13(x672,x673))
% 117.71/117.88 [68]~P6(x681,x682)+P6(x681,f18(x682,x683))
% 117.71/117.88 [71]E(x711,a3)+P7(f20(x712,x713,x711))
% 117.71/117.88 [73]E(x731,a1)+E(f7(f20(x732,x731,x733)),f14(x732))
% 117.71/117.89 [76]~P4(x762,x764)+P5(f20(x761,x762,x763),x764)
% 117.71/117.89 [82]P4(x821,x822)+~P5(f20(x823,x821,x824),x822)
% 117.71/117.89 [70]~E(x702,x704)+P4(f6(x701,f5(x702,x703)),x704)
% 117.71/117.89 [72]~P4(x721,x724)+P4(f6(x721,f5(x722,x723)),x724)
% 117.71/117.89 [81]P4(x812,x814)+E(f18(f20(x811,x812,x813),x814),f20(x811,x812,a3))
% 117.71/117.89 [78]~P1(x782,x784)+E(f6(f4(x781,x782),f5(x783,x784)),f4(f6(x781,f5(x783,x784)),x782))
% 117.71/117.89 [79]~P9(x793,x794)+E(f4(f6(x791,f5(x792,x793)),x794),f6(f4(x791,x794),f5(x792,x794)))
% 117.71/117.89 [83]~P8(x831,x834,x835)+P8(f6(x831,f5(x832,x833)),x834,x835)
% 117.71/117.89 [91]~P9(x911,x912)+~P3(f20(x913,f6(x914,f5(x911,x912)),x915))
% 117.71/117.89 [65]P9(x652,x651)+~P1(x652,x651)+P1(x651,x652)
% 117.71/117.89 [66]~P1(x661,x663)+P1(x661,x662)+~P1(x663,x662)
% 117.71/117.89 [84]P4(x841,f14(x842))+E(x841,a1)+E(f8(f20(x842,x841,x843)),f20(x842,f4(x841,f14(x842)),a3))
% 117.71/117.89 [77]E(x771,x772)+P4(x773,x772)+~P4(f6(x773,f5(x771,x774)),x772)
% 117.71/117.89 [87]~P4(x872,x874)+~P9(x874,f16(x872,x874))+E(f18(f20(x871,x872,x873),x874),f20(f19(x871,x874),f17(x872,x874),a3))
% 117.71/117.89 [88]~P4(x883,x882)+~P1(f16(x883,x882),x882)+E(f20(f19(x881,x882),f17(x883,x882),x884),f18(f20(x881,x883,x884),x882))
% 117.71/117.89 [74]~P4(x743,x742)+E(x741,x742)+E(f16(f6(x743,f5(x741,x744)),x742),f16(x743,x742))
% 117.71/117.89 [80]~P4(x803,x802)+E(x801,x802)+E(f17(f6(x803,f5(x801,x804)),x802),f6(f17(x803,x802),f5(x801,x804)))
% 117.71/117.89 [75]~E(x753,x755)+~E(x752,x754)+P8(f6(x751,f5(x752,x753)),x754,x755)
% 117.71/117.89 [85]E(x851,x852)+P8(x853,x854,x852)+~P8(f6(x853,f5(x855,x851)),x854,x852)
% 117.71/117.89 [86]E(x861,x862)+P8(x863,x862,x864)+~P8(f6(x863,f5(x861,x865)),x862,x864)
% 117.71/117.89 [92]~P1(x924,x923)+~P3(f20(x921,x922,x925))+P3(f20(x921,f6(x922,f5(x923,x924)),x925))
% 117.71/117.89 [93]~P1(x934,x935)+P3(f20(x931,x932,x933))+~P3(f20(x931,f6(x932,f5(x935,x934)),x933))
% 117.71/117.89 [89]~P4(x891,f14(x892))+E(x891,a1)+~P9(f14(x892),f16(x891,f14(x892)))+E(f8(f20(x892,x891,x893)),f20(x892,f4(x891,f14(x892)),a3))
% 117.71/117.89 [90]~P4(x901,f14(x902))+E(x901,a1)+~P1(f16(x901,f14(x902)),f14(x902))+E(f20(x902,f4(x901,f14(x902)),x903),f8(f20(x902,x901,x903)))
% 117.71/117.89 %EqnAxiom
% 117.71/117.89 [1]E(x11,x11)
% 117.71/117.89 [2]E(x22,x21)+~E(x21,x22)
% 117.71/117.89 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 117.71/117.89 [4]~E(x41,x42)+E(f4(x41,x43),f4(x42,x43))
% 117.71/117.89 [5]~E(x51,x52)+E(f4(x53,x51),f4(x53,x52))
% 117.71/117.89 [6]~E(x61,x62)+E(f5(x61,x63),f5(x62,x63))
% 117.71/117.89 [7]~E(x71,x72)+E(f5(x73,x71),f5(x73,x72))
% 117.71/117.89 [8]~E(x81,x82)+E(f6(x81,x83),f6(x82,x83))
% 117.71/117.89 [9]~E(x91,x92)+E(f6(x93,x91),f6(x93,x92))
% 117.71/117.89 [10]~E(x101,x102)+E(f20(x101,x103,x104),f20(x102,x103,x104))
% 117.71/117.89 [11]~E(x111,x112)+E(f20(x113,x111,x114),f20(x113,x112,x114))
% 117.71/117.89 [12]~E(x121,x122)+E(f20(x123,x124,x121),f20(x123,x124,x122))
% 117.71/117.89 [13]~E(x131,x132)+E(f8(x131),f8(x132))
% 117.71/117.89 [14]~E(x141,x142)+E(f17(x141,x143),f17(x142,x143))
% 117.71/117.89 [15]~E(x151,x152)+E(f17(x153,x151),f17(x153,x152))
% 117.71/117.89 [16]~E(x161,x162)+E(f14(x161),f14(x162))
% 117.71/117.89 [17]~E(x171,x172)+E(f16(x171,x173),f16(x172,x173))
% 117.71/117.89 [18]~E(x181,x182)+E(f16(x183,x181),f16(x183,x182))
% 117.71/117.89 [19]~E(x191,x192)+E(f18(x191,x193),f18(x192,x193))
% 117.71/117.89 [20]~E(x201,x202)+E(f18(x203,x201),f18(x203,x202))
% 117.71/117.89 [21]~E(x211,x212)+E(f13(x211,x213),f13(x212,x213))
% 117.71/117.89 [22]~E(x221,x222)+E(f13(x223,x221),f13(x223,x222))
% 117.71/117.89 [23]~E(x231,x232)+E(f7(x231),f7(x232))
% 117.71/117.89 [24]~E(x241,x242)+E(f15(x241,x243),f15(x242,x243))
% 117.71/117.89 [25]~E(x251,x252)+E(f15(x253,x251),f15(x253,x252))
% 117.71/117.89 [26]~E(x261,x262)+E(f19(x261,x263),f19(x262,x263))
% 117.71/117.89 [27]~E(x271,x272)+E(f19(x273,x271),f19(x273,x272))
% 117.71/117.89 [28]P1(x282,x283)+~E(x281,x282)+~P1(x281,x283)
% 117.71/117.89 [29]P1(x293,x292)+~E(x291,x292)+~P1(x293,x291)
% 117.71/117.89 [30]~P3(x301)+P3(x302)+~E(x301,x302)
% 117.71/117.89 [31]P6(x312,x313)+~E(x311,x312)+~P6(x311,x313)
% 117.71/117.89 [32]P6(x323,x322)+~E(x321,x322)+~P6(x323,x321)
% 117.71/117.89 [33]~P2(x331)+P2(x332)+~E(x331,x332)
% 117.71/117.89 [34]P4(x342,x343)+~E(x341,x342)+~P4(x341,x343)
% 117.71/117.89 [35]P4(x353,x352)+~E(x351,x352)+~P4(x353,x351)
% 117.71/117.89 [36]~P7(x361)+P7(x362)+~E(x361,x362)
% 117.71/117.89 [37]P9(x372,x373)+~E(x371,x372)+~P9(x371,x373)
% 117.71/117.89 [38]P9(x383,x382)+~E(x381,x382)+~P9(x383,x381)
% 117.71/117.89 [39]P5(x392,x393)+~E(x391,x392)+~P5(x391,x393)
% 117.71/117.89 [40]P5(x403,x402)+~E(x401,x402)+~P5(x403,x401)
% 117.71/117.89 [41]P8(x412,x413,x414)+~E(x411,x412)+~P8(x411,x413,x414)
% 117.71/117.89 [42]P8(x423,x422,x424)+~E(x421,x422)+~P8(x423,x421,x424)
% 117.71/117.89 [43]P8(x433,x434,x432)+~E(x431,x432)+~P8(x433,x434,x431)
% 117.71/117.89
% 117.71/117.89 %-------------------------------------------
% 117.83/117.90 cnf(94,plain,
% 117.83/117.90 (P4(f6(x942,f5(x941,x943)),x941)),
% 117.83/117.90 inference(equality_inference,[],[70])).
% 117.83/117.90 cnf(95,plain,
% 117.83/117.90 (E(a11,a3)),
% 117.83/117.90 inference(scs_inference,[],[59,71])).
% 117.83/117.90 cnf(97,plain,
% 117.83/117.90 (E(a1,f4(a1,x971))),
% 117.83/117.90 inference(scs_inference,[],[59,44,71,2])).
% 117.83/117.90 cnf(98,plain,
% 117.83/117.90 (~P9(x981,x981)),
% 117.83/117.90 inference(scs_inference,[],[59,44,46,71,2,64])).
% 117.83/117.90 cnf(100,plain,
% 117.83/117.90 (~P7(f8(f20(x1001,a1,x1002)))),
% 117.83/117.90 inference(scs_inference,[],[59,60,44,53,46,71,2,64,36])).
% 117.83/117.90 cnf(103,plain,
% 117.83/117.90 (E(f17(f6(f4(a1,x1031),f5(x1032,x1033)),x1032),a1)),
% 117.83/117.90 inference(scs_inference,[],[59,60,44,53,49,46,71,2,64,36,3])).
% 117.83/117.90 cnf(105,plain,
% 117.83/117.90 (P1(a1,f4(a1,x1051))),
% 117.83/117.90 inference(scs_inference,[],[59,60,44,53,49,46,71,2,64,36,3,28])).
% 117.83/117.90 cnf(106,plain,
% 117.83/117.90 (P1(x1061,x1061)),
% 117.83/117.90 inference(rename_variables,[],[46])).
% 117.83/117.90 cnf(107,plain,
% 117.83/117.90 (P1(f4(a1,x1071),a1)),
% 117.83/117.90 inference(scs_inference,[],[59,60,44,53,49,46,106,71,2,64,36,3,28,29])).
% 117.83/117.90 cnf(109,plain,
% 117.83/117.90 (P6(a1,f4(a1,x1091))),
% 117.83/117.90 inference(scs_inference,[],[59,60,44,53,49,46,106,47,71,2,64,36,3,28,29,31])).
% 117.83/117.90 cnf(110,plain,
% 117.83/117.90 (P6(x1101,x1101)),
% 117.83/117.90 inference(rename_variables,[],[47])).
% 117.83/117.90 cnf(111,plain,
% 117.83/117.90 (P6(f4(a1,x1111),a1)),
% 117.83/117.90 inference(scs_inference,[],[59,60,44,53,49,46,106,47,110,71,2,64,36,3,28,29,31,32])).
% 117.83/117.90 cnf(113,plain,
% 117.83/117.90 (~P2(f4(a1,x1131))),
% 117.83/117.90 inference(scs_inference,[],[59,60,44,53,49,46,106,47,110,56,71,2,64,36,3,28,29,31,32,33])).
% 117.83/117.90 cnf(114,plain,
% 117.83/117.90 (~E(f6(x1141,f5(x1142,x1143)),a1)),
% 117.83/117.90 inference(scs_inference,[],[59,60,94,44,53,49,46,106,47,110,57,56,71,2,64,36,3,28,29,31,32,33,34])).
% 117.83/117.90 cnf(115,plain,
% 117.83/117.90 (P4(f6(x1151,f5(x1152,x1153)),x1152)),
% 117.83/117.90 inference(rename_variables,[],[94])).
% 117.83/117.90 cnf(116,plain,
% 117.83/117.90 (P4(f6(x1161,f5(f4(a1,x1162),x1163)),a1)),
% 117.83/117.90 inference(scs_inference,[],[59,60,94,115,44,53,49,46,106,47,110,57,56,71,2,64,36,3,28,29,31,32,33,34,35])).
% 117.83/117.90 cnf(123,plain,
% 117.83/117.90 (E(a3,a11)),
% 117.83/117.90 inference(scs_inference,[],[95,105,64,2])).
% 117.83/117.90 cnf(124,plain,
% 117.83/117.90 (P1(f4(a1,x1241),f4(a1,x1242))),
% 117.83/117.90 inference(scs_inference,[],[95,105,107,64,2,66])).
% 117.83/117.90 cnf(126,plain,
% 117.83/117.90 (P4(f6(x1261,f5(a11,x1262)),a3)),
% 117.83/117.90 inference(scs_inference,[],[95,105,107,94,64,2,66,35])).
% 117.83/117.90 cnf(128,plain,
% 117.83/117.90 (~P7(f17(f6(f8(f20(x1281,a1,x1282)),f5(x1283,x1284)),x1283))),
% 117.83/117.90 inference(scs_inference,[],[100,95,105,107,94,49,64,2,66,35,36])).
% 117.83/117.90 cnf(130,plain,
% 117.83/117.90 (P6(f4(a1,x1301),f4(a1,x1302))),
% 117.83/117.90 inference(scs_inference,[],[100,95,97,105,107,111,94,49,64,2,66,35,36,32])).
% 117.83/117.90 cnf(131,plain,
% 117.83/117.90 (~P2(f17(f6(f4(a1,x1311),f5(x1312,x1313)),x1312))),
% 117.83/117.90 inference(scs_inference,[],[100,95,103,97,105,107,111,94,49,56,64,2,66,35,36,32,33])).
% 117.83/117.90 cnf(132,plain,
% 117.83/117.90 (P1(a3,a11)),
% 117.83/117.90 inference(scs_inference,[],[100,95,103,97,105,107,111,94,49,56,46,64,2,66,35,36,32,33,28])).
% 117.83/117.90 cnf(133,plain,
% 117.83/117.90 (P1(x1331,x1331)),
% 117.83/117.90 inference(rename_variables,[],[46])).
% 117.83/117.90 cnf(134,plain,
% 117.83/117.90 (P1(a11,a3)),
% 117.83/117.90 inference(scs_inference,[],[100,95,103,97,105,107,111,94,49,56,46,133,64,2,66,35,36,32,33,28,29])).
% 117.83/117.90 cnf(136,plain,
% 117.83/117.90 (P6(a3,a11)),
% 117.83/117.90 inference(scs_inference,[],[100,95,103,97,105,107,111,94,49,47,56,46,133,64,2,66,35,36,32,33,28,29,31])).
% 117.83/117.90 cnf(138,plain,
% 117.83/117.90 (E(f16(f6(x1381,f5(x1382,a11)),x1382),a3)),
% 117.83/117.90 inference(scs_inference,[],[100,95,103,97,105,107,111,50,94,49,47,56,46,133,64,2,66,35,36,32,33,28,29,31,3])).
% 117.83/117.90 cnf(143,plain,
% 117.83/117.90 (E(a3,f16(f6(x1431,f5(x1432,a11)),x1432))),
% 117.83/117.90 inference(scs_inference,[],[107,138,64,2])).
% 117.83/117.90 cnf(144,plain,
% 117.83/117.90 (P4(f6(x1441,f5(f4(a1,x1442),x1443)),f4(a1,x1444))),
% 117.83/117.90 inference(scs_inference,[],[107,138,97,116,64,2,35])).
% 117.83/117.90 cnf(145,plain,
% 117.83/117.90 (P6(a11,a3)),
% 117.83/117.90 inference(scs_inference,[],[95,107,138,97,116,47,64,2,35,32])).
% 117.83/117.90 cnf(147,plain,
% 117.83/117.90 (~P7(f17(f6(f20(a9,a10,a11),f5(x1471,x1472)),x1471))),
% 117.83/117.90 inference(scs_inference,[],[59,95,107,138,97,49,116,47,64,2,35,32,36])).
% 117.83/117.90 cnf(149,plain,
% 117.83/117.90 (~E(f6(x1491,f5(x1492,x1493)),f17(f6(f4(a1,x1494),f5(x1495,x1496)),x1495))),
% 117.83/117.91 inference(scs_inference,[],[59,95,107,138,103,97,49,116,114,47,64,2,35,32,36,3])).
% 117.83/117.91 cnf(150,plain,
% 117.83/117.91 (E(f4(a1,x1501),f4(a1,x1502))),
% 117.83/117.91 inference(scs_inference,[],[59,95,107,138,103,97,49,116,114,57,47,64,2,35,32,36,3,77])).
% 117.83/117.91 cnf(155,plain,
% 117.83/117.91 (P1(x1551,x1552)+~E(a2,x1551)),
% 117.83/117.91 inference(scs_inference,[],[59,95,107,138,103,97,49,116,45,114,57,47,64,2,35,32,36,3,77,30,33,28])).
% 117.83/117.91 cnf(157,plain,
% 117.83/117.91 (~P9(a3,a11)),
% 117.83/117.91 inference(scs_inference,[],[134,64])).
% 117.83/117.91 cnf(159,plain,
% 117.83/117.91 (E(a1,f17(f6(f4(a1,x1591),f5(x1592,x1593)),x1592))),
% 117.83/117.91 inference(scs_inference,[],[134,103,64,2])).
% 117.83/117.91 cnf(160,plain,
% 117.83/117.91 (E(f17(f6(f4(a1,x1601),f5(x1602,x1603)),x1602),f4(a1,x1604))),
% 117.83/117.91 inference(scs_inference,[],[134,103,97,64,2,3])).
% 117.83/117.91 cnf(164,plain,
% 117.83/117.91 (~P9(a11,a3)),
% 117.83/117.91 inference(scs_inference,[],[132,64])).
% 117.83/117.91 cnf(166,plain,
% 117.83/117.91 (E(f20(x1661,a1,a3),f8(f20(x1661,a1,x1662)))),
% 117.83/117.91 inference(scs_inference,[],[132,53,64,2])).
% 117.83/117.91 cnf(167,plain,
% 117.83/117.91 (P1(a11,f16(f6(x1671,f5(x1672,a11)),x1672))),
% 117.83/117.91 inference(scs_inference,[],[134,132,53,143,64,2,29])).
% 117.83/117.91 cnf(168,plain,
% 117.83/117.91 (P6(f16(f6(x1681,f5(x1682,a11)),x1682),a11)),
% 117.83/117.91 inference(scs_inference,[],[134,132,136,53,143,64,2,29,31])).
% 117.83/117.91 cnf(169,plain,
% 117.83/117.91 (P4(f6(x1691,f5(a11,x1692)),f16(f6(x1693,f5(x1694,a11)),x1694))),
% 117.83/117.91 inference(scs_inference,[],[134,132,136,53,143,126,64,2,29,31,35])).
% 117.83/117.91 cnf(170,plain,
% 117.83/117.91 (P6(a11,f16(f6(x1701,f5(x1702,a11)),x1702))),
% 117.83/117.91 inference(scs_inference,[],[134,132,136,145,53,143,126,64,2,29,31,35,32])).
% 117.83/117.91 cnf(171,plain,
% 117.83/117.91 (P1(f16(f6(x1711,f5(x1712,a11)),x1712),a11)),
% 117.83/117.91 inference(scs_inference,[],[134,132,136,145,53,143,126,64,2,29,31,35,32,28])).
% 117.83/117.91 cnf(172,plain,
% 117.83/117.91 (P3(f8(f20(x1721,a1,x1722)))),
% 117.83/117.91 inference(scs_inference,[],[134,132,136,145,53,143,126,52,64,2,29,31,35,32,28,30])).
% 117.83/117.91 cnf(174,plain,
% 117.83/117.91 (E(f17(f6(a11,f5(x1741,x1742)),x1741),a3)),
% 117.83/117.91 inference(scs_inference,[],[95,134,132,136,145,53,49,143,126,52,64,2,29,31,35,32,28,30,3])).
% 117.83/117.91 cnf(176,plain,
% 117.83/117.91 (P1(a3,f16(f6(x1761,f5(x1762,a11)),x1762))),
% 117.83/117.91 inference(scs_inference,[],[95,134,132,136,145,53,49,143,126,52,64,2,29,31,35,32,28,30,3,66])).
% 117.83/117.91 cnf(188,plain,
% 117.83/117.91 (E(f4(a1,x1881),f17(f6(f4(a1,x1882),f5(x1883,x1884)),x1883))),
% 117.83/117.91 inference(scs_inference,[],[160,167,64,2])).
% 117.83/117.91 cnf(189,plain,
% 117.83/117.91 (P1(f16(f6(x1891,f5(x1892,a11)),x1892),a3)),
% 117.83/117.91 inference(scs_inference,[],[95,160,167,171,64,2,29])).
% 117.83/117.91 cnf(191,plain,
% 117.83/117.91 (P6(f16(f6(x1911,f5(x1912,a11)),x1912),a3)),
% 117.83/117.91 inference(scs_inference,[],[95,160,167,168,170,171,64,2,29,31,32])).
% 117.83/117.91 cnf(192,plain,
% 117.83/117.91 (~E(f6(x1921,f5(x1922,x1923)),f4(a1,x1924))),
% 117.83/117.91 inference(scs_inference,[],[95,44,160,167,168,170,171,114,64,2,29,31,32,3])).
% 117.83/117.91 cnf(200,plain,
% 117.83/117.91 (E(x2001,f17(f6(x2001,f5(x2002,x2003)),x2002))),
% 117.83/117.91 inference(scs_inference,[],[49,171,64,2])).
% 117.83/117.91 cnf(201,plain,
% 117.83/117.91 (P1(f17(f6(a2,f5(x2011,x2012)),x2011),x2013)),
% 117.83/117.91 inference(scs_inference,[],[49,171,45,64,2,28])).
% 117.83/117.91 cnf(202,plain,
% 117.83/117.91 (E(f8(f20(x2021,a1,x2022)),f8(f20(x2021,a1,x2023)))),
% 117.83/117.91 inference(scs_inference,[],[53,49,166,171,45,64,2,28,3])).
% 117.83/117.91 cnf(211,plain,
% 117.83/117.91 (~P9(a3,f16(f6(x2111,f5(x2112,a11)),x2112))),
% 117.83/117.91 inference(scs_inference,[],[189,64])).
% 117.83/117.91 cnf(213,plain,
% 117.83/117.91 (E(a3,f17(f6(a11,f5(x2131,x2132)),x2131))),
% 117.83/117.91 inference(scs_inference,[],[189,174,64,2])).
% 117.83/117.91 cnf(214,plain,
% 117.83/117.91 (P4(f6(x2141,f5(a11,x2142)),f17(f6(a3,f5(x2143,x2144)),x2143))),
% 117.83/117.91 inference(scs_inference,[],[189,200,174,126,64,2,35])).
% 117.83/117.91 cnf(215,plain,
% 117.83/117.91 (E(x2151,f17(f6(x2151,f5(x2152,x2153)),x2152))),
% 117.83/117.91 inference(rename_variables,[],[200])).
% 117.83/117.91 cnf(216,plain,
% 117.83/117.91 (P6(f17(f6(a3,f5(x2161,x2162)),x2161),a11)),
% 117.83/117.91 inference(scs_inference,[],[136,189,200,215,174,126,64,2,35,31])).
% 117.83/117.91 cnf(217,plain,
% 117.83/117.91 (E(x2171,f17(f6(x2171,f5(x2172,x2173)),x2172))),
% 117.83/117.91 inference(rename_variables,[],[200])).
% 117.83/117.91 cnf(218,plain,
% 117.83/117.91 (P1(a11,f17(f6(a3,f5(x2181,x2182)),x2181))),
% 117.83/117.91 inference(scs_inference,[],[134,136,189,200,215,217,174,126,64,2,35,31,29])).
% 117.83/117.91 cnf(219,plain,
% 117.83/117.91 (E(x2191,f17(f6(x2191,f5(x2192,x2193)),x2192))),
% 117.83/117.91 inference(rename_variables,[],[200])).
% 117.83/117.91 cnf(220,plain,
% 117.83/117.91 (P6(a11,f17(f6(a3,f5(x2201,x2202)),x2201))),
% 117.83/117.91 inference(scs_inference,[],[134,136,145,189,200,215,217,219,174,126,64,2,35,31,29,32])).
% 117.83/117.91 cnf(221,plain,
% 117.83/117.91 (E(x2211,f17(f6(x2211,f5(x2212,x2213)),x2212))),
% 117.83/117.91 inference(rename_variables,[],[200])).
% 117.83/117.91 cnf(222,plain,
% 117.83/117.91 (P1(f17(f6(a3,f5(x2221,x2222)),x2221),a11)),
% 117.83/117.91 inference(scs_inference,[],[134,132,136,145,189,200,215,217,219,221,174,126,64,2,35,31,29,32,28])).
% 117.83/117.91 cnf(223,plain,
% 117.83/117.91 (E(x2231,f17(f6(x2231,f5(x2232,x2233)),x2232))),
% 117.83/117.91 inference(rename_variables,[],[200])).
% 117.83/117.91 cnf(224,plain,
% 117.83/117.91 (P2(f17(f6(f6(x2241,f5(x2242,x2243)),f5(x2244,x2245)),x2244))),
% 117.83/117.91 inference(scs_inference,[],[134,132,136,145,189,200,215,217,219,221,223,174,126,48,64,2,35,31,29,32,28,33])).
% 117.83/117.91 cnf(225,plain,
% 117.83/117.91 (E(x2251,f17(f6(x2251,f5(x2252,x2253)),x2252))),
% 117.83/117.91 inference(rename_variables,[],[200])).
% 117.83/117.91 cnf(226,plain,
% 117.83/117.91 (P3(f17(f6(f8(f20(x2261,a1,x2262)),f5(x2263,x2264)),x2263))),
% 117.83/117.91 inference(scs_inference,[],[134,132,136,145,189,200,215,217,219,221,223,225,172,174,126,48,64,2,35,31,29,32,28,33,30])).
% 117.83/117.91 cnf(227,plain,
% 117.83/117.91 (E(x2271,f17(f6(x2271,f5(x2272,x2273)),x2272))),
% 117.83/117.91 inference(rename_variables,[],[200])).
% 117.83/117.91 cnf(228,plain,
% 117.83/117.91 (E(f17(f6(f8(f20(x2281,a1,x2282)),f5(x2283,x2284)),x2283),f20(x2281,a1,a3))),
% 117.83/117.91 inference(scs_inference,[],[134,132,136,145,53,189,49,200,215,217,219,221,223,225,172,174,126,48,64,2,35,31,29,32,28,33,30,3])).
% 117.83/117.91 cnf(230,plain,
% 117.83/117.91 (P7(f17(f6(f13(f20(a9,a10,a11),a12),f5(x2301,x2302)),x2301))),
% 117.83/117.91 inference(scs_inference,[],[54,134,132,136,145,53,189,49,200,215,217,219,221,223,225,227,172,174,126,48,64,2,35,31,29,32,28,33,30,3,36])).
% 117.83/117.91 cnf(234,plain,
% 117.83/117.91 (E(a11,f17(f6(a3,f5(x2341,x2342)),x2341))),
% 117.83/117.91 inference(scs_inference,[],[54,134,132,136,145,53,189,49,200,215,217,219,221,223,225,227,172,174,126,48,57,64,2,35,31,29,32,28,33,30,3,36,66,77])).
% 117.83/117.91 cnf(241,plain,
% 117.83/117.91 (E(f20(x2411,a1,a3),f17(f6(f8(f20(x2411,a1,x2412)),f5(x2413,x2414)),x2413))),
% 117.83/117.91 inference(scs_inference,[],[201,228,64,2])).
% 117.83/117.91 cnf(243,plain,
% 117.83/117.91 (P6(f17(f6(a11,f5(x2431,x2432)),x2431),a11)),
% 117.83/117.91 inference(scs_inference,[],[136,201,228,213,126,64,2,35,31])).
% 117.83/117.91 cnf(244,plain,
% 117.83/117.91 (P1(a11,f17(f6(a11,f5(x2441,x2442)),x2441))),
% 117.83/117.91 inference(scs_inference,[],[134,136,201,228,213,126,64,2,35,31,29])).
% 117.83/117.91 cnf(245,plain,
% 117.83/117.91 (P6(a11,f17(f6(a11,f5(x2451,x2452)),x2451))),
% 117.83/117.91 inference(scs_inference,[],[134,136,145,201,228,213,126,64,2,35,31,29,32])).
% 117.83/117.91 cnf(246,plain,
% 117.83/117.91 (P1(f17(f6(a11,f5(x2461,x2462)),x2461),a11)),
% 117.83/117.91 inference(scs_inference,[],[134,132,136,145,201,228,213,126,64,2,35,31,29,32,28])).
% 117.83/117.91 cnf(247,plain,
% 117.83/117.91 (E(f17(f6(f7(f20(x2471,a1,x2472)),f5(x2473,x2474)),x2473),a2)),
% 117.83/117.91 inference(scs_inference,[],[134,132,136,145,49,201,228,213,51,126,64,2,35,31,29,32,28,3])).
% 117.83/117.91 cnf(249,plain,
% 117.83/117.91 (P1(a3,f17(f6(a11,f5(x2491,x2492)),x2491))),
% 117.83/117.91 inference(scs_inference,[],[134,132,136,145,49,201,228,213,51,126,64,2,35,31,29,32,28,3,66])).
% 117.83/117.91 cnf(258,plain,
% 117.83/117.91 (E(a2,f17(f6(f7(f20(x2581,a1,x2582)),f5(x2583,x2584)),x2583))),
% 117.83/117.91 inference(scs_inference,[],[218,247,64,2])).
% 117.83/117.91 cnf(260,plain,
% 117.83/117.91 (P1(f17(f6(a3,f5(x2601,x2602)),x2601),a3)),
% 117.83/117.91 inference(scs_inference,[],[95,218,222,247,220,64,2,31,29])).
% 117.83/117.91 cnf(262,plain,
% 117.83/117.91 (E(f8(f20(x2621,a1,x2622)),f17(f6(f8(f20(x2621,a1,x2623)),f5(x2624,x2625)),x2624))),
% 117.83/117.91 inference(scs_inference,[],[95,53,218,222,241,247,216,220,64,2,31,29,32,3])).
% 117.83/117.91 cnf(264,plain,
% 117.83/117.91 (P1(f17(f6(f7(f20(x2641,a1,x2642)),f5(x2643,x2644)),x2643),x2645)),
% 117.83/117.91 inference(scs_inference,[],[95,53,218,222,241,247,216,220,64,2,31,29,32,3,155])).
% 117.83/117.91 cnf(270,plain,
% 117.83/117.91 (E(f17(f6(f8(f20(x2701,a1,x2702)),f5(x2703,x2704)),x2703),f8(f20(x2701,a1,x2705)))),
% 117.83/117.91 inference(scs_inference,[],[244,262,64,2])).
% 117.83/117.91 cnf(272,plain,
% 117.83/117.91 (P1(f17(f6(a11,f5(x2721,x2722)),x2721),a3)),
% 117.83/117.91 inference(scs_inference,[],[95,244,246,262,245,64,2,31,29])).
% 117.83/117.91 cnf(273,plain,
% 117.83/117.91 (P1(f7(f20(x2731,a1,x2732)),x2733)),
% 117.83/117.91 inference(scs_inference,[],[95,49,244,246,264,262,245,64,2,31,29,28])).
% 117.83/117.91 cnf(276,plain,
% 117.83/117.91 (P6(f17(f6(a11,f5(x2761,x2762)),x2761),a3)),
% 117.83/117.91 inference(scs_inference,[],[95,49,244,246,264,262,243,245,64,2,31,29,28,32])).
% 117.83/117.91 cnf(282,plain,
% 117.83/117.91 (E(a2,f7(f20(x2821,a1,x2822)))),
% 117.83/117.91 inference(scs_inference,[],[260,51,64,2])).
% 117.83/117.91 cnf(283,plain,
% 117.83/117.91 (E(f17(f6(a2,f5(x2831,x2832)),x2831),f7(f20(x2833,a1,x2834)))),
% 117.83/117.91 inference(scs_inference,[],[49,260,51,64,2,3])).
% 117.83/117.91 cnf(300,plain,
% 117.83/117.91 (E(f17(f6(a3,f5(x3001,x3002)),x3001),a11)),
% 117.83/117.91 inference(scs_inference,[],[246,234,64,2])).
% 117.83/117.91 cnf(304,plain,
% 117.83/117.91 (~P9(x3041,f7(f20(x3042,a1,x3043)))),
% 117.83/117.91 inference(scs_inference,[],[273,64])).
% 117.83/117.91 cnf(306,plain,
% 117.83/117.91 (E(f13(f20(x3061,x3062,x3063),x3064),f20(f15(x3061,x3064),f6(x3062,f5(x3064,a2)),x3063))),
% 117.83/117.91 inference(scs_inference,[],[273,55,64,2])).
% 117.83/117.91 cnf(307,plain,
% 117.83/117.91 (P7(f20(f15(a9,a12),f6(a10,f5(a12,a2)),a11))),
% 117.83/117.91 inference(scs_inference,[],[54,273,55,64,2,36])).
% 117.83/117.91 cnf(312,plain,
% 117.83/117.91 (E(x3121,f16(f6(x3122,f5(x3123,x3121)),x3123))),
% 117.83/117.91 inference(scs_inference,[],[272,50,64,2])).
% 117.83/117.91 cnf(313,plain,
% 117.83/117.91 (E(a11,f16(f6(x3131,f5(x3132,a3)),x3132))),
% 117.83/117.91 inference(scs_inference,[],[95,272,50,64,2,3])).
% 117.83/117.91 cnf(345,plain,
% 117.83/117.91 (~P9(f17(f6(a11,f5(x3451,x3452)),x3451),a3)),
% 117.83/117.91 inference(scs_inference,[],[249,64])).
% 117.83/117.91 cnf(355,plain,
% 117.83/117.91 (~P9(f16(f6(x3551,f5(x3552,a11)),x3552),a3)),
% 117.83/117.91 inference(scs_inference,[],[176,64])).
% 117.83/117.91 cnf(380,plain,
% 117.83/117.91 (P6(f17(f6(f4(a1,x3801),f5(x3802,x3803)),x3802),a1)),
% 117.83/117.91 inference(scs_inference,[],[200,111,31])).
% 117.83/117.91 cnf(381,plain,
% 117.83/117.91 (E(x3811,f17(f6(x3811,f5(x3812,x3813)),x3812))),
% 117.83/117.91 inference(rename_variables,[],[200])).
% 117.83/117.91 cnf(383,plain,
% 117.83/117.91 (E(x3831,f17(f6(x3831,f5(x3832,x3833)),x3832))),
% 117.83/117.91 inference(rename_variables,[],[200])).
% 117.83/117.91 cnf(384,plain,
% 117.83/117.91 (P1(f17(f6(a1,f5(x3841,x3842)),x3841),f4(a1,x3843))),
% 117.83/117.91 inference(scs_inference,[],[105,200,381,383,111,31,29,28])).
% 117.83/117.91 cnf(385,plain,
% 117.83/117.91 (E(x3851,f17(f6(x3851,f5(x3852,x3853)),x3852))),
% 117.83/117.91 inference(rename_variables,[],[200])).
% 117.83/117.91 cnf(386,plain,
% 117.83/117.91 (P6(f4(a1,x3861),f17(f6(a1,f5(x3862,x3863)),x3862))),
% 117.83/117.91 inference(scs_inference,[],[105,200,381,383,385,111,31,29,28,32])).
% 117.83/117.91 cnf(388,plain,
% 117.83/117.91 (~P9(f17(f6(f4(a1,x3881),f5(x3882,x3883)),x3882),a1)),
% 117.83/117.91 inference(scs_inference,[],[105,200,381,383,385,111,31,29,28,32,64])).
% 117.83/117.91 cnf(403,plain,
% 117.83/117.91 (P6(f17(f6(f4(a1,x4031),f5(x4032,x4033)),x4032),f4(a1,x4034))),
% 117.83/117.91 inference(scs_inference,[],[97,44,384,386,380,64,31,29,32])).
% 117.83/117.91 cnf(430,plain,
% 117.83/117.91 (P6(f4(a1,x4301),f17(f6(f4(a1,x4302),f5(x4303,x4304)),x4303))),
% 117.83/117.91 inference(scs_inference,[],[200,130,32])).
% 117.83/117.91 cnf(431,plain,
% 117.83/117.91 (E(x4311,f17(f6(x4311,f5(x4312,x4313)),x4312))),
% 117.83/117.91 inference(rename_variables,[],[200])).
% 117.83/117.91 cnf(436,plain,
% 117.83/117.91 (P1(f17(f6(f4(a1,x4361),f5(x4362,x4363)),x4362),f4(a1,x4364))),
% 117.83/117.91 inference(scs_inference,[],[97,200,431,107,130,32,28,64,29])).
% 117.83/117.91 cnf(468,plain,
% 117.83/117.91 (E(f7(f20(x4681,a1,x4682)),f7(f20(x4683,a1,x4684)))),
% 117.83/117.91 inference(scs_inference,[],[282,51,3])).
% 117.83/117.91 cnf(495,plain,
% 117.83/117.91 (E(f4(a1,x4951),f16(f6(x4952,f5(x4953,a1)),x4953))),
% 117.83/117.91 inference(scs_inference,[],[44,312,3])).
% 117.83/117.91 cnf(497,plain,
% 117.83/117.91 (E(f16(f6(x4971,f5(x4972,a1)),x4972),f4(a1,x4973))),
% 117.83/117.91 inference(scs_inference,[],[44,312,3,2])).
% 117.83/117.91 cnf(498,plain,
% 117.83/117.91 (~P2(f16(f6(x4981,f5(x4982,a1)),x4982))),
% 117.83/117.91 inference(scs_inference,[],[44,312,113,3,2,33])).
% 117.83/117.91 cnf(505,plain,
% 117.83/117.91 (~E(f6(x5051,f5(x5052,x5053)),f16(f6(x5054,f5(x5055,a1)),x5055))),
% 117.83/117.91 inference(scs_inference,[],[192,497,3])).
% 117.83/117.91 cnf(519,plain,
% 117.83/117.91 (P6(x5191,f17(f6(x5191,f5(x5192,x5193)),x5192))),
% 117.83/117.91 inference(scs_inference,[],[49,47,31])).
% 117.83/117.91 cnf(520,plain,
% 117.83/117.91 (P6(x5201,x5201)),
% 117.83/117.91 inference(rename_variables,[],[47])).
% 117.83/117.91 cnf(521,plain,
% 117.83/117.91 (P6(f17(f6(x5211,f5(x5212,x5213)),x5212),x5211)),
% 117.83/117.91 inference(scs_inference,[],[49,47,520,31,32])).
% 117.83/117.91 cnf(523,plain,
% 117.83/117.91 (E(f17(f6(f20(x5231,a1,a3),f5(x5232,x5233)),x5232),f8(f20(x5231,a1,x5234)))),
% 117.83/117.91 inference(scs_inference,[],[49,166,47,520,31,32,3])).
% 117.83/117.91 cnf(524,plain,
% 117.83/117.91 (E(f17(f6(x5241,f5(x5242,x5243)),x5242),x5241)),
% 117.83/117.91 inference(rename_variables,[],[49])).
% 117.83/117.91 cnf(525,plain,
% 117.83/117.91 (P1(f17(f6(x5251,f5(x5252,x5253)),x5252),x5251)),
% 117.83/117.91 inference(scs_inference,[],[49,524,166,46,47,520,31,32,3,29])).
% 117.83/117.91 cnf(526,plain,
% 117.83/117.91 (P1(x5261,x5261)),
% 117.83/117.91 inference(rename_variables,[],[46])).
% 117.83/117.91 cnf(527,plain,
% 117.83/117.91 (P1(x5271,f17(f6(x5271,f5(x5272,x5273)),x5272))),
% 117.83/117.91 inference(scs_inference,[],[49,524,166,46,526,47,520,31,32,3,29,28])).
% 117.83/117.91 cnf(529,plain,
% 117.83/117.91 (~P7(f17(f6(f20(x5291,a1,a3),f5(x5292,x5293)),x5292))),
% 117.83/117.91 inference(scs_inference,[],[49,524,100,166,46,526,47,520,31,32,3,29,28,36])).
% 117.83/117.91 cnf(530,plain,
% 117.83/117.91 (E(f8(f20(x5301,a1,x5302)),f17(f6(f20(x5301,a1,a3),f5(x5303,x5304)),x5303))),
% 117.83/117.91 inference(scs_inference,[],[49,524,100,166,46,526,47,520,31,32,3,29,28,36,2])).
% 117.83/117.91 cnf(534,plain,
% 117.83/117.91 (~P9(x5341,f17(f6(x5341,f5(x5342,x5343)),x5342))),
% 117.83/117.91 inference(scs_inference,[],[525,64])).
% 117.83/117.91 cnf(544,plain,
% 117.83/117.91 (~P9(f17(f6(x5441,f5(x5442,x5443)),x5442),x5441)),
% 117.83/117.91 inference(scs_inference,[],[527,64])).
% 117.83/117.91 cnf(550,plain,
% 117.83/117.91 (P6(a1,f8(f13(f4(a1,x5501),x5502)))),
% 117.83/117.91 inference(scs_inference,[],[109,63,67])).
% 117.83/117.91 cnf(551,plain,
% 117.83/117.91 (P6(f20(x5511,a1,a3),f8(f20(x5511,a1,x5512)))),
% 117.83/117.91 inference(scs_inference,[],[228,521,31])).
% 117.83/117.91 cnf(553,plain,
% 117.83/117.91 (P6(f8(f20(x5531,a1,x5532)),f20(x5531,a1,a3))),
% 117.83/117.91 inference(scs_inference,[],[228,519,521,31,32])).
% 117.83/117.91 cnf(557,plain,
% 117.83/117.91 (P1(f8(f20(x5571,a1,x5572)),f20(x5571,a1,a3))),
% 117.83/117.91 inference(scs_inference,[],[50,282,228,527,519,521,31,32,3,29])).
% 117.83/117.91 cnf(559,plain,
% 117.83/117.91 (P1(f20(x5591,a1,a3),f8(f20(x5591,a1,x5592)))),
% 117.83/117.91 inference(scs_inference,[],[50,282,228,527,519,521,525,31,32,3,29,28])).
% 117.83/117.91 cnf(561,plain,
% 117.83/117.91 (~P9(f20(x5611,a1,a3),f8(f20(x5611,a1,x5612)))),
% 117.83/117.91 inference(scs_inference,[],[50,282,228,527,519,521,525,31,32,3,29,28,64])).
% 117.83/117.91 cnf(568,plain,
% 117.83/117.91 (~P9(f8(f20(x5681,a1,x5682)),f20(x5681,a1,a3))),
% 117.83/117.91 inference(scs_inference,[],[559,64])).
% 117.83/117.91 cnf(571,plain,
% 117.83/117.91 (P6(f8(f20(x5711,a1,x5712)),f20(x5711,a1,a3))),
% 117.83/117.91 inference(rename_variables,[],[553])).
% 117.83/117.91 cnf(572,plain,
% 117.83/117.91 (P6(f8(f20(x5721,a1,x5722)),f8(f20(x5721,a1,x5723)))),
% 117.83/117.91 inference(scs_inference,[],[166,262,553,571,559,64,31,32])).
% 117.83/117.91 cnf(574,plain,
% 117.83/117.91 (P1(f8(f20(x5741,a1,x5742)),f8(f20(x5741,a1,x5743)))),
% 117.83/117.91 inference(scs_inference,[],[166,262,553,571,557,559,64,31,32,29])).
% 117.83/117.91 cnf(575,plain,
% 117.83/117.91 (P1(f8(f20(x5751,a1,x5752)),f20(x5751,a1,a3))),
% 117.83/117.91 inference(rename_variables,[],[557])).
% 117.83/117.91 cnf(576,plain,
% 117.83/117.91 (P1(f17(f6(f8(f20(x5761,a1,x5762)),f5(x5763,x5764)),x5763),f20(x5761,a1,a3))),
% 117.83/117.91 inference(scs_inference,[],[166,262,553,571,557,575,559,64,31,32,29,28])).
% 117.83/117.91 cnf(586,plain,
% 117.83/117.91 (P6(f17(f6(f8(f20(x5861,a1,x5862)),f5(x5863,x5864)),x5863),f8(f20(x5861,a1,x5865)))),
% 117.83/117.91 inference(scs_inference,[],[262,572,574,64,31])).
% 117.83/117.91 cnf(597,plain,
% 117.83/117.91 (P6(x5971,f16(f6(x5972,f5(x5973,x5971)),x5973))),
% 117.83/117.91 inference(scs_inference,[],[50,576,47,64,31])).
% 117.83/117.91 cnf(601,plain,
% 117.83/117.91 (P1(f8(f20(x6011,a1,x6012)),f17(f6(f8(f20(x6011,a1,x6013)),f5(x6014,x6015)),x6014))),
% 117.83/117.91 inference(scs_inference,[],[50,262,576,551,574,47,64,31,32,29])).
% 117.83/117.91 cnf(603,plain,
% 117.83/117.91 (P1(x6031,f16(f6(x6032,f5(x6033,x6031)),x6033))),
% 117.83/117.91 inference(scs_inference,[],[50,262,576,551,574,46,47,64,31,32,29,28])).
% 117.83/117.91 cnf(606,plain,
% 117.83/117.91 (~P9(f16(f6(x6061,f5(x6062,x6063)),x6062),x6063)),
% 117.83/117.91 inference(scs_inference,[],[603,64])).
% 117.83/117.91 cnf(609,plain,
% 117.83/117.91 (P6(f16(f6(x6091,f5(x6092,x6093)),x6092),x6093)),
% 117.83/117.91 inference(scs_inference,[],[50,97,603,47,550,64,31,32])).
% 117.83/117.91 cnf(611,plain,
% 117.83/117.91 (P1(f16(f6(x6111,f5(x6112,x6113)),x6112),x6113)),
% 117.83/117.91 inference(scs_inference,[],[50,97,603,46,47,550,64,31,32,29])).
% 117.83/117.91 cnf(626,plain,
% 117.83/117.91 (P6(f17(f6(f7(f20(x6261,a1,x6262)),f5(x6263,x6264)),x6263),a2)),
% 117.83/117.91 inference(scs_inference,[],[51,519,521,31,32])).
% 117.83/117.91 cnf(631,plain,
% 117.83/117.91 (P6(f7(f20(x6311,a1,x6312)),a2)),
% 117.83/117.91 inference(scs_inference,[],[283,521,31])).
% 117.83/117.91 cnf(637,plain,
% 117.83/117.91 (~P5(f20(x6371,f17(f6(f4(a1,x6372),f5(x6373,x6374)),x6373),x6375),x6376)),
% 117.83/117.91 inference(scs_inference,[],[57,103,82,34])).
% 117.83/117.91 cnf(638,plain,
% 117.83/117.91 (E(f5(a3,x6381),f5(a11,x6381))),
% 117.83/117.91 inference(scs_inference,[],[95,6,2])).
% 117.83/117.91 cnf(639,plain,
% 117.83/117.91 (E(f5(a11,x6391),f5(a3,x6391))),
% 117.83/117.91 inference(scs_inference,[],[638,2])).
% 117.83/117.91 cnf(640,plain,
% 117.83/117.91 (E(f17(f6(f5(a3,x6401),f5(x6402,x6403)),x6402),f5(a11,x6401))),
% 117.83/117.91 inference(scs_inference,[],[49,638,2,3])).
% 117.83/117.91 cnf(647,plain,
% 117.83/117.91 (E(f17(f6(f5(a11,x6471),f5(x6472,x6473)),x6472),f5(a3,x6471))),
% 117.83/117.91 inference(scs_inference,[],[49,640,639,2,3])).
% 117.83/117.91 cnf(656,plain,
% 117.83/117.91 (E(f5(x6561,a3),f5(x6561,a11))),
% 117.83/117.91 inference(scs_inference,[],[95,7,2])).
% 117.83/117.91 cnf(657,plain,
% 117.83/117.91 (E(f5(x6571,a11),f5(x6571,a3))),
% 117.83/117.91 inference(scs_inference,[],[656,2])).
% 117.83/117.91 cnf(658,plain,
% 117.83/117.91 (E(f17(f6(f5(x6581,a3),f5(x6582,x6583)),x6582),f5(x6581,a11))),
% 117.83/117.91 inference(scs_inference,[],[49,656,2,3])).
% 117.83/117.91 cnf(665,plain,
% 117.83/117.91 (E(f5(x6651,a11),f17(f6(f5(x6651,a3),f5(x6652,x6653)),x6652))),
% 117.83/117.91 inference(scs_inference,[],[658,2])).
% 117.83/117.91 cnf(666,plain,
% 117.83/117.91 (E(f17(f6(f5(x6661,a11),f5(x6662,x6663)),x6662),f5(x6661,a3))),
% 117.83/117.91 inference(scs_inference,[],[49,658,657,2,3])).
% 117.83/117.91 cnf(671,plain,
% 117.83/117.91 (E(f5(x6711,a3),f17(f6(f5(x6711,a11),f5(x6712,x6713)),x6712))),
% 117.83/117.91 inference(scs_inference,[],[666,2])).
% 117.83/117.91 cnf(804,plain,
% 117.83/117.91 (P6(f13(f20(x8041,x8042,x8043),x8044),f20(f15(x8041,x8044),f6(x8042,f5(x8044,a2)),x8043))),
% 117.83/117.91 inference(scs_inference,[],[55,47,31])).
% 117.83/117.91 cnf(805,plain,
% 117.83/117.91 (P6(x8051,x8051)),
% 117.83/117.91 inference(rename_variables,[],[47])).
% 117.83/117.91 cnf(806,plain,
% 117.83/117.91 (P6(f20(f15(x8061,x8062),f6(x8063,f5(x8062,a2)),x8064),f13(f20(x8061,x8063,x8064),x8062))),
% 117.83/117.91 inference(scs_inference,[],[55,47,805,31,32])).
% 117.83/117.91 cnf(809,plain,
% 117.83/117.91 (P1(x8091,x8091)),
% 117.83/117.91 inference(rename_variables,[],[46])).
% 117.83/117.91 cnf(810,plain,
% 117.83/117.91 (P1(f13(f20(x8101,x8102,x8103),x8104),f20(f15(x8101,x8104),f6(x8102,f5(x8104,a2)),x8103))),
% 117.83/117.91 inference(scs_inference,[],[55,46,809,47,805,31,32,29,28])).
% 117.83/117.91 cnf(814,plain,
% 117.83/117.91 (~P9(f20(f15(x8141,x8142),f6(x8143,f5(x8142,a2)),x8144),f13(f20(x8141,x8143,x8144),x8142))),
% 117.83/117.91 inference(scs_inference,[],[810,64])).
% 117.83/117.91 cnf(816,plain,
% 117.83/117.91 (E(f6(a3,x8161),f6(a11,x8161))),
% 117.83/117.91 inference(scs_inference,[],[95,8,2])).
% 117.83/117.91 cnf(817,plain,
% 117.83/117.91 (E(f6(a11,x8171),f6(a3,x8171))),
% 117.83/117.91 inference(scs_inference,[],[816,2])).
% 117.83/117.91 cnf(818,plain,
% 117.83/117.91 (E(f17(f6(f6(a3,x8181),f5(x8182,x8183)),x8182),f6(a11,x8181))),
% 117.83/117.91 inference(scs_inference,[],[49,816,2,3])).
% 117.83/117.91 cnf(822,plain,
% 117.83/117.91 (E(f6(a11,x8221),f17(f6(f6(a3,x8221),f5(x8222,x8223)),x8222))),
% 117.83/117.91 inference(scs_inference,[],[818,2])).
% 117.83/117.91 cnf(823,plain,
% 117.83/117.91 (E(f17(f6(f6(a11,x8231),f5(x8232,x8233)),x8232),f6(a3,x8231))),
% 117.83/117.91 inference(scs_inference,[],[49,818,817,2,3])).
% 117.83/117.91 cnf(828,plain,
% 117.83/117.91 (E(f6(a3,x8281),f17(f6(f6(a11,x8281),f5(x8282,x8283)),x8282))),
% 117.83/117.91 inference(scs_inference,[],[823,2])).
% 117.83/117.91 cnf(856,plain,
% 117.83/117.91 (E(f6(x8561,a3),f6(x8561,a11))),
% 117.83/117.91 inference(scs_inference,[],[95,9,2])).
% 117.83/117.91 cnf(857,plain,
% 117.83/117.91 (E(f6(x8571,a11),f6(x8571,a3))),
% 117.83/117.91 inference(scs_inference,[],[856,2])).
% 117.83/117.91 cnf(858,plain,
% 117.83/117.91 (E(f17(f6(f6(x8581,a3),f5(x8582,x8583)),x8582),f6(x8581,a11))),
% 117.83/117.91 inference(scs_inference,[],[49,856,2,3])).
% 117.83/117.91 cnf(864,plain,
% 117.83/117.91 (E(f17(f6(f6(x8641,a11),f5(x8642,x8643)),x8642),f6(x8641,a3))),
% 117.83/117.91 inference(scs_inference,[],[49,858,857,2,3])).
% 117.83/117.91 cnf(914,plain,
% 117.83/117.91 (E(f17(f6(f5(a3,a11),f5(x9141,x9142)),x9141),f5(a11,a3))),
% 117.83/117.91 inference(scs_inference,[],[640,657,3])).
% 117.83/117.91 cnf(917,plain,
% 117.83/117.91 (E(f5(a11,a3),f17(f6(f5(a3,a11),f5(x9171,x9172)),x9171))),
% 117.83/117.91 inference(scs_inference,[],[640,657,3,2])).
% 117.83/117.91 cnf(920,plain,
% 117.83/117.91 (E(f17(f6(f5(a11,a3),f5(x9201,x9202)),x9201),f5(a3,a11))),
% 117.83/117.91 inference(scs_inference,[],[647,656,3])).
% 117.83/117.91 cnf(923,plain,
% 117.83/117.91 (E(f5(a3,a11),f17(f6(f5(a11,a3),f5(x9231,x9232)),x9231))),
% 117.83/117.91 inference(scs_inference,[],[647,656,3,2])).
% 117.83/117.91 cnf(931,plain,
% 117.83/117.91 (E(f5(a11,a11),f5(a3,a3))),
% 117.83/117.91 inference(scs_inference,[],[639,657,3])).
% 117.83/117.91 cnf(934,plain,
% 117.83/117.91 (E(f5(a3,a3),f5(a11,a11))),
% 117.83/117.91 inference(scs_inference,[],[639,657,3,2])).
% 117.83/117.91 cnf(938,plain,
% 117.83/117.91 (E(f5(a3,a11),f5(a11,a3))),
% 117.83/117.91 inference(scs_inference,[],[638,657,3])).
% 117.83/117.91 cnf(941,plain,
% 117.83/117.91 (E(f5(a11,a3),f5(a3,a11))),
% 117.83/117.91 inference(scs_inference,[],[638,657,3,2])).
% 117.83/117.91 cnf(945,plain,
% 117.83/117.91 (E(f5(a11,a11),f17(f6(f5(a3,a3),f5(x9451,x9452)),x9451))),
% 117.83/117.91 inference(scs_inference,[],[639,665,3])).
% 117.83/117.91 cnf(948,plain,
% 117.83/117.91 (E(f17(f6(f5(a3,a3),f5(x9481,x9482)),x9481),f5(a11,a11))),
% 117.83/117.92 inference(scs_inference,[],[639,665,3,2])).
% 117.83/117.92 cnf(951,plain,
% 117.83/117.92 (E(f5(a3,a3),f17(f6(f5(a11,a11),f5(x9511,x9512)),x9511))),
% 117.83/117.92 inference(scs_inference,[],[638,671,3])).
% 117.83/117.92 cnf(954,plain,
% 117.83/117.92 (E(f17(f6(f5(a11,a11),f5(x9541,x9542)),x9541),f5(a3,a3))),
% 117.83/117.92 inference(scs_inference,[],[638,671,3,2])).
% 117.83/117.92 cnf(974,plain,
% 117.83/117.92 (P4(f6(x9741,f5(a1,x9742)),f4(a1,x9743))),
% 117.83/117.92 inference(scs_inference,[],[97,94,35])).
% 117.83/117.92 cnf(978,plain,
% 117.83/117.92 (P6(f17(f6(a1,f5(x9781,x9782)),x9781),f4(a1,x9783))),
% 117.83/117.92 inference(scs_inference,[],[97,94,521,597,35,31,32])).
% 117.83/117.92 cnf(980,plain,
% 117.83/117.92 (P1(f16(f6(x9801,f5(x9802,a1)),x9802),f4(a1,x9803))),
% 117.83/117.92 inference(scs_inference,[],[97,611,94,521,597,35,31,32,29])).
% 117.83/117.92 cnf(982,plain,
% 117.83/117.92 (P1(f4(a1,x9821),f16(f6(x9822,f5(x9823,a1)),x9823))),
% 117.83/117.92 inference(scs_inference,[],[97,603,611,94,521,597,35,31,32,29,28])).
% 117.83/117.92 cnf(989,plain,
% 117.83/117.92 (P6(f16(f6(x9891,f5(x9892,a1)),x9892),f4(a1,x9893))),
% 117.83/117.92 inference(scs_inference,[],[97,609,982,64,32])).
% 117.83/117.92 cnf(994,plain,
% 117.83/117.92 (E(f17(a3,x9941),f17(a11,x9941))),
% 117.83/117.92 inference(scs_inference,[],[95,14,2])).
% 117.83/117.92 cnf(995,plain,
% 117.83/117.92 (E(f17(a11,x9951),f17(a3,x9951))),
% 117.83/117.92 inference(scs_inference,[],[994,2])).
% 117.83/117.92 cnf(1056,plain,
% 117.83/117.92 (~E(f6(x10561,f5(x10562,x10563)),f17(f6(a1,f5(x10564,x10565)),x10564))),
% 117.83/117.92 inference(scs_inference,[],[114,49,3])).
% 117.83/117.92 cnf(1058,plain,
% 117.83/117.92 (E(f17(x10581,a3),f17(x10581,a11))),
% 117.83/117.92 inference(scs_inference,[],[95,15,2])).
% 117.83/117.92 cnf(1059,plain,
% 117.83/117.92 (E(f17(x10591,a11),f17(x10591,a3))),
% 117.83/117.92 inference(scs_inference,[],[1058,2])).
% 117.83/117.92 cnf(1060,plain,
% 117.83/117.92 (~E(f6(x10601,f5(x10602,x10603)),f17(f6(f4(a1,x10604),f5(a11,x10605)),a3))),
% 117.83/117.92 inference(scs_inference,[],[149,1058,2,3])).
% 117.83/117.92 cnf(1061,plain,
% 117.83/117.92 (E(f17(x10611,a3),f17(x10611,a11))),
% 117.83/117.92 inference(rename_variables,[],[1058])).
% 117.83/117.92 cnf(1063,plain,
% 117.83/117.92 (P2(f17(f6(f6(x10631,f5(x10632,x10633)),f5(a3,x10634)),a11))),
% 117.83/117.92 inference(scs_inference,[],[224,149,1058,1061,2,3,33])).
% 117.83/117.92 cnf(1064,plain,
% 117.83/117.92 (E(f17(x10641,a3),f17(x10641,a11))),
% 117.83/117.92 inference(rename_variables,[],[1058])).
% 117.83/117.92 cnf(1066,plain,
% 117.83/117.92 (P7(f17(f6(f13(f20(a9,a10,a11),a12),f5(a3,x10661)),a11))),
% 117.83/117.92 inference(scs_inference,[],[230,224,149,1058,1061,1064,2,3,33,36])).
% 117.83/117.92 cnf(1072,plain,
% 117.83/117.92 (E(f16(f4(a11,x10721),x10722),f16(f4(a3,x10721),x10722))),
% 117.83/117.92 inference(scs_inference,[],[95,17,4])).
% 117.83/117.92 cnf(1073,plain,
% 117.83/117.92 (E(f16(f4(a3,x10731),x10732),f16(f4(a11,x10731),x10732))),
% 117.83/117.92 inference(scs_inference,[],[1072,2])).
% 117.83/117.92 cnf(1074,plain,
% 117.83/117.92 (E(f17(f6(f16(f4(a11,x10741),x10742),f5(x10743,x10744)),x10743),f16(f4(a3,x10741),x10742))),
% 117.83/117.92 inference(scs_inference,[],[49,1072,2,3])).
% 117.83/117.92 cnf(1076,plain,
% 117.83/117.92 (P3(f17(f6(f8(f20(x10761,a1,x10762)),f5(a3,x10763)),a11))),
% 117.83/117.92 inference(scs_inference,[],[49,1072,226,1058,2,3,30])).
% 117.83/117.92 cnf(1081,plain,
% 117.83/117.92 (E(f16(x10811,f4(x10812,a11)),f16(x10811,f4(x10812,a3)))),
% 117.83/117.92 inference(scs_inference,[],[95,18,5])).
% 117.83/117.92 cnf(1083,plain,
% 117.83/117.92 (~E(f6(x10831,f5(x10832,x10833)),f17(f6(a1,f5(a3,x10834)),a11))),
% 117.83/117.92 inference(scs_inference,[],[1059,1056,1074,2,3])).
% 117.83/117.92 cnf(1091,plain,
% 117.83/117.92 (E(f18(f5(a11,x10911),x10912),f18(f5(a3,x10911),x10912))),
% 117.83/117.92 inference(scs_inference,[],[95,19,6])).
% 117.83/117.92 cnf(1092,plain,
% 117.83/117.92 (E(f18(f5(a3,x10921),x10922),f18(f5(a11,x10921),x10922))),
% 117.83/117.92 inference(scs_inference,[],[1091,2])).
% 117.83/117.92 cnf(1093,plain,
% 117.83/117.92 (E(f17(f6(f16(f4(a3,x10931),x10932),f5(x10933,x10934)),x10933),f16(f4(a11,x10931),x10932))),
% 117.83/117.92 inference(scs_inference,[],[49,1073,1091,2,3])).
% 117.83/117.92 cnf(1098,plain,
% 117.83/117.92 (E(f18(x10981,f5(x10982,a11)),f18(x10981,f5(x10982,a3)))),
% 117.83/117.92 inference(scs_inference,[],[95,20,7])).
% 117.83/117.92 cnf(1100,plain,
% 117.83/117.92 (E(f17(f6(f18(f5(a3,x11001),x11002),f5(x11003,x11004)),x11003),f18(f5(a11,x11001),x11002))),
% 117.83/117.92 inference(scs_inference,[],[49,1093,1092,2,3])).
% 117.83/117.92 cnf(1106,plain,
% 117.83/117.92 (E(f17(f6(f18(x11061,f5(x11062,a11)),f5(x11063,x11064)),x11063),f18(x11061,f5(x11062,a3)))),
% 117.83/117.92 inference(scs_inference,[],[49,1100,1098,2,3])).
% 117.83/117.92 cnf(1112,plain,
% 117.83/117.92 (~E(f6(x11121,f5(x11122,x11123)),f16(f6(x11124,f5(f4(x11125,a3),a1)),f4(x11125,a11)))),
% 117.83/117.92 inference(scs_inference,[],[505,1106,1081,2,3])).
% 117.83/117.92 cnf(1118,plain,
% 117.83/117.92 (E(f18(x11181,f5(x11182,a3)),f18(x11181,f5(x11182,a11)))),
% 117.83/117.92 inference(scs_inference,[],[1098,2])).
% 117.83/117.92 cnf(1134,plain,
% 117.83/117.92 (E(f16(x11341,f4(x11342,a3)),f16(x11341,f4(x11342,a11)))),
% 117.83/117.92 inference(scs_inference,[],[1081,2])).
% 117.83/117.92 cnf(1334,plain,
% 117.83/117.92 (E(f17(f6(f6(a3,a3),f5(x13341,x13342)),x13341),f6(a11,a11))),
% 117.83/117.92 inference(scs_inference,[],[858,816,3])).
% 117.83/117.92 cnf(1337,plain,
% 117.83/117.92 (E(f6(a11,a11),f17(f6(f6(a3,a3),f5(x13371,x13372)),x13371))),
% 117.83/117.92 inference(scs_inference,[],[858,816,3,2])).
% 117.83/117.92 cnf(1341,plain,
% 117.83/117.92 (E(f17(f6(f6(a3,a11),f5(x13411,x13412)),x13411),f6(a11,a3))),
% 117.83/117.92 inference(scs_inference,[],[864,816,3])).
% 117.83/117.92 cnf(1344,plain,
% 117.83/117.92 (E(f6(a11,a3),f17(f6(f6(a3,a11),f5(x13441,x13442)),x13441))),
% 117.83/117.92 inference(scs_inference,[],[864,816,3,2])).
% 117.83/117.92 cnf(1349,plain,
% 117.83/117.92 (E(f15(f20(a11,x13491,x13492),x13493),f15(f20(a3,x13491,x13492),x13493))),
% 117.83/117.92 inference(scs_inference,[],[95,24,10])).
% 117.83/117.92 cnf(1350,plain,
% 117.83/117.92 (E(f15(f20(a3,x13501,x13502),x13503),f15(f20(a11,x13501,x13502),x13503))),
% 117.83/117.92 inference(scs_inference,[],[1349,2])).
% 117.83/117.92 cnf(1351,plain,
% 117.83/117.92 (E(f6(a3,a11),f6(a11,a3))),
% 117.83/117.92 inference(scs_inference,[],[200,1341,1349,2,3])).
% 117.83/117.92 cnf(1357,plain,
% 117.83/117.92 (E(f6(a11,a3),f6(a3,a11))),
% 117.83/117.92 inference(scs_inference,[],[1351,2])).
% 117.83/117.92 cnf(1358,plain,
% 117.83/117.92 (E(f6(a3,a3),f6(a11,a11))),
% 117.83/117.92 inference(scs_inference,[],[200,1351,1334,2,3])).
% 117.83/117.92 cnf(1364,plain,
% 117.83/117.92 (E(f6(a11,a11),f6(a3,a3))),
% 117.83/117.92 inference(scs_inference,[],[1358,2])).
% 117.83/117.92 cnf(1365,plain,
% 117.83/117.92 (E(f17(f6(f6(a11,a3),f5(x13651,x13652)),x13651),f6(a3,a11))),
% 117.83/117.92 inference(scs_inference,[],[49,1357,1358,2,3])).
% 117.83/117.92 cnf(1373,plain,
% 117.83/117.92 (E(f17(f6(f6(a11,a11),f5(x13731,x13732)),x13731),f6(a3,a3))),
% 117.83/117.92 inference(scs_inference,[],[49,1365,1364,2,3])).
% 117.83/117.92 cnf(1380,plain,
% 117.83/117.92 (E(f6(a3,a3),f17(f6(f6(a11,a11),f5(x13801,x13802)),x13801))),
% 117.83/117.92 inference(scs_inference,[],[1373,2])).
% 117.83/117.92 cnf(1381,plain,
% 117.83/117.92 (E(f17(f6(f15(f20(a3,x13811,x13812),x13813),f5(x13814,x13815)),x13814),f15(f20(a11,x13811,x13812),x13813))),
% 117.83/117.92 inference(scs_inference,[],[49,1373,1350,2,3])).
% 117.83/117.92 cnf(1388,plain,
% 117.83/117.92 (E(f17(f6(f15(f20(a11,x13881,x13882),x13883),f5(x13884,x13885)),x13884),f15(f20(a3,x13881,x13882),x13883))),
% 117.83/117.92 inference(scs_inference,[],[49,1381,1349,2,3])).
% 117.83/117.92 cnf(1395,plain,
% 117.83/117.92 (E(f15(f20(a3,x13951,x13952),x13953),f17(f6(f15(f20(a11,x13951,x13952),x13953),f5(x13954,x13955)),x13954))),
% 117.83/117.92 inference(scs_inference,[],[1388,2])).
% 117.83/117.92 cnf(1537,plain,
% 117.83/117.92 (P4(f6(x15371,f5(a3,x15372)),a11)),
% 117.83/117.92 inference(scs_inference,[],[123,94,35])).
% 117.83/117.92 cnf(1539,plain,
% 117.83/117.92 (P6(a11,f16(f6(x15391,f5(x15392,a3)),x15392))),
% 117.83/117.92 inference(scs_inference,[],[123,94,597,35,31])).
% 117.83/117.92 cnf(1541,plain,
% 117.83/117.92 (P6(f16(f6(x15411,f5(x15412,a3)),x15412),a11)),
% 117.83/117.92 inference(scs_inference,[],[123,94,597,609,35,31,32])).
% 117.83/117.92 cnf(1543,plain,
% 117.83/117.92 (P1(f16(f6(x15431,f5(x15432,a3)),x15432),a11)),
% 117.83/117.92 inference(scs_inference,[],[123,611,94,597,609,35,31,32,29])).
% 117.83/117.92 cnf(1545,plain,
% 117.83/117.92 (P1(a11,f16(f6(x15451,f5(x15452,a3)),x15452))),
% 117.83/117.92 inference(scs_inference,[],[123,603,611,94,597,609,35,31,32,29,28])).
% 117.83/117.92 cnf(1547,plain,
% 117.83/117.92 (~P9(a11,f16(f6(x15471,f5(x15472,a3)),x15472))),
% 117.83/117.92 inference(scs_inference,[],[123,603,611,94,597,609,35,31,32,29,28,64])).
% 117.83/117.92 cnf(1550,plain,
% 117.83/117.92 (~P9(f16(f6(x15501,f5(x15502,a3)),x15502),a11)),
% 117.83/117.92 inference(scs_inference,[],[1545,64])).
% 117.83/117.92 cnf(1558,plain,
% 117.83/117.92 (E(f15(x15581,a3),f15(x15581,a11))),
% 117.83/117.92 inference(scs_inference,[],[95,25,2])).
% 117.83/117.92 cnf(1559,plain,
% 117.83/117.92 (E(f15(x15591,a11),f15(x15591,a3))),
% 117.83/117.92 inference(scs_inference,[],[1558,2])).
% 117.83/117.92 cnf(1560,plain,
% 117.83/117.92 (E(f17(f6(f15(x15601,a3),f5(x15602,x15603)),x15602),f15(x15601,a11))),
% 117.83/117.92 inference(scs_inference,[],[49,1558,2,3])).
% 117.83/117.92 cnf(1569,plain,
% 117.83/117.92 (E(f17(f6(f15(x15691,a11),f5(x15692,x15693)),x15692),f15(x15691,a3))),
% 117.83/117.92 inference(scs_inference,[],[49,1560,1559,2,3])).
% 117.83/117.92 cnf(1574,plain,
% 117.83/117.92 (E(f15(x15741,a3),f17(f6(f15(x15741,a11),f5(x15742,x15743)),x15742))),
% 117.83/117.92 inference(scs_inference,[],[1569,2])).
% 117.83/117.92 cnf(1657,plain,
% 117.83/117.92 (P4(f6(x16571,f5(a3,x16572)),f16(f6(x16573,f5(x16574,a11)),x16574))),
% 117.83/117.92 inference(scs_inference,[],[143,94,35])).
% 117.83/117.92 cnf(1659,plain,
% 117.83/117.92 (E(f19(a3,x16591),f19(a11,x16591))),
% 117.83/117.92 inference(scs_inference,[],[95,26,2])).
% 117.83/117.92 cnf(1660,plain,
% 117.83/117.92 (E(f19(a11,x16601),f19(a3,x16601))),
% 117.83/117.92 inference(scs_inference,[],[1659,2])).
% 117.83/117.92 cnf(1661,plain,
% 117.83/117.92 (E(f17(f6(f19(a3,x16611),f5(x16612,x16613)),x16612),f19(a11,x16611))),
% 117.83/117.92 inference(scs_inference,[],[49,1659,2,3])).
% 117.83/117.92 cnf(1666,plain,
% 117.83/117.92 (E(f19(a11,x16661),f17(f6(f19(a3,x16661),f5(x16662,x16663)),x16662))),
% 117.83/117.92 inference(scs_inference,[],[1661,2])).
% 117.83/117.92 cnf(1667,plain,
% 117.83/117.92 (E(f17(f6(f19(a11,x16671),f5(x16672,x16673)),x16672),f19(a3,x16671))),
% 117.83/117.92 inference(scs_inference,[],[49,1661,1660,2,3])).
% 117.83/117.92 cnf(1672,plain,
% 117.83/117.92 (E(f19(a3,x16721),f17(f6(f19(a11,x16721),f5(x16722,x16723)),x16722))),
% 117.83/117.92 inference(scs_inference,[],[1667,2])).
% 117.83/117.92 cnf(1712,plain,
% 117.83/117.92 (E(f18(f5(a3,x17121),f5(x17122,a3)),f18(f5(a11,x17121),f5(x17122,a11)))),
% 117.83/117.92 inference(scs_inference,[],[1092,1118,3])).
% 117.83/117.92 cnf(1715,plain,
% 117.83/117.92 (E(f18(f5(a11,x17151),f5(x17152,a11)),f18(f5(a3,x17151),f5(x17152,a3)))),
% 117.83/117.92 inference(scs_inference,[],[1092,1118,3,2])).
% 117.83/117.92 cnf(1731,plain,
% 117.83/117.92 (E(f18(f5(a11,x17311),f5(x17312,a3)),f18(f5(a3,x17311),f5(x17312,a11)))),
% 117.83/117.92 inference(scs_inference,[],[1092,1098,3,2])).
% 117.83/117.92 cnf(1771,plain,
% 117.83/117.92 (~E(f6(x17711,f5(x17712,x17713)),f17(f6(f4(a1,x17714),f5(a3,x17715)),a11))),
% 117.83/117.92 inference(scs_inference,[],[149,1059,3])).
% 117.83/117.92 cnf(1774,plain,
% 117.83/117.92 (E(f19(x17741,a3),f19(x17741,a11))),
% 117.83/117.92 inference(scs_inference,[],[95,27,2])).
% 117.83/117.92 cnf(1775,plain,
% 117.83/117.92 (E(f19(x17751,a11),f19(x17751,a3))),
% 117.83/117.92 inference(scs_inference,[],[1774,2])).
% 117.83/117.92 cnf(1776,plain,
% 117.83/117.92 (E(f17(f6(f19(x17761,a3),f5(x17762,x17763)),x17762),f19(x17761,a11))),
% 117.83/117.92 inference(scs_inference,[],[49,1774,2,3])).
% 117.83/117.92 cnf(1784,plain,
% 117.83/117.92 (E(f19(x17841,a11),f17(f6(f19(x17841,a3),f5(x17842,x17843)),x17842))),
% 117.83/117.92 inference(scs_inference,[],[1776,2])).
% 117.83/117.92 cnf(1785,plain,
% 117.83/117.92 (E(f17(f6(f19(x17851,a11),f5(x17852,x17853)),x17852),f19(x17851,a3))),
% 117.83/117.92 inference(scs_inference,[],[49,1776,1775,2,3])).
% 117.83/117.92 cnf(1790,plain,
% 117.83/117.92 (E(f19(x17901,a3),f17(f6(f19(x17901,a11),f5(x17902,x17903)),x17902))),
% 117.83/117.92 inference(scs_inference,[],[1785,2])).
% 117.83/117.92 cnf(1875,plain,
% 117.83/117.92 (P4(f6(x18751,f5(a1,x18752)),f17(f6(f4(a1,x18753),f5(x18754,x18755)),x18754))),
% 117.83/117.92 inference(scs_inference,[],[159,94,35])).
% 117.83/117.92 cnf(1878,plain,
% 117.83/117.92 (P4(f6(x18781,f5(f20(x18782,a1,a3),x18783)),f8(f20(x18782,a1,x18784)))),
% 117.83/117.92 inference(scs_inference,[],[166,94,35])).
% 117.83/117.92 cnf(1882,plain,
% 117.83/117.92 (P6(f17(f6(f20(x18821,a1,a3),f5(x18822,x18823)),x18822),f8(f20(x18821,a1,x18824)))),
% 117.83/117.92 inference(scs_inference,[],[166,94,519,521,35,31,32])).
% 117.83/117.92 cnf(1884,plain,
% 117.83/117.92 (P1(f17(f6(f20(x18841,a1,a3),f5(x18842,x18843)),x18842),f8(f20(x18841,a1,x18844)))),
% 117.83/117.92 inference(scs_inference,[],[166,525,94,519,521,35,31,32,29])).
% 117.83/117.92 cnf(1886,plain,
% 117.83/117.92 (P1(f8(f20(x18861,a1,x18862)),f17(f6(f20(x18861,a1,a3),f5(x18863,x18864)),x18863))),
% 117.83/117.92 inference(scs_inference,[],[166,527,525,94,519,521,35,31,32,29,28])).
% 117.83/117.92 cnf(1890,plain,
% 117.83/117.92 (~P9(f17(f6(f20(x18901,a1,a3),f5(x18902,x18903)),x18902),f8(f20(x18901,a1,x18904)))),
% 117.83/117.92 inference(scs_inference,[],[1886,64])).
% 117.83/117.92 cnf(1893,plain,
% 117.83/117.92 (P4(f6(f6(x18931,f5(a11,x18932)),f5(x18933,x18934)),a3)),
% 117.83/117.92 inference(scs_inference,[],[95,72,70])).
% 117.83/117.92 cnf(1894,plain,
% 117.83/117.92 (P4(f6(f6(x18941,f5(a11,x18942)),f5(x18943,x18944)),f17(f6(a11,f5(x18945,x18946)),x18945))),
% 117.83/117.92 inference(scs_inference,[],[213,1893,35])).
% 117.83/117.92 cnf(1896,plain,
% 117.83/117.92 (P4(f6(f6(x18961,f5(a11,x18962)),f5(x18963,x18964)),f16(f6(x18965,f5(x18966,a11)),x18966))),
% 117.83/117.92 inference(scs_inference,[],[143,1893,35])).
% 117.83/117.92 cnf(1897,plain,
% 117.83/117.92 (E(f17(f6(f15(f20(a11,x18971,x18972),a11),f5(x18973,x18974)),x18973),f15(f20(a3,x18971,x18972),a3))),
% 117.83/117.92 inference(scs_inference,[],[1388,1559,3])).
% 117.83/117.92 cnf(1906,plain,
% 117.83/117.92 (E(f17(f6(f15(f20(a11,x19061,x19062),a3),f5(x19063,x19064)),x19063),f15(f20(a3,x19061,x19062),a11))),
% 117.83/117.92 inference(scs_inference,[],[1388,1558,3])).
% 117.83/117.92 cnf(1909,plain,
% 117.83/117.92 (E(f15(f20(a3,x19091,x19092),a11),f17(f6(f15(f20(a11,x19091,x19092),a3),f5(x19093,x19094)),x19093))),
% 117.83/117.92 inference(scs_inference,[],[1388,1558,3,2])).
% 117.83/117.92 cnf(1915,plain,
% 117.83/117.92 (E(f15(f20(a11,x19151,x19152),a11),f15(f20(a3,x19151,x19152),a3))),
% 117.83/117.92 inference(scs_inference,[],[200,1897,3])).
% 117.83/117.92 cnf(1918,plain,
% 117.83/117.92 (E(f15(f20(a3,x19181,x19182),a3),f15(f20(a11,x19181,x19182),a11))),
% 117.83/117.92 inference(scs_inference,[],[200,1897,3,2])).
% 117.83/117.92 cnf(1923,plain,
% 117.83/117.92 (E(f17(f6(f15(f20(a3,x19231,x19232),a11),f5(x19233,x19234)),x19233),f15(f20(a11,x19231,x19232),a3))),
% 117.83/117.92 inference(scs_inference,[],[1381,1559,3])).
% 117.83/117.92 cnf(1926,plain,
% 117.83/117.92 (E(f15(f20(a11,x19261,x19262),a3),f17(f6(f15(f20(a3,x19261,x19262),a11),f5(x19263,x19264)),x19263))),
% 117.83/117.92 inference(scs_inference,[],[1381,1559,3,2])).
% 117.83/117.92 cnf(1929,plain,
% 117.83/117.92 (E(f15(f20(a11,x19291,x19292),a3),f15(f20(a3,x19291,x19292),a11))),
% 117.83/117.92 inference(scs_inference,[],[200,1906,3])).
% 117.83/117.92 cnf(1932,plain,
% 117.83/117.92 (E(f15(f20(a3,x19321,x19322),a11),f15(f20(a11,x19321,x19322),a3))),
% 117.83/117.92 inference(scs_inference,[],[200,1906,3,2])).
% 117.83/117.92 cnf(1949,plain,
% 117.83/117.92 (P4(f6(x19491,f5(x19492,x19493)),f17(f6(x19492,f5(x19494,x19495)),x19494))),
% 117.83/117.92 inference(scs_inference,[],[200,94,35])).
% 117.83/117.92 cnf(1952,plain,
% 117.83/117.92 (P4(f6(x19521,f5(a3,x19522)),f17(f6(a11,f5(x19523,x19524)),x19523))),
% 117.83/117.92 inference(scs_inference,[],[200,1537,35])).
% 117.83/117.92 cnf(1955,plain,
% 117.83/117.92 (P4(f6(f6(x19551,f5(a11,x19552)),f5(x19553,x19554)),f17(f6(a3,f5(x19555,x19556)),x19555))),
% 117.83/117.92 inference(scs_inference,[],[200,1893,35])).
% 117.83/117.92 cnf(1958,plain,
% 117.83/117.92 (P4(f6(f6(x19581,f5(a11,x19582)),f5(x19583,x19584)),a11)),
% 117.83/117.92 inference(scs_inference,[],[300,1955,35])).
% 117.83/117.92 cnf(1961,plain,
% 117.83/117.92 (P4(f6(x19611,f5(a2,x19612)),f7(f20(x19613,a1,x19614)))),
% 117.83/117.92 inference(scs_inference,[],[283,1949,35])).
% 117.83/117.92 cnf(1973,plain,
% 117.83/117.92 (P2(f17(f6(f6(x19731,f5(x19732,x19733)),f5(a11,x19734)),a3))),
% 117.83/117.92 inference(scs_inference,[],[224,1059,33])).
% 117.83/117.92 cnf(1977,plain,
% 117.83/117.92 (E(f7(f20(x19771,f6(x19772,f5(x19773,x19774)),x19775)),f14(x19771))),
% 117.83/117.92 inference(scs_inference,[],[97,192,73,3])).
% 117.83/117.92 cnf(1978,plain,
% 117.83/117.92 (E(a3,f16(f6(x19781,f5(f4(x19782,a11),a11)),f4(x19782,a3)))),
% 117.83/117.92 inference(scs_inference,[],[143,1081,3])).
% 117.83/117.92 cnf(1984,plain,
% 117.83/117.92 (E(f16(f6(x19841,f5(f4(x19842,a11),a11)),f4(x19842,a3)),a3)),
% 117.83/117.92 inference(scs_inference,[],[226,143,1081,1059,3,30,2])).
% 117.83/117.92 cnf(1995,plain,
% 117.83/117.92 (E(a3,f16(f6(x19951,f5(f4(x19952,a3),a11)),f4(x19952,a11)))),
% 117.83/117.92 inference(scs_inference,[],[143,1134,3])).
% 117.83/117.92 cnf(1998,plain,
% 117.83/117.92 (E(f16(f6(x19981,f5(f4(x19982,a3),a11)),f4(x19982,a11)),a3)),
% 117.83/117.92 inference(scs_inference,[],[143,1134,3,2])).
% 117.83/117.92 cnf(2009,plain,
% 117.83/117.92 (E(f17(f6(f7(f20(x20091,a1,x20092)),f5(a3,x20093)),a11),a2)),
% 117.83/117.92 inference(scs_inference,[],[258,1058,3,155,64,2])).
% 117.83/117.92 cnf(2024,plain,
% 117.83/117.92 (P1(f17(f6(f7(f20(x20241,a1,x20242)),f5(a11,x20243)),a3),x20244)),
% 117.83/117.92 inference(scs_inference,[],[258,1059,3,155])).
% 117.83/117.92 cnf(2027,plain,
% 117.83/117.92 (E(f17(f6(f7(f20(x20271,a1,x20272)),f5(a11,x20273)),a3),a2)),
% 117.83/117.92 inference(scs_inference,[],[258,1059,3,155,64,2])).
% 117.83/117.92 cnf(2036,plain,
% 117.83/117.92 (E(a11,f16(f6(x20361,f5(f4(x20362,a11),a11)),f4(x20362,a3)))),
% 117.83/117.92 inference(scs_inference,[],[95,1978,3])).
% 117.83/117.92 cnf(2037,plain,
% 117.83/117.92 (E(f16(f6(x20371,f5(f4(x20372,a11),a11)),f4(x20372,a3)),a11)),
% 117.83/117.92 inference(scs_inference,[],[95,1978,3,2])).
% 117.83/117.92 cnf(2065,plain,
% 117.83/117.92 (E(a11,f16(f6(x20651,f5(f4(x20652,a3),a11)),f4(x20652,a11)))),
% 117.83/117.92 inference(scs_inference,[],[95,1995,3])).
% 117.83/117.92 cnf(2066,plain,
% 117.83/117.92 (E(f16(f6(x20661,f5(f4(x20662,a3),a11)),f4(x20662,a11)),a11)),
% 117.83/117.92 inference(scs_inference,[],[95,1995,3,2])).
% 117.83/117.92 cnf(2161,plain,
% 117.83/117.92 (P7(f17(f6(f13(f20(a9,a10,a11),a12),f5(a11,x21611)),a3))),
% 117.83/117.92 inference(scs_inference,[],[230,1059,36])).
% 117.83/117.92 cnf(2164,plain,
% 117.83/117.92 (E(f20(x21641,a3,x21642),f20(x21641,a11,x21642))),
% 117.83/117.92 inference(scs_inference,[],[95,11,2])).
% 117.83/117.92 cnf(2165,plain,
% 117.83/117.92 (~P4(f17(f6(f4(a1,x21651),f5(x21652,x21653)),x21652),x21654)),
% 117.83/117.92 inference(scs_inference,[],[637,76])).
% 117.83/117.92 cnf(2168,plain,
% 117.83/117.92 (P1(a1,f16(f6(x21681,f5(x21682,f4(a1,x21683))),x21682))),
% 117.83/117.92 inference(scs_inference,[],[105,603,1977,637,76,2,66])).
% 117.83/117.92 cnf(2171,plain,
% 117.83/117.92 (P4(f6(x21711,f5(f4(a1,x21712),x21713)),f17(f6(f4(a1,x21714),f5(x21715,x21716)),x21715))),
% 117.83/117.92 inference(scs_inference,[],[188,105,603,1977,144,637,76,2,66,35])).
% 117.83/117.92 cnf(2180,plain,
% 117.83/117.92 (E(x21801,f17(f6(x21801,f5(x21802,x21803)),x21802))),
% 117.83/117.92 inference(rename_variables,[],[200])).
% 117.83/117.92 cnf(2181,plain,
% 117.83/117.92 (E(f17(f6(a3,f5(x21811,x21812)),x21811),f17(f6(a3,f5(x21813,x21814)),x21813))),
% 117.83/117.92 inference(scs_inference,[],[300,234,188,105,436,384,603,200,430,989,1977,144,637,76,2,66,35,31,32,29,28,3])).
% 117.83/117.92 cnf(2183,plain,
% 117.83/117.92 (E(x21831,f17(f6(x21831,f5(x21832,x21833)),x21832))),
% 117.83/117.92 inference(rename_variables,[],[200])).
% 117.83/117.92 cnf(2184,plain,
% 117.83/117.92 (P2(f17(f6(f17(f6(f6(x21841,f5(x21842,x21843)),f5(a3,x21844)),a11),f5(x21845,x21846)),x21845))),
% 117.83/117.92 inference(scs_inference,[],[230,300,234,188,105,436,384,603,200,2180,2183,430,989,1977,1063,144,637,76,2,66,35,31,32,29,28,3,36,33])).
% 117.83/117.92 cnf(2185,plain,
% 117.83/117.92 (E(x21851,f17(f6(x21851,f5(x21852,x21853)),x21852))),
% 117.83/117.92 inference(rename_variables,[],[200])).
% 117.83/117.92 cnf(2188,plain,
% 117.83/117.92 (~P9(f16(f6(x21881,f5(x21882,f4(a1,x21883))),x21882),a1)),
% 117.83/117.92 inference(scs_inference,[],[230,300,234,188,105,436,384,603,200,2180,2183,2185,430,989,1977,1063,1076,144,637,76,2,66,35,31,32,29,28,3,36,33,30,64])).
% 117.83/117.92 cnf(2192,plain,
% 117.83/117.92 (E(f20(x21921,x21922,f4(f20(x21923,a3,x21924),x21925)),f20(x21921,x21922,f4(f20(x21923,a11,x21924),x21925)))),
% 117.83/117.92 inference(scs_inference,[],[2164,12,4])).
% 117.83/117.92 cnf(2193,plain,
% 117.83/117.92 (P6(f17(f6(f20(x21931,a1,a3),f5(x21932,x21933)),x21932),f8(f8(f20(x21931,a1,x21934))))),
% 117.83/117.92 inference(scs_inference,[],[1882,63])).
% 117.83/117.92 cnf(2195,plain,
% 117.83/117.92 (P6(f17(f6(f20(x21951,a1,a3),f5(x21952,x21953)),x21952),f13(f8(f20(x21951,a1,x21954)),x21955))),
% 117.83/117.92 inference(scs_inference,[],[1882,63,67])).
% 117.83/117.92 cnf(2197,plain,
% 117.83/117.92 (P6(f17(f6(f20(x21971,a1,a3),f5(x21972,x21973)),x21972),f18(f8(f20(x21971,a1,x21974)),x21975))),
% 117.83/117.92 inference(scs_inference,[],[1882,63,67,68])).
% 117.83/117.92 cnf(2199,plain,
% 117.83/117.92 (~P5(f20(x21991,a1,x21992),x21993)),
% 117.83/117.92 inference(scs_inference,[],[1882,57,63,67,68,82])).
% 117.83/117.92 cnf(2217,plain,
% 117.83/117.92 (E(f16(x22171,f15(f20(a11,x22172,x22173),a3)),f16(x22171,f15(f20(a3,x22172,x22173),a11)))),
% 117.83/117.92 inference(scs_inference,[],[2171,1882,1929,57,63,67,68,82,13,16,23,70,72,4,5,6,7,8,9,14,15,17,18])).
% 117.83/117.92 cnf(2231,plain,
% 117.83/117.92 (E(f18(f20(x22311,a1,x22312),x22313),f20(x22311,a1,a3))),
% 117.83/117.92 inference(scs_inference,[],[2171,1882,978,1929,57,63,67,68,82,13,16,23,70,72,4,5,6,7,8,9,14,15,17,18,19,20,21,22,24,25,26,27,69,10,11,12,81])).
% 117.83/117.92 cnf(2233,plain,
% 117.83/117.92 (E(f6(f4(x22331,a11),f5(x22332,a3)),f4(f6(x22331,f5(x22332,a3)),a11))),
% 117.83/117.92 inference(scs_inference,[],[2171,1882,978,1929,134,57,63,67,68,82,13,16,23,70,72,4,5,6,7,8,9,14,15,17,18,19,20,21,22,24,25,26,27,69,10,11,12,81,78])).
% 117.83/117.92 cnf(2238,plain,
% 117.83/117.92 (~P9(f20(x22381,x22382,f4(f20(x22383,a3,x22384),x22385)),f20(x22381,x22382,f4(f20(x22383,a11,x22384),x22385)))),
% 117.83/117.92 inference(scs_inference,[],[98,1060,2192,2171,1882,1878,978,1929,134,57,63,67,68,82,13,16,23,70,72,4,5,6,7,8,9,14,15,17,18,19,20,21,22,24,25,26,27,69,10,11,12,81,78,76,2,37])).
% 117.83/117.92 cnf(2239,plain,
% 117.83/117.92 (~P9(x22391,x22391)),
% 117.83/117.92 inference(rename_variables,[],[98])).
% 117.83/117.92 cnf(2240,plain,
% 117.83/117.92 (~P9(f20(x22401,x22402,f4(f20(x22403,a11,x22404),x22405)),f20(x22401,x22402,f4(f20(x22403,a3,x22404),x22405)))),
% 117.83/117.92 inference(scs_inference,[],[98,2239,1060,2192,2171,1882,1878,978,1929,134,57,63,67,68,82,13,16,23,70,72,4,5,6,7,8,9,14,15,17,18,19,20,21,22,24,25,26,27,69,10,11,12,81,78,76,2,37,38])).
% 117.83/117.92 cnf(2242,plain,
% 117.83/117.92 (~P8(f17(f6(f4(a1,x22421),f5(x22422,x22423)),x22422),x22424,x22425)),
% 117.83/117.92 inference(scs_inference,[],[98,2239,58,1060,2192,2171,1882,1878,978,1929,134,57,103,63,67,68,82,13,16,23,70,72,4,5,6,7,8,9,14,15,17,18,19,20,21,22,24,25,26,27,69,10,11,12,81,78,76,2,37,38,41])).
% 117.83/117.92 cnf(2243,plain,
% 117.83/117.92 (P8(f6(x22431,f5(f5(a11,a3),f5(a11,a3))),f5(a3,a11),f5(a3,a11))),
% 117.83/117.92 inference(scs_inference,[],[98,2239,58,1060,2192,2171,1882,1878,978,1929,941,134,57,103,63,67,68,82,13,16,23,70,72,4,5,6,7,8,9,14,15,17,18,19,20,21,22,24,25,26,27,69,10,11,12,81,78,76,2,37,38,41,75])).
% 117.83/117.92 cnf(2246,plain,
% 117.83/117.92 (~P8(a1,x22461,x22462)),
% 117.83/117.92 inference(rename_variables,[],[58])).
% 117.83/117.92 cnf(2251,plain,
% 117.83/117.92 (P1(f17(f6(f20(x22511,a1,a3),f5(x22512,x22513)),x22512),f17(f6(f20(x22511,a1,a3),f5(x22514,x22515)),x22514))),
% 117.83/117.92 inference(scs_inference,[],[98,2239,58,2246,1060,2192,2171,1882,1878,1884,978,1929,941,1886,192,134,57,103,63,67,68,82,13,16,23,70,72,4,5,6,7,8,9,14,15,17,18,19,20,21,22,24,25,26,27,69,10,11,12,81,78,76,2,37,38,41,75,85,86,66])).
% 117.83/117.92 cnf(2254,plain,
% 117.83/117.92 (~E(f13(f20(a9,a10,a11),a12),f17(f6(f20(a9,a10,a11),f5(x22541,x22542)),x22541))),
% 117.83/117.92 inference(scs_inference,[],[54,98,2239,58,2246,147,1060,2192,2171,1882,1878,1884,978,1929,941,1886,192,134,57,103,63,67,68,82,13,16,23,70,72,4,5,6,7,8,9,14,15,17,18,19,20,21,22,24,25,26,27,69,10,11,12,81,78,76,2,37,38,41,75,85,86,66,36])).
% 117.83/117.92 cnf(2255,plain,
% 117.83/117.92 (~E(f17(f6(f6(x22551,f5(x22552,x22553)),f5(a11,x22554)),a3),f17(f6(f4(a1,x22555),f5(x22556,x22557)),x22556))),
% 117.83/117.92 inference(scs_inference,[],[54,98,2239,58,2246,147,131,1060,1973,2192,2171,1882,1878,1884,978,1929,941,1886,192,134,57,103,63,67,68,82,13,16,23,70,72,4,5,6,7,8,9,14,15,17,18,19,20,21,22,24,25,26,27,69,10,11,12,81,78,76,2,37,38,41,75,85,86,66,36,33])).
% 117.83/117.92 cnf(2256,plain,
% 117.83/117.92 (P8(f6(f6(x22561,f5(f5(a11,a3),f5(a11,a3))),f5(x22562,x22563)),f5(a3,a11),f5(a3,a11))),
% 117.83/117.92 inference(scs_inference,[],[54,98,2239,58,2246,147,131,1060,1973,2192,2171,1882,1878,1884,978,1929,941,1886,192,134,57,103,63,67,68,82,13,16,23,70,72,4,5,6,7,8,9,14,15,17,18,19,20,21,22,24,25,26,27,69,10,11,12,81,78,76,2,37,38,41,75,85,86,66,36,33,83])).
% 117.83/117.92 cnf(2259,plain,
% 117.83/117.92 (P3(f20(x22591,f6(a1,f5(f4(a1,x22592),f4(a1,x22593))),x22594))),
% 117.83/117.92 inference(scs_inference,[],[54,98,2239,58,2246,147,131,1060,1973,2192,2171,2181,1882,1878,1884,978,1929,941,1886,124,192,52,134,57,103,63,67,68,82,13,16,23,70,72,4,5,6,7,8,9,14,15,17,18,19,20,21,22,24,25,26,27,69,10,11,12,81,78,76,2,37,38,41,75,85,86,66,36,33,83,39,92])).
% 117.83/117.92 cnf(2261,plain,
% 117.83/117.92 (~P4(f17(f6(f4(a1,x22611),f5(a11,x22612)),a3),x22613)),
% 117.83/117.92 inference(scs_inference,[],[54,98,2239,58,2246,2165,147,131,1060,1973,2192,2171,2181,1882,1878,1884,978,1929,941,1886,124,192,52,1058,134,57,103,63,67,68,82,13,16,23,70,72,4,5,6,7,8,9,14,15,17,18,19,20,21,22,24,25,26,27,69,10,11,12,81,78,76,2,37,38,41,75,85,86,66,36,33,83,39,92,34])).
% 117.83/117.92 cnf(2264,plain,
% 117.83/117.92 (P6(f5(a3,a11),f16(f6(x22641,f5(x22642,f5(a11,a3))),x22642))),
% 117.83/117.92 inference(scs_inference,[],[54,98,2239,58,2246,2165,147,131,1060,1973,2192,2171,2181,1882,1878,1884,978,1929,941,1886,124,192,597,52,1058,134,57,103,63,67,68,82,13,16,23,70,72,4,5,6,7,8,9,14,15,17,18,19,20,21,22,24,25,26,27,69,10,11,12,81,78,76,2,37,38,41,75,85,86,66,36,33,83,39,92,34,31])).
% 117.83/117.92 cnf(2266,plain,
% 117.83/117.92 (P6(f16(f6(x22661,f5(x22662,f5(a11,a3))),x22662),f5(a3,a11))),
% 117.83/117.92 inference(scs_inference,[],[54,98,2239,58,2246,2165,147,131,1060,1973,2192,2171,2181,1882,1878,1884,978,1929,941,1886,124,192,597,609,52,1058,134,57,103,63,67,68,82,13,16,23,70,72,4,5,6,7,8,9,14,15,17,18,19,20,21,22,24,25,26,27,69,10,11,12,81,78,76,2,37,38,41,75,85,86,66,36,33,83,39,92,34,31,32])).
% 117.83/117.92 cnf(2268,plain,
% 117.83/117.92 (P1(a1,f16(f6(x22681,f5(f4(x22682,a3),f4(a1,x22683))),f4(x22682,a11)))),
% 117.83/117.92 inference(scs_inference,[],[54,98,2239,58,2246,2165,147,131,1060,1973,2192,2171,2181,2168,1882,1878,1884,978,1929,941,1886,124,192,597,609,52,1134,1058,134,57,103,63,67,68,82,13,16,23,70,72,4,5,6,7,8,9,14,15,17,18,19,20,21,22,24,25,26,27,69,10,11,12,81,78,76,2,37,38,41,75,85,86,66,36,33,83,39,92,34,31,32,29])).
% 117.83/117.92 cnf(2271,plain,
% 117.83/117.92 (P1(f15(f20(a3,x22711,x22712),a11),f17(f6(f15(f20(a11,x22711,x22712),a3),f5(x22713,x22714)),x22713))),
% 117.83/117.92 inference(scs_inference,[],[54,98,2239,58,2246,2165,147,131,1060,1973,2192,2171,2181,2168,1882,1878,1884,978,1929,941,1886,124,192,597,609,52,1134,527,1058,134,57,103,63,67,68,82,13,16,23,70,72,4,5,6,7,8,9,14,15,17,18,19,20,21,22,24,25,26,27,69,10,11,12,81,78,76,2,37,38,41,75,85,86,66,36,33,83,39,92,34,31,32,29,28])).
% 117.83/117.92 cnf(2275,plain,
% 117.83/117.92 (~P9(f16(f6(x22751,f5(f4(x22752,a3),f4(a1,x22753))),f4(x22752,a11)),a1)),
% 117.83/117.92 inference(scs_inference,[],[2268,2259,91,92])).
% 117.83/117.92 cnf(2276,plain,
% 117.83/117.92 (P8(f6(f6(f6(x22761,f5(f5(a11,a3),f5(a11,a3))),f5(x22762,x22763)),f5(x22764,x22765)),f5(a3,a11),f5(a3,a11))),
% 117.83/117.92 inference(scs_inference,[],[2256,83])).
% 117.83/117.92 cnf(2278,plain,
% 117.83/117.92 (P6(f16(f6(x22781,f5(x22782,a3)),x22782),f18(f8(a11),f7(a11)))),
% 117.83/117.92 inference(scs_inference,[],[2256,1541,83,69])).
% 117.83/117.92 cnf(2280,plain,
% 117.83/117.92 (P4(f6(x22801,f5(f18(f20(x22802,a1,x22803),x22804),x22805)),f20(x22802,a1,a3))),
% 117.83/117.92 inference(scs_inference,[],[2231,2256,1541,83,69,70])).
% 117.83/117.92 cnf(2287,plain,
% 117.83/117.92 (E(f6(f4(x22871,f4(a1,x22872)),f5(x22873,a1)),f4(f6(x22871,f5(x22873,a1)),f4(a1,x22872)))),
% 117.83/117.92 inference(scs_inference,[],[2231,2256,2266,1541,107,83,69,70,63,67,5,78])).
% 117.83/117.92 cnf(2289,plain,
% 117.83/117.92 (P4(f6(f6(x22891,f5(a2,x22892)),f5(x22893,x22894)),f7(f20(x22895,a1,x22896)))),
% 117.83/117.92 inference(scs_inference,[],[2231,2256,2266,1961,1541,107,83,69,70,63,67,5,78,72])).
% 117.83/117.92 cnf(2292,plain,
% 117.83/117.92 (E(f20(x22921,f18(f20(x22922,a1,x22923),x22924),x22925),f20(x22921,f20(x22922,a1,a3),x22925))),
% 117.83/117.92 inference(scs_inference,[],[2231,2256,2266,1961,1541,107,83,69,70,63,67,5,78,72,27,11])).
% 117.83/117.92 cnf(2295,plain,
% 117.83/117.92 (E(f15(x22951,f18(f20(x22952,a1,x22953),x22954)),f15(x22951,f20(x22952,a1,a3)))),
% 117.83/117.92 inference(scs_inference,[],[2231,2256,2266,1961,1541,107,83,69,70,63,67,5,78,72,27,11,68,25])).
% 117.83/117.92 cnf(2296,plain,
% 117.83/117.92 (E(f5(x22961,f18(f20(x22962,a1,x22963),x22964)),f5(x22961,f20(x22962,a1,a3)))),
% 117.83/117.92 inference(scs_inference,[],[2231,2256,2266,1961,1541,107,83,69,70,63,67,5,78,72,27,11,68,25,7])).
% 117.83/117.92 cnf(2301,plain,
% 117.83/117.92 (E(f17(x23011,f18(f20(x23012,a1,x23013),x23014)),f17(x23011,f20(x23012,a1,a3)))),
% 117.83/117.92 inference(scs_inference,[],[2231,2261,2256,2266,1961,1541,107,83,69,70,63,67,5,78,72,27,11,68,25,7,82,4,26,15])).
% 117.83/117.92 cnf(2303,plain,
% 117.83/117.92 (E(f15(f18(f20(x23031,a1,x23032),x23033),x23034),f15(f20(x23031,a1,a3),x23034))),
% 117.83/117.92 inference(scs_inference,[],[2231,2261,2256,2266,1961,1541,107,83,69,70,63,67,5,78,72,27,11,68,25,7,82,4,26,15,6,24])).
% 117.83/117.92 cnf(2310,plain,
% 117.83/117.92 (E(f8(f18(f20(x23101,a1,x23102),x23103)),f8(f20(x23101,a1,a3)))),
% 117.83/117.92 inference(scs_inference,[],[2231,2261,2256,2266,1961,1541,107,83,69,70,63,67,5,78,72,27,11,68,25,7,82,4,26,15,6,24,16,20,9,8,17,14,13])).
% 117.83/117.92 cnf(2311,plain,
% 117.83/117.92 (E(f13(x23111,f18(f20(x23112,a1,x23113),x23114)),f13(x23111,f20(x23112,a1,a3)))),
% 117.83/117.92 inference(scs_inference,[],[2231,2261,2256,2266,1961,1541,107,83,69,70,63,67,5,78,72,27,11,68,25,7,82,4,26,15,6,24,16,20,9,8,17,14,13,22])).
% 117.83/117.92 cnf(2314,plain,
% 117.83/117.92 (E(f18(f18(f20(x23141,a1,x23142),x23143),x23144),f18(f20(x23141,a1,a3),x23144))),
% 117.83/117.92 inference(scs_inference,[],[2231,2261,2256,2266,1961,1541,107,83,69,70,63,67,5,78,72,27,11,68,25,7,82,4,26,15,6,24,16,20,9,8,17,14,13,22,76,19])).
% 117.83/117.92 cnf(2315,plain,
% 117.83/117.92 (E(f20(x23151,x23152,f18(f20(x23153,a1,x23154),x23155)),f20(x23151,x23152,f20(x23153,a1,a3)))),
% 117.83/117.92 inference(scs_inference,[],[2231,2261,2256,2266,1961,1541,107,83,69,70,63,67,5,78,72,27,11,68,25,7,82,4,26,15,6,24,16,20,9,8,17,14,13,22,76,19,12])).
% 117.83/117.92 cnf(2316,plain,
% 117.83/117.92 (E(f7(f18(f20(x23161,a1,x23162),x23163)),f7(f20(x23161,a1,a3)))),
% 117.83/117.92 inference(scs_inference,[],[2231,2261,2256,2266,1961,1541,107,83,69,70,63,67,5,78,72,27,11,68,25,7,82,4,26,15,6,24,16,20,9,8,17,14,13,22,76,19,12,23])).
% 117.83/117.92 cnf(2317,plain,
% 117.83/117.92 (E(f13(f18(f20(x23171,a1,x23172),x23173),x23174),f13(f20(x23171,a1,a3),x23174))),
% 117.83/117.92 inference(scs_inference,[],[2231,2261,2256,2266,1961,1541,107,83,69,70,63,67,5,78,72,27,11,68,25,7,82,4,26,15,6,24,16,20,9,8,17,14,13,22,76,19,12,23,21])).
% 117.83/117.92 cnf(2318,plain,
% 117.83/117.92 (E(f16(x23181,f18(f20(x23182,a1,x23183),x23184)),f16(x23181,f20(x23182,a1,a3)))),
% 117.83/117.92 inference(scs_inference,[],[2231,2261,2256,2266,1961,1541,107,83,69,70,63,67,5,78,72,27,11,68,25,7,82,4,26,15,6,24,16,20,9,8,17,14,13,22,76,19,12,23,21,18])).
% 117.83/117.92 cnf(2319,plain,
% 117.83/117.92 (E(f20(f18(f20(x23191,a1,x23192),x23193),x23194,x23195),f20(f20(x23191,a1,a3),x23194,x23195))),
% 117.83/117.92 inference(scs_inference,[],[2231,2261,2256,2266,1961,1541,107,83,69,70,63,67,5,78,72,27,11,68,25,7,82,4,26,15,6,24,16,20,9,8,17,14,13,22,76,19,12,23,21,18,10])).
% 117.83/117.92 cnf(2321,plain,
% 117.83/117.92 (P8(f17(f6(f6(a3,f5(f5(a11,a3),f5(a11,a3))),f5(x23211,x23212)),x23211),f5(a3,a11),f5(a3,a11))),
% 117.83/117.92 inference(scs_inference,[],[2231,2243,2261,2256,2254,2266,1961,1541,822,107,83,69,70,63,67,5,78,72,27,11,68,25,7,82,4,26,15,6,24,16,20,9,8,17,14,13,22,76,19,12,23,21,18,10,2,41])).
% 117.83/117.92 cnf(2329,plain,
% 117.83/117.92 (~P9(f8(f20(x23291,a1,x23292)),f18(f20(x23291,a1,x23293),x23294))),
% 117.83/117.92 inference(scs_inference,[],[2231,2243,2261,2256,2254,2266,2217,2188,568,1961,1541,822,107,83,69,70,63,67,5,78,72,27,11,68,25,7,82,4,26,15,6,24,16,20,9,8,17,14,13,22,76,19,12,23,21,18,10,2,41,75,37,38])).
% 117.83/117.92 cnf(2330,plain,
% 117.83/117.92 (E(f18(f20(x23301,a1,x23302),x23303),f20(x23301,a1,a3))),
% 117.83/117.92 inference(rename_variables,[],[2231])).
% 117.83/117.92 cnf(2331,plain,
% 117.83/117.92 (~P5(f18(f20(x23311,a1,x23312),x23313),x23314)),
% 117.83/117.92 inference(scs_inference,[],[2199,2231,2330,2243,2261,2256,2254,2266,2217,2188,568,1961,1541,822,107,83,69,70,63,67,5,78,72,27,11,68,25,7,82,4,26,15,6,24,16,20,9,8,17,14,13,22,76,19,12,23,21,18,10,2,41,75,37,38,39])).
% 117.83/117.92 cnf(2333,plain,
% 117.83/117.92 (~E(f4(f6(x23331,f5(x23332,a3)),a11),f17(f6(f4(a1,x23333),f5(a3,x23334)),a11))),
% 117.83/117.92 inference(scs_inference,[],[2199,2231,2330,2243,2261,2256,2254,1771,2233,2266,2217,2188,568,1961,1541,822,107,83,69,70,63,67,5,78,72,27,11,68,25,7,82,4,26,15,6,24,16,20,9,8,17,14,13,22,76,19,12,23,21,18,10,2,41,75,37,38,39,3])).
% 117.83/117.92 cnf(2336,plain,
% 117.83/117.92 (~E(f13(f20(a9,a10,a11),a12),f17(f6(f20(x23361,a1,a3),f5(x23362,x23363)),x23362))),
% 117.83/117.92 inference(scs_inference,[],[54,2199,2231,2330,2243,529,2261,2256,2254,1771,2233,2266,2217,2188,568,1961,1541,822,107,83,69,70,63,67,5,78,72,27,11,68,25,7,82,4,26,15,6,24,16,20,9,8,17,14,13,22,76,19,12,23,21,18,10,2,41,75,37,38,39,3,36])).
% 117.83/117.92 cnf(2337,plain,
% 117.83/117.92 (~E(f17(f6(f17(f6(f6(x23371,f5(x23372,x23373)),f5(a3,x23374)),a11),f5(x23375,x23376)),x23375),f4(a1,x23377))),
% 117.83/117.92 inference(scs_inference,[],[54,2199,2231,2330,2243,529,2261,2256,2254,1771,2233,2266,2217,2188,2184,568,1961,1541,113,822,107,83,69,70,63,67,5,78,72,27,11,68,25,7,82,4,26,15,6,24,16,20,9,8,17,14,13,22,76,19,12,23,21,18,10,2,41,75,37,38,39,3,36,33])).
% 117.83/117.92 cnf(2343,plain,
% 117.83/117.92 (P6(f16(f6(x23431,f5(x23432,a11)),x23432),f18(f8(a3),f7(a3)))),
% 117.83/117.92 inference(scs_inference,[],[2276,191,83,69])).
% 117.83/117.92 cnf(2347,plain,
% 117.83/117.92 (P4(f6(f6(f6(x23471,f5(a2,x23472)),f5(x23473,x23474)),f5(x23475,x23476)),f7(f20(x23477,a1,x23478)))),
% 117.83/117.92 inference(scs_inference,[],[2289,2278,2276,191,83,69,68,72])).
% 117.83/117.92 cnf(2355,plain,
% 117.83/117.92 (E(f6(f4(x23551,a2),f5(x23552,x23553)),f4(f6(x23551,f5(x23552,x23553)),a2))),
% 117.83/117.92 inference(scs_inference,[],[2289,2278,2276,191,1915,45,83,69,68,72,67,70,63,78])).
% 117.83/117.92 cnf(2380,plain,
% 117.83/117.92 (E(f20(f15(f20(a11,x23801,x23802),a11),x23803,x23804),f20(f15(f20(a3,x23801,x23802),a3),x23803,x23804))),
% 117.83/117.92 inference(scs_inference,[],[2289,2278,2276,191,1915,45,83,69,68,72,67,70,63,78,5,76,11,7,27,25,22,15,4,14,12,26,20,13,6,17,8,21,16,24,18,9,10])).
% 117.83/117.92 cnf(2384,plain,
% 117.83/117.92 (P8(f6(x23841,f5(f5(a3,a11),f5(a3,a11))),f5(a11,a3),f5(a11,a3))),
% 117.83/117.92 inference(scs_inference,[],[2289,2278,2336,2276,191,1915,938,45,83,69,68,72,67,70,63,78,5,76,11,7,27,25,22,15,4,14,12,26,20,13,6,17,8,21,16,24,18,9,10,23,19,2,75])).
% 117.83/117.92 cnf(2388,plain,
% 117.83/117.92 (E(f17(x23881,f18(f20(x23882,a1,x23883),x23884)),f17(x23881,f20(x23882,a1,a3)))),
% 117.83/117.92 inference(rename_variables,[],[2301])).
% 117.83/117.92 cnf(2389,plain,
% 117.83/117.92 (~P9(f8(f18(f20(x23891,a1,x23892),x23893)),f18(f20(x23891,a1,x23894),x23895))),
% 117.83/117.92 inference(scs_inference,[],[2329,2289,2301,2278,2310,2336,2276,2242,191,1915,938,45,83,69,68,72,67,70,63,78,5,76,11,7,27,25,22,15,4,14,12,26,20,13,6,17,8,21,16,24,18,9,10,23,19,2,75,41,37])).
% 117.83/117.92 cnf(2391,plain,
% 117.83/117.92 (~P9(f16(f6(x23911,f5(f4(x23912,a3),f4(a1,x23913))),f4(x23912,a11)),f17(f6(f4(a1,x23914),f5(x23915,x23916)),x23915))),
% 117.83/117.92 inference(scs_inference,[],[2329,2289,2301,2278,2310,2275,2336,2276,2242,191,1915,938,45,103,83,69,68,72,67,70,63,78,5,76,11,7,27,25,22,15,4,14,12,26,20,13,6,17,8,21,16,24,18,9,10,23,19,2,75,41,37,38])).
% 117.83/117.92 cnf(2398,plain,
% 117.83/117.92 (~E(f13(f20(a9,a10,a11),a12),f17(f6(f8(f20(x23981,a1,x23982)),f5(x23983,x23984)),x23983))),
% 117.83/117.92 inference(scs_inference,[],[54,2331,2329,2289,2301,2388,2314,2278,2310,2275,128,2336,2276,2242,191,1915,938,2165,45,103,83,69,68,72,67,70,63,78,5,76,11,7,27,25,22,15,4,14,12,26,20,13,6,17,8,21,16,24,18,9,10,23,19,2,75,41,37,38,34,39,36])).
% 117.83/117.92 cnf(2408,plain,
% 117.83/117.92 (P8(f6(f6(x24081,f5(f5(a3,a11),f5(a3,a11))),f5(x24082,x24083)),f5(a11,a3),f5(a11,a3))),
% 117.83/117.92 inference(scs_inference,[],[2384,83])).
% 117.83/117.92 cnf(2410,plain,
% 117.83/117.92 (P6(f17(f6(a11,f5(x24101,x24102)),x24101),f18(f8(a3),f7(a3)))),
% 117.83/117.92 inference(scs_inference,[],[2384,276,83,69])).
% 117.83/117.92 cnf(2414,plain,
% 117.83/117.92 (P4(f6(x24141,f5(f5(a3,a3),x24142)),f17(f6(f5(a11,a11),f5(x24143,x24144)),x24143))),
% 117.83/117.92 inference(scs_inference,[],[2384,2343,276,951,83,69,68,70])).
% 117.83/117.92 cnf(2416,plain,
% 117.83/117.92 (E(f6(f4(x24161,x24162),f5(x24163,x24162)),f4(f6(x24161,f5(x24163,x24162)),x24162))),
% 117.83/117.92 inference(scs_inference,[],[2384,2343,276,951,46,83,69,68,70,78])).
% 117.83/117.92 cnf(2422,plain,
% 117.83/117.92 (P4(f6(f6(f6(f6(x24221,f5(a2,x24222)),f5(x24223,x24224)),f5(x24225,x24226)),f5(x24227,x24228)),f7(f20(x24229,a1,x242210)))),
% 117.83/117.92 inference(scs_inference,[],[2384,2347,2343,276,951,46,83,69,68,70,78,67,76,72])).
% 117.83/117.92 cnf(2451,plain,
% 117.83/117.92 (P8(f6(x24511,f5(f20(x24512,a3,x24513),f20(x24512,a3,x24513))),f20(x24512,a11,x24513),f20(x24512,a11,x24513))),
% 117.83/117.92 inference(scs_inference,[],[2384,2347,2343,2398,276,951,2164,46,83,69,68,70,78,67,76,72,11,63,27,5,7,22,25,4,16,9,15,14,17,20,24,8,21,6,12,26,13,23,19,18,10,2,75])).
% 117.83/117.92 cnf(2454,plain,
% 117.83/117.92 (E(f6(f4(x24541,a2),f5(x24542,x24543)),f4(f6(x24541,f5(x24542,x24543)),a2))),
% 117.83/117.92 inference(rename_variables,[],[2355])).
% 117.83/117.92 cnf(2461,plain,
% 117.83/117.92 (P4(f4(f6(x24611,f5(f18(f20(x24612,a1,x24613),x24614),a1)),f4(a1,x24615)),f20(x24612,a1,a3))),
% 117.83/117.92 inference(scs_inference,[],[2384,2347,2343,2355,2454,2398,2280,2238,2292,2287,544,276,951,2164,46,83,69,68,70,78,67,76,72,11,63,27,5,7,22,25,4,16,9,15,14,17,20,24,8,21,6,12,26,13,23,19,18,10,2,75,41,37,38,34])).
% 117.83/117.92 cnf(2464,plain,
% 117.83/117.92 (~E(f4(f6(x24641,f5(x24642,x24643)),a2),f17(f6(a1,f5(a3,x24644)),a11))),
% 117.83/117.92 inference(scs_inference,[],[2384,2347,2343,2355,2454,2398,2280,2238,2292,2287,1083,544,276,951,2164,46,83,69,68,70,78,67,76,72,11,63,27,5,7,22,25,4,16,9,15,14,17,20,24,8,21,6,12,26,13,23,19,18,10,2,75,41,37,38,34,3])).
% 117.83/117.92 cnf(2466,plain,
% 117.83/117.92 (~E(f13(f20(a9,a10,a11),a12),f20(x24661,x24662,a3))),
% 117.83/117.92 inference(scs_inference,[],[54,2384,2347,2343,2355,2454,2398,2280,2238,2292,2287,1083,544,276,951,60,2164,46,83,69,68,70,78,67,76,72,11,63,27,5,7,22,25,4,16,9,15,14,17,20,24,8,21,6,12,26,13,23,19,18,10,2,75,41,37,38,34,3,36])).
% 117.83/117.92 cnf(2467,plain,
% 117.83/117.92 (~E(f17(f6(f6(x24671,f5(x24672,x24673)),f5(a3,x24674)),a11),f16(f6(x24675,f5(x24676,a1)),x24676))),
% 117.83/117.92 inference(scs_inference,[],[54,2384,2347,2343,2355,2454,2398,2280,2238,2292,2287,1083,544,276,951,60,498,1063,2164,46,83,69,68,70,78,67,76,72,11,63,27,5,7,22,25,4,16,9,15,14,17,20,24,8,21,6,12,26,13,23,19,18,10,2,75,41,37,38,34,3,36,33])).
% 117.83/117.92 cnf(2470,plain,
% 117.83/117.92 (P6(f7(f20(x24701,a1,x24702)),f18(f8(a2),f7(a2)))),
% 117.83/117.92 inference(scs_inference,[],[2451,631,83,69])).
% 117.83/117.92 cnf(2472,plain,
% 117.83/117.92 (P4(f6(x24721,f5(f5(a3,a11),x24722)),f17(f6(f5(a11,a3),f5(x24723,x24724)),x24723))),
% 117.83/117.92 inference(scs_inference,[],[2451,631,923,83,69,70])).
% 117.83/117.92 cnf(2478,plain,
% 117.83/117.92 (E(f6(f4(x24781,a3),f5(x24782,a11)),f4(f6(x24781,f5(x24782,a11)),a3))),
% 117.83/117.92 inference(scs_inference,[],[2451,2410,631,923,132,83,69,70,67,68,78])).
% 117.83/117.92 cnf(2484,plain,
% 117.83/117.92 (P4(f6(f6(f6(f6(f6(x24841,f5(a2,x24842)),f5(x24843,x24844)),f5(x24845,x24846)),f5(x24847,x24848)),f5(x24849,x248410)),f7(f20(x248411,a1,x248412)))),
% 117.83/117.92 inference(scs_inference,[],[2451,2410,2422,631,923,132,83,69,70,67,68,78,63,76,72])).
% 117.83/117.92 cnf(2511,plain,
% 117.83/117.92 (~P8(f6(a1,f5(f13(f20(a9,a10,a11),a12),x25111)),f20(x25112,x25113,a3),x25114)),
% 117.83/117.92 inference(scs_inference,[],[2466,2451,2410,2422,631,923,58,132,83,69,70,67,68,78,63,76,72,11,5,14,4,27,7,17,8,25,6,21,22,9,24,12,15,18,16,20,10,23,19,13,26,2,86])).
% 117.83/117.92 cnf(2512,plain,
% 117.83/117.92 (~P8(a1,x25121,x25122)),
% 117.83/117.92 inference(rename_variables,[],[58])).
% 117.83/117.92 cnf(2517,plain,
% 117.83/117.92 (P8(f6(x25171,f5(f4(a1,x25172),f4(a1,x25172))),f4(a1,x25173),f4(a1,x25173))),
% 117.83/117.92 inference(scs_inference,[],[2466,2451,2410,2422,631,923,150,58,2512,132,83,69,70,67,68,78,63,76,72,11,5,14,4,27,7,17,8,25,6,21,22,9,24,12,15,18,16,20,10,23,19,13,26,2,86,85,75])).
% 117.83/117.92 cnf(2523,plain,
% 117.83/117.92 (~P4(f6(a1,f5(f13(f20(a9,a10,a11),a12),x25231)),f20(x25232,x25233,a3))),
% 117.83/117.92 inference(scs_inference,[],[2466,2451,2410,2422,2391,157,631,923,150,58,2512,2066,1134,57,132,83,69,70,67,68,78,63,76,72,11,5,14,4,27,7,17,8,25,6,21,22,9,24,12,15,18,16,20,10,23,19,13,26,2,86,85,75,37,38,77])).
% 117.83/117.92 cnf(2526,plain,
% 117.83/117.92 (~E(f4(f6(x25261,f5(x25262,x25263)),x25263),f16(f6(x25264,f5(f4(x25265,a3),a1)),f4(x25265,a11)))),
% 117.83/117.92 inference(scs_inference,[],[2466,2451,2410,2416,2422,2391,1112,157,631,923,150,58,2512,2066,1134,57,132,83,69,70,67,68,78,63,76,72,11,5,14,4,27,7,17,8,25,6,21,22,9,24,12,15,18,16,20,10,23,19,13,26,2,86,85,75,37,38,77,3])).
% 117.83/117.92 cnf(2527,plain,
% 117.83/117.92 (E(f6(f4(x25271,x25272),f5(x25273,x25272)),f4(f6(x25271,f5(x25273,x25272)),x25272))),
% 117.83/117.92 inference(rename_variables,[],[2416])).
% 117.83/117.92 cnf(2529,plain,
% 117.83/117.92 (~E(f20(f15(a9,a12),f6(a10,f5(a12,a2)),a11),f17(f6(f20(a9,a10,a11),f5(x25291,x25292)),x25291))),
% 117.83/117.92 inference(scs_inference,[],[2466,2451,307,2410,2416,2422,2391,1112,157,631,923,147,150,58,2512,2066,1134,57,132,83,69,70,67,68,78,63,76,72,11,5,14,4,27,7,17,8,25,6,21,22,9,24,12,15,18,16,20,10,23,19,13,26,2,86,85,75,37,38,77,3,36])).
% 117.83/117.92 cnf(2532,plain,
% 117.83/117.92 (P3(f20(x25321,f6(f6(a1,f5(f4(a1,x25322),f4(a1,x25323))),f5(a3,a11)),x25324))),
% 117.83/117.92 inference(scs_inference,[],[2466,2451,307,2410,2416,2422,2391,1112,157,631,923,147,2259,150,58,2512,2066,126,1134,134,57,132,83,69,70,67,68,78,63,76,72,11,5,14,4,27,7,17,8,25,6,21,22,9,24,12,15,18,16,20,10,23,19,13,26,2,86,85,75,37,38,77,3,36,74,92])).
% 117.83/117.92 cnf(2537,plain,
% 117.83/117.92 (P1(f15(f20(a3,x25371,x25372),a11),f15(f20(a11,x25371,x25372),a3))),
% 117.83/117.92 inference(scs_inference,[],[2466,2451,307,2410,2416,2527,2422,2271,2391,1112,157,631,923,147,2259,150,58,2512,2066,126,525,1134,134,57,132,83,69,70,67,68,78,63,76,72,11,5,14,4,27,7,17,8,25,6,21,22,9,24,12,15,18,16,20,10,23,19,13,26,2,86,85,75,37,38,77,3,36,74,92,41,66])).
% 117.83/117.92 cnf(2538,plain,
% 117.83/117.92 (P1(f15(f20(a3,x25381,x25382),a11),f17(f6(f15(f20(a11,x25381,x25382),a3),f5(x25383,x25384)),x25383))),
% 117.83/117.92 inference(rename_variables,[],[2271])).
% 117.83/117.92 cnf(2542,plain,
% 117.83/117.92 (E(f20(f15(f20(a11,x25421,x25422),a11),x25423,x25424),f20(f15(f20(a3,x25421,x25422),a3),x25423,x25424))),
% 117.83/117.92 inference(rename_variables,[],[2380])).
% 117.83/117.92 cnf(2547,plain,
% 117.83/117.92 (P1(f15(f20(a3,x25471,x25472),a11),f15(f20(a11,x25471,x25472),a11))),
% 117.83/117.92 inference(scs_inference,[],[2466,2451,307,2410,2416,2527,2422,2271,2538,2380,2542,2391,1112,157,806,804,631,923,147,2259,150,58,2512,2066,126,525,1560,1134,134,57,132,83,69,70,67,68,78,63,76,72,11,5,14,4,27,7,17,8,25,6,21,22,9,24,12,15,18,16,20,10,23,19,13,26,2,86,85,75,37,38,77,3,36,74,92,41,66,31,32,29])).
% 117.83/117.92 cnf(2556,plain,
% 117.83/117.92 (P6(f7(f20(x25561,a1,x25562)),f13(f18(f8(a2),f7(a2)),x25563))),
% 117.83/117.92 inference(scs_inference,[],[2470,2517,403,83,69,67])).
% 117.83/117.92 cnf(2558,plain,
% 117.83/117.92 (P4(f6(x25581,f5(f5(a11,a11),x25582)),f17(f6(f5(a3,a3),f5(x25583,x25584)),x25583))),
% 117.83/117.92 inference(scs_inference,[],[2470,2517,403,945,83,69,67,70])).
% 117.83/117.92 cnf(2560,plain,
% 117.83/117.92 (P6(f7(f20(x25601,a1,x25602)),f18(f18(f8(a2),f7(a2)),x25603))),
% 117.83/117.92 inference(scs_inference,[],[2470,2517,403,945,83,69,67,70,68])).
% 117.83/117.92 cnf(2562,plain,
% 117.83/117.92 (P6(f7(f20(x25621,a1,x25622)),f8(f18(f8(a2),f7(a2))))),
% 117.83/117.92 inference(scs_inference,[],[2470,2517,403,945,83,69,67,70,68,63])).
% 117.83/117.92 cnf(2568,plain,
% 117.83/117.92 (E(f20(x25681,f5(a11,a11),x25682),f20(x25681,f17(f6(f5(a3,a3),f5(x25683,x25684)),x25683),x25682))),
% 117.83/117.92 inference(scs_inference,[],[2470,2517,2484,1952,403,945,83,69,67,70,68,63,72,76,11])).
% 117.83/117.92 cnf(2594,plain,
% 117.83/117.92 (E(f13(f20(x25941,x25942,x25943),x25944),f20(f15(x25941,x25944),f6(x25942,f5(x25944,a2)),x25943))),
% 117.83/117.92 inference(rename_variables,[],[306])).
% 117.83/117.92 cnf(2596,plain,
% 117.83/117.92 (P8(f6(x25961,f5(f6(a3,a3),f6(a3,a3))),f6(a11,a11),f6(a11,a11))),
% 117.83/117.92 inference(scs_inference,[],[2470,2517,2511,2484,2529,1952,403,945,1358,306,83,69,67,70,68,63,72,76,11,14,5,17,21,4,7,22,27,18,12,13,25,26,16,15,6,24,19,23,8,9,10,20,2,42,75])).
% 117.83/117.92 cnf(2598,plain,
% 117.83/117.92 (~P9(f20(f18(f20(x25981,a1,x25982),x25983),x25984,f4(f20(x25985,a11,x25986),x25987)),f20(f20(x25981,a1,a3),x25984,f4(f20(x25985,a3,x25986),x25987)))),
% 117.83/117.92 inference(scs_inference,[],[2470,2517,2511,2484,2529,2240,2319,1952,403,945,1358,306,83,69,67,70,68,63,72,76,11,14,5,17,21,4,7,22,27,18,12,13,25,26,16,15,6,24,19,23,8,9,10,20,2,42,75,37])).
% 117.83/117.92 cnf(2599,plain,
% 117.83/117.92 (E(f20(f18(f20(x25991,a1,x25992),x25993),x25994,x25995),f20(f20(x25991,a1,a3),x25994,x25995))),
% 117.83/117.92 inference(rename_variables,[],[2319])).
% 117.83/117.92 cnf(2600,plain,
% 117.83/117.92 (~P9(f20(x26001,x26002,f4(f20(x26003,a11,x26004),x26005)),f20(x26001,x26002,f4(f20(x26003,a3,x26004),x26005)))),
% 117.83/117.92 inference(rename_variables,[],[2240])).
% 117.83/117.92 cnf(2601,plain,
% 117.83/117.92 (~P9(f20(f20(x26011,a1,a3),x26012,f4(f20(x26013,a11,x26014),x26015)),f20(f18(f20(x26011,a1,x26016),x26017),x26012,f4(f20(x26013,a3,x26014),x26015)))),
% 117.83/117.92 inference(scs_inference,[],[2470,2517,2511,2484,2529,2240,2600,2319,2599,1952,403,945,1358,306,83,69,67,70,68,63,72,76,11,14,5,17,21,4,7,22,27,18,12,13,25,26,16,15,6,24,19,23,8,9,10,20,2,42,75,37,38])).
% 117.83/117.92 cnf(2604,plain,
% 117.83/117.92 (~E(f4(f6(x26041,f5(x26042,a11)),a3),f16(f6(x26043,f5(x26044,a1)),x26044))),
% 117.83/117.92 inference(scs_inference,[],[2470,2517,2478,2511,2484,2529,2240,2600,2319,2599,1952,403,945,505,1358,306,83,69,67,70,68,63,72,76,11,14,5,17,21,4,7,22,27,18,12,13,25,26,16,15,6,24,19,23,8,9,10,20,2,42,75,37,38,3])).
% 117.83/117.92 cnf(2606,plain,
% 117.83/117.92 (~E(f13(f20(a9,a10,a11),a12),f8(f20(x26061,a1,x26062)))),
% 117.83/117.92 inference(scs_inference,[],[54,2470,2517,2478,2511,2484,2529,2240,2600,2319,2599,1952,403,945,505,100,1358,306,83,69,67,70,68,63,72,76,11,14,5,17,21,4,7,22,27,18,12,13,25,26,16,15,6,24,19,23,8,9,10,20,2,42,75,37,38,3,36])).
% 117.83/117.92 cnf(2609,plain,
% 117.83/117.92 (~P4(f6(a1,f5(f13(f20(a9,a10,a11),a12),x26091)),f13(f20(x26092,x26093,a3),x26094))),
% 117.83/117.92 inference(scs_inference,[],[54,2470,2517,2478,2511,2523,2484,2529,2240,2600,2319,2599,1952,403,945,505,100,1358,306,2594,107,83,69,67,70,68,63,72,76,11,14,5,17,21,4,7,22,27,18,12,13,25,26,16,15,6,24,19,23,8,9,10,20,2,42,75,37,38,3,36,93,35])).
% 117.83/117.92 cnf(2612,plain,
% 117.83/117.92 (P8(f6(f6(x26121,f5(f6(a3,a3),f6(a3,a3))),f5(x26122,x26123)),f6(a11,a11),f6(a11,a11))),
% 117.83/117.92 inference(scs_inference,[],[2596,83])).
% 117.83/117.92 cnf(2616,plain,
% 117.83/117.92 (P4(f6(x26161,f5(f5(a11,a3),x26162)),f17(f6(f5(a3,a11),f5(x26163,x26164)),x26163))),
% 117.83/117.92 inference(scs_inference,[],[2596,917,989,83,69,70])).
% 117.83/117.92 cnf(2652,plain,
% 117.83/117.92 (~E(f8(f20(x26521,a1,x26522)),f13(f20(a9,a10,a11),a12))),
% 117.83/117.92 inference(scs_inference,[],[2606,2596,2556,2414,1875,917,989,83,69,70,67,68,63,72,76,17,14,13,11,22,5,21,25,7,24,4,15,19,18,6,12,16,20,10,9,27,8,26,23,2])).
% 117.83/117.92 cnf(2653,plain,
% 117.83/117.92 (P8(f6(x26531,f5(f5(a11,a11),f5(a11,a11))),f5(a3,a3),f5(a3,a3))),
% 117.83/117.92 inference(scs_inference,[],[2606,2596,2556,2414,1875,917,989,931,83,69,70,67,68,63,72,76,17,14,13,11,22,5,21,25,7,24,4,15,19,18,6,12,16,20,10,9,27,8,26,23,2,75])).
% 117.83/117.92 cnf(2655,plain,
% 117.83/117.92 (~P9(f16(f6(x26551,f5(f4(x26552,a11),a11)),f4(x26552,a3)),a3)),
% 117.83/117.92 inference(scs_inference,[],[2606,2596,2556,2414,164,1875,917,989,931,2037,83,69,70,67,68,63,72,76,17,14,13,11,22,5,21,25,7,24,4,15,19,18,6,12,16,20,10,9,27,8,26,23,2,75,37])).
% 117.83/117.92 cnf(2656,plain,
% 117.83/117.92 (~P9(a11,f16(f6(x26561,f5(f4(x26562,a3),a11)),f4(x26562,a11)))),
% 117.83/117.92 inference(scs_inference,[],[2606,2596,2556,2414,164,1875,917,989,1998,931,2037,83,69,70,67,68,63,72,76,17,14,13,11,22,5,21,25,7,24,4,15,19,18,6,12,16,20,10,9,27,8,26,23,2,75,37,38])).
% 117.83/117.92 cnf(2660,plain,
% 117.83/117.92 (~E(f17(f6(f13(f20(a9,a10,a11),a12),f5(a3,x26601)),a11),f17(f6(f20(x26602,a1,a3),f5(x26603,x26604)),x26603))),
% 117.83/117.92 inference(scs_inference,[],[2606,2596,2556,1066,2414,2568,164,2315,1875,917,529,989,1998,931,2037,83,69,70,67,68,63,72,76,17,14,13,11,22,5,21,25,7,24,4,15,19,18,6,12,16,20,10,9,27,8,26,23,2,75,37,38,3,36])).
% 117.83/117.92 cnf(2665,plain,
% 117.83/117.92 (P8(f6(f6(x26651,f5(f5(a11,a11),f5(a11,a11))),f5(x26652,x26653)),f5(a3,a3),f5(a3,a3))),
% 117.83/117.92 inference(scs_inference,[],[2653,83])).
% 117.83/117.92 cnf(2682,plain,
% 117.83/117.92 (E(f20(x26821,f17(f6(f5(a11,a3),f5(x26822,x26823)),x26822),x26824),f20(x26821,f5(a3,a11),x26824))),
% 117.83/117.92 inference(scs_inference,[],[2653,2560,2472,1958,920,468,553,83,69,67,63,70,68,72,76,14,11])).
% 117.83/117.92 cnf(2703,plain,
% 117.83/117.92 (E(f16(x27031,f17(f6(f5(a11,a3),f5(x27032,x27033)),x27032)),f16(x27031,f5(a3,a11)))),
% 117.83/117.92 inference(scs_inference,[],[2653,2560,2472,1958,920,468,553,83,69,67,63,70,68,72,76,14,11,15,25,17,22,13,21,19,5,20,24,12,10,23,4,16,6,26,7,8,27,18])).
% 117.83/117.92 cnf(2706,plain,
% 117.83/117.92 (P8(f6(x27061,f5(f5(a3,a3),f5(a3,a3))),f5(a11,a11),f5(a11,a11))),
% 117.83/117.92 inference(scs_inference,[],[2653,2560,2472,2604,1958,920,468,553,934,83,69,67,63,70,68,72,76,14,11,15,25,17,22,13,21,19,5,20,24,12,10,23,4,16,6,26,7,8,27,18,9,2,75])).
% 117.83/117.92 cnf(2708,plain,
% 117.83/117.92 (~P9(f20(f18(f20(x27081,a1,x27082),x27083),x27084,f4(f20(x27085,a3,x27086),x27087)),f20(f20(x27081,a1,a3),x27084,f4(f20(x27085,a3,x27086),x27087)))),
% 117.83/117.92 inference(scs_inference,[],[2653,2560,2472,2604,2598,1958,920,468,553,2192,934,83,69,67,63,70,68,72,76,14,11,15,25,17,22,13,21,19,5,20,24,12,10,23,4,16,6,26,7,8,27,18,9,2,75,37])).
% 117.83/117.92 cnf(2713,plain,
% 117.83/117.92 (~E(f13(f20(a9,a10,a11),a12),f20(a9,a10,a11))),
% 117.83/117.92 inference(scs_inference,[],[54,2653,2389,2560,2472,2604,2598,1958,920,468,2314,553,2192,59,934,83,69,67,63,70,68,72,76,14,11,15,25,17,22,13,21,19,5,20,24,12,10,23,4,16,6,26,7,8,27,18,9,2,75,37,38,36])).
% 117.83/117.93 cnf(2714,plain,
% 117.83/117.93 (~E(f17(f6(f6(x27141,f5(x27142,x27143)),f5(a11,x27144)),a3),f4(a1,x27145))),
% 117.83/117.93 inference(scs_inference,[],[54,2653,2389,2560,2472,2604,2598,1958,920,468,1973,2314,553,113,2192,59,934,83,69,67,63,70,68,72,76,14,11,15,25,17,22,13,21,19,5,20,24,12,10,23,4,16,6,26,7,8,27,18,9,2,75,37,38,36,33])).
% 117.83/117.93 cnf(2759,plain,
% 117.83/117.93 (P8(f6(x27591,f5(f6(a3,a11),f6(a3,a11))),f6(a11,a3),f6(a11,a3))),
% 117.83/117.93 inference(scs_inference,[],[2713,2706,2562,2558,1896,914,1918,626,1351,83,69,67,63,68,70,76,72,11,15,21,20,25,22,14,16,10,6,12,17,13,23,8,26,24,19,5,27,4,7,18,9,2,75])).
% 117.83/117.93 cnf(2763,plain,
% 117.83/117.93 (~E(f16(f6(x27631,f5(x27632,f20(a9,a10,a11))),x27632),f13(f20(a9,a10,a11),a12))),
% 117.83/117.93 inference(scs_inference,[],[2713,2706,2562,2558,211,355,1896,914,1918,626,312,1984,1351,83,69,67,63,68,70,76,72,11,15,21,20,25,22,14,16,10,6,12,17,13,23,8,26,24,19,5,27,4,7,18,9,2,75,37,38,3])).
% 117.83/117.93 cnf(2765,plain,
% 117.83/117.93 (~E(f20(f15(a9,a12),f6(a10,f5(a12,a2)),a11),f17(f6(f8(f20(x27651,a1,x27652)),f5(x27653,x27654)),x27653))),
% 117.83/117.93 inference(scs_inference,[],[2713,2706,2562,2558,211,355,1896,914,307,128,1918,626,312,1984,1351,83,69,67,63,68,70,76,72,11,15,21,20,25,22,14,16,10,6,12,17,13,23,8,26,24,19,5,27,4,7,18,9,2,75,37,38,3,36])).
% 117.83/117.93 cnf(2767,plain,
% 117.83/117.93 (~P8(a1,x27671,x27672)),
% 117.83/117.93 inference(rename_variables,[],[58])).
% 117.83/117.93 cnf(2775,plain,
% 117.83/117.93 (P1(f16(f6(x27751,f5(x27752,a3)),x27752),f16(f6(x27753,f5(x27754,a3)),x27754))),
% 117.83/117.93 inference(scs_inference,[],[2713,2706,2562,2558,2532,2682,211,355,1896,1543,914,307,128,1918,1545,626,312,58,2767,1984,1351,134,83,69,67,63,68,70,76,72,11,15,21,20,25,22,14,16,10,6,12,17,13,23,8,26,24,19,5,27,4,7,18,9,2,75,37,38,3,36,86,92,85,41,66])).
% 117.83/117.93 cnf(2780,plain,
% 117.83/117.93 (P6(f8(f20(x27801,a1,x27802)),f13(f8(f20(x27801,a1,x27803)),x27804))),
% 117.83/117.93 inference(scs_inference,[],[2713,2706,2562,2558,2532,2195,2682,211,355,1896,1543,523,914,307,128,1918,1545,626,312,58,2767,1984,1351,134,57,83,69,67,63,68,70,76,72,11,15,21,20,25,22,14,16,10,6,12,17,13,23,8,26,24,19,5,27,4,7,18,9,2,75,37,38,3,36,86,92,85,41,66,77,31])).
% 117.83/117.93 cnf(2785,plain,
% 117.83/117.93 (P1(f15(f20(a3,x27851,x27852),a11),f17(f6(f15(f20(a11,x27851,x27852),a11),f5(x27853,x27854)),x27853))),
% 117.83/117.93 inference(scs_inference,[],[2713,2537,2706,2562,2558,2532,2195,2264,2682,2703,211,355,1896,1543,523,914,307,128,1918,1545,626,312,58,2767,1984,1574,1351,134,57,83,69,67,63,68,70,76,72,11,15,21,20,25,22,14,16,10,6,12,17,13,23,8,26,24,19,5,27,4,7,18,9,2,75,37,38,3,36,86,92,85,41,66,77,31,32,29])).
% 117.83/117.93 cnf(2792,plain,
% 117.83/117.93 (P6(f17(f6(f4(a1,x27921),f5(x27922,x27923)),x27922),f18(f8(a1),f7(a1)))),
% 117.83/117.93 inference(scs_inference,[],[2759,380,83,69])).
% 117.83/117.93 cnf(2812,plain,
% 117.83/117.93 (E(f20(x28121,f18(f5(a11,x28122),f5(x28123,a11)),x28124),f20(x28121,f18(f5(a3,x28122),f5(x28123,a3)),x28124))),
% 117.83/117.93 inference(scs_inference,[],[2759,2780,2616,1894,380,1715,83,69,67,63,70,72,68,76,15,21,20,16,12,22,11])).
% 117.83/117.93 cnf(2824,plain,
% 117.83/117.93 (E(f20(f18(f5(a11,x28241),f5(x28242,a11)),x28243,x28244),f20(f18(f5(a3,x28241),f5(x28242,a3)),x28243,x28244))),
% 117.83/117.93 inference(scs_inference,[],[2759,2780,2616,1894,380,1715,83,69,67,63,70,72,68,76,15,21,20,16,12,22,11,24,25,23,13,19,8,14,17,5,6,4,10])).
% 117.83/117.93 cnf(2831,plain,
% 117.83/117.93 (P8(f6(x28311,f5(f6(a11,a11),f6(a11,a11))),f6(a3,a3),f6(a3,a3))),
% 117.83/117.93 inference(scs_inference,[],[2759,2714,2780,2616,1894,380,1715,1364,83,69,67,63,70,72,68,76,15,21,20,16,12,22,11,24,25,23,13,19,8,14,17,5,6,4,10,26,7,27,9,18,2,75])).
% 117.83/117.93 cnf(2836,plain,
% 117.83/117.93 (~P9(f20(x28361,a1,a3),f8(f18(f20(x28361,a1,x28362),x28363)))),
% 117.83/117.93 inference(scs_inference,[],[2759,2714,2780,2616,2708,561,1894,2310,380,1715,2164,1364,83,69,67,63,70,72,68,76,15,21,20,16,12,22,11,24,25,23,13,19,8,14,17,5,6,4,10,26,7,27,9,18,2,75,37,38])).
% 117.83/117.93 cnf(2851,plain,
% 117.83/117.93 (P6(f17(f6(a3,f5(x28511,x28512)),x28511),f18(f8(a11),f7(a11)))),
% 117.83/117.93 inference(scs_inference,[],[2831,216,83,69])).
% 117.83/117.93 cnf(2855,plain,
% 117.83/117.93 (P4(f6(x28551,f5(f6(a11,a3),x28552)),f17(f6(f6(a3,a11),f5(x28553,x28554)),x28553))),
% 117.83/117.93 inference(scs_inference,[],[2831,2792,216,1344,83,69,67,70])).
% 117.83/117.93 cnf(2859,plain,
% 117.83/117.93 (P4(f6(f6(x28591,f5(a3,x28592)),f5(x28593,x28594)),f16(f6(x28595,f5(x28596,a11)),x28596))),
% 117.83/117.93 inference(scs_inference,[],[2831,2792,1657,216,1344,83,69,67,70,68,72])).
% 117.83/117.93 cnf(2890,plain,
% 117.83/117.93 (P8(f6(x28901,f5(f6(a11,x28902),f6(a11,x28902))),f6(a3,x28902),f6(a3,x28902))),
% 117.83/117.93 inference(scs_inference,[],[2831,2792,2333,1657,216,1344,817,83,69,67,70,68,72,63,76,16,11,15,12,21,13,23,20,8,5,25,22,10,19,4,14,24,26,6,17,7,27,9,18,2,75])).
% 117.83/117.93 cnf(2895,plain,
% 117.83/117.93 (~P4(f4(a1,x28951),x28952)),
% 117.83/117.93 inference(scs_inference,[],[2831,2792,2812,2333,1547,1550,1657,216,1344,2165,2066,817,188,83,69,67,70,68,72,63,76,16,11,15,12,21,13,23,20,8,5,25,22,10,19,4,14,24,26,6,17,7,27,9,18,2,75,37,38,39,34])).
% 117.83/117.93 cnf(2897,plain,
% 117.83/117.93 (E(f18(f20(x28971,f4(a1,x28972),x28973),x28974),f20(x28971,f4(a1,x28972),a3))),
% 117.83/117.93 inference(scs_inference,[],[2831,2792,2812,2333,1547,1550,1657,216,1344,2165,2066,817,188,83,69,67,70,68,72,63,76,16,11,15,12,21,13,23,20,8,5,25,22,10,19,4,14,24,26,6,17,7,27,9,18,2,75,37,38,39,34,81])).
% 117.83/117.93 cnf(2899,plain,
% 117.83/117.93 (~P5(f20(x28991,f4(a1,x28992),x28993),x28994)),
% 117.83/117.93 inference(scs_inference,[],[2831,2792,2812,2333,1547,1550,1657,216,1344,2165,2066,817,188,83,69,67,70,68,72,63,76,16,11,15,12,21,13,23,20,8,5,25,22,10,19,4,14,24,26,6,17,7,27,9,18,2,75,37,38,39,34,81,82])).
% 117.83/117.93 cnf(2903,plain,
% 117.83/117.93 (P6(f16(f6(x29031,f5(x29032,x29033)),x29032),f18(f8(x29033),f7(x29033)))),
% 117.83/117.93 inference(scs_inference,[],[2890,609,83,69])).
% 117.83/117.93 cnf(2913,plain,
% 117.83/117.93 (P4(f6(f6(f6(x29131,f5(a3,x29132)),f5(x29133,x29134)),f5(x29135,x29136)),f16(f6(x29137,f5(x29138,a11)),x29138))),
% 117.83/117.93 inference(scs_inference,[],[2890,2851,2859,202,609,83,69,67,70,76,68,72])).
% 117.83/117.93 cnf(2931,plain,
% 117.83/117.93 (E(f18(f8(f20(x29311,a1,x29312)),x29313),f18(f8(f20(x29311,a1,x29314)),x29313))),
% 117.83/117.93 inference(scs_inference,[],[2890,2851,2859,202,609,83,69,67,70,76,68,72,63,11,12,15,16,13,8,20,23,21,10,25,4,22,5,19])).
% 117.83/117.93 cnf(2940,plain,
% 117.83/117.93 (E(f16(x29401,f8(f20(x29402,a1,x29403))),f16(x29401,f8(f20(x29402,a1,x29404))))),
% 117.83/117.93 inference(scs_inference,[],[2890,2851,2859,202,609,83,69,67,70,76,68,72,63,11,12,15,16,13,8,20,23,21,10,25,4,22,5,19,17,26,24,14,6,7,27,9,18])).
% 117.83/117.93 cnf(2944,plain,
% 117.83/117.93 (~P5(f18(f20(x29441,f4(a1,x29442),x29443),x29444),x29445)),
% 117.83/117.93 inference(scs_inference,[],[2899,2890,2851,2897,2859,2464,202,609,159,83,69,67,70,76,68,72,63,11,12,15,16,13,8,20,23,21,10,25,4,22,5,19,17,26,24,14,6,7,27,9,18,2,75,39])).
% 117.83/117.93 cnf(2946,plain,
% 117.83/117.93 (~P9(f16(f6(x29461,f5(x29462,f5(a11,a3))),x29462),f5(a3,a11))),
% 117.83/117.93 inference(scs_inference,[],[2899,2890,2851,2897,2859,2464,606,202,938,609,159,83,69,67,70,76,68,72,63,11,12,15,16,13,8,20,23,21,10,25,4,22,5,19,17,26,24,14,6,7,27,9,18,2,75,39,38])).
% 117.83/117.93 cnf(2948,plain,
% 117.83/117.93 (~P9(f20(f20(x29481,a1,a3),x29482,f4(f20(x29483,a3,x29484),x29485)),f20(f18(f20(x29481,a1,x29486),x29487),x29482,f4(f20(x29483,a3,x29484),x29485)))),
% 117.83/117.93 inference(scs_inference,[],[2899,2890,2851,2897,2859,2464,2601,606,202,938,2192,609,159,83,69,67,70,76,68,72,63,11,12,15,16,13,8,20,23,21,10,25,4,22,5,19,17,26,24,14,6,7,27,9,18,2,75,39,38,37])).
% 117.83/117.93 cnf(2955,plain,
% 117.83/117.93 (E(f18(f20(f18(f5(a11,x29551),f5(x29552,a11)),f4(a1,x29553),x29554),x29555),f20(f18(f5(a3,x29551),f5(x29552,a3)),f4(a1,x29553),a3))),
% 117.83/117.93 inference(scs_inference,[],[2895,2899,2652,2890,2836,2851,2897,2859,2824,2464,2601,606,202,938,2192,609,159,83,69,67,70,76,68,72,63,11,12,15,16,13,8,20,23,21,10,25,4,22,5,19,17,26,24,14,6,7,27,9,18,2,75,39,38,37,77,65,3])).
% 117.83/117.93 cnf(2958,plain,
% 117.83/117.93 (~E(f17(f6(f17(f6(f6(x29581,f5(x29582,x29583)),f5(a3,x29584)),a11),f5(x29585,x29586)),x29585),a1)),
% 117.83/117.93 inference(scs_inference,[],[2895,2899,2652,2890,2836,2851,2897,2859,2824,2464,2601,606,2184,202,938,56,2192,609,159,83,69,67,70,76,68,72,63,11,12,15,16,13,8,20,23,21,10,25,4,22,5,19,17,26,24,14,6,7,27,9,18,2,75,39,38,37,77,65,3,33])).
% 117.83/117.93 cnf(2961,plain,
% 117.83/117.93 (P6(a11,f18(f8(a3),f7(a3)))),
% 117.83/117.93 inference(scs_inference,[],[2408,145,83,69])).
% 117.83/117.93 cnf(2963,plain,
% 117.83/117.93 (P4(f6(x29631,f5(f4(a1,x29632),x29633)),f16(f6(x29634,f5(x29635,a1)),x29635))),
% 117.83/117.93 inference(scs_inference,[],[2408,495,145,83,69,70])).
% 117.83/117.93 cnf(2967,plain,
% 117.83/117.93 (P5(f20(x29671,f6(x29672,f5(a1,x29673)),x29674),f4(a1,x29675))),
% 117.83/117.93 inference(scs_inference,[],[2408,2903,974,495,145,83,69,70,67,76])).
% 117.83/117.93 cnf(2978,plain,
% 117.83/117.93 (E(f8(f16(f6(x29781,f5(x29782,a1)),x29782)),f8(f4(a1,x29783)))),
% 117.83/117.93 inference(scs_inference,[],[2408,2903,2855,974,497,495,145,83,69,70,67,76,68,72,63,16,12,15,13])).
% 117.83/117.93 cnf(2981,plain,
% 117.83/117.93 (E(f20(x29811,f16(f6(x29812,f5(x29813,a1)),x29813),x29814),f20(x29811,f4(a1,x29815),x29814))),
% 117.83/117.93 inference(scs_inference,[],[2408,2903,2855,974,497,495,145,83,69,70,67,76,68,72,63,16,12,15,13,20,8,11])).
% 117.83/117.93 cnf(2982,plain,
% 117.83/117.93 (E(f13(f16(f6(x29821,f5(x29822,a1)),x29822),x29823),f13(f4(a1,x29824),x29823))),
% 117.83/117.93 inference(scs_inference,[],[2408,2903,2855,974,497,495,145,83,69,70,67,76,68,72,63,16,12,15,13,20,8,11,21])).
% 117.83/117.93 cnf(3000,plain,
% 117.83/117.93 (P8(f6(x30001,f5(f19(x30002,a11),f19(x30002,a11))),f19(x30002,a3),f19(x30002,a3))),
% 117.83/117.93 inference(scs_inference,[],[2408,2903,2855,2337,974,497,495,145,1775,83,69,70,67,76,68,72,63,16,12,15,13,20,8,11,21,19,25,22,23,5,26,10,4,17,24,6,14,7,27,18,9,2,75])).
% 117.83/117.93 cnf(3013,plain,
% 117.83/117.93 (P6(f8(f20(x30131,a1,x30132)),f18(f8(f20(x30131,a1,x30133)),x30134))),
% 117.83/117.93 inference(scs_inference,[],[2944,2408,2903,2946,2955,2855,2940,2197,2337,388,974,980,982,523,497,495,145,1775,1106,103,83,69,70,67,76,68,72,63,16,12,15,13,20,8,11,21,19,25,22,23,5,26,10,4,17,24,6,14,7,27,18,9,2,75,39,37,38,66,41,31])).
% 117.83/117.93 cnf(3018,plain,
% 117.83/117.93 (P1(f15(f20(a3,x30181,x30182),a11),f15(f20(a3,x30181,x30182),a3))),
% 117.83/117.93 inference(scs_inference,[],[2944,2408,2903,2785,2946,2955,2855,2940,2197,2337,388,1539,974,980,2318,1897,982,523,497,495,145,1775,1106,103,83,69,70,67,76,68,72,63,16,12,15,13,20,8,11,21,19,25,22,23,5,26,10,4,17,24,6,14,7,27,18,9,2,75,39,37,38,66,41,31,32,29])).
% 117.83/117.93 cnf(3022,plain,
% 117.83/117.93 (~E(f17(f6(f13(f20(a9,a10,a11),a12),f5(a11,x30221)),a3),f20(x30222,x30223,a3))),
% 117.83/117.93 inference(scs_inference,[],[2547,2944,2408,2903,2161,2785,2946,2955,2855,2940,2197,2337,388,1539,1909,974,980,2318,1897,982,523,497,495,60,145,1775,1106,103,83,69,70,67,76,68,72,63,16,12,15,13,20,8,11,21,19,25,22,23,5,26,10,4,17,24,6,14,7,27,18,9,2,75,39,37,38,66,41,31,32,29,28,36])).
% 117.83/117.93 cnf(3025,plain,
% 117.83/117.93 (P6(f4(a1,x30251),f18(f8(f4(a1,x30252)),f7(f4(a1,x30252))))),
% 117.83/117.93 inference(scs_inference,[],[3000,130,83,69])).
% 117.83/117.93 cnf(3027,plain,
% 117.83/117.93 (P6(a11,f13(f18(f8(a3),f7(a3)),x30271))),
% 117.83/117.93 inference(scs_inference,[],[2961,3000,130,83,69,67])).
% 117.83/117.93 cnf(3031,plain,
% 117.83/117.93 (P6(a11,f18(f18(f8(a3),f7(a3)),x30311))),
% 117.83/117.93 inference(scs_inference,[],[2961,3000,1932,130,83,69,67,70,68])).
% 117.83/117.93 cnf(3037,plain,
% 117.83/117.93 (P6(a11,f8(f18(f8(a3),f7(a3))))),
% 117.83/117.93 inference(scs_inference,[],[2961,3000,2913,169,1932,130,83,69,67,70,68,76,72,63])).
% 117.83/117.93 cnf(3052,plain,
% 117.83/117.93 (E(f13(x30521,f7(f20(x30522,a1,x30523))),f13(x30521,f7(f20(x30524,a1,x30525))))),
% 117.83/117.93 inference(scs_inference,[],[2961,3000,2913,169,468,1932,130,83,69,67,70,68,76,72,63,12,20,16,15,19,8,13,25,5,11,10,26,21,22])).
% 117.83/117.93 cnf(3058,plain,
% 117.83/117.93 (E(f5(f7(f20(x30581,a1,x30582)),x30583),f5(f7(f20(x30584,a1,x30585)),x30583))),
% 117.83/117.93 inference(scs_inference,[],[2961,3000,2913,169,468,1932,130,83,69,67,70,68,76,72,63,12,20,16,15,19,8,13,25,5,11,10,26,21,22,14,23,17,4,24,6])).
% 117.83/117.93 cnf(3064,plain,
% 117.83/117.93 (P8(f6(x30641,f5(f19(a11,x30642),f19(a11,x30642))),f19(a3,x30642),f19(a3,x30642))),
% 117.83/117.93 inference(scs_inference,[],[2961,3000,3022,2913,169,468,1932,130,1660,83,69,67,70,68,76,72,63,12,20,16,15,19,8,13,25,5,11,10,26,21,22,14,23,17,4,24,6,7,9,27,18,2,75])).
% 117.83/117.93 cnf(3069,plain,
% 117.83/117.93 (~P9(f13(f4(a1,x30691),x30692),f13(f16(f6(x30693,f5(x30694,a1)),x30694),x30692))),
% 117.83/117.93 inference(scs_inference,[],[2961,3000,3022,2913,2982,2948,169,98,468,1932,2164,130,1660,83,69,67,70,68,76,72,63,12,20,16,15,19,8,13,25,5,11,10,26,21,22,14,23,17,4,24,6,7,9,27,18,2,75,37,38])).
% 117.83/117.93 cnf(3117,plain,
% 117.83/117.93 (P8(f6(x31171,f5(f6(a11,a3),f6(a11,a3))),f6(a3,a11),f6(a3,a11))),
% 117.83/117.93 inference(scs_inference,[],[3064,3027,2963,2763,214,1918,1731,109,1357,83,69,67,70,68,72,76,63,12,20,25,5,8,16,15,26,21,11,13,23,14,19,22,10,24,4,7,17,6,27,9,18,2,75])).
% 117.83/117.93 cnf(3124,plain,
% 117.83/117.93 (P6(f4(a1,x31241),f18(f8(a1),f7(a1)))),
% 117.83/117.93 inference(scs_inference,[],[3117,111,83,69])).
% 117.83/117.93 cnf(3152,plain,
% 117.83/117.93 (E(f13(x31521,f18(f5(a3,x31522),f5(x31523,a3))),f13(x31521,f18(f5(a11,x31522),f5(x31523,a11))))),
% 117.83/117.93 inference(scs_inference,[],[3117,3031,2280,1949,1712,111,83,69,67,70,76,72,68,63,12,8,25,20,15,16,5,11,26,19,21,14,13,10,22])).
% 117.83/117.93 cnf(3163,plain,
% 117.83/117.93 (P8(f6(x31631,f5(f17(a11,x31632),f17(a11,x31632))),f17(a3,x31632),f17(a3,x31632))),
% 117.83/117.93 inference(scs_inference,[],[3117,3031,2526,2280,1949,1712,111,995,83,69,67,70,76,72,68,63,12,8,25,20,15,16,5,11,26,19,21,14,13,10,22,23,4,6,7,24,27,17,18,9,2,75])).
% 117.83/117.93 cnf(3165,plain,
% 117.83/117.93 (~P9(f17(f6(f15(x31651,f20(x31652,a1,a3)),f5(x31653,x31654)),x31653),f15(x31651,f18(f20(x31652,a1,x31655),x31656)))),
% 117.83/117.93 inference(scs_inference,[],[3117,3031,2526,2295,2280,544,1949,1712,111,995,83,69,67,70,76,72,68,63,12,8,25,20,15,16,5,11,26,19,21,14,13,10,22,23,4,6,7,24,27,17,18,9,2,75,38])).
% 117.83/117.93 cnf(3167,plain,
% 117.83/117.93 (~P9(f13(f4(a1,x31671),f18(f20(x31672,a1,x31673),x31674)),f13(f16(f6(x31675,f5(x31676,a1)),x31676),f20(x31672,a1,a3)))),
% 117.83/117.93 inference(scs_inference,[],[3117,3031,2526,3069,2295,2311,2280,544,1949,1712,111,995,83,69,67,70,76,72,68,63,12,8,25,20,15,16,5,11,26,19,21,14,13,10,22,23,4,6,7,24,27,17,18,9,2,75,38,37])).
% 117.83/117.93 cnf(3175,plain,
% 117.83/117.93 (P6(a3,f18(f8(a11),f7(a11)))),
% 117.83/117.93 inference(scs_inference,[],[136,69])).
% 117.83/117.93 cnf(3179,plain,
% 117.83/117.93 (P6(f4(a1,x31791),f13(f18(f8(a1),f7(a1)),x31792))),
% 117.83/117.93 inference(scs_inference,[],[3124,3163,136,69,83,67])).
% 117.83/117.93 cnf(3181,plain,
% 117.83/117.93 (P6(f4(a1,x31811),f18(f18(f8(a1),f7(a1)),x31812))),
% 117.83/117.93 inference(scs_inference,[],[3124,3163,136,69,83,67,68])).
% 117.83/117.93 cnf(3185,plain,
% 117.83/117.93 (P4(f6(f6(x31851,f5(f20(x31852,a1,a3),x31853)),f5(x31854,x31855)),f8(f20(x31852,a1,x31856)))),
% 117.83/117.93 inference(scs_inference,[],[3124,3163,1878,1955,136,69,83,67,68,76,72])).
% 117.83/117.93 cnf(3187,plain,
% 117.83/117.93 (P4(f6(x31871,f5(f6(a3,a3),x31872)),f17(f6(f6(a11,a11),f5(x31873,x31874)),x31873))),
% 117.83/117.93 inference(scs_inference,[],[3124,3163,1878,1955,1380,136,69,83,67,68,76,72,70])).
% 117.83/117.93 cnf(3189,plain,
% 117.83/117.93 (P6(f4(a1,x31891),f8(f18(f8(a1),f7(a1))))),
% 117.83/117.93 inference(scs_inference,[],[3124,3163,1878,1955,1380,136,69,83,67,68,76,72,70,63])).
% 117.83/117.93 cnf(3216,plain,
% 117.83/117.93 (P8(f6(x32161,f5(f6(x32162,a11),f6(x32162,a11))),f6(x32162,a3),f6(x32162,a3))),
% 117.83/117.93 inference(scs_inference,[],[3124,3163,2765,1878,1955,1380,136,857,69,83,67,68,76,72,70,63,12,15,25,5,8,26,20,11,21,13,16,19,14,22,6,10,24,4,23,27,7,17,18,9,2,75])).
% 117.83/117.93 cnf(3225,plain,
% 117.83/117.93 (P6(f17(f6(x32251,f5(x32252,x32253)),x32252),f18(f8(x32251),f7(x32251)))),
% 117.83/117.93 inference(scs_inference,[],[521,69])).
% 117.83/117.93 cnf(3229,plain,
% 117.83/117.93 (P6(a3,f13(f18(f8(a11),f7(a11)),x32291))),
% 117.83/117.93 inference(scs_inference,[],[3175,3216,521,69,83,67])).
% 117.83/117.93 cnf(3235,plain,
% 117.83/117.93 (P4(f6(f6(f6(x32351,f5(f20(x32352,a1,a3),x32353)),f5(x32354,x32355)),f5(x32356,x32357)),f8(f20(x32352,a1,x32358)))),
% 117.83/117.93 inference(scs_inference,[],[3175,3216,3179,3185,521,69,83,67,68,76,72])).
% 117.83/117.93 cnf(3237,plain,
% 117.83/117.93 (P4(f6(x32371,f5(f6(a11,a11),x32372)),f17(f6(f6(a3,a3),f5(x32373,x32374)),x32373))),
% 117.83/117.93 inference(scs_inference,[],[3175,3216,3179,3185,1337,521,69,83,67,68,76,72,70])).
% 117.83/117.93 cnf(3239,plain,
% 117.83/117.93 (P6(a3,f8(f18(f8(a11),f7(a11))))),
% 117.83/117.93 inference(scs_inference,[],[3175,3216,3179,3185,1337,521,69,83,67,68,76,72,70,63])).
% 117.83/117.93 cnf(3266,plain,
% 117.83/117.93 (P8(f6(x32661,f5(f19(x32662,a3),f19(x32662,a3))),f19(x32662,a11),f19(x32662,a11))),
% 117.83/117.93 inference(scs_inference,[],[3175,3216,3179,3185,2467,1341,1337,1774,521,69,83,67,68,76,72,70,63,12,15,25,5,21,26,13,20,19,6,8,11,14,16,22,4,24,10,7,23,17,27,18,9,2,75])).
% 117.83/117.93 cnf(3268,plain,
% 117.83/117.93 (~P9(f20(f15(x32681,x32682),f6(a1,f5(x32682,a2)),a3),f13(f18(f20(x32681,a1,x32683),x32684),x32682))),
% 117.83/117.93 inference(scs_inference,[],[3175,3216,3179,3185,2467,814,2317,1341,1337,1774,521,69,83,67,68,76,72,70,63,12,15,25,5,21,26,13,20,19,6,8,11,14,16,22,4,24,10,7,23,17,27,18,9,2,75,38])).
% 117.83/117.93 cnf(3271,plain,
% 117.83/117.93 (~P9(f15(f20(a3,x32711,x32712),f20(x32713,a1,a3)),f15(f20(a11,x32711,x32712),f18(f20(x32713,a1,x32714),x32715)))),
% 117.83/117.93 inference(scs_inference,[],[3175,3216,3179,3185,3165,2467,814,2317,1341,1337,1395,1774,521,69,83,67,68,76,72,70,63,12,15,25,5,21,26,13,20,19,6,8,11,14,16,22,4,24,10,7,23,17,27,18,9,2,75,38,37])).
% 117.83/117.93 cnf(3274,plain,
% 117.83/117.93 (P6(f8(f20(x32741,a1,x32742)),f8(f8(f20(x32741,a1,x32743))))),
% 117.83/117.93 inference(scs_inference,[],[3175,3216,3179,3185,2193,3165,2467,814,2317,1341,1337,523,1395,1774,521,69,83,67,68,76,72,70,63,12,15,25,5,21,26,13,20,19,6,8,11,14,16,22,4,24,10,7,23,17,27,18,9,2,75,38,37,31])).
% 117.83/117.93 cnf(3283,plain,
% 117.83/117.93 (~E(f17(f6(f13(f20(a9,a10,a11),a12),f5(a3,x32831)),a11),f17(f6(f20(a9,a10,a11),f5(x32832,x32833)),x32832))),
% 117.83/117.93 inference(scs_inference,[],[3175,3018,3216,3179,3185,2193,3165,2467,2251,814,2317,586,1066,1909,530,147,1341,1337,523,1395,1774,521,1058,69,83,67,68,76,72,70,63,12,15,25,5,21,26,13,20,19,6,8,11,14,16,22,4,24,10,7,23,17,27,18,9,2,75,38,37,31,32,29,28,36])).
% 117.83/117.93 cnf(3291,plain,
% 117.83/117.93 (P6(x32911,f18(f8(x32911),f7(x32911)))),
% 117.83/117.93 inference(scs_inference,[],[47,69])).
% 117.83/117.93 cnf(3316,plain,
% 117.83/117.93 (E(f20(x33161,f6(a3,x33162),x33163),f20(x33161,f17(f6(f6(a11,x33162),f5(x33164,x33165)),x33164),x33163))),
% 117.83/117.93 inference(scs_inference,[],[3266,3181,3235,144,828,47,69,83,67,68,70,76,72,63,12,5,21,15,13,20,25,26,19,11])).
% 117.83/117.93 cnf(3320,plain,
% 117.83/117.93 (E(f17(f6(a3,x33201),x33202),f17(f17(f6(f6(a11,x33201),f5(x33203,x33204)),x33203),x33202))),
% 117.83/117.93 inference(scs_inference,[],[3266,3181,3235,144,828,47,69,83,67,68,70,76,72,63,12,5,21,15,13,20,25,26,19,11,6,8,16,14])).
% 117.83/117.93 cnf(3332,plain,
% 117.83/117.93 (P8(f6(x33321,f5(f19(a3,x33322),f19(a3,x33322))),f19(a11,x33322),f19(a11,x33322))),
% 117.83/117.93 inference(scs_inference,[],[3266,3181,3235,3283,144,828,1659,47,69,83,67,68,70,76,72,63,12,5,21,15,13,20,25,26,19,11,6,8,16,14,24,4,22,23,7,10,17,18,27,9,2,75])).
% 117.83/117.93 cnf(3334,plain,
% 117.83/117.93 (~P9(f15(f20(a3,a1,a3),f20(x33341,a1,a3)),f15(f18(f20(a11,a1,x33342),x33343),f18(f20(x33341,a1,x33344),x33345)))),
% 117.83/117.93 inference(scs_inference,[],[3266,3181,3271,3235,3283,2303,144,828,1659,47,69,83,67,68,70,76,72,63,12,5,21,15,13,20,25,26,19,11,6,8,16,14,24,4,22,23,7,10,17,18,27,9,2,75,38])).
% 117.83/117.93 cnf(3335,plain,
% 117.83/117.93 (~P9(f15(f20(a3,x33351,x33352),f20(x33353,a1,a3)),f15(f20(a11,x33351,x33352),f18(f20(x33353,a1,x33354),x33355)))),
% 117.83/117.93 inference(rename_variables,[],[3271])).
% 117.83/117.93 cnf(3336,plain,
% 117.83/117.93 (E(f15(f18(f20(x33361,a1,x33362),x33363),x33364),f15(f20(x33361,a1,a3),x33364))),
% 117.83/117.93 inference(rename_variables,[],[2303])).
% 117.83/117.93 cnf(3337,plain,
% 117.83/117.93 (~P9(f15(f18(f20(a3,a1,x33371),x33372),f20(x33373,a1,a3)),f15(f20(a11,a1,a3),f18(f20(x33373,a1,x33374),x33375)))),
% 117.83/117.93 inference(scs_inference,[],[3266,3181,3271,3335,3235,3283,2303,3336,144,828,1659,47,69,83,67,68,70,76,72,63,12,5,21,15,13,20,25,26,19,11,6,8,16,14,24,4,22,23,7,10,17,18,27,9,2,75,38,37])).
% 117.83/117.93 cnf(3341,plain,
% 117.83/117.93 (P6(x33411,f13(f18(f8(x33411),f7(x33411)),x33412))),
% 117.83/117.93 inference(scs_inference,[],[3291,67])).
% 117.83/117.93 cnf(3345,plain,
% 117.83/117.93 (P6(x33451,f18(f18(f8(x33451),f7(x33451)),x33452))),
% 117.83/117.93 inference(scs_inference,[],[3291,3332,67,83,68])).
% 117.83/117.93 cnf(3353,plain,
% 117.83/117.93 (P6(x33531,f8(f18(f8(x33531),f7(x33531))))),
% 117.83/117.93 inference(scs_inference,[],[3291,3332,3187,116,241,67,83,68,76,70,72,63])).
% 117.83/117.93 cnf(3380,plain,
% 117.83/117.93 (P8(f6(x33801,f5(f17(a3,x33802),f17(a3,x33802))),f17(a11,x33802),f17(a11,x33802))),
% 117.83/117.93 inference(scs_inference,[],[3291,3332,3187,2255,116,241,954,994,67,83,68,76,70,72,63,12,21,13,20,15,5,26,6,25,19,11,8,24,14,16,4,7,22,23,10,18,17,27,9,2,75])).
% 117.83/117.93 cnf(3384,plain,
% 117.83/117.93 (~P9(x33841,f7(f18(f20(x33842,a1,x33843),x33844)))),
% 117.83/117.93 inference(scs_inference,[],[3291,3332,3334,3187,2255,2316,304,2303,116,241,954,994,67,83,68,76,70,72,63,12,21,13,20,15,5,26,6,25,19,11,8,24,14,16,4,7,22,23,10,18,17,27,9,2,75,37,38])).
% 117.83/117.93 cnf(3389,plain,
% 117.83/117.93 (E(f5(f7(f20(x33891,a1,x33892)),f18(f20(x33893,a1,x33894),x33895)),f5(f7(f20(x33896,a1,x33897)),f20(x33893,a1,a3)))),
% 117.83/117.93 inference(scs_inference,[],[3291,3332,2655,3334,3187,3058,2255,2296,2316,304,2303,116,241,954,994,67,83,68,76,70,72,63,12,21,13,20,15,5,26,6,25,19,11,8,24,14,16,4,7,22,23,10,18,17,27,9,2,75,37,38,65,3])).
% 117.83/117.93 cnf(3400,plain,
% 117.83/117.93 (P4(f6(x34001,f5(f5(a3,a11),x34002)),f5(a11,a3))),
% 117.83/117.93 inference(scs_inference,[],[3380,3353,938,1537,67,83,68,76,70])).
% 117.83/117.93 cnf(3431,plain,
% 117.83/117.93 (P8(f6(x34311,f5(f6(x34312,a3),f6(x34312,a3))),f6(x34312,a11),f6(x34312,a11))),
% 117.83/117.93 inference(scs_inference,[],[3380,3353,3237,2660,948,938,1537,856,67,83,68,76,70,72,63,21,20,12,15,5,13,26,8,11,25,6,19,7,16,22,24,14,4,10,23,18,17,27,9,2,75])).
% 117.83/117.93 cnf(3437,plain,
% 117.83/117.93 (P1(f17(f6(f20(x34371,a1,a3),f5(x34372,x34373)),x34372),f17(f6(f8(f20(x34371,a1,x34374)),f5(x34375,x34376)),x34375))),
% 117.83/117.93 inference(scs_inference,[],[3380,3353,3337,3237,2660,345,1884,601,2295,948,938,1537,1998,856,67,83,68,76,70,72,63,21,20,12,15,5,13,26,8,11,25,6,19,7,16,22,24,14,4,10,23,18,17,27,9,2,75,37,38,66])).
% 117.83/117.93 cnf(3441,plain,
% 117.83/117.93 (P5(f20(x34411,f17(f6(f6(a11,f5(a1,x34412)),f5(x34413,x34414)),x34413),x34415),f4(a1,x34416))),
% 117.83/117.93 inference(scs_inference,[],[2967,3380,3353,3337,3389,3237,2660,3316,345,1884,601,2295,948,938,1537,1998,856,67,83,68,76,70,72,63,21,20,12,15,5,13,26,8,11,25,6,19,7,16,22,24,14,4,10,23,18,17,27,9,2,75,37,38,66,41,39])).
% 117.83/117.93 cnf(3452,plain,
% 117.83/117.93 (P4(f6(x34521,f5(a11,x34522)),f16(f6(x34523,f5(f4(x34524,a11),a11)),f4(x34524,a3)))),
% 117.83/117.93 inference(scs_inference,[],[3400,3431,3341,2036,67,83,68,76,70])).
% 117.83/117.93 cnf(3454,plain,
% 117.83/117.93 (P4(f6(f6(x34541,f5(f5(a3,a11),x34542)),f5(x34543,x34544)),f5(a11,a3))),
% 117.83/117.93 inference(scs_inference,[],[3400,3431,3341,2036,67,83,68,76,70,72])).
% 117.83/117.93 cnf(3458,plain,
% 117.83/117.93 (E(f13(f4(a1,x34581),x34582),f13(f16(f6(x34583,f5(x34584,a1)),x34584),x34582))),
% 117.83/117.93 inference(scs_inference,[],[3400,3431,3341,495,2036,67,83,68,76,70,72,63,21])).
% 117.83/117.93 cnf(3463,plain,
% 117.83/117.93 (E(f8(f4(a1,x34631)),f8(f16(f6(x34632,f5(x34633,a1)),x34633)))),
% 117.83/117.93 inference(scs_inference,[],[3400,3431,3341,495,2036,67,83,68,76,70,72,63,21,20,12,26,5,13])).
% 117.83/117.93 cnf(3485,plain,
% 117.83/117.93 (~P9(f15(f20(a3,x34851,x34852),a11),f15(f20(a11,x34851,x34852),a3))),
% 117.83/117.93 inference(scs_inference,[],[3400,3431,3341,2958,534,1926,495,2036,313,67,83,68,76,70,72,63,21,20,12,26,5,13,15,8,11,6,16,25,22,7,19,24,14,10,4,18,23,27,17,9,2,75,38])).
% 117.83/117.93 cnf(3498,plain,
% 117.83/117.93 (~E(f17(f6(f13(f20(a9,a10,a11),a12),f5(a11,x34981)),a3),f17(f6(f20(x34982,a1,a3),f5(x34983,x34984)),x34983))),
% 117.83/117.93 inference(scs_inference,[],[3400,3431,3341,3225,2775,2958,2931,3320,534,1926,2161,529,222,495,150,2036,1134,313,67,83,68,76,70,72,63,21,20,12,26,5,13,15,8,11,6,16,25,22,7,19,24,14,10,4,18,23,27,17,9,2,75,38,31,32,29,28,36])).
% 117.83/117.93 cnf(3505,plain,
% 117.83/117.93 (P4(f6(x35051,f5(a11,x35052)),f16(f6(x35053,f5(f4(x35054,a3),a11)),f4(x35054,a11)))),
% 117.83/117.93 inference(scs_inference,[],[3345,2612,2065,83,67,68,70])).
% 117.83/117.93 cnf(3509,plain,
% 117.83/117.93 (P4(f6(f6(f6(x35091,f5(f5(a3,a11),x35092)),f5(x35093,x35094)),f5(x35095,x35096)),f5(a11,a3))),
% 117.83/117.93 inference(scs_inference,[],[3345,2612,3454,2065,83,67,68,70,76,72])).
% 117.83/117.93 cnf(3513,plain,
% 117.83/117.93 (E(f13(f17(f6(f4(a1,x35131),f5(x35132,x35133)),x35132),x35134),f13(f4(a1,x35135),x35134))),
% 117.83/117.93 inference(scs_inference,[],[3345,2612,3454,160,2065,83,67,68,70,76,72,63,21])).
% 117.83/117.93 cnf(3540,plain,
% 117.83/117.93 (~P9(f15(f18(f20(a3,a1,x35401),x35402),a11),f15(f20(a11,a1,a3),a3))),
% 117.83/117.93 inference(scs_inference,[],[3485,3345,2612,3454,3498,2303,160,2065,234,83,67,68,70,76,72,63,21,20,12,13,15,5,26,8,25,22,11,6,7,16,10,24,4,14,19,27,18,23,17,9,2,75,37])).
% 117.83/117.93 cnf(3543,plain,
% 117.83/117.93 (~P9(f13(f4(a1,x35431),f18(f20(x35432,a1,x35433),x35434)),f13(f4(a1,x35435),f20(x35432,a1,a3)))),
% 117.83/117.93 inference(scs_inference,[],[3485,3345,2612,3454,3167,3498,3458,2303,160,2065,234,83,67,68,70,76,72,63,21,20,12,13,15,5,26,8,25,22,11,6,7,16,10,24,4,14,19,27,18,23,17,9,2,75,37,38])).
% 117.83/117.93 cnf(3555,plain,
% 117.83/117.93 (P4(f6(f6(f6(f6(x35551,f5(f5(a3,a11),x35552)),f5(x35553,x35554)),f5(x35555,x35556)),f5(x35557,x35558)),f5(a11,a3))),
% 117.83/117.93 inference(scs_inference,[],[3189,2665,3509,68,83,67,76,72])).
% 117.83/117.93 cnf(3557,plain,
% 117.83/117.93 (P4(f6(x35571,f5(a3,x35572)),f16(f6(x35573,f5(f4(x35574,a11),a11)),f4(x35574,a3)))),
% 117.83/117.93 inference(scs_inference,[],[3189,2665,3509,1978,68,83,67,76,72,70])).
% 117.83/117.93 cnf(3586,plain,
% 117.83/117.93 (P8(f6(x35861,f5(f17(x35862,a3),f17(x35862,a3))),f17(x35862,a11),f17(x35862,a11))),
% 117.83/117.93 inference(scs_inference,[],[3189,2665,3509,1112,2009,1978,1058,68,83,67,76,72,70,63,20,21,12,15,13,5,26,11,8,22,25,10,16,14,4,6,24,7,19,17,27,18,23,9,2,75])).
% 117.83/117.93 cnf(3589,plain,
% 117.83/117.93 (~P9(f13(f4(a1,x35891),f18(f20(x35892,a1,x35893),x35894)),f13(f4(a1,x35895),f20(x35892,a1,a3)))),
% 117.83/117.93 inference(rename_variables,[],[3543])).
% 117.83/117.93 cnf(3590,plain,
% 117.83/117.93 (E(f13(f17(f6(f4(a1,x35901),f5(x35902,x35903)),x35902),x35904),f13(f4(a1,x35905),x35904))),
% 117.83/117.93 inference(rename_variables,[],[3513])).
% 117.83/117.93 cnf(3593,plain,
% 117.83/117.93 (P1(f7(f18(f20(x35931,a1,x35932),x35933)),f17(f6(f7(f20(x35934,a1,x35935)),f5(a11,x35936)),a3))),
% 117.83/117.93 inference(scs_inference,[],[3384,3189,2665,3543,3589,3509,3513,3590,2024,1112,2009,1978,1058,68,83,67,76,72,70,63,20,21,12,15,13,5,26,11,8,22,25,10,16,14,4,6,24,7,19,17,27,18,23,9,2,75,37,38,65])).
% 117.83/117.93 cnf(3597,plain,
% 117.83/117.93 (E(f8(f4(a1,x35971)),f8(f4(a1,x35972)))),
% 117.83/117.93 inference(scs_inference,[],[3384,3189,2665,3543,3589,3509,3513,3590,2978,3463,2024,1112,2009,1978,1058,68,83,67,76,72,70,63,20,21,12,15,13,5,26,11,8,22,25,10,16,14,4,6,24,7,19,17,27,18,23,9,2,75,37,38,65,3])).
% 117.83/117.93 cnf(3631,plain,
% 117.83/117.93 (E(f18(f8(f4(a1,x36311)),x36312),f18(f8(f4(a1,x36313)),x36312))),
% 117.83/117.93 inference(scs_inference,[],[3597,3586,3229,3452,83,67,68,70,76,72,63,21,20,12,5,13,15,26,11,8,22,6,25,7,10,16,14,4,24,19])).
% 117.83/117.93 cnf(3638,plain,
% 117.83/117.93 (P8(f6(x36381,f5(f17(x36382,a11),f17(x36382,a11))),f17(x36382,a3),f17(x36382,a3))),
% 117.83/117.93 inference(scs_inference,[],[3597,3586,3229,3452,1056,1059,83,67,68,70,76,72,63,21,20,12,5,13,15,26,11,8,22,6,25,7,10,16,14,4,24,19,27,17,18,23,9,2,75])).
% 117.83/117.93 cnf(3640,plain,
% 117.83/117.93 (~P9(f13(f20(x36401,a1,a3),x36402),f13(f18(f20(x36401,a1,x36403),x36404),x36402))),
% 117.83/117.93 inference(scs_inference,[],[3597,3586,3229,3452,3268,1056,306,1059,83,67,68,70,76,72,63,21,20,12,5,13,15,26,11,8,22,6,25,7,10,16,14,4,24,19,27,17,18,23,9,2,75,37])).
% 117.83/117.93 cnf(3648,plain,
% 117.83/117.93 (~P5(f20(x36481,f16(f6(x36482,f5(x36483,a1)),x36483),x36484),x36485)),
% 117.83/117.93 inference(scs_inference,[],[3597,3586,3229,3540,3452,3268,3593,2981,2899,1056,2024,1923,306,1059,83,67,68,70,76,72,63,21,20,12,5,13,15,26,11,8,22,6,25,7,10,16,14,4,24,19,27,17,18,23,9,2,75,37,38,66,41,39])).
% 117.83/117.93 cnf(3689,plain,
% 117.83/117.93 (P8(f6(x36891,f5(f15(x36892,a11),f15(x36892,a11))),f15(x36892,a3),f15(x36892,a3))),
% 117.83/117.93 inference(scs_inference,[],[3638,3239,3505,1771,2027,1784,1559,83,67,68,70,76,72,63,21,20,5,12,15,26,13,8,11,22,6,4,25,7,19,24,10,16,14,17,27,18,23,9,2,75])).
% 117.83/117.93 cnf(3692,plain,
% 117.83/117.93 (~P9(f13(f20(x36921,a1,a3),x36922),f13(f18(f20(x36921,a1,x36923),x36924),x36922))),
% 117.83/117.93 inference(rename_variables,[],[3640])).
% 117.83/117.93 cnf(3698,plain,
% 117.83/117.93 (P6(f4(a1,x36981),f18(f8(f4(a1,x36982)),f7(f4(a1,x36983))))),
% 117.83/117.93 inference(scs_inference,[],[3638,3239,3037,3640,3692,3025,3505,3052,3152,3631,1771,2027,1784,2036,1559,83,67,68,70,76,72,63,21,20,5,12,15,26,13,8,11,22,6,4,25,7,19,24,10,16,14,17,27,18,23,9,2,75,37,38,31,32])).
% 117.83/117.93 cnf(3741,plain,
% 117.83/117.93 (P8(f6(x37411,f5(f15(x37412,a3),f15(x37412,a3))),f15(x37412,a11),f15(x37412,a11))),
% 117.83/117.93 inference(scs_inference,[],[3689,3013,3557,1083,1790,1558,67,83,70,68,76,72,63,20,21,15,5,12,26,8,13,11,22,19,7,6,24,25,4,14,10,17,16,18,27,23,9,2,75])).
% 117.83/117.93 cnf(3744,plain,
% 117.83/117.93 (~P9(f17(f6(f20(x37441,a1,a3),f5(x37442,x37443)),x37442),f17(f6(f8(f20(x37441,a1,x37444)),f5(x37445,x37446)),x37445))),
% 117.83/117.93 inference(scs_inference,[],[3689,2656,3013,3557,1890,1083,270,1790,300,1558,67,83,70,68,76,72,63,20,21,15,5,12,26,8,13,11,22,19,7,6,24,25,4,14,10,17,16,18,27,23,9,2,75,37,38])).
% 117.83/117.93 cnf(3788,plain,
% 117.83/117.93 (P8(f6(x37881,f5(f6(a3,x37882),f6(a3,x37882))),f6(a11,x37882),f6(a11,x37882))),
% 117.83/117.93 inference(scs_inference,[],[3741,3274,3555,505,1666,126,816,83,68,67,70,76,72,63,20,21,12,8,15,26,5,13,11,22,6,19,24,17,14,25,10,7,18,16,4,23,27,9,2,75])).
% 117.83/117.93 cnf(3808,plain,
% 117.83/117.93 (P5(f20(x38081,f6(x38082,f5(x38083,x38084)),x38085),x38083)),
% 117.83/117.93 inference(scs_inference,[],[3788,3698,1672,94,68,83,67,70,76])).
% 117.83/117.93 cnf(4207,plain,
% 117.83/117.93 (E(x42071,f16(f6(x42072,f5(x42073,x42071)),x42073))),
% 117.83/117.93 inference(rename_variables,[],[312])).
% 117.83/117.93 cnf(4211,plain,
% 117.83/117.93 (E(x42111,f16(f6(x42112,f5(x42113,x42111)),x42113))),
% 117.83/117.93 inference(rename_variables,[],[312])).
% 117.83/117.93 cnf(4216,plain,
% 117.83/117.93 (E(x42161,f16(f6(x42162,f5(x42163,x42161)),x42163))),
% 117.83/117.93 inference(rename_variables,[],[312])).
% 117.83/117.93 cnf(4218,plain,
% 117.83/117.93 (E(x42181,f16(f6(x42182,f5(x42183,x42181)),x42183))),
% 117.83/117.93 inference(rename_variables,[],[312])).
% 117.83/117.93 cnf(4220,plain,
% 117.83/117.93 (E(x42201,f16(f6(x42202,f5(x42203,x42201)),x42203))),
% 117.83/117.93 inference(rename_variables,[],[312])).
% 117.83/117.93 cnf(4222,plain,
% 117.83/117.93 (E(x42221,f16(f6(x42222,f5(x42223,x42221)),x42223))),
% 117.83/117.93 inference(rename_variables,[],[312])).
% 117.83/117.93 cnf(4224,plain,
% 117.83/117.93 (E(x42241,f16(f6(x42242,f5(x42243,x42241)),x42243))),
% 117.83/117.93 inference(rename_variables,[],[312])).
% 117.83/117.93 cnf(4233,plain,
% 117.83/117.93 (~P8(a1,x42331,x42332)),
% 117.83/117.93 inference(rename_variables,[],[58])).
% 117.83/117.93 cnf(4235,plain,
% 117.83/117.93 (E(x42351,f16(f6(x42352,f5(x42353,x42351)),x42353))),
% 117.83/117.93 inference(rename_variables,[],[312])).
% 117.83/117.93 cnf(4237,plain,
% 117.83/117.93 (E(x42371,f16(f6(x42372,f5(x42373,x42371)),x42373))),
% 117.83/117.93 inference(rename_variables,[],[312])).
% 117.83/117.93 cnf(4244,plain,
% 117.83/117.93 ($false),
% 117.83/117.93 inference(scs_inference,[],[54,95,2231,312,4207,4211,4216,4218,4220,4222,4224,4235,4237,200,57,384,107,58,4233,126,2466,52,130,224,2537,2899,2967,2384,3283,3808,2321,2461,3441,3437,3744,2609,3648,2,14,64,76,70,82,30,33,36,3,28,29,32,31,35,65,39,34,41,43,42,40,21,86,12]),
% 117.83/117.93 ['proof']).
% 117.83/117.93 % SZS output end Proof
% 117.83/117.93 % Total time :117.180000s
%------------------------------------------------------------------------------