%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : SWV398+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 : n028.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:05 EDT 2024
% Result : Theorem 77.95s 78.05s
% Output : CNFRefutation 78.03s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.04/0.14 % Problem : SWV398+1 : TPTP v8.2.0. Released v3.3.0.
% 0.04/0.14 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% 0.14/0.36 % Computer : n028.cluster.edu
% 0.14/0.36 % Model : x86_64 x86_64
% 0.14/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.36 % Memory : 8042.1875MB
% 0.14/0.36 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.36 % CPULimit : 300
% 0.14/0.36 % WCLimit : 300
% 0.14/0.36 % DateTime : Thu Jun 20 18:51:39 EDT 2024
% 0.14/0.36 % CPUTime :
% 0.57/0.65 start to proof:theBenchmark
% 77.95/78.03 %-------------------------------------------
% 77.95/78.03 % File :CSE---1.7
% 77.95/78.03 % Problem :theBenchmark
% 77.95/78.03 % Transform :cnf
% 77.95/78.03 % Format :tptp:raw
% 77.95/78.03 % Command :java -jar mcs_scs.jar %d %s
% 77.95/78.03
% 77.95/78.03 % Result :Theorem 77.320000s
% 77.95/78.03 % Output :CNFRefutation 77.320000s
% 77.95/78.03 %-------------------------------------------
% 77.95/78.05 %------------------------------------------------------------------------------
% 77.95/78.05 % File : SWV398+1 : TPTP v8.2.0. Released v3.3.0.
% 77.95/78.05 % Domain : Software Verification
% 77.95/78.05 % Problem : Priority queue checker: tmp_not_check_03
% 77.95/78.05 % Version : [dNP05] axioms.
% 77.95/78.05 % English :
% 77.95/78.05
% 77.95/78.05 % Refs : [Pis06] Piskac (2006), Email to Geoff Sutcliffe
% 77.95/78.05 % : [dNP05] de Nivelle & Piskac (2005), Verification of an Off-Lin
% 77.95/78.05 % Source : [Pis06]
% 77.95/78.05 % Names : cpq_l034 [Pis06]
% 77.95/78.05
% 77.95/78.05 % Status : Theorem
% 77.95/78.05 % Rating : 0.56 v8.2.0, 0.58 v8.1.0, 0.50 v7.5.0, 0.53 v7.3.0, 0.59 v7.1.0, 0.52 v7.0.0, 0.57 v6.4.0, 0.62 v6.2.0, 0.72 v6.1.0, 0.77 v6.0.0, 0.74 v5.5.0, 0.81 v5.4.0, 0.79 v5.3.0, 0.85 v5.2.0, 0.80 v5.1.0, 0.81 v5.0.0, 0.79 v4.1.0, 0.78 v4.0.1, 0.83 v4.0.0, 0.88 v3.7.0, 0.85 v3.5.0, 0.89 v3.4.0, 0.84 v3.3.0
% 77.95/78.05 % Syntax : Number of formulae : 44 ( 16 unt; 0 def)
% 77.95/78.05 % Number of atoms : 91 ( 29 equ)
% 77.95/78.05 % Maximal formula atoms : 4 ( 2 avg)
% 77.95/78.05 % Number of connectives : 62 ( 15 ~; 3 |; 14 &)
% 77.95/78.05 % ( 8 <=>; 22 =>; 0 <=; 0 <~>)
% 77.95/78.05 % Maximal formula depth : 9 ( 5 avg)
% 77.95/78.05 % Maximal term depth : 4 ( 1 avg)
% 77.95/78.05 % Number of predicates : 11 ( 9 usr; 1 prp; 0-3 aty)
% 77.95/78.05 % Number of functors : 18 ( 18 usr; 3 con; 0-3 aty)
% 77.95/78.05 % Number of variables : 131 ( 127 !; 4 ?)
% 77.95/78.05 % SPC : FOF_THM_RFO_SEQ
% 77.95/78.05
% 77.95/78.05 % Comments :
% 77.95/78.05 %------------------------------------------------------------------------------
% 77.95/78.05 %----Include the axioms about priority queues and checked priority queues
% 77.95/78.05 include('Axioms/SWV007+0.ax').
% 77.95/78.05 include('Axioms/SWV007+2.ax').
% 77.95/78.05 include('Axioms/SWV007+3.ax').
% 77.95/78.05 %------------------------------------------------------------------------------
% 77.95/78.05 %----lemma_check_characterization (cpq_l041.p, cpq_l042.p)
% 77.95/78.05 fof(l26_li4142,lemma,
% 77.95/78.05 ! [U,V,W] :
% 77.95/78.05 ( check_cpq(triple(U,V,W))
% 77.95/78.05 <=> ! [X,Y] :
% 77.95/78.05 ( pair_in_list(V,X,Y)
% 77.95/78.05 => less_than(Y,X) ) ) ).
% 77.95/78.05
% 77.95/78.05 %----tmp_not_check_03_1 (cpq_l035.p)
% 77.95/78.05 fof(l34_l35,lemma,
% 77.95/78.05 ! [U] :
% 77.95/78.05 ( ? [V,W] :
% 77.95/78.05 ( pair_in_list(U,V,W)
% 77.95/78.05 & strictly_less_than(V,W) )
% 77.95/78.05 => ! [X] :
% 77.95/78.05 ? [Y,Z] :
% 77.95/78.05 ( pair_in_list(update_slb(U,X),Y,Z)
% 77.95/78.05 & strictly_less_than(Y,Z) ) ) ).
% 77.95/78.05
% 77.95/78.05 %----tmp_not_check_03 (conjecture)
% 77.95/78.05 fof(l24_co,conjecture,
% 77.95/78.05 ! [U,V,W] :
% 77.95/78.05 ( ~ check_cpq(triple(U,V,W))
% 77.95/78.05 => ~ check_cpq(findmin_cpq_eff(triple(U,V,W))) ) ).
% 77.95/78.05
% 77.95/78.05 %------------------------------------------------------------------------------
% 77.95/78.05 %-------------------------------------------
% 77.95/78.05 % Proof found
% 77.95/78.05 % SZS status Theorem for theBenchmark
% 77.95/78.05 % SZS output start Proof
% 77.95/78.06 %ClaNum:106(EqnAxiom:51)
% 77.95/78.06 %VarNum:342(SingletonVarNum:166)
% 77.95/78.06 %MaxLitNum:4
% 77.95/78.06 %MaxfuncDepth:3
% 77.95/78.06 %SharedTerms:11
% 77.95/78.06 %goalClause: 62 67
% 77.95/78.06 %singleGoalClaCount:2
% 77.95/78.06 [64]~P2(a1)
% 77.95/78.06 [67]~P3(f23(a9,a14,a15))
% 77.95/78.06 [62]P3(f8(f23(a9,a14,a15)))
% 77.95/78.06 [53]P1(a2,x531)
% 77.95/78.06 [54]P1(x541,x541)
% 77.95/78.06 [55]P6(x551,x551)
% 77.95/78.06 [65]~P4(a1,x651)
% 77.95/78.06 [52]E(f4(a1,x521),a1)
% 77.95/78.06 [66]~P7(a1,x661,x662)
% 77.95/78.06 [60]P3(f23(x601,a1,x602))
% 77.95/78.06 [68]~P8(f23(x681,x682,a3))
% 77.95/78.06 [59]E(f7(f23(x591,a1,x592)),a2)
% 77.95/78.06 [61]E(f8(f23(x611,a1,x612)),f23(x611,a1,a3))
% 77.95/78.06 [56]P2(f6(x561,f5(x562,x563)))
% 77.95/78.06 [57]E(f20(f6(x571,f5(x572,x573)),x572),x571)
% 77.95/78.06 [58]E(f19(f6(x581,f5(x582,x583)),x582),x583)
% 77.95/78.06 [63]E(f23(f16(x631,x632),f6(x633,f5(x632,a2)),x634),f17(f23(x631,x633,x634),x632))
% 77.95/78.06 [69]P1(x692,x691)+P1(x691,x692)
% 77.95/78.06 [70]~P9(x701,x702)+P1(x701,x702)
% 77.95/78.06 [72]~P9(x722,x721)+~P1(x721,x722)
% 77.95/78.06 [71]~P6(x711,x712)+P6(x711,f8(x712))
% 77.95/78.06 [77]~P6(x771,x772)+P6(x771,f21(f8(x772),f7(x772)))
% 77.95/78.06 [75]~P6(x751,x752)+P6(x751,f17(x752,x753))
% 77.95/78.06 [76]~P6(x761,x762)+P6(x761,f21(x762,x763))
% 77.95/78.06 [79]E(x791,a3)+P8(f23(x792,x793,x791))
% 77.95/78.06 [92]~P1(f11(x921,x922),f12(x921,x922))+P3(f23(x921,x922,x923))
% 77.95/78.06 [93]P7(x932,f12(x931,x932),f11(x931,x932))+P3(f23(x931,x932,x933))
% 77.95/78.06 [81]E(x811,a1)+E(f7(f23(x812,x811,x813)),f18(x812))
% 77.95/78.06 [84]~P4(x842,x844)+P5(f23(x841,x842,x843),x844)
% 77.95/78.06 [91]P4(x911,x912)+~P5(f23(x913,x911,x914),x912)
% 77.95/78.06 [78]~E(x782,x784)+P4(f6(x781,f5(x782,x783)),x784)
% 77.95/78.06 [80]~P4(x801,x804)+P4(f6(x801,f5(x802,x803)),x804)
% 77.95/78.06 [90]P4(x902,x904)+E(f21(f23(x901,x902,x903),x904),f23(x901,x902,a3))
% 77.95/78.06 [87]~P1(x872,x874)+E(f6(f4(x871,x872),f5(x873,x874)),f4(f6(x871,f5(x873,x874)),x872))
% 77.95/78.06 [88]~P9(x883,x884)+E(f4(f6(x881,f5(x882,x883)),x884),f6(f4(x881,x884),f5(x882,x884)))
% 77.95/78.06 [94]~P7(x941,x944,x945)+P7(f6(x941,f5(x942,x943)),x944,x945)
% 77.95/78.06 [104]~P9(x1041,x1042)+~P3(f23(x1043,f6(x1044,f5(x1041,x1042)),x1045))
% 77.95/78.06 [73]P9(x732,x731)+~P1(x732,x731)+P1(x731,x732)
% 77.95/78.06 [74]~P1(x741,x743)+P1(x741,x742)+~P1(x743,x742)
% 77.95/78.06 [95]P4(x951,f18(x952))+E(x951,a1)+E(f8(f23(x952,x951,x953)),f23(x952,f4(x951,f18(x952)),a3))
% 77.95/78.06 [86]~P7(x861,x863,x864)+~P9(x863,x864)+P9(f10(x861,x862),f13(x861,x862))
% 77.95/78.06 [96]~P7(x961,x963,x964)+~P9(x963,x964)+P7(f4(x961,x962),f10(x961,x962),f13(x961,x962))
% 77.95/78.06 [85]E(x851,x852)+P4(x853,x852)+~P4(f6(x853,f5(x851,x854)),x852)
% 77.95/78.06 [100]~P4(x1002,x1004)+~P9(x1004,f19(x1002,x1004))+E(f21(f23(x1001,x1002,x1003),x1004),f23(f22(x1001,x1004),f20(x1002,x1004),a3))
% 77.95/78.06 [101]~P4(x1013,x1012)+~P1(f19(x1013,x1012),x1012)+E(f23(f22(x1011,x1012),f20(x1013,x1012),x1014),f21(f23(x1011,x1013,x1014),x1012))
% 77.95/78.06 [82]~P4(x823,x822)+E(x821,x822)+E(f19(f6(x823,f5(x821,x824)),x822),f19(x823,x822))
% 77.95/78.06 [89]~P4(x893,x892)+E(x891,x892)+E(f20(f6(x893,f5(x891,x894)),x892),f6(f20(x893,x892),f5(x891,x894)))
% 77.95/78.06 [99]P1(x991,x992)+~P7(x993,x992,x991)+~P3(f23(x994,x993,x995))
% 77.95/78.06 [83]~E(x833,x835)+~E(x832,x834)+P7(f6(x831,f5(x832,x833)),x834,x835)
% 77.95/78.07 [97]E(x971,x972)+P7(x973,x974,x972)+~P7(f6(x973,f5(x975,x971)),x974,x972)
% 77.95/78.07 [98]E(x981,x982)+P7(x983,x982,x984)+~P7(f6(x983,f5(x981,x985)),x982,x984)
% 77.95/78.07 [105]~P1(x1054,x1053)+~P3(f23(x1051,x1052,x1055))+P3(f23(x1051,f6(x1052,f5(x1053,x1054)),x1055))
% 77.95/78.07 [106]~P1(x1064,x1065)+P3(f23(x1061,x1062,x1063))+~P3(f23(x1061,f6(x1062,f5(x1065,x1064)),x1063))
% 77.95/78.07 [102]~P4(x1021,f18(x1022))+E(x1021,a1)+~P9(f18(x1022),f19(x1021,f18(x1022)))+E(f8(f23(x1022,x1021,x1023)),f23(x1022,f4(x1021,f18(x1022)),a3))
% 77.95/78.07 [103]~P4(x1031,f18(x1032))+E(x1031,a1)+~P1(f19(x1031,f18(x1032)),f18(x1032))+E(f23(x1032,f4(x1031,f18(x1032)),x1033),f8(f23(x1032,x1031,x1033)))
% 77.95/78.07 %EqnAxiom
% 77.95/78.07 [1]E(x11,x11)
% 77.95/78.07 [2]E(x22,x21)+~E(x21,x22)
% 77.95/78.07 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 77.95/78.07 [4]~E(x41,x42)+E(f4(x41,x43),f4(x42,x43))
% 77.95/78.07 [5]~E(x51,x52)+E(f4(x53,x51),f4(x53,x52))
% 77.95/78.07 [6]~E(x61,x62)+E(f5(x61,x63),f5(x62,x63))
% 77.95/78.07 [7]~E(x71,x72)+E(f5(x73,x71),f5(x73,x72))
% 77.95/78.07 [8]~E(x81,x82)+E(f6(x81,x83),f6(x82,x83))
% 77.95/78.07 [9]~E(x91,x92)+E(f6(x93,x91),f6(x93,x92))
% 77.95/78.07 [10]~E(x101,x102)+E(f23(x101,x103,x104),f23(x102,x103,x104))
% 77.95/78.07 [11]~E(x111,x112)+E(f23(x113,x111,x114),f23(x113,x112,x114))
% 77.95/78.07 [12]~E(x121,x122)+E(f23(x123,x124,x121),f23(x123,x124,x122))
% 77.95/78.07 [13]~E(x131,x132)+E(f18(x131),f18(x132))
% 77.95/78.07 [14]~E(x141,x142)+E(f20(x141,x143),f20(x142,x143))
% 77.95/78.07 [15]~E(x151,x152)+E(f20(x153,x151),f20(x153,x152))
% 77.95/78.07 [16]~E(x161,x162)+E(f19(x161,x163),f19(x162,x163))
% 77.95/78.07 [17]~E(x171,x172)+E(f19(x173,x171),f19(x173,x172))
% 77.95/78.07 [18]~E(x181,x182)+E(f21(x181,x183),f21(x182,x183))
% 77.95/78.07 [19]~E(x191,x192)+E(f21(x193,x191),f21(x193,x192))
% 77.95/78.07 [20]~E(x201,x202)+E(f22(x201,x203),f22(x202,x203))
% 77.95/78.07 [21]~E(x211,x212)+E(f22(x213,x211),f22(x213,x212))
% 77.95/78.07 [22]~E(x221,x222)+E(f13(x221,x223),f13(x222,x223))
% 77.95/78.07 [23]~E(x231,x232)+E(f13(x233,x231),f13(x233,x232))
% 77.95/78.07 [24]~E(x241,x242)+E(f7(x241),f7(x242))
% 77.95/78.07 [25]~E(x251,x252)+E(f8(x251),f8(x252))
% 77.95/78.07 [26]~E(x261,x262)+E(f10(x261,x263),f10(x262,x263))
% 77.95/78.07 [27]~E(x271,x272)+E(f10(x273,x271),f10(x273,x272))
% 77.95/78.07 [28]~E(x281,x282)+E(f17(x281,x283),f17(x282,x283))
% 77.95/78.07 [29]~E(x291,x292)+E(f17(x293,x291),f17(x293,x292))
% 77.95/78.07 [30]~E(x301,x302)+E(f12(x301,x303),f12(x302,x303))
% 77.95/78.07 [31]~E(x311,x312)+E(f12(x313,x311),f12(x313,x312))
% 77.95/78.07 [32]~E(x321,x322)+E(f11(x321,x323),f11(x322,x323))
% 77.95/78.07 [33]~E(x331,x332)+E(f11(x333,x331),f11(x333,x332))
% 77.95/78.07 [34]~E(x341,x342)+E(f16(x341,x343),f16(x342,x343))
% 77.95/78.07 [35]~E(x351,x352)+E(f16(x353,x351),f16(x353,x352))
% 77.95/78.07 [36]P1(x362,x363)+~E(x361,x362)+~P1(x361,x363)
% 77.95/78.07 [37]P1(x373,x372)+~E(x371,x372)+~P1(x373,x371)
% 77.95/78.07 [38]~P3(x381)+P3(x382)+~E(x381,x382)
% 77.95/78.07 [39]P6(x392,x393)+~E(x391,x392)+~P6(x391,x393)
% 77.95/78.07 [40]P6(x403,x402)+~E(x401,x402)+~P6(x403,x401)
% 77.95/78.07 [41]~P2(x411)+P2(x412)+~E(x411,x412)
% 77.95/78.07 [42]P7(x422,x423,x424)+~E(x421,x422)+~P7(x421,x423,x424)
% 77.95/78.07 [43]P7(x433,x432,x434)+~E(x431,x432)+~P7(x433,x431,x434)
% 77.95/78.07 [44]P7(x443,x444,x442)+~E(x441,x442)+~P7(x443,x444,x441)
% 77.95/78.07 [45]P4(x452,x453)+~E(x451,x452)+~P4(x451,x453)
% 77.95/78.07 [46]P4(x463,x462)+~E(x461,x462)+~P4(x463,x461)
% 77.95/78.07 [47]~P8(x471)+P8(x472)+~E(x471,x472)
% 77.95/78.07 [48]P5(x482,x483)+~E(x481,x482)+~P5(x481,x483)
% 77.95/78.07 [49]P5(x493,x492)+~E(x491,x492)+~P5(x493,x491)
% 77.95/78.07 [50]P9(x502,x503)+~E(x501,x502)+~P9(x501,x503)
% 77.95/78.07 [51]P9(x513,x512)+~E(x511,x512)+~P9(x513,x511)
% 77.95/78.07
% 77.95/78.07 %-------------------------------------------
% 78.03/78.09 cnf(107,plain,
% 78.03/78.09 (P4(f6(x1072,f5(x1071,x1073)),x1071)),
% 78.03/78.09 inference(equality_inference,[],[78])).
% 78.03/78.09 cnf(108,plain,
% 78.03/78.09 (~P1(f11(a9,a14),f12(a9,a14))),
% 78.03/78.09 inference(scs_inference,[],[67,92])).
% 78.03/78.09 cnf(110,plain,
% 78.03/78.09 (P7(a14,f12(a9,a14),f11(a9,a14))),
% 78.03/78.09 inference(scs_inference,[],[67,92,93])).
% 78.03/78.09 cnf(112,plain,
% 78.03/78.09 (P1(f12(a9,a14),f11(a9,a14))),
% 78.03/78.09 inference(scs_inference,[],[67,92,93,69])).
% 78.03/78.09 cnf(116,plain,
% 78.03/78.09 (E(a1,f4(a1,x1161))),
% 78.03/78.09 inference(scs_inference,[],[67,52,92,93,69,70,2])).
% 78.03/78.09 cnf(117,plain,
% 78.03/78.09 (~P9(x1171,x1171)),
% 78.03/78.09 inference(scs_inference,[],[67,54,52,92,93,69,70,2,72])).
% 78.03/78.09 cnf(119,plain,
% 78.03/78.09 (~P3(f20(f6(f23(a9,a14,a15),f5(x1191,x1192)),x1191))),
% 78.03/78.09 inference(scs_inference,[],[67,54,52,57,92,93,69,70,2,72,38])).
% 78.03/78.09 cnf(120,plain,
% 78.03/78.09 (E(f20(f6(x1201,f5(x1202,x1203)),x1202),x1201)),
% 78.03/78.09 inference(rename_variables,[],[57])).
% 78.03/78.09 cnf(121,plain,
% 78.03/78.09 (P9(f12(a9,a14),f11(a9,a14))),
% 78.03/78.09 inference(scs_inference,[],[67,54,52,57,92,93,69,70,2,72,38,73])).
% 78.03/78.09 cnf(123,plain,
% 78.03/78.09 (E(f20(f6(f4(a1,x1231),f5(x1232,x1233)),x1232),a1)),
% 78.03/78.09 inference(scs_inference,[],[67,54,52,57,120,92,93,69,70,2,72,38,73,3])).
% 78.03/78.09 cnf(126,plain,
% 78.03/78.09 (P1(x1261,x1261)),
% 78.03/78.09 inference(rename_variables,[],[54])).
% 78.03/78.09 cnf(129,plain,
% 78.03/78.09 (~E(a14,a1)),
% 78.03/78.09 inference(scs_inference,[],[67,54,126,66,52,57,120,92,93,69,70,2,72,38,73,3,36,37,42])).
% 78.03/78.09 cnf(131,plain,
% 78.03/78.09 (P6(a1,f4(a1,x1311))),
% 78.03/78.09 inference(scs_inference,[],[67,54,126,66,52,57,120,55,92,93,69,70,2,72,38,73,3,36,37,42,39])).
% 78.03/78.09 cnf(132,plain,
% 78.03/78.09 (P6(x1321,x1321)),
% 78.03/78.09 inference(rename_variables,[],[55])).
% 78.03/78.09 cnf(133,plain,
% 78.03/78.09 (P6(f4(a1,x1331),a1)),
% 78.03/78.09 inference(scs_inference,[],[67,54,126,66,52,57,120,55,132,92,93,69,70,2,72,38,73,3,36,37,42,39,40])).
% 78.03/78.09 cnf(135,plain,
% 78.03/78.09 (~P2(f4(a1,x1351))),
% 78.03/78.09 inference(scs_inference,[],[67,54,126,66,52,57,120,55,132,64,92,93,69,70,2,72,38,73,3,36,37,42,39,40,41])).
% 78.03/78.09 cnf(136,plain,
% 78.03/78.09 (~E(f6(x1361,f5(x1362,x1363)),a1)),
% 78.03/78.09 inference(scs_inference,[],[67,54,126,66,52,57,120,107,55,132,65,64,92,93,69,70,2,72,38,73,3,36,37,42,39,40,41,45])).
% 78.03/78.09 cnf(137,plain,
% 78.03/78.09 (P4(f6(x1371,f5(x1372,x1373)),x1372)),
% 78.03/78.09 inference(rename_variables,[],[107])).
% 78.03/78.09 cnf(138,plain,
% 78.03/78.09 (P4(f6(x1381,f5(f4(a1,x1382),x1383)),a1)),
% 78.03/78.09 inference(scs_inference,[],[67,54,126,66,52,57,120,107,137,55,132,65,64,92,93,69,70,2,72,38,73,3,36,37,42,39,40,41,45,46])).
% 78.03/78.09 cnf(140,plain,
% 78.03/78.09 (~P8(f8(f23(x1401,a1,x1402)))),
% 78.03/78.09 inference(scs_inference,[],[67,54,126,66,52,61,57,120,107,137,55,132,65,64,68,92,93,69,70,2,72,38,73,3,36,37,42,39,40,41,45,46,47])).
% 78.03/78.09 cnf(143,plain,
% 78.03/78.09 (P7(a14,x1431,f11(a9,a14))+~E(f12(a9,a14),x1431)),
% 78.03/78.09 inference(scs_inference,[],[67,54,126,66,52,61,57,120,107,137,55,132,65,64,68,92,93,69,70,2,72,38,73,3,36,37,42,39,40,41,45,46,47,43])).
% 78.03/78.09 cnf(144,plain,
% 78.03/78.09 (P7(a14,f12(a9,a14),x1441)+~E(f11(a9,a14),x1441)),
% 78.03/78.09 inference(scs_inference,[],[67,54,126,66,52,61,57,120,107,137,55,132,65,64,68,92,93,69,70,2,72,38,73,3,36,37,42,39,40,41,45,46,47,43,44])).
% 78.03/78.09 cnf(145,plain,
% 78.03/78.09 (P9(x1451,f11(a9,a14))+~E(f12(a9,a14),x1451)),
% 78.03/78.09 inference(scs_inference,[],[67,54,126,66,52,61,57,120,107,137,55,132,65,64,68,92,93,69,70,2,72,38,73,3,36,37,42,39,40,41,45,46,47,43,44,50])).
% 78.03/78.09 cnf(149,plain,
% 78.03/78.09 (~P9(x1491,a2)),
% 78.03/78.09 inference(scs_inference,[],[53,72])).
% 78.03/78.09 cnf(151,plain,
% 78.03/78.09 (E(a1,f20(f6(f4(a1,x1511),f5(x1512,x1513)),x1512))),
% 78.03/78.09 inference(scs_inference,[],[53,123,72,2])).
% 78.03/78.09 cnf(153,plain,
% 78.03/78.09 (~E(a2,f11(a9,a14))),
% 78.03/78.09 inference(scs_inference,[],[108,53,123,64,72,2,41,36])).
% 78.03/78.09 cnf(155,plain,
% 78.03/78.09 (P4(f6(x1551,f5(f4(a1,x1552),x1553)),f4(a1,x1554))),
% 78.03/78.09 inference(scs_inference,[],[108,53,123,116,138,64,72,2,41,36,46])).
% 78.03/78.09 cnf(157,plain,
% 78.03/78.09 (~E(a14,f20(f6(f4(a1,x1571),f5(x1572,x1573)),x1572))),
% 78.03/78.09 inference(scs_inference,[],[108,53,123,116,129,131,138,64,72,2,41,36,46,39,3])).
% 78.03/78.09 cnf(160,plain,
% 78.03/78.09 (P6(f20(f6(f4(a1,x1601),f5(x1602,x1603)),x1602),a1)),
% 78.03/78.09 inference(scs_inference,[],[108,53,123,116,129,57,131,140,138,55,64,72,2,41,36,46,39,3,47,40])).
% 78.03/78.09 cnf(162,plain,
% 78.03/78.09 (E(f4(a1,x1621),f4(a1,x1622))),
% 78.03/78.09 inference(scs_inference,[],[108,53,123,116,129,57,131,140,138,55,65,64,72,2,41,36,46,39,3,47,40,85])).
% 78.03/78.09 cnf(165,plain,
% 78.03/78.09 (P1(f12(a9,a14),x1651)+~E(f11(a9,a14),x1651)),
% 78.03/78.09 inference(scs_inference,[],[108,112,53,123,116,129,57,131,140,138,55,65,64,72,2,41,36,46,39,3,47,40,85,37])).
% 78.03/78.09 cnf(168,plain,
% 78.03/78.09 (E(x1681,f19(f6(x1682,f5(x1683,x1681)),x1683))),
% 78.03/78.09 inference(scs_inference,[],[58,2])).
% 78.03/78.09 cnf(169,plain,
% 78.03/78.09 (P6(f20(f6(f4(a1,x1691),f5(x1692,x1693)),x1692),f4(a1,x1694))),
% 78.03/78.09 inference(scs_inference,[],[151,58,131,2,39])).
% 78.03/78.09 cnf(170,plain,
% 78.03/78.09 (E(f19(f6(x1701,f5(x1702,a1)),x1702),f4(a1,x1703))),
% 78.03/78.09 inference(scs_inference,[],[151,58,116,131,2,39,3])).
% 78.03/78.09 cnf(172,plain,
% 78.03/78.09 (P6(f4(a1,x1721),f20(f6(f4(a1,x1722),f5(x1723,x1724)),x1723))),
% 78.03/78.09 inference(scs_inference,[],[151,58,116,133,131,2,39,3,40])).
% 78.03/78.09 cnf(174,plain,
% 78.03/78.09 (P1(x1741,f11(a9,a14))+~E(f12(a9,a14),x1741)),
% 78.03/78.09 inference(scs_inference,[],[112,151,58,63,116,133,131,2,39,3,40,41,36])).
% 78.03/78.09 cnf(178,plain,
% 78.03/78.09 (E(f23(x1781,a1,a3),f8(f23(x1781,a1,x1782)))),
% 78.03/78.09 inference(scs_inference,[],[61,2])).
% 78.03/78.09 cnf(181,plain,
% 78.03/78.09 (P6(f19(f6(x1811,f5(x1812,a1)),x1812),f4(a1,x1813))),
% 78.03/78.09 inference(scs_inference,[],[61,168,170,135,131,2,41,39])).
% 78.03/78.09 cnf(182,plain,
% 78.03/78.09 (E(x1821,f19(f6(x1822,f5(x1823,x1821)),x1823))),
% 78.03/78.09 inference(rename_variables,[],[168])).
% 78.03/78.09 cnf(183,plain,
% 78.03/78.09 (E(f20(f6(f8(f23(x1831,a1,x1832)),f5(x1833,x1834)),x1833),f23(x1831,a1,a3))),
% 78.03/78.09 inference(scs_inference,[],[61,57,168,170,135,131,2,41,39,3])).
% 78.03/78.09 cnf(187,plain,
% 78.03/78.09 (P6(f4(a1,x1871),f19(f6(x1872,f5(x1873,a1)),x1873))),
% 78.03/78.09 inference(scs_inference,[],[60,61,57,168,182,170,135,133,131,2,41,39,3,38,40])).
% 78.03/78.09 cnf(190,plain,
% 78.03/78.09 (E(x1901,f20(f6(x1901,f5(x1902,x1903)),x1902))),
% 78.03/78.09 inference(scs_inference,[],[57,2])).
% 78.03/78.09 cnf(191,plain,
% 78.03/78.09 (P2(f20(f6(f6(x1911,f5(x1912,x1913)),f5(x1914,x1915)),x1914))),
% 78.03/78.09 inference(scs_inference,[],[57,56,2,41])).
% 78.03/78.09 cnf(192,plain,
% 78.03/78.09 (P6(f23(x1921,a1,a3),f8(f23(x1921,a1,x1922)))),
% 78.03/78.09 inference(scs_inference,[],[61,57,56,55,2,41,39])).
% 78.03/78.09 cnf(193,plain,
% 78.03/78.09 (P6(x1931,x1931)),
% 78.03/78.09 inference(rename_variables,[],[55])).
% 78.03/78.09 cnf(194,plain,
% 78.03/78.09 (E(f8(f23(x1941,a1,x1942)),f8(f23(x1941,a1,x1943)))),
% 78.03/78.09 inference(scs_inference,[],[61,57,178,56,55,2,41,39,3])).
% 78.03/78.09 cnf(196,plain,
% 78.03/78.09 (P6(f8(f23(x1961,a1,x1962)),f23(x1961,a1,a3))),
% 78.03/78.09 inference(scs_inference,[],[61,57,178,56,55,193,2,41,39,3,40])).
% 78.03/78.09 cnf(201,plain,
% 78.03/78.09 (P9(f20(f6(f12(a9,a14),f5(x2011,x2012)),x2011),f11(a9,a14))),
% 78.03/78.09 inference(scs_inference,[],[190,145])).
% 78.03/78.09 cnf(202,plain,
% 78.03/78.09 (E(x2021,f20(f6(x2021,f5(x2022,x2023)),x2022))),
% 78.03/78.09 inference(rename_variables,[],[190])).
% 78.03/78.09 cnf(203,plain,
% 78.03/78.09 (P1(f12(a9,a14),f20(f6(f11(a9,a14),f5(x2031,x2032)),x2031))),
% 78.03/78.09 inference(scs_inference,[],[190,202,145,165])).
% 78.03/78.09 cnf(204,plain,
% 78.03/78.09 (E(x2041,f20(f6(x2041,f5(x2042,x2043)),x2042))),
% 78.03/78.09 inference(rename_variables,[],[190])).
% 78.03/78.09 cnf(205,plain,
% 78.03/78.09 (P1(f20(f6(f12(a9,a14),f5(x2051,x2052)),x2051),f11(a9,a14))),
% 78.03/78.09 inference(scs_inference,[],[190,202,204,145,165,174])).
% 78.03/78.09 cnf(206,plain,
% 78.03/78.09 (E(x2061,f20(f6(x2061,f5(x2062,x2063)),x2062))),
% 78.03/78.09 inference(rename_variables,[],[190])).
% 78.03/78.09 cnf(209,plain,
% 78.03/78.09 (E(f23(x2091,a1,a3),f20(f6(f8(f23(x2091,a1,x2092)),f5(x2093,x2094)),x2093))),
% 78.03/78.09 inference(scs_inference,[],[183,190,202,204,145,165,174,72,2])).
% 78.03/78.09 cnf(211,plain,
% 78.03/78.09 (~P9(x2111,x2111)),
% 78.03/78.09 inference(rename_variables,[],[117])).
% 78.03/78.09 cnf(214,plain,
% 78.03/78.09 (P7(a14,f12(a9,a14),f20(f6(f11(a9,a14),f5(x2141,x2142)),x2141))),
% 78.03/78.09 inference(scs_inference,[],[110,183,190,202,204,206,117,211,145,165,174,72,2,51,50,44])).
% 78.03/78.09 cnf(215,plain,
% 78.03/78.09 (E(x2151,f20(f6(x2151,f5(x2152,x2153)),x2152))),
% 78.03/78.09 inference(rename_variables,[],[190])).
% 78.03/78.09 cnf(216,plain,
% 78.03/78.09 (P7(a14,f20(f6(f12(a9,a14),f5(x2161,x2162)),x2161),f11(a9,a14))),
% 78.03/78.09 inference(scs_inference,[],[110,183,190,202,204,206,215,117,211,145,165,174,72,2,51,50,44,43])).
% 78.03/78.09 cnf(217,plain,
% 78.03/78.09 (E(x2171,f20(f6(x2171,f5(x2172,x2173)),x2172))),
% 78.03/78.09 inference(rename_variables,[],[190])).
% 78.03/78.09 cnf(218,plain,
% 78.03/78.09 (P6(f20(f6(f23(x2181,a1,a3),f5(x2182,x2183)),x2182),f8(f23(x2181,a1,x2184)))),
% 78.03/78.09 inference(scs_inference,[],[110,183,190,202,204,206,215,217,117,211,192,145,165,174,72,2,51,50,44,43,39])).
% 78.03/78.09 cnf(219,plain,
% 78.03/78.09 (E(x2191,f20(f6(x2191,f5(x2192,x2193)),x2192))),
% 78.03/78.09 inference(rename_variables,[],[190])).
% 78.03/78.09 cnf(220,plain,
% 78.03/78.09 (~E(a14,f4(a1,x2201))),
% 78.03/78.09 inference(scs_inference,[],[110,183,190,202,204,206,215,217,219,157,117,211,192,145,165,174,72,2,51,50,44,43,39,3])).
% 78.03/78.09 cnf(221,plain,
% 78.03/78.09 (E(x2211,f20(f6(x2211,f5(x2212,x2213)),x2212))),
% 78.03/78.09 inference(rename_variables,[],[190])).
% 78.03/78.09 cnf(223,plain,
% 78.03/78.09 (E(x2231,f20(f6(x2231,f5(x2232,x2233)),x2232))),
% 78.03/78.09 inference(rename_variables,[],[190])).
% 78.03/78.09 cnf(224,plain,
% 78.03/78.09 (P6(f8(f23(x2241,a1,x2242)),f20(f6(f23(x2241,a1,a3),f5(x2243,x2244)),x2243))),
% 78.03/78.09 inference(scs_inference,[],[62,110,183,190,202,204,206,215,217,219,221,223,157,117,211,196,192,145,165,174,72,2,51,50,44,43,39,3,38,40])).
% 78.03/78.09 cnf(232,plain,
% 78.03/78.09 (E(f4(a1,x2321),f19(f6(x2322,f5(x2323,a1)),x2323))),
% 78.03/78.09 inference(scs_inference,[],[170,205,72,2])).
% 78.03/78.09 cnf(233,plain,
% 78.03/78.09 (~E(f11(a9,a14),a2)),
% 78.03/78.09 inference(scs_inference,[],[121,170,205,149,72,2,51])).
% 78.03/78.09 cnf(237,plain,
% 78.03/78.09 (~E(a14,f19(f6(x2371,f5(x2372,a1)),x2372))),
% 78.03/78.09 inference(scs_inference,[],[121,61,170,205,220,224,149,72,2,51,39,3])).
% 78.03/78.09 cnf(246,plain,
% 78.03/78.09 (E(f17(f23(x2461,x2462,x2463),x2464),f23(f16(x2461,x2464),f6(x2462,f5(x2464,a2)),x2463))),
% 78.03/78.09 inference(scs_inference,[],[63,2])).
% 78.03/78.09 cnf(249,plain,
% 78.03/78.09 (E(f8(f23(x2491,a1,x2492)),f20(f6(f8(f23(x2491,a1,x2493)),f5(x2494,x2495)),x2494))),
% 78.03/78.09 inference(scs_inference,[],[61,190,209,63,131,2,39,3])).
% 78.03/78.09 cnf(257,plain,
% 78.03/78.09 (E(f20(f6(f8(f23(x2571,a1,x2572)),f5(x2573,x2574)),x2573),f8(f23(x2571,a1,x2575)))),
% 78.03/78.09 inference(scs_inference,[],[249,2])).
% 78.03/78.09 cnf(261,plain,
% 78.03/78.09 (P6(a1,f20(f6(f4(a1,x2611),f5(x2612,x2613)),x2612))),
% 78.03/78.09 inference(scs_inference,[],[178,190,249,59,233,192,131,2,39,3,40])).
% 78.03/78.09 cnf(266,plain,
% 78.03/78.09 (E(a2,f7(f23(x2661,a1,x2662)))),
% 78.03/78.09 inference(scs_inference,[],[59,2])).
% 78.03/78.09 cnf(295,plain,
% 78.03/78.09 (~P3(f17(f23(x2951,x2952,x2953),x2954))+P3(f23(f16(x2951,x2954),f6(x2952,f5(x2954,a2)),x2953))),
% 78.03/78.09 inference(scs_inference,[],[209,246,116,41,47,38])).
% 78.03/78.09 cnf(299,plain,
% 78.03/78.09 (P6(f23(x2991,a1,a3),f20(f6(f8(f23(x2991,a1,x2992)),f5(x2993,x2994)),x2993))),
% 78.03/78.09 inference(scs_inference,[],[183,55,39])).
% 78.03/78.09 cnf(300,plain,
% 78.03/78.09 (P6(x3001,x3001)),
% 78.03/78.09 inference(rename_variables,[],[55])).
% 78.03/78.09 cnf(301,plain,
% 78.03/78.09 (P6(f20(f6(f8(f23(x3011,a1,x3012)),f5(x3013,x3014)),x3013),f23(x3011,a1,a3))),
% 78.03/78.09 inference(scs_inference,[],[183,55,300,39,40])).
% 78.03/78.09 cnf(306,plain,
% 78.03/78.09 (P4(f6(x3061,f5(x3062,x3063)),f20(f6(x3062,f5(x3064,x3065)),x3064))),
% 78.03/78.09 inference(scs_inference,[],[190,107,46])).
% 78.03/78.09 cnf(348,plain,
% 78.03/78.09 (P6(f20(f6(x3481,f5(x3482,x3483)),x3482),x3481)),
% 78.03/78.09 inference(scs_inference,[],[190,55,39])).
% 78.03/78.09 cnf(349,plain,
% 78.03/78.09 (P6(x3491,x3491)),
% 78.03/78.09 inference(rename_variables,[],[55])).
% 78.03/78.09 cnf(350,plain,
% 78.03/78.09 (P6(x3501,f20(f6(x3501,f5(x3502,x3503)),x3502))),
% 78.03/78.09 inference(scs_inference,[],[190,55,349,39,40])).
% 78.03/78.09 cnf(395,plain,
% 78.03/78.09 (P6(a2,f7(f23(x3951,a1,x3952)))),
% 78.03/78.09 inference(scs_inference,[],[55,59,39])).
% 78.03/78.09 cnf(396,plain,
% 78.03/78.09 (P6(x3961,x3961)),
% 78.03/78.09 inference(rename_variables,[],[55])).
% 78.03/78.09 cnf(397,plain,
% 78.03/78.09 (P6(f7(f23(x3971,a1,x3972)),a2)),
% 78.03/78.09 inference(scs_inference,[],[55,396,59,39,40])).
% 78.03/78.09 cnf(400,plain,
% 78.03/78.09 (P6(a2,f20(f6(f7(f23(x4001,a1,x4002)),f5(x4003,x4004)),x4003))),
% 78.03/78.09 inference(scs_inference,[],[59,350,39])).
% 78.03/78.09 cnf(402,plain,
% 78.03/78.09 (P6(f20(f6(f7(f23(x4021,a1,x4022)),f5(x4023,x4024)),x4023),a2)),
% 78.03/78.09 inference(scs_inference,[],[59,348,350,39,40])).
% 78.03/78.09 cnf(404,plain,
% 78.03/78.09 (P7(f6(x4041,f5(a3,a3)),a3,a3)),
% 78.03/78.09 inference(scs_inference,[],[68,79,83])).
% 78.03/78.09 cnf(405,plain,
% 78.03/78.09 (P7(f6(x4051,f5(a3,a3)),a3,f20(f6(a3,f5(x4052,x4053)),x4052))),
% 78.03/78.09 inference(scs_inference,[],[190,404,44])).
% 78.03/78.09 cnf(406,plain,
% 78.03/78.09 (E(x4061,f20(f6(x4061,f5(x4062,x4063)),x4062))),
% 78.03/78.09 inference(rename_variables,[],[190])).
% 78.03/78.09 cnf(407,plain,
% 78.03/78.09 (P7(f6(x4071,f5(a3,a3)),f20(f6(a3,f5(x4072,x4073)),x4072),a3)),
% 78.03/78.09 inference(scs_inference,[],[190,406,404,44,43])).
% 78.03/78.09 cnf(414,plain,
% 78.03/78.09 (E(f20(f6(f23(x4141,a1,a3),f5(x4142,x4143)),x4142),f8(f23(x4141,a1,x4144)))),
% 78.03/78.09 inference(scs_inference,[],[57,178,3])).
% 78.03/78.09 cnf(417,plain,
% 78.03/78.09 (E(f8(f23(x4171,a1,x4172)),f20(f6(f23(x4171,a1,a3),f5(x4173,x4174)),x4173))),
% 78.03/78.09 inference(scs_inference,[],[57,178,140,3,47,2])).
% 78.03/78.09 cnf(434,plain,
% 78.03/78.09 (P6(x4341,f19(f6(x4342,f5(x4343,x4341)),x4343))),
% 78.03/78.09 inference(scs_inference,[],[58,55,39])).
% 78.03/78.09 cnf(435,plain,
% 78.03/78.09 (P6(x4351,x4351)),
% 78.03/78.09 inference(rename_variables,[],[55])).
% 78.03/78.09 cnf(436,plain,
% 78.03/78.09 (P6(f19(f6(x4361,f5(x4362,x4363)),x4362),x4363)),
% 78.03/78.09 inference(scs_inference,[],[58,55,435,39,40])).
% 78.03/78.09 cnf(439,plain,
% 78.03/78.09 (~P5(f23(x4391,f20(f6(f4(a1,x4392),f5(x4393,x4394)),x4393),x4395),x4396)),
% 78.03/78.09 inference(scs_inference,[],[65,123,91,45])).
% 78.03/78.09 cnf(440,plain,
% 78.03/78.09 (E(f5(a2,x4401),f5(f7(f23(x4402,a1,x4403)),x4401))),
% 78.03/78.09 inference(scs_inference,[],[59,6,2])).
% 78.03/78.09 cnf(441,plain,
% 78.03/78.09 (E(f5(f7(f23(x4411,a1,x4412)),x4413),f5(a2,x4413))),
% 78.03/78.09 inference(scs_inference,[],[440,2])).
% 78.03/78.09 cnf(450,plain,
% 78.03/78.09 (E(f6(f4(x4501,f7(f23(x4502,a1,x4503))),x4504),f6(f4(x4501,a2),x4504))),
% 78.03/78.09 inference(scs_inference,[],[59,8,5])).
% 78.03/78.09 cnf(458,plain,
% 78.03/78.09 (E(f6(x4581,f23(f7(f23(x4582,a1,x4583)),x4584,x4585)),f6(x4581,f23(a2,x4584,x4585)))),
% 78.03/78.09 inference(scs_inference,[],[59,9,10])).
% 78.03/78.09 cnf(461,plain,
% 78.03/78.09 (P6(f23(f16(x4611,x4612),f6(x4613,f5(x4612,a2)),x4614),f17(f23(x4611,x4613,x4614),x4612))),
% 78.03/78.09 inference(scs_inference,[],[63,55,40])).
% 78.03/78.09 cnf(462,plain,
% 78.03/78.09 (P6(x4621,x4621)),
% 78.03/78.09 inference(rename_variables,[],[55])).
% 78.03/78.09 cnf(463,plain,
% 78.03/78.09 (P6(f17(f23(x4631,x4632,x4633),x4634),f23(f16(x4631,x4634),f6(x4632,f5(x4634,a2)),x4633))),
% 78.03/78.09 inference(scs_inference,[],[63,55,462,40,39])).
% 78.03/78.09 cnf(466,plain,
% 78.03/78.09 (E(f19(x4661,f21(f7(f23(x4662,a1,x4663)),x4664)),f19(x4661,f21(a2,x4664)))),
% 78.03/78.09 inference(scs_inference,[],[59,17,18])).
% 78.03/78.09 cnf(470,plain,
% 78.03/78.09 (~P8(f20(f6(f23(x4701,x4702,a3),f5(x4703,x4704)),x4703))),
% 78.03/78.09 inference(scs_inference,[],[68,57,47])).
% 78.03/78.09 cnf(480,plain,
% 78.03/78.09 (P4(f6(f6(x4801,f5(f7(f23(x4802,a1,x4803)),x4804)),f5(x4805,x4806)),a2)),
% 78.03/78.09 inference(scs_inference,[],[59,80,78])).
% 78.03/78.09 cnf(481,plain,
% 78.03/78.09 (P7(f6(x4811,f5(a3,a3)),a3,f19(f6(x4812,f5(x4813,a3)),x4813))),
% 78.03/78.09 inference(scs_inference,[],[168,404,44])).
% 78.03/78.09 cnf(482,plain,
% 78.03/78.09 (E(x4821,f19(f6(x4822,f5(x4823,x4821)),x4823))),
% 78.03/78.09 inference(rename_variables,[],[168])).
% 78.03/78.09 cnf(483,plain,
% 78.03/78.09 (P7(f6(x4831,f5(a3,a3)),f19(f6(x4832,f5(x4833,a3)),x4833),a3)),
% 78.03/78.09 inference(scs_inference,[],[168,482,404,44,43])).
% 78.03/78.09 cnf(487,plain,
% 78.03/78.09 (P4(f6(x4871,f5(a1,x4872)),f4(a1,x4873))),
% 78.03/78.09 inference(scs_inference,[],[116,107,46])).
% 78.03/78.09 cnf(492,plain,
% 78.03/78.09 (P7(f6(a14,f5(x4921,x4922)),f12(a9,a14),f11(a9,a14))),
% 78.03/78.09 inference(scs_inference,[],[67,94,93])).
% 78.03/78.09 cnf(501,plain,
% 78.03/78.09 (~E(f6(x5011,f5(x5012,x5013)),f4(a1,x5014))),
% 78.03/78.09 inference(scs_inference,[],[136,52,3])).
% 78.03/78.09 cnf(503,plain,
% 78.03/78.09 (~E(f6(x5031,f5(x5032,x5033)),f19(f6(x5034,f5(x5035,a1)),x5035))),
% 78.03/78.09 inference(scs_inference,[],[170,501,3])).
% 78.03/78.09 cnf(505,plain,
% 78.03/78.09 (~E(f6(x5051,f5(x5052,x5053)),f20(f6(a1,f5(x5054,x5055)),x5054))),
% 78.03/78.09 inference(scs_inference,[],[136,57,3])).
% 78.03/78.09 cnf(510,plain,
% 78.03/78.09 (P4(f6(x5101,f5(a1,x5102)),f20(f6(f4(a1,x5103),f5(x5104,x5105)),x5104))),
% 78.03/78.09 inference(scs_inference,[],[151,107,46])).
% 78.03/78.09 cnf(513,plain,
% 78.03/78.09 (P1(f7(f23(x5131,a1,x5132)),x5133)),
% 78.03/78.09 inference(scs_inference,[],[266,53,36])).
% 78.03/78.09 cnf(514,plain,
% 78.03/78.09 (~P9(x5141,f7(f23(x5142,a1,x5143)))),
% 78.03/78.09 inference(scs_inference,[],[266,53,36,72])).
% 78.03/78.09 cnf(519,plain,
% 78.03/78.09 (P1(f4(a1,x5191),f4(a1,x5192))),
% 78.03/78.09 inference(scs_inference,[],[162,54,36])).
% 78.03/78.09 cnf(521,plain,
% 78.03/78.09 (~P9(f4(a1,x5211),f4(a1,x5212))),
% 78.03/78.09 inference(scs_inference,[],[162,54,36,72])).
% 78.03/78.09 cnf(524,plain,
% 78.03/78.09 (P4(f6(x5241,f5(x5242,x5243)),f19(f6(x5244,f5(x5245,x5242)),x5245))),
% 78.03/78.09 inference(scs_inference,[],[168,107,46])).
% 78.03/78.09 cnf(526,plain,
% 78.03/78.09 (P1(f19(f6(x5261,f5(x5262,x5263)),x5262),x5263)),
% 78.03/78.09 inference(scs_inference,[],[168,54,107,46,36])).
% 78.03/78.09 cnf(528,plain,
% 78.03/78.09 (P6(f7(f23(x5281,a1,x5282)),f19(f6(x5283,f5(x5284,a2)),x5284))),
% 78.03/78.09 inference(scs_inference,[],[168,54,107,397,46,36,40])).
% 78.03/78.09 cnf(529,plain,
% 78.03/78.09 (E(x5291,f19(f6(x5292,f5(x5293,x5291)),x5293))),
% 78.03/78.09 inference(rename_variables,[],[168])).
% 78.03/78.09 cnf(530,plain,
% 78.03/78.09 (P6(f19(f6(x5301,f5(x5302,a2)),x5302),f7(f23(x5303,a1,x5304)))),
% 78.03/78.09 inference(scs_inference,[],[168,529,54,107,397,395,46,36,40,39])).
% 78.03/78.09 cnf(535,plain,
% 78.03/78.09 (~P9(x5351,f19(f6(x5352,f5(x5353,x5351)),x5353))),
% 78.03/78.09 inference(scs_inference,[],[526,72])).
% 78.03/78.09 cnf(537,plain,
% 78.03/78.09 (P1(f19(f6(x5371,f5(x5372,a2)),x5372),x5373)),
% 78.03/78.09 inference(scs_inference,[],[168,53,526,72,36])).
% 78.03/78.09 cnf(540,plain,
% 78.03/78.09 (~P9(x5401,f19(f6(x5402,f5(x5403,a2)),x5403))),
% 78.03/78.09 inference(scs_inference,[],[537,72])).
% 78.03/78.09 cnf(543,plain,
% 78.03/78.09 (P1(f4(a1,x5431),a1)),
% 78.03/78.09 inference(scs_inference,[],[170,526,36])).
% 78.03/78.09 cnf(547,plain,
% 78.03/78.09 (P1(a1,f4(a1,x5471))+P9(f4(a1,x5471),a1)),
% 78.03/78.09 inference(scs_inference,[],[170,526,36,72,73])).
% 78.03/78.09 cnf(549,plain,
% 78.03/78.09 (P1(f4(a1,x5491),f20(f6(f4(a1,x5492),f5(x5493,x5494)),x5493))),
% 78.03/78.09 inference(scs_inference,[],[170,151,526,36,72,73,37])).
% 78.03/78.09 cnf(550,plain,
% 78.03/78.09 (P1(a1,f4(a1,x5501))),
% 78.03/78.09 inference(scs_inference,[],[117,52,547,50])).
% 78.03/78.09 cnf(553,plain,
% 78.03/78.09 (P1(f20(f6(f4(a1,x5531),f5(x5532,x5533)),x5532),f4(a1,x5534))),
% 78.03/78.09 inference(scs_inference,[],[151,549,550,72,36])).
% 78.03/78.09 cnf(557,plain,
% 78.03/78.09 (~P9(f4(a1,x5571),a1)),
% 78.03/78.09 inference(scs_inference,[],[550,72])).
% 78.03/78.09 cnf(559,plain,
% 78.03/78.09 (P1(f4(a1,x5591),f19(f6(x5592,f5(x5593,a1)),x5593))),
% 78.03/78.09 inference(scs_inference,[],[170,54,36])).
% 78.03/78.09 cnf(565,plain,
% 78.03/78.09 (P1(f19(f6(x5651,f5(x5652,a1)),x5652),f4(a1,x5653))+P9(f4(a1,x5654),f19(f6(x5651,f5(x5652,a1)),x5652))),
% 78.03/78.09 inference(scs_inference,[],[162,559,72,73,37])).
% 78.03/78.09 cnf(567,plain,
% 78.03/78.09 (P4(f6(x5671,f5(f23(x5672,a1,a3),x5673)),f8(f23(x5672,a1,x5674)))),
% 78.03/78.10 inference(scs_inference,[],[178,107,46])).
% 78.03/78.10 cnf(569,plain,
% 78.03/78.10 (P1(f8(f23(x5691,a1,x5692)),f23(x5691,a1,a3))),
% 78.03/78.10 inference(scs_inference,[],[178,54,107,46,36])).
% 78.03/78.10 cnf(571,plain,
% 78.03/78.10 (~P9(f23(x5711,a1,a3),f8(f23(x5711,a1,x5712)))),
% 78.03/78.10 inference(scs_inference,[],[178,54,107,46,36,72])).
% 78.03/78.10 cnf(573,plain,
% 78.03/78.10 (P1(f23(x5731,a1,a3),f8(f23(x5731,a1,x5732)))+P9(f8(f23(x5731,a1,x5732)),f23(x5731,a1,a3))),
% 78.03/78.10 inference(scs_inference,[],[178,54,107,46,36,72,73])).
% 78.03/78.10 cnf(575,plain,
% 78.03/78.10 (P1(f23(x5751,a1,a3),f8(f23(x5751,a1,x5752)))),
% 78.03/78.10 inference(scs_inference,[],[117,61,573,50])).
% 78.03/78.10 cnf(576,plain,
% 78.03/78.10 (~P9(f8(f23(x5761,a1,x5762)),f23(x5761,a1,a3))),
% 78.03/78.10 inference(scs_inference,[],[575,72])).
% 78.03/78.10 cnf(582,plain,
% 78.03/78.10 (P1(f19(f6(x5821,f5(x5822,a1)),x5822),f4(a1,x5823))),
% 78.03/78.10 inference(scs_inference,[],[535,52,565,50])).
% 78.03/78.10 cnf(589,plain,
% 78.03/78.10 (P1(f23(x5891,a1,a3),f20(f6(f8(f23(x5891,a1,x5892)),f5(x5893,x5894)),x5893))),
% 78.03/78.10 inference(scs_inference,[],[183,54,36])).
% 78.03/78.10 cnf(608,plain,
% 78.03/78.10 (P5(f17(f23(x6081,x6082,x6083),x6084),x6084)),
% 78.03/78.10 inference(scs_inference,[],[63,107,48,84])).
% 78.03/78.10 cnf(615,plain,
% 78.03/78.10 (~P3(f23(x6151,a14,x6152))),
% 78.03/78.10 inference(scs_inference,[],[110,121,99,72])).
% 78.03/78.10 cnf(616,plain,
% 78.03/78.10 (~P1(f11(x6161,a14),f12(x6161,a14))),
% 78.03/78.10 inference(scs_inference,[],[615,92])).
% 78.03/78.10 cnf(618,plain,
% 78.03/78.10 (P7(a14,f12(x6181,a14),f11(x6181,a14))),
% 78.03/78.10 inference(scs_inference,[],[615,92,93])).
% 78.03/78.10 cnf(620,plain,
% 78.03/78.10 (P1(f12(x6201,a14),f11(x6201,a14))),
% 78.03/78.10 inference(scs_inference,[],[615,92,93,69])).
% 78.03/78.10 cnf(622,plain,
% 78.03/78.10 (~P9(f11(x6221,a14),f12(x6221,a14))),
% 78.03/78.10 inference(scs_inference,[],[615,92,93,69,70])).
% 78.03/78.10 cnf(624,plain,
% 78.03/78.10 (P9(f10(a14,x6241),f13(a14,x6241))),
% 78.03/78.10 inference(scs_inference,[],[618,620,616,86,73])).
% 78.03/78.10 cnf(625,plain,
% 78.03/78.10 (~E(f10(a14,x6251),f13(a14,x6251))),
% 78.03/78.10 inference(scs_inference,[],[624,117,50])).
% 78.03/78.10 cnf(629,plain,
% 78.03/78.10 (~E(f13(a14,x6291),f7(f23(x6292,a1,x6293)))),
% 78.03/78.10 inference(scs_inference,[],[194,624,514,117,608,50,49,51])).
% 78.03/78.10 cnf(631,plain,
% 78.03/78.10 (P9(f12(x6311,a14),f11(x6311,a14))),
% 78.03/78.10 inference(scs_inference,[],[194,616,624,620,514,117,608,50,49,51,73])).
% 78.03/78.10 cnf(634,plain,
% 78.03/78.10 (~E(f11(x6341,a14),f12(x6341,a14))),
% 78.03/78.10 inference(scs_inference,[],[194,616,54,624,620,514,117,608,50,49,51,73,37])).
% 78.03/78.10 cnf(637,plain,
% 78.03/78.10 (~E(f12(x6371,a14),f11(x6371,a14))),
% 78.03/78.10 inference(scs_inference,[],[631,117,50])).
% 78.03/78.10 cnf(639,plain,
% 78.03/78.10 (E(f4(x6391,a3),f4(x6391,f20(f6(a3,f5(x6392,x6393)),x6392)))),
% 78.03/78.10 inference(scs_inference,[],[66,407,98,5])).
% 78.03/78.10 cnf(641,plain,
% 78.03/78.10 (P7(f4(a14,x6411),f10(a14,x6411),f13(a14,x6411))),
% 78.03/78.10 inference(scs_inference,[],[618,201,57,96,50])).
% 78.03/78.10 cnf(642,plain,
% 78.03/78.10 (~E(f4(a14,x6421),a1)),
% 78.03/78.10 inference(scs_inference,[],[641,66,42])).
% 78.03/78.10 cnf(644,plain,
% 78.03/78.10 (~P3(f23(x6441,f6(a14,f5(f11(x6442,a14),f12(x6442,a14))),x6443))),
% 78.03/78.10 inference(scs_inference,[],[615,616,106,69])).
% 78.03/78.10 cnf(645,plain,
% 78.03/78.10 (~E(f4(a14,x6451),f20(f6(f4(a1,x6452),f5(x6453,x6454)),x6453))),
% 78.03/78.10 inference(scs_inference,[],[123,642,3])).
% 78.03/78.10 cnf(647,plain,
% 78.03/78.10 (~E(f4(a14,x6471),f4(a1,x6472))),
% 78.03/78.10 inference(scs_inference,[],[52,642,3])).
% 78.03/78.10 cnf(649,plain,
% 78.03/78.10 (~E(f4(a14,x6491),f19(f6(x6492,f5(x6493,a1)),x6493))),
% 78.03/78.10 inference(scs_inference,[],[170,647,3])).
% 78.03/78.10 cnf(652,plain,
% 78.03/78.10 (P5(f17(f23(x6521,x6522,x6523),f23(x6524,a1,a3)),f20(f6(f8(f23(x6524,a1,x6525)),f5(x6526,x6527)),x6526))),
% 78.03/78.10 inference(scs_inference,[],[209,608,49])).
% 78.03/78.10 cnf(659,plain,
% 78.03/78.10 (~E(a1,a14)),
% 78.03/78.10 inference(scs_inference,[],[647,2,4])).
% 78.03/78.10 cnf(660,plain,
% 78.03/78.10 (E(f4(x6601,a2),f4(x6601,f7(f23(x6602,a1,x6603))))),
% 78.03/78.10 inference(scs_inference,[],[59,2,5])).
% 78.03/78.10 cnf(661,plain,
% 78.03/78.10 (E(f4(x6611,f7(f23(x6612,a1,x6613))),f4(x6611,a2))),
% 78.03/78.10 inference(scs_inference,[],[660,2])).
% 78.03/78.10 cnf(668,plain,
% 78.03/78.10 (P5(f17(f23(x6681,x6682,x6683),f4(a1,x6684)),f19(f6(x6685,f5(x6686,a1)),x6686))),
% 78.03/78.10 inference(scs_inference,[],[232,608,49])).
% 78.03/78.10 cnf(670,plain,
% 78.03/78.10 (P1(a1,f19(f6(x6701,f5(x6702,a1)),x6702))),
% 78.03/78.10 inference(scs_inference,[],[232,550,608,49,37])).
% 78.03/78.10 cnf(675,plain,
% 78.03/78.10 (P5(f17(f23(x6751,x6752,x6753),f4(a1,x6754)),f4(a1,x6755))),
% 78.03/78.10 inference(scs_inference,[],[170,668,49])).
% 78.03/78.10 cnf(677,plain,
% 78.03/78.10 (E(f4(f19(f6(x6771,f5(x6772,a1)),x6772),x6773),f4(f4(a1,x6774),x6773))),
% 78.03/78.10 inference(scs_inference,[],[232,2,4])).
% 78.03/78.10 cnf(678,plain,
% 78.03/78.10 (E(f5(x6781,a2),f5(x6781,f7(f23(x6782,a1,x6783))))),
% 78.03/78.10 inference(scs_inference,[],[59,2,7])).
% 78.03/78.10 cnf(679,plain,
% 78.03/78.10 (E(f5(x6791,f7(f23(x6792,a1,x6793))),f5(x6791,a2))),
% 78.03/78.10 inference(scs_inference,[],[678,2])).
% 78.03/78.10 cnf(687,plain,
% 78.03/78.10 (E(f5(f7(f23(x6871,a1,x6872)),f7(f23(x6873,a1,x6874))),f5(a2,a2))),
% 78.03/78.10 inference(scs_inference,[],[441,679,3])).
% 78.03/78.10 cnf(694,plain,
% 78.03/78.10 (E(f5(a2,a2),f5(f7(f23(x6941,a1,x6942)),f7(f23(x6943,a1,x6944))))),
% 78.03/78.10 inference(scs_inference,[],[687,2])).
% 78.03/78.10 cnf(719,plain,
% 78.03/78.10 (P1(f23(f16(x7191,x7192),f6(x7193,f5(x7192,a2)),x7194),f17(f23(x7191,x7193,x7194),x7192))),
% 78.03/78.10 inference(scs_inference,[],[246,54,36])).
% 78.03/78.10 cnf(723,plain,
% 78.03/78.10 (P1(f17(f23(x7231,x7232,x7233),x7234),f23(f16(x7231,x7234),f6(x7232,f5(x7234,a2)),x7233))+P9(f23(f16(x7231,x7234),f6(x7232,f5(x7234,a2)),x7233),f17(f23(x7231,x7232,x7233),x7234))),
% 78.03/78.10 inference(scs_inference,[],[246,54,36,72,73])).
% 78.03/78.10 cnf(734,plain,
% 78.03/78.10 (P5(f17(f23(x7341,x7342,x7343),f23(x7344,a1,a3)),f8(f23(x7344,a1,x7345)))),
% 78.03/78.10 inference(scs_inference,[],[257,652,49])).
% 78.03/78.10 cnf(743,plain,
% 78.03/78.10 (P4(f6(x7431,f5(a2,x7432)),f7(f23(x7433,a1,x7434)))),
% 78.03/78.10 inference(scs_inference,[],[266,107,46])).
% 78.03/78.10 cnf(763,plain,
% 78.03/78.10 (P1(f17(f23(x7631,x7632,x7633),x7634),f23(f16(x7631,x7634),f6(x7632,f5(x7634,a2)),x7633))),
% 78.03/78.10 inference(scs_inference,[],[117,63,723,50])).
% 78.03/78.10 cnf(766,plain,
% 78.03/78.10 (E(f4(a2,x7661),f4(f7(f23(x7662,a1,x7663)),x7661))),
% 78.03/78.10 inference(scs_inference,[],[59,2,4])).
% 78.03/78.10 cnf(767,plain,
% 78.03/78.10 (E(f4(f7(f23(x7671,a1,x7672)),x7673),f4(a2,x7673))),
% 78.03/78.10 inference(scs_inference,[],[766,2])).
% 78.03/78.10 cnf(768,plain,
% 78.03/78.10 (E(f4(a2,a2),f4(f7(f23(x7681,a1,x7682)),f7(f23(x7683,a1,x7684))))),
% 78.03/78.10 inference(scs_inference,[],[660,766,2,3])).
% 78.03/78.10 cnf(774,plain,
% 78.03/78.10 (E(f4(f7(f23(x7741,a1,x7742)),f7(f23(x7743,a1,x7744))),f4(a2,a2))),
% 78.03/78.10 inference(scs_inference,[],[768,2])).
% 78.03/78.10 cnf(789,plain,
% 78.03/78.10 (P1(f8(f23(x7891,a1,x7892)),f20(f6(f23(x7891,a1,a3),f5(x7893,x7894)),x7893))),
% 78.03/78.10 inference(scs_inference,[],[414,54,36])).
% 78.03/78.10 cnf(800,plain,
% 78.03/78.10 (P5(f17(f23(x8001,x8002,x8003),f23(x8004,a1,a3)),f20(f6(f23(x8004,a1,a3),f5(x8005,x8006)),x8005))),
% 78.03/78.10 inference(scs_inference,[],[417,734,49])).
% 78.03/78.10 cnf(802,plain,
% 78.03/78.10 (P1(f23(x8021,a1,a3),f20(f6(f23(x8021,a1,a3),f5(x8022,x8023)),x8022))),
% 78.03/78.10 inference(scs_inference,[],[417,575,734,49,37])).
% 78.03/78.10 cnf(824,plain,
% 78.03/78.10 (P5(f17(f23(x8241,x8242,x8243),f5(a2,x8244)),f5(f7(f23(x8245,a1,x8246)),x8244))),
% 78.03/78.10 inference(scs_inference,[],[440,608,49])).
% 78.03/78.10 cnf(826,plain,
% 78.03/78.10 (P1(f5(f7(f23(x8261,a1,x8262)),x8263),f5(a2,x8263))),
% 78.03/78.10 inference(scs_inference,[],[440,54,608,49,36])).
% 78.03/78.10 cnf(828,plain,
% 78.03/78.10 (P6(f5(a2,x8281),f5(f7(f23(x8282,a1,x8283)),x8281))),
% 78.03/78.10 inference(scs_inference,[],[440,54,55,608,49,36,40])).
% 78.03/78.10 cnf(829,plain,
% 78.03/78.10 (P6(x8291,x8291)),
% 78.03/78.10 inference(rename_variables,[],[55])).
% 78.03/78.10 cnf(830,plain,
% 78.03/78.10 (P6(f5(f7(f23(x8301,a1,x8302)),x8303),f5(a2,x8303))),
% 78.03/78.10 inference(scs_inference,[],[440,54,55,829,608,49,36,40,39])).
% 78.03/78.10 cnf(841,plain,
% 78.03/78.10 (P1(f5(a2,x8411),f5(f7(f23(x8412,a1,x8413)),x8411))),
% 78.03/78.10 inference(scs_inference,[],[441,54,36])).
% 78.03/78.10 cnf(859,plain,
% 78.03/78.10 (~E(f11(x8591,a14),f7(f23(x8592,a1,x8593)))),
% 78.03/78.10 inference(scs_inference,[],[514,631,51])).
% 78.03/78.10 cnf(862,plain,
% 78.03/78.10 (~E(f13(a14,x8621),a2)),
% 78.03/78.10 inference(scs_inference,[],[266,629,3])).
% 78.03/78.10 cnf(864,plain,
% 78.03/78.10 (~E(f11(x8641,a14),a2)),
% 78.03/78.10 inference(scs_inference,[],[266,859,3])).
% 78.03/78.10 cnf(866,plain,
% 78.03/78.10 (E(f6(a2,x8661),f6(f7(f23(x8662,a1,x8663)),x8661))),
% 78.03/78.10 inference(scs_inference,[],[59,2,8])).
% 78.03/78.10 cnf(867,plain,
% 78.03/78.10 (E(f6(f7(f23(x8671,a1,x8672)),x8673),f6(a2,x8673))),
% 78.03/78.10 inference(scs_inference,[],[866,2])).
% 78.03/78.10 cnf(874,plain,
% 78.03/78.10 (E(f6(x8741,a2),f6(x8741,f7(f23(x8742,a1,x8743))))),
% 78.03/78.10 inference(scs_inference,[],[59,2,9])).
% 78.03/78.10 cnf(875,plain,
% 78.03/78.10 (E(f6(x8751,f7(f23(x8752,a1,x8753))),f6(x8751,a2))),
% 78.03/78.10 inference(scs_inference,[],[874,2])).
% 78.03/78.10 cnf(885,plain,
% 78.03/78.10 (~E(f13(a14,x8851),f19(f6(x8852,f5(x8853,a2)),x8853))),
% 78.03/78.10 inference(scs_inference,[],[540,624,51])).
% 78.03/78.10 cnf(888,plain,
% 78.03/78.10 (~E(f11(x8881,a14),f19(f6(x8882,f5(x8883,a2)),x8883))),
% 78.03/78.10 inference(scs_inference,[],[540,631,51])).
% 78.03/78.10 cnf(895,plain,
% 78.03/78.10 (P1(a1,f20(f6(f4(a1,x8951),f5(x8952,x8953)),x8952))),
% 78.03/78.10 inference(scs_inference,[],[550,549,74])).
% 78.03/78.10 cnf(911,plain,
% 78.03/78.10 (~P9(a1,f20(f6(f4(a1,x9111),f5(x9112,x9113)),x9112))),
% 78.03/78.10 inference(scs_inference,[],[553,543,74,72])).
% 78.03/78.10 cnf(914,plain,
% 78.03/78.10 (E(f23(a2,x9141,x9142),f23(f7(f23(x9143,a1,x9144)),x9141,x9142))),
% 78.03/78.10 inference(scs_inference,[],[59,2,10])).
% 78.03/78.10 cnf(915,plain,
% 78.03/78.10 (E(f23(f7(f23(x9151,a1,x9152)),x9153,x9154),f23(a2,x9153,x9154))),
% 78.03/78.10 inference(scs_inference,[],[914,2])).
% 78.03/78.10 cnf(928,plain,
% 78.03/78.10 (E(f6(f7(f23(x9281,a1,x9282)),f7(f23(x9283,a1,x9284))),f6(a2,a2))),
% 78.03/78.10 inference(scs_inference,[],[875,867,3])).
% 78.03/78.10 cnf(931,plain,
% 78.03/78.10 (E(f6(a2,a2),f6(f7(f23(x9311,a1,x9312)),f7(f23(x9313,a1,x9314))))),
% 78.03/78.10 inference(scs_inference,[],[928,2])).
% 78.03/78.10 cnf(957,plain,
% 78.03/78.10 (~E(f10(a14,x9571),f20(f6(f13(a14,x9571),f5(x9572,x9573)),x9572))),
% 78.03/78.10 inference(scs_inference,[],[625,57,3])).
% 78.03/78.10 cnf(959,plain,
% 78.03/78.10 (E(f23(x9591,a2,x9592),f23(x9591,f7(f23(x9593,a1,x9594)),x9592))),
% 78.03/78.10 inference(scs_inference,[],[59,2,11])).
% 78.03/78.10 cnf(960,plain,
% 78.03/78.10 (E(f23(x9601,f7(f23(x9602,a1,x9603)),x9604),f23(x9601,a2,x9604))),
% 78.03/78.10 inference(scs_inference,[],[959,2])).
% 78.03/78.10 cnf(988,plain,
% 78.03/78.10 (~E(f11(x9881,a14),f20(f6(f12(x9881,a14),f5(x9882,x9883)),x9882))),
% 78.03/78.10 inference(scs_inference,[],[634,57,3])).
% 78.03/78.10 cnf(990,plain,
% 78.03/78.10 (~E(f12(x9901,a14),f20(f6(f11(x9901,a14),f5(x9902,x9903)),x9902))),
% 78.03/78.10 inference(scs_inference,[],[637,57,3])).
% 78.03/78.10 cnf(994,plain,
% 78.03/78.10 (~E(f4(a14,x9941),f20(f6(a1,f5(x9942,x9943)),x9942))),
% 78.03/78.10 inference(scs_inference,[],[642,57,3])).
% 78.03/78.10 cnf(1003,plain,
% 78.03/78.10 (~E(a1,f19(f6(x10031,f5(x10032,a14)),x10032))),
% 78.03/78.10 inference(scs_inference,[],[659,58,3])).
% 78.03/78.10 cnf(1007,plain,
% 78.03/78.10 (P5(f17(f23(x10071,x10072,x10073),f4(x10074,a2)),f4(x10074,f7(f23(x10075,a1,x10076))))),
% 78.03/78.10 inference(scs_inference,[],[660,608,49])).
% 78.03/78.10 cnf(1010,plain,
% 78.03/78.10 (P6(x10101,x10101)),
% 78.03/78.10 inference(rename_variables,[],[55])).
% 78.03/78.10 cnf(1011,plain,
% 78.03/78.10 (P1(f4(x10111,f7(f23(x10112,a1,x10113))),f4(x10111,a2))),
% 78.03/78.10 inference(scs_inference,[],[660,54,55,608,49,40,36])).
% 78.03/78.10 cnf(1013,plain,
% 78.03/78.10 (P6(f4(x10131,f7(f23(x10132,a1,x10133))),f4(x10131,a2))),
% 78.03/78.10 inference(scs_inference,[],[660,54,55,1010,608,49,40,36,39])).
% 78.03/78.10 cnf(1019,plain,
% 78.03/78.10 (P1(f4(x10191,a2),f4(x10191,f7(f23(x10192,a1,x10193))))),
% 78.03/78.10 inference(scs_inference,[],[661,54,36])).
% 78.03/78.10 cnf(1022,plain,
% 78.03/78.10 (~P9(f4(x10221,f7(f23(x10222,a1,x10223))),f4(x10221,a2))),
% 78.03/78.10 inference(scs_inference,[],[1019,72])).
% 78.03/78.10 cnf(1030,plain,
% 78.03/78.10 (P1(f5(a2,a2),f5(f7(f23(x10301,a1,x10302)),f7(f23(x10303,a1,x10304))))),
% 78.03/78.10 inference(scs_inference,[],[678,841,608,49,37])).
% 78.03/78.10 cnf(1032,plain,
% 78.03/78.10 (E(f5(x10321,a2),f5(x10321,f7(f23(x10322,a1,x10323))))),
% 78.03/78.10 inference(rename_variables,[],[678])).
% 78.03/78.10 cnf(1033,plain,
% 78.03/78.10 (P6(f5(a2,a2),f5(f7(f23(x10331,a1,x10332)),f7(f23(x10333,a1,x10334))))),
% 78.03/78.10 inference(scs_inference,[],[678,1032,841,828,608,49,37,40])).
% 78.03/78.10 cnf(1045,plain,
% 78.03/78.10 (E(f5(x10451,a2),f5(x10451,f7(f23(x10452,a1,x10453))))),
% 78.03/78.10 inference(rename_variables,[],[678])).
% 78.03/78.10 cnf(1048,plain,
% 78.03/78.10 (E(f5(f7(f23(x10481,a1,x10482)),x10483),f5(a2,x10483))),
% 78.03/78.10 inference(rename_variables,[],[441])).
% 78.03/78.10 cnf(1052,plain,
% 78.03/78.10 (P1(f5(f7(f23(x10521,a1,x10522)),f7(f23(x10523,a1,x10524))),f5(a2,a2))),
% 78.03/78.10 inference(scs_inference,[],[678,1045,441,1048,826,1030,1033,824,72,49,37,40,36])).
% 78.03/78.10 cnf(1064,plain,
% 78.03/78.10 (P6(x10641,x10641)),
% 78.03/78.10 inference(rename_variables,[],[55])).
% 78.03/78.10 cnf(1065,plain,
% 78.03/78.10 (P6(f5(x10651,f7(f23(x10652,a1,x10653))),f5(x10651,a2))),
% 78.03/78.10 inference(scs_inference,[],[678,1052,55,1064,72,40,39])).
% 78.03/78.10 cnf(1074,plain,
% 78.03/78.10 (P1(f5(x10741,a2),f5(x10741,f7(f23(x10742,a1,x10743))))),
% 78.03/78.10 inference(scs_inference,[],[679,54,36])).
% 78.03/78.10 cnf(1077,plain,
% 78.03/78.10 (~P9(f5(x10771,f7(f23(x10772,a1,x10773))),f5(x10771,a2))),
% 78.03/78.10 inference(scs_inference,[],[1074,72])).
% 78.03/78.10 cnf(1080,plain,
% 78.03/78.10 (E(f23(x10801,x10802,a2),f23(x10801,x10802,f7(f23(x10803,a1,x10804))))),
% 78.03/78.10 inference(scs_inference,[],[59,2,12])).
% 78.03/78.10 cnf(1081,plain,
% 78.03/78.10 (E(f23(x10811,x10812,f7(f23(x10813,a1,x10814))),f23(x10811,x10812,a2))),
% 78.03/78.10 inference(scs_inference,[],[1080,2])).
% 78.03/78.10 cnf(1082,plain,
% 78.03/78.10 (E(f17(f23(x10821,x10822,a2),x10823),f23(f16(x10821,x10823),f6(x10822,f5(x10823,a2)),f7(f23(x10824,a1,x10825))))),
% 78.03/78.10 inference(scs_inference,[],[246,1080,2,3])).
% 78.03/78.10 cnf(1090,plain,
% 78.03/78.10 (E(f23(f16(x10901,x10902),f6(x10903,f5(x10902,a2)),f7(f23(x10904,a1,x10905))),f17(f23(x10901,x10903,a2),x10902))),
% 78.03/78.10 inference(scs_inference,[],[1082,2])).
% 78.03/78.10 cnf(1098,plain,
% 78.03/78.10 (E(f23(a2,a2,x10981),f23(f7(f23(x10982,a1,x10983)),f7(f23(x10984,a1,x10985)),x10981))),
% 78.03/78.10 inference(scs_inference,[],[914,959,3])).
% 78.03/78.10 cnf(1104,plain,
% 78.03/78.10 (~P3(f17(f23(x11041,x11042,a2),x11043))+P3(f23(f16(x11041,x11043),f6(x11042,f5(x11043,a2)),f7(f23(x11044,a1,x11045))))),
% 78.03/78.10 inference(scs_inference,[],[914,959,1080,1082,1090,3,2,41,47,38])).
% 78.03/78.10 cnf(1131,plain,
% 78.03/78.10 (~P3(f23(f16(x11311,x11312),f6(x11313,f5(x11312,a2)),f7(f23(x11314,a1,x11315))))+P3(f17(f23(x11311,x11313,a2),x11312))),
% 78.03/78.10 inference(scs_inference,[],[1090,38])).
% 78.03/78.10 cnf(1149,plain,
% 78.03/78.10 (P1(f4(a2,a2),f4(f7(f23(x11491,a1,x11492)),f7(f23(x11493,a1,x11494))))),
% 78.03/78.10 inference(scs_inference,[],[766,1019,608,49,37])).
% 78.03/78.10 cnf(1164,plain,
% 78.03/78.10 (E(f4(a2,x11641),f4(f7(f23(x11642,a1,x11643)),x11641))),
% 78.03/78.10 inference(rename_variables,[],[766])).
% 78.03/78.10 cnf(1166,plain,
% 78.03/78.10 (P6(x11661,x11661)),
% 78.03/78.10 inference(rename_variables,[],[55])).
% 78.03/78.10 cnf(1169,plain,
% 78.03/78.10 (E(f4(a2,x11691),f4(f7(f23(x11692,a1,x11693)),x11691))),
% 78.03/78.10 inference(rename_variables,[],[766])).
% 78.03/78.10 cnf(1170,plain,
% 78.03/78.10 (P6(f4(f7(f23(x11701,a1,x11702)),x11703),f4(a2,x11703))),
% 78.03/78.10 inference(scs_inference,[],[766,1164,1169,1011,1149,55,1166,1007,72,49,40,36,39])).
% 78.03/78.10 cnf(1182,plain,
% 78.03/78.10 (P1(f4(a2,x11821),f4(f7(f23(x11822,a1,x11823)),x11821))),
% 78.03/78.10 inference(scs_inference,[],[767,54,36])).
% 78.03/78.10 cnf(1184,plain,
% 78.03/78.10 (~P9(f4(f7(f23(x11841,a1,x11842)),x11843),f4(a2,x11843))),
% 78.03/78.10 inference(scs_inference,[],[1182,72])).
% 78.03/78.10 cnf(1195,plain,
% 78.03/78.10 (~P3(f17(f23(x11951,a14,a2),x11952))),
% 78.03/78.10 inference(scs_inference,[],[616,492,1104,99])).
% 78.03/78.10 cnf(1196,plain,
% 78.03/78.10 (~P3(f23(f16(x11961,x11962),f6(a14,f5(x11962,a2)),f7(f23(x11963,a1,x11964))))),
% 78.03/78.10 inference(scs_inference,[],[1195,1131])).
% 78.03/78.10 cnf(1197,plain,
% 78.03/78.10 (~P3(f23(f16(x11971,x11972),f6(a14,f5(x11972,a2)),a2))),
% 78.03/78.10 inference(scs_inference,[],[1195,63,1131,38])).
% 78.03/78.10 cnf(1206,plain,
% 78.03/78.10 (~E(f13(a14,x12061),f20(f6(a2,f5(x12062,x12063)),x12062))),
% 78.03/78.10 inference(scs_inference,[],[862,57,3])).
% 78.03/78.10 cnf(1215,plain,
% 78.03/78.10 (P6(x12151,x12151)),
% 78.03/78.10 inference(rename_variables,[],[55])).
% 78.03/78.10 cnf(1218,plain,
% 78.03/78.10 (P6(f6(f7(f23(x12181,a1,x12182)),x12183),f6(a2,x12183))),
% 78.03/78.10 inference(scs_inference,[],[866,54,55,1215,608,49,40,36,39])).
% 78.03/78.10 cnf(1222,plain,
% 78.03/78.10 (P1(f6(a2,x12221),f6(f7(f23(x12222,a1,x12223)),x12221))+P9(f6(f7(f23(x12222,a1,x12223)),x12221),f6(a2,x12221))),
% 78.03/78.10 inference(scs_inference,[],[866,54,55,1215,608,49,40,36,39,72,73])).
% 78.03/78.10 cnf(1227,plain,
% 78.03/78.10 (P1(f6(a2,x12271),f6(f7(f23(x12272,a1,x12273)),x12271))),
% 78.03/78.10 inference(scs_inference,[],[117,867,1222,50])).
% 78.03/78.10 cnf(1228,plain,
% 78.03/78.10 (~P9(f6(f7(f23(x12281,a1,x12282)),x12283),f6(a2,x12283))),
% 78.03/78.10 inference(scs_inference,[],[1227,72])).
% 78.03/78.10 cnf(1273,plain,
% 78.03/78.10 (P6(x12731,x12731)),
% 78.03/78.10 inference(rename_variables,[],[55])).
% 78.03/78.10 cnf(1274,plain,
% 78.03/78.10 (P1(f6(x12741,f7(f23(x12742,a1,x12743))),f6(x12741,a2))),
% 78.03/78.10 inference(scs_inference,[],[874,54,55,608,49,40,36])).
% 78.03/78.10 cnf(1276,plain,
% 78.03/78.10 (P6(f6(x12761,f7(f23(x12762,a1,x12763))),f6(x12761,a2))),
% 78.03/78.10 inference(scs_inference,[],[874,54,55,1273,608,49,40,36,39])).
% 78.03/78.10 cnf(1295,plain,
% 78.03/78.10 (P5(f17(f23(x12951,x12952,x12953),f23(a2,x12954,x12955)),f23(f7(f23(x12956,a1,x12957)),x12954,x12955))),
% 78.03/78.10 inference(scs_inference,[],[914,608,49])).
% 78.03/78.10 cnf(1299,plain,
% 78.03/78.10 (E(f23(a2,x12991,x12992),f23(f7(f23(x12993,a1,x12994)),x12991,x12992))),
% 78.03/78.10 inference(rename_variables,[],[914])).
% 78.03/78.10 cnf(1302,plain,
% 78.03/78.10 (E(f23(a2,x13021,x13022),f23(f7(f23(x13023,a1,x13024)),x13021,x13022))),
% 78.03/78.10 inference(rename_variables,[],[914])).
% 78.03/78.10 cnf(1305,plain,
% 78.03/78.10 (E(f23(a2,x13051,x13052),f23(f7(f23(x13053,a1,x13054)),x13051,x13052))),
% 78.03/78.10 inference(rename_variables,[],[914])).
% 78.03/78.10 cnf(1306,plain,
% 78.03/78.10 (P1(f23(f7(f23(x13061,a1,x13062)),x13063,x13064),f23(a2,x13063,x13064))),
% 78.03/78.10 inference(scs_inference,[],[914,1299,1302,1305,54,569,196,192,608,49,37,40,39,36])).
% 78.03/78.10 cnf(1308,plain,
% 78.03/78.10 (E(f23(a2,x13081,a2),f23(f7(f23(x13082,a1,x13083)),x13081,f7(f23(x13084,a1,x13085))))),
% 78.03/78.10 inference(scs_inference,[],[914,1299,1302,1305,1080,54,569,196,192,608,49,37,40,39,36,3])).
% 78.03/78.10 cnf(1319,plain,
% 78.03/78.10 (~P9(f23(a2,x13191,x13192),f23(f7(f23(x13193,a1,x13194)),x13191,x13192))),
% 78.03/78.10 inference(scs_inference,[],[1306,72])).
% 78.03/78.10 cnf(1321,plain,
% 78.03/78.10 (P6(f23(a2,x13211,x13212),f23(f7(f23(x13213,a1,x13214)),x13211,x13212))),
% 78.03/78.10 inference(scs_inference,[],[914,1306,55,72,40])).
% 78.03/78.10 cnf(1322,plain,
% 78.03/78.10 (P6(x13221,x13221)),
% 78.03/78.10 inference(rename_variables,[],[55])).
% 78.03/78.10 cnf(1325,plain,
% 78.03/78.10 (E(f23(a2,x13251,x13252),f23(f7(f23(x13253,a1,x13254)),x13251,x13252))),
% 78.03/78.10 inference(rename_variables,[],[914])).
% 78.03/78.10 cnf(1326,plain,
% 78.03/78.10 (P6(f23(f7(f23(x13261,a1,x13262)),x13263,x13264),f23(a2,x13263,x13264))),
% 78.03/78.10 inference(scs_inference,[],[914,1325,575,1306,55,1322,72,40,36,39])).
% 78.03/78.10 cnf(1337,plain,
% 78.03/78.10 (P1(f23(a2,x13371,x13372),f23(f7(f23(x13373,a1,x13374)),x13371,x13372))),
% 78.03/78.10 inference(scs_inference,[],[915,54,36])).
% 78.03/78.10 cnf(1345,plain,
% 78.03/78.10 (~P9(f23(f7(f23(x13451,a1,x13452)),x13453,x13454),f23(a2,x13453,x13454))),
% 78.03/78.10 inference(scs_inference,[],[1337,72])).
% 78.03/78.10 cnf(1374,plain,
% 78.03/78.10 (P5(f17(f23(x13741,x13742,x13743),f23(x13744,a2,x13745)),f23(x13744,f7(f23(x13746,a1,x13747)),x13745))),
% 78.03/78.10 inference(scs_inference,[],[959,608,49])).
% 78.03/78.10 cnf(1378,plain,
% 78.03/78.10 (E(f23(x13781,a2,x13782),f23(x13781,f7(f23(x13783,a1,x13784)),x13782))),
% 78.03/78.10 inference(rename_variables,[],[959])).
% 78.03/78.10 cnf(1381,plain,
% 78.03/78.10 (E(f23(x13811,a2,x13812),f23(x13811,f7(f23(x13813,a1,x13814)),x13812))),
% 78.03/78.10 inference(rename_variables,[],[959])).
% 78.03/78.10 cnf(1384,plain,
% 78.03/78.10 (E(f23(x13841,a2,x13842),f23(x13841,f7(f23(x13843,a1,x13844)),x13842))),
% 78.03/78.10 inference(rename_variables,[],[959])).
% 78.03/78.10 cnf(1385,plain,
% 78.03/78.10 (P1(f23(x13851,f7(f23(x13852,a1,x13853)),x13854),f23(x13851,a2,x13854))),
% 78.03/78.10 inference(scs_inference,[],[959,1378,1381,1384,54,1337,1326,1321,608,49,37,40,39,36])).
% 78.03/78.10 cnf(1387,plain,
% 78.03/78.10 (E(f23(x13871,a2,a2),f23(x13871,f7(f23(x13872,a1,x13873)),f7(f23(x13874,a1,x13875))))),
% 78.03/78.10 inference(scs_inference,[],[959,1378,1381,1384,1080,54,1337,1326,1321,608,49,37,40,39,36,3])).
% 78.03/78.10 cnf(1401,plain,
% 78.03/78.10 (P5(f17(f23(x14011,x14012,x14013),f23(a2,a2,x14014)),f23(f7(f23(x14015,a1,x14016)),f7(f23(x14017,a1,x14018)),x14014))),
% 78.03/78.10 inference(scs_inference,[],[959,1385,1295,72,49])).
% 78.03/78.10 cnf(1403,plain,
% 78.03/78.10 (E(f23(x14031,a2,x14032),f23(x14031,f7(f23(x14033,a1,x14034)),x14032))),
% 78.03/78.10 inference(rename_variables,[],[959])).
% 78.03/78.10 cnf(1405,plain,
% 78.03/78.10 (P6(x14051,x14051)),
% 78.03/78.10 inference(rename_variables,[],[55])).
% 78.03/78.10 cnf(1406,plain,
% 78.03/78.10 (P6(f23(x14061,f7(f23(x14062,a1,x14063)),x14064),f23(x14061,a2,x14064))),
% 78.03/78.10 inference(scs_inference,[],[959,1403,1385,55,1405,1295,72,49,40,39])).
% 78.03/78.10 cnf(1424,plain,
% 78.03/78.10 (P1(f23(x14241,a2,x14242),f23(x14241,f7(f23(x14243,a1,x14244)),x14242))),
% 78.03/78.10 inference(scs_inference,[],[960,54,36])).
% 78.03/78.10 cnf(1427,plain,
% 78.03/78.10 (~P9(f23(x14271,f7(f23(x14272,a1,x14273)),x14274),f23(x14271,a2,x14274))),
% 78.03/78.11 inference(scs_inference,[],[1424,72])).
% 78.03/78.11 cnf(1455,plain,
% 78.03/78.11 (P1(f17(f23(x14551,x14552,a2),x14553),f23(f16(x14551,x14553),f6(x14552,f5(x14553,a2)),f7(f23(x14554,a1,x14555))))),
% 78.03/78.11 inference(scs_inference,[],[1080,763,608,49,37])).
% 78.03/78.11 cnf(1457,plain,
% 78.03/78.11 (E(f23(x14571,x14572,a2),f23(x14571,x14572,f7(f23(x14573,a1,x14574))))),
% 78.03/78.11 inference(rename_variables,[],[1080])).
% 78.03/78.11 cnf(1460,plain,
% 78.03/78.11 (E(f23(x14601,x14602,a2),f23(x14601,x14602,f7(f23(x14603,a1,x14604))))),
% 78.03/78.11 inference(rename_variables,[],[1080])).
% 78.03/78.11 cnf(1463,plain,
% 78.03/78.11 (E(f23(x14631,x14632,a2),f23(x14631,x14632,f7(f23(x14633,a1,x14634))))),
% 78.03/78.11 inference(rename_variables,[],[1080])).
% 78.03/78.11 cnf(1464,plain,
% 78.03/78.11 (P1(f23(x14641,x14642,f7(f23(x14643,a1,x14644))),f23(x14641,x14642,a2))),
% 78.03/78.11 inference(scs_inference,[],[1080,1457,1460,1463,54,763,461,463,608,49,37,40,39,36])).
% 78.03/78.11 cnf(1466,plain,
% 78.03/78.11 (~P9(f23(x14661,x14662,a2),f23(x14661,x14662,f7(f23(x14663,a1,x14664))))),
% 78.03/78.11 inference(scs_inference,[],[1080,1457,1460,1463,54,763,461,463,608,49,37,40,39,36,72])).
% 78.03/78.11 cnf(1478,plain,
% 78.03/78.11 (E(f23(x14781,x14782,a2),f23(x14781,x14782,f7(f23(x14783,a1,x14784))))),
% 78.03/78.11 inference(rename_variables,[],[1080])).
% 78.03/78.11 cnf(1481,plain,
% 78.03/78.11 (E(f23(x14811,x14812,a2),f23(x14811,x14812,f7(f23(x14813,a1,x14814))))),
% 78.03/78.11 inference(rename_variables,[],[1080])).
% 78.03/78.11 cnf(1484,plain,
% 78.03/78.11 (E(f23(x14841,x14842,a2),f23(x14841,x14842,f7(f23(x14843,a1,x14844))))),
% 78.03/78.11 inference(rename_variables,[],[1080])).
% 78.03/78.11 cnf(1485,plain,
% 78.03/78.11 (P6(f23(f7(f23(x14851,a1,x14852)),x14853,f7(f23(x14854,a1,x14855))),f23(a2,x14853,a2))),
% 78.03/78.11 inference(scs_inference,[],[1080,1478,1481,1484,1337,1455,1326,1321,1295,72,49,37,40,39])).
% 78.03/78.11 cnf(1487,plain,
% 78.03/78.11 (E(f23(x14871,x14872,a2),f23(x14871,x14872,f7(f23(x14873,a1,x14874))))),
% 78.03/78.11 inference(rename_variables,[],[1080])).
% 78.03/78.11 cnf(1488,plain,
% 78.03/78.11 (P1(f23(f16(x14881,x14882),f6(x14883,f5(x14882,a2)),f7(f23(x14884,a1,x14885))),f17(f23(x14881,x14883,a2),x14882))),
% 78.03/78.11 inference(scs_inference,[],[1080,1478,1481,1484,1487,719,1337,1455,1326,1321,1295,72,49,37,40,39,36])).
% 78.03/78.11 cnf(1495,plain,
% 78.03/78.11 (E(f23(x14951,x14952,a2),f23(x14951,x14952,f7(f23(x14953,a1,x14954))))),
% 78.03/78.11 inference(rename_variables,[],[1080])).
% 78.03/78.11 cnf(1496,plain,
% 78.03/78.11 (P1(f23(x14961,a2,a2),f23(x14961,f7(f23(x14962,a1,x14963)),f7(f23(x14964,a1,x14965))))),
% 78.03/78.11 inference(scs_inference,[],[1080,1495,1488,1424,1374,72,49,37])).
% 78.03/78.11 cnf(1525,plain,
% 78.03/78.11 (P6(x15251,x15251)),
% 78.03/78.11 inference(rename_variables,[],[55])).
% 78.03/78.11 cnf(1526,plain,
% 78.03/78.11 (P6(f23(x15261,x15262,f7(f23(x15263,a1,x15264))),f23(x15261,x15262,a2))),
% 78.03/78.11 inference(scs_inference,[],[1080,1496,55,1525,72,40,39])).
% 78.03/78.11 cnf(1541,plain,
% 78.03/78.11 (P1(f23(x15411,x15412,a2),f23(x15411,x15412,f7(f23(x15413,a1,x15414))))),
% 78.03/78.11 inference(scs_inference,[],[1081,54,36])).
% 78.03/78.11 cnf(1544,plain,
% 78.03/78.11 (~P9(f23(x15441,x15442,f7(f23(x15443,a1,x15444))),f23(x15441,x15442,a2))),
% 78.03/78.11 inference(scs_inference,[],[1541,72])).
% 78.03/78.11 cnf(1599,plain,
% 78.03/78.11 (E(f18(a2),f18(f7(f23(x15991,a1,x15992))))),
% 78.03/78.11 inference(scs_inference,[],[59,2,13])).
% 78.03/78.11 cnf(1600,plain,
% 78.03/78.11 (E(f18(f7(f23(x16001,a1,x16002))),f18(a2))),
% 78.03/78.11 inference(scs_inference,[],[1599,2])).
% 78.03/78.11 cnf(1610,plain,
% 78.03/78.11 (E(f20(a2,x16101),f20(f7(f23(x16102,a1,x16103)),x16101))),
% 78.03/78.11 inference(scs_inference,[],[59,2,14])).
% 78.03/78.11 cnf(1611,plain,
% 78.03/78.11 (E(f20(f7(f23(x16111,a1,x16112)),x16113),f20(a2,x16113))),
% 78.03/78.11 inference(scs_inference,[],[1610,2])).
% 78.03/78.11 cnf(1621,plain,
% 78.03/78.11 (E(f20(x16211,a2),f20(x16211,f7(f23(x16212,a1,x16213))))),
% 78.03/78.11 inference(scs_inference,[],[59,2,15])).
% 78.03/78.11 cnf(1622,plain,
% 78.03/78.11 (E(f20(x16221,f7(f23(x16222,a1,x16223))),f20(x16221,a2))),
% 78.03/78.11 inference(scs_inference,[],[1621,2])).
% 78.03/78.11 cnf(1639,plain,
% 78.03/78.11 (P2(f20(f6(f6(x16391,f5(x16392,x16393)),f5(a2,x16394)),f7(f23(x16395,a1,x16396))))),
% 78.03/78.11 inference(scs_inference,[],[505,1622,1621,191,3,41])).
% 78.03/78.11 cnf(1654,plain,
% 78.03/78.11 (~E(f10(a14,x16541),f20(f6(f13(a14,x16541),f5(a2,x16542)),f7(f23(x16543,a1,x16544))))),
% 78.03/78.11 inference(scs_inference,[],[957,1622,3])).
% 78.03/78.11 cnf(1658,plain,
% 78.03/78.11 (~E(f11(x16581,a14),f20(f6(f12(x16581,a14),f5(a2,x16582)),f7(f23(x16583,a1,x16584))))),
% 78.03/78.11 inference(scs_inference,[],[988,1622,3])).
% 78.03/78.11 cnf(1661,plain,
% 78.03/78.11 (~E(f12(x16611,a14),f20(f6(f11(x16611,a14),f5(a2,x16612)),f7(f23(x16613,a1,x16614))))),
% 78.03/78.11 inference(scs_inference,[],[990,1622,3])).
% 78.03/78.11 cnf(1664,plain,
% 78.03/78.11 (~E(f4(a14,x16641),f20(f6(f4(a1,x16642),f5(a2,x16643)),f7(f23(x16644,a1,x16645))))),
% 78.03/78.11 inference(scs_inference,[],[645,1622,3])).
% 78.03/78.11 cnf(1667,plain,
% 78.03/78.11 (~E(f4(a14,x16671),f20(f6(a1,f5(a2,x16672)),f7(f23(x16673,a1,x16674))))),
% 78.03/78.11 inference(scs_inference,[],[994,1622,3])).
% 78.03/78.11 cnf(1670,plain,
% 78.03/78.11 (~E(f13(a14,x16701),f20(f6(a2,f5(a2,x16702)),f7(f23(x16703,a1,x16704))))),
% 78.03/78.11 inference(scs_inference,[],[1206,1622,3])).
% 78.03/78.11 cnf(1685,plain,
% 78.03/78.11 (E(f19(a2,x16851),f19(f7(f23(x16852,a1,x16853)),x16851))),
% 78.03/78.11 inference(scs_inference,[],[59,2,16])).
% 78.03/78.11 cnf(1686,plain,
% 78.03/78.11 (E(f19(f7(f23(x16861,a1,x16862)),x16863),f19(a2,x16863))),
% 78.03/78.11 inference(scs_inference,[],[1685,2])).
% 78.03/78.11 cnf(1696,plain,
% 78.03/78.11 (E(f19(x16961,a2),f19(x16961,f7(f23(x16962,a1,x16963))))),
% 78.03/78.11 inference(scs_inference,[],[59,2,17])).
% 78.03/78.11 cnf(1697,plain,
% 78.03/78.11 (E(f19(x16971,f7(f23(x16972,a1,x16973))),f19(x16971,a2))),
% 78.03/78.11 inference(scs_inference,[],[1696,2])).
% 78.03/78.11 cnf(1698,plain,
% 78.03/78.11 (~E(f4(a14,x16981),f19(f6(x16982,f5(a2,a1)),f7(f23(x16983,a1,x16984))))),
% 78.03/78.11 inference(scs_inference,[],[649,1696,2,3])).
% 78.03/78.11 cnf(1720,plain,
% 78.03/78.11 (~P8(f19(x17201,a2))+P8(f19(x17201,f7(f23(x17202,a1,x17203))))),
% 78.03/78.11 inference(scs_inference,[],[1696,1003,1697,3,47])).
% 78.03/78.11 cnf(1726,plain,
% 78.03/78.11 (~E(f6(x17261,f5(x17262,x17263)),f19(f6(x17264,f5(a2,a1)),f7(f23(x17265,a1,x17266))))),
% 78.03/78.11 inference(scs_inference,[],[503,1697,3])).
% 78.03/78.11 cnf(1756,plain,
% 78.03/78.11 (P6(f18(a2),f18(f7(f23(x17561,a1,x17562))))),
% 78.03/78.11 inference(scs_inference,[],[1599,55,608,49,40])).
% 78.03/78.11 cnf(1757,plain,
% 78.03/78.11 (P6(x17571,x17571)),
% 78.03/78.11 inference(rename_variables,[],[55])).
% 78.03/78.11 cnf(1758,plain,
% 78.03/78.11 (P6(f18(f7(f23(x17581,a1,x17582))),f18(a2))),
% 78.03/78.11 inference(scs_inference,[],[1599,55,1757,608,49,40,39])).
% 78.03/78.11 cnf(1774,plain,
% 78.03/78.11 (P5(f17(f23(x17741,x17742,x17743),f20(a2,x17744)),f20(f7(f23(x17745,a1,x17746)),x17744))),
% 78.03/78.11 inference(scs_inference,[],[1610,608,49])).
% 78.03/78.11 cnf(1777,plain,
% 78.03/78.11 (P6(x17771,x17771)),
% 78.03/78.11 inference(rename_variables,[],[55])).
% 78.03/78.11 cnf(1778,plain,
% 78.03/78.11 (P6(f20(f7(f23(x17781,a1,x17782)),x17783),f20(a2,x17783))),
% 78.03/78.11 inference(scs_inference,[],[1610,55,1777,608,49,40,39])).
% 78.03/78.11 cnf(1784,plain,
% 78.03/78.11 (P1(f20(a2,x17841),f20(f7(f23(x17842,a1,x17843)),x17841))+P9(f20(f7(f23(x17842,a1,x17843)),x17841),f20(a2,x17841))),
% 78.03/78.11 inference(scs_inference,[],[1610,54,55,1777,608,49,40,39,36,72,73])).
% 78.03/78.11 cnf(1789,plain,
% 78.03/78.11 (P1(f20(a2,x17891),f20(f7(f23(x17892,a1,x17893)),x17891))),
% 78.03/78.11 inference(scs_inference,[],[117,1611,1784,50])).
% 78.03/78.11 cnf(1793,plain,
% 78.03/78.11 (P7(f6(x17931,f5(a3,a3)),a3,f20(f6(a3,f5(a2,x17932)),f7(f23(x17933,a1,x17934))))),
% 78.03/78.11 inference(scs_inference,[],[1621,405,44])).
% 78.03/78.11 cnf(1795,plain,
% 78.03/78.11 (E(f20(x17951,a2),f20(x17951,f7(f23(x17952,a1,x17953))))),
% 78.03/78.11 inference(rename_variables,[],[1621])).
% 78.03/78.11 cnf(1796,plain,
% 78.03/78.11 (P7(f6(x17961,f5(a3,a3)),f20(f6(a3,f5(a2,x17962)),f7(f23(x17963,a1,x17964))),a3)),
% 78.03/78.11 inference(scs_inference,[],[1621,1795,405,407,44,43])).
% 78.03/78.11 cnf(1798,plain,
% 78.03/78.11 (E(f20(x17981,a2),f20(x17981,f7(f23(x17982,a1,x17983))))),
% 78.03/78.11 inference(rename_variables,[],[1621])).
% 78.03/78.11 cnf(1799,plain,
% 78.03/78.11 (P4(f6(x17991,f5(x17992,x17993)),f20(f6(x17992,f5(a2,x17994)),f7(f23(x17995,a1,x17996))))),
% 78.03/78.11 inference(scs_inference,[],[1621,1795,1798,405,407,306,44,43,46])).
% 78.03/78.11 cnf(1801,plain,
% 78.03/78.11 (E(f20(x18011,a2),f20(x18011,f7(f23(x18012,a1,x18013))))),
% 78.03/78.11 inference(rename_variables,[],[1621])).
% 78.03/78.11 cnf(1804,plain,
% 78.03/78.11 (P1(f12(a9,a14),f20(f6(f11(a9,a14),f5(a2,x18041)),f7(f23(x18042,a1,x18043))))),
% 78.03/78.11 inference(scs_inference,[],[1621,1795,1798,1801,203,405,407,306,608,44,43,46,49,37])).
% 78.03/78.11 cnf(1806,plain,
% 78.03/78.11 (E(f20(x18061,a2),f20(x18061,f7(f23(x18062,a1,x18063))))),
% 78.03/78.11 inference(rename_variables,[],[1621])).
% 78.03/78.11 cnf(1809,plain,
% 78.03/78.11 (E(f20(x18091,a2),f20(x18091,f7(f23(x18092,a1,x18093))))),
% 78.03/78.11 inference(rename_variables,[],[1621])).
% 78.03/78.11 cnf(1812,plain,
% 78.03/78.11 (E(f20(x18121,a2),f20(x18121,f7(f23(x18122,a1,x18123))))),
% 78.03/78.11 inference(rename_variables,[],[1621])).
% 78.03/78.11 cnf(1813,plain,
% 78.03/78.11 (P1(f20(f6(f12(a9,a14),f5(a2,x18131)),f7(f23(x18132,a1,x18133))),f11(a9,a14))),
% 78.03/78.11 inference(scs_inference,[],[1621,1795,1798,1801,1806,1809,1812,203,205,405,407,169,172,306,608,44,43,46,49,37,40,39,36])).
% 78.03/78.11 cnf(1815,plain,
% 78.03/78.11 (E(f20(x18151,a2),f20(x18151,f7(f23(x18152,a1,x18153))))),
% 78.03/78.11 inference(rename_variables,[],[1621])).
% 78.03/78.11 cnf(1816,plain,
% 78.03/78.11 (E(f20(a2,a2),f20(f7(f23(x18161,a1,x18162)),f7(f23(x18163,a1,x18164))))),
% 78.03/78.11 inference(scs_inference,[],[1621,1795,1798,1801,1806,1809,1812,1815,203,205,1610,405,407,169,172,306,608,44,43,46,49,37,40,39,36,3])).
% 78.03/78.11 cnf(1831,plain,
% 78.03/78.11 (E(x18311,f20(f6(x18311,f5(a2,x18312)),f7(f23(x18313,a1,x18314))))),
% 78.03/78.11 inference(scs_inference,[],[1813,1793,66,1799,65,72,97,85])).
% 78.03/78.11 cnf(1837,plain,
% 78.03/78.11 (E(f20(x18371,a2),f20(x18371,f7(f23(x18372,a1,x18373))))),
% 78.03/78.11 inference(rename_variables,[],[1621])).
% 78.03/78.11 cnf(1840,plain,
% 78.03/78.11 (E(f20(x18401,a2),f20(x18401,f7(f23(x18402,a1,x18403))))),
% 78.03/78.11 inference(rename_variables,[],[1621])).
% 78.03/78.11 cnf(1841,plain,
% 78.03/78.11 (P4(f6(x18411,f5(a1,x18412)),f20(f6(f4(a1,x18413),f5(a2,x18414)),f7(f23(x18415,a1,x18416))))),
% 78.03/78.11 inference(scs_inference,[],[1621,1837,1840,216,214,1813,1793,66,510,1799,65,72,97,85,44,43,46])).
% 78.03/78.11 cnf(1843,plain,
% 78.03/78.11 (E(f20(x18431,a2),f20(x18431,f7(f23(x18432,a1,x18433))))),
% 78.03/78.11 inference(rename_variables,[],[1621])).
% 78.03/78.11 cnf(1846,plain,
% 78.03/78.11 (E(f20(x18461,a2),f20(x18461,f7(f23(x18462,a1,x18463))))),
% 78.03/78.11 inference(rename_variables,[],[1621])).
% 78.03/78.11 cnf(1849,plain,
% 78.03/78.11 (E(f20(x18491,a2),f20(x18491,f7(f23(x18492,a1,x18493))))),
% 78.03/78.11 inference(rename_variables,[],[1621])).
% 78.03/78.11 cnf(1852,plain,
% 78.03/78.11 (E(f20(x18521,a2),f20(x18521,f7(f23(x18522,a1,x18523))))),
% 78.03/78.11 inference(rename_variables,[],[1621])).
% 78.03/78.11 cnf(1855,plain,
% 78.03/78.11 (E(f20(x18551,a2),f20(x18551,f7(f23(x18552,a1,x18553))))),
% 78.03/78.11 inference(rename_variables,[],[1621])).
% 78.03/78.11 cnf(1856,plain,
% 78.03/78.11 (P1(f20(x18561,f7(f23(x18562,a1,x18563))),f20(x18561,a2))),
% 78.03/78.11 inference(scs_inference,[],[1621,1837,1840,1843,1846,1849,1852,1855,54,549,216,214,1813,1793,66,301,299,510,800,1799,65,72,97,85,44,43,46,49,37,40,39,36])).
% 78.03/78.11 cnf(1858,plain,
% 78.03/78.11 (P9(f20(f6(f12(a9,a14),f5(a2,x18581)),f7(f23(x18582,a1,x18583))),f11(a9,a14))),
% 78.03/78.11 inference(scs_inference,[],[1621,1837,1840,1843,1846,1849,1852,1855,54,549,216,214,1813,1793,66,301,299,510,800,1799,65,72,97,85,44,43,46,49,37,40,39,36,145])).
% 78.03/78.11 cnf(1867,plain,
% 78.03/78.11 (E(f20(f6(x18671,f5(a2,x18672)),f7(f23(x18673,a1,x18674))),x18671)),
% 78.03/78.11 inference(scs_inference,[],[1831,2])).
% 78.03/78.11 cnf(1870,plain,
% 78.03/78.11 (E(a1,f20(f6(f4(a1,x18701),f5(a2,x18702)),f7(f23(x18703,a1,x18704))))),
% 78.03/78.11 inference(scs_inference,[],[1831,1856,1841,65,2,72,85])).
% 78.03/78.11 cnf(1876,plain,
% 78.03/78.11 (E(f20(x18761,a2),f20(x18761,f7(f23(x18762,a1,x18763))))),
% 78.03/78.11 inference(rename_variables,[],[1621])).
% 78.03/78.11 cnf(1877,plain,
% 78.03/78.11 (P1(f23(x18771,a1,a3),f20(f6(f8(f23(x18771,a1,x18772)),f5(a2,x18773)),f7(f23(x18774,a1,x18775))))),
% 78.03/78.11 inference(scs_inference,[],[1621,1876,589,1831,1856,1774,1841,65,2,72,85,49,37])).
% 78.03/78.11 cnf(1879,plain,
% 78.03/78.11 (E(f20(x18791,a2),f20(x18791,f7(f23(x18792,a1,x18793))))),
% 78.03/78.11 inference(rename_variables,[],[1621])).
% 78.03/78.11 cnf(1882,plain,
% 78.03/78.11 (E(f20(x18821,a2),f20(x18821,f7(f23(x18822,a1,x18823))))),
% 78.03/78.11 inference(rename_variables,[],[1621])).
% 78.03/78.11 cnf(1883,plain,
% 78.03/78.11 (P6(f20(f6(x18831,f5(a2,x18832)),f7(f23(x18833,a1,x18834))),x18831)),
% 78.03/78.11 inference(scs_inference,[],[1621,1876,1879,1882,589,1831,1856,348,350,1774,1841,65,2,72,85,49,37,40,39])).
% 78.03/78.11 cnf(1885,plain,
% 78.03/78.11 (E(f20(x18851,a2),f20(x18851,f7(f23(x18852,a1,x18853))))),
% 78.03/78.11 inference(rename_variables,[],[1621])).
% 78.03/78.11 cnf(1886,plain,
% 78.03/78.11 (P1(f20(f6(f4(a1,x18861),f5(a2,x18862)),f7(f23(x18863,a1,x18864))),f4(a1,x18865))),
% 78.03/78.11 inference(scs_inference,[],[1621,1876,1879,1882,1885,553,589,1831,1856,348,350,1774,1841,65,2,72,85,49,37,40,39,36])).
% 78.03/78.11 cnf(1896,plain,
% 78.03/78.11 (E(f20(f6(f4(a1,x18961),f5(a2,x18962)),f7(f23(x18963,a1,x18964))),a1)),
% 78.03/78.11 inference(scs_inference,[],[1886,1870,72,2])).
% 78.03/78.11 cnf(1897,plain,
% 78.03/78.11 (P1(f23(x18971,a1,a3),f20(f6(f23(x18971,a1,a3),f5(a2,x18972)),f7(f23(x18973,a1,x18974))))),
% 78.03/78.11 inference(scs_inference,[],[1621,802,1886,1870,72,2,37])).
% 78.03/78.11 cnf(1916,plain,
% 78.03/78.11 (E(f20(x19161,a2),f20(x19161,f7(f23(x19162,a1,x19163))))),
% 78.03/78.11 inference(rename_variables,[],[1621])).
% 78.03/78.11 cnf(1919,plain,
% 78.03/78.11 (E(f20(x19191,a2),f20(x19191,f7(f23(x19192,a1,x19193))))),
% 78.03/78.11 inference(rename_variables,[],[1621])).
% 78.03/78.11 cnf(1920,plain,
% 78.03/78.11 (P6(f20(f6(f7(f23(x19201,a1,x19202)),f5(a2,x19203)),f7(f23(x19204,a1,x19205))),a2)),
% 78.03/78.11 inference(scs_inference,[],[1621,1916,1919,789,1877,400,402,72,37,40,39])).
% 78.03/78.11 cnf(1931,plain,
% 78.03/78.11 (E(f20(x19311,a2),f20(x19311,f7(f23(x19312,a1,x19313))))),
% 78.03/78.11 inference(rename_variables,[],[1621])).
% 78.03/78.11 cnf(1934,plain,
% 78.03/78.11 (E(f20(x19341,a2),f20(x19341,f7(f23(x19342,a1,x19343))))),
% 78.03/78.11 inference(rename_variables,[],[1621])).
% 78.03/78.11 cnf(1935,plain,
% 78.03/78.11 (P6(f20(f6(f4(a1,x19351),f5(a2,x19352)),f7(f23(x19353,a1,x19354))),a1)),
% 78.03/78.11 inference(scs_inference,[],[1621,1931,1934,895,1804,160,261,72,37,40,39])).
% 78.03/78.11 cnf(1943,plain,
% 78.03/78.11 (P1(f20(a2,a2),f20(f7(f23(x19431,a1,x19432)),f7(f23(x19433,a1,x19434))))),
% 78.03/78.11 inference(scs_inference,[],[1621,1897,1789,72,37])).
% 78.03/78.11 cnf(1977,plain,
% 78.03/78.11 (P6(x19771,x19771)),
% 78.03/78.11 inference(rename_variables,[],[55])).
% 78.03/78.11 cnf(1978,plain,
% 78.03/78.11 (P6(f20(x19781,f7(f23(x19782,a1,x19783))),f20(x19781,a2))),
% 78.03/78.11 inference(scs_inference,[],[1621,1943,55,1977,72,40,39])).
% 78.03/78.11 cnf(2048,plain,
% 78.03/78.11 (P5(f17(f23(x20481,x20482,x20483),f19(a2,x20484)),f19(f7(f23(x20485,a1,x20486)),x20484))),
% 78.03/78.11 inference(scs_inference,[],[1685,608,49])).
% 78.03/78.11 cnf(2051,plain,
% 78.03/78.11 (P6(x20511,x20511)),
% 78.03/78.11 inference(rename_variables,[],[55])).
% 78.03/78.11 cnf(2052,plain,
% 78.03/78.11 (P6(f19(f7(f23(x20521,a1,x20522)),x20523),f19(a2,x20523))),
% 78.03/78.11 inference(scs_inference,[],[1685,55,2051,608,49,40,39])).
% 78.03/78.11 cnf(2063,plain,
% 78.03/78.11 (P1(f19(a2,x20631),f19(f7(f23(x20632,a1,x20633)),x20631))),
% 78.03/78.11 inference(scs_inference,[],[1686,54,36])).
% 78.03/78.11 cnf(2071,plain,
% 78.03/78.11 (E(f19(x20711,a2),f19(x20711,f7(f23(x20712,a1,x20713))))),
% 78.03/78.11 inference(rename_variables,[],[1696])).
% 78.03/78.11 cnf(2072,plain,
% 78.03/78.11 (P7(f6(x20721,f5(a3,a3)),f19(f6(x20722,f5(a2,a3)),f7(f23(x20723,a1,x20724))),a3)),
% 78.03/78.11 inference(scs_inference,[],[1696,2071,483,481,44,43])).
% 78.03/78.11 cnf(2074,plain,
% 78.03/78.11 (E(f19(x20741,a2),f19(x20741,f7(f23(x20742,a1,x20743))))),
% 78.03/78.11 inference(rename_variables,[],[1696])).
% 78.03/78.11 cnf(2075,plain,
% 78.03/78.11 (P4(f6(x20751,f5(x20752,x20753)),f19(f6(x20754,f5(a2,x20752)),f7(f23(x20755,a1,x20756))))),
% 78.03/78.11 inference(scs_inference,[],[1696,2071,2074,483,481,524,44,43,46])).
% 78.03/78.11 cnf(2077,plain,
% 78.03/78.11 (E(f19(x20771,a2),f19(x20771,f7(f23(x20772,a1,x20773))))),
% 78.03/78.11 inference(rename_variables,[],[1696])).
% 78.03/78.11 cnf(2080,plain,
% 78.03/78.11 (P1(f4(a1,x20801),f19(f6(x20802,f5(a2,a1)),f7(f23(x20803,a1,x20804))))),
% 78.03/78.11 inference(scs_inference,[],[1696,2071,2074,2077,559,483,481,524,608,44,43,46,49,37])).
% 78.03/78.11 cnf(2082,plain,
% 78.03/78.11 (E(f19(x20821,a2),f19(x20821,f7(f23(x20822,a1,x20823))))),
% 78.03/78.11 inference(rename_variables,[],[1696])).
% 78.03/78.11 cnf(2085,plain,
% 78.03/78.11 (E(f19(x20851,a2),f19(x20851,f7(f23(x20852,a1,x20853))))),
% 78.03/78.11 inference(rename_variables,[],[1696])).
% 78.03/78.11 cnf(2086,plain,
% 78.03/78.11 (P6(f19(f6(x20861,f5(a2,a1)),f7(f23(x20862,a1,x20863))),f4(a1,x20864))),
% 78.03/78.11 inference(scs_inference,[],[1696,2071,2074,2077,2082,2085,559,483,481,181,187,524,608,44,43,46,49,37,40,39])).
% 78.03/78.11 cnf(2088,plain,
% 78.03/78.11 (E(f19(x20881,a2),f19(x20881,f7(f23(x20882,a1,x20883))))),
% 78.03/78.11 inference(rename_variables,[],[1696])).
% 78.03/78.11 cnf(2089,plain,
% 78.03/78.11 (P1(f19(x20891,f7(f23(x20892,a1,x20893))),f19(x20891,a2))),
% 78.03/78.11 inference(scs_inference,[],[1696,2071,2074,2077,2082,2085,2088,54,559,483,481,181,187,524,608,44,43,46,49,37,40,39,36])).
% 78.03/78.11 cnf(2091,plain,
% 78.03/78.11 (E(f19(a2,a2),f19(f7(f23(x20911,a1,x20912)),f7(f23(x20913,a1,x20914))))),
% 78.03/78.11 inference(scs_inference,[],[1696,2071,2074,2077,2082,2085,2088,1685,54,559,483,481,181,187,524,608,44,43,46,49,37,40,39,36,3])).
% 78.03/78.11 cnf(2094,plain,
% 78.03/78.11 (E(f19(f7(f23(x20941,a1,x20942)),f7(f23(x20943,a1,x20944))),f19(a2,a2))),
% 78.03/78.11 inference(scs_inference,[],[1696,2071,2074,2077,2082,2085,2088,1685,54,559,483,481,181,187,524,608,44,43,46,49,37,40,39,36,3,2])).
% 78.03/78.11 cnf(2108,plain,
% 78.03/78.11 (E(x21081,f19(f6(x21082,f5(a2,x21081)),f7(f23(x21083,a1,x21084))))),
% 78.03/78.11 inference(scs_inference,[],[2089,2072,66,2075,65,72,98,85])).
% 78.03/78.11 cnf(2114,plain,
% 78.03/78.11 (E(f19(x21141,a2),f19(x21141,f7(f23(x21142,a1,x21143))))),
% 78.03/78.11 inference(rename_variables,[],[1696])).
% 78.03/78.11 cnf(2115,plain,
% 78.03/78.11 (P1(a1,f19(f6(x21151,f5(a2,a1)),f7(f23(x21152,a1,x21153))))),
% 78.03/78.11 inference(scs_inference,[],[1696,2114,670,2089,2072,66,668,2075,65,72,98,85,49,37])).
% 78.03/78.11 cnf(2117,plain,
% 78.03/78.12 (E(f19(x21171,a2),f19(x21171,f7(f23(x21172,a1,x21173))))),
% 78.03/78.12 inference(rename_variables,[],[1696])).
% 78.03/78.12 cnf(2120,plain,
% 78.03/78.12 (E(f19(x21201,a2),f19(x21201,f7(f23(x21202,a1,x21203))))),
% 78.03/78.12 inference(rename_variables,[],[1696])).
% 78.03/78.12 cnf(2121,plain,
% 78.03/78.12 (P6(f19(f6(x21211,f5(a2,x21212)),f7(f23(x21213,a1,x21214))),x21212)),
% 78.03/78.12 inference(scs_inference,[],[1696,2114,2117,2120,670,2089,2072,66,436,434,668,2075,65,72,98,85,49,37,40,39])).
% 78.03/78.12 cnf(2123,plain,
% 78.03/78.12 (E(f19(x21231,a2),f19(x21231,f7(f23(x21232,a1,x21233))))),
% 78.03/78.12 inference(rename_variables,[],[1696])).
% 78.03/78.12 cnf(2124,plain,
% 78.03/78.12 (P1(f19(f6(x21241,f5(a2,a1)),f7(f23(x21242,a1,x21243))),f4(a1,x21244))),
% 78.03/78.12 inference(scs_inference,[],[1696,2114,2117,2120,2123,582,670,2089,2072,66,436,434,668,2075,65,72,98,85,49,37,40,39,36])).
% 78.03/78.12 cnf(2131,plain,
% 78.03/78.12 (E(f19(f6(x21311,f5(a2,x21312)),f7(f23(x21313,a1,x21314))),x21312)),
% 78.03/78.12 inference(scs_inference,[],[2108,2])).
% 78.03/78.12 cnf(2136,plain,
% 78.03/78.12 (E(f19(x21361,a2),f19(x21361,f7(f23(x21362,a1,x21363))))),
% 78.03/78.12 inference(rename_variables,[],[1696])).
% 78.03/78.12 cnf(2139,plain,
% 78.03/78.12 (E(f19(x21391,a2),f19(x21391,f7(f23(x21392,a1,x21393))))),
% 78.03/78.12 inference(rename_variables,[],[1696])).
% 78.03/78.12 cnf(2142,plain,
% 78.03/78.12 (E(f19(x21421,a2),f19(x21421,f7(f23(x21422,a1,x21423))))),
% 78.03/78.12 inference(rename_variables,[],[1696])).
% 78.03/78.12 cnf(2145,plain,
% 78.03/78.12 (E(f19(x21451,a2),f19(x21451,f7(f23(x21452,a1,x21453))))),
% 78.03/78.12 inference(rename_variables,[],[1696])).
% 78.03/78.12 cnf(2146,plain,
% 78.03/78.12 (P1(f19(f6(x21461,f5(a2,x21462)),f7(f23(x21463,a1,x21464))),x21462)),
% 78.03/78.12 inference(scs_inference,[],[1696,2136,2139,2142,2145,526,2080,2063,2108,528,530,2048,2,72,49,37,40,39,36])).
% 78.03/78.12 cnf(2154,plain,
% 78.03/78.12 (P6(f19(f7(f23(x21541,a1,x21542)),f7(f23(x21543,a1,x21544))),f19(a2,a2))),
% 78.03/78.12 inference(scs_inference,[],[1696,2115,2052,72,39])).
% 78.03/78.12 cnf(2172,plain,
% 78.03/78.12 (P6(f19(x21721,f7(f23(x21722,a1,x21723))),f19(x21721,a2))),
% 78.03/78.12 inference(scs_inference,[],[1696,2124,55,72,39])).
% 78.03/78.12 cnf(2173,plain,
% 78.03/78.12 (P6(x21731,x21731)),
% 78.03/78.12 inference(rename_variables,[],[55])).
% 78.03/78.12 cnf(2174,plain,
% 78.03/78.12 (P6(f19(x21741,a2),f19(x21741,f7(f23(x21742,a1,x21743))))),
% 78.03/78.12 inference(scs_inference,[],[1696,2124,55,2173,72,39,40])).
% 78.03/78.12 cnf(2187,plain,
% 78.03/78.12 (~P9(x21871,f19(f6(x21872,f5(a2,x21871)),f7(f23(x21873,a1,x21874))))),
% 78.03/78.12 inference(scs_inference,[],[2146,72])).
% 78.03/78.12 cnf(2194,plain,
% 78.03/78.12 (P1(f19(x21941,a2),f19(x21941,f7(f23(x21942,a1,x21943))))),
% 78.03/78.12 inference(scs_inference,[],[1697,54,36])).
% 78.03/78.12 cnf(2224,plain,
% 78.03/78.12 (E(x22241,f20(f6(x22241,f5(a2,x22242)),f7(f23(x22243,a1,x22244))))),
% 78.03/78.12 inference(rename_variables,[],[1831])).
% 78.03/78.12 cnf(2226,plain,
% 78.03/78.12 (E(x22261,f20(f6(x22261,f5(a2,x22262)),f7(f23(x22263,a1,x22264))))),
% 78.03/78.12 inference(rename_variables,[],[1831])).
% 78.03/78.12 cnf(2228,plain,
% 78.03/78.12 (E(x22281,f20(f6(x22281,f5(a2,x22282)),f7(f23(x22283,a1,x22284))))),
% 78.03/78.12 inference(rename_variables,[],[1831])).
% 78.03/78.12 cnf(2229,plain,
% 78.03/78.12 (P5(f17(f23(x22291,x22292,x22293),x22294),f20(f6(x22294,f5(a2,x22295)),f7(f23(x22296,a1,x22297))))),
% 78.03/78.12 inference(scs_inference,[],[1831,2224,2226,2228,618,608,48,44,43,49])).
% 78.03/78.12 cnf(2231,plain,
% 78.03/78.12 (P1(f4(a1,x22311),f20(f6(a1,f5(a2,x22312)),f7(f23(x22313,a1,x22314))))),
% 78.03/78.12 inference(scs_inference,[],[1831,2224,2226,2228,618,543,608,48,44,43,49,37])).
% 78.03/78.12 cnf(2232,plain,
% 78.03/78.12 (E(x22321,f20(f6(x22321,f5(a2,x22322)),f7(f23(x22323,a1,x22324))))),
% 78.03/78.12 inference(rename_variables,[],[1831])).
% 78.03/78.12 cnf(2233,plain,
% 78.03/78.12 (P1(f20(f6(x22331,f5(a2,x22332)),f7(f23(x22333,a1,x22334))),x22331)),
% 78.03/78.12 inference(scs_inference,[],[1831,2224,2226,2228,2232,618,54,543,608,48,44,43,49,37,36])).
% 78.03/78.12 cnf(2243,plain,
% 78.03/78.12 (~P9(x22431,f20(f6(x22431,f5(a2,x22432)),f7(f23(x22433,a1,x22434))))),
% 78.03/78.12 inference(scs_inference,[],[2233,72])).
% 78.03/78.12 cnf(2246,plain,
% 78.03/78.12 (E(x22461,f20(f6(x22461,f5(a2,x22462)),f7(f23(x22463,a1,x22464))))),
% 78.03/78.12 inference(rename_variables,[],[1831])).
% 78.03/78.12 cnf(2248,plain,
% 78.03/78.12 (E(x22481,f20(f6(x22481,f5(a2,x22482)),f7(f23(x22483,a1,x22484))))),
% 78.03/78.12 inference(rename_variables,[],[1831])).
% 78.03/78.12 cnf(2250,plain,
% 78.03/78.12 (E(x22501,f20(f6(x22501,f5(a2,x22502)),f7(f23(x22503,a1,x22504))))),
% 78.03/78.12 inference(rename_variables,[],[1831])).
% 78.03/78.12 cnf(2252,plain,
% 78.03/78.12 (E(x22521,f20(f6(x22521,f5(a2,x22522)),f7(f23(x22523,a1,x22524))))),
% 78.03/78.12 inference(rename_variables,[],[1831])).
% 78.03/78.12 cnf(2254,plain,
% 78.03/78.12 (E(x22541,f20(f6(x22541,f5(a2,x22542)),f7(f23(x22543,a1,x22544))))),
% 78.03/78.12 inference(rename_variables,[],[1831])).
% 78.03/78.12 cnf(2255,plain,
% 78.03/78.12 (P1(f20(f6(a2,f5(a2,x22551)),f7(f23(x22552,a1,x22553))),x22554)),
% 78.03/78.12 inference(scs_inference,[],[1831,2246,2248,2250,2252,2254,53,492,620,2233,675,72,48,44,43,49,37,36])).
% 78.03/78.12 cnf(2259,plain,
% 78.03/78.12 (~P4(f20(f6(f4(a1,x22591),f5(x22592,x22593)),x22592),x22594)),
% 78.03/78.12 inference(scs_inference,[],[439,84])).
% 78.03/78.12 cnf(2261,plain,
% 78.03/78.12 (~P3(f17(f23(x22611,a14,f7(f23(x22612,a1,x22613))),x22614))),
% 78.03/78.12 inference(scs_inference,[],[1196,439,84,295])).
% 78.03/78.12 cnf(2262,plain,
% 78.03/78.12 (P1(f12(a9,a14),f19(f6(x22621,f5(x22622,f11(a9,a14))),x22622))),
% 78.03/78.12 inference(scs_inference,[],[1196,168,439,84,295,165])).
% 78.03/78.12 cnf(2263,plain,
% 78.03/78.12 (E(x22631,f19(f6(x22632,f5(x22633,x22631)),x22633))),
% 78.03/78.12 inference(rename_variables,[],[168])).
% 78.03/78.12 cnf(2264,plain,
% 78.03/78.12 (P1(f19(f6(x22641,f5(x22642,f12(a9,a14))),x22642),f11(a9,a14))),
% 78.03/78.12 inference(scs_inference,[],[1196,168,2263,439,84,295,165,174])).
% 78.03/78.12 cnf(2265,plain,
% 78.03/78.12 (E(x22651,f19(f6(x22652,f5(x22653,x22651)),x22653))),
% 78.03/78.12 inference(rename_variables,[],[168])).
% 78.03/78.12 cnf(2266,plain,
% 78.03/78.12 (P9(f19(f6(x22661,f5(x22662,f12(a9,a14))),x22662),f11(a9,a14))),
% 78.03/78.12 inference(scs_inference,[],[1196,168,2263,2265,439,84,295,165,174,145])).
% 78.03/78.12 cnf(2267,plain,
% 78.03/78.12 (E(x22671,f19(f6(x22672,f5(x22673,x22671)),x22673))),
% 78.03/78.12 inference(rename_variables,[],[168])).
% 78.03/78.12 cnf(2268,plain,
% 78.03/78.12 (P7(f6(a14,f5(x22681,a2)),f12(f16(x22682,x22681),f6(a14,f5(x22681,a2))),f11(f16(x22682,x22681),f6(a14,f5(x22681,a2))))),
% 78.03/78.12 inference(scs_inference,[],[1197,1196,168,2263,2265,439,84,295,165,174,145,93])).
% 78.03/78.12 cnf(2270,plain,
% 78.03/78.12 (~P1(f11(f16(x22701,x22702),f6(a14,f5(x22702,a2))),f12(f16(x22701,x22702),f6(a14,f5(x22702,a2))))),
% 78.03/78.12 inference(scs_inference,[],[1197,1196,168,2263,2265,439,84,295,165,174,145,93,92])).
% 78.03/78.12 cnf(2283,plain,
% 78.03/78.12 (E(x22831,f19(f6(x22832,f5(x22833,x22831)),x22833))),
% 78.03/78.12 inference(rename_variables,[],[168])).
% 78.03/78.12 cnf(2286,plain,
% 78.03/78.12 (P4(f6(x22861,f5(f4(a1,x22862),x22863)),f20(f6(f4(a1,x22864),f5(x22865,x22866)),x22865))),
% 78.03/78.12 inference(scs_inference,[],[1197,1196,618,151,168,2263,2265,2267,624,458,2255,864,2187,138,608,439,480,84,295,165,174,145,93,92,70,2,72,85,48,44,51,46])).
% 78.03/78.12 cnf(2287,plain,
% 78.03/78.12 (P7(a14,f19(f6(x22871,f5(x22872,f12(x22873,a14))),x22872),f11(x22873,a14))),
% 78.03/78.12 inference(scs_inference,[],[1197,1196,618,151,168,2263,2265,2267,2283,624,458,2255,864,2187,138,608,439,480,84,295,165,174,145,93,92,70,2,72,85,48,44,51,46,43])).
% 78.03/78.12 cnf(2289,plain,
% 78.03/78.12 (~E(f19(f6(x22891,f5(x22892,f12(a9,a14))),x22892),f11(a9,a14))),
% 78.03/78.12 inference(scs_inference,[],[1197,1196,618,151,168,2263,2265,2267,2283,624,458,2255,864,2187,117,138,608,439,480,84,295,165,174,145,93,92,70,2,72,85,48,44,51,46,43,50])).
% 78.03/78.12 cnf(2298,plain,
% 78.03/78.12 (P1(f20(f6(f4(a1,x22981),f5(x22982,x22983)),x22982),f19(f6(x22984,f5(x22985,a1)),x22985))),
% 78.03/78.12 inference(scs_inference,[],[1197,1196,618,440,774,151,249,168,2263,2265,2267,2283,670,826,624,458,2255,864,261,218,2187,117,138,608,1007,439,480,84,295,165,174,145,93,92,70,2,72,85,48,44,51,46,43,50,49,37,39,40,36])).
% 78.03/78.12 cnf(2299,plain,
% 78.03/78.12 (E(f5(f7(f23(x22991,a1,x22992)),x22993),f5(f7(f23(x22994,a1,x22995)),x22993))),
% 78.03/78.12 inference(scs_inference,[],[1197,1196,618,440,441,774,151,249,168,2263,2265,2267,2283,670,826,624,458,2255,864,261,218,2187,117,138,608,1007,439,480,84,295,165,174,145,93,92,70,2,72,85,48,44,51,46,43,50,49,37,39,40,36,3])).
% 78.03/78.12 cnf(2305,plain,
% 78.03/78.12 (P9(f12(f16(x23051,x23052),f6(a14,f5(x23052,a2))),f11(f16(x23051,x23052),f6(a14,f5(x23052,a2))))),
% 78.03/78.12 inference(scs_inference,[],[1197,1196,618,440,441,774,151,249,168,2263,2265,2267,2283,670,826,624,458,2255,864,261,218,2187,117,138,608,1007,439,480,84,295,165,174,145,93,92,70,2,72,85,48,44,51,46,43,50,49,37,39,40,36,3,69,98,73])).
% 78.03/78.12 cnf(2312,plain,
% 78.03/78.12 (P6(f19(x23121,f7(f23(x23122,a1,x23123))),f8(f19(x23121,a2)))),
% 78.03/78.12 inference(scs_inference,[],[2172,71])).
% 78.03/78.12 cnf(2314,plain,
% 78.03/78.12 (P6(f19(x23141,f7(f23(x23142,a1,x23143))),f17(f19(x23141,a2),x23144))),
% 78.03/78.12 inference(scs_inference,[],[2172,71,75])).
% 78.03/78.12 cnf(2316,plain,
% 78.03/78.12 (P6(f19(x23161,f7(f23(x23162,a1,x23163))),f21(f19(x23161,a2),x23164))),
% 78.03/78.12 inference(scs_inference,[],[2172,71,75,76])).
% 78.03/78.12 cnf(2344,plain,
% 78.03/78.12 (E(f12(f19(f6(x23441,f5(a2,x23442)),f7(f23(x23443,a1,x23444))),x23445),f12(x23442,x23445))),
% 78.03/78.12 inference(scs_inference,[],[2172,2286,2131,1308,71,75,76,13,24,25,78,80,5,6,7,8,9,14,15,16,17,18,19,20,21,22,23,26,27,28,29,30])).
% 78.03/78.12 cnf(2346,plain,
% 78.03/78.12 (E(f11(f19(f6(x23461,f5(a2,x23462)),f7(f23(x23463,a1,x23464))),x23465),f11(x23462,x23465))),
% 78.03/78.12 inference(scs_inference,[],[2172,2286,2131,1308,71,75,76,13,24,25,78,80,5,6,7,8,9,14,15,16,17,18,19,20,21,22,23,26,27,28,29,30,31,32])).
% 78.03/78.12 cnf(2352,plain,
% 78.03/78.12 (P7(f6(a14,f5(x23521,x23522)),f19(f6(x23523,f5(x23524,f12(x23525,a14))),x23524),f11(x23525,a14))),
% 78.03/78.12 inference(scs_inference,[],[2172,2287,2286,2131,1308,71,75,76,13,24,25,78,80,5,6,7,8,9,14,15,16,17,18,19,20,21,22,23,26,27,28,29,30,31,32,33,34,35,77,94])).
% 78.03/78.12 cnf(2357,plain,
% 78.03/78.12 (E(f7(f23(x23571,f4(a14,x23572),x23573)),f18(x23571))),
% 78.03/78.12 inference(scs_inference,[],[2172,2287,2286,2131,1308,642,71,75,76,13,24,25,78,80,5,6,7,8,9,14,15,16,17,18,19,20,21,22,23,26,27,28,29,30,31,32,33,34,35,77,94,10,11,12,81])).
% 78.03/78.12 cnf(2359,plain,
% 78.03/78.12 (~P3(f23(x23591,f6(x23592,f5(f12(x23593,a14),f11(x23593,a14))),x23594))),
% 78.03/78.12 inference(scs_inference,[],[2172,2287,2286,2131,1308,642,631,71,75,76,13,24,25,78,80,5,6,7,8,9,14,15,16,17,18,19,20,21,22,23,26,27,28,29,30,31,32,33,34,35,77,94,10,11,12,81,104])).
% 78.03/78.12 cnf(2361,plain,
% 78.03/78.12 (E(f21(f23(x23611,a1,x23612),x23613),f23(x23611,a1,a3))),
% 78.03/78.12 inference(scs_inference,[],[2172,2287,2286,2131,1308,642,631,65,71,75,76,13,24,25,78,80,5,6,7,8,9,14,15,16,17,18,19,20,21,22,23,26,27,28,29,30,31,32,33,34,35,77,94,10,11,12,81,104,90])).
% 78.03/78.12 cnf(2364,plain,
% 78.03/78.12 (E(x23641,f19(f6(x23642,f5(a2,x23641)),f7(f23(x23643,a1,x23644))))),
% 78.03/78.12 inference(rename_variables,[],[2108])).
% 78.03/78.12 cnf(2372,plain,
% 78.03/78.12 (~P5(f23(x23721,a1,x23722),x23723)),
% 78.03/78.12 inference(scs_inference,[],[2172,2287,2286,2131,513,1308,2108,2364,642,631,65,71,75,76,13,24,25,78,80,5,6,7,8,9,14,15,16,17,18,19,20,21,22,23,26,27,28,29,30,31,32,33,34,35,77,94,10,11,12,81,104,90,143,144,87,88,4,91])).
% 78.03/78.12 cnf(2376,plain,
% 78.03/78.12 (P1(f10(a14,x23761),f13(a14,x23761))),
% 78.03/78.12 inference(scs_inference,[],[2172,2287,2286,2131,567,513,1308,2108,2364,642,631,624,65,71,75,76,13,24,25,78,80,5,6,7,8,9,14,15,16,17,18,19,20,21,22,23,26,27,28,29,30,31,32,33,34,35,77,94,10,11,12,81,104,90,143,144,87,88,4,91,84,70])).
% 78.03/78.12 cnf(2378,plain,
% 78.03/78.12 (~E(f19(f6(x23781,f5(x23782,a2)),x23782),f13(a14,x23783))),
% 78.03/78.12 inference(scs_inference,[],[2172,885,2287,2286,2131,567,513,1308,2108,2364,642,631,624,65,71,75,76,13,24,25,78,80,5,6,7,8,9,14,15,16,17,18,19,20,21,22,23,26,27,28,29,30,31,32,33,34,35,77,94,10,11,12,81,104,90,143,144,87,88,4,91,84,70,2])).
% 78.03/78.12 cnf(2379,plain,
% 78.03/78.12 (~P1(f11(a9,a14),f19(f6(x23791,f5(x23792,f12(a9,a14))),x23792))),
% 78.03/78.12 inference(scs_inference,[],[2172,885,2266,2287,2286,2131,567,513,1308,2108,2364,642,631,624,65,71,75,76,13,24,25,78,80,5,6,7,8,9,14,15,16,17,18,19,20,21,22,23,26,27,28,29,30,31,32,33,34,35,77,94,10,11,12,81,104,90,143,144,87,88,4,91,84,70,2,72])).
% 78.03/78.12 cnf(2381,plain,
% 78.03/78.12 (P7(f6(x23811,f5(f4(a1,x23812),f4(a1,x23812))),f4(a1,x23813),f4(a1,x23813))),
% 78.03/78.12 inference(scs_inference,[],[2172,885,2266,2287,2286,2131,567,513,1308,2108,2364,642,631,624,162,65,71,75,76,13,24,25,78,80,5,6,7,8,9,14,15,16,17,18,19,20,21,22,23,26,27,28,29,30,31,32,33,34,35,77,94,10,11,12,81,104,90,143,144,87,88,4,91,84,70,2,72,83])).
% 78.03/78.12 cnf(2383,plain,
% 78.03/78.12 (P9(f10(f6(a14,f5(x23831,a2)),x23832),f13(f6(a14,f5(x23831,a2)),x23832))),
% 78.03/78.12 inference(scs_inference,[],[2172,885,2266,2287,2286,2305,2268,2131,567,513,1308,2108,2364,642,631,624,162,65,71,75,76,13,24,25,78,80,5,6,7,8,9,14,15,16,17,18,19,20,21,22,23,26,27,28,29,30,31,32,33,34,35,77,94,10,11,12,81,104,90,143,144,87,88,4,91,84,70,2,72,83,86])).
% 78.03/78.12 cnf(2386,plain,
% 78.03/78.12 (P7(f4(f4(a14,x23861),x23862),f10(f4(a14,x23861),x23862),f13(f4(a14,x23861),x23862))),
% 78.03/78.12 inference(scs_inference,[],[2172,885,2266,2287,2286,2305,2268,2131,567,513,1308,641,2108,2364,642,631,624,162,65,71,75,76,13,24,25,78,80,5,6,7,8,9,14,15,16,17,18,19,20,21,22,23,26,27,28,29,30,31,32,33,34,35,77,94,10,11,12,81,104,90,143,144,87,88,4,91,84,70,2,72,83,86,96])).
% 78.03/78.12 cnf(2390,plain,
% 78.03/78.12 (P4(f6(x23901,f5(a1,x23902)),f4(a1,x23903))),
% 78.03/78.12 inference(rename_variables,[],[487])).
% 78.03/78.12 cnf(2395,plain,
% 78.03/78.12 (~P3(f23(x23951,f6(a14,f5(x23952,a2)),x23953))),
% 78.03/78.12 inference(scs_inference,[],[2172,885,2266,2287,2286,2270,2305,2268,2131,567,513,487,2390,1308,220,641,2108,2364,642,631,624,162,65,71,75,76,13,24,25,78,80,5,6,7,8,9,14,15,16,17,18,19,20,21,22,23,26,27,28,29,30,31,32,33,34,35,77,94,10,11,12,81,104,90,143,144,87,88,4,91,84,70,2,72,83,86,96,82,89,99])).
% 78.03/78.12 cnf(2398,plain,
% 78.03/78.12 (~P7(f6(a1,f5(f13(a14,x23981),x23982)),f19(f6(x23983,f5(x23984,a2)),x23984),x23985)),
% 78.03/78.12 inference(scs_inference,[],[2172,885,2266,2287,2286,2270,2305,2268,2131,567,513,487,2390,1308,220,641,2108,2364,642,631,624,162,66,65,71,75,76,13,24,25,78,80,5,6,7,8,9,14,15,16,17,18,19,20,21,22,23,26,27,28,29,30,31,32,33,34,35,77,94,10,11,12,81,104,90,143,144,87,88,4,91,84,70,2,72,83,86,96,82,89,99,98])).
% 78.03/78.12 cnf(2399,plain,
% 78.03/78.12 (~P7(a1,x23991,x23992)),
% 78.03/78.12 inference(rename_variables,[],[66])).
% 78.03/78.12 cnf(2405,plain,
% 78.03/78.12 (~P7(f6(a1,f5(x24051,f13(a14,x24052))),x24053,f19(f6(x24054,f5(x24055,a2)),x24055))),
% 78.03/78.12 inference(scs_inference,[],[2172,885,2266,2287,2286,2270,2305,2262,2268,2131,567,513,487,2390,1308,220,2089,641,2108,2364,642,631,624,162,66,2399,65,71,75,76,13,24,25,78,80,5,6,7,8,9,14,15,16,17,18,19,20,21,22,23,26,27,28,29,30,31,32,33,34,35,77,94,10,11,12,81,104,90,143,144,87,88,4,91,84,70,2,72,83,86,96,82,89,99,98,74,97])).
% 78.03/78.12 cnf(2408,plain,
% 78.03/78.12 (~P4(f19(f6(x24081,f5(a2,a1)),f7(f23(x24082,a1,x24083))),x24084)),
% 78.03/78.12 inference(scs_inference,[],[2172,885,2266,2287,2286,2270,2305,2262,2268,2131,567,513,487,2390,1308,220,2089,641,2108,2364,642,631,624,162,66,2399,65,71,75,76,13,24,25,78,80,5,6,7,8,9,14,15,16,17,18,19,20,21,22,23,26,27,28,29,30,31,32,33,34,35,77,94,10,11,12,81,104,90,143,144,87,88,4,91,84,70,2,72,83,86,96,82,89,99,98,74,97,45])).
% 78.03/78.12 cnf(2409,plain,
% 78.03/78.12 (E(f19(f6(x24091,f5(a2,x24092)),f7(f23(x24093,a1,x24094))),x24092)),
% 78.03/78.12 inference(rename_variables,[],[2131])).
% 78.03/78.12 cnf(2414,plain,
% 78.03/78.12 (E(f19(f6(x24141,f5(a2,x24142)),f7(f23(x24143,a1,x24144))),x24142)),
% 78.03/78.12 inference(rename_variables,[],[2131])).
% 78.03/78.12 cnf(2425,plain,
% 78.03/78.12 (E(f19(f6(x24251,f5(a2,x24252)),f7(f23(x24253,a1,x24254))),x24252)),
% 78.03/78.12 inference(rename_variables,[],[2131])).
% 78.03/78.12 cnf(2432,plain,
% 78.03/78.12 (~E(f8(f23(a9,a14,a15)),f20(f6(f23(a9,a14,a15),f5(x24321,x24322)),x24321))),
% 78.03/78.12 inference(scs_inference,[],[62,1022,1077,2172,119,885,1639,2266,2289,2287,2286,2299,2270,2305,2262,677,466,2268,639,450,2131,2409,2414,2425,1274,567,513,487,2390,1308,135,220,2089,641,2108,2364,642,631,624,616,162,66,2399,68,65,71,75,76,13,24,25,78,80,5,6,7,8,9,14,15,16,17,18,19,20,21,22,23,26,27,28,29,30,31,32,33,34,35,77,94,10,11,12,81,104,90,143,144,87,88,4,91,84,70,2,72,83,86,96,82,89,99,98,74,97,45,42,48,51,50,37,36,3,41,47,38])).
% 78.03/78.12 cnf(2436,plain,
% 78.03/78.12 (~P3(f23(x24361,f6(f6(a14,f5(f11(x24362,a14),f12(x24362,a14))),f5(x24363,a2)),x24364))),
% 78.03/78.12 inference(scs_inference,[],[62,1022,1077,2172,119,885,1639,2266,2289,2287,2286,2299,2270,2305,2262,677,466,2268,639,450,644,2131,2409,2414,2425,1274,567,513,487,2390,1308,135,220,2089,641,2108,2364,642,631,624,616,162,66,2399,68,65,53,71,75,76,13,24,25,78,80,5,6,7,8,9,14,15,16,17,18,19,20,21,22,23,26,27,28,29,30,31,32,33,34,35,77,94,10,11,12,81,104,90,143,144,87,88,4,91,84,70,2,72,83,86,96,82,89,99,98,74,97,45,42,48,51,50,37,36,3,41,47,38,1720,69,106])).
% 78.03/78.12 cnf(2440,plain,
% 78.03/78.12 (P3(f23(x24401,f6(a1,f5(f4(a1,x24402),f4(a1,x24403))),x24404))),
% 78.03/78.12 inference(scs_inference,[],[62,1022,1077,2172,119,885,1639,2266,2289,2287,2286,2299,2270,2305,2262,677,466,2268,639,450,644,2131,2409,2414,2425,1274,567,513,519,487,2390,1308,135,220,2089,641,2108,2364,642,631,624,60,616,162,66,2399,68,65,53,71,75,76,13,24,25,78,80,5,6,7,8,9,14,15,16,17,18,19,20,21,22,23,26,27,28,29,30,31,32,33,34,35,77,94,10,11,12,81,104,90,143,144,87,88,4,91,84,70,2,72,83,86,96,82,89,99,98,74,97,45,42,48,51,50,37,36,3,41,47,38,1720,69,106,95,105])).
% 78.03/78.12 cnf(2453,plain,
% 78.03/78.12 (P6(f18(f7(f23(x24531,a1,x24532))),f17(f18(a2),x24533))),
% 78.03/78.12 inference(scs_inference,[],[1758,75])).
% 78.03/78.12 cnf(2455,plain,
% 78.03/78.12 (P4(f6(x24551,f5(f21(f23(x24552,a1,x24553),x24554),x24555)),f23(x24552,a1,a3))),
% 78.03/78.12 inference(scs_inference,[],[2361,1758,75,78])).
% 78.03/78.12 cnf(2461,plain,
% 78.03/78.12 (E(f7(f23(x24611,f6(x24612,f5(x24613,x24614)),x24615)),f18(x24611))),
% 78.03/78.12 inference(scs_inference,[],[2361,1758,2408,136,75,78,91,77,81])).
% 78.03/78.12 cnf(2463,plain,
% 78.03/78.12 (E(f6(f4(x24631,f4(a1,x24632)),f5(x24633,a1)),f4(f6(x24631,f5(x24633,a1)),f4(a1,x24632)))),
% 78.03/78.12 inference(scs_inference,[],[2361,1758,2408,543,136,75,78,91,77,81,87])).
% 78.03/78.12 cnf(2468,plain,
% 78.03/78.12 (P6(f18(f7(f23(x24681,a1,x24682))),f8(f18(a2)))),
% 78.03/78.12 inference(scs_inference,[],[2361,2381,1758,2408,543,136,75,78,91,77,81,87,25,94,71])).
% 78.03/78.12 cnf(2471,plain,
% 78.03/78.12 (P6(f18(f7(f23(x24711,a1,x24712))),f21(f18(a2),x24713))),
% 78.03/78.12 inference(scs_inference,[],[2361,2381,1758,2408,543,136,75,78,91,77,81,87,25,94,71,20,76])).
% 78.03/78.12 cnf(2479,plain,
% 78.03/78.12 (E(f13(x24791,f21(f23(x24792,a1,x24793),x24794)),f13(x24791,f23(x24792,a1,a3)))),
% 78.03/78.12 inference(scs_inference,[],[2361,2381,1758,2408,743,543,136,75,78,91,77,81,87,25,94,71,20,76,19,27,84,9,30,23])).
% 78.03/78.12 cnf(2480,plain,
% 78.03/78.12 (E(f23(x24801,f21(f23(x24802,a1,x24803),x24804),x24805),f23(x24801,f23(x24802,a1,a3),x24805))),
% 78.03/78.12 inference(scs_inference,[],[2361,2381,1758,2408,743,543,136,75,78,91,77,81,87,25,94,71,20,76,19,27,84,9,30,23,11])).
% 78.03/78.12 cnf(2481,plain,
% 78.03/78.12 (E(f19(x24811,f21(f23(x24812,a1,x24813),x24814)),f19(x24811,f23(x24812,a1,a3)))),
% 78.03/78.12 inference(scs_inference,[],[2361,2381,1758,2408,743,543,136,75,78,91,77,81,87,25,94,71,20,76,19,27,84,9,30,23,11,17])).
% 78.03/78.12 cnf(2482,plain,
% 78.03/78.12 (E(f20(x24821,f21(f23(x24822,a1,x24823),x24824)),f20(x24821,f23(x24822,a1,a3)))),
% 78.03/78.12 inference(scs_inference,[],[2361,2381,1758,2408,743,543,136,75,78,91,77,81,87,25,94,71,20,76,19,27,84,9,30,23,11,17,15])).
% 78.03/78.12 cnf(2484,plain,
% 78.03/78.12 (~P3(f23(x24841,f6(x24842,f5(f10(a14,x24843),f13(a14,x24843))),x24844))),
% 78.03/78.12 inference(scs_inference,[],[2361,2381,1758,2408,743,543,136,624,75,78,91,77,81,87,25,94,71,20,76,19,27,84,9,30,23,11,17,15,22,104])).
% 78.03/78.12 cnf(2486,plain,
% 78.03/78.12 (P4(f6(f6(x24861,f5(a2,x24862)),f5(x24863,x24864)),f7(f23(x24865,a1,x24866)))),
% 78.03/78.12 inference(scs_inference,[],[2361,2381,1758,2408,743,543,136,624,75,78,91,77,81,87,25,94,71,20,76,19,27,84,9,30,23,11,17,15,22,104,80])).
% 78.03/78.12 cnf(2490,plain,
% 78.03/78.12 (E(f23(f21(f23(x24901,a1,x24902),x24903),x24904,x24905),f23(f23(x24901,a1,a3),x24904,x24905))),
% 78.03/78.12 inference(scs_inference,[],[2361,2381,1758,2408,743,543,136,624,75,78,91,77,81,87,25,94,71,20,76,19,27,84,9,30,23,11,17,15,22,104,80,21,8,10])).
% 78.03/78.12 cnf(2497,plain,
% 78.03/78.12 (E(f4(x24971,f21(f23(x24972,a1,x24973),x24974)),f4(x24971,f23(x24972,a1,a3)))),
% 78.03/78.12 inference(scs_inference,[],[2361,2381,1758,2408,743,543,136,624,75,78,91,77,81,87,25,94,71,20,76,19,27,84,9,30,23,11,17,15,22,104,80,21,8,10,31,4,12,16,32,13,5])).
% 78.03/78.12 cnf(2512,plain,
% 78.03/78.12 (~P1(f13(f6(a14,f5(x25121,a2)),x25122),f10(f6(a14,f5(x25121,a2)),x25122))),
% 78.03/78.12 inference(scs_inference,[],[2361,2381,1758,888,2408,2383,743,543,136,624,75,78,91,77,81,87,25,94,71,20,76,19,27,84,9,30,23,11,17,15,22,104,80,21,8,10,31,4,12,16,32,13,5,7,35,6,29,33,14,24,18,34,28,26,70,2,72])).
% 78.03/78.12 cnf(2516,plain,
% 78.03/78.12 (~P3(f23(x25161,f6(a14,f5(x25162,x25163)),x25164))),
% 78.03/78.12 inference(scs_inference,[],[2376,2361,2381,1758,2395,888,2408,2383,2379,2352,743,543,136,624,75,78,91,77,81,87,25,94,71,20,76,19,27,84,9,30,23,11,17,15,22,104,80,21,8,10,31,4,12,16,32,13,5,7,35,6,29,33,14,24,18,34,28,26,70,2,72,106,99])).
% 78.03/78.12 cnf(2517,plain,
% 78.03/78.12 (P7(f6(a14,f5(x25171,x25172)),f19(f6(x25173,f5(x25174,f12(x25175,a14))),x25174),f11(x25175,a14))),
% 78.03/78.12 inference(rename_variables,[],[2352])).
% 78.03/78.12 cnf(2519,plain,
% 78.03/78.12 (P9(f10(f6(a14,f5(x25191,x25192)),x25193),f13(f6(a14,f5(x25191,x25192)),x25193))),
% 78.03/78.12 inference(scs_inference,[],[2376,2361,2381,1758,2395,888,2408,2383,2379,2352,2517,743,2266,543,136,624,75,78,91,77,81,87,25,94,71,20,76,19,27,84,9,30,23,11,17,15,22,104,80,21,8,10,31,4,12,16,32,13,5,7,35,6,29,33,14,24,18,34,28,26,70,2,72,106,99,86])).
% 78.03/78.12 cnf(2522,plain,
% 78.03/78.12 (E(f19(f6(f6(x25221,f5(a14,x25222)),f5(a1,x25223)),a14),f19(f6(x25221,f5(a14,x25222)),a14))),
% 78.03/78.12 inference(scs_inference,[],[2376,2361,2381,1758,2395,888,2408,2383,2379,2352,2517,743,2266,659,543,136,624,107,75,78,91,77,81,87,25,94,71,20,76,19,27,84,9,30,23,11,17,15,22,104,80,21,8,10,31,4,12,16,32,13,5,7,35,6,29,33,14,24,18,34,28,26,70,2,72,106,99,86,82])).
% 78.03/78.12 cnf(2527,plain,
% 78.03/78.12 (P3(f23(x25271,f6(a1,f5(f13(a14,x25272),f10(a14,x25272))),x25273))),
% 78.03/78.12 inference(scs_inference,[],[2376,2361,2381,1758,2395,888,2408,2383,2379,2352,2517,743,2266,659,543,136,624,60,107,75,78,91,77,81,87,25,94,71,20,76,19,27,84,9,30,23,11,17,15,22,104,80,21,8,10,31,4,12,16,32,13,5,7,35,6,29,33,14,24,18,34,28,26,70,2,72,106,99,86,82,83,105])).
% 78.03/78.12 cnf(2529,plain,
% 78.03/78.12 (~P4(f20(f6(f4(a1,x25291),f5(a2,x25292)),f7(f23(x25293,a1,x25294))),x25295)),
% 78.03/78.12 inference(scs_inference,[],[2376,2361,2381,1758,2395,888,2408,2383,2379,2352,2517,743,2266,1896,659,543,136,624,60,107,65,75,78,91,77,81,87,25,94,71,20,76,19,27,84,9,30,23,11,17,15,22,104,80,21,8,10,31,4,12,16,32,13,5,7,35,6,29,33,14,24,18,34,28,26,70,2,72,106,99,86,82,83,105,45])).
% 78.03/78.12 cnf(2532,plain,
% 78.03/78.12 (~P5(f21(f23(x25321,a1,x25322),x25323),x25324)),
% 78.03/78.12 inference(scs_inference,[],[2372,2376,2361,2381,1758,2395,888,2408,2383,2379,2352,2517,1867,743,2266,1896,659,543,136,624,60,66,107,65,75,78,91,77,81,87,25,94,71,20,76,19,27,84,9,30,23,11,17,15,22,104,80,21,8,10,31,4,12,16,32,13,5,7,35,6,29,33,14,24,18,34,28,26,70,2,72,106,99,86,82,83,105,45,42,48])).
% 78.03/78.12 cnf(2533,plain,
% 78.03/78.12 (E(f21(f23(x25331,a1,x25332),x25333),f23(x25331,a1,a3))),
% 78.03/78.12 inference(rename_variables,[],[2361])).
% 78.03/78.12 cnf(2536,plain,
% 78.03/78.12 (~P9(f11(x25361,a14),f12(x25361,a14))),
% 78.03/78.12 inference(rename_variables,[],[622])).
% 78.03/78.12 cnf(2537,plain,
% 78.03/78.12 (E(f12(f19(f6(x25371,f5(a2,x25372)),f7(f23(x25373,a1,x25374))),x25375),f12(x25372,x25375))),
% 78.03/78.12 inference(rename_variables,[],[2344])).
% 78.03/78.12 cnf(2544,plain,
% 78.03/78.12 (~P1(f11(x25441,a14),f12(f19(f6(x25442,f5(a2,x25441)),f7(f23(x25443,a1,x25444))),a14))),
% 78.03/78.12 inference(scs_inference,[],[2372,622,2536,2376,2361,2381,1758,2395,888,2408,2383,2398,2379,2344,2537,2346,2352,2517,1867,743,2266,1896,659,543,136,1697,624,60,616,66,107,65,75,78,91,77,81,87,25,94,71,20,76,19,27,84,9,30,23,11,17,15,22,104,80,21,8,10,31,4,12,16,32,13,5,7,35,6,29,33,14,24,18,34,28,26,70,2,72,106,99,86,82,83,105,45,42,48,51,43,50,37])).
% 78.03/78.12 cnf(2547,plain,
% 78.03/78.12 (P1(f23(x25471,a1,a3),f21(f23(x25471,a1,x25472),x25473))),
% 78.03/78.12 inference(scs_inference,[],[2372,622,2536,2376,2361,2533,2381,1758,2395,888,2408,2383,2398,2379,2344,2537,2346,2352,2517,1867,743,2266,1896,659,543,136,1697,624,60,616,66,107,65,54,75,78,91,77,81,87,25,94,71,20,76,19,27,84,9,30,23,11,17,15,22,104,80,21,8,10,31,4,12,16,32,13,5,7,35,6,29,33,14,24,18,34,28,26,70,2,72,106,99,86,82,83,105,45,42,48,51,43,50,37,36])).
% 78.03/78.12 cnf(2554,plain,
% 78.03/78.12 (P1(f12(f19(f6(x25541,f5(a2,x25542)),f7(f23(x25543,a1,x25544))),a14),f11(x25542,a14))),
% 78.03/78.12 inference(scs_inference,[],[62,2372,622,2536,2376,2361,2533,2381,1758,2395,888,2408,2383,2398,2379,2344,2537,2346,2352,2517,1867,743,153,2266,1896,659,543,136,2108,1697,624,60,616,66,68,107,65,54,75,78,91,77,81,87,25,94,71,20,76,19,27,84,9,30,23,11,17,15,22,104,80,21,8,10,31,4,12,16,32,13,5,7,35,6,29,33,14,24,18,34,28,26,70,2,72,106,99,86,82,83,105,45,42,48,51,43,50,37,36,3,47,38,69])).
% 78.03/78.12 cnf(2561,plain,
% 78.03/78.12 (E(f6(f4(x25611,a2),f5(x25612,x25613)),f4(f6(x25611,f5(x25612,x25613)),a2))),
% 78.03/78.12 inference(scs_inference,[],[1387,53,78,87])).
% 78.03/78.12 cnf(2570,plain,
% 78.03/78.12 (P4(f6(f6(f6(x25701,f5(a2,x25702)),f5(x25703,x25704)),f5(x25705,x25706)),f7(f23(x25707,a1,x25708)))),
% 78.03/78.12 inference(scs_inference,[],[2486,2174,2529,2357,1883,1387,53,78,87,75,91,77,25,80])).
% 78.03/78.12 cnf(2576,plain,
% 78.03/78.12 (E(f7(f23(x25761,a14,x25762)),f18(x25761))),
% 78.03/78.12 inference(scs_inference,[],[2486,2174,2529,2357,1883,1387,129,53,78,87,75,91,77,25,80,71,76,81])).
% 78.03/78.12 cnf(2580,plain,
% 78.03/78.12 (P7(f6(f4(f4(a14,x25801),x25802),f5(x25803,x25804)),f10(f4(a14,x25801),x25802),f13(f4(a14,x25801),x25802))),
% 78.03/78.12 inference(scs_inference,[],[2386,2486,2174,2529,2357,1883,1387,129,53,78,87,75,91,77,25,80,71,76,81,27,15,94])).
% 78.03/78.12 cnf(2588,plain,
% 78.03/78.12 (E(f13(x25881,f7(f23(x25882,f4(a14,x25883),x25884))),f13(x25881,f18(x25882)))),
% 78.03/78.12 inference(scs_inference,[],[2386,2486,2174,2529,2357,1883,1387,129,53,78,87,75,91,77,25,80,71,76,81,27,15,94,17,84,19,8,9,23])).
% 78.03/78.12 cnf(2592,plain,
% 78.03/78.12 (E(f12(f7(f23(x25921,f4(a14,x25922),x25923)),x25924),f12(f18(x25921),x25924))),
% 78.03/78.12 inference(scs_inference,[],[2386,2486,2174,2529,2357,1883,1387,129,53,78,87,75,91,77,25,80,71,76,81,27,15,94,17,84,19,8,9,23,22,20,4,30])).
% 78.03/78.12 cnf(2616,plain,
% 78.03/78.12 (~P1(f13(f6(a14,f5(x26161,x26162)),x26163),f10(f6(a14,f5(x26161,x26162)),x26163))),
% 78.03/78.12 inference(scs_inference,[],[2386,2486,2174,2529,2432,2519,2357,1883,1387,129,53,78,87,75,91,77,25,80,71,76,81,27,15,94,17,84,19,8,9,23,22,20,4,30,7,29,34,12,18,11,6,14,31,35,28,16,21,33,10,26,5,32,13,24,70,2,72])).
% 78.03/78.12 cnf(2620,plain,
% 78.03/78.12 (P3(f23(x26201,f6(f6(a1,f5(f13(a14,x26202),f10(a14,x26202))),f5(x26203,a2)),x26204))),
% 78.03/78.12 inference(scs_inference,[],[2386,2486,2516,2174,2529,2432,2519,2527,2357,1883,1387,519,129,53,78,87,75,91,77,25,80,71,76,81,27,15,94,17,84,19,8,9,23,22,20,4,30,7,29,34,12,18,11,6,14,31,35,28,16,21,33,10,26,5,32,13,24,70,2,72,106,105])).
% 78.03/78.12 cnf(2622,plain,
% 78.03/78.12 (P7(f6(x26221,f5(a1,a1)),f4(a1,x26222),f4(a1,x26222))),
% 78.03/78.12 inference(scs_inference,[],[2386,2486,2516,2174,2529,2432,2519,2527,2357,1883,1387,519,129,116,53,78,87,75,91,77,25,80,71,76,81,27,15,94,17,84,19,8,9,23,22,20,4,30,7,29,34,12,18,11,6,14,31,35,28,16,21,33,10,26,5,32,13,24,70,2,72,106,105,83])).
% 78.03/78.12 cnf(2627,plain,
% 78.03/78.12 (P7(f4(f4(a14,x26271),f23(x26272,a1,a3)),f10(f4(a14,x26271),f21(f23(x26272,a1,x26273),x26274)),f13(f4(a14,x26271),f21(f23(x26272,a1,x26273),x26274)))),
% 78.03/78.12 inference(scs_inference,[],[2386,2486,2516,2174,2482,2497,2529,2432,2519,2527,2357,1883,1387,2259,519,129,116,53,78,87,75,91,77,25,80,71,76,81,27,15,94,17,84,19,8,9,23,22,20,4,30,7,29,34,12,18,11,6,14,31,35,28,16,21,33,10,26,5,32,13,24,70,2,72,106,105,83,45,42])).
% 78.03/78.12 cnf(2629,plain,
% 78.03/78.12 (P7(f4(f4(a14,x26291),x26292),f10(f4(a14,x26291),x26292),f13(f4(a14,x26291),x26292))),
% 78.03/78.12 inference(rename_variables,[],[2386])).
% 78.03/78.12 cnf(2631,plain,
% 78.03/78.12 (E(f23(x26311,f21(f23(x26312,a1,x26313),x26314),x26315),f23(x26311,f23(x26312,a1,a3),x26315))),
% 78.03/78.12 inference(rename_variables,[],[2480])).
% 78.03/78.12 cnf(2632,plain,
% 78.03/78.12 (~P9(f23(f7(f23(x26321,a1,x26322)),x26323,x26324),f23(a2,x26323,x26324))),
% 78.03/78.12 inference(rename_variables,[],[1345])).
% 78.03/78.12 cnf(2633,plain,
% 78.03/78.12 (~P9(f23(f7(f23(x26331,a1,x26332)),f21(f23(x26333,a1,x26334),x26335),x26336),f23(a2,f23(x26333,a1,a3),x26336))),
% 78.03/78.12 inference(scs_inference,[],[1345,2632,2386,2486,2516,2174,2480,2631,2482,2497,2529,2432,2519,2527,2357,1883,1387,2259,519,129,116,53,78,87,75,91,77,25,80,71,76,81,27,15,94,17,84,19,8,9,23,22,20,4,30,7,29,34,12,18,11,6,14,31,35,28,16,21,33,10,26,5,32,13,24,70,2,72,106,105,83,45,42,51,50])).
% 78.03/78.12 cnf(2634,plain,
% 78.03/78.12 (E(f23(x26341,f21(f23(x26342,a1,x26343),x26344),x26345),f23(x26341,f23(x26342,a1,a3),x26345))),
% 78.03/78.12 inference(rename_variables,[],[2480])).
% 78.03/78.12 cnf(2636,plain,
% 78.03/78.12 (P9(f12(f19(f6(x26361,f5(a2,x26362)),f7(f23(x26363,a1,x26364))),a14),f11(x26362,a14))),
% 78.03/78.12 inference(scs_inference,[],[1345,2632,2386,2486,2516,2174,2480,2631,2482,2497,2529,2432,2519,2527,2554,2544,2357,1883,1387,2259,519,129,116,53,78,87,75,91,77,25,80,71,76,81,27,15,94,17,84,19,8,9,23,22,20,4,30,7,29,34,12,18,11,6,14,31,35,28,16,21,33,10,26,5,32,13,24,70,2,72,106,105,83,45,42,51,50,73])).
% 78.03/78.12 cnf(2639,plain,
% 78.03/78.12 (P1(f23(x26391,f21(f23(x26392,a1,x26393),x26394),f7(f23(x26395,a1,x26396))),f23(x26391,f23(x26392,a1,a3),a2))),
% 78.03/78.12 inference(scs_inference,[],[1345,2632,2386,2486,2516,2174,2480,2631,2634,2482,2497,2529,2432,2519,2527,2554,2544,2357,1883,1464,1387,2259,519,129,116,53,78,87,75,91,77,25,80,71,76,81,27,15,94,17,84,19,8,9,23,22,20,4,30,7,29,34,12,18,11,6,14,31,35,28,16,21,33,10,26,5,32,13,24,70,2,72,106,105,83,45,42,51,50,73,37])).
% 78.03/78.12 cnf(2640,plain,
% 78.03/78.12 (E(f23(x26401,f21(f23(x26402,a1,x26403),x26404),x26405),f23(x26401,f23(x26402,a1,a3),x26405))),
% 78.03/78.12 inference(rename_variables,[],[2480])).
% 78.03/78.12 cnf(2642,plain,
% 78.03/78.12 (~P1(f13(f6(a14,f5(x26421,a2)),f21(f23(x26422,a1,x26423),x26424)),f10(f6(a14,f5(x26421,a2)),f23(x26422,a1,a3)))),
% 78.03/78.12 inference(scs_inference,[],[1345,2632,2386,2486,2516,2174,2480,2631,2634,2479,2482,2497,2529,2432,2519,2512,2527,2554,2544,2357,1883,1464,1387,2259,519,129,116,53,78,87,75,91,77,25,80,71,76,81,27,15,94,17,84,19,8,9,23,22,20,4,30,7,29,34,12,18,11,6,14,31,35,28,16,21,33,10,26,5,32,13,24,70,2,72,106,105,83,45,42,51,50,73,37,36])).
% 78.03/78.12 cnf(2645,plain,
% 78.03/78.12 (E(f23(f21(f23(x26451,a1,x26452),x26453),f21(f23(x26454,a1,x26455),x26456),x26457),f23(f23(x26451,a1,a3),f23(x26454,a1,a3),x26457))),
% 78.03/78.12 inference(scs_inference,[],[1345,2632,2386,2486,2516,2174,2480,2631,2634,2640,2490,2479,2482,2497,2529,2432,2519,2512,2527,2554,2544,2357,1883,1464,1387,2259,519,129,116,53,78,87,75,91,77,25,80,71,76,81,27,15,94,17,84,19,8,9,23,22,20,4,30,7,29,34,12,18,11,6,14,31,35,28,16,21,33,10,26,5,32,13,24,70,2,72,106,105,83,45,42,51,50,73,37,36,3])).
% 78.03/78.12 cnf(2648,plain,
% 78.03/78.12 (~E(f8(f23(a9,a14,a15)),f23(x26481,f6(a14,f5(x26482,x26483)),x26484))),
% 78.03/78.12 inference(scs_inference,[],[62,1345,2632,2386,2486,2516,2174,2480,2631,2634,2640,2490,2479,2482,2497,2529,2432,2519,2512,2527,2554,2544,2357,1883,1464,1387,2259,519,129,116,53,78,87,75,91,77,25,80,71,76,81,27,15,94,17,84,19,8,9,23,22,20,4,30,7,29,34,12,18,11,6,14,31,35,28,16,21,33,10,26,5,32,13,24,70,2,72,106,105,83,45,42,51,50,73,37,36,3,38])).
% 78.03/78.12 cnf(2649,plain,
% 78.03/78.12 (P1(f10(f6(a14,f5(x26491,a2)),f23(x26492,a1,a3)),f13(f6(a14,f5(x26491,a2)),f21(f23(x26492,a1,x26493),x26494)))),
% 78.03/78.12 inference(scs_inference,[],[62,1345,2632,2386,2486,2516,2174,2480,2631,2634,2640,2490,2479,2482,2497,2529,2432,2519,2512,2527,2554,2544,2357,1883,1464,1387,2259,519,129,116,53,78,87,75,91,77,25,80,71,76,81,27,15,94,17,84,19,8,9,23,22,20,4,30,7,29,34,12,18,11,6,14,31,35,28,16,21,33,10,26,5,32,13,24,70,2,72,106,105,83,45,42,51,50,73,37,36,3,38,69])).
% 78.03/78.12 cnf(2651,plain,
% 78.03/78.12 (~P9(f10(f4(a14,x26511),x26512),f13(f4(a14,x26511),x26512))+P9(f10(f4(f4(a14,x26511),x26512),x26513),f13(f4(f4(a14,x26511),x26512),x26513))),
% 78.03/78.12 inference(scs_inference,[],[62,1345,2632,2386,2629,2486,2516,2174,2480,2631,2634,2640,2490,2479,2482,2497,2529,2432,2519,2512,2527,2554,2544,2357,1883,1464,1387,2259,519,129,116,53,78,87,75,91,77,25,80,71,76,81,27,15,94,17,84,19,8,9,23,22,20,4,30,7,29,34,12,18,11,6,14,31,35,28,16,21,33,10,26,5,32,13,24,70,2,72,106,105,83,45,42,51,50,73,37,36,3,38,69,86])).
% 78.03/78.12 cnf(2656,plain,
% 78.03/78.12 (P4(f6(x26561,f5(f7(f23(x26562,a14,x26563)),x26564)),f18(x26562))),
% 78.03/78.12 inference(scs_inference,[],[2576,78])).
% 78.03/78.12 cnf(2664,plain,
% 78.03/78.12 (P4(f6(f6(f6(f6(x26641,f5(a2,x26642)),f5(x26643,x26644)),f5(x26645,x26646)),f5(x26647,x26648)),f7(f23(x26649,a1,x266410)))),
% 78.03/78.12 inference(scs_inference,[],[2576,1756,2570,1935,54,78,87,75,77,80])).
% 78.03/78.12 cnf(2668,plain,
% 78.03/78.12 (E(f10(x26681,f7(f23(x26682,a14,x26683))),f10(x26681,f18(x26682)))),
% 78.03/78.12 inference(scs_inference,[],[2576,1756,2570,1935,54,78,87,75,77,80,76,27])).
% 78.03/78.12 cnf(2669,plain,
% 78.03/78.12 (E(f20(x26691,f7(f23(x26692,a14,x26693))),f20(x26691,f18(x26692)))),
% 78.03/78.12 inference(scs_inference,[],[2576,1756,2570,1935,54,78,87,75,77,80,76,27,15])).
% 78.03/78.12 cnf(2675,plain,
% 78.03/78.12 (P7(f6(f6(x26751,f5(a1,a1)),f5(x26752,x26753)),f4(a1,x26754),f4(a1,x26754))),
% 78.03/78.12 inference(scs_inference,[],[2576,2622,1756,2570,1935,54,78,87,75,77,80,76,27,15,25,71,84,94])).
% 78.03/78.12 cnf(2677,plain,
% 78.03/78.12 (E(f19(x26771,f7(f23(x26772,a14,x26773))),f19(x26771,f18(x26772)))),
% 78.03/78.12 inference(scs_inference,[],[2576,2622,1756,2570,1935,54,78,87,75,77,80,76,27,15,25,71,84,94,17])).
% 78.03/78.12 cnf(2682,plain,
% 78.03/78.12 (E(f13(x26821,f7(f23(x26822,a14,x26823))),f13(x26821,f18(x26822)))),
% 78.03/78.12 inference(scs_inference,[],[2576,2622,1756,2570,1935,54,78,87,75,77,80,76,27,15,25,71,84,94,17,8,30,19,22,23])).
% 78.03/78.12 cnf(2683,plain,
% 78.03/78.12 (E(f17(x26831,f7(f23(x26832,a14,x26833))),f17(x26831,f18(x26832)))),
% 78.03/78.12 inference(scs_inference,[],[2576,2622,1756,2570,1935,54,78,87,75,77,80,76,27,15,25,71,84,94,17,8,30,19,22,23,29])).
% 78.03/78.12 cnf(2687,plain,
% 78.03/78.12 (E(f23(x26871,x26872,f7(f23(x26873,a14,x26874))),f23(x26871,x26872,f18(x26873)))),
% 78.03/78.12 inference(scs_inference,[],[2576,2622,1756,2570,1935,54,78,87,75,77,80,76,27,15,25,71,84,94,17,8,30,19,22,23,29,18,4,9,12])).
% 78.03/78.12 cnf(2689,plain,
% 78.03/78.12 (E(f23(x26891,f7(f23(x26892,a14,x26893)),x26894),f23(x26891,f18(x26892),x26894))),
% 78.03/78.12 inference(scs_inference,[],[2576,2622,1756,2570,1935,54,78,87,75,77,80,76,27,15,25,71,84,94,17,8,30,19,22,23,29,18,4,9,12,20,11])).
% 78.03/78.12 cnf(2700,plain,
% 78.03/78.12 (E(f23(f7(f23(x27001,a14,x27002)),x27003,x27004),f23(f18(x27001),x27003,x27004))),
% 78.03/78.12 inference(scs_inference,[],[2576,2622,1756,2570,1935,54,78,87,75,77,80,76,27,15,25,71,84,94,17,8,30,19,22,23,29,18,4,9,12,20,11,28,6,31,35,32,7,24,21,26,34,10])).
% 78.03/78.12 cnf(2705,plain,
% 78.03/78.12 (E(f4(x27051,f7(f23(x27052,a14,x27053))),f4(x27051,f18(x27052)))),
% 78.03/78.12 inference(scs_inference,[],[2576,2622,1756,2570,1935,54,78,87,75,77,80,76,27,15,25,71,84,94,17,8,30,19,22,23,29,18,4,9,12,20,11,28,6,31,35,32,7,24,21,26,34,10,16,33,13,14,5])).
% 78.03/78.12 cnf(2729,plain,
% 78.03/78.12 (P1(f18(x27291),f7(f23(x27291,a14,x27292)))),
% 78.03/78.12 inference(scs_inference,[],[557,2576,2622,2547,1544,1756,2570,2648,2645,2455,2405,2592,2231,2522,2463,1935,1858,1867,60,616,54,78,87,75,77,80,76,27,15,25,71,84,94,17,8,30,19,22,23,29,18,4,9,12,20,11,28,6,31,35,32,7,24,21,26,34,10,16,33,13,14,5,2,72,105,83,45,44,51,50,73,37,36])).
% 78.03/78.12 cnf(2738,plain,
% 78.03/78.12 (P1(f13(f4(a14,x27381),x27382),f10(f4(a14,x27381),x27382))+~P3(f17(f23(x27383,f4(f4(a14,x27381),x27382),a2),x27384))),
% 78.03/78.12 inference(scs_inference,[],[62,557,2576,2622,2547,1544,1756,2580,2570,2648,2561,2645,1726,2455,2436,2405,2592,2231,2522,2463,1935,1858,1867,60,616,54,78,87,75,77,80,76,27,15,25,71,84,94,17,8,30,19,22,23,29,18,4,9,12,20,11,28,6,31,35,32,7,24,21,26,34,10,16,33,13,14,5,2,72,105,83,45,44,51,50,73,37,36,3,38,69,99,1104])).
% 78.03/78.12 cnf(2743,plain,
% 78.03/78.12 (P4(f6(f6(f6(f6(f6(x27431,f5(a2,x27432)),f5(x27433,x27434)),f5(x27435,x27436)),f5(x27437,x27438)),f5(x27439,x274310)),f7(f23(x274311,a1,x274312)))),
% 78.03/78.12 inference(scs_inference,[],[2664,1098,78,80])).
% 78.03/78.12 cnf(2745,plain,
% 78.03/78.12 (P6(f19(f7(f23(x27451,a1,x27452)),f7(f23(x27453,a1,x27454))),f17(f19(a2,a2),x27455))),
% 78.03/78.12 inference(scs_inference,[],[2154,2664,1098,78,80,75])).
% 78.03/78.12 cnf(2751,plain,
% 78.03/78.12 (E(f10(x27511,f20(f6(x27512,f5(a2,x27513)),f7(f23(x27514,a1,x27515)))),f10(x27511,x27512))),
% 78.03/78.12 inference(scs_inference,[],[2154,2664,1920,1098,1867,78,80,75,77,76,27])).
% 78.03/78.12 cnf(2752,plain,
% 78.03/78.12 (P7(f6(f6(f6(x27521,f5(a1,a1)),f5(x27522,x27523)),f5(x27524,x27525)),f4(a1,x27526),f4(a1,x27526))),
% 78.03/78.12 inference(scs_inference,[],[2675,2154,2664,1920,1098,1867,78,80,75,77,76,27,94])).
% 78.03/78.12 cnf(2758,plain,
% 78.03/78.12 (E(f8(f20(f6(x27581,f5(a2,x27582)),f7(f23(x27583,a1,x27584)))),f8(x27581))),
% 78.03/78.12 inference(scs_inference,[],[2675,2154,2664,1920,1098,1867,78,80,75,77,76,27,94,84,71,25])).
% 78.03/78.12 cnf(2763,plain,
% 78.03/78.12 (E(f21(f20(f6(x27631,f5(a2,x27632)),f7(f23(x27633,a1,x27634))),x27635),f21(x27631,x27635))),
% 78.03/78.12 inference(scs_inference,[],[2675,2154,2664,1920,1098,1867,78,80,75,77,76,27,94,84,71,25,15,8,22,12,18])).
% 78.03/78.12 cnf(2764,plain,
% 78.03/78.12 (E(f21(x27641,f20(f6(x27642,f5(a2,x27643)),f7(f23(x27644,a1,x27645)))),f21(x27641,x27642))),
% 78.03/78.12 inference(scs_inference,[],[2675,2154,2664,1920,1098,1867,78,80,75,77,76,27,94,84,71,25,15,8,22,12,18,19])).
% 78.03/78.12 cnf(2765,plain,
% 78.03/78.12 (E(f23(x27651,f20(f6(x27652,f5(a2,x27653)),f7(f23(x27654,a1,x27655))),x27656),f23(x27651,x27652,x27656))),
% 78.03/78.12 inference(scs_inference,[],[2675,2154,2664,1920,1098,1867,78,80,75,77,76,27,94,84,71,25,15,8,22,12,18,19,11])).
% 78.03/78.12 cnf(2767,plain,
% 78.03/78.12 (E(f12(x27671,f20(f6(x27672,f5(a2,x27673)),f7(f23(x27674,a1,x27675)))),f12(x27671,x27672))),
% 78.03/78.12 inference(scs_inference,[],[2675,2154,2664,1920,1098,1867,78,80,75,77,76,27,94,84,71,25,15,8,22,12,18,19,11,17,31])).
% 78.03/78.12 cnf(2769,plain,
% 78.03/78.12 (E(f5(f20(f6(x27691,f5(a2,x27692)),f7(f23(x27693,a1,x27694))),x27695),f5(x27691,x27695))),
% 78.03/78.12 inference(scs_inference,[],[2675,2154,2664,1920,1098,1867,78,80,75,77,76,27,94,84,71,25,15,8,22,12,18,19,11,17,31,9,6])).
% 78.03/78.12 cnf(2770,plain,
% 78.03/78.12 (E(f12(f20(f6(x27701,f5(a2,x27702)),f7(f23(x27703,a1,x27704))),x27705),f12(x27701,x27705))),
% 78.03/78.12 inference(scs_inference,[],[2675,2154,2664,1920,1098,1867,78,80,75,77,76,27,94,84,71,25,15,8,22,12,18,19,11,17,31,9,6,30])).
% 78.03/78.12 cnf(2772,plain,
% 78.03/78.12 (E(f4(f20(f6(x27721,f5(a2,x27722)),f7(f23(x27723,a1,x27724))),x27725),f4(x27721,x27725))),
% 78.03/78.12 inference(scs_inference,[],[2675,2154,2664,1920,1098,1867,78,80,75,77,76,27,94,84,71,25,15,8,22,12,18,19,11,17,31,9,6,30,29,4])).
% 78.03/78.12 cnf(2773,plain,
% 78.03/78.12 (E(f16(x27731,f20(f6(x27732,f5(a2,x27733)),f7(f23(x27734,a1,x27735)))),f16(x27731,x27732))),
% 78.03/78.12 inference(scs_inference,[],[2675,2154,2664,1920,1098,1867,78,80,75,77,76,27,94,84,71,25,15,8,22,12,18,19,11,17,31,9,6,30,29,4,35])).
% 78.03/78.12 cnf(2774,plain,
% 78.03/78.12 (E(f13(x27741,f20(f6(x27742,f5(a2,x27743)),f7(f23(x27744,a1,x27745)))),f13(x27741,x27742))),
% 78.03/78.12 inference(scs_inference,[],[2675,2154,2664,1920,1098,1867,78,80,75,77,76,27,94,84,71,25,15,8,22,12,18,19,11,17,31,9,6,30,29,4,35,23])).
% 78.03/78.12 cnf(2775,plain,
% 78.03/78.12 (E(f11(f20(f6(x27751,f5(a2,x27752)),f7(f23(x27753,a1,x27754))),x27755),f11(x27751,x27755))),
% 78.03/78.12 inference(scs_inference,[],[2675,2154,2664,1920,1098,1867,78,80,75,77,76,27,94,84,71,25,15,8,22,12,18,19,11,17,31,9,6,30,29,4,35,23,32])).
% 78.03/78.12 cnf(2776,plain,
% 78.03/78.12 (E(f10(f20(f6(x27761,f5(a2,x27762)),f7(f23(x27763,a1,x27764))),x27765),f10(x27761,x27765))),
% 78.03/78.12 inference(scs_inference,[],[2675,2154,2664,1920,1098,1867,78,80,75,77,76,27,94,84,71,25,15,8,22,12,18,19,11,17,31,9,6,30,29,4,35,23,32,26])).
% 78.03/78.12 cnf(2790,plain,
% 78.03/78.12 (~P1(f11(a9,a14),f20(f6(f12(a9,a14),f5(x27901,x27902)),x27901))),
% 78.03/78.12 inference(scs_inference,[],[2675,2154,1654,2664,1920,1098,1867,201,78,80,75,77,76,27,94,84,71,25,15,8,22,12,18,19,11,17,31,9,6,30,29,4,35,23,32,26,24,20,21,28,5,10,13,7,34,33,16,14,2,72])).
% 78.03/78.12 cnf(2792,plain,
% 78.03/78.12 (P3(f23(x27921,f6(f6(f6(a1,f5(f13(a14,x27922),f10(a14,x27922))),f5(x27923,a2)),f5(x27924,a2)),x27925))),
% 78.03/78.12 inference(scs_inference,[],[2675,2154,1654,2664,2620,1920,1098,1867,201,53,78,80,75,77,76,27,94,84,71,25,15,8,22,12,18,19,11,17,31,9,6,30,29,4,35,23,32,26,24,20,21,28,5,10,13,7,34,33,16,14,2,72,105])).
% 78.03/78.12 cnf(2796,plain,
% 78.03/78.12 (~P4(f20(f6(f4(a1,x27961),f5(f18(x27962),x27963)),f7(f23(x27962,a14,x27964))),x27965)),
% 78.03/78.12 inference(scs_inference,[],[2675,2154,2669,1654,2664,2620,1920,1098,2259,1867,201,151,53,78,80,75,77,76,27,94,84,71,25,15,8,22,12,18,19,11,17,31,9,6,30,29,4,35,23,32,26,24,20,21,28,5,10,13,7,34,33,16,14,2,72,105,83,45])).
% 78.03/78.12 cnf(2799,plain,
% 78.03/78.12 (~P9(f23(x27991,f7(f23(x27992,a1,x27993)),f18(x27994)),f23(x27991,a2,f7(f23(x27994,a14,x27995))))),
% 78.03/78.12 inference(scs_inference,[],[2675,1427,2154,2687,2669,1654,2664,2620,1920,1098,2259,1867,201,151,53,78,80,75,77,76,27,94,84,71,25,15,8,22,12,18,19,11,17,31,9,6,30,29,4,35,23,32,26,24,20,21,28,5,10,13,7,34,33,16,14,2,72,105,83,45,51])).
% 78.03/78.12 cnf(2800,plain,
% 78.03/78.12 (E(f23(x28001,x28002,f7(f23(x28003,a14,x28004))),f23(x28001,x28002,f18(x28003)))),
% 78.03/78.12 inference(rename_variables,[],[2687])).
% 78.03/78.12 cnf(2801,plain,
% 78.03/78.12 (~P9(f23(x28011,f7(f23(x28012,a1,x28013)),x28014),f23(x28011,a2,x28014))),
% 78.03/78.12 inference(rename_variables,[],[1427])).
% 78.03/78.12 cnf(2802,plain,
% 78.03/78.12 (~P9(f23(x28021,f7(f23(x28022,a1,x28023)),f7(f23(x28024,a14,x28025))),f23(x28021,a2,f18(x28024)))),
% 78.03/78.12 inference(scs_inference,[],[2675,1427,2801,2154,2687,2800,2669,1654,2664,2620,1920,1098,2259,1867,201,151,53,78,80,75,77,76,27,94,84,71,25,15,8,22,12,18,19,11,17,31,9,6,30,29,4,35,23,32,26,24,20,21,28,5,10,13,7,34,33,16,14,2,72,105,83,45,51,50])).
% 78.03/78.12 cnf(2803,plain,
% 78.03/78.12 (E(f23(x28031,x28032,f7(f23(x28033,a14,x28034))),f23(x28031,x28032,f18(x28033)))),
% 78.03/78.12 inference(rename_variables,[],[2687])).
% 78.03/78.12 cnf(2814,plain,
% 78.03/78.12 (E(f23(x28141,f7(f23(x28142,a14,x28143)),f7(f23(x28144,a14,x28145))),f23(x28141,f18(x28142),f18(x28144)))),
% 78.03/78.12 inference(scs_inference,[],[2675,1427,2801,2154,2687,2800,2803,2689,2700,2669,2682,1654,2664,2639,2642,2620,2616,2649,1920,1098,2259,1867,201,151,53,78,80,75,77,76,27,94,84,71,25,15,8,22,12,18,19,11,17,31,9,6,30,29,4,35,23,32,26,24,20,21,28,5,10,13,7,34,33,16,14,2,72,105,83,45,51,50,73,37,36,3])).
% 78.03/78.12 cnf(2822,plain,
% 78.03/78.12 (P4(a14,f18(x28221))+E(f8(f23(x28221,a14,x28222)),f23(x28221,f4(a14,f18(x28221)),a3))),
% 78.03/78.12 inference(scs_inference,[],[62,2675,1427,2801,2154,2687,2800,2803,2689,2700,2669,2682,1654,2664,2639,2642,2620,2616,2649,2359,2636,1920,1098,2259,1867,201,129,151,53,78,80,75,77,76,27,94,84,71,25,15,8,22,12,18,19,11,17,31,9,6,30,29,4,35,23,32,26,24,20,21,28,5,10,13,7,34,33,16,14,2,72,105,83,45,51,50,73,37,36,3,38,69,86,95])).
% 78.03/78.12 cnf(2835,plain,
% 78.03/78.12 (P7(f6(f6(f6(f6(x28351,f5(a1,a1)),f5(x28352,x28353)),f5(x28354,x28355)),f5(x28356,x28357)),f4(a1,x28358),f4(a1,x28358))),
% 78.03/78.12 inference(scs_inference,[],[2752,2086,2656,1978,931,78,80,75,77,76,94])).
% 78.03/78.12 cnf(2857,plain,
% 78.03/78.12 (E(f12(x28571,f20(f6(f4(a1,x28572),f5(a2,x28573)),f7(f23(x28574,a1,x28575)))),f12(x28571,a1))),
% 78.03/78.12 inference(scs_inference,[],[2752,2086,2656,1978,155,931,1896,78,80,75,77,76,94,71,84,27,25,15,8,12,29,11,9,19,35,26,32,22,30,18,24,31])).
% 78.03/78.12 cnf(2874,plain,
% 78.03/78.12 (~P1(f13(a14,x28741),f10(a14,x28741))),
% 78.03/78.12 inference(scs_inference,[],[2752,2086,1658,2656,1978,155,931,1896,624,78,80,75,77,76,94,71,84,27,25,15,8,12,29,11,9,19,35,26,32,22,30,18,24,31,6,17,20,4,10,28,23,5,7,16,21,33,13,34,14,2,72])).
% 78.03/78.12 cnf(2880,plain,
% 78.03/78.12 (P3(f23(x28801,f6(a1,f5(f7(f23(x28802,a14,x28803)),f18(x28802))),x28804))),
% 78.03/78.12 inference(scs_inference,[],[2729,2752,2086,1658,2656,2298,1978,155,2194,931,1896,624,60,78,80,75,77,76,94,71,84,27,25,15,8,12,29,11,9,19,35,26,32,22,30,18,24,31,6,17,20,4,10,28,23,5,7,16,21,33,13,34,14,2,72,74,105])).
% 78.03/78.12 cnf(2882,plain,
% 78.03/78.12 (P9(f10(f4(a14,x28821),x28822),f13(f4(a14,x28821),x28822))),
% 78.03/78.12 inference(scs_inference,[],[2729,2752,2086,1658,2656,2298,1978,155,2194,931,1896,641,624,60,78,80,75,77,76,94,71,84,27,25,15,8,12,29,11,9,19,35,26,32,22,30,18,24,31,6,17,20,4,10,28,23,5,7,16,21,33,13,34,14,2,72,74,105,86])).
% 78.03/78.12 cnf(2888,plain,
% 78.03/78.12 (P7(f6(x28881,f5(f23(x28882,a1,a3),f23(x28882,a1,a3))),f8(f23(x28882,a1,x28883)),f8(f23(x28882,a1,x28883)))),
% 78.03/78.12 inference(scs_inference,[],[2729,2752,2086,1658,2656,2298,2796,1978,155,2194,931,153,1896,641,624,60,178,78,80,75,77,76,94,71,84,27,25,15,8,12,29,11,9,19,35,26,32,22,30,18,24,31,6,17,20,4,10,28,23,5,7,16,21,33,13,34,14,2,72,74,105,86,85,83])).
% 78.03/78.12 cnf(2893,plain,
% 78.03/78.12 (~P7(f20(f6(f4(a1,x28931),f5(a2,x28932)),f7(f23(x28933,a1,x28934))),x28935,x28936)),
% 78.03/78.12 inference(scs_inference,[],[2729,2752,2086,1658,2656,2298,2796,1978,155,2194,2463,931,153,1896,641,624,66,60,178,78,80,75,77,76,94,71,84,27,25,15,8,12,29,11,9,19,35,26,32,22,30,18,24,31,6,17,20,4,10,28,23,5,7,16,21,33,13,34,14,2,72,74,105,86,85,83,45,42])).
% 78.03/78.12 cnf(2895,plain,
% 78.03/78.12 (E(f8(f20(f6(x28951,f5(a2,x28952)),f7(f23(x28953,a1,x28954)))),f8(x28951))),
% 78.03/78.12 inference(rename_variables,[],[2758])).
% 78.03/78.12 cnf(2905,plain,
% 78.03/78.12 (E(f19(x29051,f7(f23(x29052,a14,x29053))),f19(x29051,f18(x29052)))),
% 78.03/78.12 inference(rename_variables,[],[2677])).
% 78.03/78.12 cnf(2908,plain,
% 78.03/78.12 (E(f19(x29081,f7(f23(x29082,a14,x29083))),f19(x29081,f18(x29082)))),
% 78.03/78.12 inference(rename_variables,[],[2677])).
% 78.03/78.12 cnf(2916,plain,
% 78.03/78.12 (P1(f10(f4(a14,x29161),x29162),f13(f4(a14,x29161),x29162))),
% 78.03/78.12 inference(scs_inference,[],[62,576,2729,571,2752,2378,2086,2668,2677,2905,2908,1658,2264,2656,2298,2796,2484,2758,2895,1485,1978,155,2052,2689,2616,2194,2463,931,153,1896,641,624,66,60,178,78,80,75,77,76,94,71,84,27,25,15,8,12,29,11,9,19,35,26,32,22,30,18,24,31,6,17,20,4,10,28,23,5,7,16,21,33,13,34,14,2,72,74,105,86,85,83,45,42,51,50,37,39,40,36,3,38,69,70])).
% 78.03/78.12 cnf(2920,plain,
% 78.03/78.12 (P9(f10(f4(f4(a14,x29201),x29202),x29203),f13(f4(f4(a14,x29201),x29202),x29203))),
% 78.03/78.12 inference(scs_inference,[],[62,576,2729,571,2752,2378,2086,2668,2677,2905,2908,1658,2802,2264,2656,2298,2796,2484,2758,2895,1485,1978,155,2052,2689,2616,2194,2463,931,153,1896,641,624,66,60,178,78,80,75,77,76,94,71,84,27,25,15,8,12,29,11,9,19,35,26,32,22,30,18,24,31,6,17,20,4,10,28,23,5,7,16,21,33,13,34,14,2,72,74,105,86,85,83,45,42,51,50,37,39,40,36,3,38,69,70,73,2651])).
% 78.03/78.12 cnf(2930,plain,
% 78.03/78.12 (P7(f6(f6(f6(f6(f6(x29301,f5(a1,a1)),f5(x29302,x29303)),f5(x29304,x29305)),f5(x29306,x29307)),f5(x29308,x29309)),f4(a1,x293010),f4(a1,x293010))),
% 78.03/78.12 inference(scs_inference,[],[2835,2743,1526,1816,78,77,80,94])).
% 78.03/78.12 cnf(2943,plain,
% 78.03/78.12 (E(f6(x29431,x29432),f6(f20(f6(x29431,f5(a2,x29433)),f7(f23(x29434,a1,x29435))),x29432))),
% 78.03/78.12 inference(scs_inference,[],[2835,2314,2743,1526,2075,1816,1831,78,77,80,94,76,75,71,84,15,25,27,8])).
% 78.03/78.12 cnf(2953,plain,
% 78.03/78.12 (E(f21(x29531,x29532),f21(f20(f6(x29531,f5(a2,x29533)),f7(f23(x29534,a1,x29535))),x29532))),
% 78.03/78.12 inference(scs_inference,[],[2835,2314,2743,2920,1526,2075,1816,1831,78,77,80,94,76,75,71,84,15,25,27,8,70,12,32,26,29,6,11,30,18])).
% 78.03/78.12 cnf(2956,plain,
% 78.03/78.12 (E(f12(x29561,x29562),f12(x29561,f20(f6(x29562,f5(a2,x29563)),f7(f23(x29564,a1,x29565)))))),
% 78.03/78.12 inference(scs_inference,[],[2835,2314,2743,2920,1526,2075,1816,1831,78,77,80,94,76,75,71,84,15,25,27,8,70,12,32,26,29,6,11,30,18,17,19,31])).
% 78.03/78.12 cnf(2971,plain,
% 78.03/78.12 (E(f11(x29711,x29712),f11(x29711,f20(f6(x29712,f5(a2,x29713)),f7(f23(x29714,a1,x29715)))))),
% 78.03/78.12 inference(scs_inference,[],[2835,2314,2743,2920,1526,2075,1816,1831,78,77,80,94,76,75,71,84,15,25,27,8,70,12,32,26,29,6,11,30,18,17,19,31,22,23,9,10,24,35,16,13,20,28,21,7,4,5,33])).
% 78.03/78.12 cnf(2975,plain,
% 78.03/78.12 (~P1(f13(f4(a14,x29751),x29752),f10(f4(a14,x29751),x29752))),
% 78.03/78.12 inference(scs_inference,[],[2882,2835,2314,1661,2743,2920,1526,2075,1816,1831,78,77,80,94,76,75,71,84,15,25,27,8,70,12,32,26,29,6,11,30,18,17,19,31,22,23,9,10,24,35,16,13,20,28,21,7,4,5,33,34,14,2,72])).
% 78.03/78.12 cnf(2977,plain,
% 78.03/78.12 (~P7(f6(f20(f6(f4(a1,x29771),f5(a2,x29772)),f7(f23(x29773,a1,x29774))),f5(f10(a14,x29775),x29776)),f13(a14,x29775),x29777)),
% 78.03/78.12 inference(scs_inference,[],[2882,2835,2314,2893,1661,2743,2920,1526,625,2075,1816,1831,78,77,80,94,76,75,71,84,15,25,27,8,70,12,32,26,29,6,11,30,18,17,19,31,22,23,9,10,24,35,16,13,20,28,21,7,4,5,33,34,14,2,72,98])).
% 78.03/78.12 cnf(2978,plain,
% 78.03/78.12 (~P7(f20(f6(f4(a1,x29781),f5(a2,x29782)),f7(f23(x29783,a1,x29784))),x29785,x29786)),
% 78.03/78.12 inference(rename_variables,[],[2893])).
% 78.03/78.12 cnf(2980,plain,
% 78.03/78.12 (~P3(f23(x29801,f4(f4(a14,x29802),f23(x29803,a1,a3)),x29804))),
% 78.03/78.12 inference(scs_inference,[],[2882,2835,2314,2893,1661,2743,2920,2627,1526,625,2075,1816,1831,78,77,80,94,76,75,71,84,15,25,27,8,70,12,32,26,29,6,11,30,18,17,19,31,22,23,9,10,24,35,16,13,20,28,21,7,4,5,33,34,14,2,72,98,99])).
% 78.03/78.12 cnf(2985,plain,
% 78.03/78.12 (P3(f23(x29851,f6(f6(a1,f5(f4(a1,x29852),f4(a1,x29853))),f5(x29854,a2)),x29855))),
% 78.03/78.12 inference(scs_inference,[],[2882,2835,2314,2893,2978,1661,2743,2920,2440,2627,1526,625,2075,1816,1831,53,78,77,80,94,76,75,71,84,15,25,27,8,70,12,32,26,29,6,11,30,18,17,19,31,22,23,9,10,24,35,16,13,20,28,21,7,4,5,33,34,14,2,72,98,99,97,105])).
% 78.03/78.12 cnf(2987,plain,
% 78.03/78.12 (P7(f6(x29871,f5(f4(a1,x29872),f4(a1,x29872))),a1,a1)),
% 78.03/78.12 inference(scs_inference,[],[2882,2835,2314,2893,2978,1661,2743,2920,2440,2627,1526,625,2075,1816,1831,52,53,78,77,80,94,76,75,71,84,15,25,27,8,70,12,32,26,29,6,11,30,18,17,19,31,22,23,9,10,24,35,16,13,20,28,21,7,4,5,33,34,14,2,72,98,99,97,105,83])).
% 78.03/78.12 cnf(2989,plain,
% 78.03/78.12 (~P4(f19(f6(x29891,f5(x29892,a1)),x29892),x29893)),
% 78.03/78.12 inference(scs_inference,[],[2882,2835,2314,2893,2978,1661,2743,2920,2440,2627,1526,625,2075,1816,1831,58,65,52,53,78,77,80,94,76,75,71,84,15,25,27,8,70,12,32,26,29,6,11,30,18,17,19,31,22,23,9,10,24,35,16,13,20,28,21,7,4,5,33,34,14,2,72,98,99,97,105,83,45])).
% 78.03/78.12 cnf(2991,plain,
% 78.03/78.12 (P7(f4(f4(a14,x29911),f18(x29912)),f10(f4(a14,x29911),f7(f23(x29912,a14,x29913))),f13(f4(a14,x29911),f7(f23(x29912,a14,x29913))))),
% 78.03/78.12 inference(scs_inference,[],[2882,2835,2705,2314,2893,2978,1661,2743,2920,2440,2627,1526,625,2075,2386,1816,1831,58,65,52,53,78,77,80,94,76,75,71,84,15,25,27,8,70,12,32,26,29,6,11,30,18,17,19,31,22,23,9,10,24,35,16,13,20,28,21,7,4,5,33,34,14,2,72,98,99,97,105,83,45,42])).
% 78.03/78.12 cnf(3039,plain,
% 78.03/78.12 (P7(f6(f6(x30391,f5(f4(a1,x30392),f4(a1,x30392))),f5(x30393,x30394)),a1,a1)),
% 78.03/78.12 inference(scs_inference,[],[2987,2956,2971,1170,2455,768,78,143,144,77,80,94])).
% 78.03/78.12 cnf(3054,plain,
% 78.03/78.12 (E(f17(x30541,f23(x30542,x30543,f7(f23(x30544,a1,x30545)))),f17(x30541,f23(x30542,x30543,a2)))),
% 78.03/78.12 inference(scs_inference,[],[2987,2316,2956,2971,1170,2455,1841,768,1081,78,143,144,77,80,94,76,75,71,84,15,25,8,27,6,29])).
% 78.03/78.12 cnf(3082,plain,
% 78.03/78.12 (~P1(f13(f4(f4(a14,x30821),x30822),x30823),f10(f4(f4(a14,x30821),x30822),x30823))),
% 78.03/78.12 inference(scs_inference,[],[2987,2316,1664,2956,2971,1170,2455,1841,2920,768,1081,78,143,144,77,80,94,76,75,71,84,15,25,8,27,6,29,30,9,11,10,12,22,35,26,32,31,13,18,16,17,21,19,23,4,24,20,28,7,5,33,34,14,2,72])).
% 78.03/78.12 cnf(3084,plain,
% 78.03/78.12 (~P3(f23(x30841,f4(f4(a14,x30842),f18(x30843)),x30844))),
% 78.03/78.12 inference(scs_inference,[],[2975,2987,2316,1664,2991,2956,2971,1170,2455,1841,2920,768,1081,78,143,144,77,80,94,76,75,71,84,15,25,8,27,6,29,30,9,11,10,12,22,35,26,32,31,13,18,16,17,21,19,23,4,24,20,28,7,5,33,34,14,2,72,99])).
% 78.03/78.12 cnf(3086,plain,
% 78.03/78.12 (~P1(f13(f4(a14,x30861),x30862),f10(f4(a14,x30861),x30862))),
% 78.03/78.12 inference(rename_variables,[],[2975])).
% 78.03/78.12 cnf(3088,plain,
% 78.03/78.12 (P7(f6(x30881,f5(a2,a2)),f7(f23(x30882,a1,x30883)),f7(f23(x30882,a1,x30883)))),
% 78.03/78.12 inference(scs_inference,[],[2975,2987,2316,1664,2991,2956,2971,1170,2455,1841,2920,768,1081,266,78,143,144,77,80,94,76,75,71,84,15,25,8,27,6,29,30,9,11,10,12,22,35,26,32,31,13,18,16,17,21,19,23,4,24,20,28,7,5,33,34,14,2,72,99,83])).
% 78.03/78.12 cnf(3093,plain,
% 78.03/78.12 (~P4(f19(f6(x30931,f5(f23(x30932,a1,a3),a1)),f21(f23(x30932,a1,x30933),x30934)),x30935)),
% 78.03/78.12 inference(scs_inference,[],[2975,2989,2987,2316,1664,2763,2991,2956,2971,2481,2532,1170,2455,1841,2920,768,1081,266,78,143,144,77,80,94,76,75,71,84,15,25,8,27,6,29,30,9,11,10,12,22,35,26,32,31,13,18,16,17,21,19,23,4,24,20,28,7,5,33,34,14,2,72,99,83,48,45])).
% 78.03/78.12 cnf(3096,plain,
% 78.03/78.12 (~P7(f19(f6(x30961,f5(x30962,a1)),x30962),x30963,x30964)),
% 78.03/78.12 inference(scs_inference,[],[2975,2989,2987,2316,1664,2763,2991,2956,2971,2481,2532,1170,2455,1841,2920,768,1081,58,66,266,78,143,144,77,80,94,76,75,71,84,15,25,8,27,6,29,30,9,11,10,12,22,35,26,32,31,13,18,16,17,21,19,23,4,24,20,28,7,5,33,34,14,2,72,99,83,48,45,42])).
% 78.03/78.12 cnf(3099,plain,
% 78.03/78.12 (~P9(f4(a1,x30991),f4(a1,x30992))),
% 78.03/78.12 inference(rename_variables,[],[521])).
% 78.03/78.12 cnf(3100,plain,
% 78.03/78.12 (E(f4(f20(f6(x31001,f5(a2,x31002)),f7(f23(x31003,a1,x31004))),x31005),f4(x31001,x31005))),
% 78.03/78.12 inference(rename_variables,[],[2772])).
% 78.03/78.12 cnf(3107,plain,
% 78.03/78.12 (P1(f23(a2,f18(x31071),f18(x31072)),f23(f7(f23(x31073,a1,x31074)),f7(f23(x31071,a14,x31075)),f7(f23(x31072,a14,x31076))))),
% 78.03/78.12 inference(scs_inference,[],[521,3099,2975,2989,2987,2316,1664,2814,2751,2763,2772,3100,2991,2956,2971,2481,2532,1170,2874,2455,1841,2920,768,1337,1081,58,66,266,78,143,144,77,80,94,76,75,71,84,15,25,8,27,6,29,30,9,11,10,12,22,35,26,32,31,13,18,16,17,21,19,23,4,24,20,28,7,5,33,34,14,2,72,99,83,48,45,42,51,50,37,36])).
% 78.03/78.12 cnf(3113,plain,
% 78.03/78.12 (~E(f8(f23(a9,a14,a15)),f23(x31131,f4(f4(a14,x31132),f23(x31133,a1,a3)),x31134))),
% 78.03/78.12 inference(scs_inference,[],[62,521,3099,2975,2989,2980,2987,2316,1664,2814,2751,2763,2772,3100,2775,2991,2956,2971,2481,2532,1170,634,2874,2455,1841,2920,768,1337,1081,58,66,266,78,143,144,77,80,94,76,75,71,84,15,25,8,27,6,29,30,9,11,10,12,22,35,26,32,31,13,18,16,17,21,19,23,4,24,20,28,7,5,33,34,14,2,72,99,83,48,45,42,51,50,37,36,3,38])).
% 78.03/78.12 cnf(3114,plain,
% 78.03/78.12 (~P3(f17(f23(x31141,f4(f4(a14,x31142),x31143),a2),x31144))),
% 78.03/78.12 inference(scs_inference,[],[62,521,3099,2975,3086,2989,2980,2987,2316,1664,2814,2751,2763,2772,3100,2775,2991,2956,2971,2481,2532,1170,634,2874,2455,1841,2920,768,1337,1081,58,66,266,78,143,144,77,80,94,76,75,71,84,15,25,8,27,6,29,30,9,11,10,12,22,35,26,32,31,13,18,16,17,21,19,23,4,24,20,28,7,5,33,34,14,2,72,99,83,48,45,42,51,50,37,36,3,38,2738])).
% 78.03/78.12 cnf(3128,plain,
% 78.03/78.12 (P7(f6(f6(x31281,f5(a2,a2)),f5(x31282,x31283)),f7(f23(x31284,a1,x31285)),f7(f23(x31284,a1,x31285)))),
% 78.03/78.12 inference(scs_inference,[],[3088,1276,694,78,77,94])).
% 78.03/78.12 cnf(3132,plain,
% 78.03/78.12 (P4(f6(f6(x31321,f5(x31322,x31323)),f5(x31324,x31325)),f20(f6(x31322,f5(a2,x31326)),f7(f23(x31327,a1,x31328))))),
% 78.03/78.12 inference(scs_inference,[],[3088,2312,1276,1799,694,78,77,94,76,80])).
% 78.03/78.12 cnf(3173,plain,
% 78.03/78.12 (~P7(f6(f19(f6(x31731,f5(x31732,a1)),x31732),f5(f12(x31733,a14),x31734)),f11(x31733,a14),x31735)),
% 78.03/78.12 inference(scs_inference,[],[3088,3096,2312,3113,1276,637,1799,694,661,2108,78,77,94,76,80,75,71,84,15,25,8,27,11,26,10,9,22,29,6,32,23,17,12,30,13,21,4,24,35,18,31,16,19,5,28,7,20,33,14,34,2,98])).
% 78.03/78.12 cnf(3184,plain,
% 78.03/78.12 (~P7(f6(f4(a1,x31841),f5(f10(a14,x31842),x31843)),f13(a14,x31842),x31844)),
% 78.03/78.12 inference(scs_inference,[],[3088,3096,2312,3113,2977,3054,2943,1401,1276,637,2975,2580,1799,694,661,2108,61,78,77,94,76,80,75,71,84,15,25,8,27,11,26,10,9,22,29,6,32,23,17,12,30,13,21,4,24,35,18,31,16,19,5,28,7,20,33,14,34,2,98,99,83,48,42])).
% 78.03/78.12 cnf(3193,plain,
% 78.03/78.12 (~P1(f13(a14,f20(f6(x31931,f5(a2,x31932)),f7(f23(x31933,a1,x31934)))),f10(a14,x31931))),
% 78.03/78.12 inference(scs_inference,[],[2916,3088,3096,2312,2243,3113,2764,2774,2977,2588,3054,2943,1401,1276,637,2975,2580,1799,2874,694,661,2108,61,117,78,77,94,76,80,75,71,84,15,25,8,27,11,26,10,9,22,29,6,32,23,17,12,30,13,21,4,24,35,18,31,16,19,5,28,7,20,33,14,34,2,98,99,83,48,42,51,50,37,36])).
% 78.03/78.12 cnf(3200,plain,
% 78.03/78.12 (~E(f8(f23(a9,a14,a15)),f23(x32001,f4(f4(a14,x32002),f18(x32003)),x32004))),
% 78.03/78.12 inference(scs_inference,[],[62,2916,3088,3096,3084,2312,2243,3113,2764,2770,2774,2977,2588,3054,2943,1401,1276,637,2975,2580,1639,1799,2874,64,694,661,2108,61,117,78,77,94,76,80,75,71,84,15,25,8,27,11,26,10,9,22,29,6,32,23,17,12,30,13,21,4,24,35,18,31,16,19,5,28,7,20,33,14,34,2,98,99,83,48,42,51,50,37,36,3,41,38])).
% 78.03/78.12 cnf(3205,plain,
% 78.03/78.12 (~P4(f19(f6(x32051,f5(f18(x32052),a1)),f7(f23(x32052,a14,x32053))),x32054)),
% 78.03/78.12 inference(scs_inference,[],[62,2916,3088,3096,3084,2312,2243,3113,2764,2770,2774,2977,2588,3054,2943,1401,1276,1796,637,2975,2989,2580,1639,2677,1799,2874,64,694,661,2108,61,117,78,77,94,76,80,75,71,84,15,25,8,27,11,26,10,9,22,29,6,32,23,17,12,30,13,21,4,24,35,18,31,16,19,5,28,7,20,33,14,34,2,98,99,83,48,42,51,50,37,36,3,41,38,69,86,45])).
% 78.03/78.12 cnf(3217,plain,
% 78.03/78.12 (P7(f6(f6(f6(x32171,f5(a2,a2)),f5(x32172,x32173)),f5(x32174,x32175)),f7(f23(x32176,a1,x32177)),f7(f23(x32176,a1,x32177)))),
% 78.03/78.12 inference(scs_inference,[],[3128,1065,2091,78,77,94])).
% 78.03/78.12 cnf(3240,plain,
% 78.03/78.12 (E(f5(a1,x32401),f5(f20(f6(f4(a1,x32402),f5(a2,x32403)),f7(f23(x32404,a1,x32405))),x32401))),
% 78.03/78.12 inference(scs_inference,[],[3128,2453,3132,1065,510,2091,1870,78,77,94,76,80,75,71,84,15,25,27,8,29,26,22,30,32,11,10,6])).
% 78.03/78.12 cnf(3249,plain,
% 78.03/78.12 (E(f13(x32491,a1),f13(x32491,f20(f6(f4(a1,x32492),f5(a2,x32493)),f7(f23(x32494,a1,x32495)))))),
% 78.03/78.12 inference(scs_inference,[],[3128,2453,3132,1065,510,2091,1870,78,77,94,76,80,75,71,84,15,25,27,8,29,26,22,30,32,11,10,6,17,35,24,13,16,9,4,21,23])).
% 78.03/78.12 cnf(3262,plain,
% 78.03/78.12 (~P3(f23(x32621,f4(f4(a14,x32622),x32623),x32624))),
% 78.03/78.12 inference(scs_inference,[],[3128,2453,3200,3132,1065,510,2975,2386,2091,1870,78,77,94,76,80,75,71,84,15,25,27,8,29,26,22,30,32,11,10,6,17,35,24,13,16,9,4,21,23,12,18,28,20,19,7,31,5,33,14,34,2,99])).
% 78.03/78.12 cnf(3269,plain,
% 78.03/78.12 (E(f23(x32691,f20(f6(x32692,f5(a2,x32693)),f7(f23(x32694,a1,x32695))),x32696),f23(x32691,x32692,x32696))),
% 78.03/78.12 inference(rename_variables,[],[2765])).
% 78.03/78.12 cnf(3280,plain,
% 78.03/78.12 (P1(f12(x32801,x32802),f12(x32801,f20(f6(x32802,f5(a2,x32803)),f7(f23(x32804,a1,x32805)))))),
% 78.03/78.12 inference(scs_inference,[],[3184,3128,2453,3200,3132,2765,3269,2767,2776,1466,911,1065,2372,510,2975,2874,2386,2091,1870,58,1867,54,59,78,77,94,76,80,75,71,84,15,25,27,8,29,26,22,30,32,11,10,6,17,35,24,13,16,9,4,21,23,12,18,28,20,19,7,31,5,33,14,34,2,99,83,48,43,51,50,37,36])).
% 78.03/78.12 cnf(3294,plain,
% 78.03/78.12 (P7(f6(f6(f6(x32941,f5(f4(a1,x32942),f4(a1,x32942))),f5(x32943,x32944)),f5(x32945,x32946)),a1,a1)),
% 78.03/78.12 inference(scs_inference,[],[3039,2121,194,78,77,94])).
% 78.03/78.12 cnf(3298,plain,
% 78.03/78.12 (P4(f6(f6(x32981,f5(f23(x32982,a1,a3),x32983)),f5(x32984,x32985)),f8(f23(x32982,a1,x32986)))),
% 78.03/78.12 inference(scs_inference,[],[2471,3039,2121,567,194,78,77,94,76,80])).
% 78.03/78.12 cnf(3307,plain,
% 78.03/78.12 (E(f10(x33071,f8(f23(x33072,a1,x33073))),f10(x33071,f8(f23(x33072,a1,x33074))))),
% 78.03/78.12 inference(scs_inference,[],[2471,3039,2121,567,524,194,78,77,94,76,80,75,71,84,15,27])).
% 78.03/78.12 cnf(3312,plain,
% 78.03/78.12 (E(f19(x33121,f8(f23(x33122,a1,x33123))),f19(x33121,f8(f23(x33122,a1,x33124))))),
% 78.03/78.12 inference(scs_inference,[],[2471,3039,2121,567,524,194,78,77,94,76,80,75,71,84,15,27,25,8,22,26,17])).
% 78.03/78.12 cnf(3314,plain,
% 78.03/78.12 (E(f23(x33141,f8(f23(x33142,a1,x33143)),x33144),f23(x33141,f8(f23(x33142,a1,x33145)),x33144))),
% 78.03/78.12 inference(scs_inference,[],[2471,3039,2121,567,524,194,78,77,94,76,80,75,71,84,15,27,25,8,22,26,17,29,11])).
% 78.03/78.12 cnf(3324,plain,
% 78.03/78.12 (E(f23(f8(f23(x33241,a1,x33242)),x33243,x33244),f23(f8(f23(x33241,a1,x33245)),x33243,x33244))),
% 78.03/78.12 inference(scs_inference,[],[2471,3039,2121,567,524,194,78,77,94,76,80,75,71,84,15,27,25,8,22,26,17,29,11,32,4,30,16,12,18,13,6,21,10])).
% 78.03/78.12 cnf(3325,plain,
% 78.03/78.12 (E(f13(x33251,f8(f23(x33252,a1,x33253))),f13(x33251,f8(f23(x33252,a1,x33254))))),
% 78.03/78.12 inference(scs_inference,[],[2471,3039,2121,567,524,194,78,77,94,76,80,75,71,84,15,27,25,8,22,26,17,29,11,32,4,30,16,12,18,13,6,21,10,23])).
% 78.03/78.12 cnf(3329,plain,
% 78.03/78.12 (E(f6(x33291,f8(f23(x33292,a1,x33293))),f6(x33291,f8(f23(x33292,a1,x33294))))),
% 78.03/78.12 inference(scs_inference,[],[2471,3039,2121,567,524,194,78,77,94,76,80,75,71,84,15,27,25,8,22,26,17,29,11,32,4,30,16,12,18,13,6,21,10,23,24,35,20,9])).
% 78.03/78.12 cnf(3330,plain,
% 78.03/78.12 (E(f4(x33301,f8(f23(x33302,a1,x33303))),f4(x33301,f8(f23(x33302,a1,x33304))))),
% 78.03/78.12 inference(scs_inference,[],[2471,3039,2121,567,524,194,78,77,94,76,80,75,71,84,15,27,25,8,22,26,17,29,11,32,4,30,16,12,18,13,6,21,10,23,24,35,20,9,5])).
% 78.03/78.12 cnf(3350,plain,
% 78.03/78.12 (~P1(f13(a14,a1),f10(a14,f4(a1,x33501)))),
% 78.03/78.12 inference(scs_inference,[],[2471,3039,1698,3173,2773,2857,3193,3280,3249,2683,2121,2229,567,524,153,194,117,78,77,94,76,80,75,71,84,15,27,25,8,22,26,17,29,11,32,4,30,16,12,18,13,6,21,10,23,24,35,20,9,5,7,28,31,19,14,33,34,2,98,48,51,37,36])).
% 78.03/78.12 cnf(3353,plain,
% 78.03/78.12 (E(f5(a1,x33531),f5(f4(a1,x33532),x33531))),
% 78.03/78.12 inference(scs_inference,[],[2471,3039,1698,3173,2769,2773,2857,3193,3280,3240,3249,2683,2121,2229,567,524,153,194,117,78,77,94,76,80,75,71,84,15,27,25,8,22,26,17,29,11,32,4,30,16,12,18,13,6,21,10,23,24,35,20,9,5,7,28,31,19,14,33,34,2,98,48,51,37,36,3])).
% 78.03/78.12 cnf(3356,plain,
% 78.03/78.12 (~E(f8(f23(a9,a14,a15)),f23(x33561,f4(f4(a14,x33562),x33563),x33564))),
% 78.03/78.12 inference(scs_inference,[],[62,3262,2471,3039,1698,3173,2769,2773,2857,3193,3280,3240,3249,2683,2121,2229,567,524,153,194,117,78,77,94,76,80,75,71,84,15,27,25,8,22,26,17,29,11,32,4,30,16,12,18,13,6,21,10,23,24,35,20,9,5,7,28,31,19,14,33,34,2,98,48,51,37,36,3,38])).
% 78.03/78.12 cnf(3357,plain,
% 78.03/78.12 (P1(f10(a14,f4(a1,x33571)),f13(a14,a1))),
% 78.03/78.12 inference(scs_inference,[],[62,3262,2471,3039,1698,3173,2769,2773,2857,3193,3280,3240,3249,2683,2121,2229,567,524,153,194,117,78,77,94,76,80,75,71,84,15,27,25,8,22,26,17,29,11,32,4,30,16,12,18,13,6,21,10,23,24,35,20,9,5,7,28,31,19,14,33,34,2,98,48,51,37,36,3,38,69])).
% 78.03/78.12 cnf(3370,plain,
% 78.03/78.12 (P7(f6(x33701,f5(f5(a1,x33702),f5(a1,x33702))),f5(f4(a1,x33703),x33702),f5(f4(a1,x33703),x33702))),
% 78.03/78.12 inference(scs_inference,[],[62,3262,2471,3039,1698,3173,3093,2985,3107,2769,2773,2857,3193,3280,3240,3249,2683,2121,2229,2072,567,524,153,1306,194,117,78,77,94,76,80,75,71,84,15,27,25,8,22,26,17,29,11,32,4,30,16,12,18,13,6,21,10,23,24,35,20,9,5,7,28,31,19,14,33,34,2,98,48,51,37,36,3,38,69,74,99,85,86,83])).
% 78.03/78.12 cnf(3372,plain,
% 78.03/78.12 (P6(f19(a2,a2),f17(f19(a2,a2),x33721))),
% 78.03/78.12 inference(scs_inference,[],[62,3262,2471,3039,1698,2745,3173,3093,2985,3107,2769,2773,2857,3193,3280,3240,3249,2683,2121,2229,2072,567,524,2094,153,1306,194,117,78,77,94,76,80,75,71,84,15,27,25,8,22,26,17,29,11,32,4,30,16,12,18,13,6,21,10,23,24,35,20,9,5,7,28,31,19,14,33,34,2,98,48,51,37,36,3,38,69,74,99,85,86,83,39])).
% 78.03/78.12 cnf(3382,plain,
% 78.03/78.12 (P4(f6(x33821,f5(f5(a1,x33822),x33823)),f5(f4(a1,x33824),x33822))),
% 78.03/78.12 inference(scs_inference,[],[3353,78])).
% 78.03/78.12 cnf(3390,plain,
% 78.03/78.12 (P6(f19(a2,a2),f21(f17(f19(a2,a2),x33901),x33902))),
% 78.03/78.12 inference(scs_inference,[],[3372,3353,2930,3298,1406,78,77,80,94,76])).
% 78.03/78.12 cnf(3392,plain,
% 78.03/78.12 (P6(f19(a2,a2),f8(f17(f19(a2,a2),x33921)))),
% 78.03/78.12 inference(scs_inference,[],[3372,3353,2930,3298,1406,78,77,80,94,76,71])).
% 78.03/78.12 cnf(3394,plain,
% 78.03/78.12 (P6(f19(a2,a2),f17(f17(f19(a2,a2),x33941),x33942))),
% 78.03/78.12 inference(scs_inference,[],[3372,3353,2930,3298,1406,78,77,80,94,76,71,75])).
% 78.03/78.12 cnf(3398,plain,
% 78.03/78.12 (E(f20(x33981,f5(a1,x33982)),f20(x33981,f5(f4(a1,x33983),x33982)))),
% 78.03/78.12 inference(scs_inference,[],[3372,3353,2930,3298,1406,78,77,80,94,76,71,75,84,15])).
% 78.03/78.12 cnf(3400,plain,
% 78.03/78.12 (E(f10(x34001,f5(a1,x34002)),f10(x34001,f5(f4(a1,x34003),x34002)))),
% 78.03/78.12 inference(scs_inference,[],[3372,3353,2930,3298,1406,78,77,80,94,76,71,75,84,15,25,27])).
% 78.03/78.12 cnf(3402,plain,
% 78.03/78.12 (E(f19(x34021,f5(a1,x34022)),f19(x34021,f5(f4(a1,x34023),x34022)))),
% 78.03/78.12 inference(scs_inference,[],[3372,3353,2930,3298,1406,78,77,80,94,76,71,75,84,15,25,27,22,17])).
% 78.03/78.12 cnf(3407,plain,
% 78.03/78.12 (E(f23(x34071,x34072,f5(a1,x34073)),f23(x34071,x34072,f5(f4(a1,x34074),x34073)))),
% 78.03/78.12 inference(scs_inference,[],[3372,3353,2930,3298,1406,78,77,80,94,76,71,75,84,15,25,27,22,17,32,8,16,26,12])).
% 78.03/78.12 cnf(3411,plain,
% 78.03/78.12 (E(f23(x34111,f5(a1,x34112),x34113),f23(x34111,f5(f4(a1,x34114),x34112),x34113))),
% 78.03/78.12 inference(scs_inference,[],[3372,3353,2930,3298,1406,78,77,80,94,76,71,75,84,15,25,27,22,17,32,8,16,26,12,29,4,18,11])).
% 78.03/78.12 cnf(3412,plain,
% 78.03/78.12 (E(f13(x34121,f5(a1,x34122)),f13(x34121,f5(f4(a1,x34123),x34122)))),
% 78.03/78.12 inference(scs_inference,[],[3372,3353,2930,3298,1406,78,77,80,94,76,71,75,84,15,25,27,22,17,32,8,16,26,12,29,4,18,11,23])).
% 78.03/78.12 cnf(3431,plain,
% 78.03/78.12 (~P3(f23(x34311,f4(a14,x34312),x34313))),
% 78.03/78.12 inference(scs_inference,[],[3372,3353,3356,2930,3298,1406,2874,641,78,77,80,94,76,71,75,84,15,25,27,22,17,32,8,16,26,12,29,4,18,11,23,10,13,21,30,9,24,20,35,7,6,19,14,5,33,31,28,34,2,99])).
% 78.03/78.12 cnf(3434,plain,
% 78.03/78.12 (P7(f6(x34341,f5(f5(a1,x34342),x34343)),f5(f4(a1,x34344),x34342),f20(f6(x34343,f5(x34345,x34346)),x34345))),
% 78.03/78.12 inference(scs_inference,[],[3372,3353,3356,2930,3298,1406,2874,641,190,78,77,80,94,76,71,75,84,15,25,27,22,17,32,8,16,26,12,29,4,18,11,23,10,13,21,30,9,24,20,35,7,6,19,14,5,33,31,28,34,2,99,83])).
% 78.03/78.12 cnf(3442,plain,
% 78.03/78.12 (~P1(f11(a9,a14),f19(f6(x34421,f5(f8(f23(x34422,a1,x34423)),f12(a9,a14))),f8(f23(x34422,a1,x34424))))),
% 78.03/78.12 inference(scs_inference,[],[3357,3372,3353,3350,3356,2930,3298,2799,3324,3312,2379,1406,2874,641,190,78,77,80,94,76,71,75,84,15,25,27,22,17,32,8,16,26,12,29,4,18,11,23,10,13,21,30,9,24,20,35,7,6,19,14,5,33,31,28,34,2,99,83,51,73,37])).
% 78.03/78.12 cnf(3451,plain,
% 78.03/78.12 (~P3(f23(x34511,f6(x34512,f5(f10(a14,f4(a1,x34513)),f13(a14,a1))),x34514))),
% 78.03/78.12 inference(scs_inference,[],[62,3357,3372,3353,3350,3356,2930,3298,2799,3324,3312,3114,237,2379,1406,1074,2874,641,2108,190,78,77,80,94,76,71,75,84,15,25,27,22,17,32,8,16,26,12,29,4,18,11,23,10,13,21,30,9,24,20,35,7,6,19,14,5,33,31,28,34,2,99,83,51,73,37,36,3,38,104])).
% 78.03/78.12 cnf(3519,plain,
% 78.03/78.12 (E(f19(x35191,f5(a1,x35192)),f19(x35191,f5(f4(a1,x35193),x35192)))),
% 78.03/78.12 inference(rename_variables,[],[3402])).
% 78.03/78.12 cnf(3524,plain,
% 78.03/78.12 (E(f23(x35241,x35242,f5(a1,x35243)),f23(x35241,x35242,f5(f4(a1,x35244),x35243)))),
% 78.03/78.12 inference(rename_variables,[],[3407])).
% 78.03/78.12 cnf(3525,plain,
% 78.03/78.12 (~P9(f23(f7(f23(x35251,a1,x35252)),f21(f23(x35253,a1,x35254),x35255),x35256),f23(a2,f23(x35253,a1,a3),x35256))),
% 78.03/78.12 inference(rename_variables,[],[2633])).
% 78.03/78.12 cnf(3527,plain,
% 78.03/78.12 (E(f23(x35271,x35272,f5(a1,x35273)),f23(x35271,x35272,f5(f4(a1,x35274),x35273)))),
% 78.03/78.12 inference(rename_variables,[],[3407])).
% 78.03/78.12 cnf(3530,plain,
% 78.03/78.12 (E(f20(x35301,f5(a1,x35302)),f20(x35301,f5(f4(a1,x35303),x35302)))),
% 78.03/78.12 inference(rename_variables,[],[3398])).
% 78.03/78.12 cnf(3532,plain,
% 78.03/78.12 (~P1(f13(f4(f4(a14,x35321),x35322),f5(a1,x35323)),f10(f4(f4(a14,x35321),x35322),f5(f4(a1,x35324),x35323)))),
% 78.03/78.12 inference(scs_inference,[],[3390,3382,3407,3524,3398,3402,3519,3412,1667,3370,2633,3525,3442,2792,2790,3082,3350,3096,1778,2989,767,1611,209,78,77,80,94,76,75,71,69,84,15,27,25,22,32,18,17,16,4,21,9,29,13,12,10,8,26,11,23,20,30,24,35,14,6,19,7,33,31,5,28,34,2,99,45,42,51,50,37,36])).
% 78.03/78.12 cnf(3535,plain,
% 78.03/78.12 (E(f23(x35351,f5(a1,x35352),f5(a1,x35353)),f23(x35351,f5(f4(a1,x35354),x35352),f5(f4(a1,x35355),x35353)))),
% 78.03/78.12 inference(scs_inference,[],[3390,3382,3407,3524,3527,3411,3398,3402,3519,3412,1667,3370,2633,3525,3442,2792,2790,3082,3350,3096,1778,2989,767,1611,209,78,77,80,94,76,75,71,69,84,15,27,25,22,32,18,17,16,4,21,9,29,13,12,10,8,26,11,23,20,30,24,35,14,6,19,7,33,31,5,28,34,2,99,45,42,51,50,37,36,3])).
% 78.03/78.12 cnf(3541,plain,
% 78.03/78.12 (~E(f8(f23(a9,a14,a15)),f23(x35411,f4(a14,x35412),x35413))),
% 78.03/78.12 inference(scs_inference,[],[62,3431,3390,3382,3407,3524,3527,3411,3398,3530,3402,3519,3412,1667,3370,2633,3525,3442,2792,2790,3082,3350,470,3096,1778,2989,767,1611,209,78,77,80,94,76,75,71,69,84,15,27,25,22,32,18,17,16,4,21,9,29,13,12,10,8,26,11,23,20,30,24,35,14,6,19,7,33,31,5,28,34,2,99,45,42,51,50,37,36,3,47,38])).
% 78.03/78.12 cnf(3546,plain,
% 78.03/78.12 (P4(a14,f18(a9))),
% 78.03/78.12 inference(scs_inference,[],[62,3431,3390,3382,3407,3524,3527,3411,3398,3530,3402,3519,3412,1667,3370,2633,3525,3442,2792,2790,3082,2729,3350,470,3096,1778,483,2989,767,1611,209,78,77,80,94,76,75,71,69,84,15,27,25,22,32,18,17,16,4,21,9,29,13,12,10,8,26,11,23,20,30,24,35,14,6,19,7,33,31,5,28,34,2,99,45,42,51,50,37,36,3,47,38,106,86,2822])).
% 78.03/78.12 cnf(3557,plain,
% 78.03/78.12 (P4(f6(a14,f5(x35571,x35572)),f18(a9))),
% 78.03/78.12 inference(scs_inference,[],[3546,1218,766,78,77,80])).
% 78.03/78.12 cnf(3603,plain,
% 78.03/78.12 (~E(f23(x36031,f4(a14,x36032),x36033),f8(f23(a9,a14,a15)))),
% 78.03/78.12 inference(scs_inference,[],[3546,3541,3392,3217,3532,1218,1600,766,78,77,80,94,76,71,75,69,84,15,25,27,22,32,17,29,16,18,9,26,24,23,21,30,8,4,10,11,13,20,12,19,35,14,6,33,31,7,28,5,34,2])).
% 78.03/78.12 cnf(3604,plain,
% 78.03/78.12 (P3(f23(x36041,f6(f6(a1,f5(f7(f23(x36042,a14,x36043)),f18(x36042))),f5(x36044,a2)),x36045))),
% 78.03/78.12 inference(scs_inference,[],[3546,3541,3392,3217,3532,2880,1218,1600,766,53,78,77,80,94,76,71,75,69,84,15,25,27,22,32,17,29,16,18,9,26,24,23,21,30,8,4,10,11,13,20,12,19,35,14,6,33,31,7,28,5,34,2,105])).
% 78.03/78.12 cnf(3625,plain,
% 78.03/78.12 (~P1(f13(f4(a14,x36251),f8(f23(x36252,a1,x36253))),f10(f4(a14,x36251),f8(f23(x36252,a1,x36254))))),
% 78.03/78.12 inference(scs_inference,[],[3546,3541,3392,3217,3307,3329,3330,3532,3434,2880,1184,1228,3398,2620,1218,2975,2259,1600,766,66,65,53,78,77,80,94,76,71,75,69,84,15,25,27,22,32,17,29,16,18,9,26,24,23,21,30,8,4,10,11,13,20,12,19,35,14,6,33,31,7,28,5,34,2,105,98,99,85,45,51,50,37])).
% 78.03/78.12 cnf(3634,plain,
% 78.03/78.12 (~P9(f18(a9),f19(a14,f18(a9)))),
% 78.03/78.12 inference(scs_inference,[],[62,3546,3541,3392,3217,3535,3307,3329,3330,3532,3434,2880,1184,1228,2261,1003,3398,2620,1218,2975,2259,1337,1600,766,129,2108,66,65,53,78,77,80,94,76,71,75,69,84,15,25,27,22,32,17,29,16,18,9,26,24,23,21,30,8,4,10,11,13,20,12,19,35,14,6,33,31,7,28,5,34,2,105,98,99,85,45,51,50,37,36,3,38,102])).
% 78.03/78.12 cnf(3649,plain,
% 78.03/78.12 (P4(f6(f6(a14,f5(x36491,x36492)),f5(x36493,x36494)),f18(a9))),
% 78.03/78.12 inference(scs_inference,[],[3557,830,232,78,77,80])).
% 78.03/78.12 cnf(3715,plain,
% 78.03/78.12 (~P1(f19(a14,f18(a9)),f18(a9))),
% 78.03/78.12 inference(scs_inference,[],[3557,3634,3603,3394,1670,2888,3314,3205,3325,3625,3604,3451,2461,3400,1319,2953,2547,957,830,3350,220,3546,2874,915,875,232,129,60,78,77,80,94,76,75,71,69,84,15,25,27,22,32,17,29,18,16,24,21,30,14,23,26,9,13,8,35,10,33,11,4,19,12,20,31,6,28,5,34,7,2,85,99,51,50,37,36,3,38,103])).
% 78.03/78.12 cnf(3720,plain,
% 78.03/78.12 (~P1(f18(a9),f19(a14,f18(a9)))),
% 78.03/78.12 inference(scs_inference,[],[3557,3634,3603,3394,1670,2888,3314,3205,3325,3625,3604,3451,2461,3400,1319,2953,2547,957,830,3350,407,220,3546,2874,915,875,232,129,60,78,77,80,94,76,75,71,69,84,15,25,27,22,32,17,29,18,16,24,21,30,14,23,26,9,13,8,35,10,33,11,4,19,12,20,31,6,28,5,34,7,2,85,99,51,50,37,36,3,38,103,86,73])).
% 78.03/78.12 cnf(3741,plain,
% 78.03/78.12 ($false),
% 78.03/78.12 inference(scs_inference,[],[3715,3720,3649,2468,3294,1013,914,78,77,80,94,76,75,71,69]),
% 78.03/78.12 ['proof']).
% 78.03/78.12 % SZS output end Proof
% 78.03/78.12 % Total time :77.320000s
%------------------------------------------------------------------------------