%------------------------------------------------------------------------------
% 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 : n032.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 : Theorem 117.49s 117.56s
% Output : CNFRefutation 117.62s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.02/0.09 % Problem : GEO147+1 : TPTP v8.2.0. Released v2.4.0.
% 0.02/0.09 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% 0.08/0.29 % Computer : n032.cluster.edu
% 0.08/0.29 % Model : x86_64 x86_64
% 0.08/0.29 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.29 % Memory : 8042.1875MB
% 0.08/0.29 % OS : Linux 3.10.0-693.el7.x86_64
% 0.08/0.29 % CPULimit : 300
% 0.08/0.29 % WCLimit : 300
% 0.08/0.29 % DateTime : Fri Jun 21 08:43:08 EDT 2024
% 0.08/0.29 % CPUTime :
% 0.15/0.45 start to proof:theBenchmark
% 117.46/117.51 %-------------------------------------------
% 117.46/117.51 % File :CSE---1.7
% 117.46/117.51 % Problem :theBenchmark
% 117.46/117.51 % Transform :cnf
% 117.46/117.51 % Format :tptp:raw
% 117.46/117.51 % Command :java -jar mcs_scs.jar %d %s
% 117.46/117.51
% 117.46/117.51 % Result :Theorem 117.000000s
% 117.46/117.51 % Output :CNFRefutation 117.000000s
% 117.46/117.51 %-------------------------------------------
% 117.49/117.56 %--------------------------------------------------------------------------
% 117.49/117.56 % File : GEO147+1 : TPTP v8.2.0. Released v2.4.0.
% 117.49/117.56 % Domain : Geometry (Oriented curves)
% 117.49/117.56 % Problem : Meeting is possible only if there is a common position
% 117.49/117.56 % Version : [EHK99] axioms.
% 117.49/117.56 % English :
% 117.49/117.56
% 117.49/117.56 % Refs : [KE99] Kulik & Eschenbach (1999), A Geometry of Oriented Curv
% 117.49/117.56 % : [EHK99] Eschenbach et al. (1999), Representing Simple Trajecto
% 117.49/117.56 % Source : [EHK99]
% 117.49/117.56 % Names : T13 [EHK99]
% 117.49/117.56
% 117.49/117.56 % Status : Theorem
% 117.49/117.56 % Rating : 0.17 v8.1.0, 0.14 v7.5.0, 0.16 v7.4.0, 0.07 v7.3.0, 0.10 v7.1.0, 0.13 v6.4.0, 0.19 v6.3.0, 0.17 v6.2.0, 0.20 v6.0.0, 0.13 v5.5.0, 0.22 v5.4.0, 0.29 v5.3.0, 0.37 v5.2.0, 0.20 v5.1.0, 0.19 v5.0.0, 0.29 v4.1.0, 0.30 v4.0.0, 0.29 v3.7.0, 0.25 v3.5.0, 0.26 v3.3.0, 0.21 v3.2.0, 0.27 v3.1.0, 0.22 v2.7.0, 0.17 v2.5.0, 0.00 v2.4.0
% 117.49/117.56 % Syntax : Number of formulae : 37 ( 3 unt; 0 def)
% 117.49/117.56 % Number of atoms : 135 ( 17 equ)
% 117.49/117.56 % Maximal formula atoms : 12 ( 3 avg)
% 117.49/117.56 % Number of connectives : 107 ( 9 ~; 10 |; 42 &)
% 117.49/117.56 % ( 24 <=>; 22 =>; 0 <=; 0 <~>)
% 117.49/117.56 % Maximal formula depth : 12 ( 7 avg)
% 117.49/117.56 % Maximal term depth : 3 ( 1 avg)
% 117.49/117.56 % Number of predicates : 16 ( 15 usr; 0 prp; 1-4 aty)
% 117.49/117.56 % Number of functors : 5 ( 5 usr; 0 con; 1-2 aty)
% 117.49/117.56 % Number of variables : 121 ( 105 !; 16 ?)
% 117.49/117.56 % SPC : FOF_THM_RFO_SEQ
% 117.49/117.56
% 117.49/117.56 % Comments :
% 117.49/117.56 %--------------------------------------------------------------------------
% 117.49/117.56 %----Include simple curve axioms
% 117.49/117.56 include('Axioms/GEO004+0.ax').
% 117.49/117.56 %----Include axioms of betweenness for simple curves
% 117.49/117.56 include('Axioms/GEO004+1.ax').
% 117.49/117.56 %----Include oriented curve axioms
% 117.49/117.56 include('Axioms/GEO004+2.ax').
% 117.49/117.56 %----Include trajectory axioms
% 117.49/117.56 include('Axioms/GEO004+3.ax').
% 117.49/117.56 %--------------------------------------------------------------------------
% 117.49/117.56 fof(t13,conjecture,
% 117.49/117.56 ! [P,X,Y] :
% 117.49/117.56 ( connect(X,Y,P)
% 117.49/117.56 => ( incident_o(P,trajectory_of(X))
% 117.49/117.56 & incident_o(P,trajectory_of(Y)) ) ) ).
% 117.49/117.56
% 117.49/117.56 %--------------------------------------------------------------------------
% 117.49/117.56 %-------------------------------------------
% 117.49/117.56 % Proof found
% 117.49/117.56 % SZS status Theorem for theBenchmark
% 117.49/117.56 % SZS output start Proof
% 117.49/117.60 %ClaNum:200(EqnAxiom:100)
% 117.49/117.60 %VarNum:767(SingletonVarNum:276)
% 117.49/117.60 %MaxLitNum:12
% 117.49/117.60 %MaxfuncDepth:3
% 117.49/117.60 %SharedTerms:8
% 117.49/117.60 %goalClause: 104 121
% 117.49/117.60 %singleGoalClaCount:1
% 117.49/117.60 [104]P3(a16,a23,a17)
% 117.49/117.60 [101]P1(f1(x1011))
% 117.49/117.60 [102]P2(f11(x1021),x1021)
% 117.49/117.60 [103]P13(f12(x1031),x1031)
% 117.49/117.60 [121]~P10(a17,f31(a16))+~P10(a17,f31(a23))
% 117.49/117.60 [105]P4(x1051)+P7(f24(x1051),x1051)
% 117.49/117.60 [107]~P1(x1071)+P7(f29(x1071),x1071)
% 117.49/117.60 [114]~P11(x1141)+P11(f2(x1141,x1141))
% 117.49/117.60 [106]P1(x1061)+~P7(x1062,x1061)
% 117.49/117.60 [109]~P4(x1091)+~P7(x1092,x1091)
% 117.49/117.60 [110]~P7(x1101,x1102)+P8(x1101,x1102)
% 117.49/117.60 [111]~P2(x1111,x1112)+P8(x1111,x1112)
% 117.49/117.60 [112]~P13(x1121,x1122)+P10(x1121,x1122)
% 117.49/117.60 [113]~P9(x1131,x1132)+P10(x1131,x1132)
% 117.49/117.60 [116]~P2(x1161,x1162)+~P7(x1161,x1162)
% 117.49/117.60 [115]~P10(x1151,x1152)+P8(x1151,f1(x1152))
% 117.49/117.60 [119]~P7(x1192,x1191)+~E(f4(x1191,x1192),x1192)
% 117.49/117.60 [120]P10(x1201,x1202)+~P8(x1201,f1(x1202))
% 117.49/117.60 [123]P11(x1231)+~P11(f2(x1232,x1231))
% 117.49/117.60 [124]P11(x1241)+~P11(f2(x1241,x1242))
% 117.49/117.60 [125]P14(x1251,x1252)+P8(f13(x1252,x1251),x1251)
% 117.49/117.60 [131]~P10(x1312,f31(x1311))+P11(f3(x1311,x1312))
% 117.49/117.60 [132]~P7(x1322,x1321)+P7(f4(x1321,x1322),x1321)
% 117.49/117.60 [133]P10(x1331,f31(x1332))+~P11(f3(x1332,x1331))
% 117.49/117.60 [142]P14(x1421,x1422)+~P8(f13(x1422,x1421),x1422)
% 117.49/117.60 [144]~P11(f2(x1442,x1441))+P11(f2(x1441,x1442))
% 117.49/117.60 [156]~P2(x1561,x1562)+P12(x1561,f33(x1562,x1561),f5(x1562,x1561))
% 117.49/117.60 [147]~P2(x1472,x1471)+E(f32(f33(x1471,x1472),f5(x1471,x1472)),x1471)
% 117.49/117.60 [165]~P11(x1651)+P11(f2(x1651,f3(x1652,f22(x1651,x1652))))
% 117.49/117.60 [148]P8(x1481,x1482)+~P12(x1481,x1483,x1482)
% 117.49/117.60 [149]P8(x1491,x1492)+~P12(x1491,x1492,x1493)
% 117.49/117.60 [150]P10(x1501,x1502)+~P15(x1502,x1503,x1501)
% 117.49/117.60 [151]P10(x1511,x1512)+~P15(x1512,x1511,x1513)
% 117.49/117.60 [154]~P12(x1543,x1541,x1542)+E(f8(x1541,x1542),f32(x1541,x1542))
% 117.49/117.60 [168]~P11(f2(f2(x1681,x1682),x1683))+P11(f2(x1681,f2(x1682,x1683)))
% 117.49/117.60 [169]~P11(f2(x1691,f2(x1692,x1693)))+P11(f2(f2(x1691,x1692),x1693))
% 117.49/117.60 [172]~P3(x1721,x1723,x1722)+P11(f2(f3(x1721,x1722),f3(x1723,x1722)))
% 117.49/117.60 [177]P3(x1771,x1772,x1773)+~P11(f2(f3(x1771,x1773),f3(x1772,x1773)))
% 117.49/117.60 [181]~E(x1811,x1812)+~P5(x1813,x1811,x1814,x1812)
% 117.49/117.60 [192]~P5(x1922,x1923,x1924,x1921)+P7(x1921,f9(x1922,x1923,x1924,x1921))
% 117.49/117.60 [193]~P5(x1932,x1931,x1933,x1934)+P7(x1931,f9(x1932,x1931,x1933,x1934))
% 117.49/117.60 [194]~P5(x1942,x1943,x1941,x1944)+P2(x1941,f9(x1942,x1943,x1941,x1944))
% 117.49/117.60 [195]~P5(x1951,x1952,x1953,x1954)+P14(f9(x1951,x1952,x1953,x1954),x1951)
% 117.49/117.60 [197]~P6(x1974,x1971,x1972,x1973)+P5(f14(x1971,x1972,x1973,x1974),x1971,x1972,x1973)
% 117.49/117.60 [108]P1(x1081)+~P14(x1081,x1082)+E(x1081,x1082)
% 117.49/117.60 [122]P2(x1221,x1222)+~P8(x1221,x1222)+P7(x1221,x1222)
% 117.49/117.60 [129]~P10(x1291,x1292)+P13(x1291,x1292)+~E(f6(x1291,x1292),x1291)
% 117.49/117.60 [130]~P10(x1301,x1302)+P9(x1301,x1302)+~E(f10(x1301,x1302),x1301)
% 117.49/117.60 [136]~P8(x1361,x1362)+P7(x1361,x1362)+P8(x1361,f25(x1361,x1362))
% 117.49/117.60 [137]~P8(x1371,x1372)+P7(x1371,x1372)+P8(x1371,f27(x1371,x1372))
% 117.49/117.60 [138]~P8(x1381,x1382)+P7(x1381,x1382)+P14(f25(x1381,x1382),x1382)
% 117.49/117.60 [139]~P8(x1391,x1392)+P7(x1391,x1392)+P14(f27(x1391,x1392),x1392)
% 117.49/117.60 [140]~P10(x1401,x1402)+P13(x1401,x1402)+P10(f6(x1401,x1402),x1402)
% 117.49/117.60 [141]~P10(x1411,x1412)+P9(x1411,x1412)+P10(f10(x1411,x1412),x1412)
% 117.49/117.60 [145]E(x1451,x1452)+P8(f7(x1451,x1452),x1452)+P8(f7(x1451,x1452),x1451)
% 117.49/117.60 [146]P8(f18(x1461,x1462),x1461)+P10(f18(x1461,x1462),x1462)+E(x1461,f30(x1462))
% 117.49/117.60 [155]E(x1551,x1552)+~P8(f7(x1551,x1552),x1552)+~P8(f7(x1551,x1552),x1551)
% 117.49/117.60 [157]~P8(f18(x1571,x1572),x1571)+~P10(f18(x1571,x1572),x1572)+E(x1571,f30(x1572))
% 117.49/117.60 [158]~P8(x1581,x1582)+P7(x1581,x1582)+~P14(f25(x1581,x1582),f27(x1581,x1582))
% 117.49/117.60 [159]~P8(x1591,x1592)+P7(x1591,x1592)+~P14(f27(x1591,x1592),f25(x1591,x1592))
% 117.49/117.60 [163]~P10(x1631,x1632)+P13(x1631,x1632)+~P15(x1632,x1631,f6(x1631,x1632))
% 117.49/117.60 [164]~P10(x1641,x1642)+P9(x1641,x1642)+~P15(x1642,f10(x1641,x1642),x1641)
% 117.49/117.60 [170]E(x1701,x1702)+P15(x1702,f20(x1701,x1702),f21(x1701,x1702))+P15(x1701,f20(x1701,x1702),f21(x1701,x1702))
% 117.49/117.60 [178]E(x1781,x1782)+~P15(x1782,f20(x1781,x1782),f21(x1781,x1782))+~P15(x1781,f20(x1781,x1782),f21(x1781,x1782))
% 117.49/117.60 [126]~P8(x1261,x1263)+P8(x1261,x1262)+~P14(x1263,x1262)
% 117.49/117.60 [117]~P10(x1171,x1173)+P8(x1171,x1172)+~E(x1172,f30(x1173))
% 117.49/117.60 [118]~P8(x1181,x1183)+P10(x1181,x1182)+~E(x1183,f30(x1182))
% 117.49/117.60 [182]~P8(f26(x1821,x1822,x1823),x1823)+~P8(f26(x1821,x1822,x1823),x1821)+E(x1821,f32(x1822,x1823))
% 117.49/117.60 [183]~P8(f26(x1831,x1832,x1833),x1832)+~P8(f26(x1831,x1832,x1833),x1831)+E(x1831,f32(x1832,x1833))
% 117.49/117.60 [184]~P15(x1841,x1843,x1842)+~P15(x1841,x1844,x1843)+P6(x1841,x1842,x1843,x1844)
% 117.49/117.60 [185]~P15(x1851,x1853,x1854)+~P15(x1851,x1852,x1853)+P6(x1851,x1852,x1853,x1854)
% 117.49/117.60 [187]~P6(x1871,x1872,x1873,x1874)+P15(x1871,x1872,x1873)+P15(x1871,x1874,x1873)
% 117.49/117.60 [188]P15(x1881,x1883,x1882)+P15(x1881,x1882,x1883)+~P6(x1881,x1884,x1882,x1883)
% 117.49/117.60 [189]P15(x1891,x1893,x1892)+P15(x1891,x1892,x1893)+~P6(x1891,x1892,x1893,x1894)
% 117.49/117.60 [190]~P6(x1901,x1904,x1902,x1903)+P15(x1901,x1902,x1903)+P15(x1901,x1902,x1904)
% 117.49/117.60 [127]~P8(x1271,x1274)+P8(x1271,x1272)+~E(x1272,f32(x1273,x1274))
% 117.49/117.60 [128]~P8(x1281,x1283)+P8(x1281,x1282)+~E(x1282,f32(x1283,x1284))
% 117.49/117.60 [196]~P10(x1961,x1965)+~P6(x1965,x1962,x1963,x1964)+P8(x1961,f14(x1962,x1963,x1964,x1965))
% 117.49/117.60 [198]P10(x1981,x1982)+~P6(x1982,x1983,x1984,x1985)+~P8(x1981,f14(x1983,x1984,x1985,x1982))
% 117.49/117.60 [152]~P10(x1522,x1523)+~P9(x1521,x1523)+E(x1521,x1522)+P15(x1523,x1522,x1521)
% 117.49/117.60 [153]~P13(x1531,x1533)+~P10(x1532,x1533)+E(x1531,x1532)+P15(x1533,x1531,x1532)
% 117.49/117.60 [173]~P8(x1731,x1733)+~P8(x1731,x1732)+P12(x1731,x1732,x1733)+P8(f28(x1731,x1732,x1733),x1733)
% 117.49/117.60 [174]~P8(x1741,x1743)+~P8(x1741,x1742)+P12(x1741,x1742,x1743)+P8(f28(x1741,x1742,x1743),x1742)
% 117.49/117.60 [180]P8(f26(x1801,x1802,x1803),x1803)+P8(f26(x1801,x1802,x1803),x1802)+P8(f26(x1801,x1802,x1803),x1801)+E(x1801,f32(x1802,x1803))
% 117.49/117.60 [161]~P8(x1611,x1612)+P7(x1611,x1612)+~P12(x1614,x1613,x1612)+~P8(x1611,x1613)
% 117.49/117.61 [162]~P8(x1621,x1622)+P7(x1621,x1622)+~P12(x1624,x1622,x1623)+~P8(x1621,x1623)
% 117.49/117.61 [135]~P8(x1351,x1354)+P8(x1351,x1352)+P8(x1351,x1353)+~E(x1354,f32(x1353,x1352))
% 117.49/117.61 [199]~P5(x1995,x1992,x1993,x1994)+P6(x1991,x1992,x1993,x1994)+P8(f15(x1992,x1993,x1994,x1991,x1995),x1995)+P10(f15(x1992,x1993,x1994,x1991,x1995),x1991)
% 117.49/117.61 [200]P6(x2001,x2002,x2003,x2004)+~P5(x2005,x2002,x2003,x2004)+~P8(f15(x2002,x2003,x2004,x2001,x2005),x2005)+~P10(f15(x2002,x2003,x2004,x2001,x2005),x2001)
% 117.49/117.61 [191]~P15(f31(x1911),x1912,x1913)+~P15(f31(x1914),x1915,x1916)+~P11(f2(f3(x1914,x1916),f3(x1911,x1912)))+~P11(f2(f3(x1914,x1915),f3(x1911,x1913)))
% 117.49/117.61 [171]~P1(x1713)+~P8(x1712,x1713)+~P8(x1711,x1713)+E(x1711,x1712)+P15(f19(x1711,x1712,x1713),x1711,x1712)
% 117.49/117.61 [186]~P8(x1861,x1863)+~P8(x1861,x1862)+P12(x1861,x1862,x1863)+~P7(f28(x1861,x1862,x1863),x1863)+~P7(f28(x1861,x1862,x1863),x1862)
% 117.49/117.61 [166]~P4(x1664)+~P7(x1661,x1662)+P12(x1661,x1662,x1663)+~P12(x1665,x1662,x1663)+~E(x1664,f32(x1662,x1663))
% 117.49/117.61 [134]E(x1343,x1341)+~P7(x1341,x1344)+~P7(x1343,x1344)+E(x1341,x1342)+E(x1343,x1342)+~P7(x1342,x1344)
% 117.49/117.61 [167]~P1(x1674)+~P8(x1672,x1674)+~P8(x1671,x1674)+~P8(x1673,x1674)+E(x1671,x1672)+P10(x1673,f19(x1671,x1672,x1674))
% 117.49/117.61 [176]~P1(x1764)+~P8(x1762,x1764)+~P8(x1761,x1764)+E(x1761,x1762)+P8(x1763,x1764)+~P10(x1763,f19(x1761,x1762,x1764))
% 117.49/117.61 [179]~P7(x1792,x1795)+~P7(x1791,x1795)+~P2(x1794,x1795)+E(x1791,x1792)+P5(x1793,x1791,x1794,x1792)+~P14(x1795,x1793)
% 117.49/117.61 [160]P14(x1602,x1601)+~P14(x1602,x1603)+~P8(x1604,x1602)+~P7(x1604,x1603)+P14(x1601,x1602)+~P14(x1601,x1603)+~P8(x1604,x1601)
% 117.49/117.61 [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)
% 117.49/117.61 %EqnAxiom
% 117.49/117.61 [1]E(x11,x11)
% 117.49/117.61 [2]E(x22,x21)+~E(x21,x22)
% 117.49/117.61 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 117.49/117.61 [4]~E(x41,x42)+E(f1(x41),f1(x42))
% 117.49/117.61 [5]~E(x51,x52)+E(f11(x51),f11(x52))
% 117.49/117.61 [6]~E(x61,x62)+E(f12(x61),f12(x62))
% 117.49/117.61 [7]~E(x71,x72)+E(f24(x71),f24(x72))
% 117.49/117.61 [8]~E(x81,x82)+E(f29(x81),f29(x82))
% 117.49/117.61 [9]~E(x91,x92)+E(f2(x91,x93),f2(x92,x93))
% 117.49/117.61 [10]~E(x101,x102)+E(f2(x103,x101),f2(x103,x102))
% 117.49/117.61 [11]~E(x111,x112)+E(f15(x111,x113,x114,x115,x116),f15(x112,x113,x114,x115,x116))
% 117.49/117.61 [12]~E(x121,x122)+E(f15(x123,x121,x124,x125,x126),f15(x123,x122,x124,x125,x126))
% 117.49/117.61 [13]~E(x131,x132)+E(f15(x133,x134,x131,x135,x136),f15(x133,x134,x132,x135,x136))
% 117.49/117.61 [14]~E(x141,x142)+E(f15(x143,x144,x145,x141,x146),f15(x143,x144,x145,x142,x146))
% 117.49/117.61 [15]~E(x151,x152)+E(f15(x153,x154,x155,x156,x151),f15(x153,x154,x155,x156,x152))
% 117.49/117.61 [16]~E(x161,x162)+E(f30(x161),f30(x162))
% 117.49/117.61 [17]~E(x171,x172)+E(f26(x171,x173,x174),f26(x172,x173,x174))
% 117.49/117.61 [18]~E(x181,x182)+E(f26(x183,x181,x184),f26(x183,x182,x184))
% 117.49/117.61 [19]~E(x191,x192)+E(f26(x193,x194,x191),f26(x193,x194,x192))
% 117.49/117.61 [20]~E(x201,x202)+E(f4(x201,x203),f4(x202,x203))
% 117.49/117.61 [21]~E(x211,x212)+E(f4(x213,x211),f4(x213,x212))
% 117.49/117.61 [22]~E(x221,x222)+E(f32(x221,x223),f32(x222,x223))
% 117.49/117.61 [23]~E(x231,x232)+E(f32(x233,x231),f32(x233,x232))
% 117.49/117.61 [24]~E(x241,x242)+E(f31(x241),f31(x242))
% 117.49/117.61 [25]~E(x251,x252)+E(f3(x251,x253),f3(x252,x253))
% 117.49/117.61 [26]~E(x261,x262)+E(f3(x263,x261),f3(x263,x262))
% 117.49/117.61 [27]~E(x271,x272)+E(f21(x271,x273),f21(x272,x273))
% 117.49/117.61 [28]~E(x281,x282)+E(f21(x283,x281),f21(x283,x282))
% 117.49/117.61 [29]~E(x291,x292)+E(f20(x291,x293),f20(x292,x293))
% 117.49/117.61 [30]~E(x301,x302)+E(f20(x303,x301),f20(x303,x302))
% 117.49/117.61 [31]~E(x311,x312)+E(f13(x311,x313),f13(x312,x313))
% 117.49/117.61 [32]~E(x321,x322)+E(f13(x323,x321),f13(x323,x322))
% 117.49/117.61 [33]~E(x331,x332)+E(f28(x331,x333,x334),f28(x332,x333,x334))
% 117.49/117.61 [34]~E(x341,x342)+E(f28(x343,x341,x344),f28(x343,x342,x344))
% 117.49/117.61 [35]~E(x351,x352)+E(f28(x353,x354,x351),f28(x353,x354,x352))
% 117.49/117.61 [36]~E(x361,x362)+E(f19(x361,x363,x364),f19(x362,x363,x364))
% 117.49/117.61 [37]~E(x371,x372)+E(f19(x373,x371,x374),f19(x373,x372,x374))
% 117.49/117.61 [38]~E(x381,x382)+E(f19(x383,x384,x381),f19(x383,x384,x382))
% 117.49/117.61 [39]~E(x391,x392)+E(f6(x391,x393),f6(x392,x393))
% 117.49/117.61 [40]~E(x401,x402)+E(f6(x403,x401),f6(x403,x402))
% 117.49/117.61 [41]~E(x411,x412)+E(f10(x411,x413),f10(x412,x413))
% 117.49/117.61 [42]~E(x421,x422)+E(f10(x423,x421),f10(x423,x422))
% 117.49/117.61 [43]~E(x431,x432)+E(f9(x431,x433,x434,x435),f9(x432,x433,x434,x435))
% 117.49/117.61 [44]~E(x441,x442)+E(f9(x443,x441,x444,x445),f9(x443,x442,x444,x445))
% 117.49/117.61 [45]~E(x451,x452)+E(f9(x453,x454,x451,x455),f9(x453,x454,x452,x455))
% 117.49/117.61 [46]~E(x461,x462)+E(f9(x463,x464,x465,x461),f9(x463,x464,x465,x462))
% 117.49/117.61 [47]~E(x471,x472)+E(f22(x471,x473),f22(x472,x473))
% 117.49/117.61 [48]~E(x481,x482)+E(f22(x483,x481),f22(x483,x482))
% 117.49/117.61 [49]~E(x491,x492)+E(f25(x491,x493),f25(x492,x493))
% 117.49/117.61 [50]~E(x501,x502)+E(f25(x503,x501),f25(x503,x502))
% 117.49/117.61 [51]~E(x511,x512)+E(f8(x511,x513),f8(x512,x513))
% 117.49/117.61 [52]~E(x521,x522)+E(f8(x523,x521),f8(x523,x522))
% 117.49/117.61 [53]~E(x531,x532)+E(f7(x531,x533),f7(x532,x533))
% 117.49/117.61 [54]~E(x541,x542)+E(f7(x543,x541),f7(x543,x542))
% 117.49/117.61 [55]~E(x551,x552)+E(f33(x551,x553),f33(x552,x553))
% 117.49/117.61 [56]~E(x561,x562)+E(f33(x563,x561),f33(x563,x562))
% 117.49/117.61 [57]~E(x571,x572)+E(f18(x571,x573),f18(x572,x573))
% 117.49/117.61 [58]~E(x581,x582)+E(f18(x583,x581),f18(x583,x582))
% 117.49/117.61 [59]~E(x591,x592)+E(f27(x591,x593),f27(x592,x593))
% 117.49/117.61 [60]~E(x601,x602)+E(f27(x603,x601),f27(x603,x602))
% 117.49/117.61 [61]~E(x611,x612)+E(f5(x611,x613),f5(x612,x613))
% 117.49/117.61 [62]~E(x621,x622)+E(f5(x623,x621),f5(x623,x622))
% 117.49/117.61 [63]~E(x631,x632)+E(f14(x631,x633,x634,x635),f14(x632,x633,x634,x635))
% 117.49/117.61 [64]~E(x641,x642)+E(f14(x643,x641,x644,x645),f14(x643,x642,x644,x645))
% 117.49/117.61 [65]~E(x651,x652)+E(f14(x653,x654,x651,x655),f14(x653,x654,x652,x655))
% 117.49/117.61 [66]~E(x661,x662)+E(f14(x663,x664,x665,x661),f14(x663,x664,x665,x662))
% 117.49/117.61 [67]~P1(x671)+P1(x672)+~E(x671,x672)
% 117.49/117.61 [68]P2(x682,x683)+~E(x681,x682)+~P2(x681,x683)
% 117.49/117.61 [69]P2(x693,x692)+~E(x691,x692)+~P2(x693,x691)
% 117.49/117.61 [70]P13(x702,x703)+~E(x701,x702)+~P13(x701,x703)
% 117.49/117.61 [71]P13(x713,x712)+~E(x711,x712)+~P13(x713,x711)
% 117.49/117.61 [72]P3(x722,x723,x724)+~E(x721,x722)+~P3(x721,x723,x724)
% 117.49/117.61 [73]P3(x733,x732,x734)+~E(x731,x732)+~P3(x733,x731,x734)
% 117.49/117.61 [74]P3(x743,x744,x742)+~E(x741,x742)+~P3(x743,x744,x741)
% 117.49/117.61 [75]~P4(x751)+P4(x752)+~E(x751,x752)
% 117.49/117.61 [76]P7(x762,x763)+~E(x761,x762)+~P7(x761,x763)
% 117.49/117.61 [77]P7(x773,x772)+~E(x771,x772)+~P7(x773,x771)
% 117.49/117.61 [78]P10(x782,x783)+~E(x781,x782)+~P10(x781,x783)
% 117.49/117.61 [79]P10(x793,x792)+~E(x791,x792)+~P10(x793,x791)
% 117.49/117.61 [80]P5(x802,x803,x804,x805)+~E(x801,x802)+~P5(x801,x803,x804,x805)
% 117.49/117.61 [81]P5(x813,x812,x814,x815)+~E(x811,x812)+~P5(x813,x811,x814,x815)
% 117.49/117.61 [82]P5(x823,x824,x822,x825)+~E(x821,x822)+~P5(x823,x824,x821,x825)
% 117.49/117.61 [83]P5(x833,x834,x835,x832)+~E(x831,x832)+~P5(x833,x834,x835,x831)
% 117.49/117.61 [84]~P11(x841)+P11(x842)+~E(x841,x842)
% 117.49/117.61 [85]P8(x852,x853)+~E(x851,x852)+~P8(x851,x853)
% 117.49/117.61 [86]P8(x863,x862)+~E(x861,x862)+~P8(x863,x861)
% 117.49/117.61 [87]P14(x872,x873)+~E(x871,x872)+~P14(x871,x873)
% 117.49/117.61 [88]P14(x883,x882)+~E(x881,x882)+~P14(x883,x881)
% 117.49/117.61 [89]P9(x892,x893)+~E(x891,x892)+~P9(x891,x893)
% 117.49/117.61 [90]P9(x903,x902)+~E(x901,x902)+~P9(x903,x901)
% 117.49/117.61 [91]P15(x912,x913,x914)+~E(x911,x912)+~P15(x911,x913,x914)
% 117.49/117.61 [92]P15(x923,x922,x924)+~E(x921,x922)+~P15(x923,x921,x924)
% 117.49/117.61 [93]P15(x933,x934,x932)+~E(x931,x932)+~P15(x933,x934,x931)
% 117.49/117.61 [94]P6(x942,x943,x944,x945)+~E(x941,x942)+~P6(x941,x943,x944,x945)
% 117.49/117.61 [95]P6(x953,x952,x954,x955)+~E(x951,x952)+~P6(x953,x951,x954,x955)
% 117.49/117.61 [96]P6(x963,x964,x962,x965)+~E(x961,x962)+~P6(x963,x964,x961,x965)
% 117.49/117.61 [97]P6(x973,x974,x975,x972)+~E(x971,x972)+~P6(x973,x974,x975,x971)
% 117.49/117.61 [98]P12(x982,x983,x984)+~E(x981,x982)+~P12(x981,x983,x984)
% 117.49/117.61 [99]P12(x993,x992,x994)+~E(x991,x992)+~P12(x993,x991,x994)
% 117.49/117.61 [100]P12(x1003,x1004,x1002)+~E(x1001,x1002)+~P12(x1003,x1004,x1001)
% 117.49/117.61
% 117.49/117.61 %-------------------------------------------
% 117.62/117.66 cnf(201,plain,
% 117.62/117.66 (~P10(x2011,x2012)+P8(x2011,f30(x2012))),
% 117.62/117.66 inference(equality_inference,[],[117])).
% 117.62/117.66 cnf(202,plain,
% 117.62/117.66 (~P8(x2021,f30(x2022))+P10(x2021,x2022)),
% 117.62/117.66 inference(equality_inference,[],[118])).
% 117.62/117.66 cnf(203,plain,
% 117.62/117.66 (~P8(x2031,x2032)+P8(x2031,f32(x2033,x2032))),
% 117.62/117.66 inference(equality_inference,[],[127])).
% 117.62/117.66 cnf(204,plain,
% 117.62/117.66 (~P8(x2041,x2042)+P8(x2041,f32(x2042,x2043))),
% 117.62/117.66 inference(equality_inference,[],[128])).
% 117.62/117.66 cnf(205,plain,
% 117.62/117.66 (~P8(x2051,f32(x2052,x2053))+P8(x2051,x2053)+P8(x2051,x2052)),
% 117.62/117.66 inference(equality_inference,[],[135])).
% 117.62/117.66 cnf(207,plain,
% 117.62/117.66 (~P5(x2072,x2071,x2073,x2071)),
% 117.62/117.66 inference(equality_inference,[],[181])).
% 117.62/117.66 cnf(208,plain,
% 117.62/117.66 (~P6(x2081,x2082,x2083,x2082)),
% 117.62/117.66 inference(scs_inference,[],[207,197])).
% 117.62/117.66 cnf(214,plain,
% 117.62/117.66 (P13(x2141,x2142)+~E(f12(x2142),x2141)),
% 117.62/117.66 inference(scs_inference,[],[104,103,207,197,72,73,74,70])).
% 117.62/117.66 cnf(215,plain,
% 117.62/117.66 (P13(f12(x2151),x2152)+~E(x2151,x2152)),
% 117.62/117.66 inference(scs_inference,[],[104,103,207,197,72,73,74,70,71])).
% 117.62/117.66 cnf(216,plain,
% 117.62/117.66 (~P15(x2161,x2162,x2163)+~P15(x2161,x2163,x2162)),
% 117.62/117.66 inference(scs_inference,[],[104,103,207,197,72,73,74,70,71,184])).
% 117.62/117.67 cnf(223,plain,
% 117.62/117.67 (P2(x2231,x2232)+~E(f11(x2232),x2231)),
% 117.62/117.67 inference(scs_inference,[],[102,68])).
% 117.62/117.67 cnf(224,plain,
% 117.62/117.67 (P2(f11(x2241),x2242)+~E(x2241,x2242)),
% 117.62/117.67 inference(scs_inference,[],[102,68,69])).
% 117.62/117.67 cnf(227,plain,
% 117.62/117.67 (~P7(x2271,x2272)+P7(f29(x2272),x2272)),
% 117.62/117.67 inference(scs_inference,[],[106,107])).
% 117.62/117.67 cnf(228,plain,
% 117.62/117.67 (~P7(x2281,x2282)+P7(f24(x2282),x2282)),
% 117.62/117.67 inference(scs_inference,[],[109,105])).
% 117.62/117.67 cnf(229,plain,
% 117.62/117.67 (E(x2291,f32(f33(x2291,f11(x2291)),f5(x2291,f11(x2291))))),
% 117.62/117.67 inference(scs_inference,[],[102,2,147])).
% 117.62/117.67 cnf(231,plain,
% 117.62/117.67 (E(f32(f33(x2311,f11(x2311)),f5(x2311,f11(x2311))),x2311)),
% 117.62/117.67 inference(scs_inference,[],[229,215,2])).
% 117.62/117.67 cnf(232,plain,
% 117.62/117.67 (~P5(x2321,x2322,x2323,f32(f33(x2322,f11(x2322)),f5(x2322,f11(x2322))))),
% 117.62/117.67 inference(scs_inference,[],[229,215,2,181])).
% 117.62/117.67 cnf(234,plain,
% 117.62/117.67 (P2(f11(x2341),f32(f33(x2341,f11(x2341)),f5(x2341,f11(x2341))))),
% 117.62/117.67 inference(scs_inference,[],[229,215,2,181,224])).
% 117.62/117.67 cnf(236,plain,
% 117.62/117.67 (E(x2361,f32(f33(x2361,f11(x2361)),f5(x2361,f11(x2361))))),
% 117.62/117.67 inference(rename_variables,[],[229])).
% 117.62/117.67 cnf(238,plain,
% 117.62/117.67 (E(x2381,f32(f33(x2381,f11(x2381)),f5(x2381,f11(x2381))))),
% 117.62/117.67 inference(rename_variables,[],[229])).
% 117.62/117.67 cnf(239,plain,
% 117.62/117.67 (P3(a16,f32(f33(a23,f11(a23)),f5(a23,f11(a23))),a17)),
% 117.62/117.67 inference(scs_inference,[],[104,229,236,238,215,2,181,224,74,72,73])).
% 117.62/117.67 cnf(240,plain,
% 117.62/117.67 (E(x2401,f32(f33(x2401,f11(x2401)),f5(x2401,f11(x2401))))),
% 117.62/117.67 inference(rename_variables,[],[229])).
% 117.62/117.67 cnf(241,plain,
% 117.62/117.67 (~P8(x2411,f5(x2412,f11(x2412)))+P8(x2411,x2412)),
% 117.62/117.67 inference(scs_inference,[],[104,229,236,238,240,215,2,181,224,74,72,73,127])).
% 117.62/117.67 cnf(243,plain,
% 117.62/117.67 (~P8(x2431,f32(f5(x2432,f11(x2432)),f5(x2432,f11(x2432))))+P8(x2431,x2432)),
% 117.62/117.67 inference(scs_inference,[],[104,229,236,238,240,215,2,181,224,74,72,73,127,205])).
% 117.62/117.67 cnf(245,plain,
% 117.62/117.67 (~P7(x2451,f5(x2452,f11(x2452)))+P8(x2451,x2452)),
% 117.62/117.67 inference(scs_inference,[],[104,229,236,238,240,215,2,181,224,74,72,73,127,205,110])).
% 117.62/117.67 cnf(255,plain,
% 117.62/117.67 (P8(f12(x2551),f1(x2551))),
% 117.62/117.67 inference(scs_inference,[],[103,112,115])).
% 117.62/117.67 cnf(256,plain,
% 117.62/117.67 (P10(f12(x2561),x2561)),
% 117.62/117.67 inference(scs_inference,[],[255,120])).
% 117.62/117.67 cnf(260,plain,
% 117.62/117.67 (P8(f12(x2601),f32(f1(x2601),x2602))),
% 117.62/117.67 inference(scs_inference,[],[255,120,203,204])).
% 117.62/117.67 cnf(262,plain,
% 117.62/117.67 (~P5(x2621,f32(f33(x2622,f11(x2622)),f5(x2622,f11(x2622))),x2623,x2622)),
% 117.62/117.67 inference(scs_inference,[],[255,231,120,203,204,181])).
% 117.62/117.67 cnf(292,plain,
% 117.62/117.67 (P8(f12(x2921),f32(f32(f1(x2921),x2922),x2923))),
% 117.62/117.67 inference(scs_inference,[],[260,203,204])).
% 117.62/117.67 cnf(351,plain,
% 117.62/117.67 (~P8(x3511,f33(x3512,f11(x3512)))+P8(x3511,x3512)),
% 117.62/117.67 inference(scs_inference,[],[229,128])).
% 117.62/117.67 cnf(353,plain,
% 117.62/117.67 (P14(x3531,x3532)+~P8(f13(x3532,x3531),f33(x3532,f11(x3532)))),
% 117.62/117.67 inference(scs_inference,[],[229,128,142])).
% 117.62/117.67 cnf(366,plain,
% 117.62/117.67 (~P1(f32(f33(x3661,f11(x3661)),f5(x3661,f11(x3661))))+P1(x3661)),
% 117.62/117.67 inference(scs_inference,[],[231,67])).
% 117.62/117.67 cnf(367,plain,
% 117.62/117.67 (~P11(x3671)+P11(f32(f33(x3671,f11(x3671)),f5(x3671,f11(x3671))))),
% 117.62/117.67 inference(scs_inference,[],[229,231,67,84])).
% 117.62/117.67 cnf(498,plain,
% 117.62/117.67 (P11(x4981)+~P11(f2(x4982,f2(x4981,x4983)))),
% 117.62/117.67 inference(scs_inference,[],[123,124])).
% 117.62/117.67 cnf(529,plain,
% 117.62/117.67 (~P15(x5291,x5292,x5293)+P8(x5293,f1(x5291))),
% 117.62/117.67 inference(scs_inference,[],[150,115])).
% 117.62/117.67 cnf(560,plain,
% 117.62/117.67 (~P15(f31(a16),a17,x5601)+~P10(a17,f31(a23))),
% 117.62/117.67 inference(scs_inference,[],[151,121])).
% 117.62/117.67 cnf(712,plain,
% 117.62/117.67 (P8(f29(x7121),x7121)+~P7(x7122,x7121)),
% 117.62/117.67 inference(scs_inference,[],[227,110])).
% 117.62/117.67 cnf(743,plain,
% 117.62/117.67 (~P7(x7431,x7432)+~P2(f24(x7432),x7432)),
% 117.62/117.67 inference(scs_inference,[],[228,116])).
% 117.62/117.67 cnf(774,plain,
% 117.62/117.67 (~P7(x7741,f1(x7742))+P10(f29(f1(x7742)),x7742)),
% 117.62/117.67 inference(scs_inference,[],[712,120])).
% 117.62/117.67 cnf(805,plain,
% 117.62/117.67 (~E(f11(x8051),f24(x8051))+~P7(x8052,x8051)),
% 117.62/117.67 inference(scs_inference,[],[743,223])).
% 117.62/117.67 cnf(836,plain,
% 117.62/117.67 (E(f1(f32(f33(x8361,f11(x8361)),f5(x8361,f11(x8361)))),f1(x8361))),
% 117.62/117.67 inference(scs_inference,[],[229,4,2])).
% 117.62/117.67 cnf(867,plain,
% 117.62/117.67 (E(f11(f12(x8671)),f11(f12(f32(f33(x8671,f11(x8671)),f5(x8671,f11(x8671))))))),
% 117.62/117.67 inference(scs_inference,[],[229,5,6])).
% 117.62/117.67 cnf(951,plain,
% 117.62/117.67 (E(f30(f2(f32(f33(x9511,f11(x9511)),f5(x9511,f11(x9511))),x9512)),f30(f2(x9511,x9512)))),
% 117.62/117.67 inference(scs_inference,[],[231,16,9])).
% 117.62/117.67 cnf(1043,plain,
% 117.62/117.67 (~E(f4(f1(x10431),f29(f1(x10431))),f29(f1(x10431)))),
% 117.62/117.67 inference(scs_inference,[],[101,119,107])).
% 117.62/117.67 cnf(1090,plain,
% 117.62/117.67 (P14(f32(f33(x10901,f11(x10901)),f5(x10901,f11(x10901))),x10902)+P8(f13(x10902,x10901),x10901)),
% 117.62/117.67 inference(scs_inference,[],[229,125,87])).
% 117.62/117.67 cnf(1136,plain,
% 117.62/117.67 (P7(f4(f1(x11361),f29(f1(x11361))),f1(x11361))),
% 117.62/117.67 inference(scs_inference,[],[101,132,107])).
% 117.62/117.67 cnf(1137,plain,
% 117.62/117.67 (P10(f29(f1(x11371)),x11371)),
% 117.62/117.67 inference(scs_inference,[],[1136,774])).
% 117.62/117.67 cnf(1141,plain,
% 117.62/117.67 (~E(f11(f1(x11411)),f4(f1(x11411),f29(f1(x11411))))),
% 117.62/117.67 inference(scs_inference,[],[102,1136,774,116,68])).
% 117.62/117.67 cnf(1195,plain,
% 117.62/117.67 (~P15(f31(a16),a17,x11951)+~P11(f3(a23,a17))),
% 117.62/117.67 inference(scs_inference,[],[133,560])).
% 117.62/117.67 cnf(1241,plain,
% 117.62/117.67 (~P11(f2(x12411,x12412))+P11(f2(f2(x12412,x12411),f3(x12413,f22(f2(x12412,x12411),x12413))))),
% 117.62/117.67 inference(scs_inference,[],[144,165])).
% 117.62/117.67 cnf(1333,plain,
% 117.62/117.67 (~P11(f2(x13331,f2(f2(f2(x13332,x13333),x13334),x13335)))+P11(f2(x13332,f2(x13333,x13334)))),
% 117.62/117.67 inference(scs_inference,[],[498,168])).
% 117.62/117.67 cnf(1425,plain,
% 117.62/117.67 (~E(f24(f1(x14251)),f11(f1(x14251)))),
% 117.62/117.67 inference(scs_inference,[],[1136,805,2])).
% 117.62/117.67 cnf(1473,plain,
% 117.62/117.67 (~P8(x14731,f5(x14732,f11(x14732)))+P8(x14731,f32(x14732,x14733))),
% 117.62/117.67 inference(scs_inference,[],[241,204])).
% 117.62/117.67 cnf(1611,plain,
% 117.62/117.67 (~P15(f32(f33(f31(a16),f11(f31(a16))),f5(f31(a16),f11(f31(a16)))),a17,x16111)+~P11(f3(a23,a17))),
% 117.62/117.67 inference(scs_inference,[],[231,1195,91])).
% 117.62/117.67 cnf(1841,plain,
% 117.62/117.67 (E(f32(x18411,f15(x18412,x18413,x18414,x18415,x18416)),f32(x18411,f15(x18412,x18413,x18414,f32(f33(x18415,f11(x18415)),f5(x18415,f11(x18415))),x18416)))),
% 117.62/117.67 inference(scs_inference,[],[229,23,14])).
% 117.62/117.67 cnf(1887,plain,
% 117.62/117.67 (E(f3(f15(x18871,x18872,x18873,x18874,x18875),x18876),f3(f15(x18871,x18872,x18873,x18874,f32(f33(x18875,f11(x18875)),f5(x18875,f11(x18875)))),x18876))),
% 117.62/117.67 inference(scs_inference,[],[229,25,15])).
% 117.62/117.67 cnf(2427,plain,
% 117.62/117.67 (E(f33(f33(x24271,x24272),x24273),f33(f33(x24271,f32(f33(x24272,f11(x24272)),f5(x24272,f11(x24272)))),x24273))),
% 117.62/117.67 inference(scs_inference,[],[229,55,56])).
% 117.62/117.67 cnf(2727,plain,
% 117.62/117.67 (E(f8(f33(x27271,f11(x27271)),f5(x27271,f11(x27271))),f32(f33(x27271,f11(x27271)),f5(x27271,f11(x27271))))),
% 117.62/117.67 inference(scs_inference,[],[102,154,156])).
% 117.62/117.67 cnf(2773,plain,
% 117.62/117.67 (P14(x27731,x27732)+~P7(f13(x27732,x27731),f33(x27732,f11(x27732)))),
% 117.62/117.67 inference(scs_inference,[],[353,110])).
% 117.62/117.67 cnf(2911,plain,
% 117.62/117.67 (P8(f11(f5(x29111,f11(x29111))),f32(x29111,x29112))),
% 117.62/117.67 inference(scs_inference,[],[102,1473,111])).
% 117.62/117.67 cnf(2913,plain,
% 117.62/117.67 (P8(f11(f5(x29131,f11(x29131))),f32(f32(x29131,x29132),x29133))),
% 117.62/117.67 inference(scs_inference,[],[2911,204])).
% 117.62/117.67 cnf(2915,plain,
% 117.62/117.67 (P8(f11(f5(x29151,f11(x29151))),f32(x29152,f32(x29151,x29153)))),
% 117.62/117.67 inference(scs_inference,[],[2911,204,203])).
% 117.62/117.67 cnf(2980,plain,
% 117.62/117.67 (~P8(f11(f1(x29801)),f1(x29802))+~P8(f24(f1(x29801)),f1(x29802))+P8(f12(f19(f24(f1(x29801)),f11(f1(x29801)),f1(x29802))),f1(x29802))),
% 117.62/117.67 inference(scs_inference,[],[256,231,1425,1136,101,176])).
% 117.62/117.67 cnf(3127,plain,
% 117.62/117.67 (P11(f2(f2(f2(x31271,x31272),x31273),f2(f2(x31271,x31272),x31273)))+~P11(f2(x31271,f2(x31272,x31273)))),
% 117.62/117.67 inference(scs_inference,[],[169,114])).
% 117.62/117.67 cnf(3402,plain,
% 117.62/117.67 (~P1(f32(f33(x34021,f11(x34021)),f5(x34021,f11(x34021))))+P7(f29(x34021),x34021)),
% 117.62/117.67 inference(scs_inference,[],[366,107])).
% 117.62/117.67 cnf(4192,plain,
% 117.62/117.67 (~P1(f32(f33(x41921,f11(x41921)),f5(x41921,f11(x41921))))+~P4(x41921)),
% 117.62/117.67 inference(scs_inference,[],[3402,109])).
% 117.62/117.67 cnf(4246,plain,
% 117.62/117.67 (~P1(f32(f33(x42461,f11(x42461)),f5(x42461,f11(x42461))))+P7(f24(x42461),x42461)),
% 117.62/117.67 inference(scs_inference,[],[4192,105])).
% 117.62/117.67 cnf(4299,plain,
% 117.62/117.67 (P8(f24(x42991),x42991)+~P1(f32(f33(x42991,f11(x42991)),f5(x42991,f11(x42991))))),
% 117.62/117.67 inference(scs_inference,[],[4246,110])).
% 117.62/117.67 cnf(4352,plain,
% 117.62/117.67 (P8(f24(x43521),x43521)+~P7(x43522,f32(f33(x43521,f11(x43521)),f5(x43521,f11(x43521))))),
% 117.62/117.67 inference(scs_inference,[],[4299,106])).
% 117.62/117.67 cnf(4426,plain,
% 117.62/117.67 (P8(f24(f1(x44261)),f1(x44261))),
% 117.62/117.67 inference(scs_inference,[],[1136,229,4352,77])).
% 117.62/117.67 cnf(4427,plain,
% 117.62/117.67 (P10(f24(f1(x44271)),x44271)),
% 117.62/117.67 inference(scs_inference,[],[4426,120])).
% 117.62/117.67 cnf(4433,plain,
% 117.62/117.67 (P7(f24(f1(x44331)),f1(x44331))+P2(f24(f1(x44331)),f1(x44331))),
% 117.62/117.67 inference(scs_inference,[],[4426,120,204,203,122])).
% 117.62/117.67 cnf(4512,plain,
% 117.62/117.67 (P2(f24(f1(x45121)),f1(x45121))+~P4(f1(x45121))),
% 117.62/117.67 inference(scs_inference,[],[4433,109])).
% 117.62/117.67 cnf(4528,plain,
% 117.62/117.67 (~P4(f1(x45281))),
% 117.62/117.67 inference(scs_inference,[],[1136,4512,743])).
% 117.62/117.67 cnf(4559,plain,
% 117.62/117.67 (P14(f32(f33(f1(x45591),f11(f1(x45591))),f5(f1(x45591),f11(f1(x45591)))),x45592)+P10(f13(x45592,f1(x45591)),x45591)),
% 117.62/117.67 inference(scs_inference,[],[1090,120])).
% 117.62/117.67 cnf(5236,plain,
% 117.62/117.67 (P11(f2(f2(f2(f2(x52361,x52362),x52361),x52362),f2(f2(f2(x52361,x52362),x52361),x52362)))+~P11(f2(x52361,x52362))),
% 117.62/117.67 inference(scs_inference,[],[3127,114])).
% 117.62/117.67 cnf(5926,plain,
% 117.62/117.67 (~P8(f29(f1(x59261)),f1(x59262))+~P8(f4(f1(x59261),f29(f1(x59261))),f1(x59262))+P8(f12(f19(f4(f1(x59261),f29(f1(x59261))),f29(f1(x59261)),f1(x59262))),f1(x59262))),
% 117.62/117.67 inference(scs_inference,[],[1043,256,231,1425,1136,101,176])).
% 117.62/117.67 cnf(6728,plain,
% 117.62/117.67 (P8(f11(x67281),x67281)),
% 117.62/117.67 inference(scs_inference,[],[102,111])).
% 117.62/117.67 cnf(6730,plain,
% 117.62/117.67 (P10(f11(f1(x67301)),x67301)),
% 117.62/117.67 inference(scs_inference,[],[102,111,120])).
% 117.62/117.67 cnf(6736,plain,
% 117.62/117.67 (P8(f4(f1(x67361),f29(f1(x67361))),f1(x67361))),
% 117.62/117.67 inference(scs_inference,[],[102,1136,111,120,204,203,110])).
% 117.62/117.67 cnf(6751,plain,
% 117.62/117.67 (P8(f4(f1(x67511),f29(f1(x67511))),f32(x67512,f1(x67511)))),
% 117.62/117.67 inference(scs_inference,[],[6736,203])).
% 117.62/117.67 cnf(6753,plain,
% 117.62/117.67 (P8(f11(x67531),f32(f33(x67531,f11(x67531)),f5(x67531,f11(x67531))))),
% 117.62/117.67 inference(scs_inference,[],[6736,234,203,111])).
% 117.62/117.67 cnf(6755,plain,
% 117.62/117.67 (P10(f4(f1(x67551),f29(f1(x67551))),x67551)),
% 117.62/117.67 inference(scs_inference,[],[6736,234,203,111,120])).
% 117.62/117.67 cnf(6759,plain,
% 117.62/117.67 (P8(f11(f5(x67591,f11(x67591))),x67591)),
% 117.62/117.67 inference(scs_inference,[],[229,6736,6728,234,203,111,120,204,127])).
% 117.62/117.67 cnf(6760,plain,
% 117.62/117.67 (P8(f11(x67601),x67601)),
% 117.62/117.67 inference(rename_variables,[],[6728])).
% 117.62/117.67 cnf(6762,plain,
% 117.62/117.67 (P8(f11(f33(x67621,f11(x67621))),x67621)),
% 117.62/117.67 inference(scs_inference,[],[229,6736,6728,6760,234,203,111,120,204,127,128])).
% 117.62/117.67 cnf(6770,plain,
% 117.62/117.67 (~E(f11(f1(x67701)),f24(f1(x67701)))),
% 117.62/117.67 inference(scs_inference,[],[1425,2])).
% 117.62/117.67 cnf(6784,plain,
% 117.62/117.67 (P8(f11(x67841),f32(x67842,x67841))),
% 117.62/117.67 inference(scs_inference,[],[6728,203])).
% 117.62/117.67 cnf(6787,plain,
% 117.62/117.67 (P8(f11(x67871),f32(x67871,x67872))),
% 117.62/117.67 inference(scs_inference,[],[6728,1141,203,2,204])).
% 117.62/117.67 cnf(6798,plain,
% 117.62/117.67 (P8(f11(x67981),f32(x67982,f32(x67983,x67981)))),
% 117.62/117.67 inference(scs_inference,[],[6784,203])).
% 117.62/117.67 cnf(6803,plain,
% 117.62/117.67 (P10(f11(f30(x68031)),x68031)),
% 117.62/117.67 inference(scs_inference,[],[6728,6784,1043,203,2,204,202])).
% 117.62/117.67 cnf(6822,plain,
% 117.62/117.67 (P8(f11(x68221),f32(x68222,f32(x68221,x68223)))),
% 117.62/117.67 inference(scs_inference,[],[6787,203])).
% 117.62/117.67 cnf(6824,plain,
% 117.62/117.67 (P8(f11(x68241),f32(f32(x68241,x68242),x68243))),
% 117.62/117.67 inference(scs_inference,[],[6787,203,204])).
% 117.62/117.67 cnf(6842,plain,
% 117.62/117.67 (P8(f11(x68421),f32(x68422,f32(x68423,f32(x68424,x68421))))),
% 117.62/117.67 inference(scs_inference,[],[6798,203])).
% 117.62/117.67 cnf(6878,plain,
% 117.62/117.67 (P8(f11(x68781),f32(f32(x68782,f32(x68781,x68783)),x68784))),
% 117.62/117.67 inference(scs_inference,[],[6822,203,204])).
% 117.62/117.67 cnf(6910,plain,
% 117.62/117.67 (P8(f11(f33(x69101,f11(x69101))),f32(x69102,x69101))),
% 117.62/117.67 inference(scs_inference,[],[6762,203])).
% 117.62/117.67 cnf(6912,plain,
% 117.62/117.67 (P8(f11(f33(x69121,f11(x69121))),f32(x69121,x69122))),
% 117.62/117.67 inference(scs_inference,[],[6762,203,204])).
% 117.62/117.67 cnf(6945,plain,
% 117.62/117.67 (P8(f11(f33(x69451,f11(x69451))),f32(x69452,f32(x69451,x69453)))),
% 117.62/117.67 inference(scs_inference,[],[6912,203])).
% 117.62/117.67 cnf(6962,plain,
% 117.62/117.67 (P8(f11(f5(x69621,f11(x69621))),f32(x69622,x69621))),
% 117.62/117.67 inference(scs_inference,[],[6759,203])).
% 117.62/117.67 cnf(6964,plain,
% 117.62/117.67 (P8(f11(f5(x69641,f11(x69641))),f32(f32(x69642,x69641),x69643))),
% 117.62/117.67 inference(scs_inference,[],[6759,203,204])).
% 117.62/117.67 cnf(10619,plain,
% 117.62/117.67 (P7(f24(f1(x106191)),f1(x106191))),
% 117.62/117.67 inference(scs_inference,[],[4528,105])).
% 117.62/117.67 cnf(10623,plain,
% 117.62/117.67 (P8(f11(f30(x106231)),f1(x106231))),
% 117.62/117.67 inference(scs_inference,[],[4528,6803,101,105,107,115])).
% 117.62/117.67 cnf(10625,plain,
% 117.62/117.67 (P8(f29(f1(x106251)),f30(x106251))),
% 117.62/117.67 inference(scs_inference,[],[4528,6803,1137,101,105,107,115,201])).
% 117.62/117.67 cnf(10627,plain,
% 117.62/117.67 (P8(f29(f1(x106271)),f1(x106271))),
% 117.62/117.67 inference(scs_inference,[],[4528,6803,1137,101,1136,105,107,115,201,712])).
% 117.62/117.67 cnf(10629,plain,
% 117.62/117.67 (~P2(f24(f1(x106291)),f1(x106291))),
% 117.62/117.67 inference(scs_inference,[],[4528,6803,1137,101,1136,105,107,115,201,712,743])).
% 117.62/117.67 cnf(10636,plain,
% 117.62/117.67 (P10(f11(f30(x106361)),x106361)),
% 117.62/117.67 inference(rename_variables,[],[6803])).
% 117.62/117.67 cnf(10638,plain,
% 117.62/117.67 (P12(f11(x106381),f33(x106381,f11(x106381)),f5(x106381,f11(x106381)))),
% 117.62/117.67 inference(scs_inference,[],[4528,6803,1137,102,101,1136,105,107,115,201,712,743,119,132,131,156])).
% 117.62/117.67 cnf(10640,plain,
% 117.62/117.67 (P11(f2(f3(a16,a17),f3(a23,a17)))),
% 117.62/117.67 inference(scs_inference,[],[104,4528,6803,1137,102,101,1136,105,107,115,201,712,743,119,132,131,156,172])).
% 117.62/117.67 cnf(10642,plain,
% 117.62/117.67 (P8(f11(x106421),f33(x106421,f11(x106421)))),
% 117.62/117.67 inference(scs_inference,[],[104,4528,6803,1137,102,101,1136,105,107,115,201,712,743,119,132,131,156,172,149])).
% 117.62/117.67 cnf(10644,plain,
% 117.62/117.67 (P8(f11(x106441),f5(x106441,f11(x106441)))),
% 117.62/117.67 inference(scs_inference,[],[104,4528,6803,1137,102,101,1136,105,107,115,201,712,743,119,132,131,156,172,149,148])).
% 117.62/117.67 cnf(10646,plain,
% 117.62/117.67 (~P7(f11(x106461),f32(f33(x106461,f11(x106461)),f5(x106461,f11(x106461))))),
% 117.62/117.67 inference(scs_inference,[],[104,4528,6803,1137,234,102,101,1136,105,107,115,201,712,743,119,132,131,156,172,149,148,116])).
% 117.62/117.67 cnf(10649,plain,
% 117.62/117.67 (~P6(x106491,x106492,x106493,x106492)),
% 117.62/117.67 inference(rename_variables,[],[208])).
% 117.62/117.67 cnf(10652,plain,
% 117.62/117.67 (P8(f12(f19(f24(f1(x106521)),f11(f1(x106521)),f1(x106521))),f1(x106521))),
% 117.62/117.67 inference(scs_inference,[],[104,4528,6803,1137,234,4426,6728,102,101,229,208,10649,1136,105,107,115,201,712,743,119,132,131,156,172,149,148,116,95,97,2980])).
% 117.62/117.67 cnf(10653,plain,
% 117.62/117.67 (P8(f11(x106531),x106531)),
% 117.62/117.67 inference(rename_variables,[],[6728])).
% 117.62/117.67 cnf(10655,plain,
% 117.62/117.67 (P10(f11(f5(f30(x106551),f11(f30(x106551)))),x106551)),
% 117.62/117.67 inference(scs_inference,[],[104,4528,6803,1137,234,6784,4426,6728,102,101,229,231,208,10649,1136,105,107,115,201,712,743,119,132,131,156,172,149,148,116,95,97,2980,118])).
% 117.62/117.67 cnf(10657,plain,
% 117.62/117.67 (E(f32(f33(x106571,f11(x106571)),f5(x106571,f11(x106571))),x106571)),
% 117.62/117.67 inference(rename_variables,[],[231])).
% 117.62/117.67 cnf(10660,plain,
% 117.62/117.67 (~E(f24(f1(x106601)),f11(f1(x106601)))),
% 117.62/117.67 inference(rename_variables,[],[1425])).
% 117.62/117.67 cnf(10666,plain,
% 117.62/117.67 (P10(f11(f1(x106661)),f19(f24(f1(x106661)),f11(f1(x106661)),f1(x106661)))),
% 117.62/117.67 inference(scs_inference,[],[104,4528,6803,1137,234,6784,4426,6728,10653,1425,102,101,229,231,208,10649,1136,105,107,115,201,712,743,119,132,131,156,172,149,148,116,95,97,2980,118,171,114,150])).
% 117.62/117.67 cnf(10668,plain,
% 117.62/117.67 (P10(f24(f1(x106681)),f19(f24(f1(x106681)),f11(f1(x106681)),f1(x106681)))),
% 117.62/117.67 inference(scs_inference,[],[104,4528,6803,1137,234,6784,4426,6728,10653,1425,102,101,229,231,208,10649,1136,105,107,115,201,712,743,119,132,131,156,172,149,148,116,95,97,2980,118,171,114,150,151])).
% 117.62/117.67 cnf(10672,plain,
% 117.62/117.67 (P11(f2(f3(a23,a17),f3(a16,a17)))),
% 117.62/117.67 inference(scs_inference,[],[104,4528,6803,1137,234,6784,4426,6728,10653,1425,102,101,229,231,208,10649,1136,105,107,115,201,712,743,119,132,131,156,172,149,148,116,95,97,2980,118,171,114,150,151,529,144])).
% 117.62/117.67 cnf(10674,plain,
% 117.62/117.67 (P11(f3(a16,a17))),
% 117.62/117.67 inference(scs_inference,[],[104,4528,6803,1137,234,6784,4426,6728,10653,1425,102,101,229,231,208,10649,1136,105,107,115,201,712,743,119,132,131,156,172,149,148,116,95,97,2980,118,171,114,150,151,529,144,498])).
% 117.62/117.67 cnf(10678,plain,
% 117.62/117.67 (P11(f2(f2(f2(f3(a16,a17),f3(a23,a17)),f3(a16,a17)),f3(a23,a17)))),
% 117.62/117.67 inference(scs_inference,[],[104,4528,6803,1137,234,6784,4426,6728,10653,1425,102,101,229,231,208,10649,1136,105,107,115,201,712,743,119,132,131,156,172,149,148,116,95,97,2980,118,171,114,150,151,529,144,498,165,169])).
% 117.62/117.67 cnf(10680,plain,
% 117.62/117.67 (~P15(f19(f24(f1(x106801)),f11(f1(x106801)),f1(x106801)),f11(f1(x106801)),f24(f1(x106801)))),
% 117.62/117.67 inference(scs_inference,[],[104,4528,6803,1137,234,6784,4426,6728,10653,1425,102,101,229,231,208,10649,1136,105,107,115,201,712,743,119,132,131,156,172,149,148,116,95,97,2980,118,171,114,150,151,529,144,498,165,169,216])).
% 117.62/117.67 cnf(10682,plain,
% 117.62/117.67 (~P14(x106821,x106822)+P14(f32(f33(x106821,f11(x106821)),f5(x106821,f11(x106821))),x106822)),
% 117.62/117.67 inference(scs_inference,[],[104,4528,6803,1137,234,6784,4426,6728,10653,1425,102,101,229,231,208,10649,1136,105,107,115,201,712,743,119,132,131,156,172,149,148,116,95,97,2980,118,171,114,150,151,529,144,498,165,169,216,87])).
% 117.62/117.67 cnf(10685,plain,
% 117.62/117.67 (P10(f11(f30(x106851)),f32(f33(x106851,f11(x106851)),f5(x106851,f11(x106851))))+P14(f32(f33(x106851,f11(x106851)),f5(x106851,f11(x106851))),x106852)),
% 117.62/117.67 inference(scs_inference,[],[104,4528,6803,10636,1137,234,6784,4426,6728,10653,1425,102,101,229,231,10657,208,10649,1136,105,107,115,201,712,743,119,132,131,156,172,149,148,116,95,97,2980,118,171,114,150,151,529,144,498,165,169,216,87,88,79])).
% 117.62/117.67 cnf(10697,plain,
% 117.62/117.67 (~E(f11(f33(x106971,f11(x106971))),f24(f33(x106971,f11(x106971))))+P14(f32(f33(x106972,f11(x106972)),f5(x106972,f11(x106972))),x106973)),
% 117.62/117.67 inference(scs_inference,[],[104,4528,6803,10636,1137,234,6784,4426,6728,10653,1425,10660,102,101,229,231,10657,208,10649,1136,105,107,115,201,712,743,119,132,131,156,172,149,148,116,95,97,2980,118,171,114,150,151,529,144,498,165,169,216,87,88,79,162,161,152,227,228,805])).
% 117.62/117.67 cnf(10699,plain,
% 117.62/117.67 (~P8(f13(x106991,x106992),f33(x106991,f11(x106991)))+P14(f32(f33(x106992,f11(x106992)),f5(x106992,f11(x106992))),x106991)),
% 117.62/117.67 inference(scs_inference,[],[104,4528,6803,10636,1137,234,6784,4426,6728,10653,1425,10660,102,101,229,231,10657,208,10649,1136,105,107,115,201,712,743,119,132,131,156,172,149,148,116,95,97,2980,118,171,114,150,151,529,144,498,165,169,216,87,88,79,162,161,152,227,228,805,353])).
% 117.62/117.67 cnf(10701,plain,
% 117.62/117.67 (~P7(f13(x107011,x107012),f33(x107011,f11(x107011)))+P14(f32(f33(x107012,f11(x107012)),f5(x107012,f11(x107012))),x107011)),
% 117.62/117.67 inference(scs_inference,[],[104,4528,6803,10636,1137,234,6784,4426,6728,10653,1425,10660,102,101,229,231,10657,208,10649,1136,105,107,115,201,712,743,119,132,131,156,172,149,148,116,95,97,2980,118,171,114,150,151,529,144,498,165,169,216,87,88,79,162,161,152,227,228,805,353,2773])).
% 117.62/117.67 cnf(10716,plain,
% 117.62/117.67 (P11(f2(f3(a16,a17),f3(a16,a17)))),
% 117.62/117.67 inference(scs_inference,[],[10674,10678,144,114])).
% 117.62/117.67 cnf(10722,plain,
% 117.62/117.67 (P8(f24(f1(x107221)),f30(x107221))),
% 117.62/117.67 inference(scs_inference,[],[10674,10619,10678,4427,144,114,169,132,201])).
% 117.62/117.67 cnf(10724,plain,
% 117.62/117.67 (P11(f3(x107241,f12(f31(x107241))))),
% 117.62/117.67 inference(scs_inference,[],[10674,10619,10678,4427,256,144,114,169,132,201,131])).
% 117.62/117.67 cnf(10727,plain,
% 117.62/117.67 (~P7(f11(x107271),x107271)),
% 117.62/117.67 inference(scs_inference,[],[10674,10619,10678,4427,102,256,144,114,169,132,201,131,116])).
% 117.62/117.67 cnf(10731,plain,
% 117.62/117.67 (P14(f25(f11(x107311),x107311),x107311)),
% 117.62/117.67 inference(scs_inference,[],[10674,10619,10678,4427,6728,102,256,144,114,169,132,201,131,116,137,138])).
% 117.62/117.67 cnf(10739,plain,
% 117.62/117.67 (P8(f11(x107391),f25(f11(x107391),x107391))),
% 117.62/117.67 inference(scs_inference,[],[10674,10619,10678,4427,6728,102,256,144,114,169,132,201,131,116,137,138,139,158,159,136])).
% 117.62/117.67 cnf(10741,plain,
% 117.62/117.67 (P7(f11(x107411),f33(x107411,f11(x107411)))),
% 117.62/117.67 inference(scs_inference,[],[10674,10619,10642,10644,10638,10678,4427,6728,102,256,144,114,169,132,201,131,116,137,138,139,158,159,136,162])).
% 117.62/117.67 cnf(10742,plain,
% 117.62/117.67 (P12(f11(x107421),f33(x107421,f11(x107421)),f5(x107421,f11(x107421)))),
% 117.62/117.67 inference(rename_variables,[],[10638])).
% 117.62/117.67 cnf(10743,plain,
% 117.62/117.67 (P8(f11(x107431),f5(x107431,f11(x107431)))),
% 117.62/117.67 inference(rename_variables,[],[10644])).
% 117.62/117.67 cnf(10745,plain,
% 117.62/117.67 (P7(f11(x107451),f5(x107451,f11(x107451)))),
% 117.62/117.67 inference(scs_inference,[],[10674,10619,10642,10644,10743,10638,10742,10678,4427,6728,102,256,144,114,169,132,201,131,116,137,138,139,158,159,136,162,161])).
% 117.62/117.67 cnf(10762,plain,
% 117.62/117.67 (P8(f29(f33(x107621,f11(x107621))),f33(x107621,f11(x107621)))),
% 117.62/117.67 inference(scs_inference,[],[10674,10619,10642,10644,10743,10638,10742,10678,4427,4426,6728,102,101,256,6770,144,114,169,132,201,131,116,137,138,139,158,159,136,162,161,167,228,743,119,227,712])).
% 117.62/117.67 cnf(10768,plain,
% 117.62/117.67 (P7(f4(f33(x107681,f11(x107681)),f11(x107681)),f33(x107681,f11(x107681)))),
% 117.62/117.67 inference(scs_inference,[],[10741,132])).
% 117.62/117.67 cnf(10770,plain,
% 117.62/117.67 (P7(f24(f5(x107701,f11(x107701))),f5(x107701,f11(x107701)))),
% 117.62/117.67 inference(scs_inference,[],[10741,10745,132,228])).
% 117.62/117.67 cnf(10774,plain,
% 117.62/117.67 (P7(f29(f5(x107741,f11(x107741))),f5(x107741,f11(x107741)))),
% 117.62/117.67 inference(scs_inference,[],[10741,10745,132,228,119,227])).
% 117.62/117.67 cnf(10780,plain,
% 117.62/117.67 (P8(f4(f1(x107801),f29(f1(x107801))),f30(x107801))),
% 117.62/117.67 inference(scs_inference,[],[10741,10745,10716,6755,132,228,119,227,743,114,201])).
% 117.62/117.67 cnf(10784,plain,
% 117.62/117.67 (P8(f11(f25(f11(x107841),x107841)),x107841)),
% 117.62/117.67 inference(scs_inference,[],[10731,10741,10745,10716,6755,6728,132,228,119,227,743,114,201,712,126])).
% 117.62/117.67 cnf(10798,plain,
% 117.62/117.67 (P11(f2(f3(a16,a17),f2(f2(f3(a16,a17),f3(a16,a17)),f3(a16,a17))))),
% 117.62/117.67 inference(scs_inference,[],[10731,10741,10745,10716,10762,6803,6755,6728,229,132,228,119,227,743,114,201,712,126,127,128,245,169,141,144])).
% 117.62/117.67 cnf(10800,plain,
% 117.62/117.67 (~E(f11(x108001),f11(f5(x108001,f11(x108001))))),
% 117.62/117.67 inference(scs_inference,[],[10727,10731,10741,10745,10716,10762,6803,6755,6728,229,132,228,119,227,743,114,201,712,126,127,128,245,169,141,144,76])).
% 117.62/117.67 cnf(10807,plain,
% 117.62/117.67 (P11(f2(f2(f3(a23,a17),f3(a16,a17)),f2(f3(a23,a17),f3(a16,a17))))),
% 117.62/117.67 inference(scs_inference,[],[10672,10745,132,114])).
% 117.62/117.67 cnf(10809,plain,
% 117.62/117.67 (P8(f11(f1(x108091)),f30(x108091))),
% 117.62/117.67 inference(scs_inference,[],[10672,10745,6730,132,114,201])).
% 117.62/117.67 cnf(10813,plain,
% 117.62/117.67 (P11(f3(a23,a17))),
% 117.62/117.67 inference(scs_inference,[],[10798,10672,10745,6730,132,114,201,169,498])).
% 117.62/117.67 cnf(10815,plain,
% 117.62/117.67 (P8(f4(f5(x108151,f11(x108151)),f11(x108151)),x108151)),
% 117.62/117.67 inference(scs_inference,[],[10798,10672,10745,6730,132,114,201,169,498,245])).
% 117.62/117.67 cnf(10819,plain,
% 117.62/117.67 (~P15(f31(a16),a17,x108191)),
% 117.62/117.67 inference(scs_inference,[],[10798,10672,1137,10745,6730,132,114,201,169,498,245,163,1195])).
% 117.62/117.67 cnf(10821,plain,
% 117.62/117.67 (~P15(f32(f33(f31(a16),f11(f31(a16))),f5(f31(a16),f11(f31(a16)))),a17,x108211)),
% 117.62/117.67 inference(scs_inference,[],[10813,1611])).
% 117.62/117.67 cnf(10822,plain,
% 117.62/117.67 (P11(f2(f3(a23,a17),f3(a23,a17)))),
% 117.62/117.67 inference(scs_inference,[],[10813,114])).
% 117.62/117.67 cnf(10826,plain,
% 117.62/117.67 (P8(f12(x108261),f30(x108261))),
% 117.62/117.67 inference(scs_inference,[],[10813,10807,256,114,169,201])).
% 117.62/117.67 cnf(10832,plain,
% 117.62/117.67 (~P15(f31(a16),a17,x108321)),
% 117.62/117.67 inference(rename_variables,[],[10819])).
% 117.62/117.67 cnf(10835,plain,
% 117.62/117.67 (~P15(f31(a16),a17,x108351)),
% 117.62/117.67 inference(rename_variables,[],[10819])).
% 117.62/117.67 cnf(10836,plain,
% 117.62/117.67 (~P15(f31(a16),a17,x108361)),
% 117.62/117.67 inference(rename_variables,[],[10819])).
% 117.62/117.67 cnf(10838,plain,
% 117.62/117.67 (~P6(f31(a16),x108381,a17,x108382)),
% 117.62/117.67 inference(scs_inference,[],[10813,10819,10832,10836,10835,10807,256,231,114,169,201,92,189,188,190])).
% 117.62/117.67 cnf(10846,plain,
% 117.62/117.67 (P11(f2(f3(a16,a17),f2(f2(f3(a23,a17),f3(a16,a17)),f3(a23,a17))))),
% 117.62/117.67 inference(scs_inference,[],[10813,10819,10832,10836,10835,10623,10807,4426,6728,1425,101,256,231,114,169,201,92,189,188,190,167,144])).
% 117.62/117.67 cnf(10851,plain,
% 117.62/117.67 (P11(f2(f2(f3(a23,a17),f3(a23,a17)),f2(f3(a23,a17),f3(a23,a17))))),
% 117.62/117.67 inference(scs_inference,[],[10822,114])).
% 117.62/117.67 cnf(10856,plain,
% 117.62/117.67 (E(f32(f33(x108561,f11(x108561)),f5(x108561,f11(x108561))),x108561)),
% 117.62/117.67 inference(rename_variables,[],[231])).
% 117.62/117.67 cnf(10858,plain,
% 117.62/117.67 (~P12(x108581,f32(f33(x108582,f11(x108582)),f5(x108582,f11(x108582))),x108583)+P12(x108581,x108582,x108583)),
% 117.62/117.67 inference(scs_inference,[],[10838,10822,10846,229,231,10856,114,169,96,91,99])).
% 117.62/117.67 cnf(10861,plain,
% 117.62/117.67 (P11(f2(f3(a23,a17),f2(f2(f3(a23,a17),f3(a23,a17)),f3(a23,a17))))),
% 117.62/117.67 inference(scs_inference,[],[10851,169,144])).
% 117.62/117.67 cnf(10880,plain,
% 117.62/117.67 (P11(f2(f2(f3(a23,a17),f2(f3(a23,a17),f3(a23,a17))),f3(a23,a17)))),
% 117.62/117.67 inference(scs_inference,[],[10861,169])).
% 117.62/117.67 cnf(10882,plain,
% 117.62/117.67 (~P8(f11(f33(x108821,f11(x108821))),f5(x108821,f11(x108821)))),
% 117.62/117.67 inference(scs_inference,[],[10861,10727,10638,6728,169,162])).
% 117.62/117.67 cnf(10883,plain,
% 117.62/117.67 (P8(f11(x108831),x108831)),
% 117.62/117.67 inference(rename_variables,[],[6728])).
% 117.62/117.67 cnf(10884,plain,
% 117.62/117.67 (~P7(f11(x108841),x108841)),
% 117.62/117.67 inference(rename_variables,[],[10727])).
% 117.62/117.67 cnf(10886,plain,
% 117.62/117.67 (~P8(f11(f5(x108861,f11(x108861))),f33(x108861,f11(x108861)))),
% 117.62/117.67 inference(scs_inference,[],[10861,10727,10884,10638,6728,10883,169,162,161])).
% 117.62/117.67 cnf(10897,plain,
% 117.62/117.67 (~E(f32(x108971,x108972),f32(f33(x108972,f11(x108972)),f33(x108972,f11(x108972))))),
% 117.62/117.67 inference(scs_inference,[],[10784,10861,10727,10884,10638,6962,6728,10883,169,162,161,110,111,205,135])).
% 117.62/117.67 cnf(11076,plain,
% 117.62/117.67 (~P10(f11(f5(x110761,f11(x110761))),x110762)+~E(f33(x110761,f11(x110761)),f30(x110762))),
% 117.62/117.67 inference(scs_inference,[],[6945,10886,10882,127,117])).
% 117.62/117.67 cnf(11090,plain,
% 117.62/117.67 (P12(f4(f5(x110901,f11(x110901)),f11(x110901)),x110901,x110901)+P8(f28(f4(f5(x110901,f11(x110901)),f11(x110901)),x110901,x110901),x110901)),
% 117.62/117.67 inference(scs_inference,[],[10815,173])).
% 117.62/117.67 cnf(11135,plain,
% 117.62/117.67 (~P12(x111351,x111352,f25(f11(x111352),x111352))),
% 117.62/117.67 inference(scs_inference,[],[10739,10727,4427,6728,163,162])).
% 117.62/117.67 cnf(11158,plain,
% 117.62/117.67 (P8(f28(f11(x111581),x111581,f25(f11(x111581),x111581)),x111581)),
% 117.62/117.67 inference(scs_inference,[],[11135,10731,6964,10739,10886,6728,127,108,174])).
% 117.62/117.67 cnf(11190,plain,
% 117.62/117.67 (~P15(f31(a23),a17,a17)),
% 117.62/117.67 inference(scs_inference,[],[10822,191])).
% 117.62/117.67 cnf(11198,plain,
% 117.62/117.67 (E(f32(f33(x111981,f11(x111981)),f5(x111981,f11(x111981))),x111981)),
% 117.62/117.67 inference(rename_variables,[],[231])).
% 117.62/117.67 cnf(11199,plain,
% 117.62/117.67 (~P15(f31(a23),f32(f33(a17,f11(a17)),f5(a17,f11(a17))),a17)),
% 117.62/117.67 inference(scs_inference,[],[11190,231,11198,93,92])).
% 117.62/117.67 cnf(11201,plain,
% 117.62/117.67 (~P6(f31(a23),x112011,a17,a17)),
% 117.62/117.67 inference(scs_inference,[],[11190,231,11198,93,92,188])).
% 117.62/117.67 cnf(11203,plain,
% 117.62/117.67 (~P6(f31(a23),a17,a17,x112031)),
% 117.62/117.67 inference(scs_inference,[],[11190,231,11198,93,92,188,189])).
% 117.62/117.67 cnf(11217,plain,
% 117.62/117.67 (E(f32(f33(x112171,f11(x112171)),f5(x112171,f11(x112171))),x112171)),
% 117.62/117.67 inference(rename_variables,[],[231])).
% 117.62/117.67 cnf(11218,plain,
% 117.62/117.67 (~P6(f31(a23),f32(f33(a17,f11(a17)),f5(a17,f11(a17))),a17,x112181)),
% 117.62/117.67 inference(scs_inference,[],[11201,11203,231,11217,96,95])).
% 117.62/117.67 cnf(11219,plain,
% 117.62/117.67 (E(f32(f33(x112191,f11(x112191)),f5(x112191,f11(x112191))),x112191)),
% 117.62/117.67 inference(rename_variables,[],[231])).
% 117.62/117.67 cnf(11222,plain,
% 117.62/117.67 (P12(f29(f1(x112221)),f1(x112221),f1(x112221))+P8(f28(f29(f1(x112221)),f1(x112221),f1(x112221)),f1(x112221))),
% 117.62/117.67 inference(scs_inference,[],[11201,11203,10627,231,11217,11219,96,95,97,174])).
% 117.62/117.67 cnf(11283,plain,
% 117.62/117.67 (P12(f29(f1(x112831)),f30(x112831),f30(x112831))+P8(f28(f29(f1(x112831)),f30(x112831),f30(x112831)),f30(x112831))),
% 117.62/117.67 inference(scs_inference,[],[10625,174])).
% 117.62/117.67 cnf(11318,plain,
% 117.62/117.67 (P12(f11(f1(x113181)),f30(x113181),f30(x113181))+P8(f28(f11(f1(x113181)),f30(x113181),f30(x113181)),f30(x113181))),
% 117.62/117.67 inference(scs_inference,[],[10809,173])).
% 117.62/117.67 cnf(11342,plain,
% 117.62/117.67 (P8(f11(f33(x113421,f11(x113421))),f32(x113422,x113421))),
% 117.62/117.67 inference(rename_variables,[],[6910])).
% 117.62/117.67 cnf(11347,plain,
% 117.62/117.67 (P8(f13(f5(x113471,f11(x113471)),f32(x113472,x113471)),f32(x113472,x113471))),
% 117.62/117.67 inference(scs_inference,[],[6910,11342,10882,128,126,125])).
% 117.62/117.67 cnf(11349,plain,
% 117.62/117.67 (~P8(f13(f5(x113491,f11(x113491)),f32(x113492,x113491)),f5(x113491,f11(x113491)))),
% 117.62/117.67 inference(scs_inference,[],[6910,11342,10882,128,126,125,142])).
% 117.62/117.67 cnf(11379,plain,
% 117.62/117.67 (~E(f33(x113791,f11(x113791)),f32(x113792,x113791))),
% 117.62/117.67 inference(scs_inference,[],[6759,10886,127])).
% 117.62/117.67 cnf(11391,plain,
% 117.62/117.67 (P8(f11(f33(x113911,f11(x113911))),x113911)),
% 117.62/117.67 inference(rename_variables,[],[6762])).
% 117.62/117.67 cnf(11396,plain,
% 117.62/117.67 (P8(f13(f5(x113961,f11(x113961)),x113961),x113961)),
% 117.62/117.67 inference(scs_inference,[],[6762,11391,10882,128,126,125])).
% 117.62/117.67 cnf(11435,plain,
% 117.62/117.67 (P12(f24(f1(x114351)),f30(x114351),f30(x114351))+P8(f28(f24(f1(x114351)),f30(x114351),f30(x114351)),f30(x114351))),
% 117.62/117.67 inference(scs_inference,[],[10722,2911,10886,127,173])).
% 117.62/117.67 cnf(11455,plain,
% 117.62/117.67 (~P14(f32(x114551,f5(x114552,f11(x114552))),f33(x114552,f11(x114552)))),
% 117.62/117.67 inference(scs_inference,[],[6784,6962,10886,128,126])).
% 117.62/117.67 cnf(11490,plain,
% 117.62/117.67 (P12(f29(f1(x114901)),f1(x114901),f1(x114901))+~P7(f28(f29(f1(x114901)),f1(x114901),f1(x114901)),f1(x114901))),
% 117.62/117.67 inference(scs_inference,[],[10627,186])).
% 117.62/117.67 cnf(11522,plain,
% 117.62/117.67 (P12(f4(f1(x115221),f29(f1(x115221))),f30(x115221),f30(x115221))+P8(f28(f4(f1(x115221),f29(f1(x115221))),f30(x115221),f30(x115221)),f30(x115221))),
% 117.62/117.67 inference(scs_inference,[],[10780,10886,2915,127,174])).
% 117.62/117.67 cnf(11533,plain,
% 117.62/117.67 (P12(f11(f30(x115331)),f1(x115331),f1(x115331))+P8(f28(f11(f30(x115331)),f1(x115331),f1(x115331)),f1(x115331))),
% 117.62/117.67 inference(scs_inference,[],[10623,173])).
% 117.62/117.67 cnf(11556,plain,
% 117.62/117.67 (~E(f33(x115561,f11(x115561)),f32(x115561,x115562))),
% 117.62/117.67 inference(scs_inference,[],[6759,10886,6728,127,128])).
% 117.62/117.67 cnf(11657,plain,
% 117.62/117.67 (P12(f12(x116571),f30(x116571),f30(x116571))+P8(f28(f12(x116571),f30(x116571),f30(x116571)),f30(x116571))),
% 117.62/117.67 inference(scs_inference,[],[10826,173])).
% 117.62/117.67 cnf(11686,plain,
% 117.62/117.67 (~P14(f32(x116861,x116862),f5(x116861,f11(x116861)))),
% 117.62/117.67 inference(scs_inference,[],[6912,10886,10882,2913,128,126])).
% 117.62/117.67 cnf(11689,plain,
% 117.62/117.67 (P8(f13(f5(x116891,f11(x116891)),f32(x116891,x116892)),f32(x116891,x116892))),
% 117.62/117.67 inference(scs_inference,[],[6912,10886,10882,2913,128,126,125])).
% 117.62/117.67 cnf(11741,plain,
% 117.62/117.67 (~P14(x117411,f33(x117411,f11(x117411)))),
% 117.62/117.67 inference(scs_inference,[],[6824,6759,10886,2915,136,128,126])).
% 117.62/117.67 cnf(11746,plain,
% 117.62/117.67 (~P8(f13(f33(x117461,f11(x117461)),x117461),f33(x117461,f11(x117461)))),
% 117.62/117.67 inference(scs_inference,[],[6824,6759,10886,2915,136,128,126,125,142])).
% 117.62/117.67 cnf(11829,plain,
% 117.62/117.67 (~P14(f32(f33(x118291,f11(x118291)),x118292),f5(x118291,f11(x118291)))),
% 117.62/117.67 inference(scs_inference,[],[6787,10882,6728,128,126])).
% 117.62/117.67 cnf(11889,plain,
% 117.62/117.67 (~P14(f32(x118891,x118892),f33(x118891,f11(x118891)))),
% 117.62/117.67 inference(scs_inference,[],[2911,10886,6728,128,126])).
% 117.62/117.67 cnf(11952,plain,
% 117.62/117.67 (~P12(x119521,x119522,f5(x119522,f11(x119522)))),
% 117.62/117.67 inference(scs_inference,[],[10644,10727,6728,162])).
% 117.62/117.67 cnf(12111,plain,
% 117.62/117.67 (~P14(f33(x121111,f11(x121111)),f5(x121111,f11(x121111)))),
% 117.62/117.67 inference(scs_inference,[],[10882,6728,126])).
% 117.62/117.67 cnf(12192,plain,
% 117.62/117.67 (P12(f11(x121921),f32(x121921,x121922),f32(x121921,x121922))+P8(f28(f11(x121921),f32(x121921,x121922),f32(x121921,x121922)),f32(x121921,x121922))),
% 117.62/117.67 inference(scs_inference,[],[6787,173])).
% 117.62/117.67 cnf(12218,plain,
% 117.62/117.67 (P12(f11(f5(x122181,f11(x122181))),f32(x122181,x122182),f32(x122181,x122182))+P8(f28(f11(f5(x122181,f11(x122181))),f32(x122181,x122182),f32(x122181,x122182)),f32(x122181,x122182))),
% 117.62/117.67 inference(scs_inference,[],[2911,174])).
% 117.62/117.67 cnf(12338,plain,
% 117.62/117.67 (P12(f24(f1(x123381)),f1(x123381),f1(x123381))+P8(f28(f24(f1(x123381)),f1(x123381),f1(x123381)),f1(x123381))),
% 117.62/117.67 inference(scs_inference,[],[4426,173])).
% 117.62/117.67 cnf(12348,plain,
% 117.62/117.67 (P12(f12(x123481),f1(x123481),f1(x123481))+P8(f28(f12(x123481),f1(x123481),f1(x123481)),f1(x123481))),
% 117.62/117.67 inference(scs_inference,[],[255,174])).
% 117.62/117.67 cnf(12466,plain,
% 117.62/117.67 (P12(f4(f1(x124661),f29(f1(x124661))),f1(x124661),f1(x124661))+P8(f28(f4(f1(x124661),f29(f1(x124661))),f1(x124661),f1(x124661)),f1(x124661))),
% 117.62/117.67 inference(scs_inference,[],[6736,173])).
% 117.62/117.67 cnf(12511,plain,
% 117.62/117.67 (P12(f12(x125111),f1(x125111),f1(x125111))+~P7(f28(f12(x125111),f1(x125111),f1(x125111)),f1(x125111))),
% 117.62/117.67 inference(scs_inference,[],[255,186])).
% 117.62/117.67 cnf(12628,plain,
% 117.62/117.67 (~P10(f13(f33(x126281,f11(x126281)),x126281),x126282)+~E(f33(x126281,f11(x126281)),f30(x126282))),
% 117.62/117.67 inference(scs_inference,[],[292,11746,126,117])).
% 117.62/117.67 cnf(13207,plain,
% 117.62/117.67 (P12(f13(f5(x132071,f11(x132071)),f32(x132072,x132071)),f32(x132072,x132071),f32(x132072,x132071))+~P7(f28(f13(f5(x132071,f11(x132071)),f32(x132072,x132071)),f32(x132072,x132071),f32(x132072,x132071)),f32(x132072,x132071))),
% 117.62/117.67 inference(scs_inference,[],[11347,186])).
% 117.62/117.67 cnf(13443,plain,
% 117.62/117.67 (P12(f4(f1(x134431),f29(f1(x134431))),f30(x134431),f30(x134431))+~P7(f28(f4(f1(x134431),f29(f1(x134431))),f30(x134431),f30(x134431)),f30(x134431))),
% 117.62/117.67 inference(scs_inference,[],[6878,10780,6728,161,186])).
% 117.62/117.67 cnf(13505,plain,
% 117.62/117.67 (~P12(x135051,x135052,f32(f33(x135052,f11(x135052)),f5(x135052,f11(x135052))))),
% 117.62/117.67 inference(scs_inference,[],[6753,10646,6728,161])).
% 117.62/117.67 cnf(13510,plain,
% 117.62/117.67 (~P12(x135101,x135102,x135102)),
% 117.62/117.67 inference(scs_inference,[],[13505,229,100])).
% 117.62/117.67 cnf(13512,plain,
% 117.62/117.67 (P8(f28(f13(f5(x135121,f11(x135121)),f32(x135121,x135122)),f32(x135121,x135122),f32(x135121,x135122)),f32(x135121,x135122))),
% 117.62/117.67 inference(scs_inference,[],[13505,11689,229,100,174])).
% 117.62/117.67 cnf(13514,plain,
% 117.62/117.67 (~P7(f28(f13(f5(x135141,f11(x135141)),f32(x135141,x135142)),f32(x135141,x135142),f32(x135141,x135142)),f32(x135141,x135142))),
% 117.62/117.67 inference(scs_inference,[],[13505,11689,229,100,174,186])).
% 117.62/117.67 cnf(13523,plain,
% 117.62/117.67 (P8(f28(f12(x135231),f1(x135231),f1(x135231)),f1(x135231))),
% 117.62/117.67 inference(scs_inference,[],[13510,12348])).
% 117.62/117.67 cnf(13524,plain,
% 117.62/117.67 (~P12(x135241,x135242,x135242)),
% 117.62/117.67 inference(rename_variables,[],[13510])).
% 117.62/117.67 cnf(13526,plain,
% 117.62/117.67 (~P12(x135261,x135262,x135262)),
% 117.62/117.67 inference(rename_variables,[],[13510])).
% 117.62/117.67 cnf(13527,plain,
% 117.62/117.67 (P8(f28(f29(f1(x135271)),f1(x135271),f1(x135271)),f1(x135271))),
% 117.62/117.67 inference(scs_inference,[],[13510,13524,13526,12348,12511,11222])).
% 117.62/117.67 cnf(13528,plain,
% 117.62/117.67 (~P12(x135281,x135282,x135282)),
% 117.62/117.67 inference(rename_variables,[],[13510])).
% 117.62/117.67 cnf(13530,plain,
% 117.62/117.67 (~P12(x135301,x135302,x135302)),
% 117.62/117.67 inference(rename_variables,[],[13510])).
% 117.62/117.67 cnf(13531,plain,
% 117.62/117.67 (~P7(f28(f4(f1(x135311),f29(f1(x135311))),f30(x135311),f30(x135311)),f30(x135311))),
% 117.62/117.67 inference(scs_inference,[],[13510,13524,13526,13528,13530,12348,12511,11222,12466,13443])).
% 117.62/117.67 cnf(13532,plain,
% 117.62/117.67 (~P12(x135321,x135322,x135322)),
% 117.62/117.67 inference(rename_variables,[],[13510])).
% 117.62/117.67 cnf(13534,plain,
% 117.62/117.67 (~P12(x135341,x135342,x135342)),
% 117.62/117.67 inference(rename_variables,[],[13510])).
% 117.62/117.67 cnf(13536,plain,
% 117.62/117.67 (~P12(x135361,x135362,x135362)),
% 117.62/117.67 inference(rename_variables,[],[13510])).
% 117.62/117.67 cnf(13538,plain,
% 117.62/117.67 (~P12(x135381,x135382,x135382)),
% 117.62/117.67 inference(rename_variables,[],[13510])).
% 117.62/117.67 cnf(13539,plain,
% 117.62/117.67 (P8(f28(f12(x135391),f30(x135391),f30(x135391)),f30(x135391))),
% 117.62/117.67 inference(scs_inference,[],[13510,13524,13526,13528,13530,13532,13534,13536,13538,12348,12511,11222,12466,13443,12218,13207,11283,11657])).
% 117.62/117.67 cnf(13540,plain,
% 117.62/117.67 (~P12(x135401,x135402,x135402)),
% 117.62/117.67 inference(rename_variables,[],[13510])).
% 117.62/117.67 cnf(13541,plain,
% 117.62/117.67 (~P12(x135411,f32(f33(x135412,f11(x135412)),f5(x135412,f11(x135412))),x135412)),
% 117.62/117.67 inference(scs_inference,[],[13510,13524,13526,13528,13530,13532,13534,13536,13538,13540,12348,12511,11222,12466,13443,12218,13207,11283,11657,10858])).
% 117.62/117.67 cnf(13543,plain,
% 117.62/117.67 (~P12(x135431,x135432,x135432)),
% 117.62/117.67 inference(rename_variables,[],[13510])).
% 117.62/117.67 cnf(13561,plain,
% 117.62/117.67 (~P12(x135611,x135612,x135612)),
% 117.62/117.67 inference(rename_variables,[],[13510])).
% 117.62/117.67 cnf(13564,plain,
% 117.62/117.67 (~P12(x135641,x135642,x135642)),
% 117.62/117.67 inference(rename_variables,[],[13510])).
% 117.62/117.67 cnf(13566,plain,
% 117.62/117.67 (P8(f28(f11(f1(x135661)),f30(x135661),f30(x135661)),f30(x135661))),
% 117.62/117.67 inference(scs_inference,[],[13510,13524,13526,13528,13530,13532,13534,13536,13538,13540,13543,13561,13564,13512,13514,11347,12348,12511,11222,12466,13443,12218,13207,11283,11657,10858,11090,158,159,137,139,138,122,136,174,173,11318])).
% 117.62/117.67 cnf(13567,plain,
% 117.62/117.67 (~P12(x135671,x135672,x135672)),
% 117.62/117.67 inference(rename_variables,[],[13510])).
% 117.62/117.67 cnf(13569,plain,
% 117.62/117.67 (~P12(x135691,x135692,x135692)),
% 117.62/117.67 inference(rename_variables,[],[13510])).
% 117.62/117.67 cnf(13570,plain,
% 117.62/117.67 (~P7(f28(f29(f1(x135701)),f1(x135701),f1(x135701)),f1(x135701))),
% 117.62/117.67 inference(scs_inference,[],[13510,13524,13526,13528,13530,13532,13534,13536,13538,13540,13543,13561,13564,13567,13569,13512,13514,11347,12348,12511,11222,12466,13443,12218,13207,11283,11657,10858,11090,158,159,137,139,138,122,136,174,173,11318,11435,11490])).
% 117.62/117.67 cnf(13571,plain,
% 117.62/117.67 (~P12(x135711,x135712,x135712)),
% 117.62/117.67 inference(rename_variables,[],[13510])).
% 117.62/117.67 cnf(13572,plain,
% 117.62/117.67 (P8(f28(f11(f30(x135721)),f1(x135721),f1(x135721)),f1(x135721))),
% 117.62/117.67 inference(scs_inference,[],[13510,13524,13526,13528,13530,13532,13534,13536,13538,13540,13543,13561,13564,13567,13569,13571,13512,13514,11347,12348,12511,11222,12466,13443,12218,13207,11283,11657,10858,11090,158,159,137,139,138,122,136,174,173,11318,11435,11490,11533])).
% 117.62/117.67 cnf(13573,plain,
% 117.62/117.67 (~P12(x135731,x135732,x135732)),
% 117.62/117.67 inference(rename_variables,[],[13510])).
% 117.62/117.67 cnf(13575,plain,
% 117.62/117.67 (~P12(x135751,x135752,x135752)),
% 117.62/117.67 inference(rename_variables,[],[13510])).
% 117.62/117.67 cnf(13577,plain,
% 117.62/117.67 (~P12(x135771,x135772,x135772)),
% 117.62/117.67 inference(rename_variables,[],[13510])).
% 117.62/117.67 cnf(13578,plain,
% 117.62/117.67 (P8(f28(f4(f1(x135781),f29(f1(x135781))),f30(x135781),f30(x135781)),f30(x135781))),
% 117.62/117.67 inference(scs_inference,[],[13510,13524,13526,13528,13530,13532,13534,13536,13538,13540,13543,13561,13564,13567,13569,13571,13573,13575,13577,13512,13514,11347,12348,12511,11222,12466,13443,12218,13207,11283,11657,10858,11090,158,159,137,139,138,122,136,174,173,11318,11435,11490,11533,12338,12192,11522])).
% 117.62/117.67 cnf(13600,plain,
% 117.62/117.67 (~P7(f28(f29(f1(x136001)),f1(x136001),f1(x136001)),f1(x136001))),
% 117.62/117.67 inference(rename_variables,[],[13570])).
% 117.62/117.67 cnf(13605,plain,
% 117.62/117.67 (P8(f28(f28(f12(x136051),f1(x136051),f1(x136051)),f1(x136051),f1(x136051)),f1(x136051))),
% 117.62/117.67 inference(scs_inference,[],[13523,13527,13570,13600,13510,139,138,174])).
% 117.62/117.67 cnf(13606,plain,
% 117.62/117.67 (~P12(x136061,x136062,x136062)),
% 117.62/117.67 inference(rename_variables,[],[13510])).
% 117.62/117.67 cnf(13608,plain,
% 117.62/117.67 (~P7(f28(f28(f12(x136081),f1(x136081),f1(x136081)),f1(x136081),f1(x136081)),f1(x136081))),
% 117.62/117.67 inference(scs_inference,[],[13523,13527,13570,13600,13510,13606,139,138,174,186])).
% 117.62/117.67 cnf(13620,plain,
% 117.62/117.67 (P14(f25(f28(f28(f12(x136201),f1(x136201),f1(x136201)),f1(x136201),f1(x136201)),f1(x136201)),f1(x136201))),
% 117.62/117.67 inference(scs_inference,[],[13605,13608,138])).
% 117.62/117.67 cnf(13715,plain,
% 117.62/117.67 (P8(f28(f28(f11(f1(x137151)),f30(x137151),f30(x137151)),f30(x137151),f30(x137151)),f30(x137151))),
% 117.62/117.67 inference(scs_inference,[],[13566,13510,173])).
% 117.62/117.67 cnf(13737,plain,
% 117.62/117.67 (P8(f28(f28(f28(f11(f1(x137371)),f30(x137371),f30(x137371)),f30(x137371),f30(x137371)),f30(x137371),f30(x137371)),f30(x137371))),
% 117.62/117.67 inference(scs_inference,[],[13620,13715,13510,108,174])).
% 117.62/117.67 cnf(13738,plain,
% 117.62/117.67 (~P12(x137381,x137382,x137382)),
% 117.62/117.67 inference(rename_variables,[],[13510])).
% 117.62/117.67 cnf(13740,plain,
% 117.62/117.67 (~P7(f28(f28(f28(f11(f1(x137401)),f30(x137401),f30(x137401)),f30(x137401),f30(x137401)),f30(x137401),f30(x137401)),f30(x137401))),
% 117.62/117.67 inference(scs_inference,[],[13620,13715,13510,13738,108,174,186])).
% 117.62/117.67 cnf(13787,plain,
% 117.62/117.67 (P8(f28(f28(f11(f30(x137871)),f1(x137871),f1(x137871)),f1(x137871),f1(x137871)),f1(x137871))),
% 117.62/117.67 inference(scs_inference,[],[13740,13572,13737,13510,122,173])).
% 117.62/117.67 cnf(13803,plain,
% 117.62/117.67 (P10(f28(f12(x138031),f1(x138031),f1(x138031)),f19(f24(f1(x138031)),f11(f1(x138031)),f1(x138031)))),
% 117.62/117.67 inference(scs_inference,[],[1425,13787,13523,13510,4426,6728,101,174,167])).
% 117.62/117.67 cnf(13873,plain,
% 117.62/117.68 (P8(f28(f28(f28(f12(x138731),f1(x138731),f1(x138731)),f1(x138731),f1(x138731)),f1(x138731),f1(x138731)),f1(x138731))),
% 117.62/117.68 inference(scs_inference,[],[13605,13510,173])).
% 117.62/117.68 cnf(14320,plain,
% 117.62/117.68 (P14(f25(f28(f28(f28(f12(x143201),f1(x143201),f1(x143201)),f1(x143201),f1(x143201)),f1(x143201),f1(x143201)),f1(x143201)),f1(x143201))),
% 117.62/117.68 inference(scs_inference,[],[13605,13873,13510,186,138])).
% 117.62/117.68 cnf(14448,plain,
% 117.62/117.68 (~P14(f32(x144481,x144482),f33(x144481,f11(x144481)))),
% 117.62/117.68 inference(rename_variables,[],[11889])).
% 117.62/117.68 cnf(14457,plain,
% 117.62/117.68 (~P14(f32(x144571,f5(x144572,f11(x144572))),f33(x144572,f11(x144572)))),
% 117.62/117.68 inference(rename_variables,[],[11455])).
% 117.62/117.68 cnf(14460,plain,
% 117.62/117.68 (~P14(f32(x144601,f5(x144602,f11(x144602))),f33(x144602,f11(x144602)))),
% 117.62/117.68 inference(rename_variables,[],[11455])).
% 117.62/117.68 cnf(14463,plain,
% 117.62/117.68 (~P14(f32(x144631,f5(x144632,f11(x144632))),f33(x144632,f11(x144632)))),
% 117.62/117.68 inference(rename_variables,[],[11455])).
% 117.62/117.68 cnf(14469,plain,
% 117.62/117.68 (P2(f11(f12(f32(f33(x144691,f11(x144691)),f5(x144691,f11(x144691))))),f12(x144691))),
% 117.62/117.68 inference(scs_inference,[],[11455,14457,14460,836,867,10640,11889,14448,11349,6910,4,5,6,7,8,16,24,9,10,20,21,22,23,25,26,27,28,29,30,31,32,39,40,41,42,47,48,49,50,51,52,53,54,55,56,57,58,59,60,61,62,10682,1090,1241,5236,4559,10697,10685,243,351,223])).
% 117.62/117.68 cnf(14508,plain,
% 117.62/117.68 (P11(f2(f2(f2(f2(f2(f3(a16,a17),f3(a23,a17)),f3(a16,a17)),f3(a23,a17)),f2(f2(f3(a16,a17),f3(a23,a17)),f3(a16,a17))),f3(a23,a17)))),
% 117.62/117.68 inference(scs_inference,[],[12111,11455,14457,14460,10655,836,867,10774,10640,11889,14448,11349,11158,6910,4,5,6,7,8,16,24,9,10,20,21,22,23,25,26,27,28,29,30,31,32,39,40,41,42,47,48,49,50,51,52,53,54,55,56,57,58,59,60,61,62,10682,1090,1241,5236,4559,10697,10685,243,351,223,64,165,44,17,35,14,34,45,2,18,19,15,11076,33,12,36,63,38,46,43,65,11,37,66,13,119,111,2773,353,241,169])).
% 117.62/117.68 cnf(14547,plain,
% 117.62/117.68 (~P5(x145471,x145472,x145473,f8(f33(x145472,f11(x145472)),f5(x145472,f11(x145472))))),
% 117.62/117.68 inference(scs_inference,[],[12111,13803,11455,14457,14460,10880,10655,836,2727,867,239,10774,10640,232,11889,14448,10813,11349,11158,234,10627,6910,6755,6736,4,5,6,7,8,16,24,9,10,20,21,22,23,25,26,27,28,29,30,31,32,39,40,41,42,47,48,49,50,51,52,53,54,55,56,57,58,59,60,61,62,10682,1090,1241,5236,4559,10697,10685,243,351,223,64,165,44,17,35,14,34,45,2,18,19,15,11076,33,12,36,63,38,46,43,65,11,37,66,13,119,111,2773,353,241,169,125,156,201,149,367,172,132,498,142,148,116,131,144,115,110,805,114,5926,83])).
% 117.62/117.68 cnf(14548,plain,
% 117.62/117.68 (E(f8(f33(x145481,f11(x145481)),f5(x145481,f11(x145481))),f32(f33(x145481,f11(x145481)),f5(x145481,f11(x145481))))),
% 117.62/117.68 inference(rename_variables,[],[2727])).
% 117.62/117.68 cnf(14551,plain,
% 117.62/117.68 (E(f1(f32(f33(x145511,f11(x145511)),f5(x145511,f11(x145511)))),f1(x145511))),
% 117.62/117.68 inference(rename_variables,[],[836])).
% 117.62/117.68 cnf(14556,plain,
% 117.62/117.68 (E(f32(f33(x145561,f11(x145561)),f5(x145561,f11(x145561))),x145561)),
% 117.62/117.68 inference(rename_variables,[],[231])).
% 117.62/117.68 cnf(14560,plain,
% 117.62/117.68 (E(x145601,f32(f33(x145601,f11(x145601)),f5(x145601,f11(x145601))))),
% 117.62/117.68 inference(rename_variables,[],[229])).
% 117.62/117.68 cnf(14565,plain,
% 117.62/117.68 (E(f8(f33(x145651,f11(x145651)),f5(x145651,f11(x145651))),f32(f33(x145651,f11(x145651)),f5(x145651,f11(x145651))))),
% 117.62/117.68 inference(rename_variables,[],[2727])).
% 117.62/117.68 cnf(14569,plain,
% 117.62/117.68 (E(f32(f33(x145691,f11(x145691)),f5(x145691,f11(x145691))),x145691)),
% 117.62/117.68 inference(rename_variables,[],[231])).
% 117.62/117.68 cnf(14577,plain,
% 117.62/117.68 (P8(f12(f19(f24(f1(x145771)),f11(f1(x145771)),f1(x145771))),f1(x145771))),
% 117.62/117.68 inference(rename_variables,[],[10652])).
% 117.62/117.68 cnf(14581,plain,
% 117.62/117.68 (E(f8(f33(x145811,f11(x145811)),f5(x145811,f11(x145811))),f32(f33(x145811,f11(x145811)),f5(x145811,f11(x145811))))),
% 117.62/117.68 inference(rename_variables,[],[2727])).
% 117.62/117.68 cnf(14586,plain,
% 117.62/117.68 (~P7(f28(f4(f1(x145861),f29(f1(x145861))),f30(x145861),f30(x145861)),f30(x145861))),
% 117.62/117.68 inference(rename_variables,[],[13531])).
% 117.62/117.68 cnf(14589,plain,
% 117.62/117.68 (~P7(f28(f4(f1(x145891),f29(f1(x145891))),f30(x145891),f30(x145891)),f30(x145891))),
% 117.62/117.68 inference(rename_variables,[],[13531])).
% 117.62/117.68 cnf(14592,plain,
% 117.62/117.68 (~P7(f28(f4(f1(x145921),f29(f1(x145921))),f30(x145921),f30(x145921)),f30(x145921))),
% 117.62/117.68 inference(rename_variables,[],[13531])).
% 117.62/117.68 cnf(14598,plain,
% 117.62/117.68 (~P7(f28(f28(f28(f11(f1(x145981)),f30(x145981),f30(x145981)),f30(x145981),f30(x145981)),f30(x145981),f30(x145981)),f30(x145981))),
% 117.62/117.68 inference(rename_variables,[],[13740])).
% 117.62/117.68 cnf(14604,plain,
% 117.62/117.68 (E(f32(f33(x146041,f11(x146041)),f5(x146041,f11(x146041))),x146041)),
% 117.62/117.68 inference(rename_variables,[],[231])).
% 117.62/117.68 cnf(14618,plain,
% 117.62/117.68 (~P15(f19(f24(f1(x146181)),f11(f1(x146181)),f1(x146181)),f11(f1(x146181)),f24(f1(x146181)))),
% 117.62/117.68 inference(rename_variables,[],[10680])).
% 117.62/117.68 cnf(14635,plain,
% 117.62/117.68 (~P14(f32(x146351,f5(x146352,f11(x146352))),f33(x146352,f11(x146352)))),
% 117.62/117.68 inference(rename_variables,[],[11455])).
% 117.62/117.68 cnf(14661,plain,
% 117.62/117.68 (E(f32(f33(x146611,f11(x146611)),f5(x146611,f11(x146611))),x146611)),
% 117.62/117.68 inference(rename_variables,[],[231])).
% 117.62/117.68 cnf(14668,plain,
% 117.62/117.68 (E(x146681,f32(f33(x146681,f11(x146681)),f5(x146681,f11(x146681))))),
% 117.62/117.68 inference(rename_variables,[],[229])).
% 117.62/117.68 cnf(14671,plain,
% 117.62/117.68 (~P2(f24(f1(f32(f33(x146711,f11(x146711)),f5(x146711,f11(x146711))))),f1(x146711))),
% 117.62/117.68 inference(scs_inference,[],[1141,12111,10724,14320,13803,11455,14457,14460,14463,14635,10880,10652,14577,10680,14618,10655,836,14551,2727,14548,14565,14581,10821,951,867,2427,1841,1887,239,13541,10629,10774,10640,232,262,11889,14448,11741,13740,14598,13531,14586,14589,14592,13505,13737,13578,11203,10741,10813,10666,10668,11218,11349,11158,6842,234,6753,11952,11347,10627,11199,6910,6755,1137,10882,13510,6728,6736,1425,101,256,6770,229,14560,14668,231,14556,14569,14604,14661,4,5,6,7,8,16,24,9,10,20,21,22,23,25,26,27,28,29,30,31,32,39,40,41,42,47,48,49,50,51,52,53,54,55,56,57,58,59,60,61,62,10682,1090,1241,5236,4559,10697,10685,243,351,223,64,165,44,17,35,14,34,45,2,18,19,15,11076,33,12,36,63,38,46,43,65,11,37,66,13,119,111,2773,353,241,169,125,156,201,149,367,172,132,498,142,148,116,131,144,115,110,805,114,5926,83,86,69,117,92,127,88,77,99,78,96,205,100,128,95,84,158,159,137,136,139,138,94,126,161,174,173,153,152,171,12628,1333,10699,10701,214,10858,151,150,227,712,228,245,743,216,81,93,3,85,87,72,74,68])).
% 117.62/117.68 cnf(14745,plain,
% 117.62/117.68 (P10(a17,f31(a23))),
% 117.62/117.68 inference(scs_inference,[],[10886,10623,11556,13539,11396,10745,10880,10768,10813,10800,10861,110,120,203,116,148,204,106,202,109,149,2,223,5,351,123,124,133])).
% 117.62/117.68 cnf(14778,plain,
% 117.62/117.68 (~P10(a17,f31(a16))),
% 117.62/117.68 inference(scs_inference,[],[14745,121])).
% 117.62/117.68 cnf(14788,plain,
% 117.62/117.68 (P8(f11(f5(x147881,f11(x147881))),x147881)),
% 117.62/117.68 inference(rename_variables,[],[6759])).
% 117.62/117.68 cnf(14828,plain,
% 117.62/117.68 (P8(f11(f5(x148281,f11(x148281))),x148281)),
% 117.62/117.68 inference(rename_variables,[],[6759])).
% 117.62/117.68 cnf(14842,plain,
% 117.62/117.68 (P10(a17,f31(a16))),
% 117.62/117.68 inference(scs_inference,[],[231,229,6751,836,10886,10882,6759,14788,14828,11379,11396,11135,10774,10768,10897,10770,10674,14671,14469,14508,14547,11829,11686,120,110,203,116,148,204,224,106,202,215,109,181,245,149,197,10858,214,2,241,111,223,351,10699,10682,124,23,1473,133])).
% 117.62/117.68 cnf(14958,plain,
% 117.62/117.68 ($false),
% 117.62/117.68 inference(scs_inference,[],[14778,14842]),
% 117.62/117.68 ['proof']).
% 117.62/117.69 % SZS output end Proof
% 117.62/117.69 % Total time :117.000000s
%------------------------------------------------------------------------------