%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : SWV408+1 : TPTP v8.2.0. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar /export/starexec/sandbox2/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 16:47:07 EDT 2024
% Result : Theorem 58.76s 58.80s
% Output : CNFRefutation 58.83s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.06/0.12 % Problem : SWV408+1 : TPTP v8.2.0. Released v3.3.0.
% 0.06/0.12 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% 0.12/0.33 % Computer : n001.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 : Thu Jun 20 20:04:09 EDT 2024
% 0.12/0.33 % CPUTime :
% 0.44/0.57 start to proof:theBenchmark
% 58.76/58.78 %-------------------------------------------
% 58.76/58.78 % File :CSE---1.7
% 58.76/58.78 % Problem :theBenchmark
% 58.76/58.78 % Transform :cnf
% 58.76/58.78 % Format :tptp:raw
% 58.76/58.78 % Command :java -jar mcs_scs.jar %d %s
% 58.76/58.78
% 58.76/58.78 % Result :Theorem 58.160000s
% 58.76/58.78 % Output :CNFRefutation 58.160000s
% 58.76/58.78 %-------------------------------------------
% 58.76/58.79 %------------------------------------------------------------------------------
% 58.76/58.79 % File : SWV408+1 : TPTP v8.2.0. Released v3.3.0.
% 58.76/58.79 % Domain : Software Verification
% 58.76/58.79 % Problem : Priority queue checker: lemma_not_min_elem_pair
% 58.76/58.79 % Version : [dNP05] axioms.
% 58.76/58.79 % English :
% 58.76/58.79
% 58.76/58.79 % Refs : [Pis06] Piskac (2006), Email to Geoff Sutcliffe
% 58.76/58.79 % : [dNP05] de Nivelle & Piskac (2005), Verification of an Off-Lin
% 58.76/58.80 % Source : [Pis06]
% 58.76/58.80 % Names : cpq_l044 [Pis06]
% 58.76/58.80
% 58.76/58.80 % Status : Theorem
% 58.76/58.80 % Rating : 0.25 v8.2.0, 0.22 v8.1.0, 0.28 v7.5.0, 0.31 v7.4.0, 0.20 v7.3.0, 0.24 v7.2.0, 0.21 v7.1.0, 0.30 v6.4.0, 0.35 v6.3.0, 0.38 v6.2.0, 0.44 v6.1.0, 0.40 v6.0.0, 0.30 v5.5.0, 0.41 v5.4.0, 0.46 v5.3.0, 0.48 v5.2.0, 0.45 v5.1.0, 0.43 v5.0.0, 0.38 v4.1.0, 0.35 v4.0.1, 0.39 v4.0.0, 0.42 v3.7.0, 0.40 v3.5.0, 0.42 v3.3.0
% 58.76/58.80 % Syntax : Number of formulae : 43 ( 16 unt; 0 def)
% 58.76/58.80 % Number of atoms : 92 ( 29 equ)
% 58.76/58.80 % Maximal formula atoms : 5 ( 2 avg)
% 58.76/58.80 % Number of connectives : 62 ( 13 ~; 5 |; 16 &)
% 58.76/58.80 % ( 7 <=>; 21 =>; 0 <=; 0 <~>)
% 58.76/58.80 % Maximal formula depth : 9 ( 5 avg)
% 58.76/58.80 % Maximal term depth : 4 ( 1 avg)
% 58.76/58.80 % Number of predicates : 11 ( 9 usr; 1 prp; 0-3 aty)
% 58.76/58.80 % Number of functors : 18 ( 18 usr; 3 con; 0-3 aty)
% 58.76/58.80 % Number of variables : 126 ( 124 !; 2 ?)
% 58.76/58.80 % SPC : FOF_THM_RFO_SEQ
% 58.76/58.80
% 58.76/58.80 % Comments :
% 58.76/58.80 %------------------------------------------------------------------------------
% 58.76/58.80 %----Include the axioms about priority queues and checked priority queues
% 58.76/58.80 include('Axioms/SWV007+0.ax').
% 58.76/58.80 include('Axioms/SWV007+2.ax').
% 58.76/58.80 include('Axioms/SWV007+3.ax').
% 58.76/58.80 %------------------------------------------------------------------------------
% 58.76/58.80 %----lemma_contains_update (cpq_l045.p)
% 58.76/58.80 fof(l44_l45,lemma,
% 58.76/58.80 ! [U,V,W] :
% 58.76/58.80 ( ( contains_slb(U,V)
% 58.76/58.80 & strictly_less_than(V,W) )
% 58.76/58.80 => ( pair_in_list(update_slb(U,W),V,W)
% 58.76/58.80 | ? [X] :
% 58.76/58.80 ( pair_in_list(update_slb(U,W),V,X)
% 58.76/58.80 & less_than(W,X) ) ) ) ).
% 58.76/58.80
% 58.76/58.80 %----lemma_not_min_elem_pair (conjecture)
% 58.76/58.80 fof(l44_co,conjecture,
% 58.76/58.80 ! [U,V,W,X] :
% 58.76/58.80 ( ( contains_slb(V,X)
% 58.76/58.80 & strictly_less_than(X,findmin_cpq_res(triple(U,V,W))) )
% 58.76/58.80 => ( pair_in_list(update_slb(V,findmin_pqp_res(U)),X,findmin_pqp_res(U))
% 58.76/58.80 | ? [Y] :
% 58.76/58.80 ( pair_in_list(update_slb(V,findmin_pqp_res(U)),X,Y)
% 58.76/58.80 & less_than(findmin_pqp_res(U),Y) ) ) ) ).
% 58.76/58.80
% 58.76/58.80 %------------------------------------------------------------------------------
% 58.76/58.80 %-------------------------------------------
% 58.76/58.80 % Proof found
% 58.76/58.80 % SZS status Theorem for theBenchmark
% 58.76/58.80 % SZS output start Proof
% 58.79/58.81 %ClaNum:100(EqnAxiom:46)
% 58.79/58.81 %VarNum:327(SingletonVarNum:154)
% 58.79/58.81 %MaxLitNum:4
% 58.79/58.81 %MaxfuncDepth:3
% 58.79/58.81 %SharedTerms:15
% 58.79/58.81 %goalClause: 47 58 63 81
% 58.79/58.81 %singleGoalClaCount:3
% 58.79/58.81 [47]P1(a1,a7)
% 58.79/58.81 [60]~P5(a2)
% 58.79/58.81 [58]P7(a7,f12(f21(a5,a1,a8)))
% 58.79/58.81 [63]~P8(f9(a1,f16(a5)),a7,f16(a5))
% 58.79/58.81 [49]P4(a3,x491)
% 58.79/58.81 [50]P4(x501,x501)
% 58.79/58.81 [51]P6(x511,x511)
% 58.79/58.81 [61]~P1(a2,x611)
% 58.79/58.81 [48]E(f9(a2,x481),a2)
% 58.79/58.81 [62]~P8(a2,x621,x622)
% 58.79/58.81 [56]P2(f21(x561,a2,x562))
% 58.79/58.81 [64]~P9(f21(x641,x642,a4))
% 58.79/58.81 [55]E(f12(f21(x551,a2,x552)),a3)
% 58.79/58.81 [57]E(f13(f21(x571,a2,x572)),f21(x571,a2,a4))
% 58.79/58.81 [52]P5(f11(x521,f10(x522,x523)))
% 58.79/58.81 [53]E(f18(f11(x531,f10(x532,x533)),x532),x531)
% 58.79/58.81 [54]E(f17(f11(x541,f10(x542,x543)),x542),x543)
% 58.79/58.81 [59]E(f21(f14(x591,x592),f11(x593,f10(x592,a3)),x594),f15(f21(x591,x593,x594),x592))
% 58.79/58.81 [81]~P4(f16(a5),x811)+~P8(f9(a1,f16(a5)),a7,x811)
% 58.79/58.81 [65]P4(x652,x651)+P4(x651,x652)
% 58.79/58.81 [66]~P7(x661,x662)+P4(x661,x662)
% 58.79/58.81 [68]~P7(x682,x681)+~P4(x681,x682)
% 58.79/58.81 [67]~P6(x671,x672)+P6(x671,f13(x672))
% 58.79/58.81 [73]~P6(x731,x732)+P6(x731,f19(f13(x732),f12(x732)))
% 58.79/58.81 [71]~P6(x711,x712)+P6(x711,f15(x712,x713))
% 58.79/58.81 [72]~P6(x721,x722)+P6(x721,f19(x722,x723))
% 58.79/58.81 [75]E(x751,a4)+P9(f21(x752,x753,x751))
% 58.79/58.81 [77]E(x771,a2)+E(f12(f21(x772,x771,x773)),f16(x772))
% 58.79/58.81 [80]~P1(x802,x804)+P3(f21(x801,x802,x803),x804)
% 58.79/58.81 [87]P1(x871,x872)+~P3(f21(x873,x871,x874),x872)
% 58.79/58.81 [74]~E(x742,x744)+P1(f11(x741,f10(x742,x743)),x744)
% 58.79/58.81 [76]~P1(x761,x764)+P1(f11(x761,f10(x762,x763)),x764)
% 58.79/58.81 [86]P1(x862,x864)+E(f19(f21(x861,x862,x863),x864),f21(x861,x862,a4))
% 58.79/58.81 [83]~P4(x832,x834)+E(f11(f9(x831,x832),f10(x833,x834)),f9(f11(x831,f10(x833,x834)),x832))
% 58.79/58.81 [84]~P7(x843,x844)+E(f9(f11(x841,f10(x842,x843)),x844),f11(f9(x841,x844),f10(x842,x844)))
% 58.79/58.81 [88]~P8(x881,x884,x885)+P8(f11(x881,f10(x882,x883)),x884,x885)
% 58.79/58.81 [98]~P7(x981,x982)+~P2(f21(x983,f11(x984,f10(x981,x982)),x985))
% 58.79/58.81 [69]P7(x692,x691)+~P4(x692,x691)+P4(x691,x692)
% 58.79/58.81 [70]~P4(x701,x703)+P4(x701,x702)+~P4(x703,x702)
% 58.79/58.81 [89]P1(x891,f16(x892))+E(x891,a2)+E(f13(f21(x892,x891,x893)),f21(x892,f9(x891,f16(x892)),a4))
% 58.79/58.81 [82]E(x821,x822)+P1(x823,x822)+~P1(f11(x823,f10(x821,x824)),x822)
% 58.79/58.81 [93]~P1(x932,x934)+~P7(x934,f17(x932,x934))+E(f19(f21(x931,x932,x933),x934),f21(f20(x931,x934),f18(x932,x934),a4))
% 58.79/58.81 [94]~P1(x943,x942)+~P4(f17(x943,x942),x942)+E(f21(f20(x941,x942),f18(x943,x942),x944),f19(f21(x941,x943,x944),x942))
% 58.79/58.81 [78]~P1(x783,x782)+E(x781,x782)+E(f17(f11(x783,f10(x781,x784)),x782),f17(x783,x782))
% 58.79/58.81 [85]~P1(x853,x852)+E(x851,x852)+E(f18(f11(x853,f10(x851,x854)),x852),f11(f18(x853,x852),f10(x851,x854)))
% 58.79/58.81 [79]~E(x793,x795)+~E(x792,x794)+P8(f11(x791,f10(x792,x793)),x794,x795)
% 58.79/58.81 [91]E(x911,x912)+P8(x913,x914,x912)+~P8(f11(x913,f10(x915,x911)),x914,x912)
% 58.79/58.81 [92]E(x921,x922)+P8(x923,x922,x924)+~P8(f11(x923,f10(x921,x925)),x922,x924)
% 58.79/58.81 [99]~P4(x994,x993)+~P2(f21(x991,x992,x995))+P2(f21(x991,f11(x992,f10(x993,x994)),x995))
% 58.79/58.81 [100]~P4(x1004,x1005)+P2(f21(x1001,x1002,x1003))+~P2(f21(x1001,f11(x1002,f10(x1005,x1004)),x1003))
% 58.79/58.81 [90]~P7(x903,x901)+~P1(x902,x903)+P8(f9(x902,x901),x903,x901)+P4(x901,f6(x902,x903,x901))
% 58.79/58.81 [95]~P7(x953,x952)+~P1(x951,x953)+P8(f9(x951,x952),x953,f6(x951,x953,x952))+P8(f9(x951,x952),x953,x952)
% 58.79/58.81 [96]~P1(x961,f16(x962))+E(x961,a2)+~P7(f16(x962),f17(x961,f16(x962)))+E(f13(f21(x962,x961,x963)),f21(x962,f9(x961,f16(x962)),a4))
% 58.79/58.81 [97]~P1(x971,f16(x972))+E(x971,a2)+~P4(f17(x971,f16(x972)),f16(x972))+E(f21(x972,f9(x971,f16(x972)),x973),f13(f21(x972,x971,x973)))
% 58.79/58.81 %EqnAxiom
% 58.79/58.81 [1]E(x11,x11)
% 58.79/58.81 [2]E(x22,x21)+~E(x21,x22)
% 58.79/58.81 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 58.79/58.81 [4]~E(x41,x42)+E(f9(x41,x43),f9(x42,x43))
% 58.79/58.81 [5]~E(x51,x52)+E(f9(x53,x51),f9(x53,x52))
% 58.79/58.81 [6]~E(x61,x62)+E(f10(x61,x63),f10(x62,x63))
% 58.79/58.81 [7]~E(x71,x72)+E(f10(x73,x71),f10(x73,x72))
% 58.79/58.81 [8]~E(x81,x82)+E(f11(x81,x83),f11(x82,x83))
% 58.79/58.81 [9]~E(x91,x92)+E(f11(x93,x91),f11(x93,x92))
% 58.79/58.81 [10]~E(x101,x102)+E(f17(x101,x103),f17(x102,x103))
% 58.79/58.81 [11]~E(x111,x112)+E(f17(x113,x111),f17(x113,x112))
% 58.79/58.81 [12]~E(x121,x122)+E(f21(x121,x123,x124),f21(x122,x123,x124))
% 58.79/58.81 [13]~E(x131,x132)+E(f21(x133,x131,x134),f21(x133,x132,x134))
% 58.79/58.81 [14]~E(x141,x142)+E(f21(x143,x144,x141),f21(x143,x144,x142))
% 58.79/58.81 [15]~E(x151,x152)+E(f18(x151,x153),f18(x152,x153))
% 58.79/58.81 [16]~E(x161,x162)+E(f18(x163,x161),f18(x163,x162))
% 58.79/58.81 [17]~E(x171,x172)+E(f16(x171),f16(x172))
% 58.79/58.81 [18]~E(x181,x182)+E(f19(x181,x183),f19(x182,x183))
% 58.79/58.81 [19]~E(x191,x192)+E(f19(x193,x191),f19(x193,x192))
% 58.79/58.81 [20]~E(x201,x202)+E(f20(x201,x203),f20(x202,x203))
% 58.79/58.81 [21]~E(x211,x212)+E(f20(x213,x211),f20(x213,x212))
% 58.79/58.81 [22]~E(x221,x222)+E(f15(x221,x223),f15(x222,x223))
% 58.79/58.81 [23]~E(x231,x232)+E(f15(x233,x231),f15(x233,x232))
% 58.79/58.81 [24]~E(x241,x242)+E(f12(x241),f12(x242))
% 58.79/58.81 [25]~E(x251,x252)+E(f6(x251,x253,x254),f6(x252,x253,x254))
% 58.79/58.81 [26]~E(x261,x262)+E(f6(x263,x261,x264),f6(x263,x262,x264))
% 58.79/58.81 [27]~E(x271,x272)+E(f6(x273,x274,x271),f6(x273,x274,x272))
% 58.79/58.81 [28]~E(x281,x282)+E(f13(x281),f13(x282))
% 58.79/58.81 [29]~E(x291,x292)+E(f14(x291,x293),f14(x292,x293))
% 58.79/58.81 [30]~E(x301,x302)+E(f14(x303,x301),f14(x303,x302))
% 58.79/58.81 [31]P1(x312,x313)+~E(x311,x312)+~P1(x311,x313)
% 58.79/58.81 [32]P1(x323,x322)+~E(x321,x322)+~P1(x323,x321)
% 58.79/58.81 [33]P4(x332,x333)+~E(x331,x332)+~P4(x331,x333)
% 58.79/58.81 [34]P4(x343,x342)+~E(x341,x342)+~P4(x343,x341)
% 58.79/58.81 [35]P7(x352,x353)+~E(x351,x352)+~P7(x351,x353)
% 58.79/58.81 [36]P7(x363,x362)+~E(x361,x362)+~P7(x363,x361)
% 58.79/58.81 [37]P6(x372,x373)+~E(x371,x372)+~P6(x371,x373)
% 58.79/58.81 [38]P6(x383,x382)+~E(x381,x382)+~P6(x383,x381)
% 58.79/58.81 [39]~P5(x391)+P5(x392)+~E(x391,x392)
% 58.79/58.81 [40]~P2(x401)+P2(x402)+~E(x401,x402)
% 58.79/58.81 [41]~P9(x411)+P9(x412)+~E(x411,x412)
% 58.79/58.81 [42]P8(x422,x423,x424)+~E(x421,x422)+~P8(x421,x423,x424)
% 58.79/58.81 [43]P8(x433,x432,x434)+~E(x431,x432)+~P8(x433,x431,x434)
% 58.79/58.81 [44]P8(x443,x444,x442)+~E(x441,x442)+~P8(x443,x444,x441)
% 58.79/58.81 [45]P3(x452,x453)+~E(x451,x452)+~P3(x451,x453)
% 58.79/58.81 [46]P3(x463,x462)+~E(x461,x462)+~P3(x463,x461)
% 58.79/58.81
% 58.79/58.81 %-------------------------------------------
% 58.83/58.82 cnf(101,plain,
% 58.83/58.82 (P1(f11(x1012,f10(x1011,x1013)),x1011)),
% 58.83/58.82 inference(equality_inference,[],[74])).
% 58.83/58.82 cnf(102,plain,
% 58.83/58.83 (~P7(x1021,x1021)),
% 58.83/58.83 inference(scs_inference,[],[50,68])).
% 58.83/58.83 cnf(104,plain,
% 58.83/58.83 (E(a2,f9(a2,x1041))),
% 58.83/58.83 inference(scs_inference,[],[50,48,68,2])).
% 58.83/58.83 cnf(105,plain,
% 58.83/58.83 (~E(a1,a2)),
% 58.83/58.83 inference(scs_inference,[],[47,50,61,48,68,2,31])).
% 58.83/58.83 cnf(107,plain,
% 58.83/58.83 (P1(f11(x1071,f10(f9(a2,x1072),x1073)),a2)),
% 58.83/58.83 inference(scs_inference,[],[47,50,101,61,48,68,2,31,32])).
% 58.83/58.83 cnf(109,plain,
% 58.83/58.83 (P4(a2,f9(a2,x1091))),
% 58.83/58.83 inference(scs_inference,[],[47,50,101,61,48,68,2,31,32,33])).
% 58.83/58.83 cnf(110,plain,
% 58.83/58.83 (P4(x1101,x1101)),
% 58.83/58.83 inference(rename_variables,[],[50])).
% 58.83/58.83 cnf(111,plain,
% 58.83/58.83 (P4(f9(a2,x1111),a2)),
% 58.83/58.83 inference(scs_inference,[],[47,50,110,101,61,48,68,2,31,32,33,34])).
% 58.83/58.83 cnf(113,plain,
% 58.83/58.83 (~E(a1,f9(a2,x1131))),
% 58.83/58.83 inference(scs_inference,[],[47,50,110,101,61,48,68,2,31,32,33,34,3])).
% 58.83/58.83 cnf(114,plain,
% 58.83/58.83 (P6(a2,f9(a2,x1141))),
% 58.83/58.83 inference(scs_inference,[],[47,50,110,101,51,61,48,68,2,31,32,33,34,3,37])).
% 58.83/58.83 cnf(115,plain,
% 58.83/58.83 (P6(x1151,x1151)),
% 58.83/58.83 inference(rename_variables,[],[51])).
% 58.83/58.83 cnf(116,plain,
% 58.83/58.83 (P6(f9(a2,x1161),a2)),
% 58.83/58.83 inference(scs_inference,[],[47,50,110,101,51,115,61,48,68,2,31,32,33,34,3,37,38])).
% 58.83/58.83 cnf(119,plain,
% 58.83/58.83 (~P9(f13(f21(x1191,a2,x1192)))),
% 58.83/58.83 inference(scs_inference,[],[47,50,110,101,51,115,61,60,48,64,57,68,2,31,32,33,34,3,37,38,39,41])).
% 58.83/58.83 cnf(124,plain,
% 58.83/58.83 (P7(x1241,f12(f21(a5,a1,a8)))+~E(a7,x1241)),
% 58.83/58.83 inference(scs_inference,[],[47,58,50,110,101,51,115,49,61,60,48,64,57,68,2,31,32,33,34,3,37,38,39,41,69,35])).
% 58.83/58.83 cnf(125,plain,
% 58.83/58.83 (P7(a7,x1251)+~E(f12(f21(a5,a1,a8)),x1251)),
% 58.83/58.83 inference(scs_inference,[],[47,58,50,110,101,51,115,49,61,60,48,64,57,68,2,31,32,33,34,3,37,38,39,41,69,35,36])).
% 58.83/58.83 cnf(129,plain,
% 58.83/58.83 (~E(f12(f21(a5,a1,a8)),a7)),
% 58.83/58.83 inference(scs_inference,[],[102,125])).
% 58.83/58.83 cnf(131,plain,
% 58.83/58.83 (E(x1311,f18(f11(x1311,f10(x1312,x1313)),x1312))),
% 58.83/58.83 inference(scs_inference,[],[102,53,125,2])).
% 58.83/58.83 cnf(134,plain,
% 58.83/58.83 (P4(f9(a2,x1341),f9(a2,x1342))),
% 58.83/58.83 inference(scs_inference,[],[102,109,111,53,125,2,68,70])).
% 58.83/58.83 cnf(136,plain,
% 58.83/58.83 (P4(f18(f11(a3,f10(x1361,x1362)),x1361),x1363)),
% 58.83/58.83 inference(scs_inference,[],[102,109,111,53,49,125,2,68,70,33])).
% 58.83/58.83 cnf(137,plain,
% 58.83/58.83 (~E(f11(x1371,f10(f9(a2,x1372),x1373)),a2)),
% 58.83/58.83 inference(scs_inference,[],[102,107,109,111,53,49,61,125,2,68,70,33,31])).
% 58.83/58.83 cnf(153,plain,
% 58.83/58.83 (E(x1531,f18(f11(x1531,f10(x1532,x1533)),x1532))),
% 58.83/58.83 inference(rename_variables,[],[131])).
% 58.83/58.83 cnf(156,plain,
% 58.83/58.83 (E(f15(f21(x1561,x1562,x1563),x1564),f21(f14(x1561,x1564),f11(x1562,f10(x1564,a3)),x1563))),
% 58.83/58.83 inference(scs_inference,[],[111,131,59,124,68,2])).
% 58.83/58.83 cnf(158,plain,
% 58.83/58.83 (~P7(x1581,x1581)),
% 58.83/58.83 inference(rename_variables,[],[102])).
% 58.83/58.83 cnf(159,plain,
% 58.83/58.83 (P4(f18(f11(f9(a2,x1591),f10(x1592,x1593)),x1592),a2)),
% 58.83/58.83 inference(scs_inference,[],[111,102,131,153,59,124,68,2,36,33])).
% 58.83/58.83 cnf(160,plain,
% 58.83/58.83 (E(x1601,f18(f11(x1601,f10(x1602,x1603)),x1602))),
% 58.83/58.83 inference(rename_variables,[],[131])).
% 58.83/58.83 cnf(161,plain,
% 58.83/58.83 (P4(a2,f18(f11(f9(a2,x1611),f10(x1612,x1613)),x1612))),
% 58.83/58.83 inference(scs_inference,[],[109,111,102,131,153,160,59,124,68,2,36,33,34])).
% 58.83/58.83 cnf(162,plain,
% 58.83/58.83 (E(x1621,f18(f11(x1621,f10(x1622,x1623)),x1622))),
% 58.83/58.83 inference(rename_variables,[],[131])).
% 58.83/58.83 cnf(163,plain,
% 58.83/58.83 (P6(f18(f11(f9(a2,x1631),f10(x1632,x1633)),x1632),a2)),
% 58.83/58.83 inference(scs_inference,[],[109,111,102,116,131,153,160,162,59,124,68,2,36,33,34,37])).
% 58.83/58.83 cnf(164,plain,
% 58.83/58.83 (E(x1641,f18(f11(x1641,f10(x1642,x1643)),x1642))),
% 58.83/58.83 inference(rename_variables,[],[131])).
% 58.83/58.83 cnf(167,plain,
% 58.83/58.83 (P6(a2,f18(f11(f9(a2,x1671),f10(x1672,x1673)),x1672))),
% 58.83/58.83 inference(scs_inference,[],[109,111,102,114,116,131,153,160,162,164,119,59,53,124,68,2,36,33,34,37,41,38])).
% 58.83/58.83 cnf(168,plain,
% 58.83/58.83 (E(x1681,f18(f11(x1681,f10(x1682,x1683)),x1682))),
% 58.83/58.83 inference(rename_variables,[],[131])).
% 58.83/58.83 cnf(170,plain,
% 58.83/58.83 (E(x1701,f18(f11(x1701,f10(x1702,x1703)),x1702))),
% 58.83/58.83 inference(rename_variables,[],[131])).
% 58.83/58.83 cnf(172,plain,
% 58.83/58.83 (E(x1721,f18(f11(x1721,f10(x1722,x1723)),x1722))),
% 58.83/58.83 inference(rename_variables,[],[131])).
% 58.83/58.83 cnf(173,plain,
% 58.83/58.83 (~E(f11(x1731,f10(x1732,x1733)),a2)),
% 58.83/58.83 inference(scs_inference,[],[47,109,111,102,114,116,131,153,160,162,164,168,170,119,101,56,59,61,53,124,68,2,36,33,34,37,41,38,32,40,31])).
% 58.83/58.83 cnf(176,plain,
% 58.83/58.83 (P5(f18(f11(f11(x1761,f10(x1762,x1763)),f10(x1764,x1765)),x1764))),
% 58.83/58.83 inference(scs_inference,[],[47,109,111,137,102,114,116,131,153,160,162,164,168,170,172,119,101,48,56,59,52,61,53,124,68,2,36,33,34,37,41,38,32,40,31,3,39])).
% 58.83/58.83 cnf(180,plain,
% 58.83/58.83 (P4(f9(a2,x1801),f18(f11(f9(a2,x1802),f10(x1803,x1804)),x1803))),
% 58.83/58.83 inference(scs_inference,[],[47,109,111,137,102,158,114,116,131,153,160,162,164,168,170,172,119,101,48,56,59,52,61,53,124,68,2,36,33,34,37,41,38,32,40,31,3,39,35,70])).
% 58.83/58.83 cnf(186,plain,
% 58.83/58.83 (E(a3,f12(f21(x1861,a2,x1862)))),
% 58.83/58.83 inference(scs_inference,[],[136,55,68,2])).
% 58.83/58.83 cnf(193,plain,
% 58.83/58.83 (P1(f11(x1931,f10(a2,x1932)),f9(a2,x1933))),
% 58.83/58.83 inference(scs_inference,[],[136,159,104,156,163,167,101,55,64,68,2,37,38,34,41,32])).
% 58.83/58.83 cnf(196,plain,
% 58.83/58.83 (~E(f12(f21(a5,a1,a8)),f18(f11(a3,f10(x1961,x1962)),x1961))),
% 58.83/58.83 inference(scs_inference,[],[136,173,159,104,156,163,167,101,48,55,64,68,2,37,38,34,41,32,3,125])).
% 58.83/58.83 cnf(204,plain,
% 58.83/58.83 (E(f21(x2041,a2,a4),f13(f21(x2041,a2,x2042)))),
% 58.83/58.83 inference(scs_inference,[],[180,57,68,2])).
% 58.83/58.83 cnf(207,plain,
% 58.83/58.83 (E(f18(f11(a3,f10(x2071,x2072)),x2071),f12(f21(x2073,a2,x2074)))),
% 58.83/58.83 inference(scs_inference,[],[180,186,53,56,57,68,2,40,3])).
% 58.83/58.83 cnf(213,plain,
% 58.83/58.83 (E(f12(f21(x2131,a2,x2132)),f18(f11(a3,f10(x2133,x2134)),x2133))),
% 58.83/58.83 inference(scs_inference,[],[161,207,68,2])).
% 58.83/58.83 cnf(214,plain,
% 58.83/58.83 (E(f18(f11(f21(x2141,a2,a4),f10(x2142,x2143)),x2142),f13(f21(x2141,a2,x2144)))),
% 58.83/58.83 inference(scs_inference,[],[161,207,204,53,68,2,3])).
% 58.83/58.83 cnf(221,plain,
% 58.83/58.83 (E(f13(f21(x2211,a2,x2212)),f18(f11(f21(x2211,a2,a4),f10(x2213,x2214)),x2213))),
% 58.83/58.83 inference(scs_inference,[],[134,214,68,2])).
% 58.83/58.83 cnf(222,plain,
% 58.83/58.83 (~E(f12(f21(a5,a1,a8)),f12(f21(x2221,a2,x2222)))),
% 58.83/58.83 inference(scs_inference,[],[134,196,214,213,68,2,3])).
% 58.83/58.83 cnf(224,plain,
% 58.83/58.83 (~E(f21(a5,a1,a8),f21(x2241,a2,x2242))),
% 58.83/58.83 inference(scs_inference,[],[134,196,214,213,68,2,3,24])).
% 58.83/58.83 cnf(228,plain,
% 58.83/58.83 (E(x2281,f17(f11(x2282,f10(x2283,x2281)),x2283))),
% 58.83/58.83 inference(scs_inference,[],[54,2])).
% 58.83/58.83 cnf(233,plain,
% 58.83/58.83 (P7(f17(f11(x2331,f10(x2332,a7)),x2332),f12(f21(a5,a1,a8)))),
% 58.83/58.83 inference(scs_inference,[],[159,222,186,54,2,68,3,124])).
% 58.83/58.83 cnf(277,plain,
% 58.83/58.83 (P4(a7,f12(f21(a5,a1,a8)))),
% 58.83/58.83 inference(scs_inference,[],[58,65,68])).
% 58.83/58.83 cnf(280,plain,
% 58.83/58.83 (P4(f18(f11(a7,f10(x2801,x2802)),x2801),f12(f21(a5,a1,a8)))),
% 58.83/58.83 inference(scs_inference,[],[277,131,68,33])).
% 58.83/58.83 cnf(281,plain,
% 58.83/58.83 (E(x2811,f18(f11(x2811,f10(x2812,x2813)),x2812))),
% 58.83/58.83 inference(rename_variables,[],[131])).
% 58.83/58.83 cnf(282,plain,
% 58.83/58.83 (P4(a7,f18(f11(f12(f21(a5,a1,a8)),f10(x2821,x2822)),x2821))),
% 58.83/58.83 inference(scs_inference,[],[277,131,281,68,33,34])).
% 58.83/58.83 cnf(291,plain,
% 58.83/58.83 (P4(f12(f21(x2911,a2,x2912)),x2913)),
% 58.83/58.83 inference(scs_inference,[],[136,282,207,68,33])).
% 58.83/58.83 cnf(296,plain,
% 58.83/58.83 (P4(f17(f11(x2961,f10(x2962,a7)),x2962),f12(f21(a5,a1,a8)))),
% 58.83/58.83 inference(scs_inference,[],[277,228,33])).
% 58.83/58.83 cnf(308,plain,
% 58.83/58.83 (E(f16(f9(a2,x3081)),f16(a2))),
% 58.83/58.83 inference(scs_inference,[],[104,17,2])).
% 58.83/58.83 cnf(309,plain,
% 58.83/58.83 (E(f16(a2),f16(f9(a2,x3091)))),
% 58.83/58.83 inference(scs_inference,[],[308,2])).
% 58.83/58.83 cnf(323,plain,
% 58.83/58.83 (P8(f11(x3231,f10(a4,a4)),a4,a4)),
% 58.83/58.83 inference(scs_inference,[],[64,75,79])).
% 58.83/58.83 cnf(324,plain,
% 58.83/58.83 (P8(f11(x3241,f10(a4,a4)),f17(f11(x3242,f10(x3243,a4)),x3243),a4)),
% 58.83/58.83 inference(scs_inference,[],[228,323,43])).
% 58.83/58.83 cnf(355,plain,
% 58.83/58.83 (P6(f18(f11(x3551,f10(x3552,x3553)),x3552),x3551)),
% 58.83/58.83 inference(scs_inference,[],[53,51,38])).
% 58.83/58.83 cnf(356,plain,
% 58.83/58.83 (P6(x3561,x3561)),
% 58.83/58.83 inference(rename_variables,[],[51])).
% 58.83/58.83 cnf(357,plain,
% 58.83/58.83 (P4(f18(f11(x3571,f10(x3572,x3573)),x3572),x3571)),
% 58.83/58.83 inference(scs_inference,[],[53,50,51,38,34])).
% 58.83/58.83 cnf(358,plain,
% 58.83/58.83 (P4(x3581,x3581)),
% 58.83/58.83 inference(rename_variables,[],[50])).
% 58.83/58.83 cnf(359,plain,
% 58.83/58.83 (P4(x3591,f18(f11(x3591,f10(x3592,x3593)),x3592))),
% 58.83/58.83 inference(scs_inference,[],[53,50,358,51,38,34,33])).
% 58.83/58.83 cnf(361,plain,
% 58.83/58.83 (P6(x3611,f18(f11(x3611,f10(x3612,x3613)),x3612))),
% 58.83/58.83 inference(scs_inference,[],[53,50,358,51,356,38,34,33,37])).
% 58.83/58.83 cnf(372,plain,
% 58.83/58.83 (E(f18(f11(f16(f9(a2,x3721)),f10(x3722,x3723)),x3722),f16(a2))),
% 58.83/58.83 inference(scs_inference,[],[53,357,308,68,3])).
% 58.83/58.83 cnf(374,plain,
% 58.83/58.83 (E(f16(a2),f18(f11(f16(f9(a2,x3741)),f10(x3742,x3743)),x3742))),
% 58.83/58.83 inference(scs_inference,[],[53,357,308,68,3,2])).
% 58.83/58.83 cnf(446,plain,
% 58.83/58.83 (P4(f17(f11(x4461,f10(x4462,x4463)),x4462),x4463)),
% 58.83/58.83 inference(scs_inference,[],[54,50,34])).
% 58.83/58.83 cnf(447,plain,
% 58.83/58.83 (P4(x4471,x4471)),
% 58.83/58.83 inference(rename_variables,[],[50])).
% 58.83/58.83 cnf(450,plain,
% 58.83/58.83 (P4(x4501,f17(f11(x4502,f10(x4503,x4501)),x4503))),
% 58.83/58.83 inference(scs_inference,[],[54,50,447,207,361,34,38,33])).
% 58.83/58.83 cnf(467,plain,
% 58.83/58.83 (P6(f17(f11(x4671,f10(x4672,x4673)),x4672),x4673)),
% 58.83/58.83 inference(scs_inference,[],[54,51,38])).
% 58.83/58.83 cnf(490,plain,
% 58.83/58.83 (P4(f21(x4901,a2,a4),f13(f21(x4901,a2,x4902)))),
% 58.83/58.83 inference(scs_inference,[],[57,50,33])).
% 58.83/58.83 cnf(491,plain,
% 58.83/58.83 (P4(x4911,x4911)),
% 58.83/58.83 inference(rename_variables,[],[50])).
% 58.83/58.83 cnf(492,plain,
% 58.83/58.83 (P4(f13(f21(x4921,a2,x4922)),f21(x4921,a2,a4))),
% 58.83/58.83 inference(scs_inference,[],[57,50,491,33,34])).
% 58.83/58.83 cnf(503,plain,
% 58.83/58.83 (P4(f21(x5031,a2,a4),f18(f11(f13(f21(x5031,a2,x5032)),f10(x5033,x5034)),x5033))),
% 58.83/58.83 inference(scs_inference,[],[57,359,492,68,33])).
% 58.83/58.83 cnf(505,plain,
% 58.83/58.83 (P4(f18(f11(f13(f21(x5051,a2,x5052)),f10(x5053,x5054)),x5053),f21(x5051,a2,a4))),
% 58.83/58.83 inference(scs_inference,[],[57,359,357,492,68,33,34])).
% 58.83/58.83 cnf(516,plain,
% 58.83/58.83 (P4(f18(f11(f13(f21(x5161,a2,x5162)),f10(x5163,x5164)),x5163),f13(f21(x5161,a2,x5165)))),
% 58.83/58.83 inference(scs_inference,[],[505,503,204,68,33,34])).
% 58.83/58.83 cnf(522,plain,
% 58.83/58.83 (~P3(f21(x5221,f9(a2,x5222),x5223),x5224)),
% 58.83/58.83 inference(scs_inference,[],[61,48,87,31])).
% 58.83/58.83 cnf(523,plain,
% 58.83/58.83 (~P1(f9(a2,x5231),x5232)),
% 58.83/58.83 inference(scs_inference,[],[522,80])).
% 58.83/58.83 cnf(527,plain,
% 58.83/58.83 (P4(f13(f21(x5271,a2,x5272)),f13(f21(x5271,a2,x5273)))),
% 58.83/58.83 inference(scs_inference,[],[516,490,204,522,80,68,33])).
% 58.83/58.83 cnf(531,plain,
% 58.83/58.83 (E(f9(x5311,f21(x5312,a2,a4)),f9(x5311,f13(f21(x5312,a2,x5313))))),
% 58.83/58.83 inference(scs_inference,[],[57,5,2])).
% 58.83/58.83 cnf(547,plain,
% 58.83/58.83 (P4(f21(f14(x5471,x5472),f11(x5473,f10(x5472,a3)),x5474),f15(f21(x5471,x5473,x5474),x5472))),
% 58.83/58.83 inference(scs_inference,[],[59,50,34])).
% 58.83/58.83 cnf(559,plain,
% 58.83/58.83 (P4(f13(f21(x5591,a2,x5592)),f13(f21(x5591,a2,x5593)))),
% 58.83/58.83 inference(rename_variables,[],[527])).
% 58.83/58.83 cnf(560,plain,
% 58.83/58.83 (P4(f18(f11(f21(x5601,a2,a4),f10(x5602,x5603)),x5602),f13(f21(x5601,a2,x5604)))),
% 58.83/58.83 inference(scs_inference,[],[527,559,547,221,68,34,33])).
% 58.83/58.83 cnf(562,plain,
% 58.83/58.83 (P6(f21(f14(x5621,x5622),f11(x5623,f10(x5622,a3)),x5624),f15(f21(x5621,x5623,x5624),x5622))),
% 58.83/58.83 inference(scs_inference,[],[59,527,559,547,221,51,68,34,33,38])).
% 58.83/58.83 cnf(563,plain,
% 58.83/58.83 (P6(x5631,x5631)),
% 58.83/58.83 inference(rename_variables,[],[51])).
% 58.83/58.83 cnf(564,plain,
% 58.83/58.83 (P6(f15(f21(x5641,x5642,x5643),x5644),f21(f14(x5641,x5644),f11(x5642,f10(x5644,a3)),x5643))),
% 58.83/58.83 inference(scs_inference,[],[59,527,559,547,221,51,563,68,34,33,38,37])).
% 58.83/58.83 cnf(590,plain,
% 58.83/58.83 (P4(f9(a2,x5901),f18(f11(a2,f10(x5902,x5903)),x5902))),
% 58.83/58.83 inference(scs_inference,[],[104,359,357,34,33])).
% 58.83/58.83 cnf(605,plain,
% 58.83/58.83 (P6(f17(f11(x6051,f10(x6052,a2)),x6052),f9(a2,x6053))),
% 58.83/58.83 inference(scs_inference,[],[104,450,590,446,467,68,34,33,38])).
% 58.83/58.83 cnf(611,plain,
% 58.83/58.83 (E(f12(f21(x6111,a1,x6112)),f16(x6111))),
% 58.83/58.83 inference(scs_inference,[],[224,77,13])).
% 58.83/58.83 cnf(612,plain,
% 58.83/58.83 (E(f16(x6121),f12(f21(x6121,a1,x6122)))),
% 58.83/58.83 inference(scs_inference,[],[611,2])).
% 58.83/58.83 cnf(681,plain,
% 58.83/58.83 (~E(a1,f18(f11(f9(a2,x6811),f10(x6812,x6813)),x6812))),
% 58.83/58.83 inference(scs_inference,[],[113,53,3])).
% 58.83/58.83 cnf(683,plain,
% 58.83/58.83 (~P8(f9(a1,f16(a5)),a7,f17(f11(x6831,f10(x6832,f16(a5))),x6832))),
% 58.83/58.83 inference(scs_inference,[],[50,228,81,34])).
% 58.83/58.83 cnf(689,plain,
% 58.83/58.83 (P8(f11(x6891,f10(a4,a4)),a4,f18(f11(a4,f10(x6892,x6893)),x6892))),
% 58.83/58.83 inference(scs_inference,[],[131,323,44])).
% 58.83/58.83 cnf(690,plain,
% 58.83/58.83 (E(x6901,f18(f11(x6901,f10(x6902,x6903)),x6902))),
% 58.83/58.83 inference(rename_variables,[],[131])).
% 58.83/58.83 cnf(691,plain,
% 58.83/58.83 (P8(f11(x6911,f10(a4,a4)),f18(f11(a4,f10(x6912,x6913)),x6912),a4)),
% 58.83/58.83 inference(scs_inference,[],[131,690,323,44,43])).
% 58.83/58.83 cnf(692,plain,
% 58.83/58.83 (E(x6921,f18(f11(x6921,f10(x6922,x6923)),x6922))),
% 58.83/58.83 inference(rename_variables,[],[131])).
% 58.83/58.83 cnf(694,plain,
% 58.83/58.83 (E(x6941,f18(f11(x6941,f10(x6942,x6943)),x6942))),
% 58.83/58.83 inference(rename_variables,[],[131])).
% 58.83/58.83 cnf(695,plain,
% 58.83/58.83 (P1(f11(x6951,f10(a2,x6952)),f18(f11(f9(a2,x6953),f10(x6954,x6955)),x6954))),
% 58.83/58.83 inference(scs_inference,[],[131,690,692,694,193,291,323,44,43,33,32])).
% 58.83/58.83 cnf(697,plain,
% 58.83/58.83 (~P7(x6971,f18(f11(f12(f21(x6972,a2,x6973)),f10(x6974,x6975)),x6974))),
% 58.83/58.83 inference(scs_inference,[],[131,690,692,694,193,291,323,44,43,33,32,68])).
% 58.83/58.83 cnf(699,plain,
% 58.83/58.83 (E(a2,f18(f11(f9(a2,x6991),f10(x6992,x6993)),x6992))),
% 58.83/58.83 inference(scs_inference,[],[131,690,692,694,523,193,291,323,44,43,33,32,68,82])).
% 58.83/58.83 cnf(713,plain,
% 58.83/58.83 (E(f18(f11(f9(a2,x7131),f10(x7132,x7133)),x7132),a2)),
% 58.83/58.83 inference(scs_inference,[],[697,699,125,2])).
% 58.83/58.83 cnf(714,plain,
% 58.83/58.83 (P1(f11(x7141,f10(x7142,x7143)),f18(f11(x7142,f10(x7144,x7145)),x7144))),
% 58.83/58.83 inference(scs_inference,[],[131,697,101,699,125,2,32])).
% 58.83/58.83 cnf(740,plain,
% 58.83/58.83 (E(f19(f21(x7401,f9(a2,x7402),x7403),x7404),f21(x7401,f9(a2,x7402),a4))),
% 58.83/58.83 inference(scs_inference,[],[522,86,80])).
% 58.83/58.83 cnf(813,plain,
% 58.83/58.83 (P4(x8131,x8131)),
% 58.83/58.83 inference(rename_variables,[],[50])).
% 58.83/58.83 cnf(814,plain,
% 58.83/58.83 (P6(f18(f11(f16(f9(a2,x8141)),f10(x8142,x8143)),x8142),f16(a2))),
% 58.83/58.83 inference(scs_inference,[],[308,50,355,34,38])).
% 58.83/58.83 cnf(816,plain,
% 58.83/58.83 (P4(f16(a2),f16(f9(a2,x8161)))),
% 58.83/58.83 inference(scs_inference,[],[308,50,813,355,34,38,33])).
% 58.83/58.83 cnf(818,plain,
% 58.83/58.83 (P6(f16(a2),f18(f11(f16(f9(a2,x8181)),f10(x8182,x8183)),x8182))),
% 58.83/58.83 inference(scs_inference,[],[308,50,813,361,355,34,38,33,37])).
% 58.83/58.83 cnf(825,plain,
% 58.83/58.83 (P4(f18(f11(f16(f9(a2,x8251)),f10(x8252,x8253)),x8252),f16(a2))),
% 58.83/58.83 inference(scs_inference,[],[308,357,816,68,34])).
% 58.83/58.83 cnf(827,plain,
% 58.83/58.83 (P6(f18(f11(f16(f9(a2,x8271)),f10(x8272,x8273)),x8272),f16(f9(a2,x8274)))),
% 58.83/58.83 inference(scs_inference,[],[308,357,816,309,814,68,34,38])).
% 58.83/58.83 cnf(828,plain,
% 58.83/58.83 (P4(f16(a2),f18(f11(f16(f9(a2,x8281)),f10(x8282,x8283)),x8282))),
% 58.83/58.83 inference(scs_inference,[],[308,359,357,816,309,814,68,34,38,33])).
% 58.83/58.83 cnf(830,plain,
% 58.83/58.83 (P6(f16(f9(a2,x8301)),f18(f11(f16(f9(a2,x8302)),f10(x8303,x8304)),x8303))),
% 58.83/58.83 inference(scs_inference,[],[308,359,357,816,309,814,818,68,34,38,33,37])).
% 58.83/58.83 cnf(835,plain,
% 58.83/58.83 (P6(f16(f9(a2,x8351)),f16(a2))),
% 58.83/58.83 inference(scs_inference,[],[825,309,372,830,68,34,38])).
% 58.83/58.83 cnf(838,plain,
% 58.83/58.83 (P6(f16(a2),f16(f9(a2,x8381)))),
% 58.83/58.83 inference(scs_inference,[],[825,828,309,372,827,830,68,34,38,33,37])).
% 58.83/58.83 cnf(888,plain,
% 58.83/58.83 (~E(f21(x8881,a1,x8882),f21(x8883,f9(a2,x8884),x8885))),
% 58.83/58.83 inference(scs_inference,[],[522,47,45,80])).
% 58.83/58.83 cnf(889,plain,
% 58.83/58.83 (~E(f21(x8891,a1,x8892),f19(f21(x8893,f9(a2,x8894),x8895),x8896))),
% 58.83/58.83 inference(scs_inference,[],[740,888,3])).
% 58.83/58.83 cnf(892,plain,
% 58.83/58.83 (~P3(f19(f21(x8921,f9(a2,x8922),x8923),x8924),f12(f21(x8925,a2,x8926)))),
% 58.83/58.83 inference(scs_inference,[],[522,213,740,46,45])).
% 58.83/58.83 cnf(894,plain,
% 58.83/58.83 (E(f12(f21(x8941,a2,x8942)),f12(f21(x8943,a2,x8944)))),
% 58.83/58.83 inference(scs_inference,[],[213,207,3])).
% 58.83/58.83 cnf(899,plain,
% 58.83/58.83 (E(f18(f11(f9(a2,x8991),f10(x8992,x8993)),x8992),f9(a2,x8994))),
% 58.83/58.83 inference(scs_inference,[],[104,713,3])).
% 58.83/58.83 cnf(900,plain,
% 58.83/58.83 (E(f9(a2,x9001),f18(f11(f9(a2,x9002),f10(x9003,x9004)),x9003))),
% 58.83/58.83 inference(scs_inference,[],[104,713,3,2])).
% 58.83/58.83 cnf(903,plain,
% 58.83/58.83 (E(f16(a2),f12(f21(f9(a2,x9031),a1,x9032)))),
% 58.83/58.83 inference(scs_inference,[],[309,612,3])).
% 58.83/58.83 cnf(927,plain,
% 58.83/58.83 (P4(x9271,x9271)),
% 58.83/58.83 inference(rename_variables,[],[50])).
% 58.83/58.83 cnf(931,plain,
% 58.83/58.83 (P6(x9311,x9311)),
% 58.83/58.83 inference(rename_variables,[],[51])).
% 58.83/58.83 cnf(932,plain,
% 58.83/58.83 (P6(f9(x9321,f13(f21(x9322,a2,x9323))),f9(x9321,f21(x9322,a2,a4)))),
% 58.83/58.83 inference(scs_inference,[],[531,50,927,51,931,34,33,38,37])).
% 58.83/58.83 cnf(966,plain,
% 58.83/58.83 (P7(a7,f16(a5))),
% 58.83/58.83 inference(scs_inference,[],[612,2,125])).
% 58.83/58.83 cnf(975,plain,
% 58.83/58.83 (E(f6(x9751,x9752,f16(x9753)),f6(x9751,x9752,f12(f21(x9753,a1,x9754))))),
% 58.83/58.83 inference(scs_inference,[],[611,2,27])).
% 58.83/58.83 cnf(977,plain,
% 58.83/58.83 (P4(a7,f16(a5))),
% 58.83/58.83 inference(scs_inference,[],[611,277,975,2,34])).
% 58.83/58.83 cnf(978,plain,
% 58.83/58.83 (E(f12(f21(x9781,a1,x9782)),f16(x9781))),
% 58.83/58.83 inference(rename_variables,[],[611])).
% 58.83/58.83 cnf(979,plain,
% 58.83/58.83 (P4(f16(x9791),f12(f21(x9791,a1,x9792)))),
% 58.83/58.83 inference(scs_inference,[],[611,978,277,50,975,2,34,33])).
% 58.83/58.83 cnf(981,plain,
% 58.83/58.83 (P6(f18(f11(f12(f21(x9811,a1,x9812)),f10(x9813,x9814)),x9813),f16(x9811))),
% 58.83/58.83 inference(scs_inference,[],[611,978,277,50,355,975,2,34,33,38])).
% 58.83/58.83 cnf(983,plain,
% 58.83/58.83 (P6(f16(x9831),f18(f11(f12(f21(x9831,a1,x9832)),f10(x9833,x9834)),x9833))),
% 58.83/58.83 inference(scs_inference,[],[611,978,277,50,361,355,975,2,34,33,38,37])).
% 58.83/58.83 cnf(985,plain,
% 58.83/58.83 (E(f12(f21(a2,a1,x9851)),f16(f9(a2,x9852)))),
% 58.83/58.83 inference(scs_inference,[],[611,978,277,50,309,361,355,975,2,34,33,38,37,3])).
% 58.83/58.83 cnf(987,plain,
% 58.83/58.83 (~P7(f16(a5),a7)),
% 58.83/58.83 inference(scs_inference,[],[611,978,277,50,309,361,355,975,2,34,33,38,37,3,68])).
% 58.83/58.83 cnf(994,plain,
% 58.83/58.83 (E(f16(f9(a2,x9941)),f12(f21(a2,a1,x9942)))),
% 58.83/58.83 inference(scs_inference,[],[985,2])).
% 58.83/58.83 cnf(995,plain,
% 58.83/58.83 (~P7(f12(f21(x9951,a1,x9952)),f16(x9951))),
% 58.83/58.83 inference(scs_inference,[],[979,985,2,68])).
% 58.83/58.83 cnf(998,plain,
% 58.83/58.83 (E(f12(f21(x9981,a1,x9982)),f16(x9981))),
% 58.83/58.83 inference(rename_variables,[],[611])).
% 58.83/58.83 cnf(999,plain,
% 58.83/58.83 (P4(f16(x9991),f18(f11(f12(f21(x9991,a1,x9992)),f10(x9993,x9994)),x9993))),
% 58.83/58.83 inference(scs_inference,[],[611,998,280,359,979,985,2,68,34,33])).
% 58.83/58.83 cnf(1005,plain,
% 58.83/58.83 (E(f12(f21(a2,a1,x10051)),f18(f11(f16(f9(a2,x10052)),f10(x10053,x10054)),x10053))),
% 58.83/58.83 inference(scs_inference,[],[611,998,280,359,979,309,374,981,983,985,2,68,34,33,38,37,3])).
% 58.83/58.83 cnf(1017,plain,
% 58.83/58.83 (E(f12(f21(x10171,a1,x10172)),f16(x10171))),
% 58.83/58.83 inference(rename_variables,[],[611])).
% 58.83/58.83 cnf(1018,plain,
% 58.83/58.83 (P4(f16(f9(a2,x10181)),f18(f11(f12(f21(a2,a1,x10182)),f10(x10183,x10184)),x10183))),
% 58.83/58.83 inference(scs_inference,[],[611,296,999,309,1005,2,68,34,33])).
% 58.83/58.83 cnf(1020,plain,
% 58.83/58.83 (P6(f12(f21(x10201,a1,x10202)),f16(x10201))),
% 58.83/58.83 inference(scs_inference,[],[611,1017,296,999,309,1005,51,2,68,34,33,38])).
% 58.83/58.83 cnf(1021,plain,
% 58.83/58.83 (P6(x10211,x10211)),
% 58.83/58.83 inference(rename_variables,[],[51])).
% 58.83/58.83 cnf(1024,plain,
% 58.83/58.83 (E(f12(f21(a2,a1,x10241)),f12(f21(f9(a2,x10242),a1,x10243)))),
% 58.83/58.83 inference(scs_inference,[],[611,1017,296,999,309,903,1005,51,1021,2,68,34,33,38,37,3])).
% 58.83/58.83 cnf(1034,plain,
% 58.83/58.84 (P4(f12(f21(x10341,a1,x10342)),f16(x10341))),
% 58.83/58.84 inference(scs_inference,[],[611,50,1018,1024,2,68,34])).
% 58.83/58.84 cnf(1210,plain,
% 58.83/58.84 (~P1(f11(f9(a2,x12101),f10(a7,x12102)),f12(f21(a5,a1,a8)))),
% 58.83/58.84 inference(scs_inference,[],[129,523,2,82])).
% 58.83/58.84 cnf(1216,plain,
% 58.83/58.84 (P4(a7,f18(f11(f12(f21(a5,a1,x12161)),f10(x12162,x12163)),x12162))),
% 58.83/58.84 inference(scs_inference,[],[977,999,70])).
% 58.83/58.84 cnf(1228,plain,
% 58.83/58.84 (~P3(f19(f21(x12281,f9(a2,x12282),x12283),x12284),f18(f11(a3,f10(x12285,x12286)),x12285))),
% 58.83/58.84 inference(scs_inference,[],[213,892,2,46])).
% 58.83/58.84 cnf(1229,plain,
% 58.83/58.84 (E(f9(f12(f21(x12291,a2,x12292)),x12293),f9(f12(f21(x12294,a2,x12295)),x12293))),
% 58.83/58.84 inference(scs_inference,[],[894,2,4])).
% 58.83/58.84 cnf(1230,plain,
% 58.83/58.84 (E(f9(x12301,f9(a2,x12302)),f9(x12301,f18(f11(f9(a2,x12303),f10(x12304,x12305)),x12304)))),
% 58.83/58.84 inference(scs_inference,[],[899,2,5])).
% 58.83/58.84 cnf(1231,plain,
% 58.83/58.84 (E(f10(f18(f11(f9(a2,x12311),f10(x12312,x12313)),x12312),x12314),f10(f9(a2,x12315),x12314))),
% 58.83/58.84 inference(scs_inference,[],[900,2,6])).
% 58.83/58.84 cnf(1236,plain,
% 58.83/58.84 (P4(f12(f21(f9(a2,x12361),a1,x12362)),f16(a2))),
% 58.83/58.84 inference(scs_inference,[],[903,50,1034,835,38,34,33])).
% 58.83/58.84 cnf(1238,plain,
% 58.83/58.84 (P6(f12(f21(f9(a2,x12381),a1,x12382)),f16(f9(a2,x12383)))),
% 58.83/58.84 inference(scs_inference,[],[903,50,1034,838,835,38,34,33,37])).
% 58.83/58.84 cnf(1248,plain,
% 58.83/58.84 (P4(f12(f21(f9(a2,x12481),a1,x12482)),f16(f9(a2,x12483)))),
% 58.83/58.84 inference(scs_inference,[],[903,816,1236,1020,68,38,33])).
% 58.83/58.84 cnf(1253,plain,
% 58.83/58.84 (P6(f12(f21(f9(a2,x12531),a1,x12532)),f16(a2))),
% 58.83/58.84 inference(scs_inference,[],[1248,308,1238,68,38])).
% 58.83/58.84 cnf(1313,plain,
% 58.83/58.84 (~P8(f11(a2,f10(a2,x13131)),a1,x13132)),
% 58.83/58.84 inference(scs_inference,[],[105,62,2,92])).
% 58.83/58.84 cnf(1322,plain,
% 58.83/58.84 (E(f10(f16(f9(a2,x13221)),x13222),f10(f12(f21(a2,a1,x13223)),x13222))),
% 58.83/58.84 inference(scs_inference,[],[985,2,6])).
% 58.83/58.84 cnf(1324,plain,
% 58.83/58.84 (E(f10(x13241,f12(f21(a2,a1,x13242))),f10(x13241,f16(f9(a2,x13243))))),
% 58.83/58.84 inference(scs_inference,[],[994,2,7])).
% 58.83/58.84 cnf(1360,plain,
% 58.83/58.84 (E(f17(x13601,f12(f21(a2,a1,x13602))),f17(x13601,f16(f9(a2,x13603))))),
% 58.83/58.84 inference(scs_inference,[],[994,2,11])).
% 58.83/58.84 cnf(1392,plain,
% 58.83/58.84 (P4(f12(f21(x13921,a1,x13922)),f18(f11(f12(f21(x13921,a1,x13923)),f10(x13924,x13925)),x13924))),
% 58.83/58.84 inference(scs_inference,[],[1034,999,70])).
% 58.83/58.84 cnf(1397,plain,
% 58.83/58.84 (~P1(f11(f9(a2,x13971),f10(a2,x13972)),a1)),
% 58.83/58.84 inference(scs_inference,[],[105,523,2,82])).
% 58.83/58.84 cnf(1398,plain,
% 58.83/58.84 (~E(f18(f11(f9(a2,x13981),f10(x13982,x13983)),x13982),a1)),
% 58.83/58.84 inference(scs_inference,[],[695,1397,32])).
% 58.83/58.84 cnf(1401,plain,
% 58.83/58.84 (~P8(f11(f11(a2,f10(a2,x14011)),f10(x14012,a1)),a1,f18(f11(f9(a2,x14013),f10(x14014,x14015)),x14014))),
% 58.83/58.84 inference(scs_inference,[],[1398,1313,2,91])).
% 58.83/58.84 cnf(1402,plain,
% 58.83/58.84 (~P8(f11(a2,f10(a1,x14021)),f18(f11(f9(a2,x14022),f10(x14023,x14024)),x14023),x14025)),
% 58.83/58.84 inference(scs_inference,[],[1398,62,2,92])).
% 58.83/58.84 cnf(1404,plain,
% 58.83/58.84 (~P1(f11(f9(a2,x14041),f10(a1,x14042)),f18(f11(f9(a2,x14043),f10(x14044,x14045)),x14044))),
% 58.83/58.84 inference(scs_inference,[],[1398,523,2,82])).
% 58.83/58.84 cnf(1420,plain,
% 58.83/58.84 (~P8(f11(f11(a2,f10(a1,x14201)),f10(a1,x14202)),f18(f11(f9(a2,x14203),f10(x14204,x14205)),x14204),x14206)),
% 58.83/58.84 inference(scs_inference,[],[1398,1402,2,92])).
% 58.83/58.84 cnf(1433,plain,
% 58.83/58.84 (~P1(f11(f9(a2,x14331),f10(a2,x14332)),f11(x14333,f10(x14334,x14335)))),
% 58.83/58.84 inference(scs_inference,[],[173,523,2,82])).
% 58.83/58.84 cnf(1434,plain,
% 58.83/58.84 (~E(a2,f11(x14341,f10(x14342,x14343)))),
% 58.83/58.84 inference(scs_inference,[],[1433,74])).
% 58.83/58.84 cnf(1438,plain,
% 58.83/58.84 (E(f12(f21(x14381,f11(x14382,f10(x14383,x14384)),x14385)),f16(x14381))),
% 58.83/58.84 inference(scs_inference,[],[1434,2,77])).
% 58.83/58.84 cnf(1450,plain,
% 58.83/58.84 (~P8(f11(f11(f11(a2,f10(a1,x14501)),f10(a1,x14502)),f10(a1,x14503)),f18(f11(f9(a2,x14504),f10(x14505,x14506)),x14505),x14507)),
% 58.83/58.84 inference(scs_inference,[],[1398,1420,2,92])).
% 58.83/58.84 cnf(1695,plain,
% 58.83/58.84 (E(f16(f9(a2,x16951)),f18(f11(f12(f21(a2,a1,x16952)),f10(x16953,x16954)),x16953))),
% 58.83/58.84 inference(scs_inference,[],[53,985,3,2])).
% 58.83/58.84 cnf(1721,plain,
% 58.83/58.84 (E(f16(a2),f18(f11(f12(f21(a2,a1,x17211)),f10(x17212,x17213)),x17212))),
% 58.83/58.84 inference(scs_inference,[],[309,1695,3])).
% 58.83/58.84 cnf(1737,plain,
% 58.83/58.84 (E(x17371,f17(f11(x17372,f10(x17373,x17371)),x17373))),
% 58.83/58.84 inference(rename_variables,[],[228])).
% 58.83/58.84 cnf(1739,plain,
% 58.83/58.84 (E(x17391,f17(f11(x17392,f10(x17393,x17391)),x17393))),
% 58.83/58.84 inference(rename_variables,[],[228])).
% 58.83/58.84 cnf(1746,plain,
% 58.83/58.84 (P4(f17(f11(x17461,f10(x17462,a7)),x17462),f18(f11(f12(f21(a5,a1,x17463)),f10(x17464,x17465)),x17464))),
% 58.83/58.84 inference(scs_inference,[],[1216,159,161,714,324,560,689,221,228,1737,1739,1404,1231,2,44,43,70,32,34,33])).
% 58.83/58.84 cnf(1750,plain,
% 58.83/58.84 (P5(f18(f11(f18(f11(f11(x17501,f10(x17502,x17503)),f10(x17504,x17505)),x17504),f10(x17506,x17507)),x17506))),
% 58.83/58.84 inference(scs_inference,[],[1216,159,161,714,324,560,689,213,221,228,1737,1739,131,355,1404,1231,176,2,44,43,70,32,34,33,38,39])).
% 58.83/58.84 cnf(1769,plain,
% 58.83/58.84 (P8(f11(x17691,f10(a4,a4)),f18(f11(a4,f10(x17692,x17693)),x17692),f17(f11(x17694,f10(x17695,a4)),x17695))),
% 58.83/58.84 inference(scs_inference,[],[691,1746,228,1230,2,68,44])).
% 58.83/58.84 cnf(1827,plain,
% 58.83/58.84 (E(f19(f21(x18271,a2,x18272),x18273),f21(x18271,a2,a4))),
% 58.83/58.84 inference(scs_inference,[],[562,1210,1253,1721,61,999,966,67,71,72,87,17,28,4,5,7,10,11,16,18,19,20,21,22,23,29,30,73,12,14,25,26,27,98,81,86])).
% 58.83/58.84 cnf(1835,plain,
% 58.83/58.84 (P1(f11(a1,f10(x18351,x18352)),a7)),
% 58.83/58.84 inference(scs_inference,[],[47,562,1210,1253,1721,134,61,999,966,67,71,72,87,17,28,4,5,7,10,11,16,18,19,20,21,22,23,29,30,73,12,14,25,26,27,98,81,86,83,84,8,6,76])).
% 58.83/58.84 cnf(1848,plain,
% 58.83/58.84 (E(x18481,f18(f11(x18481,f10(x18482,x18483)),x18482))),
% 58.83/58.84 inference(rename_variables,[],[131])).
% 58.83/58.84 cnf(1856,plain,
% 58.83/58.84 (E(x18561,f18(f11(x18561,f10(x18562,x18563)),x18562))),
% 58.83/58.84 inference(rename_variables,[],[131])).
% 58.83/58.84 cnf(1863,plain,
% 58.83/58.84 (~P8(f11(f11(f11(a2,f10(a1,x18631)),f10(a1,x18632)),f10(a1,x18633)),f18(f11(f9(a2,x18634),f10(x18635,x18636)),x18635),x18637)),
% 58.83/58.84 inference(rename_variables,[],[1450])).
% 58.83/58.84 cnf(1867,plain,
% 58.83/58.84 (~P1(f11(f9(a2,x18671),f10(a1,x18672)),f18(f11(f9(a2,x18673),f10(x18674,x18675)),x18674))),
% 58.83/58.84 inference(rename_variables,[],[1404])).
% 58.83/58.84 cnf(1880,plain,
% 58.83/58.84 (E(f12(f21(x18801,f11(x18802,f10(x18803,x18804)),x18805)),f16(x18801))),
% 58.83/58.84 inference(rename_variables,[],[1438])).
% 58.83/58.84 cnf(1885,plain,
% 58.83/58.84 (~P1(f11(f9(a2,x18851),f10(a1,x18852)),f9(a2,x18853))),
% 58.83/58.84 inference(scs_inference,[],[47,987,995,889,681,562,1438,1880,1228,1360,1769,683,1450,1863,1210,1253,1401,1392,1721,1746,233,134,899,900,1404,1867,699,713,61,999,156,966,131,1848,62,523,67,71,72,87,17,28,4,5,7,10,11,16,18,19,20,21,22,23,29,30,73,12,14,25,26,27,98,81,86,83,84,8,6,76,88,74,80,15,13,24,9,125,2,68,45,46,79,91,92,42,82,43,44,31,70,36,35,69,32])).
% 58.83/58.84 cnf(1898,plain,
% 58.83/58.84 (P4(f16(a5),f6(a1,a7,f16(a5)))),
% 58.83/58.84 inference(scs_inference,[],[47,987,995,889,681,562,1438,1880,1229,1228,1322,1324,1360,1750,1769,683,1450,1863,1210,1253,1401,1392,1721,932,1746,233,134,899,900,1404,1867,699,60,713,61,999,156,966,63,131,1848,1856,62,523,228,67,71,72,87,17,28,4,5,7,10,11,16,18,19,20,21,22,23,29,30,73,12,14,25,26,27,98,81,86,83,84,8,6,76,88,74,80,15,13,24,9,125,2,68,45,46,79,91,92,42,82,43,44,31,70,36,35,69,32,34,33,38,39,3,90])).
% 58.83/58.84 cnf(1900,plain,
% 58.83/58.84 (P8(f9(a1,f16(a5)),a7,f6(a1,a7,f16(a5)))),
% 58.83/58.84 inference(scs_inference,[],[47,987,995,889,681,562,1438,1880,1229,1228,1322,1324,1360,1750,1769,683,1450,1863,1210,1253,1401,1392,1721,932,1746,233,134,899,900,1404,1867,699,60,713,61,999,156,966,63,131,1848,1856,62,523,228,67,71,72,87,17,28,4,5,7,10,11,16,18,19,20,21,22,23,29,30,73,12,14,25,26,27,98,81,86,83,84,8,6,76,88,74,80,15,13,24,9,125,2,68,45,46,79,91,92,42,82,43,44,31,70,36,35,69,32,34,33,38,39,3,90,95])).
% 58.83/58.84 cnf(1931,plain,
% 58.83/58.84 ($false),
% 58.83/58.84 inference(scs_inference,[],[1827,1885,1898,1835,1900,564,605,67,71,88,86,19,73,22,12,76,16,72,7,81]),
% 58.83/58.84 ['proof']).
% 58.83/58.84 % SZS output end Proof
% 58.83/58.84 % Total time :58.160000s
%------------------------------------------------------------------------------