%------------------------------------------------------------------------------
% 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/sandbox/solver/bin/mcs_scs.jar %d %s
% Computer : n018.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 : Unsatisfiable 58.99s 59.01s
% Output : CNFRefutation 58.99s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.13 % Problem : GEO087-1 : TPTP v8.2.0. Released v2.4.0.
% 0.07/0.13 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% 0.13/0.34 % Computer : n018.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 08:45:54 EDT 2024
% 0.13/0.34 % CPUTime :
% 0.21/0.56 start to proof:theBenchmark
% 58.90/58.99 %-------------------------------------------
% 58.90/58.99 % File :CSE---1.7
% 58.90/58.99 % Problem :theBenchmark
% 58.90/58.99 % Transform :cnf
% 58.90/58.99 % Format :tptp:raw
% 58.90/58.99 % Command :java -jar mcs_scs.jar %d %s
% 58.90/58.99
% 58.90/58.99 % Result :Theorem 58.380000s
% 58.90/58.99 % Output :CNFRefutation 58.380000s
% 58.90/59.00 %-------------------------------------------
% 58.99/59.00 %--------------------------------------------------------------------------
% 58.99/59.00 % File : GEO087-1 : TPTP v8.2.0. Released v2.4.0.
% 58.99/59.00 % Domain : Geometry (Oriented curves)
% 58.99/59.00 % Problem : If one curve is part of another curve then they cannot meet
% 58.99/59.00 % Version : [EHK99] axioms.
% 58.99/59.00 % English :
% 58.99/59.00
% 58.99/59.00 % Refs : [KE99] Kulik & Eschenbach (1999), A Geometry of Oriented Curv
% 58.99/59.00 % : [EHK99] Eschenbach et al. (1999), Representing Simple Trajecto
% 58.99/59.00 % Source : [TPTP]
% 58.99/59.00 % Names :
% 58.99/59.00
% 58.99/59.00 % Status : Unsatisfiable
% 58.99/59.00 % Rating : 0.05 v7.4.0, 0.06 v7.3.0, 0.08 v7.0.0, 0.13 v6.4.0, 0.07 v6.3.0, 0.00 v6.2.0, 0.10 v6.1.0, 0.07 v6.0.0, 0.10 v5.5.0, 0.25 v5.4.0, 0.30 v5.3.0, 0.22 v5.2.0, 0.19 v5.1.0, 0.18 v5.0.0, 0.07 v4.1.0, 0.08 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.07 v3.2.0, 0.08 v3.1.0, 0.09 v2.7.0, 0.08 v2.6.0, 0.00 v2.4.0
% 58.99/59.00 % Syntax : Number of clauses : 50 ( 3 unt; 21 nHn; 45 RR)
% 58.99/59.00 % Number of literals : 156 ( 21 equ; 78 neg)
% 58.99/59.00 % Maximal clause size : 12 ( 3 avg)
% 58.99/59.00 % Maximal term depth : 3 ( 1 avg)
% 58.99/59.00 % Number of predicates : 8 ( 7 usr; 0 prp; 1-3 aty)
% 58.99/59.00 % Number of functors : 17 ( 17 usr; 3 con; 0-3 aty)
% 58.99/59.00 % Number of variables : 126 ( 10 sgn)
% 58.99/59.00 % SPC : CNF_UNS_RFO_SEQ_NHN
% 58.99/59.00
% 58.99/59.00 % Comments : Created by tptp2X -f tptp -t clausify:otter GEO087+1.p
% 58.99/59.00 %--------------------------------------------------------------------------
% 58.99/59.00 %----Include simple curve axioms
% 58.99/59.01 include('Axioms/GEO004-0.ax').
% 58.99/59.01 %--------------------------------------------------------------------------
% 58.99/59.01 cnf(corollary_2_9_67,negated_conjecture,
% 58.99/59.01 part_of(sk14,sk15) ).
% 58.99/59.01
% 58.99/59.01 cnf(corollary_2_9_68,negated_conjecture,
% 58.99/59.01 meet(sk16,sk14,sk15) ).
% 58.99/59.01
% 58.99/59.01 %--------------------------------------------------------------------------
% 58.99/59.01 %-------------------------------------------
% 58.99/59.01 % Proof found
% 58.99/59.01 % SZS status Theorem for theBenchmark
% 58.99/59.01 % SZS output start Proof
% 58.99/59.01 %ClaNum:88(EqnAxiom:43)
% 58.99/59.01 %VarNum:331(SingletonVarNum:113)
% 58.99/59.01 %MaxLitNum:12
% 58.99/59.01 %MaxfuncDepth:2
% 58.99/59.01 %SharedTerms:5
% 58.99/59.01 %goalClause: 44 46
% 58.99/59.01 %singleGoalClaCount:2
% 58.99/59.01 [44]P1(a1,a15)
% 58.99/59.01 [46]P6(a16,a1,a15)
% 58.99/59.01 [45]P2(f2(x451),x451)
% 58.99/59.01 [47]P3(x471)+P4(f3(x471),x471)
% 58.99/59.01 [49]~P7(x491)+P4(f13(x491),x491)
% 58.99/59.01 [48]P7(x481)+~P4(x482,x481)
% 58.99/59.01 [51]~P3(x511)+~P4(x512,x511)
% 58.99/59.01 [52]~P4(x521,x522)+P5(x521,x522)
% 58.99/59.01 [53]~P2(x531,x532)+P5(x531,x532)
% 58.99/59.01 [54]~P2(x541,x542)+~P4(x541,x542)
% 58.99/59.01 [55]~P4(x551,x552)+~E(f4(x551,x552),x551)
% 58.99/59.01 [57]P1(x571,x572)+P5(f5(x571,x572),x571)
% 58.99/59.01 [61]~P4(x611,x612)+P4(f4(x611,x612),x612)
% 58.99/59.01 [68]P1(x681,x682)+~P5(f5(x681,x682),x682)
% 58.99/59.01 [75]~P2(x751,x752)+P6(x751,f14(x751,x752),f6(x751,x752))
% 58.99/59.01 [70]~P2(x701,x702)+E(f17(f14(x701,x702),f6(x701,x702)),x702)
% 58.99/59.01 [71]P5(x711,x712)+~P6(x711,x713,x712)
% 58.99/59.01 [72]P5(x721,x722)+~P6(x721,x722,x723)
% 58.99/59.01 [73]~P6(x733,x732,x731)+E(f9(x731,x732),f17(x732,x731))
% 58.99/59.01 [50]P7(x501)+~P1(x501,x502)+E(x501,x502)
% 58.99/59.01 [56]P2(x561,x562)+~P5(x561,x562)+P4(x561,x562)
% 58.99/59.01 [64]~P5(x641,x642)+P4(x641,x642)+P5(x641,f7(x642,x641))
% 58.99/59.01 [65]~P5(x651,x652)+P4(x651,x652)+P5(x651,f11(x652,x651))
% 58.99/59.01 [66]~P5(x661,x662)+P4(x661,x662)+P1(f7(x662,x661),x662)
% 58.99/59.01 [67]~P5(x671,x672)+P4(x671,x672)+P1(f11(x672,x671),x672)
% 58.99/59.01 [69]E(x691,x692)+P5(f8(x691,x692),x692)+P5(f8(x691,x692),x691)
% 58.99/59.01 [74]E(x741,x742)+~P5(f8(x741,x742),x742)+~P5(f8(x741,x742),x741)
% 58.99/59.01 [76]~P5(x761,x762)+P4(x761,x762)+~P1(f7(x762,x761),f11(x762,x761))
% 58.99/59.01 [77]~P5(x771,x772)+P4(x771,x772)+~P1(f11(x772,x771),f7(x772,x771))
% 58.99/59.01 [58]~P5(x581,x583)+P5(x581,x582)+~P1(x583,x582)
% 58.99/59.01 [86]~P5(f10(x863,x862,x861),x861)+~P5(f10(x863,x862,x861),x862)+E(x861,f17(x862,x863))
% 58.99/59.01 [87]~P5(f10(x873,x872,x871),x871)+~P5(f10(x873,x872,x871),x873)+E(x871,f17(x872,x873))
% 58.99/59.01 [59]~P5(x591,x594)+P5(x591,x592)+~E(x592,f17(x593,x594))
% 58.99/59.01 [60]~P5(x601,x603)+P5(x601,x602)+~E(x602,f17(x603,x604))
% 58.99/59.01 [82]~P5(x821,x823)+~P5(x821,x822)+P6(x821,x822,x823)+P5(f12(x823,x822,x821),x823)
% 58.99/59.01 [83]~P5(x831,x833)+~P5(x831,x832)+P6(x831,x832,x833)+P5(f12(x833,x832,x831),x832)
% 58.99/59.01 [85]P5(f10(x853,x852,x851),x851)+P5(f10(x853,x852,x851),x852)+P5(f10(x853,x852,x851),x853)+E(x851,f17(x852,x853))
% 58.99/59.01 [79]~P5(x791,x792)+P4(x791,x792)+~P6(x794,x793,x792)+~P5(x791,x793)
% 58.99/59.01 [80]~P5(x801,x802)+P4(x801,x802)+~P6(x804,x802,x803)+~P5(x801,x803)
% 58.99/59.01 [63]~P5(x631,x634)+P5(x631,x632)+P5(x631,x633)+~E(x634,f17(x633,x632))
% 58.99/59.01 [88]~P5(x881,x883)+~P5(x881,x882)+P6(x881,x882,x883)+~P4(f12(x883,x882,x881),x883)+~P4(f12(x883,x882,x881),x882)
% 58.99/59.01 [81]~P3(x814)+~P4(x811,x812)+P6(x811,x812,x813)+~P6(x815,x812,x813)+~E(x814,f17(x812,x813))
% 58.99/59.01 [62]E(x623,x621)+~P4(x621,x624)+~P4(x623,x624)+E(x621,x622)+E(x623,x622)+~P4(x622,x624)
% 58.99/59.01 [78]P1(x782,x781)+~P1(x782,x783)+~P5(x784,x782)+~P4(x784,x783)+P1(x781,x782)+~P1(x781,x783)+~P5(x784,x781)
% 58.99/59.01 [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)
% 58.99/59.01 %EqnAxiom
% 58.99/59.01 [1]E(x11,x11)
% 58.99/59.01 [2]E(x22,x21)+~E(x21,x22)
% 58.99/59.01 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 58.99/59.01 [4]~E(x41,x42)+E(f2(x41),f2(x42))
% 58.99/59.01 [5]~E(x51,x52)+E(f3(x51),f3(x52))
% 58.99/59.01 [6]~E(x61,x62)+E(f13(x61),f13(x62))
% 58.99/59.01 [7]~E(x71,x72)+E(f4(x71,x73),f4(x72,x73))
% 58.99/59.01 [8]~E(x81,x82)+E(f4(x83,x81),f4(x83,x82))
% 58.99/59.01 [9]~E(x91,x92)+E(f5(x91,x93),f5(x92,x93))
% 58.99/59.01 [10]~E(x101,x102)+E(f5(x103,x101),f5(x103,x102))
% 58.99/59.01 [11]~E(x111,x112)+E(f17(x111,x113),f17(x112,x113))
% 58.99/59.01 [12]~E(x121,x122)+E(f17(x123,x121),f17(x123,x122))
% 58.99/59.01 [13]~E(x131,x132)+E(f10(x131,x133,x134),f10(x132,x133,x134))
% 58.99/59.01 [14]~E(x141,x142)+E(f10(x143,x141,x144),f10(x143,x142,x144))
% 58.99/59.01 [15]~E(x151,x152)+E(f10(x153,x154,x151),f10(x153,x154,x152))
% 58.99/59.01 [16]~E(x161,x162)+E(f12(x161,x163,x164),f12(x162,x163,x164))
% 58.99/59.01 [17]~E(x171,x172)+E(f12(x173,x171,x174),f12(x173,x172,x174))
% 58.99/59.01 [18]~E(x181,x182)+E(f12(x183,x184,x181),f12(x183,x184,x182))
% 58.99/59.01 [19]~E(x191,x192)+E(f11(x191,x193),f11(x192,x193))
% 58.99/59.01 [20]~E(x201,x202)+E(f11(x203,x201),f11(x203,x202))
% 58.99/59.01 [21]~E(x211,x212)+E(f7(x211,x213),f7(x212,x213))
% 58.99/59.01 [22]~E(x221,x222)+E(f7(x223,x221),f7(x223,x222))
% 58.99/59.01 [23]~E(x231,x232)+E(f6(x231,x233),f6(x232,x233))
% 58.99/59.01 [24]~E(x241,x242)+E(f6(x243,x241),f6(x243,x242))
% 58.99/59.01 [25]~E(x251,x252)+E(f8(x251,x253),f8(x252,x253))
% 58.99/59.01 [26]~E(x261,x262)+E(f8(x263,x261),f8(x263,x262))
% 58.99/59.01 [27]~E(x271,x272)+E(f14(x271,x273),f14(x272,x273))
% 58.99/59.01 [28]~E(x281,x282)+E(f14(x283,x281),f14(x283,x282))
% 58.99/59.01 [29]~E(x291,x292)+E(f9(x291,x293),f9(x292,x293))
% 58.99/59.01 [30]~E(x301,x302)+E(f9(x303,x301),f9(x303,x302))
% 58.99/59.01 [31]P1(x312,x313)+~E(x311,x312)+~P1(x311,x313)
% 58.99/59.02 [32]P1(x323,x322)+~E(x321,x322)+~P1(x323,x321)
% 58.99/59.02 [33]P2(x332,x333)+~E(x331,x332)+~P2(x331,x333)
% 58.99/59.02 [34]P2(x343,x342)+~E(x341,x342)+~P2(x343,x341)
% 58.99/59.02 [35]P6(x352,x353,x354)+~E(x351,x352)+~P6(x351,x353,x354)
% 58.99/59.02 [36]P6(x363,x362,x364)+~E(x361,x362)+~P6(x363,x361,x364)
% 58.99/59.02 [37]P6(x373,x374,x372)+~E(x371,x372)+~P6(x373,x374,x371)
% 58.99/59.02 [38]~P3(x381)+P3(x382)+~E(x381,x382)
% 58.99/59.02 [39]P4(x392,x393)+~E(x391,x392)+~P4(x391,x393)
% 58.99/59.02 [40]P4(x403,x402)+~E(x401,x402)+~P4(x403,x401)
% 58.99/59.02 [41]~P7(x411)+P7(x412)+~E(x411,x412)
% 58.99/59.02 [42]P5(x422,x423)+~E(x421,x422)+~P5(x421,x423)
% 58.99/59.02 [43]P5(x433,x432)+~E(x431,x432)+~P5(x433,x431)
% 58.99/59.02
% 58.99/59.02 %-------------------------------------------
% 58.99/59.02 cnf(89,plain,
% 58.99/59.02 (~P5(x891,x892)+P5(x891,f17(x893,x892))),
% 58.99/59.02 inference(equality_inference,[],[59])).
% 58.99/59.02 cnf(90,plain,
% 58.99/59.02 (~P5(x901,x902)+P5(x901,f17(x902,x903))),
% 58.99/59.02 inference(equality_inference,[],[60])).
% 58.99/59.02 cnf(91,plain,
% 58.99/59.02 (~P5(x911,f17(x912,x913))+P5(x911,x913)+P5(x911,x912)),
% 58.99/59.02 inference(equality_inference,[],[63])).
% 58.99/59.02 cnf(93,plain,
% 58.99/59.02 (~P5(x931,a1)+P5(x931,a15)),
% 58.99/59.02 inference(scs_inference,[],[44,58])).
% 58.99/59.02 cnf(95,plain,
% 58.99/59.02 (~P5(x951,f17(a1,a1))+P5(x951,a15)),
% 58.99/59.02 inference(scs_inference,[],[44,58,91])).
% 58.99/59.02 cnf(116,plain,
% 58.99/59.02 (P6(x1161,a1,a15)+~E(a16,x1161)),
% 58.99/59.02 inference(scs_inference,[],[46,35])).
% 58.99/59.02 cnf(119,plain,
% 58.99/59.02 (P2(f2(x1191),x1192)+~E(x1191,x1192)),
% 58.99/59.02 inference(scs_inference,[],[44,46,45,35,31,36,34])).
% 58.99/59.02 cnf(120,plain,
% 58.99/59.02 (P1(a1,x1201)+~E(a15,x1201)),
% 58.99/59.02 inference(scs_inference,[],[44,46,45,35,31,36,34,32])).
% 58.99/59.02 cnf(131,plain,
% 58.99/59.02 (~P4(x1311,x1312)+P4(f13(x1312),x1312)),
% 58.99/59.02 inference(scs_inference,[],[48,49])).
% 58.99/59.02 cnf(132,plain,
% 58.99/59.02 (~P4(x1321,x1322)+P4(f3(x1322),x1322)),
% 58.99/59.02 inference(scs_inference,[],[51,47])).
% 58.99/59.02 cnf(133,plain,
% 58.99/59.02 (~P2(f4(x1331,x1332),x1332)+~P4(x1331,x1332)),
% 58.99/59.02 inference(scs_inference,[],[54,61])).
% 58.99/59.02 cnf(135,plain,
% 58.99/59.02 (P5(f13(x1351),x1351)+~P4(x1352,x1351)),
% 58.99/59.02 inference(scs_inference,[],[131,52])).
% 58.99/59.02 cnf(136,plain,
% 58.99/59.02 (~P4(x1361,x1362)+~E(f4(f3(x1362),x1362),f3(x1362))),
% 58.99/59.02 inference(scs_inference,[],[132,55])).
% 58.99/59.02 cnf(137,plain,
% 58.99/59.02 (~P4(x1371,x1372)+P5(f13(x1372),f17(x1373,x1372))),
% 58.99/59.02 inference(scs_inference,[],[135,89])).
% 58.99/59.02 cnf(150,plain,
% 58.99/59.02 (P5(f2(x1501),f17(x1501,x1502))),
% 58.99/59.02 inference(scs_inference,[],[45,90,53])).
% 58.99/59.02 cnf(165,plain,
% 58.99/59.02 (P5(f2(f17(a1,a1)),a15)),
% 58.99/59.02 inference(scs_inference,[],[45,95,53])).
% 58.99/59.02 cnf(168,plain,
% 58.99/59.02 (P5(f2(f17(a1,a1)),f17(x1681,a15))),
% 58.99/59.02 inference(scs_inference,[],[165,90,89])).
% 58.99/59.02 cnf(246,plain,
% 58.99/59.02 (P5(f2(f17(a1,a1)),x2461)+~E(a15,x2461)),
% 58.99/59.02 inference(scs_inference,[],[165,43])).
% 58.99/59.02 cnf(264,plain,
% 58.99/59.02 (P5(f2(f17(a1,a1)),x2641)+~E(f17(x2642,a15),x2641)),
% 58.99/59.02 inference(scs_inference,[],[168,43])).
% 58.99/59.02 cnf(265,plain,
% 58.99/59.02 (P5(f2(f17(a1,a1)),f17(x2651,x2652))+~E(f17(x2653,a15),x2652)),
% 58.99/59.02 inference(scs_inference,[],[168,43,89])).
% 58.99/59.02 cnf(267,plain,
% 58.99/59.02 (P5(f2(f17(a1,a1)),f17(x2671,x2672))+~E(f17(x2673,a15),x2671)),
% 58.99/59.02 inference(scs_inference,[],[168,43,89,90])).
% 58.99/59.02 cnf(301,plain,
% 58.99/59.02 (P5(f2(x3011),x3012)+~E(f17(x3011,x3013),x3012)),
% 58.99/59.02 inference(scs_inference,[],[150,43])).
% 58.99/59.02 cnf(407,plain,
% 58.99/59.02 (~E(f3(x4071),f4(f3(x4071),x4071))+~P4(x4072,x4071)),
% 58.99/59.02 inference(scs_inference,[],[136,2])).
% 58.99/59.02 cnf(524,plain,
% 58.99/59.02 (P7(x5241)+P3(x5241)),
% 58.99/59.02 inference(scs_inference,[],[48,47])).
% 58.99/59.02 cnf(594,plain,
% 58.99/59.02 (~P3(x5941)+~P7(x5941)),
% 58.99/59.02 inference(scs_inference,[],[51,49])).
% 58.99/59.02 cnf(597,plain,
% 58.99/59.02 (~P7(x5971)+P4(f3(x5971),x5971)),
% 58.99/59.02 inference(scs_inference,[],[594,47])).
% 58.99/59.02 cnf(598,plain,
% 58.99/59.02 (P5(f3(x5981),x5981)+~P7(x5981)),
% 58.99/59.02 inference(scs_inference,[],[597,52])).
% 58.99/59.02 cnf(599,plain,
% 58.99/59.02 (P5(f3(x5991),x5991)+~P4(x5992,x5991)),
% 58.99/59.02 inference(scs_inference,[],[598,48])).
% 58.99/59.02 cnf(600,plain,
% 58.99/59.02 (~P4(x6001,x6002)+P5(f3(x6002),f17(x6003,x6002))),
% 58.99/59.02 inference(scs_inference,[],[599,89])).
% 58.99/59.02 cnf(601,plain,
% 58.99/59.02 (P5(f3(x6011),f17(x6012,x6011))+~P7(x6011)),
% 58.99/59.02 inference(scs_inference,[],[600,49])).
% 58.99/59.02 cnf(658,plain,
% 58.99/59.02 (E(a1,a15)+~P3(a1)),
% 58.99/59.02 inference(scs_inference,[],[44,594,50])).
% 58.99/59.02 cnf(659,plain,
% 58.99/59.02 (E(a15,a1)+~P3(a1)),
% 58.99/59.02 inference(scs_inference,[],[658,2])).
% 58.99/59.02 cnf(832,plain,
% 58.99/59.02 (~P3(a1)+P3(a15)),
% 58.99/59.02 inference(scs_inference,[],[658,38])).
% 58.99/59.02 cnf(840,plain,
% 58.99/59.02 (~P4(x8401,a15)+~P3(a1)),
% 58.99/59.02 inference(scs_inference,[],[832,51])).
% 58.99/59.02 cnf(841,plain,
% 58.99/59.02 (~P7(a15)+~P3(a1)),
% 58.99/59.02 inference(scs_inference,[],[840,49])).
% 58.99/59.02 cnf(874,plain,
% 58.99/59.02 (E(a15,x8741)+~P1(a15,x8741)+~P3(a1)),
% 58.99/59.02 inference(scs_inference,[],[841,50])).
% 58.99/59.02 cnf(910,plain,
% 58.99/59.02 (P1(a1,a1)+~P3(a1)),
% 58.99/59.02 inference(scs_inference,[],[659,120])).
% 58.99/59.02 cnf(911,plain,
% 58.99/59.02 (P1(x9111,a1)+~E(a1,x9111)+~P3(a1)),
% 58.99/59.03 inference(scs_inference,[],[910,31])).
% 58.99/59.03 cnf(918,plain,
% 58.99/59.03 (P5(f2(f17(a1,a1)),a1)+~P3(a1)),
% 58.99/59.03 inference(scs_inference,[],[659,246])).
% 58.99/59.03 cnf(919,plain,
% 58.99/59.03 (P4(f2(f17(a1,a1)),a1)+~P6(x9191,a1,a1)+~P3(a1)),
% 58.99/59.03 inference(scs_inference,[],[918,80])).
% 58.99/59.03 cnf(920,plain,
% 58.99/59.03 (P7(a1)+~P6(x9201,a1,a1)+~P3(a1)),
% 58.99/59.03 inference(scs_inference,[],[919,48])).
% 58.99/59.03 cnf(921,plain,
% 58.99/59.03 (~E(a15,a1)+P7(a1)+~P3(a1)),
% 58.99/59.03 inference(scs_inference,[],[46,920,37])).
% 58.99/59.03 cnf(922,plain,
% 58.99/59.03 (~P1(a15,a1)+P7(a1)+~P3(a1)),
% 58.99/59.03 inference(scs_inference,[],[921,874])).
% 58.99/59.03 cnf(923,plain,
% 58.99/59.03 (~E(a1,a15)+P7(a1)+~P3(a1)),
% 58.99/59.03 inference(scs_inference,[],[922,911])).
% 58.99/59.03 cnf(924,plain,
% 58.99/59.03 (P7(a1)+~P3(a1)),
% 58.99/59.03 inference(scs_inference,[],[44,923,50])).
% 58.99/59.03 cnf(925,plain,
% 58.99/59.03 (P4(f13(a1),a1)+~P3(a1)),
% 58.99/59.03 inference(scs_inference,[],[924,49])).
% 58.99/59.03 cnf(926,plain,
% 58.99/59.03 (~P3(a1)),
% 58.99/59.03 inference(scs_inference,[],[925,51])).
% 58.99/59.03 cnf(927,plain,
% 58.99/59.03 (P7(a1)),
% 58.99/59.03 inference(scs_inference,[],[926,524])).
% 58.99/59.03 cnf(929,plain,
% 58.99/59.03 (P5(f3(a1),a1)),
% 58.99/59.03 inference(scs_inference,[],[926,524,598])).
% 58.99/59.03 cnf(931,plain,
% 58.99/59.03 (P5(f3(a1),f17(x9311,a1))),
% 58.99/59.03 inference(scs_inference,[],[926,524,598,601])).
% 58.99/59.03 cnf(935,plain,
% 58.99/59.03 (P5(f3(a1),f17(a1,x9351))),
% 58.99/59.03 inference(scs_inference,[],[926,524,598,601,89,90])).
% 58.99/59.03 cnf(937,plain,
% 58.99/59.03 (P5(f3(a1),a15)),
% 58.99/59.03 inference(scs_inference,[],[44,926,524,598,601,89,90,58])).
% 58.99/59.03 cnf(947,plain,
% 58.99/59.03 (P2(f3(a1),a1)+~E(f2(a1),f4(f3(a1),a1))),
% 58.99/59.03 inference(scs_inference,[],[44,46,45,926,524,598,601,89,90,58,56,137,133,54,40,39,32,36,33])).
% 58.99/59.03 cnf(952,plain,
% 58.99/59.03 (P5(f3(a1),f17(x9521,a15))),
% 58.99/59.03 inference(scs_inference,[],[937,89])).
% 58.99/59.03 cnf(1015,plain,
% 58.99/59.03 (P2(f3(a1),f17(a15,a1))+P4(x10151,f17(a15,a1))+~E(f3(a1),x10151)),
% 58.99/59.03 inference(scs_inference,[],[931,56,600,133,137,54,39])).
% 58.99/59.03 cnf(1294,plain,
% 58.99/59.03 (~P4(f3(a1),a1)+~E(f2(a1),f4(f3(a1),a1))),
% 58.99/59.03 inference(scs_inference,[],[947,54])).
% 58.99/59.03 cnf(1297,plain,
% 58.99/59.03 (~E(f2(a1),f4(f3(a1),a1))),
% 58.99/59.03 inference(scs_inference,[],[926,1294,47])).
% 58.99/59.03 cnf(1420,plain,
% 58.99/59.03 (E(f17(a1,a15),f9(a15,a1))),
% 58.99/59.03 inference(scs_inference,[],[46,2,73])).
% 58.99/59.03 cnf(1421,plain,
% 58.99/59.03 (P2(f2(f17(a1,a15)),f9(a15,a1))),
% 58.99/59.03 inference(scs_inference,[],[1420,119])).
% 58.99/59.03 cnf(1427,plain,
% 58.99/59.03 (E(f9(a15,a1),f17(a1,a15))),
% 58.99/59.03 inference(scs_inference,[],[1420,119,265,267,264,2])).
% 58.99/59.03 cnf(1428,plain,
% 58.99/59.03 (P5(f3(a1),f9(a15,a1))),
% 58.99/59.03 inference(scs_inference,[],[1420,929,119,265,267,264,2,60])).
% 58.99/59.03 cnf(1430,plain,
% 58.99/59.03 (P5(f2(a1),f9(a15,a1))),
% 58.99/59.03 inference(scs_inference,[],[150,1420,929,119,265,267,264,2,60,43])).
% 58.99/59.03 cnf(1434,plain,
% 58.99/59.03 (P5(f3(a1),f17(f9(a15,a1),x14341))),
% 58.99/59.03 inference(scs_inference,[],[150,1420,929,119,265,267,264,2,60,43,89,90])).
% 58.99/59.03 cnf(1453,plain,
% 58.99/59.03 (P2(f2(f9(a15,a1)),f17(a1,a15))),
% 58.99/59.03 inference(scs_inference,[],[1427,119])).
% 58.99/59.03 cnf(1611,plain,
% 58.99/59.03 (~P3(f9(a15,a1))+P6(x16111,a1,a15)+~E(f3(a1),x16112)+~P4(x16111,a1)),
% 58.99/59.03 inference(scs_inference,[],[46,165,1427,1428,1434,42,81])).
% 58.99/59.03 cnf(1613,plain,
% 58.99/59.03 (~P3(f9(a15,a1))+~P4(x16131,a1)+P6(x16131,a1,a15)),
% 58.99/59.03 inference(equality_inference,[],[1611])).
% 58.99/59.03 cnf(3908,plain,
% 58.99/59.03 (P4(f3(a1),a1)),
% 58.99/59.03 inference(scs_inference,[],[926,47])).
% 58.99/59.03 cnf(3910,plain,
% 58.99/59.03 (P4(f13(a1),a1)),
% 58.99/59.03 inference(scs_inference,[],[927,926,47,49])).
% 58.99/59.03 cnf(3912,plain,
% 58.99/59.03 (P5(f13(a1),a1)),
% 58.99/59.03 inference(scs_inference,[],[927,926,47,49,135])).
% 58.99/59.03 cnf(3919,plain,
% 58.99/59.03 (P5(f2(a1),a15)),
% 58.99/59.03 inference(scs_inference,[],[927,926,150,1420,47,49,135,55,61,6,95])).
% 58.99/59.03 cnf(3950,plain,
% 58.99/59.03 (P5(a16,a15)),
% 58.99/59.03 inference(scs_inference,[],[927,926,150,45,1420,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,407,13,14,15,16,17,18,71])).
% 58.99/59.03 cnf(3952,plain,
% 58.99/59.03 (P5(a16,a1)),
% 58.99/59.03 inference(scs_inference,[],[927,926,150,45,1420,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,407,13,14,15,16,17,18,71,72])).
% 58.99/59.03 cnf(3964,plain,
% 58.99/59.03 (P5(f13(a1),f9(a15,a1))),
% 58.99/59.03 inference(scs_inference,[],[927,926,1421,150,1297,45,1420,1427,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,407,13,14,15,16,17,18,71,72,52,53,54,2,4,59,60])).
% 58.99/59.03 cnf(3968,plain,
% 58.99/59.03 (P4(a16,a1)),
% 58.99/59.03 inference(scs_inference,[],[927,926,1421,150,1297,45,1420,1427,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,407,13,14,15,16,17,18,71,72,52,53,54,2,4,59,60,3,40,80])).
% 58.99/59.03 cnf(3970,plain,
% 58.99/59.03 (~P6(x39701,f9(a15,a1),f9(a15,a1))),
% 58.99/59.03 inference(scs_inference,[],[927,926,1421,150,1297,45,1420,1427,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,407,13,14,15,16,17,18,71,72,52,53,54,2,4,59,60,3,40,80,79])).
% 58.99/59.03 cnf(3972,plain,
% 58.99/59.03 (P5(f13(a1),a15)),
% 58.99/59.03 inference(scs_inference,[],[927,926,1421,150,1297,45,1420,1427,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,407,13,14,15,16,17,18,71,72,52,53,54,2,4,59,60,3,40,80,79,93])).
% 58.99/59.03 cnf(3977,plain,
% 58.99/59.03 (~P6(x39771,f9(a15,a1),f17(a1,a15))),
% 58.99/59.03 inference(scs_inference,[],[927,926,1421,1434,150,1297,45,1420,1427,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,407,13,14,15,16,17,18,71,72,52,53,54,2,4,59,60,3,40,80,79,93,301,64,37])).
% 58.99/59.03 cnf(3978,plain,
% 58.99/59.03 (~P6(x39781,f17(a1,a15),f9(a15,a1))),
% 58.99/59.03 inference(scs_inference,[],[927,926,1421,1434,150,1297,45,1420,1427,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,407,13,14,15,16,17,18,71,72,52,53,54,2,4,59,60,3,40,80,79,93,301,64,37,36])).
% 58.99/59.03 cnf(3981,plain,
% 58.99/59.03 (P5(f12(f9(a15,a1),f9(a15,a1),f2(a1)),f9(a15,a1))),
% 58.99/59.03 inference(scs_inference,[],[44,927,926,1421,1434,1430,150,1297,45,1420,1427,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,407,13,14,15,16,17,18,71,72,52,53,54,2,4,59,60,3,40,80,79,93,301,64,37,36,58,82])).
% 58.99/59.03 cnf(3983,plain,
% 58.99/59.03 (~P4(f12(f9(a15,a1),f9(a15,a1),f2(a1)),f9(a15,a1))),
% 58.99/59.03 inference(scs_inference,[],[44,927,926,1421,1434,1430,150,1297,45,1420,1427,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,407,13,14,15,16,17,18,71,72,52,53,54,2,4,59,60,3,40,80,79,93,301,64,37,36,58,82,88])).
% 58.99/59.03 cnf(3990,plain,
% 58.99/59.03 (~E(f4(a16,a1),a16)),
% 58.99/59.03 inference(scs_inference,[],[3968,55])).
% 58.99/59.03 cnf(3994,plain,
% 58.99/59.03 (P4(f4(a16,a1),a1)),
% 58.99/59.03 inference(scs_inference,[],[3968,1453,55,53,61])).
% 58.99/59.03 cnf(3999,plain,
% 58.99/59.03 (P2(f12(f9(a15,a1),f9(a15,a1),f2(a1)),f9(a15,a1))),
% 58.99/59.03 inference(scs_inference,[],[3968,3983,3981,1453,55,53,61,54,2,56])).
% 58.99/59.03 cnf(4001,plain,
% 58.99/59.03 (~P6(x40011,f17(a1,a15),f17(a1,a15))),
% 58.99/59.03 inference(scs_inference,[],[3968,3977,3983,3981,1453,1420,55,53,61,54,2,56,36])).
% 58.99/59.03 cnf(4004,plain,
% 58.99/59.03 (P5(f3(a1),f17(a1,x40041))),
% 58.99/59.03 inference(rename_variables,[],[935])).
% 58.99/59.03 cnf(4005,plain,
% 58.99/59.03 (~P6(x40051,f17(a1,a15),f9(a15,a1))),
% 58.99/59.03 inference(rename_variables,[],[3978])).
% 58.99/59.03 cnf(4011,plain,
% 58.99/59.03 (P4(a16,a15)),
% 58.99/59.03 inference(scs_inference,[],[3950,3952,3968,3977,3978,4005,3983,3981,1453,935,4004,1428,1420,46,55,53,61,54,2,56,36,40,83,82,79])).
% 58.99/59.03 cnf(4021,plain,
% 58.99/59.03 (P5(f4(a16,a1),a1)),
% 58.99/59.03 inference(scs_inference,[],[3950,3952,3968,3977,3978,4005,3983,3981,1453,935,4004,1428,1420,46,55,53,61,54,2,56,36,40,83,82,79,131,132,599,136,52])).
% 58.99/59.03 cnf(4027,plain,
% 58.99/59.03 (P5(f13(a15),a15)),
% 58.99/59.03 inference(scs_inference,[],[3950,3952,3968,3977,3978,4005,3983,3981,1453,935,4004,1428,1420,46,55,53,61,54,2,56,36,40,83,82,79,131,132,599,136,52,407,51,135])).
% 58.99/59.03 cnf(4033,plain,
% 58.99/59.03 (P5(f13(a1),f17(a1,a15))),
% 58.99/59.03 inference(scs_inference,[],[3950,3952,3968,3977,3978,4005,3964,3983,3981,1453,935,4004,1428,1420,1427,46,55,53,61,54,2,56,36,40,83,82,79,131,132,599,136,52,407,51,135,48,66,43])).
% 58.99/59.03 cnf(4059,plain,
% 58.99/59.03 (~E(f4(a16,a15),a16)),
% 58.99/59.03 inference(scs_inference,[],[4011,55])).
% 58.99/59.03 cnf(4063,plain,
% 58.99/59.03 (P5(f2(x40631),x40631)),
% 58.99/59.03 inference(scs_inference,[],[4011,4021,45,55,93,53])).
% 58.99/59.03 cnf(4065,plain,
% 58.99/59.03 (~P4(f2(x40651),x40651)),
% 58.99/59.03 inference(scs_inference,[],[4011,4021,45,55,93,53,54])).
% 58.99/59.03 cnf(4067,plain,
% 58.99/59.03 (P4(f4(a16,a15),a15)),
% 58.99/59.03 inference(scs_inference,[],[4011,4021,45,55,93,53,54,61])).
% 58.99/59.03 cnf(4069,plain,
% 58.99/59.03 (~E(a16,f4(a16,a15))),
% 58.99/59.03 inference(scs_inference,[],[4011,4021,45,55,93,53,54,61,2])).
% 58.99/59.03 cnf(4080,plain,
% 58.99/59.03 (P4(f4(a16,a1),a15)),
% 58.99/59.03 inference(scs_inference,[],[4011,4001,4033,4021,3977,3964,45,46,55,93,53,54,61,2,66,65,83,82,79])).
% 58.99/59.03 cnf(4088,plain,
% 58.99/59.03 (P2(f12(f9(a15,a1),f9(a15,a1),f2(a1)),f17(a1,a15))),
% 58.99/59.03 inference(scs_inference,[],[44,4011,3908,4001,4033,4021,3999,3977,3964,45,1427,46,55,93,53,54,61,2,66,65,83,82,79,78,52,1613,34])).
% 58.99/59.03 cnf(4120,plain,
% 58.99/59.03 (P5(f2(x41201),x41201)),
% 58.99/59.03 inference(rename_variables,[],[4063])).
% 58.99/59.03 cnf(4123,plain,
% 58.99/59.03 (P5(f2(x41231),x41231)),
% 58.99/59.03 inference(rename_variables,[],[4063])).
% 58.99/59.03 cnf(4132,plain,
% 58.99/59.03 (~P6(x41321,x41322,x41322)),
% 58.99/59.03 inference(scs_inference,[],[4063,4120,4123,4065,4080,4088,3970,4001,3964,952,55,53,61,2,67,64,83,82,79])).
% 58.99/59.03 cnf(4134,plain,
% 58.99/59.03 (P5(f2(x41341),x41341)),
% 58.99/59.03 inference(rename_variables,[],[4063])).
% 58.99/59.03 cnf(4143,plain,
% 58.99/59.03 (E(f4(f4(a16,a1),a15),a16)),
% 58.99/59.03 inference(scs_inference,[],[4063,4120,4123,4134,4065,3990,4080,4088,3970,4001,3964,4011,952,55,53,61,2,67,64,83,82,79,88,52,1015,62])).
% 58.99/59.03 cnf(4154,plain,
% 58.99/59.03 (~P6(x41541,x41542,x41542)),
% 58.99/59.03 inference(rename_variables,[],[4132])).
% 58.99/59.03 cnf(4156,plain,
% 58.99/59.03 (~P6(x41561,x41562,x41562)),
% 58.99/59.03 inference(rename_variables,[],[4132])).
% 58.99/59.03 cnf(4159,plain,
% 58.99/59.03 (~P6(x41591,x41592,x41592)),
% 58.99/59.03 inference(rename_variables,[],[4132])).
% 58.99/59.03 cnf(4168,plain,
% 58.99/59.03 (P6(f4(f4(a16,a15),a15),a1,a15)),
% 58.99/59.03 inference(scs_inference,[],[4132,4154,4156,4159,4027,3972,4069,4059,4143,3912,4067,4011,46,55,61,2,37,36,3,83,82,79,62,116])).
% 58.99/59.03 cnf(4263,plain,
% 58.99/59.03 (~E(f4(f4(a16,a1),a1),f4(a16,a1))),
% 58.99/59.03 inference(scs_inference,[],[3994,55])).
% 58.99/59.03 cnf(4296,plain,
% 58.99/59.03 ($false),
% 58.99/59.03 inference(scs_inference,[],[4263,3919,4168,3910,4063,4065,61,52,2,80]),
% 58.99/59.03 ['proof']).
% 58.99/59.03 % SZS output end Proof
% 58.99/59.03 % Total time :58.380000s
%------------------------------------------------------------------------------