%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : GEO603+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 : n024.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:53 EDT 2024
% Result : Theorem 63.71s 63.76s
% Output : CNFRefutation 63.71s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.04/0.12 % Problem : GEO603+1 : TPTP v8.2.0. Released v7.5.0.
% 0.04/0.12 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% 0.12/0.33 % Computer : n024.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 300
% 0.12/0.33 % DateTime : Fri Jun 21 08:23:08 EDT 2024
% 0.12/0.33 % CPUTime :
% 0.51/0.56 start to proof:theBenchmark
% 63.69/63.75 %-------------------------------------------
% 63.69/63.75 % File :CSE---1.7
% 63.69/63.75 % Problem :theBenchmark
% 63.69/63.75 % Transform :cnf
% 63.69/63.75 % Format :tptp:raw
% 63.69/63.75 % Command :java -jar mcs_scs.jar %d %s
% 63.69/63.75
% 63.69/63.75 % Result :Theorem 63.120000s
% 63.69/63.75 % Output :CNFRefutation 63.120000s
% 63.69/63.75 %-------------------------------------------
% 63.69/63.76 %------------------------------------------------------------------------------
% 63.69/63.76 % File : GEO603+1 : TPTP v8.2.0. Released v7.5.0.
% 63.69/63.76 % Domain : Geometry
% 63.69/63.76 % Problem : JGEX problem 65
% 63.69/63.76 % Version : [CGZ00] axioms.
% 63.69/63.76 % English :
% 63.69/63.76
% 63.69/63.76 % Refs : [CGZ00] Chou et al. (2000), A Deductive Database Approach to A
% 63.69/63.76 % : [YCG08] Ye et al. (2008), An Introduction to Java Geometry Exp
% 63.69/63.76 % : [Qua20] Quaresma (2020), Email to Geoff Sutcliffe
% 63.69/63.76 % Source : [Qua20]
% 63.69/63.76 % Names : 65.p [Qua20]
% 63.69/63.76
% 63.69/63.76 % Status : Theorem
% 63.69/63.76 % Rating : 0.28 v8.2.0, 0.31 v7.5.0
% 63.69/63.76 % Syntax : Number of formulae : 95 ( 0 unt; 0 def)
% 63.69/63.76 % Number of atoms : 289 ( 1 equ)
% 63.69/63.76 % Maximal formula atoms : 8 ( 3 avg)
% 63.69/63.76 % Number of connectives : 201 ( 7 ~; 0 |; 99 &)
% 63.69/63.76 % ( 0 <=>; 95 =>; 0 <=; 0 <~>)
% 63.69/63.76 % Maximal formula depth : 15 ( 9 avg)
% 63.71/63.76 % Maximal term depth : 1 ( 1 avg)
% 63.71/63.76 % Number of predicates : 12 ( 11 usr; 0 prp; 2-8 aty)
% 63.71/63.76 % Number of functors : 0 ( 0 usr; 0 con; --- aty)
% 63.71/63.76 % Number of variables : 529 ( 509 !; 20 ?)
% 63.71/63.76 % SPC : FOF_THM_RFO_SEQ
% 63.71/63.76
% 63.71/63.76 % Comments : Taken from JGEX [YCG08], converted by Pedro Quaresma.
% 63.71/63.76 %------------------------------------------------------------------------------
% 63.71/63.76 include('Axioms/GEO012+0.ax').
% 63.71/63.76 %------------------------------------------------------------------------------
% 63.71/63.76 fof(exemplo6GDDFULL618065,conjecture,
% 63.71/63.76 ! [A,B,C,D,E,F,G] :
% 63.71/63.76 ( ( circle(D,A,B,C)
% 63.71/63.76 & coll(E,A,B)
% 63.71/63.76 & para(B,C,F,E)
% 63.71/63.76 & coll(F,A,C)
% 63.71/63.76 & circle(G,A,E,F) )
% 63.71/63.76 => coll(A,G,D) ) ).
% 63.71/63.76
% 63.71/63.76 %------------------------------------------------------------------------------
% 63.71/63.76 %-------------------------------------------
% 63.71/63.76 % Proof found
% 63.71/63.76 % SZS status Theorem for theBenchmark
% 63.71/63.76 % SZS output start Proof
% 63.71/63.76 %ClaNum:260(EqnAxiom:141)
% 63.71/63.76 %VarNum:1613(SingletonVarNum:590)
% 63.71/63.76 %MaxLitNum:5
% 63.71/63.76 %MaxfuncDepth:1
% 63.71/63.76 %SharedTerms:13
% 63.71/63.76 %goalClause: 142 143 144 145 146 147
% 63.71/63.76 %singleGoalClaCount:6
% 63.71/63.76 [142]P1(a1,a2,a15)
% 63.71/63.76 [143]P1(a18,a2,a16)
% 63.71/63.76 [144]P3(a15,a16,a18,a1)
% 63.71/63.76 [145]P2(a17,a2,a15,a16)
% 63.71/63.76 [146]P2(a19,a2,a1,a18)
% 63.71/63.76 [147]~P1(a2,a19,a17)
% 63.71/63.76 [148]~P1(x1482,x1481,x1483)+P1(x1481,x1482,x1483)
% 63.71/63.76 [149]~P1(x1491,x1493,x1492)+P1(x1491,x1492,x1493)
% 63.71/63.76 [150]~P4(x1501,x1502,x1503)+P1(x1501,x1502,x1503)
% 63.71/63.76 [151]~P4(x1511,x1513,x1512)+P4(x1511,x1512,x1513)
% 63.71/63.76 [153]~P4(x1531,x1532,x1533)+P5(x1531,x1532,x1531,x1533)
% 63.71/63.76 [157]~P3(x1571,x1572,x1571,x1573)+P1(x1571,x1572,x1573)
% 63.71/63.76 [223]~P5(x2231,x2232,x2231,x2233)+P9(x2231,x2232,x2232,x2233,x2232,x2233,x2231,x2233)
% 63.71/63.76 [160]~P3(x1603,x1604,x1601,x1602)+P3(x1601,x1602,x1603,x1604)
% 63.71/63.76 [161]~P3(x1611,x1612,x1614,x1613)+P3(x1611,x1612,x1613,x1614)
% 63.71/63.76 [162]~P10(x1623,x1624,x1621,x1622)+P10(x1621,x1622,x1623,x1624)
% 63.71/63.76 [163]~P10(x1631,x1632,x1634,x1633)+P10(x1631,x1632,x1633,x1634)
% 63.71/63.76 [164]~P5(x1643,x1644,x1641,x1642)+P5(x1641,x1642,x1643,x1644)
% 63.71/63.76 [165]~P5(x1651,x1652,x1654,x1653)+P5(x1651,x1652,x1653,x1654)
% 63.71/63.76 [166]~P6(x1662,x1661,x1663,x1664)+P6(x1661,x1662,x1663,x1664)
% 63.71/63.76 [167]~P6(x1671,x1673,x1672,x1674)+P6(x1671,x1672,x1673,x1674)
% 63.71/63.76 [168]~P6(x1681,x1682,x1684,x1683)+P6(x1681,x1682,x1683,x1684)
% 63.71/63.76 [221]~P6(x2212,x2213,x2211,x2214)+P9(x2211,x2212,x2211,x2213,x2214,x2212,x2214,x2213)
% 63.71/63.76 [184]~P2(x1844,x1841,x1842,x1843)+P10(f7(x1841,x1842,x1843,x1844),x1841,x1841,x1844)
% 63.71/63.76 [199]P5(x1991,x1992,x1993,x1994)+~P7(x1991,x1992,x1995,x1993,x1994,x1996)
% 63.71/63.76 [211]~P11(x2114,x2115,x2116,x2111,x2112,x2113)+P11(x2111,x2112,x2113,x2114,x2115,x2116)
% 63.71/63.76 [212]~P11(x2122,x2121,x2123,x2125,x2124,x2126)+P11(x2121,x2122,x2123,x2124,x2125,x2126)
% 63.71/63.76 [213]~P11(x2131,x2133,x2132,x2134,x2136,x2135)+P11(x2131,x2132,x2133,x2134,x2135,x2136)
% 63.71/63.76 [214]~P7(x2144,x2145,x2146,x2141,x2142,x2143)+P7(x2141,x2142,x2143,x2144,x2145,x2146)
% 63.71/63.76 [215]~P7(x2152,x2151,x2153,x2155,x2154,x2156)+P7(x2151,x2152,x2153,x2154,x2155,x2156)
% 63.71/63.76 [216]~P7(x2161,x2163,x2162,x2164,x2166,x2165)+P7(x2161,x2162,x2163,x2164,x2165,x2166)
% 63.71/63.76 [222]~P3(x2221,x2222,x2225,x2226)+P9(x2221,x2222,x2223,x2224,x2225,x2226,x2223,x2224)
% 63.71/63.76 [228]~P11(x2281,x2282,x2283,x2284,x2285,x2286)+P9(x2281,x2282,x2282,x2283,x2284,x2285,x2285,x2286)
% 63.71/63.76 [229]~P11(x2291,x2292,x2293,x2294,x2295,x2296)+P8(x2291,x2292,x2291,x2293,x2294,x2295,x2294,x2296)
% 63.71/63.76 [230]~P9(x2301,x2302,x2305,x2306,x2303,x2304,x2305,x2306)+P3(x2301,x2302,x2303,x2304)
% 63.71/63.76 [249]~P9(x2495,x2496,x2497,x2498,x2491,x2492,x2493,x2494)+P9(x2491,x2492,x2493,x2494,x2495,x2496,x2497,x2498)
% 63.71/63.76 [250]~P9(x2503,x2504,x2501,x2502,x2507,x2508,x2505,x2506)+P9(x2501,x2502,x2503,x2504,x2505,x2506,x2507,x2508)
% 63.71/63.76 [251]~P9(x2512,x2511,x2513,x2514,x2515,x2516,x2517,x2518)+P9(x2511,x2512,x2513,x2514,x2515,x2516,x2517,x2518)
% 63.71/63.76 [252]~P9(x2521,x2522,x2525,x2526,x2523,x2524,x2527,x2528)+P9(x2521,x2522,x2523,x2524,x2525,x2526,x2527,x2528)
% 63.71/63.76 [253]~P8(x2535,x2536,x2537,x2538,x2531,x2532,x2533,x2534)+P8(x2531,x2532,x2533,x2534,x2535,x2536,x2537,x2538)
% 63.71/63.76 [254]~P8(x2543,x2544,x2541,x2542,x2547,x2548,x2545,x2546)+P8(x2541,x2542,x2543,x2544,x2545,x2546,x2547,x2548)
% 63.71/63.76 [255]~P8(x2552,x2551,x2553,x2554,x2555,x2556,x2557,x2558)+P8(x2551,x2552,x2553,x2554,x2555,x2556,x2557,x2558)
% 63.71/63.76 [256]~P8(x2561,x2562,x2565,x2566,x2563,x2564,x2567,x2568)+P8(x2561,x2562,x2563,x2564,x2565,x2566,x2567,x2568)
% 63.71/63.76 [158]~P1(x1581,x1582,x1583)+~P5(x1581,x1582,x1581,x1583)+P4(x1581,x1582,x1583)
% 63.71/63.76 [232]P5(x2321,x2322,x2321,x2323)+~P9(x2321,x2322,x2322,x2323,x2322,x2323,x2321,x2323)+P1(x2321,x2322,x2323)
% 63.71/63.76 [173]~P10(x1731,x1732,x1732,x1733)+~P5(x1732,x1731,x1732,x1733)+P1(x1731,x1732,f3(x1731,x1733,x1732))
% 63.71/63.76 [185]~P10(x1852,x1851,x1851,x1853)+~P5(x1851,x1852,x1851,x1853)+P5(x1851,x1852,x1851,f3(x1852,x1853,x1851))
% 63.71/63.76 [152]~P1(x1523,x1524,x1521)+P1(x1521,x1522,x1523)+~P1(x1523,x1524,x1522)
% 63.71/63.76 [169]~P2(x1694,x1691,x1692,x1693)+P10(x1691,x1692,x1692,x1693)+~P1(x1694,x1691,x1693)
% 63.71/63.76 [170]~P10(x1701,x1704,x1702,x1703)+P5(x1701,x1702,x1701,x1703)+~P4(x1704,x1702,x1703)
% 63.71/63.76 [171]~P10(x1711,x1713,x1713,x1714)+P5(x1711,x1712,x1713,x1712)+~P4(x1712,x1711,x1714)
% 63.71/63.76 [178]~P5(x1781,x1784,x1782,x1784)+~P5(x1781,x1783,x1782,x1783)+P10(x1781,x1782,x1783,x1784)
% 63.71/63.76 [181]~P5(x1811,x1812,x1811,x1814)+~P5(x1811,x1812,x1811,x1813)+P2(x1811,x1812,x1813,x1814)
% 63.71/63.76 [227]~P3(x2271,x2274,x2273,x2272)+~P6(x2271,x2274,x2273,x2272)+P9(x2271,x2272,x2273,x2272,x2273,x2272,x2273,x2274)
% 63.71/63.76 [231]~P9(x2311,x2313,x2311,x2314,x2312,x2313,x2312,x2314)+P1(x2311,x2312,x2313)+P6(x2313,x2314,x2311,x2312)
% 63.71/63.76 [233]~P1(x2333,x2334,x2332)+~P9(x2333,x2331,x2333,x2332,x2334,x2331,x2334,x2332)+P6(x2331,x2332,x2333,x2334)
% 63.71/63.76 [235]P10(x2351,x2352,x2353,x2354)+~P9(x2351,x2352,x2353,x2354,x2353,x2354,x2351,x2352)+P3(x2351,x2352,x2353,x2354)
% 63.71/63.76 [174]~P10(x1741,x1744,x1742,x1743)+~P10(x1742,x1744,x1741,x1743)+P1(f4(x1741,x1742,x1743),x1743,x1742)
% 63.71/63.76 [175]~P10(x1751,x1754,x1752,x1753)+~P10(x1752,x1754,x1751,x1753)+P1(f5(x1751,x1752,x1753),x1753,x1751)
% 63.71/63.76 [186]~P10(x1861,x1864,x1862,x1863)+~P10(x1862,x1864,x1861,x1863)+P10(x1861,f4(x1861,x1862,x1863),x1863,x1862)
% 63.71/63.76 [187]~P10(x1871,x1874,x1872,x1873)+~P10(x1872,x1874,x1871,x1873)+P10(x1871,f5(x1872,x1871,x1873),x1873,x1872)
% 63.71/63.76 [188]~P10(x1881,x1883,x1883,x1882)+~P6(x1881,x1882,x1883,x1884)+P2(f8(x1881,x1882,x1883),x1881,x1882,x1883)
% 63.71/63.76 [190]~P10(x1903,x1904,x1902,x1901)+~P5(x1903,x1902,x1903,x1901)+P1(x1901,x1902,f21(x1902,x1901,x1903,x1904))
% 63.71/63.76 [191]~P10(x1913,x1914,x1911,x1912)+~P5(x1913,x1911,x1913,x1912)+P1(f21(x1911,x1912,x1913,x1914),x1913,x1914)
% 63.71/63.76 [242]~P5(x2423,x2422,x2423,x2421)+~P9(x2422,x2423,x2423,x2424,x2423,x2424,x2423,x2421)+P1(x2421,x2422,f22(x2422,x2421,x2423,x2424))
% 63.71/63.76 [243]~P10(x2433,x2434,x2432,x2431)+~P9(x2432,x2433,x2433,x2434,x2433,x2434,x2433,x2431)+P1(x2431,x2432,f23(x2432,x2431,x2433,x2434))
% 63.71/63.76 [244]~P10(x2443,x2442,x2442,x2441)+~P9(x2444,x2443,x2442,x2443,x2442,x2443,x2441,x2443)+P1(f14(x2441,x2442,x2443,x2444),x2443,x2444)
% 63.71/63.76 [245]~P10(x2453,x2452,x2452,x2451)+~P9(x2454,x2453,x2452,x2453,x2452,x2453,x2451,x2453)+P1(f14(x2451,x2452,x2453,x2454),x2451,x2452)
% 63.71/63.76 [246]~P5(x2463,x2461,x2463,x2462)+~P9(x2461,x2463,x2463,x2464,x2463,x2464,x2463,x2462)+P1(f22(x2461,x2462,x2463,x2464),x2463,x2464)
% 63.71/63.76 [247]~P10(x2473,x2474,x2471,x2472)+~P9(x2471,x2473,x2473,x2474,x2473,x2474,x2473,x2472)+P1(f23(x2471,x2472,x2473,x2474),x2473,x2474)
% 63.71/63.76 [154]~P4(x1545,x1541,x1543)+P3(x1541,x1542,x1543,x1544)+~P4(x1545,x1542,x1544)
% 63.71/63.77 [155]~P4(x1551,x1555,x1553)+P3(x1551,x1552,x1553,x1554)+~P4(x1552,x1555,x1554)
% 63.71/63.77 [182]~P6(x1825,x1821,x1822,x1823)+P6(x1821,x1822,x1823,x1824)+~P6(x1825,x1821,x1822,x1824)
% 63.71/63.77 [224]~P4(x2245,x2242,x2243)+~P2(x2244,x2241,x2242,x2243)+P9(x2241,x2242,x2241,x2243,x2244,x2242,x2244,x2245)
% 63.71/63.77 [226]~P2(x2265,x2261,x2263,x2264)+P9(x2261,x2262,x2261,x2263,x2264,x2261,x2264,x2263)+~P10(x2265,x2261,x2261,x2262)
% 63.71/63.77 [239]~P9(x2392,x2393,x2392,x2394,x2395,x2392,x2395,x2394)+P10(x2391,x2392,x2392,x2393)+~P2(x2391,x2392,x2394,x2395)
% 63.71/63.77 [194]~P1(x1942,x1944,x1945)+~P10(x1941,x1943,x1943,x1942)+P1(f12(x1941,x1942,x1943,x1944,x1945),x1944,x1945)
% 63.71/63.77 [195]~P1(x1952,x1954,x1955)+~P10(x1951,x1953,x1953,x1952)+P10(f12(x1951,x1952,x1953,x1954,x1955),x1951,x1954,x1955)
% 63.71/63.77 [196]~P10(x1963,x1964,x1964,x1961)+~P5(x1961,x1962,x1961,x1965)+P5(x1961,x1962,x1961,f26(x1963,x1964,x1962,x1965,x1961))
% 63.71/63.77 [197]~P10(x1973,x1971,x1971,x1975)+~P5(x1975,x1972,x1975,x1974)+P5(x1971,x1972,x1971,f26(x1973,x1971,x1972,x1974,x1975))
% 63.71/63.77 [198]~P10(x1981,x1982,x1982,x1985)+~P5(x1985,x1983,x1985,x1984)+P3(f26(x1981,x1982,x1983,x1984,x1985),x1983,x1981,x1982)
% 63.71/63.77 [241]~P9(x2411,x2413,x2412,x2413,x2411,x2414,x2412,x2415)+P1(x2411,x2412,x2413)+P6(x2414,x2412,x2413,f25(x2411,x2412,x2413,x2414))
% 63.71/63.77 [257]~P9(x2571,x2573,x2572,x2573,x2571,x2574,x2572,x2575)+P1(x2571,x2572,x2573)+P9(x2571,x2573,x2572,x2573,x2571,f25(x2571,x2572,x2573,x2574),x2572,f25(x2571,x2572,x2573,x2574))
% 63.71/63.77 [176]~P3(x1761,x1762,x1765,x1766)+P3(x1761,x1762,x1763,x1764)+~P3(x1765,x1766,x1763,x1764)
% 63.71/63.77 [177]~P10(x1771,x1772,x1775,x1776)+P3(x1771,x1772,x1773,x1774)+~P10(x1775,x1776,x1773,x1774)
% 63.71/63.77 [179]~P10(x1795,x1796,x1793,x1794)+P10(x1791,x1792,x1793,x1794)+~P3(x1791,x1792,x1795,x1796)
% 63.71/63.77 [180]~P5(x1801,x1802,x1805,x1806)+P5(x1801,x1802,x1803,x1804)+~P5(x1805,x1806,x1803,x1804)
% 63.71/63.77 [217]~P5(x2171,x2172,x2174,x2175)+~P11(x2171,x2172,x2173,x2174,x2175,x2176)+P7(x2171,x2172,x2173,x2174,x2175,x2176)
% 63.71/63.77 [220]~P4(x2204,x2205,x2206)+~P4(x2201,x2202,x2203)+P8(x2201,x2202,x2202,x2203,x2204,x2205,x2205,x2206)
% 63.71/63.77 [200]~P4(x2006,x2003,x2004)+~P4(x2005,x2001,x2002)+P4(f24(x2001,x2002,x2003,x2004,x2005,x2006),x2001,x2004)
% 63.71/63.77 [201]~P4(x2016,x2013,x2014)+~P4(x2015,x2011,x2012)+P3(f24(x2011,x2012,x2013,x2014,x2015,x2016),x2016,x2011,x2013)
% 63.71/63.77 [202]~P4(x2026,x2023,x2024)+~P4(x2025,x2021,x2022)+P3(f24(x2021,x2022,x2023,x2024,x2025,x2026),x2025,x2022,x2024)
% 63.71/63.77 [237]~P9(x2371,x2372,x2373,x2374,x2375,x2376,x2377,x2378)+P3(x2371,x2372,x2373,x2374)+~P3(x2375,x2376,x2377,x2378)
% 63.71/63.77 [238]~P9(x2381,x2382,x2383,x2384,x2385,x2386,x2387,x2388)+P10(x2381,x2382,x2383,x2384)+~P10(x2385,x2386,x2387,x2388)
% 63.71/63.77 [240]~P8(x2401,x2402,x2403,x2404,x2405,x2406,x2407,x2408)+P5(x2401,x2402,x2403,x2404)+~P5(x2405,x2406,x2407,x2408)
% 63.71/63.77 [218]~P11(x2181,x2182,x2183,x2187,x2188,x2189)+P11(x2181,x2182,x2183,x2184,x2185,x2186)+~P11(x2187,x2188,x2189,x2184,x2185,x2186)
% 63.71/63.77 [219]~P7(x2191,x2192,x2193,x2197,x2198,x2199)+P7(x2191,x2192,x2193,x2194,x2195,x2196)+~P7(x2197,x2198,x2199,x2194,x2195,x2196)
% 63.71/63.77 [259]~P9(x2591,x2592,x2593,x2594,x2599,x25910,x25911,x25912)+P9(x2591,x2592,x2593,x2594,x2595,x2596,x2597,x2598)+~P9(x2599,x25910,x25911,x25912,x2595,x2596,x2597,x2598)
% 63.71/63.77 [260]~P8(x2601,x2602,x2603,x2604,x2609,x26010,x26011,x26012)+P8(x2601,x2602,x2603,x2604,x2605,x2606,x2607,x2608)+~P8(x2609,x26010,x26011,x26012,x2605,x2606,x2607,x2608)
% 63.71/63.77 [192]~P5(x1922,x1921,x1924,x1921)+~P6(x1922,x1924,x1921,x1923)+P10(x1921,x1922,x1922,x1923)+~P5(x1922,x1923,x1924,x1923)
% 63.71/63.77 [159]~P1(x1591,x1592,x1593)+~P3(x1594,x1591,x1595,x1593)+P4(x1591,x1592,x1593)+~P4(x1594,x1592,x1595)
% 63.71/63.77 [172]~P3(x1724,x1723,x1725,x1722)+~P3(x1724,x1722,x1725,x1723)+P4(x1721,x1722,x1723)+~P4(x1721,x1724,x1725)
% 63.71/63.77 [193]~P5(x1935,x1931,x1935,x1933)+~P5(x1935,x1931,x1935,x1932)+P6(x1931,x1932,x1933,x1934)+~P5(x1935,x1931,x1935,x1934)
% 63.71/63.77 [225]~P1(x2251,x2254,x2255)+~P1(x2251,x2252,x2253)+~P3(x2252,x2254,x2253,x2255)+P8(x2251,x2252,x2252,x2253,x2251,x2254,x2254,x2255)
% 63.71/63.77 [236]~P1(x2361,x2362,x2363)+~P9(x2365,x2362,x2365,x2363,x2364,x2362,x2364,x2361)+P4(x2361,x2362,x2363)+~P2(x2364,x2365,x2362,x2363)
% 63.71/63.77 [183]~P10(x1833,x1831,x1833,x1835)+~P10(x1831,x1832,x1831,x1833)+~P4(x1834,x1832,x1835)+P4(f6(x1831,x1832,x1833),x1831,x1833)
% 63.71/63.77 [189]~P6(x1891,x1892,x1893,x1895)+~P3(x1891,x1892,x1893,x1895)+~P4(x1894,x1891,x1892)+P2(f9(x1891,x1892,x1893),x1891,x1892,x1893)
% 63.71/63.77 [258]~P9(x2581,x2583,x2582,x2583,x2584,x2586,x2585,x2586)+~P9(x2581,x2582,x2582,x2583,x2584,x2585,x2585,x2586)+P1(x2581,x2582,x2583)+P11(x2581,x2582,x2583,x2584,x2585,x2586)
% 63.71/63.77 [248]~P6(x2481,x2482,x2485,x2484)+~P6(x2481,x2482,x2485,x2483)+~P9(x2485,x2481,x2485,x2482,x2486,x2483,x2486,x2484)+P5(x2481,x2482,x2483,x2484)+~P6(x2481,x2482,x2485,x2486)
% 63.71/63.77 [203]~P1(x2032,x2033,x2034)+~P1(x2031,x2034,x2036)+~P1(x2031,x2033,x2035)+~P3(x2033,x2034,x2035,x2036)+P1(x2031,x2032,f13(x2033,x2034,x2035,x2036,x2031,x2032))
% 63.71/63.77 [204]~P1(x2046,x2041,x2042)+~P1(x2045,x2042,x2044)+~P1(x2045,x2041,x2043)+~P3(x2041,x2042,x2043,x2044)+P1(f13(x2041,x2042,x2043,x2044,x2045,x2046),x2043,x2044)
% 63.71/63.77 [205]~P1(x2053,x2054,x2055)+~P4(x2056,x2051,x2052)+~P3(x2051,x2053,x2055,x2056)+~P3(x2051,x2053,x2052,x2054)+P1(f27(x2051,x2052,x2053,x2054,x2055,x2056),x2056,x2055)
% 63.71/63.77 [206]~P1(x2063,x2064,x2065)+~P4(x2066,x2061,x2062)+~P3(x2061,x2063,x2065,x2066)+~P3(x2061,x2063,x2062,x2064)+P1(f27(x2061,x2062,x2063,x2064,x2065,x2066),x2061,x2064)
% 63.71/63.77 [207]~P5(x2072,x2073,x2072,x2074)+~P5(x2071,x2073,x2071,x2076)+~P2(x2071,x2073,x2074,x2075)+E(x2071,x2072)+P1(f10(x2073,x2074,x2075,x2076,x2071,x2072),x2073,x2075)
% 63.71/63.77 [208]~P5(x2082,x2083,x2082,x2084)+~P5(x2081,x2083,x2081,x2086)+~P2(x2081,x2083,x2084,x2085)+E(x2081,x2082)+P1(f11(x2083,x2084,x2085,x2086,x2081,x2082),x2084,x2086)
% 63.71/63.77 [209]~P5(x2092,x2093,x2092,x2094)+~P5(x2091,x2093,x2091,x2096)+~P2(x2091,x2093,x2094,x2095)+E(x2091,x2092)+P5(f10(x2093,x2094,x2095,x2096,x2091,x2092),x2092,x2092,x2093)
% 63.71/63.77 [210]~P5(x2102,x2103,x2102,x2104)+~P5(x2101,x2103,x2101,x2106)+~P2(x2101,x2103,x2104,x2105)+E(x2101,x2102)+P5(f11(x2103,x2104,x2105,x2106,x2101,x2102),x2102,x2102,x2103)
% 63.71/63.77 [156]~P1(x1563,x1561,x1564)+~P1(x1565,x1561,x1564)+~P4(x1566,x1565,x1563)+~P4(x1567,x1561,x1564)+P4(f20(x1561,x1562),x1561,x1562)
% 63.71/63.77 %EqnAxiom
% 63.71/63.77 [1]E(x11,x11)
% 63.71/63.77 [2]E(x22,x21)+~E(x21,x22)
% 63.71/63.77 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 63.71/63.77 [4]~E(x41,x42)+E(f20(x41,x43),f20(x42,x43))
% 63.71/63.77 [5]~E(x51,x52)+E(f20(x53,x51),f20(x53,x52))
% 63.71/63.77 [6]~E(x61,x62)+E(f3(x61,x63,x64),f3(x62,x63,x64))
% 63.71/63.77 [7]~E(x71,x72)+E(f3(x73,x71,x74),f3(x73,x72,x74))
% 63.71/63.77 [8]~E(x81,x82)+E(f3(x83,x84,x81),f3(x83,x84,x82))
% 63.71/63.77 [9]~E(x91,x92)+E(f4(x91,x93,x94),f4(x92,x93,x94))
% 63.71/63.77 [10]~E(x101,x102)+E(f4(x103,x101,x104),f4(x103,x102,x104))
% 63.71/63.77 [11]~E(x111,x112)+E(f4(x113,x114,x111),f4(x113,x114,x112))
% 63.71/63.77 [12]~E(x121,x122)+E(f5(x121,x123,x124),f5(x122,x123,x124))
% 63.71/63.77 [13]~E(x131,x132)+E(f5(x133,x131,x134),f5(x133,x132,x134))
% 63.71/63.77 [14]~E(x141,x142)+E(f5(x143,x144,x141),f5(x143,x144,x142))
% 63.71/63.77 [15]~E(x151,x152)+E(f6(x151,x153,x154),f6(x152,x153,x154))
% 63.71/63.77 [16]~E(x161,x162)+E(f6(x163,x161,x164),f6(x163,x162,x164))
% 63.71/63.77 [17]~E(x171,x172)+E(f6(x173,x174,x171),f6(x173,x174,x172))
% 63.71/63.77 [18]~E(x181,x182)+E(f7(x181,x183,x184,x185),f7(x182,x183,x184,x185))
% 63.71/63.77 [19]~E(x191,x192)+E(f7(x193,x191,x194,x195),f7(x193,x192,x194,x195))
% 63.71/63.77 [20]~E(x201,x202)+E(f7(x203,x204,x201,x205),f7(x203,x204,x202,x205))
% 63.71/63.77 [21]~E(x211,x212)+E(f7(x213,x214,x215,x211),f7(x213,x214,x215,x212))
% 63.71/63.77 [22]~E(x221,x222)+E(f25(x221,x223,x224,x225),f25(x222,x223,x224,x225))
% 63.71/63.77 [23]~E(x231,x232)+E(f25(x233,x231,x234,x235),f25(x233,x232,x234,x235))
% 63.71/63.77 [24]~E(x241,x242)+E(f25(x243,x244,x241,x245),f25(x243,x244,x242,x245))
% 63.71/63.77 [25]~E(x251,x252)+E(f25(x253,x254,x255,x251),f25(x253,x254,x255,x252))
% 63.71/63.77 [26]~E(x261,x262)+E(f22(x261,x263,x264,x265),f22(x262,x263,x264,x265))
% 63.71/63.77 [27]~E(x271,x272)+E(f22(x273,x271,x274,x275),f22(x273,x272,x274,x275))
% 63.71/63.77 [28]~E(x281,x282)+E(f22(x283,x284,x281,x285),f22(x283,x284,x282,x285))
% 63.71/63.77 [29]~E(x291,x292)+E(f22(x293,x294,x295,x291),f22(x293,x294,x295,x292))
% 63.71/63.77 [30]~E(x301,x302)+E(f23(x301,x303,x304,x305),f23(x302,x303,x304,x305))
% 63.71/63.77 [31]~E(x311,x312)+E(f23(x313,x311,x314,x315),f23(x313,x312,x314,x315))
% 63.71/63.77 [32]~E(x321,x322)+E(f23(x323,x324,x321,x325),f23(x323,x324,x322,x325))
% 63.71/63.77 [33]~E(x331,x332)+E(f23(x333,x334,x335,x331),f23(x333,x334,x335,x332))
% 63.71/63.77 [34]~E(x341,x342)+E(f8(x341,x343,x344),f8(x342,x343,x344))
% 63.71/63.77 [35]~E(x351,x352)+E(f8(x353,x351,x354),f8(x353,x352,x354))
% 63.71/63.77 [36]~E(x361,x362)+E(f8(x363,x364,x361),f8(x363,x364,x362))
% 63.71/63.77 [37]~E(x371,x372)+E(f9(x371,x373,x374),f9(x372,x373,x374))
% 63.71/63.77 [38]~E(x381,x382)+E(f9(x383,x381,x384),f9(x383,x382,x384))
% 63.71/63.77 [39]~E(x391,x392)+E(f9(x393,x394,x391),f9(x393,x394,x392))
% 63.71/63.77 [40]~E(x401,x402)+E(f21(x401,x403,x404,x405),f21(x402,x403,x404,x405))
% 63.71/63.77 [41]~E(x411,x412)+E(f21(x413,x411,x414,x415),f21(x413,x412,x414,x415))
% 63.71/63.77 [42]~E(x421,x422)+E(f21(x423,x424,x421,x425),f21(x423,x424,x422,x425))
% 63.71/63.77 [43]~E(x431,x432)+E(f21(x433,x434,x435,x431),f21(x433,x434,x435,x432))
% 63.71/63.77 [44]~E(x441,x442)+E(f14(x441,x443,x444,x445),f14(x442,x443,x444,x445))
% 63.71/63.77 [45]~E(x451,x452)+E(f14(x453,x451,x454,x455),f14(x453,x452,x454,x455))
% 63.71/63.77 [46]~E(x461,x462)+E(f14(x463,x464,x461,x465),f14(x463,x464,x462,x465))
% 63.71/63.77 [47]~E(x471,x472)+E(f14(x473,x474,x475,x471),f14(x473,x474,x475,x472))
% 63.71/63.77 [48]~E(x481,x482)+E(f12(x481,x483,x484,x485,x486),f12(x482,x483,x484,x485,x486))
% 63.71/63.77 [49]~E(x491,x492)+E(f12(x493,x491,x494,x495,x496),f12(x493,x492,x494,x495,x496))
% 63.71/63.77 [50]~E(x501,x502)+E(f12(x503,x504,x501,x505,x506),f12(x503,x504,x502,x505,x506))
% 63.71/63.77 [51]~E(x511,x512)+E(f12(x513,x514,x515,x511,x516),f12(x513,x514,x515,x512,x516))
% 63.71/63.77 [52]~E(x521,x522)+E(f12(x523,x524,x525,x526,x521),f12(x523,x524,x525,x526,x522))
% 63.71/63.77 [53]~E(x531,x532)+E(f11(x531,x533,x534,x535,x536,x537),f11(x532,x533,x534,x535,x536,x537))
% 63.71/63.77 [54]~E(x541,x542)+E(f11(x543,x541,x544,x545,x546,x547),f11(x543,x542,x544,x545,x546,x547))
% 63.71/63.77 [55]~E(x551,x552)+E(f11(x553,x554,x551,x555,x556,x557),f11(x553,x554,x552,x555,x556,x557))
% 63.71/63.77 [56]~E(x561,x562)+E(f11(x563,x564,x565,x561,x566,x567),f11(x563,x564,x565,x562,x566,x567))
% 63.71/63.77 [57]~E(x571,x572)+E(f11(x573,x574,x575,x576,x571,x577),f11(x573,x574,x575,x576,x572,x577))
% 63.71/63.77 [58]~E(x581,x582)+E(f11(x583,x584,x585,x586,x587,x581),f11(x583,x584,x585,x586,x587,x582))
% 63.71/63.77 [59]~E(x591,x592)+E(f26(x591,x593,x594,x595,x596),f26(x592,x593,x594,x595,x596))
% 63.71/63.77 [60]~E(x601,x602)+E(f26(x603,x601,x604,x605,x606),f26(x603,x602,x604,x605,x606))
% 63.71/63.77 [61]~E(x611,x612)+E(f26(x613,x614,x611,x615,x616),f26(x613,x614,x612,x615,x616))
% 63.71/63.77 [62]~E(x621,x622)+E(f26(x623,x624,x625,x621,x626),f26(x623,x624,x625,x622,x626))
% 63.71/63.77 [63]~E(x631,x632)+E(f26(x633,x634,x635,x636,x631),f26(x633,x634,x635,x636,x632))
% 63.71/63.77 [64]~E(x641,x642)+E(f10(x641,x643,x644,x645,x646,x647),f10(x642,x643,x644,x645,x646,x647))
% 63.71/63.77 [65]~E(x651,x652)+E(f10(x653,x651,x654,x655,x656,x657),f10(x653,x652,x654,x655,x656,x657))
% 63.71/63.77 [66]~E(x661,x662)+E(f10(x663,x664,x661,x665,x666,x667),f10(x663,x664,x662,x665,x666,x667))
% 63.71/63.77 [67]~E(x671,x672)+E(f10(x673,x674,x675,x671,x676,x677),f10(x673,x674,x675,x672,x676,x677))
% 63.71/63.77 [68]~E(x681,x682)+E(f10(x683,x684,x685,x686,x681,x687),f10(x683,x684,x685,x686,x682,x687))
% 63.71/63.77 [69]~E(x691,x692)+E(f10(x693,x694,x695,x696,x697,x691),f10(x693,x694,x695,x696,x697,x692))
% 63.71/63.77 [70]~E(x701,x702)+E(f27(x701,x703,x704,x705,x706,x707),f27(x702,x703,x704,x705,x706,x707))
% 63.71/63.77 [71]~E(x711,x712)+E(f27(x713,x711,x714,x715,x716,x717),f27(x713,x712,x714,x715,x716,x717))
% 63.71/63.77 [72]~E(x721,x722)+E(f27(x723,x724,x721,x725,x726,x727),f27(x723,x724,x722,x725,x726,x727))
% 63.71/63.77 [73]~E(x731,x732)+E(f27(x733,x734,x735,x731,x736,x737),f27(x733,x734,x735,x732,x736,x737))
% 63.71/63.77 [74]~E(x741,x742)+E(f27(x743,x744,x745,x746,x741,x747),f27(x743,x744,x745,x746,x742,x747))
% 63.71/63.77 [75]~E(x751,x752)+E(f27(x753,x754,x755,x756,x757,x751),f27(x753,x754,x755,x756,x757,x752))
% 63.71/63.77 [76]~E(x761,x762)+E(f24(x761,x763,x764,x765,x766,x767),f24(x762,x763,x764,x765,x766,x767))
% 63.71/63.77 [77]~E(x771,x772)+E(f24(x773,x771,x774,x775,x776,x777),f24(x773,x772,x774,x775,x776,x777))
% 63.71/63.77 [78]~E(x781,x782)+E(f24(x783,x784,x781,x785,x786,x787),f24(x783,x784,x782,x785,x786,x787))
% 63.71/63.77 [79]~E(x791,x792)+E(f24(x793,x794,x795,x791,x796,x797),f24(x793,x794,x795,x792,x796,x797))
% 63.71/63.77 [80]~E(x801,x802)+E(f24(x803,x804,x805,x806,x801,x807),f24(x803,x804,x805,x806,x802,x807))
% 63.71/63.77 [81]~E(x811,x812)+E(f24(x813,x814,x815,x816,x817,x811),f24(x813,x814,x815,x816,x817,x812))
% 63.71/63.77 [82]~E(x821,x822)+E(f13(x821,x823,x824,x825,x826,x827),f13(x822,x823,x824,x825,x826,x827))
% 63.71/63.77 [83]~E(x831,x832)+E(f13(x833,x831,x834,x835,x836,x837),f13(x833,x832,x834,x835,x836,x837))
% 63.71/63.77 [84]~E(x841,x842)+E(f13(x843,x844,x841,x845,x846,x847),f13(x843,x844,x842,x845,x846,x847))
% 63.71/63.77 [85]~E(x851,x852)+E(f13(x853,x854,x855,x851,x856,x857),f13(x853,x854,x855,x852,x856,x857))
% 63.71/63.77 [86]~E(x861,x862)+E(f13(x863,x864,x865,x866,x861,x867),f13(x863,x864,x865,x866,x862,x867))
% 63.71/63.77 [87]~E(x871,x872)+E(f13(x873,x874,x875,x876,x877,x871),f13(x873,x874,x875,x876,x877,x872))
% 63.71/63.77 [88]P1(x882,x883,x884)+~E(x881,x882)+~P1(x881,x883,x884)
% 63.71/63.77 [89]P1(x893,x892,x894)+~E(x891,x892)+~P1(x893,x891,x894)
% 63.71/63.77 [90]P1(x903,x904,x902)+~E(x901,x902)+~P1(x903,x904,x901)
% 63.71/63.77 [91]P8(x912,x913,x914,x915,x916,x917,x918,x919)+~E(x911,x912)+~P8(x911,x913,x914,x915,x916,x917,x918,x919)
% 63.71/63.77 [92]P8(x923,x922,x924,x925,x926,x927,x928,x929)+~E(x921,x922)+~P8(x923,x921,x924,x925,x926,x927,x928,x929)
% 63.71/63.77 [93]P8(x933,x934,x932,x935,x936,x937,x938,x939)+~E(x931,x932)+~P8(x933,x934,x931,x935,x936,x937,x938,x939)
% 63.71/63.77 [94]P8(x943,x944,x945,x942,x946,x947,x948,x949)+~E(x941,x942)+~P8(x943,x944,x945,x941,x946,x947,x948,x949)
% 63.71/63.77 [95]P8(x953,x954,x955,x956,x952,x957,x958,x959)+~E(x951,x952)+~P8(x953,x954,x955,x956,x951,x957,x958,x959)
% 63.71/63.77 [96]P8(x963,x964,x965,x966,x967,x962,x968,x969)+~E(x961,x962)+~P8(x963,x964,x965,x966,x967,x961,x968,x969)
% 63.71/63.77 [97]P8(x973,x974,x975,x976,x977,x978,x972,x979)+~E(x971,x972)+~P8(x973,x974,x975,x976,x977,x978,x971,x979)
% 63.71/63.77 [98]P8(x983,x984,x985,x986,x987,x988,x989,x982)+~E(x981,x982)+~P8(x983,x984,x985,x986,x987,x988,x989,x981)
% 63.71/63.77 [99]P3(x992,x993,x994,x995)+~E(x991,x992)+~P3(x991,x993,x994,x995)
% 63.71/63.77 [100]P3(x1003,x1002,x1004,x1005)+~E(x1001,x1002)+~P3(x1003,x1001,x1004,x1005)
% 63.71/63.77 [101]P3(x1013,x1014,x1012,x1015)+~E(x1011,x1012)+~P3(x1013,x1014,x1011,x1015)
% 63.71/63.77 [102]P3(x1023,x1024,x1025,x1022)+~E(x1021,x1022)+~P3(x1023,x1024,x1025,x1021)
% 63.71/63.77 [103]P2(x1032,x1033,x1034,x1035)+~E(x1031,x1032)+~P2(x1031,x1033,x1034,x1035)
% 63.71/63.77 [104]P2(x1043,x1042,x1044,x1045)+~E(x1041,x1042)+~P2(x1043,x1041,x1044,x1045)
% 63.71/63.77 [105]P2(x1053,x1054,x1052,x1055)+~E(x1051,x1052)+~P2(x1053,x1054,x1051,x1055)
% 63.71/63.77 [106]P2(x1063,x1064,x1065,x1062)+~E(x1061,x1062)+~P2(x1063,x1064,x1065,x1061)
% 63.71/63.77 [107]P9(x1072,x1073,x1074,x1075,x1076,x1077,x1078,x1079)+~E(x1071,x1072)+~P9(x1071,x1073,x1074,x1075,x1076,x1077,x1078,x1079)
% 63.71/63.77 [108]P9(x1083,x1082,x1084,x1085,x1086,x1087,x1088,x1089)+~E(x1081,x1082)+~P9(x1083,x1081,x1084,x1085,x1086,x1087,x1088,x1089)
% 63.71/63.77 [109]P9(x1093,x1094,x1092,x1095,x1096,x1097,x1098,x1099)+~E(x1091,x1092)+~P9(x1093,x1094,x1091,x1095,x1096,x1097,x1098,x1099)
% 63.71/63.77 [110]P9(x1103,x1104,x1105,x1102,x1106,x1107,x1108,x1109)+~E(x1101,x1102)+~P9(x1103,x1104,x1105,x1101,x1106,x1107,x1108,x1109)
% 63.71/63.77 [111]P9(x1113,x1114,x1115,x1116,x1112,x1117,x1118,x1119)+~E(x1111,x1112)+~P9(x1113,x1114,x1115,x1116,x1111,x1117,x1118,x1119)
% 63.71/63.77 [112]P9(x1123,x1124,x1125,x1126,x1127,x1122,x1128,x1129)+~E(x1121,x1122)+~P9(x1123,x1124,x1125,x1126,x1127,x1121,x1128,x1129)
% 63.71/63.77 [113]P9(x1133,x1134,x1135,x1136,x1137,x1138,x1132,x1139)+~E(x1131,x1132)+~P9(x1133,x1134,x1135,x1136,x1137,x1138,x1131,x1139)
% 63.71/63.77 [114]P9(x1143,x1144,x1145,x1146,x1147,x1148,x1149,x1142)+~E(x1141,x1142)+~P9(x1143,x1144,x1145,x1146,x1147,x1148,x1149,x1141)
% 63.71/63.77 [115]P6(x1152,x1153,x1154,x1155)+~E(x1151,x1152)+~P6(x1151,x1153,x1154,x1155)
% 63.71/63.77 [116]P6(x1163,x1162,x1164,x1165)+~E(x1161,x1162)+~P6(x1163,x1161,x1164,x1165)
% 63.71/63.77 [117]P6(x1173,x1174,x1172,x1175)+~E(x1171,x1172)+~P6(x1173,x1174,x1171,x1175)
% 63.71/63.77 [118]P6(x1183,x1184,x1185,x1182)+~E(x1181,x1182)+~P6(x1183,x1184,x1185,x1181)
% 63.71/63.77 [119]P7(x1192,x1193,x1194,x1195,x1196,x1197)+~E(x1191,x1192)+~P7(x1191,x1193,x1194,x1195,x1196,x1197)
% 63.71/63.77 [120]P7(x1203,x1202,x1204,x1205,x1206,x1207)+~E(x1201,x1202)+~P7(x1203,x1201,x1204,x1205,x1206,x1207)
% 63.71/63.77 [121]P7(x1213,x1214,x1212,x1215,x1216,x1217)+~E(x1211,x1212)+~P7(x1213,x1214,x1211,x1215,x1216,x1217)
% 63.71/63.77 [122]P7(x1223,x1224,x1225,x1222,x1226,x1227)+~E(x1221,x1222)+~P7(x1223,x1224,x1225,x1221,x1226,x1227)
% 63.71/63.77 [123]P7(x1233,x1234,x1235,x1236,x1232,x1237)+~E(x1231,x1232)+~P7(x1233,x1234,x1235,x1236,x1231,x1237)
% 63.71/63.77 [124]P7(x1243,x1244,x1245,x1246,x1247,x1242)+~E(x1241,x1242)+~P7(x1243,x1244,x1245,x1246,x1247,x1241)
% 63.71/63.77 [125]P11(x1252,x1253,x1254,x1255,x1256,x1257)+~E(x1251,x1252)+~P11(x1251,x1253,x1254,x1255,x1256,x1257)
% 63.71/63.77 [126]P11(x1263,x1262,x1264,x1265,x1266,x1267)+~E(x1261,x1262)+~P11(x1263,x1261,x1264,x1265,x1266,x1267)
% 63.71/63.77 [127]P11(x1273,x1274,x1272,x1275,x1276,x1277)+~E(x1271,x1272)+~P11(x1273,x1274,x1271,x1275,x1276,x1277)
% 63.71/63.77 [128]P11(x1283,x1284,x1285,x1282,x1286,x1287)+~E(x1281,x1282)+~P11(x1283,x1284,x1285,x1281,x1286,x1287)
% 63.71/63.77 [129]P11(x1293,x1294,x1295,x1296,x1292,x1297)+~E(x1291,x1292)+~P11(x1293,x1294,x1295,x1296,x1291,x1297)
% 63.71/63.77 [130]P11(x1303,x1304,x1305,x1306,x1307,x1302)+~E(x1301,x1302)+~P11(x1303,x1304,x1305,x1306,x1307,x1301)
% 63.71/63.77 [131]P4(x1312,x1313,x1314)+~E(x1311,x1312)+~P4(x1311,x1313,x1314)
% 63.71/63.77 [132]P4(x1323,x1322,x1324)+~E(x1321,x1322)+~P4(x1323,x1321,x1324)
% 63.71/63.77 [133]P4(x1333,x1334,x1332)+~E(x1331,x1332)+~P4(x1333,x1334,x1331)
% 63.71/63.77 [134]P10(x1342,x1343,x1344,x1345)+~E(x1341,x1342)+~P10(x1341,x1343,x1344,x1345)
% 63.71/63.77 [135]P10(x1353,x1352,x1354,x1355)+~E(x1351,x1352)+~P10(x1353,x1351,x1354,x1355)
% 63.71/63.77 [136]P10(x1363,x1364,x1362,x1365)+~E(x1361,x1362)+~P10(x1363,x1364,x1361,x1365)
% 63.71/63.77 [137]P10(x1373,x1374,x1375,x1372)+~E(x1371,x1372)+~P10(x1373,x1374,x1375,x1371)
% 63.71/63.77 [138]P5(x1382,x1383,x1384,x1385)+~E(x1381,x1382)+~P5(x1381,x1383,x1384,x1385)
% 63.71/63.77 [139]P5(x1393,x1392,x1394,x1395)+~E(x1391,x1392)+~P5(x1393,x1391,x1394,x1395)
% 63.71/63.77 [140]P5(x1403,x1404,x1402,x1405)+~E(x1401,x1402)+~P5(x1403,x1404,x1401,x1405)
% 63.71/63.77 [141]P5(x1413,x1414,x1415,x1412)+~E(x1411,x1412)+~P5(x1413,x1414,x1415,x1411)
% 63.71/63.77
% 63.71/63.77 %-------------------------------------------
% 63.71/63.78 cnf(261,plain,
% 63.71/63.78 (~P1(a19,a2,a17)),
% 63.71/63.78 inference(scs_inference,[],[147,148])).
% 63.71/63.78 cnf(263,plain,
% 63.71/63.78 (~P1(a2,a17,a19)),
% 63.71/63.78 inference(scs_inference,[],[147,148,149])).
% 63.71/63.78 cnf(267,plain,
% 63.71/63.78 (~P3(a2,a19,a2,a17)),
% 63.71/63.78 inference(scs_inference,[],[147,148,149,150,157])).
% 63.71/63.78 cnf(269,plain,
% 63.71/63.78 (~P3(a2,a17,a2,a19)),
% 63.71/63.78 inference(scs_inference,[],[147,148,149,150,157,160])).
% 63.71/63.78 cnf(271,plain,
% 63.71/63.78 (~P3(a2,a19,a17,a2)),
% 63.71/63.78 inference(scs_inference,[],[147,148,149,150,157,160,161])).
% 63.71/63.78 cnf(279,plain,
% 63.71/63.78 (~P9(x2791,x2792,a2,a19,x2791,x2792,a2,a17)),
% 63.71/63.78 inference(scs_inference,[],[147,148,149,150,157,160,161,151,230,249,250])).
% 63.71/63.78 cnf(281,plain,
% 63.71/63.78 (~P9(a19,a2,x2811,x2812,a2,a17,x2811,x2812)),
% 63.71/63.78 inference(scs_inference,[],[147,148,149,150,157,160,161,151,230,249,250,251])).
% 63.71/63.78 cnf(283,plain,
% 63.71/63.78 (~P9(a2,a19,a2,a17,x2831,x2832,x2831,x2832)),
% 63.71/63.78 inference(scs_inference,[],[147,148,149,150,157,160,161,151,230,249,250,251,252])).
% 63.71/63.78 cnf(285,plain,
% 63.71/63.78 (P1(a15,a15,a1)),
% 63.71/63.78 inference(scs_inference,[],[142,147,148,149,150,157,160,161,151,230,249,250,251,252,152])).
% 63.71/63.78 cnf(287,plain,
% 63.71/63.78 (~P9(a2,a19,a2,a17,a15,a16,a18,a1)),
% 63.71/63.78 inference(scs_inference,[],[142,144,147,148,149,150,157,160,161,151,230,249,250,251,252,152,237])).
% 63.71/63.78 cnf(289,plain,
% 63.71/63.78 (~P3(a19,a2,a2,a17)),
% 63.71/63.78 inference(scs_inference,[],[142,144,147,148,149,150,157,160,161,151,230,249,250,251,252,152,237,222])).
% 63.71/63.78 cnf(293,plain,
% 63.71/63.78 (~P3(x2931,x2932,a15,a16)+P3(x2931,x2932,a18,a1)),
% 63.71/63.78 inference(scs_inference,[],[142,144,147,148,149,150,157,160,161,151,230,249,250,251,252,152,237,222,228,176])).
% 63.71/63.78 cnf(295,plain,
% 63.71/63.78 (~P11(x2951,a2,a17,x2951,a2,a19)),
% 63.71/63.78 inference(scs_inference,[],[142,144,147,148,149,150,157,160,161,151,230,249,250,251,252,152,237,222,228,176,211])).
% 63.71/63.78 cnf(297,plain,
% 63.71/63.78 (~P11(a2,x2971,a19,a2,x2971,a17)),
% 63.71/63.78 inference(scs_inference,[],[142,144,147,148,149,150,157,160,161,151,230,249,250,251,252,152,237,222,228,176,211,212])).
% 63.71/63.78 cnf(299,plain,
% 63.71/63.78 (~P11(x2991,a19,a2,x2991,a17,a2)),
% 63.71/63.78 inference(scs_inference,[],[142,144,147,148,149,150,157,160,161,151,230,249,250,251,252,152,237,222,228,176,211,212,213])).
% 63.71/63.78 cnf(311,plain,
% 63.71/63.78 (~P9(a2,a17,a2,a19,a18,a1,a15,a16)),
% 63.71/63.78 inference(scs_inference,[],[287,250])).
% 63.71/63.78 cnf(313,plain,
% 63.71/63.78 (~P3(a2,a17,a19,a2)),
% 63.71/63.78 inference(scs_inference,[],[269,287,250,161])).
% 63.71/63.78 cnf(315,plain,
% 63.71/63.78 (~P1(a17,a2,a19)),
% 63.71/63.78 inference(scs_inference,[],[269,263,287,250,161,148])).
% 63.71/63.78 cnf(317,plain,
% 63.71/63.78 (~P9(a2,a19,x3171,x3172,a17,a2,x3171,x3172)),
% 63.71/63.78 inference(scs_inference,[],[269,263,271,287,250,161,148,230])).
% 63.71/63.78 cnf(327,plain,
% 63.71/63.78 (~P9(a19,a2,a2,a17,a15,a16,a18,a1)),
% 63.71/63.78 inference(scs_inference,[],[261,269,263,271,287,295,250,161,148,230,213,212,150,151,251])).
% 63.71/63.78 cnf(329,plain,
% 63.71/63.78 (~P9(a15,a16,a18,a1,a2,a19,a2,a17)),
% 63.71/63.78 inference(scs_inference,[],[261,269,263,271,287,295,250,161,148,230,213,212,150,151,251,249])).
% 63.71/63.78 cnf(331,plain,
% 63.71/63.78 (~P3(a19,a2,a19,a17)),
% 63.71/63.78 inference(scs_inference,[],[261,269,263,271,287,295,250,161,148,230,213,212,150,151,251,249,157])).
% 63.71/63.78 cnf(333,plain,
% 63.71/63.78 (~P9(a2,a19,a15,a16,a2,a17,a18,a1)),
% 63.71/63.78 inference(scs_inference,[],[261,269,263,271,287,295,250,161,148,230,213,212,150,151,251,249,157,252])).
% 63.71/63.78 cnf(335,plain,
% 63.71/63.78 (~P1(a19,a17,a2)),
% 63.71/63.78 inference(scs_inference,[],[261,269,263,271,287,295,250,161,148,230,213,212,150,151,251,249,157,252,149])).
% 63.71/63.78 cnf(337,plain,
% 63.71/63.78 (~P3(a17,a2,a2,a19)),
% 63.71/63.78 inference(scs_inference,[],[261,269,263,271,287,295,250,161,148,230,213,212,150,151,251,249,157,252,149,160])).
% 63.71/63.78 cnf(339,plain,
% 63.71/63.78 (P1(a16,a16,a18)),
% 63.71/63.78 inference(scs_inference,[],[143,261,269,263,271,287,295,250,161,148,230,213,212,150,151,251,249,157,252,149,160,152])).
% 63.71/63.78 cnf(341,plain,
% 63.71/63.78 (~P9(a2,a17,a2,a19,a15,a16,a18,a1)),
% 63.71/63.78 inference(scs_inference,[],[143,261,144,269,263,271,287,295,250,161,148,230,213,212,150,151,251,249,157,252,149,160,152,237])).
% 63.71/63.78 cnf(355,plain,
% 63.71/63.78 (~P9(a2,a19,a2,a17,a18,a1,a15,a16)),
% 63.71/63.78 inference(scs_inference,[],[341,250])).
% 63.71/63.78 cnf(359,plain,
% 63.71/63.78 (~P1(a17,a19,a2)),
% 63.71/63.78 inference(scs_inference,[],[335,341,299,250,212,148])).
% 63.71/63.78 cnf(361,plain,
% 63.71/63.78 (~P11(a17,x3611,a2,a19,x3611,a2)),
% 63.71/63.78 inference(scs_inference,[],[335,341,299,250,212,148,211])).
% 63.71/63.78 cnf(363,plain,
% 63.71/63.78 (~P9(a15,a16,a18,a1,a2,a17,a2,a19)),
% 63.71/63.78 inference(scs_inference,[],[335,341,299,250,212,148,211,249])).
% 63.71/63.78 cnf(367,plain,
% 63.71/63.78 (~P3(a19,a2,a17,a2)),
% 63.71/63.78 inference(scs_inference,[],[315,289,335,341,299,250,212,148,211,249,150,161])).
% 63.71/63.78 cnf(369,plain,
% 63.71/63.78 (~P9(a2,a17,x3691,x3692,a19,a2,x3691,x3692)),
% 63.71/63.78 inference(scs_inference,[],[315,289,313,335,341,299,250,212,148,211,249,150,161,230])).
% 63.71/63.78 cnf(371,plain,
% 63.71/63.78 (~P11(a2,a19,x3711,a2,a17,x3711)),
% 63.71/63.78 inference(scs_inference,[],[315,289,313,335,341,297,299,250,212,148,211,249,150,161,230,213])).
% 63.71/63.78 cnf(375,plain,
% 63.71/63.78 (~P3(a17,a2,a17,a19)),
% 63.71/63.78 inference(scs_inference,[],[315,289,313,335,341,297,299,250,212,148,211,249,150,161,230,213,251,157])).
% 63.71/63.78 cnf(377,plain,
% 63.71/63.78 (~P3(a19,a17,a19,a2)),
% 63.71/63.78 inference(scs_inference,[],[315,289,313,331,335,341,297,299,250,212,148,211,249,150,161,230,213,251,157,160])).
% 63.71/63.78 cnf(379,plain,
% 63.71/63.78 (~P9(a2,a17,a15,a16,a2,a19,a18,a1)),
% 63.71/63.78 inference(scs_inference,[],[315,289,313,331,335,341,297,299,250,212,148,211,249,150,161,230,213,251,157,160,252])).
% 63.71/63.78 cnf(383,plain,
% 63.71/63.78 (~P9(a2,a17,a19,a2,a15,a16,a18,a1)),
% 63.71/63.78 inference(scs_inference,[],[315,144,285,289,313,331,335,341,297,299,250,212,148,211,249,150,161,230,213,251,157,160,252,152,237])).
% 63.71/63.78 cnf(399,plain,
% 63.71/63.78 (~P9(a19,a2,a2,a17,a18,a1,a15,a16)),
% 63.71/63.78 inference(scs_inference,[],[383,250])).
% 63.71/63.78 cnf(401,plain,
% 63.71/63.78 (~P9(a17,a2,x4011,x4012,a2,a19,x4011,x4012)),
% 63.71/63.78 inference(scs_inference,[],[337,383,250,230])).
% 63.71/63.78 cnf(403,plain,
% 63.71/63.78 (~P9(a17,a2,a19,a2,a15,a16,a18,a1)),
% 63.71/63.78 inference(scs_inference,[],[337,383,250,230,251])).
% 63.71/63.78 cnf(407,plain,
% 63.71/63.78 (~P3(a17,a2,a19,a2)),
% 63.71/63.78 inference(scs_inference,[],[337,383,371,250,230,251,212,161])).
% 63.71/63.78 cnf(411,plain,
% 63.71/63.78 (~P9(a15,a16,a18,a1,a2,a17,a19,a2)),
% 63.71/63.78 inference(scs_inference,[],[337,383,371,250,230,251,212,161,211,249])).
% 63.71/63.78 cnf(413,plain,
% 63.71/63.78 (~P3(a17,a19,a17,a2)),
% 63.71/63.78 inference(scs_inference,[],[359,337,383,371,250,230,251,212,161,211,249,157])).
% 63.71/63.78 cnf(415,plain,
% 63.71/63.78 (~P9(a2,a17,a15,a16,a19,a2,a18,a1)),
% 63.71/63.78 inference(scs_inference,[],[359,337,383,371,250,230,251,212,161,211,249,157,252])).
% 63.71/63.78 cnf(421,plain,
% 63.71/63.78 (~P9(a19,a2,a17,a2,a15,a16,a18,a1)),
% 63.71/63.78 inference(scs_inference,[],[144,359,339,337,367,383,361,371,250,230,251,212,161,211,249,157,252,213,152,237])).
% 63.71/63.78 cnf(425,plain,
% 63.71/63.78 (~P9(a19,a17,a19,x4251,a2,a17,a2,x4251)+P6(x4251,a19,a2,a2)),
% 63.71/63.78 inference(scs_inference,[],[144,261,359,339,337,367,383,361,371,250,230,251,212,161,211,249,157,252,213,152,237,231,227,182])).
% 63.71/63.78 cnf(429,plain,
% 63.71/63.78 (~P9(a17,a2,a19,a2,a18,a1,a15,a16)),
% 63.71/63.78 inference(scs_inference,[],[421,250])).
% 63.71/63.78 cnf(431,plain,
% 63.71/63.78 (~P9(a2,a19,a17,a2,a15,a16,a18,a1)),
% 63.71/63.78 inference(scs_inference,[],[421,250,251])).
% 63.71/63.78 cnf(433,plain,
% 63.71/63.78 (~P9(a15,a16,a18,a1,a19,a2,a17,a2)),
% 63.71/63.78 inference(scs_inference,[],[421,250,251,249])).
% 63.71/63.78 cnf(435,plain,
% 63.71/63.78 (~P9(a17,a2,x4351,x4352,a17,a19,x4351,x4352)),
% 63.71/63.78 inference(scs_inference,[],[375,421,250,251,249,230])).
% 63.71/63.78 cnf(437,plain,
% 63.71/63.78 (~P3(a17,a2,a19,a17)),
% 63.71/63.78 inference(scs_inference,[],[375,421,250,251,249,230,161])).
% 63.71/63.78 cnf(439,plain,
% 63.71/63.78 (~P3(a19,a17,a17,a2)),
% 63.71/63.78 inference(scs_inference,[],[375,421,250,251,249,230,161,160])).
% 63.71/63.78 cnf(441,plain,
% 63.71/63.78 (~P9(a19,a2,a15,a16,a17,a2,a18,a1)),
% 63.71/63.78 inference(scs_inference,[],[375,421,250,251,249,230,161,160,252])).
% 63.71/63.78 cnf(443,plain,
% 63.71/63.78 (~P9(a17,a2,a17,a19,a15,a16,a18,a1)),
% 63.71/63.78 inference(scs_inference,[],[144,375,421,250,251,249,230,161,160,252,237])).
% 63.71/63.78 cnf(460,plain,
% 63.71/63.78 (~P9(a15,a16,a18,a1,a17,a2,a17,a19)),
% 63.71/63.78 inference(scs_inference,[],[443,250,249])).
% 63.71/63.78 cnf(462,plain,
% 63.71/63.78 (~P9(a2,a17,a17,a19,a15,a16,a18,a1)),
% 63.71/63.78 inference(scs_inference,[],[443,250,249,251])).
% 63.71/63.78 cnf(464,plain,
% 63.71/63.78 (~P9(a19,a17,x4641,x4642,a19,a2,x4641,x4642)),
% 63.71/63.78 inference(scs_inference,[],[377,443,250,249,251,230])).
% 63.71/63.78 cnf(466,plain,
% 63.71/63.78 (~P9(a17,a2,a15,a16,a17,a19,a18,a1)),
% 63.71/63.78 inference(scs_inference,[],[377,443,250,249,251,230,252])).
% 63.71/63.78 cnf(468,plain,
% 63.71/63.78 (~P3(a19,a17,a2,a19)),
% 63.71/63.78 inference(scs_inference,[],[377,443,250,249,251,230,252,161])).
% 63.71/63.78 cnf(470,plain,
% 63.71/63.78 (~P9(a19,a17,a19,a2,a15,a16,a18,a1)),
% 63.71/63.78 inference(scs_inference,[],[144,377,443,250,249,251,230,252,161,237])).
% 63.71/63.78 cnf(472,plain,
% 63.71/63.78 (~P3(a2,a19,a19,a17)),
% 63.71/63.78 inference(scs_inference,[],[144,377,443,250,249,251,230,252,161,237,160])).
% 63.71/63.78 cnf(480,plain,
% 63.71/63.78 (~P9(a19,a2,a19,a17,a18,a1,a15,a16)),
% 63.71/63.78 inference(scs_inference,[],[470,250])).
% 63.71/63.78 cnf(482,plain,
% 63.71/63.78 (~P9(a17,a19,a19,a2,a15,a16,a18,a1)),
% 63.71/63.78 inference(scs_inference,[],[470,250,251])).
% 63.71/63.78 cnf(484,plain,
% 63.71/63.78 (~P3(a19,a2,a17,a19)),
% 63.71/63.78 inference(scs_inference,[],[331,470,250,251,161])).
% 63.71/63.78 cnf(486,plain,
% 63.71/63.78 (~P9(a15,a16,a18,a1,a19,a17,a19,a2)),
% 63.71/63.78 inference(scs_inference,[],[331,470,250,251,161,249])).
% 63.71/63.78 cnf(488,plain,
% 63.71/63.78 (~P9(a19,a2,x4881,x4882,a19,a17,x4881,x4882)),
% 63.71/63.78 inference(scs_inference,[],[331,470,250,251,161,249,230])).
% 63.71/63.78 cnf(490,plain,
% 63.71/63.78 (~P9(a19,a17,a15,a16,a19,a2,a18,a1)),
% 63.71/63.78 inference(scs_inference,[],[331,470,250,251,161,249,230,252])).
% 63.71/63.78 cnf(492,plain,
% 63.71/63.78 (~P9(a19,a2,a19,a17,a15,a16,a18,a1)),
% 63.71/63.78 inference(scs_inference,[],[144,331,470,250,251,161,249,230,252,237])).
% 63.71/63.78 cnf(494,plain,
% 63.71/63.78 (~P3(a17,a19,a19,a2)),
% 63.71/63.78 inference(scs_inference,[],[144,331,470,250,251,161,249,230,252,237,160])).
% 63.71/63.78 cnf(502,plain,
% 63.71/63.78 (~P9(a19,a17,a19,a2,a18,a1,a15,a16)),
% 63.71/63.78 inference(scs_inference,[],[492,250])).
% 63.71/63.78 cnf(504,plain,
% 63.71/63.78 (~P3(a17,a19,a2,a17)),
% 63.71/63.78 inference(scs_inference,[],[413,492,250,161])).
% 63.71/63.78 cnf(506,plain,
% 63.71/63.78 (~P9(a2,a19,a19,a17,a15,a16,a18,a1)),
% 63.71/63.78 inference(scs_inference,[],[413,492,250,161,251])).
% 63.71/63.78 cnf(508,plain,
% 63.71/63.78 (~P9(a19,a2,a15,a16,a19,a17,a18,a1)),
% 63.71/63.78 inference(scs_inference,[],[413,492,250,161,251,252])).
% 63.71/63.78 cnf(510,plain,
% 63.71/63.78 (~P9(a15,a16,a18,a1,a19,a2,a19,a17)),
% 63.71/63.78 inference(scs_inference,[],[413,492,250,161,251,252,249])).
% 63.71/63.78 cnf(512,plain,
% 63.71/63.78 (~P9(a19,a2,x5121,x5122,a17,a2,x5121,x5122)),
% 63.71/63.78 inference(scs_inference,[],[367,413,492,250,161,251,252,249,230])).
% 63.71/63.78 cnf(514,plain,
% 63.71/63.78 (~P9(a17,a19,a17,a2,a15,a16,a18,a1)),
% 63.71/63.78 inference(scs_inference,[],[144,367,413,492,250,161,251,252,249,230,237])).
% 63.71/63.78 cnf(516,plain,
% 63.71/63.78 (~P3(a2,a17,a17,a19)),
% 63.71/63.78 inference(scs_inference,[],[144,367,413,492,250,161,251,252,249,230,237,160])).
% 63.71/63.78 cnf(520,plain,
% 63.71/63.78 (~P9(a2,a19,a2,x5201,a17,a19,a17,x5201)+P6(x5201,a2,a17,a17)),
% 63.71/63.78 inference(scs_inference,[],[144,263,367,413,492,250,161,251,252,249,230,237,160,231,182])).
% 63.71/63.78 cnf(524,plain,
% 63.71/63.78 (~P9(a17,a2,a17,a19,a18,a1,a15,a16)),
% 63.71/63.78 inference(scs_inference,[],[514,250])).
% 63.71/63.78 cnf(526,plain,
% 63.71/63.78 (~P9(a19,a17,a17,a2,a15,a16,a18,a1)),
% 63.71/63.78 inference(scs_inference,[],[514,250,251])).
% 63.71/63.78 cnf(528,plain,
% 63.71/63.78 (~P3(a19,a17,a2,a17)),
% 63.71/63.78 inference(scs_inference,[],[439,514,250,251,161])).
% 63.71/63.78 cnf(530,plain,
% 63.71/63.78 (~P9(a17,a2,x5301,x5302,a19,a2,x5301,x5302)),
% 63.71/63.78 inference(scs_inference,[],[407,439,514,250,251,161,230])).
% 63.71/63.78 cnf(532,plain,
% 63.71/63.78 (~P9(a17,a19,a15,a16,a17,a2,a18,a1)),
% 63.71/63.78 inference(scs_inference,[],[407,439,514,250,251,161,230,252])).
% 63.71/63.78 cnf(536,plain,
% 63.71/63.78 (~P9(a17,a2,a19,a17,a15,a16,a18,a1)),
% 63.71/63.78 inference(scs_inference,[],[144,407,437,439,514,250,251,161,230,252,249,237])).
% 63.71/63.78 cnf(538,plain,
% 63.71/63.78 (~P3(a2,a17,a19,a17)),
% 63.71/63.78 inference(scs_inference,[],[144,407,437,439,514,250,251,161,230,252,249,237,160])).
% 63.71/63.78 cnf(549,plain,
% 63.71/63.78 (~P9(a19,a17,a17,a2,a18,a1,a15,a16)),
% 63.71/63.78 inference(scs_inference,[],[536,250])).
% 63.71/63.78 cnf(551,plain,
% 63.71/63.78 (~P3(a2,a19,a17,a19)),
% 63.71/63.78 inference(scs_inference,[],[472,536,250,161])).
% 63.71/63.78 cnf(553,plain,
% 63.71/63.78 (~P9(a2,a17,a19,a17,a15,a16,a18,a1)),
% 63.71/63.78 inference(scs_inference,[],[472,536,250,161,251])).
% 63.71/63.78 cnf(555,plain,
% 63.71/63.78 (~P9(a15,a16,a18,a1,a17,a2,a19,a17)),
% 63.71/63.78 inference(scs_inference,[],[472,536,250,161,251,249])).
% 63.71/63.78 cnf(557,plain,
% 63.71/63.78 (~P9(a19,a17,x5571,x5572,a2,a19,x5571,x5572)),
% 63.71/63.78 inference(scs_inference,[],[468,472,536,250,161,251,249,230])).
% 63.71/63.78 cnf(559,plain,
% 63.71/63.78 (~P9(a17,a2,a15,a16,a19,a17,a18,a1)),
% 63.71/63.78 inference(scs_inference,[],[468,472,536,250,161,251,249,230,252])).
% 63.71/63.78 cnf(561,plain,
% 63.71/63.78 (~P9(a19,a17,a2,a19,a15,a16,a18,a1)),
% 63.71/63.78 inference(scs_inference,[],[144,468,472,536,250,161,251,249,230,252,237])).
% 63.71/63.78 cnf(563,plain,
% 63.71/63.78 (~P3(a17,a19,a2,a19)),
% 63.71/63.78 inference(scs_inference,[],[144,468,472,536,250,161,251,249,230,252,237,160])).
% 63.71/63.78 cnf(570,plain,
% 63.71/63.78 (~P9(a2,a19,a19,a17,a18,a1,a15,a16)),
% 63.71/63.78 inference(scs_inference,[],[561,250])).
% 63.71/63.78 cnf(572,plain,
% 63.71/63.78 (~P9(a17,a19,a2,a19,a15,a16,a18,a1)),
% 63.71/63.78 inference(scs_inference,[],[561,250,251])).
% 63.71/63.78 cnf(574,plain,
% 63.71/63.78 (~P9(a19,a17,a15,a16,a2,a19,a18,a1)),
% 63.71/63.78 inference(scs_inference,[],[561,250,251,252])).
% 63.71/63.78 cnf(576,plain,
% 63.71/63.78 (~P9(a15,a16,a18,a1,a19,a17,a2,a19)),
% 63.71/63.78 inference(scs_inference,[],[561,250,251,252,249])).
% 63.71/63.78 cnf(578,plain,
% 63.71/63.78 (~P9(a19,a2,x5781,x5782,a17,a19,x5781,x5782)),
% 63.71/63.78 inference(scs_inference,[],[484,561,250,251,252,249,230])).
% 63.71/63.78 cnf(580,plain,
% 63.71/63.78 (~P9(a19,a2,a17,a19,a15,a16,a18,a1)),
% 63.71/63.78 inference(scs_inference,[],[144,484,561,250,251,252,249,230,237])).
% 63.71/63.78 cnf(592,plain,
% 63.71/63.78 (~P9(a17,a19,a19,a2,a18,a1,a15,a16)),
% 63.71/63.78 inference(scs_inference,[],[580,250])).
% 63.71/63.78 cnf(594,plain,
% 63.71/63.78 (~P9(a19,a2,a15,a16,a17,a19,a18,a1)),
% 63.71/63.78 inference(scs_inference,[],[580,250,252])).
% 63.71/63.78 cnf(596,plain,
% 63.71/63.78 (~P9(a2,a19,a17,a19,a15,a16,a18,a1)),
% 63.71/63.78 inference(scs_inference,[],[580,250,252,251])).
% 63.71/63.78 cnf(598,plain,
% 63.71/63.78 (~P9(a15,a16,a18,a1,a19,a2,a17,a19)),
% 63.71/63.78 inference(scs_inference,[],[580,250,252,251,249])).
% 63.71/63.78 cnf(600,plain,
% 63.71/63.78 (~P9(a17,a19,x6001,x6002,a19,a2,x6001,x6002)),
% 63.71/63.78 inference(scs_inference,[],[494,580,250,252,251,249,230])).
% 63.71/63.78 cnf(602,plain,
% 63.71/63.78 (~P9(a17,a19,a2,a17,a15,a16,a18,a1)),
% 63.71/63.78 inference(scs_inference,[],[144,494,504,580,250,252,251,249,230,237])).
% 63.71/63.78 cnf(612,plain,
% 63.71/63.78 (~P9(a2,a17,a17,a19,a18,a1,a15,a16)),
% 63.71/63.78 inference(scs_inference,[],[602,250])).
% 63.71/63.78 cnf(614,plain,
% 63.71/63.78 (~P9(a19,a17,a2,a17,a15,a16,a18,a1)),
% 63.71/63.78 inference(scs_inference,[],[602,250,251])).
% 63.71/63.78 cnf(616,plain,
% 63.71/63.78 (~P9(a17,a19,a15,a16,a2,a17,a18,a1)),
% 63.71/63.78 inference(scs_inference,[],[602,250,251,252])).
% 63.71/63.78 cnf(618,plain,
% 63.71/63.78 (~P9(a15,a16,a18,a1,a17,a19,a2,a17)),
% 63.71/63.78 inference(scs_inference,[],[602,250,251,252,249])).
% 63.71/63.78 cnf(620,plain,
% 63.71/63.78 (~P9(a2,a17,x6201,x6202,a17,a19,x6201,x6202)),
% 63.71/63.78 inference(scs_inference,[],[516,602,250,251,252,249,230])).
% 63.71/63.78 cnf(630,plain,
% 63.71/63.78 (~P9(a2,a17,a2,a19,x6301,x6302,x6301,x6302)),
% 63.71/63.78 inference(scs_inference,[],[283,250])).
% 63.71/63.78 cnf(632,plain,
% 63.71/63.78 (~P9(x6321,x6322,x6321,x6322,a2,a19,a2,a17)),
% 63.71/63.78 inference(scs_inference,[],[279,283,250,252])).
% 63.71/63.78 cnf(634,plain,
% 63.71/63.78 (~P9(x6341,x6342,a2,a19,x6342,x6341,a2,a17)),
% 63.71/63.78 inference(scs_inference,[],[279,283,250,252,251])).
% 63.71/63.78 cnf(638,plain,
% 63.71/63.78 (~P9(a19,a17,x6381,x6382,a2,a17,x6381,x6382)),
% 63.71/63.78 inference(scs_inference,[],[528,279,283,250,252,251,249,230])).
% 63.71/63.78 cnf(642,plain,
% 63.71/63.78 (~P11(a2,a17,x6421,a19,a17,x6421)),
% 63.71/63.78 inference(scs_inference,[],[528,279,283,250,252,251,249,230,228,211])).
% 63.71/63.78 cnf(644,plain,
% 63.71/63.78 (~P11(a19,x6441,a17,a2,x6441,a17)),
% 63.71/63.78 inference(scs_inference,[],[528,279,283,250,252,251,249,230,228,211,213])).
% 63.71/63.78 cnf(646,plain,
% 63.71/63.78 (~P11(a17,a19,x6461,a17,a2,x6461)),
% 63.71/63.78 inference(scs_inference,[],[528,279,283,250,252,251,249,230,228,211,213,212])).
% 63.71/63.78 cnf(653,plain,
% 63.71/63.78 (~P11(a2,x6531,a17,a19,x6531,a17)),
% 63.71/63.78 inference(scs_inference,[],[644,211])).
% 63.71/63.78 cnf(657,plain,
% 63.71/63.78 (~P11(a17,x6571,a19,a17,x6571,a2)),
% 63.71/63.78 inference(scs_inference,[],[281,644,646,211,250,213])).
% 63.71/63.78 cnf(659,plain,
% 63.71/63.78 (~P11(a17,a2,x6591,a17,a19,x6591)),
% 63.71/63.78 inference(scs_inference,[],[281,642,644,646,211,250,213,212])).
% 63.71/63.78 cnf(661,plain,
% 63.71/63.78 (~P9(a19,a2,a2,a17,x6611,x6612,x6611,x6612)),
% 63.71/63.78 inference(scs_inference,[],[283,281,642,644,646,211,250,213,212,251])).
% 63.71/63.78 cnf(663,plain,
% 63.71/63.78 (~P9(a2,a19,a17,a2,x6631,x6632,x6631,x6632)),
% 63.71/63.78 inference(scs_inference,[],[283,281,317,642,644,646,211,250,213,212,251,252])).
% 63.71/63.78 cnf(667,plain,
% 63.71/63.78 (~P9(a2,a17,x6671,x6672,a19,a17,x6671,x6672)),
% 63.71/63.78 inference(scs_inference,[],[538,283,281,317,435,642,644,646,211,250,213,212,251,252,249,230])).
% 63.71/63.78 cnf(669,plain,
% 63.71/63.78 (~P11(a19,a2,a17,x6691,x6691,x6691)),
% 63.71/63.78 inference(scs_inference,[],[538,283,281,317,435,642,644,646,211,250,213,212,251,252,249,230,228])).
% 63.71/63.78 cnf(680,plain,
% 63.71/63.78 (~P11(x6801,x6801,x6801,a19,a2,a17)),
% 63.71/63.78 inference(scs_inference,[],[669,211])).
% 63.71/63.78 cnf(682,plain,
% 63.71/63.78 (~P11(a19,a17,a2,x6821,x6821,x6821)),
% 63.71/63.78 inference(scs_inference,[],[669,211,213])).
% 63.71/63.78 cnf(686,plain,
% 63.71/63.78 (~P11(a2,a19,a17,x6861,x6861,x6861)),
% 63.71/63.78 inference(scs_inference,[],[317,669,211,213,250,212])).
% 63.71/63.78 cnf(688,plain,
% 63.71/63.78 (~P9(a2,a17,a19,a2,x6881,x6882,x6881,x6882)),
% 63.71/63.78 inference(scs_inference,[],[317,369,669,211,213,250,212,252])).
% 63.71/63.78 cnf(690,plain,
% 63.71/63.78 (~P9(a2,a19,x6901,x6902,a19,a17,x6901,x6902)),
% 63.71/63.78 inference(scs_inference,[],[317,369,488,669,211,213,250,212,252,251])).
% 63.71/63.78 cnf(692,plain,
% 63.71/63.78 (~P9(a17,a19,x6921,x6922,a2,a17,x6921,x6922)),
% 63.71/63.79 inference(scs_inference,[],[317,369,488,620,669,211,213,250,212,252,251,249])).
% 63.71/63.79 cnf(694,plain,
% 63.71/63.79 (~P9(a2,a19,x6941,x6942,a17,a19,x6941,x6942)),
% 63.71/63.79 inference(scs_inference,[],[551,317,369,488,620,669,211,213,250,212,252,251,249,230])).
% 63.71/63.79 cnf(696,plain,
% 63.71/63.79 (~P11(a2,a19,x6961,a17,a19,x6961)),
% 63.71/63.79 inference(scs_inference,[],[551,317,369,488,620,669,211,213,250,212,252,251,249,230,228])).
% 63.71/63.79 cnf(706,plain,
% 63.71/63.79 (~P11(x7061,x7061,x7061,a19,a17,a2)),
% 63.71/63.79 inference(scs_inference,[],[682,211])).
% 63.71/63.79 cnf(708,plain,
% 63.71/63.79 (~P9(x7081,x7082,a19,a2,x7081,x7082,a17,a2)),
% 63.71/63.79 inference(scs_inference,[],[512,682,211,250])).
% 63.71/63.79 cnf(710,plain,
% 63.71/63.79 (~P11(a2,a17,a19,x7101,x7101,x7101)),
% 63.71/63.79 inference(scs_inference,[],[512,682,686,211,250,213])).
% 63.71/63.79 cnf(714,plain,
% 63.71/63.79 (~P9(a17,a19,x7141,x7142,a2,a19,x7141,x7142)),
% 63.71/63.79 inference(scs_inference,[],[512,557,680,682,686,211,250,213,212,251])).
% 63.71/63.79 cnf(718,plain,
% 63.71/63.79 (~P9(x7181,x7182,x7181,x7182,a2,a17,a2,a19)),
% 63.71/63.79 inference(scs_inference,[],[512,557,630,680,682,686,211,250,213,212,251,252,249])).
% 63.71/63.79 cnf(720,plain,
% 63.71/63.79 (~P9(a17,a2,x7201,x7202,a19,a17,x7201,x7202)),
% 63.71/63.79 inference(scs_inference,[],[437,512,557,630,680,682,686,211,250,213,212,251,252,249,230])).
% 63.71/63.79 cnf(722,plain,
% 63.71/63.79 (~P11(a17,a19,x7221,a2,a19,x7221)),
% 63.71/63.79 inference(scs_inference,[],[437,512,557,630,680,682,686,211,250,213,212,251,252,249,230,228])).
% 63.71/63.79 cnf(733,plain,
% 63.71/63.79 (~P11(x7331,x7331,x7331,a17,a19,a2)),
% 63.71/63.79 inference(scs_inference,[],[369,706,710,659,211,213,250,212])).
% 63.71/63.79 cnf(735,plain,
% 63.71/63.79 (~P9(a17,a2,a2,a19,x7351,x7352,x7351,x7352)),
% 63.71/63.79 inference(scs_inference,[],[369,401,706,710,659,211,213,250,212,252])).
% 63.71/63.79 cnf(737,plain,
% 63.71/63.79 (~P9(x7371,x7372,x7372,x7371,a2,a19,a2,a17)),
% 63.71/63.79 inference(scs_inference,[],[369,401,632,706,710,659,211,213,250,212,252,251])).
% 63.71/63.79 cnf(741,plain,
% 63.71/63.79 (~P9(a19,a17,x7411,x7412,a17,a2,x7411,x7412)),
% 63.71/63.79 inference(scs_inference,[],[439,369,401,632,634,706,710,659,211,213,250,212,252,251,249,230])).
% 63.71/63.79 cnf(752,plain,
% 63.71/63.79 (~P11(x7521,a2,a17,x7521,a19,a17)),
% 63.71/63.79 inference(scs_inference,[],[401,733,653,211,250,213,212])).
% 63.71/63.79 cnf(754,plain,
% 63.71/63.79 (~P9(x7541,x7542,x7542,x7541,a2,a17,a2,a19)),
% 63.71/63.79 inference(scs_inference,[],[401,718,733,653,211,250,213,212,251])).
% 63.71/63.79 cnf(756,plain,
% 63.71/63.79 (~P9(a17,a2,a19,a2,x7561,x7562,x7561,x7562)),
% 63.71/63.79 inference(scs_inference,[],[401,530,718,733,653,211,250,213,212,251,252])).
% 63.71/63.79 cnf(758,plain,
% 63.71/63.79 (~P9(x7581,x7582,x7581,x7582,a19,a2,a2,a17)),
% 63.71/63.79 inference(scs_inference,[],[401,530,661,718,733,653,211,250,213,212,251,252,249])).
% 63.71/63.79 cnf(763,plain,
% 63.71/63.79 (~P11(a2,x7631,a19,a17,x7631,a19)),
% 63.71/63.79 inference(scs_inference,[],[696,752,211,213])).
% 63.71/63.79 cnf(765,plain,
% 63.71/63.79 (~P9(x7651,x7652,a17,a2,x7651,x7652,a17,a19)),
% 63.71/63.79 inference(scs_inference,[],[435,696,752,211,213,250])).
% 63.71/63.79 cnf(769,plain,
% 63.71/63.79 (~P9(a17,a2,a17,a19,x7691,x7692,x7691,x7692)),
% 63.71/63.79 inference(scs_inference,[],[435,657,696,752,211,213,250,212,252])).
% 63.71/63.79 cnf(771,plain,
% 63.71/63.79 (~P9(a17,a2,a2,a19,a18,a1,a15,a16)),
% 63.71/63.79 inference(scs_inference,[],[435,311,657,696,752,211,213,250,212,252,251])).
% 63.71/63.79 cnf(773,plain,
% 63.71/63.79 (~P9(x7731,x7732,x7731,x7732,a2,a19,a17,a2)),
% 63.71/63.79 inference(scs_inference,[],[435,663,311,657,696,752,211,213,250,212,252,251,249])).
% 63.71/63.79 cnf(778,plain,
% 63.71/63.79 (~P11(a17,x7781,a19,a2,x7781,a19)),
% 63.71/63.79 inference(scs_inference,[],[763,211])).
% 63.71/63.79 cnf(780,plain,
% 63.71/63.79 (~P9(x7801,x7802,a17,a2,x7801,x7802,a19,a2)),
% 63.71/63.79 inference(scs_inference,[],[530,763,211,250])).
% 63.71/63.79 cnf(782,plain,
% 63.71/63.79 (~P11(a19,a17,x7821,a19,a2,x7821)),
% 63.71/63.79 inference(scs_inference,[],[530,722,763,211,250,212])).
% 63.71/63.79 cnf(784,plain,
% 63.71/63.79 (~P9(a16,a15,a18,a1,a2,a19,a2,a17)),
% 63.71/63.79 inference(scs_inference,[],[530,329,722,763,211,250,212,251])).
% 63.71/63.79 cnf(786,plain,
% 63.71/63.79 (~P9(a19,a17,a19,a2,x7861,x7862,x7861,x7862)),
% 63.71/63.79 inference(scs_inference,[],[530,464,329,722,763,211,250,212,251,252])).
% 63.71/63.79 cnf(788,plain,
% 63.71/63.79 (~P9(a2,a19,a2,a17,x7881,x7882,x7882,x7881)),
% 63.71/63.79 inference(scs_inference,[],[530,464,737,329,722,763,211,250,212,251,252,249])).
% 63.71/63.79 cnf(802,plain,
% 63.71/63.79 (~P9(x8021,x8022,a19,a17,x8021,x8022,a19,a2)),
% 63.71/63.79 inference(scs_inference,[],[464,782,211,213,250])).
% 63.71/63.79 cnf(804,plain,
% 63.71/63.79 (~P11(x8041,a17,a19,x8041,a2,a19)),
% 63.71/63.79 inference(scs_inference,[],[464,778,782,211,213,250,212])).
% 63.71/63.79 cnf(806,plain,
% 63.71/63.79 (~P9(a2,a17,a2,a19,x8061,x8062,x8062,x8061)),
% 63.71/63.79 inference(scs_inference,[],[464,754,778,782,211,213,250,212,249])).
% 63.71/63.79 cnf(808,plain,
% 63.71/63.79 (~P9(x8081,x8082,x8082,x8081,a19,a2,a2,a17)),
% 63.71/63.79 inference(scs_inference,[],[464,754,758,778,782,211,213,250,212,249,251])).
% 63.71/63.79 cnf(810,plain,
% 63.71/63.79 (~P9(a19,a2,a19,a17,x8101,x8102,x8101,x8102)),
% 63.71/63.79 inference(scs_inference,[],[464,488,754,758,778,782,211,213,250,212,249,251,252])).
% 63.71/63.79 cnf(822,plain,
% 63.71/63.79 (~P11(x8221,x8222,x8221,a19,a2,a17)),
% 63.71/63.79 inference(scs_inference,[],[808,804,211,228])).
% 63.71/63.79 cnf(824,plain,
% 63.71/63.79 (~P9(x8241,x8242,a19,a2,x8241,x8242,a19,a17)),
% 63.71/63.79 inference(scs_inference,[],[488,808,804,211,228,250])).
% 63.71/63.79 cnf(828,plain,
% 63.71/63.79 (~P11(x8281,x8282,x8282,a2,a19,a17)),
% 63.71/63.79 inference(scs_inference,[],[488,808,804,211,228,250,213,212])).
% 63.71/63.79 cnf(830,plain,
% 63.71/63.79 (~P9(x8301,x8302,x8302,x8301,a2,a19,a17,a2)),
% 63.71/63.79 inference(scs_inference,[],[488,773,808,804,211,228,250,213,212,251])).
% 63.71/63.79 cnf(834,plain,
% 63.71/63.79 (~P9(a19,a17,a2,a19,x8341,x8342,x8341,x8342)),
% 63.71/63.79 inference(scs_inference,[],[488,557,688,773,808,804,211,228,250,213,212,251,249,252])).
% 63.71/63.79 cnf(846,plain,
% 63.71/63.79 (~P11(x8461,x8461,x8462,a19,a17,a2)),
% 63.71/63.79 inference(scs_inference,[],[634,822,211,250,213])).
% 63.71/63.79 cnf(848,plain,
% 63.71/63.79 (~P11(a2,a19,a17,x8481,x8482,x8482)),
% 63.71/63.79 inference(scs_inference,[],[634,822,211,250,213,212])).
% 63.71/63.79 cnf(850,plain,
% 63.71/63.79 (~P9(a19,a2,a2,a17,x8501,x8502,x8502,x8501)),
% 63.71/63.79 inference(scs_inference,[],[634,788,822,211,250,213,212,251])).
% 63.71/63.79 cnf(854,plain,
% 63.71/63.79 (~P9(x8541,x8542,x8541,x8542,a17,a2,a2,a19)),
% 63.71/63.79 inference(scs_inference,[],[634,578,735,788,822,211,250,213,212,251,252,249])).
% 63.71/63.79 cnf(856,plain,
% 63.71/63.79 (~P11(a2,a19,a17,a2,a17,a19)),
% 63.71/63.79 inference(scs_inference,[],[634,578,735,788,822,211,250,213,212,251,252,249,228])).
% 63.71/63.79 cnf(868,plain,
% 63.71/63.79 (~P9(x8681,x8682,a19,a17,x8681,x8682,a2,a19)),
% 63.71/63.79 inference(scs_inference,[],[557,828,846,211,213,250])).
% 63.71/63.79 cnf(870,plain,
% 63.71/63.79 (~P11(x8701,x8701,x8702,a17,a19,a2)),
% 63.71/63.79 inference(scs_inference,[],[557,828,846,211,213,250,212])).
% 63.71/63.79 cnf(872,plain,
% 63.71/63.79 (~P9(a2,a17,a17,a19,x8721,x8722,x8721,x8722)),
% 63.71/63.79 inference(scs_inference,[],[557,769,828,846,211,213,250,212,251])).
% 63.71/63.79 cnf(874,plain,
% 63.71/63.79 (~P9(a17,a19,a19,a2,x8741,x8742,x8741,x8742)),
% 63.71/63.79 inference(scs_inference,[],[557,600,769,828,846,211,213,250,212,251,252])).
% 63.71/63.79 cnf(884,plain,
% 63.71/63.79 (~P11(a2,a17,a19,a2,a19,a17)),
% 63.71/63.79 inference(scs_inference,[],[856,211])).
% 63.71/63.79 cnf(886,plain,
% 63.71/63.79 (~P9(x8861,x8862,a19,a2,x8861,x8862,a17,a19)),
% 63.71/63.79 inference(scs_inference,[],[578,856,211,250])).
% 63.71/63.79 cnf(890,plain,
% 63.71/63.79 (~P11(a19,a2,a17,a17,a2,a19)),
% 63.71/63.79 inference(scs_inference,[],[578,856,848,211,250,213,212])).
% 63.71/63.79 cnf(896,plain,
% 63.71/63.79 (~P9(x8961,x8962,x8961,x8962,a17,a2,a17,a19)),
% 63.71/63.79 inference(scs_inference,[],[578,638,769,806,856,848,211,250,213,212,252,251,249])).
% 63.71/63.79 cnf(910,plain,
% 63.71/63.79 (~P9(x9101,x9102,a17,a19,x9101,x9102,a19,a2)),
% 63.71/63.79 inference(scs_inference,[],[600,870,211,213,250])).
% 63.71/63.79 cnf(918,plain,
% 63.71/63.79 (~P9(x9181,x9182,x9181,x9182,a17,a2,a19,a2)),
% 63.71/63.79 inference(scs_inference,[],[600,667,756,810,884,870,211,213,250,212,251,252,249])).
% 63.71/63.79 cnf(924,plain,
% 63.71/63.79 (~P9(x9241,x9242,a19,a17,x9241,x9242,a2,a17)),
% 63.71/63.79 inference(scs_inference,[],[638,250])).
% 63.71/63.79 cnf(930,plain,
% 63.71/63.79 (~P9(a2,a19,a17,a19,x9301,x9302,x9301,x9302)),
% 63.71/63.79 inference(scs_inference,[],[638,694,890,250,213,212,252])).
% 63.71/63.79 cnf(932,plain,
% 63.71/63.79 (~P9(x9321,x9322,x9321,x9322,a19,a17,a19,a2)),
% 63.71/63.79 inference(scs_inference,[],[638,694,786,890,250,213,212,252,249])).
% 63.71/63.79 cnf(939,plain,
% 63.71/63.79 (~P9(x9391,x9392,a2,a17,x9391,x9392,a19,a17)),
% 63.71/63.79 inference(scs_inference,[],[667,250])).
% 63.71/63.79 cnf(945,plain,
% 63.71/63.79 (~P9(x9451,x9452,x9451,x9452,a19,a2,a19,a17)),
% 63.71/63.79 inference(scs_inference,[],[667,714,810,854,250,251,252,249])).
% 63.71/63.79 cnf(950,plain,
% 63.71/63.79 (~P9(x9501,x9502,a2,a19,x9501,x9502,a17,a19)),
% 63.71/63.79 inference(scs_inference,[],[694,250])).
% 63.71/63.79 cnf(954,plain,
% 63.71/63.79 (~P9(x9541,x9542,a17,a2,x9542,x9541,a17,a19)),
% 63.71/63.79 inference(scs_inference,[],[694,806,765,250,252,251])).
% 63.71/63.79 cnf(956,plain,
% 63.71/63.79 (~P9(x9561,x9562,x9561,x9562,a2,a17,a17,a19)),
% 63.71/63.79 inference(scs_inference,[],[694,806,872,765,250,252,251,249])).
% 63.71/63.79 cnf(961,plain,
% 63.71/63.79 (~P9(x9611,x9612,a19,a2,x9612,x9611,a19,a17)),
% 63.71/63.79 inference(scs_inference,[],[769,824,250,251])).
% 63.71/63.79 cnf(965,plain,
% 63.71/63.79 (~P9(x9651,x9652,a17,a19,x9651,x9652,a17,a2)),
% 63.71/63.79 inference(scs_inference,[],[769,808,824,765,250,251,252,249])).
% 63.71/63.79 cnf(973,plain,
% 63.71/63.79 (~P9(x9731,x9732,a17,a19,x9731,x9732,a2,a19)),
% 63.71/63.79 inference(scs_inference,[],[714,250])).
% 63.71/63.79 cnf(977,plain,
% 63.71/63.79 (~P9(x9771,x9772,a19,a17,x9772,x9771,a19,a2)),
% 63.71/63.79 inference(scs_inference,[],[714,692,802,250,252,251])).
% 63.71/63.79 cnf(979,plain,
% 63.71/63.79 (~P9(x9791,x9792,x9791,x9792,a17,a19,a19,a2)),
% 63.71/63.79 inference(scs_inference,[],[714,692,874,802,250,252,251,249])).
% 63.71/63.79 cnf(989,plain,
% 63.71/63.79 (~P9(x9891,x9892,x9892,x9891,a17,a2,a17,a19)),
% 63.71/63.79 inference(scs_inference,[],[620,896,250,251])).
% 63.71/63.79 cnf(993,plain,
% 63.71/63.79 (~P9(a2,a19,a17,a2,x9931,x9932,x9932,x9931)),
% 63.71/63.79 inference(scs_inference,[],[620,720,896,830,250,251,252,249])).
% 63.71/63.79 cnf(996,plain,
% 63.71/63.79 (~P9(x9961,x9962,x9962,x9961,a2,a17,a19,a2)),
% 63.71/63.79 inference(scs_inference,[],[808,250])).
% 63.71/63.79 cnf(1000,plain,
% 63.71/63.79 (~P9(x10001,x10002,x10002,x10001,a19,a17,a19,a2)),
% 63.71/63.79 inference(scs_inference,[],[808,741,932,250,252,251])).
% 63.71/63.79 cnf(1002,plain,
% 63.71/63.79 (~P9(x10021,x10022,x10021,x10022,a19,a17,a2,a19)),
% 63.71/63.79 inference(scs_inference,[],[808,741,932,834,250,252,251,249])).
% 63.71/63.79 cnf(1005,plain,
% 63.71/63.79 (~P9(x10051,x10052,x10051,x10052,a17,a19,a17,a2)),
% 63.71/63.79 inference(scs_inference,[],[896,250])).
% 63.71/63.79 cnf(1007,plain,
% 63.71/63.79 (~P9(x10071,x10072,x10072,x10071,a19,a2,a19,a17)),
% 63.71/63.79 inference(scs_inference,[],[896,945,250,251])).
% 63.71/63.79 cnf(1016,plain,
% 63.71/63.79 (~P9(a2,a17,a19,a2,x10161,x10162,x10162,x10161)),
% 63.71/63.79 inference(scs_inference,[],[850,250])).
% 63.71/63.79 cnf(1025,plain,
% 63.71/63.79 (~P9(x10251,x10252,a2,a19,x10251,x10252,a19,a17)),
% 63.71/63.79 inference(scs_inference,[],[690,250])).
% 63.71/63.79 cnf(1027,plain,
% 63.71/63.79 (~P9(x10271,x10272,a17,a19,x10272,x10271,a17,a2)),
% 63.71/63.79 inference(scs_inference,[],[690,965,250,251])).
% 63.71/63.79 cnf(1034,plain,
% 63.71/63.79 (~P9(x10341,x10342,a17,a19,x10341,x10342,a2,a17)),
% 63.71/63.79 inference(scs_inference,[],[692,250])).
% 63.71/63.79 cnf(1038,plain,
% 63.71/63.79 (~P9(x10381,x10382,x10382,x10381,a2,a17,a17,a19)),
% 63.71/63.79 inference(scs_inference,[],[692,956,993,250,252,251])).
% 63.71/63.79 cnf(1040,plain,
% 63.71/63.79 (~P9(a17,a2,a17,a19,x10401,x10402,x10402,x10401)),
% 63.71/63.79 inference(scs_inference,[],[692,989,956,993,250,252,251,249])).
% 63.71/63.79 cnf(1044,plain,
% 63.71/63.79 (~P11(x10441,x10441,x10442,a2,a19,a17)),
% 63.71/63.79 inference(scs_inference,[],[692,989,956,993,250,252,251,249,228,213])).
% 63.71/63.79 cnf(1046,plain,
% 63.71/63.79 (~P11(x10461,x10462,x10462,a17,a2,a19)),
% 63.71/63.79 inference(scs_inference,[],[692,989,956,993,250,252,251,249,228,213,212])).
% 63.71/63.79 cnf(1048,plain,
% 63.71/63.79 (~P11(a2,a17,a19,x10481,x10482,x10481)),
% 63.71/63.79 inference(scs_inference,[],[692,989,956,993,250,252,251,249,228,213,212,211])).
% 63.71/63.79 cnf(1053,plain,
% 63.71/63.79 (~P11(x10531,x10532,x10532,a17,a19,a2)),
% 63.71/63.79 inference(scs_inference,[],[1044,1046,211,213])).
% 63.71/63.79 cnf(1057,plain,
% 63.71/63.79 (~P11(x10571,x10571,x10572,a19,a2,a17)),
% 63.71/63.79 inference(scs_inference,[],[954,1044,1046,211,213,250,212])).
% 63.71/63.79 cnf(1059,plain,
% 63.71/63.79 (~P9(x10591,x10592,x10592,x10591,a17,a19,a17,a2)),
% 63.71/63.79 inference(scs_inference,[],[954,1005,1044,1046,211,213,250,212,251])).
% 63.71/63.79 cnf(1063,plain,
% 63.71/63.79 (~P9(a19,a17,a19,a2,x10631,x10632,x10632,x10631)),
% 63.71/63.79 inference(scs_inference,[],[954,1000,1005,996,1044,1046,211,213,250,212,251,252,249])).
% 63.71/63.79 cnf(1065,plain,
% 63.71/63.79 (~P11(a17,a2,a19,a17,a19,a2)),
% 63.71/63.79 inference(scs_inference,[],[954,1000,1005,996,1044,1046,211,213,250,212,251,252,249,228])).
% 63.71/63.79 cnf(1070,plain,
% 63.71/63.79 (~P11(x10701,x10702,x10701,a19,a17,a2)),
% 63.71/63.79 inference(scs_inference,[],[1053,1057,211,213])).
% 63.71/63.79 cnf(1078,plain,
% 63.71/63.79 (~P9(a19,a2,a15,a16,a2,a17,a18,a1)),
% 63.71/63.79 inference(scs_inference,[],[961,918,327,1048,1053,1057,211,213,250,212,251,252])).
% 63.71/63.79 cnf(1080,plain,
% 63.71/63.79 (~P9(a19,a2,a19,a17,x10801,x10802,x10802,x10801)),
% 63.71/63.79 inference(scs_inference,[],[961,1007,918,327,1048,1053,1057,211,213,250,212,251,252,249])).
% 63.71/63.79 cnf(1082,plain,
% 63.71/63.79 (~P11(a19,a2,a17,a19,a17,a2)),
% 63.71/63.79 inference(scs_inference,[],[961,1007,918,327,1048,1053,1057,211,213,250,212,251,252,249,228])).
% 63.71/63.79 cnf(1085,plain,
% 63.71/63.79 (~P11(a17,a19,a2,a17,a2,a19)),
% 63.71/63.79 inference(scs_inference,[],[1065,211])).
% 63.71/63.79 cnf(1087,plain,
% 63.71/63.79 (~P11(a19,a17,a2,a19,a2,a17)),
% 63.71/63.79 inference(scs_inference,[],[1065,1082,211,213])).
% 63.71/63.79 cnf(1091,plain,
% 63.71/63.79 (~P11(a2,a17,a19,a19,a17,a2)),
% 63.71/63.79 inference(scs_inference,[],[977,1065,1082,211,213,250,212])).
% 63.71/63.79 cnf(1093,plain,
% 63.71/63.79 (~P9(a2,a17,a17,a19,x10931,x10932,x10932,x10931)),
% 63.71/63.79 inference(scs_inference,[],[977,1040,1065,1082,211,213,250,212,251])).
% 63.71/63.79 cnf(1100,plain,
% 63.71/63.79 (~P11(a19,a17,a2,x11001,x11002,x11001)),
% 63.71/63.79 inference(scs_inference,[],[1070,211])).
% 63.71/63.79 cnf(1104,plain,
% 63.71/63.79 (~P9(x11041,x11042,a17,a2,x11041,x11042,a19,a17)),
% 63.71/63.79 inference(scs_inference,[],[720,1070,1091,211,213,250])).
% 63.71/63.79 cnf(1106,plain,
% 63.71/63.79 (~P11(a17,a19,a2,a2,a19,a17)),
% 63.71/63.79 inference(scs_inference,[],[720,1087,1070,1091,211,213,250,212])).
% 63.71/63.79 cnf(1108,plain,
% 63.71/63.79 (~P9(a17,a19,a19,a2,x11081,x11082,x11082,x11081)),
% 63.71/63.79 inference(scs_inference,[],[720,1063,1087,1070,1091,211,213,250,212,251])).
% 63.71/63.79 cnf(1110,plain,
% 63.71/63.79 (~P9(a17,a2,a15,a16,a19,a2,a18,a1)),
% 63.71/63.79 inference(scs_inference,[],[720,1063,403,1087,1070,1091,211,213,250,212,251,252])).
% 63.71/63.79 cnf(1114,plain,
% 63.71/63.79 (~P11(a17,a19,a2,x11141,x11142,x11141)),
% 63.71/63.79 inference(scs_inference,[],[720,930,1063,403,1087,1070,1091,211,213,250,212,251,252,249,228])).
% 63.71/63.79 cnf(1117,plain,
% 63.71/63.79 (~P11(x11171,x11172,x11171,a17,a19,a2)),
% 63.71/63.79 inference(scs_inference,[],[1114,211])).
% 63.71/63.79 cnf(1119,plain,
% 63.71/63.79 (~P9(x11191,x11192,a19,a17,x11191,x11192,a17,a2)),
% 63.71/63.79 inference(scs_inference,[],[741,1114,211,250])).
% 63.71/63.79 cnf(1123,plain,
% 63.71/63.79 (~P11(a19,a17,a2,a2,a17,a19)),
% 63.71/63.79 inference(scs_inference,[],[741,1085,1100,1114,211,250,213,212])).
% 63.71/63.79 cnf(1125,plain,
% 63.71/63.79 (~P9(a2,a19,a19,a17,x11251,x11252,x11252,x11251)),
% 63.71/63.79 inference(scs_inference,[],[741,1080,1085,1100,1114,211,250,213,212,251])).
% 63.71/63.79 cnf(1127,plain,
% 63.71/63.79 (~P9(a2,a19,a15,a16,a17,a2,a18,a1)),
% 63.71/63.79 inference(scs_inference,[],[741,1080,431,1085,1100,1114,211,250,213,212,251,252])).
% 63.71/63.79 cnf(1129,plain,
% 63.71/63.79 (~P9(a17,a19,a17,a2,x11291,x11292,x11292,x11291)),
% 63.71/63.79 inference(scs_inference,[],[741,1059,1080,431,1085,1100,1114,211,250,213,212,251,252,249])).
% 63.71/63.79 cnf(1131,plain,
% 63.71/63.79 (~P11(a2,a19,a17,x11311,x11312,x11311)),
% 63.71/63.79 inference(scs_inference,[],[741,1059,1080,431,1085,1100,1114,211,250,213,212,251,252,249,228])).
% 63.71/63.79 cnf(1134,plain,
% 63.71/63.79 (~P11(x11341,x11342,x11341,a2,a19,a17)),
% 63.71/63.79 inference(scs_inference,[],[1131,211])).
% 63.71/63.79 cnf(1136,plain,
% 63.71/63.79 (~P11(x11361,x11361,x11362,a17,a2,a19)),
% 63.71/63.79 inference(scs_inference,[],[1117,1131,211,213])).
% 63.71/63.79 cnf(1140,plain,
% 63.71/63.79 (~P11(x11401,x11402,x11402,a19,a17,a2)),
% 63.71/63.79 inference(scs_inference,[],[1027,1117,1131,211,213,250,212])).
% 63.71/63.79 cnf(1144,plain,
% 63.71/63.79 (~P9(a2,a17,a15,a16,a17,a19,a18,a1)),
% 63.71/63.79 inference(scs_inference,[],[1027,979,462,1117,1131,211,213,250,212,251,252])).
% 63.71/63.79 cnf(1149,plain,
% 63.71/63.79 (~P11(a17,a2,a19,x11491,x11491,x11492)),
% 63.71/63.79 inference(scs_inference,[],[1136,211])).
% 63.71/63.79 cnf(1155,plain,
% 63.71/63.79 (~P11(x11551,x11552,x11552,a19,a2,a17)),
% 63.71/63.79 inference(scs_inference,[],[956,1134,1136,211,250,213,212])).
% 63.71/63.79 cnf(1157,plain,
% 63.71/63.79 (~P9(a19,a17,a17,a2,x11571,x11572,x11572,x11571)),
% 63.71/63.79 inference(scs_inference,[],[956,1129,1134,1136,211,250,213,212,251])).
% 63.71/63.79 cnf(1159,plain,
% 63.71/63.79 (~P9(a17,a19,a15,a16,a19,a2,a18,a1)),
% 63.71/63.79 inference(scs_inference,[],[956,1129,482,1134,1136,211,250,213,212,251,252])).
% 63.71/63.79 cnf(1166,plain,
% 63.71/63.79 (~P11(a17,a2,a19,a2,a17,a19)),
% 63.71/63.79 inference(scs_inference,[],[1140,1106,211,213])).
% 63.71/63.79 cnf(1168,plain,
% 63.71/63.79 (~P9(a19,a17,a2,a19,a18,a1,a15,a16)),
% 63.71/63.79 inference(scs_inference,[],[506,1140,1106,211,213,250])).
% 63.71/63.79 cnf(1174,plain,
% 63.71/63.79 (~P9(a2,a19,a15,a16,a19,a17,a18,a1)),
% 63.71/63.79 inference(scs_inference,[],[1002,506,1140,1149,1106,211,213,250,212,251,252])).
% 63.71/63.79 cnf(1188,plain,
% 63.71/63.79 (~P9(a19,a2,a17,a2,x11881,x11882,x11882,x11881)),
% 63.71/63.79 inference(scs_inference,[],[993,526,1155,1123,1166,211,250,213,212,251])).
% 63.71/63.79 cnf(1190,plain,
% 63.71/63.79 (~P9(a19,a17,a15,a16,a17,a2,a18,a1)),
% 63.71/63.79 inference(scs_inference,[],[993,526,1155,1123,1166,211,250,213,212,251,252])).
% 63.71/63.79 cnf(1197,plain,
% 63.71/63.79 (~P9(a19,a17,a2,a17,a18,a1,a15,a16)),
% 63.71/63.79 inference(scs_inference,[],[553,1106,211,250])).
% 63.71/63.79 cnf(1199,plain,
% 63.71/63.79 (~P9(a16,a15,a18,a1,a2,a17,a2,a19)),
% 63.71/63.79 inference(scs_inference,[],[553,363,1106,211,250,251])).
% 63.71/63.79 cnf(1201,plain,
% 63.71/63.79 (~P9(a2,a17,a15,a16,a19,a17,a18,a1)),
% 63.71/63.79 inference(scs_inference,[],[553,363,1106,211,250,251,252])).
% 63.71/63.79 cnf(1203,plain,
% 63.71/63.79 (~P9(a15,a16,a18,a1,a2,a17,a19,a17)),
% 63.71/63.79 inference(scs_inference,[],[553,363,1106,211,250,251,252,249])).
% 63.71/63.79 cnf(1206,plain,
% 63.71/63.79 (~P9(a2,a19,a17,a19,a18,a1,a15,a16)),
% 63.71/63.79 inference(scs_inference,[],[572,250])).
% 63.71/63.79 cnf(1208,plain,
% 63.71/63.79 (~P9(a16,a15,a18,a1,a2,a17,a19,a2)),
% 63.71/63.79 inference(scs_inference,[],[572,411,250,251])).
% 63.71/63.79 cnf(1210,plain,
% 63.71/63.79 (~P9(a17,a19,a15,a16,a2,a19,a18,a1)),
% 63.71/63.79 inference(scs_inference,[],[572,411,250,251,252])).
% 63.71/63.79 cnf(1212,plain,
% 63.71/63.79 (~P9(a15,a16,a18,a1,a17,a19,a2,a19)),
% 63.71/63.79 inference(scs_inference,[],[572,411,250,251,252,249])).
% 63.71/63.79 cnf(1215,plain,
% 63.71/63.79 (~P9(a17,a19,a2,a19,a18,a1,a15,a16)),
% 63.71/63.79 inference(scs_inference,[],[596,250])).
% 63.71/63.79 cnf(1217,plain,
% 63.71/63.79 (~P9(a2,a17,a19,a2,a18,a1,a15,a16)),
% 63.71/63.79 inference(scs_inference,[],[596,429,250,251])).
% 63.71/63.79 cnf(1219,plain,
% 63.71/63.79 (~P9(a2,a19,a15,a16,a17,a19,a18,a1)),
% 63.71/63.79 inference(scs_inference,[],[596,429,250,251,252])).
% 63.71/63.79 cnf(1221,plain,
% 63.71/63.79 (~P9(a15,a16,a18,a1,a2,a19,a17,a19)),
% 63.71/63.79 inference(scs_inference,[],[596,429,250,251,252,249])).
% 63.71/63.79 cnf(1226,plain,
% 63.71/63.79 (~P9(a16,a15,a18,a1,a19,a2,a17,a2)),
% 63.71/63.79 inference(scs_inference,[],[614,433,250,251])).
% 63.71/63.79 cnf(1228,plain,
% 63.71/63.79 (~P9(a19,a17,a15,a16,a2,a17,a18,a1)),
% 63.71/63.79 inference(scs_inference,[],[614,433,250,251,252])).
% 63.71/63.79 cnf(1235,plain,
% 63.71/63.79 (~P9(a16,a15,a18,a1,a17,a2,a17,a19)),
% 63.71/63.79 inference(scs_inference,[],[333,460,250,251])).
% 63.71/63.79 cnf(1237,plain,
% 63.71/63.79 (~P9(a19,a2,a18,a1,a2,a17,a15,a16)),
% 63.71/63.79 inference(scs_inference,[],[399,333,460,250,251,252])).
% 63.71/63.79 cnf(1239,plain,
% 63.71/63.79 (~P9(a18,a1,a15,a16,a19,a2,a2,a17)),
% 63.71/63.79 inference(scs_inference,[],[399,333,460,250,251,252,249])).
% 63.71/63.79 cnf(1244,plain,
% 63.71/63.79 (~P9(a16,a15,a18,a1,a19,a17,a19,a2)),
% 63.71/63.79 inference(scs_inference,[],[379,486,250,251])).
% 63.71/63.79 cnf(1248,plain,
% 63.71/63.79 (~P9(a18,a1,a15,a16,a2,a19,a2,a17)),
% 63.71/63.79 inference(scs_inference,[],[355,379,486,250,251,252,249])).
% 63.71/63.79 cnf(1253,plain,
% 63.71/63.79 (~P9(a16,a15,a18,a1,a19,a2,a19,a17)),
% 63.71/63.79 inference(scs_inference,[],[415,510,250,251])).
% 63.71/63.79 cnf(1257,plain,
% 63.71/63.79 (~P9(a18,a1,a15,a16,a19,a17,a17,a2)),
% 63.71/63.79 inference(scs_inference,[],[549,415,510,250,251,252,249])).
% 63.71/63.79 cnf(1273,plain,
% 63.71/63.79 (~P9(a2,a19,a18,a1,a19,a17,a15,a16)),
% 63.71/63.79 inference(scs_inference,[],[570,466,555,250,251,252])).
% 63.71/63.79 cnf(1275,plain,
% 63.71/63.79 (~P9(a18,a1,a15,a16,a2,a19,a19,a17)),
% 63.71/63.79 inference(scs_inference,[],[570,466,555,250,251,252,249])).
% 63.71/63.79 cnf(1282,plain,
% 63.71/63.79 (~P9(a19,a2,a18,a1,a19,a17,a15,a16)),
% 63.71/63.79 inference(scs_inference,[],[480,490,576,250,251,252])).
% 63.71/63.79 cnf(1284,plain,
% 63.71/63.79 (~P9(a18,a1,a15,a16,a19,a2,a19,a17)),
% 63.71/63.79 inference(scs_inference,[],[480,490,576,250,251,252,249])).
% 63.71/63.79 cnf(1289,plain,
% 63.71/63.79 (~P9(a16,a15,a18,a1,a19,a2,a17,a19)),
% 63.71/63.79 inference(scs_inference,[],[508,598,250,251])).
% 63.71/63.79 cnf(1291,plain,
% 63.71/63.79 (~P9(a17,a19,a18,a1,a19,a2,a15,a16)),
% 63.71/63.79 inference(scs_inference,[],[592,508,598,250,251,252])).
% 63.71/63.79 cnf(1298,plain,
% 63.71/63.79 (~P9(a16,a15,a18,a1,a17,a19,a2,a17)),
% 63.71/63.79 inference(scs_inference,[],[532,618,250,251])).
% 63.71/63.79 cnf(1300,plain,
% 63.71/63.79 (~P9(a19,a17,a18,a1,a19,a2,a15,a16)),
% 63.71/63.79 inference(scs_inference,[],[502,532,618,250,251,252])).
% 63.71/63.79 cnf(1307,plain,
% 63.71/63.79 (~P9(x13071,x13072,a19,a2,x13072,x13071,a17,a2)),
% 63.71/63.79 inference(scs_inference,[],[559,708,250,251])).
% 63.71/63.79 cnf(1309,plain,
% 63.71/63.79 (~P9(a17,a2,a18,a1,a17,a19,a15,a16)),
% 63.71/63.79 inference(scs_inference,[],[524,559,708,250,251,252])).
% 63.71/63.79 cnf(1318,plain,
% 63.71/63.79 (~P9(a2,a17,a18,a1,a17,a19,a15,a16)),
% 63.71/63.79 inference(scs_inference,[],[612,574,780,250,251,252])).
% 63.71/63.79 cnf(1326,plain,
% 63.71/63.79 (~P9(x13261,x13262,a19,a17,x13262,x13261,a2,a19)),
% 63.71/63.79 inference(scs_inference,[],[594,868,250,251])).
% 63.71/63.79 cnf(1330,plain,
% 63.71/63.79 (~P9(a2,a17,a18,a1,a19,a2,a15,a16)),
% 63.71/63.79 inference(scs_inference,[],[594,1078,868,1038,250,251,252,249])).
% 63.71/63.79 cnf(1335,plain,
% 63.71/63.79 (~P9(x13351,x13352,a19,a2,x13352,x13351,a17,a19)),
% 63.71/63.79 inference(scs_inference,[],[616,886,250,251])).
% 63.71/63.79 cnf(1337,plain,
% 63.71/63.79 (~P9(a2,a17,x13371,x13372,a17,a19,x13372,x13371)),
% 63.71/63.79 inference(scs_inference,[],[616,886,1093,250,251,252])).
% 63.71/63.79 cnf(1342,plain,
% 63.71/63.79 (~P9(a15,a16,a17,a2,a18,a1,a19,a2)),
% 63.71/63.79 inference(scs_inference,[],[1110,250])).
% 63.71/63.79 cnf(1348,plain,
% 63.71/63.79 (~P9(a19,a2,a18,a1,a17,a2,a15,a16)),
% 63.71/63.79 inference(scs_inference,[],[1110,910,1108,250,251,252,249])).
% 63.71/63.79 cnf(1351,plain,
% 63.71/63.79 (~P9(a15,a16,a2,a19,a18,a1,a19,a17)),
% 63.71/63.79 inference(scs_inference,[],[1174,250])).
% 63.71/63.79 cnf(1357,plain,
% 63.71/63.79 (~P9(a19,a17,a18,a1,a2,a19,a15,a16)),
% 63.71/63.79 inference(scs_inference,[],[1174,924,1125,250,251,252,249])).
% 63.71/63.79 cnf(1360,plain,
% 63.71/63.79 (~P9(a15,a16,a19,a17,a18,a1,a17,a2)),
% 63.71/63.79 inference(scs_inference,[],[1190,250])).
% 63.71/63.79 cnf(1362,plain,
% 63.71/63.79 (~P9(x13621,x13622,a2,a17,x13622,x13621,a19,a17)),
% 63.71/63.79 inference(scs_inference,[],[1190,939,250,251])).
% 63.71/63.79 cnf(1366,plain,
% 63.71/63.79 (~P9(a17,a2,a18,a1,a19,a17,a15,a16)),
% 63.71/63.79 inference(scs_inference,[],[1190,939,1157,250,251,252,249])).
% 63.71/63.79 cnf(1369,plain,
% 63.71/63.79 (~P9(a15,a16,a17,a19,a18,a1,a2,a19)),
% 63.71/63.79 inference(scs_inference,[],[1210,250])).
% 63.71/63.79 cnf(1371,plain,
% 63.71/63.79 (~P9(x13711,x13712,a2,a19,x13712,x13711,a17,a19)),
% 63.71/63.79 inference(scs_inference,[],[1210,950,250,251])).
% 63.71/63.79 cnf(1375,plain,
% 63.71/63.79 (~P9(a2,a19,a18,a1,a17,a19,a15,a16)),
% 63.71/63.79 inference(scs_inference,[],[1210,950,1188,250,251,252,249])).
% 63.71/63.79 cnf(1384,plain,
% 63.71/63.79 (~P9(a17,a19,a18,a1,a2,a19,a15,a16)),
% 63.71/63.79 inference(scs_inference,[],[1318,1219,973,1335,250,251,252,249])).
% 63.71/63.79 cnf(1387,plain,
% 63.71/63.79 (~P9(a18,a1,a17,a19,a15,a16,a19,a2)),
% 63.71/63.79 inference(scs_inference,[],[1291,250])).
% 63.71/63.79 cnf(1396,plain,
% 63.71/63.79 (~P9(a18,a1,a19,a17,a15,a16,a19,a2)),
% 63.71/63.79 inference(scs_inference,[],[1300,250])).
% 63.71/63.79 cnf(1402,plain,
% 63.71/63.79 (~P9(a2,a17,a18,a1,a19,a17,a15,a16)),
% 63.71/63.79 inference(scs_inference,[],[1300,1228,1016,1362,250,251,252,249])).
% 63.71/63.79 cnf(1405,plain,
% 63.71/63.79 (~P9(a18,a1,a17,a2,a15,a16,a17,a19)),
% 63.71/63.79 inference(scs_inference,[],[1309,250])).
% 63.71/63.79 cnf(1411,plain,
% 63.71/63.79 (~P9(a17,a2,a18,a1,a2,a19,a15,a16)),
% 63.71/63.79 inference(scs_inference,[],[1309,1127,1025,1371,250,251,252,249])).
% 63.71/63.79 cnf(1414,plain,
% 63.71/63.79 (~P9(a15,a16,a2,a17,a18,a1,a17,a19)),
% 63.71/63.79 inference(scs_inference,[],[1144,250])).
% 63.71/63.79 cnf(1416,plain,
% 63.71/63.79 (~P9(x14161,x14162,a17,a19,x14162,x14161,a2,a17)),
% 63.71/63.79 inference(scs_inference,[],[1144,1034,250,251])).
% 63.71/63.79 cnf(1423,plain,
% 63.71/63.79 (~P9(a15,a16,a17,a19,a18,a1,a19,a2)),
% 63.71/63.79 inference(scs_inference,[],[1159,250])).
% 63.71/63.79 cnf(1425,plain,
% 63.71/63.79 (~P9(x14251,x14252,a17,a2,x14252,x14251,a19,a17)),
% 63.71/63.79 inference(scs_inference,[],[1159,1104,250,251])).
% 63.71/63.79 cnf(1429,plain,
% 63.71/63.79 (~P9(a19,a2,a18,a1,a17,a19,a15,a16)),
% 63.71/63.79 inference(scs_inference,[],[1159,1104,1416,250,251,252,249])).
% 63.71/63.79 cnf(1432,plain,
% 63.71/63.79 (~P9(a15,a16,a2,a17,a18,a1,a19,a17)),
% 63.71/63.79 inference(scs_inference,[],[1201,250])).
% 63.71/63.79 cnf(1434,plain,
% 63.71/63.79 (~P9(x14341,x14342,a19,a17,x14342,x14341,a17,a2)),
% 63.71/63.79 inference(scs_inference,[],[1201,1119,250,251])).
% 63.71/63.79 cnf(1438,plain,
% 63.71/63.79 (~P9(a19,a17,a18,a1,a2,a17,a15,a16)),
% 63.71/63.79 inference(scs_inference,[],[1201,1119,1425,250,251,252,249])).
% 63.71/63.79 cnf(1441,plain,
% 63.71/63.79 (~P9(a19,a17,x14411,x14412,a2,a19,x14412,x14411)),
% 63.71/63.79 inference(scs_inference,[],[1326,250])).
% 63.71/63.79 cnf(1445,plain,
% 63.71/63.79 (~P9(a17,a19,a2,a17,a18,a1,a15,a16)),
% 63.71/63.79 inference(scs_inference,[],[1326,1434,1197,250,252,251])).
% 63.71/63.79 cnf(1452,plain,
% 63.71/63.79 (~P9(a17,a19,x14521,x14522,a2,a19,x14522,x14521)),
% 63.71/63.79 inference(scs_inference,[],[1441,784,250,251])).
% 63.71/63.79 cnf(1454,plain,
% 63.71/63.79 (~P9(a16,a15,a2,a19,a18,a1,a2,a17)),
% 63.71/63.79 inference(scs_inference,[],[1441,784,250,251,252])).
% 63.71/63.79 cnf(1456,plain,
% 63.71/63.79 (~P9(a18,a1,a15,a16,a17,a19,a2,a19)),
% 63.71/63.79 inference(scs_inference,[],[1215,1441,784,250,251,252,249])).
% 63.71/63.79 cnf(1460,plain,
% 63.71/63.79 (~P9(a18,a1,a17,a19,a15,a16,a2,a19)),
% 63.71/63.79 inference(scs_inference,[],[1384,250])).
% 63.71/63.79 cnf(1466,plain,
% 63.71/63.79 (~P9(a18,a1,a15,a16,a19,a17,a2,a19)),
% 63.71/63.79 inference(scs_inference,[],[1168,1384,1411,1452,250,252,251,249])).
% 63.71/63.79 cnf(1469,plain,
% 63.71/63.79 (~P9(a18,a1,a19,a17,a15,a16,a2,a19)),
% 63.71/63.79 inference(scs_inference,[],[1357,250])).
% 63.71/63.79 cnf(1473,plain,
% 63.71/63.79 (~P9(a16,a15,a2,a17,a18,a1,a2,a19)),
% 63.71/63.79 inference(scs_inference,[],[1357,1199,1203,250,251,252])).
% 63.71/63.79 cnf(1475,plain,
% 63.71/63.79 (~P9(a2,a19,x14751,x14752,a17,a19,x14752,x14751)),
% 63.71/63.79 inference(scs_inference,[],[1452,1357,1199,1203,250,251,252,249])).
% 63.71/63.79 cnf(1480,plain,
% 63.71/63.79 (~P9(a2,a19,a17,a19,x14801,x14802,x14802,x14801)),
% 63.71/63.79 inference(scs_inference,[],[1366,1475,250,252])).
% 63.71/63.79 cnf(1491,plain,
% 63.71/63.79 (~P9(a16,a15,a2,a17,a18,a1,a19,a2)),
% 63.71/63.79 inference(scs_inference,[],[1402,1480,1208,250,251,252])).
% 63.71/63.79 cnf(1496,plain,
% 63.71/63.79 (~P9(a18,a1,a2,a19,a15,a16,a17,a19)),
% 63.71/63.79 inference(scs_inference,[],[1375,250])).
% 63.71/63.79 cnf(1498,plain,
% 63.71/63.79 (~P9(a15,a16,a2,a19,a18,a1,a17,a19)),
% 63.71/63.79 inference(scs_inference,[],[1375,1221,250,252])).
% 63.71/63.79 cnf(1502,plain,
% 63.71/63.79 (~P9(a18,a1,a15,a16,a17,a2,a2,a19)),
% 63.71/63.79 inference(scs_inference,[],[771,1375,1206,1221,250,252,251,249])).
% 63.71/63.79 cnf(1511,plain,
% 63.71/63.79 (~P9(a17,a19,x15111,x15112,a2,a17,x15112,x15111)),
% 63.71/63.79 inference(scs_inference,[],[1330,1337,1226,250,251,252,249])).
% 63.71/63.79 cnf(1514,plain,
% 63.71/63.79 (~P9(a18,a1,a15,a16,a2,a19,a17,a19)),
% 63.71/63.79 inference(scs_inference,[],[1212,250])).
% 63.71/63.79 cnf(1516,plain,
% 63.71/63.79 (~P9(a17,a19,a2,a17,x15161,x15162,x15162,x15161)),
% 63.71/63.79 inference(scs_inference,[],[1212,1511,250,252])).
% 63.71/63.79 cnf(1518,plain,
% 63.71/63.79 (~P9(a16,a15,a17,a19,a18,a1,a2,a19)),
% 63.71/63.79 inference(scs_inference,[],[1369,1212,1511,250,252,251])).
% 63.71/63.79 cnf(1520,plain,
% 63.71/63.79 (~P9(a18,a1,a15,a16,a2,a17,a19,a2)),
% 63.71/63.79 inference(scs_inference,[],[1369,1212,1217,1511,250,252,251,249])).
% 63.71/63.79 cnf(1523,plain,
% 63.71/63.79 (~P9(a18,a1,a19,a2,a15,a16,a17,a19)),
% 63.71/63.79 inference(scs_inference,[],[1429,250])).
% 63.71/63.79 cnf(1525,plain,
% 63.71/63.79 (~P9(a1,a18,a2,a19,a15,a16,a17,a19)),
% 63.71/63.79 inference(scs_inference,[],[1429,1496,250,251])).
% 63.71/63.79 cnf(1534,plain,
% 63.71/63.79 (~P9(a16,a15,a17,a2,a18,a1,a17,a19)),
% 63.71/63.79 inference(scs_inference,[],[1235,250,252])).
% 63.71/63.79 cnf(1536,plain,
% 63.71/63.79 (~P9(a1,a18,a15,a16,a2,a19,a17,a19)),
% 63.71/63.79 inference(scs_inference,[],[1514,1235,250,252,251])).
% 63.71/63.79 cnf(1541,plain,
% 63.71/63.79 (~P9(a18,a1,a19,a2,a15,a16,a2,a17)),
% 63.71/63.79 inference(scs_inference,[],[1237,250])).
% 63.71/63.79 cnf(1543,plain,
% 63.71/63.79 (~P9(a19,a17,a2,a17,x15431,x15432,x15432,x15431)),
% 63.71/63.79 inference(scs_inference,[],[1516,1237,250,251])).
% 63.71/63.79 cnf(1550,plain,
% 63.71/63.79 (~P9(a18,a1,a16,a15,a19,a2,a19,a17)),
% 63.71/63.79 inference(scs_inference,[],[1244,250])).
% 63.71/63.79 cnf(1554,plain,
% 63.71/63.79 (~P9(a1,a18,a15,a16,a19,a2,a2,a17)),
% 63.71/63.79 inference(scs_inference,[],[1543,1239,1244,250,252,251])).
% 63.71/63.79 cnf(1561,plain,
% 63.71/63.79 (~P9(a1,a18,a15,a16,a2,a19,a2,a17)),
% 63.71/63.79 inference(scs_inference,[],[1454,1248,250,251])).
% 63.71/63.79 cnf(1574,plain,
% 63.71/63.79 (~P9(a18,a1,a2,a19,a16,a15,a2,a17)),
% 63.71/63.79 inference(scs_inference,[],[1473,1253,1257,250,251,252,249])).
% 63.71/63.79 cnf(1588,plain,
% 63.71/63.79 (~P9(a1,a18,a15,a16,a2,a19,a19,a17)),
% 63.71/63.79 inference(scs_inference,[],[1491,1275,250,251])).
% 63.71/63.79 cnf(1605,plain,
% 63.71/63.79 (~P9(a18,a1,a19,a2,a15,a16,a19,a17)),
% 63.71/63.79 inference(scs_inference,[],[1282,250])).
% 63.71/63.79 cnf(1607,plain,
% 63.71/63.79 (~P9(a1,a18,a19,a2,a15,a16,a2,a17)),
% 63.71/63.79 inference(scs_inference,[],[1282,1541,250,251])).
% 63.71/63.79 cnf(1609,plain,
% 63.71/63.79 (~P9(a16,a15,a19,a2,a18,a1,a17,a19)),
% 63.71/63.79 inference(scs_inference,[],[1282,1541,1289,250,251,252])).
% 63.71/63.79 cnf(1614,plain,
% 63.71/63.79 (~P9(a17,a2,a16,a15,a17,a19,a18,a1)),
% 63.71/63.79 inference(scs_inference,[],[1534,250])).
% 63.71/63.79 cnf(1616,plain,
% 63.71/63.79 (~P9(a1,a18,a19,a2,a15,a16,a19,a17)),
% 63.71/63.79 inference(scs_inference,[],[1534,1605,250,251])).
% 63.71/63.79 cnf(1618,plain,
% 63.71/63.79 (~P9(a16,a15,a17,a19,a18,a1,a2,a17)),
% 63.71/63.79 inference(scs_inference,[],[1534,1605,1298,250,251,252])).
% 63.71/63.79 cnf(1620,plain,
% 63.71/63.79 (~P9(a18,a1,a17,a19,a16,a15,a17,a2)),
% 63.71/63.79 inference(scs_inference,[],[1534,1605,1298,250,251,252,249])).
% 63.71/63.79 cnf(1623,plain,
% 63.71/63.79 (~P9(a18,a1,a2,a19,a15,a16,a19,a17)),
% 63.71/63.79 inference(scs_inference,[],[1273,250])).
% 63.71/63.79 cnf(1625,plain,
% 63.71/63.79 (~P9(a1,a18,a15,a16,a19,a2,a19,a17)),
% 63.71/63.79 inference(scs_inference,[],[1273,1284,250,251])).
% 63.71/63.79 cnf(1632,plain,
% 63.71/63.79 (~P9(a18,a1,a19,a2,a15,a16,a17,a2)),
% 63.71/63.79 inference(scs_inference,[],[1348,250])).
% 63.71/63.79 cnf(1634,plain,
% 63.71/63.79 (~P9(a1,a18,a17,a19,a15,a16,a19,a2)),
% 63.71/63.79 inference(scs_inference,[],[1387,1348,250,251])).
% 63.71/63.79 cnf(1638,plain,
% 63.71/63.79 (~P9(a18,a1,a17,a19,a15,a16,a2,a17)),
% 63.71/63.79 inference(scs_inference,[],[1387,1342,1348,1414,250,251,252,249])).
% 63.71/63.79 cnf(1643,plain,
% 63.71/63.79 (~P9(a1,a18,a19,a17,a15,a16,a19,a2)),
% 63.71/63.79 inference(scs_inference,[],[1396,1438,250,251])).
% 63.71/63.79 cnf(1647,plain,
% 63.71/63.79 (~P9(a18,a1,a15,a16,a17,a19,a2,a17)),
% 63.71/63.79 inference(scs_inference,[],[1396,1632,1438,1445,250,251,252,249])).
% 63.71/63.79 cnf(1652,plain,
% 63.71/63.79 (~P9(a1,a18,a17,a2,a15,a16,a17,a19)),
% 63.71/63.79 inference(scs_inference,[],[1405,1466,250,251])).
% 63.71/63.79 cnf(1654,plain,
% 63.71/63.79 (~P9(a15,a16,a18,a1,a19,a17,a17,a2)),
% 63.71/63.79 inference(scs_inference,[],[1405,1360,1466,250,251,252])).
% 63.71/63.79 cnf(1679,plain,
% 63.71/63.79 (~P9(a16,a15,a2,a19,a18,a1,a19,a17)),
% 63.71/63.79 inference(scs_inference,[],[1351,1647,250,251])).
% 63.71/63.79 cnf(1683,plain,
% 63.71/63.79 (~P9(a18,a1,a2,a19,a16,a15,a17,a19)),
% 63.71/63.79 inference(scs_inference,[],[1351,1647,1502,1518,250,251,252,249])).
% 63.71/63.79 cnf(1692,plain,
% 63.71/63.79 (~P9(a15,a16,a17,a19,a1,a18,a2,a19)),
% 63.71/63.79 inference(scs_inference,[],[1469,1520,1525,1550,250,251,252,249])).
% 63.71/63.79 cnf(1695,plain,
% 63.71/63.79 (~P9(a15,a16,a1,a18,a17,a19,a2,a19)),
% 63.71/63.79 inference(scs_inference,[],[1536,250])).
% 63.71/63.79 cnf(1706,plain,
% 63.71/63.79 (~P9(a16,a15,a17,a19,a18,a1,a19,a2)),
% 63.71/63.79 inference(scs_inference,[],[1423,1620,250,251])).
% 63.71/63.79 cnf(1713,plain,
% 63.71/63.79 (~P9(a19,a2,a1,a18,a2,a17,a15,a16)),
% 63.71/63.79 inference(scs_inference,[],[1607,250])).
% 63.71/63.79 cnf(1717,plain,
% 63.71/63.79 (~P9(a1,a18,a2,a19,a15,a16,a2,a17)),
% 63.71/63.79 inference(scs_inference,[],[1460,1607,1561,250,251,252])).
% 63.71/63.79 cnf(1722,plain,
% 63.71/63.79 (~P9(a15,a16,a1,a18,a2,a17,a19,a2)),
% 63.71/63.79 inference(scs_inference,[],[1554,250])).
% 63.71/63.79 cnf(1732,plain,
% 63.71/63.79 (~P9(a1,a18,a2,a19,a15,a16,a19,a17)),
% 63.71/63.79 inference(scs_inference,[],[1623,251])).
% 63.71/63.79 cnf(1747,plain,
% 63.71/63.79 (~P9(a15,a16,a2,a17,a1,a18,a2,a19)),
% 63.71/63.79 inference(scs_inference,[],[1638,1717,1574,250,251,252,249])).
% 63.71/63.79 cnf(1750,plain,
% 63.71/63.79 (~P9(a1,a18,a19,a2,a15,a16,a17,a19)),
% 63.71/63.79 inference(scs_inference,[],[1523,251])).
% 63.71/63.79 cnf(1768,plain,
% 63.71/63.79 (~P9(a16,a15,a2,a19,a18,a1,a17,a19)),
% 63.71/63.79 inference(scs_inference,[],[1498,251])).
% 63.71/63.79 cnf(1788,plain,
% 63.71/63.79 (~P9(a17,a2,a17,a19,a16,a15,a18,a1)),
% 63.71/63.79 inference(scs_inference,[],[1732,1614,249,252])).
% 63.71/63.79 cnf(1797,plain,
% 63.71/63.79 (~P9(a1,a18,a15,a16,a17,a19,a19,a2)),
% 63.71/63.79 inference(scs_inference,[],[1588,1634,249,252])).
% 63.71/63.79 cnf(1801,plain,
% 63.71/63.79 (~P9(a1,a18,a15,a16,a17,a19,a2,a19)),
% 63.71/63.79 inference(scs_inference,[],[1456,1588,1634,249,252,250,251])).
% 63.71/63.79 cnf(1804,plain,
% 63.71/63.79 (~P9(a15,a16,a19,a17,a1,a18,a19,a2)),
% 63.71/63.79 inference(scs_inference,[],[1616,249])).
% 63.71/63.79 cnf(1806,plain,
% 63.71/63.79 (~P9(a1,a18,a15,a16,a19,a17,a19,a2)),
% 63.71/63.79 inference(scs_inference,[],[1616,1643,249,252])).
% 63.71/63.79 cnf(1808,plain,
% 63.71/63.79 (~P9(a16,a15,a18,a1,a19,a17,a17,a2)),
% 63.71/63.79 inference(scs_inference,[],[1654,1616,1643,249,252,251])).
% 63.71/63.79 cnf(1815,plain,
% 63.71/63.79 (~P9(a1,a18,a15,a16,a17,a2,a17,a19)),
% 63.71/63.79 inference(scs_inference,[],[1625,1652,249,252])).
% 63.71/63.79 cnf(1817,plain,
% 63.71/63.79 (~P9(a15,a16,a1,a18,a19,a17,a19,a2)),
% 63.71/63.79 inference(scs_inference,[],[1625,1652,249,252,250])).
% 63.71/63.79 cnf(1840,plain,
% 63.71/63.79 (~P9(a18,a1,a2,a17,a16,a15,a17,a19)),
% 63.71/63.79 inference(scs_inference,[],[1618,249])).
% 63.71/63.79 cnf(1846,plain,
% 63.71/63.79 (~P9(a17,a19,a16,a15,a2,a17,a18,a1)),
% 63.71/63.79 inference(scs_inference,[],[1432,1618,1683,249,252,251,250])).
% 63.71/63.79 cnf(1869,plain,
% 63.71/63.79 (~P9(a17,a2,a17,a19,a1,a18,a15,a16)),
% 63.71/63.79 inference(scs_inference,[],[1815,249])).
% 63.71/63.79 cnf(1893,plain,
% 63.71/63.79 (~P9(a16,a15,a17,a19,a1,a18,a2,a19)),
% 63.71/63.79 inference(scs_inference,[],[1679,1692,1747,252,249,250,251])).
% 63.71/63.79 cnf(1896,plain,
% 63.71/63.79 (~P9(a17,a19,a2,a19,a15,a16,a1,a18)),
% 63.71/63.79 inference(scs_inference,[],[1695,249])).
% 63.71/63.79 cnf(1900,plain,
% 63.71/63.79 (~P9(a16,a15,a1,a18,a17,a19,a2,a19)),
% 63.71/63.79 inference(scs_inference,[],[1695,1750,249,252,251])).
% 63.71/63.79 cnf(1914,plain,
% 63.71/63.79 (~P9(a2,a17,a15,a16,a19,a2,a1,a18)),
% 63.71/63.79 inference(scs_inference,[],[1713,249])).
% 63.71/63.79 cnf(1934,plain,
% 63.71/63.79 (~P9(a16,a15,a18,a1,a2,a19,a17,a19)),
% 63.71/63.79 inference(scs_inference,[],[1801,1768,249,252])).
% 63.71/63.79 cnf(1938,plain,
% 63.71/63.79 (~P9(a15,a16,a1,a18,a2,a19,a17,a19)),
% 63.71/63.79 inference(scs_inference,[],[1722,1801,1768,249,252,251,250])).
% 63.71/63.79 cnf(1956,plain,
% 63.71/63.79 (~P9(a17,a19,a16,a15,a19,a2,a18,a1)),
% 63.71/63.79 inference(scs_inference,[],[1706,1914,1808,249,252,251,250])).
% 63.71/63.79 cnf(1997,plain,
% 63.71/63.79 (~P9(a19,a17,a19,a2,a15,a16,a1,a18)),
% 63.71/63.79 inference(scs_inference,[],[1817,1840,252,249])).
% 63.71/63.79 cnf(1999,plain,
% 63.71/63.79 (~P9(a19,a17,a15,a16,a19,a2,a1,a18)),
% 63.71/63.79 inference(scs_inference,[],[1817,1804,1840,252,249,250])).
% 63.71/63.79 cnf(2010,plain,
% 63.71/63.79 (~P9(a19,a2,a16,a15,a17,a19,a18,a1)),
% 63.71/63.79 inference(scs_inference,[],[1609,1846,249,252,250])).
% 63.71/63.79 cnf(2012,plain,
% 63.71/63.79 (~P9(a2,a17,a17,a19,a16,a15,a18,a1)),
% 63.71/63.79 inference(scs_inference,[],[1609,1788,1846,249,252,250,251])).
% 63.71/63.79 cnf(2021,plain,
% 63.71/63.79 (~P9(a17,a19,a19,a2,a15,a16,a1,a18)),
% 63.71/63.79 inference(scs_inference,[],[1797,1896,1997,252,249,250,251])).
% 63.71/63.79 cnf(2024,plain,
% 63.71/63.79 (~P9(a19,a17,a19,a2,a1,a18,a15,a16)),
% 63.71/63.79 inference(scs_inference,[],[1806,249])).
% 63.71/63.79 cnf(2030,plain,
% 63.71/63.79 (~P9(a17,a19,a15,a16,a19,a2,a1,a18)),
% 63.71/63.79 inference(scs_inference,[],[1806,1999,1869,249,252,250,251])).
% 63.71/63.79 cnf(2082,plain,
% 63.71/63.79 (~P9(a17,a19,a16,a15,a2,a19,a1,a18)),
% 63.71/63.79 inference(scs_inference,[],[1893,2010,249,252,250])).
% 63.71/63.79 cnf(2089,plain,
% 63.71/63.79 (~P9(a17,a19,a2,a19,a16,a15,a1,a18)),
% 63.71/63.79 inference(scs_inference,[],[1900,2012,252,249])).
% 63.71/63.79 cnf(2125,plain,
% 63.71/63.79 (~P9(a2,a19,a17,a19,a15,a16,a1,a18)),
% 63.71/63.79 inference(scs_inference,[],[1938,2024,252,249])).
% 63.71/63.79 cnf(2203,plain,
% 63.71/63.79 (~P9(a19,a17,a16,a15,a19,a2,a18,a1)),
% 63.71/63.79 inference(scs_inference,[],[1956,2030,2021,2125,249,252,250,251])).
% 63.71/63.79 cnf(2237,plain,
% 63.71/63.79 (~P9(a2,a19,a17,a19,a1,a18,a16,a15)),
% 63.71/63.79 inference(scs_inference,[],[2082,2089,2203,249,252,250])).
% 63.71/63.79 cnf(2902,plain,
% 63.71/63.79 (P10(f7(a2,a15,a16,a17),a2,a2,a17)),
% 63.71/63.79 inference(scs_inference,[],[145,184])).
% 63.71/63.79 cnf(2906,plain,
% 63.71/63.79 (P1(a2,a1,a15)),
% 63.71/63.79 inference(scs_inference,[],[142,145,144,184,222,148])).
% 63.71/63.79 cnf(2908,plain,
% 63.71/63.79 (P1(a1,a15,a2)),
% 63.71/63.79 inference(scs_inference,[],[142,145,144,184,222,148,149])).
% 63.71/63.79 cnf(2910,plain,
% 63.71/63.79 (P3(a15,a16,a1,a18)),
% 63.71/63.79 inference(scs_inference,[],[142,145,144,184,222,148,149,161])).
% 63.71/63.79 cnf(2912,plain,
% 63.71/63.79 (P3(a18,a1,a15,a16)),
% 63.71/63.79 inference(scs_inference,[],[142,145,144,184,222,148,149,161,160])).
% 63.71/63.79 cnf(2914,plain,
% 63.71/63.79 (P9(a15,a16,a18,a1,x29141,x29142,x29141,x29142)),
% 63.71/63.79 inference(scs_inference,[],[142,145,144,184,222,148,149,161,160,252])).
% 63.71/63.79 cnf(2916,plain,
% 63.71/63.79 (P9(a16,a15,x29161,x29162,a18,a1,x29161,x29162)),
% 63.71/63.79 inference(scs_inference,[],[142,145,144,184,222,148,149,161,160,252,251])).
% 63.71/63.79 cnf(2918,plain,
% 63.71/63.79 (P9(x29181,x29182,a15,a16,x29181,x29182,a18,a1)),
% 63.71/63.79 inference(scs_inference,[],[142,145,144,184,222,148,149,161,160,252,251,250])).
% 63.71/63.79 cnf(2926,plain,
% 63.71/63.79 (~E(a2,a19)),
% 63.71/63.79 inference(scs_inference,[],[142,441,532,1371,145,144,184,222,148,149,161,160,252,251,250,249,226,107,108])).
% 63.71/63.79 cnf(2927,plain,
% 63.71/63.79 (P3(a15,a16,a15,a16)),
% 63.71/63.79 inference(scs_inference,[],[142,441,532,1371,145,144,184,222,148,149,161,160,252,251,250,249,226,107,108,176])).
% 63.71/63.79 cnf(2929,plain,
% 63.71/63.79 (P1(a15,a15,a2)),
% 63.71/63.79 inference(scs_inference,[],[142,441,532,1371,145,144,184,222,148,149,161,160,252,251,250,249,226,107,108,176,152])).
% 63.71/63.79 cnf(2932,plain,
% 63.71/63.79 (P10(a2,a17,f7(a2,a15,a16,a17),a2)),
% 63.71/63.79 inference(scs_inference,[],[142,441,532,1371,145,144,184,222,148,149,161,160,252,251,250,249,226,107,108,176,152,2,162])).
% 63.71/63.79 cnf(2934,plain,
% 63.71/63.79 (P10(f7(a2,a15,a16,a17),a2,a17,a2)),
% 63.71/63.79 inference(scs_inference,[],[142,441,532,1371,145,144,184,222,148,149,161,160,252,251,250,249,226,107,108,176,152,2,162,163])).
% 63.71/63.79 cnf(2936,plain,
% 63.71/63.79 (P3(a18,a1,a18,a1)),
% 63.71/63.79 inference(scs_inference,[],[142,441,532,1371,145,144,184,222,148,149,161,160,252,251,250,249,226,107,108,176,152,2,162,163,293])).
% 63.71/63.79 cnf(2938,plain,
% 63.71/63.79 (P1(a15,a16,a16)),
% 63.71/63.79 inference(scs_inference,[],[142,441,532,1371,145,144,184,222,148,149,161,160,252,251,250,249,226,107,108,176,152,2,162,163,293,157])).
% 63.71/63.79 cnf(2940,plain,
% 63.71/63.79 (P3(a16,a15,a18,a1)),
% 63.71/63.79 inference(scs_inference,[],[142,441,532,1371,145,144,184,222,148,149,161,160,252,251,250,249,226,107,108,176,152,2,162,163,293,157,230])).
% 63.71/63.79 cnf(2944,plain,
% 63.71/63.79 (~P10(a2,a19,f7(a2,a15,a16,a17),a2)),
% 63.71/63.79 inference(scs_inference,[],[142,563,267,441,532,1371,145,144,184,222,148,149,161,160,252,251,250,249,226,107,108,176,152,2,162,163,293,157,230,154,177])).
% 63.71/63.79 cnf(2947,plain,
% 63.71/63.79 (P10(f7(a2,a1,a18,a19),a2,a2,a19)),
% 63.71/63.79 inference(scs_inference,[],[146,184])).
% 63.71/63.79 cnf(2949,plain,
% 63.71/63.79 (P10(a17,a2,f7(a2,a15,a16,a17),a2)),
% 63.71/63.79 inference(scs_inference,[],[2934,146,184,162])).
% 63.71/63.79 cnf(2951,plain,
% 63.71/63.79 (P10(a2,a17,a2,f7(a2,a15,a16,a17))),
% 63.71/63.79 inference(scs_inference,[],[2934,2932,146,184,162,163])).
% 63.71/63.79 cnf(2954,plain,
% 63.71/63.79 (P9(a15,a16,x29541,x29542,a1,a18,x29541,x29542)),
% 63.71/63.79 inference(scs_inference,[],[2926,2910,2934,2932,146,184,162,163,2,222])).
% 63.71/63.79 cnf(2956,plain,
% 63.71/63.79 (P1(a2,a15,a1)),
% 63.71/63.79 inference(scs_inference,[],[2926,2906,2910,2934,2932,146,184,162,163,2,222,149])).
% 63.71/63.79 cnf(2968,plain,
% 63.71/63.79 (P9(x29681,x29682,x29681,x29682,a15,a16,a18,a1)),
% 63.71/63.79 inference(scs_inference,[],[2926,2906,2914,2918,2908,2910,2912,2936,2934,2932,146,184,162,163,2,222,149,148,157,161,251,160,252])).
% 63.71/63.79 cnf(2974,plain,
% 63.71/63.79 (~P9(a2,a19,f7(a2,a15,a16,a17),a2,f7(a2,a15,a16,a17),a2,a17,a2)),
% 63.71/63.79 inference(scs_inference,[],[2926,2906,2914,2916,2918,2908,2910,2912,2936,2944,2934,2932,146,184,162,163,2,222,149,148,157,161,251,160,252,250,249,238])).
% 63.71/63.79 cnf(2979,plain,
% 63.71/63.79 (P3(f7(a2,a15,a16,a17),a2,f7(a2,a15,a16,a17),a2)),
% 63.71/63.79 inference(scs_inference,[],[1934,2926,2906,2914,2916,2918,2908,2910,2912,2936,2944,2934,2932,508,146,184,162,163,2,222,149,148,157,161,251,160,252,250,249,238,111,112,177])).
% 63.71/63.79 cnf(2990,plain,
% 63.71/63.79 (P10(a17,a2,a2,f7(a2,a15,a16,a17))),
% 63.71/63.79 inference(scs_inference,[],[2949,163])).
% 63.71/63.79 cnf(2994,plain,
% 63.71/63.79 (P9(a15,a16,x29941,x29942,a15,a16,x29941,x29942)),
% 63.71/63.79 inference(scs_inference,[],[2927,2949,2951,163,162,222])).
% 63.71/63.79 cnf(2996,plain,
% 63.71/63.79 (P1(a16,a15,a16)),
% 63.71/63.79 inference(scs_inference,[],[2938,2927,2949,2951,163,162,222,148])).
% 63.71/63.79 cnf(3004,plain,
% 63.71/63.79 (P9(a15,a16,a1,a18,x30041,x30042,x30041,x30042)),
% 63.71/63.79 inference(scs_inference,[],[2940,2938,2954,2927,2929,2979,2949,2951,163,162,222,148,149,157,161,252])).
% 63.71/63.79 cnf(3008,plain,
% 63.71/63.79 (P3(a1,a18,a16,a15)),
% 63.71/63.79 inference(scs_inference,[],[2940,2938,2954,2927,2929,2979,2949,2951,163,162,222,148,149,157,161,252,251,160])).
% 63.71/63.79 cnf(3014,plain,
% 63.71/63.79 (P1(f4(a2,a2,a17),a17,a2)),
% 63.71/63.79 inference(scs_inference,[],[2940,2938,2954,2927,2929,2979,2949,2951,163,162,222,148,149,157,161,252,251,160,250,249,174])).
% 63.71/63.79 cnf(3016,plain,
% 63.71/63.79 (P1(f5(a2,a2,a17),a17,a2)),
% 63.71/63.79 inference(scs_inference,[],[2940,2938,2954,2927,2929,2979,2949,2951,163,162,222,148,149,157,161,252,251,160,250,249,174,175])).
% 63.71/63.79 cnf(3020,plain,
% 63.71/63.79 (P10(a2,f4(a2,a2,a17),a17,a2)),
% 63.71/63.79 inference(scs_inference,[],[2940,2938,2954,2927,2929,2979,2949,2951,163,162,222,148,149,157,161,252,251,160,250,249,174,175,233,186])).
% 63.71/63.79 cnf(3022,plain,
% 63.71/63.79 (P10(a2,f5(a2,a2,a17),a17,a2)),
% 63.71/63.79 inference(scs_inference,[],[2940,2938,2954,2927,2929,2979,2949,2951,163,162,222,148,149,157,161,252,251,160,250,249,174,175,233,186,187])).
% 63.71/63.79 cnf(3024,plain,
% 63.71/63.79 (P6(a2,a15,a15,a15)),
% 63.71/63.79 inference(scs_inference,[],[2940,2938,2954,2927,2929,2979,2949,2951,163,162,222,148,149,157,161,252,251,160,250,249,174,175,233,186,187,182])).
% 63.71/63.79 cnf(3026,plain,
% 63.71/63.79 (P9(a2,f7(a2,a15,a16,a17),a2,a15,a16,a2,a16,a15)),
% 63.71/63.79 inference(scs_inference,[],[2940,2938,2954,2927,2929,2979,2949,2951,145,163,162,222,148,149,157,161,252,251,160,250,249,174,175,233,186,187,182,226])).
% 63.71/63.79 cnf(3030,plain,
% 63.71/63.79 (P3(x30301,x30302,x30301,x30302)),
% 63.71/63.79 inference(scs_inference,[],[2940,2938,2954,2968,2927,2929,2902,2979,2949,2951,504,145,144,163,162,222,148,149,157,161,252,251,160,250,249,174,175,233,186,187,182,226,177,237])).
% 63.71/63.79 cnf(3035,plain,
% 63.71/63.79 (P1(a15,a15,f13(a16,a16,a16,a16,a15,a15))),
% 63.71/63.79 inference(scs_inference,[],[2940,2938,2954,2968,2927,2929,2902,2979,2949,2951,504,335,145,144,163,162,222,148,149,157,161,252,251,160,250,249,174,175,233,186,187,182,226,177,237,88,225,203])).
% 63.71/63.79 cnf(3039,plain,
% 63.71/63.79 (P6(a2,a16,a15,a15)),
% 63.71/63.79 inference(scs_inference,[],[2940,2938,2954,2968,2927,2929,2902,2979,2949,2951,504,335,145,144,163,162,222,148,149,157,161,252,251,160,250,249,174,175,233,186,187,182,226,177,237,88,225,203,204,166])).
% 63.71/63.79 cnf(3041,plain,
% 63.71/63.79 (P6(a16,a15,a2,a15)),
% 63.71/63.79 inference(scs_inference,[],[2940,2938,2954,2968,2927,2929,2902,2979,2949,2951,504,335,145,144,163,162,222,148,149,157,161,252,251,160,250,249,174,175,233,186,187,182,226,177,237,88,225,203,204,166,167])).
% 63.71/63.79 cnf(3043,plain,
% 63.71/63.79 (P6(a16,a15,a15,a2)),
% 63.71/63.79 inference(scs_inference,[],[2940,2938,2954,2968,2927,2929,2902,2979,2949,2951,504,335,145,144,163,162,222,148,149,157,161,252,251,160,250,249,174,175,233,186,187,182,226,177,237,88,225,203,204,166,167,168])).
% 63.71/63.79 cnf(3047,plain,
% 63.71/63.79 (P8(a16,a16,a15,a16,a16,a16,a15,a16)),
% 63.71/63.79 inference(scs_inference,[],[2940,2938,2954,2968,2927,2929,2902,2979,2949,2951,504,335,145,144,163,162,222,148,149,157,161,252,251,160,250,249,174,175,233,186,187,182,226,177,237,88,225,203,204,166,167,168,221,254])).
% 63.71/63.79 cnf(3049,plain,
% 63.71/63.79 (P8(a16,a15,a16,a16,a15,a16,a16,a16)),
% 63.71/63.79 inference(scs_inference,[],[2940,2938,2954,2968,2927,2929,2902,2979,2949,2951,504,335,145,144,163,162,222,148,149,157,161,252,251,160,250,249,174,175,233,186,187,182,226,177,237,88,225,203,204,166,167,168,221,254,255])).
% 63.71/63.79 cnf(3051,plain,
% 63.71/63.79 (P8(a15,a16,a15,a16,a16,a16,a16,a16)),
% 63.71/63.79 inference(scs_inference,[],[2940,2938,2954,2968,2927,2929,2902,2979,2949,2951,504,335,145,144,163,162,222,148,149,157,161,252,251,160,250,249,174,175,233,186,187,182,226,177,237,88,225,203,204,166,167,168,221,254,255,256])).
% 63.71/63.79 cnf(3056,plain,
% 63.71/63.79 (P8(a15,a16,a16,a16,a16,a15,a16,a16)),
% 63.71/63.79 inference(scs_inference,[],[2940,2938,2954,2968,2927,2929,2902,2979,2949,2951,504,335,145,144,163,162,222,148,149,157,161,252,251,160,250,249,174,175,233,186,187,182,226,177,237,88,225,203,204,166,167,168,221,254,255,256,2,169,253])).
% 63.71/63.79 cnf(3064,plain,
% 63.71/63.79 (P6(a15,a2,a15,a15)),
% 63.71/63.79 inference(scs_inference,[],[3024,3047,3049,254,256,166])).
% 63.71/63.79 cnf(3066,plain,
% 63.71/63.79 (P6(a2,a15,a16,a15)),
% 63.71/63.79 inference(scs_inference,[],[3024,3039,3047,3049,254,256,166,167])).
% 63.71/63.79 cnf(3070,plain,
% 63.71/63.79 (P6(a2,a15,a15,a16)),
% 63.71/63.79 inference(scs_inference,[],[3024,3039,3047,3049,254,256,166,167,221,168])).
% 63.71/63.79 cnf(3072,plain,
% 63.71/63.79 (P8(a16,a15,a15,a16,a16,a16,a16,a16)),
% 63.71/63.79 inference(scs_inference,[],[3024,3039,3047,3049,3051,254,256,166,167,221,168,255])).
% 63.71/63.79 cnf(3080,plain,
% 63.71/63.79 (P9(x30801,x30802,x30803,x30804,x30801,x30802,x30803,x30804)),
% 63.71/63.79 inference(scs_inference,[],[3030,3024,3039,3047,3049,3051,2947,254,256,166,167,221,168,255,253,162,163,222])).
% 63.71/63.79 cnf(3086,plain,
% 63.71/63.79 (P1(x30861,x30862,x30862)),
% 63.71/63.79 inference(scs_inference,[],[3030,2956,2996,3024,3039,3047,3049,3051,2947,254,256,166,167,221,168,255,253,162,163,222,148,149,157])).
% 63.71/63.79 cnf(3088,plain,
% 63.71/63.79 (P3(x30881,x30882,x30882,x30881)),
% 63.71/63.79 inference(scs_inference,[],[3030,2956,2996,3024,3039,3047,3049,3051,2947,254,256,166,167,221,168,255,253,162,163,222,148,149,157,161])).
% 63.71/63.79 cnf(3090,plain,
% 63.71/63.79 (P9(a15,a16,a15,a16,x30901,x30902,x30901,x30902)),
% 63.71/63.79 inference(scs_inference,[],[3030,2994,2956,2996,3024,3039,3047,3049,3051,2947,254,256,166,167,221,168,255,253,162,163,222,148,149,157,161,252])).
% 63.71/63.79 cnf(3092,plain,
% 63.71/63.79 (P9(a16,a15,x30921,x30922,a15,a16,x30921,x30922)),
% 63.71/63.79 inference(scs_inference,[],[3030,2994,2956,2996,3024,3039,3047,3049,3051,2947,254,256,166,167,221,168,255,253,162,163,222,148,149,157,161,252,251])).
% 63.71/63.79 cnf(3094,plain,
% 63.71/63.79 (P9(a1,a18,a15,a16,x30941,x30942,x30941,x30942)),
% 63.71/63.79 inference(scs_inference,[],[3030,2994,3004,2956,2996,3024,3039,3047,3049,3051,2947,254,256,166,167,221,168,255,253,162,163,222,148,149,157,161,252,251,250])).
% 63.71/63.79 cnf(3099,plain,
% 63.71/63.79 (P6(a19,a17,a19,f25(a2,a17,a19,a19))),
% 63.71/63.79 inference(scs_inference,[],[3030,2994,3004,2956,2996,3024,3039,3047,3049,3051,2947,2944,263,254,256,166,167,221,168,255,253,162,163,222,148,149,157,161,252,251,250,249,136,241])).
% 63.71/63.79 cnf(3101,plain,
% 63.71/63.79 (P8(a15,a16,a15,a16,a15,a16,a15,a16)),
% 63.71/63.79 inference(scs_inference,[],[3030,2994,3004,2956,2996,3024,3039,3047,3049,3051,2947,2944,263,254,256,166,167,221,168,255,253,162,163,222,148,149,157,161,252,251,250,249,136,241,260])).
% 63.71/63.79 cnf(3120,plain,
% 63.71/63.79 (~P3(a2,f25(a2,a17,a19,a19),a17,f25(a2,a17,a19,a19))),
% 63.71/63.79 inference(scs_inference,[],[3030,2994,3004,2956,2996,3024,3039,3047,3049,3051,2947,2990,3035,2237,1362,2944,551,407,263,254,256,166,167,221,168,255,253,162,163,222,148,149,157,161,252,251,250,249,136,241,260,257,259,226,233,177,2,170,179,237])).
% 63.71/63.79 cnf(3124,plain,
% 63.71/63.79 (P6(a15,a16,a2,a15)),
% 63.71/63.79 inference(scs_inference,[],[3041,166])).
% 63.71/63.79 cnf(3130,plain,
% 63.71/63.79 (P8(a15,a16,a16,a15,a16,a16,a16,a16)),
% 63.71/63.79 inference(scs_inference,[],[3041,3056,3099,166,168,255,256])).
% 63.71/63.79 cnf(3138,plain,
% 63.71/63.79 (P8(a16,a16,a16,a15,a16,a16,a16,a15)),
% 63.71/63.79 inference(scs_inference,[],[3041,3056,3064,3072,3099,166,168,255,256,221,253,167,254])).
% 63.71/63.79 cnf(3140,plain,
% 63.71/63.79 (P10(a17,a2,a2,f4(a2,a2,a17))),
% 63.71/63.79 inference(scs_inference,[],[3041,3056,3064,3072,3020,3099,166,168,255,256,221,253,167,254,162])).
% 63.71/63.79 cnf(3142,plain,
% 63.71/63.79 (P9(x31421,x31422,x31423,x31424,x31422,x31421,x31423,x31424)),
% 63.71/63.79 inference(scs_inference,[],[3088,3041,3056,3064,3072,3020,3099,166,168,255,256,221,253,167,254,162,222])).
% 63.71/63.79 cnf(3148,plain,
% 63.71/63.79 (P1(x31481,x31482,x31481)),
% 63.71/63.79 inference(scs_inference,[],[3088,3086,3041,3056,3064,3072,3020,3014,3099,166,168,255,256,221,253,167,254,162,222,163,149,148])).
% 63.71/63.79 cnf(3150,plain,
% 63.71/63.79 (P9(x31501,x31502,x31501,x31502,x31503,x31504,x31503,x31504)),
% 63.71/63.79 inference(scs_inference,[],[3080,3088,3086,3041,3056,3064,3072,3020,3014,3099,166,168,255,256,221,253,167,254,162,222,163,149,148,252])).
% 63.71/63.79 cnf(3152,plain,
% 63.71/63.79 (P9(a16,a15,a15,a16,x31521,x31522,x31521,x31522)),
% 63.71/63.79 inference(scs_inference,[],[3080,3088,3086,3041,3056,3090,3064,3072,3020,3014,3099,166,168,255,256,221,253,167,254,162,222,163,149,148,252,251])).
% 63.71/63.79 cnf(3154,plain,
% 63.71/63.79 (P9(x31541,x31542,a16,a15,x31541,x31542,a15,a16)),
% 63.71/63.79 inference(scs_inference,[],[3080,3088,3086,3041,3056,3090,3092,3064,3072,3020,3014,3099,166,168,255,256,221,253,167,254,162,222,163,149,148,252,251,250])).
% 63.71/63.79 cnf(3159,plain,
% 63.71/63.79 (P9(x31591,x31592,x31593,x31594,x31591,x31592,x31593,x31594)),
% 63.71/63.79 inference(rename_variables,[],[3080])).
% 63.71/63.79 cnf(3161,plain,
% 63.71/63.79 (P9(a17,a2,a19,a2,a17,f25(a17,a19,a2,a2),a19,f25(a17,a19,a2,a2))),
% 63.71/63.79 inference(scs_inference,[],[3080,3159,3088,3086,3041,3056,3090,3092,3094,3064,3072,3020,3014,3099,359,166,168,255,256,221,253,167,254,162,222,163,149,148,252,251,250,249,241,257])).
% 63.71/63.79 cnf(3162,plain,
% 63.71/63.79 (P9(x31621,x31622,x31623,x31624,x31621,x31622,x31623,x31624)),
% 63.71/63.79 inference(rename_variables,[],[3080])).
% 63.71/63.79 cnf(3166,plain,
% 63.71/63.79 (P6(x31661,x31662,x31662,x31662)),
% 63.71/63.79 inference(scs_inference,[],[3080,3159,3162,3088,3086,3041,3056,3090,3092,3094,3064,3072,3020,3014,3099,359,166,168,255,256,221,253,167,254,162,222,163,149,148,252,251,250,249,241,257,238,233])).
% 63.71/63.79 cnf(3193,plain,
% 63.71/63.79 (P9(x31931,x31932,x31931,x31932,x31933,x31934,x31933,x31934)),
% 63.71/63.79 inference(rename_variables,[],[3150])).
% 63.71/63.79 cnf(3196,plain,
% 63.71/63.79 (P9(x31961,x31962,x31961,x31962,x31963,x31964,x31963,x31964)),
% 63.71/63.79 inference(rename_variables,[],[3150])).
% 63.71/63.79 cnf(3198,plain,
% 63.71/63.79 (P8(a16,a15,a16,a15,a16,a16,a16,a16)),
% 63.71/63.79 inference(scs_inference,[],[3150,3193,3130,425,520,255])).
% 63.71/63.79 cnf(3206,plain,
% 63.71/63.79 (P6(x32061,x32062,x32061,x32061)),
% 63.71/63.79 inference(scs_inference,[],[3150,3193,3166,3130,3124,425,520,255,253,168,167,166])).
% 63.71/63.79 cnf(3208,plain,
% 63.71/63.79 (P9(a15,a16,a15,a15,a2,a16,a2,a15)),
% 63.71/63.79 inference(scs_inference,[],[3150,3193,3166,3043,3130,3124,425,520,255,253,168,167,166,221])).
% 63.71/63.79 cnf(3216,plain,
% 63.71/63.79 (P9(a1,a18,x32161,x32162,a16,a15,x32161,x32162)),
% 63.71/63.79 inference(scs_inference,[],[3150,3193,3166,3043,3130,3124,3138,3022,3008,425,520,255,253,168,167,166,221,256,163,162,222])).
% 63.71/63.79 cnf(3220,plain,
% 63.71/63.79 (P1(x32201,x32201,x32202)),
% 63.71/63.79 inference(scs_inference,[],[3150,3193,3166,3148,3043,3130,3124,3138,3022,3016,3008,425,520,255,253,168,167,166,221,256,163,162,222,148,149])).
% 63.71/63.79 cnf(3222,plain,
% 63.71/63.79 (P9(x32221,x32222,x32222,x32221,x32223,x32224,x32223,x32224)),
% 63.71/63.79 inference(scs_inference,[],[3142,3150,3193,3166,3148,3043,3130,3124,3138,3022,3016,3008,425,520,255,253,168,167,166,221,256,163,162,222,148,149,252])).
% 63.71/63.79 cnf(3226,plain,
% 63.71/63.79 (P9(x32261,x32262,x32263,x32264,x32261,x32262,x32264,x32263)),
% 63.71/63.79 inference(scs_inference,[],[3142,3150,3193,3166,3148,3043,3130,3154,3124,3138,3022,3016,3008,425,520,255,253,168,167,166,221,256,163,162,222,148,149,252,251,250])).
% 63.71/63.79 cnf(3231,plain,
% 63.71/63.79 (P9(x32311,x32312,x32313,x32314,x32312,x32311,x32313,x32314)),
% 63.71/63.79 inference(rename_variables,[],[3142])).
% 63.71/63.79 cnf(3234,plain,
% 63.71/63.79 (P9(x32341,x32342,x32343,x32344,x32341,x32342,x32343,x32344)),
% 63.71/63.79 inference(rename_variables,[],[3080])).
% 63.71/63.79 cnf(3239,plain,
% 63.71/63.79 (P6(a15,a15,a1,a2)),
% 63.71/63.79 inference(scs_inference,[],[142,3142,3150,3193,3196,3166,3148,3043,3130,3152,3154,3124,3138,3022,3016,2974,3008,3080,3234,335,425,520,255,253,168,167,166,221,256,163,162,222,148,149,252,251,250,249,259,257,241,233])).
% 63.71/63.79 cnf(3244,plain,
% 63.71/63.79 (P10(f5(a2,a2,a17),a2,a17,a2)),
% 63.71/63.79 inference(scs_inference,[],[142,3142,3231,3150,3193,3196,3166,3148,3043,3130,3152,3154,3124,3138,3022,3016,3140,2974,3008,3080,3234,335,145,425,520,255,253,168,167,166,221,256,163,162,222,148,149,252,251,250,249,259,257,241,233,226,238])).
% 63.71/63.79 cnf(3245,plain,
% 63.71/63.79 (P9(x32451,x32452,x32453,x32454,x32452,x32451,x32453,x32454)),
% 63.71/63.79 inference(rename_variables,[],[3142])).
% 63.71/63.79 cnf(3247,plain,
% 63.71/63.79 (P3(a2,f5(a2,a2,a17),a2,f4(a2,a2,a17))),
% 63.71/63.79 inference(scs_inference,[],[142,3142,3231,3150,3193,3196,3166,3148,3043,3130,3152,3154,3124,3138,3022,3016,3140,2974,3008,3080,3234,335,145,425,520,255,253,168,167,166,221,256,163,162,222,148,149,252,251,250,249,259,257,241,233,226,238,177])).
% 63.71/63.79 cnf(3249,plain,
% 63.71/63.79 (P3(a2,f5(a2,a2,a17),f4(a2,a2,a17),a2)),
% 63.71/63.79 inference(scs_inference,[],[142,3142,3231,3150,3193,3196,3166,3148,3043,3130,3152,3154,3124,3138,3022,3016,3140,2974,3008,3080,3234,3088,335,145,425,520,255,253,168,167,166,221,256,163,162,222,148,149,252,251,250,249,259,257,241,233,226,238,177,176])).
% 63.71/63.79 cnf(3250,plain,
% 63.71/63.79 (P3(x32501,x32502,x32502,x32501)),
% 63.71/63.79 inference(rename_variables,[],[3088])).
% 63.71/63.79 cnf(3252,plain,
% 63.71/63.79 (P5(x32521,x32521,x32521,x32521)),
% 63.71/63.79 inference(scs_inference,[],[142,3142,3231,3245,3150,3193,3196,3166,3148,3043,3130,3152,3154,3124,3138,3022,3016,3140,2974,3008,3080,3234,3088,335,145,425,520,255,253,168,167,166,221,256,163,162,222,148,149,252,251,250,249,259,257,241,233,226,238,177,176,248])).
% 63.71/63.79 cnf(3255,plain,
% 63.71/63.79 (P6(x32551,x32552,x32552,x32552)),
% 63.71/63.79 inference(rename_variables,[],[3166])).
% 63.71/63.80 cnf(3256,plain,
% 63.71/63.80 (P9(x32561,x32562,x32563,x32564,x32562,x32561,x32563,x32564)),
% 63.71/63.80 inference(rename_variables,[],[3142])).
% 63.71/63.80 cnf(3258,plain,
% 63.71/63.80 (P1(a2,a1,f13(a2,a15,a15,a2,a2,a1))),
% 63.71/63.80 inference(scs_inference,[],[142,3142,3231,3245,3150,3193,3196,3166,3148,3043,3130,3152,3154,3124,3138,3022,3016,3140,2974,3008,3080,3234,3088,3250,335,145,425,520,255,253,168,167,166,221,256,163,162,222,148,149,252,251,250,249,259,257,241,233,226,238,177,176,248,203])).
% 63.71/63.80 cnf(3259,plain,
% 63.71/63.80 (P1(x32591,x32592,x32591)),
% 63.71/63.80 inference(rename_variables,[],[3148])).
% 63.71/63.80 cnf(3260,plain,
% 63.71/63.80 (P3(x32601,x32602,x32602,x32601)),
% 63.71/63.80 inference(rename_variables,[],[3088])).
% 63.71/63.80 cnf(3263,plain,
% 63.71/63.80 (P1(x32631,x32632,x32631)),
% 63.71/63.80 inference(rename_variables,[],[3148])).
% 63.71/63.80 cnf(3264,plain,
% 63.71/63.80 (P3(x32641,x32642,x32642,x32641)),
% 63.71/63.80 inference(rename_variables,[],[3088])).
% 63.71/63.80 cnf(3268,plain,
% 63.71/63.80 (P3(a2,f4(a2,a2,a17),a2,f5(a2,a2,a17))),
% 63.71/63.80 inference(scs_inference,[],[142,3142,3231,3245,3150,3193,3196,3166,3148,3259,3043,3130,3152,3154,3124,3138,3022,3016,3140,2974,3008,3080,3234,3088,3250,3260,335,145,425,520,255,253,168,167,166,221,256,163,162,222,148,149,252,251,250,249,259,257,241,233,226,238,177,176,248,203,204,157,160])).
% 63.71/63.80 cnf(3270,plain,
% 63.71/63.80 (P10(x32701,x32701,x32701,x32701)),
% 63.71/63.80 inference(scs_inference,[],[142,3142,3231,3245,3150,3193,3196,3166,3148,3259,3043,3130,3152,3154,3124,3138,3022,3016,3140,2974,3008,3080,3234,3088,3250,3260,335,145,425,520,255,253,168,167,166,221,256,163,162,222,148,149,252,251,250,249,259,257,241,233,226,238,177,176,248,203,204,157,160,178])).
% 63.71/63.80 cnf(3272,plain,
% 63.71/63.80 (P2(x32721,x32721,x32721,x32721)),
% 63.71/63.80 inference(scs_inference,[],[142,3142,3231,3245,3150,3193,3196,3166,3148,3259,3043,3130,3152,3154,3124,3138,3022,3016,3140,2974,3008,3080,3234,3088,3250,3260,335,145,425,520,255,253,168,167,166,221,256,163,162,222,148,149,252,251,250,249,259,257,241,233,226,238,177,176,248,203,204,157,160,178,181])).
% 63.71/63.80 cnf(3274,plain,
% 63.71/63.80 (P5(x32741,x32741,x32741,f3(x32741,x32741,x32741))),
% 63.71/63.80 inference(scs_inference,[],[142,3142,3231,3245,3150,3193,3196,3166,3148,3259,3043,3130,3152,3154,3124,3138,3022,3016,3140,2974,3008,3080,3234,3088,3250,3260,335,145,425,520,255,253,168,167,166,221,256,163,162,222,148,149,252,251,250,249,259,257,241,233,226,238,177,176,248,203,204,157,160,178,181,185])).
% 63.71/63.80 cnf(3287,plain,
% 63.71/63.80 (P6(x32871,x32872,x32872,x32872)),
% 63.71/63.80 inference(rename_variables,[],[3166])).
% 63.71/63.80 cnf(3299,plain,
% 63.71/63.80 (P3(f5(a2,a2,a17),a2,a2,f4(a2,a2,a17))),
% 63.71/63.80 inference(scs_inference,[],[142,3142,3231,3245,3256,3150,3193,3196,3166,3255,3287,3148,3259,3043,3130,3152,3154,3124,3138,3022,3016,3140,2974,3008,3080,3234,3088,3250,3260,3264,335,145,425,520,255,253,168,167,166,221,256,163,162,222,148,149,252,251,250,249,259,257,241,233,226,238,177,176,248,203,204,157,160,178,181,185,194,217,195,196,198,188,187,186,227,179,237])).
% 63.71/63.80 cnf(3300,plain,
% 63.71/63.80 (P9(x33001,x33002,x33003,x33004,x33002,x33001,x33003,x33004)),
% 63.71/63.80 inference(rename_variables,[],[3142])).
% 63.71/63.80 cnf(3302,plain,
% 63.71/63.80 (P4(a1,a1,a1)),
% 63.71/63.80 inference(scs_inference,[],[142,3142,3231,3245,3256,3300,3150,3193,3196,3166,3255,3287,3148,3259,3043,3130,3152,3154,3124,3138,3022,3016,3140,2974,3008,3080,3234,3088,3250,3260,3264,3086,335,145,425,520,255,253,168,167,166,221,256,163,162,222,148,149,252,251,250,249,259,257,241,233,226,238,177,176,248,203,204,157,160,178,181,185,194,217,195,196,198,188,187,186,227,179,237,236])).
% 63.71/63.80 cnf(3306,plain,
% 63.71/63.80 (P4(f20(a1,x33061),a1,x33061)),
% 63.71/63.80 inference(scs_inference,[],[142,3142,3231,3245,3256,3300,3150,3193,3196,3166,3255,3287,3148,3259,3263,3043,3130,3152,3154,3124,3138,3022,3016,3140,2974,3008,3080,3234,3088,3250,3260,3264,3086,335,145,425,520,255,253,168,167,166,221,256,163,162,222,148,149,252,251,250,249,259,257,241,233,226,238,177,176,248,203,204,157,160,178,181,185,194,217,195,196,198,188,187,186,227,179,237,236,156])).
% 63.71/63.80 cnf(3310,plain,
% 63.71/63.80 (P5(f20(a1,x33101),a1,f20(a1,x33101),x33101)),
% 63.71/63.80 inference(scs_inference,[],[142,3142,3231,3245,3256,3300,3150,3193,3196,3166,3255,3287,3148,3259,3263,3043,3130,3152,3154,3124,3138,3022,3016,3140,2974,3008,3080,3234,3088,3250,3260,3264,3086,335,145,425,520,255,253,168,167,166,221,256,163,162,222,148,149,252,251,250,249,259,257,241,233,226,238,177,176,248,203,204,157,160,178,181,185,194,217,195,196,198,188,187,186,227,179,237,236,156,153])).
% 63.71/63.80 cnf(3318,plain,
% 63.71/63.80 (P4(f20(a1,x33181),x33181,a1)),
% 63.71/63.80 inference(scs_inference,[],[142,3142,3231,3245,3256,3300,3150,3193,3196,3166,3255,3287,3148,3259,3263,3043,3130,3152,3154,3124,3138,3022,3016,3140,2974,3008,3080,3234,3088,3250,3260,3264,3086,335,145,425,520,255,253,168,167,166,221,256,163,162,222,148,149,252,251,250,249,259,257,241,233,226,238,177,176,248,203,204,157,160,178,181,185,194,217,195,196,198,188,187,186,227,179,237,236,156,153,164,165,223,151])).
% 63.71/63.80 cnf(3391,plain,
% 63.71/63.80 (P5(x33911,x33911,x33911,x33911)),
% 63.71/63.80 inference(rename_variables,[],[3252])).
% 63.71/63.80 cnf(3396,plain,
% 63.71/63.80 (P10(x33961,x33961,x33961,x33961)),
% 63.71/63.80 inference(rename_variables,[],[3270])).
% 63.71/63.80 cnf(3399,plain,
% 63.71/63.80 (P10(x33991,x33991,x33991,x33991)),
% 63.71/63.80 inference(rename_variables,[],[3270])).
% 63.71/63.80 cnf(3411,plain,
% 63.71/63.80 (P1(x34111,x34111,x34112)),
% 63.71/63.80 inference(rename_variables,[],[3220])).
% 63.71/63.80 cnf(3414,plain,
% 63.71/63.80 (P1(x34141,x34141,x34142)),
% 63.71/63.80 inference(rename_variables,[],[3220])).
% 63.71/63.80 cnf(3421,plain,
% 63.71/63.80 (P1(x34211,x34211,x34212)),
% 63.71/63.80 inference(rename_variables,[],[3220])).
% 63.71/63.80 cnf(3447,plain,
% 63.71/63.80 (~P1(a19,a19,a17)),
% 63.71/63.80 inference(scs_inference,[],[3252,3391,3270,3396,3399,3272,3206,3222,3226,3220,3411,3414,3421,3066,3070,3198,3239,3302,3216,3101,3208,3274,3026,3247,3249,3244,3258,3310,3306,3318,3268,3299,3120,3161,1307,3080,3088,407,263,165,164,184,153,223,255,254,150,221,168,166,167,256,163,222,162,157,148,149,161,230,252,160,251,250,249,180,220,200,240,201,197,198,181,178,188,194,195,187,155,169,259,233,186,226,238,224,237,176,152])).
% 63.71/63.80 cnf(3525,plain,
% 63.71/63.80 ($false),
% 63.71/63.80 inference(scs_inference,[],[3447,3220]),
% 63.71/63.80 ['proof']).
% 63.71/63.80 % SZS output end Proof
% 63.71/63.80 % Total time :63.120000s
%------------------------------------------------------------------------------