%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : GEO147-1 : TPTP v8.2.0. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% Computer : n020.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 105.62s 105.88s
% Output : CNFRefutation 105.77s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : GEO147-1 : TPTP v8.2.0. Released v2.4.0.
% 0.03/0.12 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% 0.12/0.34 % Computer : n020.cluster.edu
% 0.12/0.34 % Model : x86_64 x86_64
% 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.34 % Memory : 8042.1875MB
% 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.34 % CPULimit : 300
% 0.12/0.34 % WCLimit : 300
% 0.12/0.34 % DateTime : Fri Jun 21 06:55:54 EDT 2024
% 0.12/0.34 % CPUTime :
% 0.48/0.61 start to proof:theBenchmark
% 105.62/105.85 %-------------------------------------------
% 105.62/105.85 % File :CSE---1.7
% 105.62/105.85 % Problem :theBenchmark
% 105.62/105.85 % Transform :cnf
% 105.62/105.85 % Format :tptp:raw
% 105.62/105.85 % Command :java -jar mcs_scs.jar %d %s
% 105.62/105.85
% 105.62/105.85 % Result :Theorem 104.940000s
% 105.62/105.85 % Output :CNFRefutation 104.940000s
% 105.62/105.85 %-------------------------------------------
% 105.62/105.88 %--------------------------------------------------------------------------
% 105.62/105.88 % File : GEO147-1 : TPTP v8.2.0. Released v2.4.0.
% 105.62/105.88 % Domain : Geometry (Oriented curves)
% 105.62/105.88 % Problem : Meeting is possible only if there is a common position
% 105.62/105.88 % Version : [EHK99] axioms.
% 105.62/105.88 % English :
% 105.62/105.88
% 105.62/105.88 % Refs : [KE99] Kulik & Eschenbach (1999), A Geometry of Oriented Curv
% 105.62/105.88 % : [EHK99] Eschenbach et al. (1999), Representing Simple Trajecto
% 105.62/105.88 % Source : [TPTP]
% 105.62/105.88 % Names :
% 105.62/105.88
% 105.62/105.88 % Status : Unsatisfiable
% 105.62/105.88 % Rating : 0.05 v7.4.0, 0.06 v7.3.0, 0.00 v7.0.0, 0.13 v6.4.0, 0.07 v6.3.0, 0.09 v6.2.0, 0.10 v6.1.0, 0.07 v6.0.0, 0.10 v5.5.0, 0.20 v5.3.0, 0.22 v5.2.0, 0.19 v5.1.0, 0.24 v5.0.0, 0.14 v4.1.0, 0.23 v4.0.1, 0.27 v3.7.0, 0.00 v3.5.0, 0.09 v3.4.0, 0.17 v3.3.0, 0.14 v3.2.0, 0.15 v3.1.0, 0.09 v2.7.0, 0.17 v2.6.0, 0.11 v2.5.0, 0.00 v2.4.0
% 105.62/105.88 % Syntax : Number of clauses : 112 ( 5 unt; 42 nHn; 100 RR)
% 105.62/105.88 % Number of literals : 331 ( 41 equ; 170 neg)
% 105.62/105.88 % Maximal clause size : 12 ( 2 avg)
% 105.62/105.88 % Maximal term depth : 4 ( 1 avg)
% 105.62/105.88 % Number of predicates : 16 ( 15 usr; 0 prp; 1-4 aty)
% 105.62/105.88 % Number of functors : 34 ( 34 usr; 3 con; 0-5 aty)
% 105.62/105.88 % Number of variables : 310 ( 19 sgn)
% 105.62/105.88 % SPC : CNF_UNS_RFO_SEQ_NHN
% 105.62/105.88
% 105.62/105.88 % Comments : Created by tptp2X -f tptp -t clausify:otter GEO147+1.p
% 105.62/105.88 %--------------------------------------------------------------------------
% 105.62/105.88 %----Include simple curve axioms
% 105.62/105.88 include('Axioms/GEO004-0.ax').
% 105.62/105.88 %----Include axioms of betweenness for simple curves
% 105.62/105.88 include('Axioms/GEO004-1.ax').
% 105.62/105.88 %----Include oriented curve axioms
% 105.62/105.88 include('Axioms/GEO004-2.ax').
% 105.62/105.88 %----Include trajectory axioms
% 105.62/105.88 include('Axioms/GEO004-3.ax').
% 105.62/105.88 %--------------------------------------------------------------------------
% 105.62/105.88 cnf(t13_156,negated_conjecture,
% 105.62/105.88 connect(sk28,sk29,sk27) ).
% 105.62/105.88
% 105.62/105.88 cnf(t13_157,negated_conjecture,
% 105.62/105.88 ( ~ incident_o(sk27,trajectory_of(sk28))
% 105.62/105.88 | ~ incident_o(sk27,trajectory_of(sk29)) ) ).
% 105.62/105.88
% 105.62/105.88 %--------------------------------------------------------------------------
% 105.62/105.88 %-------------------------------------------
% 105.62/105.88 % Proof found
% 105.62/105.88 % SZS status Theorem for theBenchmark
% 105.62/105.88 % SZS output start Proof
% 105.68/105.90 %ClaNum:200(EqnAxiom:100)
% 105.68/105.91 %VarNum:767(SingletonVarNum:276)
% 105.68/105.91 %MaxLitNum:12
% 105.68/105.91 %MaxfuncDepth:3
% 105.68/105.91 %SharedTerms:8
% 105.68/105.91 %goalClause: 104 121
% 105.68/105.91 %singleGoalClaCount:1
% 105.68/105.91 [104]P3(a24,a30,a25)
% 105.68/105.91 [101]P1(f1(x1011))
% 105.68/105.91 [102]P2(f2(x1021),x1021)
% 105.68/105.91 [103]P13(f21(x1031),x1031)
% 105.68/105.91 [121]~P10(a25,f32(a24))+~P10(a25,f32(a30))
% 105.68/105.91 [105]P4(x1051)+P7(f3(x1051),x1051)
% 105.68/105.91 [107]~P1(x1071)+P7(f15(x1071),x1071)
% 105.68/105.91 [114]~P11(x1141)+P11(f4(x1141,x1141))
% 105.68/105.91 [106]P1(x1061)+~P7(x1062,x1061)
% 105.68/105.91 [109]~P4(x1091)+~P7(x1092,x1091)
% 105.68/105.91 [110]~P7(x1101,x1102)+P8(x1101,x1102)
% 105.68/105.91 [111]~P2(x1111,x1112)+P8(x1111,x1112)
% 105.68/105.91 [112]~P13(x1121,x1122)+P10(x1121,x1122)
% 105.68/105.91 [113]~P9(x1131,x1132)+P10(x1131,x1132)
% 105.68/105.91 [116]~P2(x1161,x1162)+~P7(x1161,x1162)
% 105.68/105.91 [115]~P10(x1151,x1152)+P8(x1151,f1(x1152))
% 105.68/105.91 [119]~P7(x1191,x1192)+~E(f6(x1191,x1192),x1191)
% 105.68/105.91 [120]P10(x1201,x1202)+~P8(x1201,f1(x1202))
% 105.68/105.91 [123]P11(x1231)+~P11(f4(x1232,x1231))
% 105.68/105.91 [124]P11(x1241)+~P11(f4(x1241,x1242))
% 105.68/105.91 [125]P14(x1251,x1252)+P8(f7(x1251,x1252),x1251)
% 105.68/105.91 [131]~P10(x1312,f32(x1311))+P11(f5(x1311,x1312))
% 105.68/105.91 [132]~P7(x1321,x1322)+P7(f6(x1321,x1322),x1322)
% 105.68/105.91 [133]P10(x1331,f32(x1332))+~P11(f5(x1332,x1331))
% 105.68/105.91 [142]P14(x1421,x1422)+~P8(f7(x1421,x1422),x1422)
% 105.68/105.91 [144]~P11(f4(x1442,x1441))+P11(f4(x1441,x1442))
% 105.68/105.91 [156]~P2(x1561,x1562)+P12(x1561,f17(x1561,x1562),f8(x1561,x1562))
% 105.68/105.91 [147]~P2(x1471,x1472)+E(f33(f17(x1471,x1472),f8(x1471,x1472)),x1472)
% 105.68/105.91 [165]~P11(x1651)+P11(f4(x1651,f5(x1652,f26(x1652,x1651))))
% 105.68/105.91 [148]P8(x1481,x1482)+~P12(x1481,x1483,x1482)
% 105.68/105.91 [149]P8(x1491,x1492)+~P12(x1491,x1492,x1493)
% 105.68/105.91 [150]P10(x1501,x1502)+~P15(x1502,x1503,x1501)
% 105.68/105.91 [151]P10(x1511,x1512)+~P15(x1512,x1511,x1513)
% 105.68/105.91 [154]~P12(x1543,x1542,x1541)+E(f11(x1541,x1542),f33(x1542,x1541))
% 105.68/105.91 [168]~P11(f4(f4(x1681,x1682),x1683))+P11(f4(x1681,f4(x1682,x1683)))
% 105.68/105.91 [169]~P11(f4(x1691,f4(x1692,x1693)))+P11(f4(f4(x1691,x1692),x1693))
% 105.68/105.91 [172]~P3(x1721,x1723,x1722)+P11(f4(f5(x1721,x1722),f5(x1723,x1722)))
% 105.68/105.91 [177]P3(x1771,x1772,x1773)+~P11(f4(f5(x1771,x1773),f5(x1772,x1773)))
% 105.68/105.91 [181]~E(x1811,x1812)+~P5(x1813,x1811,x1814,x1812)
% 105.68/105.91 [192]~P5(x1924,x1923,x1922,x1921)+P7(x1921,f18(x1921,x1922,x1923,x1924))
% 105.68/105.91 [193]~P5(x1934,x1931,x1933,x1932)+P7(x1931,f18(x1932,x1933,x1931,x1934))
% 105.68/105.91 [194]~P5(x1944,x1943,x1941,x1942)+P2(x1941,f18(x1942,x1941,x1943,x1944))
% 105.68/105.91 [195]~P5(x1954,x1953,x1952,x1951)+P14(f18(x1951,x1952,x1953,x1954),x1954)
% 105.68/105.91 [197]~P6(x1971,x1974,x1973,x1972)+P5(f22(x1971,x1972,x1973,x1974),x1974,x1973,x1972)
% 105.68/105.91 [108]P1(x1081)+~P14(x1081,x1082)+E(x1081,x1082)
% 105.68/105.91 [122]P2(x1221,x1222)+~P8(x1221,x1222)+P7(x1221,x1222)
% 105.68/105.91 [129]~P10(x1291,x1292)+P13(x1291,x1292)+~E(f16(x1292,x1291),x1291)
% 105.68/105.91 [130]~P10(x1301,x1302)+P9(x1301,x1302)+~E(f19(x1302,x1301),x1301)
% 105.68/105.91 [136]~P8(x1361,x1362)+P7(x1361,x1362)+P8(x1361,f9(x1362,x1361))
% 105.68/105.91 [137]~P8(x1371,x1372)+P7(x1371,x1372)+P8(x1371,f13(x1372,x1371))
% 105.68/105.91 [138]~P8(x1381,x1382)+P7(x1381,x1382)+P14(f9(x1382,x1381),x1382)
% 105.68/105.91 [139]~P8(x1391,x1392)+P7(x1391,x1392)+P14(f13(x1392,x1391),x1392)
% 105.68/105.91 [140]~P10(x1401,x1402)+P13(x1401,x1402)+P10(f16(x1402,x1401),x1402)
% 105.68/105.91 [141]~P10(x1411,x1412)+P9(x1411,x1412)+P10(f19(x1412,x1411),x1412)
% 105.68/105.91 [145]E(x1451,x1452)+P8(f10(x1451,x1452),x1452)+P8(f10(x1451,x1452),x1451)
% 105.68/105.91 [146]P8(f20(x1462,x1461),x1461)+P10(f20(x1462,x1461),x1462)+E(x1461,f31(x1462))
% 105.68/105.91 [155]E(x1551,x1552)+~P8(f10(x1551,x1552),x1552)+~P8(f10(x1551,x1552),x1551)
% 105.68/105.91 [157]~P8(f20(x1572,x1571),x1571)+~P10(f20(x1572,x1571),x1572)+E(x1571,f31(x1572))
% 105.68/105.91 [158]~P8(x1581,x1582)+P7(x1581,x1582)+~P14(f9(x1582,x1581),f13(x1582,x1581))
% 105.68/105.91 [159]~P8(x1591,x1592)+P7(x1591,x1592)+~P14(f13(x1592,x1591),f9(x1592,x1591))
% 105.68/105.91 [163]~P10(x1631,x1632)+P13(x1631,x1632)+~P15(x1632,x1631,f16(x1632,x1631))
% 105.68/105.91 [164]~P10(x1641,x1642)+P9(x1641,x1642)+~P15(x1642,f19(x1642,x1641),x1641)
% 105.68/105.91 [170]E(x1701,x1702)+P15(x1702,f28(x1702,x1701),f29(x1702,x1701))+P15(x1701,f28(x1702,x1701),f29(x1702,x1701))
% 105.68/105.91 [178]E(x1781,x1782)+~P15(x1782,f28(x1781,x1782),f29(x1781,x1782))+~P15(x1781,f28(x1781,x1782),f29(x1781,x1782))
% 105.68/105.91 [126]~P8(x1261,x1263)+P8(x1261,x1262)+~P14(x1263,x1262)
% 105.68/105.91 [117]~P10(x1171,x1173)+P8(x1171,x1172)+~E(x1172,f31(x1173))
% 105.68/105.91 [118]~P8(x1181,x1183)+P10(x1181,x1182)+~E(x1183,f31(x1182))
% 105.68/105.91 [182]~P8(f12(x1823,x1822,x1821),x1821)+~P8(f12(x1823,x1822,x1821),x1822)+E(x1821,f33(x1822,x1823))
% 105.68/105.91 [183]~P8(f12(x1833,x1832,x1831),x1831)+~P8(f12(x1833,x1832,x1831),x1833)+E(x1831,f33(x1832,x1833))
% 105.68/105.91 [184]~P15(x1841,x1843,x1842)+~P15(x1841,x1844,x1843)+P6(x1841,x1842,x1843,x1844)
% 105.68/105.91 [185]~P15(x1851,x1853,x1854)+~P15(x1851,x1852,x1853)+P6(x1851,x1852,x1853,x1854)
% 105.68/105.91 [187]P15(x1871,x1873,x1872)+P15(x1871,x1872,x1873)+~P6(x1871,x1874,x1873,x1872)
% 105.68/105.91 [188]~P6(x1881,x1884,x1883,x1882)+P15(x1881,x1882,x1883)+P15(x1881,x1884,x1883)
% 105.68/105.91 [189]~P6(x1891,x1894,x1892,x1893)+P15(x1891,x1892,x1893)+P15(x1891,x1892,x1894)
% 105.68/105.91 [190]P15(x1901,x1903,x1902)+P15(x1901,x1902,x1903)+~P6(x1901,x1903,x1902,x1904)
% 105.68/105.91 [127]~P8(x1271,x1274)+P8(x1271,x1272)+~E(x1272,f33(x1273,x1274))
% 105.68/105.91 [128]~P8(x1281,x1283)+P8(x1281,x1282)+~E(x1282,f33(x1283,x1284))
% 105.68/105.91 [196]~P10(x1961,x1962)+~P6(x1962,x1965,x1964,x1963)+P8(x1961,f22(x1962,x1963,x1964,x1965))
% 105.68/105.91 [198]P10(x1981,x1982)+~P6(x1982,x1983,x1984,x1985)+~P8(x1981,f22(x1982,x1985,x1984,x1983))
% 105.68/105.91 [152]~P10(x1522,x1523)+~P9(x1521,x1523)+E(x1521,x1522)+P15(x1523,x1522,x1521)
% 105.68/105.91 [153]~P13(x1531,x1533)+~P10(x1532,x1533)+E(x1531,x1532)+P15(x1533,x1531,x1532)
% 105.68/105.91 [173]~P8(x1731,x1733)+~P8(x1731,x1732)+P12(x1731,x1732,x1733)+P8(f14(x1733,x1732,x1731),x1733)
% 105.68/105.91 [174]~P8(x1741,x1743)+~P8(x1741,x1742)+P12(x1741,x1742,x1743)+P8(f14(x1743,x1742,x1741),x1742)
% 105.68/105.91 [180]P8(f12(x1803,x1802,x1801),x1801)+P8(f12(x1803,x1802,x1801),x1802)+P8(f12(x1803,x1802,x1801),x1803)+E(x1801,f33(x1802,x1803))
% 105.68/105.91 [161]~P8(x1611,x1612)+P7(x1611,x1612)+~P12(x1614,x1613,x1612)+~P8(x1611,x1613)
% 105.68/105.91 [162]~P8(x1621,x1622)+P7(x1621,x1622)+~P12(x1624,x1622,x1623)+~P8(x1621,x1623)
% 105.68/105.91 [135]~P8(x1351,x1354)+P8(x1351,x1352)+P8(x1351,x1353)+~E(x1354,f33(x1353,x1352))
% 105.68/105.91 [199]~P5(x1995,x1992,x1993,x1994)+P6(x1991,x1992,x1993,x1994)+P8(f23(x1995,x1991,x1994,x1993,x1992),x1995)+P10(f23(x1995,x1991,x1994,x1993,x1992),x1991)
% 105.68/105.91 [200]P6(x2001,x2002,x2003,x2004)+~P5(x2005,x2002,x2003,x2004)+~P8(f23(x2005,x2001,x2004,x2003,x2002),x2005)+~P10(f23(x2005,x2001,x2004,x2003,x2002),x2001)
% 105.68/105.91 [191]~P15(f32(x1911),x1912,x1913)+~P15(f32(x1914),x1915,x1916)+~P11(f4(f5(x1914,x1916),f5(x1911,x1912)))+~P11(f4(f5(x1914,x1915),f5(x1911,x1913)))
% 105.68/105.91 [171]~P1(x1713)+~P8(x1712,x1713)+~P8(x1711,x1713)+E(x1711,x1712)+P15(f27(x1713,x1712,x1711),x1711,x1712)
% 105.68/105.91 [186]~P8(x1861,x1863)+~P8(x1861,x1862)+P12(x1861,x1862,x1863)+~P7(f14(x1863,x1862,x1861),x1863)+~P7(f14(x1863,x1862,x1861),x1862)
% 105.68/105.91 [166]~P4(x1664)+~P7(x1661,x1662)+P12(x1661,x1662,x1663)+~P12(x1665,x1662,x1663)+~E(x1664,f33(x1662,x1663))
% 105.68/105.91 [134]E(x1343,x1341)+~P7(x1341,x1344)+~P7(x1343,x1344)+E(x1341,x1342)+E(x1343,x1342)+~P7(x1342,x1344)
% 105.68/105.91 [167]~P1(x1674)+~P8(x1673,x1674)+~P8(x1672,x1674)+~P8(x1671,x1674)+E(x1671,x1672)+P10(x1673,f27(x1674,x1672,x1671))
% 105.68/105.91 [176]~P1(x1764)+~P8(x1762,x1764)+~P8(x1761,x1764)+E(x1761,x1762)+P8(x1763,x1764)+~P10(x1763,f27(x1764,x1762,x1761))
% 105.68/105.91 [179]~P7(x1792,x1795)+~P7(x1791,x1795)+~P2(x1794,x1795)+E(x1791,x1792)+P5(x1793,x1791,x1794,x1792)+~P14(x1795,x1793)
% 105.68/105.91 [160]P14(x1602,x1601)+~P14(x1602,x1603)+~P8(x1604,x1602)+~P7(x1604,x1603)+P14(x1601,x1602)+~P14(x1601,x1603)+~P8(x1604,x1601)
% 105.68/105.91 [175]P14(x1752,x1751)+P14(x1752,x1753)+P14(x1753,x1751)+P14(x1753,x1752)+~P14(x1752,x1754)+~P14(x1753,x1754)+~P7(x1755,x1752)+~P7(x1755,x1753)+P14(x1751,x1752)+P14(x1751,x1753)+~P14(x1751,x1754)+~P7(x1755,x1751)
% 105.68/105.91 %EqnAxiom
% 105.68/105.91 [1]E(x11,x11)
% 105.68/105.91 [2]E(x22,x21)+~E(x21,x22)
% 105.68/105.91 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 105.68/105.91 [4]~E(x41,x42)+E(f1(x41),f1(x42))
% 105.68/105.91 [5]~E(x51,x52)+E(f2(x51),f2(x52))
% 105.68/105.91 [6]~E(x61,x62)+E(f21(x61),f21(x62))
% 105.68/105.91 [7]~E(x71,x72)+E(f3(x71),f3(x72))
% 105.68/105.91 [8]~E(x81,x82)+E(f15(x81),f15(x82))
% 105.68/105.91 [9]~E(x91,x92)+E(f4(x91,x93),f4(x92,x93))
% 105.68/105.91 [10]~E(x101,x102)+E(f4(x103,x101),f4(x103,x102))
% 105.68/105.91 [11]~E(x111,x112)+E(f23(x111,x113,x114,x115,x116),f23(x112,x113,x114,x115,x116))
% 105.68/105.91 [12]~E(x121,x122)+E(f23(x123,x121,x124,x125,x126),f23(x123,x122,x124,x125,x126))
% 105.68/105.91 [13]~E(x131,x132)+E(f23(x133,x134,x131,x135,x136),f23(x133,x134,x132,x135,x136))
% 105.68/105.91 [14]~E(x141,x142)+E(f23(x143,x144,x145,x141,x146),f23(x143,x144,x145,x142,x146))
% 105.68/105.91 [15]~E(x151,x152)+E(f23(x153,x154,x155,x156,x151),f23(x153,x154,x155,x156,x152))
% 105.68/105.91 [16]~E(x161,x162)+E(f31(x161),f31(x162))
% 105.68/105.91 [17]~E(x171,x172)+E(f12(x171,x173,x174),f12(x172,x173,x174))
% 105.68/105.91 [18]~E(x181,x182)+E(f12(x183,x181,x184),f12(x183,x182,x184))
% 105.68/105.91 [19]~E(x191,x192)+E(f12(x193,x194,x191),f12(x193,x194,x192))
% 105.68/105.91 [20]~E(x201,x202)+E(f6(x201,x203),f6(x202,x203))
% 105.68/105.91 [21]~E(x211,x212)+E(f6(x213,x211),f6(x213,x212))
% 105.68/105.91 [22]~E(x221,x222)+E(f33(x221,x223),f33(x222,x223))
% 105.68/105.91 [23]~E(x231,x232)+E(f33(x233,x231),f33(x233,x232))
% 105.68/105.91 [24]~E(x241,x242)+E(f32(x241),f32(x242))
% 105.68/105.91 [25]~E(x251,x252)+E(f5(x251,x253),f5(x252,x253))
% 105.68/105.91 [26]~E(x261,x262)+E(f5(x263,x261),f5(x263,x262))
% 105.68/105.91 [27]~E(x271,x272)+E(f29(x271,x273),f29(x272,x273))
% 105.68/105.91 [28]~E(x281,x282)+E(f29(x283,x281),f29(x283,x282))
% 105.68/105.91 [29]~E(x291,x292)+E(f28(x291,x293),f28(x292,x293))
% 105.68/105.91 [30]~E(x301,x302)+E(f28(x303,x301),f28(x303,x302))
% 105.68/105.91 [31]~E(x311,x312)+E(f7(x311,x313),f7(x312,x313))
% 105.68/105.91 [32]~E(x321,x322)+E(f7(x323,x321),f7(x323,x322))
% 105.68/105.91 [33]~E(x331,x332)+E(f14(x331,x333,x334),f14(x332,x333,x334))
% 105.68/105.91 [34]~E(x341,x342)+E(f14(x343,x341,x344),f14(x343,x342,x344))
% 105.68/105.91 [35]~E(x351,x352)+E(f14(x353,x354,x351),f14(x353,x354,x352))
% 105.68/105.91 [36]~E(x361,x362)+E(f27(x361,x363,x364),f27(x362,x363,x364))
% 105.68/105.91 [37]~E(x371,x372)+E(f27(x373,x371,x374),f27(x373,x372,x374))
% 105.68/105.91 [38]~E(x381,x382)+E(f27(x383,x384,x381),f27(x383,x384,x382))
% 105.68/105.91 [39]~E(x391,x392)+E(f16(x391,x393),f16(x392,x393))
% 105.68/105.91 [40]~E(x401,x402)+E(f16(x403,x401),f16(x403,x402))
% 105.68/105.91 [41]~E(x411,x412)+E(f19(x411,x413),f19(x412,x413))
% 105.68/105.91 [42]~E(x421,x422)+E(f19(x423,x421),f19(x423,x422))
% 105.68/105.91 [43]~E(x431,x432)+E(f18(x431,x433,x434,x435),f18(x432,x433,x434,x435))
% 105.68/105.91 [44]~E(x441,x442)+E(f18(x443,x441,x444,x445),f18(x443,x442,x444,x445))
% 105.68/105.91 [45]~E(x451,x452)+E(f18(x453,x454,x451,x455),f18(x453,x454,x452,x455))
% 105.68/105.91 [46]~E(x461,x462)+E(f18(x463,x464,x465,x461),f18(x463,x464,x465,x462))
% 105.68/105.91 [47]~E(x471,x472)+E(f26(x471,x473),f26(x472,x473))
% 105.68/105.91 [48]~E(x481,x482)+E(f26(x483,x481),f26(x483,x482))
% 105.68/105.91 [49]~E(x491,x492)+E(f9(x491,x493),f9(x492,x493))
% 105.68/105.91 [50]~E(x501,x502)+E(f9(x503,x501),f9(x503,x502))
% 105.68/105.91 [51]~E(x511,x512)+E(f11(x511,x513),f11(x512,x513))
% 105.68/105.91 [52]~E(x521,x522)+E(f11(x523,x521),f11(x523,x522))
% 105.68/105.91 [53]~E(x531,x532)+E(f10(x531,x533),f10(x532,x533))
% 105.68/105.91 [54]~E(x541,x542)+E(f10(x543,x541),f10(x543,x542))
% 105.68/105.91 [55]~E(x551,x552)+E(f17(x551,x553),f17(x552,x553))
% 105.68/105.91 [56]~E(x561,x562)+E(f17(x563,x561),f17(x563,x562))
% 105.68/105.91 [57]~E(x571,x572)+E(f20(x571,x573),f20(x572,x573))
% 105.68/105.91 [58]~E(x581,x582)+E(f20(x583,x581),f20(x583,x582))
% 105.68/105.91 [59]~E(x591,x592)+E(f13(x591,x593),f13(x592,x593))
% 105.68/105.91 [60]~E(x601,x602)+E(f13(x603,x601),f13(x603,x602))
% 105.68/105.91 [61]~E(x611,x612)+E(f8(x611,x613),f8(x612,x613))
% 105.68/105.91 [62]~E(x621,x622)+E(f8(x623,x621),f8(x623,x622))
% 105.68/105.91 [63]~E(x631,x632)+E(f22(x631,x633,x634,x635),f22(x632,x633,x634,x635))
% 105.68/105.91 [64]~E(x641,x642)+E(f22(x643,x641,x644,x645),f22(x643,x642,x644,x645))
% 105.68/105.91 [65]~E(x651,x652)+E(f22(x653,x654,x651,x655),f22(x653,x654,x652,x655))
% 105.68/105.91 [66]~E(x661,x662)+E(f22(x663,x664,x665,x661),f22(x663,x664,x665,x662))
% 105.68/105.91 [67]~P1(x671)+P1(x672)+~E(x671,x672)
% 105.68/105.91 [68]P2(x682,x683)+~E(x681,x682)+~P2(x681,x683)
% 105.68/105.91 [69]P2(x693,x692)+~E(x691,x692)+~P2(x693,x691)
% 105.68/105.91 [70]P13(x702,x703)+~E(x701,x702)+~P13(x701,x703)
% 105.68/105.91 [71]P13(x713,x712)+~E(x711,x712)+~P13(x713,x711)
% 105.68/105.91 [72]P3(x722,x723,x724)+~E(x721,x722)+~P3(x721,x723,x724)
% 105.68/105.91 [73]P3(x733,x732,x734)+~E(x731,x732)+~P3(x733,x731,x734)
% 105.68/105.91 [74]P3(x743,x744,x742)+~E(x741,x742)+~P3(x743,x744,x741)
% 105.68/105.91 [75]~P4(x751)+P4(x752)+~E(x751,x752)
% 105.68/105.91 [76]P7(x762,x763)+~E(x761,x762)+~P7(x761,x763)
% 105.68/105.91 [77]P7(x773,x772)+~E(x771,x772)+~P7(x773,x771)
% 105.68/105.91 [78]P10(x782,x783)+~E(x781,x782)+~P10(x781,x783)
% 105.68/105.91 [79]P10(x793,x792)+~E(x791,x792)+~P10(x793,x791)
% 105.68/105.91 [80]P5(x802,x803,x804,x805)+~E(x801,x802)+~P5(x801,x803,x804,x805)
% 105.68/105.91 [81]P5(x813,x812,x814,x815)+~E(x811,x812)+~P5(x813,x811,x814,x815)
% 105.68/105.91 [82]P5(x823,x824,x822,x825)+~E(x821,x822)+~P5(x823,x824,x821,x825)
% 105.68/105.91 [83]P5(x833,x834,x835,x832)+~E(x831,x832)+~P5(x833,x834,x835,x831)
% 105.68/105.91 [84]~P11(x841)+P11(x842)+~E(x841,x842)
% 105.68/105.91 [85]P8(x852,x853)+~E(x851,x852)+~P8(x851,x853)
% 105.68/105.91 [86]P8(x863,x862)+~E(x861,x862)+~P8(x863,x861)
% 105.68/105.91 [87]P14(x872,x873)+~E(x871,x872)+~P14(x871,x873)
% 105.68/105.91 [88]P14(x883,x882)+~E(x881,x882)+~P14(x883,x881)
% 105.68/105.91 [89]P9(x892,x893)+~E(x891,x892)+~P9(x891,x893)
% 105.68/105.91 [90]P9(x903,x902)+~E(x901,x902)+~P9(x903,x901)
% 105.68/105.91 [91]P15(x912,x913,x914)+~E(x911,x912)+~P15(x911,x913,x914)
% 105.68/105.91 [92]P15(x923,x922,x924)+~E(x921,x922)+~P15(x923,x921,x924)
% 105.68/105.91 [93]P15(x933,x934,x932)+~E(x931,x932)+~P15(x933,x934,x931)
% 105.68/105.91 [94]P6(x942,x943,x944,x945)+~E(x941,x942)+~P6(x941,x943,x944,x945)
% 105.68/105.91 [95]P6(x953,x952,x954,x955)+~E(x951,x952)+~P6(x953,x951,x954,x955)
% 105.68/105.91 [96]P6(x963,x964,x962,x965)+~E(x961,x962)+~P6(x963,x964,x961,x965)
% 105.68/105.91 [97]P6(x973,x974,x975,x972)+~E(x971,x972)+~P6(x973,x974,x975,x971)
% 105.68/105.91 [98]P12(x982,x983,x984)+~E(x981,x982)+~P12(x981,x983,x984)
% 105.68/105.91 [99]P12(x993,x992,x994)+~E(x991,x992)+~P12(x993,x991,x994)
% 105.68/105.91 [100]P12(x1003,x1004,x1002)+~E(x1001,x1002)+~P12(x1003,x1004,x1001)
% 105.68/105.91
% 105.68/105.91 %-------------------------------------------
% 105.68/105.94 cnf(201,plain,
% 105.68/105.94 (~P10(x2011,x2012)+P8(x2011,f31(x2012))),
% 105.68/105.94 inference(equality_inference,[],[117])).
% 105.68/105.94 cnf(202,plain,
% 105.68/105.94 (~P8(x2021,f31(x2022))+P10(x2021,x2022)),
% 105.68/105.94 inference(equality_inference,[],[118])).
% 105.68/105.94 cnf(203,plain,
% 105.68/105.94 (~P8(x2031,x2032)+P8(x2031,f33(x2033,x2032))),
% 105.68/105.94 inference(equality_inference,[],[127])).
% 105.68/105.94 cnf(204,plain,
% 105.68/105.94 (~P8(x2041,x2042)+P8(x2041,f33(x2042,x2043))),
% 105.68/105.94 inference(equality_inference,[],[128])).
% 105.68/105.94 cnf(205,plain,
% 105.68/105.94 (~P8(x2051,f33(x2052,x2053))+P8(x2051,x2053)+P8(x2051,x2052)),
% 105.68/105.94 inference(equality_inference,[],[135])).
% 105.68/105.94 cnf(207,plain,
% 105.68/105.94 (~P5(x2072,x2071,x2073,x2071)),
% 105.68/105.94 inference(equality_inference,[],[181])).
% 105.68/105.94 cnf(208,plain,
% 105.68/105.94 (~P6(x2081,x2082,x2083,x2082)),
% 105.68/105.94 inference(scs_inference,[],[207,197])).
% 105.68/105.94 cnf(214,plain,
% 105.68/105.94 (P13(x2141,x2142)+~E(f21(x2142),x2141)),
% 105.68/105.94 inference(scs_inference,[],[104,103,207,197,72,73,74,70])).
% 105.68/105.94 cnf(215,plain,
% 105.68/105.94 (P13(f21(x2151),x2152)+~E(x2151,x2152)),
% 105.68/105.94 inference(scs_inference,[],[104,103,207,197,72,73,74,70,71])).
% 105.68/105.94 cnf(216,plain,
% 105.68/105.94 (~P15(x2161,x2162,x2163)+~P15(x2161,x2163,x2162)),
% 105.68/105.94 inference(scs_inference,[],[104,103,207,197,72,73,74,70,71,184])).
% 105.68/105.94 cnf(223,plain,
% 105.68/105.94 (P2(x2231,x2232)+~E(f2(x2232),x2231)),
% 105.68/105.94 inference(scs_inference,[],[102,68])).
% 105.68/105.94 cnf(224,plain,
% 105.68/105.94 (P2(f2(x2241),x2242)+~E(x2241,x2242)),
% 105.68/105.94 inference(scs_inference,[],[102,68,69])).
% 105.68/105.94 cnf(227,plain,
% 105.68/105.94 (~P7(x2271,x2272)+P7(f15(x2272),x2272)),
% 105.68/105.94 inference(scs_inference,[],[106,107])).
% 105.68/105.94 cnf(228,plain,
% 105.68/105.94 (~P7(x2281,x2282)+P7(f3(x2282),x2282)),
% 105.68/105.94 inference(scs_inference,[],[109,105])).
% 105.68/105.94 cnf(229,plain,
% 105.68/105.94 (E(x2291,f33(f17(f2(x2291),x2291),f8(f2(x2291),x2291)))),
% 105.68/105.94 inference(scs_inference,[],[102,2,147])).
% 105.68/105.94 cnf(231,plain,
% 105.68/105.94 (E(f33(f17(f2(x2311),x2311),f8(f2(x2311),x2311)),x2311)),
% 105.68/105.94 inference(scs_inference,[],[229,215,2])).
% 105.68/105.94 cnf(234,plain,
% 105.68/105.94 (P2(f2(x2341),f33(f17(f2(x2341),x2341),f8(f2(x2341),x2341)))),
% 105.68/105.94 inference(scs_inference,[],[229,215,2,181,224])).
% 105.68/105.94 cnf(236,plain,
% 105.68/105.94 (E(x2361,f33(f17(f2(x2361),x2361),f8(f2(x2361),x2361)))),
% 105.68/105.94 inference(rename_variables,[],[229])).
% 105.68/105.94 cnf(238,plain,
% 105.68/105.94 (E(x2381,f33(f17(f2(x2381),x2381),f8(f2(x2381),x2381)))),
% 105.68/105.94 inference(rename_variables,[],[229])).
% 105.68/105.94 cnf(240,plain,
% 105.68/105.94 (E(x2401,f33(f17(f2(x2401),x2401),f8(f2(x2401),x2401)))),
% 105.68/105.94 inference(rename_variables,[],[229])).
% 105.68/105.94 cnf(245,plain,
% 105.68/105.94 (~P7(x2451,f8(f2(x2452),x2452))+P8(x2451,x2452)),
% 105.68/105.94 inference(scs_inference,[],[104,229,236,238,240,215,2,181,224,73,72,74,127,205,110])).
% 105.68/105.94 cnf(255,plain,
% 105.68/105.94 (P8(f21(x2551),f1(x2551))),
% 105.68/105.94 inference(scs_inference,[],[103,112,115])).
% 105.68/105.94 cnf(256,plain,
% 105.68/105.94 (P10(f21(x2561),x2561)),
% 105.68/105.94 inference(scs_inference,[],[255,120])).
% 105.68/105.94 cnf(258,plain,
% 105.68/105.94 (P8(f21(x2581),f33(x2582,f1(x2581)))),
% 105.68/105.94 inference(scs_inference,[],[255,120,203])).
% 105.68/105.94 cnf(297,plain,
% 105.68/105.94 (~P11(x2971)+P11(f33(f17(f2(x2971),x2971),f8(f2(x2971),x2971)))),
% 105.68/105.94 inference(scs_inference,[],[256,229,258,204,203,79,78,122,128,75,84])).
% 105.68/105.94 cnf(298,plain,
% 105.68/105.94 (~P1(f33(f17(f2(x2981),x2981),f8(f2(x2981),x2981)))+P1(x2981)),
% 105.68/105.94 inference(scs_inference,[],[256,229,231,258,204,203,79,78,122,128,75,84,67])).
% 105.68/105.94 cnf(530,plain,
% 105.68/105.94 (P11(x5301)+~P11(f4(x5302,f4(x5301,x5303)))),
% 105.68/105.94 inference(scs_inference,[],[123,124])).
% 105.68/105.94 cnf(592,plain,
% 105.68/105.94 (~P15(f32(a24),a25,x5921)+~P10(a25,f32(a30))),
% 105.68/105.94 inference(scs_inference,[],[151,121])).
% 105.68/105.94 cnf(731,plain,
% 105.68/105.94 (P8(f15(x7311),x7311)+~P7(x7312,x7311)),
% 105.68/105.94 inference(scs_inference,[],[227,110])).
% 105.68/105.94 cnf(762,plain,
% 105.68/105.94 (~P7(x7621,x7622)+~P2(f3(x7622),x7622)),
% 105.68/105.94 inference(scs_inference,[],[228,116])).
% 105.68/105.94 cnf(793,plain,
% 105.68/105.94 (~P7(x7931,f1(x7932))+P10(f15(f1(x7932)),x7932)),
% 105.68/105.94 inference(scs_inference,[],[731,120])).
% 105.68/105.94 cnf(824,plain,
% 105.68/105.94 (~E(f2(x8241),f3(x8241))+~P7(x8242,x8241)),
% 105.68/105.94 inference(scs_inference,[],[762,223])).
% 105.68/105.94 cnf(1055,plain,
% 105.68/105.94 (~E(f6(f15(f1(x10551)),f1(x10551)),f15(f1(x10551)))),
% 105.68/105.94 inference(scs_inference,[],[101,119,107])).
% 105.68/105.94 cnf(1148,plain,
% 105.68/105.94 (P7(f6(f15(f1(x11481)),f1(x11481)),f1(x11481))),
% 105.68/105.94 inference(scs_inference,[],[101,132,107])).
% 105.68/105.94 cnf(1149,plain,
% 105.68/105.94 (P10(f15(f1(x11491)),x11491)),
% 105.68/105.94 inference(scs_inference,[],[1148,793])).
% 105.68/105.94 cnf(1153,plain,
% 105.68/105.94 (~E(f2(f1(x11531)),f6(f15(f1(x11531)),f1(x11531)))),
% 105.68/105.94 inference(scs_inference,[],[102,1148,793,116,68])).
% 105.68/105.94 cnf(1207,plain,
% 105.68/105.94 (~P15(f32(a24),a25,x12071)+~P11(f5(a30,a25))),
% 105.68/105.94 inference(scs_inference,[],[133,592])).
% 105.68/105.94 cnf(1413,plain,
% 105.68/105.94 (~E(f3(f1(x14131)),f2(f1(x14131)))),
% 105.68/105.94 inference(scs_inference,[],[1148,824,2])).
% 105.68/105.94 cnf(3365,plain,
% 105.68/105.94 (~P1(f33(f17(f2(x33651),x33651),f8(f2(x33651),x33651)))+P7(f15(x33651),x33651)),
% 105.68/105.94 inference(scs_inference,[],[298,107])).
% 105.68/105.94 cnf(4280,plain,
% 105.68/105.94 (~P1(f33(f17(f2(x42801),x42801),f8(f2(x42801),x42801)))+~P4(x42801)),
% 105.68/105.94 inference(scs_inference,[],[3365,109])).
% 105.68/105.94 cnf(4326,plain,
% 105.68/105.94 (~P1(f33(f17(f2(x43261),x43261),f8(f2(x43261),x43261)))+P7(f3(x43261),x43261)),
% 105.68/105.94 inference(scs_inference,[],[4280,105])).
% 105.68/105.94 cnf(4372,plain,
% 105.68/105.94 (P8(f3(x43721),x43721)+~P1(f33(f17(f2(x43721),x43721),f8(f2(x43721),x43721)))),
% 105.68/105.94 inference(scs_inference,[],[4326,110])).
% 105.68/105.94 cnf(4418,plain,
% 105.68/105.94 (P8(f3(f1(x44181)),f1(x44181))),
% 105.68/105.94 inference(scs_inference,[],[229,101,4372,67])).
% 105.68/105.94 cnf(4419,plain,
% 105.68/105.94 (P10(f3(f1(x44191)),x44191)),
% 105.68/105.94 inference(scs_inference,[],[4418,120])).
% 105.68/105.94 cnf(4425,plain,
% 105.68/105.94 (P7(f3(f1(x44251)),f1(x44251))+P2(f3(f1(x44251)),f1(x44251))),
% 105.68/105.94 inference(scs_inference,[],[4418,120,204,203,122])).
% 105.68/105.94 cnf(4504,plain,
% 105.68/105.94 (P2(f3(f1(x45041)),f1(x45041))+~E(f6(f3(f1(x45041)),f1(x45041)),f3(f1(x45041)))),
% 105.68/105.94 inference(scs_inference,[],[4425,119])).
% 105.68/105.94 cnf(5623,plain,
% 105.68/105.94 (~E(f3(f1(x56231)),f6(f3(f1(x56231)),f1(x56231)))+P2(f3(f1(x56231)),f1(x56231))),
% 105.68/105.94 inference(scs_inference,[],[4504,2])).
% 105.68/105.94 cnf(10686,plain,
% 105.68/105.94 (P8(f6(f15(f1(x106861)),f1(x106861)),f1(x106861))),
% 105.68/105.94 inference(scs_inference,[],[1148,110])).
% 105.68/105.94 cnf(10688,plain,
% 105.68/105.94 (P10(f6(f15(f1(x106881)),f1(x106881)),x106881)),
% 105.68/105.94 inference(scs_inference,[],[1148,110,120])).
% 105.68/105.94 cnf(10694,plain,
% 105.68/105.94 (P8(f2(x106941),x106941)),
% 105.68/105.94 inference(scs_inference,[],[102,1148,110,120,203,204,111])).
% 105.68/105.94 cnf(10703,plain,
% 105.68/105.94 (P10(f2(f1(x107031)),x107031)),
% 105.68/105.94 inference(scs_inference,[],[1413,10694,2,120])).
% 105.68/105.94 cnf(10704,plain,
% 105.68/105.94 (P8(f2(x107041),x107041)),
% 105.68/105.94 inference(rename_variables,[],[10694])).
% 105.68/105.94 cnf(10706,plain,
% 105.68/105.94 (P8(f2(x107061),f33(f17(f2(x107061),x107061),f8(f2(x107061),x107061)))),
% 105.68/105.94 inference(scs_inference,[],[1413,10694,234,2,120,111])).
% 105.68/105.94 cnf(10708,plain,
% 105.68/105.94 (P8(f2(x107081),f33(x107082,x107081))),
% 105.68/105.94 inference(scs_inference,[],[1413,10694,10704,234,2,120,111,203])).
% 105.68/105.94 cnf(10710,plain,
% 105.68/105.94 (P8(f2(x107101),f33(x107101,x107102))),
% 105.68/105.94 inference(scs_inference,[],[1413,10694,10704,234,2,120,111,203,204])).
% 105.68/105.94 cnf(10712,plain,
% 105.68/105.94 (P8(f2(f8(f2(x107121),x107121)),x107121)),
% 105.68/105.94 inference(scs_inference,[],[1413,229,10694,10704,234,2,120,111,203,204,127])).
% 105.68/105.94 cnf(10713,plain,
% 105.68/105.94 (P8(f2(x107131),x107131)),
% 105.68/105.94 inference(rename_variables,[],[10694])).
% 105.68/105.94 cnf(10715,plain,
% 105.68/105.94 (P8(f2(f17(f2(x107151),x107151)),x107151)),
% 105.68/105.94 inference(scs_inference,[],[1413,229,10694,10704,10713,234,2,120,111,203,204,127,128])).
% 105.68/105.94 cnf(10733,plain,
% 105.68/105.94 (P10(f2(f8(f2(f1(x107331)),f1(x107331))),x107331)),
% 105.68/105.94 inference(scs_inference,[],[10712,120])).
% 105.68/105.94 cnf(10741,plain,
% 105.68/105.94 (P10(f2(f8(f2(f31(x107411)),f31(x107411))),x107411)),
% 105.68/105.94 inference(scs_inference,[],[231,10708,10712,1055,120,2,203,204,118])).
% 105.68/105.94 cnf(10760,plain,
% 105.68/105.94 (~P4(f1(x107601))),
% 105.68/105.94 inference(scs_inference,[],[1148,109])).
% 105.68/105.94 cnf(10762,plain,
% 105.68/105.94 (P10(f2(f17(f2(f1(x107621)),f1(x107621))),x107621)),
% 105.68/105.94 inference(scs_inference,[],[10715,1148,109,120])).
% 105.68/105.94 cnf(10770,plain,
% 105.68/105.94 (P10(f2(f31(x107701)),x107701)),
% 105.68/105.94 inference(scs_inference,[],[10694,10710,10715,1153,1148,109,120,2,203,204,202])).
% 105.68/105.94 cnf(10788,plain,
% 105.68/105.94 (P10(f2(f17(f2(f31(x107881)),f31(x107881))),x107881)),
% 105.68/105.94 inference(scs_inference,[],[10715,202])).
% 105.68/105.94 cnf(10825,plain,
% 105.68/105.94 (P8(f2(f17(f2(x108251),x108251)),f33(x108251,x108252))),
% 105.68/105.94 inference(scs_inference,[],[10715,203,204])).
% 105.68/105.94 cnf(10891,plain,
% 105.68/105.94 (P8(f2(f17(f2(x108911),x108911)),f33(f33(x108911,x108912),x108913))),
% 105.68/105.94 inference(scs_inference,[],[10825,204])).
% 105.68/105.94 cnf(11881,plain,
% 105.68/105.94 (P7(f3(f1(x118811)),f1(x118811))),
% 105.68/105.94 inference(scs_inference,[],[10760,105])).
% 105.68/105.94 cnf(11885,plain,
% 105.68/105.94 (P8(f2(f31(x118851)),f1(x118851))),
% 105.68/105.94 inference(scs_inference,[],[10760,10770,101,105,107,115])).
% 105.68/105.94 cnf(11887,plain,
% 105.68/105.94 (P8(f2(f8(f2(f1(x118871)),f1(x118871))),f31(x118871))),
% 105.68/105.94 inference(scs_inference,[],[10760,10770,10733,101,105,107,115,201])).
% 105.68/105.94 cnf(11890,plain,
% 105.68/105.94 (E(x118901,f33(f17(f2(x118901),x118901),f8(f2(x118901),x118901)))),
% 105.68/105.94 inference(rename_variables,[],[229])).
% 105.68/105.94 cnf(11891,plain,
% 105.68/105.94 (P8(f15(f1(x118911)),f1(x118911))),
% 105.68/105.94 inference(scs_inference,[],[10760,10770,10733,229,101,1148,105,107,115,201,214,731])).
% 105.68/105.94 cnf(11897,plain,
% 105.68/105.94 (P7(f6(f6(f15(f1(x118971)),f1(x118971)),f1(x118971)),f1(x118971))),
% 105.68/105.94 inference(scs_inference,[],[10760,10770,10733,229,101,1148,105,107,115,201,214,731,762,119,132])).
% 105.68/105.94 cnf(11900,plain,
% 105.68/105.94 (P10(f2(f31(x119001)),x119001)),
% 105.68/105.94 inference(rename_variables,[],[10770])).
% 105.68/105.94 cnf(11902,plain,
% 105.68/105.94 (P12(f2(x119021),f17(f2(x119021),x119021),f8(f2(x119021),x119021))),
% 105.68/105.94 inference(scs_inference,[],[10760,10770,10733,229,102,101,1148,105,107,115,201,214,731,762,119,132,131,156])).
% 105.68/105.94 cnf(11911,plain,
% 105.68/105.94 (E(x119111,f33(f17(f2(x119111),x119111),f8(f2(x119111),x119111)))),
% 105.68/105.94 inference(rename_variables,[],[229])).
% 105.68/105.94 cnf(11912,plain,
% 105.68/105.94 (P8(f2(x119121),f17(f2(x119121),x119121))),
% 105.68/105.94 inference(scs_inference,[],[104,10760,10770,10733,229,11890,102,101,1148,105,107,115,201,214,731,762,119,132,131,156,172,4504,5623,223,149])).
% 105.68/105.94 cnf(11914,plain,
% 105.68/105.94 (P8(f2(x119141),f8(f2(x119141),x119141))),
% 105.68/105.94 inference(scs_inference,[],[104,10760,10770,10733,229,11890,102,101,1148,105,107,115,201,214,731,762,119,132,131,156,172,4504,5623,223,149,148])).
% 105.68/105.95 cnf(11923,plain,
% 105.68/105.95 (~P6(x119231,x119232,x119233,x119232)),
% 105.68/105.95 inference(rename_variables,[],[208])).
% 105.68/105.95 cnf(11926,plain,
% 105.68/105.95 (~P7(f2(x119261),x119261)),
% 105.68/105.95 inference(scs_inference,[],[104,10760,10770,10733,10706,234,208,11923,229,11890,11911,102,101,1148,105,107,115,201,214,731,762,119,132,131,156,172,4504,5623,223,149,148,116,136,137,95,97,77])).
% 105.68/105.95 cnf(11931,plain,
% 105.68/105.95 (E(x119311,f33(f17(f2(x119311),x119311),f8(f2(x119311),x119311)))),
% 105.68/105.95 inference(rename_variables,[],[229])).
% 105.68/105.95 cnf(11933,plain,
% 105.68/105.95 (P8(f2(x119331),x119331)),
% 105.68/105.95 inference(rename_variables,[],[10694])).
% 105.68/105.95 cnf(11934,plain,
% 105.68/105.95 (P8(f2(x119341),f33(f17(f2(x119341),x119341),f8(f2(x119341),x119341)))),
% 105.68/105.95 inference(rename_variables,[],[10706])).
% 105.68/105.95 cnf(11937,plain,
% 105.68/105.95 (P8(f2(x119371),x119371)),
% 105.68/105.95 inference(rename_variables,[],[10694])).
% 105.68/105.95 cnf(11941,plain,
% 105.68/105.95 (~E(f3(f1(x119411)),f2(f1(x119411)))),
% 105.68/105.95 inference(rename_variables,[],[1413])).
% 105.68/105.95 cnf(11943,plain,
% 105.68/105.95 (P8(f2(x119431),x119431)),
% 105.68/105.95 inference(rename_variables,[],[10694])).
% 105.68/105.95 cnf(11951,plain,
% 105.68/105.95 (P11(f4(f5(a30,a25),f5(a24,a25)))),
% 105.68/105.95 inference(scs_inference,[],[104,10760,10770,10733,10706,11934,234,1413,10694,11933,11937,208,11923,229,11890,11911,102,4418,101,256,231,1148,105,107,115,201,214,731,762,119,132,131,156,172,4504,5623,223,149,148,116,136,137,95,97,77,117,67,162,161,171,112,114,150,144])).
% 105.68/105.95 cnf(11953,plain,
% 105.68/105.95 (P11(f5(a24,a25))),
% 105.68/105.95 inference(scs_inference,[],[104,10760,10770,10733,10706,11934,234,1413,10694,11933,11937,208,11923,229,11890,11911,102,4418,101,256,231,1148,105,107,115,201,214,731,762,119,132,131,156,172,4504,5623,223,149,148,116,136,137,95,97,77,117,67,162,161,171,112,114,150,144,530])).
% 105.68/105.95 cnf(11957,plain,
% 105.68/105.95 (P11(f4(f4(f4(f5(a24,a25),f5(a30,a25)),f5(a24,a25)),f5(a30,a25)))),
% 105.68/105.95 inference(scs_inference,[],[104,10760,10770,10733,10706,11934,234,1413,10694,11933,11937,208,11923,229,11890,11911,102,4418,101,256,231,1148,105,107,115,201,214,731,762,119,132,131,156,172,4504,5623,223,149,148,116,136,137,95,97,77,117,67,162,161,171,112,114,150,144,530,165,169])).
% 105.68/105.95 cnf(11962,plain,
% 105.68/105.95 (~P12(x119621,f1(x119622),f1(x119622))),
% 105.68/105.95 inference(scs_inference,[],[104,10760,10770,10733,10706,11934,234,1413,10694,11933,11937,208,11923,229,11890,11911,11931,102,4418,101,256,231,1148,105,107,115,201,214,731,762,119,132,131,156,172,4504,5623,223,149,148,116,136,137,95,97,77,117,67,162,161,171,112,114,150,144,530,165,169,297,216,99])).
% 105.68/105.95 cnf(11963,plain,
% 105.68/105.95 (E(x119631,f33(f17(f2(x119631),x119631),f8(f2(x119631),x119631)))),
% 105.68/105.95 inference(rename_variables,[],[229])).
% 105.68/105.95 cnf(11967,plain,
% 105.68/105.95 (P8(f2(x119671),x119671)),
% 105.68/105.95 inference(rename_variables,[],[10694])).
% 105.68/105.95 cnf(11970,plain,
% 105.68/105.95 (P8(f2(x119701),x119701)),
% 105.68/105.95 inference(rename_variables,[],[10694])).
% 105.68/105.95 cnf(11973,plain,
% 105.68/105.95 (P8(f2(x119731),x119731)),
% 105.68/105.95 inference(rename_variables,[],[10694])).
% 105.68/105.95 cnf(11980,plain,
% 105.68/105.95 (P8(f14(f1(x119801),f1(x119801),f21(x119801)),f1(x119801))),
% 105.68/105.95 inference(scs_inference,[],[104,10760,10770,11900,10733,10706,11934,234,255,1413,10694,11933,11937,11943,11967,11970,11973,208,11923,229,11890,11911,11931,11963,102,4418,101,256,231,1148,105,107,115,201,214,731,762,119,132,131,156,172,4504,5623,223,149,148,116,136,137,95,97,77,117,67,162,161,171,112,114,150,144,530,165,169,297,216,99,129,138,139,158,159,79,173])).
% 105.68/105.95 cnf(11981,plain,
% 105.68/105.95 (P8(f21(x119811),f1(x119811))),
% 105.68/105.95 inference(rename_variables,[],[255])).
% 105.68/105.95 cnf(11985,plain,
% 105.68/105.95 (~P7(f14(f1(x119851),f1(x119851),f21(x119851)),f1(x119851))),
% 105.68/105.95 inference(scs_inference,[],[104,10760,10770,11900,10733,10706,11934,234,255,11981,1413,11941,10694,11933,11937,11943,11967,11970,11973,208,11923,229,11890,11911,11931,11963,102,4418,101,256,231,1148,105,107,115,201,214,731,762,119,132,131,156,172,4504,5623,223,149,148,116,136,137,95,97,77,117,67,162,161,171,112,114,150,144,530,165,169,297,216,99,129,138,139,158,159,79,173,152,186])).
% 105.68/105.95 cnf(11991,plain,
% 105.68/105.95 (P7(f6(f3(f1(x119911)),f1(x119911)),f1(x119911))),
% 105.68/105.95 inference(scs_inference,[],[11881,10762,201,132])).
% 105.68/105.95 cnf(11995,plain,
% 105.68/105.95 (P11(f4(f5(a30,a25),f4(f4(f5(a24,a25),f5(a30,a25)),f5(a24,a25))))),
% 105.68/105.95 inference(scs_inference,[],[11881,11957,10741,10762,201,132,115,144])).
% 105.68/105.95 cnf(11999,plain,
% 105.68/105.95 (P11(f4(f5(a24,a25),f5(a24,a25)))),
% 105.68/105.95 inference(scs_inference,[],[11953,11881,11957,10741,10762,201,132,115,144,169,114])).
% 105.68/105.95 cnf(12005,plain,
% 105.77/105.95 (~P7(f2(x120051),x120051)),
% 105.77/105.95 inference(rename_variables,[],[11926])).
% 105.77/105.95 cnf(12008,plain,
% 105.77/105.95 (~P7(f2(x120081),x120081)),
% 105.77/105.95 inference(rename_variables,[],[11926])).
% 105.77/105.95 cnf(12011,plain,
% 105.77/105.95 (~P7(f14(f1(x120111),f1(x120111),f21(x120111)),f1(x120111))),
% 105.77/105.95 inference(rename_variables,[],[11985])).
% 105.77/105.95 cnf(12014,plain,
% 105.77/105.95 (~P7(f2(x120141),x120141)),
% 105.77/105.95 inference(rename_variables,[],[11926])).
% 105.77/105.95 cnf(12017,plain,
% 105.77/105.95 (P8(f14(f1(x120171),f1(x120171),f21(x120171)),f1(x120171))),
% 105.77/105.95 inference(rename_variables,[],[11980])).
% 105.77/105.95 cnf(12023,plain,
% 105.77/105.95 (P8(f14(f1(x120231),f1(x120231),f21(x120231)),f1(x120231))),
% 105.77/105.95 inference(rename_variables,[],[11980])).
% 105.77/105.95 cnf(12025,plain,
% 105.77/105.95 (P8(f14(f1(x120251),f1(x120251),f14(f1(x120251),f1(x120251),f21(x120251))),f1(x120251))),
% 105.77/105.95 inference(scs_inference,[],[11926,12005,12008,12014,11962,11953,11980,12017,12023,11985,12011,11881,11957,10741,10762,10694,256,201,132,115,144,169,114,131,158,139,122,138,136,159,137,174])).
% 105.77/105.95 cnf(12026,plain,
% 105.77/105.95 (P8(f14(f1(x120261),f1(x120261),f21(x120261)),f1(x120261))),
% 105.77/105.95 inference(rename_variables,[],[11980])).
% 105.77/105.95 cnf(12027,plain,
% 105.77/105.95 (~P12(x120271,f1(x120272),f1(x120272))),
% 105.77/105.95 inference(rename_variables,[],[11962])).
% 105.77/105.95 cnf(12031,plain,
% 105.77/105.95 (~P12(x120311,f1(x120312),f1(x120312))),
% 105.77/105.95 inference(rename_variables,[],[11962])).
% 105.77/105.95 cnf(12033,plain,
% 105.77/105.95 (P7(f2(x120331),f17(f2(x120331),x120331))),
% 105.77/105.95 inference(scs_inference,[],[11926,12005,12008,12014,11962,12027,11953,11980,12017,12023,11985,12011,11881,11885,11912,11914,11902,11957,10741,10762,10694,256,201,132,115,144,169,114,131,158,139,122,138,136,159,137,174,173,162])).
% 105.77/105.95 cnf(12034,plain,
% 105.77/105.95 (P8(f2(x120341),f17(f2(x120341),x120341))),
% 105.77/105.95 inference(rename_variables,[],[11912])).
% 105.77/105.95 cnf(12035,plain,
% 105.77/105.95 (P12(f2(x120351),f17(f2(x120351),x120351),f8(f2(x120351),x120351))),
% 105.77/105.95 inference(rename_variables,[],[11902])).
% 105.77/105.95 cnf(12037,plain,
% 105.77/105.95 (P7(f2(x120371),f8(f2(x120371),x120371))),
% 105.77/105.95 inference(scs_inference,[],[11926,12005,12008,12014,11962,12027,11953,11980,12017,12023,11985,12011,11881,11885,11912,12034,11914,11902,12035,11957,10741,10762,10694,256,201,132,115,144,169,114,131,158,139,122,138,136,159,137,174,173,162,161])).
% 105.77/105.95 cnf(12041,plain,
% 105.77/105.95 (~P7(f14(f1(x120411),f1(x120411),f14(f1(x120411),f1(x120411),f21(x120411))),f1(x120411))),
% 105.77/105.95 inference(scs_inference,[],[11926,12005,12008,12014,11962,12027,12031,11953,11980,12017,12023,12026,11985,12011,11881,11885,11912,12034,11914,11902,12035,11957,10741,10762,10694,256,201,132,115,144,169,114,131,158,139,122,138,136,159,137,174,173,162,161,186])).
% 105.77/105.95 cnf(12049,plain,
% 105.77/105.95 (P8(f15(f17(f2(x120491),x120491)),f17(f2(x120491),x120491))),
% 105.77/105.95 inference(scs_inference,[],[11926,12005,12008,12014,11962,12027,12031,11953,11980,12017,12023,12026,11985,12011,11881,11885,11912,12034,11914,11902,12035,11957,10741,10762,10694,256,201,132,115,144,169,114,131,158,139,122,138,136,159,137,174,173,162,161,186,227,228,731])).
% 105.77/105.95 cnf(12084,plain,
% 105.77/105.95 (P8(f14(f1(x120841),f1(x120841),f21(x120841)),f1(x120841))),
% 105.77/105.95 inference(rename_variables,[],[11980])).
% 105.77/105.95 cnf(12090,plain,
% 105.77/105.95 (~P7(f2(x120901),x120901)),
% 105.77/105.95 inference(rename_variables,[],[11926])).
% 105.77/105.95 cnf(12095,plain,
% 105.77/105.95 (P8(f15(f8(f2(x120951),x120951)),x120951)),
% 105.77/105.95 inference(scs_inference,[],[12033,12037,11999,10788,11926,12090,11985,11980,12084,4419,10694,229,228,731,115,132,227,201,119,762,114,139,138,136,137,127])).
% 105.77/105.95 cnf(12105,plain,
% 105.77/105.95 (P11(f4(f4(f4(f5(a24,a25),f5(a24,a25)),f5(a24,a25)),f5(a24,a25)))),
% 105.77/105.95 inference(scs_inference,[],[11891,12033,12037,11999,12049,10788,11926,12090,11962,11985,11980,12084,4419,10694,229,228,731,115,132,227,201,119,762,114,139,138,136,137,127,128,174,245,169])).
% 105.77/105.95 cnf(12112,plain,
% 105.77/105.95 (P7(f6(f6(f3(f1(x121121)),f1(x121121)),f1(x121121)),f1(x121121))),
% 105.77/105.95 inference(scs_inference,[],[12105,11991,144,132])).
% 105.77/105.95 cnf(12116,plain,
% 105.77/105.95 (P11(f4(f4(f5(a30,a25),f5(a24,a25)),f4(f5(a30,a25),f5(a24,a25))))),
% 105.77/105.95 inference(scs_inference,[],[11951,12105,11991,1149,144,132,201,114])).
% 105.77/105.95 cnf(12120,plain,
% 105.77/105.95 (P8(f14(f1(x121201),f1(x121201),f6(f15(f1(x121201)),f1(x121201))),f1(x121201))),
% 105.77/105.95 inference(scs_inference,[],[11951,12105,11991,11962,1149,10686,144,132,201,114,169,174])).
% 105.77/105.95 cnf(12124,plain,
% 105.77/105.95 (P11(f5(a30,a25))),
% 105.77/105.95 inference(scs_inference,[],[11951,12105,11991,11962,1149,10686,144,132,201,114,169,174,530])).
% 105.77/105.95 cnf(12138,plain,
% 105.77/105.95 (~P15(f32(a24),a25,x121381)),
% 105.77/105.95 inference(scs_inference,[],[12124,1207])).
% 105.77/105.95 cnf(12142,plain,
% 105.77/105.95 (P11(f4(f5(a30,a25),f5(a30,a25)))),
% 105.77/105.95 inference(scs_inference,[],[12124,12112,132,114])).
% 105.77/105.95 cnf(12152,plain,
% 105.77/105.95 (P11(f4(f5(a24,a25),f4(f4(f5(a30,a25),f5(a24,a25)),f5(a30,a25))))),
% 105.77/105.95 inference(scs_inference,[],[12124,12112,12116,11962,10688,10694,132,114,201,169,174,144])).
% 105.77/105.95 cnf(12161,plain,
% 105.77/105.95 (P11(f4(f4(f5(a30,a25),f5(a30,a25)),f4(f5(a30,a25),f5(a30,a25))))),
% 105.77/105.95 inference(scs_inference,[],[12142,11897,132,114])).
% 105.77/105.95 cnf(12165,plain,
% 105.77/105.95 (P11(f4(f4(f5(a24,a25),f4(f5(a30,a25),f5(a24,a25))),f5(a30,a25)))),
% 105.77/105.95 inference(scs_inference,[],[12142,12152,11897,10703,132,114,201,169])).
% 105.77/105.95 cnf(12167,plain,
% 105.77/105.95 (~P15(f32(a24),f33(f17(f2(a25),a25),f8(f2(a25),a25)),x121671)),
% 105.77/105.95 inference(scs_inference,[],[12138,12142,12152,11897,10703,231,132,114,201,169,92])).
% 105.77/105.95 cnf(12177,plain,
% 105.77/105.95 (P8(f21(x121771),f31(x121771))),
% 105.77/105.95 inference(scs_inference,[],[256,201])).
% 105.77/105.95 cnf(12185,plain,
% 105.77/105.95 (P11(f4(f5(a30,a25),f4(f4(f5(a30,a25),f5(a30,a25)),f5(a30,a25))))),
% 105.77/105.95 inference(scs_inference,[],[12161,12037,256,201,169,132,245,144])).
% 105.77/105.95 cnf(12204,plain,
% 105.77/105.95 (~P6(f32(a24),a25,f33(f17(f2(a25),a25),f8(f2(a25),a25)),x122041)),
% 105.77/105.95 inference(scs_inference,[],[12185,12167,12138,169,190])).
% 105.77/105.95 cnf(12205,plain,
% 105.77/105.95 (~P15(f32(a24),a25,x122051)),
% 105.77/105.95 inference(rename_variables,[],[12138])).
% 105.77/105.95 cnf(12206,plain,
% 105.77/105.95 (~P15(f32(a24),f33(f17(f2(a25),a25),f8(f2(a25),a25)),x122061)),
% 105.77/105.95 inference(rename_variables,[],[12167])).
% 105.77/105.95 cnf(12211,plain,
% 105.77/105.95 (~P6(f32(a24),x122111,a25,f33(f17(f2(a25),a25),f8(f2(a25),a25)))),
% 105.77/105.95 inference(scs_inference,[],[12025,12041,12185,12167,12206,12138,12205,169,190,122,187])).
% 105.77/105.95 cnf(12221,plain,
% 105.77/105.95 (~P8(f2(f17(f2(x122211),x122211)),f8(f2(x122211),x122211))),
% 105.77/105.95 inference(scs_inference,[],[12177,12025,12041,12185,12167,12206,12138,12205,11902,11926,11962,10694,4418,169,190,122,187,173,137,162])).
% 105.77/105.95 cnf(12222,plain,
% 105.77/105.95 (P8(f2(x122221),x122221)),
% 105.77/105.95 inference(rename_variables,[],[10694])).
% 105.77/105.95 cnf(12223,plain,
% 105.77/105.95 (~P7(f2(x122231),x122231)),
% 105.77/105.95 inference(rename_variables,[],[11926])).
% 105.77/105.95 cnf(12225,plain,
% 105.77/105.95 (~P8(f2(f8(f2(x122251),x122251)),f17(f2(x122251),x122251))),
% 105.77/105.95 inference(scs_inference,[],[12177,12025,12041,12185,12167,12206,12138,12205,11902,11926,12223,11962,10694,12222,4418,169,190,122,187,173,137,162,161])).
% 105.77/105.95 cnf(12256,plain,
% 105.77/105.95 (E(x122561,f33(f17(f2(x122561),x122561),f8(f2(x122561),x122561)))),
% 105.77/105.95 inference(rename_variables,[],[229])).
% 105.77/105.95 cnf(12258,plain,
% 105.77/105.95 (~P8(f2(f8(f2(x122581),x122581)),f17(f2(x122581),x122581))),
% 105.77/105.95 inference(rename_variables,[],[12225])).
% 105.77/105.95 cnf(12263,plain,
% 105.77/105.95 (E(f33(f17(f2(x122631),x122631),f8(f2(x122631),x122631)),x122631)),
% 105.77/105.95 inference(rename_variables,[],[231])).
% 105.77/105.95 cnf(12265,plain,
% 105.77/105.95 (~P8(f2(f8(f2(x122651),x122651)),f17(f2(x122651),x122651))),
% 105.77/105.95 inference(rename_variables,[],[12225])).
% 105.77/105.95 cnf(12275,plain,
% 105.77/105.95 (P10(x122751,x122752)+~P13(f33(f17(f2(x122751),x122751),f8(f2(x122751),x122751)),x122752)),
% 105.77/105.95 inference(scs_inference,[],[11887,12221,12225,12258,12265,12204,12211,10762,229,12256,231,12263,110,111,96,126,97,95,127,128,117,224,70,112])).
% 105.77/105.95 cnf(12700,plain,
% 105.77/105.95 (P8(f2(f17(f2(x127001),x127001)),f33(f33(x127001,x127002),x127003))),
% 105.77/105.95 inference(rename_variables,[],[10891])).
% 105.77/105.95 cnf(12705,plain,
% 105.77/105.95 (~P7(f14(f1(x127051),f1(x127051),f6(f15(f1(x127051)),f1(x127051))),f1(x127051))),
% 105.77/105.95 inference(scs_inference,[],[10891,12700,11962,12221,10686,127,126,186])).
% 105.77/105.95 cnf(12716,plain,
% 105.77/105.95 (~P9(f33(f17(f2(x127161),x127161),f8(f2(x127161),x127161)),x127162)+P9(x127161,x127162)),
% 105.77/105.95 inference(scs_inference,[],[12705,12120,4419,231,122,164,89])).
% 105.77/105.95 cnf(13159,plain,
% 105.77/105.95 (~P8(f7(f33(x131591,x131592),f8(f2(x131591),x131591)),f8(f2(x131591),x131591))),
% 105.77/105.95 inference(scs_inference,[],[10825,12221,126,142])).
% 105.77/105.95 cnf(14076,plain,
% 105.77/105.95 (P10(a25,f32(a24))),
% 105.77/105.95 inference(scs_inference,[],[11953,133])).
% 105.77/105.95 cnf(14078,plain,
% 105.77/105.95 (P3(a30,a24,a25)),
% 105.77/105.95 inference(scs_inference,[],[11953,11951,133,177])).
% 105.77/105.95 cnf(14080,plain,
% 105.77/105.95 (P8(a25,f31(f32(a24)))),
% 105.77/105.95 inference(scs_inference,[],[11953,11951,133,177,201])).
% 105.77/105.95 cnf(14101,plain,
% 105.77/105.95 (~P10(a25,f32(a30))),
% 105.77/105.95 inference(scs_inference,[],[14076,121])).
% 105.77/105.95 cnf(14110,plain,
% 105.77/105.95 (E(x141101,f33(f17(f2(x141101),x141101),f8(f2(x141101),x141101)))),
% 105.77/105.95 inference(rename_variables,[],[229])).
% 105.77/105.95 cnf(14119,plain,
% 105.77/105.95 (P11(f4(f4(f5(a30,a25),f5(a24,a25)),f5(a24,a25)))),
% 105.77/105.95 inference(scs_inference,[],[14078,12165,13159,11995,12095,229,202,74,124,123,148,149,144])).
% 105.77/105.95 cnf(14123,plain,
% 105.77/105.95 (P10(a25,x141231)+~E(f31(f32(a24)),f31(x141231))),
% 105.77/105.95 inference(scs_inference,[],[14078,14080,12165,13159,11995,12095,229,14110,202,74,124,123,148,149,144,72,118])).
% 105.77/105.95 cnf(14148,plain,
% 105.77/105.95 ($false),
% 105.77/105.95 inference(scs_inference,[],[14101,14119,12124,113,151,14123,12275,12716,168,133]),
% 105.77/105.95 ['proof']).
% 105.77/105.95 % SZS output end Proof
% 105.77/105.95 % Total time :104.940000s
%------------------------------------------------------------------------------