%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : SWV479+1 : TPTP v8.2.0. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% Computer : n027.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:26 EDT 2024
% Result : Theorem 126.24s 126.38s
% Output : CNFRefutation 126.35s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.05/0.09 % Problem : SWV479+1 : TPTP v8.2.0. Released v4.0.0.
% 0.05/0.09 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% 0.09/0.29 % Computer : n027.cluster.edu
% 0.09/0.29 % Model : x86_64 x86_64
% 0.09/0.29 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.29 % Memory : 8042.1875MB
% 0.09/0.29 % OS : Linux 3.10.0-693.el7.x86_64
% 0.09/0.29 % CPULimit : 300
% 0.09/0.29 % WCLimit : 300
% 0.09/0.29 % DateTime : Thu Jun 20 17:58:53 EDT 2024
% 0.09/0.29 % CPUTime :
% 0.14/0.51 start to proof:theBenchmark
% 126.24/126.36 %-------------------------------------------
% 126.24/126.37 % File :CSE---1.7
% 126.24/126.37 % Problem :theBenchmark
% 126.24/126.37 % Transform :cnf
% 126.24/126.37 % Format :tptp:raw
% 126.24/126.37 % Command :java -jar mcs_scs.jar %d %s
% 126.24/126.37
% 126.24/126.37 % Result :Theorem 125.710000s
% 126.24/126.37 % Output :CNFRefutation 125.710000s
% 126.24/126.37 %-------------------------------------------
% 126.24/126.38 %------------------------------------------------------------------------------
% 126.24/126.38 % File : SWV479+1 : TPTP v8.2.0. Released v4.0.0.
% 126.24/126.38 % Domain : Software Verification
% 126.24/126.38 % Problem : Establishing that there cannot be two leaders, part i56_p116
% 126.24/126.38 % Version : [Sve07] axioms : Especial.
% 126.24/126.38 % English :
% 126.24/126.38
% 126.24/126.38 % Refs : [Sto97] Stoller (1997), Leader Election in Distributed Systems
% 126.24/126.38 % : [Sve07] Svensson (2007), Email to Koen Claessen
% 126.24/126.38 % : [Sve08] Svensson (2008), A Semi-Automatic Correctness Proof Pr
% 126.24/126.38 % Source : [Sve07]
% 126.24/126.38 % Names : stoller_i56_p116 [Sve07]
% 126.24/126.38
% 126.24/126.38 % Status : Theorem
% 126.24/126.38 % Rating : 0.47 v8.2.0, 0.42 v7.5.0, 0.44 v7.4.0, 0.33 v7.3.0, 0.45 v7.2.0, 0.41 v7.1.0, 0.39 v7.0.0, 0.40 v6.4.0, 0.46 v6.3.0, 0.42 v6.2.0, 0.52 v6.1.0, 0.50 v6.0.0, 0.48 v5.5.0, 0.63 v5.4.0, 0.64 v5.3.0, 0.70 v5.2.0, 0.55 v5.1.0, 0.62 v5.0.0, 0.71 v4.1.0, 0.74 v4.0.0
% 126.24/126.38 % Syntax : Number of formulae : 67 ( 40 unt; 0 def)
% 126.24/126.38 % Number of atoms : 237 ( 121 equ)
% 126.24/126.38 % Maximal formula atoms : 126 ( 3 avg)
% 126.24/126.38 % Number of connectives : 239 ( 69 ~; 12 |; 105 &)
% 126.24/126.38 % ( 13 <=>; 40 =>; 0 <=; 0 <~>)
% 126.24/126.38 % Maximal formula depth : 33 ( 4 avg)
% 126.24/126.38 % Maximal term depth : 4 ( 1 avg)
% 126.24/126.38 % Number of predicates : 6 ( 5 usr; 0 prp; 1-2 aty)
% 126.24/126.38 % Number of functors : 34 ( 34 usr; 17 con; 0-2 aty)
% 126.24/126.38 % Number of variables : 175 ( 174 !; 1 ?)
% 126.24/126.38 % SPC : FOF_THM_RFO_SEQ
% 126.24/126.38
% 126.24/126.38 % Comments :
% 126.24/126.38 %------------------------------------------------------------------------------
% 126.24/126.38 %----Include axioms for verification of Stoller's leader election algorithm
% 126.24/126.38 include('Axioms/SWV011+0.ax').
% 126.24/126.38 %------------------------------------------------------------------------------
% 126.24/126.38 fof(conj,conjecture,
% 126.24/126.38 ! [V,W,X,Y] :
% 126.24/126.38 ( ( ! [Z,Pid0] :
% 126.24/126.38 ( elem(m_Ldr(Pid0),queue(host(Z)))
% 126.24/126.38 => ~ leq(host(Z),host(Pid0)) )
% 126.24/126.38 & ! [Z,Pid0] :
% 126.24/126.38 ( elem(m_Down(Pid0),queue(host(Z)))
% 126.24/126.38 => host(Pid0) != host(Z) )
% 126.24/126.38 & ! [Z,Pid0] :
% 126.24/126.38 ( ( Pid0 != Z
% 126.24/126.38 & host(Pid0) = host(Z) )
% 126.24/126.38 => ( ~ setIn(Z,alive)
% 126.24/126.38 | ~ setIn(Pid0,alive) ) )
% 126.24/126.38 & ! [Z] :
% 126.24/126.38 ( ( ( index(status,host(Z)) = elec_1
% 126.24/126.38 | index(status,host(Z)) = elec_2 )
% 126.24/126.38 & setIn(Z,alive) )
% 126.24/126.38 => index(elid,host(Z)) = Z )
% 126.24/126.38 & ! [Z,Pid0] :
% 126.24/126.38 ( ( setIn(Z,alive)
% 126.24/126.38 & setIn(Pid0,alive)
% 126.24/126.38 & setIn(host(Pid0),index(down,host(Z)))
% 126.24/126.38 & index(status,host(Pid0)) = elec_2 )
% 126.24/126.38 => leq(index(pendack,host(Pid0)),host(Z)) )
% 126.24/126.38 & ! [Z,Pid0] :
% 126.24/126.38 ( ( setIn(Pid0,alive)
% 126.24/126.38 & index(status,host(Pid0)) = norm
% 126.24/126.38 & index(ldr,host(Pid0)) = host(Pid0) )
% 126.24/126.38 => ~ ( setIn(Z,alive)
% 126.24/126.38 & setIn(host(Pid0),index(down,host(Z))) ) )
% 126.24/126.38 & ! [Z,Pid20,Pid0] :
% 126.24/126.38 ( ( setIn(Z,alive)
% 126.24/126.38 & setIn(Pid0,alive)
% 126.24/126.38 & elem(m_Down(Pid20),queue(host(Z)))
% 126.24/126.38 & host(Pid0) = host(Pid20)
% 126.24/126.38 & index(status,host(Pid0)) = elec_2 )
% 126.24/126.38 => leq(index(pendack,host(Pid0)),host(Z)) )
% 126.24/126.38 & ! [Z,Pid20,Pid0] :
% 126.24/126.38 ( ( setIn(Pid0,alive)
% 126.24/126.38 & host(Pid20) = host(Pid0)
% 126.24/126.38 & index(status,host(Pid0)) = norm
% 126.24/126.38 & index(ldr,host(Pid0)) = host(Pid0) )
% 126.24/126.38 => ~ ( setIn(Z,alive)
% 126.24/126.38 & elem(m_Down(Pid20),queue(host(Z))) ) )
% 126.24/126.38 & ! [Z,Pid0] :
% 126.24/126.38 ( ( setIn(Z,alive)
% 126.24/126.38 & setIn(Pid0,alive)
% 126.24/126.38 & index(ldr,host(Z)) = host(Z)
% 126.24/126.38 & index(status,host(Z)) = norm
% 126.24/126.38 & index(status,host(Pid0)) = norm
% 126.24/126.38 & index(ldr,host(Pid0)) = host(Pid0) )
% 126.24/126.38 => Pid0 = Z )
% 126.24/126.38 & ! [Z,Pid20,Pid0] :
% 126.24/126.38 ( ( ~ leq(host(Pid20),host(Pid0))
% 126.24/126.38 & setIn(Pid0,alive)
% 126.24/126.38 & elem(m_Down(Pid20),queue(host(Pid0)))
% 126.24/126.38 & host(Pid20) = host(Z) )
% 126.24/126.38 => ~ ( setIn(Z,alive)
% 126.24/126.38 & index(ldr,host(Z)) = host(Z)
% 126.24/126.38 & index(status,host(Z)) = norm ) )
% 126.24/126.38 & ! [Z,Pid30,Pid20,Pid0] :
% 126.24/126.38 ( ( host(Pid20) != host(Z)
% 126.24/126.38 & setIn(Z,alive)
% 126.24/126.38 & setIn(Pid20,alive)
% 126.24/126.38 & host(Pid30) = host(Z)
% 126.24/126.38 & host(Pid0) = host(Pid20) )
% 126.24/126.38 => ~ ( elem(m_Down(Pid0),queue(host(Z)))
% 126.24/126.38 & elem(m_Down(Pid30),queue(host(Pid20))) ) )
% 126.24/126.38 & ! [Z,Pid30,Pid20,Pid0] :
% 126.24/126.38 ( ( host(Pid20) != host(Z)
% 126.24/126.38 & setIn(Z,alive)
% 126.24/126.38 & setIn(Pid20,alive)
% 126.24/126.38 & host(Pid30) = host(Z)
% 126.24/126.38 & host(Pid0) = host(Pid20) )
% 126.24/126.38 => ~ ( elem(m_Down(Pid0),queue(host(Z)))
% 126.24/126.38 & setIn(host(Pid30),index(down,host(Pid20))) ) )
% 126.24/126.38 & ! [Z,Pid20,Pid0] :
% 126.24/126.38 ( ( host(Pid0) != host(Pid20)
% 126.24/126.38 & setIn(Pid0,alive)
% 126.24/126.38 & elem(m_Down(Z),queue(host(Pid0)))
% 126.24/126.38 & host(Pid20) = host(Z)
% 126.24/126.38 & index(status,host(Pid0)) = norm
% 126.24/126.38 & index(ldr,host(Pid0)) = host(Pid20) )
% 126.24/126.38 => ~ ( setIn(Pid20,alive)
% 126.24/126.38 & index(status,host(Pid20)) = norm
% 126.24/126.38 & index(ldr,host(Pid20)) = host(Pid20) ) )
% 126.24/126.38 & ! [Z,Pid20,Pid0] :
% 126.24/126.38 ( ( host(Pid0) != host(Pid20)
% 126.24/126.38 & setIn(Pid0,alive)
% 126.24/126.38 & elem(m_Down(Z),queue(host(Pid0)))
% 126.24/126.38 & host(Pid20) = host(Z)
% 126.24/126.38 & index(status,host(Pid0)) = wait
% 126.24/126.38 & host(index(elid,host(Pid0))) = host(Pid20) )
% 126.24/126.38 => ~ ( setIn(Pid20,alive)
% 126.24/126.38 & index(status,host(Pid20)) = norm
% 126.24/126.38 & index(ldr,host(Pid20)) = host(Pid20) ) )
% 126.24/126.38 & ! [Z,Pid30,Pid20,Pid0] :
% 126.24/126.38 ( ( ! [V0] :
% 126.24/126.38 ( ( ~ leq(host(Pid0),V0)
% 126.24/126.38 & leq(s(zero),V0) )
% 126.24/126.38 => ( setIn(V0,index(down,host(Pid0)))
% 126.24/126.38 | V0 = host(Pid20) ) )
% 126.24/126.38 & setIn(Z,alive)
% 126.24/126.38 & leq(host(Z),host(Pid0))
% 126.24/126.38 & elem(m_Down(Pid20),queue(host(Pid0)))
% 126.24/126.38 & host(Pid30) = host(Pid0)
% 126.24/126.38 & index(status,host(Z)) = elec_2
% 126.24/126.38 & index(status,host(Pid0)) = elec_1 )
% 126.24/126.38 => ~ elem(m_Ack(Z,Pid30),queue(host(Z))) )
% 126.24/126.38 & ! [Z,Pid30,Pid20,Pid0] :
% 126.24/126.38 ( ( ! [V0] :
% 126.24/126.38 ( ( ~ leq(host(Pid0),V0)
% 126.24/126.38 & leq(s(zero),V0) )
% 126.24/126.38 => ( setIn(V0,index(down,host(Pid0)))
% 126.24/126.38 | V0 = host(Pid20) ) )
% 126.24/126.38 & setIn(Pid0,alive)
% 126.24/126.38 & leq(nbr_proc,s(host(Pid0)))
% 126.24/126.38 & elem(m_Down(Pid20),queue(host(Pid0)))
% 126.24/126.38 & elem(m_Down(Pid30),queue(host(Pid0)))
% 126.24/126.38 & host(Pid30) = s(host(Pid0))
% 126.24/126.38 & index(status,host(Pid0)) = elec_1 )
% 126.24/126.38 => ~ ( setIn(Z,alive)
% 126.24/126.38 & index(ldr,host(Z)) = host(Z)
% 126.24/126.38 & index(status,host(Z)) = norm ) )
% 126.24/126.38 & queue(host(X)) = cons(m_Down(Y),V) )
% 126.24/126.38 => ( setIn(X,alive)
% 126.24/126.38 => ( leq(host(X),host(Y))
% 126.24/126.38 => ( ( index(status,host(X)) = elec_2
% 126.24/126.38 & host(Y) = index(pendack,host(X)) )
% 126.24/126.38 => ( leq(nbr_proc,index(pendack,host(X)))
% 126.24/126.38 => ! [Z] :
% 126.24/126.38 ( setIn(host(Z),index(acks,host(X)))
% 126.24/126.38 => ! [V0] :
% 126.24/126.38 ( host(X) = host(V0)
% 126.24/126.38 => ! [W0,X0,Y0] :
% 126.24/126.38 ( host(Z) != host(Y0)
% 126.24/126.38 => ( host(X) != host(Y0)
% 126.24/126.38 => ( ( ! [V1] :
% 126.24/126.38 ( ( ~ leq(host(Y0),V1)
% 126.24/126.38 & leq(s(zero),V1) )
% 126.24/126.38 => ( setIn(V1,index(down,host(Y0)))
% 126.24/126.38 | V1 = host(X0) ) )
% 126.24/126.38 & setIn(Y0,alive)
% 126.24/126.38 & leq(nbr_proc,s(host(Y0)))
% 126.24/126.38 & elem(m_Down(W0),queue(host(Y0)))
% 126.24/126.38 & elem(m_Down(X0),queue(host(Y0)))
% 126.24/126.38 & host(W0) = s(host(Y0))
% 126.24/126.38 & index(status,host(Y0)) = elec_1 )
% 126.24/126.38 => ~ ( setIn(V0,alive)
% 126.24/126.38 & host(X) = host(V0) ) ) ) ) ) ) ) ) ) ) ) ).
% 126.24/126.38
% 126.24/126.38 %------------------------------------------------------------------------------
% 126.24/126.38 %-------------------------------------------
% 126.24/126.38 % Proof found
% 126.24/126.38 % SZS status Theorem for theBenchmark
% 126.24/126.38 % SZS output start Proof
% 126.24/126.39 %ClaNum:187(EqnAxiom:54)
% 126.24/126.39 %VarNum:633(SingletonVarNum:295)
% 126.24/126.39 %MaxLitNum:11
% 126.24/126.39 %MaxfuncDepth:3
% 126.24/126.39 %SharedTerms:68
% 126.24/126.39 %goalClause: 57 58 61 62 63 65 66 68 70 73 76 77 82 83 84 92 93 154
% 126.24/126.39 %singleGoalClaCount:17
% 126.24/126.39 [55]P1(a1)
% 126.24/126.39 [61]P5(a2,a5)
% 126.24/126.39 [62]P5(a21,a5)
% 126.24/126.39 [63]P5(a3,a5)
% 126.24/126.39 [84]P4(a2,a22,a13)
% 126.24/126.39 [86]~E(a8,a7)
% 126.24/126.39 [87]~E(a48,a8)
% 126.24/126.39 [88]~E(a48,a7)
% 126.24/126.39 [89]~E(a38,a8)
% 126.24/126.39 [90]~E(a38,a7)
% 126.24/126.39 [91]~E(a48,a38)
% 126.24/126.39 [104]~P5(a39,a5)
% 126.24/126.39 [57]E(f20(a2),f20(a21))
% 126.24/126.39 [67]P2(f41(a46),a33)
% 126.24/126.39 [70]P2(f20(a2),f20(a22))
% 126.24/126.39 [92]~E(f20(a3),f20(a2))
% 126.24/126.39 [93]~E(f20(a23),f20(a3))
% 126.24/126.39 [58]E(f41(f20(a3)),f20(a4))
% 126.24/126.39 [65]E(f27(a43,f20(a2)),a7)
% 126.24/126.39 [66]E(f27(a43,f20(a3)),a8)
% 126.24/126.39 [68]E(f27(a37,f20(a2)),f20(a22))
% 126.24/126.39 [73]P2(a33,f41(f20(a3)))
% 126.24/126.39 [76]P3(f26(a4),f42(f20(a3)))
% 126.24/126.39 [77]P3(f26(a12),f42(f20(a3)))
% 126.24/126.39 [82]P2(a33,f27(a37,f20(a2)))
% 126.24/126.39 [83]P5(f20(a23),f27(a6,f20(a2)))
% 126.24/126.39 [64]P2(x641,x641)
% 126.24/126.39 [105]~P3(x1051,a1)
% 126.24/126.39 [106]~P5(x1061,a45)
% 126.24/126.39 [69]P2(f20(x691),a33)
% 126.24/126.39 [71]P2(f41(a46),f20(x711))
% 126.24/126.39 [72]E(f44(a1,x721),f9(x721,a1))
% 126.24/126.39 [74]P1(f9(x741,a1))
% 126.24/126.39 [75]P1(f44(a1,x751))
% 126.24/126.39 [114]~P2(f41(x1141),x1141)
% 126.24/126.39 [59]E(f32(f25(x591)),x591)
% 126.24/126.39 [60]E(f32(f26(x601)),x601)
% 126.24/126.39 [94]~E(f26(x941),f25(x942))
% 126.24/126.39 [95]~E(f34(x951),f26(x952))
% 126.24/126.39 [96]~E(f34(x961),f25(x962))
% 126.24/126.39 [97]~E(f35(x971),f26(x972))
% 126.24/126.39 [98]~E(f35(x981),f25(x982))
% 126.24/126.39 [99]~E(f35(x991),f34(x992))
% 126.24/126.39 [100]~E(f36(x1001),f26(x1002))
% 126.24/126.39 [101]~E(f36(x1011),f35(x1012))
% 126.24/126.39 [102]~E(f36(x1021),f25(x1022))
% 126.24/126.39 [103]~E(f36(x1031),f34(x1032))
% 126.24/126.39 [107]~E(f9(x1071,x1072),a1)
% 126.24/126.39 [108]~E(f44(x1081,x1082),a1)
% 126.24/126.39 [78]E(f24(f9(x781,x782)),x781)
% 126.24/126.39 [79]E(f47(f9(x791,x792)),x792)
% 126.24/126.39 [80]E(f28(f44(x801,x802)),x802)
% 126.24/126.39 [81]E(f29(f44(x811,x812)),x811)
% 126.24/126.39 [109]~E(f30(x1091,x1092),f25(x1093))
% 126.24/126.39 [110]~E(f30(x1101,x1102),f26(x1103))
% 126.24/126.39 [111]~E(f30(x1111,x1112),f34(x1113))
% 126.24/126.39 [112]~E(f30(x1121,x1122),f35(x1123))
% 126.24/126.39 [113]~E(f30(x1131,x1132),f36(x1133))
% 126.24/126.39 [85]E(f44(f9(x851,x852),x853),f9(x851,f44(x852,x853)))
% 126.24/126.39 [124]E(x1241,a1)+E(f9(f24(x1241),f47(x1241)),x1241)
% 126.24/126.39 [125]E(x1251,a1)+E(f44(f29(x1251),f28(x1251)),x1251)
% 126.24/126.39 [123]~E(x1231,x1232)+P2(x1231,x1232)
% 126.24/126.39 [126]P2(x1262,x1261)+P2(x1261,x1262)
% 126.24/126.39 [115]P6(x1151)+~E(x1151,f25(x1152))
% 126.24/126.39 [116]P6(x1161)+~E(x1161,f26(x1162))
% 126.24/126.39 [117]E(x1171,x1172)+~E(f25(x1171),f25(x1172))
% 126.24/126.39 [118]E(x1181,x1182)+~E(f26(x1181),f26(x1182))
% 126.24/126.39 [119]E(x1191,x1192)+~E(f34(x1191),f34(x1192))
% 126.24/126.39 [120]E(x1201,x1202)+~E(f35(x1201),f35(x1202))
% 126.24/126.39 [121]E(x1211,x1212)+~E(f36(x1211),f36(x1212))
% 126.24/126.39 [132]~P2(x1321,x1322)+P2(x1321,f41(x1322))
% 126.24/126.39 [138]~P2(x1381,x1382)+P2(f41(x1381),f41(x1382))
% 126.24/126.39 [141]P1(x1411)+~P1(f9(x1412,x1411))
% 126.24/126.39 [142]P1(x1421)+~P1(f44(x1421,x1422))
% 126.24/126.39 [143]P2(x1431,x1432)+~P2(f41(x1431),f41(x1432))
% 126.24/126.39 [129]~E(f20(x1291),f20(x1292))+~E(f41(f20(x1291)),f20(x1292))
% 126.24/126.39 [139]~P1(x1391)+P1(f44(x1391,f35(x1392)))
% 126.24/126.39 [155]P5(x1551,a40)+~P3(f30(x1552,x1551),f42(f20(x1552)))
% 126.24/126.39 [156]P5(x1561,a40)+~P3(f30(x1561,x1562),f42(f20(x1561)))
% 126.24/126.39 [133]~E(x1331,x1332)+P3(x1331,f9(x1332,x1333))
% 126.24/126.39 [134]~E(x1341,x1343)+P3(x1341,f44(x1342,x1343))
% 126.24/126.39 [145]~P3(x1451,x1453)+P3(x1451,f9(x1452,x1453))
% 126.24/126.39 [146]~P3(x1461,x1462)+P3(x1461,f44(x1462,x1463))
% 126.24/126.39 [153]~P1(x1531)+P1(f44(x1531,f30(x1532,x1533)))
% 126.24/126.39 [159]~P4(x1591,x1592,x1593)+E(f42(f20(x1591)),f9(f26(x1592),x1593))
% 126.24/126.39 [135]E(x1351,x1352)+~E(f30(x1353,x1351),f30(x1354,x1352))
% 126.24/126.39 [136]E(x1361,x1362)+~E(f30(x1361,x1363),f30(x1362,x1364))
% 126.24/126.39 [128]~P6(x1281)+E(f26(f17(x1281)),x1281)+E(f25(f14(x1281)),x1281)
% 126.24/126.39 [137]~P2(x1372,x1371)+~P2(x1371,x1372)+E(x1371,x1372)
% 126.24/126.39 [130]~P1(x1302)+P6(x1301)+P1(f9(x1301,x1302))
% 126.24/126.39 [131]~P1(x1312)+P6(x1311)+P1(f44(x1312,x1311))
% 126.24/126.39 [140]P2(x1401,x1402)+E(x1401,f41(x1402))+~P2(x1401,f41(x1402))
% 126.24/126.39 [147]~P1(x1472)+P1(f9(x1471,x1472))+P6(f18(x1471,x1472))
% 126.24/126.39 [148]~P1(x1482)+P1(f44(x1482,x1481))+P6(f19(x1481,x1482))
% 126.24/126.39 [149]~P1(x1492)+P3(f18(x1491,x1492),x1492)+P1(f9(x1491,x1492))
% 126.24/126.39 [150]~P1(x1501)+P3(f19(x1502,x1501),x1501)+P1(f44(x1501,x1502))
% 126.24/126.39 [167]~P1(x1672)+~P2(f32(x1671),f32(f18(x1671,x1672)))+P1(f9(x1671,x1672))
% 126.24/126.39 [168]~P1(x1681)+~P2(f32(f19(x1682,x1681)),f32(x1682))+P1(f44(x1681,x1682))
% 126.24/126.39 [157]~P1(x1572)+P1(f9(x1571,x1572))+E(f20(f32(f18(x1571,x1572))),f20(f32(x1571)))
% 126.24/126.39 [158]~P1(x1582)+P1(f44(x1582,x1581))+E(f20(f32(f19(x1581,x1582))),f20(f32(x1581)))
% 126.24/126.39 [144]~P2(x1441,x1443)+P2(x1441,x1442)+~P2(x1443,x1442)
% 126.24/126.39 [151]E(x1511,x1512)+P3(x1511,x1513)+~P3(x1511,f44(x1513,x1512))
% 126.24/126.39 [152]E(x1521,x1522)+P3(x1521,x1523)+~P3(x1521,f9(x1522,x1523))
% 126.24/126.39 [166]~P4(x1663,x1664,x1665)+~E(f20(x1661),f20(x1662))+~P3(f26(x1661),f42(f20(x1662)))
% 126.24/126.39 [169]~P4(x1691,x1692,x1693)+~P2(f20(x1694),f20(x1695))+~P3(f35(x1695),f42(f20(x1694)))
% 126.24/126.39 [154]P2(f20(a3),x1541)+~P2(f41(a46),x1541)+E(x1541,f20(a12))+P5(x1541,f27(a10,f20(a3)))
% 126.24/126.39 [160]P2(x1601,x1602)+~E(f20(x1601),f20(x1602))+~P3(f26(x1602),x1603)+~P1(f9(f25(x1601),x1603))
% 126.24/126.39 [164]~P4(x1642,x1643,x1644)+~P5(x1641,a5)+E(f27(a11,f20(x1641)),x1641)+~E(f27(a43,f20(x1641)),a8)
% 126.24/126.39 [165]~P4(x1652,x1653,x1654)+~P5(x1651,a5)+E(f27(a11,f20(x1651)),x1651)+~E(f27(a43,f20(x1651)),a7)
% 126.24/126.39 [161]E(x1611,x1612)+~P4(x1613,x1614,x1615)+~E(f20(x1611),f20(x1612))+~P5(x1612,a5)+~P5(x1611,a5)
% 126.24/126.39 [162]~P6(x1621)+~P6(x1622)+~P3(x1622,x1623)+P2(f32(x1621),f32(x1622))+~P1(f9(x1621,x1623))+~E(f20(f32(x1622)),f20(f32(x1621)))
% 126.24/126.39 [163]~P6(x1632)+~P6(x1631)+~P3(x1631,x1633)+P2(f32(x1631),f32(x1632))+~P1(f44(x1633,x1632))+~E(f20(f32(x1631)),f20(f32(x1632)))
% 126.24/126.39 [172]~P4(x1723,x1724,x1725)+~P5(x1721,a5)+~P5(x1722,a5)+~E(f27(a31,f20(x1721)),f20(x1721))+~P5(f20(x1721),f27(a10,f20(x1722)))+~E(f27(a43,f20(x1721)),a38)
% 126.24/126.39 [176]~P4(x1763,x1764,x1765)+~P5(x1761,a5)+~P5(x1762,a5)+P2(f27(a37,f20(x1761)),f20(x1762))+~P5(f20(x1761),f27(a10,f20(x1762)))+~E(f27(a43,f20(x1761)),a7)
% 126.24/126.39 [171]~P4(x1714,x1715,x1716)+~P5(x1711,a5)+~E(f20(x1711),f20(x1712))+~P5(x1713,a5)+~P3(f26(x1712),f42(f20(x1713)))+~E(f27(a31,f20(x1711)),f20(x1711))+~E(f27(a43,f20(x1711)),a38)
% 126.24/126.39 [174]~P4(x1744,x1745,x1746)+~P5(x1741,a5)+~P5(x1742,a5)+~E(f20(x1741),f20(x1743))+~P3(f26(x1743),f42(f20(x1742)))+P2(f27(a37,f20(x1741)),f20(x1742))+~E(f27(a43,f20(x1741)),a7)
% 126.24/126.39 [170]E(x1701,x1702)+~P4(x1703,x1704,x1705)+~P5(x1702,a5)+~P5(x1701,a5)+~E(f27(a31,f20(x1702)),f20(x1702))+~E(f27(a31,f20(x1701)),f20(x1701))+~E(f27(a43,f20(x1702)),a38)+~E(f27(a43,f20(x1701)),a38)
% 126.24/126.39 [175]~P4(x1754,x1755,x1756)+~P5(x1753,a5)+~P5(x1752,a5)+P2(f20(x1751),f20(x1752))+~E(f20(x1751),f20(x1753))+~P3(f26(x1751),f42(f20(x1752)))+~E(f27(a31,f20(x1753)),f20(x1753))+~E(f27(a43,f20(x1753)),a38)
% 126.24/126.39 [173]~P4(x1735,x1736,x1737)+~P5(x1732,a5)+~P5(x1731,a5)+E(f20(x1731),f20(x1732))+~E(f20(x1732),f20(x1733))+~E(f20(x1731),f20(x1734))+~P3(f26(x1733),f42(f20(x1731)))+~P3(f26(x1734),f42(f20(x1732)))
% 126.24/126.39 [177]~P4(x1775,x1776,x1777)+~P5(x1772,a5)+~P5(x1771,a5)+E(f20(x1771),f20(x1772))+~E(f20(x1772),f20(x1773))+~E(f20(x1771),f20(x1774))+~P3(f26(x1774),f42(f20(x1772)))+~P5(f20(x1773),f27(a10,f20(x1771)))
% 126.24/126.39 [184]~P4(x1846,x1845,x1844)+~P5(x1843,a5)+~E(f16(x1844,x1845,x1846,x1843,x1841,x1847,x1842),f20(x1847))+~E(f20(x1841),f20(x1842))+~P2(f20(x1843),f20(x1842))+~P3(f26(x1847),f42(f20(x1842)))+~P3(f30(x1843,x1841),f42(f20(x1843)))+~E(f27(a43,f20(x1842)),a8)+~E(f27(a43,f20(x1843)),a7)
% 126.24/126.39 [185]~P4(x1853,x1852,x1851)+~E(f20(x1855),f20(x1857))+~P5(x1854,a5)+~P2(f20(x1854),f20(x1857))+P2(f41(a46),f16(x1851,x1852,x1853,x1854,x1855,x1856,x1857))+~P3(f26(x1856),f42(f20(x1857)))+~P3(f30(x1854,x1855),f42(f20(x1854)))+~E(f27(a43,f20(x1857)),a8)+~E(f27(a43,f20(x1854)),a7)
% 126.24/126.39 [186]~P4(x1864,x1865,x1866)+~P5(x1863,a5)+~P2(f20(x1861),f16(x1866,x1865,x1864,x1863,x1862,x1867,x1861))+~E(f20(x1861),f20(x1862))+~P2(f20(x1863),f20(x1861))+~P3(f30(x1863,x1862),f42(f20(x1863)))+~P3(f26(x1867),f42(f20(x1861)))+~E(f27(a43,f20(x1861)),a8)+~E(f27(a43,f20(x1863)),a7)
% 126.24/126.39 [187]~P4(x1874,x1875,x1876)+~P5(x1873,a5)+~E(f20(x1871),f20(x1872))+~P2(f20(x1873),f20(x1872))+~P3(f30(x1873,x1871),f42(f20(x1873)))+~P3(f26(x1877),f42(f20(x1872)))+~P5(f16(x1876,x1875,x1874,x1873,x1871,x1877,x1872),f27(a10,f20(x1872)))+~E(f27(a43,f20(x1872)),a8)+~E(f27(a43,f20(x1873)),a7)
% 126.24/126.39 [180]~P4(x1806,x1805,x1804)+~P5(x1803,a5)+~P5(x1802,a5)+~E(f15(x1804,x1805,x1806,x1801,x1807,x1802),f20(x1807))+~E(f20(x1801),f41(f20(x1802)))+~P3(f26(x1807),f42(f20(x1802)))+~P3(f26(x1801),f42(f20(x1802)))+~E(f27(a31,f20(x1803)),f20(x1803))+~P2(a33,f41(f20(x1802)))+~E(f27(a43,f20(x1802)),a8)+~E(f27(a43,f20(x1803)),a38)
% 126.24/126.39 [181]~P4(x1813,x1812,x1811)+~P5(x1817,a5)+~P5(x1816,a5)+P2(f41(a46),f15(x1811,x1812,x1813,x1814,x1815,x1816))+~E(f20(x1814),f41(f20(x1816)))+~P3(f26(x1815),f42(f20(x1816)))+~P3(f26(x1814),f42(f20(x1816)))+~E(f27(a31,f20(x1817)),f20(x1817))+~P2(a33,f41(f20(x1816)))+~E(f27(a43,f20(x1816)),a8)+~E(f27(a43,f20(x1817)),a38)
% 126.24/126.39 [182]~P4(x1824,x1825,x1826)+~P5(x1823,a5)+~P5(x1822,a5)+~P2(f20(x1822),f15(x1826,x1825,x1824,x1821,x1827,x1822))+~E(f20(x1821),f41(f20(x1822)))+~P3(f26(x1821),f42(f20(x1822)))+~P3(f26(x1827),f42(f20(x1822)))+~E(f27(a31,f20(x1823)),f20(x1823))+~P2(a33,f41(f20(x1822)))+~E(f27(a43,f20(x1822)),a8)+~E(f27(a43,f20(x1823)),a38)
% 126.24/126.39 [183]~P4(x1834,x1835,x1836)+~P5(x1833,a5)+~P5(x1832,a5)+~E(f20(x1831),f41(f20(x1832)))+~P3(f26(x1831),f42(f20(x1832)))+~P3(f26(x1837),f42(f20(x1832)))+~P5(f15(x1836,x1835,x1834,x1831,x1837,x1832),f27(a10,f20(x1832)))+~E(f27(a31,f20(x1833)),f20(x1833))+~P2(a33,f41(f20(x1832)))+~E(f27(a43,f20(x1832)),a8)+~E(f27(a43,f20(x1833)),a38)
% 126.24/126.39 %EqnAxiom
% 126.24/126.39 [1]E(x11,x11)
% 126.24/126.39 [2]E(x22,x21)+~E(x21,x22)
% 126.24/126.39 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 126.24/126.39 [4]~E(x41,x42)+E(f20(x41),f20(x42))
% 126.24/126.39 [5]~E(x51,x52)+E(f27(x51,x53),f27(x52,x53))
% 126.24/126.39 [6]~E(x61,x62)+E(f27(x63,x61),f27(x63,x62))
% 126.24/126.39 [7]~E(x71,x72)+E(f16(x71,x73,x74,x75,x76,x77,x78),f16(x72,x73,x74,x75,x76,x77,x78))
% 126.24/126.39 [8]~E(x81,x82)+E(f16(x83,x81,x84,x85,x86,x87,x88),f16(x83,x82,x84,x85,x86,x87,x88))
% 126.24/126.39 [9]~E(x91,x92)+E(f16(x93,x94,x91,x95,x96,x97,x98),f16(x93,x94,x92,x95,x96,x97,x98))
% 126.24/126.39 [10]~E(x101,x102)+E(f16(x103,x104,x105,x101,x106,x107,x108),f16(x103,x104,x105,x102,x106,x107,x108))
% 126.24/126.39 [11]~E(x111,x112)+E(f16(x113,x114,x115,x116,x111,x117,x118),f16(x113,x114,x115,x116,x112,x117,x118))
% 126.24/126.39 [12]~E(x121,x122)+E(f16(x123,x124,x125,x126,x127,x121,x128),f16(x123,x124,x125,x126,x127,x122,x128))
% 126.24/126.39 [13]~E(x131,x132)+E(f16(x133,x134,x135,x136,x137,x138,x131),f16(x133,x134,x135,x136,x137,x138,x132))
% 126.24/126.39 [14]~E(x141,x142)+E(f42(x141),f42(x142))
% 126.24/126.39 [15]~E(x151,x152)+E(f30(x151,x153),f30(x152,x153))
% 126.24/126.39 [16]~E(x161,x162)+E(f30(x163,x161),f30(x163,x162))
% 126.24/126.39 [17]~E(x171,x172)+E(f41(x171),f41(x172))
% 126.24/126.39 [18]~E(x181,x182)+E(f26(x181),f26(x182))
% 126.24/126.39 [19]~E(x191,x192)+E(f25(x191),f25(x192))
% 126.24/126.39 [20]~E(x201,x202)+E(f32(x201),f32(x202))
% 126.24/126.39 [21]~E(x211,x212)+E(f44(x211,x213),f44(x212,x213))
% 126.24/126.39 [22]~E(x221,x222)+E(f44(x223,x221),f44(x223,x222))
% 126.24/126.39 [23]~E(x231,x232)+E(f14(x231),f14(x232))
% 126.24/126.39 [24]~E(x241,x242)+E(f17(x241),f17(x242))
% 126.24/126.39 [25]~E(x251,x252)+E(f9(x251,x253),f9(x252,x253))
% 126.24/126.39 [26]~E(x261,x262)+E(f9(x263,x261),f9(x263,x262))
% 126.24/126.39 [27]~E(x271,x272)+E(f35(x271),f35(x272))
% 126.24/126.39 [28]~E(x281,x282)+E(f36(x281),f36(x282))
% 126.24/126.39 [29]~E(x291,x292)+E(f15(x291,x293,x294,x295,x296,x297),f15(x292,x293,x294,x295,x296,x297))
% 126.24/126.39 [30]~E(x301,x302)+E(f15(x303,x301,x304,x305,x306,x307),f15(x303,x302,x304,x305,x306,x307))
% 126.24/126.39 [31]~E(x311,x312)+E(f15(x313,x314,x311,x315,x316,x317),f15(x313,x314,x312,x315,x316,x317))
% 126.24/126.39 [32]~E(x321,x322)+E(f15(x323,x324,x325,x321,x326,x327),f15(x323,x324,x325,x322,x326,x327))
% 126.24/126.39 [33]~E(x331,x332)+E(f15(x333,x334,x335,x336,x331,x337),f15(x333,x334,x335,x336,x332,x337))
% 126.24/126.39 [34]~E(x341,x342)+E(f15(x343,x344,x345,x346,x347,x341),f15(x343,x344,x345,x346,x347,x342))
% 126.24/126.39 [35]~E(x351,x352)+E(f19(x351,x353),f19(x352,x353))
% 126.24/126.39 [36]~E(x361,x362)+E(f19(x363,x361),f19(x363,x362))
% 126.24/126.39 [37]~E(x371,x372)+E(f34(x371),f34(x372))
% 126.24/126.39 [38]~E(x381,x382)+E(f47(x381),f47(x382))
% 126.24/126.39 [39]~E(x391,x392)+E(f28(x391),f28(x392))
% 126.24/126.39 [40]~E(x401,x402)+E(f18(x401,x403),f18(x402,x403))
% 126.24/126.39 [41]~E(x411,x412)+E(f18(x413,x411),f18(x413,x412))
% 126.24/126.39 [42]~E(x421,x422)+E(f24(x421),f24(x422))
% 126.24/126.39 [43]~E(x431,x432)+E(f29(x431),f29(x432))
% 126.24/126.39 [44]~P1(x441)+P1(x442)+~E(x441,x442)
% 126.24/126.39 [45]P5(x452,x453)+~E(x451,x452)+~P5(x451,x453)
% 126.24/126.39 [46]P5(x463,x462)+~E(x461,x462)+~P5(x463,x461)
% 126.24/126.39 [47]P2(x472,x473)+~E(x471,x472)+~P2(x471,x473)
% 126.24/126.39 [48]P2(x483,x482)+~E(x481,x482)+~P2(x483,x481)
% 126.24/126.39 [49]P4(x492,x493,x494)+~E(x491,x492)+~P4(x491,x493,x494)
% 126.24/126.39 [50]P4(x503,x502,x504)+~E(x501,x502)+~P4(x503,x501,x504)
% 126.24/126.39 [51]P4(x513,x514,x512)+~E(x511,x512)+~P4(x513,x514,x511)
% 126.24/126.39 [52]P3(x522,x523)+~E(x521,x522)+~P3(x521,x523)
% 126.24/126.39 [53]P3(x533,x532)+~E(x531,x532)+~P3(x533,x531)
% 126.24/126.39 [54]~P6(x541)+P6(x542)+~E(x541,x542)
% 126.24/126.39
% 126.24/126.39 %-------------------------------------------
% 126.35/126.42 cnf(188,plain,
% 126.35/126.42 (P6(f25(x1881))),
% 126.35/126.42 inference(equality_inference,[],[115])).
% 126.35/126.42 cnf(196,plain,
% 126.35/126.42 (P3(x1961,f9(x1961,x1962))),
% 126.35/126.42 inference(equality_inference,[],[133])).
% 126.35/126.42 cnf(197,plain,
% 126.35/126.42 (P3(x1971,f44(x1972,x1971))),
% 126.35/126.42 inference(equality_inference,[],[134])).
% 126.35/126.42 cnf(204,plain,
% 126.35/126.42 (~P4(x2041,x2042,x2043)+~P3(f26(x2044),f42(f20(x2044)))),
% 126.35/126.42 inference(equality_inference,[],[166])).
% 126.35/126.42 cnf(205,plain,
% 126.35/126.42 (~P3(f26(x2051),f42(f20(x2051)))),
% 126.35/126.42 inference(scs_inference,[],[84,204])).
% 126.35/126.42 cnf(206,plain,
% 126.35/126.42 (~E(f41(x2061),x2061)),
% 126.35/126.42 inference(scs_inference,[],[114,123])).
% 126.35/126.42 cnf(208,plain,
% 126.35/126.42 (~E(f20(a3),f20(a4))),
% 126.35/126.42 inference(scs_inference,[],[58,114,123,129])).
% 126.35/126.42 cnf(210,plain,
% 126.35/126.42 (E(f20(a21),f20(a2))),
% 126.35/126.42 inference(scs_inference,[],[57,58,114,123,129,2])).
% 126.35/126.42 cnf(211,plain,
% 126.35/126.42 (~E(a3,a2)),
% 126.35/126.42 inference(scs_inference,[],[57,92,58,114,123,129,2,4])).
% 126.35/126.42 cnf(213,plain,
% 126.35/126.42 (E(f32(f25(x2131)),x2131)),
% 126.35/126.42 inference(rename_variables,[],[59])).
% 126.35/126.42 cnf(216,plain,
% 126.35/126.42 (E(f32(f25(x2161)),x2161)),
% 126.35/126.42 inference(rename_variables,[],[59])).
% 126.35/126.42 cnf(218,plain,
% 126.35/126.42 (P2(x2181,f41(x2181))),
% 126.35/126.42 inference(scs_inference,[],[57,92,58,114,59,213,123,129,2,4,115,116,126])).
% 126.35/126.42 cnf(220,plain,
% 126.35/126.42 (~P2(f41(f41(x2201)),x2201)),
% 126.35/126.42 inference(scs_inference,[],[57,92,58,114,59,213,123,129,2,4,115,116,126,132])).
% 126.35/126.42 cnf(221,plain,
% 126.35/126.42 (~P2(f41(x2211),x2211)),
% 126.35/126.42 inference(rename_variables,[],[114])).
% 126.35/126.42 cnf(225,plain,
% 126.35/126.42 (E(f32(f25(f20(a2))),f20(a21))),
% 126.35/126.42 inference(scs_inference,[],[57,84,92,58,76,114,59,213,216,123,129,2,4,115,116,126,132,166,3])).
% 126.35/126.42 cnf(227,plain,
% 126.35/126.42 (~E(a2,a39)),
% 126.35/126.42 inference(scs_inference,[],[57,61,84,92,58,76,114,104,59,213,216,123,129,2,4,115,116,126,132,166,3,45])).
% 126.35/126.42 cnf(228,plain,
% 126.35/126.42 (~E(a5,a45)),
% 126.35/126.42 inference(scs_inference,[],[57,61,84,92,58,76,106,114,104,59,213,216,123,129,2,4,115,116,126,132,166,3,45,46])).
% 126.35/126.42 cnf(230,plain,
% 126.35/126.42 (~E(f20(a2),f41(f20(a22)))),
% 126.35/126.42 inference(scs_inference,[],[57,61,84,70,92,58,76,106,114,221,104,59,213,216,123,129,2,4,115,116,126,132,166,3,45,46,47])).
% 126.35/126.42 cnf(232,plain,
% 126.35/126.42 (P2(a33,f20(a22))),
% 126.35/126.42 inference(scs_inference,[],[57,61,84,70,92,58,76,68,82,106,114,221,104,59,213,216,123,129,2,4,115,116,126,132,166,3,45,46,47,48])).
% 126.35/126.42 cnf(235,plain,
% 126.35/126.42 (E(f25(f14(f25(x2351))),f25(x2351))),
% 126.35/126.42 inference(scs_inference,[],[57,61,84,70,92,58,76,68,82,196,188,106,114,221,94,104,59,213,216,123,129,2,4,115,116,126,132,166,3,45,46,47,48,52,128])).
% 126.35/126.42 cnf(238,plain,
% 126.35/126.42 (E(f20(a22),a33)),
% 126.35/126.42 inference(scs_inference,[],[57,61,84,70,92,58,76,68,82,196,188,106,114,221,94,104,69,59,213,216,123,129,2,4,115,116,126,132,166,3,45,46,47,48,52,128,137])).
% 126.35/126.42 cnf(241,plain,
% 126.35/126.42 (P2(a33,f41(f41(f20(a3))))),
% 126.35/126.42 inference(scs_inference,[],[57,61,84,70,92,58,76,68,82,73,196,188,106,114,221,94,104,69,59,213,216,123,129,2,4,115,116,126,132,166,3,45,46,47,48,52,128,137,144])).
% 126.35/126.42 cnf(245,plain,
% 126.35/126.42 (E(f27(a11,f20(a3)),a3)),
% 126.35/126.42 inference(scs_inference,[],[57,61,63,84,70,92,58,76,68,82,73,66,196,188,105,106,114,221,94,104,69,59,213,216,123,129,2,4,115,116,126,132,166,3,45,46,47,48,52,128,137,144,53,164])).
% 126.35/126.42 cnf(247,plain,
% 126.35/126.42 (E(f27(a11,f20(a2)),a2)),
% 126.35/126.42 inference(scs_inference,[],[57,61,63,84,70,92,58,76,68,82,73,65,66,196,188,105,106,114,221,94,104,69,59,213,216,123,129,2,4,115,116,126,132,166,3,45,46,47,48,52,128,137,144,53,164,165])).
% 126.35/126.42 cnf(249,plain,
% 126.35/126.42 (E(a2,a21)),
% 126.35/126.42 inference(scs_inference,[],[57,61,62,63,84,70,92,58,76,68,82,73,65,66,196,188,105,106,114,221,94,104,69,59,213,216,123,129,2,4,115,116,126,132,166,3,45,46,47,48,52,128,137,144,53,164,165,161])).
% 126.35/126.42 cnf(251,plain,
% 126.35/126.42 (E(f14(f25(x2511)),x2511)),
% 126.35/126.42 inference(scs_inference,[],[57,61,62,63,84,70,92,58,76,68,82,73,65,66,196,188,105,106,114,221,94,104,69,59,213,216,123,129,2,4,115,116,126,132,166,3,45,46,47,48,52,128,137,144,53,164,165,161,117])).
% 126.35/126.42 cnf(254,plain,
% 126.35/126.42 (P4(a21,a22,a13)),
% 126.35/126.42 inference(scs_inference,[],[57,61,62,63,84,70,92,58,76,68,82,73,65,66,196,188,105,106,114,221,94,104,69,59,213,216,123,129,2,4,115,116,126,132,166,3,45,46,47,48,52,128,137,144,53,164,165,161,117,44,49])).
% 126.35/126.42 cnf(263,plain,
% 126.35/126.42 (E(x2631,x2632)+~E(f20(x2631),f20(x2632))+~P5(x2632,a5)+~P5(x2631,a5)),
% 126.35/126.42 inference(scs_inference,[],[84,161])).
% 126.35/126.42 cnf(266,plain,
% 126.35/126.42 (~E(f20(x2661),f20(x2662))+~P3(f26(x2661),f42(f20(x2662)))),
% 126.35/126.42 inference(scs_inference,[],[84,166])).
% 126.35/126.42 cnf(267,plain,
% 126.35/126.42 (~P2(f20(x2671),f20(x2672))+~P3(f35(x2672),f42(f20(x2671)))),
% 126.35/126.42 inference(scs_inference,[],[84,169])).
% 126.35/126.42 cnf(272,plain,
% 126.35/126.42 (~E(f20(x2721),f20(x2722))+~P5(x2721,a5)+~P5(x2723,a5)+~P3(f26(x2722),f42(f20(x2723)))+P2(f27(a37,f20(x2721)),f20(x2723))+~E(f27(a43,f20(x2721)),a7)),
% 126.35/126.42 inference(scs_inference,[],[84,174])).
% 126.35/126.42 cnf(274,plain,
% 126.35/126.42 (~P5(x2741,a5)+~P5(x2742,a5)+P2(f27(a37,f20(x2741)),f20(x2742))+~P5(f20(x2741),f27(a10,f20(x2742)))+~E(f27(a43,f20(x2741)),a7)),
% 126.35/126.42 inference(scs_inference,[],[84,176])).
% 126.35/126.42 cnf(276,plain,
% 126.35/126.42 (~P3(f26(a2),f42(f20(a21)))),
% 126.35/126.42 inference(scs_inference,[],[57,266])).
% 126.35/126.42 cnf(278,plain,
% 126.35/126.42 (P2(x2781,f41(f41(x2781)))),
% 126.35/126.42 inference(scs_inference,[],[57,220,266,126])).
% 126.35/126.42 cnf(280,plain,
% 126.35/126.42 (~P2(f41(f41(f41(x2801))),x2801)),
% 126.35/126.42 inference(scs_inference,[],[57,220,266,126,132])).
% 126.35/126.42 cnf(281,plain,
% 126.35/126.42 (~P2(f41(f41(x2811)),x2811)),
% 126.35/126.42 inference(rename_variables,[],[220])).
% 126.35/126.42 cnf(283,plain,
% 126.35/126.42 (~E(f41(f41(x2831)),x2831)),
% 126.35/126.42 inference(scs_inference,[],[57,220,281,266,126,132,123])).
% 126.35/126.42 cnf(286,plain,
% 126.35/126.42 (E(f14(f25(x2861)),x2861)),
% 126.35/126.42 inference(rename_variables,[],[251])).
% 126.35/126.42 cnf(291,plain,
% 126.35/126.42 (~E(a23,a3)),
% 126.35/126.42 inference(scs_inference,[],[57,93,220,281,251,286,266,126,132,123,116,115,4])).
% 126.35/126.42 cnf(293,plain,
% 126.35/126.42 (P2(f20(a2),f41(f20(a22)))),
% 126.35/126.42 inference(scs_inference,[],[57,93,70,58,218,220,281,251,286,266,126,132,123,116,115,4,2,144])).
% 126.35/126.42 cnf(297,plain,
% 126.35/126.42 (~P3(f26(x2971),f42(f20(x2971)))),
% 126.35/126.42 inference(rename_variables,[],[205])).
% 126.35/126.42 cnf(298,plain,
% 126.35/126.42 (E(a33,f20(a22))),
% 126.35/126.42 inference(scs_inference,[],[57,93,77,70,58,218,205,232,220,281,251,286,69,266,126,132,123,116,115,4,2,144,52,137])).
% 126.35/126.42 cnf(303,plain,
% 126.35/126.42 (P2(a33,f20(a4))),
% 126.35/126.42 inference(scs_inference,[],[57,93,77,70,58,73,218,205,297,232,220,281,251,286,69,266,126,132,123,116,115,4,2,144,52,137,53,48])).
% 126.35/126.42 cnf(304,plain,
% 126.35/126.42 (~E(f41(f20(a21)),f20(a2))),
% 126.35/126.42 inference(scs_inference,[],[57,93,77,70,58,73,206,218,205,297,232,220,281,251,286,69,266,126,132,123,116,115,4,2,144,52,137,53,48,3])).
% 126.35/126.42 cnf(310,plain,
% 126.35/126.42 (~E(a21,a39)),
% 126.35/126.42 inference(scs_inference,[],[57,93,77,83,70,62,58,73,206,218,205,297,232,220,281,251,286,106,104,69,266,126,132,123,116,115,4,2,144,52,137,53,48,3,46,47,45])).
% 126.35/126.42 cnf(311,plain,
% 126.35/126.42 (~E(f20(a3),f20(a12))),
% 126.35/126.42 inference(scs_inference,[],[57,93,77,83,70,62,58,73,206,218,205,297,232,220,281,251,286,106,104,69,266,126,132,123,116,115,4,2,144,52,137,53,48,3,46,47,45,14])).
% 126.35/126.42 cnf(312,plain,
% 126.35/126.42 (~E(a12,a3)),
% 126.35/126.42 inference(scs_inference,[],[57,93,77,83,70,62,58,73,206,218,205,297,232,220,281,251,286,106,104,69,266,126,132,123,116,115,4,2,144,52,137,53,48,3,46,47,45,14,18])).
% 126.35/126.42 cnf(317,plain,
% 126.35/126.42 (P4(x3171,a22,a13)+~E(a21,x3171)),
% 126.35/126.42 inference(scs_inference,[],[57,93,77,83,70,62,58,73,206,218,205,297,232,254,220,281,251,286,106,104,69,266,126,132,123,116,115,4,2,144,52,137,53,48,3,46,47,45,14,18,54,51,50,44,49])).
% 126.35/126.42 cnf(326,plain,
% 126.35/126.42 (~P3(f26(a21),f42(f20(a2)))),
% 126.35/126.42 inference(scs_inference,[],[210,266])).
% 126.35/126.42 cnf(328,plain,
% 126.35/126.42 (P2(x3281,f41(f41(f41(x3281))))),
% 126.35/126.42 inference(scs_inference,[],[210,280,266,126])).
% 126.35/126.42 cnf(330,plain,
% 126.35/126.42 (~E(f41(f41(f41(x3301))),x3301)),
% 126.35/126.42 inference(scs_inference,[],[210,280,266,126,123])).
% 126.35/126.42 cnf(333,plain,
% 126.35/126.42 (E(f32(f26(x3331)),x3331)),
% 126.35/126.42 inference(rename_variables,[],[60])).
% 126.35/126.42 cnf(338,plain,
% 126.35/126.42 (~E(a3,a4)),
% 126.35/126.42 inference(scs_inference,[],[210,208,280,60,333,266,126,123,116,115,4])).
% 126.35/126.42 cnf(339,plain,
% 126.35/126.42 (E(a8,f27(a43,f20(a3)))),
% 126.35/126.42 inference(scs_inference,[],[66,210,208,280,60,333,266,126,123,116,115,4,2])).
% 126.35/126.42 cnf(340,plain,
% 126.35/126.42 (P2(a33,f41(f27(a37,f20(a2))))),
% 126.35/126.42 inference(scs_inference,[],[66,82,210,208,218,280,60,333,266,126,123,116,115,4,2,144])).
% 126.35/126.42 cnf(344,plain,
% 126.35/126.42 (~P3(f26(x3441),f42(f20(x3441)))),
% 126.35/126.42 inference(rename_variables,[],[205])).
% 126.35/126.42 cnf(349,plain,
% 126.35/126.42 (E(a33,f20(a4))),
% 126.35/126.42 inference(scs_inference,[],[57,66,82,76,283,210,208,303,218,205,344,280,60,333,69,266,126,123,116,115,4,2,144,52,53,3,137])).
% 126.35/126.42 cnf(352,plain,
% 126.35/126.42 (~E(f20(x3521),a46)),
% 126.35/126.42 inference(scs_inference,[],[57,66,82,76,283,210,208,303,218,205,344,114,280,71,60,333,69,266,126,123,116,115,4,2,144,52,53,3,137,48])).
% 126.35/126.42 cnf(353,plain,
% 126.35/126.42 (~P2(f41(x3531),x3531)),
% 126.35/126.42 inference(rename_variables,[],[114])).
% 126.35/126.42 cnf(354,plain,
% 126.35/126.42 (~E(a3,a39)),
% 126.35/126.42 inference(scs_inference,[],[57,66,63,82,76,283,210,208,303,218,205,344,114,280,71,60,333,104,69,266,126,123,116,115,4,2,144,52,53,3,137,48,45])).
% 126.35/126.42 cnf(355,plain,
% 126.35/126.42 (~E(a33,f41(f27(a37,f20(a2))))),
% 126.35/126.42 inference(scs_inference,[],[57,66,63,82,76,283,210,208,303,218,205,344,114,353,280,71,60,333,104,69,266,126,123,116,115,4,2,144,52,53,3,137,48,45,47])).
% 126.35/126.42 cnf(357,plain,
% 126.35/126.42 (~E(a4,a3)),
% 126.35/126.42 inference(scs_inference,[],[57,66,63,82,76,283,210,208,303,218,205,344,114,353,280,71,60,333,104,69,266,126,123,116,115,4,2,144,52,53,3,137,48,45,47,18])).
% 126.35/126.42 cnf(360,plain,
% 126.35/126.42 (P2(f27(a37,f20(a2)),f20(a3))+~P5(f20(a2),f27(a10,f20(a3)))),
% 126.35/126.42 inference(scs_inference,[],[57,66,65,63,82,76,61,283,210,208,303,218,205,344,114,353,280,71,60,333,104,69,266,126,123,116,115,4,2,144,52,53,3,137,48,45,47,18,54,44,274])).
% 126.35/126.42 cnf(362,plain,
% 126.35/126.42 (~E(f20(a2),f20(a4))+P2(f27(a37,f20(a2)),f20(a3))),
% 126.35/126.42 inference(scs_inference,[],[57,66,65,63,82,76,61,283,210,208,303,218,205,344,114,353,280,71,60,333,104,69,266,126,123,116,115,4,2,144,52,53,3,137,48,45,47,18,54,44,274,272])).
% 126.35/126.42 cnf(367,plain,
% 126.35/126.42 (E(f24(f9(x3671,x3672)),x3671)),
% 126.35/126.42 inference(rename_variables,[],[78])).
% 126.35/126.42 cnf(373,plain,
% 126.35/126.42 (~E(a3,a12)),
% 126.35/126.42 inference(scs_inference,[],[65,311,78,367,116,115,2,4])).
% 126.35/126.42 cnf(374,plain,
% 126.35/126.42 (P2(a46,a33)),
% 126.35/126.42 inference(scs_inference,[],[65,311,218,78,367,67,116,115,2,4,144])).
% 126.35/126.42 cnf(381,plain,
% 126.35/126.42 (P3(f20(a21),f44(x3811,f20(a2)))),
% 126.35/126.42 inference(scs_inference,[],[57,65,230,276,311,196,197,218,293,78,367,67,116,115,2,4,144,137,53,52])).
% 126.35/126.42 cnf(399,plain,
% 126.35/126.42 (E(f47(f9(x3991,x3992)),x3992)),
% 126.35/126.42 inference(rename_variables,[],[79])).
% 126.35/126.42 cnf(404,plain,
% 126.35/126.42 (E(f20(a22),f27(a37,f20(a2)))),
% 126.35/126.42 inference(scs_inference,[],[68,79,399,116,115,2])).
% 126.35/126.42 cnf(405,plain,
% 126.35/126.42 (P2(a46,f20(x4051))),
% 126.35/126.42 inference(scs_inference,[],[68,218,79,399,71,116,115,2,144])).
% 126.35/126.42 cnf(408,plain,
% 126.35/126.42 (~P2(f41(f27(a37,f20(a2))),a33)),
% 126.35/126.42 inference(scs_inference,[],[68,355,218,340,79,399,71,116,115,2,144,137])).
% 126.35/126.42 cnf(412,plain,
% 126.35/126.42 (~E(x4121,f41(f41(f41(x4121))))),
% 126.35/126.42 inference(scs_inference,[],[68,326,355,196,218,64,280,340,79,399,71,116,115,2,144,137,53,47])).
% 126.35/126.42 cnf(416,plain,
% 126.35/126.42 (P2(f20(x4161),f20(a22))),
% 126.35/126.42 inference(scs_inference,[],[66,68,206,326,355,196,218,64,280,298,340,79,399,71,69,116,115,2,144,137,53,47,3,48])).
% 126.35/126.42 cnf(420,plain,
% 126.35/126.42 (P5(x4201,f27(a6,f20(a2)))+~E(f20(a23),x4201)),
% 126.35/126.42 inference(scs_inference,[],[83,66,65,68,206,326,355,196,218,64,280,298,340,79,399,71,69,116,115,2,144,137,53,47,3,48,123,44,45])).
% 126.35/126.42 cnf(427,plain,
% 126.35/126.42 (E(f28(f44(x4271,x4272)),x4272)),
% 126.35/126.42 inference(rename_variables,[],[80])).
% 126.35/126.42 cnf(433,plain,
% 126.35/126.42 (E(f20(a4),a33)),
% 126.35/126.42 inference(scs_inference,[],[225,303,80,427,69,116,115,2,137])).
% 126.35/126.42 cnf(442,plain,
% 126.35/126.42 (P2(f20(x4421),f27(a37,f20(a2)))),
% 126.35/126.42 inference(scs_inference,[],[58,283,197,416,404,225,276,303,220,80,427,69,116,115,2,137,53,47,3,48])).
% 126.35/126.42 cnf(456,plain,
% 126.35/126.42 (E(f29(f44(x4561,x4562)),x4561)),
% 126.35/126.42 inference(rename_variables,[],[81])).
% 126.35/126.42 cnf(461,plain,
% 126.35/126.42 (E(a21,a2)),
% 126.35/126.42 inference(scs_inference,[],[249,81,456,116,115,2])).
% 126.35/126.42 cnf(468,plain,
% 126.35/126.42 (P2(f20(x4681),f20(a4))),
% 126.35/126.42 inference(scs_inference,[],[66,283,197,249,326,280,67,349,81,456,69,116,115,2,53,3,47,48])).
% 126.35/126.42 cnf(469,plain,
% 126.35/126.42 (~E(a46,f41(f41(a33)))),
% 126.35/126.42 inference(scs_inference,[],[66,283,197,249,326,280,67,349,81,456,69,116,115,2,53,3,47,48,17])).
% 126.35/126.42 cnf(472,plain,
% 126.35/126.42 (~P2(f20(a4),f20(a3))),
% 126.35/126.42 inference(scs_inference,[],[66,283,208,197,249,326,280,67,349,81,456,69,116,115,2,53,3,47,48,17,140,137])).
% 126.35/126.42 cnf(474,plain,
% 126.35/126.42 (~P2(a46,f41(f41(a33)))+P2(f41(a46),f41(f41(a33)))),
% 126.35/126.42 inference(scs_inference,[],[66,283,208,197,249,326,280,67,349,81,456,69,116,115,2,53,3,47,48,17,140,137,138])).
% 126.35/126.42 cnf(476,plain,
% 126.35/126.42 (~P2(f41(a46),f41(f41(a33)))+P2(f41(a46),f41(f41(a33)))),
% 126.35/126.42 inference(scs_inference,[],[66,283,208,197,249,326,280,67,349,81,456,69,116,115,2,53,3,47,48,17,140,137,138,132])).
% 126.35/126.42 cnf(480,plain,
% 126.35/126.42 (P2(f41(a46),f41(f41(a33)))+P2(f41(a33),f41(a46))),
% 126.35/126.42 inference(scs_inference,[],[66,278,283,208,197,249,326,280,67,349,81,456,69,116,115,2,53,3,47,48,17,140,137,138,132,126,144])).
% 126.35/126.42 cnf(490,plain,
% 126.35/126.42 (~E(f27(a37,f20(a2)),f20(a3))),
% 126.35/126.42 inference(scs_inference,[],[58,73,196,208,442,205,114,235,472,2,53,47,3,48])).
% 126.35/126.42 cnf(492,plain,
% 126.35/126.42 (E(x4921,f14(f25(x4921)))),
% 126.35/126.42 inference(scs_inference,[],[58,73,196,208,442,205,114,235,472,2,53,47,3,48,117])).
% 126.35/126.42 cnf(494,plain,
% 126.35/126.42 (P2(a46,f41(a33))+~P2(a46,f41(f41(a33)))),
% 126.35/126.42 inference(scs_inference,[],[58,73,196,208,442,469,205,114,235,472,2,53,47,3,48,117,140])).
% 126.35/126.42 cnf(496,plain,
% 126.35/126.42 (P4(a2,f14(f25(a22)),a13)),
% 126.35/126.42 inference(scs_inference,[],[84,58,73,196,208,442,469,205,114,235,472,2,53,47,3,48,117,140,50])).
% 126.35/126.42 cnf(497,plain,
% 126.35/126.42 (~P2(f41(f41(f20(a3))),a33)),
% 126.35/126.42 inference(scs_inference,[],[84,58,73,196,208,442,469,205,114,235,241,472,2,53,47,3,48,117,140,50,137])).
% 126.35/126.42 cnf(499,plain,
% 126.35/126.42 (P4(a21,f14(f25(a22)),a13)),
% 126.35/126.42 inference(scs_inference,[],[84,58,73,196,208,442,469,205,249,114,235,241,472,2,53,47,3,48,117,140,50,137,49])).
% 126.35/126.42 cnf(500,plain,
% 126.35/126.42 (~P2(a46,f41(a33))+P2(a46,f41(a33))),
% 126.35/126.42 inference(scs_inference,[],[84,58,73,196,208,442,469,205,249,114,235,241,472,2,53,47,3,48,117,140,50,137,49,132])).
% 126.35/126.42 cnf(506,plain,
% 126.35/126.42 (P2(a46,f41(a33))+P2(a33,a46)),
% 126.35/126.42 inference(scs_inference,[],[84,58,73,278,196,208,442,469,205,249,114,235,241,472,2,53,47,3,48,117,140,50,137,49,132,123,126,144])).
% 126.35/126.42 cnf(510,plain,
% 126.35/126.42 (P5(f14(f25(f20(a23))),f27(a6,f20(a2)))),
% 126.35/126.42 inference(scs_inference,[],[492,420])).
% 126.35/126.42 cnf(511,plain,
% 126.35/126.42 (E(x5111,f14(f25(x5111)))),
% 126.35/126.42 inference(rename_variables,[],[492])).
% 126.35/126.42 cnf(514,plain,
% 126.35/126.42 (E(x5141,f32(f25(x5141)))),
% 126.35/126.42 inference(scs_inference,[],[59,492,497,420,123,2])).
% 126.35/126.42 cnf(515,plain,
% 126.35/126.42 (P4(a2,a22,f14(f25(a13)))),
% 126.35/126.42 inference(scs_inference,[],[84,59,492,511,497,420,123,2,51])).
% 126.35/126.42 cnf(516,plain,
% 126.35/126.42 (E(x5161,f14(f25(x5161)))),
% 126.35/126.42 inference(rename_variables,[],[492])).
% 126.35/126.42 cnf(517,plain,
% 126.35/126.42 (P1(f14(f25(f44(a1,x5171))))),
% 126.35/126.42 inference(scs_inference,[],[84,75,59,492,511,516,497,420,123,2,51,44])).
% 126.35/126.42 cnf(518,plain,
% 126.35/126.42 (E(x5181,f14(f25(x5181)))),
% 126.35/126.42 inference(rename_variables,[],[492])).
% 126.35/126.42 cnf(523,plain,
% 126.35/126.42 (~E(f20(a22),f20(a3))),
% 126.35/126.42 inference(scs_inference,[],[84,65,283,303,416,220,75,59,472,492,511,516,497,420,123,2,51,44,3,47,48])).
% 126.35/126.42 cnf(525,plain,
% 126.35/126.42 (~E(a22,a3)),
% 126.35/126.42 inference(scs_inference,[],[84,65,283,303,416,220,75,59,472,492,511,516,497,420,123,2,51,44,3,47,48,4])).
% 126.35/126.42 cnf(530,plain,
% 126.35/126.42 (P4(a21,a22,f14(f25(a13)))),
% 126.35/126.42 inference(scs_inference,[],[84,65,283,303,416,249,220,75,59,472,492,511,516,518,497,420,123,2,51,44,3,47,48,4,140,50,49])).
% 126.35/126.42 cnf(542,plain,
% 126.35/126.42 (E(x5421,f32(f25(x5421)))),
% 126.35/126.42 inference(rename_variables,[],[514])).
% 126.35/126.42 cnf(543,plain,
% 126.35/126.42 (E(x5431,f32(f26(x5431)))),
% 126.35/126.42 inference(scs_inference,[],[514,60,420,2])).
% 126.35/126.42 cnf(545,plain,
% 126.35/126.42 (E(x5451,f32(f25(x5451)))),
% 126.35/126.42 inference(rename_variables,[],[514])).
% 126.35/126.42 cnf(546,plain,
% 126.35/126.42 (P4(f32(f25(a2)),a22,a13)),
% 126.35/126.42 inference(scs_inference,[],[84,514,542,545,60,420,2,50,49])).
% 126.35/126.42 cnf(547,plain,
% 126.35/126.42 (E(x5471,f32(f25(x5471)))),
% 126.35/126.42 inference(rename_variables,[],[514])).
% 126.35/126.42 cnf(548,plain,
% 126.35/126.42 (P4(a2,a22,f32(f25(a13)))),
% 126.35/126.42 inference(scs_inference,[],[84,514,542,545,547,60,420,2,50,49,51])).
% 126.35/126.42 cnf(549,plain,
% 126.35/126.42 (E(x5491,f32(f25(x5491)))),
% 126.35/126.42 inference(rename_variables,[],[514])).
% 126.35/126.42 cnf(550,plain,
% 126.35/126.42 (~E(x5501,f41(f41(x5501)))),
% 126.35/126.42 inference(scs_inference,[],[84,218,514,542,545,547,114,60,420,2,50,49,51,47])).
% 126.35/126.42 cnf(560,plain,
% 126.35/126.42 (~E(f20(a2),f20(a12))+P2(f27(a37,f20(a2)),f20(a3))),
% 126.35/126.42 inference(scs_inference,[],[84,63,61,77,66,65,68,82,218,330,232,514,542,545,547,549,114,60,420,2,50,49,51,47,3,48,137,54,44,272])).
% 126.35/126.42 cnf(564,plain,
% 126.35/126.42 (P5(f32(f26(f20(a23))),f27(a6,f20(a2)))),
% 126.35/126.42 inference(scs_inference,[],[543,420])).
% 126.35/126.42 cnf(565,plain,
% 126.35/126.42 (E(x5651,f32(f26(x5651)))),
% 126.35/126.42 inference(rename_variables,[],[543])).
% 126.35/126.42 cnf(566,plain,
% 126.35/126.42 (E(x5661,f24(f9(x5661,x5662)))),
% 126.35/126.42 inference(scs_inference,[],[543,78,420,2])).
% 126.35/126.42 cnf(567,plain,
% 126.35/126.42 (P4(f32(f26(a2)),a22,a13)),
% 126.35/126.42 inference(scs_inference,[],[84,543,565,78,420,2,49])).
% 126.35/126.42 cnf(568,plain,
% 126.35/126.42 (E(x5681,f32(f26(x5681)))),
% 126.35/126.42 inference(rename_variables,[],[543])).
% 126.35/126.42 cnf(570,plain,
% 126.35/126.42 (E(x5701,f32(f26(x5701)))),
% 126.35/126.42 inference(rename_variables,[],[543])).
% 126.35/126.42 cnf(571,plain,
% 126.35/126.42 (P4(a2,a22,f32(f26(a13)))),
% 126.35/126.42 inference(scs_inference,[],[84,543,565,568,570,78,420,2,49,50,51])).
% 126.35/126.42 cnf(572,plain,
% 126.35/126.42 (E(x5721,f32(f26(x5721)))),
% 126.35/126.42 inference(rename_variables,[],[543])).
% 126.35/126.42 cnf(577,plain,
% 126.35/126.42 (P2(a33,f32(f26(f20(a22))))),
% 126.35/126.42 inference(scs_inference,[],[84,58,206,232,468,543,565,568,570,572,220,78,420,2,49,50,51,3,47,48])).
% 126.35/126.42 cnf(586,plain,
% 126.35/126.42 (P5(f24(f9(f20(a23),x5861)),f27(a6,f20(a2)))),
% 126.35/126.42 inference(scs_inference,[],[566,420])).
% 126.35/126.42 cnf(587,plain,
% 126.35/126.42 (E(x5871,f24(f9(x5871,x5872)))),
% 126.35/126.42 inference(rename_variables,[],[566])).
% 126.35/126.42 cnf(588,plain,
% 126.35/126.42 (E(x5881,f47(f9(x5882,x5881)))),
% 126.35/126.42 inference(scs_inference,[],[566,79,420,2])).
% 126.35/126.42 cnf(590,plain,
% 126.35/126.42 (E(x5901,f24(f9(x5901,x5902)))),
% 126.35/126.42 inference(rename_variables,[],[566])).
% 126.35/126.42 cnf(591,plain,
% 126.35/126.42 (P4(f24(f9(a2,x5911)),a22,a13)),
% 126.35/126.42 inference(scs_inference,[],[84,566,587,590,79,420,2,50,49])).
% 126.35/126.42 cnf(592,plain,
% 126.35/126.42 (E(x5921,f24(f9(x5921,x5922)))),
% 126.35/126.42 inference(rename_variables,[],[566])).
% 126.35/126.42 cnf(593,plain,
% 126.35/126.42 (P4(a2,a22,f24(f9(a13,x5931)))),
% 126.35/126.42 inference(scs_inference,[],[84,566,587,590,592,79,420,2,50,49,51])).
% 126.35/126.42 cnf(594,plain,
% 126.35/126.42 (E(x5941,f24(f9(x5941,x5942)))),
% 126.35/126.42 inference(rename_variables,[],[566])).
% 126.35/126.42 cnf(599,plain,
% 126.35/126.42 (P2(a33,f24(f9(f20(a4),x5991)))),
% 126.35/126.42 inference(scs_inference,[],[84,68,283,303,566,587,590,592,594,280,79,69,420,2,50,49,51,47,3,48])).
% 126.35/126.42 cnf(609,plain,
% 126.35/126.42 (E(x6091,f47(f9(x6092,x6091)))),
% 126.35/126.42 inference(rename_variables,[],[588])).
% 126.35/126.42 cnf(610,plain,
% 126.35/126.42 (E(x6101,f28(f44(x6102,x6101)))),
% 126.35/126.42 inference(scs_inference,[],[588,80,420,2])).
% 126.35/126.42 cnf(611,plain,
% 126.35/126.42 (P4(f47(f9(x6111,a2)),a22,a13)),
% 126.35/126.42 inference(scs_inference,[],[84,588,609,80,420,2,49])).
% 126.35/126.42 cnf(612,plain,
% 126.35/126.42 (E(x6121,f47(f9(x6122,x6121)))),
% 126.35/126.42 inference(rename_variables,[],[588])).
% 126.35/126.42 cnf(614,plain,
% 126.35/126.42 (E(x6141,f47(f9(x6142,x6141)))),
% 126.35/126.42 inference(rename_variables,[],[588])).
% 126.35/126.42 cnf(615,plain,
% 126.35/126.42 (P4(a2,a22,f47(f9(x6151,a13)))),
% 126.35/126.42 inference(scs_inference,[],[84,588,609,612,614,80,420,2,49,50,51])).
% 126.35/126.42 cnf(616,plain,
% 126.35/126.42 (E(x6161,f47(f9(x6162,x6161)))),
% 126.35/126.42 inference(rename_variables,[],[588])).
% 126.35/126.42 cnf(621,plain,
% 126.35/126.42 (P2(a33,f47(f9(x6211,f20(a22))))),
% 126.35/126.42 inference(scs_inference,[],[84,68,442,206,232,588,609,612,614,616,114,80,420,2,49,50,51,3,47,48])).
% 126.35/126.42 cnf(630,plain,
% 126.35/126.42 (P5(f28(f44(x6301,f20(a23))),f27(a6,f20(a2)))),
% 126.35/126.42 inference(scs_inference,[],[610,420])).
% 126.35/126.42 cnf(631,plain,
% 126.35/126.42 (E(x6311,f28(f44(x6312,x6311)))),
% 126.35/126.42 inference(rename_variables,[],[610])).
% 126.35/126.42 cnf(632,plain,
% 126.35/126.42 (E(x6321,f29(f44(x6321,x6322)))),
% 126.35/126.42 inference(scs_inference,[],[610,81,420,2])).
% 126.35/126.42 cnf(633,plain,
% 126.35/126.42 (P4(a2,f28(f44(x6331,a22)),a13)),
% 126.35/126.42 inference(scs_inference,[],[84,610,631,81,420,2,50])).
% 126.35/126.42 cnf(634,plain,
% 126.35/126.42 (E(x6341,f28(f44(x6342,x6341)))),
% 126.35/126.42 inference(rename_variables,[],[610])).
% 126.35/126.42 cnf(635,plain,
% 126.35/126.42 (P4(f28(f44(x6351,a2)),a22,a13)),
% 126.35/126.42 inference(scs_inference,[],[84,610,631,634,81,420,2,50,49])).
% 126.35/126.42 cnf(636,plain,
% 126.35/126.42 (E(x6361,f28(f44(x6362,x6361)))),
% 126.35/126.42 inference(rename_variables,[],[610])).
% 126.35/126.42 cnf(637,plain,
% 126.35/126.42 (P4(a2,a22,f28(f44(x6371,a13)))),
% 126.35/126.42 inference(scs_inference,[],[84,610,631,634,636,81,420,2,50,49,51])).
% 126.35/126.42 cnf(638,plain,
% 126.35/126.42 (E(x6381,f28(f44(x6382,x6381)))),
% 126.35/126.42 inference(rename_variables,[],[610])).
% 126.35/126.42 cnf(639,plain,
% 126.35/126.42 (~E(f41(a46),f41(f41(f20(x6391))))),
% 126.35/126.42 inference(scs_inference,[],[84,610,631,634,636,220,81,71,420,2,50,49,51,47])).
% 126.35/126.42 cnf(641,plain,
% 126.35/126.42 (P2(a33,f28(f44(x6411,f20(a4))))),
% 126.35/126.42 inference(scs_inference,[],[84,303,610,631,634,636,638,220,81,71,420,2,50,49,51,47,48])).
% 126.35/126.42 cnf(644,plain,
% 126.35/126.42 (~E(a46,f41(f20(x6441)))),
% 126.35/126.42 inference(scs_inference,[],[84,92,210,303,610,631,634,636,638,220,81,71,420,2,50,49,51,47,48,3,17])).
% 126.35/126.42 cnf(645,plain,
% 126.35/126.42 (~E(a3,a21)),
% 126.35/126.42 inference(scs_inference,[],[84,92,210,303,610,631,634,636,638,220,81,71,420,2,50,49,51,47,48,3,17,4])).
% 126.35/126.42 cnf(655,plain,
% 126.35/126.42 (P5(f29(f44(f20(a23),x6551)),f27(a6,f20(a2)))),
% 126.35/126.42 inference(scs_inference,[],[632,420])).
% 126.35/126.42 cnf(656,plain,
% 126.35/126.42 (E(x6561,f29(f44(x6561,x6562)))),
% 126.35/126.42 inference(rename_variables,[],[632])).
% 126.35/126.42 cnf(657,plain,
% 126.35/126.42 (E(f9(x6571,a1),f44(a1,x6571))),
% 126.35/126.42 inference(scs_inference,[],[632,72,420,2])).
% 126.35/126.42 cnf(658,plain,
% 126.35/126.42 (P4(f29(f44(a2,x6581)),a22,a13)),
% 126.35/126.42 inference(scs_inference,[],[84,632,656,72,420,2,49])).
% 126.35/126.42 cnf(659,plain,
% 126.35/126.42 (E(x6591,f29(f44(x6591,x6592)))),
% 126.35/126.42 inference(rename_variables,[],[632])).
% 126.35/126.42 cnf(661,plain,
% 126.35/126.42 (E(x6611,f29(f44(x6611,x6612)))),
% 126.35/126.42 inference(rename_variables,[],[632])).
% 126.35/126.42 cnf(662,plain,
% 126.35/126.42 (P4(a2,a22,f29(f44(a13,x6621)))),
% 126.35/126.42 inference(scs_inference,[],[84,632,656,659,661,72,420,2,49,50,51])).
% 126.35/126.42 cnf(663,plain,
% 126.35/126.42 (E(x6631,f29(f44(x6631,x6632)))),
% 126.35/126.42 inference(rename_variables,[],[632])).
% 126.35/126.42 cnf(664,plain,
% 126.35/126.42 (P2(a33,f29(f44(f20(a22),x6641)))),
% 126.35/126.42 inference(scs_inference,[],[84,232,632,656,659,661,663,72,420,2,49,50,51,48])).
% 126.35/126.42 cnf(679,plain,
% 126.35/126.42 (E(x6791,f32(f25(x6791)))),
% 126.35/126.42 inference(rename_variables,[],[514])).
% 126.35/126.42 cnf(680,plain,
% 126.35/126.42 (P4(f32(f25(a21)),a22,a13)),
% 126.35/126.42 inference(scs_inference,[],[254,514,679,245,2,50,49])).
% 126.35/126.42 cnf(681,plain,
% 126.35/126.42 (E(x6811,f32(f25(x6811)))),
% 126.35/126.42 inference(rename_variables,[],[514])).
% 126.35/126.42 cnf(682,plain,
% 126.35/126.42 (P4(a21,a22,f32(f25(a13)))),
% 126.35/126.42 inference(scs_inference,[],[254,514,679,681,245,2,50,49,51])).
% 126.35/126.42 cnf(683,plain,
% 126.35/126.42 (E(x6831,f32(f25(x6831)))),
% 126.35/126.42 inference(rename_variables,[],[514])).
% 126.35/126.42 cnf(688,plain,
% 126.35/126.42 (P2(a33,f32(f25(f20(a4))))),
% 126.35/126.42 inference(scs_inference,[],[254,206,303,339,514,679,681,683,220,67,245,2,50,49,51,3,47,48])).
% 126.35/126.42 cnf(693,plain,
% 126.35/126.42 (~P2(a46,f41(a33))+P2(f41(a46),f41(a33))),
% 126.35/126.42 inference(scs_inference,[],[254,206,303,339,514,679,681,683,220,67,245,2,50,49,51,3,47,48,17,140,138])).
% 126.35/126.42 cnf(702,plain,
% 126.35/126.42 (E(x7021,f32(f26(x7021)))),
% 126.35/126.42 inference(rename_variables,[],[543])).
% 126.35/126.42 cnf(703,plain,
% 126.35/126.42 (P4(f32(f26(a21)),a22,a13)),
% 126.35/126.42 inference(scs_inference,[],[254,543,702,247,2,50,49])).
% 126.35/126.42 cnf(704,plain,
% 126.35/126.42 (E(x7041,f32(f26(x7041)))),
% 126.35/126.42 inference(rename_variables,[],[543])).
% 126.35/126.42 cnf(705,plain,
% 126.35/126.42 (P4(a21,a22,f32(f26(a13)))),
% 126.35/126.42 inference(scs_inference,[],[254,543,702,704,247,2,50,49,51])).
% 126.35/126.42 cnf(706,plain,
% 126.35/126.42 (E(x7061,f32(f26(x7061)))),
% 126.35/126.42 inference(rename_variables,[],[543])).
% 126.35/126.42 cnf(707,plain,
% 126.35/126.42 (P2(a33,f32(f26(f20(a4))))),
% 126.35/126.42 inference(scs_inference,[],[254,303,543,702,704,706,247,2,50,49,51,48])).
% 126.35/126.42 cnf(711,plain,
% 126.35/126.42 (~E(a46,f41(f41(f41(a33))))),
% 126.35/126.42 inference(scs_inference,[],[254,206,303,657,543,702,704,706,280,247,374,2,50,49,51,48,3,47])).
% 126.35/126.42 cnf(720,plain,
% 126.35/126.42 (P1(f24(f9(a1,x7201)))),
% 126.35/126.42 inference(scs_inference,[],[75,566,142,44])).
% 126.35/126.42 cnf(723,plain,
% 126.35/126.42 (E(x7231,f47(f9(x7232,x7231)))),
% 126.35/126.42 inference(rename_variables,[],[588])).
% 126.35/126.42 cnf(725,plain,
% 126.35/126.42 (E(x7251,f47(f9(x7252,x7251)))),
% 126.35/126.42 inference(rename_variables,[],[588])).
% 126.35/126.42 cnf(726,plain,
% 126.35/126.42 (P4(a21,a22,f47(f9(x7261,a13)))),
% 126.35/126.42 inference(scs_inference,[],[254,588,723,725,85,2,50,49,51])).
% 126.35/126.42 cnf(727,plain,
% 126.35/126.42 (E(x7271,f47(f9(x7272,x7271)))),
% 126.35/126.42 inference(rename_variables,[],[588])).
% 126.35/126.42 cnf(730,plain,
% 126.35/126.42 (P2(a33,f47(f9(x7301,f20(a4))))),
% 126.35/126.42 inference(scs_inference,[],[254,303,588,723,725,727,114,85,2,50,49,51,47,48])).
% 126.35/126.42 cnf(742,plain,
% 126.35/126.42 (E(x7421,f28(f44(x7422,x7421)))),
% 126.35/126.42 inference(rename_variables,[],[610])).
% 126.35/126.42 cnf(743,plain,
% 126.35/126.42 (P4(f28(f44(x7431,a21)),a22,a13)),
% 126.35/126.42 inference(scs_inference,[],[254,610,742,50,49])).
% 126.35/126.42 cnf(744,plain,
% 126.35/126.42 (E(x7441,f28(f44(x7442,x7441)))),
% 126.35/126.42 inference(rename_variables,[],[610])).
% 126.35/126.42 cnf(745,plain,
% 126.35/126.42 (P4(a21,a22,f28(f44(x7451,a13)))),
% 126.35/126.42 inference(scs_inference,[],[254,610,742,744,50,49,51])).
% 126.35/126.42 cnf(746,plain,
% 126.35/126.42 (E(x7461,f28(f44(x7462,x7461)))),
% 126.35/126.42 inference(rename_variables,[],[610])).
% 126.35/126.42 cnf(747,plain,
% 126.35/126.42 (~E(f41(f28(f44(x7471,x7472))),x7472)),
% 126.35/126.42 inference(scs_inference,[],[254,206,610,742,744,746,50,49,51,3])).
% 126.35/126.42 cnf(751,plain,
% 126.35/126.42 (P2(a33,f28(f44(x7511,f20(a22))))),
% 126.35/126.42 inference(scs_inference,[],[254,206,232,610,742,744,746,220,69,50,49,51,3,47,48])).
% 126.35/126.42 cnf(767,plain,
% 126.35/126.42 (E(x7671,f29(f44(x7671,x7672)))),
% 126.35/126.42 inference(rename_variables,[],[632])).
% 126.35/126.42 cnf(768,plain,
% 126.35/126.42 (P4(f29(f44(a21,x7681)),a22,a13)),
% 126.35/126.42 inference(scs_inference,[],[254,632,767,747,17,50,49])).
% 126.35/126.42 cnf(769,plain,
% 126.35/126.42 (E(x7691,f29(f44(x7691,x7692)))),
% 126.35/126.42 inference(rename_variables,[],[632])).
% 126.35/126.42 cnf(770,plain,
% 126.35/126.42 (P4(a21,a22,f29(f44(a13,x7701)))),
% 126.35/126.42 inference(scs_inference,[],[254,632,767,769,747,17,50,49,51])).
% 126.35/126.42 cnf(771,plain,
% 126.35/126.42 (E(x7711,f29(f44(x7711,x7712)))),
% 126.35/126.42 inference(rename_variables,[],[632])).
% 126.35/126.42 cnf(774,plain,
% 126.35/126.42 (P2(a33,f29(f44(f20(a4),x7741)))),
% 126.35/126.42 inference(scs_inference,[],[65,254,330,303,632,767,769,771,747,17,50,49,51,3,48])).
% 126.35/126.42 cnf(785,plain,
% 126.35/126.42 (E(x7851,f24(f9(x7851,x7852)))),
% 126.35/126.42 inference(rename_variables,[],[566])).
% 126.35/126.42 cnf(786,plain,
% 126.35/126.42 (P4(f24(f9(a21,x7861)),a22,a13)),
% 126.35/126.42 inference(scs_inference,[],[254,566,785,50,49])).
% 126.35/126.42 cnf(787,plain,
% 126.35/126.42 (E(x7871,f24(f9(x7871,x7872)))),
% 126.35/126.42 inference(rename_variables,[],[566])).
% 126.35/126.42 cnf(788,plain,
% 126.35/126.42 (P4(a21,a22,f24(f9(a13,x7881)))),
% 126.35/126.42 inference(scs_inference,[],[254,566,785,787,50,49,51])).
% 126.35/126.42 cnf(789,plain,
% 126.35/126.42 (E(x7891,f24(f9(x7891,x7892)))),
% 126.35/126.42 inference(rename_variables,[],[566])).
% 126.35/126.42 cnf(792,plain,
% 126.35/126.42 (~E(a46,f41(f41(f20(x7921))))),
% 126.35/126.42 inference(scs_inference,[],[254,330,566,785,787,461,220,405,50,49,51,3,47])).
% 126.35/126.42 cnf(794,plain,
% 126.35/126.42 (P2(a33,f24(f9(f20(a22),x7941)))),
% 126.35/126.42 inference(scs_inference,[],[254,330,232,566,785,787,789,461,220,405,50,49,51,3,47,48])).
% 126.35/126.42 cnf(819,plain,
% 126.35/126.42 (E(x8191,f32(f26(x8191)))),
% 126.35/126.42 inference(rename_variables,[],[543])).
% 126.35/126.42 cnf(821,plain,
% 126.35/126.42 (E(x8211,f32(f26(x8211)))),
% 126.35/126.42 inference(rename_variables,[],[543])).
% 126.35/126.42 cnf(823,plain,
% 126.35/126.42 (E(x8231,f32(f26(x8231)))),
% 126.35/126.42 inference(rename_variables,[],[543])).
% 126.35/126.42 cnf(828,plain,
% 126.35/126.42 (P2(a46,f32(f26(a33)))),
% 126.35/126.42 inference(scs_inference,[],[206,543,819,821,823,499,548,416,114,374,50,49,51,47,3,48])).
% 126.35/126.42 cnf(869,plain,
% 126.35/126.42 (E(x8691,f29(f44(x8691,x8692)))),
% 126.35/126.42 inference(rename_variables,[],[632])).
% 126.35/126.42 cnf(871,plain,
% 126.35/126.42 (E(x8711,f29(f44(x8711,x8712)))),
% 126.35/126.42 inference(rename_variables,[],[632])).
% 126.35/126.42 cnf(874,plain,
% 126.35/126.42 (P4(a2,f14(f25(a22)),f29(f44(a13,x8741)))),
% 126.35/126.42 inference(scs_inference,[],[92,632,869,871,496,680,251,50,49,3,51])).
% 126.35/126.42 cnf(899,plain,
% 126.35/126.42 (E(x8991,f32(f25(x8991)))),
% 126.35/126.42 inference(rename_variables,[],[514])).
% 126.35/126.42 cnf(901,plain,
% 126.35/126.42 (E(x9011,f32(f25(x9011)))),
% 126.35/126.42 inference(rename_variables,[],[514])).
% 126.35/126.42 cnf(905,plain,
% 126.35/126.42 (E(x9051,f32(f25(x9051)))),
% 126.35/126.42 inference(rename_variables,[],[514])).
% 126.35/126.42 cnf(906,plain,
% 126.35/126.42 (P2(a46,f32(f25(a33)))),
% 126.35/126.42 inference(scs_inference,[],[92,514,899,901,905,499,703,78,374,50,49,3,51,48])).
% 126.35/126.42 cnf(1108,plain,
% 126.35/126.42 (P4(f24(f9(a21,x11081)),f24(f9(a22,x11082)),a13)),
% 126.35/126.42 inference(scs_inference,[],[566,786,50])).
% 126.35/126.42 cnf(1125,plain,
% 126.35/126.42 (P4(a21,f32(f25(a22)),f24(f9(a13,x11251)))),
% 126.35/126.42 inference(scs_inference,[],[514,788,50])).
% 126.35/126.42 cnf(1175,plain,
% 126.35/126.42 (E(x11751,f24(f9(x11751,x11752)))),
% 126.35/126.42 inference(rename_variables,[],[566])).
% 126.35/126.42 cnf(1177,plain,
% 126.35/126.42 (E(x11771,f24(f9(x11771,x11772)))),
% 126.35/126.42 inference(rename_variables,[],[566])).
% 126.35/126.42 cnf(1181,plain,
% 126.35/126.42 (~P2(a33,f20(a3))),
% 126.35/126.42 inference(scs_inference,[],[566,1175,1177,208,1108,874,546,69,349,49,50,51,3,137])).
% 126.35/126.42 cnf(1308,plain,
% 126.35/126.42 (P4(f47(f9(x13081,a2)),f28(f44(x13082,a22)),a13)),
% 126.35/126.42 inference(scs_inference,[],[610,774,611,1181,48,50])).
% 126.35/126.42 cnf(1320,plain,
% 126.35/126.42 (E(x13201,f24(f9(x13201,x13202)))),
% 126.35/126.42 inference(rename_variables,[],[566])).
% 126.35/126.42 cnf(1322,plain,
% 126.35/126.42 (E(x13221,f24(f9(x13221,x13222)))),
% 126.35/126.42 inference(rename_variables,[],[566])).
% 126.35/126.42 cnf(1323,plain,
% 126.35/126.42 (P4(f24(f9(a21,x13231)),f32(f25(a22)),f24(f9(a13,x13232)))),
% 126.35/126.42 inference(scs_inference,[],[566,1320,1322,794,1308,1125,635,1181,48,50,51,49])).
% 126.35/126.42 cnf(1648,plain,
% 126.35/126.42 (P2(f41(a46),f27(a37,f20(a2)))),
% 126.35/126.42 inference(scs_inference,[],[82,67,144])).
% 126.35/126.42 cnf(1650,plain,
% 126.35/126.42 (~E(f27(a37,f20(a2)),a46)),
% 126.35/126.42 inference(scs_inference,[],[82,67,114,144,48])).
% 126.35/126.42 cnf(1662,plain,
% 126.35/126.42 (P2(f41(a46),f41(f20(a3)))),
% 126.35/126.42 inference(scs_inference,[],[73,67,144])).
% 126.35/126.42 cnf(1678,plain,
% 126.35/126.42 (P2(f41(a46),f32(f26(f20(a22))))),
% 126.35/126.42 inference(scs_inference,[],[577,67,144])).
% 126.35/126.42 cnf(1680,plain,
% 126.35/126.42 (~E(f32(f26(f20(a22))),a46)),
% 126.35/126.42 inference(scs_inference,[],[577,67,114,144,48])).
% 126.35/126.42 cnf(1692,plain,
% 126.35/126.42 (P2(f41(a46),f32(f26(f20(a4))))),
% 126.35/126.42 inference(scs_inference,[],[707,67,144])).
% 126.35/126.42 cnf(1694,plain,
% 126.35/126.42 (~E(f32(f26(f20(a4))),a46)),
% 126.35/126.42 inference(scs_inference,[],[707,67,114,144,48])).
% 126.35/126.42 cnf(1720,plain,
% 126.35/126.42 (P2(f41(a46),f32(f25(f20(a4))))),
% 126.35/126.42 inference(scs_inference,[],[688,67,144])).
% 126.35/126.42 cnf(1722,plain,
% 126.35/126.42 (~E(f32(f25(f20(a4))),a46)),
% 126.35/126.42 inference(scs_inference,[],[688,67,114,144,48])).
% 126.35/126.42 cnf(1725,plain,
% 126.35/126.42 (E(x17251,f32(f25(x17251)))),
% 126.35/126.42 inference(rename_variables,[],[514])).
% 126.35/126.42 cnf(1726,plain,
% 126.35/126.42 (P4(a2,f32(f25(a22)),f14(f25(a13)))),
% 126.35/126.42 inference(scs_inference,[],[514,1725,688,515,633,67,114,144,48,51,50])).
% 126.35/126.42 cnf(1735,plain,
% 126.35/126.42 (P2(f41(a46),f24(f9(f20(a4),x17351)))),
% 126.35/126.42 inference(scs_inference,[],[599,67,144])).
% 126.35/126.42 cnf(1737,plain,
% 126.35/126.42 (~E(f24(f9(f20(a4),x17371)),a46)),
% 126.35/126.42 inference(scs_inference,[],[599,67,114,144,48])).
% 126.35/126.42 cnf(1749,plain,
% 126.35/126.42 (P2(f41(a46),f47(f9(x17491,f20(a22))))),
% 126.35/126.42 inference(scs_inference,[],[621,67,144])).
% 126.35/126.42 cnf(1751,plain,
% 126.35/126.42 (~E(f47(f9(x17511,f20(a22))),a46)),
% 126.35/126.42 inference(scs_inference,[],[621,67,114,144,48])).
% 126.35/126.42 cnf(1754,plain,
% 126.35/126.42 (E(x17541,f28(f44(x17542,x17541)))),
% 126.35/126.42 inference(rename_variables,[],[610])).
% 126.35/126.42 cnf(1757,plain,
% 126.35/126.42 (P4(a21,f32(f25(a22)),f14(f25(a13)))),
% 126.35/126.42 inference(scs_inference,[],[249,610,1754,621,682,591,1726,67,114,144,48,50,51,49])).
% 126.35/126.42 cnf(1763,plain,
% 126.35/126.42 (P2(f41(a46),f28(f44(x17631,f20(a4))))),
% 126.35/126.42 inference(scs_inference,[],[641,67,144])).
% 126.35/126.42 cnf(1765,plain,
% 126.35/126.42 (~E(f28(f44(x17651,f20(a4))),a46)),
% 126.35/126.42 inference(scs_inference,[],[641,67,114,144,48])).
% 126.35/126.42 cnf(1777,plain,
% 126.35/126.42 (P2(f41(a46),f29(f44(f20(a22),x17771)))),
% 126.35/126.42 inference(scs_inference,[],[664,67,144])).
% 126.35/126.42 cnf(1779,plain,
% 126.35/126.42 (~E(f29(f44(f20(a22),x17791)),a46)),
% 126.35/126.42 inference(scs_inference,[],[664,67,114,144,48])).
% 126.35/126.42 cnf(1782,plain,
% 126.35/126.42 (E(x17821,f29(f44(x17821,x17822)))),
% 126.35/126.42 inference(rename_variables,[],[632])).
% 126.35/126.42 cnf(1783,plain,
% 126.35/126.42 (P4(f29(f44(a21,x17831)),a22,f29(f44(a13,x17832)))),
% 126.35/126.42 inference(scs_inference,[],[632,1782,664,745,768,67,114,144,48,50,51])).
% 126.35/126.42 cnf(1791,plain,
% 126.35/126.42 (P2(f41(a46),f47(f9(x17911,f20(a4))))),
% 126.35/126.42 inference(scs_inference,[],[730,67,144])).
% 126.35/126.42 cnf(1793,plain,
% 126.35/126.42 (~E(f47(f9(x17931,f20(a4))),a46)),
% 126.35/126.42 inference(scs_inference,[],[730,67,114,144,48])).
% 126.35/126.42 cnf(1805,plain,
% 126.35/126.42 (P2(f41(a46),f28(f44(x18051,f20(a22))))),
% 126.35/126.42 inference(scs_inference,[],[751,67,144])).
% 126.35/126.42 cnf(1807,plain,
% 126.35/126.42 (~E(f28(f44(x18071,f20(a22))),a46)),
% 126.35/126.42 inference(scs_inference,[],[751,67,114,144,48])).
% 126.35/126.42 cnf(1818,plain,
% 126.35/126.42 (P2(f41(a46),f29(f44(f20(a4),x18181)))),
% 126.35/126.42 inference(scs_inference,[],[774,67,144])).
% 126.35/126.42 cnf(1831,plain,
% 126.35/126.42 (P2(f41(a46),f24(f9(f20(a22),x18311)))),
% 126.35/126.42 inference(scs_inference,[],[794,67,144])).
% 126.35/126.42 cnf(1833,plain,
% 126.35/126.42 (~E(f24(f9(f20(a22),x18331)),a46)),
% 126.35/126.42 inference(scs_inference,[],[794,67,114,144,48])).
% 126.35/126.42 cnf(1844,plain,
% 126.35/126.42 (P2(a46,f27(a37,f20(a2)))),
% 126.35/126.42 inference(scs_inference,[],[218,1648,144])).
% 126.35/126.42 cnf(1857,plain,
% 126.35/126.42 (~P2(f41(f20(a3)),a46)),
% 126.35/126.42 inference(scs_inference,[],[218,644,1662,144,137])).
% 126.35/126.42 cnf(1868,plain,
% 126.35/126.42 (P2(a46,f32(f26(f20(a22))))),
% 126.35/126.42 inference(scs_inference,[],[218,1678,144])).
% 126.35/126.42 cnf(1878,plain,
% 126.35/126.42 (P2(a46,f32(f26(f20(a4))))),
% 126.35/126.42 inference(scs_inference,[],[218,1692,144])).
% 126.35/126.42 cnf(1898,plain,
% 126.35/126.42 (P2(a46,f32(f25(f20(a4))))),
% 126.35/126.42 inference(scs_inference,[],[218,1720,144])).
% 126.35/126.42 cnf(1908,plain,
% 126.35/126.42 (P2(a46,f24(f9(f20(a4),x19081)))),
% 126.35/126.42 inference(scs_inference,[],[218,1735,144])).
% 126.35/126.42 cnf(1918,plain,
% 126.35/126.42 (P2(a46,f47(f9(x19181,f20(a22))))),
% 126.35/126.42 inference(scs_inference,[],[218,1749,144])).
% 126.35/126.42 cnf(1928,plain,
% 126.35/126.42 (P2(a46,f28(f44(x19281,f20(a4))))),
% 126.35/126.42 inference(scs_inference,[],[218,1763,144])).
% 126.35/126.42 cnf(1938,plain,
% 126.35/126.42 (P2(a46,f29(f44(f20(a22),x19381)))),
% 126.35/126.42 inference(scs_inference,[],[218,1777,144])).
% 126.35/126.42 cnf(1948,plain,
% 126.35/126.42 (P2(a46,f47(f9(x19481,f20(a4))))),
% 126.35/126.42 inference(scs_inference,[],[218,1791,144])).
% 126.35/126.42 cnf(1960,plain,
% 126.35/126.42 (P2(a46,f28(f44(x19601,f20(a22))))),
% 126.35/126.42 inference(scs_inference,[],[218,588,1805,1783,50,144])).
% 126.35/126.42 cnf(1973,plain,
% 126.35/126.42 (P3(f20(a4),f9(f41(f20(a3)),x19731))),
% 126.35/126.42 inference(scs_inference,[],[58,218,196,610,1818,546,144,50,52])).
% 126.35/126.42 cnf(1980,plain,
% 126.35/126.42 (P2(a46,f24(f9(f20(a22),x19801)))),
% 126.35/126.42 inference(scs_inference,[],[218,1831,144])).
% 126.35/126.42 cnf(1985,plain,
% 126.35/126.42 (P3(f20(a4),f44(x19851,f41(f20(a3))))),
% 126.35/126.42 inference(scs_inference,[],[58,218,197,566,1831,703,144,50,52])).
% 126.35/126.42 cnf(1992,plain,
% 126.35/126.42 (P2(f41(a46),f41(f27(a37,f20(a2))))),
% 126.35/126.42 inference(scs_inference,[],[67,340,144])).
% 126.35/126.42 cnf(1994,plain,
% 126.35/126.42 (~E(f41(f27(a37,f20(a2))),a46)),
% 126.35/126.42 inference(scs_inference,[],[67,114,340,144,48])).
% 126.35/126.42 cnf(2006,plain,
% 126.35/126.42 (P2(a46,f41(f27(a37,f20(a2))))),
% 126.35/126.42 inference(scs_inference,[],[218,1992,144])).
% 126.35/126.42 cnf(2021,plain,
% 126.35/126.42 (E(x20211,f32(f25(x20211)))),
% 126.35/126.42 inference(rename_variables,[],[514])).
% 126.35/126.42 cnf(2031,plain,
% 126.35/126.42 (P2(a46,f41(f41(f20(a3))))),
% 126.35/126.42 inference(scs_inference,[],[639,514,2021,658,67,114,241,144,48,50,137,51,132,123,126])).
% 126.35/126.42 cnf(2052,plain,
% 126.35/126.42 (P2(f41(a46),f41(f20(a22)))),
% 126.35/126.42 inference(scs_inference,[],[71,293,144])).
% 126.35/126.42 cnf(2070,plain,
% 126.35/126.42 (~P2(f41(f20(a22)),a46)),
% 126.35/126.42 inference(scs_inference,[],[218,644,2052,144,137])).
% 126.35/126.42 cnf(2597,plain,
% 126.35/126.42 (P3(a7,f9(f27(a43,f20(a2)),x25971))),
% 126.35/126.42 inference(scs_inference,[],[65,196,52])).
% 126.35/126.42 cnf(2603,plain,
% 126.35/126.42 (P3(a7,f44(x26031,f27(a43,f20(a2))))),
% 126.35/126.42 inference(scs_inference,[],[65,197,52])).
% 126.35/126.42 cnf(2621,plain,
% 126.35/126.42 (P4(f32(f26(a2)),a22,f28(f44(x26211,a13)))),
% 126.35/126.42 inference(scs_inference,[],[610,567,51])).
% 126.35/126.42 cnf(2622,plain,
% 126.35/126.42 (E(x26221,f28(f44(x26222,x26221)))),
% 126.35/126.42 inference(rename_variables,[],[610])).
% 126.35/126.42 cnf(2624,plain,
% 126.35/126.42 (E(x26241,f28(f44(x26242,x26241)))),
% 126.35/126.42 inference(rename_variables,[],[610])).
% 126.35/126.42 cnf(2625,plain,
% 126.35/126.42 (P4(f32(f26(a2)),f28(f44(x26251,a22)),a13)),
% 126.35/126.42 inference(scs_inference,[],[610,2622,2624,567,2597,51,52,50])).
% 126.35/126.42 cnf(2629,plain,
% 126.35/126.42 (E(f28(f44(x26291,a7)),f27(a43,f20(a2)))),
% 126.35/126.42 inference(scs_inference,[],[610,2622,2624,283,567,2597,349,105,51,52,50,3,152])).
% 126.35/126.42 cnf(2639,plain,
% 126.35/126.42 (E(x26391,f24(f9(x26391,x26392)))),
% 126.35/126.42 inference(rename_variables,[],[566])).
% 126.35/126.42 cnf(2641,plain,
% 126.35/126.42 (E(x26411,f24(f9(x26411,x26412)))),
% 126.35/126.42 inference(rename_variables,[],[566])).
% 126.35/126.42 cnf(2644,plain,
% 126.35/126.42 (E(f24(f9(a7,x26441)),f27(a43,f20(a2)))),
% 126.35/126.42 inference(scs_inference,[],[566,2639,2641,680,2603,2629,105,2,51,52,50,151])).
% 126.35/126.42 cnf(2655,plain,
% 126.35/126.42 (E(x26551,f29(f44(x26551,x26552)))),
% 126.35/126.42 inference(rename_variables,[],[632])).
% 126.35/126.42 cnf(2657,plain,
% 126.35/126.42 (E(x26571,f29(f44(x26571,x26572)))),
% 126.35/126.42 inference(rename_variables,[],[632])).
% 126.35/126.42 cnf(2660,plain,
% 126.35/126.42 (E(f29(f44(a7,x26601)),f27(a43,f20(a2)))),
% 126.35/126.42 inference(scs_inference,[],[632,2655,2657,703,2597,2644,105,2,51,50,52,152])).
% 126.35/126.42 cnf(2671,plain,
% 126.35/126.42 (E(x26711,f32(f26(x26711)))),
% 126.35/126.42 inference(rename_variables,[],[543])).
% 126.35/126.42 cnf(2672,plain,
% 126.35/126.42 (P3(f32(f26(a7)),f44(x26721,f27(a43,f20(a2))))),
% 126.35/126.42 inference(scs_inference,[],[543,2671,591,2603,2660,2,51,52])).
% 126.35/126.42 cnf(2673,plain,
% 126.35/126.42 (E(x26731,f32(f26(x26731)))),
% 126.35/126.42 inference(rename_variables,[],[543])).
% 126.35/126.42 cnf(2676,plain,
% 126.35/126.42 (E(f32(f26(a7)),f27(a43,f20(a2)))),
% 126.35/126.42 inference(scs_inference,[],[543,2671,2673,591,2603,2660,105,2,51,52,50,151])).
% 126.35/126.42 cnf(2685,plain,
% 126.35/126.42 (~P2(f41(f41(f41(f41(x26851)))),x26851)),
% 126.35/126.42 inference(scs_inference,[],[280,132])).
% 126.35/126.42 cnf(2690,plain,
% 126.35/126.42 (P2(x26901,f41(f41(f41(f41(x26901)))))),
% 126.35/126.42 inference(scs_inference,[],[280,132,123,126])).
% 126.35/126.42 cnf(2693,plain,
% 126.35/126.42 (P2(a33,f41(f41(f27(a37,f20(a2)))))),
% 126.35/126.42 inference(scs_inference,[],[82,278,280,2676,132,123,126,2,144])).
% 126.35/126.42 cnf(2697,plain,
% 126.35/126.42 (E(x26971,f24(f9(x26971,x26972)))),
% 126.35/126.42 inference(rename_variables,[],[566])).
% 126.35/126.42 cnf(2699,plain,
% 126.35/126.42 (E(x26991,f24(f9(x26991,x26992)))),
% 126.35/126.42 inference(rename_variables,[],[566])).
% 126.35/126.42 cnf(2702,plain,
% 126.35/126.42 (~P2(f41(f41(f27(a37,f20(a2)))),a33)),
% 126.35/126.42 inference(scs_inference,[],[82,828,566,2697,278,635,220,280,2676,132,123,126,2,144,48,49,47,137])).
% 126.35/126.42 cnf(2704,plain,
% 126.35/126.42 (~E(f41(f41(f24(f9(x27041,x27042)))),x27041)),
% 126.35/126.42 inference(scs_inference,[],[82,828,566,2697,2699,278,283,635,220,280,2676,132,123,126,2,144,48,49,47,137,3])).
% 126.35/126.42 cnf(2707,plain,
% 126.35/126.42 (E(x27071,f24(f9(x27071,x27072)))),
% 126.35/126.42 inference(rename_variables,[],[566])).
% 126.35/126.42 cnf(2709,plain,
% 126.35/126.42 (E(x27091,f24(f9(x27091,x27092)))),
% 126.35/126.42 inference(rename_variables,[],[566])).
% 126.35/126.42 cnf(2712,plain,
% 126.35/126.42 (E(f24(f9(f20(a4),x27121)),f41(f20(a3)))),
% 126.35/126.42 inference(scs_inference,[],[82,828,566,2697,2699,2707,2709,278,283,615,496,1973,635,220,280,2676,105,132,123,126,2,144,48,49,47,137,3,51,52,50,152])).
% 126.35/126.42 cnf(2723,plain,
% 126.35/126.42 (~E(f41(f24(f9(f41(x27231),x27232))),x27231)),
% 126.35/126.42 inference(scs_inference,[],[2704,17])).
% 126.35/126.42 cnf(2727,plain,
% 126.35/126.42 (E(f41(f20(a3)),f24(f9(f20(a4),x27271)))),
% 126.35/126.42 inference(scs_inference,[],[2704,2712,2702,17,123,2])).
% 126.35/126.42 cnf(2731,plain,
% 126.35/126.42 (E(x27311,f29(f44(x27311,x27312)))),
% 126.35/126.42 inference(rename_variables,[],[632])).
% 126.35/126.42 cnf(2733,plain,
% 126.35/126.42 (E(x27331,f29(f44(x27331,x27332)))),
% 126.35/126.42 inference(rename_variables,[],[632])).
% 126.35/126.42 cnf(2738,plain,
% 126.35/126.42 (P4(a21,a22,f29(f44(f47(f9(x27381,a13)),x27382)))),
% 126.35/126.42 inference(scs_inference,[],[73,906,249,632,2731,2733,206,726,743,2704,374,220,2693,2712,2702,17,123,2,144,48,49,47,3,51])).
% 126.35/126.42 cnf(2739,plain,
% 126.35/126.42 (E(x27391,f29(f44(x27391,x27392)))),
% 126.35/126.42 inference(rename_variables,[],[632])).
% 126.35/126.42 cnf(2741,plain,
% 126.35/126.42 (E(x27411,f29(f44(x27411,x27412)))),
% 126.35/126.42 inference(rename_variables,[],[632])).
% 126.35/126.42 cnf(2742,plain,
% 126.35/126.42 (P4(a21,f29(f44(f14(f25(a22)),x27421)),a13)),
% 126.35/126.42 inference(scs_inference,[],[73,906,249,632,2731,2733,2739,2741,206,726,499,1985,743,2704,374,220,2693,2712,2702,17,123,2,144,48,49,47,3,51,52,50])).
% 126.35/126.42 cnf(2755,plain,
% 126.35/126.42 (P3(f20(a2),f9(f20(a21),x27551))),
% 126.35/126.42 inference(scs_inference,[],[57,133])).
% 126.35/126.42 cnf(2757,plain,
% 126.35/126.42 (P3(f20(a2),f44(x27571,f20(a21)))),
% 126.35/126.42 inference(scs_inference,[],[57,133,134])).
% 126.35/126.42 cnf(2771,plain,
% 126.35/126.42 (P1(f44(f24(f9(a1,x27711)),f30(x27712,x27713)))),
% 126.35/126.42 inference(scs_inference,[],[57,211,720,2672,133,134,145,146,118,119,120,121,153])).
% 126.35/126.42 cnf(2773,plain,
% 126.35/126.42 (P4(f14(f25(a21)),a22,a13)),
% 126.35/126.42 inference(scs_inference,[],[57,211,720,2672,492,133,134,145,146,118,119,120,121,153,317])).
% 126.35/126.42 cnf(2774,plain,
% 126.35/126.42 (E(x27741,f14(f25(x27741)))),
% 126.35/126.42 inference(rename_variables,[],[492])).
% 126.35/126.42 cnf(2775,plain,
% 126.35/126.42 (E(f14(f20(a2)),f14(f20(a21)))),
% 126.35/126.42 inference(scs_inference,[],[57,211,720,2672,492,133,134,145,146,118,119,120,121,153,317,23])).
% 126.35/126.42 cnf(2776,plain,
% 126.35/126.42 (E(f17(f20(a2)),f17(f20(a21)))),
% 126.35/126.42 inference(scs_inference,[],[57,211,720,2672,492,133,134,145,146,118,119,120,121,153,317,23,24])).
% 126.35/126.42 cnf(2777,plain,
% 126.35/126.42 (E(f35(f20(a2)),f35(f20(a21)))),
% 126.35/126.42 inference(scs_inference,[],[57,211,720,2672,492,133,134,145,146,118,119,120,121,153,317,23,24,27])).
% 126.35/126.42 cnf(2778,plain,
% 126.35/126.42 (E(f36(f20(a2)),f36(f20(a21)))),
% 126.35/126.42 inference(scs_inference,[],[57,211,720,2672,492,133,134,145,146,118,119,120,121,153,317,23,24,27,28])).
% 126.35/126.42 cnf(2779,plain,
% 126.35/126.42 (E(f34(f20(a2)),f34(f20(a21)))),
% 126.35/126.42 inference(scs_inference,[],[57,211,720,2672,492,133,134,145,146,118,119,120,121,153,317,23,24,27,28,37])).
% 126.35/126.42 cnf(2780,plain,
% 126.35/126.42 (~E(f30(x27801,a3),f30(x27802,a2))),
% 126.35/126.42 inference(scs_inference,[],[57,211,720,2672,492,133,134,145,146,118,119,120,121,153,317,23,24,27,28,37,135])).
% 126.35/126.42 cnf(2782,plain,
% 126.35/126.42 (~E(f30(a3,x27821),f30(a2,x27822))),
% 126.35/126.42 inference(scs_inference,[],[57,211,720,2672,492,133,134,145,146,118,119,120,121,153,317,23,24,27,28,37,135,136])).
% 126.35/126.42 cnf(2785,plain,
% 126.35/126.42 (E(f27(x27851,f20(a2)),f27(x27851,f20(a21)))),
% 126.35/126.42 inference(scs_inference,[],[57,211,720,2672,492,133,134,145,146,118,119,120,121,153,317,23,24,27,28,37,135,136,5,6])).
% 126.35/126.42 cnf(2792,plain,
% 126.35/126.42 (E(f9(f24(f9(x27921,x27922)),f47(f9(x27921,x27922))),f9(x27921,x27922))),
% 126.35/126.42 inference(scs_inference,[],[57,211,107,720,2672,492,133,134,145,146,118,119,120,121,153,317,23,24,27,28,37,135,136,5,6,15,16,35,36,40,41,124])).
% 126.35/126.42 cnf(2794,plain,
% 126.35/126.42 (E(f44(f29(f9(x27941,x27942)),f28(f9(x27941,x27942))),f9(x27941,x27942))),
% 126.35/126.42 inference(scs_inference,[],[57,211,107,720,2672,492,133,134,145,146,118,119,120,121,153,317,23,24,27,28,37,135,136,5,6,15,16,35,36,40,41,124,125])).
% 126.35/126.42 cnf(2798,plain,
% 126.35/126.42 (~P3(f35(x27981),f42(f20(x27981)))),
% 126.35/126.42 inference(scs_inference,[],[57,211,107,720,2672,1757,492,64,133,134,145,146,118,119,120,121,153,317,23,24,27,28,37,135,136,5,6,15,16,35,36,40,41,124,125,159,267])).
% 126.35/126.42 cnf(2807,plain,
% 126.35/126.42 (E(f16(f20(a2),x28071,x28072,x28073,x28074,x28075,x28076),f16(f20(a21),x28071,x28072,x28073,x28074,x28075,x28076))),
% 126.35/126.42 inference(scs_inference,[],[57,211,107,720,2672,1757,492,64,133,134,145,146,118,119,120,121,153,317,23,24,27,28,37,135,136,5,6,15,16,35,36,40,41,124,125,159,267,29,30,31,32,33,34,7])).
% 126.35/126.42 cnf(2808,plain,
% 126.35/126.42 (E(f16(x28081,f20(a2),x28082,x28083,x28084,x28085,x28086),f16(x28081,f20(a21),x28082,x28083,x28084,x28085,x28086))),
% 126.35/126.42 inference(scs_inference,[],[57,211,107,720,2672,1757,492,64,133,134,145,146,118,119,120,121,153,317,23,24,27,28,37,135,136,5,6,15,16,35,36,40,41,124,125,159,267,29,30,31,32,33,34,7,8])).
% 126.35/126.42 cnf(2809,plain,
% 126.35/126.42 (E(f16(x28091,x28092,f20(a2),x28093,x28094,x28095,x28096),f16(x28091,x28092,f20(a21),x28093,x28094,x28095,x28096))),
% 126.35/126.42 inference(scs_inference,[],[57,211,107,720,2672,1757,492,64,133,134,145,146,118,119,120,121,153,317,23,24,27,28,37,135,136,5,6,15,16,35,36,40,41,124,125,159,267,29,30,31,32,33,34,7,8,9])).
% 126.35/126.42 cnf(2810,plain,
% 126.35/126.42 (E(f16(x28101,x28102,x28103,f20(a2),x28104,x28105,x28106),f16(x28101,x28102,x28103,f20(a21),x28104,x28105,x28106))),
% 126.35/126.42 inference(scs_inference,[],[57,211,107,720,2672,1757,492,64,133,134,145,146,118,119,120,121,153,317,23,24,27,28,37,135,136,5,6,15,16,35,36,40,41,124,125,159,267,29,30,31,32,33,34,7,8,9,10])).
% 126.35/126.42 cnf(2811,plain,
% 126.35/126.42 (E(f16(x28111,x28112,x28113,x28114,f20(a2),x28115,x28116),f16(x28111,x28112,x28113,x28114,f20(a21),x28115,x28116))),
% 126.35/126.42 inference(scs_inference,[],[57,211,107,720,2672,1757,492,64,133,134,145,146,118,119,120,121,153,317,23,24,27,28,37,135,136,5,6,15,16,35,36,40,41,124,125,159,267,29,30,31,32,33,34,7,8,9,10,11])).
% 126.35/126.42 cnf(2815,plain,
% 126.35/126.42 (E(f25(f20(a2)),f25(f20(a21)))),
% 126.35/126.42 inference(scs_inference,[],[57,211,107,720,2672,1757,492,64,133,134,145,146,118,119,120,121,153,317,23,24,27,28,37,135,136,5,6,15,16,35,36,40,41,124,125,159,267,29,30,31,32,33,34,7,8,9,10,11,12,13,22,19])).
% 126.35/126.42 cnf(2821,plain,
% 126.35/126.42 (E(f42(f20(a2)),f42(f20(a21)))),
% 126.35/126.42 inference(scs_inference,[],[57,211,107,720,2672,2070,1757,492,64,133,134,145,146,118,119,120,121,153,317,23,24,27,28,37,135,136,5,6,15,16,35,36,40,41,124,125,159,267,29,30,31,32,33,34,7,8,9,10,11,12,13,22,19,26,25,21,143,14])).
% 126.35/126.42 cnf(2824,plain,
% 126.35/126.42 (E(f47(f20(a2)),f47(f20(a21)))),
% 126.35/126.42 inference(scs_inference,[],[57,211,107,720,2672,2070,1757,492,64,133,134,145,146,118,119,120,121,153,317,23,24,27,28,37,135,136,5,6,15,16,35,36,40,41,124,125,159,267,29,30,31,32,33,34,7,8,9,10,11,12,13,22,19,26,25,21,143,14,129,38])).
% 126.35/126.42 cnf(2825,plain,
% 126.35/126.42 (E(f24(f20(a2)),f24(f20(a21)))),
% 126.35/126.42 inference(scs_inference,[],[57,211,107,720,2672,2070,1757,492,64,133,134,145,146,118,119,120,121,153,317,23,24,27,28,37,135,136,5,6,15,16,35,36,40,41,124,125,159,267,29,30,31,32,33,34,7,8,9,10,11,12,13,22,19,26,25,21,143,14,129,38,42])).
% 126.35/126.42 cnf(2826,plain,
% 126.35/126.42 (E(f29(f20(a2)),f29(f20(a21)))),
% 126.35/126.42 inference(scs_inference,[],[57,211,107,720,2672,2070,1757,492,64,133,134,145,146,118,119,120,121,153,317,23,24,27,28,37,135,136,5,6,15,16,35,36,40,41,124,125,159,267,29,30,31,32,33,34,7,8,9,10,11,12,13,22,19,26,25,21,143,14,129,38,42,43])).
% 126.35/126.42 cnf(2827,plain,
% 126.35/126.42 (P1(f44(f24(f9(a1,x28271)),f35(x28272)))),
% 126.35/126.42 inference(scs_inference,[],[57,211,107,720,2672,2070,1757,492,64,133,134,145,146,118,119,120,121,153,317,23,24,27,28,37,135,136,5,6,15,16,35,36,40,41,124,125,159,267,29,30,31,32,33,34,7,8,9,10,11,12,13,22,19,26,25,21,143,14,129,38,42,43,139])).
% 126.35/126.42 cnf(2829,plain,
% 126.35/126.42 (E(f28(f20(a2)),f28(f20(a21)))),
% 126.35/126.42 inference(scs_inference,[],[57,211,107,720,2672,2070,1757,492,64,133,134,145,146,118,119,120,121,153,317,23,24,27,28,37,135,136,5,6,15,16,35,36,40,41,124,125,159,267,29,30,31,32,33,34,7,8,9,10,11,12,13,22,19,26,25,21,143,14,129,38,42,43,139,39])).
% 126.35/126.42 cnf(2834,plain,
% 126.35/126.42 (E(f20(f20(a2)),f20(f20(a21)))),
% 126.35/126.42 inference(scs_inference,[],[57,211,107,720,2672,2070,1757,492,64,77,133,134,145,146,118,119,120,121,153,317,23,24,27,28,37,135,136,5,6,15,16,35,36,40,41,124,125,159,267,29,30,31,32,33,34,7,8,9,10,11,12,13,22,19,26,25,21,143,14,129,38,42,43,139,39,266,117,4])).
% 126.35/126.42 cnf(2836,plain,
% 126.35/126.42 (E(f32(f20(a2)),f32(f20(a21)))),
% 126.35/126.42 inference(scs_inference,[],[57,211,107,720,2672,2070,1757,492,64,77,133,134,145,146,118,119,120,121,153,317,23,24,27,28,37,135,136,5,6,15,16,35,36,40,41,124,125,159,267,29,30,31,32,33,34,7,8,9,10,11,12,13,22,19,26,25,21,143,14,129,38,42,43,139,39,266,117,4,18,20])).
% 126.35/126.42 cnf(2841,plain,
% 126.35/126.42 (E(f41(f20(a2)),f41(f20(a21)))),
% 126.35/126.42 inference(scs_inference,[],[57,211,107,720,2672,2031,2070,1757,492,64,77,133,134,145,146,118,119,120,121,153,317,23,24,27,28,37,135,136,5,6,15,16,35,36,40,41,124,125,159,267,29,30,31,32,33,34,7,8,9,10,11,12,13,22,19,26,25,21,143,14,129,38,42,43,139,39,266,117,4,18,20,138,132,17])).
% 126.35/126.42 cnf(2844,plain,
% 126.35/126.42 (P2(f20(a2),f20(a21))),
% 126.35/126.42 inference(scs_inference,[],[57,211,107,720,2672,2031,2070,1757,492,64,77,133,134,145,146,118,119,120,121,153,317,23,24,27,28,37,135,136,5,6,15,16,35,36,40,41,124,125,159,267,29,30,31,32,33,34,7,8,9,10,11,12,13,22,19,26,25,21,143,14,129,38,42,43,139,39,266,117,4,18,20,138,132,17,126,123])).
% 126.35/126.42 cnf(2846,plain,
% 126.35/126.42 (~E(a2,a3)),
% 126.35/126.42 inference(scs_inference,[],[57,211,107,720,2672,2031,2070,1757,492,64,77,133,134,145,146,118,119,120,121,153,317,23,24,27,28,37,135,136,5,6,15,16,35,36,40,41,124,125,159,267,29,30,31,32,33,34,7,8,9,10,11,12,13,22,19,26,25,21,143,14,129,38,42,43,139,39,266,117,4,18,20,138,132,17,126,123,2])).
% 126.35/126.42 cnf(2847,plain,
% 126.35/126.42 (~P5(f14(f25(a39)),a5)),
% 126.35/126.42 inference(scs_inference,[],[57,211,107,720,2672,2031,2070,1757,492,64,251,104,77,133,134,145,146,118,119,120,121,153,317,23,24,27,28,37,135,136,5,6,15,16,35,36,40,41,124,125,159,267,29,30,31,32,33,34,7,8,9,10,11,12,13,22,19,26,25,21,143,14,129,38,42,43,139,39,266,117,4,18,20,138,132,17,126,123,2,45])).
% 126.35/126.42 cnf(2848,plain,
% 126.35/126.42 (E(f14(f25(x28481)),x28481)),
% 126.35/126.42 inference(rename_variables,[],[251])).
% 126.35/126.42 cnf(2849,plain,
% 126.35/126.42 (~P5(x28491,f14(f25(a45)))),
% 126.35/126.42 inference(scs_inference,[],[57,211,107,720,2672,2031,2070,1757,492,64,106,251,2848,104,77,133,134,145,146,118,119,120,121,153,317,23,24,27,28,37,135,136,5,6,15,16,35,36,40,41,124,125,159,267,29,30,31,32,33,34,7,8,9,10,11,12,13,22,19,26,25,21,143,14,129,38,42,43,139,39,266,117,4,18,20,138,132,17,126,123,2,45,46])).
% 126.35/126.42 cnf(2850,plain,
% 126.35/126.42 (E(f14(f25(x28501)),x28501)),
% 126.35/126.42 inference(rename_variables,[],[251])).
% 126.35/126.42 cnf(2853,plain,
% 126.35/126.42 (~P3(a3,f9(a2,a1))),
% 126.35/126.42 inference(scs_inference,[],[57,211,107,720,2672,2031,2070,1757,2693,492,64,106,251,2848,104,105,1181,77,133,134,145,146,118,119,120,121,153,317,23,24,27,28,37,135,136,5,6,15,16,35,36,40,41,124,125,159,267,29,30,31,32,33,34,7,8,9,10,11,12,13,22,19,26,25,21,143,14,129,38,42,43,139,39,266,117,4,18,20,138,132,17,126,123,2,45,46,144,152])).
% 126.35/126.42 cnf(2854,plain,
% 126.35/126.42 (~P3(x28541,a1)),
% 126.35/126.42 inference(rename_variables,[],[105])).
% 126.35/126.42 cnf(2857,plain,
% 126.35/126.42 (E(f14(f25(x28571)),x28571)),
% 126.35/126.42 inference(rename_variables,[],[251])).
% 126.35/126.42 cnf(2858,plain,
% 126.35/126.42 (~P3(a3,f44(a1,a2))),
% 126.35/126.42 inference(scs_inference,[],[57,211,107,720,2672,2031,2070,1757,2693,492,64,106,276,251,2848,2850,104,105,2854,1181,77,133,134,145,146,118,119,120,121,153,317,23,24,27,28,37,135,136,5,6,15,16,35,36,40,41,124,125,159,267,29,30,31,32,33,34,7,8,9,10,11,12,13,22,19,26,25,21,143,14,129,38,42,43,139,39,266,117,4,18,20,138,132,17,126,123,2,45,46,144,152,53,151])).
% 126.35/126.42 cnf(2861,plain,
% 126.35/126.42 (E(a33,f41(f20(a3)))),
% 126.35/126.42 inference(scs_inference,[],[57,211,107,720,2672,2031,2070,1757,2693,492,64,106,276,251,2848,2850,104,105,2854,1181,73,77,133,134,145,146,118,119,120,121,153,317,23,24,27,28,37,135,136,5,6,15,16,35,36,40,41,124,125,159,267,29,30,31,32,33,34,7,8,9,10,11,12,13,22,19,26,25,21,143,14,129,38,42,43,139,39,266,117,4,18,20,138,132,17,126,123,2,45,46,144,152,53,151,140])).
% 126.35/126.42 cnf(2863,plain,
% 126.35/126.42 (~P2(f41(f20(a22)),f14(f25(a46)))),
% 126.35/126.42 inference(scs_inference,[],[57,211,107,720,2672,2031,2070,1757,2693,492,64,106,276,251,2848,2850,2857,104,105,2854,1181,73,77,133,134,145,146,118,119,120,121,153,317,23,24,27,28,37,135,136,5,6,15,16,35,36,40,41,124,125,159,267,29,30,31,32,33,34,7,8,9,10,11,12,13,22,19,26,25,21,143,14,129,38,42,43,139,39,266,117,4,18,20,138,132,17,126,123,2,45,46,144,152,53,151,140,48])).
% 126.35/126.42 cnf(2864,plain,
% 126.35/126.42 (E(f14(f25(x28641)),x28641)),
% 126.35/126.42 inference(rename_variables,[],[251])).
% 126.35/126.42 cnf(2866,plain,
% 126.35/126.42 (E(f14(f25(x28661)),x28661)),
% 126.35/126.42 inference(rename_variables,[],[251])).
% 126.35/126.42 cnf(2867,plain,
% 126.35/126.42 (~P2(f27(a37,f20(a2)),f20(a3))),
% 126.35/126.42 inference(scs_inference,[],[57,211,107,490,720,2672,2031,2070,1757,2693,492,64,106,276,251,2848,2850,2857,2864,442,104,105,2854,1181,73,77,133,134,145,146,118,119,120,121,153,317,23,24,27,28,37,135,136,5,6,15,16,35,36,40,41,124,125,159,267,29,30,31,32,33,34,7,8,9,10,11,12,13,22,19,26,25,21,143,14,129,38,42,43,139,39,266,117,4,18,20,138,132,17,126,123,2,45,46,144,152,53,151,140,48,47,137])).
% 126.35/126.42 cnf(2871,plain,
% 126.35/126.42 (E(x28711,f14(f25(x28711)))),
% 126.35/126.42 inference(rename_variables,[],[492])).
% 126.35/126.42 cnf(2872,plain,
% 126.35/126.42 (~P3(f14(f25(f26(a2))),f42(f20(a21)))),
% 126.35/126.42 inference(scs_inference,[],[57,211,107,490,720,2672,2031,2070,1757,2693,492,2774,64,106,276,251,2848,2850,2857,2864,2866,442,104,105,2854,1181,73,77,133,134,145,146,118,119,120,121,153,317,23,24,27,28,37,135,136,5,6,15,16,35,36,40,41,124,125,159,267,29,30,31,32,33,34,7,8,9,10,11,12,13,22,19,26,25,21,143,14,129,38,42,43,139,39,266,117,4,18,20,138,132,17,126,123,2,45,46,144,152,53,151,140,48,47,137,3,52])).
% 126.35/126.42 cnf(2874,plain,
% 126.35/126.42 (~E(f20(a2),f20(a4))),
% 126.35/126.42 inference(scs_inference,[],[57,211,107,490,720,2672,2031,2070,1757,2693,492,2774,64,106,276,251,2848,2850,2857,2864,2866,442,104,105,2854,1181,73,77,133,134,145,146,118,119,120,121,153,317,23,24,27,28,37,135,136,5,6,15,16,35,36,40,41,124,125,159,267,29,30,31,32,33,34,7,8,9,10,11,12,13,22,19,26,25,21,143,14,129,38,42,43,139,39,266,117,4,18,20,138,132,17,126,123,2,45,46,144,152,53,151,140,48,47,137,3,52,362])).
% 126.35/126.42 cnf(2875,plain,
% 126.35/126.42 (~E(f20(a2),f20(a12))),
% 126.35/126.42 inference(scs_inference,[],[57,211,107,490,720,2672,2031,2070,1757,2693,492,2774,64,106,276,251,2848,2850,2857,2864,2866,442,104,105,2854,1181,73,77,133,134,145,146,118,119,120,121,153,317,23,24,27,28,37,135,136,5,6,15,16,35,36,40,41,124,125,159,267,29,30,31,32,33,34,7,8,9,10,11,12,13,22,19,26,25,21,143,14,129,38,42,43,139,39,266,117,4,18,20,138,132,17,126,123,2,45,46,144,152,53,151,140,48,47,137,3,52,362,560])).
% 126.35/126.42 cnf(2876,plain,
% 126.35/126.42 (~P5(f20(a2),f27(a10,f20(a3)))),
% 126.35/126.42 inference(scs_inference,[],[57,211,107,490,720,2672,2031,2070,1757,2693,492,2774,64,106,276,251,2848,2850,2857,2864,2866,442,104,105,2854,1181,73,77,133,134,145,146,118,119,120,121,153,317,23,24,27,28,37,135,136,5,6,15,16,35,36,40,41,124,125,159,267,29,30,31,32,33,34,7,8,9,10,11,12,13,22,19,26,25,21,143,14,129,38,42,43,139,39,266,117,4,18,20,138,132,17,126,123,2,45,46,144,152,53,151,140,48,47,137,3,52,362,560,360])).
% 126.35/126.42 cnf(2880,plain,
% 126.35/126.42 (E(x28801,f14(f25(x28801)))),
% 126.35/126.42 inference(rename_variables,[],[492])).
% 126.35/126.42 cnf(2882,plain,
% 126.35/126.42 (E(x28821,f14(f25(x28821)))),
% 126.35/126.42 inference(rename_variables,[],[492])).
% 126.35/126.42 cnf(2884,plain,
% 126.35/126.42 (E(x28841,f14(f25(x28841)))),
% 126.35/126.42 inference(rename_variables,[],[492])).
% 126.35/126.42 cnf(2885,plain,
% 126.35/126.42 (P1(f14(f25(a1)))),
% 126.35/126.42 inference(scs_inference,[],[57,211,55,107,490,720,2621,2672,2031,2070,1757,2693,492,2774,2871,2880,2882,2884,64,106,276,251,2848,2850,2857,2864,2866,442,104,105,2854,1181,73,77,133,134,145,146,118,119,120,121,153,317,23,24,27,28,37,135,136,5,6,15,16,35,36,40,41,124,125,159,267,29,30,31,32,33,34,7,8,9,10,11,12,13,22,19,26,25,21,143,14,129,38,42,43,139,39,266,117,4,18,20,138,132,17,126,123,2,45,46,144,152,53,151,140,48,47,137,3,52,362,560,360,147,49,51,50,44])).
% 126.35/126.42 cnf(2887,plain,
% 126.35/126.42 (P2(f20(a3),f20(a2))),
% 126.35/126.42 inference(scs_inference,[],[57,211,55,107,490,720,2621,2672,2031,2070,1757,2693,492,2774,2871,2880,2882,2884,64,106,276,251,2848,2850,2857,2864,2866,442,104,71,105,2854,1181,73,77,133,134,145,146,118,119,120,121,153,317,23,24,27,28,37,135,136,5,6,15,16,35,36,40,41,124,125,159,267,29,30,31,32,33,34,7,8,9,10,11,12,13,22,19,26,25,21,143,14,129,38,42,43,139,39,266,117,4,18,20,138,132,17,126,123,2,45,46,144,152,53,151,140,48,47,137,3,52,362,560,360,147,49,51,50,44,154])).
% 126.35/126.42 cnf(2892,plain,
% 126.35/126.42 (E(f44(f29(f44(x28921,x28922)),f28(f44(x28921,x28922))),f44(x28921,x28922))),
% 126.35/126.42 inference(scs_inference,[],[108,125])).
% 126.35/126.42 cnf(2894,plain,
% 126.35/126.42 (P1(f44(f14(f25(a1)),f30(x28941,x28942)))),
% 126.35/126.42 inference(scs_inference,[],[108,2885,125,153])).
% 126.35/126.42 cnf(2896,plain,
% 126.35/126.42 (~P2(f41(f27(a37,f20(a2))),f41(f20(a3)))),
% 126.35/126.42 inference(scs_inference,[],[108,2867,2885,125,153,143])).
% 126.35/126.42 cnf(2904,plain,
% 126.35/126.42 (E(f9(f24(f44(x29041,x29042)),f47(f44(x29041,x29042))),f44(x29041,x29042))),
% 126.35/126.42 inference(scs_inference,[],[227,2844,108,2867,2885,125,153,143,267,120,135,124])).
% 126.35/126.42 cnf(2916,plain,
% 126.35/126.42 (P3(a33,f9(f41(f20(a3)),x29161))),
% 126.35/126.42 inference(scs_inference,[],[227,2844,108,2867,2861,2885,125,153,143,267,120,135,124,9,23,40,27,10,24,41,13,25,28,133])).
% 126.35/126.42 cnf(2918,plain,
% 126.35/126.42 (P3(f20(a2),f9(x29181,f9(f20(a21),x29182)))),
% 126.35/126.42 inference(scs_inference,[],[227,2844,108,2867,2861,2885,2755,125,153,143,267,120,135,124,9,23,40,27,10,24,41,13,25,28,133,145])).
% 126.35/126.42 cnf(2920,plain,
% 126.35/126.42 (P3(f20(a2),f44(f9(f20(a21),x29201),x29202))),
% 126.35/126.42 inference(scs_inference,[],[227,2844,108,2867,2861,2885,2755,125,153,143,267,120,135,124,9,23,40,27,10,24,41,13,25,28,133,145,146])).
% 126.35/126.42 cnf(2931,plain,
% 126.35/126.42 (P3(a33,f44(x29311,f41(f20(a3))))),
% 126.35/126.42 inference(scs_inference,[],[227,2844,108,2867,2861,2885,2755,125,153,143,267,120,135,124,9,23,40,27,10,24,41,13,25,28,133,145,146,7,5,30,12,26,119,118,134])).
% 126.35/126.42 cnf(2956,plain,
% 126.35/126.42 (P1(f44(f14(f25(a1)),f35(x29561)))),
% 126.35/126.42 inference(scs_inference,[],[227,2844,108,2867,2861,2885,2755,2834,788,125,153,143,267,120,135,124,9,23,40,27,10,24,41,13,25,28,133,145,146,7,5,30,12,26,119,118,134,129,19,36,136,32,121,159,6,8,37,11,34,38,29,22,43,21,35,33,139])).
% 126.35/126.42 cnf(2968,plain,
% 126.35/126.42 (E(f20(a33),f20(f41(f20(a3))))),
% 126.35/126.42 inference(scs_inference,[],[227,2844,108,2867,2861,2885,2755,2834,788,125,153,143,267,120,135,124,9,23,40,27,10,24,41,13,25,28,133,145,146,7,5,30,12,26,119,118,134,129,19,36,136,32,121,159,6,8,37,11,34,38,29,22,43,21,35,33,139,31,15,42,16,14,39,117,20,18,4])).
% 126.35/126.42 cnf(2969,plain,
% 126.35/126.42 (P2(f41(f20(a2)),f41(f20(a21)))),
% 126.35/126.42 inference(scs_inference,[],[227,2844,108,2867,2861,2885,2755,2834,788,125,153,143,267,120,135,124,9,23,40,27,10,24,41,13,25,28,133,145,146,7,5,30,12,26,119,118,134,129,19,36,136,32,121,159,6,8,37,11,34,38,29,22,43,21,35,33,139,31,15,42,16,14,39,117,20,18,4,138])).
% 126.35/126.42 cnf(2971,plain,
% 126.35/126.42 (P2(f20(a2),f41(f20(a21)))),
% 126.35/126.42 inference(scs_inference,[],[227,2844,108,2867,2861,2885,2755,2834,788,125,153,143,267,120,135,124,9,23,40,27,10,24,41,13,25,28,133,145,146,7,5,30,12,26,119,118,134,129,19,36,136,32,121,159,6,8,37,11,34,38,29,22,43,21,35,33,139,31,15,42,16,14,39,117,20,18,4,138,132])).
% 126.35/126.42 cnf(2973,plain,
% 126.35/126.42 (P2(f16(f20(a2),x29731,x29732,x29733,x29734,x29735,x29736),f16(f20(a21),x29731,x29732,x29733,x29734,x29735,x29736))),
% 126.35/126.42 inference(scs_inference,[],[227,2844,108,2867,2861,2885,2755,2807,2834,788,125,153,143,267,120,135,124,9,23,40,27,10,24,41,13,25,28,133,145,146,7,5,30,12,26,119,118,134,129,19,36,136,32,121,159,6,8,37,11,34,38,29,22,43,21,35,33,139,31,15,42,16,14,39,117,20,18,4,138,132,123])).
% 126.35/126.42 cnf(2977,plain,
% 126.35/126.42 (E(f41(a33),f41(f41(f20(a3))))),
% 126.35/126.42 inference(scs_inference,[],[227,2844,108,2867,2861,2885,2755,2807,2834,2863,788,125,153,143,267,120,135,124,9,23,40,27,10,24,41,13,25,28,133,145,146,7,5,30,12,26,119,118,134,129,19,36,136,32,121,159,6,8,37,11,34,38,29,22,43,21,35,33,139,31,15,42,16,14,39,117,20,18,4,138,132,123,126,17])).
% 126.35/126.42 cnf(2978,plain,
% 126.35/126.42 (~E(a39,a2)),
% 126.35/126.42 inference(scs_inference,[],[227,2844,108,2867,2861,2885,2755,2807,2834,2863,788,125,153,143,267,120,135,124,9,23,40,27,10,24,41,13,25,28,133,145,146,7,5,30,12,26,119,118,134,129,19,36,136,32,121,159,6,8,37,11,34,38,29,22,43,21,35,33,139,31,15,42,16,14,39,117,20,18,4,138,132,123,126,17,2])).
% 126.35/126.42 cnf(2980,plain,
% 126.35/126.42 (E(f24(f9(x29801,x29802)),x29801)),
% 126.35/126.42 inference(rename_variables,[],[78])).
% 126.35/126.42 cnf(2990,plain,
% 126.35/126.42 (~P3(a3,f44(f9(a2,a1),a4))),
% 126.35/126.42 inference(scs_inference,[],[227,338,2844,2853,108,2867,2861,2876,2885,2755,2807,2785,2834,2863,2792,2690,655,788,78,1181,125,153,143,267,120,135,124,9,23,40,27,10,24,41,13,25,28,133,145,146,7,5,30,12,26,119,118,134,129,19,36,136,32,121,159,6,8,37,11,34,38,29,22,43,21,35,33,139,31,15,42,16,14,39,117,20,18,4,138,132,123,126,17,2,45,46,144,152,53,151])).
% 126.35/126.42 cnf(2992,plain,
% 126.35/126.42 (~P2(f27(a37,f20(a2)),f24(f9(f20(a3),x29921)))),
% 126.35/126.42 inference(scs_inference,[],[227,338,2844,2853,108,2867,2861,2876,2885,2755,2807,2785,2834,2863,2792,2690,655,788,78,2980,1181,125,153,143,267,120,135,124,9,23,40,27,10,24,41,13,25,28,133,145,146,7,5,30,12,26,119,118,134,129,19,36,136,32,121,159,6,8,37,11,34,38,29,22,43,21,35,33,139,31,15,42,16,14,39,117,20,18,4,138,132,123,126,17,2,45,46,144,152,53,151,48])).
% 126.35/126.42 cnf(2994,plain,
% 126.35/126.42 (~P2(a33,a46)),
% 126.35/126.42 inference(scs_inference,[],[227,338,2844,2853,108,2867,2861,2876,2885,2755,2807,2785,2834,2863,2792,2690,1857,655,788,78,2980,1181,125,153,143,267,120,135,124,9,23,40,27,10,24,41,13,25,28,133,145,146,7,5,30,12,26,119,118,134,129,19,36,136,32,121,159,6,8,37,11,34,38,29,22,43,21,35,33,139,31,15,42,16,14,39,117,20,18,4,138,132,123,126,17,2,45,46,144,152,53,151,48,47])).
% 126.35/126.42 cnf(2995,plain,
% 126.35/126.42 (~P2(f41(f27(a37,f20(a2))),a46)),
% 126.35/126.42 inference(scs_inference,[],[227,338,2844,2853,108,2867,2861,2876,2885,2755,2807,2785,2834,2863,2792,2690,1857,655,2006,1994,788,78,2980,1181,125,153,143,267,120,135,124,9,23,40,27,10,24,41,13,25,28,133,145,146,7,5,30,12,26,119,118,134,129,19,36,136,32,121,159,6,8,37,11,34,38,29,22,43,21,35,33,139,31,15,42,16,14,39,117,20,18,4,138,132,123,126,17,2,45,46,144,152,53,151,48,47,137])).
% 126.35/126.42 cnf(3000,plain,
% 126.35/126.42 (~E(f20(a2),f20(a3))),
% 126.35/126.42 inference(scs_inference,[],[57,227,338,2846,2875,2844,2853,108,2867,2798,2861,2876,2885,2755,2807,2785,2777,2834,2863,2792,2690,1857,655,2006,1994,788,78,2980,1181,61,63,125,153,143,267,120,135,124,9,23,40,27,10,24,41,13,25,28,133,145,146,7,5,30,12,26,119,118,134,129,19,36,136,32,121,159,6,8,37,11,34,38,29,22,43,21,35,33,139,31,15,42,16,14,39,117,20,18,4,138,132,123,126,17,2,45,46,144,152,53,151,48,47,137,3,52,263])).
% 126.35/126.42 cnf(3006,plain,
% 126.35/126.42 (P2(a46,f41(a33))),
% 126.35/126.42 inference(scs_inference,[],[2994,506])).
% 126.35/126.42 cnf(3007,plain,
% 126.35/126.42 (E(f44(f29(f41(a1)),f28(f41(a1))),f41(a1))),
% 126.35/126.42 inference(scs_inference,[],[206,125])).
% 126.35/126.42 cnf(3008,plain,
% 126.35/126.42 (~E(f41(x30081),x30081)),
% 126.35/126.42 inference(rename_variables,[],[206])).
% 126.35/126.42 cnf(3010,plain,
% 126.35/126.42 (~P2(f41(a33),f41(a46))),
% 126.35/126.42 inference(scs_inference,[],[2994,206,125,143])).
% 126.35/126.42 cnf(3014,plain,
% 126.35/126.42 (P1(f44(f44(f24(f9(a1,x30141)),f30(x30142,x30143)),f30(x30144,x30145)))),
% 126.35/126.42 inference(scs_inference,[],[228,2994,2771,206,125,143,118,153])).
% 126.35/126.42 cnf(3016,plain,
% 126.35/126.42 (P3(f16(x30161,f20(a2),x30162,x30163,x30164,x30165,x30166),f9(f16(x30161,f20(a21),x30162,x30163,x30164,x30165,x30166),x30167))),
% 126.35/126.42 inference(scs_inference,[],[228,2994,2771,2808,206,125,143,118,153,133])).
% 126.35/126.42 cnf(3018,plain,
% 126.35/126.42 (E(f9(f24(f41(a1)),f47(f41(a1))),f41(a1))),
% 126.35/126.42 inference(scs_inference,[],[228,2994,2771,2808,206,3008,125,143,118,153,133,124])).
% 126.35/126.42 cnf(3025,plain,
% 126.35/126.42 (P3(f20(a2),f9(x30251,f44(x30252,f20(a21))))),
% 126.35/126.42 inference(scs_inference,[],[228,2994,2887,2757,2771,2808,206,3008,125,143,118,153,133,124,267,23,27,145])).
% 126.35/126.42 cnf(3041,plain,
% 126.35/126.42 (P1(f44(f44(f24(f9(a1,x30411)),f30(x30412,x30413)),f35(x30414)))),
% 126.35/126.42 inference(scs_inference,[],[228,2994,2887,2757,2771,2808,2968,206,3008,125,143,118,153,133,124,267,23,27,145,24,10,129,41,40,120,119,135,12,26,139])).
% 126.35/126.42 cnf(3046,plain,
% 126.35/126.42 (P3(f20(a2),f44(f44(x30461,f20(a21)),x30462))),
% 126.35/126.42 inference(scs_inference,[],[228,2994,2887,2757,2771,2808,2968,530,206,3008,125,143,118,153,133,124,267,23,27,145,24,10,129,41,40,120,119,135,12,26,139,37,159,146])).
% 126.35/126.42 cnf(3056,plain,
% 126.35/126.42 (P3(f16(x30561,f20(a2),x30562,x30563,x30564,x30565,x30566),f44(x30567,f16(x30561,f20(a21),x30562,x30563,x30564,x30565,x30566)))),
% 126.35/126.42 inference(scs_inference,[],[228,2994,2887,2757,2771,2808,2968,530,206,3008,125,143,118,153,133,124,267,23,27,145,24,10,129,41,40,120,119,135,12,26,139,37,159,146,11,13,25,36,30,6,121,134])).
% 126.35/126.42 cnf(3084,plain,
% 126.35/126.42 (P2(f41(f20(a3)),f41(f20(a2)))),
% 126.35/126.42 inference(scs_inference,[],[228,2994,2887,2757,2771,2808,2968,530,206,3008,125,143,118,153,133,124,267,23,27,145,24,10,129,41,40,120,119,135,12,26,139,37,159,146,11,13,25,36,30,6,121,134,136,29,32,35,9,42,38,8,21,5,19,28,43,14,15,7,34,16,31,22,33,117,39,20,138])).
% 126.35/126.42 cnf(3088,plain,
% 126.35/126.42 (P2(f20(a3),f41(f20(a2)))),
% 126.35/126.42 inference(scs_inference,[],[228,2994,2887,2757,2771,2808,2968,530,206,3008,125,143,118,153,133,124,267,23,27,145,24,10,129,41,40,120,119,135,12,26,139,37,159,146,11,13,25,36,30,6,121,134,136,29,32,35,9,42,38,8,21,5,19,28,43,14,15,7,34,16,31,22,33,117,39,20,138,4,18,132])).
% 126.35/126.42 cnf(3092,plain,
% 126.35/126.42 (P2(f16(x30921,f20(a2),x30922,x30923,x30924,x30925,x30926),f16(x30921,f20(a21),x30922,x30923,x30924,x30925,x30926))),
% 126.35/126.42 inference(scs_inference,[],[228,2994,2887,2757,2771,2808,2968,2896,530,206,3008,125,143,118,153,133,124,267,23,27,145,24,10,129,41,40,120,119,135,12,26,139,37,159,146,11,13,25,36,30,6,121,134,136,29,32,35,9,42,38,8,21,5,19,28,43,14,15,7,34,16,31,22,33,117,39,20,138,4,18,132,126,123])).
% 126.35/126.42 cnf(3095,plain,
% 126.35/126.42 (~E(a45,a5)),
% 126.35/126.42 inference(scs_inference,[],[228,2994,2887,2757,2771,2808,2968,2896,530,206,3008,125,143,118,153,133,124,267,23,27,145,24,10,129,41,40,120,119,135,12,26,139,37,159,146,11,13,25,36,30,6,121,134,136,29,32,35,9,42,38,8,21,5,19,28,43,14,15,7,34,16,31,22,33,117,39,20,138,4,18,132,126,123,17,2])).
% 126.35/126.42 cnf(3097,plain,
% 126.35/126.42 (E(f14(f25(x30971)),x30971)),
% 126.35/126.42 inference(rename_variables,[],[251])).
% 126.35/126.42 cnf(3098,plain,
% 126.35/126.42 (P2(f20(a3),f41(f20(a21)))),
% 126.35/126.42 inference(scs_inference,[],[228,2994,2887,2757,2971,2771,2808,2968,2896,2876,530,251,206,3008,125,143,118,153,133,124,267,23,27,145,24,10,129,41,40,120,119,135,12,26,139,37,159,146,11,13,25,36,30,6,121,134,136,29,32,35,9,42,38,8,21,5,19,28,43,14,15,7,34,16,31,22,33,117,39,20,138,4,18,132,126,123,17,2,45,144])).
% 126.35/126.42 cnf(3100,plain,
% 126.35/126.42 (~P5(f14(f25(a39)),f14(f25(a5)))),
% 126.35/126.42 inference(scs_inference,[],[228,2994,2887,2757,2971,2847,2771,2808,2968,2896,2876,530,251,3097,206,3008,125,143,118,153,133,124,267,23,27,145,24,10,129,41,40,120,119,135,12,26,139,37,159,146,11,13,25,36,30,6,121,134,136,29,32,35,9,42,38,8,21,5,19,28,43,14,15,7,34,16,31,22,33,117,39,20,138,4,18,132,126,123,17,2,45,144,46])).
% 126.35/126.42 cnf(3101,plain,
% 126.35/126.42 (E(f14(f25(x31011)),x31011)),
% 126.35/126.42 inference(rename_variables,[],[251])).
% 126.35/126.42 cnf(3102,plain,
% 126.35/126.42 (~P3(a5,f9(a45,a1))),
% 126.35/126.42 inference(scs_inference,[],[228,2994,2887,2757,2971,2847,2771,2808,2968,2896,2876,530,251,3097,105,206,3008,125,143,118,153,133,124,267,23,27,145,24,10,129,41,40,120,119,135,12,26,139,37,159,146,11,13,25,36,30,6,121,134,136,29,32,35,9,42,38,8,21,5,19,28,43,14,15,7,34,16,31,22,33,117,39,20,138,4,18,132,126,123,17,2,45,144,46,152])).
% 126.35/126.42 cnf(3103,plain,
% 126.35/126.42 (~P3(x31031,a1)),
% 126.35/126.42 inference(rename_variables,[],[105])).
% 126.35/126.42 cnf(3107,plain,
% 126.35/126.42 (~P3(a5,f44(a1,a45))),
% 126.35/126.42 inference(scs_inference,[],[228,2994,2887,2858,2757,2971,2847,2771,2808,2968,2892,2896,2876,530,251,3097,105,3103,206,3008,125,143,118,153,133,124,267,23,27,145,24,10,129,41,40,120,119,135,12,26,139,37,159,146,11,13,25,36,30,6,121,134,136,29,32,35,9,42,38,8,21,5,19,28,43,14,15,7,34,16,31,22,33,117,39,20,138,4,18,132,126,123,17,2,45,144,46,152,53,151])).
% 126.35/126.42 cnf(3110,plain,
% 126.35/126.42 (~P2(a33,f14(f25(a46)))),
% 126.35/126.42 inference(scs_inference,[],[228,2994,2887,2858,2757,2971,2847,2771,2808,2968,2892,2896,2876,530,251,3097,3101,105,3103,206,3008,125,143,118,153,133,124,267,23,27,145,24,10,129,41,40,120,119,135,12,26,139,37,159,146,11,13,25,36,30,6,121,134,136,29,32,35,9,42,38,8,21,5,19,28,43,14,15,7,34,16,31,22,33,117,39,20,138,4,18,132,126,123,17,2,45,144,46,152,53,151,48])).
% 126.35/126.42 cnf(3111,plain,
% 126.35/126.42 (E(f14(f25(x31111)),x31111)),
% 126.35/126.42 inference(rename_variables,[],[251])).
% 126.35/126.42 cnf(3112,plain,
% 126.35/126.42 (~P2(f14(f25(a33)),a46)),
% 126.35/126.42 inference(scs_inference,[],[228,2994,2887,2858,2757,2971,2847,2771,2808,2968,2892,2896,2876,530,251,3097,3101,3111,105,3103,206,3008,125,143,118,153,133,124,267,23,27,145,24,10,129,41,40,120,119,135,12,26,139,37,159,146,11,13,25,36,30,6,121,134,136,29,32,35,9,42,38,8,21,5,19,28,43,14,15,7,34,16,31,22,33,117,39,20,138,4,18,132,126,123,17,2,45,144,46,152,53,151,48,47])).
% 126.35/126.42 cnf(3114,plain,
% 126.35/126.42 (~P2(f20(a4),f20(a2))),
% 126.35/126.42 inference(scs_inference,[],[228,2994,2874,2887,2858,2757,2971,2847,2771,2808,2968,2892,2896,2876,468,530,251,3097,3101,3111,105,3103,206,3008,125,143,118,153,133,124,267,23,27,145,24,10,129,41,40,120,119,135,12,26,139,37,159,146,11,13,25,36,30,6,121,134,136,29,32,35,9,42,38,8,21,5,19,28,43,14,15,7,34,16,31,22,33,117,39,20,138,4,18,132,126,123,17,2,45,144,46,152,53,151,48,47,137])).
% 126.35/126.42 cnf(3125,plain,
% 126.35/126.42 (P2(f41(a46),f41(f41(a33)))),
% 126.35/126.42 inference(scs_inference,[],[3010,480])).
% 126.35/126.42 cnf(3126,plain,
% 126.35/126.42 (P2(a46,f41(a33))),
% 126.35/126.42 inference(scs_inference,[],[3006,500])).
% 126.35/126.42 cnf(3127,plain,
% 126.35/126.42 (P2(f41(a46),f41(a33))),
% 126.35/126.42 inference(scs_inference,[],[3006,693])).
% 126.35/126.42 cnf(3136,plain,
% 126.35/126.42 (P1(f44(f44(f24(f9(a1,x31361)),f35(x31362)),f30(x31363,x31364)))),
% 126.35/126.42 inference(scs_inference,[],[291,2827,2918,468,145,118,267,135,153])).
% 126.35/126.42 cnf(3138,plain,
% 126.35/126.42 (~P2(f41(f41(a33)),f41(f41(a46)))),
% 126.35/126.42 inference(scs_inference,[],[291,3010,2827,2918,468,145,118,267,135,153,143])).
% 126.35/126.42 cnf(3150,plain,
% 126.35/126.42 (E(f42(f20(a2)),f9(f26(a22),f32(f25(a13))))),
% 126.35/126.42 inference(scs_inference,[],[291,3010,2827,2809,2918,548,468,145,118,267,135,153,143,27,24,146,133,10,120,41,159])).
% 126.35/126.42 cnf(3154,plain,
% 126.35/126.42 (E(f9(f16(x31541,x31542,f20(a2),x31543,x31544,x31545,x31546),x31547),f9(f16(x31541,x31542,f20(a21),x31543,x31544,x31545,x31546),x31547))),
% 126.35/126.42 inference(scs_inference,[],[291,3010,2827,2809,2918,548,468,145,118,267,135,153,143,27,24,146,133,10,120,41,159,121,25])).
% 126.35/126.42 cnf(3162,plain,
% 126.35/126.42 (P1(f44(f44(f24(f9(a1,x31621)),f35(x31622)),f35(x31623)))),
% 126.35/126.42 inference(scs_inference,[],[291,3010,2827,2809,2918,548,468,145,118,267,135,153,143,27,24,146,133,10,120,41,159,121,25,136,119,11,12,40,139])).
% 126.35/126.42 cnf(3192,plain,
% 126.35/126.42 (E(f44(x31921,f16(x31922,x31923,f20(a2),x31924,x31925,x31926,x31927)),f44(x31921,f16(x31922,x31923,f20(a21),x31924,x31925,x31926,x31927)))),
% 126.35/126.42 inference(scs_inference,[],[291,3010,2827,2809,2918,548,468,145,118,267,135,153,143,27,24,146,133,10,120,41,159,121,25,136,119,11,12,40,139,23,42,30,38,134,5,13,35,14,7,26,21,37,31,43,6,28,9,32,16,36,8,29,33,34,117,22])).
% 126.35/126.42 cnf(3197,plain,
% 126.35/126.42 (P2(a46,f41(f41(a33)))),
% 126.35/126.42 inference(scs_inference,[],[291,3006,3010,2827,2809,2918,548,468,145,118,267,135,153,143,27,24,146,133,10,120,41,159,121,25,136,119,11,12,40,139,23,42,30,38,134,5,13,35,14,7,26,21,37,31,43,6,28,9,32,16,36,8,29,33,34,117,22,19,15,39,20,132])).
% 126.35/126.42 cnf(3203,plain,
% 126.35/126.42 (P2(f16(x32031,x32032,f20(a2),x32033,x32034,x32035,x32036),f16(x32031,x32032,f20(a21),x32033,x32034,x32035,x32036))),
% 126.35/126.42 inference(scs_inference,[],[291,3006,3010,3088,2827,2809,2918,548,468,145,118,267,135,153,143,27,24,146,133,10,120,41,159,121,25,136,119,11,12,40,139,23,42,30,38,134,5,13,35,14,7,26,21,37,31,43,6,28,9,32,16,36,8,29,33,34,117,22,19,15,39,20,132,138,4,18,123])).
% 126.35/126.42 cnf(3205,plain,
% 126.35/126.42 (P2(f14(f25(a46)),a33)),
% 126.35/126.43 inference(scs_inference,[],[291,3006,3010,3088,3110,2827,2809,2918,548,468,145,118,267,135,153,143,27,24,146,133,10,120,41,159,121,25,136,119,11,12,40,139,23,42,30,38,134,5,13,35,14,7,26,21,37,31,43,6,28,9,32,16,36,8,29,33,34,117,22,19,15,39,20,132,138,4,18,123,126])).
% 126.35/126.43 cnf(3208,plain,
% 126.35/126.43 (~E(a3,a23)),
% 126.35/126.43 inference(scs_inference,[],[291,3006,3010,3088,3110,2827,2809,2918,548,468,145,118,267,135,153,143,27,24,146,133,10,120,41,159,121,25,136,119,11,12,40,139,23,42,30,38,134,5,13,35,14,7,26,21,37,31,43,6,28,9,32,16,36,8,29,33,34,117,22,19,15,39,20,132,138,4,18,123,126,17,2])).
% 126.35/126.43 cnf(3213,plain,
% 126.35/126.43 (~E(x32131,f41(f41(x32131)))),
% 126.35/126.43 inference(rename_variables,[],[550])).
% 126.35/126.43 cnf(3223,plain,
% 126.35/126.43 (~P2(f24(f9(f20(a22),x32231)),a46)),
% 126.35/126.43 inference(scs_inference,[],[291,3006,3010,3102,3088,3110,2827,2809,2821,2918,2872,2685,630,550,3213,328,1980,2785,1833,548,468,433,145,118,267,135,153,143,27,24,146,133,10,120,41,159,121,25,136,119,11,12,40,139,23,42,30,38,134,5,13,35,14,7,26,21,37,31,43,6,28,9,32,16,36,8,29,33,34,117,22,19,15,39,20,132,138,4,18,123,126,17,2,144,152,46,151,53,48,137])).
% 126.35/126.43 cnf(3235,plain,
% 126.35/126.43 (P2(f41(a46),f41(f41(a33)))),
% 126.35/126.43 inference(scs_inference,[],[3197,474])).
% 126.35/126.43 cnf(3236,plain,
% 126.35/126.43 (P2(f41(a46),f41(f41(a33)))),
% 126.35/126.43 inference(scs_inference,[],[3125,476])).
% 126.35/126.43 cnf(3237,plain,
% 126.35/126.43 (P2(a46,f41(a33))),
% 126.35/126.43 inference(scs_inference,[],[3197,494])).
% 126.35/126.43 cnf(3248,plain,
% 126.35/126.43 (E(f42(f20(a2)),f9(f26(a22),f32(f26(a13))))),
% 126.35/126.43 inference(scs_inference,[],[310,2920,2775,571,146,120,133,145,159])).
% 126.35/126.43 cnf(3255,plain,
% 126.35/126.43 (~E(f30(x32551,a21),f30(x32552,a39))),
% 126.35/126.43 inference(scs_inference,[],[310,2920,2775,571,416,146,120,133,145,159,267,10,118,135])).
% 126.35/126.43 cnf(3257,plain,
% 126.35/126.43 (~P2(f41(f20(a4)),f41(f20(a2)))),
% 126.35/126.43 inference(scs_inference,[],[310,3114,2920,2775,571,416,146,120,133,145,159,267,10,118,135,143])).
% 126.35/126.43 cnf(3259,plain,
% 126.35/126.43 (P1(f44(f44(f14(f25(a1)),f30(x32591,x32592)),f30(x32593,x32594)))),
% 126.35/126.43 inference(scs_inference,[],[310,3114,2894,2920,2775,571,416,146,120,133,145,159,267,10,118,135,143,153])).
% 126.35/126.43 cnf(3275,plain,
% 126.35/126.43 (P1(f44(f44(f14(f25(a1)),f30(x32751,x32752)),f35(x32753)))),
% 126.35/126.43 inference(scs_inference,[],[310,3114,2894,2920,2775,571,416,146,120,133,145,159,267,10,118,135,143,153,41,119,121,27,134,42,24,136,30,25,139])).
% 126.35/126.43 cnf(3315,plain,
% 126.35/126.43 (P2(a46,f14(f25(a33)))),
% 126.35/126.43 inference(scs_inference,[],[310,3127,3114,3125,3112,2894,2920,2775,571,416,146,120,133,145,159,267,10,118,135,143,153,41,119,121,27,134,42,24,136,30,25,139,11,117,23,6,28,13,14,38,16,31,12,26,32,33,40,43,35,29,15,37,8,19,9,5,22,21,7,20,36,39,34,132,138,4,18,126])).
% 126.35/126.43 cnf(3320,plain,
% 126.35/126.43 (~E(a39,a21)),
% 126.35/126.43 inference(scs_inference,[],[310,3127,3114,3125,3112,2894,2920,3150,2775,571,416,146,120,133,145,159,267,10,118,135,143,153,41,119,121,27,134,42,24,136,30,25,139,11,117,23,6,28,13,14,38,16,31,12,26,32,33,40,43,35,29,15,37,8,19,9,5,22,21,7,20,36,39,34,132,138,4,18,126,123,17,2])).
% 126.35/126.43 cnf(3321,plain,
% 126.35/126.43 (~P2(f41(a33),a46)),
% 126.35/126.43 inference(scs_inference,[],[310,3127,3114,3125,3112,2894,2920,3150,2775,571,416,114,146,120,133,145,159,267,10,118,135,143,153,41,119,121,27,134,42,24,136,30,25,139,11,117,23,6,28,13,14,38,16,31,12,26,32,33,40,43,35,29,15,37,8,19,9,5,22,21,7,20,36,39,34,132,138,4,18,126,123,17,2,144])).
% 126.35/126.43 cnf(3325,plain,
% 126.35/126.43 (~P3(x33251,a1)),
% 126.35/126.43 inference(rename_variables,[],[105])).
% 126.35/126.43 cnf(3327,plain,
% 126.35/126.43 (~P5(f14(f25(a39)),f24(f9(a5,x33271)))),
% 126.35/126.43 inference(scs_inference,[],[310,3127,3114,3125,3112,2894,2920,3150,2775,2847,571,416,78,105,114,146,120,133,145,159,267,10,118,135,143,153,41,119,121,27,134,42,24,136,30,25,139,11,117,23,6,28,13,14,38,16,31,12,26,32,33,40,43,35,29,15,37,8,19,9,5,22,21,7,20,36,39,34,132,138,4,18,126,123,17,2,144,152,46])).
% 126.35/126.43 cnf(3328,plain,
% 126.35/126.43 (E(f24(f9(x33281,x33282)),x33281)),
% 126.35/126.43 inference(rename_variables,[],[78])).
% 126.35/126.43 cnf(3329,plain,
% 126.35/126.43 (~P3(a21,f44(a1,a39))),
% 126.35/126.43 inference(scs_inference,[],[310,3127,3114,3125,3112,2894,2920,3150,2775,2847,571,416,78,105,3325,114,146,120,133,145,159,267,10,118,135,143,153,41,119,121,27,134,42,24,136,30,25,139,11,117,23,6,28,13,14,38,16,31,12,26,32,33,40,43,35,29,15,37,8,19,9,5,22,21,7,20,36,39,34,132,138,4,18,126,123,17,2,144,152,46,151])).
% 126.35/126.43 cnf(3334,plain,
% 126.35/126.43 (~P2(f20(a4),f20(a21))),
% 126.35/126.43 inference(scs_inference,[],[310,3127,3114,3107,3125,3112,2894,2920,3150,2775,2904,2847,571,416,210,78,105,3325,114,146,120,133,145,159,267,10,118,135,143,153,41,119,121,27,134,42,24,136,30,25,139,11,117,23,6,28,13,14,38,16,31,12,26,32,33,40,43,35,29,15,37,8,19,9,5,22,21,7,20,36,39,34,132,138,4,18,126,123,17,2,144,152,46,151,53,48])).
% 126.35/126.43 cnf(3335,plain,
% 126.35/126.43 (~P2(f41(f20(a21)),f20(a2))),
% 126.35/126.43 inference(scs_inference,[],[310,3127,3114,3107,304,3125,3112,2894,2920,3150,2775,2904,2971,2847,571,416,210,78,105,3325,114,146,120,133,145,159,267,10,118,135,143,153,41,119,121,27,134,42,24,136,30,25,139,11,117,23,6,28,13,14,38,16,31,12,26,32,33,40,43,35,29,15,37,8,19,9,5,22,21,7,20,36,39,34,132,138,4,18,126,123,17,2,144,152,46,151,53,48,137])).
% 126.35/126.43 cnf(3337,plain,
% 126.35/126.43 (~P2(f24(f9(f20(a4),x33371)),f20(a2))),
% 126.35/126.43 inference(scs_inference,[],[310,3127,3114,3107,304,3125,3112,2894,2920,3150,2775,2904,2971,2847,571,416,210,78,3328,105,3325,114,146,120,133,145,159,267,10,118,135,143,153,41,119,121,27,134,42,24,136,30,25,139,11,117,23,6,28,13,14,38,16,31,12,26,32,33,40,43,35,29,15,37,8,19,9,5,22,21,7,20,36,39,34,132,138,4,18,126,123,17,2,144,152,46,151,53,48,137,47])).
% 126.35/126.43 cnf(3354,plain,
% 126.35/126.43 (~E(f30(x33541,a12),f30(x33542,a3))),
% 126.35/126.43 inference(scs_inference,[],[312,3025,145,146,121,135])).
% 126.35/126.43 cnf(3358,plain,
% 126.35/126.43 (E(f42(f20(a21)),f9(f26(a22),f32(f26(a13))))),
% 126.35/126.43 inference(scs_inference,[],[312,3025,705,145,146,121,135,120,159])).
% 126.35/126.43 cnf(3362,plain,
% 126.35/126.43 (P1(f44(f44(f14(f25(a1)),f35(x33621)),f30(x33622,x33623)))),
% 126.35/126.43 inference(scs_inference,[],[312,354,2956,3025,705,145,146,121,135,120,159,118,153])).
% 126.35/126.43 cnf(3364,plain,
% 126.35/126.43 (~P2(f41(f20(a4)),f41(f20(a21)))),
% 126.35/126.43 inference(scs_inference,[],[312,354,3334,2956,3025,705,145,146,121,135,120,159,118,153,143])).
% 126.35/126.43 cnf(3377,plain,
% 126.35/126.43 (P1(f44(f44(f14(f25(a1)),f35(x33771)),f35(x33772)))),
% 126.35/126.43 inference(scs_inference,[],[312,354,3334,2956,3025,2776,705,145,146,121,135,120,159,118,153,143,133,134,119,41,42,10,25,24,139])).
% 126.35/126.43 cnf(3379,plain,
% 126.35/126.43 (~E(f30(a12,x33791),f30(a3,x33792))),
% 126.35/126.43 inference(scs_inference,[],[312,354,3334,2956,3025,2776,705,145,146,121,135,120,159,118,153,143,133,134,119,41,42,10,25,24,139,136])).
% 126.35/126.43 cnf(3402,plain,
% 126.35/126.43 (P2(a46,f41(f41(f41(a33))))),
% 126.35/126.43 inference(scs_inference,[],[312,354,3334,3197,3235,2956,3025,2776,705,145,146,121,135,120,159,118,153,143,133,134,119,41,42,10,25,24,139,136,117,27,6,30,28,23,12,13,38,35,11,14,15,138,40,22,33,37,9,132])).
% 126.35/126.43 cnf(3421,plain,
% 126.35/126.43 (P2(f41(f20(a2)),f41(f20(a4)))),
% 126.35/126.43 inference(scs_inference,[],[312,354,3334,3197,3235,2956,3257,3025,2776,705,145,146,121,135,120,159,118,153,143,133,134,119,41,42,10,25,24,139,136,117,27,6,30,28,23,12,13,38,35,11,14,15,138,40,22,33,37,9,132,16,21,31,26,43,19,32,34,29,5,8,7,20,39,36,4,18,126])).
% 126.35/126.43 cnf(3426,plain,
% 126.35/126.43 (~E(a39,a3)),
% 126.35/126.43 inference(scs_inference,[],[312,354,3334,3197,3235,2956,3257,3025,3248,2776,705,145,146,121,135,120,159,118,153,143,133,134,119,41,42,10,25,24,139,136,117,27,6,30,28,23,12,13,38,35,11,14,15,138,40,22,33,37,9,132,16,21,31,26,43,19,32,34,29,5,8,7,20,39,36,4,18,126,123,17,2])).
% 126.35/126.43 cnf(3427,plain,
% 126.35/126.43 (~P2(f41(f20(a2)),a46)),
% 126.35/126.43 inference(scs_inference,[],[312,354,3334,3197,3235,2956,3084,3257,3025,3248,2776,1857,705,145,146,121,135,120,159,118,153,143,133,134,119,41,42,10,25,24,139,136,117,27,6,30,28,23,12,13,38,35,11,14,15,138,40,22,33,37,9,132,16,21,31,26,43,19,32,34,29,5,8,7,20,39,36,4,18,126,123,17,2,144])).
% 126.35/126.43 cnf(3462,plain,
% 126.35/126.43 (~E(f30(x34621,a4),f30(x34622,a3))),
% 126.35/126.43 inference(scs_inference,[],[357,3046,2778,145,146,120,121,133,135])).
% 126.35/126.43 cnf(3472,plain,
% 126.35/126.43 (E(f42(f20(a2)),f9(f26(a22),f24(f9(a13,x34721))))),
% 126.35/126.43 inference(scs_inference,[],[357,373,3321,3046,2778,593,145,146,120,121,133,135,134,143,118,119,159])).
% 126.35/126.43 cnf(3474,plain,
% 126.35/126.43 (P1(f44(f44(f44(f24(f9(a1,x34741)),f30(x34742,x34743)),f30(x34744,x34745)),f30(x34746,x34747)))),
% 126.35/126.43 inference(scs_inference,[],[357,373,3321,3014,3046,2778,593,145,146,120,121,133,135,134,143,118,119,159,153])).
% 126.35/126.43 cnf(3476,plain,
% 126.35/126.43 (P1(f44(f44(f44(f24(f9(a1,x34761)),f30(x34762,x34763)),f30(x34764,x34765)),f35(x34766)))),
% 126.35/126.43 inference(scs_inference,[],[357,373,3321,3014,3046,2778,593,145,146,120,121,133,135,134,143,118,119,159,153,139])).
% 126.35/126.43 cnf(3478,plain,
% 126.35/126.43 (~E(f30(a4,x34781),f30(a3,x34782))),
% 126.35/126.43 inference(scs_inference,[],[357,373,3321,3014,3046,2778,593,145,146,120,121,133,135,134,143,118,119,159,153,139,136])).
% 126.35/126.43 cnf(3525,plain,
% 126.35/126.43 (P2(a46,f41(f20(a2)))),
% 126.35/126.43 inference(scs_inference,[],[357,373,3321,3098,3427,3014,3046,2778,593,145,146,120,121,133,135,134,143,118,119,159,153,139,136,25,41,117,42,6,138,28,27,30,10,24,38,14,13,33,35,12,23,40,22,34,16,32,11,29,15,132,26,19,20,37,36,9,43,31,21,8,4,5,7,39,18,126])).
% 126.35/126.43 cnf(3530,plain,
% 126.35/126.43 (~E(a3,a22)),
% 126.35/126.43 inference(scs_inference,[],[357,373,525,3321,3098,3427,3014,3046,3358,2778,593,145,146,120,121,133,135,134,143,118,119,159,153,139,136,25,41,117,42,6,138,28,27,30,10,24,38,14,13,33,35,12,23,40,22,34,16,32,11,29,15,132,26,19,20,37,36,9,43,31,21,8,4,5,7,39,18,126,123,17,2])).
% 126.35/126.43 cnf(3531,plain,
% 126.35/126.43 (~P2(f41(f41(a33)),a46)),
% 126.35/126.43 inference(scs_inference,[],[357,373,525,3321,3236,3098,3427,3014,3046,3358,2778,593,114,145,146,120,121,133,135,134,143,118,119,159,153,139,136,25,41,117,42,6,138,28,27,30,10,24,38,14,13,33,35,12,23,40,22,34,16,32,11,29,15,132,26,19,20,37,36,9,43,31,21,8,4,5,7,39,18,126,123,17,2,144])).
% 126.35/126.43 cnf(3535,plain,
% 126.35/126.43 (E(x35351,f14(f25(x35351)))),
% 126.35/126.43 inference(rename_variables,[],[492])).
% 126.35/126.43 cnf(3536,plain,
% 126.35/126.43 (~P3(a4,f9(a3,a1))),
% 126.35/126.43 inference(scs_inference,[],[357,373,525,3321,3236,2773,3098,3427,3014,3046,3358,2778,593,492,105,114,145,146,120,121,133,135,134,143,118,119,159,153,139,136,25,41,117,42,6,138,28,27,30,10,24,38,14,13,33,35,12,23,40,22,34,16,32,11,29,15,132,26,19,20,37,36,9,43,31,21,8,4,5,7,39,18,126,123,17,2,144,49,152])).
% 126.35/126.43 cnf(3537,plain,
% 126.35/126.43 (~P3(x35371,a1)),
% 126.35/126.43 inference(rename_variables,[],[105])).
% 126.35/126.43 cnf(3539,plain,
% 126.35/126.43 (~P3(a4,f44(a1,a3))),
% 126.35/126.43 inference(scs_inference,[],[357,373,525,3321,3236,2773,3098,3427,3014,3046,3358,2778,593,492,105,3537,114,145,146,120,121,133,135,134,143,118,119,159,153,139,136,25,41,117,42,6,138,28,27,30,10,24,38,14,13,33,35,12,23,40,22,34,16,32,11,29,15,132,26,19,20,37,36,9,43,31,21,8,4,5,7,39,18,126,123,17,2,144,49,152,151])).
% 126.35/126.43 cnf(3543,plain,
% 126.35/126.43 (E(f14(f25(x35431)),x35431)),
% 126.35/126.43 inference(rename_variables,[],[251])).
% 126.35/126.43 cnf(3547,plain,
% 126.35/126.43 (E(x35471,f14(f25(x35471)))),
% 126.35/126.43 inference(rename_variables,[],[492])).
% 126.35/126.43 cnf(3549,plain,
% 126.35/126.43 (E(x35491,f14(f25(x35491)))),
% 126.35/126.43 inference(rename_variables,[],[492])).
% 126.35/126.43 cnf(3551,plain,
% 126.35/126.43 (E(f14(f25(x35511)),x35511)),
% 126.35/126.43 inference(rename_variables,[],[251])).
% 126.35/126.43 cnf(3552,plain,
% 126.35/126.43 (~P2(f20(a22),f20(a3))),
% 126.35/126.43 inference(scs_inference,[],[357,373,525,3321,3329,3236,2773,3098,3427,3014,3046,3358,2778,523,2904,2876,593,492,3535,3547,251,3543,416,105,3537,114,145,146,120,121,133,135,134,143,118,119,159,153,139,136,25,41,117,42,6,138,28,27,30,10,24,38,14,13,33,35,12,23,40,22,34,16,32,11,29,15,132,26,19,20,37,36,9,43,31,21,8,4,5,7,39,18,126,123,17,2,144,49,152,151,46,53,51,50,48,137])).
% 126.35/126.43 cnf(3557,plain,
% 126.35/126.43 (~P2(f14(f25(f41(a33))),a46)),
% 126.35/126.43 inference(scs_inference,[],[357,373,525,3321,3329,3236,2773,3098,3427,3014,3046,3358,2778,523,2904,2876,593,720,492,3535,3547,3549,251,3543,3551,416,105,3537,114,145,146,120,121,133,135,134,143,118,119,159,153,139,136,25,41,117,42,6,138,28,27,30,10,24,38,14,13,33,35,12,23,40,22,34,16,32,11,29,15,132,26,19,20,37,36,9,43,31,21,8,4,5,7,39,18,126,123,17,2,144,49,152,151,46,53,51,50,48,137,44,47])).
% 126.35/126.43 cnf(3582,plain,
% 126.35/126.43 (E(f42(f20(a2)),f9(f26(a22),f47(f9(x35821,a13))))),
% 126.35/126.43 inference(scs_inference,[],[645,2916,2779,615,145,120,146,133,121,119,159])).
% 126.35/126.43 cnf(3588,plain,
% 126.35/126.43 (~E(f30(x35881,a3),f30(x35882,a21))),
% 126.35/126.43 inference(scs_inference,[],[645,2916,2779,615,145,120,146,133,121,119,159,118,134,135])).
% 126.35/126.43 cnf(3590,plain,
% 126.35/126.43 (P1(f44(f44(f44(f24(f9(a1,x35901)),f30(x35902,x35903)),f35(x35904)),f30(x35905,x35906)))),
% 126.35/126.43 inference(scs_inference,[],[645,3041,2916,2779,615,145,120,146,133,121,119,159,118,134,135,153])).
% 126.35/126.43 cnf(3592,plain,
% 126.35/126.43 (~P2(f41(f20(a22)),f41(f20(a3)))),
% 126.35/126.43 inference(scs_inference,[],[645,3552,3041,2916,2779,615,145,120,146,133,121,119,159,118,134,135,153,143])).
% 126.35/126.43 cnf(3596,plain,
% 126.35/126.43 (P1(f44(f44(f44(f24(f9(a1,x35961)),f30(x35962,x35963)),f35(x35964)),f35(x35965)))),
% 126.35/126.43 inference(scs_inference,[],[645,3552,3041,2916,2779,615,145,120,146,133,121,119,159,118,134,135,153,143,136,139])).
% 126.35/126.43 cnf(3623,plain,
% 126.35/126.43 (P2(f14(f25(a46)),f41(a33))),
% 126.35/126.43 inference(scs_inference,[],[645,3552,3205,3041,2916,2779,615,145,120,146,133,121,119,159,118,134,135,153,143,136,139,117,27,41,138,10,28,30,42,6,25,13,40,14,12,16,38,24,33,22,34,15,35,9,132])).
% 126.35/126.43 cnf(3642,plain,
% 126.35/126.43 (P2(f41(f20(a21)),f41(f20(a4)))),
% 126.35/126.43 inference(scs_inference,[],[645,3552,3205,3364,3041,2916,2779,615,145,120,146,133,121,119,159,118,134,135,153,143,136,139,117,27,41,138,10,28,30,42,6,25,13,40,14,12,16,38,24,33,22,34,15,35,9,132,23,36,19,43,37,32,11,26,29,20,4,7,21,39,31,8,5,126])).
% 126.35/126.43 cnf(3645,plain,
% 126.35/126.43 (P2(f42(f20(a2)),f9(f26(a22),f24(f9(a13,x36451))))),
% 126.35/126.43 inference(scs_inference,[],[645,3552,3205,3364,3041,2916,3472,2779,615,145,120,146,133,121,119,159,118,134,135,153,143,136,139,117,27,41,138,10,28,30,42,6,25,13,40,14,12,16,38,24,33,22,34,15,35,9,132,23,36,19,43,37,32,11,26,29,20,4,7,21,39,31,8,5,126,18,123])).
% 126.35/126.43 cnf(3649,plain,
% 126.35/126.43 (~P2(f41(f20(a21)),a46)),
% 126.35/126.43 inference(scs_inference,[],[645,3552,3205,2969,3364,3041,2916,3472,2779,3427,615,145,120,146,133,121,119,159,118,134,135,153,143,136,139,117,27,41,138,10,28,30,42,6,25,13,40,14,12,16,38,24,33,22,34,15,35,9,132,23,36,19,43,37,32,11,26,29,20,4,7,21,39,31,8,5,126,18,123,17,2,144])).
% 126.35/126.43 cnf(3652,plain,
% 126.35/126.43 (~E(x36521,f41(f41(x36521)))),
% 126.35/126.43 inference(rename_variables,[],[550])).
% 126.35/126.43 cnf(3665,plain,
% 126.35/126.43 (~P2(f41(f27(a37,f20(a2))),f20(a22))),
% 126.35/126.43 inference(scs_inference,[],[645,3552,3536,3205,2969,3364,3041,2916,3016,3472,3154,2779,586,408,1960,3427,1807,550,3652,2785,615,238,145,120,146,133,121,119,159,118,134,135,153,143,136,139,117,27,41,138,10,28,30,42,6,25,13,40,14,12,16,38,24,33,22,34,15,35,9,132,23,36,19,43,37,32,11,26,29,20,4,7,21,39,31,8,5,126,18,123,17,2,144,152,151,46,53,137,48])).
% 126.35/126.43 cnf(3687,plain,
% 126.35/126.43 (P1(f44(f44(f44(f24(f9(a1,x36871)),f35(x36872)),f30(x36873,x36874)),f30(x36875,x36876)))),
% 126.35/126.43 inference(scs_inference,[],[86,3136,2931,2815,145,146,133,121,120,119,153])).
% 126.35/126.43 cnf(3689,plain,
% 126.35/126.43 (E(f42(f20(a2)),f9(f26(a22),f28(f44(x36891,a13))))),
% 126.35/126.43 inference(scs_inference,[],[86,3136,2931,2815,637,145,146,133,121,120,119,153,159])).
% 126.35/126.43 cnf(3701,plain,
% 126.35/126.43 (P1(f44(f44(f44(f24(f9(a1,x37011)),f35(x37012)),f30(x37013,x37014)),f35(x37015)))),
% 126.35/126.43 inference(scs_inference,[],[86,3335,3136,2931,2815,637,145,146,133,121,120,119,153,159,118,135,134,143,136,139])).
% 126.35/126.43 cnf(3714,plain,
% 126.35/126.43 (P2(f14(f25(a46)),f41(f41(a33)))),
% 126.35/126.43 inference(scs_inference,[],[86,3623,3335,3136,2931,2815,637,145,146,133,121,120,119,153,159,118,135,134,143,136,139,117,138,28,30,27,25,41,6,24,132])).
% 126.35/126.43 cnf(3745,plain,
% 126.35/126.43 (P2(a46,f41(f20(a21)))),
% 126.35/126.43 inference(scs_inference,[],[86,3623,3335,3649,3136,2931,2815,637,145,146,133,121,120,119,153,159,118,135,134,143,136,139,117,138,28,30,27,25,41,6,24,132,10,12,14,42,34,40,15,13,23,35,38,22,16,43,37,33,29,19,36,20,9,11,32,4,21,26,5,31,7,126])).
% 126.35/126.43 cnf(3753,plain,
% 126.35/126.43 (~E(a7,a8)),
% 126.35/126.43 inference(scs_inference,[],[86,3623,3335,3649,3136,2931,3582,2815,637,145,146,133,121,120,119,153,159,118,135,134,143,136,139,117,138,28,30,27,25,41,6,24,132,10,12,14,42,34,40,15,13,23,35,38,22,16,43,37,33,29,19,36,20,9,11,32,4,21,26,5,31,7,126,39,8,123,18,17,2])).
% 126.35/126.43 cnf(3754,plain,
% 126.35/126.43 (~P5(a39,f24(f9(a5,x37541)))),
% 126.35/126.43 inference(scs_inference,[],[86,3623,3335,3649,3327,3136,2931,3582,2815,637,492,145,146,133,121,120,119,153,159,118,135,134,143,136,139,117,138,28,30,27,25,41,6,24,132,10,12,14,42,34,40,15,13,23,35,38,22,16,43,37,33,29,19,36,20,9,11,32,4,21,26,5,31,7,126,39,8,123,18,17,2,45])).
% 126.35/126.43 cnf(3756,plain,
% 126.35/126.43 (P2(a46,f41(f20(a4)))),
% 126.35/126.43 inference(scs_inference,[],[86,3623,3335,3525,3649,3327,3421,3136,2931,3582,2815,637,492,145,146,133,121,120,119,153,159,118,135,134,143,136,139,117,138,28,30,27,25,41,6,24,132,10,12,14,42,34,40,15,13,23,35,38,22,16,43,37,33,29,19,36,20,9,11,32,4,21,26,5,31,7,126,39,8,123,18,17,2,45,144])).
% 126.35/126.43 cnf(3758,plain,
% 126.35/126.43 (~P3(a8,f9(a7,a1))),
% 126.35/126.43 inference(scs_inference,[],[86,3623,3335,3525,3649,3327,3421,3136,2931,3582,2815,637,492,105,145,146,133,121,120,119,153,159,118,135,134,143,136,139,117,138,28,30,27,25,41,6,24,132,10,12,14,42,34,40,15,13,23,35,38,22,16,43,37,33,29,19,36,20,9,11,32,4,21,26,5,31,7,126,39,8,123,18,17,2,45,144,152])).
% 126.35/126.43 cnf(3759,plain,
% 126.35/126.43 (~P3(x37591,a1)),
% 126.35/126.43 inference(rename_variables,[],[105])).
% 126.35/126.43 cnf(3761,plain,
% 126.35/126.43 (~P3(a8,f44(a1,a7))),
% 126.35/126.43 inference(scs_inference,[],[86,3623,3335,3525,3649,3327,3421,3136,2931,3582,2815,637,492,105,3759,145,146,133,121,120,119,153,159,118,135,134,143,136,139,117,138,28,30,27,25,41,6,24,132,10,12,14,42,34,40,15,13,23,35,38,22,16,43,37,33,29,19,36,20,9,11,32,4,21,26,5,31,7,126,39,8,123,18,17,2,45,144,152,151])).
% 126.35/126.43 cnf(3764,plain,
% 126.35/126.43 (~P5(f14(f25(a39)),f29(f44(a5,x37641)))),
% 126.35/126.43 inference(scs_inference,[],[86,3623,3335,3525,3649,3327,3421,3136,2931,3582,2815,2847,637,492,81,105,3759,145,146,133,121,120,119,153,159,118,135,134,143,136,139,117,138,28,30,27,25,41,6,24,132,10,12,14,42,34,40,15,13,23,35,38,22,16,43,37,33,29,19,36,20,9,11,32,4,21,26,5,31,7,126,39,8,123,18,17,2,45,144,152,151,46])).
% 126.35/126.43 cnf(3765,plain,
% 126.35/126.43 (E(f29(f44(x37651,x37652)),x37651)),
% 126.35/126.43 inference(rename_variables,[],[81])).
% 126.35/126.43 cnf(3770,plain,
% 126.35/126.43 (~P2(f41(f20(a21)),f29(f44(f20(a2),x37701)))),
% 126.35/126.43 inference(scs_inference,[],[86,3539,3623,3335,3525,3649,3327,3421,3136,2931,3402,3582,2815,711,2892,2847,637,492,81,3765,105,3759,145,146,133,121,120,119,153,159,118,135,134,143,136,139,117,138,28,30,27,25,41,6,24,132,10,12,14,42,34,40,15,13,23,35,38,22,16,43,37,33,29,19,36,20,9,11,32,4,21,26,5,31,7,126,39,8,123,18,17,2,45,144,152,151,46,53,137,48])).
% 126.35/126.43 cnf(3781,plain,
% 126.35/126.43 (P3(f20(a21),f9(x37811,f44(x37812,f20(a2))))),
% 126.35/126.43 inference(scs_inference,[],[381,145])).
% 126.35/126.43 cnf(3785,plain,
% 126.35/126.43 (P3(f20(a21),f44(f44(x37851,f20(a2)),x37852))),
% 126.35/126.43 inference(scs_inference,[],[2824,381,145,133,146])).
% 126.35/126.43 cnf(3801,plain,
% 126.35/126.43 (E(f42(f20(a21)),f9(f26(a22),f47(f9(x38011,a13))))),
% 126.35/126.43 inference(scs_inference,[],[87,3162,2824,381,726,145,133,146,120,119,121,118,153,134,135,159])).
% 126.35/126.43 cnf(3817,plain,
% 126.35/126.43 (P2(a46,f41(f14(f25(a33))))),
% 126.35/126.43 inference(scs_inference,[],[87,3531,3315,3162,2824,381,726,145,133,146,120,119,121,118,153,134,135,159,143,136,139,138,117,27,28,24,10,132])).
% 126.35/126.43 cnf(3849,plain,
% 126.35/126.43 (P2(f41(f20(a3)),f41(f20(a22)))),
% 126.35/126.43 inference(scs_inference,[],[87,3531,3315,3592,3162,2824,381,726,145,133,146,120,119,121,118,153,134,135,159,143,136,139,138,117,27,28,24,10,132,25,42,41,30,12,14,23,40,6,15,22,34,33,38,35,13,19,29,16,36,32,43,11,21,37,4,20,7,26,9,126])).
% 126.35/126.43 cnf(3859,plain,
% 126.35/126.43 (~E(a8,a48)),
% 126.35/126.43 inference(scs_inference,[],[87,3531,3315,3592,3162,3689,2824,381,726,145,133,146,120,119,121,118,153,134,135,159,143,136,139,138,117,27,28,24,10,132,25,42,41,30,12,14,23,40,6,15,22,34,33,38,35,13,19,29,16,36,32,43,11,21,37,4,20,7,26,9,126,5,31,39,123,8,18,17,2])).
% 126.35/126.43 cnf(3862,plain,
% 126.35/126.43 (~P3(a8,f9(f41(f41(f41(a8))),f9(a7,a1)))),
% 126.35/126.43 inference(scs_inference,[],[87,3758,3531,3315,3592,3642,3162,3770,3689,2824,381,412,726,145,133,146,120,119,121,118,153,134,135,159,143,136,139,138,117,27,28,24,10,132,25,42,41,30,12,14,23,40,6,15,22,34,33,38,35,13,19,29,16,36,32,43,11,21,37,4,20,7,26,9,126,5,31,39,123,8,18,17,2,144,152])).
% 126.35/126.43 cnf(3863,plain,
% 126.35/126.43 (~E(x38631,f41(f41(f41(x38631))))),
% 126.35/126.43 inference(rename_variables,[],[412])).
% 126.35/126.43 cnf(3878,plain,
% 126.35/126.43 (~P3(f27(a11,f20(a3)),f44(f9(a2,a1),a4))),
% 126.35/126.43 inference(scs_inference,[],[87,3758,3531,3315,2990,3592,3642,3162,3056,3770,3645,3689,3192,2824,564,1948,381,1793,2712,412,3863,726,2785,245,145,133,146,120,119,121,118,153,134,135,159,143,136,139,138,117,27,28,24,10,132,25,42,41,30,12,14,23,40,6,15,22,34,33,38,35,13,19,29,16,36,32,43,11,21,37,4,20,7,26,9,126,5,31,39,123,8,18,17,2,144,152,151,46,53,137,48,47,52])).
% 126.35/126.43 cnf(3907,plain,
% 126.35/126.43 (E(f42(f20(a21)),f9(f26(a22),f28(f44(x39071,a13))))),
% 126.35/126.43 inference(scs_inference,[],[88,3138,3259,3781,2825,745,145,120,133,146,118,119,121,135,134,143,153,159])).
% 126.35/126.43 cnf(3939,plain,
% 126.35/126.43 (P2(f20(a22),f41(f27(a37,f20(a2))))),
% 126.35/126.43 inference(scs_inference,[],[88,3745,3138,3665,3259,3781,2825,745,145,120,133,146,118,119,121,135,134,143,153,159,136,139,138,24,117,132,30,23,27,28,42,25,41,10,38,33,6,34,40,14,15,12,22,19,13,126])).
% 126.35/126.43 cnf(3963,plain,
% 126.35/126.43 (~E(a7,a48)),
% 126.35/126.43 inference(scs_inference,[],[88,3745,3138,3665,3259,3781,3801,2825,745,145,120,133,146,118,119,121,135,134,143,153,159,136,139,138,24,117,132,30,23,27,28,42,25,41,10,38,33,6,34,40,14,15,12,22,19,13,126,36,29,35,20,21,11,4,26,43,16,7,37,32,8,31,123,18,9,39,5,17,2])).
% 126.35/126.43 cnf(3964,plain,
% 126.35/126.43 (~P3(a48,f9(a7,a1))),
% 126.35/126.43 inference(scs_inference,[],[88,3745,3138,3665,3259,3781,3801,2825,745,105,145,120,133,146,118,119,121,135,134,143,153,159,136,139,138,24,117,132,30,23,27,28,42,25,41,10,38,33,6,34,40,14,15,12,22,19,13,126,36,29,35,20,21,11,4,26,43,16,7,37,32,8,31,123,18,9,39,5,17,2,152])).
% 126.35/126.43 cnf(3965,plain,
% 126.35/126.43 (~P3(x39651,a1)),
% 126.35/126.43 inference(rename_variables,[],[105])).
% 126.35/126.43 cnf(3967,plain,
% 126.35/126.43 (P2(f16(f20(a2),f20(a2),x39671,x39672,x39673,x39674,x39675),f16(f20(a21),f20(a21),x39671,x39672,x39673,x39674,x39675))),
% 126.35/126.43 inference(scs_inference,[],[88,3745,2973,3092,3138,3665,3259,3781,3801,2825,745,105,145,120,133,146,118,119,121,135,134,143,153,159,136,139,138,24,117,132,30,23,27,28,42,25,41,10,38,33,6,34,40,14,15,12,22,19,13,126,36,29,35,20,21,11,4,26,43,16,7,37,32,8,31,123,18,9,39,5,17,2,152,144])).
% 126.35/126.43 cnf(3971,plain,
% 126.35/126.43 (P2(f41(a46),f41(f20(a21)))),
% 126.35/126.43 inference(scs_inference,[],[88,3745,2973,3092,3138,3665,3259,3781,3801,2825,639,745,105,145,120,133,146,118,119,121,135,134,143,153,159,136,139,138,24,117,132,30,23,27,28,42,25,41,10,38,33,6,34,40,14,15,12,22,19,13,126,36,29,35,20,21,11,4,26,43,16,7,37,32,8,31,123,18,9,39,5,17,2,152,144,140])).
% 126.35/126.43 cnf(3974,plain,
% 126.35/126.43 (~P3(a48,f44(a1,a7))),
% 126.35/126.43 inference(scs_inference,[],[88,3745,2973,3092,3138,3665,3259,3781,3801,2825,639,745,105,3965,145,120,133,146,118,119,121,135,134,143,153,159,136,139,138,24,117,132,30,23,27,28,42,25,41,10,38,33,6,34,40,14,15,12,22,19,13,126,36,29,35,20,21,11,4,26,43,16,7,37,32,8,31,123,18,9,39,5,17,2,152,144,140,151])).
% 126.35/126.43 cnf(3977,plain,
% 126.35/126.43 (~P2(f20(x39771),a46)),
% 126.35/126.43 inference(scs_inference,[],[88,3745,2973,3092,3138,3665,3259,3781,3801,2825,352,639,405,745,105,3965,145,120,133,146,118,119,121,135,134,143,153,159,136,139,138,24,117,132,30,23,27,28,42,25,41,10,38,33,6,34,40,14,15,12,22,19,13,126,36,29,35,20,21,11,4,26,43,16,7,37,32,8,31,123,18,9,39,5,17,2,152,144,140,151,137])).
% 126.35/126.43 cnf(3984,plain,
% 126.35/126.43 (~P2(f41(f20(a3)),f20(a2))),
% 126.35/126.43 inference(scs_inference,[],[88,3761,2849,3745,2973,3092,3138,3665,3337,3259,3781,3801,2825,2727,352,639,2904,405,745,80,105,3965,145,120,133,146,118,119,121,135,134,143,153,159,136,139,138,24,117,132,30,23,27,28,42,25,41,10,38,33,6,34,40,14,15,12,22,19,13,126,36,29,35,20,21,11,4,26,43,16,7,37,32,8,31,123,18,9,39,5,17,2,152,144,140,151,137,46,53,47])).
% 126.35/126.43 cnf(4013,plain,
% 126.35/126.43 (E(f42(f20(a21)),f9(f26(a22),f29(f44(a13,x40131))))),
% 126.35/126.43 inference(scs_inference,[],[89,3275,3785,2826,770,145,133,146,134,120,121,153,119,159])).
% 126.35/126.43 cnf(4017,plain,
% 126.35/126.43 (~P2(f41(f20(x40171)),f41(a46))),
% 126.35/126.43 inference(scs_inference,[],[89,3977,3275,3785,2826,770,145,133,146,134,120,121,153,119,159,136,143])).
% 126.35/126.43 cnf(4030,plain,
% 126.35/126.43 (P2(a46,f41(f41(f20(a4))))),
% 126.35/126.43 inference(scs_inference,[],[89,3977,3971,3756,3275,3785,2826,770,145,133,146,134,120,121,153,119,159,136,143,118,135,139,138,117,24,132])).
% 126.35/126.43 cnf(4050,plain,
% 126.35/126.43 (P2(f20(a2),f41(f20(a3)))),
% 126.35/126.43 inference(scs_inference,[],[89,3977,3984,3971,3756,3275,3785,2826,770,145,133,146,134,120,121,153,119,159,136,143,118,135,139,138,117,24,132,30,42,23,27,38,6,33,34,41,25,10,15,28,40,22,12,13,14,126])).
% 126.35/126.43 cnf(4075,plain,
% 126.35/126.43 (~E(a8,a38)),
% 126.35/126.43 inference(scs_inference,[],[89,3977,3984,3971,3756,3275,3785,3907,2826,770,145,133,146,134,120,121,153,119,159,136,143,118,135,139,138,117,24,132,30,42,23,27,38,6,33,34,41,25,10,15,28,40,22,12,13,14,126,29,35,123,32,7,19,11,36,21,20,43,26,37,16,4,31,8,5,9,39,18,17,2])).
% 126.35/126.43 cnf(4076,plain,
% 126.35/126.43 (~P5(f47(f9(x40761,a39)),f24(f9(a5,x40762)))),
% 126.35/126.43 inference(scs_inference,[],[89,3977,3984,3971,3756,3754,3275,3785,3907,2826,770,79,145,133,146,134,120,121,153,119,159,136,143,118,135,139,138,117,24,132,30,42,23,27,38,6,33,34,41,25,10,15,28,40,22,12,13,14,126,29,35,123,32,7,19,11,36,21,20,43,26,37,16,4,31,8,5,9,39,18,17,2,45])).
% 126.35/126.43 cnf(4080,plain,
% 126.35/126.43 (~P2(f41(f20(a4)),a46)),
% 126.35/126.43 inference(scs_inference,[],[89,91,3977,3964,3984,3971,3756,3754,3275,3785,3907,2826,3649,3642,770,79,145,133,146,134,120,121,153,119,159,136,143,118,135,139,138,117,24,132,30,42,23,27,38,6,33,34,41,25,10,15,28,40,22,12,13,14,126,29,35,123,32,7,19,11,36,21,20,43,26,37,16,4,31,8,5,9,39,18,17,2,45,152,144])).
% 126.35/126.43 cnf(4082,plain,
% 126.35/126.43 (E(f41(f20(a3)),f41(f20(a2)))),
% 126.35/126.43 inference(scs_inference,[],[89,91,3977,3964,3984,3971,3756,3754,3275,3785,3907,2826,3649,3084,3642,770,79,145,133,146,134,120,121,153,119,159,136,143,118,135,139,138,117,24,132,30,42,23,27,38,6,33,34,41,25,10,15,28,40,22,12,13,14,126,29,35,123,32,7,19,11,36,21,20,43,26,37,16,4,31,8,5,9,39,18,17,2,45,152,144,140])).
% 126.35/126.43 cnf(4089,plain,
% 126.35/126.43 (P3(f28(f41(a1)),f41(a1))),
% 126.35/126.43 inference(scs_inference,[],[89,91,3977,3964,3984,3971,3756,3754,3275,3785,3907,2826,3007,1938,3649,3084,3642,1779,770,79,197,145,133,146,134,120,121,153,119,159,136,143,118,135,139,138,117,24,132,30,42,23,27,38,6,33,34,41,25,10,15,28,40,22,12,13,14,126,29,35,123,32,7,19,11,36,21,20,43,26,37,16,4,31,8,5,9,39,18,17,2,45,152,144,140,151,137,53])).
% 126.35/126.43 cnf(4104,plain,
% 126.35/126.43 (P3(f28(f41(a1)),f9(x41041,f41(a1)))),
% 126.35/126.43 inference(scs_inference,[],[4089,145])).
% 126.35/126.43 cnf(4108,plain,
% 126.35/126.43 (P3(f28(f41(a1)),f44(f41(a1),x41081))),
% 126.35/126.43 inference(scs_inference,[],[4089,4082,145,133,146])).
% 126.35/126.43 cnf(4128,plain,
% 126.35/126.43 (E(f42(f20(a2)),f9(f26(a22),f14(f25(a13))))),
% 126.35/126.43 inference(scs_inference,[],[90,4017,4089,4082,3362,515,145,133,146,121,134,143,120,135,153,119,118,136,159])).
% 126.35/126.43 cnf(4132,plain,
% 126.35/126.43 (P2(f41(f20(a2)),f41(f41(f20(a3))))),
% 126.35/126.43 inference(scs_inference,[],[90,4017,4089,4050,4082,3362,515,145,133,146,121,134,143,120,135,153,119,118,136,159,139,138])).
% 126.35/126.43 cnf(4148,plain,
% 126.35/126.43 (E(f9(f41(f20(a3)),x41481),f9(f41(f20(a2)),x41481))),
% 126.35/126.43 inference(scs_inference,[],[90,4017,4089,4050,4082,3362,515,145,133,146,121,134,143,120,135,153,119,118,136,159,139,138,117,132,24,42,30,27,41,34,10,6,38,23,25])).
% 126.35/126.43 cnf(4151,plain,
% 126.35/126.43 (P2(f41(a46),f41(f20(x41511)))),
% 126.35/126.43 inference(scs_inference,[],[90,4017,4089,4050,4082,3362,515,145,133,146,121,134,143,120,135,153,119,118,136,159,139,138,117,132,24,42,30,27,41,34,10,6,38,23,25,15,12,126])).
% 126.35/126.43 cnf(4181,plain,
% 126.35/126.43 (E(f41(f41(f20(a3))),f41(f41(f20(a2))))),
% 126.35/126.43 inference(scs_inference,[],[90,4017,4089,4050,4082,3362,4013,515,145,133,146,121,134,143,120,135,153,119,118,136,159,139,138,117,132,24,42,30,27,41,34,10,6,38,23,25,15,12,126,33,13,123,28,40,19,35,14,36,22,32,21,29,43,7,11,16,4,26,37,20,39,31,8,5,9,18,17])).
% 126.35/126.43 cnf(4184,plain,
% 126.35/126.43 (E(f32(f25(x41841)),x41841)),
% 126.35/126.43 inference(rename_variables,[],[59])).
% 126.35/126.43 cnf(4186,plain,
% 126.35/126.43 (~P3(a38,f9(a7,a1))),
% 126.35/126.43 inference(scs_inference,[],[90,4017,4089,4050,4082,3362,4013,2738,3754,515,59,105,461,145,133,146,121,134,143,120,135,153,119,118,136,159,139,138,117,132,24,42,30,27,41,34,10,6,38,23,25,15,12,126,33,13,123,28,40,19,35,14,36,22,32,21,29,43,7,11,16,4,26,37,20,39,31,8,5,9,18,17,2,45,49,152])).
% 126.35/126.43 cnf(4187,plain,
% 126.35/126.43 (~P3(x41871,a1)),
% 126.35/126.43 inference(rename_variables,[],[105])).
% 126.35/126.43 cnf(4189,plain,
% 126.35/126.43 (P2(f16(f20(a2),f20(a2),f20(a2),x41891,x41892,x41893,x41894),f16(f20(a21),f20(a21),f20(a21),x41891,x41892,x41893,x41894))),
% 126.35/126.43 inference(scs_inference,[],[90,4017,4089,4050,3203,3967,4082,3362,4013,2738,3754,515,59,105,461,145,133,146,121,134,143,120,135,153,119,118,136,159,139,138,117,132,24,42,30,27,41,34,10,6,38,23,25,15,12,126,33,13,123,28,40,19,35,14,36,22,32,21,29,43,7,11,16,4,26,37,20,39,31,8,5,9,18,17,2,45,49,152,144])).
% 126.35/126.43 cnf(4193,plain,
% 126.35/126.43 (~P3(a38,f44(a1,a7))),
% 126.35/126.43 inference(scs_inference,[],[90,4017,4089,4050,3203,3967,4082,3362,4013,2738,3754,515,59,105,4187,461,145,133,146,121,134,143,120,135,153,119,118,136,159,139,138,117,132,24,42,30,27,41,34,10,6,38,23,25,15,12,126,33,13,123,28,40,19,35,14,36,22,32,21,29,43,7,11,16,4,26,37,20,39,31,8,5,9,18,17,2,45,49,152,144,151])).
% 126.35/126.43 cnf(4197,plain,
% 126.35/126.43 (E(x41971,f14(f25(x41971)))),
% 126.35/126.43 inference(rename_variables,[],[492])).
% 126.35/126.43 cnf(4198,plain,
% 126.35/126.43 (P4(f24(f9(a21,x41981)),a22,f24(f9(a13,x41982)))),
% 126.35/126.43 inference(scs_inference,[],[90,4017,4089,4050,3203,3967,4082,2625,3362,1323,4013,2738,3754,515,59,4184,492,105,4187,461,145,133,146,121,134,143,120,135,153,119,118,136,159,139,138,117,132,24,42,30,27,41,34,10,6,38,23,25,15,12,126,33,13,123,28,40,19,35,14,36,22,32,21,29,43,7,11,16,4,26,37,20,39,31,8,5,9,18,17,2,45,49,152,144,151,51,50])).
% 126.35/126.43 cnf(4199,plain,
% 126.35/126.43 (E(f32(f25(x41991)),x41991)),
% 126.35/126.43 inference(rename_variables,[],[59])).
% 126.35/126.43 cnf(4204,plain,
% 126.35/126.43 (E(f32(f25(x42041)),x42041)),
% 126.35/126.43 inference(rename_variables,[],[59])).
% 126.35/126.43 cnf(4205,plain,
% 126.35/126.43 (~P3(a48,f44(f29(f44(a1,a7)),f28(f44(a1,a7))))),
% 126.35/126.43 inference(scs_inference,[],[90,3974,4017,4089,4050,3203,3967,4082,2625,3362,1323,4030,4013,2738,792,2849,3754,2892,515,59,4184,4199,492,105,4187,461,145,133,146,121,134,143,120,135,153,119,118,136,159,139,138,117,132,24,42,30,27,41,34,10,6,38,23,25,15,12,126,33,13,123,28,40,19,35,14,36,22,32,21,29,43,7,11,16,4,26,37,20,39,31,8,5,9,18,17,2,45,49,152,144,151,51,50,137,46,53])).
% 126.35/126.43 cnf(4208,plain,
% 126.35/126.43 (E(f32(f25(x42081)),x42081)),
% 126.35/126.43 inference(rename_variables,[],[59])).
% 126.35/126.43 cnf(4209,plain,
% 126.35/126.43 (~P2(f41(f20(x42091)),f32(f25(f41(a46))))),
% 126.35/126.43 inference(scs_inference,[],[90,3974,4017,4089,4050,4080,3203,3967,4082,2625,3362,1323,4030,4013,2738,792,2849,3754,2892,515,59,4184,4199,4204,4208,492,105,4187,461,145,133,146,121,134,143,120,135,153,119,118,136,159,139,138,117,132,24,42,30,27,41,34,10,6,38,23,25,15,12,126,33,13,123,28,40,19,35,14,36,22,32,21,29,43,7,11,16,4,26,37,20,39,31,8,5,9,18,17,2,45,49,152,144,151,51,50,137,46,53,47,48])).
% 126.35/126.43 cnf(4210,plain,
% 126.35/126.43 (E(f32(f25(x42101)),x42101)),
% 126.35/126.43 inference(rename_variables,[],[59])).
% 126.35/126.43 cnf(4215,plain,
% 126.35/126.43 (P2(f20(a2),f20(a3))+E(f20(a2),f41(f20(a3)))),
% 126.35/126.43 inference(scs_inference,[],[90,3974,4017,4089,4050,4080,3203,3967,4082,2625,3362,1323,4030,4013,2738,792,2849,3754,2892,515,59,4184,4199,4204,4208,4210,492,4197,105,4187,461,145,133,146,121,134,143,120,135,153,119,118,136,159,139,138,117,132,24,42,30,27,41,34,10,6,38,23,25,15,12,126,33,13,123,28,40,19,35,14,36,22,32,21,29,43,7,11,16,4,26,37,20,39,31,8,5,9,18,17,2,45,49,152,144,151,51,50,137,46,53,47,48,52,3,140])).
% 126.35/126.43 cnf(4244,plain,
% 126.35/126.43 (E(f42(f20(a21)),f9(f26(a22),f32(f25(a13))))),
% 126.35/126.43 inference(scs_inference,[],[2978,4104,3377,2995,2829,682,133,145,121,146,134,143,153,135,120,118,136,119,159])).
% 126.35/126.43 cnf(4252,plain,
% 126.35/126.43 (P2(f41(a46),f41(f41(f20(x42521))))),
% 126.35/126.43 inference(scs_inference,[],[2978,4151,4104,3377,2995,2829,682,133,145,121,146,134,143,153,135,120,118,136,119,159,139,117,138,132])).
% 126.35/126.43 cnf(4257,plain,
% 126.35/126.43 (P2(f42(f20(a2)),f9(f26(a22),f14(f25(a13))))),
% 126.35/126.43 inference(scs_inference,[],[2978,4151,4104,3377,2995,4128,2829,682,133,145,121,146,134,143,153,135,120,118,136,119,159,139,117,138,132,42,6,10,123])).
% 126.35/126.43 cnf(4262,plain,
% 126.35/126.43 (P2(a46,f14(f25(f41(a33))))),
% 126.35/126.43 inference(scs_inference,[],[2978,4151,4104,3377,2995,3557,4128,2829,682,133,145,121,146,134,143,153,135,120,118,136,119,159,139,117,138,132,42,6,10,123,24,23,30,126])).
% 126.35/126.43 cnf(4299,plain,
% 126.35/126.43 (~P5(a39,f29(f44(a5,x42991)))),
% 126.35/126.43 inference(scs_inference,[],[2978,2780,4151,3764,4104,3377,2995,3557,4128,2829,682,492,133,145,121,146,134,143,153,135,120,118,136,119,159,139,117,138,132,42,6,10,123,24,23,30,126,27,41,34,38,28,33,40,15,12,25,13,35,36,32,19,7,16,4,43,14,26,21,29,22,39,11,5,37,20,31,8,9,18,17,2,45])).
% 126.35/126.43 cnf(4301,plain,
% 126.35/126.43 (~P2(f41(f27(a37,f20(a2))),f20(a3))),
% 126.35/126.43 inference(scs_inference,[],[2978,2780,4151,3764,4104,3377,2995,3939,3557,4128,2829,3552,682,492,133,145,121,146,134,143,153,135,120,118,136,119,159,139,117,138,132,42,6,10,123,24,23,30,126,27,41,34,38,28,33,40,15,12,25,13,35,36,32,19,7,16,4,43,14,26,21,29,22,39,11,5,37,20,31,8,9,18,17,2,45,144])).
% 126.35/126.43 cnf(4304,plain,
% 126.35/126.43 (~E(x43041,f41(f41(f41(x43041))))),
% 126.35/126.43 inference(rename_variables,[],[412])).
% 126.35/126.43 cnf(4314,plain,
% 126.35/126.43 (P3(f24(f41(a1)),f41(a1))),
% 126.35/126.43 inference(scs_inference,[],[2978,2780,4193,4151,3764,4104,3377,2995,3939,3557,4128,2829,3018,510,1928,1765,3552,412,4304,682,2785,196,492,133,145,121,146,134,143,153,135,120,118,136,119,159,139,117,138,132,42,6,10,123,24,23,30,126,27,41,34,38,28,33,40,15,12,25,13,35,36,32,19,7,16,4,43,14,26,21,29,22,39,11,5,37,20,31,8,9,18,17,2,45,144,152,151,137,46,53])).
% 126.35/126.43 cnf(4329,plain,
% 126.35/126.43 (P3(f24(f41(a1)),f9(x43291,f41(a1)))),
% 126.35/126.43 inference(scs_inference,[],[4314,2836,133,145])).
% 126.35/126.43 cnf(4331,plain,
% 126.35/126.43 (P3(f24(f41(a1)),f44(f41(a1),x43311))),
% 126.35/126.43 inference(scs_inference,[],[4314,2836,133,145,146])).
% 126.35/126.43 cnf(4349,plain,
% 126.35/126.43 (E(f42(f20(a2)),f9(f26(a22),f29(f44(a13,x43491))))),
% 126.35/126.43 inference(scs_inference,[],[3095,4314,517,3223,2836,662,133,145,146,121,153,120,143,135,134,118,119,159])).
% 126.35/126.43 cnf(4407,plain,
% 126.35/126.43 (E(f24(f9(x44071,x44072)),x44071)),
% 126.35/126.43 inference(rename_variables,[],[78])).
% 126.35/126.43 cnf(4408,plain,
% 126.35/126.43 (~P2(f41(f41(f20(x44081))),a46)),
% 126.35/126.43 inference(scs_inference,[],[3095,2782,4314,4299,4189,4301,517,4252,3223,4244,2836,662,78,114,133,145,146,121,153,120,143,135,134,118,119,159,136,139,138,117,132,6,10,42,123,23,126,24,30,38,13,27,15,41,40,12,25,33,34,28,36,4,35,32,16,21,43,19,14,26,7,29,22,37,11,39,5,20,9,31,18,8,17,2,45,144])).
% 126.35/126.43 cnf(4411,plain,
% 126.35/126.43 (~P3(a45,f9(a5,a1))),
% 126.35/126.43 inference(scs_inference,[],[3095,2782,4314,4299,4189,4301,517,4252,3223,4244,2836,662,78,105,114,133,145,146,121,153,120,143,135,134,118,119,159,136,139,138,117,132,6,10,42,123,23,126,24,30,38,13,27,15,41,40,12,25,33,34,28,36,4,35,32,16,21,43,19,14,26,7,29,22,37,11,39,5,20,9,31,18,8,17,2,45,144,152])).
% 126.35/126.43 cnf(4412,plain,
% 126.35/126.43 (~P3(x44121,a1)),
% 126.35/126.43 inference(rename_variables,[],[105])).
% 126.35/126.43 cnf(4414,plain,
% 126.35/126.43 (~P3(a45,f44(a1,a5))),
% 126.35/126.43 inference(scs_inference,[],[3095,2782,4314,4299,4189,4301,517,4252,3223,4244,2836,662,78,105,4412,114,133,145,146,121,153,120,143,135,134,118,119,159,136,139,138,117,132,6,10,42,123,23,126,24,30,38,13,27,15,41,40,12,25,33,34,28,36,4,35,32,16,21,43,19,14,26,7,29,22,37,11,39,5,20,9,31,18,8,17,2,45,144,152,151])).
% 126.35/126.43 cnf(4417,plain,
% 126.35/126.43 (~P2(f20(a2),f20(a3))),
% 126.35/126.43 inference(scs_inference,[],[3095,2782,4314,4299,4189,4301,517,4252,3223,4244,2836,3000,2887,662,78,105,4412,114,133,145,146,121,153,120,143,135,134,118,119,159,136,139,138,117,132,6,10,42,123,23,126,24,30,38,13,27,15,41,40,12,25,33,34,28,36,4,35,32,16,21,43,19,14,26,7,29,22,37,11,39,5,20,9,31,18,8,17,2,45,144,152,151,137])).
% 126.35/126.43 cnf(4419,plain,
% 126.35/126.43 (~P3(a38,f9(f24(f9(a7,a1)),f47(f9(a7,a1))))),
% 126.35/126.43 inference(scs_inference,[],[3095,2782,4186,4314,4299,4189,4301,517,4252,3223,4244,2836,3000,2792,2887,662,78,105,4412,114,133,145,146,121,153,120,143,135,134,118,119,159,136,139,138,117,132,6,10,42,123,23,126,24,30,38,13,27,15,41,40,12,25,33,34,28,36,4,35,32,16,21,43,19,14,26,7,29,22,37,11,39,5,20,9,31,18,8,17,2,45,144,152,151,137,53])).
% 126.35/126.43 cnf(4422,plain,
% 126.35/126.43 (E(f24(f9(x44221,x44222)),x44221)),
% 126.35/126.43 inference(rename_variables,[],[78])).
% 126.35/126.43 cnf(4423,plain,
% 126.35/126.43 (~P2(f20(a22),f24(f9(f20(a3),x44231)))),
% 126.35/126.43 inference(scs_inference,[],[3095,2782,4186,4314,4299,4189,4301,517,4252,3223,2992,4244,2836,3000,2792,404,2887,662,78,4407,105,4412,114,133,145,146,121,153,120,143,135,134,118,119,159,136,139,138,117,132,6,10,42,123,23,126,24,30,38,13,27,15,41,40,12,25,33,34,28,36,4,35,32,16,21,43,19,14,26,7,29,22,37,11,39,5,20,9,31,18,8,17,2,45,144,152,151,137,53,46,47])).
% 126.35/126.43 cnf(4425,plain,
% 126.35/126.43 (E(f24(f9(x44251,x44252)),x44251)),
% 126.35/126.43 inference(rename_variables,[],[78])).
% 126.35/126.43 cnf(4426,plain,
% 126.35/126.43 (~P3(f24(f9(a38,x44261)),f9(a7,a1))),
% 126.35/126.43 inference(scs_inference,[],[3095,2782,4186,4314,4299,4189,4301,517,4252,3223,2992,4244,2836,3000,2792,404,2887,662,78,4407,4422,4425,105,4412,114,133,145,146,121,153,120,143,135,134,118,119,159,136,139,138,117,132,6,10,42,123,23,126,24,30,38,13,27,15,41,40,12,25,33,34,28,36,4,35,32,16,21,43,19,14,26,7,29,22,37,11,39,5,20,9,31,18,8,17,2,45,144,152,151,137,53,46,47,48,52])).
% 126.35/126.43 cnf(4430,plain,
% 126.35/126.43 (E(f20(a2),f41(f20(a3)))),
% 126.35/126.43 inference(scs_inference,[],[3095,2782,4186,4314,4299,4189,4301,517,4252,3223,2992,4244,2836,3000,2792,404,2887,662,78,4407,4422,4425,492,105,4412,114,133,145,146,121,153,120,143,135,134,118,119,159,136,139,138,117,132,6,10,42,123,23,126,24,30,38,13,27,15,41,40,12,25,33,34,28,36,4,35,32,16,21,43,19,14,26,7,29,22,37,11,39,5,20,9,31,18,8,17,2,45,144,152,151,137,53,46,47,48,52,3,4215])).
% 126.35/126.43 cnf(4435,plain,
% 126.35/126.43 (P3(f20(a2),f9(f41(f20(a3)),x44351))),
% 126.35/126.43 inference(scs_inference,[],[4430,133])).
% 126.35/126.43 cnf(4447,plain,
% 126.35/126.43 (~P2(f41(f20(a2)),f41(f20(a3)))),
% 126.35/126.43 inference(scs_inference,[],[3208,4417,4430,4108,3474,133,145,146,121,153,135,143])).
% 126.35/126.43 cnf(4457,plain,
% 126.35/126.43 (P3(f20(a2),f44(x44571,f41(f20(a3))))),
% 126.35/126.43 inference(scs_inference,[],[3208,4417,4430,4108,3474,133,145,146,121,153,135,143,118,120,119,139,134])).
% 126.35/126.43 cnf(4461,plain,
% 126.35/126.43 (E(f42(f20(a21)),f9(f26(a22),a13))),
% 126.35/126.43 inference(scs_inference,[],[3208,4417,4430,4108,3474,254,133,145,146,121,153,135,143,118,120,119,139,134,136,159])).
% 126.35/126.43 cnf(4469,plain,
% 126.35/126.43 (E(f27(x44691,f20(a2)),f27(x44691,f41(f20(a3))))),
% 126.35/126.43 inference(scs_inference,[],[3208,4417,4430,4108,3714,3474,254,133,145,146,121,153,135,143,118,120,119,139,134,136,159,138,117,132,6])).
% 126.35/126.43 cnf(4470,plain,
% 126.35/126.43 (P2(f24(f9(f20(a3),x44701)),f20(a22))),
% 126.35/126.43 inference(scs_inference,[],[3208,4417,4430,4108,3714,4423,3474,254,133,145,146,121,153,135,143,118,120,119,139,134,136,159,138,117,132,6,126])).
% 126.35/126.43 cnf(4472,plain,
% 126.35/126.43 (E(f16(x44721,x44722,x44723,f20(a2),x44724,x44725,x44726),f16(x44721,x44722,x44723,f41(f20(a3)),x44724,x44725,x44726))),
% 126.35/126.43 inference(scs_inference,[],[3208,4417,4430,4108,3714,4423,3474,254,133,145,146,121,153,135,143,118,120,119,139,134,136,159,138,117,132,6,126,10])).
% 126.35/126.43 cnf(4477,plain,
% 126.35/126.43 (E(f16(x44771,x44772,x44773,x44774,x44775,x44776,f20(a2)),f16(x44771,x44772,x44773,x44774,x44775,x44776,f41(f20(a3))))),
% 126.35/126.43 inference(scs_inference,[],[3208,4417,4430,4108,3714,4423,3474,4349,254,133,145,146,121,153,135,143,118,120,119,139,134,136,159,138,117,132,6,126,10,123,24,42,13])).
% 126.35/126.43 cnf(4485,plain,
% 126.35/126.43 (E(f16(x44851,x44852,x44853,x44854,x44855,f20(a2),x44856),f16(x44851,x44852,x44853,x44854,x44855,f41(f20(a3)),x44856))),
% 126.35/126.43 inference(scs_inference,[],[3208,4417,4430,4108,3714,4423,3474,4349,254,133,145,146,121,153,135,143,118,120,119,139,134,136,159,138,117,132,6,126,10,123,24,42,13,23,15,30,27,40,38,28,12])).
% 126.35/126.43 cnf(4514,plain,
% 126.35/126.43 (~P5(a39,f14(f25(a5)))),
% 126.35/126.43 inference(scs_inference,[],[3208,3255,4417,4430,4108,3100,3714,4423,3474,4349,492,254,133,145,146,121,153,135,143,118,120,119,139,134,136,159,138,117,132,6,126,10,123,24,42,13,23,15,30,27,40,38,28,12,33,34,41,36,16,25,35,19,43,4,7,26,21,32,14,22,37,29,11,5,39,31,9,20,18,8,17,2,45])).
% 126.35/126.43 cnf(4520,plain,
% 126.35/126.43 (~E(x45201,f41(f41(x45201)))),
% 126.35/126.43 inference(rename_variables,[],[550])).
% 126.35/126.43 cnf(4528,plain,
% 126.35/126.43 (~P5(f47(f9(x45281,a39)),a5)),
% 126.35/126.43 inference(scs_inference,[],[3208,3255,4417,4411,4430,4076,4108,3100,3714,4423,3474,4349,1918,1751,2690,2994,550,4520,492,566,254,133,145,146,121,153,135,143,118,120,119,139,134,136,159,138,117,132,6,126,10,123,24,42,13,23,15,30,27,40,38,28,12,33,34,41,36,16,25,35,19,43,4,7,26,21,32,14,22,37,29,11,5,39,31,9,20,18,8,17,2,45,144,152,151,137,46])).
% 126.35/126.43 cnf(4532,plain,
% 126.35/126.43 (~P2(f20(a2),f32(f25(f41(a46))))),
% 126.35/126.43 inference(scs_inference,[],[3208,3255,4417,4411,4430,4076,4108,3100,3714,4423,3474,4209,4349,1918,1751,2690,2794,2994,550,4520,492,566,254,133,145,146,121,153,135,143,118,120,119,139,134,136,159,138,117,132,6,126,10,123,24,42,13,23,15,30,27,40,38,28,12,33,34,41,36,16,25,35,19,43,4,7,26,21,32,14,22,37,29,11,5,39,31,9,20,18,8,17,2,45,144,152,151,137,46,53,47])).
% 126.35/126.43 cnf(4559,plain,
% 126.35/126.43 (~P2(f41(f41(f20(a2))),f41(f41(f20(a3))))),
% 126.35/126.43 inference(scs_inference,[],[3320,3426,4461,4329,4447,3476,145,133,146,153,121,118,135,143])).
% 126.35/126.43 cnf(4563,plain,
% 126.35/126.43 (E(f42(f20(a2)),f9(f26(a22),a13))),
% 126.35/126.43 inference(scs_inference,[],[3320,3426,4461,4329,4447,3476,84,145,133,146,153,121,118,135,143,120,159])).
% 126.35/126.43 cnf(4573,plain,
% 126.35/126.43 (P2(f41(f41(f20(a3))),f41(f41(f20(a22))))),
% 126.35/126.43 inference(scs_inference,[],[3320,3426,4461,4329,3849,4447,3476,84,145,133,146,153,121,118,135,143,120,159,136,119,134,139,138])).
% 126.35/126.43 cnf(4579,plain,
% 126.35/126.43 (P2(f32(f25(f41(a46))),f20(a2))),
% 126.35/126.43 inference(scs_inference,[],[3320,3426,4461,4329,3849,4447,4532,3476,84,145,133,146,153,121,118,135,143,120,159,136,119,134,139,138,117,132,126])).
% 126.35/126.43 cnf(4584,plain,
% 126.35/126.43 (P2(f42(f20(a21)),f9(f26(a22),a13))),
% 126.35/126.43 inference(scs_inference,[],[3320,3426,4461,4329,3849,4447,4532,3476,84,145,133,146,153,121,118,135,143,120,159,136,119,134,139,138,117,132,126,6,10,42,123])).
% 126.35/126.43 cnf(4625,plain,
% 126.35/126.43 (E(f29(f44(x46251,x46252)),x46251)),
% 126.35/126.43 inference(rename_variables,[],[81])).
% 126.35/126.43 cnf(4629,plain,
% 126.35/126.43 (~P3(a39,f9(a21,a1))),
% 126.35/126.43 inference(scs_inference,[],[3320,3426,3126,3354,4528,4461,4329,3849,4447,4532,3476,328,81,105,84,145,133,146,153,121,118,135,143,120,159,136,119,134,139,138,117,132,126,6,10,42,123,24,13,15,38,23,30,33,27,34,36,12,40,28,35,16,4,25,43,41,21,14,37,7,19,32,26,22,39,9,29,11,5,8,31,20,18,17,2,45,144,152])).
% 126.35/126.43 cnf(4630,plain,
% 126.35/126.43 (~P3(x46301,a1)),
% 126.35/126.43 inference(rename_variables,[],[105])).
% 126.35/126.43 cnf(4632,plain,
% 126.35/126.43 (~P3(a39,f44(a1,a21))),
% 126.35/126.43 inference(scs_inference,[],[3320,3426,3126,3354,4528,4461,4329,3849,4447,4532,3476,328,81,105,4630,84,145,133,146,153,121,118,135,143,120,159,136,119,134,139,138,117,132,126,6,10,42,123,24,13,15,38,23,30,33,27,34,36,12,40,28,35,16,4,25,43,41,21,14,37,7,19,32,26,22,39,9,29,11,5,8,31,20,18,17,2,45,144,152,151])).
% 126.35/126.43 cnf(4635,plain,
% 126.35/126.43 (~P2(f27(a37,f20(a2)),a46)),
% 126.35/126.43 inference(scs_inference,[],[3320,3426,3126,3354,4528,4461,4329,3849,4447,4532,3476,1844,1650,328,81,105,4630,84,145,133,146,153,121,118,135,143,120,159,136,119,134,139,138,117,132,126,6,10,42,123,24,13,15,38,23,30,33,27,34,36,12,40,28,35,16,4,25,43,41,21,14,37,7,19,32,26,22,39,9,29,11,5,8,31,20,18,17,2,45,144,152,151,137])).
% 126.35/126.43 cnf(4641,plain,
% 126.35/126.43 (~P2(f20(a21),f32(f25(f41(a46))))),
% 126.35/126.43 inference(scs_inference,[],[3320,3426,3126,3354,4414,4528,4461,4329,3849,4447,4532,3476,1844,1650,328,2904,210,81,4625,105,4630,84,145,133,146,153,121,118,135,143,120,159,136,119,134,139,138,117,132,126,6,10,42,123,24,13,15,38,23,30,33,27,34,36,12,40,28,35,16,4,25,43,41,21,14,37,7,19,32,26,22,39,9,29,11,5,8,31,20,18,17,2,45,144,152,151,137,46,53,47])).
% 126.35/126.43 cnf(4642,plain,
% 126.35/126.43 (~P2(f41(f20(a2)),f24(f9(f20(a4),x46421)))),
% 126.35/126.43 inference(scs_inference,[],[3320,3426,3126,3354,4414,4528,4461,4329,3849,4447,4532,3476,1844,1650,328,2712,2904,210,81,4625,105,4630,84,145,133,146,153,121,118,135,143,120,159,136,119,134,139,138,117,132,126,6,10,42,123,24,13,15,38,23,30,33,27,34,36,12,40,28,35,16,4,25,43,41,21,14,37,7,19,32,26,22,39,9,29,11,5,8,31,20,18,17,2,45,144,152,151,137,46,53,47,48])).
% 126.35/126.43 cnf(4683,plain,
% 126.35/126.43 (P2(f42(f20(a2)),f9(f26(a22),a13))),
% 126.35/126.43 inference(scs_inference,[],[3530,4635,4563,4584,4331,3590,145,133,146,153,135,121,118,120,143,119,139,138,136,134,117,132,123])).
% 126.35/126.43 cnf(4685,plain,
% 126.35/126.43 (P2(f32(f25(f41(a46))),f20(a21))),
% 126.35/126.43 inference(scs_inference,[],[3530,4635,4563,4584,4331,4641,3590,145,133,146,153,135,121,118,120,143,119,139,138,136,134,117,132,123,126])).
% 126.35/126.43 cnf(4739,plain,
% 126.35/126.43 (P3(f20(a2),f9(f41(f20(a2)),x47391))),
% 126.35/126.43 inference(scs_inference,[],[3530,3379,4629,4635,4514,4563,4584,4331,4435,4641,3590,4642,4132,4148,1908,3426,1737,80,145,133,146,153,135,121,118,120,143,119,139,138,136,134,117,132,123,126,6,10,42,13,15,24,23,38,27,36,30,33,40,35,41,12,34,28,16,4,19,25,26,43,21,7,32,14,22,39,37,29,11,9,5,31,8,20,18,17,2,144,45,152,151,137,53])).
% 126.35/126.43 cnf(4744,plain,
% 126.35/126.43 (~P2(f41(f41(f20(a2))),f41(a33))),
% 126.35/126.43 inference(scs_inference,[],[3530,3379,4629,4635,4514,4563,4584,4331,4435,4641,3590,4469,4257,4642,4132,4148,4559,2977,1908,3426,1737,655,80,145,133,146,153,135,121,118,120,143,119,139,138,136,134,117,132,123,126,6,10,42,13,15,24,23,38,27,36,30,33,40,35,41,12,34,28,16,4,19,25,26,43,21,7,32,14,22,39,37,29,11,9,5,31,8,20,18,17,2,144,45,152,151,137,53,46,47,48])).
% 126.35/126.43 cnf(4785,plain,
% 126.35/126.43 (P2(f41(a33),f41(f41(f20(a2))))),
% 126.35/126.43 inference(scs_inference,[],[3753,4683,4744,4457,4408,3596,4472,2841,145,146,153,133,135,118,121,143,120,139,119,138,134,136,117,132,123,126])).
% 126.35/126.43 cnf(4811,plain,
% 126.35/126.43 (E(f9(f41(f20(a2)),x48111),f9(f41(f20(a21)),x48111))),
% 126.35/126.43 inference(scs_inference,[],[3753,4683,4744,4457,4408,3596,4472,2841,145,146,153,133,135,118,121,143,120,139,119,138,134,136,117,132,123,126,24,42,6,10,15,23,13,30,38,27,33,36,41,35,40,16,28,26,34,4,43,32,12,14,25])).
% 126.35/126.43 cnf(4829,plain,
% 126.35/126.43 (~P3(a7,f9(a8,a1))),
% 126.35/126.43 inference(scs_inference,[],[3753,3462,4683,4744,4457,4408,3596,4472,2742,2841,105,461,145,146,153,133,135,118,121,143,120,139,119,138,134,136,117,132,123,126,24,42,6,10,15,23,13,30,38,27,33,36,41,35,40,16,28,26,34,4,43,32,12,14,25,39,19,21,37,7,22,11,29,5,9,8,31,20,18,17,2,49,152])).
% 126.35/126.43 cnf(4830,plain,
% 126.35/126.43 (~P3(x48301,a1)),
% 126.35/126.43 inference(rename_variables,[],[105])).
% 126.35/126.43 cnf(4840,plain,
% 126.35/126.43 (E(f47(f9(x48401,x48402)),x48402)),
% 126.35/126.43 inference(rename_variables,[],[79])).
% 126.35/126.43 cnf(4841,plain,
% 126.35/126.43 (~P2(f32(f26(f20(a22))),a46)),
% 126.35/126.43 inference(scs_inference,[],[3753,3462,4683,4198,4470,4744,4457,4408,3596,4472,2742,2841,1868,4514,1680,3939,79,492,105,4830,461,145,146,153,133,135,118,121,143,120,139,119,138,134,136,117,132,123,126,24,42,6,10,15,23,13,30,38,27,33,36,41,35,40,16,28,26,34,4,43,32,12,14,25,39,19,21,37,7,22,11,29,5,9,8,31,20,18,17,2,49,152,50,144,151,45,137])).
% 126.35/126.43 cnf(4847,plain,
% 126.35/126.43 (~P2(f41(f41(f20(a3))),f41(a33))),
% 126.35/126.43 inference(scs_inference,[],[3753,3462,4632,4683,4198,4470,4744,4457,4408,3596,4472,4181,2742,2841,1868,4514,1680,3939,2892,79,4840,492,105,4830,461,145,146,153,133,135,118,121,143,120,139,119,138,134,136,117,132,123,126,24,42,6,10,15,23,13,30,38,27,33,36,41,35,40,16,28,26,34,4,43,32,12,14,25,39,19,21,37,7,22,11,29,5,9,8,31,20,18,17,2,49,152,50,144,151,45,137,53,46,47])).
% 126.35/126.43 cnf(4911,plain,
% 126.35/126.43 (E(f20(f16(x49111,x49112,x49113,f20(a2),x49114,x49115,x49116)),f20(f16(x49111,x49112,x49113,f20(a21),x49114,x49115,x49116)))),
% 126.35/126.43 inference(scs_inference,[],[3859,4579,4847,4841,4739,3817,3687,4477,2810,145,146,153,133,135,121,143,118,139,119,120,138,134,136,117,132,126,123,42,24,6,13,15,10,27,38,30,23,41,35,28,33,36,26,40,43,4])).
% 126.35/126.43 cnf(4934,plain,
% 126.35/126.43 (~P2(f41(f41(f20(a22))),f41(a33))),
% 126.35/126.43 inference(scs_inference,[],[3859,3478,4579,4847,4841,4739,3817,3687,4477,4573,2810,145,146,153,133,135,121,143,118,139,119,120,138,134,136,117,132,126,123,42,24,6,13,15,10,27,38,30,23,41,35,28,33,36,26,40,43,4,16,34,21,32,25,12,7,11,19,37,14,39,29,22,5,9,8,31,18,20,17,2,144])).
% 126.35/126.43 cnf(4940,plain,
% 126.35/126.43 (~P2(f32(f25(f20(a4))),a46)),
% 126.35/126.43 inference(scs_inference,[],[3859,3963,3478,4829,4579,4847,4841,4739,3817,3687,4477,4573,2810,1898,1722,145,146,153,133,135,121,143,118,139,119,120,138,134,136,117,132,126,123,42,24,6,13,15,10,27,38,30,23,41,35,28,33,36,26,40,43,4,16,34,21,32,25,12,7,11,19,37,14,39,29,22,5,9,8,31,18,20,17,2,144,152,151,137])).
% 126.35/126.43 cnf(4942,plain,
% 126.35/126.43 (P3(f20(a2),f9(f41(f20(a21)),x49421))),
% 126.35/126.43 inference(scs_inference,[],[3859,3963,3478,4829,4579,4847,4841,4739,3817,3687,4477,4811,4573,2810,1898,1722,145,146,153,133,135,121,143,118,139,119,120,138,134,136,117,132,126,123,42,24,6,13,15,10,27,38,30,23,41,35,28,33,36,26,40,43,4,16,34,21,32,25,12,7,11,19,37,14,39,29,22,5,9,8,31,18,20,17,2,144,152,151,137,53])).
% 126.35/126.43 cnf(5043,plain,
% 126.35/126.43 (~P3(f24(f9(a38,x50431)),f9(f24(f9(a7,a1)),f47(f9(a7,a1))))),
% 126.35/126.43 inference(scs_inference,[],[4075,3237,3588,4426,4685,4934,4940,4942,4785,4262,3701,3862,4485,2811,1878,1694,2792,145,146,153,135,133,143,121,118,139,119,120,138,134,136,117,132,126,123,42,24,13,15,27,10,38,6,30,23,41,35,36,28,43,40,4,33,12,26,19,16,21,7,34,32,14,11,25,37,39,22,29,9,5,18,8,31,20,17,2,144,151,152,137,53])).
% 126.35/126.43 cnf(5161,plain,
% 126.35/126.43 (~E(f20(a4),f20(a2))),
% 126.35/126.43 inference(scs_inference,[],[4563,3114,2875,2,4,123])).
% 126.35/126.43 cnf(5233,plain,
% 126.35/126.43 (~E(f24(f9(a38,x52331)),f24(f9(a7,a1)))),
% 126.35/126.43 inference(scs_inference,[],[4430,4017,3592,4744,2874,2992,4785,3878,5043,2723,4205,2,17,4,42,126,123,132,138,134,143,146,133])).
% 126.35/126.43 cnf(5239,plain,
% 126.35/126.43 (~E(f41(f41(f47(f9(x52391,x52392)))),x52392)),
% 126.35/126.43 inference(scs_inference,[],[588,4430,283,4017,3592,4744,2874,2992,4785,3878,5043,2723,4911,4205,4419,2,17,4,42,126,123,132,138,134,143,146,133,145,266,3])).
% 126.35/126.43 cnf(5278,plain,
% 126.35/126.43 (~E(f41(f41(f20(a3))),f41(a33))),
% 126.35/126.43 inference(scs_inference,[],[4461,4847,5161,5233,5239,2,17,4,42,123])).
% 126.35/126.43 cnf(5328,plain,
% 126.35/126.43 ($false),
% 126.35/126.43 inference(scs_inference,[],[2861,5278,2,17]),
% 126.35/126.43 ['proof']).
% 126.35/126.44 % SZS output end Proof
% 126.35/126.44 % Total time :125.710000s
%------------------------------------------------------------------------------