%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : GEO087+1 : TPTP v8.2.0. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% Computer : 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:44 EDT 2024
% Result : Theorem 59.55s 59.60s
% Output : CNFRefutation 59.55s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.13 % Problem : GEO087+1 : TPTP v8.2.0. Released v2.4.0.
% 0.03/0.13 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% 0.13/0.34 % Computer : n026.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 06:21:24 EDT 2024
% 0.13/0.34 % CPUTime :
% 0.53/0.56 start to proof:theBenchmark
% 59.55/59.59 %-------------------------------------------
% 59.55/59.59 % File :CSE---1.7
% 59.55/59.59 % Problem :theBenchmark
% 59.55/59.59 % Transform :cnf
% 59.55/59.59 % Format :tptp:raw
% 59.55/59.59 % Command :java -jar mcs_scs.jar %d %s
% 59.55/59.59
% 59.55/59.59 % Result :Theorem 58.980000s
% 59.55/59.59 % Output :CNFRefutation 58.980000s
% 59.55/59.59 %-------------------------------------------
% 59.55/59.60 %--------------------------------------------------------------------------
% 59.55/59.60 % File : GEO087+1 : TPTP v8.2.0. Released v2.4.0.
% 59.55/59.60 % Domain : Geometry (Oriented curves)
% 59.55/59.60 % Problem : If one curve is part of another curve then they cannot meet
% 59.55/59.60 % Version : [EHK99] axioms.
% 59.55/59.60 % English :
% 59.55/59.60
% 59.55/59.60 % Refs : [KE99] Kulik & Eschenbach (1999), A Geometry of Oriented Curv
% 59.55/59.60 % : [EHK99] Eschenbach et al. (1999), Representing Simple Trajecto
% 59.55/59.60 % Source : [KE99]
% 59.55/59.60 % Names : Corollary 2.9 [KE99]
% 59.55/59.60
% 59.55/59.60 % Status : Theorem
% 59.55/59.60 % Rating : 0.19 v7.5.0, 0.22 v7.4.0, 0.17 v7.1.0, 0.22 v7.0.0, 0.13 v6.4.0, 0.15 v6.3.0, 0.17 v6.2.0, 0.16 v6.1.0, 0.30 v6.0.0, 0.39 v5.5.0, 0.30 v5.4.0, 0.32 v5.3.0, 0.30 v5.2.0, 0.10 v5.0.0, 0.21 v4.1.0, 0.17 v4.0.1, 0.26 v4.0.0, 0.25 v3.7.0, 0.15 v3.5.0, 0.16 v3.4.0, 0.21 v3.3.0, 0.14 v3.2.0, 0.18 v3.1.0, 0.33 v2.7.0, 0.17 v2.5.0, 0.00 v2.4.0
% 59.55/59.60 % Syntax : Number of formulae : 17 ( 1 unt; 0 def)
% 59.55/59.60 % Number of atoms : 69 ( 10 equ)
% 59.55/59.60 % Maximal formula atoms : 12 ( 4 avg)
% 59.55/59.60 % Number of connectives : 57 ( 5 ~; 9 |; 21 &)
% 59.55/59.60 % ( 9 <=>; 13 =>; 0 <=; 0 <~>)
% 59.55/59.60 % Maximal formula depth : 12 ( 7 avg)
% 59.55/59.60 % Maximal term depth : 2 ( 1 avg)
% 59.55/59.60 % Number of predicates : 8 ( 7 usr; 0 prp; 1-3 aty)
% 59.55/59.60 % Number of functors : 1 ( 1 usr; 0 con; 2-2 aty)
% 59.55/59.60 % Number of variables : 56 ( 46 !; 10 ?)
% 59.55/59.60 % SPC : FOF_THM_RFO_SEQ
% 59.55/59.60
% 59.55/59.60 % Comments :
% 59.55/59.60 %--------------------------------------------------------------------------
% 59.55/59.60 %----Include simple curve axioms
% 59.55/59.60 include('Axioms/GEO004+0.ax').
% 59.55/59.60 %--------------------------------------------------------------------------
% 59.55/59.60 fof(corollary_2_9,conjecture,
% 59.55/59.60 ! [C1,C2] :
% 59.55/59.60 ( part_of(C1,C2)
% 59.55/59.60 => ~ ? [P] : meet(P,C1,C2) ) ).
% 59.55/59.60
% 59.55/59.60 %--------------------------------------------------------------------------
% 59.55/59.60 %-------------------------------------------
% 59.55/59.60 % Proof found
% 59.55/59.60 % SZS status Theorem for theBenchmark
% 59.55/59.60 % SZS output start Proof
% 59.55/59.61 %ClaNum:88(EqnAxiom:43)
% 59.55/59.61 %VarNum:331(SingletonVarNum:113)
% 59.55/59.61 %MaxLitNum:12
% 59.55/59.61 %MaxfuncDepth:2
% 59.55/59.61 %SharedTerms:5
% 59.55/59.61 %goalClause: 44 46
% 59.55/59.61 %singleGoalClaCount:2
% 59.55/59.61 [44]P1(a1,a6)
% 59.55/59.61 [46]P6(a8,a1,a6)
% 59.55/59.61 [45]P2(f7(x451),x451)
% 59.55/59.61 [47]P3(x471)+P4(f9(x471),x471)
% 59.55/59.61 [49]~P7(x491)+P4(f15(x491),x491)
% 59.55/59.61 [48]P7(x481)+~P4(x482,x481)
% 59.55/59.61 [51]~P3(x511)+~P4(x512,x511)
% 59.55/59.61 [52]~P4(x521,x522)+P5(x521,x522)
% 59.55/59.61 [53]~P2(x531,x532)+P5(x531,x532)
% 59.55/59.61 [54]~P2(x541,x542)+~P4(x541,x542)
% 59.55/59.61 [55]~P4(x552,x551)+~E(f2(x551,x552),x552)
% 59.55/59.61 [57]P1(x571,x572)+P5(f10(x572,x571),x571)
% 59.55/59.61 [61]~P4(x612,x611)+P4(f2(x611,x612),x611)
% 59.55/59.61 [68]P1(x681,x682)+~P5(f10(x682,x681),x682)
% 59.55/59.61 [75]~P2(x751,x752)+P6(x751,f17(x752,x751),f3(x752,x751))
% 59.55/59.61 [70]~P2(x702,x701)+E(f16(f17(x701,x702),f3(x701,x702)),x701)
% 59.55/59.61 [71]P5(x711,x712)+~P6(x711,x713,x712)
% 59.55/59.61 [72]P5(x721,x722)+~P6(x721,x722,x723)
% 59.55/59.61 [73]~P6(x733,x731,x732)+E(f5(x731,x732),f16(x731,x732))
% 59.55/59.61 [50]P7(x501)+~P1(x501,x502)+E(x501,x502)
% 59.55/59.61 [56]P2(x561,x562)+~P5(x561,x562)+P4(x561,x562)
% 59.55/59.61 [64]~P5(x641,x642)+P4(x641,x642)+P5(x641,f11(x641,x642))
% 59.55/59.61 [65]~P5(x651,x652)+P4(x651,x652)+P5(x651,f13(x651,x652))
% 59.55/59.61 [66]~P5(x661,x662)+P4(x661,x662)+P1(f11(x661,x662),x662)
% 59.55/59.61 [67]~P5(x671,x672)+P4(x671,x672)+P1(f13(x671,x672),x672)
% 59.55/59.61 [69]E(x691,x692)+P5(f4(x691,x692),x692)+P5(f4(x691,x692),x691)
% 59.55/59.61 [74]E(x741,x742)+~P5(f4(x741,x742),x742)+~P5(f4(x741,x742),x741)
% 59.55/59.61 [76]~P5(x761,x762)+P4(x761,x762)+~P1(f11(x761,x762),f13(x761,x762))
% 59.55/59.61 [77]~P5(x771,x772)+P4(x771,x772)+~P1(f13(x771,x772),f11(x771,x772))
% 59.55/59.61 [58]~P5(x581,x583)+P5(x581,x582)+~P1(x583,x582)
% 59.55/59.61 [86]~P5(f12(x861,x862,x863),x863)+~P5(f12(x861,x862,x863),x861)+E(x861,f16(x862,x863))
% 59.55/59.61 [87]~P5(f12(x871,x872,x873),x872)+~P5(f12(x871,x872,x873),x871)+E(x871,f16(x872,x873))
% 59.55/59.61 [59]~P5(x591,x594)+P5(x591,x592)+~E(x592,f16(x593,x594))
% 59.55/59.61 [60]~P5(x601,x603)+P5(x601,x602)+~E(x602,f16(x603,x604))
% 59.55/59.61 [82]~P5(x821,x823)+~P5(x821,x822)+P6(x821,x822,x823)+P5(f14(x821,x822,x823),x823)
% 59.55/59.61 [83]~P5(x831,x833)+~P5(x831,x832)+P6(x831,x832,x833)+P5(f14(x831,x832,x833),x832)
% 59.55/59.61 [85]P5(f12(x851,x852,x853),x853)+P5(f12(x851,x852,x853),x852)+P5(f12(x851,x852,x853),x851)+E(x851,f16(x852,x853))
% 59.55/59.61 [79]~P5(x791,x792)+P4(x791,x792)+~P6(x794,x793,x792)+~P5(x791,x793)
% 59.55/59.61 [80]~P5(x801,x802)+P4(x801,x802)+~P6(x804,x802,x803)+~P5(x801,x803)
% 59.55/59.61 [63]~P5(x631,x634)+P5(x631,x632)+P5(x631,x633)+~E(x634,f16(x633,x632))
% 59.55/59.61 [88]~P5(x881,x883)+~P5(x881,x882)+P6(x881,x882,x883)+~P4(f14(x881,x882,x883),x883)+~P4(f14(x881,x882,x883),x882)
% 59.55/59.61 [81]~P3(x814)+~P4(x811,x812)+P6(x811,x812,x813)+~P6(x815,x812,x813)+~E(x814,f16(x812,x813))
% 59.55/59.61 [62]E(x623,x621)+~P4(x621,x624)+~P4(x623,x624)+E(x621,x622)+E(x623,x622)+~P4(x622,x624)
% 59.55/59.61 [78]P1(x782,x781)+~P1(x782,x783)+~P5(x784,x782)+~P4(x784,x783)+P1(x781,x782)+~P1(x781,x783)+~P5(x784,x781)
% 59.55/59.61 [84]P1(x842,x841)+P1(x842,x843)+P1(x843,x841)+P1(x843,x842)+~P1(x842,x844)+~P1(x843,x844)+~P4(x845,x842)+~P4(x845,x843)+P1(x841,x842)+P1(x841,x843)+~P1(x841,x844)+~P4(x845,x841)
% 59.55/59.61 %EqnAxiom
% 59.55/59.61 [1]E(x11,x11)
% 59.55/59.61 [2]E(x22,x21)+~E(x21,x22)
% 59.55/59.61 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 59.55/59.61 [4]~E(x41,x42)+E(f7(x41),f7(x42))
% 59.55/59.61 [5]~E(x51,x52)+E(f9(x51),f9(x52))
% 59.55/59.61 [6]~E(x61,x62)+E(f15(x61),f15(x62))
% 59.55/59.61 [7]~E(x71,x72)+E(f2(x71,x73),f2(x72,x73))
% 59.55/59.61 [8]~E(x81,x82)+E(f2(x83,x81),f2(x83,x82))
% 59.55/59.61 [9]~E(x91,x92)+E(f10(x91,x93),f10(x92,x93))
% 59.55/59.61 [10]~E(x101,x102)+E(f10(x103,x101),f10(x103,x102))
% 59.55/59.61 [11]~E(x111,x112)+E(f16(x111,x113),f16(x112,x113))
% 59.55/59.61 [12]~E(x121,x122)+E(f16(x123,x121),f16(x123,x122))
% 59.55/59.61 [13]~E(x131,x132)+E(f12(x131,x133,x134),f12(x132,x133,x134))
% 59.55/59.61 [14]~E(x141,x142)+E(f12(x143,x141,x144),f12(x143,x142,x144))
% 59.55/59.61 [15]~E(x151,x152)+E(f12(x153,x154,x151),f12(x153,x154,x152))
% 59.55/59.61 [16]~E(x161,x162)+E(f14(x161,x163,x164),f14(x162,x163,x164))
% 59.55/59.61 [17]~E(x171,x172)+E(f14(x173,x171,x174),f14(x173,x172,x174))
% 59.55/59.61 [18]~E(x181,x182)+E(f14(x183,x184,x181),f14(x183,x184,x182))
% 59.55/59.61 [19]~E(x191,x192)+E(f13(x191,x193),f13(x192,x193))
% 59.55/59.61 [20]~E(x201,x202)+E(f13(x203,x201),f13(x203,x202))
% 59.55/59.61 [21]~E(x211,x212)+E(f11(x211,x213),f11(x212,x213))
% 59.55/59.61 [22]~E(x221,x222)+E(f11(x223,x221),f11(x223,x222))
% 59.55/59.61 [23]~E(x231,x232)+E(f3(x231,x233),f3(x232,x233))
% 59.55/59.61 [24]~E(x241,x242)+E(f3(x243,x241),f3(x243,x242))
% 59.55/59.61 [25]~E(x251,x252)+E(f4(x251,x253),f4(x252,x253))
% 59.55/59.61 [26]~E(x261,x262)+E(f4(x263,x261),f4(x263,x262))
% 59.55/59.61 [27]~E(x271,x272)+E(f17(x271,x273),f17(x272,x273))
% 59.55/59.61 [28]~E(x281,x282)+E(f17(x283,x281),f17(x283,x282))
% 59.55/59.61 [29]~E(x291,x292)+E(f5(x291,x293),f5(x292,x293))
% 59.55/59.61 [30]~E(x301,x302)+E(f5(x303,x301),f5(x303,x302))
% 59.55/59.61 [31]P1(x312,x313)+~E(x311,x312)+~P1(x311,x313)
% 59.55/59.61 [32]P1(x323,x322)+~E(x321,x322)+~P1(x323,x321)
% 59.55/59.61 [33]P2(x332,x333)+~E(x331,x332)+~P2(x331,x333)
% 59.55/59.61 [34]P2(x343,x342)+~E(x341,x342)+~P2(x343,x341)
% 59.55/59.61 [35]P6(x352,x353,x354)+~E(x351,x352)+~P6(x351,x353,x354)
% 59.55/59.61 [36]P6(x363,x362,x364)+~E(x361,x362)+~P6(x363,x361,x364)
% 59.55/59.61 [37]P6(x373,x374,x372)+~E(x371,x372)+~P6(x373,x374,x371)
% 59.55/59.61 [38]~P3(x381)+P3(x382)+~E(x381,x382)
% 59.55/59.61 [39]P4(x392,x393)+~E(x391,x392)+~P4(x391,x393)
% 59.55/59.61 [40]P4(x403,x402)+~E(x401,x402)+~P4(x403,x401)
% 59.55/59.61 [41]~P7(x411)+P7(x412)+~E(x411,x412)
% 59.55/59.61 [42]P5(x422,x423)+~E(x421,x422)+~P5(x421,x423)
% 59.55/59.61 [43]P5(x433,x432)+~E(x431,x432)+~P5(x433,x431)
% 59.55/59.61
% 59.55/59.61 %-------------------------------------------
% 59.55/59.62 cnf(89,plain,
% 59.55/59.62 (~P5(x891,x892)+P5(x891,f16(x893,x892))),
% 59.55/59.62 inference(equality_inference,[],[59])).
% 59.55/59.62 cnf(90,plain,
% 59.55/59.62 (~P5(x901,x902)+P5(x901,f16(x902,x903))),
% 59.55/59.62 inference(equality_inference,[],[60])).
% 59.55/59.62 cnf(91,plain,
% 59.55/59.62 (~P5(x911,f16(x912,x913))+P5(x911,x913)+P5(x911,x912)),
% 59.55/59.62 inference(equality_inference,[],[63])).
% 59.55/59.62 cnf(92,plain,
% 59.55/59.62 (~P3(f16(x921,x922))+P6(x923,x921,x922)+~P4(x923,x921)+~P6(x924,x921,x922)),
% 59.55/59.62 inference(equality_inference,[],[81])).
% 59.55/59.62 cnf(93,plain,
% 59.55/59.62 (~P5(x931,a1)+P5(x931,a6)),
% 59.55/59.62 inference(scs_inference,[],[44,58])).
% 59.55/59.62 cnf(95,plain,
% 59.55/59.62 (~P5(x951,f16(a1,a1))+P5(x951,a6)),
% 59.55/59.62 inference(scs_inference,[],[44,58,91])).
% 59.55/59.62 cnf(116,plain,
% 59.55/59.62 (P2(f7(x1161),x1162)+~E(x1161,x1162)),
% 59.55/59.62 inference(scs_inference,[],[45,34])).
% 59.55/59.62 cnf(117,plain,
% 59.55/59.62 (P6(a8,a1,x1171)+~E(a6,x1171)),
% 59.55/59.62 inference(scs_inference,[],[46,45,34,37])).
% 59.55/59.62 cnf(121,plain,
% 59.55/59.62 (P1(a1,x1211)+~E(a6,x1211)),
% 59.55/59.62 inference(scs_inference,[],[44,46,45,34,37,31,33,36,32])).
% 59.55/59.62 cnf(128,plain,
% 59.55/59.62 (P6(x1281,a1,a6)+~E(a8,x1281)),
% 59.55/59.62 inference(scs_inference,[],[46,35])).
% 59.55/59.62 cnf(131,plain,
% 59.55/59.62 (~P4(x1311,x1312)+P4(f15(x1312),x1312)),
% 59.55/59.62 inference(scs_inference,[],[48,49])).
% 59.55/59.62 cnf(132,plain,
% 59.55/59.62 (~P4(x1321,x1322)+P4(f9(x1322),x1322)),
% 59.55/59.62 inference(scs_inference,[],[51,47])).
% 59.55/59.62 cnf(133,plain,
% 59.55/59.62 (~P2(f2(x1331,x1332),x1331)+~P4(x1332,x1331)),
% 59.55/59.62 inference(scs_inference,[],[54,61])).
% 59.55/59.62 cnf(135,plain,
% 59.55/59.62 (P5(f15(x1351),x1351)+~P4(x1352,x1351)),
% 59.55/59.62 inference(scs_inference,[],[131,52])).
% 59.55/59.62 cnf(136,plain,
% 59.55/59.62 (~P4(x1361,x1362)+~E(f2(x1362,f9(x1362)),f9(x1362))),
% 59.55/59.62 inference(scs_inference,[],[132,55])).
% 59.55/59.62 cnf(137,plain,
% 59.55/59.62 (~P4(x1371,x1372)+P5(f15(x1372),f16(x1373,x1372))),
% 59.55/59.62 inference(scs_inference,[],[135,89])).
% 59.55/59.62 cnf(139,plain,
% 59.55/59.62 (E(f9(f5(a1,a6)),f9(f16(a1,a6)))),
% 59.55/59.62 inference(scs_inference,[],[46,5,73])).
% 59.55/59.62 cnf(140,plain,
% 59.55/59.62 (E(f9(f16(a1,a6)),f9(f5(a1,a6)))),
% 59.55/59.62 inference(scs_inference,[],[139,2])).
% 59.55/59.62 cnf(147,plain,
% 59.55/59.62 (P5(f7(x1471),f16(x1471,x1472))),
% 59.55/59.62 inference(scs_inference,[],[45,90,53])).
% 59.55/59.62 cnf(163,plain,
% 59.55/59.62 (P5(f7(f16(a1,a1)),a6)),
% 59.55/59.62 inference(scs_inference,[],[45,95,53])).
% 59.55/59.62 cnf(164,plain,
% 59.55/59.62 (P5(f7(f16(a1,a1)),f16(x1641,a6))),
% 59.55/59.62 inference(scs_inference,[],[163,89])).
% 59.55/59.62 cnf(170,plain,
% 59.55/59.62 (P5(f15(a6),f16(x1701,a6))+P2(f7(f16(a1,a1)),a6)),
% 59.55/59.62 inference(scs_inference,[],[163,89,90,56,137])).
% 59.55/59.62 cnf(231,plain,
% 59.55/59.62 (P5(f7(f16(a1,a1)),x2311)+~E(f16(x2312,a6),x2311)),
% 59.55/59.62 inference(scs_inference,[],[164,43])).
% 59.55/59.62 cnf(232,plain,
% 59.55/59.62 (P5(f7(f16(a1,a1)),f16(x2321,x2322))+~E(f16(x2323,a6),x2322)),
% 59.55/59.62 inference(scs_inference,[],[164,43,89])).
% 59.55/59.62 cnf(234,plain,
% 59.55/59.62 (P5(f7(f16(a1,a1)),f16(x2341,x2342))+~E(f16(x2343,a6),x2341)),
% 59.55/59.62 inference(scs_inference,[],[164,43,89,90])).
% 59.55/59.62 cnf(249,plain,
% 59.55/59.62 (P5(f7(x2491),x2492)+~E(f16(x2491,x2493),x2492)),
% 59.55/59.62 inference(scs_inference,[],[147,43])).
% 59.55/59.62 cnf(391,plain,
% 59.55/59.62 (~E(f9(x3911),f2(x3911,f9(x3911)))+~P4(x3912,x3911)),
% 59.55/59.62 inference(scs_inference,[],[136,2])).
% 59.55/59.62 cnf(407,plain,
% 59.55/59.62 (P2(x4071,a6)+~E(f7(f16(a1,a1)),x4071)+P5(f15(a6),f16(x4072,a6))),
% 59.55/59.62 inference(scs_inference,[],[170,33])).
% 59.55/59.62 cnf(468,plain,
% 59.55/59.62 (P4(f9(f5(a1,a6)),f16(a1,a6))+P3(f16(a1,a6))),
% 59.55/59.62 inference(scs_inference,[],[140,39,47])).
% 59.55/59.62 cnf(507,plain,
% 59.55/59.62 (P7(x5071)+P3(x5071)),
% 59.55/59.62 inference(scs_inference,[],[48,47])).
% 59.55/59.62 cnf(510,plain,
% 59.55/59.62 (P3(x5101)+P4(f15(x5101),x5101)),
% 59.55/59.62 inference(scs_inference,[],[507,49])).
% 59.55/59.62 cnf(522,plain,
% 59.55/59.62 (~P4(x5221,a1)+P7(f16(a1,a6))+P6(x5221,a1,a6)),
% 59.55/59.62 inference(scs_inference,[],[46,507,92])).
% 59.55/59.62 cnf(523,plain,
% 59.55/59.62 (P3(a1)+P7(f16(a1,a6))+P6(f9(a1),a1,a6)),
% 59.55/59.62 inference(scs_inference,[],[522,47])).
% 59.55/59.62 cnf(524,plain,
% 59.55/59.62 (P4(f15(f16(a1,a6)),f16(a1,a6))+P6(f9(a1),a1,a6)+P3(a1)),
% 59.55/59.62 inference(scs_inference,[],[523,49])).
% 59.55/59.62 cnf(525,plain,
% 59.55/59.62 (~P3(f16(a1,a6))+P6(f9(a1),a1,a6)+P3(a1)),
% 59.55/59.62 inference(scs_inference,[],[524,51])).
% 59.55/59.62 cnf(526,plain,
% 59.55/59.62 (P4(f9(f5(a1,a6)),f16(a1,a6))+P6(f9(a1),a1,a6)+P3(a1)),
% 59.55/59.62 inference(scs_inference,[],[525,468])).
% 59.55/59.62 cnf(569,plain,
% 59.55/59.62 (~P3(x5691)+~P7(x5691)),
% 59.55/59.62 inference(scs_inference,[],[51,49])).
% 59.55/59.62 cnf(572,plain,
% 59.55/59.62 (~P7(x5721)+P4(f9(x5721),x5721)),
% 59.55/59.62 inference(scs_inference,[],[569,47])).
% 59.55/59.62 cnf(573,plain,
% 59.55/59.62 (P5(f9(x5731),x5731)+~P7(x5731)),
% 59.55/59.62 inference(scs_inference,[],[572,52])).
% 59.55/59.62 cnf(574,plain,
% 59.55/59.62 (P5(f9(x5741),x5741)+~P4(x5742,x5741)),
% 59.55/59.62 inference(scs_inference,[],[573,48])).
% 59.55/59.62 cnf(575,plain,
% 59.55/59.62 (~P4(x5751,x5752)+P5(f9(x5752),f16(x5753,x5752))),
% 59.55/59.62 inference(scs_inference,[],[574,89])).
% 59.55/59.62 cnf(576,plain,
% 59.55/59.62 (P5(f9(x5761),f16(x5762,x5761))+~P7(x5761)),
% 59.55/59.62 inference(scs_inference,[],[575,49])).
% 59.55/59.62 cnf(593,plain,
% 59.55/59.62 (~P7(a1)+P7(f16(a1,a6))+P6(f9(a1),a1,a6)),
% 59.55/59.62 inference(scs_inference,[],[569,523])).
% 59.55/59.62 cnf(594,plain,
% 59.55/59.62 (P4(f15(f16(a1,a6)),f16(a1,a6))+P6(f9(a1),a1,a6)+~P7(a1)),
% 59.55/59.62 inference(scs_inference,[],[593,49])).
% 59.55/59.62 cnf(603,plain,
% 59.55/59.62 (~P7(a1)+P4(f9(f5(a1,a6)),f16(a1,a6))+P6(f9(a1),a1,a6)),
% 59.55/59.62 inference(scs_inference,[],[569,526])).
% 59.55/59.62 cnf(604,plain,
% 59.55/59.62 (P5(f9(f5(a1,a6)),f16(a1,a6))+P6(f9(a1),a1,a6)+~P7(a1)),
% 59.55/59.62 inference(scs_inference,[],[603,52])).
% 59.55/59.62 cnf(605,plain,
% 59.55/59.62 (P5(f9(f5(a1,a6)),f16(x6051,f16(a1,a6)))+P6(f9(a1),a1,a6)+~P7(a1)),
% 59.55/59.62 inference(scs_inference,[],[604,89])).
% 59.55/59.62 cnf(628,plain,
% 59.55/59.62 (E(a1,a6)+~P3(a1)),
% 59.55/59.62 inference(scs_inference,[],[44,569,50])).
% 59.55/59.62 cnf(629,plain,
% 59.55/59.62 (E(a6,a1)+~P3(a1)),
% 59.55/59.62 inference(scs_inference,[],[628,2])).
% 59.55/59.62 cnf(634,plain,
% 59.55/59.62 (~P3(f16(a1,a6))+~P4(x6341,a1)+P6(x6341,a1,a6)),
% 59.55/59.62 inference(scs_inference,[],[569,522])).
% 59.55/59.62 cnf(843,plain,
% 59.55/59.62 (~P3(a1)+P3(a6)),
% 59.55/59.62 inference(scs_inference,[],[628,38])).
% 59.55/59.62 cnf(844,plain,
% 59.55/59.62 (P4(f9(a1),a1)+P3(a6)),
% 59.55/59.62 inference(scs_inference,[],[843,47])).
% 59.55/59.62 cnf(845,plain,
% 59.55/59.62 (P7(a1)+P3(a6)),
% 59.55/59.62 inference(scs_inference,[],[844,48])).
% 59.55/59.62 cnf(846,plain,
% 59.55/59.62 (P4(f15(a1),a1)+P3(a6)),
% 59.55/59.62 inference(scs_inference,[],[845,49])).
% 59.55/59.62 cnf(847,plain,
% 59.55/59.62 (P5(f15(a1),a1)+P3(a6)),
% 59.55/59.62 inference(scs_inference,[],[846,52])).
% 59.55/59.62 cnf(848,plain,
% 59.55/59.62 (P5(f15(a1),f16(x8481,a1))+P3(a6)),
% 59.55/59.62 inference(scs_inference,[],[847,89])).
% 59.55/59.62 cnf(851,plain,
% 59.55/59.62 (~P4(x8511,a6)+~P3(a1)),
% 59.55/59.62 inference(scs_inference,[],[843,51])).
% 59.55/59.62 cnf(852,plain,
% 59.55/59.62 (~P7(a6)+~P3(a1)),
% 59.55/59.62 inference(scs_inference,[],[851,49])).
% 59.55/59.62 cnf(899,plain,
% 59.55/59.62 (E(a6,x8991)+~P1(a6,x8991)+~P3(a1)),
% 59.55/59.62 inference(scs_inference,[],[852,50])).
% 59.55/59.62 cnf(981,plain,
% 59.55/59.62 (P6(a8,a1,a1)+~P3(a1)),
% 59.55/59.62 inference(scs_inference,[],[629,117])).
% 59.55/59.62 cnf(982,plain,
% 59.55/59.62 (P5(a8,a1)+~P3(a1)),
% 59.55/59.62 inference(scs_inference,[],[981,71])).
% 59.55/59.62 cnf(988,plain,
% 59.55/59.62 (P1(a1,a1)+~P3(a1)),
% 59.55/59.62 inference(scs_inference,[],[629,121])).
% 59.55/59.62 cnf(989,plain,
% 59.55/59.62 (P1(x9891,a1)+~E(a1,x9891)+~P3(a1)),
% 59.55/59.62 inference(scs_inference,[],[988,31])).
% 59.55/59.62 cnf(1253,plain,
% 59.55/59.62 (P4(f9(a1),a1)+~P4(x12531,a6)),
% 59.55/59.62 inference(scs_inference,[],[851,47])).
% 59.55/59.62 cnf(1254,plain,
% 59.55/59.62 (P5(f9(a1),a1)+~P4(x12541,a6)),
% 59.55/59.62 inference(scs_inference,[],[1253,52])).
% 59.55/59.62 cnf(1255,plain,
% 59.55/59.62 (P5(f9(a1),f16(x12551,a1))+~P4(x12552,a6)),
% 59.55/59.62 inference(scs_inference,[],[1254,89])).
% 59.55/59.62 cnf(1256,plain,
% 59.55/59.62 (P5(f9(a1),f16(f16(x12561,a1),x12562))+~P4(x12563,a6)),
% 59.55/59.62 inference(scs_inference,[],[1255,90])).
% 59.55/59.62 cnf(1259,plain,
% 59.55/59.62 (P4(f15(a1),a1)+~P4(x12591,a6)),
% 59.55/59.62 inference(scs_inference,[],[851,510])).
% 59.55/59.62 cnf(1260,plain,
% 59.55/59.62 (P5(f15(a1),a1)+~P4(x12601,a6)),
% 59.55/59.62 inference(scs_inference,[],[1259,52])).
% 59.55/59.62 cnf(1261,plain,
% 59.55/59.62 (P5(f15(a1),f16(x12611,a1))+~P4(x12612,a6)),
% 59.55/59.62 inference(scs_inference,[],[1260,89])).
% 59.55/59.62 cnf(1262,plain,
% 59.55/59.62 (P5(f15(a1),f16(f16(x12621,a1),x12622))+~P4(x12623,a6)),
% 59.55/59.62 inference(scs_inference,[],[1261,90])).
% 59.55/59.62 cnf(1323,plain,
% 59.55/59.62 (P4(a8,a1)+~P6(x13231,a1,a1)+~P3(a1)),
% 59.55/59.62 inference(scs_inference,[],[982,79])).
% 59.55/59.62 cnf(1324,plain,
% 59.55/59.62 (~E(a6,a1)+P4(a8,a1)+~P3(a1)),
% 59.55/59.62 inference(scs_inference,[],[46,1323,37])).
% 59.55/59.62 cnf(1325,plain,
% 59.55/59.62 (~P1(a6,a1)+P4(a8,a1)+~P3(a1)),
% 59.55/59.62 inference(scs_inference,[],[1324,899])).
% 59.55/59.62 cnf(1326,plain,
% 59.55/59.62 (~E(a1,a6)+P4(a8,a1)+~P3(a1)),
% 59.55/59.62 inference(scs_inference,[],[1325,989])).
% 59.55/59.62 cnf(1327,plain,
% 59.55/59.62 (P7(a1)+P4(a8,a1)+~P3(a1)),
% 59.55/59.62 inference(scs_inference,[],[44,1326,50])).
% 59.55/59.62 cnf(1328,plain,
% 59.55/59.62 (P7(a1)+~P3(a1)),
% 59.55/59.62 inference(scs_inference,[],[1327,48])).
% 59.55/59.62 cnf(1329,plain,
% 59.55/59.62 (P4(f15(a1),a1)+~P3(a1)),
% 59.55/59.62 inference(scs_inference,[],[1328,49])).
% 59.55/59.63 cnf(1330,plain,
% 59.55/59.63 (~P3(a1)),
% 59.55/59.63 inference(scs_inference,[],[1329,51])).
% 59.55/59.63 cnf(1337,plain,
% 59.55/59.63 (P7(a1)),
% 59.55/59.63 inference(scs_inference,[],[1330,507])).
% 59.55/59.63 cnf(1339,plain,
% 59.55/59.63 (P5(f9(a1),a1)),
% 59.55/59.63 inference(scs_inference,[],[1330,507,573])).
% 59.55/59.63 cnf(1347,plain,
% 59.55/59.63 (P5(f9(a1),a6)),
% 59.55/59.63 inference(scs_inference,[],[44,1330,507,573,576,90,89,58])).
% 59.55/59.63 cnf(1357,plain,
% 59.55/59.63 (P2(f9(a1),a1)+~E(f7(a1),f2(a1,f9(a1)))),
% 59.55/59.63 inference(scs_inference,[],[45,44,1330,507,573,576,90,89,58,56,133,137,54,593,594,603,604,605,40,39,33])).
% 59.55/59.63 cnf(1377,plain,
% 59.55/59.63 (P2(f9(a1),a6)+P4(f15(a1),a1)),
% 59.55/59.63 inference(scs_inference,[],[1347,90,89,56,575,1256,1259])).
% 59.55/59.63 cnf(1393,plain,
% 59.55/59.63 (P2(f9(a1),a6)+~E(f7(a6),f2(a6,f9(a1)))),
% 59.55/59.63 inference(scs_inference,[],[45,1347,140,90,89,56,575,1256,1259,1261,1262,1253,1260,133,137,54,407,40,39,41,33])).
% 59.55/59.63 cnf(1714,plain,
% 59.55/59.63 (P2(f9(a1),a6)+~E(f2(a1,f15(a1)),f15(a1))),
% 59.55/59.63 inference(scs_inference,[],[1377,55])).
% 59.55/59.63 cnf(1734,plain,
% 59.55/59.63 (~P4(f9(a1),a1)+~E(f7(a1),f2(a1,f9(a1)))),
% 59.55/59.63 inference(scs_inference,[],[1357,54])).
% 59.55/59.63 cnf(1736,plain,
% 59.55/59.63 (~P4(f9(a1),a6)+~E(f7(a6),f2(a6,f9(a1)))),
% 59.55/59.63 inference(scs_inference,[],[1393,54])).
% 59.55/59.63 cnf(1737,plain,
% 59.55/59.63 (~P4(f9(a1),a6)+~E(f2(a1,f15(a1)),f15(a1))),
% 59.55/59.63 inference(scs_inference,[],[1714,54])).
% 59.55/59.63 cnf(1739,plain,
% 59.55/59.63 (~E(f7(a1),f2(a1,f9(a1)))),
% 59.55/59.63 inference(scs_inference,[],[1330,1734,47])).
% 59.55/59.63 cnf(1886,plain,
% 59.55/59.63 (E(f16(a1,a6),f5(a1,a6))),
% 59.55/59.63 inference(scs_inference,[],[46,2,73])).
% 59.55/59.63 cnf(1888,plain,
% 59.55/59.63 (P2(f7(f16(a1,a6)),f5(a1,a6))),
% 59.55/59.63 inference(scs_inference,[],[1886,116])).
% 59.55/59.63 cnf(1893,plain,
% 59.55/59.63 (P5(f7(f16(a1,a1)),f5(a1,a6))),
% 59.55/59.63 inference(scs_inference,[],[1886,116,232,234,231])).
% 59.55/59.63 cnf(1894,plain,
% 59.55/59.63 (E(f5(a1,a6),f16(a1,a6))),
% 59.55/59.63 inference(scs_inference,[],[1886,116,232,234,231,2])).
% 59.55/59.63 cnf(1911,plain,
% 59.55/59.63 (P2(f7(f5(a1,a6)),f16(a1,a6))),
% 59.55/59.63 inference(scs_inference,[],[1894,116])).
% 59.55/59.63 cnf(3713,plain,
% 59.55/59.63 (P4(f15(a1),a1)),
% 59.55/59.63 inference(scs_inference,[],[1337,1330,47,49])).
% 59.55/59.63 cnf(3719,plain,
% 59.55/59.63 (P4(f2(a1,f9(a1)),a1)),
% 59.55/59.63 inference(scs_inference,[],[1337,1330,47,49,135,55,61])).
% 59.55/59.63 cnf(3722,plain,
% 59.55/59.63 (P5(f7(a1),a6)),
% 59.55/59.63 inference(scs_inference,[],[1337,1330,1886,147,47,49,135,55,61,6,95])).
% 59.55/59.63 cnf(3755,plain,
% 59.55/59.63 (P5(a8,a6)),
% 59.55/59.63 inference(scs_inference,[],[1337,1330,1888,1886,147,45,46,47,49,135,55,61,6,95,7,8,9,10,11,12,19,20,21,22,23,24,25,26,27,28,29,30,75,391,13,14,15,16,17,18,53,71])).
% 59.55/59.63 cnf(3757,plain,
% 59.55/59.63 (P5(f2(a1,f9(a1)),a1)),
% 59.55/59.63 inference(scs_inference,[],[1337,1330,1888,1886,147,45,46,47,49,135,55,61,6,95,7,8,9,10,11,12,19,20,21,22,23,24,25,26,27,28,29,30,75,391,13,14,15,16,17,18,53,71,52])).
% 59.55/59.63 cnf(3759,plain,
% 59.55/59.63 (P5(a8,a1)),
% 59.55/59.63 inference(scs_inference,[],[1337,1330,1888,1886,147,45,46,47,49,135,55,61,6,95,7,8,9,10,11,12,19,20,21,22,23,24,25,26,27,28,29,30,75,391,13,14,15,16,17,18,53,71,52,72])).
% 59.55/59.63 cnf(3771,plain,
% 59.55/59.63 (P5(f15(a1),f5(a1,a6))),
% 59.55/59.63 inference(scs_inference,[],[1337,1330,1888,1886,147,1739,45,46,1894,47,49,135,55,61,6,95,7,8,9,10,11,12,19,20,21,22,23,24,25,26,27,28,29,30,75,391,13,14,15,16,17,18,53,71,52,72,54,2,4,66,67,59,60])).
% 59.55/59.63 cnf(3773,plain,
% 59.55/59.63 (P5(f15(a1),a6)),
% 59.55/59.63 inference(scs_inference,[],[44,1337,1330,1888,1886,147,1739,45,46,1894,47,49,135,55,61,6,95,7,8,9,10,11,12,19,20,21,22,23,24,25,26,27,28,29,30,75,391,13,14,15,16,17,18,53,71,52,72,54,2,4,66,67,59,60,58])).
% 59.55/59.63 cnf(3777,plain,
% 59.55/59.63 (P4(f9(a1),a6)),
% 59.55/59.63 inference(scs_inference,[],[44,1337,1330,1888,1339,1347,1886,147,1739,45,46,1894,47,49,135,55,61,6,95,7,8,9,10,11,12,19,20,21,22,23,24,25,26,27,28,29,30,75,391,13,14,15,16,17,18,53,71,52,72,54,2,4,66,67,59,60,58,40,3,79])).
% 59.55/59.63 cnf(3779,plain,
% 59.55/59.63 (~P6(x37791,f5(a1,a6),f5(a1,a6))),
% 59.55/59.63 inference(scs_inference,[],[44,1337,1330,1888,1339,1347,1886,147,1739,45,46,1894,47,49,135,55,61,6,95,7,8,9,10,11,12,19,20,21,22,23,24,25,26,27,28,29,30,75,391,13,14,15,16,17,18,53,71,52,72,54,2,4,66,67,59,60,58,40,3,79,80])).
% 59.55/59.63 cnf(3783,plain,
% 59.55/59.63 (P5(f2(a1,f9(a1)),a6)),
% 59.55/59.63 inference(scs_inference,[],[44,1337,1330,1893,1888,1339,1347,1886,147,1739,45,46,1894,47,49,135,55,61,6,95,7,8,9,10,11,12,19,20,21,22,23,24,25,26,27,28,29,30,75,391,13,14,15,16,17,18,53,71,52,72,54,2,4,66,67,59,60,58,40,3,79,80,82,93])).
% 59.55/59.63 cnf(3785,plain,
% 59.55/59.63 (P4(f15(a6),a6)),
% 59.55/59.63 inference(scs_inference,[],[44,1337,1330,1893,1888,1339,1347,1886,147,1739,45,46,1894,47,49,135,55,61,6,95,7,8,9,10,11,12,19,20,21,22,23,24,25,26,27,28,29,30,75,391,13,14,15,16,17,18,53,71,52,72,54,2,4,66,67,59,60,58,40,3,79,80,82,93,131])).
% 59.55/59.63 cnf(3787,plain,
% 59.55/59.63 (P4(f9(a6),a6)),
% 59.55/59.63 inference(scs_inference,[],[44,1337,1330,1893,1888,1339,1347,1886,147,1739,45,46,1894,47,49,135,55,61,6,95,7,8,9,10,11,12,19,20,21,22,23,24,25,26,27,28,29,30,75,391,13,14,15,16,17,18,53,71,52,72,54,2,4,66,67,59,60,58,40,3,79,80,82,93,131,132])).
% 59.55/59.63 cnf(3794,plain,
% 59.55/59.63 (~E(f7(a6),f2(a6,f9(a1)))),
% 59.55/59.63 inference(scs_inference,[],[44,1337,1330,1893,1888,1339,1347,1886,147,1739,45,46,1894,47,49,135,55,61,6,95,7,8,9,10,11,12,19,20,21,22,23,24,25,26,27,28,29,30,75,391,13,14,15,16,17,18,53,71,52,72,54,2,4,66,67,59,60,58,40,3,79,80,82,93,131,132,574,249,136,1736])).
% 59.55/59.63 cnf(3795,plain,
% 59.55/59.63 (~E(f2(a1,f15(a1)),f15(a1))),
% 59.55/59.63 inference(scs_inference,[],[44,1337,1330,1893,1888,1339,1347,1886,147,1739,45,46,1894,47,49,135,55,61,6,95,7,8,9,10,11,12,19,20,21,22,23,24,25,26,27,28,29,30,75,391,13,14,15,16,17,18,53,71,52,72,54,2,4,66,67,59,60,58,40,3,79,80,82,93,131,132,574,249,136,1736,1737])).
% 59.55/59.63 cnf(3798,plain,
% 59.55/59.63 (~P3(a6)),
% 59.55/59.63 inference(scs_inference,[],[44,1337,1330,1893,1888,1339,1347,1886,147,1739,45,46,1894,47,49,135,55,61,6,95,7,8,9,10,11,12,19,20,21,22,23,24,25,26,27,28,29,30,75,391,13,14,15,16,17,18,53,71,52,72,54,2,4,66,67,59,60,58,40,3,79,80,82,93,131,132,574,249,136,1736,1737,48,51])).
% 59.55/59.63 cnf(3826,plain,
% 59.55/59.63 (P5(f15(a1),f16(x38261,a1))),
% 59.55/59.63 inference(scs_inference,[],[3798,848])).
% 59.55/59.63 cnf(3860,plain,
% 59.55/59.63 (~E(f2(a6,f9(a1)),f9(a1))),
% 59.55/59.63 inference(scs_inference,[],[3777,391,55])).
% 59.55/59.63 cnf(3866,plain,
% 59.55/59.63 (P5(f15(a6),a6)),
% 59.55/59.63 inference(scs_inference,[],[3777,1911,391,55,53,61,135])).
% 59.55/59.63 cnf(3868,plain,
% 59.55/59.63 (P5(f2(a6,f9(a1)),a6)),
% 59.55/59.63 inference(scs_inference,[],[3777,1911,391,55,53,61,135,52])).
% 59.55/59.63 cnf(3875,plain,
% 59.55/59.63 (~P6(x38751,f5(a1,a6),f16(a1,a6))),
% 59.55/59.63 inference(scs_inference,[],[3777,3779,3795,1911,1886,1894,391,55,53,61,135,52,54,2,40,36,37])).
% 59.55/59.63 cnf(3879,plain,
% 59.55/59.63 (P4(a8,a1)),
% 59.55/59.63 inference(scs_inference,[],[3755,3759,3777,3779,3771,3795,1911,1886,46,1894,391,55,53,61,135,52,54,2,40,36,37,82,80])).
% 59.55/59.63 cnf(3881,plain,
% 59.55/59.63 (P4(a8,a6)),
% 59.55/59.63 inference(scs_inference,[],[3755,3759,3777,3779,3771,3795,1911,1886,46,1894,391,55,53,61,135,52,54,2,40,36,37,82,80,79])).
% 59.55/59.63 cnf(3885,plain,
% 59.55/59.63 (P5(f15(a1),f16(a1,a6))),
% 59.55/59.63 inference(scs_inference,[],[3755,3759,3777,3779,3722,3771,3795,1911,1886,46,1894,391,55,53,61,135,52,54,2,40,36,37,82,80,79,65,43])).
% 59.55/59.63 cnf(3896,plain,
% 59.55/59.63 (~E(f2(a6,a8),a8)),
% 59.55/59.63 inference(scs_inference,[],[3881,55])).
% 59.55/59.63 cnf(3898,plain,
% 59.55/59.63 (P4(f2(a6,a8),a6)),
% 59.55/59.63 inference(scs_inference,[],[3881,55,61])).
% 59.55/59.63 cnf(3900,plain,
% 59.55/59.63 (P5(f7(x39001),x39001)),
% 59.55/59.63 inference(scs_inference,[],[3881,45,55,61,53])).
% 59.55/59.63 cnf(3902,plain,
% 59.55/59.63 (P5(f2(a6,a8),a6)),
% 59.55/59.63 inference(scs_inference,[],[3881,45,55,61,53,52])).
% 59.55/59.63 cnf(3904,plain,
% 59.55/59.63 (~P4(f7(x39041),x39041)),
% 59.55/59.63 inference(scs_inference,[],[3881,45,55,61,53,52,54])).
% 59.55/59.63 cnf(3913,plain,
% 59.55/59.63 (~P6(x39131,f16(a1,a6),f16(a1,a6))),
% 59.55/59.63 inference(scs_inference,[],[3881,3875,3860,1886,45,55,61,53,52,54,2,66,67,65,36])).
% 59.55/59.63 cnf(3940,plain,
% 59.55/59.63 (P4(f2(a6,f2(a6,a8)),a6)),
% 59.55/59.63 inference(scs_inference,[],[3898,61])).
% 59.55/59.63 cnf(3942,plain,
% 59.55/59.63 (~E(f2(a6,f2(a6,a8)),f2(a6,a8))),
% 59.55/59.63 inference(scs_inference,[],[3898,61,55])).
% 59.55/59.63 cnf(3944,plain,
% 59.55/59.63 (P5(f2(a6,f2(a6,a8)),a6)),
% 59.55/59.63 inference(scs_inference,[],[3898,61,55,52])).
% 59.55/59.63 cnf(3946,plain,
% 59.55/59.63 (~E(a8,f2(a6,a8))),
% 59.55/59.63 inference(scs_inference,[],[3898,3896,61,55,52,2])).
% 59.55/59.63 cnf(3947,plain,
% 59.55/59.63 (~P6(x39471,x39472,x39472)),
% 59.55/59.63 inference(scs_inference,[],[3900,3904,3898,3896,61,55,52,2,79])).
% 59.55/59.63 cnf(3962,plain,
% 59.55/59.63 (E(f2(a6,f2(a6,a8)),a8)),
% 59.55/59.63 inference(scs_inference,[],[3900,3904,3913,3866,3773,3898,3896,3885,3881,61,55,52,2,79,82,83,88,66,56,62])).
% 59.55/59.63 cnf(3968,plain,
% 59.55/59.63 (~E(f2(a1,a8),a8)),
% 59.55/59.63 inference(scs_inference,[],[3879,55])).
% 59.55/59.63 cnf(3970,plain,
% 59.55/59.63 (P4(f2(a1,a8),a1)),
% 59.55/59.63 inference(scs_inference,[],[3879,55,61])).
% 59.55/59.63 cnf(3972,plain,
% 59.55/59.63 (P5(f2(a1,a8),a1)),
% 59.55/59.63 inference(scs_inference,[],[3879,55,61,52])).
% 59.55/59.63 cnf(3975,plain,
% 59.55/59.63 (P5(f2(a1,a8),a6)),
% 59.55/59.63 inference(scs_inference,[],[44,3942,3879,55,61,52,2,58])).
% 59.55/59.63 cnf(3980,plain,
% 59.55/59.63 (~P6(x39801,x39802,x39802)),
% 59.55/59.63 inference(rename_variables,[],[3947])).
% 59.55/59.63 cnf(3982,plain,
% 59.55/59.63 (~P6(x39821,x39822,x39822)),
% 59.55/59.63 inference(rename_variables,[],[3947])).
% 59.55/59.63 cnf(3986,plain,
% 59.55/59.63 (~P6(x39861,x39862,x39862)),
% 59.55/59.63 inference(rename_variables,[],[3947])).
% 59.55/59.63 cnf(3991,plain,
% 59.55/59.63 (E(a8,f2(a6,f2(a6,a8)))),
% 59.55/59.63 inference(scs_inference,[],[44,3947,3980,3982,3986,3946,3902,3942,3783,3940,3962,3826,3757,3879,3904,3898,3881,46,55,61,52,2,58,40,37,36,79,82,83,62])).
% 59.55/59.63 cnf(3993,plain,
% 59.55/59.63 (P6(f2(a6,f2(a6,a8)),a1,a6)),
% 59.55/59.63 inference(scs_inference,[],[44,3947,3980,3982,3986,3946,3902,3942,3783,3940,3962,3826,3757,3879,3904,3898,3881,46,55,61,52,2,58,40,37,36,79,82,83,62,128])).
% 59.55/59.63 cnf(3994,plain,
% 59.55/59.63 (P5(f14(f15(a1),f16(a1,a1),f16(a1,a1)),a6)),
% 59.55/59.63 inference(scs_inference,[],[44,3947,3980,3982,3986,3946,3902,3942,3783,3940,3962,3826,3757,3879,3904,3898,3881,46,55,61,52,2,58,40,37,36,79,82,83,62,128,95])).
% 59.55/59.63 cnf(4000,plain,
% 59.55/59.63 (P5(f14(f15(a1),f16(a1,a1),f16(a1,a1)),a1)),
% 59.55/59.63 inference(scs_inference,[],[44,3947,3980,3982,3986,3946,3902,3942,3783,3940,3962,3826,3757,3879,3719,3904,3898,3881,46,55,61,52,2,58,40,37,36,79,82,83,62,128,95,72,634,91])).
% 59.55/59.63 cnf(4020,plain,
% 59.55/59.63 (~E(f2(a1,f2(a1,a8)),f2(a1,a8))),
% 59.55/59.63 inference(scs_inference,[],[3970,61,55])).
% 59.55/59.63 cnf(4027,plain,
% 59.55/59.63 (~E(f2(a1,a8),f7(a1))),
% 59.55/59.63 inference(scs_inference,[],[3970,3968,3991,3904,45,61,55,52,2,34,39])).
% 59.55/59.63 cnf(4029,plain,
% 59.55/59.63 (P4(f2(a1,a8),a6)),
% 59.55/59.63 inference(scs_inference,[],[3975,3970,3972,3968,3991,3993,3904,45,61,55,52,2,34,39,79])).
% 59.55/59.63 cnf(4055,plain,
% 59.55/59.63 (~E(f2(a6,f2(a1,a8)),f2(a1,a8))),
% 59.55/59.63 inference(scs_inference,[],[4029,55])).
% 59.55/59.63 cnf(4062,plain,
% 59.55/59.63 (P5(f2(a6,f2(a6,a8)),f5(a1,a6))),
% 59.55/59.63 inference(scs_inference,[],[4029,4027,3944,1894,55,61,52,2,59])).
% 59.55/59.63 cnf(4091,plain,
% 59.55/59.63 (~E(f2(a6,f15(a6)),f15(a6))),
% 59.55/59.63 inference(scs_inference,[],[3785,61,55])).
% 59.55/59.63 cnf(4096,plain,
% 59.55/59.63 (P5(a8,f5(a1,a6))),
% 59.55/59.63 inference(scs_inference,[],[4062,4020,3785,3962,61,55,52,2,42])).
% 59.55/59.63 cnf(4126,plain,
% 59.55/59.63 (P5(f14(a8,f5(a1,a6),f5(a1,a6)),f5(a1,a6))),
% 59.55/59.63 inference(scs_inference,[],[4096,4055,3994,3787,4000,3993,3947,61,52,2,80,83])).
% 59.55/59.63 cnf(4127,plain,
% 59.55/59.63 (~P6(x41271,x41272,x41272)),
% 59.55/59.63 inference(rename_variables,[],[3947])).
% 59.55/59.63 cnf(4129,plain,
% 59.55/59.63 (~P4(f14(a8,f5(a1,a6),f5(a1,a6)),f5(a1,a6))),
% 59.55/59.63 inference(scs_inference,[],[4096,4055,3994,3787,4000,3993,3947,4127,61,52,2,80,83,88])).
% 59.55/59.63 cnf(4161,plain,
% 59.55/59.63 (P5(f2(a1,f15(a1)),a1)),
% 59.55/59.63 inference(scs_inference,[],[3713,61,52])).
% 59.55/59.63 cnf(4164,plain,
% 59.55/59.63 (P2(f14(a8,f5(a1,a6),f5(a1,a6)),f5(a1,a6))),
% 59.55/59.63 inference(scs_inference,[],[4129,4126,4091,3713,61,52,2,56])).
% 59.55/59.63 cnf(4167,plain,
% 59.55/59.63 (~P6(x41671,x41672,x41672)),
% 59.55/59.63 inference(rename_variables,[],[3947])).
% 59.55/59.63 cnf(4172,plain,
% 59.55/59.63 (P5(f2(a1,f15(a1)),a6)),
% 59.55/59.63 inference(scs_inference,[],[4129,4126,4091,3773,3713,3947,4167,61,52,2,56,83,88,93])).
% 59.55/59.63 cnf(4201,plain,
% 59.55/59.63 (P4(f2(a1,f15(a1)),a6)),
% 59.55/59.63 inference(scs_inference,[],[4172,3794,4164,4161,3993,1894,2,34,79])).
% 59.55/59.63 cnf(4236,plain,
% 59.55/59.63 (P5(f14(f2(a1,a8),a1,a1),a1)),
% 59.55/59.63 inference(scs_inference,[],[3868,4161,3972,3970,3947,1894,59,60,522,83])).
% 59.55/59.63 cnf(4268,plain,
% 59.55/59.63 (P5(f14(a8,a6,a6),a6)),
% 59.55/59.63 inference(scs_inference,[],[4236,4201,3755,3904,3947,93,39,82])).
% 59.55/59.63 cnf(4269,plain,
% 59.55/59.63 (~P6(x42691,x42692,x42692)),
% 59.55/59.63 inference(rename_variables,[],[3947])).
% 59.55/59.63 cnf(4274,plain,
% 59.55/59.63 (P5(f14(a8,a1,a1),a1)),
% 59.55/59.63 inference(scs_inference,[],[4236,4201,4027,3755,3759,3904,3947,4269,93,39,82,2,69,83])).
% 59.55/59.63 cnf(4280,plain,
% 59.55/59.63 (P5(f14(a8,a1,a1),a6)),
% 59.55/59.63 inference(scs_inference,[],[4274,93])).
% 59.55/59.63 cnf(4282,plain,
% 59.55/59.63 (P4(f14(a8,a1,a1),a1)),
% 59.55/59.63 inference(scs_inference,[],[4274,3993,93,80])).
% 59.55/59.63 cnf(4284,plain,
% 59.55/59.63 (P5(f14(f14(a8,a6,a6),a6,a6),a6)),
% 59.55/59.63 inference(scs_inference,[],[4268,4274,3993,3947,93,80,82])).
% 59.55/59.63 cnf(4285,plain,
% 59.55/59.63 (~P6(x42851,x42852,x42852)),
% 59.55/59.63 inference(rename_variables,[],[3947])).
% 59.55/59.63 cnf(4287,plain,
% 59.55/59.63 (~P4(f14(f14(a8,a6,a6),a6,a6),a6)),
% 59.55/59.63 inference(scs_inference,[],[4268,4274,3993,3947,4285,93,80,82,88])).
% 59.55/59.63 cnf(4294,plain,
% 59.55/59.63 (P5(f2(a1,f14(a8,a1,a1)),a1)),
% 59.55/59.63 inference(scs_inference,[],[4268,4274,3993,3947,4285,93,80,82,88,55,61,52])).
% 59.55/59.63 cnf(4309,plain,
% 59.55/59.63 (~P6(x43091,x43092,x43092)),
% 59.55/59.63 inference(rename_variables,[],[3947])).
% 59.55/59.63 cnf(4311,plain,
% 59.55/59.63 ($false),
% 59.55/59.63 inference(scs_inference,[],[4280,4282,4284,4287,4294,4274,3759,3993,3947,4309,93,56,79,83,88]),
% 59.55/59.63 ['proof']).
% 59.55/59.63 % SZS output end Proof
% 59.55/59.63 % Total time :58.980000s
%------------------------------------------------------------------------------