%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : SET798+4 : TPTP v8.2.0. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% Computer : n018.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.67s 58.82s
% Output : CNFRefutation 58.77s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.09/0.14 % Problem : SET798+4 : TPTP v8.2.0. Released v3.2.0.
% 0.09/0.14 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% 0.14/0.36 % Computer : n018.cluster.edu
% 0.14/0.36 % Model : x86_64 x86_64
% 0.14/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.36 % Memory : 8042.1875MB
% 0.14/0.36 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.36 % CPULimit : 300
% 0.14/0.36 % WCLimit : 300
% 0.14/0.36 % DateTime : Sun Jun 23 16:44:24 EDT 2024
% 0.14/0.36 % CPUTime :
% 0.57/0.59 start to proof:theBenchmark
% 58.67/58.81 %-------------------------------------------
% 58.67/58.81 % File :CSE---1.7
% 58.67/58.81 % Problem :theBenchmark
% 58.67/58.81 % Transform :cnf
% 58.67/58.81 % Format :tptp:raw
% 58.67/58.81 % Command :java -jar mcs_scs.jar %d %s
% 58.67/58.81
% 58.67/58.81 % Result :Theorem 58.020000s
% 58.67/58.81 % Output :CNFRefutation 58.020000s
% 58.67/58.81 %-------------------------------------------
% 58.67/58.82 %------------------------------------------------------------------------------
% 58.67/58.82 % File : SET798+4 : TPTP v8.2.0. Released v3.2.0.
% 58.67/58.82 % Domain : Set Theory (Order relations)
% 58.67/58.82 % Problem : If X subset Y, then a lower bound of Y is a lower bound of X
% 58.67/58.82 % Version : [Pas05] axioms.
% 58.67/58.82 % English :
% 58.67/58.82
% 58.67/58.82 % Refs : [Pas05] Pastre (2005), Email to G. Sutcliffe
% 58.67/58.82 % Source : [Pas05]
% 58.67/58.82 % Names :
% 58.67/58.82
% 58.67/58.82 % Status : Theorem
% 58.67/58.82 % Rating : 0.17 v8.1.0, 0.14 v7.5.0, 0.16 v7.4.0, 0.13 v7.3.0, 0.10 v7.2.0, 0.07 v7.1.0, 0.13 v7.0.0, 0.20 v6.4.0, 0.23 v6.3.0, 0.21 v6.2.0, 0.12 v6.1.0, 0.23 v6.0.0, 0.26 v5.5.0, 0.30 v5.4.0, 0.29 v5.3.0, 0.33 v5.2.0, 0.25 v5.1.0, 0.29 v4.1.0, 0.26 v4.0.0, 0.29 v3.7.0, 0.30 v3.5.0, 0.32 v3.4.0, 0.42 v3.3.0, 0.29 v3.2.0
% 58.67/58.82 % Syntax : Number of formulae : 22 ( 1 unt; 0 def)
% 58.67/58.82 % Number of atoms : 91 ( 6 equ)
% 58.67/58.82 % Maximal formula atoms : 14 ( 4 avg)
% 58.67/58.82 % Number of connectives : 71 ( 2 ~; 3 |; 27 &)
% 58.67/58.82 % ( 20 <=>; 19 =>; 0 <=; 0 <~>)
% 58.67/58.82 % Maximal formula depth : 12 ( 7 avg)
% 58.67/58.82 % Maximal term depth : 2 ( 1 avg)
% 58.67/58.82 % Number of predicates : 15 ( 14 usr; 0 prp; 2-4 aty)
% 58.67/58.82 % Number of functors : 9 ( 9 usr; 1 con; 0-2 aty)
% 58.67/58.82 % Number of variables : 79 ( 78 !; 1 ?)
% 58.67/58.82 % SPC : FOF_THM_RFO_SEQ
% 58.67/58.82
% 58.67/58.82 % Comments :
% 58.67/58.82 %------------------------------------------------------------------------------
% 58.67/58.82 %----Include set theory definitions
% 58.67/58.82 include('Axioms/SET006+0.ax').
% 58.67/58.82 %----Include order relation axioms
% 58.67/58.82 include('Axioms/SET006+3.ax').
% 58.67/58.82 %------------------------------------------------------------------------------
% 58.67/58.82 fof(thIV10,conjecture,
% 58.67/58.82 ! [R,E] :
% 58.67/58.82 ( order(R,E)
% 58.67/58.82 => ! [X,Y] :
% 58.67/58.82 ( ( subset(X,E)
% 58.67/58.82 & subset(Y,E)
% 58.67/58.82 & subset(X,Y) )
% 58.67/58.82 => ! [M] :
% 58.67/58.82 ( lower_bound(M,R,Y)
% 58.67/58.82 => lower_bound(M,R,X) ) ) ) ).
% 58.67/58.82
% 58.67/58.82 %------------------------------------------------------------------------------
% 58.67/58.82 %-------------------------------------------
% 58.67/58.82 % Proof found
% 58.67/58.82 % SZS status Theorem for theBenchmark
% 58.67/58.82 % SZS output start Proof
% 58.67/58.83 %ClaNum:246(EqnAxiom:104)
% 58.67/58.83 %VarNum:1415(SingletonVarNum:350)
% 58.67/58.83 %MaxLitNum:7
% 58.67/58.83 %MaxfuncDepth:1
% 58.67/58.83 %SharedTerms:12
% 58.67/58.83 %goalClause: 105 106 107 108 109 111
% 58.67/58.83 %singleGoalClaCount:6
% 58.67/58.83 [105]P1(a1,a2)
% 58.67/58.83 [106]P1(a1,a10)
% 58.67/58.83 [107]P1(a10,a2)
% 58.67/58.83 [108]P2(a3,a2)
% 58.67/58.83 [109]P3(a11,a3,a10)
% 58.67/58.83 [111]~P3(a11,a3,a1)
% 58.67/58.83 [110]~P11(x1101,a4)
% 58.67/58.83 [114]~P4(x1142,x1141)+P1(x1141,x1142)
% 58.67/58.83 [115]~P4(x1151,x1152)+P1(x1151,x1152)
% 58.67/58.83 [116]~P14(x1161,x1162)+P2(x1161,x1162)
% 58.67/58.83 [117]~P5(x1171,x1172)+P2(x1171,x1172)
% 58.67/58.83 [118]~P2(x1181,x1182)+P5(x1181,x1182)
% 58.67/58.83 [112]~E(x1121,x1122)+P11(x1121,f12(x1122))
% 58.67/58.83 [113]E(x1131,x1132)+~P11(x1131,f12(x1132))
% 58.67/58.83 [119]~P1(x1191,x1192)+P11(x1191,f13(x1192))
% 58.67/58.83 [122]P1(x1221,x1222)+~P11(x1221,f13(x1222))
% 58.67/58.83 [123]P1(x1231,x1232)+P11(f14(x1231,x1232),x1231)
% 58.67/58.83 [126]P11(f16(x1261,x1262),x1262)+P11(x1261,f30(x1262))
% 58.67/58.83 [132]~P11(x1321,f33(x1322))+P11(x1321,f17(x1321,x1322))
% 58.67/58.83 [133]~P11(x1331,f33(x1332))+P11(f17(x1331,x1332),x1332)
% 58.67/58.83 [140]P1(x1401,x1402)+~P11(f14(x1401,x1402),x1402)
% 58.67/58.83 [141]~P11(x1411,f16(x1411,x1412))+P11(x1411,f30(x1412))
% 58.67/58.83 [146]P11(x1461,x1462)+~P7(x1461,x1463,x1462)
% 58.67/58.83 [147]P11(x1471,x1472)+~P8(x1471,x1473,x1472)
% 58.67/58.83 [148]P11(x1481,x1482)+~P12(x1481,x1483,x1482)
% 58.67/58.83 [149]P11(x1491,x1492)+~P13(x1491,x1493,x1492)
% 58.67/58.83 [120]~E(x1201,x1203)+P11(x1201,f31(x1202,x1203))
% 58.67/58.83 [121]~E(x1211,x1212)+P11(x1211,f31(x1212,x1213))
% 58.67/58.83 [127]~P11(x1271,x1273)+P11(x1271,f32(x1272,x1273))
% 58.67/58.83 [128]~P11(x1281,x1282)+P11(x1281,f32(x1282,x1283))
% 58.67/58.83 [137]P11(x1371,x1372)+~P11(x1371,f25(x1373,x1372))
% 58.67/58.83 [138]P11(x1381,x1382)+~P11(x1381,f25(x1382,x1383))
% 58.67/58.83 [139]P11(x1391,x1392)+~P11(x1391,f5(x1392,x1393))
% 58.67/58.83 [143]~P11(x1431,x1432)+~P11(x1431,f5(x1433,x1432))
% 58.67/58.83 [165]P15(x1651,x1652,x1653)+P11(f26(x1652,x1653,x1651),x1653)
% 58.67/58.83 [166]P3(x1661,x1662,x1663)+P11(f27(x1662,x1663,x1661),x1663)
% 58.67/58.83 [207]P3(x2071,x2072,x2073)+~P6(x2072,x2071,f27(x2072,x2073,x2071))
% 58.67/58.83 [208]P15(x2081,x2082,x2083)+~P6(x2082,f26(x2082,x2083,x2081),x2081)
% 58.67/58.83 [233]P11(x2331,x2332)+~P10(x2331,x2332,x2333,x2334)
% 58.67/58.83 [234]P11(x2341,x2342)+~P9(x2341,x2342,x2343,x2344)
% 58.67/58.83 [235]P15(x2351,x2352,x2353)+~P10(x2351,x2353,x2352,x2354)
% 58.67/58.83 [236]P3(x2361,x2362,x2363)+~P9(x2361,x2363,x2362,x2364)
% 58.67/58.83 [125]~P1(x1252,x1251)+~P1(x1251,x1252)+P4(x1251,x1252)
% 58.67/58.83 [135]~P2(x1351,x1352)+P14(x1351,x1352)+P11(f23(x1351,x1352),x1352)
% 58.67/58.83 [136]~P2(x1361,x1362)+P14(x1361,x1362)+P11(f24(x1361,x1362),x1362)
% 58.67/58.83 [184]~P2(x1841,x1842)+P14(x1841,x1842)+~P6(x1841,f23(x1841,x1842),f24(x1841,x1842))
% 58.67/58.83 [185]~P2(x1851,x1852)+P14(x1851,x1852)+~P6(x1851,f24(x1851,x1852),f23(x1851,x1852))
% 58.67/58.83 [124]~P11(x1241,x1243)+P11(x1241,x1242)+~P1(x1243,x1242)
% 58.67/58.83 [145]~P5(x1451,x1453)+P6(x1451,x1452,x1452)+~P11(x1452,x1453)
% 58.67/58.83 [129]~P11(x1293,x1292)+~P11(x1291,x1293)+P11(x1291,f33(x1292))
% 58.67/58.83 [130]E(x1301,x1302)+E(x1301,x1303)+~P11(x1301,f31(x1303,x1302))
% 58.67/58.83 [131]P11(x1311,x1312)+~P11(x1312,x1313)+~P11(x1311,f30(x1313))
% 58.67/58.83 [134]~P11(x1341,x1343)+P11(x1341,x1342)+P11(x1341,f5(x1343,x1342))
% 58.67/58.83 [142]~P11(x1421,x1423)+~P11(x1421,x1422)+P11(x1421,f25(x1422,x1423))
% 58.67/58.83 [144]P11(x1441,x1442)+P11(x1441,x1443)+~P11(x1441,f32(x1443,x1442))
% 58.67/58.83 [163]~P11(x1631,x1633)+P12(x1631,x1632,x1633)+~E(f6(x1632,x1633,x1631),x1631)
% 58.67/58.83 [164]~P11(x1641,x1643)+P13(x1641,x1642,x1643)+~E(f7(x1642,x1643,x1641),x1641)
% 58.67/58.83 [170]~P11(x1701,x1703)+P7(x1701,x1702,x1703)+P11(f28(x1702,x1703,x1701),x1703)
% 58.67/58.83 [171]~P11(x1711,x1713)+P8(x1711,x1712,x1713)+P11(f29(x1712,x1713,x1711),x1713)
% 58.67/58.83 [172]~P11(x1721,x1723)+P12(x1721,x1722,x1723)+P11(f6(x1722,x1723,x1721),x1723)
% 58.67/58.83 [173]~P11(x1731,x1733)+P13(x1731,x1732,x1733)+P11(f7(x1732,x1733,x1731),x1733)
% 58.67/58.83 [188]~P11(x1881,x1883)+P12(x1881,x1882,x1883)+P6(x1882,x1881,f6(x1882,x1883,x1881))
% 58.67/58.83 [189]~P11(x1891,x1893)+P13(x1891,x1892,x1893)+P6(x1892,f7(x1892,x1893,x1891),x1891)
% 58.67/58.83 [222]~P11(x2221,x2223)+P8(x2221,x2222,x2223)+~P6(x2222,x2221,f29(x2222,x2223,x2221))
% 58.67/58.83 [223]~P11(x2231,x2233)+P7(x2231,x2232,x2233)+~P6(x2232,f28(x2232,x2233,x2231),x2231)
% 58.67/58.83 [159]~P8(x1592,x1591,x1594)+P6(x1591,x1592,x1593)+~P11(x1593,x1594)
% 58.67/58.83 [160]~P7(x1603,x1601,x1604)+P6(x1601,x1602,x1603)+~P11(x1602,x1604)
% 58.67/58.83 [161]~P15(x1613,x1611,x1614)+P6(x1611,x1612,x1613)+~P11(x1612,x1614)
% 58.67/58.83 [162]~P3(x1622,x1621,x1624)+P6(x1621,x1622,x1623)+~P11(x1623,x1624)
% 58.67/58.83 [150]P5(x1501,x1502)+P11(f15(x1502,x1501),x1502)+P11(f18(x1502,x1501),x1502)+P11(f19(x1502,x1501),x1502)
% 58.67/58.83 [151]P5(x1511,x1512)+P11(f15(x1512,x1511),x1512)+P11(f18(x1512,x1511),x1512)+P11(f21(x1512,x1511),x1512)
% 58.67/58.83 [152]P5(x1521,x1522)+P11(f15(x1522,x1521),x1522)+P11(f18(x1522,x1521),x1522)+P11(f22(x1522,x1521),x1522)
% 58.67/58.83 [153]P5(x1531,x1532)+P11(f15(x1532,x1531),x1532)+P11(f20(x1532,x1531),x1532)+P11(f19(x1532,x1531),x1532)
% 58.67/58.83 [154]P5(x1541,x1542)+P11(f15(x1542,x1541),x1542)+P11(f20(x1542,x1541),x1542)+P11(f21(x1542,x1541),x1542)
% 58.67/58.83 [155]P5(x1551,x1552)+P11(f15(x1552,x1551),x1552)+P11(f20(x1552,x1551),x1552)+P11(f22(x1552,x1551),x1552)
% 58.67/58.83 [156]P5(x1561,x1562)+P11(f15(x1562,x1561),x1562)+P11(f19(x1562,x1561),x1562)+~E(f20(x1562,x1561),f18(x1562,x1561))
% 58.67/58.83 [157]P5(x1571,x1572)+P11(f15(x1572,x1571),x1572)+P11(f21(x1572,x1571),x1572)+~E(f20(x1572,x1571),f18(x1572,x1571))
% 58.67/58.83 [158]P5(x1581,x1582)+P11(f15(x1582,x1581),x1582)+P11(f22(x1582,x1581),x1582)+~E(f20(x1582,x1581),f18(x1582,x1581))
% 58.67/58.83 [174]P5(x1741,x1742)+P6(x1741,f18(x1742,x1741),f20(x1742,x1741))+P11(f15(x1742,x1741),x1742)+P11(f19(x1742,x1741),x1742)
% 58.67/58.83 [175]P5(x1751,x1752)+P6(x1751,f20(x1752,x1751),f18(x1752,x1751))+P11(f15(x1752,x1751),x1752)+P11(f19(x1752,x1751),x1752)
% 58.67/58.83 [176]P5(x1761,x1762)+P6(x1761,f18(x1762,x1761),f20(x1762,x1761))+P11(f15(x1762,x1761),x1762)+P11(f21(x1762,x1761),x1762)
% 58.67/58.83 [177]P5(x1771,x1772)+P6(x1771,f20(x1772,x1771),f18(x1772,x1771))+P11(f15(x1772,x1771),x1772)+P11(f21(x1772,x1771),x1772)
% 58.67/58.83 [178]P5(x1781,x1782)+P6(x1781,f18(x1782,x1781),f20(x1782,x1781))+P11(f15(x1782,x1781),x1782)+P11(f22(x1782,x1781),x1782)
% 58.67/58.83 [179]P5(x1791,x1792)+P6(x1791,f20(x1792,x1791),f18(x1792,x1791))+P11(f15(x1792,x1791),x1792)+P11(f22(x1792,x1791),x1792)
% 58.67/58.83 [180]P5(x1801,x1802)+P6(x1801,f19(x1802,x1801),f21(x1802,x1801))+P11(f15(x1802,x1801),x1802)+P11(f18(x1802,x1801),x1802)
% 58.67/58.83 [181]P5(x1811,x1812)+P6(x1811,f21(x1812,x1811),f22(x1812,x1811))+P11(f15(x1812,x1811),x1812)+P11(f18(x1812,x1811),x1812)
% 58.67/58.83 [182]P5(x1821,x1822)+P6(x1821,f19(x1822,x1821),f21(x1822,x1821))+P11(f15(x1822,x1821),x1822)+P11(f20(x1822,x1821),x1822)
% 58.67/58.83 [183]P5(x1831,x1832)+P6(x1831,f21(x1832,x1831),f22(x1832,x1831))+P11(f15(x1832,x1831),x1832)+P11(f20(x1832,x1831),x1832)
% 58.67/58.83 [186]P5(x1861,x1862)+P6(x1861,f19(x1862,x1861),f21(x1862,x1861))+P11(f15(x1862,x1861),x1862)+~E(f20(x1862,x1861),f18(x1862,x1861))
% 58.67/58.83 [187]P5(x1871,x1872)+P6(x1871,f21(x1872,x1871),f22(x1872,x1871))+P11(f15(x1872,x1871),x1872)+~E(f20(x1872,x1871),f18(x1872,x1871))
% 58.67/58.83 [191]P5(x1911,x1912)+~P6(x1911,f15(x1912,x1911),f15(x1912,x1911))+P11(f18(x1912,x1911),x1912)+P11(f19(x1912,x1911),x1912)
% 58.67/58.83 [192]P5(x1921,x1922)+~P6(x1921,f15(x1922,x1921),f15(x1922,x1921))+P11(f18(x1922,x1921),x1922)+P11(f21(x1922,x1921),x1922)
% 58.67/58.83 [193]P5(x1931,x1932)+~P6(x1931,f15(x1932,x1931),f15(x1932,x1931))+P11(f18(x1932,x1931),x1932)+P11(f22(x1932,x1931),x1932)
% 58.67/58.83 [194]P5(x1941,x1942)+~P6(x1941,f15(x1942,x1941),f15(x1942,x1941))+P11(f20(x1942,x1941),x1942)+P11(f19(x1942,x1941),x1942)
% 58.67/58.83 [195]P5(x1951,x1952)+~P6(x1951,f15(x1952,x1951),f15(x1952,x1951))+P11(f20(x1952,x1951),x1952)+P11(f21(x1952,x1951),x1952)
% 58.67/58.83 [196]P5(x1961,x1962)+~P6(x1961,f15(x1962,x1961),f15(x1962,x1961))+P11(f20(x1962,x1961),x1962)+P11(f22(x1962,x1961),x1962)
% 58.67/58.83 [197]P5(x1971,x1972)+~P6(x1971,f19(x1972,x1971),f22(x1972,x1971))+P11(f15(x1972,x1971),x1972)+P11(f18(x1972,x1971),x1972)
% 58.67/58.83 [198]P5(x1981,x1982)+~P6(x1981,f19(x1982,x1981),f22(x1982,x1981))+P11(f15(x1982,x1981),x1982)+P11(f20(x1982,x1981),x1982)
% 58.67/58.83 [199]P5(x1991,x1992)+~P6(x1991,f15(x1992,x1991),f15(x1992,x1991))+P11(f19(x1992,x1991),x1992)+~E(f20(x1992,x1991),f18(x1992,x1991))
% 58.67/58.83 [200]P5(x2001,x2002)+~P6(x2001,f15(x2002,x2001),f15(x2002,x2001))+P11(f21(x2002,x2001),x2002)+~E(f20(x2002,x2001),f18(x2002,x2001))
% 58.67/58.83 [201]P5(x2011,x2012)+~P6(x2011,f15(x2012,x2011),f15(x2012,x2011))+P11(f22(x2012,x2011),x2012)+~E(f20(x2012,x2011),f18(x2012,x2011))
% 58.67/58.83 [202]P5(x2021,x2022)+~P6(x2021,f19(x2022,x2021),f22(x2022,x2021))+P11(f15(x2022,x2021),x2022)+~E(f20(x2022,x2021),f18(x2022,x2021))
% 58.67/58.83 [203]P5(x2031,x2032)+P6(x2031,f18(x2032,x2031),f20(x2032,x2031))+P6(x2031,f19(x2032,x2031),f21(x2032,x2031))+P11(f15(x2032,x2031),x2032)
% 58.67/58.84 [204]P5(x2041,x2042)+P6(x2041,f18(x2042,x2041),f20(x2042,x2041))+P6(x2041,f21(x2042,x2041),f22(x2042,x2041))+P11(f15(x2042,x2041),x2042)
% 58.67/58.84 [205]P5(x2051,x2052)+P6(x2051,f20(x2052,x2051),f18(x2052,x2051))+P6(x2051,f19(x2052,x2051),f21(x2052,x2051))+P11(f15(x2052,x2051),x2052)
% 58.67/58.84 [206]P5(x2061,x2062)+P6(x2061,f20(x2062,x2061),f18(x2062,x2061))+P6(x2061,f21(x2062,x2061),f22(x2062,x2061))+P11(f15(x2062,x2061),x2062)
% 58.67/58.84 [210]P5(x2101,x2102)+P6(x2101,f18(x2102,x2101),f20(x2102,x2101))+~P6(x2101,f15(x2102,x2101),f15(x2102,x2101))+P11(f19(x2102,x2101),x2102)
% 58.67/58.84 [211]P5(x2111,x2112)+P6(x2111,f20(x2112,x2111),f18(x2112,x2111))+~P6(x2111,f15(x2112,x2111),f15(x2112,x2111))+P11(f19(x2112,x2111),x2112)
% 58.67/58.84 [212]P5(x2121,x2122)+P6(x2121,f18(x2122,x2121),f20(x2122,x2121))+~P6(x2121,f15(x2122,x2121),f15(x2122,x2121))+P11(f21(x2122,x2121),x2122)
% 58.67/58.84 [213]P5(x2131,x2132)+P6(x2131,f20(x2132,x2131),f18(x2132,x2131))+~P6(x2131,f15(x2132,x2131),f15(x2132,x2131))+P11(f21(x2132,x2131),x2132)
% 58.67/58.84 [214]P5(x2141,x2142)+P6(x2141,f18(x2142,x2141),f20(x2142,x2141))+~P6(x2141,f15(x2142,x2141),f15(x2142,x2141))+P11(f22(x2142,x2141),x2142)
% 58.67/58.84 [215]P5(x2151,x2152)+P6(x2151,f20(x2152,x2151),f18(x2152,x2151))+~P6(x2151,f15(x2152,x2151),f15(x2152,x2151))+P11(f22(x2152,x2151),x2152)
% 58.67/58.84 [216]P5(x2161,x2162)+P6(x2161,f18(x2162,x2161),f20(x2162,x2161))+~P6(x2161,f19(x2162,x2161),f22(x2162,x2161))+P11(f15(x2162,x2161),x2162)
% 58.67/58.84 [217]P5(x2171,x2172)+P6(x2171,f20(x2172,x2171),f18(x2172,x2171))+~P6(x2171,f19(x2172,x2171),f22(x2172,x2171))+P11(f15(x2172,x2171),x2172)
% 58.67/58.84 [218]P5(x2181,x2182)+P6(x2181,f19(x2182,x2181),f21(x2182,x2181))+~P6(x2181,f15(x2182,x2181),f15(x2182,x2181))+P11(f18(x2182,x2181),x2182)
% 58.67/58.84 [219]P5(x2191,x2192)+P6(x2191,f21(x2192,x2191),f22(x2192,x2191))+~P6(x2191,f15(x2192,x2191),f15(x2192,x2191))+P11(f18(x2192,x2191),x2192)
% 58.67/58.84 [220]P5(x2201,x2202)+P6(x2201,f19(x2202,x2201),f21(x2202,x2201))+~P6(x2201,f15(x2202,x2201),f15(x2202,x2201))+P11(f20(x2202,x2201),x2202)
% 58.67/58.84 [221]P5(x2211,x2212)+P6(x2211,f21(x2212,x2211),f22(x2212,x2211))+~P6(x2211,f15(x2212,x2211),f15(x2212,x2211))+P11(f20(x2212,x2211),x2212)
% 58.67/58.84 [224]P5(x2241,x2242)+P6(x2241,f19(x2242,x2241),f21(x2242,x2241))+~P6(x2241,f15(x2242,x2241),f15(x2242,x2241))+~E(f20(x2242,x2241),f18(x2242,x2241))
% 58.67/58.84 [225]P5(x2251,x2252)+P6(x2251,f21(x2252,x2251),f22(x2252,x2251))+~P6(x2251,f15(x2252,x2251),f15(x2252,x2251))+~E(f20(x2252,x2251),f18(x2252,x2251))
% 58.67/58.84 [226]P5(x2261,x2262)+~P6(x2261,f15(x2262,x2261),f15(x2262,x2261))+~P6(x2261,f19(x2262,x2261),f22(x2262,x2261))+P11(f18(x2262,x2261),x2262)
% 58.67/58.84 [227]P5(x2271,x2272)+~P6(x2271,f15(x2272,x2271),f15(x2272,x2271))+~P6(x2271,f19(x2272,x2271),f22(x2272,x2271))+P11(f20(x2272,x2271),x2272)
% 58.67/58.84 [228]P5(x2281,x2282)+~P6(x2281,f15(x2282,x2281),f15(x2282,x2281))+~P6(x2281,f19(x2282,x2281),f22(x2282,x2281))+~E(f20(x2282,x2281),f18(x2282,x2281))
% 58.67/58.84 [229]P5(x2291,x2292)+P6(x2291,f18(x2292,x2291),f20(x2292,x2291))+P6(x2291,f19(x2292,x2291),f21(x2292,x2291))+~P6(x2291,f15(x2292,x2291),f15(x2292,x2291))
% 58.67/58.84 [230]P5(x2301,x2302)+P6(x2301,f18(x2302,x2301),f20(x2302,x2301))+P6(x2301,f21(x2302,x2301),f22(x2302,x2301))+~P6(x2301,f15(x2302,x2301),f15(x2302,x2301))
% 58.67/58.84 [231]P5(x2311,x2312)+P6(x2311,f20(x2312,x2311),f18(x2312,x2311))+P6(x2311,f19(x2312,x2311),f21(x2312,x2311))+~P6(x2311,f15(x2312,x2311),f15(x2312,x2311))
% 58.67/58.84 [232]P5(x2321,x2322)+P6(x2321,f20(x2322,x2321),f18(x2322,x2321))+P6(x2321,f21(x2322,x2321),f22(x2322,x2321))+~P6(x2321,f15(x2322,x2321),f15(x2322,x2321))
% 58.67/58.84 [237]P5(x2371,x2372)+P6(x2371,f18(x2372,x2371),f20(x2372,x2371))+~P6(x2371,f15(x2372,x2371),f15(x2372,x2371))+~P6(x2371,f19(x2372,x2371),f22(x2372,x2371))
% 58.67/58.84 [238]P5(x2381,x2382)+P6(x2381,f20(x2382,x2381),f18(x2382,x2381))+~P6(x2381,f15(x2382,x2381),f15(x2382,x2381))+~P6(x2381,f19(x2382,x2381),f22(x2382,x2381))
% 58.67/58.84 [168]~P12(x1682,x1684,x1683)+E(x1681,x1682)+~P6(x1684,x1682,x1681)+~P11(x1681,x1683)
% 58.67/58.84 [169]~P13(x1692,x1694,x1693)+E(x1691,x1692)+~P6(x1694,x1691,x1692)+~P11(x1691,x1693)
% 58.67/58.84 [241]~P11(x2411,x2412)+~P15(x2411,x2413,x2412)+P10(x2411,x2412,x2413,x2414)+P11(f8(x2411,x2412,x2413,x2414),x2414)
% 58.67/58.84 [242]~P11(x2421,x2422)+~P3(x2421,x2423,x2422)+P9(x2421,x2422,x2423,x2424)+P11(f9(x2421,x2422,x2423,x2424),x2424)
% 58.67/58.84 [243]~P11(x2431,x2432)+~P15(x2431,x2433,x2432)+P10(x2431,x2432,x2433,x2434)+P15(f8(x2431,x2432,x2433,x2434),x2433,x2432)
% 58.67/58.84 [244]~P11(x2441,x2442)+~P3(x2441,x2443,x2442)+P9(x2441,x2442,x2443,x2444)+P3(f9(x2441,x2442,x2443,x2444),x2443,x2442)
% 58.67/58.84 [245]~P11(x2451,x2452)+~P15(x2451,x2453,x2452)+P10(x2451,x2452,x2453,x2454)+~P6(x2453,x2451,f8(x2451,x2452,x2453,x2454))
% 58.67/58.84 [246]~P11(x2461,x2462)+~P3(x2461,x2463,x2462)+P9(x2461,x2462,x2463,x2464)+~P6(x2463,f9(x2461,x2462,x2463,x2464),x2461)
% 58.67/58.84 [239]~P10(x2392,x2395,x2391,x2394)+P6(x2391,x2392,x2393)+~P15(x2393,x2391,x2395)+~P11(x2393,x2394)
% 58.67/58.84 [240]~P9(x2403,x2405,x2401,x2404)+P6(x2401,x2402,x2403)+~P3(x2402,x2401,x2405)+~P11(x2402,x2404)
% 58.67/58.84 [167]P6(x1671,x1673,x1672)+~P11(x1673,x1674)+~P14(x1671,x1674)+P6(x1671,x1672,x1673)+~P11(x1672,x1674)
% 58.67/58.84 [190]~P11(x1901,x1903)+~P6(x1904,x1902,x1901)+~P6(x1904,x1901,x1902)+E(x1901,x1902)+~P11(x1902,x1903)+~P5(x1904,x1903)
% 58.67/58.84 [209]~P11(x2092,x2094)+~P5(x2091,x2094)+~P6(x2091,x2095,x2093)+~P6(x2091,x2092,x2095)+P6(x2091,x2092,x2093)+~P11(x2093,x2094)+~P11(x2095,x2094)
% 58.67/58.84 %EqnAxiom
% 58.67/58.84 [1]E(x11,x11)
% 58.67/58.84 [2]E(x22,x21)+~E(x21,x22)
% 58.67/58.84 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 58.67/58.84 [4]~E(x41,x42)+E(f12(x41),f12(x42))
% 58.67/58.84 [5]~E(x51,x52)+E(f9(x51,x53,x54,x55),f9(x52,x53,x54,x55))
% 58.67/58.84 [6]~E(x61,x62)+E(f9(x63,x61,x64,x65),f9(x63,x62,x64,x65))
% 58.67/58.84 [7]~E(x71,x72)+E(f9(x73,x74,x71,x75),f9(x73,x74,x72,x75))
% 58.67/58.84 [8]~E(x81,x82)+E(f9(x83,x84,x85,x81),f9(x83,x84,x85,x82))
% 58.67/58.84 [9]~E(x91,x92)+E(f13(x91),f13(x92))
% 58.67/58.84 [10]~E(x101,x102)+E(f31(x101,x103),f31(x102,x103))
% 58.67/58.84 [11]~E(x111,x112)+E(f31(x113,x111),f31(x113,x112))
% 58.67/58.84 [12]~E(x121,x122)+E(f8(x121,x123,x124,x125),f8(x122,x123,x124,x125))
% 58.67/58.84 [13]~E(x131,x132)+E(f8(x133,x131,x134,x135),f8(x133,x132,x134,x135))
% 58.67/58.84 [14]~E(x141,x142)+E(f8(x143,x144,x141,x145),f8(x143,x144,x142,x145))
% 58.67/58.84 [15]~E(x151,x152)+E(f8(x153,x154,x155,x151),f8(x153,x154,x155,x152))
% 58.67/58.84 [16]~E(x161,x162)+E(f22(x161,x163),f22(x162,x163))
% 58.67/58.84 [17]~E(x171,x172)+E(f22(x173,x171),f22(x173,x172))
% 58.67/58.84 [18]~E(x181,x182)+E(f14(x181,x183),f14(x182,x183))
% 58.67/58.84 [19]~E(x191,x192)+E(f14(x193,x191),f14(x193,x192))
% 58.67/58.84 [20]~E(x201,x202)+E(f30(x201),f30(x202))
% 58.67/58.84 [21]~E(x211,x212)+E(f16(x211,x213),f16(x212,x213))
% 58.67/58.84 [22]~E(x221,x222)+E(f16(x223,x221),f16(x223,x222))
% 58.67/58.84 [23]~E(x231,x232)+E(f32(x231,x233),f32(x232,x233))
% 58.67/58.84 [24]~E(x241,x242)+E(f32(x243,x241),f32(x243,x242))
% 58.67/58.84 [25]~E(x251,x252)+E(f18(x251,x253),f18(x252,x253))
% 58.67/58.84 [26]~E(x261,x262)+E(f18(x263,x261),f18(x263,x262))
% 58.67/58.84 [27]~E(x271,x272)+E(f33(x271),f33(x272))
% 58.67/58.84 [28]~E(x281,x282)+E(f19(x281,x283),f19(x282,x283))
% 58.67/58.84 [29]~E(x291,x292)+E(f19(x293,x291),f19(x293,x292))
% 58.67/58.84 [30]~E(x301,x302)+E(f21(x301,x303),f21(x302,x303))
% 58.67/58.84 [31]~E(x311,x312)+E(f21(x313,x311),f21(x313,x312))
% 58.67/58.84 [32]~E(x321,x322)+E(f17(x321,x323),f17(x322,x323))
% 58.67/58.84 [33]~E(x331,x332)+E(f17(x333,x331),f17(x333,x332))
% 58.67/58.84 [34]~E(x341,x342)+E(f20(x341,x343),f20(x342,x343))
% 58.67/58.84 [35]~E(x351,x352)+E(f20(x353,x351),f20(x353,x352))
% 58.67/58.84 [36]~E(x361,x362)+E(f15(x361,x363),f15(x362,x363))
% 58.67/58.84 [37]~E(x371,x372)+E(f15(x373,x371),f15(x373,x372))
% 58.67/58.84 [38]~E(x381,x382)+E(f7(x381,x383,x384),f7(x382,x383,x384))
% 58.67/58.84 [39]~E(x391,x392)+E(f7(x393,x391,x394),f7(x393,x392,x394))
% 58.67/58.84 [40]~E(x401,x402)+E(f7(x403,x404,x401),f7(x403,x404,x402))
% 58.67/58.84 [41]~E(x411,x412)+E(f5(x411,x413),f5(x412,x413))
% 58.67/58.84 [42]~E(x421,x422)+E(f5(x423,x421),f5(x423,x422))
% 58.67/58.84 [43]~E(x431,x432)+E(f23(x431,x433),f23(x432,x433))
% 58.67/58.84 [44]~E(x441,x442)+E(f23(x443,x441),f23(x443,x442))
% 58.67/58.84 [45]~E(x451,x452)+E(f24(x451,x453),f24(x452,x453))
% 58.67/58.84 [46]~E(x461,x462)+E(f24(x463,x461),f24(x463,x462))
% 58.67/58.84 [47]~E(x471,x472)+E(f25(x471,x473),f25(x472,x473))
% 58.67/58.84 [48]~E(x481,x482)+E(f25(x483,x481),f25(x483,x482))
% 58.67/58.84 [49]~E(x491,x492)+E(f6(x491,x493,x494),f6(x492,x493,x494))
% 58.67/58.84 [50]~E(x501,x502)+E(f6(x503,x501,x504),f6(x503,x502,x504))
% 58.67/58.84 [51]~E(x511,x512)+E(f6(x513,x514,x511),f6(x513,x514,x512))
% 58.67/58.84 [52]~E(x521,x522)+E(f26(x521,x523,x524),f26(x522,x523,x524))
% 58.67/58.84 [53]~E(x531,x532)+E(f26(x533,x531,x534),f26(x533,x532,x534))
% 58.67/58.84 [54]~E(x541,x542)+E(f26(x543,x544,x541),f26(x543,x544,x542))
% 58.67/58.84 [55]~E(x551,x552)+E(f27(x551,x553,x554),f27(x552,x553,x554))
% 58.67/58.84 [56]~E(x561,x562)+E(f27(x563,x561,x564),f27(x563,x562,x564))
% 58.67/58.84 [57]~E(x571,x572)+E(f27(x573,x574,x571),f27(x573,x574,x572))
% 58.67/58.84 [58]~E(x581,x582)+E(f29(x581,x583,x584),f29(x582,x583,x584))
% 58.67/58.84 [59]~E(x591,x592)+E(f29(x593,x591,x594),f29(x593,x592,x594))
% 58.67/58.84 [60]~E(x601,x602)+E(f29(x603,x604,x601),f29(x603,x604,x602))
% 58.67/58.84 [61]~E(x611,x612)+E(f28(x611,x613,x614),f28(x612,x613,x614))
% 58.67/58.84 [62]~E(x621,x622)+E(f28(x623,x621,x624),f28(x623,x622,x624))
% 58.67/58.84 [63]~E(x631,x632)+E(f28(x633,x634,x631),f28(x633,x634,x632))
% 58.67/58.84 [64]P1(x642,x643)+~E(x641,x642)+~P1(x641,x643)
% 58.67/58.84 [65]P1(x653,x652)+~E(x651,x652)+~P1(x653,x651)
% 58.67/58.84 [66]P6(x662,x663,x664)+~E(x661,x662)+~P6(x661,x663,x664)
% 58.67/58.84 [67]P6(x673,x672,x674)+~E(x671,x672)+~P6(x673,x671,x674)
% 58.67/58.84 [68]P6(x683,x684,x682)+~E(x681,x682)+~P6(x683,x684,x681)
% 58.67/58.84 [69]P3(x692,x693,x694)+~E(x691,x692)+~P3(x691,x693,x694)
% 58.67/58.84 [70]P3(x703,x702,x704)+~E(x701,x702)+~P3(x703,x701,x704)
% 58.67/58.84 [71]P3(x713,x714,x712)+~E(x711,x712)+~P3(x713,x714,x711)
% 58.67/58.84 [72]P2(x722,x723)+~E(x721,x722)+~P2(x721,x723)
% 58.67/58.84 [73]P2(x733,x732)+~E(x731,x732)+~P2(x733,x731)
% 58.67/58.84 [74]P5(x742,x743)+~E(x741,x742)+~P5(x741,x743)
% 58.67/58.84 [75]P5(x753,x752)+~E(x751,x752)+~P5(x753,x751)
% 58.67/58.84 [76]P11(x762,x763)+~E(x761,x762)+~P11(x761,x763)
% 58.67/58.84 [77]P11(x773,x772)+~E(x771,x772)+~P11(x773,x771)
% 58.67/58.84 [78]P10(x782,x783,x784,x785)+~E(x781,x782)+~P10(x781,x783,x784,x785)
% 58.67/58.84 [79]P10(x793,x792,x794,x795)+~E(x791,x792)+~P10(x793,x791,x794,x795)
% 58.67/58.84 [80]P10(x803,x804,x802,x805)+~E(x801,x802)+~P10(x803,x804,x801,x805)
% 58.67/58.84 [81]P10(x813,x814,x815,x812)+~E(x811,x812)+~P10(x813,x814,x815,x811)
% 58.67/58.84 [82]P9(x822,x823,x824,x825)+~E(x821,x822)+~P9(x821,x823,x824,x825)
% 58.67/58.84 [83]P9(x833,x832,x834,x835)+~E(x831,x832)+~P9(x833,x831,x834,x835)
% 58.67/58.84 [84]P9(x843,x844,x842,x845)+~E(x841,x842)+~P9(x843,x844,x841,x845)
% 58.67/58.84 [85]P9(x853,x854,x855,x852)+~E(x851,x852)+~P9(x853,x854,x855,x851)
% 58.67/58.84 [86]P13(x862,x863,x864)+~E(x861,x862)+~P13(x861,x863,x864)
% 58.67/58.84 [87]P13(x873,x872,x874)+~E(x871,x872)+~P13(x873,x871,x874)
% 58.67/58.84 [88]P13(x883,x884,x882)+~E(x881,x882)+~P13(x883,x884,x881)
% 58.67/58.84 [89]P15(x892,x893,x894)+~E(x891,x892)+~P15(x891,x893,x894)
% 58.67/58.84 [90]P15(x903,x902,x904)+~E(x901,x902)+~P15(x903,x901,x904)
% 58.67/58.84 [91]P15(x913,x914,x912)+~E(x911,x912)+~P15(x913,x914,x911)
% 58.67/58.84 [92]P4(x922,x923)+~E(x921,x922)+~P4(x921,x923)
% 58.67/58.84 [93]P4(x933,x932)+~E(x931,x932)+~P4(x933,x931)
% 58.67/58.84 [94]P12(x942,x943,x944)+~E(x941,x942)+~P12(x941,x943,x944)
% 58.67/58.84 [95]P12(x953,x952,x954)+~E(x951,x952)+~P12(x953,x951,x954)
% 58.67/58.84 [96]P12(x963,x964,x962)+~E(x961,x962)+~P12(x963,x964,x961)
% 58.67/58.84 [97]P8(x972,x973,x974)+~E(x971,x972)+~P8(x971,x973,x974)
% 58.67/58.84 [98]P8(x983,x982,x984)+~E(x981,x982)+~P8(x983,x981,x984)
% 58.67/58.84 [99]P8(x993,x994,x992)+~E(x991,x992)+~P8(x993,x994,x991)
% 58.67/58.84 [100]P7(x1002,x1003,x1004)+~E(x1001,x1002)+~P7(x1001,x1003,x1004)
% 58.67/58.84 [101]P7(x1013,x1012,x1014)+~E(x1011,x1012)+~P7(x1013,x1011,x1014)
% 58.67/58.84 [102]P7(x1023,x1024,x1022)+~E(x1021,x1022)+~P7(x1023,x1024,x1021)
% 58.67/58.84 [103]P14(x1032,x1033)+~E(x1031,x1032)+~P14(x1031,x1033)
% 58.67/58.84 [104]P14(x1043,x1042)+~E(x1041,x1042)+~P14(x1043,x1041)
% 58.67/58.84
% 58.67/58.84 %-------------------------------------------
% 58.67/58.84 cnf(247,plain,
% 58.67/58.84 (P11(x2471,f12(x2471))),
% 58.67/58.84 inference(equality_inference,[],[112])).
% 58.67/58.84 cnf(248,plain,
% 58.67/58.84 (P11(x2481,f31(x2482,x2481))),
% 58.67/58.84 inference(equality_inference,[],[120])).
% 58.67/58.84 cnf(249,plain,
% 58.67/58.84 (P11(x2491,f31(x2491,x2492))),
% 58.67/58.84 inference(equality_inference,[],[121])).
% 58.67/58.84 cnf(250,plain,
% 58.67/58.84 (P3(x2501,x2502,a4)),
% 58.67/58.84 inference(scs_inference,[],[110,166])).
% 58.67/58.84 cnf(251,plain,
% 58.67/58.84 (~P11(x2511,a4)),
% 58.67/58.84 inference(rename_variables,[],[110])).
% 58.67/58.84 cnf(255,plain,
% 58.67/58.84 (P1(a4,x2551)),
% 58.67/58.84 inference(scs_inference,[],[111,110,251,166,236,123])).
% 58.67/58.84 cnf(256,plain,
% 58.67/58.84 (~P11(x2561,a4)),
% 58.67/58.84 inference(rename_variables,[],[110])).
% 58.67/58.84 cnf(258,plain,
% 58.67/58.84 (~P11(x2581,f33(a4))),
% 58.67/58.84 inference(scs_inference,[],[111,110,251,256,166,236,123,133])).
% 58.67/58.84 cnf(259,plain,
% 58.67/58.84 (~P11(x2591,a4)),
% 58.67/58.84 inference(rename_variables,[],[110])).
% 58.67/58.84 cnf(261,plain,
% 58.67/58.84 (~P7(x2611,x2612,a4)),
% 58.67/58.84 inference(scs_inference,[],[111,110,251,256,259,166,236,123,133,146])).
% 58.67/58.84 cnf(263,plain,
% 58.67/58.84 (~P8(x2631,x2632,a4)),
% 58.67/58.84 inference(scs_inference,[],[111,110,251,256,259,166,236,123,133,146,147])).
% 58.67/58.84 cnf(265,plain,
% 58.67/58.84 (~P12(x2651,x2652,a4)),
% 58.67/58.84 inference(scs_inference,[],[111,110,251,256,259,166,236,123,133,146,147,148])).
% 58.67/58.84 cnf(267,plain,
% 58.67/58.84 (~P13(x2671,x2672,a4)),
% 58.67/58.84 inference(scs_inference,[],[111,110,251,256,259,166,236,123,133,146,147,148,149])).
% 58.67/58.84 cnf(269,plain,
% 58.67/58.84 (P15(x2691,x2692,a4)),
% 58.67/58.84 inference(scs_inference,[],[111,110,251,256,259,166,236,123,133,146,147,148,149,165])).
% 58.67/58.84 cnf(270,plain,
% 58.67/58.84 (~P11(x2701,a4)),
% 58.67/58.84 inference(rename_variables,[],[110])).
% 58.67/58.84 cnf(276,plain,
% 58.67/58.84 (P4(a4,a4)),
% 58.67/58.84 inference(scs_inference,[],[111,110,251,256,259,270,166,236,123,133,146,147,148,149,165,233,234,125])).
% 58.67/58.84 cnf(281,plain,
% 58.67/58.84 (~P11(x2811,a1)+P11(x2811,a2)),
% 58.67/58.84 inference(scs_inference,[],[105,109,111,247,110,251,256,259,270,166,236,123,133,146,147,148,149,165,233,234,125,71,77,124])).
% 58.67/58.84 cnf(286,plain,
% 58.67/58.84 (P14(x2861,f33(a4))+~P2(x2861,f33(a4))),
% 58.67/58.84 inference(scs_inference,[],[105,109,111,247,110,251,256,259,270,166,236,123,133,146,147,148,149,165,233,234,125,71,77,124,135,136])).
% 58.67/58.84 cnf(294,plain,
% 58.67/58.84 (~P8(x2941,x2942,f33(a4))),
% 58.67/58.84 inference(scs_inference,[],[258,147])).
% 58.67/58.84 cnf(296,plain,
% 58.67/58.84 (~P11(x2961,f33(f33(a4)))),
% 58.67/58.84 inference(scs_inference,[],[258,147,133])).
% 58.67/58.84 cnf(297,plain,
% 58.67/58.84 (~P11(x2971,f33(a4))),
% 58.67/58.84 inference(rename_variables,[],[258])).
% 58.67/58.84 cnf(301,plain,
% 58.67/58.84 (P1(f33(a4),x3011)),
% 58.67/58.84 inference(scs_inference,[],[258,297,147,133,233,123])).
% 58.67/58.84 cnf(302,plain,
% 58.67/58.84 (~P11(x3021,f33(a4))),
% 58.67/58.84 inference(rename_variables,[],[258])).
% 58.67/58.85 cnf(304,plain,
% 58.67/58.85 (~P7(x3041,x3042,f33(a4))),
% 58.67/58.85 inference(scs_inference,[],[258,297,302,147,133,233,123,146])).
% 58.67/58.85 cnf(308,plain,
% 58.67/58.85 (P3(x3081,x3082,f33(a4))),
% 58.67/58.85 inference(scs_inference,[],[258,297,302,147,133,233,123,146,234,166])).
% 58.67/58.85 cnf(309,plain,
% 58.67/58.85 (~P11(x3091,f33(a4))),
% 58.67/58.85 inference(rename_variables,[],[258])).
% 58.67/58.85 cnf(311,plain,
% 58.67/58.85 (~P12(x3111,x3112,f33(a4))),
% 58.67/58.85 inference(scs_inference,[],[258,297,302,309,147,133,233,123,146,234,166,148])).
% 58.67/58.85 cnf(313,plain,
% 58.67/58.85 (P15(x3131,x3132,f33(a4))),
% 58.67/58.85 inference(scs_inference,[],[258,297,302,309,147,133,233,123,146,234,166,148,165])).
% 58.67/58.85 cnf(314,plain,
% 58.67/58.85 (~P11(x3141,f33(a4))),
% 58.67/58.85 inference(rename_variables,[],[258])).
% 58.67/58.85 cnf(316,plain,
% 58.67/58.85 (~P13(x3161,x3162,f33(a4))),
% 58.67/58.85 inference(scs_inference,[],[258,297,302,309,314,147,133,233,123,146,234,166,148,165,149])).
% 58.67/58.85 cnf(318,plain,
% 58.67/58.85 (P4(f33(a4),a4)),
% 58.67/58.85 inference(scs_inference,[],[255,258,297,302,309,314,147,133,233,123,146,234,166,148,165,149,125])).
% 58.67/58.85 cnf(323,plain,
% 58.67/58.85 (~E(a4,a1)),
% 58.67/58.85 inference(scs_inference,[],[111,250,255,248,258,297,302,309,314,147,133,233,123,146,234,166,148,165,149,125,77,71])).
% 58.67/58.85 cnf(354,plain,
% 58.67/58.85 (P11(x3541,f31(x3541,x3542))),
% 58.67/58.85 inference(rename_variables,[],[249])).
% 58.67/58.85 cnf(355,plain,
% 58.67/58.85 (~E(f33(a4),a1)),
% 58.67/58.85 inference(scs_inference,[],[111,308,301,110,249,296,234,147,233,149,146,148,125,77,71])).
% 58.67/58.85 cnf(359,plain,
% 58.67/58.85 (~P15(x3591,x3592,f31(x3593,x3594))+P6(x3592,x3593,x3591)),
% 58.67/58.85 inference(scs_inference,[],[111,308,301,110,249,354,296,234,147,233,149,146,148,125,77,71,160,161])).
% 58.67/58.85 cnf(383,plain,
% 58.67/58.85 (P11(x3831,f12(x3831))),
% 58.67/58.85 inference(rename_variables,[],[247])).
% 58.67/58.85 cnf(387,plain,
% 58.67/58.85 (~P11(x3871,a1)+P11(x3871,a10)),
% 58.67/58.85 inference(scs_inference,[],[106,318,258,247,383,77,92,161,124])).
% 58.77/58.85 cnf(459,plain,
% 58.77/58.85 (P15(x4591,x4592,x4593)+~E(a4,x4593)),
% 58.77/58.85 inference(scs_inference,[],[107,318,276,248,269,160,125,65,93,92,91])).
% 58.77/58.85 cnf(483,plain,
% 58.77/58.85 (P15(x4831,x4832,x4833)+~E(f33(a4),x4833)),
% 58.77/58.85 inference(scs_inference,[],[276,313,93,91])).
% 58.77/58.85 cnf(490,plain,
% 58.77/58.85 (P11(x4901,f12(x4901))),
% 58.77/58.85 inference(rename_variables,[],[247])).
% 58.77/58.85 cnf(493,plain,
% 58.77/58.85 (~P11(x4931,f33(a4))),
% 58.77/58.85 inference(rename_variables,[],[258])).
% 58.77/58.85 cnf(495,plain,
% 58.77/58.85 (~P11(x4951,f33(a4))),
% 58.77/58.85 inference(rename_variables,[],[258])).
% 58.77/58.85 cnf(497,plain,
% 58.77/58.85 (P5(x4971,f33(a4))+P11(f18(f33(a4),x4971),f33(a4))+P11(f21(f33(a4),x4971),f33(a4))),
% 58.77/58.85 inference(scs_inference,[],[109,258,493,495,247,490,151])).
% 58.77/58.85 cnf(498,plain,
% 58.77/58.85 (~P11(a1,f12(f33(a4)))),
% 58.77/58.85 inference(scs_inference,[],[355,2,113])).
% 58.77/58.85 cnf(514,plain,
% 58.77/58.85 (~P11(x5141,f33(a4))),
% 58.77/58.85 inference(rename_variables,[],[258])).
% 58.77/58.85 cnf(517,plain,
% 58.77/58.85 (~P11(x5171,f33(a4))),
% 58.77/58.85 inference(rename_variables,[],[258])).
% 58.77/58.85 cnf(519,plain,
% 58.77/58.85 (~P11(x5191,f33(a4))),
% 58.77/58.85 inference(rename_variables,[],[258])).
% 58.77/58.85 cnf(521,plain,
% 58.77/58.85 (~P11(x5211,f33(a4))),
% 58.77/58.85 inference(rename_variables,[],[258])).
% 58.77/58.85 cnf(523,plain,
% 58.77/58.85 (~P11(x5231,f33(a4))),
% 58.77/58.85 inference(rename_variables,[],[258])).
% 58.77/58.85 cnf(528,plain,
% 58.77/58.85 (~P11(x5281,f33(a4))),
% 58.77/58.85 inference(rename_variables,[],[258])).
% 58.77/58.85 cnf(531,plain,
% 58.77/58.85 (P5(x5311,f33(a4))),
% 58.77/58.85 inference(scs_inference,[],[308,301,258,514,517,519,521,523,528,296,313,498,294,304,311,316,112,233,148,149,234,147,146,497,129,173,170,172,171,161,124,162,77])).
% 58.77/58.85 cnf(620,plain,
% 58.77/58.85 (P11(a4,f13(f33(a4)))),
% 58.77/58.85 inference(scs_inference,[],[318,114,119])).
% 58.77/58.85 cnf(705,plain,
% 58.77/58.85 (P11(f33(a4),f13(a4))),
% 58.77/58.85 inference(scs_inference,[],[318,115,119])).
% 58.77/58.85 cnf(706,plain,
% 58.77/58.85 (~E(f13(a4),f33(a4))),
% 58.77/58.85 inference(scs_inference,[],[705,258,77])).
% 58.77/58.85 cnf(782,plain,
% 58.77/58.85 (P14(x7821,f33(a4))),
% 58.77/58.85 inference(scs_inference,[],[531,117,286])).
% 58.77/58.85 cnf(1960,plain,
% 58.77/58.85 (P11(a1,f32(x19601,f13(a2)))),
% 58.77/58.85 inference(scs_inference,[],[105,127,119])).
% 58.77/58.85 cnf(1961,plain,
% 58.77/58.85 (P11(a1,f13(a2))),
% 58.77/58.85 inference(scs_inference,[],[1960,258,144])).
% 58.77/58.85 cnf(2113,plain,
% 58.77/58.85 (~P11(a4,f25(x21131,f12(a1)))),
% 58.77/58.85 inference(scs_inference,[],[323,137,113])).
% 58.77/58.85 cnf(2126,plain,
% 58.77/58.85 (~P11(a4,f12(a1))),
% 58.77/58.85 inference(scs_inference,[],[620,2113,149,148,233,147,234,146,142])).
% 58.77/58.85 cnf(2145,plain,
% 58.77/58.85 (~E(a1,a4)),
% 58.77/58.85 inference(scs_inference,[],[2126,247,234,147,149,148,233,146,76])).
% 58.77/58.85 cnf(3401,plain,
% 58.77/58.85 (~P11(x34011,a4)),
% 58.77/58.85 inference(rename_variables,[],[110])).
% 58.77/58.85 cnf(3402,plain,
% 58.77/58.85 (~P11(x34021,a4)),
% 58.77/58.85 inference(rename_variables,[],[110])).
% 58.77/58.85 cnf(3404,plain,
% 58.77/58.85 (P5(x34041,a4)+P11(f20(a4,x34041),a4)+P11(f19(a4,x34041),a4)),
% 58.77/58.85 inference(scs_inference,[],[110,3401,3402,153])).
% 58.77/58.85 cnf(3406,plain,
% 58.77/58.85 (~P11(x34061,a4)),
% 58.77/58.85 inference(rename_variables,[],[110])).
% 58.77/58.85 cnf(3407,plain,
% 58.77/58.85 (~P11(x34071,a4)),
% 58.77/58.85 inference(rename_variables,[],[110])).
% 58.77/58.85 cnf(3412,plain,
% 58.77/58.85 (~P11(x34121,a4)),
% 58.77/58.85 inference(rename_variables,[],[110])).
% 58.77/58.85 cnf(3414,plain,
% 58.77/58.85 (~P11(x34141,a4)),
% 58.77/58.85 inference(rename_variables,[],[110])).
% 58.77/58.85 cnf(3416,plain,
% 58.77/58.85 (~P11(x34161,a4)),
% 58.77/58.85 inference(rename_variables,[],[110])).
% 58.77/58.85 cnf(3420,plain,
% 58.77/58.85 (~P11(x34201,a4)),
% 58.77/58.85 inference(rename_variables,[],[110])).
% 58.77/58.85 cnf(3426,plain,
% 58.77/58.85 (P5(x34261,a4)),
% 58.77/58.85 inference(scs_inference,[],[110,3406,3407,3412,3414,3416,3420,250,255,258,269,261,263,265,267,3404,173,129,172,170,171,76,124,161,162,77])).
% 58.77/58.85 cnf(6751,plain,
% 58.77/58.85 (~P15(f27(a3,a1,a11),a3,f31(a11,x67511))),
% 58.77/58.85 inference(scs_inference,[],[111,359,207])).
% 58.77/58.85 cnf(11803,plain,
% 58.77/58.85 (~P11(x118031,a4)),
% 58.77/58.85 inference(rename_variables,[],[110])).
% 58.77/58.85 cnf(11814,plain,
% 58.77/58.85 (~P11(x118141,a4)),
% 58.77/58.85 inference(rename_variables,[],[110])).
% 58.77/58.85 cnf(11830,plain,
% 58.77/58.85 ($false),
% 58.77/58.85 inference(scs_inference,[],[2145,706,6751,3426,255,782,1961,111,109,108,110,11803,11814,117,2,113,119,459,137,138,139,483,126,207,116,166,118,134,130,142,77,162,124,64,281,387]),
% 58.77/58.85 ['proof']).
% 58.77/58.86 % SZS output end Proof
% 58.77/58.86 % Total time :58.020000s
%------------------------------------------------------------------------------