%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : SWV381+1 : TPTP v8.2.0. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% Computer : n029.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Mon Jun 24 16:47:02 EDT 2024
% Result : Theorem 59.87s 59.93s
% Output : CNFRefutation 59.96s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : SWV381+1 : TPTP v8.2.0. Released v3.3.0.
% 0.07/0.12 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% 0.13/0.33 % Computer : n029.cluster.edu
% 0.13/0.33 % Model : x86_64 x86_64
% 0.13/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.33 % Memory : 8042.1875MB
% 0.13/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.33 % CPULimit : 300
% 0.13/0.33 % WCLimit : 300
% 0.13/0.33 % DateTime : Thu Jun 20 14:31:24 EDT 2024
% 0.13/0.33 % CPUTime :
% 0.47/0.57 start to proof:theBenchmark
% 59.87/59.91 %-------------------------------------------
% 59.87/59.91 % File :CSE---1.7
% 59.87/59.91 % Problem :theBenchmark
% 59.87/59.91 % Transform :cnf
% 59.87/59.91 % Format :tptp:raw
% 59.87/59.91 % Command :java -jar mcs_scs.jar %d %s
% 59.87/59.91
% 59.87/59.91 % Result :Theorem 59.280000s
% 59.87/59.91 % Output :CNFRefutation 59.280000s
% 59.87/59.91 %-------------------------------------------
% 59.87/59.93 %------------------------------------------------------------------------------
% 59.87/59.93 % File : SWV381+1 : TPTP v8.2.0. Released v3.3.0.
% 59.87/59.93 % Domain : Software Verification
% 59.87/59.93 % Problem : Priority queue checker: lemma_min_elem_smallest
% 59.87/59.93 % Version : [dNP05] axioms.
% 59.87/59.93 % English :
% 59.87/59.93
% 59.87/59.93 % Refs : [Pis06] Piskac (2006), Email to Geoff Sutcliffe
% 59.87/59.93 % : [dNP05] de Nivelle & Piskac (2005), Verification of an Off-Lin
% 59.87/59.93 % Source : [Pis06]
% 59.87/59.93 % Names : cpq_l017 [Pis06]
% 59.87/59.93
% 59.87/59.93 % Status : Theorem
% 59.87/59.93 % Rating : 0.28 v8.2.0, 0.33 v8.1.0, 0.25 v7.4.0, 0.30 v7.3.0, 0.28 v7.2.0, 0.24 v7.1.0, 0.26 v7.0.0, 0.23 v6.4.0, 0.27 v6.3.0, 0.25 v6.2.0, 0.28 v6.1.0, 0.30 v6.0.0, 0.26 v5.5.0, 0.37 v5.4.0, 0.46 v5.3.0, 0.52 v5.2.0, 0.35 v5.1.0, 0.33 v5.0.0, 0.42 v4.1.0, 0.48 v4.0.0, 0.50 v3.5.0, 0.58 v3.3.0
% 59.87/59.93 % Syntax : Number of formulae : 65 ( 23 unt; 0 def)
% 59.87/59.93 % Number of atoms : 135 ( 40 equ)
% 59.87/59.93 % Maximal formula atoms : 4 ( 2 avg)
% 59.87/59.93 % Number of connectives : 87 ( 17 ~; 4 |; 22 &)
% 59.87/59.93 % ( 17 <=>; 27 =>; 0 <=; 0 <~>)
% 59.87/59.93 % Maximal formula depth : 9 ( 5 avg)
% 59.87/59.93 % Maximal term depth : 5 ( 1 avg)
% 59.87/59.93 % Number of predicates : 21 ( 19 usr; 1 prp; 0-3 aty)
% 59.87/59.93 % Number of functors : 26 ( 26 usr; 4 con; 0-3 aty)
% 59.87/59.93 % Number of variables : 174 ( 170 !; 4 ?)
% 59.87/59.93 % SPC : FOF_THM_RFO_SEQ
% 59.87/59.93
% 59.87/59.93 % Comments :
% 59.87/59.93 %------------------------------------------------------------------------------
% 59.87/59.93 %----Include the axioms about priority queues and checked priority queues
% 59.87/59.93 include('Axioms/SWV007+0.ax').
% 59.87/59.93 include('Axioms/SWV007+1.ax').
% 59.87/59.93 include('Axioms/SWV007+2.ax').
% 59.87/59.93 include('Axioms/SWV007+3.ax').
% 59.87/59.93 include('Axioms/SWV007+4.ax').
% 59.87/59.93 %------------------------------------------------------------------------------
% 59.87/59.93 %----lemma_contains_s_I (cpq_l005.p, cpq_l006.p)
% 59.87/59.93 fof(l17_li56,lemma,
% 59.87/59.93 ! [U,V,W,X] :
% 59.87/59.93 ( contains_cpq(triple(U,V,W),X)
% 59.87/59.93 <=> contains_pq(i(triple(U,V,W)),X) ) ).
% 59.87/59.93
% 59.87/59.93 %----lemma_not_min_elem_not_phi (cpq_l018.p)
% 59.87/59.93 fof(l17_l18,lemma,
% 59.87/59.93 ! [U,V,W] :
% 59.87/59.93 ( ? [X] :
% 59.87/59.93 ( contains_cpq(triple(U,V,W),X)
% 59.87/59.93 & strictly_less_than(X,findmin_cpq_res(triple(U,V,W))) )
% 59.87/59.93 => ~ phi(findmin_cpq_eff(triple(U,V,W))) ) ).
% 59.87/59.93
% 59.87/59.93 %----lemma_min_elem_smallest (conjecture)
% 59.87/59.93 fof(l17_co,conjecture,
% 59.87/59.93 ! [U,V,W] :
% 59.87/59.93 ( phi(findmin_cpq_eff(triple(U,V,W)))
% 59.87/59.93 => issmallestelement_pq(i(triple(U,V,W)),findmin_cpq_res(triple(U,V,W))) ) ).
% 59.87/59.93
% 59.87/59.93 %------------------------------------------------------------------------------
% 59.87/59.93 %-------------------------------------------
% 59.87/59.93 % Proof found
% 59.87/59.93 % SZS status Theorem for theBenchmark
% 59.87/59.93 % SZS output start Proof
% 59.93/59.94 %ClaNum:166(EqnAxiom:77)
% 59.93/59.94 %VarNum:490(SingletonVarNum:232)
% 59.93/59.94 %MaxLitNum:4
% 59.93/59.95 %MaxfuncDepth:4
% 59.93/59.95 %SharedTerms:15
% 59.93/59.95 %goalClause: 92 101
% 59.93/59.95 %singleGoalClaCount:2
% 59.93/59.95 [95]~P2(a4)
% 59.93/59.95 [96]~P7(a1)
% 59.93/59.95 [92]P10(f8(f29(a9,a14,a15)))
% 59.93/59.95 [101]~P8(f16(f29(a9,a14,a15)),f7(f29(a9,a14,a15)))
% 59.93/59.95 [79]P1(a2,x791)
% 59.93/59.95 [80]P1(x801,x801)
% 59.93/59.95 [81]P9(x811,x811)
% 59.93/59.95 [97]~P4(a4,x971)
% 59.93/59.95 [98]~P6(a1,x981)
% 59.93/59.95 [78]E(f5(a1,x781),a1)
% 59.93/59.95 [99]~P11(a1,x991,x992)
% 59.93/59.95 [82]P2(f6(x821,x822))
% 59.93/59.95 [90]P3(f29(x901,a1,x902))
% 59.93/59.95 [100]~P12(f29(x1001,x1002,a3))
% 59.93/59.95 [83]E(f21(f6(x831,x832),x832),x831)
% 59.93/59.95 [88]E(f7(f29(x881,a1,x882)),a2)
% 59.93/59.95 [89]E(f16(f29(x891,a1,x892)),a4)
% 59.93/59.95 [91]E(f8(f29(x911,a1,x912)),f29(x911,a1,a3))
% 59.93/59.95 [84]E(f6(f6(x841,x842),x843),f6(f6(x841,x843),x842))
% 59.93/59.95 [85]P7(f23(x851,f22(x852,x853)))
% 59.93/59.95 [86]E(f27(f23(x861,f22(x862,x863)),x862),x861)
% 59.93/59.95 [87]E(f25(f23(x871,f22(x872,x873)),x872),x873)
% 59.93/59.95 [93]E(f29(f24(x931,x932),f23(x933,f22(x932,a2)),x934),f20(f29(x931,x933,x934),x932))
% 59.93/59.95 [94]E(f16(f29(x941,f23(x942,f22(x943,x944)),x945)),f6(f16(f29(x941,x942,x945)),x943))
% 59.93/59.95 [102]~P10(x1021)+P3(f10(x1021))
% 59.93/59.95 [103]~P10(x1031)+P12(f10(x1031))
% 59.93/59.95 [104]~P10(x1041)+P9(x1041,f10(x1041))
% 59.93/59.95 [106]~P14(x1061)+P13(f16(x1061),f11(x1061))
% 59.93/59.95 [107]~P15(x1071)+P13(f16(x1071),f13(x1071))
% 59.93/59.95 [105]P1(x1052,x1051)+P1(x1051,x1052)
% 59.93/59.95 [110]~P17(x1101,x1102)+P1(x1101,x1102)
% 59.93/59.95 [111]~P18(x1111,x1112)+P4(x1111,x1112)
% 59.93/59.95 [112]~P13(x1121,x1122)+P4(x1121,x1122)
% 59.93/59.95 [113]~P19(x1131,x1132)+P4(x1131,x1132)
% 59.93/59.95 [114]~P13(x1141,x1142)+P8(x1141,x1142)
% 59.93/59.95 [115]~P19(x1151,x1152)+P8(x1151,x1152)
% 59.93/59.95 [116]~P4(x1161,x1162)+P18(x1161,x1162)
% 59.93/59.95 [121]~P17(x1212,x1211)+~P1(x1211,x1212)
% 59.93/59.95 [108]P14(x1081)+~P13(f16(x1081),x1082)
% 59.93/59.95 [109]P15(x1091)+~P13(f16(x1091),x1092)
% 59.93/59.95 [118]~P9(x1181,x1182)+P9(x1181,f8(x1182))
% 59.93/59.95 [119]~P16(x1191,x1192)+P18(f16(x1191),x1192)
% 59.93/59.95 [122]P16(x1221,x1222)+~P18(f16(x1221),x1222)
% 59.93/59.95 [124]P8(x1241,x1242)+P4(x1241,f12(x1241,x1242))
% 59.93/59.95 [136]P8(x1361,x1362)+~P1(x1362,f12(x1361,x1362))
% 59.93/59.95 [138]~P9(x1381,x1382)+P9(x1381,f26(f8(x1382),f7(x1382)))
% 59.93/59.95 [120]~E(x1202,x1203)+P4(f6(x1201,x1202),x1203)
% 59.93/59.95 [132]~P9(x1321,x1322)+P9(x1321,f20(x1322,x1323))
% 59.93/59.95 [133]~P9(x1331,x1332)+P9(x1331,f26(x1332,x1333))
% 59.93/59.95 [134]~P4(x1341,x1343)+P4(f6(x1341,x1342),x1343)
% 59.93/59.95 [141]E(x1411,a3)+P12(f29(x1412,x1413,x1411))
% 59.93/59.95 [143]E(x1431,a1)+E(f7(f29(x1432,x1431,x1433)),f19(x1432))
% 59.93/59.95 [146]~P6(x1462,x1464)+P5(f29(x1461,x1462,x1463),x1464)
% 59.93/59.95 [152]P6(x1521,x1522)+~P5(f29(x1523,x1521,x1524),x1522)
% 59.93/59.95 [139]~E(x1392,x1394)+P6(f23(x1391,f22(x1392,x1393)),x1394)
% 59.93/59.95 [142]~P6(x1421,x1424)+P6(f23(x1421,f22(x1422,x1423)),x1424)
% 59.93/59.95 [151]P6(x1512,x1514)+E(f26(f29(x1511,x1512,x1513),x1514),f29(x1511,x1512,a3))
% 59.93/59.95 [161]~P5(f29(x1611,x1612,x1613),x1614)+P4(f16(f29(x1611,x1612,x1613)),x1614)
% 59.93/59.95 [164]P5(f29(x1641,x1642,x1643),x1644)+~P4(f16(f29(x1641,x1642,x1643)),x1644)
% 59.93/59.95 [148]~P1(x1482,x1484)+E(f23(f5(x1481,x1482),f22(x1483,x1484)),f5(f23(x1481,f22(x1483,x1484)),x1482))
% 59.93/59.95 [149]~P17(x1493,x1494)+E(f5(f23(x1491,f22(x1492,x1493)),x1494),f23(f5(x1491,x1494),f22(x1492,x1494)))
% 59.93/59.95 [153]~P11(x1531,x1534,x1535)+P11(f23(x1531,f22(x1532,x1533)),x1534,x1535)
% 59.93/59.95 [162]~P17(x1621,x1622)+~P3(f29(x1623,f23(x1624,f22(x1621,x1622)),x1625))
% 59.93/59.95 [123]P17(x1232,x1231)+~P1(x1232,x1231)+P1(x1231,x1232)
% 59.93/59.95 [127]~P4(x1271,x1272)+~P8(x1271,x1272)+P13(x1271,x1272)
% 59.93/59.95 [128]~P4(x1281,x1282)+~P8(x1281,x1282)+P19(x1281,x1282)
% 59.93/59.95 [129]~P4(x1291,x1292)+~P8(x1291,x1292)+E(f17(x1291,x1292),x1291)
% 59.93/59.95 [130]~P4(x1301,x1302)+~P8(x1301,x1302)+E(f18(x1301,x1302),x1302)
% 59.93/59.95 [131]~P4(x1311,x1312)+~P8(x1311,x1312)+E(f30(x1311,x1312),x1312)
% 59.93/59.95 [135]~P4(x1351,x1352)+~P8(x1351,x1352)+E(f31(x1351,x1352),f21(x1351,x1352))
% 59.93/59.95 [125]~P8(x1253,x1251)+P1(x1251,x1252)+~P4(x1253,x1252)
% 59.93/59.95 [126]~P1(x1261,x1263)+P1(x1261,x1262)+~P1(x1263,x1262)
% 59.93/59.95 [137]E(x1371,x1372)+P4(x1373,x1372)+~P4(f6(x1373,x1371),x1372)
% 59.93/59.95 [140]~P4(x1403,x1401)+E(x1401,x1402)+E(f21(f6(x1403,x1402),x1401),f6(f21(x1403,x1401),x1402))
% 59.93/59.95 [154]P6(x1541,f19(x1542))+E(x1541,a1)+E(f8(f29(x1542,x1541,x1543)),f29(x1542,f5(x1541,f19(x1542)),a3))
% 59.93/59.95 [147]E(x1471,x1472)+P6(x1473,x1472)+~P6(f23(x1473,f22(x1471,x1474)),x1472)
% 59.93/59.95 [157]~P6(x1572,x1574)+~P17(x1574,f25(x1572,x1574))+E(f26(f29(x1571,x1572,x1573),x1574),f29(f28(x1571,x1574),f27(x1572,x1574),a3))
% 59.93/59.95 [158]~P6(x1583,x1582)+~P1(f25(x1583,x1582),x1582)+E(f29(f28(x1581,x1582),f27(x1583,x1582),x1584),f26(f29(x1581,x1583,x1584),x1582))
% 59.93/59.95 [166]~P5(f29(x1661,x1662,x1663),x1664)+~P17(x1664,f7(f29(x1661,x1662,x1663)))+~P10(f8(f29(x1661,x1662,x1663)))
% 59.93/59.95 [144]~P6(x1443,x1442)+E(x1441,x1442)+E(f25(f23(x1443,f22(x1441,x1444)),x1442),f25(x1443,x1442))
% 59.93/59.95 [150]~P6(x1503,x1502)+E(x1501,x1502)+E(f27(f23(x1503,f22(x1501,x1504)),x1502),f23(f27(x1503,x1502),f22(x1501,x1504)))
% 59.93/59.95 [145]~E(x1453,x1455)+~E(x1452,x1454)+P11(f23(x1451,f22(x1452,x1453)),x1454,x1455)
% 59.93/59.95 [155]E(x1551,x1552)+P11(x1553,x1554,x1552)+~P11(f23(x1553,f22(x1555,x1551)),x1554,x1552)
% 59.93/59.95 [156]E(x1561,x1562)+P11(x1563,x1562,x1564)+~P11(f23(x1563,f22(x1561,x1565)),x1562,x1564)
% 59.93/59.95 [163]~P1(x1634,x1633)+~P3(f29(x1631,x1632,x1635))+P3(f29(x1631,f23(x1632,f22(x1633,x1634)),x1635))
% 59.93/59.95 [165]~P1(x1654,x1655)+P3(f29(x1651,x1652,x1653))+~P3(f29(x1651,f23(x1652,f22(x1655,x1654)),x1653))
% 59.93/59.95 [117]~P12(x1172)+~P9(x1171,x1172)+P10(x1171)+~P3(x1172)
% 59.93/59.95 [159]~P6(x1591,f19(x1592))+E(x1591,a1)+~P17(f19(x1592),f25(x1591,f19(x1592)))+E(f8(f29(x1592,x1591,x1593)),f29(x1592,f5(x1591,f19(x1592)),a3))
% 59.93/59.95 [160]~P6(x1601,f19(x1602))+E(x1601,a1)+~P1(f25(x1601,f19(x1602)),f19(x1602))+E(f29(x1602,f5(x1601,f19(x1602)),x1603),f8(f29(x1602,x1601,x1603)))
% 59.93/59.95 %EqnAxiom
% 59.93/59.95 [1]E(x11,x11)
% 59.93/59.95 [2]E(x22,x21)+~E(x21,x22)
% 59.93/59.95 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 59.93/59.95 [4]~E(x41,x42)+E(f5(x41,x43),f5(x42,x43))
% 59.93/59.95 [5]~E(x51,x52)+E(f5(x53,x51),f5(x53,x52))
% 59.93/59.95 [6]~E(x61,x62)+E(f6(x61,x63),f6(x62,x63))
% 59.93/59.95 [7]~E(x71,x72)+E(f6(x73,x71),f6(x73,x72))
% 59.93/59.95 [8]~E(x81,x82)+E(f22(x81,x83),f22(x82,x83))
% 59.93/59.95 [9]~E(x91,x92)+E(f22(x93,x91),f22(x93,x92))
% 59.93/59.95 [10]~E(x101,x102)+E(f21(x101,x103),f21(x102,x103))
% 59.93/59.95 [11]~E(x111,x112)+E(f21(x113,x111),f21(x113,x112))
% 59.93/59.95 [12]~E(x121,x122)+E(f29(x121,x123,x124),f29(x122,x123,x124))
% 59.93/59.95 [13]~E(x131,x132)+E(f29(x133,x131,x134),f29(x133,x132,x134))
% 59.93/59.95 [14]~E(x141,x142)+E(f29(x143,x144,x141),f29(x143,x144,x142))
% 59.93/59.95 [15]~E(x151,x152)+E(f16(x151),f16(x152))
% 59.93/59.95 [16]~E(x161,x162)+E(f27(x161,x163),f27(x162,x163))
% 59.93/59.95 [17]~E(x171,x172)+E(f27(x173,x171),f27(x173,x172))
% 59.93/59.95 [18]~E(x181,x182)+E(f28(x181,x183),f28(x182,x183))
% 59.93/59.95 [19]~E(x191,x192)+E(f28(x193,x191),f28(x193,x192))
% 59.93/59.95 [20]~E(x201,x202)+E(f25(x201,x203),f25(x202,x203))
% 59.93/59.95 [21]~E(x211,x212)+E(f25(x213,x211),f25(x213,x212))
% 59.93/59.95 [22]~E(x221,x222)+E(f23(x221,x223),f23(x222,x223))
% 59.93/59.95 [23]~E(x231,x232)+E(f23(x233,x231),f23(x233,x232))
% 59.93/59.95 [24]~E(x241,x242)+E(f19(x241),f19(x242))
% 59.93/59.95 [25]~E(x251,x252)+E(f26(x251,x253),f26(x252,x253))
% 59.93/59.95 [26]~E(x261,x262)+E(f26(x263,x261),f26(x263,x262))
% 59.93/59.95 [27]~E(x271,x272)+E(f7(x271),f7(x272))
% 59.93/59.95 [28]~E(x281,x282)+E(f8(x281),f8(x282))
% 59.93/59.95 [29]~E(x291,x292)+E(f20(x291,x293),f20(x292,x293))
% 59.93/59.95 [30]~E(x301,x302)+E(f20(x303,x301),f20(x303,x302))
% 59.93/59.95 [31]~E(x311,x312)+E(f10(x311),f10(x312))
% 59.93/59.95 [32]~E(x321,x322)+E(f11(x321),f11(x322))
% 59.93/59.95 [33]~E(x331,x332)+E(f18(x331,x333),f18(x332,x333))
% 59.93/59.95 [34]~E(x341,x342)+E(f18(x343,x341),f18(x343,x342))
% 59.93/59.95 [35]~E(x351,x352)+E(f30(x351,x353),f30(x352,x353))
% 59.93/59.95 [36]~E(x361,x362)+E(f30(x363,x361),f30(x363,x362))
% 59.93/59.95 [37]~E(x371,x372)+E(f12(x371,x373),f12(x372,x373))
% 59.93/59.95 [38]~E(x381,x382)+E(f12(x383,x381),f12(x383,x382))
% 59.93/59.95 [39]~E(x391,x392)+E(f13(x391),f13(x392))
% 59.93/59.95 [40]~E(x401,x402)+E(f24(x401,x403),f24(x402,x403))
% 59.93/59.95 [41]~E(x411,x412)+E(f24(x413,x411),f24(x413,x412))
% 59.93/59.95 [42]~E(x421,x422)+E(f17(x421,x423),f17(x422,x423))
% 59.93/59.95 [43]~E(x431,x432)+E(f17(x433,x431),f17(x433,x432))
% 59.93/59.95 [44]~E(x441,x442)+E(f31(x441,x443),f31(x442,x443))
% 59.93/59.95 [45]~E(x451,x452)+E(f31(x453,x451),f31(x453,x452))
% 59.93/59.95 [46]P1(x462,x463)+~E(x461,x462)+~P1(x461,x463)
% 59.93/59.95 [47]P1(x473,x472)+~E(x471,x472)+~P1(x473,x471)
% 59.93/59.95 [48]P17(x482,x483)+~E(x481,x482)+~P17(x481,x483)
% 59.93/59.95 [49]P17(x493,x492)+~E(x491,x492)+~P17(x493,x491)
% 59.93/59.95 [50]P9(x502,x503)+~E(x501,x502)+~P9(x501,x503)
% 59.93/59.95 [51]P9(x513,x512)+~E(x511,x512)+~P9(x513,x511)
% 59.93/59.95 [52]~P2(x521)+P2(x522)+~E(x521,x522)
% 59.93/59.95 [53]~P7(x531)+P7(x532)+~E(x531,x532)
% 59.93/59.95 [54]~P3(x541)+P3(x542)+~E(x541,x542)
% 59.93/59.95 [55]~P10(x551)+P10(x552)+~E(x551,x552)
% 59.93/59.95 [56]P11(x562,x563,x564)+~E(x561,x562)+~P11(x561,x563,x564)
% 59.93/59.95 [57]P11(x573,x572,x574)+~E(x571,x572)+~P11(x573,x571,x574)
% 59.93/59.95 [58]P11(x583,x584,x582)+~E(x581,x582)+~P11(x583,x584,x581)
% 59.93/59.95 [59]P4(x592,x593)+~E(x591,x592)+~P4(x591,x593)
% 59.93/59.95 [60]P4(x603,x602)+~E(x601,x602)+~P4(x603,x601)
% 59.93/59.95 [61]P6(x612,x613)+~E(x611,x612)+~P6(x611,x613)
% 59.93/59.95 [62]P6(x623,x622)+~E(x621,x622)+~P6(x623,x621)
% 59.93/59.95 [63]P8(x632,x633)+~E(x631,x632)+~P8(x631,x633)
% 59.93/59.95 [64]P8(x643,x642)+~E(x641,x642)+~P8(x643,x641)
% 59.93/59.95 [65]P18(x652,x653)+~E(x651,x652)+~P18(x651,x653)
% 59.93/59.95 [66]P18(x663,x662)+~E(x661,x662)+~P18(x663,x661)
% 59.93/59.95 [67]~P12(x671)+P12(x672)+~E(x671,x672)
% 59.93/59.95 [68]P16(x682,x683)+~E(x681,x682)+~P16(x681,x683)
% 59.93/59.95 [69]P16(x693,x692)+~E(x691,x692)+~P16(x693,x691)
% 59.93/59.95 [70]P5(x702,x703)+~E(x701,x702)+~P5(x701,x703)
% 59.93/59.95 [71]P5(x713,x712)+~E(x711,x712)+~P5(x713,x711)
% 59.93/59.95 [72]P19(x722,x723)+~E(x721,x722)+~P19(x721,x723)
% 59.93/59.95 [73]P19(x733,x732)+~E(x731,x732)+~P19(x733,x731)
% 59.93/59.95 [74]~P15(x741)+P15(x742)+~E(x741,x742)
% 59.93/59.95 [75]P13(x752,x753)+~E(x751,x752)+~P13(x751,x753)
% 59.93/59.95 [76]P13(x763,x762)+~E(x761,x762)+~P13(x763,x761)
% 59.93/59.95 [77]~P14(x771)+P14(x772)+~E(x771,x772)
% 59.93/59.95
% 59.93/59.95 %-------------------------------------------
% 59.96/59.97 cnf(167,plain,
% 59.96/59.97 (P4(f6(x1672,x1671),x1671)),
% 59.96/59.97 inference(equality_inference,[],[120])).
% 59.96/59.97 cnf(168,plain,
% 59.96/59.97 (P6(f23(x1682,f22(x1681,x1683)),x1681)),
% 59.96/59.97 inference(equality_inference,[],[139])).
% 59.96/59.97 cnf(169,plain,
% 59.96/59.97 (~P13(f16(f29(a9,a14,a15)),f7(f29(a9,a14,a15)))),
% 59.96/59.97 inference(scs_inference,[],[101,114])).
% 59.96/59.97 cnf(171,plain,
% 59.96/59.97 (~P19(f16(f29(a9,a14,a15)),f7(f29(a9,a14,a15)))),
% 59.96/59.97 inference(scs_inference,[],[101,114,115])).
% 59.96/59.97 cnf(174,plain,
% 59.96/59.97 (~P4(a4,x1741)),
% 59.96/59.97 inference(rename_variables,[],[97])).
% 59.96/59.97 cnf(176,plain,
% 59.96/59.97 (P8(x1761,a2)),
% 59.96/59.97 inference(scs_inference,[],[101,79,97,114,115,124,136])).
% 59.96/59.97 cnf(177,plain,
% 59.96/59.97 (P1(a2,x1771)),
% 59.96/59.97 inference(rename_variables,[],[79])).
% 59.96/59.97 cnf(179,plain,
% 59.96/59.97 (E(x1791,f21(f6(x1791,x1792),x1792))),
% 59.96/59.97 inference(scs_inference,[],[101,79,97,83,114,115,124,136,2])).
% 59.96/59.97 cnf(180,plain,
% 59.96/59.97 (~P18(a4,x1801)),
% 59.96/59.97 inference(scs_inference,[],[101,79,97,174,83,114,115,124,136,2,111])).
% 59.96/59.97 cnf(182,plain,
% 59.96/59.97 (~P13(a4,x1821)),
% 59.96/59.97 inference(scs_inference,[],[101,79,97,174,83,114,115,124,136,2,111,112])).
% 59.96/59.97 cnf(189,plain,
% 59.96/59.97 (~E(a4,f16(f29(a9,a14,a15)))),
% 59.96/59.97 inference(scs_inference,[],[92,101,79,177,97,174,83,114,115,124,136,2,111,112,113,121,55,63])).
% 59.96/59.97 cnf(190,plain,
% 59.96/59.97 (~E(a2,f7(f29(a9,a14,a15)))),
% 59.96/59.97 inference(scs_inference,[],[92,101,79,177,97,174,83,114,115,124,136,2,111,112,113,121,55,63,64])).
% 59.96/59.97 cnf(191,plain,
% 59.96/59.97 (E(f27(f23(f21(f6(f8(f29(a9,a14,a15)),x1911),x1911),f22(x1912,x1913)),x1912),f8(f29(a9,a14,a15)))),
% 59.96/59.97 inference(scs_inference,[],[92,101,79,177,97,174,83,86,114,115,124,136,2,111,112,113,121,55,63,64,3])).
% 59.96/59.97 cnf(192,plain,
% 59.96/59.97 (E(f21(f6(x1921,x1922),x1922),x1921)),
% 59.96/59.97 inference(rename_variables,[],[83])).
% 59.96/59.97 cnf(194,plain,
% 59.96/59.97 (P1(x1941,f21(f6(x1941,x1942),x1942))),
% 59.96/59.97 inference(scs_inference,[],[92,101,79,177,97,174,83,192,86,80,114,115,124,136,2,111,112,113,121,55,63,64,3,46])).
% 59.96/59.97 cnf(195,plain,
% 59.96/59.97 (P1(x1951,x1951)),
% 59.96/59.97 inference(rename_variables,[],[80])).
% 59.96/59.97 cnf(196,plain,
% 59.96/59.97 (P1(f21(f6(x1961,x1962),x1962),x1961)),
% 59.96/59.97 inference(scs_inference,[],[92,101,79,177,97,174,83,192,86,80,195,114,115,124,136,2,111,112,113,121,55,63,64,3,46,47])).
% 59.96/59.97 cnf(198,plain,
% 59.96/59.97 (P9(x1981,f21(f6(x1981,x1982),x1982))),
% 59.96/59.97 inference(scs_inference,[],[92,101,81,79,177,97,174,83,192,86,80,195,114,115,124,136,2,111,112,113,121,55,63,64,3,46,47,50])).
% 59.96/59.97 cnf(199,plain,
% 59.96/59.97 (P9(x1991,x1991)),
% 59.96/59.97 inference(rename_variables,[],[81])).
% 59.96/59.97 cnf(200,plain,
% 59.96/59.97 (P9(f21(f6(x2001,x2002),x2002),x2001)),
% 59.96/59.97 inference(scs_inference,[],[92,101,81,199,79,177,97,174,83,192,86,80,195,114,115,124,136,2,111,112,113,121,55,63,64,3,46,47,50,51])).
% 59.96/59.97 cnf(202,plain,
% 59.96/59.97 (~E(f6(x2021,x2022),a4)),
% 59.96/59.97 inference(scs_inference,[],[92,101,81,199,79,177,97,174,83,192,86,80,195,167,114,115,124,136,2,111,112,113,121,55,63,64,3,46,47,50,51,59])).
% 59.96/59.97 cnf(203,plain,
% 59.96/59.97 (P4(f6(x2031,x2032),x2032)),
% 59.96/59.97 inference(rename_variables,[],[167])).
% 59.96/59.97 cnf(204,plain,
% 59.96/59.97 (P4(f6(x2041,f21(f6(x2042,x2043),x2043)),x2042)),
% 59.96/59.97 inference(scs_inference,[],[92,101,81,199,79,177,97,174,83,192,86,80,195,167,203,114,115,124,136,2,111,112,113,121,55,63,64,3,46,47,50,51,59,60])).
% 59.96/59.97 cnf(205,plain,
% 59.96/59.97 (P4(f6(x2051,x2052),x2052)),
% 59.96/59.97 inference(rename_variables,[],[167])).
% 59.96/59.97 cnf(206,plain,
% 59.96/59.97 (~P12(f21(f6(f29(x2061,x2062,a3),x2063),x2063))),
% 59.96/59.97 inference(scs_inference,[],[92,101,81,199,79,177,97,174,83,192,86,80,195,167,203,100,114,115,124,136,2,111,112,113,121,55,63,64,3,46,47,50,51,59,60,67])).
% 59.96/59.97 cnf(207,plain,
% 59.96/59.97 (E(f21(f6(x2071,x2072),x2072),x2071)),
% 59.96/59.97 inference(rename_variables,[],[83])).
% 59.96/59.97 cnf(208,plain,
% 59.96/59.97 (~P2(f21(f6(a4,x2081),x2081))),
% 59.96/59.97 inference(scs_inference,[],[92,101,81,199,79,177,97,174,83,192,207,86,80,195,167,203,100,95,114,115,124,136,2,111,112,113,121,55,63,64,3,46,47,50,51,59,60,67,52])).
% 59.96/59.97 cnf(209,plain,
% 59.96/59.98 (E(f21(f6(x2091,x2092),x2092),x2091)),
% 59.96/59.98 inference(rename_variables,[],[83])).
% 59.96/59.98 cnf(210,plain,
% 59.96/59.98 (~P7(f21(f6(a1,x2101),x2101))),
% 59.96/59.98 inference(scs_inference,[],[92,101,81,199,79,177,97,174,83,192,207,209,86,80,195,167,203,100,95,96,114,115,124,136,2,111,112,113,121,55,63,64,3,46,47,50,51,59,60,67,52,53])).
% 59.96/59.98 cnf(211,plain,
% 59.96/59.98 (E(f21(f6(x2111,x2112),x2112),x2111)),
% 59.96/59.98 inference(rename_variables,[],[83])).
% 59.96/59.98 cnf(212,plain,
% 59.96/59.98 (~E(f23(x2121,f22(x2122,x2123)),a1)),
% 59.96/59.98 inference(scs_inference,[],[92,101,81,199,79,177,97,174,83,192,207,209,86,80,195,167,203,168,100,98,95,96,114,115,124,136,2,111,112,113,121,55,63,64,3,46,47,50,51,59,60,67,52,53,61])).
% 59.96/59.98 cnf(213,plain,
% 59.96/59.98 (P6(f23(x2131,f22(x2132,x2133)),x2132)),
% 59.96/59.98 inference(rename_variables,[],[168])).
% 59.96/59.98 cnf(214,plain,
% 59.96/59.98 (P6(f23(x2141,f22(f21(f6(x2142,x2143),x2143),x2144)),x2142)),
% 59.96/59.98 inference(scs_inference,[],[92,101,81,199,79,177,97,174,83,192,207,209,211,86,80,195,167,203,168,213,100,98,95,96,114,115,124,136,2,111,112,113,121,55,63,64,3,46,47,50,51,59,60,67,52,53,61,62])).
% 59.96/59.98 cnf(218,plain,
% 59.96/59.98 (~P8(f6(x2181,x2182),x2183)+P1(x2183,x2182)),
% 59.96/59.98 inference(scs_inference,[],[92,101,81,199,79,177,97,174,83,192,207,209,211,86,80,195,167,203,205,168,213,100,98,95,96,114,115,124,136,2,111,112,113,121,55,63,64,3,46,47,50,51,59,60,67,52,53,61,62,166,125])).
% 59.96/59.98 cnf(231,plain,
% 59.96/59.98 (E(f8(f29(a9,a14,a15)),f27(f23(f21(f6(f8(f29(a9,a14,a15)),x2311),x2311),f22(x2312,x2313)),x2312))),
% 59.96/59.98 inference(scs_inference,[],[194,191,121,2])).
% 59.96/59.98 cnf(232,plain,
% 59.96/59.98 (P1(f21(f6(x2321,x2322),x2322),f21(f6(x2321,x2323),x2323))),
% 59.96/59.98 inference(scs_inference,[],[194,196,191,121,2,126])).
% 59.96/59.98 cnf(233,plain,
% 59.96/59.98 (P1(x2331,f21(f6(x2331,x2332),x2332))),
% 59.96/59.98 inference(rename_variables,[],[194])).
% 59.96/59.98 cnf(235,plain,
% 59.96/59.98 (P9(f21(f6(x2351,x2352),x2352),f21(f6(x2351,x2353),x2353))),
% 59.96/59.98 inference(scs_inference,[],[179,194,196,198,191,121,2,126,50])).
% 59.96/59.98 cnf(236,plain,
% 59.96/59.98 (P9(x2361,f21(f6(x2361,x2362),x2362))),
% 59.96/59.98 inference(rename_variables,[],[198])).
% 59.96/59.98 cnf(237,plain,
% 59.96/59.98 (P7(f21(f6(f23(x2371,f22(x2372,x2373)),x2374),x2374))),
% 59.96/59.98 inference(scs_inference,[],[179,194,196,198,191,85,121,2,126,50,53])).
% 59.96/59.98 cnf(238,plain,
% 59.96/59.98 (E(x2381,f21(f6(x2381,x2382),x2382))),
% 59.96/59.98 inference(rename_variables,[],[179])).
% 59.96/59.98 cnf(239,plain,
% 59.96/59.98 (P1(f21(f6(f21(f6(x2391,x2392),x2392),x2393),x2393),x2391)),
% 59.96/59.98 inference(scs_inference,[],[179,238,194,196,198,191,85,121,2,126,50,53,46])).
% 59.96/59.98 cnf(240,plain,
% 59.96/59.98 (E(x2401,f21(f6(x2401,x2402),x2402))),
% 59.96/59.98 inference(rename_variables,[],[179])).
% 59.96/59.98 cnf(241,plain,
% 59.96/59.98 (P4(f6(x2411,f21(f6(x2412,x2413),x2413)),f21(f6(x2412,x2414),x2414))),
% 59.96/59.98 inference(scs_inference,[],[179,238,240,194,196,198,204,191,85,121,2,126,50,53,46,60])).
% 59.96/59.98 cnf(243,plain,
% 59.96/59.98 (P1(x2431,f21(f6(f21(f6(x2431,x2432),x2432),x2433),x2433))),
% 59.96/59.98 inference(scs_inference,[],[179,238,240,194,233,196,198,204,191,85,121,2,126,50,53,46,60,47])).
% 59.96/59.98 cnf(244,plain,
% 59.96/59.98 (E(x2441,f21(f6(x2441,x2442),x2442))),
% 59.96/59.98 inference(rename_variables,[],[179])).
% 59.96/59.98 cnf(245,plain,
% 59.96/59.98 (P9(x2451,f21(f6(f21(f6(x2451,x2452),x2452),x2453),x2453))),
% 59.96/59.98 inference(scs_inference,[],[179,238,240,244,194,233,196,198,236,204,191,85,121,2,126,50,53,46,60,47,51])).
% 59.96/59.98 cnf(246,plain,
% 59.96/59.98 (E(x2461,f21(f6(x2461,x2462),x2462))),
% 59.96/59.98 inference(rename_variables,[],[179])).
% 59.96/59.98 cnf(251,plain,
% 59.96/59.98 (P2(f21(f6(f6(x2511,x2512),x2513),x2513))),
% 59.96/59.98 inference(scs_inference,[],[92,179,238,240,244,246,194,233,196,198,236,204,191,91,100,82,85,121,2,126,50,53,46,60,47,51,67,55,52])).
% 59.96/59.98 cnf(252,plain,
% 59.96/59.98 (E(x2521,f21(f6(x2521,x2522),x2522))),
% 59.96/59.98 inference(rename_variables,[],[179])).
% 59.96/59.98 cnf(253,plain,
% 59.96/59.98 (P3(f21(f6(f29(x2531,a1,x2532),x2533),x2533))),
% 59.96/59.98 inference(scs_inference,[],[92,179,238,240,244,246,252,194,233,196,198,236,204,191,91,90,100,82,85,121,2,126,50,53,46,60,47,51,67,55,52,54])).
% 59.96/59.98 cnf(254,plain,
% 59.96/59.98 (E(x2541,f21(f6(x2541,x2542),x2542))),
% 59.96/59.98 inference(rename_variables,[],[179])).
% 59.96/59.98 cnf(255,plain,
% 59.96/59.98 (~E(f23(x2551,f22(x2552,x2553)),f5(a1,x2554))),
% 59.96/59.98 inference(scs_inference,[],[92,179,238,240,244,246,252,194,233,196,198,236,204,191,78,91,212,90,100,82,85,121,2,126,50,53,46,60,47,51,67,55,52,54,3])).
% 59.96/59.98 cnf(258,plain,
% 59.96/59.98 (E(f21(f6(x2581,x2582),x2582),f21(f6(x2581,x2583),x2583))),
% 59.96/59.98 inference(scs_inference,[],[92,179,238,240,244,246,252,254,194,233,196,198,236,204,191,78,91,214,212,90,100,82,85,98,121,2,126,50,53,46,60,47,51,67,55,52,54,3,62,147])).
% 59.96/59.98 cnf(265,plain,
% 59.96/59.98 (E(x2651,f25(f23(x2652,f22(x2653,x2651)),x2653))),
% 59.96/59.98 inference(scs_inference,[],[196,87,121,2])).
% 59.96/59.98 cnf(266,plain,
% 59.96/59.98 (P1(f21(f6(f21(f6(x2661,x2662),x2662),x2663),x2663),f21(f6(x2661,x2664),x2664))),
% 59.96/59.98 inference(scs_inference,[],[196,258,87,121,2,47])).
% 59.96/59.98 cnf(268,plain,
% 59.96/59.98 (P9(f21(f6(x2681,x2682),x2682),f21(f6(f21(f6(x2681,x2683),x2683),x2684),x2684))),
% 59.96/59.98 inference(scs_inference,[],[196,258,87,198,121,2,47,50])).
% 59.96/59.98 cnf(270,plain,
% 59.96/59.98 (P1(f21(f6(a2,x2701),x2701),x2702)),
% 59.96/59.98 inference(scs_inference,[],[79,196,258,87,198,179,121,2,47,50,46])).
% 59.96/59.98 cnf(271,plain,
% 59.96/59.98 (E(x2711,f21(f6(x2711,x2712),x2712))),
% 59.96/59.98 inference(rename_variables,[],[179])).
% 59.96/59.98 cnf(272,plain,
% 59.96/59.98 (~P12(f27(f23(f21(f6(f29(x2721,x2722,a3),x2723),x2723),f22(x2724,x2725)),x2724))),
% 59.96/59.98 inference(scs_inference,[],[79,196,258,206,87,198,86,179,121,2,47,50,46,67])).
% 59.96/59.98 cnf(275,plain,
% 59.96/59.98 (E(f25(f23(x2751,f22(x2752,x2753)),x2752),x2753)),
% 59.96/59.98 inference(rename_variables,[],[87])).
% 59.96/59.98 cnf(277,plain,
% 59.96/59.98 (E(f25(f23(x2771,f22(x2772,x2773)),x2772),x2773)),
% 59.96/59.98 inference(rename_variables,[],[87])).
% 59.96/59.98 cnf(278,plain,
% 59.96/59.98 (P9(f21(f6(f21(f6(x2781,x2782),x2782),x2783),x2783),f21(f6(x2781,x2784),x2784))),
% 59.96/59.98 inference(scs_inference,[],[190,79,196,200,258,206,87,275,198,86,179,210,121,2,47,50,46,67,3,53,51])).
% 59.96/59.98 cnf(284,plain,
% 59.96/59.98 (P8(x2841,f21(f6(a2,x2842),x2842))),
% 59.96/59.98 inference(scs_inference,[],[190,79,196,200,258,206,253,87,275,277,198,86,179,271,208,210,121,2,47,50,46,67,3,53,51,52,54,136])).
% 59.96/59.98 cnf(300,plain,
% 59.96/59.98 (E(f20(f29(x3001,x3002,x3003),x3004),f29(f24(x3001,x3004),f23(x3002,f22(x3004,a2)),x3003))),
% 59.96/59.98 inference(scs_inference,[],[239,93,121,2])).
% 59.96/59.98 cnf(302,plain,
% 59.96/59.98 (P9(x3021,x3021)),
% 59.96/59.98 inference(rename_variables,[],[81])).
% 59.96/59.98 cnf(303,plain,
% 59.96/59.98 (~P7(f5(a1,x3031))),
% 59.96/59.98 inference(scs_inference,[],[239,231,93,81,78,96,121,2,50,53])).
% 59.96/59.98 cnf(304,plain,
% 59.96/59.98 (P1(f8(f29(a9,a14,a15)),f27(f23(f21(f6(f8(f29(a9,a14,a15)),x3041),x3041),f22(x3042,x3043)),x3042))),
% 59.96/59.98 inference(scs_inference,[],[239,231,93,81,78,80,96,121,2,50,53,47])).
% 59.96/59.98 cnf(311,plain,
% 59.96/59.98 (E(x3111,f25(f23(x3112,f22(x3113,x3111)),x3113))),
% 59.96/59.98 inference(rename_variables,[],[265])).
% 59.96/59.98 cnf(312,plain,
% 59.96/59.98 (P1(f25(f23(x3121,f22(x3122,a2)),x3122),x3123)),
% 59.96/59.98 inference(scs_inference,[],[92,189,79,239,231,83,265,311,272,93,81,78,86,80,96,121,2,50,53,47,3,67,55,46])).
% 59.96/59.98 cnf(322,plain,
% 59.96/59.98 (~E(f25(f23(x3221,f22(x3222,a2)),x3222),f7(f29(a9,a14,a15)))),
% 59.96/59.98 inference(scs_inference,[],[92,101,189,79,239,231,83,265,311,272,93,89,81,302,78,86,80,95,96,121,2,50,53,47,3,67,55,46,52,51,136,123,64])).
% 59.96/59.98 cnf(333,plain,
% 59.96/59.98 (E(a2,f7(f29(x3331,a1,x3332)))),
% 59.96/59.98 inference(scs_inference,[],[243,88,121,2])).
% 59.96/59.98 cnf(334,plain,
% 59.96/59.98 (P1(f21(f6(f21(f6(a2,x3341),x3341),x3342),x3342),x3343)),
% 59.96/59.98 inference(scs_inference,[],[243,239,79,88,121,2,126])).
% 59.96/59.98 cnf(344,plain,
% 59.96/59.98 (P1(f21(f6(x3441,x3442),x3442),f21(f6(f21(f6(x3441,x3443),x3443),x3444),x3444))),
% 59.96/59.98 inference(scs_inference,[],[322,243,239,194,258,79,83,300,88,179,251,100,121,2,126,67,3,52,46])).
% 59.96/59.98 cnf(355,plain,
% 59.96/59.98 (E(a1,f5(a1,x3551))),
% 59.96/59.98 inference(scs_inference,[],[270,78,121,2])).
% 59.96/59.98 cnf(378,plain,
% 59.96/59.98 (E(f29(x3781,a1,a3),f8(f29(x3781,a1,x3782)))),
% 59.96/59.98 inference(scs_inference,[],[266,91,121,2])).
% 59.96/59.98 cnf(381,plain,
% 59.96/59.98 (P3(f8(f29(x3811,a1,x3812)))),
% 59.96/59.98 inference(scs_inference,[],[190,266,83,91,90,121,2,3,54])).
% 59.96/59.98 cnf(408,plain,
% 59.96/59.98 (E(x4081,f27(f23(x4081,f22(x4082,x4083)),x4082))),
% 59.96/59.98 inference(scs_inference,[],[304,86,121,2])).
% 59.96/59.98 cnf(410,plain,
% 59.96/59.98 (E(f21(f6(f20(f29(x4101,x4102,x4103),x4104),x4105),x4105),f29(f24(x4101,x4104),f23(x4102,f22(x4104,a2)),x4103))),
% 59.96/59.98 inference(scs_inference,[],[304,83,300,86,237,121,2,53,3])).
% 59.96/59.98 cnf(421,plain,
% 59.96/59.98 (P10(f27(f23(f8(f29(a9,a14,a15)),f22(x4211,x4212)),x4211))),
% 59.96/59.98 inference(scs_inference,[],[92,344,408,410,121,2,55])).
% 59.96/59.98 cnf(426,plain,
% 59.96/59.98 (E(f21(f6(f8(f29(x4261,a1,x4262)),x4263),x4263),f29(x4261,a1,a3))),
% 59.96/59.98 inference(scs_inference,[],[92,344,83,91,408,410,100,121,2,55,67,3])).
% 59.96/59.98 cnf(436,plain,
% 59.96/59.98 (E(f29(x4361,a1,a3),f21(f6(f8(f29(x4361,a1,x4362)),x4363),x4363))),
% 59.96/59.98 inference(scs_inference,[],[334,426,121,2])).
% 59.96/59.98 cnf(440,plain,
% 59.96/59.98 (~E(f6(x4401,x4402),f16(f29(x4403,a1,x4404)))),
% 59.96/59.98 inference(scs_inference,[],[334,89,426,202,100,121,2,67,3])).
% 59.96/59.98 cnf(488,plain,
% 59.96/59.98 (~P17(x4881,x4881)),
% 59.96/59.98 inference(scs_inference,[],[80,121])).
% 59.96/59.98 cnf(512,plain,
% 59.96/59.98 (E(f21(f6(f29(x5121,a1,a3),x5122),x5122),f8(f29(x5121,a1,x5123)))),
% 59.96/59.98 inference(scs_inference,[],[83,378,3])).
% 59.96/59.98 cnf(542,plain,
% 59.96/59.98 (E(f21(f6(a2,x5421),x5421),f7(f29(x5422,a1,x5423)))),
% 59.96/59.98 inference(scs_inference,[],[83,333,3])).
% 59.96/59.98 cnf(544,plain,
% 59.96/59.98 (E(f7(f29(x5441,a1,x5442)),f21(f6(a2,x5443),x5443))),
% 59.96/59.98 inference(scs_inference,[],[83,333,3,2])).
% 59.96/59.98 cnf(555,plain,
% 59.96/59.98 (E(f21(f6(f7(f29(x5551,a1,x5552)),x5553),x5553),a2)),
% 59.96/59.98 inference(scs_inference,[],[83,88,3])).
% 59.96/59.98 cnf(557,plain,
% 59.96/59.98 (E(a2,f21(f6(f7(f29(x5571,a1,x5572)),x5573),x5573))),
% 59.96/59.98 inference(scs_inference,[],[83,88,3,2])).
% 59.96/59.98 cnf(570,plain,
% 59.96/59.98 (E(f21(f6(f7(f29(x5701,a1,x5702)),x5703),x5703),f21(f6(a2,x5704),x5704))),
% 59.96/59.98 inference(scs_inference,[],[83,544,3])).
% 59.96/59.98 cnf(572,plain,
% 59.96/59.98 (E(f21(f6(a2,x5721),x5721),f21(f6(f7(f29(x5722,a1,x5723)),x5724),x5724))),
% 59.96/59.98 inference(scs_inference,[],[83,544,3,2])).
% 59.96/59.98 cnf(579,plain,
% 59.96/59.98 (E(f27(f23(f8(f29(x5791,a1,x5792)),f22(x5793,x5794)),x5793),f29(x5791,a1,a3))),
% 59.96/59.98 inference(scs_inference,[],[86,91,3])).
% 59.96/59.98 cnf(583,plain,
% 59.96/59.98 (E(f29(x5831,a1,a3),f27(f23(f8(f29(x5831,a1,x5832)),f22(x5833,x5834)),x5833))),
% 59.96/59.98 inference(scs_inference,[],[86,91,100,3,67,2])).
% 59.96/59.98 cnf(593,plain,
% 59.96/59.98 (E(f21(f6(f29(x5931,a1,a3),x5932),x5932),f27(f23(f8(f29(x5931,a1,x5933)),f22(x5934,x5935)),x5934))),
% 59.96/59.98 inference(scs_inference,[],[83,583,3])).
% 59.96/59.98 cnf(633,plain,
% 59.96/59.98 (E(f21(f6(f8(f29(x6331,a1,x6332)),x6333),x6333),f8(f29(x6331,a1,x6334)))),
% 59.96/59.98 inference(scs_inference,[],[91,436,3,2])).
% 59.96/59.98 cnf(645,plain,
% 59.96/59.98 (E(f8(f29(x6451,a1,x6452)),f27(f23(f8(f29(x6451,a1,x6453)),f22(x6454,x6455)),x6454))),
% 59.96/59.98 inference(scs_inference,[],[91,583,3])).
% 59.96/59.98 cnf(659,plain,
% 59.96/59.98 (E(f27(f23(f8(f29(x6591,a1,x6592)),f22(x6593,x6594)),x6593),f21(f6(f8(f29(x6591,a1,x6595)),x6596),x6596))),
% 59.96/59.98 inference(scs_inference,[],[83,645,3,2])).
% 59.96/59.98 cnf(666,plain,
% 59.96/59.98 (E(f27(f23(f20(f29(x6661,x6662,x6663),x6664),f22(x6665,x6666)),x6665),f29(f24(x6661,x6664),f23(x6662,f22(x6664,a2)),x6663))),
% 59.96/59.98 inference(scs_inference,[],[86,300,3])).
% 59.96/59.98 cnf(688,plain,
% 59.96/59.98 (E(f29(f24(x6881,x6882),f23(x6883,f22(x6882,a2)),x6884),f27(f23(f20(f29(x6881,x6883,x6884),x6882),f22(x6885,x6886)),x6885))),
% 59.96/59.98 inference(scs_inference,[],[666,2])).
% 59.96/59.98 cnf(1095,plain,
% 59.96/59.98 (P1(f12(f16(f29(a9,a14,a15)),f7(f29(a9,a14,a15))),f7(f29(a9,a14,a15)))),
% 59.96/59.98 inference(scs_inference,[],[101,105,136])).
% 59.96/59.98 cnf(1220,plain,
% 59.96/59.98 (P4(f6(x12201,f21(f6(f5(a1,x12202),x12203),x12203)),a1)),
% 59.96/59.98 inference(scs_inference,[],[78,204,60])).
% 59.96/59.98 cnf(1222,plain,
% 59.96/59.98 (P6(f23(x12221,f22(f5(a1,x12222),x12223)),a1)),
% 59.96/59.98 inference(scs_inference,[],[78,204,168,60,62])).
% 59.96/59.98 cnf(1224,plain,
% 59.96/59.98 (P9(a1,f5(a1,x12241))),
% 59.96/59.98 inference(scs_inference,[],[78,204,81,168,60,62,50])).
% 59.96/59.98 cnf(1225,plain,
% 59.96/59.98 (P9(x12251,x12251)),
% 59.96/59.98 inference(rename_variables,[],[81])).
% 59.96/59.98 cnf(1226,plain,
% 59.96/59.98 (P9(f5(a1,x12261),a1)),
% 59.96/59.98 inference(scs_inference,[],[78,204,81,1225,168,60,62,50,51])).
% 59.96/59.98 cnf(1228,plain,
% 59.96/59.98 (P1(f21(f6(f5(a1,x12281),x12282),x12282),a1)),
% 59.96/59.98 inference(scs_inference,[],[78,196,204,81,1225,168,60,62,50,51,47])).
% 59.96/59.98 cnf(1230,plain,
% 59.96/59.98 (P1(a1,f21(f6(f5(a1,x12301),x12302),x12302))),
% 59.96/59.98 inference(scs_inference,[],[78,194,196,204,81,1225,168,60,62,50,51,47,46])).
% 59.96/59.98 cnf(1234,plain,
% 59.96/59.98 (E(f21(f6(f5(a1,x12341),x12342),x12342),a1)),
% 59.96/59.98 inference(scs_inference,[],[78,194,196,97,204,81,1225,168,60,62,50,51,47,46,121,137])).
% 59.96/59.98 cnf(1250,plain,
% 59.96/59.98 (P6(f23(x12501,f22(f21(f6(f5(a1,x12502),x12503),x12503),x12504)),a1)),
% 59.96/59.98 inference(scs_inference,[],[78,355,1220,1230,214,121,60,62])).
% 59.96/59.98 cnf(1252,plain,
% 59.96/59.98 (P9(a1,f21(f6(f5(a1,x12521),x12522),x12522))),
% 59.96/59.98 inference(scs_inference,[],[78,355,198,1220,1230,214,121,60,62,50])).
% 59.96/59.98 cnf(1254,plain,
% 59.96/59.98 (P9(f21(f6(f5(a1,x12541),x12542),x12542),a1)),
% 59.96/59.98 inference(scs_inference,[],[78,355,198,200,1220,1230,214,121,60,62,50,51])).
% 59.96/59.98 cnf(1256,plain,
% 59.96/59.98 (P1(f21(f6(f21(f6(f5(a1,x12561),x12562),x12562),x12563),x12563),a1)),
% 59.96/59.98 inference(scs_inference,[],[78,355,239,198,200,1220,1230,214,121,60,62,50,51,47])).
% 59.96/59.98 cnf(1258,plain,
% 59.96/59.98 (P1(a1,f21(f6(f21(f6(f5(a1,x12581),x12582),x12582),x12583),x12583))),
% 59.96/59.98 inference(scs_inference,[],[78,355,243,239,198,200,1220,1230,214,121,60,62,50,51,47,46])).
% 59.96/59.98 cnf(1260,plain,
% 59.96/59.98 (E(f21(f6(f5(a1,x12601),x12602),x12602),f5(a1,x12603))),
% 59.96/59.98 inference(scs_inference,[],[78,355,97,243,239,198,200,1220,1230,214,121,60,62,50,51,47,46,137])).
% 59.96/59.98 cnf(1269,plain,
% 59.96/59.98 (P18(f6(x12691,f21(f6(x12692,x12693),x12693)),f21(f6(x12692,x12694),x12694))),
% 59.96/59.98 inference(scs_inference,[],[241,258,116,66])).
% 59.96/59.98 cnf(1273,plain,
% 59.96/59.98 (P4(f6(x12731,f5(a1,x12732)),a1)),
% 59.96/59.98 inference(scs_inference,[],[78,1260,1256,167,121,2,60])).
% 59.96/59.98 cnf(1275,plain,
% 59.96/59.98 (P6(f23(x12751,f22(f5(a1,x12752),x12753)),f5(a1,x12754))),
% 59.96/59.98 inference(scs_inference,[],[78,355,1260,1256,167,1222,121,2,60,62])).
% 59.96/59.98 cnf(1276,plain,
% 59.96/59.98 (P9(a1,f21(f6(f21(f6(f5(a1,x12761),x12762),x12762),x12763),x12763))),
% 59.96/59.98 inference(scs_inference,[],[78,355,245,1260,1256,167,1222,121,2,60,62,50])).
% 59.96/59.98 cnf(1278,plain,
% 59.96/59.98 (P9(f21(f6(f5(a1,x12781),x12782),x12782),f5(a1,x12783))),
% 59.96/59.98 inference(scs_inference,[],[78,355,245,1260,1256,1254,167,1222,121,2,60,62,50,51])).
% 59.96/59.98 cnf(1279,plain,
% 59.96/59.98 (P1(f21(f6(f5(a1,x12791),x12792),x12792),f5(a1,x12793))),
% 59.96/59.98 inference(scs_inference,[],[78,355,245,1228,1260,1256,1254,167,1222,121,2,60,62,50,51,47])).
% 59.96/59.98 cnf(1280,plain,
% 59.96/59.98 (P1(f5(a1,x12801),f21(f6(f5(a1,x12802),x12803),x12803))),
% 59.96/59.98 inference(scs_inference,[],[78,355,245,1228,1230,1260,1256,1254,167,1222,121,2,60,62,50,51,47,46])).
% 59.96/59.98 cnf(1295,plain,
% 59.96/59.98 (P9(f5(a1,x12951),f5(a1,x12952))),
% 59.96/59.98 inference(scs_inference,[],[355,1258,1276,1273,1226,1250,121,60,62,50,51])).
% 59.96/59.98 cnf(1306,plain,
% 59.96/59.98 (P1(f5(a1,x13061),a1)),
% 59.96/59.98 inference(scs_inference,[],[78,355,1279,1252,80,121,50,47])).
% 59.96/59.98 cnf(1307,plain,
% 59.96/59.98 (P1(x13071,x13071)),
% 59.96/59.98 inference(rename_variables,[],[80])).
% 59.96/59.98 cnf(1308,plain,
% 59.96/59.98 (P1(a1,f5(a1,x13081))),
% 59.96/59.98 inference(scs_inference,[],[78,355,1279,1252,80,1307,121,50,47,46])).
% 59.96/59.98 cnf(1316,plain,
% 59.96/59.98 (P1(f5(a1,x13161),f5(a1,x13162))),
% 59.96/59.98 inference(scs_inference,[],[355,1280,1306,121,47])).
% 59.96/59.98 cnf(1342,plain,
% 59.96/59.98 (P1(f7(f29(x13421,a1,x13422)),x13423)),
% 59.96/59.98 inference(scs_inference,[],[79,333,46])).
% 59.96/59.98 cnf(1347,plain,
% 59.96/59.98 (~E(f7(f29(x13471,a1,x13472)),f7(f29(a9,a14,a15)))),
% 59.96/59.98 inference(scs_inference,[],[101,79,333,46,136,121,64])).
% 59.96/59.98 cnf(1367,plain,
% 59.96/59.98 (P1(f25(f23(x13671,f22(x13672,f7(f29(x13673,a1,x13674)))),x13672),x13675)),
% 59.96/59.98 inference(scs_inference,[],[1347,83,265,1342,27,121,3,46])).
% 59.96/59.98 cnf(1369,plain,
% 59.96/59.98 (~E(a1,a14)),
% 59.96/59.98 inference(scs_inference,[],[1347,83,265,1342,27,121,3,46,13])).
% 59.96/59.98 cnf(1374,plain,
% 59.96/59.98 (E(f27(f23(f27(f23(f8(f29(x13741,a1,x13742)),f22(x13743,x13744)),x13743),f22(x13745,x13746)),x13745),f29(x13741,a1,a3))),
% 59.96/59.98 inference(scs_inference,[],[86,579,1367,121,3])).
% 59.96/59.98 cnf(1376,plain,
% 59.96/59.98 (E(f29(x13761,a1,a3),f27(f23(f27(f23(f8(f29(x13761,a1,x13762)),f22(x13763,x13764)),x13763),f22(x13765,x13766)),x13765))),
% 59.96/59.98 inference(scs_inference,[],[1374,2])).
% 59.96/59.98 cnf(1377,plain,
% 59.96/59.98 (~P12(f27(f23(f27(f23(f8(f29(x13771,a1,x13772)),f22(x13773,x13774)),x13773),f22(x13775,x13776)),x13775))),
% 59.96/59.98 inference(scs_inference,[],[1374,100,2,67])).
% 59.96/59.98 cnf(1421,plain,
% 59.96/59.98 (P18(f6(x14211,f21(f6(x14212,x14213),x14213)),x14212)),
% 59.96/59.98 inference(scs_inference,[],[83,1269,66])).
% 59.96/59.98 cnf(1423,plain,
% 59.96/59.98 (P4(f6(x14231,f21(f6(f21(f6(x14232,x14233),x14233),x14234),x14234)),x14232)),
% 59.96/59.98 inference(scs_inference,[],[83,204,1269,66,60])).
% 59.96/59.98 cnf(1425,plain,
% 59.96/59.98 (P9(f21(f6(f21(f6(x14251,x14252),x14252),x14253),x14253),x14251)),
% 59.96/59.98 inference(scs_inference,[],[83,204,278,1269,66,60,51])).
% 59.96/59.98 cnf(1427,plain,
% 59.96/59.98 (E(f21(f6(f21(f6(a2,x14271),x14271),x14272),x14272),f7(f29(x14273,a1,x14274)))),
% 59.96/59.98 inference(scs_inference,[],[83,542,204,278,1269,66,60,51,3])).
% 59.96/59.98 cnf(1429,plain,
% 59.96/59.98 (E(f7(f29(x14291,a1,x14292)),f21(f6(f21(f6(a2,x14293),x14293),x14294),x14294))),
% 59.96/59.98 inference(scs_inference,[],[83,542,204,278,1269,66,60,51,3,2])).
% 59.96/59.98 cnf(1447,plain,
% 59.96/59.98 (E(f21(f6(f29(x14471,a1,a3),x14472),x14472),f27(f23(f27(f23(f8(f29(x14471,a1,x14473)),f22(x14474,x14475)),x14474),f22(x14476,x14477)),x14476))),
% 59.96/59.98 inference(scs_inference,[],[83,97,1376,1423,1421,66,137,3])).
% 59.96/59.98 cnf(1451,plain,
% 59.96/59.98 (E(x14511,f21(f6(f21(f6(x14511,x14512),x14512),x14513),x14513))),
% 59.96/59.98 inference(scs_inference,[],[83,86,97,1376,1423,1377,1421,66,137,3,67,2])).
% 59.96/59.98 cnf(1472,plain,
% 59.96/59.98 (E(f21(f6(x14721,x14722),x14722),f21(f6(f21(f6(x14721,x14723),x14723),x14724),x14724))),
% 59.96/59.98 inference(scs_inference,[],[83,1451,1447,2,3])).
% 59.96/59.98 cnf(1711,plain,
% 59.96/59.98 (P4(f6(x17111,f6(f6(x17112,x17113),x17114)),f6(f6(x17112,x17114),x17113))),
% 59.96/59.98 inference(scs_inference,[],[84,167,60])).
% 59.96/59.98 cnf(1713,plain,
% 59.96/59.98 (P6(f23(x17131,f22(f6(f6(x17132,x17133),x17134),x17135)),f6(f6(x17132,x17134),x17133))),
% 59.96/59.98 inference(scs_inference,[],[84,167,168,60,62])).
% 59.96/59.98 cnf(1715,plain,
% 59.96/59.98 (P9(f6(f6(x17151,x17152),x17153),f6(f6(x17151,x17153),x17152))),
% 59.96/59.98 inference(scs_inference,[],[84,81,167,168,60,62,50])).
% 59.96/59.98 cnf(1721,plain,
% 59.96/59.98 (P1(f21(f6(f6(f6(x17211,x17212),x17213),x17214),x17214),f6(f6(x17211,x17213),x17212))),
% 59.96/59.98 inference(scs_inference,[],[84,91,196,1376,81,200,167,168,60,62,50,51,3,47])).
% 59.96/59.98 cnf(1723,plain,
% 59.96/59.98 (P1(f6(f6(x17231,x17232),x17233),f21(f6(f6(f6(x17231,x17233),x17232),x17234),x17234))),
% 59.96/59.98 inference(scs_inference,[],[84,91,194,196,1376,81,200,167,168,60,62,50,51,3,47,46])).
% 59.96/59.98 cnf(1737,plain,
% 59.96/59.98 (P1(f6(f6(x17371,x17372),x17373),f6(f6(x17371,x17373),x17372))),
% 59.96/59.98 inference(scs_inference,[],[84,198,1723,80,121,50,47])).
% 59.96/59.98 cnf(1787,plain,
% 59.96/59.98 (E(f19(f5(f5(a1,x17871),x17872)),f19(f5(a1,x17872)))),
% 59.96/59.98 inference(scs_inference,[],[78,24,4])).
% 59.96/59.98 cnf(1788,plain,
% 59.96/59.98 (E(f19(f5(a1,x17881)),f19(f5(f5(a1,x17882),x17881)))),
% 59.96/59.98 inference(scs_inference,[],[1787,2])).
% 59.96/59.98 cnf(1789,plain,
% 59.96/59.98 (P18(f6(x17891,f21(f6(f5(a1,x17892),x17893),x17893)),a1)),
% 59.96/59.98 inference(scs_inference,[],[78,1787,1421,2,66])).
% 59.96/59.98 cnf(1793,plain,
% 59.96/59.98 (E(f5(a1,x17931),f21(f6(f21(f6(a1,x17932),x17932),x17933),x17933))),
% 59.96/59.98 inference(scs_inference,[],[78,1451,1425,1787,1421,2,66,51,3])).
% 59.96/59.98 cnf(1804,plain,
% 59.96/59.98 (E(f8(f5(x18041,f5(a1,x18042))),f8(f5(x18041,a1)))),
% 59.96/59.98 inference(scs_inference,[],[78,28,5])).
% 59.96/59.98 cnf(1805,plain,
% 59.96/59.98 (E(f8(f5(x18051,a1)),f8(f5(x18051,f5(a1,x18052))))),
% 59.96/59.98 inference(scs_inference,[],[1804,2])).
% 59.96/59.98 cnf(1836,plain,
% 59.96/59.98 (~E(f23(x18361,f22(x18362,x18363)),f21(f6(f21(f6(a1,x18364),x18364),x18365),x18365))),
% 59.96/59.98 inference(scs_inference,[],[1793,255,2,3])).
% 59.96/59.98 cnf(1855,plain,
% 59.96/59.98 (~E(f23(x18551,f22(x18552,x18553)),f21(f6(a1,x18554),x18554))),
% 59.96/59.98 inference(scs_inference,[],[1472,1836,3])).
% 59.96/59.98 cnf(2126,plain,
% 59.96/59.98 (E(f13(f22(f27(f23(x21261,f22(x21262,x21263)),x21262),x21264)),f13(f22(x21261,x21264)))),
% 59.96/59.98 inference(scs_inference,[],[86,39,8])).
% 59.96/59.98 cnf(2127,plain,
% 59.96/59.98 (P4(f6(x21271,f27(f23(x21272,f22(x21273,x21274)),x21273)),x21272)),
% 59.96/59.98 inference(scs_inference,[],[86,167,60])).
% 59.96/59.98 cnf(2131,plain,
% 59.96/59.98 (P9(x21311,f27(f23(x21311,f22(x21312,x21313)),x21312))),
% 59.96/59.98 inference(scs_inference,[],[86,81,167,168,60,62,50])).
% 59.96/59.98 cnf(2132,plain,
% 59.96/59.98 (P9(x21321,x21321)),
% 59.96/59.98 inference(rename_variables,[],[81])).
% 59.96/59.98 cnf(2133,plain,
% 59.96/59.98 (P9(f27(f23(x21331,f22(x21332,x21333)),x21332),x21331)),
% 59.96/59.98 inference(scs_inference,[],[86,81,2132,167,168,60,62,50,51])).
% 59.96/59.98 cnf(2135,plain,
% 59.96/59.98 (E(f27(f23(f29(x21351,a1,a3),f22(x21352,x21353)),x21352),f8(f29(x21351,a1,x21354)))),
% 59.96/59.98 inference(scs_inference,[],[86,378,81,2132,167,168,60,62,50,51,3])).
% 59.96/59.98 cnf(2136,plain,
% 59.96/59.98 (E(f27(f23(x21361,f22(x21362,x21363)),x21362),x21361)),
% 59.96/59.98 inference(rename_variables,[],[86])).
% 59.96/59.98 cnf(2139,plain,
% 59.96/59.98 (P1(x21391,f21(f6(f27(f23(x21391,f22(x21392,x21393)),x21392),x21394),x21394))),
% 59.96/59.98 inference(scs_inference,[],[86,2136,378,194,196,81,2132,167,168,60,62,50,51,3,47,46])).
% 59.96/59.98 cnf(2151,plain,
% 59.96/59.98 (P9(f21(f6(x21511,x21512),x21512),f20(f26(f21(f6(x21511,x21513),x21513),x21514),x21515))),
% 59.96/59.98 inference(scs_inference,[],[235,132,133])).
% 59.96/59.98 cnf(2154,plain,
% 59.96/59.98 (P4(f6(x21541,f27(f23(f27(f23(x21542,f22(x21543,x21544)),x21543),f22(x21545,x21546)),x21545)),x21542)),
% 59.96/59.98 inference(scs_inference,[],[86,2127,2139,121,60])).
% 59.96/59.98 cnf(2160,plain,
% 59.96/59.98 (E(f27(f23(f21(f6(f8(f29(x21601,a1,x21602)),x21603),x21603),f22(x21604,x21605)),x21604),f29(x21601,a1,a3))),
% 59.96/59.98 inference(scs_inference,[],[86,426,200,198,2127,2139,121,60,50,51,3])).
% 59.96/59.98 cnf(2161,plain,
% 59.96/59.98 (E(f27(f23(x21611,f22(x21612,x21613)),x21612),x21611)),
% 59.96/59.98 inference(rename_variables,[],[86])).
% 59.96/59.98 cnf(2162,plain,
% 59.96/59.98 (P1(f27(f23(x21621,f22(x21622,x21623)),x21622),x21621)),
% 59.96/59.98 inference(scs_inference,[],[86,2161,426,200,198,2127,2139,80,121,60,50,51,3,47])).
% 59.96/59.98 cnf(2163,plain,
% 59.96/59.98 (P1(x21631,x21631)),
% 59.96/59.98 inference(rename_variables,[],[80])).
% 59.96/59.98 cnf(2164,plain,
% 59.96/59.98 (P1(x21641,f27(f23(x21641,f22(x21642,x21643)),x21642))),
% 59.96/59.98 inference(scs_inference,[],[86,2161,426,200,198,2127,2139,80,2163,121,60,50,51,3,47,46])).
% 59.96/59.98 cnf(2185,plain,
% 59.96/59.98 (E(f29(x21851,a1,a3),f27(f23(f21(f6(f8(f29(x21851,a1,x21852)),x21853),x21853),f22(x21854,x21855)),x21854))),
% 59.96/59.98 inference(scs_inference,[],[2162,2160,121,2])).
% 59.96/59.98 cnf(2186,plain,
% 59.96/59.98 (E(f27(f23(f27(f23(x21861,f22(x21862,x21863)),x21862),f22(x21864,x21865)),x21864),x21861)),
% 59.96/59.98 inference(scs_inference,[],[97,2162,2154,2160,121,2,137])).
% 59.96/59.98 cnf(2189,plain,
% 59.96/59.98 (P9(x21891,f27(f23(f27(f23(x21891,f22(x21892,x21893)),x21892),f22(x21894,x21895)),x21894))),
% 59.96/59.98 inference(scs_inference,[],[86,97,2131,2162,2154,2160,121,2,137,50])).
% 59.96/59.98 cnf(2191,plain,
% 59.96/59.98 (P9(f27(f23(f27(f23(x21911,f22(x21912,x21913)),x21912),f22(x21914,x21915)),x21914),x21911)),
% 59.96/59.98 inference(scs_inference,[],[86,97,2131,2133,2162,2154,2160,121,2,137,50,51])).
% 59.96/59.98 cnf(2193,plain,
% 59.96/59.98 (E(f27(f23(f29(x21931,a1,a3),f22(x21932,x21933)),x21932),f21(f6(f8(f29(x21931,a1,x21934)),x21935),x21935))),
% 59.96/59.98 inference(scs_inference,[],[86,436,97,2131,2133,2162,2154,2160,121,2,137,50,51,3])).
% 59.96/59.98 cnf(2194,plain,
% 59.96/59.98 (E(f27(f23(x21941,f22(x21942,x21943)),x21942),x21941)),
% 59.96/59.98 inference(rename_variables,[],[86])).
% 59.96/59.98 cnf(2195,plain,
% 59.96/59.98 (P1(f27(f23(f27(f23(x21951,f22(x21952,x21953)),x21952),f22(x21954,x21955)),x21954),x21951)),
% 59.96/59.98 inference(scs_inference,[],[86,2194,436,97,2131,2133,2162,2154,2160,121,2,137,50,51,3,47])).
% 59.96/59.98 cnf(2197,plain,
% 59.96/59.98 (P1(x21971,f27(f23(f27(f23(x21971,f22(x21972,x21973)),x21972),f22(x21974,x21975)),x21974))),
% 59.96/59.98 inference(scs_inference,[],[86,2194,436,97,2131,2133,2162,2164,2154,2160,121,2,137,50,51,3,47,46])).
% 59.96/59.98 cnf(2220,plain,
% 59.96/59.98 (E(x22201,f27(f23(f27(f23(x22201,f22(x22202,x22203)),x22202),f22(x22204,x22205)),x22204))),
% 59.96/59.98 inference(scs_inference,[],[2186,2195,121,2])).
% 59.96/59.98 cnf(2225,plain,
% 59.96/59.98 (E(f27(f23(f21(f6(f29(x22251,a1,a3),x22252),x22252),f22(x22253,x22254)),x22253),f8(f29(x22251,a1,x22255)))),
% 59.96/59.98 inference(scs_inference,[],[86,512,2186,2189,2191,2195,121,2,50,51,3])).
% 59.96/59.98 cnf(2226,plain,
% 59.96/59.98 (E(f27(f23(x22261,f22(x22262,x22263)),x22262),x22261)),
% 59.96/59.98 inference(rename_variables,[],[86])).
% 59.96/59.98 cnf(2227,plain,
% 59.96/59.98 (P1(f27(f23(f27(f23(f27(f23(x22271,f22(x22272,x22273)),x22272),f22(x22274,x22275)),x22274),f22(x22276,x22277)),x22276),x22271)),
% 59.96/59.98 inference(scs_inference,[],[86,2226,512,2186,2189,2191,2195,121,2,50,51,3,47])).
% 59.96/59.98 cnf(2229,plain,
% 59.96/59.98 (P1(x22291,f27(f23(f27(f23(f27(f23(x22291,f22(x22292,x22293)),x22292),f22(x22294,x22295)),x22294),f22(x22296,x22297)),x22296))),
% 59.96/59.98 inference(scs_inference,[],[86,2226,512,2186,2189,2191,2195,2197,121,2,50,51,3,47,46])).
% 59.96/59.98 cnf(2240,plain,
% 59.96/59.98 (E(f21(f6(f8(f29(x22401,a1,x22402)),x22403),x22403),f27(f23(f29(x22401,a1,a3),f22(x22404,x22405)),x22404))),
% 59.96/59.98 inference(scs_inference,[],[2193,2164,121,2])).
% 59.96/59.98 cnf(2241,plain,
% 59.96/59.98 (E(f27(f23(f29(x22411,a1,a3),f22(x22412,x22413)),x22412),f27(f23(f8(f29(x22411,a1,x22414)),f22(x22415,x22416)),x22415))),
% 59.96/59.98 inference(scs_inference,[],[86,583,2193,2164,121,2,3])).
% 59.96/59.98 cnf(2261,plain,
% 59.96/59.98 (E(f27(f23(a2,f22(x22611,x22612)),x22611),f7(f29(x22613,a1,x22614)))),
% 59.96/59.98 inference(scs_inference,[],[86,333,2229,2225,121,2,3])).
% 59.96/59.98 cnf(2278,plain,
% 59.96/59.98 (E(f27(f23(f21(f6(f29(x22781,a1,a3),x22782),x22782),f22(x22783,x22784)),x22783),f27(f23(f8(f29(x22781,a1,x22785)),f22(x22786,x22787)),x22786))),
% 59.96/59.98 inference(scs_inference,[],[86,593,2197,2241,121,2,3])).
% 59.96/59.98 cnf(2301,plain,
% 59.96/59.98 (E(f27(f23(f7(f29(x23011,a1,x23012)),f22(x23013,x23014)),x23013),a2)),
% 59.96/59.98 inference(scs_inference,[],[86,88,2227,2278,121,2,3])).
% 59.96/59.98 cnf(2342,plain,
% 59.96/59.98 (E(a2,f27(f23(f7(f29(x23421,a1,x23422)),f22(x23423,x23424)),x23423))),
% 59.96/59.98 inference(scs_inference,[],[2301,2])).
% 59.96/59.98 cnf(2343,plain,
% 59.96/59.98 (E(f27(f23(f21(f6(a2,x23431),x23431),f22(x23432,x23433)),x23432),f7(f29(x23434,a1,x23435)))),
% 59.96/59.98 inference(scs_inference,[],[86,542,2301,2,3])).
% 59.96/59.98 cnf(2371,plain,
% 59.96/59.98 (E(f27(f23(f21(f6(f8(f29(x23711,a1,x23712)),x23713),x23713),f22(x23714,x23715)),x23714),f8(f29(x23711,a1,x23716)))),
% 59.96/59.98 inference(scs_inference,[],[86,633,2343,2,3])).
% 59.96/59.98 cnf(2384,plain,
% 59.96/59.98 (E(f27(f23(a2,f22(x23841,x23842)),x23841),f21(f6(f7(f29(x23843,a1,x23844)),x23845),x23845))),
% 59.96/59.98 inference(scs_inference,[],[86,557,2371,2,3])).
% 59.96/59.98 cnf(2416,plain,
% 59.96/59.98 (E(f27(f23(f21(f6(f7(f29(x24161,a1,x24162)),x24163),x24163),f22(x24164,x24165)),x24164),f21(f6(a2,x24166),x24166))),
% 59.96/59.98 inference(scs_inference,[],[86,570,2384,2,3])).
% 59.96/59.98 cnf(2445,plain,
% 59.96/59.98 (E(f27(f23(f7(f29(x24451,a1,x24452)),f22(x24453,x24454)),x24453),f21(f6(a2,x24455),x24455))),
% 59.96/59.98 inference(scs_inference,[],[86,544,2416,2,3])).
% 59.96/59.98 cnf(2454,plain,
% 59.96/59.98 (E(f21(f6(a2,x24541),x24541),f27(f23(f7(f29(x24542,a1,x24543)),f22(x24544,x24545)),x24544))),
% 59.96/59.98 inference(scs_inference,[],[2445,2])).
% 59.96/59.98 cnf(2455,plain,
% 59.96/59.98 (E(f27(f23(f21(f6(a2,x24551),x24551),f22(x24552,x24553)),x24552),f21(f6(f7(f29(x24554,a1,x24555)),x24556),x24556))),
% 59.96/59.98 inference(scs_inference,[],[86,572,2445,2,3])).
% 59.96/59.98 cnf(2484,plain,
% 59.96/59.98 (E(f27(f23(f21(f6(f7(f29(x24841,a1,x24842)),x24843),x24843),f22(x24844,x24845)),x24844),a2)),
% 59.96/59.98 inference(scs_inference,[],[86,555,2455,2,3])).
% 59.96/59.98 cnf(2498,plain,
% 59.96/59.98 (E(f27(f23(f29(f24(x24981,x24982),f23(x24983,f22(x24982,a2)),x24984),f22(x24985,x24986)),x24985),f20(f29(x24981,x24983,x24984),x24982))),
% 59.96/59.98 inference(scs_inference,[],[86,93,2484,2,3])).
% 59.96/59.98 cnf(2526,plain,
% 59.96/59.98 (E(f27(f23(f29(f24(x25261,x25262),f23(x25263,f22(x25262,a2)),x25264),f22(x25265,x25266)),x25265),f27(f23(f20(f29(x25261,x25263,x25264),x25262),f22(x25267,x25268)),x25267))),
% 59.96/59.98 inference(scs_inference,[],[86,688,2498,2,3])).
% 59.96/59.98 cnf(2545,plain,
% 59.96/59.98 (E(f27(f23(f27(f23(f20(f29(x25451,x25452,x25453),x25454),f22(x25455,x25456)),x25455),f22(x25457,x25458)),x25457),f29(f24(x25451,x25454),f23(x25452,f22(x25454,a2)),x25453))),
% 59.96/59.98 inference(scs_inference,[],[86,666,2526,2,3])).
% 59.96/59.98 cnf(2560,plain,
% 59.96/59.98 (E(f23(f5(x25601,f21(f6(a2,x25602),x25602)),f22(x25603,x25604)),f5(f23(x25601,f22(x25603,x25604)),f21(f6(a2,x25602),x25602)))),
% 59.96/59.98 inference(scs_inference,[],[284,218,148])).
% 59.96/59.98 cnf(2562,plain,
% 59.96/59.98 (E(f27(f23(f29(x25621,a1,a3),f22(x25622,x25623)),x25622),f27(f23(f27(f23(f8(f29(x25621,a1,x25624)),f22(x25625,x25626)),x25625),f22(x25627,x25628)),x25627))),
% 59.96/59.98 inference(scs_inference,[],[86,1376,2545,2,3])).
% 59.96/59.98 cnf(2564,plain,
% 59.96/59.98 (P7(f5(f23(x25641,f22(x25642,x25643)),f21(f6(a2,x25644),x25644)))),
% 59.96/59.98 inference(scs_inference,[],[86,1376,2545,2560,85,2,3,53])).
% 59.96/59.98 cnf(2582,plain,
% 59.96/59.98 (E(f27(f23(f27(f23(f27(f23(f8(f29(x25821,a1,x25822)),f22(x25823,x25824)),x25823),f22(x25825,x25826)),x25825),f22(x25827,x25828)),x25827),f29(x25821,a1,a3))),
% 59.96/59.98 inference(scs_inference,[],[86,1374,2562,2,3])).
% 59.96/59.98 cnf(2596,plain,
% 59.96/59.98 (E(f27(f23(f21(f6(f21(f6(a2,x25961),x25961),x25962),x25962),f22(x25963,x25964)),x25963),f7(f29(x25965,a1,x25966)))),
% 59.96/59.98 inference(scs_inference,[],[86,1427,2560,2,3])).
% 59.96/59.98 cnf(2614,plain,
% 59.96/59.98 (E(f27(f23(f7(f29(x26141,a1,x26142)),f22(x26143,x26144)),x26143),f21(f6(f21(f6(a2,x26145),x26145),x26146),x26146))),
% 59.96/59.98 inference(scs_inference,[],[86,1429,2582,2,3])).
% 59.96/59.98 cnf(2624,plain,
% 59.96/59.98 (E(f27(f23(f19(f5(a1,x26241)),f22(x26242,x26243)),x26242),f19(f5(f5(a1,x26244),x26241)))),
% 59.96/59.98 inference(scs_inference,[],[86,1788,2614,2,3])).
% 59.96/59.98 cnf(2639,plain,
% 59.96/59.98 (E(f19(f5(f5(a1,x26391),x26392)),f27(f23(f19(f5(a1,x26392)),f22(x26393,x26394)),x26393))),
% 59.96/59.98 inference(scs_inference,[],[2624,2])).
% 59.96/59.98 cnf(2640,plain,
% 59.96/59.98 (E(f27(f23(f8(f5(x26401,a1)),f22(x26402,x26403)),x26402),f8(f5(x26401,f5(a1,x26404))))),
% 59.96/59.98 inference(scs_inference,[],[86,1805,2624,2,3])).
% 59.96/59.98 cnf(2653,plain,
% 59.96/59.98 (E(f27(f23(f19(f5(f5(a1,x26531),x26532)),f22(x26533,x26534)),x26533),f19(f5(a1,x26532)))),
% 59.96/59.98 inference(scs_inference,[],[86,1787,2640,2,3])).
% 59.96/59.98 cnf(2683,plain,
% 59.96/59.98 (E(f27(f23(f8(f5(x26831,f5(a1,x26832))),f22(x26833,x26834)),x26833),f8(f5(x26831,a1)))),
% 59.96/59.98 inference(scs_inference,[],[86,1804,2596,2,3])).
% 59.96/59.98 cnf(2717,plain,
% 59.96/59.98 (E(f8(f5(x27171,a1)),f27(f23(f8(f5(x27171,f5(a1,x27172))),f22(x27173,x27174)),x27173))),
% 59.96/59.98 inference(scs_inference,[],[2683,2])).
% 59.96/59.98 cnf(2718,plain,
% 59.96/59.98 (E(f27(f23(f27(f23(f29(x27181,a1,a3),f22(x27182,x27183)),x27182),f22(x27184,x27185)),x27184),f8(f29(x27181,a1,x27186)))),
% 59.96/59.98 inference(scs_inference,[],[86,2135,2683,2,3])).
% 59.96/59.98 cnf(2753,plain,
% 59.96/59.98 (E(f27(f23(f27(f23(f21(f6(f29(x27531,a1,a3),x27532),x27532),f22(x27533,x27534)),x27533),f22(x27535,x27536)),x27535),f8(f29(x27531,a1,x27537)))),
% 59.96/59.98 inference(scs_inference,[],[86,2225,2718,2,3])).
% 59.96/59.98 cnf(2774,plain,
% 59.96/59.99 (E(f27(f23(f27(f23(f29(x27741,a1,a3),f22(x27742,x27743)),x27742),f22(x27744,x27745)),x27744),f27(f23(f8(f29(x27741,a1,x27746)),f22(x27747,x27748)),x27747))),
% 59.96/59.99 inference(scs_inference,[],[86,2241,2753,2,3])).
% 59.96/59.99 cnf(2785,plain,
% 59.96/59.99 (E(f27(f23(f27(f23(f29(f24(x27851,x27852),f23(x27853,f22(x27852,a2)),x27854),f22(x27855,x27856)),x27855),f22(x27857,x27858)),x27857),f20(f29(x27851,x27853,x27854),x27852))),
% 59.96/59.99 inference(scs_inference,[],[86,2498,2774,2,3])).
% 59.96/59.99 cnf(2812,plain,
% 59.96/59.99 (E(f27(f23(f27(f23(a2,f22(x28121,x28122)),x28121),f22(x28123,x28124)),x28123),f7(f29(x28125,a1,x28126)))),
% 59.96/59.99 inference(scs_inference,[],[86,2261,2785,2,3])).
% 59.96/59.99 cnf(2840,plain,
% 59.96/59.99 (E(f7(f29(x28401,a1,x28402)),f27(f23(f27(f23(a2,f22(x28403,x28404)),x28403),f22(x28405,x28406)),x28405))),
% 59.96/59.99 inference(scs_inference,[],[2812,2])).
% 59.96/59.99 cnf(2841,plain,
% 59.96/59.99 (E(f27(f23(a2,f22(x28411,x28412)),x28411),f27(f23(f7(f29(x28413,a1,x28414)),f22(x28415,x28416)),x28415))),
% 59.96/59.99 inference(scs_inference,[],[86,2342,2812,2,3])).
% 59.96/59.99 cnf(2858,plain,
% 59.96/59.99 (E(f27(f23(f7(f29(x28581,a1,x28582)),f22(x28583,x28584)),x28583),f27(f23(a2,f22(x28585,x28586)),x28585))),
% 59.96/59.99 inference(scs_inference,[],[2841,2])).
% 59.96/59.99 cnf(2859,plain,
% 59.96/59.99 (E(f27(f23(f27(f23(f27(f23(f29(x28591,a1,a3),f22(x28592,x28593)),x28592),f22(x28594,x28595)),x28594),f22(x28596,x28597)),x28596),f8(f29(x28591,a1,x28598)))),
% 59.96/59.99 inference(scs_inference,[],[86,2718,2841,2,3])).
% 59.96/59.99 cnf(2875,plain,
% 59.96/59.99 (E(f27(f23(f27(f23(f7(f29(x28751,a1,x28752)),f22(x28753,x28754)),x28753),f22(x28755,x28756)),x28755),f27(f23(a2,f22(x28757,x28758)),x28757))),
% 59.96/59.99 inference(scs_inference,[],[86,2858,2859,2,3])).
% 59.96/59.99 cnf(2886,plain,
% 59.96/59.99 (E(f27(f23(f7(f29(x28861,a1,x28862)),f22(x28863,x28864)),x28863),f27(f23(f27(f23(a2,f22(x28865,x28866)),x28865),f22(x28867,x28868)),x28867))),
% 59.96/59.99 inference(scs_inference,[],[86,2875,2840,2,3])).
% 59.96/59.99 cnf(2916,plain,
% 59.96/59.99 (E(f27(f23(f8(f5(x29161,a1)),f22(x29162,x29163)),x29162),f27(f23(f8(f5(x29161,f5(a1,x29164))),f22(x29165,x29166)),x29165))),
% 59.96/59.99 inference(scs_inference,[],[86,2886,2717,2,3])).
% 59.96/59.99 cnf(2926,plain,
% 59.96/59.99 (E(f27(f23(f27(f23(f19(f5(a1,x29261)),f22(x29262,x29263)),x29262),f22(x29264,x29265)),x29264),f19(f5(f5(a1,x29266),x29261)))),
% 59.96/59.99 inference(scs_inference,[],[86,2916,2624,2,3])).
% 59.96/59.99 cnf(2941,plain,
% 59.96/59.99 (E(f27(f23(f19(f5(f5(a1,x29411),x29412)),f22(x29413,x29414)),x29413),f27(f23(f19(f5(a1,x29412)),f22(x29415,x29416)),x29415))),
% 59.96/59.99 inference(scs_inference,[],[86,2926,2639,2,3])).
% 59.96/59.99 cnf(2954,plain,
% 59.96/59.99 (E(f27(f23(f27(f23(f8(f5(x29541,a1)),f22(x29542,x29543)),x29542),f22(x29544,x29545)),x29544),f8(f5(x29541,f5(a1,x29546))))),
% 59.96/59.99 inference(scs_inference,[],[86,2941,2640,2,3])).
% 59.96/59.99 cnf(2976,plain,
% 59.96/59.99 (E(f27(f23(f21(f6(a2,x29761),x29761),f22(x29762,x29763)),x29762),f27(f23(f7(f29(x29764,a1,x29765)),f22(x29766,x29767)),x29766))),
% 59.96/59.99 inference(scs_inference,[],[86,2954,2454,2,3])).
% 59.96/59.99 cnf(2991,plain,
% 59.96/59.99 (E(f27(f23(f27(f23(f27(f23(a2,f22(x29911,x29912)),x29911),f22(x29913,x29914)),x29913),f22(x29915,x29916)),x29915),f7(f29(x29917,a1,x29918)))),
% 59.96/59.99 inference(scs_inference,[],[86,2976,2812,2,3])).
% 59.96/59.99 cnf(3011,plain,
% 59.96/59.99 (E(f27(f23(f27(f23(f19(f5(f5(a1,x30111),x30112)),f22(x30113,x30114)),x30113),f22(x30115,x30116)),x30115),f19(f5(a1,x30112)))),
% 59.96/59.99 inference(scs_inference,[],[86,2991,2653,2,3])).
% 59.96/59.99 cnf(3046,plain,
% 59.96/59.99 (E(f27(f23(f27(f23(f8(f5(x30461,f5(a1,x30462))),f22(x30463,x30464)),x30463),f22(x30465,x30466)),x30465),f8(f5(x30461,a1)))),
% 59.96/59.99 inference(scs_inference,[],[86,3011,2683,2,3])).
% 59.96/59.99 cnf(3081,plain,
% 59.96/59.99 (E(f27(f23(f27(f23(f7(f29(x30811,a1,x30812)),f22(x30813,x30814)),x30813),f22(x30815,x30816)),x30815),f21(f6(a2,x30817),x30817))),
% 59.96/59.99 inference(scs_inference,[],[86,3046,2445,2,3])).
% 59.96/59.99 cnf(3091,plain,
% 59.96/59.99 (E(f27(f23(f27(f23(f21(f6(a2,x30911),x30911),f22(x30912,x30913)),x30912),f22(x30914,x30915)),x30914),f7(f29(x30916,a1,x30917)))),
% 59.96/59.99 inference(scs_inference,[],[86,3081,2343,2,3])).
% 59.96/59.99 cnf(3114,plain,
% 59.96/59.99 (E(f27(f23(f27(f23(f7(f29(x31141,a1,x31142)),f22(x31143,x31144)),x31143),f22(x31145,x31146)),x31145),a2)),
% 59.96/59.99 inference(scs_inference,[],[86,3091,2301,2,3])).
% 59.96/59.99 cnf(3136,plain,
% 59.96/59.99 (E(a2,f27(f23(f27(f23(f7(f29(x31361,a1,x31362)),f22(x31363,x31364)),x31363),f22(x31365,x31366)),x31365))),
% 59.96/59.99 inference(scs_inference,[],[3114,2])).
% 59.96/59.99 cnf(3810,plain,
% 59.96/59.99 (E(f25(f23(x38101,f22(x38102,x38103)),x38102),x38103)),
% 59.96/59.99 inference(rename_variables,[],[87])).
% 59.96/59.99 cnf(3812,plain,
% 59.96/59.99 (E(x38121,f27(f23(f27(f23(x38121,f22(x38122,x38123)),x38122),f22(x38124,x38125)),x38124))),
% 59.96/59.99 inference(rename_variables,[],[2220])).
% 59.96/59.99 cnf(3813,plain,
% 59.96/59.99 (P4(f6(x38131,f27(f23(f25(f23(x38132,f22(x38133,x38134)),x38133),f22(x38135,x38136)),x38135)),x38134)),
% 59.96/59.99 inference(scs_inference,[],[87,3810,2220,1316,2127,2342,3,47,60])).
% 59.96/59.99 cnf(3815,plain,
% 59.96/59.99 (P1(f27(f23(f27(f23(f5(a1,x38151),f22(x38152,x38153)),x38152),f22(x38154,x38155)),x38154),f5(a1,x38156))),
% 59.96/59.99 inference(scs_inference,[],[87,3810,2220,3812,1316,2127,2342,3,47,60,46])).
% 59.96/59.99 cnf(3816,plain,
% 59.96/59.99 (E(x38161,f27(f23(f27(f23(x38161,f22(x38162,x38163)),x38162),f22(x38164,x38165)),x38164))),
% 59.96/59.99 inference(rename_variables,[],[2220])).
% 59.96/59.99 cnf(3818,plain,
% 59.96/59.99 (E(x38181,f27(f23(f27(f23(x38181,f22(x38182,x38183)),x38182),f22(x38184,x38185)),x38184))),
% 59.96/59.99 inference(rename_variables,[],[2220])).
% 59.96/59.99 cnf(3819,plain,
% 59.96/59.99 (P1(f21(f6(x38191,x38192),x38192),f27(f23(f21(f6(f21(f6(x38191,x38193),x38193),x38194),x38194),f22(x38195,x38196)),x38195))),
% 59.96/59.99 inference(scs_inference,[],[87,3810,2220,3812,3816,344,1316,2127,2164,2342,1222,3,47,60,46,62,126])).
% 59.96/59.99 cnf(3823,plain,
% 59.96/59.99 (E(x38231,f27(f23(f27(f23(x38231,f22(x38232,x38233)),x38232),f22(x38234,x38235)),x38234))),
% 59.96/59.99 inference(rename_variables,[],[2220])).
% 59.96/59.99 cnf(3825,plain,
% 59.96/59.99 (E(x38251,f27(f23(f27(f23(x38251,f22(x38252,x38253)),x38252),f22(x38254,x38255)),x38254))),
% 59.96/59.99 inference(rename_variables,[],[2220])).
% 59.96/59.99 cnf(3831,plain,
% 59.96/59.99 (E(f5(a1,x38311),f27(f23(f27(f23(a1,f22(x38312,x38313)),x38312),f22(x38314,x38315)),x38314))),
% 59.96/59.99 inference(scs_inference,[],[87,3810,2220,3812,3816,3818,3823,3825,344,1316,2127,2164,1278,2342,1222,1269,98,3,47,60,46,62,126,51,66,50,2,121,147])).
% 59.96/59.99 cnf(3851,plain,
% 59.96/59.99 (E(f27(f23(f27(f23(a1,f22(x38511,x38512)),x38511),f22(x38513,x38514)),x38513),f5(a1,x38515))),
% 59.96/59.99 inference(scs_inference,[],[3831,2])).
% 59.96/59.99 cnf(3854,plain,
% 59.96/59.99 (E(f25(f23(x38541,f22(x38542,a2)),x38542),f27(f23(f27(f23(f7(f29(x38543,a1,x38544)),f22(x38545,x38546)),x38545),f22(x38547,x38548)),x38547))),
% 59.96/59.99 inference(scs_inference,[],[87,3136,3819,3831,2,121,3])).
% 59.96/59.99 cnf(3855,plain,
% 59.96/59.99 (E(f25(f23(x38551,f22(x38552,x38553)),x38552),x38553)),
% 59.96/59.99 inference(rename_variables,[],[87])).
% 59.96/59.99 cnf(3856,plain,
% 59.96/59.99 (E(f27(f23(f25(f23(x38561,f22(x38562,x38563)),x38562),f22(x38564,x38565)),x38564),x38563)),
% 59.96/59.99 inference(scs_inference,[],[87,3136,97,3819,3813,3831,2,121,3,137])).
% 59.96/59.99 cnf(3859,plain,
% 59.96/59.99 (P1(f27(f23(f25(f23(x38591,f22(x38592,x38593)),x38592),f22(x38594,x38595)),x38594),x38593)),
% 59.96/59.99 inference(scs_inference,[],[87,3855,2162,3136,97,3819,3813,3831,2,121,3,137,47])).
% 59.96/59.99 cnf(3860,plain,
% 59.96/59.99 (P1(f27(f23(x38601,f22(x38602,x38603)),x38602),x38601)),
% 59.96/59.99 inference(rename_variables,[],[2162])).
% 59.96/59.99 cnf(3861,plain,
% 59.96/59.99 (P1(f21(f6(f8(f29(x38611,a1,x38612)),x38613),x38613),f29(x38611,a1,a3))),
% 59.96/59.99 inference(scs_inference,[],[87,3855,2193,2162,3860,3136,97,3819,3813,3831,2,121,3,137,47,46])).
% 59.96/59.99 cnf(3862,plain,
% 59.96/59.99 (P1(f27(f23(x38621,f22(x38622,x38623)),x38622),x38621)),
% 59.96/59.99 inference(rename_variables,[],[2162])).
% 59.96/59.99 cnf(3864,plain,
% 59.96/59.99 (E(x38641,f27(f23(f27(f23(x38641,f22(x38642,x38643)),x38642),f22(x38644,x38645)),x38644))),
% 59.96/59.99 inference(rename_variables,[],[2220])).
% 59.96/59.99 cnf(3869,plain,
% 59.96/59.99 (E(x38691,f27(f23(f27(f23(x38691,f22(x38692,x38693)),x38692),f22(x38694,x38695)),x38694))),
% 59.96/59.99 inference(rename_variables,[],[2220])).
% 59.96/59.99 cnf(3871,plain,
% 59.96/59.99 (E(x38711,f27(f23(f27(f23(x38711,f22(x38712,x38713)),x38712),f22(x38714,x38715)),x38714))),
% 59.96/59.99 inference(rename_variables,[],[2220])).
% 59.96/59.99 cnf(3875,plain,
% 59.96/59.99 (E(f5(a1,x38751),f27(f23(f27(f23(f5(a1,x38752),f22(x38753,x38754)),x38753),f22(x38755,x38756)),x38755))),
% 59.96/59.99 inference(scs_inference,[],[87,3855,2193,2220,3864,3869,3871,2162,3860,3862,1295,312,3136,1273,97,3819,3813,3831,1275,303,98,2,121,3,137,47,46,62,126,60,51,50,53,147])).
% 59.96/59.99 cnf(3886,plain,
% 59.96/59.99 (E(x38861,f27(f23(f25(f23(x38862,f22(x38863,x38861)),x38863),f22(x38864,x38865)),x38864))),
% 59.96/59.99 inference(scs_inference,[],[3856,2])).
% 59.96/59.99 cnf(3889,plain,
% 59.96/59.99 (E(f25(f23(x38891,f22(x38892,f29(x38893,a1,a3))),x38892),f8(f29(x38893,a1,x38894)))),
% 59.96/59.99 inference(scs_inference,[],[87,378,3815,3856,2,121,3])).
% 59.96/59.99 cnf(3890,plain,
% 59.96/59.99 (E(f25(f23(x38901,f22(x38902,x38903)),x38902),x38903)),
% 59.96/59.99 inference(rename_variables,[],[87])).
% 59.96/59.99 cnf(3892,plain,
% 59.96/59.99 (P1(f27(f23(f27(f23(x38921,f22(x38922,x38923)),x38922),f22(x38924,x38925)),x38924),x38921)),
% 59.96/59.99 inference(rename_variables,[],[2195])).
% 59.96/59.99 cnf(3894,plain,
% 59.96/59.99 (P1(f27(f23(f27(f23(f25(f23(x38941,f22(x38942,x38943)),x38942),f22(x38944,x38945)),x38944),f22(x38946,x38947)),x38946),x38943)),
% 59.96/59.99 inference(scs_inference,[],[87,3890,2195,3892,312,378,3815,3856,2,121,3,126,47])).
% 59.96/59.99 cnf(3898,plain,
% 59.96/59.99 (P1(x38981,f27(f23(f27(f23(f25(f23(x38982,f22(x38983,x38981)),x38983),f22(x38984,x38985)),x38984),f22(x38986,x38987)),x38986))),
% 59.96/59.99 inference(scs_inference,[],[87,3890,2195,3892,2197,312,378,3815,3856,168,2,121,3,126,47,62,46])).
% 59.96/59.99 cnf(3915,plain,
% 59.96/59.99 (P1(f27(f23(f21(f6(a2,x39151),x39151),f22(x39152,x39153)),x39152),x39154)),
% 59.96/59.99 inference(scs_inference,[],[2162,270,3859,3854,2,121,126])).
% 59.96/59.99 cnf(3916,plain,
% 59.96/59.99 (P1(f27(f23(x39161,f22(x39162,x39163)),x39162),x39161)),
% 59.96/59.99 inference(rename_variables,[],[2162])).
% 59.96/59.99 cnf(3918,plain,
% 59.96/59.99 (E(f25(f23(x39181,f22(x39182,f8(f29(x39183,a1,x39184)))),x39182),f29(x39183,a1,a3))),
% 59.96/59.99 inference(scs_inference,[],[87,2162,270,91,3859,3854,2,121,126,3])).
% 59.96/59.99 cnf(3920,plain,
% 59.96/59.99 (P1(f6(f6(x39201,x39202),x39203),f27(f23(f27(f23(f6(f6(x39201,x39203),x39202),f22(x39204,x39205)),x39204),f22(x39206,x39207)),x39206))),
% 59.96/59.99 inference(scs_inference,[],[87,2220,2162,1737,270,91,3859,3854,2,121,126,3,47])).
% 59.96/59.99 cnf(3921,plain,
% 59.96/59.99 (E(x39211,f27(f23(f27(f23(x39211,f22(x39212,x39213)),x39212),f22(x39214,x39215)),x39214))),
% 59.96/59.99 inference(rename_variables,[],[2220])).
% 59.96/59.99 cnf(3923,plain,
% 59.96/59.99 (E(x39231,f27(f23(f27(f23(x39231,f22(x39232,x39233)),x39232),f22(x39234,x39235)),x39234))),
% 59.96/59.99 inference(rename_variables,[],[2220])).
% 59.96/59.99 cnf(3924,plain,
% 59.96/59.99 (P1(f29(x39241,a1,a3),f21(f6(f8(f29(x39241,a1,x39242)),x39243),x39243))),
% 59.96/59.99 inference(scs_inference,[],[87,2160,2220,3921,2162,3916,1737,270,91,1711,3859,3854,2,121,126,3,47,60,46])).
% 59.96/59.99 cnf(3928,plain,
% 59.96/59.99 (P9(a1,f27(f23(f27(f23(f21(f6(f5(a1,x39281),x39282),x39282),f22(x39283,x39284)),x39283),f22(x39285,x39286)),x39285))),
% 59.96/59.99 inference(scs_inference,[],[87,2160,2220,3921,3923,2162,3916,1737,1252,270,91,1711,3859,3854,100,2,121,126,3,47,60,46,67,51])).
% 59.96/59.99 cnf(3929,plain,
% 59.96/59.99 (E(x39291,f27(f23(f27(f23(x39291,f22(x39292,x39293)),x39292),f22(x39294,x39295)),x39294))),
% 59.96/59.99 inference(rename_variables,[],[2220])).
% 59.96/59.99 cnf(3934,plain,
% 59.96/59.99 (E(f6(f6(x39341,x39342),x39343),f27(f23(f27(f23(f6(f6(x39341,x39343),x39342),f22(x39344,x39345)),x39344),f22(x39346,x39347)),x39346))),
% 59.96/59.99 inference(scs_inference,[],[87,2160,2220,3921,3923,3929,2162,3916,1737,1252,270,91,1711,97,3859,3854,100,2,121,126,3,47,60,46,67,51,50,136,137])).
% 59.96/59.99 cnf(3968,plain,
% 59.96/59.99 (E(f25(f23(x39681,f22(x39682,f29(x39683,a1,a3))),x39682),f27(f23(f8(f29(x39683,a1,x39684)),f22(x39685,x39686)),x39685))),
% 59.96/59.99 inference(scs_inference,[],[87,2195,270,583,3920,3934,2,121,126,3])).
% 59.96/59.99 cnf(3969,plain,
% 59.96/59.99 (E(f25(f23(x39691,f22(x39692,x39693)),x39692),x39693)),
% 59.96/59.99 inference(rename_variables,[],[87])).
% 59.96/59.99 cnf(3970,plain,
% 59.96/59.99 (P1(f8(f29(x39701,a1,x39702)),f21(f6(f8(f29(x39701,a1,x39703)),x39704),x39704))),
% 59.96/59.99 inference(scs_inference,[],[87,659,2164,2195,270,583,3920,3934,2,121,126,3,47])).
% 59.96/59.99 cnf(3971,plain,
% 59.96/59.99 (P1(x39711,f27(f23(x39711,f22(x39712,x39713)),x39712))),
% 59.96/59.99 inference(rename_variables,[],[2164])).
% 59.96/59.99 cnf(3972,plain,
% 59.96/59.99 (P1(x39721,f27(f23(f25(f23(x39722,f22(x39723,x39721)),x39723),f22(x39724,x39725)),x39724))),
% 59.96/59.99 inference(scs_inference,[],[87,3969,659,2164,3971,2195,270,583,3920,3934,2,121,126,3,47,46])).
% 59.96/59.99 cnf(3975,plain,
% 59.96/59.99 (E(x39751,f27(f23(f27(f23(x39751,f22(x39752,x39753)),x39752),f22(x39754,x39755)),x39754))),
% 59.96/59.99 inference(rename_variables,[],[2220])).
% 59.96/59.99 cnf(3977,plain,
% 59.96/59.99 (E(x39771,f27(f23(f27(f23(x39771,f22(x39772,x39773)),x39772),f22(x39774,x39775)),x39774))),
% 59.96/59.99 inference(rename_variables,[],[2220])).
% 59.96/59.99 cnf(3978,plain,
% 59.96/59.99 (P9(f27(f23(f27(f23(f21(f6(f5(a1,x39781),x39782),x39782),f22(x39783,x39784)),x39783),f22(x39785,x39786)),x39785),a1)),
% 59.96/59.99 inference(scs_inference,[],[87,3969,659,2220,3975,3977,2164,3971,2195,1254,270,583,241,3920,3934,2,121,126,3,47,46,60,51,50])).
% 59.96/59.99 cnf(3979,plain,
% 59.96/59.99 (E(x39791,f27(f23(f27(f23(x39791,f22(x39792,x39793)),x39792),f22(x39794,x39795)),x39794))),
% 59.96/59.99 inference(rename_variables,[],[2220])).
% 59.96/59.99 cnf(3980,plain,
% 59.96/59.99 (P7(f27(f23(f27(f23(f5(f23(x39801,f22(x39802,x39803)),f21(f6(a2,x39804),x39804)),f22(x39805,x39806)),x39805),f22(x39807,x39808)),x39807))),
% 59.96/59.99 inference(scs_inference,[],[87,3969,659,2220,3975,3977,3979,2164,3971,2195,1254,270,583,241,3920,3934,2564,2,121,126,3,47,46,60,51,50,53])).
% 59.96/59.99 cnf(3982,plain,
% 59.96/59.99 (E(f21(f6(x39821,x39822),x39822),f27(f23(f27(f23(f21(f6(x39821,x39823),x39823),f22(x39824,x39825)),x39824),f22(x39826,x39827)),x39826))),
% 59.96/59.99 inference(scs_inference,[],[87,3969,659,2220,3975,3977,3979,2164,3971,2195,1254,270,583,97,241,3920,3934,2564,2,121,126,3,47,46,60,51,50,53,137])).
% 59.96/59.99 cnf(4001,plain,
% 59.96/59.99 (P1(f27(f23(a2,f22(x40011,x40012)),x40011),x40013)),
% 59.96/59.99 inference(scs_inference,[],[2162,79,3915,3889,121,2,126])).
% 59.96/59.99 cnf(4004,plain,
% 59.96/59.99 (E(f25(f23(x40041,f22(x40042,a2)),x40042),f7(f29(x40043,a1,x40044)))),
% 59.96/59.99 inference(scs_inference,[],[87,2162,79,333,3915,3889,121,2,126,3])).
% 59.96/59.99 cnf(4005,plain,
% 59.96/59.99 (E(f25(f23(x40051,f22(x40052,x40053)),x40052),x40053)),
% 59.96/59.99 inference(rename_variables,[],[87])).
% 59.96/59.99 cnf(4007,plain,
% 59.96/59.99 (E(x40071,f27(f23(f27(f23(x40071,f22(x40072,x40073)),x40072),f22(x40074,x40075)),x40074))),
% 59.96/59.99 inference(rename_variables,[],[2220])).
% 59.96/59.99 cnf(4009,plain,
% 59.96/59.99 (P4(f6(x40091,f25(f23(x40092,f22(x40093,x40094)),x40093)),x40094)),
% 59.96/59.99 inference(scs_inference,[],[87,4005,2220,2162,79,232,333,3915,3889,381,167,121,2,126,3,47,54,60])).
% 59.96/59.99 cnf(4011,plain,
% 59.96/59.99 (P1(f27(f23(f27(f23(f6(f6(x40111,x40112),x40113),f22(x40114,x40115)),x40114),f22(x40116,x40117)),x40116),f6(f6(x40111,x40113),x40112))),
% 59.96/59.99 inference(scs_inference,[],[87,4005,2220,4007,2162,1737,79,232,333,3915,3889,381,167,121,2,126,3,47,54,60,46])).
% 59.96/59.99 cnf(4012,plain,
% 59.96/59.99 (E(x40121,f27(f23(f27(f23(x40121,f22(x40122,x40123)),x40122),f22(x40124,x40125)),x40124))),
% 59.96/59.99 inference(rename_variables,[],[2220])).
% 59.96/59.99 cnf(4014,plain,
% 59.96/59.99 (E(x40141,f27(f23(f27(f23(x40141,f22(x40142,x40143)),x40142),f22(x40144,x40145)),x40144))),
% 59.96/59.99 inference(rename_variables,[],[2220])).
% 59.96/59.99 cnf(4021,plain,
% 59.96/59.99 (~E(f27(f23(a2,f22(x40211,x40212)),x40211),f7(f29(a9,a14,a15)))),
% 59.96/59.99 inference(scs_inference,[],[87,4005,101,2220,4007,4012,4014,2162,1737,1226,79,232,86,333,3915,3889,381,167,3980,121,2,126,3,47,54,60,46,51,50,53,136,64])).
% 59.96/59.99 cnf(4043,plain,
% 59.96/59.99 (P1(f27(f23(f7(f29(x40431,a1,x40432)),f22(x40433,x40434)),x40433),x40435)),
% 59.96/59.99 inference(scs_inference,[],[2162,1342,3918,3972,121,2,126])).
% 59.96/59.99 cnf(4046,plain,
% 59.96/59.99 (E(f25(f23(x40461,f22(x40462,f7(f29(x40463,a1,x40464)))),x40462),a2)),
% 59.96/59.99 inference(scs_inference,[],[87,2162,1342,88,3918,3972,121,2,126,3])).
% 59.96/59.99 cnf(4080,plain,
% 59.96/59.99 (E(f27(f23(f27(f23(f21(f6(x40801,x40802),x40802),f22(x40803,x40804)),x40803),f22(x40805,x40806)),x40805),f21(f6(x40801,x40807),x40807))),
% 59.96/59.99 inference(scs_inference,[],[3982,3970,121,2])).
% 59.96/59.99 cnf(4084,plain,
% 59.96/59.99 (E(f25(f23(x40841,f22(x40842,a2)),x40842),f21(f6(f7(f29(x40843,a1,x40844)),x40845),x40845))),
% 59.96/59.99 inference(scs_inference,[],[87,2195,1342,557,3982,3970,121,2,126,3])).
% 59.96/59.99 cnf(4087,plain,
% 59.96/59.99 (E(x40871,f27(f23(f27(f23(x40871,f22(x40872,x40873)),x40872),f22(x40874,x40875)),x40874))),
% 59.96/59.99 inference(rename_variables,[],[2220])).
% 59.96/59.99 cnf(4088,plain,
% 59.96/59.99 (P1(f27(f23(f27(f23(f21(f6(x40881,x40882),x40882),f22(x40883,x40884)),x40883),f22(x40885,x40886)),x40885),f21(f6(x40881,x40887),x40887))),
% 59.96/59.99 inference(scs_inference,[],[87,2220,4087,2195,1342,232,1279,557,3982,3970,121,2,126,3,47,46])).
% 59.96/59.99 cnf(4109,plain,
% 59.96/59.99 (~E(f23(x41091,f22(x41092,x41093)),f27(f23(f27(f23(a1,f22(x41094,x41095)),x41094),f22(x41096,x41097)),x41096))),
% 59.96/59.99 inference(scs_inference,[],[2195,1230,3968,3851,4001,255,121,2,126,3])).
% 59.96/59.99 cnf(4111,plain,
% 59.96/59.99 (P1(a1,f27(f23(f27(f23(f5(a1,x41111),f22(x41112,x41113)),x41112),f22(x41114,x41115)),x41114))),
% 59.96/59.99 inference(scs_inference,[],[2220,2195,1230,1308,3968,3851,4001,255,121,2,126,3,47])).
% 59.96/59.99 cnf(4131,plain,
% 59.96/59.99 (P1(f27(f23(a1,f22(x41311,x41312)),x41311),f21(f6(f5(a1,x41313),x41314),x41314))),
% 59.96/59.99 inference(scs_inference,[],[2162,1230,3898,4084,121,2,126])).
% 59.96/59.99 cnf(4136,plain,
% 59.96/59.99 (P1(f21(f6(f8(f29(x41361,a1,x41362)),x41363),x41363),f27(f23(f29(x41361,a1,a3),f22(x41364,x41365)),x41364))),
% 59.96/59.99 inference(scs_inference,[],[2240,2162,408,232,1230,3898,4109,4084,121,2,126,3,47])).
% 59.96/59.99 cnf(4137,plain,
% 59.96/59.99 (P1(f21(f6(x41371,x41372),x41372),f21(f6(x41371,x41373),x41373))),
% 59.96/59.99 inference(rename_variables,[],[232])).
% 59.96/59.99 cnf(4140,plain,
% 59.96/59.99 (P9(f27(f23(f25(f23(x41401,f22(x41402,x41403)),x41402),f22(x41404,x41405)),x41404),x41403)),
% 59.96/59.99 inference(scs_inference,[],[87,2240,2162,408,232,4137,2133,1230,3898,4109,4084,121,2,126,3,47,46,51])).
% 59.96/59.99 cnf(4156,plain,
% 59.96/59.99 (P1(f27(f23(f27(f23(f21(f6(f5(a1,x41561),x41562),x41562),f22(x41563,x41564)),x41563),f22(x41565,x41566)),x41565),f5(a1,x41567))),
% 59.96/59.99 inference(scs_inference,[],[2195,1279,4043,4004,121,2,126])).
% 59.96/59.99 cnf(4159,plain,
% 59.96/59.99 (E(f25(f23(x41591,f22(x41592,x41593)),x41592),f27(f23(f25(f23(x41594,f22(x41595,x41593)),x41595),f22(x41596,x41597)),x41596))),
% 59.96/59.99 inference(scs_inference,[],[87,2195,1279,4043,3886,4004,121,2,126,3])).
% 59.96/59.99 cnf(4161,plain,
% 59.96/59.99 (P1(f5(a1,x41611),f27(f23(f27(f23(f21(f6(f5(a1,x41612),x41613),x41613),f22(x41614,x41615)),x41614),f22(x41616,x41617)),x41616))),
% 59.96/59.99 inference(scs_inference,[],[87,2220,2195,1279,1280,4043,3886,4004,121,2,126,3,47])).
% 59.96/59.99 cnf(4162,plain,
% 59.96/59.99 (E(x41621,f27(f23(f27(f23(x41621,f22(x41622,x41623)),x41622),f22(x41624,x41625)),x41624))),
% 59.96/59.99 inference(rename_variables,[],[2220])).
% 59.96/59.99 cnf(4163,plain,
% 59.96/59.99 (P1(f27(f23(f27(f23(f5(a1,x41631),f22(x41632,x41633)),x41632),f22(x41634,x41635)),x41634),f21(f6(f5(a1,x41636),x41637),x41637))),
% 59.96/59.99 inference(scs_inference,[],[87,2220,4162,2195,1279,1280,4043,3886,4004,121,2,126,3,47,46])).
% 59.96/59.99 cnf(4180,plain,
% 59.96/59.99 (E(f27(f23(f25(f23(x41801,f22(x41802,x41803)),x41802),f22(x41804,x41805)),x41804),f25(f23(x41806,f22(x41807,x41803)),x41807))),
% 59.96/59.99 inference(scs_inference,[],[3861,4159,121,2])).
% 59.96/59.99 cnf(4181,plain,
% 59.96/59.99 (P1(f27(f23(f21(f6(f5(a1,x41811),x41812),x41812),f22(x41813,x41814)),x41813),f5(a1,x41815))),
% 59.96/59.99 inference(scs_inference,[],[2162,1279,3861,4159,121,2,126])).
% 59.96/59.99 cnf(4184,plain,
% 59.96/59.99 (P1(f21(f6(f5(a1,x41841),x41842),x41842),f27(f23(f27(f23(a1,f22(x41843,x41844)),x41843),f22(x41845,x41846)),x41845))),
% 59.96/59.99 inference(scs_inference,[],[2220,2162,1279,1228,3861,4159,121,2,126,47])).
% 59.96/59.99 cnf(4185,plain,
% 59.96/59.99 (E(x41851,f27(f23(f27(f23(x41851,f22(x41852,x41853)),x41852),f22(x41854,x41855)),x41854))),
% 59.96/59.99 inference(rename_variables,[],[2220])).
% 59.96/59.99 cnf(4186,plain,
% 59.96/59.99 (P1(f27(f23(f27(f23(f21(f6(f5(a1,x41861),x41862),x41862),f22(x41863,x41864)),x41863),f22(x41865,x41866)),x41865),a1)),
% 59.96/59.99 inference(scs_inference,[],[2220,4185,2162,1279,1228,3861,4159,121,2,126,47,46])).
% 59.96/59.99 cnf(4188,plain,
% 59.96/59.99 (P9(a2,f7(f29(x41881,a1,x41882)))),
% 59.96/59.99 inference(scs_inference,[],[1427,2220,4185,2162,245,1279,1228,3861,4159,121,2,126,47,46,51])).
% 59.96/59.99 cnf(4205,plain,
% 59.96/59.99 (P1(f25(f23(x42051,f22(x42052,x42053)),x42052),x42053)),
% 59.96/59.99 inference(scs_inference,[],[2197,3924,3894,3875,121,2,126])).
% 59.96/59.99 cnf(4209,plain,
% 59.96/59.99 (~E(f23(x42091,f22(x42092,x42093)),f27(f23(f27(f23(f5(a1,x42094),f22(x42095,x42096)),x42095),f22(x42097,x42098)),x42097))),
% 59.96/59.99 inference(scs_inference,[],[2197,3924,3894,3875,255,121,2,126,3])).
% 59.96/59.99 cnf(4210,plain,
% 59.96/59.99 (P1(f5(a1,x42101),f27(f23(f27(f23(a1,f22(x42102,x42103)),x42102),f22(x42104,x42105)),x42104))),
% 59.96/59.99 inference(scs_inference,[],[2220,2197,1306,3924,3894,3875,255,121,2,126,3,47])).
% 59.96/59.99 cnf(4211,plain,
% 59.96/59.99 (E(x42111,f27(f23(f27(f23(x42111,f22(x42112,x42113)),x42112),f22(x42114,x42115)),x42114))),
% 59.96/59.99 inference(rename_variables,[],[2220])).
% 59.96/59.99 cnf(4212,plain,
% 59.96/59.99 (P1(f27(f23(f27(f23(f5(a1,x42121),f22(x42122,x42123)),x42122),f22(x42124,x42125)),x42124),a1)),
% 59.96/59.99 inference(scs_inference,[],[2220,4211,2197,1306,3924,3894,3875,255,121,2,126,3,47,46])).
% 59.96/59.99 cnf(4233,plain,
% 59.96/59.99 (P1(x42331,f21(f6(x42331,x42332),x42332))),
% 59.96/59.99 inference(rename_variables,[],[194])).
% 59.96/59.99 cnf(4234,plain,
% 59.96/59.99 (P1(x42341,f21(f6(f25(f23(x42342,f22(x42343,x42341)),x42343),x42344),x42344))),
% 59.96/59.99 inference(scs_inference,[],[87,2240,408,194,4233,4136,4209,4046,121,2,3,47,46])).
% 59.96/59.99 cnf(4236,plain,
% 59.96/59.99 (P9(f21(f6(a2,x42361),x42361),f7(f29(x42362,a1,x42363)))),
% 59.96/59.99 inference(scs_inference,[],[87,2240,1427,408,194,4233,268,4136,4209,4046,121,2,3,47,46,51])).
% 59.96/59.99 cnf(4240,plain,
% 59.96/59.99 (P1(f27(f23(f27(f23(f8(f29(x42401,a1,x42402)),f22(x42403,x42404)),x42403),f22(x42405,x42406)),x42405),f27(f23(f29(x42401,a1,a3),f22(x42407,x42408)),x42407))),
% 59.96/59.99 inference(scs_inference,[],[87,2240,1427,408,2195,194,4233,268,200,4136,4209,4046,121,2,3,47,46,51,50,126])).
% 59.96/59.99 cnf(4254,plain,
% 59.96/59.99 (P1(f27(f23(a1,f22(x42541,x42542)),x42541),f5(a1,x42543))),
% 59.96/59.99 inference(scs_inference,[],[2162,1308,4163,121,126])).
% 59.96/59.99 cnf(4258,plain,
% 59.96/59.99 (P1(f21(f6(x42581,x42582),x42582),x42581)),
% 59.96/59.99 inference(rename_variables,[],[196])).
% 59.96/59.99 cnf(4259,plain,
% 59.96/59.99 (P1(f27(f23(f29(x42591,a1,a3),f22(x42592,x42593)),x42592),f8(f29(x42591,a1,x42594)))),
% 59.96/59.99 inference(scs_inference,[],[87,2240,2162,1308,196,4258,4163,121,126,47,46])).
% 59.96/59.99 cnf(4263,plain,
% 59.96/59.99 (P9(f7(f29(x42631,a1,x42632)),f21(f6(a2,x42633),x42633))),
% 59.96/59.99 inference(scs_inference,[],[87,2240,1427,2162,1308,196,4258,235,278,4163,121,126,47,46,51,50])).
% 59.96/59.99 cnf(4276,plain,
% 59.96/59.99 (P1(f29(x42761,a1,a3),f8(f29(x42761,a1,x42762)))),
% 59.96/59.99 inference(scs_inference,[],[2164,4156,4259,121,126])).
% 59.96/59.99 cnf(4299,plain,
% 59.96/59.99 (P1(f27(f23(f27(f23(f29(x42991,a1,a3),f22(x42992,x42993)),x42992),f22(x42994,x42995)),x42994),f8(f29(x42991,a1,x42996)))),
% 59.96/59.99 inference(scs_inference,[],[2195,4184,4276,121,126])).
% 59.96/59.99 cnf(4300,plain,
% 59.96/59.99 (P1(f27(f23(f27(f23(x43001,f22(x43002,x43003)),x43002),f22(x43004,x43005)),x43004),x43001)),
% 59.96/59.99 inference(rename_variables,[],[2195])).
% 59.96/59.99 cnf(4302,plain,
% 59.96/59.99 (P1(x43021,f25(f23(x43022,f22(x43023,x43021)),x43023))),
% 59.96/59.99 inference(scs_inference,[],[83,2195,4184,4234,4276,121,126,47])).
% 59.96/59.99 cnf(4305,plain,
% 59.96/59.99 (P1(f8(f29(x43051,a1,x43052)),f29(x43051,a1,a3))),
% 59.96/59.99 inference(scs_inference,[],[83,2718,2195,4300,4184,4234,4276,121,126,47,46])).
% 59.96/59.99 cnf(4322,plain,
% 59.96/59.99 (P1(f27(f23(f12(f16(f29(a9,a14,a15)),f7(f29(a9,a14,a15))),f22(x43221,x43222)),x43221),f7(f29(a9,a14,a15)))),
% 59.96/59.99 inference(scs_inference,[],[2162,1095,4161,121,126])).
% 59.96/59.99 cnf(4325,plain,
% 59.96/59.99 (P1(f27(f23(a1,f22(x43251,x43252)),x43251),f27(f23(f27(f23(f5(a1,x43253),f22(x43254,x43255)),x43254),f22(x43256,x43257)),x43256))),
% 59.96/59.99 inference(scs_inference,[],[2220,2162,1095,4161,4254,121,126,47])).
% 59.96/59.99 cnf(4344,plain,
% 59.96/59.99 (P1(f27(f23(f27(f23(f8(f29(x43441,a1,x43442)),f22(x43443,x43444)),x43443),f22(x43445,x43446)),x43445),f29(x43441,a1,a3))),
% 59.96/59.99 inference(scs_inference,[],[2195,4210,4305,121,126])).
% 59.96/59.99 cnf(4347,plain,
% 59.96/59.99 (P1(f27(f23(f21(f6(f5(a1,x43471),x43472),x43472),f22(x43473,x43474)),x43473),a1)),
% 59.96/59.99 inference(scs_inference,[],[78,2195,4210,4181,4305,121,126,47])).
% 59.96/59.99 cnf(4367,plain,
% 59.96/59.99 (E(x43671,f25(f23(x43672,f22(x43673,x43671)),x43673))),
% 59.96/59.99 inference(rename_variables,[],[265])).
% 59.96/59.99 cnf(4369,plain,
% 59.96/59.99 (E(x43691,f25(f23(x43692,f22(x43693,x43691)),x43693))),
% 59.96/59.99 inference(rename_variables,[],[265])).
% 59.96/59.99 cnf(4371,plain,
% 59.96/59.99 (E(x43711,f25(f23(x43712,f22(x43713,x43711)),x43713))),
% 59.96/59.99 inference(rename_variables,[],[265])).
% 59.96/59.99 cnf(4372,plain,
% 59.96/59.99 (P1(f27(f23(f21(f6(f6(f6(x43721,x43722),x43723),x43724),x43724),f22(x43725,x43726)),x43725),f6(f6(x43721,x43723),x43722))),
% 59.96/59.99 inference(scs_inference,[],[265,4367,4369,2162,1273,1721,4186,1222,1789,121,66,62,60,126])).
% 59.96/59.99 cnf(4376,plain,
% 59.96/59.99 (E(x43761,f25(f23(x43762,f22(x43763,x43761)),x43763))),
% 59.96/59.99 inference(rename_variables,[],[265])).
% 59.96/59.99 cnf(4378,plain,
% 59.96/59.99 (E(x43781,f25(f23(x43782,f22(x43783,x43781)),x43783))),
% 59.96/59.99 inference(rename_variables,[],[265])).
% 59.96/59.99 cnf(4379,plain,
% 59.96/59.99 (P1(f25(f23(x43791,f22(x43792,a1)),x43792),f21(f6(f5(a1,x43793),x43794),x43794))),
% 59.96/59.99 inference(scs_inference,[],[265,4367,4369,4371,4376,4378,2162,1254,1273,1230,1228,1721,4186,1222,1789,121,66,62,60,126,47,51,46])).
% 59.96/59.99 cnf(4380,plain,
% 59.96/59.99 (E(x43801,f25(f23(x43802,f22(x43803,x43801)),x43803))),
% 59.96/59.99 inference(rename_variables,[],[265])).
% 59.96/59.99 cnf(4386,plain,
% 59.96/59.99 (E(f25(f23(x43861,f22(x43862,f5(a1,x43863))),x43862),f25(f23(x43864,f22(x43865,a1)),x43865))),
% 59.96/59.99 inference(scs_inference,[],[87,265,4367,4369,4371,4376,4378,4380,2162,1224,1254,1273,1230,1228,1721,4186,1222,1789,98,121,66,62,60,126,47,51,46,50,147,3])).
% 59.96/59.99 cnf(4390,plain,
% 59.96/59.99 (E(f25(f23(x43901,f22(x43902,a1)),x43902),f5(a1,x43903))),
% 59.96/59.99 inference(scs_inference,[],[87,265,4367,4369,4371,4376,4378,4380,2162,1224,1254,1273,1230,1228,1721,4186,4344,1222,1789,98,121,66,62,60,126,47,51,46,50,147,3,123,2])).
% 59.96/59.99 cnf(4401,plain,
% 59.96/59.99 (~E(f23(x44011,f22(x44012,x44013)),f25(f23(x44014,f22(x44015,a1)),x44015))),
% 59.96/59.99 inference(scs_inference,[],[4111,4386,4390,255,121,2,3])).
% 59.96/59.99 cnf(4426,plain,
% 59.96/59.99 (E(x44261,f27(f23(f27(f23(x44261,f22(x44262,x44263)),x44262),f22(x44264,x44265)),x44264))),
% 59.96/59.99 inference(rename_variables,[],[2220])).
% 59.96/59.99 cnf(4428,plain,
% 59.96/59.99 (E(x44281,f27(f23(f27(f23(x44281,f22(x44282,x44283)),x44282),f22(x44284,x44285)),x44284))),
% 59.96/59.99 inference(rename_variables,[],[2220])).
% 59.96/59.99 cnf(4429,plain,
% 59.96/59.99 (P9(f27(f23(f27(f23(f7(f29(x44291,a1,x44292)),f22(x44293,x44294)),x44293),f22(x44295,x44296)),x44295),f21(f6(a2,x44297),x44297))),
% 59.96/59.99 inference(scs_inference,[],[2185,2220,4426,4428,4131,4180,4254,4305,4401,4236,4263,121,3,47,46,51,50])).
% 59.96/59.99 cnf(4444,plain,
% 59.96/59.99 (E(x44441,f25(f23(x44442,f22(x44443,x44441)),x44443))),
% 59.96/59.99 inference(rename_variables,[],[265])).
% 59.96/59.99 cnf(4452,plain,
% 59.96/59.99 (E(x44521,f25(f23(x44522,f22(x44523,x44521)),x44523))),
% 59.96/59.99 inference(rename_variables,[],[265])).
% 59.96/59.99 cnf(4453,plain,
% 59.96/59.99 (P1(f25(f23(x44531,f22(x44532,a1)),x44532),f5(a1,x44533))),
% 59.96/59.99 inference(scs_inference,[],[265,4444,4452,2164,1220,1308,1306,4163,4181,4401,4386,121,60,126,3,47,46])).
% 59.96/59.99 cnf(4455,plain,
% 59.96/59.99 (P9(f27(f23(f27(f23(f7(f29(x44551,a1,x44552)),f22(x44553,x44554)),x44553),f22(x44555,x44556)),x44555),a2)),
% 59.96/59.99 inference(scs_inference,[],[83,265,4444,4452,2164,1220,1308,1306,4163,4181,4429,4401,4386,121,60,126,3,47,46,51])).
% 59.96/59.99 cnf(4502,plain,
% 59.96/59.99 (P1(f27(f23(f8(f29(x45021,a1,x45022)),f22(x45023,x45024)),x45023),f27(f23(f29(x45021,a1,a3),f22(x45025,x45026)),x45025))),
% 59.96/59.99 inference(scs_inference,[],[2164,4240,121,126])).
% 59.96/59.99 cnf(4526,plain,
% 59.96/59.99 (E(x45261,f21(f6(x45261,x45262),x45262))),
% 59.96/59.99 inference(rename_variables,[],[179])).
% 59.96/59.99 cnf(4527,plain,
% 59.96/59.99 (P6(f23(x45271,f22(f5(a1,x45272),x45273)),f21(f6(a1,x45274),x45274))),
% 59.96/59.99 inference(scs_inference,[],[179,4526,4254,1222,1789,121,66,62])).
% 59.96/59.99 cnf(4562,plain,
% 59.96/59.99 (P1(f27(f23(f6(f6(x45621,x45622),x45623),f22(x45624,x45625)),x45624),f6(f6(x45621,x45623),x45622))),
% 59.96/59.99 inference(scs_inference,[],[2164,4299,4011,121,126])).
% 59.96/59.99 cnf(4566,plain,
% 59.96/59.99 (P1(f27(f23(f27(f23(f5(a1,x45661),f22(x45662,x45663)),x45662),f22(x45664,x45665)),x45664),f25(f23(x45666,f22(x45667,a1)),x45667))),
% 59.96/59.99 inference(scs_inference,[],[265,2164,4299,4212,4011,121,126,47])).
% 59.96/59.99 cnf(4567,plain,
% 59.96/59.99 (E(x45671,f25(f23(x45672,f22(x45673,x45671)),x45673))),
% 59.96/59.99 inference(rename_variables,[],[265])).
% 59.96/59.99 cnf(4569,plain,
% 59.96/59.99 (E(x45691,f25(f23(x45692,f22(x45693,x45691)),x45693))),
% 59.96/59.99 inference(rename_variables,[],[265])).
% 59.96/59.99 cnf(4570,plain,
% 59.96/59.99 (P1(f25(f23(x45701,f22(x45702,a1)),x45702),f27(f23(f27(f23(f5(a1,x45703),f22(x45704,x45705)),x45704),f22(x45706,x45707)),x45706))),
% 59.96/59.99 inference(scs_inference,[],[265,4567,4569,2164,4111,4299,4212,4011,4455,121,126,47,51,46])).
% 59.96/59.99 cnf(4587,plain,
% 59.96/59.99 (E(x45871,f21(f6(x45871,x45872),x45872))),
% 59.96/59.99 inference(rename_variables,[],[179])).
% 59.96/59.99 cnf(4593,plain,
% 59.96/59.99 (E(x45931,f21(f6(x45931,x45932),x45932))),
% 59.96/59.99 inference(rename_variables,[],[179])).
% 59.96/59.99 cnf(4595,plain,
% 59.96/59.99 (E(x45951,f21(f6(x45951,x45952),x45952))),
% 59.96/59.99 inference(rename_variables,[],[179])).
% 59.96/59.99 cnf(4596,plain,
% 59.96/59.99 (P1(f21(f6(a1,x45961),x45961),f21(f6(f5(a1,x45962),x45963),x45963))),
% 59.96/59.99 inference(scs_inference,[],[179,4587,4593,4595,2164,1254,1220,1230,1306,4325,4088,121,60,126,47,51,46])).
% 59.96/59.99 cnf(4619,plain,
% 59.96/59.99 (P1(f21(f6(a1,x46191),x46191),f5(a1,x46192))),
% 59.96/59.99 inference(scs_inference,[],[83,2164,4305,4566,4596,121,126,47])).
% 59.96/59.99 cnf(4637,plain,
% 59.96/59.99 (~P17(f8(f29(x46371,a1,x46372)),f29(x46371,a1,a3))),
% 59.96/59.99 inference(scs_inference,[],[4276,121])).
% 59.96/59.99 cnf(4662,plain,
% 59.96/59.99 (E(x46621,f21(f6(x46621,x46622),x46622))),
% 59.96/59.99 inference(rename_variables,[],[179])).
% 59.96/59.99 cnf(4667,plain,
% 59.96/59.99 (E(x46671,f21(f6(x46671,x46672),x46672))),
% 59.96/59.99 inference(rename_variables,[],[179])).
% 59.96/59.99 cnf(4669,plain,
% 59.96/59.99 (E(x46691,f21(f6(x46691,x46692),x46692))),
% 59.96/59.99 inference(rename_variables,[],[179])).
% 59.96/59.99 cnf(4671,plain,
% 59.96/59.99 (E(x46711,f21(f6(x46711,x46712),x46712))),
% 59.96/59.99 inference(rename_variables,[],[179])).
% 59.96/59.99 cnf(4674,plain,
% 59.96/59.99 (P8(x46741,f21(f6(f27(f23(a2,f22(x46742,x46743)),x46742),x46744),x46744))),
% 59.96/59.99 inference(scs_inference,[],[179,4662,4667,4669,4671,2162,1711,1723,4001,4372,4347,3928,3978,121,60,126,47,51,46,50,136])).
% 59.96/59.99 cnf(4694,plain,
% 59.96/59.99 (P1(f27(f23(f8(f29(x46941,a1,x46942)),f22(x46943,x46944)),x46943),f21(f6(f8(f29(x46941,a1,x46945)),x46946),x46946))),
% 59.96/59.99 inference(scs_inference,[],[2193,2195,4322,4453,4502,121,126,47])).
% 59.96/59.99 cnf(4711,plain,
% 59.96/59.99 (P18(f6(x47111,f21(f6(f5(a1,x47112),x47113),x47113)),f27(f23(a1,f22(x47114,x47115)),x47114))),
% 59.96/59.99 inference(scs_inference,[],[408,4347,1789,121,66])).
% 59.96/59.99 cnf(4712,plain,
% 59.96/59.99 (E(x47121,f27(f23(x47121,f22(x47122,x47123)),x47122))),
% 59.96/59.99 inference(rename_variables,[],[408])).
% 59.96/59.99 cnf(4713,plain,
% 59.96/59.99 (P6(f23(x47131,f22(f6(f6(x47132,x47133),x47134),x47135)),f27(f23(f6(f6(x47132,x47134),x47133),f22(x47136,x47137)),x47136))),
% 59.96/59.99 inference(scs_inference,[],[408,4712,4347,1713,1789,121,66,62])).
% 59.96/59.99 cnf(4714,plain,
% 59.96/59.99 (E(x47141,f27(f23(x47141,f22(x47142,x47143)),x47142))),
% 59.96/59.99 inference(rename_variables,[],[408])).
% 59.96/59.99 cnf(4715,plain,
% 59.96/59.99 (P4(f6(x47151,f5(a1,x47152)),f27(f23(a1,f22(x47153,x47154)),x47153))),
% 59.96/59.99 inference(scs_inference,[],[408,4712,4714,1273,4347,1713,1789,121,66,62,60])).
% 59.96/59.99 cnf(4716,plain,
% 59.96/59.99 (E(x47161,f27(f23(x47161,f22(x47162,x47163)),x47162))),
% 59.96/59.99 inference(rename_variables,[],[408])).
% 59.96/59.99 cnf(4721,plain,
% 59.96/59.99 (E(x47211,f27(f23(x47211,f22(x47212,x47213)),x47212))),
% 59.96/59.99 inference(rename_variables,[],[408])).
% 59.96/59.99 cnf(4723,plain,
% 59.96/59.99 (E(x47231,f27(f23(x47231,f22(x47232,x47233)),x47232))),
% 59.96/59.99 inference(rename_variables,[],[408])).
% 59.96/59.99 cnf(4725,plain,
% 59.96/59.99 (E(x47251,f27(f23(x47251,f22(x47252,x47253)),x47252))),
% 59.96/59.99 inference(rename_variables,[],[408])).
% 59.96/59.99 cnf(4728,plain,
% 59.96/59.99 (E(f6(f6(x47281,x47282),x47283),f27(f23(f6(f6(x47281,x47283),x47282),f22(x47284,x47285)),x47284))),
% 59.96/59.99 inference(scs_inference,[],[408,4712,4714,4716,4721,4723,4725,2162,1737,1273,1224,1226,4347,4379,4212,1713,1789,98,121,66,62,60,126,47,51,46,50,147])).
% 59.96/59.99 cnf(4736,plain,
% 59.96/59.99 (E(f27(f23(f6(f6(x47361,x47362),x47363),f22(x47364,x47365)),x47364),f6(f6(x47361,x47363),x47362))),
% 59.96/59.99 inference(scs_inference,[],[408,4712,4714,4716,4721,4723,4725,2162,1737,1273,1224,1226,97,4347,4379,4212,4694,1713,1789,98,121,66,62,60,126,47,51,46,50,147,137,123,2])).
% 59.96/59.99 cnf(4788,plain,
% 59.96/59.99 (P4(f6(x47881,f5(a1,x47882)),f27(f23(f27(f23(f27(f23(a1,f22(x47883,x47884)),x47883),f22(x47885,x47886)),x47885),f22(x47887,x47888)),x47887))),
% 59.96/59.99 inference(scs_inference,[],[2220,4379,4715,121,60])).
% 59.96/59.99 cnf(4817,plain,
% 59.96/59.99 (P4(f6(x48171,f6(f6(x48172,x48173),x48174)),f27(f23(f6(f6(x48172,x48174),x48173),f22(x48175,x48176)),x48175))),
% 59.96/59.99 inference(scs_inference,[],[408,1711,97,4570,4788,121,137,60])).
% 59.96/59.99 cnf(4818,plain,
% 59.96/59.99 (E(x48181,f27(f23(x48181,f22(x48182,x48183)),x48182))),
% 59.96/59.99 inference(rename_variables,[],[408])).
% 59.96/59.99 cnf(4822,plain,
% 59.96/59.99 (P9(f6(f6(x48221,x48222),x48223),f27(f23(f6(f6(x48221,x48223),x48222),f22(x48224,x48225)),x48224))),
% 59.96/59.99 inference(scs_inference,[],[408,4818,2195,1715,1711,97,4570,4596,4788,121,137,60,126,51])).
% 59.96/59.99 cnf(4965,plain,
% 59.96/59.99 (E(x49651,f27(f23(x49651,f22(x49652,x49653)),x49652))),
% 59.96/59.99 inference(rename_variables,[],[408])).
% 59.96/59.99 cnf(4967,plain,
% 59.96/59.99 (E(x49671,f27(f23(x49671,f22(x49672,x49673)),x49672))),
% 59.96/59.99 inference(rename_variables,[],[408])).
% 59.96/59.99 cnf(4968,plain,
% 59.96/59.99 (P9(f27(f23(a2,f22(x49681,x49682)),x49681),f7(f29(x49683,a1,x49684)))),
% 59.96/59.99 inference(scs_inference,[],[408,4965,4967,2151,4210,4596,4188,121,51,47,50])).
% 59.96/59.99 cnf(4980,plain,
% 59.96/59.99 (P9(f8(f29(a9,a14,a15)),f10(f8(f29(a9,a14,a15))))),
% 59.96/59.99 inference(scs_inference,[],[92,102,104])).
% 59.96/59.99 cnf(4994,plain,
% 59.96/59.99 (~P5(f29(x49941,a1,x49942),x49943)),
% 59.96/59.99 inference(scs_inference,[],[92,4968,2126,4817,4713,98,102,104,118,120,132,133,134,146,152])).
% 59.96/59.99 cnf(5004,plain,
% 59.96/59.99 (P6(f23(f23(x50041,f22(f6(f6(x50042,x50043),x50044),x50045)),f22(x50046,x50047)),f27(f23(f6(f6(x50042,x50044),x50043),f22(x50048,x50049)),x50048))),
% 59.96/59.99 inference(scs_inference,[],[92,4968,2126,4817,4713,4736,98,102,104,118,120,132,133,134,146,152,15,24,28,31,32,39,139,142])).
% 59.96/59.99 cnf(5044,plain,
% 59.96/59.99 (E(f26(f29(x50441,a1,x50442),x50443),f29(x50441,a1,a3))),
% 59.96/59.99 inference(scs_inference,[],[92,4968,2126,4817,4713,4736,212,98,102,104,118,120,132,133,134,146,152,15,24,28,31,32,39,139,142,4,5,7,8,9,11,16,17,18,19,20,21,22,23,25,26,29,30,33,34,35,36,37,38,40,41,42,43,44,45,138,12,14,143,164,151])).
% 59.96/59.99 cnf(5049,plain,
% 59.96/59.99 (P18(f6(x50491,f6(f6(x50492,x50493),x50494)),f27(f23(f6(f6(x50492,x50494),x50493),f22(x50495,x50496)),x50495))),
% 59.96/59.99 inference(scs_inference,[],[92,4968,2126,4205,4817,4713,4736,212,98,102,104,118,120,132,133,134,146,152,15,24,28,31,32,39,139,142,4,5,7,8,9,11,16,17,18,19,20,21,22,23,25,26,29,30,33,34,35,36,37,38,40,41,42,43,44,45,138,12,14,143,164,151,148,6,116])).
% 59.96/59.99 cnf(5054,plain,
% 59.96/59.99 (P4(f16(f29(a9,a14,a15)),f12(f16(f29(a9,a14,a15)),f7(f29(a9,a14,a15))))),
% 59.96/59.99 inference(scs_inference,[],[92,4968,2126,4711,4205,4817,4713,4736,212,98,101,102,104,118,120,132,133,134,146,152,15,24,28,31,32,39,139,142,4,5,7,8,9,11,16,17,18,19,20,21,22,23,25,26,29,30,33,34,35,36,37,38,40,41,42,43,44,45,138,12,14,143,164,151,148,6,116,111,13,124])).
% 59.96/59.99 cnf(5062,plain,
% 59.96/59.99 (~E(a14,a1)),
% 59.96/59.99 inference(scs_inference,[],[92,1369,4968,2126,4711,4205,4817,4713,4736,212,98,101,102,104,118,120,132,133,134,146,152,15,24,28,31,32,39,139,142,4,5,7,8,9,11,16,17,18,19,20,21,22,23,25,26,29,30,33,34,35,36,37,38,40,41,42,43,44,45,138,12,14,143,164,151,148,6,116,111,13,124,103,10,27,136,2])).
% 59.96/59.99 cnf(5064,plain,
% 59.96/59.99 (~P17(x50641,x50641)),
% 59.96/59.99 inference(rename_variables,[],[488])).
% 59.96/59.99 cnf(5068,plain,
% 59.96/59.99 (E(f27(f23(f25(f23(x50681,f22(x50682,x50683)),x50682),f22(x50684,x50685)),x50684),x50683)),
% 59.96/59.99 inference(rename_variables,[],[3856])).
% 59.96/59.99 cnf(5069,plain,
% 59.96/59.99 (~P13(f27(f23(f25(f23(x50691,f22(x50692,a4)),x50692),f22(x50693,x50694)),x50693),x50695)),
% 59.96/59.99 inference(scs_inference,[],[92,488,5064,1369,182,4968,2126,4711,4205,4817,4713,4736,3856,5068,212,98,101,102,104,118,120,132,133,134,146,152,15,24,28,31,32,39,139,142,4,5,7,8,9,11,16,17,18,19,20,21,22,23,25,26,29,30,33,34,35,36,37,38,40,41,42,43,44,45,138,12,14,143,164,151,148,6,116,111,13,124,103,10,27,136,2,48,49,70,75])).
% 59.96/59.99 cnf(5070,plain,
% 59.96/59.99 (E(f27(f23(f25(f23(x50701,f22(x50702,x50703)),x50702),f22(x50704,x50705)),x50704),x50703)),
% 59.96/59.99 inference(rename_variables,[],[3856])).
% 59.96/59.99 cnf(5071,plain,
% 59.96/59.99 (~P11(f21(f6(f5(a1,x50711),x50712),x50712),x50713,x50714)),
% 59.96/59.99 inference(scs_inference,[],[92,488,5064,1369,99,182,4968,2126,4711,4205,4817,4713,1234,4736,3856,5068,212,98,101,102,104,118,120,132,133,134,146,152,15,24,28,31,32,39,139,142,4,5,7,8,9,11,16,17,18,19,20,21,22,23,25,26,29,30,33,34,35,36,37,38,40,41,42,43,44,45,138,12,14,143,164,151,148,6,116,111,13,124,103,10,27,136,2,48,49,70,75,56])).
% 59.96/59.99 cnf(5073,plain,
% 59.96/59.99 (P8(x50731,a2)),
% 59.96/59.99 inference(rename_variables,[],[176])).
% 59.96/59.99 cnf(5074,plain,
% 59.96/59.99 (P4(f6(x50741,f25(f23(x50742,f22(x50743,x50744)),x50743)),x50744)),
% 59.96/59.99 inference(rename_variables,[],[4009])).
% 59.96/59.99 cnf(5077,plain,
% 59.96/59.99 (P8(x50771,a2)),
% 59.96/59.99 inference(rename_variables,[],[176])).
% 59.96/59.99 cnf(5078,plain,
% 59.96/59.99 (P4(f6(x50781,f25(f23(x50782,f22(x50783,x50784)),x50783)),x50784)),
% 59.96/59.99 inference(rename_variables,[],[4009])).
% 59.96/59.99 cnf(5086,plain,
% 59.96/59.99 (~P11(f23(a1,f22(x50861,a1)),x50862,a14)),
% 59.96/59.99 inference(scs_inference,[],[92,488,5064,1369,99,182,4968,2126,4711,4205,4728,4817,4713,4009,5074,5078,176,5073,5077,1234,4736,3856,5068,212,98,101,102,104,118,120,132,133,134,146,152,15,24,28,31,32,39,139,142,4,5,7,8,9,11,16,17,18,19,20,21,22,23,25,26,29,30,33,34,35,36,37,38,40,41,42,43,44,45,138,12,14,143,164,151,148,6,116,111,13,124,103,10,27,136,2,48,49,70,75,56,129,130,131,145,155])).
% 59.96/59.99 cnf(5087,plain,
% 59.96/59.99 (~P11(a1,x50871,x50872)),
% 59.96/59.99 inference(rename_variables,[],[99])).
% 59.96/59.99 cnf(5089,plain,
% 59.96/59.99 (~P11(f23(a1,f22(a1,x50891)),a14,x50892)),
% 59.96/59.99 inference(scs_inference,[],[92,488,5064,1369,99,5087,182,4968,2126,4711,4205,4728,4817,4713,4009,5074,5078,176,5073,5077,1234,4736,3856,5068,212,98,101,102,104,118,120,132,133,134,146,152,15,24,28,31,32,39,139,142,4,5,7,8,9,11,16,17,18,19,20,21,22,23,25,26,29,30,33,34,35,36,37,38,40,41,42,43,44,45,138,12,14,143,164,151,148,6,116,111,13,124,103,10,27,136,2,48,49,70,75,56,129,130,131,145,155,156])).
% 59.96/59.99 cnf(5107,plain,
% 59.96/59.99 (E(f27(f23(f25(f23(x51071,f22(x51072,x51073)),x51072),f22(x51074,x51075)),x51074),x51073)),
% 59.96/59.99 inference(rename_variables,[],[3856])).
% 59.96/59.99 cnf(5109,plain,
% 59.96/59.99 (E(f27(f23(f25(f23(x51091,f22(x51092,x51093)),x51092),f22(x51094,x51095)),x51094),x51093)),
% 59.96/59.99 inference(rename_variables,[],[3856])).
% 59.96/59.99 cnf(5110,plain,
% 59.96/59.99 (~P6(f21(f6(f5(a1,x51101),x51102),x51102),x51103)),
% 59.96/59.99 inference(scs_inference,[],[92,488,5064,1369,99,5087,182,440,1855,4968,2126,4711,4205,4728,4817,4713,4527,4009,5074,5078,176,5073,5077,180,1234,4736,3856,5068,5070,5107,1275,212,1711,168,98,101,97,102,104,118,120,132,133,134,146,152,15,24,28,31,32,39,139,142,4,5,7,8,9,11,16,17,18,19,20,21,22,23,25,26,29,30,33,34,35,36,37,38,40,41,42,43,44,45,138,12,14,143,164,151,148,6,116,111,13,124,103,10,27,136,2,48,49,70,75,56,129,130,131,145,155,156,140,144,150,158,65,59,61])).
% 59.96/59.99 cnf(5112,plain,
% 59.96/59.99 (E(f27(f23(f25(f23(x51121,f22(x51122,x51123)),x51122),f22(x51124,x51125)),x51124),x51123)),
% 59.96/59.99 inference(rename_variables,[],[3856])).
% 59.96/59.99 cnf(5113,plain,
% 59.96/59.99 (~P6(f23(a1,f22(a1,x51131)),a14)),
% 59.96/59.99 inference(scs_inference,[],[92,488,5064,1369,99,5087,182,440,1855,4968,2126,4711,4205,4728,4817,4713,4527,4009,5074,5078,176,5073,5077,180,1234,4736,3856,5068,5070,5107,5109,1275,212,1711,168,98,101,97,102,104,118,120,132,133,134,146,152,15,24,28,31,32,39,139,142,4,5,7,8,9,11,16,17,18,19,20,21,22,23,25,26,29,30,33,34,35,36,37,38,40,41,42,43,44,45,138,12,14,143,164,151,148,6,116,111,13,124,103,10,27,136,2,48,49,70,75,56,129,130,131,145,155,156,140,144,150,158,65,59,61,63,147])).
% 59.96/59.99 cnf(5117,plain,
% 59.96/59.99 (E(f27(f23(f25(f23(x51171,f22(x51172,x51173)),x51172),f22(x51174,x51175)),x51174),x51173)),
% 59.96/59.99 inference(rename_variables,[],[3856])).
% 59.96/59.99 cnf(5118,plain,
% 59.96/59.99 (~P4(f6(a4,a1),a14)),
% 59.96/59.99 inference(scs_inference,[],[92,488,5064,1369,99,5087,182,440,171,1855,4968,2126,4711,4205,4728,4817,4713,4527,4009,5074,5078,176,5073,5077,180,1234,4736,3856,5068,5070,5107,5109,5112,1275,212,1711,168,98,101,97,102,104,118,120,132,133,134,146,152,15,24,28,31,32,39,139,142,4,5,7,8,9,11,16,17,18,19,20,21,22,23,25,26,29,30,33,34,35,36,37,38,40,41,42,43,44,45,138,12,14,143,164,151,148,6,116,111,13,124,103,10,27,136,2,48,49,70,75,56,129,130,131,145,155,156,140,144,150,158,65,59,61,63,147,72,137])).
% 59.96/59.99 cnf(5122,plain,
% 59.96/59.99 (E(f27(f23(f25(f23(x51221,f22(x51222,x51223)),x51222),f22(x51224,x51225)),x51224),x51223)),
% 59.96/59.99 inference(rename_variables,[],[3856])).
% 59.96/59.99 cnf(5125,plain,
% 59.96/59.99 (~E(f27(f23(f25(f23(x51251,f22(x51252,a1)),x51252),f22(x51253,x51254)),x51253),a14)),
% 59.96/59.99 inference(scs_inference,[],[92,488,5064,1369,99,5087,182,440,171,1855,4968,2126,4711,4205,4728,4817,4713,4527,4009,5074,5078,176,5073,5077,180,1234,4736,3856,5068,5070,5107,5109,5112,5117,5122,1275,212,3886,1711,168,98,101,97,102,104,118,120,132,133,134,146,152,15,24,28,31,32,39,139,142,4,5,7,8,9,11,16,17,18,19,20,21,22,23,25,26,29,30,33,34,35,36,37,38,40,41,42,43,44,45,138,12,14,143,164,151,148,6,116,111,13,124,103,10,27,136,2,48,49,70,75,56,129,130,131,145,155,156,140,144,150,158,65,59,61,63,147,72,137,62,60,3])).
% 59.96/59.99 cnf(5130,plain,
% 59.96/59.99 (P17(f12(f16(f29(a9,a14,a15)),f7(f29(a9,a14,a15))),f7(f29(a9,a14,a15)))),
% 59.96/59.99 inference(scs_inference,[],[92,488,5064,1369,99,5087,182,440,171,1855,4968,2126,4562,4302,4711,4205,4728,4817,4713,4527,4009,5074,5078,176,5073,5077,180,1234,4736,3856,5068,5070,5107,5109,5112,5117,5122,1275,212,3886,1711,168,1095,98,101,97,102,104,118,120,132,133,134,146,152,15,24,28,31,32,39,139,142,4,5,7,8,9,11,16,17,18,19,20,21,22,23,25,26,29,30,33,34,35,36,37,38,40,41,42,43,44,45,138,12,14,143,164,151,148,6,116,111,13,124,103,10,27,136,2,48,49,70,75,56,129,130,131,145,155,156,140,144,150,158,65,59,61,63,147,72,137,62,60,3,126,123])).
% 59.96/59.99 cnf(5179,plain,
% 59.96/59.99 (P6(f23(x51791,f22(f26(f29(x51792,a1,x51793),x51794),x51795)),f29(x51792,a1,a3))),
% 59.96/59.99 inference(scs_inference,[],[5044,4140,138,139])).
% 59.96/59.99 cnf(5183,plain,
% 59.96/59.99 (E(f7(f29(x51831,a14,x51832)),f19(x51831))),
% 59.96/59.99 inference(scs_inference,[],[5062,5044,4140,138,139,120,143])).
% 59.96/59.99 cnf(5257,plain,
% 59.96/59.99 (E(f27(f23(f27(f23(x52571,f22(x52572,x52573)),x52572),f22(x52574,x52575)),x52574),x52571)),
% 59.96/59.99 inference(rename_variables,[],[2186])).
% 59.96/59.99 cnf(5259,plain,
% 59.96/59.99 (~P11(f23(a1,f22(x52591,a1)),x52592,a14)),
% 59.96/59.99 inference(rename_variables,[],[5086])).
% 59.96/59.99 cnf(5265,plain,
% 59.96/59.99 (E(f27(f23(f25(f23(x52651,f22(x52652,x52653)),x52652),f22(x52654,x52655)),x52654),x52653)),
% 59.96/59.99 inference(rename_variables,[],[3856])).
% 59.96/59.99 cnf(5272,plain,
% 59.96/59.99 (E(f27(f23(f25(f23(x52721,f22(x52722,x52723)),x52722),f22(x52724,x52725)),x52724),x52723)),
% 59.96/59.99 inference(rename_variables,[],[3856])).
% 59.96/59.99 cnf(5274,plain,
% 59.96/59.99 (E(f27(f23(f27(f23(f21(f6(x52741,x52742),x52742),f22(x52743,x52744)),x52743),f22(x52745,x52746)),x52745),f21(f6(x52741,x52747),x52747))),
% 59.96/59.99 inference(rename_variables,[],[4080])).
% 59.96/59.99 cnf(5278,plain,
% 59.96/59.99 (E(f26(f29(x52781,a1,x52782),x52783),f29(x52781,a1,a3))),
% 59.96/59.99 inference(rename_variables,[],[5044])).
% 59.96/59.99 cnf(5283,plain,
% 59.96/59.99 (E(f27(f23(f27(f23(x52831,f22(x52832,x52833)),x52832),f22(x52834,x52835)),x52834),x52831)),
% 59.96/59.99 inference(rename_variables,[],[2186])).
% 59.96/59.99 cnf(5298,plain,
% 59.96/59.99 (~P5(f29(a9,a14,a15),f12(f16(f29(a9,a14,a15)),f7(f29(a9,a14,a15))))),
% 59.96/59.99 inference(scs_inference,[],[92,5062,4994,5118,5044,5278,4637,5086,5259,5089,5113,169,5071,5110,4021,4980,5130,4822,5054,4140,5069,5125,5049,5004,4674,4080,5274,171,4619,4728,3856,5265,5272,4159,2186,5257,5283,101,421,138,139,120,143,102,146,132,152,148,134,164,118,151,24,14,23,19,116,31,15,4,17,28,16,7,39,5,133,21,34,43,26,25,104,142,11,33,20,30,37,40,6,103,29,9,22,8,18,36,41,44,32,12,42,35,38,45,10,13,27,2,76,156,155,71,65,145,58,56,75,70,49,63,59,61,127,147,72,137,166])).
% 59.96/59.99 cnf(5326,plain,
% 59.96/59.99 ($false),
% 59.96/59.99 inference(scs_inference,[],[5183,5298,5179,5054,139,146,164]),
% 59.96/59.99 ['proof']).
% 59.96/59.99 % SZS output end Proof
% 59.96/59.99 % Total time :59.280000s
%------------------------------------------------------------------------------