%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : GEO601+1 : TPTP v8.2.0. Released v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% Computer : n019.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:05:52 EDT 2024
% Result : Theorem 60.85s 61.58s
% Output : CNFRefutation 60.87s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.12 % Problem : GEO601+1 : TPTP v8.2.0. Released v7.5.0.
% 0.11/0.12 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% 0.11/0.32 % Computer : n019.cluster.edu
% 0.11/0.32 % Model : x86_64 x86_64
% 0.11/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.32 % Memory : 8042.1875MB
% 0.11/0.32 % OS : Linux 3.10.0-693.el7.x86_64
% 0.11/0.32 % CPULimit : 300
% 0.11/0.32 % WCLimit : 300
% 0.11/0.32 % DateTime : Fri Jun 21 06:08:39 EDT 2024
% 0.11/0.32 % CPUTime :
% 0.18/0.57 start to proof:theBenchmark
% 60.85/61.57 %-------------------------------------------
% 60.85/61.57 % File :CSE---1.7
% 60.85/61.57 % Problem :theBenchmark
% 60.85/61.57 % Transform :cnf
% 60.85/61.57 % Format :tptp:raw
% 60.85/61.57 % Command :java -jar mcs_scs.jar %d %s
% 60.85/61.57
% 60.85/61.57 % Result :Theorem 60.240000s
% 60.85/61.57 % Output :CNFRefutation 60.240000s
% 60.85/61.57 %-------------------------------------------
% 60.85/61.58 %------------------------------------------------------------------------------
% 60.85/61.58 % File : GEO601+1 : TPTP v8.2.0. Released v7.5.0.
% 60.85/61.58 % Domain : Geometry
% 60.85/61.58 % Problem : JGEX problem 63f
% 60.85/61.58 % Version : [CGZ00] axioms.
% 60.85/61.58 % English :
% 60.85/61.58
% 60.85/61.58 % Refs : [CGZ00] Chou et al. (2000), A Deductive Database Approach to A
% 60.85/61.58 % : [YCG08] Ye et al. (2008), An Introduction to Java Geometry Exp
% 60.85/61.58 % : [Qua20] Quaresma (2020), Email to Geoff Sutcliffe
% 60.85/61.58 % Source : [Qua20]
% 60.85/61.58 % Names : 63f.p [Qua20]
% 60.85/61.58
% 60.85/61.58 % Status : Theorem
% 60.85/61.58 % Rating : 0.39 v8.2.0, 0.36 v8.1.0, 0.47 v7.5.0
% 60.85/61.58 % Syntax : Number of formulae : 95 ( 0 unt; 0 def)
% 60.85/61.58 % Number of atoms : 288 ( 1 equ)
% 60.85/61.58 % Maximal formula atoms : 8 ( 3 avg)
% 60.85/61.58 % Number of connectives : 200 ( 7 ~; 0 |; 98 &)
% 60.85/61.58 % ( 0 <=>; 95 =>; 0 <=; 0 <~>)
% 60.85/61.58 % Maximal formula depth : 15 ( 9 avg)
% 60.85/61.58 % Maximal term depth : 1 ( 1 avg)
% 60.85/61.58 % Number of predicates : 12 ( 11 usr; 0 prp; 2-8 aty)
% 60.85/61.58 % Number of functors : 0 ( 0 usr; 0 con; --- aty)
% 60.85/61.58 % Number of variables : 529 ( 509 !; 20 ?)
% 60.85/61.58 % SPC : FOF_THM_RFO_SEQ
% 60.85/61.58
% 60.85/61.58 % Comments : Taken from JGEX [YCG08], converted by Pedro Quaresma.
% 60.85/61.58 %------------------------------------------------------------------------------
% 60.85/61.58 include('Axioms/GEO012+0.ax').
% 60.85/61.58 %------------------------------------------------------------------------------
% 60.85/61.58 fof(exemplo6GDDFULL618063f,conjecture,
% 60.85/61.58 ! [A,B,C,D,E,F,G] :
% 60.85/61.58 ( ( coll(D,B,C)
% 60.85/61.58 & circle(E,A,D,C)
% 60.85/61.58 & circle(F,A,D,B)
% 60.85/61.58 & circle(G,B,A,C) )
% 60.85/61.58 => cyclic(A,F,G,E) ) ).
% 60.85/61.58
% 60.85/61.58 %------------------------------------------------------------------------------
% 60.85/61.58 %-------------------------------------------
% 60.85/61.58 % Proof found
% 60.85/61.58 % SZS status Theorem for theBenchmark
% 60.85/61.58 % SZS output start Proof
% 60.87/61.60 %ClaNum:259(EqnAxiom:141)
% 60.87/61.60 %VarNum:1613(SingletonVarNum:590)
% 60.87/61.60 %MaxLitNum:5
% 60.87/61.60 %MaxfuncDepth:1
% 60.87/61.60 %SharedTerms:12
% 60.87/61.60 %goalClause: 142 143 144 145 146
% 60.87/61.60 %singleGoalClaCount:5
% 60.87/61.60 [142]P1(a1,a2,a16)
% 60.87/61.60 [143]P2(a17,a3,a1,a16)
% 60.87/61.60 [144]P2(a18,a3,a1,a2)
% 60.87/61.60 [145]P2(a19,a2,a3,a16)
% 60.87/61.60 [146]~P3(a3,a18,a19,a17)
% 60.87/61.60 [147]~P1(x1472,x1471,x1473)+P1(x1471,x1472,x1473)
% 60.87/61.60 [148]~P1(x1481,x1483,x1482)+P1(x1481,x1482,x1483)
% 60.87/61.60 [149]~P6(x1491,x1492,x1493)+P1(x1491,x1492,x1493)
% 60.87/61.60 [150]~P6(x1501,x1503,x1502)+P6(x1501,x1502,x1503)
% 60.87/61.60 [152]~P6(x1521,x1522,x1523)+P4(x1521,x1522,x1521,x1523)
% 60.87/61.60 [156]~P9(x1561,x1562,x1561,x1563)+P1(x1561,x1562,x1563)
% 60.87/61.60 [222]~P4(x2221,x2222,x2221,x2223)+P8(x2221,x2222,x2222,x2223,x2222,x2223,x2221,x2223)
% 60.87/61.60 [159]~P9(x1593,x1594,x1591,x1592)+P9(x1591,x1592,x1593,x1594)
% 60.87/61.60 [160]~P9(x1601,x1602,x1604,x1603)+P9(x1601,x1602,x1603,x1604)
% 60.87/61.60 [161]~P10(x1613,x1614,x1611,x1612)+P10(x1611,x1612,x1613,x1614)
% 60.87/61.60 [162]~P10(x1621,x1622,x1624,x1623)+P10(x1621,x1622,x1623,x1624)
% 60.87/61.60 [163]~P4(x1633,x1634,x1631,x1632)+P4(x1631,x1632,x1633,x1634)
% 60.87/61.60 [164]~P4(x1641,x1642,x1644,x1643)+P4(x1641,x1642,x1643,x1644)
% 60.87/61.60 [165]~P3(x1652,x1651,x1653,x1654)+P3(x1651,x1652,x1653,x1654)
% 60.87/61.60 [166]~P3(x1661,x1663,x1662,x1664)+P3(x1661,x1662,x1663,x1664)
% 60.87/61.60 [167]~P3(x1671,x1672,x1674,x1673)+P3(x1671,x1672,x1673,x1674)
% 60.87/61.60 [220]~P3(x2202,x2203,x2201,x2204)+P8(x2201,x2202,x2201,x2203,x2204,x2202,x2204,x2203)
% 60.87/61.60 [183]~P2(x1834,x1831,x1832,x1833)+P10(f8(x1831,x1832,x1833,x1834),x1831,x1831,x1834)
% 60.87/61.60 [198]P4(x1981,x1982,x1983,x1984)+~P5(x1981,x1982,x1985,x1983,x1984,x1986)
% 60.87/61.60 [210]~P11(x2104,x2105,x2106,x2101,x2102,x2103)+P11(x2101,x2102,x2103,x2104,x2105,x2106)
% 60.87/61.60 [211]~P11(x2112,x2111,x2113,x2115,x2114,x2116)+P11(x2111,x2112,x2113,x2114,x2115,x2116)
% 60.87/61.60 [212]~P11(x2121,x2123,x2122,x2124,x2126,x2125)+P11(x2121,x2122,x2123,x2124,x2125,x2126)
% 60.87/61.60 [213]~P5(x2134,x2135,x2136,x2131,x2132,x2133)+P5(x2131,x2132,x2133,x2134,x2135,x2136)
% 60.87/61.60 [214]~P5(x2142,x2141,x2143,x2145,x2144,x2146)+P5(x2141,x2142,x2143,x2144,x2145,x2146)
% 60.87/61.60 [215]~P5(x2151,x2153,x2152,x2154,x2156,x2155)+P5(x2151,x2152,x2153,x2154,x2155,x2156)
% 60.87/61.60 [221]~P9(x2211,x2212,x2215,x2216)+P8(x2211,x2212,x2213,x2214,x2215,x2216,x2213,x2214)
% 60.87/61.60 [227]~P11(x2271,x2272,x2273,x2274,x2275,x2276)+P8(x2271,x2272,x2272,x2273,x2274,x2275,x2275,x2276)
% 60.87/61.60 [228]~P11(x2281,x2282,x2283,x2284,x2285,x2286)+P7(x2281,x2282,x2281,x2283,x2284,x2285,x2284,x2286)
% 60.87/61.60 [229]~P8(x2291,x2292,x2295,x2296,x2293,x2294,x2295,x2296)+P9(x2291,x2292,x2293,x2294)
% 60.87/61.60 [248]~P8(x2485,x2486,x2487,x2488,x2481,x2482,x2483,x2484)+P8(x2481,x2482,x2483,x2484,x2485,x2486,x2487,x2488)
% 60.87/61.60 [249]~P8(x2493,x2494,x2491,x2492,x2497,x2498,x2495,x2496)+P8(x2491,x2492,x2493,x2494,x2495,x2496,x2497,x2498)
% 60.87/61.60 [250]~P8(x2502,x2501,x2503,x2504,x2505,x2506,x2507,x2508)+P8(x2501,x2502,x2503,x2504,x2505,x2506,x2507,x2508)
% 60.87/61.60 [251]~P8(x2511,x2512,x2515,x2516,x2513,x2514,x2517,x2518)+P8(x2511,x2512,x2513,x2514,x2515,x2516,x2517,x2518)
% 60.87/61.60 [252]~P7(x2525,x2526,x2527,x2528,x2521,x2522,x2523,x2524)+P7(x2521,x2522,x2523,x2524,x2525,x2526,x2527,x2528)
% 60.87/61.60 [253]~P7(x2533,x2534,x2531,x2532,x2537,x2538,x2535,x2536)+P7(x2531,x2532,x2533,x2534,x2535,x2536,x2537,x2538)
% 60.87/61.60 [254]~P7(x2542,x2541,x2543,x2544,x2545,x2546,x2547,x2548)+P7(x2541,x2542,x2543,x2544,x2545,x2546,x2547,x2548)
% 60.87/61.60 [255]~P7(x2551,x2552,x2555,x2556,x2553,x2554,x2557,x2558)+P7(x2551,x2552,x2553,x2554,x2555,x2556,x2557,x2558)
% 60.87/61.60 [157]~P1(x1571,x1572,x1573)+~P4(x1571,x1572,x1571,x1573)+P6(x1571,x1572,x1573)
% 60.87/61.60 [231]P4(x2311,x2312,x2311,x2313)+~P8(x2311,x2312,x2312,x2313,x2312,x2313,x2311,x2313)+P1(x2311,x2312,x2313)
% 60.87/61.60 [172]~P10(x1721,x1722,x1722,x1723)+~P4(x1722,x1721,x1722,x1723)+P1(x1721,x1722,f4(x1721,x1723,x1722))
% 60.87/61.60 [184]~P10(x1842,x1841,x1841,x1843)+~P4(x1841,x1842,x1841,x1843)+P4(x1841,x1842,x1841,f4(x1842,x1843,x1841))
% 60.87/61.60 [151]~P1(x1513,x1514,x1511)+P1(x1511,x1512,x1513)+~P1(x1513,x1514,x1512)
% 60.87/61.60 [168]~P2(x1684,x1681,x1682,x1683)+P10(x1681,x1682,x1682,x1683)+~P1(x1684,x1681,x1683)
% 60.87/61.60 [169]~P10(x1691,x1694,x1692,x1693)+P4(x1691,x1692,x1691,x1693)+~P6(x1694,x1692,x1693)
% 60.87/61.60 [170]~P10(x1701,x1703,x1703,x1704)+P4(x1701,x1702,x1703,x1702)+~P6(x1702,x1701,x1704)
% 60.87/61.60 [177]~P4(x1771,x1774,x1772,x1774)+~P4(x1771,x1773,x1772,x1773)+P10(x1771,x1772,x1773,x1774)
% 60.87/61.60 [180]~P4(x1801,x1802,x1801,x1804)+~P4(x1801,x1802,x1801,x1803)+P2(x1801,x1802,x1803,x1804)
% 60.87/61.60 [226]~P9(x2261,x2264,x2263,x2262)+~P3(x2261,x2264,x2263,x2262)+P8(x2261,x2262,x2263,x2262,x2263,x2262,x2263,x2264)
% 60.87/61.60 [230]~P8(x2301,x2303,x2301,x2304,x2302,x2303,x2302,x2304)+P1(x2301,x2302,x2303)+P3(x2303,x2304,x2301,x2302)
% 60.87/61.60 [232]~P1(x2323,x2324,x2322)+~P8(x2323,x2321,x2323,x2322,x2324,x2321,x2324,x2322)+P3(x2321,x2322,x2323,x2324)
% 60.87/61.60 [234]P10(x2341,x2342,x2343,x2344)+~P8(x2341,x2342,x2343,x2344,x2343,x2344,x2341,x2342)+P9(x2341,x2342,x2343,x2344)
% 60.87/61.60 [173]~P10(x1731,x1734,x1732,x1733)+~P10(x1732,x1734,x1731,x1733)+P1(f5(x1731,x1732,x1733),x1733,x1732)
% 60.87/61.60 [174]~P10(x1741,x1744,x1742,x1743)+~P10(x1742,x1744,x1741,x1743)+P1(f6(x1741,x1742,x1743),x1743,x1741)
% 60.87/61.60 [185]~P10(x1851,x1854,x1852,x1853)+~P10(x1852,x1854,x1851,x1853)+P10(x1851,f5(x1851,x1852,x1853),x1853,x1852)
% 60.87/61.60 [186]~P10(x1861,x1864,x1862,x1863)+~P10(x1862,x1864,x1861,x1863)+P10(x1861,f6(x1862,x1861,x1863),x1863,x1862)
% 60.87/61.60 [187]~P10(x1871,x1873,x1873,x1872)+~P3(x1871,x1872,x1873,x1874)+P2(f9(x1871,x1872,x1873),x1871,x1872,x1873)
% 60.87/61.60 [189]~P10(x1893,x1894,x1892,x1891)+~P4(x1893,x1892,x1893,x1891)+P1(x1891,x1892,f21(x1892,x1891,x1893,x1894))
% 60.87/61.60 [190]~P10(x1903,x1904,x1901,x1902)+~P4(x1903,x1901,x1903,x1902)+P1(f21(x1901,x1902,x1903,x1904),x1903,x1904)
% 60.87/61.60 [241]~P4(x2413,x2412,x2413,x2411)+~P8(x2412,x2413,x2413,x2414,x2413,x2414,x2413,x2411)+P1(x2411,x2412,f22(x2412,x2411,x2413,x2414))
% 60.87/61.60 [242]~P10(x2423,x2424,x2422,x2421)+~P8(x2422,x2423,x2423,x2424,x2423,x2424,x2423,x2421)+P1(x2421,x2422,f23(x2422,x2421,x2423,x2424))
% 60.87/61.60 [243]~P10(x2433,x2432,x2432,x2431)+~P8(x2434,x2433,x2432,x2433,x2432,x2433,x2431,x2433)+P1(f15(x2431,x2432,x2433,x2434),x2433,x2434)
% 60.87/61.60 [244]~P10(x2443,x2442,x2442,x2441)+~P8(x2444,x2443,x2442,x2443,x2442,x2443,x2441,x2443)+P1(f15(x2441,x2442,x2443,x2444),x2441,x2442)
% 60.87/61.60 [245]~P4(x2453,x2451,x2453,x2452)+~P8(x2451,x2453,x2453,x2454,x2453,x2454,x2453,x2452)+P1(f22(x2451,x2452,x2453,x2454),x2453,x2454)
% 60.87/61.60 [246]~P10(x2463,x2464,x2461,x2462)+~P8(x2461,x2463,x2463,x2464,x2463,x2464,x2463,x2462)+P1(f23(x2461,x2462,x2463,x2464),x2463,x2464)
% 60.87/61.60 [153]~P6(x1535,x1531,x1533)+P9(x1531,x1532,x1533,x1534)+~P6(x1535,x1532,x1534)
% 60.87/61.60 [154]~P6(x1541,x1545,x1543)+P9(x1541,x1542,x1543,x1544)+~P6(x1542,x1545,x1544)
% 60.87/61.60 [181]~P3(x1815,x1811,x1812,x1813)+P3(x1811,x1812,x1813,x1814)+~P3(x1815,x1811,x1812,x1814)
% 60.87/61.60 [223]~P6(x2235,x2232,x2233)+~P2(x2234,x2231,x2232,x2233)+P8(x2231,x2232,x2231,x2233,x2234,x2232,x2234,x2235)
% 60.87/61.60 [225]~P2(x2255,x2251,x2253,x2254)+P8(x2251,x2252,x2251,x2253,x2254,x2251,x2254,x2253)+~P10(x2255,x2251,x2251,x2252)
% 60.87/61.60 [238]~P8(x2382,x2383,x2382,x2384,x2385,x2382,x2385,x2384)+P10(x2381,x2382,x2382,x2383)+~P2(x2381,x2382,x2384,x2385)
% 60.87/61.60 [193]~P1(x1932,x1934,x1935)+~P10(x1931,x1933,x1933,x1932)+P1(f13(x1931,x1932,x1933,x1934,x1935),x1934,x1935)
% 60.87/61.60 [194]~P1(x1942,x1944,x1945)+~P10(x1941,x1943,x1943,x1942)+P10(f13(x1941,x1942,x1943,x1944,x1945),x1941,x1944,x1945)
% 60.87/61.60 [195]~P10(x1953,x1954,x1954,x1951)+~P4(x1951,x1952,x1951,x1955)+P4(x1951,x1952,x1951,f26(x1953,x1954,x1952,x1955,x1951))
% 60.87/61.60 [196]~P10(x1963,x1961,x1961,x1965)+~P4(x1965,x1962,x1965,x1964)+P4(x1961,x1962,x1961,f26(x1963,x1961,x1962,x1964,x1965))
% 60.87/61.60 [197]~P10(x1971,x1972,x1972,x1975)+~P4(x1975,x1973,x1975,x1974)+P9(f26(x1971,x1972,x1973,x1974,x1975),x1973,x1971,x1972)
% 60.87/61.60 [240]~P8(x2401,x2403,x2402,x2403,x2401,x2404,x2402,x2405)+P1(x2401,x2402,x2403)+P3(x2404,x2402,x2403,f25(x2401,x2402,x2403,x2404))
% 60.87/61.60 [256]~P8(x2561,x2563,x2562,x2563,x2561,x2564,x2562,x2565)+P1(x2561,x2562,x2563)+P8(x2561,x2563,x2562,x2563,x2561,f25(x2561,x2562,x2563,x2564),x2562,f25(x2561,x2562,x2563,x2564))
% 60.87/61.60 [175]~P9(x1751,x1752,x1755,x1756)+P9(x1751,x1752,x1753,x1754)+~P9(x1755,x1756,x1753,x1754)
% 60.87/61.60 [176]~P10(x1761,x1762,x1765,x1766)+P9(x1761,x1762,x1763,x1764)+~P10(x1765,x1766,x1763,x1764)
% 60.87/61.60 [178]~P10(x1785,x1786,x1783,x1784)+P10(x1781,x1782,x1783,x1784)+~P9(x1781,x1782,x1785,x1786)
% 60.87/61.60 [179]~P4(x1791,x1792,x1795,x1796)+P4(x1791,x1792,x1793,x1794)+~P4(x1795,x1796,x1793,x1794)
% 60.87/61.60 [216]~P4(x2161,x2162,x2164,x2165)+~P11(x2161,x2162,x2163,x2164,x2165,x2166)+P5(x2161,x2162,x2163,x2164,x2165,x2166)
% 60.87/61.60 [219]~P6(x2194,x2195,x2196)+~P6(x2191,x2192,x2193)+P7(x2191,x2192,x2192,x2193,x2194,x2195,x2195,x2196)
% 60.87/61.60 [199]~P6(x1996,x1993,x1994)+~P6(x1995,x1991,x1992)+P6(f24(x1991,x1992,x1993,x1994,x1995,x1996),x1991,x1994)
% 60.87/61.60 [200]~P6(x2006,x2003,x2004)+~P6(x2005,x2001,x2002)+P9(f24(x2001,x2002,x2003,x2004,x2005,x2006),x2006,x2001,x2003)
% 60.87/61.60 [201]~P6(x2016,x2013,x2014)+~P6(x2015,x2011,x2012)+P9(f24(x2011,x2012,x2013,x2014,x2015,x2016),x2015,x2012,x2014)
% 60.87/61.60 [236]~P8(x2361,x2362,x2363,x2364,x2365,x2366,x2367,x2368)+P9(x2361,x2362,x2363,x2364)+~P9(x2365,x2366,x2367,x2368)
% 60.87/61.60 [237]~P8(x2371,x2372,x2373,x2374,x2375,x2376,x2377,x2378)+P10(x2371,x2372,x2373,x2374)+~P10(x2375,x2376,x2377,x2378)
% 60.87/61.60 [239]~P7(x2391,x2392,x2393,x2394,x2395,x2396,x2397,x2398)+P4(x2391,x2392,x2393,x2394)+~P4(x2395,x2396,x2397,x2398)
% 60.87/61.60 [217]~P11(x2171,x2172,x2173,x2177,x2178,x2179)+P11(x2171,x2172,x2173,x2174,x2175,x2176)+~P11(x2177,x2178,x2179,x2174,x2175,x2176)
% 60.87/61.60 [218]~P5(x2181,x2182,x2183,x2187,x2188,x2189)+P5(x2181,x2182,x2183,x2184,x2185,x2186)+~P5(x2187,x2188,x2189,x2184,x2185,x2186)
% 60.87/61.60 [258]~P8(x2581,x2582,x2583,x2584,x2589,x25810,x25811,x25812)+P8(x2581,x2582,x2583,x2584,x2585,x2586,x2587,x2588)+~P8(x2589,x25810,x25811,x25812,x2585,x2586,x2587,x2588)
% 60.87/61.60 [259]~P7(x2591,x2592,x2593,x2594,x2599,x25910,x25911,x25912)+P7(x2591,x2592,x2593,x2594,x2595,x2596,x2597,x2598)+~P7(x2599,x25910,x25911,x25912,x2595,x2596,x2597,x2598)
% 60.87/61.60 [191]~P4(x1912,x1911,x1914,x1911)+~P3(x1912,x1914,x1911,x1913)+P10(x1911,x1912,x1912,x1913)+~P4(x1912,x1913,x1914,x1913)
% 60.87/61.60 [158]~P1(x1581,x1582,x1583)+~P9(x1584,x1581,x1585,x1583)+P6(x1581,x1582,x1583)+~P6(x1584,x1582,x1585)
% 60.87/61.60 [171]~P9(x1714,x1713,x1715,x1712)+~P9(x1714,x1712,x1715,x1713)+P6(x1711,x1712,x1713)+~P6(x1711,x1714,x1715)
% 60.87/61.60 [192]~P4(x1925,x1921,x1925,x1923)+~P4(x1925,x1921,x1925,x1922)+P3(x1921,x1922,x1923,x1924)+~P4(x1925,x1921,x1925,x1924)
% 60.87/61.60 [224]~P1(x2241,x2244,x2245)+~P1(x2241,x2242,x2243)+~P9(x2242,x2244,x2243,x2245)+P7(x2241,x2242,x2242,x2243,x2241,x2244,x2244,x2245)
% 60.87/61.60 [235]~P1(x2351,x2352,x2353)+~P8(x2355,x2352,x2355,x2353,x2354,x2352,x2354,x2351)+P6(x2351,x2352,x2353)+~P2(x2354,x2355,x2352,x2353)
% 60.87/61.60 [182]~P10(x1823,x1821,x1823,x1825)+~P10(x1821,x1822,x1821,x1823)+~P6(x1824,x1822,x1825)+P6(f7(x1821,x1822,x1823),x1821,x1823)
% 60.87/61.60 [188]~P3(x1881,x1882,x1883,x1885)+~P9(x1881,x1882,x1883,x1885)+~P6(x1884,x1881,x1882)+P2(f10(x1881,x1882,x1883),x1881,x1882,x1883)
% 60.87/61.60 [257]~P8(x2571,x2573,x2572,x2573,x2574,x2576,x2575,x2576)+~P8(x2571,x2572,x2572,x2573,x2574,x2575,x2575,x2576)+P1(x2571,x2572,x2573)+P11(x2571,x2572,x2573,x2574,x2575,x2576)
% 60.87/61.60 [247]~P3(x2471,x2472,x2475,x2474)+~P3(x2471,x2472,x2475,x2473)+~P8(x2475,x2471,x2475,x2472,x2476,x2473,x2476,x2474)+P4(x2471,x2472,x2473,x2474)+~P3(x2471,x2472,x2475,x2476)
% 60.87/61.60 [202]~P1(x2022,x2023,x2024)+~P1(x2021,x2024,x2026)+~P1(x2021,x2023,x2025)+~P9(x2023,x2024,x2025,x2026)+P1(x2021,x2022,f14(x2023,x2024,x2025,x2026,x2021,x2022))
% 60.87/61.60 [203]~P1(x2036,x2031,x2032)+~P1(x2035,x2032,x2034)+~P1(x2035,x2031,x2033)+~P9(x2031,x2032,x2033,x2034)+P1(f14(x2031,x2032,x2033,x2034,x2035,x2036),x2033,x2034)
% 60.87/61.60 [204]~P1(x2043,x2044,x2045)+~P6(x2046,x2041,x2042)+~P9(x2041,x2043,x2045,x2046)+~P9(x2041,x2043,x2042,x2044)+P1(f27(x2041,x2042,x2043,x2044,x2045,x2046),x2046,x2045)
% 60.87/61.60 [205]~P1(x2053,x2054,x2055)+~P6(x2056,x2051,x2052)+~P9(x2051,x2053,x2055,x2056)+~P9(x2051,x2053,x2052,x2054)+P1(f27(x2051,x2052,x2053,x2054,x2055,x2056),x2051,x2054)
% 60.87/61.60 [206]~P4(x2062,x2063,x2062,x2064)+~P4(x2061,x2063,x2061,x2066)+~P2(x2061,x2063,x2064,x2065)+E(x2061,x2062)+P1(f11(x2063,x2064,x2065,x2066,x2061,x2062),x2063,x2065)
% 60.87/61.60 [207]~P4(x2072,x2073,x2072,x2074)+~P4(x2071,x2073,x2071,x2076)+~P2(x2071,x2073,x2074,x2075)+E(x2071,x2072)+P1(f12(x2073,x2074,x2075,x2076,x2071,x2072),x2074,x2076)
% 60.87/61.60 [208]~P4(x2082,x2083,x2082,x2084)+~P4(x2081,x2083,x2081,x2086)+~P2(x2081,x2083,x2084,x2085)+E(x2081,x2082)+P4(f11(x2083,x2084,x2085,x2086,x2081,x2082),x2082,x2082,x2083)
% 60.87/61.60 [209]~P4(x2092,x2093,x2092,x2094)+~P4(x2091,x2093,x2091,x2096)+~P2(x2091,x2093,x2094,x2095)+E(x2091,x2092)+P4(f12(x2093,x2094,x2095,x2096,x2091,x2092),x2092,x2092,x2093)
% 60.87/61.60 [155]~P1(x1553,x1551,x1554)+~P1(x1555,x1551,x1554)+~P6(x1556,x1555,x1553)+~P6(x1557,x1551,x1554)+P6(f20(x1551,x1552),x1551,x1552)
% 60.87/61.60 %EqnAxiom
% 60.87/61.60 [1]E(x11,x11)
% 60.87/61.60 [2]E(x22,x21)+~E(x21,x22)
% 60.87/61.60 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 60.87/61.60 [4]~E(x41,x42)+E(f20(x41,x43),f20(x42,x43))
% 60.87/61.60 [5]~E(x51,x52)+E(f20(x53,x51),f20(x53,x52))
% 60.87/61.60 [6]~E(x61,x62)+E(f4(x61,x63,x64),f4(x62,x63,x64))
% 60.87/61.60 [7]~E(x71,x72)+E(f4(x73,x71,x74),f4(x73,x72,x74))
% 60.87/61.60 [8]~E(x81,x82)+E(f4(x83,x84,x81),f4(x83,x84,x82))
% 60.87/61.60 [9]~E(x91,x92)+E(f5(x91,x93,x94),f5(x92,x93,x94))
% 60.87/61.60 [10]~E(x101,x102)+E(f5(x103,x101,x104),f5(x103,x102,x104))
% 60.87/61.60 [11]~E(x111,x112)+E(f5(x113,x114,x111),f5(x113,x114,x112))
% 60.87/61.60 [12]~E(x121,x122)+E(f6(x121,x123,x124),f6(x122,x123,x124))
% 60.87/61.60 [13]~E(x131,x132)+E(f6(x133,x131,x134),f6(x133,x132,x134))
% 60.87/61.60 [14]~E(x141,x142)+E(f6(x143,x144,x141),f6(x143,x144,x142))
% 60.87/61.60 [15]~E(x151,x152)+E(f7(x151,x153,x154),f7(x152,x153,x154))
% 60.87/61.60 [16]~E(x161,x162)+E(f7(x163,x161,x164),f7(x163,x162,x164))
% 60.87/61.60 [17]~E(x171,x172)+E(f7(x173,x174,x171),f7(x173,x174,x172))
% 60.87/61.60 [18]~E(x181,x182)+E(f8(x181,x183,x184,x185),f8(x182,x183,x184,x185))
% 60.87/61.60 [19]~E(x191,x192)+E(f8(x193,x191,x194,x195),f8(x193,x192,x194,x195))
% 60.87/61.60 [20]~E(x201,x202)+E(f8(x203,x204,x201,x205),f8(x203,x204,x202,x205))
% 60.87/61.60 [21]~E(x211,x212)+E(f8(x213,x214,x215,x211),f8(x213,x214,x215,x212))
% 60.87/61.60 [22]~E(x221,x222)+E(f25(x221,x223,x224,x225),f25(x222,x223,x224,x225))
% 60.87/61.60 [23]~E(x231,x232)+E(f25(x233,x231,x234,x235),f25(x233,x232,x234,x235))
% 60.87/61.60 [24]~E(x241,x242)+E(f25(x243,x244,x241,x245),f25(x243,x244,x242,x245))
% 60.87/61.60 [25]~E(x251,x252)+E(f25(x253,x254,x255,x251),f25(x253,x254,x255,x252))
% 60.87/61.60 [26]~E(x261,x262)+E(f22(x261,x263,x264,x265),f22(x262,x263,x264,x265))
% 60.87/61.60 [27]~E(x271,x272)+E(f22(x273,x271,x274,x275),f22(x273,x272,x274,x275))
% 60.87/61.60 [28]~E(x281,x282)+E(f22(x283,x284,x281,x285),f22(x283,x284,x282,x285))
% 60.87/61.60 [29]~E(x291,x292)+E(f22(x293,x294,x295,x291),f22(x293,x294,x295,x292))
% 60.87/61.60 [30]~E(x301,x302)+E(f23(x301,x303,x304,x305),f23(x302,x303,x304,x305))
% 60.87/61.60 [31]~E(x311,x312)+E(f23(x313,x311,x314,x315),f23(x313,x312,x314,x315))
% 60.87/61.60 [32]~E(x321,x322)+E(f23(x323,x324,x321,x325),f23(x323,x324,x322,x325))
% 60.87/61.60 [33]~E(x331,x332)+E(f23(x333,x334,x335,x331),f23(x333,x334,x335,x332))
% 60.87/61.60 [34]~E(x341,x342)+E(f9(x341,x343,x344),f9(x342,x343,x344))
% 60.87/61.60 [35]~E(x351,x352)+E(f9(x353,x351,x354),f9(x353,x352,x354))
% 60.87/61.60 [36]~E(x361,x362)+E(f9(x363,x364,x361),f9(x363,x364,x362))
% 60.87/61.60 [37]~E(x371,x372)+E(f10(x371,x373,x374),f10(x372,x373,x374))
% 60.87/61.60 [38]~E(x381,x382)+E(f10(x383,x381,x384),f10(x383,x382,x384))
% 60.87/61.60 [39]~E(x391,x392)+E(f10(x393,x394,x391),f10(x393,x394,x392))
% 60.87/61.60 [40]~E(x401,x402)+E(f21(x401,x403,x404,x405),f21(x402,x403,x404,x405))
% 60.87/61.60 [41]~E(x411,x412)+E(f21(x413,x411,x414,x415),f21(x413,x412,x414,x415))
% 60.87/61.60 [42]~E(x421,x422)+E(f21(x423,x424,x421,x425),f21(x423,x424,x422,x425))
% 60.87/61.60 [43]~E(x431,x432)+E(f21(x433,x434,x435,x431),f21(x433,x434,x435,x432))
% 60.87/61.60 [44]~E(x441,x442)+E(f15(x441,x443,x444,x445),f15(x442,x443,x444,x445))
% 60.87/61.60 [45]~E(x451,x452)+E(f15(x453,x451,x454,x455),f15(x453,x452,x454,x455))
% 60.87/61.60 [46]~E(x461,x462)+E(f15(x463,x464,x461,x465),f15(x463,x464,x462,x465))
% 60.87/61.60 [47]~E(x471,x472)+E(f15(x473,x474,x475,x471),f15(x473,x474,x475,x472))
% 60.87/61.60 [48]~E(x481,x482)+E(f13(x481,x483,x484,x485,x486),f13(x482,x483,x484,x485,x486))
% 60.87/61.60 [49]~E(x491,x492)+E(f13(x493,x491,x494,x495,x496),f13(x493,x492,x494,x495,x496))
% 60.87/61.60 [50]~E(x501,x502)+E(f13(x503,x504,x501,x505,x506),f13(x503,x504,x502,x505,x506))
% 60.87/61.60 [51]~E(x511,x512)+E(f13(x513,x514,x515,x511,x516),f13(x513,x514,x515,x512,x516))
% 60.87/61.60 [52]~E(x521,x522)+E(f13(x523,x524,x525,x526,x521),f13(x523,x524,x525,x526,x522))
% 60.87/61.60 [53]~E(x531,x532)+E(f12(x531,x533,x534,x535,x536,x537),f12(x532,x533,x534,x535,x536,x537))
% 60.87/61.60 [54]~E(x541,x542)+E(f12(x543,x541,x544,x545,x546,x547),f12(x543,x542,x544,x545,x546,x547))
% 60.87/61.60 [55]~E(x551,x552)+E(f12(x553,x554,x551,x555,x556,x557),f12(x553,x554,x552,x555,x556,x557))
% 60.87/61.60 [56]~E(x561,x562)+E(f12(x563,x564,x565,x561,x566,x567),f12(x563,x564,x565,x562,x566,x567))
% 60.87/61.60 [57]~E(x571,x572)+E(f12(x573,x574,x575,x576,x571,x577),f12(x573,x574,x575,x576,x572,x577))
% 60.87/61.60 [58]~E(x581,x582)+E(f12(x583,x584,x585,x586,x587,x581),f12(x583,x584,x585,x586,x587,x582))
% 60.87/61.60 [59]~E(x591,x592)+E(f26(x591,x593,x594,x595,x596),f26(x592,x593,x594,x595,x596))
% 60.87/61.60 [60]~E(x601,x602)+E(f26(x603,x601,x604,x605,x606),f26(x603,x602,x604,x605,x606))
% 60.87/61.60 [61]~E(x611,x612)+E(f26(x613,x614,x611,x615,x616),f26(x613,x614,x612,x615,x616))
% 60.87/61.60 [62]~E(x621,x622)+E(f26(x623,x624,x625,x621,x626),f26(x623,x624,x625,x622,x626))
% 60.87/61.60 [63]~E(x631,x632)+E(f26(x633,x634,x635,x636,x631),f26(x633,x634,x635,x636,x632))
% 60.87/61.60 [64]~E(x641,x642)+E(f11(x641,x643,x644,x645,x646,x647),f11(x642,x643,x644,x645,x646,x647))
% 60.87/61.60 [65]~E(x651,x652)+E(f11(x653,x651,x654,x655,x656,x657),f11(x653,x652,x654,x655,x656,x657))
% 60.87/61.60 [66]~E(x661,x662)+E(f11(x663,x664,x661,x665,x666,x667),f11(x663,x664,x662,x665,x666,x667))
% 60.87/61.61 [67]~E(x671,x672)+E(f11(x673,x674,x675,x671,x676,x677),f11(x673,x674,x675,x672,x676,x677))
% 60.87/61.61 [68]~E(x681,x682)+E(f11(x683,x684,x685,x686,x681,x687),f11(x683,x684,x685,x686,x682,x687))
% 60.87/61.61 [69]~E(x691,x692)+E(f11(x693,x694,x695,x696,x697,x691),f11(x693,x694,x695,x696,x697,x692))
% 60.87/61.61 [70]~E(x701,x702)+E(f27(x701,x703,x704,x705,x706,x707),f27(x702,x703,x704,x705,x706,x707))
% 60.87/61.61 [71]~E(x711,x712)+E(f27(x713,x711,x714,x715,x716,x717),f27(x713,x712,x714,x715,x716,x717))
% 60.87/61.61 [72]~E(x721,x722)+E(f27(x723,x724,x721,x725,x726,x727),f27(x723,x724,x722,x725,x726,x727))
% 60.87/61.61 [73]~E(x731,x732)+E(f27(x733,x734,x735,x731,x736,x737),f27(x733,x734,x735,x732,x736,x737))
% 60.87/61.61 [74]~E(x741,x742)+E(f27(x743,x744,x745,x746,x741,x747),f27(x743,x744,x745,x746,x742,x747))
% 60.87/61.61 [75]~E(x751,x752)+E(f27(x753,x754,x755,x756,x757,x751),f27(x753,x754,x755,x756,x757,x752))
% 60.87/61.61 [76]~E(x761,x762)+E(f24(x761,x763,x764,x765,x766,x767),f24(x762,x763,x764,x765,x766,x767))
% 60.87/61.61 [77]~E(x771,x772)+E(f24(x773,x771,x774,x775,x776,x777),f24(x773,x772,x774,x775,x776,x777))
% 60.87/61.61 [78]~E(x781,x782)+E(f24(x783,x784,x781,x785,x786,x787),f24(x783,x784,x782,x785,x786,x787))
% 60.87/61.61 [79]~E(x791,x792)+E(f24(x793,x794,x795,x791,x796,x797),f24(x793,x794,x795,x792,x796,x797))
% 60.87/61.61 [80]~E(x801,x802)+E(f24(x803,x804,x805,x806,x801,x807),f24(x803,x804,x805,x806,x802,x807))
% 60.87/61.61 [81]~E(x811,x812)+E(f24(x813,x814,x815,x816,x817,x811),f24(x813,x814,x815,x816,x817,x812))
% 60.87/61.61 [82]~E(x821,x822)+E(f14(x821,x823,x824,x825,x826,x827),f14(x822,x823,x824,x825,x826,x827))
% 60.87/61.61 [83]~E(x831,x832)+E(f14(x833,x831,x834,x835,x836,x837),f14(x833,x832,x834,x835,x836,x837))
% 60.87/61.61 [84]~E(x841,x842)+E(f14(x843,x844,x841,x845,x846,x847),f14(x843,x844,x842,x845,x846,x847))
% 60.87/61.61 [85]~E(x851,x852)+E(f14(x853,x854,x855,x851,x856,x857),f14(x853,x854,x855,x852,x856,x857))
% 60.87/61.61 [86]~E(x861,x862)+E(f14(x863,x864,x865,x866,x861,x867),f14(x863,x864,x865,x866,x862,x867))
% 60.87/61.61 [87]~E(x871,x872)+E(f14(x873,x874,x875,x876,x877,x871),f14(x873,x874,x875,x876,x877,x872))
% 60.87/61.61 [88]P1(x882,x883,x884)+~E(x881,x882)+~P1(x881,x883,x884)
% 60.87/61.61 [89]P1(x893,x892,x894)+~E(x891,x892)+~P1(x893,x891,x894)
% 60.87/61.61 [90]P1(x903,x904,x902)+~E(x901,x902)+~P1(x903,x904,x901)
% 60.87/61.61 [91]P2(x912,x913,x914,x915)+~E(x911,x912)+~P2(x911,x913,x914,x915)
% 60.87/61.61 [92]P2(x923,x922,x924,x925)+~E(x921,x922)+~P2(x923,x921,x924,x925)
% 60.87/61.61 [93]P2(x933,x934,x932,x935)+~E(x931,x932)+~P2(x933,x934,x931,x935)
% 60.87/61.61 [94]P2(x943,x944,x945,x942)+~E(x941,x942)+~P2(x943,x944,x945,x941)
% 60.87/61.61 [95]P4(x952,x953,x954,x955)+~E(x951,x952)+~P4(x951,x953,x954,x955)
% 60.87/61.61 [96]P4(x963,x962,x964,x965)+~E(x961,x962)+~P4(x963,x961,x964,x965)
% 60.87/61.61 [97]P4(x973,x974,x972,x975)+~E(x971,x972)+~P4(x973,x974,x971,x975)
% 60.87/61.61 [98]P4(x983,x984,x985,x982)+~E(x981,x982)+~P4(x983,x984,x985,x981)
% 60.87/61.61 [99]P8(x992,x993,x994,x995,x996,x997,x998,x999)+~E(x991,x992)+~P8(x991,x993,x994,x995,x996,x997,x998,x999)
% 60.87/61.61 [100]P8(x1003,x1002,x1004,x1005,x1006,x1007,x1008,x1009)+~E(x1001,x1002)+~P8(x1003,x1001,x1004,x1005,x1006,x1007,x1008,x1009)
% 60.87/61.61 [101]P8(x1013,x1014,x1012,x1015,x1016,x1017,x1018,x1019)+~E(x1011,x1012)+~P8(x1013,x1014,x1011,x1015,x1016,x1017,x1018,x1019)
% 60.87/61.61 [102]P8(x1023,x1024,x1025,x1022,x1026,x1027,x1028,x1029)+~E(x1021,x1022)+~P8(x1023,x1024,x1025,x1021,x1026,x1027,x1028,x1029)
% 60.87/61.61 [103]P8(x1033,x1034,x1035,x1036,x1032,x1037,x1038,x1039)+~E(x1031,x1032)+~P8(x1033,x1034,x1035,x1036,x1031,x1037,x1038,x1039)
% 60.87/61.61 [104]P8(x1043,x1044,x1045,x1046,x1047,x1042,x1048,x1049)+~E(x1041,x1042)+~P8(x1043,x1044,x1045,x1046,x1047,x1041,x1048,x1049)
% 60.87/61.61 [105]P8(x1053,x1054,x1055,x1056,x1057,x1058,x1052,x1059)+~E(x1051,x1052)+~P8(x1053,x1054,x1055,x1056,x1057,x1058,x1051,x1059)
% 60.87/61.61 [106]P8(x1063,x1064,x1065,x1066,x1067,x1068,x1069,x1062)+~E(x1061,x1062)+~P8(x1063,x1064,x1065,x1066,x1067,x1068,x1069,x1061)
% 60.87/61.61 [107]P3(x1072,x1073,x1074,x1075)+~E(x1071,x1072)+~P3(x1071,x1073,x1074,x1075)
% 60.87/61.61 [108]P3(x1083,x1082,x1084,x1085)+~E(x1081,x1082)+~P3(x1083,x1081,x1084,x1085)
% 60.87/61.61 [109]P3(x1093,x1094,x1092,x1095)+~E(x1091,x1092)+~P3(x1093,x1094,x1091,x1095)
% 60.87/61.61 [110]P3(x1103,x1104,x1105,x1102)+~E(x1101,x1102)+~P3(x1103,x1104,x1105,x1101)
% 60.87/61.61 [111]P7(x1112,x1113,x1114,x1115,x1116,x1117,x1118,x1119)+~E(x1111,x1112)+~P7(x1111,x1113,x1114,x1115,x1116,x1117,x1118,x1119)
% 60.87/61.61 [112]P7(x1123,x1122,x1124,x1125,x1126,x1127,x1128,x1129)+~E(x1121,x1122)+~P7(x1123,x1121,x1124,x1125,x1126,x1127,x1128,x1129)
% 60.87/61.61 [113]P7(x1133,x1134,x1132,x1135,x1136,x1137,x1138,x1139)+~E(x1131,x1132)+~P7(x1133,x1134,x1131,x1135,x1136,x1137,x1138,x1139)
% 60.87/61.61 [114]P7(x1143,x1144,x1145,x1142,x1146,x1147,x1148,x1149)+~E(x1141,x1142)+~P7(x1143,x1144,x1145,x1141,x1146,x1147,x1148,x1149)
% 60.87/61.61 [115]P7(x1153,x1154,x1155,x1156,x1152,x1157,x1158,x1159)+~E(x1151,x1152)+~P7(x1153,x1154,x1155,x1156,x1151,x1157,x1158,x1159)
% 60.87/61.61 [116]P7(x1163,x1164,x1165,x1166,x1167,x1162,x1168,x1169)+~E(x1161,x1162)+~P7(x1163,x1164,x1165,x1166,x1167,x1161,x1168,x1169)
% 60.87/61.61 [117]P7(x1173,x1174,x1175,x1176,x1177,x1178,x1172,x1179)+~E(x1171,x1172)+~P7(x1173,x1174,x1175,x1176,x1177,x1178,x1171,x1179)
% 60.87/61.61 [118]P7(x1183,x1184,x1185,x1186,x1187,x1188,x1189,x1182)+~E(x1181,x1182)+~P7(x1183,x1184,x1185,x1186,x1187,x1188,x1189,x1181)
% 60.87/61.61 [119]P6(x1192,x1193,x1194)+~E(x1191,x1192)+~P6(x1191,x1193,x1194)
% 60.87/61.61 [120]P6(x1203,x1202,x1204)+~E(x1201,x1202)+~P6(x1203,x1201,x1204)
% 60.87/61.61 [121]P6(x1213,x1214,x1212)+~E(x1211,x1212)+~P6(x1213,x1214,x1211)
% 60.87/61.61 [122]P10(x1222,x1223,x1224,x1225)+~E(x1221,x1222)+~P10(x1221,x1223,x1224,x1225)
% 60.87/61.61 [123]P10(x1233,x1232,x1234,x1235)+~E(x1231,x1232)+~P10(x1233,x1231,x1234,x1235)
% 60.87/61.61 [124]P10(x1243,x1244,x1242,x1245)+~E(x1241,x1242)+~P10(x1243,x1244,x1241,x1245)
% 60.87/61.61 [125]P10(x1253,x1254,x1255,x1252)+~E(x1251,x1252)+~P10(x1253,x1254,x1255,x1251)
% 60.87/61.61 [126]P5(x1262,x1263,x1264,x1265,x1266,x1267)+~E(x1261,x1262)+~P5(x1261,x1263,x1264,x1265,x1266,x1267)
% 60.87/61.61 [127]P5(x1273,x1272,x1274,x1275,x1276,x1277)+~E(x1271,x1272)+~P5(x1273,x1271,x1274,x1275,x1276,x1277)
% 60.87/61.61 [128]P5(x1283,x1284,x1282,x1285,x1286,x1287)+~E(x1281,x1282)+~P5(x1283,x1284,x1281,x1285,x1286,x1287)
% 60.87/61.61 [129]P5(x1293,x1294,x1295,x1292,x1296,x1297)+~E(x1291,x1292)+~P5(x1293,x1294,x1295,x1291,x1296,x1297)
% 60.87/61.61 [130]P5(x1303,x1304,x1305,x1306,x1302,x1307)+~E(x1301,x1302)+~P5(x1303,x1304,x1305,x1306,x1301,x1307)
% 60.87/61.61 [131]P5(x1313,x1314,x1315,x1316,x1317,x1312)+~E(x1311,x1312)+~P5(x1313,x1314,x1315,x1316,x1317,x1311)
% 60.87/61.61 [132]P11(x1322,x1323,x1324,x1325,x1326,x1327)+~E(x1321,x1322)+~P11(x1321,x1323,x1324,x1325,x1326,x1327)
% 60.87/61.61 [133]P11(x1333,x1332,x1334,x1335,x1336,x1337)+~E(x1331,x1332)+~P11(x1333,x1331,x1334,x1335,x1336,x1337)
% 60.87/61.61 [134]P11(x1343,x1344,x1342,x1345,x1346,x1347)+~E(x1341,x1342)+~P11(x1343,x1344,x1341,x1345,x1346,x1347)
% 60.87/61.61 [135]P11(x1353,x1354,x1355,x1352,x1356,x1357)+~E(x1351,x1352)+~P11(x1353,x1354,x1355,x1351,x1356,x1357)
% 60.87/61.61 [136]P11(x1363,x1364,x1365,x1366,x1362,x1367)+~E(x1361,x1362)+~P11(x1363,x1364,x1365,x1366,x1361,x1367)
% 60.87/61.61 [137]P11(x1373,x1374,x1375,x1376,x1377,x1372)+~E(x1371,x1372)+~P11(x1373,x1374,x1375,x1376,x1377,x1371)
% 60.87/61.61 [138]P9(x1382,x1383,x1384,x1385)+~E(x1381,x1382)+~P9(x1381,x1383,x1384,x1385)
% 60.87/61.61 [139]P9(x1393,x1392,x1394,x1395)+~E(x1391,x1392)+~P9(x1393,x1391,x1394,x1395)
% 60.87/61.61 [140]P9(x1403,x1404,x1402,x1405)+~E(x1401,x1402)+~P9(x1403,x1404,x1401,x1405)
% 60.87/61.61 [141]P9(x1413,x1414,x1415,x1412)+~E(x1411,x1412)+~P9(x1413,x1414,x1415,x1411)
% 60.87/61.61
% 60.87/61.61 %-------------------------------------------
% 60.87/61.63 cnf(260,plain,
% 60.87/61.63 (~P3(a18,a3,a19,a17)),
% 60.87/61.63 inference(scs_inference,[],[146,165])).
% 60.87/61.63 cnf(262,plain,
% 60.87/61.63 (~P3(a3,a19,a18,a17)),
% 60.87/61.63 inference(scs_inference,[],[146,165,166])).
% 60.87/61.63 cnf(264,plain,
% 60.87/61.63 (~P3(a3,a18,a17,a19)),
% 60.87/61.63 inference(scs_inference,[],[146,165,166,167])).
% 60.87/61.63 cnf(266,plain,
% 60.87/61.63 (P1(a16,a16,a1)),
% 60.87/61.63 inference(scs_inference,[],[142,146,165,166,167,151])).
% 60.87/61.63 cnf(280,plain,
% 60.87/61.63 (~P3(a18,a3,a17,a19)),
% 60.87/61.63 inference(scs_inference,[],[260,167])).
% 60.87/61.63 cnf(282,plain,
% 60.87/61.63 (~P3(a19,a3,a18,a17)),
% 60.87/61.63 inference(scs_inference,[],[260,262,167,165])).
% 60.87/61.63 cnf(284,plain,
% 60.87/61.63 (~P3(a18,a19,a3,a17)),
% 60.87/61.63 inference(scs_inference,[],[260,262,167,165,166])).
% 60.87/61.63 cnf(286,plain,
% 60.87/61.63 (P1(a1,a1,a16)),
% 60.87/61.63 inference(scs_inference,[],[266,260,262,167,165,166,151])).
% 60.87/61.63 cnf(288,plain,
% 60.87/61.63 (P2(x2881,a3,a1,a2)+~E(a18,x2881)),
% 60.87/61.63 inference(scs_inference,[],[144,266,260,262,167,165,166,151,91])).
% 60.87/61.63 cnf(300,plain,
% 60.87/61.63 (~P3(a19,a3,a17,a18)),
% 60.87/61.63 inference(scs_inference,[],[282,167])).
% 60.87/61.63 cnf(302,plain,
% 60.87/61.63 (~P3(a3,a17,a18,a19)),
% 60.87/61.63 inference(scs_inference,[],[264,282,167,166])).
% 60.87/61.63 cnf(304,plain,
% 60.87/61.63 (~P3(a19,a18,a3,a17)),
% 60.87/61.63 inference(scs_inference,[],[264,282,284,167,166,165])).
% 60.87/61.63 cnf(318,plain,
% 60.87/61.63 (~P3(a3,a17,a19,a18)),
% 60.87/61.63 inference(scs_inference,[],[302,167])).
% 60.87/61.63 cnf(320,plain,
% 60.87/61.63 (~P3(a3,a19,a17,a18)),
% 60.87/61.63 inference(scs_inference,[],[300,302,167,165])).
% 60.87/61.63 cnf(322,plain,
% 60.87/61.63 (~P3(a18,a17,a3,a19)),
% 60.87/61.63 inference(scs_inference,[],[280,300,302,167,165,166])).
% 60.87/61.63 cnf(335,plain,
% 60.87/61.63 (~P3(a19,a18,a17,a3)),
% 60.87/61.63 inference(scs_inference,[],[304,167])).
% 60.87/61.63 cnf(337,plain,
% 60.87/61.63 (~P3(a19,a17,a3,a18)),
% 60.87/61.63 inference(scs_inference,[],[304,300,167,166])).
% 60.87/61.63 cnf(339,plain,
% 60.87/61.63 (~P3(a17,a3,a19,a18)),
% 60.87/61.63 inference(scs_inference,[],[304,318,300,167,166,165])).
% 60.87/61.63 cnf(353,plain,
% 60.87/61.63 (~P3(a18,a17,a19,a3)),
% 60.87/61.63 inference(scs_inference,[],[322,167])).
% 60.87/61.63 cnf(357,plain,
% 60.87/61.63 (~P3(a19,a17,a18,a3)),
% 60.87/61.63 inference(scs_inference,[],[322,335,167,165,166])).
% 60.87/61.63 cnf(371,plain,
% 60.87/61.63 (~P3(a17,a3,a18,a19)),
% 60.87/61.63 inference(scs_inference,[],[339,167])).
% 60.87/61.63 cnf(373,plain,
% 60.87/61.63 (~P3(a17,a19,a3,a18)),
% 60.87/61.63 inference(scs_inference,[],[339,167,166])).
% 60.87/61.63 cnf(375,plain,
% 60.87/61.63 (~P3(a17,a18,a19,a3)),
% 60.87/61.63 inference(scs_inference,[],[339,353,167,166,165])).
% 60.87/61.63 cnf(391,plain,
% 60.87/61.63 (~P3(a18,a19,a17,a3)),
% 60.87/61.63 inference(scs_inference,[],[373,335,167,165])).
% 60.87/61.63 cnf(588,plain,
% 60.87/61.63 (P1(a2,a16,a1)),
% 60.87/61.63 inference(scs_inference,[],[142,147,148])).
% 60.87/61.63 cnf(589,plain,
% 60.87/61.63 (P1(a1,a1,a2)),
% 60.87/61.63 inference(scs_inference,[],[588,151])).
% 60.87/61.63 cnf(598,plain,
% 60.87/61.63 (P1(a2,a2,a1)),
% 60.87/61.63 inference(scs_inference,[],[589,151])).
% 60.87/61.63 cnf(619,plain,
% 60.87/61.63 (P10(x6191,x6192,x6193,x6194)+~P10(x6194,x6193,x6191,x6192)),
% 60.87/61.63 inference(scs_inference,[],[161,162])).
% 60.87/61.63 cnf(1181,plain,
% 60.87/61.63 (P10(f8(a3,a1,a2,x11811),a3,a3,x11811)+~E(a18,x11811)),
% 60.87/61.63 inference(scs_inference,[],[183,288])).
% 60.87/61.63 cnf(1182,plain,
% 60.87/61.63 (P10(f8(a3,a1,a2,a18),a3,a3,a18)),
% 60.87/61.63 inference(equality_inference,[],[1181])).
% 60.87/61.63 cnf(1183,plain,
% 60.87/61.63 (P10(a3,a18,a3,f8(a3,a1,a2,a18))),
% 60.87/61.63 inference(scs_inference,[],[1182,619])).
% 60.87/61.63 cnf(1185,plain,
% 60.87/61.63 (P9(f8(a3,a1,a2,a18),a3,a3,f8(a3,a1,a2,a18))),
% 60.87/61.63 inference(scs_inference,[],[1182,619,176])).
% 60.87/61.63 cnf(1193,plain,
% 60.87/61.63 (P10(a3,f8(a3,a1,a2,a18),a18,a3)),
% 60.87/61.63 inference(scs_inference,[],[1183,619])).
% 60.87/61.63 cnf(1195,plain,
% 60.87/61.63 (P10(f8(a3,a1,a2,a18),a3,a18,a3)),
% 60.87/61.63 inference(scs_inference,[],[1185,1183,619,178])).
% 60.87/61.63 cnf(1197,plain,
% 60.87/61.63 (P9(a3,a18,a18,a3)),
% 60.87/61.63 inference(scs_inference,[],[1185,1183,619,178,176])).
% 60.87/61.63 cnf(1203,plain,
% 60.87/61.63 (P10(a18,a3,f8(a3,a1,a2,a18),a3)),
% 60.87/61.63 inference(scs_inference,[],[1193,619])).
% 60.87/61.63 cnf(1207,plain,
% 60.87/61.63 (P9(a18,a3,a3,a18)),
% 60.87/61.63 inference(scs_inference,[],[1182,1193,1197,619,178,176])).
% 60.87/61.63 cnf(1229,plain,
% 60.87/61.63 (P10(a18,a3,a3,f8(a3,a1,a2,a18))),
% 60.87/61.63 inference(scs_inference,[],[1195,619])).
% 60.87/61.63 cnf(1231,plain,
% 60.87/61.63 (P8(a3,f8(a3,a1,a2,a18),a3,a1,a2,a3,a2,a1)),
% 60.87/61.63 inference(scs_inference,[],[144,1195,619,225])).
% 60.87/61.63 cnf(1233,plain,
% 60.87/61.63 (P9(f8(a3,a1,a2,a18),a3,f8(a3,a1,a2,a18),a3)),
% 60.87/61.63 inference(scs_inference,[],[144,1195,1203,619,225,176])).
% 60.87/61.63 cnf(1235,plain,
% 60.87/61.63 (~P8(x12351,x12352,x12353,x12354,a3,f8(a3,a1,a2,a18),a3,a1)+P8(x12351,x12352,x12353,x12354,a2,a3,a2,a1)),
% 60.87/61.63 inference(scs_inference,[],[144,1195,1203,619,225,176,258])).
% 60.87/61.63 cnf(1240,plain,
% 60.87/61.63 (P10(a3,f8(a3,a1,a2,a18),a3,a18)),
% 60.87/61.63 inference(scs_inference,[],[1229,619])).
% 60.87/61.63 cnf(1242,plain,
% 60.87/61.63 (P9(a3,a18,a3,a18)),
% 60.87/61.63 inference(scs_inference,[],[1197,1207,1229,619,175])).
% 60.87/61.63 cnf(1299,plain,
% 60.87/61.63 (P9(a3,f8(a3,a1,a2,a18),a3,f8(a3,a1,a2,a18))),
% 60.87/61.63 inference(scs_inference,[],[1229,1193,176])).
% 60.87/61.63 cnf(1328,plain,
% 60.87/61.63 (~P1(x13281,a3,x13282)+~P9(a3,a3,a18,a18)+~P1(x13283,a3,x13282)+~P6(x13284,x13283,x13281)+P6(f20(a3,a18),a18,a3)+~P6(x13285,a3,x13282)),
% 60.87/61.63 inference(scs_inference,[],[1231,1229,1197,1207,1183,1242,171,155])).
% 60.87/61.63 cnf(1362,plain,
% 60.87/61.63 (P9(a3,f8(a3,a1,a2,a18),f8(a3,a1,a2,a18),a3)),
% 60.87/61.63 inference(scs_inference,[],[1203,1193,176])).
% 60.87/61.63 cnf(1478,plain,
% 60.87/61.63 (~P6(x14781,f8(a3,a1,a2,a18),f8(a3,a1,a2,a18))+P6(x14781,a3,a3)),
% 60.87/61.63 inference(scs_inference,[],[1233,171])).
% 60.87/61.63 cnf(1481,plain,
% 60.87/61.63 (~P6(x14811,a3,a3)+P6(x14811,a18,a18)),
% 60.87/61.63 inference(scs_inference,[],[1242,171])).
% 60.87/61.63 cnf(1483,plain,
% 60.87/61.63 (P6(x14831,a18,a18)+~P6(x14831,f8(a3,a1,a2,a18),f8(a3,a1,a2,a18))),
% 60.87/61.63 inference(scs_inference,[],[1242,171,1478])).
% 60.87/61.63 cnf(1928,plain,
% 60.87/61.63 (~P9(a18,a18,a3,a3)+~P1(x19281,a18,x19282)+~P1(x19283,a18,x19282)+~P6(x19284,x19283,x19281)+P6(f20(a18,a3),a3,a18)+~P6(x19285,a18,x19282)),
% 60.87/61.63 inference(scs_inference,[],[1299,1207,171,155])).
% 60.87/61.63 cnf(3213,plain,
% 60.87/61.63 (P1(a2,a1,a16)),
% 60.87/61.63 inference(scs_inference,[],[142,147])).
% 60.87/61.63 cnf(3215,plain,
% 60.87/61.63 (P1(a1,a16,a2)),
% 60.87/61.63 inference(scs_inference,[],[142,147,148])).
% 60.87/61.63 cnf(3217,plain,
% 60.87/61.63 (P1(a3,a18,a18)),
% 60.87/61.64 inference(scs_inference,[],[142,1242,147,148,156])).
% 60.87/61.64 cnf(3219,plain,
% 60.87/61.64 (P8(a3,f8(a3,a1,a2,a18),x32191,x32192,f8(a3,a1,a2,a18),a3,x32191,x32192)),
% 60.87/61.64 inference(scs_inference,[],[142,1362,1242,147,148,156,221])).
% 60.87/61.64 cnf(3233,plain,
% 60.87/61.64 (P1(f6(a3,a3,a18),a18,a3)),
% 60.87/61.64 inference(scs_inference,[],[142,1362,1242,143,1231,1240,147,148,156,221,183,248,250,251,249,173,174])).
% 60.87/61.64 cnf(3235,plain,
% 60.87/61.64 (P10(a3,f5(a3,a3,a18),a18,a3)),
% 60.87/61.64 inference(scs_inference,[],[142,1362,1242,143,1231,1240,147,148,156,221,183,248,250,251,249,173,174,185])).
% 60.87/61.64 cnf(3237,plain,
% 60.87/61.64 (P10(a3,f6(a3,a3,a18),a18,a3)),
% 60.87/61.64 inference(scs_inference,[],[142,1362,1242,143,1231,1240,147,148,156,221,183,248,250,251,249,173,174,185,186])).
% 60.87/61.64 cnf(3243,plain,
% 60.87/61.64 (P1(a16,a16,a2)),
% 60.87/61.64 inference(scs_inference,[],[142,1362,1242,1203,143,1231,1240,147,148,156,221,183,248,250,251,249,173,174,185,186,176,258,151])).
% 60.87/61.64 cnf(3245,plain,
% 60.87/61.64 (P9(a3,f5(a3,a3,a18),a3,f8(a3,a1,a2,a18))),
% 60.87/61.64 inference(scs_inference,[],[142,1362,1242,1203,143,1185,1231,1240,147,148,156,221,183,248,250,251,249,173,174,185,186,176,258,151,175])).
% 60.87/61.64 cnf(3249,plain,
% 60.87/61.64 (P9(f8(a3,a1,a2,a18),a3,f5(a3,a3,a18),a3)),
% 60.87/61.64 inference(scs_inference,[],[142,1362,1242,1203,143,1185,1231,1240,147,148,156,221,183,248,250,251,249,173,174,185,186,176,258,151,175,159,160])).
% 60.87/61.64 cnf(3251,plain,
% 60.87/61.64 (P10(a3,a17,f8(a3,a1,a16,a17),a3)),
% 60.87/61.64 inference(scs_inference,[],[142,1362,1242,1203,143,1185,1231,1240,147,148,156,221,183,248,250,251,249,173,174,185,186,176,258,151,175,159,160,161])).
% 60.87/61.64 cnf(3253,plain,
% 60.87/61.64 (P10(f8(a3,a1,a16,a17),a3,a17,a3)),
% 60.87/61.64 inference(scs_inference,[],[142,1362,1242,1203,143,1185,1231,1240,147,148,156,221,183,248,250,251,249,173,174,185,186,176,258,151,175,159,160,161,162])).
% 60.87/61.64 cnf(3255,plain,
% 60.87/61.64 (P8(a2,a3,a2,a1,a2,a3,a2,a1)),
% 60.87/61.64 inference(scs_inference,[],[142,1362,1242,1203,143,1185,1231,1240,147,148,156,221,183,248,250,251,249,173,174,185,186,176,258,151,175,159,160,161,162,1235])).
% 60.87/61.64 cnf(3293,plain,
% 60.87/61.64 (P9(a2,a3,a2,a3)),
% 60.87/61.64 inference(scs_inference,[],[3255,229])).
% 60.87/61.64 cnf(3295,plain,
% 60.87/61.64 (P10(f8(a2,a3,a16,a19),a2,a2,a19)),
% 60.87/61.64 inference(scs_inference,[],[3255,145,229,183])).
% 60.87/61.64 cnf(3297,plain,
% 60.87/61.64 (P10(a17,a3,f8(a3,a1,a16,a17),a3)),
% 60.87/61.64 inference(scs_inference,[],[3255,3253,145,229,183,161])).
% 60.87/61.64 cnf(3299,plain,
% 60.87/61.64 (P8(a3,f5(a3,a3,a18),x32991,x32992,a3,f8(a3,a1,a2,a18),x32991,x32992)),
% 60.87/61.64 inference(scs_inference,[],[3255,3245,3253,145,229,183,161,221])).
% 60.87/61.64 cnf(3301,plain,
% 60.87/61.64 (P1(a3,f5(a3,a3,a18),f8(a3,a1,a2,a18))),
% 60.87/61.64 inference(scs_inference,[],[3255,3245,3253,145,229,183,161,221,156])).
% 60.87/61.64 cnf(3303,plain,
% 60.87/61.64 (P9(a2,a3,a3,a2)),
% 60.87/61.64 inference(scs_inference,[],[3255,3245,3253,145,229,183,161,221,156,160])).
% 60.87/61.64 cnf(3305,plain,
% 60.87/61.64 (P9(a3,f8(a3,a1,a2,a18),a3,f5(a3,a3,a18))),
% 60.87/61.64 inference(scs_inference,[],[3255,3245,3253,145,229,183,161,221,156,160,159])).
% 60.87/61.64 cnf(3307,plain,
% 60.87/61.64 (P1(a16,a1,a2)),
% 60.87/61.64 inference(scs_inference,[],[3255,3215,3245,3253,145,229,183,161,221,156,160,159,147])).
% 60.87/61.64 cnf(3309,plain,
% 60.87/61.64 (P1(a16,a2,a16)),
% 60.87/61.64 inference(scs_inference,[],[3255,3215,3243,3245,3253,145,229,183,161,221,156,160,159,147,148])).
% 60.87/61.64 cnf(3315,plain,
% 60.87/61.64 (P8(a3,a2,a2,a1,a2,a3,a2,a1)),
% 60.87/61.64 inference(scs_inference,[],[3255,3215,3243,3245,3219,3253,3251,145,229,183,161,221,156,160,159,147,148,162,248,250])).
% 60.87/61.64 cnf(3319,plain,
% 60.87/61.64 (P8(a2,a1,a2,a3,a2,a1,a2,a3)),
% 60.87/61.64 inference(scs_inference,[],[3255,3215,3243,3245,3219,3253,3251,145,229,183,161,221,156,160,159,147,148,162,248,250,251,249])).
% 60.87/61.64 cnf(3321,plain,
% 60.87/61.64 (P9(a3,f8(a3,a1,a2,a18),f5(a3,a3,a18),a3)),
% 60.87/61.64 inference(scs_inference,[],[3255,3215,3243,3245,3219,3249,3253,3251,145,229,183,161,221,156,160,159,147,148,162,248,250,251,249,236])).
% 60.87/61.64 cnf(3326,plain,
% 60.87/61.64 (P3(a3,a1,a2,a2)),
% 60.87/61.64 inference(scs_inference,[],[3255,3215,3243,3245,3219,3249,3253,3251,598,145,1240,229,183,161,221,156,160,159,147,148,162,248,250,251,249,236,237,232])).
% 60.87/61.64 cnf(3328,plain,
% 60.87/61.64 (P3(a3,a2,a1,a2)),
% 60.87/61.64 inference(scs_inference,[],[3255,3215,3243,3245,3219,3249,3253,3251,598,145,1240,229,183,161,221,156,160,159,147,148,162,248,250,251,249,236,237,232,166])).
% 60.87/61.64 cnf(3330,plain,
% 60.87/61.64 (P3(a1,a3,a2,a2)),
% 60.87/61.64 inference(scs_inference,[],[3255,3215,3243,3245,3219,3249,3253,3251,598,145,1240,229,183,161,221,156,160,159,147,148,162,248,250,251,249,236,237,232,166,165])).
% 60.87/61.64 cnf(3334,plain,
% 60.87/61.64 (P8(a1,a3,a1,a2,a2,a3,a2,a2)),
% 60.87/61.64 inference(scs_inference,[],[3255,3215,3243,3245,3219,3249,3253,3251,598,143,145,1240,229,183,161,221,156,160,159,147,148,162,248,250,251,249,236,237,232,166,165,168,220])).
% 60.87/61.64 cnf(3336,plain,
% 60.87/61.64 (P3(a3,a2,a2,a1)),
% 60.87/61.64 inference(scs_inference,[],[3255,3215,3243,3245,3219,3249,3253,3251,598,143,145,1240,229,183,161,221,156,160,159,147,148,162,248,250,251,249,236,237,232,166,165,168,220,167])).
% 60.87/61.64 cnf(3338,plain,
% 60.87/61.64 (~P3(a18,x33381,a17,a3)+~E(x33381,a19)),
% 60.87/61.64 inference(scs_inference,[],[3255,3215,3243,3245,3219,3249,3253,3251,391,598,143,145,1240,229,183,161,221,156,160,159,147,148,162,248,250,251,249,236,237,232,166,165,168,220,167,108])).
% 60.87/61.64 cnf(3341,plain,
% 60.87/61.64 (P8(a3,f5(a3,a3,a18),x33411,x33412,a3,f8(a3,a1,a2,a18),x33411,x33412)),
% 60.87/61.64 inference(rename_variables,[],[3299])).
% 60.87/61.64 cnf(3343,plain,
% 60.87/61.64 (P1(a2,a3,a3)),
% 60.87/61.64 inference(scs_inference,[],[3293,3299,1235,156])).
% 60.87/61.64 cnf(3345,plain,
% 60.87/61.64 (P9(a3,a2,a2,a3)),
% 60.87/61.64 inference(scs_inference,[],[3293,3315,3299,1235,156,229])).
% 60.87/61.64 cnf(3347,plain,
% 60.87/61.64 (P8(a2,a3,x33471,x33472,a2,a3,x33471,x33472)),
% 60.87/61.64 inference(scs_inference,[],[3293,3315,3299,1235,156,229,221])).
% 60.87/61.64 cnf(3349,plain,
% 60.87/61.64 (P10(a18,a3,a3,f5(a3,a3,a18))),
% 60.87/61.64 inference(scs_inference,[],[3293,3315,3235,3299,1235,156,229,221,161])).
% 60.87/61.64 cnf(3351,plain,
% 60.87/61.64 (P10(a3,f6(a3,a3,a18),a3,a18)),
% 60.87/61.64 inference(scs_inference,[],[3293,3315,3235,3237,3299,1235,156,229,221,161,162])).
% 60.87/61.64 cnf(3353,plain,
% 60.87/61.64 (P1(a16,a2,a1)),
% 60.87/61.64 inference(scs_inference,[],[3293,3307,3315,3235,3237,3299,1235,156,229,221,161,162,148])).
% 60.87/61.64 cnf(3355,plain,
% 60.87/61.64 (P8(a2,a3,a2,a2,a1,a3,a1,a2)),
% 60.87/61.64 inference(scs_inference,[],[3293,3307,3315,3336,3235,3237,3299,1235,156,229,221,161,162,148,220])).
% 60.87/61.64 cnf(3357,plain,
% 60.87/61.64 (P1(a18,a3,a18)),
% 60.87/61.64 inference(scs_inference,[],[3293,3217,3307,3315,3336,3235,3237,3299,1235,156,229,221,161,162,148,220,147])).
% 60.87/61.64 cnf(3363,plain,
% 60.87/61.64 (P8(a3,a2,a2,a3,a2,a1,a2,a1)),
% 60.87/61.64 inference(scs_inference,[],[3293,3217,3307,3315,3336,3235,3237,3299,3321,1235,156,229,221,161,162,148,220,147,159,248,251])).
% 60.87/61.64 cnf(3365,plain,
% 60.87/61.64 (P8(a1,a2,a2,a3,a2,a1,a2,a3)),
% 60.87/61.64 inference(scs_inference,[],[3293,3217,3307,3315,3319,3336,3235,3237,3299,3321,1235,156,229,221,161,162,148,220,147,159,248,251,250])).
% 60.87/61.64 cnf(3369,plain,
% 60.87/61.64 (P3(a1,a2,a3,a2)),
% 60.87/61.64 inference(scs_inference,[],[3293,3330,3217,3307,3315,3319,3336,3235,3237,3299,3321,1235,156,229,221,161,162,148,220,147,159,248,251,250,249,166])).
% 60.87/61.64 cnf(3371,plain,
% 60.87/61.64 (P3(a2,a3,a1,a2)),
% 60.87/61.64 inference(scs_inference,[],[3293,3328,3330,3217,3307,3315,3319,3336,3235,3237,3299,3321,1235,156,229,221,161,162,148,220,147,159,248,251,250,249,166,165])).
% 60.87/61.64 cnf(3373,plain,
% 60.87/61.64 (P3(a1,a2,a2,a2)),
% 60.87/61.64 inference(scs_inference,[],[3293,3326,3328,3330,3217,3307,3315,3319,3336,3235,3237,3299,3321,1235,156,229,221,161,162,148,220,147,159,248,251,250,249,166,165,181])).
% 60.87/61.64 cnf(3375,plain,
% 60.87/61.64 (P9(a3,f5(a3,a3,a18),a3,f5(a3,a3,a18))),
% 60.87/61.64 inference(scs_inference,[],[3293,3326,3328,3330,3217,3307,3315,3319,3336,3235,3237,3299,3341,3305,3321,1235,156,229,221,161,162,148,220,147,159,248,251,250,249,166,165,181,236])).
% 60.87/61.64 cnf(3378,plain,
% 60.87/61.64 (P10(a3,a18,a3,f5(a3,a3,a18))),
% 60.87/61.64 inference(scs_inference,[],[3293,3326,3328,3330,3217,3307,3315,3319,3336,3235,3237,3299,3341,3305,3321,1197,1235,156,229,221,161,162,148,220,147,159,248,251,250,249,166,165,181,236,178])).
% 60.87/61.64 cnf(3380,plain,
% 60.87/61.64 (P9(a3,a2,a3,a2)),
% 60.87/61.64 inference(scs_inference,[],[3293,3326,3328,3330,3217,3307,3315,3319,3336,3235,3237,3299,3341,3305,3321,1197,1235,156,229,221,161,162,148,220,147,159,248,251,250,249,166,165,181,236,178,160])).
% 60.87/61.64 cnf(3382,plain,
% 60.87/61.64 (P3(a1,a2,a2,a3)),
% 60.87/61.64 inference(scs_inference,[],[3293,3326,3328,3330,3217,3307,3315,3319,3336,3235,3237,3299,3341,3305,3321,1197,1235,156,229,221,161,162,148,220,147,159,248,251,250,249,166,165,181,236,178,160,167])).
% 60.87/61.64 cnf(3396,plain,
% 60.87/61.64 (P9(a3,f5(a3,a3,a18),f5(a3,a3,a18),a3)),
% 60.87/61.64 inference(scs_inference,[],[3375,160])).
% 60.87/61.64 cnf(3398,plain,
% 60.87/61.64 (P1(a3,a2,a2)),
% 60.87/61.64 inference(scs_inference,[],[3380,3375,160,156])).
% 60.87/61.64 cnf(3400,plain,
% 60.87/61.64 (P9(a1,a2,a2,a1)),
% 60.87/61.64 inference(scs_inference,[],[3365,3380,3375,160,156,229])).
% 60.87/61.64 cnf(3402,plain,
% 60.87/61.64 (P10(f8(a2,a3,a16,a19),a2,a19,a2)),
% 60.87/61.64 inference(scs_inference,[],[3365,3380,3295,3375,160,156,229,162])).
% 60.87/61.64 cnf(3406,plain,
% 60.87/61.64 (P8(a2,a3,x34061,x34062,a3,a2,x34061,x34062)),
% 60.87/61.64 inference(scs_inference,[],[3303,3357,3365,3380,3295,3375,160,156,229,162,148,221])).
% 60.87/61.64 cnf(3408,plain,
% 60.87/61.64 (P10(a2,a19,f8(a2,a3,a16,a19),a2)),
% 60.87/61.64 inference(scs_inference,[],[3303,3357,3365,3380,3295,3375,160,156,229,162,148,221,161])).
% 60.87/61.64 cnf(3414,plain,
% 60.87/61.64 (P9(f5(a3,a3,a18),a3,f8(a3,a1,a2,a18),a3)),
% 60.87/61.64 inference(scs_inference,[],[3303,3309,3357,3365,3369,3380,3295,3375,3249,160,156,229,162,148,221,161,147,220,159])).
% 60.87/61.64 cnf(3416,plain,
% 60.87/61.64 (P8(a2,a1,a2,a1,a3,a2,a2,a3)),
% 60.87/61.64 inference(scs_inference,[],[3303,3363,3309,3357,3365,3369,3380,3295,3375,3249,160,156,229,162,148,221,161,147,220,159,248])).
% 60.87/61.64 cnf(3418,plain,
% 60.87/61.64 (P3(a2,a3,a2,a1)),
% 60.87/61.64 inference(scs_inference,[],[3303,3363,3309,3357,3365,3369,3371,3380,3295,3375,3249,160,156,229,162,148,221,161,147,220,159,248,167])).
% 60.87/61.64 cnf(3420,plain,
% 60.87/61.64 (P8(a1,a3,a2,a3,a1,a2,a2,a2)),
% 60.87/61.64 inference(scs_inference,[],[3303,3334,3363,3309,3357,3365,3369,3371,3380,3295,3375,3249,160,156,229,162,148,221,161,147,220,159,248,167,251])).
% 60.87/61.64 cnf(3424,plain,
% 60.87/61.64 (P8(a1,a2,a1,a3,a2,a2,a2,a3)),
% 60.87/61.64 inference(scs_inference,[],[3303,3334,3363,3309,3357,3365,3369,3371,3380,3295,3375,3249,160,156,229,162,148,221,161,147,220,159,248,167,251,250,249])).
% 60.87/61.64 cnf(3426,plain,
% 60.87/61.64 (P3(a2,a1,a3,a2)),
% 60.87/61.64 inference(scs_inference,[],[3303,3334,3363,3309,3357,3365,3369,3371,3380,3295,3375,3249,160,156,229,162,148,221,161,147,220,159,248,167,251,250,249,165])).
% 60.87/61.64 cnf(3428,plain,
% 60.87/61.64 (P3(a2,a2,a3,a1)),
% 60.87/61.64 inference(scs_inference,[],[3303,3334,3363,3309,3357,3365,3369,3371,3380,3295,3375,3249,160,156,229,162,148,221,161,147,220,159,248,167,251,250,249,165,166])).
% 60.87/61.64 cnf(3433,plain,
% 60.87/61.64 (P9(a2,a1,a2,a1)),
% 60.87/61.64 inference(scs_inference,[],[3303,3334,3363,3345,3347,3309,3357,3365,3369,3371,3380,3295,3375,3249,160,156,229,162,148,221,161,147,220,159,248,167,251,250,249,165,166,230,236])).
% 60.87/61.64 cnf(3435,plain,
% 60.87/61.64 (P1(a18,a18,f14(a3,a18,a18,a3,a18,a18))),
% 60.87/61.64 inference(scs_inference,[],[3303,3334,3363,3345,3347,3309,3357,3365,3369,3371,3380,3295,3375,3249,1197,160,156,229,162,148,221,161,147,220,159,248,167,251,250,249,165,166,230,236,202])).
% 60.87/61.64 cnf(3437,plain,
% 60.87/61.64 (P1(f14(a3,a18,a18,a3,a18,a18),a18,a3)),
% 60.87/61.64 inference(scs_inference,[],[3303,3334,3363,3345,3347,3309,3357,3365,3369,3371,3380,3295,3375,3249,1197,160,156,229,162,148,221,161,147,220,159,248,167,251,250,249,165,166,230,236,202,203])).
% 60.87/61.64 cnf(3439,plain,
% 60.87/61.64 (~P3(a17,a18,x34391,a3)+~E(x34391,a19)),
% 60.87/61.64 inference(scs_inference,[],[3303,3334,3363,3345,3347,3309,3357,3365,3369,3371,3380,3295,3375,3249,375,1197,160,156,229,162,148,221,161,147,220,159,248,167,251,250,249,165,166,230,236,202,203,109])).
% 60.87/61.64 cnf(3441,plain,
% 60.87/61.64 (P9(a1,a2,a1,a2)),
% 60.87/61.64 inference(scs_inference,[],[3400,160])).
% 60.87/61.64 cnf(3443,plain,
% 60.87/61.64 (P1(a2,a1,a1)),
% 60.87/61.64 inference(scs_inference,[],[3400,3433,160,156])).
% 60.87/61.64 cnf(3445,plain,
% 60.87/61.64 (P8(a1,a2,x34451,x34452,a2,a1,x34451,x34452)),
% 60.87/61.64 inference(scs_inference,[],[3400,3433,160,156,221])).
% 60.87/61.64 cnf(3447,plain,
% 60.87/61.64 (P10(a19,a2,f8(a2,a3,a16,a19),a2)),
% 60.87/61.64 inference(scs_inference,[],[3400,3433,3402,160,156,221,161])).
% 60.87/61.64 cnf(3449,plain,
% 60.87/61.64 (P10(a18,a3,f5(a3,a3,a18),a3)),
% 60.87/61.64 inference(scs_inference,[],[3400,3433,3349,3402,160,156,221,161,162])).
% 60.87/61.64 cnf(3453,plain,
% 60.87/61.64 (P8(a2,a1,a2,a2,a3,a1,a3,a2)),
% 60.87/61.64 inference(scs_inference,[],[3382,3400,3433,3233,3349,3402,160,156,221,161,162,148,220])).
% 60.87/61.64 cnf(3455,plain,
% 60.87/61.64 (P1(a3,a2,a3)),
% 60.87/61.64 inference(scs_inference,[],[3382,3343,3400,3433,3233,3349,3402,160,156,221,161,162,148,220,147])).
% 60.87/61.64 cnf(3461,plain,
% 60.87/61.64 (P3(a2,a1,a2,a3)),
% 60.87/61.64 inference(scs_inference,[],[3382,3426,3406,3343,3400,3433,3233,3349,3402,160,156,221,161,162,148,220,147,159,248,167])).
% 60.87/61.64 cnf(3463,plain,
% 60.87/61.64 (P8(a2,a3,a1,a3,a2,a2,a1,a2)),
% 60.87/61.64 inference(scs_inference,[],[3355,3382,3426,3406,3343,3400,3433,3233,3349,3402,160,156,221,161,162,148,220,147,159,248,167,251])).
% 60.87/61.64 cnf(3467,plain,
% 60.87/61.64 (P8(a2,a2,a2,a3,a1,a2,a1,a3)),
% 60.87/61.64 inference(scs_inference,[],[3355,3382,3426,3406,3343,3400,3433,3233,3349,3402,160,156,221,161,162,148,220,147,159,248,167,251,250,249])).
% 60.87/61.64 cnf(3469,plain,
% 60.87/61.64 (P3(a2,a1,a2,a2)),
% 60.87/61.64 inference(scs_inference,[],[3355,3382,3426,3406,3343,3373,3400,3433,3233,3349,3402,160,156,221,161,162,148,220,147,159,248,167,251,250,249,165])).
% 60.87/61.64 cnf(3471,plain,
% 60.87/61.64 (P3(a2,a2,a1,a3)),
% 60.87/61.64 inference(scs_inference,[],[3355,3382,3426,3406,3343,3373,3400,3433,3233,3349,3402,160,156,221,161,162,148,220,147,159,248,167,251,250,249,165,166])).
% 60.87/61.64 cnf(3477,plain,
% 60.87/61.64 (~P10(a1,a2,a2,a2)+P2(f9(a1,a2,a2),a1,a2,a2)),
% 60.87/61.64 inference(scs_inference,[],[3355,3382,3426,3406,3343,3353,3373,3400,3433,3233,3349,3402,3307,160,156,221,161,162,148,220,147,159,248,167,251,250,249,165,166,202,203,187])).
% 60.87/61.64 cnf(3491,plain,
% 60.87/61.64 (P8(a1,a2,x34911,x34912,a1,a2,x34911,x34912)),
% 60.87/61.64 inference(scs_inference,[],[3441,156,221])).
% 60.87/61.64 cnf(3495,plain,
% 60.87/61.64 (P1(a3,a3,a2)),
% 60.87/61.64 inference(scs_inference,[],[3441,3455,3449,156,221,161,148])).
% 60.87/61.64 cnf(3499,plain,
% 60.87/61.64 (P10(a3,a18,f5(a3,a3,a18),a3)),
% 60.87/61.64 inference(scs_inference,[],[3428,3441,3455,3378,3449,156,221,161,148,220,162])).
% 60.87/61.64 cnf(3501,plain,
% 60.87/61.64 (P1(a2,a3,a2)),
% 60.87/61.64 inference(scs_inference,[],[3428,3441,3398,3455,3378,3449,156,221,161,148,220,162,147])).
% 60.87/61.64 cnf(3507,plain,
% 60.87/61.64 (P8(a1,a2,a2,a1,x35071,x35072,x35071,x35072)),
% 60.87/61.64 inference(scs_inference,[],[3428,3441,3445,3398,3455,3396,3378,3449,156,221,161,148,220,162,147,159,248,251])).
% 60.87/61.64 cnf(3509,plain,
% 60.87/61.64 (P8(a2,a1,x35091,x35092,a2,a1,x35091,x35092)),
% 60.87/61.64 inference(scs_inference,[],[3428,3441,3445,3398,3455,3396,3378,3449,156,221,161,148,220,162,147,159,248,251,250])).
% 60.87/61.64 cnf(3511,plain,
% 60.87/61.64 (P8(x35111,x35112,a1,a2,x35111,x35112,a2,a1)),
% 60.87/61.64 inference(scs_inference,[],[3428,3441,3445,3398,3455,3396,3378,3449,156,221,161,148,220,162,147,159,248,251,250,249])).
% 60.87/61.64 cnf(3513,plain,
% 60.87/61.64 (P3(a2,a2,a1,a2)),
% 60.87/61.64 inference(scs_inference,[],[3428,3441,3445,3398,3455,3469,3396,3378,3449,156,221,161,148,220,162,147,159,248,251,250,249,166])).
% 60.87/61.64 cnf(3515,plain,
% 60.87/61.64 (P3(a2,a16,a1,a1)),
% 60.87/61.64 inference(scs_inference,[],[3428,3441,3445,3398,3455,3469,3396,3378,3449,286,156,221,161,148,220,162,147,159,248,251,250,249,166,232])).
% 60.87/61.64 cnf(3517,plain,
% 60.87/61.64 (P9(f5(a3,a3,a18),a3,f5(a3,a3,a18),a3)),
% 60.87/61.64 inference(scs_inference,[],[3428,3441,3445,3398,3455,3469,3396,3378,3449,286,156,221,161,148,220,162,147,159,248,251,250,249,166,232,160])).
% 60.87/61.64 cnf(3519,plain,
% 60.87/61.64 (P3(a2,a2,a2,a1)),
% 60.87/61.64 inference(scs_inference,[],[3428,3441,3445,3398,3455,3469,3396,3378,3449,286,156,221,161,148,220,162,147,159,248,251,250,249,166,232,160,167])).
% 60.87/61.64 cnf(3521,plain,
% 60.87/61.64 (P3(a16,a2,a1,a1)),
% 60.87/61.64 inference(scs_inference,[],[3428,3441,3445,3398,3455,3469,3396,3378,3449,286,156,221,161,148,220,162,147,159,248,251,250,249,166,232,160,167,165])).
% 60.87/61.64 cnf(3540,plain,
% 60.87/61.64 (P10(a19,a2,a2,f8(a2,a3,a16,a19))),
% 60.87/61.64 inference(scs_inference,[],[3414,3517,3499,3447,156,221,161,162])).
% 60.87/61.64 cnf(3542,plain,
% 60.87/61.64 (P1(a2,a2,a3)),
% 60.87/61.64 inference(scs_inference,[],[3501,3414,3517,3499,3447,156,221,161,162,148])).
% 60.87/61.64 cnf(3544,plain,
% 60.87/61.64 (P1(a1,a2,a1)),
% 60.87/61.64 inference(scs_inference,[],[3443,3501,3414,3517,3499,3447,156,221,161,162,148,147])).
% 60.87/61.64 cnf(3548,plain,
% 60.87/61.64 (P8(x35481,x35482,x35481,x35482,a1,a2,a2,a1)),
% 60.87/61.64 inference(scs_inference,[],[3461,3507,3443,3501,3414,3517,3499,3447,156,221,161,162,148,147,220,248])).
% 60.87/61.64 cnf(3552,plain,
% 60.87/61.64 (P8(a2,a1,a2,a1,x35521,x35522,x35521,x35522)),
% 60.87/61.64 inference(scs_inference,[],[3461,3467,3507,3443,3501,3414,3517,3499,3447,156,221,161,162,148,147,220,248,251,250])).
% 60.87/61.64 cnf(3556,plain,
% 60.87/61.64 (P3(a2,a1,a16,a1)),
% 60.87/61.64 inference(scs_inference,[],[3461,3467,3491,3507,3443,3501,3515,3414,3517,3499,3447,156,221,161,162,148,147,220,248,251,250,249,166])).
% 60.87/61.64 cnf(3558,plain,
% 60.87/61.64 (P3(a1,a2,a16,a1)),
% 60.87/61.64 inference(scs_inference,[],[3461,3467,3491,3507,3443,3501,3515,3414,3517,3499,3447,156,221,161,162,148,147,220,248,251,250,249,166,165])).
% 60.87/61.64 cnf(3564,plain,
% 60.87/61.64 (P3(a1,a1,a2,a2)),
% 60.87/61.64 inference(scs_inference,[],[3461,3467,3491,3507,3509,3443,3501,3515,3414,3517,3499,3447,3402,598,156,221,161,162,148,147,220,248,251,250,249,166,165,176,151,232])).
% 60.87/61.64 cnf(3571,plain,
% 60.87/61.64 (P9(x35711,x35712,x35711,x35712)),
% 60.87/61.64 inference(scs_inference,[],[3461,3467,3491,3507,3509,3443,3495,3501,3515,3414,3517,3499,3447,3455,3402,3345,598,156,221,161,162,148,147,220,248,251,250,249,166,165,176,151,232,203,202,229])).
% 60.87/61.64 cnf(3577,plain,
% 60.87/61.64 (P3(a2,a1,a1,a16)),
% 60.87/61.64 inference(scs_inference,[],[3461,3467,3491,3507,3509,3443,3495,3501,3515,3414,3517,3499,3447,3455,3402,3345,598,156,221,161,162,148,147,220,248,251,250,249,166,165,176,151,232,203,202,229,160,159,167])).
% 60.87/61.64 cnf(3601,plain,
% 60.87/61.64 (P1(x36011,x36012,x36012)),
% 60.87/61.64 inference(scs_inference,[],[3571,156])).
% 60.87/61.64 cnf(3603,plain,
% 60.87/61.64 (P9(x36031,x36032,x36032,x36031)),
% 60.87/61.64 inference(scs_inference,[],[3571,156,160])).
% 60.87/61.64 cnf(3605,plain,
% 60.87/61.64 (P8(x36051,x36052,x36053,x36054,x36051,x36052,x36053,x36054)),
% 60.87/61.64 inference(scs_inference,[],[3571,156,160,221])).
% 60.87/61.64 cnf(3611,plain,
% 60.87/61.64 (P10(a2,a19,a2,f8(a2,a3,a16,a19))),
% 60.87/61.64 inference(scs_inference,[],[3571,3471,3540,3408,156,160,221,161,220,162])).
% 60.87/61.64 cnf(3613,plain,
% 60.87/61.64 (P1(a18,f14(a3,a18,a18,a3,a18,a18),a3)),
% 60.87/61.64 inference(scs_inference,[],[3571,3471,3540,3437,3408,156,160,221,161,220,162,147])).
% 60.87/61.64 cnf(3617,plain,
% 60.87/61.64 (P8(x36171,x36172,a2,a1,x36171,x36172,a1,a2)),
% 60.87/61.64 inference(scs_inference,[],[3571,3471,3511,3540,3437,3408,156,160,221,161,220,162,147,148,248])).
% 60.87/61.65 cnf(3619,plain,
% 60.87/61.65 (P3(a1,a2,a1,a16)),
% 60.87/61.65 inference(scs_inference,[],[3571,3471,3511,3558,3540,3437,3408,156,160,221,161,220,162,147,148,248,167])).
% 60.87/61.65 cnf(3625,plain,
% 60.87/61.65 (P8(x36251,x36252,x36251,x36252,a2,a1,a1,a2)),
% 60.87/61.65 inference(scs_inference,[],[3571,3471,3424,3511,3548,3558,3540,3437,3408,156,160,221,161,220,162,147,148,248,167,251,250,249])).
% 60.87/61.65 cnf(3627,plain,
% 60.87/61.65 (P3(a16,a1,a2,a1)),
% 60.87/61.65 inference(scs_inference,[],[3571,3471,3424,3521,3511,3548,3558,3540,3437,3408,156,160,221,161,220,162,147,148,248,167,251,250,249,166])).
% 60.87/61.65 cnf(3629,plain,
% 60.87/61.65 (P3(a1,a16,a2,a1)),
% 60.87/61.65 inference(scs_inference,[],[3571,3471,3424,3521,3511,3548,3558,3540,3437,3408,156,160,221,161,220,162,147,148,248,167,251,250,249,166,165])).
% 60.87/61.65 cnf(3631,plain,
% 60.87/61.65 (P3(x36311,f14(a3,a18,a18,a3,a18,a18),a18,a18)),
% 60.87/61.65 inference(scs_inference,[],[3571,3471,3424,3521,3511,3548,3558,3540,3437,3435,3408,156,160,221,161,220,162,147,148,248,167,251,250,249,166,165,232])).
% 60.87/61.65 cnf(3645,plain,
% 60.87/61.65 (P7(a3,a18,a3,a18,a18,a18,a18,a18)),
% 60.87/61.65 inference(scs_inference,[],[3571,3471,3542,3424,3521,3511,3548,3552,3558,3564,3540,3437,3435,3408,3217,3303,3501,156,160,221,161,220,162,147,148,248,167,251,250,249,166,165,232,224,247,202,203,163,255])).
% 60.87/61.65 cnf(3647,plain,
% 60.87/61.65 (P7(a18,a3,a18,a18,a3,a18,a18,a18)),
% 60.87/61.65 inference(scs_inference,[],[3571,3471,3542,3424,3521,3511,3548,3552,3558,3564,3540,3437,3435,3408,3217,3303,3501,156,160,221,161,220,162,147,148,248,167,251,250,249,166,165,232,224,247,202,203,163,255,254])).
% 60.87/61.65 cnf(3653,plain,
% 60.87/61.65 (P7(a18,a18,a18,a18,a3,a18,a3,a18)),
% 60.87/61.65 inference(scs_inference,[],[3571,3471,3542,3424,3521,3511,3548,3552,3558,3564,3540,3437,3435,3408,3217,3303,3501,156,160,221,161,220,162,147,148,248,167,251,250,249,166,165,232,224,247,202,203,163,255,254,253,216,252])).
% 60.87/61.65 cnf(3658,plain,
% 60.87/61.65 (P7(a3,a18,a18,a18,a18,a3,a18,a18)),
% 60.87/61.65 inference(scs_inference,[],[3647,252])).
% 60.87/61.65 cnf(3660,plain,
% 60.87/61.65 (P1(a3,f8(a3,a1,a2,a18),f5(a3,a3,a18))),
% 60.87/61.65 inference(scs_inference,[],[3647,3305,252,156])).
% 60.87/61.65 cnf(3662,plain,
% 60.87/61.65 (P7(a18,a3,a3,a18,a18,a18,a18,a18)),
% 60.87/61.65 inference(scs_inference,[],[3645,3647,3305,252,156,254])).
% 60.87/61.65 cnf(3666,plain,
% 60.87/61.65 (P7(a3,a18,a18,a3,a18,a18,a18,a18)),
% 60.87/61.65 inference(scs_inference,[],[3645,3647,3305,252,156,254,253,255])).
% 60.87/61.65 cnf(3668,plain,
% 60.87/61.65 (P8(x36681,x36682,x36683,x36684,x36682,x36681,x36683,x36684)),
% 60.87/61.65 inference(scs_inference,[],[3603,3645,3647,3305,252,156,254,253,255,221])).
% 60.87/61.65 cnf(3670,plain,
% 60.87/61.65 (P1(x36701,x36702,x36701)),
% 60.87/61.65 inference(scs_inference,[],[3603,3601,3645,3647,3305,252,156,254,253,255,221,147])).
% 60.87/61.65 cnf(3674,plain,
% 60.87/61.65 (P10(a17,a3,a3,f8(a3,a1,a16,a17))),
% 60.87/61.65 inference(scs_inference,[],[3603,3601,3645,3647,3611,3297,3305,252,156,254,253,255,221,147,161,162])).
% 60.87/61.65 cnf(3682,plain,
% 60.87/61.65 (P3(a16,a1,a1,a2)),
% 60.87/61.65 inference(scs_inference,[],[3603,3601,3513,3625,3627,3645,3647,3613,3611,3297,3305,252,156,254,253,255,221,147,161,162,220,148,248,167])).
% 60.87/61.65 cnf(3684,plain,
% 60.87/61.65 (P8(x36841,x36842,x36841,x36842,x36843,x36844,x36843,x36844)),
% 60.87/61.65 inference(scs_inference,[],[3603,3605,3601,3513,3625,3627,3645,3647,3613,3611,3297,3305,252,156,254,253,255,221,147,161,162,220,148,248,167,251])).
% 60.87/61.65 cnf(3686,plain,
% 60.87/61.65 (P8(x36861,x36862,a2,a1,x36862,x36861,a1,a2)),
% 60.87/61.65 inference(scs_inference,[],[3603,3605,3601,3513,3617,3625,3627,3645,3647,3613,3611,3297,3305,252,156,254,253,255,221,147,161,162,220,148,248,167,251,250])).
% 60.87/61.65 cnf(3690,plain,
% 60.87/61.65 (P3(a1,a1,a2,a16)),
% 60.87/61.65 inference(scs_inference,[],[3603,3605,3601,3513,3619,3617,3625,3416,3627,3645,3647,3613,3611,3297,3305,252,156,254,253,255,221,147,161,162,220,148,248,167,251,250,249,166])).
% 60.87/61.65 cnf(3694,plain,
% 60.87/61.65 (P7(a3,a18,a3,a18,a3,a18,a3,a18)),
% 60.87/61.65 inference(scs_inference,[],[3603,3605,3601,3513,3619,3617,3625,3416,3627,3645,3647,3653,3631,3613,3611,3297,3305,252,156,254,253,255,221,147,161,162,220,148,248,167,251,250,249,166,165,259])).
% 60.87/61.65 cnf(3696,plain,
% 60.87/61.65 (P1(f5(a2,a2,a19),a19,a2)),
% 60.87/61.65 inference(scs_inference,[],[3603,3605,3601,3513,3619,3617,3625,3416,3627,3645,3647,3653,3631,3613,3611,3297,3305,252,156,254,253,255,221,147,161,162,220,148,248,167,251,250,249,166,165,259,173])).
% 60.87/61.65 cnf(3700,plain,
% 60.87/61.65 (P1(f6(a2,a2,a19),a19,a2)),
% 60.87/61.65 inference(scs_inference,[],[3603,3605,3601,3513,3619,3617,3625,3416,3627,3645,3647,3653,3631,3613,3611,3297,3305,252,156,254,253,255,221,147,161,162,220,148,248,167,251,250,249,166,165,259,173,186,174])).
% 60.87/61.65 cnf(3704,plain,
% 60.87/61.65 (P3(a3,a2,a1,a1)),
% 60.87/61.65 inference(scs_inference,[],[3603,3605,3601,3418,3513,3619,3617,3625,3416,3627,3645,3647,3653,3631,3613,3611,3297,3305,252,156,254,253,255,221,147,161,162,220,148,248,167,251,250,249,166,165,259,173,186,174,185,181])).
% 60.87/61.65 cnf(3706,plain,
% 60.87/61.65 (P10(f6(a3,a3,a18),a3,a3,a18)),
% 60.87/61.65 inference(scs_inference,[],[3603,3605,3601,3418,3513,3619,3617,3625,3416,3627,3645,3647,3653,3631,3613,3611,3297,3351,3305,252,156,254,253,255,221,147,161,162,220,148,248,167,251,250,249,166,165,259,173,186,174,185,181,178])).
% 60.87/61.65 cnf(3707,plain,
% 60.87/61.65 (P9(x37071,x37072,x37072,x37071)),
% 60.87/61.65 inference(rename_variables,[],[3603])).
% 60.87/61.65 cnf(3709,plain,
% 60.87/61.65 (P3(x37091,x37092,x37092,x37092)),
% 60.87/61.65 inference(scs_inference,[],[3603,3605,3601,3418,3513,3619,3617,3625,3416,3627,3645,3647,3653,3631,3613,3611,3297,3351,3305,252,156,254,253,255,221,147,161,162,220,148,248,167,251,250,249,166,165,259,173,186,174,185,181,178,232])).
% 60.87/61.65 cnf(3710,plain,
% 60.87/61.65 (P8(x37101,x37102,x37103,x37104,x37101,x37102,x37103,x37104)),
% 60.87/61.65 inference(rename_variables,[],[3605])).
% 60.87/61.65 cnf(3711,plain,
% 60.87/61.65 (P1(x37111,x37112,x37112)),
% 60.87/61.65 inference(rename_variables,[],[3601])).
% 60.87/61.65 cnf(3716,plain,
% 60.87/61.65 (P9(x37161,x37162,x37162,x37161)),
% 60.87/61.65 inference(rename_variables,[],[3603])).
% 60.87/61.65 cnf(3719,plain,
% 60.87/61.65 (P9(x37191,x37192,x37192,x37191)),
% 60.87/61.65 inference(rename_variables,[],[3603])).
% 60.87/61.65 cnf(3721,plain,
% 60.87/61.65 (P10(a2,a2,a2,a2)),
% 60.87/61.65 inference(scs_inference,[],[142,3603,3707,3716,3605,3601,3418,3513,3619,3617,3625,3416,3627,3645,3647,3653,3631,3613,3611,3297,3351,3215,3305,252,156,254,253,255,221,147,161,162,220,148,248,167,251,250,249,166,165,259,173,186,174,185,181,178,232,247,203,202,177])).
% 60.87/61.65 cnf(3727,plain,
% 60.87/61.65 (~P4(a18,a18,a18,a18)+P4(a3,a18,a3,a18)),
% 60.87/61.65 inference(scs_inference,[],[142,3603,3707,3716,3605,3601,3418,3513,3619,3617,3625,3416,3627,3645,3647,3653,3631,3613,3611,3297,3351,3215,3305,252,156,254,253,255,221,147,161,162,220,148,248,167,251,250,249,166,165,259,173,186,174,185,181,178,232,247,203,202,177,184,189,239])).
% 60.87/61.65 cnf(3729,plain,
% 60.87/61.65 (P10(f13(a2,a2,a2,x37291,x37291),a2,x37291,x37291)),
% 60.87/61.65 inference(scs_inference,[],[142,3603,3707,3716,3605,3601,3711,3418,3513,3619,3617,3625,3416,3627,3645,3647,3653,3631,3613,3611,3297,3351,3215,3305,252,156,254,253,255,221,147,161,162,220,148,248,167,251,250,249,166,165,259,173,186,174,185,181,178,232,247,203,202,177,184,189,239,194])).
% 60.87/61.65 cnf(3730,plain,
% 60.87/61.65 (P1(x37301,x37302,x37302)),
% 60.87/61.65 inference(rename_variables,[],[3601])).
% 60.87/61.65 cnf(3732,plain,
% 60.87/61.65 (P4(a2,a2,a2,f26(a2,a2,a2,a2,a2))),
% 60.87/61.65 inference(scs_inference,[],[142,3603,3707,3716,3605,3601,3711,3418,3513,3619,3617,3625,3416,3627,3645,3647,3653,3631,3613,3611,3297,3351,3215,3305,252,156,254,253,255,221,147,161,162,220,148,248,167,251,250,249,166,165,259,173,186,174,185,181,178,232,247,203,202,177,184,189,239,194,195])).
% 60.87/61.65 cnf(3734,plain,
% 60.87/61.65 (P9(f26(a2,a2,a2,a2,a2),a2,a2,a2)),
% 60.87/61.65 inference(scs_inference,[],[142,3603,3707,3716,3605,3601,3711,3418,3513,3619,3617,3625,3416,3627,3645,3647,3653,3631,3613,3611,3297,3351,3215,3305,252,156,254,253,255,221,147,161,162,220,148,248,167,251,250,249,166,165,259,173,186,174,185,181,178,232,247,203,202,177,184,189,239,194,195,197])).
% 60.87/61.65 cnf(3737,plain,
% 60.87/61.65 (P8(x37371,x37372,x37373,x37374,x37371,x37372,x37373,x37374)),
% 60.87/61.65 inference(rename_variables,[],[3605])).
% 60.87/61.65 cnf(3740,plain,
% 60.87/61.65 (P8(x37401,x37402,x37403,x37404,x37401,x37402,x37403,x37404)),
% 60.87/61.65 inference(rename_variables,[],[3605])).
% 60.87/61.65 cnf(3744,plain,
% 60.87/61.65 (P2(f9(a2,a2,a2),a2,a2,a2)),
% 60.87/61.65 inference(scs_inference,[],[142,3603,3707,3716,3605,3710,3737,3601,3711,3418,3513,3519,3619,3617,3625,3416,3627,3645,3647,3653,3631,3613,3611,3297,3351,3215,3305,252,156,254,253,255,221,147,161,162,220,148,248,167,251,250,249,166,165,259,173,186,174,185,181,178,232,247,203,202,177,184,189,239,194,195,197,241,242,172,187])).
% 60.87/61.65 cnf(3746,plain,
% 60.87/61.65 (P2(a2,a2,a2,a2)),
% 60.87/61.65 inference(scs_inference,[],[142,3603,3707,3716,3605,3710,3737,3601,3711,3418,3513,3519,3619,3617,3625,3416,3627,3645,3647,3653,3631,3613,3611,3297,3351,3215,3305,252,156,254,253,255,221,147,161,162,220,148,248,167,251,250,249,166,165,259,173,186,174,185,181,178,232,247,203,202,177,184,189,239,194,195,197,241,242,172,187,180])).
% 60.87/61.65 cnf(3748,plain,
% 60.87/61.65 (P6(a2,a2,a2)),
% 60.87/61.65 inference(scs_inference,[],[142,3603,3707,3716,3605,3710,3737,3601,3711,3730,3418,3513,3519,3619,3617,3625,3416,3627,3645,3647,3653,3631,3613,3611,3297,3351,3215,3305,252,156,254,253,255,221,147,161,162,220,148,248,167,251,250,249,166,165,259,173,186,174,185,181,178,232,247,203,202,177,184,189,239,194,195,197,241,242,172,187,180,157])).
% 60.87/61.65 cnf(3749,plain,
% 60.87/61.65 (P1(x37491,x37492,x37492)),
% 60.87/61.65 inference(rename_variables,[],[3601])).
% 60.87/61.65 cnf(3751,plain,
% 60.87/61.65 (P6(f24(a2,a2,a2,a2,a2,a2),a2,a2)),
% 60.87/61.65 inference(scs_inference,[],[142,3603,3707,3716,3605,3710,3737,3601,3711,3730,3418,3513,3519,3619,3617,3625,3416,3627,3645,3647,3653,3631,3613,3611,3297,3351,3215,3305,252,156,254,253,255,221,147,161,162,220,148,248,167,251,250,249,166,165,259,173,186,174,185,181,178,232,247,203,202,177,184,189,239,194,195,197,241,242,172,187,180,157,199])).
% 60.87/61.65 cnf(3757,plain,
% 60.87/61.65 (P9(x37571,x37572,x37572,x37571)),
% 60.87/61.65 inference(rename_variables,[],[3603])).
% 60.87/61.65 cnf(3759,plain,
% 60.87/61.65 (P6(a1,a2,a1)),
% 60.87/61.65 inference(scs_inference,[],[142,3603,3707,3716,3719,3605,3710,3737,3740,3601,3711,3730,3418,3513,3519,3619,3617,3625,3416,3544,3627,3645,3647,3653,3631,3613,3611,3297,3351,3215,3305,3571,252,156,254,253,255,221,147,161,162,220,148,248,167,251,250,249,166,165,259,173,186,174,185,181,178,232,247,203,202,177,184,189,239,194,195,197,241,242,172,187,180,157,199,238,188,158])).
% 60.87/61.65 cnf(3760,plain,
% 60.87/61.65 (P9(x37601,x37602,x37601,x37602)),
% 60.87/61.65 inference(rename_variables,[],[3571])).
% 60.87/61.65 cnf(3762,plain,
% 60.87/61.65 (P6(f7(a2,a2,a2),a2,a2)),
% 60.87/61.65 inference(scs_inference,[],[142,3603,3707,3716,3719,3605,3710,3737,3740,3601,3711,3730,3418,3513,3519,3619,3617,3625,3416,3544,3627,3645,3647,3653,3631,3613,3611,3297,3351,3215,3305,3571,252,156,254,253,255,221,147,161,162,220,148,248,167,251,250,249,166,165,259,173,186,174,185,181,178,232,247,203,202,177,184,189,239,194,195,197,241,242,172,187,180,157,199,238,188,158,182])).
% 60.87/61.65 cnf(3766,plain,
% 60.87/61.65 (P1(x37661,x37662,x37662)),
% 60.87/61.65 inference(rename_variables,[],[3601])).
% 60.87/61.65 cnf(3769,plain,
% 60.87/61.65 (P6(f20(a2,x37691),a2,x37691)),
% 60.87/61.65 inference(scs_inference,[],[142,3603,3707,3716,3719,3757,3605,3710,3737,3740,3601,3711,3730,3749,3766,3418,3513,3519,3619,3617,3625,3416,3544,3627,3645,3647,3653,3631,3613,3611,3297,3351,3215,3305,3571,3760,252,156,254,253,255,221,147,161,162,220,148,248,167,251,250,249,166,165,259,173,186,174,185,181,178,232,247,203,202,177,184,189,239,194,195,197,241,242,172,187,180,157,199,238,188,158,182,204,155])).
% 60.87/61.65 cnf(3772,plain,
% 60.87/61.65 (P4(a2,a2,f4(a2,a2,a2),a2)),
% 60.87/61.65 inference(scs_inference,[],[142,3603,3707,3716,3719,3757,3605,3710,3737,3740,3601,3711,3730,3749,3766,3418,3513,3519,3619,3617,3625,3416,3544,3627,3645,3647,3653,3631,3613,3611,3297,3351,3215,3305,3571,3760,252,156,254,253,255,221,147,161,162,220,148,248,167,251,250,249,166,165,259,173,186,174,185,181,178,232,247,203,202,177,184,189,239,194,195,197,241,242,172,187,180,157,199,238,188,158,182,204,155,164])).
% 60.87/61.65 cnf(3803,plain,
% 60.87/61.65 (P4(a1,a2,a1,a1)),
% 60.87/61.65 inference(scs_inference,[],[3662,3759,3732,252,222,152])).
% 60.87/61.65 cnf(3809,plain,
% 60.87/61.65 (P6(a1,a1,a2)),
% 60.87/61.65 inference(scs_inference,[],[3662,3759,3732,3769,252,222,152,164,149,150])).
% 60.87/61.65 cnf(3811,plain,
% 60.87/61.65 (P10(f8(a2,a2,a2,a2),a2,a2,a2)),
% 60.87/61.65 inference(scs_inference,[],[3662,3746,3759,3732,3769,252,222,152,164,149,150,183])).
% 60.87/61.65 cnf(3815,plain,
% 60.87/61.65 (P9(a2,a2,a2,f26(a2,a2,a2,a2,a2))),
% 60.87/61.65 inference(scs_inference,[],[3662,3746,3759,3732,3769,252,222,152,164,149,150,183,163,229])).
% 60.87/61.65 cnf(3817,plain,
% 60.87/61.65 (P7(a18,a3,a18,a18,a18,a3,a18,a18)),
% 60.87/61.65 inference(scs_inference,[],[3662,3658,3746,3759,3732,3769,252,222,152,164,149,150,183,163,229,254])).
% 60.87/61.65 cnf(3821,plain,
% 60.87/61.65 (P7(a18,a18,a3,a18,a18,a18,a18,a3)),
% 60.87/61.65 inference(scs_inference,[],[3662,3658,3746,3759,3732,3769,252,222,152,164,149,150,183,163,229,254,160,253])).
% 60.87/61.65 cnf(3823,plain,
% 60.87/61.65 (P7(a18,a3,a18,a3,a18,a18,a18,a18)),
% 60.87/61.65 inference(scs_inference,[],[3662,3658,3746,3759,3732,3769,252,222,152,164,149,150,183,163,229,254,160,253,255])).
% 60.87/61.65 cnf(3825,plain,
% 60.87/61.65 (P8(f26(a2,a2,a2,a2,a2),a2,x38251,x38252,a2,a2,x38251,x38252)),
% 60.87/61.65 inference(scs_inference,[],[3662,3658,3746,3759,3732,3769,3734,252,222,152,164,149,150,183,163,229,254,160,253,255,221])).
% 60.87/61.65 cnf(3827,plain,
% 60.87/61.65 (P1(f8(a3,a1,a2,a18),a3,f5(a3,a3,a18))),
% 60.87/61.65 inference(scs_inference,[],[3662,3658,3746,3759,3660,3732,3769,3734,252,222,152,164,149,150,183,163,229,254,160,253,255,221,147])).
% 60.87/61.65 cnf(3831,plain,
% 60.87/61.65 (P10(a3,f8(a3,a1,a16,a17),a17,a3)),
% 60.87/61.65 inference(scs_inference,[],[3662,3658,3746,3759,3660,3674,3732,3769,3706,3734,252,222,152,164,149,150,183,163,229,254,160,253,255,221,147,162,161])).
% 60.87/61.65 cnf(3833,plain,
% 60.87/61.65 (P9(a2,f26(a2,a2,a2,a2,a2),a2,a2)),
% 60.87/61.65 inference(scs_inference,[],[3662,3658,3746,3759,3660,3674,3732,3769,3706,3734,252,222,152,164,149,150,183,163,229,254,160,253,255,221,147,162,161,159])).
% 60.87/61.65 cnf(3837,plain,
% 60.87/61.65 (P1(x38371,x38371,x38372)),
% 60.87/61.65 inference(scs_inference,[],[3670,3577,3662,3658,3746,3759,3660,3674,3732,3769,3706,3734,252,222,152,164,149,150,183,163,229,254,160,253,255,221,147,162,161,159,220,148])).
% 60.87/61.65 cnf(3839,plain,
% 60.87/61.65 (P8(x38391,x38392,a1,a2,x38392,x38391,a2,a1)),
% 60.87/61.65 inference(scs_inference,[],[3670,3577,3662,3686,3658,3746,3759,3660,3674,3732,3769,3706,3734,252,222,152,164,149,150,183,163,229,254,160,253,255,221,147,162,161,159,220,148,248])).
% 60.87/61.65 cnf(3841,plain,
% 60.87/61.65 (P3(a1,a16,a1,a2)),
% 60.87/61.65 inference(scs_inference,[],[3670,3577,3662,3629,3686,3658,3746,3759,3660,3674,3732,3769,3706,3734,252,222,152,164,149,150,183,163,229,254,160,253,255,221,147,162,161,159,220,148,248,167])).
% 60.87/61.65 cnf(3843,plain,
% 60.87/61.65 (P8(x38431,x38432,x38432,x38431,x38433,x38434,x38433,x38434)),
% 60.87/61.65 inference(scs_inference,[],[3668,3670,3577,3662,3629,3686,3658,3746,3759,3660,3674,3732,3769,3706,3734,252,222,152,164,149,150,183,163,229,254,160,253,255,221,147,162,161,159,220,148,248,167,251])).
% 60.87/61.65 cnf(3845,plain,
% 60.87/61.65 (P8(a3,a1,a2,a3,a1,a2,a2,a2)),
% 60.87/61.65 inference(scs_inference,[],[3668,3670,3577,3662,3629,3686,3420,3658,3746,3759,3660,3674,3732,3769,3706,3734,252,222,152,164,149,150,183,163,229,254,160,253,255,221,147,162,161,159,220,148,248,167,251,250])).
% 60.87/61.65 cnf(3847,plain,
% 60.87/61.65 (P8(x38471,x38472,x38473,x38474,x38471,x38472,x38474,x38473)),
% 60.87/61.65 inference(scs_inference,[],[3668,3670,3577,3662,3629,3686,3420,3658,3746,3759,3660,3674,3732,3769,3706,3734,252,222,152,164,149,150,183,163,229,254,160,253,255,221,147,162,161,159,220,148,248,167,251,250,249])).
% 60.87/61.65 cnf(3849,plain,
% 60.87/61.65 (P3(x38491,x38492,x38491,x38491)),
% 60.87/61.65 inference(scs_inference,[],[3668,3709,3670,3577,3662,3629,3686,3420,3658,3746,3759,3660,3674,3732,3769,3706,3734,252,222,152,164,149,150,183,163,229,254,160,253,255,221,147,162,161,159,220,148,248,167,251,250,249,165])).
% 60.87/61.65 cnf(3851,plain,
% 60.87/61.65 (P3(a3,a1,a2,a1)),
% 60.87/61.65 inference(scs_inference,[],[3668,3709,3670,3577,3662,3629,3686,3420,3658,3704,3746,3759,3660,3674,3732,3769,3706,3734,252,222,152,164,149,150,183,163,229,254,160,253,255,221,147,162,161,159,220,148,248,167,251,250,249,165,166])).
% 60.87/61.65 cnf(3853,plain,
% 60.87/61.65 (P1(f13(a2,a2,a2,x38531,a2),x38531,a2)),
% 60.87/61.65 inference(scs_inference,[],[3668,3709,3670,3577,3721,3662,3629,3686,3420,3658,3704,3746,3759,3660,3674,3732,3769,3706,3734,252,222,152,164,149,150,183,163,229,254,160,253,255,221,147,162,161,159,220,148,248,167,251,250,249,165,166,193])).
% 60.87/61.65 cnf(3854,plain,
% 60.87/61.65 (P1(x38541,x38542,x38541)),
% 60.87/61.65 inference(rename_variables,[],[3670])).
% 60.87/61.65 cnf(3855,plain,
% 60.87/61.65 (~P1(x38551,x38552,x38553)+~P10(x38554,x38555,x38555,x38551)+P1(f13(x38554,x38551,x38555,x38552,x38553),x38552,x38553)),
% 60.87/61.65 inference(rename_variables,[],[193])).
% 60.87/61.65 cnf(3858,plain,
% 60.87/61.65 (P9(f20(a2,x38581),a2,x38581,a2)),
% 60.87/61.65 inference(scs_inference,[],[3668,3709,3670,3577,3721,3662,3629,3748,3686,3420,3658,3704,3746,3759,3660,3674,3732,3769,3706,3734,3772,252,222,152,164,149,150,183,163,229,254,160,253,255,221,147,162,161,159,220,148,248,167,251,250,249,165,166,193,177,154])).
% 60.87/61.65 cnf(3860,plain,
% 60.87/61.65 (P9(a2,a2,a1,a1)),
% 60.87/61.65 inference(scs_inference,[],[3668,3709,3670,3577,3721,3662,3629,3748,3686,3420,3658,3704,3746,3759,3660,3674,3732,3769,3706,3734,3772,252,222,152,164,149,150,183,163,229,254,160,253,255,221,147,162,161,159,220,148,248,167,251,250,249,165,166,193,177,154,153])).
% 60.87/61.65 cnf(3862,plain,
% 60.87/61.65 (P10(x38621,x38622,x38621,x38622)),
% 60.87/61.65 inference(scs_inference,[],[3668,3684,3709,3670,3577,3721,3662,3629,3748,3686,3420,3658,3704,3746,3759,3660,3674,3732,3769,3706,3734,3772,252,222,152,164,149,150,183,163,229,254,160,253,255,221,147,162,161,159,220,148,248,167,251,250,249,165,166,193,177,154,153,237])).
% 60.87/61.65 cnf(3863,plain,
% 60.87/61.65 (P8(x38631,x38632,x38631,x38632,x38633,x38634,x38633,x38634)),
% 60.87/61.65 inference(rename_variables,[],[3684])).
% 60.87/61.65 cnf(3873,plain,
% 60.87/61.65 (P4(f13(a2,a2,a2,a2,a2),a2,f13(a2,a2,a2,a2,a2),a2)),
% 60.87/61.65 inference(scs_inference,[],[142,3668,3684,3709,3670,3577,3721,3662,3629,3748,3686,3420,3658,3704,3746,3759,3660,3674,3732,3729,3769,3706,3734,3772,252,222,152,164,149,150,183,163,229,254,160,253,255,221,147,162,161,159,220,148,248,167,251,250,249,165,166,193,177,154,153,237,200,194,219,201,169])).
% 60.87/61.65 cnf(3876,plain,
% 60.87/61.65 (P4(a1,a2,a1,f26(a1,a1,a2,a1,a1))),
% 60.87/61.65 inference(scs_inference,[],[142,3668,3684,3709,3670,3577,3721,3662,3629,3748,3686,3420,3658,3704,3746,3759,3660,3674,3732,3729,3769,3706,3734,3772,252,222,152,164,149,150,183,163,229,254,160,253,255,221,147,162,161,159,220,148,248,167,251,250,249,165,166,193,177,154,153,237,200,194,219,201,169,195])).
% 60.87/61.65 cnf(3878,plain,
% 60.87/61.65 (P2(a2,a2,f26(a2,a2,a2,a2,a2),f26(a2,a2,a2,a2,a2))),
% 60.87/61.65 inference(scs_inference,[],[142,3668,3684,3709,3670,3577,3721,3662,3629,3748,3686,3420,3658,3704,3746,3759,3660,3674,3732,3729,3769,3706,3734,3772,252,222,152,164,149,150,183,163,229,254,160,253,255,221,147,162,161,159,220,148,248,167,251,250,249,165,166,193,177,154,153,237,200,194,219,201,169,195,180])).
% 60.87/61.65 cnf(3886,plain,
% 60.87/61.65 (P6(f24(a2,a1,a2,a1,a1,a1),a2,a1)),
% 60.87/61.65 inference(scs_inference,[],[142,3668,3684,3709,3670,3577,3721,3662,3629,3748,3686,3420,3658,3704,3746,3759,3660,3674,3732,3729,3769,3706,3734,3772,252,222,152,164,149,150,183,163,229,254,160,253,255,221,147,162,161,159,220,148,248,167,251,250,249,165,166,193,177,154,153,237,200,194,219,201,169,195,180,197,186,185,199])).
% 60.87/61.65 cnf(3889,plain,
% 60.87/61.65 (P6(f20(a2,x38891),a2,x38891)),
% 60.87/61.65 inference(rename_variables,[],[3769])).
% 60.87/61.65 cnf(3891,plain,
% 60.87/61.65 (P3(a16,a16,a1,a2)),
% 60.87/61.65 inference(scs_inference,[],[142,3668,3684,3863,3709,3670,3577,3721,3662,3629,3748,3686,3420,3658,3704,3746,3759,3660,3674,3732,3729,3769,3706,3734,3772,252,222,152,164,149,150,183,163,229,254,160,253,255,221,147,162,161,159,220,148,248,167,251,250,249,165,166,193,177,154,153,237,200,194,219,201,169,195,180,197,186,185,199,223,232])).
% 60.87/61.65 cnf(3892,plain,
% 60.87/61.65 (P8(x38921,x38922,x38921,x38922,x38923,x38924,x38923,x38924)),
% 60.87/61.65 inference(rename_variables,[],[3684])).
% 60.87/61.65 cnf(3896,plain,
% 60.87/61.65 (P1(x38961,x38962,x38961)),
% 60.87/61.65 inference(rename_variables,[],[3670])).
% 60.87/61.65 cnf(3898,plain,
% 60.87/61.65 (P6(a2,a2,f20(a2,a2))),
% 60.87/61.65 inference(scs_inference,[],[142,3668,3684,3863,3892,3709,3670,3854,3577,3721,3662,3629,3748,3686,3420,3658,3704,3746,3759,3660,3674,3732,3729,3769,3889,3706,3734,3772,3603,252,222,152,164,149,150,183,163,229,254,160,253,255,221,147,162,161,159,220,148,248,167,251,250,249,165,166,193,177,154,153,237,200,194,219,201,169,195,180,197,186,185,199,223,232,235,158])).
% 60.87/61.65 cnf(3900,plain,
% 60.87/61.65 (P9(x39001,x39002,x39002,x39001)),
% 60.87/61.65 inference(rename_variables,[],[3603])).
% 60.87/61.65 cnf(3902,plain,
% 60.87/61.65 (P4(x39021,x39021,x39021,x39021)),
% 60.87/61.65 inference(scs_inference,[],[142,3668,3684,3863,3892,3709,3670,3854,3577,3721,3662,3629,3748,3686,3420,3658,3704,3746,3759,3660,3674,3732,3729,3769,3889,3706,3734,3772,3603,252,222,152,164,149,150,183,163,229,254,160,253,255,221,147,162,161,159,220,148,248,167,251,250,249,165,166,193,177,154,153,237,200,194,219,201,169,195,180,197,186,185,199,223,232,235,158,247])).
% 60.87/61.65 cnf(3904,plain,
% 60.87/61.65 (P8(x39041,x39042,x39043,x39044,x39042,x39041,x39043,x39044)),
% 60.87/61.65 inference(rename_variables,[],[3668])).
% 60.87/61.65 cnf(3908,plain,
% 60.87/61.65 (P1(x39081,x39082,x39081)),
% 60.87/61.65 inference(rename_variables,[],[3670])).
% 60.87/61.65 cnf(3909,plain,
% 60.87/61.65 (P9(x39091,x39092,x39092,x39091)),
% 60.87/61.65 inference(rename_variables,[],[3603])).
% 60.87/61.65 cnf(3912,plain,
% 60.87/61.65 (P1(x39121,x39122,x39121)),
% 60.87/61.65 inference(rename_variables,[],[3670])).
% 60.87/61.65 cnf(3913,plain,
% 60.87/61.65 (P9(x39131,x39132,x39132,x39131)),
% 60.87/61.65 inference(rename_variables,[],[3603])).
% 60.87/61.65 cnf(3915,plain,
% 60.87/61.65 (P6(f20(a1,x39151),a1,x39151)),
% 60.87/61.65 inference(scs_inference,[],[142,3668,3684,3863,3892,3709,3670,3854,3896,3908,3912,3577,3721,3662,3629,3748,3686,3420,3658,3704,3746,3759,3660,3674,3732,3729,3769,3889,3706,3734,3772,3243,3603,3900,3909,589,252,222,152,164,149,150,183,163,229,254,160,253,255,221,147,162,161,159,220,148,248,167,251,250,249,165,166,193,177,154,153,237,200,194,219,201,169,195,180,197,186,185,199,223,232,235,158,247,202,203,155])).
% 60.87/61.65 cnf(3929,plain,
% 60.87/61.65 (P6(a2,f26(a2,a2,a2,a2,a2),a2)),
% 60.87/61.65 inference(scs_inference,[],[142,3668,3904,3684,3863,3892,3709,3670,3854,3896,3908,3912,3577,3721,3662,3629,3748,3686,3420,3658,3704,3746,3759,3660,3674,3732,3729,3769,3889,3706,3734,3772,3243,3603,3900,3909,589,252,222,152,164,149,150,183,163,229,254,160,253,255,221,147,162,161,159,220,148,248,167,251,250,249,165,166,193,177,154,153,237,200,194,219,201,169,195,180,197,186,185,199,223,232,235,158,247,202,203,155,245,3855,239,236,182,171])).
% 60.87/61.65 cnf(3936,plain,
% 60.87/61.65 (P4(a3,a18,a3,a18)),
% 60.87/61.65 inference(scs_inference,[],[142,3668,3904,3684,3863,3892,3709,3670,3854,3896,3908,3912,3577,3721,3662,3629,3748,3686,3420,3658,3704,3746,3759,3660,3674,3732,3729,3769,3889,3706,3734,3772,3243,3603,3900,3909,3913,3601,3571,589,252,222,152,164,149,150,183,163,229,254,160,253,255,221,147,162,161,159,220,148,248,167,251,250,249,165,166,193,177,154,153,237,200,194,219,201,169,195,180,197,186,185,199,223,232,235,158,247,202,203,155,245,3855,239,236,182,171,204,3727])).
% 60.87/61.65 cnf(3943,plain,
% 60.87/61.65 (P8(x39431,x39432,x39433,x39434,x39431,x39432,x39434,x39433)),
% 60.87/61.65 inference(rename_variables,[],[3847])).
% 60.87/61.65 cnf(3947,plain,
% 60.87/61.65 (P8(a3,a18,a18,a18,a18,a18,a3,a18)),
% 60.87/61.65 inference(scs_inference,[],[3847,3936,3666,1235,252,222])).
% 60.87/61.65 cnf(3949,plain,
% 60.87/61.65 (P4(a1,a1,a1,a2)),
% 60.87/61.65 inference(scs_inference,[],[3847,3936,3666,3809,1235,252,222,152])).
% 60.87/61.65 cnf(3953,plain,
% 60.87/61.65 (P6(f20(a1,x39531),x39531,a1)),
% 60.87/61.65 inference(scs_inference,[],[3847,3936,3666,3809,3915,1235,252,222,152,164,150])).
% 60.87/61.65 cnf(3959,plain,
% 60.87/61.65 (P7(a18,a3,a3,a18,a3,a18,a3,a18)),
% 60.87/61.65 inference(scs_inference,[],[3847,3936,3666,3809,3694,3876,3915,1235,252,222,152,164,150,149,163,254])).
% 60.87/61.65 cnf(3967,plain,
% 60.87/61.65 (P8(a2,a2,x39671,x39672,a1,a1,x39671,x39672)),
% 60.87/61.65 inference(scs_inference,[],[3847,3936,3666,3860,3809,3694,3817,3876,3915,3858,1235,252,222,152,164,150,149,163,254,160,253,255,221])).
% 60.87/61.65 cnf(3971,plain,
% 60.87/61.65 (P10(x39711,x39712,x39712,x39711)),
% 60.87/61.65 inference(scs_inference,[],[3847,3862,3936,3666,3860,3809,3694,3817,3301,3876,3915,3858,1235,252,222,152,164,150,149,163,254,160,253,255,221,147,162])).
% 60.87/61.65 cnf(3973,plain,
% 60.87/61.65 (P9(a1,a1,a2,a2)),
% 60.87/61.65 inference(scs_inference,[],[3847,3862,3936,3666,3860,3809,3694,3817,3301,3876,3915,3858,1235,252,222,152,164,150,149,163,254,160,253,255,221,147,162,159])).
% 60.87/61.65 cnf(3977,plain,
% 60.87/61.65 (P10(a2,a2,f8(a2,a2,a2,a2),a2)),
% 60.87/61.65 inference(scs_inference,[],[3847,3862,3936,3556,3666,3860,3809,3694,3817,3301,3876,3811,3915,3858,1235,252,222,152,164,150,149,163,254,160,253,255,221,147,162,159,220,161])).
% 60.87/61.65 cnf(3981,plain,
% 60.87/61.65 (P8(x39811,x39812,x39811,x39812,x39813,x39814,x39814,x39813)),
% 60.87/61.65 inference(scs_inference,[],[3843,3847,3862,3936,3556,3666,3860,3809,3694,3817,3301,3876,3700,3811,3915,3858,1235,252,222,152,164,150,149,163,254,160,253,255,221,147,162,159,220,161,148,248])).
% 60.87/61.65 cnf(3985,plain,
% 60.87/61.65 (P8(x39851,x39852,x39852,x39851,a1,a2,a2,a1)),
% 60.87/61.65 inference(scs_inference,[],[3843,3847,3862,3936,3556,3666,3860,3891,3809,3839,3694,3817,3301,3876,3700,3811,3915,3858,1235,252,222,152,164,150,149,163,254,160,253,255,221,147,162,159,220,161,148,248,167,251])).
% 60.87/61.65 cnf(3989,plain,
% 60.87/61.65 (P8(x39891,x39892,x39893,x39894,x39892,x39891,x39894,x39893)),
% 60.87/61.65 inference(scs_inference,[],[3843,3847,3943,3862,3936,3556,3666,3860,3891,3809,3839,3694,3817,3301,3876,3700,3811,3915,3858,1235,252,222,152,164,150,149,163,254,160,253,255,221,147,162,159,220,161,148,248,167,251,249,250])).
% 60.87/61.65 cnf(3993,plain,
% 60.87/61.65 (P3(x39931,x39931,x39932,x39931)),
% 60.87/61.65 inference(scs_inference,[],[3843,3847,3943,3849,3862,3936,3556,3666,3860,3891,3809,3839,3694,3817,3851,3301,3876,3700,3811,3915,3858,1235,252,222,152,164,150,149,163,254,160,253,255,221,147,162,159,220,161,148,248,167,251,249,250,165,166])).
% 60.87/61.65 cnf(4000,plain,
% 60.87/61.65 (P10(x40001,x40002,x40001,x40002)),
% 60.87/61.65 inference(rename_variables,[],[3862])).
% 60.87/61.65 cnf(4004,plain,
% 60.87/61.65 (P10(x40041,x40042,x40041,x40042)),
% 60.87/61.65 inference(rename_variables,[],[3862])).
% 60.87/61.65 cnf(4006,plain,
% 60.87/61.65 (P10(a3,a3,a18,a18)),
% 60.87/61.65 inference(scs_inference,[],[3843,3847,3943,3849,3862,4000,3936,3556,3666,3803,3860,3891,3809,3839,3694,3817,3851,3301,3876,3700,3811,3915,3858,1235,252,222,152,164,150,149,163,254,160,253,255,221,147,162,159,220,161,148,248,167,251,249,250,165,166,190,196,173,187,177])).
% 60.87/61.65 cnf(4017,plain,
% 60.87/61.65 (P4(a18,a3,a18,a3)),
% 60.87/61.65 inference(scs_inference,[],[142,3902,3843,3847,3943,3849,3862,4000,3936,3556,3666,3803,3860,3891,3809,3839,3694,3817,3823,3851,3301,3876,3700,3811,3915,3858,3831,1235,252,222,152,164,150,149,163,254,160,253,255,221,147,162,159,220,161,148,248,167,251,249,250,165,166,190,196,173,187,177,189,200,193,237,239])).
% 60.87/61.65 cnf(4018,plain,
% 60.87/61.65 (P4(x40181,x40181,x40181,x40181)),
% 60.87/61.65 inference(rename_variables,[],[3902])).
% 60.87/61.65 cnf(4022,plain,
% 60.87/61.65 (P9(f26(x40221,x40221,x40221,x40221,x40221),x40221,x40221,x40221)),
% 60.87/61.65 inference(scs_inference,[],[142,3902,4018,3843,3847,3943,3849,3862,4000,4004,3936,3556,3666,3803,3860,3891,3809,3839,3694,3817,3823,3851,3301,3876,3700,3811,3915,3858,3831,1235,252,222,152,164,150,149,163,254,160,253,255,221,147,162,159,220,161,148,248,167,251,249,250,165,166,190,196,173,187,177,189,200,193,237,239,194,197])).
% 60.87/61.65 cnf(4023,plain,
% 60.87/61.65 (P4(x40231,x40231,x40231,x40231)),
% 60.87/61.65 inference(rename_variables,[],[3902])).
% 60.87/61.65 cnf(4024,plain,
% 60.87/61.65 (P10(x40241,x40242,x40241,x40242)),
% 60.87/61.65 inference(rename_variables,[],[3862])).
% 60.87/61.65 cnf(4027,plain,
% 60.87/61.65 (P1(x40271,x40271,x40272)),
% 60.87/61.65 inference(rename_variables,[],[3837])).
% 60.87/61.65 cnf(4032,plain,
% 60.87/61.65 (P1(f6(x40321,x40321,x40322),x40322,x40321)),
% 60.87/61.65 inference(scs_inference,[],[142,3902,4018,3843,3847,3943,3849,3862,4000,4004,4024,3837,3936,3556,3666,3803,3860,3891,3809,3839,3694,3817,3823,3851,3301,3876,3700,3811,3825,3915,3878,3858,3831,1235,252,222,152,164,150,149,163,254,160,253,255,221,147,162,159,220,161,148,248,167,251,249,250,165,166,190,196,173,187,177,189,200,193,237,239,194,197,168,236,174])).
% 60.87/61.65 cnf(4034,plain,
% 60.87/61.65 (P7(a1,a1,a1,a2,a1,a1,a1,a2)),
% 60.87/61.65 inference(scs_inference,[],[142,3902,4018,3843,3847,3943,3849,3862,4000,4004,4024,3837,3936,3556,3666,3803,3860,3891,3809,3839,3694,3817,3823,3851,3301,3876,3700,3811,3825,3915,3878,3858,3831,1235,252,222,152,164,150,149,163,254,160,253,255,221,147,162,159,220,161,148,248,167,251,249,250,165,166,190,196,173,187,177,189,200,193,237,239,194,197,168,236,174,219])).
% 60.87/61.65 cnf(4036,plain,
% 60.87/61.65 (P2(x40361,x40361,x40361,x40361)),
% 60.87/61.65 inference(scs_inference,[],[142,3902,4018,4023,3843,3847,3943,3849,3862,4000,4004,4024,3837,3936,3556,3666,3803,3860,3891,3809,3839,3694,3817,3823,3851,3301,3876,3700,3811,3825,3915,3878,3858,3831,1235,252,222,152,164,150,149,163,254,160,253,255,221,147,162,159,220,161,148,248,167,251,249,250,165,166,190,196,173,187,177,189,200,193,237,239,194,197,168,236,174,219,180])).
% 60.87/61.65 cnf(4041,plain,
% 60.87/61.65 (P10(x40411,x40412,x40411,x40412)),
% 60.87/61.65 inference(rename_variables,[],[3862])).
% 60.87/61.65 cnf(4043,plain,
% 60.87/61.65 (P10(x40431,f6(x40431,x40431,x40432),x40432,x40431)),
% 60.87/61.65 inference(scs_inference,[],[142,3902,4018,4023,3843,3847,3943,3849,3862,4000,4004,4024,4041,3837,3936,3556,3666,3803,3860,3891,3809,3839,3694,3817,3823,3851,3301,3876,3700,3811,3825,3915,3878,3858,3929,3831,1235,252,222,152,164,150,149,163,254,160,253,255,221,147,162,159,220,161,148,248,167,251,249,250,165,166,190,196,173,187,177,189,200,193,237,239,194,197,168,236,174,219,180,201,169,186])).
% 60.87/61.65 cnf(4045,plain,
% 60.87/61.65 (P4(x40451,x40451,x40451,f26(x40451,x40451,x40451,x40451,x40451))),
% 60.87/61.65 inference(scs_inference,[],[142,3902,4018,4023,3843,3847,3943,3849,3862,4000,4004,4024,4041,3837,3936,3556,3666,3803,3860,3891,3809,3839,3694,3817,3823,3851,3301,3876,3700,3811,3825,3915,3878,3858,3929,3831,1235,252,222,152,164,150,149,163,254,160,253,255,221,147,162,159,220,161,148,248,167,251,249,250,165,166,190,196,173,187,177,189,200,193,237,239,194,197,168,236,174,219,180,201,169,186,195])).
% 60.87/61.65 cnf(4046,plain,
% 60.87/61.65 (P4(x40461,x40461,x40461,x40461)),
% 60.87/61.65 inference(rename_variables,[],[3902])).
% 60.87/61.65 cnf(4047,plain,
% 60.87/61.65 (P10(x40471,x40472,x40471,x40472)),
% 60.87/61.65 inference(rename_variables,[],[3862])).
% 60.87/61.65 cnf(4051,plain,
% 60.87/61.65 (P6(f24(a1,a2,a1,a2,a1,a1),a1,a2)),
% 60.87/61.65 inference(scs_inference,[],[142,3902,4018,4023,3843,3847,3943,3849,3862,4000,4004,4024,4041,4047,3837,3936,3556,3666,3803,3860,3891,3809,3839,3694,3817,3823,3851,3301,3876,3700,3811,3825,3915,3878,3858,3929,3831,1235,252,222,152,164,150,149,163,254,160,253,255,221,147,162,159,220,161,148,248,167,251,249,250,165,166,190,196,173,187,177,189,200,193,237,239,194,197,168,236,174,219,180,201,169,186,195,185,199])).
% 60.87/61.65 cnf(4057,plain,
% 60.87/61.65 (P3(x40571,x40572,x40573,x40573)),
% 60.87/61.65 inference(scs_inference,[],[142,3902,4018,4023,3843,3847,3943,3849,3862,4000,4004,4024,4041,4047,3837,4027,3936,3556,3666,3803,3860,3891,3809,3839,3694,3817,3823,3851,3833,3301,3876,3700,3762,3811,3825,3915,3878,3858,3929,3831,3744,3605,1235,252,222,152,164,150,149,163,254,160,253,255,221,147,162,159,220,161,148,248,167,251,249,250,165,166,190,196,173,187,177,189,200,193,237,239,194,197,168,236,174,219,180,201,169,186,195,185,199,223,175,232])).
% 60.87/61.65 cnf(4060,plain,
% 60.87/61.65 (P2(f10(a2,a2,a1),a2,a2,a1)),
% 60.87/61.65 inference(scs_inference,[],[142,3902,4018,4023,3843,3847,3943,3849,3862,4000,4004,4024,4041,4047,3837,4027,3936,3556,3666,3803,3860,3891,3809,3839,3694,3817,3823,3851,3833,3301,3876,3700,3762,3811,3825,3915,3878,3858,3929,3831,3744,3605,1235,252,222,152,164,150,149,163,254,160,253,255,221,147,162,159,220,161,148,248,167,251,249,250,165,166,190,196,173,187,177,189,200,193,237,239,194,197,168,236,174,219,180,201,169,186,195,185,199,223,175,232,188])).
% 60.87/61.65 cnf(4063,plain,
% 60.87/61.65 (P1(x40631,x40632,x40632)),
% 60.87/61.65 inference(rename_variables,[],[3601])).
% 60.87/61.65 cnf(4069,plain,
% 60.87/61.65 (P9(x40691,x40692,x40692,x40691)),
% 60.87/61.65 inference(rename_variables,[],[3603])).
% 60.87/61.65 cnf(4083,plain,
% 60.87/61.65 (P6(f7(a2,a2,a2),a2,f26(a2,a2,a2,a2,a2))),
% 60.87/61.65 inference(scs_inference,[],[142,3902,4018,4023,4046,3843,3847,3943,3849,3862,4000,4004,4024,4041,4047,3837,4027,3936,3556,3666,3803,3860,3891,3809,3839,3463,3694,3817,3823,3851,3833,3301,3876,3700,3762,3815,3811,3825,3915,3878,3858,3929,3831,3744,3670,3605,3603,4069,3601,4063,3215,3748,3759,1235,252,222,152,164,150,149,163,254,160,253,255,221,147,162,159,220,161,148,248,167,251,249,250,165,166,190,196,173,187,177,189,200,193,237,239,194,197,168,236,174,219,180,201,169,186,195,185,199,223,175,232,188,158,205,203,202,183,256,184,171])).
% 60.87/61.65 cnf(4085,plain,
% 60.87/61.65 (P4(a16,a16,a2,a2)),
% 60.87/61.65 inference(scs_inference,[],[142,3902,4018,4023,4046,3843,3847,3943,3849,3862,4000,4004,4024,4041,4047,3837,4027,3936,3556,3666,3803,3860,3891,3809,3839,3463,3694,3817,3823,3851,3833,3301,3876,3700,3762,3815,3811,3825,3915,3878,3858,3929,3831,3744,3684,3670,3605,3603,4069,3601,4063,3215,3748,3759,1235,252,222,152,164,150,149,163,254,160,253,255,221,147,162,159,220,161,148,248,167,251,249,250,165,166,190,196,173,187,177,189,200,193,237,239,194,197,168,236,174,219,180,201,169,186,195,185,199,223,175,232,188,158,205,203,202,183,256,184,171,247])).
% 60.87/61.65 cnf(4095,plain,
% 60.87/61.65 (P8(x40951,x40952,x40953,x40954,x40952,x40951,x40954,x40953)),
% 60.87/61.65 inference(rename_variables,[],[3989])).
% 60.87/61.65 cnf(4097,plain,
% 60.87/61.65 (P7(a3,a18,a3,a18,a18,a3,a3,a18)),
% 60.87/61.65 inference(scs_inference,[],[3989,3959,1235,252])).
% 60.87/61.65 cnf(4099,plain,
% 60.87/61.65 (P8(a1,a1,a1,a2,a1,a2,a1,a2)),
% 60.87/61.65 inference(scs_inference,[],[3989,3949,3959,1235,252,222])).
% 60.87/61.65 cnf(4101,plain,
% 60.87/61.65 (P4(f24(a2,a2,a2,a2,a2,a2),a2,f24(a2,a2,a2,a2,a2,a2),a2)),
% 60.87/61.65 inference(scs_inference,[],[3989,3949,3959,3751,1235,252,222,152])).
% 60.87/61.65 cnf(4103,plain,
% 60.87/61.65 (P6(f7(a2,a2,a2),f26(a2,a2,a2,a2,a2),a2)),
% 60.87/61.65 inference(scs_inference,[],[3989,3949,3959,3751,4083,1235,252,222,152,150])).
% 60.87/61.65 cnf(4107,plain,
% 60.87/61.65 (P4(a1,a1,a2,a1)),
% 60.87/61.65 inference(scs_inference,[],[3989,3949,3959,3751,4083,1235,252,222,152,150,149,164])).
% 60.87/61.65 cnf(4109,plain,
% 60.87/61.65 (P9(a1,a1,a1,a2)),
% 60.87/61.65 inference(scs_inference,[],[3989,3949,3959,3751,4083,1235,252,222,152,150,149,164,229])).
% 60.87/61.65 cnf(4113,plain,
% 60.87/61.65 (P7(a18,a3,a3,a18,a18,a3,a3,a18)),
% 60.87/61.65 inference(scs_inference,[],[3989,3949,3959,4085,3751,4083,1235,252,222,152,150,149,164,229,163,254])).
% 60.87/61.65 cnf(4115,plain,
% 60.87/61.65 (P9(a1,a1,a2,a1)),
% 60.87/61.65 inference(scs_inference,[],[3989,3949,3959,4085,3751,4083,1235,252,222,152,150,149,164,229,163,254,160])).
% 60.87/61.65 cnf(4117,plain,
% 60.87/61.65 (P7(a3,a18,a18,a3,a3,a18,a3,a18)),
% 60.87/61.65 inference(scs_inference,[],[3989,3949,3959,4085,3751,4083,1235,252,222,152,150,149,164,229,163,254,160,253])).
% 60.87/61.65 cnf(4121,plain,
% 60.87/61.65 (P8(a1,a1,x41211,x41212,a2,a2,x41211,x41212)),
% 60.87/61.65 inference(scs_inference,[],[3989,3949,3959,3973,4034,4085,3751,4083,1235,252,222,152,150,149,164,229,163,254,160,253,255,221])).
% 60.87/61.65 cnf(4123,plain,
% 60.87/61.65 (P1(x41231,f6(x41232,x41232,x41231),x41232)),
% 60.87/61.65 inference(scs_inference,[],[3989,3949,3959,3973,4034,4085,4032,3751,4083,1235,252,222,152,150,149,164,229,163,254,160,253,255,221,147])).
% 60.87/61.65 cnf(4125,plain,
% 60.87/61.65 (P10(a18,a18,a3,a3)),
% 60.87/61.65 inference(scs_inference,[],[3989,3949,3959,3973,4006,4034,4085,4032,3751,4083,1235,252,222,152,150,149,164,229,163,254,160,253,255,221,147,161])).
% 60.87/61.65 cnf(4127,plain,
% 60.87/61.65 (P1(f6(x41271,x41271,x41272),x41271,x41272)),
% 60.87/61.65 inference(scs_inference,[],[3989,3949,3959,3973,4006,4034,4085,4032,3751,4083,1235,252,222,152,150,149,164,229,163,254,160,253,255,221,147,161,148])).
% 60.87/61.65 cnf(4129,plain,
% 60.87/61.65 (P10(x41291,f6(x41291,x41291,x41292),x41291,x41292)),
% 60.87/61.65 inference(scs_inference,[],[3989,3949,3959,3973,4006,4034,4085,4043,4032,3751,4083,1235,252,222,152,150,149,164,229,163,254,160,253,255,221,147,161,148,162])).
% 60.87/61.65 cnf(4131,plain,
% 60.87/61.65 (P9(x41311,x41311,f26(x41311,x41311,x41311,x41311,x41311),x41311)),
% 60.87/61.65 inference(scs_inference,[],[3989,3949,3959,3973,4006,4034,4085,4022,4043,4032,3751,4083,1235,252,222,152,150,149,164,229,163,254,160,253,255,221,147,161,148,162,159])).
% 60.87/61.65 cnf(4137,plain,
% 60.87/61.65 (P3(x41371,x41371,x41371,x41372)),
% 60.87/61.65 inference(scs_inference,[],[3989,3993,3682,3949,3985,3959,3973,4006,4034,4085,4022,4043,4032,3751,4083,1235,252,222,152,150,149,164,229,163,254,160,253,255,221,147,161,148,162,159,220,248,167])).
% 60.87/61.65 cnf(4139,plain,
% 60.87/61.65 (P8(x41391,x41392,x41392,x41391,x41393,x41394,x41394,x41393)),
% 60.87/61.65 inference(scs_inference,[],[3989,4095,3993,3682,3949,3985,3959,3973,4006,4034,4085,4022,4043,4032,3751,4083,1235,252,222,152,150,149,164,229,163,254,160,253,255,221,147,161,148,162,159,220,248,167,251])).
% 60.87/61.65 cnf(4141,plain,
% 60.87/61.65 (P8(x41411,x41412,a2,a2,x41411,x41412,a1,a1)),
% 60.87/61.65 inference(scs_inference,[],[3989,4095,3993,3682,3949,3967,3985,3959,3973,4006,4034,4085,4022,4043,4032,3751,4083,1235,252,222,152,150,149,164,229,163,254,160,253,255,221,147,161,148,162,159,220,248,167,251,249])).
% 60.87/61.65 cnf(4145,plain,
% 60.87/61.65 (P3(x41451,x41452,x41453,x41452)),
% 60.87/61.65 inference(scs_inference,[],[3989,4095,3993,4057,3682,3949,3967,3985,3453,3959,3973,4006,4034,4085,4022,4043,4032,3751,4083,1235,252,222,152,150,149,164,229,163,254,160,253,255,221,147,161,148,162,159,220,248,167,251,249,250,166])).
% 60.87/61.65 cnf(4148,plain,
% 60.87/61.65 (P10(x41481,x41482,x41481,x41482)),
% 60.87/61.65 inference(rename_variables,[],[3862])).
% 60.87/61.65 cnf(4151,plain,
% 60.87/61.65 (P3(x41511,x41512,x41513,x41513)),
% 60.87/61.65 inference(rename_variables,[],[4057])).
% 60.87/61.65 cnf(4154,plain,
% 60.87/61.65 (P10(x41541,x41542,x41542,x41541)),
% 60.87/61.65 inference(rename_variables,[],[3971])).
% 60.87/61.65 cnf(4156,plain,
% 60.87/61.65 (P2(f9(x41561,x41561,x41562),x41561,x41561,x41562)),
% 60.87/61.65 inference(scs_inference,[],[3971,4154,3989,4095,3993,4057,3682,3949,3967,3985,3453,3959,3973,4006,4017,4034,4085,4022,4043,4032,3751,4083,3862,1235,252,222,152,150,149,164,229,163,254,160,253,255,221,147,161,148,162,159,220,248,167,251,249,250,166,190,226,184,187])).
% 60.87/61.65 cnf(4157,plain,
% 60.87/61.65 (P10(x41571,x41572,x41572,x41571)),
% 60.87/61.65 inference(rename_variables,[],[3971])).
% 60.87/61.65 cnf(4160,plain,
% 60.87/61.65 (P8(x41601,x41602,x41602,x41601,x41603,x41604,x41603,x41604)),
% 60.87/61.65 inference(rename_variables,[],[3843])).
% 60.87/61.65 cnf(4165,plain,
% 60.87/61.65 (P10(x41651,x41652,x41652,x41651)),
% 60.87/61.65 inference(rename_variables,[],[3971])).
% 60.87/61.65 cnf(4167,plain,
% 60.87/61.65 (P4(x41671,a1,x41671,f26(a1,x41671,a1,a2,a1))),
% 60.87/61.65 inference(scs_inference,[],[3971,4154,4157,4165,3989,4095,3993,4057,3682,3949,3967,3985,3453,3959,3973,4006,4017,4034,4085,4022,4043,4032,3751,4083,3873,3843,3862,1235,252,222,152,150,149,164,229,163,254,160,253,255,221,147,161,148,162,159,220,248,167,251,249,250,166,190,226,184,187,245,177,173,196])).
% 60.87/61.65 cnf(4168,plain,
% 60.87/61.65 (P10(x41681,x41682,x41682,x41681)),
% 60.87/61.65 inference(rename_variables,[],[3971])).
% 60.87/61.65 cnf(4171,plain,
% 60.87/61.65 (P10(x41711,x41712,x41712,x41711)),
% 60.87/61.65 inference(rename_variables,[],[3971])).
% 60.87/61.65 cnf(4176,plain,
% 60.87/61.65 (P10(x41761,x41762,x41761,x41762)),
% 60.87/61.65 inference(rename_variables,[],[3862])).
% 60.87/61.65 cnf(4180,plain,
% 60.87/61.65 (P4(a2,f24(a2,a2,a2,a2,a2,a2),x41801,f24(a2,a2,a2,a2,a2,a2))),
% 60.87/61.65 inference(scs_inference,[],[3971,4154,4157,4165,4168,4171,3989,4095,3993,4057,3682,3949,3967,3985,3453,3959,3973,4006,4017,4034,4085,4022,4043,4032,3751,4083,3873,3843,3862,4148,3759,1235,252,222,152,150,149,164,229,163,254,160,253,255,221,147,161,148,162,159,220,248,167,251,249,250,166,190,226,184,187,245,177,173,196,172,200,189,241,170])).
% 60.87/61.65 cnf(4181,plain,
% 60.87/61.65 (P10(x41811,x41812,x41812,x41811)),
% 60.87/61.65 inference(rename_variables,[],[3971])).
% 60.87/61.65 cnf(4187,plain,
% 60.87/61.65 (P10(x41871,x41872,x41872,x41871)),
% 60.87/61.65 inference(rename_variables,[],[3971])).
% 60.87/61.65 cnf(4190,plain,
% 60.87/61.65 (P3(x41901,x41902,x41903,x41903)),
% 60.87/61.65 inference(rename_variables,[],[4057])).
% 60.87/61.65 cnf(4192,plain,
% 60.87/61.65 (P3(x41921,x41922,x41923,x41923)),
% 60.87/61.65 inference(rename_variables,[],[4057])).
% 60.87/61.65 cnf(4198,plain,
% 60.87/61.65 (P10(x41981,x41982,x41982,x41981)),
% 60.87/61.65 inference(rename_variables,[],[3971])).
% 60.87/61.65 cnf(4200,plain,
% 60.87/61.65 (P2(a1,a1,a2,a2)),
% 60.87/61.65 inference(scs_inference,[],[142,3971,4154,4157,4165,4168,4171,4181,4187,3989,4095,3993,4057,4151,4190,3682,3949,3967,3985,3453,3959,3973,4006,4017,4034,4085,4022,4043,4032,3751,4083,3873,3843,357,3862,4148,4176,3759,1235,252,222,152,150,149,164,229,163,254,160,253,255,221,147,161,148,162,159,220,248,167,251,249,250,166,190,226,184,187,245,177,173,196,172,200,189,241,170,242,193,110,109,236,194,180])).
% 60.87/61.65 cnf(4202,plain,
% 60.87/61.65 (P10(a2,a2,a1,a1)),
% 60.87/61.65 inference(scs_inference,[],[142,3971,4154,4157,4165,4168,4171,4181,4187,4198,3989,4095,3993,4057,4151,4190,3682,3949,3967,3985,3453,3959,3973,4006,4017,4034,4085,4022,4043,4032,3751,4083,3873,3843,357,3862,4148,4176,3759,1235,252,222,152,150,149,164,229,163,254,160,253,255,221,147,161,148,162,159,220,248,167,251,249,250,166,190,226,184,187,245,177,173,196,172,200,189,241,170,242,193,110,109,236,194,180,237])).
% 60.87/61.65 cnf(4203,plain,
% 60.87/61.65 (P8(a2,a2,x42031,x42032,a1,a1,x42031,x42032)),
% 60.87/61.65 inference(rename_variables,[],[3967])).
% 60.87/61.65 cnf(4204,plain,
% 60.87/61.65 (P10(x42041,x42042,x42042,x42041)),
% 60.87/61.65 inference(rename_variables,[],[3971])).
% 60.87/61.65 cnf(4207,plain,
% 60.87/61.65 (P10(x42071,x42072,x42072,x42071)),
% 60.87/61.65 inference(rename_variables,[],[3971])).
% 60.87/61.65 cnf(4209,plain,
% 60.87/61.65 (P10(a1,a2,a2,a2)),
% 60.87/61.65 inference(scs_inference,[],[142,3971,4154,4157,4165,4168,4171,4181,4187,4198,4204,3989,4095,3993,4057,4151,4190,3682,3949,3967,3985,3453,3959,3973,4006,4017,4034,4085,4022,4043,4032,3751,4083,3898,3873,3837,3843,357,3862,4148,4176,3759,1235,252,222,152,150,149,164,229,163,254,160,253,255,221,147,161,148,162,159,220,248,167,251,249,250,166,190,226,184,187,245,177,173,196,172,200,189,241,170,242,193,110,109,236,194,180,237,169,168])).
% 60.87/61.65 cnf(4210,plain,
% 60.87/61.65 (P1(x42101,x42101,x42102)),
% 60.87/61.65 inference(rename_variables,[],[3837])).
% 60.87/61.65 cnf(4212,plain,
% 60.87/61.65 (P7(f24(a2,a2,a2,a2,a2,a2),a2,a2,a2,f24(a2,a2,a2,a2,a2,a2),a2,a2,a2)),
% 60.87/61.65 inference(scs_inference,[],[142,3971,4154,4157,4165,4168,4171,4181,4187,4198,4204,3989,4095,3993,4057,4151,4190,3682,3949,3967,3985,3453,3959,3973,4006,4017,4034,4085,4022,4043,4032,3751,4083,3898,3873,3837,3843,357,3862,4148,4176,3759,1235,252,222,152,150,149,164,229,163,254,160,253,255,221,147,161,148,162,159,220,248,167,251,249,250,166,190,226,184,187,245,177,173,196,172,200,189,241,170,242,193,110,109,236,194,180,237,169,168,219])).
% 60.87/61.65 cnf(4214,plain,
% 60.87/61.65 (P9(f26(a1,x42141,a1,a2,a1),a1,a1,x42141)),
% 60.87/61.65 inference(scs_inference,[],[142,3971,4154,4157,4165,4168,4171,4181,4187,4198,4204,4207,3989,4095,3993,4057,4151,4190,3682,3949,3967,3985,3453,3959,3973,4006,4017,4034,4085,4022,4043,4032,3751,4083,3898,3873,3837,3843,357,3862,4148,4176,3759,1235,252,222,152,150,149,164,229,163,254,160,253,255,221,147,161,148,162,159,220,248,167,251,249,250,166,190,226,184,187,245,177,173,196,172,200,189,241,170,242,193,110,109,236,194,180,237,169,168,219,197])).
% 60.87/61.65 cnf(4215,plain,
% 60.87/61.65 (P10(x42151,x42152,x42152,x42151)),
% 60.87/61.65 inference(rename_variables,[],[3971])).
% 60.87/61.65 cnf(4218,plain,
% 60.87/61.65 (P10(x42181,x42182,x42182,x42181)),
% 60.87/61.65 inference(rename_variables,[],[3971])).
% 60.87/61.65 cnf(4221,plain,
% 60.87/61.65 (P10(x42211,x42212,x42212,x42211)),
% 60.87/61.65 inference(rename_variables,[],[3971])).
% 60.87/61.65 cnf(4227,plain,
% 60.87/61.65 (P2(x42271,x42271,x42271,x42271)),
% 60.87/61.65 inference(rename_variables,[],[4036])).
% 60.87/61.65 cnf(4229,plain,
% 60.87/61.65 (P8(a2,a2,a1,a1,x42291,x42292,x42292,x42291)),
% 60.87/61.65 inference(scs_inference,[],[142,4036,3971,4154,4157,4165,4168,4171,4181,4187,4198,4204,4207,4215,4218,4221,3981,3989,4095,3993,4057,4151,4190,3682,3949,3967,4203,3985,3453,3959,3973,4006,4017,4034,4085,4022,4043,4032,3751,4083,3898,3873,3837,3843,357,3862,4148,4176,3759,1235,252,222,152,150,149,164,229,163,254,160,253,255,221,147,161,148,162,159,220,248,167,251,249,250,166,190,226,184,187,245,177,173,196,172,200,189,241,170,242,193,110,109,236,194,180,237,169,168,219,197,185,195,186,223,258])).
% 60.87/61.65 cnf(4231,plain,
% 60.87/61.65 (P8(x42311,x42312,x42311,x42312,x42313,x42314,x42314,x42313)),
% 60.87/61.65 inference(rename_variables,[],[3981])).
% 60.87/61.65 cnf(4236,plain,
% 60.87/61.65 (P10(a3,a18,a18,a18)),
% 60.87/61.65 inference(scs_inference,[],[142,4036,3971,4154,4157,4165,4168,4171,4181,4187,4198,4204,4207,4215,4218,4221,3981,3989,4095,3993,4057,4151,4190,3682,3949,3967,4203,3985,3453,3959,3973,4006,4017,4034,4085,4022,4043,4032,3696,3751,4083,3898,3873,3902,3837,3843,357,3862,4148,4176,3684,3759,1235,252,222,152,150,149,164,229,163,254,160,253,255,221,147,161,148,162,159,220,248,167,251,249,250,166,190,226,184,187,245,177,173,196,172,200,189,241,170,242,193,110,109,236,194,180,237,169,168,219,197,185,195,186,223,258,232,191])).
% 60.87/61.65 cnf(4238,plain,
% 60.87/61.65 (P4(x42381,x42381,x42381,x42381)),
% 60.87/61.65 inference(rename_variables,[],[3902])).
% 60.87/61.65 cnf(4243,plain,
% 60.87/61.65 (P6(x42431,x42431,x42431)),
% 60.87/61.65 inference(scs_inference,[],[142,4036,4227,3971,4154,4157,4165,4168,4171,4181,4187,4198,4204,4207,4215,4218,4221,3981,4231,3989,4095,3993,4057,4151,4190,3682,3949,3967,4203,3985,3453,3959,3973,4006,4017,4034,4085,4022,4043,4032,3696,3751,4083,4051,3898,3873,3902,3837,4210,3843,357,3862,4148,4176,3684,3571,3759,1235,252,222,152,150,149,164,229,163,254,160,253,255,221,147,161,148,162,159,220,248,167,251,249,250,166,190,226,184,187,245,177,173,196,172,200,189,241,170,242,193,110,109,236,194,180,237,169,168,219,197,185,195,186,223,258,232,191,188,235])).
% 60.87/61.65 cnf(4244,plain,
% 60.87/61.65 (P8(x42441,x42442,x42441,x42442,x42443,x42444,x42444,x42443)),
% 60.87/61.65 inference(rename_variables,[],[3981])).
% 60.87/61.65 cnf(4245,plain,
% 60.87/61.65 (P1(x42451,x42451,x42452)),
% 60.87/61.65 inference(rename_variables,[],[3837])).
% 60.87/61.65 cnf(4248,plain,
% 60.87/61.65 (P4(x42481,x42481,x42481,x42481)),
% 60.87/61.65 inference(rename_variables,[],[3902])).
% 60.87/61.65 cnf(4249,plain,
% 60.87/61.65 (P2(x42491,x42491,x42491,x42491)),
% 60.87/61.65 inference(rename_variables,[],[4036])).
% 60.87/61.65 cnf(4264,plain,
% 60.87/61.65 (P6(f20(a18,x42641),a18,x42641)),
% 60.87/61.65 inference(scs_inference,[],[142,4036,4227,4249,3971,4154,4157,4165,4168,4171,4181,4187,4198,4204,4207,4215,4218,4221,3981,4231,4244,3989,4095,3993,4057,4151,4190,3682,3949,3967,4203,3985,3453,3690,3959,3973,4006,4017,4034,4085,4022,4043,4032,3696,3751,4083,3953,4051,3898,3213,3873,3902,4238,4248,3837,4210,4245,3843,357,3862,4148,4176,3684,3936,3603,3601,3809,588,3571,3759,1235,252,222,152,150,149,164,229,163,254,160,253,255,221,147,161,148,162,159,220,248,167,251,249,250,166,190,226,184,187,245,177,173,196,172,200,189,241,170,242,193,110,109,236,194,180,237,169,168,219,197,185,195,186,223,258,232,191,188,235,208,209,204,247,203,155])).
% 60.87/61.65 cnf(4276,plain,
% 60.87/61.65 (P1(f23(a2,a2,a1,a2),a1,a2)),
% 60.87/61.65 inference(scs_inference,[],[142,4036,4227,4249,3971,4154,4157,4165,4168,4171,4181,4187,4198,4204,4207,4215,4218,4221,3981,4231,4244,3989,4095,3993,4057,4151,4190,4192,3682,3949,3967,4203,3985,3453,3690,3959,3973,4006,4017,4034,4085,4022,4043,4032,3696,3751,4083,3953,4051,3898,3213,3873,3902,4238,4248,3837,4210,4245,3843,4160,357,3862,4148,4176,3684,3936,3603,3601,3809,588,3571,3759,1235,252,222,152,150,149,164,229,163,254,160,253,255,221,147,161,148,162,159,220,248,167,251,249,250,166,190,226,184,187,245,177,173,196,172,200,189,241,170,242,193,110,109,236,194,180,237,169,168,219,197,185,195,186,223,258,232,191,188,235,208,209,204,247,203,155,3439,183,165,3,246])).
% 60.87/61.65 cnf(4284,plain,
% 60.87/61.65 (P2(f9(a1,a2,a2),a1,a2,a2)),
% 60.87/61.65 inference(scs_inference,[],[142,4036,4227,4249,3971,4154,4157,4165,4168,4171,4181,4187,4198,4204,4207,4215,4218,4221,3981,4231,4244,3989,4095,3993,4057,4151,4190,4192,3682,3949,3967,4203,3985,3453,3690,3959,3973,4006,4017,4034,4085,4022,4043,4032,3696,3751,4083,3953,4051,3898,3213,3873,3902,4238,4248,3837,4210,4245,3843,4160,357,3862,4148,4176,3684,3936,3603,3601,3809,588,3571,3759,1235,252,222,152,150,149,164,229,163,254,160,253,255,221,147,161,148,162,159,220,248,167,251,249,250,166,190,226,184,187,245,177,173,196,172,200,189,241,170,242,193,110,109,236,194,180,237,169,168,219,197,185,195,186,223,258,232,191,188,235,208,209,204,247,203,155,3439,183,165,3,246,201,199,2,3477])).
% 60.87/61.65 cnf(4292,plain,
% 60.87/61.65 (P6(a3,a18,a18)),
% 60.87/61.65 inference(scs_inference,[],[4243,1481])).
% 60.87/61.65 cnf(4293,plain,
% 60.87/61.65 (P6(x42931,x42931,x42931)),
% 60.87/61.65 inference(rename_variables,[],[4243])).
% 60.87/61.65 cnf(4296,plain,
% 60.87/61.65 (P6(x42961,x42961,x42961)),
% 60.87/61.65 inference(rename_variables,[],[4243])).
% 60.87/61.65 cnf(4299,plain,
% 60.87/61.65 (P6(x42991,x42991,x42991)),
% 60.87/61.65 inference(rename_variables,[],[4243])).
% 60.87/61.65 cnf(4301,plain,
% 60.87/61.65 (P7(a3,a18,a3,a18,a3,a18,a18,a3)),
% 60.87/61.65 inference(scs_inference,[],[4243,4293,4296,4117,1481,1483,1478,252])).
% 60.87/61.65 cnf(4303,plain,
% 60.87/61.65 (P8(x43031,x43031,x43031,f26(x43031,x43031,x43031,x43031,x43031),x43031,f26(x43031,x43031,x43031,x43031,x43031),x43031,f26(x43031,x43031,x43031,x43031,x43031))),
% 60.87/61.65 inference(scs_inference,[],[4243,4293,4296,4117,4045,1481,1483,1478,252,222])).
% 60.87/61.65 cnf(4309,plain,
% 60.87/61.65 (P4(x43091,x43091,f26(x43091,x43091,x43091,x43091,x43091),x43091)),
% 60.87/61.65 inference(scs_inference,[],[4243,4293,4296,4117,4045,3886,1481,1483,1478,252,222,152,150,164])).
% 60.87/61.65 cnf(4315,plain,
% 60.87/61.65 (P7(a18,a3,a18,a3,a3,a18,a3,a18)),
% 60.87/61.65 inference(scs_inference,[],[4243,4293,4296,4117,4045,3886,1481,1483,1478,252,222,152,150,164,149,229,254])).
% 60.87/61.65 cnf(4317,plain,
% 60.87/61.65 (P4(a2,a1,a1,a1)),
% 60.87/61.65 inference(scs_inference,[],[4243,4293,4296,4107,4117,4045,3886,1481,1483,1478,252,222,152,150,164,149,229,254,163])).
% 60.87/61.65 cnf(4319,plain,
% 60.87/61.65 (P7(a3,a18,a18,a3,a3,a18,a18,a3)),
% 60.87/61.65 inference(scs_inference,[],[4243,4293,4296,4107,4113,4117,4045,3886,1481,1483,1478,252,222,152,150,164,149,229,254,163,253])).
% 60.87/61.65 cnf(4323,plain,
% 60.87/61.65 (P8(a1,a1,x43231,x43232,a1,a2,x43231,x43232)),
% 60.87/61.65 inference(scs_inference,[],[4243,4293,4296,4107,4109,4113,4117,4045,3886,4214,1481,1483,1478,252,222,152,150,164,149,229,254,163,253,160,221])).
% 60.87/61.65 cnf(4327,plain,
% 60.87/61.65 (P10(a1,a1,a2,a2)),
% 60.87/61.65 inference(scs_inference,[],[4243,4293,4296,4107,4109,4113,4117,4202,4045,3886,4214,4212,1481,1483,1478,252,222,152,150,164,149,229,254,163,253,160,221,255,161])).
% 60.87/61.65 cnf(4329,plain,
% 60.87/61.65 (P1(x43291,x43292,f6(x43292,x43292,x43291))),
% 60.87/61.65 inference(scs_inference,[],[4243,4293,4296,4107,4109,4113,4117,4202,4045,4123,3886,4214,4212,1481,1483,1478,252,222,152,150,164,149,229,254,163,253,160,221,255,161,148])).
% 60.87/61.65 cnf(4333,plain,
% 60.87/61.66 (P9(a1,a2,a1,a1)),
% 60.87/61.66 inference(scs_inference,[],[4243,4293,4296,4107,4109,4113,4117,4202,4045,4123,4127,3886,4214,4212,1481,1483,1478,252,222,152,150,164,149,229,254,163,253,160,221,255,161,148,147,159])).
% 60.87/61.66 cnf(4337,plain,
% 60.87/61.66 (P8(x43371,x43372,x43371,x43373,x43373,x43372,x43373,x43373)),
% 60.87/61.66 inference(scs_inference,[],[4243,4293,4296,4145,4107,4109,4113,4117,4202,4045,4123,4127,3886,4214,3977,4212,1481,1483,1478,252,222,152,150,164,149,229,254,163,253,160,221,255,161,148,147,159,162,220])).
% 60.87/61.66 cnf(4343,plain,
% 60.87/61.66 (P3(x43431,x43432,x43433,x43431)),
% 60.87/61.66 inference(scs_inference,[],[4243,4293,4296,4145,4121,4141,4107,4109,4113,4117,4202,4045,4123,4127,3886,4214,3977,4212,1481,1483,1478,252,222,152,150,164,149,229,254,163,253,160,221,255,161,148,147,159,162,220,248,251,165])).
% 60.87/61.66 cnf(4345,plain,
% 60.87/61.66 (P3(x43451,x43452,x43452,x43453)),
% 60.87/61.66 inference(scs_inference,[],[4243,4293,4296,4145,4121,4141,4107,4109,4113,4117,4202,4045,4123,4127,3886,4214,3977,4212,1481,1483,1478,252,222,152,150,164,149,229,254,163,253,160,221,255,161,148,147,159,162,220,248,251,165,167])).
% 60.87/61.66 cnf(4359,plain,
% 60.87/61.66 (P10(a1,a2,a1,a1)),
% 60.87/61.66 inference(scs_inference,[],[4243,4293,4296,4145,3841,4121,4141,4229,4107,4109,4113,4117,4202,4236,4045,4123,4127,3886,4167,4214,3977,4212,371,3936,1481,1483,1478,252,222,152,150,164,149,229,254,163,253,160,221,255,161,148,147,159,162,220,248,251,165,167,249,250,166,179,190,107,177])).
% 60.87/61.66 cnf(4361,plain,
% 60.87/61.66 (P9(f24(x43611,x43611,x43611,x43611,x43611,x43611),x43611,x43611,x43611)),
% 60.87/61.66 inference(scs_inference,[],[4243,4293,4296,4299,4145,3841,4121,4141,4229,4107,4109,4113,4117,4202,4236,4045,4123,4127,3886,4167,4214,3977,4212,371,3936,1481,1483,1478,252,222,152,150,164,149,229,254,163,253,160,221,255,161,148,147,159,162,220,248,251,165,167,249,250,166,179,190,107,177,200])).
% 60.87/61.66 cnf(4367,plain,
% 60.87/61.66 (P10(x43671,x43672,x43672,x43671)),
% 60.87/61.66 inference(rename_variables,[],[3971])).
% 60.87/61.66 cnf(4370,plain,
% 60.87/61.66 (P4(x43701,x43701,x43701,x43701)),
% 60.87/61.66 inference(rename_variables,[],[3902])).
% 60.87/61.66 cnf(4376,plain,
% 60.87/61.66 (P10(x43761,x43762,x43762,x43761)),
% 60.87/61.66 inference(rename_variables,[],[3971])).
% 60.87/61.66 cnf(4378,plain,
% 60.87/61.66 (P1(f5(x43781,x43781,x43782),x43782,x43781)),
% 60.87/61.66 inference(scs_inference,[],[4243,4293,4296,4299,4145,3841,4121,4141,4229,4099,4107,4109,4113,4117,4202,4209,4236,4045,4129,4123,4127,3886,4167,4214,3977,4212,3971,4367,371,3902,3843,3862,3936,1481,1483,1478,252,222,152,150,164,149,229,254,163,253,160,221,255,161,148,147,159,162,220,248,251,165,167,249,250,166,179,190,107,177,200,246,184,196,245,172,173])).
% 60.87/61.66 cnf(4380,plain,
% 60.87/61.66 (P10(a3,a1,a2,a3)),
% 60.87/61.66 inference(scs_inference,[],[4243,4293,4296,4299,4145,3841,4121,4141,4229,3845,4099,4107,4109,4113,4117,4202,4209,4236,4045,4129,4123,4127,3886,4167,4214,3977,4212,3971,4367,371,3902,3843,3862,3936,1481,1483,1478,252,222,152,150,164,149,229,254,163,253,160,221,255,161,148,147,159,162,220,248,251,165,167,249,250,166,179,190,107,177,200,246,184,196,245,172,173,237])).
% 60.87/61.66 cnf(4383,plain,
% 60.87/61.66 (P10(x43831,x43832,x43832,x43831)),
% 60.87/61.66 inference(rename_variables,[],[3971])).
% 60.87/61.66 cnf(4385,plain,
% 60.87/61.66 (P9(a1,a1,f26(a2,a2,a2,a2,a2),a2)),
% 60.87/61.66 inference(scs_inference,[],[4243,4293,4296,4299,4145,3841,4125,4121,4141,4229,3845,4099,4107,4109,4113,4117,4202,4209,4236,4045,4131,4129,4123,4127,3886,4167,4214,3977,4212,3971,4367,4376,371,3902,3843,3862,3936,1481,1483,1478,252,222,152,150,164,149,229,254,163,253,160,221,255,161,148,147,159,162,220,248,251,165,167,249,250,166,179,190,107,177,200,246,184,196,245,172,173,237,174,236])).
% 60.87/61.66 cnf(4391,plain,
% 60.87/61.66 (P9(f26(a1,a2,a2,a2,a2),a2,a1,a2)),
% 60.87/61.66 inference(scs_inference,[],[4243,4293,4296,4299,4145,3841,4125,4121,4141,4229,3845,4099,4107,4109,4113,4117,4202,4209,4236,4045,4131,4129,4123,4127,3886,4167,4214,3977,4212,3971,4367,4376,371,3902,4370,3843,3862,3936,1481,1483,1478,252,222,152,150,164,149,229,254,163,253,160,221,255,161,148,147,159,162,220,248,251,165,167,249,250,166,179,190,107,177,200,246,184,196,245,172,173,237,174,236,180,197])).
% 60.87/61.66 cnf(4392,plain,
% 60.87/61.66 (P4(x43921,x43921,x43921,x43921)),
% 60.87/61.66 inference(rename_variables,[],[3902])).
% 60.87/61.66 cnf(4396,plain,
% 60.87/61.66 (P4(a1,a2,a1,a2)),
% 60.87/61.66 inference(scs_inference,[],[4243,4293,4296,4299,4145,3841,4125,4121,4141,4229,3845,4099,4107,4109,4113,4117,4202,4209,4236,4045,4131,4129,4123,4127,3886,4167,4214,3977,4212,3971,4367,4376,371,3902,4370,3843,3862,3936,1481,1483,1478,252,222,152,150,164,149,229,254,163,253,160,221,255,161,148,147,159,162,220,248,251,165,167,249,250,166,179,190,107,177,200,246,184,196,245,172,173,237,174,236,180,197,219,169])).
% 60.87/61.66 cnf(4397,plain,
% 60.87/61.66 (P6(x43971,x43971,x43971)),
% 60.87/61.66 inference(rename_variables,[],[4243])).
% 60.87/61.66 cnf(4400,plain,
% 60.87/61.66 (P10(x44001,x44002,x44002,x44001)),
% 60.87/61.66 inference(rename_variables,[],[3971])).
% 60.87/61.66 cnf(4407,plain,
% 60.87/61.66 (P10(x44071,x44072,x44072,x44071)),
% 60.87/61.66 inference(rename_variables,[],[3971])).
% 60.87/61.66 cnf(4409,plain,
% 60.87/61.66 (P6(f24(x44091,x44091,x44091,x44091,x44091,x44091),x44091,x44091)),
% 60.87/61.66 inference(scs_inference,[],[4243,4293,4296,4299,4397,4145,3841,4125,4121,4141,4229,3845,4099,4107,4109,4113,4117,4202,4209,4236,4045,4131,4129,4123,4127,3886,4167,4214,3977,4212,3971,4367,4376,4383,4400,371,3902,4370,3843,3862,4017,3936,1481,1483,1478,252,222,152,150,164,149,229,254,163,253,160,221,255,161,148,147,159,162,220,248,251,165,167,249,250,166,179,190,107,177,200,246,184,196,245,172,173,237,174,236,180,197,219,169,185,201,195,186,199])).
% 60.87/61.66 cnf(4413,plain,
% 60.87/61.66 (P9(a18,a18,a3,a3)),
% 60.87/61.66 inference(scs_inference,[],[4243,4293,4296,4299,4397,4145,3841,4125,4121,4141,4229,3845,4099,4107,4109,4113,4117,4202,4209,4236,4045,4131,4129,4123,4127,3886,4167,4214,3977,4212,4060,3971,4367,4376,4383,4400,4407,371,3902,4370,3843,3862,4017,3936,1481,1483,1478,252,222,152,150,164,149,229,254,163,253,160,221,255,161,148,147,159,162,220,248,251,165,167,249,250,166,179,190,107,177,200,246,184,196,245,172,173,237,174,236,180,197,219,169,185,201,195,186,199,223,176])).
% 60.87/61.66 cnf(4414,plain,
% 60.87/61.66 (P10(x44141,x44142,x44142,x44141)),
% 60.87/61.66 inference(rename_variables,[],[3971])).
% 60.87/61.66 cnf(4416,plain,
% 60.87/61.66 (P8(a1,f9(a1,a2,a2),a1,a2,a2,a1,a2,a2)),
% 60.87/61.66 inference(scs_inference,[],[4243,4293,4296,4299,4397,4145,3841,4125,4121,4141,4229,3845,4099,4107,4109,4113,4117,4202,4209,4236,4045,4131,4129,4123,4127,4284,3886,4167,4214,3977,4212,4060,3971,4367,4376,4383,4400,4407,4414,371,3902,4370,3843,3862,4017,3936,1481,1483,1478,252,222,152,150,164,149,229,254,163,253,160,221,255,161,148,147,159,162,220,248,251,165,167,249,250,166,179,190,107,177,200,246,184,196,245,172,173,237,174,236,180,197,219,169,185,201,195,186,199,223,176,225])).
% 60.87/61.66 cnf(4417,plain,
% 60.87/61.66 (P10(x44171,x44172,x44172,x44171)),
% 60.87/61.66 inference(rename_variables,[],[3971])).
% 60.87/61.66 cnf(4422,plain,
% 60.87/61.66 (P6(x44221,x44221,x44221)),
% 60.87/61.66 inference(rename_variables,[],[4243])).
% 60.87/61.66 cnf(4423,plain,
% 60.87/61.66 (P3(x44231,x44231,x44231,x44232)),
% 60.87/61.66 inference(rename_variables,[],[4137])).
% 60.87/61.66 cnf(4426,plain,
% 60.87/61.66 (P3(x44261,x44261,x44261,x44262)),
% 60.87/61.66 inference(rename_variables,[],[4137])).
% 60.87/61.66 cnf(4429,plain,
% 60.87/61.66 (P6(f8(a3,a1,a2,a18),a3,f5(a3,a3,a18))),
% 60.87/61.66 inference(scs_inference,[],[142,4243,4293,4296,4299,4397,4422,4137,4423,4145,3841,4125,4121,4141,4229,3845,4099,4107,4109,4113,4117,4202,4209,4236,4045,4131,4129,4123,4127,4284,3886,4101,3827,4167,4214,3977,4212,4060,3971,4367,4376,4383,4400,4407,4414,371,3902,4370,4392,3843,3305,3862,4017,3936,1481,1483,1478,252,222,152,150,164,149,229,254,163,253,160,221,255,161,148,147,159,162,220,248,251,165,167,249,250,166,179,190,107,177,200,246,184,196,245,172,173,237,174,236,180,197,219,169,185,201,195,186,199,223,176,225,151,188,191,158])).
% 60.87/61.66 cnf(4430,plain,
% 60.87/61.66 (P6(x44301,x44301,x44301)),
% 60.87/61.66 inference(rename_variables,[],[4243])).
% 60.87/61.66 cnf(4432,plain,
% 60.87/61.66 (P6(f7(x44321,x44321,x44321),x44321,x44321)),
% 60.87/61.66 inference(scs_inference,[],[142,4243,4293,4296,4299,4397,4422,4430,4137,4423,4145,3841,4125,4121,4141,4229,3845,4099,4107,4109,4113,4117,4202,4209,4236,4045,4131,4129,4123,4127,4284,3886,4101,3827,4167,4214,3977,4212,4060,3971,4367,4376,4383,4400,4407,4414,4417,371,3902,4370,4392,3843,3305,3862,4017,3936,1481,1483,1478,252,222,152,150,164,149,229,254,163,253,160,221,255,161,148,147,159,162,220,248,251,165,167,249,250,166,179,190,107,177,200,246,184,196,245,172,173,237,174,236,180,197,219,169,185,201,195,186,199,223,176,225,151,188,191,158,182])).
% 60.87/61.66 cnf(4438,plain,
% 60.87/61.66 (P1(x44381,x44381,x44382)),
% 60.87/61.66 inference(rename_variables,[],[3837])).
% 60.87/61.66 cnf(4441,plain,
% 60.87/61.66 (P4(x44411,x44411,x44412,x44412)),
% 60.87/61.66 inference(scs_inference,[],[142,4243,4293,4296,4299,4397,4422,4430,4137,4423,4426,4139,4145,3841,4125,4121,4141,4229,3845,4099,4107,4109,4113,4117,4202,4209,4236,4045,4131,4129,4123,4127,4284,3886,4101,3827,4167,4214,3977,4212,4060,3971,4367,4376,4383,4400,4407,4414,4417,371,3902,4370,4392,3837,3843,3305,3862,4017,3936,3571,1481,1483,1478,252,222,152,150,164,149,229,254,163,253,160,221,255,161,148,147,159,162,220,248,251,165,167,249,250,166,179,190,107,177,200,246,184,196,245,172,173,237,174,236,180,197,219,169,185,201,195,186,199,223,176,225,151,188,191,158,182,205,247])).
% 60.87/61.66 cnf(4448,plain,
% 60.87/61.66 (P6(x44481,x44481,x44481)),
% 60.87/61.66 inference(rename_variables,[],[4243])).
% 60.87/61.66 cnf(4451,plain,
% 60.87/61.66 (P6(x44511,x44511,x44511)),
% 60.87/61.66 inference(rename_variables,[],[4243])).
% 60.87/61.66 cnf(4462,plain,
% 60.87/61.66 (P10(x44621,f26(x44621,x44621,x44621,x44621,x44621),f26(x44621,x44621,x44621,x44621,x44621),f26(x44621,x44621,x44621,x44621,x44621))),
% 60.87/61.66 inference(scs_inference,[],[142,4243,4293,4296,4299,4397,4422,4430,4448,4451,4137,4423,4426,4139,4145,3841,4125,4121,4141,4229,3845,3947,4099,4107,4109,4113,4115,4117,4202,4209,4236,4045,4131,4129,4123,4127,4284,3886,4101,3827,4167,4264,4214,3977,4212,4060,3971,4367,4376,4383,4400,4407,4414,4417,3213,371,3902,4370,4392,3837,4438,3843,3305,3862,4017,3601,3936,3571,1481,1483,1478,252,222,152,150,164,149,229,254,163,253,160,221,255,161,148,147,159,162,220,248,251,165,167,249,250,166,179,190,107,177,200,246,184,196,245,172,173,237,174,236,180,197,219,169,185,201,195,186,199,223,176,225,151,188,191,158,182,205,247,204,155,1928,2,243,194,168])).
% 60.87/61.66 cnf(4480,plain,
% 60.87/61.66 (P6(f24(x44801,x44801,x44801,x44801,x44801,x44801),x44801,x44801)),
% 60.87/61.66 inference(rename_variables,[],[4409])).
% 60.87/61.66 cnf(4488,plain,
% 60.87/61.66 (P4(a1,a2,a2,a1)),
% 60.87/61.66 inference(scs_inference,[],[4315,4396,4409,4429,1481,252,222,150,164])).
% 60.87/61.66 cnf(4490,plain,
% 60.87/61.66 (P4(f24(x44901,x44901,x44901,x44901,x44901,x44901),x44901,f24(x44901,x44901,x44901,x44901,x44901,x44901),x44901)),
% 60.87/61.66 inference(scs_inference,[],[4315,4396,4409,4480,4429,1481,252,222,150,164,152])).
% 60.87/61.66 cnf(4496,plain,
% 60.87/61.66 (P7(a18,a3,a3,a18,a3,a18,a18,a3)),
% 60.87/61.66 inference(scs_inference,[],[4301,4315,4396,4309,4409,4480,4429,4103,1481,252,222,150,164,152,149,163,254])).
% 60.87/61.66 cnf(4506,plain,
% 60.87/61.66 (P10(a1,a1,a1,a2)),
% 60.87/61.66 inference(scs_inference,[],[4301,4315,4333,4359,4396,4309,4409,4480,4429,4103,4385,4034,1481,252,222,150,164,152,149,163,254,160,253,255,221,161])).
% 60.87/61.66 cnf(4508,plain,
% 60.87/61.66 (P9(a3,a3,a18,a18)),
% 60.87/61.66 inference(scs_inference,[],[4301,4315,4333,4359,4396,4413,4309,4409,4480,4429,4103,4385,4034,1481,252,222,150,164,152,149,163,254,160,253,255,221,161,159])).
% 60.87/61.66 cnf(4512,plain,
% 60.87/61.66 (P1(f5(x45121,x45121,x45122),x45121,x45122)),
% 60.87/61.66 inference(scs_inference,[],[4301,4315,4333,4359,4396,4413,4309,4409,4480,4329,4378,4429,4103,4385,4034,1481,252,222,150,164,152,149,163,254,160,253,255,221,161,159,147,148])).
% 60.87/61.66 cnf(4516,plain,
% 60.87/61.66 (P8(x45161,x45162,x45161,x45163,x45162,x45162,x45162,x45163)),
% 60.87/61.66 inference(scs_inference,[],[4343,4301,4315,4333,4359,4380,4396,4413,4309,4409,4480,4329,4378,4429,4103,4385,4034,1481,252,222,150,164,152,149,163,254,160,253,255,221,161,159,147,148,162,220])).
% 60.87/61.66 cnf(4518,plain,
% 60.87/61.66 (P8(x45181,x45182,x45181,x45181,x45183,x45182,x45183,x45181)),
% 60.87/61.66 inference(scs_inference,[],[4337,4343,4301,4315,4333,4359,4380,4396,4413,4309,4409,4480,4329,4378,4429,4103,4385,4034,1481,252,222,150,164,152,149,163,254,160,253,255,221,161,159,147,148,162,220,248])).
% 60.87/61.66 cnf(4520,plain,
% 60.87/61.66 (P8(x45201,x45202,x45203,x45202,x45201,x45203,x45203,x45203)),
% 60.87/61.66 inference(scs_inference,[],[4337,4343,4301,4315,4333,4359,4380,4396,4413,4309,4409,4480,4329,4378,4429,4103,4385,4034,1481,252,222,150,164,152,149,163,254,160,253,255,221,161,159,147,148,162,220,248,251])).
% 60.87/61.66 cnf(4522,plain,
% 60.87/61.66 (P3(x45221,x45222,x45221,x45223)),
% 60.87/61.66 inference(scs_inference,[],[4337,4343,4301,4315,4333,4359,4380,4396,4413,4309,4409,4480,4329,4378,4429,4103,4385,4034,1481,252,222,150,164,152,149,163,254,160,253,255,221,161,159,147,148,162,220,248,251,167])).
% 60.87/61.66 cnf(4526,plain,
% 60.87/61.66 (P3(x45261,x45261,x45262,x45263)),
% 60.87/61.66 inference(scs_inference,[],[4337,4343,4301,4315,4323,4333,4359,4380,4396,4413,4309,4409,4480,4329,4378,4429,4103,4385,4034,1481,252,222,150,164,152,149,163,254,160,253,255,221,161,159,147,148,162,220,248,251,167,249,166])).
% 60.87/61.66 cnf(4528,plain,
% 60.87/61.66 (P8(x45281,x45282,x45282,x45283,x45283,x45281,x45283,x45283)),
% 60.87/61.66 inference(scs_inference,[],[4337,4343,4301,4315,4323,4333,4359,4380,4396,4413,4309,4409,4480,4329,4378,4429,4103,4385,4034,1481,252,222,150,164,152,149,163,254,160,253,255,221,161,159,147,148,162,220,248,251,167,249,166,250])).
% 60.87/61.66 cnf(4536,plain,
% 60.87/61.66 (P3(x45361,x45362,x45362,x45363)),
% 60.87/61.66 inference(rename_variables,[],[4345])).
% 60.87/61.66 cnf(4540,plain,
% 60.87/61.66 (P4(x45401,x45401,x45402,x45402)),
% 60.87/61.66 inference(rename_variables,[],[4441])).
% 60.87/61.66 cnf(4547,plain,
% 60.87/61.66 (P10(a2,a1,a1,a1)),
% 60.87/61.66 inference(scs_inference,[],[4337,4441,4343,4345,4301,4315,4323,4292,4317,4333,4359,4380,4396,4413,4309,4409,4480,4329,4378,4429,4103,4385,4243,3619,4034,337,4236,3684,3843,3949,1481,252,222,150,164,152,149,163,254,160,253,255,221,161,159,147,148,162,220,248,251,167,249,166,250,243,184,108,187,190,246,200,177])).
% 60.87/61.66 cnf(4556,plain,
% 60.87/61.66 (P10(x45561,x45562,x45562,x45561)),
% 60.87/61.66 inference(rename_variables,[],[3971])).
% 60.87/61.66 cnf(4557,plain,
% 60.87/61.66 (P4(x45571,x45571,x45572,x45572)),
% 60.87/61.66 inference(rename_variables,[],[4441])).
% 60.87/61.66 cnf(4559,plain,
% 60.87/61.66 (P9(x45591,a2,x45591,a1)),
% 60.87/61.66 inference(scs_inference,[],[142,4337,4441,4540,4343,4345,4301,4315,4323,4292,4317,4333,4359,4380,4396,4413,4309,4409,4480,4329,4378,4429,4103,4385,4243,3619,4034,337,3971,4236,3803,3684,3843,3949,1481,252,222,150,164,152,149,163,254,160,253,255,221,161,159,147,148,162,220,248,251,167,249,166,250,243,184,108,187,190,246,200,177,242,193,172,196,236])).
% 60.87/61.66 cnf(4560,plain,
% 60.87/61.66 (P8(x45601,x45602,x45601,x45603,x45603,x45602,x45603,x45603)),
% 60.87/61.66 inference(rename_variables,[],[4337])).
% 60.87/61.66 cnf(4563,plain,
% 60.87/61.66 (P10(x45631,x45632,x45632,x45631)),
% 60.87/61.66 inference(rename_variables,[],[3971])).
% 60.87/61.66 cnf(4566,plain,
% 60.87/61.66 (P10(x45661,x45662,x45662,x45661)),
% 60.87/61.66 inference(rename_variables,[],[3971])).
% 60.87/61.66 cnf(4568,plain,
% 60.87/61.66 (P10(x45681,a2,x45681,a1)),
% 60.87/61.66 inference(scs_inference,[],[142,4337,4560,4441,4540,4343,4345,4301,4315,4323,4292,4317,4327,4333,4359,4380,4396,4413,4309,4409,4480,4329,4378,4429,4103,4385,4243,3619,4034,337,3971,4556,4563,4236,3803,3684,3843,3949,1481,252,222,150,164,152,149,163,254,160,253,255,221,161,159,147,148,162,220,248,251,167,249,166,250,243,184,108,187,190,246,200,177,242,193,172,196,236,173,174,237])).
% 60.87/61.66 cnf(4572,plain,
% 60.87/61.66 (P6(x45721,x45721,x45721)),
% 60.87/61.66 inference(rename_variables,[],[4243])).
% 60.87/61.66 cnf(4574,plain,
% 60.87/61.66 (P2(a1,a2,a2,a2)),
% 60.87/61.66 inference(scs_inference,[],[142,4337,4560,4441,4540,4343,4345,4301,4315,4323,4292,4317,4327,4333,4359,4380,4396,4413,4462,4309,4409,4480,4329,4378,4429,4103,4385,4243,3619,4034,337,3971,4556,4563,4236,3803,3684,3843,3949,1481,252,222,150,164,152,149,163,254,160,253,255,221,161,159,147,148,162,220,248,251,167,249,166,250,243,184,108,187,190,246,200,177,242,193,172,196,236,173,174,237,169,180])).
% 60.87/61.66 cnf(4579,plain,
% 60.87/61.66 (P10(x45791,x45792,x45792,x45791)),
% 60.87/61.66 inference(rename_variables,[],[3971])).
% 60.87/61.66 cnf(4580,plain,
% 60.87/61.66 (P4(x45801,x45801,x45802,x45802)),
% 60.87/61.66 inference(rename_variables,[],[4441])).
% 60.87/61.66 cnf(4582,plain,
% 60.87/61.66 (P7(f24(x45821,x45821,x45821,x45821,x45821,x45821),x45821,x45821,x45821,a3,a18,a18,a18)),
% 60.87/61.66 inference(scs_inference,[],[142,4337,4560,4441,4540,4557,4343,4345,4301,4315,4323,4292,4317,4327,4333,4359,4380,4396,4413,4462,4309,4409,4480,4329,4378,4429,4103,4385,4243,3619,4034,337,3971,4556,4563,4566,4236,3803,3684,3843,3949,1481,252,222,150,164,152,149,163,254,160,253,255,221,161,159,147,148,162,220,248,251,167,249,166,250,243,184,108,187,190,246,200,177,242,193,172,196,236,173,174,237,169,180,194,197,219])).
% 60.87/61.66 cnf(4587,plain,
% 60.87/61.66 (P10(x45871,x45872,x45872,x45871)),
% 60.87/61.66 inference(rename_variables,[],[3971])).
% 60.87/61.66 cnf(4590,plain,
% 60.87/61.66 (P10(x45901,x45902,x45902,x45901)),
% 60.87/61.66 inference(rename_variables,[],[3971])).
% 60.87/61.66 cnf(4591,plain,
% 60.87/61.66 (P4(x45911,x45911,x45912,x45912)),
% 60.87/61.66 inference(rename_variables,[],[4441])).
% 60.87/61.66 cnf(4613,plain,
% 60.87/61.66 (P6(a18,a18,a3)),
% 60.87/61.66 inference(scs_inference,[],[142,4337,4560,4441,4540,4557,4580,4591,4343,4345,4536,4301,4315,4323,4292,4317,4327,4333,4359,4380,4396,4413,4462,4309,4409,4480,4329,4378,4429,4103,4385,4391,4416,4156,4180,4200,4243,4572,3619,4034,337,3971,4556,4563,4566,4579,4587,4590,4057,3837,4236,3803,3684,3843,3603,3949,1481,252,222,150,164,152,149,163,254,160,253,255,221,161,159,147,148,162,220,248,251,167,249,166,250,243,184,108,187,190,246,200,177,242,193,172,196,236,173,174,237,169,180,194,197,219,201,186,195,185,223,199,178,238,191,188,158])).
% 60.87/61.66 cnf(4615,plain,
% 60.87/61.66 (P1(x46151,x46151,x46152)),
% 60.87/61.66 inference(rename_variables,[],[3837])).
% 60.87/61.66 cnf(4618,plain,
% 60.87/61.66 (P6(f24(x46181,x46181,x46181,x46181,x46181,x46181),x46181,x46181)),
% 60.87/61.66 inference(rename_variables,[],[4409])).
% 60.87/61.66 cnf(4627,plain,
% 60.87/61.66 (P6(f20(a3,a18),a18,a3)),
% 60.87/61.66 inference(scs_inference,[],[142,4337,4560,4441,4540,4557,4580,4591,4343,4345,4536,4301,4315,4323,4292,4317,4327,4333,4359,4380,4396,4413,4303,4462,4309,4409,4480,4618,4329,4378,4276,4429,4103,4385,4391,4416,4156,4180,4200,4243,4572,3619,4034,337,3971,4556,4563,4566,4579,4587,4590,3973,4057,3837,4615,4145,4236,3803,3684,3843,3603,3949,1481,252,222,150,164,152,149,163,254,160,253,255,221,161,159,147,148,162,220,248,251,167,249,166,250,243,184,108,187,190,246,200,177,242,193,172,196,236,173,174,237,169,180,194,197,219,201,186,195,185,223,199,178,238,191,188,158,182,224,247,1328])).
% 60.87/61.66 cnf(4631,plain,
% 60.87/61.66 (P1(x46311,a2,a1)),
% 60.87/61.66 inference(scs_inference,[],[142,4337,4560,4441,4540,4557,4580,4591,4343,4345,4536,4301,4315,4323,4292,4317,4327,4333,4359,4380,4396,4413,4303,4462,4309,4409,4480,4618,4329,4378,4276,4429,4103,4385,4391,4416,4156,4180,4200,4243,4572,3619,4034,337,3971,4556,4563,4566,4579,4587,4590,3973,4057,3837,4615,4145,4236,3803,3684,3843,3603,3949,1481,252,222,150,164,152,149,163,254,160,253,255,221,161,159,147,148,162,220,248,251,167,249,166,250,243,184,108,187,190,246,200,177,242,193,172,196,236,173,174,237,169,180,194,197,219,201,186,195,185,223,199,178,238,191,188,158,182,224,247,1328,156])).
% 60.87/61.66 cnf(4667,plain,
% 60.87/61.66 (P8(x46671,x46672,x46671,x46671,x46673,x46672,x46673,x46671)),
% 60.87/61.66 inference(rename_variables,[],[4518])).
% 60.87/61.66 cnf(4674,plain,
% 60.87/61.66 (P6(f7(x46741,x46741,x46741),x46741,x46741)),
% 60.87/61.66 inference(rename_variables,[],[4432])).
% 60.87/61.66 cnf(4722,plain,
% 60.87/61.66 (P10(x47221,x47222,x47222,x47221)),
% 60.87/61.66 inference(rename_variables,[],[3971])).
% 60.87/61.66 cnf(4725,plain,
% 60.87/61.66 (P3(x47251,x47252,x47251,x47253)),
% 60.87/61.66 inference(rename_variables,[],[4522])).
% 60.87/61.66 cnf(4728,plain,
% 60.87/61.66 (P10(x47281,a2,x47281,a1)),
% 60.87/61.66 inference(rename_variables,[],[4568])).
% 60.87/61.66 cnf(4729,plain,
% 60.87/61.66 (P3(x47291,x47292,x47291,x47293)),
% 60.87/61.66 inference(rename_variables,[],[4522])).
% 60.87/61.66 cnf(4739,plain,
% 60.87/61.66 (P10(x47391,x47392,x47392,x47391)),
% 60.87/61.66 inference(rename_variables,[],[3971])).
% 60.87/61.66 cnf(4742,plain,
% 60.87/61.66 (P10(x47421,x47422,x47421,x47422)),
% 60.87/61.66 inference(rename_variables,[],[3862])).
% 60.87/61.66 cnf(4745,plain,
% 60.87/61.66 (P10(x47451,a2,x47451,a1)),
% 60.87/61.66 inference(rename_variables,[],[4568])).
% 60.87/61.66 cnf(4748,plain,
% 60.87/61.66 (P4(x47481,x47481,x47482,x47482)),
% 60.87/61.66 inference(rename_variables,[],[4441])).
% 60.87/61.66 cnf(4749,plain,
% 60.87/61.66 (P10(x47491,a2,x47491,a1)),
% 60.87/61.66 inference(rename_variables,[],[4568])).
% 60.87/61.66 cnf(4754,plain,
% 60.87/61.66 (P8(x47541,x47542,x47543,x47542,x47541,x47543,x47543,x47543)),
% 60.87/61.66 inference(rename_variables,[],[4520])).
% 60.87/61.66 cnf(4759,plain,
% 60.87/61.66 (P10(x47591,x47592,x47592,x47591)),
% 60.87/61.66 inference(rename_variables,[],[3971])).
% 60.87/61.66 cnf(4767,plain,
% 60.87/61.66 (P4(x47671,x47671,x47672,x47672)),
% 60.87/61.66 inference(rename_variables,[],[4441])).
% 60.87/61.66 cnf(4768,plain,
% 60.87/61.66 (P10(x47681,a2,x47681,a1)),
% 60.87/61.66 inference(rename_variables,[],[4568])).
% 60.87/61.66 cnf(4771,plain,
% 60.87/61.66 (P10(x47711,a2,x47711,a1)),
% 60.87/61.66 inference(rename_variables,[],[4568])).
% 60.87/61.66 cnf(4776,plain,
% 60.87/61.66 (P4(x47761,x47761,x47762,x47762)),
% 60.87/61.66 inference(rename_variables,[],[4441])).
% 60.87/61.66 cnf(4780,plain,
% 60.87/61.66 (P6(f7(x47801,x47801,x47801),x47801,x47801)),
% 60.87/61.66 inference(rename_variables,[],[4432])).
% 60.87/61.66 cnf(4783,plain,
% 60.87/61.66 (P10(x47831,x47832,x47832,x47831)),
% 60.87/61.66 inference(rename_variables,[],[3971])).
% 60.87/61.66 cnf(4792,plain,
% 60.87/61.66 (P3(x47921,x47922,x47921,x47923)),
% 60.87/61.66 inference(rename_variables,[],[4522])).
% 60.87/61.66 cnf(4795,plain,
% 60.87/61.66 (P3(x47951,x47952,x47951,x47953)),
% 60.87/61.66 inference(rename_variables,[],[4522])).
% 60.87/61.66 cnf(4799,plain,
% 60.87/61.66 (P9(x47991,a2,x47991,a1)),
% 60.87/61.66 inference(rename_variables,[],[4559])).
% 60.87/61.66 cnf(4800,plain,
% 60.87/61.66 (P1(x48001,a2,a1)),
% 60.87/61.66 inference(rename_variables,[],[4631])).
% 60.87/61.66 cnf(4824,plain,
% 60.87/61.66 ($false),
% 60.87/61.66 inference(scs_inference,[],[142,4516,4518,4667,4520,4754,4528,4522,4725,4729,4792,4795,4526,3821,4097,4319,4488,4559,4799,4568,4728,4745,4749,4768,4771,4631,4800,4496,4506,4508,4547,4574,4613,4490,4361,4432,4674,4780,4512,4627,4582,3853,4441,4748,4767,4776,4345,4315,4202,3873,320,4243,3971,4722,4739,4759,4783,4396,3670,4145,3862,4742,3603,3601,3571,3949,3338,1235,222,252,1481,150,164,2,149,152,163,254,160,255,253,221,161,148,147,159,162,220,248,251,249,250,259,189,184,181,187,239,157,200,172,242,193,196,177,236,180,169,201,237,197,194,219,195,223,185,199,186,191,188,158,182,224,205,204,247,165]),
% 60.87/61.66 ['proof']).
% 60.87/61.66 % SZS output end Proof
% 60.87/61.66 % Total time :60.240000s
%------------------------------------------------------------------------------