%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : GEO148+1 : TPTP v8.2.0. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% Computer : n001.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:03 EDT 2024
% Result : Theorem 117.32s 117.34s
% Output : CNFRefutation 117.47s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.08/0.13 % Problem : GEO148+1 : TPTP v8.2.0. Released v2.4.0.
% 0.08/0.13 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% 0.13/0.35 % Computer : n001.cluster.edu
% 0.13/0.35 % Model : x86_64 x86_64
% 0.13/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.35 % Memory : 8042.1875MB
% 0.13/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.35 % CPULimit : 300
% 0.13/0.35 % WCLimit : 300
% 0.13/0.35 % DateTime : Fri Jun 21 09:57:54 EDT 2024
% 0.13/0.35 % CPUTime :
% 0.21/0.58 start to proof:theBenchmark
% 117.32/117.30 %-------------------------------------------
% 117.32/117.30 % File :CSE---1.7
% 117.32/117.30 % Problem :theBenchmark
% 117.32/117.30 % Transform :cnf
% 117.32/117.30 % Format :tptp:raw
% 117.32/117.30 % Command :java -jar mcs_scs.jar %d %s
% 117.32/117.30
% 117.32/117.30 % Result :Theorem 116.660000s
% 117.32/117.30 % Output :CNFRefutation 116.660000s
% 117.32/117.30 %-------------------------------------------
% 117.32/117.33 %--------------------------------------------------------------------------
% 117.32/117.33 % File : GEO148+1 : TPTP v8.2.0. Released v2.4.0.
% 117.32/117.33 % Domain : Geometry (Oriented curves)
% 117.32/117.33 % Problem : No meeting if someone has already passed
% 117.32/117.33 % Version : [EHK99] axioms.
% 117.32/117.33 % English : A point can only be a meeting point of two moving objects if
% 117.32/117.33 % it is not the case that one object already passed through it
% 117.32/117.33 % when the other object was still moving towards it
% 117.32/117.33
% 117.32/117.33 % Refs : [KE99] Kulik & Eschenbach (1999), A Geometry of Oriented Curv
% 117.32/117.33 % : [EHK99] Eschenbach et al. (1999), Representing Simple Trajecto
% 117.32/117.33 % Source : [EHK99]
% 117.32/117.33 % Names : T14 [EHK99]
% 117.32/117.33
% 117.32/117.33 % Status : Theorem
% 117.32/117.33 % Rating : 0.19 v8.1.0, 0.14 v7.5.0, 0.19 v7.4.0, 0.17 v7.2.0, 0.14 v7.1.0, 0.17 v7.0.0, 0.13 v6.4.0, 0.19 v6.3.0, 0.25 v6.2.0, 0.28 v6.1.0, 0.23 v6.0.0, 0.22 v5.5.0, 0.26 v5.4.0, 0.32 v5.3.0, 0.41 v5.2.0, 0.25 v5.1.0, 0.29 v5.0.0, 0.38 v4.1.0, 0.39 v4.0.0, 0.38 v3.7.0, 0.35 v3.5.0, 0.37 v3.4.0, 0.32 v3.3.0, 0.29 v3.2.0, 0.27 v3.1.0, 0.33 v2.4.0
% 117.32/117.33 % Syntax : Number of formulae : 37 ( 3 unt; 0 def)
% 117.32/117.33 % Number of atoms : 136 ( 17 equ)
% 117.32/117.33 % Maximal formula atoms : 12 ( 3 avg)
% 117.32/117.33 % Number of connectives : 109 ( 10 ~; 10 |; 42 &)
% 117.32/117.33 % ( 24 <=>; 23 =>; 0 <=; 0 <~>)
% 117.32/117.33 % Maximal formula depth : 12 ( 7 avg)
% 117.32/117.33 % Maximal term depth : 3 ( 1 avg)
% 117.32/117.33 % Number of predicates : 16 ( 15 usr; 0 prp; 1-4 aty)
% 117.32/117.33 % Number of functors : 5 ( 5 usr; 0 con; 1-2 aty)
% 117.32/117.33 % Number of variables : 123 ( 107 !; 16 ?)
% 117.32/117.34 % SPC : FOF_THM_RFO_SEQ
% 117.32/117.34
% 117.32/117.34 % Comments :
% 117.32/117.34 %--------------------------------------------------------------------------
% 117.32/117.34 %----Include simple curve axioms
% 117.32/117.34 include('Axioms/GEO004+0.ax').
% 117.32/117.34 %----Include axioms of betweenness for simple curves
% 117.32/117.34 include('Axioms/GEO004+1.ax').
% 117.32/117.34 %----Include oriented curve axioms
% 117.32/117.34 include('Axioms/GEO004+2.ax').
% 117.32/117.34 %----Include trajectory axioms
% 117.32/117.34 include('Axioms/GEO004+3.ax').
% 117.32/117.34 %--------------------------------------------------------------------------
% 117.32/117.34 fof(t14,conjecture,
% 117.32/117.34 ! [P,X,Y] :
% 117.32/117.34 ( connect(X,Y,P)
% 117.32/117.34 => ! [Q1,Q2] :
% 117.32/117.34 ( ( ordered_by(trajectory_of(Y),Q2,P)
% 117.32/117.34 & ordered_by(trajectory_of(X),P,Q1) )
% 117.32/117.34 => ~ once(at_the_same_time(at(X,Q1),at(Y,Q2))) ) ) ).
% 117.32/117.34
% 117.32/117.34 %--------------------------------------------------------------------------
% 117.32/117.34 %-------------------------------------------
% 117.32/117.34 % Proof found
% 117.32/117.34 % SZS status Theorem for theBenchmark
% 117.32/117.34 % SZS output start Proof
% 117.32/117.37 %ClaNum:202(EqnAxiom:100)
% 117.32/117.37 %VarNum:767(SingletonVarNum:276)
% 117.32/117.37 %MaxLitNum:12
% 117.32/117.37 %MaxfuncDepth:3
% 117.32/117.37 %SharedTerms:14
% 117.32/117.37 %goalClause: 104 105 106 107
% 117.32/117.37 %singleGoalClaCount:4
% 117.32/117.37 [104]P3(a16,a23,a17)
% 117.32/117.37 [105]P14(f32(a16),a17,a24)
% 117.32/117.37 [106]P14(f32(a23),a26,a17)
% 117.32/117.37 [107]P11(f3(f2(a16,a24),f2(a23,a26)))
% 117.32/117.37 [101]P1(f1(x1011))
% 117.32/117.37 [102]P2(f11(x1021),x1021)
% 117.32/117.37 [103]P13(f12(x1031),x1031)
% 117.32/117.37 [108]P4(x1081)+P7(f27(x1081),x1081)
% 117.32/117.37 [110]~P1(x1101)+P7(f31(x1101),x1101)
% 117.32/117.37 [117]~P11(x1171)+P11(f3(x1171,x1171))
% 117.32/117.37 [109]P1(x1091)+~P7(x1092,x1091)
% 117.32/117.37 [112]~P4(x1121)+~P7(x1122,x1121)
% 117.32/117.37 [113]~P7(x1131,x1132)+P8(x1131,x1132)
% 117.32/117.37 [114]~P2(x1141,x1142)+P8(x1141,x1142)
% 117.32/117.37 [115]~P13(x1151,x1152)+P10(x1151,x1152)
% 117.32/117.37 [116]~P9(x1161,x1162)+P10(x1161,x1162)
% 117.32/117.37 [119]~P2(x1191,x1192)+~P7(x1191,x1192)
% 117.32/117.37 [118]~P10(x1181,x1182)+P8(x1181,f1(x1182))
% 117.32/117.37 [122]~P7(x1222,x1221)+~E(f4(x1221,x1222),x1222)
% 117.32/117.37 [123]P10(x1231,x1232)+~P8(x1231,f1(x1232))
% 117.32/117.37 [125]P11(x1251)+~P11(f3(x1252,x1251))
% 117.32/117.37 [126]P11(x1261)+~P11(f3(x1261,x1262))
% 117.32/117.37 [127]P15(x1271,x1272)+P8(f13(x1272,x1271),x1271)
% 117.32/117.37 [133]~P10(x1332,f32(x1331))+P11(f2(x1331,x1332))
% 117.32/117.37 [134]~P7(x1342,x1341)+P7(f4(x1341,x1342),x1341)
% 117.32/117.37 [135]P10(x1351,f32(x1352))+~P11(f2(x1352,x1351))
% 117.32/117.37 [144]P15(x1441,x1442)+~P8(f13(x1442,x1441),x1442)
% 117.32/117.37 [146]~P11(f3(x1462,x1461))+P11(f3(x1461,x1462))
% 117.32/117.37 [158]~P2(x1581,x1582)+P12(x1581,f34(x1582,x1581),f5(x1582,x1581))
% 117.32/117.37 [149]~P2(x1492,x1491)+E(f33(f34(x1491,x1492),f5(x1491,x1492)),x1491)
% 117.32/117.37 [167]~P11(x1671)+P11(f3(x1671,f2(x1672,f22(x1671,x1672))))
% 117.32/117.37 [150]P8(x1501,x1502)+~P12(x1501,x1503,x1502)
% 117.32/117.37 [151]P8(x1511,x1512)+~P12(x1511,x1512,x1513)
% 117.32/117.37 [152]P10(x1521,x1522)+~P14(x1522,x1523,x1521)
% 117.32/117.37 [153]P10(x1531,x1532)+~P14(x1532,x1531,x1533)
% 117.32/117.37 [156]~P12(x1563,x1561,x1562)+E(f8(x1561,x1562),f33(x1561,x1562))
% 117.32/117.37 [170]~P11(f3(f3(x1701,x1702),x1703))+P11(f3(x1701,f3(x1702,x1703)))
% 117.32/117.37 [171]~P11(f3(x1711,f3(x1712,x1713)))+P11(f3(f3(x1711,x1712),x1713))
% 117.32/117.37 [174]~P3(x1741,x1743,x1742)+P11(f3(f2(x1741,x1742),f2(x1743,x1742)))
% 117.32/117.37 [179]P3(x1791,x1792,x1793)+~P11(f3(f2(x1791,x1793),f2(x1792,x1793)))
% 117.32/117.37 [183]~E(x1831,x1832)+~P5(x1833,x1831,x1834,x1832)
% 117.32/117.37 [194]~P5(x1942,x1943,x1944,x1941)+P7(x1941,f9(x1942,x1943,x1944,x1941))
% 117.32/117.37 [195]~P5(x1952,x1951,x1953,x1954)+P7(x1951,f9(x1952,x1951,x1953,x1954))
% 117.32/117.37 [196]~P5(x1962,x1963,x1961,x1964)+P2(x1961,f9(x1962,x1963,x1961,x1964))
% 117.32/117.37 [197]~P5(x1971,x1972,x1973,x1974)+P15(f9(x1971,x1972,x1973,x1974),x1971)
% 117.32/117.37 [199]~P6(x1994,x1991,x1992,x1993)+P5(f14(x1991,x1992,x1993,x1994),x1991,x1992,x1993)
% 117.32/117.37 [111]P1(x1111)+~P15(x1111,x1112)+E(x1111,x1112)
% 117.32/117.37 [124]P2(x1241,x1242)+~P8(x1241,x1242)+P7(x1241,x1242)
% 117.32/117.37 [131]~P10(x1311,x1312)+P13(x1311,x1312)+~E(f6(x1311,x1312),x1311)
% 117.32/117.37 [132]~P10(x1321,x1322)+P9(x1321,x1322)+~E(f10(x1321,x1322),x1321)
% 117.32/117.37 [138]~P8(x1381,x1382)+P7(x1381,x1382)+P8(x1381,f28(x1381,x1382))
% 117.32/117.37 [139]~P8(x1391,x1392)+P7(x1391,x1392)+P8(x1391,f29(x1391,x1392))
% 117.32/117.37 [140]~P8(x1401,x1402)+P7(x1401,x1402)+P15(f28(x1401,x1402),x1402)
% 117.32/117.37 [141]~P8(x1411,x1412)+P7(x1411,x1412)+P15(f29(x1411,x1412),x1412)
% 117.32/117.37 [142]~P10(x1421,x1422)+P13(x1421,x1422)+P10(f6(x1421,x1422),x1422)
% 117.32/117.37 [143]~P10(x1431,x1432)+P9(x1431,x1432)+P10(f10(x1431,x1432),x1432)
% 117.32/117.37 [147]E(x1471,x1472)+P8(f7(x1471,x1472),x1472)+P8(f7(x1471,x1472),x1471)
% 117.32/117.37 [148]P8(f18(x1481,x1482),x1481)+P10(f18(x1481,x1482),x1482)+E(x1481,f35(x1482))
% 117.32/117.37 [157]E(x1571,x1572)+~P8(f7(x1571,x1572),x1572)+~P8(f7(x1571,x1572),x1571)
% 117.32/117.37 [159]~P8(f18(x1591,x1592),x1591)+~P10(f18(x1591,x1592),x1592)+E(x1591,f35(x1592))
% 117.32/117.37 [160]~P8(x1601,x1602)+P7(x1601,x1602)+~P15(f28(x1601,x1602),f29(x1601,x1602))
% 117.32/117.37 [161]~P8(x1611,x1612)+P7(x1611,x1612)+~P15(f29(x1611,x1612),f28(x1611,x1612))
% 117.32/117.37 [165]~P10(x1651,x1652)+P13(x1651,x1652)+~P14(x1652,x1651,f6(x1651,x1652))
% 117.32/117.37 [166]~P10(x1661,x1662)+P9(x1661,x1662)+~P14(x1662,f10(x1661,x1662),x1661)
% 117.32/117.37 [172]E(x1721,x1722)+P14(x1722,f20(x1721,x1722),f21(x1721,x1722))+P14(x1721,f20(x1721,x1722),f21(x1721,x1722))
% 117.32/117.37 [180]E(x1801,x1802)+~P14(x1802,f20(x1801,x1802),f21(x1801,x1802))+~P14(x1801,f20(x1801,x1802),f21(x1801,x1802))
% 117.32/117.37 [128]~P8(x1281,x1283)+P8(x1281,x1282)+~P15(x1283,x1282)
% 117.32/117.37 [120]~P10(x1201,x1203)+P8(x1201,x1202)+~E(x1202,f35(x1203))
% 117.32/117.37 [121]~P8(x1211,x1213)+P10(x1211,x1212)+~E(x1213,f35(x1212))
% 117.32/117.37 [184]~P8(f25(x1841,x1842,x1843),x1843)+~P8(f25(x1841,x1842,x1843),x1841)+E(x1841,f33(x1842,x1843))
% 117.32/117.37 [185]~P8(f25(x1851,x1852,x1853),x1852)+~P8(f25(x1851,x1852,x1853),x1851)+E(x1851,f33(x1852,x1853))
% 117.32/117.37 [186]~P14(x1861,x1863,x1862)+~P14(x1861,x1864,x1863)+P6(x1861,x1862,x1863,x1864)
% 117.32/117.37 [187]~P14(x1871,x1873,x1874)+~P14(x1871,x1872,x1873)+P6(x1871,x1872,x1873,x1874)
% 117.32/117.37 [189]~P6(x1891,x1892,x1893,x1894)+P14(x1891,x1892,x1893)+P14(x1891,x1894,x1893)
% 117.32/117.37 [190]P14(x1901,x1903,x1902)+P14(x1901,x1902,x1903)+~P6(x1901,x1904,x1902,x1903)
% 117.32/117.37 [191]P14(x1911,x1913,x1912)+P14(x1911,x1912,x1913)+~P6(x1911,x1912,x1913,x1914)
% 117.32/117.37 [192]~P6(x1921,x1924,x1922,x1923)+P14(x1921,x1922,x1923)+P14(x1921,x1922,x1924)
% 117.32/117.37 [129]~P8(x1291,x1294)+P8(x1291,x1292)+~E(x1292,f33(x1293,x1294))
% 117.32/117.37 [130]~P8(x1301,x1303)+P8(x1301,x1302)+~E(x1302,f33(x1303,x1304))
% 117.32/117.37 [198]~P10(x1981,x1985)+~P6(x1985,x1982,x1983,x1984)+P8(x1981,f14(x1982,x1983,x1984,x1985))
% 117.32/117.37 [200]P10(x2001,x2002)+~P6(x2002,x2003,x2004,x2005)+~P8(x2001,f14(x2003,x2004,x2005,x2002))
% 117.32/117.37 [154]~P10(x1542,x1543)+~P9(x1541,x1543)+E(x1541,x1542)+P14(x1543,x1542,x1541)
% 117.32/117.37 [155]~P13(x1551,x1553)+~P10(x1552,x1553)+E(x1551,x1552)+P14(x1553,x1551,x1552)
% 117.32/117.37 [175]~P8(x1751,x1753)+~P8(x1751,x1752)+P12(x1751,x1752,x1753)+P8(f30(x1751,x1752,x1753),x1753)
% 117.32/117.37 [176]~P8(x1761,x1763)+~P8(x1761,x1762)+P12(x1761,x1762,x1763)+P8(f30(x1761,x1762,x1763),x1762)
% 117.32/117.37 [182]P8(f25(x1821,x1822,x1823),x1823)+P8(f25(x1821,x1822,x1823),x1822)+P8(f25(x1821,x1822,x1823),x1821)+E(x1821,f33(x1822,x1823))
% 117.32/117.37 [163]~P8(x1631,x1632)+P7(x1631,x1632)+~P12(x1634,x1633,x1632)+~P8(x1631,x1633)
% 117.32/117.37 [164]~P8(x1641,x1642)+P7(x1641,x1642)+~P12(x1644,x1642,x1643)+~P8(x1641,x1643)
% 117.32/117.37 [137]~P8(x1371,x1374)+P8(x1371,x1372)+P8(x1371,x1373)+~E(x1374,f33(x1373,x1372))
% 117.32/117.37 [201]~P5(x2015,x2012,x2013,x2014)+P6(x2011,x2012,x2013,x2014)+P8(f15(x2012,x2013,x2014,x2011,x2015),x2015)+P10(f15(x2012,x2013,x2014,x2011,x2015),x2011)
% 117.32/117.37 [202]P6(x2021,x2022,x2023,x2024)+~P5(x2025,x2022,x2023,x2024)+~P8(f15(x2022,x2023,x2024,x2021,x2025),x2025)+~P10(f15(x2022,x2023,x2024,x2021,x2025),x2021)
% 117.32/117.37 [193]~P14(f32(x1931),x1932,x1933)+~P14(f32(x1934),x1935,x1936)+~P11(f3(f2(x1934,x1936),f2(x1931,x1932)))+~P11(f3(f2(x1934,x1935),f2(x1931,x1933)))
% 117.32/117.37 [173]~P1(x1733)+~P8(x1732,x1733)+~P8(x1731,x1733)+E(x1731,x1732)+P14(f19(x1731,x1732,x1733),x1731,x1732)
% 117.32/117.37 [188]~P8(x1881,x1883)+~P8(x1881,x1882)+P12(x1881,x1882,x1883)+~P7(f30(x1881,x1882,x1883),x1883)+~P7(f30(x1881,x1882,x1883),x1882)
% 117.32/117.37 [168]~P4(x1684)+~P7(x1681,x1682)+P12(x1681,x1682,x1683)+~P12(x1685,x1682,x1683)+~E(x1684,f33(x1682,x1683))
% 117.32/117.37 [136]E(x1363,x1361)+~P7(x1361,x1364)+~P7(x1363,x1364)+E(x1361,x1362)+E(x1363,x1362)+~P7(x1362,x1364)
% 117.32/117.37 [169]~P1(x1694)+~P8(x1692,x1694)+~P8(x1691,x1694)+~P8(x1693,x1694)+E(x1691,x1692)+P10(x1693,f19(x1691,x1692,x1694))
% 117.32/117.37 [178]~P1(x1784)+~P8(x1782,x1784)+~P8(x1781,x1784)+E(x1781,x1782)+P8(x1783,x1784)+~P10(x1783,f19(x1781,x1782,x1784))
% 117.32/117.37 [181]~P7(x1812,x1815)+~P7(x1811,x1815)+~P2(x1814,x1815)+E(x1811,x1812)+P5(x1813,x1811,x1814,x1812)+~P15(x1815,x1813)
% 117.32/117.37 [162]P15(x1622,x1621)+~P15(x1622,x1623)+~P8(x1624,x1622)+~P7(x1624,x1623)+P15(x1621,x1622)+~P15(x1621,x1623)+~P8(x1624,x1621)
% 117.32/117.37 [177]P15(x1772,x1771)+P15(x1772,x1773)+P15(x1773,x1771)+P15(x1773,x1772)+~P15(x1772,x1774)+~P15(x1773,x1774)+~P7(x1775,x1772)+~P7(x1775,x1773)+P15(x1771,x1772)+P15(x1771,x1773)+~P15(x1771,x1774)+~P7(x1775,x1771)
% 117.32/117.37 %EqnAxiom
% 117.32/117.37 [1]E(x11,x11)
% 117.32/117.37 [2]E(x22,x21)+~E(x21,x22)
% 117.32/117.37 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 117.32/117.37 [4]~E(x41,x42)+E(f1(x41),f1(x42))
% 117.32/117.37 [5]~E(x51,x52)+E(f11(x51),f11(x52))
% 117.32/117.37 [6]~E(x61,x62)+E(f12(x61),f12(x62))
% 117.32/117.37 [7]~E(x71,x72)+E(f32(x71),f32(x72))
% 117.32/117.37 [8]~E(x81,x82)+E(f15(x81,x83,x84,x85,x86),f15(x82,x83,x84,x85,x86))
% 117.32/117.37 [9]~E(x91,x92)+E(f15(x93,x91,x94,x95,x96),f15(x93,x92,x94,x95,x96))
% 117.32/117.37 [10]~E(x101,x102)+E(f15(x103,x104,x101,x105,x106),f15(x103,x104,x102,x105,x106))
% 117.32/117.37 [11]~E(x111,x112)+E(f15(x113,x114,x115,x111,x116),f15(x113,x114,x115,x112,x116))
% 117.32/117.37 [12]~E(x121,x122)+E(f15(x123,x124,x125,x126,x121),f15(x123,x124,x125,x126,x122))
% 117.32/117.37 [13]~E(x131,x132)+E(f2(x131,x133),f2(x132,x133))
% 117.32/117.37 [14]~E(x141,x142)+E(f2(x143,x141),f2(x143,x142))
% 117.32/117.37 [15]~E(x151,x152)+E(f9(x151,x153,x154,x155),f9(x152,x153,x154,x155))
% 117.32/117.37 [16]~E(x161,x162)+E(f9(x163,x161,x164,x165),f9(x163,x162,x164,x165))
% 117.32/117.37 [17]~E(x171,x172)+E(f9(x173,x174,x171,x175),f9(x173,x174,x172,x175))
% 117.32/117.37 [18]~E(x181,x182)+E(f9(x183,x184,x185,x181),f9(x183,x184,x185,x182))
% 117.32/117.37 [19]~E(x191,x192)+E(f3(x191,x193),f3(x192,x193))
% 117.32/117.37 [20]~E(x201,x202)+E(f3(x203,x201),f3(x203,x202))
% 117.32/117.37 [21]~E(x211,x212)+E(f27(x211),f27(x212))
% 117.32/117.37 [22]~E(x221,x222)+E(f31(x221),f31(x222))
% 117.32/117.37 [23]~E(x231,x232)+E(f25(x231,x233,x234),f25(x232,x233,x234))
% 117.32/117.37 [24]~E(x241,x242)+E(f25(x243,x241,x244),f25(x243,x242,x244))
% 117.32/117.37 [25]~E(x251,x252)+E(f25(x253,x254,x251),f25(x253,x254,x252))
% 117.32/117.37 [26]~E(x261,x262)+E(f21(x261,x263),f21(x262,x263))
% 117.32/117.37 [27]~E(x271,x272)+E(f21(x273,x271),f21(x273,x272))
% 117.32/117.37 [28]~E(x281,x282)+E(f35(x281),f35(x282))
% 117.32/117.37 [29]~E(x291,x292)+E(f19(x291,x293,x294),f19(x292,x293,x294))
% 117.32/117.37 [30]~E(x301,x302)+E(f19(x303,x301,x304),f19(x303,x302,x304))
% 117.32/117.37 [31]~E(x311,x312)+E(f19(x313,x314,x311),f19(x313,x314,x312))
% 117.32/117.37 [32]~E(x321,x322)+E(f4(x321,x323),f4(x322,x323))
% 117.32/117.37 [33]~E(x331,x332)+E(f4(x333,x331),f4(x333,x332))
% 117.32/117.37 [34]~E(x341,x342)+E(f33(x341,x343),f33(x342,x343))
% 117.32/117.37 [35]~E(x351,x352)+E(f33(x353,x351),f33(x353,x352))
% 117.32/117.37 [36]~E(x361,x362)+E(f14(x361,x363,x364,x365),f14(x362,x363,x364,x365))
% 117.32/117.37 [37]~E(x371,x372)+E(f14(x373,x371,x374,x375),f14(x373,x372,x374,x375))
% 117.32/117.37 [38]~E(x381,x382)+E(f14(x383,x384,x381,x385),f14(x383,x384,x382,x385))
% 117.32/117.37 [39]~E(x391,x392)+E(f14(x393,x394,x395,x391),f14(x393,x394,x395,x392))
% 117.32/117.37 [40]~E(x401,x402)+E(f20(x401,x403),f20(x402,x403))
% 117.32/117.37 [41]~E(x411,x412)+E(f20(x413,x411),f20(x413,x412))
% 117.32/117.37 [42]~E(x421,x422)+E(f13(x421,x423),f13(x422,x423))
% 117.32/117.37 [43]~E(x431,x432)+E(f13(x433,x431),f13(x433,x432))
% 117.32/117.37 [44]~E(x441,x442)+E(f22(x441,x443),f22(x442,x443))
% 117.32/117.37 [45]~E(x451,x452)+E(f22(x453,x451),f22(x453,x452))
% 117.32/117.37 [46]~E(x461,x462)+E(f10(x461,x463),f10(x462,x463))
% 117.32/117.37 [47]~E(x471,x472)+E(f10(x473,x471),f10(x473,x472))
% 117.32/117.37 [48]~E(x481,x482)+E(f6(x481,x483),f6(x482,x483))
% 117.32/117.37 [49]~E(x491,x492)+E(f6(x493,x491),f6(x493,x492))
% 117.32/117.37 [50]~E(x501,x502)+E(f7(x501,x503),f7(x502,x503))
% 117.32/117.37 [51]~E(x511,x512)+E(f7(x513,x511),f7(x513,x512))
% 117.32/117.37 [52]~E(x521,x522)+E(f30(x521,x523,x524),f30(x522,x523,x524))
% 117.32/117.37 [53]~E(x531,x532)+E(f30(x533,x531,x534),f30(x533,x532,x534))
% 117.32/117.37 [54]~E(x541,x542)+E(f30(x543,x544,x541),f30(x543,x544,x542))
% 117.32/117.37 [55]~E(x551,x552)+E(f18(x551,x553),f18(x552,x553))
% 117.32/117.37 [56]~E(x561,x562)+E(f18(x563,x561),f18(x563,x562))
% 117.32/117.37 [57]~E(x571,x572)+E(f5(x571,x573),f5(x572,x573))
% 117.32/117.37 [58]~E(x581,x582)+E(f5(x583,x581),f5(x583,x582))
% 117.32/117.37 [59]~E(x591,x592)+E(f34(x591,x593),f34(x592,x593))
% 117.32/117.37 [60]~E(x601,x602)+E(f34(x603,x601),f34(x603,x602))
% 117.32/117.37 [61]~E(x611,x612)+E(f8(x611,x613),f8(x612,x613))
% 117.32/117.37 [62]~E(x621,x622)+E(f8(x623,x621),f8(x623,x622))
% 117.32/117.37 [63]~E(x631,x632)+E(f28(x631,x633),f28(x632,x633))
% 117.32/117.37 [64]~E(x641,x642)+E(f28(x643,x641),f28(x643,x642))
% 117.32/117.37 [65]~E(x651,x652)+E(f29(x651,x653),f29(x652,x653))
% 117.32/117.37 [66]~E(x661,x662)+E(f29(x663,x661),f29(x663,x662))
% 117.32/117.37 [67]~P1(x671)+P1(x672)+~E(x671,x672)
% 117.32/117.37 [68]P2(x682,x683)+~E(x681,x682)+~P2(x681,x683)
% 117.32/117.37 [69]P2(x693,x692)+~E(x691,x692)+~P2(x693,x691)
% 117.32/117.37 [70]P13(x702,x703)+~E(x701,x702)+~P13(x701,x703)
% 117.32/117.37 [71]P13(x713,x712)+~E(x711,x712)+~P13(x713,x711)
% 117.32/117.37 [72]P3(x722,x723,x724)+~E(x721,x722)+~P3(x721,x723,x724)
% 117.32/117.37 [73]P3(x733,x732,x734)+~E(x731,x732)+~P3(x733,x731,x734)
% 117.32/117.37 [74]P3(x743,x744,x742)+~E(x741,x742)+~P3(x743,x744,x741)
% 117.32/117.37 [75]P14(x752,x753,x754)+~E(x751,x752)+~P14(x751,x753,x754)
% 117.32/117.37 [76]P14(x763,x762,x764)+~E(x761,x762)+~P14(x763,x761,x764)
% 117.32/117.37 [77]P14(x773,x774,x772)+~E(x771,x772)+~P14(x773,x774,x771)
% 117.32/117.37 [78]P5(x782,x783,x784,x785)+~E(x781,x782)+~P5(x781,x783,x784,x785)
% 117.32/117.37 [79]P5(x793,x792,x794,x795)+~E(x791,x792)+~P5(x793,x791,x794,x795)
% 117.32/117.37 [80]P5(x803,x804,x802,x805)+~E(x801,x802)+~P5(x803,x804,x801,x805)
% 117.32/117.37 [81]P5(x813,x814,x815,x812)+~E(x811,x812)+~P5(x813,x814,x815,x811)
% 117.32/117.37 [82]~P11(x821)+P11(x822)+~E(x821,x822)
% 117.32/117.37 [83]~P4(x831)+P4(x832)+~E(x831,x832)
% 117.32/117.37 [84]P7(x842,x843)+~E(x841,x842)+~P7(x841,x843)
% 117.32/117.37 [85]P7(x853,x852)+~E(x851,x852)+~P7(x853,x851)
% 117.32/117.37 [86]P10(x862,x863)+~E(x861,x862)+~P10(x861,x863)
% 117.32/117.37 [87]P10(x873,x872)+~E(x871,x872)+~P10(x873,x871)
% 117.32/117.37 [88]P15(x882,x883)+~E(x881,x882)+~P15(x881,x883)
% 117.32/117.37 [89]P15(x893,x892)+~E(x891,x892)+~P15(x893,x891)
% 117.32/117.37 [90]P8(x902,x903)+~E(x901,x902)+~P8(x901,x903)
% 117.32/117.37 [91]P8(x913,x912)+~E(x911,x912)+~P8(x913,x911)
% 117.32/117.37 [92]P6(x922,x923,x924,x925)+~E(x921,x922)+~P6(x921,x923,x924,x925)
% 117.32/117.37 [93]P6(x933,x932,x934,x935)+~E(x931,x932)+~P6(x933,x931,x934,x935)
% 117.32/117.37 [94]P6(x943,x944,x942,x945)+~E(x941,x942)+~P6(x943,x944,x941,x945)
% 117.32/117.37 [95]P6(x953,x954,x955,x952)+~E(x951,x952)+~P6(x953,x954,x955,x951)
% 117.32/117.37 [96]P12(x962,x963,x964)+~E(x961,x962)+~P12(x961,x963,x964)
% 117.32/117.37 [97]P12(x973,x972,x974)+~E(x971,x972)+~P12(x973,x971,x974)
% 117.32/117.37 [98]P12(x983,x984,x982)+~E(x981,x982)+~P12(x983,x984,x981)
% 117.32/117.37 [99]P9(x992,x993)+~E(x991,x992)+~P9(x991,x993)
% 117.32/117.37 [100]P9(x1003,x1002)+~E(x1001,x1002)+~P9(x1003,x1001)
% 117.32/117.37
% 117.32/117.37 %-------------------------------------------
% 117.32/117.41 cnf(203,plain,
% 117.32/117.41 (~P10(x2031,x2032)+P8(x2031,f35(x2032))),
% 117.32/117.41 inference(equality_inference,[],[120])).
% 117.32/117.41 cnf(204,plain,
% 117.32/117.41 (~P8(x2041,f35(x2042))+P10(x2041,x2042)),
% 117.32/117.41 inference(equality_inference,[],[121])).
% 117.32/117.41 cnf(205,plain,
% 117.32/117.41 (~P8(x2051,x2052)+P8(x2051,f33(x2053,x2052))),
% 117.32/117.41 inference(equality_inference,[],[129])).
% 117.32/117.41 cnf(206,plain,
% 117.32/117.41 (~P8(x2061,x2062)+P8(x2061,f33(x2062,x2063))),
% 117.32/117.41 inference(equality_inference,[],[130])).
% 117.32/117.41 cnf(207,plain,
% 117.32/117.41 (~P8(x2071,f33(x2072,x2073))+P8(x2071,x2073)+P8(x2071,x2072)),
% 117.32/117.41 inference(equality_inference,[],[137])).
% 117.32/117.41 cnf(209,plain,
% 117.32/117.41 (~P5(x2092,x2091,x2093,x2091)),
% 117.32/117.41 inference(equality_inference,[],[183])).
% 117.32/117.41 cnf(210,plain,
% 117.32/117.41 (P11(f2(a23,a26))),
% 117.32/117.41 inference(scs_inference,[],[107,125])).
% 117.32/117.41 cnf(212,plain,
% 117.32/117.41 (P11(f2(a16,a24))),
% 117.32/117.41 inference(scs_inference,[],[107,125,126])).
% 117.32/117.41 cnf(214,plain,
% 117.32/117.41 (P10(a26,f32(a23))),
% 117.32/117.41 inference(scs_inference,[],[107,125,126,135])).
% 117.32/117.41 cnf(216,plain,
% 117.32/117.41 (~P6(x2161,x2162,x2163,x2162)),
% 117.32/117.41 inference(scs_inference,[],[107,209,125,126,135,199])).
% 117.32/117.41 cnf(221,plain,
% 117.32/117.41 (P3(x2211,a23,a17)+~E(a16,x2211)),
% 117.32/117.41 inference(scs_inference,[],[104,105,107,209,125,126,135,199,186,72])).
% 117.32/117.41 cnf(225,plain,
% 117.32/117.41 (P14(f32(a16),x2251,a24)+~E(a17,x2251)),
% 117.32/117.41 inference(scs_inference,[],[104,105,107,209,125,126,135,199,186,72,73,74,75,76])).
% 117.32/117.41 cnf(226,plain,
% 117.32/117.41 (P14(f32(a16),a17,x2261)+~E(a24,x2261)),
% 117.32/117.41 inference(scs_inference,[],[104,105,107,209,125,126,135,199,186,72,73,74,75,76,77])).
% 117.32/117.41 cnf(233,plain,
% 117.32/117.41 (P10(a24,f32(a16))),
% 117.32/117.41 inference(scs_inference,[],[212,135])).
% 117.32/117.41 cnf(235,plain,
% 117.32/117.41 (~P14(f32(a23),a17,a26)),
% 117.32/117.41 inference(scs_inference,[],[106,212,216,135,187])).
% 117.32/117.41 cnf(238,plain,
% 117.32/117.41 (P10(x2381,f32(a23))+~E(a26,x2381)),
% 117.32/117.41 inference(scs_inference,[],[106,212,216,214,135,187,86])).
% 117.32/117.41 cnf(240,plain,
% 117.32/117.41 (P2(x2401,x2402)+~E(f11(x2402),x2401)),
% 117.32/117.41 inference(scs_inference,[],[106,212,216,102,214,135,187,86,87,68])).
% 117.32/117.41 cnf(241,plain,
% 117.32/117.41 (P2(f11(x2411),x2412)+~E(x2411,x2412)),
% 117.32/117.41 inference(scs_inference,[],[106,212,216,102,214,135,187,86,87,68,69])).
% 117.32/117.41 cnf(242,plain,
% 117.32/117.41 (P13(x2421,x2422)+~E(f12(x2422),x2421)),
% 117.32/117.41 inference(scs_inference,[],[106,212,216,102,214,103,135,187,86,87,68,69,70])).
% 117.32/117.41 cnf(243,plain,
% 117.32/117.41 (P13(f12(x2431),x2432)+~E(x2431,x2432)),
% 117.32/117.41 inference(scs_inference,[],[106,212,216,102,214,103,135,187,86,87,68,69,70,71])).
% 117.32/117.41 cnf(256,plain,
% 117.32/117.41 (P14(f32(a23),a26,x2561)+~E(a17,x2561)),
% 117.32/117.41 inference(scs_inference,[],[106,233,87,77])).
% 117.32/117.41 cnf(260,plain,
% 117.32/117.41 (P10(x2601,f32(a16))+~E(a24,x2601)),
% 117.32/117.41 inference(scs_inference,[],[233,86])).
% 117.32/117.41 cnf(263,plain,
% 117.32/117.41 (P14(f32(a23),x2631,a17)+~E(a26,x2631)),
% 117.32/117.41 inference(scs_inference,[],[106,76])).
% 117.32/117.41 cnf(273,plain,
% 117.32/117.41 (~P7(x2731,x2732)+P7(f31(x2732),x2732)),
% 117.32/117.41 inference(scs_inference,[],[109,110])).
% 117.32/117.41 cnf(274,plain,
% 117.32/117.41 (~P7(x2741,x2742)+P7(f27(x2742),x2742)),
% 117.32/117.41 inference(scs_inference,[],[112,108])).
% 117.32/117.41 cnf(275,plain,
% 117.32/117.41 (E(x2751,f33(f34(x2751,f11(x2751)),f5(x2751,f11(x2751))))),
% 117.32/117.41 inference(scs_inference,[],[102,2,149])).
% 117.32/117.41 cnf(276,plain,
% 117.32/117.41 (P14(f32(a16),f33(f34(a17,f11(a17)),f5(a17,f11(a17))),a24)),
% 117.32/117.41 inference(scs_inference,[],[275,225])).
% 117.32/117.41 cnf(277,plain,
% 117.32/117.41 (E(x2771,f33(f34(x2771,f11(x2771)),f5(x2771,f11(x2771))))),
% 117.32/117.41 inference(rename_variables,[],[275])).
% 117.32/117.41 cnf(278,plain,
% 117.32/117.41 (P14(f32(a16),a17,f33(f34(a24,f11(a24)),f5(a24,f11(a24))))),
% 117.32/117.41 inference(scs_inference,[],[275,277,225,226])).
% 117.32/117.41 cnf(279,plain,
% 117.32/117.41 (E(x2791,f33(f34(x2791,f11(x2791)),f5(x2791,f11(x2791))))),
% 117.32/117.41 inference(rename_variables,[],[275])).
% 117.32/117.41 cnf(280,plain,
% 117.32/117.41 (P14(f32(a23),a26,f33(f34(a17,f11(a17)),f5(a17,f11(a17))))),
% 117.32/117.41 inference(scs_inference,[],[275,277,279,225,226,256])).
% 117.32/117.41 cnf(281,plain,
% 117.32/117.41 (E(x2811,f33(f34(x2811,f11(x2811)),f5(x2811,f11(x2811))))),
% 117.32/117.41 inference(rename_variables,[],[275])).
% 117.32/117.41 cnf(282,plain,
% 117.32/117.41 (P14(f32(a23),f33(f34(a26,f11(a26)),f5(a26,f11(a26))),a17)),
% 117.32/117.41 inference(scs_inference,[],[275,277,279,281,225,226,256,263])).
% 117.32/117.41 cnf(283,plain,
% 117.32/117.41 (E(x2831,f33(f34(x2831,f11(x2831)),f5(x2831,f11(x2831))))),
% 117.32/117.41 inference(rename_variables,[],[275])).
% 117.32/117.41 cnf(284,plain,
% 117.32/117.41 (P10(f33(f34(a26,f11(a26)),f5(a26,f11(a26))),f32(a23))),
% 117.32/117.41 inference(scs_inference,[],[275,277,279,281,283,225,226,256,263,238])).
% 117.32/117.41 cnf(285,plain,
% 117.32/117.41 (E(x2851,f33(f34(x2851,f11(x2851)),f5(x2851,f11(x2851))))),
% 117.32/117.41 inference(rename_variables,[],[275])).
% 117.32/117.41 cnf(287,plain,
% 117.32/117.41 (E(x2871,f33(f34(x2871,f11(x2871)),f5(x2871,f11(x2871))))),
% 117.32/117.41 inference(rename_variables,[],[275])).
% 117.32/117.41 cnf(288,plain,
% 117.32/117.41 (E(f33(f34(x2881,f11(x2881)),f5(x2881,f11(x2881))),x2881)),
% 117.32/117.41 inference(scs_inference,[],[275,277,279,281,283,285,287,225,226,256,263,238,260,2])).
% 117.32/117.41 cnf(291,plain,
% 117.32/117.41 (P2(f11(x2911),f33(f34(x2911,f11(x2911)),f5(x2911,f11(x2911))))),
% 117.32/117.41 inference(scs_inference,[],[275,277,279,281,283,285,287,225,226,256,263,238,260,2,183,241])).
% 117.32/117.41 cnf(292,plain,
% 117.32/117.41 (P13(f12(x2921),f33(f34(x2921,f11(x2921)),f5(x2921,f11(x2921))))),
% 117.32/117.41 inference(scs_inference,[],[275,277,279,281,283,285,287,225,226,256,263,238,260,2,183,241,243])).
% 117.32/117.41 cnf(294,plain,
% 117.32/117.41 (E(x2941,f33(f34(x2941,f11(x2941)),f5(x2941,f11(x2941))))),
% 117.32/117.41 inference(rename_variables,[],[275])).
% 117.32/117.41 cnf(296,plain,
% 117.32/117.41 (E(x2961,f33(f34(x2961,f11(x2961)),f5(x2961,f11(x2961))))),
% 117.32/117.41 inference(rename_variables,[],[275])).
% 117.32/117.41 cnf(298,plain,
% 117.32/117.41 (E(x2981,f33(f34(x2981,f11(x2981)),f5(x2981,f11(x2981))))),
% 117.32/117.41 inference(rename_variables,[],[275])).
% 117.32/117.41 cnf(300,plain,
% 117.32/117.41 (~P8(x3001,f5(x3002,f11(x3002)))+P8(x3001,x3002)),
% 117.32/117.41 inference(scs_inference,[],[104,275,277,279,281,283,285,287,294,296,298,225,226,256,263,238,260,2,183,241,243,73,72,74,82,129])).
% 117.32/117.41 cnf(302,plain,
% 117.32/117.41 (~P8(x3021,f34(x3022,f11(x3022)))+P8(x3021,x3022)),
% 117.32/117.41 inference(scs_inference,[],[104,275,277,279,281,283,285,287,294,296,298,225,226,256,263,238,260,2,183,241,243,73,72,74,82,129,130])).
% 117.32/117.41 cnf(313,plain,
% 117.32/117.41 (~P7(x3131,f1(x3132))+P10(x3131,x3132)),
% 117.32/117.41 inference(scs_inference,[],[113,123])).
% 117.32/117.41 cnf(318,plain,
% 117.32/117.41 (~P1(f33(f34(x3181,f11(x3181)),f5(x3181,f11(x3181))))+P1(x3181)),
% 117.32/117.41 inference(scs_inference,[],[288,183,83,82,67])).
% 117.32/117.41 cnf(323,plain,
% 117.32/117.41 (~P4(x3231)+P4(f33(f34(x3231,f11(x3231)),f5(x3231,f11(x3231))))),
% 117.32/117.41 inference(scs_inference,[],[275,83])).
% 117.32/117.41 cnf(349,plain,
% 117.32/117.41 (P10(f11(f35(x3491)),x3491)),
% 117.32/117.41 inference(scs_inference,[],[102,114,204])).
% 117.32/117.41 cnf(380,plain,
% 117.32/117.41 (P8(f12(x3801),f1(x3801))),
% 117.32/117.41 inference(scs_inference,[],[103,115,118])).
% 117.32/117.41 cnf(381,plain,
% 117.32/117.41 (P10(f12(x3811),x3811)),
% 117.32/117.41 inference(scs_inference,[],[380,123])).
% 117.32/117.41 cnf(595,plain,
% 117.32/117.41 (P11(f3(f2(a23,a26),f2(a23,a26)))),
% 117.32/117.41 inference(scs_inference,[],[107,117,125])).
% 117.32/117.41 cnf(596,plain,
% 117.32/117.41 (P3(a23,a23,a26)),
% 117.32/117.41 inference(scs_inference,[],[595,179])).
% 117.32/117.41 cnf(599,plain,
% 117.32/117.41 (E(x5991,f33(f34(x5991,f11(x5991)),f5(x5991,f11(x5991))))),
% 117.32/117.41 inference(rename_variables,[],[275])).
% 117.32/117.41 cnf(601,plain,
% 117.32/117.41 (E(x6011,f33(f34(x6011,f11(x6011)),f5(x6011,f11(x6011))))),
% 117.32/117.41 inference(rename_variables,[],[275])).
% 117.32/117.41 cnf(604,plain,
% 117.32/117.41 (~P14(f32(a23),a26,a26)),
% 117.32/117.41 inference(scs_inference,[],[595,275,599,601,179,72,73,74,193])).
% 117.32/117.41 cnf(606,plain,
% 117.32/117.41 (~P6(f32(a23),a26,a26,x6061)),
% 117.32/117.41 inference(scs_inference,[],[595,275,599,601,179,72,73,74,193,191])).
% 117.32/117.41 cnf(608,plain,
% 117.32/117.41 (~P6(f32(a23),x6081,a26,a26)),
% 117.32/117.41 inference(scs_inference,[],[595,275,599,601,179,72,73,74,193,191,190])).
% 117.32/117.41 cnf(611,plain,
% 117.32/117.41 (~P13(a17,f32(a23))),
% 117.32/117.41 inference(scs_inference,[],[106,235,595,275,599,601,214,179,72,73,74,193,191,190,77,155])).
% 117.32/117.41 cnf(613,plain,
% 117.32/117.41 (~E(a17,f33(f34(a26,f11(a26)),f5(a26,f11(a26))))),
% 117.32/117.41 inference(scs_inference,[],[106,235,595,275,599,601,288,214,179,72,73,74,193,191,190,77,155,3])).
% 117.32/117.41 cnf(617,plain,
% 117.32/117.41 (~E(f12(f32(a23)),a17)),
% 117.32/117.41 inference(scs_inference,[],[106,235,595,275,599,601,288,214,103,179,72,73,74,193,191,190,77,155,3,111,70])).
% 117.32/117.41 cnf(622,plain,
% 117.32/117.41 (~E(f33(f34(a17,f11(a17)),f5(a17,f11(a17))),a26)),
% 117.32/117.41 inference(scs_inference,[],[280,604,77])).
% 117.32/117.41 cnf(625,plain,
% 117.32/117.41 (P14(f32(a23),f12(f32(a23)),a17)+~P10(a17,f32(a23))),
% 117.32/117.41 inference(scs_inference,[],[280,604,613,103,617,77,111,182,154,155])).
% 117.32/117.41 cnf(789,plain,
% 117.32/117.41 (~P12(x7891,x7892,x7893)+P8(x7891,f33(x7894,x7892))),
% 117.32/117.41 inference(scs_inference,[],[151,205])).
% 117.32/117.41 cnf(835,plain,
% 117.32/117.41 (P8(a17,f35(f32(a23)))),
% 117.32/117.41 inference(scs_inference,[],[106,152,203])).
% 117.32/117.41 cnf(1066,plain,
% 117.32/117.41 (~P7(x10661,x10662)+~P2(f31(x10662),x10662)),
% 117.32/117.41 inference(scs_inference,[],[273,119])).
% 117.32/117.41 cnf(1310,plain,
% 117.32/117.41 (~E(f11(x13101),f31(x13101))+~P7(x13102,x13101)),
% 117.32/117.41 inference(scs_inference,[],[1066,240])).
% 117.32/117.41 cnf(1676,plain,
% 117.32/117.41 (P7(f4(f1(x16761),f31(f1(x16761))),f1(x16761))),
% 117.32/117.41 inference(scs_inference,[],[101,134,110])).
% 117.32/117.41 cnf(1679,plain,
% 117.32/117.41 (~E(f11(f1(x16791)),f4(f1(x16791),f31(f1(x16791))))),
% 117.32/117.41 inference(scs_inference,[],[102,1676,119,68])).
% 117.32/117.41 cnf(1688,plain,
% 117.32/117.41 (P14(x16881,a17,f12(f32(a23)))+~P10(a17,x16881)+~P9(f12(f32(a23)),x16881)),
% 117.32/117.41 inference(scs_inference,[],[613,288,617,1679,1676,154])).
% 117.32/117.41 cnf(1810,plain,
% 117.32/117.41 (~E(f31(f1(x18101)),f11(f1(x18101)))),
% 117.32/117.41 inference(scs_inference,[],[1676,1310,2])).
% 117.32/117.41 cnf(2000,plain,
% 117.32/117.41 (P8(f11(x20001),f33(x20002,f34(x20001,f11(x20001))))),
% 117.32/117.41 inference(scs_inference,[],[102,789,158])).
% 117.32/117.41 cnf(2267,plain,
% 117.32/117.41 (E(f4(f25(f33(f34(x22671,f11(x22671)),f5(x22671,f11(x22671))),x22672,x22673),x22674),f4(f25(x22671,x22672,x22673),x22674))),
% 117.32/117.41 inference(scs_inference,[],[288,32,23])).
% 117.32/117.41 cnf(3287,plain,
% 117.32/117.41 (P11(x32871)+~P11(f3(x32872,f3(x32873,x32871)))),
% 117.32/117.41 inference(scs_inference,[],[171,125])).
% 117.32/117.41 cnf(3318,plain,
% 117.32/117.41 (~P11(f3(x33181,f3(x33182,f3(f2(a16,a17),f2(a23,a17)))))),
% 117.32/117.41 inference(scs_inference,[],[107,106,105,3287,193])).
% 117.32/117.41 cnf(3349,plain,
% 117.32/117.41 (P11(f3(f2(f33(f34(a16,f11(a16)),f5(a16,f11(a16))),a17),f2(a23,a17)))),
% 117.32/117.41 inference(scs_inference,[],[275,174,221])).
% 117.32/117.41 cnf(3535,plain,
% 117.32/117.41 (~P1(f33(f34(x35351,f11(x35351)),f5(x35351,f11(x35351))))+P7(f31(x35351),x35351)),
% 117.32/117.41 inference(scs_inference,[],[318,110])).
% 117.32/117.41 cnf(3566,plain,
% 117.32/117.41 (~P4(x35661)+~P7(x35662,f33(f34(x35661,f11(x35661)),f5(x35661,f11(x35661))))),
% 117.32/117.41 inference(scs_inference,[],[323,112])).
% 117.32/117.41 cnf(3814,plain,
% 117.32/117.41 (~P4(f1(x38141))),
% 117.32/117.41 inference(scs_inference,[],[1676,275,3566,85])).
% 117.32/117.41 cnf(4388,plain,
% 117.32/117.41 (~P1(f33(f34(x43881,f11(x43881)),f5(x43881,f11(x43881))))+~P4(x43881)),
% 117.32/117.41 inference(scs_inference,[],[3535,112])).
% 117.32/117.41 cnf(4419,plain,
% 117.32/117.41 (~P1(f33(f34(x44191,f11(x44191)),f5(x44191,f11(x44191))))+P7(f27(x44191),x44191)),
% 117.32/117.41 inference(scs_inference,[],[4388,108])).
% 117.32/117.41 cnf(4566,plain,
% 117.32/117.41 (~P14(f32(a23),f33(f34(a17,f11(a17)),f5(a17,f11(a17))),a26)),
% 117.32/117.41 inference(scs_inference,[],[280,216,186])).
% 117.32/117.41 cnf(4569,plain,
% 117.32/117.41 (~P13(f33(f34(a17,f11(a17)),f5(a17,f11(a17))),f32(a23))),
% 117.32/117.41 inference(scs_inference,[],[280,622,216,214,186,155])).
% 117.32/117.41 cnf(4607,plain,
% 117.32/117.41 (P8(f27(x46071),x46071)+~P1(f33(f34(x46071,f11(x46071)),f5(x46071,f11(x46071))))),
% 117.32/117.41 inference(scs_inference,[],[4419,113])).
% 117.32/117.41 cnf(4638,plain,
% 117.32/117.41 (P8(f27(f1(x46381)),f1(x46381))),
% 117.32/117.41 inference(scs_inference,[],[275,101,4607,67])).
% 117.32/117.41 cnf(4639,plain,
% 117.32/117.41 (P10(f27(f1(x46391)),x46391)),
% 117.32/117.41 inference(scs_inference,[],[4638,123])).
% 117.32/117.41 cnf(4899,plain,
% 117.32/117.41 (~P14(f32(a23),a17,f33(f34(a26,f11(a26)),f5(a26,f11(a26))))),
% 117.32/117.41 inference(scs_inference,[],[282,216,186])).
% 117.32/117.41 cnf(7969,plain,
% 117.32/117.41 (~P7(f11(x79691),x79691)),
% 117.32/117.41 inference(scs_inference,[],[102,119])).
% 117.32/117.41 cnf(7977,plain,
% 117.32/117.41 (~P7(f11(x79771),f33(f34(x79771,f11(x79771)),f5(x79771,f11(x79771))))),
% 117.32/117.41 inference(scs_inference,[],[291,119])).
% 117.32/117.41 cnf(8142,plain,
% 117.32/117.41 (P8(f11(x81421),x81421)),
% 117.32/117.41 inference(scs_inference,[],[381,102,203,114])).
% 117.32/117.41 cnf(8146,plain,
% 117.32/117.41 (P8(f11(x81461),f33(f34(x81461,f11(x81461)),f5(x81461,f11(x81461))))),
% 117.32/117.41 inference(scs_inference,[],[381,275,102,203,114,206,91])).
% 117.32/117.41 cnf(8153,plain,
% 117.32/117.41 (P10(f11(f1(x81531)),x81531)),
% 117.32/117.41 inference(scs_inference,[],[381,275,102,7969,2000,203,114,206,91,164,205,123])).
% 117.32/117.41 cnf(8158,plain,
% 117.32/117.41 (P10(x81581,x81582)+~E(f12(x81582),x81581)),
% 117.32/117.41 inference(scs_inference,[],[381,596,275,380,102,7969,2000,292,203,114,206,91,164,205,123,73,90,70,86])).
% 117.32/117.41 cnf(8177,plain,
% 117.32/117.41 (P8(f11(x81771),f33(x81772,x81771))),
% 117.32/117.41 inference(scs_inference,[],[8142,205])).
% 117.32/117.41 cnf(8179,plain,
% 117.32/117.41 (P8(a26,f35(f32(a23)))),
% 117.32/117.41 inference(scs_inference,[],[214,8142,205,203])).
% 117.32/117.41 cnf(8183,plain,
% 117.32/117.41 (P8(f11(f34(x81831,f11(x81831))),x81831)),
% 117.32/117.41 inference(scs_inference,[],[275,214,8142,205,203,206,130])).
% 117.32/117.41 cnf(8184,plain,
% 117.32/117.41 (P8(f11(x81841),x81841)),
% 117.32/117.41 inference(rename_variables,[],[8142])).
% 117.32/117.41 cnf(8186,plain,
% 117.32/117.41 (P8(f11(f5(x81861,f11(x81861))),x81861)),
% 117.32/117.41 inference(scs_inference,[],[275,214,8142,8184,205,203,206,130,129])).
% 117.32/117.41 cnf(8199,plain,
% 117.32/117.41 (P8(a24,f35(f32(a16)))),
% 117.32/117.41 inference(scs_inference,[],[233,8179,205,203])).
% 117.32/117.42 cnf(8215,plain,
% 117.32/117.42 (P8(f27(f1(x82151)),f35(x82151))),
% 117.32/117.42 inference(scs_inference,[],[8199,4639,205,203])).
% 117.32/117.42 cnf(8233,plain,
% 117.32/117.42 (~E(a26,f33(f34(a17,f11(a17)),f5(a17,f11(a17))))),
% 117.32/117.42 inference(scs_inference,[],[622,2])).
% 117.32/117.42 cnf(8236,plain,
% 117.32/117.42 (P8(f11(f1(x82361)),f35(x82361))),
% 117.32/117.42 inference(scs_inference,[],[622,8215,8153,2,205,203])).
% 117.32/117.42 cnf(8240,plain,
% 117.32/117.42 (~E(a26,a17)),
% 117.32/117.42 inference(scs_inference,[],[622,275,8215,8153,2,205,203,206,3])).
% 117.32/117.42 cnf(8252,plain,
% 117.32/117.42 (~E(f33(f34(a26,f11(a26)),f5(a26,f11(a26))),a17)),
% 117.32/117.42 inference(scs_inference,[],[613,2])).
% 117.32/117.42 cnf(8257,plain,
% 117.32/117.42 (~P12(x82571,f35(x82572),f1(x82572))),
% 117.32/117.42 inference(scs_inference,[],[613,8236,7969,8142,2,205,206,163])).
% 117.32/117.42 cnf(8258,plain,
% 117.32/117.42 (~P7(f11(x82581),x82581)),
% 117.32/117.42 inference(rename_variables,[],[7969])).
% 117.32/117.42 cnf(8259,plain,
% 117.32/117.42 (P8(f11(x82591),x82591)),
% 117.32/117.42 inference(rename_variables,[],[8142])).
% 117.32/117.42 cnf(8261,plain,
% 117.32/117.42 (~P12(x82611,f1(x82612),f35(x82612))),
% 117.32/117.42 inference(scs_inference,[],[613,8236,7969,8258,8142,8259,2,205,206,163,164])).
% 117.32/117.42 cnf(8269,plain,
% 117.32/117.42 (~P10(f33(f34(a17,f11(a17)),f5(a17,f11(a17))),f32(a23))+~P9(a26,f32(a23))),
% 117.32/117.42 inference(scs_inference,[],[4566,613,8236,8233,8240,7969,8258,8142,8259,2,205,206,163,164,111,124,154])).
% 117.32/117.42 cnf(8281,plain,
% 117.32/117.42 (P8(f4(f1(x82811),f31(f1(x82811))),f1(x82811))),
% 117.32/117.42 inference(scs_inference,[],[1810,1676,8177,2,205,206,113])).
% 117.32/117.42 cnf(8283,plain,
% 117.32/117.42 (P10(a17,f32(a23))),
% 117.32/117.42 inference(scs_inference,[],[835,1810,1676,8177,2,205,206,113,204])).
% 117.32/117.42 cnf(8287,plain,
% 117.32/117.42 (P8(f4(f1(x82871),f31(f1(x82871))),f35(x82871))),
% 117.32/117.42 inference(scs_inference,[],[835,1810,1676,8177,2,205,206,113,204,123,203])).
% 117.32/117.42 cnf(8291,plain,
% 117.32/117.42 (P10(f33(f34(a17,f11(a17)),f5(a17,f11(a17))),f32(a23))),
% 117.32/117.42 inference(scs_inference,[],[275,835,1810,1676,8177,2,205,206,113,204,123,203,1688,86])).
% 117.32/117.42 cnf(8302,plain,
% 117.32/117.42 (P14(f32(a23),f12(f32(a23)),a17)),
% 117.32/117.42 inference(scs_inference,[],[8283,625])).
% 117.32/117.42 cnf(8303,plain,
% 117.32/117.42 (~P9(a26,f32(a23))),
% 117.32/117.42 inference(scs_inference,[],[8291,8269])).
% 117.32/117.42 cnf(8309,plain,
% 117.32/117.42 (~P9(f33(f34(a26,f11(a26)),f5(a26,f11(a26))),f32(a23))),
% 117.32/117.42 inference(scs_inference,[],[4899,8287,8252,617,8283,2,205,206,154])).
% 117.32/117.42 cnf(8469,plain,
% 117.32/117.42 (P8(f11(f34(x84691,f11(x84691))),f33(x84692,x84691))),
% 117.32/117.42 inference(scs_inference,[],[8183,205])).
% 117.32/117.42 cnf(8471,plain,
% 117.32/117.42 (P8(f11(f34(x84711,f11(x84711))),f33(x84711,x84712))),
% 117.32/117.42 inference(scs_inference,[],[8183,205,206])).
% 117.32/117.42 cnf(8487,plain,
% 117.32/117.42 (P8(f11(f34(x84871,f11(x84871))),f33(f33(x84872,x84871),x84873))),
% 117.32/117.42 inference(scs_inference,[],[8469,205,206])).
% 117.32/117.42 cnf(8521,plain,
% 117.32/117.42 (P8(f11(f5(x85211,f11(x85211))),f33(x85212,x85211))),
% 117.32/117.42 inference(scs_inference,[],[8186,205])).
% 117.32/117.42 cnf(8523,plain,
% 117.32/117.42 (P8(f11(f5(x85231,f11(x85231))),f33(x85231,x85232))),
% 117.32/117.42 inference(scs_inference,[],[8186,205,206])).
% 117.32/117.42 cnf(8551,plain,
% 117.32/117.42 (P8(f11(f5(x85511,f11(x85511))),f33(x85512,f33(x85511,x85513)))),
% 117.32/117.42 inference(scs_inference,[],[8523,205])).
% 117.32/117.42 cnf(9168,plain,
% 117.32/117.42 (P7(f27(f1(x91681)),f1(x91681))),
% 117.32/117.42 inference(scs_inference,[],[3814,108])).
% 117.32/117.42 cnf(9170,plain,
% 117.32/117.42 (P7(f31(f1(x91701)),f1(x91701))),
% 117.32/117.42 inference(scs_inference,[],[3814,101,108,110])).
% 117.32/117.42 cnf(9172,plain,
% 117.32/117.42 (P11(f3(f2(a16,a24),f2(a16,a24)))),
% 117.32/117.42 inference(scs_inference,[],[3814,212,101,108,110,117])).
% 117.32/117.42 cnf(9179,plain,
% 117.32/117.42 (P10(f31(f1(x91791)),x91791)),
% 117.32/117.42 inference(scs_inference,[],[3814,8291,212,4569,276,101,108,110,117,153,118,242,313])).
% 117.32/117.42 cnf(9190,plain,
% 117.32/117.42 (P11(f3(f2(a23,a26),f2(a16,a24)))),
% 117.32/117.42 inference(scs_inference,[],[3814,8291,4639,212,4569,276,107,1676,101,108,110,117,153,118,242,313,1066,122,134,133,146])).
% 117.32/117.42 cnf(9192,plain,
% 117.32/117.42 (P12(f11(x91921),f34(x91921,f11(x91921)),f5(x91921,f11(x91921)))),
% 117.32/117.42 inference(scs_inference,[],[3814,8291,4639,212,4569,276,102,107,1676,101,108,110,117,153,118,242,313,1066,122,134,133,146,158])).
% 117.32/117.42 cnf(9194,plain,
% 117.32/117.42 (P11(f3(f2(a23,a26),f2(x91941,f22(f2(a23,a26),x91941))))),
% 117.32/117.42 inference(scs_inference,[],[3814,8291,210,4639,212,4569,276,102,107,1676,101,108,110,117,153,118,242,313,1066,122,134,133,146,158,167])).
% 117.32/117.42 cnf(9196,plain,
% 117.32/117.42 (P11(f3(f2(a16,a17),f2(a23,a17)))),
% 117.32/117.42 inference(scs_inference,[],[104,3814,8291,210,4639,212,4569,276,102,107,1676,101,108,110,117,153,118,242,313,1066,122,134,133,146,158,167,174])).
% 117.32/117.42 cnf(9198,plain,
% 117.32/117.42 (P8(f11(x91981),f5(x91981,f11(x91981)))),
% 117.32/117.42 inference(scs_inference,[],[104,3814,8291,210,4639,212,4569,276,102,107,1676,101,108,110,117,153,118,242,313,1066,122,134,133,146,158,167,174,150])).
% 117.32/117.42 cnf(9200,plain,
% 117.32/117.42 (P8(f11(x92001),f34(x92001,f11(x92001)))),
% 117.32/117.42 inference(scs_inference,[],[104,3814,8291,210,4639,212,4569,276,102,107,1676,101,108,110,117,153,118,242,313,1066,122,134,133,146,158,167,174,150,151])).
% 117.32/117.42 cnf(9208,plain,
% 117.32/117.42 (P8(f11(x92081),f28(f11(x92081),x92081))),
% 117.32/117.42 inference(scs_inference,[],[104,3814,8291,210,4639,212,611,8303,4569,276,7969,102,8283,107,8142,1676,214,101,108,110,117,153,118,242,313,1066,122,134,133,146,158,167,174,150,151,119,131,132,138])).
% 117.32/117.42 cnf(9209,plain,
% 117.32/117.42 (~P7(f11(x92091),x92091)),
% 117.32/117.42 inference(rename_variables,[],[7969])).
% 117.47/117.42 cnf(9211,plain,
% 117.47/117.42 (P8(f11(x92111),f29(f11(x92111),x92111))),
% 117.47/117.42 inference(scs_inference,[],[104,3814,8291,210,4639,212,611,8303,4569,276,7969,9209,102,8283,107,8142,1676,214,101,108,110,117,153,118,242,313,1066,122,134,133,146,158,167,174,150,151,119,131,132,138,139])).
% 117.47/117.42 cnf(9212,plain,
% 117.47/117.42 (~P7(f11(x92121),x92121)),
% 117.47/117.42 inference(rename_variables,[],[7969])).
% 117.47/117.42 cnf(9214,plain,
% 117.47/117.42 (P15(f28(f11(x92141),x92141),x92141)),
% 117.47/117.42 inference(scs_inference,[],[104,3814,8291,210,4639,212,611,8303,4569,276,7969,9209,9212,102,8283,107,8142,1676,214,101,108,110,117,153,118,242,313,1066,122,134,133,146,158,167,174,150,151,119,131,132,138,139,140])).
% 117.47/117.42 cnf(9215,plain,
% 117.47/117.42 (~P7(f11(x92151),x92151)),
% 117.47/117.42 inference(rename_variables,[],[7969])).
% 117.47/117.42 cnf(9217,plain,
% 117.47/117.42 (P15(f29(f11(x92171),x92171),x92171)),
% 117.47/117.42 inference(scs_inference,[],[104,3814,8291,210,4639,212,611,8303,4569,276,7969,9209,9212,9215,102,8283,107,8142,1676,214,101,108,110,117,153,118,242,313,1066,122,134,133,146,158,167,174,150,151,119,131,132,138,139,140,141])).
% 117.47/117.42 cnf(9218,plain,
% 117.47/117.42 (~P7(f11(x92181),x92181)),
% 117.47/117.42 inference(rename_variables,[],[7969])).
% 117.47/117.42 cnf(9220,plain,
% 117.47/117.42 (P10(f6(a17,f32(a23)),f32(a23))),
% 117.47/117.42 inference(scs_inference,[],[104,3814,8291,210,4639,212,611,8303,4569,276,7969,9209,9212,9215,102,8283,107,8142,1676,214,101,108,110,117,153,118,242,313,1066,122,134,133,146,158,167,174,150,151,119,131,132,138,139,140,141,142])).
% 117.47/117.42 cnf(9227,plain,
% 117.47/117.42 (~P6(x92271,x92272,x92273,x92272)),
% 117.47/117.42 inference(rename_variables,[],[216])).
% 117.47/117.42 cnf(9229,plain,
% 117.47/117.42 (E(f33(f34(x92291,f11(x92291)),f5(x92291,f11(x92291))),x92291)),
% 117.47/117.42 inference(rename_variables,[],[288])).
% 117.47/117.42 cnf(9231,plain,
% 117.47/117.42 (~P6(x92311,x92312,x92313,x92312)),
% 117.47/117.42 inference(rename_variables,[],[216])).
% 117.47/117.42 cnf(9233,plain,
% 117.47/117.42 (~P7(f11(x92331),x92331)),
% 117.47/117.42 inference(rename_variables,[],[7969])).
% 117.47/117.42 cnf(9242,plain,
% 117.47/117.42 (E(f33(f34(x92421,f11(x92421)),f5(x92421,f11(x92421))),x92421)),
% 117.47/117.42 inference(rename_variables,[],[288])).
% 117.47/117.42 cnf(9247,plain,
% 117.47/117.42 (~P14(f32(a23),f33(f34(a26,f11(a26)),f5(a26,f11(a26))),a26)),
% 117.47/117.42 inference(scs_inference,[],[104,3814,8302,8291,284,210,8309,4639,212,611,8303,4569,8177,276,216,9227,9231,604,7969,9209,9212,9215,9218,9233,102,8283,107,606,8142,1676,214,101,288,9229,9242,108,110,117,153,118,242,313,1066,122,134,133,146,158,167,174,150,151,119,131,132,138,139,140,141,142,143,165,93,94,95,160,161,166,121,186,76])).
% 117.47/117.42 cnf(9248,plain,
% 117.47/117.42 (E(f33(f34(x92481,f11(x92481)),f5(x92481,f11(x92481))),x92481)),
% 117.47/117.42 inference(rename_variables,[],[288])).
% 117.47/117.42 cnf(9249,plain,
% 117.47/117.42 (~P9(f12(f32(a23)),f32(a23))),
% 117.47/117.42 inference(scs_inference,[],[104,3814,8302,8291,284,210,8309,4639,212,611,8303,4569,8177,276,216,9227,9231,604,7969,9209,9212,9215,9218,9233,102,8283,107,606,8142,1676,214,101,288,9229,9242,108,110,117,153,118,242,313,1066,122,134,133,146,158,167,174,150,151,119,131,132,138,139,140,141,142,143,165,93,94,95,160,161,166,121,186,76,1688])).
% 117.47/117.42 cnf(9252,plain,
% 117.47/117.42 (~P14(f32(a23),a26,f33(f34(a26,f11(a26)),f5(a26,f11(a26))))),
% 117.47/117.42 inference(scs_inference,[],[104,3814,8302,8291,3318,284,210,8309,4639,212,611,8303,4569,8177,276,216,9227,9231,604,7969,9209,9212,9215,9218,9233,102,8283,107,606,8142,1676,214,101,288,9229,9242,9248,108,110,117,153,118,242,313,1066,122,134,133,146,158,167,174,150,151,119,131,132,138,139,140,141,142,143,165,93,94,95,160,161,166,121,186,76,1688,82,77])).
% 117.47/117.42 cnf(9257,plain,
% 117.47/117.42 (~P12(x92571,f35(x92572),f1(x92572))),
% 117.47/117.42 inference(rename_variables,[],[8257])).
% 117.47/117.42 cnf(9258,plain,
% 117.47/117.42 (P8(f4(f1(x92581),f31(f1(x92581))),f1(x92581))),
% 117.47/117.42 inference(rename_variables,[],[8281])).
% 117.47/117.42 cnf(9265,plain,
% 117.47/117.42 (P8(f11(x92651),x92651)),
% 117.47/117.42 inference(rename_variables,[],[8142])).
% 117.47/117.42 cnf(9266,plain,
% 117.47/117.42 (P8(f11(x92661),f33(f34(x92661,f11(x92661)),f5(x92661,f11(x92661))))),
% 117.47/117.42 inference(rename_variables,[],[8146])).
% 117.47/117.42 cnf(9268,plain,
% 117.47/117.42 (~P12(x92681,f33(f34(x92682,f11(x92682)),f5(x92682,f11(x92682))),x92682)),
% 117.47/117.42 inference(scs_inference,[],[104,8257,9257,3814,8302,8291,3318,284,8146,9266,7977,210,8309,4639,212,611,8303,4569,8281,9258,8177,8287,276,216,9227,9231,604,7969,9209,9212,9215,9218,9233,102,8283,107,606,8142,9265,1676,214,101,288,9229,9242,9248,108,110,117,153,118,242,313,1066,122,134,133,146,158,167,174,150,151,119,131,132,138,139,140,141,142,143,165,93,94,95,160,161,166,121,186,76,1688,82,77,191,176,175,163,164])).
% 117.47/117.42 cnf(9272,plain,
% 117.47/117.42 (~P9(f6(a17,f32(a23)),f32(a23))),
% 117.47/117.42 inference(scs_inference,[],[104,8257,9257,3814,8302,8291,3318,284,8146,9266,7977,210,8309,4639,212,611,8303,4569,8281,9258,8177,8287,276,216,9227,9231,604,7969,9209,9212,9215,9218,9233,102,8283,107,606,8142,9265,1676,214,101,288,9229,9242,9248,108,110,117,153,118,242,313,1066,122,134,133,146,158,167,174,150,151,119,131,132,138,139,140,141,142,143,165,93,94,95,160,161,166,121,186,76,1688,82,77,191,176,175,163,164,154])).
% 117.47/117.42 cnf(9274,plain,
% 117.47/117.42 (~P13(f10(a26,f32(a23)),f32(a23))),
% 117.47/117.42 inference(scs_inference,[],[104,8257,9257,3814,8302,8291,3318,284,8146,9266,7977,210,8309,4639,212,611,8303,4569,8281,9258,8177,8287,276,216,9227,9231,604,7969,9209,9212,9215,9218,9233,102,8283,107,606,8142,9265,1676,214,101,288,9229,9242,9248,108,110,117,153,118,242,313,1066,122,134,133,146,158,167,174,150,151,119,131,132,138,139,140,141,142,143,165,93,94,95,160,161,166,121,186,76,1688,82,77,191,176,175,163,164,154,155])).
% 117.47/117.42 cnf(9278,plain,
% 117.47/117.42 (~P8(f13(f29(f11(x92781),x92781),f28(f11(x92781),x92781)),f29(f11(x92781),x92781))),
% 117.47/117.42 inference(scs_inference,[],[104,8257,9257,3814,8302,8291,3318,284,8146,9266,7977,210,8309,4639,212,611,8303,4569,8281,9258,8177,8287,276,216,9227,9231,604,7969,9209,9212,9215,9218,9233,102,8283,107,606,8142,9265,1676,214,101,288,9229,9242,9248,108,110,117,153,118,242,313,1066,122,134,133,146,158,167,174,150,151,119,131,132,138,139,140,141,142,143,165,93,94,95,160,161,166,121,186,76,1688,82,77,191,176,175,163,164,154,155,127,144])).
% 117.47/117.42 cnf(9307,plain,
% 117.47/117.42 (P10(f4(f1(x93071),f27(f1(x93071))),x93071)),
% 117.47/117.42 inference(scs_inference,[],[9168,9170,122,134,313])).
% 117.47/117.42 cnf(9313,plain,
% 117.47/117.42 (P11(f3(f2(a23,a17),f2(a16,a17)))),
% 117.47/117.42 inference(scs_inference,[],[9168,9170,9220,9190,9196,122,134,313,118,117,146])).
% 117.47/117.42 cnf(9315,plain,
% 117.47/117.42 (P10(a17,f32(a16))),
% 117.47/117.42 inference(scs_inference,[],[9168,9170,9220,9190,9196,278,122,134,313,118,117,146,153])).
% 117.47/117.42 cnf(9322,plain,
% 117.47/117.42 (P10(f10(f6(a17,f32(a23)),f32(a23)),f32(a23))),
% 117.47/117.42 inference(scs_inference,[],[9168,9170,9272,9274,9220,9190,9196,278,122,134,313,118,117,146,153,133,242,119,143])).
% 117.47/117.42 cnf(9324,plain,
% 117.47/117.42 (~E(f10(f6(a17,f32(a23)),f32(a23)),f6(a17,f32(a23)))),
% 117.47/117.42 inference(scs_inference,[],[9168,9170,9272,9274,9220,9190,9196,278,122,134,313,118,117,146,153,133,242,119,143,132])).
% 117.47/117.42 cnf(9326,plain,
% 117.47/117.42 (~P14(f32(a23),f10(f6(a17,f32(a23)),f32(a23)),f6(a17,f32(a23)))),
% 117.47/117.42 inference(scs_inference,[],[9168,9170,9272,9274,9220,9190,9196,278,122,134,313,118,117,146,153,133,242,119,143,132,166])).
% 117.47/117.42 cnf(9328,plain,
% 117.47/117.42 (P7(f11(x93281),f5(x93281,f11(x93281)))),
% 117.47/117.42 inference(scs_inference,[],[9168,9170,9272,9274,9220,9198,9200,9190,9196,9192,278,122,134,313,118,117,146,153,133,242,119,143,132,166,163])).
% 117.47/117.42 cnf(9329,plain,
% 117.47/117.42 (P8(f11(x93291),f5(x93291,f11(x93291)))),
% 117.47/117.42 inference(rename_variables,[],[9198])).
% 117.47/117.42 cnf(9330,plain,
% 117.47/117.42 (P12(f11(x93301),f34(x93301,f11(x93301)),f5(x93301,f11(x93301)))),
% 117.47/117.42 inference(rename_variables,[],[9192])).
% 117.47/117.42 cnf(9332,plain,
% 117.47/117.42 (P7(f11(x93321),f34(x93321,f11(x93321)))),
% 117.47/117.42 inference(scs_inference,[],[9168,9170,9272,9274,9220,9198,9329,9200,9190,9196,9192,9330,278,122,134,313,118,117,146,153,133,242,119,143,132,166,163,164])).
% 117.47/117.42 cnf(9336,plain,
% 117.47/117.42 (P11(f3(f3(f3(f2(a23,a26),f2(a16,a24)),f2(a23,a26)),f2(a16,a24)))),
% 117.47/117.43 inference(scs_inference,[],[9168,9170,9272,9274,9220,9198,9329,9200,9190,9196,9192,9330,278,122,134,313,118,117,146,153,133,242,119,143,132,166,163,164,171])).
% 117.47/117.43 cnf(9340,plain,
% 117.47/117.43 (P7(f27(f5(x93401,f11(x93401))),f5(x93401,f11(x93401)))),
% 117.47/117.43 inference(scs_inference,[],[9168,9170,9272,9274,9220,9198,9329,9200,9190,9196,9192,9330,278,122,134,313,118,117,146,153,133,242,119,143,132,166,163,164,171,273,274])).
% 117.47/117.43 cnf(9369,plain,
% 117.47/117.43 (P7(f27(f34(x93691,f11(x93691))),f34(x93691,f11(x93691)))),
% 117.47/117.43 inference(scs_inference,[],[9332,274])).
% 117.47/117.43 cnf(9371,plain,
% 117.47/117.43 (P7(f4(f5(x93711,f11(x93711)),f11(x93711)),f5(x93711,f11(x93711)))),
% 117.47/117.43 inference(scs_inference,[],[9328,9332,274,134])).
% 117.47/117.43 cnf(9375,plain,
% 117.47/117.43 (P7(f31(f34(x93751,f11(x93751))),f34(x93751,f11(x93751)))),
% 117.47/117.43 inference(scs_inference,[],[9328,9332,9313,274,134,117,273])).
% 117.47/117.43 cnf(9381,plain,
% 117.47/117.43 (P11(f3(f2(a16,a24),f3(f3(f2(a23,a26),f2(a16,a24)),f2(a23,a26))))),
% 117.47/117.43 inference(scs_inference,[],[9315,9328,9332,9313,9336,274,134,117,273,118,122,146])).
% 117.47/117.43 cnf(9383,plain,
% 117.47/117.43 (P11(f2(a16,a17))),
% 117.47/117.43 inference(scs_inference,[],[9315,9328,9332,9313,9336,274,134,117,273,118,122,146,133])).
% 117.47/117.43 cnf(9390,plain,
% 117.47/117.43 (P10(f12(x93901),x93901)),
% 117.47/117.43 inference(rename_variables,[],[381])).
% 117.47/117.43 cnf(9395,plain,
% 117.47/117.43 (P10(f10(f12(f32(a23)),f32(a23)),f32(a23))),
% 117.47/117.43 inference(scs_inference,[],[9315,9249,9214,9328,9332,9313,9336,8142,381,9390,274,134,117,273,118,122,146,133,1066,119,132,128,143])).
% 117.47/117.43 cnf(9396,plain,
% 117.47/117.43 (P10(f12(x93961),x93961)),
% 117.47/117.43 inference(rename_variables,[],[381])).
% 117.47/117.43 cnf(9401,plain,
% 117.47/117.43 (P11(f3(f3(f3(f2(a23,a17),f2(a16,a17)),f2(a23,a17)),f2(a16,a17)))),
% 117.47/117.43 inference(scs_inference,[],[9315,9249,9214,9328,9332,9313,9336,8142,381,9390,9396,274,134,117,273,118,122,146,133,1066,119,132,128,143,166,171])).
% 117.47/117.43 cnf(9413,plain,
% 117.47/117.43 (P7(f4(f34(x94131,f11(x94131)),f11(x94131)),f34(x94131,f11(x94131)))),
% 117.47/117.43 inference(scs_inference,[],[9332,134])).
% 117.47/117.43 cnf(9415,plain,
% 117.47/117.43 (P11(f3(f2(a16,a17),f2(a16,a17)))),
% 117.47/117.43 inference(scs_inference,[],[9383,9332,134,117])).
% 117.47/117.43 cnf(9419,plain,
% 117.47/117.43 (P8(f31(f1(x94191)),f1(x94191))),
% 117.47/117.43 inference(scs_inference,[],[9383,9179,9401,9332,134,117,146,118])).
% 117.47/117.43 cnf(9429,plain,
% 117.47/117.43 (P10(f10(a26,f32(a23)),f32(a23))),
% 117.47/117.43 inference(scs_inference,[],[9383,9179,9395,9371,9401,9381,9332,8303,214,134,117,146,118,171,133,122,119,143])).
% 117.47/117.43 cnf(9431,plain,
% 117.47/117.43 (P11(f2(a23,a17))),
% 117.47/117.43 inference(scs_inference,[],[9383,9179,9395,9371,9401,9381,9332,8303,214,134,117,146,118,171,133,122,119,143,3287])).
% 117.47/117.43 cnf(9435,plain,
% 117.47/117.43 (~P14(f32(a23),f10(a26,f32(a23)),f6(f10(a26,f32(a23)),f32(a23)))),
% 117.47/117.43 inference(scs_inference,[],[9383,9208,9179,9395,9371,9401,9381,9274,9332,8303,214,134,117,146,118,171,133,122,119,143,3287,140,165])).
% 117.47/117.43 cnf(9437,plain,
% 117.47/117.43 (P10(f6(f10(a26,f32(a23)),f32(a23)),f32(a23))),
% 117.47/117.43 inference(scs_inference,[],[9383,9208,9179,9395,9371,9401,9381,9274,9332,8303,214,134,117,146,118,171,133,122,119,143,3287,140,165,142])).
% 117.47/117.43 cnf(9439,plain,
% 117.47/117.43 (~E(f6(f10(a26,f32(a23)),f32(a23)),f10(a26,f32(a23)))),
% 117.47/117.43 inference(scs_inference,[],[9383,9208,9179,9395,9371,9401,9381,9274,9332,8303,214,134,117,146,118,171,133,122,119,143,3287,140,165,142,131])).
% 117.47/117.43 cnf(9451,plain,
% 117.47/117.43 (P11(f3(f2(a23,a17),f2(a23,a17)))),
% 117.47/117.43 inference(scs_inference,[],[9431,117])).
% 117.47/117.43 cnf(9490,plain,
% 117.47/117.43 (P11(f3(f2(a16,a17),f3(f3(f2(a16,a17),f2(a16,a17)),f2(a16,a17))))),
% 117.47/117.43 inference(scs_inference,[],[9211,9415,9322,9340,117,118,133,119,171,138,146])).
% 117.47/117.43 cnf(9512,plain,
% 117.47/117.43 (P11(f3(f3(f2(a23,a17),f2(a23,a17)),f3(f2(a23,a17),f2(a23,a17))))),
% 117.47/117.43 inference(scs_inference,[],[9451,9437,9490,171,118,117])).
% 117.47/117.43 cnf(9518,plain,
% 117.47/117.43 (~P9(f6(f10(a26,f32(a23)),f32(a23)),f32(a23))),
% 117.47/117.43 inference(scs_inference,[],[9451,9437,9439,9490,9435,9369,9429,171,118,117,133,119,154])).
% 117.47/117.43 cnf(9526,plain,
% 117.47/117.43 (P8(f4(f1(x95261),f27(f1(x95261))),f1(x95261))),
% 117.47/117.43 inference(scs_inference,[],[9307,118])).
% 117.47/117.43 cnf(9530,plain,
% 117.47/117.43 (P11(f3(f3(f2(a16,a24),f2(a16,a24)),f3(f2(a16,a24),f2(a16,a24))))),
% 117.47/117.43 inference(scs_inference,[],[9172,9307,9512,118,171,117])).
% 117.47/117.43 cnf(9537,plain,
% 117.47/117.43 (P8(f11(f29(f11(x95371),x95371)),x95371)),
% 117.47/117.43 inference(scs_inference,[],[9172,9307,9512,9217,9332,8142,381,118,171,117,133,119,128])).
% 117.47/117.43 cnf(9538,plain,
% 117.47/117.43 (P8(f11(x95381),x95381)),
% 117.47/117.43 inference(rename_variables,[],[8142])).
% 117.47/117.43 cnf(9540,plain,
% 117.47/117.43 (P10(f10(f6(f10(a26,f32(a23)),f32(a23)),f32(a23)),f32(a23))),
% 117.47/117.43 inference(scs_inference,[],[9172,9518,9307,9512,9217,9437,9332,8142,381,118,171,117,133,119,128,143])).
% 117.47/117.43 cnf(9545,plain,
% 117.47/117.43 (P11(f3(f2(a23,a17),f3(f3(f2(a23,a17),f2(a23,a17)),f2(a23,a17))))),
% 117.47/117.43 inference(scs_inference,[],[9172,9518,9307,9512,9217,9247,9252,9437,9332,8142,381,118,171,117,133,119,128,143,190,241,146])).
% 117.47/117.43 cnf(9549,plain,
% 117.47/117.43 (~P8(f11(f5(x95491,f11(x95491))),f34(x95491,f11(x95491)))),
% 117.47/117.43 inference(scs_inference,[],[9172,9518,9307,9512,9217,9179,9247,9252,9192,9437,9332,7969,8142,9538,381,118,171,117,133,119,128,143,190,241,146,165,163])).
% 117.47/117.43 cnf(9550,plain,
% 117.47/117.43 (P8(f11(x95501),x95501)),
% 117.47/117.43 inference(rename_variables,[],[8142])).
% 117.47/117.43 cnf(9551,plain,
% 117.47/117.43 (~P7(f11(x95511),x95511)),
% 117.47/117.43 inference(rename_variables,[],[7969])).
% 117.47/117.43 cnf(9553,plain,
% 117.47/117.43 (~P8(f11(f34(x95531,f11(x95531))),f5(x95531,f11(x95531)))),
% 117.47/117.43 inference(scs_inference,[],[9172,9518,9307,9512,9217,9179,9247,9252,9192,9437,9332,7969,9551,8142,9538,9550,381,118,171,117,133,119,128,143,190,241,146,165,163,164])).
% 117.47/117.43 cnf(9557,plain,
% 117.47/117.43 (~P13(f10(f6(a17,f32(a23)),f32(a23)),f32(a23))),
% 117.47/117.43 inference(scs_inference,[],[9172,9518,9324,9307,9512,9217,9326,9179,9247,9252,9192,9437,9332,9220,7969,9551,8142,9538,9550,381,118,171,117,133,119,128,143,190,241,146,165,163,164,155])).
% 117.47/117.43 cnf(9560,plain,
% 117.47/117.43 (~P2(f11(f5(x95601,f11(x95601))),f34(x95601,f11(x95601)))),
% 117.47/117.43 inference(scs_inference,[],[9172,9518,9324,9307,9512,9217,9326,9179,9247,9252,9192,9437,9332,9220,7969,9551,8142,9538,9550,381,118,171,117,133,119,128,143,190,241,146,165,163,164,155,242,114])).
% 117.47/117.43 cnf(9574,plain,
% 117.47/117.43 (~P2(f11(f34(x95741,f11(x95741))),f5(x95741,f11(x95741)))),
% 117.47/117.43 inference(scs_inference,[],[9553,9560,9545,241,113,171,114])).
% 117.47/117.43 cnf(9578,plain,
% 117.47/117.43 (P11(f3(f3(f2(a16,a17),f2(a23,a17)),f3(f2(a16,a17),f2(a23,a17))))),
% 117.47/117.43 inference(scs_inference,[],[9540,9553,9560,9545,9196,241,113,171,114,118,117])).
% 117.47/117.43 cnf(9580,plain,
% 117.47/117.43 (P10(f6(f10(f6(a17,f32(a23)),f32(a23)),f32(a23)),f32(a23))),
% 117.47/117.43 inference(scs_inference,[],[9557,9540,9553,9560,9545,9196,9322,241,113,171,114,118,117,142])).
% 117.47/117.43 cnf(9599,plain,
% 117.47/117.43 (P11(f3(f3(f2(a23,a26),f2(a23,a26)),f3(f2(a23,a26),f2(a23,a26))))),
% 117.47/117.43 inference(scs_inference,[],[9580,9574,9578,595,241,171,118,117])).
% 117.47/117.43 cnf(9604,plain,
% 117.47/117.43 (P11(f3(f2(a23,a17),f3(f3(f2(a16,a17),f2(a23,a17)),f2(a16,a17))))),
% 117.47/117.43 inference(scs_inference,[],[9580,9574,9578,595,8183,9553,241,171,118,117,137,146])).
% 117.47/117.43 cnf(9623,plain,
% 117.47/117.43 (P11(f3(f3(f2(a16,a24),f2(a23,a26)),f3(f2(a16,a24),f2(a23,a26))))),
% 117.47/117.43 inference(scs_inference,[],[9604,9395,107,171,118,117])).
% 117.47/117.43 cnf(9635,plain,
% 117.47/117.43 (P11(f3(f2(a23,a26),f3(f3(f2(a16,a24),f2(a23,a26)),f2(a16,a24))))),
% 117.47/117.43 inference(scs_inference,[],[9623,233,608,288,118,171,94,146])).
% 117.47/117.43 cnf(9658,plain,
% 117.47/117.43 (P8(f11(f35(x96581)),f1(x96581))),
% 117.47/117.43 inference(scs_inference,[],[9635,349,171,118])).
% 117.47/117.43 cnf(9686,plain,
% 117.47/117.43 (P8(f11(f34(x96861,f11(x96861))),f33(f33(x96862,x96861),x96863))),
% 117.47/117.43 inference(rename_variables,[],[8487])).
% 117.47/117.43 cnf(9689,plain,
% 117.47/117.43 (P8(f11(f34(x96891,f11(x96891))),f33(f33(x96892,x96891),x96893))),
% 117.47/117.43 inference(rename_variables,[],[8487])).
% 117.47/117.43 cnf(9694,plain,
% 117.47/117.43 (P8(f30(f11(f35(x96941)),f1(x96941),f35(x96941)),f1(x96941))),
% 117.47/117.43 inference(scs_inference,[],[9658,9599,8487,9686,9689,9553,8283,8261,8142,118,171,130,128,129,176])).
% 117.47/117.43 cnf(9695,plain,
% 117.47/117.43 (P8(f11(x96951),x96951)),
% 117.47/117.43 inference(rename_variables,[],[8142])).
% 117.47/117.43 cnf(9696,plain,
% 117.47/117.43 (P8(f11(f35(x96961)),f1(x96961))),
% 117.47/117.43 inference(rename_variables,[],[9658])).
% 117.47/117.43 cnf(9697,plain,
% 117.47/117.43 (~P12(x96971,f1(x96972),f35(x96972))),
% 117.47/117.43 inference(rename_variables,[],[8261])).
% 117.47/117.43 cnf(9699,plain,
% 117.47/117.43 (P8(f30(f11(f35(x96991)),f1(x96991),f35(x96991)),f35(x96991))),
% 117.47/117.43 inference(scs_inference,[],[9658,9696,9599,8487,9686,9689,9553,8283,8261,9697,8142,9695,118,171,130,128,129,176,175])).
% 117.47/117.43 cnf(9756,plain,
% 117.47/117.43 (P11(f3(f2(a16,a24),f3(f3(f2(a16,a24),f2(a16,a24)),f2(a16,a24))))),
% 117.47/117.43 inference(scs_inference,[],[9530,171,146])).
% 117.47/117.43 cnf(9863,plain,
% 117.47/117.43 (P12(f4(f1(x98631),f27(f1(x98631))),f1(x98631),f1(x98631))+P8(f30(f4(f1(x98631),f27(f1(x98631))),f1(x98631),f1(x98631)),f1(x98631))),
% 117.47/117.43 inference(scs_inference,[],[9526,8551,8471,9549,9553,128,137,176])).
% 117.47/117.43 cnf(9901,plain,
% 117.47/117.43 (P12(f31(f1(x99011)),f1(x99011),f1(x99011))+P8(f30(f31(f1(x99011)),f1(x99011),f1(x99011)),f1(x99011))),
% 117.47/117.43 inference(scs_inference,[],[9419,175])).
% 117.47/117.43 cnf(9992,plain,
% 117.47/117.43 (P12(f30(f11(f35(x99921)),f1(x99921),f35(x99921)),f1(x99921),f1(x99921))+P8(f30(f30(f11(f35(x99921)),f1(x99921),f35(x99921)),f1(x99921),f1(x99921)),f1(x99921))),
% 117.47/117.43 inference(scs_inference,[],[9694,175])).
% 117.47/117.43 cnf(10099,plain,
% 117.47/117.43 (P12(f11(f35(x100991)),f1(x100991),f1(x100991))+P8(f30(f11(f35(x100991)),f1(x100991),f1(x100991)),f1(x100991))),
% 117.47/117.43 inference(scs_inference,[],[9658,175])).
% 117.47/117.43 cnf(10131,plain,
% 117.47/117.43 (~P8(f13(f34(x101311,f11(x101311)),x101311),f34(x101311,f11(x101311)))),
% 117.47/117.43 inference(scs_inference,[],[8186,9549,128,144])).
% 117.47/117.43 cnf(10133,plain,
% 117.47/117.43 (P8(f13(f34(x101331,f11(x101331)),x101331),x101331)),
% 117.47/117.43 inference(scs_inference,[],[8186,9549,128,144,127])).
% 117.47/117.43 cnf(10191,plain,
% 117.47/117.43 (~P15(f33(x101911,x101912),f34(x101912,f11(x101912)))),
% 117.47/117.43 inference(scs_inference,[],[8521,9549,128])).
% 117.47/117.43 cnf(10200,plain,
% 117.47/117.43 (P8(f13(f34(x102001,f11(x102001)),f33(x102002,x102001)),f33(x102002,x102001))),
% 117.47/117.43 inference(scs_inference,[],[10191,144,127])).
% 117.47/117.43 cnf(10217,plain,
% 117.47/117.43 (P8(f11(f5(x102171,f11(x102171))),f33(x102171,x102172))),
% 117.47/117.43 inference(rename_variables,[],[8523])).
% 117.47/117.43 cnf(10222,plain,
% 117.47/117.43 (P12(f13(f34(x102221,f11(x102221)),f33(x102222,x102221)),f33(x102222,x102221),f33(x102222,x102221))+P8(f30(f13(f34(x102221,f11(x102221)),f33(x102222,x102221)),f33(x102222,x102221),f33(x102222,x102221)),f33(x102222,x102221))),
% 117.47/117.43 inference(scs_inference,[],[10200,9375,8523,10217,9549,113,130,129,175])).
% 117.47/117.43 cnf(10230,plain,
% 117.47/117.43 (~P12(x102301,x102302,x102302)),
% 117.47/117.43 inference(scs_inference,[],[9268,275,97])).
% 117.47/117.43 cnf(10247,plain,
% 117.47/117.43 (P8(f30(f11(f35(x102471)),f1(x102471),f1(x102471)),f1(x102471))),
% 117.47/117.43 inference(scs_inference,[],[10230,10099])).
% 117.47/117.43 cnf(10248,plain,
% 117.47/117.43 (~P12(x102481,x102482,x102482)),
% 117.47/117.43 inference(rename_variables,[],[10230])).
% 117.47/117.43 cnf(10250,plain,
% 117.47/117.43 (~P12(x102501,x102502,x102502)),
% 117.47/117.43 inference(rename_variables,[],[10230])).
% 117.47/117.43 cnf(10252,plain,
% 117.47/117.43 (~P12(x102521,x102522,x102522)),
% 117.47/117.43 inference(rename_variables,[],[10230])).
% 117.47/117.43 cnf(10253,plain,
% 117.47/117.43 (P8(f30(f13(f34(x102531,f11(x102531)),f33(x102532,x102531)),f33(x102532,x102531),f33(x102532,x102531)),f33(x102532,x102531))),
% 117.47/117.43 inference(scs_inference,[],[10230,10248,10250,10252,10099,9863,9992,10222])).
% 117.47/117.43 cnf(10254,plain,
% 117.47/117.43 (~P12(x102541,x102542,x102542)),
% 117.47/117.43 inference(rename_variables,[],[10230])).
% 117.47/117.43 cnf(10256,plain,
% 117.47/117.43 (~P12(x102561,x102562,x102562)),
% 117.47/117.43 inference(rename_variables,[],[10230])).
% 117.47/117.43 cnf(10259,plain,
% 117.47/117.43 (P8(f30(f30(f11(f35(x102591)),f1(x102591),f35(x102591)),f35(x102591),f35(x102591)),f35(x102591))),
% 117.47/117.43 inference(scs_inference,[],[10230,10248,10250,10252,10254,10256,9340,9699,10099,9863,9992,10222,9901,113,176])).
% 117.47/117.43 cnf(10331,plain,
% 117.47/117.43 (P8(f30(f30(f30(f11(f35(x103311)),f1(x103311),f35(x103311)),f35(x103311),f35(x103311)),f35(x103311),f35(x103311)),f35(x103311))),
% 117.47/117.43 inference(scs_inference,[],[10259,9756,10230,125,176])).
% 117.47/117.43 cnf(10332,plain,
% 117.47/117.43 (~P12(x103321,x103322,x103322)),
% 117.47/117.43 inference(rename_variables,[],[10230])).
% 117.47/117.43 cnf(10334,plain,
% 117.47/117.43 (~P7(f30(f30(f30(f11(f35(x103341)),f1(x103341),f35(x103341)),f35(x103341),f35(x103341)),f35(x103341),f35(x103341)),f35(x103341))),
% 117.47/117.43 inference(scs_inference,[],[10259,9756,10230,10332,125,176,188])).
% 117.47/117.43 cnf(10362,plain,
% 117.47/117.43 (P8(f30(f30(f13(f34(x103621,f11(x103621)),f33(x103622,x103621)),f33(x103622,x103621),f33(x103622,x103621)),f33(x103622,x103621),f33(x103622,x103621)),f33(x103622,x103621))),
% 117.47/117.43 inference(scs_inference,[],[10253,10230,175])).
% 117.47/117.43 cnf(10373,plain,
% 117.47/117.43 (~P7(f30(f30(f11(f35(x103731)),f1(x103731),f1(x103731)),f1(x103731),f1(x103731)),f1(x103731))),
% 117.47/117.43 inference(scs_inference,[],[10334,10331,10247,10230,124,188])).
% 117.47/117.43 cnf(10435,plain,
% 117.47/117.43 (P8(f13(f34(f35(x104351),f11(f35(x104351))),f35(x104351)),f1(x104351))),
% 117.47/117.43 inference(scs_inference,[],[10133,9413,113,204,302,118])).
% 117.47/117.43 cnf(10442,plain,
% 117.47/117.43 (P8(f30(f30(f11(f35(x104421)),f1(x104421),f1(x104421)),f1(x104421),f1(x104421)),f1(x104421))),
% 117.47/117.43 inference(scs_inference,[],[10362,10133,10247,10131,9413,10230,113,204,302,118,207,120,175])).
% 117.47/117.43 cnf(10454,plain,
% 117.47/117.43 (~P8(f13(f34(x104541,f11(x104541)),x104541),f34(x104541,f11(x104541)))),
% 117.47/117.43 inference(rename_variables,[],[10131])).
% 117.47/117.43 cnf(10462,plain,
% 117.47/117.43 (~P11(f3(f2(a23,f12(f32(a23))),f2(a16,a24)))),
% 117.47/117.43 inference(scs_inference,[],[105,10373,10442,10435,9313,8302,10131,10454,129,128,141,193])).
% 117.47/117.43 cnf(12037,plain,
% 117.47/117.43 ($false),
% 117.47/117.43 inference(scs_inference,[],[9553,275,9537,8183,10462,9328,3318,9578,9278,2267,3349,9194,123,2,109,300,302,125,126,114,8158,151,150,146,205,170]),
% 117.47/117.43 ['proof']).
% 117.47/117.43 % SZS output end Proof
% 117.47/117.43 % Total time :116.660000s
%------------------------------------------------------------------------------