%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : GEO094-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 : n026.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Mon Jun 24 06:03:46 EDT 2024
% Result : Unsatisfiable 117.06s 117.65s
% Output : CNFRefutation 117.16s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.08/0.13 % Problem : GEO094-1 : TPTP v8.2.0. Released v2.4.0.
% 0.08/0.13 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% 0.13/0.35 % Computer : n026.cluster.edu
% 0.13/0.35 % Model : x86_64 x86_64
% 0.13/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.35 % Memory : 8042.1875MB
% 0.13/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.35 % CPULimit : 300
% 0.13/0.35 % WCLimit : 300
% 0.13/0.35 % DateTime : Fri Jun 21 07:16:39 EDT 2024
% 0.13/0.35 % CPUTime :
% 0.22/0.60 start to proof:theBenchmark
% 117.06/117.63 %-------------------------------------------
% 117.06/117.63 % File :CSE---1.7
% 117.06/117.63 % Problem :theBenchmark
% 117.06/117.63 % Transform :cnf
% 117.06/117.63 % Format :tptp:raw
% 117.06/117.64 % Command :java -jar mcs_scs.jar %d %s
% 117.06/117.64
% 117.06/117.64 % Result :Theorem 116.380000s
% 117.06/117.64 % Output :CNFRefutation 116.380000s
% 117.06/117.64 %-------------------------------------------
% 117.06/117.65 %--------------------------------------------------------------------------
% 117.06/117.65 % File : GEO094-1 : TPTP v8.2.0. Released v2.4.0.
% 117.06/117.65 % Domain : Geometry (Oriented curves)
% 117.06/117.65 % Problem : Meeting point is not an endpoint of contianing curve
% 117.06/117.65 % Version : [EHK99] axioms.
% 117.06/117.65 % English : A meeting point of two curves is not an endpoint of any curve
% 117.06/117.65 % that includes both as sub-curves.
% 117.06/117.65
% 117.06/117.65 % Refs : [KE99] Kulik & Eschenbach (1999), A Geometry of Oriented Curv
% 117.06/117.65 % : [EHK99] Eschenbach et al. (1999), Representing Simple Trajecto
% 117.06/117.65 % Source : [TPTP]
% 117.06/117.65 % Names :
% 117.06/117.65
% 117.06/117.65 % Status : Unsatisfiable
% 117.06/117.65 % Rating : 0.15 v8.2.0, 0.19 v8.1.0, 0.11 v7.4.0, 0.18 v7.3.0, 0.17 v7.1.0, 0.08 v7.0.0, 0.13 v6.3.0, 0.09 v6.2.0, 0.20 v6.1.0, 0.21 v6.0.0, 0.20 v5.5.0, 0.40 v5.3.0, 0.39 v5.2.0, 0.31 v5.1.0, 0.41 v5.0.0, 0.36 v4.1.0, 0.23 v4.0.1, 0.36 v4.0.0, 0.18 v3.7.0, 0.10 v3.5.0, 0.09 v3.4.0, 0.08 v3.3.0, 0.21 v3.2.0, 0.23 v3.1.0, 0.09 v2.7.0, 0.17 v2.6.0, 0.00 v2.5.0, 0.22 v2.4.0
% 117.06/117.65 % Syntax : Number of clauses : 52 ( 5 unt; 21 nHn; 47 RR)
% 117.06/117.65 % Number of literals : 158 ( 21 equ; 78 neg)
% 117.06/117.65 % Maximal clause size : 12 ( 3 avg)
% 117.06/117.65 % Maximal term depth : 3 ( 1 avg)
% 117.06/117.65 % Number of predicates : 8 ( 7 usr; 0 prp; 1-3 aty)
% 117.06/117.65 % Number of functors : 18 ( 18 usr; 4 con; 0-3 aty)
% 117.06/117.65 % Number of variables : 126 ( 10 sgn)
% 117.06/117.65 % SPC : CNF_UNS_RFO_SEQ_NHN
% 117.06/117.65
% 117.06/117.65 % Comments : Created by tptp2X -f tptp -t clausify:otter GEO094+1.p
% 117.06/117.65 %--------------------------------------------------------------------------
% 117.06/117.65 %----Include simple curve axioms
% 117.06/117.65 include('Axioms/GEO004-0.ax').
% 117.06/117.65 %--------------------------------------------------------------------------
% 117.06/117.65 cnf(proposition_2_14_3_67,negated_conjecture,
% 117.06/117.65 meet(sk17,sk15,sk16) ).
% 117.06/117.65
% 117.06/117.65 cnf(proposition_2_14_3_68,negated_conjecture,
% 117.06/117.65 part_of(sk15,sk14) ).
% 117.06/117.65
% 117.06/117.65 cnf(proposition_2_14_3_69,negated_conjecture,
% 117.06/117.65 part_of(sk16,sk14) ).
% 117.06/117.65
% 117.06/117.65 cnf(proposition_2_14_3_70,negated_conjecture,
% 117.06/117.65 end_point(sk17,sk14) ).
% 117.06/117.65
% 117.06/117.65 %--------------------------------------------------------------------------
% 117.06/117.65 %-------------------------------------------
% 117.06/117.65 % Proof found
% 117.06/117.65 % SZS status Theorem for theBenchmark
% 117.06/117.65 % SZS output start Proof
% 117.06/117.66 %ClaNum:90(EqnAxiom:43)
% 117.06/117.66 %VarNum:331(SingletonVarNum:113)
% 117.06/117.66 %MaxLitNum:12
% 117.06/117.66 %MaxfuncDepth:2
% 117.06/117.66 %SharedTerms:8
% 117.06/117.66 %goalClause: 44 45 46 48
% 117.06/117.66 %singleGoalClaCount:4
% 117.06/117.66 [44]P1(a1,a2)
% 117.06/117.66 [45]P1(a16,a2)
% 117.06/117.66 [46]P2(a17,a2)
% 117.06/117.66 [48]P6(a17,a1,a16)
% 117.06/117.66 [47]P4(f3(x471),x471)
% 117.06/117.66 [49]P3(x491)+P2(f4(x491),x491)
% 117.06/117.66 [51]~P7(x511)+P2(f14(x511),x511)
% 117.06/117.66 [50]P7(x501)+~P2(x502,x501)
% 117.06/117.66 [53]~P3(x531)+~P2(x532,x531)
% 117.06/117.66 [54]~P2(x541,x542)+P5(x541,x542)
% 117.06/117.66 [55]~P4(x551,x552)+P5(x551,x552)
% 117.06/117.66 [56]~P4(x561,x562)+~P2(x561,x562)
% 117.06/117.66 [57]~P2(x571,x572)+~E(f5(x571,x572),x571)
% 117.06/117.66 [59]P1(x591,x592)+P5(f6(x591,x592),x591)
% 117.06/117.66 [63]~P2(x631,x632)+P2(f5(x631,x632),x632)
% 117.06/117.66 [70]P1(x701,x702)+~P5(f6(x701,x702),x702)
% 117.06/117.66 [77]~P4(x771,x772)+P6(x771,f15(x771,x772),f7(x771,x772))
% 117.06/117.66 [72]~P4(x721,x722)+E(f18(f15(x721,x722),f7(x721,x722)),x722)
% 117.06/117.66 [73]P5(x731,x732)+~P6(x731,x733,x732)
% 117.06/117.66 [74]P5(x741,x742)+~P6(x741,x742,x743)
% 117.06/117.66 [75]~P6(x753,x752,x751)+E(f10(x751,x752),f18(x752,x751))
% 117.06/117.66 [52]P7(x521)+~P1(x521,x522)+E(x521,x522)
% 117.06/117.66 [58]P4(x581,x582)+~P5(x581,x582)+P2(x581,x582)
% 117.06/117.66 [66]~P5(x661,x662)+P2(x661,x662)+P5(x661,f8(x662,x661))
% 117.06/117.66 [67]~P5(x671,x672)+P2(x671,x672)+P5(x671,f12(x672,x671))
% 117.06/117.66 [68]~P5(x681,x682)+P2(x681,x682)+P1(f8(x682,x681),x682)
% 117.06/117.66 [69]~P5(x691,x692)+P2(x691,x692)+P1(f12(x692,x691),x692)
% 117.06/117.66 [71]E(x711,x712)+P5(f9(x711,x712),x712)+P5(f9(x711,x712),x711)
% 117.06/117.66 [76]E(x761,x762)+~P5(f9(x761,x762),x762)+~P5(f9(x761,x762),x761)
% 117.06/117.66 [78]~P5(x781,x782)+P2(x781,x782)+~P1(f8(x782,x781),f12(x782,x781))
% 117.06/117.66 [79]~P5(x791,x792)+P2(x791,x792)+~P1(f12(x792,x791),f8(x792,x791))
% 117.06/117.66 [60]~P5(x601,x603)+P5(x601,x602)+~P1(x603,x602)
% 117.06/117.66 [88]~P5(f11(x883,x882,x881),x881)+~P5(f11(x883,x882,x881),x882)+E(x881,f18(x882,x883))
% 117.06/117.66 [89]~P5(f11(x893,x892,x891),x891)+~P5(f11(x893,x892,x891),x893)+E(x891,f18(x892,x893))
% 117.06/117.66 [61]~P5(x611,x614)+P5(x611,x612)+~E(x612,f18(x613,x614))
% 117.06/117.66 [62]~P5(x621,x623)+P5(x621,x622)+~E(x622,f18(x623,x624))
% 117.06/117.66 [84]~P5(x841,x843)+~P5(x841,x842)+P6(x841,x842,x843)+P5(f13(x843,x842,x841),x843)
% 117.06/117.66 [85]~P5(x851,x853)+~P5(x851,x852)+P6(x851,x852,x853)+P5(f13(x853,x852,x851),x852)
% 117.06/117.66 [87]P5(f11(x873,x872,x871),x871)+P5(f11(x873,x872,x871),x872)+P5(f11(x873,x872,x871),x873)+E(x871,f18(x872,x873))
% 117.06/117.66 [81]~P5(x811,x812)+P2(x811,x812)+~P6(x814,x813,x812)+~P5(x811,x813)
% 117.06/117.66 [82]~P5(x821,x822)+P2(x821,x822)+~P6(x824,x822,x823)+~P5(x821,x823)
% 117.06/117.66 [65]~P5(x651,x654)+P5(x651,x652)+P5(x651,x653)+~E(x654,f18(x653,x652))
% 117.06/117.66 [90]~P5(x901,x903)+~P5(x901,x902)+P6(x901,x902,x903)+~P2(f13(x903,x902,x901),x903)+~P2(f13(x903,x902,x901),x902)
% 117.06/117.66 [83]~P3(x834)+~P2(x831,x832)+P6(x831,x832,x833)+~P6(x835,x832,x833)+~E(x834,f18(x832,x833))
% 117.06/117.66 [64]E(x643,x641)+~P2(x641,x644)+~P2(x643,x644)+E(x641,x642)+E(x643,x642)+~P2(x642,x644)
% 117.06/117.66 [80]P1(x802,x801)+~P1(x802,x803)+~P5(x804,x802)+~P2(x804,x803)+P1(x801,x802)+~P1(x801,x803)+~P5(x804,x801)
% 117.06/117.66 [86]P1(x862,x861)+P1(x862,x863)+P1(x863,x861)+P1(x863,x862)+~P1(x862,x864)+~P1(x863,x864)+~P2(x865,x862)+~P2(x865,x863)+P1(x861,x862)+P1(x861,x863)+~P1(x861,x864)+~P2(x865,x861)
% 117.06/117.66 %EqnAxiom
% 117.06/117.66 [1]E(x11,x11)
% 117.06/117.66 [2]E(x22,x21)+~E(x21,x22)
% 117.06/117.66 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 117.06/117.66 [4]~E(x41,x42)+E(f3(x41),f3(x42))
% 117.06/117.66 [5]~E(x51,x52)+E(f4(x51),f4(x52))
% 117.06/117.66 [6]~E(x61,x62)+E(f14(x61),f14(x62))
% 117.06/117.66 [7]~E(x71,x72)+E(f5(x71,x73),f5(x72,x73))
% 117.06/117.66 [8]~E(x81,x82)+E(f5(x83,x81),f5(x83,x82))
% 117.06/117.66 [9]~E(x91,x92)+E(f6(x91,x93),f6(x92,x93))
% 117.06/117.66 [10]~E(x101,x102)+E(f6(x103,x101),f6(x103,x102))
% 117.06/117.66 [11]~E(x111,x112)+E(f18(x111,x113),f18(x112,x113))
% 117.06/117.66 [12]~E(x121,x122)+E(f18(x123,x121),f18(x123,x122))
% 117.06/117.66 [13]~E(x131,x132)+E(f11(x131,x133,x134),f11(x132,x133,x134))
% 117.06/117.66 [14]~E(x141,x142)+E(f11(x143,x141,x144),f11(x143,x142,x144))
% 117.06/117.66 [15]~E(x151,x152)+E(f11(x153,x154,x151),f11(x153,x154,x152))
% 117.06/117.66 [16]~E(x161,x162)+E(f13(x161,x163,x164),f13(x162,x163,x164))
% 117.06/117.66 [17]~E(x171,x172)+E(f13(x173,x171,x174),f13(x173,x172,x174))
% 117.06/117.66 [18]~E(x181,x182)+E(f13(x183,x184,x181),f13(x183,x184,x182))
% 117.06/117.66 [19]~E(x191,x192)+E(f12(x191,x193),f12(x192,x193))
% 117.06/117.66 [20]~E(x201,x202)+E(f12(x203,x201),f12(x203,x202))
% 117.06/117.66 [21]~E(x211,x212)+E(f8(x211,x213),f8(x212,x213))
% 117.06/117.66 [22]~E(x221,x222)+E(f8(x223,x221),f8(x223,x222))
% 117.06/117.66 [23]~E(x231,x232)+E(f7(x231,x233),f7(x232,x233))
% 117.06/117.66 [24]~E(x241,x242)+E(f7(x243,x241),f7(x243,x242))
% 117.06/117.66 [25]~E(x251,x252)+E(f9(x251,x253),f9(x252,x253))
% 117.06/117.66 [26]~E(x261,x262)+E(f9(x263,x261),f9(x263,x262))
% 117.06/117.66 [27]~E(x271,x272)+E(f15(x271,x273),f15(x272,x273))
% 117.06/117.66 [28]~E(x281,x282)+E(f15(x283,x281),f15(x283,x282))
% 117.06/117.66 [29]~E(x291,x292)+E(f10(x291,x293),f10(x292,x293))
% 117.06/117.66 [30]~E(x301,x302)+E(f10(x303,x301),f10(x303,x302))
% 117.06/117.66 [31]P1(x312,x313)+~E(x311,x312)+~P1(x311,x313)
% 117.06/117.66 [32]P1(x323,x322)+~E(x321,x322)+~P1(x323,x321)
% 117.06/117.66 [33]P2(x332,x333)+~E(x331,x332)+~P2(x331,x333)
% 117.06/117.66 [34]P2(x343,x342)+~E(x341,x342)+~P2(x343,x341)
% 117.06/117.66 [35]P5(x352,x353)+~E(x351,x352)+~P5(x351,x353)
% 117.06/117.66 [36]P5(x363,x362)+~E(x361,x362)+~P5(x363,x361)
% 117.06/117.66 [37]P4(x372,x373)+~E(x371,x372)+~P4(x371,x373)
% 117.06/117.66 [38]P4(x383,x382)+~E(x381,x382)+~P4(x383,x381)
% 117.06/117.66 [39]P6(x392,x393,x394)+~E(x391,x392)+~P6(x391,x393,x394)
% 117.06/117.66 [40]P6(x403,x402,x404)+~E(x401,x402)+~P6(x403,x401,x404)
% 117.06/117.66 [41]P6(x413,x414,x412)+~E(x411,x412)+~P6(x413,x414,x411)
% 117.06/117.66 [42]~P3(x421)+P3(x422)+~E(x421,x422)
% 117.06/117.66 [43]~P7(x431)+P7(x432)+~E(x431,x432)
% 117.06/117.66
% 117.06/117.66 %-------------------------------------------
% 117.06/117.67 cnf(91,plain,
% 117.06/117.67 (~P5(x911,x912)+P5(x911,f18(x913,x912))),
% 117.06/117.67 inference(equality_inference,[],[61])).
% 117.06/117.67 cnf(92,plain,
% 117.06/117.67 (~P5(x921,x922)+P5(x921,f18(x922,x923))),
% 117.06/117.67 inference(equality_inference,[],[62])).
% 117.06/117.67 cnf(93,plain,
% 117.06/117.67 (~P5(x931,f18(x932,x933))+P5(x931,x933)+P5(x931,x932)),
% 117.06/117.67 inference(equality_inference,[],[65])).
% 117.06/117.67 cnf(94,plain,
% 117.06/117.67 (~P3(f18(x941,x942))+P6(x943,x941,x942)+~P2(x943,x941)+~P6(x944,x941,x942)),
% 117.06/117.67 inference(equality_inference,[],[83])).
% 117.06/117.67 cnf(95,plain,
% 117.06/117.67 (~P4(a17,a2)),
% 117.06/117.67 inference(scs_inference,[],[46,56])).
% 117.06/117.67 cnf(97,plain,
% 117.06/117.68 (~E(f3(a2),a17)),
% 117.06/117.68 inference(scs_inference,[],[46,47,56,37])).
% 117.06/117.68 cnf(101,plain,
% 117.06/117.68 (~P5(x1011,a1)+P5(x1011,a2)),
% 117.06/117.68 inference(scs_inference,[],[44,46,47,56,37,52,60])).
% 117.06/117.68 cnf(105,plain,
% 117.06/117.68 (~P5(x1051,f18(a1,a1))+P5(x1051,a2)),
% 117.06/117.68 inference(scs_inference,[],[44,46,47,56,37,52,60,31,32,93])).
% 117.06/117.68 cnf(111,plain,
% 117.06/117.68 (P4(f3(x1111),x1112)+~E(x1111,x1112)),
% 117.06/117.68 inference(scs_inference,[],[47,38])).
% 117.06/117.68 cnf(112,plain,
% 117.06/117.68 (~E(f3(x1121),a17)+~E(x1121,a2)),
% 117.06/117.68 inference(scs_inference,[],[95,47,38,37])).
% 117.06/117.68 cnf(124,plain,
% 117.06/117.68 (P6(x1241,a1,a16)+~E(a17,x1241)),
% 117.06/117.68 inference(scs_inference,[],[46,45,48,31,41,34,39])).
% 117.06/117.68 cnf(125,plain,
% 117.06/117.68 (~P5(x1251,a16)+P5(x1251,a2)),
% 117.06/117.68 inference(scs_inference,[],[46,45,48,31,41,34,39,60])).
% 117.06/117.68 cnf(140,plain,
% 117.06/117.68 (P1(a1,a1)+~P5(a17,a1)),
% 117.06/117.68 inference(scs_inference,[],[44,46,94,80])).
% 117.06/117.68 cnf(151,plain,
% 117.06/117.68 (P2(f14(a2),a2)),
% 117.06/117.68 inference(scs_inference,[],[46,50,51])).
% 117.06/117.68 cnf(155,plain,
% 117.06/117.68 (P2(x1551,a2)+~E(f14(a2),x1551)),
% 117.06/117.68 inference(scs_inference,[],[151,56,34,33])).
% 117.06/117.68 cnf(179,plain,
% 117.06/117.68 (P2(f4(a2),a2)),
% 117.06/117.68 inference(scs_inference,[],[46,53,49])).
% 117.06/117.68 cnf(180,plain,
% 117.06/117.68 (~P4(f4(a2),a2)),
% 117.06/117.68 inference(scs_inference,[],[179,56])).
% 117.06/117.68 cnf(183,plain,
% 117.06/117.68 (P2(x1831,a2)+~E(f4(a2),x1831)),
% 117.06/117.68 inference(scs_inference,[],[179,56,34,33])).
% 117.06/117.68 cnf(223,plain,
% 117.06/117.68 (P5(a17,f18(x2231,a2))),
% 117.06/117.68 inference(scs_inference,[],[46,54,91])).
% 117.06/117.68 cnf(224,plain,
% 117.06/117.68 (P5(a17,f18(x2241,f18(x2242,a2)))),
% 117.06/117.68 inference(scs_inference,[],[223,91])).
% 117.06/117.68 cnf(226,plain,
% 117.06/117.68 (P5(a17,f18(f18(x2261,a2),x2262))),
% 117.06/117.68 inference(scs_inference,[],[223,91,92])).
% 117.06/117.68 cnf(283,plain,
% 117.06/117.68 (P5(x2831,f18(f18(x2832,a2),x2833))+~E(a17,x2831)),
% 117.06/117.68 inference(scs_inference,[],[226,35])).
% 117.06/117.68 cnf(287,plain,
% 117.06/117.68 (P5(x2871,f18(x2872,f18(x2873,a2)))+~E(a17,x2871)),
% 117.06/117.68 inference(scs_inference,[],[224,35])).
% 117.06/117.68 cnf(297,plain,
% 117.06/117.68 (P5(f3(x2971),f18(x2971,x2972))),
% 117.06/117.68 inference(scs_inference,[],[47,55,92])).
% 117.06/117.68 cnf(317,plain,
% 117.06/117.68 (P5(f3(x3171),x3172)+~E(f18(x3171,x3173),x3172)),
% 117.06/117.68 inference(scs_inference,[],[297,36])).
% 117.06/117.68 cnf(337,plain,
% 117.06/117.68 (P5(x3371,f18(x3372,x3373))+~E(f3(x3372),x3371)),
% 117.06/117.68 inference(scs_inference,[],[297,35])).
% 117.06/117.68 cnf(338,plain,
% 117.06/117.68 (P1(x3381,f18(x3382,x3383))+~E(f3(x3382),f6(x3381,f18(x3382,x3383)))),
% 117.06/117.68 inference(scs_inference,[],[297,35,70])).
% 117.06/117.68 cnf(394,plain,
% 117.06/117.68 (P1(a16,a16)+~P5(a17,a16)),
% 117.06/117.68 inference(scs_inference,[],[45,46,94,80])).
% 117.06/117.68 cnf(406,plain,
% 117.06/117.68 (P1(x4061,a16)+~E(a16,x4061)+~P5(a17,a16)),
% 117.06/117.68 inference(scs_inference,[],[394,31])).
% 117.06/117.68 cnf(423,plain,
% 117.06/117.68 (P5(a17,f18(x4231,a16))),
% 117.06/117.68 inference(scs_inference,[],[48,73,91])).
% 117.06/117.68 cnf(424,plain,
% 117.06/117.68 (P5(a17,f18(x4241,f18(x4242,a16)))),
% 117.06/117.68 inference(scs_inference,[],[423,91])).
% 117.06/117.68 cnf(426,plain,
% 117.06/117.68 (P5(a17,f18(f18(x4261,a16),x4262))),
% 117.06/117.68 inference(scs_inference,[],[423,91,92])).
% 117.06/117.68 cnf(441,plain,
% 117.06/117.68 (P5(x4411,f18(x4412,a16))+~E(a17,x4411)),
% 117.06/117.68 inference(scs_inference,[],[423,35])).
% 117.06/117.68 cnf(442,plain,
% 117.06/117.68 (P1(x4421,f18(x4422,a16))+~E(a17,f6(x4421,f18(x4422,a16)))),
% 117.06/117.68 inference(scs_inference,[],[423,35,70])).
% 117.06/117.68 cnf(463,plain,
% 117.06/117.68 (P5(x4631,f18(x4632,f18(x4633,a16)))+~E(a17,x4631)),
% 117.06/117.68 inference(scs_inference,[],[424,35])).
% 117.06/117.68 cnf(473,plain,
% 117.06/117.68 (P5(x4731,f18(f18(x4732,a16),x4733))+~E(a17,x4731)),
% 117.06/117.68 inference(scs_inference,[],[426,35])).
% 117.06/117.68 cnf(484,plain,
% 117.06/117.68 (P1(a1,a1)),
% 117.06/117.68 inference(scs_inference,[],[48,74,140])).
% 117.06/117.68 cnf(486,plain,
% 117.06/117.68 (P1(x4861,a1)+~E(a1,x4861)),
% 117.06/117.68 inference(scs_inference,[],[484,32,31])).
% 117.06/117.68 cnf(587,plain,
% 117.06/117.68 (E(f3(f10(a16,a1)),f3(f18(a1,a16)))),
% 117.06/117.68 inference(scs_inference,[],[48,4,75])).
% 117.06/117.68 cnf(654,plain,
% 117.06/117.68 (~E(f5(f5(a17,a2),a2),f5(a17,a2))),
% 117.06/117.68 inference(scs_inference,[],[46,57,63])).
% 117.06/117.68 cnf(655,plain,
% 117.06/117.68 (~E(f5(a17,a2),a17)),
% 117.06/117.68 inference(scs_inference,[],[654,7])).
% 117.06/117.68 cnf(675,plain,
% 117.06/117.68 (P5(f3(f18(a1,a1)),a2)),
% 117.06/117.68 inference(scs_inference,[],[47,105,55])).
% 117.06/117.68 cnf(676,plain,
% 117.06/117.68 (P5(f3(f18(a1,a1)),f18(a2,x6761))),
% 117.06/117.68 inference(scs_inference,[],[675,92])).
% 117.06/117.68 cnf(678,plain,
% 117.06/117.68 (P5(f3(f18(a1,a1)),f18(x6781,a2))),
% 117.06/117.68 inference(scs_inference,[],[675,92,91])).
% 117.06/117.68 cnf(681,plain,
% 117.06/117.68 (P1(x6811,a2)+~E(f3(f18(a1,a1)),f6(x6811,a2))),
% 117.06/117.68 inference(scs_inference,[],[675,92,91,35,70])).
% 117.06/117.68 cnf(1500,plain,
% 117.06/117.68 (~E(f6(x15001,a2),f3(f18(a1,a1)))+P1(x15001,a2)),
% 117.06/117.68 inference(scs_inference,[],[681,2])).
% 117.06/117.68 cnf(1676,plain,
% 117.06/117.68 (~E(x16761,f3(f18(a1,a1)))+~E(f6(x16762,a2),x16761)+P1(x16762,a2)),
% 117.06/117.68 inference(scs_inference,[],[1500,3])).
% 117.06/117.68 cnf(2267,plain,
% 117.06/117.68 (~E(f6(x22671,f18(x22672,x22673)),f3(x22672))+P1(x22671,f18(x22672,x22673))),
% 117.06/117.68 inference(scs_inference,[],[338,2])).
% 117.06/117.68 cnf(3860,plain,
% 117.06/117.68 (P7(a1)+P1(a2,a1)),
% 117.06/117.68 inference(scs_inference,[],[44,48,52,40,31,486])).
% 117.06/117.68 cnf(3867,plain,
% 117.06/117.68 (P2(a17,a1)+P7(a1)),
% 117.06/117.68 inference(scs_inference,[],[44,48,46,675,180,587,52,40,31,486,111,112,2,60,58,37,36,42,43,34])).
% 117.06/117.68 cnf(3869,plain,
% 117.06/117.68 (E(a16,a2)+P7(a16)),
% 117.06/117.68 inference(scs_inference,[],[45,52])).
% 117.06/117.68 cnf(3873,plain,
% 117.06/117.68 (P7(a16)+~E(f3(a16),a17)),
% 117.06/117.68 inference(scs_inference,[],[45,52,31,111,112])).
% 117.06/117.68 cnf(3919,plain,
% 117.06/117.68 (P2(f14(a1),a1)+P1(a2,a1)),
% 117.06/117.68 inference(scs_inference,[],[3860,51])).
% 117.06/117.68 cnf(3933,plain,
% 117.06/117.68 (~P2(f3(x39331),x39331)),
% 117.06/117.68 inference(scs_inference,[],[47,56])).
% 117.06/117.68 cnf(3935,plain,
% 117.06/117.68 (~E(a17,f3(a2))),
% 117.06/117.68 inference(scs_inference,[],[46,47,56,33])).
% 117.06/117.68 cnf(3968,plain,
% 117.06/117.68 (~P2(f3(x39681),x39681)),
% 117.06/117.68 inference(rename_variables,[],[3933])).
% 117.06/117.68 cnf(3970,plain,
% 117.06/117.68 (~P2(f3(x39701),x39701)),
% 117.06/117.68 inference(rename_variables,[],[3933])).
% 117.06/117.68 cnf(3971,plain,
% 117.06/117.68 (~P5(f3(f18(a1,a1)),f18(a1,a1))+~P6(x39711,f18(a1,a1),a2)),
% 117.06/117.68 inference(scs_inference,[],[675,3933,3968,3970,155,183,82])).
% 117.06/117.68 cnf(4001,plain,
% 117.06/117.68 (~P5(f3(f18(a1,a1)),f18(a1,a1))+~P6(x40011,a2,f18(a1,a1))),
% 117.06/117.68 inference(scs_inference,[],[675,3933,81])).
% 117.06/117.68 cnf(4045,plain,
% 117.06/117.68 (P7(a1)),
% 117.06/117.68 inference(scs_inference,[],[3867,50])).
% 117.06/117.68 cnf(4073,plain,
% 117.06/117.68 (~E(a17,f5(a17,a2))),
% 117.06/117.68 inference(scs_inference,[],[654,2,7])).
% 117.06/117.68 cnf(4086,plain,
% 117.06/117.68 (P5(a17,a2)),
% 117.06/117.68 inference(scs_inference,[],[46,54])).
% 117.06/117.68 cnf(4088,plain,
% 117.06/117.68 (P5(a17,f18(a2,x40881))),
% 117.06/117.68 inference(scs_inference,[],[46,54,92])).
% 117.06/117.68 cnf(4090,plain,
% 117.06/117.68 (P5(a17,f18(x40901,f18(a2,x40902)))),
% 117.06/117.68 inference(scs_inference,[],[46,54,92,91])).
% 117.06/117.68 cnf(4098,plain,
% 117.06/117.68 (P5(f4(a2),a2)),
% 117.06/117.68 inference(scs_inference,[],[179,54])).
% 117.06/117.68 cnf(4100,plain,
% 117.06/117.68 (P5(a17,f18(f18(a2,x41001),x41002))),
% 117.06/117.68 inference(scs_inference,[],[179,4088,54,92])).
% 117.06/117.68 cnf(4102,plain,
% 117.06/117.68 (P5(f4(a2),f18(x41021,a2))),
% 117.06/117.68 inference(scs_inference,[],[179,4088,54,92,91])).
% 117.06/117.68 cnf(4104,plain,
% 117.06/117.68 (~E(x41041,a17)+~E(f3(a2),x41041)),
% 117.06/117.68 inference(scs_inference,[],[179,97,4088,54,92,91,3])).
% 117.06/117.68 cnf(4108,plain,
% 117.06/117.68 (P5(f4(a2),f18(a2,x41081))),
% 117.06/117.68 inference(scs_inference,[],[4098,92])).
% 117.06/117.68 cnf(4110,plain,
% 117.06/117.68 (P5(f14(a2),a2)),
% 117.06/117.68 inference(scs_inference,[],[4098,151,92,54])).
% 117.06/117.68 cnf(4112,plain,
% 117.06/117.68 (P5(f4(a2),f18(x41121,f18(x41122,a2)))),
% 117.06/117.68 inference(scs_inference,[],[4098,151,4102,92,54,91])).
% 117.06/117.68 cnf(4121,plain,
% 117.06/117.68 (P5(f14(a2),f18(x41211,a2))),
% 117.06/117.68 inference(scs_inference,[],[4110,92,91])).
% 117.06/117.68 cnf(4123,plain,
% 117.06/117.68 (~E(x41231,a17)+~E(f5(a17,a2),x41231)),
% 117.06/117.68 inference(scs_inference,[],[4110,655,92,91,3])).
% 117.06/117.68 cnf(4149,plain,
% 117.06/117.68 (~E(x41491,f3(a2))+~E(a17,x41491)),
% 117.06/117.68 inference(scs_inference,[],[3935,4121,92,91,3])).
% 117.06/117.68 cnf(4252,plain,
% 117.06/117.68 (~E(x42521,f5(a17,a2))+~E(a17,x42521)),
% 117.06/117.68 inference(scs_inference,[],[4073,3])).
% 117.06/117.68 cnf(4272,plain,
% 117.06/117.68 (P5(x42721,f18(a2,x42722))+~E(a17,x42721)),
% 117.06/117.68 inference(scs_inference,[],[4088,35])).
% 117.06/117.68 cnf(4408,plain,
% 117.06/117.68 (~P5(f3(f18(a1,a1)),f18(a1,a1))+~P6(x44081,f18(a1,a1),f18(a2,x44082))),
% 117.06/117.68 inference(scs_inference,[],[676,3933,4108,4112,35,36,82])).
% 117.06/117.68 cnf(4429,plain,
% 117.06/117.68 (~E(a17,f3(a16))+P7(a16)),
% 117.06/117.68 inference(scs_inference,[],[3873,2])).
% 117.06/117.68 cnf(4442,plain,
% 117.06/117.68 (P5(x44421,f18(x44422,f18(a2,x44423)))+~E(a17,x44421)),
% 117.06/117.68 inference(scs_inference,[],[4090,35])).
% 117.06/117.68 cnf(4448,plain,
% 117.06/117.68 (P5(x44481,f18(f18(a2,x44482),x44483))+~E(a17,x44481)),
% 117.06/117.68 inference(scs_inference,[],[4100,35])).
% 117.06/117.68 cnf(4518,plain,
% 117.06/117.68 (~E(x45181,f3(a16))+~E(a17,x45181)+P7(a16)),
% 117.06/117.68 inference(scs_inference,[],[4429,3])).
% 117.16/117.68 cnf(4566,plain,
% 117.16/117.68 (P5(f14(a1),a1)+P1(a2,a1)),
% 117.16/117.68 inference(scs_inference,[],[3919,54])).
% 117.16/117.68 cnf(4621,plain,
% 117.16/117.68 (~P5(f3(f18(a1,a1)),f18(a1,a1))+~P6(x46211,f18(x46212,a2),f18(a1,a1))),
% 117.16/117.68 inference(scs_inference,[],[678,3933,81])).
% 117.16/117.68 cnf(4674,plain,
% 117.16/117.68 (~E(x46741,f3(a2))+~E(x46741,a17)),
% 117.16/117.68 inference(scs_inference,[],[4104,2])).
% 117.16/117.68 cnf(4722,plain,
% 117.16/117.68 (P5(f14(a1),f18(a1,x47221))+P1(a2,a1)),
% 117.16/117.68 inference(scs_inference,[],[4566,92])).
% 117.16/117.68 cnf(5781,plain,
% 117.16/117.68 (P2(f14(a1),a1)),
% 117.16/117.68 inference(scs_inference,[],[4045,51])).
% 117.16/117.68 cnf(5787,plain,
% 117.16/117.68 (E(f10(a16,a1),f18(a1,a16))),
% 117.16/117.68 inference(scs_inference,[],[4045,48,179,51,57,63,75])).
% 117.16/117.68 cnf(5789,plain,
% 117.16/117.68 (P6(f3(x57891),f15(f3(x57891),x57891),f7(f3(x57891),x57891))),
% 117.16/117.68 inference(scs_inference,[],[4045,47,48,179,51,57,63,75,77])).
% 117.16/117.68 cnf(5795,plain,
% 117.16/117.68 (E(f13(x57951,f10(a16,a1),x57952),f13(x57951,f18(a1,a16),x57952))),
% 117.16/117.68 inference(scs_inference,[],[4045,47,48,179,51,57,63,75,77,13,14,15,16,17])).
% 117.16/117.68 cnf(5797,plain,
% 117.16/117.68 (E(f18(a1,a16),f10(a16,a1))),
% 117.16/117.68 inference(scs_inference,[],[4045,47,48,179,51,57,63,75,77,13,14,15,16,17,18,2])).
% 117.16/117.68 cnf(5798,plain,
% 117.16/117.68 (E(f18(f10(a16,a1),x57981),f18(f18(a1,a16),x57981))),
% 117.16/117.68 inference(scs_inference,[],[4045,47,48,179,51,57,63,75,77,13,14,15,16,17,18,2,11])).
% 117.16/117.68 cnf(5799,plain,
% 117.16/117.68 (P5(f3(a1),a2)),
% 117.16/117.68 inference(scs_inference,[],[4045,297,47,48,179,51,57,63,75,77,13,14,15,16,17,18,2,11,105])).
% 117.16/117.68 cnf(5805,plain,
% 117.16/117.68 (P4(f3(f10(a16,a1)),f18(a1,a16))),
% 117.16/117.68 inference(scs_inference,[],[4045,297,47,48,179,51,57,63,75,77,13,14,15,16,17,18,2,11,105,6,5,8,111])).
% 117.16/117.68 cnf(5807,plain,
% 117.16/117.68 (P5(f3(x58071),x58071)),
% 117.16/117.68 inference(scs_inference,[],[4045,297,47,48,179,51,57,63,75,77,13,14,15,16,17,18,2,11,105,6,5,8,111,7,55])).
% 117.16/117.68 cnf(5809,plain,
% 117.16/117.68 (P5(a17,a1)),
% 117.16/117.68 inference(scs_inference,[],[4045,297,47,48,179,51,57,63,75,77,13,14,15,16,17,18,2,11,105,6,5,8,111,7,55,74])).
% 117.16/117.68 cnf(5811,plain,
% 117.16/117.68 (~P4(f14(a1),a1)),
% 117.16/117.68 inference(scs_inference,[],[4045,297,47,48,179,51,57,63,75,77,13,14,15,16,17,18,2,11,105,6,5,8,111,7,55,74,56])).
% 117.16/117.68 cnf(5813,plain,
% 117.16/117.68 (P5(a17,a16)),
% 117.16/117.68 inference(scs_inference,[],[4045,297,47,48,179,51,57,63,75,77,13,14,15,16,17,18,2,11,105,6,5,8,111,7,55,74,56,73])).
% 117.16/117.68 cnf(5815,plain,
% 117.16/117.68 (P5(f3(a1),f10(a16,a1))),
% 117.16/117.68 inference(scs_inference,[],[4045,297,47,48,179,51,57,63,75,77,13,14,15,16,17,18,2,11,105,6,5,8,111,7,55,74,56,73,317])).
% 117.16/117.68 cnf(5816,plain,
% 117.16/117.68 (P5(f3(a1),f18(f10(a16,a1),a2))),
% 117.16/117.68 inference(scs_inference,[],[4045,297,47,48,179,51,57,63,75,77,13,14,15,16,17,18,2,11,105,6,5,8,111,7,55,74,56,73,317,61])).
% 117.16/117.68 cnf(5818,plain,
% 117.16/117.68 (P5(a17,f10(a16,a1))),
% 117.16/117.68 inference(scs_inference,[],[4045,297,47,48,179,51,57,63,75,77,13,14,15,16,17,18,2,11,105,6,5,8,111,7,55,74,56,73,317,61,62])).
% 117.16/117.68 cnf(5821,plain,
% 117.16/117.68 (~P2(f3(x58211),x58211)),
% 117.16/117.68 inference(rename_variables,[],[3933])).
% 117.16/117.68 cnf(5824,plain,
% 117.16/117.68 (~P2(f3(x58241),x58241)),
% 117.16/117.68 inference(rename_variables,[],[3933])).
% 117.16/117.68 cnf(5826,plain,
% 117.16/117.68 (P1(f8(x58261,f3(x58261)),x58261)),
% 117.16/117.68 inference(scs_inference,[],[4045,297,3933,5821,5824,47,48,179,51,57,63,75,77,13,14,15,16,17,18,2,11,105,6,5,8,111,7,55,74,56,73,317,61,62,66,67,68])).
% 117.16/117.68 cnf(5827,plain,
% 117.16/117.68 (~P2(f3(x58271),x58271)),
% 117.16/117.68 inference(rename_variables,[],[3933])).
% 117.16/117.68 cnf(5829,plain,
% 117.16/117.68 (P1(f12(x58291,f3(x58291)),x58291)),
% 117.16/117.68 inference(scs_inference,[],[4045,297,3933,5821,5824,5827,47,48,179,51,57,63,75,77,13,14,15,16,17,18,2,11,105,6,5,8,111,7,55,74,56,73,317,61,62,66,67,68,69])).
% 117.16/117.68 cnf(5830,plain,
% 117.16/117.68 (~P2(f3(x58301),x58301)),
% 117.16/117.68 inference(rename_variables,[],[3933])).
% 117.16/117.68 cnf(5833,plain,
% 117.16/117.68 (~P2(f3(x58331),x58331)),
% 117.16/117.68 inference(rename_variables,[],[3933])).
% 117.16/117.68 cnf(5836,plain,
% 117.16/117.68 (~P2(f3(x58361),x58361)),
% 117.16/117.68 inference(rename_variables,[],[3933])).
% 117.16/117.68 cnf(5839,plain,
% 117.16/117.68 (~P2(f3(x58391),x58391)),
% 117.16/117.68 inference(rename_variables,[],[3933])).
% 117.16/117.68 cnf(5840,plain,
% 117.16/117.68 (P4(f3(f18(a1,a16)),f10(a16,a1))),
% 117.16/117.68 inference(scs_inference,[],[4045,297,3933,5821,5824,5827,5830,5833,5836,587,47,48,179,51,57,63,75,77,13,14,15,16,17,18,2,11,105,6,5,8,111,7,55,74,56,73,317,61,62,66,67,68,69,78,79,33,37])).
% 117.16/117.68 cnf(5843,plain,
% 117.16/117.68 (~P6(x58431,f10(a16,a1),f10(a16,a1))),
% 117.16/117.68 inference(scs_inference,[],[4045,297,3933,5821,5824,5827,5830,5833,5836,5839,587,47,48,179,51,57,63,75,77,13,14,15,16,17,18,2,11,105,6,5,8,111,7,55,74,56,73,317,61,62,66,67,68,69,78,79,33,37,3,82])).
% 117.16/117.68 cnf(5844,plain,
% 117.16/117.68 (~P2(f3(x58441),x58441)),
% 117.16/117.68 inference(rename_variables,[],[3933])).
% 117.16/117.68 cnf(5848,plain,
% 117.16/117.68 (E(f18(x58481,f10(a16,a1)),f18(x58481,f18(a1,a16)))),
% 117.16/117.68 inference(scs_inference,[],[4045,297,3933,5821,5824,5827,5830,5833,5836,5839,587,47,48,179,51,57,63,75,77,13,14,15,16,17,18,2,11,105,6,5,8,111,7,55,74,56,73,317,61,62,66,67,68,69,78,79,33,37,3,82,9,10,12])).
% 117.16/117.68 cnf(5865,plain,
% 117.16/117.68 (~P6(x58651,f10(a16,a1),f18(a1,a16))),
% 117.16/117.68 inference(scs_inference,[],[4045,297,3933,5821,5824,5827,5830,5833,5836,5839,587,47,48,179,51,57,63,75,77,13,14,15,16,17,18,2,11,105,6,5,8,111,7,55,74,56,73,317,61,62,66,67,68,69,78,79,33,37,3,82,9,10,12,19,20,21,22,23,24,25,26,27,28,29,30,394,1676,36,41])).
% 117.16/117.68 cnf(5868,plain,
% 117.16/117.68 (~P6(x58681,f18(a1,a16),f10(a16,a1))),
% 117.16/117.68 inference(scs_inference,[],[4045,297,3933,5821,5824,5827,5830,5833,5836,5839,5844,587,47,48,179,51,57,63,75,77,13,14,15,16,17,18,2,11,105,6,5,8,111,7,55,74,56,73,317,61,62,66,67,68,69,78,79,33,37,3,82,9,10,12,19,20,21,22,23,24,25,26,27,28,29,30,394,1676,36,41,34,40])).
% 117.16/117.68 cnf(5869,plain,
% 117.16/117.68 (P5(f13(f10(a16,a1),f10(a16,a1),f3(a1)),f10(a16,a1))),
% 117.16/117.68 inference(scs_inference,[],[4045,297,3933,5821,5824,5827,5830,5833,5836,5839,5844,587,47,48,179,51,57,63,75,77,13,14,15,16,17,18,2,11,105,6,5,8,111,7,55,74,56,73,317,61,62,66,67,68,69,78,79,33,37,3,82,9,10,12,19,20,21,22,23,24,25,26,27,28,29,30,394,1676,36,41,34,40,84])).
% 117.16/117.68 cnf(5871,plain,
% 117.16/117.68 (P2(a17,a16)),
% 117.16/117.68 inference(scs_inference,[],[4045,297,3933,5821,5824,5827,5830,5833,5836,5839,5844,587,47,48,179,51,57,63,75,77,13,14,15,16,17,18,2,11,105,6,5,8,111,7,55,74,56,73,317,61,62,66,67,68,69,78,79,33,37,3,82,9,10,12,19,20,21,22,23,24,25,26,27,28,29,30,394,1676,36,41,34,40,84,81])).
% 117.16/117.68 cnf(5873,plain,
% 117.16/117.68 (~P2(f13(f10(a16,a1),f10(a16,a1),f3(a1)),f10(a16,a1))),
% 117.16/117.68 inference(scs_inference,[],[4045,297,3933,5821,5824,5827,5830,5833,5836,5839,5844,587,47,48,179,51,57,63,75,77,13,14,15,16,17,18,2,11,105,6,5,8,111,7,55,74,56,73,317,61,62,66,67,68,69,78,79,33,37,3,82,9,10,12,19,20,21,22,23,24,25,26,27,28,29,30,394,1676,36,41,34,40,84,81,90])).
% 117.16/117.68 cnf(5877,plain,
% 117.16/117.68 (~E(a16,x58771)+P1(x58771,a16)),
% 117.16/117.68 inference(scs_inference,[],[5813,406])).
% 117.16/117.68 cnf(5879,plain,
% 117.16/117.68 (~P6(x58791,f18(a1,a1),a2)),
% 117.16/117.68 inference(scs_inference,[],[5807,3971])).
% 117.16/117.68 cnf(5880,plain,
% 117.16/117.68 (~P6(x58801,a2,f18(a1,a1))),
% 117.16/117.68 inference(scs_inference,[],[5807,4001])).
% 117.16/117.68 cnf(5881,plain,
% 117.16/117.68 (~P6(x58811,f18(a1,a1),f18(a2,x58812))),
% 117.16/117.68 inference(scs_inference,[],[5807,4408])).
% 117.16/117.68 cnf(5884,plain,
% 117.16/117.68 (~P6(x58841,f18(x58842,a2),f18(a1,a1))),
% 117.16/117.68 inference(scs_inference,[],[5807,4621])).
% 117.16/117.68 cnf(5896,plain,
% 117.16/117.68 (~E(f5(a17,a16),a17)),
% 117.16/117.68 inference(scs_inference,[],[5871,57])).
% 117.16/117.69 cnf(5898,plain,
% 117.16/117.69 (P2(f5(a17,a16),a16)),
% 117.16/117.69 inference(scs_inference,[],[5871,57,63])).
% 117.16/117.69 cnf(5900,plain,
% 117.16/117.69 (P5(f3(a16),a2)),
% 117.16/117.69 inference(scs_inference,[],[5871,5807,57,63,125])).
% 117.16/117.69 cnf(5907,plain,
% 117.16/117.69 (~P6(x59071,f18(a1,a16),f18(a1,a16))),
% 117.16/117.69 inference(scs_inference,[],[5871,5807,5868,5840,5797,57,63,125,55,56,41])).
% 117.16/117.69 cnf(5915,plain,
% 117.16/117.69 (P5(f3(x59151),f18(x59151,x59152))),
% 117.16/117.69 inference(rename_variables,[],[297])).
% 117.16/117.69 cnf(5917,plain,
% 117.16/117.69 (P2(a17,a1)),
% 117.16/117.69 inference(scs_inference,[],[5809,5813,5871,5807,5868,5865,5815,5811,5873,5869,5840,5797,297,47,48,57,63,125,55,56,41,58,37,34,85,82])).
% 117.16/117.69 cnf(5923,plain,
% 117.16/117.69 (~P2(f13(f10(a16,a1),f10(a16,a1),a17),f10(a16,a1))),
% 117.16/117.69 inference(scs_inference,[],[5809,5813,5871,5807,5868,5865,5843,5815,5818,5811,5873,5869,5840,5797,297,5915,47,48,57,63,125,55,56,41,58,37,34,85,82,84,90])).
% 117.16/117.69 cnf(5943,plain,
% 117.16/117.69 (P2(f5(a17,a1),a1)),
% 117.16/117.69 inference(scs_inference,[],[5917,63])).
% 117.16/117.69 cnf(5945,plain,
% 117.16/117.69 (~E(f5(a17,a1),a17)),
% 117.16/117.69 inference(scs_inference,[],[5917,63,57])).
% 117.16/117.69 cnf(5947,plain,
% 117.16/117.69 (~P4(a17,a1)),
% 117.16/117.69 inference(scs_inference,[],[5917,63,57,56])).
% 117.16/117.69 cnf(5949,plain,
% 117.16/117.69 (P5(f3(a16),f10(a16,a1))),
% 117.16/117.69 inference(scs_inference,[],[5917,5787,5807,63,57,56,61])).
% 117.16/117.69 cnf(5955,plain,
% 117.16/117.69 (P5(f3(x59551),f18(x59551,x59552))),
% 117.16/117.69 inference(rename_variables,[],[297])).
% 117.16/117.69 cnf(5957,plain,
% 117.16/117.69 (P5(f13(f18(a1,a1),a2,f3(a1)),f18(a1,a1))),
% 117.16/117.69 inference(scs_inference,[],[5917,5799,5879,5880,5923,5787,5807,5797,297,5955,63,57,56,61,34,85,84])).
% 117.16/117.69 cnf(5965,plain,
% 117.16/117.69 (P5(f13(a2,f18(a1,a1),f3(a1)),a1)),
% 117.16/117.69 inference(scs_inference,[],[5917,5799,5879,5880,5923,5787,5807,5797,297,5955,63,57,56,61,34,85,84,105,68,93])).
% 117.16/117.69 cnf(5978,plain,
% 117.16/117.69 (P2(f5(f14(a1),a1),a1)),
% 117.16/117.69 inference(scs_inference,[],[5781,5957,57,105,63])).
% 117.16/117.69 cnf(5982,plain,
% 117.16/117.69 (P5(f13(f10(a16,a1),f10(a16,a1),f3(a16)),f10(a16,a1))),
% 117.16/117.69 inference(scs_inference,[],[5781,5949,5898,5957,5843,57,105,63,56,85])).
% 117.16/117.69 cnf(5983,plain,
% 117.16/117.69 (~P6(x59831,f10(a16,a1),f10(a16,a1))),
% 117.16/117.69 inference(rename_variables,[],[5843])).
% 117.16/117.69 cnf(5985,plain,
% 117.16/117.69 (P5(f13(f10(a16,a1),f10(a16,a1),a17),f10(a16,a1))),
% 117.16/117.69 inference(scs_inference,[],[5781,5949,5898,5957,5818,5843,5983,57,105,63,56,85,84])).
% 117.16/117.69 cnf(5990,plain,
% 117.16/117.69 (P5(f13(a2,f18(a1,a1),f3(a1)),f10(a16,a1))),
% 117.16/117.69 inference(scs_inference,[],[5781,5900,5949,5898,5957,5965,5818,5843,5983,5787,57,105,63,56,85,84,69,62])).
% 117.16/117.69 cnf(5994,plain,
% 117.16/117.69 (P2(f5(f5(a17,a1),a1),a1)),
% 117.16/117.69 inference(scs_inference,[],[5943,63])).
% 117.16/117.69 cnf(5996,plain,
% 117.16/117.69 (~E(f5(f5(a17,a1),a1),f5(a17,a1))),
% 117.16/117.69 inference(scs_inference,[],[5943,63,57])).
% 117.16/117.69 cnf(6011,plain,
% 117.16/117.69 (~E(f5(f5(a17,a16),a16),f5(a17,a16))),
% 117.16/117.69 inference(scs_inference,[],[5898,57])).
% 117.16/117.69 cnf(6013,plain,
% 117.16/117.69 (P2(f5(f5(a17,a16),a16),a16)),
% 117.16/117.69 inference(scs_inference,[],[5898,57,63])).
% 117.16/117.69 cnf(6021,plain,
% 117.16/117.69 (P2(f5(f14(a2),a2),a2)),
% 117.16/117.69 inference(scs_inference,[],[151,63])).
% 117.16/117.69 cnf(6030,plain,
% 117.16/117.69 (E(f5(f5(a17,a1),a1),a17)),
% 117.16/117.69 inference(scs_inference,[],[5945,5990,5996,6013,5994,5917,5943,5787,3933,151,63,57,56,36,33,64])).
% 117.16/117.69 cnf(6032,plain,
% 117.16/117.69 (E(a17,f5(f5(a17,a1),a1))),
% 117.16/117.69 inference(scs_inference,[],[5945,5990,5996,6013,5994,5917,5943,5787,3933,151,63,57,56,36,33,64,2])).
% 117.16/117.69 cnf(6034,plain,
% 117.16/117.69 (P5(f3(a17),f5(f5(a17,a1),a1))),
% 117.16/117.69 inference(scs_inference,[],[5945,5990,5996,6013,5994,5917,5943,5787,3933,151,63,57,56,36,33,64,2,111,55])).
% 117.16/117.69 cnf(6039,plain,
% 117.16/117.69 (~P4(f5(f5(a17,a1),a1),a1)),
% 117.16/117.69 inference(scs_inference,[],[5945,5990,5996,6013,5994,5947,5813,5917,5943,5787,3933,151,63,57,56,36,33,64,2,111,55,4518,35,37])).
% 117.16/117.69 cnf(6048,plain,
% 117.16/117.69 (P2(f5(a17,a2),a2)),
% 117.16/117.69 inference(scs_inference,[],[46,63])).
% 117.16/117.69 cnf(6052,plain,
% 117.16/117.69 (P2(f5(f5(a17,a1),a1),a16)),
% 117.16/117.69 inference(scs_inference,[],[5978,6032,5871,46,63,56,33])).
% 117.16/117.69 cnf(6053,plain,
% 117.16/117.69 (P4(f13(f10(a16,a1),f10(a16,a1),a17),f10(a16,a1))),
% 117.16/117.69 inference(scs_inference,[],[5978,6032,5985,5923,5871,46,63,56,33,58])).
% 117.16/117.69 cnf(6055,plain,
% 117.16/117.69 (~P2(f3(a17),f5(f5(a17,a1),a1))),
% 117.16/117.69 inference(scs_inference,[],[5978,6030,6032,5985,5923,5871,3933,46,63,56,33,58,34])).
% 117.16/117.69 cnf(6086,plain,
% 117.16/117.69 (P2(f5(f5(a17,a2),a2),a2)),
% 117.16/117.69 inference(scs_inference,[],[6048,63])).
% 117.16/117.69 cnf(6095,plain,
% 117.16/117.69 (P5(f13(f10(a16,a1),f10(a16,a1),a17),f18(a1,a16))),
% 117.16/117.69 inference(scs_inference,[],[6048,6053,5957,5787,3933,63,56,33,93,38,55])).
% 117.16/117.69 cnf(6106,plain,
% 117.16/117.69 (E(a17,f5(f5(a17,a2),a2))),
% 117.16/117.69 inference(scs_inference,[],[6052,6086,4073,6048,654,46,56,64])).
% 117.16/117.69 cnf(6108,plain,
% 117.16/117.69 (P6(f5(f5(a17,a2),a2),a1,a16)),
% 117.16/117.69 inference(scs_inference,[],[6052,6086,4073,6048,654,46,56,64,124])).
% 117.16/117.69 cnf(6109,plain,
% 117.16/117.69 (E(f5(f5(a17,a2),a2),a17)),
% 117.16/117.69 inference(scs_inference,[],[6052,6086,4073,6048,654,46,56,64,124,2])).
% 117.16/117.69 cnf(6110,plain,
% 117.16/117.69 (P5(f5(f5(a17,a2),a2),a16)),
% 117.16/117.69 inference(scs_inference,[],[6052,6086,4073,6048,654,46,56,64,124,2,73])).
% 117.16/117.69 cnf(6112,plain,
% 117.16/117.69 (P5(f5(f5(a17,a2),a2),a1)),
% 117.16/117.69 inference(scs_inference,[],[6052,6086,4073,6048,654,46,56,64,124,2,73,74])).
% 117.16/117.69 cnf(6115,plain,
% 117.16/117.69 (P5(f3(a17),f5(f5(a17,a2),a2))),
% 117.16/117.69 inference(scs_inference,[],[6052,6086,4073,6048,654,46,56,64,124,2,73,74,111,55])).
% 117.16/117.69 cnf(6132,plain,
% 117.16/117.69 (~P4(f5(f14(a2),a2),a2)),
% 117.16/117.69 inference(scs_inference,[],[6021,6110,125,56])).
% 117.16/117.69 cnf(6137,plain,
% 117.16/117.69 (P2(f5(f5(a17,a2),a2),a16)),
% 117.16/117.69 inference(scs_inference,[],[6021,6112,6110,6109,6108,5947,3933,125,56,33,37,81])).
% 117.16/117.69 cnf(6146,plain,
% 117.16/117.69 (P5(f5(f5(a17,a2),a2),f10(a16,a1))),
% 117.16/117.69 inference(scs_inference,[],[6137,6112,5787,56,62])).
% 117.16/117.69 cnf(6148,plain,
% 117.16/117.69 (~P2(f3(a17),f5(f5(a17,a2),a2))),
% 117.16/117.69 inference(scs_inference,[],[6137,6112,6109,5787,3933,56,62,34])).
% 117.16/117.69 cnf(6179,plain,
% 117.16/117.69 (~P2(f13(f10(a16,a1),f10(a16,a1),f3(a16)),f10(a16,a1))),
% 117.16/117.69 inference(scs_inference,[],[6146,5907,6086,5843,5949,423,5787,56,36,68,84,90])).
% 117.16/117.69 cnf(6187,plain,
% 117.16/117.69 (P4(f13(f10(a16,a1),f10(a16,a1),f3(a16)),f10(a16,a1))),
% 117.16/117.69 inference(scs_inference,[],[6179,5982,58])).
% 117.16/117.69 cnf(6193,plain,
% 117.16/117.69 (P5(f13(f18(a1,a16),f10(a16,a1),a17),f18(a1,a16))),
% 117.16/117.69 inference(scs_inference,[],[6179,5982,6115,6148,5865,5818,5797,5807,423,58,34,81,84])).
% 117.16/117.69 cnf(6197,plain,
% 117.16/117.69 (~P6(x61971,a17,a17)),
% 117.16/117.69 inference(scs_inference,[],[6179,5982,6115,6148,6106,5865,5818,5797,5807,423,58,34,81,84,41])).
% 117.16/117.69 cnf(6211,plain,
% 117.16/117.69 (~P5(f3(a16),a1)),
% 117.16/117.69 inference(scs_inference,[],[6197,6187,6108,6030,6109,5807,5787,3933,41,38,40,81])).
% 117.16/117.69 cnf(6212,plain,
% 117.16/117.69 (P5(f3(x62121),x62121)),
% 117.16/117.69 inference(rename_variables,[],[5807])).
% 117.16/117.69 cnf(6215,plain,
% 117.16/117.69 (P5(f13(a17,a17,f3(a17)),a17)),
% 117.16/117.69 inference(scs_inference,[],[6197,6187,6108,6030,6109,5807,6212,5787,3933,41,38,40,81,85])).
% 117.16/117.69 cnf(6216,plain,
% 117.16/117.69 (~P6(x62161,a17,a17)),
% 117.16/117.69 inference(rename_variables,[],[6197])).
% 117.16/117.69 cnf(6217,plain,
% 117.16/117.69 (P5(f3(x62171),x62171)),
% 117.16/117.69 inference(rename_variables,[],[5807])).
% 117.16/117.69 cnf(6219,plain,
% 117.16/117.69 (~P2(f13(a17,a17,f3(a17)),a17)),
% 117.16/117.69 inference(scs_inference,[],[6197,6216,6187,6108,6030,6109,5807,6212,6217,5787,3933,41,38,40,81,85,90])).
% 117.16/117.69 cnf(6279,plain,
% 117.16/117.69 (~P5(f3(a1),a16)),
% 117.16/117.69 inference(scs_inference,[],[6108,5807,3933,82])).
% 117.16/117.69 cnf(6290,plain,
% 117.16/117.69 (~P1(f18(f10(a16,a1),a2),a16)),
% 117.16/117.69 inference(scs_inference,[],[6193,5816,6108,5807,3933,82,65,54,36,93,60])).
% 117.16/117.69 cnf(6297,plain,
% 117.16/117.69 (P4(f13(a17,a17,f3(a17)),a17)),
% 117.16/117.69 inference(scs_inference,[],[6290,6219,6215,5877,58])).
% 117.16/117.69 cnf(6364,plain,
% 117.16/117.69 (E(f5(f5(a17,a16),a16),a17)),
% 117.16/117.69 inference(scs_inference,[],[6011,6132,5896,6013,5898,6109,5871,5900,6211,47,62,37,31,64])).
% 117.16/117.69 cnf(6384,plain,
% 117.16/117.69 (~P6(x63841,a17,f5(f5(a17,a16),a16))),
% 117.16/117.69 inference(scs_inference,[],[6364,6197,2,111,55,41])).
% 117.16/117.69 cnf(6396,plain,
% 117.16/117.69 (P5(f5(f5(a17,a16),a16),a1)),
% 117.16/117.69 inference(scs_inference,[],[6364,5907,6197,5813,5917,423,3933,2,111,55,41,35,33,34,90,125,124,74])).
% 117.16/117.69 cnf(6556,plain,
% 117.16/117.69 (~E(a2,f18(a1,a1))),
% 117.16/117.69 inference(scs_inference,[],[5900,6211,65])).
% 117.16/117.69 cnf(6731,plain,
% 117.16/117.69 (~P1(a2,a1)),
% 117.16/117.69 inference(scs_inference,[],[5900,6211,60])).
% 117.16/117.69 cnf(6733,plain,
% 117.16/117.69 (~P5(f6(a2,a1),a1)),
% 117.16/117.69 inference(scs_inference,[],[5900,6211,60,70])).
% 117.16/117.69 cnf(6735,plain,
% 117.16/117.69 (P5(f6(a2,a1),a2)),
% 117.16/117.69 inference(scs_inference,[],[5900,6211,60,70,59])).
% 117.16/117.69 cnf(6741,plain,
% 117.16/117.69 (~P5(f6(a2,a1),f18(a1,a1))),
% 117.16/117.69 inference(scs_inference,[],[6039,5826,5900,6211,60,70,59,486,38,31,93])).
% 117.16/117.69 cnf(6746,plain,
% 117.16/117.69 (~P2(f6(a2,a1),a1)),
% 117.16/117.69 inference(scs_inference,[],[6039,6396,5826,5900,6211,60,70,59,486,38,31,93,35,65,54])).
% 117.16/117.69 cnf(6752,plain,
% 117.16/117.69 (P5(f14(a1),a1)),
% 117.16/117.69 inference(scs_inference,[],[6731,4566])).
% 117.16/117.69 cnf(6753,plain,
% 117.16/117.69 (P5(f14(a1),f18(a1,x67531))),
% 117.16/117.69 inference(scs_inference,[],[6731,4722])).
% 117.16/117.69 cnf(6764,plain,
% 117.16/117.69 (~E(a2,a1)),
% 117.16/117.69 inference(scs_inference,[],[6741,6733,6735,54,337,61,62,60,36])).
% 117.16/117.69 cnf(6770,plain,
% 117.16/117.69 (~P5(f6(a2,f18(a1,a1)),f18(a1,a1))),
% 117.16/117.69 inference(scs_inference,[],[6741,6733,6746,6735,5978,54,337,61,62,60,36,33,338,2267,70])).
% 117.16/117.69 cnf(6776,plain,
% 117.16/117.69 (~P1(f18(a1,a16),x67761)+P1(f10(a16,a1),x67761)),
% 117.16/117.69 inference(scs_inference,[],[6741,6733,6746,6735,5978,5797,54,337,61,62,60,36,33,338,2267,70,92,59,31])).
% 117.16/117.69 cnf(6781,plain,
% 117.16/117.69 (P5(f14(a1),a2)),
% 117.16/117.69 inference(scs_inference,[],[6753,6770,54,105])).
% 117.16/117.69 cnf(6782,plain,
% 117.16/117.69 (P5(f14(a1),f18(a1,x67821))),
% 117.16/117.69 inference(rename_variables,[],[6753])).
% 117.16/117.69 cnf(6788,plain,
% 117.16/117.69 (P5(f14(a1),f10(a16,a1))),
% 117.16/117.69 inference(scs_inference,[],[6753,6782,6770,6731,5829,5949,5797,6211,54,105,60,31,36])).
% 117.16/117.69 cnf(6789,plain,
% 117.16/117.69 (P5(f14(a1),f18(a1,x67891))),
% 117.16/117.69 inference(rename_variables,[],[6753])).
% 117.16/117.69 cnf(6790,plain,
% 117.16/117.69 (P5(f13(f18(a1,a1),a2,f14(a1)),f18(a1,a1))),
% 117.16/117.69 inference(scs_inference,[],[6753,6782,6789,6770,6731,5829,5880,5949,5797,6211,54,105,60,31,36,84])).
% 117.16/117.69 cnf(6792,plain,
% 117.16/117.69 (P5(f14(a1),f18(a1,x67921))),
% 117.16/117.69 inference(rename_variables,[],[6753])).
% 117.16/117.69 cnf(6795,plain,
% 117.16/117.69 (~P6(x67951,f18(a1,a16),f18(a1,a16))),
% 117.16/117.69 inference(rename_variables,[],[5907])).
% 117.16/117.69 cnf(6796,plain,
% 117.16/117.69 (P5(f14(a1),f18(a1,x67961))),
% 117.16/117.69 inference(rename_variables,[],[6753])).
% 117.16/117.69 cnf(6798,plain,
% 117.16/117.69 (~P2(f13(f18(a1,a16),f18(a1,a16),f14(a1)),f18(a1,a16))),
% 117.16/117.69 inference(scs_inference,[],[6753,6782,6789,6792,6796,6770,6731,5829,5907,6795,5880,5949,5797,6211,54,105,60,31,36,84,85,90])).
% 117.16/117.69 cnf(6802,plain,
% 117.16/117.69 (~P5(f6(f10(a16,a1),a1),a1)),
% 117.16/117.69 inference(scs_inference,[],[6753,6782,6789,6792,6796,6770,6731,5829,5907,6795,5880,5949,5797,6211,54,105,60,31,36,84,85,90,70])).
% 117.16/117.69 cnf(6804,plain,
% 117.16/117.69 (P5(f6(f10(a16,a1),a1),f10(a16,a1))),
% 117.16/117.69 inference(scs_inference,[],[6753,6782,6789,6792,6796,6770,6731,5829,5907,6795,5880,5949,5797,6211,54,105,60,31,36,84,85,90,70,59])).
% 117.16/117.69 cnf(6809,plain,
% 117.16/117.69 (P4(f13(f18(a1,a16),f18(a1,a16),f14(a1)),f18(a1,a16))),
% 117.16/117.69 inference(scs_inference,[],[6753,6782,6789,6792,6796,6770,6731,6095,5829,5907,6795,5880,5949,5797,6211,54,105,60,31,36,84,85,90,70,59,486,93,58])).
% 117.16/117.69 cnf(6811,plain,
% 117.16/117.69 (~P1(f18(a1,a16),a1)),
% 117.16/117.69 inference(scs_inference,[],[6753,6782,6789,6792,6796,6770,6731,6095,5829,5907,6795,5880,5949,5797,6211,54,105,60,31,36,84,85,90,70,59,486,93,58,6776])).
% 117.16/117.69 cnf(6818,plain,
% 117.16/117.69 (~P5(f6(f18(a1,a16),a1),a1)),
% 117.16/117.69 inference(scs_inference,[],[6811,6802,54,70])).
% 117.16/117.69 cnf(6822,plain,
% 117.16/117.69 (P5(f6(f18(a1,a16),a1),f18(a1,a16))),
% 117.16/117.69 inference(scs_inference,[],[6811,6790,6802,54,70,105,59])).
% 117.16/117.69 cnf(6830,plain,
% 117.16/117.69 (~P5(f6(f10(a16,a1),a1),f18(a1,a1))),
% 117.16/117.69 inference(scs_inference,[],[6811,6809,6790,6802,5797,54,70,105,59,486,61,38,62,93])).
% 117.16/117.69 cnf(6838,plain,
% 117.16/117.69 (P5(f13(f10(a16,a1),f10(a16,a1),f14(a1)),f10(a16,a1))),
% 117.16/117.69 inference(scs_inference,[],[6781,6788,6811,6809,6798,6804,6790,6802,6753,5879,5843,5787,5797,54,70,105,59,486,61,38,62,93,36,34,84,85])).
% 117.16/117.69 cnf(6846,plain,
% 117.16/117.69 (~P1(f10(a16,a1),f18(a1,a1))),
% 117.16/117.69 inference(scs_inference,[],[6781,6788,6811,6809,6798,6804,6790,6802,6753,5879,5843,5787,5797,54,70,105,59,486,61,38,62,93,36,34,84,85,65,337,55,60])).
% 117.16/117.69 cnf(6858,plain,
% 117.16/117.69 (~P5(f6(f10(a16,a1),f18(a1,a1)),f18(a1,a1))),
% 117.16/117.69 inference(scs_inference,[],[6846,6830,54,70])).
% 117.16/117.69 cnf(6860,plain,
% 117.16/117.69 (P5(f6(f10(a16,a1),f18(a1,a1)),f10(a16,a1))),
% 117.16/117.69 inference(scs_inference,[],[6846,6830,54,70,59])).
% 117.16/117.69 cnf(6862,plain,
% 117.16/117.69 (~P5(f6(f10(a16,a1),f18(a1,a1)),a1)),
% 117.16/117.69 inference(scs_inference,[],[6846,6830,54,70,59,91])).
% 117.16/117.69 cnf(6868,plain,
% 117.16/117.69 (~P1(f10(a16,a1),a16)),
% 117.16/117.69 inference(scs_inference,[],[6846,6830,6804,5815,6279,54,70,59,91,61,62,60])).
% 117.16/117.69 cnf(6870,plain,
% 117.16/117.69 (~P1(f18(a1,a16),f18(a1,a1))),
% 117.16/117.69 inference(scs_inference,[],[6846,6830,6804,5815,5797,6279,54,70,59,91,61,62,60,31])).
% 117.16/117.69 cnf(6871,plain,
% 117.16/117.69 (P5(f6(f18(a1,a16),a1),a16)),
% 117.16/117.69 inference(scs_inference,[],[6846,6830,6822,6818,6804,5815,5797,6279,54,70,59,91,61,62,60,31,93])).
% 117.16/117.69 cnf(6875,plain,
% 117.16/117.69 (P5(f13(f18(a1,a16),f10(a16,a1),f14(a1)),f10(a16,a1))),
% 117.16/117.69 inference(scs_inference,[],[6846,6830,6822,6818,6752,6788,6753,6804,5865,5815,5797,6279,54,70,59,91,61,62,60,31,93,35,36,85])).
% 117.16/117.69 cnf(6896,plain,
% 117.16/117.69 (~P5(f6(f18(a1,a16),f18(a1,a1)),f18(a1,a1))),
% 117.16/117.69 inference(scs_inference,[],[6870,6858,54,70])).
% 117.16/117.69 cnf(6898,plain,
% 117.16/117.69 (P5(f6(f18(a1,a16),f18(a1,a1)),f18(a1,a16))),
% 117.16/117.69 inference(scs_inference,[],[6870,6858,54,70,59])).
% 117.16/117.69 cnf(6900,plain,
% 117.16/117.69 (~P5(f6(f18(a1,a16),f18(a1,a1)),a1)),
% 117.16/117.69 inference(scs_inference,[],[6870,6858,54,70,59,91])).
% 117.16/117.69 cnf(6906,plain,
% 117.16/117.69 (~P1(f18(a1,a16),a16)),
% 117.16/117.69 inference(scs_inference,[],[6870,6868,6858,5797,54,70,59,91,61,62,31])).
% 117.16/117.69 cnf(6907,plain,
% 117.16/117.69 (~P5(f6(a2,a1),f18(f18(a1,a1),f18(a1,a1)))),
% 117.16/117.69 inference(scs_inference,[],[6870,6868,6858,6741,5797,54,70,59,91,61,62,31,93])).
% 117.16/117.69 cnf(6927,plain,
% 117.16/117.69 (~P5(f6(f18(a1,a16),a16),a16)),
% 117.16/117.69 inference(scs_inference,[],[6906,6896,54,70])).
% 117.16/117.69 cnf(6929,plain,
% 117.16/117.69 (P5(f6(f18(a1,a16),a16),f18(a1,a16))),
% 117.16/117.69 inference(scs_inference,[],[6906,6896,54,70,59])).
% 117.16/117.69 cnf(6935,plain,
% 117.16/117.69 (~P1(a16,a1)),
% 117.16/117.69 inference(scs_inference,[],[6906,6896,6907,6871,6818,6735,54,70,59,61,62,60])).
% 117.16/117.69 cnf(6937,plain,
% 117.16/117.69 (P5(f6(f18(a1,a16),f18(a1,a1)),a16)),
% 117.16/117.69 inference(scs_inference,[],[6906,6896,6898,6907,6900,6871,6818,6735,54,70,59,61,62,60,93])).
% 117.16/117.69 cnf(6939,plain,
% 117.16/117.69 (P5(f6(f10(a16,a1),f18(a1,a1)),f18(a1,a16))),
% 117.16/117.69 inference(scs_inference,[],[6906,6860,6896,6898,6907,6900,6871,6818,6735,5787,54,70,59,61,62,60,93,36])).
% 117.16/117.69 cnf(6946,plain,
% 117.16/117.69 (P5(f13(f10(a16,a1),f18(a1,a16),f14(a1)),f10(a16,a1))),
% 117.16/117.69 inference(scs_inference,[],[6764,6906,6860,6896,6898,6907,6900,6871,6818,6788,6753,5868,6735,5787,54,70,59,61,62,60,93,36,65,125,76,84])).
% 117.16/117.69 cnf(6955,plain,
% 117.16/117.69 (~P5(f6(a16,a1),a1)),
% 117.16/117.69 inference(scs_inference,[],[6935,6862,54,70])).
% 117.16/117.69 cnf(6965,plain,
% 117.16/117.69 (~P1(a16,f18(a1,a1))),
% 117.16/117.69 inference(scs_inference,[],[6935,6862,6937,6896,54,70,59,125,61,62,60])).
% 117.16/117.69 cnf(6967,plain,
% 117.16/117.69 (P5(f6(f10(a16,a1),f18(a1,a1)),a16)),
% 117.16/117.69 inference(scs_inference,[],[6935,6939,6862,6937,6896,54,70,59,125,61,62,60,93])).
% 117.16/117.69 cnf(6990,plain,
% 117.16/117.69 (~P5(f6(a16,f18(a1,a1)),f18(a1,a1))),
% 117.16/117.69 inference(scs_inference,[],[6965,6955,54,70])).
% 117.16/117.69 cnf(6992,plain,
% 117.16/117.69 (P5(f6(a16,f18(a1,a1)),a16)),
% 117.16/117.69 inference(scs_inference,[],[6965,6955,54,70,59])).
% 117.16/117.69 cnf(6998,plain,
% 117.16/117.69 (~P1(a2,a16)),
% 117.16/117.69 inference(scs_inference,[],[6965,6955,6967,5799,6279,54,70,59,125,91,60])).
% 117.16/117.69 cnf(7000,plain,
% 117.16/117.69 (P5(f6(f18(a1,a16),a16),a1)),
% 117.16/117.69 inference(scs_inference,[],[6965,6955,6967,6929,6927,5799,6279,54,70,59,125,91,60,93])).
% 117.16/117.69 cnf(7012,plain,
% 117.16/117.69 (P2(f14(a16),a16)),
% 117.16/117.69 inference(scs_inference,[],[6965,6955,6838,6967,6929,6927,6907,6735,5799,5787,6279,54,70,59,125,91,60,93,36,5877,101,61,62,3869,51])).
% 117.16/117.69 cnf(7014,plain,
% 117.16/117.69 (P2(f5(f14(a16),a16),a16)),
% 117.16/117.69 inference(scs_inference,[],[6965,6955,6838,6967,6929,6927,6907,6735,5799,5787,6279,54,70,59,125,91,60,93,36,5877,101,61,62,3869,51,63])).
% 117.16/117.69 cnf(7027,plain,
% 117.16/117.69 (~P5(f6(a2,a16),a16)),
% 117.16/117.69 inference(scs_inference,[],[6998,7012,6990,57,54,70])).
% 117.16/117.69 cnf(7029,plain,
% 117.16/117.69 (~P4(f5(f14(a16),a16),a16)),
% 117.16/117.69 inference(scs_inference,[],[6998,7012,6990,7014,57,54,70,56])).
% 117.16/117.69 cnf(7031,plain,
% 117.16/117.69 (P5(f6(a2,a16),a2)),
% 117.16/117.69 inference(scs_inference,[],[6998,7012,6990,7014,57,54,70,56,59])).
% 117.16/117.69 cnf(7035,plain,
% 117.16/117.69 (~P1(a1,a16)),
% 117.16/117.69 inference(scs_inference,[],[6998,7012,6990,6992,7000,7014,6927,57,54,70,56,59,125,60])).
% 117.16/117.69 cnf(7037,plain,
% 117.16/117.69 (~P5(f6(a16,a1),f18(a1,a1))),
% 117.16/117.69 inference(scs_inference,[],[6998,7012,6990,6992,7000,7014,6955,6927,57,54,70,56,59,125,60,93])).
% 117.16/117.69 cnf(7050,plain,
% 117.16/117.69 (~P5(f6(a1,a16),a16)),
% 117.16/117.69 inference(scs_inference,[],[7035,7037,54,70])).
% 117.16/117.69 cnf(7052,plain,
% 117.16/117.69 (P5(f6(a1,a16),a1)),
% 117.16/117.69 inference(scs_inference,[],[7035,7037,54,70,59])).
% 117.16/117.69 cnf(7056,plain,
% 117.16/117.69 (~P1(f18(a16,x70561),a1)),
% 117.16/117.69 inference(scs_inference,[],[7035,7037,297,6211,54,70,59,101,60])).
% 117.16/117.69 cnf(7059,plain,
% 117.16/117.69 (P5(f13(f18(a1,a1),a2,f14(a1)),a1)),
% 117.16/117.69 inference(scs_inference,[],[7035,7037,6790,297,6211,54,70,59,101,60,93])).
% 117.16/117.69 cnf(7076,plain,
% 117.16/117.69 (~P5(f6(f18(a16,x70761),a1),a1)),
% 117.16/117.69 inference(scs_inference,[],[7056,7027,54,70])).
% 117.16/117.69 cnf(7078,plain,
% 117.16/117.69 (P5(f6(f18(a16,x70781),a1),f18(a16,x70781))),
% 117.16/117.69 inference(scs_inference,[],[7056,7027,54,70,59])).
% 117.16/117.69 cnf(7080,plain,
% 117.16/117.69 (~P5(f6(a2,a16),f18(a16,a16))),
% 117.16/117.69 inference(scs_inference,[],[7056,7027,54,70,59,93])).
% 117.16/117.69 cnf(7084,plain,
% 117.16/117.69 (~P2(f13(f10(a16,a1),f10(a16,a1),f14(a1)),f10(a16,a1))),
% 117.16/117.69 inference(scs_inference,[],[7056,7027,6788,5843,5815,6279,54,70,59,93,65,90])).
% 117.16/117.69 cnf(7093,plain,
% 117.16/117.69 (~P1(a2,f18(a16,a16))),
% 117.16/117.69 inference(scs_inference,[],[7031,7056,7027,6788,5843,5815,6279,54,70,59,93,65,90,441,337,61,62,60])).
% 117.16/117.69 cnf(7112,plain,
% 117.16/117.69 (~P5(f6(a2,f18(a16,a16)),a16)),
% 117.16/117.69 inference(scs_inference,[],[7080,7093,54,70,59,91])).
% 117.16/117.69 cnf(7116,plain,
% 117.16/117.69 (P5(f6(f18(a16,a1),a1),a16)),
% 117.16/117.69 inference(scs_inference,[],[7080,7093,7078,7076,7059,5787,54,70,59,91,62,93])).
% 117.16/117.69 cnf(7131,plain,
% 117.16/117.69 (P5(f13(f10(a16,a1),f18(a1,a16),a17),f10(a16,a1))),
% 117.16/117.69 inference(scs_inference,[],[47,7080,7093,7084,6875,7078,7076,7059,7029,6838,7031,5868,5818,423,5797,5787,54,70,59,91,62,93,58,34,65,125,37,61,84])).
% 117.16/117.69 cnf(7140,plain,
% 117.16/117.69 (~P5(f6(f10(a16,a1),a16),a16)),
% 117.16/117.69 inference(scs_inference,[],[7050,6868,54,70])).
% 117.16/117.69 cnf(7142,plain,
% 117.16/117.69 (P5(f6(f10(a16,a1),a16),f10(a16,a1))),
% 117.16/117.69 inference(scs_inference,[],[7050,6868,54,70,59])).
% 117.16/117.69 cnf(7145,plain,
% 117.16/117.69 (~P5(f6(a1,a16),f18(a16,a16))),
% 117.16/117.69 inference(scs_inference,[],[7050,7116,6868,54,70,59,35,93])).
% 117.16/117.69 cnf(7169,plain,
% 117.16/117.69 (~P5(f6(f10(a16,a1),a16),f18(a16,a16))),
% 117.16/117.69 inference(scs_inference,[],[7112,7140,7145,7052,54,62,93])).
% 117.16/117.69 cnf(7179,plain,
% 117.16/117.69 (~P1(f10(a16,a1),f18(a16,a16))),
% 117.16/117.69 inference(scs_inference,[],[6946,7112,7142,7078,7140,7076,7145,7052,5787,54,62,93,36,65,441,337,61,60])).
% 117.16/117.69 cnf(7221,plain,
% 117.16/117.69 (P5(f6(f10(a16,a1),f18(a16,a16)),f10(a16,a1))),
% 117.16/117.69 inference(scs_inference,[],[7179,7169,442,338,2267,54,59])).
% 117.16/117.69 cnf(7223,plain,
% 117.16/117.69 (~P5(f6(f10(a16,a1),f18(a16,a16)),f18(a16,a16))),
% 117.16/117.69 inference(scs_inference,[],[7179,7169,442,338,2267,54,59,70])).
% 117.16/117.69 cnf(7225,plain,
% 117.16/117.69 (~P5(f6(f10(a16,a1),f18(a16,a16)),a16)),
% 117.16/117.69 inference(scs_inference,[],[7179,7169,442,338,2267,54,59,70,91])).
% 117.16/117.69 cnf(7229,plain,
% 117.16/117.69 (~P1(f18(a1,a16),f18(a16,a16))),
% 117.16/117.69 inference(scs_inference,[],[7179,7169,7142,5797,442,338,2267,54,59,70,91,62,31])).
% 117.16/117.69 cnf(7263,plain,
% 117.16/117.69 (P5(f13(f18(a1,a16),f10(a16,a1),f14(a1)),f18(a1,a16))),
% 117.16/117.69 inference(scs_inference,[],[7229,7223,7131,6788,6753,5865,442,338,2267,54,59,70,91,61,62,93,65,101,60,84])).
% 117.16/117.69 cnf(7330,plain,
% 117.16/117.69 (~E(f18(f18(a16,a16),f18(a16,a16)),f18(x73301,a2))),
% 117.16/117.69 inference(scs_inference,[],[7225,7080,7145,7031,7052,54,60,93,442,338,2267,59,101,70,91,337,61])).
% 117.16/117.69 cnf(7431,plain,
% 117.16/117.69 (~P5(f6(a1,a16),f18(f18(a16,a16),f18(a16,a16)))),
% 117.16/117.69 inference(scs_inference,[],[6900,7145,54,93])).
% 117.16/117.69 cnf(7563,plain,
% 117.16/117.69 (~P5(a17,f18(a1,a1))+P5(f13(f18(a1,a1),a2,a17),f18(a1,a1))),
% 117.16/117.69 inference(scs_inference,[],[6818,4086,5880,54,84])).
% 117.16/117.69 cnf(7995,plain,
% 117.16/117.69 (~P5(a17,f18(a1,a1))+P5(f13(a2,f18(a1,a1),a17),a2)),
% 117.16/117.69 inference(scs_inference,[],[5879,4086,84])).
% 117.16/117.69 cnf(8037,plain,
% 117.16/117.69 (~P5(a17,f18(a1,a1))+P5(f13(f18(a1,a1),a2,a17),a2)),
% 117.16/117.69 inference(scs_inference,[],[4086,5880,85])).
% 117.16/117.69 cnf(8082,plain,
% 117.16/117.69 (P5(f6(f10(a16,a1),f18(a16,a16)),a1)),
% 117.16/117.69 inference(scs_inference,[],[7221,7225,7431,7052,5787,36,61,93])).
% 117.16/117.69 cnf(8242,plain,
% 117.16/117.69 (~P5(a17,f18(a1,a1))+P5(f13(f18(a2,a2),f18(a1,a1),a17),f18(a1,a1))),
% 117.16/117.69 inference(scs_inference,[],[223,5881,85])).
% 117.16/117.69 cnf(8269,plain,
% 117.16/117.69 (~P5(a17,f18(a1,a1))+P5(f13(f18(a1,a1),f18(x82691,a2),a17),f18(a1,a1))),
% 117.16/117.69 inference(scs_inference,[],[223,5884,8082,6955,35,84])).
% 117.16/117.69 cnf(8913,plain,
% 117.16/117.69 (~P5(a17,f18(a1,a1))+P5(f13(f18(a2,a16),f18(a1,a1),a17),f18(a2,a16))),
% 117.16/117.69 inference(scs_inference,[],[423,5881,6032,35,84])).
% 117.16/117.69 cnf(9294,plain,
% 117.16/117.69 (P5(f3(x92941),f18(x92941,x92942))),
% 117.16/117.69 inference(rename_variables,[],[297])).
% 117.16/117.69 cnf(9299,plain,
% 117.16/117.69 (E(f13(x92991,f10(a16,a1),x92992),f13(x92991,f18(a1,a16),x92992))),
% 117.16/117.69 inference(rename_variables,[],[5795])).
% 117.16/117.69 cnf(9307,plain,
% 117.16/117.69 (P5(f3(x93071),f18(x93071,x93072))),
% 117.16/117.69 inference(rename_variables,[],[297])).
% 117.16/117.69 cnf(9315,plain,
% 117.16/117.69 (P5(f3(x93151),f18(x93151,x93152))),
% 117.16/117.69 inference(rename_variables,[],[297])).
% 117.16/117.69 cnf(9320,plain,
% 117.16/117.69 ($false),
% 117.16/117.69 inference(scs_inference,[],[45,44,48,46,5787,6211,297,9294,9307,9315,5809,6935,7052,5898,5813,5949,6109,6032,5848,6364,6830,7035,5789,6034,6798,6556,5896,7263,6055,5798,5795,9299,6187,7330,6384,6297,5805,54,73,56,2,92,12,53,74,91,4272,55,8913,8242,4123,8037,7995,7563,8269,4442,4448,4674,4252,4149,283,287,4104,463,473,39,62,93,33,41,35,58,38,61,36,40,37,3,81,82,80]),
% 117.16/117.69 ['proof']).
% 117.16/117.69 % SZS output end Proof
% 117.16/117.69 % Total time :116.380000s
%------------------------------------------------------------------------------