%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : GEO093+1 : TPTP v8.2.0. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% Computer : n017.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 06:03:46 EDT 2024
% Result : Theorem 60.74s 60.81s
% Output : CNFRefutation 60.81s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : GEO093+1 : TPTP v8.2.0. Released v2.4.0.
% 0.07/0.12 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% 0.12/0.33 % Computer : n017.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 300
% 0.12/0.33 % DateTime : Fri Jun 21 08:09:54 EDT 2024
% 0.12/0.33 % CPUTime :
% 0.49/0.55 start to proof:theBenchmark
% 60.74/60.79 %-------------------------------------------
% 60.74/60.79 % File :CSE---1.7
% 60.74/60.79 % Problem :theBenchmark
% 60.74/60.79 % Transform :cnf
% 60.74/60.79 % Format :tptp:raw
% 60.74/60.79 % Command :java -jar mcs_scs.jar %d %s
% 60.74/60.79
% 60.74/60.79 % Result :Theorem 60.200000s
% 60.74/60.79 % Output :CNFRefutation 60.200000s
% 60.74/60.79 %-------------------------------------------
% 60.74/60.81 %--------------------------------------------------------------------------
% 60.74/60.81 % File : GEO093+1 : TPTP v8.2.0. Released v2.4.0.
% 60.74/60.81 % Domain : Geometry (Oriented curves)
% 60.74/60.81 % Problem : Sum of meeting open curves is open
% 60.74/60.81 % Version : [EHK99] axioms.
% 60.74/60.81 % English : If two open sub-curves of an open curve meet, then their sum
% 60.74/60.81 % is also open.
% 60.74/60.81
% 60.74/60.81 % Refs : [KE99] Kulik & Eschenbach (1999), A Geometry of Oriented Curv
% 60.74/60.81 % : [EHK99] Eschenbach et al. (1999), Representing Simple Trajecto
% 60.74/60.81 % Source : [KE99]
% 60.74/60.81 % Names : Proposition 2.14 (2) [KE99]
% 60.74/60.81
% 60.74/60.81 % Status : Theorem
% 60.74/60.81 % Rating : 0.56 v8.1.0, 0.58 v7.5.0, 0.62 v7.4.0, 0.53 v7.3.0, 0.59 v7.2.0, 0.55 v7.1.0, 0.57 v7.0.0, 0.53 v6.4.0, 0.54 v6.2.0, 0.64 v6.1.0, 0.70 v6.0.0, 0.74 v5.4.0, 0.75 v5.3.0, 0.74 v5.2.0, 0.65 v5.1.0, 0.67 v4.1.0, 0.65 v4.0.1, 0.61 v4.0.0, 0.58 v3.7.0, 0.60 v3.5.0, 0.63 v3.4.0, 0.68 v3.3.0, 0.71 v3.2.0, 0.73 v3.1.0, 0.78 v2.7.0, 0.67 v2.4.0
% 60.74/60.81 % Syntax : Number of formulae : 17 ( 1 unt; 0 def)
% 60.74/60.81 % Number of atoms : 72 ( 10 equ)
% 60.74/60.81 % Maximal formula atoms : 12 ( 4 avg)
% 60.74/60.81 % Number of connectives : 59 ( 4 ~; 9 |; 24 &)
% 60.74/60.81 % ( 9 <=>; 13 =>; 0 <=; 0 <~>)
% 60.74/60.81 % Maximal formula depth : 12 ( 7 avg)
% 60.74/60.81 % Maximal term depth : 2 ( 1 avg)
% 60.74/60.81 % Number of predicates : 8 ( 7 usr; 0 prp; 1-3 aty)
% 60.74/60.81 % Number of functors : 1 ( 1 usr; 0 con; 2-2 aty)
% 60.74/60.81 % Number of variables : 57 ( 48 !; 9 ?)
% 60.74/60.81 % SPC : FOF_THM_RFO_SEQ
% 60.74/60.81
% 60.74/60.81 % Comments :
% 60.74/60.81 %--------------------------------------------------------------------------
% 60.74/60.81 %----Include simple curve axioms
% 60.74/60.81 include('Axioms/GEO004+0.ax').
% 60.74/60.81 %--------------------------------------------------------------------------
% 60.74/60.81 fof(proposition_2_14_2,conjecture,
% 60.74/60.81 ! [C,C1,C2,P] :
% 60.74/60.81 ( ( open(C)
% 60.74/60.81 & part_of(C1,C)
% 60.74/60.81 & part_of(C2,C)
% 60.74/60.81 & meet(P,C1,C2) )
% 60.74/60.81 => open(sum(C1,C2)) ) ).
% 60.74/60.81
% 60.74/60.81 %--------------------------------------------------------------------------
% 60.74/60.81 %-------------------------------------------
% 60.74/60.81 % Proof found
% 60.74/60.81 % SZS status Theorem for theBenchmark
% 60.74/60.81 % SZS output start Proof
% 60.74/60.81 %ClaNum:91(EqnAxiom:43)
% 60.74/60.81 %VarNum:331(SingletonVarNum:113)
% 60.74/60.81 %MaxLitNum:12
% 60.74/60.82 %MaxfuncDepth:2
% 60.74/60.82 %SharedTerms:10
% 60.74/60.82 %goalClause: 44 45 46 48 49
% 60.74/60.82 %singleGoalClaCount:5
% 60.74/60.82 [44]P1(a1)
% 60.74/60.82 [45]P7(a6,a1)
% 60.74/60.82 [46]P7(a7,a1)
% 60.74/60.82 [48]P6(a9,a6,a7)
% 60.74/60.82 [49]~P1(f17(a6,a7))
% 60.74/60.82 [47]P2(f8(x471),x471)
% 60.74/60.82 [50]P3(x501)+P4(f10(x501),x501)
% 60.74/60.82 [52]~P1(x521)+P4(f16(x521),x521)
% 60.74/60.82 [51]P1(x511)+~P4(x512,x511)
% 60.74/60.82 [54]~P3(x541)+~P4(x542,x541)
% 60.74/60.82 [55]~P4(x551,x552)+P5(x551,x552)
% 60.74/60.82 [56]~P2(x561,x562)+P5(x561,x562)
% 60.74/60.82 [57]~P2(x571,x572)+~P4(x571,x572)
% 60.74/60.82 [58]~P4(x582,x581)+~E(f2(x581,x582),x582)
% 60.74/60.82 [60]P7(x601,x602)+P5(f11(x602,x601),x601)
% 60.74/60.82 [64]~P4(x642,x641)+P4(f2(x641,x642),x641)
% 60.74/60.82 [71]P7(x711,x712)+~P5(f11(x712,x711),x712)
% 60.74/60.82 [78]~P2(x781,x782)+P6(x781,f18(x782,x781),f3(x782,x781))
% 60.74/60.82 [73]~P2(x732,x731)+E(f17(f18(x731,x732),f3(x731,x732)),x731)
% 60.74/60.82 [74]P5(x741,x742)+~P6(x741,x743,x742)
% 60.74/60.82 [75]P5(x751,x752)+~P6(x751,x752,x753)
% 60.74/60.82 [76]~P6(x763,x761,x762)+E(f5(x761,x762),f17(x761,x762))
% 60.74/60.82 [53]P1(x531)+~P7(x531,x532)+E(x531,x532)
% 60.74/60.82 [59]P2(x591,x592)+~P5(x591,x592)+P4(x591,x592)
% 60.74/60.82 [67]~P5(x671,x672)+P4(x671,x672)+P5(x671,f12(x671,x672))
% 60.74/60.82 [68]~P5(x681,x682)+P4(x681,x682)+P5(x681,f14(x681,x682))
% 60.74/60.82 [69]~P5(x691,x692)+P4(x691,x692)+P7(f12(x691,x692),x692)
% 60.74/60.82 [70]~P5(x701,x702)+P4(x701,x702)+P7(f14(x701,x702),x702)
% 60.74/60.82 [72]E(x721,x722)+P5(f4(x721,x722),x722)+P5(f4(x721,x722),x721)
% 60.74/60.82 [77]E(x771,x772)+~P5(f4(x771,x772),x772)+~P5(f4(x771,x772),x771)
% 60.74/60.82 [79]~P5(x791,x792)+P4(x791,x792)+~P7(f12(x791,x792),f14(x791,x792))
% 60.74/60.82 [80]~P5(x801,x802)+P4(x801,x802)+~P7(f14(x801,x802),f12(x801,x802))
% 60.74/60.82 [61]~P5(x611,x613)+P5(x611,x612)+~P7(x613,x612)
% 60.74/60.82 [89]~P5(f13(x891,x892,x893),x893)+~P5(f13(x891,x892,x893),x891)+E(x891,f17(x892,x893))
% 60.74/60.82 [90]~P5(f13(x901,x902,x903),x902)+~P5(f13(x901,x902,x903),x901)+E(x901,f17(x902,x903))
% 60.74/60.82 [62]~P5(x621,x624)+P5(x621,x622)+~E(x622,f17(x623,x624))
% 60.74/60.82 [63]~P5(x631,x633)+P5(x631,x632)+~E(x632,f17(x633,x634))
% 60.74/60.82 [85]~P5(x851,x853)+~P5(x851,x852)+P6(x851,x852,x853)+P5(f15(x851,x852,x853),x853)
% 60.74/60.82 [86]~P5(x861,x863)+~P5(x861,x862)+P6(x861,x862,x863)+P5(f15(x861,x862,x863),x862)
% 60.74/60.82 [88]P5(f13(x881,x882,x883),x883)+P5(f13(x881,x882,x883),x882)+P5(f13(x881,x882,x883),x881)+E(x881,f17(x882,x883))
% 60.74/60.82 [82]~P5(x821,x822)+P4(x821,x822)+~P6(x824,x823,x822)+~P5(x821,x823)
% 60.74/60.82 [83]~P5(x831,x832)+P4(x831,x832)+~P6(x834,x832,x833)+~P5(x831,x833)
% 60.74/60.82 [66]~P5(x661,x664)+P5(x661,x662)+P5(x661,x663)+~E(x664,f17(x663,x662))
% 60.74/60.82 [91]~P5(x911,x913)+~P5(x911,x912)+P6(x911,x912,x913)+~P4(f15(x911,x912,x913),x913)+~P4(f15(x911,x912,x913),x912)
% 60.74/60.82 [84]~P3(x844)+~P4(x841,x842)+P6(x841,x842,x843)+~P6(x845,x842,x843)+~E(x844,f17(x842,x843))
% 60.74/60.82 [65]E(x653,x651)+~P4(x651,x654)+~P4(x653,x654)+E(x651,x652)+E(x653,x652)+~P4(x652,x654)
% 60.74/60.82 [81]P7(x812,x811)+~P7(x812,x813)+~P5(x814,x812)+~P4(x814,x813)+P7(x811,x812)+~P7(x811,x813)+~P5(x814,x811)
% 60.74/60.82 [87]P7(x872,x871)+P7(x872,x873)+P7(x873,x871)+P7(x873,x872)+~P7(x872,x874)+~P7(x873,x874)+~P4(x875,x872)+~P4(x875,x873)+P7(x871,x872)+P7(x871,x873)+~P7(x871,x874)+~P4(x875,x871)
% 60.74/60.82 %EqnAxiom
% 60.74/60.82 [1]E(x11,x11)
% 60.74/60.82 [2]E(x22,x21)+~E(x21,x22)
% 60.74/60.82 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 60.74/60.82 [4]~E(x41,x42)+E(f8(x41),f8(x42))
% 60.74/60.82 [5]~E(x51,x52)+E(f17(x51,x53),f17(x52,x53))
% 60.74/60.82 [6]~E(x61,x62)+E(f17(x63,x61),f17(x63,x62))
% 60.74/60.82 [7]~E(x71,x72)+E(f10(x71),f10(x72))
% 60.74/60.82 [8]~E(x81,x82)+E(f16(x81),f16(x82))
% 60.74/60.82 [9]~E(x91,x92)+E(f2(x91,x93),f2(x92,x93))
% 60.74/60.82 [10]~E(x101,x102)+E(f2(x103,x101),f2(x103,x102))
% 60.74/60.82 [11]~E(x111,x112)+E(f11(x111,x113),f11(x112,x113))
% 60.74/60.82 [12]~E(x121,x122)+E(f11(x123,x121),f11(x123,x122))
% 60.74/60.82 [13]~E(x131,x132)+E(f15(x131,x133,x134),f15(x132,x133,x134))
% 60.74/60.82 [14]~E(x141,x142)+E(f15(x143,x141,x144),f15(x143,x142,x144))
% 60.74/60.82 [15]~E(x151,x152)+E(f15(x153,x154,x151),f15(x153,x154,x152))
% 60.74/60.82 [16]~E(x161,x162)+E(f13(x161,x163,x164),f13(x162,x163,x164))
% 60.74/60.82 [17]~E(x171,x172)+E(f13(x173,x171,x174),f13(x173,x172,x174))
% 60.74/60.82 [18]~E(x181,x182)+E(f13(x183,x184,x181),f13(x183,x184,x182))
% 60.74/60.82 [19]~E(x191,x192)+E(f12(x191,x193),f12(x192,x193))
% 60.74/60.82 [20]~E(x201,x202)+E(f12(x203,x201),f12(x203,x202))
% 60.74/60.82 [21]~E(x211,x212)+E(f14(x211,x213),f14(x212,x213))
% 60.74/60.82 [22]~E(x221,x222)+E(f14(x223,x221),f14(x223,x222))
% 60.74/60.82 [23]~E(x231,x232)+E(f18(x231,x233),f18(x232,x233))
% 60.74/60.82 [24]~E(x241,x242)+E(f18(x243,x241),f18(x243,x242))
% 60.74/60.82 [25]~E(x251,x252)+E(f3(x251,x253),f3(x252,x253))
% 60.74/60.82 [26]~E(x261,x262)+E(f3(x263,x261),f3(x263,x262))
% 60.74/60.82 [27]~E(x271,x272)+E(f4(x271,x273),f4(x272,x273))
% 60.74/60.82 [28]~E(x281,x282)+E(f4(x283,x281),f4(x283,x282))
% 60.74/60.82 [29]~E(x291,x292)+E(f5(x291,x293),f5(x292,x293))
% 60.74/60.82 [30]~E(x301,x302)+E(f5(x303,x301),f5(x303,x302))
% 60.74/60.82 [31]~P1(x311)+P1(x312)+~E(x311,x312)
% 60.74/60.82 [32]P7(x322,x323)+~E(x321,x322)+~P7(x321,x323)
% 60.74/60.82 [33]P7(x333,x332)+~E(x331,x332)+~P7(x333,x331)
% 60.74/60.82 [34]P6(x342,x343,x344)+~E(x341,x342)+~P6(x341,x343,x344)
% 60.74/60.82 [35]P6(x353,x352,x354)+~E(x351,x352)+~P6(x353,x351,x354)
% 60.74/60.82 [36]P6(x363,x364,x362)+~E(x361,x362)+~P6(x363,x364,x361)
% 60.74/60.82 [37]P2(x372,x373)+~E(x371,x372)+~P2(x371,x373)
% 60.74/60.82 [38]P2(x383,x382)+~E(x381,x382)+~P2(x383,x381)
% 60.74/60.82 [39]P5(x392,x393)+~E(x391,x392)+~P5(x391,x393)
% 60.74/60.82 [40]P5(x403,x402)+~E(x401,x402)+~P5(x403,x401)
% 60.74/60.82 [41]P4(x412,x413)+~E(x411,x412)+~P4(x411,x413)
% 60.74/60.82 [42]P4(x423,x422)+~E(x421,x422)+~P4(x423,x421)
% 60.74/60.82 [43]~P3(x431)+P3(x432)+~E(x431,x432)
% 60.74/60.82
% 60.74/60.82 %-------------------------------------------
% 60.81/60.83 cnf(92,plain,
% 60.81/60.83 (~P5(x921,x922)+P5(x921,f17(x923,x922))),
% 60.81/60.83 inference(equality_inference,[],[62])).
% 60.81/60.83 cnf(93,plain,
% 60.81/60.83 (~P5(x931,x932)+P5(x931,f17(x932,x933))),
% 60.81/60.83 inference(equality_inference,[],[63])).
% 60.81/60.83 cnf(94,plain,
% 60.81/60.83 (~P5(x941,f17(x942,x943))+P5(x941,x943)+P5(x941,x942)),
% 60.81/60.83 inference(equality_inference,[],[66])).
% 60.81/60.83 cnf(95,plain,
% 60.81/60.83 (~P3(f17(x951,x952))+P6(x953,x951,x952)+~P4(x953,x951)+~P6(x954,x951,x952)),
% 60.81/60.83 inference(equality_inference,[],[84])).
% 60.81/60.83 cnf(96,plain,
% 60.81/60.83 (~P4(x961,f17(a6,a7))),
% 60.81/60.83 inference(scs_inference,[],[49,51])).
% 60.81/60.83 cnf(98,plain,
% 60.81/60.83 (P3(f17(a6,a7))),
% 60.81/60.83 inference(scs_inference,[],[49,51,50])).
% 60.81/60.83 cnf(100,plain,
% 60.81/60.83 (~P5(x1001,a6)+P5(x1001,a1)),
% 60.81/60.83 inference(scs_inference,[],[45,49,51,50,61])).
% 60.81/60.83 cnf(102,plain,
% 60.81/60.83 (~P5(x1021,f17(a6,a6))+P5(x1021,a1)),
% 60.81/60.83 inference(scs_inference,[],[45,49,51,50,61,94])).
% 60.81/60.83 cnf(115,plain,
% 60.81/60.83 (~P5(x1151,a7)+P5(x1151,a1)),
% 60.81/60.83 inference(scs_inference,[],[46,61])).
% 60.81/60.83 cnf(117,plain,
% 60.81/60.83 (~P5(x1171,f17(a7,a7))+P5(x1171,a1)),
% 60.81/60.83 inference(scs_inference,[],[46,61,94])).
% 60.81/60.83 cnf(119,plain,
% 60.81/60.83 (P7(a7,x1191)+P5(f11(x1191,a7),a1)),
% 60.81/60.83 inference(scs_inference,[],[46,61,94,60])).
% 60.81/60.83 cnf(134,plain,
% 60.81/60.83 (P6(a9,a6,x1341)+~E(a7,x1341)),
% 60.81/60.83 inference(scs_inference,[],[48,36])).
% 60.81/60.83 cnf(136,plain,
% 60.81/60.83 (P6(x1361,a6,a7)+~E(a9,x1361)),
% 60.81/60.83 inference(scs_inference,[],[45,48,36,33,34])).
% 60.81/60.83 cnf(137,plain,
% 60.81/60.83 (P2(f8(x1371),x1372)+~E(x1371,x1372)),
% 60.81/60.83 inference(scs_inference,[],[45,48,47,36,33,34,38])).
% 60.81/60.83 cnf(146,plain,
% 60.81/60.83 (P2(x1461,x1462)+~E(f8(x1462),x1461)),
% 60.81/60.83 inference(scs_inference,[],[47,37])).
% 60.81/60.83 cnf(149,plain,
% 60.81/60.83 (~P5(x1491,x1492)+~P5(x1491,f17(a6,a7))+~P6(x1493,x1492,f17(a6,a7))+~E(f8(x1494),x1495)),
% 60.81/60.83 inference(scs_inference,[],[46,96,47,37,82])).
% 60.81/60.83 cnf(152,plain,
% 60.81/60.83 (~P5(x1521,x1522)+~P6(x1524,x1522,f17(a6,a7))+~P5(x1521,f17(a6,a7))),
% 60.81/60.83 inference(equality_inference,[],[149])).
% 60.81/60.83 cnf(242,plain,
% 60.81/60.83 (~E(a1,f17(a6,a7))),
% 60.81/60.83 inference(scs_inference,[],[96,44,52,31])).
% 60.81/60.83 cnf(243,plain,
% 60.81/60.83 (~P5(f13(a1,a6,a7),a7)+~P5(f13(a1,a6,a7),a1)),
% 60.81/60.83 inference(scs_inference,[],[242,89])).
% 60.81/60.83 cnf(350,plain,
% 60.81/60.83 (P7(x3501,a1)+~P5(f11(a1,x3501),a6)),
% 60.81/60.83 inference(scs_inference,[],[100,71])).
% 60.81/60.83 cnf(534,plain,
% 60.81/60.83 (~P5(f13(a1,a6,a7),a7)),
% 60.81/60.83 inference(scs_inference,[],[115,243])).
% 60.81/60.83 cnf(539,plain,
% 60.81/60.83 (~P2(f13(a1,a6,a7),a7)),
% 60.81/60.83 inference(scs_inference,[],[534,55,75,56])).
% 60.81/60.83 cnf(541,plain,
% 60.81/60.83 (~P6(f13(a1,a6,a7),x5411,a7)),
% 60.81/60.83 inference(scs_inference,[],[534,55,75,56,74])).
% 60.81/60.83 cnf(543,plain,
% 60.81/60.83 (~P5(f13(a1,a6,a7),f17(a7,a7))),
% 60.81/60.83 inference(scs_inference,[],[534,55,75,56,74,94])).
% 60.81/60.83 cnf(545,plain,
% 60.81/60.83 (~E(a9,f13(a1,a6,a7))),
% 60.81/60.83 inference(scs_inference,[],[48,534,55,75,56,74,94,34])).
% 60.81/60.83 cnf(555,plain,
% 60.81/60.83 (~P6(f13(a1,a6,a7),f17(a7,a7),x5551)),
% 60.81/60.83 inference(scs_inference,[],[543,55,75])).
% 60.81/60.83 cnf(563,plain,
% 60.81/60.83 (~P5(x5631,x5632)+~P5(x5631,f17(a6,a7))+~P6(x5633,f17(a6,a7),x5632)),
% 60.81/60.83 inference(scs_inference,[],[96,543,55,75,56,74,94,83])).
% 60.81/60.83 cnf(617,plain,
% 60.81/60.83 (E(f8(f5(a6,a7)),f8(f17(a6,a7)))),
% 60.81/60.83 inference(scs_inference,[],[48,4,76])).
% 60.81/60.83 cnf(618,plain,
% 60.81/60.83 (P2(f8(f17(a6,a7)),f5(a6,a7))),
% 60.81/60.83 inference(scs_inference,[],[617,146])).
% 60.81/60.83 cnf(619,plain,
% 60.81/60.83 (E(f8(f17(a6,a7)),f8(f5(a6,a7)))),
% 60.81/60.83 inference(scs_inference,[],[617,146,2])).
% 60.81/60.83 cnf(626,plain,
% 60.81/60.83 (P2(f8(f5(a6,a7)),f17(a6,a7))),
% 60.81/60.83 inference(scs_inference,[],[619,146])).
% 60.81/60.83 cnf(684,plain,
% 60.81/60.83 (~E(f2(a1,f16(a1)),f16(a1))),
% 60.81/60.83 inference(scs_inference,[],[44,58,52])).
% 60.81/60.83 cnf(719,plain,
% 60.81/60.83 (P5(f8(f17(a6,a6)),a1)),
% 60.81/60.83 inference(scs_inference,[],[47,102,56])).
% 60.81/60.83 cnf(720,plain,
% 60.81/60.83 (P5(f8(f17(a6,a6)),f17(x7201,a1))),
% 60.81/60.83 inference(scs_inference,[],[719,92])).
% 60.81/60.83 cnf(722,plain,
% 60.81/60.83 (P5(f8(f17(a6,a6)),f17(a1,x7221))),
% 60.81/60.83 inference(scs_inference,[],[719,92,93])).
% 60.81/60.83 cnf(732,plain,
% 60.81/60.83 (P5(f8(f17(a6,a6)),f17(x7321,f17(x7322,a1)))),
% 60.81/60.83 inference(scs_inference,[],[720,92])).
% 60.81/60.83 cnf(734,plain,
% 60.81/60.83 (P5(f8(f17(a6,a6)),f17(f17(x7341,a1),x7342))),
% 60.81/60.83 inference(scs_inference,[],[720,92,93])).
% 60.81/60.83 cnf(745,plain,
% 60.81/60.83 (P5(f8(f17(a6,a6)),f17(x7451,f17(a1,x7452)))),
% 60.81/60.83 inference(scs_inference,[],[722,92])).
% 60.81/60.83 cnf(747,plain,
% 60.81/60.83 (P5(f8(f17(a6,a6)),f17(f17(a1,x7471),x7472))),
% 60.81/60.83 inference(scs_inference,[],[722,92,93])).
% 60.81/60.83 cnf(855,plain,
% 60.81/60.83 (P7(x8551,a1)+~E(f8(f17(a6,a6)),f11(a1,x8551))),
% 60.81/60.83 inference(scs_inference,[],[719,39,71])).
% 60.81/60.83 cnf(863,plain,
% 60.81/60.83 (P5(f8(f17(a7,a7)),a1)),
% 60.81/60.83 inference(scs_inference,[],[47,117,56])).
% 60.81/60.83 cnf(864,plain,
% 60.81/60.83 (P5(f8(f17(a7,a7)),f17(a1,x8641))),
% 60.81/60.83 inference(scs_inference,[],[863,93])).
% 60.81/60.83 cnf(866,plain,
% 60.81/60.83 (P5(f8(f17(a7,a7)),f17(x8661,a1))),
% 60.81/60.83 inference(scs_inference,[],[863,93,92])).
% 60.81/60.83 cnf(992,plain,
% 60.81/60.83 (P7(x9921,a1)+~E(f8(f17(a7,a7)),f11(a1,x9921))),
% 60.81/60.83 inference(scs_inference,[],[863,39,71])).
% 60.81/60.83 cnf(1092,plain,
% 60.81/60.83 (~P5(f8(f17(a6,a6)),f17(a6,a7))+~P6(x10921,a1,f17(a6,a7))),
% 60.81/60.83 inference(scs_inference,[],[719,96,82])).
% 60.81/60.83 cnf(1844,plain,
% 60.81/60.83 (~E(f11(a1,x18441),f8(f17(a6,a6)))+P7(x18441,a1)),
% 60.81/60.83 inference(scs_inference,[],[855,2])).
% 60.81/60.83 cnf(1940,plain,
% 60.81/60.83 (~E(f11(a1,x19401),f8(f17(a7,a7)))+P7(x19401,a1)),
% 60.81/60.83 inference(scs_inference,[],[992,2])).
% 60.81/60.83 cnf(2116,plain,
% 60.81/60.83 (P1(f11(a1,x21161))+~P7(f11(a1,x21161),f8(f17(a6,a6)))+P7(x21161,a1)),
% 60.81/60.83 inference(scs_inference,[],[1844,53])).
% 60.81/60.83 cnf(2526,plain,
% 60.81/60.83 (~E(f8(a7),f13(a1,a6,a7))),
% 60.81/60.83 inference(scs_inference,[],[539,47,37])).
% 60.81/60.83 cnf(3530,plain,
% 60.81/60.83 (~P5(f8(f17(a6,a6)),a6)+~P6(x35301,a1,f17(a6,a7))),
% 60.81/60.83 inference(scs_inference,[],[1092,93])).
% 60.81/60.83 cnf(3546,plain,
% 60.81/60.83 (~P6(x35461,a1,x35462)+~E(x35462,f17(a6,a7))+~P5(f8(f17(a6,a6)),a6)),
% 60.81/60.83 inference(scs_inference,[],[3530,36])).
% 60.81/60.83 cnf(4386,plain,
% 60.81/60.83 (~P4(f8(f17(a6,a7)),f5(a6,a7))),
% 60.81/60.83 inference(scs_inference,[],[618,57])).
% 60.81/60.83 cnf(4389,plain,
% 60.81/60.83 (~P4(f8(x43891),x43891)),
% 60.81/60.83 inference(scs_inference,[],[47,57])).
% 60.81/60.83 cnf(4391,plain,
% 60.81/60.83 (~P5(f8(f17(a6,a6)),f17(a6,a6))+~P6(x43911,a1,f17(a6,a6))),
% 60.81/60.83 inference(scs_inference,[],[719,47,57,82])).
% 60.81/60.83 cnf(4427,plain,
% 60.81/60.83 (~P5(f8(f17(a6,a6)),f17(a6,a6))+~P6(x44271,f17(a6,a6),a1)),
% 60.81/60.83 inference(scs_inference,[],[719,4389,83])).
% 60.81/60.83 cnf(4499,plain,
% 60.81/60.83 (~E(f17(a6,a7),a1)),
% 60.81/60.83 inference(scs_inference,[],[242,2])).
% 60.81/60.83 cnf(4500,plain,
% 60.81/60.83 (~P7(f17(a6,a7),a1)),
% 60.81/60.83 inference(scs_inference,[],[49,242,2,53])).
% 60.81/60.83 cnf(4502,plain,
% 60.81/60.83 (~E(a7,f17(a6,a7))),
% 60.81/60.83 inference(scs_inference,[],[46,49,242,2,53,32])).
% 60.81/60.83 cnf(4513,plain,
% 60.81/60.83 (~P5(f13(a7,a6,a7),a7)),
% 60.81/60.83 inference(scs_inference,[],[46,49,242,2,53,32,855,992,1844,1940,2116,89])).
% 60.81/60.83 cnf(4515,plain,
% 60.81/60.83 (P5(f13(a7,a6,a7),a6)),
% 60.81/60.83 inference(scs_inference,[],[46,49,242,2,53,32,855,992,1844,1940,2116,89,88])).
% 60.81/60.83 cnf(4517,plain,
% 60.81/60.83 (~P2(f13(a7,a6,a7),a7)),
% 60.81/60.83 inference(scs_inference,[],[46,49,242,2,53,32,855,992,1844,1940,2116,89,88,56])).
% 60.81/60.84 cnf(4519,plain,
% 60.81/60.84 (~P6(f13(a7,a6,a7),x45191,a7)),
% 60.81/60.84 inference(scs_inference,[],[46,49,242,2,53,32,855,992,1844,1940,2116,89,88,56,74])).
% 60.81/60.84 cnf(4521,plain,
% 60.81/60.84 (~P6(f13(a7,a6,a7),a7,x45211)),
% 60.81/60.84 inference(scs_inference,[],[46,49,242,2,53,32,855,992,1844,1940,2116,89,88,56,74,75])).
% 60.81/60.84 cnf(4529,plain,
% 60.81/60.84 (~E(a9,f13(a7,a6,a7))),
% 60.81/60.84 inference(scs_inference,[],[4519,136])).
% 60.81/60.84 cnf(4532,plain,
% 60.81/60.84 (P5(f13(a7,a6,a7),a1)),
% 60.81/60.84 inference(scs_inference,[],[45,545,4519,4515,136,2,61])).
% 60.81/60.84 cnf(4534,plain,
% 60.81/60.84 (~P5(f13(a7,a6,a7),f17(a7,a7))),
% 60.81/60.84 inference(scs_inference,[],[45,545,4519,4515,4513,136,2,61,94])).
% 60.81/60.84 cnf(4537,plain,
% 60.81/60.84 (~E(a6,f17(a6,a7))),
% 60.81/60.84 inference(scs_inference,[],[45,545,4500,4519,4515,4513,136,2,61,94,40,32])).
% 60.81/60.84 cnf(4538,plain,
% 60.81/60.84 (~P2(f13(a7,a6,a7),f17(a7,a7))),
% 60.81/60.84 inference(scs_inference,[],[45,545,4500,4519,4515,4513,136,2,61,94,40,32,56])).
% 60.81/60.84 cnf(4544,plain,
% 60.81/60.84 (P4(f13(a7,a6,a7),a6)+P2(f13(a7,a6,a7),a6)),
% 60.81/60.84 inference(scs_inference,[],[45,545,4500,4519,4515,4513,136,2,61,94,40,32,56,74,75,59])).
% 60.81/60.84 cnf(4562,plain,
% 60.81/60.84 (~E(f8(f17(a7,a7)),f13(a7,a6,a7))),
% 60.81/60.84 inference(scs_inference,[],[4538,146])).
% 60.81/60.84 cnf(4563,plain,
% 60.81/60.84 (~E(f17(a6,a7),a7)),
% 60.81/60.84 inference(scs_inference,[],[4502,4538,146,2])).
% 60.81/60.84 cnf(4564,plain,
% 60.81/60.84 (~P7(f17(a6,a7),a7)),
% 60.81/60.84 inference(scs_inference,[],[49,4502,4538,146,2,53])).
% 60.81/60.84 cnf(4566,plain,
% 60.81/60.84 (~P5(f13(a7,a6,a7),f17(f17(a7,a7),f17(a7,a7)))),
% 60.81/60.84 inference(scs_inference,[],[49,4502,4538,4534,146,2,53,94])).
% 60.81/60.84 cnf(4568,plain,
% 60.81/60.84 (~P5(f13(a6,a6,a7),a6)),
% 60.81/60.84 inference(scs_inference,[],[49,4502,4537,4538,4534,146,2,53,94,90])).
% 60.81/60.84 cnf(4570,plain,
% 60.81/60.84 (~E(a1,f17(a7,a7))),
% 60.81/60.84 inference(scs_inference,[],[49,4502,4537,4532,4538,4534,146,2,53,94,90,40])).
% 60.81/60.84 cnf(4572,plain,
% 60.81/60.84 (P5(f13(a6,a6,a7),a7)),
% 60.81/60.84 inference(scs_inference,[],[49,4502,4537,4532,4538,4534,4515,146,2,53,94,90,40,39,88])).
% 60.81/60.84 cnf(4575,plain,
% 60.81/60.84 (~P2(f13(a7,a6,a7),f17(f17(a7,a7),f17(a7,a7)))),
% 60.81/60.84 inference(scs_inference,[],[49,4502,4537,4532,4538,4534,4515,146,2,53,94,90,40,39,88,16,56])).
% 60.81/60.84 cnf(4581,plain,
% 60.81/60.84 (P5(f13(a6,a6,a7),a1)),
% 60.81/60.84 inference(scs_inference,[],[46,49,4502,4537,4532,4538,4534,4515,146,2,53,94,90,40,39,88,16,56,74,75,61])).
% 60.81/60.84 cnf(4591,plain,
% 60.81/60.84 (~P2(f13(a6,a6,a7),a6)),
% 60.81/60.84 inference(scs_inference,[],[4568,4517,146,56])).
% 60.81/60.84 cnf(4593,plain,
% 60.81/60.84 (~E(f17(a6,a7),a6)),
% 60.81/60.84 inference(scs_inference,[],[4537,4568,4517,146,56,2])).
% 60.81/60.84 cnf(4598,plain,
% 60.81/60.84 (~P7(f17(a6,a7),a6)),
% 60.81/60.84 inference(scs_inference,[],[49,4537,4568,4517,146,56,2,74,75,53])).
% 60.81/60.84 cnf(4600,plain,
% 60.81/60.84 (~P5(f13(a6,a6,a7),f17(a6,a6))),
% 60.81/60.84 inference(scs_inference,[],[49,4537,4568,4517,146,56,2,74,75,53,94])).
% 60.81/60.84 cnf(4604,plain,
% 60.81/60.84 (~E(a9,f13(a6,a6,a7))),
% 60.81/60.84 inference(scs_inference,[],[49,4537,4581,534,4568,4572,4517,146,56,2,74,75,53,94,40,39,136])).
% 60.81/60.84 cnf(4605,plain,
% 60.81/60.84 (~E(a6,a1)),
% 60.81/60.84 inference(scs_inference,[],[49,4537,4581,534,4568,4572,4517,146,56,2,74,75,53,94,40,39,136,16])).
% 60.81/60.84 cnf(4615,plain,
% 60.81/60.84 (~P2(f13(a6,a6,a7),f17(a6,a6))),
% 60.81/60.84 inference(scs_inference,[],[4600,4591,146,56])).
% 60.81/60.84 cnf(4622,plain,
% 60.81/60.84 (P1(a6)),
% 60.81/60.84 inference(scs_inference,[],[45,4529,4605,4600,4591,146,56,2,74,75,53])).
% 60.81/60.84 cnf(4624,plain,
% 60.81/60.84 (~P5(f13(a6,a6,a7),f17(f17(a6,a6),f17(a6,a6)))),
% 60.81/60.84 inference(scs_inference,[],[45,4529,4605,4600,4591,146,56,2,74,75,53,94])).
% 60.81/60.84 cnf(4626,plain,
% 60.81/60.84 (~E(a1,f17(a6,a6))),
% 60.81/60.84 inference(scs_inference,[],[45,4529,4581,4605,4600,4591,146,56,2,74,75,53,94,40])).
% 60.81/60.84 cnf(4639,plain,
% 60.81/60.84 (~P6(f13(a6,a6,a7),f17(f17(a6,a6),f17(a6,a6)),x46391)),
% 60.81/60.84 inference(scs_inference,[],[4604,4624,4615,56,146,74,2,75])).
% 60.81/60.84 cnf(4651,plain,
% 60.81/60.84 (~E(a6,f17(a7,a7))),
% 60.81/60.84 inference(scs_inference,[],[684,4534,4515,2,40])).
% 60.81/60.84 cnf(4660,plain,
% 60.81/60.84 (~P5(f13(a1,a6,a6),a6)+~P5(f13(a1,a6,a6),a1)),
% 60.81/60.84 inference(scs_inference,[],[2526,4626,2,89])).
% 60.81/60.84 cnf(4662,plain,
% 60.81/60.84 (~P5(f13(a1,a6,a6),f17(a6,a6))+~P5(f13(a1,a6,a6),a1)),
% 60.81/60.84 inference(scs_inference,[],[2526,4626,2,89,94])).
% 60.81/60.84 cnf(4670,plain,
% 60.81/60.84 (~E(f8(a6),f13(a1,a6,a6))+~P5(f13(a1,a6,a6),a1)),
% 60.81/60.84 inference(scs_inference,[],[2526,4626,2,89,94,88,56,74,146])).
% 60.81/60.84 cnf(4671,plain,
% 60.81/60.84 (~P6(f13(a1,a6,a6),a6,x46711)+~P5(f13(a1,a6,a6),a1)),
% 60.81/60.84 inference(scs_inference,[],[2526,4626,2,89,94,88,56,74,146,75])).
% 60.81/60.84 cnf(4759,plain,
% 60.81/60.84 (~P5(f8(f17(a6,a7)),x47591)+~P5(f8(f17(a6,a7)),f5(a6,a7))+~P6(x47592,x47591,f5(a6,a7))),
% 60.81/60.84 inference(scs_inference,[],[4502,4639,4386,4570,4651,2,82])).
% 60.81/60.84 cnf(4774,plain,
% 60.81/60.84 (P5(f13(a1,a6,a6),a6)+P5(f13(a1,a6,a6),a1)),
% 60.81/60.84 inference(scs_inference,[],[4521,4604,4626,4562,2,53,35,88])).
% 60.81/60.84 cnf(4804,plain,
% 60.81/60.84 (~P4(f13(a1,a6,a7),a6)),
% 60.81/60.84 inference(scs_inference,[],[48,541,98,95])).
% 60.81/60.84 cnf(4812,plain,
% 60.81/60.84 (~P4(f13(a7,a6,a7),a6)),
% 60.81/60.84 inference(scs_inference,[],[48,4519,98,95])).
% 60.81/60.84 cnf(4815,plain,
% 60.81/60.84 (~P6(x48151,a1,a6)),
% 60.81/60.84 inference(scs_inference,[],[48,4532,4519,4515,98,95,82])).
% 60.81/60.84 cnf(4819,plain,
% 60.81/60.84 (~E(a7,a1)),
% 60.81/60.84 inference(scs_inference,[],[48,4532,4519,4515,98,95,82,83,134])).
% 60.81/60.84 cnf(4820,plain,
% 60.81/60.84 (P2(f13(a7,a6,a7),a6)),
% 60.81/60.84 inference(scs_inference,[],[48,4532,4519,4515,98,95,82,83,134,4544])).
% 60.81/60.84 cnf(4823,plain,
% 60.81/60.84 (P1(a7)),
% 60.81/60.84 inference(scs_inference,[],[46,48,4532,4519,4515,98,95,82,83,134,4544,2,42,53])).
% 60.81/60.84 cnf(5367,plain,
% 60.81/60.84 (~P5(f8(f17(a6,a6)),f17(a6,a6))+~P6(x53671,f17(a6,a6),f17(x53672,a1))),
% 60.81/60.84 inference(scs_inference,[],[720,4389,83])).
% 60.81/60.84 cnf(5371,plain,
% 60.81/60.84 (~P5(f8(f17(a6,a6)),f17(a6,a6))+~P6(x53711,f17(x53712,a1),f17(a6,a6))),
% 60.81/60.84 inference(scs_inference,[],[720,4389,82])).
% 60.81/60.84 cnf(5545,plain,
% 60.81/60.84 (~P5(f8(f17(a6,a6)),f17(a6,a6))+~P6(x55451,f17(a6,a6),f17(a1,x55452))),
% 60.81/60.84 inference(scs_inference,[],[722,4389,83])).
% 60.81/60.84 cnf(5551,plain,
% 60.81/60.84 (~P5(f8(f17(a6,a6)),f17(a6,a6))+~P6(x55511,f17(a1,x55512),f17(a6,a6))),
% 60.81/60.84 inference(scs_inference,[],[722,4389,82])).
% 60.81/60.84 cnf(5719,plain,
% 60.81/60.84 (~P5(f8(f17(a6,a6)),f17(a6,a6))+~P6(x57191,f17(a6,a6),f17(x57192,f17(x57193,a1)))),
% 60.81/60.84 inference(scs_inference,[],[732,4389,83])).
% 60.81/60.84 cnf(5723,plain,
% 60.81/60.84 (~P5(f8(f17(a6,a6)),f17(a6,a6))+~P6(x57231,f17(x57232,f17(x57233,a1)),f17(a6,a6))),
% 60.81/60.84 inference(scs_inference,[],[732,4389,82])).
% 60.81/60.84 cnf(5728,plain,
% 60.81/60.84 (~P5(f8(f17(a6,a7)),x57281)+~P5(f8(f17(a6,a7)),f5(a6,a7))+~P6(x57282,f5(a6,a7),x57281)),
% 60.81/60.84 inference(scs_inference,[],[4804,555,4386,83])).
% 60.81/60.84 cnf(5819,plain,
% 60.81/60.84 (P5(f13(a1,a6,a6),a1)),
% 60.81/60.84 inference(scs_inference,[],[4774,100])).
% 60.81/60.84 cnf(5820,plain,
% 60.81/60.84 (~P5(f13(a1,a6,a6),a6)),
% 60.81/60.84 inference(scs_inference,[],[5819,4660])).
% 60.81/60.84 cnf(5821,plain,
% 60.81/60.84 (~P5(f13(a1,a6,a6),f17(a6,a6))),
% 60.81/60.84 inference(scs_inference,[],[5819,4662])).
% 60.81/60.84 cnf(5824,plain,
% 60.81/60.84 (~E(f8(a6),f13(a1,a6,a6))),
% 60.81/60.84 inference(scs_inference,[],[5819,4670])).
% 60.81/60.84 cnf(5825,plain,
% 60.81/60.84 (~P6(f13(a1,a6,a6),a6,x58251)),
% 60.81/60.84 inference(scs_inference,[],[5819,4671])).
% 60.81/60.84 cnf(5844,plain,
% 60.81/60.84 (~P5(f13(a1,a6,a6),f17(f17(a6,a6),f17(a6,a6)))),
% 60.81/60.84 inference(scs_inference,[],[5825,5821,5824,56,75,136,146,2,74,94])).
% 60.81/60.84 cnf(5935,plain,
% 60.81/60.84 (~P5(f8(f17(a6,a6)),f17(a6,a6))+~P6(x59351,f17(f17(x59352,a1),x59353),f17(a6,a6))),
% 60.81/60.84 inference(scs_inference,[],[734,4389,82])).
% 60.81/60.84 cnf(5960,plain,
% 60.81/60.84 (~P5(f8(f17(a6,a6)),f17(a6,a6))+~P6(x59601,f17(a6,a6),f17(f17(x59602,a1),x59603))),
% 60.81/60.84 inference(scs_inference,[],[734,4389,83])).
% 60.81/60.84 cnf(6102,plain,
% 60.81/60.84 (~P5(f8(f17(a6,a6)),f17(a6,a6))+~P6(x61021,f17(x61022,f17(a1,x61023)),f17(a6,a6))),
% 60.81/60.84 inference(scs_inference,[],[745,4389,82])).
% 60.81/60.84 cnf(6127,plain,
% 60.81/60.84 (~P5(f8(f17(a6,a6)),f17(a6,a6))+~P6(x61271,f17(a6,a6),f17(x61272,f17(a1,x61273)))),
% 60.81/60.84 inference(scs_inference,[],[745,4389,83])).
% 60.81/60.84 cnf(6283,plain,
% 60.81/60.84 (~P5(f8(f17(a6,a6)),f17(a6,a6))+~P6(x62831,f17(f17(a1,x62832),x62833),f17(a6,a6))),
% 60.81/60.84 inference(scs_inference,[],[747,4389,82])).
% 60.81/60.84 cnf(6313,plain,
% 60.81/60.84 (~P5(f8(f17(a6,a6)),f17(a6,a6))+~P6(x63131,f17(a6,a6),f17(f17(a1,x63132),x63133))),
% 60.81/60.84 inference(scs_inference,[],[747,4389,83])).
% 60.81/60.84 cnf(6435,plain,
% 60.81/60.84 (~P5(f8(f17(a7,a7)),f17(a7,a7))+~P6(x64351,a1,f17(a7,a7))),
% 60.81/60.84 inference(scs_inference,[],[863,4389,82])).
% 60.81/60.84 cnf(6574,plain,
% 60.81/60.84 (~P5(f8(f17(a7,a7)),f17(a7,a7))+~P6(x65741,f17(a7,a7),f17(a1,x65742))),
% 60.81/60.84 inference(scs_inference,[],[864,4389,83])).
% 60.81/60.84 cnf(6744,plain,
% 60.81/60.84 (~P5(f8(f17(a7,a7)),f17(a7,a7))+~P6(x67441,f17(a7,a7),f17(x67442,a1))),
% 60.81/60.84 inference(scs_inference,[],[866,4389,83])).
% 60.81/60.84 cnf(6748,plain,
% 60.81/60.84 (~P5(f8(f17(a7,a7)),f17(a7,a7))+~P6(x67481,f17(x67482,a1),f17(a7,a7))),
% 60.81/60.84 inference(scs_inference,[],[866,4389,82])).
% 60.81/60.84 cnf(6768,plain,
% 60.81/60.84 (~P4(f8(x67681),x67682)+~E(x67682,x67681)),
% 60.81/60.84 inference(scs_inference,[],[4389,42])).
% 60.81/60.84 cnf(6824,plain,
% 60.81/60.84 (~P5(f11(a1,f17(a6,a7)),a6)),
% 60.81/60.84 inference(scs_inference,[],[4500,350])).
% 60.81/60.84 cnf(6826,plain,
% 60.81/60.84 (E(f5(a6,a7),f17(a6,a7))),
% 60.81/60.84 inference(scs_inference,[],[4500,48,350,76])).
% 60.81/60.84 cnf(6833,plain,
% 60.81/60.84 (P4(f16(a1),a1)),
% 60.81/60.84 inference(scs_inference,[],[44,4500,48,350,76,13,14,15,17,18,52])).
% 60.81/60.84 cnf(6837,plain,
% 60.81/60.84 (P5(f11(a7,f17(a6,a7)),f17(a6,a7))),
% 60.81/60.84 inference(scs_inference,[],[44,4564,4500,48,350,76,13,14,15,17,18,52,64,60])).
% 60.81/60.84 cnf(6839,plain,
% 60.81/60.84 (~P5(f11(a7,f17(a6,a7)),a7)),
% 60.81/60.84 inference(scs_inference,[],[44,4564,4500,48,350,76,13,14,15,17,18,52,64,60,71])).
% 60.81/60.84 cnf(6844,plain,
% 60.81/60.84 (P5(a9,a7)),
% 60.81/60.84 inference(scs_inference,[],[44,4566,4564,4500,48,350,76,13,14,15,17,18,52,64,60,71,55,5,74])).
% 60.81/60.84 cnf(6850,plain,
% 60.81/60.84 (P5(f13(a6,a6,a7),f17(x68501,a1))),
% 60.81/60.84 inference(scs_inference,[],[44,4566,4564,4581,4500,48,350,76,13,14,15,17,18,52,64,60,71,55,5,74,6,16,57,92])).
% 60.81/60.84 cnf(6854,plain,
% 60.81/60.84 (P5(a9,a6)),
% 60.81/60.84 inference(scs_inference,[],[44,4566,4564,4820,4581,4500,48,350,76,13,14,15,17,18,52,64,60,71,55,5,74,6,16,57,92,78,75])).
% 60.81/60.84 cnf(6858,plain,
% 60.81/60.84 (P5(f13(a6,a6,a7),f17(a1,x68581))),
% 60.81/60.84 inference(scs_inference,[],[44,4566,4564,4820,4581,626,4500,48,350,76,13,14,15,17,18,52,64,60,71,55,5,74,6,16,57,92,78,75,56,93])).
% 60.81/60.84 cnf(6860,plain,
% 60.81/60.84 (E(f17(a6,a7),f5(a6,a7))),
% 60.81/60.84 inference(scs_inference,[],[44,4566,4564,4820,4581,626,4500,48,350,76,13,14,15,17,18,52,64,60,71,55,5,74,6,16,57,92,78,75,56,93,2])).
% 60.81/60.84 cnf(6865,plain,
% 60.81/60.84 (P5(f13(a7,a6,a7),f12(f13(a7,a6,a7),a6))),
% 60.81/60.84 inference(scs_inference,[],[44,4566,4564,4820,4624,4581,626,4812,4515,4500,48,350,76,13,14,15,17,18,52,64,60,71,55,5,74,6,16,57,92,78,75,56,93,2,62,63,67])).
% 60.81/60.84 cnf(6867,plain,
% 60.81/60.84 (P5(f13(a7,a6,a7),f14(f13(a7,a6,a7),a6))),
% 60.81/60.84 inference(scs_inference,[],[44,4566,4564,4820,4624,4581,626,4812,4515,4500,48,350,76,13,14,15,17,18,52,64,60,71,55,5,74,6,16,57,92,78,75,56,93,2,62,63,67,68])).
% 60.81/60.84 cnf(6869,plain,
% 60.81/60.84 (P7(f12(f13(a7,a6,a7),a6),a6)),
% 60.81/60.84 inference(scs_inference,[],[44,4566,4564,4820,4624,4581,626,4812,4515,4500,48,350,76,13,14,15,17,18,52,64,60,71,55,5,74,6,16,57,92,78,75,56,93,2,62,63,67,68,69])).
% 60.81/60.84 cnf(6871,plain,
% 60.81/60.84 (P7(f14(f13(a7,a6,a7),a6),a6)),
% 60.81/60.84 inference(scs_inference,[],[44,4566,4564,4820,4624,4581,626,4812,4515,4500,48,350,76,13,14,15,17,18,52,64,60,71,55,5,74,6,16,57,92,78,75,56,93,2,62,63,67,68,69,70])).
% 60.81/60.84 cnf(6879,plain,
% 60.81/60.84 (~P5(f11(a1,f17(a6,a7)),f17(a6,a6))),
% 60.81/60.84 inference(scs_inference,[],[44,4566,4564,4820,4624,4581,626,4812,4515,98,4500,48,350,76,13,14,15,17,18,52,64,60,71,55,5,74,6,16,57,92,78,75,56,93,2,62,63,67,68,69,70,79,80,3,43,94])).
% 60.81/60.84 cnf(6889,plain,
% 60.81/60.84 (P2(f11(a7,f17(a6,a7)),f17(a6,a7))),
% 60.81/60.84 inference(scs_inference,[],[44,4575,5820,4566,4564,4820,4624,4521,4581,626,4812,4532,96,4515,98,4500,48,350,76,13,14,15,17,18,52,64,60,71,55,5,74,6,16,57,92,78,75,56,93,2,62,63,67,68,69,70,79,80,3,43,94,61,38,39,33,35,40,59])).
% 60.81/60.84 cnf(6890,plain,
% 60.81/60.84 (~P4(x68901,f17(a6,a7))),
% 60.81/60.84 inference(rename_variables,[],[96])).
% 60.81/60.84 cnf(6892,plain,
% 60.81/60.84 (~P1(f5(a6,a7))),
% 60.81/60.84 inference(scs_inference,[],[44,4575,5820,4566,4564,4820,4624,4521,4581,626,49,4812,4532,96,4515,98,4500,48,350,76,13,14,15,17,18,52,64,60,71,55,5,74,6,16,57,92,78,75,56,93,2,62,63,67,68,69,70,79,80,3,43,94,61,38,39,33,35,40,59,31])).
% 60.81/60.84 cnf(6893,plain,
% 60.81/60.84 (~P7(f5(a6,a7),a7)),
% 60.81/60.84 inference(scs_inference,[],[44,4575,5820,4566,4564,4820,4624,4521,4581,626,49,4812,4532,96,4515,98,4500,48,350,76,13,14,15,17,18,52,64,60,71,55,5,74,6,16,57,92,78,75,56,93,2,62,63,67,68,69,70,79,80,3,43,94,61,38,39,33,35,40,59,31,32])).
% 60.81/60.84 cnf(6894,plain,
% 60.81/60.84 (~E(f17(a6,a7),f17(a7,a7))),
% 60.81/60.84 inference(scs_inference,[],[44,4575,5820,4566,4564,4820,4624,4521,4581,626,49,4812,4532,96,4515,98,4500,48,350,76,13,14,15,17,18,52,64,60,71,55,5,74,6,16,57,92,78,75,56,93,2,62,63,67,68,69,70,79,80,3,43,94,61,38,39,33,35,40,59,31,32,66])).
% 60.81/60.84 cnf(6897,plain,
% 60.81/60.84 (~P6(x68971,a1,a6)),
% 60.81/60.84 inference(rename_variables,[],[4815])).
% 60.81/60.84 cnf(6899,plain,
% 60.81/60.84 (P5(f15(f13(a7,a6,a7),a1,a6),a1)),
% 60.81/60.84 inference(scs_inference,[],[44,4575,5820,4566,4564,4820,4624,4521,4581,626,49,4812,4532,96,4515,98,4500,48,4815,6897,350,76,13,14,15,17,18,52,64,60,71,55,5,74,6,16,57,92,78,75,56,93,2,62,63,67,68,69,70,79,80,3,43,94,61,38,39,33,35,40,59,31,32,66,85,86])).
% 60.81/60.84 cnf(6902,plain,
% 60.81/60.84 (~P6(x69021,a6,a6)),
% 60.81/60.84 inference(scs_inference,[],[44,4575,5820,4566,4564,4820,4624,4521,4581,626,49,4812,4532,96,4515,98,4500,48,4815,6897,350,76,13,14,15,17,18,52,64,60,71,55,5,74,6,16,57,92,78,75,56,93,2,62,63,67,68,69,70,79,80,3,43,94,61,38,39,33,35,40,59,31,32,66,85,86,83])).
% 60.81/60.84 cnf(6904,plain,
% 60.81/60.84 (~P6(x69041,f17(a6,a7),f17(a6,a7))),
% 60.81/60.84 inference(scs_inference,[],[44,4575,5820,4566,4564,4820,4624,4521,4581,626,49,4812,4532,96,6890,4515,98,4500,48,4815,6897,350,76,13,14,15,17,18,52,64,60,71,55,5,74,6,16,57,92,78,75,56,93,2,62,63,67,68,69,70,79,80,3,43,94,61,38,39,33,35,40,59,31,32,66,85,86,83,82])).
% 60.81/60.84 cnf(6907,plain,
% 60.81/60.84 (P5(a9,a1)),
% 60.81/60.84 inference(scs_inference,[],[44,4575,5820,4566,4564,4820,4624,4521,4581,626,49,4812,4532,96,6890,4515,98,4500,48,4815,6897,350,76,13,14,15,17,18,52,64,60,71,55,5,74,6,16,57,92,78,75,56,93,2,62,63,67,68,69,70,79,80,3,43,94,61,38,39,33,35,40,59,31,32,66,85,86,83,82,100])).
% 60.81/60.84 cnf(6927,plain,
% 60.81/60.84 (~P4(x69271,f5(a6,a7))),
% 60.81/60.84 inference(scs_inference,[],[44,4575,5820,4566,4564,4820,4624,4521,4581,626,49,4812,4532,96,6890,4515,98,4500,48,4815,6897,350,76,13,14,15,17,18,52,64,60,71,55,5,74,6,16,57,92,78,75,56,93,2,62,63,67,68,69,70,79,80,3,43,94,61,38,39,33,35,40,59,31,32,66,85,86,83,82,100,7,8,9,10,11,12,19,20,21,22,23,24,25,26,27,28,29,30,54])).
% 60.81/60.84 cnf(6933,plain,
% 60.81/60.84 (~P4(f15(f13(a7,a6,a7),a6,a6),a6)),
% 60.81/60.84 inference(scs_inference,[],[44,4575,4819,5820,4566,4564,4820,4624,4521,4581,626,49,47,4812,4532,96,6890,4515,98,4500,48,4815,6897,350,76,13,14,15,17,18,52,64,60,71,55,5,74,6,16,57,92,78,75,56,93,2,62,63,67,68,69,70,79,80,3,43,94,61,38,39,33,35,40,59,31,32,66,85,86,83,82,100,7,8,9,10,11,12,19,20,21,22,23,24,25,26,27,28,29,30,54,77,37,91])).
% 60.81/60.84 cnf(6940,plain,
% 60.81/60.84 (P5(f11(a7,f5(a6,a7)),f5(a6,a7))),
% 60.81/60.84 inference(scs_inference,[],[4622,6893,52,60])).
% 60.81/60.84 cnf(6944,plain,
% 60.81/60.84 (~P5(f11(a7,f5(a6,a7)),a7)),
% 60.81/60.84 inference(scs_inference,[],[4622,6893,6879,52,60,55,71])).
% 60.81/60.84 cnf(6948,plain,
% 60.81/60.84 (P5(a9,f17(x69481,a1))),
% 60.81/60.84 inference(scs_inference,[],[6907,4622,6893,6879,52,60,55,71,57,92])).
% 60.81/60.84 cnf(6950,plain,
% 60.81/60.84 (P5(f8(x69501),x69501)),
% 60.81/60.84 inference(scs_inference,[],[6907,4622,6893,6879,47,52,60,55,71,57,92,56])).
% 60.81/60.84 cnf(6952,plain,
% 60.81/60.84 (P5(a9,f17(a1,x69521))),
% 60.81/60.84 inference(scs_inference,[],[6907,4622,6893,6879,47,52,60,55,71,57,92,56,93])).
% 60.81/60.84 cnf(6955,plain,
% 60.81/60.84 (~P4(f8(x69551),x69551)),
% 60.81/60.84 inference(rename_variables,[],[4389])).
% 60.81/60.84 cnf(6960,plain,
% 60.81/60.84 (~P6(x69601,f17(a6,a7),f5(a6,a7))),
% 60.81/60.84 inference(scs_inference,[],[6907,4622,6904,6826,6893,6879,47,4389,6955,52,60,55,71,57,92,56,93,68,67,36])).
% 60.81/60.84 cnf(6969,plain,
% 60.81/60.84 (P5(f11(a7,f17(a6,a7)),a6)),
% 60.81/60.84 inference(scs_inference,[],[6907,4622,6927,6904,6894,6860,6826,6833,6893,6879,6837,6839,6933,47,4389,6955,52,60,55,71,57,92,56,93,68,67,36,62,63,3,41,42,94])).
% 60.81/60.84 cnf(6971,plain,
% 60.81/60.84 (~P7(a1,a6)),
% 60.81/60.84 inference(scs_inference,[],[6907,4622,6927,6904,6894,6860,6826,6833,6893,6879,6837,6839,6933,5820,5819,47,4389,6955,52,60,55,71,57,92,56,93,68,67,36,62,63,3,41,42,94,61])).
% 60.81/60.84 cnf(6975,plain,
% 60.81/60.84 (~P7(f5(a6,a7),a6)),
% 60.81/60.84 inference(scs_inference,[],[6907,4622,6927,6904,6894,6860,6826,6833,6893,6879,6889,6837,6839,6933,4598,5820,5819,47,4389,6955,52,60,55,71,57,92,56,93,68,67,36,62,63,3,41,42,94,61,38,40,32])).
% 60.81/60.84 cnf(6977,plain,
% 60.81/60.84 (~E(a6,f5(a6,a7))),
% 60.81/60.84 inference(scs_inference,[],[6907,4622,6927,6904,6894,6892,6860,6826,6833,6893,6879,6889,6837,6839,6933,4598,5820,5819,47,4389,6955,52,60,55,71,57,92,56,93,68,67,36,62,63,3,41,42,94,61,38,40,32,35,31])).
% 60.81/60.84 cnf(6980,plain,
% 60.81/60.84 (P5(f15(a9,a6,a6),a6)),
% 60.81/60.84 inference(scs_inference,[],[6907,6902,4622,6854,6927,6904,6894,6892,6860,6826,6833,6893,6879,6889,6837,6865,6839,6933,4598,5820,4513,5819,47,4389,6955,52,60,55,71,57,92,56,93,68,67,36,62,63,3,41,42,94,61,38,40,32,35,31,66,85])).
% 60.81/60.84 cnf(6981,plain,
% 60.81/60.84 (~P6(x69811,a6,a6)),
% 60.81/60.84 inference(rename_variables,[],[6902])).
% 60.81/60.84 cnf(6983,plain,
% 60.81/60.84 (P5(f15(f13(a7,a6,a7),a6,a6),a6)),
% 60.81/60.84 inference(scs_inference,[],[6907,6902,6981,4622,6854,6927,6904,6894,6892,6860,6826,6833,6893,6879,6889,6837,6865,6839,6933,4598,5820,4513,5819,47,4389,6955,4515,52,60,55,71,57,92,56,93,68,67,36,62,63,3,41,42,94,61,38,40,32,35,31,66,85,86])).
% 60.81/60.84 cnf(6984,plain,
% 60.81/60.84 (~P6(x69841,a6,a6)),
% 60.81/60.84 inference(rename_variables,[],[6902])).
% 60.81/60.84 cnf(6986,plain,
% 60.81/60.84 (P6(f16(a6),a6,a7)),
% 60.81/60.84 inference(scs_inference,[],[6907,6902,6981,4622,6854,6927,6904,6894,6892,6860,6826,6833,6893,6879,6889,6837,6865,6839,6933,4598,5820,4513,5819,47,4389,6955,98,4515,48,52,60,55,71,57,92,56,93,68,67,36,62,63,3,41,42,94,61,38,40,32,35,31,66,85,86,95])).
% 60.81/60.84 cnf(6988,plain,
% 60.81/60.84 (P4(a9,a6)),
% 60.81/60.84 inference(scs_inference,[],[6907,6902,6981,4622,6844,6854,6927,6904,6894,6892,6860,6826,6833,6893,6879,6889,6837,6865,6839,6933,4598,5820,4513,5819,47,4389,6955,98,4515,48,52,60,55,71,57,92,56,93,68,67,36,62,63,3,41,42,94,61,38,40,32,35,31,66,85,86,95,83])).
% 60.81/60.84 cnf(6990,plain,
% 60.81/60.84 (P4(a9,a7)),
% 60.81/60.84 inference(scs_inference,[],[6907,6902,6981,4622,6844,6854,6927,6904,6894,6892,6860,6826,6833,6893,6879,6889,6837,6865,6839,6933,4598,5820,4513,5819,47,4389,6955,98,4515,48,52,60,55,71,57,92,56,93,68,67,36,62,63,3,41,42,94,61,38,40,32,35,31,66,85,86,95,83,82])).
% 60.81/60.84 cnf(6992,plain,
% 60.81/60.84 (~P4(f15(a9,a6,a6),a6)),
% 60.81/60.84 inference(scs_inference,[],[6907,6902,6981,6984,4622,6844,6854,6927,6904,6894,6892,6860,6826,6833,6893,6879,6889,6837,6865,6839,6933,4598,5820,4513,5819,47,4389,6955,98,4515,48,52,60,55,71,57,92,56,93,68,67,36,62,63,3,41,42,94,61,38,40,32,35,31,66,85,86,95,83,82,91])).
% 60.81/60.84 cnf(6995,plain,
% 60.81/60.84 (~P6(x69951,a1,f17(a6,a6))),
% 60.81/60.84 inference(scs_inference,[],[6907,6902,6981,6984,4622,6844,6854,6927,6904,6894,6892,6860,6826,6833,6893,6879,6889,6837,6865,6839,6933,4598,5820,4513,5819,47,4389,6955,98,4515,48,52,60,55,71,57,92,56,93,68,67,36,62,63,3,41,42,94,61,38,40,32,35,31,66,85,86,95,83,82,91,4391])).
% 60.81/60.84 cnf(6997,plain,
% 60.81/60.84 (~P6(x69971,f17(a6,a6),f17(x69972,a1))),
% 60.81/60.84 inference(scs_inference,[],[6907,6902,6981,6984,4622,6844,6854,6927,6904,6894,6892,6860,6826,6833,6893,6879,6889,6837,6865,6839,6933,4598,5820,4513,5819,47,4389,6955,98,4515,48,52,60,55,71,57,92,56,93,68,67,36,62,63,3,41,42,94,61,38,40,32,35,31,66,85,86,95,83,82,91,4391,4427,5367])).
% 60.81/60.84 cnf(6998,plain,
% 60.81/60.84 (~P6(x69981,f17(x69982,a1),f17(a6,a6))),
% 60.81/60.84 inference(scs_inference,[],[6907,6902,6981,6984,4622,6844,6854,6927,6904,6894,6892,6860,6826,6833,6893,6879,6889,6837,6865,6839,6933,4598,5820,4513,5819,47,4389,6955,98,4515,48,52,60,55,71,57,92,56,93,68,67,36,62,63,3,41,42,94,61,38,40,32,35,31,66,85,86,95,83,82,91,4391,4427,5367,5371])).
% 60.81/60.84 cnf(6999,plain,
% 60.81/60.84 (~P6(x69991,f17(a6,a6),f17(a1,x69992))),
% 60.81/60.84 inference(scs_inference,[],[6907,6902,6981,6984,4622,6844,6854,6927,6904,6894,6892,6860,6826,6833,6893,6879,6889,6837,6865,6839,6933,4598,5820,4513,5819,47,4389,6955,98,4515,48,52,60,55,71,57,92,56,93,68,67,36,62,63,3,41,42,94,61,38,40,32,35,31,66,85,86,95,83,82,91,4391,4427,5367,5371,5545])).
% 60.81/60.84 cnf(7000,plain,
% 60.81/60.84 (~P6(x70001,f17(a1,x70002),f17(a6,a6))),
% 60.81/60.84 inference(scs_inference,[],[6907,6902,6981,6984,4622,6844,6854,6927,6904,6894,6892,6860,6826,6833,6893,6879,6889,6837,6865,6839,6933,4598,5820,4513,5819,47,4389,6955,98,4515,48,52,60,55,71,57,92,56,93,68,67,36,62,63,3,41,42,94,61,38,40,32,35,31,66,85,86,95,83,82,91,4391,4427,5367,5371,5545,5551])).
% 60.81/60.84 cnf(7011,plain,
% 60.81/60.84 (P5(f11(a7,f17(a6,a7)),a1)),
% 60.81/60.84 inference(scs_inference,[],[6907,6902,6981,6984,4622,6844,6854,6927,6904,6894,6892,6860,6826,6833,6893,6879,6889,6837,6865,6839,6933,4598,5820,4513,5819,47,4389,6955,98,4515,48,52,60,55,71,57,92,56,93,68,67,36,62,63,3,41,42,94,61,38,40,32,35,31,66,85,86,95,83,82,91,4391,4427,5367,5371,5545,5551,5719,5723,5935,5960,6102,6127,6283,6313,58,100])).
% 60.81/60.84 cnf(7013,plain,
% 60.81/60.84 (P4(f2(a6,f16(a6)),a6)),
% 60.81/60.84 inference(scs_inference,[],[6907,6902,6981,6984,4622,6844,6854,6927,6904,6894,6892,6860,6826,6833,6893,6879,6889,6837,6865,6839,6933,4598,5820,4513,5819,47,4389,6955,98,4515,48,52,60,55,71,57,92,56,93,68,67,36,62,63,3,41,42,94,61,38,40,32,35,31,66,85,86,95,83,82,91,4391,4427,5367,5371,5545,5551,5719,5723,5935,5960,6102,6127,6283,6313,58,100,64])).
% 60.81/60.84 cnf(7015,plain,
% 60.81/60.84 (P5(f16(a6),a7)),
% 60.81/60.84 inference(scs_inference,[],[6907,6902,6981,6984,4622,6844,6854,6927,6904,6894,6892,6860,6826,6833,6893,6879,6889,6837,6865,6839,6933,4598,5820,4513,5819,47,4389,6955,98,4515,48,52,60,55,71,57,92,56,93,68,67,36,62,63,3,41,42,94,61,38,40,32,35,31,66,85,86,95,83,82,91,4391,4427,5367,5371,5545,5551,5719,5723,5935,5960,6102,6127,6283,6313,58,100,64,74])).
% 60.81/60.84 cnf(7017,plain,
% 60.81/60.84 (P5(f16(a6),a6)),
% 60.81/60.84 inference(scs_inference,[],[6907,6902,6981,6984,4622,6844,6854,6927,6904,6894,6892,6860,6826,6833,6893,6879,6889,6837,6865,6839,6933,4598,5820,4513,5819,47,4389,6955,98,4515,48,52,60,55,71,57,92,56,93,68,67,36,62,63,3,41,42,94,61,38,40,32,35,31,66,85,86,95,83,82,91,4391,4427,5367,5371,5545,5551,5719,5723,5935,5960,6102,6127,6283,6313,58,100,64,74,75])).
% 60.81/60.84 cnf(7027,plain,
% 60.81/60.84 (~P6(x70271,a6,f17(a6,a7))),
% 60.81/60.84 inference(scs_inference,[],[6907,6902,6981,6984,4622,6844,6854,6927,6904,6894,6892,6860,6826,6833,6893,6879,6889,6837,6865,6839,6933,4598,5820,4513,5819,47,4389,6955,98,4515,48,52,60,55,71,57,92,56,93,68,67,36,62,63,3,41,42,94,61,38,40,32,35,31,66,85,86,95,83,82,91,4391,4427,5367,5371,5545,5551,5719,5723,5935,5960,6102,6127,6283,6313,58,100,64,74,75,3546,70,69,563,152])).
% 60.81/60.84 cnf(7029,plain,
% 60.81/60.84 (~P7(f5(a6,a7),f17(a7,a7))),
% 60.81/60.84 inference(scs_inference,[],[6907,6902,6981,6984,4622,6844,6854,6927,6904,6894,6892,6860,6826,6833,6893,6879,6889,6837,6865,6839,6933,4598,5820,4513,5819,47,4389,6955,98,4515,48,52,60,55,71,57,92,56,93,68,67,36,62,63,3,41,42,94,61,38,40,32,35,31,66,85,86,95,83,82,91,4391,4427,5367,5371,5545,5551,5719,5723,5935,5960,6102,6127,6283,6313,58,100,64,74,75,3546,70,69,563,152,53])).
% 60.81/60.84 cnf(7038,plain,
% 60.81/60.84 (~P6(x70381,a1,f17(a7,a7))),
% 60.81/60.84 inference(scs_inference,[],[6950,6435])).
% 60.81/60.84 cnf(7039,plain,
% 60.81/60.84 (~P6(x70391,f17(a7,a7),f17(a1,x70392))),
% 60.81/60.84 inference(scs_inference,[],[6950,6574])).
% 60.81/60.84 cnf(7041,plain,
% 60.81/60.84 (~P6(x70411,f17(a7,a7),f17(x70412,a1))),
% 60.81/60.84 inference(scs_inference,[],[6950,6744])).
% 60.81/60.84 cnf(7043,plain,
% 60.81/60.84 (~P6(x70431,f17(x70432,a1),f17(a7,a7))),
% 60.81/60.84 inference(scs_inference,[],[6950,6748])).
% 60.81/60.84 cnf(7045,plain,
% 60.81/60.84 (~E(f2(a6,a9),a9)),
% 60.81/60.84 inference(scs_inference,[],[6988,58])).
% 60.81/60.84 cnf(7047,plain,
% 60.81/60.84 (P5(f8(a6),a1)),
% 60.81/60.84 inference(scs_inference,[],[6988,6950,58,100])).
% 60.81/60.84 cnf(7048,plain,
% 60.81/60.84 (P5(f8(x70481),x70481)),
% 60.81/60.84 inference(rename_variables,[],[6950])).
% 60.81/60.84 cnf(7050,plain,
% 60.81/60.84 (P5(f11(a6,a1),a1)),
% 60.81/60.84 inference(scs_inference,[],[6971,6988,6950,58,100,60])).
% 60.81/60.84 cnf(7052,plain,
% 60.81/60.84 (P4(f16(a7),a7)),
% 60.81/60.84 inference(scs_inference,[],[6971,4823,6988,6950,58,100,60,52])).
% 60.81/60.84 cnf(7054,plain,
% 60.81/60.84 (P4(f2(a6,a9),a6)),
% 60.81/60.84 inference(scs_inference,[],[6971,4823,6988,6950,58,100,60,52,64])).
% 60.81/60.84 cnf(7058,plain,
% 60.81/60.84 (~P5(f11(a6,a1),a6)),
% 60.81/60.84 inference(scs_inference,[],[6971,4823,6988,6950,6824,58,100,60,52,64,55,71])).
% 60.81/60.84 cnf(7062,plain,
% 60.81/60.84 (P5(f8(f17(a6,a7)),f5(a6,a7))),
% 60.81/60.84 inference(scs_inference,[],[6971,4823,6988,6950,6824,618,58,100,60,52,64,55,71,57,56])).
% 60.81/60.84 cnf(7064,plain,
% 60.81/60.85 (P5(f8(x70641),f17(x70642,x70641))),
% 60.81/60.85 inference(scs_inference,[],[6971,4823,6988,6950,7048,6824,618,58,100,60,52,64,55,71,57,56,92])).
% 60.81/60.85 cnf(7066,plain,
% 60.81/60.85 (P5(f8(x70661),f17(x70661,x70662))),
% 60.81/60.85 inference(scs_inference,[],[6971,4823,6988,6950,7048,6824,618,58,100,60,52,64,55,71,57,56,92,93])).
% 60.81/60.85 cnf(7068,plain,
% 60.81/60.85 (~P6(x70681,f5(a6,a7),f5(a6,a7))),
% 60.81/60.85 inference(scs_inference,[],[6971,4823,6988,6950,7048,6824,618,58,100,60,52,64,55,71,57,56,92,93,4759])).
% 60.81/60.85 cnf(7070,plain,
% 60.81/60.85 (~P6(x70701,f5(a6,a7),f17(x70702,f17(a6,a7)))),
% 60.81/60.85 inference(scs_inference,[],[6971,4823,6988,6950,7048,6824,618,58,100,60,52,64,55,71,57,56,92,93,4759,5728])).
% 60.81/60.85 cnf(7074,plain,
% 60.81/60.85 (P5(f15(a9,a6,a6),f14(f15(a9,a6,a6),a6))),
% 60.81/60.85 inference(scs_inference,[],[6971,4823,6988,6950,7048,6980,6992,6824,618,58,100,60,52,64,55,71,57,56,92,93,4759,5728,67,68])).
% 60.81/60.85 cnf(7084,plain,
% 60.81/60.85 (~P5(f11(a7,f5(a6,a7)),f17(a7,a7))),
% 60.81/60.85 inference(scs_inference,[],[6971,4823,6988,6950,7048,6850,6986,7027,6980,6992,6824,6944,4563,5825,6860,6826,4568,618,58,100,60,52,64,55,71,57,56,92,93,4759,5728,67,68,62,63,36,3,34,94])).
% 60.81/60.85 cnf(7086,plain,
% 60.81/60.85 (~P7(f17(x70861,a1),a6)),
% 60.81/60.85 inference(scs_inference,[],[6971,4823,6988,6950,7048,6850,6986,7027,6980,6992,6824,6944,4563,5825,6860,6826,4568,618,58,100,60,52,64,55,71,57,56,92,93,4759,5728,67,68,62,63,36,3,34,94,61])).
% 60.81/60.85 cnf(7092,plain,
% 60.81/60.85 (P6(f2(a6,f16(a6)),a6,a7)),
% 60.81/60.85 inference(scs_inference,[],[6971,4823,6988,6950,7048,6850,6986,7027,6980,6992,6824,6867,6869,6944,7013,4563,5825,6860,5844,4513,6826,4568,5819,618,98,58,100,60,52,64,55,71,57,56,92,93,4759,5728,67,68,62,63,36,3,34,94,61,32,40,66,95])).
% 60.81/60.85 cnf(7094,plain,
% 60.81/60.85 (P5(f2(a6,f16(a6)),a7)),
% 60.81/60.85 inference(scs_inference,[],[6971,4823,6988,6950,7048,6850,6986,7027,6980,6992,6824,6867,6869,6944,7013,4563,5825,6860,5844,4513,6826,4568,5819,618,98,58,100,60,52,64,55,71,57,56,92,93,4759,5728,67,68,62,63,36,3,34,94,61,32,40,66,95,74])).
% 60.81/60.85 cnf(7096,plain,
% 60.81/60.85 (P5(f2(a6,f16(a6)),a6)),
% 60.81/60.85 inference(scs_inference,[],[6971,4823,6988,6950,7048,6850,6986,7027,6980,6992,6824,6867,6869,6944,7013,4563,5825,6860,5844,4513,6826,4568,5819,618,98,58,100,60,52,64,55,71,57,56,92,93,4759,5728,67,68,62,63,36,3,34,94,61,32,40,66,95,74,75])).
% 60.81/60.85 cnf(7104,plain,
% 60.81/60.85 (~P5(f8(f17(a6,a7)),x71041)+~P6(x71042,x71041,f5(a6,a7))),
% 60.81/60.85 inference(scs_inference,[],[7062,4759])).
% 60.81/60.85 cnf(7105,plain,
% 60.81/60.85 (~P5(f8(f17(a6,a7)),x71051)+~P6(x71052,f5(a6,a7),x71051)),
% 60.81/60.85 inference(scs_inference,[],[7062,5728])).
% 60.81/60.85 cnf(7107,plain,
% 60.81/60.85 (P5(f8(x71071),f17(x71072,x71071))),
% 60.81/60.85 inference(rename_variables,[],[7064])).
% 60.81/60.85 cnf(7112,plain,
% 60.81/60.85 (P5(f8(a7),a1)),
% 60.81/60.85 inference(scs_inference,[],[7064,7107,7066,7104,7105,117])).
% 60.81/60.85 cnf(7113,plain,
% 60.81/60.85 (P5(f8(x71131),f17(x71132,x71131))),
% 60.81/60.85 inference(rename_variables,[],[7064])).
% 60.81/60.85 cnf(7117,plain,
% 60.81/60.85 (P5(f16(a6),a1)),
% 60.81/60.85 inference(scs_inference,[],[7064,7107,7066,7017,7052,7104,7105,117,58,100])).
% 60.81/60.85 cnf(7119,plain,
% 60.81/60.85 (P4(f2(a7,f16(a7)),a7)),
% 60.81/60.85 inference(scs_inference,[],[7064,7107,7066,7017,7052,7104,7105,117,58,100,64])).
% 60.81/60.85 cnf(7121,plain,
% 60.81/60.85 (P5(f11(f17(a7,a7),f5(a6,a7)),f5(a6,a7))),
% 60.81/60.85 inference(scs_inference,[],[7064,7107,7066,7029,7017,7052,7104,7105,117,58,100,64,60])).
% 60.81/60.85 cnf(7123,plain,
% 60.81/60.85 (~P5(f11(f17(a7,a7),f5(a6,a7)),f17(a7,a7))),
% 60.81/60.85 inference(scs_inference,[],[7064,7107,7066,7029,7017,7052,7104,7105,117,58,100,64,60,71])).
% 60.81/60.85 cnf(7127,plain,
% 60.81/60.85 (~P2(f16(a7),a7)),
% 60.81/60.85 inference(scs_inference,[],[7064,7107,7066,7029,7017,7052,7058,7104,7105,117,58,100,64,60,71,55,57])).
% 60.81/60.85 cnf(7129,plain,
% 60.81/60.85 (P5(f8(x71291),f17(x71292,f17(x71293,x71291)))),
% 60.81/60.85 inference(scs_inference,[],[7064,7107,7113,7066,7029,7017,7052,7058,7104,7105,117,58,100,64,60,71,55,57,92])).
% 60.81/60.85 cnf(7131,plain,
% 60.81/60.85 (P5(f8(x71311),f17(f17(x71312,x71311),x71313))),
% 60.81/60.85 inference(scs_inference,[],[7064,7107,7113,7066,7029,7017,7052,7058,7104,7105,117,58,100,64,60,71,55,57,92,93])).
% 60.81/60.85 cnf(7134,plain,
% 60.81/60.85 (P5(f8(x71341),f17(x71342,x71341))),
% 60.81/60.85 inference(rename_variables,[],[7064])).
% 60.81/60.85 cnf(7135,plain,
% 60.81/60.85 (~P4(x71351,f17(a6,a7))),
% 60.81/60.85 inference(rename_variables,[],[96])).
% 60.81/60.85 cnf(7138,plain,
% 60.81/60.85 (~P4(x71381,f17(a6,a7))),
% 60.81/60.85 inference(rename_variables,[],[96])).
% 60.81/60.85 cnf(7139,plain,
% 60.81/60.85 (P5(f8(x71391),f17(x71392,x71391))),
% 60.81/60.85 inference(rename_variables,[],[7064])).
% 60.81/60.85 cnf(7141,plain,
% 60.81/60.85 (P5(f8(a7),f14(f8(a7),f17(a6,a7)))),
% 60.81/60.85 inference(scs_inference,[],[7064,7107,7113,7134,7139,7066,7029,7017,7052,7058,96,7135,7138,7104,7105,117,58,100,64,60,71,55,57,92,93,70,67,68])).
% 60.81/60.85 cnf(7142,plain,
% 60.81/60.85 (~P4(x71421,f17(a6,a7))),
% 60.81/60.85 inference(rename_variables,[],[96])).
% 60.81/60.85 cnf(7143,plain,
% 60.81/60.85 (P5(f8(x71431),f17(x71432,x71431))),
% 60.81/60.85 inference(rename_variables,[],[7064])).
% 60.81/60.85 cnf(7146,plain,
% 60.81/60.85 (P5(f8(x71461),f17(x71462,x71461))),
% 60.81/60.85 inference(rename_variables,[],[7064])).
% 60.81/60.85 cnf(7155,plain,
% 60.81/60.85 (~P7(a6,a7)),
% 60.81/60.85 inference(scs_inference,[],[7064,7107,7113,7134,7139,7143,7066,7029,7017,7052,7058,7050,6969,4593,6839,6860,96,7135,7138,7142,7104,7105,117,58,100,64,60,71,55,57,92,93,70,67,68,69,63,62,3,33,61])).
% 60.81/60.85 cnf(7157,plain,
% 60.81/60.85 (~P7(f17(a6,a7),f17(a7,a7))),
% 60.81/60.85 inference(scs_inference,[],[7064,7107,7113,7134,7139,7143,7066,7029,7017,7052,7058,7050,6969,4593,6839,6860,96,7135,7138,7142,7104,7105,117,58,100,64,60,71,55,57,92,93,70,67,68,69,63,62,3,33,61,32])).
% 60.81/60.85 cnf(7158,plain,
% 60.81/60.85 (P5(f8(a7),f5(a6,a7))),
% 60.81/60.85 inference(scs_inference,[],[7064,7107,7113,7134,7139,7143,7146,7066,7029,7017,7052,7058,7050,6969,4593,6839,6860,96,7135,7138,7142,7104,7105,117,58,100,64,60,71,55,57,92,93,70,67,68,69,63,62,3,33,61,32,40])).
% 60.81/60.85 cnf(7159,plain,
% 60.81/60.85 (P5(f8(x71591),f17(x71592,x71591))),
% 60.81/60.85 inference(rename_variables,[],[7064])).
% 60.81/60.85 cnf(7161,plain,
% 60.81/60.85 (P5(f8(x71611),f17(x71612,x71611))),
% 60.81/60.85 inference(rename_variables,[],[7064])).
% 60.81/60.85 cnf(7162,plain,
% 60.81/60.85 (~P6(x71621,f17(a6,a7),f5(a6,a7))),
% 60.81/60.85 inference(rename_variables,[],[6960])).
% 60.81/60.85 cnf(7164,plain,
% 60.81/60.85 (~E(f5(a6,a7),f17(f17(a7,a7),f17(a7,a7)))),
% 60.81/60.85 inference(scs_inference,[],[7064,7107,7113,7134,7139,7143,7146,7159,7066,6960,7029,7017,7052,7058,7050,7084,6969,6940,4593,6839,6860,96,7135,7138,7142,7104,7105,117,58,100,64,60,71,55,57,92,93,70,67,68,69,63,62,3,33,61,32,40,86,66])).
% 60.81/60.85 cnf(7167,plain,
% 60.81/60.85 (P5(f8(x71671),f17(x71672,x71671))),
% 60.81/60.85 inference(rename_variables,[],[7064])).
% 60.81/60.85 cnf(7170,plain,
% 60.81/60.85 (P6(f2(a6,a9),a6,a7)),
% 60.81/60.85 inference(scs_inference,[],[7064,7107,7113,7134,7139,7143,7146,7159,7161,7066,6960,7162,7029,7017,7052,7054,7058,7050,7084,6969,7092,6940,4593,6839,6860,96,7135,7138,7142,98,7104,7105,117,58,100,64,60,71,55,57,92,93,70,67,68,69,63,62,3,33,61,32,40,86,66,85,95])).
% 60.81/60.85 cnf(7172,plain,
% 60.81/60.85 (~P6(x71721,f17(x71722,f5(a6,a7)),f5(a6,a7))),
% 60.81/60.85 inference(scs_inference,[],[7064,7107,7113,7134,7139,7143,7146,7159,7161,7167,7066,6960,7162,7029,7017,7052,7054,7058,7050,7084,6969,7092,6940,4593,6950,6927,6839,6860,96,7135,7138,7142,98,7104,7105,117,58,100,64,60,71,55,57,92,93,70,67,68,69,63,62,3,33,61,32,40,86,66,85,95,82])).
% 60.81/60.85 cnf(7177,plain,
% 60.81/60.85 (P5(f2(a6,a9),a7)),
% 60.81/60.85 inference(scs_inference,[],[7064,7107,7113,7134,7139,7143,7146,7159,7161,7167,7066,6960,7162,7029,7017,7052,7054,7058,7050,7084,6969,7092,6940,4593,6950,6927,6839,6860,96,7135,7138,7142,98,7104,7105,117,58,100,64,60,71,55,57,92,93,70,67,68,69,63,62,3,33,61,32,40,86,66,85,95,82,74])).
% 60.81/60.85 cnf(7179,plain,
% 60.81/60.85 (P5(f2(a6,a9),a6)),
% 60.81/60.85 inference(scs_inference,[],[7064,7107,7113,7134,7139,7143,7146,7159,7161,7167,7066,6960,7162,7029,7017,7052,7054,7058,7050,7084,6969,7092,6940,4593,6950,6927,6839,6860,96,7135,7138,7142,98,7104,7105,117,58,100,64,60,71,55,57,92,93,70,67,68,69,63,62,3,33,61,32,40,86,66,85,95,82,74,75])).
% 60.81/60.85 cnf(7185,plain,
% 60.81/60.85 (P5(f2(a6,a9),a1)),
% 60.81/60.85 inference(scs_inference,[],[7179,100])).
% 60.81/60.85 cnf(7189,plain,
% 60.81/60.85 (P5(f11(a7,a6),a6)),
% 60.81/60.85 inference(scs_inference,[],[7155,7179,6990,100,58,60])).
% 60.81/60.85 cnf(7191,plain,
% 60.81/60.85 (P4(f2(a7,a9),a7)),
% 60.81/60.85 inference(scs_inference,[],[7155,7179,6990,100,58,60,64])).
% 60.81/60.85 cnf(7193,plain,
% 60.81/60.85 (~P5(f11(a7,a6),a7)),
% 60.81/60.85 inference(scs_inference,[],[7155,7179,6990,100,58,60,64,71])).
% 60.81/60.85 cnf(7197,plain,
% 60.81/60.85 (~P2(f2(a7,f16(a7)),a7)),
% 60.81/60.85 inference(scs_inference,[],[7155,7179,7123,7119,6990,100,58,60,64,71,55,57])).
% 60.81/60.85 cnf(7199,plain,
% 60.81/60.85 (P5(f8(a6),f17(x71991,a1))),
% 60.81/60.85 inference(scs_inference,[],[7155,7047,7179,7123,7119,6990,100,58,60,64,71,55,57,92])).
% 60.81/60.85 cnf(7201,plain,
% 60.81/60.85 (P5(f8(a6),f17(a1,x72011))),
% 60.81/60.85 inference(scs_inference,[],[7155,7047,7179,7123,7119,6990,100,58,60,64,71,55,57,92,93])).
% 60.81/60.85 cnf(7204,plain,
% 60.81/60.85 (~P4(x72041,f5(a6,a7))),
% 60.81/60.85 inference(rename_variables,[],[6927])).
% 60.81/60.85 cnf(7206,plain,
% 60.81/60.85 (P5(f8(a7),f14(f8(a7),f5(a6,a7)))),
% 60.81/60.85 inference(scs_inference,[],[7155,7047,7158,7179,7123,7119,6990,6927,7204,100,58,60,64,71,55,57,92,93,70,68])).
% 60.81/60.85 cnf(7207,plain,
% 60.81/60.85 (~P4(x72071,f5(a6,a7))),
% 60.81/60.85 inference(rename_variables,[],[6927])).
% 60.81/60.85 cnf(7210,plain,
% 60.81/60.85 (~P4(x72101,f5(a6,a7))),
% 60.81/60.85 inference(rename_variables,[],[6927])).
% 60.81/60.85 cnf(7212,plain,
% 60.81/60.85 (P5(f2(a6,a9),f5(a6,a7))),
% 60.81/60.85 inference(scs_inference,[],[7155,7047,7158,7179,7123,7119,6990,6927,7204,7207,6826,100,58,60,64,71,55,57,92,93,70,68,67,63])).
% 60.81/60.85 cnf(7217,plain,
% 60.81/60.85 (P5(f16(a6),f5(a6,a7))),
% 60.81/60.85 inference(scs_inference,[],[7155,7047,7015,7158,7179,7123,7119,6990,6927,7204,7207,7210,6826,100,58,60,64,71,55,57,92,93,70,68,67,63,69,62])).
% 60.81/60.85 cnf(7220,plain,
% 60.81/60.85 (P5(f2(a6,f16(a6)),a1)),
% 60.81/60.85 inference(scs_inference,[],[7155,7047,7015,7158,7179,7123,7094,7119,6990,4499,6927,7204,7207,7210,6826,6860,46,100,58,60,64,71,55,57,92,93,70,68,67,63,69,62,3,61])).
% 60.81/60.85 cnf(7233,plain,
% 60.81/60.85 (P4(f2(a6,a9),a7)),
% 60.81/60.85 inference(scs_inference,[],[7155,7068,7047,7015,7158,7170,6995,7086,7177,7179,7123,6871,7094,7119,6858,6990,4499,7064,6865,6927,7204,7207,7210,4513,4600,6826,6860,46,100,58,60,64,71,55,57,92,93,70,68,67,63,69,62,3,61,32,40,85,86,66,82])).
% 60.81/60.85 cnf(7235,plain,
% 60.81/60.85 (E(f2(a6,a9),f2(a7,a9))),
% 60.81/60.85 inference(scs_inference,[],[7155,7068,7047,7015,7158,7170,6995,7086,7177,7179,7045,7123,6871,7094,7119,6858,6990,4499,7064,6865,6927,7204,7207,7210,4513,4600,6826,6860,46,100,58,60,64,71,55,57,92,93,70,68,67,63,69,62,3,61,32,40,85,86,66,82,65])).
% 60.81/60.85 cnf(7240,plain,
% 60.81/60.85 (E(f2(a7,a9),f2(a6,a9))),
% 60.81/60.85 inference(scs_inference,[],[7155,7068,7047,7015,7158,7170,6995,7086,7177,7179,7045,7123,6871,7094,7119,6858,6990,4499,7064,6865,6927,7204,7207,7210,4513,4600,6826,6860,46,100,58,60,64,71,55,57,92,93,70,68,67,63,69,62,3,61,32,40,85,86,66,82,65,137,56,2])).
% 60.81/60.85 cnf(7255,plain,
% 60.81/60.85 (P5(f11(a7,a6),a1)),
% 60.81/60.85 inference(scs_inference,[],[7240,7189,137,100])).
% 60.81/60.85 cnf(7259,plain,
% 60.81/60.85 (P5(f11(f17(a7,a7),f17(a6,a7)),f17(a6,a7))),
% 60.81/60.85 inference(scs_inference,[],[7157,7240,7233,7189,137,100,58,60])).
% 60.81/60.85 cnf(7261,plain,
% 60.81/60.85 (P4(f2(a7,f2(a6,a9)),a7)),
% 60.81/60.85 inference(scs_inference,[],[7157,7240,7233,7189,137,100,58,60,64])).
% 60.81/60.85 cnf(7263,plain,
% 60.81/60.85 (~P5(f11(f17(a7,a7),f17(a6,a7)),f17(a7,a7))),
% 60.81/60.85 inference(scs_inference,[],[7157,7240,7233,7189,137,100,58,60,64,71])).
% 60.81/60.85 cnf(7265,plain,
% 60.81/60.85 (~P4(f11(a7,a6),a7)),
% 60.81/60.85 inference(scs_inference,[],[7157,7240,7233,7193,7189,137,100,58,60,64,71,55])).
% 60.81/60.85 cnf(7269,plain,
% 60.81/60.85 (P5(f8(f2(a7,a9)),f2(a6,a9))),
% 60.81/60.85 inference(scs_inference,[],[7157,7240,7233,7193,7189,137,100,58,60,64,71,55,57,56])).
% 60.81/60.85 cnf(7271,plain,
% 60.81/60.85 (P5(f8(a7),f17(x72711,a1))),
% 60.81/60.85 inference(scs_inference,[],[7157,7112,7240,7233,7193,7189,137,100,58,60,64,71,55,57,56,92])).
% 60.81/60.85 cnf(7273,plain,
% 60.81/60.85 (P5(f8(a7),f17(a1,x72731))),
% 60.81/60.85 inference(scs_inference,[],[7157,7112,7240,7233,7193,7189,137,100,58,60,64,71,55,57,56,92,93])).
% 60.81/60.85 cnf(7276,plain,
% 60.81/60.85 (~P4(x72761,f5(a6,a7))),
% 60.81/60.85 inference(rename_variables,[],[6927])).
% 60.81/60.85 cnf(7281,plain,
% 60.81/60.85 (~P4(x72811,f5(a6,a7))),
% 60.81/60.85 inference(rename_variables,[],[6927])).
% 60.81/60.85 cnf(7284,plain,
% 60.81/60.85 (~P4(x72841,f5(a6,a7))),
% 60.81/60.85 inference(rename_variables,[],[6927])).
% 60.81/60.85 cnf(7292,plain,
% 60.81/60.85 (~E(f17(a6,a7),f17(f17(a7,a7),f17(a7,a7)))),
% 60.81/60.85 inference(scs_inference,[],[7157,7112,7212,7240,7233,7193,7189,7164,7015,6927,7276,7281,7284,6826,137,100,58,60,64,71,55,57,56,92,93,70,63,67,68,69,62,39,3])).
% 60.81/60.85 cnf(7293,plain,
% 60.81/60.85 (~P7(a1,a7)),
% 60.81/60.85 inference(scs_inference,[],[7157,7112,7212,7240,7233,7193,7189,7164,7011,7015,6927,7276,7281,7284,6839,6826,137,100,58,60,64,71,55,57,56,92,93,70,63,67,68,69,62,39,3,61])).
% 60.81/60.85 cnf(7296,plain,
% 60.81/60.85 (P5(f2(a6,a9),f17(a6,a7))),
% 60.81/60.85 inference(scs_inference,[],[7157,7112,7212,7240,7233,7193,7189,7164,7011,7015,6927,7276,7281,7284,6839,6826,137,100,58,60,64,71,55,57,56,92,93,70,63,67,68,69,62,39,3,61,37,40])).
% 60.81/60.85 cnf(7298,plain,
% 60.81/60.85 (~P6(x72981,f5(a6,a7),f5(a6,a7))),
% 60.81/60.85 inference(rename_variables,[],[7068])).
% 60.81/60.85 cnf(7305,plain,
% 60.81/60.85 (P4(f16(a6),a7)),
% 60.81/60.85 inference(scs_inference,[],[7157,7112,7212,7240,7217,7233,7193,7189,7164,7011,7068,7298,7015,7017,6858,7170,6927,7276,7281,7284,6839,4568,6826,137,100,58,60,64,71,55,57,56,92,93,70,63,67,68,69,62,39,3,61,37,40,86,85,66,82])).
% 60.81/60.85 cnf(7321,plain,
% 60.81/60.85 (P4(f2(a7,f16(a6)),a7)),
% 60.81/60.85 inference(scs_inference,[],[7305,6983,7235,6768,100,58,64])).
% 60.81/60.85 cnf(7323,plain,
% 60.81/60.85 (P5(f11(a7,a1),a1)),
% 60.81/60.85 inference(scs_inference,[],[7293,7305,6983,7235,6768,100,58,64,60])).
% 60.81/60.85 cnf(7325,plain,
% 60.81/60.85 (~P5(f11(a7,a1),a7)),
% 60.81/60.85 inference(scs_inference,[],[7293,7305,6983,7235,6768,100,58,64,60,71])).
% 60.81/60.85 cnf(7335,plain,
% 60.81/60.85 (P7(f14(f8(x73351),x73351),x73351)),
% 60.81/60.85 inference(scs_inference,[],[7293,7305,7296,7263,6983,7235,6950,4389,6768,100,58,64,60,71,55,57,92,93,70])).
% 60.81/60.85 cnf(7336,plain,
% 60.81/60.85 (~P4(f8(x73361),x73361)),
% 60.81/60.85 inference(rename_variables,[],[4389])).
% 60.81/60.85 cnf(7341,plain,
% 60.81/60.85 (~P4(x73411,f17(a6,a7))),
% 60.81/60.85 inference(rename_variables,[],[96])).
% 60.81/60.85 cnf(7346,plain,
% 60.81/60.85 (P7(f12(f8(x73461),x73461),x73461)),
% 60.81/60.85 inference(scs_inference,[],[7293,7305,7296,7255,7263,6983,7235,6950,7193,4389,7336,96,7341,6768,100,58,64,60,71,55,57,92,93,70,63,67,68,69])).
% 60.81/60.85 cnf(7351,plain,
% 60.81/60.85 (~P5(f11(a6,a1),f17(a6,a6))),
% 60.81/60.85 inference(scs_inference,[],[7293,7305,7296,7255,7263,6983,7235,6950,7058,7193,4389,7336,96,7341,6768,100,58,64,60,71,55,57,92,93,70,63,67,68,69,62,94])).
% 60.81/60.85 cnf(7355,plain,
% 60.81/60.85 (P5(f15(a9,a6,a6),a1)),
% 60.81/60.85 inference(scs_inference,[],[7293,7305,7296,7255,7263,6983,7235,6933,6980,6950,7058,7193,45,4389,7336,96,7341,6768,100,58,64,60,71,55,57,92,93,70,63,67,68,69,62,94,59,61])).
% 60.81/60.85 cnf(7357,plain,
% 60.81/60.85 (P5(f2(a7,a9),f17(a6,a7))),
% 60.81/60.85 inference(scs_inference,[],[7293,7305,7296,7255,7263,6983,7235,6933,6980,6950,7058,7193,45,4389,7336,96,7341,6768,100,58,64,60,71,55,57,92,93,70,63,67,68,69,62,94,59,61,39])).
% 60.81/60.85 cnf(7362,plain,
% 60.81/60.85 (~P6(x73621,f17(a6,a7),f5(a6,a7))),
% 60.81/60.85 inference(rename_variables,[],[6960])).
% 60.81/60.85 cnf(7367,plain,
% 60.81/60.85 (~P6(x73671,f2(a6,a9),f2(a6,a9))),
% 60.81/60.85 inference(scs_inference,[],[7293,7305,7296,7255,7127,7263,7269,6983,7235,6960,7362,6867,6933,6980,6950,7058,7193,4513,7212,45,47,4389,7336,96,7341,6768,100,58,64,60,71,55,57,92,93,70,63,67,68,69,62,94,59,61,39,37,40,86,85,82])).
% 60.81/60.85 cnf(7382,plain,
% 60.81/60.85 (~E(f2(a7,f2(a7,a9)),f2(a7,a9))),
% 60.81/60.85 inference(scs_inference,[],[7191,58])).
% 60.81/60.85 cnf(7384,plain,
% 60.81/60.85 (P5(f11(a6,f5(a6,a7)),f5(a6,a7))),
% 60.81/60.85 inference(scs_inference,[],[6975,7191,58,60])).
% 60.81/60.85 cnf(7386,plain,
% 60.81/60.85 (P4(f2(a7,f2(a7,a9)),a7)),
% 60.81/60.85 inference(scs_inference,[],[6975,7191,58,60,64])).
% 60.81/60.85 cnf(7390,plain,
% 60.81/60.85 (~P5(f11(a6,f5(a6,a7)),a6)),
% 60.81/60.85 inference(scs_inference,[],[6975,7351,7191,58,60,64,55,71])).
% 60.81/60.85 cnf(7400,plain,
% 60.81/60.85 (P7(f14(f2(a7,a9),f17(a6,a7)),f17(a6,a7))),
% 60.81/60.85 inference(scs_inference,[],[7357,6975,7351,7185,7321,7191,7296,96,58,60,64,55,71,57,92,93,563,70])).
% 60.81/60.85 cnf(7401,plain,
% 60.81/60.85 (~P4(x74011,f17(a6,a7))),
% 60.81/60.85 inference(rename_variables,[],[96])).
% 60.81/60.85 cnf(7406,plain,
% 60.81/60.85 (~P4(x74061,f17(a6,a7))),
% 60.81/60.85 inference(rename_variables,[],[96])).
% 60.81/60.85 cnf(7409,plain,
% 60.81/60.85 (~P4(x74091,f17(a6,a7))),
% 60.81/60.85 inference(rename_variables,[],[96])).
% 60.81/60.85 cnf(7415,plain,
% 60.81/60.85 (~P6(x74151,a1,f17(a6,a7))),
% 60.81/60.85 inference(scs_inference,[],[7357,6975,7351,7185,7265,7321,7191,7050,7296,96,7401,7406,7409,58,60,64,55,71,57,92,93,563,70,63,67,68,69,41,152])).
% 60.81/60.85 cnf(7419,plain,
% 60.81/60.85 (~P7(f17(a6,a7),f17(f17(a7,a7),f17(a7,a7)))),
% 60.81/60.85 inference(scs_inference,[],[7357,6975,7351,7185,7265,7292,7321,7191,7050,7296,49,96,7401,7406,7409,58,60,64,55,71,57,92,93,563,70,63,67,68,69,41,152,62,53])).
% 60.81/60.85 cnf(7421,plain,
% 60.81/60.85 (~P6(x74211,f2(a6,a9),f2(a7,a9))),
% 60.81/60.85 inference(scs_inference,[],[7357,6975,7351,7185,7367,7265,7292,7321,7191,7050,7240,7296,49,96,7401,7406,7409,58,60,64,55,71,57,92,93,563,70,63,67,68,69,41,152,62,53,36])).
% 60.81/60.85 cnf(7422,plain,
% 60.81/60.85 (~P7(a1,f17(a6,a6))),
% 60.81/60.85 inference(scs_inference,[],[7357,6975,7351,7185,7367,7265,7292,7321,7191,7050,7240,7296,49,96,7401,7406,7409,58,60,64,55,71,57,92,93,563,70,63,67,68,69,41,152,62,53,36,61])).
% 60.81/60.85 cnf(7425,plain,
% 60.81/60.85 (P5(f8(x74251),f17(x74251,x74252))),
% 60.81/60.85 inference(rename_variables,[],[7066])).
% 60.81/60.85 cnf(7426,plain,
% 60.81/60.85 (P5(f2(a7,a9),f5(a6,a7))),
% 60.81/60.85 inference(scs_inference,[],[7357,6975,7351,7185,7367,7265,7292,7321,7191,7066,7050,7240,7296,6860,49,96,7401,7406,7409,58,60,64,55,71,57,92,93,563,70,63,67,68,69,41,152,62,53,36,61,39,40])).
% 60.81/60.85 cnf(7428,plain,
% 60.81/60.85 (~P6(x74281,f17(a6,a6),f17(x74282,a1))),
% 60.81/60.85 inference(rename_variables,[],[6997])).
% 60.81/60.85 cnf(7429,plain,
% 60.81/60.85 (P5(f8(x74291),f17(x74291,x74292))),
% 60.81/60.85 inference(rename_variables,[],[7066])).
% 60.81/60.85 cnf(7431,plain,
% 60.81/60.85 (~E(f5(a6,a7),f17(a6,a6))),
% 60.81/60.85 inference(scs_inference,[],[7357,6997,6975,7351,7185,7367,7199,7265,7292,7321,7191,7066,7425,7050,7240,7296,6860,49,96,7401,7406,7409,58,60,64,55,71,57,92,93,563,70,63,67,68,69,41,152,62,53,36,61,39,40,86,66])).
% 60.81/60.85 cnf(7435,plain,
% 60.81/60.85 (P5(f8(x74351),f17(x74351,x74352))),
% 60.81/60.85 inference(rename_variables,[],[7066])).
% 60.81/60.85 cnf(7437,plain,
% 60.81/60.85 (P4(f2(a6,f16(a6)),a7)),
% 60.81/60.85 inference(scs_inference,[],[7357,6997,7428,6975,7351,7185,7367,7199,7265,7292,7096,7321,7191,7094,7066,7425,7429,7092,7050,7240,7296,6860,49,96,7401,7406,7409,58,60,64,55,71,57,92,93,563,70,63,67,68,69,41,152,62,53,36,61,39,40,86,66,85,82])).
% 60.81/60.85 cnf(7448,plain,
% 60.81/60.85 (~P5(f15(f13(a7,a6,a7),a6,a6),a7)),
% 60.81/60.85 inference(scs_inference,[],[7357,6977,6997,7428,6975,7351,7185,7367,7199,7265,7292,7096,7321,7191,7094,7066,7425,7429,7435,7092,7050,6933,6983,7240,7296,6860,49,96,7401,7406,7409,58,60,64,55,71,57,92,93,563,70,63,67,68,69,41,152,62,53,36,61,39,40,86,66,85,82,102,7104,77,94,83])).
% 60.81/60.85 cnf(7453,plain,
% 60.81/60.85 (~E(f2(a6,f2(a6,a9)),f2(a6,a9))),
% 60.81/60.85 inference(scs_inference,[],[7054,58])).
% 60.81/60.85 cnf(7457,plain,
% 60.81/60.85 (P4(f2(a6,f2(a6,a9)),a6)),
% 60.81/60.85 inference(scs_inference,[],[7422,7054,58,60,64])).
% 60.81/60.85 cnf(7459,plain,
% 60.81/60.85 (~P5(f11(f17(a6,a6),a1),f17(a6,a6))),
% 60.81/60.85 inference(scs_inference,[],[7422,7054,58,60,64,71])).
% 60.81/60.85 cnf(7470,plain,
% 60.81/60.85 (~P4(x74701,f5(a6,a7))),
% 60.81/60.85 inference(rename_variables,[],[6927])).
% 60.81/60.85 cnf(7473,plain,
% 60.81/60.85 (~P4(x74731,f5(a6,a7))),
% 60.81/60.85 inference(rename_variables,[],[6927])).
% 60.81/60.85 cnf(7476,plain,
% 60.81/60.85 (~P4(x74761,f5(a6,a7))),
% 60.81/60.85 inference(rename_variables,[],[6927])).
% 60.81/60.85 cnf(7485,plain,
% 60.81/60.85 (~E(f2(a6,a9),f13(a7,a6,a7))),
% 60.81/60.85 inference(scs_inference,[],[7422,7426,7325,7384,7386,7390,7054,7170,4519,6927,7470,7473,7476,58,60,64,71,55,57,92,93,70,67,68,63,69,62,34])).
% 60.81/60.85 cnf(7487,plain,
% 60.81/60.85 (~P5(f11(a7,a1),f17(a7,a7))),
% 60.81/60.85 inference(scs_inference,[],[7422,7426,7325,7384,7386,7390,7054,7170,4519,6927,7470,7473,7476,58,60,64,71,55,57,92,93,70,67,68,63,69,62,34,94])).
% 60.81/60.85 cnf(7490,plain,
% 60.81/60.85 (~E(f17(a6,a7),f17(a6,a6))),
% 60.81/60.85 inference(scs_inference,[],[7422,7431,7426,7415,7325,7384,7386,7390,7054,7170,4519,6927,7470,7473,7476,6826,58,60,64,71,55,57,92,93,70,67,68,63,69,62,34,94,36,3])).
% 60.81/60.85 cnf(7497,plain,
% 60.81/60.85 (P5(f15(f2(a7,a9),f5(a6,a7),f5(a6,a7)),f5(a6,a7))),
% 60.81/60.85 inference(scs_inference,[],[7422,7431,7426,7415,7325,7384,7419,7386,7390,7197,7054,7068,6858,7170,4519,6927,7470,7473,7476,4624,4568,6826,47,58,60,64,71,55,57,92,93,70,67,68,63,69,62,34,94,36,3,61,32,37,40,86])).
% 60.81/60.85 cnf(7510,plain,
% 60.81/60.85 (P5(f11(a6,f17(x75101,a1)),f17(x75101,a1))),
% 60.81/60.85 inference(scs_inference,[],[7086,60])).
% 60.81/60.85 cnf(7512,plain,
% 60.81/60.85 (~P5(f11(a6,f17(x75121,a1)),a6)),
% 60.81/60.85 inference(scs_inference,[],[7086,60,71])).
% 60.81/60.85 cnf(7518,plain,
% 60.81/60.85 (P5(f16(a6),f17(x75181,a1))),
% 60.81/60.85 inference(scs_inference,[],[7487,7117,7457,7086,60,71,55,57,92])).
% 60.81/60.85 cnf(7520,plain,
% 60.81/60.85 (P5(f16(a6),f17(a1,x75201))),
% 60.81/60.85 inference(scs_inference,[],[7487,7117,7457,7086,60,71,55,57,92,93])).
% 60.81/60.85 cnf(7523,plain,
% 60.81/60.85 (~P4(x75231,f5(a6,a7))),
% 60.81/60.85 inference(rename_variables,[],[6927])).
% 60.81/60.85 cnf(7534,plain,
% 60.81/60.85 (~P7(f17(a6,a7),f17(a6,a6))),
% 60.81/60.85 inference(scs_inference,[],[7490,7487,7117,7457,7323,7086,7217,6927,7523,49,60,71,55,57,92,93,70,63,62,69,94,53])).
% 60.81/60.85 cnf(7537,plain,
% 60.81/60.85 (~P7(a1,f17(a7,a7))),
% 60.81/60.85 inference(scs_inference,[],[7490,7487,7117,7485,7457,7323,7086,7217,7235,6927,7523,49,60,71,55,57,92,93,70,63,62,69,94,53,3,61])).
% 60.81/60.85 cnf(7544,plain,
% 60.81/60.85 (P5(f8(a6),f17(a1,x75441))),
% 60.81/60.85 inference(rename_variables,[],[7201])).
% 60.81/60.85 cnf(7545,plain,
% 60.81/60.85 (~P6(x75451,f17(x75452,a1),f17(a6,a6))),
% 60.81/60.85 inference(rename_variables,[],[6998])).
% 60.81/60.85 cnf(7546,plain,
% 60.81/60.85 (P5(f8(x75461),f17(x75462,x75461))),
% 60.81/60.85 inference(rename_variables,[],[7064])).
% 60.81/60.85 cnf(7555,plain,
% 60.81/60.85 (P6(f2(a6,f2(a6,a9)),a6,a7)),
% 60.81/60.85 inference(scs_inference,[],[7490,7487,7117,6998,7545,7485,7201,7544,7497,7335,7457,7323,7086,7217,7064,7546,7235,6986,6927,7523,49,6826,98,60,71,55,57,92,93,70,63,62,69,94,53,3,61,32,40,86,66,85,95])).
% 60.81/60.85 cnf(7559,plain,
% 60.81/60.85 (P5(f2(a6,f2(a6,a9)),a7)),
% 60.81/60.85 inference(scs_inference,[],[7490,7487,7117,6998,7545,7485,7201,7544,7497,7335,7457,7323,7086,7217,7064,7546,7235,6986,6927,7523,49,6826,98,60,71,55,57,92,93,70,63,62,69,94,53,3,61,32,40,86,66,85,95,102,74])).
% 60.81/60.85 cnf(7561,plain,
% 60.81/60.85 (P5(f2(a6,f2(a6,a9)),a6)),
% 60.81/60.85 inference(scs_inference,[],[7490,7487,7117,6998,7545,7485,7201,7544,7497,7335,7457,7323,7086,7217,7064,7546,7235,6986,6927,7523,49,6826,98,60,71,55,57,92,93,70,63,62,69,94,53,3,61,32,40,86,66,85,95,102,74,75])).
% 60.81/60.85 cnf(7578,plain,
% 60.81/60.85 (P5(f11(f17(a6,a6),f17(a6,a7)),f17(a6,a7))),
% 60.81/60.85 inference(scs_inference,[],[7534,7561,100,60])).
% 60.81/60.85 cnf(7580,plain,
% 60.81/60.85 (~P5(f11(f17(a6,a6),f17(a6,a7)),f17(a6,a6))),
% 60.81/60.85 inference(scs_inference,[],[7534,7561,100,60,71])).
% 60.81/60.85 cnf(7586,plain,
% 60.81/60.85 (P5(f15(a9,a6,a6),f17(x75861,a1))),
% 60.81/60.85 inference(scs_inference,[],[7534,7355,7459,7561,7437,100,60,71,55,57,92])).
% 60.81/60.85 cnf(7588,plain,
% 60.81/60.85 (P5(f15(a9,a6,a6),f17(a1,x75881))),
% 60.81/60.85 inference(scs_inference,[],[7534,7355,7459,7561,7437,100,60,71,55,57,92,93])).
% 60.81/60.85 cnf(7594,plain,
% 60.81/60.85 (~P5(f15(f13(a7,a6,a7),a6,a6),f17(a7,a7))),
% 60.81/60.85 inference(scs_inference,[],[7534,7355,7459,7448,7561,7121,7437,7123,6826,100,60,71,55,57,92,93,63,62,94])).
% 60.81/60.85 cnf(7598,plain,
% 60.81/60.85 (~P6(x75981,f2(a7,a9),f2(a7,a9))),
% 60.81/60.85 inference(scs_inference,[],[7534,7355,7421,7459,7448,7561,7121,7437,7123,6850,7240,4624,6826,100,60,71,55,57,92,93,63,62,94,61,35])).
% 60.81/60.85 cnf(7599,plain,
% 60.81/60.85 (~P7(f5(a6,a7),f17(a6,a6))),
% 60.81/60.85 inference(scs_inference,[],[7534,7355,7421,7459,7448,7561,7121,7437,7123,6850,7240,4624,6826,100,60,71,55,57,92,93,63,62,94,61,35,32])).
% 60.81/60.85 cnf(7601,plain,
% 60.81/60.85 (~P5(f11(a6,f17(x76011,a1)),a6)),
% 60.81/60.85 inference(rename_variables,[],[7512])).
% 60.81/60.85 cnf(7602,plain,
% 60.81/60.85 (P5(f15(f8(a7),f17(a7,a7),f17(a1,a1)),f17(a7,a7))),
% 60.81/60.85 inference(scs_inference,[],[7534,7355,7039,7421,7271,7459,7510,7448,7561,7512,7121,7437,7123,7066,6850,7240,4624,6826,100,60,71,55,57,92,93,63,62,94,61,35,32,40,86])).
% 60.81/60.85 cnf(7603,plain,
% 60.81/60.85 (~P6(x76031,f17(a7,a7),f17(a1,x76032))),
% 60.81/60.85 inference(rename_variables,[],[7039])).
% 60.81/60.85 cnf(7604,plain,
% 60.81/60.85 (P5(f8(a7),f17(x76041,a1))),
% 60.81/60.85 inference(rename_variables,[],[7271])).
% 60.81/60.85 cnf(7605,plain,
% 60.81/60.85 (P5(f8(x76051),f17(x76051,x76052))),
% 60.81/60.85 inference(rename_variables,[],[7066])).
% 60.81/60.85 cnf(7615,plain,
% 60.81/60.85 (P4(f2(a6,f2(a6,a9)),a7)),
% 60.81/60.85 inference(scs_inference,[],[7534,7355,7039,7603,7421,7271,7604,7459,7510,7555,7448,7561,7559,7512,7601,7121,7437,7123,7066,7605,6850,7240,4624,6826,100,60,71,55,57,92,93,63,62,94,61,35,32,40,86,66,85,82])).
% 60.81/60.85 cnf(7647,plain,
% 60.81/60.85 (P5(f15(f8(a7),f17(a7,a7),f17(a1,a1)),a7)),
% 60.81/60.85 inference(scs_inference,[],[7537,7586,7578,7580,7602,7615,7217,7066,6927,96,60,71,55,57,92,93,67,70,63,62,94])).
% 60.81/60.85 cnf(7654,plain,
% 60.81/60.85 (P5(f11(f17(a6,a6),f17(a6,a7)),f5(a6,a7))),
% 60.81/60.85 inference(scs_inference,[],[7537,7598,7586,7578,7580,7602,7346,7615,6865,6971,7217,7066,7235,4534,6927,6860,96,60,71,55,57,92,93,67,70,63,62,94,36,61,32,40])).
% 60.81/60.85 cnf(7655,plain,
% 60.81/60.85 (P5(f15(f2(a6,a9),a6,a6),a6)),
% 60.81/60.85 inference(scs_inference,[],[7537,7598,7586,7578,7580,7602,7346,7615,6902,6865,6971,7179,7217,7066,7235,4534,6927,6860,96,60,71,55,57,92,93,67,70,63,62,94,36,61,32,40,86])).
% 60.81/60.85 cnf(7656,plain,
% 60.81/60.85 (~P6(x76561,a6,a6)),
% 60.81/60.85 inference(rename_variables,[],[6902])).
% 60.81/60.85 cnf(7658,plain,
% 60.81/60.85 (~E(f17(a6,a7),f17(f17(a6,a6),f17(a6,a6)))),
% 60.81/60.85 inference(scs_inference,[],[7537,7598,7586,7578,7580,7602,7346,7615,6902,6865,6971,7179,7217,7066,7235,4534,6927,6860,96,60,71,55,57,92,93,67,70,63,62,94,36,61,32,40,86,66])).
% 60.81/60.85 cnf(7660,plain,
% 60.81/60.85 (P5(f15(f11(a7,a6),a6,a6),a6)),
% 60.81/60.85 inference(scs_inference,[],[7537,7598,7586,7578,7580,7602,7346,7615,6902,7656,6865,6971,7179,7189,7217,7066,7235,4534,6927,6860,96,60,71,55,57,92,93,67,70,63,62,94,36,61,32,40,86,66,85])).
% 60.81/60.85 cnf(7674,plain,
% 60.81/60.85 (P5(f11(f17(a6,a6),f5(a6,a7)),f5(a6,a7))),
% 60.81/60.85 inference(scs_inference,[],[7599,7660,100,60])).
% 60.81/60.85 cnf(7676,plain,
% 60.81/60.85 (~P5(f11(f17(a6,a6),f5(a6,a7)),f17(a6,a6))),
% 60.81/60.85 inference(scs_inference,[],[7599,7660,100,60,71])).
% 60.81/60.85 cnf(7687,plain,
% 60.81/60.85 (P5(f8(x76871),f17(x76872,x76871))),
% 60.81/60.85 inference(rename_variables,[],[7064])).
% 60.81/60.85 cnf(7699,plain,
% 60.81/60.85 (~P7(a6,f17(a7,a7))),
% 60.81/60.85 inference(scs_inference,[],[7599,7588,7273,7172,7654,7400,7594,7660,7261,7390,6992,6980,6983,7064,7580,6860,100,60,71,55,57,92,93,563,63,62,94,59,33,36,61])).
% 60.81/60.85 cnf(7704,plain,
% 60.81/60.85 (P5(f8(a6),f17(a1,x77041))),
% 60.81/60.85 inference(rename_variables,[],[7201])).
% 60.81/60.85 cnf(7705,plain,
% 60.81/60.85 (~P6(x77051,f17(a1,x77052),f17(a6,a6))),
% 60.81/60.85 inference(rename_variables,[],[7000])).
% 60.81/60.85 cnf(7706,plain,
% 60.81/60.85 (P5(f8(x77061),f17(x77062,x77061))),
% 60.81/60.85 inference(rename_variables,[],[7064])).
% 60.81/60.85 cnf(7710,plain,
% 60.81/60.85 (P5(f15(f8(a6),f17(a1,x77101),f17(a6,a6)),f17(a6,a6))),
% 60.81/60.85 inference(scs_inference,[],[7599,7000,7705,7588,7273,7172,7654,7400,7594,7658,7660,7201,7704,7261,7390,6992,6980,6983,7064,7687,7706,7580,6850,4572,4600,4624,6860,100,60,71,55,57,92,93,563,63,62,94,59,33,36,61,3,40,86,66,85])).
% 60.81/60.85 cnf(7713,plain,
% 60.81/60.85 (P5(f8(x77131),f17(x77132,x77131))),
% 60.81/60.85 inference(rename_variables,[],[7064])).
% 60.81/60.85 cnf(7719,plain,
% 60.81/60.85 (~P6(x77191,f17(a1,x77192),f17(a6,a7))),
% 60.81/60.85 inference(scs_inference,[],[7599,7000,7705,7588,7273,7172,7654,7400,7594,7658,7660,7201,7704,7261,7390,6992,6980,6983,7064,7687,7706,7713,7580,6850,4572,4600,4624,6860,4804,100,60,71,55,57,92,93,563,63,62,94,59,33,36,61,3,40,86,66,85,102,68,152])).
% 60.81/60.85 cnf(7732,plain,
% 60.81/60.85 (~P5(f11(f17(a7,a7),a6),f17(a7,a7))),
% 60.81/60.85 inference(scs_inference,[],[7699,60,71])).
% 60.81/60.85 cnf(7756,plain,
% 60.81/60.85 (~P5(f8(a7),a6)),
% 60.81/60.85 inference(scs_inference,[],[7699,7719,7518,7674,7676,7453,7710,7259,7263,7555,7013,6867,7217,6950,4534,7240,6927,6826,4389,60,71,55,57,92,93,63,68,62,94,36,61,3,40,82])).
% 60.81/60.85 cnf(7764,plain,
% 60.81/60.85 (P5(f15(f8(a6),f17(a6,a6),f17(a1,x77641)),f17(a6,a6))),
% 60.81/60.85 inference(scs_inference,[],[7699,6999,7719,7518,7674,7676,7453,7710,7259,7263,7555,7013,7201,6867,7217,7064,6950,4534,7240,6927,6826,4389,4804,60,71,55,57,92,93,63,68,62,94,36,61,3,40,82,100,69,86])).
% 60.81/60.85 cnf(7781,plain,
% 60.81/60.85 (P5(f11(a6,f17(a6,a7)),f17(a6,a7))),
% 60.81/60.85 inference(scs_inference,[],[4598,60])).
% 60.81/60.85 cnf(7783,plain,
% 60.81/60.85 (~P5(f11(a6,f17(a6,a7)),a6)),
% 60.81/60.85 inference(scs_inference,[],[4598,60,71])).
% 60.81/60.85 cnf(7787,plain,
% 60.81/60.85 (~P2(f2(a6,a9),a6)),
% 60.81/60.85 inference(scs_inference,[],[7756,4598,7054,60,71,55,57])).
% 60.81/60.85 cnf(7795,plain,
% 60.81/60.85 (P7(f12(f8(a6),f17(a6,a7)),f17(a6,a7))),
% 60.81/60.85 inference(scs_inference,[],[7520,7756,7647,4598,7054,7066,6826,96,60,71,55,57,92,93,62,69])).
% 60.81/60.85 cnf(7796,plain,
% 60.81/60.85 (P5(f8(x77961),f17(x77961,x77962))),
% 60.81/60.85 inference(rename_variables,[],[7066])).
% 60.81/60.85 cnf(7797,plain,
% 60.81/60.85 (~P4(x77971,f17(a6,a7))),
% 60.81/60.85 inference(rename_variables,[],[96])).
% 60.81/60.85 cnf(7805,plain,
% 60.81/60.85 (~P5(f11(a7,a1),f17(f17(a7,a7),f17(a7,a7)))),
% 60.81/60.85 inference(scs_inference,[],[7520,7756,7647,7655,4598,7054,7066,7796,7487,6826,96,7797,60,71,55,57,92,93,62,69,67,63,94])).
% 60.81/60.85 cnf(7832,plain,
% 60.81/60.85 (P5(f11(a1,f17(a6,a7)),f17(a6,a7))),
% 60.81/60.85 inference(scs_inference,[],[4500,60])).
% 60.81/60.85 cnf(7834,plain,
% 60.81/60.85 (~P5(f11(a1,f17(a6,a7)),a1)),
% 60.81/60.85 inference(scs_inference,[],[4500,60,71])).
% 60.81/60.85 cnf(7838,plain,
% 60.81/60.85 (~P2(a9,a7)),
% 60.81/60.85 inference(scs_inference,[],[7732,6990,4500,60,71,55,57])).
% 60.81/60.85 cnf(7853,plain,
% 60.81/60.85 (P5(f8(x78531),f17(x78532,f17(x78533,x78531)))),
% 60.81/60.85 inference(rename_variables,[],[7129])).
% 60.81/60.85 cnf(7862,plain,
% 60.81/60.85 (P5(f15(f8(a7),f17(a6,a7),f17(a6,a7)),f17(a6,a7))),
% 60.81/60.85 inference(scs_inference,[],[7787,6948,6952,7732,7764,7781,7129,7853,7805,6904,7323,6902,7756,6980,6990,7064,7240,6860,4500,60,71,55,57,92,93,63,62,94,61,39,37,40,86,66,85])).
% 60.81/60.85 cnf(7866,plain,
% 60.81/60.85 (~P5(f11(a1,f17(a6,a7)),a7)),
% 60.81/60.85 inference(scs_inference,[],[7787,6948,6952,7732,7764,7781,7129,7853,7805,6904,7323,6902,7756,6980,6990,7064,7240,6860,4500,60,71,55,57,92,93,63,62,94,61,39,37,40,86,66,85,115])).
% 60.81/60.85 cnf(7898,plain,
% 60.81/60.85 (P5(f11(a6,f17(a6,a7)),a7)),
% 60.81/60.85 inference(scs_inference,[],[7832,6899,7783,7834,7781,55,92,93,62,63,94])).
% 60.81/60.85 cnf(7902,plain,
% 60.81/60.85 (P5(f8(x79021),f17(f17(x79022,x79021),x79023))),
% 60.81/60.85 inference(rename_variables,[],[7131])).
% 60.81/60.85 cnf(7908,plain,
% 60.81/60.85 (P5(f15(f8(a7),f17(a7,a7),f17(x79081,a1)),f17(a7,a7))),
% 60.81/60.85 inference(scs_inference,[],[7838,7832,7131,7902,6899,7783,7834,7041,7070,7271,7781,7756,7064,6860,47,55,92,93,62,63,94,35,61,37,40,86])).
% 60.81/60.85 cnf(7913,plain,
% 60.81/60.85 (~E(f17(a6,a7),f17(a1,a1))),
% 60.81/60.85 inference(scs_inference,[],[7838,7832,7131,7902,6899,7783,7834,7041,7070,7271,7781,7756,7064,6860,47,55,92,93,62,63,94,35,61,37,40,86,66])).
% 60.81/60.85 cnf(7944,plain,
% 60.81/60.85 (~E(f5(a6,a7),f17(a1,a1))),
% 60.81/60.85 inference(scs_inference,[],[7913,7908,7220,7866,7898,6824,7783,7832,6860,55,92,93,63,62,94,61,3])).
% 60.81/60.85 cnf(7945,plain,
% 60.81/60.85 (P5(f15(f8(a7),f17(a6,a7),f17(a6,a7)),f5(a6,a7))),
% 60.81/60.85 inference(scs_inference,[],[7913,7908,7220,7866,7898,7862,6824,7783,7832,6860,55,92,93,63,62,94,61,3,40])).
% 60.81/60.85 cnf(7948,plain,
% 60.81/60.85 (P5(f11(a6,a7),a1)),
% 60.81/60.85 inference(scs_inference,[],[7913,7908,7220,7866,7141,7898,7862,6824,7783,7832,7756,6860,55,92,93,63,62,94,61,3,40,66,119])).
% 60.81/60.85 cnf(7950,plain,
% 60.81/60.85 (P5(f11(a6,a7),a7)),
% 60.81/60.85 inference(scs_inference,[],[7913,7908,7220,7866,7141,7898,7862,6824,7783,7832,7756,6860,55,92,93,63,62,94,61,3,40,66,119,60])).
% 60.81/60.85 cnf(7952,plain,
% 60.81/60.85 (~P5(f11(a6,a7),a6)),
% 60.81/60.85 inference(scs_inference,[],[7913,7908,7220,7866,7141,7898,7862,6824,7783,7832,7756,6860,55,92,93,63,62,94,61,3,40,66,119,60,71])).
% 60.81/60.85 cnf(7962,plain,
% 60.81/60.85 (P5(f11(a6,a7),f17(x79621,a7))),
% 60.81/60.85 inference(scs_inference,[],[7952,7950,55,92])).
% 60.81/60.85 cnf(7964,plain,
% 60.81/60.85 (P5(f11(a6,a7),f17(a7,x79641))),
% 60.81/60.85 inference(scs_inference,[],[7952,7950,55,92,93])).
% 60.81/60.85 cnf(7970,plain,
% 60.81/60.85 (P2(f15(f8(a7),f17(a6,a7),f17(a6,a7)),f5(a6,a7))),
% 60.81/60.85 inference(scs_inference,[],[7952,7950,7945,6927,55,92,93,62,63,59])).
% 60.81/60.85 cnf(7973,plain,
% 60.81/60.85 (~P5(f11(a1,f17(a6,a7)),f17(a7,a7))),
% 60.81/60.85 inference(scs_inference,[],[7952,7950,7945,7866,6927,55,92,93,62,63,59,94])).
% 60.81/60.85 cnf(7981,plain,
% 60.81/60.85 (~P6(x79811,a1,f17(a7,a7))),
% 60.81/60.85 inference(rename_variables,[],[7038])).
% 60.81/60.85 cnf(7985,plain,
% 60.81/60.85 (P5(f15(f11(a6,a7),a1,f17(a7,a7)),f17(a7,a7))),
% 60.81/60.85 inference(scs_inference,[],[7952,7950,7948,7795,7945,7206,7038,7981,7382,7866,7235,6927,7756,6860,55,92,93,62,63,59,94,33,61,3,40,86,66,85])).
% 60.81/60.85 cnf(7988,plain,
% 60.81/60.85 (~P5(f15(a9,a6,a6),a7)),
% 60.81/60.85 inference(scs_inference,[],[7952,7950,7948,7795,7945,7206,7038,7981,7382,7866,7555,6992,6980,7235,6927,7756,6860,55,92,93,62,63,59,94,33,61,3,40,86,66,85,83])).
% 60.81/60.85 cnf(8003,plain,
% 60.81/60.85 (~P4(x80031,f17(a6,a7))),
% 60.81/60.85 inference(rename_variables,[],[96])).
% 60.81/60.85 cnf(8004,plain,
% 60.81/60.85 (P5(f11(a6,a7),f17(x80041,a7))),
% 60.81/60.85 inference(rename_variables,[],[7962])).
% 60.81/60.85 cnf(8007,plain,
% 60.81/60.85 (~P4(x80071,f17(a6,a7))),
% 60.81/60.85 inference(rename_variables,[],[96])).
% 60.81/60.85 cnf(8008,plain,
% 60.81/60.85 (P5(f11(a6,a7),f17(x80081,a7))),
% 60.81/60.85 inference(rename_variables,[],[7962])).
% 60.81/60.85 cnf(8011,plain,
% 60.81/60.85 (P5(f11(a6,a7),f17(x80111,a7))),
% 60.81/60.85 inference(rename_variables,[],[7962])).
% 60.81/60.85 cnf(8012,plain,
% 60.81/60.85 (~P4(x80121,f17(a6,a7))),
% 60.81/60.85 inference(rename_variables,[],[96])).
% 60.81/60.85 cnf(8016,plain,
% 60.81/60.85 (P5(f11(a6,a7),f17(x80161,a7))),
% 60.81/60.85 inference(rename_variables,[],[7962])).
% 60.81/60.85 cnf(8029,plain,
% 60.81/60.85 (P5(f11(a6,a7),f5(a6,a7))),
% 60.81/60.85 inference(scs_inference,[],[7944,7962,8004,8008,8011,8016,7988,7970,7985,7074,6944,6940,6892,6860,6826,96,8003,8007,8012,55,92,93,69,70,67,68,63,62,53,94,38,61,40])).
% 60.81/60.85 cnf(8030,plain,
% 60.81/60.85 (P5(f11(a6,a7),f17(x80301,a7))),
% 60.81/60.85 inference(rename_variables,[],[7962])).
% 60.81/60.85 cnf(8032,plain,
% 60.81/60.85 (~P6(x80321,f17(x80322,a1),f17(a7,a7))),
% 60.81/60.85 inference(rename_variables,[],[7043])).
% 60.81/60.85 cnf(8033,plain,
% 60.81/60.85 (P5(f11(a6,a7),f17(x80331,a7))),
% 60.81/60.85 inference(rename_variables,[],[7962])).
% 60.81/60.85 cnf(8034,plain,
% 60.81/60.85 (P5(f11(a6,a7),f17(a7,x80341))),
% 60.81/60.85 inference(rename_variables,[],[7964])).
% 60.81/60.85 cnf(8045,plain,
% 60.81/60.85 (P5(f11(f17(a1,a1),f5(a6,a7)),f5(a6,a7))),
% 60.81/60.85 inference(scs_inference,[],[7944,7962,8004,8008,8011,8016,8030,8033,7964,8034,7988,7970,7985,7074,7043,8032,6944,6940,6892,6860,6826,96,8003,8007,8012,55,92,93,69,70,67,68,63,62,53,94,38,61,40,86,66,85,117,60])).
% 60.81/60.85 cnf(8047,plain,
% 60.81/60.85 (~P5(f11(f17(a1,a1),f5(a6,a7)),f17(a1,a1))),
% 60.81/60.85 inference(scs_inference,[],[7944,7962,8004,8008,8011,8016,8030,8033,7964,8034,7988,7970,7985,7074,7043,8032,6944,6940,6892,6860,6826,96,8003,8007,8012,55,92,93,69,70,67,68,63,62,53,94,38,61,40,86,66,85,117,60,71])).
% 60.81/60.85 cnf(8065,plain,
% 60.81/60.85 (~P4(x80651,f5(a6,a7))),
% 60.81/60.85 inference(rename_variables,[],[6927])).
% 60.81/60.85 cnf(8068,plain,
% 60.81/60.85 (~P4(x80681,f5(a6,a7))),
% 60.81/60.85 inference(rename_variables,[],[6927])).
% 60.81/60.85 cnf(8071,plain,
% 60.81/60.85 (~P4(x80711,f5(a6,a7))),
% 60.81/60.85 inference(rename_variables,[],[6927])).
% 60.81/60.85 cnf(8074,plain,
% 60.81/60.85 (~P4(x80741,f5(a6,a7))),
% 60.81/60.85 inference(rename_variables,[],[6927])).
% 60.81/60.85 cnf(8083,plain,
% 60.81/60.85 ($false),
% 60.81/60.85 inference(scs_inference,[],[8029,7973,8045,8047,7866,6824,7832,6927,8065,8068,8071,8074,55,92,93,70,67,69,68,59,63,62,94]),
% 60.81/60.85 ['proof']).
% 60.81/60.85 % SZS output end Proof
% 60.81/60.85 % Total time :60.200000s
%------------------------------------------------------------------------------