%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : GEO148-1 : TPTP v8.2.0. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% Computer : n021.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 06:04:02 EDT 2024
% Result : Unsatisfiable 66.23s 66.32s
% Output : CNFRefutation 66.37s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : GEO148-1 : TPTP v8.2.0. Released v2.4.0.
% 0.03/0.12 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% 0.12/0.33 % Computer : n021.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 300
% 0.12/0.33 % DateTime : Fri Jun 21 06:17:24 EDT 2024
% 0.12/0.33 % CPUTime :
% 0.49/0.56 start to proof:theBenchmark
% 66.23/66.28 %-------------------------------------------
% 66.23/66.28 % File :CSE---1.7
% 66.23/66.28 % Problem :theBenchmark
% 66.23/66.28 % Transform :cnf
% 66.23/66.28 % Format :tptp:raw
% 66.23/66.28 % Command :java -jar mcs_scs.jar %d %s
% 66.23/66.28
% 66.23/66.28 % Result :Theorem 65.660000s
% 66.23/66.28 % Output :CNFRefutation 65.660000s
% 66.23/66.28 %-------------------------------------------
% 66.23/66.31 %--------------------------------------------------------------------------
% 66.23/66.31 % File : GEO148-1 : TPTP v8.2.0. Released v2.4.0.
% 66.23/66.31 % Domain : Geometry (Oriented curves)
% 66.23/66.31 % Problem : No meeting if someone has already passed
% 66.23/66.31 % Version : [EHK99] axioms.
% 66.23/66.31 % English : A point can only be a meeting point of two moving objects if
% 66.23/66.31 % it is not the case that one object already passed through it
% 66.23/66.31 % when the other object was still moving towards it
% 66.23/66.31
% 66.23/66.31 % Refs : [KE99] Kulik & Eschenbach (1999), A Geometry of Oriented Curv
% 66.23/66.31 % : [EHK99] Eschenbach et al. (1999), Representing Simple Trajecto
% 66.23/66.31 % Source : [TPTP]
% 66.23/66.31 % Names :
% 66.23/66.31
% 66.23/66.31 % Status : Unsatisfiable
% 66.23/66.32 % Rating : 0.10 v8.1.0, 0.11 v7.4.0, 0.06 v7.3.0, 0.00 v7.0.0, 0.13 v6.4.0, 0.07 v6.3.0, 0.00 v6.2.0, 0.10 v6.1.0, 0.07 v6.0.0, 0.00 v5.5.0, 0.35 v5.3.0, 0.33 v5.2.0, 0.25 v5.1.0, 0.35 v5.0.0, 0.29 v4.1.0, 0.38 v4.0.1, 0.45 v4.0.0, 0.36 v3.7.0, 0.10 v3.5.0, 0.18 v3.4.0, 0.25 v3.3.0, 0.21 v3.2.0, 0.15 v3.1.0, 0.18 v2.7.0, 0.25 v2.6.0, 0.22 v2.5.0, 0.44 v2.4.0
% 66.23/66.32 % Syntax : Number of clauses : 114 ( 8 unt; 42 nHn; 102 RR)
% 66.23/66.32 % Number of literals : 332 ( 41 equ; 168 neg)
% 66.23/66.32 % Maximal clause size : 12 ( 2 avg)
% 66.23/66.32 % Maximal term depth : 4 ( 1 avg)
% 66.23/66.32 % Number of predicates : 16 ( 15 usr; 0 prp; 1-4 aty)
% 66.23/66.32 % Number of functors : 36 ( 36 usr; 5 con; 0-5 aty)
% 66.23/66.32 % Number of variables : 310 ( 19 sgn)
% 66.23/66.32 % SPC : CNF_UNS_RFO_SEQ_NHN
% 66.23/66.32
% 66.23/66.32 % Comments : Created by tptp2X -f tptp -t clausify:otter GEO148+1.p
% 66.23/66.32 %--------------------------------------------------------------------------
% 66.23/66.32 %----Include simple curve axioms
% 66.23/66.32 include('Axioms/GEO004-0.ax').
% 66.23/66.32 %----Include axioms of betweenness for simple curves
% 66.23/66.32 include('Axioms/GEO004-1.ax').
% 66.23/66.32 %----Include oriented curve axioms
% 66.23/66.32 include('Axioms/GEO004-2.ax').
% 66.23/66.32 %----Include trajectory axioms
% 66.23/66.32 include('Axioms/GEO004-3.ax').
% 66.23/66.32 %--------------------------------------------------------------------------
% 66.23/66.32 cnf(t14_156,negated_conjecture,
% 66.23/66.32 connect(sk28,sk29,sk27) ).
% 66.23/66.32
% 66.23/66.32 cnf(t14_157,negated_conjecture,
% 66.23/66.32 ordered_by(trajectory_of(sk29),sk31,sk27) ).
% 66.23/66.32
% 66.23/66.32 cnf(t14_158,negated_conjecture,
% 66.23/66.32 ordered_by(trajectory_of(sk28),sk27,sk30) ).
% 66.23/66.32
% 66.23/66.32 cnf(t14_159,negated_conjecture,
% 66.23/66.32 once(at_the_same_time(at(sk28,sk30),at(sk29,sk31))) ).
% 66.23/66.32
% 66.23/66.32 %--------------------------------------------------------------------------
% 66.23/66.32 %-------------------------------------------
% 66.23/66.32 % Proof found
% 66.23/66.32 % SZS status Theorem for theBenchmark
% 66.23/66.32 % SZS output start Proof
% 66.30/66.34 %ClaNum:202(EqnAxiom:100)
% 66.30/66.34 %VarNum:767(SingletonVarNum:276)
% 66.30/66.34 %MaxLitNum:12
% 66.30/66.34 %MaxfuncDepth:3
% 66.30/66.34 %SharedTerms:14
% 66.30/66.34 %goalClause: 104 105 106 107
% 66.30/66.34 %singleGoalClaCount:4
% 66.30/66.34 [104]P3(a24,a30,a25)
% 66.30/66.34 [105]P14(f31(a24),a25,a32)
% 66.30/66.34 [106]P14(f31(a30),a33,a25)
% 66.30/66.34 [107]P11(f4(f3(a24,a32),f3(a30,a33)))
% 66.30/66.34 [101]P1(f1(x1011))
% 66.30/66.34 [102]P2(f2(x1021),x1021)
% 66.30/66.34 [103]P13(f21(x1031),x1031)
% 66.30/66.34 [108]P4(x1081)+P7(f5(x1081),x1081)
% 66.30/66.34 [110]~P1(x1101)+P7(f15(x1101),x1101)
% 66.30/66.34 [117]~P11(x1171)+P11(f4(x1171,x1171))
% 66.30/66.34 [109]P1(x1091)+~P7(x1092,x1091)
% 66.30/66.34 [112]~P4(x1121)+~P7(x1122,x1121)
% 66.30/66.34 [113]~P7(x1131,x1132)+P8(x1131,x1132)
% 66.30/66.34 [114]~P2(x1141,x1142)+P8(x1141,x1142)
% 66.30/66.34 [115]~P13(x1151,x1152)+P10(x1151,x1152)
% 66.30/66.34 [116]~P9(x1161,x1162)+P10(x1161,x1162)
% 66.30/66.34 [119]~P2(x1191,x1192)+~P7(x1191,x1192)
% 66.30/66.34 [118]~P10(x1181,x1182)+P8(x1181,f1(x1182))
% 66.30/66.34 [122]~P7(x1221,x1222)+~E(f6(x1221,x1222),x1221)
% 66.30/66.34 [123]P10(x1231,x1232)+~P8(x1231,f1(x1232))
% 66.30/66.34 [125]P11(x1251)+~P11(f4(x1252,x1251))
% 66.30/66.34 [126]P11(x1261)+~P11(f4(x1261,x1262))
% 66.30/66.34 [127]P15(x1271,x1272)+P8(f7(x1271,x1272),x1271)
% 66.30/66.34 [133]~P10(x1332,f31(x1331))+P11(f3(x1331,x1332))
% 66.30/66.34 [134]~P7(x1341,x1342)+P7(f6(x1341,x1342),x1342)
% 66.30/66.34 [135]P10(x1351,f31(x1352))+~P11(f3(x1352,x1351))
% 66.30/66.34 [144]P15(x1441,x1442)+~P8(f7(x1441,x1442),x1442)
% 66.30/66.34 [146]~P11(f4(x1462,x1461))+P11(f4(x1461,x1462))
% 66.30/66.34 [158]~P2(x1581,x1582)+P12(x1581,f17(x1581,x1582),f8(x1581,x1582))
% 66.30/66.34 [149]~P2(x1491,x1492)+E(f34(f17(x1491,x1492),f8(x1491,x1492)),x1492)
% 66.30/66.34 [167]~P11(x1671)+P11(f4(x1671,f3(x1672,f26(x1672,x1671))))
% 66.30/66.34 [150]P8(x1501,x1502)+~P12(x1501,x1503,x1502)
% 66.30/66.34 [151]P8(x1511,x1512)+~P12(x1511,x1512,x1513)
% 66.30/66.34 [152]P10(x1521,x1522)+~P14(x1522,x1523,x1521)
% 66.30/66.34 [153]P10(x1531,x1532)+~P14(x1532,x1531,x1533)
% 66.30/66.34 [156]~P12(x1563,x1562,x1561)+E(f11(x1561,x1562),f34(x1562,x1561))
% 66.30/66.34 [170]~P11(f4(f4(x1701,x1702),x1703))+P11(f4(x1701,f4(x1702,x1703)))
% 66.30/66.34 [171]~P11(f4(x1711,f4(x1712,x1713)))+P11(f4(f4(x1711,x1712),x1713))
% 66.30/66.34 [174]~P3(x1741,x1743,x1742)+P11(f4(f3(x1741,x1742),f3(x1743,x1742)))
% 66.30/66.34 [179]P3(x1791,x1792,x1793)+~P11(f4(f3(x1791,x1793),f3(x1792,x1793)))
% 66.30/66.34 [183]~E(x1831,x1832)+~P5(x1833,x1831,x1834,x1832)
% 66.30/66.34 [194]~P5(x1944,x1943,x1942,x1941)+P7(x1941,f18(x1941,x1942,x1943,x1944))
% 66.30/66.34 [195]~P5(x1954,x1951,x1953,x1952)+P7(x1951,f18(x1952,x1953,x1951,x1954))
% 66.30/66.34 [196]~P5(x1964,x1963,x1961,x1962)+P2(x1961,f18(x1962,x1961,x1963,x1964))
% 66.30/66.34 [197]~P5(x1974,x1973,x1972,x1971)+P15(f18(x1971,x1972,x1973,x1974),x1974)
% 66.30/66.34 [199]~P6(x1991,x1994,x1993,x1992)+P5(f22(x1991,x1992,x1993,x1994),x1994,x1993,x1992)
% 66.30/66.34 [111]P1(x1111)+~P15(x1111,x1112)+E(x1111,x1112)
% 66.30/66.34 [124]P2(x1241,x1242)+~P8(x1241,x1242)+P7(x1241,x1242)
% 66.30/66.34 [131]~P10(x1311,x1312)+P13(x1311,x1312)+~E(f16(x1312,x1311),x1311)
% 66.30/66.34 [132]~P10(x1321,x1322)+P9(x1321,x1322)+~E(f19(x1322,x1321),x1321)
% 66.30/66.34 [138]~P8(x1381,x1382)+P7(x1381,x1382)+P8(x1381,f9(x1382,x1381))
% 66.30/66.34 [139]~P8(x1391,x1392)+P7(x1391,x1392)+P8(x1391,f13(x1392,x1391))
% 66.30/66.34 [140]~P8(x1401,x1402)+P7(x1401,x1402)+P15(f9(x1402,x1401),x1402)
% 66.30/66.34 [141]~P8(x1411,x1412)+P7(x1411,x1412)+P15(f13(x1412,x1411),x1412)
% 66.30/66.34 [142]~P10(x1421,x1422)+P13(x1421,x1422)+P10(f16(x1422,x1421),x1422)
% 66.30/66.34 [143]~P10(x1431,x1432)+P9(x1431,x1432)+P10(f19(x1432,x1431),x1432)
% 66.30/66.34 [147]E(x1471,x1472)+P8(f10(x1471,x1472),x1472)+P8(f10(x1471,x1472),x1471)
% 66.30/66.34 [148]P8(f20(x1482,x1481),x1481)+P10(f20(x1482,x1481),x1482)+E(x1481,f35(x1482))
% 66.30/66.34 [157]E(x1571,x1572)+~P8(f10(x1571,x1572),x1572)+~P8(f10(x1571,x1572),x1571)
% 66.30/66.34 [159]~P8(f20(x1592,x1591),x1591)+~P10(f20(x1592,x1591),x1592)+E(x1591,f35(x1592))
% 66.30/66.34 [160]~P8(x1601,x1602)+P7(x1601,x1602)+~P15(f9(x1602,x1601),f13(x1602,x1601))
% 66.30/66.34 [161]~P8(x1611,x1612)+P7(x1611,x1612)+~P15(f13(x1612,x1611),f9(x1612,x1611))
% 66.30/66.34 [165]~P10(x1651,x1652)+P13(x1651,x1652)+~P14(x1652,x1651,f16(x1652,x1651))
% 66.30/66.34 [166]~P10(x1661,x1662)+P9(x1661,x1662)+~P14(x1662,f19(x1662,x1661),x1661)
% 66.30/66.34 [172]E(x1721,x1722)+P14(x1722,f28(x1722,x1721),f29(x1722,x1721))+P14(x1721,f28(x1722,x1721),f29(x1722,x1721))
% 66.30/66.34 [180]E(x1801,x1802)+~P14(x1802,f28(x1801,x1802),f29(x1801,x1802))+~P14(x1801,f28(x1801,x1802),f29(x1801,x1802))
% 66.30/66.34 [128]~P8(x1281,x1283)+P8(x1281,x1282)+~P15(x1283,x1282)
% 66.30/66.34 [120]~P10(x1201,x1203)+P8(x1201,x1202)+~E(x1202,f35(x1203))
% 66.30/66.34 [121]~P8(x1211,x1213)+P10(x1211,x1212)+~E(x1213,f35(x1212))
% 66.30/66.34 [184]~P8(f12(x1843,x1842,x1841),x1841)+~P8(f12(x1843,x1842,x1841),x1842)+E(x1841,f34(x1842,x1843))
% 66.30/66.34 [185]~P8(f12(x1853,x1852,x1851),x1851)+~P8(f12(x1853,x1852,x1851),x1853)+E(x1851,f34(x1852,x1853))
% 66.30/66.34 [186]~P14(x1861,x1863,x1862)+~P14(x1861,x1864,x1863)+P6(x1861,x1862,x1863,x1864)
% 66.30/66.34 [187]~P14(x1871,x1873,x1874)+~P14(x1871,x1872,x1873)+P6(x1871,x1872,x1873,x1874)
% 66.30/66.34 [189]P14(x1891,x1893,x1892)+P14(x1891,x1892,x1893)+~P6(x1891,x1894,x1893,x1892)
% 66.30/66.34 [190]~P6(x1901,x1904,x1903,x1902)+P14(x1901,x1902,x1903)+P14(x1901,x1904,x1903)
% 66.30/66.34 [191]~P6(x1911,x1914,x1912,x1913)+P14(x1911,x1912,x1913)+P14(x1911,x1912,x1914)
% 66.30/66.34 [192]P14(x1921,x1923,x1922)+P14(x1921,x1922,x1923)+~P6(x1921,x1923,x1922,x1924)
% 66.30/66.34 [129]~P8(x1291,x1294)+P8(x1291,x1292)+~E(x1292,f34(x1293,x1294))
% 66.30/66.34 [130]~P8(x1301,x1303)+P8(x1301,x1302)+~E(x1302,f34(x1303,x1304))
% 66.30/66.34 [198]~P10(x1981,x1982)+~P6(x1982,x1985,x1984,x1983)+P8(x1981,f22(x1982,x1983,x1984,x1985))
% 66.30/66.34 [200]P10(x2001,x2002)+~P6(x2002,x2003,x2004,x2005)+~P8(x2001,f22(x2002,x2005,x2004,x2003))
% 66.30/66.34 [154]~P10(x1542,x1543)+~P9(x1541,x1543)+E(x1541,x1542)+P14(x1543,x1542,x1541)
% 66.30/66.34 [155]~P13(x1551,x1553)+~P10(x1552,x1553)+E(x1551,x1552)+P14(x1553,x1551,x1552)
% 66.30/66.34 [175]~P8(x1751,x1753)+~P8(x1751,x1752)+P12(x1751,x1752,x1753)+P8(f14(x1753,x1752,x1751),x1753)
% 66.30/66.34 [176]~P8(x1761,x1763)+~P8(x1761,x1762)+P12(x1761,x1762,x1763)+P8(f14(x1763,x1762,x1761),x1762)
% 66.30/66.34 [182]P8(f12(x1823,x1822,x1821),x1821)+P8(f12(x1823,x1822,x1821),x1822)+P8(f12(x1823,x1822,x1821),x1823)+E(x1821,f34(x1822,x1823))
% 66.30/66.34 [163]~P8(x1631,x1632)+P7(x1631,x1632)+~P12(x1634,x1633,x1632)+~P8(x1631,x1633)
% 66.30/66.34 [164]~P8(x1641,x1642)+P7(x1641,x1642)+~P12(x1644,x1642,x1643)+~P8(x1641,x1643)
% 66.30/66.35 [137]~P8(x1371,x1374)+P8(x1371,x1372)+P8(x1371,x1373)+~E(x1374,f34(x1373,x1372))
% 66.30/66.35 [201]~P5(x2015,x2012,x2013,x2014)+P6(x2011,x2012,x2013,x2014)+P8(f23(x2015,x2011,x2014,x2013,x2012),x2015)+P10(f23(x2015,x2011,x2014,x2013,x2012),x2011)
% 66.30/66.35 [202]P6(x2021,x2022,x2023,x2024)+~P5(x2025,x2022,x2023,x2024)+~P8(f23(x2025,x2021,x2024,x2023,x2022),x2025)+~P10(f23(x2025,x2021,x2024,x2023,x2022),x2021)
% 66.30/66.35 [193]~P14(f31(x1931),x1932,x1933)+~P14(f31(x1934),x1935,x1936)+~P11(f4(f3(x1934,x1936),f3(x1931,x1932)))+~P11(f4(f3(x1934,x1935),f3(x1931,x1933)))
% 66.30/66.35 [173]~P1(x1733)+~P8(x1732,x1733)+~P8(x1731,x1733)+E(x1731,x1732)+P14(f27(x1733,x1732,x1731),x1731,x1732)
% 66.30/66.35 [188]~P8(x1881,x1883)+~P8(x1881,x1882)+P12(x1881,x1882,x1883)+~P7(f14(x1883,x1882,x1881),x1883)+~P7(f14(x1883,x1882,x1881),x1882)
% 66.30/66.35 [168]~P4(x1684)+~P7(x1681,x1682)+P12(x1681,x1682,x1683)+~P12(x1685,x1682,x1683)+~E(x1684,f34(x1682,x1683))
% 66.30/66.35 [136]E(x1363,x1361)+~P7(x1361,x1364)+~P7(x1363,x1364)+E(x1361,x1362)+E(x1363,x1362)+~P7(x1362,x1364)
% 66.30/66.35 [169]~P1(x1694)+~P8(x1693,x1694)+~P8(x1692,x1694)+~P8(x1691,x1694)+E(x1691,x1692)+P10(x1693,f27(x1694,x1692,x1691))
% 66.30/66.35 [178]~P1(x1784)+~P8(x1782,x1784)+~P8(x1781,x1784)+E(x1781,x1782)+P8(x1783,x1784)+~P10(x1783,f27(x1784,x1782,x1781))
% 66.30/66.35 [181]~P7(x1812,x1815)+~P7(x1811,x1815)+~P2(x1814,x1815)+E(x1811,x1812)+P5(x1813,x1811,x1814,x1812)+~P15(x1815,x1813)
% 66.30/66.35 [162]P15(x1622,x1621)+~P15(x1622,x1623)+~P8(x1624,x1622)+~P7(x1624,x1623)+P15(x1621,x1622)+~P15(x1621,x1623)+~P8(x1624,x1621)
% 66.30/66.35 [177]P15(x1772,x1771)+P15(x1772,x1773)+P15(x1773,x1771)+P15(x1773,x1772)+~P15(x1772,x1774)+~P15(x1773,x1774)+~P7(x1775,x1772)+~P7(x1775,x1773)+P15(x1771,x1772)+P15(x1771,x1773)+~P15(x1771,x1774)+~P7(x1775,x1771)
% 66.30/66.35 %EqnAxiom
% 66.30/66.35 [1]E(x11,x11)
% 66.30/66.35 [2]E(x22,x21)+~E(x21,x22)
% 66.30/66.35 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 66.30/66.35 [4]~E(x41,x42)+E(f1(x41),f1(x42))
% 66.30/66.35 [5]~E(x51,x52)+E(f2(x51),f2(x52))
% 66.30/66.35 [6]~E(x61,x62)+E(f21(x61),f21(x62))
% 66.30/66.35 [7]~E(x71,x72)+E(f31(x71),f31(x72))
% 66.30/66.35 [8]~E(x81,x82)+E(f23(x81,x83,x84,x85,x86),f23(x82,x83,x84,x85,x86))
% 66.30/66.35 [9]~E(x91,x92)+E(f23(x93,x91,x94,x95,x96),f23(x93,x92,x94,x95,x96))
% 66.30/66.35 [10]~E(x101,x102)+E(f23(x103,x104,x101,x105,x106),f23(x103,x104,x102,x105,x106))
% 66.30/66.35 [11]~E(x111,x112)+E(f23(x113,x114,x115,x111,x116),f23(x113,x114,x115,x112,x116))
% 66.30/66.35 [12]~E(x121,x122)+E(f23(x123,x124,x125,x126,x121),f23(x123,x124,x125,x126,x122))
% 66.30/66.35 [13]~E(x131,x132)+E(f3(x131,x133),f3(x132,x133))
% 66.30/66.35 [14]~E(x141,x142)+E(f3(x143,x141),f3(x143,x142))
% 66.30/66.35 [15]~E(x151,x152)+E(f18(x151,x153,x154,x155),f18(x152,x153,x154,x155))
% 66.30/66.35 [16]~E(x161,x162)+E(f18(x163,x161,x164,x165),f18(x163,x162,x164,x165))
% 66.30/66.35 [17]~E(x171,x172)+E(f18(x173,x174,x171,x175),f18(x173,x174,x172,x175))
% 66.30/66.35 [18]~E(x181,x182)+E(f18(x183,x184,x185,x181),f18(x183,x184,x185,x182))
% 66.30/66.35 [19]~E(x191,x192)+E(f4(x191,x193),f4(x192,x193))
% 66.30/66.35 [20]~E(x201,x202)+E(f4(x203,x201),f4(x203,x202))
% 66.30/66.35 [21]~E(x211,x212)+E(f5(x211),f5(x212))
% 66.30/66.35 [22]~E(x221,x222)+E(f15(x221),f15(x222))
% 66.30/66.35 [23]~E(x231,x232)+E(f12(x231,x233,x234),f12(x232,x233,x234))
% 66.30/66.35 [24]~E(x241,x242)+E(f12(x243,x241,x244),f12(x243,x242,x244))
% 66.30/66.35 [25]~E(x251,x252)+E(f12(x253,x254,x251),f12(x253,x254,x252))
% 66.30/66.35 [26]~E(x261,x262)+E(f29(x261,x263),f29(x262,x263))
% 66.30/66.35 [27]~E(x271,x272)+E(f29(x273,x271),f29(x273,x272))
% 66.30/66.35 [28]~E(x281,x282)+E(f35(x281),f35(x282))
% 66.30/66.35 [29]~E(x291,x292)+E(f27(x291,x293,x294),f27(x292,x293,x294))
% 66.30/66.35 [30]~E(x301,x302)+E(f27(x303,x301,x304),f27(x303,x302,x304))
% 66.30/66.35 [31]~E(x311,x312)+E(f27(x313,x314,x311),f27(x313,x314,x312))
% 66.30/66.35 [32]~E(x321,x322)+E(f6(x321,x323),f6(x322,x323))
% 66.30/66.35 [33]~E(x331,x332)+E(f6(x333,x331),f6(x333,x332))
% 66.30/66.35 [34]~E(x341,x342)+E(f34(x341,x343),f34(x342,x343))
% 66.30/66.35 [35]~E(x351,x352)+E(f34(x353,x351),f34(x353,x352))
% 66.30/66.35 [36]~E(x361,x362)+E(f22(x361,x363,x364,x365),f22(x362,x363,x364,x365))
% 66.30/66.35 [37]~E(x371,x372)+E(f22(x373,x371,x374,x375),f22(x373,x372,x374,x375))
% 66.30/66.35 [38]~E(x381,x382)+E(f22(x383,x384,x381,x385),f22(x383,x384,x382,x385))
% 66.30/66.35 [39]~E(x391,x392)+E(f22(x393,x394,x395,x391),f22(x393,x394,x395,x392))
% 66.30/66.35 [40]~E(x401,x402)+E(f28(x401,x403),f28(x402,x403))
% 66.30/66.35 [41]~E(x411,x412)+E(f28(x413,x411),f28(x413,x412))
% 66.30/66.35 [42]~E(x421,x422)+E(f7(x421,x423),f7(x422,x423))
% 66.30/66.35 [43]~E(x431,x432)+E(f7(x433,x431),f7(x433,x432))
% 66.30/66.35 [44]~E(x441,x442)+E(f26(x441,x443),f26(x442,x443))
% 66.30/66.35 [45]~E(x451,x452)+E(f26(x453,x451),f26(x453,x452))
% 66.30/66.35 [46]~E(x461,x462)+E(f19(x461,x463),f19(x462,x463))
% 66.30/66.35 [47]~E(x471,x472)+E(f19(x473,x471),f19(x473,x472))
% 66.30/66.35 [48]~E(x481,x482)+E(f16(x481,x483),f16(x482,x483))
% 66.30/66.35 [49]~E(x491,x492)+E(f16(x493,x491),f16(x493,x492))
% 66.30/66.35 [50]~E(x501,x502)+E(f10(x501,x503),f10(x502,x503))
% 66.30/66.35 [51]~E(x511,x512)+E(f10(x513,x511),f10(x513,x512))
% 66.30/66.35 [52]~E(x521,x522)+E(f14(x521,x523,x524),f14(x522,x523,x524))
% 66.30/66.35 [53]~E(x531,x532)+E(f14(x533,x531,x534),f14(x533,x532,x534))
% 66.30/66.35 [54]~E(x541,x542)+E(f14(x543,x544,x541),f14(x543,x544,x542))
% 66.30/66.35 [55]~E(x551,x552)+E(f20(x551,x553),f20(x552,x553))
% 66.30/66.35 [56]~E(x561,x562)+E(f20(x563,x561),f20(x563,x562))
% 66.30/66.35 [57]~E(x571,x572)+E(f8(x571,x573),f8(x572,x573))
% 66.30/66.35 [58]~E(x581,x582)+E(f8(x583,x581),f8(x583,x582))
% 66.30/66.35 [59]~E(x591,x592)+E(f17(x591,x593),f17(x592,x593))
% 66.30/66.35 [60]~E(x601,x602)+E(f17(x603,x601),f17(x603,x602))
% 66.30/66.35 [61]~E(x611,x612)+E(f11(x611,x613),f11(x612,x613))
% 66.30/66.35 [62]~E(x621,x622)+E(f11(x623,x621),f11(x623,x622))
% 66.30/66.35 [63]~E(x631,x632)+E(f9(x631,x633),f9(x632,x633))
% 66.30/66.35 [64]~E(x641,x642)+E(f9(x643,x641),f9(x643,x642))
% 66.30/66.35 [65]~E(x651,x652)+E(f13(x651,x653),f13(x652,x653))
% 66.30/66.35 [66]~E(x661,x662)+E(f13(x663,x661),f13(x663,x662))
% 66.30/66.35 [67]~P1(x671)+P1(x672)+~E(x671,x672)
% 66.30/66.35 [68]P2(x682,x683)+~E(x681,x682)+~P2(x681,x683)
% 66.30/66.35 [69]P2(x693,x692)+~E(x691,x692)+~P2(x693,x691)
% 66.30/66.35 [70]P13(x702,x703)+~E(x701,x702)+~P13(x701,x703)
% 66.30/66.35 [71]P13(x713,x712)+~E(x711,x712)+~P13(x713,x711)
% 66.30/66.35 [72]P3(x722,x723,x724)+~E(x721,x722)+~P3(x721,x723,x724)
% 66.30/66.35 [73]P3(x733,x732,x734)+~E(x731,x732)+~P3(x733,x731,x734)
% 66.30/66.35 [74]P3(x743,x744,x742)+~E(x741,x742)+~P3(x743,x744,x741)
% 66.30/66.35 [75]P14(x752,x753,x754)+~E(x751,x752)+~P14(x751,x753,x754)
% 66.30/66.35 [76]P14(x763,x762,x764)+~E(x761,x762)+~P14(x763,x761,x764)
% 66.30/66.35 [77]P14(x773,x774,x772)+~E(x771,x772)+~P14(x773,x774,x771)
% 66.30/66.35 [78]P5(x782,x783,x784,x785)+~E(x781,x782)+~P5(x781,x783,x784,x785)
% 66.30/66.35 [79]P5(x793,x792,x794,x795)+~E(x791,x792)+~P5(x793,x791,x794,x795)
% 66.30/66.35 [80]P5(x803,x804,x802,x805)+~E(x801,x802)+~P5(x803,x804,x801,x805)
% 66.30/66.35 [81]P5(x813,x814,x815,x812)+~E(x811,x812)+~P5(x813,x814,x815,x811)
% 66.30/66.35 [82]~P11(x821)+P11(x822)+~E(x821,x822)
% 66.30/66.35 [83]~P4(x831)+P4(x832)+~E(x831,x832)
% 66.30/66.35 [84]P7(x842,x843)+~E(x841,x842)+~P7(x841,x843)
% 66.30/66.35 [85]P7(x853,x852)+~E(x851,x852)+~P7(x853,x851)
% 66.30/66.35 [86]P10(x862,x863)+~E(x861,x862)+~P10(x861,x863)
% 66.30/66.35 [87]P10(x873,x872)+~E(x871,x872)+~P10(x873,x871)
% 66.30/66.35 [88]P15(x882,x883)+~E(x881,x882)+~P15(x881,x883)
% 66.30/66.35 [89]P15(x893,x892)+~E(x891,x892)+~P15(x893,x891)
% 66.30/66.35 [90]P8(x902,x903)+~E(x901,x902)+~P8(x901,x903)
% 66.30/66.35 [91]P8(x913,x912)+~E(x911,x912)+~P8(x913,x911)
% 66.30/66.35 [92]P6(x922,x923,x924,x925)+~E(x921,x922)+~P6(x921,x923,x924,x925)
% 66.30/66.35 [93]P6(x933,x932,x934,x935)+~E(x931,x932)+~P6(x933,x931,x934,x935)
% 66.30/66.35 [94]P6(x943,x944,x942,x945)+~E(x941,x942)+~P6(x943,x944,x941,x945)
% 66.30/66.35 [95]P6(x953,x954,x955,x952)+~E(x951,x952)+~P6(x953,x954,x955,x951)
% 66.30/66.35 [96]P12(x962,x963,x964)+~E(x961,x962)+~P12(x961,x963,x964)
% 66.30/66.35 [97]P12(x973,x972,x974)+~E(x971,x972)+~P12(x973,x971,x974)
% 66.30/66.35 [98]P12(x983,x984,x982)+~E(x981,x982)+~P12(x983,x984,x981)
% 66.30/66.35 [99]P9(x992,x993)+~E(x991,x992)+~P9(x991,x993)
% 66.30/66.35 [100]P9(x1003,x1002)+~E(x1001,x1002)+~P9(x1003,x1001)
% 66.30/66.35
% 66.30/66.35 %-------------------------------------------
% 66.37/66.38 cnf(203,plain,
% 66.37/66.38 (~P10(x2031,x2032)+P8(x2031,f35(x2032))),
% 66.37/66.38 inference(equality_inference,[],[120])).
% 66.37/66.38 cnf(205,plain,
% 66.37/66.38 (~P8(x2051,x2052)+P8(x2051,f34(x2053,x2052))),
% 66.37/66.38 inference(equality_inference,[],[129])).
% 66.37/66.38 cnf(209,plain,
% 66.37/66.38 (~P5(x2092,x2091,x2093,x2091)),
% 66.37/66.38 inference(equality_inference,[],[183])).
% 66.37/66.38 cnf(210,plain,
% 66.37/66.38 (P11(f3(a30,a33))),
% 66.37/66.38 inference(scs_inference,[],[107,125])).
% 66.37/66.38 cnf(212,plain,
% 66.37/66.38 (P11(f3(a24,a32))),
% 66.37/66.38 inference(scs_inference,[],[107,125,126])).
% 66.37/66.38 cnf(214,plain,
% 66.37/66.38 (P10(a33,f31(a30))),
% 66.37/66.38 inference(scs_inference,[],[107,125,126,135])).
% 66.37/66.38 cnf(216,plain,
% 66.37/66.38 (~P6(x2161,x2162,x2163,x2162)),
% 66.37/66.38 inference(scs_inference,[],[107,209,125,126,135,199])).
% 66.37/66.38 cnf(224,plain,
% 66.37/66.38 (P14(x2241,a25,a32)+~E(f31(a24),x2241)),
% 66.37/66.38 inference(scs_inference,[],[104,105,107,209,125,126,135,199,186,72,73,74,75])).
% 66.37/66.38 cnf(225,plain,
% 66.37/66.38 (P14(f31(a24),x2251,a32)+~E(a25,x2251)),
% 66.37/66.38 inference(scs_inference,[],[104,105,107,209,125,126,135,199,186,72,73,74,75,76])).
% 66.37/66.38 cnf(226,plain,
% 66.37/66.38 (P14(f31(a24),a25,x2261)+~E(a32,x2261)),
% 66.37/66.38 inference(scs_inference,[],[104,105,107,209,125,126,135,199,186,72,73,74,75,76,77])).
% 66.37/66.38 cnf(233,plain,
% 66.37/66.38 (P10(a32,f31(a24))),
% 66.37/66.38 inference(scs_inference,[],[212,135])).
% 66.37/66.38 cnf(235,plain,
% 66.37/66.38 (~P14(f31(a30),a25,a33)),
% 66.37/66.38 inference(scs_inference,[],[106,212,216,135,187])).
% 66.37/66.38 cnf(238,plain,
% 66.37/66.38 (P10(x2381,f31(a30))+~E(a33,x2381)),
% 66.37/66.38 inference(scs_inference,[],[106,212,216,214,135,187,86])).
% 66.37/66.38 cnf(239,plain,
% 66.37/66.38 (P10(a33,x2391)+~E(f31(a30),x2391)),
% 66.37/66.38 inference(scs_inference,[],[106,212,216,214,135,187,86,87])).
% 66.37/66.38 cnf(240,plain,
% 66.37/66.38 (P2(x2401,x2402)+~E(f2(x2402),x2401)),
% 66.37/66.38 inference(scs_inference,[],[106,212,216,102,214,135,187,86,87,68])).
% 66.37/66.38 cnf(241,plain,
% 66.37/66.38 (P2(f2(x2411),x2412)+~E(x2411,x2412)),
% 66.37/66.38 inference(scs_inference,[],[106,212,216,102,214,135,187,86,87,68,69])).
% 66.37/66.38 cnf(242,plain,
% 66.37/66.38 (P13(x2421,x2422)+~E(f21(x2422),x2421)),
% 66.37/66.38 inference(scs_inference,[],[106,212,216,102,214,103,135,187,86,87,68,69,70])).
% 66.37/66.38 cnf(250,plain,
% 66.37/66.38 (P10(a32,x2501)+~E(f31(a24),x2501)),
% 66.37/66.38 inference(scs_inference,[],[233,87])).
% 66.37/66.38 cnf(251,plain,
% 66.37/66.38 (P14(x2511,a33,a25)+~E(f31(a30),x2511)),
% 66.37/66.38 inference(scs_inference,[],[106,233,87,75])).
% 66.37/66.38 cnf(252,plain,
% 66.37/66.38 (P14(f31(a30),a33,x2521)+~E(a25,x2521)),
% 66.37/66.38 inference(scs_inference,[],[106,233,87,75,77])).
% 66.37/66.38 cnf(253,plain,
% 66.37/66.38 (P14(f31(a30),x2531,a25)+~E(a33,x2531)),
% 66.37/66.38 inference(scs_inference,[],[106,233,87,75,77,76])).
% 66.37/66.38 cnf(254,plain,
% 66.37/66.38 (P10(x2541,f31(a24))+~E(a32,x2541)),
% 66.37/66.38 inference(scs_inference,[],[106,233,87,75,77,76,86])).
% 66.37/66.38 cnf(269,plain,
% 66.37/66.38 (~P7(x2691,x2692)+P7(f15(x2692),x2692)),
% 66.37/66.38 inference(scs_inference,[],[109,110])).
% 66.37/66.38 cnf(271,plain,
% 66.37/66.38 (E(x2711,f34(f17(f2(x2711),x2711),f8(f2(x2711),x2711)))),
% 66.37/66.38 inference(scs_inference,[],[102,2,149])).
% 66.37/66.38 cnf(272,plain,
% 66.37/66.38 (P14(f31(a24),f34(f17(f2(a25),a25),f8(f2(a25),a25)),a32)),
% 66.37/66.38 inference(scs_inference,[],[271,225])).
% 66.37/66.38 cnf(273,plain,
% 66.37/66.38 (E(x2731,f34(f17(f2(x2731),x2731),f8(f2(x2731),x2731)))),
% 66.37/66.38 inference(rename_variables,[],[271])).
% 66.37/66.38 cnf(274,plain,
% 66.37/66.38 (P14(f31(a24),a25,f34(f17(f2(a32),a32),f8(f2(a32),a32)))),
% 66.37/66.38 inference(scs_inference,[],[271,273,225,226])).
% 66.37/66.38 cnf(275,plain,
% 66.37/66.38 (E(x2751,f34(f17(f2(x2751),x2751),f8(f2(x2751),x2751)))),
% 66.37/66.38 inference(rename_variables,[],[271])).
% 66.37/66.38 cnf(276,plain,
% 66.37/66.38 (P14(f31(a30),a33,f34(f17(f2(a25),a25),f8(f2(a25),a25)))),
% 66.37/66.38 inference(scs_inference,[],[271,273,275,225,226,252])).
% 66.37/66.38 cnf(277,plain,
% 66.37/66.38 (E(x2771,f34(f17(f2(x2771),x2771),f8(f2(x2771),x2771)))),
% 66.37/66.38 inference(rename_variables,[],[271])).
% 66.37/66.38 cnf(278,plain,
% 66.37/66.38 (P14(f31(a30),f34(f17(f2(a33),a33),f8(f2(a33),a33)),a25)),
% 66.37/66.38 inference(scs_inference,[],[271,273,275,277,225,226,252,253])).
% 66.37/66.38 cnf(279,plain,
% 66.37/66.38 (E(x2791,f34(f17(f2(x2791),x2791),f8(f2(x2791),x2791)))),
% 66.37/66.38 inference(rename_variables,[],[271])).
% 66.37/66.38 cnf(281,plain,
% 66.37/66.38 (E(x2811,f34(f17(f2(x2811),x2811),f8(f2(x2811),x2811)))),
% 66.37/66.38 inference(rename_variables,[],[271])).
% 66.37/66.38 cnf(282,plain,
% 66.37/66.38 (P10(f34(f17(f2(a32),a32),f8(f2(a32),a32)),f31(a24))),
% 66.37/66.38 inference(scs_inference,[],[271,273,275,277,279,281,225,226,252,253,238,254])).
% 66.37/66.38 cnf(283,plain,
% 66.37/66.38 (E(x2831,f34(f17(f2(x2831),x2831),f8(f2(x2831),x2831)))),
% 66.37/66.38 inference(rename_variables,[],[271])).
% 66.37/66.38 cnf(284,plain,
% 66.37/66.38 (E(f34(f17(f2(x2841),x2841),f8(f2(x2841),x2841)),x2841)),
% 66.37/66.38 inference(scs_inference,[],[271,273,275,277,279,281,283,225,226,252,253,238,254,2])).
% 66.37/66.38 cnf(287,plain,
% 66.37/66.38 (P2(f2(x2871),f34(f17(f2(x2871),x2871),f8(f2(x2871),x2871)))),
% 66.37/66.38 inference(scs_inference,[],[271,273,275,277,279,281,283,225,226,252,253,238,254,2,183,241])).
% 66.37/66.38 cnf(312,plain,
% 66.37/66.38 (~P7(x3121,f1(x3122))+P10(x3121,x3122)),
% 66.37/66.38 inference(scs_inference,[],[113,123])).
% 66.37/66.38 cnf(317,plain,
% 66.37/66.38 (~P1(f34(f17(f2(x3171),x3171),f8(f2(x3171),x3171)))+P1(x3171)),
% 66.37/66.38 inference(scs_inference,[],[284,183,82,83,67])).
% 66.37/66.38 cnf(322,plain,
% 66.37/66.38 (~P4(x3221)+P4(f34(f17(f2(x3221),x3221),f8(f2(x3221),x3221)))),
% 66.37/66.38 inference(scs_inference,[],[271,83])).
% 66.37/66.38 cnf(374,plain,
% 66.37/66.38 (P8(f21(x3741),f1(x3741))),
% 66.37/66.38 inference(scs_inference,[],[103,115,118])).
% 66.37/66.38 cnf(375,plain,
% 66.37/66.38 (P10(f21(x3751),x3751)),
% 66.37/66.38 inference(scs_inference,[],[374,123])).
% 66.37/66.38 cnf(590,plain,
% 66.37/66.38 (P11(f4(f3(a30,a33),f3(a30,a33)))),
% 66.37/66.38 inference(scs_inference,[],[107,117,125])).
% 66.37/66.38 cnf(594,plain,
% 66.37/66.38 (E(x5941,f34(f17(f2(x5941),x5941),f8(f2(x5941),x5941)))),
% 66.37/66.38 inference(rename_variables,[],[271])).
% 66.37/66.38 cnf(596,plain,
% 66.37/66.38 (E(x5961,f34(f17(f2(x5961),x5961),f8(f2(x5961),x5961)))),
% 66.37/66.38 inference(rename_variables,[],[271])).
% 66.37/66.38 cnf(599,plain,
% 66.37/66.38 (~P14(f31(a30),a33,a33)),
% 66.37/66.38 inference(scs_inference,[],[590,271,594,596,179,73,72,74,193])).
% 66.37/66.38 cnf(603,plain,
% 66.37/66.38 (~P6(f31(a30),a33,a33,x6031)),
% 66.37/66.38 inference(scs_inference,[],[590,271,594,596,179,73,72,74,193,189,192])).
% 66.37/66.38 cnf(605,plain,
% 66.37/66.38 (~E(a25,a33)),
% 66.37/66.38 inference(scs_inference,[],[106,590,271,594,596,179,73,72,74,193,189,192,77])).
% 66.37/66.38 cnf(606,plain,
% 66.37/66.38 (~P13(a25,f31(a30))),
% 66.37/66.38 inference(scs_inference,[],[106,235,590,271,594,596,214,179,73,72,74,193,189,192,77,155])).
% 66.37/66.38 cnf(610,plain,
% 66.37/66.38 (~E(a25,f34(f17(f2(a33),a33),f8(f2(a33),a33)))),
% 66.37/66.38 inference(scs_inference,[],[106,235,590,271,594,596,284,214,179,73,72,74,193,189,192,77,155,111,3])).
% 66.37/66.38 cnf(617,plain,
% 66.37/66.38 (~E(f34(f17(f2(a25),a25),f8(f2(a25),a25)),a33)),
% 66.37/66.38 inference(scs_inference,[],[276,599,77])).
% 66.37/66.38 cnf(781,plain,
% 66.37/66.38 (~P12(x7811,x7812,x7813)+P8(x7811,f34(x7814,x7812))),
% 66.37/66.38 inference(scs_inference,[],[151,205])).
% 66.37/66.38 cnf(1014,plain,
% 66.37/66.38 (~P7(x10141,x10142)+~P2(f15(x10142),x10142)),
% 66.37/66.38 inference(scs_inference,[],[269,119])).
% 66.37/66.38 cnf(1138,plain,
% 66.37/66.38 (~E(f2(x11381),f15(x11381))+~P7(x11382,x11381)),
% 66.37/66.38 inference(scs_inference,[],[1014,240])).
% 66.37/66.38 cnf(1456,plain,
% 66.37/66.38 (P7(f6(f15(f1(x14561)),f1(x14561)),f1(x14561))),
% 66.37/66.38 inference(scs_inference,[],[101,134,110])).
% 66.37/66.38 cnf(1554,plain,
% 66.37/66.38 (~E(f15(f1(x15541)),f2(f1(x15541)))),
% 66.37/66.38 inference(scs_inference,[],[1456,1138,2])).
% 66.37/66.38 cnf(1648,plain,
% 66.37/66.38 (P8(f2(x16481),f34(x16482,f17(f2(x16481),x16481)))),
% 66.37/66.38 inference(scs_inference,[],[102,781,158])).
% 66.37/66.38 cnf(2937,plain,
% 66.37/66.38 (P11(x29371)+~P11(f4(x29372,f4(x29373,x29371)))),
% 66.37/66.38 inference(scs_inference,[],[171,125])).
% 66.37/66.38 cnf(2968,plain,
% 66.37/66.38 (~P11(f4(x29681,f4(x29682,f4(f3(a24,a25),f3(a30,a25)))))),
% 66.37/66.38 inference(scs_inference,[],[107,106,105,2937,193])).
% 66.37/66.38 cnf(3185,plain,
% 66.37/66.38 (~P1(f34(f17(f2(x31851),x31851),f8(f2(x31851),x31851)))+P7(f15(x31851),x31851)),
% 66.37/66.38 inference(scs_inference,[],[317,110])).
% 66.37/66.38 cnf(3216,plain,
% 66.37/66.38 (~P4(x32161)+~P7(x32162,f34(f17(f2(x32161),x32161),f8(f2(x32161),x32161)))),
% 66.37/66.38 inference(scs_inference,[],[322,112])).
% 66.37/66.38 cnf(3464,plain,
% 66.37/66.38 (~P4(f1(x34641))),
% 66.37/66.38 inference(scs_inference,[],[1456,271,3216,85])).
% 66.37/66.38 cnf(3988,plain,
% 66.37/66.38 (~P1(f34(f17(f2(x39881),x39881),f8(f2(x39881),x39881)))+~P4(x39881)),
% 66.37/66.38 inference(scs_inference,[],[3185,112])).
% 66.37/66.38 cnf(4019,plain,
% 66.37/66.38 (~P1(f34(f17(f2(x40191),x40191),f8(f2(x40191),x40191)))+P7(f5(x40191),x40191)),
% 66.37/66.38 inference(scs_inference,[],[3988,108])).
% 66.37/66.38 cnf(4173,plain,
% 66.37/66.38 (P8(f5(x41731),x41731)+~P1(f34(f17(f2(x41731),x41731),f8(f2(x41731),x41731)))),
% 66.37/66.38 inference(scs_inference,[],[4019,113])).
% 66.37/66.38 cnf(4204,plain,
% 66.37/66.38 (P8(f5(x42041),x42041)+~P7(x42042,f34(f17(f2(x42041),x42041),f8(f2(x42041),x42041)))),
% 66.37/66.38 inference(scs_inference,[],[4173,109])).
% 66.37/66.38 cnf(4351,plain,
% 66.37/66.38 (~P13(f34(f17(f2(a25),a25),f8(f2(a25),a25)),f31(a30))),
% 66.37/66.38 inference(scs_inference,[],[276,617,216,214,186,155])).
% 66.37/66.38 cnf(4422,plain,
% 66.37/66.38 (P8(f5(f1(x44221)),f1(x44221))),
% 66.37/66.38 inference(scs_inference,[],[1456,271,4204,85])).
% 66.37/66.38 cnf(4423,plain,
% 66.37/66.38 (P10(f5(f1(x44231)),x44231)),
% 66.37/66.38 inference(scs_inference,[],[4422,123])).
% 66.37/66.38 cnf(8018,plain,
% 66.37/66.38 (~P7(f2(x80181),x80181)),
% 66.37/66.38 inference(scs_inference,[],[102,119])).
% 66.37/66.38 cnf(8020,plain,
% 66.37/66.38 (~E(f6(f15(f1(x80201)),f1(x80201)),f2(f1(x80201)))),
% 66.37/66.38 inference(scs_inference,[],[102,1456,119,84])).
% 66.37/66.38 cnf(8045,plain,
% 66.37/66.38 (~P7(f2(x80451),f34(f17(f2(x80451),x80451),f8(f2(x80451),x80451)))),
% 66.37/66.38 inference(scs_inference,[],[287,119])).
% 66.37/66.38 cnf(8050,plain,
% 66.37/66.38 (~P7(f2(x80501),x80501)),
% 66.37/66.38 inference(rename_variables,[],[8018])).
% 66.37/66.38 cnf(8052,plain,
% 66.37/66.38 (~P8(f2(x80521),x80521)+~P12(x80522,f34(x80523,f17(f2(x80521),x80521)),x80521)),
% 66.37/66.38 inference(scs_inference,[],[1648,287,8018,8050,8020,119,111,164,163])).
% 66.37/66.38 cnf(8372,plain,
% 66.37/66.38 (P8(f2(x83721),x83721)),
% 66.37/66.38 inference(scs_inference,[],[102,114])).
% 66.37/66.38 cnf(8403,plain,
% 66.37/66.38 (P10(f2(f1(x84031)),x84031)),
% 66.37/66.38 inference(scs_inference,[],[8372,8052,123])).
% 66.37/66.38 cnf(8406,plain,
% 66.37/66.38 (~E(a33,a25)),
% 66.37/66.38 inference(scs_inference,[],[605,8372,8052,123,2])).
% 66.37/66.38 cnf(8407,plain,
% 66.37/66.38 (P8(f2(x84071),f34(f17(f2(x84071),x84071),f8(f2(x84071),x84071)))),
% 66.37/66.38 inference(scs_inference,[],[605,287,8372,8052,123,2,114])).
% 66.37/66.38 cnf(8628,plain,
% 66.37/66.38 (P8(f2(f1(x86281)),f35(x86281))),
% 66.37/66.38 inference(scs_inference,[],[8403,203])).
% 66.37/66.38 cnf(9276,plain,
% 66.37/66.38 (~P12(x92761,f35(x92762),f1(x92762))),
% 66.37/66.38 inference(scs_inference,[],[8628,8018,8372,163])).
% 66.37/66.38 cnf(9834,plain,
% 66.37/66.38 (~P10(a25,f31(a30))+~P9(a33,f31(a30))),
% 66.37/66.38 inference(scs_inference,[],[235,610,8406,1554,8403,155,182,154])).
% 66.37/66.38 cnf(9888,plain,
% 66.37/66.38 (~P9(a33,f31(a30))),
% 66.37/66.38 inference(scs_inference,[],[106,9834,152])).
% 66.37/66.38 cnf(10054,plain,
% 66.37/66.38 (P7(f5(f1(x100541)),f1(x100541))),
% 66.37/66.38 inference(scs_inference,[],[3464,108])).
% 66.37/66.38 cnf(10056,plain,
% 66.37/66.38 (P7(f15(f1(x100561)),f1(x100561))),
% 66.37/66.38 inference(scs_inference,[],[3464,101,108,110])).
% 66.37/66.38 cnf(10065,plain,
% 66.37/66.38 (P7(f6(f6(f15(f1(x100651)),f1(x100651)),f1(x100651)),f1(x100651))),
% 66.37/66.38 inference(scs_inference,[],[212,3464,4351,1456,101,108,110,117,242,1014,122,134])).
% 66.37/66.38 cnf(10070,plain,
% 66.37/66.38 (P11(f4(f3(a30,a33),f3(a24,a32)))),
% 66.37/66.38 inference(scs_inference,[],[212,4423,3464,4351,1456,107,101,108,110,117,242,1014,122,134,133,146])).
% 66.37/66.38 cnf(10073,plain,
% 66.37/66.38 (E(x100731,f34(f17(f2(x100731),x100731),f8(f2(x100731),x100731)))),
% 66.37/66.38 inference(rename_variables,[],[271])).
% 66.37/66.38 cnf(10075,plain,
% 66.37/66.38 (E(x100751,f34(f17(f2(x100751),x100751),f8(f2(x100751),x100751)))),
% 66.37/66.38 inference(rename_variables,[],[271])).
% 66.37/66.38 cnf(10077,plain,
% 66.37/66.38 (E(x100771,f34(f17(f2(x100771),x100771),f8(f2(x100771),x100771)))),
% 66.37/66.38 inference(rename_variables,[],[271])).
% 66.37/66.38 cnf(10082,plain,
% 66.37/66.38 (P11(f4(f3(a24,a25),f3(a30,a25)))),
% 66.37/66.38 inference(scs_inference,[],[104,210,212,4423,3464,4351,1456,271,10073,10075,102,107,101,108,110,117,242,1014,122,134,133,146,239,250,251,158,167,174])).
% 66.37/66.38 cnf(10085,plain,
% 66.37/66.38 (E(x100851,f34(f17(f2(x100851),x100851),f8(f2(x100851),x100851)))),
% 66.37/66.38 inference(rename_variables,[],[271])).
% 66.37/66.38 cnf(10096,plain,
% 66.37/66.38 (P10(a25,f31(a30))),
% 66.37/66.38 inference(scs_inference,[],[104,282,210,278,212,272,4423,3464,4351,1456,271,10073,10075,10077,102,107,101,108,110,117,242,1014,122,134,133,146,239,250,251,158,167,174,240,312,153,151,118,119,152])).
% 66.37/66.38 cnf(10101,plain,
% 66.37/66.38 (E(x101011,f34(f17(f2(x101011),x101011),f8(f2(x101011),x101011)))),
% 66.37/66.38 inference(rename_variables,[],[271])).
% 66.37/66.38 cnf(10103,plain,
% 66.37/66.38 (E(f34(f17(f2(x101031),x101031),f8(f2(x101031),x101031)),x101031)),
% 66.37/66.38 inference(rename_variables,[],[284])).
% 66.37/66.38 cnf(10105,plain,
% 66.37/66.38 (E(f34(f17(f2(x101051),x101051),f8(f2(x101051),x101051)),x101051)),
% 66.37/66.38 inference(rename_variables,[],[284])).
% 66.37/66.38 cnf(10108,plain,
% 66.37/66.38 (E(f34(f17(f2(x101081),x101081),f8(f2(x101081),x101081)),x101081)),
% 66.37/66.38 inference(rename_variables,[],[284])).
% 66.37/66.38 cnf(10110,plain,
% 66.37/66.38 (E(f34(f17(f2(x101101),x101101),f8(f2(x101101),x101101)),x101101)),
% 66.37/66.38 inference(rename_variables,[],[284])).
% 66.37/66.38 cnf(10116,plain,
% 66.37/66.38 (~P7(f2(x101161),f34(f17(f2(x101161),x101161),f8(f2(x101161),x101161)))),
% 66.37/66.38 inference(rename_variables,[],[8045])).
% 66.37/66.38 cnf(10122,plain,
% 66.37/66.38 (~P7(f2(x101221),x101221)),
% 66.37/66.38 inference(rename_variables,[],[8018])).
% 66.37/66.38 cnf(10125,plain,
% 66.37/66.38 (~P7(f2(x101251),x101251)),
% 66.37/66.38 inference(rename_variables,[],[8018])).
% 66.37/66.38 cnf(10136,plain,
% 66.37/66.38 (~P6(x101361,x101362,x101363,x101362)),
% 66.37/66.38 inference(rename_variables,[],[216])).
% 66.37/66.38 cnf(10138,plain,
% 66.37/66.38 (E(f34(f17(f2(x101381),x101381),f8(f2(x101381),x101381)),x101381)),
% 66.37/66.38 inference(rename_variables,[],[284])).
% 66.37/66.38 cnf(10140,plain,
% 66.37/66.38 (~P6(x101401,x101402,x101403,x101402)),
% 66.37/66.38 inference(rename_variables,[],[216])).
% 66.37/66.38 cnf(10142,plain,
% 66.37/66.38 (~P7(f2(x101421),x101421)),
% 66.37/66.38 inference(rename_variables,[],[8018])).
% 66.37/66.38 cnf(10145,plain,
% 66.37/66.38 (~P7(f2(x101451),x101451)),
% 66.37/66.38 inference(rename_variables,[],[8018])).
% 66.37/66.38 cnf(10148,plain,
% 66.37/66.38 (~P6(x101481,x101482,x101483,x101482)),
% 66.37/66.38 inference(rename_variables,[],[216])).
% 66.37/66.38 cnf(10151,plain,
% 66.37/66.38 (E(f34(f17(f2(x101511),x101511),f8(f2(x101511),x101511)),x101511)),
% 66.37/66.38 inference(rename_variables,[],[284])).
% 66.37/66.38 cnf(10157,plain,
% 66.37/66.38 (E(f34(f17(f2(x101571),x101571),f8(f2(x101571),x101571)),x101571)),
% 66.37/66.38 inference(rename_variables,[],[284])).
% 66.37/66.38 cnf(10159,plain,
% 66.37/66.38 (E(x101591,f34(f17(f2(x101591),x101591),f8(f2(x101591),x101591)))),
% 66.37/66.38 inference(rename_variables,[],[271])).
% 66.37/66.38 cnf(10161,plain,
% 66.37/66.38 (E(f34(f17(f2(x101611),x101611),f8(f2(x101611),x101611)),x101611)),
% 66.37/66.38 inference(rename_variables,[],[284])).
% 66.37/66.38 cnf(10163,plain,
% 66.37/66.38 (E(f34(f17(f2(x101631),x101631),f8(f2(x101631),x101631)),x101631)),
% 66.37/66.38 inference(rename_variables,[],[284])).
% 66.37/66.38 cnf(10177,plain,
% 66.37/66.38 (E(x101771,f34(f17(f2(x101771),x101771),f8(f2(x101771),x101771)))),
% 66.37/66.38 inference(rename_variables,[],[271])).
% 66.37/66.38 cnf(10182,plain,
% 66.37/66.38 (E(f34(f17(f2(x101821),x101821),f8(f2(x101821),x101821)),x101821)),
% 66.37/66.38 inference(rename_variables,[],[284])).
% 66.37/66.38 cnf(10187,plain,
% 66.37/66.38 (~P8(f2(f17(f2(x101871),x101871)),f8(f2(x101871),x101871))),
% 66.37/66.38 inference(scs_inference,[],[104,9276,9888,2968,282,210,278,212,8045,10116,272,8407,4423,3464,4351,606,216,10136,10140,10148,599,8018,10122,10125,10142,10145,8372,1456,271,10073,10075,10077,10085,10101,10159,10177,102,603,107,375,284,10103,10105,10108,10110,10138,10151,10157,10161,10163,10182,101,214,108,110,117,242,1014,122,134,133,146,239,250,251,158,167,174,240,312,153,151,118,119,152,150,224,99,120,97,98,131,132,138,139,140,141,142,143,165,166,93,94,95,160,161,186,76,82,187,77,67,75,84,154,155,127,144,113,114,89,100,129,83,71,130,164])).
% 66.37/66.38 cnf(10217,plain,
% 66.37/66.38 (P11(f4(f3(a30,a25),f3(a24,a25)))),
% 66.37/66.38 inference(scs_inference,[],[10096,10054,10056,10070,10082,10065,10187,274,117,113,153,118,312,134,122,146])).
% 66.37/66.38 cnf(11086,plain,
% 66.37/66.38 ($false),
% 66.37/66.38 inference(scs_inference,[],[105,10070,10217,106,193]),
% 66.37/66.38 ['proof']).
% 66.37/66.39 % SZS output end Proof
% 66.37/66.39 % Total time :65.660000s
%------------------------------------------------------------------------------