%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : SET799+4 : TPTP v8.2.0. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% Computer : n022.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 14:22:30 EDT 2024
% Result : Theorem 58.62s 58.70s
% Output : CNFRefutation 58.67s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.10/0.12 % Problem : SET799+4 : TPTP v8.2.0. Released v3.2.0.
% 0.10/0.12 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% 0.11/0.31 % Computer : n022.cluster.edu
% 0.11/0.31 % Model : x86_64 x86_64
% 0.11/0.31 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.31 % Memory : 8042.1875MB
% 0.11/0.31 % OS : Linux 3.10.0-693.el7.x86_64
% 0.11/0.31 % CPULimit : 300
% 0.11/0.31 % WCLimit : 300
% 0.11/0.31 % DateTime : Sun Jun 23 17:38:24 EDT 2024
% 0.11/0.32 % CPUTime :
% 0.17/0.56 start to proof:theBenchmark
% 58.62/58.69 %-------------------------------------------
% 58.62/58.69 % File :CSE---1.7
% 58.62/58.69 % Problem :theBenchmark
% 58.62/58.69 % Transform :cnf
% 58.62/58.69 % Format :tptp:raw
% 58.62/58.69 % Command :java -jar mcs_scs.jar %d %s
% 58.62/58.69
% 58.62/58.69 % Result :Theorem 58.050000s
% 58.62/58.69 % Output :CNFRefutation 58.050000s
% 58.62/58.69 %-------------------------------------------
% 58.62/58.69 %------------------------------------------------------------------------------
% 58.62/58.69 % File : SET799+4 : TPTP v8.2.0. Released v3.2.0.
% 58.62/58.69 % Domain : Set Theory (Order relations)
% 58.62/58.69 % Problem : Least upper bounds of set in total order
% 58.62/58.69 % Version : [Pas05] axioms.
% 58.62/58.69 % English : If an order is total, the least upper bound of a set is less
% 58.62/58.69 % than the least upper bound of a subset of it.
% 58.62/58.69
% 58.62/58.69 % Refs : [Pas05] Pastre (2005), Email to G. Sutcliffe
% 58.62/58.69 % Source : [Pas05]
% 58.62/58.69 % Names :
% 58.62/58.69
% 58.62/58.69 % Status : Theorem
% 58.62/58.69 % Rating : 0.11 v8.1.0, 0.06 v7.4.0, 0.10 v7.3.0, 0.07 v7.1.0, 0.09 v7.0.0, 0.07 v6.4.0, 0.08 v6.3.0, 0.12 v6.1.0, 0.13 v6.0.0, 0.22 v5.5.0, 0.15 v5.4.0, 0.21 v5.3.0, 0.22 v5.2.0, 0.10 v5.0.0, 0.12 v4.1.0, 0.13 v4.0.0, 0.17 v3.7.0, 0.15 v3.5.0, 0.16 v3.4.0, 0.21 v3.3.0, 0.07 v3.2.0
% 58.62/58.69 % Syntax : Number of formulae : 22 ( 1 unt; 0 def)
% 58.62/58.69 % Number of atoms : 92 ( 6 equ)
% 58.62/58.69 % Maximal formula atoms : 14 ( 4 avg)
% 58.62/58.69 % Number of connectives : 72 ( 2 ~; 3 |; 28 &)
% 58.62/58.69 % ( 20 <=>; 19 =>; 0 <=; 0 <~>)
% 58.62/58.69 % Maximal formula depth : 12 ( 7 avg)
% 58.62/58.69 % Maximal term depth : 2 ( 1 avg)
% 58.62/58.69 % Number of predicates : 15 ( 14 usr; 0 prp; 2-4 aty)
% 58.62/58.69 % Number of functors : 9 ( 9 usr; 1 con; 0-2 aty)
% 58.62/58.69 % Number of variables : 80 ( 79 !; 1 ?)
% 58.62/58.70 % SPC : FOF_THM_RFO_SEQ
% 58.62/58.70
% 58.62/58.70 % Comments :
% 58.62/58.70 %------------------------------------------------------------------------------
% 58.62/58.70 %----Include set theory definitions
% 58.62/58.70 include('Axioms/SET006+0.ax').
% 58.62/58.70 %----Include order relation axioms
% 58.62/58.70 include('Axioms/SET006+3.ax').
% 58.62/58.70 %------------------------------------------------------------------------------
% 58.62/58.70 fof(thIV11,conjecture,
% 58.62/58.70 ! [R,E] :
% 58.62/58.70 ( order(R,E)
% 58.62/58.70 => ! [X1,X2] :
% 58.62/58.70 ( ( subset(X1,E)
% 58.62/58.70 & subset(X2,E)
% 58.62/58.70 & subset(X1,X2) )
% 58.62/58.70 => ! [M1,M2] :
% 58.62/58.70 ( ( least_upper_bound(M1,X1,R,E)
% 58.62/58.70 & least_upper_bound(M2,X2,R,E) )
% 58.62/58.70 => apply(R,M1,M2) ) ) ) ).
% 58.62/58.70
% 58.62/58.70 %------------------------------------------------------------------------------
% 58.62/58.70 %-------------------------------------------
% 58.62/58.70 % Proof found
% 58.62/58.70 % SZS status Theorem for theBenchmark
% 58.62/58.70 % SZS output start Proof
% 58.67/58.70 %ClaNum:247(EqnAxiom:104)
% 58.67/58.70 %VarNum:1415(SingletonVarNum:350)
% 58.67/58.70 %MaxLitNum:7
% 58.67/58.70 %MaxfuncDepth:1
% 58.67/58.70 %SharedTerms:14
% 58.67/58.70 %goalClause: 105 106 107 108 109 110 112
% 58.67/58.70 %singleGoalClaCount:7
% 58.67/58.70 [105]P1(a1,a2)
% 58.67/58.70 [106]P1(a1,a10)
% 58.67/58.70 [107]P1(a10,a2)
% 58.67/58.70 [108]P2(a3,a2)
% 58.67/58.70 [109]P3(a11,a1,a3,a2)
% 58.67/58.70 [110]P3(a12,a10,a3,a2)
% 58.67/58.70 [112]~P4(a3,a11,a12)
% 58.67/58.70 [111]~P10(x1111,a4)
% 58.67/58.70 [115]~P5(x1152,x1151)+P1(x1151,x1152)
% 58.67/58.70 [116]~P5(x1161,x1162)+P1(x1161,x1162)
% 58.67/58.70 [117]~P14(x1171,x1172)+P2(x1171,x1172)
% 58.67/58.70 [118]~P6(x1181,x1182)+P2(x1181,x1182)
% 58.67/58.70 [119]~P2(x1191,x1192)+P6(x1191,x1192)
% 58.67/58.70 [113]~E(x1131,x1132)+P10(x1131,f13(x1132))
% 58.67/58.70 [114]E(x1141,x1142)+~P10(x1141,f13(x1142))
% 58.67/58.70 [120]~P1(x1201,x1202)+P10(x1201,f14(x1202))
% 58.67/58.70 [123]P1(x1231,x1232)+~P10(x1231,f14(x1232))
% 58.67/58.70 [124]P1(x1241,x1242)+P10(f15(x1241,x1242),x1241)
% 58.67/58.70 [127]P10(f16(x1271,x1272),x1272)+P10(x1271,f31(x1272))
% 58.67/58.70 [133]~P10(x1331,f34(x1332))+P10(x1331,f17(x1331,x1332))
% 58.67/58.70 [134]~P10(x1341,f34(x1342))+P10(f17(x1341,x1342),x1342)
% 58.67/58.70 [141]P1(x1411,x1412)+~P10(f15(x1411,x1412),x1412)
% 58.67/58.70 [142]~P10(x1421,f16(x1421,x1422))+P10(x1421,f31(x1422))
% 58.67/58.70 [147]P10(x1471,x1472)+~P7(x1471,x1473,x1472)
% 58.67/58.70 [148]P10(x1481,x1482)+~P8(x1481,x1483,x1482)
% 58.67/58.70 [149]P10(x1491,x1492)+~P11(x1491,x1493,x1492)
% 58.67/58.70 [150]P10(x1501,x1502)+~P13(x1501,x1503,x1502)
% 58.67/58.70 [121]~E(x1211,x1213)+P10(x1211,f32(x1212,x1213))
% 58.67/58.70 [122]~E(x1221,x1222)+P10(x1221,f32(x1222,x1223))
% 58.67/58.70 [128]~P10(x1281,x1283)+P10(x1281,f33(x1282,x1283))
% 58.67/58.70 [129]~P10(x1291,x1292)+P10(x1291,f33(x1292,x1293))
% 58.67/58.70 [138]P10(x1381,x1382)+~P10(x1381,f26(x1383,x1382))
% 58.67/58.70 [139]P10(x1391,x1392)+~P10(x1391,f26(x1392,x1393))
% 58.67/58.70 [140]P10(x1401,x1402)+~P10(x1401,f5(x1402,x1403))
% 58.67/58.70 [144]~P10(x1441,x1442)+~P10(x1441,f5(x1443,x1442))
% 58.67/58.70 [166]P15(x1661,x1662,x1663)+P10(f27(x1662,x1663,x1661),x1663)
% 58.67/58.70 [167]P12(x1671,x1672,x1673)+P10(f28(x1672,x1673,x1671),x1673)
% 58.67/58.70 [208]P12(x2081,x2082,x2083)+~P4(x2082,x2081,f28(x2082,x2083,x2081))
% 58.67/58.70 [209]P15(x2091,x2092,x2093)+~P4(x2092,f27(x2092,x2093,x2091),x2091)
% 58.67/58.70 [234]P10(x2341,x2342)+~P3(x2341,x2342,x2343,x2344)
% 58.67/58.70 [235]P10(x2351,x2352)+~P9(x2351,x2352,x2353,x2354)
% 58.67/58.70 [236]P15(x2361,x2362,x2363)+~P3(x2361,x2363,x2362,x2364)
% 58.67/58.70 [237]P12(x2371,x2372,x2373)+~P9(x2371,x2373,x2372,x2374)
% 58.67/58.70 [126]~P1(x1262,x1261)+~P1(x1261,x1262)+P5(x1261,x1262)
% 58.67/58.70 [136]~P2(x1361,x1362)+P14(x1361,x1362)+P10(f24(x1361,x1362),x1362)
% 58.67/58.70 [137]~P2(x1371,x1372)+P14(x1371,x1372)+P10(f25(x1371,x1372),x1372)
% 58.67/58.70 [185]~P2(x1851,x1852)+P14(x1851,x1852)+~P4(x1851,f24(x1851,x1852),f25(x1851,x1852))
% 58.67/58.70 [186]~P2(x1861,x1862)+P14(x1861,x1862)+~P4(x1861,f25(x1861,x1862),f24(x1861,x1862))
% 58.67/58.70 [125]~P10(x1251,x1253)+P10(x1251,x1252)+~P1(x1253,x1252)
% 58.67/58.70 [146]~P6(x1461,x1463)+P4(x1461,x1462,x1462)+~P10(x1462,x1463)
% 58.67/58.70 [130]~P10(x1303,x1302)+~P10(x1301,x1303)+P10(x1301,f34(x1302))
% 58.67/58.70 [131]E(x1311,x1312)+E(x1311,x1313)+~P10(x1311,f32(x1313,x1312))
% 58.67/58.70 [132]P10(x1321,x1322)+~P10(x1322,x1323)+~P10(x1321,f31(x1323))
% 58.67/58.70 [135]~P10(x1351,x1353)+P10(x1351,x1352)+P10(x1351,f5(x1353,x1352))
% 58.67/58.70 [143]~P10(x1431,x1433)+~P10(x1431,x1432)+P10(x1431,f26(x1432,x1433))
% 58.67/58.70 [145]P10(x1451,x1452)+P10(x1451,x1453)+~P10(x1451,f33(x1453,x1452))
% 58.67/58.70 [164]~P10(x1641,x1643)+P11(x1641,x1642,x1643)+~E(f6(x1642,x1643,x1641),x1641)
% 58.67/58.70 [165]~P10(x1651,x1653)+P13(x1651,x1652,x1653)+~E(f7(x1652,x1653,x1651),x1651)
% 58.67/58.70 [171]~P10(x1711,x1713)+P7(x1711,x1712,x1713)+P10(f29(x1712,x1713,x1711),x1713)
% 58.67/58.70 [172]~P10(x1721,x1723)+P8(x1721,x1722,x1723)+P10(f30(x1722,x1723,x1721),x1723)
% 58.67/58.70 [173]~P10(x1731,x1733)+P11(x1731,x1732,x1733)+P10(f6(x1732,x1733,x1731),x1733)
% 58.67/58.70 [174]~P10(x1741,x1743)+P13(x1741,x1742,x1743)+P10(f7(x1742,x1743,x1741),x1743)
% 58.67/58.70 [189]~P10(x1891,x1893)+P11(x1891,x1892,x1893)+P4(x1892,x1891,f6(x1892,x1893,x1891))
% 58.67/58.70 [190]~P10(x1901,x1903)+P13(x1901,x1902,x1903)+P4(x1902,f7(x1902,x1903,x1901),x1901)
% 58.67/58.70 [223]~P10(x2231,x2233)+P8(x2231,x2232,x2233)+~P4(x2232,x2231,f30(x2232,x2233,x2231))
% 58.67/58.70 [224]~P10(x2241,x2243)+P7(x2241,x2242,x2243)+~P4(x2242,f29(x2242,x2243,x2241),x2241)
% 58.67/58.70 [160]~P8(x1602,x1601,x1604)+P4(x1601,x1602,x1603)+~P10(x1603,x1604)
% 58.67/58.70 [161]~P7(x1613,x1611,x1614)+P4(x1611,x1612,x1613)+~P10(x1612,x1614)
% 58.67/58.70 [162]~P15(x1623,x1621,x1624)+P4(x1621,x1622,x1623)+~P10(x1622,x1624)
% 58.67/58.70 [163]~P12(x1632,x1631,x1634)+P4(x1631,x1632,x1633)+~P10(x1633,x1634)
% 58.67/58.70 [151]P6(x1511,x1512)+P10(f18(x1512,x1511),x1512)+P10(f19(x1512,x1511),x1512)+P10(f20(x1512,x1511),x1512)
% 58.67/58.70 [152]P6(x1521,x1522)+P10(f18(x1522,x1521),x1522)+P10(f19(x1522,x1521),x1522)+P10(f22(x1522,x1521),x1522)
% 58.67/58.70 [153]P6(x1531,x1532)+P10(f18(x1532,x1531),x1532)+P10(f19(x1532,x1531),x1532)+P10(f23(x1532,x1531),x1532)
% 58.67/58.70 [154]P6(x1541,x1542)+P10(f18(x1542,x1541),x1542)+P10(f21(x1542,x1541),x1542)+P10(f20(x1542,x1541),x1542)
% 58.67/58.70 [155]P6(x1551,x1552)+P10(f18(x1552,x1551),x1552)+P10(f21(x1552,x1551),x1552)+P10(f22(x1552,x1551),x1552)
% 58.67/58.70 [156]P6(x1561,x1562)+P10(f18(x1562,x1561),x1562)+P10(f21(x1562,x1561),x1562)+P10(f23(x1562,x1561),x1562)
% 58.67/58.70 [157]P6(x1571,x1572)+P10(f18(x1572,x1571),x1572)+P10(f20(x1572,x1571),x1572)+~E(f21(x1572,x1571),f19(x1572,x1571))
% 58.67/58.70 [158]P6(x1581,x1582)+P10(f18(x1582,x1581),x1582)+P10(f22(x1582,x1581),x1582)+~E(f21(x1582,x1581),f19(x1582,x1581))
% 58.67/58.70 [159]P6(x1591,x1592)+P10(f18(x1592,x1591),x1592)+P10(f23(x1592,x1591),x1592)+~E(f21(x1592,x1591),f19(x1592,x1591))
% 58.67/58.70 [175]P6(x1751,x1752)+P4(x1751,f19(x1752,x1751),f21(x1752,x1751))+P10(f18(x1752,x1751),x1752)+P10(f20(x1752,x1751),x1752)
% 58.67/58.70 [176]P6(x1761,x1762)+P4(x1761,f21(x1762,x1761),f19(x1762,x1761))+P10(f18(x1762,x1761),x1762)+P10(f20(x1762,x1761),x1762)
% 58.67/58.70 [177]P6(x1771,x1772)+P4(x1771,f19(x1772,x1771),f21(x1772,x1771))+P10(f18(x1772,x1771),x1772)+P10(f22(x1772,x1771),x1772)
% 58.67/58.70 [178]P6(x1781,x1782)+P4(x1781,f21(x1782,x1781),f19(x1782,x1781))+P10(f18(x1782,x1781),x1782)+P10(f22(x1782,x1781),x1782)
% 58.67/58.70 [179]P6(x1791,x1792)+P4(x1791,f19(x1792,x1791),f21(x1792,x1791))+P10(f18(x1792,x1791),x1792)+P10(f23(x1792,x1791),x1792)
% 58.67/58.70 [180]P6(x1801,x1802)+P4(x1801,f21(x1802,x1801),f19(x1802,x1801))+P10(f18(x1802,x1801),x1802)+P10(f23(x1802,x1801),x1802)
% 58.67/58.70 [181]P6(x1811,x1812)+P4(x1811,f20(x1812,x1811),f22(x1812,x1811))+P10(f18(x1812,x1811),x1812)+P10(f19(x1812,x1811),x1812)
% 58.67/58.70 [182]P6(x1821,x1822)+P4(x1821,f22(x1822,x1821),f23(x1822,x1821))+P10(f18(x1822,x1821),x1822)+P10(f19(x1822,x1821),x1822)
% 58.67/58.70 [183]P6(x1831,x1832)+P4(x1831,f20(x1832,x1831),f22(x1832,x1831))+P10(f18(x1832,x1831),x1832)+P10(f21(x1832,x1831),x1832)
% 58.67/58.70 [184]P6(x1841,x1842)+P4(x1841,f22(x1842,x1841),f23(x1842,x1841))+P10(f18(x1842,x1841),x1842)+P10(f21(x1842,x1841),x1842)
% 58.67/58.70 [187]P6(x1871,x1872)+P4(x1871,f20(x1872,x1871),f22(x1872,x1871))+P10(f18(x1872,x1871),x1872)+~E(f21(x1872,x1871),f19(x1872,x1871))
% 58.67/58.70 [188]P6(x1881,x1882)+P4(x1881,f22(x1882,x1881),f23(x1882,x1881))+P10(f18(x1882,x1881),x1882)+~E(f21(x1882,x1881),f19(x1882,x1881))
% 58.67/58.70 [192]P6(x1921,x1922)+~P4(x1921,f18(x1922,x1921),f18(x1922,x1921))+P10(f19(x1922,x1921),x1922)+P10(f20(x1922,x1921),x1922)
% 58.67/58.70 [193]P6(x1931,x1932)+~P4(x1931,f18(x1932,x1931),f18(x1932,x1931))+P10(f19(x1932,x1931),x1932)+P10(f22(x1932,x1931),x1932)
% 58.67/58.70 [194]P6(x1941,x1942)+~P4(x1941,f18(x1942,x1941),f18(x1942,x1941))+P10(f19(x1942,x1941),x1942)+P10(f23(x1942,x1941),x1942)
% 58.67/58.70 [195]P6(x1951,x1952)+~P4(x1951,f18(x1952,x1951),f18(x1952,x1951))+P10(f21(x1952,x1951),x1952)+P10(f20(x1952,x1951),x1952)
% 58.67/58.70 [196]P6(x1961,x1962)+~P4(x1961,f18(x1962,x1961),f18(x1962,x1961))+P10(f21(x1962,x1961),x1962)+P10(f22(x1962,x1961),x1962)
% 58.67/58.70 [197]P6(x1971,x1972)+~P4(x1971,f18(x1972,x1971),f18(x1972,x1971))+P10(f21(x1972,x1971),x1972)+P10(f23(x1972,x1971),x1972)
% 58.67/58.70 [198]P6(x1981,x1982)+~P4(x1981,f20(x1982,x1981),f23(x1982,x1981))+P10(f18(x1982,x1981),x1982)+P10(f19(x1982,x1981),x1982)
% 58.67/58.70 [199]P6(x1991,x1992)+~P4(x1991,f20(x1992,x1991),f23(x1992,x1991))+P10(f18(x1992,x1991),x1992)+P10(f21(x1992,x1991),x1992)
% 58.67/58.70 [200]P6(x2001,x2002)+~P4(x2001,f18(x2002,x2001),f18(x2002,x2001))+P10(f20(x2002,x2001),x2002)+~E(f21(x2002,x2001),f19(x2002,x2001))
% 58.67/58.70 [201]P6(x2011,x2012)+~P4(x2011,f18(x2012,x2011),f18(x2012,x2011))+P10(f22(x2012,x2011),x2012)+~E(f21(x2012,x2011),f19(x2012,x2011))
% 58.67/58.70 [202]P6(x2021,x2022)+~P4(x2021,f18(x2022,x2021),f18(x2022,x2021))+P10(f23(x2022,x2021),x2022)+~E(f21(x2022,x2021),f19(x2022,x2021))
% 58.67/58.70 [203]P6(x2031,x2032)+~P4(x2031,f20(x2032,x2031),f23(x2032,x2031))+P10(f18(x2032,x2031),x2032)+~E(f21(x2032,x2031),f19(x2032,x2031))
% 58.67/58.70 [204]P6(x2041,x2042)+P4(x2041,f19(x2042,x2041),f21(x2042,x2041))+P4(x2041,f20(x2042,x2041),f22(x2042,x2041))+P10(f18(x2042,x2041),x2042)
% 58.67/58.70 [205]P6(x2051,x2052)+P4(x2051,f19(x2052,x2051),f21(x2052,x2051))+P4(x2051,f22(x2052,x2051),f23(x2052,x2051))+P10(f18(x2052,x2051),x2052)
% 58.67/58.70 [206]P6(x2061,x2062)+P4(x2061,f21(x2062,x2061),f19(x2062,x2061))+P4(x2061,f20(x2062,x2061),f22(x2062,x2061))+P10(f18(x2062,x2061),x2062)
% 58.67/58.70 [207]P6(x2071,x2072)+P4(x2071,f21(x2072,x2071),f19(x2072,x2071))+P4(x2071,f22(x2072,x2071),f23(x2072,x2071))+P10(f18(x2072,x2071),x2072)
% 58.67/58.70 [211]P6(x2111,x2112)+P4(x2111,f19(x2112,x2111),f21(x2112,x2111))+~P4(x2111,f18(x2112,x2111),f18(x2112,x2111))+P10(f20(x2112,x2111),x2112)
% 58.67/58.70 [212]P6(x2121,x2122)+P4(x2121,f21(x2122,x2121),f19(x2122,x2121))+~P4(x2121,f18(x2122,x2121),f18(x2122,x2121))+P10(f20(x2122,x2121),x2122)
% 58.67/58.70 [213]P6(x2131,x2132)+P4(x2131,f19(x2132,x2131),f21(x2132,x2131))+~P4(x2131,f18(x2132,x2131),f18(x2132,x2131))+P10(f22(x2132,x2131),x2132)
% 58.67/58.70 [214]P6(x2141,x2142)+P4(x2141,f21(x2142,x2141),f19(x2142,x2141))+~P4(x2141,f18(x2142,x2141),f18(x2142,x2141))+P10(f22(x2142,x2141),x2142)
% 58.67/58.70 [215]P6(x2151,x2152)+P4(x2151,f19(x2152,x2151),f21(x2152,x2151))+~P4(x2151,f18(x2152,x2151),f18(x2152,x2151))+P10(f23(x2152,x2151),x2152)
% 58.67/58.70 [216]P6(x2161,x2162)+P4(x2161,f21(x2162,x2161),f19(x2162,x2161))+~P4(x2161,f18(x2162,x2161),f18(x2162,x2161))+P10(f23(x2162,x2161),x2162)
% 58.67/58.70 [217]P6(x2171,x2172)+P4(x2171,f19(x2172,x2171),f21(x2172,x2171))+~P4(x2171,f20(x2172,x2171),f23(x2172,x2171))+P10(f18(x2172,x2171),x2172)
% 58.67/58.70 [218]P6(x2181,x2182)+P4(x2181,f21(x2182,x2181),f19(x2182,x2181))+~P4(x2181,f20(x2182,x2181),f23(x2182,x2181))+P10(f18(x2182,x2181),x2182)
% 58.67/58.70 [219]P6(x2191,x2192)+P4(x2191,f20(x2192,x2191),f22(x2192,x2191))+~P4(x2191,f18(x2192,x2191),f18(x2192,x2191))+P10(f19(x2192,x2191),x2192)
% 58.67/58.70 [220]P6(x2201,x2202)+P4(x2201,f22(x2202,x2201),f23(x2202,x2201))+~P4(x2201,f18(x2202,x2201),f18(x2202,x2201))+P10(f19(x2202,x2201),x2202)
% 58.67/58.70 [221]P6(x2211,x2212)+P4(x2211,f20(x2212,x2211),f22(x2212,x2211))+~P4(x2211,f18(x2212,x2211),f18(x2212,x2211))+P10(f21(x2212,x2211),x2212)
% 58.67/58.70 [222]P6(x2221,x2222)+P4(x2221,f22(x2222,x2221),f23(x2222,x2221))+~P4(x2221,f18(x2222,x2221),f18(x2222,x2221))+P10(f21(x2222,x2221),x2222)
% 58.67/58.70 [225]P6(x2251,x2252)+P4(x2251,f20(x2252,x2251),f22(x2252,x2251))+~P4(x2251,f18(x2252,x2251),f18(x2252,x2251))+~E(f21(x2252,x2251),f19(x2252,x2251))
% 58.67/58.70 [226]P6(x2261,x2262)+P4(x2261,f22(x2262,x2261),f23(x2262,x2261))+~P4(x2261,f18(x2262,x2261),f18(x2262,x2261))+~E(f21(x2262,x2261),f19(x2262,x2261))
% 58.67/58.70 [227]P6(x2271,x2272)+~P4(x2271,f18(x2272,x2271),f18(x2272,x2271))+~P4(x2271,f20(x2272,x2271),f23(x2272,x2271))+P10(f19(x2272,x2271),x2272)
% 58.67/58.70 [228]P6(x2281,x2282)+~P4(x2281,f18(x2282,x2281),f18(x2282,x2281))+~P4(x2281,f20(x2282,x2281),f23(x2282,x2281))+P10(f21(x2282,x2281),x2282)
% 58.67/58.70 [229]P6(x2291,x2292)+~P4(x2291,f18(x2292,x2291),f18(x2292,x2291))+~P4(x2291,f20(x2292,x2291),f23(x2292,x2291))+~E(f21(x2292,x2291),f19(x2292,x2291))
% 58.67/58.70 [230]P6(x2301,x2302)+P4(x2301,f19(x2302,x2301),f21(x2302,x2301))+P4(x2301,f20(x2302,x2301),f22(x2302,x2301))+~P4(x2301,f18(x2302,x2301),f18(x2302,x2301))
% 58.67/58.70 [231]P6(x2311,x2312)+P4(x2311,f19(x2312,x2311),f21(x2312,x2311))+P4(x2311,f22(x2312,x2311),f23(x2312,x2311))+~P4(x2311,f18(x2312,x2311),f18(x2312,x2311))
% 58.67/58.70 [232]P6(x2321,x2322)+P4(x2321,f21(x2322,x2321),f19(x2322,x2321))+P4(x2321,f20(x2322,x2321),f22(x2322,x2321))+~P4(x2321,f18(x2322,x2321),f18(x2322,x2321))
% 58.67/58.70 [233]P6(x2331,x2332)+P4(x2331,f21(x2332,x2331),f19(x2332,x2331))+P4(x2331,f22(x2332,x2331),f23(x2332,x2331))+~P4(x2331,f18(x2332,x2331),f18(x2332,x2331))
% 58.67/58.70 [238]P6(x2381,x2382)+P4(x2381,f19(x2382,x2381),f21(x2382,x2381))+~P4(x2381,f18(x2382,x2381),f18(x2382,x2381))+~P4(x2381,f20(x2382,x2381),f23(x2382,x2381))
% 58.67/58.70 [239]P6(x2391,x2392)+P4(x2391,f21(x2392,x2391),f19(x2392,x2391))+~P4(x2391,f18(x2392,x2391),f18(x2392,x2391))+~P4(x2391,f20(x2392,x2391),f23(x2392,x2391))
% 58.67/58.70 [169]~P11(x1692,x1694,x1693)+E(x1691,x1692)+~P4(x1694,x1692,x1691)+~P10(x1691,x1693)
% 58.67/58.70 [170]~P13(x1702,x1704,x1703)+E(x1701,x1702)+~P4(x1704,x1701,x1702)+~P10(x1701,x1703)
% 58.67/58.70 [242]~P10(x2421,x2422)+~P15(x2421,x2423,x2422)+P3(x2421,x2422,x2423,x2424)+P10(f8(x2421,x2422,x2423,x2424),x2424)
% 58.67/58.70 [243]~P10(x2431,x2432)+~P12(x2431,x2433,x2432)+P9(x2431,x2432,x2433,x2434)+P10(f9(x2431,x2432,x2433,x2434),x2434)
% 58.67/58.70 [244]~P10(x2441,x2442)+~P15(x2441,x2443,x2442)+P3(x2441,x2442,x2443,x2444)+P15(f8(x2441,x2442,x2443,x2444),x2443,x2442)
% 58.67/58.70 [245]~P10(x2451,x2452)+~P12(x2451,x2453,x2452)+P9(x2451,x2452,x2453,x2454)+P12(f9(x2451,x2452,x2453,x2454),x2453,x2452)
% 58.67/58.70 [246]~P10(x2461,x2462)+~P15(x2461,x2463,x2462)+P3(x2461,x2462,x2463,x2464)+~P4(x2463,x2461,f8(x2461,x2462,x2463,x2464))
% 58.67/58.70 [247]~P10(x2471,x2472)+~P12(x2471,x2473,x2472)+P9(x2471,x2472,x2473,x2474)+~P4(x2473,f9(x2471,x2472,x2473,x2474),x2471)
% 58.67/58.70 [240]~P3(x2402,x2405,x2401,x2404)+P4(x2401,x2402,x2403)+~P15(x2403,x2401,x2405)+~P10(x2403,x2404)
% 58.67/58.70 [241]~P9(x2413,x2415,x2411,x2414)+P4(x2411,x2412,x2413)+~P12(x2412,x2411,x2415)+~P10(x2412,x2414)
% 58.67/58.70 [168]P4(x1681,x1683,x1682)+~P10(x1683,x1684)+~P14(x1681,x1684)+P4(x1681,x1682,x1683)+~P10(x1682,x1684)
% 58.67/58.70 [191]~P10(x1911,x1913)+~P4(x1914,x1912,x1911)+~P4(x1914,x1911,x1912)+E(x1911,x1912)+~P10(x1912,x1913)+~P6(x1914,x1913)
% 58.67/58.70 [210]~P10(x2102,x2104)+~P6(x2101,x2104)+~P4(x2101,x2105,x2103)+~P4(x2101,x2102,x2105)+P4(x2101,x2102,x2103)+~P10(x2103,x2104)+~P10(x2105,x2104)
% 58.67/58.70 %EqnAxiom
% 58.67/58.70 [1]E(x11,x11)
% 58.67/58.70 [2]E(x22,x21)+~E(x21,x22)
% 58.67/58.70 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 58.67/58.70 [4]~E(x41,x42)+E(f13(x41),f13(x42))
% 58.67/58.70 [5]~E(x51,x52)+E(f9(x51,x53,x54,x55),f9(x52,x53,x54,x55))
% 58.67/58.70 [6]~E(x61,x62)+E(f9(x63,x61,x64,x65),f9(x63,x62,x64,x65))
% 58.67/58.70 [7]~E(x71,x72)+E(f9(x73,x74,x71,x75),f9(x73,x74,x72,x75))
% 58.67/58.70 [8]~E(x81,x82)+E(f9(x83,x84,x85,x81),f9(x83,x84,x85,x82))
% 58.67/58.70 [9]~E(x91,x92)+E(f14(x91),f14(x92))
% 58.67/58.70 [10]~E(x101,x102)+E(f32(x101,x103),f32(x102,x103))
% 58.67/58.70 [11]~E(x111,x112)+E(f32(x113,x111),f32(x113,x112))
% 58.67/58.70 [12]~E(x121,x122)+E(f8(x121,x123,x124,x125),f8(x122,x123,x124,x125))
% 58.67/58.70 [13]~E(x131,x132)+E(f8(x133,x131,x134,x135),f8(x133,x132,x134,x135))
% 58.67/58.70 [14]~E(x141,x142)+E(f8(x143,x144,x141,x145),f8(x143,x144,x142,x145))
% 58.67/58.70 [15]~E(x151,x152)+E(f8(x153,x154,x155,x151),f8(x153,x154,x155,x152))
% 58.67/58.70 [16]~E(x161,x162)+E(f23(x161,x163),f23(x162,x163))
% 58.67/58.70 [17]~E(x171,x172)+E(f23(x173,x171),f23(x173,x172))
% 58.67/58.70 [18]~E(x181,x182)+E(f15(x181,x183),f15(x182,x183))
% 58.67/58.70 [19]~E(x191,x192)+E(f15(x193,x191),f15(x193,x192))
% 58.67/58.70 [20]~E(x201,x202)+E(f31(x201),f31(x202))
% 58.67/58.70 [21]~E(x211,x212)+E(f16(x211,x213),f16(x212,x213))
% 58.67/58.70 [22]~E(x221,x222)+E(f16(x223,x221),f16(x223,x222))
% 58.67/58.70 [23]~E(x231,x232)+E(f33(x231,x233),f33(x232,x233))
% 58.67/58.70 [24]~E(x241,x242)+E(f33(x243,x241),f33(x243,x242))
% 58.67/58.70 [25]~E(x251,x252)+E(f19(x251,x253),f19(x252,x253))
% 58.67/58.70 [26]~E(x261,x262)+E(f19(x263,x261),f19(x263,x262))
% 58.67/58.70 [27]~E(x271,x272)+E(f34(x271),f34(x272))
% 58.67/58.70 [28]~E(x281,x282)+E(f20(x281,x283),f20(x282,x283))
% 58.67/58.70 [29]~E(x291,x292)+E(f20(x293,x291),f20(x293,x292))
% 58.67/58.70 [30]~E(x301,x302)+E(f22(x301,x303),f22(x302,x303))
% 58.67/58.70 [31]~E(x311,x312)+E(f22(x313,x311),f22(x313,x312))
% 58.67/58.70 [32]~E(x321,x322)+E(f17(x321,x323),f17(x322,x323))
% 58.67/58.70 [33]~E(x331,x332)+E(f17(x333,x331),f17(x333,x332))
% 58.67/58.70 [34]~E(x341,x342)+E(f21(x341,x343),f21(x342,x343))
% 58.67/58.70 [35]~E(x351,x352)+E(f21(x353,x351),f21(x353,x352))
% 58.67/58.70 [36]~E(x361,x362)+E(f18(x361,x363),f18(x362,x363))
% 58.67/58.70 [37]~E(x371,x372)+E(f18(x373,x371),f18(x373,x372))
% 58.67/58.70 [38]~E(x381,x382)+E(f7(x381,x383,x384),f7(x382,x383,x384))
% 58.67/58.70 [39]~E(x391,x392)+E(f7(x393,x391,x394),f7(x393,x392,x394))
% 58.67/58.70 [40]~E(x401,x402)+E(f7(x403,x404,x401),f7(x403,x404,x402))
% 58.67/58.70 [41]~E(x411,x412)+E(f5(x411,x413),f5(x412,x413))
% 58.67/58.70 [42]~E(x421,x422)+E(f5(x423,x421),f5(x423,x422))
% 58.67/58.70 [43]~E(x431,x432)+E(f24(x431,x433),f24(x432,x433))
% 58.67/58.70 [44]~E(x441,x442)+E(f24(x443,x441),f24(x443,x442))
% 58.67/58.71 [45]~E(x451,x452)+E(f25(x451,x453),f25(x452,x453))
% 58.67/58.71 [46]~E(x461,x462)+E(f25(x463,x461),f25(x463,x462))
% 58.67/58.71 [47]~E(x471,x472)+E(f26(x471,x473),f26(x472,x473))
% 58.67/58.71 [48]~E(x481,x482)+E(f26(x483,x481),f26(x483,x482))
% 58.67/58.71 [49]~E(x491,x492)+E(f6(x491,x493,x494),f6(x492,x493,x494))
% 58.67/58.71 [50]~E(x501,x502)+E(f6(x503,x501,x504),f6(x503,x502,x504))
% 58.67/58.71 [51]~E(x511,x512)+E(f6(x513,x514,x511),f6(x513,x514,x512))
% 58.67/58.71 [52]~E(x521,x522)+E(f27(x521,x523,x524),f27(x522,x523,x524))
% 58.67/58.71 [53]~E(x531,x532)+E(f27(x533,x531,x534),f27(x533,x532,x534))
% 58.67/58.71 [54]~E(x541,x542)+E(f27(x543,x544,x541),f27(x543,x544,x542))
% 58.67/58.71 [55]~E(x551,x552)+E(f28(x551,x553,x554),f28(x552,x553,x554))
% 58.67/58.71 [56]~E(x561,x562)+E(f28(x563,x561,x564),f28(x563,x562,x564))
% 58.67/58.71 [57]~E(x571,x572)+E(f28(x573,x574,x571),f28(x573,x574,x572))
% 58.67/58.71 [58]~E(x581,x582)+E(f30(x581,x583,x584),f30(x582,x583,x584))
% 58.67/58.71 [59]~E(x591,x592)+E(f30(x593,x591,x594),f30(x593,x592,x594))
% 58.67/58.71 [60]~E(x601,x602)+E(f30(x603,x604,x601),f30(x603,x604,x602))
% 58.67/58.71 [61]~E(x611,x612)+E(f29(x611,x613,x614),f29(x612,x613,x614))
% 58.67/58.71 [62]~E(x621,x622)+E(f29(x623,x621,x624),f29(x623,x622,x624))
% 58.67/58.71 [63]~E(x631,x632)+E(f29(x633,x634,x631),f29(x633,x634,x632))
% 58.67/58.71 [64]P1(x642,x643)+~E(x641,x642)+~P1(x641,x643)
% 58.67/58.71 [65]P1(x653,x652)+~E(x651,x652)+~P1(x653,x651)
% 58.67/58.71 [66]P4(x662,x663,x664)+~E(x661,x662)+~P4(x661,x663,x664)
% 58.67/58.71 [67]P4(x673,x672,x674)+~E(x671,x672)+~P4(x673,x671,x674)
% 58.67/58.71 [68]P4(x683,x684,x682)+~E(x681,x682)+~P4(x683,x684,x681)
% 58.67/58.71 [69]P12(x692,x693,x694)+~E(x691,x692)+~P12(x691,x693,x694)
% 58.67/58.71 [70]P12(x703,x702,x704)+~E(x701,x702)+~P12(x703,x701,x704)
% 58.67/58.71 [71]P12(x713,x714,x712)+~E(x711,x712)+~P12(x713,x714,x711)
% 58.67/58.71 [72]P2(x722,x723)+~E(x721,x722)+~P2(x721,x723)
% 58.67/58.71 [73]P2(x733,x732)+~E(x731,x732)+~P2(x733,x731)
% 58.67/58.71 [74]P3(x742,x743,x744,x745)+~E(x741,x742)+~P3(x741,x743,x744,x745)
% 58.67/58.71 [75]P3(x753,x752,x754,x755)+~E(x751,x752)+~P3(x753,x751,x754,x755)
% 58.67/58.71 [76]P3(x763,x764,x762,x765)+~E(x761,x762)+~P3(x763,x764,x761,x765)
% 58.67/58.71 [77]P3(x773,x774,x775,x772)+~E(x771,x772)+~P3(x773,x774,x775,x771)
% 58.67/58.71 [78]P10(x782,x783)+~E(x781,x782)+~P10(x781,x783)
% 58.67/58.71 [79]P10(x793,x792)+~E(x791,x792)+~P10(x793,x791)
% 58.67/58.71 [80]P15(x802,x803,x804)+~E(x801,x802)+~P15(x801,x803,x804)
% 58.67/58.71 [81]P15(x813,x812,x814)+~E(x811,x812)+~P15(x813,x811,x814)
% 58.67/58.71 [82]P15(x823,x824,x822)+~E(x821,x822)+~P15(x823,x824,x821)
% 58.67/58.71 [83]P9(x832,x833,x834,x835)+~E(x831,x832)+~P9(x831,x833,x834,x835)
% 58.67/58.71 [84]P9(x843,x842,x844,x845)+~E(x841,x842)+~P9(x843,x841,x844,x845)
% 58.67/58.71 [85]P9(x853,x854,x852,x855)+~E(x851,x852)+~P9(x853,x854,x851,x855)
% 58.67/58.71 [86]P9(x863,x864,x865,x862)+~E(x861,x862)+~P9(x863,x864,x865,x861)
% 58.67/58.71 [87]P6(x872,x873)+~E(x871,x872)+~P6(x871,x873)
% 58.67/58.71 [88]P6(x883,x882)+~E(x881,x882)+~P6(x883,x881)
% 58.67/58.71 [89]P7(x892,x893,x894)+~E(x891,x892)+~P7(x891,x893,x894)
% 58.67/58.71 [90]P7(x903,x902,x904)+~E(x901,x902)+~P7(x903,x901,x904)
% 58.67/58.71 [91]P7(x913,x914,x912)+~E(x911,x912)+~P7(x913,x914,x911)
% 58.67/58.71 [92]P13(x922,x923,x924)+~E(x921,x922)+~P13(x921,x923,x924)
% 58.67/58.71 [93]P13(x933,x932,x934)+~E(x931,x932)+~P13(x933,x931,x934)
% 58.67/58.71 [94]P13(x943,x944,x942)+~E(x941,x942)+~P13(x943,x944,x941)
% 58.67/58.71 [95]P5(x952,x953)+~E(x951,x952)+~P5(x951,x953)
% 58.67/58.71 [96]P5(x963,x962)+~E(x961,x962)+~P5(x963,x961)
% 58.67/58.71 [97]P14(x972,x973)+~E(x971,x972)+~P14(x971,x973)
% 58.67/58.71 [98]P14(x983,x982)+~E(x981,x982)+~P14(x983,x981)
% 58.67/58.71 [99]P8(x992,x993,x994)+~E(x991,x992)+~P8(x991,x993,x994)
% 58.67/58.71 [100]P8(x1003,x1002,x1004)+~E(x1001,x1002)+~P8(x1003,x1001,x1004)
% 58.67/58.71 [101]P8(x1013,x1014,x1012)+~E(x1011,x1012)+~P8(x1013,x1014,x1011)
% 58.67/58.71 [102]P11(x1022,x1023,x1024)+~E(x1021,x1022)+~P11(x1021,x1023,x1024)
% 58.67/58.71 [103]P11(x1033,x1032,x1034)+~E(x1031,x1032)+~P11(x1033,x1031,x1034)
% 58.67/58.71 [104]P11(x1043,x1044,x1042)+~E(x1041,x1042)+~P11(x1043,x1044,x1041)
% 58.67/58.71
% 58.67/58.71 %-------------------------------------------
% 58.67/58.72 cnf(248,plain,
% 58.67/58.72 (P10(x2481,f13(x2481))),
% 58.67/58.72 inference(equality_inference,[],[113])).
% 58.67/58.72 cnf(249,plain,
% 58.67/58.72 (P10(x2491,f32(x2492,x2491))),
% 58.67/58.72 inference(equality_inference,[],[121])).
% 58.67/58.72 cnf(250,plain,
% 58.67/58.72 (P10(x2501,f32(x2501,x2502))),
% 58.67/58.72 inference(equality_inference,[],[122])).
% 58.67/58.72 cnf(251,plain,
% 58.67/58.72 (~P3(x2511,a4,x2512,x2513)),
% 58.67/58.72 inference(scs_inference,[],[111,234])).
% 58.67/58.72 cnf(253,plain,
% 58.67/58.72 (P1(a4,x2531)),
% 58.67/58.72 inference(scs_inference,[],[111,234,124])).
% 58.67/58.72 cnf(254,plain,
% 58.67/58.72 (~P10(x2541,a4)),
% 58.67/58.72 inference(rename_variables,[],[111])).
% 58.67/58.72 cnf(256,plain,
% 58.67/58.72 (~P10(x2561,f34(a4))),
% 58.67/58.72 inference(scs_inference,[],[111,254,234,124,134])).
% 58.67/58.72 cnf(257,plain,
% 58.67/58.72 (~P10(x2571,a4)),
% 58.67/58.72 inference(rename_variables,[],[111])).
% 58.67/58.72 cnf(259,plain,
% 58.67/58.72 (~P7(x2591,x2592,a4)),
% 58.67/58.72 inference(scs_inference,[],[111,254,257,234,124,134,147])).
% 58.67/58.72 cnf(261,plain,
% 58.67/58.72 (~P8(x2611,x2612,a4)),
% 58.67/58.72 inference(scs_inference,[],[111,254,257,234,124,134,147,148])).
% 58.67/58.72 cnf(263,plain,
% 58.67/58.72 (~P11(x2631,x2632,a4)),
% 58.67/58.72 inference(scs_inference,[],[111,254,257,234,124,134,147,148,149])).
% 58.67/58.72 cnf(265,plain,
% 58.67/58.72 (~P13(x2651,x2652,a4)),
% 58.67/58.72 inference(scs_inference,[],[111,254,257,234,124,134,147,148,149,150])).
% 58.67/58.72 cnf(267,plain,
% 58.67/58.72 (P15(x2671,x2672,a4)),
% 58.67/58.72 inference(scs_inference,[],[111,254,257,234,124,134,147,148,149,150,166])).
% 58.67/58.72 cnf(268,plain,
% 58.67/58.72 (~P10(x2681,a4)),
% 58.67/58.72 inference(rename_variables,[],[111])).
% 58.67/58.72 cnf(270,plain,
% 58.67/58.72 (P12(x2701,x2702,a4)),
% 58.67/58.72 inference(scs_inference,[],[111,254,257,268,234,124,134,147,148,149,150,166,167])).
% 58.67/58.72 cnf(271,plain,
% 58.67/58.72 (~P10(x2711,a4)),
% 58.67/58.72 inference(rename_variables,[],[111])).
% 58.67/58.72 cnf(278,plain,
% 58.67/58.72 (P10(x2781,f13(x2781))),
% 58.67/58.72 inference(rename_variables,[],[248])).
% 58.67/58.72 cnf(280,plain,
% 58.67/58.72 (~P7(a12,a3,f13(a11))),
% 58.67/58.72 inference(scs_inference,[],[112,248,278,111,254,257,268,271,234,124,134,147,148,149,150,166,167,235,126,160,161])).
% 58.67/58.72 cnf(281,plain,
% 58.67/58.72 (P10(x2811,f13(x2811))),
% 58.67/58.72 inference(rename_variables,[],[248])).
% 58.67/58.72 cnf(283,plain,
% 58.67/58.72 (~P15(a12,a3,f13(a11))),
% 58.67/58.72 inference(scs_inference,[],[112,248,278,281,111,254,257,268,271,234,124,134,147,148,149,150,166,167,235,126,160,161,162])).
% 58.67/58.72 cnf(284,plain,
% 58.67/58.72 (P10(x2841,f13(x2841))),
% 58.67/58.72 inference(rename_variables,[],[248])).
% 58.67/58.72 cnf(286,plain,
% 58.67/58.72 (~P12(a11,a3,f13(a12))),
% 58.67/58.72 inference(scs_inference,[],[112,248,278,281,284,111,254,257,268,271,234,124,134,147,148,149,150,166,167,235,126,160,161,162,163])).
% 58.67/58.72 cnf(287,plain,
% 58.67/58.72 (P10(x2871,f13(x2871))),
% 58.67/58.72 inference(rename_variables,[],[248])).
% 58.67/58.72 cnf(297,plain,
% 58.67/58.72 (~P10(x2971,a1)+P10(x2971,a2)),
% 58.67/58.72 inference(scs_inference,[],[105,112,248,278,281,284,287,111,254,257,268,271,234,124,134,147,148,149,150,166,167,235,126,160,161,162,163,71,79,82,236,237,125])).
% 58.67/58.72 cnf(303,plain,
% 58.67/58.72 (P14(x3031,f34(a4))+~P2(x3031,f34(a4))),
% 58.67/58.72 inference(scs_inference,[],[105,110,112,248,278,281,284,287,111,254,257,268,271,234,124,134,147,148,149,150,166,167,235,126,160,161,162,163,71,79,82,236,237,125,75,136,137])).
% 58.67/58.72 cnf(311,plain,
% 58.67/58.72 (~P3(x3111,f34(a4),x3112,x3113)),
% 58.67/58.73 inference(scs_inference,[],[256,234])).
% 58.67/58.73 cnf(313,plain,
% 58.67/58.73 (~P11(x3131,x3132,f34(a4))),
% 58.67/58.73 inference(scs_inference,[],[256,234,149])).
% 58.67/58.73 cnf(317,plain,
% 58.67/58.73 (P12(x3171,x3172,f34(a4))),
% 58.67/58.73 inference(scs_inference,[],[256,234,149,235,167])).
% 58.67/58.73 cnf(318,plain,
% 58.67/58.73 (~P10(x3181,f34(a4))),
% 58.67/58.73 inference(rename_variables,[],[256])).
% 58.67/58.73 cnf(320,plain,
% 58.67/58.73 (P15(x3201,x3202,f34(a4))),
% 58.67/58.73 inference(scs_inference,[],[256,318,234,149,235,167,166])).
% 58.67/58.73 cnf(321,plain,
% 58.67/58.73 (~P10(x3211,f34(a4))),
% 58.67/58.73 inference(rename_variables,[],[256])).
% 58.67/58.73 cnf(323,plain,
% 58.67/58.73 (~P10(x3231,f34(f34(a4)))),
% 58.67/58.73 inference(scs_inference,[],[256,318,321,234,149,235,167,166,134])).
% 58.67/58.73 cnf(324,plain,
% 58.67/58.73 (~P10(x3241,f34(a4))),
% 58.67/58.73 inference(rename_variables,[],[256])).
% 58.67/58.73 cnf(326,plain,
% 58.67/58.73 (~P7(x3261,x3262,f34(a4))),
% 58.67/58.73 inference(scs_inference,[],[256,318,321,324,234,149,235,167,166,134,147])).
% 58.67/58.73 cnf(328,plain,
% 58.67/58.73 (~P13(x3281,x3282,f34(a4))),
% 58.67/58.73 inference(scs_inference,[],[256,318,321,324,234,149,235,167,166,134,147,150])).
% 58.67/58.73 cnf(330,plain,
% 58.67/58.73 (~P8(x3301,x3302,f34(a4))),
% 58.67/58.73 inference(scs_inference,[],[256,318,321,324,234,149,235,167,166,134,147,150,148])).
% 58.67/58.73 cnf(332,plain,
% 58.67/58.73 (P1(f34(a4),x3321)),
% 58.67/58.73 inference(scs_inference,[],[256,318,321,324,234,149,235,167,166,134,147,150,148,124])).
% 58.67/58.73 cnf(333,plain,
% 58.67/58.73 (~P10(x3331,f34(a4))),
% 58.67/58.73 inference(rename_variables,[],[256])).
% 58.67/58.73 cnf(336,plain,
% 58.67/58.73 (P10(x3361,f32(x3362,x3361))),
% 58.67/58.73 inference(rename_variables,[],[249])).
% 58.67/58.73 cnf(339,plain,
% 58.67/58.73 (P10(x3391,f32(x3392,x3391))),
% 58.67/58.73 inference(rename_variables,[],[249])).
% 58.67/58.73 cnf(341,plain,
% 58.67/58.73 (~P15(a12,a3,f32(x3411,a11))),
% 58.67/58.73 inference(scs_inference,[],[112,249,336,339,256,318,321,324,234,149,235,167,166,134,147,150,148,124,160,161,162])).
% 58.67/58.73 cnf(342,plain,
% 58.67/58.73 (P10(x3421,f32(x3422,x3421))),
% 58.67/58.73 inference(rename_variables,[],[249])).
% 58.67/58.73 cnf(346,plain,
% 58.67/58.73 (P10(x3461,f32(x3462,x3461))),
% 58.67/58.73 inference(rename_variables,[],[249])).
% 58.67/58.73 cnf(347,plain,
% 58.67/58.73 (~P12(a11,a3,f32(x3471,a12))),
% 58.67/58.73 inference(scs_inference,[],[112,286,249,336,339,342,346,256,318,321,324,333,234,149,235,167,166,134,147,150,148,124,160,161,162,71,79,163])).
% 58.67/58.73 cnf(350,plain,
% 58.67/58.73 (P5(f34(a4),a4)),
% 58.67/58.73 inference(scs_inference,[],[112,286,253,249,336,339,342,346,256,318,321,324,333,234,149,235,167,166,134,147,150,148,124,160,161,162,71,79,163,126])).
% 58.67/58.73 cnf(358,plain,
% 58.67/58.73 (~P3(a12,f32(x3581,a11),a3,x3582)),
% 58.67/58.73 inference(scs_inference,[],[109,112,251,283,286,253,249,336,339,342,346,256,318,321,324,333,234,149,235,167,166,134,147,150,148,124,160,161,162,71,79,163,126,75,82,237,236])).
% 58.67/58.73 cnf(379,plain,
% 58.67/58.73 (P10(x3791,f32(x3791,x3792))),
% 58.67/58.73 inference(rename_variables,[],[250])).
% 58.67/58.73 cnf(382,plain,
% 58.67/58.73 (P10(x3821,f32(x3821,x3822))),
% 58.67/58.73 inference(rename_variables,[],[250])).
% 58.67/58.73 cnf(385,plain,
% 58.67/58.73 (P10(x3851,f32(x3851,x3852))),
% 58.67/58.73 inference(rename_variables,[],[250])).
% 58.67/58.73 cnf(388,plain,
% 58.67/58.73 (P10(x3881,f32(x3881,x3882))),
% 58.67/58.73 inference(rename_variables,[],[250])).
% 58.67/58.73 cnf(404,plain,
% 58.67/58.73 (~P3(a12,f32(a11,x4041),a3,x4042)),
% 58.67/58.73 inference(scs_inference,[],[110,112,311,341,347,332,111,267,270,250,379,382,385,388,323,234,235,149,150,148,147,161,162,160,163,71,126,79,75,82,237,236])).
% 58.67/58.73 cnf(466,plain,
% 58.67/58.73 (~P10(x4661,a1)+P10(x4661,a10)),
% 58.67/58.73 inference(scs_inference,[],[106,110,358,249,75,74,78,76,125])).
% 58.67/58.73 cnf(475,plain,
% 58.67/58.73 (~E(a1,f34(a4))),
% 58.67/58.73 inference(scs_inference,[],[109,311,75])).
% 58.67/58.73 cnf(491,plain,
% 58.67/58.73 (~P10(x4911,a10)+P10(x4911,a2)),
% 58.67/58.73 inference(scs_inference,[],[107,110,404,75,125])).
% 58.67/58.73 cnf(536,plain,
% 58.67/58.73 (~E(a10,a4)),
% 58.67/58.73 inference(scs_inference,[],[110,251,75])).
% 58.67/58.73 cnf(551,plain,
% 58.67/58.73 (~P10(x5511,f34(a4))),
% 58.67/58.73 inference(rename_variables,[],[256])).
% 58.67/58.73 cnf(552,plain,
% 58.67/58.73 (~P10(x5521,f34(a4))),
% 58.67/58.73 inference(rename_variables,[],[256])).
% 58.67/58.73 cnf(554,plain,
% 58.67/58.73 (P6(x5541,f34(a4))+P10(f21(f34(a4),x5541),f34(a4))+P10(f20(f34(a4),x5541),f34(a4))),
% 58.67/58.73 inference(scs_inference,[],[256,551,552,154])).
% 58.67/58.73 cnf(556,plain,
% 58.67/58.73 (~P10(x5561,f34(a4))),
% 58.67/58.73 inference(rename_variables,[],[256])).
% 58.67/58.73 cnf(557,plain,
% 58.67/58.73 (~P10(x5571,f34(a4))),
% 58.67/58.73 inference(rename_variables,[],[256])).
% 58.67/58.73 cnf(560,plain,
% 58.67/58.73 (~P10(x5601,f34(a4))),
% 58.67/58.73 inference(rename_variables,[],[256])).
% 58.67/58.73 cnf(562,plain,
% 58.67/58.73 (~P10(x5621,f34(a4))),
% 58.67/58.73 inference(rename_variables,[],[256])).
% 58.67/58.73 cnf(568,plain,
% 58.67/58.73 (~P10(x5681,f34(a4))),
% 58.67/58.73 inference(rename_variables,[],[256])).
% 58.67/58.73 cnf(573,plain,
% 58.67/58.73 (P6(x5731,f34(a4))),
% 58.67/58.73 inference(scs_inference,[],[256,556,557,560,562,568,323,317,320,326,313,328,330,554,171,174,172,162,130,173,163,78,79])).
% 58.67/58.73 cnf(594,plain,
% 58.67/58.73 (~P10(a4,f13(a10))),
% 58.67/58.73 inference(scs_inference,[],[536,2,114])).
% 58.67/58.73 cnf(595,plain,
% 58.67/58.73 (~E(a4,a10)),
% 58.67/58.73 inference(scs_inference,[],[594,113])).
% 58.67/58.73 cnf(715,plain,
% 58.67/58.73 (~P10(x7151,a4)),
% 58.67/58.73 inference(rename_variables,[],[111])).
% 58.67/58.73 cnf(716,plain,
% 58.67/58.73 (~P10(x7161,a4)),
% 58.67/58.73 inference(rename_variables,[],[111])).
% 58.67/58.73 cnf(718,plain,
% 58.67/58.73 (P6(x7181,a4)+P10(f19(a4,x7181),a4)+P10(f22(a4,x7181),a4)),
% 58.67/58.73 inference(scs_inference,[],[111,715,716,152])).
% 58.67/58.73 cnf(720,plain,
% 58.67/58.73 (~P10(x7201,a4)),
% 58.67/58.73 inference(rename_variables,[],[111])).
% 58.67/58.73 cnf(721,plain,
% 58.67/58.73 (~P10(x7211,a4)),
% 58.67/58.73 inference(rename_variables,[],[111])).
% 58.67/58.73 cnf(726,plain,
% 58.67/58.73 (~P10(x7261,a4)),
% 58.67/58.73 inference(rename_variables,[],[111])).
% 58.67/58.73 cnf(728,plain,
% 58.67/58.73 (~P10(x7281,a4)),
% 58.67/58.73 inference(rename_variables,[],[111])).
% 58.67/58.73 cnf(730,plain,
% 58.67/58.73 (~P10(x7301,a4)),
% 58.67/58.73 inference(rename_variables,[],[111])).
% 58.67/58.73 cnf(737,plain,
% 58.67/58.73 (P6(x7371,a4)),
% 58.67/58.73 inference(scs_inference,[],[111,720,721,726,728,730,256,270,267,259,261,263,265,718,174,130,171,173,172,162,163,78,79])).
% 58.67/58.73 cnf(777,plain,
% 58.67/58.73 (P10(f34(a4),f14(a4))),
% 58.67/58.73 inference(scs_inference,[],[350,116,120])).
% 58.67/58.73 cnf(778,plain,
% 58.67/58.73 (~E(f14(a4),f34(a4))),
% 58.67/58.73 inference(scs_inference,[],[777,256,79])).
% 58.67/58.73 cnf(792,plain,
% 58.67/58.73 (~E(f14(a4),a4)),
% 58.67/58.73 inference(scs_inference,[],[777,111,79])).
% 58.67/58.73 cnf(2024,plain,
% 58.67/58.73 (P10(x20241,f33(x20242,f31(a4)))),
% 58.67/58.73 inference(scs_inference,[],[111,128,127])).
% 58.67/58.73 cnf(2025,plain,
% 58.67/58.73 (P10(x20251,f31(a4))),
% 58.67/58.73 inference(scs_inference,[],[2024,111,145])).
% 58.67/58.73 cnf(2026,plain,
% 58.67/58.73 (P10(x20261,f33(x20262,f31(a4)))),
% 58.67/58.73 inference(rename_variables,[],[2024])).
% 58.67/58.73 cnf(2029,plain,
% 58.67/58.73 (P10(x20291,f33(x20292,f31(a4)))),
% 58.67/58.73 inference(rename_variables,[],[2024])).
% 58.67/58.73 cnf(2032,plain,
% 58.67/58.73 (P10(x20321,f33(x20322,f31(a4)))),
% 58.67/58.73 inference(rename_variables,[],[2024])).
% 58.67/58.73 cnf(2034,plain,
% 58.67/58.73 (P10(x20341,f33(x20342,f31(a4)))),
% 58.67/58.73 inference(rename_variables,[],[2024])).
% 58.67/58.73 cnf(2037,plain,
% 58.67/58.73 (P10(x20371,f33(x20372,f31(a4)))),
% 58.67/58.73 inference(rename_variables,[],[2024])).
% 58.67/58.73 cnf(2046,plain,
% 58.67/58.73 (~P3(a12,f33(x20461,f31(a4)),a3,x20462)),
% 58.67/58.73 inference(scs_inference,[],[112,2024,2026,2029,2032,2034,2037,111,145,163,79,161,160,162,141,237,236])).
% 58.67/58.73 cnf(2061,plain,
% 58.67/58.73 (~P12(a11,a3,f31(a4))),
% 58.67/58.73 inference(scs_inference,[],[110,112,2046,2025,75,163])).
% 58.67/58.73 cnf(2062,plain,
% 58.67/58.73 (P10(x20621,f31(a4))),
% 58.67/58.73 inference(rename_variables,[],[2025])).
% 58.67/58.73 cnf(2067,plain,
% 58.67/58.73 (P10(x20671,f31(a4))),
% 58.67/58.73 inference(rename_variables,[],[2025])).
% 58.67/58.73 cnf(2069,plain,
% 58.67/58.73 (~P15(a12,a3,f31(a4))),
% 58.67/58.73 inference(scs_inference,[],[110,112,2046,2024,256,2025,2062,2067,75,163,79,161,162])).
% 58.67/58.73 cnf(2399,plain,
% 58.67/58.73 (P14(x23991,f34(a4))),
% 58.67/58.73 inference(scs_inference,[],[573,303,118])).
% 58.67/58.73 cnf(3905,plain,
% 58.67/58.73 (~E(f31(a4),a4)),
% 58.67/58.73 inference(scs_inference,[],[111,2025,79])).
% 58.67/58.73 cnf(12266,plain,
% 58.67/58.73 (P15(a12,a3,a10)),
% 58.67/58.73 inference(scs_inference,[],[105,778,792,737,2399,110,111,118,2,120,138,139,140,114,117,236])).
% 58.67/58.73 cnf(12270,plain,
% 58.67/58.73 (P10(a12,a10)),
% 58.67/58.73 inference(scs_inference,[],[105,778,792,737,2399,108,110,111,118,2,120,138,139,140,114,117,236,119,234])).
% 58.67/58.73 cnf(12273,plain,
% 58.67/58.73 (~P10(x122731,a4)),
% 58.67/58.73 inference(rename_variables,[],[111])).
% 58.67/58.73 cnf(12279,plain,
% 58.67/58.73 (~P10(a11,a10)),
% 58.67/58.73 inference(scs_inference,[],[105,595,778,792,737,2399,108,110,112,111,118,2,120,138,139,140,114,117,236,119,234,135,143,131,162])).
% 58.67/58.73 cnf(12286,plain,
% 58.67/58.73 (P10(x122861,f31(a4))),
% 58.67/58.73 inference(rename_variables,[],[2025])).
% 58.67/58.73 cnf(12295,plain,
% 58.67/58.73 (P10(a12,a2)),
% 58.67/58.73 inference(scs_inference,[],[105,595,778,792,2061,2069,737,320,2399,2025,12286,270,108,594,248,110,112,111,12273,118,2,120,138,139,140,114,117,236,119,234,135,143,131,162,82,71,125,78,79,242,491])).
% 58.67/58.73 cnf(12306,plain,
% 58.67/58.73 (P4(a3,a12,a12)),
% 58.67/58.73 inference(scs_inference,[],[105,595,280,778,792,2061,2069,737,320,2399,2025,12286,270,108,594,248,110,112,111,12273,118,2,120,138,139,140,114,117,236,119,234,135,143,131,162,82,71,125,78,79,242,491,128,129,144,89,145,240])).
% 58.67/58.73 cnf(12353,plain,
% 58.67/58.73 ($false),
% 58.67/58.73 inference(scs_inference,[],[12306,12266,12270,12279,12295,3905,475,253,249,109,112,111,139,144,120,129,138,140,128,236,2,114,234,143,135,145,131,160,67,125,240,123,297,466]),
% 58.67/58.73 ['proof']).
% 58.67/58.74 % SZS output end Proof
% 58.67/58.74 % Total time :58.050000s
%------------------------------------------------------------------------------