%------------------------------------------------------------------------------
% 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/sandbox2/solver/bin/mcs_scs.jar %d %s
% Computer : n017.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 : Theorem 58.89s 58.98s
% Output : CNFRefutation 58.99s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : GEO111+1 : TPTP v8.2.0. Released v2.4.0.
% 0.07/0.12 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% 0.13/0.34 % Computer : n017.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 10:37:24 EDT 2024
% 0.13/0.34 % CPUTime :
% 0.20/0.59 start to proof:theBenchmark
% 58.89/58.97 %-------------------------------------------
% 58.89/58.97 % File :CSE---1.7
% 58.89/58.97 % Problem :theBenchmark
% 58.89/58.97 % Transform :cnf
% 58.89/58.97 % Format :tptp:raw
% 58.89/58.97 % Command :java -jar mcs_scs.jar %d %s
% 58.89/58.97
% 58.89/58.97 % Result :Theorem 58.330000s
% 58.89/58.97 % Output :CNFRefutation 58.330000s
% 58.89/58.97 %-------------------------------------------
% 58.89/58.98 %--------------------------------------------------------------------------
% 58.89/58.98 % File : GEO111+1 : TPTP v8.2.0. Released v2.4.0.
% 58.89/58.98 % Domain : Geometry (Oriented curves)
% 58.89/58.98 % Problem : Basic property of orderings on linear structures 1
% 58.89/58.98 % Version : [EHK99] axioms.
% 58.89/58.98 % English : If Q is between P and R wrt. c, then P, Q and R are incident
% 58.89/58.98 % with c and are pairwise distinct
% 58.89/58.98
% 58.89/58.98 % Refs : [KE99] Kulik & Eschenbach (1999), A Geometry of Oriented Curv
% 58.89/58.98 % : [EHK99] Eschenbach et al. (1999), Representing Simple Trajecto
% 58.89/58.98 % Source : [KE99]
% 58.89/58.98 % Names : Theorem 3.8 (1) [KE99]
% 58.89/58.98 % : T4 [EHK99]
% 58.89/58.98
% 58.89/58.98 % Status : Theorem
% 58.89/58.98 % Rating : 0.22 v8.2.0, 0.17 v8.1.0, 0.19 v7.5.0, 0.22 v7.4.0, 0.17 v7.3.0, 0.10 v7.2.0, 0.07 v7.1.0, 0.13 v7.0.0, 0.17 v6.4.0, 0.19 v6.3.0, 0.12 v6.2.0, 0.20 v6.1.0, 0.33 v6.0.0, 0.22 v5.5.0, 0.26 v5.4.0, 0.36 v5.3.0, 0.41 v5.2.0, 0.20 v5.1.0, 0.19 v5.0.0, 0.25 v4.1.0, 0.26 v4.0.0, 0.25 v3.7.0, 0.20 v3.5.0, 0.21 v3.4.0, 0.32 v3.3.0, 0.21 v3.2.0, 0.18 v3.1.0, 0.33 v2.7.0, 0.17 v2.6.0, 0.33 v2.5.0, 0.17 v2.4.0
% 58.89/58.98 % Syntax : Number of formulae : 18 ( 1 unt; 0 def)
% 58.89/58.98 % Number of atoms : 80 ( 14 equ)
% 58.89/58.98 % Maximal formula atoms : 12 ( 4 avg)
% 58.89/58.98 % Number of connectives : 70 ( 8 ~; 9 |; 30 &)
% 58.89/58.98 % ( 10 <=>; 13 =>; 0 <=; 0 <~>)
% 58.89/58.98 % Maximal formula depth : 12 ( 8 avg)
% 58.89/58.98 % Maximal term depth : 2 ( 1 avg)
% 58.89/58.98 % Number of predicates : 9 ( 8 usr; 0 prp; 1-4 aty)
% 58.89/58.98 % Number of functors : 1 ( 1 usr; 0 con; 2-2 aty)
% 58.89/58.98 % Number of variables : 62 ( 52 !; 10 ?)
% 58.89/58.98 % SPC : FOF_THM_RFO_SEQ
% 58.89/58.98
% 58.89/58.98 % Comments :
% 58.89/58.98 %--------------------------------------------------------------------------
% 58.89/58.98 %----Include simple curve axioms
% 58.89/58.98 include('Axioms/GEO004+0.ax').
% 58.89/58.98 %----Include axioms of betweenness for simple curves
% 58.89/58.98 include('Axioms/GEO004+1.ax').
% 58.89/58.98 %--------------------------------------------------------------------------
% 58.89/58.98 fof(theorem_3_8_1,conjecture,
% 58.89/58.98 ! [C,P,Q,R] :
% 58.89/58.98 ( between_c(C,P,Q,R)
% 58.89/58.98 => ( incident_c(P,C)
% 58.89/58.98 & incident_c(Q,C)
% 58.89/58.98 & incident_c(R,C)
% 58.89/58.98 & P != Q
% 58.89/58.98 & Q != R
% 58.89/58.98 & P != R ) ) ).
% 58.89/58.98
% 58.89/58.98 %--------------------------------------------------------------------------
% 58.89/58.98 %-------------------------------------------
% 58.89/58.98 % Proof found
% 58.89/58.98 % SZS status Theorem for theBenchmark
% 58.89/58.98 % SZS output start Proof
% 58.89/58.99 %ClaNum:102(EqnAxiom:51)
% 58.89/58.99 %VarNum:387(SingletonVarNum:138)
% 58.89/58.99 %MaxLitNum:12
% 58.89/58.99 %MaxfuncDepth:2
% 58.89/58.99 %SharedTerms:11
% 58.89/58.99 %goalClause: 53 65
% 58.89/58.99 %singleGoalClaCount:1
% 58.89/58.99 [53]P2(a2,a8,a9,a10)
% 58.89/58.99 [52]P1(f1(x521),x521)
% 58.89/58.99 [54]P3(x541)+P4(f11(x541),x541)
% 58.89/58.99 [56]~P6(x561)+P4(f17(x561),x561)
% 58.89/58.99 [55]P6(x551)+~P4(x552,x551)
% 58.89/58.99 [58]~P3(x581)+~P4(x582,x581)
% 58.89/58.99 [59]~P4(x591,x592)+P5(x591,x592)
% 58.89/58.99 [60]~P1(x601,x602)+P5(x601,x602)
% 58.89/58.99 [61]~P1(x611,x612)+~P4(x611,x612)
% 58.89/58.99 [62]~P4(x622,x621)+~E(f3(x621,x622),x622)
% 58.89/58.99 [64]P8(x641,x642)+P5(f12(x642,x641),x641)
% 58.89/58.99 [69]~P4(x692,x691)+P4(f3(x691,x692),x691)
% 58.89/58.99 [76]P8(x761,x762)+~P5(f12(x762,x761),x762)
% 58.89/58.99 [83]~P1(x831,x832)+P7(x831,f19(x832,x831),f4(x832,x831))
% 58.89/58.99 [78]~P1(x782,x781)+E(f18(f19(x781,x782),f4(x781,x782)),x781)
% 58.89/58.99 [79]P5(x791,x792)+~P7(x791,x793,x792)
% 58.89/58.99 [80]P5(x801,x802)+~P7(x801,x802,x803)
% 58.89/58.99 [81]~P7(x813,x811,x812)+E(f6(x811,x812),f18(x811,x812))
% 58.89/58.99 [95]~E(x951,x952)+~P2(x953,x951,x954,x952)
% 58.89/58.99 [99]~P2(x992,x993,x994,x991)+P4(x991,f7(x992,x993,x994,x991))
% 58.89/58.99 [100]~P2(x1002,x1001,x1003,x1004)+P4(x1001,f7(x1002,x1001,x1003,x1004))
% 58.89/58.99 [101]~P2(x1012,x1013,x1011,x1014)+P1(x1011,f7(x1012,x1013,x1011,x1014))
% 58.89/58.99 [102]~P2(x1021,x1022,x1023,x1024)+P8(f7(x1021,x1022,x1023,x1024),x1021)
% 58.89/58.99 [57]P6(x571)+~P8(x571,x572)+E(x571,x572)
% 58.89/58.99 [63]P1(x631,x632)+~P5(x631,x632)+P4(x631,x632)
% 58.89/58.99 [72]~P5(x721,x722)+P4(x721,x722)+P5(x721,f13(x721,x722))
% 58.89/58.99 [73]~P5(x731,x732)+P4(x731,x732)+P5(x731,f15(x731,x732))
% 58.89/58.99 [74]~P5(x741,x742)+P4(x741,x742)+P8(f13(x741,x742),x742)
% 58.89/58.99 [75]~P5(x751,x752)+P4(x751,x752)+P8(f15(x751,x752),x752)
% 58.89/58.99 [77]E(x771,x772)+P5(f5(x771,x772),x772)+P5(f5(x771,x772),x771)
% 58.89/58.99 [82]E(x821,x822)+~P5(f5(x821,x822),x822)+~P5(f5(x821,x822),x821)
% 58.89/58.99 [84]~P5(x841,x842)+P4(x841,x842)+~P8(f13(x841,x842),f15(x841,x842))
% 58.89/58.99 [85]~P5(x851,x852)+P4(x851,x852)+~P8(f15(x851,x852),f13(x851,x852))
% 58.89/58.99 [66]~P5(x661,x663)+P5(x661,x662)+~P8(x663,x662)
% 58.89/58.99 [96]~P5(f14(x961,x962,x963),x963)+~P5(f14(x961,x962,x963),x961)+E(x961,f18(x962,x963))
% 58.89/58.99 [97]~P5(f14(x971,x972,x973),x972)+~P5(f14(x971,x972,x973),x971)+E(x971,f18(x972,x973))
% 58.89/58.99 [67]~P5(x671,x674)+P5(x671,x672)+~E(x672,f18(x673,x674))
% 58.89/58.99 [68]~P5(x681,x683)+P5(x681,x682)+~E(x682,f18(x683,x684))
% 58.89/58.99 [90]~P5(x901,x903)+~P5(x901,x902)+P7(x901,x902,x903)+P5(f16(x901,x902,x903),x903)
% 58.89/58.99 [91]~P5(x911,x913)+~P5(x911,x912)+P7(x911,x912,x913)+P5(f16(x911,x912,x913),x912)
% 58.89/58.99 [94]P5(f14(x941,x942,x943),x943)+P5(f14(x941,x942,x943),x942)+P5(f14(x941,x942,x943),x941)+E(x941,f18(x942,x943))
% 58.89/58.99 [87]~P5(x871,x872)+P4(x871,x872)+~P7(x874,x873,x872)+~P5(x871,x873)
% 58.89/58.99 [88]~P5(x881,x882)+P4(x881,x882)+~P7(x884,x882,x883)+~P5(x881,x883)
% 58.89/58.99 [71]~P5(x711,x714)+P5(x711,x712)+P5(x711,x713)+~E(x714,f18(x713,x712))
% 58.89/58.99 [98]~P5(x981,x983)+~P5(x981,x982)+P7(x981,x982,x983)+~P4(f16(x981,x982,x983),x983)+~P4(f16(x981,x982,x983),x982)
% 58.89/58.99 [89]~P3(x894)+~P4(x891,x892)+P7(x891,x892,x893)+~P7(x895,x892,x893)+~E(x894,f18(x892,x893))
% 58.89/58.99 [65]E(a9,a8)+E(a10,a8)+E(a10,a9)+~P5(a8,a2)+~P5(a9,a2)+~P5(a10,a2)
% 58.89/58.99 [70]E(x703,x701)+~P4(x701,x704)+~P4(x703,x704)+E(x701,x702)+E(x703,x702)+~P4(x702,x704)
% 58.89/58.99 [93]~P4(x932,x935)+~P4(x931,x935)+~P1(x934,x935)+E(x931,x932)+P2(x933,x931,x934,x932)+~P8(x935,x933)
% 58.89/58.99 [86]P8(x862,x861)+~P8(x862,x863)+~P5(x864,x862)+~P4(x864,x863)+P8(x861,x862)+~P8(x861,x863)+~P5(x864,x861)
% 58.89/58.99 [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)
% 58.89/58.99 %EqnAxiom
% 58.89/58.99 [1]E(x11,x11)
% 58.89/58.99 [2]E(x22,x21)+~E(x21,x22)
% 58.89/58.99 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 58.89/58.99 [4]~E(x41,x42)+E(f1(x41),f1(x42))
% 58.89/58.99 [5]~E(x51,x52)+E(f11(x51),f11(x52))
% 58.89/58.99 [6]~E(x61,x62)+E(f17(x61),f17(x62))
% 58.89/58.99 [7]~E(x71,x72)+E(f3(x71,x73),f3(x72,x73))
% 58.89/58.99 [8]~E(x81,x82)+E(f3(x83,x81),f3(x83,x82))
% 58.89/58.99 [9]~E(x91,x92)+E(f12(x91,x93),f12(x92,x93))
% 58.89/58.99 [10]~E(x101,x102)+E(f12(x103,x101),f12(x103,x102))
% 58.89/58.99 [11]~E(x111,x112)+E(f18(x111,x113),f18(x112,x113))
% 58.89/58.99 [12]~E(x121,x122)+E(f18(x123,x121),f18(x123,x122))
% 58.89/58.99 [13]~E(x131,x132)+E(f7(x131,x133,x134,x135),f7(x132,x133,x134,x135))
% 58.89/58.99 [14]~E(x141,x142)+E(f7(x143,x141,x144,x145),f7(x143,x142,x144,x145))
% 58.89/58.99 [15]~E(x151,x152)+E(f7(x153,x154,x151,x155),f7(x153,x154,x152,x155))
% 58.89/58.99 [16]~E(x161,x162)+E(f7(x163,x164,x165,x161),f7(x163,x164,x165,x162))
% 58.89/58.99 [17]~E(x171,x172)+E(f14(x171,x173,x174),f14(x172,x173,x174))
% 58.89/58.99 [18]~E(x181,x182)+E(f14(x183,x181,x184),f14(x183,x182,x184))
% 58.89/58.99 [19]~E(x191,x192)+E(f14(x193,x194,x191),f14(x193,x194,x192))
% 58.89/58.99 [20]~E(x201,x202)+E(f16(x201,x203,x204),f16(x202,x203,x204))
% 58.89/58.99 [21]~E(x211,x212)+E(f16(x213,x211,x214),f16(x213,x212,x214))
% 58.89/58.99 [22]~E(x221,x222)+E(f16(x223,x224,x221),f16(x223,x224,x222))
% 58.89/58.99 [23]~E(x231,x232)+E(f13(x231,x233),f13(x232,x233))
% 58.89/58.99 [24]~E(x241,x242)+E(f13(x243,x241),f13(x243,x242))
% 58.89/58.99 [25]~E(x251,x252)+E(f15(x251,x253),f15(x252,x253))
% 58.89/58.99 [26]~E(x261,x262)+E(f15(x263,x261),f15(x263,x262))
% 58.89/58.99 [27]~E(x271,x272)+E(f4(x271,x273),f4(x272,x273))
% 58.89/58.99 [28]~E(x281,x282)+E(f4(x283,x281),f4(x283,x282))
% 58.89/58.99 [29]~E(x291,x292)+E(f5(x291,x293),f5(x292,x293))
% 58.89/58.99 [30]~E(x301,x302)+E(f5(x303,x301),f5(x303,x302))
% 58.89/58.99 [31]~E(x311,x312)+E(f19(x311,x313),f19(x312,x313))
% 58.89/58.99 [32]~E(x321,x322)+E(f19(x323,x321),f19(x323,x322))
% 58.89/58.99 [33]~E(x331,x332)+E(f6(x331,x333),f6(x332,x333))
% 58.89/59.00 [34]~E(x341,x342)+E(f6(x343,x341),f6(x343,x342))
% 58.89/59.00 [35]P1(x352,x353)+~E(x351,x352)+~P1(x351,x353)
% 58.99/59.00 [36]P1(x363,x362)+~E(x361,x362)+~P1(x363,x361)
% 58.99/59.00 [37]P2(x372,x373,x374,x375)+~E(x371,x372)+~P2(x371,x373,x374,x375)
% 58.99/59.00 [38]P2(x383,x382,x384,x385)+~E(x381,x382)+~P2(x383,x381,x384,x385)
% 58.99/59.00 [39]P2(x393,x394,x392,x395)+~E(x391,x392)+~P2(x393,x394,x391,x395)
% 58.99/59.00 [40]P2(x403,x404,x405,x402)+~E(x401,x402)+~P2(x403,x404,x405,x401)
% 58.99/59.00 [41]~P3(x411)+P3(x412)+~E(x411,x412)
% 58.99/59.00 [42]P4(x422,x423)+~E(x421,x422)+~P4(x421,x423)
% 58.99/59.00 [43]P4(x433,x432)+~E(x431,x432)+~P4(x433,x431)
% 58.99/59.00 [44]~P6(x441)+P6(x442)+~E(x441,x442)
% 58.99/59.00 [45]P5(x452,x453)+~E(x451,x452)+~P5(x451,x453)
% 58.99/59.00 [46]P5(x463,x462)+~E(x461,x462)+~P5(x463,x461)
% 58.99/59.00 [47]P7(x472,x473,x474)+~E(x471,x472)+~P7(x471,x473,x474)
% 58.99/59.00 [48]P7(x483,x482,x484)+~E(x481,x482)+~P7(x483,x481,x484)
% 58.99/59.00 [49]P7(x493,x494,x492)+~E(x491,x492)+~P7(x493,x494,x491)
% 58.99/59.00 [50]P8(x502,x503)+~E(x501,x502)+~P8(x501,x503)
% 58.99/59.00 [51]P8(x513,x512)+~E(x511,x512)+~P8(x513,x511)
% 58.99/59.00
% 58.99/59.00 %-------------------------------------------
% 58.99/59.00 cnf(103,plain,
% 58.99/59.00 (~P5(x1031,x1032)+P5(x1031,f18(x1033,x1032))),
% 58.99/59.00 inference(equality_inference,[],[67])).
% 58.99/59.00 cnf(104,plain,
% 58.99/59.00 (~P5(x1041,x1042)+P5(x1041,f18(x1042,x1043))),
% 58.99/59.00 inference(equality_inference,[],[68])).
% 58.99/59.00 cnf(105,plain,
% 58.99/59.00 (~P5(x1051,f18(x1052,x1053))+P5(x1051,x1053)+P5(x1051,x1052)),
% 58.99/59.00 inference(equality_inference,[],[71])).
% 58.99/59.00 cnf(107,plain,
% 58.99/59.00 (~P2(x1072,x1071,x1073,x1071)),
% 58.99/59.00 inference(equality_inference,[],[95])).
% 58.99/59.00 cnf(108,plain,
% 58.99/59.00 (~E(a8,a10)),
% 58.99/59.00 inference(scs_inference,[],[53,107,38])).
% 58.99/59.00 cnf(109,plain,
% 58.99/59.00 (~P2(x1091,x1092,x1093,x1092)),
% 58.99/59.00 inference(rename_variables,[],[107])).
% 58.99/59.00 cnf(110,plain,
% 58.99/59.00 (~E(a10,a8)),
% 58.99/59.00 inference(scs_inference,[],[53,107,109,38,40])).
% 58.99/59.00 cnf(112,plain,
% 58.99/59.00 (P1(x1121,x1122)+~E(f1(x1122),x1121)),
% 58.99/59.00 inference(scs_inference,[],[53,107,109,52,38,40,35])).
% 58.99/59.00 cnf(113,plain,
% 58.99/59.00 (P1(f1(x1131),x1132)+~E(x1131,x1132)),
% 58.99/59.00 inference(scs_inference,[],[53,107,109,52,38,40,35,36])).
% 58.99/59.00 cnf(114,plain,
% 58.99/59.00 (P2(x1141,a8,a9,a10)+~E(a2,x1141)),
% 58.99/59.00 inference(scs_inference,[],[53,107,109,52,38,40,35,36,37])).
% 58.99/59.00 cnf(115,plain,
% 58.99/59.00 (P2(a2,a8,x1151,a10)+~E(a9,x1151)),
% 58.99/59.00 inference(scs_inference,[],[53,107,109,52,38,40,35,36,37,39])).
% 58.99/59.00 cnf(122,plain,
% 58.99/59.00 (E(a9,a8)+E(a10,a9)+~P5(a8,a2)+~P5(a9,a2)+~P5(a10,a2)),
% 58.99/59.00 inference(scs_inference,[],[110,65])).
% 58.99/59.00 cnf(126,plain,
% 58.99/59.00 (~P4(x1261,x1262)+~P4(a10,x1262)+P2(x1262,a8,f1(x1262),a10)+~P4(a8,x1262)+~P8(x1262,x1263)),
% 58.99/59.00 inference(scs_inference,[],[108,52,93,92])).
% 58.99/59.00 cnf(139,plain,
% 58.99/59.00 (~P4(x1391,x1392)+P4(f17(x1392),x1392)),
% 58.99/59.00 inference(scs_inference,[],[55,56])).
% 58.99/59.00 cnf(155,plain,
% 58.99/59.00 (~P4(x1551,x1552)+P4(f11(x1552),x1552)),
% 58.99/59.00 inference(scs_inference,[],[58,54])).
% 58.99/59.00 cnf(219,plain,
% 58.99/59.00 (~P4(x2191,x2192)+P5(x2191,f18(x2193,x2192))),
% 58.99/59.00 inference(scs_inference,[],[59,103])).
% 58.99/59.00 cnf(235,plain,
% 58.99/59.00 (P5(f1(x2351),f18(x2351,x2352))),
% 58.99/59.00 inference(scs_inference,[],[52,60,104])).
% 58.99/59.00 cnf(333,plain,
% 58.99/59.00 (~P4(x3331,x3332)+~P1(f17(x3332),x3332)),
% 58.99/59.00 inference(scs_inference,[],[139,61])).
% 58.99/59.00 cnf(381,plain,
% 58.99/59.00 (~E(f1(x3811),f17(x3811))+~P4(x3812,x3811)),
% 58.99/59.00 inference(scs_inference,[],[333,112])).
% 58.99/59.00 cnf(445,plain,
% 58.99/59.00 (P4(f3(f7(a2,a8,a9,a10),a10),f7(a2,a8,a9,a10))),
% 58.99/59.00 inference(scs_inference,[],[53,69,99])).
% 58.99/59.00 cnf(448,plain,
% 58.99/59.00 (~P1(f3(f7(a2,a8,a9,a10),a10),f7(a2,a8,a9,a10))),
% 58.99/59.00 inference(scs_inference,[],[445,219,61])).
% 58.99/59.00 cnf(450,plain,
% 58.99/59.00 (~E(f1(f7(a2,a8,a9,a10)),f3(f7(a2,a8,a9,a10),a10))),
% 58.99/59.00 inference(scs_inference,[],[52,445,219,61,35])).
% 58.99/59.00 cnf(486,plain,
% 58.99/59.00 (P4(x4861,f7(a2,a8,a9,a10))+~E(f3(f7(a2,a8,a9,a10),a10),x4861)),
% 58.99/59.00 inference(scs_inference,[],[450,445,57,42])).
% 58.99/59.00 cnf(1214,plain,
% 58.99/59.00 (P4(a8,f7(x12141,a8,a9,a10))+~E(a2,x12141)),
% 58.99/59.01 inference(scs_inference,[],[100,114])).
% 58.99/59.01 cnf(1215,plain,
% 58.99/59.01 (P4(a8,f7(a2,a8,a9,a10))),
% 58.99/59.01 inference(equality_inference,[],[1214])).
% 58.99/59.01 cnf(1218,plain,
% 58.99/59.01 (~P1(a8,f7(a2,a8,a9,a10))),
% 58.99/59.01 inference(scs_inference,[],[1215,219,61])).
% 58.99/59.01 cnf(1278,plain,
% 58.99/59.01 (P1(x12781,f7(a2,a8,x12781,a10))+~E(a9,x12781)),
% 58.99/59.01 inference(scs_inference,[],[101,115])).
% 58.99/59.01 cnf(1279,plain,
% 58.99/59.01 (P1(a9,f7(a2,a8,a9,a10))),
% 58.99/59.01 inference(equality_inference,[],[1278])).
% 58.99/59.01 cnf(1280,plain,
% 58.99/59.01 (~E(a9,f3(f7(a2,a8,a9,a10),a10))),
% 58.99/59.01 inference(scs_inference,[],[1279,448,35])).
% 58.99/59.01 cnf(1287,plain,
% 58.99/59.01 (~E(a9,a8)),
% 58.99/59.01 inference(scs_inference,[],[1279,1218,35])).
% 58.99/59.01 cnf(1290,plain,
% 58.99/59.01 (E(a10,a9)+~P5(a10,a2)+~P5(a9,a2)+~P5(a8,a2)),
% 58.99/59.01 inference(scs_inference,[],[1215,1279,1218,35,122])).
% 58.99/59.01 cnf(1384,plain,
% 58.99/59.01 (P8(f7(x13841,a8,a9,a10),x13841)+~E(a2,x13841)),
% 58.99/59.01 inference(scs_inference,[],[102,114])).
% 58.99/59.01 cnf(1385,plain,
% 58.99/59.01 (P8(f7(a2,a8,a9,a10),a2)),
% 58.99/59.01 inference(equality_inference,[],[1384])).
% 58.99/59.01 cnf(1389,plain,
% 58.99/59.01 (~P5(x13891,f7(a2,a8,a9,a10))+P5(x13891,a2)),
% 58.99/59.01 inference(scs_inference,[],[1385,66])).
% 58.99/59.01 cnf(1420,plain,
% 58.99/59.01 (P2(a2,a10,a9,a8)+~P4(a10,f7(a2,a8,a9,a10))),
% 58.99/59.01 inference(scs_inference,[],[1215,1279,110,1385,93])).
% 58.99/59.01 cnf(1425,plain,
% 58.99/59.01 (~P4(a9,f7(a2,a8,a9,a10))+~E(f3(f7(a2,a8,a9,a10),a10),a9)),
% 58.99/59.01 inference(scs_inference,[],[1279,1280,1385,107,445,93,40])).
% 58.99/59.01 cnf(1438,plain,
% 58.99/59.01 (P5(a8,a2)),
% 58.99/59.01 inference(scs_inference,[],[1215,1389,59])).
% 58.99/59.01 cnf(1439,plain,
% 58.99/59.01 (E(a10,a9)+~P5(a10,a2)+~P5(a9,a2)),
% 58.99/59.01 inference(scs_inference,[],[1438,1290])).
% 58.99/59.01 cnf(1811,plain,
% 58.99/59.01 (~P4(a10,f7(a2,a8,a9,a10))+P4(a8,f7(a2,a10,a9,a8))),
% 58.99/59.01 inference(scs_inference,[],[1420,99])).
% 58.99/59.01 cnf(2172,plain,
% 58.99/59.01 (P4(a8,f7(a2,a10,a9,a8))),
% 58.99/59.01 inference(scs_inference,[],[53,1811,99])).
% 58.99/59.01 cnf(2175,plain,
% 58.99/59.01 (~P1(a8,f7(a2,a10,a9,a8))),
% 58.99/59.01 inference(scs_inference,[],[2172,219,61])).
% 58.99/59.01 cnf(2177,plain,
% 58.99/59.01 (P4(x21771,f7(a2,a10,a9,a8))+~E(a8,x21771)),
% 58.99/59.01 inference(scs_inference,[],[2172,219,61,42])).
% 58.99/59.01 cnf(2179,plain,
% 58.99/59.01 (P5(x21791,f18(x21792,f7(a2,a10,a9,a8)))+~E(a8,x21791)),
% 58.99/59.01 inference(scs_inference,[],[2172,219,61,42,43,45])).
% 58.99/59.01 cnf(2188,plain,
% 58.99/59.01 (~E(f1(f7(a2,a10,a9,a8)),a8)),
% 58.99/59.01 inference(scs_inference,[],[52,2175,35])).
% 58.99/59.01 cnf(2533,plain,
% 58.99/59.01 (~E(f3(f7(a2,a8,a9,a10),a10),a9)),
% 58.99/59.01 inference(scs_inference,[],[1425,486])).
% 58.99/59.01 cnf(4141,plain,
% 58.99/59.01 (~P4(a9,f7(a2,a8,a9,a10))),
% 58.99/59.01 inference(scs_inference,[],[1279,61])).
% 58.99/59.01 cnf(4145,plain,
% 58.99/59.01 (~P4(f1(x41451),x41451)),
% 58.99/59.01 inference(scs_inference,[],[52,61])).
% 58.99/59.01 cnf(4147,plain,
% 58.99/59.01 (~P5(f1(x41471),x41471)+~P7(x41472,f18(x41471,x41473),x41471)),
% 58.99/59.01 inference(scs_inference,[],[52,235,61,87])).
% 58.99/59.01 cnf(4292,plain,
% 58.99/59.01 (~P5(f1(x42921),x42921)+~P7(x42922,x42921,f18(x42921,x42923))),
% 58.99/59.01 inference(scs_inference,[],[235,4145,88])).
% 58.99/59.01 cnf(4336,plain,
% 58.99/59.01 (~P5(a9,x43361)+~P5(a9,f7(a2,a8,a9,a10))+~P7(x43362,f7(a2,a8,a9,a10),x43361)),
% 58.99/59.01 inference(scs_inference,[],[1215,4141,88])).
% 58.99/59.01 cnf(4339,plain,
% 58.99/59.01 (P5(a9,f7(a2,a8,a9,a10))),
% 58.99/59.01 inference(scs_inference,[],[1279,60])).
% 58.99/59.01 cnf(4341,plain,
% 58.99/59.01 (P5(a9,f18(f7(a2,a8,a9,a10),x43411))),
% 58.99/59.01 inference(scs_inference,[],[1279,60,104])).
% 58.99/59.01 cnf(4343,plain,
% 58.99/59.01 (P5(a9,f18(x43431,f7(a2,a8,a9,a10)))),
% 58.99/59.01 inference(scs_inference,[],[1279,60,104,103])).
% 58.99/59.01 cnf(4348,plain,
% 58.99/59.01 (P5(a9,a2)),
% 58.99/59.01 inference(scs_inference,[],[1279,1385,60,104,103,4336,46,66])).
% 58.99/59.01 cnf(4364,plain,
% 58.99/59.01 (E(a10,a9)+~P5(a10,a2)),
% 58.99/59.01 inference(scs_inference,[],[4348,1439])).
% 58.99/59.01 cnf(4370,plain,
% 58.99/59.01 (~P7(x43701,f7(a2,a8,a9,a10),x43702)+~P5(a9,x43702)),
% 58.99/59.01 inference(scs_inference,[],[4339,4336])).
% 58.99/59.01 cnf(4373,plain,
% 58.99/59.01 (P5(f1(x43731),x43731)),
% 58.99/59.01 inference(scs_inference,[],[52,4341,4370,60])).
% 58.99/59.01 cnf(4375,plain,
% 58.99/59.01 (P5(a9,f18(a2,x43751))),
% 58.99/59.01 inference(scs_inference,[],[52,4341,4348,4370,60,104])).
% 58.99/59.01 cnf(4377,plain,
% 58.99/59.01 (P5(a9,f18(x43771,a2))),
% 58.99/59.01 inference(scs_inference,[],[52,4341,4348,4370,60,104,103])).
% 58.99/59.01 cnf(4379,plain,
% 58.99/59.01 (P5(f1(f7(a2,a8,a9,a10)),a2)),
% 58.99/59.01 inference(scs_inference,[],[1385,52,4341,4348,4370,60,104,103,66])).
% 58.99/59.01 cnf(4392,plain,
% 58.99/59.01 (~P7(x43921,f18(x43922,x43923),x43922)),
% 58.99/59.01 inference(scs_inference,[],[4373,4147])).
% 58.99/59.01 cnf(4400,plain,
% 58.99/59.01 (P5(f1(x44001),f18(x44002,x44001))),
% 58.99/59.01 inference(scs_inference,[],[4373,4379,4375,4147,4292,4370,104,103])).
% 58.99/59.01 cnf(4413,plain,
% 58.99/59.01 (P5(f1(x44131),f18(f18(x44132,x44131),x44133))),
% 58.99/59.01 inference(scs_inference,[],[4400,4377,4370,104])).
% 58.99/59.01 cnf(4444,plain,
% 58.99/59.01 (P5(a9,f18(x44441,f18(a2,x44442)))),
% 58.99/59.01 inference(scs_inference,[],[4375,4348,4370,103])).
% 58.99/59.01 cnf(4446,plain,
% 58.99/59.01 (P5(a9,f18(f18(a2,x44461),x44462))),
% 58.99/59.01 inference(scs_inference,[],[4375,4348,4370,103,104])).
% 58.99/59.01 cnf(4457,plain,
% 58.99/59.01 (P5(a8,f7(a2,a8,a9,a10))),
% 58.99/59.01 inference(scs_inference,[],[1215,59])).
% 58.99/59.01 cnf(4461,plain,
% 58.99/59.01 (P5(a9,f18(f18(x44611,a2),x44612))),
% 58.99/59.01 inference(scs_inference,[],[1215,4444,4377,59,4370,104])).
% 58.99/59.01 cnf(4463,plain,
% 58.99/59.01 (P5(a9,f18(x44631,f18(x44632,a2)))),
% 58.99/59.01 inference(scs_inference,[],[1215,4444,4377,59,4370,104,103])).
% 58.99/59.01 cnf(4465,plain,
% 58.99/59.01 (P5(f1(x44651),x44652)+~E(x44651,x44652)),
% 58.99/59.01 inference(scs_inference,[],[1215,4373,4444,4377,59,4370,104,103,46])).
% 58.99/59.01 cnf(4473,plain,
% 58.99/59.01 (P5(a8,f7(a2,a10,a9,a8))),
% 58.99/59.01 inference(scs_inference,[],[2172,59])).
% 58.99/59.01 cnf(4479,plain,
% 58.99/59.01 (P5(f1(f7(a2,a8,a9,a10)),f18(x44791,a2))),
% 58.99/59.01 inference(scs_inference,[],[2172,4457,4446,4379,59,4370,104,103])).
% 58.99/59.01 cnf(4481,plain,
% 58.99/59.01 (P5(x44811,x44812)+~E(f1(x44812),x44811)),
% 58.99/59.01 inference(scs_inference,[],[2172,4373,4457,4446,4379,59,4370,104,103,45])).
% 58.99/59.01 cnf(4482,plain,
% 58.99/59.01 (P5(x44821,a2)+~E(f1(f7(a2,a8,a9,a10)),x44821)),
% 58.99/59.01 inference(scs_inference,[],[1385,2172,4373,4457,4446,4379,59,4370,104,103,45,66])).
% 58.99/59.01 cnf(4503,plain,
% 58.99/59.01 (P5(f3(f7(a2,a8,a9,a10),a10),a2)),
% 58.99/59.01 inference(scs_inference,[],[1385,445,4479,4461,59,4370,104,103,66])).
% 58.99/59.01 cnf(4518,plain,
% 58.99/59.01 (P5(a8,f18(f7(a2,a10,a9,a8),x45181))),
% 58.99/59.01 inference(scs_inference,[],[4473,4463,4370,104])).
% 58.99/59.01 cnf(4520,plain,
% 58.99/59.01 (P5(f3(f7(a2,a8,a9,a10),a10),f18(x45201,a2))),
% 58.99/59.01 inference(scs_inference,[],[4473,4463,4503,4370,104,103])).
% 58.99/59.01 cnf(4522,plain,
% 58.99/59.01 (~E(a8,f1(f7(a2,a10,a9,a8)))),
% 58.99/59.01 inference(scs_inference,[],[2188,4473,4463,4503,4370,104,103,2])).
% 58.99/59.01 cnf(4523,plain,
% 58.99/59.01 (P6(f7(a2,a8,a9,a10))),
% 58.99/59.01 inference(scs_inference,[],[1215,2188,4473,4463,4503,4370,104,103,2,55])).
% 58.99/59.01 cnf(4525,plain,
% 58.99/59.01 (~P3(f7(a2,a8,a9,a10))),
% 58.99/59.01 inference(scs_inference,[],[1215,2188,4473,4463,4503,4370,104,103,2,55,58])).
% 58.99/59.01 cnf(4533,plain,
% 58.99/59.01 (E(a9,a10)+~P5(a10,a2)),
% 58.99/59.01 inference(scs_inference,[],[4364,2])).
% 58.99/59.01 cnf(4550,plain,
% 58.99/59.01 (~E(a8,a9)),
% 58.99/59.01 inference(scs_inference,[],[1287,2])).
% 58.99/59.01 cnf(4551,plain,
% 58.99/59.01 (P5(f3(f7(a2,a8,a9,a10),a10),f18(a2,x45511))),
% 58.99/59.01 inference(scs_inference,[],[1287,4503,2,104])).
% 58.99/59.01 cnf(4584,plain,
% 58.99/59.01 (~P5(a10,f18(a2,a2))+~E(f3(f7(a2,a8,a9,a10),a10),a10)),
% 58.99/59.01 inference(scs_inference,[],[2533,4520,104,3,4364,4482,1389,80,79,2,105])).
% 58.99/59.01 cnf(4589,plain,
% 58.99/59.01 (~E(x45891,a8)+~E(a9,x45891)),
% 58.99/59.01 inference(scs_inference,[],[1287,3])).
% 58.99/59.01 cnf(4608,plain,
% 58.99/59.01 (~E(x46081,a10)+~E(a8,x46081)),
% 58.99/59.01 inference(scs_inference,[],[108,3])).
% 58.99/59.01 cnf(4614,plain,
% 58.99/59.01 (~E(x46141,a8)+~E(a10,x46141)),
% 58.99/59.01 inference(scs_inference,[],[110,3])).
% 58.99/59.01 cnf(4645,plain,
% 58.99/59.01 (~E(x46451,f1(f7(a2,a10,a9,a8)))+~E(a8,x46451)),
% 58.99/59.01 inference(scs_inference,[],[4522,4473,57,66,3])).
% 58.99/59.01 cnf(4660,plain,
% 58.99/59.01 (P5(x46601,f7(a2,a10,a9,a8))+~E(a8,x46601)),
% 58.99/59.01 inference(scs_inference,[],[4550,4473,4375,57,46,66,3,63,45])).
% 58.99/59.01 cnf(4778,plain,
% 58.99/59.01 (P5(x47781,a2)+~E(a9,x47781)),
% 58.99/59.01 inference(scs_inference,[],[4348,45])).
% 58.99/59.01 cnf(5018,plain,
% 58.99/59.01 (~E(f3(f7(a2,a8,a9,a10),a10),a10)),
% 58.99/59.01 inference(scs_inference,[],[4551,45,4584])).
% 58.99/59.01 cnf(5023,plain,
% 58.99/59.01 (~E(a10,f3(f7(a2,a8,a9,a10),a10))),
% 58.99/59.01 inference(scs_inference,[],[5018,2])).
% 58.99/59.01 cnf(5104,plain,
% 58.99/59.01 (P2(a2,a10,a9,f3(f7(a2,a8,a9,a10),a10))+~P4(a10,f7(a2,a8,a9,a10))),
% 58.99/59.01 inference(scs_inference,[],[1385,1279,5023,445,4503,4461,45,66,46,93])).
% 58.99/59.01 cnf(5122,plain,
% 58.99/59.01 (~P4(a10,f7(a2,a8,a9,a10))+P2(a2,f3(f7(a2,a8,a9,a10),a10),a9,a10)),
% 58.99/59.01 inference(scs_inference,[],[1385,1279,5018,445,4520,4343,4413,45,66,46,93])).
% 58.99/59.01 cnf(5277,plain,
% 58.99/59.01 (P5(x52771,f18(f7(a2,a10,a9,a8),x52772))+~E(a8,x52771)),
% 58.99/59.01 inference(scs_inference,[],[4518,45])).
% 58.99/59.01 cnf(5433,plain,
% 58.99/59.01 (~P7(x54331,x54332,x54332)),
% 58.99/59.01 inference(scs_inference,[],[4373,4145,88])).
% 58.99/59.01 cnf(5436,plain,
% 58.99/59.01 (~P7(x54361,x54362,x54363)+~E(x54362,x54363)),
% 58.99/59.01 inference(scs_inference,[],[4373,4145,88,48])).
% 58.99/59.01 cnf(5451,plain,
% 58.99/59.01 (~P4(f1(x54511),x54511)),
% 58.99/59.01 inference(rename_variables,[],[4145])).
% 58.99/59.01 cnf(5452,plain,
% 58.99/59.01 (P5(f1(x54521),f18(x54522,x54521))),
% 58.99/59.01 inference(rename_variables,[],[4400])).
% 58.99/59.01 cnf(5454,plain,
% 58.99/59.01 (~P7(x54541,f18(x54542,x54543),x54543)),
% 58.99/59.01 inference(scs_inference,[],[4400,5452,4373,4145,5451,88,87])).
% 58.99/59.01 cnf(5558,plain,
% 58.99/59.01 (~P7(x55581,f18(x55582,f18(x55583,a2)),f7(a2,a8,a9,a10))),
% 58.99/59.01 inference(scs_inference,[],[4463,4339,4141,87])).
% 58.99/59.01 cnf(5862,plain,
% 58.99/59.01 (E(a8,f3(f7(a2,a8,a9,a10),a10))+~P4(a10,f7(a2,a8,a9,a10))),
% 58.99/59.01 inference(scs_inference,[],[5023,108,1215,445,70])).
% 58.99/59.01 cnf(5864,plain,
% 58.99/59.01 (~P2(x58641,a8,x58642,f3(f7(a2,a8,a9,a10),a10))+~P4(a10,f7(a2,a8,a9,a10))),
% 58.99/59.01 inference(scs_inference,[],[5023,108,1215,445,70,95])).
% 58.99/59.01 cnf(5866,plain,
% 58.99/59.01 (P1(f1(a8),f3(f7(a2,a8,a9,a10),a10))+~P4(a10,f7(a2,a8,a9,a10))),
% 58.99/59.01 inference(scs_inference,[],[5023,108,1215,445,70,95,113])).
% 58.99/59.01 cnf(5867,plain,
% 58.99/59.01 (~P4(a10,f7(a2,a8,a9,a10))+P4(f3(f7(a2,a8,a9,a10),a10),f7(a2,a10,a9,a8))),
% 58.99/59.01 inference(scs_inference,[],[5023,108,1215,445,70,95,113,2177])).
% 58.99/59.01 cnf(5868,plain,
% 58.99/59.01 (~P4(a10,f7(a2,a8,a9,a10))+P5(f3(f7(a2,a8,a9,a10),a10),f18(x58681,f7(a2,a10,a9,a8)))),
% 58.99/59.01 inference(scs_inference,[],[5023,108,1215,445,70,95,113,2177,2179])).
% 58.99/59.01 cnf(5869,plain,
% 58.99/59.01 (P5(f1(a8),f3(f7(a2,a8,a9,a10),a10))+~P4(a10,f7(a2,a8,a9,a10))),
% 58.99/59.01 inference(scs_inference,[],[5023,108,1215,445,70,95,113,2177,2179,4465])).
% 58.99/59.01 cnf(5870,plain,
% 58.99/59.01 (~P4(a10,f7(a2,a8,a9,a10))+~E(f3(f7(a2,a8,a9,a10),a10),f1(f7(a2,a10,a9,a8)))),
% 58.99/59.01 inference(scs_inference,[],[5023,108,1215,445,70,95,113,2177,2179,4465,4645])).
% 58.99/59.01 cnf(5871,plain,
% 58.99/59.01 (~P4(a10,f7(a2,a8,a9,a10))+P5(f3(f7(a2,a8,a9,a10),a10),f7(a2,a10,a9,a8))),
% 58.99/59.01 inference(scs_inference,[],[5023,108,1215,445,70,95,113,2177,2179,4465,4645,4660])).
% 58.99/59.01 cnf(5872,plain,
% 58.99/59.01 (~P4(a10,f7(a2,a8,a9,a10))+P5(f3(f7(a2,a8,a9,a10),a10),f18(f7(a2,a10,a9,a8),x58721))),
% 58.99/59.01 inference(scs_inference,[],[5023,108,1215,445,70,95,113,2177,2179,4465,4645,4660,5277])).
% 58.99/59.01 cnf(5873,plain,
% 58.99/59.01 (~P7(x58731,a8,f3(f7(a2,a8,a9,a10),a10))+~P4(a10,f7(a2,a8,a9,a10))),
% 58.99/59.01 inference(scs_inference,[],[5023,108,1215,445,70,95,113,2177,2179,4465,4645,4660,5277,5436])).
% 58.99/59.01 cnf(5874,plain,
% 58.99/59.01 (~E(f1(f7(a2,a10,a9,a8)),f3(f7(a2,a8,a9,a10),a10))+~P4(a10,f7(a2,a8,a9,a10))),
% 58.99/59.01 inference(scs_inference,[],[5023,108,1215,445,70,95,113,2177,2179,4465,4645,4660,5277,5436,2])).
% 58.99/59.01 cnf(5875,plain,
% 58.99/59.01 (~P4(f1(a8),f3(f7(a2,a8,a9,a10),a10))+~P4(a10,f7(a2,a8,a9,a10))),
% 58.99/59.01 inference(scs_inference,[],[5023,108,1215,445,70,95,113,2177,2179,4465,4645,4660,5277,5436,2,61])).
% 58.99/59.01 cnf(6369,plain,
% 58.99/59.01 (P4(f11(f7(a2,a8,a9,a10)),f7(a2,a8,a9,a10))),
% 58.99/59.01 inference(scs_inference,[],[4525,54])).
% 58.99/59.01 cnf(6373,plain,
% 58.99/59.01 (P4(f17(f7(a2,a10,a9,a8)),f7(a2,a10,a9,a8))),
% 58.99/59.01 inference(scs_inference,[],[4523,4525,2172,54,56,139])).
% 58.99/59.01 cnf(6375,plain,
% 58.99/59.01 (P4(f11(f7(a2,a10,a9,a8)),f7(a2,a10,a9,a8))),
% 58.99/59.01 inference(scs_inference,[],[4523,4525,2172,54,56,139,155])).
% 58.99/59.01 cnf(6379,plain,
% 58.99/59.01 (~E(f3(f7(a2,a8,a9,a10),a8),a8)),
% 58.99/59.01 inference(scs_inference,[],[4523,4525,445,1215,2172,54,56,139,155,333,62])).
% 58.99/59.01 cnf(6381,plain,
% 58.99/59.01 (P4(f3(f7(a2,a8,a9,a10),a8),f7(a2,a8,a9,a10))),
% 58.99/59.01 inference(scs_inference,[],[4523,4525,445,1215,2172,54,56,139,155,333,62,69])).
% 58.99/59.01 cnf(6385,plain,
% 58.99/59.01 (P4(a10,f7(a2,a8,a9,a10))),
% 58.99/59.01 inference(scs_inference,[],[53,4523,4525,445,1215,2172,54,56,139,155,333,62,69,381,99])).
% 58.99/59.01 cnf(6387,plain,
% 58.99/59.01 (~P1(f11(f7(a2,a8,a9,a10)),f7(a2,a8,a9,a10))),
% 58.99/59.01 inference(scs_inference,[],[53,4523,4525,445,1215,2172,54,56,139,155,333,62,69,381,99,61])).
% 58.99/59.01 cnf(6395,plain,
% 58.99/59.01 (P5(f1(x63951),f15(f1(x63951),x63951))),
% 58.99/59.01 inference(scs_inference,[],[53,4523,4525,5433,4339,4373,4145,1279,4141,445,1215,2172,54,56,139,155,333,62,69,381,99,61,83,49,72,73])).
% 58.99/59.01 cnf(6396,plain,
% 58.99/59.01 (~P4(f1(x63961),x63961)),
% 58.99/59.01 inference(rename_variables,[],[4145])).
% 58.99/59.01 cnf(6398,plain,
% 58.99/59.01 (P8(f13(f1(x63981),x63981),x63981)),
% 58.99/59.01 inference(scs_inference,[],[53,4523,4525,5433,4339,4373,4145,6396,1279,4141,445,1215,2172,54,56,139,155,333,62,69,381,99,61,83,49,72,73,74])).
% 58.99/59.01 cnf(6399,plain,
% 58.99/59.01 (~P4(f1(x63991),x63991)),
% 58.99/59.01 inference(rename_variables,[],[4145])).
% 58.99/59.01 cnf(6401,plain,
% 58.99/59.01 (P8(f15(f1(x64011),x64011),x64011)),
% 58.99/59.01 inference(scs_inference,[],[53,4523,4525,5433,4339,4373,4145,6396,6399,1279,4141,445,1215,2172,54,56,139,155,333,62,69,381,99,61,83,49,72,73,74,75])).
% 58.99/59.01 cnf(6402,plain,
% 58.99/59.01 (~P4(f1(x64021),x64021)),
% 58.99/59.01 inference(rename_variables,[],[4145])).
% 58.99/59.01 cnf(6405,plain,
% 58.99/59.01 (~P4(f1(x64051),x64051)),
% 58.99/59.01 inference(rename_variables,[],[4145])).
% 58.99/59.01 cnf(6408,plain,
% 58.99/59.01 (~P4(f1(x64081),x64081)),
% 58.99/59.01 inference(rename_variables,[],[4145])).
% 58.99/59.01 cnf(6416,plain,
% 58.99/59.01 (P2(a2,a10,a9,a8)),
% 58.99/59.01 inference(scs_inference,[],[53,4523,4525,5558,5433,4341,4339,4373,4145,6396,6399,6402,6405,6408,1279,4141,445,1215,2172,54,56,139,155,333,62,69,381,99,61,83,49,72,73,74,75,84,85,42,90,1420])).
% 58.99/59.01 cnf(6438,plain,
% 58.99/59.01 (E(f3(f7(a2,a8,a9,a10),a10),a8)),
% 58.99/59.01 inference(scs_inference,[],[53,4523,4525,5558,5433,4341,4339,4373,4145,6396,6399,6402,6405,6408,1279,4141,445,1215,2172,54,56,139,155,333,62,69,381,99,61,83,49,72,73,74,75,84,85,42,90,1420,5862,5873,5864,5866,5869,5875,5104,5122,5867,5871,5870,5874,5868,5872,5436,1389,79,80,2])).
% 58.99/59.01 cnf(6475,plain,
% 58.99/59.01 (P4(f3(f7(a2,a10,a9,a8),a8),f7(a2,a10,a9,a8))),
% 58.99/59.01 inference(scs_inference,[],[2172,69])).
% 58.99/59.01 cnf(6479,plain,
% 58.99/59.01 (P4(a10,f7(a2,a10,a9,a8))),
% 58.99/59.01 inference(scs_inference,[],[6416,2172,69,101,100])).
% 58.99/59.01 cnf(6485,plain,
% 58.99/59.01 (P8(f7(a2,a10,a9,a8),a2)),
% 58.99/59.01 inference(scs_inference,[],[6416,6373,2172,69,101,100,333,62,102])).
% 58.99/59.01 cnf(6487,plain,
% 58.99/59.01 (~P1(a10,f7(a2,a8,a9,a10))),
% 58.99/59.01 inference(scs_inference,[],[6416,6385,6373,2172,69,101,100,333,62,102,61])).
% 58.99/59.01 cnf(6498,plain,
% 58.99/59.01 (~P4(f1(x64981),x64981)),
% 58.99/59.01 inference(rename_variables,[],[4145])).
% 58.99/59.01 cnf(6502,plain,
% 58.99/59.01 (~P4(f1(x65021),x65021)),
% 58.99/59.01 inference(rename_variables,[],[4145])).
% 58.99/59.01 cnf(6503,plain,
% 58.99/59.01 (P5(f16(a8,f7(a2,a10,a9,a8),f7(a2,a10,a9,a8)),f7(a2,a10,a9,a8))),
% 58.99/59.01 inference(scs_inference,[],[6416,6385,6387,6373,6438,4392,5433,4473,4339,4145,6498,4373,1279,4141,2172,69,101,100,333,62,102,61,75,74,73,49,72,35,42,91])).
% 58.99/59.01 cnf(6504,plain,
% 58.99/59.01 (~P7(x65041,x65042,x65042)),
% 58.99/59.01 inference(rename_variables,[],[5433])).
% 58.99/59.01 cnf(6507,plain,
% 58.99/59.01 (P5(f1(x65071),x65071)),
% 58.99/59.01 inference(rename_variables,[],[4373])).
% 58.99/59.01 cnf(6508,plain,
% 58.99/59.01 (P5(f1(x65081),f15(f1(x65081),x65081))),
% 58.99/59.01 inference(rename_variables,[],[6395])).
% 58.99/59.01 cnf(6514,plain,
% 58.99/59.01 (~P4(f16(a8,f7(a2,a10,a9,a8),f7(a2,a10,a9,a8)),f7(a2,a10,a9,a8))),
% 58.99/59.01 inference(scs_inference,[],[6416,6385,6387,6373,6395,6508,6438,4392,5433,6504,4473,4339,4145,6498,6502,4373,6507,1279,4141,2172,69,101,100,333,62,102,61,75,74,73,49,72,35,42,91,88,87,98])).
% 58.99/59.01 cnf(6519,plain,
% 58.99/59.01 (E(f3(f7(a2,a8,a9,a10),a8),a10)),
% 58.99/59.01 inference(scs_inference,[],[6416,6385,6387,6381,6373,6395,6508,6438,6379,4392,5433,6504,4473,4339,4145,6498,6502,4373,6507,1279,4141,108,1215,1385,2172,69,101,100,333,62,102,61,75,74,73,49,72,35,42,91,88,87,98,126,70])).
% 58.99/59.01 cnf(6523,plain,
% 58.99/59.01 (E(a10,f3(f7(a2,a8,a9,a10),a8))),
% 58.99/59.01 inference(scs_inference,[],[6416,6385,6387,6381,6373,6395,6508,6438,6379,4392,5433,6504,4473,4339,4145,6498,6502,4373,6507,1279,4141,108,1215,1385,2172,69,101,100,333,62,102,61,75,74,73,49,72,35,42,91,88,87,98,126,70,4608,2177,2])).
% 58.99/59.01 cnf(6534,plain,
% 58.99/59.01 (P4(f3(f7(a2,a10,a9,a8),a10),f7(a2,a10,a9,a8))),
% 58.99/59.01 inference(scs_inference,[],[6479,69])).
% 58.99/59.01 cnf(6536,plain,
% 58.99/59.01 (~E(f3(f7(a2,a10,a9,a8),a10),a10)),
% 58.99/59.01 inference(scs_inference,[],[6479,69,62])).
% 58.99/59.01 cnf(6538,plain,
% 58.99/59.01 (~P1(a10,f7(a2,a10,a9,a8))),
% 58.99/59.01 inference(scs_inference,[],[6479,69,62,61])).
% 58.99/59.01 cnf(6546,plain,
% 58.99/59.01 (P1(f16(a8,f7(a2,a10,a9,a8),f7(a2,a10,a9,a8)),f7(a2,a10,a9,a8))),
% 58.99/59.01 inference(scs_inference,[],[6479,6514,6503,6519,5454,107,4145,69,62,61,38,49,43,63])).
% 58.99/59.01 cnf(6549,plain,
% 58.99/59.01 (~E(a9,a10)),
% 58.99/59.01 inference(scs_inference,[],[6479,6487,6514,6503,6519,5454,107,4145,1279,69,62,61,38,49,43,63,42,35])).
% 58.99/59.01 cnf(6556,plain,
% 58.99/59.01 (~P5(a10,a2)),
% 58.99/59.01 inference(scs_inference,[],[6549,4533])).
% 58.99/59.01 cnf(6570,plain,
% 58.99/59.01 (~P5(a10,f18(a2,a2))),
% 58.99/59.01 inference(scs_inference,[],[6556,6534,6398,6523,52,4481,59,60,61,66,36,105])).
% 58.99/59.01 cnf(6572,plain,
% 58.99/59.01 (~P5(f3(f7(a2,a8,a9,a10),a8),a2)),
% 58.99/59.01 inference(scs_inference,[],[6556,6534,6398,6523,6519,52,4481,59,60,61,66,36,105,45])).
% 58.99/59.01 cnf(6579,plain,
% 58.99/59.01 (E(f3(f7(a2,a10,a9,a8),a10),a8)),
% 58.99/59.01 inference(scs_inference,[],[6556,6538,6546,6534,6398,6536,6369,6523,6519,6385,6479,4141,108,52,2172,4481,59,60,61,66,36,105,45,43,42,35,70,4778,2])).
% 58.99/59.01 cnf(6603,plain,
% 58.99/59.01 (~P5(f3(f7(a2,a8,a9,a10),a8),f7(a2,a10,a9,a8))),
% 58.99/59.01 inference(scs_inference,[],[6570,6579,6572,6375,6485,4614,4589,4481,59,60,61,66])).
% 58.99/59.01 cnf(6631,plain,
% 58.99/59.01 (~P5(a10,f7(a2,a10,a9,a8))),
% 58.99/59.01 inference(scs_inference,[],[6603,6401,6475,6523,6556,59,60,61,66,45])).
% 58.99/59.01 cnf(6652,plain,
% 58.99/59.01 ($false),
% 58.99/59.02 inference(scs_inference,[],[6631,6479,59]),
% 58.99/59.02 ['proof']).
% 58.99/59.02 % SZS output end Proof
% 58.99/59.02 % Total time :58.330000s
%------------------------------------------------------------------------------