%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : GEO084-1 : TPTP v8.2.0. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% Computer : n019.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:43 EDT 2024
% Result : Unsatisfiable 119.03s 119.45s
% Output : CNFRefutation 119.12s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.13 % Problem : GEO084-1 : TPTP v8.2.0. Released v2.4.0.
% 0.07/0.13 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% 0.13/0.34 % Computer : n019.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % WCLimit : 300
% 0.13/0.34 % DateTime : Fri Jun 21 07:17:39 EDT 2024
% 0.13/0.34 % CPUTime :
% 0.54/0.60 start to proof:theBenchmark
% 118.93/119.42 %-------------------------------------------
% 118.93/119.42 % File :CSE---1.7
% 118.93/119.42 % Problem :theBenchmark
% 118.93/119.42 % Transform :cnf
% 118.93/119.43 % Format :tptp:raw
% 118.93/119.43 % Command :java -jar mcs_scs.jar %d %s
% 118.93/119.43
% 118.93/119.43 % Result :Theorem 118.410000s
% 118.93/119.43 % Output :CNFRefutation 118.410000s
% 118.93/119.43 %-------------------------------------------
% 119.03/119.45 %--------------------------------------------------------------------------
% 119.03/119.45 % File : GEO084-1 : TPTP v8.2.0. Released v2.4.0.
% 119.03/119.45 % Domain : Geometry (Oriented curves)
% 119.03/119.45 % Problem : Sum is monotone, part 2
% 119.03/119.45 % Version : [EHK99] axioms.
% 119.03/119.45 % English :
% 119.03/119.45
% 119.03/119.45 % Refs : [KE99] Kulik & Eschenbach (1999), A Geometry of Oriented Curv
% 119.03/119.45 % : [EHK99] Eschenbach et al. (1999), Representing Simple Trajecto
% 119.03/119.45 % Source : [TPTP]
% 119.03/119.45 % Names :
% 119.03/119.45
% 119.03/119.45 % Status : Unsatisfiable
% 119.03/119.45 % Rating : 0.20 v8.2.0, 0.24 v8.1.0, 0.11 v7.5.0, 0.16 v7.4.0, 0.24 v7.3.0, 0.17 v7.1.0, 0.08 v7.0.0, 0.20 v6.4.0, 0.13 v6.3.0, 0.18 v6.2.0, 0.10 v6.1.0, 0.21 v6.0.0, 0.20 v5.5.0, 0.50 v5.3.0, 0.44 v5.2.0, 0.38 v5.1.0, 0.47 v5.0.0, 0.29 v4.1.0, 0.54 v4.0.1, 0.64 v4.0.0, 0.55 v3.7.0, 0.30 v3.5.0, 0.36 v3.4.0, 0.25 v3.3.0, 0.36 v3.2.0, 0.31 v3.1.0, 0.27 v2.7.0, 0.25 v2.6.0, 0.22 v2.5.0, 0.44 v2.4.0
% 119.03/119.45 % Syntax : Number of clauses : 52 ( 5 unt; 21 nHn; 47 RR)
% 119.03/119.45 % Number of literals : 158 ( 21 equ; 79 neg)
% 119.03/119.45 % Maximal clause size : 12 ( 3 avg)
% 119.03/119.45 % Maximal term depth : 3 ( 1 avg)
% 119.03/119.45 % Number of predicates : 8 ( 7 usr; 0 prp; 1-3 aty)
% 119.03/119.45 % Number of functors : 18 ( 18 usr; 4 con; 0-3 aty)
% 119.03/119.45 % Number of variables : 126 ( 10 sgn)
% 119.03/119.45 % SPC : CNF_UNS_RFO_SEQ_NHN
% 119.03/119.45
% 119.03/119.45 % Comments : Created by tptp2X -f tptp -t clausify:otter GEO084+1.p
% 119.03/119.45 %--------------------------------------------------------------------------
% 119.03/119.45 %----Include simple curve axioms
% 119.03/119.45 include('Axioms/GEO004-0.ax').
% 119.03/119.45 %--------------------------------------------------------------------------
% 119.03/119.45 cnf(corollary_2_6_2_67,negated_conjecture,
% 119.03/119.45 part_of(sk14,sk16) ).
% 119.03/119.45
% 119.03/119.45 cnf(corollary_2_6_2_68,negated_conjecture,
% 119.03/119.45 part_of(sk15,sk16) ).
% 119.03/119.45
% 119.03/119.45 cnf(corollary_2_6_2_69,negated_conjecture,
% 119.03/119.45 meet(sk17,sk14,sk15) ).
% 119.03/119.45
% 119.03/119.45 cnf(corollary_2_6_2_70,negated_conjecture,
% 119.03/119.45 ~ part_of(sum(sk14,sk15),sk16) ).
% 119.03/119.45
% 119.03/119.45 %--------------------------------------------------------------------------
% 119.03/119.45 %-------------------------------------------
% 119.03/119.45 % Proof found
% 119.03/119.45 % SZS status Theorem for theBenchmark
% 119.03/119.45 % SZS output start Proof
% 119.03/119.47 %ClaNum:90(EqnAxiom:43)
% 119.03/119.47 %VarNum:331(SingletonVarNum:113)
% 119.03/119.47 %MaxLitNum:12
% 119.03/119.47 %MaxfuncDepth:2
% 119.03/119.47 %SharedTerms:9
% 119.03/119.47 %goalClause: 44 45 47 48
% 119.03/119.47 %singleGoalClaCount:4
% 119.03/119.47 [44]P1(a1,a15)
% 119.03/119.47 [45]P1(a16,a15)
% 119.03/119.47 [47]P6(a17,a1,a16)
% 119.03/119.47 [48]~P1(f18(a1,a16),a15)
% 119.03/119.47 [46]P2(f2(x461),x461)
% 119.03/119.47 [49]P3(x491)+P4(f3(x491),x491)
% 119.03/119.47 [51]~P7(x511)+P4(f13(x511),x511)
% 119.03/119.47 [50]P7(x501)+~P4(x502,x501)
% 119.03/119.47 [53]~P3(x531)+~P4(x532,x531)
% 119.03/119.47 [54]~P4(x541,x542)+P5(x541,x542)
% 119.03/119.47 [55]~P2(x551,x552)+P5(x551,x552)
% 119.03/119.47 [56]~P2(x561,x562)+~P4(x561,x562)
% 119.03/119.47 [57]~P4(x571,x572)+~E(f4(x571,x572),x571)
% 119.03/119.47 [59]P1(x591,x592)+P5(f5(x591,x592),x591)
% 119.03/119.47 [63]~P4(x631,x632)+P4(f4(x631,x632),x632)
% 119.03/119.47 [70]P1(x701,x702)+~P5(f5(x701,x702),x702)
% 119.03/119.47 [77]~P2(x771,x772)+P6(x771,f14(x771,x772),f6(x771,x772))
% 119.03/119.47 [72]~P2(x721,x722)+E(f18(f14(x721,x722),f6(x721,x722)),x722)
% 119.03/119.47 [73]P5(x731,x732)+~P6(x731,x733,x732)
% 119.03/119.47 [74]P5(x741,x742)+~P6(x741,x742,x743)
% 119.03/119.47 [75]~P6(x753,x752,x751)+E(f9(x751,x752),f18(x752,x751))
% 119.03/119.47 [52]P7(x521)+~P1(x521,x522)+E(x521,x522)
% 119.03/119.47 [58]P2(x581,x582)+~P5(x581,x582)+P4(x581,x582)
% 119.03/119.47 [66]~P5(x661,x662)+P4(x661,x662)+P5(x661,f7(x662,x661))
% 119.03/119.47 [67]~P5(x671,x672)+P4(x671,x672)+P5(x671,f11(x672,x671))
% 119.03/119.47 [68]~P5(x681,x682)+P4(x681,x682)+P1(f7(x682,x681),x682)
% 119.03/119.47 [69]~P5(x691,x692)+P4(x691,x692)+P1(f11(x692,x691),x692)
% 119.03/119.47 [71]E(x711,x712)+P5(f8(x711,x712),x712)+P5(f8(x711,x712),x711)
% 119.03/119.47 [76]E(x761,x762)+~P5(f8(x761,x762),x762)+~P5(f8(x761,x762),x761)
% 119.03/119.47 [78]~P5(x781,x782)+P4(x781,x782)+~P1(f7(x782,x781),f11(x782,x781))
% 119.03/119.47 [79]~P5(x791,x792)+P4(x791,x792)+~P1(f11(x792,x791),f7(x792,x791))
% 119.03/119.47 [60]~P5(x601,x603)+P5(x601,x602)+~P1(x603,x602)
% 119.03/119.47 [88]~P5(f10(x883,x882,x881),x881)+~P5(f10(x883,x882,x881),x882)+E(x881,f18(x882,x883))
% 119.03/119.47 [89]~P5(f10(x893,x892,x891),x891)+~P5(f10(x893,x892,x891),x893)+E(x891,f18(x892,x893))
% 119.03/119.47 [61]~P5(x611,x614)+P5(x611,x612)+~E(x612,f18(x613,x614))
% 119.03/119.47 [62]~P5(x621,x623)+P5(x621,x622)+~E(x622,f18(x623,x624))
% 119.03/119.47 [84]~P5(x841,x843)+~P5(x841,x842)+P6(x841,x842,x843)+P5(f12(x843,x842,x841),x843)
% 119.03/119.47 [85]~P5(x851,x853)+~P5(x851,x852)+P6(x851,x852,x853)+P5(f12(x853,x852,x851),x852)
% 119.03/119.47 [87]P5(f10(x873,x872,x871),x871)+P5(f10(x873,x872,x871),x872)+P5(f10(x873,x872,x871),x873)+E(x871,f18(x872,x873))
% 119.03/119.47 [81]~P5(x811,x812)+P4(x811,x812)+~P6(x814,x813,x812)+~P5(x811,x813)
% 119.03/119.47 [82]~P5(x821,x822)+P4(x821,x822)+~P6(x824,x822,x823)+~P5(x821,x823)
% 119.03/119.47 [65]~P5(x651,x654)+P5(x651,x652)+P5(x651,x653)+~E(x654,f18(x653,x652))
% 119.03/119.47 [90]~P5(x901,x903)+~P5(x901,x902)+P6(x901,x902,x903)+~P4(f12(x903,x902,x901),x903)+~P4(f12(x903,x902,x901),x902)
% 119.03/119.47 [83]~P3(x834)+~P4(x831,x832)+P6(x831,x832,x833)+~P6(x835,x832,x833)+~E(x834,f18(x832,x833))
% 119.03/119.47 [64]E(x643,x641)+~P4(x641,x644)+~P4(x643,x644)+E(x641,x642)+E(x643,x642)+~P4(x642,x644)
% 119.03/119.47 [80]P1(x802,x801)+~P1(x802,x803)+~P5(x804,x802)+~P4(x804,x803)+P1(x801,x802)+~P1(x801,x803)+~P5(x804,x801)
% 119.03/119.47 [86]P1(x862,x861)+P1(x862,x863)+P1(x863,x861)+P1(x863,x862)+~P1(x862,x864)+~P1(x863,x864)+~P4(x865,x862)+~P4(x865,x863)+P1(x861,x862)+P1(x861,x863)+~P1(x861,x864)+~P4(x865,x861)
% 119.03/119.47 %EqnAxiom
% 119.03/119.47 [1]E(x11,x11)
% 119.03/119.47 [2]E(x22,x21)+~E(x21,x22)
% 119.03/119.47 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 119.03/119.47 [4]~E(x41,x42)+E(f2(x41),f2(x42))
% 119.03/119.47 [5]~E(x51,x52)+E(f18(x51,x53),f18(x52,x53))
% 119.03/119.47 [6]~E(x61,x62)+E(f18(x63,x61),f18(x63,x62))
% 119.03/119.47 [7]~E(x71,x72)+E(f3(x71),f3(x72))
% 119.03/119.47 [8]~E(x81,x82)+E(f13(x81),f13(x82))
% 119.03/119.47 [9]~E(x91,x92)+E(f4(x91,x93),f4(x92,x93))
% 119.03/119.47 [10]~E(x101,x102)+E(f4(x103,x101),f4(x103,x102))
% 119.03/119.47 [11]~E(x111,x112)+E(f5(x111,x113),f5(x112,x113))
% 119.03/119.47 [12]~E(x121,x122)+E(f5(x123,x121),f5(x123,x122))
% 119.03/119.47 [13]~E(x131,x132)+E(f12(x131,x133,x134),f12(x132,x133,x134))
% 119.03/119.47 [14]~E(x141,x142)+E(f12(x143,x141,x144),f12(x143,x142,x144))
% 119.03/119.47 [15]~E(x151,x152)+E(f12(x153,x154,x151),f12(x153,x154,x152))
% 119.03/119.47 [16]~E(x161,x162)+E(f10(x161,x163,x164),f10(x162,x163,x164))
% 119.03/119.47 [17]~E(x171,x172)+E(f10(x173,x171,x174),f10(x173,x172,x174))
% 119.03/119.47 [18]~E(x181,x182)+E(f10(x183,x184,x181),f10(x183,x184,x182))
% 119.03/119.47 [19]~E(x191,x192)+E(f7(x191,x193),f7(x192,x193))
% 119.03/119.47 [20]~E(x201,x202)+E(f7(x203,x201),f7(x203,x202))
% 119.03/119.47 [21]~E(x211,x212)+E(f11(x211,x213),f11(x212,x213))
% 119.03/119.47 [22]~E(x221,x222)+E(f11(x223,x221),f11(x223,x222))
% 119.03/119.47 [23]~E(x231,x232)+E(f14(x231,x233),f14(x232,x233))
% 119.03/119.47 [24]~E(x241,x242)+E(f14(x243,x241),f14(x243,x242))
% 119.03/119.47 [25]~E(x251,x252)+E(f6(x251,x253),f6(x252,x253))
% 119.03/119.47 [26]~E(x261,x262)+E(f6(x263,x261),f6(x263,x262))
% 119.03/119.47 [27]~E(x271,x272)+E(f8(x271,x273),f8(x272,x273))
% 119.03/119.47 [28]~E(x281,x282)+E(f8(x283,x281),f8(x283,x282))
% 119.03/119.47 [29]~E(x291,x292)+E(f9(x291,x293),f9(x292,x293))
% 119.03/119.47 [30]~E(x301,x302)+E(f9(x303,x301),f9(x303,x302))
% 119.03/119.47 [31]P1(x312,x313)+~E(x311,x312)+~P1(x311,x313)
% 119.03/119.47 [32]P1(x323,x322)+~E(x321,x322)+~P1(x323,x321)
% 119.03/119.47 [33]P4(x332,x333)+~E(x331,x332)+~P4(x331,x333)
% 119.03/119.47 [34]P4(x343,x342)+~E(x341,x342)+~P4(x343,x341)
% 119.03/119.47 [35]P2(x352,x353)+~E(x351,x352)+~P2(x351,x353)
% 119.03/119.47 [36]P2(x363,x362)+~E(x361,x362)+~P2(x363,x361)
% 119.03/119.47 [37]P6(x372,x373,x374)+~E(x371,x372)+~P6(x371,x373,x374)
% 119.03/119.47 [38]P6(x383,x382,x384)+~E(x381,x382)+~P6(x383,x381,x384)
% 119.03/119.47 [39]P6(x393,x394,x392)+~E(x391,x392)+~P6(x393,x394,x391)
% 119.03/119.47 [40]P5(x402,x403)+~E(x401,x402)+~P5(x401,x403)
% 119.03/119.47 [41]P5(x413,x412)+~E(x411,x412)+~P5(x413,x411)
% 119.03/119.47 [42]~P3(x421)+P3(x422)+~E(x421,x422)
% 119.03/119.47 [43]~P7(x431)+P7(x432)+~E(x431,x432)
% 119.03/119.47
% 119.03/119.47 %-------------------------------------------
% 119.03/119.50 cnf(91,plain,
% 119.03/119.50 (~P5(x911,x912)+P5(x911,f18(x913,x912))),
% 119.03/119.50 inference(equality_inference,[],[61])).
% 119.03/119.50 cnf(92,plain,
% 119.03/119.50 (~P5(x921,x922)+P5(x921,f18(x922,x923))),
% 119.03/119.51 inference(equality_inference,[],[62])).
% 119.03/119.51 cnf(93,plain,
% 119.03/119.51 (~P5(x931,f18(x932,x933))+P5(x931,x933)+P5(x931,x932)),
% 119.03/119.51 inference(equality_inference,[],[65])).
% 119.03/119.51 cnf(96,plain,
% 119.03/119.51 (~P5(f10(a16,a1,a1),a1)),
% 119.03/119.51 inference(scs_inference,[],[44,48,31,88])).
% 119.03/119.51 cnf(98,plain,
% 119.03/119.51 (P5(f10(a16,a1,a1),a16)),
% 119.03/119.51 inference(scs_inference,[],[44,48,31,88,87])).
% 119.03/119.51 cnf(104,plain,
% 119.03/119.51 (P5(f10(a16,a1,a1),f18(x1041,a16))),
% 119.03/119.51 inference(scs_inference,[],[44,48,31,88,87,73,74,91])).
% 119.03/119.51 cnf(106,plain,
% 119.03/119.51 (P5(f10(a16,a1,a1),f18(a16,x1061))),
% 119.03/119.51 inference(scs_inference,[],[44,48,31,88,87,73,74,91,92])).
% 119.03/119.51 cnf(108,plain,
% 119.03/119.51 (~P4(f10(a16,a1,a1),a1)),
% 119.03/119.51 inference(scs_inference,[],[44,48,31,88,87,73,74,91,92,54])).
% 119.03/119.51 cnf(110,plain,
% 119.03/119.51 (~P2(f10(a16,a1,a1),a1)),
% 119.03/119.51 inference(scs_inference,[],[44,48,31,88,87,73,74,91,92,54,55])).
% 119.03/119.51 cnf(114,plain,
% 119.03/119.51 (P5(f10(a16,a1,a1),a15)),
% 119.03/119.51 inference(scs_inference,[],[44,45,48,31,88,87,73,74,91,92,54,55,52,60])).
% 119.03/119.51 cnf(117,plain,
% 119.03/119.51 (~P5(f10(a16,a1,a1),f18(a1,a1))),
% 119.03/119.51 inference(scs_inference,[],[44,45,47,48,31,88,87,73,74,91,92,54,55,52,60,37,93])).
% 119.03/119.51 cnf(119,plain,
% 119.03/119.51 (~E(f2(a1),f10(a16,a1,a1))),
% 119.03/119.51 inference(scs_inference,[],[44,45,47,48,46,31,88,87,73,74,91,92,54,55,52,60,37,93,35])).
% 119.03/119.51 cnf(120,plain,
% 119.03/119.51 (P2(f2(x1201),x1201)),
% 119.03/119.51 inference(rename_variables,[],[46])).
% 119.03/119.51 cnf(125,plain,
% 119.03/119.51 (P2(f2(x1251),x1252)+~E(x1251,x1252)),
% 119.03/119.51 inference(scs_inference,[],[44,45,47,48,46,120,31,88,87,73,74,91,92,54,55,52,60,37,93,35,41,32,38,39,36])).
% 119.03/119.51 cnf(136,plain,
% 119.03/119.51 (P5(f10(a16,a1,a1),f18(x1361,a15))),
% 119.03/119.51 inference(scs_inference,[],[114,117,74,73,91])).
% 119.03/119.51 cnf(138,plain,
% 119.03/119.51 (P5(f10(a16,a1,a1),f18(a15,x1381))),
% 119.03/119.51 inference(scs_inference,[],[114,117,74,73,91,92])).
% 119.03/119.51 cnf(140,plain,
% 119.03/119.51 (~P2(f10(a16,a1,a1),f18(a1,a1))),
% 119.03/119.51 inference(scs_inference,[],[114,117,74,73,91,92,55])).
% 119.03/119.51 cnf(144,plain,
% 119.03/119.51 (~P5(f10(a16,a1,a1),f18(f18(a1,a1),f18(a1,a1)))),
% 119.03/119.51 inference(scs_inference,[],[114,117,74,73,91,92,55,54,93])).
% 119.03/119.51 cnf(146,plain,
% 119.03/119.51 (~E(a15,f18(a1,a1))),
% 119.03/119.51 inference(scs_inference,[],[114,117,74,73,91,92,55,54,93,41])).
% 119.03/119.51 cnf(147,plain,
% 119.03/119.51 (~E(a16,f18(a1,a16))),
% 119.03/119.51 inference(scs_inference,[],[45,48,114,117,74,73,91,92,55,54,93,41,31])).
% 119.03/119.51 cnf(151,plain,
% 119.03/119.51 (~P5(f10(a1,a1,a15),a1)),
% 119.03/119.51 inference(scs_inference,[],[44,45,48,114,117,74,73,91,92,55,54,93,41,31,89,40,60])).
% 119.03/119.51 cnf(156,plain,
% 119.03/119.51 (~P2(f10(a1,a1,a15),a1)),
% 119.03/119.51 inference(scs_inference,[],[151,73,55])).
% 119.03/119.51 cnf(158,plain,
% 119.03/119.51 (P5(f10(a16,a1,a1),f18(f18(x1581,a15),x1582))),
% 119.03/119.51 inference(scs_inference,[],[151,136,73,55,92])).
% 119.03/119.51 cnf(160,plain,
% 119.03/119.51 (~P4(f10(a1,a1,a15),a1)),
% 119.03/119.51 inference(scs_inference,[],[151,136,73,55,92,54])).
% 119.03/119.51 cnf(164,plain,
% 119.03/119.51 (~P6(f10(a1,a1,a15),a1,x1641)),
% 119.03/119.51 inference(scs_inference,[],[151,136,73,55,92,54,91,74])).
% 119.03/119.51 cnf(166,plain,
% 119.03/119.51 (~P5(f10(a16,a1,a16),a16)),
% 119.03/119.51 inference(scs_inference,[],[151,147,136,73,55,92,54,91,74,89])).
% 119.03/119.51 cnf(168,plain,
% 119.03/119.51 (~E(f2(f18(a1,a1)),f10(a16,a1,a1))),
% 119.03/119.51 inference(scs_inference,[],[151,147,136,46,140,73,55,92,54,91,74,89,35])).
% 119.03/119.51 cnf(170,plain,
% 119.03/119.51 (~P5(f10(a1,a1,a15),f18(a1,a1))),
% 119.03/119.51 inference(scs_inference,[],[151,147,136,46,140,73,55,92,54,91,74,89,35,93])).
% 119.03/119.51 cnf(174,plain,
% 119.03/119.51 (P5(f10(a16,a1,a16),a1)),
% 119.03/119.51 inference(scs_inference,[],[151,147,114,136,144,46,98,140,73,55,92,54,91,74,89,35,93,40,41,87])).
% 119.03/119.51 cnf(179,plain,
% 119.03/119.51 (P5(f10(a16,a1,a16),a15)),
% 119.03/119.51 inference(scs_inference,[],[44,151,147,114,136,144,46,98,140,73,55,92,54,91,74,89,35,93,40,41,87,18,88,60])).
% 119.12/119.51 cnf(189,plain,
% 119.12/119.51 (~P2(f10(a1,a1,a15),f18(a1,a1))),
% 119.12/119.51 inference(scs_inference,[],[170,55])).
% 119.12/119.51 cnf(193,plain,
% 119.12/119.51 (P5(f10(a16,a1,a16),f18(x1931,a15))),
% 119.12/119.51 inference(scs_inference,[],[179,170,55,54,91])).
% 119.12/119.51 cnf(197,plain,
% 119.12/119.51 (P5(f10(a16,a1,a16),f18(a15,x1971))),
% 119.12/119.51 inference(scs_inference,[],[179,170,55,54,91,73,92])).
% 119.12/119.51 cnf(201,plain,
% 119.12/119.51 (~P5(f10(a1,a1,a15),f18(f18(a1,a1),f18(a1,a1)))),
% 119.12/119.51 inference(scs_inference,[],[179,170,55,54,91,73,92,74,93])).
% 119.12/119.51 cnf(203,plain,
% 119.12/119.51 (~E(a17,f10(a1,a1,a15))),
% 119.12/119.51 inference(scs_inference,[],[47,164,179,170,55,54,91,73,92,74,93,37])).
% 119.12/119.51 cnf(205,plain,
% 119.12/119.51 (~E(f2(a1),f10(a1,a1,a15))),
% 119.12/119.51 inference(scs_inference,[],[47,164,179,170,46,156,55,54,91,73,92,74,93,37,35])).
% 119.12/119.51 cnf(209,plain,
% 119.12/119.51 (P5(f10(a1,a1,a15),a15)),
% 119.12/119.51 inference(scs_inference,[],[47,164,179,151,170,46,146,166,156,174,55,54,91,73,92,74,93,37,35,40,41,87])).
% 119.12/119.51 cnf(222,plain,
% 119.12/119.51 (~P2(f10(a1,a1,a15),f18(f18(a1,a1),f18(a1,a1)))),
% 119.12/119.51 inference(scs_inference,[],[201,138,54,92,73,55])).
% 119.12/119.51 cnf(228,plain,
% 119.12/119.51 (~P5(f10(a16,a1,a16),f18(a16,a16))),
% 119.12/119.51 inference(scs_inference,[],[201,138,166,54,92,73,55,74,91,93])).
% 119.12/119.51 cnf(230,plain,
% 119.12/119.51 (~E(f2(f18(a1,a1)),f10(a1,a1,a15))),
% 119.12/119.51 inference(scs_inference,[],[201,138,46,189,166,54,92,73,55,74,91,93,35])).
% 119.12/119.51 cnf(233,plain,
% 119.12/119.51 (~E(f18(x2331,a15),f18(a1,a1))),
% 119.12/119.51 inference(scs_inference,[],[158,201,138,144,46,189,166,54,92,73,55,74,91,93,35,41,5])).
% 119.12/119.51 cnf(243,plain,
% 119.12/119.51 (P5(f10(a16,a1,a1),f18(f18(a16,x2431),x2432))),
% 119.12/119.51 inference(scs_inference,[],[106,92])).
% 119.12/119.51 cnf(245,plain,
% 119.12/119.51 (~P2(f10(a16,a1,a16),f18(a16,a16))),
% 119.12/119.51 inference(scs_inference,[],[106,228,92,55])).
% 119.12/119.51 cnf(251,plain,
% 119.12/119.51 (P5(f10(a16,a1,a1),f18(x2511,f18(a16,x2512)))),
% 119.12/119.51 inference(scs_inference,[],[106,228,92,55,74,54,91])).
% 119.12/119.51 cnf(255,plain,
% 119.12/119.51 (~P5(f10(a16,a1,a16),f18(f18(a16,a16),f18(a16,a16)))),
% 119.12/119.51 inference(scs_inference,[],[106,228,92,55,74,54,91,73,93])).
% 119.12/119.51 cnf(257,plain,
% 119.12/119.51 (~E(a15,f18(a16,a16))),
% 119.12/119.51 inference(scs_inference,[],[179,106,228,92,55,74,54,91,73,93,41])).
% 119.12/119.51 cnf(270,plain,
% 119.12/119.51 (P5(f10(a16,a1,a1),f18(x2701,f18(x2702,a16)))),
% 119.12/119.51 inference(scs_inference,[],[104,255,55,54,91])).
% 119.12/119.51 cnf(292,plain,
% 119.12/119.51 (P5(f10(a16,a1,a16),f18(f18(x2921,a15),x2922))),
% 119.12/119.51 inference(scs_inference,[],[193,144,54,73,92])).
% 119.12/119.51 cnf(298,plain,
% 119.12/119.51 (P5(f10(a16,a1,a16),f18(x2981,f18(x2982,a15)))),
% 119.12/119.51 inference(scs_inference,[],[193,144,54,73,92,74,55,91])).
% 119.12/119.51 cnf(309,plain,
% 119.12/119.51 (~P6(f10(a16,a1,a16),x3091,a16)),
% 119.12/119.51 inference(scs_inference,[],[166,73])).
% 119.12/119.51 cnf(311,plain,
% 119.12/119.51 (~P2(f10(a16,a1,a16),a16)),
% 119.12/119.52 inference(scs_inference,[],[166,73,55])).
% 119.12/119.52 cnf(315,plain,
% 119.12/119.52 (~P4(f10(a16,a1,a16),a16)),
% 119.12/119.52 inference(scs_inference,[],[166,73,55,74,54])).
% 119.12/119.52 cnf(317,plain,
% 119.12/119.52 (P5(f10(a16,a1,a16),f18(x3171,f18(a15,x3172)))),
% 119.12/119.52 inference(scs_inference,[],[197,166,73,55,74,54,91])).
% 119.12/119.52 cnf(319,plain,
% 119.12/119.52 (P5(f10(a16,a1,a16),f18(f18(a15,x3191),x3192))),
% 119.12/119.52 inference(scs_inference,[],[197,166,73,55,74,54,91,92])).
% 119.12/119.52 cnf(332,plain,
% 119.12/119.52 (P5(f10(a1,a1,a15),f18(x3321,a15))),
% 119.12/119.52 inference(scs_inference,[],[209,91])).
% 119.12/119.52 cnf(334,plain,
% 119.12/119.52 (P5(f10(a1,a1,a15),f18(a15,x3341))),
% 119.12/119.52 inference(scs_inference,[],[209,91,92])).
% 119.12/119.52 cnf(336,plain,
% 119.12/119.52 (~E(a17,f10(a16,a1,a16))),
% 119.12/119.52 inference(scs_inference,[],[47,309,209,91,92,37])).
% 119.12/119.52 cnf(339,plain,
% 119.12/119.52 (~E(f18(a16,x3391),a1)),
% 119.12/119.52 inference(scs_inference,[],[47,309,117,243,209,91,92,37,41,5])).
% 119.12/119.52 cnf(358,plain,
% 119.12/119.52 (P5(f10(a1,a1,a15),f18(f18(x3581,a15),x3582))),
% 119.12/119.52 inference(scs_inference,[],[332,92])).
% 119.12/119.52 cnf(360,plain,
% 119.12/119.52 (P5(f10(a1,a1,a15),f18(x3601,f18(x3602,a15)))),
% 119.12/119.52 inference(scs_inference,[],[332,92,91])).
% 119.12/119.52 cnf(367,plain,
% 119.12/119.52 (P5(x3671,a15)+~E(f10(a16,a1,a1),x3671)),
% 119.12/119.52 inference(scs_inference,[],[203,114,117,106,251,332,92,91,41,52,58,40])).
% 119.12/119.52 cnf(372,plain,
% 119.12/119.52 (P5(f10(a1,a1,a15),f18(x3721,f18(a15,x3722)))),
% 119.12/119.52 inference(scs_inference,[],[334,91])).
% 119.12/119.52 cnf(374,plain,
% 119.12/119.52 (P5(f10(a1,a1,a15),f18(f18(a15,x3741),x3742))),
% 119.12/119.52 inference(scs_inference,[],[334,91,92])).
% 119.12/119.52 cnf(382,plain,
% 119.12/119.52 (P5(x3821,a15)+~E(f10(a16,a1,a16),x3821)),
% 119.12/119.52 inference(scs_inference,[],[179,336,117,104,270,334,91,92,41,6,52,58,40])).
% 119.12/119.52 cnf(387,plain,
% 119.12/119.52 (P5(f10(a16,a1,a16),f18(a1,x3871))),
% 119.12/119.52 inference(scs_inference,[],[174,92])).
% 119.12/119.52 cnf(389,plain,
% 119.12/119.52 (P5(f10(a16,a1,a16),f18(x3891,a1))),
% 119.12/119.52 inference(scs_inference,[],[174,92,91])).
% 119.12/119.52 cnf(401,plain,
% 119.12/119.52 (P5(f10(a16,a1,a16),f18(x4011,f18(a1,x4012)))),
% 119.12/119.52 inference(scs_inference,[],[387,91])).
% 119.12/119.52 cnf(403,plain,
% 119.12/119.52 (P5(f10(a16,a1,a16),f18(f18(a1,x4031),x4032))),
% 119.12/119.52 inference(scs_inference,[],[387,91,92])).
% 119.12/119.52 cnf(417,plain,
% 119.12/119.52 (P5(f10(a16,a1,a16),f18(f18(x4171,a1),x4172))),
% 119.12/119.52 inference(scs_inference,[],[389,92])).
% 119.12/119.52 cnf(419,plain,
% 119.12/119.52 (P5(f10(a16,a1,a16),f18(x4191,f18(x4192,a1)))),
% 119.12/119.52 inference(scs_inference,[],[389,92,91])).
% 119.12/119.52 cnf(458,plain,
% 119.12/119.52 (~P4(x4581,x4582)+P4(f13(x4582),x4582)),
% 119.12/119.52 inference(scs_inference,[],[50,51])).
% 119.12/119.52 cnf(528,plain,
% 119.12/119.52 (P5(x5281,f18(x5282,a15))+~E(f10(a16,a1,a16),x5281)),
% 119.12/119.52 inference(scs_inference,[],[228,387,193,401,119,41,6,52,58,40])).
% 119.12/119.52 cnf(538,plain,
% 119.12/119.52 (P5(x5381,f18(a15,x5382))+~E(f10(a16,a1,a16),x5381)),
% 119.12/119.52 inference(scs_inference,[],[228,389,197,403,168,41,52,58,40])).
% 119.12/119.52 cnf(549,plain,
% 119.12/119.52 (P5(x5491,f18(x5492,a15))+~E(f10(a16,a1,a1),x5491)),
% 119.12/119.52 inference(scs_inference,[],[228,270,136,417,230,41,5,52,58,40])).
% 119.12/119.52 cnf(559,plain,
% 119.12/119.52 (P5(x5591,f18(a15,x5592))+~E(f10(a1,a1,a15),x5591)),
% 119.12/119.52 inference(scs_inference,[],[228,332,334,419,205,41,52,58,40])).
% 119.12/119.52 cnf(570,plain,
% 119.12/119.52 (P5(x5701,f18(a15,x5702))+~E(f10(a16,a1,a1),x5701)),
% 119.12/119.52 inference(scs_inference,[],[228,193,138,298,339,41,6,52,58,40])).
% 119.12/119.52 cnf(637,plain,
% 119.12/119.52 (~P4(x6371,x6372)+P4(f3(x6372),x6372)),
% 119.12/119.52 inference(scs_inference,[],[53,49])).
% 119.12/119.52 cnf(739,plain,
% 119.12/119.52 (P5(x7391,a15)+~E(f10(a1,a1,a15),x7391)),
% 119.12/119.52 inference(scs_inference,[],[372,257,209,52,58,40])).
% 119.12/119.52 cnf(921,plain,
% 119.12/119.52 (~E(a1,a15)),
% 119.12/119.52 inference(scs_inference,[],[233,2,6])).
% 119.12/119.52 cnf(922,plain,
% 119.12/119.52 (P7(a1)),
% 119.12/119.52 inference(scs_inference,[],[44,921,52])).
% 119.12/119.52 cnf(955,plain,
% 119.12/119.52 (P5(f13(x9551),x9551)+~P4(x9552,x9551)),
% 119.12/119.52 inference(scs_inference,[],[458,54])).
% 119.12/119.52 cnf(971,plain,
% 119.12/119.52 (~P4(x9711,x9712)+~P2(f3(x9712),x9712)),
% 119.12/119.52 inference(scs_inference,[],[637,56])).
% 119.12/119.52 cnf(1099,plain,
% 119.12/119.52 (~P4(x10991,x10992)+P5(f13(x10992),f18(x10992,x10993))),
% 119.12/119.52 inference(scs_inference,[],[955,92])).
% 119.12/119.52 cnf(1115,plain,
% 119.12/119.52 (~P4(x11151,x11152)+~E(f2(x11152),f3(x11152))),
% 119.12/119.52 inference(scs_inference,[],[46,971,35])).
% 119.12/119.52 cnf(1163,plain,
% 119.12/119.52 (E(f2(f18(f14(f2(x11631),x11631),f6(f2(x11631),x11631))),f2(x11631))),
% 119.12/119.52 inference(scs_inference,[],[46,4,72])).
% 119.12/119.52 cnf(1242,plain,
% 119.12/119.52 (P4(f4(f13(a1),a1),a1)),
% 119.12/119.52 inference(scs_inference,[],[922,63,51])).
% 119.12/119.52 cnf(1243,plain,
% 119.12/119.52 (P5(f13(a1),f18(a1,x12431))),
% 119.12/119.52 inference(scs_inference,[],[1242,1099])).
% 119.12/119.52 cnf(1245,plain,
% 119.12/119.52 (~P2(f4(f13(a1),a1),a1)),
% 119.12/119.52 inference(scs_inference,[],[1242,1099,56])).
% 119.12/119.52 cnf(1247,plain,
% 119.12/119.52 (P5(f13(a1),f18(x12471,f18(a1,x12472)))),
% 119.12/119.52 inference(scs_inference,[],[1242,1099,56,91])).
% 119.12/119.52 cnf(1249,plain,
% 119.12/119.52 (P5(f13(a1),f18(f18(a1,x12491),x12492))),
% 119.12/119.52 inference(scs_inference,[],[1242,1099,56,91,92])).
% 119.12/119.52 cnf(1733,plain,
% 119.12/119.52 (~E(f4(f13(a1),a1),f10(a1,a1,a15))),
% 119.12/119.52 inference(scs_inference,[],[160,1242,33])).
% 119.12/119.52 cnf(2605,plain,
% 119.12/119.52 (P4(f3(a1),a1)),
% 119.12/119.52 inference(scs_inference,[],[1242,53,49])).
% 119.12/119.52 cnf(2607,plain,
% 119.12/119.52 (P4(f13(a1),a1)),
% 119.12/119.52 inference(scs_inference,[],[922,1242,53,49,51])).
% 119.12/119.52 cnf(2609,plain,
% 119.12/119.52 (P5(f13(a1),a1)),
% 119.12/119.52 inference(scs_inference,[],[922,1242,53,49,51,955])).
% 119.12/119.52 cnf(2611,plain,
% 119.12/119.52 (~P2(f3(a1),a1)),
% 119.12/119.52 inference(scs_inference,[],[922,1242,53,49,51,955,971])).
% 119.12/119.52 cnf(2613,plain,
% 119.12/119.52 (~E(f4(f3(a1),a1),f3(a1))),
% 119.12/119.52 inference(scs_inference,[],[922,1242,53,49,51,955,971,57])).
% 119.12/119.52 cnf(2615,plain,
% 119.12/119.52 (P5(f5(f18(a1,a16),a15),f18(a1,a16))),
% 119.12/119.52 inference(scs_inference,[],[922,48,1242,53,49,51,955,971,57,59])).
% 119.12/119.52 cnf(2617,plain,
% 119.12/119.52 (P4(f4(f3(a1),a1),a1)),
% 119.12/119.52 inference(scs_inference,[],[922,48,1242,53,49,51,955,971,57,59,63])).
% 119.12/119.52 cnf(2619,plain,
% 119.12/119.52 (~P5(f5(f18(a1,a16),a15),a15)),
% 119.12/119.52 inference(scs_inference,[],[922,48,1242,53,49,51,955,971,57,59,63,70])).
% 119.12/119.52 cnf(2623,plain,
% 119.12/119.52 (E(f9(a16,a1),f18(a1,a16))),
% 119.12/119.52 inference(scs_inference,[],[922,47,48,1242,53,49,51,955,971,57,59,63,70,1115,75])).
% 119.12/119.52 cnf(2625,plain,
% 119.12/119.52 (P6(f2(x26251),f14(f2(x26251),x26251),f6(f2(x26251),x26251))),
% 119.12/119.52 inference(scs_inference,[],[922,46,47,48,1242,53,49,51,955,971,57,59,63,70,1115,75,77])).
% 119.12/119.52 cnf(2632,plain,
% 119.12/119.52 (~P4(f2(x26321),x26321)),
% 119.12/119.52 inference(scs_inference,[],[922,46,47,48,1242,53,49,51,955,971,57,59,63,70,1115,75,77,13,14,15,16,17,56])).
% 119.12/119.52 cnf(2634,plain,
% 119.12/119.52 (P5(f2(x26341),x26341)),
% 119.12/119.52 inference(scs_inference,[],[922,46,47,48,1242,53,49,51,955,971,57,59,63,70,1115,75,77,13,14,15,16,17,56,55])).
% 119.12/119.52 cnf(2638,plain,
% 119.12/119.52 (P5(a17,a1)),
% 119.12/119.52 inference(scs_inference,[],[1733,922,46,47,48,1242,53,49,51,955,971,57,59,63,70,1115,75,77,13,14,15,16,17,56,55,18,2,74])).
% 119.12/119.52 cnf(2640,plain,
% 119.12/119.52 (P5(f4(f13(a1),a1),a1)),
% 119.12/119.52 inference(scs_inference,[],[1733,922,46,47,48,1242,53,49,51,955,971,57,59,63,70,1115,75,77,13,14,15,16,17,56,55,18,2,74,54])).
% 119.12/119.52 cnf(2642,plain,
% 119.12/119.52 (P5(a17,a16)),
% 119.12/119.52 inference(scs_inference,[],[1733,922,46,47,48,1242,53,49,51,955,971,57,59,63,70,1115,75,77,13,14,15,16,17,56,55,18,2,74,54,73])).
% 119.12/119.52 cnf(2645,plain,
% 119.12/119.52 (E(f18(f9(a16,a1),x26451),f18(f18(a1,a16),x26451))),
% 119.12/119.52 inference(scs_inference,[],[1733,922,46,47,48,1242,53,49,51,955,971,57,59,63,70,1115,75,77,13,14,15,16,17,56,55,18,2,74,54,73,6,5])).
% 119.12/119.52 cnf(2646,plain,
% 119.12/119.52 (E(f12(f9(a16,a1),f9(a16,a1),x26461),f12(f18(a1,a16),f18(a1,a16),x26461))),
% 119.12/119.52 inference(scs_inference,[],[1733,922,46,47,48,1242,53,49,51,955,971,57,59,63,70,1115,75,77,13,14,15,16,17,56,55,18,2,74,54,73,6,5,3])).
% 119.12/119.52 cnf(2650,plain,
% 119.12/119.52 (~E(f18(f18(a1,a1),f18(a1,a1)),f18(a15,x26501))),
% 119.12/119.52 inference(scs_inference,[],[1733,922,201,1243,209,46,47,48,1242,53,49,51,955,971,57,59,63,70,1115,75,77,13,14,15,16,17,56,55,18,2,74,54,73,6,5,3,61,62])).
% 119.12/119.52 cnf(2652,plain,
% 119.12/119.52 (P5(f2(x26521),f7(x26521,f2(x26521)))),
% 119.12/119.52 inference(scs_inference,[],[1733,922,201,1243,209,46,47,48,1242,53,49,51,955,971,57,59,63,70,1115,75,77,13,14,15,16,17,56,55,18,2,74,54,73,6,5,3,61,62,66])).
% 119.12/119.52 cnf(2654,plain,
% 119.12/119.52 (P5(f2(x26541),f11(x26541,f2(x26541)))),
% 119.12/119.52 inference(scs_inference,[],[1733,922,201,1243,209,46,47,48,1242,53,49,51,955,971,57,59,63,70,1115,75,77,13,14,15,16,17,56,55,18,2,74,54,73,6,5,3,61,62,66,67])).
% 119.12/119.52 cnf(2656,plain,
% 119.12/119.52 (P1(f7(x26561,f2(x26561)),x26561)),
% 119.12/119.52 inference(scs_inference,[],[1733,922,201,1243,209,46,47,48,1242,53,49,51,955,971,57,59,63,70,1115,75,77,13,14,15,16,17,56,55,18,2,74,54,73,6,5,3,61,62,66,67,68])).
% 119.12/119.52 cnf(2658,plain,
% 119.12/119.52 (P1(f11(x26581,f2(x26581)),x26581)),
% 119.12/119.52 inference(scs_inference,[],[1733,922,201,1243,209,46,47,48,1242,53,49,51,955,971,57,59,63,70,1115,75,77,13,14,15,16,17,56,55,18,2,74,54,73,6,5,3,61,62,66,67,68,69])).
% 119.12/119.52 cnf(2660,plain,
% 119.12/119.52 (~P1(f7(x26601,f2(x26601)),f11(x26601,f2(x26601)))),
% 119.12/119.52 inference(scs_inference,[],[1733,922,201,1243,209,46,47,48,1242,53,49,51,955,971,57,59,63,70,1115,75,77,13,14,15,16,17,56,55,18,2,74,54,73,6,5,3,61,62,66,67,68,69,78])).
% 119.12/119.52 cnf(2662,plain,
% 119.12/119.52 (~P1(f11(x26621,f2(x26621)),f7(x26621,f2(x26621)))),
% 119.12/119.52 inference(scs_inference,[],[1733,922,201,1243,209,46,47,48,1242,53,49,51,955,971,57,59,63,70,1115,75,77,13,14,15,16,17,56,55,18,2,74,54,73,6,5,3,61,62,66,67,68,69,78,79])).
% 119.12/119.52 cnf(2664,plain,
% 119.12/119.52 (~E(x26641,f11(x26641,f2(x26641)))),
% 119.12/119.52 inference(scs_inference,[],[1733,922,201,1243,209,46,47,48,1242,53,49,51,955,971,57,59,63,70,1115,75,77,13,14,15,16,17,56,55,18,2,74,54,73,6,5,3,61,62,66,67,68,69,78,79,32])).
% 119.12/119.52 cnf(2668,plain,
% 119.12/119.52 (~P5(f5(f18(a1,a16),a15),f18(a15,a15))),
% 119.12/119.52 inference(scs_inference,[],[1733,922,401,360,201,1243,209,255,46,47,48,1242,53,49,51,955,971,57,59,63,70,1115,75,77,13,14,15,16,17,56,55,18,2,74,54,73,6,5,3,61,62,66,67,68,69,78,79,32,41,60,93])).
% 119.12/119.52 cnf(2670,plain,
% 119.12/119.52 (~P1(f9(a16,a1),a15)),
% 119.12/119.52 inference(scs_inference,[],[1733,922,401,360,201,1243,209,255,46,47,48,1242,53,49,51,955,971,57,59,63,70,1115,75,77,13,14,15,16,17,56,55,18,2,74,54,73,6,5,3,61,62,66,67,68,69,78,79,32,41,60,93,31])).
% 119.12/119.52 cnf(2671,plain,
% 119.12/119.52 (~E(f18(a1,a16),f18(a15,a15))),
% 119.12/119.52 inference(scs_inference,[],[1733,922,401,360,201,1243,209,255,46,47,48,1242,53,49,51,955,971,57,59,63,70,1115,75,77,13,14,15,16,17,56,55,18,2,74,54,73,6,5,3,61,62,66,67,68,69,78,79,32,41,60,93,31,65])).
% 119.12/119.52 cnf(2673,plain,
% 119.12/119.52 (~P6(x26731,x26732,x26732)),
% 119.12/119.52 inference(scs_inference,[],[1733,922,401,360,201,1243,209,255,46,47,48,1242,53,49,51,955,971,57,59,63,70,1115,75,77,13,14,15,16,17,56,55,18,2,74,54,73,6,5,3,61,62,66,67,68,69,78,79,32,41,60,93,31,65,82])).
% 119.12/119.52 cnf(2675,plain,
% 119.12/119.52 (E(f2(f9(a16,a1)),f2(f18(a1,a16)))),
% 119.12/119.52 inference(scs_inference,[],[1733,922,401,360,201,1243,209,255,46,47,48,1242,53,49,51,955,971,57,59,63,70,1115,75,77,13,14,15,16,17,56,55,18,2,74,54,73,6,5,3,61,62,66,67,68,69,78,79,32,41,60,93,31,65,82,4])).
% 119.12/119.52 cnf(2683,plain,
% 119.12/119.52 (E(f11(f9(a16,a1),x26831),f11(f18(a1,a16),x26831))),
% 119.12/119.52 inference(scs_inference,[],[1733,922,401,360,201,1243,209,255,46,47,48,1242,53,49,51,955,971,57,59,63,70,1115,75,77,13,14,15,16,17,56,55,18,2,74,54,73,6,5,3,61,62,66,67,68,69,78,79,32,41,60,93,31,65,82,4,8,9,10,11,12,19,20,21])).
% 119.12/119.52 cnf(2696,plain,
% 119.12/119.52 (P2(f2(f9(a16,a1)),f18(a1,a16))),
% 119.12/119.52 inference(scs_inference,[],[1733,921,922,401,360,201,1243,209,255,46,47,48,1242,53,49,51,955,971,57,59,63,70,1115,75,77,13,14,15,16,17,56,55,18,2,74,54,73,6,5,3,61,62,66,67,68,69,78,79,32,41,60,93,31,65,82,4,8,9,10,11,12,19,20,21,22,23,24,25,26,27,28,29,30,76,40,36])).
% 119.12/119.52 cnf(2697,plain,
% 119.12/119.52 (P2(f2(x26971),x26971)),
% 119.12/119.52 inference(rename_variables,[],[46])).
% 119.12/119.52 cnf(2698,plain,
% 119.12/119.52 (P2(f2(f18(a1,a16)),f9(a16,a1))),
% 119.12/119.52 inference(scs_inference,[],[1733,921,922,401,360,201,1243,209,255,46,2697,47,48,1242,53,49,51,955,971,57,59,63,70,1115,75,77,13,14,15,16,17,56,55,18,2,74,54,73,6,5,3,61,62,66,67,68,69,78,79,32,41,60,93,31,65,82,4,8,9,10,11,12,19,20,21,22,23,24,25,26,27,28,29,30,76,40,36,35])).
% 119.12/119.52 cnf(2700,plain,
% 119.12/119.52 (P4(a17,a16)),
% 119.12/119.52 inference(scs_inference,[],[1733,921,922,401,360,201,1243,209,255,46,2697,47,48,1242,53,49,51,955,971,57,59,63,70,1115,75,77,13,14,15,16,17,56,55,18,2,74,54,73,6,5,3,61,62,66,67,68,69,78,79,32,41,60,93,31,65,82,4,8,9,10,11,12,19,20,21,22,23,24,25,26,27,28,29,30,76,40,36,35,81])).
% 119.12/119.52 cnf(2702,plain,
% 119.12/119.52 (P4(f13(a16),a16)),
% 119.12/119.52 inference(scs_inference,[],[1733,921,922,401,360,201,1243,209,255,46,2697,47,48,1242,53,49,51,955,971,57,59,63,70,1115,75,77,13,14,15,16,17,56,55,18,2,74,54,73,6,5,3,61,62,66,67,68,69,78,79,32,41,60,93,31,65,82,4,8,9,10,11,12,19,20,21,22,23,24,25,26,27,28,29,30,76,40,36,35,81,458])).
% 119.12/119.52 cnf(2704,plain,
% 119.12/119.52 (P4(f3(a16),a16)),
% 119.12/119.52 inference(scs_inference,[],[1733,921,922,401,360,201,1243,209,255,46,2697,47,48,1242,53,49,51,955,971,57,59,63,70,1115,75,77,13,14,15,16,17,56,55,18,2,74,54,73,6,5,3,61,62,66,67,68,69,78,79,32,41,60,93,31,65,82,4,8,9,10,11,12,19,20,21,22,23,24,25,26,27,28,29,30,76,40,36,35,81,458,637])).
% 119.12/119.52 cnf(2712,plain,
% 119.12/119.52 (~P2(f3(a16),a16)),
% 119.12/119.52 inference(scs_inference,[],[2700,971])).
% 119.12/119.52 cnf(2714,plain,
% 119.12/119.52 (P5(f5(f9(a16,a1),a15),f9(a16,a1))),
% 119.12/119.52 inference(scs_inference,[],[2700,2670,971,59])).
% 119.12/119.52 cnf(2716,plain,
% 119.12/119.52 (P4(f4(a17,a16),a16)),
% 119.12/119.52 inference(scs_inference,[],[2700,2670,971,59,63])).
% 119.12/119.52 cnf(2718,plain,
% 119.12/119.52 (~E(f2(a16),f3(a16))),
% 119.12/119.52 inference(scs_inference,[],[2700,2670,971,59,63,1115])).
% 119.12/119.52 cnf(2720,plain,
% 119.12/119.52 (~P3(a16)),
% 119.12/119.52 inference(scs_inference,[],[2700,2670,971,59,63,1115,53])).
% 119.12/119.52 cnf(2722,plain,
% 119.12/119.52 (~P5(f5(f9(a16,a1),a15),a15)),
% 119.12/119.52 inference(scs_inference,[],[2700,2670,971,59,63,1115,53,70])).
% 119.12/119.52 cnf(2726,plain,
% 119.12/119.52 (P5(f13(a16),a16)),
% 119.12/119.52 inference(scs_inference,[],[2700,2670,2698,971,59,63,1115,53,70,56,955])).
% 119.12/119.52 cnf(2728,plain,
% 119.12/119.52 (~E(f4(a17,a16),a17)),
% 119.12/119.52 inference(scs_inference,[],[2700,2670,2698,971,59,63,1115,53,70,56,955,57])).
% 119.12/119.52 cnf(2732,plain,
% 119.12/119.52 (~E(f18(a15,a15),f18(a1,a16))),
% 119.12/119.52 inference(scs_inference,[],[2700,2671,2670,2698,2696,971,59,63,1115,53,70,56,955,57,55,2])).
% 119.12/119.52 cnf(2733,plain,
% 119.12/119.52 (P5(f3(a1),a1)),
% 119.12/119.52 inference(scs_inference,[],[2700,2671,2605,2670,2698,2696,971,59,63,1115,53,70,56,955,57,55,2,54])).
% 119.12/119.52 cnf(2735,plain,
% 119.12/119.52 (~E(f18(a15,a15),f18(x27351,f18(a1,a16)))),
% 119.12/119.52 inference(scs_inference,[],[2700,2671,2605,2670,2698,2696,2668,2615,971,59,63,1115,53,70,56,955,57,55,2,54,61])).
% 119.12/119.52 cnf(2737,plain,
% 119.12/119.52 (~P6(x27371,f9(a16,a1),f18(a1,a16))),
% 119.12/119.52 inference(scs_inference,[],[2673,2700,2671,2605,2623,2670,2698,2696,2668,2615,971,59,63,1115,53,70,56,955,57,55,2,54,61,38])).
% 119.12/119.52 cnf(2738,plain,
% 119.12/119.52 (~P6(x27381,x27382,x27382)),
% 119.12/119.52 inference(rename_variables,[],[2673])).
% 119.12/119.52 cnf(2739,plain,
% 119.12/119.52 (~E(f18(a15,a15),f18(f18(a1,a16),x27391))),
% 119.12/119.52 inference(scs_inference,[],[2673,2700,2671,2605,2623,2670,2698,2696,2668,2615,971,59,63,1115,53,70,56,955,57,55,2,54,61,38,62])).
% 119.12/119.52 cnf(2741,plain,
% 119.12/119.52 (~P6(x27411,f18(a1,a16),f9(a16,a1))),
% 119.12/119.52 inference(scs_inference,[],[2673,2738,2700,2671,2605,2623,2670,2698,2696,2668,2615,971,59,63,1115,53,70,56,955,57,55,2,54,61,38,62,39])).
% 119.12/119.52 cnf(2742,plain,
% 119.12/119.52 (~P6(x27421,x27422,x27422)),
% 119.12/119.52 inference(rename_variables,[],[2673])).
% 119.12/119.52 cnf(2743,plain,
% 119.12/119.52 (~E(a16,f9(a16,a1))),
% 119.12/119.52 inference(scs_inference,[],[2673,2738,2700,2671,2605,2623,2670,2698,2696,2668,2615,147,971,59,63,1115,53,70,56,955,57,55,2,54,61,38,62,39,3])).
% 119.12/119.52 cnf(2744,plain,
% 119.12/119.52 (~E(f2(a15),f5(f18(a1,a16),a15))),
% 119.12/119.52 inference(scs_inference,[],[2673,2738,2700,2634,2671,2605,2623,2670,2698,2696,2668,2615,2619,147,971,59,63,1115,53,70,56,955,57,55,2,54,61,38,62,39,3,40])).
% 119.12/119.52 cnf(2746,plain,
% 119.12/119.52 (~P1(f18(a1,a16),f18(a15,a15))),
% 119.12/119.52 inference(scs_inference,[],[2673,2738,2700,2634,2671,2605,2623,2670,2698,2696,2668,2615,2619,147,971,59,63,1115,53,70,56,955,57,55,2,54,61,38,62,39,3,40,60])).
% 119.12/119.52 cnf(2748,plain,
% 119.12/119.52 (~E(f2(a16),f10(a16,a1,a16))),
% 119.12/119.52 inference(scs_inference,[],[2673,2738,2700,2634,2671,2605,2623,2670,2698,2696,2668,2615,2619,311,147,46,971,59,63,1115,53,70,56,955,57,55,2,54,61,38,62,39,3,40,60,35])).
% 119.12/119.52 cnf(2750,plain,
% 119.12/119.52 (P5(f12(a1,a1,a17),a1)),
% 119.12/119.52 inference(scs_inference,[],[2673,2738,2742,2638,2700,2634,2671,2605,2623,2670,2698,2696,2668,2615,2619,311,147,46,971,59,63,1115,53,70,56,955,57,55,2,54,61,38,62,39,3,40,60,35,84])).
% 119.12/119.52 cnf(2751,plain,
% 119.12/119.52 (~P6(x27511,x27512,x27512)),
% 119.12/119.52 inference(rename_variables,[],[2673])).
% 119.12/119.52 cnf(2753,plain,
% 119.12/119.52 (P5(f12(a16,a16,a17),a16)),
% 119.12/119.52 inference(scs_inference,[],[2673,2738,2742,2751,2638,2642,2700,2634,2671,2605,2623,2670,2698,2696,2668,2615,2619,311,147,46,971,59,63,1115,53,70,56,955,57,55,2,54,61,38,62,39,3,40,60,35,84,85])).
% 119.12/119.52 cnf(2754,plain,
% 119.12/119.52 (~P6(x27541,x27542,x27542)),
% 119.12/119.52 inference(rename_variables,[],[2673])).
% 119.12/119.52 cnf(2756,plain,
% 119.12/119.52 (~E(f18(a1,a16),f18(f18(a15,a15),f18(a15,a15)))),
% 119.12/119.52 inference(scs_inference,[],[2673,2738,2742,2751,2638,2642,2700,2634,2671,2605,2623,2670,2698,2696,2668,2615,2619,311,147,46,971,59,63,1115,53,70,56,955,57,55,2,54,61,38,62,39,3,40,60,35,84,85,65])).
% 119.12/119.52 cnf(2758,plain,
% 119.12/119.52 (P4(a17,a1)),
% 119.12/119.52 inference(scs_inference,[],[2673,2738,2742,2751,2638,2642,2700,2634,2671,2605,2623,2670,2698,2696,2668,2615,2619,311,147,46,47,971,59,63,1115,53,70,56,955,57,55,2,54,61,38,62,39,3,40,60,35,84,85,65,82])).
% 119.12/119.52 cnf(2760,plain,
% 119.12/119.52 (~P4(f12(a1,a1,a17),a1)),
% 119.12/119.52 inference(scs_inference,[],[2673,2738,2742,2751,2754,2638,2642,2700,2634,2671,2605,2623,2670,2698,2696,2668,2615,2619,311,147,46,47,971,59,63,1115,53,70,56,955,57,55,2,54,61,38,62,39,3,40,60,35,84,85,65,82,90])).
% 119.12/119.52 cnf(2765,plain,
% 119.12/119.52 (P5(f12(a1,a1,a17),f11(a1,f12(a1,a1,a17)))),
% 119.12/119.52 inference(scs_inference,[],[2673,2738,2742,2751,2754,2638,2642,2700,2634,2671,2605,2623,2670,2698,2696,2668,2615,2619,311,147,389,46,47,971,59,63,1115,53,70,56,955,57,55,2,54,61,38,62,39,3,40,60,35,84,85,65,82,90,69,67])).
% 119.12/119.52 cnf(2767,plain,
% 119.12/119.52 (P5(f12(a1,a1,a17),f7(a1,f12(a1,a1,a17)))),
% 119.12/119.52 inference(scs_inference,[],[2673,2738,2742,2751,2754,2638,2642,2700,2634,2671,2605,2623,2670,2698,2696,2668,2615,2619,311,147,389,46,47,971,59,63,1115,53,70,56,955,57,55,2,54,61,38,62,39,3,40,60,35,84,85,65,82,90,69,67,66])).
% 119.12/119.52 cnf(2769,plain,
% 119.12/119.52 (P1(f7(a1,f12(a1,a1,a17)),a1)),
% 119.12/119.52 inference(scs_inference,[],[2673,2738,2742,2751,2754,2638,2642,2700,2634,2671,2605,2623,2670,2698,2696,2668,2615,2619,311,147,389,46,47,971,59,63,1115,53,70,56,955,57,55,2,54,61,38,62,39,3,40,60,35,84,85,65,82,90,69,67,66,68])).
% 119.12/119.52 cnf(2771,plain,
% 119.12/119.52 (~E(a17,f2(a16))),
% 119.12/119.52 inference(scs_inference,[],[2673,2738,2742,2751,2754,2638,2642,2700,2632,2634,2671,2605,2623,2670,2698,2696,2668,2615,2619,311,147,389,46,47,971,59,63,1115,53,70,56,955,57,55,2,54,61,38,62,39,3,40,60,35,84,85,65,82,90,69,67,66,68,33])).
% 119.12/119.52 cnf(2780,plain,
% 119.12/119.52 (~P4(f2(f9(a16,a1)),f18(a1,a16))),
% 119.12/119.52 inference(scs_inference,[],[2696,56])).
% 119.12/119.52 cnf(2782,plain,
% 119.12/119.52 (P4(f4(a17,a1),a1)),
% 119.12/119.52 inference(scs_inference,[],[2758,2696,56,63])).
% 119.12/119.52 cnf(2784,plain,
% 119.12/119.52 (P5(f5(f18(a1,a16),f18(a15,a15)),f18(a1,a16))),
% 119.12/119.52 inference(scs_inference,[],[2758,2746,2696,56,63,59])).
% 119.12/119.52 cnf(2786,plain,
% 119.12/119.52 (~E(f4(a17,a1),a17)),
% 119.12/119.52 inference(scs_inference,[],[2758,2746,2696,56,63,59,57])).
% 119.12/119.52 cnf(2788,plain,
% 119.12/119.52 (~P5(f5(f18(a1,a16),f18(a15,a15)),f18(a15,a15))),
% 119.12/119.52 inference(scs_inference,[],[2758,2746,2696,56,63,59,57,70])).
% 119.12/119.52 cnf(2790,plain,
% 119.12/119.52 (~P5(f5(f18(a1,a16),f18(a15,a15)),a15)),
% 119.12/119.52 inference(scs_inference,[],[2758,2746,2696,56,63,59,57,70,91])).
% 119.12/119.52 cnf(2793,plain,
% 119.12/119.52 (P5(f4(a17,a16),a16)),
% 119.12/119.52 inference(scs_inference,[],[2758,2746,2748,2716,2696,56,63,59,57,70,91,2,54])).
% 119.12/119.52 cnf(2795,plain,
% 119.12/119.52 (P5(f13(a16),f9(a16,a1))),
% 119.12/119.52 inference(scs_inference,[],[2758,2746,2748,2716,2726,2696,2623,56,63,59,57,70,91,2,54,61])).
% 119.12/119.52 cnf(2797,plain,
% 119.12/119.52 (P1(f11(a1,f12(a1,a1,a17)),a1)),
% 119.12/119.52 inference(scs_inference,[],[2758,2746,2748,2750,2760,2716,2726,2696,2623,56,63,59,57,70,91,2,54,61,69])).
% 119.12/119.52 cnf(2799,plain,
% 119.12/119.52 (P5(f12(a1,a1,a17),f9(a16,a1))),
% 119.12/119.52 inference(scs_inference,[],[2758,2746,2748,2750,2760,2716,2726,2696,2623,56,63,59,57,70,91,2,54,61,69,62])).
% 119.12/119.52 cnf(2801,plain,
% 119.12/119.52 (P5(f5(f9(a16,a1),a15),f18(a1,a16))),
% 119.12/119.52 inference(scs_inference,[],[2758,2746,2748,2750,2760,2716,2726,2714,2696,2623,56,63,59,57,70,91,2,54,61,69,62,41])).
% 119.12/119.52 cnf(2802,plain,
% 119.12/119.52 (P2(f12(a1,a1,a17),a1)),
% 119.12/119.52 inference(scs_inference,[],[2758,2746,2748,2750,2760,2716,2726,2714,2696,2623,56,63,59,57,70,91,2,54,61,69,62,41,58])).
% 119.12/119.52 cnf(2804,plain,
% 119.12/119.52 (P5(f12(a1,a1,a17),a15)),
% 119.12/119.52 inference(scs_inference,[],[44,2758,2746,2748,2750,2760,2716,2726,2714,2696,2623,56,63,59,57,70,91,2,54,61,69,62,41,58,60])).
% 119.12/119.52 cnf(2806,plain,
% 119.12/119.52 (~P1(f9(a16,a1),f18(a15,a15))),
% 119.12/119.52 inference(scs_inference,[],[44,2758,2746,2748,2750,2760,2716,2726,2714,2696,2623,56,63,59,57,70,91,2,54,61,69,62,41,58,60,31])).
% 119.12/119.52 cnf(2807,plain,
% 119.12/119.52 (P5(f12(a1,a1,f12(a1,a1,a17)),a1)),
% 119.12/119.52 inference(scs_inference,[],[44,2758,2746,2748,2750,2760,2716,2726,2714,2673,2696,2623,56,63,59,57,70,91,2,54,61,69,62,41,58,60,31,84])).
% 119.12/119.52 cnf(2808,plain,
% 119.12/119.52 (~P6(x28081,x28082,x28082)),
% 119.12/119.52 inference(rename_variables,[],[2673])).
% 119.12/119.52 cnf(2818,plain,
% 119.12/119.52 (P5(f12(a16,a16,f13(a16)),a16)),
% 119.12/119.52 inference(scs_inference,[],[44,2758,2720,2732,2746,2748,2750,2760,2716,2726,2714,2722,1245,2673,2808,2634,2696,2623,46,56,63,59,57,70,91,2,54,61,69,62,41,58,60,31,84,65,42,40,3,35,85])).
% 119.12/119.52 cnf(2826,plain,
% 119.12/119.52 (~P5(f5(f9(a16,a1),f18(a15,a15)),f18(a15,a15))),
% 119.12/119.52 inference(scs_inference,[],[2806,70])).
% 119.12/119.52 cnf(2828,plain,
% 119.12/119.52 (~E(f4(f4(a17,a1),a1),f4(a17,a1))),
% 119.12/119.52 inference(scs_inference,[],[2806,2782,70,57])).
% 119.12/119.52 cnf(2830,plain,
% 119.12/119.52 (P5(f5(f9(a16,a1),f18(a15,a15)),f9(a16,a1))),
% 119.12/119.52 inference(scs_inference,[],[2806,2782,70,57,59])).
% 119.12/119.52 cnf(2832,plain,
% 119.12/119.52 (P4(f4(f4(a17,a1),a1),a1)),
% 119.12/119.52 inference(scs_inference,[],[2806,2782,70,57,59,63])).
% 119.12/119.52 cnf(2834,plain,
% 119.12/119.52 (~P5(f5(f9(a16,a1),f18(a15,a15)),a15)),
% 119.12/119.52 inference(scs_inference,[],[2806,2782,70,57,59,63,92])).
% 119.12/119.52 cnf(2837,plain,
% 119.12/119.52 (P5(f4(a17,a1),a1)),
% 119.12/119.52 inference(scs_inference,[],[2806,2718,2782,70,57,59,63,92,2,54])).
% 119.12/119.52 cnf(2841,plain,
% 119.12/119.52 (~E(a15,f18(f18(a1,a16),x28411))),
% 119.12/119.53 inference(scs_inference,[],[2806,2718,2782,2784,2790,70,57,59,63,92,2,54,61,62])).
% 119.12/119.53 cnf(2843,plain,
% 119.12/119.53 (~E(f18(a1,a16),a15)),
% 119.12/119.53 inference(scs_inference,[],[2806,2718,2782,2784,2790,70,57,59,63,92,2,54,61,62,41])).
% 119.12/119.53 cnf(2844,plain,
% 119.12/119.53 (~P1(f18(f18(x28441,a1),x28442),a16)),
% 119.12/119.53 inference(scs_inference,[],[2806,2718,2782,2784,2790,417,166,70,57,59,63,92,2,54,61,62,41,60])).
% 119.12/119.53 cnf(2846,plain,
% 119.12/119.53 (~E(a1,f9(a16,a1))),
% 119.12/119.53 inference(scs_inference,[],[44,2806,2718,2782,2784,2790,2670,417,166,70,57,59,63,92,2,54,61,62,41,60,31])).
% 119.12/119.53 cnf(2847,plain,
% 119.12/119.53 (P5(f12(f9(a16,a1),f9(a16,a1),f12(a1,a1,a17)),f9(a16,a1))),
% 119.12/119.53 inference(scs_inference,[],[44,2806,2799,2718,2782,2784,2790,2673,2670,417,166,70,57,59,63,92,2,54,61,62,41,60,31,84])).
% 119.12/119.53 cnf(2848,plain,
% 119.12/119.53 (~P6(x28481,x28482,x28482)),
% 119.12/119.53 inference(rename_variables,[],[2673])).
% 119.12/119.53 cnf(2852,plain,
% 119.12/119.53 (~P4(f12(f9(a16,a1),f9(a16,a1),f12(a1,a1,a17)),f9(a16,a1))),
% 119.12/119.53 inference(scs_inference,[],[44,2806,2799,2718,2782,2784,2790,2673,2848,2670,417,166,70,57,59,63,92,2,54,61,62,41,60,31,84,65,90])).
% 119.12/119.53 cnf(2857,plain,
% 119.12/119.53 (E(f4(f4(a17,a1),a1),a17)),
% 119.12/119.53 inference(scs_inference,[],[44,2806,2799,2718,2786,2782,2784,2790,2673,2848,2670,2758,417,166,70,57,59,63,92,2,54,61,62,41,60,31,84,65,90,69,64])).
% 119.12/119.53 cnf(2872,plain,
% 119.12/119.53 (P4(f4(f13(a16),a16),a16)),
% 119.12/119.53 inference(scs_inference,[],[2702,63])).
% 119.12/119.53 cnf(2874,plain,
% 119.12/119.53 (~E(f4(f13(a16),a16),f13(a16))),
% 119.12/119.53 inference(scs_inference,[],[2702,63,57])).
% 119.12/119.53 cnf(2876,plain,
% 119.12/119.53 (P5(f4(f4(a17,a1),a1),a1)),
% 119.12/119.53 inference(scs_inference,[],[2832,2702,63,57,54])).
% 119.12/119.53 cnf(2878,plain,
% 119.12/119.53 (~E(a15,f18(a1,a16))),
% 119.12/119.53 inference(scs_inference,[],[2843,2832,2702,63,57,54,2])).
% 119.12/119.53 cnf(2879,plain,
% 119.12/119.53 (P5(f4(a17,a16),f9(a16,a1))),
% 119.12/119.53 inference(scs_inference,[],[2843,2793,2832,2702,2623,63,57,54,2,61])).
% 119.12/119.53 cnf(2881,plain,
% 119.12/119.53 (P5(f4(a17,a1),f9(a16,a1))),
% 119.12/119.53 inference(scs_inference,[],[2843,2793,2837,2832,2702,2623,63,57,54,2,61,62])).
% 119.12/119.53 cnf(2883,plain,
% 119.12/119.53 (~P6(x28831,a17,f4(f4(a17,a1),a1))),
% 119.12/119.53 inference(scs_inference,[],[2843,2793,2837,2857,2832,2702,2673,2623,63,57,54,2,61,62,39])).
% 119.12/119.53 cnf(2885,plain,
% 119.12/119.53 (~E(a17,f4(a17,a1))),
% 119.12/119.53 inference(scs_inference,[],[2843,2793,2837,2828,2857,2832,2702,2673,2623,63,57,54,2,61,62,39,3])).
% 119.12/119.53 cnf(2886,plain,
% 119.12/119.53 (P5(f13(a16),f18(a1,a16))),
% 119.12/119.53 inference(scs_inference,[],[2795,2843,2793,2837,2828,2857,2832,2702,2673,2623,63,57,54,2,61,62,39,3,41])).
% 119.12/119.53 cnf(2889,plain,
% 119.12/119.53 (P5(f4(a17,a16),a15)),
% 119.12/119.53 inference(scs_inference,[],[2795,2843,2793,2837,2828,2857,2832,2702,2632,2673,45,2623,63,57,54,2,61,62,39,3,41,34,60])).
% 119.12/119.53 cnf(2891,plain,
% 119.12/119.53 (P5(f12(f18(a1,a16),f9(a16,a1),f13(a16)),f18(a1,a16))),
% 119.12/119.53 inference(scs_inference,[],[2795,2843,2793,2837,2828,2857,2832,2737,2702,2632,2673,45,2623,63,57,54,2,61,62,39,3,41,34,60,84])).
% 119.12/119.53 cnf(2892,plain,
% 119.12/119.53 (~P6(x28921,f9(a16,a1),f18(a1,a16))),
% 119.12/119.53 inference(rename_variables,[],[2737])).
% 119.12/119.53 cnf(2898,plain,
% 119.12/119.53 (P1(a1,a1)),
% 119.12/119.53 inference(scs_inference,[],[44,2795,2843,2793,2837,2828,2857,2832,2737,2892,2702,2632,2673,45,2623,63,57,54,2,61,62,39,3,41,34,60,84,85,33,86])).
% 119.12/119.53 cnf(2902,plain,
% 119.12/119.53 (P4(f4(f3(a16),a16),a16)),
% 119.12/119.53 inference(scs_inference,[],[2704,63])).
% 119.12/119.53 cnf(2904,plain,
% 119.12/119.53 (~E(f4(f3(a16),a16),f3(a16))),
% 119.12/119.53 inference(scs_inference,[],[2704,63,57])).
% 119.12/119.53 cnf(2906,plain,
% 119.12/119.53 (P5(f4(f13(a16),a16),a16)),
% 119.12/119.53 inference(scs_inference,[],[2872,2704,63,57,54])).
% 119.12/119.53 cnf(2913,plain,
% 119.12/119.53 (~E(f4(f13(a16),a16),f10(a16,a1,a16))),
% 119.12/119.53 inference(scs_inference,[],[2743,2830,2872,2834,2704,315,63,57,54,2,61,62,33])).
% 119.12/119.53 cnf(2918,plain,
% 119.12/119.53 (P5(f12(f9(a16,a1),f9(a16,a1),f4(a17,a16)),f9(a16,a1))),
% 119.12/119.53 inference(scs_inference,[],[2879,2878,2743,2830,2872,2834,2704,315,372,2673,170,2623,63,57,54,2,61,62,33,3,41,60,84])).
% 119.12/119.53 cnf(2919,plain,
% 119.12/119.53 (~P6(x29191,x29192,x29192)),
% 119.12/119.53 inference(rename_variables,[],[2673])).
% 119.12/119.53 cnf(2924,plain,
% 119.12/119.53 (P1(a16,a16)),
% 119.12/119.53 inference(scs_inference,[],[2879,2881,2878,2743,2830,2872,2834,2704,315,372,2673,2919,45,170,2623,63,57,54,2,61,62,33,3,41,60,84,85,86])).
% 119.12/119.53 cnf(2941,plain,
% 119.12/119.53 (P4(f4(f4(a17,a16),a16),a16)),
% 119.12/119.53 inference(scs_inference,[],[2716,63])).
% 119.12/119.53 cnf(2943,plain,
% 119.12/119.53 (~E(f4(f4(a17,a16),a16),f4(a17,a16))),
% 119.12/119.53 inference(scs_inference,[],[2716,63,57])).
% 119.12/119.53 cnf(2945,plain,
% 119.12/119.53 (P5(f4(f3(a16),a16),a16)),
% 119.12/119.53 inference(scs_inference,[],[2902,2716,63,57,54])).
% 119.12/119.53 cnf(2948,plain,
% 119.12/119.53 (P5(f12(a16,a16,a17),f9(a16,a1))),
% 119.12/119.53 inference(scs_inference,[],[2846,2753,2902,2716,2623,63,57,54,2,61])).
% 119.12/119.53 cnf(2950,plain,
% 119.12/119.53 (P5(f3(a1),f9(a16,a1))),
% 119.12/119.53 inference(scs_inference,[],[2846,2733,2753,2902,2716,2623,63,57,54,2,61,62])).
% 119.12/119.53 cnf(2952,plain,
% 119.12/119.53 (~P5(f5(f9(a16,a1),a15),f18(a15,a15))),
% 119.12/119.53 inference(scs_inference,[],[2846,2733,2753,2902,2716,2722,2623,63,57,54,2,61,62,93])).
% 119.12/119.53 cnf(2955,plain,
% 119.12/119.53 (P5(f3(a1),a15)),
% 119.12/119.53 inference(scs_inference,[],[44,2846,2733,2753,2918,2902,2716,2722,2623,63,57,54,2,61,62,93,41,60])).
% 119.12/119.53 cnf(2968,plain,
% 119.12/119.53 (P5(f4(f4(a17,a16),a16),a16)),
% 119.12/119.53 inference(scs_inference,[],[2941,54])).
% 119.12/119.53 cnf(2971,plain,
% 119.12/119.53 (~P6(x29711,f4(f4(a17,a1),a1),a17)),
% 119.12/119.53 inference(scs_inference,[],[2728,2941,2857,2673,54,2,38])).
% 119.12/119.53 cnf(2972,plain,
% 119.12/119.53 (~P6(x29721,x29722,x29722)),
% 119.12/119.53 inference(rename_variables,[],[2673])).
% 119.12/119.53 cnf(2975,plain,
% 119.12/119.53 (~E(f18(a15,a15),f18(f9(a16,a1),x29751))),
% 119.12/119.53 inference(scs_inference,[],[2728,2941,2826,2830,2857,2673,54,2,38,61,62])).
% 119.12/119.53 cnf(2981,plain,
% 119.12/119.53 (~P6(x29811,x29812,x29812)),
% 119.12/119.53 inference(rename_variables,[],[2673])).
% 119.12/119.53 cnf(2983,plain,
% 119.12/119.53 (P5(f12(f9(a16,a1),f9(a16,a1),f12(a16,a16,a17)),f9(a16,a1))),
% 119.12/119.53 inference(scs_inference,[],[2948,2728,2889,2941,2826,403,2830,2857,2673,2972,2981,166,54,2,38,61,62,41,60,84,85])).
% 119.12/119.53 cnf(2987,plain,
% 119.12/119.53 (~P5(f2(a1),a16)),
% 119.12/119.53 inference(scs_inference,[],[2948,2728,2889,2941,2712,2826,2634,2632,403,2830,2857,2673,2972,2981,166,47,54,2,38,61,62,41,60,84,85,36,82])).
% 119.12/119.53 cnf(2991,plain,
% 119.12/119.53 (~E(f7(a1,f2(a1)),f18(a16,a16))),
% 119.12/119.53 inference(scs_inference,[],[2948,2728,2889,2652,2941,2712,2826,2634,2632,403,2830,2857,2673,2972,2981,166,47,54,2,38,61,62,41,60,84,85,36,82,65])).
% 119.12/119.53 cnf(2994,plain,
% 119.12/119.53 (E(a17,f4(f4(a17,a16),a16))),
% 119.12/119.53 inference(scs_inference,[],[2948,2728,2889,2943,2652,2941,2712,2826,2634,2632,403,2830,2857,2716,2673,2972,2981,2700,166,47,54,2,38,61,62,41,60,84,85,36,82,65,64])).
% 119.12/119.53 cnf(2999,plain,
% 119.12/119.53 (P5(f4(f3(a1),a1),a1)),
% 119.12/119.53 inference(scs_inference,[],[2617,54])).
% 119.12/119.53 cnf(3001,plain,
% 119.12/119.53 (~E(f2(a16),a17)),
% 119.12/119.53 inference(scs_inference,[],[2771,2617,54,2])).
% 119.12/119.53 cnf(3002,plain,
% 119.12/119.53 (P5(f4(f4(a17,a16),a16),f9(a16,a1))),
% 119.12/119.53 inference(scs_inference,[],[2771,2968,2617,2623,54,2,61])).
% 119.12/119.53 cnf(3004,plain,
% 119.12/119.53 (P5(f12(a1,a1,f12(a1,a1,a17)),f9(a16,a1))),
% 119.12/119.53 inference(scs_inference,[],[2771,2807,2968,2617,2623,54,2,61,62])).
% 119.12/119.53 cnf(3006,plain,
% 119.12/119.53 (~E(f4(f4(a17,a16),a16),f2(a1))),
% 119.12/119.53 inference(scs_inference,[],[2771,2987,2807,2968,2617,2623,54,2,61,62,40])).
% 119.12/119.53 cnf(3007,plain,
% 119.12/119.53 (P2(f12(f9(a16,a1),f9(a16,a1),f12(a1,a1,a17)),f9(a16,a1))),
% 119.12/119.53 inference(scs_inference,[],[2771,2987,2852,2807,2968,2847,2617,2623,54,2,61,62,40,58])).
% 119.12/119.53 cnf(3009,plain,
% 119.12/119.53 (P4(f4(f4(a17,a16),a16),a1)),
% 119.12/119.53 inference(scs_inference,[],[2771,2987,2852,2807,2994,2968,2847,2617,2758,2623,54,2,61,62,40,58,33])).
% 119.12/119.53 cnf(3012,plain,
% 119.12/119.53 (~P1(f11(a1,f2(a1)),a16)),
% 119.12/119.53 inference(scs_inference,[],[2771,2987,2852,2654,2807,2994,2968,2847,2617,2758,2623,46,54,2,61,62,40,58,33,36,60])).
% 119.12/119.53 cnf(3013,plain,
% 119.12/119.53 (P5(f2(x30131),f11(x30131,f2(x30131)))),
% 119.12/119.53 inference(rename_variables,[],[2654])).
% 119.12/119.53 cnf(3016,plain,
% 119.12/119.53 (~E(f12(a1,a1,a17),f3(a1))),
% 119.12/119.53 inference(scs_inference,[],[2924,2771,2987,2852,2654,2807,2994,2968,2844,2847,2802,2611,2617,2758,2623,46,54,2,61,62,40,58,33,36,60,31,35])).
% 119.12/119.53 cnf(3017,plain,
% 119.12/119.53 (P5(f2(a17),f4(f4(a17,a16),a16))),
% 119.12/119.53 inference(scs_inference,[],[2924,2771,2987,2852,2654,2807,2994,2968,2844,2847,2802,2611,2617,2634,2758,2623,46,54,2,61,62,40,58,33,36,60,31,35,41])).
% 119.12/119.53 cnf(3020,plain,
% 119.12/119.53 (~P6(x30201,x30202,x30202)),
% 119.12/119.53 inference(rename_variables,[],[2673])).
% 119.12/119.53 cnf(3025,plain,
% 119.12/119.53 (~E(f11(a1,f2(a1)),f18(a16,a16))),
% 119.12/119.53 inference(scs_inference,[],[2924,2950,2771,2955,2987,2852,2654,3013,2807,2994,2968,2844,2847,2802,2611,2617,2634,2758,2673,3020,2623,46,54,2,61,62,40,58,33,36,60,31,35,41,84,85,65])).
% 119.12/119.53 cnf(3028,plain,
% 119.12/119.53 (~P4(f2(a17),f4(f4(a17,a16),a16))),
% 119.12/119.53 inference(scs_inference,[],[2924,2950,2771,2955,2987,2852,2654,3013,2807,2994,2968,2844,2847,2802,2611,2617,2634,2758,2673,3020,2623,46,54,2,61,62,40,58,33,36,60,31,35,41,84,85,65,56])).
% 119.12/119.53 cnf(3035,plain,
% 119.12/119.53 (P5(f4(f4(a17,a16),a16),a1)),
% 119.12/119.53 inference(scs_inference,[],[3009,54])).
% 119.12/119.53 cnf(3038,plain,
% 119.12/119.53 (~E(f4(f3(a16),a16),f10(a16,a1,a16))),
% 119.12/119.53 inference(scs_inference,[],[3016,3009,2902,315,54,2,33])).
% 119.12/119.53 cnf(3040,plain,
% 119.12/119.53 (P5(f2(x30401),f7(x30401,f2(x30401)))),
% 119.12/119.53 inference(rename_variables,[],[2652])).
% 119.12/119.53 cnf(3044,plain,
% 119.12/119.53 (P5(f12(a1,a1,f13(a1)),a1)),
% 119.12/119.53 inference(scs_inference,[],[3016,3009,2609,2652,3040,2902,315,2987,2673,54,2,33,60,41,84])).
% 119.12/119.53 cnf(3045,plain,
% 119.12/119.53 (~P6(x30451,x30452,x30452)),
% 119.12/119.53 inference(rename_variables,[],[2673])).
% 119.12/119.53 cnf(3047,plain,
% 119.12/119.53 (P5(f12(a1,a1,f4(a17,a1)),a1)),
% 119.12/119.53 inference(scs_inference,[],[3016,3009,2609,2837,2652,3040,2902,315,2987,2673,3045,54,2,33,60,41,84,85])).
% 119.12/119.53 cnf(3065,plain,
% 119.12/119.53 (P5(f3(a16),a16)),
% 119.12/119.53 inference(scs_inference,[],[2704,54])).
% 119.12/119.53 cnf(3072,plain,
% 119.12/119.53 (P5(f12(a1,a1,f13(a1)),f9(a16,a1))),
% 119.12/119.53 inference(scs_inference,[],[3038,3044,2818,2704,2994,2673,2623,54,2,39,61,62])).
% 119.12/119.53 cnf(3074,plain,
% 119.12/119.53 (~E(f4(f4(a17,a16),a16),f4(a17,a1))),
% 119.12/119.53 inference(scs_inference,[],[2885,3038,3044,2818,2704,2994,2673,2623,54,2,39,61,62,3])).
% 119.12/119.53 cnf(3075,plain,
% 119.12/119.53 (P5(f12(a1,a1,f13(a1)),a15)),
% 119.12/119.53 inference(scs_inference,[],[44,2885,3038,3044,2818,2704,2994,2673,2623,54,2,39,61,62,3,60])).
% 119.12/119.53 cnf(3077,plain,
% 119.12/119.53 (P5(f4(f4(a17,a16),a16),f18(a1,a16))),
% 119.12/119.53 inference(scs_inference,[],[44,2885,3038,3002,3044,2818,2704,2994,2673,2623,54,2,39,61,62,3,60,41])).
% 119.12/119.53 cnf(3095,plain,
% 119.12/119.53 (P5(f12(a16,a16,f3(a16)),a16)),
% 119.12/119.53 inference(scs_inference,[],[3065,3074,2654,374,2987,170,2673,2,60,41,85])).
% 119.12/119.53 cnf(3096,plain,
% 119.12/119.53 (~P6(x30961,x30962,x30962)),
% 119.12/119.53 inference(rename_variables,[],[2673])).
% 119.12/119.53 cnf(3098,plain,
% 119.12/119.53 (~P5(f2(a16),a1)),
% 119.12/119.53 inference(scs_inference,[],[3065,3074,2654,2632,374,2987,2634,170,2673,47,2,60,41,85,81])).
% 119.12/119.53 cnf(3104,plain,
% 119.12/119.53 (P5(f12(a16,a16,f12(a16,a16,a17)),a16)),
% 119.12/119.53 inference(scs_inference,[],[3065,3074,2881,2753,2654,2632,374,2987,2634,170,2673,3096,47,2,60,41,85,81,66,84])).
% 119.12/119.53 cnf(3107,plain,
% 119.12/119.53 (E(f4(f4(a17,a16),a16),a17)),
% 119.12/119.53 inference(scs_inference,[],[3065,3074,2786,2881,2753,2654,3009,2632,374,2782,2758,2987,2634,170,2673,3096,47,2,60,41,85,81,66,84,64])).
% 119.12/119.53 cnf(3129,plain,
% 119.12/119.53 (~P5(f2(a16),f18(a1,a1))),
% 119.12/119.53 inference(scs_inference,[],[3098,2613,2,93])).
% 119.12/119.53 cnf(3131,plain,
% 119.12/119.53 (P5(a17,f18(a1,a16))),
% 119.12/119.53 inference(scs_inference,[],[3098,3077,2613,3107,2,93,40])).
% 119.12/119.53 cnf(3132,plain,
% 119.12/119.53 (~E(a17,f2(a1))),
% 119.12/119.53 inference(scs_inference,[],[3098,3077,2613,3006,3107,2,93,40,3])).
% 119.12/119.53 cnf(3133,plain,
% 119.12/119.53 (P5(f4(f4(a17,a16),a16),a15)),
% 119.12/119.53 inference(scs_inference,[],[44,3098,3077,2613,3006,3035,3107,2,93,40,3,60])).
% 119.12/119.53 cnf(3136,plain,
% 119.12/119.53 (~E(f7(a16,f2(a16)),f18(a1,a1))),
% 119.12/119.53 inference(scs_inference,[],[44,3098,3077,2613,3004,3006,3035,3107,2652,2623,2,93,40,3,60,41,65])).
% 119.12/119.53 cnf(3139,plain,
% 119.12/119.53 (P5(f12(a1,a1,f3(a1)),a1)),
% 119.12/119.53 inference(scs_inference,[],[44,3098,3077,2613,3004,3006,3035,3107,2733,2652,2673,2623,2,93,40,3,60,41,65,85])).
% 119.12/119.53 cnf(3146,plain,
% 119.12/119.53 (~E(f2(a1),a17)),
% 119.12/119.53 inference(scs_inference,[],[3132,2])).
% 119.12/119.53 cnf(3147,plain,
% 119.12/119.53 (~E(f13(a1),f2(a16))),
% 119.12/119.53 inference(scs_inference,[],[3129,3132,1243,2,40])).
% 119.12/119.53 cnf(3149,plain,
% 119.12/119.53 (~E(f2(a16),f4(f4(a17,a16),a16))),
% 119.12/119.53 inference(scs_inference,[],[3129,3001,3132,3107,1243,2,40,3])).
% 119.12/119.53 cnf(3151,plain,
% 119.12/119.53 (P5(f2(x31511),f11(x31511,f2(x31511)))),
% 119.12/119.53 inference(rename_variables,[],[2654])).
% 119.12/119.53 cnf(3153,plain,
% 119.12/119.53 (~E(f11(a16,f2(a16)),f18(a1,a1))),
% 119.12/119.53 inference(scs_inference,[],[3129,3001,3132,2654,3151,3107,1243,2,40,3,60,41])).
% 119.12/119.53 cnf(3155,plain,
% 119.12/119.53 (P5(f12(f18(a1,a16),f18(a1,a16),a17),f18(a1,a16))),
% 119.12/119.53 inference(scs_inference,[],[3129,3131,3001,3132,2654,3151,3107,1243,2673,2,40,3,60,41,84])).
% 119.12/119.53 cnf(3156,plain,
% 119.12/119.53 (~P6(x31561,x31562,x31562)),
% 119.12/119.53 inference(rename_variables,[],[2673])).
% 119.12/119.53 cnf(3158,plain,
% 119.12/119.53 (P5(f12(a16,a16,f4(a17,a16)),a16)),
% 119.12/119.53 inference(scs_inference,[],[3129,3131,3001,3132,2793,2654,3151,3107,1243,2673,3156,2,40,3,60,41,84,85])).
% 119.12/119.53 cnf(3159,plain,
% 119.12/119.53 (~P6(x31591,x31592,x31592)),
% 119.12/119.53 inference(rename_variables,[],[2673])).
% 119.12/119.53 cnf(3161,plain,
% 119.12/119.53 (~P4(f12(f18(a1,a16),f18(a1,a16),a17),f18(a1,a16))),
% 119.12/119.53 inference(scs_inference,[],[3129,3131,3001,3132,2793,2654,3151,3107,1243,2673,3156,3159,2,40,3,60,41,84,85,90])).
% 119.12/119.53 cnf(3168,plain,
% 119.12/119.53 (~E(f2(a16),f13(a1))),
% 119.12/119.53 inference(scs_inference,[],[3147,2])).
% 119.12/119.53 cnf(3171,plain,
% 119.12/119.53 (~P4(f12(f18(a1,a16),f18(a1,a16),a17),f9(a16,a1))),
% 119.12/119.53 inference(scs_inference,[],[3147,3161,3155,2623,2,58,34])).
% 119.12/119.53 cnf(3172,plain,
% 119.12/119.53 (~P5(f2(a16),f18(f18(a1,a1),f18(a1,a1)))),
% 119.12/119.53 inference(scs_inference,[],[3147,3161,3155,3129,2623,2,58,34,93])).
% 119.12/119.53 cnf(3174,plain,
% 119.12/119.53 (P5(a17,a15)),
% 119.12/119.53 inference(scs_inference,[],[3147,3161,3155,3133,3129,3107,2623,2,58,34,93,40])).
% 119.12/119.53 cnf(3175,plain,
% 119.12/119.53 (~E(f12(a1,a1,a17),f10(a16,a1,a1))),
% 119.12/119.53 inference(scs_inference,[],[3147,3161,3155,3133,110,2802,3129,3107,2623,2,58,34,93,40,35])).
% 119.12/119.53 cnf(3178,plain,
% 119.12/119.53 (P5(f12(f9(a16,a1),f9(a16,a1),f12(a16,a16,a17)),f18(a1,a16))),
% 119.12/119.53 inference(scs_inference,[],[44,3147,2983,3161,3155,2999,3133,110,2802,3129,3107,2623,2,58,34,93,40,35,60,41])).
% 119.12/119.53 cnf(3204,plain,
% 119.12/119.53 (P2(f12(f9(a16,a1),f9(a16,a1),f12(a1,a1,a17)),f18(a1,a16))),
% 119.12/119.53 inference(scs_inference,[],[3175,3007,2623,2,36])).
% 119.12/119.53 cnf(3207,plain,
% 119.12/119.53 (~P1(f7(a16,f2(a16)),a1)),
% 119.12/119.53 inference(scs_inference,[],[3175,2952,3007,3098,2652,334,2623,2,36,40,60])).
% 119.12/119.53 cnf(3208,plain,
% 119.12/119.53 (P5(f2(x32081),f7(x32081,f2(x32081)))),
% 119.12/119.53 inference(rename_variables,[],[2652])).
% 119.12/119.53 cnf(3212,plain,
% 119.12/119.53 (P5(f12(a15,a15,a17),a15)),
% 119.12/119.53 inference(scs_inference,[],[3174,3175,2952,3007,3098,2652,3208,334,2673,2623,2,36,40,60,41,84])).
% 119.12/119.53 cnf(3213,plain,
% 119.12/119.53 (~P6(x32131,x32132,x32132)),
% 119.12/119.53 inference(rename_variables,[],[2673])).
% 119.12/119.53 cnf(3215,plain,
% 119.12/119.53 (~P4(f12(a15,a15,a17),a15)),
% 119.12/119.53 inference(scs_inference,[],[3174,3175,2952,3007,3098,2652,3208,334,2673,3213,2623,2,36,40,60,41,84,90])).
% 119.12/119.53 cnf(3218,plain,
% 119.12/119.53 (~P4(f12(f9(a16,a1),f9(a16,a1),f12(a1,a1,a17)),f18(a1,a16))),
% 119.12/119.53 inference(scs_inference,[],[3174,3175,2952,3007,3098,2652,3208,334,2673,3213,2623,2,36,40,60,41,84,90,56])).
% 119.12/119.53 cnf(3220,plain,
% 119.12/119.53 (P5(f12(f9(a16,a1),f9(a16,a1),f12(a1,a1,a17)),f18(a1,a16))),
% 119.12/119.53 inference(scs_inference,[],[3174,3175,2952,3007,3098,2652,3208,334,2673,3213,2623,2,36,40,60,41,84,90,56,55])).
% 119.12/119.53 cnf(3222,plain,
% 119.12/119.53 (P1(f7(a15,f12(a15,a15,a17)),a15)),
% 119.12/119.53 inference(scs_inference,[],[3174,3175,2952,3007,3098,2652,3208,334,2673,3213,2623,2,36,40,60,41,84,90,56,55,68])).
% 119.12/119.53 cnf(3234,plain,
% 119.12/119.53 (P5(f4(f4(a17,a1),a1),f9(a16,a1))),
% 119.12/119.53 inference(scs_inference,[],[3174,3175,2876,3095,2952,3007,3098,2652,3208,334,2673,3213,2623,2,36,40,60,41,84,90,56,55,68,79,66,67,69,61,62])).
% 119.12/119.53 cnf(3258,plain,
% 119.12/119.53 (~P6(x32581,a17,f4(f4(a17,a16),a16))),
% 119.12/119.53 inference(scs_inference,[],[2874,3107,2673,2,39])).
% 119.12/119.53 cnf(3259,plain,
% 119.12/119.53 (~P6(x32591,x32592,x32592)),
% 119.12/119.53 inference(rename_variables,[],[2673])).
% 119.12/119.53 cnf(3260,plain,
% 119.12/119.53 (~E(f4(f3(a1),a1),f10(a1,a1,a15))),
% 119.12/119.53 inference(scs_inference,[],[2874,2617,160,3107,2673,2,39,33])).
% 119.12/119.53 cnf(3262,plain,
% 119.12/119.53 (P5(a17,f9(a16,a1))),
% 119.12/119.53 inference(scs_inference,[],[2898,3234,2874,3207,2617,160,3107,2857,2673,2,39,33,31,40])).
% 119.12/119.53 cnf(3266,plain,
% 119.12/119.53 (P5(f12(a15,a15,f12(a15,a15,a17)),a15)),
% 119.12/119.53 inference(scs_inference,[],[44,2898,3212,3234,2874,2640,3207,2617,160,3107,2857,2673,3259,2623,2,39,33,31,40,60,41,84])).
% 119.12/119.53 cnf(3271,plain,
% 119.12/119.53 (P5(f12(f9(a16,a1),f18(a1,a16),f13(a16)),f18(a1,a16))),
% 119.12/119.53 inference(scs_inference,[],[44,2898,3212,3234,2874,2640,3207,2955,2741,2617,160,2886,3107,2857,2795,2673,3259,2623,2,39,33,31,40,60,41,84,68,85])).
% 119.12/119.53 cnf(3298,plain,
% 119.12/119.53 (~E(f10(a16,a1,a1),f5(f18(a1,a16),f18(a15,a15)))),
% 119.12/119.53 inference(scs_inference,[],[3260,2788,136,2,40])).
% 119.12/119.53 cnf(3301,plain,
% 119.12/119.53 (P5(f2(x33011),f11(x33011,f2(x33011)))),
% 119.12/119.53 inference(rename_variables,[],[2654])).
% 119.12/119.53 cnf(3308,plain,
% 119.12/119.53 (P5(f12(f9(a16,a1),f18(a1,a16),a17),f18(a1,a16))),
% 119.12/119.53 inference(scs_inference,[],[3262,3260,2788,3131,2741,2654,3301,3098,136,2673,2,40,60,41,84,85])).
% 119.12/119.53 cnf(3336,plain,
% 119.12/119.53 (~P5(f12(a1,a1,a17),a16)),
% 119.12/119.53 inference(scs_inference,[],[44,3146,2904,3047,2760,3107,2750,47,2,3,60,82])).
% 119.12/119.53 cnf(3338,plain,
% 119.12/119.53 (~E(f11(a1,f12(a1,a1,a17)),f18(a16,a16))),
% 119.12/119.53 inference(scs_inference,[],[44,3146,2904,2765,3047,2760,3107,2750,47,2,3,60,82,65])).
% 119.12/119.53 cnf(3340,plain,
% 119.12/119.53 (P5(f12(f18(a16,x33401),f18(a16,x33401),f10(a16,a1,a1)),f18(a16,x33401))),
% 119.12/119.53 inference(scs_inference,[],[44,3146,2904,2765,3047,2760,106,3107,2750,2673,47,2,3,60,82,65,85])).
% 119.12/119.53 cnf(3372,plain,
% 119.12/119.53 (~E(f7(a1,f12(a1,a1,a17)),f18(a16,a16))),
% 119.12/119.53 inference(scs_inference,[],[3336,3338,2767,2,60,65])).
% 119.12/119.53 cnf(3399,plain,
% 119.12/119.53 (P5(f12(a1,a1,f3(a1)),a15)),
% 119.12/119.53 inference(scs_inference,[],[44,3372,3104,3139,3215,3212,156,2788,2802,332,2623,2,58,61,62,35,40,60])).
% 119.12/119.53 cnf(3434,plain,
% 119.12/119.53 (~E(f4(f4(a17,a16),a16),f10(a16,a1,a16))),
% 119.12/119.53 inference(scs_inference,[],[2991,2941,315,2,33])).
% 119.12/119.53 cnf(3435,plain,
% 119.12/119.53 (P5(f4(f4(a17,a1),a1),a15)),
% 119.12/119.53 inference(scs_inference,[],[44,2991,2876,2941,315,2,33,60])).
% 119.12/119.53 cnf(3437,plain,
% 119.12/119.53 (~E(f11(a1,f12(a1,a1,a17)),a16)),
% 119.12/119.53 inference(scs_inference,[],[44,2991,2876,2765,2941,315,3336,2,33,60,41])).
% 119.12/119.53 cnf(3440,plain,
% 119.12/119.53 (P5(f12(a16,a16,f4(a17,a16)),f9(a16,a1))),
% 119.12/119.53 inference(scs_inference,[],[44,2991,3158,2876,2948,2765,2941,315,3336,2623,2,33,60,41,67,61])).
% 119.12/119.53 cnf(3444,plain,
% 119.12/119.53 (P5(f12(f18(a1,a16),f9(a16,a1),a17),f18(a1,a16))),
% 119.12/119.53 inference(scs_inference,[],[44,2991,3158,2999,2876,2948,2765,2737,2941,315,3336,3262,3131,2623,2,33,60,41,67,61,62,84])).
% 119.12/119.53 cnf(3466,plain,
% 119.12/119.53 (~E(f10(a16,a1,a16),f4(f4(a17,a16),a16))),
% 119.12/119.53 inference(scs_inference,[],[3434,2])).
% 119.12/119.53 cnf(3483,plain,
% 119.12/119.53 (P5(f4(f3(a16),a16),f9(a16,a1))),
% 119.12/119.53 inference(scs_inference,[],[3136,2945,2623,2,61])).
% 119.12/119.53 cnf(3485,plain,
% 119.12/119.53 (P5(f4(f13(a1),a1),f9(a16,a1))),
% 119.12/119.53 inference(scs_inference,[],[3136,2945,2640,2623,2,61,62])).
% 119.12/119.53 cnf(3487,plain,
% 119.12/119.53 (~E(f10(a16,a1,a16),a17)),
% 119.12/119.53 inference(scs_inference,[],[3136,3466,2945,2640,2994,2623,2,61,62,3])).
% 119.12/119.53 cnf(3513,plain,
% 119.12/119.53 (~P5(f2(a1),f18(a16,a16))),
% 119.12/119.53 inference(scs_inference,[],[3025,2987,2,93])).
% 119.12/119.53 cnf(3522,plain,
% 119.12/119.53 (~P4(f12(a1,a1,f13(a1)),a1)),
% 119.12/119.53 inference(scs_inference,[],[3485,3025,2609,2804,358,2987,170,3336,2673,2623,2,93,61,62,60,41,90])).
% 119.12/119.53 cnf(3549,plain,
% 119.12/119.53 (P2(f12(a1,a1,f13(a1)),a1)),
% 119.12/119.53 inference(scs_inference,[],[3153,3522,3044,2,58])).
% 119.12/119.53 cnf(3551,plain,
% 119.12/119.53 (P5(f4(f13(a16),a16),f9(a16,a1))),
% 119.12/119.53 inference(scs_inference,[],[3153,3522,2906,3044,2623,2,58,61])).
% 119.12/119.53 cnf(3553,plain,
% 119.12/119.53 (P5(f12(a1,a1,f4(a17,a1)),f9(a16,a1))),
% 119.12/119.53 inference(scs_inference,[],[3153,3522,2906,3047,3044,2623,2,58,61,62])).
% 119.12/119.53 cnf(3555,plain,
% 119.12/119.53 (~E(f12(a1,a1,a17),f4(f13(a1),a1))),
% 119.12/119.53 inference(scs_inference,[],[3153,3522,2906,3047,1245,3044,2802,2623,2,58,61,62,35])).
% 119.12/119.53 cnf(3556,plain,
% 119.12/119.53 (~E(f12(f18(a16,a16),f18(a16,a16),f10(a16,a1,a1)),f2(a1))),
% 119.12/119.53 inference(scs_inference,[],[3513,3153,3340,3522,2906,3047,1245,3044,2802,2623,2,58,61,62,35,40])).
% 119.12/119.53 cnf(3558,plain,
% 119.12/119.53 (P5(f4(a17,a1),a15)),
% 119.12/119.53 inference(scs_inference,[],[44,3513,3153,3340,3522,2906,3047,1245,3044,2837,2802,2623,2,58,61,62,35,40,60])).
% 119.12/119.53 cnf(3563,plain,
% 119.12/119.53 (P5(f12(a15,a15,f4(a17,a1)),a15)),
% 119.12/119.53 inference(scs_inference,[],[44,3513,3153,3340,2656,3522,2906,3047,1245,3044,2837,419,2802,166,2673,2623,2,58,61,62,35,40,60,41,52,85])).
% 119.12/119.53 cnf(3573,plain,
% 119.12/119.53 (~P4(f12(a15,a15,f4(a17,a1)),a15)),
% 119.12/119.53 inference(scs_inference,[],[3558,3551,2913,3513,2654,2673,2623,2,60,41,90])).
% 119.12/119.53 cnf(3601,plain,
% 119.12/119.53 (P5(f13(a1),a15)),
% 119.12/119.53 inference(scs_inference,[],[44,2650,3522,2605,2609,2,33,60])).
% 119.12/119.53 cnf(3605,plain,
% 119.12/119.53 (P5(f12(a15,a15,f13(a1)),a15)),
% 119.12/119.53 inference(scs_inference,[],[44,2650,222,3522,2605,2609,298,166,2673,2,33,60,41,36,84])).
% 119.12/119.53 cnf(3615,plain,
% 119.12/119.53 (P5(f4(f3(a16),a16),f18(a1,a16))),
% 119.12/119.53 inference(scs_inference,[],[3483,3556,3513,2652,2623,2,60,41])).
% 119.12/119.53 cnf(3616,plain,
% 119.12/119.53 (~P5(f12(a1,a1,f13(a1)),a16)),
% 119.12/119.53 inference(scs_inference,[],[3483,3556,3522,3513,3044,2652,2623,47,2,60,41,82])).
% 119.12/119.53 cnf(3618,plain,
% 119.12/119.53 (~E(f9(a16,a1),f18(a16,a16))),
% 119.12/119.53 inference(scs_inference,[],[3483,3072,3556,3522,3513,3044,2652,2623,47,2,60,41,82,65])).
% 119.12/119.53 cnf(3622,plain,
% 119.12/119.53 (~E(a16,f18(x36221,f9(a16,a1)))),
% 119.12/119.53 inference(scs_inference,[],[3601,3483,3072,3556,3522,3513,3044,2652,2623,47,2,60,41,82,65,66,61])).
% 119.12/119.53 cnf(3624,plain,
% 119.12/119.53 (~E(a16,f18(f9(a16,a1),x36241))),
% 119.12/119.53 inference(scs_inference,[],[3601,3483,3072,3556,3522,3513,3044,2652,2623,47,2,60,41,82,65,66,61,62])).
% 119.12/119.53 cnf(3648,plain,
% 119.12/119.53 (P5(f3(a16),f9(a16,a1))),
% 119.12/119.53 inference(scs_inference,[],[3618,3065,2623,2,61])).
% 119.12/119.53 cnf(3651,plain,
% 119.12/119.53 (P5(f13(a1),f9(a16,a1))),
% 119.12/119.53 inference(scs_inference,[],[3618,3487,3065,2609,2857,2623,2,61,3,62])).
% 119.12/119.53 cnf(3653,plain,
% 119.12/119.53 (~P1(a15,a16)),
% 119.12/119.53 inference(scs_inference,[],[3618,3487,3075,3616,3065,2609,2857,2623,2,61,3,62,60])).
% 119.12/119.53 cnf(3656,plain,
% 119.12/119.53 (~P5(f5(a15,a16),a16)),
% 119.12/119.53 inference(scs_inference,[],[3618,3487,3075,3616,3065,2609,401,2857,166,2623,2,61,3,62,60,41,70])).
% 119.12/119.53 cnf(3658,plain,
% 119.12/119.53 (P5(f5(a15,a16),a15)),
% 119.12/119.53 inference(scs_inference,[],[3618,3487,3075,3616,3065,2609,401,2857,166,2623,2,61,3,62,60,41,70,59])).
% 119.12/119.53 cnf(3662,plain,
% 119.12/119.53 (P5(f12(f9(a16,a1),f18(a1,a16),f13(a1)),f18(a1,a16))),
% 119.12/119.53 inference(scs_inference,[],[3618,3487,3178,3075,3616,3065,2609,401,2741,2857,1243,166,2623,2,61,3,62,60,41,70,59,93,85])).
% 119.12/119.53 cnf(3668,plain,
% 119.12/119.53 (~E(f11(x36681,f2(x36681)),x36681)),
% 119.12/119.53 inference(scs_inference,[],[2664,2])).
% 119.12/119.53 cnf(3669,plain,
% 119.12/119.53 (~P5(f5(a15,a16),f18(a16,a16))),
% 119.12/119.53 inference(scs_inference,[],[3656,2664,2,93])).
% 119.12/119.53 cnf(3671,plain,
% 119.12/119.53 (~E(f18(a16,a16),f18(x36711,a15))),
% 119.12/119.53 inference(scs_inference,[],[3656,3658,2664,2,93,61])).
% 119.12/119.53 cnf(3673,plain,
% 119.12/119.53 (~E(f11(a16,f2(a16)),a15)),
% 119.12/119.53 inference(scs_inference,[],[3653,3656,3658,2658,2664,2,93,61,31])).
% 119.12/119.53 cnf(3679,plain,
% 119.12/119.53 (P5(f3(a16),f18(a1,a16))),
% 119.12/119.53 inference(scs_inference,[],[3653,3648,3656,3658,2658,2664,360,170,2623,2,93,61,31,62,60,41])).
% 119.12/119.53 cnf(3683,plain,
% 119.12/119.53 (P5(f12(f9(a16,a1),f18(a1,a16),f3(a16)),f18(a1,a16))),
% 119.12/119.53 inference(scs_inference,[],[3653,3648,3656,3658,2658,2664,2737,360,2741,170,2623,2,93,61,31,62,60,41,84,85])).
% 119.12/119.53 cnf(3686,plain,
% 119.12/119.53 (~P2(f4(f4(a17,a16),a16),x36861)+P2(a17,x36861)),
% 119.12/119.53 inference(scs_inference,[],[3653,3648,3656,3658,2658,2664,2737,360,2741,3107,170,2623,2,93,61,31,62,60,41,84,85,35])).
% 119.12/119.53 cnf(3698,plain,
% 119.12/119.53 (P7(f11(x36981,f2(x36981)))),
% 119.12/119.53 inference(scs_inference,[],[2735,3668,2658,2,52])).
% 119.12/119.53 cnf(3703,plain,
% 119.12/119.53 (~E(a16,f18(x37031,a1))),
% 119.12/119.53 inference(scs_inference,[],[2735,3668,3573,3563,2658,3616,3044,2,52,58,61])).
% 119.12/119.53 cnf(3708,plain,
% 119.12/119.53 (~E(f12(f18(a16,a16),f18(a16,a16),f10(a16,a1,a1)),f5(a15,a16))),
% 119.12/119.53 inference(scs_inference,[],[3669,2735,3668,3573,3563,3549,3340,2658,3616,2611,3044,2,52,58,61,62,35,40])).
% 119.12/119.53 cnf(3726,plain,
% 119.12/119.53 (~P5(f5(a15,a16),f18(f18(a16,a16),f18(a16,a16)))),
% 119.12/119.53 inference(scs_inference,[],[3669,3651,2735,3668,3573,3563,3549,3340,2658,3616,2611,3658,417,3044,2741,1243,166,2673,2,52,58,61,62,35,40,60,41,85,84,70,91,59,93])).
% 119.12/119.53 cnf(3750,plain,
% 119.12/119.53 (~E(f18(f18(a16,a16),f18(a16,a16)),f18(x37501,a15))),
% 119.12/119.53 inference(scs_inference,[],[3708,3726,3658,2,61])).
% 119.12/119.53 cnf(3753,plain,
% 119.12/119.53 (~E(f18(f18(a16,a16),f18(a16,a16)),f18(a15,x37531))),
% 119.12/119.53 inference(scs_inference,[],[3708,3726,3012,2924,3658,2,61,31,62])).
% 119.12/119.53 cnf(3766,plain,
% 119.12/119.53 (~E(f12(a1,a1,f13(a1)),f10(a16,a1,a1))),
% 119.12/119.53 inference(scs_inference,[],[3679,3553,2891,3708,3726,3012,2924,3549,110,3648,3658,2737,2673,2623,2,61,31,62,60,41,84,85,93,35])).
% 119.12/119.53 cnf(3767,plain,
% 119.12/119.53 (~E(f11(x37671,f2(x37671)),x37672)+P7(x37672)),
% 119.12/119.53 inference(scs_inference,[],[3679,3553,2891,3708,3698,3726,3012,2924,3549,110,3648,3658,2737,2673,2623,2,61,31,62,60,41,84,85,93,35,43])).
% 119.12/119.53 cnf(3770,plain,
% 119.12/119.53 (~P5(f12(a1,a1,f13(a1)),f18(a16,a16))),
% 119.12/119.53 inference(scs_inference,[],[3766,3616,2,93])).
% 119.12/119.53 cnf(3772,plain,
% 119.12/119.53 (~E(f18(f18(a1,a1),f18(a1,a1)),f18(x37721,a15))),
% 119.12/119.53 inference(scs_inference,[],[3766,3616,209,201,2,93,61])).
% 119.12/119.53 cnf(3774,plain,
% 119.12/119.53 (~E(f13(a1),f12(a1,a1,f13(a1)))),
% 119.12/119.53 inference(scs_inference,[],[3766,2607,3522,3616,209,201,2,93,61,33])).
% 119.12/119.53 cnf(3775,plain,
% 119.12/119.53 (~E(f18(f18(a1,a1),f18(a1,a1)),f18(a16,x37751))),
% 119.12/119.53 inference(scs_inference,[],[3766,2607,3522,3616,209,98,144,201,2,93,61,33,62])).
% 119.12/119.53 cnf(3777,plain,
% 119.12/119.53 (~P1(f9(a16,a1),a16)),
% 119.12/119.53 inference(scs_inference,[],[3766,2607,3522,3072,3616,209,98,144,201,2,93,61,33,62,60])).
% 119.12/119.53 cnf(3782,plain,
% 119.12/119.53 (~P5(f5(f9(a16,a1),a16),a16)),
% 119.12/119.53 inference(scs_inference,[],[3766,2607,3679,3522,3072,3616,3648,209,98,144,201,2741,2,93,61,33,62,60,84,70])).
% 119.12/119.53 cnf(3784,plain,
% 119.12/119.53 (P5(f5(f9(a16,a1),a16),f9(a16,a1))),
% 119.12/119.53 inference(scs_inference,[],[3766,2607,3679,3522,3072,3616,3648,209,98,144,201,2741,2,93,61,33,62,60,84,70,59])).
% 119.12/119.53 cnf(3790,plain,
% 119.12/119.53 (~E(f7(a16,f2(a16)),f9(a16,a1))),
% 119.12/119.53 inference(scs_inference,[],[3777,3750,2656,2,31])).
% 119.12/119.53 cnf(3792,plain,
% 119.12/119.53 (~P1(f18(x37921,f18(x37922,a1)),a16)),
% 119.12/119.53 inference(scs_inference,[],[3777,3750,2656,419,166,2,31,60])).
% 119.12/119.53 cnf(3796,plain,
% 119.12/119.53 (~E(f9(a16,a1),f18(f18(a16,a16),f18(a16,a16)))),
% 119.12/119.53 inference(scs_inference,[],[3777,3770,3271,3750,2656,419,3072,166,2,31,60,93,65])).
% 119.12/119.53 cnf(3800,plain,
% 119.12/119.53 (~E(f9(a16,a1),f7(a16,f2(a16)))),
% 119.12/119.53 inference(scs_inference,[],[3790,2])).
% 119.12/119.53 cnf(3806,plain,
% 119.12/119.53 (~E(f18(a16,a16),f18(f9(a16,a1),x38061))),
% 119.12/119.53 inference(scs_inference,[],[3790,3796,3784,3782,2623,2,93,61,3,62])).
% 119.12/119.53 cnf(3811,plain,
% 119.12/119.53 (~P5(f5(f9(a16,a1),f18(a16,a16)),f18(a16,a16))),
% 119.12/119.53 inference(scs_inference,[],[3790,3796,3784,3782,3770,292,3072,166,2623,2,93,61,3,62,60,41,70])).
% 119.12/119.53 cnf(3813,plain,
% 119.12/119.53 (P5(f5(f9(a16,a1),f18(a16,a16)),f9(a16,a1))),
% 119.12/119.53 inference(scs_inference,[],[3790,3796,3784,3782,3770,292,3072,166,2623,2,93,61,3,62,60,41,70,59])).
% 119.12/119.53 cnf(3819,plain,
% 119.12/119.53 (~P5(f5(f9(a16,a1),f18(a16,a16)),a16)),
% 119.12/119.53 inference(scs_inference,[],[3790,3796,3784,3782,3770,292,3072,3658,166,2673,2623,2,93,61,3,62,60,41,70,59,40,85,92])).
% 119.12/119.53 cnf(3827,plain,
% 119.12/119.53 (~E(f12(a16,a16,f12(a16,a16,a17)),f5(a15,a16))),
% 119.12/119.53 inference(scs_inference,[],[3753,3104,3656,3770,3044,2,61,62,40])).
% 119.12/119.53 cnf(3828,plain,
% 119.12/119.53 (~P1(f18(x38281,f18(a15,x38282)),a1)),
% 119.12/119.53 inference(scs_inference,[],[3753,3104,3656,3770,372,3044,151,2,61,62,40,60])).
% 119.12/119.53 cnf(3830,plain,
% 119.12/119.53 (P5(f5(f9(a16,a1),f18(a16,a16)),f18(a1,a16))),
% 119.12/119.53 inference(scs_inference,[],[3813,3753,3104,3656,3770,372,3044,151,2623,2,61,62,40,60,41])).
% 119.12/119.53 cnf(3831,plain,
% 119.12/119.53 (~P4(f12(a15,a15,f13(a1)),a15)),
% 119.12/119.53 inference(scs_inference,[],[3813,3753,3104,3601,3656,3770,372,3044,151,2673,2623,2,61,62,40,60,41,90])).
% 119.12/119.53 cnf(3836,plain,
% 119.12/119.53 (P5(f5(f9(a16,a1),f18(a16,a16)),a1)),
% 119.12/119.53 inference(scs_inference,[],[3813,3753,3819,3104,3601,3656,3770,372,3044,151,2673,2623,2,61,62,40,60,41,90,67,93])).
% 119.12/119.53 cnf(3875,plain,
% 119.12/119.53 (~P5(f5(f18(a1,a16),f18(a16,a16)),f18(a16,a16))),
% 119.12/119.53 inference(scs_inference,[],[3830,3827,3831,3605,3811,3651,3513,317,2737,1243,166,2,58,93,61,62,60,41,84,70])).
% 119.12/119.53 cnf(3877,plain,
% 119.12/119.53 (P5(f5(f18(a1,a16),f18(a16,a16)),f18(a1,a16))),
% 119.12/119.53 inference(scs_inference,[],[3830,3827,3831,3605,3811,3651,3513,317,2737,1243,166,2,58,93,61,62,60,41,84,70,59])).
% 119.12/119.53 cnf(3881,plain,
% 119.12/119.53 (~P5(f5(f18(a1,a16),f18(a16,a16)),a16)),
% 119.12/119.53 inference(scs_inference,[],[3830,3827,2769,3831,3605,3811,3651,3513,317,2737,1243,166,2,58,93,61,62,60,41,84,70,59,52,91])).
% 119.12/119.53 cnf(3886,plain,
% 119.12/119.53 (P5(f5(f18(a1,a16),f18(a16,a16)),a1)),
% 119.12/119.53 inference(scs_inference,[],[3877,3772,3881,2,93])).
% 119.12/119.53 cnf(3892,plain,
% 119.12/119.53 (~E(f12(a1,a1,f13(a1)),f10(a1,a1,a15))),
% 119.12/119.53 inference(scs_inference,[],[3877,3772,3881,3819,3549,156,3830,2,93,61,62,35])).
% 119.12/119.53 cnf(3895,plain,
% 119.12/119.53 (P5(f12(a16,a16,f4(a17,a16)),f18(a1,a16))),
% 119.12/119.53 inference(scs_inference,[],[3877,3440,3772,3881,3819,3549,156,3830,2623,2,93,61,62,35,60,41])).
% 119.12/119.53 cnf(3898,plain,
% 119.12/119.53 (~P5(f5(f18(a1,a16),a16),a16)),
% 119.12/119.53 inference(scs_inference,[],[3877,3440,3772,3881,3836,3819,3549,156,3830,3811,2623,2,93,61,62,35,60,41,65,70])).
% 119.12/119.53 cnf(3900,plain,
% 119.12/119.53 (P5(f5(f18(a1,a16),a16),f18(a1,a16))),
% 119.12/119.53 inference(scs_inference,[],[3877,3440,3772,3881,3836,3819,3549,156,3830,3811,2623,2,93,61,62,35,60,41,65,70,59])).
% 119.12/119.53 cnf(3931,plain,
% 119.12/119.53 (~P5(f5(f18(a1,a16),a16),f18(a16,a16))),
% 119.12/119.53 inference(scs_inference,[],[3892,3898,2,93])).
% 119.12/119.53 cnf(3933,plain,
% 119.12/119.53 (~E(f4(f4(a17,a16),a16),f10(a1,a1,a15))),
% 119.12/119.53 inference(scs_inference,[],[3892,3898,160,3009,2,93,33])).
% 119.12/119.53 cnf(3938,plain,
% 119.12/119.53 (~P5(f5(a1,f18(a16,a16)),f18(a16,a16))),
% 119.12/119.53 inference(scs_inference,[],[3892,3886,3792,3898,3875,2924,160,3009,319,166,2,93,33,31,60,41,70])).
% 119.12/119.53 cnf(3940,plain,
% 119.12/119.53 (P5(f5(a1,f18(a16,a16)),a1)),
% 119.12/119.53 inference(scs_inference,[],[3892,3886,3792,3898,3875,2924,160,3009,319,166,2,93,33,31,60,41,70,59])).
% 119.12/119.53 cnf(3942,plain,
% 119.12/119.53 (~P2(f4(f4(a17,a1),a1),x39421)+P2(a17,x39421)),
% 119.12/119.53 inference(scs_inference,[],[3892,3886,3792,3898,3875,2924,160,3009,319,2857,166,2,93,33,31,60,41,70,59,35])).
% 119.12/119.53 cnf(3958,plain,
% 119.12/119.53 (~E(f10(a1,a1,a15),f4(f4(a17,a16),a16))),
% 119.12/119.53 inference(scs_inference,[],[3933,3938,91,2])).
% 119.12/119.53 cnf(3959,plain,
% 119.12/119.53 (P5(f5(f18(a1,a16),a16),a1)),
% 119.12/119.53 inference(scs_inference,[],[3933,3900,3938,3898,91,2,93])).
% 119.12/119.53 cnf(3961,plain,
% 119.12/119.53 (~E(f18(f18(a1,a1),f18(a1,a1)),f18(x39611,a16))),
% 119.12/119.53 inference(scs_inference,[],[3933,3900,3938,3172,3898,2634,91,2,93,61])).
% 119.12/119.53 cnf(3964,plain,
% 119.12/119.53 (~E(f18(f18(a16,a16),f18(a16,a16)),f18(a1,x39641))),
% 119.12/119.53 inference(scs_inference,[],[3933,3900,3938,3172,3898,2634,255,174,91,2,93,61,62])).
% 119.12/119.53 cnf(3968,plain,
% 119.12/119.53 (~P5(f5(a1,a16),a16)),
% 119.12/119.53 inference(scs_inference,[],[3933,3900,3938,3172,3886,3898,3881,2634,255,174,91,2,93,61,62,60,70])).
% 119.12/119.53 cnf(3970,plain,
% 119.12/119.53 (P5(f5(a1,a16),a1)),
% 119.12/119.53 inference(scs_inference,[],[3933,3900,3938,3172,3886,3898,3881,2634,255,174,91,2,93,61,62,60,70,59])).
% 119.12/119.53 cnf(3972,plain,
% 119.12/119.53 (~E(f7(a16,f2(a16)),a15)),
% 119.12/119.53 inference(scs_inference,[],[3933,3900,3938,3172,3886,3898,3653,2656,3881,2634,255,174,91,2,93,61,62,60,70,59,31])).
% 119.12/119.53 cnf(3974,plain,
% 119.12/119.53 (~P5(f12(a1,a1,f4(a17,a1)),a16)+P4(f12(a1,a1,f4(a17,a1)),a1)),
% 119.12/119.53 inference(scs_inference,[],[3933,3900,3938,3172,3886,3898,3653,2656,3047,3881,2634,255,174,47,91,2,93,61,62,60,70,59,31,82])).
% 119.12/119.53 cnf(3979,plain,
% 119.12/119.53 (~E(f18(f18(a1,a1),f18(a1,a1)),f9(a16,a1))),
% 119.12/119.53 inference(scs_inference,[],[3775,3961,2623,2,3])).
% 119.12/119.53 cnf(3981,plain,
% 119.12/119.53 (~P5(f5(a1,a16),f18(a16,a16))),
% 119.12/119.53 inference(scs_inference,[],[3968,3775,3961,2623,2,3,93])).
% 119.12/119.53 cnf(3985,plain,
% 119.12/119.53 (P5(f12(a1,a1,f5(a1,a16)),a1)),
% 119.12/119.53 inference(scs_inference,[],[3970,3968,3775,3961,389,255,2673,2623,2,3,93,60,84])).
% 119.12/119.53 cnf(3986,plain,
% 119.12/119.53 (~P6(x39861,x39862,x39862)),
% 119.12/119.53 inference(rename_variables,[],[2673])).
% 119.12/119.53 cnf(3988,plain,
% 119.12/119.53 (~P4(f12(a1,a1,f5(a1,a16)),a1)),
% 119.12/119.53 inference(scs_inference,[],[3970,3968,3775,3961,389,255,2673,3986,2623,2,3,93,60,84,90])).
% 119.12/119.53 cnf(4012,plain,
% 119.12/119.53 (P4(f12(a16,a16,a17),a16)+P1(f11(a16,f12(a16,a16,a17)),a16)),
% 119.12/119.53 inference(scs_inference,[],[3979,3444,2753,374,151,2,60,93,69])).
% 119.12/119.53 cnf(4015,plain,
% 119.12/119.53 (P2(f12(a1,a1,f5(a1,a16)),a1)),
% 119.12/119.53 inference(scs_inference,[],[3964,3988,3985,2,58])).
% 119.12/119.53 cnf(4017,plain,
% 119.12/119.53 (~P5(f5(a1,a16),f18(f18(a16,a16),f18(a16,a16)))),
% 119.12/119.53 inference(scs_inference,[],[3964,3988,3985,3981,2,58,93])).
% 119.12/119.53 cnf(4019,plain,
% 119.12/119.53 (P5(f12(a1,a1,f5(a1,a16)),a15)),
% 119.12/119.53 inference(scs_inference,[],[44,3964,3988,3985,3981,2,58,93,60])).
% 119.12/119.53 cnf(4023,plain,
% 119.12/119.53 (~E(f18(f18(a16,a16),f18(a16,a16)),f18(x40231,a1))),
% 119.12/119.53 inference(scs_inference,[],[44,3964,2797,3988,3985,3981,3970,2,58,93,60,52,61])).
% 119.12/119.53 cnf(4028,plain,
% 119.12/119.53 (~E(f10(a16,a1,a1),f5(a1,a16))),
% 119.12/119.53 inference(scs_inference,[],[4023,4017,270,2,40])).
% 119.12/119.53 cnf(4034,plain,
% 119.12/119.53 (~E(f12(a1,a1,f5(a1,a16)),f3(a1))),
% 119.12/119.53 inference(scs_inference,[],[4023,4017,4015,3308,2611,270,3970,2,40,60,93,35])).
% 119.12/119.53 cnf(4038,plain,
% 119.12/119.53 (~E(f4(f3(a16),a16),f2(a16))),
% 119.12/119.53 inference(scs_inference,[],[4028,2902,2632,2,33])).
% 119.12/119.53 cnf(4040,plain,
% 119.12/119.53 (~P5(f12(a1,a1,a17),f18(a16,a16))),
% 119.12/119.53 inference(scs_inference,[],[4028,2902,2632,3336,2,33,93])).
% 119.12/119.53 cnf(4044,plain,
% 119.12/119.53 (P5(f12(a1,a1,f5(a1,a16)),x40441)+~E(x40441,f18(x40442,a15))),
% 119.12/119.53 inference(scs_inference,[],[4028,4019,2902,2632,106,144,3336,2,33,93,60,61])).
% 119.12/119.53 cnf(4047,plain,
% 119.12/119.53 (P5(f12(a1,a1,f5(a1,a16)),f18(x40471,a15))),
% 119.12/119.53 inference(equality_inference,[],[4044])).
% 119.12/119.53 cnf(4057,plain,
% 119.12/119.53 (P5(f12(f9(a16,a1),f9(a16,a1),f3(a16)),f9(a16,a1))),
% 119.12/119.53 inference(scs_inference,[],[4040,4034,3828,3683,2898,2765,3985,3648,2673,2623,2,62,31,60,93,85])).
% 119.12/119.53 cnf(4064,plain,
% 119.12/119.53 (~P5(f12(a1,a1,a17),f18(f18(a16,a16),f18(a16,a16)))),
% 119.12/119.53 inference(scs_inference,[],[4038,3800,4040,2623,2,3,93])).
% 119.12/119.53 cnf(4073,plain,
% 119.12/119.53 (~E(f12(a1,a1,f5(a1,a16)),f10(a16,a1,a1))),
% 119.12/119.53 inference(scs_inference,[],[2739,4015,110,2,35])).
% 119.12/119.53 cnf(4078,plain,
% 119.12/119.53 (~P5(f12(a1,a1,f5(a1,a16)),a16)),
% 119.12/119.53 inference(scs_inference,[],[2739,3662,4015,3988,110,3985,358,151,47,2,35,60,93,82])).
% 119.12/119.53 cnf(4083,plain,
% 119.12/119.53 (~P1(f18(x40831,a15),a16)),
% 119.12/119.53 inference(scs_inference,[],[4073,4078,4047,2,60])).
% 119.12/119.53 cnf(4085,plain,
% 119.12/119.53 (~P4(f12(a15,a15,f12(a15,a15,a17)),a15)),
% 119.12/119.53 inference(scs_inference,[],[4073,4078,4047,3212,2673,2,60,90])).
% 119.12/119.53 cnf(4086,plain,
% 119.12/119.53 (~P6(x40861,x40862,x40862)),
% 119.12/119.53 inference(rename_variables,[],[2673])).
% 119.12/119.53 cnf(4088,plain,
% 119.12/119.53 (~P5(f5(f18(x40881,a15),a16),a16)),
% 119.12/119.53 inference(scs_inference,[],[4073,4078,4047,3212,2673,2,60,90,70])).
% 119.12/119.53 cnf(4100,plain,
% 119.12/119.53 (P5(f12(f18(x41001,a16),f18(x41001,a16),f10(a16,a1,a1)),f18(x41001,a16))),
% 119.12/119.53 inference(scs_inference,[],[4073,3222,4078,4047,3212,104,2673,4086,2,60,90,70,59,52,61,62,93,84])).
% 119.12/119.53 cnf(4108,plain,
% 119.12/119.53 (~E(f12(a16,a16,f13(a16)),f5(a1,a16))),
% 119.12/119.53 inference(scs_inference,[],[2756,4085,3266,2818,3968,2,58,40])).
% 119.12/119.53 cnf(4111,plain,
% 119.12/119.53 (P5(f12(f9(a16,a1),f9(a16,a1),f3(a16)),x41111)+~E(x41111,f18(x41112,f9(a16,a1)))),
% 119.12/119.53 inference(scs_inference,[],[4057,2756,4085,3266,2818,3968,298,166,2,58,40,60,61])).
% 119.12/119.53 cnf(4115,plain,
% 119.12/119.53 (P5(f12(f9(a16,a1),f9(a16,a1),f3(a16)),f18(x41151,f9(a16,a1)))),
% 119.12/119.53 inference(equality_inference,[],[4111])).
% 119.12/119.53 cnf(4117,plain,
% 119.12/119.53 (~E(f13(a16),f10(a16,a1,a16))),
% 119.12/119.53 inference(scs_inference,[],[4108,2702,315,2,33])).
% 119.12/119.53 cnf(4120,plain,
% 119.12/119.53 (P5(f12(f18(x41201,a16),f18(x41201,a16),f10(a16,a1,a1)),x41202)+~E(x41202,f18(f18(x41201,a16),x41203))),
% 119.12/119.53 inference(scs_inference,[],[4108,4100,4064,2702,315,2799,2,33,60,62])).
% 119.12/119.53 cnf(4127,plain,
% 119.12/119.53 (~E(f11(a16,f2(a16)),f18(x41271,a15))),
% 119.12/119.53 inference(scs_inference,[],[4117,4083,2658,2,31])).
% 119.12/119.53 cnf(4146,plain,
% 119.12/119.53 (~P1(f18(x41461,f18(a1,x41462)),a16)),
% 119.12/119.53 inference(scs_inference,[],[4127,401,166,2,60])).
% 119.12/119.53 cnf(4161,plain,
% 119.12/119.53 (~E(f12(f18(a16,a16),f18(a16,a16),f10(a16,a1,a1)),f5(a1,a16))),
% 119.12/119.53 inference(scs_inference,[],[2975,4100,3981,2,40])).
% 119.12/119.53 cnf(4171,plain,
% 119.12/119.53 (~E(f4(f3(a1),a1),f12(a1,a1,a17))),
% 119.12/119.53 inference(scs_inference,[],[4161,2617,2760,2,33])).
% 119.12/119.53 cnf(4174,plain,
% 119.12/119.53 (P5(f12(f18(a15,x41741),f18(a15,x41741),f10(a16,a1,a1)),f18(a15,x41741))),
% 119.12/119.53 inference(scs_inference,[],[4161,2617,2760,138,136,144,2673,2,33,60,85])).
% 119.12/119.53 cnf(4186,plain,
% 119.12/119.53 (~P5(f12(a16,a16,f4(a17,a16)),a1)+P4(f12(a16,a16,f4(a17,a16)),a16)),
% 119.12/119.53 inference(scs_inference,[],[4171,4146,3158,2924,403,228,47,2,31,60,81])).
% 119.12/119.53 cnf(4191,plain,
% 119.12/119.53 (~E(f10(a1,a1,a15),a17)),
% 119.12/119.53 inference(scs_inference,[],[3298,3958,2994,2,3])).
% 119.12/119.53 cnf(4244,plain,
% 119.12/119.53 (~E(f11(a16,f2(a16)),f9(a16,a1))),
% 119.12/119.53 inference(scs_inference,[],[3806,3777,2658,2,31])).
% 119.12/119.53 cnf(4246,plain,
% 119.12/119.53 (~P1(f18(x42461,f18(a15,x42462)),a16)),
% 119.12/119.53 inference(scs_inference,[],[3806,3777,2658,317,166,2,31,60])).
% 119.12/119.53 cnf(4253,plain,
% 119.12/119.53 (~E(f9(a16,a1),f11(a16,f2(a16)))),
% 119.12/119.53 inference(scs_inference,[],[4244,2])).
% 119.12/119.53 cnf(4310,plain,
% 119.12/119.53 (~P6(x43101,x43102,x43102)),
% 119.12/119.53 inference(rename_variables,[],[2673])).
% 119.12/119.53 cnf(4312,plain,
% 119.12/119.53 (~P4(f12(a1,a1,f4(a17,a1)),a1)),
% 119.12/119.53 inference(scs_inference,[],[4253,3437,2837,389,2673,4310,2623,2,3,84,90])).
% 119.12/119.53 cnf(4317,plain,
% 119.12/119.53 (~P5(f12(a1,a1,f4(a17,a1)),a16)),
% 119.12/119.53 inference(scs_inference,[],[4312,3974])).
% 119.12/119.53 cnf(4332,plain,
% 119.12/119.53 (~P5(f12(a1,a1,f3(a1)),a16)+P4(f12(a1,a1,f3(a1)),a1)),
% 119.12/119.53 inference(scs_inference,[],[3555,4317,3139,47,2,93,82])).
% 119.12/119.53 cnf(4337,plain,
% 119.12/119.53 (~E(f12(a16,a16,f4(a17,a16)),f5(a1,a16))),
% 119.12/119.53 inference(scs_inference,[],[3149,3158,3968,2,40])).
% 119.12/119.53 cnf(4347,plain,
% 119.12/119.53 (P2(f12(a1,a1,f4(a17,a1)),a1)),
% 119.12/119.53 inference(scs_inference,[],[4337,4312,2906,3047,2607,47,2,33,82,58])).
% 119.12/119.53 cnf(4372,plain,
% 119.12/119.53 (P5(f12(a16,a16,f10(a16,a1,a1)),a16)),
% 119.12/119.53 inference(scs_inference,[],[3774,98,2673,2,85])).
% 119.12/119.53 cnf(4377,plain,
% 119.12/119.53 (~E(f4(f4(a17,a16),a16),f12(a1,a1,a17))),
% 119.12/119.53 inference(scs_inference,[],[3774,3171,3009,2760,98,2673,2,85,58,33])).
% 119.12/119.53 cnf(4382,plain,
% 119.12/119.53 (~E(f12(a1,a1,f4(a17,a1)),f10(a16,a1,a1))),
% 119.12/119.53 inference(scs_inference,[],[4377,4347,110,2,35])).
% 119.12/119.53 cnf(4383,plain,
% 119.12/119.53 (~E(a17,f12(a1,a1,a17))),
% 119.12/119.53 inference(scs_inference,[],[4377,4347,110,3107,2,35,3])).
% 119.12/119.53 cnf(4391,plain,
% 119.12/119.53 (~E(f12(a1,a1,a17),a17)),
% 119.12/119.53 inference(scs_inference,[],[4383,2])).
% 119.12/119.53 cnf(4392,plain,
% 119.12/119.53 (~E(f10(a1,a1,a15),f4(f4(a17,a1),a1))),
% 119.12/119.53 inference(scs_inference,[],[4191,4383,2857,2,3])).
% 119.12/119.53 cnf(4395,plain,
% 119.12/119.53 (~E(f12(a1,a1,f4(a17,a1)),f10(a1,a1,a15))),
% 119.12/119.53 inference(scs_inference,[],[4191,4383,4372,4347,156,2857,47,2,3,82,35])).
% 119.12/119.53 cnf(4399,plain,
% 119.12/119.53 (P5(f12(a16,a16,f10(a16,a1,a1)),a15)),
% 119.12/119.53 inference(scs_inference,[],[45,4382,4372,2,60])).
% 119.12/119.53 cnf(4402,plain,
% 119.12/119.53 (P5(f12(f18(a1,x44021),f18(a1,x44021),f10(a16,a1,a16)),f18(a1,x44021))),
% 119.12/119.53 inference(scs_inference,[],[45,4382,4246,4372,2924,387,2673,2,60,31,84])).
% 119.12/119.53 cnf(4405,plain,
% 119.12/119.53 (~P5(f12(a16,a16,f10(a16,a1,a1)),a1)+P4(f12(a16,a16,f10(a16,a1,a1)),a16)),
% 119.12/119.53 inference(scs_inference,[],[45,4382,4246,4372,2924,387,2673,47,2,60,31,84,81])).
% 119.12/119.53 cnf(4415,plain,
% 119.12/119.53 (~E(f12(a1,a1,a17),f4(f4(a17,a1),a1))),
% 119.12/119.53 inference(scs_inference,[],[4391,4395,2857,2,3])).
% 119.12/119.53 cnf(4435,plain,
% 119.12/119.53 (~E(f12(f18(a16,a16),f18(a16,a16),f10(a16,a1,a1)),f12(a1,a1,a17))),
% 119.12/119.53 inference(scs_inference,[],[4392,3340,4040,2,40])).
% 119.12/119.53 cnf(4442,plain,
% 119.12/119.53 (~P4(f12(a16,a16,f4(a17,a16)),a16)),
% 119.12/119.53 inference(scs_inference,[],[4435,2793,2673,2,90])).
% 119.12/119.53 cnf(4445,plain,
% 119.12/119.53 (~E(x44451,f13(a1))+~E(f2(a16),x44451)),
% 119.12/119.53 inference(scs_inference,[],[3168,4435,2793,2673,2,90,3])).
% 119.12/119.53 cnf(4446,plain,
% 119.12/119.53 (~P5(f12(a16,a16,f4(a17,a16)),a1)),
% 119.12/119.53 inference(scs_inference,[],[4442,4186])).
% 119.12/119.53 cnf(4448,plain,
% 119.12/119.53 (P2(f12(a16,a16,f4(a17,a16)),a16)),
% 119.12/119.53 inference(scs_inference,[],[4415,4442,3158,2,58])).
% 119.12/119.53 cnf(4450,plain,
% 119.12/119.53 (~E(f7(a15,f12(a15,a15,a17)),f9(a16,a1))),
% 119.12/119.53 inference(scs_inference,[],[4415,4442,3222,3158,2670,2,58,31])).
% 119.12/119.53 cnf(4451,plain,
% 119.12/119.53 (~P4(x44511,f18(a1,a16))+~E(x44511,f2(f9(a16,a1)))),
% 119.12/119.53 inference(scs_inference,[],[4415,4442,2780,3222,3158,2670,2,58,31,33])).
% 119.12/119.53 cnf(4457,plain,
% 119.12/119.53 (~E(f9(a16,a1),f7(a15,f12(a15,a15,a17)))),
% 119.12/119.53 inference(scs_inference,[],[4450,2])).
% 119.12/119.53 cnf(4464,plain,
% 119.12/119.53 (~P5(f5(f18(a1,a16),a1),a1)),
% 119.12/119.53 inference(scs_inference,[],[4450,4446,3895,2,61,60,62,70])).
% 119.12/119.53 cnf(4468,plain,
% 119.12/119.53 (~E(f12(a16,a16,f4(a17,a16)),f3(a16))),
% 119.12/119.53 inference(scs_inference,[],[4450,4446,4448,3895,2712,2,61,60,62,70,59,35])).
% 119.12/119.53 cnf(4469,plain,
% 119.12/119.53 (P5(f5(f18(a1,a16),a1),a16)),
% 119.12/119.53 inference(scs_inference,[],[4450,4446,4448,3895,2712,2,61,60,62,70,59,35,93])).
% 119.12/119.53 cnf(4471,plain,
% 119.12/119.53 (~P5(f12(a16,a16,f3(a16)),a1)+P4(f12(a16,a16,f3(a16)),a16)),
% 119.12/119.53 inference(scs_inference,[],[47,4450,4446,4448,3895,2712,3095,2,61,60,62,70,59,35,93,81])).
% 119.12/119.53 cnf(4477,plain,
% 119.12/119.53 (~E(a1,f18(x44771,f9(a16,a1)))),
% 119.12/119.53 inference(scs_inference,[],[4468,3440,4446,2,61])).
% 119.12/119.53 cnf(4479,plain,
% 119.12/119.53 (~P1(f9(a16,a1),a1)),
% 119.12/119.53 inference(scs_inference,[],[4468,3440,4446,2,61,60])).
% 119.12/119.53 cnf(4481,plain,
% 119.12/119.53 (~E(a1,f18(f9(a16,a1),x44811))),
% 119.12/119.53 inference(scs_inference,[],[4468,3440,4446,2,61,60,62])).
% 119.12/119.53 cnf(4483,plain,
% 119.12/119.53 (~E(f9(a16,a1),f18(a1,a1))),
% 119.12/119.53 inference(scs_inference,[],[4468,3440,4446,2,61,60,62,65])).
% 119.12/119.53 cnf(4488,plain,
% 119.12/119.53 (~P5(f5(f9(a16,a1),a1),a1)),
% 119.12/119.53 inference(scs_inference,[],[4468,3440,4446,334,2673,2,61,60,62,65,85,70])).
% 119.12/119.53 cnf(4490,plain,
% 119.12/119.53 (P5(f5(f9(a16,a1),a1),f9(a16,a1))),
% 119.12/119.53 inference(scs_inference,[],[4468,3440,4446,334,2673,2,61,60,62,65,85,70,59])).
% 119.12/119.53 cnf(4497,plain,
% 119.12/119.53 (~P5(f5(f9(a16,a1),a1),f18(a1,a1))),
% 119.12/119.53 inference(scs_inference,[],[4483,4488,2,93])).
% 119.12/119.53 cnf(4505,plain,
% 119.12/119.53 (~P5(f5(a16,a1),a1)),
% 119.12/119.53 inference(scs_inference,[],[4483,4469,4464,4488,2,93,61,60,62,70])).
% 119.12/119.53 cnf(4507,plain,
% 119.12/119.53 (P5(f5(a16,a1),a16)),
% 119.12/119.53 inference(scs_inference,[],[4483,4469,4464,4488,2,93,61,60,62,70,59])).
% 119.12/119.53 cnf(4513,plain,
% 119.12/119.53 (~E(f5(f18(a1,a16),a16),f5(a16,a1))),
% 119.12/119.53 inference(scs_inference,[],[4505,3673,3959,2,40])).
% 119.12/119.53 cnf(4514,plain,
% 119.12/119.53 (~E(f18(a1,a1),f18(x45141,f9(a16,a1)))),
% 119.12/119.53 inference(scs_inference,[],[4505,4497,3673,4490,3959,2,40,61])).
% 119.12/119.53 cnf(4520,plain,
% 119.12/119.53 (P5(f12(a16,a16,f5(a16,a1)),a16)),
% 119.12/119.53 inference(scs_inference,[],[4507,4505,4497,3673,4490,3959,2673,2,40,61,60,62,84])).
% 119.12/119.53 cnf(4521,plain,
% 119.12/119.53 (~P6(x45211,x45212,x45212)),
% 119.12/119.53 inference(rename_variables,[],[2673])).
% 119.12/119.53 cnf(4523,plain,
% 119.12/119.53 (~P5(f5(f9(a16,a1),f18(a1,a1)),f18(a1,a1))),
% 119.12/119.53 inference(scs_inference,[],[4507,4505,4497,3673,4490,3959,2673,2,40,61,60,62,84,70])).
% 119.12/119.53 cnf(4525,plain,
% 119.12/119.53 (P5(f5(f9(a16,a1),f18(a1,a1)),f9(a16,a1))),
% 119.12/119.53 inference(scs_inference,[],[4507,4505,4497,3673,4490,3959,2673,2,40,61,60,62,84,70,59])).
% 119.12/119.53 cnf(4527,plain,
% 119.12/119.53 (~P5(f5(f9(a16,a1),f18(a1,a1)),a1)),
% 119.12/119.53 inference(scs_inference,[],[4507,4505,4497,3673,4490,3959,2673,2,40,61,60,62,84,70,59,92])).
% 119.12/119.53 cnf(4529,plain,
% 119.12/119.53 (~P5(f5(a16,a1),f18(a1,a1))),
% 119.12/119.53 inference(scs_inference,[],[4507,4505,4497,3673,4490,3959,2673,2,40,61,60,62,84,70,59,92,93])).
% 119.12/119.53 cnf(4533,plain,
% 119.12/119.53 (~P4(f12(a16,a16,f5(a16,a1)),a16)),
% 119.12/119.53 inference(scs_inference,[],[47,4507,4505,4497,3673,4490,3959,2876,2673,4521,2,40,61,60,62,84,70,59,92,93,81,90])).
% 119.12/119.53 cnf(4539,plain,
% 119.12/119.53 (~E(f3(a1),f10(a16,a1,a1))),
% 119.12/119.53 inference(scs_inference,[],[4513,2605,108,2,33])).
% 119.12/119.53 cnf(4540,plain,
% 119.12/119.53 (P5(f12(a16,a16,f5(a16,a1)),f9(a16,a1))),
% 119.12/119.53 inference(scs_inference,[],[4513,4520,2605,108,2623,2,33,61])).
% 119.12/119.53 cnf(4544,plain,
% 119.12/119.53 (~E(f18(a1,a1),f18(a16,x45441))),
% 119.12/119.53 inference(scs_inference,[],[4529,4513,4520,4507,2605,108,2623,2,33,61,60,62])).
% 119.12/119.53 cnf(4546,plain,
% 119.12/119.53 (~P5(f12(a16,a16,f5(a16,a1)),a1)),
% 119.12/119.53 inference(scs_inference,[],[47,4529,4513,4520,4533,4507,2605,108,2623,2,33,61,60,62,81])).
% 119.12/119.53 cnf(4548,plain,
% 119.12/119.53 (~P5(f5(a16,f18(a1,a1)),f18(a1,a1))),
% 119.12/119.53 inference(scs_inference,[],[47,4529,4513,4520,4533,4507,2605,108,2623,2,33,61,60,62,81,70])).
% 119.12/119.53 cnf(4550,plain,
% 119.12/119.53 (P5(f5(a16,f18(a1,a1)),a16)),
% 119.12/119.53 inference(scs_inference,[],[47,4529,4513,4520,4533,4507,2605,108,2623,2,33,61,60,62,81,70,59])).
% 119.12/119.53 cnf(4555,plain,
% 119.12/119.53 (P5(f5(f9(a16,a1),f18(a1,a1)),f18(a1,a16))),
% 119.12/119.53 inference(scs_inference,[],[47,4529,4525,4513,4520,4533,4448,311,4507,2605,108,2623,2,33,61,60,62,81,70,59,92,35,41])).
% 119.12/119.53 cnf(4560,plain,
% 119.12/119.53 (~E(f10(a16,a1,a1),f3(a1))),
% 119.12/119.53 inference(scs_inference,[],[4539,2])).
% 119.12/119.53 cnf(4567,plain,
% 119.12/119.53 (~E(f7(a1,f12(a1,a1,a17)),f9(a16,a1))),
% 119.12/119.53 inference(scs_inference,[],[4479,4539,4555,4548,4550,4546,4523,2769,2,93,61,60,31])).
% 119.12/119.53 cnf(4591,plain,
% 119.12/119.53 (~E(f9(a16,a1),f7(a1,f12(a1,a1,a17)))),
% 119.12/119.53 inference(scs_inference,[],[4567,2])).
% 119.12/119.53 cnf(4592,plain,
% 119.12/119.53 (~E(f18(a1,a16),f7(a15,f12(a15,a15,a17)))),
% 119.12/119.53 inference(scs_inference,[],[4567,4457,2623,2,3])).
% 119.12/119.53 cnf(4595,plain,
% 119.12/119.53 (~P5(f12(a16,a16,a17),a1)+P4(f12(a16,a16,a17),a16)),
% 119.12/119.53 inference(scs_inference,[],[47,4567,4457,4527,4555,2753,2623,2,3,93,81])).
% 119.12/119.53 cnf(4597,plain,
% 119.12/119.53 (P2(f12(a16,a16,f5(a16,a1)),a16)),
% 119.12/119.53 inference(scs_inference,[],[47,4567,4457,4527,4533,4520,4555,2753,2623,2,3,93,81,58])).
% 119.12/119.53 cnf(4602,plain,
% 119.12/119.53 (~E(f12(a16,a16,f5(a16,a1)),f3(a16))),
% 119.12/119.53 inference(scs_inference,[],[4514,4597,2712,2,35])).
% 119.12/119.53 cnf(4603,plain,
% 119.12/119.53 (~P4(f12(a16,a16,a17),a16)),
% 119.12/119.53 inference(scs_inference,[],[4514,4597,2712,2642,2673,2,35,90])).
% 119.12/119.53 cnf(4606,plain,
% 119.12/119.53 (~P5(f12(a16,a16,a17),a1)),
% 119.12/119.53 inference(scs_inference,[],[4514,4597,2712,2642,2673,2,35,90,4595])).
% 119.12/119.53 cnf(4607,plain,
% 119.12/119.53 (P1(f11(a16,f12(a16,a16,a17)),a16)),
% 119.12/119.53 inference(scs_inference,[],[4514,4597,2712,2642,2673,2,35,90,4595,4012])).
% 119.12/119.53 cnf(4608,plain,
% 119.12/119.53 (P1(f7(a16,f12(a16,a16,a17)),a16)),
% 119.12/119.53 inference(scs_inference,[],[4514,4597,2712,2642,2753,2673,2,35,90,4595,4012,68])).
% 119.12/119.53 cnf(4610,plain,
% 119.12/119.53 (P5(f12(a16,a16,a17),f7(a16,f12(a16,a16,a17)))),
% 119.12/119.53 inference(scs_inference,[],[4514,4597,2712,2642,2753,2673,2,35,90,4595,4012,68,66])).
% 119.12/119.53 cnf(4612,plain,
% 119.12/119.53 (P5(f12(a16,a16,a17),f11(a16,f12(a16,a16,a17)))),
% 119.12/119.53 inference(scs_inference,[],[4514,4597,2712,2642,2753,2673,2,35,90,4595,4012,68,66,67])).
% 119.12/119.53 cnf(4619,plain,
% 119.12/119.53 (~E(f4(f3(a16),a16),f12(a16,a16,a17))),
% 119.12/119.53 inference(scs_inference,[],[4603,4602,2902,2,33])).
% 119.12/119.53 cnf(4621,plain,
% 119.12/119.53 (~E(f5(a1,f18(a16,a16)),f12(a16,a16,a17))),
% 119.12/119.53 inference(scs_inference,[],[4603,4606,4602,4612,3940,2902,2,33,41,40])).
% 119.12/119.53 cnf(4624,plain,
% 119.12/119.53 (~E(f11(a16,f12(a16,a16,a17)),f18(a1,a1))),
% 119.12/119.53 inference(scs_inference,[],[4603,4606,4602,4612,3940,2902,2,33,41,40,60,65])).
% 119.12/119.53 cnf(4635,plain,
% 119.12/119.53 (~E(f7(a16,f12(a16,a16,a17)),f18(a1,a1))),
% 119.12/119.53 inference(scs_inference,[],[4619,4610,4540,4606,2623,2,41,60,65])).
% 119.12/119.53 cnf(4643,plain,
% 119.12/119.53 (P5(f8(f18(a1,a1),f18(a16,x46431)),f18(a16,x46431))+~E(f18(a16,x46431),f18(x46432,f18(a1,a1)))),
% 119.12/119.53 inference(scs_inference,[],[4544,4619,4610,4540,4606,2623,2,41,60,65,71,76,93,61])).
% 119.12/119.53 cnf(4648,plain,
% 119.12/119.53 (P5(f8(f18(a1,a1),f18(a16,f18(a1,a1))),f18(a16,f18(a1,a1)))),
% 119.12/119.53 inference(equality_inference,[],[4643])).
% 119.12/119.53 cnf(4650,plain,
% 119.12/119.53 (~E(f7(a16,f12(a16,a16,a17)),a1)),
% 119.12/119.53 inference(scs_inference,[],[4621,4610,4606,2,41])).
% 119.12/119.53 cnf(4651,plain,
% 119.12/119.53 (~P5(f5(a16,a1),f18(f18(a1,a1),f18(a1,a1)))),
% 119.12/119.53 inference(scs_inference,[],[4621,4610,4529,4606,2,41,93])).
% 119.12/119.53 cnf(4653,plain,
% 119.12/119.53 (~E(f11(a1,f12(a1,a1,a17)),f9(a16,a1))),
% 119.12/119.53 inference(scs_inference,[],[4621,4479,2797,4610,4529,4606,2,41,93,31])).
% 119.12/119.53 cnf(4664,plain,
% 119.12/119.53 (P2(f12(a16,a16,a17),a16)),
% 119.12/119.53 inference(scs_inference,[],[4560,4635,4603,136,2753,2673,2,85,3,58])).
% 119.12/119.53 cnf(4666,plain,
% 119.12/119.53 (~E(f12(a16,a16,f5(a16,a1)),f10(a16,a1,a16))),
% 119.12/119.53 inference(scs_inference,[],[4560,4635,4603,4597,311,136,2753,2673,2,85,3,58,35])).
% 119.12/119.53 cnf(4669,plain,
% 119.12/119.53 (~E(f9(a16,a1),f11(a1,f12(a1,a1,a17)))),
% 119.12/119.53 inference(scs_inference,[],[4653,2])).
% 119.12/119.53 cnf(4681,plain,
% 119.12/119.53 (~P5(f12(a16,a16,a17),f18(a1,a1))),
% 119.12/119.53 inference(scs_inference,[],[4624,4606,2,93])).
% 119.12/119.53 cnf(4684,plain,
% 119.12/119.53 (~P1(f11(a16,f12(a16,a16,a17)),f18(a1,a1))),
% 119.12/119.53 inference(scs_inference,[],[4624,3218,4612,4606,2,93,33,60])).
% 119.12/119.53 cnf(4689,plain,
% 119.12/119.53 (~E(x46891,f2(a16))+~E(x46891,f13(a1))),
% 119.12/119.53 inference(scs_inference,[],[4445,2])).
% 119.12/119.53 cnf(4691,plain,
% 119.12/119.53 (~E(f12(f18(a1,a1),f18(a1,a1),f10(a16,a1,a16)),f12(a16,a16,a17))),
% 119.12/119.53 inference(scs_inference,[],[4681,4666,4402,2,40])).
% 119.12/119.53 cnf(4701,plain,
% 119.12/119.53 (P5(f8(a16,f18(x47011,a1)),f18(x47011,a1))+~E(f18(x47011,a1),f18(a16,x47012))),
% 119.12/119.53 inference(scs_inference,[],[4681,3703,4666,4402,4610,2,40,60,71,76,61,62])).
% 119.12/119.53 cnf(4704,plain,
% 119.12/119.53 (P5(f8(a16,f18(a16,a1)),f18(a16,a1))),
% 119.12/119.53 inference(equality_inference,[],[4701])).
% 119.12/119.53 cnf(4706,plain,
% 119.12/119.54 (~E(f12(a16,a16,a17),f3(a16))),
% 119.12/119.54 inference(scs_inference,[],[4691,4664,2712,2,35])).
% 119.12/119.54 cnf(4710,plain,
% 119.12/119.54 (P5(f8(a16,f18(a16,a1)),a1)),
% 119.12/119.54 inference(scs_inference,[],[4691,4704,4664,3703,2712,2,35,76,93])).
% 119.12/119.54 cnf(4712,plain,
% 119.12/119.54 (~P1(f18(a16,a1),a16)),
% 119.12/119.54 inference(scs_inference,[],[4691,4704,4664,3703,2712,2,35,76,93,60])).
% 119.12/119.54 cnf(4714,plain,
% 119.12/119.54 (~P5(f5(f18(a16,a1),a16),a16)),
% 119.12/119.54 inference(scs_inference,[],[4691,4704,4664,3703,2712,2,35,76,93,60,70])).
% 119.12/119.54 cnf(4716,plain,
% 119.12/119.54 (P5(f5(f18(a16,a1),a16),f18(a16,a1))),
% 119.12/119.54 inference(scs_inference,[],[4691,4704,4664,3703,2712,2,35,76,93,60,70,59])).
% 119.12/119.54 cnf(4738,plain,
% 119.12/119.54 (~E(f3(a16),f12(a16,a16,a17))),
% 119.12/119.54 inference(scs_inference,[],[4706,2])).
% 119.12/119.54 cnf(4739,plain,
% 119.12/119.54 (P5(f5(f18(a16,a1),a16),a1)),
% 119.12/119.54 inference(scs_inference,[],[4706,4716,4714,2,93])).
% 119.12/119.54 cnf(4741,plain,
% 119.12/119.54 (~E(f11(a16,f12(a16,a16,a17)),f18(a16,a1))),
% 119.12/119.54 inference(scs_inference,[],[4706,4712,4716,4607,4714,2,93,31])).
% 119.12/119.54 cnf(4766,plain,
% 119.12/119.54 (~E(f12(a16,a16,a17),f10(a16,a1,a16))),
% 119.12/119.54 inference(scs_inference,[],[4738,4741,4664,311,2,76,35])).
% 119.12/119.54 cnf(4772,plain,
% 119.12/119.54 (~P4(x47721,f4(f4(a17,a16),a16))+~E(x47721,f2(a17))),
% 119.12/119.54 inference(scs_inference,[],[4766,3028,2,33])).
% 119.12/119.54 cnf(4795,plain,
% 119.12/119.54 (~E(f13(a1),f5(a16,a1))),
% 119.12/119.54 inference(scs_inference,[],[4592,4651,1247,2,40])).
% 119.12/119.54 cnf(4802,plain,
% 119.12/119.54 (~E(f18(a1,a16),f7(a1,f12(a1,a1,a17)))),
% 119.12/119.54 inference(scs_inference,[],[4795,4591,2623,2,3])).
% 119.12/119.54 cnf(4803,plain,
% 119.12/119.54 (~P5(f12(a16,a16,a17),f18(f18(a1,a1),f18(a1,a1)))),
% 119.12/119.54 inference(scs_inference,[],[4795,4591,4681,2623,2,3,93])).
% 119.12/119.54 cnf(4815,plain,
% 119.12/119.54 (~E(f11(a16,f12(a16,a16,a17)),f18(x48151,a15))),
% 119.12/119.54 inference(scs_inference,[],[4802,4607,4083,2,31])).
% 119.12/119.54 cnf(4825,plain,
% 119.12/119.54 (~E(f4(f4(a17,a16),a16),f12(a16,a16,a17))),
% 119.12/119.54 inference(scs_inference,[],[4815,4603,2941,2,33])).
% 119.12/119.54 cnf(4826,plain,
% 119.12/119.54 (P5(f12(f18(a1,x48261),f18(a1,x48261),f13(a1)),f18(a1,x48261))),
% 119.12/119.54 inference(scs_inference,[],[4815,4603,2941,1243,2673,2,33,84])).
% 119.12/119.54 cnf(4847,plain,
% 119.12/119.54 (~E(f7(a16,f12(a16,a16,a17)),f18(a16,a1))),
% 119.12/119.54 inference(scs_inference,[],[4825,4608,4712,2,31])).
% 119.12/119.54 cnf(4848,plain,
% 119.12/119.54 (~E(a17,f12(a16,a16,a17))),
% 119.12/119.54 inference(scs_inference,[],[4825,4608,4712,3107,2,31,3])).
% 119.12/119.54 cnf(4855,plain,
% 119.12/119.54 (~E(f18(a1,a16),f11(a1,f12(a1,a1,a17)))),
% 119.12/119.54 inference(scs_inference,[],[4848,4669,2623,2,3])).
% 119.12/119.54 cnf(4862,plain,
% 119.12/119.54 (~E(f11(a16,f12(a16,a16,a17)),a15)),
% 119.12/119.54 inference(scs_inference,[],[4847,4607,3653,2,31])).
% 119.12/119.54 cnf(4863,plain,
% 119.12/119.54 (~E(f13(a1),f12(a16,a16,a17))),
% 119.12/119.54 inference(scs_inference,[],[4847,4803,4607,3653,1249,2,31,40])).
% 119.12/119.54 cnf(4869,plain,
% 119.12/119.54 (~E(f12(a16,a16,a17),f13(a1))),
% 119.12/119.54 inference(scs_inference,[],[4863,2])).
% 119.12/119.54 cnf(4875,plain,
% 119.12/119.54 (~E(f3(a16),f10(a16,a1,a16))),
% 119.12/119.54 inference(scs_inference,[],[4869,4855,2704,315,2,3,33])).
% 119.12/119.54 cnf(4879,plain,
% 119.12/119.54 (~E(f7(a16,f12(a16,a16,a17)),f18(x48791,a15))),
% 119.12/119.54 inference(scs_inference,[],[4875,4608,4083,2,31])).
% 119.12/119.54 cnf(4880,plain,
% 119.12/119.54 (~P4(f12(a16,a16,f13(a16)),a16)),
% 119.12/119.54 inference(scs_inference,[],[4875,4608,4083,2726,2673,2,31,90])).
% 119.12/119.54 cnf(4892,plain,
% 119.12/119.54 (~E(f11(a16,f12(a16,a16,a17)),f9(a16,a1))),
% 119.12/119.54 inference(scs_inference,[],[96,4879,4607,3777,251,106,2,61,60,31])).
% 119.12/119.54 cnf(4893,plain,
% 119.12/119.54 (P2(f12(a16,a16,f13(a16)),a16)),
% 119.12/119.54 inference(scs_inference,[],[96,4879,4880,4607,2818,3777,251,106,2,61,60,31,58])).
% 119.12/119.54 cnf(4899,plain,
% 119.12/119.54 (~E(f9(a16,a1),f11(a16,f12(a16,a16,a17)))),
% 119.12/119.54 inference(scs_inference,[],[4892,2])).
% 119.12/119.54 cnf(4900,plain,
% 119.12/119.54 (~E(f12(a16,a16,f13(a16)),f3(a16))),
% 119.12/119.54 inference(scs_inference,[],[4892,4893,2712,2,35])).
% 119.12/119.54 cnf(4908,plain,
% 119.12/119.54 (~E(f5(f18(a16,a1),a16),f10(a16,a1,a1))),
% 119.12/119.54 inference(scs_inference,[],[96,4900,4739,2,40])).
% 119.12/119.54 cnf(4913,plain,
% 119.12/119.54 (~E(f4(a17,a16),f12(a16,a16,f4(a17,a16)))),
% 119.12/119.54 inference(scs_inference,[],[4908,4442,2716,2,33])).
% 119.12/119.54 cnf(4914,plain,
% 119.12/119.54 (P5(f12(a1,a1,f10(a16,a1,a16)),a1)),
% 119.12/119.54 inference(scs_inference,[],[4908,4442,2716,174,2673,2,33,85])).
% 119.12/119.54 cnf(4923,plain,
% 119.12/119.54 (P5(f12(a15,a15,f10(a16,a1,a16)),a15)),
% 119.12/119.54 inference(scs_inference,[],[4913,179,2673,2,84])).
% 119.12/119.54 cnf(4926,plain,
% 119.12/119.54 (~E(f7(a16,f12(a16,a16,a17)),a15)),
% 119.12/119.54 inference(scs_inference,[],[4913,4608,3653,179,2673,2,84,31])).
% 119.12/119.54 cnf(4946,plain,
% 119.12/119.54 (P5(f12(a15,a15,f10(a16,a1,a16)),x49461)+~E(x49461,f18(a15,x49462))),
% 119.12/119.54 inference(scs_inference,[],[4650,4923,2,62])).
% 119.12/119.54 cnf(4950,plain,
% 119.12/119.54 (P5(f12(a15,a15,f10(a16,a1,a16)),f18(a15,x49501))),
% 119.12/119.54 inference(equality_inference,[],[4946])).
% 119.12/119.54 cnf(4985,plain,
% 119.12/119.54 (~E(f18(a1,a16),f11(a16,f12(a16,a16,a17)))),
% 119.12/119.54 inference(scs_inference,[],[4899,4862,2623,2,3])).
% 119.12/119.54 cnf(4988,plain,
% 119.12/119.54 (P5(f12(a1,a1,f10(a16,a1,a16)),f9(a16,a1))),
% 119.12/119.54 inference(scs_inference,[],[4899,4862,4950,4914,2623,2,3,60,62])).
% 119.12/119.54 cnf(4993,plain,
% 119.12/119.54 (~E(f7(a16,f12(a16,a16,a17)),f9(a16,a1))),
% 119.12/119.54 inference(scs_inference,[],[4985,4608,3777,2,31])).
% 119.12/119.54 cnf(4994,plain,
% 119.12/119.54 (P5(f12(a1,a1,f10(a16,a1,a16)),f18(a1,a16))),
% 119.12/119.54 inference(scs_inference,[],[4988,4985,4608,3777,2623,2,31,41])).
% 119.12/119.54 cnf(4995,plain,
% 119.12/119.54 (~P4(f12(a16,a16,f10(a16,a1,a1)),a16)),
% 119.12/119.54 inference(scs_inference,[],[98,4988,4985,4608,3777,2673,2623,2,31,41,90])).
% 119.12/119.54 cnf(4998,plain,
% 119.12/119.54 (P2(f12(a16,a16,f10(a16,a1,a1)),a16)),
% 119.12/119.54 inference(scs_inference,[],[98,4988,4985,4608,3777,4372,2673,2623,2,31,41,90,58])).
% 119.12/119.54 cnf(5002,plain,
% 119.12/119.54 (~P5(f12(a16,a16,f10(a16,a1,a1)),a1)),
% 119.12/119.54 inference(scs_inference,[],[98,4988,4985,4608,2793,3777,4372,2673,47,2623,2,31,41,90,58,82,4405])).
% 119.12/119.54 cnf(5003,plain,
% 119.12/119.54 (~P1(a15,a1)),
% 119.12/119.54 inference(scs_inference,[],[98,4988,4985,4399,4608,2793,3777,4372,2673,47,2623,2,31,41,90,58,82,4405,60])).
% 119.12/119.54 cnf(5011,plain,
% 119.12/119.54 (~P5(f5(a15,a1),a1)),
% 119.12/119.54 inference(scs_inference,[],[5003,70])).
% 119.12/119.54 cnf(5013,plain,
% 119.12/119.54 (~E(f9(a16,a1),f7(a16,f12(a16,a16,a17)))),
% 119.12/119.54 inference(scs_inference,[],[5003,4993,70,2])).
% 119.12/119.54 cnf(5019,plain,
% 119.12/119.54 (~P6(x50191,x50192,x50192)),
% 119.12/119.54 inference(rename_variables,[],[2673])).
% 119.12/119.54 cnf(5030,plain,
% 119.12/119.54 (P5(f12(a1,a1,f10(a16,a1,a16)),x50301)+~E(x50301,f18(f18(a1,a16),x50302))),
% 119.12/119.54 inference(scs_inference,[],[5003,4993,4994,5002,4998,4399,3065,2712,2673,5019,70,2,59,61,84,90,60,35,93,4471,62])).
% 119.12/119.54 cnf(5111,plain,
% 119.12/119.54 (~P5(f5(a15,a1),f18(a1,a1))),
% 119.12/119.54 inference(scs_inference,[],[4995,2744,5011,2702,2,33,93])).
% 119.12/119.54 cnf(5113,plain,
% 119.12/119.54 (~E(f10(a16,a1,a1),f5(f18(x51131,a15),a16))),
% 119.12/119.54 inference(scs_inference,[],[98,4995,2744,4088,5011,2702,2,33,93,40])).
% 119.12/119.54 cnf(5120,plain,
% 119.12/119.54 (~E(f18(a1,a16),f7(a16,f12(a16,a16,a17)))),
% 119.12/119.54 inference(scs_inference,[],[5013,5113,2623,2,3])).
% 119.12/119.54 cnf(5126,plain,
% 119.12/119.54 (~E(f11(a1,f12(a1,a1,a17)),a15)),
% 119.12/119.54 inference(scs_inference,[],[5120,2797,5003,2,31])).
% 119.12/119.54 cnf(5195,plain,
% 119.12/119.54 (~E(f12(f18(a1,a1),f18(a1,a1),f13(a1)),f5(a15,a1))),
% 119.12/119.54 inference(scs_inference,[],[2841,4826,5111,2,40])).
% 119.12/119.54 cnf(5208,plain,
% 119.12/119.54 (~E(f4(f4(a17,a16),a16),f10(a16,a1,a1))),
% 119.12/119.54 inference(scs_inference,[],[5195,3009,108,2,33])).
% 119.12/119.54 cnf(5214,plain,
% 119.12/119.54 (~E(f10(a16,a1,a1),f4(f4(a17,a16),a16))),
% 119.12/119.54 inference(scs_inference,[],[5208,2])).
% 119.12/119.54 cnf(5230,plain,
% 119.12/119.54 (P5(f12(a1,a1,f3(a1)),x52301)+~E(x52301,f18(a15,x52302))),
% 119.12/119.54 inference(scs_inference,[],[3622,3399,2,62])).
% 119.12/119.54 cnf(5234,plain,
% 119.12/119.54 (P5(f12(a1,a1,f3(a1)),f18(a15,x52341))),
% 119.12/119.54 inference(equality_inference,[],[5230])).
% 119.12/119.54 cnf(5236,plain,
% 119.12/119.54 (~E(f8(a16,f18(a16,a1)),f5(a15,a1))),
% 119.12/119.54 inference(scs_inference,[],[3624,4710,5011,2,40])).
% 119.12/119.54 cnf(5243,plain,
% 119.12/119.54 (~P1(f18(a15,x52431),x52432)+P5(f12(a1,a1,f3(a1)),x52432)),
% 119.12/119.54 inference(scs_inference,[],[5236,5234,5214,2994,2,3,60])).
% 119.12/119.54 cnf(5252,plain,
% 119.12/119.54 (~P5(f12(a1,a1,f3(a1)),a16)),
% 119.12/119.54 inference(scs_inference,[],[3972,2733,2673,2,90,4332])).
% 119.12/119.54 cnf(5253,plain,
% 119.12/119.54 (~P5(f12(a1,a1,f3(a1)),f18(a16,a16))),
% 119.12/119.54 inference(scs_inference,[],[3972,2733,2673,2,90,4332,93])).
% 119.12/119.54 cnf(5257,plain,
% 119.12/119.54 (P2(f12(a1,a1,f3(a1)),a1)),
% 119.12/119.54 inference(scs_inference,[],[3972,2999,3139,2733,2673,47,2,90,4332,93,81,58])).
% 119.12/119.54 cnf(5265,plain,
% 119.12/119.54 (P5(f5(f18(a15,x52651),f18(a16,a16)),f18(a15,x52651))),
% 119.12/119.54 inference(scs_inference,[],[5253,5243,70,59])).
% 119.12/119.54 cnf(5267,plain,
% 119.12/119.54 (~P5(f5(f18(a15,x52671),f18(a16,a16)),a16)),
% 119.12/119.54 inference(scs_inference,[],[5253,5243,70,59,92])).
% 119.12/119.54 cnf(5270,plain,
% 119.12/119.54 (~P1(f18(a15,x52701),a16)),
% 119.12/119.54 inference(scs_inference,[],[5253,4477,5243,70,59,92,2,60])).
% 119.12/119.54 cnf(5274,plain,
% 119.12/119.54 (~E(f11(a16,f12(a16,a16,a17)),f18(a15,x52741))),
% 119.12/119.54 inference(scs_inference,[],[5253,4477,4607,5243,70,59,92,2,60,62,31])).
% 119.12/119.54 cnf(5277,plain,
% 119.12/119.54 (~E(f12(a1,a1,f3(a1)),f3(a1))),
% 119.12/119.54 inference(scs_inference,[],[5253,4477,5257,5234,4607,2611,5243,70,59,92,2,60,62,31,61,35])).
% 119.12/119.54 cnf(5278,plain,
% 119.12/119.54 (P5(f5(f9(a16,a1),a15),a1)+P5(f5(f9(a16,a1),a15),a16)),
% 119.12/119.54 inference(scs_inference,[],[5253,4477,5257,2801,5234,4607,2611,5243,70,59,92,2,60,62,31,61,35,93])).
% 119.12/119.54 cnf(5290,plain,
% 119.12/119.54 (~P5(f5(f18(a15,x52901),a16),f18(a16,a16))),
% 119.12/119.54 inference(scs_inference,[],[5270,5274,5252,5234,70,59,2,62,93])).
% 119.12/119.54 cnf(5301,plain,
% 119.12/119.54 (P5(f4(f4(a17,a1),a1),x53011)+~E(x53011,f18(a15,x53012))),
% 119.12/119.54 inference(scs_inference,[],[5265,5277,5267,3435,2,93,62])).
% 119.12/119.54 cnf(5307,plain,
% 119.12/119.54 (P5(f4(f4(a17,a1),a1),f18(a15,x53071))),
% 119.12/119.54 inference(equality_inference,[],[5301])).
% 119.12/119.54 cnf(5309,plain,
% 119.12/119.54 (~P1(f18(x53091,a16),f18(a1,a1))),
% 119.12/119.54 inference(scs_inference,[],[104,4481,117,2,60])).
% 119.12/119.54 cnf(5314,plain,
% 119.12/119.54 (~E(f10(a16,a1,a1),f5(f18(a15,x53141),a16))),
% 119.12/119.54 inference(scs_inference,[],[104,4481,5290,144,117,2,60,62,41,40])).
% 119.12/119.54 cnf(5315,plain,
% 119.12/119.54 (P5(f10(a16,a1,a1),f18(x53151,a16))),
% 119.12/119.54 inference(rename_variables,[],[104])).
% 119.12/119.54 cnf(5320,plain,
% 119.12/119.54 (P5(f5(f18(a16,a16),f18(a1,a1)),f18(a16,a16))),
% 119.12/119.54 inference(scs_inference,[],[104,5315,4481,5290,144,117,2,60,62,41,40,61,70,59])).
% 119.12/119.54 cnf(5322,plain,
% 119.12/119.54 (~P5(f5(f18(a16,a16),f18(a1,a1)),a1)),
% 119.12/119.54 inference(scs_inference,[],[104,5315,4481,5290,144,117,2,60,62,41,40,61,70,59,92])).
% 119.12/119.54 cnf(5331,plain,
% 119.12/119.54 (~P5(f5(f18(x53311,a16),f18(a1,a1)),f18(a1,a1))),
% 119.12/119.54 inference(scs_inference,[],[5309,5314,2,70])).
% 119.12/119.54 cnf(5333,plain,
% 119.12/119.54 (P5(f5(f18(x53331,a16),f18(a1,a1)),f18(x53331,a16))),
% 119.12/119.54 inference(scs_inference,[],[5309,5314,2,70,59])).
% 119.12/119.54 cnf(5335,plain,
% 119.12/119.54 (~P5(f5(f18(x53351,a16),f18(a1,a1)),a1)),
% 119.12/119.54 inference(scs_inference,[],[5309,5314,2,70,59,92])).
% 119.12/119.54 cnf(5341,plain,
% 119.12/119.54 (~P6(x53411,x53412,x53412)),
% 119.12/119.54 inference(rename_variables,[],[2673])).
% 119.12/119.54 cnf(5343,plain,
% 119.12/119.54 (~P4(f12(f18(x53431,a16),f18(x53431,a16),f10(a16,a1,a1)),f18(x53431,a16))),
% 119.12/119.54 inference(scs_inference,[],[104,5309,5320,5314,5307,2857,2673,5341,2,70,59,92,93,40,85,90])).
% 119.12/119.54 cnf(5355,plain,
% 119.12/119.54 (~E(f12(a1,a1,f3(a1)),f10(a16,a1,a1))),
% 119.12/119.54 inference(scs_inference,[],[104,5309,5320,5314,5322,5307,5257,4174,5270,2658,110,2857,2673,5341,2,70,59,92,93,40,85,90,60,62,58,31,35])).
% 119.12/119.54 cnf(5363,plain,
% 119.12/119.54 (~P4(f12(f18(a1,a16),f18(a1,a16),f10(a16,a1,a1)),f9(a16,a1))),
% 119.12/119.54 inference(scs_inference,[],[5355,5343,5333,5335,2623,2,60,34])).
% 119.12/119.54 cnf(5390,plain,
% 119.12/119.54 (~P5(f12(a16,a16,a17),f18(a1,a16))+P5(f12(f9(a16,a1),f18(a1,a16),f12(a16,a16,a17)),f9(a16,a1))),
% 119.12/119.54 inference(scs_inference,[],[4926,2948,2741,2,84])).
% 119.12/119.54 cnf(5397,plain,
% 119.12/119.54 (P2(f12(f18(x53971,a16),f18(x53971,a16),f10(a16,a1,a1)),f18(x53971,a16))),
% 119.12/119.54 inference(scs_inference,[],[5126,5343,4100,2,58])).
% 119.12/119.54 cnf(5402,plain,
% 119.12/119.54 (~E(f12(a1,a1,f3(a1)),f10(a1,a1,a15))),
% 119.12/119.54 inference(scs_inference,[],[5126,5343,5257,4100,4712,2656,156,2,58,31,35])).
% 119.12/119.54 cnf(5423,plain,
% 119.12/119.54 (~E(f10(a16,a1,a1),f5(f18(a1,a16),a16))),
% 119.12/119.54 inference(scs_inference,[],[104,5402,3931,2,40])).
% 119.12/119.54 cnf(5425,plain,
% 119.12/119.54 (P5(f4(f3(a16),a16),x54251)+~E(x54251,f18(f18(a1,a16),x54252))),
% 119.12/119.54 inference(scs_inference,[],[104,5402,3615,3931,2,40,62])).
% 119.12/119.54 cnf(5429,plain,
% 119.12/119.54 (P5(f4(f3(a16),a16),f18(f18(a1,a16),x54291))),
% 119.12/119.54 inference(equality_inference,[],[5425])).
% 119.12/119.54 cnf(5431,plain,
% 119.12/119.54 (E(f2(f18(f14(f2(x54311),x54311),f6(f2(x54311),x54311))),f2(x54311))),
% 119.12/119.54 inference(rename_variables,[],[1163])).
% 119.12/119.54 cnf(5433,plain,
% 119.12/119.54 (E(f2(f18(f14(f2(x54331),x54331),f6(f2(x54331),x54331))),f2(x54331))),
% 119.12/119.54 inference(rename_variables,[],[1163])).
% 119.12/119.54 cnf(5441,plain,
% 119.12/119.54 (E(f9(f6(f2(x54411),x54411),f14(f2(x54411),x54411)),f18(f14(f2(x54411),x54411),f6(f2(x54411),x54411)))),
% 119.12/119.54 inference(scs_inference,[],[2625,2675,2645,1163,5431,5433,4689,4451,4772,5030,4120,7,75])).
% 119.12/119.54 cnf(5452,plain,
% 119.12/119.54 (E(f11(f2(f9(a16,a1)),x54521),f11(f2(f18(a1,a16)),x54521))),
% 119.12/119.54 inference(scs_inference,[],[2625,2675,2645,1163,5431,5433,4689,4451,4772,5030,4120,7,75,26,22,29,24,8,11,16,25,27,21])).
% 119.12/119.54 cnf(5469,plain,
% 119.12/119.54 (P4(f13(f11(x54691,f2(x54691))),f11(x54691,f2(x54691)))),
% 119.12/119.54 inference(scs_inference,[],[5423,2625,2675,2645,1163,5431,5433,3698,2902,4689,4451,4772,5030,4120,7,75,26,22,29,24,8,11,16,25,27,21,15,13,2,4,30,12,9,63,23,28,10,20,14,17,19,51])).
% 119.12/119.54 cnf(5472,plain,
% 119.12/119.54 (P6(f12(f18(x54721,a16),f18(x54721,a16),f10(a16,a1,a1)),f14(f12(f18(x54721,a16),f18(x54721,a16),f10(a16,a1,a1)),f18(x54721,a16)),f6(f12(f18(x54721,a16),f18(x54721,a16),f10(a16,a1,a1)),f18(x54721,a16)))),
% 119.12/119.54 inference(scs_inference,[],[5423,2625,2675,2645,1163,5431,5433,5397,3698,2902,4689,4451,4772,5030,4120,7,75,26,22,29,24,8,11,16,25,27,21,15,13,2,4,30,12,9,63,23,28,10,20,14,17,19,51,18,77])).
% 119.12/119.54 cnf(5498,plain,
% 119.12/119.54 (~P1(f11(f18(a1,a16),f12(f9(a16,a1),f9(a16,a1),f12(a1,a1,a17))),f7(f18(a1,a16),f12(f9(a16,a1),f9(a16,a1),f12(a1,a1,a17))))),
% 119.12/119.54 inference(scs_inference,[],[4684,5423,2625,2675,2645,1163,5431,5433,5397,3220,3218,3698,4803,4612,2902,4689,4451,4772,5030,4120,7,75,26,22,29,24,8,11,16,25,27,21,15,13,2,4,30,12,9,63,23,28,10,20,14,17,19,51,18,77,70,637,72,6,59,74,5,73,57,92,62,60,78,79])).
% 119.12/119.54 cnf(5502,plain,
% 119.12/119.54 (E(f11(f9(a16,a1),x55021),f11(f18(a1,a16),x55021))),
% 119.12/119.54 inference(rename_variables,[],[2683])).
% 119.12/119.54 cnf(5504,plain,
% 119.12/119.54 (E(f11(f9(a16,a1),x55041),f11(f18(a1,a16),x55041))),
% 119.12/119.54 inference(rename_variables,[],[2683])).
% 119.12/119.54 cnf(5506,plain,
% 119.12/119.54 (P2(f12(f18(a1,a16),f18(a1,a16),f12(a1,a1,a17)),f18(a1,a16))),
% 119.12/119.54 inference(scs_inference,[],[4684,5423,2625,2662,2675,2683,5502,2646,2645,1163,5431,5433,5397,3220,3204,3218,3698,4803,4612,2902,4689,4451,4772,5030,4120,7,75,26,22,29,24,8,11,16,25,27,21,15,13,2,4,30,12,9,63,23,28,10,20,14,17,19,51,18,77,70,637,72,6,59,74,5,73,57,92,62,60,78,79,43,31,35])).
% 119.12/119.54 cnf(5507,plain,
% 119.12/119.54 (E(f12(f9(a16,a1),f9(a16,a1),x55071),f12(f18(a1,a16),f18(a1,a16),x55071))),
% 119.12/119.54 inference(rename_variables,[],[2646])).
% 119.12/119.54 cnf(5509,plain,
% 119.12/119.54 (P1(f11(f18(a1,a16),f12(f9(a16,a1),f9(a16,a1),f12(a1,a1,a17))),f18(a1,a16))),
% 119.12/119.54 inference(scs_inference,[],[4684,5423,2625,2662,2675,2683,5502,2646,2645,1163,5431,5433,5397,3220,3204,3218,3698,4803,4612,2902,4689,4451,4772,5030,4120,7,75,26,22,29,24,8,11,16,25,27,21,15,13,2,4,30,12,9,63,23,28,10,20,14,17,19,51,18,77,70,637,72,6,59,74,5,73,57,92,62,60,78,79,43,31,35,41,69])).
% 119.12/119.54 cnf(5528,plain,
% 119.12/119.54 (E(f12(f9(a16,a1),f9(a16,a1),x55281),f12(f18(a1,a16),f18(a1,a16),x55281))),
% 119.12/119.54 inference(rename_variables,[],[2646])).
% 119.12/119.54 cnf(5541,plain,
% 119.12/119.54 (P5(f2(x55411),x55411)),
% 119.12/119.54 inference(rename_variables,[],[2634])).
% 119.12/119.54 cnf(5546,plain,
% 119.12/119.54 (P5(f12(f18(f18(a1,a16),x55461),f18(f18(a1,a16),x55461),f4(f3(a16),a16)),f18(f18(a1,a16),x55461))),
% 119.12/119.54 inference(scs_inference,[],[104,4684,5363,5423,2625,2660,2662,2675,5429,2683,5502,5504,2646,5507,5528,2645,4115,4648,1163,5431,5433,5397,5331,3220,3204,2664,2883,5333,2971,3218,3698,4803,4544,5343,4612,2902,2632,2634,144,3107,2673,4689,4451,4772,5030,4120,7,75,26,22,29,24,8,11,16,25,27,21,15,13,2,4,30,12,9,63,23,28,10,20,14,17,19,51,18,77,70,637,72,6,59,74,5,73,57,92,62,60,78,79,43,31,35,41,69,3,38,76,67,66,68,34,39,33,32,93,40,61,81,65,84])).
% 119.12/119.54 cnf(5547,plain,
% 119.12/119.54 (~P6(x55471,x55472,x55472)),
% 119.12/119.54 inference(rename_variables,[],[2673])).
% 119.12/119.54 cnf(5553,plain,
% 119.12/119.54 (~P4(f12(f18(f18(a1,a16),x55531),f18(f18(a1,a16),x55531),f4(f3(a16),a16)),f18(f18(a1,a16),x55531))),
% 119.12/119.54 inference(scs_inference,[],[104,4684,5363,5423,2625,2660,2662,2675,5429,2683,5502,5504,2646,5507,5528,2645,4115,4648,1163,5431,5433,5397,3258,5331,3220,3204,2664,3017,2883,5333,2971,3218,3698,4803,4544,5343,4612,2902,2632,2634,5541,144,3107,2673,5547,4689,4451,4772,5030,4120,7,75,26,22,29,24,8,11,16,25,27,21,15,13,2,4,30,12,9,63,23,28,10,20,14,17,19,51,18,77,70,637,72,6,59,74,5,73,57,92,62,60,78,79,43,31,35,41,69,3,38,76,67,66,68,34,39,33,32,93,40,61,81,65,84,85,90])).
% 119.12/119.54 cnf(5623,plain,
% 119.12/119.54 (~P6(x56231,x56232,x56232)),
% 119.12/119.54 inference(rename_variables,[],[2673])).
% 119.12/119.54 cnf(5638,plain,
% 119.12/119.54 (P5(f5(f9(a16,a1),a15),a16)),
% 119.12/119.54 inference(scs_inference,[],[44,2623,2673,5623,108,117,2857,98,174,3336,1243,2753,2881,2758,2700,2799,4446,2760,2750,2782,2658,2625,2668,2722,2834,2786,5397,2826,2662,2650,3671,245,5506,73,5,74,6,56,2,528,538,55,91,92,1099,54,5390,739,549,559,570,367,382,3942,3686,61,40,36,93,32,33,39,38,3,41,35,60,62,82,81,5278])).
% 119.12/119.54 cnf(5684,plain,
% 119.12/119.54 (E(f11(f9(a16,a1),x56841),f11(f18(a1,a16),x56841))),
% 119.12/119.54 inference(rename_variables,[],[2683])).
% 119.12/119.54 cnf(5687,plain,
% 119.12/119.54 (~P6(x56871,x56872,x56872)),
% 119.12/119.54 inference(rename_variables,[],[2673])).
% 119.12/119.54 cnf(5701,plain,
% 119.12/119.54 ($false),
% 119.12/119.54 inference(scs_inference,[],[45,2623,2673,5687,2675,2857,144,2881,2700,4606,2634,2950,315,3658,2625,2658,2722,2716,2645,5397,2788,1163,2683,5684,3753,5441,5452,5546,5638,5553,5509,5498,5469,5472,73,5,74,56,2,528,55,91,92,1099,3686,3942,3767,54,125,61,40,36,93,32,34,33,39,38,3,41,37,31,58,60]),
% 119.12/119.54 ['proof']).
% 119.12/119.54 % SZS output end Proof
% 119.12/119.54 % Total time :118.410000s
%------------------------------------------------------------------------------