%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : SWV376+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 : n024.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:02 EDT 2024
% Result : Theorem 58.74s 58.85s
% Output : CNFRefutation 58.84s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.06/0.11 % Problem : SWV376+1 : TPTP v8.2.0. Released v3.3.0.
% 0.06/0.11 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% 0.12/0.32 % Computer : n024.cluster.edu
% 0.12/0.32 % Model : x86_64 x86_64
% 0.12/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.32 % Memory : 8042.1875MB
% 0.12/0.32 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.32 % CPULimit : 300
% 0.12/0.32 % WCLimit : 300
% 0.12/0.32 % DateTime : Thu Jun 20 19:33:24 EDT 2024
% 0.12/0.32 % CPUTime :
% 0.19/0.51 start to proof:theBenchmark
% 58.74/58.83 %-------------------------------------------
% 58.74/58.83 % File :CSE---1.7
% 58.74/58.83 % Problem :theBenchmark
% 58.74/58.83 % Transform :cnf
% 58.74/58.83 % Format :tptp:raw
% 58.74/58.83 % Command :java -jar mcs_scs.jar %d %s
% 58.74/58.83
% 58.74/58.83 % Result :Theorem 58.250000s
% 58.74/58.83 % Output :CNFRefutation 58.250000s
% 58.74/58.83 %-------------------------------------------
% 58.74/58.84 %------------------------------------------------------------------------------
% 58.74/58.84 % File : SWV376+1 : TPTP v8.2.0. Released v3.3.0.
% 58.74/58.84 % Domain : Software Verification
% 58.74/58.84 % Problem : Priority queue checker: lemma_not_ok_persistence
% 58.74/58.84 % Version : [dNP05] axioms.
% 58.74/58.84 % English :
% 58.74/58.84
% 58.74/58.84 % Refs : [Pis06] Piskac (2006), Email to Geoff Sutcliffe
% 58.74/58.84 % : [dNP05] de Nivelle & Piskac (2005), Verification of an Off-Lin
% 58.74/58.84 % Source : [Pis06]
% 58.74/58.84 % Names : cpq_l012 [Pis06]
% 58.74/58.84
% 58.74/58.84 % Status : Theorem
% 58.74/58.84 % Rating : 0.25 v8.2.0, 0.22 v7.4.0, 0.20 v7.3.0, 0.24 v7.2.0, 0.21 v7.1.0, 0.30 v7.0.0, 0.27 v6.4.0, 0.31 v6.3.0, 0.33 v6.2.0, 0.36 v6.1.0, 0.23 v6.0.0, 0.22 v5.5.0, 0.30 v5.4.0, 0.36 v5.3.0, 0.37 v5.2.0, 0.30 v5.1.0, 0.24 v5.0.0, 0.29 v4.1.0, 0.39 v4.0.0, 0.42 v3.7.0, 0.45 v3.5.0, 0.47 v3.3.0
% 58.74/58.84 % Syntax : Number of formulae : 44 ( 16 unt; 0 def)
% 58.74/58.84 % Number of atoms : 93 ( 29 equ)
% 58.74/58.84 % Maximal formula atoms : 6 ( 2 avg)
% 58.74/58.84 % Number of connectives : 70 ( 21 ~; 3 |; 12 &)
% 58.74/58.84 % ( 7 <=>; 27 =>; 0 <=; 0 <~>)
% 58.74/58.84 % Maximal formula depth : 11 ( 5 avg)
% 58.74/58.84 % Maximal term depth : 4 ( 1 avg)
% 58.74/58.84 % Number of predicates : 11 ( 9 usr; 1 prp; 0-3 aty)
% 58.74/58.84 % Number of functors : 19 ( 19 usr; 3 con; 0-3 aty)
% 58.74/58.84 % Number of variables : 138 ( 138 !; 0 ?)
% 58.74/58.84 % SPC : FOF_THM_RFO_SEQ
% 58.74/58.84
% 58.74/58.84 % Comments :
% 58.74/58.84 %------------------------------------------------------------------------------
% 58.74/58.84 %----Include the axioms about priority queues and checked priority queues
% 58.74/58.84 include('Axioms/SWV007+0.ax').
% 58.74/58.84 include('Axioms/SWV007+2.ax').
% 58.74/58.84 include('Axioms/SWV007+3.ax').
% 58.74/58.84 %------------------------------------------------------------------------------
% 58.74/58.84 /*----
% 58.74/58.84 Explanation about induction
% 58.74/58.84 ===========================
% 58.74/58.84
% 58.74/58.84 In order to prove lemma_not_ok_persistence we use the following induction
% 58.74/58.84 principle: (the induction principle used in Coq)
% 58.74/58.84 =====================
% 58.74/58.84 let s/1 be the successor function defined on some set S and let =</2 be the
% 58.74/58.84 predicate that satisfies the following axioms:
% 58.74/58.84
% 58.74/58.84 1) x =< x
% 58.74/58.84 2) x =< y -> x =< s(y)
% 58.74/58.84
% 58.74/58.84 Note that our predicate succ_cpq/2 satisfies those two axioms
% 58.74/58.84
% 58.74/58.84 The induction principle: (V = for eVery
% 58.74/58.84
% 58.74/58.84 Vx ( (P(x) and Vy (x =< y -> (P(y) -> P(s(y)))) -> Vy (x=<y -> P(y)) )
% 58.74/58.84 ======================
% 58.74/58.84
% 58.74/58.84 Let P(x) == ~(ok(x)) and let =</2 == succ/2
% 58.74/58.84
% 58.74/58.84 Then, in order to confirm correctness of lemma_not_ok_persistence we have
% 58.74/58.84 to only verify "Vy (x =< y -> (P(y) -> P(s(y))))" part of the induction
% 58.74/58.84 principle, in other words we need to prove validity of:
% 58.74/58.84
% 58.74/58.84 all(CPQ1, all(CPQ2, succ_cpq(CPQ1, CPQ2) => ( ~(ok(CPQ2)) => ~(ok(s(CPQ2))) ) )), (1)
% 58.74/58.84
% 58.74/58.84 where s(CPQ2) is the immediate successor of CPQ2
% 58.74/58.84
% 58.74/58.84 all(CPQ2, ~(ok(CPQ2)) => ~(ok(s(CPQ2))) ) (2)
% 58.74/58.84
% 58.74/58.84 is a valid formula.
% 58.74/58.84
% 58.74/58.84 the validity of formula (2) is proved in lemma_not_ok_persistence_induction,
% 58.74/58.84 so here we have included it as a valid formula
% 58.74/58.84
% 58.74/58.84 lemma_not_ok_persistence_induction proves the validity of formula (1)
% 58.74/58.84 and thus, since (1) is valid we can conclude that the following formula holds:
% 58.74/58.85
% 58.74/58.85 Vx ( P(x) -> Vy (x=<y -> P(y)) )
% 58.74/58.85
% 58.74/58.85 or in our example:
% 58.74/58.85
% 58.74/58.85 all(CPQ, ~(ok(CPQ)) => all(CPQ1, succ(CPQ, CPQ1) => ~(ok(CPQ1)) ) )
% 58.74/58.85
% 58.74/58.85 which completes the inductive proof of lemma_not_ok_persistence
% 58.74/58.85 ----*/
% 58.74/58.85
% 58.74/58.85 %----induction axiom
% 58.74/58.85 fof(l12_induction,axiom,
% 58.74/58.85 ( ! [U,V,W,X,Y,Z] :
% 58.74/58.85 ( succ_cpq(triple(U,V,W),triple(X,Y,Z))
% 58.74/58.85 => ( ~ ok(triple(X,Y,Z))
% 58.74/58.85 => ~ ok(im_succ_cpq(triple(X,Y,Z))) ) )
% 58.74/58.85 => ! [X1,X2,X3] :
% 58.74/58.85 ( ~ ok(triple(X1,X2,X3))
% 58.74/58.85 => ! [X4,X5,X6] :
% 58.74/58.85 ( succ_cpq(triple(X1,X2,X3),triple(X4,X5,X6))
% 58.74/58.85 => ~ ok(triple(X4,X5,X6)) ) ) ) ).
% 58.74/58.85
% 58.74/58.85 %----lemma_not_ok_persistence_induction (cpq_l013.p .. cpq_l016.p)
% 58.74/58.85 fof(l12_l13,lemma,
% 58.74/58.85 ! [U,V,W] :
% 58.74/58.85 ( ~ ok(triple(U,V,W))
% 58.74/58.85 => ~ ok(im_succ_cpq(triple(U,V,W))) ) ).
% 58.74/58.85
% 58.74/58.85 %----lemma_not_ok_persistence (conjecture)
% 58.74/58.85 fof(l12_co,conjecture,
% 58.74/58.85 ! [U,V,W] :
% 58.74/58.85 ( ~ ok(triple(U,V,W))
% 58.74/58.85 => ! [X,Y,Z] :
% 58.74/58.85 ( succ_cpq(triple(U,V,W),triple(X,Y,Z))
% 58.74/58.85 => ~ ok(triple(X,Y,Z)) ) ) ).
% 58.74/58.85
% 58.74/58.85 %------------------------------------------------------------------------------
% 58.74/58.85 %-------------------------------------------
% 58.74/58.85 % Proof found
% 58.74/58.85 % SZS status Theorem for theBenchmark
% 58.74/58.85 % SZS output start Proof
% 58.74/58.85 %ClaNum:99(EqnAxiom:44)
% 58.74/58.85 %VarNum:341(SingletonVarNum:168)
% 58.74/58.85 %MaxLitNum:4
% 58.74/58.85 %MaxfuncDepth:3
% 58.74/58.85 %SharedTerms:27
% 58.74/58.85 %goalClause: 52 56 61
% 58.74/58.85 %singleGoalClaCount:3
% 58.74/58.85 [58]~P2(a1)
% 58.74/58.85 [52]P7(f29(a7,a8,a9))
% 58.74/58.85 [56]P6(f29(a12,a19,a20),f29(a7,a8,a9))
% 58.74/58.85 [61]~P7(f29(a12,a19,a20))
% 58.74/58.85 [46]P1(a2,x461)
% 58.74/58.85 [47]P1(x471,x471)
% 58.74/58.85 [48]P6(x481,x481)
% 58.74/58.85 [59]~P4(a1,x591)
% 58.74/58.85 [45]E(f4(a1,x451),a1)
% 58.74/58.85 [60]~P8(a1,x601,x602)
% 58.74/58.85 [54]P3(f29(x541,a1,x542))
% 58.74/58.85 [62]~P7(f29(x621,x622,a3))
% 58.74/58.85 [53]E(f10(f29(x531,a1,x532)),a2)
% 58.74/58.85 [55]E(f11(f29(x551,a1,x552)),f29(x551,a1,a3))
% 58.74/58.85 [49]P2(f6(x491,f5(x492,x493)))
% 58.74/58.85 [50]E(f26(f6(x501,f5(x502,x503)),x502),x501)
% 58.74/58.85 [51]E(f25(f6(x511,f5(x512,x513)),x512),x513)
% 58.74/58.85 [57]E(f29(f21(x571,x572),f6(x573,f5(x572,a2)),x574),f22(f29(x571,x573,x574),x572))
% 58.74/58.85 [63]P1(x632,x631)+P1(x631,x632)
% 58.74/58.85 [64]~P9(x641,x642)+P1(x641,x642)
% 58.74/58.85 [66]~P9(x662,x661)+~P1(x661,x662)
% 58.74/58.85 [65]~P6(x651,x652)+P6(x651,f11(x652))
% 58.74/58.85 [71]~P6(x711,x712)+P6(x711,f27(f11(x712),f10(x712)))
% 58.74/58.85 [69]~P6(x691,x692)+P6(x691,f22(x692,x693))
% 58.74/58.85 [70]~P6(x701,x702)+P6(x701,f27(x702,x703))
% 58.74/58.85 [73]E(x731,a3)+P7(f29(x732,x733,x731))
% 58.74/58.85 [75]E(x751,a1)+E(f10(f29(x752,x751,x753)),f23(x752))
% 58.74/58.85 [94]P7(f29(x941,x942,x943))+~P7(f24(f29(x941,x942,x943)))
% 58.74/58.85 [78]~P4(x782,x784)+P5(f29(x781,x782,x783),x784)
% 58.74/58.85 [84]P4(x841,x842)+~P5(f29(x843,x841,x844),x842)
% 58.74/58.85 [72]~E(x722,x724)+P4(f6(x721,f5(x722,x723)),x724)
% 58.74/58.85 [74]~P4(x741,x744)+P4(f6(x741,f5(x742,x743)),x744)
% 58.74/58.85 [83]P4(x832,x834)+E(f27(f29(x831,x832,x833),x834),f29(x831,x832,a3))
% 58.74/58.85 [80]~P1(x802,x804)+E(f6(f4(x801,x802),f5(x803,x804)),f4(f6(x801,f5(x803,x804)),x802))
% 58.74/58.85 [81]~P9(x813,x814)+E(f4(f6(x811,f5(x812,x813)),x814),f6(f4(x811,x814),f5(x812,x814)))
% 58.74/58.85 [85]~P8(x851,x854,x855)+P8(f6(x851,f5(x852,x853)),x854,x855)
% 58.74/58.85 [93]~P9(x931,x932)+~P3(f29(x933,f6(x934,f5(x931,x932)),x935))
% 58.74/58.85 [67]P9(x672,x671)+~P1(x672,x671)+P1(x671,x672)
% 58.74/58.85 [68]~P1(x681,x683)+P1(x681,x682)+~P1(x683,x682)
% 58.74/58.85 [86]P4(x861,f23(x862))+E(x861,a1)+E(f11(f29(x862,x861,x863)),f29(x862,f4(x861,f23(x862)),a3))
% 58.74/58.85 [79]E(x791,x792)+P4(x793,x792)+~P4(f6(x793,f5(x791,x794)),x792)
% 58.74/58.85 [89]~P4(x892,x894)+~P9(x894,f25(x892,x894))+E(f27(f29(x891,x892,x893),x894),f29(f28(x891,x894),f26(x892,x894),a3))
% 58.74/58.85 [90]~P4(x903,x902)+~P1(f25(x903,x902),x902)+E(f29(f28(x901,x902),f26(x903,x902),x904),f27(f29(x901,x903,x904),x902))
% 58.74/58.85 [76]~P4(x763,x762)+E(x761,x762)+E(f25(f6(x763,f5(x761,x764)),x762),f25(x763,x762))
% 58.74/58.85 [82]~P4(x823,x822)+E(x821,x822)+E(f26(f6(x823,f5(x821,x824)),x822),f6(f26(x823,x822),f5(x821,x824)))
% 58.74/58.85 [77]~E(x773,x775)+~E(x772,x774)+P8(f6(x771,f5(x772,x773)),x774,x775)
% 58.74/58.85 [87]E(x871,x872)+P8(x873,x874,x872)+~P8(f6(x873,f5(x875,x871)),x874,x872)
% 58.74/58.85 [88]E(x881,x882)+P8(x883,x882,x884)+~P8(f6(x883,f5(x881,x885)),x882,x884)
% 58.74/58.85 [95]~P1(x954,x953)+~P3(f29(x951,x952,x955))+P3(f29(x951,f6(x952,f5(x953,x954)),x955))
% 58.74/58.86 [96]~P1(x964,x965)+P3(f29(x961,x962,x963))+~P3(f29(x961,f6(x962,f5(x965,x964)),x963))
% 58.74/58.86 [91]~P4(x911,f23(x912))+E(x911,a1)+~P9(f23(x912),f25(x911,f23(x912)))+E(f11(f29(x912,x911,x913)),f29(x912,f4(x911,f23(x912)),a3))
% 58.74/58.86 [92]~P4(x921,f23(x922))+E(x921,a1)+~P1(f25(x921,f23(x922)),f23(x922))+E(f29(x922,f4(x921,f23(x922)),x923),f11(f29(x922,x921,x923)))
% 58.74/58.86 [97]~P6(f29(x971,x972,x973),f29(x974,x975,x976))+P7(f29(x971,x972,x973))+~P7(f29(x974,x975,x976))+~P7(f29(a13,a17,a18))
% 58.74/58.86 [99]~P6(f29(x991,x992,x993),f29(x994,x995,x996))+P6(f29(a14,a15,a16),f29(a13,a17,a18))+P7(f29(x991,x992,x993))+~P7(f29(x994,x995,x996))
% 58.74/58.86 [98]~P6(f29(x981,x982,x983),f29(x984,x985,x986))+P7(f29(x981,x982,x983))+~P7(f29(x984,x985,x986))+P7(f24(f29(a13,a17,a18)))
% 58.74/58.86 %EqnAxiom
% 58.74/58.86 [1]E(x11,x11)
% 58.74/58.86 [2]E(x22,x21)+~E(x21,x22)
% 58.74/58.86 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 58.74/58.86 [4]~E(x41,x42)+E(f4(x41,x43),f4(x42,x43))
% 58.74/58.86 [5]~E(x51,x52)+E(f4(x53,x51),f4(x53,x52))
% 58.74/58.86 [6]~E(x61,x62)+E(f5(x61,x63),f5(x62,x63))
% 58.74/58.86 [7]~E(x71,x72)+E(f5(x73,x71),f5(x73,x72))
% 58.74/58.86 [8]~E(x81,x82)+E(f6(x81,x83),f6(x82,x83))
% 58.74/58.86 [9]~E(x91,x92)+E(f6(x93,x91),f6(x93,x92))
% 58.74/58.86 [10]~E(x101,x102)+E(f29(x101,x103,x104),f29(x102,x103,x104))
% 58.74/58.86 [11]~E(x111,x112)+E(f29(x113,x111,x114),f29(x113,x112,x114))
% 58.74/58.86 [12]~E(x121,x122)+E(f29(x123,x124,x121),f29(x123,x124,x122))
% 58.74/58.86 [13]~E(x131,x132)+E(f11(x131),f11(x132))
% 58.74/58.86 [14]~E(x141,x142)+E(f26(x141,x143),f26(x142,x143))
% 58.74/58.86 [15]~E(x151,x152)+E(f26(x153,x151),f26(x153,x152))
% 58.74/58.86 [16]~E(x161,x162)+E(f25(x161,x163),f25(x162,x163))
% 58.74/58.86 [17]~E(x171,x172)+E(f25(x173,x171),f25(x173,x172))
% 58.74/58.86 [18]~E(x181,x182)+E(f27(x181,x183),f27(x182,x183))
% 58.74/58.86 [19]~E(x191,x192)+E(f27(x193,x191),f27(x193,x192))
% 58.74/58.86 [20]~E(x201,x202)+E(f10(x201),f10(x202))
% 58.74/58.86 [21]~E(x211,x212)+E(f23(x211),f23(x212))
% 58.74/58.86 [22]~E(x221,x222)+E(f28(x221,x223),f28(x222,x223))
% 58.74/58.86 [23]~E(x231,x232)+E(f28(x233,x231),f28(x233,x232))
% 58.74/58.86 [24]~E(x241,x242)+E(f22(x241,x243),f22(x242,x243))
% 58.74/58.86 [25]~E(x251,x252)+E(f22(x253,x251),f22(x253,x252))
% 58.74/58.86 [26]~E(x261,x262)+E(f24(x261),f24(x262))
% 58.74/58.86 [27]~E(x271,x272)+E(f21(x271,x273),f21(x272,x273))
% 58.74/58.86 [28]~E(x281,x282)+E(f21(x283,x281),f21(x283,x282))
% 58.74/58.86 [29]P1(x292,x293)+~E(x291,x292)+~P1(x291,x293)
% 58.74/58.86 [30]P1(x303,x302)+~E(x301,x302)+~P1(x303,x301)
% 58.74/58.86 [31]P6(x312,x313)+~E(x311,x312)+~P6(x311,x313)
% 58.74/58.86 [32]P6(x323,x322)+~E(x321,x322)+~P6(x323,x321)
% 58.74/58.86 [33]~P3(x331)+P3(x332)+~E(x331,x332)
% 58.74/58.86 [34]~P2(x341)+P2(x342)+~E(x341,x342)
% 58.74/58.86 [35]~P7(x351)+P7(x352)+~E(x351,x352)
% 58.74/58.86 [36]P9(x362,x363)+~E(x361,x362)+~P9(x361,x363)
% 58.74/58.86 [37]P9(x373,x372)+~E(x371,x372)+~P9(x373,x371)
% 58.74/58.86 [38]P4(x382,x383)+~E(x381,x382)+~P4(x381,x383)
% 58.74/58.86 [39]P4(x393,x392)+~E(x391,x392)+~P4(x393,x391)
% 58.74/58.86 [40]P8(x402,x403,x404)+~E(x401,x402)+~P8(x401,x403,x404)
% 58.74/58.86 [41]P8(x413,x412,x414)+~E(x411,x412)+~P8(x413,x411,x414)
% 58.74/58.86 [42]P8(x423,x424,x422)+~E(x421,x422)+~P8(x423,x424,x421)
% 58.74/58.86 [43]P5(x432,x433)+~E(x431,x432)+~P5(x431,x433)
% 58.74/58.86 [44]P5(x443,x442)+~E(x441,x442)+~P5(x443,x441)
% 58.74/58.86
% 58.74/58.86 %-------------------------------------------
% 58.84/58.87 cnf(100,plain,
% 58.84/58.87 (P4(f6(x1002,f5(x1001,x1003)),x1001)),
% 58.84/58.87 inference(equality_inference,[],[72])).
% 58.84/58.87 cnf(101,plain,
% 58.84/58.87 (E(a20,a3)),
% 58.84/58.87 inference(scs_inference,[],[61,73])).
% 58.84/58.87 cnf(103,plain,
% 58.84/58.87 (E(a1,f4(a1,x1031))),
% 58.84/58.87 inference(scs_inference,[],[61,45,73,2])).
% 58.84/58.87 cnf(106,plain,
% 58.84/58.87 (P6(a1,f4(a1,x1061))),
% 58.84/58.87 inference(scs_inference,[],[61,48,45,47,73,2,66,31])).
% 58.84/58.87 cnf(107,plain,
% 58.84/58.87 (P6(x1071,x1071)),
% 58.84/58.87 inference(rename_variables,[],[48])).
% 58.84/58.87 cnf(108,plain,
% 58.84/58.87 (P6(f4(a1,x1081),a1)),
% 58.84/58.87 inference(scs_inference,[],[61,48,107,45,47,73,2,66,31,32])).
% 58.84/58.87 cnf(113,plain,
% 58.84/58.87 (E(f26(f6(f4(a1,x1131),f5(x1132,x1133)),x1132),a1)),
% 58.84/58.87 inference(scs_inference,[],[61,48,107,45,62,55,50,47,73,2,66,31,32,35,3])).
% 58.84/58.87 cnf(115,plain,
% 58.84/58.87 (P1(a1,f4(a1,x1151))),
% 58.84/58.87 inference(scs_inference,[],[61,48,107,45,62,55,50,47,73,2,66,31,32,35,3,29])).
% 58.84/58.87 cnf(116,plain,
% 58.84/58.87 (P1(x1161,x1161)),
% 58.84/58.87 inference(rename_variables,[],[47])).
% 58.84/58.87 cnf(117,plain,
% 58.84/58.87 (P1(f4(a1,x1171),a1)),
% 58.84/58.87 inference(scs_inference,[],[61,48,107,45,62,55,50,47,116,73,2,66,31,32,35,3,29,30])).
% 58.84/58.87 cnf(119,plain,
% 58.84/58.87 (~P2(f4(a1,x1191))),
% 58.84/58.87 inference(scs_inference,[],[61,48,107,45,62,55,50,47,116,58,73,2,66,31,32,35,3,29,30,34])).
% 58.84/58.87 cnf(120,plain,
% 58.84/58.87 (~E(f6(x1201,f5(x1202,x1203)),a1)),
% 58.84/58.87 inference(scs_inference,[],[61,48,107,100,45,62,55,50,47,116,59,58,73,2,66,31,32,35,3,29,30,34,38])).
% 58.84/58.87 cnf(121,plain,
% 58.84/58.87 (P4(f6(x1211,f5(x1212,x1213)),x1212)),
% 58.84/58.87 inference(rename_variables,[],[100])).
% 58.84/58.87 cnf(122,plain,
% 58.84/58.87 (P4(f6(x1221,f5(f4(a1,x1222),x1223)),a1)),
% 58.84/58.87 inference(scs_inference,[],[61,48,107,100,121,45,62,55,50,47,116,59,58,73,2,66,31,32,35,3,29,30,34,38,39])).
% 58.84/58.87 cnf(124,plain,
% 58.84/58.87 (P6(f29(a14,a15,a16),f29(a13,a17,a18))),
% 58.84/58.87 inference(scs_inference,[],[52,56,61,48,107,100,121,45,62,55,50,47,116,59,58,73,2,66,31,32,35,3,29,30,34,38,39,99])).
% 58.84/58.87 cnf(131,plain,
% 58.84/58.87 (E(a3,a20)),
% 58.84/58.87 inference(scs_inference,[],[101,115,66,2])).
% 58.84/58.87 cnf(132,plain,
% 58.84/58.87 (P1(f4(a1,x1321),f4(a1,x1322))),
% 58.84/58.87 inference(scs_inference,[],[101,115,117,66,2,68])).
% 58.84/58.87 cnf(134,plain,
% 58.84/58.87 (P6(f4(a1,x1341),f4(a1,x1342))),
% 58.84/58.87 inference(scs_inference,[],[106,101,103,115,117,66,2,68,31])).
% 58.84/58.87 cnf(135,plain,
% 58.84/58.87 (~P7(f26(f6(f29(a12,a19,a20),f5(x1351,x1352)),x1351))),
% 58.84/58.87 inference(scs_inference,[],[61,106,101,103,115,117,50,66,2,68,31,35])).
% 58.84/58.87 cnf(137,plain,
% 58.84/58.87 (P6(a20,a3)),
% 58.84/58.87 inference(scs_inference,[],[61,106,101,48,103,115,117,50,66,2,68,31,35,32])).
% 58.84/58.87 cnf(139,plain,
% 58.84/58.87 (P1(a20,a3)),
% 58.84/58.87 inference(scs_inference,[],[61,106,101,48,103,115,117,50,47,66,2,68,31,35,32,30])).
% 58.84/58.87 cnf(140,plain,
% 58.84/58.87 (P1(x1401,x1401)),
% 58.84/58.87 inference(rename_variables,[],[47])).
% 58.84/58.87 cnf(141,plain,
% 58.84/58.87 (E(f25(f6(x1411,f5(x1412,a20)),x1412),a3)),
% 58.84/58.87 inference(scs_inference,[],[61,106,101,48,103,115,117,51,50,47,66,2,68,31,35,32,30,3])).
% 58.84/58.87 cnf(144,plain,
% 58.84/58.87 (P4(f6(x1441,f5(a20,x1442)),a3)),
% 58.84/58.87 inference(scs_inference,[],[61,106,101,48,113,103,115,117,51,100,50,58,47,66,2,68,31,35,32,30,3,34,39])).
% 58.84/58.87 cnf(146,plain,
% 58.84/58.87 (P1(a3,a20)),
% 58.84/58.87 inference(scs_inference,[],[61,106,101,48,113,103,115,117,51,100,50,58,47,140,66,2,68,31,35,32,30,3,34,39,29])).
% 58.84/58.87 cnf(151,plain,
% 58.84/58.87 (E(a3,f25(f6(x1511,f5(x1512,a20)),x1512))),
% 58.84/58.87 inference(scs_inference,[],[117,141,66,2])).
% 58.84/58.87 cnf(152,plain,
% 58.84/58.87 (P6(a3,a20)),
% 58.84/58.87 inference(scs_inference,[],[48,101,117,141,66,2,31])).
% 58.84/58.87 cnf(154,plain,
% 58.84/58.87 (P4(f6(x1541,f5(f4(a1,x1542),x1543)),f4(a1,x1544))),
% 58.84/58.87 inference(scs_inference,[],[48,101,117,141,103,122,66,2,31,39])).
% 58.84/58.87 cnf(160,plain,
% 58.84/58.87 (P6(f29(a12,a19,a20),x1601)+~E(f29(a7,a8,a9),x1601)),
% 58.84/58.87 inference(scs_inference,[],[56,48,101,117,141,113,103,122,120,59,66,2,31,39,3,79,35,32])).
% 58.84/58.87 cnf(162,plain,
% 58.84/58.87 (P1(x1621,x1622)+~E(a2,x1621)),
% 58.84/58.87 inference(scs_inference,[],[56,48,101,117,141,113,103,122,46,120,59,66,2,31,39,3,79,35,32,34,29])).
% 58.84/58.87 cnf(168,plain,
% 58.84/58.87 (E(a1,f26(f6(f4(a1,x1681),f5(x1682,x1683)),x1682))),
% 58.84/58.87 inference(scs_inference,[],[139,113,66,2])).
% 58.84/58.87 cnf(169,plain,
% 58.84/58.87 (E(f26(f6(f4(a1,x1691),f5(x1692,x1693)),x1692),f4(a1,x1694))),
% 58.84/58.87 inference(scs_inference,[],[139,113,103,66,2,3])).
% 58.84/58.87 cnf(171,plain,
% 58.84/58.87 (P6(x1711,f29(a7,a8,a9))+~E(f29(a12,a19,a20),x1711)),
% 58.84/58.87 inference(scs_inference,[],[56,139,113,103,66,2,3,35,31])).
% 58.84/58.87 cnf(173,plain,
% 58.84/58.87 (P6(f29(a14,a15,a16),x1731)+~E(f29(a13,a17,a18),x1731)),
% 58.84/58.87 inference(scs_inference,[],[56,124,139,113,103,131,66,2,3,35,31,34,32])).
% 58.84/58.87 cnf(179,plain,
% 58.84/58.87 (E(f4(a1,x1791),f26(f6(f4(a1,x1792),f5(x1793,x1794)),x1793))),
% 58.84/58.87 inference(scs_inference,[],[146,169,66,2])).
% 58.84/58.87 cnf(180,plain,
% 58.84/58.87 (P1(a20,f25(f6(x1801,f5(x1802,a20)),x1802))),
% 58.84/58.87 inference(scs_inference,[],[139,146,169,151,66,2,30])).
% 58.84/58.87 cnf(183,plain,
% 58.84/58.87 (P1(f25(f6(x1831,f5(x1832,a20)),x1832),a20)),
% 58.84/58.87 inference(scs_inference,[],[152,139,146,169,151,144,66,2,30,39,31,29])).
% 58.84/58.87 cnf(185,plain,
% 58.84/58.87 (~E(f6(x1851,f5(x1852,x1853)),f4(a1,x1854))),
% 58.84/58.87 inference(scs_inference,[],[137,152,139,146,45,169,151,144,120,66,2,30,39,31,29,32,3])).
% 58.84/58.87 cnf(198,plain,
% 58.84/58.87 (P1(f25(f6(x1981,f5(x1982,a20)),x1982),a3)),
% 58.84/58.87 inference(scs_inference,[],[101,180,183,57,66,2,30])).
% 58.84/58.87 cnf(207,plain,
% 58.84/58.87 (E(a2,f10(f29(x2071,a1,x2072)))),
% 58.84/58.87 inference(scs_inference,[],[183,53,66,2])).
% 58.84/58.87 cnf(208,plain,
% 58.84/58.87 (P1(f10(f29(x2081,a1,x2082)),x2083)),
% 58.84/58.87 inference(scs_inference,[],[183,53,46,66,2,29])).
% 58.84/58.87 cnf(210,plain,
% 58.84/58.87 (P6(x2101,f29(a13,a17,a18))+~E(f29(a14,a15,a16),x2101)),
% 58.84/58.87 inference(scs_inference,[],[124,45,183,53,46,66,2,29,35,31])).
% 58.84/58.87 cnf(215,plain,
% 58.84/58.87 (E(f29(x2151,a1,a3),f11(f29(x2151,a1,x2152)))),
% 58.84/58.87 inference(scs_inference,[],[198,55,66,2])).
% 58.84/58.87 cnf(216,plain,
% 58.84/58.87 (E(f25(f6(x2161,f5(x2162,a2)),x2162),f10(f29(x2163,a1,x2164)))),
% 58.84/58.87 inference(scs_inference,[],[198,207,55,51,66,2,3])).
% 58.84/58.87 cnf(218,plain,
% 58.84/58.87 (P3(f11(f29(x2181,a1,x2182)))),
% 58.84/58.87 inference(scs_inference,[],[198,207,55,51,54,66,2,3,33])).
% 58.84/58.87 cnf(224,plain,
% 58.84/58.87 (E(f10(f29(x2241,a1,x2242)),f25(f6(x2243,f5(x2244,a2)),x2244))),
% 58.84/58.87 inference(scs_inference,[],[208,216,66,2])).
% 58.84/58.87 cnf(235,plain,
% 58.84/58.87 (E(x2351,f26(f6(x2351,f5(x2352,x2353)),x2352))),
% 58.84/58.87 inference(scs_inference,[],[50,46,66,2])).
% 58.84/58.87 cnf(236,plain,
% 58.84/58.87 (P1(f25(f6(x2361,f5(x2362,a2)),x2362),x2363)),
% 58.84/58.87 inference(scs_inference,[],[208,224,50,46,66,2,29])).
% 58.84/58.87 cnf(242,plain,
% 58.84/58.87 (P6(x2421,f26(f6(f29(a7,a8,a9),f5(x2422,x2423)),x2422))+~E(f29(a12,a19,a20),x2421)),
% 58.84/58.87 inference(scs_inference,[],[52,56,208,215,55,224,50,46,66,2,29,35,32,3,31])).
% 58.84/58.87 cnf(247,plain,
% 58.84/58.87 (E(x2471,f26(f6(x2471,f5(x2472,x2473)),x2472))),
% 58.84/58.87 inference(rename_variables,[],[235])).
% 58.84/58.87 cnf(248,plain,
% 58.84/58.87 (P6(f26(f6(f29(a14,a15,a16),f5(x2481,x2482)),x2481),f29(a13,a17,a18))),
% 58.84/58.87 inference(scs_inference,[],[235,247,171,210])).
% 58.84/58.87 cnf(249,plain,
% 58.84/58.87 (E(x2491,f26(f6(x2491,f5(x2492,x2493)),x2492))),
% 58.84/58.87 inference(rename_variables,[],[235])).
% 58.84/58.87 cnf(250,plain,
% 58.84/58.87 (P1(f26(f6(a2,f5(x2501,x2502)),x2501),x2503)),
% 58.84/58.87 inference(scs_inference,[],[235,247,249,171,210,162])).
% 58.84/58.87 cnf(251,plain,
% 58.84/58.87 (E(x2511,f26(f6(x2511,f5(x2512,x2513)),x2512))),
% 58.84/58.87 inference(rename_variables,[],[235])).
% 58.84/58.87 cnf(254,plain,
% 58.84/58.87 (E(x2541,f25(f6(x2542,f5(x2543,x2541)),x2543))),
% 58.84/58.87 inference(scs_inference,[],[235,247,249,236,51,171,210,162,66,2])).
% 58.84/58.87 cnf(256,plain,
% 58.84/58.87 (E(x2561,f26(f6(x2561,f5(x2562,x2563)),x2562))),
% 58.84/58.87 inference(rename_variables,[],[235])).
% 58.84/58.87 cnf(258,plain,
% 58.84/58.87 (E(x2581,f26(f6(x2581,f5(x2582,x2583)),x2582))),
% 58.84/58.87 inference(rename_variables,[],[235])).
% 58.84/58.87 cnf(259,plain,
% 58.84/58.87 (E(a20,f25(f6(x2591,f5(x2592,a3)),x2592))),
% 58.84/58.87 inference(scs_inference,[],[101,124,208,235,247,249,251,256,236,51,171,210,162,66,2,29,32,3])).
% 58.84/58.87 cnf(260,plain,
% 58.84/58.87 (P2(f26(f6(f6(x2601,f5(x2602,x2603)),f5(x2604,x2605)),x2604))),
% 58.84/58.87 inference(scs_inference,[],[101,124,208,235,247,249,251,256,258,236,51,49,171,210,162,66,2,29,32,3,34])).
% 58.84/58.87 cnf(261,plain,
% 58.84/58.87 (E(x2611,f26(f6(x2611,f5(x2612,x2613)),x2612))),
% 58.84/58.87 inference(rename_variables,[],[235])).
% 58.84/58.87 cnf(262,plain,
% 58.84/58.87 (P3(f26(f6(f11(f29(x2621,a1,x2622)),f5(x2623,x2624)),x2623))),
% 58.84/58.87 inference(scs_inference,[],[101,124,208,235,247,249,251,256,258,261,236,218,51,49,171,210,162,66,2,29,32,3,34,33])).
% 58.84/58.87 cnf(275,plain,
% 58.84/58.87 (E(a3,f26(f6(a20,f5(x2751,x2752)),x2751))),
% 58.84/58.87 inference(scs_inference,[],[101,250,50,66,3,2])).
% 58.84/58.87 cnf(287,plain,
% 58.84/58.87 (E(x2871,f26(f6(x2871,f5(x2872,x2873)),x2872))),
% 58.84/58.87 inference(rename_variables,[],[235])).
% 58.84/58.88 cnf(288,plain,
% 58.84/58.88 (P1(a20,f26(f6(a3,f5(x2881,x2882)),x2881))),
% 58.84/58.88 inference(scs_inference,[],[139,235,287,144,132,66,39,30])).
% 58.84/58.88 cnf(289,plain,
% 58.84/58.88 (E(x2891,f26(f6(x2891,f5(x2892,x2893)),x2892))),
% 58.84/58.88 inference(rename_variables,[],[235])).
% 58.84/58.88 cnf(291,plain,
% 58.84/58.88 (E(x2911,f26(f6(x2911,f5(x2912,x2913)),x2912))),
% 58.84/58.88 inference(rename_variables,[],[235])).
% 58.84/58.88 cnf(293,plain,
% 58.84/58.88 (E(x2931,f26(f6(x2931,f5(x2932,x2933)),x2932))),
% 58.84/58.88 inference(rename_variables,[],[235])).
% 58.84/58.88 cnf(299,plain,
% 58.84/58.88 (E(a20,f26(f6(a3,f5(x2991,x2992)),x2991))),
% 58.84/58.88 inference(scs_inference,[],[137,152,139,146,235,287,289,291,293,207,50,144,132,59,66,39,30,29,31,32,3,2,79])).
% 58.84/58.88 cnf(302,plain,
% 58.84/58.88 (P1(a3,f26(f6(a3,f5(x3021,x3022)),x3021))),
% 58.84/58.88 inference(scs_inference,[],[137,152,139,146,235,287,289,291,293,207,50,144,132,59,66,39,30,29,31,32,3,2,79,68])).
% 58.84/58.88 cnf(311,plain,
% 58.84/58.88 (E(f26(f6(a3,f5(x3111,x3112)),x3111),a20)),
% 58.84/58.88 inference(scs_inference,[],[288,299,66,2])).
% 58.84/58.88 cnf(350,plain,
% 58.84/58.88 (E(f11(f29(x3501,a1,x3502)),f26(f6(f29(x3501,a1,a3),f5(x3503,x3504)),x3503))),
% 58.84/58.88 inference(scs_inference,[],[215,50,302,66,3,2])).
% 58.84/58.88 cnf(385,plain,
% 58.84/58.88 (E(x3851,f26(f6(x3851,f5(x3852,x3853)),x3852))),
% 58.84/58.88 inference(rename_variables,[],[235])).
% 58.84/58.88 cnf(386,plain,
% 58.84/58.88 (P1(f26(f6(a1,f5(x3861,x3862)),x3861),f4(a1,x3863))),
% 58.84/58.88 inference(scs_inference,[],[115,235,385,30,29])).
% 58.84/58.88 cnf(387,plain,
% 58.84/58.88 (E(x3871,f26(f6(x3871,f5(x3872,x3873)),x3872))),
% 58.84/58.88 inference(rename_variables,[],[235])).
% 58.84/58.88 cnf(388,plain,
% 58.84/58.88 (P6(f26(f6(f4(a1,x3881),f5(x3882,x3883)),x3882),f4(a1,x3884))),
% 58.84/58.88 inference(scs_inference,[],[134,115,235,385,387,30,29,31])).
% 58.84/58.88 cnf(389,plain,
% 58.84/58.88 (E(x3891,f26(f6(x3891,f5(x3892,x3893)),x3892))),
% 58.84/58.88 inference(rename_variables,[],[235])).
% 58.84/58.88 cnf(396,plain,
% 58.84/58.88 (P1(f4(a1,x3961),f26(f6(f4(a1,x3962),f5(x3963,x3964)),x3963))),
% 58.84/58.88 inference(scs_inference,[],[134,115,235,385,387,389,117,30,29,31,32,66,67,68])).
% 58.84/58.88 cnf(403,plain,
% 58.84/58.88 (P1(f26(f6(a1,f5(x4031,x4032)),x4031),a1)),
% 58.84/58.88 inference(scs_inference,[],[45,386,66,30])).
% 58.84/58.88 cnf(419,plain,
% 58.84/58.88 (P1(f26(f6(f4(a1,x4191),f5(x4192,x4193)),x4192),f4(a1,x4194))),
% 58.84/58.88 inference(scs_inference,[],[103,235,117,403,66,29,30])).
% 58.84/58.88 cnf(438,plain,
% 58.84/58.88 (P6(f4(a1,x4381),f26(f6(a1,f5(x4382,x4383)),x4382))),
% 58.84/58.88 inference(scs_inference,[],[108,235,396,66,32])).
% 58.84/58.88 cnf(439,plain,
% 58.84/58.88 (E(x4391,f26(f6(x4391,f5(x4392,x4393)),x4392))),
% 58.84/58.88 inference(rename_variables,[],[235])).
% 58.84/58.88 cnf(440,plain,
% 58.84/58.88 (P6(f26(f6(a1,f5(x4401,x4402)),x4401),f4(a1,x4403))),
% 58.84/58.88 inference(scs_inference,[],[108,106,235,439,396,66,32,31])).
% 58.84/58.88 cnf(516,plain,
% 58.84/58.88 (E(f25(f6(x5161,f5(x5162,a1)),x5162),f4(a1,x5163))),
% 58.84/58.88 inference(scs_inference,[],[45,440,438,254,32,31,3,2])).
% 58.84/58.88 cnf(522,plain,
% 58.84/58.88 (~E(f6(x5221,f5(x5222,x5223)),f25(f6(x5224,f5(x5225,a1)),x5225))),
% 58.84/58.88 inference(scs_inference,[],[185,516,3])).
% 58.84/58.88 cnf(530,plain,
% 58.84/58.88 (P1(x5301,f26(f6(x5301,f5(x5302,x5303)),x5302))),
% 58.84/58.88 inference(scs_inference,[],[50,47,29])).
% 58.84/58.88 cnf(531,plain,
% 58.84/58.88 (P1(x5311,x5311)),
% 58.84/58.88 inference(rename_variables,[],[47])).
% 58.84/58.88 cnf(532,plain,
% 58.84/58.88 (P6(f26(f6(x5321,f5(x5322,x5323)),x5322),x5321)),
% 58.84/58.88 inference(scs_inference,[],[50,48,47,29,32])).
% 58.84/58.88 cnf(533,plain,
% 58.84/58.88 (P6(x5331,x5331)),
% 58.84/58.88 inference(rename_variables,[],[48])).
% 58.84/58.88 cnf(534,plain,
% 58.84/58.88 (P1(f26(f6(x5341,f5(x5342,x5343)),x5342),x5341)),
% 58.84/58.88 inference(scs_inference,[],[50,48,47,531,29,32,30])).
% 58.84/58.88 cnf(536,plain,
% 58.84/58.88 (P6(x5361,f26(f6(x5361,f5(x5362,x5363)),x5362))),
% 58.84/58.88 inference(scs_inference,[],[50,48,533,47,531,29,32,30,31])).
% 58.84/58.88 cnf(538,plain,
% 58.84/58.88 (E(f26(f6(f11(f29(x5381,a1,x5382)),f5(x5383,x5384)),x5383),f29(x5381,a1,a3))),
% 58.84/58.88 inference(scs_inference,[],[50,48,533,55,47,531,29,32,30,31,3])).
% 58.84/58.88 cnf(561,plain,
% 58.84/58.88 (P6(f29(a12,a19,a20),f11(f22(f29(a7,a8,a9),x5611)))),
% 58.84/58.88 inference(scs_inference,[],[56,65,69])).
% 58.84/58.88 cnf(571,plain,
% 58.84/58.88 (P1(x5711,f25(f6(x5712,f5(x5713,x5711)),x5713))),
% 58.84/58.88 inference(scs_inference,[],[51,47,29])).
% 58.84/58.88 cnf(572,plain,
% 58.84/58.88 (P1(x5721,x5721)),
% 58.84/58.88 inference(rename_variables,[],[47])).
% 58.84/58.88 cnf(573,plain,
% 58.84/58.88 (P1(f25(f6(x5731,f5(x5732,x5733)),x5732),x5733)),
% 58.84/58.88 inference(scs_inference,[],[51,47,572,29,30])).
% 58.84/58.88 cnf(575,plain,
% 58.84/58.88 (P6(f25(f6(x5751,f5(x5752,x5753)),x5752),x5753)),
% 58.84/58.88 inference(scs_inference,[],[51,48,47,572,29,30,32])).
% 58.84/58.88 cnf(576,plain,
% 58.84/58.88 (P6(x5761,x5761)),
% 58.84/58.88 inference(rename_variables,[],[48])).
% 58.84/58.88 cnf(577,plain,
% 58.84/58.88 (P6(x5771,f25(f6(x5772,f5(x5773,x5771)),x5773))),
% 58.84/58.88 inference(scs_inference,[],[51,48,576,47,572,29,30,32,31])).
% 58.84/58.88 cnf(634,plain,
% 58.84/58.88 (P1(f29(x6341,a1,a3),f26(f6(f11(f29(x6341,a1,x6342)),f5(x6343,x6344)),x6343))),
% 58.84/58.88 inference(scs_inference,[],[55,530,29])).
% 58.84/58.88 cnf(636,plain,
% 58.84/58.88 (P1(f26(f6(f11(f29(x6361,a1,x6362)),f5(x6363,x6364)),x6363),f29(x6361,a1,a3))),
% 58.84/58.88 inference(scs_inference,[],[55,530,534,29,30])).
% 58.84/58.88 cnf(647,plain,
% 58.84/58.88 (P1(x6471,x6471)),
% 58.84/58.88 inference(rename_variables,[],[47])).
% 58.84/58.88 cnf(648,plain,
% 58.84/58.88 (P1(f11(f29(x6481,a1,x6482)),f29(x6481,a1,a3))),
% 58.84/58.88 inference(scs_inference,[],[55,636,47,647,66,29,30])).
% 58.84/58.88 cnf(652,plain,
% 58.84/58.88 (P6(f29(x6521,a1,a3),f26(f6(f11(f29(x6521,a1,x6522)),f5(x6523,x6524)),x6523))),
% 58.84/58.88 inference(scs_inference,[],[55,532,536,636,47,647,66,29,30,32,31])).
% 58.84/58.88 cnf(665,plain,
% 58.84/58.88 (~P5(f29(x6651,f26(f6(f4(a1,x6652),f5(x6653,x6654)),x6653),x6655),x6656)),
% 58.84/58.88 inference(scs_inference,[],[59,113,84,38])).
% 58.84/58.88 cnf(698,plain,
% 58.84/58.88 (E(f27(f11(a20),x6981),f27(f11(a3),x6981))),
% 58.84/58.88 inference(scs_inference,[],[101,18,13])).
% 58.84/58.88 cnf(699,plain,
% 58.84/58.88 (E(f27(f11(a3),x6991),f27(f11(a20),x6991))),
% 58.84/58.88 inference(scs_inference,[],[698,2])).
% 58.84/58.88 cnf(705,plain,
% 58.84/58.88 (E(f27(x7051,f10(a20)),f27(x7051,f10(a3)))),
% 58.84/58.88 inference(scs_inference,[],[101,19,20])).
% 58.84/58.88 cnf(775,plain,
% 58.84/58.88 (E(f27(x7751,f10(a3)),f27(x7751,f10(a20)))),
% 58.84/58.88 inference(scs_inference,[],[705,2])).
% 58.84/58.88 cnf(1142,plain,
% 58.84/58.88 (~P9(f25(f6(x11421,f5(x11422,a1)),x11422),f4(a1,x11423))),
% 58.84/58.88 inference(scs_inference,[],[103,575,577,571,573,100,39,29,30,31,32,66])).
% 58.84/58.88 cnf(1196,plain,
% 58.84/58.88 (E(f27(f11(a3),f10(a3)),f27(f11(a20),f10(a20)))),
% 58.84/58.88 inference(scs_inference,[],[699,775,3])).
% 58.84/58.88 cnf(1278,plain,
% 58.84/58.88 (~E(f6(x12781,f5(x12782,x12783)),f26(f6(a1,f5(x12784,x12785)),x12784))),
% 58.84/58.88 inference(scs_inference,[],[120,50,3])).
% 58.84/58.88 cnf(1287,plain,
% 58.84/58.88 (P1(f25(f6(x12871,f5(x12872,a3)),x12872),a20)),
% 58.84/58.88 inference(scs_inference,[],[131,573,100,39,30])).
% 58.84/58.88 cnf(1289,plain,
% 58.84/58.88 (P1(a20,f25(f6(x12891,f5(x12892,a3)),x12892))),
% 58.84/58.88 inference(scs_inference,[],[131,571,573,100,39,30,29])).
% 58.84/58.88 cnf(1304,plain,
% 58.84/58.88 (E(f10(f29(x13041,f6(x13042,f5(x13043,x13044)),x13045)),f23(x13041))),
% 58.84/58.88 inference(scs_inference,[],[235,1278,75,3])).
% 58.84/58.88 cnf(1305,plain,
% 58.84/58.88 (~P7(f24(f29(a12,a19,a20)))),
% 58.84/58.88 inference(scs_inference,[],[235,135,94,35])).
% 58.84/58.88 cnf(1307,plain,
% 58.84/58.88 (P8(f6(f6(x13071,f5(a20,a20)),f5(x13072,x13073)),a3,a3)),
% 58.84/58.88 inference(scs_inference,[],[101,85,77])).
% 58.84/58.88 cnf(1389,plain,
% 58.84/58.88 (P4(f6(x13891,f5(f29(x13892,a1,a3),x13893)),f11(f29(x13892,a1,x13894)))),
% 58.84/58.88 inference(scs_inference,[],[215,100,39])).
% 58.84/58.88 cnf(1393,plain,
% 58.84/58.88 (P1(f11(f29(x13931,a1,x13932)),f26(f6(f11(f29(x13931,a1,x13933)),f5(x13934,x13935)),x13934))),
% 58.84/58.88 inference(scs_inference,[],[215,648,100,634,39,30,29])).
% 58.84/58.88 cnf(1405,plain,
% 58.84/58.88 (P6(f11(f29(x14051,a1,x14052)),f26(f6(f11(f29(x14051,a1,x14053)),f5(x14054,x14055)),x14054))),
% 58.84/58.88 inference(scs_inference,[],[215,652,636,1393,66,30,31])).
% 58.84/58.88 cnf(1641,plain,
% 58.84/58.88 (P8(f6(f6(x16411,f5(a20,a20)),f5(x16412,x16413)),f26(f6(a20,f5(x16414,x16415)),x16414),a3)),
% 58.84/58.88 inference(scs_inference,[],[275,1307,41])).
% 58.84/58.88 cnf(2504,plain,
% 58.84/58.88 (E(x25041,f26(f6(x25041,f5(x25042,x25043)),x25042))),
% 58.84/58.88 inference(rename_variables,[],[235])).
% 58.84/58.88 cnf(2508,plain,
% 58.84/58.88 (E(x25081,f25(f6(x25082,f5(x25083,x25081)),x25083))),
% 58.84/58.88 inference(rename_variables,[],[254])).
% 58.84/58.88 cnf(2510,plain,
% 58.84/58.88 (E(x25101,f25(f6(x25102,f5(x25103,x25101)),x25103))),
% 58.84/58.88 inference(rename_variables,[],[254])).
% 58.84/58.88 cnf(2517,plain,
% 58.84/58.88 (P4(f6(x25171,f5(f4(a1,x25172),x25173)),f26(f6(f4(a1,x25174),f5(x25175,x25176)),x25175))),
% 58.84/58.88 inference(scs_inference,[],[179,235,115,571,254,2508,2510,1304,154,665,242,78,210,171,160,2,68,39])).
% 58.84/58.88 cnf(2520,plain,
% 58.84/58.88 (E(x25201,f26(f6(x25201,f5(x25202,x25203)),x25202))),
% 58.84/58.88 inference(rename_variables,[],[235])).
% 58.84/58.88 cnf(2531,plain,
% 58.84/58.88 (E(x25311,f26(f6(x25311,f5(x25312,x25313)),x25312))),
% 58.84/58.88 inference(rename_variables,[],[235])).
% 58.84/58.88 cnf(2532,plain,
% 58.84/58.88 (P2(f26(f6(f26(f6(f6(x25321,f5(x25322,x25323)),f5(x25324,x25325)),x25324),f5(x25326,x25327)),x25326))),
% 58.84/58.88 inference(scs_inference,[],[1405,61,388,311,259,179,350,51,235,2504,2520,2531,115,419,386,571,254,2508,2510,1304,262,260,154,665,242,78,210,171,160,2,68,39,29,30,31,32,3,35,33,34])).
% 58.84/58.88 cnf(2600,plain,
% 58.84/58.88 (~P8(a1,x26001,x26002)),
% 58.84/58.88 inference(rename_variables,[],[60])).
% 58.84/58.88 cnf(2608,plain,
% 58.84/58.88 (~P7(f29(a13,a17,a18))),
% 58.84/58.88 inference(scs_inference,[],[52,60,2600,1305,1142,561,522,2517,2532,248,1389,1287,538,1196,119,185,1289,1641,516,168,62,61,254,146,59,113,56,65,69,70,84,13,20,21,26,72,74,4,5,6,7,8,9,14,15,16,17,18,19,22,23,24,25,27,28,71,85,94,10,11,12,83,173,80,78,2,37,43,77,40,68,87,88,3,35,34,97])).
% 58.84/58.88 cnf(2610,plain,
% 58.84/58.88 (P7(f24(f29(a13,a17,a18)))),
% 58.84/58.88 inference(scs_inference,[],[52,60,2600,1305,1142,561,522,2517,2532,248,1389,1287,538,1196,119,185,1289,1641,516,168,62,61,254,146,59,113,56,65,69,70,84,13,20,21,26,72,74,4,5,6,7,8,9,14,15,16,17,18,19,22,23,24,25,27,28,71,85,94,10,11,12,83,173,80,78,2,37,43,77,40,68,87,88,3,35,34,97,98])).
% 58.84/58.88 cnf(2620,plain,
% 58.84/58.88 ($false),
% 58.84/58.88 inference(scs_inference,[],[2608,2610,94]),
% 58.84/58.88 ['proof']).
% 58.84/58.88 % SZS output end Proof
% 58.84/58.88 % Total time :58.250000s
%------------------------------------------------------------------------------