%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : SWV409+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 : n020.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:08 EDT 2024
% Result : Theorem 77.02s 77.02s
% Output : CNFRefutation 77.02s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.12 % Problem : SWV409+1 : TPTP v8.2.0. Released v3.3.0.
% 0.11/0.12 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% 0.12/0.33 % Computer : n020.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 14:09:54 EDT 2024
% 0.12/0.33 % CPUTime :
% 0.21/0.57 start to proof:theBenchmark
% 76.92/77.00 %-------------------------------------------
% 76.92/77.00 % File :CSE---1.7
% 76.92/77.00 % Problem :theBenchmark
% 76.92/77.00 % Transform :cnf
% 76.92/77.00 % Format :tptp:raw
% 76.92/77.00 % Command :java -jar mcs_scs.jar %d %s
% 76.92/77.00
% 76.92/77.00 % Result :Theorem 76.390000s
% 76.92/77.00 % Output :CNFRefutation 76.390000s
% 76.92/77.00 %-------------------------------------------
% 77.02/77.02 %------------------------------------------------------------------------------
% 77.02/77.02 % File : SWV409+1 : TPTP v8.2.0. Released v3.3.0.
% 77.02/77.02 % Domain : Software Verification
% 77.02/77.02 % Problem : Priority queue checker: lemma_contains_update
% 77.02/77.02 % Version : [dNP05] axioms.
% 77.02/77.02 % English :
% 77.02/77.02
% 77.02/77.02 % Refs : [Pis06] Piskac (2006), Email to Geoff Sutcliffe
% 77.02/77.02 % : [dNP05] de Nivelle & Piskac (2005), Verification of an Off-Lin
% 77.02/77.02 % Source : [Pis06]
% 77.02/77.02 % Names : cpq_l045 [Pis06]
% 77.02/77.02
% 77.02/77.02 % Status : Theorem
% 77.02/77.02 % Rating : 0.19 v8.1.0, 0.22 v7.4.0, 0.13 v7.3.0, 0.17 v7.2.0, 0.14 v7.1.0, 0.17 v7.0.0, 0.13 v6.4.0, 0.19 v6.3.0, 0.25 v6.2.0, 0.28 v6.1.0, 0.27 v6.0.0, 0.17 v5.5.0, 0.22 v5.4.0, 0.25 v5.3.0, 0.33 v5.2.0, 0.25 v5.1.0, 0.24 v5.0.0, 0.29 v4.1.0, 0.30 v4.0.1, 0.26 v4.0.0, 0.25 v3.7.0, 0.20 v3.5.0, 0.21 v3.3.0
% 77.02/77.02 % Syntax : Number of formulae : 22 ( 9 unt; 0 def)
% 77.02/77.02 % Number of atoms : 50 ( 12 equ)
% 77.02/77.02 % Maximal formula atoms : 5 ( 2 avg)
% 77.02/77.02 % Number of connectives : 34 ( 6 ~; 4 |; 12 &)
% 77.02/77.02 % ( 3 <=>; 9 =>; 0 <=; 0 <~>)
% 77.02/77.02 % Maximal formula depth : 9 ( 5 avg)
% 77.02/77.02 % Maximal term depth : 4 ( 1 avg)
% 77.02/77.02 % Number of predicates : 6 ( 5 usr; 0 prp; 1-3 aty)
% 77.02/77.02 % Number of functors : 7 ( 7 usr; 2 con; 0-2 aty)
% 77.02/77.02 % Number of variables : 63 ( 60 !; 3 ?)
% 77.02/77.02 % SPC : FOF_THM_RFO_SEQ
% 77.02/77.02
% 77.02/77.02 % Comments :
% 77.02/77.02 %------------------------------------------------------------------------------
% 77.02/77.02 %----Include the axioms about priority queues and checked priority queues
% 77.02/77.02 include('Axioms/SWV007+0.ax').
% 77.02/77.02 include('Axioms/SWV007+2.ax').
% 77.02/77.02 %------------------------------------------------------------------------------
% 77.02/77.02 %----lemma_contains_pair (cpq_l046.p, cpq_l047.p)
% 77.02/77.02 fof(l45_li4647,lemma,
% 77.02/77.02 ! [U,V] :
% 77.02/77.02 ( contains_slb(U,V)
% 77.02/77.02 => ? [W] : pair_in_list(U,V,W) ) ).
% 77.02/77.02
% 77.02/77.02 %----lemma_contains_update_01 (cpq_l048.p)
% 77.02/77.02 fof(l45_l48,lemma,
% 77.02/77.02 ! [U,V,W,X] :
% 77.02/77.02 ( ( pair_in_list(U,V,W)
% 77.02/77.02 & strictly_less_than(V,X)
% 77.02/77.02 & strictly_less_than(W,X) )
% 77.02/77.02 => pair_in_list(update_slb(U,X),V,X) ) ).
% 77.02/77.02
% 77.02/77.02 %----lemma_contains_update_02 (cpq_l049.p)
% 77.02/77.02 fof(l45_l49,lemma,
% 77.02/77.02 ! [U,V,W,X] :
% 77.02/77.02 ( ( pair_in_list(U,V,W)
% 77.02/77.02 & strictly_less_than(V,X)
% 77.02/77.02 & less_than(X,W) )
% 77.02/77.02 => ? [Y] :
% 77.02/77.02 ( pair_in_list(update_slb(U,X),V,Y)
% 77.02/77.02 & less_than(X,Y) ) ) ).
% 77.02/77.02
% 77.02/77.02 %----lemma_contains_update (conjecture)
% 77.02/77.02 fof(l45_co,conjecture,
% 77.02/77.02 ! [U,V,W] :
% 77.02/77.02 ( ( contains_slb(U,V)
% 77.02/77.02 & strictly_less_than(V,W) )
% 77.02/77.02 => ( pair_in_list(update_slb(U,W),V,W)
% 77.02/77.02 | ? [X] :
% 77.02/77.02 ( pair_in_list(update_slb(U,W),V,X)
% 77.02/77.02 & less_than(W,X) ) ) ) ).
% 77.02/77.02
% 77.02/77.02 %------------------------------------------------------------------------------
% 77.02/77.02 %-------------------------------------------
% 77.02/77.02 % Proof found
% 77.02/77.02 % SZS status Theorem for theBenchmark
% 77.02/77.02 % SZS output start Proof
% 77.02/77.04 %ClaNum:62(EqnAxiom:29)
% 77.02/77.04 %VarNum:188(SingletonVarNum:89)
% 77.02/77.04 %MaxLitNum:4
% 77.02/77.04 %MaxfuncDepth:3
% 77.02/77.04 %SharedTerms:10
% 77.02/77.04 %goalClause: 30 31 41 51
% 77.02/77.04 %singleGoalClaCount:3
% 77.02/77.04 [30]P1(a1,a7)
% 77.02/77.04 [31]P2(a2,a1)
% 77.02/77.04 [38]~P4(a3)
% 77.02/77.04 [41]~P5(f8(a2,a7),a1,a7)
% 77.02/77.04 [33]P3(a4,x331)
% 77.02/77.04 [34]P3(x341,x341)
% 77.02/77.04 [39]~P2(a3,x391)
% 77.02/77.04 [32]E(f8(a3,x321),a3)
% 77.02/77.04 [40]~P5(a3,x401,x402)
% 77.02/77.04 [35]P4(f10(x351,f9(x352,x353)))
% 77.02/77.04 [36]E(f12(f10(x361,f9(x362,x363)),x362),x361)
% 77.02/77.04 [37]E(f11(f10(x371,f9(x372,x373)),x372),x373)
% 77.02/77.04 [51]~P3(a7,x511)+~P5(f8(a2,a7),a1,x511)
% 77.02/77.04 [42]P3(x422,x421)+P3(x421,x422)
% 77.02/77.04 [43]~P1(x431,x432)+P3(x431,x432)
% 77.02/77.04 [44]~P1(x442,x441)+~P3(x441,x442)
% 77.02/77.04 [48]~P2(x481,x482)+P5(x481,x482,f5(x481,x482))
% 77.02/77.04 [47]~E(x472,x474)+P2(f10(x471,f9(x472,x473)),x474)
% 77.02/77.04 [49]~P2(x491,x494)+P2(f10(x491,f9(x492,x493)),x494)
% 77.02/77.04 [54]~P3(x542,x544)+E(f10(f8(x541,x542),f9(x543,x544)),f8(f10(x541,f9(x543,x544)),x542))
% 77.02/77.04 [55]~P1(x553,x554)+E(f8(f10(x551,f9(x552,x553)),x554),f10(f8(x551,x554),f9(x552,x554)))
% 77.02/77.04 [58]~P5(x581,x584,x585)+P5(f10(x581,f9(x582,x583)),x584,x585)
% 77.02/77.04 [45]P1(x452,x451)+~P3(x452,x451)+P3(x451,x452)
% 77.02/77.04 [46]~P3(x461,x463)+P3(x461,x462)+~P3(x463,x462)
% 77.02/77.04 [53]E(x531,x532)+P2(x533,x532)+~P2(f10(x533,f9(x531,x534)),x532)
% 77.02/77.04 [50]~P2(x503,x502)+E(x501,x502)+E(f11(f10(x503,f9(x501,x504)),x502),f11(x503,x502))
% 77.02/77.04 [56]~P2(x563,x562)+E(x561,x562)+E(f12(f10(x563,f9(x561,x564)),x562),f10(f12(x563,x562),f9(x561,x564)))
% 77.02/77.04 [52]~E(x523,x525)+~E(x522,x524)+P5(f10(x521,f9(x522,x523)),x524,x525)
% 77.02/77.04 [59]E(x591,x592)+P5(x593,x594,x592)+~P5(f10(x593,f9(x595,x591)),x594,x592)
% 77.02/77.04 [60]E(x601,x602)+P5(x603,x602,x604)+~P5(f10(x603,f9(x601,x605)),x602,x604)
% 77.02/77.04 [57]~P1(x573,x572)+~P5(x571,x573,x574)+~P1(x574,x572)+P5(f8(x571,x572),x573,x572)
% 77.02/77.04 [61]~P3(x611,x614)+~P1(x613,x611)+~P5(x612,x613,x614)+P3(x611,f6(x612,x613,x614,x611))
% 77.02/77.04 [62]~P3(x622,x624)+~P1(x623,x622)+~P5(x621,x623,x624)+P5(f8(x621,x622),x623,f6(x621,x623,x624,x622))
% 77.02/77.04 %EqnAxiom
% 77.02/77.04 [1]E(x11,x11)
% 77.02/77.04 [2]E(x22,x21)+~E(x21,x22)
% 77.02/77.04 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 77.02/77.04 [4]~E(x41,x42)+E(f8(x41,x43),f8(x42,x43))
% 77.02/77.04 [5]~E(x51,x52)+E(f8(x53,x51),f8(x53,x52))
% 77.02/77.04 [6]~E(x61,x62)+E(f9(x61,x63),f9(x62,x63))
% 77.02/77.04 [7]~E(x71,x72)+E(f9(x73,x71),f9(x73,x72))
% 77.02/77.04 [8]~E(x81,x82)+E(f10(x81,x83),f10(x82,x83))
% 77.02/77.04 [9]~E(x91,x92)+E(f10(x93,x91),f10(x93,x92))
% 77.02/77.04 [10]~E(x101,x102)+E(f6(x101,x103,x104,x105),f6(x102,x103,x104,x105))
% 77.02/77.04 [11]~E(x111,x112)+E(f6(x113,x111,x114,x115),f6(x113,x112,x114,x115))
% 77.02/77.04 [12]~E(x121,x122)+E(f6(x123,x124,x121,x125),f6(x123,x124,x122,x125))
% 77.02/77.04 [13]~E(x131,x132)+E(f6(x133,x134,x135,x131),f6(x133,x134,x135,x132))
% 77.02/77.04 [14]~E(x141,x142)+E(f11(x141,x143),f11(x142,x143))
% 77.02/77.04 [15]~E(x151,x152)+E(f11(x153,x151),f11(x153,x152))
% 77.02/77.04 [16]~E(x161,x162)+E(f12(x161,x163),f12(x162,x163))
% 77.02/77.04 [17]~E(x171,x172)+E(f12(x173,x171),f12(x173,x172))
% 77.02/77.04 [18]~E(x181,x182)+E(f5(x181,x183),f5(x182,x183))
% 77.02/77.04 [19]~E(x191,x192)+E(f5(x193,x191),f5(x193,x192))
% 77.02/77.04 [20]P1(x202,x203)+~E(x201,x202)+~P1(x201,x203)
% 77.02/77.04 [21]P1(x213,x212)+~E(x211,x212)+~P1(x213,x211)
% 77.02/77.04 [22]P2(x222,x223)+~E(x221,x222)+~P2(x221,x223)
% 77.02/77.04 [23]P2(x233,x232)+~E(x231,x232)+~P2(x233,x231)
% 77.02/77.04 [24]P3(x242,x243)+~E(x241,x242)+~P3(x241,x243)
% 77.02/77.04 [25]P3(x253,x252)+~E(x251,x252)+~P3(x253,x251)
% 77.02/77.04 [26]P5(x262,x263,x264)+~E(x261,x262)+~P5(x261,x263,x264)
% 77.02/77.04 [27]P5(x273,x272,x274)+~E(x271,x272)+~P5(x273,x271,x274)
% 77.02/77.04 [28]P5(x283,x284,x282)+~E(x281,x282)+~P5(x283,x284,x281)
% 77.02/77.04 [29]~P4(x291)+P4(x292)+~E(x291,x292)
% 77.02/77.04
% 77.02/77.04 %-------------------------------------------
% 77.02/77.06 cnf(63,plain,
% 77.02/77.06 (P2(f10(x632,f9(x631,x633)),x631)),
% 77.02/77.06 inference(equality_inference,[],[47])).
% 77.02/77.06 cnf(64,plain,
% 77.02/77.06 (~P1(x641,x641)),
% 77.02/77.06 inference(scs_inference,[],[34,44])).
% 77.02/77.06 cnf(66,plain,
% 77.02/77.06 (E(a3,f8(a3,x661))),
% 77.02/77.06 inference(scs_inference,[],[34,32,44,2])).
% 77.02/77.06 cnf(67,plain,
% 77.02/77.06 (~E(a1,a7)),
% 77.02/77.06 inference(scs_inference,[],[30,34,32,44,2,20])).
% 77.02/77.06 cnf(68,plain,
% 77.02/77.06 (~E(a2,a3)),
% 77.02/77.06 inference(scs_inference,[],[30,31,34,39,32,44,2,20,22])).
% 77.02/77.06 cnf(70,plain,
% 77.02/77.06 (P2(f10(x701,f9(f8(a3,x702),x703)),a3)),
% 77.02/77.06 inference(scs_inference,[],[30,31,34,63,39,32,44,2,20,22,23])).
% 77.02/77.06 cnf(72,plain,
% 77.02/77.06 (~E(a2,f8(a3,x721))),
% 77.02/77.06 inference(scs_inference,[],[30,31,34,63,39,32,44,2,20,22,23,3])).
% 77.02/77.06 cnf(73,plain,
% 77.02/77.06 (~P4(f8(a3,x731))),
% 77.02/77.06 inference(scs_inference,[],[30,31,34,63,39,38,32,44,2,20,22,23,3,29])).
% 77.02/77.06 cnf(74,plain,
% 77.02/77.06 (~P5(a2,a1,a1)),
% 77.02/77.06 inference(scs_inference,[],[30,31,41,34,63,39,38,32,44,2,20,22,23,3,29,57])).
% 77.02/77.06 cnf(81,plain,
% 77.02/77.06 (P1(a4,f8(a3,x811))+P3(a7,x812)+~E(a7,x812)),
% 77.02/77.06 inference(scs_inference,[],[30,31,41,34,63,33,39,38,32,44,2,20,22,23,3,29,57,45,24,25])).
% 77.02/77.06 cnf(83,plain,
% 77.02/77.06 (~P1(x831,a4)),
% 77.02/77.06 inference(scs_inference,[],[33,44])).
% 77.02/77.06 cnf(85,plain,
% 77.02/77.06 (E(x851,f12(f10(x851,f9(x852,x853)),x852))),
% 77.02/77.06 inference(scs_inference,[],[33,36,44,2])).
% 77.02/77.06 cnf(87,plain,
% 77.02/77.06 (~P2(a3,x871)),
% 77.02/77.06 inference(rename_variables,[],[39])).
% 77.02/77.06 cnf(88,plain,
% 77.02/77.06 (~E(a1,f12(f10(a7,f9(x881,x882)),x881))),
% 77.02/77.06 inference(scs_inference,[],[70,67,33,36,39,44,2,22,3])).
% 77.02/77.06 cnf(89,plain,
% 77.02/77.06 (E(f12(f10(x891,f9(x892,x893)),x892),x891)),
% 77.02/77.06 inference(rename_variables,[],[36])).
% 77.02/77.06 cnf(90,plain,
% 77.02/77.06 (~P4(f12(f10(f8(a3,x901),f9(x902,x903)),x902))),
% 77.02/77.06 inference(scs_inference,[],[70,67,33,73,36,89,39,44,2,22,3,29])).
% 77.02/77.06 cnf(92,plain,
% 77.02/77.06 (P3(f8(a3,x921),a3)),
% 77.02/77.06 inference(scs_inference,[],[70,67,34,33,73,66,36,89,39,44,2,22,3,29,24])).
% 77.02/77.06 cnf(93,plain,
% 77.02/77.06 (P3(x931,x931)),
% 77.02/77.06 inference(rename_variables,[],[34])).
% 77.02/77.06 cnf(94,plain,
% 77.02/77.06 (P2(f10(x941,f9(f8(a3,x942),x943)),f8(a3,x944))),
% 77.02/77.06 inference(scs_inference,[],[70,67,34,33,73,66,36,89,39,44,2,22,3,29,24,23])).
% 77.02/77.06 cnf(95,plain,
% 77.02/77.06 (~E(a7,a1)),
% 77.02/77.06 inference(scs_inference,[],[30,64,70,67,34,33,73,66,36,89,39,44,2,22,3,29,24,23,21])).
% 77.02/77.06 cnf(97,plain,
% 77.02/77.06 (P3(a3,f8(a3,x971))),
% 77.02/77.06 inference(scs_inference,[],[30,64,70,67,34,93,33,73,66,36,89,39,44,2,22,3,29,24,23,21,25])).
% 77.02/77.06 cnf(99,plain,
% 77.02/77.06 (E(f8(a3,x991),f8(a3,x992))),
% 77.02/77.06 inference(scs_inference,[],[30,64,70,67,34,93,33,73,66,36,89,39,87,44,2,22,3,29,24,23,21,25,53])).
% 77.02/77.06 cnf(102,plain,
% 77.02/77.06 (~P1(a3,f8(a3,x1021))),
% 77.02/77.06 inference(scs_inference,[],[92,44])).
% 77.02/77.06 cnf(104,plain,
% 77.02/77.06 (E(x1041,f11(f10(x1042,f9(x1043,x1041)),x1043))),
% 77.02/77.06 inference(scs_inference,[],[92,37,44,2])).
% 77.02/77.06 cnf(105,plain,
% 77.02/77.06 (P3(f8(a3,x1051),f8(a3,x1052))),
% 77.02/77.06 inference(scs_inference,[],[92,97,37,44,2,46])).
% 77.02/77.06 cnf(107,plain,
% 77.02/77.06 (~E(a2,f11(f10(x1071,f9(x1072,a3)),x1072))),
% 77.02/77.06 inference(scs_inference,[],[68,92,97,37,44,2,46,3])).
% 77.02/77.06 cnf(109,plain,
% 77.02/77.06 (P3(f12(f10(f8(a3,x1091),f9(x1092,x1093)),x1092),a3)),
% 77.02/77.06 inference(scs_inference,[],[68,92,97,85,37,44,2,46,3,24])).
% 77.02/77.06 cnf(110,plain,
% 77.02/77.06 (E(x1101,f12(f10(x1101,f9(x1102,x1103)),x1102))),
% 77.02/77.06 inference(rename_variables,[],[85])).
% 77.02/77.06 cnf(111,plain,
% 77.02/77.06 (P4(f12(f10(f10(x1111,f9(x1112,x1113)),f9(x1114,x1115)),x1114))),
% 77.02/77.06 inference(scs_inference,[],[68,92,97,85,110,37,35,44,2,46,3,24,29])).
% 77.02/77.06 cnf(112,plain,
% 77.02/77.06 (E(x1121,f12(f10(x1121,f9(x1122,x1123)),x1122))),
% 77.02/77.06 inference(rename_variables,[],[85])).
% 77.02/77.06 cnf(113,plain,
% 77.02/77.06 (P2(a2,f12(f10(a1,f9(x1131,x1132)),x1131))),
% 77.02/77.06 inference(scs_inference,[],[31,68,92,97,85,110,112,37,35,44,2,46,3,24,29,23])).
% 77.02/77.06 cnf(114,plain,
% 77.02/77.06 (E(x1141,f12(f10(x1141,f9(x1142,x1143)),x1142))),
% 77.02/77.06 inference(rename_variables,[],[85])).
% 77.02/77.06 cnf(115,plain,
% 77.02/77.06 (~E(f10(x1151,f9(x1152,x1153)),a3)),
% 77.02/77.06 inference(scs_inference,[],[31,68,92,97,85,110,112,63,37,35,39,44,2,46,3,24,29,23,22])).
% 77.02/77.06 cnf(117,plain,
% 77.02/77.06 (~E(a7,a4)),
% 77.02/77.06 inference(scs_inference,[],[30,31,68,83,92,97,85,110,112,63,37,35,39,44,2,46,3,24,29,23,22,21])).
% 77.02/77.06 cnf(119,plain,
% 77.02/77.06 (P3(f8(a3,x1191),f12(f10(a3,f9(x1192,x1193)),x1192))),
% 77.02/77.06 inference(scs_inference,[],[30,31,68,83,92,97,85,110,112,114,63,37,35,39,44,2,46,3,24,29,23,22,21,25])).
% 77.02/77.06 cnf(127,plain,
% 77.02/77.06 (P2(a2,f11(f10(x1271,f9(x1272,a1)),x1272))),
% 77.02/77.06 inference(scs_inference,[],[31,119,115,104,36,44,3,23])).
% 77.02/77.06 cnf(128,plain,
% 77.02/77.06 (E(x1281,f11(f10(x1282,f9(x1283,x1281)),x1283))),
% 77.02/77.06 inference(rename_variables,[],[104])).
% 77.02/77.06 cnf(129,plain,
% 77.02/77.06 (P3(f11(f10(x1291,f9(x1292,a3)),x1292),f8(a3,x1293))),
% 77.02/77.06 inference(scs_inference,[],[31,119,115,97,104,128,36,44,3,23,24])).
% 77.02/77.06 cnf(130,plain,
% 77.02/77.06 (E(x1301,f11(f10(x1302,f9(x1303,x1301)),x1303))),
% 77.02/77.06 inference(rename_variables,[],[104])).
% 77.02/77.06 cnf(131,plain,
% 77.02/77.06 (P3(f8(a3,x1311),f11(f10(x1312,f9(x1313,a3)),x1313))),
% 77.02/77.06 inference(scs_inference,[],[31,92,119,115,97,104,128,130,36,44,3,23,24,25])).
% 77.02/77.06 cnf(135,plain,
% 77.02/77.06 (~P1(f8(a3,x1351),a3)),
% 77.02/77.06 inference(scs_inference,[],[97,44])).
% 77.02/77.06 cnf(137,plain,
% 77.02/77.06 (P3(a3,f12(f10(a3,f9(x1371,x1372)),x1371))),
% 77.02/77.06 inference(scs_inference,[],[119,97,44,46])).
% 77.02/77.06 cnf(140,plain,
% 77.02/77.06 (~E(a7,f11(f10(x1401,f9(x1402,a1)),x1402))),
% 77.02/77.06 inference(scs_inference,[],[119,97,95,37,44,46,3])).
% 77.02/77.06 cnf(142,plain,
% 77.02/77.06 (P3(f12(f10(f8(a3,x1421),f9(x1422,x1423)),x1422),f8(a3,x1424))),
% 77.02/77.06 inference(scs_inference,[],[119,97,95,105,85,37,44,46,3,24])).
% 77.02/77.06 cnf(143,plain,
% 77.02/77.06 (E(x1431,f12(f10(x1431,f9(x1432,x1433)),x1432))),
% 77.02/77.06 inference(rename_variables,[],[85])).
% 77.02/77.06 cnf(144,plain,
% 77.02/77.06 (P2(f10(x1441,f9(a3,x1442)),f8(a3,x1443))),
% 77.02/77.06 inference(scs_inference,[],[119,97,95,105,66,63,85,37,44,46,3,24,23])).
% 77.02/77.06 cnf(146,plain,
% 77.02/77.06 (P3(a3,f12(f10(f8(a3,x1461),f9(x1462,x1463)),x1462))),
% 77.02/77.06 inference(scs_inference,[],[119,97,95,105,66,63,85,143,37,44,46,3,24,23,25])).
% 77.02/77.06 cnf(152,plain,
% 77.02/77.06 (P3(f8(a3,x1521),f12(f10(f8(a3,x1522),f9(x1523,x1524)),x1523))),
% 77.02/77.06 inference(scs_inference,[],[92,129,146,44,46])).
% 77.02/77.06 cnf(154,plain,
% 77.02/77.06 (P3(f11(f10(x1541,f9(x1542,a4)),x1542),x1543)),
% 77.02/77.06 inference(scs_inference,[],[92,129,146,33,104,44,46,24])).
% 77.02/77.06 cnf(156,plain,
% 77.02/77.06 (~E(a7,f12(f10(a4,f9(x1561,x1562)),x1561))),
% 77.02/77.06 inference(scs_inference,[],[92,129,146,117,33,104,36,44,46,24,3])).
% 77.02/77.06 cnf(160,plain,
% 77.02/77.06 (P3(f11(f10(x1601,f9(x1602,a3)),x1602),a3)),
% 77.02/77.06 inference(scs_inference,[],[92,109,129,44,46])).
% 77.02/77.06 cnf(164,plain,
% 77.02/77.06 (E(x1641,f12(f10(x1641,f9(x1642,x1643)),x1642))),
% 77.02/77.06 inference(rename_variables,[],[85])).
% 77.02/77.06 cnf(165,plain,
% 77.02/77.06 (~E(a2,f12(f10(a3,f9(x1651,x1652)),x1651))),
% 77.02/77.06 inference(scs_inference,[],[92,109,129,144,68,85,36,44,46,23,3])).
% 77.02/77.06 cnf(167,plain,
% 77.02/77.06 (P3(f12(f10(a4,f9(x1671,x1672)),x1671),x1673)),
% 77.02/77.06 inference(scs_inference,[],[92,109,129,144,68,33,85,164,36,44,46,23,3,24])).
% 77.02/77.06 cnf(169,plain,
% 77.02/77.06 (E(a3,f12(f10(f8(a3,x1691),f9(x1692,x1693)),x1692))),
% 77.02/77.06 inference(scs_inference,[],[92,109,129,144,68,33,85,164,36,39,44,46,23,3,24,53])).
% 77.02/77.06 cnf(174,plain,
% 77.02/77.06 (E(f12(f10(f8(a3,x1741),f9(x1742,x1743)),x1742),a3)),
% 77.02/77.06 inference(scs_inference,[],[92,109,129,144,68,33,85,164,36,39,44,46,23,3,24,53,45,2])).
% 77.02/77.06 cnf(177,plain,
% 77.02/77.06 (~E(f10(x1771,f9(x1772,x1773)),f12(f10(f8(a3,x1774),f9(x1775,x1776)),x1775))),
% 77.02/77.06 inference(scs_inference,[],[142,115,174,44,3])).
% 77.02/77.06 cnf(180,plain,
% 77.02/77.06 (~E(f10(x1801,f9(x1802,x1803)),f8(a3,x1804))),
% 77.02/77.06 inference(scs_inference,[],[137,85,177,44,3])).
% 77.02/77.06 cnf(184,plain,
% 77.02/77.06 (~E(a2,f12(f10(f8(a3,x1841),f9(x1842,x1843)),x1842))),
% 77.02/77.06 inference(scs_inference,[],[160,68,174,44,3])).
% 77.02/77.06 cnf(185,plain,
% 77.02/77.06 (~P1(x1851,f11(f10(x1852,f9(x1853,a4)),x1853))),
% 77.02/77.06 inference(scs_inference,[],[154,44])).
% 77.02/77.06 cnf(187,plain,
% 77.02/77.06 (~E(a1,f11(f10(x1871,f9(x1872,a7)),x1872))),
% 77.02/77.06 inference(scs_inference,[],[154,67,37,44,3])).
% 77.02/77.06 cnf(193,plain,
% 77.02/77.06 (~E(a7,f12(f10(a1,f9(x1931,x1932)),x1931))),
% 77.02/77.06 inference(scs_inference,[],[30,105,185,95,36,44,21,3])).
% 77.02/77.06 cnf(197,plain,
% 77.02/77.06 (~P1(f11(f10(x1971,f9(x1972,a3)),x1972),f8(a3,x1973))),
% 77.02/77.06 inference(scs_inference,[],[131,44])).
% 77.02/77.06 cnf(199,plain,
% 77.02/77.06 (~P1(f12(f10(f8(a3,x1991),f9(x1992,x1993)),x1992),f8(a3,x1994))),
% 77.02/77.06 inference(scs_inference,[],[152,44])).
% 77.02/77.06 cnf(201,plain,
% 77.02/77.06 (~P1(x2011,f12(f10(a4,f9(x2012,x2013)),x2012))),
% 77.02/77.06 inference(scs_inference,[],[167,44])).
% 77.02/77.06 cnf(203,plain,
% 77.02/77.06 (P3(a1,a7)),
% 77.02/77.06 inference(scs_inference,[],[30,42,44])).
% 77.02/77.06 cnf(204,plain,
% 77.02/77.06 (~P1(a7,a1)),
% 77.02/77.06 inference(scs_inference,[],[203,44])).
% 77.02/77.06 cnf(206,plain,
% 77.02/77.06 (P3(a1,f11(f10(x2061,f9(x2062,a7)),x2062))),
% 77.02/77.06 inference(scs_inference,[],[203,104,44,25])).
% 77.02/77.06 cnf(214,plain,
% 77.02/77.06 (P3(a1,f12(f10(a7,f9(x2141,x2142)),x2141))),
% 77.02/77.06 inference(scs_inference,[],[203,206,85,44,25])).
% 77.02/77.06 cnf(215,plain,
% 77.02/77.06 (E(x2151,f12(f10(x2151,f9(x2152,x2153)),x2152))),
% 77.02/77.06 inference(rename_variables,[],[85])).
% 77.02/77.06 cnf(216,plain,
% 77.02/77.06 (P3(f12(f10(a1,f9(x2161,x2162)),x2161),a7)),
% 77.02/77.06 inference(scs_inference,[],[203,206,85,215,44,25,24])).
% 77.02/77.06 cnf(230,plain,
% 77.02/77.06 (E(f10(f8(x2301,a1),f9(x2302,a7)),f8(f10(x2301,f9(x2302,a7)),a1))),
% 77.02/77.06 inference(scs_inference,[],[30,43,54])).
% 77.02/77.06 cnf(232,plain,
% 77.02/77.06 (P4(f8(f10(x2321,f9(x2322,a7)),a1))),
% 77.02/77.07 inference(scs_inference,[],[230,35,2,29])).
% 77.02/77.07 cnf(243,plain,
% 77.02/77.07 (~P5(f8(a2,a7),a1,f11(f10(x2431,f9(x2432,a7)),x2432))),
% 77.02/77.07 inference(scs_inference,[],[34,104,51,25])).
% 77.02/77.07 cnf(244,plain,
% 77.02/77.07 (E(f8(f8(a3,x2441),x2442),f8(a3,x2442))),
% 77.02/77.07 inference(scs_inference,[],[66,4,2])).
% 77.02/77.07 cnf(245,plain,
% 77.02/77.07 (E(f8(a3,x2451),f8(f8(a3,x2452),x2451))),
% 77.02/77.07 inference(scs_inference,[],[244,2])).
% 77.02/77.07 cnf(246,plain,
% 77.02/77.07 (~P4(f8(f8(a3,x2461),x2462))),
% 77.02/77.07 inference(scs_inference,[],[244,73,2,29])).
% 77.02/77.07 cnf(247,plain,
% 77.02/77.07 (E(f8(f8(a3,x2471),x2472),f8(a3,x2472))),
% 77.02/77.07 inference(rename_variables,[],[244])).
% 77.02/77.07 cnf(248,plain,
% 77.02/77.07 (~E(f10(x2481,f9(x2482,x2483)),f8(f8(a3,x2484),x2485))),
% 77.02/77.07 inference(scs_inference,[],[180,244,247,73,2,29,3])).
% 77.02/77.07 cnf(250,plain,
% 77.02/77.07 (E(f8(x2501,f9(a3,x2502)),f8(x2501,f9(f8(a3,x2503),x2502)))),
% 77.02/77.07 inference(scs_inference,[],[66,5,6])).
% 77.02/77.07 cnf(251,plain,
% 77.02/77.07 (E(f8(x2511,f9(f8(a3,x2512),x2513)),f8(x2511,f9(a3,x2513)))),
% 77.02/77.07 inference(scs_inference,[],[250,2])).
% 77.02/77.07 cnf(252,plain,
% 77.02/77.07 (~E(a2,f8(f8(a3,x2521),x2522))),
% 77.02/77.07 inference(scs_inference,[],[250,72,244,2,3])).
% 77.02/77.07 cnf(254,plain,
% 77.02/77.07 (E(f9(x2541,f10(a3,x2542)),f9(x2541,f10(f8(a3,x2543),x2542)))),
% 77.02/77.07 inference(scs_inference,[],[66,7,8])).
% 77.02/77.07 cnf(255,plain,
% 77.02/77.07 (E(f9(x2551,f10(f8(a3,x2552),x2553)),f9(x2551,f10(a3,x2553)))),
% 77.02/77.07 inference(scs_inference,[],[254,2])).
% 77.02/77.07 cnf(257,plain,
% 77.02/77.07 (E(f10(x2571,f6(a3,x2572,x2573,x2574)),f10(x2571,f6(f8(a3,x2575),x2572,x2573,x2574)))),
% 77.02/77.07 inference(scs_inference,[],[66,9,10])).
% 77.02/77.07 cnf(260,plain,
% 77.02/77.07 (E(f11(f6(x2601,a3,x2602,x2603),x2604),f11(f6(x2601,f8(a3,x2605),x2602,x2603),x2604))),
% 77.02/77.07 inference(scs_inference,[],[66,14,11])).
% 77.02/77.07 cnf(261,plain,
% 77.02/77.07 (E(f11(f6(x2611,f8(a3,x2612),x2613,x2614),x2615),f11(f6(x2611,a3,x2613,x2614),x2615))),
% 77.02/77.07 inference(scs_inference,[],[260,2])).
% 77.02/77.07 cnf(263,plain,
% 77.02/77.07 (E(f11(x2631,f6(x2632,x2633,a3,x2634)),f11(x2631,f6(x2632,x2633,f8(a3,x2635),x2634)))),
% 77.02/77.07 inference(scs_inference,[],[66,15,12])).
% 77.02/77.07 cnf(264,plain,
% 77.02/77.07 (E(f11(x2641,f6(x2642,x2643,f8(a3,x2644),x2645)),f11(x2641,f6(x2642,x2643,a3,x2645)))),
% 77.02/77.07 inference(scs_inference,[],[263,2])).
% 77.02/77.07 cnf(269,plain,
% 77.02/77.07 (E(f12(f6(x2691,x2692,x2693,a3),x2694),f12(f6(x2691,x2692,x2693,f8(a3,x2695)),x2694))),
% 77.02/77.07 inference(scs_inference,[],[66,16,13])).
% 77.02/77.07 cnf(270,plain,
% 77.02/77.07 (E(f12(f6(x2701,x2702,x2703,f8(a3,x2704)),x2705),f12(f6(x2701,x2702,x2703,a3),x2705))),
% 77.02/77.07 inference(scs_inference,[],[269,2])).
% 77.02/77.07 cnf(271,plain,
% 77.02/77.07 (E(f11(f6(x2711,f8(a3,x2712),x2713,x2714),f6(x2715,x2716,f8(a3,x2717),x2718)),f11(f6(x2711,a3,x2713,x2714),f6(x2715,x2716,a3,x2718)))),
% 77.02/77.07 inference(scs_inference,[],[264,269,261,2,3])).
% 77.02/77.07 cnf(273,plain,
% 77.02/77.07 (E(f11(x2731,f6(x2732,x2733,f8(a3,x2734),x2735)),f11(x2731,f6(x2732,x2733,a3,x2735)))),
% 77.02/77.07 inference(rename_variables,[],[264])).
% 77.02/77.07 cnf(274,plain,
% 77.02/77.07 (~P4(f11(x2741,f6(x2742,x2743,f8(a3,x2744),x2745)))+P4(f11(x2741,f6(x2742,x2743,a3,x2745)))),
% 77.02/77.07 inference(scs_inference,[],[264,273,269,261,2,3,29])).
% 77.02/77.07 cnf(279,plain,
% 77.02/77.07 (E(f12(x2791,f5(a3,x2792)),f12(x2791,f5(f8(a3,x2793),x2792)))),
% 77.02/77.07 inference(scs_inference,[],[66,17,18])).
% 77.02/77.07 cnf(281,plain,
% 77.02/77.07 (E(f12(f6(x2811,x2812,x2813,f8(a3,x2814)),f5(a3,x2815)),f12(f6(x2811,x2812,x2813,a3),f5(f8(a3,x2816),x2815)))),
% 77.02/77.07 inference(scs_inference,[],[270,271,279,2,3])).
% 77.02/77.07 cnf(287,plain,
% 77.02/77.07 (E(f12(f6(x2871,x2872,x2873,a3),f5(f8(a3,x2874),x2875)),f12(f6(x2871,x2872,x2873,f8(a3,x2876)),f5(a3,x2875)))),
% 77.02/77.07 inference(scs_inference,[],[281,2])).
% 77.02/77.07 cnf(289,plain,
% 77.02/77.07 (E(f12(x2891,f5(f8(a3,x2892),x2893)),f12(x2891,f5(a3,x2893)))),
% 77.02/77.07 inference(scs_inference,[],[279,2])).
% 77.02/77.07 cnf(359,plain,
% 77.02/77.07 (E(f5(x3591,f8(a3,x3592)),f5(x3591,a3))),
% 77.02/77.07 inference(scs_inference,[],[66,19,2])).
% 77.02/77.07 cnf(360,plain,
% 77.02/77.07 (E(f5(x3601,a3),f5(x3601,f8(a3,x3602)))),
% 77.02/77.07 inference(scs_inference,[],[359,2])).
% 77.02/77.07 cnf(361,plain,
% 77.02/77.07 (E(f12(f10(f5(x3611,f8(a3,x3612)),f9(x3613,x3614)),x3613),f5(x3611,a3))),
% 77.02/77.07 inference(scs_inference,[],[359,36,2,3])).
% 77.02/77.07 cnf(365,plain,
% 77.02/77.07 (E(f12(f10(f5(x3651,f8(a3,x3652)),f9(x3653,x3654)),x3653),f5(x3651,f8(a3,x3655)))),
% 77.02/77.07 inference(scs_inference,[],[361,360,2,3])).
% 77.02/77.07 cnf(369,plain,
% 77.02/77.07 (E(f5(x3691,f8(a3,x3692)),f5(x3691,f8(a3,x3693)))),
% 77.02/77.07 inference(scs_inference,[],[85,365,2,3])).
% 77.02/77.07 cnf(385,plain,
% 77.02/77.07 (P2(f10(f10(x3851,f9(a3,x3852)),f9(x3853,x3854)),f8(a3,x3855))),
% 77.02/77.07 inference(scs_inference,[],[66,49,47])).
% 77.02/77.07 cnf(387,plain,
% 77.02/77.07 (P3(f12(f10(x3871,f9(x3872,x3873)),x3872),x3871)),
% 77.02/77.07 inference(scs_inference,[],[36,34,25])).
% 77.02/77.07 cnf(388,plain,
% 77.02/77.07 (P3(x3881,x3881)),
% 77.02/77.07 inference(rename_variables,[],[34])).
% 77.02/77.07 cnf(389,plain,
% 77.02/77.07 (P3(x3891,f12(f10(x3891,f9(x3892,x3893)),x3892))),
% 77.02/77.07 inference(scs_inference,[],[36,34,388,25,24])).
% 77.02/77.07 cnf(395,plain,
% 77.02/77.07 (~P1(x3951,f12(f10(x3951,f9(x3952,x3953)),x3952))),
% 77.02/77.07 inference(scs_inference,[],[387,44])).
% 77.02/77.07 cnf(407,plain,
% 77.02/77.07 (P5(f10(a2,f9(x4071,x4072)),a1,f5(a2,a1))),
% 77.02/77.07 inference(scs_inference,[],[31,58,48])).
% 77.02/77.07 cnf(408,plain,
% 77.02/77.07 (~P1(f12(f10(x4081,f9(x4082,x4083)),x4082),x4081)),
% 77.02/77.07 inference(scs_inference,[],[389,44])).
% 77.02/77.07 cnf(410,plain,
% 77.02/77.07 (P5(a2,a1,f5(a2,a1))),
% 77.02/77.07 inference(scs_inference,[],[389,95,407,44,60])).
% 77.02/77.07 cnf(411,plain,
% 77.02/77.07 (P5(f10(a2,f9(x4111,x4112)),a1,f5(a2,a1))),
% 77.02/77.07 inference(rename_variables,[],[407])).
% 77.02/77.07 cnf(413,plain,
% 77.02/77.07 (P5(f10(a2,f9(x4131,x4132)),f11(f10(x4133,f9(x4134,a1)),x4134),f5(a2,a1))),
% 77.02/77.07 inference(scs_inference,[],[389,95,104,407,411,44,60,27])).
% 77.02/77.07 cnf(415,plain,
% 77.02/77.07 (~E(f5(a2,a1),a1)),
% 77.02/77.07 inference(scs_inference,[],[389,74,95,104,407,411,44,60,27,28])).
% 77.02/77.07 cnf(430,plain,
% 77.02/77.07 (E(x4301,f12(f10(x4301,f9(x4302,x4303)),x4302))),
% 77.02/77.07 inference(rename_variables,[],[85])).
% 77.02/77.07 cnf(431,plain,
% 77.02/77.07 (P5(f10(a2,f9(x4311,x4312)),a1,f12(f10(f5(a2,a1),f9(x4313,x4314)),x4313))),
% 77.02/77.07 inference(scs_inference,[],[413,410,85,430,140,407,60,27,28])).
% 77.02/77.07 cnf(432,plain,
% 77.02/77.07 (E(x4321,f12(f10(x4321,f9(x4322,x4323)),x4322))),
% 77.02/77.07 inference(rename_variables,[],[85])).
% 77.02/77.07 cnf(433,plain,
% 77.02/77.07 (P2(f10(f10(x4331,f9(a3,x4332)),f9(x4333,x4334)),f12(f10(f8(a3,x4335),f9(x4336,x4337)),x4336))),
% 77.02/77.07 inference(scs_inference,[],[385,413,410,85,430,432,140,407,60,27,28,23])).
% 77.02/77.07 cnf(435,plain,
% 77.02/77.07 (~E(f5(a2,a1),f12(f10(a1,f9(x4351,x4352)),x4351))),
% 77.02/77.07 inference(scs_inference,[],[36,385,413,410,415,85,430,432,140,407,60,27,28,23,3])).
% 77.02/77.07 cnf(448,plain,
% 77.02/77.07 (P5(f10(a2,f9(x4481,x4482)),f12(f10(a1,f9(x4483,x4484)),x4483),f5(a2,a1))),
% 77.02/77.07 inference(scs_inference,[],[431,415,85,407,60,27])).
% 77.02/77.07 cnf(450,plain,
% 77.02/77.07 (~E(f12(f10(f5(a2,a1),f9(x4501,x4502)),x4501),a1)),
% 77.02/77.07 inference(scs_inference,[],[431,74,415,85,407,60,27,28])).
% 77.02/77.07 cnf(451,plain,
% 77.02/77.07 (~E(f5(a2,a1),f11(f10(x4511,f9(x4512,a1)),x4512))),
% 77.02/77.07 inference(scs_inference,[],[431,74,415,85,37,407,60,27,28,3])).
% 77.02/77.07 cnf(453,plain,
% 77.02/77.07 (P2(f10(f10(x4531,f9(a3,x4532)),f9(x4533,x4534)),a3)),
% 77.02/77.07 inference(scs_inference,[],[433,174,23])).
% 77.02/77.07 cnf(455,plain,
% 77.02/77.07 (P3(f11(f10(x4551,f9(x4552,x4553)),x4552),x4553)),
% 77.02/77.07 inference(scs_inference,[],[37,34,433,174,23,25])).
% 77.02/77.07 cnf(456,plain,
% 77.02/77.07 (P3(x4561,x4561)),
% 77.02/77.07 inference(rename_variables,[],[34])).
% 77.02/77.07 cnf(457,plain,
% 77.02/77.07 (P3(x4571,f11(f10(x4572,f9(x4573,x4571)),x4573))),
% 77.02/77.07 inference(scs_inference,[],[37,34,456,433,174,23,25,24])).
% 77.02/77.07 cnf(460,plain,
% 77.02/77.07 (~P1(x4601,f11(f10(x4602,f9(x4603,x4601)),x4603))),
% 77.02/77.07 inference(scs_inference,[],[455,44])).
% 77.02/77.07 cnf(466,plain,
% 77.02/77.07 (P3(x4661,x4661)),
% 77.02/77.07 inference(rename_variables,[],[34])).
% 77.02/77.07 cnf(469,plain,
% 77.02/77.07 (~P4(f11(f10(x4691,f9(x4692,a3)),x4692))),
% 77.02/77.07 inference(scs_inference,[],[38,34,466,261,37,25,24,29])).
% 77.02/77.07 cnf(521,plain,
% 77.02/77.07 (P2(f10(f10(x5211,f9(a3,x5212)),f9(x5213,x5214)),f12(f10(a3,f9(x5215,x5216)),x5215))),
% 77.02/77.07 inference(scs_inference,[],[85,453,23])).
% 77.02/77.07 cnf(526,plain,
% 77.02/77.07 (P2(f10(x5261,f9(x5262,x5263)),f12(f10(x5262,f9(x5264,x5265)),x5264))),
% 77.02/77.07 inference(scs_inference,[],[85,63,23])).
% 77.02/77.07 cnf(533,plain,
% 77.02/77.07 (P2(f10(f10(x5331,f9(a3,x5332)),f9(x5333,x5334)),f11(f10(x5335,f9(x5336,a3)),x5336))),
% 77.02/77.07 inference(scs_inference,[],[104,453,23])).
% 77.02/77.07 cnf(538,plain,
% 77.02/77.07 (P2(f10(x5381,f9(x5382,x5383)),f11(f10(x5384,f9(x5385,x5382)),x5385))),
% 77.02/77.07 inference(scs_inference,[],[104,63,23])).
% 77.02/77.07 cnf(541,plain,
% 77.02/77.07 (~E(f10(x5411,f9(x5412,x5413)),f11(f10(x5414,f9(x5415,a3)),x5415))),
% 77.02/77.07 inference(scs_inference,[],[115,37,3])).
% 77.02/77.07 cnf(560,plain,
% 77.02/77.07 (E(f5(f12(f10(f8(a3,x5601),f9(x5602,x5603)),x5602),x5604),f5(a3,x5604))),
% 77.02/77.07 inference(scs_inference,[],[169,2,18])).
% 77.02/77.07 cnf(562,plain,
% 77.02/77.07 (E(f10(f8(x5621,a7),f9(x5622,a7)),f8(f10(x5621,f9(x5622,a1)),a7))),
% 77.02/77.07 inference(scs_inference,[],[30,2,55])).
% 77.02/77.07 cnf(563,plain,
% 77.02/77.07 (E(f8(f10(x5631,f9(x5632,a1)),a7),f10(f8(x5631,a7),f9(x5632,a7)))),
% 77.02/77.07 inference(scs_inference,[],[562,2])).
% 77.02/77.07 cnf(564,plain,
% 77.02/77.07 (P4(f8(f10(x5641,f9(x5642,a1)),a7))),
% 77.02/77.07 inference(scs_inference,[],[562,35,2,29])).
% 77.02/77.07 cnf(570,plain,
% 77.02/77.07 (~E(f12(f10(f8(a3,x5701),f9(x5702,x5703)),x5702),f12(f10(a2,f9(x5704,x5705)),x5704))),
% 77.02/77.07 inference(scs_inference,[],[184,36,2,3])).
% 77.02/77.07 cnf(572,plain,
% 77.02/77.07 (P1(a1,f12(f10(a7,f9(x5721,x5722)),x5721))),
% 77.02/77.07 inference(scs_inference,[],[30,85,21])).
% 77.02/77.07 cnf(574,plain,
% 77.02/77.07 (~P2(f10(a3,f9(a1,x5741)),f12(f10(f5(a2,a1),f9(x5742,x5743)),x5742))),
% 77.02/77.07 inference(scs_inference,[],[450,39,2,53])).
% 77.02/77.07 cnf(575,plain,
% 77.02/77.07 (~E(a1,f12(f10(f5(a2,a1),f9(x5751,x5752)),x5751))),
% 77.02/77.07 inference(scs_inference,[],[574,47])).
% 77.02/77.07 cnf(577,plain,
% 77.02/77.07 (~E(f10(x5771,f9(f5(a2,a1),x5772)),f10(a3,f9(a1,x5773)))),
% 77.02/77.07 inference(scs_inference,[],[526,574,47,22])).
% 77.02/77.07 cnf(579,plain,
% 77.02/77.07 (~E(f9(f5(a2,a1),x5791),f9(a1,x5792))),
% 77.02/77.07 inference(scs_inference,[],[526,574,47,22,9])).
% 77.02/77.07 cnf(581,plain,
% 77.02/77.07 (~E(a1,f5(a2,a1))),
% 77.02/77.07 inference(scs_inference,[],[579,2,6])).
% 77.02/77.07 cnf(583,plain,
% 77.02/77.07 (~E(f9(a1,x5831),f9(f5(a2,a1),x5832))),
% 77.02/77.07 inference(scs_inference,[],[577,2,9])).
% 77.02/77.07 cnf(586,plain,
% 77.02/77.07 (E(f11(f10(a2,f9(a7,x5861)),a1),f11(a2,a1))),
% 77.02/77.07 inference(scs_inference,[],[67,31,2,50])).
% 77.02/77.07 cnf(608,plain,
% 77.02/77.07 (E(f8(x6081,f11(a2,a1)),f8(x6081,f11(f10(a2,f9(a7,x6082)),a1)))),
% 77.02/77.07 inference(scs_inference,[],[586,2,5])).
% 77.02/77.07 cnf(613,plain,
% 77.02/77.07 (E(f6(f11(a2,a1),x6131,x6132,x6133),f6(f11(f10(a2,f9(a7,x6134)),a1),x6131,x6132,x6133))),
% 77.02/77.07 inference(scs_inference,[],[586,2,10])).
% 77.02/77.07 cnf(631,plain,
% 77.02/77.07 (E(f8(f8(a3,x6311),x6312),f8(f8(f8(a3,x6313),x6311),x6312))),
% 77.02/77.07 inference(scs_inference,[],[244,2,4])).
% 77.02/77.07 cnf(632,plain,
% 77.02/77.07 (E(f8(f8(f8(a3,x6321),x6322),x6323),f8(f8(a3,x6322),x6323))),
% 77.02/77.07 inference(scs_inference,[],[631,2])).
% 77.02/77.07 cnf(634,plain,
% 77.02/77.07 (P3(x6341,x6341)),
% 77.02/77.07 inference(rename_variables,[],[34])).
% 77.02/77.07 cnf(635,plain,
% 77.02/77.07 (E(f8(f8(a3,x6351),f9(f8(a3,x6352),x6353)),f8(f8(f8(a3,x6354),x6351),f9(a3,x6353)))),
% 77.02/77.07 inference(scs_inference,[],[244,34,251,631,2,24,3])).
% 77.02/77.07 cnf(640,plain,
% 77.02/77.07 (~P4(f8(f8(f8(a3,x6401),x6402),f9(a3,x6403)))),
% 77.02/77.07 inference(scs_inference,[],[244,34,634,251,631,246,2,24,3,25,29])).
% 77.02/77.07 cnf(644,plain,
% 77.02/77.07 (P3(f12(f10(f8(a3,x6441),f9(x6442,x6443)),x6442),f8(f8(a3,x6444),x6445))),
% 77.02/77.07 inference(scs_inference,[],[244,142,34,634,251,631,246,2,24,3,25,29,44,46])).
% 77.02/77.07 cnf(646,plain,
% 77.02/77.07 (P3(f8(f8(a3,x6461),x6462),f12(f10(f8(a3,x6463),f9(x6464,x6465)),x6464))+P1(f12(f10(f8(a3,x6463),f9(x6464,x6465)),x6464),f8(f8(a3,x6461),x6462))),
% 77.02/77.07 inference(scs_inference,[],[244,142,34,634,251,631,246,2,24,3,25,29,44,46,45])).
% 77.02/77.07 cnf(648,plain,
% 77.02/77.07 (P3(f8(f8(a3,x6481),x6482),f12(f10(f8(a3,x6483),f9(x6484,x6485)),x6484))),
% 77.02/77.07 inference(scs_inference,[],[244,199,646,21])).
% 77.02/77.07 cnf(649,plain,
% 77.02/77.07 (E(f8(f8(f8(a3,x6491),x6492),f9(a3,x6493)),f8(f8(a3,x6492),f9(f8(a3,x6494),x6493)))),
% 77.02/77.07 inference(scs_inference,[],[635,2])).
% 77.02/77.07 cnf(652,plain,
% 77.02/77.07 (P3(a3,f8(f8(a3,x6521),x6522))),
% 77.02/77.07 inference(scs_inference,[],[146,644,635,2,44,46])).
% 77.02/77.07 cnf(655,plain,
% 77.02/77.07 (P3(f8(a3,x6551),f12(f10(f8(f8(a3,x6552),x6551),f9(x6553,x6554)),x6553))),
% 77.02/77.07 inference(scs_inference,[],[244,146,389,644,635,2,44,46,24])).
% 77.02/77.07 cnf(663,plain,
% 77.02/77.07 (P3(f8(f8(a3,x6631),x6632),a3)+P1(a3,f8(f8(a3,x6631),x6632))),
% 77.02/77.07 inference(scs_inference,[],[244,146,389,387,644,251,248,632,635,640,2,44,46,24,3,25,29,45])).
% 77.02/77.07 cnf(665,plain,
% 77.02/77.07 (P3(f8(f8(a3,x6651),x6652),a3)),
% 77.02/77.07 inference(scs_inference,[],[244,102,663,21])).
% 77.02/77.07 cnf(668,plain,
% 77.02/77.07 (P3(f8(a3,x6681),f8(f8(a3,x6682),x6683))),
% 77.02/77.07 inference(scs_inference,[],[648,652,66,44,24])).
% 77.02/77.07 cnf(672,plain,
% 77.02/77.07 (P3(f8(f8(a3,x6721),x6722),f8(a3,x6723))),
% 77.02/77.07 inference(scs_inference,[],[648,652,665,66,649,252,44,24,3,25])).
% 77.02/77.07 cnf(673,plain,
% 77.02/77.07 (~P4(f8(f8(f8(a3,x6731),x6732),x6733))),
% 77.02/77.07 inference(scs_inference,[],[648,652,665,66,649,252,632,246,44,24,3,25,29])).
% 77.02/77.07 cnf(678,plain,
% 77.02/77.07 (E(f8(x6781,f8(a3,x6782)),f8(x6781,f8(f8(a3,x6783),x6782)))),
% 77.02/77.07 inference(scs_inference,[],[244,2,5])).
% 77.02/77.07 cnf(679,plain,
% 77.02/77.07 (E(f8(x6791,f8(f8(a3,x6792),x6793)),f8(x6791,f8(a3,x6793)))),
% 77.02/77.07 inference(scs_inference,[],[678,2])).
% 77.02/77.07 cnf(682,plain,
% 77.02/77.07 (E(f9(f8(a3,x6821),x6822),f9(f8(f8(a3,x6823),x6821),x6822))),
% 77.02/77.07 inference(scs_inference,[],[244,2,6])).
% 77.02/77.07 cnf(683,plain,
% 77.02/77.07 (E(f9(f8(f8(a3,x6831),x6832),x6833),f9(f8(a3,x6832),x6833))),
% 77.02/77.07 inference(scs_inference,[],[682,2])).
% 77.02/77.07 cnf(686,plain,
% 77.02/77.07 (E(f9(f8(a3,x6861),f10(f8(a3,x6862),x6863)),f9(f8(f8(a3,x6864),x6861),f10(a3,x6863)))),
% 77.02/77.07 inference(scs_inference,[],[668,255,682,2,44,3])).
% 77.02/77.07 cnf(701,plain,
% 77.02/77.07 (E(f9(f8(f8(a3,x7011),x7012),f10(f8(a3,x7013),x7014)),f9(f8(a3,x7012),f10(a3,x7014)))),
% 77.02/77.07 inference(scs_inference,[],[665,255,683,686,2,44,3])).
% 77.02/77.07 cnf(715,plain,
% 77.02/77.07 (P1(a1,f11(f10(x7151,f9(x7152,a7)),x7152))),
% 77.02/77.07 inference(scs_inference,[],[30,655,104,701,2,44,21])).
% 77.02/77.07 cnf(729,plain,
% 77.02/77.07 (P2(f10(x7291,f9(f8(a3,x7292),x7293)),f8(f8(a3,x7294),x7295))),
% 77.02/77.07 inference(scs_inference,[],[245,94,23])).
% 77.02/77.07 cnf(731,plain,
% 77.02/77.07 (P3(f8(f8(a3,x7311),x7312),f12(f10(a3,f9(x7313,x7314)),x7313))),
% 77.02/77.07 inference(scs_inference,[],[245,119,94,23,24])).
% 77.02/77.07 cnf(733,plain,
% 77.02/77.07 (P3(f11(f10(x7331,f9(x7332,a3)),x7332),f8(f8(a3,x7333),x7334))),
% 77.02/77.07 inference(scs_inference,[],[245,119,94,129,23,24,25])).
% 77.02/77.07 cnf(737,plain,
% 77.02/77.07 (E(f8(a3,x7371),f8(f8(a3,x7372),x7373))),
% 77.02/77.07 inference(scs_inference,[],[245,119,94,129,39,23,24,25,44,53])).
% 77.02/77.07 cnf(742,plain,
% 77.02/77.07 (E(f8(f8(a3,x7421),x7422),f8(a3,x7423))),
% 77.02/77.07 inference(scs_inference,[],[245,119,94,129,39,23,24,25,44,53,45,2])).
% 77.02/77.07 cnf(746,plain,
% 77.02/77.07 (P3(f12(f10(f8(f8(a3,x7461),x7462),f9(x7463,x7464)),x7463),a3)),
% 77.02/77.07 inference(scs_inference,[],[665,733,85,44,24])).
% 77.02/77.07 cnf(747,plain,
% 77.02/77.07 (E(x7471,f12(f10(x7471,f9(x7472,x7473)),x7472))),
% 77.02/77.07 inference(rename_variables,[],[85])).
% 77.02/77.07 cnf(748,plain,
% 77.02/77.07 (~E(f10(x7481,f9(x7482,x7483)),f12(f10(f8(f8(a3,x7484),x7485),f9(x7486,x7487)),x7486))),
% 77.02/77.07 inference(scs_inference,[],[248,665,733,85,36,44,24,3])).
% 77.02/77.07 cnf(750,plain,
% 77.02/77.07 (P3(f8(a3,x7501),f12(f10(f8(f8(a3,x7502),x7503),f9(x7504,x7505)),x7504))),
% 77.02/77.07 inference(scs_inference,[],[248,668,665,733,85,747,36,44,24,3,25])).
% 77.02/77.07 cnf(755,plain,
% 77.02/77.07 (~P1(f12(f10(f8(f8(a3,x7551),x7552),f9(x7553,x7554)),x7553),f8(a3,x7555))),
% 77.02/77.07 inference(scs_inference,[],[750,44])).
% 77.02/77.07 cnf(757,plain,
% 77.02/77.07 (P3(f12(f10(f8(f8(a3,x7571),x7572),f9(x7573,x7574)),x7573),f8(a3,x7575))),
% 77.02/77.07 inference(scs_inference,[],[750,746,66,44,25])).
% 77.02/77.07 cnf(758,plain,
% 77.02/77.07 (P3(a3,f12(f10(f8(f8(a3,x7581),x7582),f9(x7583,x7584)),x7583))+P1(f12(f10(f8(f8(a3,x7581),x7582),f9(x7583,x7584)),x7583),a3)),
% 77.02/77.07 inference(scs_inference,[],[750,746,66,44,25,45])).
% 77.02/77.07 cnf(766,plain,
% 77.02/77.07 (~E(a2,f8(f8(f8(a3,x7661),x7662),x7663))),
% 77.02/77.07 inference(scs_inference,[],[632,252,3])).
% 77.02/77.07 cnf(768,plain,
% 77.02/77.07 (P3(f8(x7681,f9(f8(a3,x7682),x7683)),f8(x7681,f9(a3,x7683)))),
% 77.02/77.07 inference(scs_inference,[],[250,34,632,252,3,24])).
% 77.02/77.07 cnf(769,plain,
% 77.02/77.07 (P3(x7691,x7691)),
% 77.02/77.07 inference(rename_variables,[],[34])).
% 77.02/77.07 cnf(770,plain,
% 77.02/77.07 (P3(f8(x7701,f9(a3,x7702)),f8(x7701,f9(f8(a3,x7703),x7702)))),
% 77.02/77.07 inference(scs_inference,[],[250,34,769,632,252,3,24,25])).
% 77.02/77.07 cnf(772,plain,
% 77.02/77.07 (~P1(f8(x7721,f9(a3,x7722)),f8(x7721,f9(f8(a3,x7723),x7722)))),
% 77.02/77.07 inference(scs_inference,[],[250,34,769,632,252,3,24,25,44])).
% 77.02/77.07 cnf(774,plain,
% 77.02/77.07 (~P1(f8(x7741,f9(f8(a3,x7742),x7743)),f8(x7741,f9(a3,x7743)))),
% 77.02/77.07 inference(scs_inference,[],[770,44])).
% 77.02/77.07 cnf(777,plain,
% 77.02/77.07 (~E(a2,f12(f10(f8(f8(a3,x7771),x7772),f9(x7773,x7774)),x7773))),
% 77.02/77.07 inference(scs_inference,[],[252,36,3])).
% 77.02/77.07 cnf(780,plain,
% 77.02/77.07 (P3(a3,f12(f10(f8(f8(a3,x7801),x7802),f9(x7803,x7804)),x7803))),
% 77.02/77.07 inference(scs_inference,[],[66,755,758,21])).
% 77.02/77.07 cnf(783,plain,
% 77.02/77.07 (P3(f9(x7831,f10(f8(a3,x7832),x7833)),f9(x7831,f10(a3,x7833)))),
% 77.02/77.07 inference(scs_inference,[],[254,34,780,44,24])).
% 77.02/77.07 cnf(784,plain,
% 77.02/77.07 (P3(x7841,x7841)),
% 77.02/77.07 inference(rename_variables,[],[34])).
% 77.02/77.07 cnf(785,plain,
% 77.02/77.07 (P3(f9(x7851,f10(a3,x7852)),f9(x7851,f10(f8(a3,x7853),x7852)))),
% 77.02/77.07 inference(scs_inference,[],[254,34,784,780,44,24,25])).
% 77.02/77.07 cnf(787,plain,
% 77.02/77.07 (~P1(f9(x7871,f10(a3,x7872)),f9(x7871,f10(f8(a3,x7873),x7872)))),
% 77.02/77.07 inference(scs_inference,[],[783,44])).
% 77.02/77.07 cnf(789,plain,
% 77.02/77.07 (~P1(f9(x7891,f10(f8(a3,x7892),x7893)),f9(x7891,f10(a3,x7893)))),
% 77.02/77.07 inference(scs_inference,[],[785,44])).
% 77.02/77.07 cnf(794,plain,
% 77.02/77.07 (P3(f10(x7941,f6(f8(a3,x7942),x7943,x7944,x7945)),f10(x7941,f6(a3,x7943,x7944,x7945)))),
% 77.02/77.07 inference(scs_inference,[],[257,34,24])).
% 77.02/77.07 cnf(795,plain,
% 77.02/77.07 (P3(x7951,x7951)),
% 77.02/77.07 inference(rename_variables,[],[34])).
% 77.02/77.07 cnf(796,plain,
% 77.02/77.07 (P3(f10(x7961,f6(a3,x7962,x7963,x7964)),f10(x7961,f6(f8(a3,x7965),x7962,x7963,x7964)))),
% 77.02/77.07 inference(scs_inference,[],[257,34,795,24,25])).
% 77.02/77.07 cnf(826,plain,
% 77.02/77.07 (P3(f11(x8261,f6(x8262,x8263,f8(a3,x8264),x8265)),f11(x8261,f6(x8262,x8263,a3,x8265)))),
% 77.02/77.07 inference(scs_inference,[],[263,34,24])).
% 77.02/77.07 cnf(827,plain,
% 77.02/77.07 (P3(x8271,x8271)),
% 77.02/77.07 inference(rename_variables,[],[34])).
% 77.02/77.07 cnf(828,plain,
% 77.02/77.07 (P3(f11(x8281,f6(x8282,x8283,a3,x8284)),f11(x8281,f6(x8282,x8283,f8(a3,x8285),x8284)))),
% 77.02/77.07 inference(scs_inference,[],[263,34,827,24,25])).
% 77.02/77.07 cnf(830,plain,
% 77.02/77.07 (~P1(f11(x8301,f6(x8302,x8303,a3,x8304)),f11(x8301,f6(x8302,x8303,f8(a3,x8305),x8304)))),
% 77.02/77.07 inference(scs_inference,[],[263,34,827,24,25,44])).
% 77.02/77.07 cnf(833,plain,
% 77.02/77.07 (~P1(f11(x8331,f6(x8332,x8333,f8(a3,x8334),x8335)),f11(x8331,f6(x8332,x8333,a3,x8335)))),
% 77.02/77.07 inference(scs_inference,[],[828,44])).
% 77.02/77.07 cnf(843,plain,
% 77.02/77.07 (P3(x8431,x8431)),
% 77.02/77.07 inference(rename_variables,[],[34])).
% 77.02/77.07 cnf(844,plain,
% 77.02/77.07 (P3(f12(f6(x8441,x8442,x8443,a3),x8444),f12(f6(x8441,x8442,x8443,f8(a3,x8445)),x8444))),
% 77.02/77.07 inference(scs_inference,[],[269,34,843,24,25])).
% 77.02/77.07 cnf(849,plain,
% 77.02/77.07 (~P1(f12(f6(x8491,x8492,x8493,f8(a3,x8494)),x8495),f12(f6(x8491,x8492,x8493,a3),x8495))),
% 77.02/77.07 inference(scs_inference,[],[844,44])).
% 77.02/77.07 cnf(883,plain,
% 77.02/77.07 (P3(f12(x8831,f5(f8(a3,x8832),x8833)),f12(x8831,f5(a3,x8833)))),
% 77.02/77.07 inference(scs_inference,[],[279,34,24])).
% 77.02/77.07 cnf(884,plain,
% 77.02/77.07 (P3(x8841,x8841)),
% 77.02/77.07 inference(rename_variables,[],[34])).
% 77.02/77.07 cnf(885,plain,
% 77.02/77.07 (P3(f12(x8851,f5(a3,x8852)),f12(x8851,f5(f8(a3,x8853),x8852)))),
% 77.02/77.07 inference(scs_inference,[],[279,34,884,24,25])).
% 77.02/77.07 cnf(887,plain,
% 77.02/77.07 (~P1(f12(x8871,f5(a3,x8872)),f12(x8871,f5(f8(a3,x8873),x8872)))),
% 77.02/77.07 inference(scs_inference,[],[279,34,884,24,25,44])).
% 77.02/77.07 cnf(890,plain,
% 77.02/77.07 (~P1(f12(x8901,f5(f8(a3,x8902),x8903)),f12(x8901,f5(a3,x8903)))),
% 77.02/77.07 inference(scs_inference,[],[885,44])).
% 77.02/77.07 cnf(913,plain,
% 77.02/77.07 (E(f6(f5(x9131,a3),x9132,x9133,x9134),f6(f5(x9131,f8(a3,x9135)),x9132,x9133,x9134))),
% 77.02/77.07 inference(scs_inference,[],[359,2,10])).
% 77.02/77.07 cnf(916,plain,
% 77.02/77.07 (P3(x9161,x9161)),
% 77.02/77.07 inference(rename_variables,[],[34])).
% 77.02/77.07 cnf(917,plain,
% 77.02/77.07 (P3(f5(x9171,f8(a3,x9172)),f5(x9171,a3))),
% 77.02/77.07 inference(scs_inference,[],[359,34,916,913,2,24,25])).
% 77.02/77.07 cnf(919,plain,
% 77.02/77.07 (~P1(f5(x9191,f8(a3,x9192)),f5(x9191,a3))),
% 77.02/77.07 inference(scs_inference,[],[359,34,916,913,2,24,25,44])).
% 77.02/77.07 cnf(922,plain,
% 77.02/77.07 (~P1(f5(x9221,a3),f5(x9221,f8(a3,x9222)))),
% 77.02/77.07 inference(scs_inference,[],[917,44])).
% 77.02/77.07 cnf(934,plain,
% 77.02/77.07 (E(f8(f5(x9341,a3),x9342),f8(f5(x9341,f8(a3,x9343)),x9342))),
% 77.02/77.07 inference(scs_inference,[],[359,2,4])).
% 77.02/77.07 cnf(935,plain,
% 77.02/77.07 (E(f8(f5(x9351,f8(a3,x9352)),x9353),f8(f5(x9351,a3),x9353))),
% 77.02/77.07 inference(scs_inference,[],[934,2])).
% 77.02/77.07 cnf(1005,plain,
% 77.02/77.07 (P2(f10(x10051,f9(f11(a2,a1),x10052)),f11(f10(a2,f9(a7,x10053)),a1))),
% 77.02/77.07 inference(scs_inference,[],[586,2,47])).
% 77.02/77.07 cnf(1010,plain,
% 77.02/77.07 (~E(f12(f10(a1,f9(x10101,x10102)),x10101),f12(f10(f5(a2,a1),f9(x10103,x10104)),x10103))),
% 77.02/77.07 inference(scs_inference,[],[435,36,2,3])).
% 77.02/77.07 cnf(1072,plain,
% 77.02/77.07 (P3(f10(f8(x10721,a7),f9(x10722,a7)),f8(f10(x10721,f9(x10722,a1)),a7))),
% 77.02/77.07 inference(scs_inference,[],[562,34,25])).
% 77.02/77.07 cnf(1073,plain,
% 77.02/77.07 (P3(x10731,x10731)),
% 77.02/77.07 inference(rename_variables,[],[34])).
% 77.02/77.07 cnf(1074,plain,
% 77.02/77.07 (P3(f8(f10(x10741,f9(x10742,a1)),a7),f10(f8(x10741,a7),f9(x10742,a7)))),
% 77.02/77.07 inference(scs_inference,[],[562,34,1073,25,24])).
% 77.02/77.07 cnf(1087,plain,
% 77.02/77.07 (~E(f9(f5(a2,a1),x10871),f12(f10(f9(a1,x10872),f9(x10873,x10874)),x10873))),
% 77.02/77.07 inference(scs_inference,[],[579,36,3])).
% 77.02/77.07 cnf(1092,plain,
% 77.02/77.07 (~E(f9(a1,x10921),f12(f10(f9(f5(a2,a1),x10922),f9(x10923,x10924)),x10923))),
% 77.02/77.07 inference(scs_inference,[],[583,36,3])).
% 77.02/77.07 cnf(1103,plain,
% 77.02/77.08 (P3(x11031,x11031)),
% 77.02/77.08 inference(rename_variables,[],[34])).
% 77.02/77.08 cnf(1104,plain,
% 77.02/77.08 (P3(f8(f8(a3,x11041),x11042),f8(f8(f8(a3,x11043),x11041),x11042))),
% 77.02/77.08 inference(scs_inference,[],[631,34,1103,24,25])).
% 77.02/77.08 cnf(1111,plain,
% 77.02/77.08 (P3(a3,f8(f8(f8(a3,x11111),x11112),x11113))),
% 77.02/77.08 inference(scs_inference,[],[631,652,1104,44,25])).
% 77.02/77.08 cnf(1118,plain,
% 77.02/77.08 (P3(f8(f8(f8(a3,x11181),x11182),f9(f8(a3,x11183),x11184)),f8(f8(a3,x11182),f9(a3,x11184)))),
% 77.02/77.08 inference(scs_inference,[],[631,768,1111,44,24])).
% 77.02/77.08 cnf(1120,plain,
% 77.02/77.08 (E(f8(f8(a3,x11201),x11202),f8(f8(f8(a3,x11203),x11201),x11202))),
% 77.02/77.08 inference(rename_variables,[],[631])).
% 77.02/77.08 cnf(1121,plain,
% 77.02/77.08 (P3(f8(a3,x11211),f8(f8(f8(a3,x11212),x11213),x11214))),
% 77.02/77.08 inference(scs_inference,[],[631,1120,668,768,1111,44,24,25])).
% 77.02/77.08 cnf(1128,plain,
% 77.02/77.08 (P3(f8(f8(a3,x11281),f9(f8(a3,x11282),x11283)),f8(f8(f8(a3,x11284),x11281),f9(a3,x11283)))),
% 77.02/77.08 inference(scs_inference,[],[631,768,1118,44,25])).
% 77.02/77.08 cnf(1130,plain,
% 77.02/77.08 (E(f8(f8(a3,x11301),x11302),f8(f8(f8(a3,x11303),x11301),x11302))),
% 77.02/77.08 inference(rename_variables,[],[631])).
% 77.02/77.08 cnf(1131,plain,
% 77.02/77.08 (P3(f8(f8(f8(a3,x11311),x11312),x11313),f8(a3,x11314))),
% 77.02/77.08 inference(scs_inference,[],[631,1130,768,672,1118,44,25,24])).
% 77.02/77.08 cnf(1137,plain,
% 77.02/77.08 (P3(f11(f10(x11371,f9(x11372,a3)),x11372),f8(f8(f8(a3,x11373),x11374),f9(a3,x11375)))),
% 77.02/77.08 inference(scs_inference,[],[733,1128,44,46])).
% 77.02/77.08 cnf(1168,plain,
% 77.02/77.08 (P2(f10(x11681,f9(f8(a3,x11682),x11683)),f8(f8(f8(a3,x11684),x11685),f9(a3,x11686)))),
% 77.02/77.08 inference(scs_inference,[],[635,729,23])).
% 77.02/77.08 cnf(1176,plain,
% 77.02/77.08 (E(f8(a3,x11761),f8(f8(f8(a3,x11762),x11763),f9(a3,x11764)))),
% 77.02/77.08 inference(scs_inference,[],[635,731,644,729,39,23,24,25,44,53])).
% 77.02/77.08 cnf(1181,plain,
% 77.02/77.08 (E(f8(f8(f8(a3,x11811),x11812),f9(a3,x11813)),f8(a3,x11814))),
% 77.02/77.08 inference(scs_inference,[],[635,731,644,729,39,23,24,25,44,53,45,2])).
% 77.02/77.08 cnf(1221,plain,
% 77.02/77.08 (P3(f8(f8(a3,x12211),x12212),f11(f10(x12213,f9(x12214,a3)),x12214))),
% 77.02/77.08 inference(scs_inference,[],[665,457,46])).
% 77.02/77.08 cnf(1227,plain,
% 77.02/77.08 (P3(f8(f8(a3,x12271),x12272),f12(f10(f8(f8(a3,x12273),x12274),f9(x12275,x12276)),x12275))),
% 77.02/77.08 inference(scs_inference,[],[665,780,46])).
% 77.02/77.08 cnf(1240,plain,
% 77.02/77.08 (E(f8(f5(x12401,f8(a3,x12402)),f8(a3,x12403)),f8(f5(x12401,a3),f8(f8(a3,x12404),x12403)))),
% 77.02/77.08 inference(scs_inference,[],[678,935,3])).
% 77.02/77.08 cnf(1242,plain,
% 77.02/77.08 (E(f8(x12421,f8(a3,x12422)),f8(x12421,f8(f8(a3,x12423),x12422)))),
% 77.02/77.08 inference(rename_variables,[],[678])).
% 77.02/77.08 cnf(1244,plain,
% 77.02/77.08 (P3(x12441,x12441)),
% 77.02/77.08 inference(rename_variables,[],[34])).
% 77.02/77.08 cnf(1245,plain,
% 77.02/77.08 (P3(f8(x12451,f8(a3,x12452)),f8(x12451,f8(f8(a3,x12453),x12452)))),
% 77.02/77.08 inference(scs_inference,[],[678,1242,34,1244,935,3,24,25])).
% 77.02/77.08 cnf(1247,plain,
% 77.02/77.08 (~P1(f8(x12471,f8(a3,x12472)),f8(x12471,f8(f8(a3,x12473),x12472)))),
% 77.02/77.08 inference(scs_inference,[],[678,1242,34,1244,935,3,24,25,44])).
% 77.02/77.08 cnf(1251,plain,
% 77.02/77.08 (~P1(f8(x12511,f8(f8(a3,x12512),x12513)),f8(x12511,f8(a3,x12513)))),
% 77.02/77.08 inference(scs_inference,[],[1245,1240,2,44])).
% 77.02/77.08 cnf(1331,plain,
% 77.02/77.08 (P3(x13311,x13311)),
% 77.02/77.08 inference(rename_variables,[],[34])).
% 77.02/77.08 cnf(1332,plain,
% 77.02/77.08 (P3(f9(f8(f8(a3,x13321),x13322),x13323),f9(f8(a3,x13322),x13323))),
% 77.02/77.08 inference(scs_inference,[],[682,34,1331,25,24])).
% 77.02/77.08 cnf(1334,plain,
% 77.02/77.08 (~P1(f9(f8(f8(a3,x13341),x13342),x13343),f9(f8(a3,x13342),x13343))),
% 77.02/77.08 inference(scs_inference,[],[682,34,1331,25,24,44])).
% 77.02/77.08 cnf(1337,plain,
% 77.02/77.08 (~P1(f9(f8(a3,x13371),x13372),f9(f8(f8(a3,x13373),x13371),x13372))),
% 77.02/77.08 inference(scs_inference,[],[1332,44])).
% 77.02/77.08 cnf(1380,plain,
% 77.02/77.08 (P2(f10(x13801,f9(a3,x13802)),f8(f8(a3,x13803),x13804))),
% 77.02/77.08 inference(scs_inference,[],[737,144,23])).
% 77.02/77.08 cnf(1386,plain,
% 77.02/77.08 (E(a3,f8(f8(a3,x13861),x13862))),
% 77.02/77.08 inference(scs_inference,[],[737,144,757,39,23,25,44,53])).
% 77.02/77.08 cnf(1389,plain,
% 77.02/77.08 (E(f8(f8(a3,x13891),x13892),a3)),
% 77.02/77.08 inference(scs_inference,[],[737,144,757,39,23,25,44,53,2])).
% 77.02/77.08 cnf(1391,plain,
% 77.02/77.08 (P2(f10(f10(x13911,f9(a3,x13912)),f9(x13913,x13914)),f8(f8(a3,x13915),x13916))),
% 77.02/77.08 inference(scs_inference,[],[737,385,23])).
% 77.02/77.08 cnf(1393,plain,
% 77.02/77.08 (P3(f8(f8(f8(a3,x13931),x13932),x13933),f8(f8(a3,x13934),x13935))),
% 77.02/77.08 inference(scs_inference,[],[737,385,1131,23,25])).
% 77.02/77.08 cnf(1440,plain,
% 77.02/77.08 (P3(f6(f5(x14401,f8(a3,x14402)),x14403,x14404,x14405),f6(f5(x14401,a3),x14403,x14404,x14405))),
% 77.02/77.08 inference(scs_inference,[],[913,34,24])).
% 77.02/77.08 cnf(1441,plain,
% 77.02/77.08 (P3(x14411,x14411)),
% 77.02/77.08 inference(rename_variables,[],[34])).
% 77.02/77.08 cnf(1442,plain,
% 77.02/77.08 (P3(f6(f5(x14421,a3),x14422,x14423,x14424),f6(f5(x14421,f8(a3,x14425)),x14422,x14423,x14424))),
% 77.02/77.08 inference(scs_inference,[],[913,34,1441,24,25])).
% 77.02/77.08 cnf(1444,plain,
% 77.02/77.08 (~P1(f6(f5(x14441,a3),x14442,x14443,x14444),f6(f5(x14441,f8(a3,x14445)),x14442,x14443,x14444))),
% 77.02/77.08 inference(scs_inference,[],[913,34,1441,24,25,44])).
% 77.02/77.08 cnf(1447,plain,
% 77.02/77.08 (~P1(f6(f5(x14471,f8(a3,x14472)),x14473,x14474,x14475),f6(f5(x14471,a3),x14473,x14474,x14475))),
% 77.02/77.08 inference(scs_inference,[],[1442,44])).
% 77.02/77.08 cnf(1458,plain,
% 77.02/77.08 (P3(f8(f5(x14581,f8(a3,x14582)),x14583),f8(f5(x14581,a3),x14583))),
% 77.02/77.08 inference(scs_inference,[],[934,34,24])).
% 77.02/77.08 cnf(1459,plain,
% 77.02/77.08 (P3(x14591,x14591)),
% 77.02/77.08 inference(rename_variables,[],[34])).
% 77.02/77.08 cnf(1460,plain,
% 77.02/77.08 (P3(f8(f5(x14601,a3),x14602),f8(f5(x14601,f8(a3,x14603)),x14602))),
% 77.02/77.08 inference(scs_inference,[],[934,34,1459,24,25])).
% 77.02/77.08 cnf(1509,plain,
% 77.02/77.08 (P2(f10(x15091,f9(a3,x15092)),f8(f8(f8(a3,x15093),x15094),f9(a3,x15095)))),
% 77.02/77.08 inference(scs_inference,[],[1176,144,23])).
% 77.02/77.08 cnf(1513,plain,
% 77.02/77.08 (P3(f8(f8(f8(a3,x15131),x15132),x15133),f8(f8(f8(a3,x15134),x15135),f9(a3,x15136)))),
% 77.02/77.08 inference(scs_inference,[],[1176,144,131,1131,23,24,25])).
% 77.02/77.08 cnf(1517,plain,
% 77.02/77.08 (E(a3,f8(f8(f8(a3,x15171),x15172),f9(a3,x15173)))),
% 77.02/77.08 inference(scs_inference,[],[1176,144,131,1131,39,23,24,25,44,53])).
% 77.02/77.08 cnf(1520,plain,
% 77.02/77.08 (E(f8(f8(f8(a3,x15201),x15202),f9(a3,x15203)),a3)),
% 77.02/77.08 inference(scs_inference,[],[1176,144,131,1131,39,23,24,25,44,53,2])).
% 77.02/77.08 cnf(1523,plain,
% 77.02/77.08 (P2(f10(f10(x15231,f9(a3,x15232)),f9(x15233,x15234)),f8(f8(f8(a3,x15235),x15236),f9(a3,x15237)))),
% 77.02/77.08 inference(scs_inference,[],[1176,385,1513,44,23])).
% 77.02/77.08 cnf(1525,plain,
% 77.02/77.08 (P3(f8(f8(f8(a3,x15251),x15252),f9(a3,x15253)),f8(f8(f8(a3,x15254),x15255),x15256))),
% 77.02/77.08 inference(scs_inference,[],[1176,385,1121,1513,44,23,24])).
% 77.02/77.08 cnf(1530,plain,
% 77.02/77.08 (P2(f10(x15301,f9(a3,x15302)),f8(f8(f8(a3,x15303),x15304),f9(f8(a3,x15305),x15306)))),
% 77.02/77.08 inference(scs_inference,[],[1525,1509,250,44,23])).
% 77.02/77.08 cnf(1534,plain,
% 77.02/77.08 (E(a3,f8(f8(f8(a3,x15341),x15342),f9(f8(a3,x15343),x15344)))),
% 77.02/77.08 inference(scs_inference,[],[1530,39,53])).
% 77.02/77.08 cnf(1538,plain,
% 77.02/77.08 (E(f8(f8(f8(a3,x15381),x15382),f9(f8(a3,x15383),x15384)),a3)),
% 77.02/77.08 inference(scs_inference,[],[1530,39,53,2])).
% 77.02/77.08 cnf(1637,plain,
% 77.02/77.08 (~E(f12(f10(a7,f9(x16371,x16372)),x16371),a1)),
% 77.02/77.08 inference(scs_inference,[],[64,572,21])).
% 77.02/77.08 cnf(1640,plain,
% 77.02/77.08 (~E(f11(f10(x16401,f9(x16402,a7)),x16402),a1)),
% 77.02/77.08 inference(scs_inference,[],[64,715,21])).
% 77.02/77.08 cnf(1650,plain,
% 77.02/77.08 (~E(f12(f10(a7,f9(x16501,x16502)),x16501),a4)),
% 77.02/77.08 inference(scs_inference,[],[83,572,21])).
% 77.02/77.08 cnf(1652,plain,
% 77.02/77.08 (~E(f11(f10(x16521,f9(x16522,a7)),x16522),a4)),
% 77.02/77.08 inference(scs_inference,[],[83,715,21])).
% 77.02/77.08 cnf(1656,plain,
% 77.02/77.08 (P2(f10(x16561,f9(a3,x16562)),f12(f10(f8(f8(a3,x16563),x16564),f9(x16565,x16566)),x16565))),
% 77.02/77.08 inference(scs_inference,[],[85,1380,23])).
% 77.02/77.08 cnf(1658,plain,
% 77.02/77.08 (E(a3,f12(f10(f8(f8(a3,x16581),x16582),f9(x16583,x16584)),x16583))),
% 77.02/77.08 inference(scs_inference,[],[85,1380,39,23,53])).
% 77.02/77.08 cnf(1661,plain,
% 77.02/77.08 (E(f12(f10(f8(f8(a3,x16611),x16612),f9(x16613,x16614)),x16613),a3)),
% 77.02/77.08 inference(scs_inference,[],[85,1380,39,23,53,2])).
% 77.02/77.08 cnf(1662,plain,
% 77.02/77.08 (~P4(f12(f10(f8(f8(a3,x16621),x16622),f9(x16623,x16624)),x16623))),
% 77.02/77.08 inference(scs_inference,[],[85,1380,38,39,23,53,2,29])).
% 77.02/77.08 cnf(1702,plain,
% 77.02/77.08 (~E(f10(f8(a3,x17021),f9(x17022,x17023)),f10(a2,f9(x17022,x17024)))),
% 77.02/77.08 inference(scs_inference,[],[570,16])).
% 77.02/77.08 cnf(1708,plain,
% 77.02/77.08 (E(x17081,f11(f10(x17082,f9(x17083,x17081)),x17083))),
% 77.02/77.08 inference(rename_variables,[],[104])).
% 77.02/77.08 cnf(1709,plain,
% 77.02/77.08 (P5(f10(a2,f9(x17091,x17092)),f11(f10(x17093,f9(x17094,a1)),x17094),f12(f10(f5(a2,a1),f9(x17095,x17096)),x17095))),
% 77.02/77.08 inference(scs_inference,[],[431,104,1708,570,613,469,407,16,274,2,28,27])).
% 77.02/77.08 cnf(1710,plain,
% 77.02/77.08 (E(x17101,f11(f10(x17102,f9(x17103,x17101)),x17103))),
% 77.02/77.08 inference(rename_variables,[],[104])).
% 77.02/77.08 cnf(1711,plain,
% 77.02/77.08 (P3(f11(f10(x17111,f9(x17112,a3)),x17112),f12(f10(a3,f9(x17113,x17114)),x17113))),
% 77.02/77.08 inference(scs_inference,[],[733,431,731,104,1708,570,613,469,407,16,274,2,28,27,46])).
% 77.02/77.08 cnf(1714,plain,
% 77.02/77.08 (~E(f12(f10(a7,f9(x17141,x17142)),x17141),f12(f10(a4,f9(x17143,x17144)),x17143))),
% 77.02/77.08 inference(scs_inference,[],[201,733,431,731,572,104,1708,570,613,469,407,16,274,2,28,27,46,21])).
% 77.02/77.08 cnf(1716,plain,
% 77.02/77.08 (~E(f11(f10(x17161,f9(x17162,a1)),x17162),f12(f10(f5(a2,a1),f9(x17163,x17164)),x17163))),
% 77.02/77.08 inference(scs_inference,[],[201,733,431,731,538,572,104,1708,570,613,469,407,574,16,274,2,28,27,46,21,23])).
% 77.02/77.08 cnf(1718,plain,
% 77.02/77.08 (E(f12(f6(x17181,x17182,x17183,f8(a3,x17184)),f5(f8(a3,x17185),x17186)),f12(f6(x17181,x17182,x17183,f8(a3,x17187)),f5(a3,x17186)))),
% 77.02/77.08 inference(scs_inference,[],[201,733,431,731,538,572,270,287,104,1708,570,613,469,407,574,16,274,2,28,27,46,21,23,3])).
% 77.02/77.08 cnf(1721,plain,
% 77.02/77.08 (P4(f12(f10(f8(f10(x17211,f9(x17212,a1)),a7),f9(x17213,x17214)),x17213))),
% 77.02/77.08 inference(scs_inference,[],[201,733,431,731,538,572,270,287,104,1708,85,570,613,564,469,407,574,16,274,2,28,27,46,21,23,3,29])).
% 77.02/77.08 cnf(1724,plain,
% 77.02/77.08 (E(x17241,f11(f10(x17242,f9(x17243,x17241)),x17243))),
% 77.02/77.08 inference(rename_variables,[],[104])).
% 77.02/77.08 cnf(1725,plain,
% 77.02/77.08 (P3(f11(f10(x17251,f9(x17252,a1)),x17252),f11(f10(x17253,f9(x17254,a7)),x17254))),
% 77.02/77.08 inference(scs_inference,[],[201,206,216,733,431,731,538,572,270,287,104,1708,1710,1724,85,570,613,564,469,407,574,16,274,2,28,27,46,21,23,3,29,25,24])).
% 77.02/77.08 cnf(1727,plain,
% 77.02/77.08 (~E(f8(a3,x17271),a2)),
% 77.02/77.08 inference(scs_inference,[],[201,206,216,733,431,731,538,572,270,287,104,1708,1710,1724,85,570,613,564,469,407,574,16,274,2,28,27,46,21,23,3,29,25,24,8])).
% 77.02/77.08 cnf(1732,plain,
% 77.02/77.08 (P5(a2,a1,f11(f10(x17321,f9(x17322,f5(a2,a1))),x17322))),
% 77.02/77.08 inference(scs_inference,[],[201,206,216,733,431,731,538,572,1640,270,287,104,1708,1710,1724,85,570,613,564,469,407,574,16,274,2,28,27,46,21,23,3,29,25,24,8,44,59,60])).
% 77.02/77.08 cnf(1734,plain,
% 77.02/77.08 (P3(f12(f10(a3,f9(x17341,x17342)),x17341),f11(f10(x17343,f9(x17344,a3)),x17344))+P1(f11(f10(x17343,f9(x17344,a3)),x17344),f12(f10(a3,f9(x17341,x17342)),x17341))),
% 77.02/77.08 inference(scs_inference,[],[201,206,216,733,431,731,538,572,1640,270,287,104,1708,1710,1724,85,570,613,564,469,407,574,16,274,2,28,27,46,21,23,3,29,25,24,8,44,59,60,45])).
% 77.02/77.08 cnf(1736,plain,
% 77.02/77.08 (P3(f12(f10(a3,f9(x17361,x17362)),x17361),f11(f10(x17363,f9(x17364,a3)),x17364))),
% 77.02/77.08 inference(scs_inference,[],[395,37,1734,20])).
% 77.02/77.08 cnf(1740,plain,
% 77.02/77.08 (~P1(f11(f10(x17401,f9(x17402,a7)),x17402),f11(f10(x17403,f9(x17404,a1)),x17404))),
% 77.02/77.08 inference(scs_inference,[],[1725,1714,1718,16,2,44])).
% 77.02/77.08 cnf(1745,plain,
% 77.02/77.08 (~E(f11(f10(x17451,f9(x17452,f5(a2,a1))),x17452),a1)),
% 77.02/77.08 inference(scs_inference,[],[1725,1716,1714,1709,1732,74,1718,16,2,44,59,28])).
% 77.02/77.08 cnf(1746,plain,
% 77.02/77.08 (P3(f12(f10(f8(a3,x17461),f9(x17462,x17463)),x17462),f12(f10(f8(a3,x17464),f9(x17465,x17466)),x17465))),
% 77.02/77.08 inference(scs_inference,[],[109,146,1725,1716,1714,1709,1732,74,1718,16,2,44,59,28,46])).
% 77.02/77.08 cnf(1748,plain,
% 77.02/77.08 (~E(f11(f10(x17481,f9(x17482,a7)),x17482),f12(f10(a4,f9(x17483,x17484)),x17483))),
% 77.02/77.08 inference(scs_inference,[],[201,109,146,715,1725,1716,1714,1709,1732,74,1718,16,2,44,59,28,46,21])).
% 77.02/77.08 cnf(1752,plain,
% 77.02/77.08 (E(f8(x17521,f9(a3,x17522)),f8(x17521,f9(f8(a3,x17523),x17522)))),
% 77.02/77.08 inference(rename_variables,[],[250])).
% 77.02/77.08 cnf(1753,plain,
% 77.02/77.08 (E(f12(f6(x17531,x17532,x17533,a3),f5(f8(a3,x17534),x17535)),f12(f6(x17531,x17532,x17533,a3),f5(f8(a3,x17536),x17535)))),
% 77.02/77.08 inference(scs_inference,[],[201,109,146,715,1168,1725,1716,1714,1709,1732,74,287,281,250,1718,16,2,44,59,28,46,21,23,3])).
% 77.02/77.08 cnf(1760,plain,
% 77.02/77.08 (E(f8(a3,x17601),f8(f8(f8(a3,x17602),x17603),f9(f8(a3,x17604),x17605)))),
% 77.02/77.08 inference(scs_inference,[],[201,214,1137,109,146,715,1168,1725,1716,1714,1709,1732,74,287,281,250,1752,104,1718,39,16,2,44,59,28,46,21,23,3,25,24,53])).
% 77.02/77.08 cnf(1763,plain,
% 77.02/77.08 (P3(f11(f10(x17631,f9(x17632,a7)),x17632),f11(f10(x17633,f9(x17634,a1)),x17634))+P1(f11(f10(x17633,f9(x17634,a1)),x17634),f11(f10(x17631,f9(x17632,a7)),x17632))),
% 77.02/77.08 inference(scs_inference,[],[201,214,1137,109,146,715,1168,1725,1716,1714,1709,1732,74,287,281,250,1752,104,1718,39,16,2,44,59,28,46,21,23,3,25,24,53,45])).
% 77.02/77.08 cnf(1765,plain,
% 77.02/77.08 (P3(f11(f10(x17651,f9(x17652,a7)),x17652),f11(f10(x17653,f9(x17654,a1)),x17654))+~E(f11(f10(x17653,f9(x17654,a1)),x17654),a7)),
% 77.02/77.08 inference(scs_inference,[],[201,214,1137,109,146,460,715,1168,1725,1716,1714,1709,1732,74,287,281,250,1752,104,1718,39,16,2,44,59,28,46,21,23,3,25,24,53,45,20])).
% 77.02/77.08 cnf(1768,plain,
% 77.02/77.08 (~P1(f11(f10(x17681,f9(x17682,a1)),x17682),f11(f10(x17683,f9(x17684,a7)),x17684))+~E(f11(f10(x17681,f9(x17682,a1)),x17682),a7)),
% 77.02/77.08 inference(scs_inference,[],[1765,44])).
% 77.02/77.08 cnf(1769,plain,
% 77.02/77.08 (~E(f10(a1,f9(x17691,x17692)),f10(f5(a2,a1),f9(x17691,x17693)))),
% 77.02/77.08 inference(scs_inference,[],[1010,16])).
% 77.02/77.08 cnf(1774,plain,
% 77.02/77.08 (P3(a1,f11(f10(x17741,f9(f6(x17742,x17743,f8(a3,x17744),x17745),a7)),f6(x17742,x17743,a3,x17745)))),
% 77.02/77.08 inference(scs_inference,[],[206,826,1746,608,1010,16,2,44,46])).
% 77.02/77.08 cnf(1778,plain,
% 77.02/77.08 (P2(f10(f10(x17781,f9(a3,x17782)),f9(x17783,x17784)),f8(f8(f8(a3,x17785),x17786),f9(f8(a3,x17787),x17788)))),
% 77.02/77.08 inference(scs_inference,[],[206,826,1523,1746,250,608,1010,16,2,44,46,23])).
% 77.02/77.08 cnf(1804,plain,
% 77.02/77.08 (~P5(f8(a2,a7),a1,f12(f10(a7,f9(x18041,x18042)),x18041))),
% 77.02/77.08 inference(scs_inference,[],[1760,389,4,5,7,14,15,17,18,19,51])).
% 77.02/77.08 cnf(1807,plain,
% 77.02/77.08 (P5(f10(f10(a2,f9(x18071,x18072)),f9(x18073,x18074)),f12(f10(a1,f9(x18075,x18076)),x18075),f5(a2,a1))),
% 77.02/77.08 inference(scs_inference,[],[1760,448,389,4,5,7,14,15,17,18,19,51,58])).
% 77.02/77.08 cnf(1820,plain,
% 77.02/77.08 (P2(f10(x18201,f9(f8(f8(a3,x18202),x18203),x18204)),a3)),
% 77.02/77.08 inference(scs_inference,[],[1778,1760,1391,448,1389,105,389,4,5,7,14,15,17,18,19,51,58,10,11,12,13,54,49,48,6,47])).
% 77.02/77.08 cnf(1825,plain,
% 77.02/77.08 (~E(f10(f5(a2,a1),f9(x18251,x18252)),f10(a1,f9(x18251,x18253)))),
% 77.02/77.08 inference(scs_inference,[],[1769,1778,1760,1391,448,1389,105,389,4,5,7,14,15,17,18,19,51,58,10,11,12,13,54,49,48,6,47,8,9,16,2])).
% 77.02/77.08 cnf(1826,plain,
% 77.02/77.08 (~P3(a7,a1)),
% 77.02/77.08 inference(scs_inference,[],[30,1769,1778,1760,1391,448,1389,105,389,4,5,7,14,15,17,18,19,51,58,10,11,12,13,54,49,48,6,47,8,9,16,2,44])).
% 77.02/77.08 cnf(1828,plain,
% 77.02/77.08 (P5(f10(x18281,f9(a3,a3)),f8(f8(a3,x18282),x18283),f8(f8(a3,x18282),x18283))),
% 77.02/77.08 inference(scs_inference,[],[30,1769,1778,1760,1386,1391,448,1389,105,389,4,5,7,14,15,17,18,19,51,58,10,11,12,13,54,49,48,6,47,8,9,16,2,44,52])).
% 77.02/77.08 cnf(1830,plain,
% 77.02/77.08 (E(f11(f10(f10(f10(x18301,f9(a3,x18302)),f9(x18303,x18304)),f9(a2,x18305)),f8(a3,x18306)),f11(f10(f10(x18301,f9(a3,x18302)),f9(x18303,x18304)),f8(a3,x18306)))),
% 77.02/77.08 inference(scs_inference,[],[30,1769,1778,1760,1386,1391,448,1389,105,385,72,389,4,5,7,14,15,17,18,19,51,58,10,11,12,13,54,49,48,6,47,8,9,16,2,44,52,50])).
% 77.02/77.08 cnf(1831,plain,
% 77.02/77.08 (P2(f10(f10(x18311,f9(a3,x18312)),f9(x18313,x18314)),f8(a3,x18315))),
% 77.02/77.08 inference(rename_variables,[],[385])).
% 77.02/77.08 cnf(1836,plain,
% 77.02/77.08 (~P5(f12(f10(f8(f8(a3,x18361),x18362),f9(x18363,x18364)),x18363),x18365,x18366)),
% 77.02/77.08 inference(scs_inference,[],[30,1769,1778,1760,1386,1661,1391,448,1389,105,385,1831,72,389,40,4,5,7,14,15,17,18,19,51,58,10,11,12,13,54,49,48,6,47,8,9,16,2,44,52,50,56,26])).
% 77.02/77.08 cnf(1838,plain,
% 77.02/77.08 (E(f5(f12(f10(f8(a3,x18381),f9(x18382,x18383)),x18382),x18384),f5(a3,x18384))),
% 77.02/77.08 inference(rename_variables,[],[560])).
% 77.02/77.08 cnf(1839,plain,
% 77.02/77.08 (~P1(f5(x18391,f8(a3,x18392)),f5(x18391,a3))),
% 77.02/77.08 inference(rename_variables,[],[919])).
% 77.02/77.08 cnf(1840,plain,
% 77.02/77.08 (~P5(f10(a3,f9(a1,x18401)),f5(a2,a1),x18402)),
% 77.02/77.08 inference(scs_inference,[],[30,581,919,1769,560,1778,1760,1386,1661,1391,448,1389,105,385,1831,72,389,40,4,5,7,14,15,17,18,19,51,58,10,11,12,13,54,49,48,6,47,8,9,16,2,44,52,50,56,26,20,60])).
% 77.02/77.08 cnf(1843,plain,
% 77.02/77.08 (~P5(f10(f8(a2,a7),f9(x18431,a1)),a1,f11(f10(x18432,f9(x18433,a7)),x18433))),
% 77.02/77.08 inference(scs_inference,[],[30,581,919,1769,243,187,560,1778,1760,1386,1661,1391,448,1389,105,385,1831,72,389,40,4,5,7,14,15,17,18,19,51,58,10,11,12,13,54,49,48,6,47,8,9,16,2,44,52,50,56,26,20,60,59])).
% 77.02/77.08 cnf(1844,plain,
% 77.02/77.08 (~P5(f8(a2,a7),a1,f11(f10(x18441,f9(x18442,a7)),x18442))),
% 77.02/77.08 inference(rename_variables,[],[243])).
% 77.02/77.08 cnf(1846,plain,
% 77.02/77.08 (~P2(f12(f10(f8(f8(a3,x18461),x18462),f9(x18463,x18464)),x18463),x18465)),
% 77.02/77.08 inference(scs_inference,[],[30,581,919,1769,243,187,560,1778,1760,1386,1661,1391,448,1389,105,385,1831,72,389,40,39,4,5,7,14,15,17,18,19,51,58,10,11,12,13,54,49,48,6,47,8,9,16,2,44,52,50,56,26,20,60,59,22])).
% 77.02/77.08 cnf(1847,plain,
% 77.02/77.08 (~P5(f8(a2,a7),f11(f10(x18471,f9(x18472,a1)),x18472),f11(f10(x18473,f9(x18474,a7)),x18474))),
% 77.02/77.08 inference(scs_inference,[],[30,581,919,1769,243,1844,187,560,1778,1760,1386,1661,1391,448,1389,105,385,1831,72,389,40,37,39,4,5,7,14,15,17,18,19,51,58,10,11,12,13,54,49,48,6,47,8,9,16,2,44,52,50,56,26,20,60,59,22,27])).
% 77.02/77.08 cnf(1849,plain,
% 77.02/77.08 (~P2(f10(f10(a3,f9(a1,x18491)),f9(a1,x18492)),f12(f10(f5(a2,a1),f9(x18493,x18494)),x18493))),
% 77.02/77.08 inference(scs_inference,[],[30,581,919,1769,243,1844,187,575,560,1778,1760,1386,1661,1391,448,1389,105,574,385,1831,72,389,40,37,39,4,5,7,14,15,17,18,19,51,58,10,11,12,13,54,49,48,6,47,8,9,16,2,44,52,50,56,26,20,60,59,22,27,53])).
% 77.02/77.08 cnf(1850,plain,
% 77.02/77.08 (~P2(f10(a3,f9(a1,x18501)),f12(f10(f5(a2,a1),f9(x18502,x18503)),x18502))),
% 77.02/77.08 inference(rename_variables,[],[574])).
% 77.02/77.08 cnf(1855,plain,
% 77.02/77.08 (~P3(f11(f10(x18551,f9(x18552,a7)),x18552),a1)),
% 77.02/77.08 inference(scs_inference,[],[30,581,919,1769,243,1844,187,575,560,1778,1760,1386,1661,1391,448,1389,457,105,574,264,385,1831,72,389,40,37,39,4,5,7,14,15,17,18,19,51,58,10,11,12,13,54,49,48,6,47,8,9,16,2,44,52,50,56,26,20,60,59,22,27,53,28,46])).
% 77.02/77.08 cnf(1864,plain,
% 77.02/77.08 (~E(f12(f10(f8(f10(x18641,f9(x18642,a1)),a7),f9(x18643,x18644)),x18643),f8(a3,x18645))),
% 77.02/77.08 inference(scs_inference,[],[30,581,919,1839,1769,243,1844,187,575,560,1838,1721,1778,1760,1386,1661,1391,448,1389,73,289,457,105,574,1850,264,385,1831,72,389,40,37,39,4,5,7,14,15,17,18,19,51,58,10,11,12,13,54,49,48,6,47,8,9,16,2,44,52,50,56,26,20,60,59,22,27,53,28,46,21,23,29])).
% 77.02/77.08 cnf(1880,plain,
% 77.02/77.08 (E(f10(f8(x18801,a4),f9(x18802,x18803)),f8(f10(x18801,f9(x18802,x18803)),a4))),
% 77.02/77.08 inference(scs_inference,[],[33,54])).
% 77.02/77.08 cnf(1882,plain,
% 77.02/77.08 (E(f8(a3,x18821),f8(f8(f8(f8(a3,x18822),x18823),f9(a3,x18824)),x18821))),
% 77.02/77.08 inference(scs_inference,[],[1517,33,54,4])).
% 77.02/77.08 cnf(1883,plain,
% 77.02/77.08 (E(f8(x18831,a3),f8(x18831,f8(f8(f8(a3,x18832),x18833),f9(a3,x18834))))),
% 77.02/77.08 inference(scs_inference,[],[1517,33,54,4,5])).
% 77.02/77.08 cnf(1884,plain,
% 77.02/77.08 (E(f12(x18841,a3),f12(x18841,f8(f8(f8(a3,x18842),x18843),f9(a3,x18844))))),
% 77.02/77.08 inference(scs_inference,[],[1517,33,54,4,5,17])).
% 77.02/77.08 cnf(1887,plain,
% 77.02/77.08 (E(f6(a3,x18871,x18872,x18873),f6(f8(f8(f8(a3,x18874),x18875),f9(a3,x18876)),x18871,x18872,x18873))),
% 77.02/77.08 inference(scs_inference,[],[1820,1517,33,54,4,5,17,49,10])).
% 77.02/77.08 cnf(1888,plain,
% 77.02/77.08 (P5(f10(f10(x18881,f9(a3,a3)),f9(x18882,x18883)),f8(f8(a3,x18884),x18885),f8(f8(a3,x18884),x18885))),
% 77.02/77.08 inference(scs_inference,[],[1828,1820,1517,33,54,4,5,17,49,10,58])).
% 77.02/77.08 cnf(1890,plain,
% 77.02/77.08 (E(f6(x18901,x18902,x18903,a3),f6(x18901,x18902,x18903,f8(f8(f8(a3,x18904),x18905),f9(a3,x18906))))),
% 77.02/77.08 inference(scs_inference,[],[1828,1820,1517,33,54,4,5,17,49,10,58,13])).
% 77.02/77.08 cnf(1891,plain,
% 77.02/77.08 (E(f9(x18911,a3),f9(x18911,f8(f8(f8(a3,x18912),x18913),f9(a3,x18914))))),
% 77.02/77.08 inference(scs_inference,[],[1828,1820,1517,33,54,4,5,17,49,10,58,13,7])).
% 77.02/77.08 cnf(1892,plain,
% 77.02/77.08 (P5(f10(x18921,f9(a3,x18922)),f8(f8(a3,x18923),x18924),f5(f10(x18921,f9(a3,x18922)),f8(f8(a3,x18923),x18924)))),
% 77.02/77.08 inference(scs_inference,[],[1828,1820,1517,1380,33,54,4,5,17,49,10,58,13,7,48])).
% 77.02/77.08 cnf(1894,plain,
% 77.02/77.08 (E(f6(x18941,a3,x18942,x18943),f6(x18941,f8(f8(f8(a3,x18944),x18945),f9(a3,x18946)),x18942,x18943))),
% 77.02/77.08 inference(scs_inference,[],[1828,1820,1517,1380,33,54,4,5,17,49,10,58,13,7,48,11])).
% 77.02/77.08 cnf(1895,plain,
% 77.02/77.08 (E(f6(x18951,x18952,a3,x18953),f6(x18951,x18952,f8(f8(f8(a3,x18954),x18955),f9(a3,x18956)),x18953))),
% 77.02/77.08 inference(scs_inference,[],[1828,1820,1517,1380,33,54,4,5,17,49,10,58,13,7,48,11,12])).
% 77.02/77.08 cnf(1896,plain,
% 77.02/77.08 (E(f5(a3,x18961),f5(f8(f8(f8(a3,x18962),x18963),f9(a3,x18964)),x18961))),
% 77.02/77.08 inference(scs_inference,[],[1828,1820,1517,1380,33,54,4,5,17,49,10,58,13,7,48,11,12,18])).
% 77.02/77.08 cnf(1897,plain,
% 77.02/77.08 (E(f5(x18971,a3),f5(x18971,f8(f8(f8(a3,x18972),x18973),f9(a3,x18974))))),
% 77.02/77.08 inference(scs_inference,[],[1828,1820,1517,1380,33,54,4,5,17,49,10,58,13,7,48,11,12,18,19])).
% 77.02/77.08 cnf(1898,plain,
% 77.02/77.08 (E(f11(a3,x18981),f11(f8(f8(f8(a3,x18982),x18983),f9(a3,x18984)),x18981))),
% 77.02/77.08 inference(scs_inference,[],[1828,1820,1517,1380,33,54,4,5,17,49,10,58,13,7,48,11,12,18,19,14])).
% 77.02/77.08 cnf(1899,plain,
% 77.02/77.08 (E(f9(a3,x18991),f9(f8(f8(f8(a3,x18992),x18993),f9(a3,x18994)),x18991))),
% 77.02/77.08 inference(scs_inference,[],[1828,1820,1517,1380,33,54,4,5,17,49,10,58,13,7,48,11,12,18,19,14,6])).
% 77.02/77.08 cnf(1901,plain,
% 77.02/77.08 (P2(f10(x19011,f9(f8(f8(a3,x19012),x19013),x19014)),f8(a3,x19015))),
% 77.02/77.08 inference(scs_inference,[],[1828,1820,1517,1380,742,33,54,4,5,17,49,10,58,13,7,48,11,12,18,19,14,6,15,47])).
% 77.02/77.08 cnf(1903,plain,
% 77.02/77.08 (E(f10(x19031,a3),f10(x19031,f8(f8(f8(a3,x19032),x19033),f9(a3,x19034))))),
% 77.02/77.08 inference(scs_inference,[],[1828,1820,1517,1380,742,33,54,4,5,17,49,10,58,13,7,48,11,12,18,19,14,6,15,47,9])).
% 77.02/77.08 cnf(1904,plain,
% 77.02/77.08 (E(f10(a3,x19041),f10(f8(f8(f8(a3,x19042),x19043),f9(a3,x19044)),x19041))),
% 77.02/77.08 inference(scs_inference,[],[1828,1820,1517,1380,742,33,54,4,5,17,49,10,58,13,7,48,11,12,18,19,14,6,15,47,9,8])).
% 77.02/77.08 cnf(1905,plain,
% 77.02/77.08 (E(f12(a3,x19051),f12(f8(f8(f8(a3,x19052),x19053),f9(a3,x19054)),x19051))),
% 77.02/77.08 inference(scs_inference,[],[1828,1820,1517,1380,742,33,54,4,5,17,49,10,58,13,7,48,11,12,18,19,14,6,15,47,9,8,16])).
% 77.02/77.08 cnf(1906,plain,
% 77.02/77.08 (~E(f11(f10(x19061,f9(x19062,a1)),x19062),f5(a2,a1))),
% 77.02/77.08 inference(scs_inference,[],[1828,451,1820,1517,1380,742,33,54,4,5,17,49,10,58,13,7,48,11,12,18,19,14,6,15,47,9,8,16,2])).
% 77.02/77.08 cnf(1907,plain,
% 77.02/77.08 (~P3(f12(f10(a7,f9(x19071,x19072)),x19071),a1)),
% 77.02/77.08 inference(scs_inference,[],[1828,451,1820,1517,1380,742,572,33,54,4,5,17,49,10,58,13,7,48,11,12,18,19,14,6,15,47,9,8,16,2,44])).
% 77.02/77.08 cnf(1909,plain,
% 77.02/77.08 (E(f11(f10(f10(x19091,f9(a7,x19092)),f9(a1,x19093)),a7),f11(f10(x19091,f9(a7,x19092)),a7))),
% 77.02/77.08 inference(scs_inference,[],[1828,451,1820,1517,1380,742,67,572,33,63,54,4,5,17,49,10,58,13,7,48,11,12,18,19,14,6,15,47,9,8,16,2,44,50])).
% 77.02/77.08 cnf(1912,plain,
% 77.02/77.08 (P5(f10(x19121,f9(a3,a3)),f8(f8(f8(a3,x19122),x19123),f9(a3,x19124)),f8(f8(f8(a3,x19122),x19123),f9(a3,x19124)))),
% 77.02/77.08 inference(scs_inference,[],[1828,451,1820,1517,1380,742,67,572,33,63,54,4,5,17,49,10,58,13,7,48,11,12,18,19,14,6,15,47,9,8,16,2,44,50,52])).
% 77.02/77.08 cnf(1914,plain,
% 77.02/77.08 (~P5(f8(f8(f8(a3,x19141),x19142),f9(f8(a3,x19143),x19144)),x19145,x19146)),
% 77.02/77.08 inference(scs_inference,[],[1828,451,1820,1517,1538,1380,742,67,572,33,40,63,54,4,5,17,49,10,58,13,7,48,11,12,18,19,14,6,15,47,9,8,16,2,44,50,52,26])).
% 77.02/77.08 cnf(1915,plain,
% 77.02/77.08 (~P5(f10(f10(a3,f9(a1,x19151)),f9(a1,x19152)),f5(a2,a1),x19153)),
% 77.02/77.08 inference(scs_inference,[],[1840,1828,451,1820,1517,1538,581,1380,742,67,572,33,40,63,54,4,5,17,49,10,58,13,7,48,11,12,18,19,14,6,15,47,9,8,16,2,44,50,52,26,60])).
% 77.02/77.08 cnf(1918,plain,
% 77.02/77.08 (~P5(f10(a3,f9(a1,x19181)),f5(a2,a1),x19182)),
% 77.02/77.08 inference(rename_variables,[],[1840])).
% 77.02/77.08 cnf(1920,plain,
% 77.02/77.08 (~P1(f11(f10(f10(f10(x19201,f9(a3,x19202)),f9(f8(a3,x19203),a3)),f9(a2,x19204)),f8(a3,x19203)),f8(a3,x19205))),
% 77.02/77.08 inference(scs_inference,[],[1840,197,1828,451,1820,1830,1517,1538,581,1380,742,67,572,33,40,63,54,4,5,17,49,10,58,13,7,48,11,12,18,19,14,6,15,47,9,8,16,2,44,50,52,26,60,59,20])).
% 77.02/77.08 cnf(1921,plain,
% 77.02/77.08 (E(f11(f10(f10(f10(x19211,f9(a3,x19212)),f9(x19213,x19214)),f9(a2,x19215)),f8(a3,x19216)),f11(f10(f10(x19211,f9(a3,x19212)),f9(x19213,x19214)),f8(a3,x19216)))),
% 77.02/77.08 inference(rename_variables,[],[1830])).
% 77.02/77.08 cnf(1923,plain,
% 77.02/77.08 (~P2(f8(f8(f8(a3,x19231),x19232),f9(f8(a3,x19233),x19234)),x19235)),
% 77.02/77.08 inference(scs_inference,[],[1840,197,1828,451,1820,1830,1517,1538,581,1380,742,67,572,33,40,63,39,54,4,5,17,49,10,58,13,7,48,11,12,18,19,14,6,15,47,9,8,16,2,44,50,52,26,60,59,20,22])).
% 77.02/77.08 cnf(1924,plain,
% 77.02/77.08 (~P5(f10(a3,f9(a1,x19241)),f11(f10(x19242,f9(x19243,f5(a2,a1))),x19243),x19244)),
% 77.02/77.08 inference(scs_inference,[],[1840,1918,197,1828,451,1820,1830,1517,1538,581,1380,742,67,572,33,40,37,63,39,54,4,5,17,49,10,58,13,7,48,11,12,18,19,14,6,15,47,9,8,16,2,44,50,52,26,60,59,20,22,27])).
% 77.02/77.08 cnf(1925,plain,
% 77.02/77.08 (E(f11(f10(x19251,f9(x19252,x19253)),x19252),x19253)),
% 77.02/77.08 inference(rename_variables,[],[37])).
% 77.02/77.08 cnf(1926,plain,
% 77.02/77.08 (~P2(f10(f10(f10(a3,f9(a1,x19261)),f9(a1,x19262)),f9(a1,x19263)),f12(f10(f5(a2,a1),f9(x19264,x19265)),x19264))),
% 77.02/77.08 inference(scs_inference,[],[1840,1918,197,1828,451,1849,1820,1830,1517,1538,581,575,1380,742,67,572,33,40,37,63,39,54,4,5,17,49,10,58,13,7,48,11,12,18,19,14,6,15,47,9,8,16,2,44,50,52,26,60,59,20,22,27,53])).
% 77.02/77.08 cnf(1931,plain,
% 77.02/77.08 (E(f11(f10(f10(f10(x19311,f9(a3,x19312)),f9(x19313,x19314)),f9(a2,x19315)),f8(a3,x19316)),f11(f10(f10(x19311,f9(a3,x19312)),f9(x19313,x19314)),f8(a3,x19316)))),
% 77.02/77.08 inference(rename_variables,[],[1830])).
% 77.02/77.08 cnf(1938,plain,
% 77.02/77.08 (~E(f8(f10(x19381,f9(x19382,a7)),a1),f12(f10(f8(a3,x19383),f9(x19384,x19385)),x19384))),
% 77.02/77.08 inference(scs_inference,[],[1840,1918,197,1828,90,451,849,1843,1849,1753,1711,1736,1820,1830,1921,1517,1538,581,232,575,1380,742,67,572,33,40,37,63,39,54,4,5,17,49,10,58,13,7,48,11,12,18,19,14,6,15,47,9,8,16,2,44,50,52,26,60,59,20,22,27,53,28,46,21,29])).
% 77.02/77.08 cnf(1939,plain,
% 77.02/77.08 (E(f11(f10(f10(f10(x19391,f9(a3,x19392)),f9(f8(a3,x19393),x19394)),f9(a2,x19395)),f8(a3,x19393)),x19394)),
% 77.02/77.08 inference(scs_inference,[],[1840,1918,197,1828,90,451,849,1843,1849,1753,1711,1736,1820,1830,1921,1931,1517,1538,581,232,575,1380,742,67,572,33,40,37,1925,63,39,54,4,5,17,49,10,58,13,7,48,11,12,18,19,14,6,15,47,9,8,16,2,44,50,52,26,60,59,20,22,27,53,28,46,21,29,3])).
% 77.02/77.08 cnf(1940,plain,
% 77.02/77.08 (E(f11(f10(f10(f10(x19401,f9(a3,x19402)),f9(x19403,x19404)),f9(a2,x19405)),f8(a3,x19406)),f11(f10(f10(x19401,f9(a3,x19402)),f9(x19403,x19404)),f8(a3,x19406)))),
% 77.02/77.08 inference(rename_variables,[],[1830])).
% 77.02/77.08 cnf(1941,plain,
% 77.02/77.08 (E(f11(f10(x19411,f9(x19412,x19413)),x19412),x19413)),
% 77.02/77.08 inference(rename_variables,[],[37])).
% 77.02/77.08 cnf(1942,plain,
% 77.02/77.08 (~P3(a7,f11(f10(x19421,f9(x19422,a1)),x19422))),
% 77.02/77.08 inference(scs_inference,[],[1826,1840,1918,197,1828,90,451,849,1843,1849,1753,1711,1736,1820,1830,1921,1931,1517,1538,581,232,575,1380,742,67,572,33,40,37,1925,1941,63,39,54,4,5,17,49,10,58,13,7,48,11,12,18,19,14,6,15,47,9,8,16,2,44,50,52,26,60,59,20,22,27,53,28,46,21,29,3,25])).
% 77.02/77.08 cnf(1944,plain,
% 77.02/77.08 (~P3(f11(f10(f10(f10(x19441,f9(a3,x19442)),f9(f8(a3,x19443),a7)),f9(a2,x19444)),f8(a3,x19443)),a1)),
% 77.02/77.08 inference(scs_inference,[],[1826,1840,1918,197,1828,90,451,1855,849,1843,1849,1753,1711,1736,1820,1830,1921,1931,1940,1517,1538,581,232,575,1380,742,67,572,33,40,37,1925,1941,63,39,54,4,5,17,49,10,58,13,7,48,11,12,18,19,14,6,15,47,9,8,16,2,44,50,52,26,60,59,20,22,27,53,28,46,21,29,3,25,24])).
% 77.02/77.08 cnf(1956,plain,
% 77.02/77.08 (E(f10(f8(x19561,f8(a3,x19562)),f9(x19563,a3)),f8(f10(x19561,f9(x19563,a3)),f8(a3,x19562)))),
% 77.02/77.08 inference(scs_inference,[],[92,54])).
% 77.02/77.08 cnf(1958,plain,
% 77.02/77.08 (P3(a1,f11(f10(f10(f10(x19581,f9(a3,x19582)),f9(f8(a3,x19583),a7)),f9(a2,x19584)),f8(a3,x19583)))),
% 77.02/77.08 inference(scs_inference,[],[1944,92,54,42])).
% 77.02/77.08 cnf(1962,plain,
% 77.02/77.08 (P5(f10(f10(f10(x19621,f9(a3,a3)),f9(x19622,x19623)),f9(x19624,x19625)),f8(f8(a3,x19626),x19627),f8(f8(a3,x19626),x19627))),
% 77.02/77.08 inference(scs_inference,[],[1888,1944,1658,92,54,42,4,10,58])).
% 77.02/77.08 cnf(1982,plain,
% 77.02/77.08 (E(f10(a3,x19821),f10(f12(f10(f8(f8(a3,x19822),x19823),f9(x19824,x19825)),x19824),x19821))),
% 77.02/77.08 inference(scs_inference,[],[1888,1887,1901,1944,1658,94,92,54,42,4,10,58,5,49,48,11,12,17,14,19,13,18,47,7,6,15,9,8])).
% 77.02/77.08 cnf(1984,plain,
% 77.02/77.08 (~E(a4,f11(f10(x19841,f9(x19842,a7)),x19842))),
% 77.02/77.08 inference(scs_inference,[],[1652,1888,1887,1901,1944,1658,94,92,54,42,4,10,58,5,49,48,11,12,17,14,19,13,18,47,7,6,15,9,8,16,2])).
% 77.02/77.08 cnf(1985,plain,
% 77.02/77.08 (P5(f10(x19851,f9(f8(a3,x19852),f8(a3,x19852))),f8(a3,x19853),f8(a3,x19853))),
% 77.02/77.08 inference(scs_inference,[],[1652,1888,1887,1901,1944,1658,99,94,92,54,42,4,10,58,5,49,48,11,12,17,14,19,13,18,47,7,6,15,9,8,16,2,52])).
% 77.02/77.08 cnf(1987,plain,
% 77.02/77.08 (~P5(f11(f10(f10(f10(x19871,f9(a3,x19872)),f9(f8(a3,x19873),a2)),f9(a2,x19874)),f8(a3,x19873)),a1,a1)),
% 77.02/77.08 inference(scs_inference,[],[1652,1888,1887,1901,1944,1658,99,1939,94,74,92,54,42,4,10,58,5,49,48,11,12,17,14,19,13,18,47,7,6,15,9,8,16,2,52,26])).
% 77.02/77.08 cnf(1989,plain,
% 77.02/77.08 (~P5(f10(f8(a2,a7),f9(x19891,a1)),a1,f12(f10(a7,f9(x19892,x19893)),x19892))),
% 77.02/77.08 inference(scs_inference,[],[1804,1652,88,1888,1887,1901,1944,1658,99,1939,94,74,92,54,42,4,10,58,5,49,48,11,12,17,14,19,13,18,47,7,6,15,9,8,16,2,52,26,59])).
% 77.02/77.08 cnf(1992,plain,
% 77.02/77.08 (~P5(f10(f12(f10(f8(f8(a3,x19921),x19922),f9(x19923,x19924)),x19923),f9(f8(a3,x19925),x19926)),a2,x19927)),
% 77.02/77.08 inference(scs_inference,[],[1804,1652,88,1888,1836,1887,1901,1944,1658,99,1727,1939,94,74,92,54,42,4,10,58,5,49,48,11,12,17,14,19,13,18,47,7,6,15,9,8,16,2,52,26,59,60])).
% 77.02/77.08 cnf(1995,plain,
% 77.02/77.08 (~P1(f6(f5(x19951,f8(a3,x19952)),x19953,x19954,a3),f6(f5(x19951,a3),x19953,x19954,f8(f8(f8(a3,x19955),x19956),f9(a3,x19957))))),
% 77.02/77.08 inference(scs_inference,[],[1804,1652,88,1447,1888,1836,1887,1890,1901,1944,1658,99,1727,1939,94,74,92,54,42,4,10,58,5,49,48,11,12,17,14,19,13,18,47,7,6,15,9,8,16,2,52,26,59,60,20])).
% 77.02/77.08 cnf(1996,plain,
% 77.02/77.08 (E(f6(x19961,x19962,x19963,a3),f6(x19961,x19962,x19963,f8(f8(f8(a3,x19964),x19965),f9(a3,x19966))))),
% 77.02/77.08 inference(rename_variables,[],[1890])).
% 77.02/77.08 cnf(1998,plain,
% 77.02/77.08 (~P2(f8(f8(a3,x19981),x19982),x19983)),
% 77.02/77.08 inference(scs_inference,[],[1804,1652,88,1447,1888,1836,1887,1890,1901,1944,1658,99,1727,1939,94,1389,74,92,39,54,42,4,10,58,5,49,48,11,12,17,14,19,13,18,47,7,6,15,9,8,16,2,52,26,59,60,20,22])).
% 77.02/77.08 cnf(2001,plain,
% 77.02/77.08 (~P2(f10(f8(f8(f8(a3,x20011),x20012),f9(f8(a3,x20013),x20014)),f9(f8(a3,x20015),x20016)),a2)),
% 77.02/77.08 inference(scs_inference,[],[1915,1804,1652,88,1447,1888,1836,1923,1887,1890,1901,1944,1658,99,1727,1939,94,1389,74,92,39,36,54,42,4,10,58,5,49,48,11,12,17,14,19,13,18,47,7,6,15,9,8,16,2,52,26,59,60,20,22,27,53])).
% 77.02/77.08 cnf(2004,plain,
% 77.02/77.08 (~P3(f11(f10(x20041,f9(x20042,a7)),x20042),f11(f10(x20043,f9(x20044,a1)),x20044))),
% 77.02/77.08 inference(scs_inference,[],[1915,1804,1652,1942,88,1447,1888,1836,1923,1887,1890,1901,1944,1658,99,1727,1939,94,1389,74,457,92,39,36,54,42,4,10,58,5,49,48,11,12,17,14,19,13,18,47,7,6,15,9,8,16,2,52,26,59,60,20,22,27,53,46])).
% 77.02/77.08 cnf(2009,plain,
% 77.02/77.08 (~E(f12(f10(f10(f5(a2,a1),f9(x20091,x20092)),f9(x20093,x20094)),x20093),f10(a1,f9(x20091,x20095)))),
% 77.02/77.08 inference(scs_inference,[],[1915,1825,1804,1652,1942,88,1447,1888,1836,1923,1887,1890,1901,1944,1658,99,1727,408,1939,94,1389,74,457,92,85,39,36,54,42,4,10,58,5,49,48,11,12,17,14,19,13,18,47,7,6,15,9,8,16,2,52,26,59,60,20,22,27,53,46,21,3])).
% 77.02/77.08 cnf(2011,plain,
% 77.02/77.08 (~E(f8(f10(x20111,f9(x20112,a1)),a7),f8(f8(f8(a3,x20113),x20114),x20115))),
% 77.02/77.08 inference(scs_inference,[],[1915,1825,673,1804,1652,1942,88,1447,1888,1836,1923,1887,1890,1901,1944,1658,99,1727,408,564,1939,94,1389,74,457,92,85,39,36,54,42,4,10,58,5,49,48,11,12,17,14,19,13,18,47,7,6,15,9,8,16,2,52,26,59,60,20,22,27,53,46,21,3,29])).
% 77.02/77.08 cnf(2012,plain,
% 77.02/77.08 (P3(f6(f5(x20121,f8(a3,x20122)),x20123,x20124,a3),f6(f5(x20121,a3),x20123,x20124,f8(f8(f8(a3,x20125),x20126),f9(a3,x20127))))),
% 77.02/77.08 inference(scs_inference,[],[1915,1825,673,1804,1652,1942,88,1447,1888,1836,1923,1887,1890,1996,1901,1944,1440,1658,99,1727,408,564,1939,94,1389,74,457,92,85,39,36,54,42,4,10,58,5,49,48,11,12,17,14,19,13,18,47,7,6,15,9,8,16,2,52,26,59,60,20,22,27,53,46,21,3,29,25])).
% 77.02/77.08 cnf(2013,plain,
% 77.02/77.08 (E(f6(x20131,x20132,x20133,a3),f6(x20131,x20132,x20133,f8(f8(f8(a3,x20134),x20135),f9(a3,x20136))))),
% 77.02/77.08 inference(rename_variables,[],[1890])).
% 77.02/77.08 cnf(2014,plain,
% 77.02/77.08 (P3(f6(f5(x20141,f8(a3,x20142)),x20143,x20144,x20145),f6(f5(x20141,a3),x20143,x20144,x20145))),
% 77.02/77.08 inference(rename_variables,[],[1440])).
% 77.02/77.08 cnf(2015,plain,
% 77.02/77.08 (P3(f6(f5(x20151,f8(a3,x20152)),x20153,x20154,f8(f8(f8(a3,x20155),x20156),f9(a3,x20157))),f6(f5(x20151,a3),x20153,x20154,a3))),
% 77.02/77.08 inference(scs_inference,[],[1915,1825,673,1804,1652,1942,88,1447,1888,1836,1923,1887,1890,1996,2013,1901,1944,1440,2014,1658,99,1727,408,564,1939,94,1389,74,457,92,85,39,36,54,42,4,10,58,5,49,48,11,12,17,14,19,13,18,47,7,6,15,9,8,16,2,52,26,59,60,20,22,27,53,46,21,3,29,25,24])).
% 77.02/77.08 cnf(2018,plain,
% 77.02/77.08 (P1(f11(f10(x20181,f9(x20182,a1)),x20182),f11(f10(x20183,f9(x20184,a7)),x20184))),
% 77.02/77.08 inference(scs_inference,[],[1915,1825,673,1804,1652,1942,88,1447,1888,1836,1923,1887,1890,1996,2013,1901,1944,1440,2014,1658,99,1727,408,564,1939,94,1389,74,457,92,85,39,36,54,42,4,10,58,5,49,48,11,12,17,14,19,13,18,47,7,6,15,9,8,16,2,52,26,59,60,20,22,27,53,46,21,3,29,25,24,1763])).
% 77.02/77.08 cnf(2033,plain,
% 77.02/77.08 (E(f10(f8(x20331,x20332),f9(x20333,x20332)),f8(f10(x20331,f9(x20333,x20332)),x20332))),
% 77.02/77.08 inference(scs_inference,[],[34,54])).
% 77.02/77.08 cnf(2037,plain,
% 77.02/77.08 (P2(f10(f10(x20371,f9(a3,x20372)),f9(x20373,x20374)),f12(f10(f8(f8(a3,x20375),x20376),f9(x20377,x20378)),x20377))),
% 77.02/77.08 inference(scs_inference,[],[1534,1656,34,54,4,5,49])).
% 77.02/77.08 cnf(2039,plain,
% 77.02/77.08 (P5(f10(f10(x20391,f9(f8(a3,x20392),f8(a3,x20392))),f9(x20393,x20394)),f8(a3,x20395),f8(a3,x20395))),
% 77.02/77.08 inference(scs_inference,[],[1985,1534,1656,34,54,4,5,49,58])).
% 77.02/77.08 cnf(2056,plain,
% 77.02/77.08 (E(f10(a3,x20561),f10(f8(f8(f8(a3,x20562),x20563),f9(f8(a3,x20564),x20565)),x20561))),
% 77.02/77.08 inference(scs_inference,[],[1985,1894,1534,1656,453,34,54,4,5,49,58,48,17,10,18,47,13,14,19,11,12,7,6,15,8])).
% 77.02/77.08 cnf(2059,plain,
% 77.02/77.08 (~E(f12(f10(a4,f9(x20591,x20592)),x20591),a7)),
% 77.02/77.08 inference(scs_inference,[],[1985,156,1894,1534,1656,453,34,54,4,5,49,58,48,17,10,18,47,13,14,19,11,12,7,6,15,8,9,16,2])).
% 77.02/77.08 cnf(2063,plain,
% 77.02/77.08 (E(f10(f8(x20631,f8(a3,x20632)),f9(x20633,a3)),f8(f10(x20631,f9(x20633,a3)),f8(a3,x20632)))),
% 77.02/77.08 inference(rename_variables,[],[1956])).
% 77.02/77.08 cnf(2065,plain,
% 77.02/77.08 (~P5(f10(f8(f8(f8(a3,x20651),x20652),f9(f8(a3,x20653),x20654)),f9(x20655,a1)),x20656,f5(a2,a1))),
% 77.02/77.08 inference(scs_inference,[],[1985,156,1956,1914,1894,1912,1534,1656,169,581,453,34,54,4,5,49,58,48,17,10,18,47,13,14,19,11,12,7,6,15,8,9,16,2,52,26,59])).
% 77.02/77.08 cnf(2069,plain,
% 77.02/77.08 (~P5(f8(a2,a7),f11(f10(x20691,f9(x20692,a1)),x20692),f11(f10(x20693,f9(x20694,a7)),x20694))),
% 77.02/77.08 inference(rename_variables,[],[1847])).
% 77.02/77.08 cnf(2071,plain,
% 77.02/77.08 (~P1(f10(f8(x20711,f8(a3,x20712)),f9(x20713,a3)),f8(f10(x20711,f9(x20713,a3)),f8(f8(a3,x20714),x20712)))),
% 77.02/77.08 inference(scs_inference,[],[1985,156,1956,2063,1914,1247,1894,1912,1847,1534,1656,140,169,581,453,34,54,4,5,49,58,48,17,10,18,47,13,14,19,11,12,7,6,15,8,9,16,2,52,26,59,60,20])).
% 77.02/77.08 cnf(2072,plain,
% 77.02/77.08 (E(f10(f8(x20721,f8(a3,x20722)),f9(x20723,a3)),f8(f10(x20721,f9(x20723,a3)),f8(a3,x20722)))),
% 77.02/77.08 inference(rename_variables,[],[1956])).
% 77.02/77.08 cnf(2074,plain,
% 77.02/77.08 (~P2(f11(f10(f10(f10(x20741,f9(a3,x20742)),f9(f8(a3,x20743),a3)),f9(a2,x20744)),f8(a3,x20743)),x20745)),
% 77.02/77.08 inference(scs_inference,[],[1985,156,1956,2063,1914,1247,1894,1912,1847,1534,1656,140,169,581,1939,453,39,34,54,4,5,49,58,48,17,10,18,47,13,14,19,11,12,7,6,15,8,9,16,2,52,26,59,60,20,22])).
% 77.02/77.08 cnf(2075,plain,
% 77.02/77.08 (E(f11(f10(f10(f10(x20751,f9(a3,x20752)),f9(f8(a3,x20753),x20754)),f9(a2,x20755)),f8(a3,x20753)),x20754)),
% 77.02/77.08 inference(rename_variables,[],[1939])).
% 77.02/77.08 cnf(2078,plain,
% 77.02/77.08 (E(f11(f10(f10(x20781,f9(a7,x20782)),f9(a1,x20783)),a7),f11(f10(x20781,f9(a7,x20782)),a7))),
% 77.02/77.08 inference(rename_variables,[],[1909])).
% 77.02/77.08 cnf(2085,plain,
% 77.02/77.08 (~P1(f8(a3,x20851),f11(f10(f10(f10(x20852,f9(a3,x20853)),f9(f8(a3,x20854),a3)),f9(a2,x20855)),f8(a3,x20854)))),
% 77.02/77.08 inference(scs_inference,[],[135,1985,156,1956,2063,1914,1247,1894,1912,1958,1847,2069,1909,1458,1534,1656,140,1944,1460,169,581,1939,2075,453,39,34,54,4,5,49,58,48,17,10,18,47,13,14,19,11,12,7,6,15,8,9,16,2,52,26,59,60,20,22,27,46,45,21])).
% 77.02/77.08 cnf(2091,plain,
% 77.02/77.08 (~P3(f11(f10(x20911,f9(x20912,a7)),x20912),f11(f10(f10(x20913,f9(a7,a1)),f9(a1,x20914)),a7))),
% 77.02/77.08 inference(scs_inference,[],[135,1985,156,1956,2063,2072,1662,541,1914,1247,1894,1912,1958,2004,1847,2069,1909,2078,1458,1534,1656,140,1944,1460,169,581,232,1939,2075,453,39,34,54,4,5,49,58,48,17,10,18,47,13,14,19,11,12,7,6,15,8,9,16,2,52,26,59,60,20,22,27,46,45,21,3,29,25])).
% 77.02/77.08 cnf(2092,plain,
% 77.02/77.08 (~P3(f11(f10(x20921,f9(x20922,a7)),x20922),f11(f10(x20923,f9(x20924,a1)),x20924))),
% 77.02/77.08 inference(rename_variables,[],[2004])).
% 77.02/77.08 cnf(2093,plain,
% 77.02/77.08 (E(f11(f10(f10(x20931,f9(a7,x20932)),f9(a1,x20933)),a7),f11(f10(x20931,f9(a7,x20932)),a7))),
% 77.02/77.08 inference(rename_variables,[],[1909])).
% 77.02/77.08 cnf(2094,plain,
% 77.02/77.08 (~P3(f11(f10(f10(x20941,f9(a7,a7)),f9(a1,x20942)),a7),f11(f10(x20943,f9(x20944,a1)),x20944))),
% 77.02/77.08 inference(scs_inference,[],[135,1985,156,1956,2063,2072,1662,541,1914,1247,1894,1912,1958,2004,2092,1847,2069,1909,2078,2093,1458,1534,1656,140,1944,1460,169,581,232,1939,2075,453,39,34,54,4,5,49,58,48,17,10,18,47,13,14,19,11,12,7,6,15,8,9,16,2,52,26,59,60,20,22,27,46,45,21,3,29,25,24])).
% 77.02/77.08 cnf(2096,plain,
% 77.02/77.08 (E(f11(f10(f10(x20961,f9(a7,x20962)),f9(a1,x20963)),a7),f11(f10(x20961,f9(a7,x20962)),a7))),
% 77.02/77.08 inference(rename_variables,[],[1909])).
% 77.02/77.08 cnf(2099,plain,
% 77.02/77.08 (P3(f11(f10(f10(x20991,f9(a7,a1)),f9(a1,x20992)),a7),f11(f10(x20993,f9(x20994,a7)),x20994))),
% 77.02/77.08 inference(scs_inference,[],[135,1985,156,1956,2063,2072,1662,541,1914,1247,1894,1912,1958,2004,2092,2018,1847,2069,1909,2078,2093,1458,1534,1656,140,1944,1460,169,581,232,1939,2075,453,39,34,54,4,5,49,58,48,17,10,18,47,13,14,19,11,12,7,6,15,8,9,16,2,52,26,59,60,20,22,27,46,45,21,3,29,25,24,1768,42])).
% 77.02/77.08 cnf(2101,plain,
% 77.02/77.08 (~P2(f10(f8(f8(a3,x21011),x21012),f9(a4,x21013)),f11(f10(x21014,f9(x21015,a7)),x21015))),
% 77.02/77.08 inference(scs_inference,[],[135,1998,1985,1984,156,1956,2063,2072,1662,541,1914,1247,1894,1912,1958,2004,2092,2018,1847,2069,1909,2078,2093,1458,1534,1656,140,1944,1460,169,581,232,1939,2075,453,39,34,54,4,5,49,58,48,17,10,18,47,13,14,19,11,12,7,6,15,8,9,16,2,52,26,59,60,20,22,27,46,45,21,3,29,25,24,1768,42,53])).
% 77.02/77.08 cnf(2104,plain,
% 77.02/77.08 (~P2(f10(f8(f8(a3,x21041),x21042),f9(a4,x21043)),f11(f10(f10(x21044,f9(a7,a7)),f9(a1,x21045)),a7))),
% 77.02/77.08 inference(scs_inference,[],[135,1998,1985,1984,156,1956,2063,2072,1662,541,1914,1247,1894,1912,1958,2004,2092,2018,1847,2069,1909,2078,2093,2096,1458,1534,1656,140,1944,1460,169,581,232,1939,2075,453,39,34,54,4,5,49,58,48,17,10,18,47,13,14,19,11,12,7,6,15,8,9,16,2,52,26,59,60,20,22,27,46,45,21,3,29,25,24,1768,42,53,23])).
% 77.02/77.08 cnf(2116,plain,
% 77.02/77.08 (P5(f10(x21161,f9(a3,x21162)),f8(a3,x21163),f5(f10(x21161,f9(a3,x21162)),f8(a3,x21163)))),
% 77.02/77.08 inference(scs_inference,[],[2094,144,42,48])).
% 77.02/77.08 cnf(2118,plain,
% 77.02/77.08 (E(f8(a3,x21181),f8(f8(f8(a3,x21182),x21183),x21181))),
% 77.02/77.08 inference(scs_inference,[],[2094,1386,144,42,48,4])).
% 77.02/77.08 cnf(2119,plain,
% 77.02/77.08 (E(f8(x21191,a3),f8(x21191,f8(f8(a3,x21192),x21193)))),
% 77.02/77.08 inference(scs_inference,[],[2094,1386,144,42,48,4,5])).
% 77.02/77.08 cnf(2122,plain,
% 77.02/77.08 (P5(f10(f10(f10(x21221,f9(f8(a3,x21222),f8(a3,x21222))),f9(x21223,x21224)),f9(x21225,x21226)),f8(a3,x21227),f8(a3,x21227))),
% 77.02/77.08 inference(scs_inference,[],[2039,2037,2094,1386,144,42,48,4,5,49,58])).
% 77.02/77.08 cnf(2126,plain,
% 77.02/77.08 (E(f6(x21261,x21262,x21263,a3),f6(x21261,x21262,x21263,f8(f8(a3,x21264),x21265)))),
% 77.02/77.08 inference(scs_inference,[],[2039,1895,2037,2094,1386,144,42,48,4,5,49,58,47,13])).
% 77.02/77.08 cnf(2127,plain,
% 77.02/77.08 (E(f12(x21271,a3),f12(x21271,f8(f8(a3,x21272),x21273)))),
% 77.02/77.08 inference(scs_inference,[],[2039,1895,2037,2094,1386,144,42,48,4,5,49,58,47,13,17])).
% 77.02/77.08 cnf(2128,plain,
% 77.02/77.08 (E(f6(a3,x21281,x21282,x21283),f6(f8(f8(a3,x21284),x21285),x21281,x21282,x21283))),
% 77.02/77.08 inference(scs_inference,[],[2039,1895,2037,2094,1386,144,42,48,4,5,49,58,47,13,17,10])).
% 77.02/77.08 cnf(2129,plain,
% 77.02/77.08 (E(f6(x21291,x21292,a3,x21293),f6(x21291,x21292,f8(f8(a3,x21294),x21295),x21293))),
% 77.02/77.08 inference(scs_inference,[],[2039,1895,2037,2094,1386,144,42,48,4,5,49,58,47,13,17,10,12])).
% 77.02/77.08 cnf(2130,plain,
% 77.02/77.08 (E(f11(a3,x21301),f11(f8(f8(a3,x21302),x21303),x21301))),
% 77.02/77.08 inference(scs_inference,[],[2039,1895,2037,2094,1386,144,42,48,4,5,49,58,47,13,17,10,12,14])).
% 77.02/77.08 cnf(2131,plain,
% 77.02/77.08 (E(f6(x21311,a3,x21312,x21313),f6(x21311,f8(f8(a3,x21314),x21315),x21312,x21313))),
% 77.02/77.08 inference(scs_inference,[],[2039,1895,2037,2094,1386,144,42,48,4,5,49,58,47,13,17,10,12,14,11])).
% 77.02/77.08 cnf(2132,plain,
% 77.02/77.08 (E(f5(x21321,a3),f5(x21321,f8(f8(a3,x21322),x21323)))),
% 77.02/77.08 inference(scs_inference,[],[2039,1895,2037,2094,1386,144,42,48,4,5,49,58,47,13,17,10,12,14,11,19])).
% 77.02/77.08 cnf(2133,plain,
% 77.02/77.08 (E(f5(a3,x21331),f5(f8(f8(a3,x21332),x21333),x21331))),
% 77.02/77.08 inference(scs_inference,[],[2039,1895,2037,2094,1386,144,42,48,4,5,49,58,47,13,17,10,12,14,11,19,18])).
% 77.02/77.08 cnf(2134,plain,
% 77.02/77.08 (E(f9(x21341,a3),f9(x21341,f8(f8(a3,x21342),x21343)))),
% 77.02/77.08 inference(scs_inference,[],[2039,1895,2037,2094,1386,144,42,48,4,5,49,58,47,13,17,10,12,14,11,19,18,7])).
% 77.02/77.08 cnf(2135,plain,
% 77.02/77.08 (E(f9(a3,x21351),f9(f8(f8(a3,x21352),x21353),x21351))),
% 77.02/77.08 inference(scs_inference,[],[2039,1895,2037,2094,1386,144,42,48,4,5,49,58,47,13,17,10,12,14,11,19,18,7,6])).
% 77.02/77.08 cnf(2136,plain,
% 77.02/77.08 (E(f11(x21361,a3),f11(x21361,f8(f8(a3,x21362),x21363)))),
% 77.02/77.08 inference(scs_inference,[],[2039,1895,2037,2094,1386,144,42,48,4,5,49,58,47,13,17,10,12,14,11,19,18,7,6,15])).
% 77.02/77.08 cnf(2137,plain,
% 77.02/77.08 (E(f10(a3,x21371),f10(f8(f8(a3,x21372),x21373),x21371))),
% 77.02/77.08 inference(scs_inference,[],[2039,1895,2037,2094,1386,144,42,48,4,5,49,58,47,13,17,10,12,14,11,19,18,7,6,15,8])).
% 77.02/77.08 cnf(2138,plain,
% 77.02/77.08 (E(f10(x21381,a3),f10(x21381,f8(f8(a3,x21382),x21383)))),
% 77.02/77.08 inference(scs_inference,[],[2039,1895,2037,2094,1386,144,42,48,4,5,49,58,47,13,17,10,12,14,11,19,18,7,6,15,8,9])).
% 77.02/77.08 cnf(2139,plain,
% 77.02/77.08 (E(f12(a3,x21391),f12(f8(f8(a3,x21392),x21393),x21391))),
% 77.02/77.08 inference(scs_inference,[],[2039,1895,2037,2094,1386,144,42,48,4,5,49,58,47,13,17,10,12,14,11,19,18,7,6,15,8,9,16])).
% 77.02/77.08 cnf(2140,plain,
% 77.02/77.08 (~E(f12(f10(a3,f9(x21401,x21402)),x21401),a2)),
% 77.02/77.08 inference(scs_inference,[],[165,2039,1895,2037,2094,1386,144,42,48,4,5,49,58,47,13,17,10,12,14,11,19,18,7,6,15,8,9,16,2])).
% 77.02/77.08 cnf(2143,plain,
% 77.02/77.08 (~P5(f10(a3,f9(x21431,a1)),x21432,f5(a2,a1))),
% 77.02/77.08 inference(scs_inference,[],[165,2039,1895,2065,2037,2094,2056,1386,742,144,42,48,4,5,49,58,47,13,17,10,12,14,11,19,18,7,6,15,8,9,16,2,52,26])).
% 77.02/77.08 cnf(2144,plain,
% 77.02/77.08 (~P5(f10(f8(f8(f8(a3,x21441),x21442),f9(f8(a3,x21443),x21444)),f9(x21445,a1)),x21446,f5(a2,a1))),
% 77.02/77.08 inference(rename_variables,[],[2065])).
% 77.02/77.08 cnf(2145,plain,
% 77.02/77.08 (E(f10(a3,x21451),f10(f8(f8(f8(a3,x21452),x21453),f9(f8(a3,x21454),x21455)),x21451))),
% 77.02/77.08 inference(rename_variables,[],[2056])).
% 77.02/77.08 cnf(2146,plain,
% 77.02/77.08 (~P5(f10(f10(f8(a2,a7),f9(x21461,a1)),f9(x21462,a1)),a1,f12(f10(a7,f9(x21463,x21464)),x21463))),
% 77.02/77.08 inference(scs_inference,[],[165,2039,1895,1989,2065,2037,2094,2056,88,1386,742,144,42,48,4,5,49,58,47,13,17,10,12,14,11,19,18,7,6,15,8,9,16,2,52,26,59])).
% 77.02/77.08 cnf(2147,plain,
% 77.02/77.08 (~P5(f10(f8(a2,a7),f9(x21471,a1)),a1,f12(f10(a7,f9(x21472,x21473)),x21472))),
% 77.02/77.08 inference(rename_variables,[],[1989])).
% 77.02/77.08 cnf(2149,plain,
% 77.02/77.08 (~P5(f10(f10(f8(f8(f8(a3,x21491),x21492),f9(f8(a3,x21493),x21494)),f9(x21495,a1)),f9(a2,x21496)),a3,f5(a2,a1))),
% 77.02/77.08 inference(scs_inference,[],[165,2039,1895,1989,2065,2144,2037,2094,2056,88,1386,742,68,144,42,48,4,5,49,58,47,13,17,10,12,14,11,19,18,7,6,15,8,9,16,2,52,26,59,60])).
% 77.02/77.08 cnf(2152,plain,
% 77.02/77.08 (~P2(f10(f10(f8(f8(a3,x21521),x21522),f9(a4,x21523)),f9(a1,x21524)),f11(f10(x21525,f9(x21526,a7)),x21526))),
% 77.02/77.08 inference(scs_inference,[],[165,2039,1895,1989,2065,2144,2101,2037,2094,2056,187,88,1386,742,68,144,42,48,4,5,49,58,47,13,17,10,12,14,11,19,18,7,6,15,8,9,16,2,52,26,59,60,53])).
% 77.02/77.08 cnf(2153,plain,
% 77.02/77.08 (~P2(f10(f8(f8(a3,x21531),x21532),f9(a4,x21533)),f11(f10(x21534,f9(x21535,a7)),x21535))),
% 77.02/77.08 inference(rename_variables,[],[2101])).
% 77.02/77.08 cnf(2156,plain,
% 77.02/77.08 (E(f6(x21561,x21562,a3,x21563),f6(x21561,x21562,f8(f8(f8(a3,x21564),x21565),f9(a3,x21566)),x21563))),
% 77.02/77.08 inference(rename_variables,[],[1895])).
% 77.02/77.08 cnf(2157,plain,
% 77.02/77.08 (~P1(f6(f5(x21571,a3),x21572,x21573,x21574),f6(f5(x21571,f8(a3,x21575)),x21572,x21573,x21574))),
% 77.02/77.08 inference(rename_variables,[],[1444])).
% 77.02/77.08 cnf(2158,plain,
% 77.02/77.08 (~P2(f10(a3,f9(f8(a3,x21581),x21582)),a2)),
% 77.02/77.08 inference(scs_inference,[],[165,2039,1444,1895,1989,2065,2144,2101,2037,2094,2001,2056,2145,187,88,1386,742,68,144,42,48,4,5,49,58,47,13,17,10,12,14,11,19,18,7,6,15,8,9,16,2,52,26,59,60,53,20,22])).
% 77.02/77.08 cnf(2162,plain,
% 77.02/77.08 (~P5(f10(f8(a2,a7),f9(x21621,a1)),a1,f12(f10(a7,f9(x21622,x21623)),x21622))),
% 77.02/77.08 inference(rename_variables,[],[1989])).
% 77.02/77.08 cnf(2165,plain,
% 77.02/77.08 (~P3(f12(f10(a7,f9(f5(f8(a3,x21651),x21652),x21653)),f5(a3,x21652)),a1)),
% 77.02/77.08 inference(scs_inference,[],[165,1907,2039,1444,1895,1989,2147,2162,2065,2144,2101,2037,2094,2001,2056,2145,883,187,88,1386,742,68,289,144,37,42,48,4,5,49,58,47,13,17,10,12,14,11,19,18,7,6,15,8,9,16,2,52,26,59,60,53,20,22,28,27,46])).
% 77.02/77.08 cnf(2175,plain,
% 77.02/77.08 (~P2(f10(f8(f8(a3,x21751),x21752),f9(a4,x21753)),a7)),
% 77.02/77.08 inference(scs_inference,[],[165,1907,2039,1444,2157,1895,2156,1989,2147,2162,2065,2144,2101,2153,2037,1995,2012,2094,2001,2056,2145,883,187,88,1386,742,68,289,144,37,104,42,48,4,5,49,58,47,13,17,10,12,14,11,19,18,7,6,15,8,9,16,2,52,26,59,60,53,20,22,28,27,46,45,21,23])).
% 77.02/77.08 cnf(2177,plain,
% 77.02/77.08 (~E(f12(f10(a2,f9(x21771,x21772)),x21771),f12(f10(a3,f9(x21773,x21774)),x21773))),
% 77.02/77.08 inference(scs_inference,[],[165,1907,2039,1444,2157,1895,2156,1989,2147,2162,2065,2144,2101,2153,2037,1995,2012,2094,2001,2056,2145,883,187,88,1386,742,68,289,144,37,85,104,42,48,4,5,49,58,47,13,17,10,12,14,11,19,18,7,6,15,8,9,16,2,52,26,59,60,53,20,22,28,27,46,45,21,23,3])).
% 77.02/77.08 cnf(2181,plain,
% 77.02/77.08 (E(f10(f8(x21811,x21812),f9(x21813,x21812)),f8(f10(x21811,f9(x21813,x21812)),x21812))),
% 77.02/77.08 inference(rename_variables,[],[2033])).
% 77.02/77.08 cnf(2184,plain,
% 77.02/77.08 (~P3(a7,f5(a2,a1))+P3(a7,f6(a2,a1,f5(a2,a1),a7))),
% 77.02/77.08 inference(scs_inference,[],[30,165,1907,2039,2033,2181,1444,2157,1895,2156,1989,2147,2162,2065,2144,2101,2153,2037,1995,2012,2094,2001,2056,2145,1072,883,90,187,88,111,1386,1074,742,410,68,289,144,37,85,104,42,48,4,5,49,58,47,13,17,10,12,14,11,19,18,7,6,15,8,9,16,2,52,26,59,60,53,20,22,28,27,46,45,21,23,3,29,25,24,61])).
% 77.02/77.08 cnf(2192,plain,
% 77.02/77.08 (P5(f10(f10(x21921,f9(a3,x21922)),f9(x21923,x21924)),f8(a3,x21925),f5(f10(f10(x21921,f9(a3,x21922)),f9(x21923,x21924)),f8(a3,x21925)))),
% 77.02/77.08 inference(scs_inference,[],[2165,385,42,48])).
% 77.02/77.08 cnf(2194,plain,
% 77.02/77.08 (P5(f10(f10(x21941,f9(a3,x21942)),f9(x21943,x21944)),f8(a3,x21945),f5(f10(x21941,f9(a3,x21942)),f8(a3,x21945)))),
% 77.02/77.08 inference(scs_inference,[],[2116,2165,385,42,48,58])).
% 77.02/77.08 cnf(2200,plain,
% 77.02/77.08 (P2(f10(x22001,f9(f6(x22002,x22003,x22004,a3),x22005)),f6(x22002,x22003,x22004,f8(f8(a3,x22006),x22007)))),
% 77.02/77.08 inference(scs_inference,[],[2116,2126,2165,1005,385,42,48,58,4,49,5,47])).
% 77.02/77.08 cnf(2216,plain,
% 77.02/77.08 (~E(a4,f12(f10(a7,f9(x22161,x22162)),x22161))),
% 77.02/77.08 inference(scs_inference,[],[2116,2126,1650,2165,1005,385,42,48,58,4,49,5,47,12,14,19,11,13,18,10,17,7,15,6,8,16,9,2])).
% 77.02/77.08 cnf(2217,plain,
% 77.02/77.08 (E(f11(f10(f10(x22171,f9(a4,x22172)),f9(a7,x22173)),a4),f11(f10(x22171,f9(a4,x22172)),a4))),
% 77.02/77.08 inference(scs_inference,[],[2116,2126,1650,2165,1005,117,385,63,42,48,58,4,49,5,47,12,14,19,11,13,18,10,17,7,15,6,8,16,9,2,50])).
% 77.02/77.08 cnf(2222,plain,
% 77.02/77.08 (~P5(f10(f10(f10(f8(a2,a7),f9(x22221,a1)),f9(x22222,a1)),f9(x22223,a1)),a1,f12(f10(a7,f9(x22224,x22225)),x22224))),
% 77.02/77.08 inference(scs_inference,[],[2116,2126,1650,2146,2165,1005,88,117,1389,385,63,42,48,58,4,49,5,47,12,14,19,11,13,18,10,17,7,15,6,8,16,9,2,50,52,59])).
% 77.02/77.08 cnf(2225,plain,
% 77.02/77.08 (~P5(f8(a3,f9(f8(a3,x22251),x22252)),x22253,x22254)),
% 77.02/77.08 inference(scs_inference,[],[2116,2126,2118,1650,2146,2165,1005,1914,88,117,1389,385,63,42,48,58,4,49,5,47,12,14,19,11,13,18,10,17,7,15,6,8,16,9,2,50,52,59,26])).
% 77.02/77.08 cnf(2231,plain,
% 77.02/77.08 (~P1(f5(x22311,a3),f5(x22311,f8(a3,x22312)))),
% 77.02/77.08 inference(rename_variables,[],[922])).
% 77.02/77.08 cnf(2232,plain,
% 77.02/77.08 (E(f5(a3,x22321),f5(f8(f8(a3,x22322),x22323),x22321))),
% 77.02/77.08 inference(rename_variables,[],[2133])).
% 77.02/77.08 cnf(2234,plain,
% 77.02/77.08 (E(f11(f10(f10(f10(x22341,f9(a3,x22342)),f9(f8(a3,x22343),x22344)),f9(a2,x22345)),f8(a3,x22343)),x22344)),
% 77.02/77.08 inference(rename_variables,[],[1939])).
% 77.02/77.08 cnf(2239,plain,
% 77.02/77.08 (E(f11(f10(f10(f10(x22391,f9(a3,x22392)),f9(f8(a3,x22393),x22394)),f9(a2,x22395)),f8(a3,x22393)),x22394)),
% 77.02/77.08 inference(rename_variables,[],[1939])).
% 77.02/77.08 cnf(2245,plain,
% 77.02/77.08 (~P1(f5(f8(f8(a3,x22451),x22452),a3),f5(a3,f8(a3,x22453)))),
% 77.02/77.08 inference(scs_inference,[],[922,2231,2175,2116,2126,2118,2133,2232,2137,1650,2146,2074,2165,1393,1221,1005,1914,88,117,1939,2234,1389,74,385,63,42,48,58,4,49,5,47,12,14,19,11,13,18,10,17,7,15,6,8,16,9,2,50,52,59,26,53,20,28,22,27,46,45,21])).
% 77.02/77.08 cnf(2249,plain,
% 77.02/77.08 (E(f11(f10(f10(f10(x22491,f9(a3,x22492)),f9(f8(a3,x22493),x22494)),f9(a2,x22495)),f8(a3,x22493)),x22494)),
% 77.02/77.08 inference(rename_variables,[],[1939])).
% 77.02/77.08 cnf(2250,plain,
% 77.02/77.08 (E(f6(a3,x22501,x22502,a3),f6(f8(f8(a3,x22503),x22504),x22501,x22502,f8(f8(a3,x22505),x22506)))),
% 77.02/77.08 inference(scs_inference,[],[922,2231,2175,2116,2126,2128,2118,2133,2232,2137,1650,2146,2074,2165,1393,1221,1005,1914,88,117,1939,2234,2239,1389,74,385,63,42,48,58,4,49,5,47,12,14,19,11,13,18,10,17,7,15,6,8,16,9,2,50,52,59,26,53,20,28,22,27,46,45,21,23,3])).
% 77.02/77.08 cnf(2253,plain,
% 77.02/77.08 (~P3(a7,f11(f10(f10(f10(x22531,f9(a3,x22532)),f9(f8(a3,x22533),a1)),f9(a2,x22534)),f8(a3,x22533)))),
% 77.02/77.08 inference(scs_inference,[],[922,2231,2175,2116,2126,2128,2118,2133,2232,2137,1650,2146,2074,2165,1393,1221,1005,1914,1826,88,117,1939,2234,2239,2249,1389,74,385,63,42,48,58,4,49,5,47,12,14,19,11,13,18,10,17,7,15,6,8,16,9,2,50,52,59,26,53,20,28,22,27,46,45,21,23,3,25])).
% 77.02/77.08 cnf(2262,plain,
% 77.02/77.08 (P5(f10(x22621,f9(x22622,x22623)),x22622,f5(f10(x22621,f9(x22622,x22623)),x22622))),
% 77.02/77.08 inference(scs_inference,[],[2253,63,42,48])).
% 77.02/77.08 cnf(2264,plain,
% 77.02/77.08 (P5(f10(f10(f10(x22641,f9(a3,x22642)),f9(x22643,x22644)),f9(x22645,x22646)),f8(a3,x22647),f5(f10(x22641,f9(a3,x22642)),f8(a3,x22647)))),
% 77.02/77.08 inference(scs_inference,[],[2194,2253,63,42,48,58])).
% 77.02/77.08 cnf(2270,plain,
% 77.02/77.08 (P2(f10(x22701,f9(f6(x22702,x22703,a3,x22704),x22705)),f6(x22702,x22703,f8(f8(a3,x22706),x22707),x22704))),
% 77.02/77.08 inference(scs_inference,[],[2129,2194,2253,2200,63,42,48,58,49,4,5,47])).
% 77.02/77.08 cnf(2272,plain,
% 77.02/77.08 (E(f11(f6(x22721,x22722,a3,x22723),x22724),f11(f6(x22721,x22722,f8(f8(a3,x22725),x22726),x22723),x22724))),
% 77.02/77.08 inference(scs_inference,[],[2129,2194,2253,2200,63,42,48,58,49,4,5,47,14])).
% 77.02/77.08 cnf(2284,plain,
% 77.02/77.08 (E(f10(f6(x22841,x22842,a3,x22843),x22844),f10(f6(x22841,x22842,f8(f8(a3,x22845),x22846),x22843),x22844))),
% 77.02/77.08 inference(scs_inference,[],[2129,2194,2253,2200,63,42,48,58,49,4,5,47,14,19,11,12,17,13,18,10,7,6,15,16,8])).
% 77.02/77.08 cnf(2286,plain,
% 77.02/77.08 (~E(f12(f10(f9(a1,x22861),f9(x22862,x22863)),x22862),f9(f5(a2,a1),x22864))),
% 77.02/77.08 inference(scs_inference,[],[2129,2194,1087,2253,2200,63,42,48,58,49,4,5,47,14,19,11,12,17,13,18,10,7,6,15,16,8,9,2])).
% 77.02/77.08 cnf(2292,plain,
% 77.02/77.08 (~P5(f10(f10(a3,f9(x22921,a1)),f9(a4,x22922)),f12(f10(a7,f9(x22923,x22924)),x22923),f5(a2,a1))),
% 77.02/77.08 inference(scs_inference,[],[2143,2129,2216,2194,1087,2253,2200,2222,1176,63,42,48,58,49,4,5,47,14,19,11,12,17,13,18,10,7,6,15,16,8,9,2,52,59,60])).
% 77.02/77.08 cnf(2293,plain,
% 77.02/77.08 (~P5(f10(a3,f9(x22931,a1)),x22932,f5(a2,a1))),
% 77.02/77.08 inference(rename_variables,[],[2143])).
% 77.02/77.08 cnf(2295,plain,
% 77.02/77.08 (~P5(f8(a3,x22951),x22952,x22953)),
% 77.02/77.08 inference(scs_inference,[],[2143,2129,2225,2216,2194,1087,2253,2200,2222,99,1176,63,42,48,58,49,4,5,47,14,19,11,12,17,13,18,10,7,6,15,16,8,9,2,52,59,60,26])).
% 77.02/77.08 cnf(2298,plain,
% 77.02/77.08 (~P2(f10(f10(f8(f8(a3,x22981),x22982),f9(a4,x22983)),f9(a1,x22984)),f11(f10(x22985,f9(x22986,a7)),x22986))),
% 77.02/77.08 inference(rename_variables,[],[2152])).
% 77.02/77.08 cnf(2305,plain,
% 77.02/77.08 (~P1(f6(f5(x23051,f8(a3,x23052)),x23053,a3,x23054),f6(f5(x23051,a3),x23053,f8(f8(a3,x23055),x23056),x23054))),
% 77.02/77.08 inference(scs_inference,[],[2143,2293,2129,2225,2216,2194,1087,2253,2200,2152,2104,2222,563,1984,1447,99,1176,37,63,42,48,58,49,4,5,47,14,19,11,12,17,13,18,10,7,6,15,16,8,9,2,52,59,60,26,53,28,22,20])).
% 77.02/77.08 cnf(2308,plain,
% 77.02/77.08 (~P3(f11(f10(x23081,f9(f6(x23082,x23083,f8(a3,x23084),x23085),a7)),f6(x23082,x23083,a3,x23085)),a1)),
% 77.02/77.08 inference(scs_inference,[],[2143,2293,2129,2225,2216,2194,1087,2253,2200,2152,2104,2222,563,1855,1984,1447,826,99,1176,37,63,42,48,58,49,4,5,47,14,19,11,12,17,13,18,10,7,6,15,16,8,9,2,52,59,60,26,53,28,22,20,46])).
% 77.02/77.08 cnf(2318,plain,
% 77.02/77.08 (~E(f11(f10(x23181,f9(a3,a1)),f8(f8(a3,x23182),x23183)),f5(a2,a1))),
% 77.02/77.08 inference(scs_inference,[],[2143,2293,1906,2129,2225,2130,2136,2216,833,2194,1087,2253,2200,2152,2298,2104,2222,2217,563,1855,1984,1447,826,99,1176,37,63,42,48,58,49,4,5,47,14,19,11,12,17,13,18,10,7,6,15,16,8,9,2,52,59,60,26,53,28,22,20,46,21,23,3])).
% 77.02/77.08 cnf(2328,plain,
% 77.02/77.08 (P5(f10(f10(x23281,f9(x23282,x23283)),f9(x23284,x23285)),x23282,f5(f10(x23281,f9(x23282,x23283)),x23282))),
% 77.02/77.08 inference(scs_inference,[],[2262,58])).
% 77.02/77.08 cnf(2332,plain,
% 77.02/77.08 (E(f8(f6(x23321,a3,x23322,x23323),x23324),f8(f6(x23321,f8(f8(a3,x23325),x23326),x23322,x23323),x23324))),
% 77.02/77.08 inference(scs_inference,[],[2262,2270,2131,58,49,4])).
% 77.02/77.08 cnf(2334,plain,
% 77.02/77.08 (P2(f10(x23341,f9(f6(x23342,a3,x23343,x23344),x23345)),f6(x23342,f8(f8(a3,x23346),x23347),x23343,x23344))),
% 77.02/77.08 inference(scs_inference,[],[2262,2270,2131,58,49,4,5,47])).
% 77.02/77.08 cnf(2351,plain,
% 77.02/77.08 (P5(f10(x23511,f9(f8(a3,x23512),f8(a3,x23512))),f8(f8(a3,x23513),x23514),f8(f8(a3,x23513),x23514))),
% 77.02/77.08 inference(scs_inference,[],[2318,2262,2270,2131,737,58,49,4,5,47,19,11,12,14,10,7,17,13,18,15,6,8,16,9,2,52])).
% 77.02/77.08 cnf(2353,plain,
% 77.02/77.08 (~P5(f10(f8(a3,x23531),f9(x23532,f9(a1,x23533))),x23534,f12(f10(f9(f5(a2,a1),x23535),f9(x23536,x23537)),x23536))),
% 77.02/77.08 inference(scs_inference,[],[2295,2318,2262,1092,2270,2131,737,58,49,4,5,47,19,11,12,14,10,7,17,13,18,15,6,8,16,9,2,52,59])).
% 77.02/77.08 cnf(2356,plain,
% 77.02/77.08 (~P5(f10(f10(f10(a3,f9(x23561,a1)),f9(a4,x23562)),f9(a4,x23563)),f12(f10(a7,f9(x23564,x23565)),x23564),f5(a2,a1))),
% 77.02/77.08 inference(scs_inference,[],[2295,2318,2262,1092,2292,2270,2131,2216,737,58,49,4,5,47,19,11,12,14,10,7,17,13,18,15,6,8,16,9,2,52,59,60])).
% 77.02/77.08 cnf(2365,plain,
% 77.02/77.08 (~P2(f8(a3,f9(f8(a3,x23651),x23652)),x23653)),
% 77.02/77.08 inference(scs_inference,[],[2295,2318,2262,1092,2292,2270,1926,2284,2131,1923,2118,575,2216,737,58,49,4,5,47,19,11,12,14,10,7,17,13,18,15,6,8,16,9,2,52,59,60,26,53,22])).
% 77.02/77.08 cnf(2368,plain,
% 77.02/77.08 (P3(f11(f10(f10(x23681,f9(a7,a1)),f9(a1,x23682)),a7),a7)),
% 77.02/77.08 inference(scs_inference,[],[2295,2318,2262,1092,2292,2270,1926,2099,2284,2131,1923,2118,575,2216,455,737,58,49,4,5,47,19,11,12,14,10,7,17,13,18,15,6,8,16,9,2,52,59,60,26,53,22,46])).
% 77.02/77.08 cnf(2375,plain,
% 77.02/77.08 (~P5(f8(a2,a7),a1,f11(f10(f10(f10(x23751,f9(a3,x23752)),f9(f8(a3,x23753),a7)),f9(a2,x23754)),f8(a3,x23753)))),
% 77.02/77.08 inference(scs_inference,[],[2295,2318,2262,830,1092,2292,2270,1926,2099,2272,2284,2131,1923,2118,575,2216,455,1939,737,41,58,49,4,5,47,19,11,12,14,10,7,17,13,18,15,6,8,16,9,2,52,59,60,26,53,22,46,20,28])).
% 77.02/77.08 cnf(2380,plain,
% 77.02/77.08 (~P1(f5(f8(f8(a3,x23801),x23802),a3),f5(f12(f10(f8(a3,x23803),f9(x23804,x23805)),x23804),f8(a3,x23806)))),
% 77.02/77.08 inference(scs_inference,[],[2295,2318,2245,2262,830,1092,2292,2270,1926,1774,2308,2099,2272,2284,2131,1923,2118,560,575,2216,455,1939,737,41,58,49,4,5,47,19,11,12,14,10,7,17,13,18,15,6,8,16,9,2,52,59,60,26,53,22,46,20,28,45,21])).
% 77.02/77.08 cnf(2382,plain,
% 77.02/77.08 (~E(f12(f10(f8(f10(x23821,f9(x23822,a1)),a7),f9(x23823,x23824)),x23823),f8(f8(a3,x23825),x23826))),
% 77.02/77.08 inference(scs_inference,[],[2295,2318,2245,2262,830,1092,2292,2270,1926,1774,2308,2099,2272,2284,2131,1923,1721,2118,560,246,575,2216,455,1939,737,41,58,49,4,5,47,19,11,12,14,10,7,17,13,18,15,6,8,16,9,2,52,59,60,26,53,22,46,20,28,45,21,29])).
% 77.02/77.08 cnf(2383,plain,
% 77.02/77.08 (~E(f12(f10(a7,f9(a3,x23831)),f8(f8(a3,x23832),x23833)),a1)),
% 77.02/77.08 inference(scs_inference,[],[2295,1637,2318,2245,2262,830,1092,2292,2270,1926,1774,2308,2099,2272,2284,2131,2127,1923,1721,2118,560,246,575,2216,455,1939,737,41,58,49,4,5,47,19,11,12,14,10,7,17,13,18,15,6,8,16,9,2,52,59,60,26,53,22,46,20,28,45,21,29,3])).
% 77.02/77.08 cnf(2396,plain,
% 77.02/77.08 (P2(f10(x23961,f9(f5(x23962,a3),x23963)),f5(x23962,f8(f8(a3,x23964),x23965)))),
% 77.02/77.08 inference(scs_inference,[],[2122,2334,2132,58,49,47])).
% 77.02/77.08 cnf(2398,plain,
% 77.02/77.08 (E(f8(f5(x23981,a3),x23982),f8(f5(x23981,f8(f8(a3,x23983),x23984)),x23982))),
% 77.02/77.08 inference(scs_inference,[],[2122,2334,2132,58,49,47,4])).
% 77.02/77.08 cnf(2401,plain,
% 77.02/77.08 (E(f11(f5(x24011,a3),x24012),f11(f5(x24011,f8(f8(a3,x24013),x24014)),x24012))),
% 77.02/77.08 inference(scs_inference,[],[2122,2334,2132,58,49,47,4,5,19,14])).
% 77.02/77.08 cnf(2407,plain,
% 77.02/77.08 (E(f9(f5(x24071,a3),x24072),f9(f5(x24071,f8(f8(a3,x24073),x24074)),x24072))),
% 77.02/77.08 inference(scs_inference,[],[2122,2334,2132,58,49,47,4,5,19,14,11,12,10,7,15,6])).
% 77.02/77.08 cnf(2411,plain,
% 77.02/77.08 (E(f10(f5(x24111,a3),x24112),f10(f5(x24111,f8(f8(a3,x24113),x24114)),x24112))),
% 77.02/77.08 inference(scs_inference,[],[2122,2334,2132,58,49,47,4,5,19,14,11,12,10,7,15,6,17,13,18,8])).
% 77.02/77.08 cnf(2415,plain,
% 77.02/77.08 (P5(f10(x24151,f9(f5(x24152,a3),f5(x24152,a3))),f5(x24152,f8(a3,x24153)),f5(x24152,f8(a3,x24153)))),
% 77.02/77.08 inference(scs_inference,[],[777,2122,2334,2132,360,58,49,47,4,5,19,14,11,12,10,7,15,6,17,13,18,8,16,9,2,52])).
% 77.02/77.08 cnf(2417,plain,
% 77.02/77.08 (~P5(f10(f10(f8(a2,a7),f9(x24171,a1)),f9(x24172,a1)),a1,f11(f10(x24173,f9(x24174,a7)),x24174))),
% 77.02/77.08 inference(scs_inference,[],[777,2122,2334,2132,1843,187,360,58,49,47,4,5,19,14,11,12,10,7,15,6,17,13,18,8,16,9,2,52,59])).
% 77.02/77.08 cnf(2423,plain,
% 77.02/77.08 (~P5(f10(a3,f9(f8(a3,x24231),x24232)),a2,x24233)),
% 77.02/77.08 inference(scs_inference,[],[777,2122,2356,2334,1992,2132,1982,1843,187,88,360,58,49,47,4,5,19,14,11,12,10,7,15,6,17,13,18,8,16,9,2,52,59,60,26])).
% 77.02/77.08 cnf(2431,plain,
% 77.02/77.08 (~P5(f10(f8(a3,x24311),f9(x24312,f9(a1,x24313))),x24314,f9(f5(a2,a1),x24315))),
% 77.02/77.08 inference(scs_inference,[],[777,2122,2356,2334,2353,1992,2132,1982,1843,2152,187,88,1939,360,85,41,58,49,47,4,5,19,14,11,12,10,7,15,6,17,13,18,8,16,9,2,52,59,60,26,53,27,28])).
% 77.02/77.08 cnf(2436,plain,
% 77.02/77.08 (~P1(f8(f6(x24361,a3,x24362,x24363),f9(f8(a3,x24364),x24365)),f8(f6(x24361,f8(f8(a3,x24366),x24367),x24362,x24363),f9(a3,x24365)))),
% 77.02/77.08 inference(scs_inference,[],[777,2122,2356,2334,2353,1992,2332,2132,1982,1843,2152,774,1956,187,88,1939,360,85,41,58,49,47,4,5,19,14,11,12,10,7,15,6,17,13,18,8,16,9,2,52,59,60,26,53,27,28,22,20])).
% 77.02/77.08 cnf(2447,plain,
% 77.02/77.08 (P5(f10(f10(f10(a2,f9(x24471,x24472)),f9(x24473,x24474)),f9(x24475,x24476)),f12(f10(a1,f9(x24477,x24478)),x24477),f5(a2,a1))),
% 77.02/77.08 inference(scs_inference,[],[1807,58])).
% 77.02/77.08 cnf(2449,plain,
% 77.02/77.08 (P2(f10(x24491,f9(f9(x24492,a3),x24493)),f9(x24492,f8(f8(a3,x24494),x24495)))),
% 77.02/77.08 inference(scs_inference,[],[1807,2134,58,47])).
% 77.02/77.08 cnf(2454,plain,
% 77.02/77.08 (E(f8(f9(x24541,a3),x24542),f8(f9(x24541,f8(f8(a3,x24543),x24544)),x24542))),
% 77.02/77.08 inference(scs_inference,[],[1807,2396,2134,58,47,49,5,4])).
% 77.02/77.08 cnf(2463,plain,
% 77.02/77.08 (E(f9(f9(x24631,a3),x24632),f9(f9(x24631,f8(f8(a3,x24633),x24634)),x24632))),
% 77.02/77.08 inference(scs_inference,[],[1807,2396,2134,58,47,49,5,4,19,12,10,14,7,11,13,18,6])).
% 77.02/77.08 cnf(2465,plain,
% 77.02/77.08 (E(f12(f9(x24651,a3),x24652),f12(f9(x24651,f8(f8(a3,x24653),x24654)),x24652))),
% 77.02/77.08 inference(scs_inference,[],[1807,2396,2134,58,47,49,5,4,19,12,10,14,7,11,13,18,6,15,16])).
% 77.02/77.08 cnf(2469,plain,
% 77.02/77.08 (~E(a1,f12(f10(a7,f9(a3,x24691)),f8(f8(a3,x24692),x24693)))),
% 77.02/77.08 inference(scs_inference,[],[2383,1807,2396,2134,58,47,49,5,4,19,12,10,14,7,11,13,18,6,15,16,17,8,9,2])).
% 77.02/77.08 cnf(2470,plain,
% 77.02/77.08 (P5(f10(x24701,f9(f8(a3,x24702),f8(a3,x24702))),a3,a3)),
% 77.02/77.08 inference(scs_inference,[],[2383,1807,2396,2134,32,58,47,49,5,4,19,12,10,14,7,11,13,18,6,15,16,17,8,9,2,52])).
% 77.02/77.08 cnf(2476,plain,
% 77.02/77.08 (~P5(f10(a3,f9(f8(a3,x24761),x24762)),a2,x24763)),
% 77.02/77.08 inference(rename_variables,[],[2423])).
% 77.02/77.08 cnf(2478,plain,
% 77.02/77.08 (~P2(f10(f8(a3,f9(f8(a3,x24781),x24782)),f9(a2,x24783)),f11(f10(x24784,f9(x24785,a3)),x24785))),
% 77.02/77.08 inference(scs_inference,[],[2423,2383,1807,2396,2365,2134,107,2356,2216,32,58,47,49,5,4,19,12,10,14,7,11,13,18,6,15,16,17,8,9,2,52,60,59,53])).
% 77.02/77.08 cnf(2479,plain,
% 77.02/77.08 (~P2(f8(a3,f9(f8(a3,x24791),x24792)),x24793)),
% 77.02/77.08 inference(rename_variables,[],[2365])).
% 77.02/77.08 cnf(2481,plain,
% 77.02/77.08 (P5(f8(f10(x24811,f9(f5(x24812,a3),f5(x24812,a3))),f5(x24812,a3)),f5(x24812,f8(a3,x24813)),f5(x24812,f8(a3,x24813)))),
% 77.02/77.08 inference(scs_inference,[],[2423,2383,1807,2415,2396,2365,2134,107,2356,2033,2216,32,58,47,49,5,4,19,12,10,14,7,11,13,18,6,15,16,17,8,9,2,52,60,59,53,26])).
% 77.02/77.08 cnf(2484,plain,
% 77.02/77.08 (~P5(f10(a3,f9(f8(a3,x24841),x24842)),f11(f10(x24843,f9(x24844,a2)),x24844),x24845)),
% 77.02/77.08 inference(scs_inference,[],[2423,2476,2383,1807,2415,2396,2365,2134,107,2356,2033,2216,32,37,58,47,49,5,4,19,12,10,14,7,11,13,18,6,15,16,17,8,9,2,52,60,59,53,26,27])).
% 77.02/77.08 cnf(2485,plain,
% 77.02/77.08 (E(f11(f10(x24851,f9(x24852,x24853)),x24852),x24853)),
% 77.02/77.08 inference(rename_variables,[],[37])).
% 77.02/77.08 cnf(2486,plain,
% 77.02/77.08 (~P1(f10(a3,f9(x24861,a3)),f8(f10(f8(a3,x24862),f9(x24861,a3)),f8(f8(a3,x24863),x24864)))),
% 77.02/77.08 inference(scs_inference,[],[2423,2476,2383,1807,2415,2396,2071,2365,2134,107,2356,2137,2033,2216,32,37,58,47,49,5,4,19,12,10,14,7,11,13,18,6,15,16,17,8,9,2,52,60,59,53,26,27,20])).
% 77.02/77.08 cnf(2487,plain,
% 77.02/77.08 (~P1(f10(f8(x24871,f8(a3,x24872)),f9(x24873,a3)),f8(f10(x24871,f9(x24873,a3)),f8(f8(a3,x24874),x24872)))),
% 77.02/77.08 inference(rename_variables,[],[2071])).
% 77.02/77.08 cnf(2489,plain,
% 77.02/77.08 (~P2(f8(f8(f8(a3,x24891),x24892),f9(a3,x24893)),x24894)),
% 77.02/77.08 inference(scs_inference,[],[2423,2476,2383,1807,2415,2396,2071,2365,2479,2134,107,2356,2137,2033,1181,2216,32,37,58,47,49,5,4,19,12,10,14,7,11,13,18,6,15,16,17,8,9,2,52,60,59,53,26,27,20,22])).
% 77.02/77.08 cnf(2497,plain,
% 77.02/77.08 (~P2(f10(a3,f9(f8(a3,x24971),x24972)),f11(f10(x24973,f9(x24974,a2)),x24974))),
% 77.02/77.08 inference(scs_inference,[],[2423,2476,2158,2383,1807,2415,2396,2071,2487,2365,2479,2091,2134,107,2356,2099,2119,2137,2033,1181,2216,32,37,2485,58,47,49,5,4,19,12,10,14,7,11,13,18,6,15,16,17,8,9,2,52,60,59,53,26,27,20,22,45,21,23])).
% 77.02/77.08 cnf(2505,plain,
% 77.02/77.08 (E(f11(f10(f10(x25051,f9(a1,x25052)),f9(a7,x25053)),a1),f11(f10(x25051,f9(a1,x25052)),a1))),
% 77.02/77.08 inference(scs_inference,[],[2423,2476,2158,2383,1807,2415,2396,2071,2487,2401,2411,2365,2479,2091,2134,2138,107,2356,2099,2119,2137,2033,1181,826,2216,95,32,37,2485,63,58,47,49,5,4,19,12,10,14,7,11,13,18,6,15,16,17,8,9,2,52,60,59,53,26,27,20,22,45,21,23,3,24,50])).
% 77.02/77.08 cnf(2517,plain,
% 77.02/77.08 (P5(f10(f10(x25171,f9(f8(a3,x25172),f8(a3,x25172))),f9(x25173,x25174)),a3,a3)),
% 77.02/77.08 inference(scs_inference,[],[2470,2449,49,58])).
% 77.02/77.08 cnf(2519,plain,
% 77.02/77.08 (P2(f10(x25191,f9(f9(a3,x25192),x25193)),f9(f8(f8(a3,x25194),x25195),x25192))),
% 77.02/77.08 inference(scs_inference,[],[2470,2449,2135,49,58,47])).
% 77.02/77.08 cnf(2540,plain,
% 77.02/77.08 (~P5(f10(f10(f10(f8(a2,a7),f9(x25401,a1)),f9(x25402,a1)),f9(x25403,a4)),a1,f11(f10(x25404,f9(x25405,a7)),x25405))),
% 77.02/77.08 inference(scs_inference,[],[2470,2009,2417,2449,2135,1984,359,49,58,47,4,5,19,14,7,11,12,10,15,16,8,17,13,18,6,9,2,52,59])).
% 77.02/77.08 cnf(2541,plain,
% 77.02/77.08 (~P5(f10(f10(f8(a2,a7),f9(x25411,a1)),f9(x25412,a1)),a1,f11(f10(x25413,f9(x25414,a7)),x25414))),
% 77.02/77.08 inference(rename_variables,[],[2417])).
% 77.02/77.08 cnf(2546,plain,
% 77.02/77.08 (~P3(f11(f10(x25461,f9(f6(x25462,x25463,a3,x25464),a7)),f6(x25462,x25463,f8(a3,x25465),x25464)),a1)),
% 77.02/77.08 inference(scs_inference,[],[2470,2431,2009,2417,2449,2135,1984,1855,828,581,359,49,58,47,4,5,19,14,7,11,12,10,15,16,8,17,13,18,6,9,2,52,59,60,46])).
% 77.02/77.08 cnf(2550,plain,
% 77.02/77.08 (~P2(f10(f10(f8(f8(a3,x25501),x25502),f9(a4,x25503)),f9(a4,x25504)),f11(f10(x25505,f9(x25506,a7)),x25506))),
% 77.02/77.08 inference(scs_inference,[],[2470,2431,2009,2417,2449,2135,2101,1984,1855,828,581,359,49,58,47,4,5,19,14,7,11,12,10,15,16,8,17,13,18,6,9,2,52,59,60,46,53])).
% 77.02/77.08 cnf(2553,plain,
% 77.02/77.08 (~P5(f8(f8(f8(a3,x25531),x25532),f9(a3,x25533)),x25534,x25535)),
% 77.02/77.08 inference(scs_inference,[],[2470,2431,2009,2417,2449,2135,2101,1984,1855,1520,828,581,359,40,49,58,47,4,5,19,14,7,11,12,10,15,16,8,17,13,18,6,9,2,52,59,60,46,53,26])).
% 77.02/77.08 cnf(2556,plain,
% 77.02/77.08 (E(f11(f10(f10(x25561,f9(a1,x25562)),f9(a7,x25563)),a1),f11(f10(x25561,f9(a1,x25562)),a1))),
% 77.02/77.08 inference(rename_variables,[],[2505])).
% 77.02/77.08 cnf(2559,plain,
% 77.02/77.08 (E(f11(f10(f10(x25591,f9(a1,x25592)),f9(a7,x25593)),a1),f11(f10(x25591,f9(a1,x25592)),a1))),
% 77.02/77.08 inference(rename_variables,[],[2505])).
% 77.02/77.08 cnf(2561,plain,
% 77.02/77.08 (E(f11(f10(f10(x25611,f9(a1,x25612)),f9(a7,x25613)),a1),f11(f10(x25611,f9(a1,x25612)),a1))),
% 77.02/77.08 inference(rename_variables,[],[2505])).
% 77.02/77.08 cnf(2562,plain,
% 77.02/77.08 (~P1(f11(f10(x25621,f9(x25622,a7)),x25622),f11(f10(x25623,f9(x25624,a1)),x25624))),
% 77.02/77.08 inference(rename_variables,[],[1740])).
% 77.02/77.08 cnf(2563,plain,
% 77.02/77.08 (~P2(f8(f10(f8(a3,x25631),f9(a4,a1)),a7),a7)),
% 77.02/77.08 inference(scs_inference,[],[2470,2431,2009,2417,2541,1740,2449,2484,2505,2556,2559,2135,2175,2101,563,1984,1855,1520,828,581,359,40,49,58,47,4,5,19,14,7,11,12,10,15,16,8,17,13,18,6,9,2,52,59,60,46,53,26,27,28,20,22])).
% 77.02/77.08 cnf(2567,plain,
% 77.02/77.08 (E(f11(f10(f10(x25671,f9(a1,x25672)),f9(a7,x25673)),a1),f11(f10(x25671,f9(a1,x25672)),a1))),
% 77.02/77.08 inference(rename_variables,[],[2505])).
% 77.02/77.08 cnf(2571,plain,
% 77.02/77.08 (E(f11(f10(f10(x25711,f9(a1,x25712)),f9(a7,x25713)),a1),f11(f10(x25711,f9(a1,x25712)),a1))),
% 77.02/77.09 inference(rename_variables,[],[2505])).
% 77.02/77.09 cnf(2574,plain,
% 77.02/77.09 (~P3(f11(f10(f10(x25741,f9(a1,a7)),f9(a7,x25742)),a1),f11(f10(x25743,f9(x25744,a1)),x25744))),
% 77.02/77.09 inference(scs_inference,[],[2470,2431,2469,2009,2417,2541,1740,2562,2449,2484,2497,2505,2556,2559,2561,2567,2571,2135,2175,2101,2004,563,1984,1855,1520,828,581,359,40,85,49,58,47,4,5,19,14,7,11,12,10,15,16,8,17,13,18,6,9,2,52,59,60,46,53,26,27,28,20,22,21,23,3,24])).
% 77.02/77.09 cnf(2575,plain,
% 77.02/77.09 (~P3(f11(f10(x25751,f9(x25752,a7)),x25752),f11(f10(x25753,f9(x25754,a1)),x25754))),
% 77.02/77.09 inference(rename_variables,[],[2004])).
% 77.02/77.09 cnf(2576,plain,
% 77.02/77.09 (E(f11(f10(f10(x25761,f9(a1,x25762)),f9(a7,x25763)),a1),f11(f10(x25761,f9(a1,x25762)),a1))),
% 77.02/77.09 inference(rename_variables,[],[2505])).
% 77.02/77.09 cnf(2577,plain,
% 77.02/77.09 (~P3(f11(f10(x25771,f9(x25772,a7)),x25772),f11(f10(f10(x25773,f9(a1,a1)),f9(a7,x25774)),a1))),
% 77.02/77.09 inference(scs_inference,[],[2470,2431,2469,2009,2417,2541,1740,2562,2449,2484,2497,2505,2556,2559,2561,2567,2571,2576,2135,2175,2101,2004,2575,563,1984,1855,1520,828,581,359,40,85,49,58,47,4,5,19,14,7,11,12,10,15,16,8,17,13,18,6,9,2,52,59,60,46,53,26,27,28,20,22,21,23,3,24,25])).
% 77.02/77.09 cnf(2580,plain,
% 77.02/77.09 (P3(a1,f11(f10(x25801,f9(f6(x25802,x25803,a3,x25804),a7)),f6(x25802,x25803,f8(a3,x25805),x25804)))),
% 77.02/77.09 inference(scs_inference,[],[2470,2431,2469,2009,2417,2541,1740,2562,2449,2484,2497,2505,2556,2559,2561,2567,2571,2576,2135,2175,2101,2004,2575,563,1984,1855,1520,828,581,359,40,85,49,58,47,4,5,19,14,7,11,12,10,15,16,8,17,13,18,6,9,2,52,59,60,46,53,26,27,28,20,22,21,23,3,24,25,42])).
% 77.02/77.09 cnf(2589,plain,
% 77.02/77.09 (P2(f10(x25891,f9(f12(a3,x25892),x25893)),f12(f8(f8(a3,x25894),x25895),x25892))),
% 77.02/77.09 inference(scs_inference,[],[2519,2574,2139,42,49,47])).
% 77.02/77.09 cnf(2591,plain,
% 77.02/77.09 (P5(f10(f10(f10(x25911,f9(f8(a3,x25912),f8(a3,x25912))),f9(x25913,x25914)),f9(x25915,x25916)),a3,a3)),
% 77.02/77.09 inference(scs_inference,[],[2517,2519,2574,2139,42,49,47,58])).
% 77.02/77.09 cnf(2610,plain,
% 77.02/77.09 (P5(f10(x26101,f9(a3,a3)),f8(a3,x26102),f8(a3,x26102))),
% 77.02/77.09 inference(scs_inference,[],[2517,748,2519,2574,2139,66,42,49,47,58,5,4,19,14,12,7,11,10,17,16,15,13,18,6,8,9,2,52])).
% 77.02/77.09 cnf(2612,plain,
% 77.02/77.09 (~P5(f10(f10(f10(a3,f9(x26121,a1)),f9(a4,x26122)),f9(a1,x26123)),f12(f10(a7,f9(x26124,x26125)),x26124),f5(a2,a1))),
% 77.02/77.09 inference(scs_inference,[],[2517,748,2519,2574,2139,2292,88,66,42,49,47,58,5,4,19,14,12,7,11,10,17,16,15,13,18,6,8,9,2,52,60])).
% 77.02/77.09 cnf(2615,plain,
% 77.02/77.09 (~P5(f10(f8(f8(f8(a3,x26151),x26152),f9(a3,x26153)),f9(x26154,a2)),x26155,f12(f10(f8(a3,x26156),f9(x26157,x26158)),x26157))),
% 77.02/77.09 inference(scs_inference,[],[2553,2517,748,2519,2574,2139,184,2292,88,66,42,49,47,58,5,4,19,14,12,7,11,10,17,16,15,13,18,6,8,9,2,52,60,59])).
% 77.02/77.09 cnf(2621,plain,
% 77.02/77.09 (~P2(f10(f8(f8(f8(a3,x26211),x26212),f9(a3,x26213)),f9(a2,x26214)),f12(f10(f8(a3,x26215),f9(x26216,x26217)),x26216))),
% 77.02/77.09 inference(scs_inference,[],[2553,2489,2517,748,2519,2574,2139,794,184,2292,796,88,66,42,49,47,58,5,4,19,14,12,7,11,10,17,16,15,13,18,6,8,9,2,52,60,59,46,53])).
% 77.02/77.09 cnf(2624,plain,
% 77.02/77.09 (~P5(f10(a3,f9(x26241,a2)),x26242,f12(f10(f8(a3,x26243),f9(x26244,x26245)),x26244))),
% 77.02/77.09 inference(scs_inference,[],[2553,2489,2517,748,2519,2574,2139,1904,794,184,2292,796,88,66,42,49,47,58,5,4,19,14,12,7,11,10,17,16,15,13,18,6,8,9,2,52,60,59,46,53,26])).
% 77.02/77.09 cnf(2632,plain,
% 77.02/77.09 (~P1(f10(a3,f9(x26321,a3)),f8(f10(f8(a3,x26322),f9(x26321,a3)),a3))),
% 77.02/77.09 inference(scs_inference,[],[2553,2489,2517,748,2486,2519,2546,2580,2380,2574,2139,1904,794,184,2292,2133,796,2119,88,66,42,49,47,58,5,4,19,14,12,7,11,10,17,16,15,13,18,6,8,9,2,52,60,59,46,53,26,20,45,21])).
% 77.02/77.09 cnf(2635,plain,
% 77.02/77.09 (~E(f8(f8(f8(f8(a3,x26351),x26352),f9(a3,x26353)),x26354),a2)),
% 77.02/77.09 inference(scs_inference,[],[2553,2489,2517,748,2486,2519,2546,2580,2380,2574,2139,1882,1904,794,184,2292,2133,796,2119,1727,88,66,42,49,47,58,5,4,19,14,12,7,11,10,17,16,15,13,18,6,8,9,2,52,60,59,46,53,26,20,45,21,3])).
% 77.02/77.09 cnf(2637,plain,
% 77.02/77.09 (P3(f9(f5(x26371,f8(f8(a3,x26372),x26373)),f10(a3,x26374)),f9(f5(x26371,a3),f10(f8(a3,x26375),x26374)))),
% 77.02/77.09 inference(scs_inference,[],[2553,2489,2517,748,2486,2519,2546,2580,2380,2574,2407,2139,1882,1904,794,184,2292,2133,796,2119,785,1727,88,66,42,49,47,58,5,4,19,14,12,7,11,10,17,16,15,13,18,6,8,9,2,52,60,59,46,53,26,20,45,21,3,24])).
% 77.02/77.09 cnf(2652,plain,
% 77.02/77.09 (P5(f10(f10(x26521,f9(a3,a3)),f9(x26522,x26523)),f8(a3,x26524),f8(a3,x26524))),
% 77.02/77.09 inference(scs_inference,[],[2610,2589,2577,2250,42,47,49,58])).
% 77.02/77.09 cnf(2670,plain,
% 77.02/77.09 (~E(a2,f8(f8(f8(f8(a3,x26701),x26702),f9(a3,x26703)),x26704))),
% 77.02/77.09 inference(scs_inference,[],[2610,2635,2589,2577,2250,2130,42,47,49,58,5,4,19,7,14,12,11,15,17,10,13,6,8,18,16,9,2])).
% 77.02/77.09 cnf(2671,plain,
% 77.02/77.09 (~P5(f10(f10(a3,f9(x26711,a2)),f9(a2,x26712)),f8(f8(a3,x26713),x26714),f12(f10(f8(a3,x26715),f9(x26716,x26717)),x26716))),
% 77.02/77.09 inference(scs_inference,[],[2610,2624,2635,2589,2577,2250,2130,252,42,47,49,58,5,4,19,7,14,12,11,15,17,10,13,6,8,18,16,9,2,60])).
% 77.02/77.09 cnf(2675,plain,
% 77.02/77.09 (~P5(f10(f10(f10(f8(a2,a7),f9(x26751,a1)),f9(x26752,a1)),f9(x26753,a4)),a1,f11(f10(x26754,f9(x26755,a7)),x26755))),
% 77.02/77.09 inference(rename_variables,[],[2540])).
% 77.02/77.09 cnf(2677,plain,
% 77.02/77.09 (~P3(a7,f11(f10(f10(x26771,f9(a1,a1)),f9(a7,x26772)),a1))),
% 77.02/77.09 inference(scs_inference,[],[2610,2624,2635,2589,2540,2577,2250,2130,252,455,187,42,47,49,58,5,4,19,7,14,12,11,15,17,10,13,6,8,18,16,9,2,60,59,46])).
% 77.02/77.09 cnf(2687,plain,
% 77.02/77.09 (~P5(f11(f10(f10(f10(x26871,f9(a3,x26872)),f9(f8(a3,x26873),f8(a2,a7))),f9(a2,x26874)),f8(a3,x26873)),a1,a7)),
% 77.02/77.09 inference(scs_inference,[],[2610,2624,2635,2589,2550,2540,2675,2577,2250,2505,2130,252,455,187,1939,41,42,47,49,58,5,4,19,7,14,12,11,15,17,10,13,6,8,18,16,9,2,60,59,46,53,28,26])).
% 77.02/77.09 cnf(2689,plain,
% 77.02/77.09 (~P1(f8(f5(x26891,a3),f8(f8(a3,x26892),x26893)),f8(f5(x26891,f8(f8(a3,x26894),x26895)),f8(a3,x26893)))),
% 77.02/77.09 inference(scs_inference,[],[2610,2624,2635,2589,2550,2540,2675,2577,2398,2250,2505,1251,2130,252,455,187,1939,41,42,47,49,58,5,4,19,7,14,12,11,15,17,10,13,6,8,18,16,9,2,60,59,46,53,28,26,20])).
% 77.02/77.09 cnf(2710,plain,
% 77.02/77.09 (P2(f10(f10(f10(x27101,f9(a3,x27102)),f9(x27103,x27104)),f9(x27105,x27106)),f11(f10(x27107,f9(x27108,a3)),x27108))),
% 77.02/77.09 inference(scs_inference,[],[2677,533,42,49])).
% 77.02/77.09 cnf(2714,plain,
% 77.02/77.09 (P5(f10(f10(f10(x27141,f9(a3,a3)),f9(x27142,x27143)),f9(x27144,x27145)),f8(a3,x27146),f8(a3,x27146))),
% 77.02/77.09 inference(scs_inference,[],[2652,2677,1883,533,42,49,47,58])).
% 77.02/77.09 cnf(2734,plain,
% 77.02/77.09 (~E(a2,f12(f10(f8(a3,x27341),f9(x27342,x27343)),x27342))),
% 77.02/77.09 inference(rename_variables,[],[184])).
% 77.02/77.09 cnf(2743,plain,
% 77.02/77.09 (~P2(f10(f10(f8(f8(f8(a3,x27431),x27432),f9(a3,x27433)),f9(a2,x27434)),f9(a2,x27435)),f12(f10(f8(a3,x27436),f9(x27437,x27438)),x27437))),
% 77.02/77.09 inference(scs_inference,[],[2652,2677,2612,1864,2615,2621,2637,1883,533,2136,783,184,2734,2216,42,49,47,58,5,19,4,7,12,14,13,11,17,18,6,15,8,16,10,9,2,59,60,46,53])).
% 77.02/77.09 cnf(2747,plain,
% 77.02/77.09 (P5(f8(f10(x27471,f9(f8(a3,x27472),f8(a3,x27472))),f8(a3,x27472)),f8(f8(a3,x27473),x27474),f8(f8(a3,x27473),x27474))),
% 77.02/77.09 inference(scs_inference,[],[2652,2677,2351,2612,1864,2149,2615,2621,2637,1883,533,2136,2033,783,184,2734,2216,1389,42,49,47,58,5,19,4,7,12,14,13,11,17,18,6,15,8,16,10,9,2,59,60,46,53,27,26])).
% 77.02/77.09 cnf(2748,plain,
% 77.02/77.09 (E(f10(f8(x27481,x27482),f9(x27483,x27482)),f8(f10(x27481,f9(x27483,x27482)),x27482))),
% 77.02/77.09 inference(rename_variables,[],[2033])).
% 77.02/77.09 cnf(2750,plain,
% 77.02/77.09 (~P1(f8(f5(x27501,a3),a3),f8(f5(x27501,f8(f8(a3,x27502),x27503)),f8(a3,x27504)))),
% 77.02/77.09 inference(scs_inference,[],[2652,2677,2351,2612,1864,2149,2615,2621,2689,2637,1883,533,2136,2033,783,184,2734,2119,2216,1389,42,49,47,58,5,19,4,7,12,14,13,11,17,18,6,15,8,16,10,9,2,59,60,46,53,27,26,20])).
% 77.02/77.09 cnf(2758,plain,
% 77.02/77.09 (~E(f12(f10(a4,f9(a3,x27581)),f8(f8(f8(a3,x27582),x27583),f9(a3,x27584))),a7)),
% 77.02/77.09 inference(scs_inference,[],[2652,2059,2632,2677,2351,2612,1864,2149,2615,2621,2689,2637,1883,1884,533,2136,2033,2748,783,184,2734,2119,2216,1389,42,49,47,58,5,19,4,7,12,14,13,11,17,18,6,15,8,16,10,9,2,59,60,46,53,27,26,20,45,21,3])).
% 77.02/77.09 cnf(2761,plain,
% 77.02/77.09 (P3(f12(f9(x27611,a3),f5(a3,x27612)),f12(f9(x27611,f8(f8(a3,x27613),x27614)),f5(f8(a3,x27615),x27612)))),
% 77.02/77.09 inference(scs_inference,[],[2652,2059,2632,2677,2351,2612,1864,2149,2615,2621,2689,2637,2465,1883,1884,533,2136,885,2033,2748,783,184,2734,2119,2216,1389,42,49,47,58,5,19,4,7,12,14,13,11,17,18,6,15,8,16,10,9,2,59,60,46,53,27,26,20,45,21,3,25])).
% 77.02/77.09 cnf(2770,plain,
% 77.02/77.09 (P5(f10(f10(f10(f10(x27701,f9(a3,a3)),f9(x27702,x27703)),f9(x27704,x27705)),f9(x27706,x27707)),f8(a3,x27708),f8(a3,x27708))),
% 77.02/77.09 inference(scs_inference,[],[2714,1891,47,58])).
% 77.02/77.09 cnf(2797,plain,
% 77.02/77.09 (~P3(f12(f10(a7,f9(f5(a3,x27971),x27972)),f5(f8(a3,x27973),x27971)),a1)),
% 77.02/77.09 inference(scs_inference,[],[2714,2758,2710,2671,1891,243,2127,1907,885,252,1984,47,58,49,5,19,4,12,14,7,18,13,6,16,10,17,11,15,8,9,2,59,60,46])).
% 77.02/77.09 cnf(2804,plain,
% 77.02/77.09 (~P5(f10(f10(a3,f9(x28041,a2)),f9(a2,x28042)),f8(f8(a3,x28043),x28044),a3)),
% 77.02/77.09 inference(scs_inference,[],[2714,2758,2710,2671,1891,243,2550,2127,1907,885,169,252,1984,47,58,49,5,19,4,12,14,7,18,13,6,16,10,17,11,15,8,9,2,59,60,46,53,28])).
% 77.02/77.09 cnf(2814,plain,
% 77.02/77.09 (P3(a1,f12(f10(a7,f9(f5(a3,x28141),x28142)),f5(f8(a3,x28143),x28141)))),
% 77.02/77.09 inference(scs_inference,[],[2714,2670,2758,2710,2671,2454,2463,789,1891,243,772,2550,2127,1907,885,169,252,1984,85,47,58,49,5,19,4,12,14,7,18,13,6,16,10,17,11,15,8,9,2,59,60,46,53,28,20,21,3,42])).
% 77.02/77.09 cnf(2819,plain,
% 77.02/77.09 (P2(f10(f10(f10(x28191,f9(a3,x28192)),f9(x28193,x28194)),f9(x28195,x28196)),f12(f10(a3,f9(x28197,x28198)),x28197))),
% 77.02/77.09 inference(scs_inference,[],[521,49])).
% 77.02/77.09 cnf(2821,plain,
% 77.02/77.09 (P5(f10(f10(f10(f10(f10(x28211,f9(a3,a3)),f9(x28212,x28213)),f9(x28214,x28215)),f9(x28216,x28217)),f9(x28218,x28219)),f8(a3,x282110),f8(a3,x282110))),
% 77.02/77.09 inference(scs_inference,[],[2770,521,49,58])).
% 77.02/77.09 cnf(2826,plain,
% 77.02/77.09 (E(f5(x28261,f6(a3,x28262,x28263,x28264)),f5(x28261,f6(f8(f8(a3,x28265),x28266),x28262,x28263,x28264)))),
% 77.02/77.09 inference(scs_inference,[],[2770,1896,521,2128,49,58,47,5,19])).
% 77.02/77.09 cnf(2833,plain,
% 77.02/77.09 (E(f5(f6(a3,x28331,x28332,x28333),x28334),f5(f6(f8(f8(a3,x28335),x28336),x28331,x28332,x28333),x28334))),
% 77.02/77.09 inference(scs_inference,[],[2770,1896,521,2128,49,58,47,5,19,4,12,7,14,10,13,18])).
% 77.02/77.09 cnf(2835,plain,
% 77.02/77.09 (E(f12(f6(a3,x28351,x28352,x28353),x28354),f12(f6(f8(f8(a3,x28355),x28356),x28351,x28352,x28353),x28354))),
% 77.02/77.09 inference(scs_inference,[],[2770,1896,521,2128,49,58,47,5,19,4,12,7,14,10,13,18,17,16])).
% 77.02/77.09 cnf(2845,plain,
% 77.02/77.09 (~P5(f10(f10(f10(a3,f9(x28451,a2)),f9(a2,x28452)),f9(x28453,a2)),f8(f8(a3,x28454),x28455),a3)),
% 77.02/77.09 inference(scs_inference,[],[2804,2770,1748,1896,521,2612,2128,68,88,49,58,47,5,19,4,12,7,14,10,13,18,17,16,6,8,11,15,9,2,60,59])).
% 77.02/77.09 cnf(2851,plain,
% 77.02/77.09 (~P2(f10(f12(f10(f8(f8(a3,x28511),x28512),f9(x28513,x28514)),x28513),f9(a2,x28515)),a3)),
% 77.02/77.09 inference(scs_inference,[],[2804,2770,1748,2761,1896,1846,521,2612,2128,883,68,88,49,58,47,5,19,4,12,7,14,10,13,18,17,16,6,8,11,15,9,2,60,59,46,53])).
% 77.02/77.09 cnf(2856,plain,
% 77.02/77.09 (~P1(f8(f5(x28561,a3),a3),f8(f5(x28561,f8(f8(a3,x28562),x28563)),f8(a3,x28564)))),
% 77.02/77.09 inference(rename_variables,[],[2750])).
% 77.02/77.09 cnf(2861,plain,
% 77.02/77.09 (~P1(f8(f5(x28611,a3),a3),f8(f5(x28611,a3),f8(a3,x28612)))),
% 77.02/77.09 inference(scs_inference,[],[2804,2770,2750,2856,1748,2797,2814,2761,1896,1846,521,2612,2398,2128,1661,883,68,88,935,49,58,47,5,19,4,12,7,14,10,13,18,17,16,6,8,11,15,9,2,60,59,46,53,28,20,45,21])).
% 77.02/77.09 cnf(2864,plain,
% 77.02/77.09 (~E(f8(f10(a3,f9(x28641,x28642)),a4),f10(a2,f9(x28641,x28643)))),
% 77.02/77.09 inference(scs_inference,[],[2804,2770,2750,2856,1748,2797,2814,2761,1702,1896,1880,1846,521,2612,2398,2128,1661,883,68,88,935,49,58,47,5,19,4,12,7,14,10,13,18,17,16,6,8,11,15,9,2,60,59,46,53,28,20,45,21,3])).
% 77.02/77.09 cnf(2871,plain,
% 77.02/77.09 (~P5(f10(f10(a3,f9(x28711,a2)),f9(a2,x28712)),f8(f8(f8(a3,x28713),x28714),f9(a3,x28715)),a3)),
% 77.02/77.09 inference(scs_inference,[],[30,2804,2770,2750,2856,1748,2797,2814,2761,1702,1896,1880,1846,521,2612,2398,2128,649,2677,1732,1661,883,68,88,935,41,49,58,47,5,19,4,12,7,14,10,13,18,17,16,6,8,11,15,9,2,60,59,46,53,28,20,45,21,3,57,81,27])).
% 77.02/77.09 cnf(2897,plain,
% 77.02/77.09 (~P5(f10(f10(f10(a3,f9(x28971,a2)),f9(a2,x28972)),f9(a2,x28973)),f8(f8(f8(a3,x28974),x28975),f9(a3,x28976)),a3)),
% 77.02/77.09 inference(scs_inference,[],[2864,2871,2821,2819,1897,766,2138,49,58,47,5,19,4,7,12,10,14,13,17,18,16,6,11,15,8,9,2,60])).
% 77.02/77.09 cnf(2900,plain,
% 77.02/77.09 (~P5(f10(f8(a2,a7),f9(x29001,a4)),a1,f12(f10(a7,f9(x29002,x29003)),x29002))),
% 77.02/77.09 inference(scs_inference,[],[2864,2871,2821,2819,1897,1804,766,2138,2216,49,58,47,5,19,4,7,12,10,14,13,17,18,16,6,11,15,8,9,2,60,59])).
% 77.02/77.09 cnf(2903,plain,
% 77.02/77.09 (~P5(f10(f10(f10(a3,f9(x29031,a2)),f9(a2,x29032)),f9(x29033,a2)),f8(f8(a3,x29034),x29035),f8(f8(f8(a3,x29036),x29037),f9(a3,x29038)))),
% 77.02/77.09 inference(scs_inference,[],[2864,2845,2871,2821,2819,1897,1804,766,2138,1520,2216,49,58,47,5,19,4,7,12,10,14,13,17,18,16,6,11,15,8,9,2,60,59,28])).
% 77.02/77.09 cnf(2905,plain,
% 77.02/77.09 (E(f12(f6(a3,x29051,x29052,x29053),x29054),f12(f6(f8(f8(a3,x29055),x29056),x29051,x29052,x29053),x29054))),
% 77.02/77.09 inference(rename_variables,[],[2835])).
% 77.02/77.09 cnf(2906,plain,
% 77.02/77.09 (~P1(f12(x29061,f5(f8(a3,x29062),x29063)),f12(x29061,f5(a3,x29063)))),
% 77.02/77.09 inference(rename_variables,[],[890])).
% 77.02/77.09 cnf(2910,plain,
% 77.02/77.09 (~E(f12(f10(f8(f10(a3,f9(x29101,x29102)),a4),f9(x29103,x29104)),x29103),f10(a2,f9(x29101,x29105)))),
% 77.02/77.09 inference(scs_inference,[],[2864,2845,2871,2821,2819,2835,2905,890,2906,1897,1804,766,2138,1520,2216,85,49,58,47,5,19,4,7,12,10,14,13,17,18,16,6,11,15,8,9,2,60,59,28,20,21,3])).
% 77.02/77.09 cnf(2921,plain,
% 77.02/77.09 (~P3(a7,f5(a2,a1))+~P5(f8(a2,a7),a1,f6(a2,a1,f5(a2,a1),a7))),
% 77.02/77.09 inference(scs_inference,[],[2184,51])).
% 77.02/77.09 cnf(2922,plain,
% 77.02/77.09 (P2(f10(a2,f9(x29221,x29222)),f11(f10(x29223,f9(x29224,a1)),x29224))),
% 77.02/77.09 inference(scs_inference,[],[127,49])).
% 77.02/77.09 cnf(2926,plain,
% 77.02/77.09 (P5(f10(f10(f10(f10(x29261,f9(a3,a3)),f9(x29262,x29263)),f9(x29264,x29265)),f9(x29266,x29267)),f8(f8(a3,x29268),x29269),f8(f8(a3,x29268),x29269))),
% 77.02/77.09 inference(scs_inference,[],[1962,1898,127,49,47,58])).
% 77.02/77.09 cnf(2931,plain,
% 77.02/77.09 (E(f6(x29311,x29312,f5(x29313,f8(a3,x29314)),x29315),f6(x29311,x29312,f5(x29313,f8(a3,x29316)),x29315))),
% 77.02/77.09 inference(scs_inference,[],[1962,1898,127,369,49,47,58,5,4,19,12])).
% 77.02/77.09 cnf(2932,plain,
% 77.02/77.09 (E(f9(x29321,f5(x29322,f8(a3,x29323))),f9(x29321,f5(x29322,f8(a3,x29324))))),
% 77.02/77.09 inference(scs_inference,[],[1962,1898,127,369,49,47,58,5,4,19,12,7])).
% 77.02/77.09 cnf(2936,plain,
% 77.02/77.09 (E(f12(f5(x29361,f8(a3,x29362)),x29363),f12(f5(x29361,f8(a3,x29364)),x29363))),
% 77.02/77.09 inference(scs_inference,[],[1962,1898,127,369,49,47,58,5,4,19,12,7,10,14,18,16])).
% 77.02/77.09 cnf(2938,plain,
% 77.02/77.09 (E(f9(f5(x29381,f8(a3,x29382)),x29383),f9(f5(x29381,f8(a3,x29384)),x29383))),
% 77.02/77.09 inference(scs_inference,[],[1962,1898,127,369,49,47,58,5,4,19,12,7,10,14,18,16,17,6])).
% 77.02/77.09 cnf(2942,plain,
% 77.02/77.09 (E(f11(x29421,f5(x29422,f8(a3,x29423))),f11(x29421,f5(x29422,f8(a3,x29424))))),
% 77.02/77.09 inference(scs_inference,[],[1962,1898,127,369,49,47,58,5,4,19,12,7,10,14,18,16,17,6,8,13,11,15])).
% 77.02/77.09 cnf(2945,plain,
% 77.02/77.09 (~P5(f10(f10(f10(f10(a3,f9(x29451,a2)),f9(a2,x29452)),f9(x29453,a2)),f9(x29454,a2)),f8(f8(a3,x29455),x29456),f8(f8(f8(a3,x29457),x29458),f9(a3,x29459)))),
% 77.02/77.09 inference(scs_inference,[],[1962,2903,2177,1898,127,369,766,49,47,58,5,4,19,12,7,10,14,18,16,17,6,8,13,11,15,9,2,59])).
% 77.02/77.09 cnf(2950,plain,
% 77.02/77.09 (~P1(f8(f5(x29501,a3),a3),f8(f5(x29501,a3),f8(a3,x29502)))),
% 77.02/77.09 inference(rename_variables,[],[2861])).
% 77.02/77.09 cnf(2955,plain,
% 77.02/77.09 (~P2(f10(f10(f8(f8(f8(a3,x29551),x29552),f9(a3,x29553)),f9(a2,x29554)),f9(a2,x29555)),a3)),
% 77.02/77.09 inference(scs_inference,[],[2861,2950,1962,2903,2177,2743,1898,127,679,369,766,1538,2804,169,935,49,47,58,5,4,19,12,7,10,14,18,16,17,6,8,13,11,15,9,2,59,28,20,21,23])).
% 77.02/77.09 cnf(2958,plain,
% 77.02/77.09 (E(f11(f10(f10(x29581,f9(a4,x29582)),f9(a7,x29583)),a4),x29582)),
% 77.02/77.09 inference(scs_inference,[],[2861,2950,1962,2903,2177,2743,1898,127,673,2217,679,369,766,111,1538,2804,169,935,37,49,47,58,5,4,19,12,7,10,14,18,16,17,6,8,13,11,15,9,2,59,28,20,21,23,29,3])).
% 77.02/77.09 cnf(2974,plain,
% 77.02/77.09 (P2(f10(f10(a2,f9(x29741,x29742)),f9(x29743,x29744)),f11(f10(x29745,f9(x29746,a1)),x29746))),
% 77.02/77.09 inference(scs_inference,[],[2922,49])).
% 77.02/77.09 cnf(2980,plain,
% 77.02/77.09 (E(f8(x29801,f11(f10(f10(x29802,f9(a4,x29803)),f9(a7,x29804)),a4)),f8(x29801,x29803))),
% 77.02/77.09 inference(scs_inference,[],[2922,2958,2264,1899,49,58,47,5])).
% 77.02/77.09 cnf(2982,plain,
% 77.02/77.09 (E(f8(f11(f10(f10(x29821,f9(a4,x29822)),f9(a7,x29823)),a4),x29824),f8(x29822,x29824))),
% 77.02/77.09 inference(scs_inference,[],[2922,2958,2264,1899,49,58,47,5,19,4])).
% 77.02/77.09 cnf(2990,plain,
% 77.02/77.09 (E(f5(f11(f10(f10(x29901,f9(a4,x29902)),f9(a7,x29903)),a4),x29904),f5(x29902,x29904))),
% 77.02/77.09 inference(scs_inference,[],[2922,2958,2264,1899,49,58,47,5,19,4,7,12,10,14,17,16,6,18])).
% 77.02/77.09 cnf(2992,plain,
% 77.02/77.09 (E(f10(f11(f10(f10(x29921,f9(a4,x29922)),f9(a7,x29923)),a4),x29924),f10(x29922,x29924))),
% 77.02/77.09 inference(scs_inference,[],[2922,2958,2264,1899,49,58,47,5,19,4,7,12,10,14,17,16,6,18,13,8])).
% 77.02/77.09 cnf(2997,plain,
% 77.02/77.09 (~P5(f10(f10(f10(f10(a3,f9(x29971,a2)),f9(a2,x29972)),f9(a2,x29973)),f9(a2,x29974)),f8(f8(f8(a3,x29975),x29976),f9(a3,x29977)),a3)),
% 77.02/77.09 inference(scs_inference,[],[2922,2958,2264,1938,2897,1899,766,49,58,47,5,19,4,7,12,10,14,17,16,6,18,13,8,15,11,9,2,60])).
% 77.02/77.09 cnf(3000,plain,
% 77.02/77.09 (~P5(f10(f10(f8(a2,a7),f9(x30001,a4)),f9(x30002,a1)),a1,f12(f10(a7,f9(x30003,x30004)),x30003))),
% 77.02/77.09 inference(scs_inference,[],[2922,2958,2264,1938,2900,2897,1899,766,88,49,58,47,5,19,4,7,12,10,14,17,16,6,18,13,8,15,11,9,2,60,59])).
% 77.02/77.09 cnf(3004,plain,
% 77.02/77.09 (E(f11(f10(f10(x30041,f9(a4,x30042)),f9(a7,x30043)),a4),x30042)),
% 77.02/77.09 inference(rename_variables,[],[2958])).
% 77.02/77.09 cnf(3005,plain,
% 77.02/77.09 (~P2(f11(f10(f10(x30051,f9(a4,a3)),f9(a7,x30052)),a4),x30053)),
% 77.02/77.09 inference(scs_inference,[],[2922,2958,3004,2264,1938,2900,2897,1899,2423,766,88,39,49,58,47,5,19,4,7,12,10,14,17,16,6,18,13,8,15,11,9,2,60,59,27,22])).
% 77.02/77.09 cnf(3006,plain,
% 77.02/77.09 (E(f11(f10(f10(x30061,f9(a4,x30062)),f9(a7,x30063)),a4),x30062)),
% 77.02/77.09 inference(rename_variables,[],[2958])).
% 77.02/77.09 cnf(3007,plain,
% 77.02/77.09 (~P5(f11(f10(f10(x30071,f9(a4,f8(a3,x30072))),f9(a7,x30073)),a4),x30074,x30075)),
% 77.02/77.09 inference(scs_inference,[],[2922,2958,3004,3006,2264,1938,2900,2897,1899,2423,766,2295,88,39,49,58,47,5,19,4,7,12,10,14,17,16,6,18,13,8,15,11,9,2,60,59,27,22,26])).
% 77.02/77.09 cnf(3008,plain,
% 77.02/77.09 (E(f11(f10(f10(x30081,f9(a4,x30082)),f9(a7,x30083)),a4),x30082)),
% 77.02/77.09 inference(rename_variables,[],[2958])).
% 77.02/77.09 cnf(3009,plain,
% 77.02/77.09 (~P5(f10(f10(f10(f10(a3,f9(x30091,a2)),f9(a2,x30092)),f9(x30093,a2)),f9(x30094,a2)),f8(f8(a3,x30095),x30096),f8(a3,f9(a3,x30097)))),
% 77.02/77.09 inference(scs_inference,[],[2922,2958,3004,3006,2264,1938,2945,2900,2897,1899,2423,2118,766,2295,88,39,49,58,47,5,19,4,7,12,10,14,17,16,6,18,13,8,15,11,9,2,60,59,27,22,26,28])).
% 77.02/77.09 cnf(3018,plain,
% 77.02/77.09 (E(f11(f10(f10(x30181,f9(a4,x30182)),f9(a7,x30183)),a4),x30182)),
% 77.02/77.09 inference(rename_variables,[],[2958])).
% 77.02/77.09 cnf(3022,plain,
% 77.02/77.09 (~P3(f12(f10(a7,f9(x30221,x30222)),x30221),f11(f10(f10(x30223,f9(a4,a1)),f9(a7,x30224)),a4))),
% 77.02/77.09 inference(scs_inference,[],[2922,2958,3004,3006,3008,3018,2264,2931,2932,2942,1938,1745,2945,2900,1334,2897,2563,1899,1444,2423,2118,1907,766,2295,88,39,49,58,47,5,19,4,7,12,10,14,17,16,6,18,13,8,15,11,9,2,60,59,27,22,26,28,20,21,23,3,25])).
% 77.02/77.09 cnf(3023,plain,
% 77.02/77.09 (E(f11(f10(f10(x30231,f9(a4,x30232)),f9(a7,x30233)),a4),x30232)),
% 77.02/77.09 inference(rename_variables,[],[2958])).
% 77.02/77.09 cnf(3024,plain,
% 77.02/77.09 (~P3(f11(f10(f10(x30241,f9(a4,a7)),f9(a7,x30242)),a4),f11(f10(x30243,f9(x30244,a1)),x30244))),
% 77.02/77.09 inference(scs_inference,[],[2922,2958,3004,3006,3008,3018,3023,2264,2931,2932,2942,1938,1745,2945,2900,1334,2897,2563,1899,1444,2423,1942,2118,1907,766,2295,88,39,49,58,47,5,19,4,7,12,10,14,17,16,6,18,13,8,15,11,9,2,60,59,27,22,26,28,20,21,23,3,25,24])).
% 77.02/77.09 cnf(3026,plain,
% 77.02/77.09 (P3(f11(f10(f10(x30261,f9(a4,a1)),f9(a7,x30262)),a4),f12(f10(a7,f9(x30263,x30264)),x30263))),
% 77.02/77.09 inference(scs_inference,[],[2922,2958,3004,3006,3008,3018,3023,2264,2931,2932,2942,1938,1745,2945,2900,1334,2897,2563,1899,1444,2423,1942,2118,1907,766,2295,88,39,49,58,47,5,19,4,7,12,10,14,17,16,6,18,13,8,15,11,9,2,60,59,27,22,26,28,20,21,23,3,25,24,42])).
% 77.02/77.09 cnf(3034,plain,
% 77.02/77.09 (P2(f10(f10(f10(a2,f9(x30341,x30342)),f9(x30343,x30344)),f9(x30345,x30346)),f11(f10(x30347,f9(x30348,a1)),x30348))),
% 77.02/77.09 inference(scs_inference,[],[2974,3024,42,49])).
% 77.02/77.09 cnf(3063,plain,
% 77.02/77.09 (~P2(f10(a3,f9(a2,x30631)),a3)),
% 77.02/77.09 inference(scs_inference,[],[2192,2974,3009,3007,2011,3024,2851,1903,1982,2133,649,581,42,49,47,58,5,19,4,12,10,7,6,17,18,14,16,11,8,13,15,9,2,59,27,22])).
% 77.02/77.09 cnf(3071,plain,
% 77.02/77.09 (E(f11(f10(f10(f10(x30711,f9(a3,x30712)),f9(f8(a3,x30713),x30714)),f9(a2,x30715)),f8(a3,x30713)),x30714)),
% 77.02/77.09 inference(rename_variables,[],[1939])).
% 77.02/77.09 cnf(3075,plain,
% 77.02/77.09 (~E(f12(f10(a3,f9(a3,x30751)),f8(f8(f8(a3,x30752),x30753),f9(a3,x30754))),a2)),
% 77.02/77.09 inference(scs_inference,[],[2140,2955,2192,2974,3009,1892,3007,2011,3024,204,2851,1903,1884,1982,2133,2137,649,581,1520,1939,3071,42,49,47,58,5,19,4,12,10,7,6,17,18,14,16,11,8,13,15,9,2,59,27,22,26,45,20,23,21,3])).
% 77.02/77.09 cnf(3094,plain,
% 77.02/77.09 (E(f8(x30941,f8(a3,x30942)),f8(x30941,f8(a3,x30943)))),
% 77.02/77.09 inference(scs_inference,[],[2591,3034,1905,99,49,47,58,5])).
% 77.02/77.09 cnf(3096,plain,
% 77.02/77.09 (E(f6(x30961,x30962,f8(a3,x30963),x30964),f6(x30961,x30962,f8(a3,x30965),x30964))),
% 77.02/77.09 inference(scs_inference,[],[2591,3034,1905,99,2118,49,47,58,5,19,12])).
% 77.02/77.09 cnf(3097,plain,
% 77.02/77.09 (E(f6(f8(a3,x30971),x30972,x30973,x30974),f6(f8(a3,x30975),x30972,x30973,x30974))),
% 77.02/77.09 inference(scs_inference,[],[2591,3034,1905,99,2118,49,47,58,5,19,12,10])).
% 77.02/77.09 cnf(3098,plain,
% 77.02/77.09 (E(f8(f8(a3,x30981),x30982),f8(f8(a3,x30983),x30982))),
% 77.02/77.09 inference(scs_inference,[],[2591,3034,1905,99,2118,49,47,58,5,19,12,10,4])).
% 77.02/77.09 cnf(3099,plain,
% 77.02/77.09 (E(f5(f8(a3,x30991),x30992),f5(f8(a3,x30993),x30992))),
% 77.02/77.09 inference(scs_inference,[],[2591,3034,1905,99,2118,49,47,58,5,19,12,10,4,18])).
% 77.02/77.09 cnf(3102,plain,
% 77.02/77.09 (E(f6(x31021,f8(a3,x31022),x31023,x31024),f6(x31021,f8(a3,x31025),x31023,x31024))),
% 77.02/77.09 inference(scs_inference,[],[2591,3034,1905,99,2118,49,47,58,5,19,12,10,4,18,7,6,11])).
% 77.02/77.09 cnf(3104,plain,
% 77.02/77.09 (E(f6(x31041,x31042,x31043,f8(a3,x31044)),f6(x31041,x31042,x31043,f8(a3,x31045)))),
% 77.02/77.09 inference(scs_inference,[],[2591,3034,1905,99,2118,49,47,58,5,19,12,10,4,18,7,6,11,14,13])).
% 77.02/77.09 cnf(3105,plain,
% 77.02/77.09 (E(f12(x31051,f8(a3,x31052)),f12(x31051,f8(a3,x31053)))),
% 77.02/77.09 inference(scs_inference,[],[2591,3034,1905,99,2118,49,47,58,5,19,12,10,4,18,7,6,11,14,13,17])).
% 77.02/77.09 cnf(3107,plain,
% 77.02/77.09 (E(f10(f8(a3,x31071),x31072),f10(f8(a3,x31073),x31072))),
% 77.02/77.09 inference(scs_inference,[],[2591,3034,1905,99,2118,49,47,58,5,19,12,10,4,18,7,6,11,14,13,17,16,8])).
% 77.02/77.09 cnf(3108,plain,
% 77.02/77.09 (E(f11(x31081,f8(a3,x31082)),f11(x31081,f8(a3,x31083)))),
% 77.02/77.09 inference(scs_inference,[],[2591,3034,1905,99,2118,49,47,58,5,19,12,10,4,18,7,6,11,14,13,17,16,8,15])).
% 77.02/77.09 cnf(3114,plain,
% 77.02/77.09 (~P5(f10(f10(f10(f8(a2,a7),f9(x31141,a4)),f9(x31142,a1)),f9(x31143,a4)),a1,f12(f10(a7,f9(x31144,x31145)),x31144))),
% 77.02/77.09 inference(scs_inference,[],[2591,3000,3075,2997,3034,1905,99,2118,766,2216,49,47,58,5,19,12,10,4,18,7,6,11,14,13,17,16,8,15,9,2,60,59])).
% 77.02/77.09 cnf(3121,plain,
% 77.02/77.09 (E(f10(f11(f10(f10(x31211,f9(a4,x31212)),f9(a7,x31213)),a4),x31214),f10(x31212,x31214))),
% 77.02/77.09 inference(rename_variables,[],[2992])).
% 77.02/77.09 cnf(3122,plain,
% 77.02/77.09 (~P5(f10(f11(f10(f10(x31221,f9(a4,a3)),f9(a7,x31222)),a4),f9(x31223,a1)),x31224,f5(a2,a1))),
% 77.02/77.09 inference(scs_inference,[],[3063,3005,2591,3000,3075,2997,3034,2992,3121,1905,2143,99,2118,415,766,2216,49,47,58,5,19,12,10,4,18,7,6,11,14,13,17,16,8,15,9,2,60,59,53,22,26])).
% 77.02/77.09 cnf(3130,plain,
% 77.02/77.09 (~P2(f10(a3,f9(a2,x31301)),f12(f10(f8(f8(a3,x31302),x31303),f9(x31304,x31305)),x31304))),
% 77.02/77.09 inference(scs_inference,[],[3063,3005,2591,3000,3075,2997,2936,2938,3034,2992,3121,887,787,1905,2143,99,2118,1661,415,766,2216,49,47,58,5,19,12,10,4,18,7,6,11,14,13,17,16,8,15,9,2,60,59,53,22,26,20,21,23])).
% 77.02/77.09 cnf(3145,plain,
% 77.02/77.09 (P2(f10(a2,f9(x31451,x31452)),f12(f10(a1,f9(x31453,x31454)),x31453))),
% 77.02/77.09 inference(scs_inference,[],[113,49])).
% 77.02/77.09 cnf(3152,plain,
% 77.02/77.09 (E(f6(x31521,x31522,f6(x31523,x31524,f8(a3,x31525),x31526),x31527),f6(x31521,x31522,f6(x31523,x31524,f8(a3,x31528),x31526),x31527))),
% 77.02/77.09 inference(scs_inference,[],[3096,2328,113,49,47,58,5,12])).
% 77.02/77.09 cnf(3153,plain,
% 77.02/77.09 (E(f5(x31531,f6(x31532,x31533,f8(a3,x31534),x31535)),f5(x31531,f6(x31532,x31533,f8(a3,x31536),x31535)))),
% 77.02/77.09 inference(scs_inference,[],[3096,2328,113,49,47,58,5,12,19])).
% 77.02/77.09 cnf(3155,plain,
% 77.02/77.09 (E(f8(f6(x31551,x31552,f8(a3,x31553),x31554),x31555),f8(f6(x31551,x31552,f8(a3,x31556),x31554),x31555))),
% 77.02/77.09 inference(scs_inference,[],[3096,2328,113,49,47,58,5,12,19,10,4])).
% 77.02/77.09 cnf(3156,plain,
% 77.02/77.09 (E(f6(x31561,f6(x31562,x31563,f8(a3,x31564),x31565),x31566,x31567),f6(x31561,f6(x31562,x31563,f8(a3,x31568),x31565),x31566,x31567))),
% 77.02/77.09 inference(scs_inference,[],[3096,2328,113,49,47,58,5,12,19,10,4,11])).
% 77.02/77.09 cnf(3159,plain,
% 77.02/77.09 (E(f5(f6(x31591,x31592,f8(a3,x31593),x31594),x31595),f5(f6(x31591,x31592,f8(a3,x31596),x31594),x31595))),
% 77.02/77.09 inference(scs_inference,[],[3096,2328,113,49,47,58,5,12,19,10,4,11,6,17,18])).
% 77.02/77.09 cnf(3161,plain,
% 77.02/77.09 (E(f9(x31611,f6(x31612,x31613,f8(a3,x31614),x31615)),f9(x31611,f6(x31612,x31613,f8(a3,x31616),x31615)))),
% 77.02/77.09 inference(scs_inference,[],[3096,2328,113,49,47,58,5,12,19,10,4,11,6,17,18,14,7])).
% 77.02/77.09 cnf(3165,plain,
% 77.02/77.09 (E(f11(x31651,f6(x31652,x31653,f8(a3,x31654),x31655)),f11(x31651,f6(x31652,x31653,f8(a3,x31656),x31655)))),
% 77.02/77.09 inference(scs_inference,[],[3096,2328,113,49,47,58,5,12,19,10,4,11,6,17,18,14,7,13,16,8,15])).
% 77.02/77.09 cnf(3170,plain,
% 77.02/77.09 (~P3(a7,f11(f10(f10(x31701,f9(a7,a1)),f9(a1,x31702)),a7))),
% 77.02/77.09 inference(scs_inference,[],[3096,3122,2328,2382,113,2091,455,581,49,47,58,5,12,19,10,4,11,6,17,18,14,7,13,16,8,15,9,2,59,46])).
% 77.02/77.09 cnf(3174,plain,
% 77.02/77.09 (~P5(f10(a3,f9(a1,x31741)),f11(f10(x31742,f9(f8(a3,x31743),f5(a2,a1))),f8(a3,x31744)),x31745)),
% 77.02/77.09 inference(scs_inference,[],[3096,3108,3122,2328,2382,1924,113,2091,455,581,49,47,58,5,12,19,10,4,11,6,17,18,14,7,13,16,8,15,9,2,59,46,27])).
% 77.02/77.09 cnf(3176,plain,
% 77.02/77.09 (E(f11(x31761,f8(a3,x31762)),f11(x31761,f8(a3,x31763)))),
% 77.02/77.09 inference(rename_variables,[],[3108])).
% 77.02/77.09 cnf(3178,plain,
% 77.02/77.09 (E(f12(x31781,f8(a3,x31782)),f12(x31781,f8(a3,x31783)))),
% 77.02/77.09 inference(rename_variables,[],[3105])).
% 77.02/77.09 cnf(3180,plain,
% 77.02/77.09 (~P5(f8(a2,a7),a1,f11(f10(f10(f10(x31801,f9(a3,x31802)),f9(f8(a3,x31803),a7)),f9(a2,x31804)),f8(a3,x31805)))),
% 77.02/77.09 inference(scs_inference,[],[3096,3105,3108,3176,3122,2328,2375,2382,1924,113,2091,1846,455,581,49,47,58,5,12,19,10,4,11,6,17,18,14,7,13,16,8,15,9,2,59,46,27,22,28])).
% 77.02/77.09 cnf(3182,plain,
% 77.02/77.09 (E(f11(x31821,f8(a3,x31822)),f11(x31821,f8(a3,x31823)))),
% 77.02/77.09 inference(rename_variables,[],[3108])).
% 77.02/77.09 cnf(3183,plain,
% 77.02/77.09 (~P5(f12(f10(f8(f8(a3,x31831),x31832),f9(f8(a3,x31833),x31834)),f8(a3,x31835)),x31836,x31837)),
% 77.02/77.09 inference(scs_inference,[],[3096,3105,3178,3108,3176,3122,2328,2375,2382,1924,113,2091,1836,1846,455,581,49,47,58,5,12,19,10,4,11,6,17,18,14,7,13,16,8,15,9,2,59,46,27,22,28,26])).
% 77.02/77.09 cnf(3184,plain,
% 77.02/77.09 (E(f12(x31841,f8(a3,x31842)),f12(x31841,f8(a3,x31843)))),
% 77.02/77.09 inference(rename_variables,[],[3105])).
% 77.02/77.09 cnf(3191,plain,
% 77.02/77.09 (E(f11(x31911,f8(a3,x31912)),f11(x31911,f8(a3,x31913)))),
% 77.02/77.09 inference(rename_variables,[],[3108])).
% 77.02/77.09 cnf(3194,plain,
% 77.02/77.09 (E(f11(x31941,f8(a3,x31942)),f11(x31941,f8(a3,x31943)))),
% 77.02/77.09 inference(rename_variables,[],[3108])).
% 77.02/77.09 cnf(3196,plain,
% 77.02/77.09 (E(f12(x31961,f8(a3,x31962)),f12(x31961,f8(a3,x31963)))),
% 77.02/77.09 inference(rename_variables,[],[3105])).
% 77.02/77.09 cnf(3198,plain,
% 77.02/77.09 (~E(f12(f10(f9(a1,x31981),f9(f8(a3,x31982),x31983)),f8(a3,x31984)),f9(f5(a2,a1),x31985))),
% 77.02/77.09 inference(scs_inference,[],[3096,3105,3178,3184,3196,3108,3176,3182,3191,2286,3122,2328,3130,1920,2085,2375,2382,3026,3022,1924,113,2091,1836,1846,455,581,49,47,58,5,12,19,10,4,11,6,17,18,14,7,13,16,8,15,9,2,59,46,27,22,28,26,45,20,21,23,3])).
% 77.02/77.09 cnf(3201,plain,
% 77.02/77.09 (~P3(a7,f11(f10(f10(f10(x32011,f9(a3,x32012)),f9(f8(a3,x32013),a1)),f9(a2,x32014)),f8(a3,x32015)))),
% 77.02/77.09 inference(scs_inference,[],[3096,3105,3178,3184,3196,3108,3176,3182,3191,3194,2286,3122,2328,3130,1920,2085,2375,2382,3026,3022,1924,113,2091,1836,1846,2253,455,581,49,47,58,5,12,19,10,4,11,6,17,18,14,7,13,16,8,15,9,2,59,46,27,22,28,26,45,20,21,23,3,25])).
% 77.02/77.09 cnf(3203,plain,
% 77.02/77.09 (E(f11(x32031,f8(a3,x32032)),f11(x32031,f8(a3,x32033)))),
% 77.02/77.09 inference(rename_variables,[],[3108])).
% 77.02/77.09 cnf(3204,plain,
% 77.02/77.09 (~P3(f11(f10(f10(f10(x32041,f9(a3,x32042)),f9(f8(a3,x32043),a7)),f9(a2,x32044)),f8(a3,x32045)),a1)),
% 77.02/77.09 inference(scs_inference,[],[3096,3105,3178,3184,3196,3108,3176,3182,3191,3194,3203,2286,3122,2328,3130,1920,2085,2375,2382,3026,3022,1924,113,2091,1836,1846,2253,1944,455,581,49,47,58,5,12,19,10,4,11,6,17,18,14,7,13,16,8,15,9,2,59,46,27,22,28,26,45,20,21,23,3,25,24])).
% 77.02/77.09 cnf(3209,plain,
% 77.02/77.09 (~E(f12(f10(f8(f10(x32091,f9(x32092,a1)),a7),f9(x32093,x32094)),x32093),a3)),
% 77.02/77.09 inference(scs_inference,[],[3096,3105,3178,3184,3196,3108,3176,3182,3191,3194,3203,2286,3122,2328,3130,1920,2085,2375,2382,3026,3022,1924,113,2091,1836,1846,2253,1721,1944,38,455,581,49,47,58,5,12,19,10,4,11,6,17,18,14,7,13,16,8,15,9,2,59,46,27,22,28,26,45,20,21,23,3,25,24,81,29])).
% 77.02/77.09 cnf(3215,plain,
% 77.02/77.09 (P2(f10(f10(a2,f9(x32151,x32152)),f9(x32153,x32154)),f12(f10(a1,f9(x32155,x32156)),x32155))),
% 77.02/77.09 inference(scs_inference,[],[3145,3201,42,49])).
% 77.02/77.09 cnf(3226,plain,
% 77.02/77.09 (E(f6(x32261,f6(f8(a3,x32262),x32263,x32264,x32265),x32266,x32267),f6(x32261,f6(f8(a3,x32268),x32263,x32264,x32265),x32266,x32267))),
% 77.02/77.09 inference(scs_inference,[],[3097,3145,2447,3201,42,49,58,47,5,12,10,19,4,11])).
% 77.02/77.09 cnf(3244,plain,
% 77.02/77.09 (~P2(f10(f8(a3,x32441),f9(a2,x32442)),f11(f10(x32443,f9(x32444,a3)),x32444))),
% 77.02/77.09 inference(scs_inference,[],[3097,3107,3145,3198,2447,3201,3114,2478,1227,1393,88,42,49,58,47,5,12,10,19,4,11,6,14,17,7,18,13,16,15,8,9,2,59,46,22])).
% 77.02/77.09 cnf(3249,plain,
% 77.02/77.09 (E(f6(x32491,f8(a3,x32492),x32493,x32494),f6(x32491,f8(a3,x32495),x32493,x32494))),
% 77.02/77.09 inference(rename_variables,[],[3102])).
% 77.02/77.09 cnf(3250,plain,
% 77.02/77.09 (~P1(f6(f5(x32501,f8(a3,x32502)),x32503,a3,x32504),f6(f5(x32501,a3),x32503,f8(f8(a3,x32505),x32506),x32504))),
% 77.02/77.09 inference(rename_variables,[],[2305])).
% 77.02/77.09 cnf(3251,plain,
% 77.02/77.09 (~P1(f6(f5(x32511,f8(a3,x32512)),x32513,a3,f8(a3,x32514)),f6(f5(x32511,a3),x32513,f8(f8(a3,x32515),x32516),f8(a3,x32517)))),
% 77.02/77.09 inference(scs_inference,[],[3097,3102,3104,3107,3145,3198,2447,3201,2305,3250,3114,2980,2478,1227,1393,88,41,42,49,58,47,5,12,10,19,4,11,6,14,17,7,18,13,16,15,8,9,2,59,46,22,26,20,21])).
% 77.02/77.09 cnf(3252,plain,
% 77.02/77.09 (E(f6(x32521,x32522,x32523,f8(a3,x32524)),f6(x32521,x32522,x32523,f8(a3,x32525)))),
% 77.02/77.09 inference(rename_variables,[],[3104])).
% 77.02/77.09 cnf(3255,plain,
% 77.02/77.09 (~E(f12(f10(a7,f9(x32551,x32552)),x32551),f12(f10(a1,f9(x32553,x32554)),x32553))),
% 77.02/77.09 inference(scs_inference,[],[3097,3102,3104,3107,3145,3198,2447,3201,2305,3250,3114,2980,2478,1227,193,1393,3063,1538,88,85,41,42,49,58,47,5,12,10,19,4,11,6,14,17,7,18,13,16,15,8,9,2,59,46,22,26,20,21,23,3])).
% 77.02/77.09 cnf(3260,plain,
% 77.02/77.09 (P3(f6(f5(x32601,a3),x32602,x32603,f8(a3,x32604)),f6(f5(x32601,f8(a3,x32605)),x32602,x32603,f8(a3,x32606)))),
% 77.02/77.09 inference(scs_inference,[],[3097,3102,3249,3104,3252,3107,3145,3198,2447,2015,3201,2305,3250,3114,2980,2478,1227,193,1393,1442,3063,1538,88,85,41,42,49,58,47,5,12,10,19,4,11,6,14,17,7,18,13,16,15,8,9,2,59,46,22,26,20,21,23,3,24,25])).
% 77.02/77.09 cnf(3268,plain,
% 77.02/77.09 (P2(f10(f10(f10(a2,f9(x32681,x32682)),f9(x32683,x32684)),f9(x32685,x32686)),f12(f10(a1,f9(x32687,x32688)),x32687))),
% 77.02/77.09 inference(scs_inference,[],[3215,3204,42,49])).
% 77.02/77.09 cnf(3292,plain,
% 77.02/77.09 (~P5(f12(f10(f8(f8(a3,x32921),x32922),f9(f8(a3,x32923),x32924)),f8(a3,x32925)),x32926,x32927)),
% 77.02/77.09 inference(rename_variables,[],[3183])).
% 77.02/77.09 cnf(3295,plain,
% 77.02/77.09 (E(f11(x32951,f8(a3,x32952)),f11(x32951,f8(a3,x32953)))),
% 77.02/77.09 inference(rename_variables,[],[3108])).
% 77.02/77.09 cnf(3297,plain,
% 77.02/77.09 (E(f11(x32971,f8(a3,x32972)),f11(x32971,f8(a3,x32973)))),
% 77.02/77.09 inference(rename_variables,[],[3108])).
% 77.02/77.09 cnf(3301,plain,
% 77.02/77.09 (~P1(f6(f5(x33011,f8(a3,x33012)),f6(x33013,x33014,f8(a3,x33015),x33016),a3,f8(a3,x33017)),f6(f5(x33011,a3),f6(x33013,x33014,f8(a3,x33018),x33016),f8(f8(a3,x33019),x330110),f8(a3,x330111)))),
% 77.02/77.09 inference(scs_inference,[],[3251,3170,3183,3215,2926,3204,2687,3156,3255,2368,3094,3108,3295,2074,67,42,49,47,58,5,12,4,10,19,11,6,18,14,7,17,13,16,8,15,9,2,59,22,26,45,20])).
% 77.02/77.09 cnf(3316,plain,
% 77.02/77.09 (~P3(a7,f5(a2,a1))+P5(f8(a2,a7),a1,f6(a2,a1,f5(a2,a1),a7))),
% 77.02/77.09 inference(scs_inference,[],[30,3251,3244,3170,3183,3292,3215,2926,3204,2687,3156,3153,3155,3255,2436,2368,3094,2826,3108,3295,3297,2074,410,67,42,49,47,58,5,12,4,10,19,11,6,18,14,7,17,13,16,8,15,9,2,59,22,26,45,20,21,23,3,60,62])).
% 77.02/77.09 cnf(3346,plain,
% 77.02/77.09 (E(f8(f11(f10(f10(x33461,f9(a4,x33462)),f9(a7,x33463)),a4),x33464),f8(x33462,x33464))),
% 77.02/77.09 inference(rename_variables,[],[2982])).
% 77.02/77.09 cnf(3347,plain,
% 77.02/77.09 (~P5(f8(f11(f10(f10(x33471,f9(a4,a2)),f9(a7,x33472)),a4),a7),a1,a7)),
% 77.02/77.09 inference(scs_inference,[],[2481,3268,3209,2982,3346,3098,2365,41,49,58,47,5,19,4,10,12,11,6,17,13,7,18,14,16,15,8,9,2,22,26])).
% 77.02/77.09 cnf(3360,plain,
% 77.02/77.09 (~P1(f5(a2,a1),a7)),
% 77.02/77.09 inference(scs_inference,[],[30,2481,3301,3180,3226,3161,3165,3268,3209,2982,3346,3098,1337,1745,2365,410,41,49,58,47,5,19,4,10,12,11,6,17,13,7,18,14,16,15,8,9,2,22,26,20,21,3,59,57])).
% 77.02/77.09 cnf(3407,plain,
% 77.02/77.09 (P3(a7,f5(a2,a1))+~P3(f5(a2,a1),a7)),
% 77.02/77.09 inference(scs_inference,[],[30,3360,3260,3174,2747,1987,3152,3159,2990,2910,3347,3099,2833,3201,2621,1523,1904,3108,252,1939,49,47,58,5,4,19,10,12,11,6,18,7,17,13,14,16,8,15,9,2,59,22,26,20,21,3,57,81,24,45])).
% 77.02/77.09 cnf(3684,plain,
% 77.02/77.09 (P3(a7,f5(a2,a1))),
% 77.02/77.09 inference(scs_inference,[],[3407,42])).
% 77.02/77.09 cnf(3687,plain,
% 77.02/77.09 (~P5(f8(a2,a7),a1,f6(a2,a1,f5(a2,a1),a7))),
% 77.02/77.09 inference(scs_inference,[],[3684,2921])).
% 77.02/77.09 cnf(3688,plain,
% 77.02/77.09 (P5(f8(a2,a7),a1,f6(a2,a1,f5(a2,a1),a7))),
% 77.02/77.09 inference(scs_inference,[],[3684,3316])).
% 77.02/77.09 cnf(3748,plain,
% 77.02/77.09 ($false),
% 77.02/77.09 inference(scs_inference,[],[3688,3687]),
% 77.02/77.09 ['proof']).
% 77.02/77.09 % SZS output end Proof
% 77.02/77.09 % Total time :76.390000s
%------------------------------------------------------------------------------