%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : SWV416+1 : TPTP v8.2.0. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% Computer : n025.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:09 EDT 2024
% Result : Theorem 58.84s 58.91s
% Output : CNFRefutation 58.92s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.09 % Problem : SWV416+1 : TPTP v8.2.0. Released v3.3.0.
% 0.00/0.09 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% 0.09/0.29 % Computer : n025.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 13:58:24 EDT 2024
% 0.09/0.29 % CPUTime :
% 0.15/0.47 start to proof:theBenchmark
% 58.84/58.89 %-------------------------------------------
% 58.84/58.89 % File :CSE---1.7
% 58.84/58.89 % Problem :theBenchmark
% 58.84/58.89 % Transform :cnf
% 58.84/58.89 % Format :tptp:raw
% 58.84/58.89 % Command :java -jar mcs_scs.jar %d %s
% 58.84/58.89
% 58.84/58.89 % Result :Theorem 58.360000s
% 58.84/58.89 % Output :CNFRefutation 58.360000s
% 58.84/58.89 %-------------------------------------------
% 58.84/58.91 %--------------------------------------------------------------------------
% 58.84/58.91 % File : SWV416+1 : TPTP v8.2.0. Released v3.3.0.
% 58.84/58.91 % Domain : Software Verification
% 58.84/58.91 % Problem : Priority queue checker: Formula (8)
% 58.84/58.91 % Version : [dNP05] axioms.
% 58.84/58.91 % English :
% 58.84/58.91
% 58.84/58.91 % Refs : [Pis06] Piskac (2006), Email to Geoff Sutcliffe
% 58.84/58.91 % : [dNP05] de Nivelle & Piskac (2005), Verification of an Off-Lin
% 58.84/58.91 % Source : [Pis06]
% 58.84/58.91 % Names : cpq003 [Pis06]
% 58.84/58.91
% 58.84/58.91 % Status : Theorem
% 58.84/58.91 % Rating : 0.25 v8.2.0, 0.28 v8.1.0, 0.25 v7.5.0, 0.28 v7.4.0, 0.23 v7.3.0, 0.24 v7.1.0, 0.30 v6.4.0, 0.35 v6.3.0, 0.38 v6.2.0, 0.40 v6.0.0, 0.35 v5.5.0, 0.41 v5.4.0, 0.46 v5.3.0, 0.52 v5.2.0, 0.45 v5.1.0, 0.43 v5.0.0, 0.38 v4.1.0, 0.43 v4.0.0, 0.46 v3.7.0, 0.40 v3.5.0, 0.47 v3.3.0
% 58.84/58.91 % Syntax : Number of formulae : 65 ( 24 unt; 0 def)
% 58.84/58.91 % Number of atoms : 135 ( 43 equ)
% 58.84/58.91 % Maximal formula atoms : 4 ( 2 avg)
% 58.84/58.91 % Number of connectives : 86 ( 16 ~; 4 |; 22 &)
% 58.84/58.91 % ( 16 <=>; 28 =>; 0 <=; 0 <~>)
% 58.84/58.91 % Maximal formula depth : 9 ( 5 avg)
% 58.84/58.91 % Maximal term depth : 5 ( 1 avg)
% 58.84/58.91 % Number of predicates : 21 ( 19 usr; 1 prp; 0-3 aty)
% 58.84/58.91 % Number of functors : 26 ( 26 usr; 4 con; 0-3 aty)
% 58.84/58.91 % Number of variables : 176 ( 173 !; 3 ?)
% 58.84/58.91 % SPC : FOF_THM_RFO_SEQ
% 58.84/58.91
% 58.84/58.91 % Comments :
% 58.84/58.91 %--------------------------------------------------------------------------
% 58.84/58.91 %----Include the axioms about priority queues and checked priority queues
% 58.84/58.91 include('Axioms/SWV007+0.ax').
% 58.84/58.91 include('Axioms/SWV007+1.ax').
% 58.84/58.91 include('Axioms/SWV007+2.ax').
% 58.84/58.91 include('Axioms/SWV007+3.ax').
% 58.84/58.91 include('Axioms/SWV007+4.ax').
% 58.84/58.91 %--------------------------------------------------------------------------
% 58.84/58.91 fof(main3_li12,lemma,
% 58.84/58.91 ! [U,V,W,X,Y] : i(triple(U,W,X)) = i(triple(V,W,Y)) ).
% 58.84/58.91
% 58.84/58.91 fof(main3_li34,lemma,
% 58.84/58.91 ! [U,V,W,X] :
% 58.84/58.91 ( contains_pq(i(triple(U,V,W)),X)
% 58.84/58.91 => i(remove_cpq(triple(U,V,W),X)) = remove_pq(i(triple(U,V,W)),X) ) ).
% 58.84/58.91
% 58.84/58.91 fof(co3,conjecture,
% 58.84/58.91 ! [U,V,W,X] :
% 58.84/58.91 ( pi_remove(triple(U,V,W),X)
% 58.84/58.91 => ( phi(remove_cpq(triple(U,V,W),X))
% 58.84/58.91 => ( pi_sharp_remove(i(triple(U,V,W)),X)
% 58.84/58.91 & i(remove_cpq(triple(U,V,W),X)) = remove_pq(i(triple(U,V,W)),X) ) ) ) ).
% 58.84/58.91
% 58.84/58.91 %--------------------------------------------------------------------------
% 58.84/58.91 %-------------------------------------------
% 58.84/58.91 % Proof found
% 58.84/58.91 % SZS status Theorem for theBenchmark
% 58.84/58.91 % SZS output start Proof
% 58.84/58.92 %ClaNum:166(EqnAxiom:77)
% 58.84/58.92 %VarNum:481(SingletonVarNum:229)
% 58.84/58.92 %MaxLitNum:4
% 58.84/58.92 %MaxfuncDepth:4
% 58.84/58.92 %SharedTerms:19
% 58.84/58.92 %goalClause: 91 94 166
% 58.84/58.92 %singleGoalClaCount:2
% 58.84/58.92 [97]~P2(a4)
% 58.84/58.92 [98]~P7(a1)
% 58.84/58.92 [91]P10(f30(a8,a13,a14),a15)
% 58.84/58.92 [94]P11(f27(f30(a8,a13,a14),a15))
% 58.84/58.92 [79]P1(a2,x791)
% 58.84/58.92 [80]P1(x801,x801)
% 58.84/58.92 [81]P9(x811,x811)
% 58.84/58.92 [99]~P4(a4,x991)
% 58.84/58.92 [100]~P6(a1,x1001)
% 58.84/58.92 [78]E(f5(a1,x781),a1)
% 58.84/58.92 [101]~P12(a1,x1011,x1012)
% 58.84/58.92 [82]P2(f6(x821,x822))
% 58.84/58.92 [90]P3(f30(x901,a1,x902))
% 58.84/58.92 [102]~P13(f30(x1021,x1022,a3))
% 58.84/58.92 [83]E(f22(f6(x831,x832),x832),x831)
% 58.84/58.92 [88]E(f7(f30(x881,a1,x882)),a2)
% 58.84/58.92 [89]E(f17(f30(x891,a1,x892)),a4)
% 58.84/58.92 [92]E(f16(f30(x921,a1,x922)),f30(x921,a1,a3))
% 58.84/58.92 [84]E(f6(f6(x841,x842),x843),f6(f6(x841,x843),x842))
% 58.84/58.92 [85]P7(f24(x851,f23(x852,x853)))
% 58.84/58.92 [86]E(f28(f24(x861,f23(x862,x863)),x862),x861)
% 58.84/58.92 [87]E(f26(f24(x871,f23(x872,x873)),x872),x873)
% 58.84/58.92 [95]E(f30(f25(x951,x952),f24(x953,f23(x952,a2)),x954),f21(f30(x951,x953,x954),x952))
% 58.84/58.92 [93]E(f17(f30(x931,x932,x933)),f17(f30(x934,x932,x935)))
% 58.84/58.92 [96]E(f17(f30(x961,f24(x962,f23(x963,x964)),x965)),f6(f17(f30(x961,x962,x965)),x963))
% 58.84/58.92 [166]~P18(f17(f30(a8,a13,a14)),a15)+~E(f17(f27(f30(a8,a13,a14),a15)),f22(f17(f30(a8,a13,a14)),a15))
% 58.84/58.92 [103]~P11(x1031)+P3(f9(x1031))
% 58.84/58.92 [104]~P11(x1041)+P13(f9(x1041))
% 58.84/58.92 [105]~P11(x1051)+P9(x1051,f9(x1051))
% 58.84/58.92 [107]~P14(x1071)+P15(f17(x1071),f10(x1071))
% 58.84/58.92 [108]~P16(x1081)+P15(f17(x1081),f12(x1081))
% 58.84/58.92 [106]P1(x1062,x1061)+P1(x1061,x1062)
% 58.84/58.92 [111]~P17(x1111,x1112)+P1(x1111,x1112)
% 58.84/58.92 [112]~P18(x1121,x1122)+P4(x1121,x1122)
% 58.84/58.92 [113]~P15(x1131,x1132)+P4(x1131,x1132)
% 58.84/58.92 [114]~P19(x1141,x1142)+P4(x1141,x1142)
% 58.84/58.92 [115]~P15(x1151,x1152)+P8(x1151,x1152)
% 58.84/58.92 [116]~P19(x1161,x1162)+P8(x1161,x1162)
% 58.84/58.92 [117]~P4(x1171,x1172)+P18(x1171,x1172)
% 58.84/58.92 [122]~P17(x1222,x1221)+~P1(x1221,x1222)
% 58.84/58.92 [109]P14(x1091)+~P15(f17(x1091),x1092)
% 58.84/58.92 [110]P16(x1101)+~P15(f17(x1101),x1102)
% 58.84/58.92 [119]~P9(x1191,x1192)+P9(x1191,f16(x1192))
% 58.84/58.92 [120]~P10(x1201,x1202)+P18(f17(x1201),x1202)
% 58.84/58.92 [123]P10(x1231,x1232)+~P18(f17(x1231),x1232)
% 58.84/58.92 [125]P8(x1251,x1252)+P4(x1251,f11(x1251,x1252))
% 58.84/58.92 [137]P8(x1371,x1372)+~P1(x1372,f11(x1371,x1372))
% 58.84/58.92 [139]~P9(x1391,x1392)+P9(x1391,f27(f16(x1392),f7(x1392)))
% 58.84/58.92 [121]~E(x1212,x1213)+P4(f6(x1211,x1212),x1213)
% 58.84/58.92 [133]~P9(x1331,x1332)+P9(x1331,f21(x1332,x1333))
% 58.84/58.92 [134]~P9(x1341,x1342)+P9(x1341,f27(x1342,x1343))
% 58.84/58.92 [135]~P4(x1351,x1353)+P4(f6(x1351,x1352),x1353)
% 58.84/58.92 [142]E(x1421,a3)+P13(f30(x1422,x1423,x1421))
% 58.84/58.92 [144]E(x1441,a1)+E(f7(f30(x1442,x1441,x1443)),f20(x1442))
% 58.84/58.92 [147]~P6(x1472,x1474)+P5(f30(x1471,x1472,x1473),x1474)
% 58.84/58.92 [153]P6(x1531,x1532)+~P5(f30(x1533,x1531,x1534),x1532)
% 58.84/58.92 [140]~E(x1402,x1404)+P6(f24(x1401,f23(x1402,x1403)),x1404)
% 58.84/58.92 [143]~P6(x1431,x1434)+P6(f24(x1431,f23(x1432,x1433)),x1434)
% 58.84/58.92 [152]P6(x1522,x1524)+E(f27(f30(x1521,x1522,x1523),x1524),f30(x1521,x1522,a3))
% 58.84/58.92 [149]~P1(x1492,x1494)+E(f24(f5(x1491,x1492),f23(x1493,x1494)),f5(f24(x1491,f23(x1493,x1494)),x1492))
% 58.84/58.92 [150]~P17(x1503,x1504)+E(f5(f24(x1501,f23(x1502,x1503)),x1504),f24(f5(x1501,x1504),f23(x1502,x1504)))
% 58.84/58.92 [165]~P4(f17(f30(x1651,x1652,x1653)),x1654)+E(f17(f27(f30(x1651,x1652,x1653),x1654)),f22(f17(f30(x1651,x1652,x1653)),x1654))
% 58.84/58.92 [154]~P12(x1541,x1544,x1545)+P12(f24(x1541,f23(x1542,x1543)),x1544,x1545)
% 58.84/58.92 [162]~P17(x1621,x1622)+~P3(f30(x1623,f24(x1624,f23(x1621,x1622)),x1625))
% 58.84/58.92 [124]P17(x1242,x1241)+~P1(x1242,x1241)+P1(x1241,x1242)
% 58.84/58.92 [128]~P4(x1281,x1282)+~P8(x1281,x1282)+P15(x1281,x1282)
% 58.84/58.92 [129]~P4(x1291,x1292)+~P8(x1291,x1292)+P19(x1291,x1292)
% 58.84/58.92 [130]~P4(x1301,x1302)+~P8(x1301,x1302)+E(f18(x1301,x1302),x1301)
% 58.84/58.92 [131]~P4(x1311,x1312)+~P8(x1311,x1312)+E(f19(x1311,x1312),x1312)
% 58.84/58.92 [132]~P4(x1321,x1322)+~P8(x1321,x1322)+E(f31(x1321,x1322),x1322)
% 58.84/58.92 [136]~P4(x1361,x1362)+~P8(x1361,x1362)+E(f32(x1361,x1362),f22(x1361,x1362))
% 58.84/58.92 [126]~P8(x1263,x1261)+P1(x1261,x1262)+~P4(x1263,x1262)
% 58.84/58.92 [127]~P1(x1271,x1273)+P1(x1271,x1272)+~P1(x1273,x1272)
% 58.84/58.92 [138]E(x1381,x1382)+P4(x1383,x1382)+~P4(f6(x1383,x1381),x1382)
% 58.84/58.92 [141]~P4(x1413,x1411)+E(x1411,x1412)+E(f22(f6(x1413,x1412),x1411),f6(f22(x1413,x1411),x1412))
% 58.84/58.92 [155]P6(x1551,f20(x1552))+E(x1551,a1)+E(f16(f30(x1552,x1551,x1553)),f30(x1552,f5(x1551,f20(x1552)),a3))
% 58.84/58.92 [148]E(x1481,x1482)+P6(x1483,x1482)+~P6(f24(x1483,f23(x1481,x1484)),x1482)
% 58.84/58.92 [158]~P6(x1582,x1584)+~P17(x1584,f26(x1582,x1584))+E(f27(f30(x1581,x1582,x1583),x1584),f30(f29(x1581,x1584),f28(x1582,x1584),a3))
% 58.84/58.92 [159]~P6(x1593,x1592)+~P1(f26(x1593,x1592),x1592)+E(f30(f29(x1591,x1592),f28(x1593,x1592),x1594),f27(f30(x1591,x1593,x1594),x1592))
% 58.84/58.92 [145]~P6(x1453,x1452)+E(x1451,x1452)+E(f26(f24(x1453,f23(x1451,x1454)),x1452),f26(x1453,x1452))
% 58.84/58.92 [151]~P6(x1513,x1512)+E(x1511,x1512)+E(f28(f24(x1513,f23(x1511,x1514)),x1512),f24(f28(x1513,x1512),f23(x1511,x1514)))
% 58.84/58.92 [146]~E(x1463,x1465)+~E(x1462,x1464)+P12(f24(x1461,f23(x1462,x1463)),x1464,x1465)
% 58.84/58.92 [156]E(x1561,x1562)+P12(x1563,x1564,x1562)+~P12(f24(x1563,f23(x1565,x1561)),x1564,x1562)
% 58.84/58.92 [157]E(x1571,x1572)+P12(x1573,x1572,x1574)+~P12(f24(x1573,f23(x1571,x1575)),x1572,x1574)
% 58.84/58.92 [163]~P1(x1634,x1633)+~P3(f30(x1631,x1632,x1635))+P3(f30(x1631,f24(x1632,f23(x1633,x1634)),x1635))
% 58.84/58.92 [164]~P1(x1644,x1645)+P3(f30(x1641,x1642,x1643))+~P3(f30(x1641,f24(x1642,f23(x1645,x1644)),x1643))
% 58.84/58.92 [118]~P13(x1182)+~P9(x1181,x1182)+P11(x1181)+~P3(x1182)
% 58.84/58.92 [160]~P6(x1601,f20(x1602))+E(x1601,a1)+~P17(f20(x1602),f26(x1601,f20(x1602)))+E(f16(f30(x1602,x1601,x1603)),f30(x1602,f5(x1601,f20(x1602)),a3))
% 58.84/58.92 [161]~P6(x1611,f20(x1612))+E(x1611,a1)+~P1(f26(x1611,f20(x1612)),f20(x1612))+E(f30(x1612,f5(x1611,f20(x1612)),x1613),f16(f30(x1612,x1611,x1613)))
% 58.84/58.92 %EqnAxiom
% 58.84/58.92 [1]E(x11,x11)
% 58.84/58.92 [2]E(x22,x21)+~E(x21,x22)
% 58.84/58.92 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 58.84/58.92 [4]~E(x41,x42)+E(f5(x41,x43),f5(x42,x43))
% 58.84/58.92 [5]~E(x51,x52)+E(f5(x53,x51),f5(x53,x52))
% 58.84/58.92 [6]~E(x61,x62)+E(f6(x61,x63),f6(x62,x63))
% 58.84/58.92 [7]~E(x71,x72)+E(f6(x73,x71),f6(x73,x72))
% 58.84/58.92 [8]~E(x81,x82)+E(f30(x81,x83,x84),f30(x82,x83,x84))
% 58.84/58.92 [9]~E(x91,x92)+E(f30(x93,x91,x94),f30(x93,x92,x94))
% 58.84/58.92 [10]~E(x101,x102)+E(f30(x103,x104,x101),f30(x103,x104,x102))
% 58.84/58.92 [11]~E(x111,x112)+E(f22(x111,x113),f22(x112,x113))
% 58.84/58.92 [12]~E(x121,x122)+E(f22(x123,x121),f22(x123,x122))
% 58.84/58.92 [13]~E(x131,x132)+E(f17(x131),f17(x132))
% 58.84/58.92 [14]~E(x141,x142)+E(f23(x141,x143),f23(x142,x143))
% 58.84/58.92 [15]~E(x151,x152)+E(f23(x153,x151),f23(x153,x152))
% 58.84/58.92 [16]~E(x161,x162)+E(f24(x161,x163),f24(x162,x163))
% 58.84/58.92 [17]~E(x171,x172)+E(f24(x173,x171),f24(x173,x172))
% 58.84/58.92 [18]~E(x181,x182)+E(f27(x181,x183),f27(x182,x183))
% 58.84/58.92 [19]~E(x191,x192)+E(f27(x193,x191),f27(x193,x192))
% 58.84/58.92 [20]~E(x201,x202)+E(f20(x201),f20(x202))
% 58.84/58.92 [21]~E(x211,x212)+E(f7(x211),f7(x212))
% 58.84/58.92 [22]~E(x221,x222)+E(f26(x221,x223),f26(x222,x223))
% 58.84/58.93 [23]~E(x231,x232)+E(f26(x233,x231),f26(x233,x232))
% 58.84/58.93 [24]~E(x241,x242)+E(f16(x241),f16(x242))
% 58.84/58.93 [25]~E(x251,x252)+E(f28(x251,x253),f28(x252,x253))
% 58.84/58.93 [26]~E(x261,x262)+E(f28(x263,x261),f28(x263,x262))
% 58.84/58.93 [27]~E(x271,x272)+E(f9(x271),f9(x272))
% 58.84/58.93 [28]~E(x281,x282)+E(f25(x281,x283),f25(x282,x283))
% 58.84/58.93 [29]~E(x291,x292)+E(f25(x293,x291),f25(x293,x292))
% 58.84/58.93 [30]~E(x301,x302)+E(f29(x301,x303),f29(x302,x303))
% 58.84/58.93 [31]~E(x311,x312)+E(f29(x313,x311),f29(x313,x312))
% 58.84/58.93 [32]~E(x321,x322)+E(f18(x321,x323),f18(x322,x323))
% 58.84/58.93 [33]~E(x331,x332)+E(f18(x333,x331),f18(x333,x332))
% 58.84/58.93 [34]~E(x341,x342)+E(f11(x341,x343),f11(x342,x343))
% 58.84/58.93 [35]~E(x351,x352)+E(f11(x353,x351),f11(x353,x352))
% 58.84/58.93 [36]~E(x361,x362)+E(f31(x361,x363),f31(x362,x363))
% 58.84/58.93 [37]~E(x371,x372)+E(f31(x373,x371),f31(x373,x372))
% 58.84/58.93 [38]~E(x381,x382)+E(f10(x381),f10(x382))
% 58.84/58.93 [39]~E(x391,x392)+E(f19(x391,x393),f19(x392,x393))
% 58.84/58.93 [40]~E(x401,x402)+E(f19(x403,x401),f19(x403,x402))
% 58.84/58.93 [41]~E(x411,x412)+E(f21(x411,x413),f21(x412,x413))
% 58.84/58.93 [42]~E(x421,x422)+E(f21(x423,x421),f21(x423,x422))
% 58.84/58.93 [43]~E(x431,x432)+E(f12(x431),f12(x432))
% 58.84/58.93 [44]~E(x441,x442)+E(f32(x441,x443),f32(x442,x443))
% 58.84/58.93 [45]~E(x451,x452)+E(f32(x453,x451),f32(x453,x452))
% 58.84/58.93 [46]P1(x462,x463)+~E(x461,x462)+~P1(x461,x463)
% 58.84/58.93 [47]P1(x473,x472)+~E(x471,x472)+~P1(x473,x471)
% 58.84/58.93 [48]P18(x482,x483)+~E(x481,x482)+~P18(x481,x483)
% 58.84/58.93 [49]P18(x493,x492)+~E(x491,x492)+~P18(x493,x491)
% 58.84/58.93 [50]P9(x502,x503)+~E(x501,x502)+~P9(x501,x503)
% 58.84/58.93 [51]P9(x513,x512)+~E(x511,x512)+~P9(x513,x511)
% 58.84/58.93 [52]~P2(x521)+P2(x522)+~E(x521,x522)
% 58.84/58.93 [53]~P7(x531)+P7(x532)+~E(x531,x532)
% 58.84/58.93 [54]~P3(x541)+P3(x542)+~E(x541,x542)
% 58.84/58.93 [55]P10(x552,x553)+~E(x551,x552)+~P10(x551,x553)
% 58.84/58.93 [56]P10(x563,x562)+~E(x561,x562)+~P10(x563,x561)
% 58.84/58.93 [57]~P11(x571)+P11(x572)+~E(x571,x572)
% 58.84/58.93 [58]P6(x582,x583)+~E(x581,x582)+~P6(x581,x583)
% 58.84/58.93 [59]P6(x593,x592)+~E(x591,x592)+~P6(x593,x591)
% 58.84/58.93 [60]P8(x602,x603)+~E(x601,x602)+~P8(x601,x603)
% 58.84/58.93 [61]P8(x613,x612)+~E(x611,x612)+~P8(x613,x611)
% 58.84/58.93 [62]P4(x622,x623)+~E(x621,x622)+~P4(x621,x623)
% 58.84/58.93 [63]P4(x633,x632)+~E(x631,x632)+~P4(x633,x631)
% 58.84/58.93 [64]P17(x642,x643)+~E(x641,x642)+~P17(x641,x643)
% 58.84/58.93 [65]P17(x653,x652)+~E(x651,x652)+~P17(x653,x651)
% 58.84/58.93 [66]P12(x662,x663,x664)+~E(x661,x662)+~P12(x661,x663,x664)
% 58.84/58.93 [67]P12(x673,x672,x674)+~E(x671,x672)+~P12(x673,x671,x674)
% 58.84/58.93 [68]P12(x683,x684,x682)+~E(x681,x682)+~P12(x683,x684,x681)
% 58.84/58.93 [69]~P13(x691)+P13(x692)+~E(x691,x692)
% 58.84/58.93 [70]P15(x702,x703)+~E(x701,x702)+~P15(x701,x703)
% 58.84/58.93 [71]P15(x713,x712)+~E(x711,x712)+~P15(x713,x711)
% 58.84/58.93 [72]P5(x722,x723)+~E(x721,x722)+~P5(x721,x723)
% 58.84/58.93 [73]P5(x733,x732)+~E(x731,x732)+~P5(x733,x731)
% 58.84/58.93 [74]P19(x742,x743)+~E(x741,x742)+~P19(x741,x743)
% 58.84/58.93 [75]P19(x753,x752)+~E(x751,x752)+~P19(x753,x751)
% 58.84/58.93 [76]~P16(x761)+P16(x762)+~E(x761,x762)
% 58.84/58.93 [77]~P14(x771)+P14(x772)+~E(x771,x772)
% 58.84/58.93
% 58.84/58.93 %-------------------------------------------
% 58.91/58.94 cnf(167,plain,
% 58.91/58.94 (P4(f6(x1672,x1671),x1671)),
% 58.91/58.94 inference(equality_inference,[],[121])).
% 58.91/58.94 cnf(168,plain,
% 58.91/58.94 (P6(f24(x1682,f23(x1681,x1683)),x1681)),
% 58.91/58.94 inference(equality_inference,[],[140])).
% 58.91/58.94 cnf(169,plain,
% 58.91/58.94 (E(x1691,f22(f6(x1691,x1692),x1692))),
% 58.91/58.94 inference(scs_inference,[],[83,2])).
% 58.91/58.94 cnf(172,plain,
% 58.91/58.94 (~P15(a4,x1721)),
% 58.91/58.94 inference(scs_inference,[],[83,99,2,112,113])).
% 58.91/58.94 cnf(174,plain,
% 58.91/58.94 (~P19(a4,x1741)),
% 58.91/58.94 inference(scs_inference,[],[83,99,2,112,113,114])).
% 58.91/58.94 cnf(177,plain,
% 58.91/58.94 (~P4(a4,x1771)),
% 58.91/58.94 inference(rename_variables,[],[99])).
% 58.91/58.94 cnf(179,plain,
% 58.91/58.94 (~P17(x1791,x1791)),
% 58.91/58.94 inference(scs_inference,[],[83,80,99,2,112,113,114,125,122])).
% 58.91/58.94 cnf(181,plain,
% 58.91/58.94 (P8(x1811,a2)),
% 58.91/58.94 inference(scs_inference,[],[83,80,79,99,2,112,113,114,125,122,137])).
% 58.91/58.94 cnf(184,plain,
% 58.91/58.94 (E(f28(f24(f22(f6(x1841,x1842),x1842),f23(x1843,x1844)),x1843),x1841)),
% 58.91/58.94 inference(scs_inference,[],[83,86,80,79,99,2,112,113,114,125,122,137,3])).
% 58.91/58.94 cnf(186,plain,
% 58.91/58.94 (P10(f22(f6(f30(a8,a13,a14),x1861),x1861),a15)),
% 58.91/58.94 inference(scs_inference,[],[91,83,86,80,79,99,2,112,113,114,125,122,137,3,55])).
% 58.91/58.94 cnf(187,plain,
% 58.91/58.94 (P1(f30(a8,a13,a14),f22(f6(f30(a8,a13,a14),x1871),x1871))),
% 58.91/58.94 inference(scs_inference,[],[91,83,86,80,79,99,2,112,113,114,125,122,137,3,55,46])).
% 58.91/58.94 cnf(188,plain,
% 58.91/58.94 (P1(x1881,x1881)),
% 58.91/58.94 inference(rename_variables,[],[80])).
% 58.91/58.94 cnf(189,plain,
% 58.91/58.94 (E(f22(f6(x1891,x1892),x1892),x1891)),
% 58.91/58.94 inference(rename_variables,[],[83])).
% 58.91/58.94 cnf(190,plain,
% 58.91/58.94 (P1(f22(f6(x1901,x1902),x1902),x1901)),
% 58.91/58.94 inference(scs_inference,[],[91,83,189,86,80,188,79,99,2,112,113,114,125,122,137,3,55,46,47])).
% 58.91/58.94 cnf(192,plain,
% 58.91/58.94 (P9(x1921,f22(f6(x1921,x1922),x1922))),
% 58.91/58.94 inference(scs_inference,[],[91,83,189,86,80,188,81,79,99,2,112,113,114,125,122,137,3,55,46,47,50])).
% 58.91/58.94 cnf(193,plain,
% 58.91/58.94 (P9(x1931,x1931)),
% 58.91/58.94 inference(rename_variables,[],[81])).
% 58.91/58.94 cnf(194,plain,
% 58.91/58.94 (P9(f22(f6(x1941,x1942),x1942),x1941)),
% 58.91/58.94 inference(scs_inference,[],[91,83,189,86,80,188,81,193,79,99,2,112,113,114,125,122,137,3,55,46,47,50,51])).
% 58.91/58.94 cnf(196,plain,
% 58.91/58.94 (~P2(f22(f6(a4,x1961),x1961))),
% 58.91/58.94 inference(scs_inference,[],[91,83,189,86,80,188,81,193,79,99,97,2,112,113,114,125,122,137,3,55,46,47,50,51,52])).
% 58.91/58.94 cnf(197,plain,
% 58.91/58.94 (E(f22(f6(x1971,x1972),x1972),x1971)),
% 58.91/58.94 inference(rename_variables,[],[83])).
% 58.91/58.94 cnf(198,plain,
% 58.91/58.94 (~P7(f22(f6(a1,x1981),x1981))),
% 58.91/58.94 inference(scs_inference,[],[91,83,189,197,86,80,188,81,193,79,99,97,98,2,112,113,114,125,122,137,3,55,46,47,50,51,52,53])).
% 58.91/58.94 cnf(199,plain,
% 58.91/58.94 (E(f22(f6(x1991,x1992),x1992),x1991)),
% 58.91/58.94 inference(rename_variables,[],[83])).
% 58.91/58.94 cnf(200,plain,
% 58.91/58.94 (~E(f24(x2001,f23(x2002,x2003)),a1)),
% 58.91/58.94 inference(scs_inference,[],[91,168,83,189,197,86,80,188,81,193,79,99,100,97,98,2,112,113,114,125,122,137,3,55,46,47,50,51,52,53,58])).
% 58.91/58.94 cnf(201,plain,
% 58.91/58.94 (P6(f24(x2011,f23(x2012,x2013)),x2012)),
% 58.91/58.94 inference(rename_variables,[],[168])).
% 58.91/58.94 cnf(202,plain,
% 58.91/58.94 (P6(f24(x2021,f23(f22(f6(x2022,x2023),x2023),x2024)),x2022)),
% 58.91/58.94 inference(scs_inference,[],[91,168,201,83,189,197,199,86,80,188,81,193,79,99,100,97,98,2,112,113,114,125,122,137,3,55,46,47,50,51,52,53,58,59])).
% 58.91/58.94 cnf(204,plain,
% 58.91/58.94 (~E(f6(x2041,x2042),a4)),
% 58.91/58.94 inference(scs_inference,[],[91,167,168,201,83,189,197,199,86,80,188,81,193,79,99,177,100,97,98,2,112,113,114,125,122,137,3,55,46,47,50,51,52,53,58,59,62])).
% 58.91/58.94 cnf(205,plain,
% 58.91/58.94 (P4(f6(x2051,x2052),x2052)),
% 58.91/58.94 inference(rename_variables,[],[167])).
% 58.91/58.94 cnf(206,plain,
% 58.91/58.94 (P4(f6(x2061,f22(f6(x2062,x2063),x2063)),x2062)),
% 58.91/58.94 inference(scs_inference,[],[91,167,205,168,201,83,189,197,199,86,80,188,81,193,79,99,177,100,97,98,2,112,113,114,125,122,137,3,55,46,47,50,51,52,53,58,59,62,63])).
% 58.91/58.94 cnf(207,plain,
% 58.91/58.94 (P4(f6(x2071,x2072),x2072)),
% 58.91/58.94 inference(rename_variables,[],[167])).
% 58.91/58.94 cnf(208,plain,
% 58.91/58.94 (~P13(f22(f6(f30(x2081,x2082,a3),x2083),x2083))),
% 58.91/58.94 inference(scs_inference,[],[91,167,205,168,201,83,189,197,199,86,80,188,81,193,79,99,177,100,97,98,102,2,112,113,114,125,122,137,3,55,46,47,50,51,52,53,58,59,62,63,69])).
% 58.91/58.94 cnf(209,plain,
% 58.91/58.94 (E(f22(f6(x2091,x2092),x2092),x2091)),
% 58.91/58.94 inference(rename_variables,[],[83])).
% 58.91/58.94 cnf(210,plain,
% 58.91/58.94 (P15(f6(x2101,a2),a2)),
% 58.91/58.94 inference(scs_inference,[],[91,167,205,207,168,201,83,189,197,199,86,80,188,81,193,79,99,177,100,97,98,102,2,112,113,114,125,122,137,3,55,46,47,50,51,52,53,58,59,62,63,69,128])).
% 58.91/58.94 cnf(211,plain,
% 58.91/58.94 (P4(f6(x2111,x2112),x2112)),
% 58.91/58.94 inference(rename_variables,[],[167])).
% 58.91/58.94 cnf(213,plain,
% 58.91/58.94 (P19(f6(x2131,a2),a2)),
% 58.91/58.94 inference(scs_inference,[],[91,167,205,207,211,168,201,83,189,197,199,86,80,188,81,193,79,99,177,100,97,98,102,2,112,113,114,125,122,137,3,55,46,47,50,51,52,53,58,59,62,63,69,128,129])).
% 58.91/58.94 cnf(216,plain,
% 58.91/58.94 (P19(f6(f6(x2161,a2),x2162),a2)),
% 58.91/58.94 inference(scs_inference,[],[91,167,205,207,211,168,201,83,189,197,199,84,86,80,188,81,193,79,99,177,100,97,98,102,2,112,113,114,125,122,137,3,55,46,47,50,51,52,53,58,59,62,63,69,128,129,74])).
% 58.91/58.94 cnf(217,plain,
% 58.91/58.94 (E(f6(f6(x2171,x2172),x2173),f6(f6(x2171,x2173),x2172))),
% 58.91/58.94 inference(rename_variables,[],[84])).
% 58.91/58.94 cnf(218,plain,
% 58.91/58.94 (P10(f30(a8,a13,a14),x2181)+~E(a15,x2181)),
% 58.91/58.94 inference(scs_inference,[],[91,167,205,207,211,168,201,83,189,197,199,84,86,80,188,81,193,79,99,177,100,97,98,102,2,112,113,114,125,122,137,3,55,46,47,50,51,52,53,58,59,62,63,69,128,129,74,56])).
% 58.91/58.94 cnf(219,plain,
% 58.91/58.94 (P15(f6(f6(x2191,a2),x2192),a2)),
% 58.91/58.94 inference(scs_inference,[],[91,167,205,207,211,168,201,83,189,197,199,84,217,86,80,188,81,193,79,99,177,100,97,98,102,2,112,113,114,125,122,137,3,55,46,47,50,51,52,53,58,59,62,63,69,128,129,74,56,70])).
% 58.91/58.94 cnf(221,plain,
% 58.91/58.94 (~P11(f22(f6(x2211,x2212),x2212))+P11(x2211)),
% 58.91/58.94 inference(scs_inference,[],[91,167,205,207,211,168,201,83,189,197,199,209,84,217,86,80,188,81,193,79,99,177,100,97,98,102,2,112,113,114,125,122,137,3,55,46,47,50,51,52,53,58,59,62,63,69,128,129,74,56,70,57])).
% 58.91/58.94 cnf(223,plain,
% 58.91/58.94 (P8(x2231,x2232)+~E(a4,x2231)),
% 58.91/58.94 inference(scs_inference,[],[91,167,205,207,211,168,201,83,189,197,199,209,84,217,86,80,188,81,193,79,99,177,100,97,98,102,2,112,113,114,125,122,137,3,55,46,47,50,51,52,53,58,59,62,63,69,128,129,74,56,70,57,54,60])).
% 58.91/58.94 cnf(224,plain,
% 58.91/58.94 (P8(f6(f6(x2241,x2242),a2),x2243)+~E(a2,x2243)),
% 58.91/58.94 inference(scs_inference,[],[91,167,205,207,211,168,201,83,189,197,199,209,84,217,86,80,188,81,193,79,99,177,100,97,98,102,2,112,113,114,125,122,137,3,55,46,47,50,51,52,53,58,59,62,63,69,128,129,74,56,70,57,54,60,61])).
% 58.91/58.94 cnf(230,plain,
% 58.92/58.94 (P10(f30(a8,a13,a14),f22(f6(a15,x2301),x2301))),
% 58.92/58.94 inference(scs_inference,[],[169,218])).
% 58.92/58.94 cnf(231,plain,
% 58.92/58.94 (E(x2311,f22(f6(x2311,x2312),x2312))),
% 58.92/58.94 inference(rename_variables,[],[169])).
% 58.92/58.94 cnf(232,plain,
% 58.92/58.94 (P8(f22(f6(a4,x2321),x2321),x2322)),
% 58.92/58.94 inference(scs_inference,[],[169,231,218,223])).
% 58.92/58.94 cnf(233,plain,
% 58.92/58.94 (E(x2331,f22(f6(x2331,x2332),x2332))),
% 58.92/58.94 inference(rename_variables,[],[169])).
% 58.92/58.94 cnf(235,plain,
% 58.92/58.94 (E(x2351,f22(f6(x2351,x2352),x2352))),
% 58.92/58.94 inference(rename_variables,[],[169])).
% 58.92/58.94 cnf(238,plain,
% 58.92/58.94 (E(x2381,f28(f24(f22(f6(x2381,x2382),x2382),f23(x2383,x2384)),x2383))),
% 58.92/58.94 inference(scs_inference,[],[169,231,233,184,190,218,223,224,122,2])).
% 58.92/58.94 cnf(240,plain,
% 58.92/58.94 (P1(f22(f6(x2401,x2402),x2402),x2401)),
% 58.92/58.94 inference(rename_variables,[],[190])).
% 58.92/58.94 cnf(242,plain,
% 58.92/58.94 (P15(f6(f6(x2421,a2),x2422),f22(f6(a2,x2423),x2423))),
% 58.92/58.94 inference(scs_inference,[],[169,231,233,235,184,190,187,219,218,223,224,122,2,127,71])).
% 58.92/58.94 cnf(243,plain,
% 58.92/58.94 (E(x2431,f22(f6(x2431,x2432),x2432))),
% 58.92/58.94 inference(rename_variables,[],[169])).
% 58.92/58.94 cnf(244,plain,
% 58.92/58.94 (P19(f6(f6(x2441,a2),x2442),f22(f6(a2,x2443),x2443))),
% 58.92/58.94 inference(scs_inference,[],[169,231,233,235,243,184,190,187,219,216,218,223,224,122,2,127,71,75])).
% 58.92/58.94 cnf(245,plain,
% 58.92/58.94 (E(x2451,f22(f6(x2451,x2452),x2452))),
% 58.92/58.94 inference(rename_variables,[],[169])).
% 58.92/58.94 cnf(246,plain,
% 58.92/58.94 (P1(f22(f6(x2461,x2462),x2462),f22(f6(x2461,x2463),x2463))),
% 58.92/58.94 inference(scs_inference,[],[169,231,233,235,243,245,184,190,240,187,219,216,218,223,224,122,2,127,71,75,47])).
% 58.92/58.94 cnf(247,plain,
% 58.92/58.94 (P1(f22(f6(x2471,x2472),x2472),x2471)),
% 58.92/58.94 inference(rename_variables,[],[190])).
% 58.92/58.94 cnf(248,plain,
% 58.92/58.94 (P1(f22(f6(f22(f6(x2481,x2482),x2482),x2483),x2483),x2481)),
% 58.92/58.94 inference(scs_inference,[],[169,231,233,235,243,245,184,190,240,247,187,219,216,218,223,224,122,2,127,71,75,47,46])).
% 58.92/58.94 cnf(249,plain,
% 58.92/58.94 (E(x2491,f22(f6(x2491,x2492),x2492))),
% 58.92/58.94 inference(rename_variables,[],[169])).
% 58.92/58.94 cnf(251,plain,
% 58.92/58.94 (E(x2511,f22(f6(x2511,x2512),x2512))),
% 58.92/58.94 inference(rename_variables,[],[169])).
% 58.92/58.94 cnf(252,plain,
% 58.92/58.94 (P2(f22(f6(f6(x2521,x2522),x2523),x2523))),
% 58.92/58.94 inference(scs_inference,[],[169,231,233,235,243,245,249,251,184,186,190,240,247,187,219,216,82,218,223,224,122,2,127,71,75,47,46,55,52])).
% 58.92/58.94 cnf(253,plain,
% 58.92/58.94 (E(x2531,f22(f6(x2531,x2532),x2532))),
% 58.92/58.94 inference(rename_variables,[],[169])).
% 58.92/58.94 cnf(254,plain,
% 58.92/58.94 (P6(f24(x2541,f23(f22(f6(x2542,x2543),x2543),x2544)),f22(f6(x2542,x2545),x2545))),
% 58.92/58.94 inference(scs_inference,[],[169,231,233,235,243,245,249,251,253,184,186,190,240,247,202,187,219,216,82,218,223,224,122,2,127,71,75,47,46,55,52,59])).
% 58.92/58.94 cnf(259,plain,
% 58.92/58.94 (P7(f22(f6(f24(x2591,f23(x2592,x2593)),x2594),x2594))),
% 58.92/58.94 inference(scs_inference,[],[169,231,233,235,243,245,249,251,253,184,186,190,240,247,202,187,219,92,216,82,85,102,218,223,224,122,2,127,71,75,47,46,55,52,59,69,53])).
% 58.92/58.94 cnf(260,plain,
% 58.92/58.94 (E(x2601,f22(f6(x2601,x2602),x2602))),
% 58.92/58.94 inference(rename_variables,[],[169])).
% 58.92/58.94 cnf(261,plain,
% 58.92/58.94 (P8(x2611,f22(f6(a2,x2612),x2612))),
% 58.92/58.94 inference(scs_inference,[],[169,231,233,235,243,245,249,251,253,260,184,186,190,240,247,202,187,219,92,181,216,82,85,102,218,223,224,122,2,127,71,75,47,46,55,52,59,69,53,61])).
% 58.92/58.94 cnf(262,plain,
% 58.92/58.94 (E(x2621,f22(f6(x2621,x2622),x2622))),
% 58.92/58.94 inference(rename_variables,[],[169])).
% 58.92/58.94 cnf(263,plain,
% 58.92/58.94 (P9(x2631,f22(f6(f22(f6(x2631,x2632),x2632),x2633),x2633))),
% 58.92/58.94 inference(scs_inference,[],[169,231,233,235,243,245,249,251,253,260,262,184,186,190,240,247,192,202,187,219,92,181,216,82,85,102,218,223,224,122,2,127,71,75,47,46,55,52,59,69,53,61,51])).
% 58.92/58.94 cnf(264,plain,
% 58.92/58.94 (E(x2641,f22(f6(x2641,x2642),x2642))),
% 58.92/58.94 inference(rename_variables,[],[169])).
% 58.92/58.94 cnf(265,plain,
% 58.92/58.94 (P8(f22(f6(f22(f6(a4,x2651),x2651),x2652),x2652),x2653)),
% 58.92/58.94 inference(scs_inference,[],[169,231,233,235,243,245,249,251,253,260,262,264,184,186,190,240,247,192,202,187,219,92,181,216,82,85,102,218,223,224,122,2,127,71,75,47,46,55,52,59,69,53,61,51,60])).
% 58.92/58.95 cnf(266,plain,
% 58.92/58.95 (E(x2661,f22(f6(x2661,x2662),x2662))),
% 58.92/58.95 inference(rename_variables,[],[169])).
% 58.92/58.95 cnf(267,plain,
% 58.92/58.95 (P3(f22(f6(f30(x2671,a1,x2672),x2673),x2673))),
% 58.92/58.95 inference(scs_inference,[],[169,231,233,235,243,245,249,251,253,260,262,264,266,184,186,190,240,247,192,202,187,219,92,181,216,82,90,85,102,218,223,224,122,2,127,71,75,47,46,55,52,59,69,53,61,51,60,54])).
% 58.92/58.95 cnf(268,plain,
% 58.92/58.95 (E(x2681,f22(f6(x2681,x2682),x2682))),
% 58.92/58.95 inference(rename_variables,[],[169])).
% 58.92/58.95 cnf(269,plain,
% 58.92/58.95 (P11(f22(f6(f27(f30(a8,a13,a14),a15),x2691),x2691))),
% 58.92/58.95 inference(scs_inference,[],[94,169,231,233,235,243,245,249,251,253,260,262,264,266,268,184,186,190,240,247,192,202,187,219,92,181,216,82,90,85,102,218,223,224,122,2,127,71,75,47,46,55,52,59,69,53,61,51,60,54,57])).
% 58.92/58.95 cnf(270,plain,
% 58.92/58.95 (E(x2701,f22(f6(x2701,x2702),x2702))),
% 58.92/58.95 inference(rename_variables,[],[169])).
% 58.92/58.95 cnf(271,plain,
% 58.92/58.95 (E(f28(f24(f22(f6(x2711,x2712),x2712),f23(x2713,x2714)),x2713),f22(f6(x2711,x2715),x2715))),
% 58.92/58.95 inference(scs_inference,[],[94,169,231,233,235,243,245,249,251,253,260,262,264,266,268,270,184,186,190,240,247,192,202,187,219,92,181,216,82,90,85,102,218,223,224,122,2,127,71,75,47,46,55,52,59,69,53,61,51,60,54,57,3])).
% 58.92/58.95 cnf(272,plain,
% 58.92/58.95 (E(x2721,f22(f6(x2721,x2722),x2722))),
% 58.92/58.95 inference(rename_variables,[],[169])).
% 58.92/58.95 cnf(273,plain,
% 58.92/58.95 (P9(f22(f6(x2731,x2732),x2732),f22(f6(x2731,x2733),x2733))),
% 58.92/58.95 inference(scs_inference,[],[94,169,231,233,235,243,245,249,251,253,260,262,264,266,268,270,272,184,186,190,240,247,192,202,187,219,92,181,216,82,90,85,102,218,223,224,122,2,127,71,75,47,46,55,52,59,69,53,61,51,60,54,57,3,50])).
% 58.92/58.95 cnf(275,plain,
% 58.92/58.95 (P4(f6(x2751,f22(f6(x2752,x2753),x2753)),f22(f6(x2752,x2754),x2754))),
% 58.92/58.95 inference(scs_inference,[],[94,169,231,233,235,243,245,249,251,253,260,262,264,266,268,270,272,184,186,190,240,247,192,206,202,187,219,92,181,216,82,90,85,102,218,223,224,122,2,127,71,75,47,46,55,52,59,69,53,61,51,60,54,57,3,50,63])).
% 58.92/58.95 cnf(278,plain,
% 58.92/58.95 (E(x2781,f22(f6(x2781,x2782),x2782))),
% 58.92/58.95 inference(rename_variables,[],[169])).
% 58.92/58.95 cnf(286,plain,
% 58.92/58.95 (E(f22(f6(x2861,x2862),x2862),x2861)),
% 58.92/58.95 inference(rename_variables,[],[83])).
% 58.92/58.95 cnf(290,plain,
% 58.92/58.95 (~P4(f22(f6(a4,x2901),x2901),x2902)),
% 58.92/58.95 inference(scs_inference,[],[94,169,231,233,235,243,245,249,251,253,260,262,264,266,268,270,272,278,184,186,190,240,247,192,206,202,187,172,174,219,92,83,286,181,216,82,90,85,102,99,218,223,224,122,2,127,71,75,47,46,55,52,59,69,53,61,51,60,54,57,3,50,63,56,138,128,70,129,74])).
% 58.92/58.95 cnf(297,plain,
% 58.92/58.95 (P8(f28(f24(f22(f6(a4,x2971),x2971),f23(x2972,x2973)),x2972),x2974)),
% 58.92/58.95 inference(scs_inference,[],[238,290,112,113,114,223])).
% 58.92/58.95 cnf(298,plain,
% 58.92/58.95 (E(x2981,f28(f24(f22(f6(x2981,x2982),x2982),f23(x2983,x2984)),x2983))),
% 58.92/58.95 inference(rename_variables,[],[238])).
% 58.92/58.95 cnf(300,plain,
% 58.92/58.95 (E(x3001,f28(f24(f22(f6(x3001,x3002),x3002),f23(x3003,x3004)),x3003))),
% 58.92/58.95 inference(rename_variables,[],[238])).
% 58.92/58.95 cnf(301,plain,
% 58.92/58.95 (P10(f30(a8,a13,a14),f28(f24(f22(f6(a15,x3011),x3011),f23(x3012,x3013)),x3012))),
% 58.92/58.95 inference(scs_inference,[],[238,298,300,290,112,113,114,223,224,218])).
% 58.92/58.95 cnf(302,plain,
% 58.92/58.95 (E(x3021,f28(f24(f22(f6(x3021,x3022),x3022),f23(x3023,x3024)),x3023))),
% 58.92/58.95 inference(rename_variables,[],[238])).
% 58.92/58.95 cnf(305,plain,
% 58.92/58.95 (E(f22(f6(x3051,x3052),x3052),f28(f24(f22(f6(x3051,x3053),x3053),f23(x3054,x3055)),x3054))),
% 58.92/58.95 inference(scs_inference,[],[271,238,298,300,187,290,112,113,114,223,224,218,122,2])).
% 58.92/58.95 cnf(306,plain,
% 58.92/58.95 (E(f22(f6(x3061,x3062),x3062),f22(f6(x3061,x3063),x3063))),
% 58.92/58.95 inference(scs_inference,[],[271,238,298,300,187,254,290,100,112,113,114,223,224,218,122,2,148])).
% 58.92/58.95 cnf(310,plain,
% 58.92/58.95 (P1(f22(f6(a2,x3101),x3101),x3102)),
% 58.92/58.95 inference(scs_inference,[],[271,238,298,300,167,187,254,261,290,100,112,113,114,223,224,218,122,2,148,126])).
% 58.92/58.95 cnf(311,plain,
% 58.92/58.95 (P8(x3111,f22(f6(a2,x3112),x3112))),
% 58.92/58.95 inference(rename_variables,[],[261])).
% 58.92/58.95 cnf(313,plain,
% 58.92/58.95 (P1(f22(f6(f22(f6(a2,x3131),x3131),x3132),x3132),x3133)),
% 58.92/58.95 inference(scs_inference,[],[271,238,298,300,167,187,254,248,261,79,290,100,112,113,114,223,224,218,122,2,148,126,127])).
% 58.92/58.95 cnf(314,plain,
% 58.92/58.95 (P1(f22(f6(f22(f6(x3141,x3142),x3142),x3143),x3143),x3141)),
% 58.92/58.95 inference(rename_variables,[],[248])).
% 58.92/58.95 cnf(317,plain,
% 58.92/58.95 (P4(f6(x3171,x3172),x3172)),
% 58.92/58.95 inference(rename_variables,[],[167])).
% 58.92/58.95 cnf(318,plain,
% 58.92/58.95 (P15(f6(f6(x3181,a2),x3182),f28(f24(f22(f6(a2,x3183),x3183),f23(x3184,x3185)),x3184))),
% 58.92/58.95 inference(scs_inference,[],[271,238,298,300,302,167,219,187,254,248,261,79,290,100,112,113,114,223,224,218,122,2,148,126,127,62,71])).
% 58.92/58.95 cnf(319,plain,
% 58.92/58.95 (E(x3191,f28(f24(f22(f6(x3191,x3192),x3192),f23(x3193,x3194)),x3193))),
% 58.92/58.95 inference(rename_variables,[],[238])).
% 58.92/58.95 cnf(320,plain,
% 58.92/58.95 (P1(f28(f24(f22(f6(f30(a8,a13,a14),x3201),x3201),f23(x3202,x3203)),x3202),f22(f6(f30(a8,a13,a14),x3204),x3204))),
% 58.92/58.95 inference(scs_inference,[],[271,238,298,300,302,319,167,219,187,254,248,261,79,290,100,112,113,114,223,224,218,122,2,148,126,127,62,71,46])).
% 58.92/58.95 cnf(321,plain,
% 58.92/58.95 (E(x3211,f28(f24(f22(f6(x3211,x3212),x3212),f23(x3213,x3214)),x3213))),
% 58.92/58.95 inference(rename_variables,[],[238])).
% 58.92/58.95 cnf(322,plain,
% 58.92/58.95 (P1(f22(f6(x3221,x3222),x3222),f28(f24(f22(f6(f22(f6(x3221,x3223),x3223),x3224),x3224),f23(x3225,x3226)),x3225))),
% 58.92/58.95 inference(scs_inference,[],[271,238,298,300,302,319,321,167,219,187,246,254,248,261,79,290,100,112,113,114,223,224,218,122,2,148,126,127,62,71,46,47])).
% 58.92/58.95 cnf(323,plain,
% 58.92/58.95 (E(x3231,f28(f24(f22(f6(x3231,x3232),x3232),f23(x3233,x3234)),x3233))),
% 58.92/58.95 inference(rename_variables,[],[238])).
% 58.92/58.95 cnf(325,plain,
% 58.92/58.95 (E(x3251,f28(f24(f22(f6(x3251,x3252),x3252),f23(x3253,x3254)),x3253))),
% 58.92/58.95 inference(rename_variables,[],[238])).
% 58.92/58.95 cnf(326,plain,
% 58.92/58.95 (P19(f6(x3261,a2),f28(f24(f22(f6(a2,x3262),x3262),f23(x3263,x3264)),x3263))),
% 58.92/58.95 inference(scs_inference,[],[91,271,238,298,300,302,319,321,323,325,167,219,187,246,254,248,261,213,79,290,100,112,113,114,223,224,218,122,2,148,126,127,62,71,46,47,55,75])).
% 58.92/58.95 cnf(327,plain,
% 58.92/58.95 (E(x3271,f28(f24(f22(f6(x3271,x3272),x3272),f23(x3273,x3274)),x3273))),
% 58.92/58.95 inference(rename_variables,[],[238])).
% 58.92/58.95 cnf(328,plain,
% 58.92/58.95 (~P13(f28(f24(f22(f6(f30(x3281,x3282,a3),x3283),x3283),f23(x3284,x3285)),x3284))),
% 58.92/58.95 inference(scs_inference,[],[91,271,238,298,300,302,319,321,323,325,167,219,187,246,254,248,208,261,213,79,290,100,112,113,114,223,224,218,122,2,148,126,127,62,71,46,47,55,75,69])).
% 58.92/58.95 cnf(329,plain,
% 58.92/58.95 (E(f28(f24(f22(f6(x3291,x3292),x3292),f23(x3293,x3294)),x3293),f22(f6(x3291,x3295),x3295))),
% 58.92/58.95 inference(rename_variables,[],[271])).
% 58.92/58.95 cnf(331,plain,
% 58.92/58.95 (E(f28(f24(f22(f6(x3311,x3312),x3312),f23(x3313,x3314)),x3313),f22(f6(x3311,x3315),x3315))),
% 58.92/58.95 inference(rename_variables,[],[271])).
% 58.92/58.95 cnf(333,plain,
% 58.92/58.95 (E(x3331,f28(f24(f22(f6(x3331,x3332),x3332),f23(x3333,x3334)),x3333))),
% 58.92/58.95 inference(rename_variables,[],[238])).
% 58.92/58.95 cnf(335,plain,
% 58.92/58.95 (E(f28(f24(f22(f6(x3351,x3352),x3352),f23(x3353,x3354)),x3353),f22(f6(x3351,x3355),x3355))),
% 58.92/58.95 inference(rename_variables,[],[271])).
% 58.92/58.95 cnf(337,plain,
% 58.92/58.95 (E(x3371,f28(f24(f22(f6(x3371,x3372),x3372),f23(x3373,x3374)),x3373))),
% 58.92/58.95 inference(rename_variables,[],[238])).
% 58.92/58.95 cnf(339,plain,
% 58.92/58.95 (E(x3391,f28(f24(f22(f6(x3391,x3392),x3392),f23(x3393,x3394)),x3393))),
% 58.92/58.95 inference(rename_variables,[],[238])).
% 58.92/58.95 cnf(340,plain,
% 58.92/58.95 (P8(x3401,f28(f24(f22(f6(f22(f6(a2,x3402),x3402),x3403),x3403),f23(x3404,x3405)),x3404))),
% 58.92/58.95 inference(scs_inference,[],[91,94,271,329,331,238,298,300,302,319,321,323,325,327,333,337,339,167,219,187,246,273,254,248,208,232,261,311,196,198,213,79,290,100,112,113,114,223,224,218,122,2,148,126,127,62,71,46,47,55,75,69,53,51,52,60,57,61])).
% 58.92/58.95 cnf(341,plain,
% 58.92/58.95 (E(x3411,f28(f24(f22(f6(x3411,x3412),x3412),f23(x3413,x3414)),x3413))),
% 58.92/58.95 inference(rename_variables,[],[238])).
% 58.92/58.95 cnf(342,plain,
% 58.92/58.95 (~E(f6(x3421,x3422),f28(f24(f22(f6(a4,x3423),x3423),f23(x3424,x3425)),x3424))),
% 58.92/58.95 inference(scs_inference,[],[91,94,271,329,331,335,238,298,300,302,319,321,323,325,327,333,337,339,167,219,187,246,273,254,248,208,232,261,311,196,198,213,79,290,100,112,113,114,223,224,218,122,2,148,126,127,62,71,46,47,55,75,69,53,51,52,60,57,61,3])).
% 58.92/58.95 cnf(343,plain,
% 58.92/58.95 (E(f28(f24(f22(f6(x3431,x3432),x3432),f23(x3433,x3434)),x3433),f22(f6(x3431,x3435),x3435))),
% 58.92/58.95 inference(rename_variables,[],[271])).
% 58.92/58.95 cnf(346,plain,
% 58.92/58.95 (P9(f28(f24(f22(f6(f22(f6(x3461,x3462),x3462),x3463),x3463),f23(x3464,x3465)),x3464),x3461)),
% 58.92/58.95 inference(scs_inference,[],[91,94,271,329,331,335,238,298,300,302,319,321,323,325,327,333,337,339,341,169,167,219,187,194,246,273,254,248,208,267,232,261,311,196,198,213,79,290,100,112,113,114,223,224,218,122,2,148,126,127,62,71,46,47,55,75,69,53,51,52,60,57,61,3,54,50])).
% 58.92/58.95 cnf(347,plain,
% 58.92/58.95 (E(x3471,f28(f24(f22(f6(x3471,x3472),x3472),f23(x3473,x3474)),x3473))),
% 58.92/58.95 inference(rename_variables,[],[238])).
% 58.92/58.95 cnf(348,plain,
% 58.92/58.95 (P4(f6(x3481,f28(f24(f22(f6(x3482,x3483),x3483),f23(x3484,x3485)),x3484)),f22(f6(x3482,x3486),x3486))),
% 58.92/58.95 inference(scs_inference,[],[91,94,271,329,331,335,343,238,298,300,302,319,321,323,325,327,333,337,339,341,169,167,317,219,187,194,246,273,254,248,208,267,232,261,311,196,198,213,79,290,100,112,113,114,223,224,218,122,2,148,126,127,62,71,46,47,55,75,69,53,51,52,60,57,61,3,54,50,63])).
% 58.92/58.95 cnf(360,plain,
% 58.92/58.95 (~P4(f22(f6(f22(f6(a4,x3601),x3601),x3602),x3602),x3603)+~E(f22(f6(f22(f6(a4,x3601),x3601),x3602),x3602),a4)),
% 58.92/58.95 inference(scs_inference,[],[91,94,271,329,331,335,343,238,298,300,302,319,321,323,325,327,333,337,339,341,347,230,169,167,317,219,187,194,246,273,254,248,314,265,208,267,232,261,311,196,198,172,213,79,290,100,112,113,114,223,224,218,122,2,148,126,127,62,71,46,47,55,75,69,53,51,52,60,57,61,3,54,50,63,56,76,128,77,129,124,70])).
% 58.92/58.95 cnf(363,plain,
% 58.92/58.95 (E(a1,f5(a1,x3631))),
% 58.92/58.95 inference(scs_inference,[],[246,78,122,2])).
% 58.92/58.95 cnf(364,plain,
% 58.92/58.95 (P1(f28(f24(f22(f6(f22(f6(a2,x3641),x3641),x3642),x3642),f23(x3643,x3644)),x3643),x3645)),
% 58.92/58.95 inference(scs_inference,[],[167,246,340,78,122,2,126])).
% 58.92/58.95 cnf(367,plain,
% 58.92/58.95 (P1(f28(f24(f22(f6(a2,x3671),x3671),f23(x3672,x3673)),x3672),x3674)),
% 58.92/58.95 inference(scs_inference,[],[238,167,246,340,78,79,122,2,126,46])).
% 58.92/58.95 cnf(368,plain,
% 58.92/58.95 (E(x3681,f28(f24(f22(f6(x3681,x3682),x3682),f23(x3683,x3684)),x3683))),
% 58.92/58.95 inference(rename_variables,[],[238])).
% 58.92/58.95 cnf(370,plain,
% 58.92/58.95 (E(x3701,f28(f24(f22(f6(x3701,x3702),x3702),f23(x3703,x3704)),x3703))),
% 58.92/58.95 inference(rename_variables,[],[238])).
% 58.92/58.95 cnf(371,plain,
% 58.92/58.95 (P1(f22(f6(f22(f6(x3711,x3712),x3712),x3713),x3713),f22(f6(x3711,x3714),x3714))),
% 58.92/58.95 inference(scs_inference,[],[306,238,368,167,246,190,340,78,216,79,122,2,126,46,75,47])).
% 58.92/58.95 cnf(373,plain,
% 58.92/58.95 (P15(f6(x3731,a2),f28(f24(f22(f6(a2,x3732),x3732),f23(x3733,x3734)),x3733))),
% 58.92/58.95 inference(scs_inference,[],[306,238,368,370,167,246,190,340,78,210,216,79,122,2,126,46,75,47,71])).
% 58.92/58.95 cnf(374,plain,
% 58.92/58.95 (E(x3741,f28(f24(f22(f6(x3741,x3742),x3742),f23(x3743,x3744)),x3743))),
% 58.92/58.95 inference(rename_variables,[],[238])).
% 58.92/58.95 cnf(376,plain,
% 58.92/58.95 (E(x3761,f28(f24(f22(f6(x3761,x3762),x3762),f23(x3763,x3764)),x3763))),
% 58.92/58.95 inference(rename_variables,[],[238])).
% 58.92/58.95 cnf(381,plain,
% 58.92/58.95 (~E(f24(x3811,f23(x3812,x3813)),f5(a1,x3814))),
% 58.92/58.95 inference(scs_inference,[],[306,301,238,368,370,374,167,246,190,340,328,200,78,194,86,210,216,79,122,2,126,46,75,47,71,55,69,51,3])).
% 58.92/58.95 cnf(382,plain,
% 58.92/58.95 (P2(f28(f24(f22(f6(f6(x3821,x3822),x3823),x3823),f23(x3824,x3825)),x3824))),
% 58.92/58.95 inference(scs_inference,[],[306,305,301,238,368,370,374,167,246,190,252,340,328,200,78,194,86,210,216,79,122,2,126,46,75,47,71,55,69,51,3,52])).
% 58.92/58.95 cnf(383,plain,
% 58.92/58.95 (E(f22(f6(x3831,x3832),x3832),f28(f24(f22(f6(x3831,x3833),x3833),f23(x3834,x3835)),x3834))),
% 58.92/58.95 inference(rename_variables,[],[305])).
% 58.92/58.95 cnf(384,plain,
% 58.92/58.95 (P7(f28(f24(f22(f6(f24(x3841,f23(x3842,x3843)),x3844),x3844),f23(x3845,x3846)),x3845))),
% 58.92/58.95 inference(scs_inference,[],[306,305,383,301,238,368,370,374,167,246,190,252,259,340,328,200,78,194,86,210,216,79,122,2,126,46,75,47,71,55,69,51,3,52,53])).
% 58.92/58.95 cnf(386,plain,
% 58.92/58.95 (P8(x3861,f28(f24(f22(f6(a2,x3862),x3862),f23(x3863,x3864)),x3863))),
% 58.92/58.95 inference(scs_inference,[],[306,305,383,301,238,368,370,374,376,167,246,190,252,259,340,328,200,78,194,86,210,216,79,181,122,2,126,46,75,47,71,55,69,51,3,52,53,61])).
% 58.92/58.95 cnf(402,plain,
% 58.92/58.95 (E(x4021,f26(f24(x4022,f23(x4023,x4021)),x4023))),
% 58.92/58.95 inference(scs_inference,[],[248,87,122,2])).
% 58.92/58.95 cnf(403,plain,
% 58.92/58.95 (P6(f24(x4031,f23(x4032,x4033)),f22(f6(x4032,x4034),x4034))),
% 58.92/58.95 inference(scs_inference,[],[169,168,248,87,122,2,59])).
% 58.92/58.95 cnf(405,plain,
% 58.92/58.95 (P15(f6(x4051,a2),f22(f6(a2,x4052),x4052))),
% 58.92/58.95 inference(scs_inference,[],[169,168,248,87,210,122,2,59,71])).
% 58.92/58.95 cnf(406,plain,
% 58.92/58.95 (E(x4061,f22(f6(x4061,x4062),x4062))),
% 58.92/58.95 inference(rename_variables,[],[169])).
% 58.92/58.95 cnf(407,plain,
% 58.92/58.95 (E(f28(f24(f22(f6(f7(f30(x4071,a1,x4072)),x4073),x4073),f23(x4074,x4075)),x4074),a2)),
% 58.92/58.95 inference(scs_inference,[],[169,184,168,248,87,88,210,122,2,59,71,3])).
% 58.92/58.95 cnf(409,plain,
% 58.92/58.95 (P9(f28(f24(f22(f6(f22(f6(x4091,x4092),x4092),x4093),x4093),f23(x4094,x4095)),x4094),f22(f6(x4091,x4096),x4096))),
% 58.92/58.95 inference(scs_inference,[],[169,406,184,168,248,346,87,88,210,122,2,59,71,3,51])).
% 58.92/58.95 cnf(411,plain,
% 58.92/58.95 (P19(f6(x4111,a2),f22(f6(a2,x4112),x4112))),
% 58.92/58.95 inference(scs_inference,[],[169,406,184,168,248,346,87,88,213,210,122,2,59,71,3,51,75])).
% 58.92/58.95 cnf(412,plain,
% 58.92/58.95 (E(x4121,f22(f6(x4121,x4122),x4122))),
% 58.92/58.95 inference(rename_variables,[],[169])).
% 58.92/58.95 cnf(414,plain,
% 58.92/58.95 (E(x4141,f22(f6(x4141,x4142),x4142))),
% 58.92/58.95 inference(rename_variables,[],[169])).
% 58.92/58.95 cnf(415,plain,
% 58.92/58.95 (P4(f6(x4151,x4152),f22(f6(x4152,x4153),x4153))),
% 58.92/58.95 inference(scs_inference,[],[169,406,412,414,184,168,167,187,248,346,87,88,213,210,122,2,59,71,3,51,75,47,63])).
% 58.92/58.95 cnf(417,plain,
% 58.92/58.95 (~P7(f5(a1,x4171))),
% 58.92/58.95 inference(scs_inference,[],[169,406,412,414,184,168,167,187,248,346,87,88,78,213,210,98,122,2,59,71,3,51,75,47,63,53])).
% 58.92/58.95 cnf(418,plain,
% 58.92/58.95 (~P2(f17(f30(x4181,a1,x4182)))),
% 58.92/58.95 inference(scs_inference,[],[169,406,412,414,184,168,167,187,248,346,87,88,89,78,213,210,97,98,122,2,59,71,3,51,75,47,63,53,52])).
% 58.92/58.95 cnf(420,plain,
% 58.92/58.95 (E(x4201,f22(f6(x4201,x4202),x4202))),
% 58.92/58.95 inference(rename_variables,[],[169])).
% 58.92/58.95 cnf(421,plain,
% 58.92/58.95 (P9(f22(f6(f22(f6(x4211,x4212),x4212),x4213),x4213),x4211)),
% 58.92/58.95 inference(scs_inference,[],[169,406,412,414,420,184,168,167,187,261,248,346,87,88,89,194,78,213,210,97,98,122,2,59,71,3,51,75,47,63,53,52,61,50])).
% 58.92/58.95 cnf(436,plain,
% 58.92/58.95 (P8(f26(f24(x4361,f23(x4362,a4)),x4362),x4363)),
% 58.92/58.95 inference(scs_inference,[],[402,223])).
% 58.92/58.95 cnf(437,plain,
% 58.92/58.95 (E(x4371,f26(f24(x4372,f23(x4373,x4371)),x4373))),
% 58.92/58.95 inference(rename_variables,[],[402])).
% 58.92/58.95 cnf(438,plain,
% 58.92/58.95 (P8(f6(f6(x4381,x4382),a2),f26(f24(x4383,f23(x4384,a2)),x4384))),
% 58.92/58.95 inference(scs_inference,[],[402,437,223,224])).
% 58.92/58.95 cnf(439,plain,
% 58.92/58.95 (E(x4391,f26(f24(x4392,f23(x4393,x4391)),x4393))),
% 58.92/58.95 inference(rename_variables,[],[402])).
% 58.92/58.95 cnf(440,plain,
% 58.92/58.95 (P10(f30(a8,a13,a14),f26(f24(x4401,f23(x4402,a15)),x4402))),
% 58.92/58.95 inference(scs_inference,[],[402,437,439,223,224,218])).
% 58.92/58.95 cnf(441,plain,
% 58.92/58.95 (E(x4411,f26(f24(x4412,f23(x4413,x4411)),x4413))),
% 58.92/58.95 inference(rename_variables,[],[402])).
% 58.92/58.95 cnf(444,plain,
% 58.92/58.95 (E(a2,f28(f24(f22(f6(f7(f30(x4441,a1,x4442)),x4443),x4443),f23(x4444,x4445)),x4444))),
% 58.92/58.95 inference(scs_inference,[],[402,437,439,407,371,223,224,218,122,2])).
% 58.92/58.95 cnf(446,plain,
% 58.92/58.95 (E(x4461,f22(f6(x4461,x4462),x4462))),
% 58.92/58.95 inference(rename_variables,[],[169])).
% 58.92/58.95 cnf(448,plain,
% 58.92/58.95 (E(x4481,f22(f6(x4481,x4482),x4482))),
% 58.92/58.95 inference(rename_variables,[],[169])).
% 58.92/58.95 cnf(450,plain,
% 58.92/58.95 (E(x4501,f22(f6(x4501,x4502),x4502))),
% 58.92/58.95 inference(rename_variables,[],[169])).
% 58.92/58.95 cnf(452,plain,
% 58.92/58.95 (E(x4521,f22(f6(x4521,x4522),x4522))),
% 58.92/58.95 inference(rename_variables,[],[169])).
% 58.92/58.95 cnf(453,plain,
% 58.92/58.95 (E(x4531,f26(f24(x4532,f23(x4533,f22(f6(x4531,x4534),x4534))),x4533))),
% 58.92/58.95 inference(scs_inference,[],[169,446,448,450,452,402,437,439,441,407,275,371,403,244,242,223,224,218,122,2,59,71,63,75,3])).
% 58.92/58.95 cnf(455,plain,
% 58.92/58.95 (P8(f22(f6(f26(f24(x4551,f23(x4552,a4)),x4552),x4553),x4553),x4554)),
% 58.92/58.95 inference(scs_inference,[],[169,446,448,450,452,402,437,439,441,407,275,371,403,244,242,223,224,218,122,2,59,71,63,75,3,60])).
% 58.92/58.95 cnf(456,plain,
% 58.92/58.95 (E(x4561,f22(f6(x4561,x4562),x4562))),
% 58.92/58.95 inference(rename_variables,[],[169])).
% 58.92/58.95 cnf(457,plain,
% 58.92/58.95 (P1(f22(f6(x4571,x4572),x4572),f22(f6(f22(f6(x4571,x4573),x4573),x4574),x4574))),
% 58.92/58.95 inference(scs_inference,[],[169,446,448,450,452,456,402,437,439,441,407,275,246,371,403,244,242,223,224,218,122,2,59,71,63,75,3,60,47])).
% 58.92/58.95 cnf(458,plain,
% 58.92/58.95 (E(x4581,f22(f6(x4581,x4582),x4582))),
% 58.92/58.95 inference(rename_variables,[],[169])).
% 58.92/58.95 cnf(460,plain,
% 58.92/58.95 (E(x4601,f22(f6(x4601,x4602),x4602))),
% 58.92/58.95 inference(rename_variables,[],[169])).
% 58.92/58.95 cnf(461,plain,
% 58.92/58.95 (P10(f30(a8,a13,a14),f22(f6(f22(f6(a15,x4611),x4611),x4612),x4612))),
% 58.92/58.95 inference(scs_inference,[],[169,446,448,450,452,456,458,460,230,402,437,439,441,407,275,246,371,403,244,242,223,224,218,122,2,59,71,63,75,3,60,47,55,56])).
% 58.92/58.95 cnf(463,plain,
% 58.92/58.95 (E(x4631,f22(f6(f22(f6(x4631,x4632),x4632),x4633),x4633))),
% 58.92/58.95 inference(scs_inference,[],[169,446,448,450,452,456,458,460,230,402,437,439,441,407,275,246,371,403,244,242,100,223,224,218,122,2,59,71,63,75,3,60,47,55,56,148])).
% 58.92/58.95 cnf(466,plain,
% 58.92/58.95 (E(f22(f6(x4661,x4662),x4662),f22(f6(f22(f6(x4661,x4663),x4663),x4664),x4664))),
% 58.92/58.95 inference(scs_inference,[],[169,446,448,450,452,456,458,460,230,402,437,439,441,407,275,246,371,403,290,244,242,100,223,224,218,122,2,59,71,63,75,3,60,47,55,56,148,138])).
% 58.92/58.95 cnf(484,plain,
% 58.92/58.95 (E(x4841,f26(f24(x4842,f23(x4843,f22(f6(x4841,x4844),x4844))),x4843))),
% 58.92/58.95 inference(rename_variables,[],[453])).
% 58.92/58.95 cnf(485,plain,
% 58.92/58.95 (P8(f6(f6(x4851,x4852),a2),f28(f24(f22(f6(f7(f30(x4853,a1,x4854)),x4855),x4855),f23(x4856,x4857)),x4856))),
% 58.92/58.95 inference(scs_inference,[],[453,444,223,224])).
% 58.92/58.95 cnf(490,plain,
% 58.92/58.95 (E(f22(f6(f22(f6(x4901,x4902),x4902),x4903),x4903),x4901)),
% 58.92/58.95 inference(scs_inference,[],[463,453,484,444,367,223,224,122,218,2])).
% 58.92/58.95 cnf(493,plain,
% 58.92/58.95 (P3(f28(f24(f22(f6(f30(x4931,a1,x4932),x4933),x4933),f23(x4934,x4935)),x4934))),
% 58.92/58.95 inference(scs_inference,[],[305,463,453,484,342,444,86,367,267,223,224,122,218,2,3,54])).
% 58.92/58.95 cnf(499,plain,
% 58.92/58.95 (~P4(f22(f6(f22(f6(a4,x4991),x4991),x4992),x4992),x4993)),
% 58.92/58.95 inference(scs_inference,[],[238,305,230,463,466,453,484,342,444,86,367,267,252,223,224,122,218,2,3,54,55,52,360])).
% 58.92/58.95 cnf(501,plain,
% 58.92/58.95 (~P15(f22(f6(f22(f6(a4,x5011),x5011),x5012),x5012),x5013)),
% 58.92/58.95 inference(scs_inference,[],[238,305,230,463,466,453,484,342,444,86,367,267,252,223,224,122,218,2,3,54,55,52,360,113])).
% 58.92/58.95 cnf(528,plain,
% 58.92/58.95 (E(f22(f6(f22(f6(x5281,x5282),x5282),x5283),x5283),f22(f6(x5281,x5284),x5284))),
% 58.92/58.95 inference(scs_inference,[],[466,457,122,2])).
% 58.92/58.95 cnf(534,plain,
% 58.92/58.95 (E(f28(f24(f22(f6(f16(f30(x5341,a1,x5342)),x5343),x5343),f23(x5344,x5345)),x5344),f30(x5341,a1,a3))),
% 58.92/58.95 inference(scs_inference,[],[169,184,466,219,457,92,501,438,198,122,2,70,60,53,3])).
% 58.92/58.95 cnf(590,plain,
% 58.92/58.95 (P3(f28(f24(f22(f6(f16(f30(x5901,a1,x5902)),x5903),x5903),f23(x5904,x5905)),x5904))),
% 58.92/58.95 inference(scs_inference,[],[534,322,90,122,2,54])).
% 58.92/58.95 cnf(619,plain,
% 58.92/58.95 (E(x6191,f28(f24(x6191,f23(x6192,x6193)),x6192))),
% 58.92/58.95 inference(scs_inference,[],[86,320,122,2])).
% 58.92/58.95 cnf(623,plain,
% 58.92/58.95 (~E(f6(x6231,x6232),f17(f30(x6233,a1,x6234)))),
% 58.92/58.95 inference(scs_inference,[],[271,86,320,89,382,590,204,122,2,52,54,3])).
% 58.92/58.95 cnf(628,plain,
% 58.92/58.95 (~P13(x6281)+P13(f26(f24(x6282,f23(x6283,x6281)),x6283))),
% 58.92/58.95 inference(scs_inference,[],[402,271,86,320,455,89,485,382,590,204,122,2,52,54,3,128,129,69])).
% 58.92/58.95 cnf(632,plain,
% 58.92/58.95 (P8(f6(f6(x6321,x6322),a2),f28(f24(a2,f23(x6323,x6324)),x6323))),
% 58.92/58.95 inference(scs_inference,[],[619,224])).
% 58.92/58.95 cnf(633,plain,
% 58.92/58.95 (E(x6331,f28(f24(x6331,f23(x6332,x6333)),x6332))),
% 58.92/58.95 inference(rename_variables,[],[619])).
% 58.92/58.95 cnf(634,plain,
% 58.92/58.95 (P8(f28(f24(a4,f23(x6341,x6342)),x6341),x6343)),
% 58.92/58.95 inference(scs_inference,[],[619,633,224,223])).
% 58.92/58.95 cnf(635,plain,
% 58.92/58.95 (E(x6351,f28(f24(x6351,f23(x6352,x6353)),x6352))),
% 58.92/58.95 inference(rename_variables,[],[619])).
% 58.92/58.95 cnf(636,plain,
% 58.92/58.95 (P10(f30(a8,a13,a14),f28(f24(a15,f23(x6361,x6362)),x6361))),
% 58.92/58.95 inference(scs_inference,[],[619,633,635,224,223,218])).
% 58.92/58.95 cnf(637,plain,
% 58.92/58.95 (E(x6371,f28(f24(x6371,f23(x6372,x6373)),x6372))),
% 58.92/58.95 inference(rename_variables,[],[619])).
% 58.92/58.95 cnf(640,plain,
% 58.92/58.95 (E(f30(x6401,a1,a3),f16(f30(x6401,a1,x6402)))),
% 58.92/58.95 inference(scs_inference,[],[619,633,635,92,79,224,223,218,122,2])).
% 58.92/58.95 cnf(643,plain,
% 58.92/58.95 (P11(f28(f24(f27(f30(a8,a13,a14),a15),f23(x6431,x6432)),x6431))),
% 58.92/58.95 inference(scs_inference,[],[94,238,619,633,635,637,92,79,224,223,218,122,2,55,57])).
% 58.92/58.95 cnf(644,plain,
% 58.92/58.95 (E(x6441,f28(f24(x6441,f23(x6442,x6443)),x6442))),
% 58.92/58.95 inference(rename_variables,[],[619])).
% 58.92/58.95 cnf(647,plain,
% 58.92/58.95 (E(f28(f24(f22(f6(f30(x6471,a1,a3),x6472),x6472),f23(x6473,x6474)),x6473),f16(f30(x6471,a1,x6475)))),
% 58.92/58.95 inference(scs_inference,[],[94,238,184,619,633,635,637,644,92,493,79,224,223,218,122,2,55,57,54,3])).
% 58.92/58.95 cnf(659,plain,
% 58.92/58.95 (E(f16(f30(x6591,a1,x6592)),f28(f24(f22(f6(f30(x6591,a1,a3),x6593),x6593),f23(x6594,x6595)),x6594))),
% 58.92/58.95 inference(scs_inference,[],[647,310,122,2])).
% 58.92/58.95 cnf(660,plain,
% 58.92/58.95 (P8(f22(f6(f28(f24(a4,f23(x6601,x6602)),x6601),x6603),x6603),x6604)),
% 58.92/58.95 inference(scs_inference,[],[169,647,634,310,122,2,60])).
% 58.92/58.95 cnf(661,plain,
% 58.92/58.95 (E(x6611,f22(f6(x6611,x6612),x6612))),
% 58.92/58.95 inference(rename_variables,[],[169])).
% 58.92/58.95 cnf(662,plain,
% 58.92/58.95 (P10(f22(f6(f30(a8,a13,a14),x6621),x6621),f28(f24(a15,f23(x6622,x6623)),x6622))),
% 58.92/58.95 inference(scs_inference,[],[169,661,636,647,634,310,122,2,60,55])).
% 58.92/58.95 cnf(691,plain,
% 58.92/58.95 (P8(f17(f30(x6911,a1,x6912)),x6913)),
% 58.92/58.95 inference(scs_inference,[],[89,313,122,2,223])).
% 58.92/58.95 cnf(694,plain,
% 58.92/58.95 (P8(f28(f24(f22(f6(f17(f30(x6941,a1,x6942)),x6943),x6943),f23(x6944,x6945)),x6944),x6946)),
% 58.92/58.95 inference(scs_inference,[],[238,89,660,313,122,2,223,128,60])).
% 58.92/58.95 cnf(703,plain,
% 58.92/58.95 (E(a2,f7(f30(x7031,a1,x7032)))),
% 58.92/58.95 inference(scs_inference,[],[88,364,122,2])).
% 58.92/58.95 cnf(707,plain,
% 58.92/58.95 (E(f22(f6(f16(f30(x7071,a1,x7072)),x7073),x7073),f30(x7071,a1,a3))),
% 58.92/58.95 inference(scs_inference,[],[271,305,534,88,694,364,122,2,60,3])).
% 58.92/58.95 cnf(710,plain,
% 58.92/58.95 (P8(f6(f6(x7101,x7102),a2),f7(f30(x7103,a1,x7104)))),
% 58.92/58.95 inference(scs_inference,[],[271,305,534,88,694,364,122,2,60,3,224])).
% 58.92/58.95 cnf(737,plain,
% 58.92/58.95 (E(f28(f24(f22(f6(a2,x7371),x7371),f23(x7372,x7373)),x7372),f7(f30(x7374,a1,x7375)))),
% 58.92/58.95 inference(scs_inference,[],[169,184,707,703,632,2,60,3])).
% 58.92/58.95 cnf(764,plain,
% 58.92/58.95 (P3(f9(f27(f30(a8,a13,a14),a15)))),
% 58.92/58.95 inference(scs_inference,[],[269,103,221])).
% 58.92/58.95 cnf(765,plain,
% 58.92/58.95 (E(f7(f30(x7651,a1,x7652)),f28(f24(f22(f6(a2,x7653),x7653),f23(x7654,x7655)),x7654))),
% 58.92/58.95 inference(scs_inference,[],[737,2])).
% 58.92/58.95 cnf(766,plain,
% 58.92/58.95 (P8(f28(f24(f22(f6(f6(f6(x7661,x7662),a2),x7663),x7663),f23(x7664,x7665)),x7664),f7(f30(x7666,a1,x7667)))),
% 58.92/58.95 inference(scs_inference,[],[238,737,710,2,60])).
% 58.92/58.95 cnf(792,plain,
% 58.92/58.95 (E(f21(f30(x7921,x7922,x7923),x7924),f30(f25(x7921,x7924),f24(x7922,f23(x7924,a2)),x7923))),
% 58.92/58.95 inference(scs_inference,[],[95,2])).
% 58.92/58.95 cnf(793,plain,
% 58.92/58.95 (P1(f26(f24(x7931,f23(x7932,f30(a8,a13,a14))),x7932),f22(f6(f30(a8,a13,a14),x7933),x7933))),
% 58.92/58.95 inference(scs_inference,[],[402,187,95,2,46])).
% 58.92/58.95 cnf(794,plain,
% 58.92/58.95 (E(x7941,f26(f24(x7942,f23(x7943,x7941)),x7943))),
% 58.92/58.95 inference(rename_variables,[],[402])).
% 58.92/58.95 cnf(795,plain,
% 58.92/58.95 (P15(f6(f6(x7951,a2),x7952),f26(f24(x7953,f23(x7954,a2)),x7954))),
% 58.92/58.95 inference(scs_inference,[],[402,794,187,219,95,2,46,71])).
% 58.92/58.95 cnf(796,plain,
% 58.92/58.95 (E(x7961,f26(f24(x7962,f23(x7963,x7961)),x7963))),
% 58.92/58.95 inference(rename_variables,[],[402])).
% 58.92/58.95 cnf(797,plain,
% 58.92/58.95 (P10(f26(f24(x7971,f23(x7972,f30(a8,a13,a14))),x7972),a15)),
% 58.92/58.95 inference(scs_inference,[],[91,402,794,796,187,219,95,2,46,71,55])).
% 58.92/58.95 cnf(798,plain,
% 58.92/58.95 (E(x7981,f26(f24(x7982,f23(x7983,x7981)),x7983))),
% 58.92/58.95 inference(rename_variables,[],[402])).
% 58.92/58.95 cnf(799,plain,
% 58.92/58.95 (P19(f6(x7991,a2),f26(f24(x7992,f23(x7993,a2)),x7993))),
% 58.92/58.95 inference(scs_inference,[],[91,402,794,796,798,187,219,95,213,2,46,71,55,75])).
% 58.92/58.95 cnf(800,plain,
% 58.92/58.95 (E(x8001,f26(f24(x8002,f23(x8003,x8001)),x8003))),
% 58.92/58.95 inference(rename_variables,[],[402])).
% 58.92/58.95 cnf(802,plain,
% 58.92/58.95 (E(x8021,f26(f24(x8022,f23(x8023,x8021)),x8023))),
% 58.92/58.95 inference(rename_variables,[],[402])).
% 58.92/58.95 cnf(803,plain,
% 58.92/58.95 (P8(x8031,f26(f24(x8032,f23(x8033,a2)),x8033))),
% 58.92/58.95 inference(scs_inference,[],[91,402,794,796,798,800,802,187,219,691,95,213,181,2,46,71,55,75,60,61])).
% 58.92/58.95 cnf(807,plain,
% 58.92/58.95 (E(f22(f6(f30(x8071,a1,a3),x8072),x8072),f16(f30(x8071,a1,x8073)))),
% 58.92/58.95 inference(scs_inference,[],[91,305,402,794,796,798,800,802,647,528,187,219,691,95,208,213,181,2,46,71,55,75,60,61,69,3])).
% 58.92/58.95 cnf(835,plain,
% 58.92/58.95 (~P13(f21(f30(x8351,x8352,a3),x8353))),
% 58.92/58.95 inference(scs_inference,[],[271,792,807,766,102,2,60,69])).
% 58.92/58.95 cnf(838,plain,
% 58.92/58.95 (P10(f26(f24(x8381,f23(x8382,f30(a8,a13,a14))),x8382),f28(f24(f22(f6(a15,x8383),x8383),f23(x8384,x8385)),x8384))),
% 58.92/58.95 inference(scs_inference,[],[271,238,792,807,797,766,102,2,60,69,56])).
% 58.92/58.95 cnf(864,plain,
% 58.92/58.95 (E(x8641,f22(f6(x8641,x8642),x8642))),
% 58.92/58.95 inference(rename_variables,[],[169])).
% 58.92/58.95 cnf(867,plain,
% 58.92/58.95 (P2(f17(f30(x8671,f24(x8672,f23(x8673,x8674)),x8675)))),
% 58.92/58.95 inference(scs_inference,[],[169,864,803,96,799,82,2,75,61,52])).
% 58.92/58.95 cnf(869,plain,
% 58.92/58.95 (P10(f26(f24(x8691,f23(x8692,f30(a8,a13,a14))),x8692),f22(f6(a15,x8693),x8693))),
% 58.92/58.95 inference(scs_inference,[],[271,169,864,838,803,96,799,82,2,75,61,52,56])).
% 58.92/58.95 cnf(872,plain,
% 58.92/58.95 (E(f22(f6(f7(f30(x8721,a1,x8722)),x8723),x8723),a2)),
% 58.92/58.95 inference(scs_inference,[],[271,169,864,305,407,838,803,96,799,82,2,75,61,52,56,3])).
% 58.92/58.95 cnf(882,plain,
% 58.92/58.95 (E(f28(f24(f22(f6(a2,x8821),x8821),f23(x8822,x8823)),x8822),f22(f6(f7(f30(x8824,a1,x8825)),x8826),x8826))),
% 58.92/58.95 inference(scs_inference,[],[184,872,2,3])).
% 58.92/58.95 cnf(1038,plain,
% 58.92/58.95 (P13(f9(f27(f30(a8,a13,a14),a15)))),
% 58.92/58.95 inference(scs_inference,[],[269,104,221])).
% 58.92/58.95 cnf(1050,plain,
% 58.92/58.95 (E(x10501,f28(f24(x10501,f23(x10502,x10503)),x10502))),
% 58.92/58.95 inference(rename_variables,[],[619])).
% 58.92/58.95 cnf(1051,plain,
% 58.92/58.95 (P13(f28(f24(f9(f27(f30(a8,a13,a14),a15)),f23(x10511,x10512)),x10511))),
% 58.92/58.95 inference(scs_inference,[],[619,1050,882,1038,3,69])).
% 58.92/58.95 cnf(1541,plain,
% 58.92/58.95 (P1(x15411,f22(f6(x15411,x15412),x15412))),
% 58.92/58.95 inference(scs_inference,[],[169,80,47])).
% 58.92/58.95 cnf(1857,plain,
% 58.92/58.95 (P9(f27(f30(a8,a13,a14),a15),f9(f27(f30(a8,a13,a14),a15)))),
% 58.92/58.95 inference(scs_inference,[],[269,105,221])).
% 58.92/58.95 cnf(1882,plain,
% 58.92/58.95 (P9(f27(f30(a8,a13,a14),a15),f28(f24(f9(f27(f30(a8,a13,a14),a15)),f23(x18821,x18822)),x18821))),
% 58.92/58.95 inference(scs_inference,[],[619,1857,51])).
% 58.92/58.95 cnf(1883,plain,
% 58.92/58.95 (E(x18831,f28(f24(x18831,f23(x18832,x18833)),x18832))),
% 58.92/58.95 inference(rename_variables,[],[619])).
% 58.92/58.95 cnf(1884,plain,
% 58.92/58.95 (P15(f6(f6(x18841,a2),x18842),f28(f24(a2,f23(x18843,x18844)),x18843))),
% 58.92/58.95 inference(scs_inference,[],[619,1883,1857,219,51,71])).
% 58.92/58.95 cnf(1885,plain,
% 58.92/58.95 (E(x18851,f28(f24(x18851,f23(x18852,x18853)),x18852))),
% 58.92/58.95 inference(rename_variables,[],[619])).
% 58.92/58.96 cnf(1886,plain,
% 58.92/58.96 (P1(f28(f24(f28(f24(f22(f6(a2,x18861),x18861),f23(x18862,x18863)),x18862),f23(x18864,x18865)),x18864),x18866)),
% 58.92/58.96 inference(scs_inference,[],[619,1883,1885,1857,367,219,51,71,46])).
% 58.92/58.96 cnf(1887,plain,
% 58.92/58.96 (E(x18871,f28(f24(x18871,f23(x18872,x18873)),x18872))),
% 58.92/58.96 inference(rename_variables,[],[619])).
% 58.92/58.96 cnf(1888,plain,
% 58.92/58.96 (P8(f28(f24(f26(f24(x18881,f23(x18882,a4)),x18882),f23(x18883,x18884)),x18883),x18885)),
% 58.92/58.96 inference(scs_inference,[],[619,1883,1885,1887,1857,436,367,219,51,71,46,60])).
% 58.92/58.96 cnf(1889,plain,
% 58.92/58.96 (E(x18891,f28(f24(x18891,f23(x18892,x18893)),x18892))),
% 58.92/58.96 inference(rename_variables,[],[619])).
% 58.92/58.96 cnf(1890,plain,
% 58.92/58.96 (P10(f30(a8,a13,a14),f28(f24(f26(f24(x18901,f23(x18902,a15)),x18902),f23(x18903,x18904)),x18903))),
% 58.92/58.96 inference(scs_inference,[],[619,1883,1885,1887,1889,440,1857,436,367,219,51,71,46,60,56])).
% 58.92/58.96 cnf(1891,plain,
% 58.92/58.96 (E(x18911,f28(f24(x18911,f23(x18912,x18913)),x18912))),
% 58.92/58.96 inference(rename_variables,[],[619])).
% 58.92/58.96 cnf(1892,plain,
% 58.92/58.96 (P8(f6(f6(x18921,x18922),a2),f28(f24(f7(f30(x18923,a1,x18924)),f23(x18925,x18926)),x18925))),
% 58.92/58.96 inference(scs_inference,[],[619,1883,1885,1887,1889,1891,440,1857,436,710,367,219,51,71,46,60,56,61])).
% 58.92/58.96 cnf(1893,plain,
% 58.92/58.96 (E(x18931,f28(f24(x18931,f23(x18932,x18933)),x18932))),
% 58.92/58.96 inference(rename_variables,[],[619])).
% 58.92/58.96 cnf(1894,plain,
% 58.92/58.96 (P10(f28(f24(f30(a8,a13,a14),f23(x18941,x18942)),x18941),a15)),
% 58.92/58.96 inference(scs_inference,[],[91,619,1883,1885,1887,1889,1891,1893,440,1857,436,710,367,219,51,71,46,60,56,61,55])).
% 58.92/58.96 cnf(1895,plain,
% 58.92/58.96 (E(x18951,f28(f24(x18951,f23(x18952,x18953)),x18952))),
% 58.92/58.96 inference(rename_variables,[],[619])).
% 58.92/58.96 cnf(1896,plain,
% 58.92/58.96 (P9(f28(f24(f27(f30(a8,a13,a14),a15),f23(x18961,x18962)),x18961),f9(f27(f30(a8,a13,a14),a15)))),
% 58.92/58.96 inference(scs_inference,[],[91,619,1883,1885,1887,1889,1891,1893,1895,440,1857,436,710,367,219,51,71,46,60,56,61,55,50])).
% 58.92/58.96 cnf(1897,plain,
% 58.92/58.96 (E(x18971,f28(f24(x18971,f23(x18972,x18973)),x18972))),
% 58.92/58.96 inference(rename_variables,[],[619])).
% 58.92/58.96 cnf(1898,plain,
% 58.92/58.96 (P19(f6(x18981,a2),f28(f24(a2,f23(x18982,x18983)),x18982))),
% 58.92/58.96 inference(scs_inference,[],[91,619,1883,1885,1887,1889,1891,1893,1895,1897,440,1857,436,710,367,219,213,51,71,46,60,56,61,55,50,75])).
% 58.92/58.96 cnf(1918,plain,
% 58.92/58.96 (E(x19181,f22(f6(x19181,x19182),x19182))),
% 58.92/58.96 inference(rename_variables,[],[169])).
% 58.92/58.96 cnf(1919,plain,
% 58.92/58.96 (P10(f28(f24(f30(a8,a13,a14),f23(x19191,x19192)),x19191),f22(f6(a15,x19193),x19193))),
% 58.92/58.96 inference(scs_inference,[],[169,1918,1894,1886,1892,122,60,56])).
% 58.92/58.96 cnf(1934,plain,
% 58.92/58.96 (E(x19341,f28(f24(x19341,f23(x19342,x19343)),x19342))),
% 58.92/58.96 inference(rename_variables,[],[619])).
% 58.92/58.96 cnf(1935,plain,
% 58.92/58.96 (P15(f6(x19351,a2),f28(f24(a2,f23(x19352,x19353)),x19352))),
% 58.92/58.96 inference(scs_inference,[],[619,1934,1896,210,51,71])).
% 58.92/58.96 cnf(1936,plain,
% 58.92/58.96 (E(x19361,f28(f24(x19361,f23(x19362,x19363)),x19362))),
% 58.92/58.96 inference(rename_variables,[],[619])).
% 58.92/58.96 cnf(1937,plain,
% 58.92/58.96 (P1(f28(f24(f28(f24(f28(f24(f22(f6(a2,x19371),x19371),f23(x19372,x19373)),x19372),f23(x19374,x19375)),x19374),f23(x19376,x19377)),x19376),x19378)),
% 58.92/58.96 inference(scs_inference,[],[619,1934,1936,1886,1896,210,51,71,46])).
% 58.92/58.96 cnf(1938,plain,
% 58.92/58.96 (E(x19381,f28(f24(x19381,f23(x19382,x19383)),x19382))),
% 58.92/58.96 inference(rename_variables,[],[619])).
% 58.92/58.96 cnf(1939,plain,
% 58.92/58.96 (P8(f28(f24(f28(f24(a4,f23(x19391,x19392)),x19391),f23(x19393,x19394)),x19393),x19395)),
% 58.92/58.96 inference(scs_inference,[],[619,1934,1936,1938,634,1886,1896,210,51,71,46,60])).
% 58.92/58.96 cnf(1940,plain,
% 58.92/58.96 (E(x19401,f28(f24(x19401,f23(x19402,x19403)),x19402))),
% 58.92/58.96 inference(rename_variables,[],[619])).
% 58.92/58.96 cnf(1941,plain,
% 58.92/58.96 (P8(f6(f6(x19411,x19412),a2),f28(f24(f28(f24(a2,f23(x19413,x19414)),x19413),f23(x19415,x19416)),x19415))),
% 58.92/58.96 inference(scs_inference,[],[619,1934,1936,1938,1940,634,632,1886,1896,210,51,71,46,60,61])).
% 58.92/58.96 cnf(1942,plain,
% 58.92/58.96 (E(x19421,f28(f24(x19421,f23(x19422,x19423)),x19422))),
% 58.92/58.96 inference(rename_variables,[],[619])).
% 58.92/58.96 cnf(1943,plain,
% 58.92/58.96 (P10(f30(a8,a13,a14),f28(f24(f28(f24(a15,f23(x19431,x19432)),x19431),f23(x19433,x19434)),x19433))),
% 58.92/58.96 inference(scs_inference,[],[619,1934,1936,1938,1940,1942,636,634,632,1886,1896,210,51,71,46,60,61,56])).
% 58.92/58.96 cnf(1944,plain,
% 58.92/58.96 (E(x19441,f28(f24(x19441,f23(x19442,x19443)),x19442))),
% 58.92/58.96 inference(rename_variables,[],[619])).
% 58.92/58.96 cnf(1945,plain,
% 58.92/58.96 (P10(f28(f24(f30(a8,a13,a14),f23(x19451,x19452)),x19451),f26(f24(x19453,f23(x19454,a15)),x19454))),
% 58.92/58.96 inference(scs_inference,[],[619,1934,1936,1938,1940,1942,1944,440,636,634,632,1886,1896,210,51,71,46,60,61,56,55])).
% 58.92/58.96 cnf(1946,plain,
% 58.92/58.96 (E(x19461,f28(f24(x19461,f23(x19462,x19463)),x19462))),
% 58.92/58.96 inference(rename_variables,[],[619])).
% 58.92/58.96 cnf(1947,plain,
% 58.92/58.96 (P9(f28(f24(f28(f24(f27(f30(a8,a13,a14),a15),f23(x19471,x19472)),x19471),f23(x19473,x19474)),x19473),f9(f27(f30(a8,a13,a14),a15)))),
% 58.92/58.96 inference(scs_inference,[],[619,1934,1936,1938,1940,1942,1944,1946,440,636,634,632,1886,1896,210,51,71,46,60,61,56,55,50])).
% 58.92/58.96 cnf(1948,plain,
% 58.92/58.96 (E(x19481,f28(f24(x19481,f23(x19482,x19483)),x19482))),
% 58.92/58.96 inference(rename_variables,[],[619])).
% 58.92/58.96 cnf(1949,plain,
% 58.92/58.96 (P19(f6(f6(x19491,a2),x19492),f28(f24(a2,f23(x19493,x19494)),x19493))),
% 58.92/58.96 inference(scs_inference,[],[619,1934,1936,1938,1940,1942,1944,1946,1948,440,636,634,632,1886,1896,210,216,51,71,46,60,61,56,55,50,75])).
% 58.92/58.96 cnf(1969,plain,
% 58.92/58.96 (E(x19691,f28(f24(x19691,f23(x19692,x19693)),x19692))),
% 58.92/58.96 inference(rename_variables,[],[619])).
% 58.92/58.96 cnf(1971,plain,
% 58.92/58.96 (E(x19711,f28(f24(x19711,f23(x19712,x19713)),x19712))),
% 58.92/58.96 inference(rename_variables,[],[619])).
% 58.92/58.96 cnf(1972,plain,
% 58.92/58.96 (P1(f28(f24(a2,f23(x19721,x19722)),x19721),x19723)),
% 58.92/58.96 inference(scs_inference,[],[619,1969,1971,1937,1882,79,318,122,51,71,46])).
% 58.92/58.96 cnf(1973,plain,
% 58.92/58.96 (E(x19731,f28(f24(x19731,f23(x19732,x19733)),x19732))),
% 58.92/58.96 inference(rename_variables,[],[619])).
% 58.92/58.96 cnf(1974,plain,
% 58.92/58.96 (P8(f28(f24(f17(f30(x19741,a1,x19742)),f23(x19743,x19744)),x19743),x19745)),
% 58.92/58.96 inference(scs_inference,[],[619,1969,1971,1973,691,1937,1882,79,318,122,51,71,46,60])).
% 58.92/58.96 cnf(1975,plain,
% 58.92/58.96 (E(x19751,f28(f24(x19751,f23(x19752,x19753)),x19752))),
% 58.92/58.96 inference(rename_variables,[],[619])).
% 58.92/58.96 cnf(1977,plain,
% 58.92/58.96 (E(x19771,f28(f24(x19771,f23(x19772,x19773)),x19772))),
% 58.92/58.96 inference(rename_variables,[],[619])).
% 58.92/58.96 cnf(1978,plain,
% 58.92/58.96 (P10(f30(a8,a13,a14),f28(f24(f28(f24(f22(f6(a15,x19781),x19781),f23(x19782,x19783)),x19782),f23(x19784,x19785)),x19784))),
% 58.92/58.96 inference(scs_inference,[],[619,1969,1971,1973,1975,1977,301,691,386,1937,1882,79,318,122,51,71,46,60,61,56])).
% 58.92/58.96 cnf(1979,plain,
% 58.92/58.96 (E(x19791,f28(f24(x19791,f23(x19792,x19793)),x19792))),
% 58.92/58.96 inference(rename_variables,[],[619])).
% 58.92/58.96 cnf(1981,plain,
% 58.92/58.96 (E(x19811,f28(f24(x19811,f23(x19812,x19813)),x19812))),
% 58.92/58.96 inference(rename_variables,[],[619])).
% 58.92/58.96 cnf(1982,plain,
% 58.92/58.96 (P19(f6(x19821,a2),f28(f24(f26(f24(x19822,f23(x19823,a2)),x19823),f23(x19824,x19825)),x19824))),
% 58.92/58.96 inference(scs_inference,[],[619,1969,1971,1973,1975,1977,1979,1981,461,301,691,386,1937,1882,79,318,799,122,51,71,46,60,61,56,55,75])).
% 58.92/58.96 cnf(1984,plain,
% 58.92/58.96 (P8(x19841,f28(f24(a2,f23(x19842,x19843)),x19842))),
% 58.92/58.96 inference(scs_inference,[],[619,1969,1971,1973,1975,1977,1979,1981,461,301,691,386,1937,1882,79,318,799,122,51,71,46,60,61,56,55,75,137])).
% 58.92/58.96 cnf(2036,plain,
% 58.92/58.96 (P15(f6(x20361,a2),f28(f24(f28(f24(f22(f6(a2,x20362),x20362),f23(x20363,x20364)),x20363),f23(x20365,x20366)),x20365))),
% 58.92/58.96 inference(scs_inference,[],[619,373,71])).
% 58.92/58.96 cnf(2037,plain,
% 58.92/58.96 (E(x20371,f28(f24(x20371,f23(x20372,x20373)),x20372))),
% 58.92/58.96 inference(rename_variables,[],[619])).
% 58.92/58.96 cnf(2038,plain,
% 58.92/58.96 (P1(f28(f24(f28(f24(a2,f23(x20381,x20382)),x20381),f23(x20383,x20384)),x20383),x20385)),
% 58.92/58.96 inference(scs_inference,[],[619,2037,1972,373,71,46])).
% 58.92/58.96 cnf(2039,plain,
% 58.92/58.96 (E(x20391,f28(f24(x20391,f23(x20392,x20393)),x20392))),
% 58.92/58.96 inference(rename_variables,[],[619])).
% 58.92/58.96 cnf(2041,plain,
% 58.92/58.96 (E(x20411,f28(f24(x20411,f23(x20412,x20413)),x20412))),
% 58.92/58.96 inference(rename_variables,[],[619])).
% 58.92/58.96 cnf(2043,plain,
% 58.92/58.96 (E(x20431,f28(f24(x20431,f23(x20432,x20433)),x20432))),
% 58.92/58.96 inference(rename_variables,[],[619])).
% 58.92/58.96 cnf(2044,plain,
% 58.92/58.96 (P8(x20441,f28(f24(f26(f24(x20442,f23(x20443,a2)),x20443),f23(x20444,x20445)),x20444))),
% 58.92/58.96 inference(scs_inference,[],[619,2037,2039,2041,2043,662,710,803,1972,373,71,46,60,56,61])).
% 58.92/58.96 cnf(2045,plain,
% 58.92/58.96 (E(x20451,f28(f24(x20451,f23(x20452,x20453)),x20452))),
% 58.92/58.96 inference(rename_variables,[],[619])).
% 58.92/58.96 cnf(2047,plain,
% 58.92/58.96 (E(x20471,f28(f24(x20471,f23(x20472,x20473)),x20472))),
% 58.92/58.96 inference(rename_variables,[],[619])).
% 58.92/58.96 cnf(2048,plain,
% 58.92/58.96 (P19(f6(x20481,a2),f28(f24(f28(f24(f22(f6(a2,x20482),x20482),f23(x20483,x20484)),x20483),f23(x20485,x20486)),x20485))),
% 58.92/58.96 inference(scs_inference,[],[619,2037,2039,2041,2043,2045,2047,636,662,710,803,1972,373,326,71,46,60,56,61,55,75])).
% 58.92/58.96 cnf(2068,plain,
% 58.92/58.96 (P15(f6(f6(x20681,a2),x20682),f28(f24(f26(f24(x20683,f23(x20684,a2)),x20684),f23(x20685,x20686)),x20685))),
% 58.92/58.96 inference(scs_inference,[],[619,795,71])).
% 58.92/58.96 cnf(2069,plain,
% 58.92/58.96 (E(x20691,f28(f24(x20691,f23(x20692,x20693)),x20692))),
% 58.92/58.96 inference(rename_variables,[],[619])).
% 58.92/58.96 cnf(2071,plain,
% 58.92/58.96 (E(x20711,f28(f24(x20711,f23(x20712,x20713)),x20712))),
% 58.92/58.96 inference(rename_variables,[],[619])).
% 58.92/58.96 cnf(2072,plain,
% 58.92/58.96 (P8(f28(f24(f28(f24(f22(f6(a4,x20721),x20721),f23(x20722,x20723)),x20722),f23(x20724,x20725)),x20724),x20726)),
% 58.92/58.96 inference(scs_inference,[],[619,2069,2071,297,2038,795,71,46,60])).
% 58.92/58.96 cnf(2189,plain,
% 58.92/58.96 (P15(f6(x21891,a2),f28(f24(f28(f24(a2,f23(x21892,x21893)),x21892),f23(x21894,x21895)),x21894))),
% 58.92/58.96 inference(scs_inference,[],[619,1935,71])).
% 58.92/58.96 cnf(2190,plain,
% 58.92/58.96 (E(x21901,f28(f24(x21901,f23(x21902,x21903)),x21902))),
% 58.92/58.96 inference(rename_variables,[],[619])).
% 58.92/58.96 cnf(2192,plain,
% 58.92/58.96 (E(x21921,f28(f24(x21921,f23(x21922,x21923)),x21922))),
% 58.92/58.96 inference(rename_variables,[],[619])).
% 58.92/58.96 cnf(2194,plain,
% 58.92/58.96 (E(x21941,f28(f24(x21941,f23(x21942,x21943)),x21942))),
% 58.92/58.96 inference(rename_variables,[],[619])).
% 58.92/58.96 cnf(2196,plain,
% 58.92/58.96 (E(x21961,f28(f24(x21961,f23(x21962,x21963)),x21962))),
% 58.92/58.96 inference(rename_variables,[],[619])).
% 58.92/58.96 cnf(2197,plain,
% 58.92/58.96 (P10(f28(f24(f30(a8,a13,a14),f23(x21971,x21972)),x21971),f28(f24(f22(f6(a15,x21973),x21973),f23(x21974,x21975)),x21974))),
% 58.92/58.96 inference(scs_inference,[],[619,2190,2192,2194,2196,301,1943,1888,1892,1935,71,60,56,61,55])).
% 58.92/58.96 cnf(2198,plain,
% 58.92/58.96 (E(x21981,f28(f24(x21981,f23(x21982,x21983)),x21982))),
% 58.92/58.96 inference(rename_variables,[],[619])).
% 58.92/58.96 cnf(2199,plain,
% 58.92/58.96 (P19(f6(x21991,a2),f28(f24(f28(f24(a2,f23(x21992,x21993)),x21992),f23(x21994,x21995)),x21994))),
% 58.92/58.96 inference(scs_inference,[],[619,2190,2192,2194,2196,2198,301,1943,1888,1892,1898,1935,71,60,56,61,55,75])).
% 58.92/58.96 cnf(2217,plain,
% 58.92/58.96 (P1(f7(f30(x22171,a1,x22172)),f22(f6(a2,x22173),x22173))),
% 58.92/58.96 inference(scs_inference,[],[415,710,126])).
% 58.92/58.96 cnf(2220,plain,
% 58.92/58.96 (P1(f22(f6(f7(f30(x22201,a1,x22202)),x22203),x22203),f22(f6(a2,x22204),x22204))),
% 58.92/58.96 inference(scs_inference,[],[415,190,710,126,127])).
% 58.92/58.96 cnf(2250,plain,
% 58.92/58.96 (P1(f7(f30(x22501,a1,x22502)),a2)),
% 58.92/58.96 inference(scs_inference,[],[710,167,2220,122,126])).
% 58.92/58.96 cnf(2253,plain,
% 58.92/58.96 (P1(f22(f6(f7(f30(x22531,a1,x22532)),x22533),x22533),a2)),
% 58.92/58.96 inference(scs_inference,[],[190,710,167,2220,122,126,127])).
% 58.92/58.96 cnf(2571,plain,
% 58.92/58.96 (P1(x25711,f22(f6(f22(f6(x25711,x25712),x25712),x25713),x25713))),
% 58.92/58.96 inference(scs_inference,[],[169,1541,47])).
% 58.92/58.96 cnf(2598,plain,
% 58.92/58.96 (E(x25981,f28(f24(x25981,f23(x25982,x25983)),x25982))),
% 58.92/58.96 inference(rename_variables,[],[619])).
% 58.92/58.96 cnf(2600,plain,
% 58.92/58.96 (E(x26001,f28(f24(x26001,f23(x26002,x26003)),x26002))),
% 58.92/58.96 inference(rename_variables,[],[619])).
% 58.92/58.96 cnf(2601,plain,
% 58.92/58.96 (P1(f28(f24(f7(f30(x26011,a1,x26012)),f23(x26013,x26014)),x26013),f22(f6(a2,x26015),x26015))),
% 58.92/58.96 inference(scs_inference,[],[619,2598,2600,1892,2217,2250,60,47,46])).
% 58.92/58.96 cnf(2602,plain,
% 58.92/58.96 (E(x26021,f28(f24(x26021,f23(x26022,x26023)),x26022))),
% 58.92/58.96 inference(rename_variables,[],[619])).
% 58.92/58.96 cnf(2603,plain,
% 58.92/58.96 (P15(f6(f6(x26031,a2),x26032),f28(f24(f28(f24(a2,f23(x26033,x26034)),x26033),f23(x26035,x26036)),x26035))),
% 58.92/58.96 inference(scs_inference,[],[619,2598,2600,2602,1892,2217,2250,1884,60,47,46,71])).
% 58.92/58.96 cnf(2604,plain,
% 58.92/58.96 (E(x26041,f28(f24(x26041,f23(x26042,x26043)),x26042))),
% 58.92/58.96 inference(rename_variables,[],[619])).
% 58.92/58.96 cnf(2606,plain,
% 58.92/58.96 (E(x26061,f28(f24(x26061,f23(x26062,x26063)),x26062))),
% 58.92/58.96 inference(rename_variables,[],[619])).
% 58.92/58.96 cnf(2608,plain,
% 58.92/58.96 (E(x26081,f28(f24(x26081,f23(x26082,x26083)),x26082))),
% 58.92/58.96 inference(rename_variables,[],[619])).
% 58.92/58.96 cnf(2610,plain,
% 58.92/58.96 (E(x26101,f28(f24(x26101,f23(x26102,x26103)),x26102))),
% 58.92/58.96 inference(rename_variables,[],[619])).
% 58.92/58.96 cnf(2611,plain,
% 58.92/58.96 (P19(f6(f6(x26111,a2),x26112),f28(f24(f28(f24(a2,f23(x26113,x26114)),x26113),f23(x26115,x26116)),x26115))),
% 58.92/58.96 inference(scs_inference,[],[619,2598,2600,2602,2604,2606,2608,2610,869,1978,1892,1941,2217,2250,1884,1949,60,47,46,71,56,61,55,75])).
% 58.92/58.96 cnf(2645,plain,
% 58.92/58.96 (P9(f22(f6(f16(f30(x26451,a1,x26452)),x26453),x26453),f30(x26451,a1,a3))),
% 58.92/58.96 inference(scs_inference,[],[707,273,51])).
% 58.92/58.96 cnf(2647,plain,
% 58.92/58.96 (P1(f22(f6(f16(f30(x26471,a1,x26472)),x26473),x26473),f30(x26471,a1,a3))),
% 58.92/58.96 inference(scs_inference,[],[707,246,273,51,47])).
% 58.92/58.96 cnf(2648,plain,
% 58.92/58.96 (P1(f22(f6(x26481,x26482),x26482),f22(f6(x26481,x26483),x26483))),
% 58.92/58.96 inference(rename_variables,[],[246])).
% 58.92/58.96 cnf(2651,plain,
% 58.92/58.96 (P1(f30(x26511,a1,a3),f22(f6(f16(f30(x26511,a1,x26512)),x26513),x26513))),
% 58.92/58.96 inference(scs_inference,[],[707,275,246,2648,273,51,47,63,46])).
% 58.92/58.96 cnf(2653,plain,
% 58.92/58.96 (P8(x26531,f7(f30(x26532,a1,x26533)))),
% 58.92/58.96 inference(scs_inference,[],[707,703,275,246,2648,273,181,51,47,63,46,61])).
% 58.92/58.96 cnf(2654,plain,
% 58.92/58.96 (P19(f6(x26541,a2),f7(f30(x26542,a1,x26543)))),
% 58.92/58.96 inference(scs_inference,[],[707,703,275,246,2648,273,181,213,51,47,63,46,61,75])).
% 58.92/58.96 cnf(2660,plain,
% 58.92/58.96 (P15(f6(f6(x26601,a2),x26602),f7(f30(x26603,a1,x26604)))),
% 58.92/58.96 inference(scs_inference,[],[534,640,707,703,275,246,2648,190,219,273,181,213,51,47,63,46,61,75,3,127,71])).
% 58.92/58.96 cnf(2661,plain,
% 58.92/58.96 (P6(f24(x26611,f23(f16(f30(x26612,a1,x26613)),x26614)),f30(x26612,a1,a3))),
% 58.92/58.96 inference(scs_inference,[],[534,640,707,703,275,246,2648,403,190,219,273,181,213,51,47,63,46,61,75,3,127,71,59])).
% 58.92/58.96 cnf(2663,plain,
% 58.92/58.96 (P9(f30(x26631,a1,a3),f16(f30(x26631,a1,x26632)))),
% 58.92/58.96 inference(scs_inference,[],[534,640,707,703,275,246,2648,403,190,194,219,273,181,213,51,47,63,46,61,75,3,127,71,59,50])).
% 58.92/58.96 cnf(2665,plain,
% 58.92/58.96 (E(f16(f30(x26651,a1,x26652)),f28(f24(f22(f6(f16(f30(x26651,a1,x26653)),x26654),x26654),f23(x26655,x26656)),x26655))),
% 58.92/58.96 inference(scs_inference,[],[534,640,707,703,275,246,2648,403,190,194,219,273,181,213,51,47,63,46,61,75,3,127,71,59,50,2])).
% 58.92/58.96 cnf(2675,plain,
% 58.92/58.96 (P9(f16(f30(x26751,a1,x26752)),f30(x26751,a1,a3))),
% 58.92/58.96 inference(scs_inference,[],[707,192,2651,122,51])).
% 58.92/58.96 cnf(2677,plain,
% 58.92/58.96 (P1(f16(f30(x26771,a1,x26772)),f30(x26771,a1,a3))),
% 58.92/58.96 inference(scs_inference,[],[707,192,1541,2651,122,51,47])).
% 58.92/58.96 cnf(2679,plain,
% 58.92/58.96 (P4(f6(x26791,f16(f30(x26792,a1,x26793))),f30(x26792,a1,a3))),
% 58.92/58.96 inference(scs_inference,[],[707,415,192,1541,2651,122,51,47,63])).
% 58.92/58.96 cnf(2681,plain,
% 58.92/58.96 (P1(f30(x26811,a1,a3),f16(f30(x26811,a1,x26812)))),
% 58.92/58.96 inference(scs_inference,[],[707,415,190,192,1541,2651,122,51,47,63,46])).
% 58.92/58.96 cnf(2682,plain,
% 58.92/58.96 (P1(f22(f6(x26821,x26822),x26822),x26821)),
% 58.92/58.96 inference(rename_variables,[],[190])).
% 58.92/58.96 cnf(2683,plain,
% 58.92/58.96 (P1(f22(f6(f30(x26831,a1,a3),x26832),x26832),f16(f30(x26831,a1,x26833)))),
% 58.92/58.96 inference(scs_inference,[],[707,415,190,2682,192,1541,2651,122,51,47,63,46,127])).
% 58.92/58.96 cnf(2686,plain,
% 58.92/58.96 (P19(f6(f6(x26861,a2),x26862),f7(f30(x26863,a1,x26864)))),
% 58.92/58.96 inference(scs_inference,[],[707,703,415,190,2682,192,1541,2651,216,122,51,47,63,46,127,75])).
% 58.92/58.96 cnf(2689,plain,
% 58.92/58.96 (P15(f6(x26891,a2),f7(f30(x26892,a1,x26893)))),
% 58.92/58.96 inference(scs_inference,[],[707,703,490,415,190,2682,192,1541,2651,210,216,122,51,47,63,46,127,75,3,71])).
% 58.92/58.96 cnf(2690,plain,
% 58.92/58.96 (P6(f24(x26901,f23(f16(f30(x26902,a1,x26903)),x26904)),f16(f30(x26902,a1,x26905)))),
% 58.92/58.96 inference(scs_inference,[],[640,707,703,490,415,190,2682,192,1541,2661,2651,210,216,122,51,47,63,46,127,75,3,71,59])).
% 58.92/58.96 cnf(2708,plain,
% 58.92/58.96 (P1(f22(f6(f16(f30(x27081,a1,x27082)),x27083),x27083),f16(f30(x27081,a1,x27084)))),
% 58.92/58.96 inference(scs_inference,[],[640,2647,2645,2677,122,51,47])).
% 58.92/58.96 cnf(2710,plain,
% 58.92/58.96 (P1(f16(f30(x27101,a1,x27102)),f22(f6(f16(f30(x27101,a1,x27103)),x27104),x27104))),
% 58.92/58.96 inference(scs_inference,[],[640,2647,2651,2645,2677,122,51,47,46])).
% 58.92/58.96 cnf(2712,plain,
% 58.92/58.96 (P4(f6(x27121,f16(f30(x27122,a1,x27123))),f16(f30(x27122,a1,x27124)))),
% 58.92/58.96 inference(scs_inference,[],[640,2647,2651,2645,2679,2677,122,51,47,46,63])).
% 58.92/58.96 cnf(2725,plain,
% 58.92/58.96 (P9(f16(f30(x27251,a1,x27252)),f16(f30(x27251,a1,x27253)))),
% 58.92/58.96 inference(scs_inference,[],[640,2681,2675,122,51])).
% 58.92/58.96 cnf(2726,plain,
% 58.92/58.96 (P9(f16(f30(x27261,a1,x27262)),f30(x27261,a1,a3))),
% 58.92/58.96 inference(rename_variables,[],[2675])).
% 58.92/58.96 cnf(2727,plain,
% 58.92/58.96 (P4(f6(x27271,f16(f30(x27272,a1,x27273))),f28(f24(f22(f6(f30(x27272,a1,a3),x27274),x27274),f23(x27275,x27276)),x27275))),
% 58.92/58.96 inference(scs_inference,[],[640,659,2681,2712,2675,122,51,63])).
% 58.92/58.96 cnf(2729,plain,
% 58.92/58.96 (P1(f16(f30(x27291,a1,x27292)),f16(f30(x27291,a1,x27293)))),
% 58.92/58.96 inference(scs_inference,[],[640,659,2681,2712,2675,122,51,63,46])).
% 58.92/58.96 cnf(2730,plain,
% 58.92/58.96 (P1(f30(x27301,a1,a3),f16(f30(x27301,a1,x27302)))),
% 58.92/58.96 inference(rename_variables,[],[2681])).
% 58.92/58.96 cnf(2731,plain,
% 58.92/58.96 (P1(f30(x27311,a1,a3),f28(f24(f22(f6(f30(x27311,a1,a3),x27312),x27312),f23(x27313,x27314)),x27313))),
% 58.92/58.96 inference(scs_inference,[],[640,659,2681,2730,2712,2675,122,51,63,46,47])).
% 58.92/58.96 cnf(2733,plain,
% 58.92/58.96 (P9(f28(f24(f22(f6(f30(x27331,a1,a3),x27332),x27332),f23(x27333,x27334)),x27333),f30(x27331,a1,a3))),
% 58.92/58.96 inference(scs_inference,[],[640,659,2681,2730,2712,2675,2726,122,51,63,46,47,50])).
% 58.92/58.96 cnf(2750,plain,
% 58.92/58.96 (P1(f16(f30(x27501,a1,x27502)),f28(f24(f22(f6(f30(x27501,a1,a3),x27503),x27503),f23(x27504,x27505)),x27504))),
% 58.92/58.96 inference(scs_inference,[],[640,659,2708,2733,2729,122,51,47])).
% 58.92/58.96 cnf(2769,plain,
% 58.92/58.96 (P1(f28(f24(f22(f6(f16(f30(x27691,a1,x27692)),x27693),x27693),f23(x27694,x27695)),x27694),f30(x27691,a1,a3))),
% 58.92/58.96 inference(scs_inference,[],[534,659,2731,2725,2729,80,122,51,46,47])).
% 58.92/58.96 cnf(2783,plain,
% 58.92/58.96 (P1(f28(f24(f22(f6(f16(f30(x27831,a1,x27832)),x27833),x27833),f23(x27834,x27835)),x27834),f16(f30(x27831,a1,x27836)))),
% 58.92/58.96 inference(scs_inference,[],[640,659,2750,2769,2663,122,51,47])).
% 58.92/58.96 cnf(2796,plain,
% 58.92/58.96 (P9(f28(f24(f22(f6(f16(f30(x27961,a1,x27962)),x27963),x27963),f23(x27964,x27965)),x27964),f30(x27961,a1,a3))),
% 58.92/58.96 inference(scs_inference,[],[534,2710,81,122,51])).
% 58.92/58.96 cnf(2813,plain,
% 58.92/58.96 (P1(f7(f30(x28131,a1,x28132)),x28133)),
% 58.92/58.96 inference(scs_inference,[],[640,703,2783,2796,79,2253,122,51,47,46])).
% 58.92/58.96 cnf(2818,plain,
% 58.92/58.96 (P8(x28181,f22(f6(f7(f30(x28182,a1,x28183)),x28184),x28184))),
% 58.92/58.96 inference(scs_inference,[],[640,703,190,93,2783,2796,79,2253,122,51,47,46,127,53,137])).
% 58.92/58.96 cnf(2858,plain,
% 58.92/58.96 (P6(f24(x28581,f23(f30(x28582,a1,a3),x28583)),f16(f30(x28582,a1,x28584)))),
% 58.92/58.96 inference(scs_inference,[],[640,402,206,168,2813,122,63,3,59])).
% 58.92/58.96 cnf(2860,plain,
% 58.92/58.96 (P9(f22(f6(f30(x28601,a1,a3),x28602),x28602),f16(f30(x28601,a1,x28603)))),
% 58.92/58.96 inference(scs_inference,[],[640,402,206,168,194,2813,122,63,3,59,51])).
% 58.92/58.96 cnf(2862,plain,
% 58.92/58.96 (P9(f16(f30(x28621,a1,x28622)),f22(f6(f30(x28621,a1,a3),x28623),x28623))),
% 58.92/58.96 inference(scs_inference,[],[640,402,206,168,194,192,2813,122,63,3,59,51,50])).
% 58.92/58.96 cnf(2864,plain,
% 58.92/58.96 (P1(f16(f30(x28641,a1,x28642)),f22(f6(f30(x28641,a1,a3),x28643),x28643))),
% 58.92/58.96 inference(scs_inference,[],[640,402,206,168,194,192,1541,2813,122,63,3,59,51,50,46])).
% 58.92/58.96 cnf(2903,plain,
% 58.92/58.96 (P4(f6(x29031,f30(x29032,a1,a3)),f16(f30(x29032,a1,x29033)))),
% 58.92/58.96 inference(scs_inference,[],[640,167,2729,122,63])).
% 58.92/58.96 cnf(2995,plain,
% 58.92/58.96 (P6(f24(x29951,f23(f22(f6(a1,x29952),x29952),x29953)),f5(a1,x29954))),
% 58.92/58.96 inference(scs_inference,[],[363,202,2683,122,59])).
% 58.92/58.96 cnf(2997,plain,
% 58.92/58.96 (P4(f6(x29971,f22(f6(a1,x29972),x29972)),f5(a1,x29973))),
% 58.92/58.96 inference(scs_inference,[],[363,206,202,2683,122,59,63])).
% 58.92/58.96 cnf(2999,plain,
% 58.92/58.96 (E(a1,f26(f24(x29991,f23(x29992,f5(a1,x29993))),x29992))),
% 58.92/58.96 inference(scs_inference,[],[363,402,206,202,2683,122,59,63,3])).
% 58.92/58.96 cnf(3001,plain,
% 58.92/58.96 (P1(f22(f6(a1,x30011),x30011),f5(a1,x30012))),
% 58.92/58.96 inference(scs_inference,[],[363,402,206,190,202,2683,122,59,63,3,47])).
% 58.92/58.96 cnf(3003,plain,
% 58.92/58.96 (P9(f22(f6(a1,x30031),x30031),f5(a1,x30032))),
% 58.92/58.96 inference(scs_inference,[],[363,402,206,190,202,194,2683,122,59,63,3,47,51])).
% 58.92/58.96 cnf(3005,plain,
% 58.92/58.96 (P9(f5(a1,x30051),f22(f6(a1,x30052),x30052))),
% 58.92/58.96 inference(scs_inference,[],[363,402,206,190,202,194,192,2683,122,59,63,3,47,51,50])).
% 58.92/58.96 cnf(3007,plain,
% 58.92/58.96 (P1(f5(a1,x30071),f22(f6(a1,x30072),x30072))),
% 58.92/58.96 inference(scs_inference,[],[363,402,206,190,202,194,192,1541,2683,122,59,63,3,47,51,50,46])).
% 58.92/58.96 cnf(3009,plain,
% 58.92/58.96 (E(f26(f24(x30091,f23(x30092,f5(a1,x30093))),x30092),a1)),
% 58.92/58.96 inference(scs_inference,[],[363,402,206,190,202,194,192,1541,2683,122,59,63,3,47,51,50,46,2])).
% 58.92/58.96 cnf(3010,plain,
% 58.92/58.96 (E(f22(f6(a1,x30101),x30101),f5(a1,x30102))),
% 58.92/58.96 inference(scs_inference,[],[363,402,206,190,202,194,192,1541,2683,100,122,59,63,3,47,51,50,46,2,148])).
% 58.92/58.96 cnf(3029,plain,
% 58.92/58.96 (P1(f22(f6(f5(a1,x30291),x30292),x30292),f22(f6(a1,x30293),x30293))),
% 58.92/58.96 inference(scs_inference,[],[3010,190,3001,3007,2,122,127])).
% 58.92/58.96 cnf(3032,plain,
% 58.92/58.96 (P6(f24(x30321,f23(a1,x30322)),f5(a1,x30323))),
% 58.92/58.96 inference(scs_inference,[],[363,3010,190,168,3001,3007,2,122,127,59])).
% 58.92/58.96 cnf(3034,plain,
% 58.92/58.96 (P4(f6(x30341,a1),f5(a1,x30342))),
% 58.92/58.96 inference(scs_inference,[],[363,3010,167,190,168,3001,3007,2,122,127,59,63])).
% 58.92/58.96 cnf(3036,plain,
% 58.92/58.96 (~E(f24(x30361,f23(x30362,x30363)),f22(f6(a1,x30364),x30364))),
% 58.92/58.96 inference(scs_inference,[],[363,381,3010,167,190,168,3001,3007,2,122,127,59,63,3])).
% 58.92/58.96 cnf(3038,plain,
% 58.92/58.96 (P9(f5(a1,x30381),f22(f6(f22(f6(a1,x30382),x30382),x30383),x30383))),
% 58.92/58.96 inference(scs_inference,[],[363,381,3010,167,190,168,263,3001,3007,2,122,127,59,63,3,50])).
% 58.92/58.96 cnf(3040,plain,
% 58.92/58.96 (P1(a1,f5(a1,x30401))),
% 58.92/58.96 inference(scs_inference,[],[363,381,3010,167,190,168,263,3001,3007,80,2,122,127,59,63,3,50,47])).
% 58.92/58.96 cnf(3042,plain,
% 58.92/58.96 (P9(f22(f6(f22(f6(a1,x30421),x30421),x30422),x30422),f5(a1,x30423))),
% 58.92/58.96 inference(scs_inference,[],[363,381,3010,167,190,168,263,421,3001,3007,80,2,122,127,59,63,3,50,47,51])).
% 58.92/58.96 cnf(3044,plain,
% 58.92/58.96 (P1(f5(a1,x30441),f22(f6(f22(f6(a1,x30442),x30442),x30443),x30443))),
% 58.92/58.96 inference(scs_inference,[],[363,381,3010,167,190,168,263,421,2571,3001,3007,80,2,122,127,59,63,3,50,47,51,46])).
% 58.92/58.96 cnf(3059,plain,
% 58.92/58.96 (E(x30591,f22(f6(x30591,x30592),x30592))),
% 58.92/58.96 inference(rename_variables,[],[169])).
% 58.92/58.96 cnf(3061,plain,
% 58.92/58.96 (E(x30611,f22(f6(x30611,x30612),x30612))),
% 58.92/58.96 inference(rename_variables,[],[169])).
% 58.92/58.96 cnf(3063,plain,
% 58.92/58.96 (E(x30631,f22(f6(x30631,x30632),x30632))),
% 58.92/58.96 inference(rename_variables,[],[169])).
% 58.92/58.96 cnf(3065,plain,
% 58.92/58.96 (E(x30651,f22(f6(x30651,x30652),x30652))),
% 58.92/58.96 inference(rename_variables,[],[169])).
% 58.92/58.96 cnf(3066,plain,
% 58.92/58.96 (~E(f24(x30661,f23(x30662,x30663)),f22(f6(f22(f6(a1,x30664),x30664),x30665),x30665))),
% 58.92/58.96 inference(scs_inference,[],[528,169,3059,3061,3063,3036,190,2997,2995,3044,2660,2654,122,127,71,75,59,63,3])).
% 58.92/58.96 cnf(3068,plain,
% 58.92/58.96 (P9(a1,f5(a1,x30681))),
% 58.92/58.96 inference(scs_inference,[],[490,528,169,3059,3061,3063,3036,190,2997,2995,3042,3044,2660,2654,122,127,71,75,59,63,3,50])).
% 58.92/58.96 cnf(3069,plain,
% 58.92/58.96 (P9(f22(f6(f22(f6(a1,x30691),x30691),x30692),x30692),f5(a1,x30693))),
% 58.92/58.96 inference(rename_variables,[],[3042])).
% 58.92/58.96 cnf(3071,plain,
% 58.92/58.96 (P1(f28(f24(f7(f30(x30711,a1,x30712)),f23(x30713,x30714)),x30713),f22(f6(f22(f6(a2,x30715),x30715),x30716),x30716))),
% 58.92/58.96 inference(scs_inference,[],[490,528,169,3059,3061,3063,3065,3036,190,2601,2997,2995,3042,3044,2660,2654,122,127,71,75,59,63,3,50,47])).
% 58.92/58.96 cnf(3072,plain,
% 58.92/58.96 (E(x30721,f22(f6(x30721,x30722),x30722))),
% 58.92/58.96 inference(rename_variables,[],[169])).
% 58.92/58.96 cnf(3073,plain,
% 58.92/58.96 (P9(f22(f6(f22(f6(a1,x30731),x30731),x30732),x30732),f22(f6(f5(a1,x30733),x30734),x30734))),
% 58.92/58.96 inference(scs_inference,[],[490,528,169,3059,3061,3063,3065,3072,3036,190,2601,2997,2995,3042,3069,3044,2660,2654,122,127,71,75,59,63,3,50,47,51])).
% 58.92/58.96 cnf(3075,plain,
% 58.92/58.96 (P1(f5(a1,x30751),f5(a1,x30752))),
% 58.92/58.96 inference(scs_inference,[],[363,490,528,169,3059,3061,3063,3065,3072,3036,190,2601,2997,2995,3042,3069,3044,3040,2660,2654,122,127,71,75,59,63,3,50,47,51,46])).
% 58.92/58.96 cnf(3081,plain,
% 58.92/58.96 (E(f22(f6(f5(a1,x30811),x30812),x30812),f22(f6(a1,x30813),x30813))),
% 58.92/58.96 inference(scs_inference,[],[363,490,528,169,3059,3061,3063,3065,3072,3036,190,2601,2997,2995,3042,3069,3044,3040,99,2660,2654,122,127,71,75,59,63,3,50,47,51,46,138,124,2])).
% 58.92/58.96 cnf(3086,plain,
% 58.92/58.96 (~P7(f22(f6(f5(a1,x30861),x30862),x30862))),
% 58.92/58.96 inference(scs_inference,[],[363,490,528,169,3059,3061,3063,3065,3072,2665,2999,3009,3036,190,2601,2997,2995,3042,3069,3044,3040,198,99,2660,2654,122,127,71,75,59,63,3,50,47,51,46,138,124,2,69,54,76,77,53])).
% 58.92/58.96 cnf(3091,plain,
% 58.92/58.96 (E(x30911,f28(f24(x30911,f23(x30912,x30913)),x30912))),
% 58.92/58.96 inference(rename_variables,[],[619])).
% 58.92/58.96 cnf(3093,plain,
% 58.92/58.96 (E(x30931,f28(f24(x30931,f23(x30932,x30933)),x30932))),
% 58.92/58.96 inference(rename_variables,[],[619])).
% 58.92/58.96 cnf(3094,plain,
% 58.92/58.96 (P8(f28(f24(f28(f24(f28(f24(a4,f23(x30941,x30942)),x30941),f23(x30943,x30944)),x30943),f23(x30945,x30946)),x30945),x30947)),
% 58.92/58.96 inference(scs_inference,[],[619,3091,3093,797,1890,1939,3071,122,55,56,60])).
% 58.92/58.96 cnf(3095,plain,
% 58.92/58.96 (E(x30951,f28(f24(x30951,f23(x30952,x30953)),x30952))),
% 58.92/58.96 inference(rename_variables,[],[619])).
% 58.92/58.96 cnf(3096,plain,
% 58.92/58.96 (P8(x30961,f28(f24(f28(f24(f26(f24(x30962,f23(x30963,a2)),x30963),f23(x30964,x30965)),x30964),f23(x30966,x30967)),x30966))),
% 58.92/58.96 inference(scs_inference,[],[619,3091,3093,3095,797,1890,1939,2044,3071,122,55,56,60,61])).
% 58.92/58.96 cnf(3097,plain,
% 58.92/58.96 (E(x30971,f28(f24(x30971,f23(x30972,x30973)),x30972))),
% 58.92/58.96 inference(rename_variables,[],[619])).
% 58.92/58.96 cnf(3099,plain,
% 58.92/58.96 (E(x30991,f28(f24(x30991,f23(x30992,x30993)),x30992))),
% 58.92/58.96 inference(rename_variables,[],[619])).
% 58.92/58.96 cnf(3101,plain,
% 58.92/58.96 (E(x31011,f28(f24(x31011,f23(x31012,x31013)),x31012))),
% 58.92/58.96 inference(rename_variables,[],[619])).
% 58.92/58.96 cnf(3103,plain,
% 58.92/58.96 (E(x31031,f28(f24(x31031,f23(x31032,x31033)),x31032))),
% 58.92/58.96 inference(rename_variables,[],[619])).
% 58.92/58.96 cnf(3104,plain,
% 58.92/58.96 (P4(f6(x31041,f22(f6(a1,x31042),x31042)),f28(f24(f5(a1,x31043),f23(x31044,x31045)),x31044))),
% 58.92/58.96 inference(scs_inference,[],[619,3091,3093,3095,3097,3099,3101,3103,797,1890,1939,2044,2997,2995,3071,2036,1982,122,55,56,60,61,75,71,59,63])).
% 58.92/58.96 cnf(3105,plain,
% 58.92/58.96 (E(x31051,f28(f24(x31051,f23(x31052,x31053)),x31052))),
% 58.92/58.96 inference(rename_variables,[],[619])).
% 58.92/58.96 cnf(3108,plain,
% 58.92/58.96 (P9(a1,f22(f6(f5(a1,x31081),x31082),x31082))),
% 58.92/58.96 inference(scs_inference,[],[490,619,3091,3093,3095,3097,3099,3101,3103,271,797,1890,3066,1939,2044,2997,2995,3071,3073,2036,1982,122,55,56,60,61,75,71,59,63,3,50])).
% 58.92/58.96 cnf(3110,plain,
% 58.92/58.96 (E(f22(f6(f22(f6(x31101,x31102),x31102),x31103),x31103),x31101)),
% 58.92/58.96 inference(rename_variables,[],[490])).
% 58.92/58.96 cnf(3112,plain,
% 58.92/58.96 (E(x31121,f28(f24(x31121,f23(x31122,x31123)),x31122))),
% 58.92/58.96 inference(rename_variables,[],[619])).
% 58.92/58.96 cnf(3113,plain,
% 58.92/58.96 (P9(f5(a1,x31131),a1)),
% 58.92/58.96 inference(scs_inference,[],[490,3110,619,3091,3093,3095,3097,3099,3101,3103,3105,271,797,1890,3066,1939,2044,2601,2997,2995,3071,3073,3038,2036,1982,122,55,56,60,61,75,71,59,63,3,50,47,51])).
% 58.92/58.96 cnf(3116,plain,
% 58.92/58.96 (P1(f28(f24(f7(f30(x31161,a1,x31162)),f23(x31163,x31164)),x31163),x31165)),
% 58.92/58.96 inference(scs_inference,[],[490,3110,619,3091,3093,3095,3097,3099,3101,3103,3105,3112,271,797,1890,3066,1939,2044,2813,2601,2997,2995,3071,3073,3038,2036,1982,122,55,56,60,61,75,71,59,63,3,50,47,51,46])).
% 58.92/58.96 cnf(3118,plain,
% 58.92/58.96 (P8(x31181,f28(f24(f7(f30(x31182,a1,x31183)),f23(x31184,x31185)),x31184))),
% 58.92/58.96 inference(scs_inference,[],[490,3110,619,3091,3093,3095,3097,3099,3101,3103,3105,3112,271,797,1890,3066,1939,2044,2813,2601,2997,2995,3071,3073,3038,2036,1982,122,55,56,60,61,75,71,59,63,3,50,47,51,46,137])).
% 58.92/58.96 cnf(3120,plain,
% 58.92/58.96 (E(f22(f6(a1,x31201),x31201),f28(f24(f5(a1,x31202),f23(x31203,x31204)),x31203))),
% 58.92/58.96 inference(scs_inference,[],[490,3110,619,3091,3093,3095,3097,3099,3101,3103,3105,3112,271,797,1890,3066,1939,2044,2813,2601,2997,2995,3071,3073,3038,2036,1982,100,122,55,56,60,61,75,71,59,63,3,50,47,51,46,137,148])).
% 58.92/58.96 cnf(3126,plain,
% 58.92/58.96 (E(f28(f24(f5(a1,x31261),f23(x31262,x31263)),x31262),f22(f6(a1,x31264),x31264))),
% 58.92/58.96 inference(scs_inference,[],[490,3110,619,3091,3093,3095,3097,3099,3101,3103,3105,3112,271,797,1890,3066,1939,2044,2813,2601,2997,2995,3071,3073,3038,2036,1982,100,122,55,56,60,61,75,71,59,63,3,50,47,51,46,137,148,124,2])).
% 58.92/58.96 cnf(3132,plain,
% 58.92/58.96 (E(f19(f6(f6(x31321,a2),f22(f6(a2,x31322),x31322)),a2),a2)),
% 58.92/58.96 inference(scs_inference,[],[216,206,116,131])).
% 58.92/58.96 cnf(3133,plain,
% 58.92/58.96 (E(a2,f19(f6(f6(x31331,a2),f22(f6(a2,x31332),x31332)),a2))),
% 58.92/58.96 inference(scs_inference,[],[3132,2])).
% 58.92/58.96 cnf(3137,plain,
% 58.92/58.96 (E(x31371,f22(f6(x31371,x31372),x31372))),
% 58.92/58.96 inference(rename_variables,[],[169])).
% 58.92/58.96 cnf(3139,plain,
% 58.92/58.96 (E(x31391,f22(f6(x31391,x31392),x31392))),
% 58.92/58.96 inference(rename_variables,[],[169])).
% 58.92/58.96 cnf(3141,plain,
% 58.92/58.96 (E(x31411,f22(f6(x31411,x31412),x31412))),
% 58.92/58.96 inference(rename_variables,[],[169])).
% 58.92/58.96 cnf(3144,plain,
% 58.92/58.96 (E(x31441,f22(f6(x31441,x31442),x31442))),
% 58.92/58.96 inference(rename_variables,[],[169])).
% 58.92/58.96 cnf(3146,plain,
% 58.92/58.96 (E(x31461,f22(f6(x31461,x31462),x31462))),
% 58.92/58.96 inference(rename_variables,[],[169])).
% 58.92/58.96 cnf(3148,plain,
% 58.92/58.96 (E(x31481,f22(f6(x31481,x31482),x31482))),
% 58.92/58.96 inference(rename_variables,[],[169])).
% 58.92/58.96 cnf(3149,plain,
% 58.92/58.96 (P1(f22(f6(a1,x31491),x31491),f22(f6(f5(a1,x31492),x31493),x31493))),
% 58.92/58.96 inference(scs_inference,[],[169,3137,3139,3141,3144,3146,3148,3009,3034,3001,3032,3007,3003,3005,3132,200,2686,2689,2,122,75,71,59,3,63,50,51,47])).
% 58.92/58.96 cnf(3150,plain,
% 58.92/58.96 (E(x31501,f22(f6(x31501,x31502),x31502))),
% 58.92/58.96 inference(rename_variables,[],[169])).
% 58.92/58.96 cnf(3153,plain,
% 58.92/58.96 (P1(f22(f6(f5(a1,x31531),x31532),x31532),f5(a1,x31533))),
% 58.92/58.96 inference(scs_inference,[],[169,3137,3139,3141,3144,3146,3148,3150,3009,3126,3034,3001,3032,3007,3003,3005,3075,3132,200,198,2686,2689,2,122,75,71,59,3,63,50,51,47,53,46])).
% 58.92/58.96 cnf(3155,plain,
% 58.92/58.96 (P8(f6(f6(x31551,x31552),a2),f19(f6(f6(x31553,a2),f22(f6(a2,x31554),x31554)),a2))),
% 58.92/58.96 inference(scs_inference,[],[169,3137,3139,3141,3144,3146,3148,3150,3009,3126,3034,3001,3032,3007,3003,3005,3075,3132,200,198,2686,2689,2,122,75,71,59,3,63,50,51,47,53,46,224])).
% 58.92/58.96 cnf(3156,plain,
% 58.92/58.96 (E(a1,f22(f6(f5(a1,x31561),x31562),x31562))),
% 58.92/58.96 inference(scs_inference,[],[169,3137,3139,3141,3144,3146,3148,3150,3009,3126,3034,3001,3032,3007,3003,3005,3075,3132,200,198,2686,2689,100,2,122,75,71,59,3,63,50,51,47,53,46,224,148])).
% 58.92/58.96 cnf(3161,plain,
% 58.92/58.96 (P1(f22(f6(f22(f6(a1,x31611),x31611),x31612),x31612),f22(f6(f5(a1,x31613),x31614),x31614))),
% 58.92/58.96 inference(scs_inference,[],[169,3137,3139,3141,3144,3146,3148,3150,3009,3126,371,3034,3001,3032,3007,3094,3003,3005,3075,3132,200,198,2686,2689,100,2,122,75,71,59,3,63,50,51,47,53,46,224,148,128,127])).
% 58.92/58.96 cnf(3174,plain,
% 58.92/58.96 (~E(f24(x31741,f23(x31742,x31743)),f22(f6(f5(a1,x31744),x31745),x31745))),
% 58.92/58.96 inference(scs_inference,[],[3081,3156,3036,371,3040,3153,2,122,127,3])).
% 58.92/58.96 cnf(3176,plain,
% 58.92/58.96 (P9(f5(a1,x31761),f22(f6(f5(a1,x31762),x31763),x31763))),
% 58.92/58.96 inference(scs_inference,[],[363,3081,3156,3036,371,3040,3153,3108,2,122,127,3,50])).
% 58.92/58.96 cnf(3177,plain,
% 58.92/58.96 (P9(f5(a1,x31771),f5(a1,x31772))),
% 58.92/58.96 inference(scs_inference,[],[363,3081,3156,3036,371,3040,3153,3108,3113,2,122,127,3,50,51])).
% 58.92/58.96 cnf(3178,plain,
% 58.92/58.96 (P1(f5(a1,x31781),a1)),
% 58.92/58.96 inference(scs_inference,[],[363,490,3081,3156,3036,371,3044,3040,3153,3108,3113,2,122,127,3,50,51,47])).
% 58.92/58.96 cnf(3180,plain,
% 58.92/58.96 (E(f22(f6(f22(f6(x31801,x31802),x31802),x31803),x31803),x31801)),
% 58.92/58.96 inference(rename_variables,[],[490])).
% 58.92/58.96 cnf(3181,plain,
% 58.92/58.96 (P1(a1,f22(f6(f5(a1,x31811),x31812),x31812))),
% 58.92/58.96 inference(scs_inference,[],[363,490,3180,3081,3156,3036,371,3044,3040,3153,3108,3113,3161,2,122,127,3,50,51,47,46])).
% 58.92/58.96 cnf(3194,plain,
% 58.92/58.96 (P1(f22(f6(f5(a1,x31941),x31942),x31942),a1)),
% 58.92/58.96 inference(scs_inference,[],[190,3075,3178,122,127])).
% 58.92/58.96 cnf(3200,plain,
% 58.92/58.96 (E(x32001,f22(f6(x32001,x32002),x32002))),
% 58.92/58.96 inference(rename_variables,[],[169])).
% 58.92/58.96 cnf(3201,plain,
% 58.92/58.96 (P1(f5(a1,x32011),f22(f6(f5(a1,x32012),x32013),x32013))),
% 58.92/58.96 inference(scs_inference,[],[169,3200,271,3174,190,3075,3176,3178,122,127,3,50,47])).
% 58.92/58.96 cnf(3202,plain,
% 58.92/58.96 (E(x32021,f22(f6(x32021,x32022),x32022))),
% 58.92/58.96 inference(rename_variables,[],[169])).
% 58.92/58.96 cnf(3203,plain,
% 58.92/58.96 (P1(f22(f6(f5(a1,x32031),x32032),x32032),f22(f6(f5(a1,x32033),x32034),x32034))),
% 58.92/58.96 inference(scs_inference,[],[169,3200,3202,271,3174,190,3075,3176,3178,122,127,3,50,47,46])).
% 58.92/58.96 cnf(3214,plain,
% 58.92/58.96 (P10(f28(f24(f28(f24(f30(a8,a13,a14),f23(x32141,x32142)),x32141),f23(x32143,x32144)),x32143),a15)),
% 58.92/58.96 inference(scs_inference,[],[619,1894,3116,122,55])).
% 58.92/58.96 cnf(3215,plain,
% 58.92/58.96 (E(x32151,f28(f24(x32151,f23(x32152,x32153)),x32152))),
% 58.92/58.96 inference(rename_variables,[],[619])).
% 58.92/58.96 cnf(3217,plain,
% 58.92/58.96 (E(x32171,f28(f24(x32171,f23(x32172,x32173)),x32172))),
% 58.92/58.96 inference(rename_variables,[],[619])).
% 58.92/58.96 cnf(3218,plain,
% 58.92/58.96 (P8(f28(f24(f28(f24(f17(f30(x32181,a1,x32182)),f23(x32183,x32184)),x32183),f23(x32185,x32186)),x32185),x32187)),
% 58.92/58.96 inference(scs_inference,[],[619,3215,3217,1894,2197,1974,3116,122,55,56,60])).
% 58.92/58.96 cnf(3219,plain,
% 58.92/58.96 (E(x32191,f28(f24(x32191,f23(x32192,x32193)),x32192))),
% 58.92/58.96 inference(rename_variables,[],[619])).
% 58.92/58.96 cnf(3221,plain,
% 58.92/58.96 (E(x32211,f28(f24(x32211,f23(x32212,x32213)),x32212))),
% 58.92/58.96 inference(rename_variables,[],[619])).
% 58.92/58.96 cnf(3227,plain,
% 58.92/58.96 (E(x32271,f28(f24(x32271,f23(x32272,x32273)),x32272))),
% 58.92/58.96 inference(rename_variables,[],[619])).
% 58.92/58.96 cnf(3228,plain,
% 58.92/58.96 (P6(f24(x32281,f23(a1,x32282)),f28(f24(f5(a1,x32283),f23(x32284,x32285)),x32284))),
% 58.92/58.96 inference(scs_inference,[],[619,3215,3217,3219,3221,3227,1894,2197,371,1974,3032,3116,3155,2068,3194,122,55,56,60,61,127,71,59])).
% 58.92/58.96 cnf(3229,plain,
% 58.92/58.96 (E(x32291,f28(f24(x32291,f23(x32292,x32293)),x32292))),
% 58.92/58.96 inference(rename_variables,[],[619])).
% 58.92/58.96 cnf(3231,plain,
% 58.92/58.96 (E(x32311,f28(f24(x32311,f23(x32312,x32313)),x32312))),
% 58.92/58.96 inference(rename_variables,[],[619])).
% 58.92/58.96 cnf(3232,plain,
% 58.92/58.96 (P4(f6(x32321,a1),f28(f24(f5(a1,x32322),f23(x32323,x32324)),x32323))),
% 58.92/58.96 inference(scs_inference,[],[619,3215,3217,3219,3221,3227,3229,3231,1894,2197,371,1974,3034,3032,3116,3155,2068,2048,3194,122,55,56,60,61,127,71,59,75,63])).
% 58.92/58.96 cnf(3233,plain,
% 58.92/58.96 (E(x32331,f28(f24(x32331,f23(x32332,x32333)),x32332))),
% 58.92/58.96 inference(rename_variables,[],[619])).
% 58.92/58.96 cnf(3238,plain,
% 58.92/58.96 (E(x32381,f28(f24(x32381,f23(x32382,x32383)),x32382))),
% 58.92/58.96 inference(rename_variables,[],[619])).
% 58.92/58.96 cnf(3239,plain,
% 58.92/58.96 (P9(f5(a1,x32391),f28(f24(f5(a1,x32392),f23(x32393,x32394)),x32393))),
% 58.92/58.96 inference(scs_inference,[],[528,619,3215,3217,3219,3221,3227,3229,3231,3233,3238,1894,3120,2197,371,1974,3034,3032,3116,3155,3177,2068,2048,3194,122,55,56,60,61,127,71,59,75,63,3,50,51])).
% 58.92/58.96 cnf(3240,plain,
% 58.92/58.96 (E(x32401,f28(f24(x32401,f23(x32402,x32403)),x32402))),
% 58.92/58.96 inference(rename_variables,[],[619])).
% 58.92/58.96 cnf(3241,plain,
% 58.92/58.96 (P1(f22(f6(a1,x32411),x32411),f28(f24(f5(a1,x32412),f23(x32413,x32414)),x32413))),
% 58.92/58.96 inference(scs_inference,[],[528,619,3215,3217,3219,3221,3227,3229,3231,3233,3238,3240,1894,3120,2197,371,1974,3034,3032,3001,3116,3155,3177,2068,2048,3194,122,55,56,60,61,127,71,59,75,63,3,50,51,47])).
% 58.92/58.96 cnf(3242,plain,
% 58.92/58.96 (E(x32421,f28(f24(x32421,f23(x32422,x32423)),x32422))),
% 58.92/58.96 inference(rename_variables,[],[619])).
% 58.92/58.96 cnf(3246,plain,
% 58.92/58.96 (E(a1,f28(f24(f5(a1,x32461),f23(x32462,x32463)),x32462))),
% 58.92/58.96 inference(scs_inference,[],[528,619,3215,3217,3219,3221,3227,3229,3231,3233,3238,3240,3242,1894,3120,2197,371,1974,3034,3032,3001,3007,3116,3155,3177,290,2068,2048,3194,122,55,56,60,61,127,71,59,75,63,3,50,51,47,46,2,138])).
% 58.92/58.96 cnf(3259,plain,
% 58.92/58.96 (P10(f28(f24(f28(f24(f30(a8,a13,a14),f23(x32591,x32592)),x32591),f23(x32593,x32594)),x32593),f22(f6(a15,x32595),x32595))),
% 58.92/58.96 inference(scs_inference,[],[619,1919,3246,3149,2,122,55])).
% 58.92/58.96 cnf(3260,plain,
% 58.92/58.96 (E(x32601,f28(f24(x32601,f23(x32602,x32603)),x32602))),
% 58.92/58.96 inference(rename_variables,[],[619])).
% 58.92/58.96 cnf(3262,plain,
% 58.92/58.96 (E(x32621,f28(f24(x32621,f23(x32622,x32623)),x32622))),
% 58.92/58.96 inference(rename_variables,[],[619])).
% 58.92/58.96 cnf(3264,plain,
% 58.92/58.96 (E(x32641,f28(f24(x32641,f23(x32642,x32643)),x32642))),
% 58.92/58.96 inference(rename_variables,[],[619])).
% 58.92/58.96 cnf(3265,plain,
% 58.92/58.96 (P8(x32651,f28(f24(f28(f24(a2,f23(x32652,x32653)),x32652),f23(x32654,x32655)),x32654))),
% 58.92/58.96 inference(scs_inference,[],[619,3260,3262,3264,1919,1945,3246,2072,3149,1984,2,122,55,56,60,61])).
% 58.92/58.96 cnf(3266,plain,
% 58.92/58.96 (E(x32661,f28(f24(x32661,f23(x32662,x32663)),x32662))),
% 58.92/58.96 inference(rename_variables,[],[619])).
% 58.92/58.96 cnf(3272,plain,
% 58.92/58.96 (E(x32721,f28(f24(x32721,f23(x32722,x32723)),x32722))),
% 58.92/58.96 inference(rename_variables,[],[619])).
% 58.92/58.96 cnf(3273,plain,
% 58.92/58.96 (P6(f24(x32731,f23(a1,x32732)),f28(f24(f28(f24(f5(a1,x32733),f23(x32734,x32735)),x32734),f23(x32736,x32737)),x32736))),
% 58.92/58.96 inference(scs_inference,[],[619,3260,3262,3264,3266,3272,1919,1945,3246,371,2072,3149,3241,3228,1984,2189,2,122,55,56,60,61,127,71,59])).
% 58.92/58.96 cnf(3274,plain,
% 58.92/58.96 (E(x32741,f28(f24(x32741,f23(x32742,x32743)),x32742))),
% 58.92/58.96 inference(rename_variables,[],[619])).
% 58.92/58.96 cnf(3276,plain,
% 58.92/58.96 (E(x32761,f28(f24(x32761,f23(x32762,x32763)),x32762))),
% 58.92/58.96 inference(rename_variables,[],[619])).
% 58.92/58.96 cnf(3278,plain,
% 58.92/58.96 (E(x32781,f28(f24(x32781,f23(x32782,x32783)),x32782))),
% 58.92/58.96 inference(rename_variables,[],[619])).
% 58.92/58.96 cnf(3282,plain,
% 58.92/58.96 (E(x32821,f28(f24(x32821,f23(x32822,x32823)),x32822))),
% 58.92/58.96 inference(rename_variables,[],[619])).
% 58.92/58.96 cnf(3283,plain,
% 58.92/58.96 (P9(f28(f24(f5(a1,x32831),f23(x32832,x32833)),x32832),f22(f6(f22(f6(a1,x32834),x32834),x32835),x32835))),
% 58.92/58.96 inference(scs_inference,[],[619,3260,3262,3264,3266,3272,3274,3276,3278,3282,1919,3126,1945,3246,3036,371,2072,3104,3149,3068,3038,3241,3228,1984,2189,2199,2,122,55,56,60,61,127,71,59,75,63,3,51,50])).
% 58.92/58.96 cnf(3284,plain,
% 58.92/58.96 (E(x32841,f28(f24(x32841,f23(x32842,x32843)),x32842))),
% 58.92/58.96 inference(rename_variables,[],[619])).
% 58.92/58.96 cnf(3285,plain,
% 58.92/58.96 (P1(a1,f28(f24(f5(a1,x32851),f23(x32852,x32853)),x32852))),
% 58.92/58.96 inference(scs_inference,[],[619,3260,3262,3264,3266,3272,3274,3276,3278,3282,3284,1919,3126,1945,3246,3036,371,2072,3104,3040,3149,3068,3038,3241,3228,1984,2189,2199,2,122,55,56,60,61,127,71,59,75,63,3,51,50,47])).
% 58.92/58.96 cnf(3286,plain,
% 58.92/58.96 (E(x32861,f28(f24(x32861,f23(x32862,x32863)),x32862))),
% 58.92/58.96 inference(rename_variables,[],[619])).
% 58.92/58.96 cnf(3287,plain,
% 58.92/58.96 (P1(f28(f24(f5(a1,x32871),f23(x32872,x32873)),x32872),f22(f6(f22(f6(a1,x32874),x32874),x32875),x32875))),
% 58.92/58.96 inference(scs_inference,[],[619,3260,3262,3264,3266,3272,3274,3276,3278,3282,3284,3286,1919,3126,1945,3246,3036,371,2072,3104,3044,3040,3149,3068,3038,3241,3228,1984,2189,2199,2,122,55,56,60,61,127,71,59,75,63,3,51,50,47,46])).
% 58.92/58.96 cnf(3289,plain,
% 58.92/58.96 (E(f22(f6(a1,x32891),x32891),f28(f24(f28(f24(f5(a1,x32892),f23(x32893,x32894)),x32893),f23(x32895,x32896)),x32895))),
% 58.92/58.96 inference(scs_inference,[],[619,3260,3262,3264,3266,3272,3274,3276,3278,3282,3284,3286,1919,3126,1945,3246,3036,371,2072,3104,3044,3040,3149,3068,3038,3241,3228,99,1984,2189,2199,2,122,55,56,60,61,127,71,59,75,63,3,51,50,47,46,138])).
% 58.92/58.96 cnf(3292,plain,
% 58.92/58.96 (E(a1,f28(f24(f28(f24(f5(a1,x32921),f23(x32922,x32923)),x32922),f23(x32924,x32925)),x32924))),
% 58.92/58.96 inference(scs_inference,[],[619,3260,3262,3264,3266,3272,3274,3276,3278,3282,3284,3286,1919,3126,1945,3246,3036,371,2072,3104,3044,3040,3149,3068,3038,3241,3228,99,1984,2189,2199,100,2,122,55,56,60,61,127,71,59,75,63,3,51,50,47,46,138,148])).
% 58.92/58.96 cnf(3308,plain,
% 58.92/58.96 (E(x33081,f22(f6(x33081,x33082),x33082))),
% 58.92/58.96 inference(rename_variables,[],[169])).
% 58.92/58.96 cnf(3311,plain,
% 58.92/58.96 (P9(f22(f6(f5(a1,x33111),x33112),x33112),a1)),
% 58.92/58.96 inference(scs_inference,[],[169,3308,3289,3036,3153,3232,3113,198,122,2,63,3,53,50])).
% 58.92/58.96 cnf(3313,plain,
% 58.92/58.96 (P9(f28(f24(f5(a1,x33131),f23(x33132,x33133)),x33132),a1)),
% 58.92/58.96 inference(scs_inference,[],[490,169,3308,3289,3036,3153,3232,3113,3283,198,122,2,63,3,53,50,51])).
% 58.92/58.96 cnf(3315,plain,
% 58.92/58.96 (E(f22(f6(f22(f6(x33151,x33152),x33152),x33153),x33153),x33151)),
% 58.92/58.96 inference(rename_variables,[],[490])).
% 58.92/58.96 cnf(3316,plain,
% 58.92/58.96 (P1(f28(f24(f5(a1,x33161),f23(x33162,x33163)),x33162),a1)),
% 58.92/58.96 inference(scs_inference,[],[490,3315,169,3308,3289,3036,3153,3232,3113,3283,3287,198,122,2,63,3,53,50,51,47])).
% 58.92/58.96 cnf(3319,plain,
% 58.92/58.96 (P1(f5(a1,x33191),f28(f24(f5(a1,x33192),f23(x33193,x33194)),x33193))),
% 58.92/58.96 inference(scs_inference,[],[363,490,3315,169,3308,3289,3036,3153,3232,3113,3283,3287,3285,198,122,2,63,3,53,50,51,47,46])).
% 58.92/58.96 cnf(3320,plain,
% 58.92/58.96 (E(a1,f22(f6(f28(f24(f5(a1,x33201),f23(x33202,x33203)),x33202),x33204),x33204))),
% 58.92/58.96 inference(scs_inference,[],[363,490,3315,169,3308,3289,3036,3153,3232,3113,3283,3287,3285,198,290,122,2,63,3,53,50,51,47,46,138])).
% 58.92/58.96 cnf(3339,plain,
% 58.92/58.96 (E(x33391,f28(f24(x33391,f23(x33392,x33393)),x33392))),
% 58.92/58.96 inference(rename_variables,[],[619])).
% 58.92/58.96 cnf(3341,plain,
% 58.92/58.96 (E(x33411,f28(f24(x33411,f23(x33412,x33413)),x33412))),
% 58.92/58.96 inference(rename_variables,[],[619])).
% 58.92/58.96 cnf(3343,plain,
% 58.92/58.96 (E(x33431,f28(f24(x33431,f23(x33432,x33433)),x33432))),
% 58.92/58.96 inference(rename_variables,[],[619])).
% 58.92/58.96 cnf(3345,plain,
% 58.92/58.96 (E(x33451,f28(f24(x33451,f23(x33452,x33453)),x33452))),
% 58.92/58.96 inference(rename_variables,[],[619])).
% 58.92/58.96 cnf(3350,plain,
% 58.92/58.96 (E(x33501,f28(f24(x33501,f23(x33502,x33503)),x33502))),
% 58.92/58.96 inference(rename_variables,[],[619])).
% 58.92/58.96 cnf(3351,plain,
% 58.92/58.96 (P6(f24(x33511,f23(a1,x33512)),f28(f24(f28(f24(f28(f24(f5(a1,x33513),f23(x33514,x33515)),x33514),f23(x33516,x33517)),x33516),f23(x33518,x33519)),x33518))),
% 58.92/58.96 inference(scs_inference,[],[619,3339,3341,3343,3345,3350,1943,3214,3292,190,3155,3178,3265,3273,3319,2660,122,2,55,56,60,61,127,71,59])).
% 58.92/58.96 cnf(3352,plain,
% 58.92/58.96 (E(x33521,f28(f24(x33521,f23(x33522,x33523)),x33522))),
% 58.92/58.96 inference(rename_variables,[],[619])).
% 58.92/58.96 cnf(3354,plain,
% 58.92/58.96 (E(x33541,f28(f24(x33541,f23(x33542,x33543)),x33542))),
% 58.92/58.96 inference(rename_variables,[],[619])).
% 58.92/58.96 cnf(3355,plain,
% 58.92/58.96 (P4(f6(x33551,a1),f28(f24(f28(f24(f5(a1,x33552),f23(x33553,x33554)),x33553),f23(x33555,x33556)),x33555))),
% 58.92/58.96 inference(scs_inference,[],[619,3339,3341,3343,3345,3350,3352,3354,1943,3214,3292,190,3155,3178,3232,3265,3273,3319,2660,2654,122,2,55,56,60,61,127,71,59,75,63])).
% 58.92/58.96 cnf(3356,plain,
% 58.92/58.96 (E(x33561,f28(f24(x33561,f23(x33562,x33563)),x33562))),
% 58.92/58.96 inference(rename_variables,[],[619])).
% 58.92/58.96 cnf(3357,plain,
% 58.92/58.96 (P9(f28(f24(f5(a1,x33571),f23(x33572,x33573)),x33572),f22(f6(f5(a1,x33574),x33575),x33575))),
% 58.92/58.96 inference(scs_inference,[],[619,3339,3341,3343,3345,3350,3352,3354,3356,1943,3214,3292,190,3155,3178,3232,3265,3273,3176,3319,2660,2654,122,2,55,56,60,61,127,71,59,75,63,50])).
% 58.92/58.96 cnf(3358,plain,
% 58.92/58.96 (E(x33581,f28(f24(x33581,f23(x33582,x33583)),x33582))),
% 58.92/58.96 inference(rename_variables,[],[619])).
% 58.92/58.96 cnf(3360,plain,
% 58.92/58.96 (E(x33601,f28(f24(x33601,f23(x33602,x33603)),x33602))),
% 58.92/58.96 inference(rename_variables,[],[619])).
% 58.92/58.96 cnf(3362,plain,
% 58.92/58.96 (E(x33621,f28(f24(x33621,f23(x33622,x33623)),x33622))),
% 58.92/58.96 inference(rename_variables,[],[619])).
% 58.92/58.96 cnf(3363,plain,
% 58.92/58.96 (P1(f28(f24(f5(a1,x33631),f23(x33632,x33633)),x33632),f5(a1,x33634))),
% 58.92/58.96 inference(scs_inference,[],[619,3339,3341,3343,3345,3350,3352,3354,3356,3358,3360,3362,1943,3214,3292,190,3155,3075,3178,3232,3265,3273,3241,3042,3176,3319,2660,2654,122,2,55,56,60,61,127,71,59,75,63,50,51,47,46])).
% 58.92/58.96 cnf(3377,plain,
% 58.92/58.96 (E(a1,f28(f24(f28(f24(f28(f24(f5(a1,x33771),f23(x33772,x33773)),x33772),f23(x33774,x33775)),x33774),f23(x33776,x33777)),x33776))),
% 58.92/58.96 inference(scs_inference,[],[3320,3201,3351,100,122,2,148])).
% 58.92/58.96 cnf(3403,plain,
% 58.92/58.96 (P9(f22(f6(f5(a1,x34031),x34032),x34032),f5(a1,x34033))),
% 58.92/58.96 inference(scs_inference,[],[169,3377,3203,3177,122,2,50])).
% 58.92/58.96 cnf(3426,plain,
% 58.92/58.96 (E(x34261,f28(f24(x34261,f23(x34262,x34263)),x34262))),
% 58.92/58.96 inference(rename_variables,[],[619])).
% 58.92/58.96 cnf(3428,plain,
% 58.92/58.96 (E(x34281,f28(f24(x34281,f23(x34282,x34283)),x34282))),
% 58.92/58.96 inference(rename_variables,[],[619])).
% 58.92/58.96 cnf(3429,plain,
% 58.92/58.96 (P8(x34291,f28(f24(f28(f24(f7(f30(x34292,a1,x34293)),f23(x34294,x34295)),x34294),f23(x34296,x34297)),x34296))),
% 58.92/58.96 inference(scs_inference,[],[619,3426,3428,3259,3181,3218,3118,122,55,60,61])).
% 58.92/58.96 cnf(3430,plain,
% 58.92/58.96 (E(x34301,f28(f24(x34301,f23(x34302,x34303)),x34302))),
% 58.92/58.96 inference(rename_variables,[],[619])).
% 58.92/58.96 cnf(3431,plain,
% 58.92/58.96 (P15(f6(x34311,a2),f28(f24(f7(f30(x34312,a1,x34313)),f23(x34314,x34315)),x34314))),
% 58.92/58.96 inference(scs_inference,[],[619,3426,3428,3430,3259,3181,3218,2689,3118,122,55,60,61,71])).
% 58.92/58.96 cnf(3432,plain,
% 58.92/58.96 (E(x34321,f28(f24(x34321,f23(x34322,x34323)),x34322))),
% 58.92/58.96 inference(rename_variables,[],[619])).
% 58.92/58.96 cnf(3433,plain,
% 58.92/58.96 (P19(f6(f6(x34331,a2),x34332),f28(f24(f7(f30(x34333,a1,x34334)),f23(x34335,x34336)),x34335))),
% 58.92/58.96 inference(scs_inference,[],[619,3426,3428,3430,3432,3259,3181,3218,2686,2689,3118,122,55,60,61,71,75])).
% 58.92/58.96 cnf(3434,plain,
% 58.92/58.96 (E(x34341,f28(f24(x34341,f23(x34342,x34343)),x34342))),
% 58.92/58.96 inference(rename_variables,[],[619])).
% 58.92/58.96 cnf(3436,plain,
% 58.92/58.96 (E(x34361,f28(f24(x34361,f23(x34362,x34363)),x34362))),
% 58.92/58.96 inference(rename_variables,[],[619])).
% 58.92/58.96 cnf(3438,plain,
% 58.92/58.96 (E(x34381,f28(f24(x34381,f23(x34382,x34383)),x34382))),
% 58.92/58.96 inference(rename_variables,[],[619])).
% 58.92/58.96 cnf(3439,plain,
% 58.92/58.96 (P1(a1,f28(f24(f28(f24(f5(a1,x34391),f23(x34392,x34393)),x34392),f23(x34394,x34395)),x34394))),
% 58.92/58.96 inference(scs_inference,[],[619,3426,3428,3430,3432,3434,3436,3438,3259,3181,3218,3355,3285,3005,2686,2689,3118,122,55,60,61,71,75,63,50,47])).
% 58.92/58.96 cnf(3440,plain,
% 58.92/58.96 (E(x34401,f28(f24(x34401,f23(x34402,x34403)),x34402))),
% 58.92/58.96 inference(rename_variables,[],[619])).
% 58.92/58.96 cnf(3441,plain,
% 58.92/58.96 (P9(f22(f6(a1,x34411),x34411),f28(f24(f5(a1,x34412),f23(x34413,x34414)),x34413))),
% 58.92/58.96 inference(scs_inference,[],[619,3426,3428,3430,3432,3434,3436,3438,3440,3259,3181,3218,3355,3285,3003,3005,2686,2689,3118,122,55,60,61,71,75,63,50,47,51])).
% 58.92/58.96 cnf(3472,plain,
% 58.92/58.96 (E(x34721,f28(f24(x34721,f23(x34722,x34723)),x34722))),
% 58.92/58.96 inference(rename_variables,[],[619])).
% 58.92/58.96 cnf(3474,plain,
% 58.92/58.96 (E(x34741,f28(f24(x34741,f23(x34742,x34743)),x34742))),
% 58.92/58.96 inference(rename_variables,[],[619])).
% 58.92/58.96 cnf(3476,plain,
% 58.92/58.96 (E(x34761,f28(f24(x34761,f23(x34762,x34763)),x34762))),
% 58.92/58.96 inference(rename_variables,[],[619])).
% 58.92/58.96 cnf(3478,plain,
% 58.92/58.96 (E(x34781,f28(f24(x34781,f23(x34782,x34783)),x34782))),
% 58.92/58.96 inference(rename_variables,[],[619])).
% 58.92/58.96 cnf(3480,plain,
% 58.92/58.96 (E(x34801,f28(f24(x34801,f23(x34802,x34803)),x34802))),
% 58.92/58.96 inference(rename_variables,[],[619])).
% 58.92/58.96 cnf(3482,plain,
% 58.92/58.96 (E(x34821,f28(f24(x34821,f23(x34822,x34823)),x34822))),
% 58.92/58.96 inference(rename_variables,[],[619])).
% 58.92/58.96 cnf(3484,plain,
% 58.92/58.96 (E(x34841,f28(f24(x34841,f23(x34842,x34843)),x34842))),
% 58.92/58.96 inference(rename_variables,[],[619])).
% 58.92/58.96 cnf(3485,plain,
% 58.92/58.96 (P1(f28(f24(f28(f24(f5(a1,x34851),f23(x34852,x34853)),x34852),f23(x34854,x34855)),x34854),a1)),
% 58.92/58.96 inference(scs_inference,[],[619,3472,3474,3476,3478,3480,3482,3484,3214,3285,3316,3363,3429,3357,3403,2603,2611,122,55,61,71,75,50,47,51,46])).
% 58.92/58.96 cnf(3546,plain,
% 58.92/58.96 (E(x35461,f28(f24(x35461,f23(x35462,x35463)),x35462))),
% 58.92/58.96 inference(rename_variables,[],[619])).
% 58.92/58.96 cnf(3548,plain,
% 58.92/58.96 (E(x35481,f28(f24(x35481,f23(x35482,x35483)),x35482))),
% 58.92/58.96 inference(rename_variables,[],[619])).
% 58.92/58.96 cnf(3550,plain,
% 58.92/58.96 (E(x35501,f28(f24(x35501,f23(x35502,x35503)),x35502))),
% 58.92/58.96 inference(rename_variables,[],[619])).
% 58.92/58.96 cnf(3551,plain,
% 58.92/58.96 (P9(f5(a1,x35511),f28(f24(f28(f24(f5(a1,x35512),f23(x35513,x35514)),x35513),f23(x35515,x35516)),x35515))),
% 58.92/58.96 inference(scs_inference,[],[619,3546,3548,3550,1945,3439,3239,3433,3431,122,55,71,75,51])).
% 58.92/58.96 cnf(3865,plain,
% 58.92/58.96 (~P17(f22(f6(a1,x38651),x38651),f22(f6(f5(a1,x38652),x38653),x38653))),
% 58.92/58.96 inference(scs_inference,[],[3029,122])).
% 58.92/58.96 cnf(4060,plain,
% 58.92/58.96 (P6(f24(x40601,f23(f22(f6(a2,x40602),x40602),x40603)),f7(f30(x40604,a1,x40605)))),
% 58.92/58.96 inference(scs_inference,[],[703,202,59])).
% 58.92/58.96 cnf(4062,plain,
% 58.92/58.96 (P4(f6(x40621,f22(f6(a2,x40622),x40622)),f7(f30(x40623,a1,x40624)))),
% 58.92/58.96 inference(scs_inference,[],[703,206,202,59,63])).
% 58.92/58.96 cnf(4076,plain,
% 58.92/58.96 (P6(f24(x40761,f23(a2,x40762)),f7(f30(x40763,a1,x40764)))),
% 58.92/58.96 inference(scs_inference,[],[703,168,59])).
% 58.92/58.96 cnf(4078,plain,
% 58.92/58.96 (E(f28(f24(f22(f6(f7(f30(x40781,a1,x40782)),x40783),x40783),f23(x40784,x40785)),x40784),f7(f30(x40786,a1,x40787)))),
% 58.92/58.96 inference(scs_inference,[],[703,407,168,59,3])).
% 58.92/58.96 cnf(4079,plain,
% 58.92/58.96 (P4(f6(x40791,a2),f7(f30(x40792,a1,x40793)))),
% 58.92/58.96 inference(scs_inference,[],[703,407,167,168,59,3,63])).
% 58.92/58.96 cnf(4096,plain,
% 58.92/58.96 (E(f22(f6(f7(f30(x40961,a1,x40962)),x40963),x40963),f7(f30(x40964,a1,x40965)))),
% 58.92/58.96 inference(scs_inference,[],[169,619,4078,4076,59,3])).
% 58.92/58.96 cnf(4126,plain,
% 58.92/58.96 (P4(f6(x41261,a2),f22(f6(f7(f30(x41262,a1,x41263)),x41264),x41264))),
% 58.92/58.96 inference(scs_inference,[],[169,4096,4079,2,63])).
% 58.92/58.96 cnf(4128,plain,
% 58.92/58.96 (P9(f7(f30(x41281,a1,x41282)),a2)),
% 58.92/58.96 inference(scs_inference,[],[703,169,4096,4079,81,2,63,50])).
% 58.92/58.96 cnf(4139,plain,
% 58.92/58.96 (E(x41391,f28(f24(x41391,f23(x41392,x41393)),x41392))),
% 58.92/58.96 inference(rename_variables,[],[619])).
% 58.92/58.96 cnf(4141,plain,
% 58.92/58.96 (E(x41411,f28(f24(x41411,f23(x41412,x41413)),x41412))),
% 58.92/58.96 inference(rename_variables,[],[619])).
% 58.92/58.96 cnf(4143,plain,
% 58.92/58.96 (E(x41431,f28(f24(x41431,f23(x41432,x41433)),x41432))),
% 58.92/58.96 inference(rename_variables,[],[619])).
% 58.92/58.96 cnf(4144,plain,
% 58.92/58.96 (P1(f28(f24(f28(f24(f28(f24(f5(a1,x41441),f23(x41442,x41443)),x41442),f23(x41444,x41445)),x41444),f23(x41446,x41447)),x41446),a1)),
% 58.92/58.96 inference(scs_inference,[],[619,4139,4141,4143,3485,3551,4062,4060,59,63,50,46])).
% 58.92/58.96 cnf(4145,plain,
% 58.92/58.96 (E(x41451,f28(f24(x41451,f23(x41452,x41453)),x41452))),
% 58.92/58.96 inference(rename_variables,[],[619])).
% 58.92/58.96 cnf(4148,plain,
% 58.92/58.96 (E(f22(f6(a2,x41481),x41481),f28(f24(f7(f30(x41482,a1,x41483)),f23(x41484,x41485)),x41484))),
% 58.92/58.96 inference(scs_inference,[],[619,4139,4141,4143,4145,3485,3441,3551,4062,4060,99,59,63,50,46,51,138])).
% 58.92/58.96 cnf(4165,plain,
% 58.92/58.96 (P9(f7(f30(x41651,a1,x41652)),f7(f30(x41653,a1,x41654)))),
% 58.92/58.96 inference(scs_inference,[],[703,363,169,4148,4144,4128,2,122,50,47,51])).
% 58.92/58.96 cnf(4177,plain,
% 58.92/58.96 (E(x41771,f28(f24(x41771,f23(x41772,x41773)),x41772))),
% 58.92/58.96 inference(rename_variables,[],[619])).
% 58.92/58.96 cnf(4178,plain,
% 58.92/58.96 (P4(f6(x41781,a2),f28(f24(f7(f30(x41782,a1,x41783)),f23(x41784,x41785)),x41784))),
% 58.92/58.96 inference(scs_inference,[],[619,4177,4079,4076,59,63])).
% 58.92/58.96 cnf(4381,plain,
% 58.92/58.96 (E(x43811,f28(f24(x43811,f23(x43812,x43813)),x43812))),
% 58.92/58.96 inference(rename_variables,[],[619])).
% 58.92/58.96 cnf(4382,plain,
% 58.92/58.96 (P4(f6(x43821,f16(f30(x43822,a1,x43823))),f28(f24(f16(f30(x43822,a1,x43824)),f23(x43825,x43826)),x43825))),
% 58.92/58.96 inference(scs_inference,[],[619,4381,2712,2858,59,63])).
% 58.92/58.96 cnf(4383,plain,
% 58.92/58.96 (E(x43831,f28(f24(x43831,f23(x43832,x43833)),x43832))),
% 58.92/58.96 inference(rename_variables,[],[619])).
% 58.92/58.96 cnf(4384,plain,
% 58.92/58.96 (P9(f28(f24(f16(f30(x43841,a1,x43842)),f23(x43843,x43844)),x43843),f16(f30(x43841,a1,x43845)))),
% 58.92/58.96 inference(scs_inference,[],[619,4381,4383,2712,2858,2725,59,63,50])).
% 58.92/58.96 cnf(4385,plain,
% 58.92/58.96 (E(x43851,f28(f24(x43851,f23(x43852,x43853)),x43852))),
% 58.92/58.96 inference(rename_variables,[],[619])).
% 58.92/58.96 cnf(4386,plain,
% 58.92/58.96 (P1(f30(x43861,a1,a3),f28(f24(f16(f30(x43861,a1,x43862)),f23(x43863,x43864)),x43863))),
% 58.92/58.96 inference(scs_inference,[],[619,4381,4383,4385,2712,2681,2858,2725,59,63,50,47])).
% 58.92/58.96 cnf(4387,plain,
% 58.92/58.96 (E(x43871,f28(f24(x43871,f23(x43872,x43873)),x43872))),
% 58.92/58.96 inference(rename_variables,[],[619])).
% 58.92/58.96 cnf(4388,plain,
% 58.92/58.96 (P9(f16(f30(x43881,a1,x43882)),f28(f24(f16(f30(x43881,a1,x43883)),f23(x43884,x43885)),x43884))),
% 58.92/58.96 inference(scs_inference,[],[619,4381,4383,4385,4387,2712,2681,2858,2725,59,63,50,47,51])).
% 58.92/58.96 cnf(4389,plain,
% 58.92/58.96 (E(x43891,f28(f24(x43891,f23(x43892,x43893)),x43892))),
% 58.92/58.96 inference(rename_variables,[],[619])).
% 58.92/58.96 cnf(4390,plain,
% 58.92/58.96 (P1(f28(f24(f16(f30(x43901,a1,x43902)),f23(x43903,x43904)),x43903),f30(x43901,a1,a3))),
% 58.92/58.96 inference(scs_inference,[],[619,4381,4383,4385,4387,4389,2712,2681,2677,2858,2725,59,63,50,47,51,46])).
% 58.92/58.96 cnf(4397,plain,
% 58.92/58.96 (E(f16(f30(x43971,a1,x43972)),f28(f24(f16(f30(x43971,a1,x43973)),f23(x43974,x43975)),x43974))),
% 58.92/58.96 inference(scs_inference,[],[619,4381,4383,4385,4387,4389,2712,2681,2677,2858,2725,290,100,59,63,50,47,51,46,122,148,138])).
% 58.92/58.96 cnf(4400,plain,
% 58.92/58.96 (P1(f22(f6(f30(x44001,a1,a3),x44002),x44002),f28(f24(f16(f30(x44001,a1,x44003)),f23(x44004,x44005)),x44004))),
% 58.92/58.96 inference(scs_inference,[],[619,4381,4383,4385,4387,4389,190,2712,2681,2677,2858,2725,290,100,59,63,50,47,51,46,122,148,138,127])).
% 58.92/58.96 cnf(4407,plain,
% 58.92/58.96 (E(f28(f24(f16(f30(x44071,a1,x44072)),f23(x44073,x44074)),x44073),f30(x44071,a1,a3))),
% 58.92/58.96 inference(scs_inference,[],[619,4381,4383,4385,4387,4389,190,2712,2681,2677,2858,2725,290,100,90,59,63,50,47,51,46,122,148,138,127,124,54,2])).
% 58.92/58.96 cnf(4417,plain,
% 58.92/58.96 (E(x44171,f22(f6(x44171,x44172),x44172))),
% 58.92/58.96 inference(rename_variables,[],[169])).
% 58.92/58.96 cnf(4418,plain,
% 58.92/58.96 (P1(f28(f24(f16(f30(x44181,a1,x44182)),f23(x44183,x44184)),x44183),f16(f30(x44181,a1,x44185)))),
% 58.92/58.96 inference(scs_inference,[],[640,169,4397,4388,4390,2,122,50,47])).
% 58.92/58.96 cnf(4427,plain,
% 58.92/58.96 (P1(f22(f6(f16(f30(x44271,a1,x44272)),x44273),x44273),f28(f24(f16(f30(x44271,a1,x44274)),f23(x44275,x44276)),x44275))),
% 58.92/58.96 inference(scs_inference,[],[640,169,4417,4397,4407,190,4384,4388,4390,4386,102,2,122,50,47,51,69,46,127])).
% 58.92/58.96 cnf(4531,plain,
% 58.92/58.96 (P1(f28(f24(f16(f30(x45311,a1,x45312)),f23(x45313,x45314)),x45313),f22(f6(f16(f30(x45311,a1,x45315)),x45316),x45316))),
% 58.92/58.96 inference(scs_inference,[],[169,4418,4427,122,47])).
% 58.92/58.96 cnf(4544,plain,
% 58.92/58.96 (E(x45441,f28(f24(x45441,f23(x45442,x45443)),x45442))),
% 58.92/58.96 inference(rename_variables,[],[619])).
% 58.92/58.96 cnf(4546,plain,
% 58.92/58.96 (E(x45461,f28(f24(x45461,f23(x45462,x45463)),x45462))),
% 58.92/58.96 inference(rename_variables,[],[619])).
% 58.92/58.96 cnf(4548,plain,
% 58.92/58.96 (E(x45481,f28(f24(x45481,f23(x45482,x45483)),x45482))),
% 58.92/58.96 inference(rename_variables,[],[619])).
% 58.92/58.96 cnf(4549,plain,
% 58.92/58.96 (P1(f28(f24(f16(f30(x45491,a1,x45492)),f23(x45493,x45494)),x45493),f22(f6(f30(x45491,a1,a3),x45495),x45495))),
% 58.92/58.96 inference(scs_inference,[],[619,4544,4546,4548,2903,2864,2690,2862,4531,122,59,63,50,46])).
% 58.92/58.96 cnf(4550,plain,
% 58.92/58.96 (E(x45501,f28(f24(x45501,f23(x45502,x45503)),x45502))),
% 58.92/58.96 inference(rename_variables,[],[619])).
% 58.92/58.96 cnf(4552,plain,
% 58.92/58.96 (E(x45521,f28(f24(x45521,f23(x45522,x45523)),x45522))),
% 58.92/58.96 inference(rename_variables,[],[619])).
% 58.92/58.96 cnf(4553,plain,
% 58.92/58.96 (P1(f5(a1,x45531),f28(f24(a1,f23(x45532,x45533)),x45532))),
% 58.92/58.96 inference(scs_inference,[],[619,4544,4546,4548,4550,4552,2903,2864,3178,2690,2860,2862,4531,122,59,63,50,46,51,47])).
% 58.92/58.96 cnf(4567,plain,
% 58.92/58.96 (P1(f5(a1,x45671),f22(f6(f28(f24(a1,f23(x45672,x45673)),x45672),x45674),x45674))),
% 58.92/58.96 inference(scs_inference,[],[169,4549,4553,122,47])).
% 58.92/58.96 cnf(4578,plain,
% 58.92/58.96 (P1(f28(f24(f28(f24(f16(f30(x45781,a1,x45782)),f23(x45783,x45784)),x45783),f23(x45785,x45786)),x45785),f30(x45781,a1,a3))),
% 58.92/58.96 inference(scs_inference,[],[619,4390,4553,122,46])).
% 58.92/58.96 cnf(4579,plain,
% 58.92/58.96 (E(x45791,f28(f24(x45791,f23(x45792,x45793)),x45792))),
% 58.92/58.96 inference(rename_variables,[],[619])).
% 58.92/58.96 cnf(4581,plain,
% 58.92/58.96 (E(x45811,f28(f24(x45811,f23(x45812,x45813)),x45812))),
% 58.92/58.96 inference(rename_variables,[],[619])).
% 58.92/58.96 cnf(4583,plain,
% 58.92/58.96 (E(x45831,f28(f24(x45831,f23(x45832,x45833)),x45832))),
% 58.92/58.96 inference(rename_variables,[],[619])).
% 58.92/58.96 cnf(4584,plain,
% 58.92/58.96 (P9(f28(f24(f7(f30(x45841,a1,x45842)),f23(x45843,x45844)),x45843),a2)),
% 58.92/58.96 inference(scs_inference,[],[619,4579,4581,4583,4128,4165,4386,4390,4553,122,46,51,47,50])).
% 58.92/58.96 cnf(4585,plain,
% 58.92/58.96 (E(x45851,f28(f24(x45851,f23(x45852,x45853)),x45852))),
% 58.92/58.96 inference(rename_variables,[],[619])).
% 58.92/58.96 cnf(4586,plain,
% 58.92/58.96 (P4(f6(x45861,f16(f30(x45862,a1,x45863))),f28(f24(f28(f24(f16(f30(x45862,a1,x45864)),f23(x45865,x45866)),x45865),f23(x45867,x45868)),x45867))),
% 58.92/58.96 inference(scs_inference,[],[619,4579,4581,4583,4585,4382,4128,4165,4386,4390,4553,122,46,51,47,50,63])).
% 58.92/58.96 cnf(4603,plain,
% 58.92/58.96 (P1(f26(f24(x46031,f23(x46032,f30(a8,a13,a14))),x46032),f30(a8,a13,a14))),
% 58.92/58.96 inference(scs_inference,[],[444,793,219,190,4567,122,71,127])).
% 58.92/58.96 cnf(4606,plain,
% 58.92/58.96 (P6(f24(x46061,f23(f22(f6(f5(a1,x46062),x46063),x46063),x46064)),a1)),
% 58.92/58.96 inference(scs_inference,[],[78,444,793,202,219,190,4567,122,71,127,59])).
% 58.92/58.96 cnf(4612,plain,
% 58.92/58.96 (P1(f28(f24(f22(f6(f7(f30(x46121,a1,x46122)),x46123),x46123),f23(x46124,x46125)),x46124),x46126)),
% 58.92/58.96 inference(scs_inference,[],[78,444,238,793,202,219,2813,190,4586,4567,290,122,71,127,59,138,46])).
% 58.92/58.96 cnf(4613,plain,
% 58.92/58.96 (E(x46131,f28(f24(f22(f6(x46131,x46132),x46132),f23(x46133,x46134)),x46133))),
% 58.92/58.96 inference(rename_variables,[],[238])).
% 58.92/58.96 cnf(4620,plain,
% 58.92/58.96 (P1(f5(a1,x46201),f26(f24(x46202,f23(x46203,f5(a1,x46204))),x46203))),
% 58.92/58.96 inference(scs_inference,[],[78,2999,444,238,4613,793,803,202,219,2679,2813,2653,3178,190,4586,4567,290,216,122,71,127,59,138,46,61,75,126,47])).
% 58.92/58.96 cnf(4625,plain,
% 58.92/58.96 (E(f5(a1,x46251),f28(f24(f28(f24(f28(f24(f5(a1,x46252),f23(x46253,x46254)),x46253),f23(x46255,x46256)),x46255),f23(x46257,x46258)),x46257))),
% 58.92/58.96 inference(scs_inference,[],[78,2999,444,238,4613,3377,793,803,202,219,2679,2813,2653,3178,263,421,190,4586,4567,290,216,122,71,127,59,138,46,61,75,126,47,51,50,3])).
% 58.92/58.96 cnf(4642,plain,
% 58.92/58.96 (P6(f24(x46421,f23(f5(a1,x46422),x46423)),a1)),
% 58.92/58.96 inference(scs_inference,[],[78,444,3010,4625,168,322,4612,210,2,122,71,46,59])).
% 58.92/58.96 cnf(4648,plain,
% 58.92/58.96 (P1(f28(f24(f5(a1,x46481),f23(x46482,x46483)),x46482),f26(f24(x46484,f23(x46485,f5(a1,x46486))),x46485))),
% 58.92/58.96 inference(scs_inference,[],[78,2999,444,3010,4625,803,168,2712,322,3316,4612,210,213,2,122,71,46,59,126,75,47])).
% 58.92/58.96 cnf(4653,plain,
% 58.92/58.96 (E(f5(a1,x46531),f22(f6(f28(f24(f5(a1,x46532),f23(x46533,x46534)),x46533),x46535),x46535))),
% 58.92/58.96 inference(scs_inference,[],[78,2999,444,3010,238,3320,4625,803,168,2712,2903,322,3316,409,4612,210,213,2,122,71,46,59,126,75,47,51,63,3])).
% 58.92/58.96 cnf(4667,plain,
% 58.92/58.96 (P15(f6(f6(x46671,a2),x46672),f28(f24(f22(f6(f22(f6(a2,x46673),x46673),x46674),x46674),f23(x46675,x46676)),x46675))),
% 58.92/58.96 inference(scs_inference,[],[238,4653,4578,242,2,122,71])).
% 58.92/58.96 cnf(4668,plain,
% 58.92/58.96 (E(x46681,f28(f24(f22(f6(x46681,x46682),x46682),f23(x46683,x46684)),x46683))),
% 58.92/58.96 inference(rename_variables,[],[238])).
% 58.92/58.96 cnf(4673,plain,
% 58.92/58.96 (E(x46731,f28(f24(f22(f6(x46731,x46732),x46732),f23(x46733,x46734)),x46733))),
% 58.92/58.96 inference(rename_variables,[],[238])).
% 58.92/58.96 cnf(4674,plain,
% 58.92/58.96 (P1(f26(f24(x46741,f23(x46742,f5(a1,x46743))),x46742),f22(f6(f5(a1,x46744),x46745),x46745))),
% 58.92/58.96 inference(scs_inference,[],[2999,238,4668,4653,803,2727,3181,4076,4578,242,2,122,71,126,59,46])).
% 58.92/58.96 cnf(4681,plain,
% 58.92/58.96 (E(f5(a1,x46811),f26(f24(x46812,f23(x46813,f22(f6(a1,x46814),x46814))),x46813))),
% 58.92/58.96 inference(scs_inference,[],[78,2999,3010,238,4668,4673,453,4653,803,2727,3181,348,4076,3113,4578,242,244,3194,2,122,71,126,59,46,75,47,51,63,3])).
% 58.92/58.96 cnf(4701,plain,
% 58.92/58.96 (E(x47011,f28(f24(f22(f6(x47011,x47012),x47012),f23(x47013,x47014)),x47013))),
% 58.92/58.96 inference(rename_variables,[],[238])).
% 58.92/58.96 cnf(4702,plain,
% 58.92/58.96 (P1(f26(f24(x47021,f23(x47022,f5(a1,x47023))),x47022),f5(a1,x47024))),
% 58.92/58.96 inference(scs_inference,[],[2999,238,4681,803,2997,3040,4620,405,2,122,126,71,46])).
% 58.92/58.96 cnf(4707,plain,
% 58.92/58.96 (P19(f6(x47071,a2),f28(f24(f22(f6(f22(f6(a2,x47072),x47072),x47073),x47073),f23(x47074,x47075)),x47074))),
% 58.92/58.96 inference(scs_inference,[],[2999,3081,238,4701,4681,803,2997,3040,3311,4620,4642,4674,405,411,2,122,126,71,46,59,51,47,75])).
% 58.92/58.96 cnf(4712,plain,
% 58.92/58.96 (E(f22(f6(a1,x47121),x47121),f28(f24(f28(f24(f28(f24(f5(a1,x47122),f23(x47123,x47124)),x47123),f23(x47125,x47126)),x47125),f23(x47127,x47128)),x47127))),
% 58.92/58.96 inference(scs_inference,[],[78,2999,3010,3081,238,4701,4625,4681,803,2997,3040,206,3311,4620,4642,4674,417,405,411,2,122,126,71,46,59,51,47,75,53,63,3])).
% 58.92/58.96 cnf(4735,plain,
% 58.92/58.96 (P4(f6(x47351,a2),f28(f24(f22(f6(f7(f30(x47352,a1,x47353)),x47354),x47354),f23(x47355,x47356)),x47355))),
% 58.92/58.96 inference(scs_inference,[],[78,2999,238,4712,803,275,3285,4079,3313,4648,4702,2,122,126,46,51,47,63])).
% 58.92/58.96 cnf(4737,plain,
% 58.92/58.96 (E(f28(f24(f22(f6(a2,x47371),x47371),f23(x47372,x47373)),x47372),f28(f24(f7(f30(x47374,a1,x47375)),f23(x47376,x47377)),x47376))),
% 58.92/58.96 inference(scs_inference,[],[78,2999,271,238,4148,4712,803,275,3285,4079,3313,4648,4702,2,122,126,46,51,47,63,3])).
% 58.92/58.96 cnf(4801,plain,
% 58.92/58.96 (P1(f26(f24(x48011,f23(x48012,a2)),x48012),x48013)),
% 58.92/58.96 inference(scs_inference,[],[4737,803,206,4674,122,2,126])).
% 58.92/58.96 cnf(5274,plain,
% 58.92/58.96 (E(f28(f24(f22(f6(a2,x52741),x52741),f23(x52742,x52743)),x52742),f28(f24(f22(f6(a2,x52744),x52744),f23(x52745,x52746)),x52745))),
% 58.92/58.96 inference(scs_inference,[],[737,765,3])).
% 58.92/58.96 cnf(5316,plain,
% 58.92/58.96 (E(f28(f24(f22(f6(a2,x53161),x53161),f23(x53162,x53163)),x53162),f19(f6(f6(x53164,a2),f22(f6(a2,x53165),x53165)),a2))),
% 58.92/58.96 inference(scs_inference,[],[3133,184,3])).
% 58.92/58.96 cnf(5553,plain,
% 58.92/58.96 (E(f22(f6(x55531,x55532),x55532),x55531)),
% 58.92/58.96 inference(rename_variables,[],[83])).
% 58.92/58.96 cnf(5555,plain,
% 58.92/58.96 (E(f22(f6(x55551,x55552),x55552),x55551)),
% 58.92/58.96 inference(rename_variables,[],[83])).
% 58.92/58.96 cnf(5557,plain,
% 58.92/58.96 (E(f22(f6(x55571,x55572),x55572),x55571)),
% 58.92/58.96 inference(rename_variables,[],[83])).
% 58.92/58.96 cnf(5559,plain,
% 58.92/58.96 (P4(f6(x55591,a2),f22(f6(f7(f30(x55592,a1,x55593)),x55594),x55594))),
% 58.92/58.96 inference(rename_variables,[],[4126])).
% 58.92/58.96 cnf(5560,plain,
% 58.92/58.96 (P8(x55601,f22(f6(f7(f30(x55602,a1,x55603)),x55604),x55604))),
% 58.92/58.96 inference(rename_variables,[],[2818])).
% 58.92/58.96 cnf(5563,plain,
% 58.92/58.96 (P4(f6(x55631,a2),f22(f6(f7(f30(x55632,a1,x55633)),x55634),x55634))),
% 58.92/58.96 inference(rename_variables,[],[4126])).
% 58.92/58.96 cnf(5564,plain,
% 58.92/58.96 (P8(x55641,f22(f6(f7(f30(x55642,a1,x55643)),x55644),x55644))),
% 58.92/58.96 inference(rename_variables,[],[2818])).
% 58.92/58.96 cnf(5575,plain,
% 58.92/58.96 (~P12(a1,x55751,x55752)),
% 58.92/58.96 inference(rename_variables,[],[101])).
% 58.92/58.96 cnf(5584,plain,
% 58.92/58.96 (P6(f24(x55841,f23(a1,x55842)),f5(a1,x55843))),
% 58.92/58.96 inference(rename_variables,[],[3032])).
% 58.92/58.96 cnf(5591,plain,
% 58.92/58.96 (P6(f24(x55911,f23(x55912,x55913)),x55912)),
% 58.92/58.96 inference(rename_variables,[],[168])).
% 58.92/58.96 cnf(5597,plain,
% 58.92/58.96 (~P6(a1,x55971)),
% 58.92/58.96 inference(rename_variables,[],[100])).
% 58.92/58.96 cnf(5600,plain,
% 58.92/58.96 (E(f22(f6(x56001,x56002),x56002),x56001)),
% 58.92/58.96 inference(rename_variables,[],[83])).
% 58.92/58.96 cnf(5605,plain,
% 58.92/58.96 (E(f22(f6(x56051,x56052),x56052),x56051)),
% 58.92/58.96 inference(rename_variables,[],[83])).
% 58.92/58.96 cnf(5610,plain,
% 58.92/58.96 (E(f22(f6(x56101,x56102),x56102),x56101)),
% 58.92/58.96 inference(rename_variables,[],[83])).
% 58.92/58.96 cnf(5615,plain,
% 58.92/58.96 (E(x56151,f22(f6(f22(f6(x56151,x56152),x56152),x56153),x56153))),
% 58.92/58.96 inference(rename_variables,[],[463])).
% 58.92/58.96 cnf(5629,plain,
% 58.92/58.96 ($false),
% 58.92/58.96 inference(scs_inference,[],[91,179,101,5575,623,835,418,3086,643,3865,4584,1051,867,1947,5274,4667,4707,4606,4735,3096,4126,5559,5563,499,2818,5560,5564,4549,4400,4801,4178,3118,381,4603,3032,5584,384,5316,83,5553,5555,5557,5600,5605,5610,463,5615,94,168,5591,167,100,5597,200,764,1038,103,104,105,119,120,121,133,134,135,147,153,13,20,21,24,27,38,43,140,143,4,5,6,7,12,14,15,16,17,18,19,22,23,25,26,28,29,30,31,32,33,34,35,36,37,39,40,41,42,44,45,139,8,9,10,144,152,149,166,117,11,628,114,113,112,2,64,65,72,66,130,131,132,136,146,156,157,141,145,151,159,127,148,58,138,62,126,59,69,53,52,3,63,57,161,118,154,165]),
% 58.92/58.96 ['proof']).
% 58.92/58.96 % SZS output end Proof
% 58.92/58.96 % Total time :58.360000s
%------------------------------------------------------------------------------