%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : GEO083+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 : n029.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:43 EDT 2024
% Result : Theorem 58.77s 58.78s
% Output : CNFRefutation 58.83s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.12/0.12 % Problem : GEO083+1 : TPTP v8.2.0. Released v2.4.0.
% 0.12/0.12 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% 0.12/0.33 % Computer : n029.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 10:45:09 EDT 2024
% 0.12/0.33 % CPUTime :
% 0.21/0.57 start to proof:theBenchmark
% 58.68/58.77 %-------------------------------------------
% 58.68/58.77 % File :CSE---1.7
% 58.68/58.77 % Problem :theBenchmark
% 58.68/58.77 % Transform :cnf
% 58.68/58.77 % Format :tptp:raw
% 58.68/58.77 % Command :java -jar mcs_scs.jar %d %s
% 58.68/58.77
% 58.68/58.77 % Result :Theorem 58.160000s
% 58.68/58.77 % Output :CNFRefutation 58.160000s
% 58.68/58.77 %-------------------------------------------
% 58.77/58.78 %--------------------------------------------------------------------------
% 58.77/58.78 % File : GEO083+1 : TPTP v8.2.0. Released v2.4.0.
% 58.77/58.78 % Domain : Geometry (Oriented curves)
% 58.77/58.78 % Problem : Sum is monotone, part 1
% 58.77/58.78 % Version : [EHK99] axioms.
% 58.77/58.78 % English :
% 58.77/58.78
% 58.77/58.78 % Refs : [KE99] Kulik & Eschenbach (1999), A Geometry of Oriented Curv
% 58.77/58.78 % : [EHK99] Eschenbach et al. (1999), Representing Simple Trajecto
% 58.77/58.78 % Source : [KE99]
% 58.77/58.78 % Names : Corollary 2.6 (1) [KE99]
% 58.77/58.78
% 58.77/58.78 % Status : Theorem
% 58.77/58.78 % Rating : 0.39 v8.2.0, 0.42 v8.1.0, 0.39 v7.5.0, 0.44 v7.4.0, 0.30 v7.3.0, 0.28 v7.2.0, 0.24 v7.1.0, 0.30 v7.0.0, 0.33 v6.4.0, 0.38 v6.3.0, 0.29 v6.2.0, 0.36 v6.1.0, 0.50 v6.0.0, 0.48 v5.5.0, 0.59 v5.4.0, 0.61 v5.3.0, 0.59 v5.2.0, 0.45 v5.1.0, 0.48 v5.0.0, 0.46 v4.1.0, 0.48 v4.0.1, 0.52 v4.0.0, 0.50 v3.5.0, 0.53 v3.4.0, 0.58 v3.3.0, 0.57 v3.2.0, 0.64 v3.1.0, 0.78 v2.7.0, 0.67 v2.5.0, 0.50 v2.4.0
% 58.77/58.78 % Syntax : Number of formulae : 17 ( 1 unt; 0 def)
% 58.77/58.78 % Number of atoms : 71 ( 10 equ)
% 58.77/58.78 % Maximal formula atoms : 12 ( 4 avg)
% 58.77/58.78 % Number of connectives : 58 ( 4 ~; 9 |; 23 &)
% 58.77/58.78 % ( 9 <=>; 13 =>; 0 <=; 0 <~>)
% 58.77/58.78 % Maximal formula depth : 12 ( 7 avg)
% 58.77/58.78 % Maximal term depth : 2 ( 1 avg)
% 58.77/58.78 % Number of predicates : 8 ( 7 usr; 0 prp; 1-3 aty)
% 58.77/58.78 % Number of functors : 1 ( 1 usr; 0 con; 2-2 aty)
% 58.77/58.78 % Number of variables : 57 ( 48 !; 9 ?)
% 58.77/58.78 % SPC : FOF_THM_RFO_SEQ
% 58.77/58.78
% 58.77/58.78 % Comments :
% 58.77/58.78 %--------------------------------------------------------------------------
% 58.77/58.78 %----Include simple curve axioms
% 58.77/58.78 include('Axioms/GEO004+0.ax').
% 58.77/58.78 %--------------------------------------------------------------------------
% 58.77/58.78 fof(corollary_2_6_1,conjecture,
% 58.77/58.78 ! [C1,C2,C3,P] :
% 58.77/58.78 ( ( part_of(C2,C3)
% 58.77/58.78 & meet(P,C1,C2)
% 58.77/58.78 & meet(P,C1,C3) )
% 58.77/58.78 => part_of(sum(C1,C2),sum(C1,C3)) ) ).
% 58.77/58.78
% 58.77/58.78 %--------------------------------------------------------------------------
% 58.77/58.78 %-------------------------------------------
% 58.77/58.78 % Proof found
% 58.77/58.78 % SZS status Theorem for theBenchmark
% 58.77/58.78 % SZS output start Proof
% 58.77/58.79 %ClaNum:90(EqnAxiom:43)
% 58.77/58.79 %VarNum:331(SingletonVarNum:113)
% 58.77/58.79 %MaxLitNum:12
% 58.77/58.79 %MaxfuncDepth:2
% 58.77/58.79 %SharedTerms:10
% 58.77/58.79 %goalClause: 44 46 47 48
% 58.77/58.79 %singleGoalClaCount:4
% 58.77/58.79 [44]P1(a1,a7)
% 58.77/58.79 [46]P6(a9,a2,a1)
% 58.77/58.79 [47]P6(a9,a2,a7)
% 58.77/58.79 [48]~P1(f17(a2,a1),f17(a2,a7))
% 58.77/58.79 [45]P2(f8(x451),x451)
% 58.77/58.79 [49]P3(x491)+P4(f10(x491),x491)
% 58.77/58.79 [51]~P7(x511)+P4(f16(x511),x511)
% 58.77/58.79 [50]P7(x501)+~P4(x502,x501)
% 58.77/58.79 [53]~P3(x531)+~P4(x532,x531)
% 58.77/58.79 [54]~P4(x541,x542)+P5(x541,x542)
% 58.77/58.79 [55]~P2(x551,x552)+P5(x551,x552)
% 58.77/58.79 [56]~P2(x561,x562)+~P4(x561,x562)
% 58.77/58.79 [57]~P4(x572,x571)+~E(f3(x571,x572),x572)
% 58.77/58.79 [59]P1(x591,x592)+P5(f11(x592,x591),x591)
% 58.77/58.79 [63]~P4(x632,x631)+P4(f3(x631,x632),x631)
% 58.77/58.79 [70]P1(x701,x702)+~P5(f11(x702,x701),x702)
% 58.77/58.79 [77]~P2(x771,x772)+P6(x771,f18(x772,x771),f4(x772,x771))
% 58.77/58.79 [72]~P2(x722,x721)+E(f17(f18(x721,x722),f4(x721,x722)),x721)
% 58.77/58.79 [73]P5(x731,x732)+~P6(x731,x733,x732)
% 58.77/58.79 [74]P5(x741,x742)+~P6(x741,x742,x743)
% 58.77/58.79 [75]~P6(x753,x751,x752)+E(f6(x751,x752),f17(x751,x752))
% 58.77/58.79 [52]P7(x521)+~P1(x521,x522)+E(x521,x522)
% 58.77/58.79 [58]P2(x581,x582)+~P5(x581,x582)+P4(x581,x582)
% 58.77/58.79 [66]~P5(x661,x662)+P4(x661,x662)+P5(x661,f12(x661,x662))
% 58.77/58.79 [67]~P5(x671,x672)+P4(x671,x672)+P5(x671,f14(x671,x672))
% 58.77/58.79 [68]~P5(x681,x682)+P4(x681,x682)+P1(f12(x681,x682),x682)
% 58.77/58.79 [69]~P5(x691,x692)+P4(x691,x692)+P1(f14(x691,x692),x692)
% 58.77/58.79 [71]E(x711,x712)+P5(f5(x711,x712),x712)+P5(f5(x711,x712),x711)
% 58.77/58.79 [76]E(x761,x762)+~P5(f5(x761,x762),x762)+~P5(f5(x761,x762),x761)
% 58.77/58.79 [78]~P5(x781,x782)+P4(x781,x782)+~P1(f12(x781,x782),f14(x781,x782))
% 58.77/58.79 [79]~P5(x791,x792)+P4(x791,x792)+~P1(f14(x791,x792),f12(x791,x792))
% 58.77/58.79 [60]~P5(x601,x603)+P5(x601,x602)+~P1(x603,x602)
% 58.77/58.79 [88]~P5(f13(x881,x882,x883),x883)+~P5(f13(x881,x882,x883),x881)+E(x881,f17(x882,x883))
% 58.77/58.79 [89]~P5(f13(x891,x892,x893),x892)+~P5(f13(x891,x892,x893),x891)+E(x891,f17(x892,x893))
% 58.77/58.79 [61]~P5(x611,x614)+P5(x611,x612)+~E(x612,f17(x613,x614))
% 58.77/58.79 [62]~P5(x621,x623)+P5(x621,x622)+~E(x622,f17(x623,x624))
% 58.77/58.79 [84]~P5(x841,x843)+~P5(x841,x842)+P6(x841,x842,x843)+P5(f15(x841,x842,x843),x843)
% 58.77/58.79 [85]~P5(x851,x853)+~P5(x851,x852)+P6(x851,x852,x853)+P5(f15(x851,x852,x853),x852)
% 58.77/58.79 [87]P5(f13(x871,x872,x873),x873)+P5(f13(x871,x872,x873),x872)+P5(f13(x871,x872,x873),x871)+E(x871,f17(x872,x873))
% 58.77/58.79 [81]~P5(x811,x812)+P4(x811,x812)+~P6(x814,x813,x812)+~P5(x811,x813)
% 58.77/58.79 [82]~P5(x821,x822)+P4(x821,x822)+~P6(x824,x822,x823)+~P5(x821,x823)
% 58.77/58.79 [65]~P5(x651,x654)+P5(x651,x652)+P5(x651,x653)+~E(x654,f17(x653,x652))
% 58.77/58.79 [90]~P5(x901,x903)+~P5(x901,x902)+P6(x901,x902,x903)+~P4(f15(x901,x902,x903),x903)+~P4(f15(x901,x902,x903),x902)
% 58.77/58.79 [83]~P3(x834)+~P4(x831,x832)+P6(x831,x832,x833)+~P6(x835,x832,x833)+~E(x834,f17(x832,x833))
% 58.77/58.79 [64]E(x643,x641)+~P4(x641,x644)+~P4(x643,x644)+E(x641,x642)+E(x643,x642)+~P4(x642,x644)
% 58.77/58.79 [80]P1(x802,x801)+~P1(x802,x803)+~P5(x804,x802)+~P4(x804,x803)+P1(x801,x802)+~P1(x801,x803)+~P5(x804,x801)
% 58.77/58.79 [86]P1(x862,x861)+P1(x862,x863)+P1(x863,x861)+P1(x863,x862)+~P1(x862,x864)+~P1(x863,x864)+~P4(x865,x862)+~P4(x865,x863)+P1(x861,x862)+P1(x861,x863)+~P1(x861,x864)+~P4(x865,x861)
% 58.77/58.79 %EqnAxiom
% 58.77/58.79 [1]E(x11,x11)
% 58.77/58.79 [2]E(x22,x21)+~E(x21,x22)
% 58.77/58.79 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 58.77/58.79 [4]~E(x41,x42)+E(f8(x41),f8(x42))
% 58.77/58.79 [5]~E(x51,x52)+E(f17(x51,x53),f17(x52,x53))
% 58.77/58.79 [6]~E(x61,x62)+E(f17(x63,x61),f17(x63,x62))
% 58.77/58.79 [7]~E(x71,x72)+E(f15(x71,x73,x74),f15(x72,x73,x74))
% 58.77/58.79 [8]~E(x81,x82)+E(f15(x83,x81,x84),f15(x83,x82,x84))
% 58.77/58.79 [9]~E(x91,x92)+E(f15(x93,x94,x91),f15(x93,x94,x92))
% 58.77/58.79 [10]~E(x101,x102)+E(f10(x101),f10(x102))
% 58.77/58.79 [11]~E(x111,x112)+E(f16(x111),f16(x112))
% 58.77/58.79 [12]~E(x121,x122)+E(f3(x121,x123),f3(x122,x123))
% 58.77/58.79 [13]~E(x131,x132)+E(f3(x133,x131),f3(x133,x132))
% 58.77/58.79 [14]~E(x141,x142)+E(f11(x141,x143),f11(x142,x143))
% 58.77/58.79 [15]~E(x151,x152)+E(f11(x153,x151),f11(x153,x152))
% 58.77/58.79 [16]~E(x161,x162)+E(f13(x161,x163,x164),f13(x162,x163,x164))
% 58.77/58.79 [17]~E(x171,x172)+E(f13(x173,x171,x174),f13(x173,x172,x174))
% 58.77/58.79 [18]~E(x181,x182)+E(f13(x183,x184,x181),f13(x183,x184,x182))
% 58.77/58.79 [19]~E(x191,x192)+E(f12(x191,x193),f12(x192,x193))
% 58.77/58.79 [20]~E(x201,x202)+E(f12(x203,x201),f12(x203,x202))
% 58.77/58.79 [21]~E(x211,x212)+E(f14(x211,x213),f14(x212,x213))
% 58.77/58.79 [22]~E(x221,x222)+E(f14(x223,x221),f14(x223,x222))
% 58.77/58.79 [23]~E(x231,x232)+E(f6(x231,x233),f6(x232,x233))
% 58.77/58.79 [24]~E(x241,x242)+E(f6(x243,x241),f6(x243,x242))
% 58.77/58.79 [25]~E(x251,x252)+E(f5(x251,x253),f5(x252,x253))
% 58.77/58.79 [26]~E(x261,x262)+E(f5(x263,x261),f5(x263,x262))
% 58.77/58.79 [27]~E(x271,x272)+E(f4(x271,x273),f4(x272,x273))
% 58.77/58.79 [28]~E(x281,x282)+E(f4(x283,x281),f4(x283,x282))
% 58.77/58.79 [29]~E(x291,x292)+E(f18(x291,x293),f18(x292,x293))
% 58.77/58.79 [30]~E(x301,x302)+E(f18(x303,x301),f18(x303,x302))
% 58.77/58.79 [31]P1(x312,x313)+~E(x311,x312)+~P1(x311,x313)
% 58.77/58.79 [32]P1(x323,x322)+~E(x321,x322)+~P1(x323,x321)
% 58.77/58.80 [33]P2(x332,x333)+~E(x331,x332)+~P2(x331,x333)
% 58.77/58.80 [34]P2(x343,x342)+~E(x341,x342)+~P2(x343,x341)
% 58.77/58.80 [35]P6(x352,x353,x354)+~E(x351,x352)+~P6(x351,x353,x354)
% 58.77/58.80 [36]P6(x363,x362,x364)+~E(x361,x362)+~P6(x363,x361,x364)
% 58.77/58.80 [37]P6(x373,x374,x372)+~E(x371,x372)+~P6(x373,x374,x371)
% 58.77/58.80 [38]P5(x382,x383)+~E(x381,x382)+~P5(x381,x383)
% 58.77/58.80 [39]P5(x393,x392)+~E(x391,x392)+~P5(x393,x391)
% 58.77/58.80 [40]P4(x402,x403)+~E(x401,x402)+~P4(x401,x403)
% 58.77/58.80 [41]P4(x413,x412)+~E(x411,x412)+~P4(x413,x411)
% 58.77/58.80 [42]~P3(x421)+P3(x422)+~E(x421,x422)
% 58.77/58.80 [43]~P7(x431)+P7(x432)+~E(x431,x432)
% 58.77/58.80
% 58.77/58.80 %-------------------------------------------
% 58.83/58.80 cnf(91,plain,
% 58.83/58.80 (~P5(x911,x912)+P5(x911,f17(x913,x912))),
% 58.83/58.80 inference(equality_inference,[],[61])).
% 58.83/58.80 cnf(92,plain,
% 58.83/58.80 (~P5(x921,x922)+P5(x921,f17(x922,x923))),
% 58.83/58.80 inference(equality_inference,[],[62])).
% 58.83/58.80 cnf(93,plain,
% 58.83/58.80 (~P5(x931,f17(x932,x933))+P5(x931,x933)+P5(x931,x932)),
% 58.83/58.80 inference(equality_inference,[],[65])).
% 58.83/58.80 cnf(95,plain,
% 58.83/58.80 (~P5(x951,a1)+P5(x951,a7)),
% 58.83/58.80 inference(scs_inference,[],[44,60])).
% 58.83/58.80 cnf(97,plain,
% 58.83/58.80 (~P5(x971,f17(a1,a1))+P5(x971,a7)),
% 58.83/58.80 inference(scs_inference,[],[44,60,93])).
% 58.83/58.80 cnf(118,plain,
% 58.83/58.80 (P2(f8(x1181),x1182)+~E(x1181,x1182)),
% 58.83/58.80 inference(scs_inference,[],[45,34])).
% 58.83/58.80 cnf(123,plain,
% 58.83/58.81 (P2(x1231,x1232)+~E(f8(x1232),x1231)),
% 58.83/58.81 inference(scs_inference,[],[44,47,45,34,32,35,37,31,33])).
% 58.83/58.81 cnf(132,plain,
% 58.83/58.81 (P6(x1321,a2,a1)+~E(a9,x1321)),
% 58.83/58.81 inference(scs_inference,[],[47,46,36,37,35])).
% 58.83/58.81 cnf(151,plain,
% 58.83/58.81 (~P4(x1511,x1512)+P4(f16(x1512),x1512)),
% 58.83/58.81 inference(scs_inference,[],[50,51])).
% 58.83/58.81 cnf(167,plain,
% 58.83/58.81 (~P4(x1671,x1672)+P4(f10(x1672),x1672)),
% 58.83/58.81 inference(scs_inference,[],[53,49])).
% 58.83/58.81 cnf(215,plain,
% 58.83/58.81 (P5(f16(x2151),x2151)+~P4(x2152,x2151)),
% 58.83/58.81 inference(scs_inference,[],[151,54])).
% 58.83/58.81 cnf(231,plain,
% 58.83/58.81 (~P4(x2311,x2312)+~E(f3(x2312,f10(x2312)),f10(x2312))),
% 58.83/58.81 inference(scs_inference,[],[167,57])).
% 58.83/58.81 cnf(324,plain,
% 58.83/58.81 (~E(x3241,f17(a2,a1))+P5(f11(f17(a2,a7),x3241),x3241)),
% 58.83/58.81 inference(scs_inference,[],[48,59,31])).
% 58.83/58.81 cnf(325,plain,
% 58.83/58.81 (P5(f11(f17(a2,a7),f17(a2,a1)),f17(a2,a1))),
% 58.83/58.81 inference(equality_inference,[],[324])).
% 58.83/58.81 cnf(328,plain,
% 58.83/58.81 (P5(f11(f17(a2,a7),f17(a2,a1)),f17(f17(a2,a1),x3281))),
% 58.83/58.81 inference(scs_inference,[],[325,91,92])).
% 58.83/58.81 cnf(337,plain,
% 58.83/58.81 (P5(f11(f17(a2,a7),f17(a2,a1)),x3371)+~E(f17(a2,a1),x3371)),
% 58.83/58.81 inference(scs_inference,[],[325,39])).
% 58.83/58.81 cnf(338,plain,
% 58.83/58.81 (P5(f11(f17(a2,a7),f17(a2,a1)),a7)+~E(f17(a2,a1),a1)),
% 58.83/58.81 inference(scs_inference,[],[44,325,39,60])).
% 58.83/58.81 cnf(358,plain,
% 58.83/58.81 (P1(x3581,f17(a2,a1))+~E(f11(f17(a2,a7),f17(a2,a1)),f11(f17(a2,a1),x3581))),
% 58.83/58.81 inference(scs_inference,[],[325,38,70])).
% 58.83/58.81 cnf(398,plain,
% 58.83/58.81 (P5(f8(f17(a1,a1)),a7)),
% 58.83/58.81 inference(scs_inference,[],[45,97,55])).
% 58.83/58.81 cnf(776,plain,
% 58.83/58.81 (~E(f10(x7761),f3(x7761,f10(x7761)))+~P4(x7762,x7761)),
% 58.83/58.81 inference(scs_inference,[],[231,2])).
% 58.83/58.81 cnf(1238,plain,
% 58.83/58.81 (~E(a1,f17(a2,a1))+P5(f11(f17(a2,a7),f17(a2,a1)),a7)),
% 58.83/58.81 inference(scs_inference,[],[338,2])).
% 58.83/58.81 cnf(1302,plain,
% 58.83/58.81 (P5(f11(f17(a2,a7),f17(a2,a1)),f17(x13021,a7))+~E(a1,f17(a2,a1))),
% 58.83/58.81 inference(scs_inference,[],[1238,91])).
% 58.83/58.81 cnf(1682,plain,
% 58.83/58.81 (~E(a1,f17(a2,a1))),
% 58.83/58.81 inference(scs_inference,[],[48,1302,70])).
% 58.83/58.81 cnf(1683,plain,
% 58.83/58.81 (~P5(f13(a1,a2,a1),a1)),
% 58.83/58.81 inference(scs_inference,[],[1682,88])).
% 58.83/58.81 cnf(1685,plain,
% 58.83/58.81 (~P5(f13(a1,a2,a1),f17(a1,a1))),
% 58.83/58.81 inference(scs_inference,[],[1682,88,93])).
% 58.83/58.81 cnf(1687,plain,
% 58.83/58.81 (P5(f13(a1,a2,a1),a2)),
% 58.83/58.81 inference(scs_inference,[],[1682,88,93,87])).
% 58.83/58.81 cnf(1691,plain,
% 58.83/58.81 (~P4(f13(a1,a2,a1),a1)),
% 58.83/58.81 inference(scs_inference,[],[1682,88,93,87,74,54])).
% 58.83/58.81 cnf(1697,plain,
% 58.83/58.81 (P5(f13(a1,a2,a1),f17(a2,x16971))),
% 58.83/58.81 inference(scs_inference,[],[1682,88,93,87,74,54,55,73,92])).
% 58.83/58.81 cnf(1699,plain,
% 58.83/58.81 (P5(f13(a1,a2,a1),f17(x16991,a2))),
% 58.83/58.81 inference(scs_inference,[],[1682,88,93,87,74,54,55,73,92,91])).
% 58.83/58.81 cnf(1718,plain,
% 58.83/58.81 (~P2(f13(a1,a2,a1),f17(a1,a1))),
% 58.83/58.81 inference(scs_inference,[],[1685,54,74,55])).
% 58.83/58.81 cnf(1722,plain,
% 58.83/58.81 (P5(f13(a1,a2,a1),f17(f17(x17221,a2),x17222))),
% 58.83/58.81 inference(scs_inference,[],[1685,1699,54,74,55,73,92])).
% 58.83/58.81 cnf(1724,plain,
% 58.83/58.81 (P5(f13(a1,a2,a1),f17(x17241,f17(x17242,a2)))),
% 58.83/58.81 inference(scs_inference,[],[1685,1699,54,74,55,73,92,91])).
% 58.83/58.81 cnf(1726,plain,
% 58.83/58.81 (~P5(f13(a1,a2,a1),f17(f17(a1,a1),f17(a1,a1)))),
% 58.83/58.81 inference(scs_inference,[],[1685,1699,54,74,55,73,92,91,93])).
% 58.83/58.81 cnf(1728,plain,
% 58.83/58.81 (~E(f17(x17281,a2),f17(a1,a1))),
% 58.83/58.81 inference(scs_inference,[],[1685,1699,54,74,55,73,92,91,93,39])).
% 58.83/58.81 cnf(1735,plain,
% 58.83/58.81 (~P4(f13(a1,a2,a1),f17(f17(a1,a1),f17(a1,a1)))),
% 58.83/58.81 inference(scs_inference,[],[1726,54])).
% 58.83/58.81 cnf(1743,plain,
% 58.83/58.81 (P5(f13(a1,a2,a1),f17(f17(a2,x17431),x17432))),
% 58.83/58.81 inference(scs_inference,[],[1726,1697,54,74,73,55,92])).
% 58.83/58.81 cnf(1749,plain,
% 58.83/58.81 (~E(f17(f17(x17491,a2),x17492),f17(f17(a1,a1),f17(a1,a1)))),
% 58.83/58.81 inference(scs_inference,[],[1726,1722,1697,45,1718,54,74,73,55,92,91,33,39])).
% 58.83/58.81 cnf(1759,plain,
% 58.83/58.81 (~E(f17(x17591,f17(x17592,a2)),f17(a1,a1))),
% 58.83/58.81 inference(scs_inference,[],[1685,1724,39])).
% 58.83/58.81 cnf(1760,plain,
% 58.83/58.81 (~E(f17(x17601,a2),a1)),
% 58.83/58.81 inference(scs_inference,[],[1685,1724,39,6])).
% 58.83/58.81 cnf(1771,plain,
% 58.83/58.81 (~E(f17(a2,x17711),f17(a1,a1))),
% 58.83/58.81 inference(scs_inference,[],[1685,1697,39])).
% 58.83/58.81 cnf(1788,plain,
% 58.83/58.81 (~E(f17(f17(a2,x17881),x17882),f17(a1,a1))),
% 58.83/58.81 inference(scs_inference,[],[1685,1743,39])).
% 58.83/58.81 cnf(1789,plain,
% 58.83/58.81 (~E(f17(a2,x17891),a1)),
% 58.83/58.81 inference(scs_inference,[],[1685,1743,39,5])).
% 58.83/58.81 cnf(1819,plain,
% 58.83/58.81 (~E(a2,f17(a1,a1))),
% 58.83/58.81 inference(scs_inference,[],[1685,1687,39])).
% 58.83/58.81 cnf(2661,plain,
% 58.83/58.81 (~E(f17(x26611,f17(x26612,a2)),a1)),
% 58.83/58.81 inference(scs_inference,[],[1683,1724,39])).
% 58.83/58.81 cnf(2665,plain,
% 58.83/58.81 (~E(f17(f17(a2,x26651),x26652),a1)),
% 58.83/58.81 inference(scs_inference,[],[1683,1743,39])).
% 58.83/58.81 cnf(3444,plain,
% 58.83/58.81 (~E(f11(f17(a2,a1),x34441),f11(f17(a2,a7),f17(a2,a1)))+P1(x34441,f17(a2,a1))),
% 58.83/58.81 inference(scs_inference,[],[358,2])).
% 58.83/58.81 cnf(3713,plain,
% 58.83/58.81 (~E(f17(a2,a1),f17(a2,a7))+P1(f17(a2,a1),f17(a2,a1))),
% 58.83/58.81 inference(scs_inference,[],[3444,14])).
% 58.83/58.81 cnf(3729,plain,
% 58.83/58.81 (~E(f17(a2,a7),f17(a2,a1))+P1(f17(a2,a1),f17(a2,a1))),
% 58.83/58.81 inference(scs_inference,[],[3713,2])).
% 58.83/58.81 cnf(3745,plain,
% 58.83/58.81 (~E(a7,a1)+P1(f17(a2,a1),f17(a2,a1))),
% 58.83/58.81 inference(scs_inference,[],[3729,6])).
% 58.83/58.81 cnf(3761,plain,
% 58.83/58.81 (~E(f17(a2,a1),f17(a2,a7))+~E(a7,a1)),
% 58.83/58.81 inference(scs_inference,[],[48,3745,32])).
% 58.83/58.81 cnf(3777,plain,
% 58.83/58.81 (~E(f17(a2,a7),f17(a2,a1))+~E(a7,a1)),
% 58.83/58.81 inference(scs_inference,[],[3761,2])).
% 58.83/58.81 cnf(3793,plain,
% 58.83/58.81 (~E(a7,a1)),
% 58.83/58.81 inference(scs_inference,[],[3777,6])).
% 58.83/58.81 cnf(4024,plain,
% 58.83/58.81 (~P1(x40241,f17(a2,a7))+~E(x40241,f17(a2,a1))),
% 58.83/58.81 inference(scs_inference,[],[48,31])).
% 58.83/58.81 cnf(4052,plain,
% 58.83/58.81 (~P4(f8(x40521),x40521)),
% 58.83/58.81 inference(scs_inference,[],[1735,45,40,56])).
% 58.83/58.81 cnf(4070,plain,
% 58.83/58.81 (~P4(x40701,x40702)+~E(x40701,f8(x40702))),
% 58.83/58.81 inference(scs_inference,[],[4052,40])).
% 58.83/58.81 cnf(4130,plain,
% 58.83/58.81 (~E(a1,f17(x41301,a2))),
% 58.83/58.81 inference(scs_inference,[],[1760,2])).
% 58.83/58.81 cnf(4146,plain,
% 58.83/58.81 (~E(a1,f17(a2,x41461))),
% 58.83/58.81 inference(scs_inference,[],[1789,2])).
% 58.83/58.81 cnf(4152,plain,
% 58.83/58.81 (P7(a1)),
% 58.83/58.81 inference(scs_inference,[],[44,3793,2,52])).
% 58.83/58.81 cnf(4160,plain,
% 58.83/58.81 (~E(f17(a1,a1),f17(x41601,a2))),
% 58.83/58.81 inference(scs_inference,[],[1728,2])).
% 58.83/58.81 cnf(4166,plain,
% 58.83/58.81 (~E(f17(a1,a1),f17(a2,x41661))),
% 58.83/58.81 inference(scs_inference,[],[1771,2])).
% 58.83/58.81 cnf(4178,plain,
% 58.83/58.81 (~P5(f13(f17(a1,a1),a7,a2),f17(a1,a1))),
% 58.83/58.81 inference(scs_inference,[],[44,398,4160,1819,2,89,60,38,97])).
% 58.83/58.81 cnf(4187,plain,
% 58.83/58.81 (~E(f17(a1,a1),f17(x41871,f17(x41872,a2)))),
% 58.83/58.81 inference(scs_inference,[],[4178,1759,74,73,55,2])).
% 58.83/58.81 cnf(4188,plain,
% 58.83/58.81 (~P5(f13(f17(a1,a1),a7,a2),f17(f17(a1,a1),f17(a1,a1)))),
% 58.83/58.81 inference(scs_inference,[],[4178,1759,74,73,55,2,93])).
% 58.83/58.81 cnf(4190,plain,
% 58.83/58.81 (~E(f8(f17(a1,a1)),f13(f17(a1,a1),a7,a2))),
% 58.83/58.81 inference(scs_inference,[],[4178,1759,74,73,55,2,93,123])).
% 58.83/58.81 cnf(4193,plain,
% 58.83/58.81 (~P5(f13(a1,a2,a7),a1)),
% 58.83/58.81 inference(scs_inference,[],[44,4146,4178,1759,74,73,55,2,93,123,88,60])).
% 58.83/58.81 cnf(4203,plain,
% 58.83/58.81 (~P5(f13(a1,a2,a7),f17(a1,a1))),
% 58.83/58.81 inference(scs_inference,[],[4193,4190,74,55,73,2,93])).
% 58.83/58.81 cnf(4205,plain,
% 58.83/58.81 (~E(a9,f13(a1,a2,a7))),
% 58.83/58.81 inference(scs_inference,[],[4193,4190,74,55,73,2,93,132])).
% 58.83/58.81 cnf(4206,plain,
% 58.83/58.81 (~E(f8(a1),f13(a1,a2,a7))),
% 58.83/58.81 inference(scs_inference,[],[4193,4190,74,55,73,2,93,132,123])).
% 58.83/58.81 cnf(4212,plain,
% 58.83/58.81 (~P5(f13(f17(a1,a1),a2,a7),f17(a1,a1))),
% 58.83/58.81 inference(scs_inference,[],[44,398,4193,4166,4190,74,55,73,2,93,132,123,88,60,38,97])).
% 58.83/58.81 cnf(4222,plain,
% 58.83/58.81 (~P5(f13(f17(a1,a1),a2,a7),f17(f17(a1,a1),f17(a1,a1)))),
% 58.83/58.81 inference(scs_inference,[],[4205,4188,4212,74,73,55,2,93])).
% 58.83/58.81 cnf(4237,plain,
% 58.83/58.81 (~P5(f13(a1,a2,a7),f17(f17(a1,a1),f17(a1,a1)))),
% 58.83/58.81 inference(scs_inference,[],[4222,4203,4206,74,55,73,2,93])).
% 58.83/58.81 cnf(4244,plain,
% 58.83/58.81 (~P5(f13(f17(a1,a1),a7,f17(x42441,a2)),f17(a1,a1))),
% 58.83/58.81 inference(scs_inference,[],[44,398,4187,4222,4203,4206,74,55,73,2,93,89,60,38,97])).
% 58.83/58.81 cnf(4258,plain,
% 58.83/58.81 (~P5(f13(a1,a7,a2),a1)),
% 58.83/58.81 inference(scs_inference,[],[44,4237,4244,4130,1749,74,73,55,2,93,89,60])).
% 58.83/58.81 cnf(4268,plain,
% 58.83/58.81 (~P5(f13(a1,a7,a2),f17(a1,a1))),
% 58.83/58.81 inference(scs_inference,[],[4258,1788,74,55,73,2,93])).
% 58.83/58.81 cnf(4270,plain,
% 58.83/58.81 (~E(a9,f13(a1,a7,a2))),
% 58.83/58.81 inference(scs_inference,[],[4258,1788,74,55,73,2,93,132])).
% 58.83/58.81 cnf(4286,plain,
% 58.83/58.81 (~E(f13(a1,a7,a2),a9)),
% 58.83/58.81 inference(scs_inference,[],[4270,4268,74,73,55,2])).
% 58.83/58.81 cnf(4401,plain,
% 58.83/58.81 (~P5(f13(a1,a7,f17(x44011,a2)),a1)),
% 58.83/58.81 inference(scs_inference,[],[44,2661,2,89,60])).
% 58.83/58.81 cnf(4410,plain,
% 58.83/58.81 (~E(a1,f17(f17(a2,x44101),x44102))),
% 58.83/58.81 inference(scs_inference,[],[4401,2665,74,55,73,2])).
% 58.83/58.81 cnf(4587,plain,
% 58.83/58.81 (~P5(f13(a1,f17(a2,x45871),a7),a1)),
% 58.83/58.81 inference(scs_inference,[],[44,4410,88,60])).
% 58.83/58.81 cnf(4597,plain,
% 58.83/58.81 (~E(f8(a1),f13(a1,f17(a2,x45971),a7))),
% 58.83/58.81 inference(scs_inference,[],[4587,74,55,73,123])).
% 58.83/58.81 cnf(4599,plain,
% 58.83/58.81 (~P5(f13(a1,f17(a2,x45991),a7),f17(a1,a1))),
% 58.83/58.81 inference(scs_inference,[],[4587,74,55,73,123,2,93])).
% 58.83/58.81 cnf(4601,plain,
% 58.83/58.81 (~E(a9,f13(a1,f17(a2,x46011),a7))),
% 58.83/58.81 inference(scs_inference,[],[4587,74,55,73,123,2,93,132])).
% 58.83/58.81 cnf(4614,plain,
% 58.83/58.81 (~E(f8(f17(a1,a1)),f13(a1,f17(a2,x46141),a7))),
% 58.83/58.81 inference(scs_inference,[],[4599,74,73,55,123])).
% 58.83/58.81 cnf(4616,plain,
% 58.83/58.81 (~P5(f13(a1,f17(a2,x46161),a7),f17(f17(a1,a1),f17(a1,a1)))),
% 58.83/58.81 inference(scs_inference,[],[4601,4599,74,73,55,123,2,93])).
% 58.83/58.81 cnf(4618,plain,
% 58.83/58.81 (~E(x46181,f13(a1,f17(a2,x46182),a7))+~E(a9,x46181)),
% 58.83/58.81 inference(scs_inference,[],[4601,4599,74,73,55,123,2,93,3])).
% 58.83/58.81 cnf(4623,plain,
% 58.83/58.81 (~P6(f13(a1,f17(a2,x46231),a7),f17(f17(a1,a1),f17(a1,a1)),x46232)),
% 58.83/58.81 inference(scs_inference,[],[4616,74])).
% 58.83/58.81 cnf(4625,plain,
% 58.83/58.81 (~P2(f13(a1,f17(a2,x46251),a7),f17(f17(a1,a1),f17(a1,a1)))),
% 58.83/58.81 inference(scs_inference,[],[4616,74,55])).
% 58.83/58.81 cnf(4632,plain,
% 58.83/58.81 (~E(x46321,a1)+~E(f17(a2,x46322),x46321)),
% 58.83/58.81 inference(scs_inference,[],[4601,1789,4614,4616,74,55,73,2,52,3])).
% 58.83/58.81 cnf(4640,plain,
% 58.83/58.81 (~E(x46401,f17(a2,x46402))+~E(a1,x46401)),
% 58.83/58.81 inference(scs_inference,[],[4146,3])).
% 58.83/58.81 cnf(4705,plain,
% 58.83/58.81 (~E(x47051,f17(f17(a2,x47052),x47053))+~E(a1,x47051)),
% 58.83/58.81 inference(scs_inference,[],[4410,4286,52,3])).
% 58.83/58.81 cnf(4910,plain,
% 58.83/58.81 (~E(x49101,f13(a1,f17(a2,x49102),a7))+~E(f8(a1),x49101)),
% 58.83/58.81 inference(scs_inference,[],[4597,3])).
% 58.83/58.81 cnf(4911,plain,
% 58.83/58.81 (~E(x49111,f17(a2,x49112))+~E(f8(a1),f13(a1,x49111,a7))),
% 58.83/58.81 inference(scs_inference,[],[4597,3,17])).
% 58.83/58.81 cnf(5470,plain,
% 58.83/58.81 (E(f6(a2,a1),f17(a2,a1))),
% 58.83/58.81 inference(scs_inference,[],[4152,4178,46,91,51,56,75])).
% 58.83/58.81 cnf(5472,plain,
% 58.83/58.81 (P5(a9,a1)),
% 58.83/58.81 inference(scs_inference,[],[4152,4178,46,91,51,56,75,73])).
% 58.83/58.81 cnf(5478,plain,
% 58.83/58.81 (~P5(f11(f17(a2,a7),f17(a2,a1)),f17(a2,a7))),
% 58.83/58.81 inference(scs_inference,[],[4152,4616,4178,46,48,91,51,56,75,73,54,5,6,70])).
% 58.83/58.81 cnf(5480,plain,
% 58.83/58.81 (P5(f8(x54801),x54801)),
% 58.83/58.81 inference(scs_inference,[],[4152,4616,4178,46,45,48,91,51,56,75,73,54,5,6,70,55])).
% 58.83/58.81 cnf(5485,plain,
% 58.83/58.81 (E(f17(a2,a1),f6(a2,a1))),
% 58.83/58.81 inference(scs_inference,[],[4152,4616,4178,46,45,48,91,51,56,75,73,54,5,6,70,55,77,4,2])).
% 58.83/58.81 cnf(5487,plain,
% 58.83/58.81 (P5(a9,a2)),
% 58.83/58.81 inference(scs_inference,[],[4152,4616,4178,46,45,48,91,51,56,75,73,54,5,6,70,55,77,4,2,17,74])).
% 58.83/58.81 cnf(5498,plain,
% 58.83/58.81 (~P4(f8(x54981),x54981)),
% 58.83/58.81 inference(rename_variables,[],[4052])).
% 58.83/58.81 cnf(5501,plain,
% 58.83/58.81 (~P4(f8(x55011),x55011)),
% 58.83/58.81 inference(rename_variables,[],[4052])).
% 58.83/58.81 cnf(5504,plain,
% 58.83/58.81 (~P4(f8(x55041),x55041)),
% 58.83/58.81 inference(rename_variables,[],[4052])).
% 58.83/58.81 cnf(5507,plain,
% 58.83/58.81 (~P4(f8(x55071),x55071)),
% 58.83/58.81 inference(rename_variables,[],[4052])).
% 58.83/58.81 cnf(5510,plain,
% 58.83/58.81 (~P4(f8(x55101),x55101)),
% 58.83/58.81 inference(rename_variables,[],[4052])).
% 58.83/58.81 cnf(5513,plain,
% 58.83/58.81 (~P4(f8(x55131),x55131)),
% 58.83/58.81 inference(rename_variables,[],[4052])).
% 58.83/58.81 cnf(5521,plain,
% 58.83/58.81 (~P1(f17(f17(a2,a1),x55211),f17(a2,a7))),
% 58.83/58.81 inference(scs_inference,[],[4152,1691,4616,328,4178,4212,4052,5498,5501,5504,5507,5510,46,45,325,48,91,51,56,75,73,54,5,6,70,55,77,4,2,17,74,16,18,92,61,62,66,67,69,78,79,68,31,3,38,32,40,60])).
% 58.83/58.81 cnf(5530,plain,
% 58.83/58.81 (~P6(x55301,f17(a2,a7),f17(a2,a7))),
% 58.83/58.81 inference(scs_inference,[],[4152,4623,4625,1691,4616,328,1687,4178,4212,4052,5498,5501,5504,5507,5510,5513,1726,46,45,325,48,91,51,56,75,73,54,5,6,70,55,77,4,2,17,74,16,18,92,61,62,66,67,69,78,79,68,31,3,38,32,40,60,39,35,33,65,82])).
% 58.83/58.81 cnf(5567,plain,
% 58.83/58.81 (P4(f10(a1),a1)),
% 58.83/58.81 inference(scs_inference,[],[4152,4623,4625,1691,4616,328,1687,4178,4212,4052,5498,5501,5504,5507,5510,5513,1726,46,45,325,48,91,51,56,75,73,54,5,6,70,55,77,4,2,17,74,16,18,92,61,62,66,67,69,78,79,68,31,3,38,32,40,60,39,35,33,65,82,118,215,4070,57,11,12,13,14,15,19,20,21,22,24,25,26,27,28,29,30,231,776,4705,7,8,9,4024,4618,4910,337,167])).
% 58.83/58.81 cnf(5572,plain,
% 58.83/58.81 (P2(f8(f17(a2,a1)),f6(a2,a1))),
% 58.83/58.81 inference(scs_inference,[],[4152,4623,4625,1691,4616,328,1687,4178,4212,4052,5498,5501,5504,5507,5510,5513,1726,46,45,325,48,91,51,56,75,73,54,5,6,70,55,77,4,2,17,74,16,18,92,61,62,66,67,69,78,79,68,31,3,38,32,40,60,39,35,33,65,82,118,215,4070,57,11,12,13,14,15,19,20,21,22,24,25,26,27,28,29,30,231,776,4705,7,8,9,4024,4618,4910,337,167,63,23,123])).
% 58.83/58.81 cnf(5598,plain,
% 58.83/58.81 (P5(a9,a7)),
% 58.83/58.81 inference(scs_inference,[],[5567,5478,47,91,56,4070,337,63,73])).
% 58.83/58.81 cnf(5600,plain,
% 58.83/58.81 (E(f6(a2,a7),f17(a2,a7))),
% 58.83/58.81 inference(scs_inference,[],[5567,5478,47,91,56,4070,337,63,73,75])).
% 58.83/58.81 cnf(5606,plain,
% 58.83/58.81 (E(f17(a2,a7),f6(a2,a7))),
% 58.83/58.81 inference(scs_inference,[],[5567,5478,5572,47,91,56,4070,337,63,73,75,54,55,2])).
% 58.83/58.81 cnf(5607,plain,
% 58.83/58.81 (~P5(f11(f17(a2,a7),f17(a2,a1)),a2)),
% 58.83/58.81 inference(scs_inference,[],[5567,5478,5572,47,91,56,4070,337,63,73,75,54,55,2,92])).
% 58.83/58.81 cnf(5615,plain,
% 58.83/58.81 (~P5(f11(f17(a2,a7),f17(a2,a1)),f17(a7,a7))),
% 58.83/58.81 inference(scs_inference,[],[5485,5567,5478,5572,4052,47,325,91,56,4070,337,63,73,75,54,55,2,92,61,62,41,93])).
% 58.83/58.81 cnf(5625,plain,
% 58.83/58.81 (P5(f13(a1,a2,a1),f17(a2,x56251))),
% 58.83/58.81 inference(rename_variables,[],[1697])).
% 58.83/58.81 cnf(5626,plain,
% 58.83/58.81 (~P6(x56261,f17(a2,a7),f17(a2,a7))),
% 58.83/58.81 inference(rename_variables,[],[5530])).
% 58.83/58.81 cnf(5632,plain,
% 58.83/58.81 (P4(a9,a1)),
% 58.83/58.81 inference(scs_inference,[],[5472,5487,5480,5530,5485,5470,5567,5521,5478,5572,1683,1724,4052,1697,46,47,325,48,91,56,4070,337,63,73,75,54,55,2,92,61,62,41,93,31,36,60,39,32,85,65,82,81])).
% 58.83/58.81 cnf(5638,plain,
% 58.83/58.81 (~P5(f11(f17(a2,a7),f17(a2,a1)),a1)),
% 58.83/58.81 inference(scs_inference,[],[5472,5487,5480,5530,5626,5485,5470,5567,5521,5478,5572,1683,1724,4052,1697,5625,46,47,325,48,91,56,4070,337,63,73,75,54,55,2,92,61,62,41,93,31,36,60,39,32,85,65,82,81,90,95])).
% 58.83/58.81 cnf(5649,plain,
% 58.83/58.81 (P5(f16(a2),a2)),
% 58.83/58.81 inference(scs_inference,[],[5472,5487,5480,5530,5626,5485,5470,5567,5521,5478,5572,1683,1724,4052,1697,5625,46,47,325,48,91,56,4070,337,63,73,75,54,55,2,92,61,62,41,93,31,36,60,39,32,85,65,82,81,90,95,4632,4640,4911,59,151,776,215])).
% 58.83/58.81 cnf(5653,plain,
% 58.83/58.81 (P2(f8(f6(a2,a7)),f17(a2,a7))),
% 58.83/58.81 inference(scs_inference,[],[5472,5487,5480,5530,5626,5485,5470,5567,5521,5478,5572,1683,1724,4052,1697,5625,46,47,325,48,91,56,4070,337,63,73,75,54,55,2,92,61,62,41,93,31,36,60,39,32,85,65,82,81,90,95,4632,4640,4911,59,151,776,215,57,118])).
% 58.83/58.81 cnf(5658,plain,
% 58.83/58.82 (~P5(f11(f17(a2,a7),f6(a2,a1)),f17(a2,a7))),
% 58.83/58.82 inference(scs_inference,[],[5472,5487,5480,5530,5626,5485,5470,5567,5521,5478,5572,1683,1724,4052,1697,5625,46,47,325,48,91,56,4070,337,63,73,75,54,55,2,92,61,62,41,93,31,36,60,39,32,85,65,82,81,90,95,4632,4640,4911,59,151,776,215,57,118,231,167,70])).
% 58.83/58.82 cnf(5691,plain,
% 58.83/58.82 ($false),
% 58.83/58.82 inference(scs_inference,[],[5632,5598,5606,5600,5649,5653,5658,5615,5607,5638,4052,325,91,95,57,4070,63,56,337,54,55,92,61,62,41,93]),
% 58.83/58.82 ['proof']).
% 58.83/58.82 % SZS output end Proof
% 58.83/58.82 % Total time :58.160000s
%------------------------------------------------------------------------------