%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : GEO111-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:51 EDT 2024
% Result : Unsatisfiable 59.01s 59.03s
% Output : CNFRefutation 59.05s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : GEO111-1 : TPTP v8.2.0. Released v2.4.0.
% 0.03/0.12 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% 0.12/0.33 % Computer : n026.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 300
% 0.12/0.33 % DateTime : Fri Jun 21 06:55:09 EDT 2024
% 0.12/0.33 % CPUTime :
% 0.50/0.59 start to proof:theBenchmark
% 58.97/59.01 %-------------------------------------------
% 58.97/59.01 % File :CSE---1.7
% 58.97/59.01 % Problem :theBenchmark
% 58.97/59.01 % Transform :cnf
% 58.97/59.01 % Format :tptp:raw
% 58.97/59.01 % Command :java -jar mcs_scs.jar %d %s
% 58.97/59.01
% 58.97/59.01 % Result :Theorem 58.380000s
% 58.97/59.01 % Output :CNFRefutation 58.380000s
% 58.97/59.01 %-------------------------------------------
% 59.01/59.02 %--------------------------------------------------------------------------
% 59.01/59.03 % File : GEO111-1 : TPTP v8.2.0. Released v2.4.0.
% 59.01/59.03 % Domain : Geometry (Oriented curves)
% 59.01/59.03 % Problem : Basic property of orderings on linear structures 1
% 59.01/59.03 % Version : [EHK99] axioms.
% 59.01/59.03 % English : If Q is between P and R wrt. c, then P, Q and R are incident
% 59.01/59.03 % with c and are pairwise distinct
% 59.01/59.03
% 59.01/59.03 % Refs : [KE99] Kulik & Eschenbach (1999), A Geometry of Oriented Curv
% 59.01/59.03 % : [EHK99] Eschenbach et al. (1999), Representing Simple Trajecto
% 59.01/59.03 % Source : [TPTP]
% 59.01/59.03 % Names :
% 59.01/59.03
% 59.01/59.03 % Status : Unsatisfiable
% 59.01/59.03 % Rating : 0.10 v8.1.0, 0.00 v7.5.0, 0.05 v7.4.0, 0.06 v7.3.0, 0.08 v7.1.0, 0.00 v7.0.0, 0.07 v6.3.0, 0.00 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.38 v5.1.0, 0.35 v5.0.0, 0.29 v4.1.0, 0.23 v4.0.1, 0.18 v4.0.0, 0.09 v3.7.0, 0.10 v3.5.0, 0.09 v3.4.0, 0.17 v3.3.0, 0.14 v3.2.0, 0.23 v3.1.0, 0.27 v2.7.0, 0.33 v2.6.0, 0.11 v2.5.0, 0.33 v2.4.0
% 59.01/59.03 % Syntax : Number of clauses : 56 ( 2 unt; 23 nHn; 51 RR)
% 59.01/59.03 % Number of literals : 177 ( 26 equ; 91 neg)
% 59.01/59.03 % Maximal clause size : 12 ( 3 avg)
% 59.01/59.03 % Maximal term depth : 3 ( 1 avg)
% 59.01/59.03 % Number of predicates : 9 ( 8 usr; 0 prp; 1-4 aty)
% 59.01/59.03 % Number of functors : 19 ( 19 usr; 4 con; 0-4 aty)
% 59.01/59.03 % Number of variables : 151 ( 12 sgn)
% 59.01/59.03 % SPC : CNF_UNS_RFO_SEQ_NHN
% 59.01/59.03
% 59.01/59.03 % Comments : Created by tptp2X -f tptp -t clausify:otter GEO111+1.p
% 59.01/59.03 %--------------------------------------------------------------------------
% 59.01/59.03 %----Include simple curve axioms
% 59.01/59.03 include('Axioms/GEO004-0.ax').
% 59.01/59.03 %----Include axioms of betweenness for simple curves
% 59.01/59.03 include('Axioms/GEO004-1.ax').
% 59.01/59.03 %--------------------------------------------------------------------------
% 59.01/59.03 cnf(theorem_3_8_1_77,negated_conjecture,
% 59.01/59.03 between_c(sk15,sk16,sk17,sk18) ).
% 59.01/59.03
% 59.01/59.03 cnf(theorem_3_8_1_78,negated_conjecture,
% 59.01/59.03 ( ~ incident_c(sk16,sk15)
% 59.01/59.03 | ~ incident_c(sk17,sk15)
% 59.01/59.03 | ~ incident_c(sk18,sk15)
% 59.01/59.03 | sk16 = sk17
% 59.01/59.03 | sk17 = sk18
% 59.01/59.03 | sk16 = sk18 ) ).
% 59.01/59.03
% 59.01/59.03 %--------------------------------------------------------------------------
% 59.01/59.03 %-------------------------------------------
% 59.01/59.03 % Proof found
% 59.01/59.03 % SZS status Theorem for theBenchmark
% 59.01/59.03 % SZS output start Proof
% 59.01/59.03 %ClaNum:102(EqnAxiom:51)
% 59.01/59.03 %VarNum:387(SingletonVarNum:138)
% 59.01/59.03 %MaxLitNum:12
% 59.01/59.03 %MaxfuncDepth:2
% 59.01/59.03 %SharedTerms:11
% 59.01/59.03 %goalClause: 53 65
% 59.01/59.03 %singleGoalClaCount:1
% 59.01/59.03 [53]P2(a13,a16,a17,a18)
% 59.01/59.03 [52]P1(f1(x521),x521)
% 59.01/59.03 [54]P3(x541)+P4(f2(x541),x541)
% 59.01/59.03 [56]~P6(x561)+P4(f12(x561),x561)
% 59.01/59.03 [55]P6(x551)+~P4(x552,x551)
% 59.01/59.03 [58]~P3(x581)+~P4(x582,x581)
% 59.01/59.03 [59]~P4(x591,x592)+P5(x591,x592)
% 59.01/59.03 [60]~P1(x601,x602)+P5(x601,x602)
% 59.01/59.03 [61]~P1(x611,x612)+~P4(x611,x612)
% 59.01/59.03 [62]~P4(x621,x622)+~E(f3(x621,x622),x621)
% 59.01/59.03 [64]P8(x641,x642)+P5(f4(x641,x642),x641)
% 59.01/59.03 [69]~P4(x691,x692)+P4(f3(x691,x692),x692)
% 59.01/59.03 [76]P8(x761,x762)+~P5(f4(x761,x762),x762)
% 59.01/59.03 [83]~P1(x831,x832)+P7(x831,f14(x831,x832),f5(x831,x832))
% 59.01/59.03 [78]~P1(x781,x782)+E(f19(f14(x781,x782),f5(x781,x782)),x782)
% 59.01/59.03 [79]P5(x791,x792)+~P7(x791,x793,x792)
% 59.01/59.03 [80]P5(x801,x802)+~P7(x801,x802,x803)
% 59.01/59.03 [81]~P7(x813,x812,x811)+E(f8(x811,x812),f19(x812,x811))
% 59.01/59.03 [95]~E(x951,x952)+~P2(x953,x951,x954,x952)
% 59.01/59.04 [99]~P2(x994,x993,x992,x991)+P4(x991,f15(x991,x992,x993,x994))
% 59.01/59.04 [100]~P2(x1004,x1001,x1003,x1002)+P4(x1001,f15(x1002,x1003,x1001,x1004))
% 59.01/59.04 [101]~P2(x1014,x1013,x1011,x1012)+P1(x1011,f15(x1012,x1011,x1013,x1014))
% 59.01/59.04 [102]~P2(x1024,x1023,x1022,x1021)+P8(f15(x1021,x1022,x1023,x1024),x1024)
% 59.01/59.04 [57]P6(x571)+~P8(x571,x572)+E(x571,x572)
% 59.01/59.04 [63]P1(x631,x632)+~P5(x631,x632)+P4(x631,x632)
% 59.01/59.04 [72]~P5(x721,x722)+P4(x721,x722)+P5(x721,f6(x722,x721))
% 59.01/59.04 [73]~P5(x731,x732)+P4(x731,x732)+P5(x731,f10(x732,x731))
% 59.01/59.04 [74]~P5(x741,x742)+P4(x741,x742)+P8(f6(x742,x741),x742)
% 59.01/59.04 [75]~P5(x751,x752)+P4(x751,x752)+P8(f10(x752,x751),x752)
% 59.01/59.04 [77]E(x771,x772)+P5(f7(x771,x772),x772)+P5(f7(x771,x772),x771)
% 59.01/59.04 [82]E(x821,x822)+~P5(f7(x821,x822),x822)+~P5(f7(x821,x822),x821)
% 59.01/59.04 [84]~P5(x841,x842)+P4(x841,x842)+~P8(f6(x842,x841),f10(x842,x841))
% 59.01/59.04 [85]~P5(x851,x852)+P4(x851,x852)+~P8(f10(x852,x851),f6(x852,x851))
% 59.01/59.04 [66]~P5(x661,x663)+P5(x661,x662)+~P8(x663,x662)
% 59.01/59.04 [96]~P5(f9(x963,x962,x961),x961)+~P5(f9(x963,x962,x961),x962)+E(x961,f19(x962,x963))
% 59.01/59.04 [97]~P5(f9(x973,x972,x971),x971)+~P5(f9(x973,x972,x971),x973)+E(x971,f19(x972,x973))
% 59.01/59.04 [67]~P5(x671,x674)+P5(x671,x672)+~E(x672,f19(x673,x674))
% 59.01/59.04 [68]~P5(x681,x683)+P5(x681,x682)+~E(x682,f19(x683,x684))
% 59.01/59.04 [90]~P5(x901,x903)+~P5(x901,x902)+P7(x901,x902,x903)+P5(f11(x903,x902,x901),x903)
% 59.01/59.04 [91]~P5(x911,x913)+~P5(x911,x912)+P7(x911,x912,x913)+P5(f11(x913,x912,x911),x912)
% 59.01/59.04 [94]P5(f9(x943,x942,x941),x941)+P5(f9(x943,x942,x941),x942)+P5(f9(x943,x942,x941),x943)+E(x941,f19(x942,x943))
% 59.01/59.04 [87]~P5(x871,x872)+P4(x871,x872)+~P7(x874,x873,x872)+~P5(x871,x873)
% 59.01/59.04 [88]~P5(x881,x882)+P4(x881,x882)+~P7(x884,x882,x883)+~P5(x881,x883)
% 59.01/59.04 [71]~P5(x711,x714)+P5(x711,x712)+P5(x711,x713)+~E(x714,f19(x713,x712))
% 59.01/59.04 [98]~P5(x981,x983)+~P5(x981,x982)+P7(x981,x982,x983)+~P4(f11(x983,x982,x981),x983)+~P4(f11(x983,x982,x981),x982)
% 59.01/59.04 [89]~P3(x894)+~P4(x891,x892)+P7(x891,x892,x893)+~P7(x895,x892,x893)+~E(x894,f19(x892,x893))
% 59.01/59.04 [65]E(a17,a16)+E(a18,a16)+E(a18,a17)+~P5(a16,a13)+~P5(a17,a13)+~P5(a18,a13)
% 59.01/59.04 [70]E(x703,x701)+~P4(x701,x704)+~P4(x703,x704)+E(x701,x702)+E(x703,x702)+~P4(x702,x704)
% 59.01/59.04 [93]~P4(x932,x935)+~P4(x931,x935)+~P1(x934,x935)+E(x931,x932)+P2(x933,x931,x934,x932)+~P8(x935,x933)
% 59.01/59.04 [86]P8(x862,x861)+~P8(x862,x863)+~P5(x864,x862)+~P4(x864,x863)+P8(x861,x862)+~P8(x861,x863)+~P5(x864,x861)
% 59.01/59.04 [92]P8(x922,x921)+P8(x922,x923)+P8(x923,x921)+P8(x923,x922)+~P8(x922,x924)+~P8(x923,x924)+~P4(x925,x922)+~P4(x925,x923)+P8(x921,x922)+P8(x921,x923)+~P8(x921,x924)+~P4(x925,x921)
% 59.01/59.04 %EqnAxiom
% 59.01/59.04 [1]E(x11,x11)
% 59.01/59.04 [2]E(x22,x21)+~E(x21,x22)
% 59.01/59.04 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 59.01/59.04 [4]~E(x41,x42)+E(f1(x41),f1(x42))
% 59.01/59.04 [5]~E(x51,x52)+E(f2(x51),f2(x52))
% 59.01/59.04 [6]~E(x61,x62)+E(f12(x61),f12(x62))
% 59.01/59.04 [7]~E(x71,x72)+E(f3(x71,x73),f3(x72,x73))
% 59.01/59.04 [8]~E(x81,x82)+E(f3(x83,x81),f3(x83,x82))
% 59.01/59.04 [9]~E(x91,x92)+E(f4(x91,x93),f4(x92,x93))
% 59.01/59.04 [10]~E(x101,x102)+E(f4(x103,x101),f4(x103,x102))
% 59.01/59.04 [11]~E(x111,x112)+E(f19(x111,x113),f19(x112,x113))
% 59.01/59.04 [12]~E(x121,x122)+E(f19(x123,x121),f19(x123,x122))
% 59.01/59.04 [13]~E(x131,x132)+E(f15(x131,x133,x134,x135),f15(x132,x133,x134,x135))
% 59.01/59.04 [14]~E(x141,x142)+E(f15(x143,x141,x144,x145),f15(x143,x142,x144,x145))
% 59.01/59.04 [15]~E(x151,x152)+E(f15(x153,x154,x151,x155),f15(x153,x154,x152,x155))
% 59.01/59.04 [16]~E(x161,x162)+E(f15(x163,x164,x165,x161),f15(x163,x164,x165,x162))
% 59.01/59.04 [17]~E(x171,x172)+E(f9(x171,x173,x174),f9(x172,x173,x174))
% 59.01/59.04 [18]~E(x181,x182)+E(f9(x183,x181,x184),f9(x183,x182,x184))
% 59.01/59.04 [19]~E(x191,x192)+E(f9(x193,x194,x191),f9(x193,x194,x192))
% 59.01/59.04 [20]~E(x201,x202)+E(f11(x201,x203,x204),f11(x202,x203,x204))
% 59.01/59.04 [21]~E(x211,x212)+E(f11(x213,x211,x214),f11(x213,x212,x214))
% 59.01/59.04 [22]~E(x221,x222)+E(f11(x223,x224,x221),f11(x223,x224,x222))
% 59.01/59.04 [23]~E(x231,x232)+E(f6(x231,x233),f6(x232,x233))
% 59.01/59.04 [24]~E(x241,x242)+E(f6(x243,x241),f6(x243,x242))
% 59.01/59.04 [25]~E(x251,x252)+E(f10(x251,x253),f10(x252,x253))
% 59.01/59.04 [26]~E(x261,x262)+E(f10(x263,x261),f10(x263,x262))
% 59.01/59.04 [27]~E(x271,x272)+E(f5(x271,x273),f5(x272,x273))
% 59.01/59.04 [28]~E(x281,x282)+E(f5(x283,x281),f5(x283,x282))
% 59.01/59.04 [29]~E(x291,x292)+E(f7(x291,x293),f7(x292,x293))
% 59.01/59.04 [30]~E(x301,x302)+E(f7(x303,x301),f7(x303,x302))
% 59.01/59.04 [31]~E(x311,x312)+E(f14(x311,x313),f14(x312,x313))
% 59.01/59.04 [32]~E(x321,x322)+E(f14(x323,x321),f14(x323,x322))
% 59.01/59.04 [33]~E(x331,x332)+E(f8(x331,x333),f8(x332,x333))
% 59.01/59.04 [34]~E(x341,x342)+E(f8(x343,x341),f8(x343,x342))
% 59.01/59.04 [35]P1(x352,x353)+~E(x351,x352)+~P1(x351,x353)
% 59.01/59.04 [36]P1(x363,x362)+~E(x361,x362)+~P1(x363,x361)
% 59.01/59.04 [37]P2(x372,x373,x374,x375)+~E(x371,x372)+~P2(x371,x373,x374,x375)
% 59.01/59.04 [38]P2(x383,x382,x384,x385)+~E(x381,x382)+~P2(x383,x381,x384,x385)
% 59.01/59.04 [39]P2(x393,x394,x392,x395)+~E(x391,x392)+~P2(x393,x394,x391,x395)
% 59.01/59.04 [40]P2(x403,x404,x405,x402)+~E(x401,x402)+~P2(x403,x404,x405,x401)
% 59.01/59.04 [41]~P3(x411)+P3(x412)+~E(x411,x412)
% 59.01/59.04 [42]P4(x422,x423)+~E(x421,x422)+~P4(x421,x423)
% 59.01/59.04 [43]P4(x433,x432)+~E(x431,x432)+~P4(x433,x431)
% 59.01/59.04 [44]~P6(x441)+P6(x442)+~E(x441,x442)
% 59.01/59.04 [45]P5(x452,x453)+~E(x451,x452)+~P5(x451,x453)
% 59.01/59.04 [46]P5(x463,x462)+~E(x461,x462)+~P5(x463,x461)
% 59.01/59.04 [47]P7(x472,x473,x474)+~E(x471,x472)+~P7(x471,x473,x474)
% 59.01/59.04 [48]P7(x483,x482,x484)+~E(x481,x482)+~P7(x483,x481,x484)
% 59.01/59.04 [49]P7(x493,x494,x492)+~E(x491,x492)+~P7(x493,x494,x491)
% 59.01/59.04 [50]P8(x502,x503)+~E(x501,x502)+~P8(x501,x503)
% 59.01/59.04 [51]P8(x513,x512)+~E(x511,x512)+~P8(x513,x511)
% 59.01/59.04
% 59.01/59.04 %-------------------------------------------
% 59.01/59.05 cnf(103,plain,
% 59.01/59.05 (~P5(x1031,x1032)+P5(x1031,f19(x1033,x1032))),
% 59.01/59.05 inference(equality_inference,[],[67])).
% 59.01/59.05 cnf(104,plain,
% 59.01/59.05 (~P5(x1041,x1042)+P5(x1041,f19(x1042,x1043))),
% 59.01/59.05 inference(equality_inference,[],[68])).
% 59.01/59.05 cnf(105,plain,
% 59.01/59.05 (~P5(x1051,f19(x1052,x1053))+P5(x1051,x1053)+P5(x1051,x1052)),
% 59.05/59.05 inference(equality_inference,[],[71])).
% 59.05/59.05 cnf(107,plain,
% 59.05/59.05 (~P2(x1072,x1071,x1073,x1071)),
% 59.05/59.05 inference(equality_inference,[],[95])).
% 59.05/59.05 cnf(108,plain,
% 59.05/59.05 (~E(a16,a18)),
% 59.05/59.05 inference(scs_inference,[],[53,107,38])).
% 59.05/59.05 cnf(109,plain,
% 59.05/59.05 (~P2(x1091,x1092,x1093,x1092)),
% 59.05/59.05 inference(rename_variables,[],[107])).
% 59.05/59.05 cnf(110,plain,
% 59.05/59.05 (~E(a18,a16)),
% 59.05/59.05 inference(scs_inference,[],[53,107,109,38,40])).
% 59.05/59.05 cnf(112,plain,
% 59.05/59.05 (P1(x1121,x1122)+~E(f1(x1122),x1121)),
% 59.05/59.05 inference(scs_inference,[],[53,107,109,52,38,40,35])).
% 59.05/59.05 cnf(114,plain,
% 59.05/59.05 (P2(x1141,a16,a17,a18)+~E(a13,x1141)),
% 59.05/59.05 inference(scs_inference,[],[53,107,109,52,38,40,35,36,37])).
% 59.05/59.05 cnf(115,plain,
% 59.05/59.05 (P2(a13,a16,x1151,a18)+~E(a17,x1151)),
% 59.05/59.05 inference(scs_inference,[],[53,107,109,52,38,40,35,36,37,39])).
% 59.05/59.05 cnf(122,plain,
% 59.05/59.05 (E(a17,a16)+E(a18,a17)+~P5(a16,a13)+~P5(a17,a13)+~P5(a18,a13)),
% 59.05/59.05 inference(scs_inference,[],[110,65])).
% 59.05/59.05 cnf(126,plain,
% 59.05/59.05 (~P4(x1261,x1262)+~P4(a18,x1262)+P2(x1262,a16,f1(x1262),a18)+~P4(a16,x1262)+~P8(x1262,x1263)),
% 59.05/59.05 inference(scs_inference,[],[108,52,93,92])).
% 59.05/59.05 cnf(139,plain,
% 59.05/59.05 (~P4(x1391,x1392)+P4(f12(x1392),x1392)),
% 59.05/59.05 inference(scs_inference,[],[55,56])).
% 59.05/59.05 cnf(155,plain,
% 59.05/59.05 (~P4(x1551,x1552)+P4(f2(x1552),x1552)),
% 59.05/59.05 inference(scs_inference,[],[58,54])).
% 59.05/59.05 cnf(219,plain,
% 59.05/59.05 (~P4(x2191,x2192)+P5(x2191,f19(x2193,x2192))),
% 59.05/59.05 inference(scs_inference,[],[59,103])).
% 59.05/59.05 cnf(235,plain,
% 59.05/59.05 (P5(f1(x2351),f19(x2351,x2352))),
% 59.05/59.05 inference(scs_inference,[],[52,60,104])).
% 59.05/59.05 cnf(236,plain,
% 59.05/59.05 (P5(f1(x2361),f19(x2362,f19(x2361,x2363)))),
% 59.05/59.05 inference(scs_inference,[],[235,103])).
% 59.05/59.05 cnf(334,plain,
% 59.05/59.05 (~P4(x3341,x3342)+~P1(f12(x3342),x3342)),
% 59.05/59.05 inference(scs_inference,[],[139,61])).
% 59.05/59.05 cnf(382,plain,
% 59.05/59.05 (~E(f1(x3821),f12(x3821))+~P4(x3822,x3821)),
% 59.05/59.05 inference(scs_inference,[],[334,112])).
% 59.05/59.05 cnf(446,plain,
% 59.05/59.05 (P4(f3(a18,f15(a18,a17,a16,a13)),f15(a18,a17,a16,a13))),
% 59.05/59.05 inference(scs_inference,[],[53,69,99])).
% 59.05/59.05 cnf(449,plain,
% 59.05/59.05 (~P1(f3(a18,f15(a18,a17,a16,a13)),f15(a18,a17,a16,a13))),
% 59.05/59.05 inference(scs_inference,[],[446,219,61])).
% 59.05/59.05 cnf(455,plain,
% 59.05/59.05 (P4(x4551,f15(a18,a17,a16,a13))+~E(f3(a18,f15(a18,a17,a16,a13)),x4551)),
% 59.05/59.05 inference(scs_inference,[],[52,446,219,61,35,63,42])).
% 59.05/59.05 cnf(496,plain,
% 59.05/59.05 (~E(f12(f15(a18,a17,a16,a13)),f1(f15(a18,a17,a16,a13)))),
% 59.05/59.05 inference(scs_inference,[],[446,382,2])).
% 59.05/59.05 cnf(1185,plain,
% 59.05/59.05 (P4(a16,f15(a18,a17,a16,x11851))+~E(a13,x11851)),
% 59.05/59.05 inference(scs_inference,[],[100,114])).
% 59.05/59.05 cnf(1186,plain,
% 59.05/59.05 (P4(a16,f15(a18,a17,a16,a13))),
% 59.05/59.05 inference(equality_inference,[],[1185])).
% 59.05/59.05 cnf(1189,plain,
% 59.05/59.05 (~P1(a16,f15(a18,a17,a16,a13))),
% 59.05/59.05 inference(scs_inference,[],[1186,219,61])).
% 59.05/59.05 cnf(1231,plain,
% 59.05/59.05 (P1(x12311,f15(a18,x12311,a16,a13))+~E(a17,x12311)),
% 59.05/59.05 inference(scs_inference,[],[101,115])).
% 59.05/59.05 cnf(1232,plain,
% 59.05/59.05 (P1(a17,f15(a18,a17,a16,a13))),
% 59.05/59.05 inference(equality_inference,[],[1231])).
% 59.05/59.05 cnf(1233,plain,
% 59.05/59.05 (~E(a17,f3(a18,f15(a18,a17,a16,a13)))),
% 59.05/59.05 inference(scs_inference,[],[1232,449,35])).
% 59.05/59.05 cnf(1240,plain,
% 59.05/59.05 (~E(a17,a16)),
% 59.05/59.05 inference(scs_inference,[],[1232,1189,35])).
% 59.05/59.05 cnf(1243,plain,
% 59.05/59.05 (E(a18,a17)+~P5(a18,a13)+~P5(a17,a13)+~P5(a16,a13)),
% 59.05/59.05 inference(scs_inference,[],[1186,1232,1189,35,122])).
% 59.05/59.05 cnf(1337,plain,
% 59.05/59.05 (P8(f15(a18,a17,a16,x13371),x13371)+~E(a13,x13371)),
% 59.05/59.05 inference(scs_inference,[],[102,114])).
% 59.05/59.05 cnf(1338,plain,
% 59.05/59.05 (P8(f15(a18,a17,a16,a13),a13)),
% 59.05/59.05 inference(equality_inference,[],[1337])).
% 59.05/59.05 cnf(1342,plain,
% 59.05/59.05 (~P5(x13421,f15(a18,a17,a16,a13))+P5(x13421,a13)),
% 59.05/59.05 inference(scs_inference,[],[1338,66])).
% 59.05/59.05 cnf(1378,plain,
% 59.05/59.05 (~E(f1(f15(a18,a17,a16,a13)),a16)),
% 59.05/59.05 inference(scs_inference,[],[52,1189,35])).
% 59.05/59.05 cnf(1383,plain,
% 59.05/59.05 (P2(a13,a18,a17,a16)+~P4(a18,f15(a18,a17,a16,a13))),
% 59.05/59.05 inference(scs_inference,[],[1186,110,1232,1338,93])).
% 59.05/59.05 cnf(1388,plain,
% 59.05/59.05 (~P4(a17,f15(a18,a17,a16,a13))+~E(f3(a18,f15(a18,a17,a16,a13)),a17)),
% 59.05/59.05 inference(scs_inference,[],[1232,1233,1338,107,446,93,40])).
% 59.05/59.05 cnf(1406,plain,
% 59.05/59.05 (P5(a16,a13)),
% 59.05/59.05 inference(scs_inference,[],[1186,1342,59])).
% 59.05/59.05 cnf(1407,plain,
% 59.05/59.05 (E(a18,a17)+~P5(a18,a13)+~P5(a17,a13)),
% 59.05/59.05 inference(scs_inference,[],[1406,1243])).
% 59.05/59.05 cnf(1779,plain,
% 59.05/59.05 (~P4(a18,f15(a18,a17,a16,a13))+P4(a16,f15(a16,a17,a18,a13))),
% 59.05/59.05 inference(scs_inference,[],[1383,99])).
% 59.05/59.05 cnf(2140,plain,
% 59.05/59.05 (P4(a16,f15(a16,a17,a18,a13))),
% 59.05/59.05 inference(scs_inference,[],[53,1779,99])).
% 59.05/59.05 cnf(2143,plain,
% 59.05/59.05 (~P1(a16,f15(a16,a17,a18,a13))),
% 59.05/59.05 inference(scs_inference,[],[2140,219,61])).
% 59.05/59.05 cnf(2156,plain,
% 59.05/59.05 (~E(f1(f15(a16,a17,a18,a13)),a16)),
% 59.05/59.05 inference(scs_inference,[],[52,2143,35])).
% 59.05/59.05 cnf(2160,plain,
% 59.05/59.05 (P4(x21601,f15(a16,a17,a18,a13))+~E(a16,x21601)),
% 59.05/59.05 inference(scs_inference,[],[2140,52,2143,35,57,42])).
% 59.05/59.05 cnf(2498,plain,
% 59.05/59.05 (~E(f3(a18,f15(a18,a17,a16,a13)),a17)),
% 59.05/59.05 inference(scs_inference,[],[1388,455])).
% 59.05/59.05 cnf(4163,plain,
% 59.05/59.05 (~P4(a17,f15(a18,a17,a16,a13))),
% 59.05/59.05 inference(scs_inference,[],[1232,236,66,61])).
% 59.05/59.05 cnf(4171,plain,
% 59.05/59.05 (~P4(f1(x41711),x41711)),
% 59.05/59.05 inference(scs_inference,[],[52,61])).
% 59.05/59.05 cnf(4212,plain,
% 59.05/59.05 (~P5(f1(x42121),x42121)+~P7(x42122,f19(x42121,x42123),x42121)),
% 59.05/59.05 inference(scs_inference,[],[235,4171,87])).
% 59.05/59.05 cnf(4249,plain,
% 59.05/59.05 (~P5(f1(x42491),x42491)+~P7(x42492,x42491,f19(x42491,x42493))),
% 59.05/59.05 inference(scs_inference,[],[235,4171,88])).
% 59.05/59.05 cnf(4281,plain,
% 59.05/59.05 (~P5(a17,x42811)+~P5(a17,f15(a18,a17,a16,a13))+~P7(x42812,f15(a18,a17,a16,a13),x42811)),
% 59.05/59.05 inference(scs_inference,[],[1186,4163,88])).
% 59.05/59.05 cnf(4289,plain,
% 59.05/59.05 (P5(a17,f15(a18,a17,a16,a13))),
% 59.05/59.05 inference(scs_inference,[],[1232,60])).
% 59.05/59.05 cnf(4291,plain,
% 59.05/59.05 (P5(a17,f19(f15(a18,a17,a16,a13),x42911))),
% 59.05/59.05 inference(scs_inference,[],[1232,60,104])).
% 59.05/59.05 cnf(4293,plain,
% 59.05/59.05 (P5(a17,f19(x42931,f15(a18,a17,a16,a13)))),
% 59.05/59.05 inference(scs_inference,[],[1232,60,104,103])).
% 59.05/59.05 cnf(4295,plain,
% 59.05/59.05 (~P7(x42951,f15(a18,a17,a16,a13),f15(a18,a17,a16,a13))),
% 59.05/59.05 inference(scs_inference,[],[1232,60,104,103,4281])).
% 59.05/59.05 cnf(4298,plain,
% 59.05/59.05 (P5(a17,a13)),
% 59.05/59.05 inference(scs_inference,[],[1338,1232,60,104,103,4281,45,66])).
% 59.05/59.05 cnf(4310,plain,
% 59.05/59.05 (E(a18,a17)+~P5(a18,a13)),
% 59.05/59.05 inference(scs_inference,[],[4298,1407])).
% 59.05/59.05 cnf(4316,plain,
% 59.05/59.05 (~P7(x43161,f15(a18,a17,a16,a13),x43162)+~P5(a17,x43162)),
% 59.05/59.05 inference(scs_inference,[],[4289,4281])).
% 59.05/59.05 cnf(4319,plain,
% 59.05/59.05 (P5(f1(x43191),x43191)),
% 59.05/59.05 inference(scs_inference,[],[52,4291,4316,60])).
% 59.05/59.05 cnf(4321,plain,
% 59.05/59.05 (P5(a17,f19(x43211,a13))),
% 59.05/59.05 inference(scs_inference,[],[52,4291,4298,4316,60,103])).
% 59.05/59.05 cnf(4323,plain,
% 59.05/59.05 (P5(a17,f19(a13,x43231))),
% 59.05/59.05 inference(scs_inference,[],[52,4291,4298,4316,60,103,104])).
% 59.05/59.05 cnf(4325,plain,
% 59.05/59.05 (P5(f1(f15(a18,a17,a16,a13)),a13)),
% 59.05/59.05 inference(scs_inference,[],[1338,52,4291,4298,4316,60,103,104,66])).
% 59.05/59.05 cnf(4342,plain,
% 59.05/59.05 (P5(f1(x43421),f19(x43422,x43421))),
% 59.05/59.05 inference(scs_inference,[],[4319,4293,4212,4249,4316,103])).
% 59.05/59.05 cnf(4357,plain,
% 59.05/59.05 (P5(f1(x43571),f19(f19(x43572,x43571),x43573))),
% 59.05/59.05 inference(scs_inference,[],[4342,4321,4316,103,104])).
% 59.05/59.05 cnf(4384,plain,
% 59.05/59.05 (P5(a17,f19(x43841,f19(x43842,a13)))),
% 59.05/59.05 inference(scs_inference,[],[4321,4298,4316,103])).
% 59.05/59.05 cnf(4386,plain,
% 59.05/59.05 (P5(a17,f19(f19(x43861,a13),x43862))),
% 59.05/59.05 inference(scs_inference,[],[4321,4298,4316,103,104])).
% 59.05/59.05 cnf(4397,plain,
% 59.05/59.05 (P5(a16,f15(a18,a17,a16,a13))),
% 59.05/59.05 inference(scs_inference,[],[1186,59])).
% 59.05/59.05 cnf(4401,plain,
% 59.05/59.05 (P5(a17,f19(f19(a13,x44011),x44012))),
% 59.05/59.05 inference(scs_inference,[],[1186,4384,4323,59,4316,104])).
% 59.05/59.05 cnf(4403,plain,
% 59.05/59.05 (P5(a17,f19(x44031,f19(a13,x44032)))),
% 59.05/59.05 inference(scs_inference,[],[1186,4384,4323,59,4316,104,103])).
% 59.05/59.05 cnf(4413,plain,
% 59.05/59.05 (P5(a16,f15(a16,a17,a18,a13))),
% 59.05/59.05 inference(scs_inference,[],[2140,59])).
% 59.05/59.05 cnf(4419,plain,
% 59.05/59.05 (P5(f1(f15(a18,a17,a16,a13)),f19(x44191,a13))),
% 59.05/59.05 inference(scs_inference,[],[2140,4397,4386,4325,59,4316,104,103])).
% 59.05/59.05 cnf(4429,plain,
% 59.05/59.05 (P5(f3(a18,f15(a18,a17,a16,a13)),f15(a18,a17,a16,a13))),
% 59.05/59.05 inference(scs_inference,[],[446,59])).
% 59.05/59.05 cnf(4437,plain,
% 59.05/59.05 (P5(f3(a18,f15(a18,a17,a16,a13)),a13)),
% 59.05/59.05 inference(scs_inference,[],[1338,446,4419,4401,59,4316,104,103,66])).
% 59.05/59.05 cnf(4456,plain,
% 59.05/59.05 (~P3(f15(a18,a17,a16,a13))),
% 59.05/59.05 inference(scs_inference,[],[1186,2156,4429,4403,4437,4316,104,103,2,55,58])).
% 59.05/59.05 cnf(4458,plain,
% 59.05/59.05 (~E(x44581,a16)+~E(a18,x44581)),
% 59.05/59.05 inference(scs_inference,[],[110,1186,2156,4429,4403,4437,4316,104,103,2,55,58,3])).
% 59.05/59.05 cnf(4468,plain,
% 59.05/59.05 (~E(a16,f1(f15(a18,a17,a16,a13)))),
% 59.05/59.05 inference(scs_inference,[],[1378,2140,55,58,2])).
% 59.05/59.05 cnf(4481,plain,
% 59.05/59.05 (E(a17,a18)+~P5(a18,a13)),
% 59.05/59.05 inference(scs_inference,[],[4310,2])).
% 59.05/59.05 cnf(4482,plain,
% 59.05/59.05 (~E(f1(f15(a18,a17,a16,a13)),f12(f15(a18,a17,a16,a13)))),
% 59.05/59.05 inference(scs_inference,[],[496,2])).
% 59.05/59.05 cnf(4483,plain,
% 59.05/59.05 (P5(f3(a18,f15(a18,a17,a16,a13)),f19(a13,x44831))),
% 59.05/59.05 inference(scs_inference,[],[496,4437,2,104])).
% 59.05/59.05 cnf(4527,plain,
% 59.05/59.05 (~P5(a18,f19(a13,a13))+~E(f3(a18,f15(a18,a17,a16,a13)),a18)),
% 59.05/59.05 inference(scs_inference,[],[2498,3,4310,1342,79,80,2,105])).
% 59.05/59.05 cnf(4538,plain,
% 59.05/59.05 (~E(x45381,a18)+~E(a16,x45381)),
% 59.05/59.05 inference(scs_inference,[],[108,3])).
% 59.05/59.05 cnf(4544,plain,
% 59.05/59.05 (~E(x45441,a16)+~E(a17,x45441)),
% 59.05/59.05 inference(scs_inference,[],[1240,3])).
% 59.05/59.05 cnf(4563,plain,
% 59.05/59.05 (P5(x45631,x45632)+~E(f1(x45632),x45631)),
% 59.05/59.05 inference(scs_inference,[],[4482,4319,4295,4298,57,48,63,3,45])).
% 59.05/59.05 cnf(4600,plain,
% 59.05/59.05 (P4(f12(f15(a18,a17,a16,a13)),f15(a18,a17,a16,a13))),
% 59.05/59.05 inference(scs_inference,[],[1186,139])).
% 59.05/59.05 cnf(4610,plain,
% 59.05/59.05 (P5(f12(f15(a18,a17,a16,a13)),a13)),
% 59.05/59.05 inference(scs_inference,[],[1186,1338,4468,139,219,59,104,57,66])).
% 59.05/59.05 cnf(4624,plain,
% 59.05/59.05 (P4(f12(f15(a16,a17,a18,a13)),f15(a16,a17,a18,a13))),
% 59.05/59.05 inference(scs_inference,[],[2140,139])).
% 59.05/59.05 cnf(4736,plain,
% 59.05/59.05 (P5(x47361,a13)+~E(a17,x47361)),
% 59.05/59.05 inference(scs_inference,[],[4298,45])).
% 59.05/59.05 cnf(4861,plain,
% 59.05/59.05 (P6(a13)+P1(f12(f15(a18,a17,a16,a13)),a13)),
% 59.05/59.05 inference(scs_inference,[],[4610,63,139,59,58,219,55])).
% 59.05/59.05 cnf(5220,plain,
% 59.05/59.05 (~E(f3(a18,f15(a18,a17,a16,a13)),a18)),
% 59.05/59.05 inference(scs_inference,[],[4483,45,4527])).
% 59.05/59.05 cnf(5225,plain,
% 59.05/59.05 (~E(a18,f3(a18,f15(a18,a17,a16,a13)))),
% 59.05/59.05 inference(scs_inference,[],[5220,2])).
% 59.05/59.05 cnf(5775,plain,
% 59.05/59.05 (~P7(x57751,x57752,x57752)),
% 59.05/59.05 inference(scs_inference,[],[4319,4171,87])).
% 59.05/59.05 cnf(6183,plain,
% 59.05/59.05 (~P7(x61831,x61832,f19(x61833,x61832))),
% 59.05/59.05 inference(scs_inference,[],[4342,4319,4171,88])).
% 59.05/59.05 cnf(6223,plain,
% 59.05/59.05 (~P7(x62231,x62232,f19(f19(x62233,x62232),x62234))),
% 59.05/59.05 inference(scs_inference,[],[4357,4319,4171,88])).
% 59.05/59.05 cnf(6265,plain,
% 59.05/59.05 (P1(f12(f15(a18,a17,a16,a13)),x62651)+~E(a13,x62651)+P6(a13)),
% 59.05/59.05 inference(scs_inference,[],[4861,36])).
% 59.05/59.05 cnf(6586,plain,
% 59.05/59.05 (E(a16,f3(a18,f15(a18,a17,a16,a13)))+~P4(a18,f15(a18,a17,a16,a13))),
% 59.05/59.05 inference(scs_inference,[],[1186,5225,108,446,70])).
% 59.05/59.05 cnf(6719,plain,
% 59.05/59.05 (~P4(a18,f15(a18,a17,a16,a13))+E(f3(a18,f15(a18,a17,a16,a13)),a16)),
% 59.05/59.05 inference(scs_inference,[],[108,1186,5220,446,70])).
% 59.05/59.05 cnf(6830,plain,
% 59.05/59.05 (P4(f2(f15(a18,a17,a16,a13)),f15(a18,a17,a16,a13))),
% 59.05/59.05 inference(scs_inference,[],[4456,54])).
% 59.05/59.05 cnf(6832,plain,
% 59.05/59.05 (P4(f2(f15(a16,a17,a18,a13)),f15(a16,a17,a18,a13))),
% 59.05/59.05 inference(scs_inference,[],[4456,4624,54,155])).
% 59.05/59.05 cnf(6834,plain,
% 59.05/59.05 (~P1(f12(f15(a16,a17,a18,a13)),f15(a16,a17,a18,a13))),
% 59.05/59.05 inference(scs_inference,[],[4456,4624,54,155,334])).
% 59.05/59.05 cnf(6836,plain,
% 59.05/59.05 (~E(f3(a16,f15(a18,a17,a16,a13)),a16)),
% 59.05/59.06 inference(scs_inference,[],[4456,4624,1186,54,155,334,62])).
% 59.05/59.06 cnf(6842,plain,
% 59.05/59.06 (~P1(f12(f15(a18,a17,a16,a13)),f15(a18,a17,a16,a13))),
% 59.05/59.06 inference(scs_inference,[],[4456,4624,4600,1186,54,155,334,62,69,382,61])).
% 59.05/59.06 cnf(6848,plain,
% 59.05/59.06 (P4(a18,f15(a18,a17,a16,a13))),
% 59.05/59.06 inference(scs_inference,[],[53,4456,4624,1232,4600,1186,54,155,334,62,69,382,61,83,79,99])).
% 59.05/59.06 cnf(6853,plain,
% 59.05/59.06 (~P7(x68531,x68532,x68532)),
% 59.05/59.06 inference(rename_variables,[],[5775])).
% 59.05/59.06 cnf(6856,plain,
% 59.05/59.06 (P5(f1(x68561),f10(x68561,f1(x68561)))),
% 59.05/59.06 inference(scs_inference,[],[53,4456,4624,5775,4289,4171,4319,4163,1232,4600,1186,54,155,334,62,69,382,61,83,79,99,80,49,72,73])).
% 59.05/59.06 cnf(6857,plain,
% 59.05/59.06 (~P4(f1(x68571),x68571)),
% 59.05/59.06 inference(rename_variables,[],[4171])).
% 59.05/59.06 cnf(6859,plain,
% 59.05/59.06 (P8(f6(x68591,f1(x68591)),x68591)),
% 59.05/59.06 inference(scs_inference,[],[53,4456,4624,5775,4289,4171,6857,4319,4163,1232,4600,1186,54,155,334,62,69,382,61,83,79,99,80,49,72,73,74])).
% 59.05/59.06 cnf(6860,plain,
% 59.05/59.06 (~P4(f1(x68601),x68601)),
% 59.05/59.06 inference(rename_variables,[],[4171])).
% 59.05/59.06 cnf(6862,plain,
% 59.05/59.06 (P8(f10(x68621,f1(x68621)),x68621)),
% 59.05/59.06 inference(scs_inference,[],[53,4456,4624,5775,4289,4171,6857,6860,4319,4163,1232,4600,1186,54,155,334,62,69,382,61,83,79,99,80,49,72,73,74,75])).
% 59.05/59.06 cnf(6863,plain,
% 59.05/59.06 (~P4(f1(x68631),x68631)),
% 59.05/59.06 inference(rename_variables,[],[4171])).
% 59.05/59.06 cnf(6866,plain,
% 59.05/59.06 (~P4(f1(x68661),x68661)),
% 59.05/59.06 inference(rename_variables,[],[4171])).
% 59.05/59.06 cnf(6869,plain,
% 59.05/59.06 (~P4(f1(x68691),x68691)),
% 59.05/59.06 inference(rename_variables,[],[4171])).
% 59.05/59.06 cnf(6881,plain,
% 59.05/59.06 (P2(a13,a18,a17,a16)),
% 59.05/59.06 inference(scs_inference,[],[53,4456,6223,4624,5775,6853,4289,4357,4171,6857,6860,6863,6866,6869,4319,4163,1232,4600,1186,54,155,334,62,69,382,61,83,79,99,80,49,72,73,74,75,84,85,35,42,90,91,1383])).
% 59.05/59.06 cnf(6883,plain,
% 59.05/59.06 (E(f3(a18,f15(a18,a17,a16,a13)),a16)),
% 59.05/59.06 inference(scs_inference,[],[53,4456,6223,4624,5775,6853,4289,4357,4171,6857,6860,6863,6866,6869,4319,4163,1232,4600,1186,54,155,334,62,69,382,61,83,79,99,80,49,72,73,74,75,84,85,35,42,90,91,1383,6586,6719])).
% 59.05/59.06 cnf(6938,plain,
% 59.05/59.06 (P8(f15(a16,a17,a18,a13),a13)),
% 59.05/59.06 inference(scs_inference,[],[6881,1186,69,101,102])).
% 59.05/59.06 cnf(6940,plain,
% 59.05/59.06 (P4(a18,f15(a16,a17,a18,a13))),
% 59.05/59.06 inference(scs_inference,[],[6881,1186,69,101,102,100])).
% 59.05/59.06 cnf(6944,plain,
% 59.05/59.06 (~P1(a18,f15(a18,a17,a16,a13))),
% 59.05/59.06 inference(scs_inference,[],[6881,6848,1186,2140,69,101,102,100,62,61])).
% 59.05/59.06 cnf(6949,plain,
% 59.05/59.06 (~P4(f1(x69491),x69491)),
% 59.05/59.06 inference(rename_variables,[],[4171])).
% 59.05/59.06 cnf(6956,plain,
% 59.05/59.06 (~P4(f1(x69561),x69561)),
% 59.05/59.06 inference(rename_variables,[],[4171])).
% 59.05/59.06 cnf(6959,plain,
% 59.05/59.06 (~P4(f1(x69591),x69591)),
% 59.05/59.06 inference(rename_variables,[],[4171])).
% 59.05/59.06 cnf(6965,plain,
% 59.05/59.06 (P5(f1(x69651),x69651)),
% 59.05/59.06 inference(rename_variables,[],[4319])).
% 59.05/59.06 cnf(6968,plain,
% 59.05/59.06 (~P4(f11(f15(a16,a17,a18,a13),f15(a16,a17,a18,a13),a16),f15(a16,a17,a18,a13))),
% 59.05/59.06 inference(scs_inference,[],[6881,6848,6834,6856,6883,6183,5775,4413,4298,4321,4289,4171,6949,6956,6959,4319,4163,1186,2140,69,101,102,100,62,61,75,72,73,74,43,35,42,90,88,98])).
% 59.05/59.06 cnf(6973,plain,
% 59.05/59.06 (E(f3(a16,f15(a18,a17,a16,a13)),a18)),
% 59.05/59.06 inference(scs_inference,[],[6881,6848,6834,6856,6883,6836,6183,5775,4413,4298,4321,4289,4171,6949,6956,6959,4319,4163,1186,1338,108,2140,69,101,102,100,62,61,75,72,73,74,43,35,42,90,88,98,126,70])).
% 59.05/59.06 cnf(6976,plain,
% 59.05/59.06 (E(a18,f3(a16,f15(a18,a17,a16,a13)))),
% 59.05/59.06 inference(scs_inference,[],[6881,6848,6834,6856,6883,6836,6183,5775,4413,4298,4321,4289,4171,6949,6956,6959,4319,4163,1186,1338,108,2140,69,101,102,100,62,61,75,72,73,74,43,35,42,90,88,98,126,70,4538,2])).
% 59.05/59.06 cnf(6982,plain,
% 59.05/59.06 (P5(f1(a18),f3(a16,f15(a18,a17,a16,a13)))),
% 59.05/59.06 inference(scs_inference,[],[6881,6848,6842,6834,6856,6883,6836,6183,5775,4413,4298,4321,4289,107,4171,6949,6956,6959,4319,6965,4163,1186,1338,108,2140,69,101,102,100,62,61,75,72,73,74,43,35,42,90,88,98,126,70,4538,2,2160,6265,38,46])).
% 59.05/59.06 cnf(6989,plain,
% 59.05/59.06 (P4(f3(a18,f15(a16,a17,a18,a13)),f15(a16,a17,a18,a13))),
% 59.05/59.06 inference(scs_inference,[],[6940,69])).
% 59.05/59.06 cnf(6991,plain,
% 59.05/59.06 (~E(f3(a18,f15(a16,a17,a18,a13)),a18)),
% 59.05/59.06 inference(scs_inference,[],[6940,69,62])).
% 59.05/59.06 cnf(6993,plain,
% 59.05/59.06 (~P1(a18,f15(a16,a17,a18,a13))),
% 59.05/59.06 inference(scs_inference,[],[6940,69,62,61])).
% 59.05/59.06 cnf(6997,plain,
% 59.05/59.06 (~P4(f1(a18),f3(a16,f15(a18,a17,a16,a13)))),
% 59.05/59.06 inference(scs_inference,[],[6940,6973,107,4171,69,62,61,40,43])).
% 59.05/59.06 cnf(7000,plain,
% 59.05/59.06 (~E(a17,a18)),
% 59.05/59.06 inference(scs_inference,[],[6940,6944,6968,6973,107,4171,1232,69,62,61,40,43,42,35])).
% 59.05/59.06 cnf(7007,plain,
% 59.05/59.06 (~P5(a18,a13)),
% 59.05/59.06 inference(scs_inference,[],[7000,4481])).
% 59.05/59.06 cnf(7009,plain,
% 59.05/59.06 (P4(f3(a16,f15(a16,a17,a18,a13)),f15(a16,a17,a18,a13))),
% 59.05/59.06 inference(scs_inference,[],[2140,69])).
% 59.05/59.06 cnf(7020,plain,
% 59.05/59.06 (~P5(a18,f19(a13,a13))),
% 59.05/59.06 inference(scs_inference,[],[7007,6989,6982,6997,2140,69,59,4563,61,60,63,105])).
% 59.05/59.06 cnf(7022,plain,
% 59.05/59.06 (~P5(f3(a16,f15(a18,a17,a16,a13)),a13)),
% 59.05/59.06 inference(scs_inference,[],[7007,6989,6982,6997,6973,2140,69,59,4563,61,60,63,105,45])).
% 59.05/59.06 cnf(7029,plain,
% 59.05/59.06 (E(a16,f3(a18,f15(a16,a17,a18,a13)))),
% 59.05/59.06 inference(scs_inference,[],[7007,6993,6989,6859,6982,6997,6991,6830,6973,6940,4163,108,52,2140,69,59,4563,61,60,63,105,45,66,35,42,70])).
% 59.05/59.06 cnf(7032,plain,
% 59.05/59.06 (E(f3(a18,f15(a16,a17,a18,a13)),a16)),
% 59.05/59.06 inference(scs_inference,[],[7007,6993,6989,6859,6982,6997,6991,6830,6973,6940,4163,108,52,2140,69,59,4563,61,60,63,105,45,66,35,42,70,4736,2])).
% 59.05/59.06 cnf(7062,plain,
% 59.05/59.06 (~P5(f3(a16,f15(a18,a17,a16,a13)),f15(a16,a17,a18,a13))),
% 59.05/59.06 inference(scs_inference,[],[7020,7009,7022,7029,7032,6938,107,4544,4458,59,4563,61,60,38,66])).
% 59.05/59.06 cnf(7098,plain,
% 59.05/59.06 (~P5(a18,f15(a16,a17,a18,a13))),
% 59.05/59.06 inference(scs_inference,[],[7062,6862,6832,6976,7007,59,61,60,66,45])).
% 59.05/59.06 cnf(7115,plain,
% 59.05/59.06 ($false),
% 59.05/59.06 inference(scs_inference,[],[7098,6940,59]),
% 59.05/59.06 ['proof']).
% 59.05/59.06 % SZS output end Proof
% 59.05/59.06 % Total time :58.380000s
%------------------------------------------------------------------------------