%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : GEO596+1 : TPTP v8.2.0. Released v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% Computer : n027.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:51 EDT 2024
% Result : Theorem 59.83s 59.92s
% Output : CNFRefutation 59.83s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.12 % Problem : GEO596+1 : TPTP v8.2.0. Released v7.5.0.
% 0.11/0.12 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% 0.13/0.33 % Computer : n027.cluster.edu
% 0.13/0.33 % Model : x86_64 x86_64
% 0.13/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.33 % Memory : 8042.1875MB
% 0.13/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.33 % CPULimit : 300
% 0.13/0.33 % WCLimit : 300
% 0.13/0.33 % DateTime : Fri Jun 21 09:49:39 EDT 2024
% 0.13/0.33 % CPUTime :
% 0.57/0.61 start to proof:theBenchmark
% 59.83/59.91 %-------------------------------------------
% 59.83/59.91 % File :CSE---1.7
% 59.83/59.91 % Problem :theBenchmark
% 59.83/59.91 % Transform :cnf
% 59.83/59.91 % Format :tptp:raw
% 59.83/59.91 % Command :java -jar mcs_scs.jar %d %s
% 59.83/59.91
% 59.83/59.91 % Result :Theorem 59.150000s
% 59.83/59.91 % Output :CNFRefutation 59.150000s
% 59.83/59.91 %-------------------------------------------
% 59.83/59.92 %------------------------------------------------------------------------------
% 59.83/59.92 % File : GEO596+1 : TPTP v8.2.0. Released v7.5.0.
% 59.83/59.92 % Domain : Geometry
% 59.83/59.92 % Problem : JGEX problem 58
% 59.83/59.92 % Version : [CGZ00] axioms.
% 59.83/59.92 % English :
% 59.83/59.92
% 59.83/59.92 % Refs : [CGZ00] Chou et al. (2000), A Deductive Database Approach to A
% 59.83/59.92 % : [YCG08] Ye et al. (2008), An Introduction to Java Geometry Exp
% 59.83/59.92 % : [Qua20] Quaresma (2020), Email to Geoff Sutcliffe
% 59.83/59.92 % Source : [Qua20]
% 59.83/59.92 % Names : 58.p [Qua20]
% 59.83/59.92
% 59.83/59.92 % Status : Theorem
% 59.83/59.92 % Rating : 0.39 v8.2.0, 0.36 v8.1.0, 0.42 v7.5.0
% 59.83/59.92 % Syntax : Number of formulae : 95 ( 0 unt; 0 def)
% 59.83/59.92 % Number of atoms : 290 ( 1 equ)
% 59.83/59.92 % Maximal formula atoms : 8 ( 3 avg)
% 59.83/59.92 % Number of connectives : 202 ( 7 ~; 0 |; 100 &)
% 59.83/59.92 % ( 0 <=>; 95 =>; 0 <=; 0 <~>)
% 59.83/59.92 % Maximal formula depth : 15 ( 9 avg)
% 59.83/59.92 % Maximal term depth : 1 ( 1 avg)
% 59.83/59.92 % Number of predicates : 12 ( 11 usr; 0 prp; 2-8 aty)
% 59.83/59.92 % Number of functors : 0 ( 0 usr; 0 con; --- aty)
% 59.83/59.92 % Number of variables : 530 ( 510 !; 20 ?)
% 59.83/59.92 % SPC : FOF_THM_RFO_SEQ
% 59.83/59.92
% 59.83/59.92 % Comments : Taken from JGEX [YCG08], converted by Pedro Quaresma.
% 59.83/59.92 %------------------------------------------------------------------------------
% 59.83/59.92 include('Axioms/GEO012+0.ax').
% 59.83/59.92 %------------------------------------------------------------------------------
% 59.83/59.92 fof(exemplo6GDDFULL416058,conjecture,
% 59.83/59.92 ! [A,B,C,D,E,F,G,NWPNT1] :
% 59.83/59.92 ( ( circle(D,A,B,C)
% 59.83/59.92 & circle(D,A,E,NWPNT1)
% 59.83/59.92 & coll(F,A,B)
% 59.83/59.92 & coll(F,C,E)
% 59.83/59.92 & para(A,E,G,F)
% 59.83/59.92 & coll(G,B,C) )
% 59.83/59.92 => eqangle(G,F,F,B,F,C,C,B) ) ).
% 59.83/59.92
% 59.83/59.92 %------------------------------------------------------------------------------
% 59.83/59.92 %-------------------------------------------
% 59.83/59.92 % Proof found
% 59.83/59.92 % SZS status Theorem for theBenchmark
% 59.83/59.92 % SZS output start Proof
% 59.83/59.93 %ClaNum:261(EqnAxiom:141)
% 59.83/59.93 %VarNum:1613(SingletonVarNum:590)
% 59.83/59.93 %MaxLitNum:5
% 59.83/59.93 %MaxfuncDepth:1
% 59.83/59.93 %SharedTerms:15
% 59.83/59.93 %goalClause: 142 143 144 145 146 147 148
% 59.83/59.93 %singleGoalClaCount:7
% 59.83/59.93 [142]P1(a1,a2,a15)
% 59.83/59.93 [143]P1(a1,a16,a17)
% 59.83/59.93 [144]P1(a19,a15,a16)
% 59.83/59.93 [145]P3(a2,a17,a19,a1)
% 59.83/59.93 [146]P2(a18,a2,a15,a16)
% 59.83/59.93 [147]P2(a18,a2,a17,a20)
% 59.83/59.93 [148]~P4(a19,a1,a1,a15,a1,a16,a16,a15)
% 59.83/59.93 [149]~P1(x1492,x1491,x1493)+P1(x1491,x1492,x1493)
% 59.83/59.93 [150]~P1(x1501,x1503,x1502)+P1(x1501,x1502,x1503)
% 59.83/59.93 [151]~P8(x1511,x1512,x1513)+P1(x1511,x1512,x1513)
% 59.83/59.93 [152]~P8(x1521,x1523,x1522)+P8(x1521,x1522,x1523)
% 59.83/59.93 [154]~P8(x1541,x1542,x1543)+P5(x1541,x1542,x1541,x1543)
% 59.83/59.93 [158]~P3(x1581,x1582,x1581,x1583)+P1(x1581,x1582,x1583)
% 59.83/59.93 [224]~P5(x2241,x2242,x2241,x2243)+P4(x2241,x2242,x2242,x2243,x2242,x2243,x2241,x2243)
% 59.83/59.93 [161]~P3(x1613,x1614,x1611,x1612)+P3(x1611,x1612,x1613,x1614)
% 59.83/59.93 [162]~P3(x1621,x1622,x1624,x1623)+P3(x1621,x1622,x1623,x1624)
% 59.83/59.93 [163]~P10(x1633,x1634,x1631,x1632)+P10(x1631,x1632,x1633,x1634)
% 59.83/59.93 [164]~P10(x1641,x1642,x1644,x1643)+P10(x1641,x1642,x1643,x1644)
% 59.83/59.93 [165]~P5(x1653,x1654,x1651,x1652)+P5(x1651,x1652,x1653,x1654)
% 59.83/59.93 [166]~P5(x1661,x1662,x1664,x1663)+P5(x1661,x1662,x1663,x1664)
% 59.83/59.93 [167]~P6(x1672,x1671,x1673,x1674)+P6(x1671,x1672,x1673,x1674)
% 59.83/59.93 [168]~P6(x1681,x1683,x1682,x1684)+P6(x1681,x1682,x1683,x1684)
% 59.83/59.93 [169]~P6(x1691,x1692,x1694,x1693)+P6(x1691,x1692,x1693,x1694)
% 59.83/59.93 [222]~P6(x2222,x2223,x2221,x2224)+P4(x2221,x2222,x2221,x2223,x2224,x2222,x2224,x2223)
% 59.83/59.93 [185]~P2(x1854,x1851,x1852,x1853)+P10(f7(x1851,x1852,x1853,x1854),x1851,x1851,x1854)
% 59.83/59.93 [200]P5(x2001,x2002,x2003,x2004)+~P7(x2001,x2002,x2005,x2003,x2004,x2006)
% 59.83/59.93 [212]~P11(x2124,x2125,x2126,x2121,x2122,x2123)+P11(x2121,x2122,x2123,x2124,x2125,x2126)
% 59.83/59.93 [213]~P11(x2132,x2131,x2133,x2135,x2134,x2136)+P11(x2131,x2132,x2133,x2134,x2135,x2136)
% 59.83/59.93 [214]~P11(x2141,x2143,x2142,x2144,x2146,x2145)+P11(x2141,x2142,x2143,x2144,x2145,x2146)
% 59.83/59.93 [215]~P7(x2154,x2155,x2156,x2151,x2152,x2153)+P7(x2151,x2152,x2153,x2154,x2155,x2156)
% 59.83/59.93 [216]~P7(x2162,x2161,x2163,x2165,x2164,x2166)+P7(x2161,x2162,x2163,x2164,x2165,x2166)
% 59.83/59.93 [217]~P7(x2171,x2173,x2172,x2174,x2176,x2175)+P7(x2171,x2172,x2173,x2174,x2175,x2176)
% 59.83/59.93 [223]~P3(x2231,x2232,x2235,x2236)+P4(x2231,x2232,x2233,x2234,x2235,x2236,x2233,x2234)
% 59.83/59.93 [229]~P11(x2291,x2292,x2293,x2294,x2295,x2296)+P4(x2291,x2292,x2292,x2293,x2294,x2295,x2295,x2296)
% 59.83/59.93 [230]~P11(x2301,x2302,x2303,x2304,x2305,x2306)+P9(x2301,x2302,x2301,x2303,x2304,x2305,x2304,x2306)
% 59.83/59.93 [231]~P4(x2311,x2312,x2315,x2316,x2313,x2314,x2315,x2316)+P3(x2311,x2312,x2313,x2314)
% 59.83/59.93 [250]~P4(x2505,x2506,x2507,x2508,x2501,x2502,x2503,x2504)+P4(x2501,x2502,x2503,x2504,x2505,x2506,x2507,x2508)
% 59.83/59.93 [251]~P4(x2513,x2514,x2511,x2512,x2517,x2518,x2515,x2516)+P4(x2511,x2512,x2513,x2514,x2515,x2516,x2517,x2518)
% 59.83/59.93 [252]~P4(x2522,x2521,x2523,x2524,x2525,x2526,x2527,x2528)+P4(x2521,x2522,x2523,x2524,x2525,x2526,x2527,x2528)
% 59.83/59.93 [253]~P4(x2531,x2532,x2535,x2536,x2533,x2534,x2537,x2538)+P4(x2531,x2532,x2533,x2534,x2535,x2536,x2537,x2538)
% 59.83/59.93 [254]~P9(x2545,x2546,x2547,x2548,x2541,x2542,x2543,x2544)+P9(x2541,x2542,x2543,x2544,x2545,x2546,x2547,x2548)
% 59.83/59.93 [255]~P9(x2553,x2554,x2551,x2552,x2557,x2558,x2555,x2556)+P9(x2551,x2552,x2553,x2554,x2555,x2556,x2557,x2558)
% 59.83/59.93 [256]~P9(x2562,x2561,x2563,x2564,x2565,x2566,x2567,x2568)+P9(x2561,x2562,x2563,x2564,x2565,x2566,x2567,x2568)
% 59.83/59.93 [257]~P9(x2571,x2572,x2575,x2576,x2573,x2574,x2577,x2578)+P9(x2571,x2572,x2573,x2574,x2575,x2576,x2577,x2578)
% 59.83/59.93 [159]~P1(x1591,x1592,x1593)+~P5(x1591,x1592,x1591,x1593)+P8(x1591,x1592,x1593)
% 59.83/59.93 [233]P5(x2331,x2332,x2331,x2333)+~P4(x2331,x2332,x2332,x2333,x2332,x2333,x2331,x2333)+P1(x2331,x2332,x2333)
% 59.83/59.93 [174]~P10(x1741,x1742,x1742,x1743)+~P5(x1742,x1741,x1742,x1743)+P1(x1741,x1742,f3(x1741,x1743,x1742))
% 59.83/59.93 [186]~P10(x1862,x1861,x1861,x1863)+~P5(x1861,x1862,x1861,x1863)+P5(x1861,x1862,x1861,f3(x1862,x1863,x1861))
% 59.83/59.93 [153]~P1(x1533,x1534,x1531)+P1(x1531,x1532,x1533)+~P1(x1533,x1534,x1532)
% 59.83/59.93 [170]~P2(x1704,x1701,x1702,x1703)+P10(x1701,x1702,x1702,x1703)+~P1(x1704,x1701,x1703)
% 59.83/59.93 [171]~P10(x1711,x1714,x1712,x1713)+P5(x1711,x1712,x1711,x1713)+~P8(x1714,x1712,x1713)
% 59.83/59.93 [172]~P10(x1721,x1723,x1723,x1724)+P5(x1721,x1722,x1723,x1722)+~P8(x1722,x1721,x1724)
% 59.83/59.93 [179]~P5(x1791,x1794,x1792,x1794)+~P5(x1791,x1793,x1792,x1793)+P10(x1791,x1792,x1793,x1794)
% 59.83/59.93 [182]~P5(x1821,x1822,x1821,x1824)+~P5(x1821,x1822,x1821,x1823)+P2(x1821,x1822,x1823,x1824)
% 59.83/59.93 [228]~P3(x2281,x2284,x2283,x2282)+~P6(x2281,x2284,x2283,x2282)+P4(x2281,x2282,x2283,x2282,x2283,x2282,x2283,x2284)
% 59.83/59.93 [232]~P4(x2321,x2323,x2321,x2324,x2322,x2323,x2322,x2324)+P1(x2321,x2322,x2323)+P6(x2323,x2324,x2321,x2322)
% 59.83/59.93 [234]~P1(x2343,x2344,x2342)+~P4(x2343,x2341,x2343,x2342,x2344,x2341,x2344,x2342)+P6(x2341,x2342,x2343,x2344)
% 59.83/59.93 [236]P10(x2361,x2362,x2363,x2364)+~P4(x2361,x2362,x2363,x2364,x2363,x2364,x2361,x2362)+P3(x2361,x2362,x2363,x2364)
% 59.83/59.93 [175]~P10(x1751,x1754,x1752,x1753)+~P10(x1752,x1754,x1751,x1753)+P1(f4(x1751,x1752,x1753),x1753,x1752)
% 59.83/59.93 [176]~P10(x1761,x1764,x1762,x1763)+~P10(x1762,x1764,x1761,x1763)+P1(f5(x1761,x1762,x1763),x1763,x1761)
% 59.83/59.93 [187]~P10(x1871,x1874,x1872,x1873)+~P10(x1872,x1874,x1871,x1873)+P10(x1871,f4(x1871,x1872,x1873),x1873,x1872)
% 59.83/59.93 [188]~P10(x1881,x1884,x1882,x1883)+~P10(x1882,x1884,x1881,x1883)+P10(x1881,f5(x1882,x1881,x1883),x1883,x1882)
% 59.83/59.93 [189]~P10(x1891,x1893,x1893,x1892)+~P6(x1891,x1892,x1893,x1894)+P2(f8(x1891,x1892,x1893),x1891,x1892,x1893)
% 59.83/59.93 [191]~P10(x1913,x1914,x1912,x1911)+~P5(x1913,x1912,x1913,x1911)+P1(x1911,x1912,f22(x1912,x1911,x1913,x1914))
% 59.83/59.93 [192]~P10(x1923,x1924,x1921,x1922)+~P5(x1923,x1921,x1923,x1922)+P1(f22(x1921,x1922,x1923,x1924),x1923,x1924)
% 59.83/59.93 [243]~P5(x2433,x2432,x2433,x2431)+~P4(x2432,x2433,x2433,x2434,x2433,x2434,x2433,x2431)+P1(x2431,x2432,f23(x2432,x2431,x2433,x2434))
% 59.83/59.93 [244]~P10(x2443,x2444,x2442,x2441)+~P4(x2442,x2443,x2443,x2444,x2443,x2444,x2443,x2441)+P1(x2441,x2442,f24(x2442,x2441,x2443,x2444))
% 59.83/59.93 [245]~P10(x2453,x2452,x2452,x2451)+~P4(x2454,x2453,x2452,x2453,x2452,x2453,x2451,x2453)+P1(f14(x2451,x2452,x2453,x2454),x2453,x2454)
% 59.83/59.93 [246]~P10(x2463,x2462,x2462,x2461)+~P4(x2464,x2463,x2462,x2463,x2462,x2463,x2461,x2463)+P1(f14(x2461,x2462,x2463,x2464),x2461,x2462)
% 59.83/59.93 [247]~P5(x2473,x2471,x2473,x2472)+~P4(x2471,x2473,x2473,x2474,x2473,x2474,x2473,x2472)+P1(f23(x2471,x2472,x2473,x2474),x2473,x2474)
% 59.83/59.93 [248]~P10(x2483,x2484,x2481,x2482)+~P4(x2481,x2483,x2483,x2484,x2483,x2484,x2483,x2482)+P1(f24(x2481,x2482,x2483,x2484),x2483,x2484)
% 59.83/59.93 [155]~P8(x1555,x1551,x1553)+P3(x1551,x1552,x1553,x1554)+~P8(x1555,x1552,x1554)
% 59.83/59.93 [156]~P8(x1561,x1565,x1563)+P3(x1561,x1562,x1563,x1564)+~P8(x1562,x1565,x1564)
% 59.83/59.93 [183]~P6(x1835,x1831,x1832,x1833)+P6(x1831,x1832,x1833,x1834)+~P6(x1835,x1831,x1832,x1834)
% 59.83/59.93 [225]~P8(x2255,x2252,x2253)+~P2(x2254,x2251,x2252,x2253)+P4(x2251,x2252,x2251,x2253,x2254,x2252,x2254,x2255)
% 59.83/59.93 [227]~P2(x2275,x2271,x2273,x2274)+P4(x2271,x2272,x2271,x2273,x2274,x2271,x2274,x2273)+~P10(x2275,x2271,x2271,x2272)
% 59.83/59.93 [240]~P4(x2402,x2403,x2402,x2404,x2405,x2402,x2405,x2404)+P10(x2401,x2402,x2402,x2403)+~P2(x2401,x2402,x2404,x2405)
% 59.83/59.93 [195]~P1(x1952,x1954,x1955)+~P10(x1951,x1953,x1953,x1952)+P1(f12(x1951,x1952,x1953,x1954,x1955),x1954,x1955)
% 59.83/59.93 [196]~P1(x1962,x1964,x1965)+~P10(x1961,x1963,x1963,x1962)+P10(f12(x1961,x1962,x1963,x1964,x1965),x1961,x1964,x1965)
% 59.83/59.93 [197]~P10(x1973,x1974,x1974,x1971)+~P5(x1971,x1972,x1971,x1975)+P5(x1971,x1972,x1971,f27(x1973,x1974,x1972,x1975,x1971))
% 59.83/59.93 [198]~P10(x1983,x1981,x1981,x1985)+~P5(x1985,x1982,x1985,x1984)+P5(x1981,x1982,x1981,f27(x1983,x1981,x1982,x1984,x1985))
% 59.83/59.93 [199]~P10(x1991,x1992,x1992,x1995)+~P5(x1995,x1993,x1995,x1994)+P3(f27(x1991,x1992,x1993,x1994,x1995),x1993,x1991,x1992)
% 59.83/59.93 [242]~P4(x2421,x2423,x2422,x2423,x2421,x2424,x2422,x2425)+P1(x2421,x2422,x2423)+P6(x2424,x2422,x2423,f26(x2421,x2422,x2423,x2424))
% 59.83/59.93 [258]~P4(x2581,x2583,x2582,x2583,x2581,x2584,x2582,x2585)+P1(x2581,x2582,x2583)+P4(x2581,x2583,x2582,x2583,x2581,f26(x2581,x2582,x2583,x2584),x2582,f26(x2581,x2582,x2583,x2584))
% 59.83/59.93 [177]~P3(x1771,x1772,x1775,x1776)+P3(x1771,x1772,x1773,x1774)+~P3(x1775,x1776,x1773,x1774)
% 59.83/59.93 [178]~P10(x1781,x1782,x1785,x1786)+P3(x1781,x1782,x1783,x1784)+~P10(x1785,x1786,x1783,x1784)
% 59.83/59.93 [180]~P10(x1805,x1806,x1803,x1804)+P10(x1801,x1802,x1803,x1804)+~P3(x1801,x1802,x1805,x1806)
% 59.83/59.93 [181]~P5(x1811,x1812,x1815,x1816)+P5(x1811,x1812,x1813,x1814)+~P5(x1815,x1816,x1813,x1814)
% 59.83/59.93 [218]~P5(x2181,x2182,x2184,x2185)+~P11(x2181,x2182,x2183,x2184,x2185,x2186)+P7(x2181,x2182,x2183,x2184,x2185,x2186)
% 59.83/59.94 [221]~P8(x2214,x2215,x2216)+~P8(x2211,x2212,x2213)+P9(x2211,x2212,x2212,x2213,x2214,x2215,x2215,x2216)
% 59.83/59.94 [201]~P8(x2016,x2013,x2014)+~P8(x2015,x2011,x2012)+P8(f25(x2011,x2012,x2013,x2014,x2015,x2016),x2011,x2014)
% 59.83/59.94 [202]~P8(x2026,x2023,x2024)+~P8(x2025,x2021,x2022)+P3(f25(x2021,x2022,x2023,x2024,x2025,x2026),x2026,x2021,x2023)
% 59.83/59.94 [203]~P8(x2036,x2033,x2034)+~P8(x2035,x2031,x2032)+P3(f25(x2031,x2032,x2033,x2034,x2035,x2036),x2035,x2032,x2034)
% 59.83/59.94 [238]~P4(x2381,x2382,x2383,x2384,x2385,x2386,x2387,x2388)+P3(x2381,x2382,x2383,x2384)+~P3(x2385,x2386,x2387,x2388)
% 59.83/59.94 [239]~P4(x2391,x2392,x2393,x2394,x2395,x2396,x2397,x2398)+P10(x2391,x2392,x2393,x2394)+~P10(x2395,x2396,x2397,x2398)
% 59.83/59.94 [241]~P9(x2411,x2412,x2413,x2414,x2415,x2416,x2417,x2418)+P5(x2411,x2412,x2413,x2414)+~P5(x2415,x2416,x2417,x2418)
% 59.83/59.94 [219]~P11(x2191,x2192,x2193,x2197,x2198,x2199)+P11(x2191,x2192,x2193,x2194,x2195,x2196)+~P11(x2197,x2198,x2199,x2194,x2195,x2196)
% 59.83/59.94 [220]~P7(x2201,x2202,x2203,x2207,x2208,x2209)+P7(x2201,x2202,x2203,x2204,x2205,x2206)+~P7(x2207,x2208,x2209,x2204,x2205,x2206)
% 59.83/59.94 [260]~P4(x2601,x2602,x2603,x2604,x2609,x26010,x26011,x26012)+P4(x2601,x2602,x2603,x2604,x2605,x2606,x2607,x2608)+~P4(x2609,x26010,x26011,x26012,x2605,x2606,x2607,x2608)
% 59.83/59.94 [261]~P9(x2611,x2612,x2613,x2614,x2619,x26110,x26111,x26112)+P9(x2611,x2612,x2613,x2614,x2615,x2616,x2617,x2618)+~P9(x2619,x26110,x26111,x26112,x2615,x2616,x2617,x2618)
% 59.83/59.94 [193]~P5(x1932,x1931,x1934,x1931)+~P6(x1932,x1934,x1931,x1933)+P10(x1931,x1932,x1932,x1933)+~P5(x1932,x1933,x1934,x1933)
% 59.83/59.94 [160]~P1(x1601,x1602,x1603)+~P3(x1604,x1601,x1605,x1603)+P8(x1601,x1602,x1603)+~P8(x1604,x1602,x1605)
% 59.83/59.94 [173]~P3(x1734,x1733,x1735,x1732)+~P3(x1734,x1732,x1735,x1733)+P8(x1731,x1732,x1733)+~P8(x1731,x1734,x1735)
% 59.83/59.94 [194]~P5(x1945,x1941,x1945,x1943)+~P5(x1945,x1941,x1945,x1942)+P6(x1941,x1942,x1943,x1944)+~P5(x1945,x1941,x1945,x1944)
% 59.83/59.94 [226]~P1(x2261,x2264,x2265)+~P1(x2261,x2262,x2263)+~P3(x2262,x2264,x2263,x2265)+P9(x2261,x2262,x2262,x2263,x2261,x2264,x2264,x2265)
% 59.83/59.94 [237]~P1(x2371,x2372,x2373)+~P4(x2375,x2372,x2375,x2373,x2374,x2372,x2374,x2371)+P8(x2371,x2372,x2373)+~P2(x2374,x2375,x2372,x2373)
% 59.83/59.94 [184]~P10(x1843,x1841,x1843,x1845)+~P10(x1841,x1842,x1841,x1843)+~P8(x1844,x1842,x1845)+P8(f6(x1841,x1842,x1843),x1841,x1843)
% 59.83/59.94 [190]~P6(x1901,x1902,x1903,x1905)+~P3(x1901,x1902,x1903,x1905)+~P8(x1904,x1901,x1902)+P2(f9(x1901,x1902,x1903),x1901,x1902,x1903)
% 59.83/59.94 [259]~P4(x2591,x2593,x2592,x2593,x2594,x2596,x2595,x2596)+~P4(x2591,x2592,x2592,x2593,x2594,x2595,x2595,x2596)+P1(x2591,x2592,x2593)+P11(x2591,x2592,x2593,x2594,x2595,x2596)
% 59.83/59.94 [249]~P6(x2491,x2492,x2495,x2494)+~P6(x2491,x2492,x2495,x2493)+~P4(x2495,x2491,x2495,x2492,x2496,x2493,x2496,x2494)+P5(x2491,x2492,x2493,x2494)+~P6(x2491,x2492,x2495,x2496)
% 59.83/59.94 [204]~P1(x2042,x2043,x2044)+~P1(x2041,x2044,x2046)+~P1(x2041,x2043,x2045)+~P3(x2043,x2044,x2045,x2046)+P1(x2041,x2042,f13(x2043,x2044,x2045,x2046,x2041,x2042))
% 59.83/59.94 [205]~P1(x2056,x2051,x2052)+~P1(x2055,x2052,x2054)+~P1(x2055,x2051,x2053)+~P3(x2051,x2052,x2053,x2054)+P1(f13(x2051,x2052,x2053,x2054,x2055,x2056),x2053,x2054)
% 59.83/59.94 [206]~P1(x2063,x2064,x2065)+~P8(x2066,x2061,x2062)+~P3(x2061,x2063,x2065,x2066)+~P3(x2061,x2063,x2062,x2064)+P1(f28(x2061,x2062,x2063,x2064,x2065,x2066),x2066,x2065)
% 59.83/59.94 [207]~P1(x2073,x2074,x2075)+~P8(x2076,x2071,x2072)+~P3(x2071,x2073,x2075,x2076)+~P3(x2071,x2073,x2072,x2074)+P1(f28(x2071,x2072,x2073,x2074,x2075,x2076),x2071,x2074)
% 59.83/59.94 [208]~P5(x2082,x2083,x2082,x2084)+~P5(x2081,x2083,x2081,x2086)+~P2(x2081,x2083,x2084,x2085)+E(x2081,x2082)+P1(f10(x2083,x2084,x2085,x2086,x2081,x2082),x2083,x2085)
% 59.83/59.94 [209]~P5(x2092,x2093,x2092,x2094)+~P5(x2091,x2093,x2091,x2096)+~P2(x2091,x2093,x2094,x2095)+E(x2091,x2092)+P1(f11(x2093,x2094,x2095,x2096,x2091,x2092),x2094,x2096)
% 59.83/59.94 [210]~P5(x2102,x2103,x2102,x2104)+~P5(x2101,x2103,x2101,x2106)+~P2(x2101,x2103,x2104,x2105)+E(x2101,x2102)+P5(f10(x2103,x2104,x2105,x2106,x2101,x2102),x2102,x2102,x2103)
% 59.83/59.94 [211]~P5(x2112,x2113,x2112,x2114)+~P5(x2111,x2113,x2111,x2116)+~P2(x2111,x2113,x2114,x2115)+E(x2111,x2112)+P5(f11(x2113,x2114,x2115,x2116,x2111,x2112),x2112,x2112,x2113)
% 59.83/59.94 [157]~P1(x1573,x1571,x1574)+~P1(x1575,x1571,x1574)+~P8(x1576,x1575,x1573)+~P8(x1577,x1571,x1574)+P8(f21(x1571,x1572),x1571,x1572)
% 59.83/59.94 %EqnAxiom
% 59.83/59.94 [1]E(x11,x11)
% 59.83/59.94 [2]E(x22,x21)+~E(x21,x22)
% 59.83/59.94 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 59.83/59.94 [4]~E(x41,x42)+E(f21(x41,x43),f21(x42,x43))
% 59.83/59.94 [5]~E(x51,x52)+E(f21(x53,x51),f21(x53,x52))
% 59.83/59.94 [6]~E(x61,x62)+E(f3(x61,x63,x64),f3(x62,x63,x64))
% 59.83/59.94 [7]~E(x71,x72)+E(f3(x73,x71,x74),f3(x73,x72,x74))
% 59.83/59.94 [8]~E(x81,x82)+E(f3(x83,x84,x81),f3(x83,x84,x82))
% 59.83/59.94 [9]~E(x91,x92)+E(f4(x91,x93,x94),f4(x92,x93,x94))
% 59.83/59.94 [10]~E(x101,x102)+E(f4(x103,x101,x104),f4(x103,x102,x104))
% 59.83/59.94 [11]~E(x111,x112)+E(f4(x113,x114,x111),f4(x113,x114,x112))
% 59.83/59.94 [12]~E(x121,x122)+E(f5(x121,x123,x124),f5(x122,x123,x124))
% 59.83/59.94 [13]~E(x131,x132)+E(f5(x133,x131,x134),f5(x133,x132,x134))
% 59.83/59.94 [14]~E(x141,x142)+E(f5(x143,x144,x141),f5(x143,x144,x142))
% 59.83/59.94 [15]~E(x151,x152)+E(f6(x151,x153,x154),f6(x152,x153,x154))
% 59.83/59.94 [16]~E(x161,x162)+E(f6(x163,x161,x164),f6(x163,x162,x164))
% 59.83/59.94 [17]~E(x171,x172)+E(f6(x173,x174,x171),f6(x173,x174,x172))
% 59.83/59.94 [18]~E(x181,x182)+E(f7(x181,x183,x184,x185),f7(x182,x183,x184,x185))
% 59.83/59.94 [19]~E(x191,x192)+E(f7(x193,x191,x194,x195),f7(x193,x192,x194,x195))
% 59.83/59.94 [20]~E(x201,x202)+E(f7(x203,x204,x201,x205),f7(x203,x204,x202,x205))
% 59.83/59.94 [21]~E(x211,x212)+E(f7(x213,x214,x215,x211),f7(x213,x214,x215,x212))
% 59.83/59.94 [22]~E(x221,x222)+E(f26(x221,x223,x224,x225),f26(x222,x223,x224,x225))
% 59.83/59.94 [23]~E(x231,x232)+E(f26(x233,x231,x234,x235),f26(x233,x232,x234,x235))
% 59.83/59.94 [24]~E(x241,x242)+E(f26(x243,x244,x241,x245),f26(x243,x244,x242,x245))
% 59.83/59.94 [25]~E(x251,x252)+E(f26(x253,x254,x255,x251),f26(x253,x254,x255,x252))
% 59.83/59.94 [26]~E(x261,x262)+E(f23(x261,x263,x264,x265),f23(x262,x263,x264,x265))
% 59.83/59.94 [27]~E(x271,x272)+E(f23(x273,x271,x274,x275),f23(x273,x272,x274,x275))
% 59.83/59.94 [28]~E(x281,x282)+E(f23(x283,x284,x281,x285),f23(x283,x284,x282,x285))
% 59.83/59.94 [29]~E(x291,x292)+E(f23(x293,x294,x295,x291),f23(x293,x294,x295,x292))
% 59.83/59.94 [30]~E(x301,x302)+E(f24(x301,x303,x304,x305),f24(x302,x303,x304,x305))
% 59.83/59.94 [31]~E(x311,x312)+E(f24(x313,x311,x314,x315),f24(x313,x312,x314,x315))
% 59.83/59.94 [32]~E(x321,x322)+E(f24(x323,x324,x321,x325),f24(x323,x324,x322,x325))
% 59.83/59.94 [33]~E(x331,x332)+E(f24(x333,x334,x335,x331),f24(x333,x334,x335,x332))
% 59.83/59.94 [34]~E(x341,x342)+E(f8(x341,x343,x344),f8(x342,x343,x344))
% 59.83/59.94 [35]~E(x351,x352)+E(f8(x353,x351,x354),f8(x353,x352,x354))
% 59.83/59.94 [36]~E(x361,x362)+E(f8(x363,x364,x361),f8(x363,x364,x362))
% 59.83/59.94 [37]~E(x371,x372)+E(f9(x371,x373,x374),f9(x372,x373,x374))
% 59.83/59.94 [38]~E(x381,x382)+E(f9(x383,x381,x384),f9(x383,x382,x384))
% 59.83/59.94 [39]~E(x391,x392)+E(f9(x393,x394,x391),f9(x393,x394,x392))
% 59.83/59.94 [40]~E(x401,x402)+E(f22(x401,x403,x404,x405),f22(x402,x403,x404,x405))
% 59.83/59.94 [41]~E(x411,x412)+E(f22(x413,x411,x414,x415),f22(x413,x412,x414,x415))
% 59.83/59.94 [42]~E(x421,x422)+E(f22(x423,x424,x421,x425),f22(x423,x424,x422,x425))
% 59.83/59.94 [43]~E(x431,x432)+E(f22(x433,x434,x435,x431),f22(x433,x434,x435,x432))
% 59.83/59.94 [44]~E(x441,x442)+E(f14(x441,x443,x444,x445),f14(x442,x443,x444,x445))
% 59.83/59.94 [45]~E(x451,x452)+E(f14(x453,x451,x454,x455),f14(x453,x452,x454,x455))
% 59.83/59.94 [46]~E(x461,x462)+E(f14(x463,x464,x461,x465),f14(x463,x464,x462,x465))
% 59.83/59.94 [47]~E(x471,x472)+E(f14(x473,x474,x475,x471),f14(x473,x474,x475,x472))
% 59.83/59.94 [48]~E(x481,x482)+E(f12(x481,x483,x484,x485,x486),f12(x482,x483,x484,x485,x486))
% 59.83/59.94 [49]~E(x491,x492)+E(f12(x493,x491,x494,x495,x496),f12(x493,x492,x494,x495,x496))
% 59.83/59.94 [50]~E(x501,x502)+E(f12(x503,x504,x501,x505,x506),f12(x503,x504,x502,x505,x506))
% 59.83/59.94 [51]~E(x511,x512)+E(f12(x513,x514,x515,x511,x516),f12(x513,x514,x515,x512,x516))
% 59.83/59.94 [52]~E(x521,x522)+E(f12(x523,x524,x525,x526,x521),f12(x523,x524,x525,x526,x522))
% 59.83/59.94 [53]~E(x531,x532)+E(f11(x531,x533,x534,x535,x536,x537),f11(x532,x533,x534,x535,x536,x537))
% 59.83/59.94 [54]~E(x541,x542)+E(f11(x543,x541,x544,x545,x546,x547),f11(x543,x542,x544,x545,x546,x547))
% 59.83/59.94 [55]~E(x551,x552)+E(f11(x553,x554,x551,x555,x556,x557),f11(x553,x554,x552,x555,x556,x557))
% 59.83/59.94 [56]~E(x561,x562)+E(f11(x563,x564,x565,x561,x566,x567),f11(x563,x564,x565,x562,x566,x567))
% 59.83/59.94 [57]~E(x571,x572)+E(f11(x573,x574,x575,x576,x571,x577),f11(x573,x574,x575,x576,x572,x577))
% 59.83/59.94 [58]~E(x581,x582)+E(f11(x583,x584,x585,x586,x587,x581),f11(x583,x584,x585,x586,x587,x582))
% 59.83/59.94 [59]~E(x591,x592)+E(f27(x591,x593,x594,x595,x596),f27(x592,x593,x594,x595,x596))
% 59.83/59.94 [60]~E(x601,x602)+E(f27(x603,x601,x604,x605,x606),f27(x603,x602,x604,x605,x606))
% 59.83/59.94 [61]~E(x611,x612)+E(f27(x613,x614,x611,x615,x616),f27(x613,x614,x612,x615,x616))
% 59.83/59.94 [62]~E(x621,x622)+E(f27(x623,x624,x625,x621,x626),f27(x623,x624,x625,x622,x626))
% 59.83/59.94 [63]~E(x631,x632)+E(f27(x633,x634,x635,x636,x631),f27(x633,x634,x635,x636,x632))
% 59.83/59.94 [64]~E(x641,x642)+E(f10(x641,x643,x644,x645,x646,x647),f10(x642,x643,x644,x645,x646,x647))
% 59.83/59.94 [65]~E(x651,x652)+E(f10(x653,x651,x654,x655,x656,x657),f10(x653,x652,x654,x655,x656,x657))
% 59.83/59.94 [66]~E(x661,x662)+E(f10(x663,x664,x661,x665,x666,x667),f10(x663,x664,x662,x665,x666,x667))
% 59.83/59.94 [67]~E(x671,x672)+E(f10(x673,x674,x675,x671,x676,x677),f10(x673,x674,x675,x672,x676,x677))
% 59.83/59.94 [68]~E(x681,x682)+E(f10(x683,x684,x685,x686,x681,x687),f10(x683,x684,x685,x686,x682,x687))
% 59.83/59.94 [69]~E(x691,x692)+E(f10(x693,x694,x695,x696,x697,x691),f10(x693,x694,x695,x696,x697,x692))
% 59.83/59.94 [70]~E(x701,x702)+E(f28(x701,x703,x704,x705,x706,x707),f28(x702,x703,x704,x705,x706,x707))
% 59.83/59.94 [71]~E(x711,x712)+E(f28(x713,x711,x714,x715,x716,x717),f28(x713,x712,x714,x715,x716,x717))
% 59.83/59.94 [72]~E(x721,x722)+E(f28(x723,x724,x721,x725,x726,x727),f28(x723,x724,x722,x725,x726,x727))
% 59.83/59.94 [73]~E(x731,x732)+E(f28(x733,x734,x735,x731,x736,x737),f28(x733,x734,x735,x732,x736,x737))
% 59.83/59.94 [74]~E(x741,x742)+E(f28(x743,x744,x745,x746,x741,x747),f28(x743,x744,x745,x746,x742,x747))
% 59.83/59.94 [75]~E(x751,x752)+E(f28(x753,x754,x755,x756,x757,x751),f28(x753,x754,x755,x756,x757,x752))
% 59.83/59.94 [76]~E(x761,x762)+E(f25(x761,x763,x764,x765,x766,x767),f25(x762,x763,x764,x765,x766,x767))
% 59.83/59.94 [77]~E(x771,x772)+E(f25(x773,x771,x774,x775,x776,x777),f25(x773,x772,x774,x775,x776,x777))
% 59.83/59.94 [78]~E(x781,x782)+E(f25(x783,x784,x781,x785,x786,x787),f25(x783,x784,x782,x785,x786,x787))
% 59.83/59.94 [79]~E(x791,x792)+E(f25(x793,x794,x795,x791,x796,x797),f25(x793,x794,x795,x792,x796,x797))
% 59.83/59.94 [80]~E(x801,x802)+E(f25(x803,x804,x805,x806,x801,x807),f25(x803,x804,x805,x806,x802,x807))
% 59.83/59.94 [81]~E(x811,x812)+E(f25(x813,x814,x815,x816,x817,x811),f25(x813,x814,x815,x816,x817,x812))
% 59.83/59.94 [82]~E(x821,x822)+E(f13(x821,x823,x824,x825,x826,x827),f13(x822,x823,x824,x825,x826,x827))
% 59.83/59.94 [83]~E(x831,x832)+E(f13(x833,x831,x834,x835,x836,x837),f13(x833,x832,x834,x835,x836,x837))
% 59.83/59.94 [84]~E(x841,x842)+E(f13(x843,x844,x841,x845,x846,x847),f13(x843,x844,x842,x845,x846,x847))
% 59.83/59.94 [85]~E(x851,x852)+E(f13(x853,x854,x855,x851,x856,x857),f13(x853,x854,x855,x852,x856,x857))
% 59.83/59.94 [86]~E(x861,x862)+E(f13(x863,x864,x865,x866,x861,x867),f13(x863,x864,x865,x866,x862,x867))
% 59.83/59.94 [87]~E(x871,x872)+E(f13(x873,x874,x875,x876,x877,x871),f13(x873,x874,x875,x876,x877,x872))
% 59.83/59.94 [88]P1(x882,x883,x884)+~E(x881,x882)+~P1(x881,x883,x884)
% 59.83/59.94 [89]P1(x893,x892,x894)+~E(x891,x892)+~P1(x893,x891,x894)
% 59.83/59.94 [90]P1(x903,x904,x902)+~E(x901,x902)+~P1(x903,x904,x901)
% 59.83/59.94 [91]P9(x912,x913,x914,x915,x916,x917,x918,x919)+~E(x911,x912)+~P9(x911,x913,x914,x915,x916,x917,x918,x919)
% 59.83/59.94 [92]P9(x923,x922,x924,x925,x926,x927,x928,x929)+~E(x921,x922)+~P9(x923,x921,x924,x925,x926,x927,x928,x929)
% 59.83/59.94 [93]P9(x933,x934,x932,x935,x936,x937,x938,x939)+~E(x931,x932)+~P9(x933,x934,x931,x935,x936,x937,x938,x939)
% 59.83/59.94 [94]P9(x943,x944,x945,x942,x946,x947,x948,x949)+~E(x941,x942)+~P9(x943,x944,x945,x941,x946,x947,x948,x949)
% 59.83/59.94 [95]P9(x953,x954,x955,x956,x952,x957,x958,x959)+~E(x951,x952)+~P9(x953,x954,x955,x956,x951,x957,x958,x959)
% 59.83/59.94 [96]P9(x963,x964,x965,x966,x967,x962,x968,x969)+~E(x961,x962)+~P9(x963,x964,x965,x966,x967,x961,x968,x969)
% 59.83/59.94 [97]P9(x973,x974,x975,x976,x977,x978,x972,x979)+~E(x971,x972)+~P9(x973,x974,x975,x976,x977,x978,x971,x979)
% 59.83/59.94 [98]P9(x983,x984,x985,x986,x987,x988,x989,x982)+~E(x981,x982)+~P9(x983,x984,x985,x986,x987,x988,x989,x981)
% 59.83/59.94 [99]P6(x992,x993,x994,x995)+~E(x991,x992)+~P6(x991,x993,x994,x995)
% 59.83/59.94 [100]P6(x1003,x1002,x1004,x1005)+~E(x1001,x1002)+~P6(x1003,x1001,x1004,x1005)
% 59.83/59.94 [101]P6(x1013,x1014,x1012,x1015)+~E(x1011,x1012)+~P6(x1013,x1014,x1011,x1015)
% 59.83/59.94 [102]P6(x1023,x1024,x1025,x1022)+~E(x1021,x1022)+~P6(x1023,x1024,x1025,x1021)
% 59.83/59.94 [103]P3(x1032,x1033,x1034,x1035)+~E(x1031,x1032)+~P3(x1031,x1033,x1034,x1035)
% 59.83/59.94 [104]P3(x1043,x1042,x1044,x1045)+~E(x1041,x1042)+~P3(x1043,x1041,x1044,x1045)
% 59.83/59.94 [105]P3(x1053,x1054,x1052,x1055)+~E(x1051,x1052)+~P3(x1053,x1054,x1051,x1055)
% 59.83/59.94 [106]P3(x1063,x1064,x1065,x1062)+~E(x1061,x1062)+~P3(x1063,x1064,x1065,x1061)
% 59.83/59.94 [107]P2(x1072,x1073,x1074,x1075)+~E(x1071,x1072)+~P2(x1071,x1073,x1074,x1075)
% 59.83/59.94 [108]P2(x1083,x1082,x1084,x1085)+~E(x1081,x1082)+~P2(x1083,x1081,x1084,x1085)
% 59.83/59.94 [109]P2(x1093,x1094,x1092,x1095)+~E(x1091,x1092)+~P2(x1093,x1094,x1091,x1095)
% 59.83/59.94 [110]P2(x1103,x1104,x1105,x1102)+~E(x1101,x1102)+~P2(x1103,x1104,x1105,x1101)
% 59.83/59.94 [111]P11(x1112,x1113,x1114,x1115,x1116,x1117)+~E(x1111,x1112)+~P11(x1111,x1113,x1114,x1115,x1116,x1117)
% 59.83/59.94 [112]P11(x1123,x1122,x1124,x1125,x1126,x1127)+~E(x1121,x1122)+~P11(x1123,x1121,x1124,x1125,x1126,x1127)
% 59.83/59.94 [113]P11(x1133,x1134,x1132,x1135,x1136,x1137)+~E(x1131,x1132)+~P11(x1133,x1134,x1131,x1135,x1136,x1137)
% 59.83/59.94 [114]P11(x1143,x1144,x1145,x1142,x1146,x1147)+~E(x1141,x1142)+~P11(x1143,x1144,x1145,x1141,x1146,x1147)
% 59.83/59.94 [115]P11(x1153,x1154,x1155,x1156,x1152,x1157)+~E(x1151,x1152)+~P11(x1153,x1154,x1155,x1156,x1151,x1157)
% 59.83/59.94 [116]P11(x1163,x1164,x1165,x1166,x1167,x1162)+~E(x1161,x1162)+~P11(x1163,x1164,x1165,x1166,x1167,x1161)
% 59.83/59.94 [117]P4(x1172,x1173,x1174,x1175,x1176,x1177,x1178,x1179)+~E(x1171,x1172)+~P4(x1171,x1173,x1174,x1175,x1176,x1177,x1178,x1179)
% 59.83/59.94 [118]P4(x1183,x1182,x1184,x1185,x1186,x1187,x1188,x1189)+~E(x1181,x1182)+~P4(x1183,x1181,x1184,x1185,x1186,x1187,x1188,x1189)
% 59.83/59.94 [119]P4(x1193,x1194,x1192,x1195,x1196,x1197,x1198,x1199)+~E(x1191,x1192)+~P4(x1193,x1194,x1191,x1195,x1196,x1197,x1198,x1199)
% 59.83/59.94 [120]P4(x1203,x1204,x1205,x1202,x1206,x1207,x1208,x1209)+~E(x1201,x1202)+~P4(x1203,x1204,x1205,x1201,x1206,x1207,x1208,x1209)
% 59.83/59.94 [121]P4(x1213,x1214,x1215,x1216,x1212,x1217,x1218,x1219)+~E(x1211,x1212)+~P4(x1213,x1214,x1215,x1216,x1211,x1217,x1218,x1219)
% 59.83/59.94 [122]P4(x1223,x1224,x1225,x1226,x1227,x1222,x1228,x1229)+~E(x1221,x1222)+~P4(x1223,x1224,x1225,x1226,x1227,x1221,x1228,x1229)
% 59.83/59.94 [123]P4(x1233,x1234,x1235,x1236,x1237,x1238,x1232,x1239)+~E(x1231,x1232)+~P4(x1233,x1234,x1235,x1236,x1237,x1238,x1231,x1239)
% 59.83/59.94 [124]P4(x1243,x1244,x1245,x1246,x1247,x1248,x1249,x1242)+~E(x1241,x1242)+~P4(x1243,x1244,x1245,x1246,x1247,x1248,x1249,x1241)
% 59.83/59.94 [125]P10(x1252,x1253,x1254,x1255)+~E(x1251,x1252)+~P10(x1251,x1253,x1254,x1255)
% 59.83/59.94 [126]P10(x1263,x1262,x1264,x1265)+~E(x1261,x1262)+~P10(x1263,x1261,x1264,x1265)
% 59.83/59.94 [127]P10(x1273,x1274,x1272,x1275)+~E(x1271,x1272)+~P10(x1273,x1274,x1271,x1275)
% 59.83/59.94 [128]P10(x1283,x1284,x1285,x1282)+~E(x1281,x1282)+~P10(x1283,x1284,x1285,x1281)
% 59.83/59.94 [129]P5(x1292,x1293,x1294,x1295)+~E(x1291,x1292)+~P5(x1291,x1293,x1294,x1295)
% 59.83/59.94 [130]P5(x1303,x1302,x1304,x1305)+~E(x1301,x1302)+~P5(x1303,x1301,x1304,x1305)
% 59.83/59.94 [131]P5(x1313,x1314,x1312,x1315)+~E(x1311,x1312)+~P5(x1313,x1314,x1311,x1315)
% 59.83/59.94 [132]P5(x1323,x1324,x1325,x1322)+~E(x1321,x1322)+~P5(x1323,x1324,x1325,x1321)
% 59.83/59.94 [133]P8(x1332,x1333,x1334)+~E(x1331,x1332)+~P8(x1331,x1333,x1334)
% 59.83/59.94 [134]P8(x1343,x1342,x1344)+~E(x1341,x1342)+~P8(x1343,x1341,x1344)
% 59.83/59.94 [135]P8(x1353,x1354,x1352)+~E(x1351,x1352)+~P8(x1353,x1354,x1351)
% 59.83/59.94 [136]P7(x1362,x1363,x1364,x1365,x1366,x1367)+~E(x1361,x1362)+~P7(x1361,x1363,x1364,x1365,x1366,x1367)
% 59.83/59.94 [137]P7(x1373,x1372,x1374,x1375,x1376,x1377)+~E(x1371,x1372)+~P7(x1373,x1371,x1374,x1375,x1376,x1377)
% 59.83/59.94 [138]P7(x1383,x1384,x1382,x1385,x1386,x1387)+~E(x1381,x1382)+~P7(x1383,x1384,x1381,x1385,x1386,x1387)
% 59.83/59.94 [139]P7(x1393,x1394,x1395,x1392,x1396,x1397)+~E(x1391,x1392)+~P7(x1393,x1394,x1395,x1391,x1396,x1397)
% 59.83/59.94 [140]P7(x1403,x1404,x1405,x1406,x1402,x1407)+~E(x1401,x1402)+~P7(x1403,x1404,x1405,x1406,x1401,x1407)
% 59.83/59.94 [141]P7(x1413,x1414,x1415,x1416,x1417,x1412)+~E(x1411,x1412)+~P7(x1413,x1414,x1415,x1416,x1417,x1411)
% 59.83/59.94
% 59.83/59.94 %-------------------------------------------
% 59.83/59.94 cnf(264,plain,
% 59.83/59.94 (~P4(a1,a16,a16,a15,a19,a1,a1,a15)),
% 59.83/59.94 inference(scs_inference,[],[148,229,250])).
% 59.83/59.94 cnf(266,plain,
% 59.83/59.94 (~P4(a1,a15,a19,a1,a16,a15,a1,a16)),
% 59.83/59.94 inference(scs_inference,[],[148,229,250,251])).
% 59.83/59.94 cnf(268,plain,
% 59.83/59.94 (~P4(a1,a19,a1,a15,a1,a16,a16,a15)),
% 59.83/59.94 inference(scs_inference,[],[148,229,250,251,252])).
% 59.83/59.94 cnf(270,plain,
% 59.83/59.94 (~P4(a19,a1,a1,a16,a1,a15,a16,a15)),
% 59.83/59.94 inference(scs_inference,[],[148,229,250,251,252,253])).
% 59.83/59.94 cnf(272,plain,
% 59.83/59.94 (~P11(a1,a16,a15,a19,a1,a15)),
% 59.83/59.94 inference(scs_inference,[],[148,229,250,251,252,253,212])).
% 59.83/59.94 cnf(274,plain,
% 59.83/59.94 (~P11(a1,a19,a15,a16,a1,a15)),
% 59.83/59.94 inference(scs_inference,[],[148,229,250,251,252,253,212,213])).
% 59.83/59.94 cnf(276,plain,
% 59.83/59.94 (~P11(a19,a15,a1,a1,a15,a16)),
% 59.83/59.94 inference(scs_inference,[],[148,229,250,251,252,253,212,213,214])).
% 59.83/59.94 cnf(280,plain,
% 59.83/59.94 (~P3(x2801,x2802,a2,a17)+P3(x2801,x2802,a19,a1)),
% 59.83/59.94 inference(scs_inference,[],[142,145,148,229,250,251,252,253,212,213,214,153,177])).
% 59.83/59.94 cnf(282,plain,
% 59.83/59.94 (~P10(a19,a1,x2821,x2822)+P10(a2,a17,x2821,x2822)),
% 59.83/59.94 inference(scs_inference,[],[142,145,148,229,250,251,252,253,212,213,214,153,177,180])).
% 59.83/59.94 cnf(292,plain,
% 59.83/59.94 (~P4(a16,a15,a1,a16,a1,a15,a19,a1)),
% 59.83/59.94 inference(scs_inference,[],[266,250])).
% 59.83/59.94 cnf(294,plain,
% 59.83/59.94 (~P4(a1,a15,a1,a19,a16,a15,a1,a16)),
% 59.83/59.94 inference(scs_inference,[],[266,268,250,251])).
% 59.83/59.94 cnf(296,plain,
% 59.83/59.94 (~P4(a16,a1,a16,a15,a19,a1,a1,a15)),
% 59.83/59.94 inference(scs_inference,[],[264,266,268,250,251,252])).
% 59.83/59.94 cnf(302,plain,
% 59.83/59.94 (~P4(a1,a16,a19,a1,a16,a15,a1,a15)),
% 59.83/59.94 inference(scs_inference,[],[264,266,268,272,250,251,252,213,214,253])).
% 59.83/59.94 cnf(318,plain,
% 59.83/59.94 (~P4(a16,a15,a16,a1,a1,a15,a19,a1)),
% 59.83/59.94 inference(scs_inference,[],[296,251])).
% 59.83/59.94 cnf(320,plain,
% 59.83/59.94 (~P4(a1,a15,a16,a15,a19,a1,a1,a16)),
% 59.83/59.94 inference(scs_inference,[],[270,296,251,250])).
% 59.83/59.94 cnf(322,plain,
% 59.83/59.94 (~P4(a1,a19,a1,a16,a1,a15,a16,a15)),
% 59.83/59.94 inference(scs_inference,[],[270,296,251,250,252])).
% 59.83/59.94 cnf(326,plain,
% 59.83/59.94 (~P11(a1,a15,a19,a16,a15,a1)),
% 59.83/59.94 inference(scs_inference,[],[270,296,274,276,251,250,252,213,214])).
% 59.83/59.94 cnf(328,plain,
% 59.83/59.94 (~P4(a16,a15,a1,a15,a1,a16,a19,a1)),
% 59.83/59.94 inference(scs_inference,[],[270,292,296,274,276,251,250,252,213,214,253])).
% 59.83/59.94 cnf(330,plain,
% 59.83/59.94 (P1(a16,a16,a19)),
% 59.83/59.95 inference(scs_inference,[],[144,270,292,296,274,276,251,250,252,213,214,253,153])).
% 59.83/59.95 cnf(332,plain,
% 59.83/59.95 (~P11(a15,a1,a16,a15,a19,a1)),
% 59.83/59.95 inference(scs_inference,[],[144,270,292,296,274,276,251,250,252,213,214,253,153,212])).
% 59.83/59.95 cnf(346,plain,
% 59.83/59.95 (~P4(a16,a15,a1,a16,a1,a15,a1,a19)),
% 59.83/59.95 inference(scs_inference,[],[294,250])).
% 59.83/59.95 cnf(348,plain,
% 59.83/59.95 (~P4(a1,a16,a1,a19,a16,a15,a1,a15)),
% 59.83/59.95 inference(scs_inference,[],[294,322,250,251])).
% 59.83/59.95 cnf(350,plain,
% 59.83/59.95 (~P4(a16,a1,a19,a1,a16,a15,a1,a15)),
% 59.83/59.95 inference(scs_inference,[],[302,294,322,250,251,252])).
% 59.83/59.95 cnf(358,plain,
% 59.83/59.95 (~P4(a1,a15,a16,a15,a1,a19,a1,a16)),
% 59.83/59.95 inference(scs_inference,[],[302,294,322,326,332,250,251,252,213,212,214,253])).
% 59.83/59.95 cnf(366,plain,
% 59.83/59.95 (~P4(a1,a16,a16,a15,a1,a19,a1,a15)),
% 59.83/59.95 inference(scs_inference,[],[346,251])).
% 59.83/59.95 cnf(368,plain,
% 59.83/59.95 (~P4(a15,a16,a1,a15,a1,a16,a19,a1)),
% 59.83/59.95 inference(scs_inference,[],[328,346,251,252])).
% 59.83/59.95 cnf(370,plain,
% 59.83/59.95 (~P4(a1,a15,a19,a1,a16,a15,a16,a1)),
% 59.83/59.95 inference(scs_inference,[],[328,318,346,251,252,250])).
% 59.83/59.95 cnf(381,plain,
% 59.83/59.95 (~P4(a15,a1,a16,a15,a19,a1,a1,a16)),
% 59.83/59.95 inference(scs_inference,[],[320,252])).
% 59.83/59.95 cnf(383,plain,
% 59.83/59.95 (~P4(a16,a15,a1,a15,a1,a16,a1,a19)),
% 59.83/59.95 inference(scs_inference,[],[320,348,252,250])).
% 59.83/59.95 cnf(387,plain,
% 59.83/59.95 (~P4(a15,a16,a1,a16,a1,a15,a19,a1)),
% 59.83/59.95 inference(scs_inference,[],[320,348,350,368,252,250,251,253])).
% 59.83/59.95 cnf(389,plain,
% 59.83/59.95 (P1(a19,a19,a16)),
% 59.83/59.95 inference(scs_inference,[],[330,320,348,350,368,252,250,251,253,153])).
% 59.83/59.95 cnf(398,plain,
% 59.83/59.95 (~P4(a19,a1,a1,a16,a15,a1,a16,a15)),
% 59.83/59.95 inference(scs_inference,[],[381,250])).
% 59.83/59.95 cnf(400,plain,
% 59.83/59.95 (~P4(a19,a1,a1,a15,a16,a1,a16,a15)),
% 59.83/59.95 inference(scs_inference,[],[370,381,250,251])).
% 59.83/59.95 cnf(402,plain,
% 59.83/59.95 (~P4(a16,a1,a16,a15,a1,a19,a1,a15)),
% 59.83/59.95 inference(scs_inference,[],[366,370,381,250,251,252])).
% 59.83/59.95 cnf(404,plain,
% 59.83/59.95 (~P4(a1,a15,a16,a15,a19,a1,a16,a1)),
% 59.83/59.95 inference(scs_inference,[],[366,370,381,250,251,252,253])).
% 59.83/59.95 cnf(417,plain,
% 59.83/59.95 (~P4(a1,a16,a15,a16,a19,a1,a1,a15)),
% 59.83/59.95 inference(scs_inference,[],[387,251])).
% 59.83/59.95 cnf(421,plain,
% 59.83/59.95 (~P4(a1,a15,a19,a1,a15,a16,a1,a16)),
% 59.83/59.95 inference(scs_inference,[],[383,387,251,252,250])).
% 59.83/59.95 cnf(423,plain,
% 59.83/59.95 (~P4(a19,a1,a15,a1,a1,a16,a16,a15)),
% 59.83/59.95 inference(scs_inference,[],[383,387,398,251,252,250,253])).
% 59.83/59.95 cnf(436,plain,
% 59.83/59.95 (~P4(a15,a1,a16,a15,a19,a1,a16,a1)),
% 59.83/59.95 inference(scs_inference,[],[404,252])).
% 59.83/59.95 cnf(438,plain,
% 59.83/59.95 (~P4(a1,a19,a1,a15,a16,a1,a16,a15)),
% 59.83/59.95 inference(scs_inference,[],[404,402,252,250])).
% 59.83/59.95 cnf(440,plain,
% 59.83/59.95 (~P4(a16,a15,a16,a1,a1,a15,a1,a19)),
% 59.83/59.95 inference(scs_inference,[],[404,402,252,250,251])).
% 59.83/59.95 cnf(442,plain,
% 59.83/59.95 (~P4(a16,a1,a1,a19,a16,a15,a1,a15)),
% 59.83/59.95 inference(scs_inference,[],[404,402,252,250,251,253])).
% 59.83/59.95 cnf(449,plain,
% 59.83/59.95 (~P4(a19,a1,a1,a15,a1,a16,a15,a16)),
% 59.83/59.95 inference(scs_inference,[],[417,250])).
% 59.83/59.95 cnf(467,plain,
% 59.83/59.95 (~P4(a15,a1,a19,a1,a16,a15,a1,a16)),
% 59.83/59.95 inference(scs_inference,[],[423,251])).
% 59.83/59.95 cnf(469,plain,
% 59.83/59.95 (~P4(a15,a16,a16,a1,a1,a15,a1,a19)),
% 59.83/59.95 inference(scs_inference,[],[440,423,251,252])).
% 59.83/59.95 cnf(471,plain,
% 59.83/59.95 (~P4(a1,a15,a1,a19,a16,a15,a16,a1)),
% 59.83/59.95 inference(scs_inference,[],[440,423,251,252,250])).
% 59.83/59.95 cnf(473,plain,
% 59.83/59.95 (~P4(a16,a15,a1,a15,a16,a1,a1,a19)),
% 59.83/59.95 inference(scs_inference,[],[440,423,251,252,250,253])).
% 59.83/59.95 cnf(480,plain,
% 59.83/59.95 (~P4(a15,a1,a16,a15,a1,a19,a1,a16)),
% 59.83/59.95 inference(scs_inference,[],[358,252])).
% 59.83/59.95 cnf(482,plain,
% 59.83/59.95 (~P4(a19,a1,a16,a1,a15,a1,a16,a15)),
% 59.83/59.95 inference(scs_inference,[],[358,436,252,250])).
% 59.83/59.95 cnf(486,plain,
% 59.83/59.95 (~P4(a19,a1,a1,a16,a1,a15,a15,a16)),
% 59.83/59.95 inference(scs_inference,[],[358,449,436,252,250,251,253])).
% 59.83/59.95 cnf(490,plain,
% 59.83/59.95 (~P11(a1,a19,a16,a15,a1,a16)),
% 59.83/59.95 inference(scs_inference,[],[358,449,436,252,250,251,253,229,213])).
% 59.83/59.95 cnf(492,plain,
% 59.83/59.95 (~P11(a1,a15,a16,a19,a1,a16)),
% 59.83/59.95 inference(scs_inference,[],[358,449,436,252,250,251,253,229,213,212])).
% 59.83/59.95 cnf(494,plain,
% 59.83/59.95 (~P11(a19,a16,a1,a1,a16,a15)),
% 59.83/59.95 inference(scs_inference,[],[358,449,436,252,250,251,253,229,213,212,214])).
% 59.83/59.95 cnf(507,plain,
% 59.83/59.95 (~P4(a15,a1,a1,a19,a16,a15,a16,a1)),
% 59.83/59.95 inference(scs_inference,[],[471,469,492,250,213,251,252])).
% 59.83/59.95 cnf(509,plain,
% 59.83/59.95 (~P11(a1,a16,a15,a19,a16,a1)),
% 59.83/59.95 inference(scs_inference,[],[471,469,492,494,250,213,251,252,212])).
% 59.83/59.95 cnf(511,plain,
% 59.83/59.95 (~P11(a1,a16,a19,a15,a16,a1)),
% 59.83/59.95 inference(scs_inference,[],[471,469,490,492,494,250,213,251,252,212,214])).
% 59.83/59.95 cnf(523,plain,
% 59.83/59.95 (~P11(a16,a1,a15,a16,a19,a1)),
% 59.83/59.95 inference(scs_inference,[],[509,213])).
% 59.83/59.95 cnf(525,plain,
% 59.83/59.95 (~P4(a16,a15,a15,a1,a1,a16,a1,a19)),
% 59.83/59.95 inference(scs_inference,[],[480,509,213,251])).
% 59.83/59.95 cnf(527,plain,
% 59.83/59.95 (~P4(a1,a15,a15,a16,a19,a1,a1,a16)),
% 59.83/59.95 inference(scs_inference,[],[486,480,509,213,251,250])).
% 59.83/59.95 cnf(529,plain,
% 59.83/59.95 (~P4(a1,a19,a1,a16,a1,a15,a15,a16)),
% 59.83/59.95 inference(scs_inference,[],[486,480,509,213,251,250,252])).
% 59.83/59.95 cnf(533,plain,
% 59.83/59.95 (~P11(a16,a15,a1,a16,a1,a19)),
% 59.83/59.95 inference(scs_inference,[],[486,480,509,511,213,251,250,252,212,214])).
% 59.83/59.95 cnf(543,plain,
% 59.83/59.95 (~P11(a16,a19,a1,a16,a1,a15)),
% 59.83/59.95 inference(scs_inference,[],[507,494,251,213])).
% 59.83/59.95 cnf(545,plain,
% 59.83/59.95 (~P4(a16,a15,a16,a1,a15,a1,a1,a19)),
% 59.83/59.95 inference(scs_inference,[],[507,494,251,213,250])).
% 59.83/59.95 cnf(551,plain,
% 59.83/59.95 (~P4(a15,a1,a16,a15,a1,a19,a16,a1)),
% 59.83/59.95 inference(scs_inference,[],[473,507,533,494,251,213,250,252,212,253])).
% 59.83/59.95 cnf(561,plain,
% 59.83/59.95 (~P4(a15,a1,a15,a16,a19,a1,a1,a16)),
% 59.83/59.95 inference(scs_inference,[],[527,529,467,250,251,252])).
% 59.83/59.95 cnf(571,plain,
% 59.83/59.95 (~P4(a16,a1,a19,a1,a16,a15,a15,a1)),
% 59.83/59.95 inference(scs_inference,[],[482,251])).
% 59.83/59.95 cnf(586,plain,
% 59.83/59.95 (~P4(a16,a1,a16,a15,a19,a1,a15,a1)),
% 59.83/59.95 inference(scs_inference,[],[421,551,571,250,251,252,253])).
% 59.83/59.95 cnf(589,plain,
% 59.83/59.95 (~P4(a15,a16,a15,a1,a1,a16,a19,a1)),
% 59.83/59.95 inference(scs_inference,[],[561,251])).
% 59.83/59.95 cnf(609,plain,
% 59.83/59.95 (~P4(a15,a16,a15,a1,a1,a16,a1,a19)),
% 59.83/59.95 inference(scs_inference,[],[525,545,251,252])).
% 59.83/59.95 cnf(631,plain,
% 59.83/59.95 (~P4(a1,a16,a1,a19,a15,a16,a15,a1)),
% 59.83/59.95 inference(scs_inference,[],[609,251,250])).
% 59.83/59.95 cnf(651,plain,
% 59.83/59.95 (~P4(a1,a19,a1,a16,a15,a1,a15,a16)),
% 59.83/59.95 inference(scs_inference,[],[631,251])).
% 59.83/59.95 cnf(825,plain,
% 59.83/59.95 (P1(x8251,x8252,x8253)+~P3(x8252,x8251,x8252,x8253)),
% 59.83/59.95 inference(scs_inference,[],[158,149])).
% 59.83/59.95 cnf(992,plain,
% 59.83/59.95 (P1(x9921,x9922,x9923)+~P3(x9922,x9923,x9922,x9921)),
% 59.83/59.95 inference(scs_inference,[],[825,161])).
% 59.83/59.95 cnf(1008,plain,
% 59.83/59.95 (P1(x10081,x10082,x10083)+~P3(x10082,x10083,x10081,x10082)),
% 59.83/59.95 inference(scs_inference,[],[992,162])).
% 59.83/59.95 cnf(1024,plain,
% 59.83/59.95 (~P4(x10241,x10242,x10243,x10244,x10245,x10241,x10243,x10244)+P1(x10245,x10241,x10242)),
% 59.83/59.95 inference(scs_inference,[],[1008,231])).
% 59.83/59.95 cnf(1057,plain,
% 59.83/59.95 (P10(x10571,x10572,x10573,x10574)+~P10(x10574,x10573,x10571,x10572)),
% 59.83/59.95 inference(scs_inference,[],[163,164])).
% 59.83/59.95 cnf(1089,plain,
% 59.83/59.95 (P6(x10891,x10892,x10893,x10894)+~P6(x10893,x10891,x10892,x10894)),
% 59.83/59.95 inference(scs_inference,[],[167,168])).
% 59.83/59.95 cnf(1121,plain,
% 59.83/59.95 (P4(x11211,x11212,x11213,x11214,a19,a1,x11213,x11214)+~P3(x11211,x11212,a2,a17)),
% 59.83/59.95 inference(scs_inference,[],[280,223])).
% 59.83/59.95 cnf(1137,plain,
% 59.83/59.95 (P10(x11371,x11372,a17,a2)+~P10(a19,a1,x11371,x11372)),
% 59.83/59.95 inference(scs_inference,[],[282,1057])).
% 59.83/59.95 cnf(1153,plain,
% 59.83/59.95 (P6(x11531,x11532,x11533,x11534)+~P6(x11533,x11532,x11531,x11534)),
% 59.83/59.95 inference(scs_inference,[],[1089,168])).
% 59.83/59.95 cnf(1169,plain,
% 59.83/59.95 (~P10(x11691,x11692,a19,a1)+P10(x11691,x11692,a17,a2)),
% 59.83/59.95 inference(scs_inference,[],[1137,163])).
% 59.83/59.95 cnf(1185,plain,
% 59.83/59.95 (P6(x11851,x11852,x11853,x11854)+~P6(x11852,x11853,x11851,x11854)),
% 59.83/59.95 inference(scs_inference,[],[1153,167])).
% 59.83/59.95 cnf(1217,plain,
% 59.83/59.95 (P6(x12171,x12172,x12173,x12174)+~P6(x12172,x12173,x12174,x12171)),
% 59.83/59.95 inference(scs_inference,[],[1185,169])).
% 59.83/59.95 cnf(1249,plain,
% 59.83/59.95 (~P6(x12491,x12492,x12493,x12494)+P6(x12494,x12492,x12493,x12491)),
% 59.83/59.95 inference(scs_inference,[],[1217,1089])).
% 59.83/59.95 cnf(1941,plain,
% 59.83/59.95 (P1(a2,a1,a15)),
% 59.83/59.95 inference(scs_inference,[],[142,149])).
% 59.83/59.95 cnf(1943,plain,
% 59.83/59.95 (P1(a1,a15,a2)),
% 59.83/59.95 inference(scs_inference,[],[142,149,150])).
% 59.83/59.95 cnf(1947,plain,
% 59.83/59.95 (P3(a2,a17,a1,a19)),
% 59.83/59.95 inference(scs_inference,[],[142,145,149,150,161,162])).
% 59.83/59.95 cnf(1951,plain,
% 59.83/59.95 (P3(a19,a1,a19,a1)),
% 59.83/59.95 inference(scs_inference,[],[142,145,149,150,161,162,223,280])).
% 59.83/59.95 cnf(1955,plain,
% 59.83/59.95 (P4(a2,a17,a19,a1,x19551,x19552,x19551,x19552)),
% 59.83/59.95 inference(scs_inference,[],[142,147,145,149,150,161,162,223,280,185,253])).
% 59.83/59.95 cnf(1957,plain,
% 59.83/59.95 (P4(x19571,x19572,a2,a17,x19571,x19572,a19,a1)),
% 59.83/59.95 inference(scs_inference,[],[142,147,145,149,150,161,162,223,280,185,253,251])).
% 59.83/59.95 cnf(1961,plain,
% 59.83/59.95 (P4(a19,a1,x19611,x19612,a2,a17,x19611,x19612)),
% 59.83/59.95 inference(scs_inference,[],[142,147,145,149,150,161,162,223,280,185,253,251,252,250])).
% 59.83/59.95 cnf(1963,plain,
% 59.83/59.95 (P3(a2,a17,a2,a17)),
% 59.83/59.95 inference(scs_inference,[],[142,147,145,149,150,161,162,223,280,185,253,251,252,250,238])).
% 59.83/59.95 cnf(1967,plain,
% 59.83/59.95 (P1(a15,a15,a2)),
% 59.83/59.95 inference(scs_inference,[],[142,147,145,149,150,161,162,223,280,185,253,251,252,250,238,260,153])).
% 59.83/59.95 cnf(1969,plain,
% 59.83/59.95 (P1(a19,a1,a1)),
% 59.83/59.95 inference(scs_inference,[],[142,147,145,149,150,161,162,223,280,185,253,251,252,250,238,260,153,158])).
% 59.83/59.95 cnf(1971,plain,
% 59.83/59.95 (P10(a2,a18,f7(a2,a17,a20,a18),a2)),
% 59.83/59.95 inference(scs_inference,[],[142,147,145,149,150,161,162,223,280,185,253,251,252,250,238,260,153,158,163])).
% 59.83/59.95 cnf(1973,plain,
% 59.83/59.95 (P10(f7(a2,a17,a20,a18),a2,a18,a2)),
% 59.83/59.95 inference(scs_inference,[],[142,147,145,149,150,161,162,223,280,185,253,251,252,250,238,260,153,158,163,164])).
% 59.83/59.95 cnf(1975,plain,
% 59.83/59.95 (P3(a17,a2,a19,a1)),
% 59.83/59.95 inference(scs_inference,[],[142,147,145,149,150,161,162,223,280,185,253,251,252,250,238,260,153,158,163,164,231])).
% 59.83/59.95 cnf(1988,plain,
% 59.83/59.95 (P3(a1,a19,a2,a17)),
% 59.83/59.95 inference(scs_inference,[],[1947,161])).
% 59.83/59.95 cnf(1992,plain,
% 59.83/59.95 (P10(f7(a2,a15,a16,a18),a2,a2,a18)),
% 59.83/59.95 inference(scs_inference,[],[1951,1947,146,161,162,185])).
% 59.83/59.95 cnf(1994,plain,
% 59.83/59.95 (P1(a2,a17,a17)),
% 59.83/59.95 inference(scs_inference,[],[1951,1963,1947,146,161,162,185,158])).
% 59.83/59.95 cnf(1996,plain,
% 59.83/59.95 (P1(a15,a1,a2)),
% 59.83/59.95 inference(scs_inference,[],[1951,1963,1943,1947,146,161,162,185,158,149])).
% 59.83/59.95 cnf(1998,plain,
% 59.83/59.95 (P10(a2,a18,a2,f7(a2,a17,a20,a18))),
% 59.83/59.95 inference(scs_inference,[],[1951,1963,1943,1947,1971,146,161,162,185,158,149,164])).
% 59.83/59.95 cnf(2000,plain,
% 59.83/59.95 (P10(a18,a2,f7(a2,a17,a20,a18),a2)),
% 59.83/59.95 inference(scs_inference,[],[1951,1963,1943,1947,1973,1971,146,161,162,185,158,149,164,163])).
% 59.83/59.95 cnf(2002,plain,
% 59.83/59.95 (P4(a19,a1,x20021,x20022,a19,a1,x20021,x20022)),
% 59.83/59.95 inference(scs_inference,[],[1951,1963,1943,1947,1973,1971,146,161,162,185,158,149,164,163,223])).
% 59.83/59.95 cnf(2008,plain,
% 59.83/59.95 (P4(x20081,x20082,x20081,x20082,a2,a17,a19,a1)),
% 59.83/59.95 inference(scs_inference,[],[1951,1963,1957,1943,1947,1967,1973,1971,146,161,162,185,158,149,164,163,223,280,150,253])).
% 59.83/59.95 cnf(2012,plain,
% 59.83/59.95 (P4(x20121,x20122,a19,a1,x20121,x20122,a2,a17)),
% 59.83/59.95 inference(scs_inference,[],[1951,1963,1955,1957,1943,1947,1967,1973,1971,146,161,162,185,158,149,164,163,223,280,150,253,251,250])).
% 59.83/59.95 cnf(2014,plain,
% 59.83/59.95 (P4(a17,a2,a19,a1,x20141,x20142,x20141,x20142)),
% 59.83/59.95 inference(scs_inference,[],[1951,1963,1955,1957,1943,1947,1967,1973,1971,146,161,162,185,158,149,164,163,223,280,150,253,251,250,252])).
% 59.83/59.95 cnf(2018,plain,
% 59.83/59.95 (P6(a1,a16,a19,a19)),
% 59.83/59.95 inference(scs_inference,[],[1951,1963,1955,1957,1943,1947,1967,1973,1971,389,146,161,162,185,158,149,164,163,223,280,150,253,251,250,252,178,234])).
% 59.83/59.95 cnf(2020,plain,
% 59.83/59.95 (P3(x20201,x20202,x20201,x20202)),
% 59.83/59.95 inference(scs_inference,[],[1951,1963,1955,1957,1943,1947,1967,1973,1971,389,146,145,161,162,185,158,149,164,163,223,280,150,253,251,250,252,178,234,238])).
% 59.83/59.95 cnf(2022,plain,
% 59.83/59.95 (~P4(a2,a17,a1,a15,a16,a1,a16,a15)),
% 59.83/59.95 inference(scs_inference,[],[1951,1963,1955,1957,1961,1943,1947,1967,1973,1971,400,389,146,145,161,162,185,158,149,164,163,223,280,150,253,251,250,252,178,234,238,260])).
% 59.83/59.95 cnf(2027,plain,
% 59.83/59.95 (P1(a19,a19,f13(a1,a1,a1,a1,a19,a19))),
% 59.83/59.95 inference(scs_inference,[],[1951,1963,1955,1957,1961,1943,1947,1967,1969,1973,1971,400,389,146,145,161,162,185,158,149,164,163,223,280,150,253,251,250,252,178,234,238,260,226,204])).
% 59.83/59.95 cnf(2031,plain,
% 59.83/59.95 (P6(a16,a1,a19,a19)),
% 59.83/59.95 inference(scs_inference,[],[1951,1963,1955,1957,1961,1943,1947,1967,1969,1973,1971,400,389,146,145,161,162,185,158,149,164,163,223,280,150,253,251,250,252,178,234,238,260,226,204,205,167])).
% 59.83/59.95 cnf(2033,plain,
% 59.83/59.95 (P6(a1,a19,a16,a19)),
% 59.83/59.95 inference(scs_inference,[],[1951,1963,1955,1957,1961,1943,1947,1967,1969,1973,1971,400,389,146,145,161,162,185,158,149,164,163,223,280,150,253,251,250,252,178,234,238,260,226,204,205,167,168])).
% 59.83/59.95 cnf(2035,plain,
% 59.83/59.95 (P6(a1,a19,a19,a16)),
% 59.83/59.95 inference(scs_inference,[],[1951,1963,1955,1957,1961,1943,1947,1967,1969,1973,1971,400,389,146,145,161,162,185,158,149,164,163,223,280,150,253,251,250,252,178,234,238,260,226,204,205,167,168,169])).
% 59.83/59.95 cnf(2037,plain,
% 59.83/59.95 (P6(a19,a16,a19,a1)),
% 59.83/59.95 inference(scs_inference,[],[1951,1963,1955,1957,1961,1943,1947,1967,1969,1973,1971,400,389,146,145,161,162,185,158,149,164,163,223,280,150,253,251,250,252,178,234,238,260,226,204,205,167,168,169,1249])).
% 59.83/59.95 cnf(2041,plain,
% 59.83/59.95 (P9(a1,a1,a19,a1,a1,a1,a19,a1)),
% 59.83/59.95 inference(scs_inference,[],[1951,1963,1955,1957,1961,1943,1947,1967,1969,1973,1971,400,389,146,145,161,162,185,158,149,164,163,223,280,150,253,251,250,252,178,234,238,260,226,204,205,167,168,169,1249,222,255])).
% 59.83/59.95 cnf(2043,plain,
% 59.83/59.95 (P9(a1,a19,a1,a1,a19,a1,a1,a1)),
% 59.83/59.95 inference(scs_inference,[],[1951,1963,1955,1957,1961,1943,1947,1967,1969,1973,1971,400,389,146,145,161,162,185,158,149,164,163,223,280,150,253,251,250,252,178,234,238,260,226,204,205,167,168,169,1249,222,255,256])).
% 59.83/59.95 cnf(2045,plain,
% 59.83/59.95 (P9(a19,a1,a19,a1,a1,a1,a1,a1)),
% 59.83/59.95 inference(scs_inference,[],[1951,1963,1955,1957,1961,1943,1947,1967,1969,1973,1971,400,389,146,145,161,162,185,158,149,164,163,223,280,150,253,251,250,252,178,234,238,260,226,204,205,167,168,169,1249,222,255,256,257])).
% 59.83/59.95 cnf(2049,plain,
% 59.83/59.95 (P9(a19,a1,a1,a1,a1,a19,a1,a1)),
% 59.83/59.95 inference(scs_inference,[],[1951,1963,1955,1957,1961,1943,1947,1967,1969,1973,1971,400,389,146,145,161,162,185,158,149,164,163,223,280,150,253,251,250,252,178,234,238,260,226,204,205,167,168,169,1249,222,255,256,257,171,254])).
% 59.83/59.95 cnf(2055,plain,
% 59.83/59.95 (P6(a16,a19,a1,a19)),
% 59.83/59.95 inference(scs_inference,[],[2031,2041,257,168])).
% 59.83/59.95 cnf(2059,plain,
% 59.83/59.95 (P4(a16,a1,a16,a19,a19,a1,a19,a19)),
% 59.83/59.95 inference(scs_inference,[],[2031,2033,2041,2045,257,168,256,222])).
% 59.83/59.95 cnf(2061,plain,
% 59.83/59.95 (P6(a19,a16,a1,a19)),
% 59.83/59.95 inference(scs_inference,[],[2031,2033,2037,2041,2045,257,168,256,222,169])).
% 59.83/59.95 cnf(2063,plain,
% 59.83/59.95 (P1(x20631,x20632,x20632)),
% 59.83/59.95 inference(scs_inference,[],[2020,2031,2033,2037,2041,2045,257,168,256,222,169,158])).
% 59.83/59.95 cnf(2065,plain,
% 59.83/59.95 (P6(a19,a1,a16,a19)),
% 59.83/59.95 inference(scs_inference,[],[2020,2031,2033,2037,2041,2045,257,168,256,222,169,158,167])).
% 59.83/59.95 cnf(2069,plain,
% 59.83/59.95 (P9(a1,a1,a1,a19,a1,a1,a19,a1)),
% 59.83/59.95 inference(scs_inference,[],[2020,1975,2031,2033,2037,2041,2043,2045,257,168,256,222,169,158,167,161,255])).
% 59.83/59.95 cnf(2071,plain,
% 59.83/59.95 (P6(a19,a1,a19,a16)),
% 59.83/59.95 inference(scs_inference,[],[2020,1975,2031,2033,2037,2041,2043,2045,257,168,256,222,169,158,167,161,255,1249])).
% 59.83/59.95 cnf(2075,plain,
% 59.83/59.95 (P3(x20751,x20752,x20752,x20751)),
% 59.83/59.95 inference(scs_inference,[],[2020,1975,2031,2033,2037,2041,2043,2045,1998,257,168,256,222,169,158,167,161,255,1249,163,162])).
% 59.83/59.95 cnf(2077,plain,
% 59.83/59.95 (P4(x20771,x20772,x20773,x20774,x20771,x20772,x20773,x20774)),
% 59.83/59.95 inference(scs_inference,[],[2020,1975,2031,2033,2037,2041,2043,2045,1998,257,168,256,222,169,158,167,161,255,1249,163,162,223])).
% 59.83/59.95 cnf(2079,plain,
% 59.83/59.95 (P1(a17,a2,a17)),
% 59.83/59.95 inference(scs_inference,[],[2020,1975,1994,2031,2033,2037,2041,2043,2045,1998,257,168,256,222,169,158,167,161,255,1249,163,162,223,149])).
% 59.83/59.95 cnf(2081,plain,
% 59.83/59.95 (P1(a15,a2,a1)),
% 59.83/59.95 inference(scs_inference,[],[2020,1975,1994,1996,2031,2033,2037,2041,2043,2045,1998,257,168,256,222,169,158,167,161,255,1249,163,162,223,149,150])).
% 59.83/59.95 cnf(2085,plain,
% 59.83/59.95 (P4(a19,a1,a19,a1,x20851,x20852,x20851,x20852)),
% 59.83/59.95 inference(scs_inference,[],[2020,1975,2002,1994,1996,2031,2033,2037,2041,2043,2045,1998,2000,257,168,256,222,169,158,167,161,255,1249,163,162,223,149,150,164,253])).
% 59.83/59.95 cnf(2087,plain,
% 59.83/59.95 (P4(a1,a19,x20871,x20872,a19,a1,x20871,x20872)),
% 59.83/59.95 inference(scs_inference,[],[2020,1975,2002,1994,1996,2031,2033,2037,2041,2043,2045,1998,2000,257,168,256,222,169,158,167,161,255,1249,163,162,223,149,150,164,253,252])).
% 59.83/59.95 cnf(2093,plain,
% 59.83/59.95 (P6(a16,a19,a19,a19)),
% 59.83/59.95 inference(scs_inference,[],[2020,1975,2002,2008,2014,1994,1996,2018,2031,2033,2037,2041,2043,2045,1998,2000,257,168,256,222,169,158,167,161,255,1249,163,162,223,149,150,164,253,252,251,250,183])).
% 59.83/59.95 cnf(2095,plain,
% 59.83/59.95 (P1(f4(a2,a2,a18),a18,a2)),
% 59.83/59.95 inference(scs_inference,[],[2020,1975,2002,2008,2014,1994,1996,2018,2031,2033,2037,2041,2043,2045,1998,2000,257,168,256,222,169,158,167,161,255,1249,163,162,223,149,150,164,253,252,251,250,183,175])).
% 59.83/59.95 cnf(2097,plain,
% 59.83/59.95 (P1(f5(a2,a2,a18),a18,a2)),
% 59.83/59.95 inference(scs_inference,[],[2020,1975,2002,2008,2014,1994,1996,2018,2031,2033,2037,2041,2043,2045,1998,2000,257,168,256,222,169,158,167,161,255,1249,163,162,223,149,150,164,253,252,251,250,183,175,176])).
% 59.83/59.95 cnf(2099,plain,
% 59.83/59.95 (P10(a2,f4(a2,a2,a18),a18,a2)),
% 59.83/59.95 inference(scs_inference,[],[2020,1975,2002,2008,2014,1994,1996,2018,2031,2033,2037,2041,2043,2045,1998,2000,257,168,256,222,169,158,167,161,255,1249,163,162,223,149,150,164,253,252,251,250,183,175,176,187])).
% 59.83/59.95 cnf(2101,plain,
% 59.83/59.95 (P10(a2,f5(a2,a2,a18),a18,a2)),
% 59.83/59.95 inference(scs_inference,[],[2020,1975,2002,2008,2014,1994,1996,2018,2031,2033,2037,2041,2043,2045,1998,2000,257,168,256,222,169,158,167,161,255,1249,163,162,223,149,150,164,253,252,251,250,183,175,176,187,188])).
% 59.83/59.95 cnf(2103,plain,
% 59.83/59.95 (P9(a19,a1,a19,a1,a19,a1,a19,a1)),
% 59.83/59.95 inference(scs_inference,[],[2020,1975,2002,2008,2014,1994,1996,2018,2031,2033,2037,2041,2043,2045,1998,2000,257,168,256,222,169,158,167,161,255,1249,163,162,223,149,150,164,253,252,251,250,183,175,176,187,188,261])).
% 59.83/59.95 cnf(2105,plain,
% 59.83/59.95 (P6(a1,f13(a1,a1,a1,a1,a19,a19),a19,a19)),
% 59.83/59.95 inference(scs_inference,[],[2020,1975,2002,2008,2014,1994,1996,2018,2031,2033,2037,2041,2043,2045,1998,2000,2027,257,168,256,222,169,158,167,161,255,1249,163,162,223,149,150,164,253,252,251,250,183,175,176,187,188,261,234])).
% 59.83/59.95 cnf(2111,plain,
% 59.83/59.95 (P1(f13(a2,a15,a15,a2,a1,a1),a15,a2)),
% 59.83/59.95 inference(scs_inference,[],[142,2020,1975,2002,2008,2012,2014,1994,1996,2018,2031,2033,2037,2041,2043,2045,1998,2000,2027,1943,257,168,256,222,169,158,167,161,255,1249,163,162,223,149,150,164,253,252,251,250,183,175,176,187,188,261,234,260,205])).
% 59.83/59.95 cnf(2117,plain,
% 59.83/59.95 (P9(a1,a1,a1,a1,a1,a19,a19,a1)),
% 59.83/59.95 inference(scs_inference,[],[142,2020,1975,2002,2008,2012,2014,1994,1996,2018,2031,2033,2037,2041,2043,2045,1998,2000,2027,1943,257,168,256,222,169,158,167,161,255,1249,163,162,223,149,150,164,253,252,251,250,183,175,176,187,188,261,234,260,205,204,1024,254])).
% 59.83/59.95 cnf(2120,plain,
% 59.83/59.95 (P4(a2,f7(a2,a17,a20,a18),a2,a17,a20,a2,a20,a17)),
% 59.83/59.95 inference(scs_inference,[],[142,2020,1975,2002,2008,2012,2014,1994,1996,2018,2031,2033,2037,2041,2043,2045,1998,2000,2027,543,1943,147,257,168,256,222,169,158,167,161,255,1249,163,162,223,149,150,164,253,252,251,250,183,175,176,187,188,261,234,260,205,204,1024,254,111,227])).
% 59.83/59.95 cnf(2125,plain,
% 59.83/59.95 (P9(a1,a19,a1,a1,a1,a19,a1,a1)),
% 59.83/59.95 inference(scs_inference,[],[2049,256])).
% 59.83/59.95 cnf(2127,plain,
% 59.83/59.95 (P4(a19,a1,a19,a19,a16,a1,a16,a19)),
% 59.83/59.95 inference(scs_inference,[],[2049,2035,256,222])).
% 59.83/59.95 cnf(2129,plain,
% 59.83/59.95 (P9(a19,a1,a1,a19,a1,a1,a1,a1)),
% 59.83/59.95 inference(scs_inference,[],[2049,2035,256,222,257])).
% 59.83/59.95 cnf(2131,plain,
% 59.83/59.95 (P9(a1,a1,a19,a1,a1,a1,a1,a19)),
% 59.83/59.95 inference(scs_inference,[],[2049,2035,2069,256,222,257,254])).
% 59.83/59.95 cnf(2133,plain,
% 59.83/59.95 (P6(a19,a16,a19,a19)),
% 59.83/59.95 inference(scs_inference,[],[2049,2035,2069,2093,256,222,257,254,167])).
% 59.83/59.95 cnf(2135,plain,
% 59.83/59.95 (P6(a19,a19,a1,a16)),
% 59.83/59.95 inference(scs_inference,[],[2049,2035,2069,2071,2093,256,222,257,254,167,168])).
% 59.83/59.95 cnf(2137,plain,
% 59.83/59.95 (P6(a16,a19,a19,a1)),
% 59.83/59.95 inference(scs_inference,[],[2049,2035,2055,2069,2071,2093,256,222,257,254,167,168,169])).
% 59.83/59.95 cnf(2145,plain,
% 59.83/59.95 (P3(a1,a19,a17,a2)),
% 59.83/59.95 inference(scs_inference,[],[2049,2035,2055,2069,2071,2093,2117,1992,1988,256,222,257,254,167,168,169,163,1249,255,162])).
% 59.83/59.95 cnf(2147,plain,
% 59.83/59.95 (P1(x21471,x21472,x21471)),
% 59.83/59.95 inference(scs_inference,[],[2063,2049,2035,2055,2069,2071,2093,2117,1992,1988,256,222,257,254,167,168,169,163,1249,255,162,149])).
% 59.83/59.95 cnf(2149,plain,
% 59.83/59.95 (P4(x21491,x21492,x21493,x21494,x21492,x21491,x21493,x21494)),
% 59.83/59.95 inference(scs_inference,[],[2075,2063,2049,2035,2055,2069,2071,2093,2117,1992,1988,256,222,257,254,167,168,169,163,1249,255,162,149,223])).
% 59.83/59.95 cnf(2155,plain,
% 59.83/59.95 (P4(x21551,x21552,x21551,x21552,x21553,x21554,x21553,x21554)),
% 59.83/59.95 inference(scs_inference,[],[2075,2077,2063,2049,2035,2055,2069,2071,2079,2093,2117,1992,1988,256,222,257,254,167,168,169,163,1249,255,162,149,223,150,164,253])).
% 59.83/59.95 cnf(2161,plain,
% 59.83/59.95 (P4(a1,a19,a19,a1,x21611,x21612,x21611,x21612)),
% 59.83/59.95 inference(scs_inference,[],[2075,2077,2063,2049,2035,2085,2087,2055,2069,2071,2079,2093,2117,1992,2120,1988,256,222,257,254,167,168,169,163,1249,255,162,149,223,150,164,253,251,250,252])).
% 59.83/59.95 cnf(2163,plain,
% 59.83/59.95 (P6(x21631,x21632,x21632,x21632)),
% 59.83/59.95 inference(scs_inference,[],[2075,2077,2063,2049,2035,2085,2087,2055,2069,2071,2079,2093,2117,1992,2120,1988,256,222,257,254,167,168,169,163,1249,255,162,149,223,150,164,253,251,250,252,234])).
% 59.83/59.95 cnf(2164,plain,
% 59.83/59.95 (P4(x21641,x21642,x21643,x21644,x21641,x21642,x21643,x21644)),
% 59.83/59.95 inference(rename_variables,[],[2077])).
% 59.83/59.95 cnf(2165,plain,
% 59.83/59.95 (P1(x21651,x21652,x21652)),
% 59.83/59.95 inference(rename_variables,[],[2063])).
% 59.83/59.95 cnf(2167,plain,
% 59.83/59.95 (P3(a17,a2,a1,a19)),
% 59.83/59.95 inference(scs_inference,[],[2075,2077,2063,2049,2035,2085,2087,2055,2069,2071,2079,2093,2117,1992,2120,1988,1975,256,222,257,254,167,168,169,163,1249,255,162,149,223,150,164,253,251,250,252,234,177])).
% 59.83/59.95 cnf(2168,plain,
% 59.83/59.95 (P3(x21681,x21682,x21682,x21681)),
% 59.83/59.95 inference(rename_variables,[],[2075])).
% 59.83/59.95 cnf(2171,plain,
% 59.83/59.95 (P3(x21711,x21712,x21712,x21711)),
% 59.83/59.95 inference(rename_variables,[],[2075])).
% 59.83/59.95 cnf(2174,plain,
% 59.83/59.95 (P3(x21741,x21742,x21741,x21742)),
% 59.83/59.95 inference(rename_variables,[],[2020])).
% 59.83/59.95 cnf(2175,plain,
% 59.83/59.95 (P1(x21751,x21752,x21752)),
% 59.83/59.95 inference(rename_variables,[],[2063])).
% 59.83/59.95 cnf(2182,plain,
% 59.83/59.95 (P4(x21821,x21822,x21823,x21824,x21821,x21822,x21823,x21824)),
% 59.83/59.95 inference(rename_variables,[],[2077])).
% 59.83/59.95 cnf(2187,plain,
% 59.83/59.95 (P5(a2,a2,a2,a2)),
% 59.83/59.95 inference(scs_inference,[],[142,2075,2168,2171,2077,2164,2182,2063,2165,2175,2049,2035,2085,2087,2055,2069,2071,2079,2093,2117,1992,2120,1988,1975,2020,2174,256,222,257,254,167,168,169,163,1249,255,162,149,223,150,164,253,251,250,252,234,177,180,205,204,232,226,249])).
% 59.83/59.95 cnf(2190,plain,
% 59.83/59.95 (P10(a2,a2,a2,a2)),
% 59.83/59.95 inference(scs_inference,[],[142,2075,2168,2171,2077,2164,2182,2063,2165,2175,2049,2035,2085,2087,2055,2069,2071,2079,2093,2117,1992,2120,1988,1975,2020,2174,256,222,257,254,167,168,169,163,1249,255,162,149,223,150,164,253,251,250,252,234,177,180,205,204,232,226,249,179])).
% 59.83/59.95 cnf(2192,plain,
% 59.83/59.95 (P2(a2,a2,a2,a2)),
% 59.83/59.95 inference(scs_inference,[],[142,2075,2168,2171,2077,2164,2182,2063,2165,2175,2049,2035,2085,2087,2055,2069,2071,2079,2093,2117,1992,2120,1988,1975,2020,2174,256,222,257,254,167,168,169,163,1249,255,162,149,223,150,164,253,251,250,252,234,177,180,205,204,232,226,249,179,182])).
% 59.83/59.95 cnf(2196,plain,
% 59.83/59.95 (P10(f7(a2,a2,a2,a2),a2,a2,a2)),
% 59.83/59.95 inference(scs_inference,[],[2192,185])).
% 59.83/59.95 cnf(2202,plain,
% 59.83/59.95 (P9(a1,a19,a19,a1,a19,a1,a19,a1)),
% 59.83/59.95 inference(scs_inference,[],[2103,2125,2192,185,257,254,256])).
% 59.83/59.95 cnf(2206,plain,
% 59.83/59.95 (P4(a1,a19,a1,a16,a19,a19,a19,a16)),
% 59.83/59.95 inference(scs_inference,[],[2061,2135,2103,2125,2192,185,257,254,256,169,222])).
% 59.83/59.95 cnf(2216,plain,
% 59.83/59.95 (P6(x22161,x22161,x22161,x22162)),
% 59.83/59.95 inference(scs_inference,[],[2163,2061,2135,2103,2125,2192,2099,2095,185,257,254,256,169,222,167,149,163,255,1249])).
% 59.83/59.95 cnf(2220,plain,
% 59.83/59.95 (P1(x22201,x22201,x22202)),
% 59.83/59.95 inference(scs_inference,[],[2163,2147,2061,2135,2103,2125,2133,2192,2099,2095,185,257,254,256,169,222,167,149,163,255,1249,168,150])).
% 59.83/59.95 cnf(2222,plain,
% 59.83/59.95 (P4(a1,a19,x22221,x22222,a17,a2,x22221,x22222)),
% 59.83/59.95 inference(scs_inference,[],[2163,2147,2145,2061,2135,2103,2125,2133,2192,2099,2095,185,257,254,256,169,222,167,149,163,255,1249,168,150,223])).
% 59.83/59.95 cnf(2226,plain,
% 59.83/59.95 (P4(x22261,x22262,x22262,x22261,x22263,x22264,x22263,x22264)),
% 59.83/59.95 inference(scs_inference,[],[2149,2163,2147,2145,2061,2135,2103,2125,2133,2192,2099,2095,185,257,254,256,169,222,167,149,163,255,1249,168,150,223,164,253])).
% 59.83/59.95 cnf(2230,plain,
% 59.83/59.95 (P4(x22301,x22302,x22303,x22304,x22301,x22302,x22304,x22303)),
% 59.83/59.95 inference(scs_inference,[],[2149,2163,2147,2145,2061,2127,2135,2103,2125,2133,2192,2099,2095,185,257,254,256,169,222,167,149,163,255,1249,168,150,223,164,253,252,251])).
% 59.83/59.95 cnf(2236,plain,
% 59.83/59.95 (P2(f8(a2,a2,a2),a2,a2,a2)),
% 59.83/59.95 inference(scs_inference,[],[2149,2163,2147,2145,2061,2127,2135,2187,2161,2103,2125,2133,2190,2192,2099,2095,185,257,254,256,169,222,167,149,163,255,1249,168,150,223,164,253,252,251,250,186,189])).
% 59.83/59.95 cnf(2237,plain,
% 59.83/59.95 (P6(x22371,x22372,x22372,x22372)),
% 59.83/59.95 inference(rename_variables,[],[2163])).
% 59.83/59.95 cnf(2239,plain,
% 59.83/59.95 (P1(f12(a2,a2,a2,x22391,a2),x22391,a2)),
% 59.83/59.95 inference(scs_inference,[],[2149,2163,2147,2145,2061,2127,2135,2187,2161,2103,2125,2133,2190,2192,2099,2095,185,257,254,256,169,222,167,149,163,255,1249,168,150,223,164,253,252,251,250,186,189,195])).
% 59.83/59.95 cnf(2240,plain,
% 59.83/59.95 (P1(x22401,x22402,x22401)),
% 59.83/59.95 inference(rename_variables,[],[2147])).
% 59.83/59.95 cnf(2243,plain,
% 59.83/59.95 (P4(x22431,x22432,x22433,x22434,x22432,x22431,x22433,x22434)),
% 59.83/59.95 inference(rename_variables,[],[2149])).
% 59.83/59.95 cnf(2245,plain,
% 59.83/59.95 (P10(f12(a2,a2,a2,x22451,a2),a2,x22451,a2)),
% 59.83/59.95 inference(scs_inference,[],[2149,2163,2147,2240,2145,2061,2127,2135,2187,2161,2103,2125,2133,2190,2192,2099,2095,185,257,254,256,169,222,167,149,163,255,1249,168,150,223,164,253,252,251,250,186,189,195,239,196])).
% 59.83/59.95 cnf(2246,plain,
% 59.83/59.95 (P1(x22461,x22462,x22461)),
% 59.83/59.95 inference(rename_variables,[],[2147])).
% 59.83/59.95 cnf(2248,plain,
% 59.83/59.95 (P5(a2,a2,a2,f27(a2,a2,a2,a2,a2))),
% 59.83/59.95 inference(scs_inference,[],[2149,2163,2147,2240,2145,2061,2127,2135,2187,2161,2103,2125,2133,2190,2192,2099,2095,185,257,254,256,169,222,167,149,163,255,1249,168,150,223,164,253,252,251,250,186,189,195,239,196,197])).
% 59.83/59.95 cnf(2250,plain,
% 59.83/59.95 (P3(f27(a2,a2,a2,a2,a2),a2,a2,a2)),
% 59.83/59.95 inference(scs_inference,[],[2149,2163,2147,2240,2145,2061,2127,2135,2187,2161,2103,2125,2133,2190,2192,2099,2095,185,257,254,256,169,222,167,149,163,255,1249,168,150,223,164,253,252,251,250,186,189,195,239,196,197,199])).
% 59.83/59.95 cnf(2252,plain,
% 59.83/59.95 (P2(a2,a2,f3(a2,a2,a2),f3(a2,a2,a2))),
% 59.83/59.95 inference(scs_inference,[],[2149,2163,2147,2240,2145,2061,2127,2135,2187,2161,2103,2125,2133,2190,2192,2099,2095,185,257,254,256,169,222,167,149,163,255,1249,168,150,223,164,253,252,251,250,186,189,195,239,196,197,199,182])).
% 59.83/59.95 cnf(2258,plain,
% 59.83/59.95 (P3(a2,f27(a2,a2,a2,a2,a2),a2,a2)),
% 59.83/59.95 inference(scs_inference,[],[2149,2243,2163,2147,2240,2145,2061,2127,2135,2187,2161,2103,2125,2133,2190,2192,2099,2095,185,257,254,256,169,222,167,149,163,255,1249,168,150,223,164,253,252,251,250,186,189,195,239,196,197,199,182,187,188,238])).
% 59.83/59.95 cnf(2259,plain,
% 59.83/59.95 (P4(x22591,x22592,x22593,x22594,x22592,x22591,x22593,x22594)),
% 59.83/59.95 inference(rename_variables,[],[2149])).
% 59.83/59.95 cnf(2261,plain,
% 59.83/59.95 (~P4(a17,a2,a1,a15,a16,a1,a16,a15)),
% 59.83/59.95 inference(scs_inference,[],[2149,2243,2259,2163,2147,2240,2145,2061,2127,2135,2187,2161,2022,2103,2125,2133,2190,2192,2099,2095,185,257,254,256,169,222,167,149,163,255,1249,168,150,223,164,253,252,251,250,186,189,195,239,196,197,199,182,187,188,238,260])).
% 59.83/59.95 cnf(2262,plain,
% 59.83/59.95 (P4(x22621,x22622,x22623,x22624,x22622,x22621,x22623,x22624)),
% 59.83/59.95 inference(rename_variables,[],[2149])).
% 59.83/59.95 cnf(2264,plain,
% 59.83/59.95 (P6(a15,a15,a1,a2)),
% 59.83/59.95 inference(scs_inference,[],[142,2149,2243,2259,2155,2163,2147,2240,2145,2061,2127,2135,2187,2161,2022,2103,2125,2133,2190,2192,2099,2095,185,257,254,256,169,222,167,149,163,255,1249,168,150,223,164,253,252,251,250,186,189,195,239,196,197,199,182,187,188,238,260,234])).
% 59.83/59.95 cnf(2267,plain,
% 59.83/59.95 (P8(a2,a2,a2)),
% 59.83/59.96 inference(scs_inference,[],[142,2149,2243,2259,2262,2155,2163,2147,2240,2246,2145,2061,2127,2135,2187,2161,2022,2103,2125,2133,2190,2192,2099,2095,185,257,254,256,169,222,167,149,163,255,1249,168,150,223,164,253,252,251,250,186,189,195,239,196,197,199,182,187,188,238,260,234,237])).
% 59.83/59.96 cnf(2268,plain,
% 59.83/59.96 (P1(x22681,x22682,x22681)),
% 59.83/59.96 inference(rename_variables,[],[2147])).
% 59.83/59.96 cnf(2269,plain,
% 59.83/59.96 (P4(x22691,x22692,x22693,x22694,x22692,x22691,x22693,x22694)),
% 59.83/59.96 inference(rename_variables,[],[2149])).
% 59.83/59.96 cnf(2271,plain,
% 59.83/59.96 (P2(f9(a2,a2,a2),a2,a2,a2)),
% 59.83/59.96 inference(scs_inference,[],[142,2149,2243,2259,2262,2155,2163,2237,2147,2240,2246,2145,2061,2127,2135,2187,2161,2022,2103,2125,2133,2190,2192,2099,2095,2075,185,257,254,256,169,222,167,149,163,255,1249,168,150,223,164,253,252,251,250,186,189,195,239,196,197,199,182,187,188,238,260,234,237,190])).
% 59.83/59.96 cnf(2272,plain,
% 59.83/59.96 (P3(x22721,x22722,x22722,x22721)),
% 59.83/59.96 inference(rename_variables,[],[2075])).
% 59.83/59.96 cnf(2273,plain,
% 59.83/59.96 (P6(x22731,x22732,x22732,x22732)),
% 59.83/59.96 inference(rename_variables,[],[2163])).
% 59.83/59.96 cnf(2278,plain,
% 59.83/59.96 (P5(x22781,x22781,x22781,x22781)),
% 59.83/59.96 inference(scs_inference,[],[142,2149,2243,2259,2262,2269,2155,2163,2237,2273,2147,2240,2246,2145,2061,2127,2135,2187,2161,2022,2103,2125,2133,2190,2192,2099,2095,2075,2272,1943,185,257,254,256,169,222,167,149,163,255,1249,168,150,223,164,253,252,251,250,186,189,195,239,196,197,199,182,187,188,238,260,234,237,190,205,249])).
% 59.83/59.96 cnf(2281,plain,
% 59.83/59.96 (P6(x22811,x22812,x22812,x22812)),
% 59.83/59.96 inference(rename_variables,[],[2163])).
% 59.83/59.96 cnf(2283,plain,
% 59.83/59.96 (P8(f21(a2,x22831),a2,x22831)),
% 59.83/59.96 inference(scs_inference,[],[142,2149,2243,2259,2262,2269,2155,2163,2237,2273,2147,2240,2246,2268,2145,2061,2127,2135,2187,2161,2022,2103,2125,2133,2190,2192,2099,2095,2075,2272,2063,1943,185,257,254,256,169,222,167,149,163,255,1249,168,150,223,164,253,252,251,250,186,189,195,239,196,197,199,182,187,188,238,260,234,237,190,205,249,157])).
% 59.83/59.96 cnf(2289,plain,
% 59.83/59.96 (P5(f21(a2,x22891),a2,f21(a2,x22891),x22891)),
% 59.83/59.96 inference(scs_inference,[],[142,2149,2243,2259,2262,2269,2155,2163,2237,2273,2147,2240,2246,2268,2145,2061,2127,2135,2187,2161,2022,2103,2125,2133,2190,2192,2099,2095,2075,2272,2063,1943,185,257,254,256,169,222,167,149,163,255,1249,168,150,223,164,253,252,251,250,186,189,195,239,196,197,199,182,187,188,238,260,234,237,190,205,249,157,151,154])).
% 59.83/59.96 cnf(2297,plain,
% 59.83/59.96 (P3(a2,a2,a2,f3(a2,a2,a2))),
% 59.83/59.96 inference(scs_inference,[],[142,2149,2243,2259,2262,2269,2155,2163,2237,2273,2147,2240,2246,2268,2145,2061,2127,2135,2187,2161,2022,2103,2125,2133,2190,2192,2099,2095,2075,2272,2063,1943,185,257,254,256,169,222,167,149,163,255,1249,168,150,223,164,253,252,251,250,186,189,195,239,196,197,199,182,187,188,238,260,234,237,190,205,249,157,151,154,165,166,224,231])).
% 59.83/59.96 cnf(2299,plain,
% 59.83/59.96 (P3(a2,a2,f27(a2,a2,a2,a2,a2),a2)),
% 59.83/59.96 inference(scs_inference,[],[142,2149,2243,2259,2262,2269,2155,2163,2237,2273,2147,2240,2246,2268,2145,2061,2127,2135,2187,2161,2022,2103,2125,2133,2190,2192,2099,2095,2075,2272,2063,1943,185,257,254,256,169,222,167,149,163,255,1249,168,150,223,164,253,252,251,250,186,189,195,239,196,197,199,182,187,188,238,260,234,237,190,205,249,157,151,154,165,166,224,231,161])).
% 59.83/59.96 cnf(2303,plain,
% 59.83/59.96 (P8(f21(a2,x23031),x23031,a2)),
% 59.83/59.96 inference(scs_inference,[],[142,2149,2243,2259,2262,2269,2155,2163,2237,2273,2147,2240,2246,2268,2145,2061,2127,2135,2187,2161,2022,2103,2125,2133,2190,2192,2099,2095,2075,2272,2063,1943,185,257,254,256,169,222,167,149,163,255,1249,168,150,223,164,253,252,251,250,186,189,195,239,196,197,199,182,187,188,238,260,234,237,190,205,249,157,151,154,165,166,224,231,161,162,152])).
% 59.83/59.96 cnf(2305,plain,
% 59.83/59.96 (P3(a2,a2,x23051,x23051)),
% 59.83/59.96 inference(scs_inference,[],[142,2149,2243,2259,2262,2269,2155,2163,2237,2273,2147,2240,2246,2268,2145,2061,2127,2135,2187,2161,2022,2103,2125,2133,2190,2192,2099,2095,2075,2272,2063,1943,185,257,254,256,169,222,167,149,163,255,1249,168,150,223,164,253,252,251,250,186,189,195,239,196,197,199,182,187,188,238,260,234,237,190,205,249,157,151,154,165,166,224,231,161,162,152,155])).
% 59.83/59.96 cnf(2307,plain,
% 59.83/59.96 (P3(f21(a2,x23071),a2,x23071,a2)),
% 59.83/59.96 inference(scs_inference,[],[142,2149,2243,2259,2262,2269,2155,2163,2237,2273,2147,2240,2246,2268,2145,2061,2127,2135,2187,2161,2022,2103,2125,2133,2190,2192,2099,2095,2075,2272,2063,1943,185,257,254,256,169,222,167,149,163,255,1249,168,150,223,164,253,252,251,250,186,189,195,239,196,197,199,182,187,188,238,260,234,237,190,205,249,157,151,154,165,166,224,231,161,162,152,155,156])).
% 59.83/59.96 cnf(2309,plain,
% 59.83/59.96 (~P5(a2,f27(a2,a2,a2,a2,a2),x23091,x23092)+P5(a2,a2,x23091,x23092)),
% 59.83/59.96 inference(scs_inference,[],[142,2149,2243,2259,2262,2269,2155,2163,2237,2273,2147,2240,2246,2268,2145,2061,2127,2135,2187,2161,2022,2103,2125,2133,2190,2192,2099,2095,2075,2272,2063,1943,185,257,254,256,169,222,167,149,163,255,1249,168,150,223,164,253,252,251,250,186,189,195,239,196,197,199,182,187,188,238,260,234,237,190,205,249,157,151,154,165,166,224,231,161,162,152,155,156,181])).
% 59.83/59.96 cnf(2311,plain,
% 59.83/59.96 (P9(a2,a2,a2,a2,f21(a2,x23111),a2,a2,x23111)),
% 59.83/59.96 inference(scs_inference,[],[142,2149,2243,2259,2262,2269,2155,2163,2237,2273,2147,2240,2246,2268,2145,2061,2127,2135,2187,2161,2022,2103,2125,2133,2190,2192,2099,2095,2075,2272,2063,1943,185,257,254,256,169,222,167,149,163,255,1249,168,150,223,164,253,252,251,250,186,189,195,239,196,197,199,182,187,188,238,260,234,237,190,205,249,157,151,154,165,166,224,231,161,162,152,155,156,181,221])).
% 59.83/59.96 cnf(2318,plain,
% 59.83/59.96 (P5(a19,a1,a1,a19)),
% 59.83/59.96 inference(scs_inference,[],[142,2149,2243,2259,2262,2269,2155,2163,2237,2273,2281,2147,2240,2246,2268,2145,2061,2127,2129,2135,2187,2161,2022,2103,2125,2133,2190,2192,2099,2095,2075,2272,2063,1943,185,257,254,256,169,222,167,149,163,255,1249,168,150,223,164,253,252,251,250,186,189,195,239,196,197,199,182,187,188,238,260,234,237,190,205,249,157,151,154,165,166,224,231,161,162,152,155,156,181,221,201,228,241])).
% 59.83/59.96 cnf(2343,plain,
% 59.83/59.96 (P5(a19,a1,a19,a1)),
% 59.83/59.96 inference(scs_inference,[],[2318,2303,151,166])).
% 59.83/59.96 cnf(2345,plain,
% 59.83/59.96 (P5(f21(a2,x23451),x23451,f21(a2,x23451),a2)),
% 59.83/59.96 inference(scs_inference,[],[2318,2303,151,166,154])).
% 59.83/59.96 cnf(2347,plain,
% 59.83/59.96 (P5(a1,a19,a19,a1)),
% 59.83/59.96 inference(scs_inference,[],[2318,2303,151,166,154,165])).
% 59.83/59.96 cnf(2351,plain,
% 59.83/59.96 (P9(a19,a1,a19,a1,a1,a19,a19,a1)),
% 59.83/59.96 inference(scs_inference,[],[2202,2318,2248,2303,151,166,154,165,224,254])).
% 59.83/59.96 cnf(2353,plain,
% 59.83/59.96 (P3(x23531,x23531,a2,a2)),
% 59.83/59.96 inference(scs_inference,[],[2305,2202,2318,2248,2303,151,166,154,165,224,254,161])).
% 59.83/59.96 cnf(2355,plain,
% 59.83/59.96 (P9(a1,a19,a19,a1,a1,a19,a19,a1)),
% 59.83/59.96 inference(scs_inference,[],[2305,2202,2318,2248,2303,151,166,154,165,224,254,161,256])).
% 59.83/59.96 cnf(2357,plain,
% 59.83/59.96 (P9(a2,a2,f21(a2,x23571),a2,a2,a2,a2,x23571)),
% 59.83/59.96 inference(scs_inference,[],[2305,2202,2318,2248,2303,2311,151,166,154,165,224,254,161,256,257])).
% 59.83/59.96 cnf(2361,plain,
% 59.83/59.96 (P6(x23611,x23611,x23612,x23611)),
% 59.83/59.96 inference(scs_inference,[],[2216,2305,2202,2318,2248,2303,2105,2311,151,166,154,165,224,254,161,256,257,167,169])).
% 59.83/59.96 cnf(2363,plain,
% 59.83/59.96 (P4(a16,a19,a16,a1,a19,a19,a19,a1)),
% 59.83/59.96 inference(scs_inference,[],[2216,2065,2305,2202,2318,2248,2303,2105,2311,151,166,154,165,224,254,161,256,257,167,169,222])).
% 59.83/59.96 cnf(2367,plain,
% 59.83/59.96 (P4(a17,a2,x23671,x23672,a1,a19,x23671,x23672)),
% 59.83/59.96 inference(scs_inference,[],[2216,2167,2065,2305,2202,2318,2097,2248,2303,2105,2311,151,166,154,165,224,254,161,256,257,167,169,222,149,223])).
% 59.83/59.96 cnf(2369,plain,
% 59.83/59.96 (P6(a15,a1,a15,a2)),
% 59.83/59.96 inference(scs_inference,[],[2216,2167,2065,2305,2202,2264,2318,2097,2248,2303,2105,2311,151,166,154,165,224,254,161,256,257,167,169,222,149,223,168])).
% 59.83/59.96 cnf(2375,plain,
% 59.83/59.96 (P9(a19,a1,a1,a19,a19,a1,a19,a1)),
% 59.83/59.96 inference(scs_inference,[],[2216,2167,2065,2305,2202,2264,2318,2097,2101,2248,2303,2105,2311,151,166,154,165,224,254,161,256,257,167,169,222,149,223,168,163,1249,255])).
% 59.83/59.96 cnf(2379,plain,
% 59.83/59.96 (P3(f21(a2,x23791),a2,a2,x23791)),
% 59.83/59.96 inference(scs_inference,[],[2216,2167,2065,2305,2202,2264,2318,2097,2101,2248,2303,2307,2105,2311,151,166,154,165,224,254,161,256,257,167,169,222,149,223,168,163,1249,255,150,162])).
% 59.83/59.96 cnf(2383,plain,
% 59.83/59.96 (P4(x23831,x23832,x23831,x23832,x23833,x23834,x23834,x23833)),
% 59.83/59.96 inference(scs_inference,[],[2216,2230,2167,2065,2305,2202,2264,2318,2097,2101,2248,2303,2307,2105,2311,151,166,154,165,224,254,161,256,257,167,169,222,149,223,168,163,1249,255,150,162,164,253])).
% 59.83/59.96 cnf(2387,plain,
% 59.83/59.96 (P4(x23871,x23872,x23873,x23874,x23872,x23871,x23874,x23873)),
% 59.83/59.96 inference(scs_inference,[],[2216,2230,2167,2065,2305,2202,2206,2264,2318,2097,2101,2248,2303,2307,2105,2311,151,166,154,165,224,254,161,256,257,167,169,222,149,223,168,163,1249,255,150,162,164,253,250,252])).
% 59.83/59.96 cnf(2389,plain,
% 59.83/59.96 (P4(x23891,x23892,a1,a19,x23891,x23892,a17,a2)),
% 59.83/59.96 inference(scs_inference,[],[2216,2230,2167,2065,2222,2305,2202,2206,2264,2318,2097,2101,2248,2303,2307,2105,2311,151,166,154,165,224,254,161,256,257,167,169,222,149,223,168,163,1249,255,150,162,164,253,250,252,251])).
% 59.83/59.96 cnf(2392,plain,
% 59.83/59.96 (P1(x23921,x23921,x23922)),
% 59.83/59.96 inference(rename_variables,[],[2220])).
% 59.83/59.96 cnf(2394,plain,
% 59.83/59.96 (P10(x23941,x23942,x23942,x23941)),
% 59.83/59.96 inference(scs_inference,[],[2216,2226,2230,2220,2167,2065,2222,2305,2202,2206,2264,2318,2097,2101,2248,2303,2252,2307,2105,2311,2190,151,166,154,165,224,254,161,256,257,167,169,222,149,223,168,163,1249,255,150,162,164,253,250,252,251,170,239])).
% 59.83/59.96 cnf(2395,plain,
% 59.83/59.96 (P4(x23951,x23952,x23952,x23951,x23953,x23954,x23953,x23954)),
% 59.83/59.96 inference(rename_variables,[],[2226])).
% 59.83/59.96 cnf(2399,plain,
% 59.83/59.96 (P3(f27(a19,a1,a1,a1,a19),a1,a19,a1)),
% 59.83/59.96 inference(scs_inference,[],[2216,2226,2230,2220,2167,2065,2222,2305,2202,2206,2264,2318,2097,2101,2248,2303,2252,2307,2105,2311,438,2190,151,166,154,165,224,254,161,256,257,167,169,222,149,223,168,163,1249,255,150,162,164,253,250,252,251,170,239,227,199])).
% 59.83/59.96 cnf(2401,plain,
% 59.83/59.96 (P5(f12(a2,a2,a2,a2,a2),a2,f12(a2,a2,a2,a2,a2),a2)),
% 59.83/59.96 inference(scs_inference,[],[2216,2226,2230,2220,2167,2065,2222,2305,2202,2206,2264,2267,2318,2097,2101,2248,2303,2252,2307,2245,2105,2311,438,2190,151,166,154,165,224,254,161,256,257,167,169,222,149,223,168,163,1249,255,150,162,164,253,250,252,251,170,239,227,199,171])).
% 59.83/59.96 cnf(2404,plain,
% 59.83/59.96 (P10(f12(a2,a2,a2,a2,x24041),a2,a2,x24041)),
% 59.83/59.96 inference(scs_inference,[],[2216,2226,2230,2220,2392,2167,2065,2222,2305,2202,2206,2264,2267,2318,2097,2101,2248,2303,2252,2307,2245,2105,2311,438,2190,151,166,154,165,224,254,161,256,257,167,169,222,149,223,168,163,1249,255,150,162,164,253,250,252,251,170,239,227,199,171,196])).
% 59.83/59.96 cnf(2405,plain,
% 59.83/59.96 (P1(x24051,x24051,x24052)),
% 59.83/59.96 inference(rename_variables,[],[2220])).
% 59.83/59.96 cnf(2408,plain,
% 59.83/59.96 (P5(x24081,x24081,x24081,x24081)),
% 59.83/59.96 inference(rename_variables,[],[2278])).
% 59.83/59.96 cnf(2411,plain,
% 59.83/59.96 (P1(x24111,x24111,x24112)),
% 59.83/59.96 inference(rename_variables,[],[2220])).
% 59.83/59.96 cnf(2414,plain,
% 59.83/59.96 (P5(f21(a2,x24141),a2,f21(a2,x24141),x24141)),
% 59.83/59.96 inference(rename_variables,[],[2289])).
% 59.83/59.96 cnf(2416,plain,
% 59.83/59.96 (P9(f21(a2,x24161),a2,a2,x24161,a2,a2,a2,a2)),
% 59.83/59.96 inference(scs_inference,[],[2278,2216,2226,2230,2220,2392,2405,2167,2065,2222,2305,2202,2206,2264,2267,2318,2097,2101,2248,2289,2283,2303,2252,2307,2245,2105,2311,438,2190,151,166,154,165,224,254,161,256,257,167,169,222,149,223,168,163,1249,255,150,162,164,253,250,252,251,170,239,227,199,171,196,198,195,179,221])).
% 59.83/59.96 cnf(2420,plain,
% 59.83/59.96 (P2(x24201,x24201,x24201,x24201)),
% 59.83/59.96 inference(scs_inference,[],[2278,2408,2216,2226,2230,2220,2392,2405,2167,2065,2222,2305,2202,2206,2264,2267,2318,2097,2101,2248,2289,2283,2303,2252,2307,2245,2105,2311,438,2190,151,166,154,165,224,254,161,256,257,167,169,222,149,223,168,163,1249,255,150,162,164,253,250,252,251,170,239,227,199,171,196,198,195,179,221,197,182])).
% 59.83/59.96 cnf(2428,plain,
% 59.83/59.96 (P6(x24281,x24282,x24283,x24283)),
% 59.83/59.96 inference(scs_inference,[],[2278,2408,2216,2226,2230,2220,2392,2405,2411,2167,2065,2222,2305,2202,2206,2261,2264,2267,2318,2097,2101,2248,2289,2283,2303,2252,2307,2245,2105,2311,438,2077,2020,2190,151,166,154,165,224,254,161,256,257,167,169,222,149,223,168,163,1249,255,150,162,164,253,250,252,251,170,239,227,199,171,196,198,195,179,221,197,182,238,260,234])).
% 59.83/59.96 cnf(2432,plain,
% 59.83/59.96 (P4(x24321,x24322,x24322,x24321,x24323,x24324,x24323,x24324)),
% 59.83/59.96 inference(rename_variables,[],[2226])).
% 59.83/59.96 cnf(2434,plain,
% 59.83/59.96 (P4(a2,a2,a2,a2,f8(a2,a2,a2),a2,f8(a2,a2,a2),f21(a2,a2))),
% 59.83/59.96 inference(scs_inference,[],[2278,2408,2216,2226,2395,2230,2220,2392,2405,2411,2167,2065,2222,2305,2202,2206,2261,2264,2267,2318,2097,2101,2248,2289,2283,2303,2252,2307,2245,2105,2311,2236,438,2077,2020,2190,151,166,154,165,224,254,161,256,257,167,169,222,149,223,168,163,1249,255,150,162,164,253,250,252,251,170,239,227,199,171,196,198,195,179,221,197,182,238,260,234,240,225])).
% 59.83/59.96 cnf(2439,plain,
% 59.83/59.96 (P5(x24391,x24391,x24391,x24391)),
% 59.83/59.96 inference(rename_variables,[],[2278])).
% 59.83/59.96 cnf(2443,plain,
% 59.83/59.96 (P1(x24431,x24431,x24432)),
% 59.83/59.96 inference(rename_variables,[],[2220])).
% 59.83/59.96 cnf(2445,plain,
% 59.83/59.96 (P8(f6(a2,a2,a2),a2,a2)),
% 59.83/59.96 inference(scs_inference,[],[2278,2408,2216,2226,2395,2230,2220,2392,2405,2411,2167,2065,2222,2305,2202,2206,2261,2264,2267,2318,2097,2101,2248,2289,2414,2283,2303,2252,2307,2245,2105,2311,2236,438,2155,2077,2020,2190,151,166,154,165,224,254,161,256,257,167,169,222,149,223,168,163,1249,255,150,162,164,253,250,252,251,170,239,227,199,171,196,198,195,179,221,197,182,238,260,234,240,225,193,237,184])).
% 59.83/59.96 cnf(2451,plain,
% 59.83/59.96 (P1(x24511,x24511,x24512)),
% 59.83/59.96 inference(rename_variables,[],[2220])).
% 59.83/59.96 cnf(2453,plain,
% 59.83/59.96 (P10(a2,a17,a1,a19)),
% 59.83/59.96 inference(scs_inference,[],[142,2278,2408,2216,2226,2395,2230,2220,2392,2405,2411,2443,2167,2065,2222,2305,2202,2206,2261,2264,2267,2318,2097,2101,2248,2289,2414,2283,2303,2252,2307,2245,2258,2105,2311,2236,438,2155,2077,2020,2190,151,166,154,165,224,254,161,256,257,167,169,222,149,223,168,163,1249,255,150,162,164,253,250,252,251,170,239,227,199,171,196,198,195,179,221,197,182,238,260,234,240,225,193,237,184,173,204,282])).
% 59.83/59.96 cnf(2455,plain,
% 59.83/59.96 (P3(f21(a2,a17),a2,a19,a1)),
% 59.83/59.96 inference(scs_inference,[],[142,2278,2408,2216,2226,2395,2230,2220,2392,2405,2411,2443,2167,2065,2222,2305,2202,2206,2261,2264,2267,2318,2097,2101,2248,2289,2414,2283,2303,2252,2307,2245,2258,2105,2311,2236,438,2155,2077,2020,2190,151,166,154,165,224,254,161,256,257,167,169,222,149,223,168,163,1249,255,150,162,164,253,250,252,251,170,239,227,199,171,196,198,195,179,221,197,182,238,260,234,240,225,193,237,184,173,204,282,280])).
% 59.83/59.96 cnf(2461,plain,
% 59.83/59.96 (P1(f23(a1,a1,a19,a1),a19,a1)),
% 59.83/59.96 inference(scs_inference,[],[142,2278,2408,2439,2216,2226,2395,2432,2230,2220,2392,2405,2411,2443,2167,2065,2222,2305,2202,2206,2261,2264,2267,2318,2097,2101,2248,2289,2414,2283,2303,2252,2307,2245,2258,2105,2311,2236,438,2155,2077,2020,2190,151,166,154,165,224,254,161,256,257,167,169,222,149,223,168,163,1249,255,150,162,164,253,250,252,251,170,239,227,199,171,196,198,195,179,221,197,182,238,260,234,240,225,193,237,184,173,204,282,280,152,218,247])).
% 59.83/59.96 cnf(2462,plain,
% 59.83/59.96 (P4(x24621,x24622,x24622,x24621,x24623,x24624,x24623,x24624)),
% 59.83/59.96 inference(rename_variables,[],[2226])).
% 59.83/59.96 cnf(2466,plain,
% 59.83/59.96 (P8(a2,a2,f3(a2,a2,a2))),
% 59.83/59.96 inference(scs_inference,[],[142,2278,2408,2439,2216,2226,2395,2432,2230,2220,2392,2405,2411,2443,2451,2167,2065,2222,2305,2202,2206,2261,2264,2267,2318,2097,2101,2248,2289,2414,2283,2303,2252,2307,2245,2297,2258,2105,2311,2236,438,2155,2135,2077,2020,2190,151,166,154,165,224,254,161,256,257,167,169,222,149,223,168,163,1249,255,150,162,164,253,250,252,251,170,239,227,199,171,196,198,195,179,221,197,182,238,260,234,240,225,193,237,184,173,204,282,280,152,218,247,189,160])).
% 59.83/59.96 cnf(2469,plain,
% 59.83/59.96 (P5(f21(a2,a2),f21(a2,a2),a2,a2)),
% 59.83/59.96 inference(scs_inference,[],[142,2278,2408,2439,2216,2226,2395,2432,2462,2230,2220,2392,2405,2411,2443,2451,2167,2065,2222,2305,2202,2206,2261,2264,2267,2318,2097,2101,2248,2289,2414,2283,2303,2252,2307,2245,2297,2258,2105,2311,2236,438,2155,2135,2077,2020,2190,151,166,154,165,224,254,161,256,257,167,169,222,149,223,168,163,1249,255,150,162,164,253,250,252,251,170,239,227,199,171,196,198,195,179,221,197,182,238,260,234,240,225,193,237,184,173,204,282,280,152,218,247,189,160,249])).
% 59.83/59.96 cnf(2478,plain,
% 59.83/59.96 (P10(a1,a19,a17,a2)),
% 59.83/59.96 inference(scs_inference,[],[2394,1169])).
% 59.83/59.96 cnf(2479,plain,
% 59.83/59.96 (P10(x24791,x24792,x24792,x24791)),
% 59.83/59.96 inference(rename_variables,[],[2394])).
% 59.83/59.96 cnf(2485,plain,
% 59.83/59.96 (P10(f7(x24851,x24851,x24851,x24851),x24851,x24851,x24851)),
% 59.83/59.96 inference(scs_inference,[],[2420,2394,2445,2469,1169,154,165,185])).
% 59.83/59.96 cnf(2487,plain,
% 59.83/59.96 (P5(a1,a19,a1,a19)),
% 59.83/59.96 inference(scs_inference,[],[2420,2394,2347,2445,2469,1169,154,165,185,166])).
% 59.83/59.96 cnf(2489,plain,
% 59.83/59.96 (P4(a19,a1,a1,a1,a1,a1,a19,a1)),
% 59.83/59.96 inference(scs_inference,[],[2420,2394,2347,2343,2445,2469,1169,154,165,185,166,224])).
% 59.83/59.96 cnf(2491,plain,
% 59.83/59.96 (P3(a2,x24911,f21(a2,x24911),a2)),
% 59.83/59.96 inference(scs_inference,[],[2420,2394,2347,2343,2445,2469,2379,1169,154,165,185,166,224,161])).
% 59.83/59.96 cnf(2493,plain,
% 59.83/59.96 (P9(a1,a19,a1,a19,a19,a1,a19,a1)),
% 59.83/59.96 inference(scs_inference,[],[2420,2394,2347,2343,2375,2445,2469,2379,1169,154,165,185,166,224,161,256])).
% 59.83/59.96 cnf(2495,plain,
% 59.83/59.96 (P9(a19,a1,a19,a1,a19,a1,a1,a19)),
% 59.83/59.96 inference(scs_inference,[],[2420,2394,2347,2343,2375,2445,2469,2379,1169,154,165,185,166,224,161,256,254])).
% 59.83/59.96 cnf(2503,plain,
% 59.83/59.96 (P4(x25031,x25031,x25032,x25033,a2,a2,x25032,x25033)),
% 59.83/59.96 inference(scs_inference,[],[2420,2394,2347,2353,2343,2369,2375,2445,2469,2379,2416,1169,154,165,185,166,224,161,256,254,257,167,169,223])).
% 59.83/59.96 cnf(2511,plain,
% 59.83/59.96 (P6(x25111,x25112,x25113,x25112)),
% 59.83/59.96 inference(scs_inference,[],[2420,2394,2428,2347,2137,2353,2343,2369,2375,2111,2445,2469,2379,2416,1169,154,165,185,166,224,161,256,254,257,167,169,223,222,150,149,168])).
% 59.83/59.96 cnf(2517,plain,
% 59.83/59.96 (P6(x25171,x25172,x25171,x25173)),
% 59.83/59.96 inference(scs_inference,[],[2420,2394,2428,2347,2137,2353,2343,2369,2375,2453,2111,2445,2469,2379,2416,2399,1169,154,165,185,166,224,161,256,254,257,167,169,223,222,150,149,168,163,162,1249])).
% 59.83/59.96 cnf(2519,plain,
% 59.83/59.96 (P9(a19,a1,a1,a19,a19,a1,a1,a19)),
% 59.83/59.96 inference(scs_inference,[],[2420,2394,2428,2347,2137,2353,2343,2355,2369,2375,2453,2111,2445,2469,2379,2416,2399,1169,154,165,185,166,224,161,256,254,257,167,169,223,222,150,149,168,163,162,1249,255])).
% 59.83/59.96 cnf(2521,plain,
% 59.83/59.96 (P10(x25211,x25212,x25211,x25212)),
% 59.83/59.96 inference(scs_inference,[],[2420,2394,2479,2428,2347,2137,2353,2343,2355,2369,2375,2453,2111,2445,2469,2379,2416,2399,1169,154,165,185,166,224,161,256,254,257,167,169,223,222,150,149,168,163,162,1249,255,164])).
% 59.83/59.96 cnf(2523,plain,
% 59.83/59.96 (P4(x25231,x25232,x25232,x25231,x25233,x25234,x25234,x25233)),
% 59.83/59.96 inference(scs_inference,[],[2420,2387,2394,2479,2428,2347,2137,2353,2343,2355,2369,2375,2453,2111,2445,2469,2379,2416,2399,1169,154,165,185,166,224,161,256,254,257,167,169,223,222,150,149,168,163,162,1249,255,164,253])).
% 59.83/59.96 cnf(2525,plain,
% 59.83/59.96 (P8(a2,f3(a2,a2,a2),a2)),
% 59.83/59.96 inference(scs_inference,[],[2420,2387,2394,2479,2428,2347,2137,2353,2343,2355,2369,2375,2453,2111,2445,2469,2379,2466,2416,2399,1169,154,165,185,166,224,161,256,254,257,167,169,223,222,150,149,168,163,162,1249,255,164,253,152])).
% 59.83/59.96 cnf(2531,plain,
% 59.83/59.96 (P4(x25311,x25312,a17,a2,x25311,x25312,a1,a19)),
% 59.83/59.96 inference(scs_inference,[],[2420,2387,2394,2479,2428,2347,2059,2363,2137,2353,2367,2343,2355,2369,2375,2453,2111,2445,2469,2379,2466,2416,2399,1169,154,165,185,166,224,161,256,254,257,167,169,223,222,150,149,168,163,162,1249,255,164,253,152,250,252,251])).
% 59.83/59.96 cnf(2534,plain,
% 59.83/59.96 (P10(x25341,x25342,x25342,x25341)),
% 59.83/59.96 inference(rename_variables,[],[2394])).
% 59.83/59.96 cnf(2539,plain,
% 59.83/59.96 (P10(x25391,x25392,x25392,x25391)),
% 59.83/59.96 inference(rename_variables,[],[2394])).
% 59.83/59.96 cnf(2545,plain,
% 59.83/59.96 (P10(x25451,x25452,x25452,x25451)),
% 59.83/59.96 inference(rename_variables,[],[2394])).
% 59.83/59.96 cnf(2548,plain,
% 59.83/59.96 (P10(x25481,x25482,x25482,x25481)),
% 59.83/59.96 inference(rename_variables,[],[2394])).
% 59.83/59.96 cnf(2551,plain,
% 59.83/59.96 (P10(x25511,x25512,x25512,x25511)),
% 59.83/59.96 inference(rename_variables,[],[2394])).
% 59.83/59.96 cnf(2553,plain,
% 59.83/59.96 (P2(f8(x25531,x25531,x25532),x25531,x25531,x25532)),
% 59.83/59.96 inference(scs_inference,[],[142,2420,2361,2387,2394,2479,2534,2539,2545,2548,2551,2428,2347,2059,2363,2137,2353,2367,2343,2355,2369,2375,2453,2271,2111,2445,2239,2401,2469,2379,2466,2416,2399,1169,154,165,185,166,224,161,256,254,257,167,169,223,222,150,149,168,163,162,1249,255,164,253,152,250,252,251,174,176,186,159,199,227,196,189])).
% 59.83/59.96 cnf(2554,plain,
% 59.83/59.96 (P10(x25541,x25542,x25542,x25541)),
% 59.83/59.96 inference(rename_variables,[],[2394])).
% 59.83/59.96 cnf(2560,plain,
% 59.83/59.96 (P10(x25601,x25602,x25602,x25601)),
% 59.83/59.96 inference(rename_variables,[],[2394])).
% 59.83/59.96 cnf(2565,plain,
% 59.83/59.96 (P10(x25651,x25652,x25652,x25651)),
% 59.83/59.96 inference(rename_variables,[],[2394])).
% 59.83/59.96 cnf(2567,plain,
% 59.83/59.96 (P10(a19,a19,a1,a1)),
% 59.83/59.96 inference(scs_inference,[],[142,2420,2361,2387,2394,2479,2534,2539,2545,2548,2551,2554,2560,2428,2347,2059,2363,2137,2353,2367,2343,2355,2369,2375,2453,2271,2196,2111,2445,2239,2401,2469,2379,2466,2416,2399,2267,1169,154,165,185,166,224,161,256,254,257,167,169,223,222,150,149,168,163,162,1249,255,164,253,152,250,252,251,174,176,186,159,199,227,196,189,175,187,171,197,179])).
% 59.83/59.96 cnf(2571,plain,
% 59.83/59.96 (P10(x25711,x25712,x25712,x25711)),
% 59.83/59.96 inference(rename_variables,[],[2394])).
% 59.83/59.96 cnf(2574,plain,
% 59.83/59.96 (P10(x25741,x25742,x25742,x25741)),
% 59.83/59.96 inference(rename_variables,[],[2394])).
% 59.83/59.96 cnf(2577,plain,
% 59.83/59.96 (P4(x25771,x25772,x25773,x25774,x25772,x25771,x25774,x25773)),
% 59.83/59.96 inference(rename_variables,[],[2387])).
% 59.83/59.96 cnf(2579,plain,
% 59.83/59.96 (P2(a19,a1,a1,a1)),
% 59.83/59.96 inference(scs_inference,[],[142,2420,2361,2387,2394,2479,2534,2539,2545,2548,2551,2554,2560,2565,2571,2428,2347,2059,2363,2137,2353,2367,2343,2355,2369,2375,2453,2271,2196,2111,2445,2239,2401,2469,2379,2466,2416,2399,2267,1169,154,165,185,166,224,161,256,254,257,167,169,223,222,150,149,168,163,162,1249,255,164,253,152,250,252,251,174,176,186,159,199,227,196,189,175,187,171,197,179,188,195,239,182])).
% 59.83/59.96 cnf(2581,plain,
% 59.83/59.96 (P5(x25811,a1,x25811,f27(a19,x25811,a1,a1,a19))),
% 59.83/59.96 inference(scs_inference,[],[142,2420,2361,2387,2394,2479,2534,2539,2545,2548,2551,2554,2560,2565,2571,2574,2428,2347,2059,2363,2137,2353,2367,2343,2355,2369,2375,2453,2271,2196,2111,2445,2239,2401,2469,2379,2466,2416,2399,2267,1169,154,165,185,166,224,161,256,254,257,167,169,223,222,150,149,168,163,162,1249,255,164,253,152,250,252,251,174,176,186,159,199,227,196,189,175,187,171,197,179,188,195,239,182,198])).
% 59.83/59.96 cnf(2582,plain,
% 59.83/59.96 (P10(x25821,x25822,x25822,x25821)),
% 59.83/59.96 inference(rename_variables,[],[2394])).
% 59.83/59.96 cnf(2586,plain,
% 59.83/59.96 (P4(x25861,x25862,x25863,x25864,x25862,x25861,x25864,x25863)),
% 59.83/59.96 inference(rename_variables,[],[2387])).
% 59.83/59.96 cnf(2588,plain,
% 59.83/59.96 (P9(f6(a2,a2,a2),a2,a2,a2,f6(a2,a2,a2),a2,a2,a2)),
% 59.83/59.96 inference(scs_inference,[],[142,2420,2361,2387,2577,2394,2479,2534,2539,2545,2548,2551,2554,2560,2565,2571,2574,2428,2347,2059,2363,2137,2353,2367,2343,2355,2369,2375,2453,2271,2196,2111,2445,2239,2401,2469,2379,2466,2416,2399,2267,1169,154,165,185,166,224,161,256,254,257,167,169,223,222,150,149,168,163,162,1249,255,164,253,152,250,252,251,174,176,186,159,199,227,196,189,175,187,171,197,179,188,195,239,182,198,238,221])).
% 59.83/59.96 cnf(2594,plain,
% 59.83/59.96 (P4(x25941,x25942,x25941,x25942,x25943,x25944,x25943,x25944)),
% 59.83/59.96 inference(rename_variables,[],[2155])).
% 59.83/59.96 cnf(2598,plain,
% 59.83/59.96 (P10(a1,a19,a19,a19)),
% 59.83/59.96 inference(scs_inference,[],[142,2420,2361,2387,2577,2586,2394,2479,2534,2539,2545,2548,2551,2554,2560,2565,2571,2574,2428,2347,2059,2363,2137,2353,2367,2081,2343,2355,2369,2375,2453,2271,2196,2111,2445,2239,2401,2469,2379,2466,2416,2399,2278,2261,2155,2267,1169,154,165,185,166,224,161,256,254,257,167,169,223,222,150,149,168,163,162,1249,255,164,253,152,250,252,251,174,176,186,159,199,227,196,189,175,187,171,197,179,188,195,239,182,198,238,221,260,234,225,193])).
% 59.83/59.96 cnf(2599,plain,
% 59.83/59.96 (P6(x25991,x25991,x25992,x25991)),
% 59.83/59.96 inference(rename_variables,[],[2361])).
% 59.83/59.96 cnf(2602,plain,
% 59.83/59.96 (P8(x26021,x26021,x26021)),
% 59.83/59.96 inference(scs_inference,[],[142,2420,2361,2383,2387,2577,2586,2394,2479,2534,2539,2545,2548,2551,2554,2560,2565,2571,2574,2428,2347,2059,2363,2137,2353,2367,2081,2343,2355,2369,2375,2453,2271,2196,2111,2445,2239,2401,2469,2379,2466,2416,2399,2278,2220,2261,2155,2267,1169,154,165,185,166,224,161,256,254,257,167,169,223,222,150,149,168,163,162,1249,255,164,253,152,250,252,251,174,176,186,159,199,227,196,189,175,187,171,197,179,188,195,239,182,198,238,221,260,234,225,193,237])).
% 59.83/59.96 cnf(2604,plain,
% 59.83/59.96 (P1(x26041,x26041,x26042)),
% 59.83/59.96 inference(rename_variables,[],[2220])).
% 59.83/59.96 cnf(2606,plain,
% 59.83/59.96 (P8(f6(x26061,x26061,x26061),x26061,x26061)),
% 59.83/59.96 inference(scs_inference,[],[142,2420,2361,2383,2387,2577,2586,2394,2479,2534,2539,2545,2548,2551,2554,2560,2565,2571,2574,2582,2428,2347,2059,2363,2137,2353,2367,2081,2343,2355,2369,2375,2453,2271,2196,2111,2445,2239,2401,2469,2379,2466,2416,2399,2278,2220,2261,2155,2267,1169,154,165,185,166,224,161,256,254,257,167,169,223,222,150,149,168,163,162,1249,255,164,253,152,250,252,251,174,176,186,159,199,227,196,189,175,187,171,197,179,188,195,239,182,198,238,221,260,234,225,193,237,184])).
% 59.83/59.96 cnf(2616,plain,
% 59.83/59.96 (P1(x26161,x26161,x26162)),
% 59.83/59.96 inference(rename_variables,[],[2220])).
% 59.83/59.96 cnf(2620,plain,
% 59.83/59.96 (P3(x26201,x26201,a2,a2)),
% 59.83/59.96 inference(rename_variables,[],[2353])).
% 59.83/59.96 cnf(2623,plain,
% 59.83/59.96 (P8(f21(a15,x26231),a15,x26231)),
% 59.83/59.96 inference(scs_inference,[],[142,2420,2361,2599,2383,2387,2577,2586,2394,2479,2534,2539,2545,2548,2551,2554,2560,2565,2571,2574,2582,2428,2347,2059,2363,2137,2353,2367,2081,2343,2355,2369,2375,2453,2271,2196,2111,2445,2239,2401,2469,2379,2434,2466,2416,2399,2278,2220,2604,2616,1996,2261,2155,2216,2303,2063,2267,2020,1169,154,165,185,166,224,161,256,254,257,167,169,223,222,150,149,168,163,162,1249,255,164,253,152,250,252,251,174,176,186,159,199,227,196,189,175,187,171,197,179,188,195,239,182,198,238,221,260,234,225,193,237,184,249,205,204,157])).
% 59.83/59.96 cnf(2640,plain,
% 59.83/59.96 (P8(f21(a15,a2),a2,a15)),
% 59.83/59.96 inference(scs_inference,[],[142,2420,2361,2599,2383,2387,2577,2586,2394,2479,2534,2539,2545,2548,2551,2554,2560,2565,2571,2574,2582,2428,2347,2059,2363,2137,2353,2620,2367,2081,2343,2355,2369,2375,2453,2271,2196,2111,2445,2239,2401,2469,2379,2434,2466,2416,2399,523,2278,2226,2220,2604,2616,1996,2261,2155,2594,2216,2303,2063,2075,2267,2020,1169,154,165,185,166,224,161,256,254,257,167,169,223,222,150,149,168,163,162,1249,255,164,253,152,250,252,251,174,176,186,159,199,227,196,189,175,187,171,197,179,188,195,239,182,198,238,221,260,234,225,193,237,184,249,205,204,157,151,231,219,192,245,248,173])).
% 59.83/59.96 cnf(2647,plain,
% 59.83/59.96 (P10(a19,a1,a17,a2)),
% 59.83/59.96 inference(scs_inference,[],[2521,1169])).
% 59.83/59.96 cnf(2648,plain,
% 59.83/59.96 (P10(x26481,x26482,x26481,x26482)),
% 59.83/59.96 inference(rename_variables,[],[2521])).
% 59.83/59.96 cnf(2651,plain,
% 59.83/59.96 (P10(x26511,x26512,x26511,x26512)),
% 59.83/59.96 inference(rename_variables,[],[2521])).
% 59.83/59.96 cnf(2655,plain,
% 59.83/59.96 (P10(f7(a1,a1,a1,a19),a1,a1,a19)),
% 59.83/59.96 inference(scs_inference,[],[2521,2648,2579,2581,1169,282,165,185])).
% 59.83/59.96 cnf(2659,plain,
% 59.83/59.96 (P5(f6(x26591,x26591,x26591),x26591,f6(x26591,x26591,x26591),x26591)),
% 59.83/59.96 inference(scs_inference,[],[2521,2648,2579,2606,2581,2640,1169,282,165,185,151,154])).
% 59.83/59.96 cnf(2665,plain,
% 59.83/59.96 (P9(a1,a19,a19,a1,a19,a1,a1,a19)),
% 59.83/59.96 inference(scs_inference,[],[2521,2648,2495,2579,2606,2455,2345,2581,2640,1169,282,165,185,151,154,161,166,256])).
% 59.83/59.96 cnf(2667,plain,
% 59.83/59.96 (P4(a1,a19,a19,a19,a19,a19,a1,a19)),
% 59.83/59.96 inference(scs_inference,[],[2521,2648,2495,2487,2579,2606,2455,2345,2581,2640,1169,282,165,185,151,154,161,166,256,224])).
% 59.83/59.96 cnf(2669,plain,
% 59.83/59.96 (P9(a19,a1,a19,a1,a1,a19,a1,a19)),
% 59.83/59.96 inference(scs_inference,[],[2521,2648,2493,2495,2487,2579,2606,2455,2345,2581,2640,1169,282,165,185,151,154,161,166,256,224,254])).
% 59.83/59.96 cnf(2673,plain,
% 59.83/59.96 (P4(x26731,x26732,x26731,x26733,x26733,x26732,x26733,x26733)),
% 59.83/59.96 inference(scs_inference,[],[2521,2648,2511,2493,2495,2487,2579,2606,2455,2345,2581,2588,2640,1169,282,165,185,151,154,161,166,256,224,254,257,222])).
% 59.83/59.96 cnf(2675,plain,
% 59.83/59.96 (P6(x26751,x26752,x26753,x26751)),
% 59.83/59.96 inference(scs_inference,[],[2521,2648,2511,2493,2495,2487,2579,2606,2455,2345,2581,2588,2640,1169,282,165,185,151,154,161,166,256,224,254,257,222,167])).
% 59.83/59.96 cnf(2677,plain,
% 59.83/59.96 (P6(x26771,x26772,x26772,x26773)),
% 59.83/59.96 inference(scs_inference,[],[2521,2648,2511,2493,2495,2487,2579,2606,2455,2345,2581,2588,2640,1169,282,165,185,151,154,161,166,256,224,254,257,222,167,169])).
% 59.83/59.96 cnf(2683,plain,
% 59.83/59.96 (P9(a2,a2,f6(a2,a2,a2),a2,a2,a2,f6(a2,a2,a2),a2)),
% 59.83/59.96 inference(scs_inference,[],[2521,2648,2511,2493,2495,2487,2579,2606,2250,2455,2345,2581,2588,2640,1169,282,165,185,151,154,161,166,256,224,254,257,222,167,169,223,162,255])).
% 59.83/59.96 cnf(2687,plain,
% 59.83/59.96 (P6(x26871,x26871,x26872,x26873)),
% 59.83/59.96 inference(scs_inference,[],[2521,2648,2511,2493,2495,2487,2579,2606,2250,2461,2455,2345,2581,2588,2640,1169,282,165,185,151,154,161,166,256,224,254,257,222,167,169,223,162,255,150,1249])).
% 59.83/59.96 cnf(2695,plain,
% 59.83/59.96 (P4(x26951,x26951,a2,a2,x26952,x26953,x26952,x26953)),
% 59.83/59.96 inference(scs_inference,[],[2521,2648,2511,2493,2495,2503,2478,2487,2579,2606,2250,2461,2455,2345,2581,2404,2588,2640,1169,282,165,185,151,154,161,166,256,224,254,257,222,167,169,223,162,255,150,1249,149,163,164,253])).
% 59.83/59.96 cnf(2697,plain,
% 59.83/59.96 (P8(f21(a15,x26971),x26971,a15)),
% 59.83/59.96 inference(scs_inference,[],[2521,2648,2511,2493,2495,2503,2478,2487,2579,2606,2250,2461,2455,2345,2581,2623,2404,2588,2640,1169,282,165,185,151,154,161,166,256,224,254,257,222,167,169,223,162,255,150,1249,149,163,164,253,152])).
% 59.83/59.96 cnf(2699,plain,
% 59.83/59.96 (P4(x26991,x26992,a1,a19,x26992,x26991,a17,a2)),
% 59.83/59.96 inference(scs_inference,[],[2521,2648,2511,2493,2495,2503,2389,2478,2487,2579,2606,2250,2461,2455,2345,2581,2623,2404,2588,2640,1169,282,165,185,151,154,161,166,256,224,254,257,222,167,169,223,162,255,150,1249,149,163,164,253,152,252])).
% 59.83/59.96 cnf(2703,plain,
% 59.83/59.96 (P4(x27031,x27032,x27033,x27033,x27031,x27032,a2,a2)),
% 59.83/59.96 inference(scs_inference,[],[2521,2648,2511,2493,2495,2503,2389,2478,2487,2579,2606,2250,2461,2455,2345,2581,2623,2404,2588,2640,1169,282,165,185,151,154,161,166,256,224,254,257,222,167,169,223,162,255,150,1249,149,163,164,253,152,252,250,251])).
% 59.83/59.96 cnf(2705,plain,
% 59.83/59.96 (~E(a1,a19)),
% 59.83/59.96 inference(scs_inference,[],[2521,2648,2511,2493,2495,2503,2389,2478,2487,2579,2606,2250,2461,2455,2345,2581,2623,2404,2588,2640,589,1169,282,165,185,151,154,161,166,256,224,254,257,222,167,169,223,162,255,150,1249,149,163,164,253,152,252,250,251,123])).
% 59.83/59.96 cnf(2706,plain,
% 59.83/59.96 (P3(f25(x27061,x27061,x27061,x27061,x27061,x27061),x27061,x27061,x27061)),
% 59.83/59.96 inference(scs_inference,[],[2602,2521,2648,2511,2493,2495,2503,2389,2478,2487,2579,2606,2250,2461,2455,2345,2581,2623,2404,2588,2640,589,1169,282,165,185,151,154,161,166,256,224,254,257,222,167,169,223,162,255,150,1249,149,163,164,253,152,252,250,251,123,203])).
% 59.83/59.96 cnf(2709,plain,
% 59.83/59.96 (P10(x27091,x27092,x27092,x27091)),
% 59.83/59.96 inference(rename_variables,[],[2394])).
% 59.83/59.96 cnf(2714,plain,
% 59.83/59.96 (P1(f5(x27141,x27141,x27142),x27142,x27141)),
% 59.83/59.96 inference(scs_inference,[],[2602,2521,2648,2651,2511,2493,2495,2503,2389,2478,2487,2579,2606,2250,2461,2455,2345,2581,2623,2404,2588,2640,2394,589,2226,1169,282,165,185,151,154,161,166,256,224,254,257,222,167,169,223,162,255,150,1249,149,163,164,253,152,252,250,251,123,203,174,247,176])).
% 59.83/59.96 cnf(2716,plain,
% 59.83/59.96 (P3(a19,a19,a1,a1)),
% 59.83/59.96 inference(scs_inference,[],[2602,2521,2648,2651,2511,2493,2495,2503,2389,2478,2487,2567,2579,2606,2250,2461,2455,2345,2581,2623,2404,2588,2640,2394,589,2226,1169,282,165,185,151,154,161,166,256,224,254,257,222,167,169,223,162,255,150,1249,149,163,164,253,152,252,250,251,123,203,174,247,176,178])).
% 59.83/59.96 cnf(2717,plain,
% 59.83/59.96 (P10(x27171,x27172,x27171,x27172)),
% 59.83/59.96 inference(rename_variables,[],[2521])).
% 59.83/59.96 cnf(2722,plain,
% 59.83/59.96 (P10(x27221,x27222,x27222,x27221)),
% 59.83/59.96 inference(rename_variables,[],[2394])).
% 59.83/59.96 cnf(2724,plain,
% 59.83/59.96 (P8(f25(x27241,x27241,x27241,x27241,x27241,x27241),x27241,x27241)),
% 59.83/59.96 inference(scs_inference,[],[2602,2521,2648,2651,2717,2511,2493,2495,2503,2389,2478,2487,2567,2579,2606,2250,2461,2455,2345,2581,2623,2404,2588,2640,2394,2709,589,2226,1169,282,165,185,151,154,161,166,256,224,254,257,222,167,169,223,162,255,150,1249,149,163,164,253,152,252,250,251,123,203,174,247,176,178,175,186,201])).
% 59.83/59.96 cnf(2726,plain,
% 59.83/59.96 (P5(f3(a2,a2,a2),f3(a2,a2,a2),f3(a2,a2,a2),a2)),
% 59.83/59.96 inference(scs_inference,[],[2602,2521,2648,2651,2717,2511,2493,2495,2503,2389,2478,2487,2567,2579,2606,2250,2461,2455,2345,2581,2623,2404,2525,2588,2640,2394,2709,589,2226,1169,282,165,185,151,154,161,166,256,224,254,257,222,167,169,223,162,255,150,1249,149,163,164,253,152,252,250,251,123,203,174,247,176,178,175,186,201,171])).
% 59.83/59.96 cnf(2727,plain,
% 59.83/59.96 (P10(x27271,x27272,x27271,x27272)),
% 59.83/59.96 inference(rename_variables,[],[2521])).
% 59.83/59.96 cnf(2729,plain,
% 59.83/59.96 (P10(f12(a1,a19,a19,a19,x27291),a1,a19,x27291)),
% 59.83/59.96 inference(scs_inference,[],[2602,2521,2648,2651,2717,2511,2493,2495,2503,2389,2478,2487,2567,2579,2598,2606,2250,2461,2455,2345,2581,2623,2404,2525,2588,2640,2394,2709,589,2226,2220,1169,282,165,185,151,154,161,166,256,224,254,257,222,167,169,223,162,255,150,1249,149,163,164,253,152,252,250,251,123,203,174,247,176,178,175,186,201,171,196])).
% 59.83/59.96 cnf(2730,plain,
% 59.83/59.96 (P1(x27301,x27301,x27302)),
% 59.83/59.96 inference(rename_variables,[],[2220])).
% 59.83/59.96 cnf(2733,plain,
% 59.83/59.96 (P10(x27331,x27332,x27332,x27331)),
% 59.83/59.96 inference(rename_variables,[],[2394])).
% 59.83/59.96 cnf(2735,plain,
% 59.83/59.96 (P10(x27351,f4(x27351,x27351,x27352),x27352,x27351)),
% 59.83/59.96 inference(scs_inference,[],[2602,2521,2648,2651,2717,2727,2511,2493,2495,2503,2389,2478,2487,2567,2579,2598,2606,2250,2461,2455,2345,2581,2623,2404,2525,2588,2640,651,2394,2709,2722,589,2226,2220,1169,282,165,185,151,154,161,166,256,224,254,257,222,167,169,223,162,255,150,1249,149,163,164,253,152,252,250,251,123,203,174,247,176,178,175,186,201,171,196,227,187])).
% 59.83/59.96 cnf(2738,plain,
% 59.83/59.96 (P10(x27381,x27382,x27381,x27382)),
% 59.83/59.96 inference(rename_variables,[],[2521])).
% 59.83/59.96 cnf(2740,plain,
% 59.83/59.96 (P2(a1,a19,a19,a19)),
% 59.83/59.96 inference(scs_inference,[],[2602,2521,2648,2651,2717,2727,2511,2493,2495,2503,2389,2478,2487,2567,2579,2598,2606,2250,2461,2455,2345,2581,2623,2404,2525,2588,2640,651,2394,2709,2722,589,2226,2220,1169,282,165,185,151,154,161,166,256,224,254,257,222,167,169,223,162,255,150,1249,149,163,164,253,152,252,250,251,123,203,174,247,176,178,175,186,201,171,196,227,187,199,182])).
% 59.83/59.96 cnf(2742,plain,
% 59.83/59.96 (P10(x27421,x27421,a2,a2)),
% 59.83/59.96 inference(scs_inference,[],[2602,2521,2648,2651,2717,2727,2738,2511,2493,2495,2503,2389,2478,2487,2567,2579,2598,2606,2250,2461,2455,2345,2581,2623,2404,2525,2588,2640,651,2394,2709,2722,589,2226,2220,1169,282,165,185,151,154,161,166,256,224,254,257,222,167,169,223,162,255,150,1249,149,163,164,253,152,252,250,251,123,203,174,247,176,178,175,186,201,171,196,227,187,199,182,239])).
% 59.83/59.96 cnf(2743,plain,
% 59.83/59.96 (P4(x27431,x27431,x27432,x27433,a2,a2,x27432,x27433)),
% 59.83/59.96 inference(rename_variables,[],[2503])).
% 59.83/59.96 cnf(2744,plain,
% 59.83/59.96 (P10(x27441,x27442,x27441,x27442)),
% 59.83/59.96 inference(rename_variables,[],[2521])).
% 59.83/59.96 cnf(2747,plain,
% 59.83/59.96 (P10(x27471,x27472,x27471,x27472)),
% 59.83/59.96 inference(rename_variables,[],[2521])).
% 59.83/59.96 cnf(2749,plain,
% 59.83/59.96 (P10(x27491,f5(x27491,x27491,x27492),x27492,x27491)),
% 59.83/59.96 inference(scs_inference,[],[2602,2521,2648,2651,2717,2727,2738,2744,2747,2511,2493,2495,2503,2389,2478,2487,2567,2579,2598,2606,2250,2461,2455,2345,2581,2623,2404,2525,2588,2640,651,2394,2709,2722,589,2226,2220,1169,282,165,185,151,154,161,166,256,224,254,257,222,167,169,223,162,255,150,1249,149,163,164,253,152,252,250,251,123,203,174,247,176,178,175,186,201,171,196,227,187,199,182,239,197,188])).
% 59.83/59.96 cnf(2753,plain,
% 59.83/59.96 (P10(a1,a1,a19,a19)),
% 59.83/59.96 inference(scs_inference,[],[2602,2521,2648,2651,2717,2727,2738,2744,2747,2511,2493,2495,2503,2389,2478,2487,2567,2579,2598,2606,2250,2461,2455,2345,2581,2623,2404,2525,2588,2640,651,2394,2709,2722,2035,589,2226,2220,1169,282,165,185,151,154,161,166,256,224,254,257,222,167,169,223,162,255,150,1249,149,163,164,253,152,252,250,251,123,203,174,247,176,178,175,186,201,171,196,227,187,199,182,239,197,188,189,179])).
% 59.83/59.96 cnf(2758,plain,
% 59.83/59.96 (P3(x27581,x27581,f27(a2,a2,a2,a2,a2),a2)),
% 59.83/59.96 inference(scs_inference,[],[2602,2521,2648,2651,2717,2727,2738,2744,2747,2511,2493,2495,2503,2743,2389,2478,2487,2567,2579,2598,2606,2250,2461,2299,2455,2345,2581,2623,2404,2525,2588,2640,651,2394,2709,2722,2035,589,2226,2220,2730,1169,282,165,185,151,154,161,166,256,224,254,257,222,167,169,223,162,255,150,1249,149,163,164,253,152,252,250,251,123,203,174,247,176,178,175,186,201,171,196,227,187,199,182,239,197,188,189,179,195,238])).
% 59.83/59.96 cnf(2759,plain,
% 59.83/59.96 (P4(x27591,x27591,x27592,x27593,a2,a2,x27592,x27593)),
% 59.83/59.96 inference(rename_variables,[],[2503])).
% 59.83/59.96 cnf(2768,plain,
% 59.83/59.96 (P4(x27681,x27682,x27682,x27681,x27683,x27684,x27684,x27683)),
% 59.83/59.96 inference(rename_variables,[],[2523])).
% 59.83/59.96 cnf(2773,plain,
% 59.83/59.96 (P2(f9(x27731,x27731,x27731),x27731,x27731,x27731)),
% 59.83/59.96 inference(scs_inference,[],[2602,2521,2648,2651,2717,2727,2738,2744,2747,2523,2511,2517,2493,2495,2503,2743,2759,2389,2478,2487,2567,2579,2598,2606,2250,2461,2299,2455,2345,2581,2623,2404,2525,2588,2640,651,2394,2709,2722,2733,2035,589,2226,2220,2730,2075,1169,282,165,185,151,154,161,166,256,224,254,257,222,167,169,223,162,255,150,1249,149,163,164,253,152,252,250,251,123,203,174,247,176,178,175,186,201,171,196,227,187,199,182,239,197,188,189,179,195,238,198,221,260,225,190])).
% 59.83/59.96 cnf(2775,plain,
% 59.83/59.96 (P6(x27751,x27752,x27751,x27753)),
% 59.83/59.96 inference(rename_variables,[],[2517])).
% 59.83/59.96 cnf(2782,plain,
% 59.83/59.96 (P5(x27821,x27821,x27821,x27821)),
% 59.83/59.96 inference(rename_variables,[],[2278])).
% 59.83/59.96 cnf(2787,plain,
% 59.83/59.96 (P5(x27871,x27871,x27872,x27872)),
% 59.83/59.96 inference(scs_inference,[],[2602,2521,2648,2651,2717,2727,2738,2744,2747,2523,2768,2511,2517,2775,2493,2495,2503,2743,2759,2389,2478,2487,2567,2579,2598,2606,2250,2461,2299,2455,2345,2581,2623,2404,2525,2588,2640,651,2394,2709,2722,2733,2035,1998,589,2278,2782,2226,2220,2730,2283,2075,1169,282,165,185,151,154,161,166,256,224,254,257,222,167,169,223,162,255,150,1249,149,163,164,253,152,252,250,251,123,203,174,247,176,178,175,186,201,171,196,227,187,199,182,239,197,188,189,179,195,238,198,221,260,225,190,184,210,211,249])).
% 59.83/59.96 cnf(2793,plain,
% 59.83/59.96 (P8(f21(a1,x27931),a1,x27931)),
% 59.83/59.96 inference(scs_inference,[],[2602,2521,2648,2651,2717,2727,2738,2744,2747,2523,2768,2511,2517,2775,2493,2495,2503,2743,2759,2389,2478,2487,2567,2579,2598,2606,2250,2461,2299,2455,2345,2581,2623,2404,2525,2588,2640,651,2394,2709,2722,2733,1941,2035,1998,589,2278,2782,2226,2220,2730,2283,2075,1169,282,165,185,151,154,161,166,256,224,254,257,222,167,169,223,162,255,150,1249,149,163,164,253,152,252,250,251,123,203,174,247,176,178,175,186,201,171,196,227,187,199,182,239,197,188,189,179,195,238,198,221,260,225,190,184,210,211,249,157])).
% 59.83/59.96 cnf(2814,plain,
% 59.83/59.96 (P3(a1,a1,a19,a19)),
% 59.83/59.96 inference(scs_inference,[],[2716,2740,2735,2726,2697,165,1169,185,151,161])).
% 59.83/59.96 cnf(2816,plain,
% 59.83/59.96 (P5(f25(x28161,x28161,x28161,x28161,x28161,x28161),x28161,f25(x28161,x28161,x28161,x28161,x28161,x28161),x28161)),
% 59.83/59.96 inference(scs_inference,[],[2716,2740,2724,2735,2726,2697,165,1169,185,151,161,154])).
% 59.83/59.96 cnf(2818,plain,
% 59.83/59.96 (P5(f6(x28181,x28181,x28181),x28181,x28181,f6(x28181,x28181,x28181))),
% 59.83/59.96 inference(scs_inference,[],[2716,2740,2659,2724,2735,2726,2697,165,1169,185,151,161,154,166])).
% 59.83/59.96 cnf(2828,plain,
% 59.83/59.96 (P1(f5(x28281,x28281,x28282),x28281,x28282)),
% 59.83/59.96 inference(scs_inference,[],[2669,2665,2716,2740,2659,2724,2735,2714,2726,2697,2683,165,1169,185,151,161,154,166,256,224,254,257,150])).
% 59.83/59.96 cnf(2830,plain,
% 59.83/59.96 (P4(x28301,x28302,x28301,x28303,x28302,x28302,x28302,x28303)),
% 59.83/59.96 inference(scs_inference,[],[2675,2669,2665,2716,2740,2659,2724,2735,2714,2726,2697,2683,165,1169,185,151,161,154,166,256,224,254,257,150,222])).
% 59.83/59.96 cnf(2832,plain,
% 59.83/59.96 (P1(x28321,f5(x28322,x28322,x28321),x28322)),
% 59.83/59.96 inference(scs_inference,[],[2675,2669,2665,2716,2740,2659,2724,2735,2714,2726,2697,2683,165,1169,185,151,161,154,166,256,224,254,257,150,222,149])).
% 59.83/59.96 cnf(2836,plain,
% 59.83/59.96 (P3(x28361,x28361,a2,f27(a2,a2,a2,a2,a2))),
% 59.83/59.96 inference(scs_inference,[],[2675,2669,2665,2716,2740,2659,2724,2735,2714,2726,2758,2697,2683,165,1169,185,151,161,154,166,256,224,254,257,150,222,149,223,162])).
% 59.83/59.96 cnf(2842,plain,
% 59.83/59.96 (P10(a2,a2,x28421,x28421)),
% 59.83/59.96 inference(scs_inference,[],[2675,2669,2742,2647,2665,2716,2740,2659,2724,2735,2714,2726,2758,2697,2683,2311,165,1169,185,151,161,154,166,256,224,254,257,150,222,149,223,162,255,164,163])).
% 59.83/59.96 cnf(2844,plain,
% 59.83/59.96 (P4(x28441,x28442,x28443,x28442,x28441,x28443,x28443,x28443)),
% 59.83/59.96 inference(scs_inference,[],[2673,2675,2669,2742,2647,2665,2716,2740,2659,2724,2735,2714,2726,2758,2697,2683,2311,165,1169,185,151,161,154,166,256,224,254,257,150,222,149,223,162,255,164,163,253])).
% 59.83/59.96 cnf(2848,plain,
% 59.83/59.96 (P4(x28481,x28482,x28482,x28483,x28483,x28481,x28483,x28483)),
% 59.83/59.96 inference(scs_inference,[],[2673,2675,2669,2742,2647,2665,2716,2740,2659,2724,2735,2714,2726,2758,2697,2793,2683,2311,165,1169,185,151,161,154,166,256,224,254,257,150,222,149,223,162,255,164,163,253,152,252])).
% 59.83/59.96 cnf(2857,plain,
% 59.83/59.96 (P10(x28571,x28572,x28572,x28571)),
% 59.83/59.96 inference(rename_variables,[],[2394])).
% 59.83/59.96 cnf(2859,plain,
% 59.83/59.96 (P5(x28591,x28591,x28591,f3(x28591,x28591,x28591))),
% 59.83/59.96 inference(scs_inference,[],[2673,2787,2675,2351,2669,2695,2742,2647,2665,2716,2740,2753,2659,2724,2735,2714,2726,2758,2697,2793,2683,2521,2493,2311,2394,165,1169,185,151,161,154,166,256,224,254,257,150,222,149,223,162,255,164,163,253,152,252,250,251,261,176,186])).
% 59.83/59.96 cnf(2860,plain,
% 59.83/59.96 (P10(x28601,x28602,x28601,x28602)),
% 59.83/59.96 inference(rename_variables,[],[2521])).
% 59.83/59.96 cnf(2861,plain,
% 59.83/59.96 (P5(x28611,x28611,x28612,x28612)),
% 59.83/59.96 inference(rename_variables,[],[2787])).
% 59.83/59.96 cnf(2864,plain,
% 59.83/59.96 (P10(x28641,x28641,a2,a2)),
% 59.83/59.96 inference(rename_variables,[],[2742])).
% 59.83/59.96 cnf(2865,plain,
% 59.83/59.96 (P8(f25(x28651,x28651,x28651,x28651,x28651,x28651),x28651,x28651)),
% 59.83/59.96 inference(rename_variables,[],[2724])).
% 59.83/59.96 cnf(2867,plain,
% 59.83/59.96 (P5(f7(x28671,x28671,x28671,x28671),x28671,f7(x28671,x28671,x28671,x28671),x28671)),
% 59.83/59.96 inference(scs_inference,[],[2673,2787,2675,2351,2669,2695,2742,2647,2665,2716,2740,2753,2659,2724,2485,2735,2714,2726,2758,2697,2793,2683,2521,2493,2311,2394,2602,165,1169,185,151,161,154,166,256,224,254,257,150,222,149,223,162,255,164,163,253,152,252,250,251,261,176,186,172,171])).
% 59.83/59.96 cnf(2868,plain,
% 59.83/59.96 (P10(f7(x28681,x28681,x28681,x28681),x28681,x28681,x28681)),
% 59.83/59.96 inference(rename_variables,[],[2485])).
% 59.83/59.96 cnf(2872,plain,
% 59.83/59.96 (P4(x28721,x28722,x28723,x28723,x28721,x28722,a2,a2)),
% 59.83/59.96 inference(rename_variables,[],[2703])).
% 59.83/59.96 cnf(2877,plain,
% 59.83/59.96 (P10(x28771,x28771,a2,a2)),
% 59.83/59.96 inference(rename_variables,[],[2742])).
% 59.83/59.96 cnf(2880,plain,
% 59.83/59.96 (P10(x28801,x28802,x28802,x28801)),
% 59.83/59.96 inference(rename_variables,[],[2394])).
% 59.83/59.96 cnf(2883,plain,
% 59.83/59.96 (P10(x28831,x28832,x28832,x28831)),
% 59.83/59.96 inference(rename_variables,[],[2394])).
% 59.83/59.96 cnf(2885,plain,
% 59.83/59.96 (P4(a19,a1,a19,a19,a19,a19,a19,a19)),
% 59.83/59.96 inference(scs_inference,[],[2673,2787,2675,2351,2669,2695,2703,2742,2864,2877,2647,2665,2716,2740,2753,2659,2724,2485,2868,2735,2714,2726,2758,2697,2793,2683,2521,2493,2311,2394,2857,2880,2883,1941,2602,165,1169,185,151,161,154,166,256,224,254,257,150,222,149,223,162,255,164,163,253,152,252,250,251,261,176,186,172,171,239,182,196,187,175,227])).
% 59.83/59.96 cnf(2886,plain,
% 59.83/59.96 (P10(x28861,x28862,x28862,x28861)),
% 59.83/59.96 inference(rename_variables,[],[2394])).
% 59.83/59.96 cnf(2891,plain,
% 59.83/59.96 (P3(f27(x28911,x28911,x28911,x28911,x28911),x28911,x28911,x28911)),
% 59.83/59.96 inference(scs_inference,[],[2673,2787,2861,2675,2351,2669,2695,2703,2742,2864,2877,2647,2665,2716,2740,2753,2659,2724,2485,2868,2735,2714,2726,2758,2697,2793,2683,2521,2860,2493,2311,2394,2857,2880,2883,2886,1941,2602,165,1169,185,151,161,154,166,256,224,254,257,150,222,149,223,162,255,164,163,253,152,252,250,251,261,176,186,172,171,239,182,196,187,175,227,188,199])).
% 59.83/59.96 cnf(2892,plain,
% 59.83/59.96 (P10(x28921,x28922,x28921,x28922)),
% 59.83/59.96 inference(rename_variables,[],[2521])).
% 59.83/59.96 cnf(2893,plain,
% 59.83/59.96 (P5(x28931,x28931,x28932,x28932)),
% 59.83/59.96 inference(rename_variables,[],[2787])).
% 59.83/59.96 cnf(2898,plain,
% 59.83/59.96 (P5(x28981,x28981,x28981,f27(x28981,x28981,x28981,x28981,x28981))),
% 59.83/59.96 inference(scs_inference,[],[2673,2787,2861,2893,2675,2351,2669,2695,2703,2742,2864,2877,2647,2665,2716,2740,2753,2659,2724,2485,2868,2735,2714,2726,2758,2697,2793,2683,2521,2860,2892,2493,2311,2394,2857,2880,2883,2886,1941,2602,165,1169,185,151,161,154,166,256,224,254,257,150,222,149,223,162,255,164,163,253,152,252,250,251,261,176,186,172,171,239,182,196,187,175,227,188,199,195,197])).
% 59.83/59.96 cnf(2900,plain,
% 59.83/59.96 (P5(x29001,x29001,x29002,x29002)),
% 59.83/59.96 inference(rename_variables,[],[2787])).
% 59.83/59.96 cnf(2902,plain,
% 59.83/59.96 (P10(f6(x29021,x29021,x29021),f6(x29021,x29021,x29021),x29021,f6(x29021,x29021,x29021))),
% 59.83/59.96 inference(scs_inference,[],[2673,2787,2861,2893,2900,2675,2351,2669,2695,2703,2742,2864,2877,2647,2665,2716,2740,2753,2659,2724,2485,2868,2735,2714,2726,2758,2697,2793,2683,2521,2860,2892,2493,2311,2394,2857,2880,2883,2886,1941,2602,165,1169,185,151,161,154,166,256,224,254,257,150,222,149,223,162,255,164,163,253,152,252,250,251,261,176,186,172,171,239,182,196,187,175,227,188,199,195,197,179])).
% 59.83/59.96 cnf(2903,plain,
% 59.83/59.96 (P5(x29031,x29031,x29032,x29032)),
% 59.83/59.96 inference(rename_variables,[],[2787])).
% 59.83/59.96 cnf(2905,plain,
% 59.83/59.96 (P9(f25(x29051,x29051,x29051,x29051,x29051,x29051),x29051,x29051,x29051,f25(x29051,x29051,x29051,x29051,x29051,x29051),x29051,x29051,x29051)),
% 59.83/59.96 inference(scs_inference,[],[2673,2787,2861,2893,2900,2675,2351,2669,2695,2703,2742,2864,2877,2647,2665,2716,2740,2753,2659,2724,2865,2485,2868,2735,2714,2726,2758,2697,2793,2683,2521,2860,2892,2493,2311,2394,2857,2880,2883,2886,1941,2602,165,1169,185,151,161,154,166,256,224,254,257,150,222,149,223,162,255,164,163,253,152,252,250,251,261,176,186,172,171,239,182,196,187,175,227,188,199,195,197,179,221])).
% 59.83/59.96 cnf(2907,plain,
% 59.83/59.96 (P3(f25(a2,a2,a2,a2,a2,a2),a2,x29071,x29071)),
% 59.83/59.96 inference(scs_inference,[],[2673,2787,2861,2893,2900,2675,2351,2669,2695,2703,2872,2742,2864,2877,2647,2665,2716,2740,2753,2706,2659,2724,2865,2485,2868,2735,2714,2726,2758,2697,2793,2683,2521,2860,2892,2493,2311,2394,2857,2880,2883,2886,1941,2602,165,1169,185,151,161,154,166,256,224,254,257,150,222,149,223,162,255,164,163,253,152,252,250,251,261,176,186,172,171,239,182,196,187,175,227,188,199,195,197,179,221,238])).
% 59.83/59.96 cnf(2915,plain,
% 59.83/59.96 (P8(f25(x29151,x29151,x29151,x29151,x29151,x29151),x29151,x29151)),
% 59.83/59.96 inference(rename_variables,[],[2724])).
% 59.83/59.96 cnf(2919,plain,
% 59.83/59.96 (P5(x29191,x29191,x29192,x29192)),
% 59.83/59.96 inference(rename_variables,[],[2787])).
% 59.83/59.96 cnf(2922,plain,
% 59.83/59.96 (P2(f9(a19,a19,a1),a19,a19,a1)),
% 59.83/59.96 inference(scs_inference,[],[2673,2787,2861,2893,2900,2903,2675,2677,2687,2351,2669,2695,2703,2872,2699,2742,2864,2877,2647,2665,2716,2740,2753,2706,2659,2724,2865,2915,2485,2868,2735,2714,2726,2758,2697,2793,2683,442,2521,2860,2892,2493,2311,2394,2857,2880,2883,2886,1941,2602,165,1169,185,151,161,154,166,256,224,254,257,150,222,149,223,162,255,164,163,253,152,252,250,251,261,176,186,172,171,239,182,196,187,175,227,188,199,195,197,179,221,238,260,225,193,190])).
% 59.83/59.96 cnf(2924,plain,
% 59.83/59.96 (P8(f25(x29241,x29241,x29241,x29241,x29241,x29241),x29241,x29241)),
% 59.83/59.96 inference(rename_variables,[],[2724])).
% 59.83/59.96 cnf(2926,plain,
% 59.83/59.96 (P9(a1,a2,a2,a15,a1,a2,a2,a15)),
% 59.83/59.96 inference(scs_inference,[],[142,2673,2787,2861,2893,2900,2903,2675,2677,2687,2351,2669,2695,2703,2872,2699,2742,2864,2877,2647,2665,2716,2740,2753,2706,2659,2724,2865,2915,2485,2868,2735,2714,2726,2758,2697,2793,2683,442,2521,2860,2892,2493,2311,2394,2857,2880,2883,2886,1941,2305,2602,165,1169,185,151,161,154,166,256,224,254,257,150,222,149,223,162,255,164,163,253,152,252,250,251,261,176,186,172,171,239,182,196,187,175,227,188,199,195,197,179,221,238,260,225,193,190,226])).
% 59.83/59.96 cnf(2930,plain,
% 59.83/59.96 (P2(x29301,x29301,x29301,x29301)),
% 59.83/59.96 inference(rename_variables,[],[2420])).
% 59.83/59.96 cnf(2931,plain,
% 59.83/59.96 (P5(x29311,x29311,x29312,x29312)),
% 59.83/59.96 inference(rename_variables,[],[2787])).
% 59.83/59.96 cnf(2937,plain,
% 59.83/59.96 (P8(f21(x29371,x29372),x29371,x29372)),
% 59.83/59.96 inference(scs_inference,[],[142,2673,2787,2861,2893,2900,2903,2919,2931,2675,2677,2687,2351,2669,2695,2703,2872,2705,2699,2742,2864,2877,2647,2665,2716,2740,2753,2706,2659,2724,2865,2915,2924,2485,2868,2735,2714,2726,2758,2697,2793,2683,442,2521,2860,2892,2493,2311,2394,2857,2880,2883,2886,1941,2305,2420,2930,2147,2602,2343,165,1169,185,151,161,154,166,256,224,254,257,150,222,149,223,162,255,164,163,253,152,252,250,251,261,176,186,172,171,239,182,196,187,175,227,188,199,195,197,179,221,238,260,225,193,190,226,210,211,157])).
% 59.83/59.96 cnf(2942,plain,
% 59.83/59.96 (P3(a19,a1,a19,a19)),
% 59.83/59.96 inference(scs_inference,[],[142,2673,2787,2861,2893,2900,2903,2919,2931,2675,2677,2687,2351,2669,2695,2703,2872,2705,2699,2742,2864,2877,2647,2665,2716,2740,2753,2706,2659,2724,2865,2915,2924,2485,2868,2735,2714,2726,2758,2697,2793,2683,442,2521,2860,2892,2493,2311,2394,2857,2880,2883,2886,1941,2305,2420,2930,2147,2602,2343,165,1169,185,151,161,154,166,256,224,254,257,150,222,149,223,162,255,164,163,253,152,252,250,251,261,176,186,172,171,239,182,196,187,175,227,188,199,195,197,179,221,238,260,225,193,190,226,210,211,157,231])).
% 59.83/59.96 cnf(2957,plain,
% 59.83/59.96 (P10(x29571,f5(x29571,x29571,x29572),x29572,x29571)),
% 59.83/59.96 inference(rename_variables,[],[2749])).
% 59.83/59.96 cnf(2963,plain,
% 59.83/59.96 (P3(a19,a19,a19,a1)),
% 59.83/59.96 inference(scs_inference,[],[2942,2818,2749,2937,1169,165,151,161])).
% 59.83/59.96 cnf(2969,plain,
% 59.83/59.96 (P9(a1,a19,a1,a19,a19,a1,a1,a19)),
% 59.83/59.96 inference(scs_inference,[],[2519,2942,2816,2818,2749,2937,1169,165,151,161,154,166,256])).
% 59.83/59.96 cnf(2973,plain,
% 59.83/59.96 (P4(x29731,x29731,x29731,x29732,x29733,x29731,x29733,x29732)),
% 59.83/59.96 inference(scs_inference,[],[2519,2942,2816,2818,2749,2937,2517,1169,165,151,161,154,166,256,224,222])).
% 59.83/59.96 cnf(2975,plain,
% 59.83/59.96 (P9(a1,a2,a1,a2,a2,a15,a2,a15)),
% 59.83/59.96 inference(scs_inference,[],[2519,2926,2942,2816,2818,2749,2937,2517,1169,165,151,161,154,166,256,224,222,257])).
% 59.83/59.96 cnf(2979,plain,
% 59.83/59.96 (P1(x29791,x29792,f5(x29792,x29792,x29791))),
% 59.83/59.96 inference(scs_inference,[],[2519,2926,2942,2816,2818,2749,2832,2937,2357,2517,1169,165,151,161,154,166,256,224,222,257,254,150])).
% 59.83/59.96 cnf(2981,plain,
% 59.83/59.96 (P1(x29811,f5(x29811,x29811,x29812),x29812)),
% 59.83/59.96 inference(scs_inference,[],[2519,2926,2942,2816,2818,2749,2828,2832,2937,2357,2517,1169,165,151,161,154,166,256,224,222,257,254,150,149])).
% 59.83/59.96 cnf(2983,plain,
% 59.83/59.96 (P9(a2,a15,a1,a2,a2,a15,a1,a2)),
% 59.83/59.96 inference(scs_inference,[],[2519,2926,2942,2816,2818,2749,2828,2832,2937,2357,2517,1169,165,151,161,154,166,256,224,222,257,254,150,149,255])).
% 59.83/59.96 cnf(2985,plain,
% 59.83/59.96 (P10(x29851,f6(x29851,x29851,x29851),f6(x29851,x29851,x29851),f6(x29851,x29851,x29851))),
% 59.83/59.96 inference(scs_inference,[],[2519,2926,2942,2816,2902,2818,2749,2828,2832,2937,2357,2517,1169,165,151,161,154,166,256,224,222,257,254,150,149,255,163])).
% 59.83/59.96 cnf(2991,plain,
% 59.83/59.96 (P10(x29911,f5(x29911,x29911,x29912),x29911,x29912)),
% 59.83/59.96 inference(scs_inference,[],[2519,2926,2814,2942,2816,2902,2818,2749,2957,2828,2832,2937,2491,2357,2517,1169,165,151,161,154,166,256,224,222,257,254,150,149,255,163,162,223,164])).
% 59.83/59.96 cnf(2993,plain,
% 59.83/59.96 (P4(x29931,x29932,x29932,x29932,x29931,x29933,x29932,x29933)),
% 59.83/59.96 inference(scs_inference,[],[2830,2519,2926,2814,2942,2816,2902,2818,2749,2957,2828,2832,2937,2491,2357,2517,1169,165,151,161,154,166,256,224,222,257,254,150,149,255,163,162,223,164,253])).
% 59.83/59.96 cnf(2995,plain,
% 59.83/59.96 (P4(x29951,x29952,x29952,x29953,x29951,x29951,x29951,x29953)),
% 59.83/59.96 inference(scs_inference,[],[2830,2519,2926,2814,2942,2816,2902,2818,2749,2957,2828,2832,2937,2491,2357,2517,1169,165,151,161,154,166,256,224,222,257,254,150,149,255,163,162,223,164,253,252])).
% 59.83/59.96 cnf(2997,plain,
% 59.83/59.96 (P8(f21(x29971,x29972),x29972,x29971)),
% 59.83/59.96 inference(scs_inference,[],[2830,2519,2926,2814,2942,2816,2902,2818,2749,2957,2828,2832,2937,2491,2357,2517,1169,165,151,161,154,166,256,224,222,257,254,150,149,255,163,162,223,164,253,252,152])).
% 59.83/59.96 cnf(3003,plain,
% 59.83/59.96 (P1(f5(a2,x30031,x30031),x30031,a2)),
% 59.83/59.96 inference(scs_inference,[],[2830,2844,2848,2519,2926,2842,2814,2942,2816,2902,2818,2749,2957,2828,2832,2937,2491,2357,2517,2394,1169,165,151,161,154,166,256,224,222,257,254,150,149,255,163,162,223,164,253,252,152,250,251,176])).
% 59.83/59.96 cnf(3004,plain,
% 59.83/59.96 (P10(x30041,x30042,x30042,x30041)),
% 59.83/59.96 inference(rename_variables,[],[2394])).
% 59.83/59.96 cnf(3007,plain,
% 59.83/59.96 (P5(x30071,x30071,x30072,x30072)),
% 59.83/59.96 inference(rename_variables,[],[2787])).
% 59.83/59.96 cnf(3010,plain,
% 59.83/59.96 (P10(x30101,x30102,x30102,x30101)),
% 59.83/59.96 inference(rename_variables,[],[2394])).
% 59.83/59.96 cnf(3012,plain,
% 59.83/59.96 (P1(f4(a1,a19,a1),a1,a19)),
% 59.83/59.96 inference(scs_inference,[],[2830,2844,2848,2519,2926,2842,2814,2942,2816,2902,2818,2749,2957,2828,2832,2937,2491,2357,2787,2416,2567,2517,2394,3004,3010,1169,165,151,161,154,166,256,224,222,257,254,150,149,255,163,162,223,164,253,252,152,250,251,176,241,187,175])).
% 59.83/59.96 cnf(3013,plain,
% 59.83/59.96 (P10(x30131,x30132,x30132,x30131)),
% 59.83/59.96 inference(rename_variables,[],[2394])).
% 59.83/59.96 cnf(3015,plain,
% 59.83/59.96 (P2(f25(x30151,x30151,x30151,x30151,x30151,x30151),x30151,x30151,x30151)),
% 59.83/59.96 inference(scs_inference,[],[2830,2844,2848,2519,2926,2842,2814,2942,2816,2902,2818,2749,2957,2828,2832,2937,2491,2357,2787,2416,2567,2517,2394,3004,3010,1169,165,151,161,154,166,256,224,222,257,254,150,149,255,163,162,223,164,253,252,152,250,251,176,241,187,175,182])).
% 59.83/59.96 cnf(3017,plain,
% 59.83/59.96 (P10(a19,a1,a19,a19)),
% 59.83/59.96 inference(scs_inference,[],[2830,2844,2848,2519,2926,2842,2814,2885,2942,2816,2902,2818,2749,2957,2828,2832,2937,2491,2357,2787,2416,2567,2517,2521,2394,3004,3010,1169,165,151,161,154,166,256,224,222,257,254,150,149,255,163,162,223,164,253,252,152,250,251,176,241,187,175,182,239])).
% 59.83/59.96 cnf(3018,plain,
% 59.83/59.96 (P10(x30181,x30182,x30181,x30182)),
% 59.83/59.96 inference(rename_variables,[],[2521])).
% 59.83/59.96 cnf(3030,plain,
% 59.83/59.96 (P3(x30301,x30301,a2,f27(a2,a2,a2,a2,a2))),
% 59.83/59.96 inference(rename_variables,[],[2836])).
% 59.83/59.96 cnf(3032,plain,
% 59.83/59.96 (P3(x30321,a2,x30321,f27(a2,a2,a2,a2,a2))),
% 59.83/59.96 inference(scs_inference,[],[2830,2844,2848,2519,2926,2842,2814,2885,2942,2816,2902,2818,2749,2957,2828,2832,2937,2836,3030,2491,2357,2655,2787,2416,2567,2517,438,2521,2394,3004,3010,3013,1169,165,151,161,154,166,256,224,222,257,254,150,149,255,163,162,223,164,253,252,152,250,251,176,241,187,175,182,239,188,227,179,221,177,238])).
% 59.83/59.96 cnf(3033,plain,
% 59.83/59.96 (P4(x30331,x30332,x30331,x30333,x30332,x30332,x30332,x30333)),
% 59.83/59.96 inference(rename_variables,[],[2830])).
% 59.83/59.96 cnf(3039,plain,
% 59.83/59.96 (~P4(a1,a1,a1,a15,a19,a1,a15,a1)),
% 59.83/59.96 inference(scs_inference,[],[2830,3033,2844,2848,2519,2926,2842,2814,2885,2942,2816,2902,2818,2891,2749,2957,2828,2832,2937,2836,3030,2491,2357,2655,586,2787,2416,2567,2517,438,2521,2394,3004,3010,3013,1169,165,151,161,154,166,256,224,222,257,254,150,149,255,163,162,223,164,253,252,152,250,251,176,241,187,175,182,239,188,227,179,221,177,238,180,260])).
% 59.83/59.96 cnf(3045,plain,
% 59.83/59.96 (P8(f21(x30451,x30452),x30451,x30452)),
% 59.83/59.96 inference(rename_variables,[],[2937])).
% 59.83/59.96 cnf(3047,plain,
% 59.83/59.96 (P8(a1,a19,a1)),
% 59.83/59.96 inference(scs_inference,[],[142,2830,3033,2844,2848,2519,2926,2842,2814,2885,2942,2816,2902,2818,2891,2773,2749,2957,2828,2832,2937,2836,3030,2491,2357,2655,2922,586,2787,2416,2567,2517,438,2521,2394,3004,3010,3013,2147,1169,165,151,161,154,166,256,224,222,257,254,150,149,255,163,162,223,164,253,252,152,250,251,176,241,187,175,182,239,188,227,179,221,177,238,180,260,153,225,237])).
% 59.83/59.96 cnf(3048,plain,
% 59.83/59.96 (P1(x30481,x30482,x30481)),
% 59.83/59.96 inference(rename_variables,[],[2147])).
% 59.83/59.96 cnf(3050,plain,
% 59.83/59.96 (P10(f25(x30501,x30501,x30501,x30501,x30501,x30501),f25(x30501,x30501,x30501,x30501,x30501,x30501),f25(x30501,x30501,x30501,x30501,x30501,x30501),x30501)),
% 59.83/59.96 inference(scs_inference,[],[142,2830,3033,2844,2848,2519,2926,2842,2814,2885,2942,2816,2902,2818,2891,2773,2749,2957,2828,2832,2937,2836,3030,2491,2357,2655,2922,586,2787,3007,2677,2416,2567,2517,438,2521,2394,3004,3010,3013,2147,1169,165,151,161,154,166,256,224,222,257,254,150,149,255,163,162,223,164,253,252,152,250,251,176,241,187,175,182,239,188,227,179,221,177,238,180,260,153,225,237,193])).
% 59.83/59.96 cnf(3052,plain,
% 59.83/59.96 (P6(x30521,x30522,x30522,x30523)),
% 59.83/59.96 inference(rename_variables,[],[2677])).
% 59.83/59.96 cnf(3054,plain,
% 59.83/59.96 (P2(f9(a1,a1,a19),a1,a1,a19)),
% 59.83/59.96 inference(scs_inference,[],[142,2830,3033,2844,2848,2519,2926,2842,2814,2885,2942,2816,2902,2818,2891,2773,2749,2957,2828,2832,2937,3045,2836,3030,2491,2357,2655,2922,586,2787,3007,2677,2687,2416,2567,2517,438,2521,2394,3004,3010,3013,2147,1169,165,151,161,154,166,256,224,222,257,254,150,149,255,163,162,223,164,253,252,152,250,251,176,241,187,175,182,239,188,227,179,221,177,238,180,260,153,225,237,193,190])).
% 59.83/59.96 cnf(3055,plain,
% 59.83/59.96 (P8(f21(x30551,x30552),x30551,x30552)),
% 59.83/59.96 inference(rename_variables,[],[2937])).
% 59.83/59.96 cnf(3058,plain,
% 59.83/59.96 (P8(f6(a19,a1,a19),a19,a19)),
% 59.83/59.96 inference(scs_inference,[],[142,2830,3033,2844,2848,2519,2926,2842,2814,2885,2942,2816,2902,2818,2891,2773,2749,2957,2828,2832,2937,3045,3055,2836,3030,2491,2357,2655,2922,586,2787,3007,2677,2687,2416,2567,2517,438,2521,3018,2394,3004,3010,3013,2147,1169,165,151,161,154,166,256,224,222,257,254,150,149,255,163,162,223,164,253,252,152,250,251,176,241,187,175,182,239,188,227,179,221,177,238,180,260,153,225,237,193,190,184])).
% 59.83/59.96 cnf(3059,plain,
% 59.83/59.96 (P8(f21(x30591,x30592),x30591,x30592)),
% 59.83/59.96 inference(rename_variables,[],[2937])).
% 59.83/59.96 cnf(3065,plain,
% 59.83/59.96 (P10(a2,a17,a19,a19)),
% 59.83/59.96 inference(scs_inference,[],[142,2830,3033,2844,2848,2519,2926,2842,2814,2885,2942,2816,2902,2818,2891,2773,2749,2957,2828,2832,2937,3045,3055,2836,3030,2491,2357,2655,2922,586,2787,3007,2677,2687,2416,2567,2517,438,2521,3018,2394,3004,3010,3013,2716,2147,3048,1169,165,151,161,154,166,256,224,222,257,254,150,149,255,163,162,223,164,253,252,152,250,251,176,241,187,175,182,239,188,227,179,221,177,238,180,260,153,225,237,193,190,184,206,282])).
% 59.83/59.96 cnf(3075,plain,
% 59.83/59.96 (P8(f25(a19,a1,a19,a1,a1,a1),a19,a1)),
% 59.83/59.96 inference(scs_inference,[],[142,2830,3033,2844,2848,2519,2926,2842,2814,2885,2942,2816,2902,2818,2891,2773,2749,2957,2828,2832,2937,3045,3055,2836,3030,2491,2357,2655,2922,586,2787,3007,2677,2687,2416,2567,2517,438,2521,3018,2394,3004,3010,3013,2716,2147,3048,1169,165,151,161,154,166,256,224,222,257,254,150,149,255,163,162,223,164,253,252,152,250,251,176,241,187,175,182,239,188,227,179,221,177,238,180,260,153,225,237,193,190,184,206,282,158,242,202,203,201])).
% 59.83/59.96 cnf(3087,plain,
% 59.83/59.96 (P5(a1,a19,a19,a19)),
% 59.83/59.96 inference(scs_inference,[],[142,2830,3033,2844,2848,2519,2926,2842,2814,2885,2942,2816,2902,2818,2891,2773,2749,2957,2828,2832,2937,3045,3055,3059,2836,3030,2491,2729,2357,2655,2922,586,2787,3007,2677,3052,2687,2416,2567,2517,438,2521,3018,2394,3004,3010,3013,2716,2147,3048,2063,2075,1169,165,151,161,154,166,256,224,222,257,254,150,149,255,163,162,223,164,253,252,152,250,251,176,241,187,175,182,239,188,227,179,221,177,238,180,260,153,225,237,193,190,184,206,282,158,242,202,203,201,171,160,207,249])).
% 59.83/59.96 cnf(3093,plain,
% 59.83/59.96 (P1(x30931,a2,f27(a2,a2,a2,a2,a2))),
% 59.83/59.96 inference(scs_inference,[],[3032,158])).
% 59.83/59.96 cnf(3100,plain,
% 59.83/59.96 (P3(x31001,x31001,f25(a2,a2,a2,a2,a2,a2),a2)),
% 59.83/59.96 inference(scs_inference,[],[3087,2991,2907,3032,158,165,1169,161])).
% 59.83/59.96 cnf(3102,plain,
% 59.83/59.96 (P5(a1,a19,a1,a1)),
% 59.83/59.96 inference(scs_inference,[],[3047,3087,2991,2907,3032,158,165,1169,161,154])).
% 59.83/59.96 cnf(3104,plain,
% 59.83/59.96 (P1(f21(x31041,x31042),x31042,x31041)),
% 59.83/59.96 inference(scs_inference,[],[3047,3087,2991,2997,2907,3032,158,165,1169,161,154,151])).
% 59.83/59.96 cnf(3108,plain,
% 59.83/59.96 (P9(a2,a1,a1,a2,a2,a15,a2,a15)),
% 59.83/59.96 inference(scs_inference,[],[2975,3047,3087,2867,2991,2997,2907,3032,158,165,1169,161,154,151,166,256])).
% 59.83/59.96 cnf(3112,plain,
% 59.83/59.96 (P9(a19,a1,a1,a19,a1,a19,a1,a19)),
% 59.83/59.96 inference(scs_inference,[],[2969,2975,3047,3087,2867,2991,2997,2907,3032,158,165,1169,161,154,151,166,256,224,254])).
% 59.83/59.96 cnf(3116,plain,
% 59.83/59.96 (P9(a2,a15,a2,a15,a1,a2,a1,a2)),
% 59.83/59.96 inference(scs_inference,[],[2969,2975,2983,3047,3087,2867,2991,2979,2997,2907,3032,158,165,1169,161,154,151,166,256,224,254,149,257])).
% 59.83/59.96 cnf(3120,plain,
% 59.83/59.96 (P3(a19,a19,a1,a19)),
% 59.83/59.96 inference(scs_inference,[],[2963,2969,2975,2983,3047,3087,2867,2991,2979,2997,2907,3032,3003,158,165,1169,161,154,151,166,256,224,254,149,257,150,162])).
% 59.83/59.96 cnf(3126,plain,
% 59.83/59.96 (P10(a19,a19,a19,a1)),
% 59.83/59.96 inference(scs_inference,[],[2963,2969,2975,2983,3017,3047,3087,2905,2867,2991,2979,2997,2907,3032,3003,158,165,1169,161,154,151,166,256,224,254,149,257,150,162,223,255,163])).
% 59.83/59.96 cnf(3128,plain,
% 59.83/59.96 (P10(f25(x31281,x31281,x31281,x31281,x31281,x31281),f25(x31281,x31281,x31281,x31281,x31281,x31281),x31281,f25(x31281,x31281,x31281,x31281,x31281,x31281))),
% 59.83/59.96 inference(scs_inference,[],[2963,2969,2975,2983,3017,3047,3087,3050,2905,2867,2991,2979,2997,2907,3032,3003,158,165,1169,161,154,151,166,256,224,254,149,257,150,162,223,255,163,164])).
% 59.83/59.96 cnf(3132,plain,
% 59.83/59.96 (P8(a1,a1,a19)),
% 59.83/59.96 inference(scs_inference,[],[2973,2963,2969,2975,2983,3017,3047,3087,3050,2905,2867,2991,2979,2997,2907,3032,3003,158,165,1169,161,154,151,166,256,224,254,149,257,150,162,223,255,163,164,253,152])).
% 59.83/59.96 cnf(3134,plain,
% 59.83/59.96 (P4(x31341,x31342,x31341,x31341,x31342,x31343,x31341,x31343)),
% 59.83/59.96 inference(scs_inference,[],[2973,2993,2963,2969,2975,2983,3017,3047,3087,3050,2905,2867,2991,2979,2997,2907,3032,3003,158,165,1169,161,154,151,166,256,224,254,149,257,150,162,223,255,163,164,253,152,252])).
% 59.83/59.96 cnf(3136,plain,
% 59.83/59.96 (P4(x31361,x31361,x31361,x31362,x31361,x31363,x31363,x31362)),
% 59.83/59.96 inference(scs_inference,[],[2973,2993,2995,2963,2969,2975,2983,3017,3047,3087,3050,2905,2867,2991,2979,2997,2907,3032,3003,158,165,1169,161,154,151,166,256,224,254,149,257,150,162,223,255,163,164,253,152,252,250])).
% 59.83/59.96 cnf(3141,plain,
% 59.83/59.96 (P10(x31411,x31412,x31411,x31412)),
% 59.83/59.96 inference(rename_variables,[],[2521])).
% 59.83/59.96 cnf(3146,plain,
% 59.83/59.96 (P10(x31461,x31462,x31461,x31462)),
% 59.83/59.96 inference(rename_variables,[],[2521])).
% 59.83/59.96 cnf(3162,plain,
% 59.83/59.96 (P8(f21(x31621,x31622),x31622,x31621)),
% 59.83/59.96 inference(rename_variables,[],[2997])).
% 59.83/59.96 cnf(3164,plain,
% 59.83/59.96 (P3(x31641,x31641,x31642,x31642)),
% 59.83/59.96 inference(scs_inference,[],[2973,2993,2995,2667,2963,2969,2975,2983,3017,3047,3087,3050,2905,2867,2898,2991,2979,2997,3162,2907,3032,3003,2787,2677,2521,3141,2602,158,165,1169,161,154,151,166,256,224,254,149,257,150,162,223,255,163,164,253,152,252,250,251,244,246,248,192,181,228,203,202,156,155])).
% 59.83/59.96 cnf(3169,plain,
% 59.83/59.96 (P2(f8(x31691,x31691,x31692),x31691,x31691,x31692)),
% 59.83/59.96 inference(rename_variables,[],[2553])).
% 59.83/59.96 cnf(3172,plain,
% 59.83/59.96 (P10(x31721,x31722,x31722,x31721)),
% 59.83/59.96 inference(rename_variables,[],[2394])).
% 59.83/59.96 cnf(3174,plain,
% 59.83/59.96 (P8(f25(a19,a1,x31741,x31741,a1,x31741),a19,x31741)),
% 59.83/59.96 inference(scs_inference,[],[2973,2993,2995,2667,2963,2969,2975,2983,3017,3047,3087,3050,2905,2867,2898,2991,2979,2997,3162,2907,3032,3003,2553,2787,2677,2521,3141,2394,2567,2602,158,165,1169,161,154,151,166,256,224,254,149,257,150,162,223,255,163,164,253,152,252,250,251,244,246,248,192,181,228,203,202,156,155,245,170,176,201])).
% 59.83/59.96 cnf(3182,plain,
% 59.83/59.96 (P10(x31821,x31822,x31822,x31821)),
% 59.83/59.96 inference(rename_variables,[],[2394])).
% 59.83/59.96 cnf(3186,plain,
% 59.83/59.96 (P2(f7(x31861,x31861,x31861,x31861),x31861,x31861,x31861)),
% 59.83/59.96 inference(scs_inference,[],[142,2973,2993,2995,2667,2963,2969,2975,2983,3017,3047,3087,3050,2905,2867,2985,2898,2991,2979,2997,3162,2907,3032,3003,2553,2787,2677,2049,2521,3141,2394,3172,2567,2602,158,165,1169,161,154,151,166,256,224,254,149,257,150,162,223,255,163,164,253,152,252,250,251,244,246,248,192,181,228,203,202,156,155,245,170,176,201,196,171,187,241,182])).
% 59.83/59.96 cnf(3192,plain,
% 59.83/59.96 (P10(a1,a1,a1,a19)),
% 59.83/59.96 inference(scs_inference,[],[142,2973,2993,2995,2667,2963,2969,2975,2983,3017,3047,3087,3050,2905,2867,2985,2898,2991,2979,2997,3162,2907,3032,3003,2553,2787,2677,2049,2521,3141,2394,3172,2567,2602,158,165,1169,161,154,151,166,256,224,254,149,257,150,162,223,255,163,164,253,152,252,250,251,244,246,248,192,181,228,203,202,156,155,245,170,176,201,196,171,187,241,182,195,179,239])).
% 59.83/59.96 cnf(3193,plain,
% 59.83/59.96 (P4(x31931,x31931,x31931,x31932,x31933,x31931,x31933,x31932)),
% 59.83/59.96 inference(rename_variables,[],[2973])).
% 59.83/59.96 cnf(3197,plain,
% 59.83/59.96 (P4(x31971,f25(x31971,x31971,x31971,x31971,x31971,x31971),x31971,x31971,x31971,x31971,x31971,x31971)),
% 59.83/59.96 inference(scs_inference,[],[142,2973,2993,2995,2667,2963,2969,2975,2983,3017,3047,3087,3050,2905,2867,2985,3015,2898,2991,2979,2997,3162,2907,3032,3003,2553,2787,2677,2049,2521,3141,2394,3172,3182,2567,2602,158,165,1169,161,154,151,166,256,224,254,149,257,150,162,223,255,163,164,253,152,252,250,251,244,246,248,192,181,228,203,202,156,155,245,170,176,201,196,171,187,241,182,195,179,239,221,227])).
% 59.83/59.96 cnf(3198,plain,
% 59.83/59.96 (P2(f25(x31981,x31981,x31981,x31981,x31981,x31981),x31981,x31981,x31981)),
% 59.83/59.96 inference(rename_variables,[],[3015])).
% 59.83/59.96 cnf(3199,plain,
% 59.83/59.96 (P10(x31991,x31992,x31992,x31991)),
% 59.83/59.96 inference(rename_variables,[],[2394])).
% 59.83/59.96 cnf(3206,plain,
% 59.83/59.96 (P4(x32061,x32061,x32061,x32062,x32063,x32061,x32063,x32062)),
% 59.83/59.96 inference(rename_variables,[],[2973])).
% 59.83/59.96 cnf(3208,plain,
% 59.83/59.96 (~P4(x32081,a1,x32081,a15,a19,a1,a15,a1)),
% 59.83/59.96 inference(scs_inference,[],[142,2973,3193,3206,2993,2995,2667,2963,2969,2975,2983,3017,3039,3047,3087,3050,2905,2867,2985,3015,2898,2991,2979,2997,3162,2907,3032,3003,2553,2787,2677,2049,2521,3141,2394,3172,3182,3199,2567,2602,158,165,1169,161,154,151,166,256,224,254,149,257,150,162,223,255,163,164,253,152,252,250,251,244,246,248,192,181,228,203,202,156,155,245,170,176,201,196,171,187,241,182,195,179,239,221,227,188,238,260])).
% 59.83/59.96 cnf(3209,plain,
% 59.83/59.96 (P4(x32091,x32091,x32091,x32092,x32093,x32091,x32093,x32092)),
% 59.83/59.96 inference(rename_variables,[],[2973])).
% 59.83/59.96 cnf(3215,plain,
% 59.83/59.96 (P8(a19,a19,f6(a19,a1,a19))),
% 59.83/59.96 inference(scs_inference,[],[142,2973,3193,3206,2993,2995,2667,2963,2969,2975,2983,3017,3039,3047,3087,3050,2905,2867,2985,3015,3198,2898,2991,2979,2997,3162,2907,3032,3003,3058,2553,2787,2677,2049,2521,3141,2220,2394,3172,3182,3199,2567,2075,2602,158,165,1169,161,154,151,166,256,224,254,149,257,150,162,223,255,163,164,253,152,252,250,251,244,246,248,192,181,228,203,202,156,155,245,170,176,201,196,171,187,241,182,195,179,239,221,227,188,238,260,225,160])).
% 59.83/59.96 cnf(3217,plain,
% 59.83/59.96 (P1(x32171,x32171,x32172)),
% 59.83/59.96 inference(rename_variables,[],[2220])).
% 59.83/59.96 cnf(3219,plain,
% 59.83/59.96 (P8(x32191,f5(x32191,x32191,x32191),x32191)),
% 59.83/59.96 inference(scs_inference,[],[142,2973,3193,3206,3209,2993,2995,2667,2963,2969,2975,2983,3017,3039,3047,3087,3050,2905,2867,2985,3015,3198,2898,2991,2979,2981,2997,3162,2907,3032,3003,3058,2553,3169,2787,2677,2049,2521,3141,2220,2394,3172,3182,3199,2567,2075,2602,158,165,1169,161,154,151,166,256,224,254,149,257,150,162,223,255,163,164,253,152,252,250,251,244,246,248,192,181,228,203,202,156,155,245,170,176,201,196,171,187,241,182,195,179,239,221,227,188,238,260,225,160,237])).
% 59.83/59.96 cnf(3220,plain,
% 59.83/59.96 (P4(x32201,x32201,x32201,x32202,x32203,x32201,x32203,x32202)),
% 59.83/59.96 inference(rename_variables,[],[2973])).
% 59.83/59.96 cnf(3225,plain,
% 59.83/59.96 (P6(x32251,x32252,x32253,x32251)),
% 59.83/59.96 inference(rename_variables,[],[2675])).
% 59.83/59.96 cnf(3235,plain,
% 59.83/59.96 (P5(x32351,x32352,x32351,x32352)),
% 59.83/59.96 inference(scs_inference,[],[142,2973,3193,3206,3209,3220,2993,2995,2667,2963,2969,2975,2983,3017,3039,3047,3087,3050,2905,2867,2985,3015,3198,2898,2991,2979,2981,2997,3162,2907,3032,3003,3012,3058,2553,3169,2675,3225,2787,2677,2049,2942,2814,2517,2521,3141,3146,2220,3217,2394,3172,3182,3199,2567,2075,2602,158,165,1169,161,154,151,166,256,224,254,149,257,150,162,223,255,163,164,253,152,252,250,251,244,246,248,192,181,228,203,202,156,155,245,170,176,201,196,171,187,241,182,195,179,239,221,227,188,238,260,225,160,237,190,184,226,206,249])).
% 59.83/59.96 cnf(3254,plain,
% 59.83/59.96 (P5(a1,a1,a1,a19)),
% 59.83/59.96 inference(scs_inference,[],[3102,165])).
% 59.83/59.96 cnf(3256,plain,
% 59.83/59.96 (P10(a19,a19,a17,a2)),
% 59.83/59.96 inference(scs_inference,[],[3102,3126,165,1169])).
% 59.83/59.96 cnf(3258,plain,
% 59.83/59.96 (P3(a1,a19,a19,a19)),
% 59.83/59.96 inference(scs_inference,[],[3102,3120,3126,165,1169,161])).
% 59.83/59.96 cnf(3264,plain,
% 59.83/59.96 (P5(x32641,x32642,x32642,x32641)),
% 59.83/59.96 inference(scs_inference,[],[3235,3102,3120,3126,3219,3075,165,1169,161,151,154,166])).
% 59.83/59.96 cnf(3268,plain,
% 59.83/59.96 (P4(x32681,x32682,x32682,x32682,x32682,x32682,x32681,x32682)),
% 59.83/59.96 inference(scs_inference,[],[3235,3112,3102,3120,3126,3219,3075,165,1169,161,151,154,166,256,224])).
% 59.83/59.96 cnf(3274,plain,
% 59.83/59.96 (P9(a2,a1,a2,a15,a1,a2,a2,a15)),
% 59.83/59.96 inference(scs_inference,[],[3235,3112,3102,3108,3120,3126,3219,3104,3075,3093,165,1169,161,151,154,166,256,224,150,149,257])).
% 59.83/59.96 cnf(3276,plain,
% 59.83/59.96 (P9(a2,a15,a2,a15,a2,a1,a1,a2)),
% 59.83/59.96 inference(scs_inference,[],[3235,3112,3102,3108,3120,3126,3219,3104,3075,3093,165,1169,161,151,154,166,256,224,150,149,257,254])).
% 59.83/59.96 cnf(3278,plain,
% 59.83/59.96 (P10(a19,a19,a2,a17)),
% 59.83/59.96 inference(scs_inference,[],[3235,3065,3112,3102,3108,3120,3126,3219,3104,3075,3093,165,1169,161,151,154,166,256,224,150,149,257,254,163])).
% 59.83/59.96 cnf(3284,plain,
% 59.83/59.96 (P4(x32841,x32841,x32842,x32843,x32844,x32844,x32842,x32843)),
% 59.83/59.96 inference(scs_inference,[],[3164,3235,3065,3112,3102,3108,3120,3126,3219,3104,3075,3100,3093,165,1169,161,151,154,166,256,224,150,149,257,254,163,255,162,223])).
% 59.83/59.96 cnf(3286,plain,
% 59.83/59.96 (P10(a19,a19,a1,a19)),
% 59.83/59.96 inference(scs_inference,[],[3164,3235,3065,3112,3102,3108,3120,3126,3219,3104,3075,3100,3093,165,1169,161,151,154,166,256,224,150,149,257,254,163,255,162,223,164])).
% 59.83/59.96 cnf(3294,plain,
% 59.83/59.96 (P8(x32941,x32941,f5(x32941,x32941,x32941))),
% 59.83/59.96 inference(scs_inference,[],[3134,3136,3164,3235,3065,3112,2531,3102,3108,3120,3126,3219,3104,3075,3100,3093,165,1169,161,151,154,166,256,224,150,149,257,254,163,255,162,223,164,253,250,252,152])).
% 59.83/59.96 cnf(3296,plain,
% 59.83/59.96 (P4(x32961,x32962,x32961,x32961,x32963,x32962,x32961,x32963)),
% 59.83/59.96 inference(scs_inference,[],[3134,3136,3164,3235,3065,3112,2531,3102,3108,3120,3126,3219,3104,3075,3100,3093,165,1169,161,151,154,166,256,224,150,149,257,254,163,255,162,223,164,253,250,252,152,251])).
% 59.83/59.96 cnf(3301,plain,
% 59.83/59.96 (P5(x33011,x33012,x33011,x33012)),
% 59.83/59.96 inference(rename_variables,[],[3235])).
% 59.83/59.96 cnf(3314,plain,
% 59.83/59.96 (P10(x33141,x33142,x33142,x33141)),
% 59.83/59.96 inference(rename_variables,[],[2394])).
% 59.83/59.96 cnf(3319,plain,
% 59.83/59.96 (P1(x33191,x33192,x33191)),
% 59.83/59.96 inference(rename_variables,[],[2147])).
% 59.83/59.96 cnf(3321,plain,
% 59.83/59.96 (P8(f25(a1,a19,a1,a19,a1,a1),a1,a19)),
% 59.83/59.96 inference(scs_inference,[],[3134,3136,3164,3235,2131,3065,3112,2531,2489,3102,3108,3120,3126,3132,3192,3219,3104,3075,3100,3093,2753,2147,2394,165,1169,161,151,154,166,256,224,150,149,257,254,163,255,162,223,164,253,250,252,152,251,191,192,246,245,202,203,186,187,241,196,201])).
% 59.83/59.96 cnf(3323,plain,
% 59.83/59.96 (P2(x33231,x33232,x33232,x33232)),
% 59.83/59.96 inference(scs_inference,[],[3134,3136,3164,3235,3301,2131,3065,3112,2531,2489,3102,3108,3120,3126,3132,3192,3219,3104,3075,3100,3093,2753,2147,2394,165,1169,161,151,154,166,256,224,150,149,257,254,163,255,162,223,164,253,250,252,152,251,191,192,246,245,202,203,186,187,241,196,201,182])).
% 59.83/59.96 cnf(3326,plain,
% 59.83/59.96 (P10(x33261,x33262,x33262,x33261)),
% 59.83/59.96 inference(rename_variables,[],[2394])).
% 59.83/59.96 cnf(3329,plain,
% 59.83/59.96 (P5(x33291,x33292,x33291,x33292)),
% 59.83/59.96 inference(rename_variables,[],[3235])).
% 59.83/59.96 cnf(3334,plain,
% 59.83/59.96 (P4(x33341,x33342,x33341,x33341,x33342,x33343,x33341,x33343)),
% 59.83/59.96 inference(rename_variables,[],[3134])).
% 59.83/59.96 cnf(3340,plain,
% 59.83/59.96 (P5(x33401,x33402,x33401,x33402)),
% 59.83/59.96 inference(rename_variables,[],[3235])).
% 59.83/59.96 cnf(3345,plain,
% 59.83/59.96 (P5(x33451,x33452,x33451,x33452)),
% 59.83/59.96 inference(rename_variables,[],[3235])).
% 59.83/59.96 cnf(3349,plain,
% 59.83/59.96 (P10(x33491,x33491,x33492,x33492)),
% 59.83/59.96 inference(scs_inference,[],[3134,3136,3164,3235,3301,3329,3340,3345,2131,3065,3112,2531,2489,3102,3108,3120,3126,3132,3192,3128,3219,3104,3075,3100,3093,3215,651,2753,2598,2147,3319,2394,3314,165,1169,161,151,154,166,256,224,150,149,257,254,163,255,162,223,164,253,250,252,152,251,191,192,246,245,202,203,186,187,241,196,201,182,171,199,175,239,195,197,221,198,227,179])).
% 59.83/59.96 cnf(3352,plain,
% 59.83/59.96 (P10(x33521,x33522,x33522,x33521)),
% 59.83/59.96 inference(rename_variables,[],[2394])).
% 59.83/59.96 cnf(3354,plain,
% 59.83/59.96 (P10(f7(x33541,x33541,x33541,x33541),x33541,x33541,f25(x33541,x33541,x33541,x33541,x33541,x33541))),
% 59.83/59.96 inference(scs_inference,[],[3134,3136,3164,3235,3301,3329,3340,3345,2131,3065,3112,2531,2489,3102,3108,3120,3126,3132,3192,3128,3197,3186,3219,3104,3075,3100,3093,3215,651,2753,2598,2147,3319,2394,3314,3326,165,1169,161,151,154,166,256,224,150,149,257,254,163,255,162,223,164,253,250,252,152,251,191,192,246,245,202,203,186,187,241,196,201,182,171,199,175,239,195,197,221,198,227,179,188,240])).
% 59.83/59.96 cnf(3357,plain,
% 59.83/59.96 (P3(a19,a19,a17,a2)),
% 59.83/59.96 inference(scs_inference,[],[3134,3136,3164,3235,3301,3329,3340,3345,2131,3065,3112,2531,2489,3102,3108,3120,3126,3132,3192,3128,3197,3186,3219,3104,3075,3100,3093,3215,651,2753,2598,2147,3319,2394,3314,3326,165,1169,161,151,154,166,256,224,150,149,257,254,163,255,162,223,164,253,250,252,152,251,191,192,246,245,202,203,186,187,241,196,201,182,171,199,175,239,195,197,221,198,227,179,188,240,238])).
% 59.83/59.96 cnf(3371,plain,
% 59.83/59.96 (P8(x33711,f21(x33711,x33711),x33711)),
% 59.83/59.96 inference(scs_inference,[],[3134,3334,3136,3164,3235,3301,3329,3340,3345,2131,3065,3112,2531,3208,2489,3102,3108,3120,3126,3132,3192,3128,3197,3186,3219,3104,3075,3100,3093,3215,3054,2553,651,2973,2753,2598,2147,3319,2394,3314,3326,2020,2602,165,1169,161,151,154,166,256,224,150,149,257,254,163,255,162,223,164,253,250,252,152,251,191,192,246,245,202,203,186,187,241,196,201,182,171,199,175,239,195,197,221,198,227,179,188,240,238,260,225,160,237])).
% 59.83/59.96 cnf(3377,plain,
% 59.83/59.96 (P8(f25(a19,a1,x33771,x33771,a1,x33771),a19,x33771)),
% 59.83/59.96 inference(rename_variables,[],[3174])).
% 59.83/59.96 cnf(3378,plain,
% 59.83/59.96 (P3(x33781,x33781,x33782,x33782)),
% 59.83/59.96 inference(rename_variables,[],[3164])).
% 59.83/59.96 cnf(3385,plain,
% 59.83/59.96 (P5(x33851,x33852,x33851,x33852)),
% 59.83/59.96 inference(rename_variables,[],[3235])).
% 59.83/59.96 cnf(3388,plain,
% 59.83/59.96 (P5(x33881,x33882,x33881,x33882)),
% 59.83/59.96 inference(rename_variables,[],[3235])).
% 59.83/59.96 cnf(3391,plain,
% 59.83/59.96 (P5(x33911,x33912,x33911,x33912)),
% 59.83/59.96 inference(rename_variables,[],[3235])).
% 59.83/59.96 cnf(3397,plain,
% 59.83/59.96 (~P3(a1,a1,a2,a17)),
% 59.83/59.96 inference(scs_inference,[],[142,3134,3334,3136,3164,3378,3235,3301,3329,3340,3345,3385,3388,2131,3065,3112,2531,3208,2489,3102,3108,3120,3126,3132,3192,3128,3197,3186,3219,3104,3075,3100,3093,3174,3377,3215,3054,2553,651,2973,2705,2687,2753,2740,2598,2521,2147,3319,2394,3314,3326,2063,2020,2602,165,1169,161,151,154,166,256,224,150,149,257,254,163,255,162,223,164,253,250,252,152,251,191,192,246,245,202,203,186,187,241,196,201,182,171,199,175,239,195,197,221,198,227,179,188,240,238,260,225,160,237,190,184,209,211,210,204,1121])).
% 59.83/59.96 cnf(3399,plain,
% 59.83/59.96 (P10(f7(x33991,x33991,x33991,a1),x33991,x33991,a1)),
% 59.83/59.96 inference(scs_inference,[],[142,3134,3334,3136,3164,3378,3235,3301,3329,3340,3345,3385,3388,2131,3065,3112,2531,3208,2489,3102,3108,3120,3126,3132,3192,3128,3197,3186,3219,3104,3075,3100,3093,3174,3377,3215,3054,2553,651,2973,2705,2687,2753,2740,2598,2521,2147,3319,2394,3314,3326,2063,2020,2602,165,1169,161,151,154,166,256,224,150,149,257,254,163,255,162,223,164,253,250,252,152,251,191,192,246,245,202,203,186,187,241,196,201,182,171,199,175,239,195,197,221,198,227,179,188,240,238,260,225,160,237,190,184,209,211,210,204,1121,185])).
% 59.83/59.96 cnf(3403,plain,
% 59.83/59.96 (P1(x34031,x34032,f3(x34031,x34031,x34032))),
% 59.83/59.96 inference(scs_inference,[],[142,3134,3334,3136,3164,3378,3235,3301,3329,3340,3345,3385,3388,3391,2131,3065,3112,2531,3208,2489,3102,3108,3120,3126,3132,3192,3128,3197,3186,3219,3104,3075,3100,3093,3174,3377,3215,3054,2553,651,2973,2705,2687,2753,2740,2598,2521,2147,3319,2394,3314,3326,3352,2063,2020,2602,165,1169,161,151,154,166,256,224,150,149,257,254,163,255,162,223,164,253,250,252,152,251,191,192,246,245,202,203,186,187,241,196,201,182,171,199,175,239,195,197,221,198,227,179,188,240,238,260,225,160,237,190,184,209,211,210,204,1121,185,243,174])).
% 59.83/59.96 cnf(3406,plain,
% 59.83/59.96 (~P8(f21(a2,a1),a1,a17)),
% 59.83/59.96 inference(scs_inference,[],[142,3134,3334,3136,3164,3378,3235,3301,3329,3340,3345,3385,3388,3391,2131,3065,3112,2531,3208,2489,3102,3108,3120,3126,3132,3192,3128,3197,3186,3219,3104,3075,3100,3093,3174,3377,3215,3054,2553,651,2973,2997,2705,2687,2753,2740,2598,2521,2147,3319,2394,3314,3326,3352,2063,2020,2602,165,1169,161,151,154,166,256,224,150,149,257,254,163,255,162,223,164,253,250,252,152,251,191,192,246,245,202,203,186,187,241,196,201,182,171,199,175,239,195,197,221,198,227,179,188,240,238,260,225,160,237,190,184,209,211,210,204,1121,185,243,174,155])).
% 59.83/59.96 cnf(3497,plain,
% 59.83/59.96 ($false),
% 59.83/59.96 inference(scs_inference,[],[3268,3296,3264,3284,3323,3349,3254,3116,3256,3258,3274,3276,3278,3286,3357,3397,3354,2859,3294,3371,3403,3406,3399,3321,3174,2997,2687,2309,185,165,1169,151,154,161,166,256,224,150,257,149,254,163,223,164,255,162,253,250,251,152,252,135,244,243,159,228,156,178]),
% 59.83/59.96 ['proof']).
% 59.83/59.96 % SZS output end Proof
% 59.83/59.96 % Total time :59.150000s
%------------------------------------------------------------------------------