%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : SWV374+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 : n027.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Mon Jun 24 16:47:01 EDT 2024
% Result : Theorem 118.58s 118.73s
% Output : CNFRefutation 118.67s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : SWV374+1 : TPTP v8.2.0. Released v3.3.0.
% 0.03/0.12 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% 0.12/0.33 % Computer : n027.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 300
% 0.12/0.33 % DateTime : Thu Jun 20 19:06:24 EDT 2024
% 0.12/0.33 % CPUTime :
% 0.55/0.59 start to proof:theBenchmark
% 118.58/118.70 %-------------------------------------------
% 118.58/118.70 % File :CSE---1.7
% 118.58/118.70 % Problem :theBenchmark
% 118.58/118.70 % Transform :cnf
% 118.58/118.70 % Format :tptp:raw
% 118.58/118.70 % Command :java -jar mcs_scs.jar %d %s
% 118.58/118.70
% 118.58/118.70 % Result :Theorem 117.930000s
% 118.58/118.70 % Output :CNFRefutation 117.930000s
% 118.58/118.70 %-------------------------------------------
% 118.58/118.73 %------------------------------------------------------------------------------
% 118.58/118.73 % File : SWV374+1 : TPTP v8.2.0. Released v3.3.0.
% 118.58/118.73 % Domain : Software Verification
% 118.58/118.73 % Problem : Priority queue checker: lemma_ok_find_min
% 118.58/118.73 % Version : [dNP05] axioms.
% 118.58/118.73 % English :
% 118.58/118.73
% 118.58/118.73 % Refs : [Pis06] Piskac (2006), Email to Geoff Sutcliffe
% 118.58/118.73 % : [dNP05] de Nivelle & Piskac (2005), Verification of an Off-Lin
% 118.58/118.73 % Source : [Pis06]
% 118.58/118.73 % Names : cpq_l010 [Pis06]
% 118.58/118.73
% 118.58/118.73 % Status : Theorem
% 118.58/118.73 % Rating : 0.39 v8.1.0, 0.42 v7.5.0, 0.44 v7.4.0, 0.33 v7.3.0, 0.45 v7.2.0, 0.41 v7.1.0, 0.39 v7.0.0, 0.37 v6.4.0, 0.50 v6.2.0, 0.48 v6.1.0, 0.57 v6.0.0, 0.52 v5.4.0, 0.54 v5.3.0, 0.63 v5.2.0, 0.65 v5.1.0, 0.62 v5.0.0, 0.54 v4.1.0, 0.52 v4.0.0, 0.54 v3.7.0, 0.55 v3.5.0, 0.53 v3.4.0, 0.58 v3.3.0
% 118.58/118.73 % Syntax : Number of formulae : 42 ( 16 unt; 0 def)
% 118.58/118.73 % Number of atoms : 86 ( 30 equ)
% 118.58/118.73 % Maximal formula atoms : 4 ( 2 avg)
% 118.58/118.73 % Number of connectives : 58 ( 14 ~; 3 |; 14 &)
% 118.58/118.73 % ( 7 <=>; 20 =>; 0 <=; 0 <~>)
% 118.58/118.73 % Maximal formula depth : 9 ( 5 avg)
% 118.58/118.73 % Maximal term depth : 4 ( 1 avg)
% 118.58/118.73 % Number of predicates : 11 ( 9 usr; 1 prp; 0-3 aty)
% 118.58/118.73 % Number of functors : 18 ( 18 usr; 3 con; 0-3 aty)
% 118.58/118.73 % Number of variables : 120 ( 120 !; 0 ?)
% 118.58/118.73 % SPC : FOF_THM_RFO_SEQ
% 118.58/118.73
% 118.58/118.73 % Comments :
% 118.58/118.73 %------------------------------------------------------------------------------
% 118.58/118.73 %----Include the axioms about priority queues and checked priority queues
% 118.58/118.73 include('Axioms/SWV007+0.ax').
% 118.58/118.73 include('Axioms/SWV007+2.ax').
% 118.58/118.73 include('Axioms/SWV007+3.ax').
% 118.58/118.73 %------------------------------------------------------------------------------
% 118.58/118.73 %----lemma_ok_find_min (conjecture)
% 118.58/118.73 fof(l10_co,conjecture,
% 118.58/118.73 ! [U,V,W] :
% 118.58/118.73 ( ok(findmin_cpq_eff(triple(U,V,W)))
% 118.58/118.73 => ( V != create_slb
% 118.58/118.73 & contains_slb(V,findmin_pqp_res(U))
% 118.58/118.73 & less_than(lookup_slb(V,findmin_pqp_res(U)),findmin_pqp_res(U)) ) ) ).
% 118.58/118.73
% 118.58/118.73 %------------------------------------------------------------------------------
% 118.58/118.73 %-------------------------------------------
% 118.58/118.73 % Proof found
% 118.58/118.73 % SZS status Theorem for theBenchmark
% 118.58/118.73 % SZS output start Proof
% 118.63/118.75 %ClaNum:93(EqnAxiom:43)
% 118.63/118.75 %VarNum:299(SingletonVarNum:147)
% 118.63/118.75 %MaxLitNum:4
% 118.63/118.75 %MaxfuncDepth:3
% 118.63/118.75 %SharedTerms:15
% 118.63/118.75 %goalClause: 54 70
% 118.63/118.75 %singleGoalClaCount:1
% 118.63/118.75 [56]~P2(a1)
% 118.63/118.75 [54]P7(f8(f19(a9,a10,a11)))
% 118.63/118.75 [45]P1(a2,x451)
% 118.63/118.75 [46]P1(x461,x461)
% 118.63/118.75 [47]P6(x471,x471)
% 118.63/118.75 [57]~P4(a1,x571)
% 118.63/118.75 [44]E(f4(a1,x441),a1)
% 118.63/118.75 [58]~P8(a1,x581,x582)
% 118.63/118.75 [52]P3(f19(x521,a1,x522))
% 118.63/118.75 [59]~P7(f19(x591,x592,a3))
% 118.63/118.75 [51]E(f7(f19(x511,a1,x512)),a2)
% 118.63/118.75 [53]E(f8(f19(x531,a1,x532)),f19(x531,a1,a3))
% 118.63/118.75 [48]P2(f6(x481,f5(x482,x483)))
% 118.63/118.75 [49]E(f16(f6(x491,f5(x492,x493)),x492),x491)
% 118.63/118.75 [50]E(f15(f6(x501,f5(x502,x503)),x502),x503)
% 118.63/118.75 [55]E(f19(f12(x551,x552),f6(x553,f5(x552,a2)),x554),f13(f19(x551,x553,x554),x552))
% 118.63/118.75 [60]P1(x602,x601)+P1(x601,x602)
% 118.63/118.75 [61]~P9(x611,x612)+P1(x611,x612)
% 118.63/118.75 [63]~P9(x632,x631)+~P1(x631,x632)
% 118.63/118.75 [62]~P6(x621,x622)+P6(x621,f8(x622))
% 118.63/118.75 [68]~P6(x681,x682)+P6(x681,f17(f8(x682),f7(x682)))
% 118.63/118.75 [66]~P6(x661,x662)+P6(x661,f13(x662,x663))
% 118.63/118.75 [67]~P6(x671,x672)+P6(x671,f17(x672,x673))
% 118.63/118.75 [71]E(x711,a3)+P7(f19(x712,x713,x711))
% 118.63/118.75 [73]E(x731,a1)+E(f7(f19(x732,x731,x733)),f14(x732))
% 118.63/118.75 [76]~P4(x762,x764)+P5(f19(x761,x762,x763),x764)
% 118.63/118.75 [82]P4(x821,x822)+~P5(f19(x823,x821,x824),x822)
% 118.63/118.75 [69]~E(x692,x694)+P4(f6(x691,f5(x692,x693)),x694)
% 118.63/118.75 [72]~P4(x721,x724)+P4(f6(x721,f5(x722,x723)),x724)
% 118.63/118.75 [81]P4(x812,x814)+E(f17(f19(x811,x812,x813),x814),f19(x811,x812,a3))
% 118.63/118.75 [78]~P1(x782,x784)+E(f6(f4(x781,x782),f5(x783,x784)),f4(f6(x781,f5(x783,x784)),x782))
% 118.63/118.75 [79]~P9(x793,x794)+E(f4(f6(x791,f5(x792,x793)),x794),f6(f4(x791,x794),f5(x792,x794)))
% 118.63/118.75 [83]~P8(x831,x834,x835)+P8(f6(x831,f5(x832,x833)),x834,x835)
% 118.63/118.75 [91]~P9(x911,x912)+~P3(f19(x913,f6(x914,f5(x911,x912)),x915))
% 118.63/118.75 [70]E(a10,a1)+~P4(a10,f14(a9))+~P1(f15(a10,f14(a9)),f14(a9))
% 118.63/118.75 [64]P9(x642,x641)+~P1(x642,x641)+P1(x641,x642)
% 118.63/118.76 [65]~P1(x651,x653)+P1(x651,x652)+~P1(x653,x652)
% 118.63/118.76 [84]P4(x841,f14(x842))+E(x841,a1)+E(f8(f19(x842,x841,x843)),f19(x842,f4(x841,f14(x842)),a3))
% 118.63/118.76 [77]E(x771,x772)+P4(x773,x772)+~P4(f6(x773,f5(x771,x774)),x772)
% 118.63/118.76 [87]~P4(x872,x874)+~P9(x874,f15(x872,x874))+E(f17(f19(x871,x872,x873),x874),f19(f18(x871,x874),f16(x872,x874),a3))
% 118.63/118.76 [88]~P4(x883,x882)+~P1(f15(x883,x882),x882)+E(f19(f18(x881,x882),f16(x883,x882),x884),f17(f19(x881,x883,x884),x882))
% 118.63/118.76 [74]~P4(x743,x742)+E(x741,x742)+E(f15(f6(x743,f5(x741,x744)),x742),f15(x743,x742))
% 118.63/118.76 [80]~P4(x803,x802)+E(x801,x802)+E(f16(f6(x803,f5(x801,x804)),x802),f6(f16(x803,x802),f5(x801,x804)))
% 118.63/118.76 [75]~E(x753,x755)+~E(x752,x754)+P8(f6(x751,f5(x752,x753)),x754,x755)
% 118.63/118.76 [85]E(x851,x852)+P8(x853,x854,x852)+~P8(f6(x853,f5(x855,x851)),x854,x852)
% 118.63/118.76 [86]E(x861,x862)+P8(x863,x862,x864)+~P8(f6(x863,f5(x861,x865)),x862,x864)
% 118.63/118.76 [92]~P1(x924,x923)+~P3(f19(x921,x922,x925))+P3(f19(x921,f6(x922,f5(x923,x924)),x925))
% 118.63/118.76 [93]~P1(x934,x935)+P3(f19(x931,x932,x933))+~P3(f19(x931,f6(x932,f5(x935,x934)),x933))
% 118.63/118.76 [89]~P4(x891,f14(x892))+E(x891,a1)+~P9(f14(x892),f15(x891,f14(x892)))+E(f8(f19(x892,x891,x893)),f19(x892,f4(x891,f14(x892)),a3))
% 118.63/118.76 [90]~P4(x901,f14(x902))+E(x901,a1)+~P1(f15(x901,f14(x902)),f14(x902))+E(f19(x902,f4(x901,f14(x902)),x903),f8(f19(x902,x901,x903)))
% 118.63/118.76 %EqnAxiom
% 118.63/118.76 [1]E(x11,x11)
% 118.63/118.76 [2]E(x22,x21)+~E(x21,x22)
% 118.63/118.76 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 118.63/118.76 [4]~E(x41,x42)+E(f4(x41,x43),f4(x42,x43))
% 118.63/118.76 [5]~E(x51,x52)+E(f4(x53,x51),f4(x53,x52))
% 118.63/118.76 [6]~E(x61,x62)+E(f5(x61,x63),f5(x62,x63))
% 118.63/118.76 [7]~E(x71,x72)+E(f5(x73,x71),f5(x73,x72))
% 118.63/118.76 [8]~E(x81,x82)+E(f6(x81,x83),f6(x82,x83))
% 118.63/118.76 [9]~E(x91,x92)+E(f6(x93,x91),f6(x93,x92))
% 118.63/118.76 [10]~E(x101,x102)+E(f19(x101,x103,x104),f19(x102,x103,x104))
% 118.63/118.76 [11]~E(x111,x112)+E(f19(x113,x111,x114),f19(x113,x112,x114))
% 118.63/118.76 [12]~E(x121,x122)+E(f19(x123,x124,x121),f19(x123,x124,x122))
% 118.63/118.76 [13]~E(x131,x132)+E(f8(x131),f8(x132))
% 118.63/118.76 [14]~E(x141,x142)+E(f16(x141,x143),f16(x142,x143))
% 118.63/118.76 [15]~E(x151,x152)+E(f16(x153,x151),f16(x153,x152))
% 118.63/118.76 [16]~E(x161,x162)+E(f14(x161),f14(x162))
% 118.63/118.76 [17]~E(x171,x172)+E(f15(x171,x173),f15(x172,x173))
% 118.63/118.76 [18]~E(x181,x182)+E(f15(x183,x181),f15(x183,x182))
% 118.63/118.76 [19]~E(x191,x192)+E(f17(x191,x193),f17(x192,x193))
% 118.63/118.76 [20]~E(x201,x202)+E(f17(x203,x201),f17(x203,x202))
% 118.63/118.76 [21]~E(x211,x212)+E(f13(x211,x213),f13(x212,x213))
% 118.63/118.76 [22]~E(x221,x222)+E(f13(x223,x221),f13(x223,x222))
% 118.63/118.76 [23]~E(x231,x232)+E(f7(x231),f7(x232))
% 118.63/118.76 [24]~E(x241,x242)+E(f18(x241,x243),f18(x242,x243))
% 118.63/118.76 [25]~E(x251,x252)+E(f18(x253,x251),f18(x253,x252))
% 118.63/118.76 [26]~E(x261,x262)+E(f12(x261,x263),f12(x262,x263))
% 118.63/118.76 [27]~E(x271,x272)+E(f12(x273,x271),f12(x273,x272))
% 118.63/118.76 [28]P1(x282,x283)+~E(x281,x282)+~P1(x281,x283)
% 118.63/118.76 [29]P1(x293,x292)+~E(x291,x292)+~P1(x293,x291)
% 118.63/118.76 [30]~P3(x301)+P3(x302)+~E(x301,x302)
% 118.63/118.76 [31]P6(x312,x313)+~E(x311,x312)+~P6(x311,x313)
% 118.63/118.76 [32]P6(x323,x322)+~E(x321,x322)+~P6(x323,x321)
% 118.63/118.76 [33]~P2(x331)+P2(x332)+~E(x331,x332)
% 118.63/118.76 [34]P8(x342,x343,x344)+~E(x341,x342)+~P8(x341,x343,x344)
% 118.63/118.76 [35]P8(x353,x352,x354)+~E(x351,x352)+~P8(x353,x351,x354)
% 118.63/118.76 [36]P8(x363,x364,x362)+~E(x361,x362)+~P8(x363,x364,x361)
% 118.63/118.76 [37]~P7(x371)+P7(x372)+~E(x371,x372)
% 118.63/118.76 [38]P4(x382,x383)+~E(x381,x382)+~P4(x381,x383)
% 118.63/118.76 [39]P4(x393,x392)+~E(x391,x392)+~P4(x393,x391)
% 118.63/118.76 [40]P9(x402,x403)+~E(x401,x402)+~P9(x401,x403)
% 118.63/118.76 [41]P9(x413,x412)+~E(x411,x412)+~P9(x413,x411)
% 118.63/118.76 [42]P5(x422,x423)+~E(x421,x422)+~P5(x421,x423)
% 118.63/118.76 [43]P5(x433,x432)+~E(x431,x432)+~P5(x433,x431)
% 118.63/118.76
% 118.63/118.76 %-------------------------------------------
% 118.67/118.79 cnf(94,plain,
% 118.67/118.79 (P4(f6(x942,f5(x941,x943)),x941)),
% 118.67/118.79 inference(equality_inference,[],[69])).
% 118.67/118.79 cnf(95,plain,
% 118.67/118.79 (E(a1,f4(a1,x951))),
% 118.67/118.79 inference(scs_inference,[],[44,2])).
% 118.67/118.79 cnf(98,plain,
% 118.67/118.79 (~P7(f8(f19(x981,a1,x982)))),
% 118.67/118.79 inference(scs_inference,[],[46,44,59,53,2,63,37])).
% 118.67/118.79 cnf(101,plain,
% 118.67/118.79 (E(f16(f6(f4(a1,x1011),f5(x1012,x1013)),x1012),a1)),
% 118.67/118.79 inference(scs_inference,[],[46,44,59,53,49,2,63,37,3])).
% 118.67/118.79 cnf(103,plain,
% 118.67/118.79 (P1(a1,f4(a1,x1031))),
% 118.67/118.79 inference(scs_inference,[],[46,44,59,53,49,2,63,37,3,28])).
% 118.67/118.79 cnf(104,plain,
% 118.67/118.79 (P1(x1041,x1041)),
% 118.67/118.79 inference(rename_variables,[],[46])).
% 118.67/118.79 cnf(105,plain,
% 118.67/118.79 (P1(f4(a1,x1051),a1)),
% 118.67/118.79 inference(scs_inference,[],[46,104,44,59,53,49,2,63,37,3,28,29])).
% 118.67/118.79 cnf(107,plain,
% 118.67/118.79 (P6(a1,f4(a1,x1071))),
% 118.67/118.79 inference(scs_inference,[],[46,104,47,44,59,53,49,2,63,37,3,28,29,31])).
% 118.67/118.79 cnf(108,plain,
% 118.67/118.79 (P6(x1081,x1081)),
% 118.67/118.79 inference(rename_variables,[],[47])).
% 118.67/118.79 cnf(109,plain,
% 118.67/118.79 (P6(f4(a1,x1091),a1)),
% 118.67/118.79 inference(scs_inference,[],[46,104,47,108,44,59,53,49,2,63,37,3,28,29,31,32])).
% 118.67/118.79 cnf(111,plain,
% 118.67/118.79 (~P2(f4(a1,x1111))),
% 118.67/118.79 inference(scs_inference,[],[46,104,47,108,56,44,59,53,49,2,63,37,3,28,29,31,32,33])).
% 118.67/118.79 cnf(112,plain,
% 118.67/118.79 (~E(f6(x1121,f5(x1122,x1123)),a1)),
% 118.67/118.79 inference(scs_inference,[],[94,46,104,47,108,57,56,44,59,53,49,2,63,37,3,28,29,31,32,33,38])).
% 118.67/118.79 cnf(113,plain,
% 118.67/118.79 (P4(f6(x1131,f5(x1132,x1133)),x1132)),
% 118.67/118.79 inference(rename_variables,[],[94])).
% 118.67/118.79 cnf(114,plain,
% 118.67/118.79 (P4(f6(x1141,f5(f4(a1,x1142),x1143)),a1)),
% 118.67/118.79 inference(scs_inference,[],[94,113,46,104,47,108,57,56,44,59,53,49,2,63,37,3,28,29,31,32,33,38,39])).
% 118.67/118.79 cnf(121,plain,
% 118.67/118.79 (E(a1,f16(f6(f4(a1,x1211),f5(x1212,x1213)),x1212))),
% 118.67/118.79 inference(scs_inference,[],[101,103,63,2])).
% 118.67/118.79 cnf(122,plain,
% 118.67/118.79 (P1(f4(a1,x1221),f4(a1,x1222))),
% 118.67/118.79 inference(scs_inference,[],[101,103,105,63,2,65])).
% 118.67/118.79 cnf(124,plain,
% 118.67/118.79 (~P2(f16(f6(f4(a1,x1241),f5(x1242,x1243)),x1242))),
% 118.67/118.79 inference(scs_inference,[],[101,103,105,56,63,2,65,33])).
% 118.67/118.79 cnf(125,plain,
% 118.67/118.79 (P1(f16(f6(f4(a1,x1251),f5(x1252,x1253)),x1252),a1)),
% 118.67/118.79 inference(scs_inference,[],[101,103,105,56,46,63,2,65,33,29])).
% 118.67/118.79 cnf(126,plain,
% 118.67/118.79 (P1(x1261,x1261)),
% 118.67/118.79 inference(rename_variables,[],[46])).
% 118.67/118.79 cnf(127,plain,
% 118.67/118.79 (P6(f4(a1,x1271),f4(a1,x1272))),
% 118.67/118.79 inference(scs_inference,[],[101,95,103,105,109,56,46,63,2,65,33,29,32])).
% 118.67/118.79 cnf(128,plain,
% 118.67/118.79 (P4(f6(x1281,f5(f4(a1,x1282),x1283)),f4(a1,x1284))),
% 118.67/118.79 inference(scs_inference,[],[101,95,103,105,109,114,56,46,63,2,65,33,29,32,39])).
% 118.67/118.79 cnf(131,plain,
% 118.67/118.79 (~E(f6(x1311,f5(x1312,x1313)),f16(f6(f4(a1,x1314),f5(x1315,x1316)),x1315))),
% 118.67/118.79 inference(scs_inference,[],[112,101,95,103,105,109,114,47,56,46,63,2,65,33,29,32,39,31,3])).
% 118.67/118.79 cnf(132,plain,
% 118.67/118.79 (~P7(f16(f6(f8(f19(x1321,a1,x1322)),f5(x1323,x1324)),x1323))),
% 118.67/118.79 inference(scs_inference,[],[98,112,101,95,103,105,109,114,47,56,49,46,63,2,65,33,29,32,39,31,3,37])).
% 118.67/118.79 cnf(134,plain,
% 118.67/118.79 (P1(a1,f16(f6(f4(a1,x1341),f5(x1342,x1343)),x1342))),
% 118.67/118.79 inference(scs_inference,[],[98,112,101,95,103,105,109,114,47,56,49,46,126,63,2,65,33,29,32,39,31,3,37,28])).
% 118.67/118.79 cnf(136,plain,
% 118.67/118.79 (E(f4(a1,x1361),f4(a1,x1362))),
% 118.67/118.79 inference(scs_inference,[],[98,112,101,95,103,105,109,114,47,57,56,49,46,126,63,2,65,33,29,32,39,31,3,37,28,77])).
% 118.67/118.79 cnf(142,plain,
% 118.67/118.79 (E(x1421,f15(f6(x1422,f5(x1423,x1421)),x1423))),
% 118.67/118.79 inference(scs_inference,[],[105,50,63,2])).
% 118.67/118.79 cnf(146,plain,
% 118.67/118.79 (E(f16(f6(f4(a1,x1461),f5(x1462,x1463)),x1462),f4(a1,x1464))),
% 118.67/118.79 inference(scs_inference,[],[105,121,134,109,95,101,50,63,2,65,32,3])).
% 118.67/118.79 cnf(147,plain,
% 118.67/118.79 (P6(f16(f6(f4(a1,x1471),f5(x1472,x1473)),x1472),f4(a1,x1474))),
% 118.67/118.79 inference(scs_inference,[],[105,121,134,107,109,95,101,50,63,2,65,32,3,31])).
% 118.67/118.79 cnf(148,plain,
% 118.67/118.79 (P4(f6(x1481,f5(a1,x1482)),f16(f6(f4(a1,x1483),f5(x1484,x1485)),x1484))),
% 118.67/118.79 inference(scs_inference,[],[94,105,121,134,107,109,95,101,50,63,2,65,32,3,31,39])).
% 118.67/118.79 cnf(150,plain,
% 118.67/118.79 (P1(f16(f6(f4(a1,x1501),f5(x1502,x1503)),x1502),f4(a1,x1504))),
% 118.67/118.79 inference(scs_inference,[],[94,103,105,121,134,107,109,95,101,50,63,2,65,32,3,31,39,28])).
% 118.67/118.79 cnf(156,plain,
% 118.67/118.79 (E(f4(a1,x1561),f16(f6(f4(a1,x1562),f5(x1563,x1564)),x1563))),
% 118.67/118.79 inference(scs_inference,[],[134,146,63,2])).
% 118.67/118.79 cnf(157,plain,
% 118.67/118.79 (P1(f4(a1,x1571),f15(f6(x1572,f5(x1573,a1)),x1573))),
% 118.67/118.79 inference(scs_inference,[],[134,105,142,146,63,2,29])).
% 118.67/118.79 cnf(158,plain,
% 118.67/118.79 (E(x1581,f15(f6(x1582,f5(x1583,x1581)),x1583))),
% 118.67/118.79 inference(rename_variables,[],[142])).
% 118.67/118.79 cnf(159,plain,
% 118.67/118.79 (P6(f15(f6(x1591,f5(x1592,a1)),x1592),f4(a1,x1593))),
% 118.67/118.79 inference(scs_inference,[],[134,105,142,158,146,107,63,2,29,31])).
% 118.67/118.79 cnf(160,plain,
% 118.67/118.79 (E(x1601,f15(f6(x1602,f5(x1603,x1601)),x1603))),
% 118.67/118.79 inference(rename_variables,[],[142])).
% 118.67/118.79 cnf(161,plain,
% 118.67/118.79 (P6(f4(a1,x1611),f15(f6(x1612,f5(x1613,a1)),x1613))),
% 118.67/118.79 inference(scs_inference,[],[134,105,142,158,160,146,107,109,63,2,29,31,32])).
% 118.67/118.79 cnf(162,plain,
% 118.67/118.79 (E(x1621,f15(f6(x1622,f5(x1623,x1621)),x1623))),
% 118.67/118.79 inference(rename_variables,[],[142])).
% 118.67/118.79 cnf(163,plain,
% 118.67/118.79 (P1(f15(f6(x1631,f5(x1632,a1)),x1632),f4(a1,x1633))),
% 118.67/118.79 inference(scs_inference,[],[103,134,105,142,158,160,162,146,107,109,63,2,29,31,32,28])).
% 118.67/118.79 cnf(164,plain,
% 118.67/118.79 (E(x1641,f15(f6(x1642,f5(x1643,x1641)),x1643))),
% 118.67/118.79 inference(rename_variables,[],[142])).
% 118.67/118.79 cnf(165,plain,
% 118.67/118.79 (P4(f6(x1651,f5(x1652,x1653)),f15(f6(x1654,f5(x1655,x1652)),x1655))),
% 118.67/118.79 inference(scs_inference,[],[103,134,105,94,142,158,160,162,164,146,107,109,63,2,29,31,32,28,39])).
% 118.67/118.79 cnf(167,plain,
% 118.67/118.79 (~E(f6(x1671,f5(x1672,x1673)),f4(a1,x1674))),
% 118.67/118.79 inference(scs_inference,[],[103,134,105,94,142,158,160,162,164,146,112,107,109,44,63,2,29,31,32,28,39,3])).
% 118.67/118.79 cnf(177,plain,
% 118.67/118.79 (E(f19(x1771,a1,a3),f8(f19(x1771,a1,x1772)))),
% 118.67/118.79 inference(scs_inference,[],[125,53,63,2])).
% 118.67/118.79 cnf(178,plain,
% 118.67/118.79 (P6(f16(f6(f4(a1,x1781),f5(x1782,x1783)),x1782),a1)),
% 118.67/118.79 inference(scs_inference,[],[125,156,109,53,63,2,31])).
% 118.67/118.79 cnf(180,plain,
% 118.67/118.79 (P1(f15(f6(x1801,f5(x1802,a2)),x1802),x1803)),
% 118.67/118.79 inference(scs_inference,[],[125,156,142,109,45,53,63,2,31,28])).
% 118.67/118.79 cnf(188,plain,
% 118.67/118.79 (E(f13(f19(x1881,x1882,x1883),x1884),f19(f12(x1881,x1884),f6(x1882,f5(x1884,a2)),x1883))),
% 118.67/118.79 inference(scs_inference,[],[150,55,63,2])).
% 118.67/118.79 cnf(189,plain,
% 118.67/118.79 (E(f8(f19(x1891,a1,x1892)),f8(f19(x1891,a1,x1893)))),
% 118.67/118.79 inference(scs_inference,[],[150,177,53,55,63,2,3])).
% 118.67/118.79 cnf(191,plain,
% 118.67/118.79 (P4(f6(x1911,f5(a1,x1912)),f4(a1,x1913))),
% 118.67/118.79 inference(scs_inference,[],[150,146,177,148,53,55,63,2,3,39])).
% 118.67/118.79 cnf(193,plain,
% 118.67/118.79 (~P7(f13(f19(x1931,x1932,a3),x1933))),
% 118.67/118.79 inference(scs_inference,[],[150,146,177,148,53,59,55,63,2,3,39,37])).
% 118.67/118.79 cnf(204,plain,
% 118.67/118.79 (E(a2,f7(f19(x2041,a1,x2042)))),
% 118.67/118.79 inference(scs_inference,[],[163,51,63,2])).
% 118.67/118.79 cnf(205,plain,
% 118.67/118.79 (E(f15(f6(x2051,f5(x2052,a2)),x2052),f7(f19(x2053,a1,x2054)))),
% 118.67/118.79 inference(scs_inference,[],[163,50,51,63,2,3])).
% 118.67/118.79 cnf(210,plain,
% 118.67/118.79 (~P9(f15(f6(x2101,f5(x2102,a1)),x2102),f4(a1,x2103))),
% 118.67/118.79 inference(scs_inference,[],[157,63])).
% 118.67/118.79 cnf(212,plain,
% 118.67/118.79 (E(f7(f19(x2121,a1,x2122)),f15(f6(x2123,f5(x2124,a2)),x2124))),
% 118.67/118.79 inference(scs_inference,[],[157,205,63,2])).
% 118.67/118.79 cnf(213,plain,
% 118.67/118.79 (P4(f6(x2131,f5(a2,x2132)),f7(f19(x2133,a1,x2134)))),
% 118.67/118.79 inference(scs_inference,[],[157,205,165,63,2,39])).
% 118.67/118.79 cnf(215,plain,
% 118.67/118.79 (P1(f7(f19(x2151,a1,x2152)),x2153)),
% 118.67/118.79 inference(scs_inference,[],[157,180,205,165,63,2,39,28])).
% 118.67/118.79 cnf(217,plain,
% 118.67/118.79 (E(f16(f6(a2,f5(x2171,x2172)),x2171),f7(f19(x2173,a1,x2174)))),
% 118.67/118.79 inference(scs_inference,[],[157,180,205,204,165,49,63,2,39,28,3])).
% 118.67/118.79 cnf(224,plain,
% 118.67/118.79 (E(f7(f19(x2241,a1,x2242)),f16(f6(a2,f5(x2243,x2244)),x2243))),
% 118.67/118.79 inference(scs_inference,[],[180,217,63,2])).
% 118.67/118.79 cnf(225,plain,
% 118.67/118.79 (P1(f8(f19(x2251,a1,x2252)),f8(f19(x2251,a1,x2253)))),
% 118.67/118.79 inference(scs_inference,[],[189,180,217,46,63,2,29])).
% 118.67/118.79 cnf(229,plain,
% 118.67/118.79 (E(f7(f19(x2291,a1,x2292)),f7(f19(x2293,a1,x2294)))),
% 118.67/118.79 inference(scs_inference,[],[189,180,212,217,205,46,47,63,2,29,32,3])).
% 118.67/118.79 cnf(241,plain,
% 118.67/118.79 (E(x2411,f16(f6(x2411,f5(x2412,x2413)),x2412))),
% 118.67/118.79 inference(scs_inference,[],[215,49,63,2])).
% 118.67/118.79 cnf(242,plain,
% 118.67/118.79 (P1(f19(x2421,a1,a3),f8(f19(x2421,a1,x2422)))),
% 118.67/118.79 inference(scs_inference,[],[177,215,46,49,63,2,29])).
% 118.67/118.79 cnf(245,plain,
% 118.67/118.79 (P6(x2451,x2451)),
% 118.67/118.79 inference(rename_variables,[],[47])).
% 118.67/118.79 cnf(246,plain,
% 118.67/118.79 (P6(f8(f19(x2461,a1,x2462)),f19(x2461,a1,a3))),
% 118.67/118.79 inference(scs_inference,[],[177,215,46,47,245,49,63,2,29,32,31])).
% 118.67/118.79 cnf(248,plain,
% 118.67/118.79 (P2(f16(f6(f6(x2481,f5(x2482,x2483)),f5(x2484,x2485)),x2484))),
% 118.67/118.80 inference(scs_inference,[],[177,215,46,47,245,48,49,63,2,29,32,31,33])).
% 118.67/118.80 cnf(249,plain,
% 118.67/118.80 (P4(f6(x2491,f5(f19(x2492,a1,a3),x2493)),f8(f19(x2492,a1,x2494)))),
% 118.67/118.80 inference(scs_inference,[],[177,94,215,46,47,245,48,49,63,2,29,32,31,33,39])).
% 118.67/118.80 cnf(251,plain,
% 118.67/118.80 (P1(f16(f6(a2,f5(x2511,x2512)),x2511),x2513)),
% 118.67/118.80 inference(scs_inference,[],[177,94,215,224,46,47,245,48,49,63,2,29,32,31,33,39,28])).
% 118.67/118.80 cnf(259,plain,
% 118.67/118.80 (P1(f8(f19(x2591,a1,x2592)),f19(x2591,a1,a3))),
% 118.67/118.80 inference(scs_inference,[],[177,251,46,63,28])).
% 118.67/118.80 cnf(261,plain,
% 118.67/118.80 (P7(f16(f6(f8(f19(a9,a10,a11)),f5(x2611,x2612)),x2611))),
% 118.67/118.80 inference(scs_inference,[],[54,177,241,251,46,63,28,37])).
% 118.67/118.80 cnf(266,plain,
% 118.67/118.80 (~P9(f8(f19(x2661,a1,x2662)),f19(x2661,a1,a3))),
% 118.67/118.80 inference(scs_inference,[],[242,63])).
% 118.67/118.80 cnf(280,plain,
% 118.67/118.80 (~P9(f8(f19(x2801,a1,x2802)),f8(f19(x2801,a1,x2803)))),
% 118.67/118.80 inference(scs_inference,[],[225,63])).
% 118.67/118.80 cnf(294,plain,
% 118.67/118.80 (~P9(f19(x2941,a1,a3),f8(f19(x2941,a1,x2942)))),
% 118.67/118.80 inference(scs_inference,[],[259,63])).
% 118.67/118.80 cnf(344,plain,
% 118.67/118.80 (~P3(f19(f12(x3441,x3442),f6(x3443,f5(x3442,a2)),x3444))+P3(f13(f19(x3441,x3443,x3444),x3442))),
% 118.67/118.80 inference(scs_inference,[],[55,44,37,30])).
% 118.67/118.80 cnf(370,plain,
% 118.67/118.80 (E(f4(a1,x3701),f15(f6(x3702,f5(x3703,a1)),x3703))),
% 118.67/118.80 inference(scs_inference,[],[44,163,142,159,161,32,29,31,3])).
% 118.67/118.80 cnf(374,plain,
% 118.67/118.80 (E(f15(f6(x3741,f5(x3742,a1)),x3742),f4(a1,x3743))),
% 118.67/118.80 inference(scs_inference,[],[44,163,142,159,161,32,29,31,3,63,2])).
% 118.67/118.80 cnf(375,plain,
% 118.67/118.80 (~P2(f15(f6(x3751,f5(x3752,a1)),x3752))),
% 118.67/118.80 inference(scs_inference,[],[44,163,142,159,161,111,32,29,31,3,63,2,33])).
% 118.67/118.80 cnf(381,plain,
% 118.67/118.80 (~E(f6(x3811,f5(x3812,x3813)),f15(f6(x3814,f5(x3815,a1)),x3815))),
% 118.67/118.80 inference(scs_inference,[],[167,374,3])).
% 118.67/118.80 cnf(388,plain,
% 118.67/118.80 (P6(x3881,x3881)),
% 118.67/118.80 inference(rename_variables,[],[47])).
% 118.67/118.80 cnf(389,plain,
% 118.67/118.80 (P6(f7(f19(x3891,a1,x3892)),f16(f6(a2,f5(x3893,x3894)),x3893))),
% 118.67/118.80 inference(scs_inference,[],[217,47,388,32,31])).
% 118.67/118.80 cnf(391,plain,
% 118.67/118.80 (P6(f7(f19(x3911,a1,x3912)),f7(f19(x3913,a1,x3914)))),
% 118.67/118.80 inference(scs_inference,[],[217,389,32])).
% 118.67/118.80 cnf(393,plain,
% 118.67/118.80 (P6(f7(f19(x3931,a1,x3932)),a2)),
% 118.67/118.80 inference(scs_inference,[],[204,217,389,47,32,31])).
% 118.67/118.80 cnf(395,plain,
% 118.67/118.80 (P6(f7(f19(x3951,a1,x3952)),f15(f6(x3953,f5(x3954,a2)),x3954))),
% 118.67/118.80 inference(scs_inference,[],[212,391,32])).
% 118.67/118.80 cnf(399,plain,
% 118.67/118.80 (P6(a1,f8(f13(f4(a1,x3991),x3992)))),
% 118.67/118.80 inference(scs_inference,[],[107,62,66])).
% 118.67/118.80 cnf(404,plain,
% 118.67/118.80 (E(f8(f7(f19(x4041,a1,x4042))),f8(a2))),
% 118.67/118.80 inference(scs_inference,[],[204,13,2])).
% 118.67/118.80 cnf(405,plain,
% 118.67/118.80 (E(f8(a2),f8(f7(f19(x4051,a1,x4052))))),
% 118.67/118.80 inference(scs_inference,[],[404,2])).
% 118.67/118.80 cnf(422,plain,
% 118.67/118.80 (P6(x4221,f17(f17(f8(x4221),f7(x4221)),x4222))),
% 118.67/118.80 inference(scs_inference,[],[47,67,68])).
% 118.67/118.80 cnf(423,plain,
% 118.67/118.80 (P8(f6(x4231,f5(a3,a3)),a3,a3)),
% 118.67/118.80 inference(scs_inference,[],[59,71,75])).
% 118.67/118.80 cnf(424,plain,
% 118.67/118.80 (P8(f6(x4241,f5(a3,a3)),f16(f6(a3,f5(x4242,x4243)),x4242),a3)),
% 118.67/118.80 inference(scs_inference,[],[241,423,35])).
% 118.67/118.80 cnf(425,plain,
% 118.67/118.80 (E(x4251,f16(f6(x4251,f5(x4252,x4253)),x4252))),
% 118.67/118.80 inference(rename_variables,[],[241])).
% 118.67/118.80 cnf(426,plain,
% 118.67/118.80 (P8(f6(x4261,f5(a3,a3)),a3,f16(f6(a3,f5(x4262,x4263)),x4262))),
% 118.67/118.80 inference(scs_inference,[],[241,425,423,35,36])).
% 118.67/118.80 cnf(429,plain,
% 118.67/118.80 (P1(f16(f6(x4291,f5(x4292,x4293)),x4292),x4291)),
% 118.67/118.80 inference(scs_inference,[],[49,46,29])).
% 118.67/118.80 cnf(430,plain,
% 118.67/118.80 (P1(x4301,x4301)),
% 118.67/118.80 inference(rename_variables,[],[46])).
% 118.67/118.80 cnf(431,plain,
% 118.67/118.80 (P1(x4311,f16(f6(x4311,f5(x4312,x4313)),x4312))),
% 118.67/118.80 inference(scs_inference,[],[49,46,430,29,28])).
% 118.67/118.80 cnf(433,plain,
% 118.67/118.80 (P6(f16(f6(x4331,f5(x4332,x4333)),x4332),x4331)),
% 118.67/118.80 inference(scs_inference,[],[49,46,430,47,29,28,32])).
% 118.67/118.80 cnf(434,plain,
% 118.67/118.80 (P6(x4341,x4341)),
% 118.67/118.80 inference(rename_variables,[],[47])).
% 118.67/118.80 cnf(435,plain,
% 118.67/118.80 (E(f16(f6(f19(x4351,a1,a3),f5(x4352,x4353)),x4352),f8(f19(x4351,a1,x4354)))),
% 118.67/118.80 inference(scs_inference,[],[49,177,46,430,47,29,28,32,3])).
% 118.67/118.80 cnf(436,plain,
% 118.67/118.80 (E(f16(f6(x4361,f5(x4362,x4363)),x4362),x4361)),
% 118.67/118.80 inference(rename_variables,[],[49])).
% 118.67/118.80 cnf(437,plain,
% 118.67/118.80 (P6(x4371,f16(f6(x4371,f5(x4372,x4373)),x4372))),
% 118.67/118.80 inference(scs_inference,[],[49,436,177,46,430,47,434,29,28,32,3,31])).
% 118.67/118.80 cnf(439,plain,
% 118.67/118.80 (~P7(f16(f6(f19(x4391,a1,a3),f5(x4392,x4393)),x4392))),
% 118.67/118.80 inference(scs_inference,[],[49,436,98,177,46,430,47,434,29,28,32,3,31,37])).
% 118.67/118.80 cnf(453,plain,
% 118.67/118.80 (~P9(f16(f6(x4531,f5(x4532,x4533)),x4532),x4531)),
% 118.67/118.80 inference(scs_inference,[],[431,63])).
% 118.67/118.80 cnf(455,plain,
% 118.67/118.80 (E(f16(f6(f8(f19(x4551,a1,x4552)),f5(x4553,x4554)),x4553),f19(x4551,a1,a3))),
% 118.67/118.80 inference(scs_inference,[],[49,431,53,63,3])).
% 118.67/118.80 cnf(457,plain,
% 118.67/118.80 (E(f19(x4571,a1,a3),f16(f6(f8(f19(x4571,a1,x4572)),f5(x4573,x4574)),x4573))),
% 118.67/118.80 inference(scs_inference,[],[49,431,53,63,3,2])).
% 118.67/118.80 cnf(474,plain,
% 118.67/118.80 (P1(x4741,f15(f6(x4742,f5(x4743,x4741)),x4743))),
% 118.67/118.80 inference(scs_inference,[],[50,46,28])).
% 118.67/118.80 cnf(475,plain,
% 118.67/118.80 (P1(x4751,x4751)),
% 118.67/118.80 inference(rename_variables,[],[46])).
% 118.67/118.80 cnf(478,plain,
% 118.67/118.80 (P6(f15(f6(x4781,f5(x4782,x4783)),x4782),x4783)),
% 118.67/118.80 inference(scs_inference,[],[50,46,475,47,28,29,32])).
% 118.67/118.80 cnf(489,plain,
% 118.67/118.80 (P6(f16(f6(f7(f19(x4891,a1,x4892)),f5(x4893,x4894)),x4893),a2)),
% 118.67/118.80 inference(scs_inference,[],[51,429,433,29,32])).
% 118.67/118.80 cnf(491,plain,
% 118.67/118.80 (E(f16(f6(f8(f19(x4911,a1,x4912)),f5(x4913,x4914)),x4913),f8(f19(x4911,a1,x4915)))),
% 118.67/118.80 inference(scs_inference,[],[51,177,455,429,433,29,32,3])).
% 118.67/118.80 cnf(497,plain,
% 118.67/118.80 (E(f8(f19(x4971,a1,x4972)),f16(f6(f8(f19(x4971,a1,x4973)),f5(x4974,x4975)),x4974))),
% 118.67/118.80 inference(scs_inference,[],[51,177,455,429,433,437,29,32,3,31,63,2])).
% 118.67/118.80 cnf(510,plain,
% 118.67/118.80 (P5(f19(x5101,f6(x5102,f5(f7(f19(x5103,a1,x5104)),x5105)),x5106),a2)),
% 118.67/118.80 inference(scs_inference,[],[51,76,69])).
% 118.67/118.80 cnf(513,plain,
% 118.67/118.80 (~P5(f19(x5131,f16(f6(f4(a1,x5132),f5(x5133,x5134)),x5133),x5135),x5136)),
% 118.67/118.80 inference(scs_inference,[],[57,101,82,38])).
% 118.67/118.80 cnf(514,plain,
% 118.67/118.80 (E(f5(f7(f19(x5141,a1,x5142)),x5143),f5(a2,x5143))),
% 118.67/118.80 inference(scs_inference,[],[204,6,2])).
% 118.67/118.80 cnf(515,plain,
% 118.67/118.80 (E(f5(a2,x5151),f5(f7(f19(x5152,a1,x5153)),x5151))),
% 118.67/118.80 inference(scs_inference,[],[514,2])).
% 118.67/118.80 cnf(516,plain,
% 118.67/118.80 (P6(f7(f19(x5161,a1,x5162)),f17(f17(f8(a2),f7(a2)),x5163))),
% 118.67/118.80 inference(scs_inference,[],[204,514,422,2,31])).
% 118.67/118.80 cnf(518,plain,
% 118.67/118.80 (P3(f16(f6(f19(x5181,a1,x5182),f5(x5183,x5184)),x5183))),
% 118.67/118.80 inference(scs_inference,[],[52,204,241,514,422,2,31,30])).
% 118.67/118.80 cnf(562,plain,
% 118.67/118.80 (P1(f13(f19(x5621,x5622,x5623),x5624),f19(f12(x5621,x5624),f6(x5622,f5(x5624,a2)),x5623))),
% 118.67/118.80 inference(scs_inference,[],[55,46,28])).
% 118.67/118.80 cnf(563,plain,
% 118.67/118.80 (P1(x5631,x5631)),
% 118.67/118.80 inference(rename_variables,[],[46])).
% 118.67/118.80 cnf(564,plain,
% 118.67/118.80 (P6(f19(f12(x5641,x5642),f6(x5643,f5(x5642,a2)),x5644),f13(f19(x5641,x5643,x5644),x5642))),
% 118.67/118.80 inference(scs_inference,[],[55,46,47,28,32])).
% 118.67/118.80 cnf(565,plain,
% 118.67/118.80 (P6(x5651,x5651)),
% 118.67/118.80 inference(rename_variables,[],[47])).
% 118.67/118.80 cnf(566,plain,
% 118.67/118.80 (P1(f19(f12(x5661,x5662),f6(x5663,f5(x5662,a2)),x5664),f13(f19(x5661,x5663,x5664),x5662))),
% 118.67/118.80 inference(scs_inference,[],[55,46,563,47,28,32,29])).
% 118.67/118.80 cnf(568,plain,
% 118.67/118.80 (P6(f13(f19(x5681,x5682,x5683),x5684),f19(f12(x5681,x5684),f6(x5682,f5(x5684,a2)),x5683))),
% 118.67/118.80 inference(scs_inference,[],[55,46,563,47,565,28,32,29,31])).
% 118.67/118.80 cnf(578,plain,
% 118.67/118.80 (P4(f6(f6(x5781,f5(a2,x5782)),f5(x5783,x5784)),f7(f19(x5785,a1,x5786)))),
% 118.67/118.80 inference(scs_inference,[],[204,72,69])).
% 118.67/118.80 cnf(587,plain,
% 118.67/118.80 (P6(f16(f6(a1,f5(x5871,x5872)),x5871),f4(a1,x5873))),
% 118.67/118.80 inference(scs_inference,[],[95,431,433,28,32])).
% 118.67/118.80 cnf(589,plain,
% 118.67/118.80 (P1(f16(f6(a1,f5(x5891,x5892)),x5891),f4(a1,x5893))),
% 118.67/118.80 inference(scs_inference,[],[95,431,429,433,28,32,29])).
% 118.67/118.80 cnf(591,plain,
% 118.67/118.80 (P6(f4(a1,x5911),f16(f6(a1,f5(x5912,x5913)),x5912))),
% 118.67/118.80 inference(scs_inference,[],[95,431,429,433,437,28,32,29,31])).
% 118.67/118.80 cnf(598,plain,
% 118.67/118.80 (P6(f4(a1,x5981),f17(f17(f8(a1),f7(a1)),x5982))),
% 118.67/118.80 inference(scs_inference,[],[95,589,422,63,31])).
% 118.67/118.80 cnf(600,plain,
% 118.67/118.80 (P6(f4(a1,x6001),f8(f13(f4(a1,x6002),x6003)))),
% 118.67/118.80 inference(scs_inference,[],[95,399,31])).
% 118.67/118.80 cnf(604,plain,
% 118.67/118.80 (P8(f6(f16(f6(f6(x6041,f5(a3,a3)),f5(x6042,x6043)),x6042),f5(x6044,x6045)),a3,a3)),
% 118.67/118.80 inference(scs_inference,[],[423,241,83,34])).
% 118.67/118.80 cnf(615,plain,
% 118.67/118.80 (~E(f6(x6151,f5(x6152,x6153)),f16(f6(a1,f5(x6154,x6155)),x6154))),
% 118.67/118.80 inference(scs_inference,[],[112,49,3])).
% 118.67/118.80 cnf(628,plain,
% 118.67/118.80 (P8(f6(x6281,f5(a3,a3)),a3,f15(f6(x6282,f5(x6283,a3)),x6283))),
% 118.67/118.80 inference(scs_inference,[],[142,423,36])).
% 118.67/118.80 cnf(629,plain,
% 118.67/118.80 (E(x6291,f15(f6(x6292,f5(x6293,x6291)),x6293))),
% 118.67/118.80 inference(rename_variables,[],[142])).
% 118.67/118.80 cnf(630,plain,
% 118.67/118.80 (P8(f6(x6301,f5(a3,a3)),f15(f6(x6302,f5(x6303,a3)),x6303),a3)),
% 118.67/118.80 inference(scs_inference,[],[142,629,423,36,35])).
% 118.67/118.80 cnf(664,plain,
% 118.67/118.80 (P4(f6(f6(x6641,f5(a2,x6642)),f5(x6643,x6644)),f16(f6(a2,f5(x6645,x6646)),x6645))),
% 118.67/118.80 inference(scs_inference,[],[224,578,39])).
% 118.67/118.80 cnf(680,plain,
% 118.67/118.80 (P4(f6(x6801,f5(x6802,x6803)),f16(f6(x6802,f5(x6804,x6805)),x6804))),
% 118.67/118.80 inference(scs_inference,[],[241,94,39])).
% 118.67/118.80 cnf(686,plain,
% 118.67/118.80 (P4(f6(x6861,f5(a2,x6862)),f16(f6(f7(f19(x6863,a1,x6864)),f5(x6865,x6866)),x6865))),
% 118.67/118.80 inference(scs_inference,[],[241,213,39])).
% 118.67/118.80 cnf(705,plain,
% 118.67/118.80 (P6(f8(f7(f19(x7051,a1,x7052))),f8(a2))),
% 118.67/118.80 inference(scs_inference,[],[404,46,47,28,32])).
% 118.67/118.80 cnf(733,plain,
% 118.67/118.80 (P1(f5(a2,x7331),f5(f7(f19(x7332,a1,x7333)),x7331))),
% 118.67/118.80 inference(scs_inference,[],[514,46,28])).
% 118.67/118.80 cnf(734,plain,
% 118.67/118.80 (P1(x7341,x7341)),
% 118.67/118.80 inference(rename_variables,[],[46])).
% 118.67/118.80 cnf(735,plain,
% 118.67/118.80 (P6(f5(f7(f19(x7351,a1,x7352)),x7353),f5(a2,x7353))),
% 118.67/118.80 inference(scs_inference,[],[514,46,47,28,32])).
% 118.67/118.80 cnf(737,plain,
% 118.67/118.80 (P1(f5(f7(f19(x7371,a1,x7372)),x7373),f5(a2,x7373))),
% 118.67/118.80 inference(scs_inference,[],[514,46,734,47,28,32,29])).
% 118.67/118.80 cnf(741,plain,
% 118.67/118.80 (~P9(f5(a2,x7411),f5(f7(f19(x7412,a1,x7413)),x7411))),
% 118.67/118.80 inference(scs_inference,[],[737,63])).
% 118.67/118.80 cnf(743,plain,
% 118.67/118.80 (E(f4(f5(a2,x7431),x7432),f4(f5(f7(f19(x7433,a1,x7434)),x7431),x7432))),
% 118.67/118.80 inference(scs_inference,[],[514,2,4])).
% 118.67/118.80 cnf(744,plain,
% 118.67/118.80 (~P9(f5(f7(f19(x7441,a1,x7442)),x7443),f5(a2,x7443))),
% 118.67/118.80 inference(scs_inference,[],[733,63])).
% 118.67/118.80 cnf(747,plain,
% 118.67/118.80 (E(f5(f5(f7(f19(x7471,a1,x7472)),x7473),x7474),f5(f5(a2,x7473),x7474))),
% 118.67/118.80 inference(scs_inference,[],[515,2,6])).
% 118.67/118.80 cnf(748,plain,
% 118.67/118.80 (E(f5(x7481,f7(f19(x7482,a1,x7483))),f5(x7481,a2))),
% 118.67/118.80 inference(scs_inference,[],[204,2,7])).
% 118.67/118.80 cnf(749,plain,
% 118.67/118.80 (E(f5(x7491,a2),f5(x7491,f7(f19(x7492,a1,x7493))))),
% 118.67/118.80 inference(scs_inference,[],[748,2])).
% 118.67/118.80 cnf(750,plain,
% 118.67/118.80 (E(f5(a2,a2),f5(f7(f19(x7501,a1,x7502)),f7(f19(x7503,a1,x7504))))),
% 118.67/118.80 inference(scs_inference,[],[515,748,2,3])).
% 118.67/118.80 cnf(836,plain,
% 118.67/118.80 (E(f4(f7(f19(x8361,a1,x8362)),x8363),f4(a2,x8363))),
% 118.67/118.80 inference(scs_inference,[],[204,2,4])).
% 118.67/118.80 cnf(864,plain,
% 118.67/118.80 (E(f4(x8641,f7(f19(x8642,a1,x8643))),f4(x8641,a2))),
% 118.67/118.80 inference(scs_inference,[],[204,2,5])).
% 118.67/118.80 cnf(865,plain,
% 118.67/118.80 (E(f4(x8651,a2),f4(x8651,f7(f19(x8652,a1,x8653))))),
% 118.67/118.80 inference(scs_inference,[],[864,2])).
% 118.67/118.80 cnf(910,plain,
% 118.67/118.80 (E(f5(x9101,f7(f19(x9102,a1,x9103))),f5(x9101,a2))),
% 118.67/118.80 inference(rename_variables,[],[748])).
% 118.67/118.80 cnf(913,plain,
% 118.67/118.80 (E(f5(x9131,f7(f19(x9132,a1,x9133))),f5(x9131,a2))),
% 118.67/118.80 inference(rename_variables,[],[748])).
% 118.67/118.80 cnf(914,plain,
% 118.67/118.80 (P1(f5(f7(f19(x9141,a1,x9142)),f7(f19(x9143,a1,x9144))),f5(a2,a2))),
% 118.67/118.80 inference(scs_inference,[],[748,910,913,737,733,735,28,32,29])).
% 118.67/118.80 cnf(925,plain,
% 118.67/118.80 (P1(f5(x9251,a2),f5(x9251,f7(f19(x9252,a1,x9253))))),
% 118.67/118.80 inference(scs_inference,[],[748,914,46,63,28])).
% 118.67/118.80 cnf(926,plain,
% 118.67/118.80 (P1(x9261,x9261)),
% 118.67/118.80 inference(rename_variables,[],[46])).
% 118.67/118.80 cnf(927,plain,
% 118.67/118.80 (P6(f5(x9271,f7(f19(x9272,a1,x9273))),f5(x9271,a2))),
% 118.67/118.80 inference(scs_inference,[],[748,914,46,47,63,28,32])).
% 118.67/118.80 cnf(929,plain,
% 118.67/118.80 (P1(f5(x9291,f7(f19(x9292,a1,x9293))),f5(x9291,a2))),
% 118.67/118.80 inference(scs_inference,[],[748,914,46,926,47,63,28,32,29])).
% 118.67/118.80 cnf(933,plain,
% 118.67/118.80 (~P9(f5(x9331,a2),f5(x9331,f7(f19(x9332,a1,x9333))))),
% 118.67/118.80 inference(scs_inference,[],[929,63])).
% 118.67/118.80 cnf(943,plain,
% 118.67/118.80 (P1(f4(a2,x9431),f4(f7(f19(x9432,a1,x9433)),x9431))),
% 118.67/118.80 inference(scs_inference,[],[836,46,28])).
% 118.67/118.80 cnf(944,plain,
% 118.67/118.80 (P1(x9441,x9441)),
% 118.67/118.80 inference(rename_variables,[],[46])).
% 118.67/118.80 cnf(945,plain,
% 118.67/118.80 (P6(f4(f7(f19(x9451,a1,x9452)),x9453),f4(a2,x9453))),
% 118.67/118.80 inference(scs_inference,[],[836,46,47,28,32])).
% 118.67/118.80 cnf(947,plain,
% 118.67/118.80 (P1(f4(f7(f19(x9471,a1,x9472)),x9473),f4(a2,x9473))),
% 118.67/118.80 inference(scs_inference,[],[836,46,944,47,28,32,29])).
% 118.67/118.80 cnf(955,plain,
% 118.67/118.80 (~P9(f4(f7(f19(x9551,a1,x9552)),x9553),f4(a2,x9553))),
% 118.67/118.80 inference(scs_inference,[],[943,63])).
% 118.67/118.80 cnf(958,plain,
% 118.67/118.80 (P1(f4(a2,a2),f4(f7(f19(x9581,a1,x9582)),f7(f19(x9583,a1,x9584))))),
% 118.67/118.80 inference(scs_inference,[],[864,943,28])).
% 118.67/118.80 cnf(960,plain,
% 118.67/118.80 (E(f4(x9601,f7(f19(x9602,a1,x9603))),f4(x9601,a2))),
% 118.67/118.80 inference(rename_variables,[],[864])).
% 118.67/118.80 cnf(963,plain,
% 118.67/118.80 (E(f4(x9631,f7(f19(x9632,a1,x9633))),f4(x9631,a2))),
% 118.67/118.80 inference(rename_variables,[],[864])).
% 118.67/118.80 cnf(964,plain,
% 118.67/118.80 (E(f4(f7(f19(x9641,a1,x9642)),f7(f19(x9643,a1,x9644))),f4(a2,a2))),
% 118.67/118.80 inference(scs_inference,[],[864,960,963,836,945,943,28,32,3])).
% 118.67/118.80 cnf(966,plain,
% 118.67/118.80 (E(f4(x9661,f7(f19(x9662,a1,x9663))),f4(x9661,a2))),
% 118.67/118.80 inference(rename_variables,[],[864])).
% 118.67/118.80 cnf(967,plain,
% 118.67/118.80 (P1(f4(f7(f19(x9671,a1,x9672)),f7(f19(x9673,a1,x9674))),f4(a2,a2))),
% 118.67/118.80 inference(scs_inference,[],[864,960,963,966,836,947,945,943,28,32,3,29])).
% 118.67/118.80 cnf(977,plain,
% 118.67/118.80 (E(f4(a2,a2),f4(f7(f19(x9771,a1,x9772)),f7(f19(x9773,a1,x9774))))),
% 118.67/118.80 inference(scs_inference,[],[967,964,63,2])).
% 118.67/118.80 cnf(978,plain,
% 118.67/118.80 (P1(f4(x9781,a2),f4(x9781,f7(f19(x9782,a1,x9783))))),
% 118.67/118.80 inference(scs_inference,[],[864,967,964,46,63,2,28])).
% 118.67/118.80 cnf(979,plain,
% 118.67/118.80 (P1(x9791,x9791)),
% 118.67/118.80 inference(rename_variables,[],[46])).
% 118.67/118.80 cnf(980,plain,
% 118.67/118.80 (P6(f4(x9801,f7(f19(x9802,a1,x9803))),f4(x9801,a2))),
% 118.67/118.80 inference(scs_inference,[],[864,967,964,46,47,63,2,28,32])).
% 118.67/118.80 cnf(981,plain,
% 118.67/118.80 (P6(x9811,x9811)),
% 118.67/118.80 inference(rename_variables,[],[47])).
% 118.67/118.80 cnf(982,plain,
% 118.67/118.80 (P1(f4(x9821,f7(f19(x9822,a1,x9823))),f4(x9821,a2))),
% 118.67/118.80 inference(scs_inference,[],[864,967,964,46,979,47,63,2,28,32,29])).
% 118.67/118.80 cnf(984,plain,
% 118.67/118.80 (P6(f4(x9841,a2),f4(x9841,f7(f19(x9842,a1,x9843))))),
% 118.67/118.80 inference(scs_inference,[],[864,967,964,46,979,47,981,63,2,28,32,29,31])).
% 118.67/118.80 cnf(999,plain,
% 118.67/118.80 (~P9(f4(x9991,f7(f19(x9992,a1,x9993))),f4(x9991,a2))),
% 118.67/118.80 inference(scs_inference,[],[978,63])).
% 118.67/118.80 cnf(1009,plain,
% 118.67/118.80 (E(f6(f7(f19(x10091,a1,x10092)),x10093),f6(a2,x10093))),
% 118.67/118.80 inference(scs_inference,[],[204,2,8])).
% 118.67/118.80 cnf(1010,plain,
% 118.67/118.80 (E(f6(a2,x10101),f6(f7(f19(x10102,a1,x10103)),x10101))),
% 118.67/118.80 inference(scs_inference,[],[1009,2])).
% 118.67/118.80 cnf(1026,plain,
% 118.67/118.80 (E(f6(x10261,f7(f19(x10262,a1,x10263))),f6(x10261,a2))),
% 118.67/118.80 inference(scs_inference,[],[204,2,9])).
% 118.67/118.80 cnf(1027,plain,
% 118.67/118.80 (E(f6(x10271,a2),f6(x10271,f7(f19(x10272,a1,x10273))))),
% 118.67/118.80 inference(scs_inference,[],[1026,2])).
% 118.67/118.80 cnf(1028,plain,
% 118.67/118.80 (E(f6(f7(f19(x10281,a1,x10282)),f7(f19(x10283,a1,x10284))),f6(a2,a2))),
% 118.67/118.80 inference(scs_inference,[],[1009,1026,2,3])).
% 118.67/118.80 cnf(1034,plain,
% 118.67/118.80 (E(f6(a2,a2),f6(f7(f19(x10341,a1,x10342)),f7(f19(x10343,a1,x10344))))),
% 118.67/118.80 inference(scs_inference,[],[1028,2])).
% 118.67/118.80 cnf(1081,plain,
% 118.67/118.80 (P1(f6(a2,x10811),f6(f7(f19(x10812,a1,x10813)),x10811))),
% 118.67/118.80 inference(scs_inference,[],[1009,46,28])).
% 118.67/118.80 cnf(1082,plain,
% 118.67/118.80 (P1(x10821,x10821)),
% 118.67/118.80 inference(rename_variables,[],[46])).
% 118.67/118.80 cnf(1083,plain,
% 118.67/118.80 (P6(f6(f7(f19(x10831,a1,x10832)),x10833),f6(a2,x10833))),
% 118.67/118.80 inference(scs_inference,[],[1009,46,47,28,32])).
% 118.67/118.80 cnf(1085,plain,
% 118.67/118.80 (P1(f6(f7(f19(x10851,a1,x10852)),x10853),f6(a2,x10853))),
% 118.67/118.80 inference(scs_inference,[],[1009,46,1082,47,28,32,29])).
% 118.67/118.80 cnf(1097,plain,
% 118.67/118.80 (P1(f6(a2,a2),f6(f7(f19(x10971,a1,x10972)),f7(f19(x10973,a1,x10974))))),
% 118.67/118.80 inference(scs_inference,[],[1026,1081,28])).
% 118.67/118.80 cnf(1099,plain,
% 118.67/118.80 (E(f6(x10991,f7(f19(x10992,a1,x10993))),f6(x10991,a2))),
% 118.67/118.80 inference(rename_variables,[],[1026])).
% 118.67/118.80 cnf(1100,plain,
% 118.67/118.80 (P6(f6(f7(f19(x11001,a1,x11002)),f7(f19(x11003,a1,x11004))),f6(a2,a2))),
% 118.67/118.80 inference(scs_inference,[],[1026,1099,1083,1081,28,32])).
% 118.67/118.80 cnf(1102,plain,
% 118.67/118.80 (E(f6(x11021,f7(f19(x11022,a1,x11023))),f6(x11021,a2))),
% 118.67/118.80 inference(rename_variables,[],[1026])).
% 118.67/118.80 cnf(1103,plain,
% 118.67/118.80 (P1(f6(f7(f19(x11031,a1,x11032)),f7(f19(x11033,a1,x11034))),f6(a2,a2))),
% 118.67/118.80 inference(scs_inference,[],[1026,1099,1102,1085,1083,1081,28,32,29])).
% 118.67/118.80 cnf(1114,plain,
% 118.67/118.80 (P1(f6(x11141,a2),f6(x11141,f7(f19(x11142,a1,x11143))))),
% 118.67/118.80 inference(scs_inference,[],[1026,1103,46,63,28])).
% 118.67/118.80 cnf(1115,plain,
% 118.67/118.80 (P1(x11151,x11151)),
% 118.67/118.80 inference(rename_variables,[],[46])).
% 118.67/118.80 cnf(1116,plain,
% 118.67/118.80 (P6(f6(x11161,f7(f19(x11162,a1,x11163))),f6(x11161,a2))),
% 118.67/118.80 inference(scs_inference,[],[1026,1103,46,47,63,28,32])).
% 118.67/118.80 cnf(1118,plain,
% 118.67/118.80 (P1(f6(x11181,f7(f19(x11182,a1,x11183))),f6(x11181,a2))),
% 118.67/118.80 inference(scs_inference,[],[1026,1103,46,1115,47,63,28,32,29])).
% 118.67/118.80 cnf(1126,plain,
% 118.67/118.80 (~P9(f6(x11261,f7(f19(x11262,a1,x11263))),f6(x11261,a2))),
% 118.67/118.80 inference(scs_inference,[],[1114,63])).
% 118.67/118.80 cnf(1132,plain,
% 118.67/118.80 (E(f19(f7(f19(x11321,a1,x11322)),x11323,x11324),f19(a2,x11323,x11324))),
% 118.67/118.80 inference(scs_inference,[],[204,2,10])).
% 118.67/118.80 cnf(1133,plain,
% 118.67/118.80 (E(f19(a2,x11331,x11332),f19(f7(f19(x11333,a1,x11334)),x11331,x11332))),
% 118.67/118.80 inference(scs_inference,[],[1132,2])).
% 118.67/118.80 cnf(1148,plain,
% 118.67/118.80 (P1(f19(a2,x11481,x11482),f19(f7(f19(x11483,a1,x11484)),x11481,x11482))),
% 118.67/118.80 inference(scs_inference,[],[1132,46,28])).
% 118.67/118.80 cnf(1149,plain,
% 118.67/118.80 (P1(x11491,x11491)),
% 118.67/118.80 inference(rename_variables,[],[46])).
% 118.67/118.80 cnf(1150,plain,
% 118.67/118.80 (P6(f19(f7(f19(x11501,a1,x11502)),x11503,x11504),f19(a2,x11503,x11504))),
% 118.67/118.80 inference(scs_inference,[],[1132,46,47,28,32])).
% 118.67/118.80 cnf(1151,plain,
% 118.67/118.80 (P6(x11511,x11511)),
% 118.67/118.80 inference(rename_variables,[],[47])).
% 118.67/118.80 cnf(1152,plain,
% 118.67/118.80 (E(f19(f7(f19(x11521,a1,x11522)),a1,a3),f8(f19(a2,a1,x11523)))),
% 118.67/118.80 inference(scs_inference,[],[1132,177,46,47,28,32,3])).
% 118.67/118.80 cnf(1154,plain,
% 118.67/118.80 (E(f19(f7(f19(x11541,a1,x11542)),x11543,x11544),f19(a2,x11543,x11544))),
% 118.67/118.80 inference(rename_variables,[],[1132])).
% 118.67/118.80 cnf(1155,plain,
% 118.67/118.80 (P1(f19(f7(f19(x11551,a1,x11552)),x11553,x11554),f19(a2,x11553,x11554))),
% 118.67/118.80 inference(scs_inference,[],[1132,1154,177,46,1149,47,28,32,3,29])).
% 118.67/118.80 cnf(1159,plain,
% 118.67/118.80 (E(f8(f19(a2,a1,x11591)),f19(f7(f19(x11592,a1,x11593)),a1,a3))),
% 118.67/118.80 inference(scs_inference,[],[1132,1154,177,46,1149,47,1151,28,32,3,29,31,2])).
% 118.67/118.80 cnf(1162,plain,
% 118.67/118.80 (~P9(f19(a2,x11621,x11622),f19(f7(f19(x11623,a1,x11624)),x11621,x11622))),
% 118.67/118.80 inference(scs_inference,[],[1155,63])).
% 118.67/118.80 cnf(1181,plain,
% 118.67/118.80 (~P9(f19(f7(f19(x11811,a1,x11812)),x11813,x11814),f19(a2,x11813,x11814))),
% 118.67/118.80 inference(scs_inference,[],[1148,63])).
% 118.67/118.80 cnf(1186,plain,
% 118.67/118.80 (E(f19(x11861,f7(f19(x11862,a1,x11863)),x11864),f19(x11861,a2,x11864))),
% 118.67/118.80 inference(scs_inference,[],[204,2,11])).
% 118.67/118.80 cnf(1187,plain,
% 118.67/118.80 (E(f19(x11871,a2,x11872),f19(x11871,f7(f19(x11873,a1,x11874)),x11872))),
% 118.67/118.80 inference(scs_inference,[],[1186,2])).
% 118.67/118.80 cnf(1188,plain,
% 118.67/118.80 (E(f19(a2,a2,x11881),f19(f7(f19(x11882,a1,x11883)),f7(f19(x11884,a1,x11885)),x11881))),
% 118.67/118.80 inference(scs_inference,[],[1133,1186,2,3])).
% 118.67/118.80 cnf(1194,plain,
% 118.67/118.80 (E(f19(f7(f19(x11941,a1,x11942)),f7(f19(x11943,a1,x11944)),x11945),f19(a2,a2,x11945))),
% 118.67/118.80 inference(scs_inference,[],[1188,2])).
% 118.67/118.80 cnf(1245,plain,
% 118.67/118.80 (P1(f19(a2,a2,x12451),f19(f7(f19(x12452,a1,x12453)),f7(f19(x12454,a1,x12455)),x12451))),
% 118.67/118.80 inference(scs_inference,[],[1186,1148,28])).
% 118.67/118.80 cnf(1247,plain,
% 118.67/118.80 (E(f19(x12471,f7(f19(x12472,a1,x12473)),x12474),f19(x12471,a2,x12474))),
% 118.67/118.80 inference(rename_variables,[],[1186])).
% 118.67/118.80 cnf(1248,plain,
% 118.67/118.80 (P6(f19(f7(f19(x12481,a1,x12482)),f7(f19(x12483,a1,x12484)),x12485),f19(a2,a2,x12485))),
% 118.67/118.80 inference(scs_inference,[],[1186,1247,1148,1150,28,32])).
% 118.67/118.80 cnf(1250,plain,
% 118.67/118.80 (E(f19(x12501,f7(f19(x12502,a1,x12503)),x12504),f19(x12501,a2,x12504))),
% 118.67/118.80 inference(rename_variables,[],[1186])).
% 118.67/118.80 cnf(1251,plain,
% 118.67/118.80 (P1(f19(f7(f19(x12511,a1,x12512)),f7(f19(x12513,a1,x12514)),x12515),f19(a2,a2,x12515))),
% 118.67/118.80 inference(scs_inference,[],[1186,1247,1250,1148,1155,1150,28,32,29])).
% 118.67/118.80 cnf(1262,plain,
% 118.67/118.80 (P1(f19(x12621,a2,x12622),f19(x12621,f7(f19(x12623,a1,x12624)),x12622))),
% 118.67/118.80 inference(scs_inference,[],[1186,1251,46,63,28])).
% 118.67/118.80 cnf(1263,plain,
% 118.67/118.80 (P1(x12631,x12631)),
% 118.67/118.80 inference(rename_variables,[],[46])).
% 118.67/118.80 cnf(1264,plain,
% 118.67/118.80 (P6(f19(x12641,f7(f19(x12642,a1,x12643)),x12644),f19(x12641,a2,x12644))),
% 118.67/118.80 inference(scs_inference,[],[1186,1251,46,47,63,28,32])).
% 118.67/118.80 cnf(1266,plain,
% 118.67/118.80 (P1(f19(x12661,f7(f19(x12662,a1,x12663)),x12664),f19(x12661,a2,x12664))),
% 118.67/118.80 inference(scs_inference,[],[1186,1251,46,1263,47,63,28,32,29])).
% 118.67/118.80 cnf(1271,plain,
% 118.67/118.80 (~P9(f19(x12711,a2,x12712),f19(x12711,f7(f19(x12713,a1,x12714)),x12712))),
% 118.67/118.80 inference(scs_inference,[],[1266,63])).
% 118.67/118.80 cnf(1274,plain,
% 118.67/118.80 (~P9(f19(x12741,f7(f19(x12742,a1,x12743)),x12744),f19(x12741,a2,x12744))),
% 118.67/118.80 inference(scs_inference,[],[1262,63])).
% 118.67/118.80 cnf(1281,plain,
% 118.67/118.80 (E(f19(x12811,x12812,f7(f19(x12813,a1,x12814))),f19(x12811,x12812,a2))),
% 118.67/118.80 inference(scs_inference,[],[204,2,12])).
% 118.67/118.80 cnf(1282,plain,
% 118.67/118.80 (E(f19(x12821,x12822,a2),f19(x12821,x12822,f7(f19(x12823,a1,x12824))))),
% 118.67/118.80 inference(scs_inference,[],[1281,2])).
% 118.67/118.80 cnf(1283,plain,
% 118.67/118.80 (E(f13(f19(x12831,x12832,a2),x12833),f19(f12(x12831,x12833),f6(x12832,f5(x12833,a2)),f7(f19(x12834,a1,x12835))))),
% 118.67/118.80 inference(scs_inference,[],[188,1281,2,3])).
% 118.67/118.80 cnf(1290,plain,
% 118.67/118.80 (E(f19(f12(x12901,x12902),f6(x12903,f5(x12902,a2)),f7(f19(x12904,a1,x12905))),f13(f19(x12901,x12903,a2),x12902))),
% 118.67/118.80 inference(scs_inference,[],[1283,2])).
% 118.67/118.80 cnf(1328,plain,
% 118.67/118.80 (E(f19(x13281,x13282,f7(f19(x13283,a1,x13284))),f19(x13281,x13282,a2))),
% 118.67/118.80 inference(rename_variables,[],[1281])).
% 118.67/118.80 cnf(1329,plain,
% 118.67/118.80 (P6(f19(f7(f19(x13291,a1,x13292)),x13293,f7(f19(x13294,a1,x13295))),f19(a2,x13293,a2))),
% 118.67/118.80 inference(scs_inference,[],[1281,1328,1148,1150,28,32])).
% 118.67/118.80 cnf(1331,plain,
% 118.67/118.80 (E(f19(x13311,x13312,f7(f19(x13313,a1,x13314))),f19(x13311,x13312,a2))),
% 118.67/118.80 inference(rename_variables,[],[1281])).
% 118.67/118.80 cnf(1332,plain,
% 118.67/118.80 (E(f19(f7(f19(x13321,a1,x13322)),f7(f19(x13323,a1,x13324)),f7(f19(x13325,a1,x13326))),f19(a2,a2,a2))),
% 118.67/118.80 inference(scs_inference,[],[1281,1328,1331,1194,1148,1150,28,32,3])).
% 118.67/118.80 cnf(1334,plain,
% 118.67/118.80 (E(f19(x13341,x13342,f7(f19(x13343,a1,x13344))),f19(x13341,x13342,a2))),
% 118.67/118.80 inference(rename_variables,[],[1281])).
% 118.67/118.80 cnf(1335,plain,
% 118.67/118.80 (P1(f19(f7(f19(x13351,a1,x13352)),x13353,f7(f19(x13354,a1,x13355))),f19(a2,x13353,a2))),
% 118.67/118.80 inference(scs_inference,[],[1281,1328,1331,1334,1194,1148,1155,1150,28,32,3,29])).
% 118.67/118.80 cnf(1347,plain,
% 118.67/118.80 (P1(f19(a2,a2,a2),f19(f7(f19(x13471,a1,x13472)),f7(f19(x13473,a1,x13474)),f7(f19(x13475,a1,x13476))))),
% 118.67/118.80 inference(scs_inference,[],[1281,1245,1332,1335,63,2,28])).
% 118.67/118.80 cnf(1349,plain,
% 118.67/118.80 (E(f19(x13491,x13492,f7(f19(x13493,a1,x13494))),f19(x13491,x13492,a2))),
% 118.67/118.80 inference(rename_variables,[],[1281])).
% 118.67/118.80 cnf(1350,plain,
% 118.67/118.80 (P6(f19(x13501,f7(f19(x13502,a1,x13503)),f7(f19(x13504,a1,x13505))),f19(x13501,a2,a2))),
% 118.67/118.80 inference(scs_inference,[],[1281,1349,1245,1264,1332,1335,63,2,28,32])).
% 118.67/118.80 cnf(1352,plain,
% 118.67/118.80 (E(f19(x13521,x13522,f7(f19(x13523,a1,x13524))),f19(x13521,x13522,a2))),
% 118.67/118.80 inference(rename_variables,[],[1281])).
% 118.67/118.80 cnf(1353,plain,
% 118.67/118.80 (E(f19(x13531,f7(f19(x13532,a1,x13533)),f7(f19(x13534,a1,x13535))),f19(x13531,a2,a2))),
% 118.67/118.80 inference(scs_inference,[],[1281,1349,1352,1186,1245,1264,1332,1335,63,2,28,32,3])).
% 118.67/118.80 cnf(1355,plain,
% 118.67/118.80 (E(f19(x13551,x13552,f7(f19(x13553,a1,x13554))),f19(x13551,x13552,a2))),
% 118.67/118.80 inference(rename_variables,[],[1281])).
% 118.67/118.80 cnf(1356,plain,
% 118.67/118.80 (P1(f19(x13561,f7(f19(x13562,a1,x13563)),f7(f19(x13564,a1,x13565))),f19(x13561,a2,a2))),
% 118.67/118.80 inference(scs_inference,[],[1281,1349,1352,1355,1186,1266,1245,1264,1332,1335,63,2,28,32,3,29])).
% 118.67/118.80 cnf(1370,plain,
% 118.67/118.80 (E(f19(x13701,a2,a2),f19(x13701,f7(f19(x13702,a1,x13703)),f7(f19(x13704,a1,x13705))))),
% 118.67/118.80 inference(scs_inference,[],[1347,1353,63,2])).
% 118.67/118.80 cnf(1373,plain,
% 118.67/118.80 (E(f19(x13731,x13732,f7(f19(x13733,a1,x13734))),f19(x13731,x13732,a2))),
% 118.67/118.80 inference(rename_variables,[],[1281])).
% 118.67/118.80 cnf(1374,plain,
% 118.67/118.80 (P6(f19(f7(f19(x13741,a1,x13742)),f7(f19(x13743,a1,x13744)),f7(f19(x13745,a1,x13746))),f19(a2,a2,a2))),
% 118.67/118.80 inference(scs_inference,[],[1281,1373,1262,1347,1248,1353,63,2,28,32])).
% 118.67/118.80 cnf(1376,plain,
% 118.67/118.80 (E(f19(x13761,x13762,f7(f19(x13763,a1,x13764))),f19(x13761,x13762,a2))),
% 118.67/118.80 inference(rename_variables,[],[1281])).
% 118.67/118.80 cnf(1377,plain,
% 118.67/118.80 (E(f19(f7(f19(x13771,a1,x13772)),x13773,f7(f19(x13774,a1,x13775))),f19(a2,x13773,a2))),
% 118.67/118.80 inference(scs_inference,[],[1281,1373,1376,1132,1262,1347,1248,1353,63,2,28,32,3])).
% 118.67/118.80 cnf(1396,plain,
% 118.67/118.81 (E(f19(a2,x13961,a2),f19(f7(f19(x13962,a1,x13963)),x13961,f7(f19(x13964,a1,x13965))))),
% 118.67/118.81 inference(scs_inference,[],[1356,1377,63,2])).
% 118.67/118.81 cnf(1397,plain,
% 118.67/118.81 (P1(f19(x13971,x13972,a2),f19(x13971,x13972,f7(f19(x13973,a1,x13974))))),
% 118.67/118.81 inference(scs_inference,[],[1281,1356,1377,46,63,2,28])).
% 118.67/118.81 cnf(1398,plain,
% 118.67/118.81 (P1(x13981,x13981)),
% 118.67/118.81 inference(rename_variables,[],[46])).
% 118.67/118.81 cnf(1399,plain,
% 118.67/118.81 (P6(f19(x13991,x13992,f7(f19(x13993,a1,x13994))),f19(x13991,x13992,a2))),
% 118.67/118.81 inference(scs_inference,[],[1281,1356,1377,46,47,63,2,28,32])).
% 118.67/118.81 cnf(1401,plain,
% 118.67/118.81 (P1(f19(x14011,x14012,f7(f19(x14013,a1,x14014))),f19(x14011,x14012,a2))),
% 118.67/118.81 inference(scs_inference,[],[1281,1356,1377,46,1398,47,63,2,28,32,29])).
% 118.67/118.81 cnf(1432,plain,
% 118.67/118.81 (~P9(f19(x14321,x14322,f7(f19(x14323,a1,x14324))),f19(x14321,x14322,a2))),
% 118.67/118.81 inference(scs_inference,[],[1397,63])).
% 118.67/118.81 cnf(1448,plain,
% 118.67/118.81 (~P9(f19(x14481,x14482,a2),f19(x14481,x14482,f7(f19(x14483,a1,x14484))))),
% 118.67/118.81 inference(scs_inference,[],[1401,63])).
% 118.67/118.81 cnf(1489,plain,
% 118.67/118.81 (P1(f19(f12(x14891,x14892),f6(x14893,f5(x14892,a2)),f7(f19(x14894,a1,x14895))),f13(f19(x14891,x14893,a2),x14892))),
% 118.67/118.81 inference(scs_inference,[],[1282,566,28])).
% 118.67/118.81 cnf(1491,plain,
% 118.67/118.81 (E(f19(x14911,x14912,a2),f19(x14911,x14912,f7(f19(x14913,a1,x14914))))),
% 118.67/118.81 inference(rename_variables,[],[1282])).
% 118.67/118.81 cnf(1494,plain,
% 118.67/118.81 (E(f19(x14941,x14942,a2),f19(x14941,x14942,f7(f19(x14943,a1,x14944))))),
% 118.67/118.81 inference(rename_variables,[],[1282])).
% 118.67/118.81 cnf(1495,plain,
% 118.67/118.81 (P1(f13(f19(x14951,x14952,a2),x14953),f19(f12(x14951,x14953),f6(x14952,f5(x14953,a2)),f7(f19(x14954,a1,x14955))))),
% 118.67/118.81 inference(scs_inference,[],[1282,1491,1494,566,562,568,28,32,29])).
% 118.67/118.81 cnf(1497,plain,
% 118.67/118.81 (E(f19(x14971,x14972,a2),f19(x14971,x14972,f7(f19(x14973,a1,x14974))))),
% 118.67/118.81 inference(rename_variables,[],[1282])).
% 118.67/118.81 cnf(1498,plain,
% 118.67/118.81 (P6(f19(f12(x14981,x14982),f6(x14983,f5(x14982,a2)),f7(f19(x14984,a1,x14985))),f13(f19(x14981,x14983,a2),x14982))),
% 118.67/118.81 inference(scs_inference,[],[1282,1491,1494,1497,566,562,564,568,28,32,29,31])).
% 118.67/118.81 cnf(1546,plain,
% 118.67/118.81 (P4(f6(f6(x15461,f5(a2,x15462)),f5(x15463,x15464)),a2)),
% 118.67/118.81 inference(scs_inference,[],[49,664,39])).
% 118.67/118.81 cnf(1704,plain,
% 118.67/118.81 (E(f4(f4(x17041,f7(f19(x17042,a1,x17043))),x17044),f4(f4(x17041,a2),x17044))),
% 118.67/118.81 inference(scs_inference,[],[865,2,4])).
% 118.67/118.81 cnf(1705,plain,
% 118.67/118.81 (E(f16(f7(f19(x17051,a1,x17052)),x17053),f16(a2,x17053))),
% 118.67/118.81 inference(scs_inference,[],[204,2,14])).
% 118.67/118.81 cnf(1706,plain,
% 118.67/118.81 (E(f16(a2,x17061),f16(f7(f19(x17062,a1,x17063)),x17061))),
% 118.67/118.81 inference(scs_inference,[],[1705,2])).
% 118.67/118.81 cnf(1733,plain,
% 118.67/118.81 (~P4(f16(f6(f4(a1,x17331),f5(x17332,x17333)),x17332),x17334)),
% 118.67/118.81 inference(scs_inference,[],[513,76])).
% 118.67/118.81 cnf(1737,plain,
% 118.67/118.81 (E(x17371,f16(f6(x17371,f5(x17372,x17373)),x17372))),
% 118.67/118.81 inference(rename_variables,[],[241])).
% 118.67/118.81 cnf(1738,plain,
% 118.67/118.81 (P8(f6(x17381,f5(a3,a3)),f16(f6(f16(f6(a3,f5(x17382,x17383)),x17382),f5(x17384,x17385)),x17384),a3)),
% 118.67/118.81 inference(scs_inference,[],[241,1737,424,747,513,76,2,36,35])).
% 118.67/118.81 cnf(1739,plain,
% 118.67/118.81 (E(x17391,f16(f6(x17391,f5(x17392,x17393)),x17392))),
% 118.67/118.81 inference(rename_variables,[],[241])).
% 118.67/118.81 cnf(1743,plain,
% 118.67/118.81 (P4(f6(x17431,f5(f4(a1,x17432),x17433)),f16(f6(f4(a1,x17434),f5(x17435,x17436)),x17435))),
% 118.67/118.81 inference(scs_inference,[],[914,156,431,241,1737,424,747,128,513,76,2,36,35,65,39])).
% 118.67/118.81 cnf(1745,plain,
% 118.67/118.81 (P1(f16(f6(f4(a1,x17451),f5(x17452,x17453)),x17452),f15(f6(x17454,f5(x17455,a1)),x17455))),
% 118.67/118.81 inference(scs_inference,[],[914,156,157,431,241,1737,424,747,128,513,76,2,36,35,65,39,28])).
% 118.67/118.81 cnf(1754,plain,
% 118.67/118.81 (P2(f16(f6(f16(f6(f6(x17541,f5(x17542,x17543)),f5(x17544,x17545)),x17544),f5(x17546,x17547)),x17546))),
% 118.67/118.81 inference(scs_inference,[],[914,212,405,404,515,156,157,431,241,1737,1739,424,395,147,747,248,128,513,76,2,36,35,65,39,28,32,3,29,31,33])).
% 118.67/118.81 cnf(1768,plain,
% 118.67/118.81 (E(x17681,f16(f6(x17681,f5(x17682,x17683)),x17682))),
% 118.67/118.81 inference(rename_variables,[],[241])).
% 118.67/118.81 cnf(1774,plain,
% 118.67/118.81 (E(a3,f16(f6(f16(f6(a3,f5(x17741,x17742)),x17741),f5(x17743,x17744)),x17743))),
% 118.67/118.81 inference(scs_inference,[],[914,241,1768,426,925,628,1745,1704,1738,58,63,2,36,65,35,86])).
% 118.67/118.81 cnf(1793,plain,
% 118.67/118.81 (P6(f8(f7(f19(x17931,a1,x17932))),f8(f8(a2)))),
% 118.67/118.81 inference(scs_inference,[],[705,62])).
% 118.67/118.81 cnf(1795,plain,
% 118.67/118.81 (P6(f8(f7(f19(x17951,a1,x17952))),f13(f8(a2),x17953))),
% 118.67/118.81 inference(scs_inference,[],[705,62,66])).
% 118.67/118.81 cnf(1797,plain,
% 118.67/118.81 (P6(f8(f7(f19(x17971,a1,x17972))),f17(f8(a2),x17973))),
% 118.67/118.81 inference(scs_inference,[],[705,62,66,67])).
% 118.67/118.81 cnf(1799,plain,
% 118.67/118.81 (~P5(f19(x17991,a1,x17992),x17993)),
% 118.67/118.81 inference(scs_inference,[],[705,57,62,66,67,82])).
% 118.67/118.81 cnf(1808,plain,
% 118.67/118.81 (E(f4(f15(f6(x18081,f5(x18082,a1)),x18082),x18083),f4(f4(a1,x18084),x18083))),
% 118.67/118.81 inference(scs_inference,[],[705,1774,1743,374,57,62,66,67,82,13,16,23,69,72,4])).
% 118.67/118.81 cnf(1812,plain,
% 118.67/118.81 (E(f6(f15(f6(x18121,f5(x18122,a1)),x18122),x18123),f6(f4(a1,x18124),x18123))),
% 118.67/118.81 inference(scs_inference,[],[705,1774,1743,374,57,62,66,67,82,13,16,23,69,72,4,5,6,7,8])).
% 118.67/118.81 cnf(1828,plain,
% 118.67/118.81 (P8(f6(f6(x18281,f5(a3,a3)),f5(x18282,x18283)),f15(f6(x18284,f5(x18285,a3)),x18285),a3)),
% 118.67/118.81 inference(scs_inference,[],[705,1774,1743,630,374,57,62,66,67,82,13,16,23,69,72,4,5,6,7,8,9,14,15,17,18,19,20,21,22,24,25,26,27,68,83])).
% 118.67/118.81 cnf(1835,plain,
% 118.67/118.81 (E(f17(f19(x18351,a1,x18352),x18353),f19(x18351,a1,a3))),
% 118.67/118.81 inference(scs_inference,[],[705,1774,1743,630,374,112,57,62,66,67,82,13,16,23,69,72,4,5,6,7,8,9,14,15,17,18,19,20,21,22,24,25,26,27,68,83,10,11,12,73,81])).
% 118.67/118.81 cnf(1837,plain,
% 118.67/118.81 (E(f6(f4(x18371,a2),f5(x18372,x18373)),f4(f6(x18371,f5(x18372,x18373)),a2))),
% 118.67/118.81 inference(scs_inference,[],[705,1774,1743,630,374,112,45,57,62,66,67,82,13,16,23,69,72,4,5,6,7,8,9,14,15,17,18,19,20,21,22,24,25,26,27,68,83,10,11,12,73,81,78])).
% 118.67/118.81 cnf(1841,plain,
% 118.67/118.81 (~E(f16(f6(f4(a1,x18411),f5(x18412,x18413)),x18412),f6(x18414,f5(x18415,x18416)))),
% 118.67/118.81 inference(scs_inference,[],[705,131,1774,1743,630,680,374,112,45,57,62,66,67,82,13,16,23,69,72,4,5,6,7,8,9,14,15,17,18,19,20,21,22,24,25,26,27,68,83,10,11,12,73,81,78,76,2])).
% 118.67/118.81 cnf(1844,plain,
% 118.67/118.81 (~P9(f8(f19(f7(f19(x18441,a1,x18442)),a1,x18443)),f8(f19(a2,a1,x18444)))),
% 118.67/118.81 inference(scs_inference,[],[266,294,705,131,1774,1743,630,680,1159,374,112,45,57,62,66,67,82,13,16,23,69,72,4,5,6,7,8,9,14,15,17,18,19,20,21,22,24,25,26,27,68,83,10,11,12,73,81,78,76,2,40,41])).
% 118.67/118.81 cnf(1846,plain,
% 118.67/118.81 (~P5(f8(f19(a2,a1,x18461)),x18462)),
% 118.67/118.81 inference(scs_inference,[],[266,294,705,131,1774,1743,630,680,1159,374,112,45,57,62,66,67,82,13,16,23,69,72,4,5,6,7,8,9,14,15,17,18,19,20,21,22,24,25,26,27,68,83,10,11,12,73,81,78,76,2,40,41,42])).
% 118.67/118.81 cnf(1847,plain,
% 118.67/118.81 (P8(f6(x18471,f5(f4(a1,x18472),f4(a1,x18472))),f4(a1,x18473),f4(a1,x18473))),
% 118.67/118.81 inference(scs_inference,[],[266,294,705,131,1774,1743,630,680,1159,374,112,45,136,57,62,66,67,82,13,16,23,69,72,4,5,6,7,8,9,14,15,17,18,19,20,21,22,24,25,26,27,68,83,10,11,12,73,81,78,76,2,40,41,42,75])).
% 118.67/118.81 cnf(1849,plain,
% 118.67/118.81 (P3(f19(x18491,f6(a1,f5(f4(a1,x18492),f4(a1,x18493))),x18494))),
% 118.67/118.81 inference(scs_inference,[],[266,294,705,131,1774,1743,630,680,1159,122,374,112,45,136,57,52,62,66,67,82,13,16,23,69,72,4,5,6,7,8,9,14,15,17,18,19,20,21,22,24,25,26,27,68,83,10,11,12,73,81,78,76,2,40,41,42,75,92])).
% 118.67/118.81 cnf(1851,plain,
% 118.67/118.81 (~P8(f15(f6(x18511,f5(x18512,a1)),x18512),x18513,x18514)),
% 118.67/118.81 inference(scs_inference,[],[266,294,705,131,1774,1743,630,680,1159,122,374,58,112,45,136,57,50,52,62,66,67,82,13,16,23,69,72,4,5,6,7,8,9,14,15,17,18,19,20,21,22,24,25,26,27,68,83,10,11,12,73,81,78,76,2,40,41,42,75,92,34])).
% 118.67/118.81 cnf(1853,plain,
% 118.67/118.81 (~P4(f16(f6(f16(f6(f4(a1,x18531),f5(x18532,x18533)),x18532),f5(x18534,x18535)),x18534),x18536)),
% 118.67/118.81 inference(scs_inference,[],[266,294,705,1733,131,1774,1743,630,680,1159,122,374,58,112,45,136,57,50,52,49,62,66,67,82,13,16,23,69,72,4,5,6,7,8,9,14,15,17,18,19,20,21,22,24,25,26,27,68,83,10,11,12,73,81,78,76,2,40,41,42,75,92,34,38])).
% 118.67/118.81 cnf(1859,plain,
% 118.67/118.81 (~P8(a1,x18591,x18592)),
% 118.67/118.81 inference(rename_variables,[],[58])).
% 118.67/118.81 cnf(1866,plain,
% 118.67/118.81 (~E(f16(f6(f16(f6(f6(x18661,f5(x18662,x18663)),f5(x18664,x18665)),x18664),f5(x18666,x18667)),x18666),f4(a1,x18668))),
% 118.67/118.81 inference(scs_inference,[],[266,294,705,1733,131,1774,1754,1743,630,958,680,1152,1159,111,982,122,374,58,1859,167,112,45,136,57,50,52,49,62,66,67,82,13,16,23,69,72,4,5,6,7,8,9,14,15,17,18,19,20,21,22,24,25,26,27,68,83,10,11,12,73,81,78,76,2,40,41,42,75,92,34,38,65,86,85,3,33])).
% 118.67/118.81 cnf(1867,plain,
% 118.67/118.81 (~E(f8(f19(a9,a10,a11)),f13(f19(x18671,x18672,a3),x18673))),
% 118.67/118.81 inference(scs_inference,[],[54,266,193,294,705,1733,131,1774,1754,1743,630,958,680,1152,1159,111,982,122,374,58,1859,167,112,45,136,57,50,52,49,62,66,67,82,13,16,23,69,72,4,5,6,7,8,9,14,15,17,18,19,20,21,22,24,25,26,27,68,83,10,11,12,73,81,78,76,2,40,41,42,75,92,34,38,65,86,85,3,33,37])).
% 118.67/118.81 cnf(1889,plain,
% 118.67/118.81 (P8(f6(f6(x18891,f5(f4(a1,x18892),f4(a1,x18892))),f5(x18893,x18894)),f4(a1,x18895),f4(a1,x18895))),
% 118.67/118.81 inference(scs_inference,[],[1847,600,587,68,67,66,83])).
% 118.67/118.81 cnf(1891,plain,
% 118.67/118.81 (P4(f6(f6(x18911,f5(a2,x18912)),f5(x18913,x18914)),f16(f6(f7(f19(x18915,a1,x18916)),f5(x18917,x18918)),x18917))),
% 118.67/118.81 inference(scs_inference,[],[1847,600,587,686,68,67,66,83,72])).
% 118.67/118.81 cnf(1893,plain,
% 118.67/118.81 (E(f13(f17(f19(x18931,a1,x18932),x18933),x18934),f13(f19(x18931,a1,a3),x18934))),
% 118.67/118.81 inference(scs_inference,[],[1835,1847,600,587,686,68,67,66,83,72,21])).
% 118.67/118.81 cnf(1894,plain,
% 118.67/118.81 (E(f6(x18941,f17(f19(x18942,a1,x18943),x18944)),f6(x18941,f19(x18942,a1,a3)))),
% 118.67/118.81 inference(scs_inference,[],[1835,1847,600,587,686,68,67,66,83,72,21,9])).
% 118.67/118.81 cnf(1895,plain,
% 118.67/118.81 (E(f18(f17(f19(x18951,a1,x18952),x18953),x18954),f18(f19(x18951,a1,a3),x18954))),
% 118.67/118.81 inference(scs_inference,[],[1835,1847,600,587,686,68,67,66,83,72,21,9,24])).
% 118.67/118.81 cnf(1897,plain,
% 118.67/118.81 (E(f8(f17(f19(x18971,a1,x18972),x18973)),f8(f19(x18971,a1,a3)))),
% 118.67/118.81 inference(scs_inference,[],[1835,1847,600,587,686,68,67,66,83,72,21,9,24,14,13])).
% 118.67/118.81 cnf(1898,plain,
% 118.67/118.81 (E(f18(x18981,f17(f19(x18982,a1,x18983),x18984)),f18(x18981,f19(x18982,a1,a3)))),
% 118.67/118.81 inference(scs_inference,[],[1835,1847,600,587,686,68,67,66,83,72,21,9,24,14,13,25])).
% 118.67/118.81 cnf(1900,plain,
% 118.67/118.81 (E(f6(f4(x19001,f4(a1,x19002)),f5(x19003,a1)),f4(f6(x19001,f5(x19003,a1)),f4(a1,x19002)))),
% 118.67/118.81 inference(scs_inference,[],[1835,1847,600,587,686,105,68,67,66,83,72,21,9,24,14,13,25,5,78])).
% 118.67/118.81 cnf(1902,plain,
% 118.67/118.81 (P4(f6(x19021,f5(f17(f19(x19022,a1,x19023),x19024),x19025)),f19(x19022,a1,a3))),
% 118.67/118.81 inference(scs_inference,[],[1835,1847,600,587,686,105,68,67,66,83,72,21,9,24,14,13,25,5,78,69])).
% 118.67/118.81 cnf(1904,plain,
% 118.67/118.81 (E(f19(x19041,f17(f19(x19042,a1,x19043),x19044),x19045),f19(x19041,f19(x19042,a1,a3),x19045))),
% 118.67/118.81 inference(scs_inference,[],[1835,1847,600,587,686,105,68,67,66,83,72,21,9,24,14,13,25,5,78,69,11])).
% 118.67/118.81 cnf(1905,plain,
% 118.67/118.81 (E(f4(f17(f19(x19051,a1,x19052),x19053),x19054),f4(f19(x19051,a1,a3),x19054))),
% 118.67/118.81 inference(scs_inference,[],[1835,1847,600,587,686,105,68,67,66,83,72,21,9,24,14,13,25,5,78,69,11,4])).
% 118.67/118.81 cnf(1907,plain,
% 118.67/118.81 (E(f6(f17(f19(x19071,a1,x19072),x19073),x19074),f6(f19(x19071,a1,a3),x19074))),
% 118.67/118.81 inference(scs_inference,[],[1835,1847,600,587,686,105,68,67,66,83,72,21,9,24,14,13,25,5,78,69,11,4,6,8])).
% 118.67/118.81 cnf(1910,plain,
% 118.67/118.81 (E(f15(x19101,f17(f19(x19102,a1,x19103),x19104)),f15(x19101,f19(x19102,a1,a3)))),
% 118.67/118.81 inference(scs_inference,[],[1835,1847,600,587,686,105,68,67,66,83,72,21,9,24,14,13,25,5,78,69,11,4,6,8,62,18])).
% 118.67/118.81 cnf(1911,plain,
% 118.67/118.81 (E(f19(x19111,x19112,f17(f19(x19113,a1,x19114),x19115)),f19(x19111,x19112,f19(x19113,a1,a3)))),
% 118.67/118.81 inference(scs_inference,[],[1835,1847,600,587,686,105,68,67,66,83,72,21,9,24,14,13,25,5,78,69,11,4,6,8,62,18,12])).
% 118.67/118.81 cnf(1913,plain,
% 118.67/118.81 (E(f5(x19131,f17(f19(x19132,a1,x19133),x19134)),f5(x19131,f19(x19132,a1,a3)))),
% 118.67/118.81 inference(scs_inference,[],[1835,1847,600,587,686,105,68,67,66,83,72,21,9,24,14,13,25,5,78,69,11,4,6,8,62,18,12,23,7])).
% 118.67/118.81 cnf(1916,plain,
% 118.67/118.81 (E(f17(f17(f19(x19161,a1,x19162),x19163),x19164),f17(f19(x19161,a1,a3),x19164))),
% 118.67/118.81 inference(scs_inference,[],[1835,1847,600,587,686,105,68,67,66,83,72,21,9,24,14,13,25,5,78,69,11,4,6,8,62,18,12,23,7,22,17,19])).
% 118.67/118.81 cnf(1920,plain,
% 118.67/118.81 (E(f19(f17(f19(x19201,a1,x19202),x19203),x19204,x19205),f19(f19(x19201,a1,a3),x19204,x19205))),
% 118.67/118.81 inference(scs_inference,[],[1835,1847,600,587,686,105,68,67,66,83,72,21,9,24,14,13,25,5,78,69,11,4,6,8,62,18,12,23,7,22,17,19,26,16,27,10])).
% 118.67/118.81 cnf(1921,plain,
% 118.67/118.81 (E(f16(x19211,f17(f19(x19212,a1,x19213),x19214)),f16(x19211,f19(x19212,a1,a3)))),
% 118.67/118.81 inference(scs_inference,[],[1835,1847,600,587,686,105,68,67,66,83,72,21,9,24,14,13,25,5,78,69,11,4,6,8,62,18,12,23,7,22,17,19,26,16,27,10,15])).
% 118.67/118.81 cnf(1930,plain,
% 118.67/118.81 (~P9(f19(f7(f19(x19301,a1,x19302)),a1,a3),f17(f19(a2,a1,x19303),x19304))),
% 118.67/118.81 inference(scs_inference,[],[1835,1867,1847,600,1844,1181,587,686,435,105,68,67,66,83,72,21,9,24,14,13,25,5,78,69,11,4,6,8,62,18,12,23,7,22,17,19,26,16,27,10,15,76,20,2,75,40,41])).
% 118.67/118.81 cnf(1931,plain,
% 118.67/118.81 (E(f17(f19(x19311,a1,x19312),x19313),f19(x19311,a1,a3))),
% 118.67/118.81 inference(rename_variables,[],[1835])).
% 118.67/118.81 cnf(1933,plain,
% 118.67/118.81 (~P5(f17(f19(x19331,a1,x19332),x19333),x19334)),
% 118.67/118.81 inference(scs_inference,[],[1799,1835,1931,1867,1847,600,1844,1181,587,686,435,105,68,67,66,83,72,21,9,24,14,13,25,5,78,69,11,4,6,8,62,18,12,23,7,22,17,19,26,16,27,10,15,76,20,2,75,40,41,42])).
% 118.67/118.81 cnf(1936,plain,
% 118.67/118.81 (~P4(f15(f6(x19361,f5(x19362,a1)),x19362),x19363)),
% 118.67/118.81 inference(scs_inference,[],[1799,1835,1931,1867,1847,600,1844,1181,587,686,435,105,57,50,68,67,66,83,72,21,9,24,14,13,25,5,78,69,11,4,6,8,62,18,12,23,7,22,17,19,26,16,27,10,15,76,20,2,75,40,41,42,38])).
% 118.67/118.81 cnf(1939,plain,
% 118.67/118.81 (~P8(a1,x19391,x19392)),
% 118.67/118.81 inference(rename_variables,[],[58])).
% 118.67/118.81 cnf(1944,plain,
% 118.67/118.81 (P1(f4(f4(a1,x19441),a2),f4(f15(f6(x19442,f5(x19443,a1)),x19443),f7(f19(x19444,a1,x19445))))),
% 118.67/118.81 inference(scs_inference,[],[1799,1835,1931,1867,1847,600,1808,1844,1181,587,686,978,435,58,1939,105,57,50,68,67,66,83,72,21,9,24,14,13,25,5,78,69,11,4,6,8,62,18,12,23,7,22,17,19,26,16,27,10,15,76,20,2,75,40,41,42,38,86,85,28])).
% 118.67/118.81 cnf(1947,plain,
% 118.67/118.81 (~E(f4(f6(x19471,f5(x19472,x19473)),a2),f16(f6(a1,f5(x19474,x19475)),x19474))),
% 118.67/118.81 inference(scs_inference,[],[1799,1835,1931,1867,1847,600,615,1837,1808,1844,1181,587,686,978,435,58,1939,105,57,50,68,67,66,83,72,21,9,24,14,13,25,5,78,69,11,4,6,8,62,18,12,23,7,22,17,19,26,16,27,10,15,76,20,2,75,40,41,42,38,86,85,28,3])).
% 118.67/118.81 cnf(1952,plain,
% 118.67/118.81 (~E(f16(f6(f6(x19521,f5(x19522,x19523)),f5(x19524,x19525)),x19524),f15(f6(x19526,f5(x19527,a1)),x19527))),
% 118.67/118.81 inference(scs_inference,[],[1799,1835,1931,1867,1847,375,600,615,1837,1808,1844,1181,587,743,980,686,978,248,435,58,1939,105,57,50,68,67,66,83,72,21,9,24,14,13,25,5,78,69,11,4,6,8,62,18,12,23,7,22,17,19,26,16,27,10,15,76,20,2,75,40,41,42,38,86,85,28,3,31,33])).
% 118.67/118.81 cnf(1953,plain,
% 118.67/118.81 (~E(f8(f19(a9,a10,a11)),f16(f6(f19(x19531,a1,a3),f5(x19532,x19533)),x19532))),
% 118.67/118.81 inference(scs_inference,[],[54,1799,1835,1931,1867,1847,375,439,600,615,1837,1808,1844,1181,587,743,980,686,978,248,435,58,1939,105,57,50,68,67,66,83,72,21,9,24,14,13,25,5,78,69,11,4,6,8,62,18,12,23,7,22,17,19,26,16,27,10,15,76,20,2,75,40,41,42,38,86,85,28,3,31,33,37])).
% 118.67/118.81 cnf(1954,plain,
% 118.67/118.81 (~P5(f19(x19541,f15(f6(x19542,f5(x19543,a1)),x19543),x19544),x19545)),
% 118.67/118.81 inference(scs_inference,[],[54,1799,1835,1931,1867,1847,375,439,600,615,1837,1808,1844,1181,587,743,980,686,978,248,435,58,1939,105,57,50,68,67,66,83,72,21,9,24,14,13,25,5,78,69,11,4,6,8,62,18,12,23,7,22,17,19,26,16,27,10,15,76,20,2,75,40,41,42,38,86,85,28,3,31,33,37,82])).
% 118.67/118.81 cnf(1967,plain,
% 118.67/118.81 (P8(f6(f6(f6(x19671,f5(f4(a1,x19672),f4(a1,x19672))),f5(x19673,x19674)),f5(x19675,x19676)),f4(a1,x19677),f4(a1,x19677))),
% 118.67/118.81 inference(scs_inference,[],[591,1889,1902,72,66,67,83])).
% 118.67/118.81 cnf(1973,plain,
% 118.67/118.81 (E(f19(x19731,f4(a1,x19732),x19733),f19(x19731,f15(f6(x19734,f5(x19735,a1)),x19735),x19733))),
% 118.67/118.81 inference(scs_inference,[],[591,1889,1902,1399,977,370,72,66,67,83,69,68,11])).
% 118.67/118.81 cnf(1978,plain,
% 118.67/118.81 (E(f6(f4(x19781,x19782),f5(x19783,x19782)),f4(f6(x19781,f5(x19783,x19782)),x19782))),
% 118.67/118.81 inference(scs_inference,[],[591,1889,1902,1399,977,370,46,72,66,67,83,69,68,11,25,4,62,78])).
% 118.67/118.81 cnf(1992,plain,
% 118.67/118.81 (E(f6(f4(a1,x19921),x19922),f6(f15(f6(x19923,f5(x19924,a1)),x19924),x19922))),
% 118.67/118.81 inference(scs_inference,[],[591,1889,1902,1399,249,977,370,46,72,66,67,83,69,68,11,25,4,62,78,13,5,23,9,14,22,24,21,76,17,16,8])).
% 118.67/118.81 cnf(2006,plain,
% 118.67/118.81 (E(f15(x20061,f17(f19(x20062,a1,x20063),x20064)),f15(x20061,f19(x20062,a1,a3)))),
% 118.67/118.81 inference(rename_variables,[],[1910])).
% 118.67/118.81 cnf(2009,plain,
% 118.67/118.81 (~P9(f19(f7(f19(x20091,a1,x20092)),a1,a3),f17(f17(f19(a2,a1,x20093),x20094),x20095))),
% 118.67/118.81 inference(scs_inference,[],[591,1889,1910,1916,1930,1953,1902,1851,1399,249,977,370,51,46,72,66,67,83,69,68,11,25,4,62,78,13,5,23,9,14,22,24,21,76,17,16,8,15,18,6,20,27,7,12,19,26,10,2,34,75,41])).
% 118.67/118.81 cnf(2011,plain,
% 118.67/118.81 (E(f17(f17(f19(x20111,a1,x20112),x20113),x20114),f17(f19(x20111,a1,a3),x20114))),
% 118.67/118.81 inference(rename_variables,[],[1916])).
% 118.67/118.81 cnf(2012,plain,
% 118.67/118.81 (~P9(f8(f17(f19(x20121,a1,x20122),x20123)),f8(f19(x20121,a1,x20124)))),
% 118.67/118.81 inference(scs_inference,[],[591,1889,1910,1916,1897,1930,1953,1902,280,1851,1399,249,977,370,51,46,72,66,67,83,69,68,11,25,4,62,78,13,5,23,9,14,22,24,21,76,17,16,8,15,18,6,20,27,7,12,19,26,10,2,34,75,41,40])).
% 118.67/118.81 cnf(2022,plain,
% 118.67/118.81 (~E(f8(f19(a9,a10,a11)),f16(f6(f8(f19(x20221,a1,x20222)),f5(x20223,x20224)),x20223))),
% 118.67/118.81 inference(scs_inference,[],[54,1933,1936,591,1889,1904,1911,1910,2006,1916,2011,1897,1930,132,1953,1902,280,1851,1399,249,977,370,51,46,72,66,67,83,69,68,11,25,4,62,78,13,5,23,9,14,22,24,21,76,17,16,8,15,18,6,20,27,7,12,19,26,10,2,34,75,41,40,42,38,3,37])).
% 118.67/118.81 cnf(2049,plain,
% 118.67/118.81 (E(f19(x20491,f6(a2,x20492),x20493),f19(x20491,f6(f7(f19(x20494,a1,x20495)),x20492),x20493))),
% 118.67/118.81 inference(scs_inference,[],[598,1967,1891,1116,1396,1010,67,66,69,83,72,62,68,9,14,13,11])).
% 118.67/118.81 cnf(2054,plain,
% 118.67/118.81 (P5(f19(x20541,f6(x20542,f5(a1,x20543)),x20544),f4(a1,x20545))),
% 118.67/118.81 inference(scs_inference,[],[598,1967,1891,1116,191,1396,1010,67,66,69,83,72,62,68,9,14,13,11,4,23,25,16,76])).
% 118.67/118.81 cnf(2073,plain,
% 118.67/118.81 (P3(f19(x20731,f6(f6(a1,f5(f4(a1,x20732),f4(a1,x20733))),f5(x20734,a2)),x20735))),
% 118.67/118.81 inference(scs_inference,[],[598,1967,2022,1891,1849,1116,191,1396,1010,45,67,66,69,83,72,62,68,9,14,13,11,4,23,25,16,76,5,15,21,18,24,27,22,19,8,7,17,6,10,26,20,12,2,92])).
% 118.67/118.81 cnf(2075,plain,
% 118.67/118.81 (P8(f6(x20751,f5(f4(a1,x20752),f4(a1,x20752))),a1,a1)),
% 118.67/118.81 inference(scs_inference,[],[598,1967,2022,1891,1849,1116,191,1396,1010,45,44,67,66,69,83,72,62,68,9,14,13,11,4,23,25,16,76,5,15,21,18,24,27,22,19,8,7,17,6,10,26,20,12,2,92,75])).
% 118.67/118.81 cnf(2077,plain,
% 118.67/118.81 (~P8(f16(f6(f4(a1,x20771),f5(x20772,x20773)),x20772),x20774,x20775)),
% 118.67/118.81 inference(scs_inference,[],[598,1967,2022,1891,1849,1116,191,1396,1010,45,58,101,44,67,66,69,83,72,62,68,9,14,13,11,4,23,25,16,76,5,15,21,18,24,27,22,19,8,7,17,6,10,26,20,12,2,92,75,34])).
% 118.67/118.81 cnf(2078,plain,
% 118.67/118.81 (~P9(f19(a2,a1,a3),f17(f17(f19(a2,a1,x20781),x20782),x20783))),
% 118.67/118.81 inference(scs_inference,[],[598,1967,2022,1891,2009,1849,1116,191,1396,1010,1133,45,58,101,44,67,66,69,83,72,62,68,9,14,13,11,4,23,25,16,76,5,15,21,18,24,27,22,19,8,7,17,6,10,26,20,12,2,92,75,34,40])).
% 118.67/118.81 cnf(2080,plain,
% 118.67/118.81 (~P9(f19(f19(x20801,a1,a3),f7(f19(x20802,a1,x20803)),x20804),f19(f17(f19(x20801,a1,x20805),x20806),a2,x20804))),
% 118.67/118.81 inference(scs_inference,[],[598,1920,1967,2022,1891,2009,1274,1849,1116,191,1396,1010,1133,45,58,101,44,67,66,69,83,72,62,68,9,14,13,11,4,23,25,16,76,5,15,21,18,24,27,22,19,8,7,17,6,10,26,20,12,2,92,75,34,40,41])).
% 118.67/118.81 cnf(2083,plain,
% 118.67/118.81 (~P5(f19(x20831,f4(a1,x20832),x20833),x20834)),
% 118.67/118.81 inference(scs_inference,[],[598,1920,1967,2022,1891,2009,1954,1973,1274,1849,1116,191,1396,1010,1133,45,58,101,44,67,66,69,83,72,62,68,9,14,13,11,4,23,25,16,76,5,15,21,18,24,27,22,19,8,7,17,6,10,26,20,12,2,92,75,34,40,41,42])).
% 118.67/118.81 cnf(2085,plain,
% 118.67/118.81 (~E(f16(f6(f8(f19(a9,a10,a11)),f5(x20851,x20852)),x20851),f13(f19(x20853,x20854,a3),x20855))),
% 118.67/118.81 inference(scs_inference,[],[598,1920,261,1967,2022,1891,2009,1954,1973,1274,1849,1116,191,193,1396,1010,1133,45,58,101,44,67,66,69,83,72,62,68,9,14,13,11,4,23,25,16,76,5,15,21,18,24,27,22,19,8,7,17,6,10,26,20,12,2,92,75,34,40,41,42,37])).
% 118.67/118.81 cnf(2088,plain,
% 118.67/118.81 (P6(f6(f7(f19(x20881,a1,x20882)),f7(f19(x20883,a1,x20884))),f13(f6(a2,a2),x20885))),
% 118.67/118.81 inference(scs_inference,[],[1100,66])).
% 118.67/118.81 cnf(2092,plain,
% 118.67/118.81 (P6(f6(f7(f19(x20921,a1,x20922)),f7(f19(x20923,a1,x20924))),f17(f6(a2,a2),x20925))),
% 118.67/118.81 inference(scs_inference,[],[1100,229,66,69,67])).
% 118.67/118.81 cnf(2094,plain,
% 118.67/118.81 (P8(f6(f6(x20941,f5(f4(a1,x20942),f4(a1,x20942))),f5(x20943,x20944)),a1,a1)),
% 118.67/118.81 inference(scs_inference,[],[2075,1100,229,66,69,67,83])).
% 118.67/118.81 cnf(2096,plain,
% 118.67/118.81 (P4(f6(f6(f6(x20961,f5(a2,x20962)),f5(x20963,x20964)),f5(x20965,x20966)),a2)),
% 118.67/118.81 inference(scs_inference,[],[2075,1100,1546,229,66,69,67,83,72])).
% 118.67/118.81 cnf(2098,plain,
% 118.67/118.81 (P6(f6(f7(f19(x20981,a1,x20982)),f7(f19(x20983,a1,x20984))),f8(f6(a2,a2)))),
% 118.67/118.81 inference(scs_inference,[],[2075,1100,1546,229,66,69,67,83,72,62])).
% 118.67/118.81 cnf(2109,plain,
% 118.67/118.81 (E(f4(x21091,f7(f19(x21092,a1,x21093))),f4(x21091,f7(f19(x21094,a1,x21095))))),
% 118.67/118.81 inference(scs_inference,[],[2075,1100,927,1546,229,66,69,67,83,72,62,68,14,9,23,25,76,21,5])).
% 118.67/118.81 cnf(2112,plain,
% 118.67/118.81 (E(f19(x21121,f7(f19(x21122,a1,x21123)),x21124),f19(x21121,f7(f19(x21125,a1,x21126)),x21124))),
% 118.67/118.81 inference(scs_inference,[],[2075,1100,927,1546,229,1706,66,69,67,83,72,62,68,14,9,23,25,76,21,5,16,13,11])).
% 118.67/118.81 cnf(2131,plain,
% 118.67/118.81 (~P9(f16(f6(f8(f19(a2,a1,x21311)),f5(x21312,x21313)),x21312),f17(f17(f19(a2,a1,x21314),x21315),x21316))),
% 118.67/118.81 inference(scs_inference,[],[2078,2075,1100,2085,927,1546,229,1706,455,53,66,69,67,83,72,62,68,14,9,23,25,76,21,5,16,13,11,18,4,27,8,7,26,15,19,20,24,22,12,17,10,6,2,75,40])).
% 118.67/118.81 cnf(2135,plain,
% 118.67/118.81 (~P5(f16(f6(f8(f19(a2,a1,x21351)),f5(x21352,x21353)),x21352),x21354)),
% 118.67/118.81 inference(scs_inference,[],[2078,2075,1100,2012,2085,1846,927,1546,491,229,1706,455,53,66,69,67,83,72,62,68,14,9,23,25,76,21,5,16,13,11,18,4,27,8,7,26,15,19,20,24,22,12,17,10,6,2,75,40,41,42])).
% 118.67/118.81 cnf(2138,plain,
% 118.67/118.81 (~E(f8(f19(a9,a10,a11)),f19(x21381,x21382,a3))),
% 118.67/118.81 inference(scs_inference,[],[54,2078,2075,1100,2012,2085,1846,927,1546,491,229,59,1706,455,53,66,69,67,83,72,62,68,14,9,23,25,76,21,5,16,13,11,18,4,27,8,7,26,15,19,20,24,22,12,17,10,6,2,75,40,41,42,37])).
% 118.67/118.81 cnf(2139,plain,
% 118.67/118.81 (P1(f6(a2,f7(f19(x21391,a1,x21392))),f6(f7(f19(x21393,a1,x21394)),f7(f19(x21395,a1,x21396))))),
% 118.67/118.81 inference(scs_inference,[],[54,2078,2075,1100,2012,2085,1846,927,1097,1546,491,1118,229,59,1706,455,53,66,69,67,83,72,62,68,14,9,23,25,76,21,5,16,13,11,18,4,27,8,7,26,15,19,20,24,22,12,17,10,6,2,75,40,41,42,37,65])).
% 118.67/118.81 cnf(2147,plain,
% 118.67/118.81 (~E(f16(f6(f6(x21471,f5(x21472,x21473)),f5(x21474,x21475)),x21474),f16(f6(f4(a1,x21476),f5(x21477,x21478)),x21477))),
% 118.67/118.81 inference(scs_inference,[],[54,2078,2075,1100,1905,2012,2085,1944,1846,124,927,984,1097,1546,491,1808,1118,229,59,1706,455,248,53,66,69,67,83,72,62,68,14,9,23,25,76,21,5,16,13,11,18,4,27,8,7,26,15,19,20,24,22,12,17,10,6,2,75,40,41,42,37,65,32,29,33])).
% 118.67/118.81 cnf(2154,plain,
% 118.67/118.81 (P6(f15(f6(x21541,f5(x21542,x21543)),x21542),f17(f8(x21543),f7(x21543)))),
% 118.67/118.81 inference(scs_inference,[],[1795,478,1188,69,67,66,68])).
% 118.67/118.81 cnf(2156,plain,
% 118.67/118.81 (P8(f6(f6(f6(x21561,f5(f4(a1,x21562),f4(a1,x21562))),f5(x21563,x21564)),f5(x21565,x21566)),a1,a1)),
% 118.67/118.81 inference(scs_inference,[],[1795,2094,478,1188,69,67,66,68,83])).
% 118.67/118.81 cnf(2158,plain,
% 118.67/118.81 (P4(f6(f6(f6(f6(x21581,f5(a2,x21582)),f5(x21583,x21584)),f5(x21585,x21586)),f5(x21587,x21588)),a2)),
% 118.67/118.81 inference(scs_inference,[],[2096,1795,2094,478,1188,69,67,66,68,83,72])).
% 118.67/118.81 cnf(2188,plain,
% 118.67/118.81 (~E(f19(x21881,x21882,a3),f8(f19(a9,a10,a11)))),
% 118.67/118.81 inference(scs_inference,[],[2138,2096,1795,2094,478,1188,1187,69,67,66,68,83,72,62,9,14,21,5,76,4,23,16,11,25,7,13,19,27,20,15,17,8,18,26,10,24,6,22,12,2])).
% 118.67/118.81 cnf(2189,plain,
% 118.67/118.81 (P8(f6(x21891,f5(a1,a1)),f4(a1,x21892),f4(a1,x21892))),
% 118.67/118.81 inference(scs_inference,[],[2138,2096,1795,2094,478,1188,1187,95,69,67,66,68,83,72,62,9,14,21,5,76,4,23,16,11,25,7,13,19,27,20,15,17,8,18,26,10,24,6,22,12,2,75])).
% 118.67/118.81 cnf(2191,plain,
% 118.67/118.81 (~P9(f8(f19(a2,a1,x21911)),f17(f17(f19(a2,a1,x21912),x21913),x21914))),
% 118.67/118.81 inference(scs_inference,[],[2138,2096,1795,2094,2131,478,497,1188,1187,95,69,67,66,68,83,72,62,9,14,21,5,76,4,23,16,11,25,7,13,19,27,20,15,17,8,18,26,10,24,6,22,12,2,75,40])).
% 118.67/118.81 cnf(2196,plain,
% 118.67/118.81 (~P9(f16(f6(f13(f19(x21961,a1,a3),x21962),f5(x21963,x21964)),x21963),f13(f17(f19(x21961,a1,x21965),x21966),x21962))),
% 118.67/118.81 inference(scs_inference,[],[2138,2096,1893,1795,2094,2135,2131,453,478,497,1921,1188,1187,95,69,67,66,68,83,72,62,9,14,21,5,76,4,23,16,11,25,7,13,19,27,20,15,17,8,18,26,10,24,6,22,12,2,75,40,42,41])).
% 118.67/118.81 cnf(2199,plain,
% 118.67/118.81 (~P8(f16(f6(f4(a1,x21991),f5(x21992,x21993)),x21992),x21994,x21995)),
% 118.67/118.81 inference(rename_variables,[],[2077])).
% 118.67/118.81 cnf(2204,plain,
% 118.67/118.81 (~E(f16(f6(f8(f19(a9,a10,a11)),f5(x22041,x22042)),x22041),f16(f6(f19(x22043,a1,a3),f5(x22044,x22045)),x22044))),
% 118.67/118.81 inference(scs_inference,[],[2138,2096,2077,2199,1893,1795,2094,2135,2131,453,478,497,439,1921,261,1188,1187,95,69,67,66,68,83,72,62,9,14,21,5,76,4,23,16,11,25,7,13,19,27,20,15,17,8,18,26,10,24,6,22,12,2,75,40,42,41,86,85,37])).
% 118.67/118.81 cnf(2207,plain,
% 118.67/118.81 (~P4(f6(a1,f5(f8(f19(a9,a10,a11)),x22071)),f19(x22072,x22073,a3))),
% 118.67/118.81 inference(scs_inference,[],[2138,2096,2077,2199,1893,1795,2094,2135,2080,2131,453,478,497,439,1921,261,1188,1187,57,95,69,67,66,68,83,72,62,9,14,21,5,76,4,23,16,11,25,7,13,19,27,20,15,17,8,18,26,10,24,6,22,12,2,75,40,42,41,86,85,37,64,77])).
% 118.67/118.81 cnf(2223,plain,
% 118.67/118.81 (P8(f6(f6(x22231,f5(a1,a1)),f5(x22232,x22233)),f4(a1,x22234),f4(a1,x22234))),
% 118.67/118.81 inference(scs_inference,[],[2189,2154,457,67,66,69,62,83])).
% 118.67/118.81 cnf(2225,plain,
% 118.67/118.81 (P6(f16(f6(f4(a1,x22251),f5(x22252,x22253)),x22252),f17(f8(a1),f7(a1)))),
% 118.67/118.81 inference(scs_inference,[],[2189,2154,178,457,67,66,69,62,83,68])).
% 118.67/118.81 cnf(2227,plain,
% 118.67/118.81 (P4(f6(f6(f6(f6(f6(x22271,f5(a2,x22272)),f5(x22273,x22274)),f5(x22275,x22276)),f5(x22277,x22278)),f5(x22279,x222710)),a2)),
% 118.67/118.81 inference(scs_inference,[],[2189,2154,2158,178,457,67,66,69,62,83,68,72])).
% 118.67/118.81 cnf(2231,plain,
% 118.67/118.81 (E(f4(f6(x22311,a2),x22312),f4(f6(x22311,f7(f19(x22313,a1,x22314))),x22312))),
% 118.67/118.81 inference(scs_inference,[],[2189,2154,2158,178,457,1027,67,66,69,62,83,68,72,14,9,4])).
% 118.67/118.81 cnf(2258,plain,
% 118.67/118.81 (~P9(f8(f17(f19(a2,a1,x22581),x22582)),f17(f17(f19(a2,a1,x22583),x22584),x22585))),
% 118.67/118.81 inference(scs_inference,[],[2189,2154,2158,2191,1866,178,1897,457,1027,121,67,66,69,62,83,68,72,14,9,4,23,76,13,21,25,16,5,11,20,19,8,18,17,27,7,6,15,22,26,12,10,24,2,75,40])).
% 118.67/118.81 cnf(2260,plain,
% 118.67/118.81 (E(f8(f17(f19(x22601,a1,x22602),x22603)),f8(f19(x22601,a1,a3)))),
% 118.67/118.81 inference(rename_variables,[],[1897])).
% 118.67/118.81 cnf(2261,plain,
% 118.67/118.81 (~P9(f19(x22611,f7(f19(x22612,a1,x22613)),f7(f19(x22614,a1,x22615))),f19(x22611,f7(f19(x22616,a1,x22617)),a2))),
% 118.67/118.81 inference(scs_inference,[],[2189,2154,2158,2191,2112,1866,1432,178,1897,457,1027,121,67,66,69,62,83,68,72,14,9,4,23,76,13,21,25,16,5,11,20,19,8,18,17,27,7,6,15,22,26,12,10,24,2,75,40,41])).
% 118.67/118.81 cnf(2267,plain,
% 118.67/118.81 (~P8(f6(f15(f6(x22671,f5(x22672,a1)),x22672),f5(f19(x22673,x22674,a3),x22675)),f8(f19(a9,a10,a11)),x22676)),
% 118.67/118.81 inference(scs_inference,[],[2189,2188,2154,2158,2191,2112,1866,1432,178,1897,2260,1846,1851,457,1027,121,67,66,69,62,83,68,72,14,9,4,23,76,13,21,25,16,5,11,20,19,8,18,17,27,7,6,15,22,26,12,10,24,2,75,40,41,42,86])).
% 118.67/118.81 cnf(2268,plain,
% 118.67/118.81 (~P8(f15(f6(x22681,f5(x22682,a1)),x22682),x22683,x22684)),
% 118.67/118.81 inference(rename_variables,[],[1851])).
% 118.67/118.81 cnf(2270,plain,
% 118.67/118.81 (~P8(f6(f15(f6(x22701,f5(x22702,a1)),x22702),f5(x22703,f19(x22704,x22705,a3))),x22706,f8(f19(a9,a10,a11)))),
% 118.67/118.81 inference(scs_inference,[],[2189,2188,2154,2158,2191,2112,1866,1432,178,1897,2260,1846,1851,2268,457,1027,121,67,66,69,62,83,68,72,14,9,4,23,76,13,21,25,16,5,11,20,19,8,18,17,27,7,6,15,22,26,12,10,24,2,75,40,41,42,86,85])).
% 118.67/118.81 cnf(2274,plain,
% 118.67/118.81 (E(f6(x22741,f17(f19(x22742,a1,x22743),x22744)),f6(x22741,f19(x22742,a1,a3)))),
% 118.67/118.81 inference(rename_variables,[],[1894])).
% 118.67/118.81 cnf(2276,plain,
% 118.67/118.81 (~E(f8(f19(a9,a10,a11)),f8(f19(x22761,a1,x22762)))),
% 118.67/118.81 inference(scs_inference,[],[54,2189,2188,2154,1894,1907,2158,2191,2112,1866,1432,178,1897,2260,1846,1851,2268,457,1027,98,121,67,66,69,62,83,68,72,14,9,4,23,76,13,21,25,16,5,11,20,19,8,18,17,27,7,6,15,22,26,12,10,24,2,75,40,41,42,86,85,3,37])).
% 118.67/118.81 cnf(2278,plain,
% 118.67/118.81 (~P4(f4(a1,x22781),x22782)),
% 118.67/118.81 inference(scs_inference,[],[54,2189,2188,2154,1894,2274,1907,2158,2191,2112,1866,1432,178,1897,2260,1846,1851,2268,457,1027,98,57,44,121,67,66,69,62,83,68,72,14,9,4,23,76,13,21,25,16,5,11,20,19,8,18,17,27,7,6,15,22,26,12,10,24,2,75,40,41,42,86,85,3,37,34,38])).
% 118.67/118.81 cnf(2281,plain,
% 118.67/118.81 (E(f17(f19(x22811,f4(a1,x22812),x22813),x22814),f19(x22811,f4(a1,x22812),a3))),
% 118.67/118.81 inference(scs_inference,[],[54,2189,2188,2154,1894,2274,1907,2158,2191,2207,2112,1866,1432,178,1897,2260,1846,1851,2268,457,1027,1159,98,57,44,121,67,66,69,62,83,68,72,14,9,4,23,76,13,21,25,16,5,11,20,19,8,18,17,27,7,6,15,22,26,12,10,24,2,75,40,41,42,86,85,3,37,34,38,39,81])).
% 118.67/118.81 cnf(2291,plain,
% 118.67/118.81 (P8(f6(f6(f6(x22911,f5(a1,a1)),f5(x22912,x22913)),f5(x22914,x22915)),f4(a1,x22916),f4(a1,x22916))),
% 118.67/118.81 inference(scs_inference,[],[2223,2225,1370,67,66,69,62,83])).
% 118.67/118.81 cnf(2323,plain,
% 118.67/118.81 (~E(f8(f19(x23231,a1,x23232)),f8(f19(a9,a10,a11)))),
% 118.67/118.81 inference(scs_inference,[],[2223,2276,2225,2227,246,1370,749,67,66,69,62,83,72,68,9,76,14,4,21,23,11,25,16,19,5,20,13,18,6,8,17,15,7,27,26,22,12,24,10,2])).
% 118.67/118.81 cnf(2324,plain,
% 118.67/118.81 (P8(f6(x23241,f5(f19(x23242,a1,a3),f19(x23242,a1,a3))),f8(f19(x23242,a1,x23243)),f8(f19(x23242,a1,x23243)))),
% 118.67/118.81 inference(scs_inference,[],[2223,2276,2225,2227,246,1370,749,177,67,66,69,62,83,72,68,9,76,14,4,21,23,11,25,16,19,5,20,13,18,6,8,17,15,7,27,26,22,12,24,10,2,75])).
% 118.67/118.81 cnf(2326,plain,
% 118.67/118.81 (~P8(f6(f4(a1,x23261),f5(f19(x23262,x23263,a3),x23264)),f8(f19(a9,a10,a11)),x23265)),
% 118.67/118.81 inference(scs_inference,[],[2223,2276,2225,2227,2267,1992,246,1370,749,177,67,66,69,62,83,72,68,9,76,14,4,21,23,11,25,16,19,5,20,13,18,6,8,17,15,7,27,26,22,12,24,10,2,75,34])).
% 118.67/118.81 cnf(2332,plain,
% 118.67/118.81 (~P9(f5(f7(f19(x23321,a1,x23322)),f19(x23323,a1,a3)),f5(a2,f17(f19(x23323,a1,x23324),x23325)))),
% 118.67/118.81 inference(scs_inference,[],[2223,2276,2225,1913,2227,2267,2261,744,1992,246,1396,1370,749,177,67,66,69,62,83,72,68,9,76,14,4,21,23,11,25,16,19,5,20,13,18,6,8,17,15,7,27,26,22,12,24,10,2,75,34,40,41])).
% 118.67/118.81 cnf(2341,plain,
% 118.67/118.81 (~E(f4(f6(x23411,f5(x23412,a1)),f4(a1,x23413)),f15(f6(x23414,f5(x23415,a1)),x23415))),
% 118.67/118.81 inference(scs_inference,[],[2278,2223,2276,2225,1913,1900,2281,2227,2267,2261,2083,744,1992,246,381,1396,1370,749,177,67,66,69,62,83,72,68,9,76,14,4,21,23,11,25,16,19,5,20,13,18,6,8,17,15,7,27,26,22,12,24,10,2,75,34,40,41,42,77,3])).
% 118.67/118.81 cnf(2343,plain,
% 118.67/118.81 (P3(f19(x23431,f6(f6(f6(a1,f5(f4(a1,x23432),f4(a1,x23433))),f5(x23434,a2)),f5(x23435,a2)),x23436))),
% 118.67/118.81 inference(scs_inference,[],[2278,2223,2276,2225,1913,1900,2281,2227,2267,2261,2083,744,2073,1992,246,381,1396,1370,749,45,177,67,66,69,62,83,72,68,9,76,14,4,21,23,11,25,16,19,5,20,13,18,6,8,17,15,7,27,26,22,12,24,10,2,75,34,40,41,42,77,3,92])).
% 118.67/118.81 cnf(2358,plain,
% 118.67/118.81 (P8(f6(f6(f6(f6(x23581,f5(a1,a1)),f5(x23582,x23583)),f5(x23584,x23585)),f5(x23586,x23587)),f4(a1,x23588),f4(a1,x23588))),
% 118.67/118.81 inference(scs_inference,[],[2291,1797,67,66,62,83])).
% 118.67/118.81 cnf(2364,plain,
% 118.67/118.81 (P4(f6(f6(x23641,f5(x23642,x23643)),f5(x23644,x23645)),f16(f6(x23642,f5(x23646,x23647)),x23646))),
% 118.67/118.81 inference(scs_inference,[],[2291,1797,1264,680,1034,67,66,62,83,69,68,72])).
% 118.67/118.81 cnf(2393,plain,
% 118.67/118.81 (P8(f6(x23931,f5(a2,a2)),f7(f19(x23932,a1,x23933)),f7(f19(x23932,a1,x23933)))),
% 118.67/118.81 inference(scs_inference,[],[2291,1797,2341,1264,680,128,1034,1705,204,67,66,62,83,69,68,72,76,9,14,21,4,11,25,5,23,16,20,13,19,6,7,18,8,27,15,17,22,12,26,10,24,2,75])).
% 118.67/118.81 cnf(2395,plain,
% 118.67/118.81 (P8(f4(f6(x23951,f5(f19(x23952,a1,a3),f19(x23952,a1,a3))),f19(x23952,a1,a3)),f8(f19(x23952,a1,x23953)),f8(f19(x23952,a1,x23953)))),
% 118.67/118.81 inference(scs_inference,[],[2291,1797,2324,2341,1978,1264,680,128,1034,1705,204,67,66,62,83,69,68,72,76,9,14,21,4,11,25,5,23,16,20,13,19,6,7,18,8,27,15,17,22,12,26,10,24,2,75,34])).
% 118.67/118.81 cnf(2401,plain,
% 118.67/118.81 (~P9(f4(f7(f19(x24011,a1,x24012)),f7(f19(x24013,a1,x24014))),f4(a2,f7(f19(x24015,a1,x24016))))),
% 118.67/118.81 inference(scs_inference,[],[2291,1797,2324,2341,2332,2109,955,1978,1913,1264,680,128,1034,1705,204,67,66,62,83,69,68,72,76,9,14,21,4,11,25,5,23,16,20,13,19,6,7,18,8,27,15,17,22,12,26,10,24,2,75,34,40,41])).
% 118.67/118.81 cnf(2410,plain,
% 118.67/118.81 (E(f18(f17(f19(x24101,a1,x24102),x24103),x24104),f18(f19(x24101,a1,a3),x24104))),
% 118.67/118.81 inference(rename_variables,[],[1895])).
% 118.67/118.81 cnf(2415,plain,
% 118.67/118.81 (P1(f6(f7(f19(x24151,a1,x24152)),f7(f19(x24153,a1,x24154))),f6(a2,f7(f19(x24155,a1,x24156))))),
% 118.67/118.81 inference(scs_inference,[],[2323,2291,1895,2410,1898,1797,2326,2324,2341,2332,2109,955,1978,2278,1913,1264,1103,1114,680,128,2188,1034,1705,49,204,67,66,62,83,69,68,72,76,9,14,21,4,11,25,5,23,16,20,13,19,6,7,18,8,27,15,17,22,12,26,10,24,2,75,34,40,41,77,86,3,35,42,65])).
% 118.67/118.81 cnf(2430,plain,
% 118.67/118.81 (P8(f6(f6(x24301,f5(a2,a2)),f5(x24302,x24303)),f7(f19(x24304,a1,x24305)),f7(f19(x24304,a1,x24305)))),
% 118.67/118.81 inference(scs_inference,[],[2393,1793,67,62,83])).
% 118.67/118.81 cnf(2436,plain,
% 118.67/118.81 (P4(f6(x24361,f5(f19(a2,x24362,x24363),x24364)),f19(f7(f19(x24365,a1,x24366)),x24362,x24363))),
% 118.67/118.81 inference(scs_inference,[],[2393,1793,2364,1133,67,62,83,66,72,69])).
% 118.67/118.81 cnf(2475,plain,
% 118.67/118.81 (~E(f16(f6(f16(f6(f6(x24751,f5(x24752,x24753)),f5(x24754,x24755)),x24754),f5(x24756,x24757)),x24756),a1)),
% 118.67/118.81 inference(scs_inference,[],[2393,1793,2364,2270,1952,2401,2231,999,1754,1992,980,56,1133,865,67,62,83,66,72,69,68,76,14,9,11,4,21,19,25,5,20,18,23,6,16,13,7,27,8,15,17,26,10,22,12,24,2,34,40,41,33])).
% 118.67/118.81 cnf(2478,plain,
% 118.67/118.81 (P1(f19(f12(x24781,x24782),f6(f7(f19(x24783,a1,x24784)),f5(x24782,a2)),f7(f19(x24785,a1,x24786))),f13(f19(x24781,a2,a2),x24782))),
% 118.67/118.81 inference(scs_inference,[],[2393,1793,2364,2258,2270,1952,2401,2231,999,2049,1754,1992,980,1489,56,1133,865,67,62,83,66,72,69,68,76,14,9,11,4,21,19,25,5,20,18,23,6,16,13,7,27,8,15,17,26,10,22,12,24,2,34,40,41,33,64,28])).
% 118.67/118.81 cnf(2485,plain,
% 118.67/118.81 (P8(f6(f6(f6(f6(f6(x24851,f5(a1,a1)),f5(x24852,x24853)),f5(x24854,x24855)),f5(x24856,x24857)),f5(x24858,x24859)),f4(a1,x248510),f4(a1,x248510))),
% 118.67/118.81 inference(scs_inference,[],[2358,2088,67,83])).
% 118.67/118.81 cnf(2538,plain,
% 118.67/118.81 (P8(f6(f6(f6(x25381,f5(a2,a2)),f5(x25382,x25383)),f5(x25384,x25385)),f7(f19(x25386,a1,x25387)),f7(f19(x25386,a1,x25387)))),
% 118.67/118.81 inference(scs_inference,[],[2430,2092,67,83])).
% 118.67/118.81 cnf(2550,plain,
% 118.67/118.81 (E(f6(x25501,f4(a1,x25502)),f6(x25501,f4(a1,x25503)))),
% 118.67/118.81 inference(scs_inference,[],[2430,2092,2436,735,136,750,67,83,66,62,69,68,72,9])).
% 118.67/118.81 cnf(2553,plain,
% 118.67/118.81 (E(f16(f4(a1,x25531),x25532),f16(f4(a1,x25533),x25532))),
% 118.67/118.81 inference(scs_inference,[],[2430,2092,2436,735,165,136,750,67,83,66,62,69,68,72,9,76,14])).
% 118.67/118.81 cnf(2554,plain,
% 118.67/118.81 (E(f13(f4(a1,x25541),x25542),f13(f4(a1,x25543),x25542))),
% 118.67/118.81 inference(scs_inference,[],[2430,2092,2436,735,165,136,750,67,83,66,62,69,68,72,9,76,14,21])).
% 118.67/118.81 cnf(2555,plain,
% 118.67/118.81 (E(f17(f4(a1,x25551),x25552),f17(f4(a1,x25553),x25552))),
% 118.67/118.81 inference(scs_inference,[],[2430,2092,2436,735,165,136,750,67,83,66,62,69,68,72,9,76,14,21,19])).
% 118.67/118.81 cnf(2557,plain,
% 118.67/118.81 (E(f5(f4(a1,x25571),x25572),f5(f4(a1,x25573),x25572))),
% 118.67/118.81 inference(scs_inference,[],[2430,2092,2436,735,165,136,750,67,83,66,62,69,68,72,9,76,14,21,19,4,6])).
% 118.67/118.81 cnf(2558,plain,
% 118.67/118.81 (E(f19(x25581,f4(a1,x25582),x25583),f19(x25581,f4(a1,x25584),x25583))),
% 118.67/118.81 inference(scs_inference,[],[2430,2092,2436,735,165,136,750,67,83,66,62,69,68,72,9,76,14,21,19,4,6,11])).
% 118.67/118.81 cnf(2559,plain,
% 118.67/118.81 (E(f18(x25591,f4(a1,x25592)),f18(x25591,f4(a1,x25593)))),
% 118.67/118.81 inference(scs_inference,[],[2430,2092,2436,735,165,136,750,67,83,66,62,69,68,72,9,76,14,21,19,4,6,11,25])).
% 118.67/118.81 cnf(2561,plain,
% 118.67/118.81 (E(f5(x25611,f4(a1,x25612)),f5(x25611,f4(a1,x25613)))),
% 118.67/118.81 inference(scs_inference,[],[2430,2092,2436,735,165,136,750,67,83,66,62,69,68,72,9,76,14,21,19,4,6,11,25,5,7])).
% 118.67/118.81 cnf(2563,plain,
% 118.67/118.81 (E(f15(x25631,f4(a1,x25632)),f15(x25631,f4(a1,x25633)))),
% 118.67/118.81 inference(scs_inference,[],[2430,2092,2436,735,165,136,750,67,83,66,62,69,68,72,9,76,14,21,19,4,6,11,25,5,7,16,18])).
% 118.67/118.81 cnf(2567,plain,
% 118.67/118.81 (E(f6(f4(a1,x25671),x25672),f6(f4(a1,x25673),x25672))),
% 118.67/118.81 inference(scs_inference,[],[2430,2092,2436,735,165,136,750,67,83,66,62,69,68,72,9,76,14,21,19,4,6,11,25,5,7,16,18,13,23,27,8])).
% 118.67/118.81 cnf(2570,plain,
% 118.67/118.81 (E(f19(f4(a1,x25701),x25702,x25703),f19(f4(a1,x25704),x25702,x25703))),
% 118.67/118.81 inference(scs_inference,[],[2430,2092,2436,735,165,136,750,67,83,66,62,69,68,72,9,76,14,21,19,4,6,11,25,5,7,16,18,13,23,27,8,20,17,10])).
% 118.67/118.81 cnf(2572,plain,
% 118.67/118.81 (E(f13(x25721,f4(a1,x25722)),f13(x25721,f4(a1,x25723)))),
% 118.67/118.81 inference(scs_inference,[],[2430,2092,2436,735,165,136,750,67,83,66,62,69,68,72,9,76,14,21,19,4,6,11,25,5,7,16,18,13,23,27,8,20,17,10,26,22])).
% 118.67/118.81 cnf(2573,plain,
% 118.67/118.81 (E(f16(x25731,f4(a1,x25732)),f16(x25731,f4(a1,x25733)))),
% 118.67/118.81 inference(scs_inference,[],[2430,2092,2436,735,165,136,750,67,83,66,62,69,68,72,9,76,14,21,19,4,6,11,25,5,7,16,18,13,23,27,8,20,17,10,26,22,15])).
% 118.67/118.81 cnf(2574,plain,
% 118.67/118.81 (E(f19(x25741,x25742,f4(a1,x25743)),f19(x25741,x25742,f4(a1,x25744)))),
% 118.67/118.81 inference(scs_inference,[],[2430,2092,2436,735,165,136,750,67,83,66,62,69,68,72,9,76,14,21,19,4,6,11,25,5,7,16,18,13,23,27,8,20,17,10,26,22,15,12])).
% 118.67/118.81 cnf(2594,plain,
% 118.67/118.81 (P4(f6(f6(x25941,f5(f19(x25942,a1,a3),x25943)),f5(x25944,x25945)),f8(f19(x25942,a1,x25946)))),
% 118.67/118.81 inference(scs_inference,[],[2558,2485,2098,1083,249,67,83,66,62,68,69,72])).
% 118.67/118.81 cnf(2625,plain,
% 118.67/118.81 (E(f16(x26251,f4(a1,x26252)),f16(x26251,f4(a1,x26253)))),
% 118.67/118.81 inference(rename_variables,[],[2573])).
% 118.67/118.81 cnf(2628,plain,
% 118.67/118.81 (E(f16(x26281,f4(a1,x26282)),f16(x26281,f4(a1,x26283)))),
% 118.67/118.81 inference(rename_variables,[],[2573])).
% 118.67/118.81 cnf(2631,plain,
% 118.67/118.81 (E(f16(x26311,f4(a1,x26312)),f16(x26311,f4(a1,x26313)))),
% 118.67/118.81 inference(rename_variables,[],[2573])).
% 118.67/118.81 cnf(2635,plain,
% 118.67/118.81 (~P9(f16(f6(f13(f19(x26351,a1,a3),f4(a1,x26352)),f5(x26353,x26354)),x26353),f13(f17(f19(x26351,a1,x26355),x26356),f4(a1,x26357)))),
% 118.67/118.81 inference(scs_inference,[],[2558,2563,2572,2573,2625,2628,2485,2098,2196,2475,210,1853,2135,1083,249,148,2077,67,83,66,62,68,69,72,9,76,14,21,5,25,4,19,7,6,16,11,13,27,8,20,18,23,26,10,17,22,12,15,24,2,38,42,34,40,41])).
% 118.67/118.81 cnf(2638,plain,
% 118.67/118.81 (~E(f16(f6(f4(a1,x26381),f5(f4(a1,x26382),x26383)),f4(a1,x26384)),f6(x26385,f5(x26386,x26387)))),
% 118.67/118.81 inference(scs_inference,[],[2558,2563,2572,2573,2625,2628,2631,1841,2485,2098,2196,2475,210,1853,2135,1083,249,148,2077,67,83,66,62,68,69,72,9,76,14,21,5,25,4,19,7,6,16,11,13,27,8,20,18,23,26,10,17,22,12,15,24,2,38,42,34,40,41,3])).
% 118.67/118.81 cnf(2640,plain,
% 118.67/118.81 (E(f16(x26401,f4(a1,x26402)),f16(x26401,f4(a1,x26403)))),
% 118.67/118.81 inference(rename_variables,[],[2573])).
% 118.67/118.81 cnf(2647,plain,
% 118.67/118.81 (P6(f19(f7(f19(x26471,a1,x26472)),f4(a1,x26473),f7(f19(x26474,a1,x26475))),f19(a2,f4(a1,x26476),a2))),
% 118.67/118.81 inference(scs_inference,[],[2558,2563,2572,2573,2625,2628,2631,2640,1841,2485,2098,2196,2415,2475,210,1853,2139,1329,518,2135,1083,249,148,2077,67,83,66,62,68,69,72,9,76,14,21,5,25,4,19,7,6,16,11,13,27,8,20,18,23,26,10,17,22,12,15,24,2,38,42,34,40,41,3,30,65,32])).
% 118.67/118.81 cnf(2657,plain,
% 118.67/118.81 (P8(f6(f6(f6(f6(x26571,f5(a2,a2)),f5(x26572,x26573)),f5(x26574,x26575)),f5(x26576,x26577)),f7(f19(x26578,a1,x26579)),f7(f19(x26578,a1,x26579)))),
% 118.67/118.81 inference(scs_inference,[],[2538,2647,67,66,83])).
% 118.67/118.81 cnf(2665,plain,
% 118.67/118.81 (P4(f6(f6(f6(x26651,f5(f19(x26652,a1,a3),x26653)),f5(x26654,x26655)),f5(x26656,x26657)),f8(f19(x26652,a1,x26658)))),
% 118.67/118.81 inference(scs_inference,[],[2570,2594,2538,2647,159,67,66,83,62,69,68,72])).
% 118.67/118.81 cnf(2677,plain,
% 118.67/118.81 (E(f19(x26771,f19(f4(a1,x26772),x26773,x26774),x26775),f19(x26771,f19(f4(a1,x26776),x26773,x26774),x26775))),
% 118.67/118.81 inference(scs_inference,[],[2570,2594,2538,2647,159,67,66,83,62,69,68,72,9,76,14,25,21,7,6,5,16,11])).
% 118.67/118.81 cnf(2688,plain,
% 118.67/118.81 (E(f19(f19(f4(a1,x26881),x26882,x26883),x26884,x26885),f19(f19(f4(a1,x26886),x26882,x26883),x26884,x26885))),
% 118.67/118.81 inference(scs_inference,[],[2570,2594,2538,2647,159,67,66,83,62,69,68,72,9,76,14,25,21,7,6,5,16,11,4,27,19,20,13,18,23,8,17,26,10])).
% 118.67/118.81 cnf(2695,plain,
% 118.67/118.81 (E(f15(x26951,f4(a1,x26952)),f15(x26951,f4(a1,x26953)))),
% 118.67/118.81 inference(rename_variables,[],[2563])).
% 118.67/118.81 cnf(2697,plain,
% 118.67/118.81 (P5(f13(f19(x26971,x26972,a2),a1),f4(a1,x26973))),
% 118.67/118.81 inference(scs_inference,[],[2570,2054,2638,2594,2538,2647,2563,1936,159,1290,67,66,83,62,69,68,72,9,76,14,25,21,7,6,5,16,11,4,27,19,20,13,18,23,8,17,26,10,22,15,12,24,2,38,42])).
% 118.67/118.81 cnf(2703,plain,
% 118.67/118.81 (~P9(f16(f6(f13(f19(x27031,a1,a3),f4(a1,x27032)),f5(f4(a1,x27033),x27034)),f4(a1,x27035)),f13(f17(f19(x27031,a1,x27036),x27037),f4(a1,x27038)))),
% 118.67/118.81 inference(scs_inference,[],[2570,2054,2638,2594,2538,2647,2635,2563,2695,2573,1936,159,1851,1290,67,66,83,62,69,68,72,9,76,14,25,21,7,6,5,16,11,4,27,19,20,13,18,23,8,17,26,10,22,15,12,24,2,38,42,34,40])).
% 118.67/118.81 cnf(2706,plain,
% 118.67/118.81 (~P9(f6(f4(a1,x27061),f7(f19(x27062,a1,x27063))),f6(f4(a1,x27064),a2))),
% 118.67/118.81 inference(scs_inference,[],[2570,2567,2054,2638,2594,2538,2647,2635,1126,2563,2695,2573,1936,159,1851,1290,67,66,83,62,69,68,72,9,76,14,25,21,7,6,5,16,11,4,27,19,20,13,18,23,8,17,26,10,22,15,12,24,2,38,42,34,40,41])).
% 118.67/118.81 cnf(2730,plain,
% 118.67/118.81 (P6(f16(f6(f7(f19(x27301,a1,x27302)),f5(x27303,x27304)),x27303),f17(f8(a2),f7(a2)))),
% 118.67/118.81 inference(scs_inference,[],[2156,1498,489,67,83,66,62,68])).
% 118.67/118.81 cnf(2741,plain,
% 118.67/118.81 (E(f19(x27411,f19(x27412,x27413,f4(a1,x27414)),x27415),f19(x27411,f19(x27412,x27413,f4(a1,x27416)),x27415))),
% 118.67/118.81 inference(scs_inference,[],[2156,2665,1498,2574,489,578,67,83,66,62,68,69,72,76,9,14,7,11])).
% 118.67/118.81 cnf(2754,plain,
% 118.67/118.81 (E(f19(f19(x27541,x27542,f4(a1,x27543)),x27544,x27545),f19(f19(x27541,x27542,f4(a1,x27546)),x27544,x27545))),
% 118.67/118.81 inference(scs_inference,[],[2156,2665,1498,2574,489,578,67,83,66,62,68,69,72,76,9,14,7,11,6,4,21,25,27,16,20,5,19,23,13,18,10])).
% 118.67/118.81 cnf(2766,plain,
% 118.67/118.81 (~P9(f19(a2,f19(f4(a1,x27661),x27662,x27663),x27664),f19(f7(f19(x27665,a1,x27666)),f19(f4(a1,x27667),x27662,x27663),x27664))),
% 118.67/118.81 inference(scs_inference,[],[2706,2156,2665,2677,1162,1498,2574,1812,1947,489,578,67,83,66,62,68,69,72,76,9,14,7,11,6,4,21,25,27,16,20,5,19,23,13,18,10,17,8,26,22,12,15,24,2,40,41])).
% 118.67/118.81 cnf(2777,plain,
% 118.67/118.81 (P8(f6(f6(f6(x27771,f5(a3,a3)),f5(x27772,x27773)),f5(x27774,x27775)),f15(f6(x27776,f5(x27777,a3)),x27777),a3)),
% 118.67/118.81 inference(scs_inference,[],[2730,1828,67,66,83])).
% 118.67/118.81 cnf(2785,plain,
% 118.67/118.81 (P4(f6(f6(x27851,f5(a1,x27852)),f5(x27853,x27854)),f4(a1,x27855))),
% 118.67/118.81 inference(scs_inference,[],[2730,1828,2550,147,191,67,66,83,62,69,68,72])).
% 118.67/118.81 cnf(2814,plain,
% 118.67/118.81 (~P9(f19(a2,f19(f4(a1,x28141),x28142,f4(a1,x28143)),x28144),f19(f7(f19(x28145,a1,x28146)),f19(f4(a1,x28147),x28142,f4(a1,x28148)),x28144))),
% 118.67/118.81 inference(scs_inference,[],[2730,1828,2741,2766,2550,615,147,191,213,67,66,83,62,69,68,72,76,9,14,6,27,11,4,16,7,20,25,21,19,5,23,18,13,17,10,26,8,22,15,12,24,2,40])).
% 118.67/118.81 cnf(2830,plain,
% 118.67/118.81 (P6(f7(f19(x28301,a1,x28302)),f17(f8(a2),f7(a2)))),
% 118.67/118.81 inference(scs_inference,[],[2657,2553,1374,393,67,62,66,69,83,68])).
% 118.67/118.81 cnf(2832,plain,
% 118.67/118.81 (P4(f6(f6(f6(x28321,f5(a1,x28322)),f5(x28323,x28324)),f5(x28325,x28326)),f4(a1,x28327))),
% 118.67/118.81 inference(scs_inference,[],[2785,2657,2553,1374,393,67,62,66,69,83,68,72])).
% 118.67/118.81 cnf(2863,plain,
% 118.67/118.81 (E(f19(f19(x28631,x28632,f4(a1,x28633)),x28634,x28635),f19(f19(x28631,x28632,f4(a1,x28636)),x28634,x28635))),
% 118.67/118.81 inference(rename_variables,[],[2754])).
% 118.67/118.81 cnf(2864,plain,
% 118.67/118.81 (~P9(f19(f19(x28641,x28642,f4(a1,x28643)),x28644,a2),f19(f19(x28641,x28642,f4(a1,x28645)),x28644,f7(f19(x28646,a1,x28647))))),
% 118.67/118.81 inference(scs_inference,[],[2785,2657,2754,2863,1271,1448,2553,1374,393,381,67,62,66,69,83,68,72,76,9,14,11,27,4,16,6,7,20,25,18,19,21,5,23,13,8,17,22,26,10,12,15,24,2,40,41])).
% 118.67/118.81 cnf(2866,plain,
% 118.67/118.81 (E(f19(f19(x28661,x28662,f4(a1,x28663)),x28664,x28665),f19(f19(x28661,x28662,f4(a1,x28666)),x28664,x28665))),
% 118.67/118.81 inference(rename_variables,[],[2754])).
% 118.67/118.81 cnf(2867,plain,
% 118.67/118.81 (P1(f13(f19(x28671,f7(f19(x28672,a1,x28673)),a2),x28674),f13(f19(x28671,a2,a2),x28674))),
% 118.67/118.81 inference(scs_inference,[],[2785,2478,2657,2754,2863,1271,1448,2553,1374,1495,393,381,67,62,66,69,83,68,72,76,9,14,11,27,4,16,6,7,20,25,18,19,21,5,23,13,8,17,22,26,10,12,15,24,2,40,41,65])).
% 118.67/118.81 cnf(2871,plain,
% 118.67/118.81 (~P8(f4(a1,x28711),x28712,x28713)),
% 118.67/118.81 inference(scs_inference,[],[2785,2478,2657,2754,2863,2866,1271,1448,2553,1374,1495,393,381,58,44,67,62,66,69,83,68,72,76,9,14,11,27,4,16,6,7,20,25,18,19,21,5,23,13,8,17,22,26,10,12,15,24,2,40,41,65,38,34])).
% 118.67/118.81 cnf(2879,plain,
% 118.67/118.81 (P6(f7(f19(x28791,a1,x28792)),f13(f17(f8(a2),f7(a2)),x28793))),
% 118.67/118.81 inference(scs_inference,[],[2830,1350,67,66])).
% 118.67/118.81 cnf(2881,plain,
% 118.67/118.81 (P6(f7(f19(x28811,a1,x28812)),f8(f17(f8(a2),f7(a2))))),
% 118.67/118.81 inference(scs_inference,[],[2830,1350,67,66,62])).
% 118.67/118.81 cnf(2887,plain,
% 118.67/118.81 (P6(f16(f6(x28871,f5(x28872,x28873)),x28872),f17(f8(x28871),f7(x28871)))),
% 118.67/118.81 inference(scs_inference,[],[2830,2395,2554,1350,433,67,66,62,83,69,68])).
% 118.67/118.81 cnf(2889,plain,
% 118.67/118.81 (P4(f6(f6(f6(f6(x28891,f5(a1,x28892)),f5(x28893,x28894)),f5(x28895,x28896)),f5(x28897,x28898)),f4(a1,x28899))),
% 118.67/118.81 inference(scs_inference,[],[2830,2832,2395,2554,1350,433,67,66,62,83,69,68,72])).
% 118.67/118.81 cnf(2897,plain,
% 118.67/118.81 (E(f5(x28971,f13(f4(a1,x28972),x28973)),f5(x28971,f13(f4(a1,x28974),x28973)))),
% 118.67/118.81 inference(scs_inference,[],[2830,2832,2395,2554,1350,433,67,66,62,83,69,68,72,76,9,14,27,4,7])).
% 118.67/118.81 cnf(2901,plain,
% 118.67/118.81 (E(f5(f13(f4(a1,x29011),x29012),x29013),f5(f13(f4(a1,x29014),x29012),x29013))),
% 118.67/118.81 inference(scs_inference,[],[2830,2832,2395,2554,1350,433,67,66,62,83,69,68,72,76,9,14,27,4,7,16,11,20,6])).
% 118.67/118.81 cnf(2917,plain,
% 118.67/118.81 (~E(f4(a1,x29171),f6(x29172,f5(x29173,x29174)))),
% 118.67/118.81 inference(scs_inference,[],[2830,2832,2395,2554,1350,167,433,67,66,62,83,69,68,72,76,9,14,27,4,7,16,11,20,6,5,18,19,25,13,21,23,8,17,26,22,10,12,15,24,2])).
% 118.67/118.81 cnf(2948,plain,
% 118.67/118.81 (P4(f6(f6(f6(f6(f6(x29481,f5(a1,x29482)),f5(x29483,x29484)),f5(x29485,x29486)),f5(x29487,x29488)),f5(x29489,x294810)),f4(a1,x294811))),
% 118.67/118.81 inference(scs_inference,[],[2889,2887,2777,2555,67,62,66,69,83,72])).
% 118.67/118.81 cnf(2950,plain,
% 118.67/118.81 (P6(f4(a1,x29501),f17(f8(a1),f7(a1)))),
% 118.67/118.81 inference(scs_inference,[],[2889,2887,2777,2555,109,67,62,66,69,83,72,68])).
% 118.67/118.81 cnf(2988,plain,
% 118.67/118.81 (~P8(f6(f4(a1,x29881),f5(f4(a1,x29882),x29883)),f6(x29884,f5(x29885,x29886)),x29887)),
% 118.67/118.81 inference(scs_inference,[],[2917,2889,2887,2897,2901,2777,741,933,2555,2871,1733,109,112,67,62,66,69,83,72,68,76,9,14,16,4,20,27,11,5,7,13,18,21,6,25,23,19,17,8,26,22,10,12,15,24,2,41,40,77,86])).
% 118.67/118.81 cnf(3002,plain,
% 118.67/118.81 (P6(f4(a1,x30021),f8(f17(f8(a1),f7(a1))))),
% 118.67/118.81 inference(scs_inference,[],[2950,2879,67,62])).
% 118.67/118.81 cnf(3004,plain,
% 118.67/118.81 (P6(f4(a1,x30041),f13(f17(f8(a1),f7(a1)),x30042))),
% 118.67/118.81 inference(scs_inference,[],[2950,2879,67,62,66])).
% 118.67/118.81 cnf(3006,plain,
% 118.67/118.81 (P8(f6(f6(x30061,f5(f19(x30062,a1,a3),f19(x30062,a1,a3))),f5(x30063,x30064)),f8(f19(x30062,a1,x30065)),f8(f19(x30062,a1,x30065)))),
% 118.67/118.81 inference(scs_inference,[],[2950,2879,2324,67,62,66,83])).
% 118.67/118.81 cnf(3014,plain,
% 118.67/118.81 (P5(f19(x30141,f6(f6(f6(f6(f6(x30142,f5(a1,x30143)),f5(x30144,x30145)),f5(x30146,x30147)),f5(x30148,x30149)),f5(x301410,x301411)),x301412),f4(a1,x301413))),
% 118.67/118.81 inference(scs_inference,[],[2950,2879,2948,2557,2324,1150,67,62,66,83,69,68,72,76])).
% 118.67/118.81 cnf(3040,plain,
% 118.67/118.81 (~P8(f6(f4(a1,x30401),f5(f4(a1,x30402),x30403)),f16(f6(f6(x30404,f5(x30405,x30406)),f5(x30407,x30408)),x30407),x30409)),
% 118.67/118.81 inference(scs_inference,[],[2950,2988,2879,2948,2557,2324,1150,49,67,62,66,83,69,68,72,76,9,14,7,16,20,5,11,13,25,4,27,6,19,21,18,17,23,8,10,26,22,12,24,15,35])).
% 118.67/118.81 cnf(3042,plain,
% 118.67/118.81 (~P9(f19(f19(f4(a1,x30421),x30422,f4(a1,x30423)),x30424,a2),f19(f19(f4(a1,x30425),x30422,f4(a1,x30426)),x30424,f7(f19(x30427,a1,x30428))))),
% 118.67/118.81 inference(scs_inference,[],[2950,2988,2879,2948,2864,2557,2324,2688,1150,49,67,62,66,83,69,68,72,76,9,14,7,16,20,5,11,13,25,4,27,6,19,21,18,17,23,8,10,26,22,12,24,15,35,41])).
% 118.67/118.81 cnf(3066,plain,
% 118.67/118.81 (P4(f6(f6(x30661,f5(f4(a1,x30662),x30663)),f5(x30664,x30665)),f4(a1,x30666))),
% 118.67/118.81 inference(scs_inference,[],[3004,3006,2559,128,107,67,62,66,83,69,68,72])).
% 118.67/118.81 cnf(3117,plain,
% 118.67/118.81 (P8(f6(f6(x31171,f5(a3,a3)),f5(x31172,x31173)),a3,f15(f6(x31174,f5(x31175,a3)),x31175))),
% 118.67/118.81 inference(scs_inference,[],[3002,628,67,62,66,83])).
% 118.67/118.81 cnf(3159,plain,
% 118.67/118.81 (P1(f13(f19(x31591,f7(f19(x31592,a1,x31593)),a2),f4(a1,x31594)),f13(f19(x31591,a2,a2),f4(a1,x31595)))),
% 118.67/118.81 inference(scs_inference,[],[3002,3066,2703,2814,3042,2561,2867,2572,1904,1911,628,127,67,62,66,83,68,72,69,76,9,14,25,7,4,20,11,13,5,16,6,23,18,27,19,21,17,8,22,26,10,12,24,15,41,40,64,28])).
% 118.67/118.81 cnf(3173,plain,
% 118.67/118.81 (P6(x31731,f17(f8(x31731),f7(x31731)))),
% 118.67/118.81 inference(scs_inference,[],[2881,3117,47,67,62,66,83,68])).
% 118.67/118.81 cnf(3853,plain,
% 118.67/118.81 (~E(a10,a1)),
% 118.67/118.81 inference(scs_inference,[],[1835,2276,3159,2,63,13,11])).
% 118.67/118.81 cnf(3857,plain,
% 118.67/118.81 (E(f16(x38571,f4(a1,x38572)),f16(x38571,f4(a1,x38573)))),
% 118.67/118.81 inference(rename_variables,[],[2573])).
% 118.67/118.81 cnf(3866,plain,
% 118.67/118.81 (E(x38661,f16(f6(x38661,f5(x38662,x38663)),x38662))),
% 118.67/118.81 inference(rename_variables,[],[241])).
% 118.67/118.81 cnf(3868,plain,
% 118.67/118.81 (E(x38681,f16(f6(x38681,f5(x38682,x38683)),x38682))),
% 118.67/118.81 inference(rename_variables,[],[241])).
% 118.67/118.81 cnf(3872,plain,
% 118.67/118.81 (P8(f6(f6(x38721,f5(a1,a1)),f5(x38722,x38723)),f4(a1,x38724),f4(a1,x38724))),
% 118.67/118.81 inference(rename_variables,[],[2223])).
% 118.67/118.81 cnf(3875,plain,
% 118.67/118.81 (P4(a10,f14(a9))),
% 118.67/118.81 inference(scs_inference,[],[156,241,3866,3868,2573,3857,1133,1835,52,423,248,2138,261,3173,2276,2223,3872,3159,2697,2,63,13,11,30,37,33,3,32,42,34,35,36,84])).
% 118.67/118.81 cnf(3876,plain,
% 118.67/118.81 (~E(f8(f19(a9,a10,a11)),f19(x38761,x38762,a3))),
% 118.67/118.81 inference(rename_variables,[],[2138])).
% 118.67/118.81 cnf(3880,plain,
% 118.67/118.81 (~P9(f14(a9),f15(a10,f14(a9)))),
% 118.67/118.81 inference(scs_inference,[],[156,241,3866,3868,2573,3857,1133,1835,52,423,248,2138,3876,261,3173,2276,2223,3872,3159,2697,2,63,13,11,30,37,33,3,32,42,34,35,36,84,43,89])).
% 118.67/118.81 cnf(3899,plain,
% 118.67/118.81 (~P1(f15(a10,f14(a9)),f14(a9))),
% 118.67/118.81 inference(scs_inference,[],[3875,3853,70])).
% 118.67/118.81 cnf(3913,plain,
% 118.67/118.81 (P3(f15(f6(x39131,f5(x39132,f19(x39133,a1,x39134))),x39132))),
% 118.67/118.81 inference(scs_inference,[],[52,142,1911,2478,2323,2147,2073,510,2,63,13,11,14,82,344,30])).
% 118.67/118.81 cnf(3923,plain,
% 118.67/118.81 (E(f19(x39231,a1,a3),f8(f19(x39231,a1,x39232)))),
% 118.67/118.81 inference(rename_variables,[],[177])).
% 118.67/118.81 cnf(3925,plain,
% 118.67/118.81 (E(x39251,f16(f6(x39251,f5(x39252,x39253)),x39252))),
% 118.67/118.81 inference(rename_variables,[],[241])).
% 118.67/118.81 cnf(3930,plain,
% 118.67/118.81 (E(x39301,f16(f6(x39301,f5(x39302,x39303)),x39302))),
% 118.67/118.81 inference(rename_variables,[],[241])).
% 118.67/118.81 cnf(3932,plain,
% 118.67/118.81 (E(x39321,f16(f6(x39321,f5(x39322,x39323)),x39322))),
% 118.67/118.81 inference(rename_variables,[],[241])).
% 118.67/118.81 cnf(3936,plain,
% 118.67/118.81 (E(x39361,f16(f6(x39361,f5(x39362,x39363)),x39362))),
% 118.67/118.81 inference(rename_variables,[],[241])).
% 118.67/118.81 cnf(3938,plain,
% 118.67/118.81 (E(x39381,f16(f6(x39381,f5(x39382,x39383)),x39382))),
% 118.67/118.81 inference(rename_variables,[],[241])).
% 118.67/118.81 cnf(3943,plain,
% 118.67/118.81 (E(x39431,f16(f6(x39431,f5(x39432,x39433)),x39432))),
% 118.67/118.81 inference(rename_variables,[],[241])).
% 118.67/118.81 cnf(3949,plain,
% 118.67/118.81 (P5(f19(x39491,f6(f6(f6(f6(f6(x39492,f5(a1,x39493)),f5(x39494,x39495)),f5(x39496,x39497)),f5(x39498,x39499)),f5(x394910,x394911)),x394912),f16(f6(f4(a1,x394913),f5(x394914,x394915)),x394914))),
% 118.67/118.81 inference(scs_inference,[],[204,604,156,103,177,3923,241,3925,3930,3932,3936,3938,3943,1133,2563,1835,516,52,1150,431,150,142,1911,59,165,2478,2323,2054,2147,2207,2073,375,474,3014,510,3040,2,63,13,11,14,82,344,30,37,33,31,29,3,32,28,39,42,34,65,35,36,75,43])).
% 118.67/118.81 cnf(3979,plain,
% 118.67/118.81 (E(x39791,f16(f6(x39791,f5(x39792,x39793)),x39792))),
% 118.67/118.81 inference(rename_variables,[],[241])).
% 118.67/118.81 cnf(3981,plain,
% 118.67/118.81 (E(x39811,f16(f6(x39811,f5(x39812,x39813)),x39812))),
% 118.67/118.81 inference(rename_variables,[],[241])).
% 118.67/118.81 cnf(3986,plain,
% 118.67/118.81 (E(x39861,f16(f6(x39861,f5(x39862,x39863)),x39862))),
% 118.67/118.81 inference(rename_variables,[],[241])).
% 118.67/118.81 cnf(3988,plain,
% 118.67/118.81 (E(x39881,f16(f6(x39881,f5(x39882,x39883)),x39882))),
% 118.67/118.81 inference(rename_variables,[],[241])).
% 118.67/118.81 cnf(3990,plain,
% 118.67/118.81 (E(x39901,f16(f6(x39901,f5(x39902,x39903)),x39902))),
% 118.67/118.81 inference(rename_variables,[],[241])).
% 118.67/118.81 cnf(3995,plain,
% 118.67/118.81 (E(x39951,f16(f6(x39951,f5(x39952,x39953)),x39952))),
% 118.67/118.81 inference(rename_variables,[],[241])).
% 118.67/118.81 cnf(3998,plain,
% 118.67/118.81 ($false),
% 118.67/118.81 inference(scs_inference,[],[241,3979,3981,3986,3988,3990,3995,2573,2563,1705,57,50,98,248,437,433,429,2478,1921,424,148,2867,510,2204,3913,3899,3949,3880,2343,2,63,14,82,344,60,61,30,37,33,31,29,3,32,28,39,77,42,34,64]),
% 118.67/118.81 ['proof']).
% 118.67/118.81 % SZS output end Proof
% 118.67/118.81 % Total time :117.930000s
%------------------------------------------------------------------------------