%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : GEO093-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 : n001.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Mon Jun 24 06:03:46 EDT 2024
% Result : Unsatisfiable 58.71s 58.83s
% Output : CNFRefutation 58.79s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.09/0.14 % Problem : GEO093-1 : TPTP v8.2.0. Released v2.4.0.
% 0.09/0.14 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% 0.13/0.35 % Computer : n001.cluster.edu
% 0.13/0.35 % Model : x86_64 x86_64
% 0.13/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.35 % Memory : 8042.1875MB
% 0.13/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.35 % CPULimit : 300
% 0.13/0.35 % WCLimit : 300
% 0.13/0.35 % DateTime : Fri Jun 21 07:42:08 EDT 2024
% 0.13/0.36 % CPUTime :
% 0.50/0.64 start to proof:theBenchmark
% 58.71/58.81 %-------------------------------------------
% 58.71/58.81 % File :CSE---1.7
% 58.71/58.81 % Problem :theBenchmark
% 58.71/58.81 % Transform :cnf
% 58.71/58.81 % Format :tptp:raw
% 58.71/58.81 % Command :java -jar mcs_scs.jar %d %s
% 58.71/58.81
% 58.71/58.81 % Result :Theorem 58.120000s
% 58.71/58.81 % Output :CNFRefutation 58.120000s
% 58.71/58.81 %-------------------------------------------
% 58.71/58.82 %--------------------------------------------------------------------------
% 58.71/58.82 % File : GEO093-1 : TPTP v8.2.0. Released v2.4.0.
% 58.71/58.82 % Domain : Geometry (Oriented curves)
% 58.71/58.82 % Problem : Sum of meeting open curves is open
% 58.71/58.82 % Version : [EHK99] axioms.
% 58.71/58.82 % English : If two open sub-curves of an open curve meet, then their sum
% 58.71/58.82 % is also open.
% 58.71/58.82
% 58.71/58.82 % Refs : [KE99] Kulik & Eschenbach (1999), A Geometry of Oriented Curv
% 58.71/58.82 % : [EHK99] Eschenbach et al. (1999), Representing Simple Trajecto
% 58.71/58.82 % Source : [TPTP]
% 58.71/58.82 % Names :
% 58.71/58.82
% 58.71/58.82 % Status : Unsatisfiable
% 58.71/58.82 % Rating : 0.30 v8.2.0, 0.33 v8.1.0, 0.37 v7.5.0, 0.32 v7.4.0, 0.35 v7.3.0, 0.50 v7.1.0, 0.42 v7.0.0, 0.53 v6.4.0, 0.33 v6.3.0, 0.36 v6.2.0, 0.40 v6.1.0, 0.64 v6.0.0, 0.70 v5.5.0, 0.80 v5.3.0, 0.83 v5.2.0, 0.75 v5.1.0, 0.76 v5.0.0, 0.64 v4.1.0, 0.69 v4.0.1, 0.64 v4.0.0, 0.55 v3.7.0, 0.40 v3.5.0, 0.55 v3.4.0, 0.67 v3.3.0, 0.71 v3.2.0, 0.69 v3.1.0, 0.55 v2.7.0, 0.58 v2.6.0, 0.56 v2.4.0
% 58.71/58.82 % Syntax : Number of clauses : 53 ( 6 unt; 21 nHn; 48 RR)
% 58.71/58.83 % Number of literals : 159 ( 21 equ; 79 neg)
% 58.71/58.83 % Maximal clause size : 12 ( 3 avg)
% 58.71/58.83 % Maximal term depth : 3 ( 1 avg)
% 58.71/58.83 % Number of predicates : 8 ( 7 usr; 0 prp; 1-3 aty)
% 58.71/58.83 % Number of functors : 18 ( 18 usr; 4 con; 0-3 aty)
% 58.71/58.83 % Number of variables : 126 ( 10 sgn)
% 58.71/58.83 % SPC : CNF_UNS_RFO_SEQ_NHN
% 58.71/58.83
% 58.71/58.83 % Comments : Created by tptp2X -f tptp -t clausify:otter GEO093+1.p
% 58.71/58.83 %--------------------------------------------------------------------------
% 58.71/58.83 %----Include simple curve axioms
% 58.71/58.83 include('Axioms/GEO004-0.ax').
% 58.71/58.83 %--------------------------------------------------------------------------
% 58.71/58.83 cnf(proposition_2_14_2_67,negated_conjecture,
% 58.71/58.83 open(sk14) ).
% 58.71/58.83
% 58.71/58.83 cnf(proposition_2_14_2_68,negated_conjecture,
% 58.71/58.83 part_of(sk15,sk14) ).
% 58.71/58.83
% 58.71/58.83 cnf(proposition_2_14_2_69,negated_conjecture,
% 58.71/58.83 part_of(sk16,sk14) ).
% 58.71/58.83
% 58.71/58.83 cnf(proposition_2_14_2_70,negated_conjecture,
% 58.71/58.83 meet(sk17,sk15,sk16) ).
% 58.71/58.83
% 58.71/58.83 cnf(proposition_2_14_2_71,negated_conjecture,
% 58.71/58.83 ~ open(sum(sk15,sk16)) ).
% 58.71/58.83
% 58.71/58.83 %--------------------------------------------------------------------------
% 58.71/58.83 %-------------------------------------------
% 58.71/58.83 % Proof found
% 58.71/58.83 % SZS status Theorem for theBenchmark
% 58.71/58.83 % SZS output start Proof
% 58.76/58.84 %ClaNum:91(EqnAxiom:43)
% 58.76/58.84 %VarNum:331(SingletonVarNum:113)
% 58.76/58.84 %MaxLitNum:12
% 58.76/58.84 %MaxfuncDepth:2
% 58.76/58.84 %SharedTerms:10
% 58.76/58.84 %goalClause: 44 45 46 48 49
% 58.76/58.84 %singleGoalClaCount:5
% 58.76/58.84 [44]P1(a1)
% 58.76/58.84 [45]P7(a15,a1)
% 58.76/58.84 [46]P7(a16,a1)
% 58.76/58.84 [48]P6(a17,a15,a16)
% 58.76/58.84 [49]~P1(f18(a15,a16))
% 58.76/58.84 [47]P2(f2(x471),x471)
% 58.76/58.84 [50]P3(x501)+P4(f3(x501),x501)
% 58.76/58.84 [52]~P1(x521)+P4(f13(x521),x521)
% 58.76/58.84 [51]P1(x511)+~P4(x512,x511)
% 58.76/58.84 [54]~P3(x541)+~P4(x542,x541)
% 58.76/58.84 [55]~P4(x551,x552)+P5(x551,x552)
% 58.76/58.84 [56]~P2(x561,x562)+P5(x561,x562)
% 58.76/58.84 [57]~P2(x571,x572)+~P4(x571,x572)
% 58.76/58.84 [58]~P4(x581,x582)+~E(f4(x581,x582),x581)
% 58.76/58.84 [60]P7(x601,x602)+P5(f5(x601,x602),x601)
% 58.76/58.84 [64]~P4(x641,x642)+P4(f4(x641,x642),x642)
% 58.76/58.84 [71]P7(x711,x712)+~P5(f5(x711,x712),x712)
% 58.76/58.84 [78]~P2(x781,x782)+P6(x781,f14(x781,x782),f6(x781,x782))
% 58.76/58.84 [73]~P2(x731,x732)+E(f18(f14(x731,x732),f6(x731,x732)),x732)
% 58.76/58.84 [74]P5(x741,x742)+~P6(x741,x743,x742)
% 58.76/58.84 [75]P5(x751,x752)+~P6(x751,x752,x753)
% 58.76/58.84 [76]~P6(x763,x762,x761)+E(f9(x761,x762),f18(x762,x761))
% 58.76/58.84 [53]P1(x531)+~P7(x531,x532)+E(x531,x532)
% 58.76/58.84 [59]P2(x591,x592)+~P5(x591,x592)+P4(x591,x592)
% 58.76/58.84 [67]~P5(x671,x672)+P4(x671,x672)+P5(x671,f7(x672,x671))
% 58.76/58.84 [68]~P5(x681,x682)+P4(x681,x682)+P5(x681,f11(x682,x681))
% 58.76/58.84 [69]~P5(x691,x692)+P4(x691,x692)+P7(f7(x692,x691),x692)
% 58.76/58.84 [70]~P5(x701,x702)+P4(x701,x702)+P7(f11(x702,x701),x702)
% 58.76/58.84 [72]E(x721,x722)+P5(f8(x721,x722),x722)+P5(f8(x721,x722),x721)
% 58.76/58.84 [77]E(x771,x772)+~P5(f8(x771,x772),x772)+~P5(f8(x771,x772),x771)
% 58.76/58.84 [79]~P5(x791,x792)+P4(x791,x792)+~P7(f7(x792,x791),f11(x792,x791))
% 58.76/58.84 [80]~P5(x801,x802)+P4(x801,x802)+~P7(f11(x802,x801),f7(x802,x801))
% 58.76/58.84 [61]~P5(x611,x613)+P5(x611,x612)+~P7(x613,x612)
% 58.76/58.84 [89]~P5(f10(x893,x892,x891),x891)+~P5(f10(x893,x892,x891),x892)+E(x891,f18(x892,x893))
% 58.76/58.84 [90]~P5(f10(x903,x902,x901),x901)+~P5(f10(x903,x902,x901),x903)+E(x901,f18(x902,x903))
% 58.76/58.84 [62]~P5(x621,x624)+P5(x621,x622)+~E(x622,f18(x623,x624))
% 58.76/58.84 [63]~P5(x631,x633)+P5(x631,x632)+~E(x632,f18(x633,x634))
% 58.76/58.84 [85]~P5(x851,x853)+~P5(x851,x852)+P6(x851,x852,x853)+P5(f12(x853,x852,x851),x853)
% 58.76/58.84 [86]~P5(x861,x863)+~P5(x861,x862)+P6(x861,x862,x863)+P5(f12(x863,x862,x861),x862)
% 58.76/58.84 [88]P5(f10(x883,x882,x881),x881)+P5(f10(x883,x882,x881),x882)+P5(f10(x883,x882,x881),x883)+E(x881,f18(x882,x883))
% 58.76/58.84 [82]~P5(x821,x822)+P4(x821,x822)+~P6(x824,x823,x822)+~P5(x821,x823)
% 58.76/58.84 [83]~P5(x831,x832)+P4(x831,x832)+~P6(x834,x832,x833)+~P5(x831,x833)
% 58.76/58.84 [66]~P5(x661,x664)+P5(x661,x662)+P5(x661,x663)+~E(x664,f18(x663,x662))
% 58.76/58.84 [91]~P5(x911,x913)+~P5(x911,x912)+P6(x911,x912,x913)+~P4(f12(x913,x912,x911),x913)+~P4(f12(x913,x912,x911),x912)
% 58.76/58.84 [84]~P3(x844)+~P4(x841,x842)+P6(x841,x842,x843)+~P6(x845,x842,x843)+~E(x844,f18(x842,x843))
% 58.76/58.84 [65]E(x653,x651)+~P4(x651,x654)+~P4(x653,x654)+E(x651,x652)+E(x653,x652)+~P4(x652,x654)
% 58.76/58.84 [81]P7(x812,x811)+~P7(x812,x813)+~P5(x814,x812)+~P4(x814,x813)+P7(x811,x812)+~P7(x811,x813)+~P5(x814,x811)
% 58.76/58.84 [87]P7(x872,x871)+P7(x872,x873)+P7(x873,x871)+P7(x873,x872)+~P7(x872,x874)+~P7(x873,x874)+~P4(x875,x872)+~P4(x875,x873)+P7(x871,x872)+P7(x871,x873)+~P7(x871,x874)+~P4(x875,x871)
% 58.76/58.84 %EqnAxiom
% 58.76/58.84 [1]E(x11,x11)
% 58.76/58.84 [2]E(x22,x21)+~E(x21,x22)
% 58.76/58.84 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 58.76/58.84 [4]~E(x41,x42)+E(f2(x41),f2(x42))
% 58.76/58.84 [5]~E(x51,x52)+E(f18(x51,x53),f18(x52,x53))
% 58.76/58.84 [6]~E(x61,x62)+E(f18(x63,x61),f18(x63,x62))
% 58.76/58.84 [7]~E(x71,x72)+E(f3(x71),f3(x72))
% 58.76/58.84 [8]~E(x81,x82)+E(f13(x81),f13(x82))
% 58.76/58.84 [9]~E(x91,x92)+E(f4(x91,x93),f4(x92,x93))
% 58.76/58.84 [10]~E(x101,x102)+E(f4(x103,x101),f4(x103,x102))
% 58.76/58.84 [11]~E(x111,x112)+E(f5(x111,x113),f5(x112,x113))
% 58.76/58.84 [12]~E(x121,x122)+E(f5(x123,x121),f5(x123,x122))
% 58.76/58.84 [13]~E(x131,x132)+E(f12(x131,x133,x134),f12(x132,x133,x134))
% 58.76/58.84 [14]~E(x141,x142)+E(f12(x143,x141,x144),f12(x143,x142,x144))
% 58.76/58.84 [15]~E(x151,x152)+E(f12(x153,x154,x151),f12(x153,x154,x152))
% 58.76/58.84 [16]~E(x161,x162)+E(f10(x161,x163,x164),f10(x162,x163,x164))
% 58.76/58.84 [17]~E(x171,x172)+E(f10(x173,x171,x174),f10(x173,x172,x174))
% 58.76/58.84 [18]~E(x181,x182)+E(f10(x183,x184,x181),f10(x183,x184,x182))
% 58.76/58.84 [19]~E(x191,x192)+E(f7(x191,x193),f7(x192,x193))
% 58.76/58.84 [20]~E(x201,x202)+E(f7(x203,x201),f7(x203,x202))
% 58.76/58.84 [21]~E(x211,x212)+E(f11(x211,x213),f11(x212,x213))
% 58.76/58.84 [22]~E(x221,x222)+E(f11(x223,x221),f11(x223,x222))
% 58.76/58.84 [23]~E(x231,x232)+E(f14(x231,x233),f14(x232,x233))
% 58.76/58.84 [24]~E(x241,x242)+E(f14(x243,x241),f14(x243,x242))
% 58.76/58.84 [25]~E(x251,x252)+E(f6(x251,x253),f6(x252,x253))
% 58.76/58.84 [26]~E(x261,x262)+E(f6(x263,x261),f6(x263,x262))
% 58.76/58.84 [27]~E(x271,x272)+E(f8(x271,x273),f8(x272,x273))
% 58.76/58.84 [28]~E(x281,x282)+E(f8(x283,x281),f8(x283,x282))
% 58.76/58.84 [29]~E(x291,x292)+E(f9(x291,x293),f9(x292,x293))
% 58.76/58.84 [30]~E(x301,x302)+E(f9(x303,x301),f9(x303,x302))
% 58.76/58.84 [31]~P1(x311)+P1(x312)+~E(x311,x312)
% 58.76/58.84 [32]P7(x322,x323)+~E(x321,x322)+~P7(x321,x323)
% 58.76/58.84 [33]P7(x333,x332)+~E(x331,x332)+~P7(x333,x331)
% 58.76/58.84 [34]P6(x342,x343,x344)+~E(x341,x342)+~P6(x341,x343,x344)
% 58.76/58.84 [35]P6(x353,x352,x354)+~E(x351,x352)+~P6(x353,x351,x354)
% 58.76/58.84 [36]P6(x363,x364,x362)+~E(x361,x362)+~P6(x363,x364,x361)
% 58.76/58.84 [37]P2(x372,x373)+~E(x371,x372)+~P2(x371,x373)
% 58.76/58.84 [38]P2(x383,x382)+~E(x381,x382)+~P2(x383,x381)
% 58.76/58.84 [39]P5(x392,x393)+~E(x391,x392)+~P5(x391,x393)
% 58.76/58.84 [40]P5(x403,x402)+~E(x401,x402)+~P5(x403,x401)
% 58.76/58.84 [41]P4(x412,x413)+~E(x411,x412)+~P4(x411,x413)
% 58.76/58.84 [42]P4(x423,x422)+~E(x421,x422)+~P4(x423,x421)
% 58.76/58.84 [43]~P3(x431)+P3(x432)+~E(x431,x432)
% 58.76/58.84
% 58.76/58.84 %-------------------------------------------
% 58.79/58.86 cnf(92,plain,
% 58.79/58.86 (~P5(x921,x922)+P5(x921,f18(x923,x922))),
% 58.79/58.86 inference(equality_inference,[],[62])).
% 58.79/58.86 cnf(93,plain,
% 58.79/58.86 (~P5(x931,x932)+P5(x931,f18(x932,x933))),
% 58.79/58.86 inference(equality_inference,[],[63])).
% 58.79/58.86 cnf(94,plain,
% 58.79/58.86 (~P5(x941,f18(x942,x943))+P5(x941,x943)+P5(x941,x942)),
% 58.79/58.86 inference(equality_inference,[],[66])).
% 58.79/58.86 cnf(96,plain,
% 58.79/58.86 (~P4(x961,f18(a15,a16))),
% 58.79/58.86 inference(scs_inference,[],[49,51])).
% 58.79/58.86 cnf(98,plain,
% 58.79/58.86 (P3(f18(a15,a16))),
% 58.79/58.86 inference(scs_inference,[],[49,51,50])).
% 58.79/58.86 cnf(100,plain,
% 58.79/58.86 (~P5(x1001,a15)+P5(x1001,a1)),
% 58.79/58.86 inference(scs_inference,[],[45,49,51,50,61])).
% 58.79/58.86 cnf(102,plain,
% 58.79/58.86 (~P5(x1021,f18(a15,a15))+P5(x1021,a1)),
% 58.79/58.86 inference(scs_inference,[],[45,49,51,50,61,94])).
% 58.79/58.86 cnf(115,plain,
% 58.79/58.86 (P7(x1151,a1)+~E(a16,x1151)),
% 58.79/58.86 inference(scs_inference,[],[46,32])).
% 58.79/58.86 cnf(117,plain,
% 58.79/58.86 (~P5(x1171,a16)+P5(x1171,a1)),
% 58.79/58.86 inference(scs_inference,[],[46,48,32,36,61])).
% 58.79/58.86 cnf(120,plain,
% 58.79/58.86 (P6(x1201,a15,a16)+~E(a17,x1201)),
% 58.79/58.86 inference(scs_inference,[],[46,48,47,32,36,61,38,34])).
% 58.79/58.86 cnf(127,plain,
% 58.79/58.86 (P2(x1271,x1272)+~E(f2(x1272),x1271)),
% 58.79/58.86 inference(scs_inference,[],[47,37])).
% 58.79/58.86 cnf(135,plain,
% 58.79/58.86 (P7(x1351,a1)+~E(a15,x1351)),
% 58.79/58.86 inference(scs_inference,[],[45,32])).
% 58.79/58.86 cnf(153,plain,
% 58.79/58.86 (~E(f18(a15,a16),x1531)+~P4(x1532,x1531)),
% 58.79/58.86 inference(scs_inference,[],[98,54,43])).
% 58.79/58.86 cnf(186,plain,
% 58.79/58.86 (~E(a1,f18(a15,a16))),
% 58.79/58.86 inference(scs_inference,[],[96,44,52,31])).
% 58.79/58.86 cnf(189,plain,
% 58.79/58.86 (~P5(f10(a16,a15,a1),f18(a1,a1))+~P5(f10(a16,a15,a1),a15)),
% 58.79/58.86 inference(scs_inference,[],[186,89,94])).
% 58.79/58.86 cnf(210,plain,
% 58.79/58.86 (~P5(f10(a16,a15,a1),a16)),
% 58.79/58.86 inference(scs_inference,[],[46,186,90,61])).
% 58.79/58.86 cnf(228,plain,
% 58.79/58.86 (P5(f10(a16,a15,a1),a1)+P5(f10(a16,a15,a1),a15)),
% 58.79/58.86 inference(scs_inference,[],[48,186,210,47,75,56,55,74,94,37,34,53,88])).
% 58.79/58.86 cnf(333,plain,
% 58.79/58.86 (P7(x3331,a1)+~P5(f5(x3331,a1),a16)),
% 58.79/58.86 inference(scs_inference,[],[117,71])).
% 58.79/58.86 cnf(365,plain,
% 58.79/58.86 (E(f2(f9(a16,a15)),f2(f18(a15,a16)))),
% 58.79/58.86 inference(scs_inference,[],[48,4,76])).
% 58.79/58.86 cnf(367,plain,
% 58.79/58.86 (E(f2(f18(a15,a16)),f2(f9(a16,a15)))),
% 58.79/58.86 inference(scs_inference,[],[365,127,2])).
% 58.79/58.86 cnf(376,plain,
% 58.79/58.86 (P2(f2(f9(a16,a15)),f18(a15,a16))),
% 58.79/58.86 inference(scs_inference,[],[367,127])).
% 58.79/58.86 cnf(1201,plain,
% 58.79/58.86 (P5(f10(a16,a15,a1),a15)+P5(f10(a16,a15,a1),f18(x12011,a1))),
% 58.79/58.86 inference(scs_inference,[],[228,92])).
% 58.79/58.86 cnf(2381,plain,
% 58.79/58.86 (P5(f10(a16,a15,a1),f18(x23811,a15))+P5(f10(a16,a15,a1),f18(x23812,a1))),
% 58.79/58.86 inference(scs_inference,[],[1201,92])).
% 58.79/58.86 cnf(2668,plain,
% 58.79/58.86 (P5(f10(a16,a15,a1),f18(x26681,a1))+P5(f10(a16,a15,a1),a1)),
% 58.79/58.86 inference(scs_inference,[],[2381,102])).
% 58.79/58.86 cnf(2684,plain,
% 58.79/58.86 (P5(f10(a16,a15,a1),f18(x26841,a1))+P5(f10(a16,a15,a1),f18(x26842,a1))),
% 58.79/58.86 inference(scs_inference,[],[2668,92])).
% 58.79/58.86 cnf(2733,plain,
% 58.79/58.86 (~P5(f10(a16,a15,a1),a15)),
% 58.79/58.86 inference(scs_inference,[],[2684,189])).
% 58.79/58.86 cnf(2734,plain,
% 58.79/58.86 (P5(f10(a16,a15,a1),a1)),
% 58.79/58.86 inference(scs_inference,[],[2733,228])).
% 58.79/58.86 cnf(2744,plain,
% 58.79/58.86 (~P5(f10(a16,a15,a1),f18(a15,a15))),
% 58.79/58.86 inference(scs_inference,[],[2733,75,56,55,74,94])).
% 58.79/58.86 cnf(2748,plain,
% 58.79/58.86 (P5(f10(a16,a15,a1),f18(a1,x27481))),
% 58.79/58.86 inference(scs_inference,[],[2734,93])).
% 58.79/58.86 cnf(2761,plain,
% 58.79/58.86 (~P5(f10(a16,a15,a1),f18(f18(a15,a15),f18(a15,a15)))),
% 58.79/58.86 inference(scs_inference,[],[210,2734,2744,93,92,56,75,55,74,40,94])).
% 58.79/58.86 cnf(3097,plain,
% 58.79/58.86 (~E(a1,f18(a15,a15))),
% 58.79/58.86 inference(scs_inference,[],[2744,2734,40])).
% 58.79/58.86 cnf(3100,plain,
% 58.79/58.86 (~P5(f10(a15,a15,a1),a15)),
% 58.79/58.86 inference(scs_inference,[],[2744,45,2734,40,89,61])).
% 58.79/58.86 cnf(3113,plain,
% 58.79/58.86 (~P5(f10(a15,a15,a1),f18(a15,a15))),
% 58.79/58.86 inference(scs_inference,[],[3100,75,55,56,74,94])).
% 58.79/58.86 cnf(3119,plain,
% 58.79/58.86 (P5(f10(a15,a15,a1),f18(x31191,a1))),
% 58.79/58.86 inference(scs_inference,[],[2744,3100,2748,3097,75,55,56,74,94,40,88,120,92])).
% 58.79/58.86 cnf(3128,plain,
% 58.79/58.86 (P5(f10(a15,a15,a1),f18(x31281,f18(x31282,a1)))),
% 58.79/58.86 inference(scs_inference,[],[3119,92])).
% 58.79/58.86 cnf(3140,plain,
% 58.79/58.86 (~P5(f10(a15,a15,a1),f18(f18(a15,a15),f18(a15,a15)))),
% 58.79/58.86 inference(scs_inference,[],[3113,3119,92,93,55,75,56,74,94])).
% 58.79/58.86 cnf(3262,plain,
% 58.79/58.86 (~P5(f10(f18(a15,a15),f18(a15,a15),a1),a1)+~P5(f10(f18(a15,a15),f18(a15,a15),a1),f18(a15,a15))),
% 58.79/58.86 inference(scs_inference,[],[2761,2734,40,89])).
% 58.79/58.86 cnf(4174,plain,
% 58.79/58.86 (~P5(f10(f18(a15,a15),f18(a15,a15),a1),f18(a15,a15))),
% 58.79/58.86 inference(scs_inference,[],[3262,102])).
% 58.79/58.86 cnf(4178,plain,
% 58.79/58.86 (~P2(f10(f18(a15,a15),f18(a15,a15),a1),f18(a15,a15))),
% 58.79/58.86 inference(scs_inference,[],[4174,55,56])).
% 58.79/58.86 cnf(4468,plain,
% 58.79/58.86 (~E(f2(f18(a15,a15)),f10(f18(a15,a15),f18(a15,a15),a1))),
% 58.79/58.86 inference(scs_inference,[],[4178,47,37])).
% 58.79/58.86 cnf(5166,plain,
% 58.79/58.86 (~P7(f9(a16,a15),a1)),
% 58.79/58.86 inference(scs_inference,[],[44,4468,3140,98,4174,3119,49,376,47,48,96,76,78,13,14,15,16,18,52,64,6,54,50,2,17,5,92,57,55,74,56,75,3,62,63,43,53,42,39,32])).
% 58.79/58.86 cnf(5172,plain,
% 58.79/58.86 (P4(a17,a16)),
% 58.79/58.86 inference(scs_inference,[],[44,4468,3140,98,4174,3128,3119,49,376,47,48,96,76,78,13,14,15,16,18,52,64,6,54,50,2,17,5,92,57,55,74,56,75,3,62,63,43,53,42,39,32,61,83,82])).
% 58.79/58.86 cnf(5202,plain,
% 58.79/58.86 (~P5(f5(f18(a15,a16),a1),a1)),
% 58.79/58.86 inference(scs_inference,[],[44,4468,3140,98,4174,3128,3119,49,376,47,48,96,76,78,13,14,15,16,18,52,64,6,54,50,2,17,5,92,57,55,74,56,75,3,62,63,43,53,42,39,32,61,83,82,115,135,58,60,7,8,153,333,9,10,11,12,19,20,21,22,23,24,25,26,27,28,29,30,71])).
% 58.79/58.86 cnf(5206,plain,
% 58.79/58.86 (P1(a16)),
% 58.79/58.86 inference(scs_inference,[],[44,4468,3140,98,4174,3128,3119,49,376,47,48,96,76,78,13,14,15,16,18,52,64,6,54,50,2,17,5,92,57,55,74,56,75,3,62,63,43,53,42,39,32,61,83,82,115,135,58,60,7,8,153,333,9,10,11,12,19,20,21,22,23,24,25,26,27,28,29,30,71,100,51])).
% 58.79/58.86 cnf(5210,plain,
% 58.79/58.86 (P5(f5(f18(a15,a16),a1),a15)),
% 58.79/58.86 inference(scs_inference,[],[44,4468,3140,98,4174,3128,3119,49,376,47,48,96,76,78,13,14,15,16,18,52,64,6,54,50,2,17,5,92,57,55,74,56,75,3,62,63,43,53,42,39,32,61,83,82,115,135,58,60,7,8,153,333,9,10,11,12,19,20,21,22,23,24,25,26,27,28,29,30,71,100,51,67,94])).
% 58.79/58.86 cnf(5226,plain,
% 58.79/58.86 ($false),
% 58.79/58.86 inference(scs_inference,[],[5172,5206,5166,5210,5202,58,52,64,333,100]),
% 58.79/58.86 ['proof']).
% 58.79/58.87 % SZS output end Proof
% 58.79/58.87 % Total time :58.120000s
%------------------------------------------------------------------------------