%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : GEO619+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 : n001.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Mon Jun 24 06:05:57 EDT 2024
% Result : Theorem 59.51s 59.57s
% Output : CNFRefutation 59.70s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.04/0.13 % Problem : GEO619+1 : TPTP v8.2.0. Released v7.5.0.
% 0.04/0.13 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% 0.12/0.34 % Computer : n001.cluster.edu
% 0.12/0.34 % Model : x86_64 x86_64
% 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.34 % Memory : 8042.1875MB
% 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.34 % CPULimit : 300
% 0.12/0.34 % WCLimit : 300
% 0.12/0.34 % DateTime : Fri Jun 21 10:39:09 EDT 2024
% 0.12/0.34 % CPUTime :
% 0.53/0.62 start to proof:theBenchmark
% 59.51/59.56 %-------------------------------------------
% 59.51/59.56 % File :CSE---1.7
% 59.51/59.56 % Problem :theBenchmark
% 59.51/59.56 % Transform :cnf
% 59.51/59.56 % Format :tptp:raw
% 59.51/59.56 % Command :java -jar mcs_scs.jar %d %s
% 59.51/59.56
% 59.51/59.56 % Result :Theorem 58.860000s
% 59.51/59.56 % Output :CNFRefutation 58.860000s
% 59.51/59.56 %-------------------------------------------
% 59.51/59.57 %------------------------------------------------------------------------------
% 59.51/59.57 % File : GEO619+1 : TPTP v8.2.0. Released v7.5.0.
% 59.51/59.57 % Domain : Geometry
% 59.51/59.57 % Problem : JGEX problem 81
% 59.51/59.57 % Version : [CGZ00] axioms.
% 59.51/59.57 % English :
% 59.51/59.57
% 59.51/59.57 % Refs : [CGZ00] Chou et al. (2000), A Deductive Database Approach to A
% 59.51/59.57 % : [YCG08] Ye et al. (2008), An Introduction to Java Geometry Exp
% 59.51/59.57 % : [Qua20] Quaresma (2020), Email to Geoff Sutcliffe
% 59.51/59.57 % Source : [Qua20]
% 59.51/59.57 % Names : 81.p [Qua20]
% 59.51/59.57
% 59.51/59.57 % Status : Theorem
% 59.51/59.57 % Rating : 0.42 v8.2.0, 0.39 v8.1.0, 0.44 v7.5.0
% 59.51/59.57 % Syntax : Number of formulae : 95 ( 0 unt; 0 def)
% 59.51/59.57 % Number of atoms : 295 ( 1 equ)
% 59.51/59.57 % Maximal formula atoms : 12 ( 3 avg)
% 59.51/59.57 % Number of connectives : 207 ( 7 ~; 0 |; 105 &)
% 59.51/59.57 % ( 0 <=>; 95 =>; 0 <=; 0 <~>)
% 59.51/59.57 % Maximal formula depth : 24 ( 9 avg)
% 59.51/59.57 % Maximal term depth : 1 ( 1 avg)
% 59.51/59.57 % Number of predicates : 12 ( 11 usr; 0 prp; 2-8 aty)
% 59.51/59.57 % Number of functors : 0 ( 0 usr; 0 con; --- aty)
% 59.51/59.57 % Number of variables : 534 ( 514 !; 20 ?)
% 59.51/59.57 % SPC : FOF_THM_RFO_SEQ
% 59.51/59.57
% 59.51/59.57 % Comments : Taken from JGEX [YCG08], converted by Pedro Quaresma.
% 59.51/59.57 %------------------------------------------------------------------------------
% 59.51/59.57 include('Axioms/GEO012+0.ax').
% 59.51/59.57 %------------------------------------------------------------------------------
% 59.51/59.57 fof(exemplo6GDDFULL8110981,conjecture,
% 59.51/59.57 ! [A,B,C,D,E,F,G,H,NWPNT1,NWPNT2,NWPNT3,NWPNT4] :
% 59.51/59.57 ( ( perp(C,A,C,B)
% 59.51/59.57 & cong(A,C,B,C)
% 59.51/59.57 & coll(D,A,B)
% 59.51/59.57 & eqangle(E,C,C,A,A,C,C,D)
% 59.51/59.57 & coll(E,A,B)
% 59.51/59.57 & midp(F,D,E)
% 59.51/59.57 & circle(F,E,NWPNT1,NWPNT2)
% 59.51/59.57 & coll(G,C,E)
% 59.51/59.57 & circle(F,E,G,NWPNT3)
% 59.51/59.57 & coll(H,C,D)
% 59.51/59.57 & circle(F,E,H,NWPNT4) )
% 59.51/59.57 => cong(D,G,D,H) ) ).
% 59.51/59.57
% 59.51/59.57 %------------------------------------------------------------------------------
% 59.51/59.57 %-------------------------------------------
% 59.51/59.57 % Proof found
% 59.51/59.57 % SZS status Theorem for theBenchmark
% 59.51/59.57 % SZS output start Proof
% 59.51/59.58 %ClaNum:266(EqnAxiom:141)
% 59.51/59.58 %VarNum:1613(SingletonVarNum:590)
% 59.51/59.58 %MaxLitNum:5
% 59.51/59.58 %MaxfuncDepth:1
% 59.51/59.58 %SharedTerms:24
% 59.51/59.58 %goalClause: 142 143 144 145 146 147 148 149 150 151 152 153
% 59.51/59.58 %singleGoalClaCount:12
% 59.51/59.58 [142]P1(a1,a2,a15)
% 59.51/59.58 [143]P1(a17,a2,a15)
% 59.51/59.58 [144]P1(a18,a16,a17)
% 59.51/59.58 [145]P1(a20,a16,a1)
% 59.51/59.58 [146]P3(a19,a1,a17)
% 59.51/59.58 [147]P9(a16,a2,a16,a15)
% 59.51/59.58 [148]P4(a2,a16,a15,a16)
% 59.51/59.58 [149]P2(a19,a17,a18,a21)
% 59.51/59.58 [150]P2(a19,a17,a20,a25)
% 59.51/59.58 [151]P2(a19,a17,a22,a23)
% 59.51/59.58 [152]P5(a17,a16,a16,a2,a2,a16,a16,a1)
% 59.51/59.58 [153]~P4(a1,a18,a1,a20)
% 59.51/59.58 [154]~P1(x1542,x1541,x1543)+P1(x1541,x1542,x1543)
% 59.51/59.58 [155]~P1(x1551,x1553,x1552)+P1(x1551,x1552,x1553)
% 59.51/59.58 [156]~P3(x1561,x1562,x1563)+P1(x1561,x1562,x1563)
% 59.51/59.58 [157]~P3(x1571,x1573,x1572)+P3(x1571,x1572,x1573)
% 59.51/59.58 [159]~P3(x1591,x1592,x1593)+P4(x1591,x1592,x1591,x1593)
% 59.51/59.58 [163]~P10(x1631,x1632,x1631,x1633)+P1(x1631,x1632,x1633)
% 59.51/59.58 [229]~P4(x2291,x2292,x2291,x2293)+P5(x2291,x2292,x2292,x2293,x2292,x2293,x2291,x2293)
% 59.51/59.58 [166]~P10(x1663,x1664,x1661,x1662)+P10(x1661,x1662,x1663,x1664)
% 59.51/59.58 [167]~P10(x1671,x1672,x1674,x1673)+P10(x1671,x1672,x1673,x1674)
% 59.51/59.58 [168]~P9(x1683,x1684,x1681,x1682)+P9(x1681,x1682,x1683,x1684)
% 59.51/59.58 [169]~P9(x1691,x1692,x1694,x1693)+P9(x1691,x1692,x1693,x1694)
% 59.51/59.58 [170]~P4(x1703,x1704,x1701,x1702)+P4(x1701,x1702,x1703,x1704)
% 59.51/59.58 [171]~P4(x1711,x1712,x1714,x1713)+P4(x1711,x1712,x1713,x1714)
% 59.51/59.58 [172]~P6(x1722,x1721,x1723,x1724)+P6(x1721,x1722,x1723,x1724)
% 59.51/59.58 [173]~P6(x1731,x1733,x1732,x1734)+P6(x1731,x1732,x1733,x1734)
% 59.51/59.58 [174]~P6(x1741,x1742,x1744,x1743)+P6(x1741,x1742,x1743,x1744)
% 59.51/59.58 [227]~P6(x2272,x2273,x2271,x2274)+P5(x2271,x2272,x2271,x2273,x2274,x2272,x2274,x2273)
% 59.51/59.58 [190]~P2(x1904,x1901,x1902,x1903)+P9(f7(x1901,x1902,x1903,x1904),x1901,x1901,x1904)
% 59.51/59.58 [205]P4(x2051,x2052,x2053,x2054)+~P7(x2051,x2052,x2055,x2053,x2054,x2056)
% 59.51/59.58 [217]~P11(x2174,x2175,x2176,x2171,x2172,x2173)+P11(x2171,x2172,x2173,x2174,x2175,x2176)
% 59.51/59.58 [218]~P11(x2182,x2181,x2183,x2185,x2184,x2186)+P11(x2181,x2182,x2183,x2184,x2185,x2186)
% 59.51/59.58 [219]~P11(x2191,x2193,x2192,x2194,x2196,x2195)+P11(x2191,x2192,x2193,x2194,x2195,x2196)
% 59.51/59.58 [220]~P7(x2204,x2205,x2206,x2201,x2202,x2203)+P7(x2201,x2202,x2203,x2204,x2205,x2206)
% 59.51/59.58 [221]~P7(x2212,x2211,x2213,x2215,x2214,x2216)+P7(x2211,x2212,x2213,x2214,x2215,x2216)
% 59.51/59.58 [222]~P7(x2221,x2223,x2222,x2224,x2226,x2225)+P7(x2221,x2222,x2223,x2224,x2225,x2226)
% 59.51/59.58 [228]~P10(x2281,x2282,x2285,x2286)+P5(x2281,x2282,x2283,x2284,x2285,x2286,x2283,x2284)
% 59.51/59.58 [234]~P11(x2341,x2342,x2343,x2344,x2345,x2346)+P5(x2341,x2342,x2342,x2343,x2344,x2345,x2345,x2346)
% 59.51/59.58 [235]~P11(x2351,x2352,x2353,x2354,x2355,x2356)+P8(x2351,x2352,x2351,x2353,x2354,x2355,x2354,x2356)
% 59.51/59.58 [236]~P5(x2361,x2362,x2365,x2366,x2363,x2364,x2365,x2366)+P10(x2361,x2362,x2363,x2364)
% 59.51/59.58 [255]~P5(x2555,x2556,x2557,x2558,x2551,x2552,x2553,x2554)+P5(x2551,x2552,x2553,x2554,x2555,x2556,x2557,x2558)
% 59.51/59.58 [256]~P5(x2563,x2564,x2561,x2562,x2567,x2568,x2565,x2566)+P5(x2561,x2562,x2563,x2564,x2565,x2566,x2567,x2568)
% 59.51/59.58 [257]~P5(x2572,x2571,x2573,x2574,x2575,x2576,x2577,x2578)+P5(x2571,x2572,x2573,x2574,x2575,x2576,x2577,x2578)
% 59.51/59.58 [258]~P5(x2581,x2582,x2585,x2586,x2583,x2584,x2587,x2588)+P5(x2581,x2582,x2583,x2584,x2585,x2586,x2587,x2588)
% 59.51/59.58 [259]~P8(x2595,x2596,x2597,x2598,x2591,x2592,x2593,x2594)+P8(x2591,x2592,x2593,x2594,x2595,x2596,x2597,x2598)
% 59.51/59.58 [260]~P8(x2603,x2604,x2601,x2602,x2607,x2608,x2605,x2606)+P8(x2601,x2602,x2603,x2604,x2605,x2606,x2607,x2608)
% 59.51/59.58 [261]~P8(x2612,x2611,x2613,x2614,x2615,x2616,x2617,x2618)+P8(x2611,x2612,x2613,x2614,x2615,x2616,x2617,x2618)
% 59.51/59.58 [262]~P8(x2621,x2622,x2625,x2626,x2623,x2624,x2627,x2628)+P8(x2621,x2622,x2623,x2624,x2625,x2626,x2627,x2628)
% 59.51/59.58 [164]~P1(x1641,x1642,x1643)+~P4(x1641,x1642,x1641,x1643)+P3(x1641,x1642,x1643)
% 59.51/59.58 [238]P4(x2381,x2382,x2381,x2383)+~P5(x2381,x2382,x2382,x2383,x2382,x2383,x2381,x2383)+P1(x2381,x2382,x2383)
% 59.51/59.58 [179]~P9(x1791,x1792,x1792,x1793)+~P4(x1792,x1791,x1792,x1793)+P1(x1791,x1792,f3(x1791,x1793,x1792))
% 59.51/59.58 [191]~P9(x1912,x1911,x1911,x1913)+~P4(x1911,x1912,x1911,x1913)+P4(x1911,x1912,x1911,f3(x1912,x1913,x1911))
% 59.51/59.58 [158]~P1(x1583,x1584,x1581)+P1(x1581,x1582,x1583)+~P1(x1583,x1584,x1582)
% 59.51/59.58 [175]~P2(x1754,x1751,x1752,x1753)+P9(x1751,x1752,x1752,x1753)+~P1(x1754,x1751,x1753)
% 59.51/59.58 [176]~P9(x1761,x1764,x1762,x1763)+P4(x1761,x1762,x1761,x1763)+~P3(x1764,x1762,x1763)
% 59.51/59.58 [177]~P9(x1771,x1773,x1773,x1774)+P4(x1771,x1772,x1773,x1772)+~P3(x1772,x1771,x1774)
% 59.51/59.58 [184]~P4(x1841,x1844,x1842,x1844)+~P4(x1841,x1843,x1842,x1843)+P9(x1841,x1842,x1843,x1844)
% 59.51/59.58 [187]~P4(x1871,x1872,x1871,x1874)+~P4(x1871,x1872,x1871,x1873)+P2(x1871,x1872,x1873,x1874)
% 59.51/59.58 [233]~P10(x2331,x2334,x2333,x2332)+~P6(x2331,x2334,x2333,x2332)+P5(x2331,x2332,x2333,x2332,x2333,x2332,x2333,x2334)
% 59.51/59.58 [237]~P5(x2371,x2373,x2371,x2374,x2372,x2373,x2372,x2374)+P1(x2371,x2372,x2373)+P6(x2373,x2374,x2371,x2372)
% 59.51/59.58 [239]~P1(x2393,x2394,x2392)+~P5(x2393,x2391,x2393,x2392,x2394,x2391,x2394,x2392)+P6(x2391,x2392,x2393,x2394)
% 59.51/59.58 [241]P9(x2411,x2412,x2413,x2414)+~P5(x2411,x2412,x2413,x2414,x2413,x2414,x2411,x2412)+P10(x2411,x2412,x2413,x2414)
% 59.51/59.58 [180]~P9(x1801,x1804,x1802,x1803)+~P9(x1802,x1804,x1801,x1803)+P1(f4(x1801,x1802,x1803),x1803,x1802)
% 59.51/59.58 [181]~P9(x1811,x1814,x1812,x1813)+~P9(x1812,x1814,x1811,x1813)+P1(f5(x1811,x1812,x1813),x1813,x1811)
% 59.51/59.58 [192]~P9(x1921,x1924,x1922,x1923)+~P9(x1922,x1924,x1921,x1923)+P9(x1921,f4(x1921,x1922,x1923),x1923,x1922)
% 59.51/59.58 [193]~P9(x1931,x1934,x1932,x1933)+~P9(x1932,x1934,x1931,x1933)+P9(x1931,f5(x1932,x1931,x1933),x1933,x1932)
% 59.51/59.58 [194]~P9(x1941,x1943,x1943,x1942)+~P6(x1941,x1942,x1943,x1944)+P2(f8(x1941,x1942,x1943),x1941,x1942,x1943)
% 59.51/59.58 [196]~P9(x1963,x1964,x1962,x1961)+~P4(x1963,x1962,x1963,x1961)+P1(x1961,x1962,f27(x1962,x1961,x1963,x1964))
% 59.51/59.58 [197]~P9(x1973,x1974,x1971,x1972)+~P4(x1973,x1971,x1973,x1972)+P1(f27(x1971,x1972,x1973,x1974),x1973,x1974)
% 59.51/59.58 [248]~P4(x2483,x2482,x2483,x2481)+~P5(x2482,x2483,x2483,x2484,x2483,x2484,x2483,x2481)+P1(x2481,x2482,f24(x2482,x2481,x2483,x2484))
% 59.51/59.58 [249]~P9(x2493,x2494,x2492,x2491)+~P5(x2492,x2493,x2493,x2494,x2493,x2494,x2493,x2491)+P1(x2491,x2492,f28(x2492,x2491,x2493,x2494))
% 59.51/59.58 [250]~P9(x2503,x2502,x2502,x2501)+~P5(x2504,x2503,x2502,x2503,x2502,x2503,x2501,x2503)+P1(f14(x2501,x2502,x2503,x2504),x2503,x2504)
% 59.51/59.58 [251]~P9(x2513,x2512,x2512,x2511)+~P5(x2514,x2513,x2512,x2513,x2512,x2513,x2511,x2513)+P1(f14(x2511,x2512,x2513,x2514),x2511,x2512)
% 59.51/59.58 [252]~P4(x2523,x2521,x2523,x2522)+~P5(x2521,x2523,x2523,x2524,x2523,x2524,x2523,x2522)+P1(f24(x2521,x2522,x2523,x2524),x2523,x2524)
% 59.51/59.58 [253]~P9(x2533,x2534,x2531,x2532)+~P5(x2531,x2533,x2533,x2534,x2533,x2534,x2533,x2532)+P1(f28(x2531,x2532,x2533,x2534),x2533,x2534)
% 59.51/59.58 [160]~P3(x1605,x1601,x1603)+P10(x1601,x1602,x1603,x1604)+~P3(x1605,x1602,x1604)
% 59.51/59.58 [161]~P3(x1611,x1615,x1613)+P10(x1611,x1612,x1613,x1614)+~P3(x1612,x1615,x1614)
% 59.51/59.58 [188]~P6(x1885,x1881,x1882,x1883)+P6(x1881,x1882,x1883,x1884)+~P6(x1885,x1881,x1882,x1884)
% 59.51/59.58 [230]~P3(x2305,x2302,x2303)+~P2(x2304,x2301,x2302,x2303)+P5(x2301,x2302,x2301,x2303,x2304,x2302,x2304,x2305)
% 59.51/59.58 [232]~P2(x2325,x2321,x2323,x2324)+P5(x2321,x2322,x2321,x2323,x2324,x2321,x2324,x2323)+~P9(x2325,x2321,x2321,x2322)
% 59.51/59.58 [245]~P5(x2452,x2453,x2452,x2454,x2455,x2452,x2455,x2454)+P9(x2451,x2452,x2452,x2453)+~P2(x2451,x2452,x2454,x2455)
% 59.51/59.58 [200]~P1(x2002,x2004,x2005)+~P9(x2001,x2003,x2003,x2002)+P1(f12(x2001,x2002,x2003,x2004,x2005),x2004,x2005)
% 59.51/59.58 [201]~P1(x2012,x2014,x2015)+~P9(x2011,x2013,x2013,x2012)+P9(f12(x2011,x2012,x2013,x2014,x2015),x2011,x2014,x2015)
% 59.51/59.58 [202]~P9(x2023,x2024,x2024,x2021)+~P4(x2021,x2022,x2021,x2025)+P4(x2021,x2022,x2021,f31(x2023,x2024,x2022,x2025,x2021))
% 59.51/59.58 [203]~P9(x2033,x2031,x2031,x2035)+~P4(x2035,x2032,x2035,x2034)+P4(x2031,x2032,x2031,f31(x2033,x2031,x2032,x2034,x2035))
% 59.51/59.58 [204]~P9(x2041,x2042,x2042,x2045)+~P4(x2045,x2043,x2045,x2044)+P10(f31(x2041,x2042,x2043,x2044,x2045),x2043,x2041,x2042)
% 59.51/59.58 [247]~P5(x2471,x2473,x2472,x2473,x2471,x2474,x2472,x2475)+P1(x2471,x2472,x2473)+P6(x2474,x2472,x2473,f30(x2471,x2472,x2473,x2474))
% 59.51/59.58 [263]~P5(x2631,x2633,x2632,x2633,x2631,x2634,x2632,x2635)+P1(x2631,x2632,x2633)+P5(x2631,x2633,x2632,x2633,x2631,f30(x2631,x2632,x2633,x2634),x2632,f30(x2631,x2632,x2633,x2634))
% 59.51/59.58 [182]~P10(x1821,x1822,x1825,x1826)+P10(x1821,x1822,x1823,x1824)+~P10(x1825,x1826,x1823,x1824)
% 59.51/59.58 [183]~P9(x1831,x1832,x1835,x1836)+P10(x1831,x1832,x1833,x1834)+~P9(x1835,x1836,x1833,x1834)
% 59.51/59.58 [185]~P9(x1855,x1856,x1853,x1854)+P9(x1851,x1852,x1853,x1854)+~P10(x1851,x1852,x1855,x1856)
% 59.51/59.58 [186]~P4(x1861,x1862,x1865,x1866)+P4(x1861,x1862,x1863,x1864)+~P4(x1865,x1866,x1863,x1864)
% 59.51/59.58 [223]~P4(x2231,x2232,x2234,x2235)+~P11(x2231,x2232,x2233,x2234,x2235,x2236)+P7(x2231,x2232,x2233,x2234,x2235,x2236)
% 59.51/59.58 [226]~P3(x2264,x2265,x2266)+~P3(x2261,x2262,x2263)+P8(x2261,x2262,x2262,x2263,x2264,x2265,x2265,x2266)
% 59.51/59.58 [206]~P3(x2066,x2063,x2064)+~P3(x2065,x2061,x2062)+P3(f29(x2061,x2062,x2063,x2064,x2065,x2066),x2061,x2064)
% 59.51/59.58 [207]~P3(x2076,x2073,x2074)+~P3(x2075,x2071,x2072)+P10(f29(x2071,x2072,x2073,x2074,x2075,x2076),x2076,x2071,x2073)
% 59.51/59.58 [208]~P3(x2086,x2083,x2084)+~P3(x2085,x2081,x2082)+P10(f29(x2081,x2082,x2083,x2084,x2085,x2086),x2085,x2082,x2084)
% 59.51/59.58 [243]~P5(x2431,x2432,x2433,x2434,x2435,x2436,x2437,x2438)+P10(x2431,x2432,x2433,x2434)+~P10(x2435,x2436,x2437,x2438)
% 59.51/59.58 [244]~P5(x2441,x2442,x2443,x2444,x2445,x2446,x2447,x2448)+P9(x2441,x2442,x2443,x2444)+~P9(x2445,x2446,x2447,x2448)
% 59.51/59.58 [246]~P8(x2461,x2462,x2463,x2464,x2465,x2466,x2467,x2468)+P4(x2461,x2462,x2463,x2464)+~P4(x2465,x2466,x2467,x2468)
% 59.51/59.58 [224]~P11(x2241,x2242,x2243,x2247,x2248,x2249)+P11(x2241,x2242,x2243,x2244,x2245,x2246)+~P11(x2247,x2248,x2249,x2244,x2245,x2246)
% 59.51/59.58 [225]~P7(x2251,x2252,x2253,x2257,x2258,x2259)+P7(x2251,x2252,x2253,x2254,x2255,x2256)+~P7(x2257,x2258,x2259,x2254,x2255,x2256)
% 59.51/59.58 [265]~P5(x2651,x2652,x2653,x2654,x2659,x26510,x26511,x26512)+P5(x2651,x2652,x2653,x2654,x2655,x2656,x2657,x2658)+~P5(x2659,x26510,x26511,x26512,x2655,x2656,x2657,x2658)
% 59.51/59.58 [266]~P8(x2661,x2662,x2663,x2664,x2669,x26610,x26611,x26612)+P8(x2661,x2662,x2663,x2664,x2665,x2666,x2667,x2668)+~P8(x2669,x26610,x26611,x26612,x2665,x2666,x2667,x2668)
% 59.51/59.58 [198]~P4(x1982,x1981,x1984,x1981)+~P6(x1982,x1984,x1981,x1983)+P9(x1981,x1982,x1982,x1983)+~P4(x1982,x1983,x1984,x1983)
% 59.51/59.58 [165]~P1(x1651,x1652,x1653)+~P10(x1654,x1651,x1655,x1653)+P3(x1651,x1652,x1653)+~P3(x1654,x1652,x1655)
% 59.51/59.58 [178]~P10(x1784,x1783,x1785,x1782)+~P10(x1784,x1782,x1785,x1783)+P3(x1781,x1782,x1783)+~P3(x1781,x1784,x1785)
% 59.51/59.58 [199]~P4(x1995,x1991,x1995,x1993)+~P4(x1995,x1991,x1995,x1992)+P6(x1991,x1992,x1993,x1994)+~P4(x1995,x1991,x1995,x1994)
% 59.51/59.58 [231]~P1(x2311,x2314,x2315)+~P1(x2311,x2312,x2313)+~P10(x2312,x2314,x2313,x2315)+P8(x2311,x2312,x2312,x2313,x2311,x2314,x2314,x2315)
% 59.51/59.58 [242]~P1(x2421,x2422,x2423)+~P5(x2425,x2422,x2425,x2423,x2424,x2422,x2424,x2421)+P3(x2421,x2422,x2423)+~P2(x2424,x2425,x2422,x2423)
% 59.51/59.58 [189]~P9(x1893,x1891,x1893,x1895)+~P9(x1891,x1892,x1891,x1893)+~P3(x1894,x1892,x1895)+P3(f6(x1891,x1892,x1893),x1891,x1893)
% 59.51/59.58 [195]~P6(x1951,x1952,x1953,x1955)+~P10(x1951,x1952,x1953,x1955)+~P3(x1954,x1951,x1952)+P2(f9(x1951,x1952,x1953),x1951,x1952,x1953)
% 59.51/59.58 [264]~P5(x2641,x2643,x2642,x2643,x2644,x2646,x2645,x2646)+~P5(x2641,x2642,x2642,x2643,x2644,x2645,x2645,x2646)+P1(x2641,x2642,x2643)+P11(x2641,x2642,x2643,x2644,x2645,x2646)
% 59.51/59.58 [254]~P6(x2541,x2542,x2545,x2544)+~P6(x2541,x2542,x2545,x2543)+~P5(x2545,x2541,x2545,x2542,x2546,x2543,x2546,x2544)+P4(x2541,x2542,x2543,x2544)+~P6(x2541,x2542,x2545,x2546)
% 59.51/59.58 [209]~P1(x2092,x2093,x2094)+~P1(x2091,x2094,x2096)+~P1(x2091,x2093,x2095)+~P10(x2093,x2094,x2095,x2096)+P1(x2091,x2092,f13(x2093,x2094,x2095,x2096,x2091,x2092))
% 59.51/59.59 [210]~P1(x2106,x2101,x2102)+~P1(x2105,x2102,x2104)+~P1(x2105,x2101,x2103)+~P10(x2101,x2102,x2103,x2104)+P1(f13(x2101,x2102,x2103,x2104,x2105,x2106),x2103,x2104)
% 59.51/59.59 [211]~P1(x2113,x2114,x2115)+~P3(x2116,x2111,x2112)+~P10(x2111,x2113,x2115,x2116)+~P10(x2111,x2113,x2112,x2114)+P1(f32(x2111,x2112,x2113,x2114,x2115,x2116),x2116,x2115)
% 59.51/59.59 [212]~P1(x2123,x2124,x2125)+~P3(x2126,x2121,x2122)+~P10(x2121,x2123,x2125,x2126)+~P10(x2121,x2123,x2122,x2124)+P1(f32(x2121,x2122,x2123,x2124,x2125,x2126),x2121,x2124)
% 59.51/59.59 [213]~P4(x2132,x2133,x2132,x2134)+~P4(x2131,x2133,x2131,x2136)+~P2(x2131,x2133,x2134,x2135)+E(x2131,x2132)+P1(f10(x2133,x2134,x2135,x2136,x2131,x2132),x2133,x2135)
% 59.51/59.59 [214]~P4(x2142,x2143,x2142,x2144)+~P4(x2141,x2143,x2141,x2146)+~P2(x2141,x2143,x2144,x2145)+E(x2141,x2142)+P1(f11(x2143,x2144,x2145,x2146,x2141,x2142),x2144,x2146)
% 59.51/59.59 [215]~P4(x2152,x2153,x2152,x2154)+~P4(x2151,x2153,x2151,x2156)+~P2(x2151,x2153,x2154,x2155)+E(x2151,x2152)+P4(f10(x2153,x2154,x2155,x2156,x2151,x2152),x2152,x2152,x2153)
% 59.51/59.59 [216]~P4(x2162,x2163,x2162,x2164)+~P4(x2161,x2163,x2161,x2166)+~P2(x2161,x2163,x2164,x2165)+E(x2161,x2162)+P4(f11(x2163,x2164,x2165,x2166,x2161,x2162),x2162,x2162,x2163)
% 59.51/59.59 [162]~P1(x1623,x1621,x1624)+~P1(x1625,x1621,x1624)+~P3(x1626,x1625,x1623)+~P3(x1627,x1621,x1624)+P3(f26(x1621,x1622),x1621,x1622)
% 59.51/59.59 %EqnAxiom
% 59.51/59.59 [1]E(x11,x11)
% 59.51/59.59 [2]E(x22,x21)+~E(x21,x22)
% 59.51/59.59 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 59.51/59.59 [4]~E(x41,x42)+E(f26(x41,x43),f26(x42,x43))
% 59.51/59.59 [5]~E(x51,x52)+E(f26(x53,x51),f26(x53,x52))
% 59.51/59.59 [6]~E(x61,x62)+E(f3(x61,x63,x64),f3(x62,x63,x64))
% 59.51/59.59 [7]~E(x71,x72)+E(f3(x73,x71,x74),f3(x73,x72,x74))
% 59.51/59.59 [8]~E(x81,x82)+E(f3(x83,x84,x81),f3(x83,x84,x82))
% 59.51/59.59 [9]~E(x91,x92)+E(f4(x91,x93,x94),f4(x92,x93,x94))
% 59.51/59.59 [10]~E(x101,x102)+E(f4(x103,x101,x104),f4(x103,x102,x104))
% 59.51/59.59 [11]~E(x111,x112)+E(f4(x113,x114,x111),f4(x113,x114,x112))
% 59.51/59.59 [12]~E(x121,x122)+E(f5(x121,x123,x124),f5(x122,x123,x124))
% 59.51/59.59 [13]~E(x131,x132)+E(f5(x133,x131,x134),f5(x133,x132,x134))
% 59.51/59.59 [14]~E(x141,x142)+E(f5(x143,x144,x141),f5(x143,x144,x142))
% 59.51/59.59 [15]~E(x151,x152)+E(f6(x151,x153,x154),f6(x152,x153,x154))
% 59.51/59.59 [16]~E(x161,x162)+E(f6(x163,x161,x164),f6(x163,x162,x164))
% 59.51/59.59 [17]~E(x171,x172)+E(f6(x173,x174,x171),f6(x173,x174,x172))
% 59.51/59.59 [18]~E(x181,x182)+E(f7(x181,x183,x184,x185),f7(x182,x183,x184,x185))
% 59.51/59.59 [19]~E(x191,x192)+E(f7(x193,x191,x194,x195),f7(x193,x192,x194,x195))
% 59.51/59.59 [20]~E(x201,x202)+E(f7(x203,x204,x201,x205),f7(x203,x204,x202,x205))
% 59.51/59.59 [21]~E(x211,x212)+E(f7(x213,x214,x215,x211),f7(x213,x214,x215,x212))
% 59.51/59.59 [22]~E(x221,x222)+E(f30(x221,x223,x224,x225),f30(x222,x223,x224,x225))
% 59.51/59.59 [23]~E(x231,x232)+E(f30(x233,x231,x234,x235),f30(x233,x232,x234,x235))
% 59.51/59.59 [24]~E(x241,x242)+E(f30(x243,x244,x241,x245),f30(x243,x244,x242,x245))
% 59.51/59.59 [25]~E(x251,x252)+E(f30(x253,x254,x255,x251),f30(x253,x254,x255,x252))
% 59.51/59.59 [26]~E(x261,x262)+E(f24(x261,x263,x264,x265),f24(x262,x263,x264,x265))
% 59.51/59.59 [27]~E(x271,x272)+E(f24(x273,x271,x274,x275),f24(x273,x272,x274,x275))
% 59.51/59.59 [28]~E(x281,x282)+E(f24(x283,x284,x281,x285),f24(x283,x284,x282,x285))
% 59.51/59.59 [29]~E(x291,x292)+E(f24(x293,x294,x295,x291),f24(x293,x294,x295,x292))
% 59.51/59.59 [30]~E(x301,x302)+E(f28(x301,x303,x304,x305),f28(x302,x303,x304,x305))
% 59.51/59.59 [31]~E(x311,x312)+E(f28(x313,x311,x314,x315),f28(x313,x312,x314,x315))
% 59.51/59.59 [32]~E(x321,x322)+E(f28(x323,x324,x321,x325),f28(x323,x324,x322,x325))
% 59.51/59.59 [33]~E(x331,x332)+E(f28(x333,x334,x335,x331),f28(x333,x334,x335,x332))
% 59.51/59.59 [34]~E(x341,x342)+E(f8(x341,x343,x344),f8(x342,x343,x344))
% 59.51/59.59 [35]~E(x351,x352)+E(f8(x353,x351,x354),f8(x353,x352,x354))
% 59.51/59.59 [36]~E(x361,x362)+E(f8(x363,x364,x361),f8(x363,x364,x362))
% 59.51/59.59 [37]~E(x371,x372)+E(f9(x371,x373,x374),f9(x372,x373,x374))
% 59.51/59.59 [38]~E(x381,x382)+E(f9(x383,x381,x384),f9(x383,x382,x384))
% 59.51/59.59 [39]~E(x391,x392)+E(f9(x393,x394,x391),f9(x393,x394,x392))
% 59.51/59.59 [40]~E(x401,x402)+E(f27(x401,x403,x404,x405),f27(x402,x403,x404,x405))
% 59.51/59.59 [41]~E(x411,x412)+E(f27(x413,x411,x414,x415),f27(x413,x412,x414,x415))
% 59.51/59.59 [42]~E(x421,x422)+E(f27(x423,x424,x421,x425),f27(x423,x424,x422,x425))
% 59.51/59.59 [43]~E(x431,x432)+E(f27(x433,x434,x435,x431),f27(x433,x434,x435,x432))
% 59.51/59.59 [44]~E(x441,x442)+E(f14(x441,x443,x444,x445),f14(x442,x443,x444,x445))
% 59.51/59.59 [45]~E(x451,x452)+E(f14(x453,x451,x454,x455),f14(x453,x452,x454,x455))
% 59.51/59.59 [46]~E(x461,x462)+E(f14(x463,x464,x461,x465),f14(x463,x464,x462,x465))
% 59.51/59.59 [47]~E(x471,x472)+E(f14(x473,x474,x475,x471),f14(x473,x474,x475,x472))
% 59.51/59.59 [48]~E(x481,x482)+E(f12(x481,x483,x484,x485,x486),f12(x482,x483,x484,x485,x486))
% 59.51/59.59 [49]~E(x491,x492)+E(f12(x493,x491,x494,x495,x496),f12(x493,x492,x494,x495,x496))
% 59.51/59.59 [50]~E(x501,x502)+E(f12(x503,x504,x501,x505,x506),f12(x503,x504,x502,x505,x506))
% 59.51/59.59 [51]~E(x511,x512)+E(f12(x513,x514,x515,x511,x516),f12(x513,x514,x515,x512,x516))
% 59.51/59.59 [52]~E(x521,x522)+E(f12(x523,x524,x525,x526,x521),f12(x523,x524,x525,x526,x522))
% 59.51/59.59 [53]~E(x531,x532)+E(f11(x531,x533,x534,x535,x536,x537),f11(x532,x533,x534,x535,x536,x537))
% 59.51/59.59 [54]~E(x541,x542)+E(f11(x543,x541,x544,x545,x546,x547),f11(x543,x542,x544,x545,x546,x547))
% 59.51/59.59 [55]~E(x551,x552)+E(f11(x553,x554,x551,x555,x556,x557),f11(x553,x554,x552,x555,x556,x557))
% 59.51/59.59 [56]~E(x561,x562)+E(f11(x563,x564,x565,x561,x566,x567),f11(x563,x564,x565,x562,x566,x567))
% 59.51/59.59 [57]~E(x571,x572)+E(f11(x573,x574,x575,x576,x571,x577),f11(x573,x574,x575,x576,x572,x577))
% 59.51/59.59 [58]~E(x581,x582)+E(f11(x583,x584,x585,x586,x587,x581),f11(x583,x584,x585,x586,x587,x582))
% 59.51/59.59 [59]~E(x591,x592)+E(f31(x591,x593,x594,x595,x596),f31(x592,x593,x594,x595,x596))
% 59.51/59.59 [60]~E(x601,x602)+E(f31(x603,x601,x604,x605,x606),f31(x603,x602,x604,x605,x606))
% 59.51/59.59 [61]~E(x611,x612)+E(f31(x613,x614,x611,x615,x616),f31(x613,x614,x612,x615,x616))
% 59.51/59.59 [62]~E(x621,x622)+E(f31(x623,x624,x625,x621,x626),f31(x623,x624,x625,x622,x626))
% 59.51/59.59 [63]~E(x631,x632)+E(f31(x633,x634,x635,x636,x631),f31(x633,x634,x635,x636,x632))
% 59.51/59.59 [64]~E(x641,x642)+E(f10(x641,x643,x644,x645,x646,x647),f10(x642,x643,x644,x645,x646,x647))
% 59.51/59.59 [65]~E(x651,x652)+E(f10(x653,x651,x654,x655,x656,x657),f10(x653,x652,x654,x655,x656,x657))
% 59.51/59.59 [66]~E(x661,x662)+E(f10(x663,x664,x661,x665,x666,x667),f10(x663,x664,x662,x665,x666,x667))
% 59.51/59.59 [67]~E(x671,x672)+E(f10(x673,x674,x675,x671,x676,x677),f10(x673,x674,x675,x672,x676,x677))
% 59.51/59.59 [68]~E(x681,x682)+E(f10(x683,x684,x685,x686,x681,x687),f10(x683,x684,x685,x686,x682,x687))
% 59.51/59.59 [69]~E(x691,x692)+E(f10(x693,x694,x695,x696,x697,x691),f10(x693,x694,x695,x696,x697,x692))
% 59.51/59.59 [70]~E(x701,x702)+E(f32(x701,x703,x704,x705,x706,x707),f32(x702,x703,x704,x705,x706,x707))
% 59.51/59.59 [71]~E(x711,x712)+E(f32(x713,x711,x714,x715,x716,x717),f32(x713,x712,x714,x715,x716,x717))
% 59.51/59.59 [72]~E(x721,x722)+E(f32(x723,x724,x721,x725,x726,x727),f32(x723,x724,x722,x725,x726,x727))
% 59.51/59.59 [73]~E(x731,x732)+E(f32(x733,x734,x735,x731,x736,x737),f32(x733,x734,x735,x732,x736,x737))
% 59.51/59.59 [74]~E(x741,x742)+E(f32(x743,x744,x745,x746,x741,x747),f32(x743,x744,x745,x746,x742,x747))
% 59.51/59.59 [75]~E(x751,x752)+E(f32(x753,x754,x755,x756,x757,x751),f32(x753,x754,x755,x756,x757,x752))
% 59.51/59.59 [76]~E(x761,x762)+E(f29(x761,x763,x764,x765,x766,x767),f29(x762,x763,x764,x765,x766,x767))
% 59.51/59.59 [77]~E(x771,x772)+E(f29(x773,x771,x774,x775,x776,x777),f29(x773,x772,x774,x775,x776,x777))
% 59.51/59.59 [78]~E(x781,x782)+E(f29(x783,x784,x781,x785,x786,x787),f29(x783,x784,x782,x785,x786,x787))
% 59.51/59.59 [79]~E(x791,x792)+E(f29(x793,x794,x795,x791,x796,x797),f29(x793,x794,x795,x792,x796,x797))
% 59.51/59.59 [80]~E(x801,x802)+E(f29(x803,x804,x805,x806,x801,x807),f29(x803,x804,x805,x806,x802,x807))
% 59.51/59.59 [81]~E(x811,x812)+E(f29(x813,x814,x815,x816,x817,x811),f29(x813,x814,x815,x816,x817,x812))
% 59.51/59.59 [82]~E(x821,x822)+E(f13(x821,x823,x824,x825,x826,x827),f13(x822,x823,x824,x825,x826,x827))
% 59.51/59.59 [83]~E(x831,x832)+E(f13(x833,x831,x834,x835,x836,x837),f13(x833,x832,x834,x835,x836,x837))
% 59.51/59.59 [84]~E(x841,x842)+E(f13(x843,x844,x841,x845,x846,x847),f13(x843,x844,x842,x845,x846,x847))
% 59.51/59.59 [85]~E(x851,x852)+E(f13(x853,x854,x855,x851,x856,x857),f13(x853,x854,x855,x852,x856,x857))
% 59.51/59.59 [86]~E(x861,x862)+E(f13(x863,x864,x865,x866,x861,x867),f13(x863,x864,x865,x866,x862,x867))
% 59.51/59.59 [87]~E(x871,x872)+E(f13(x873,x874,x875,x876,x877,x871),f13(x873,x874,x875,x876,x877,x872))
% 59.51/59.59 [88]P1(x882,x883,x884)+~E(x881,x882)+~P1(x881,x883,x884)
% 59.51/59.59 [89]P1(x893,x892,x894)+~E(x891,x892)+~P1(x893,x891,x894)
% 59.51/59.59 [90]P1(x903,x904,x902)+~E(x901,x902)+~P1(x903,x904,x901)
% 59.51/59.59 [91]P8(x912,x913,x914,x915,x916,x917,x918,x919)+~E(x911,x912)+~P8(x911,x913,x914,x915,x916,x917,x918,x919)
% 59.51/59.59 [92]P8(x923,x922,x924,x925,x926,x927,x928,x929)+~E(x921,x922)+~P8(x923,x921,x924,x925,x926,x927,x928,x929)
% 59.51/59.59 [93]P8(x933,x934,x932,x935,x936,x937,x938,x939)+~E(x931,x932)+~P8(x933,x934,x931,x935,x936,x937,x938,x939)
% 59.51/59.59 [94]P8(x943,x944,x945,x942,x946,x947,x948,x949)+~E(x941,x942)+~P8(x943,x944,x945,x941,x946,x947,x948,x949)
% 59.51/59.59 [95]P8(x953,x954,x955,x956,x952,x957,x958,x959)+~E(x951,x952)+~P8(x953,x954,x955,x956,x951,x957,x958,x959)
% 59.51/59.59 [96]P8(x963,x964,x965,x966,x967,x962,x968,x969)+~E(x961,x962)+~P8(x963,x964,x965,x966,x967,x961,x968,x969)
% 59.51/59.59 [97]P8(x973,x974,x975,x976,x977,x978,x972,x979)+~E(x971,x972)+~P8(x973,x974,x975,x976,x977,x978,x971,x979)
% 59.51/59.59 [98]P8(x983,x984,x985,x986,x987,x988,x989,x982)+~E(x981,x982)+~P8(x983,x984,x985,x986,x987,x988,x989,x981)
% 59.51/59.59 [99]P6(x992,x993,x994,x995)+~E(x991,x992)+~P6(x991,x993,x994,x995)
% 59.51/59.59 [100]P6(x1003,x1002,x1004,x1005)+~E(x1001,x1002)+~P6(x1003,x1001,x1004,x1005)
% 59.51/59.59 [101]P6(x1013,x1014,x1012,x1015)+~E(x1011,x1012)+~P6(x1013,x1014,x1011,x1015)
% 59.51/59.59 [102]P6(x1023,x1024,x1025,x1022)+~E(x1021,x1022)+~P6(x1023,x1024,x1025,x1021)
% 59.51/59.59 [103]P4(x1032,x1033,x1034,x1035)+~E(x1031,x1032)+~P4(x1031,x1033,x1034,x1035)
% 59.51/59.59 [104]P4(x1043,x1042,x1044,x1045)+~E(x1041,x1042)+~P4(x1043,x1041,x1044,x1045)
% 59.51/59.59 [105]P4(x1053,x1054,x1052,x1055)+~E(x1051,x1052)+~P4(x1053,x1054,x1051,x1055)
% 59.51/59.59 [106]P4(x1063,x1064,x1065,x1062)+~E(x1061,x1062)+~P4(x1063,x1064,x1065,x1061)
% 59.51/59.59 [107]P3(x1072,x1073,x1074)+~E(x1071,x1072)+~P3(x1071,x1073,x1074)
% 59.51/59.59 [108]P3(x1083,x1082,x1084)+~E(x1081,x1082)+~P3(x1083,x1081,x1084)
% 59.51/59.59 [109]P3(x1093,x1094,x1092)+~E(x1091,x1092)+~P3(x1093,x1094,x1091)
% 59.51/59.59 [110]P9(x1102,x1103,x1104,x1105)+~E(x1101,x1102)+~P9(x1101,x1103,x1104,x1105)
% 59.51/59.59 [111]P9(x1113,x1112,x1114,x1115)+~E(x1111,x1112)+~P9(x1113,x1111,x1114,x1115)
% 59.51/59.59 [112]P9(x1123,x1124,x1122,x1125)+~E(x1121,x1122)+~P9(x1123,x1124,x1121,x1125)
% 59.51/59.59 [113]P9(x1133,x1134,x1135,x1132)+~E(x1131,x1132)+~P9(x1133,x1134,x1135,x1131)
% 59.51/59.59 [114]P11(x1142,x1143,x1144,x1145,x1146,x1147)+~E(x1141,x1142)+~P11(x1141,x1143,x1144,x1145,x1146,x1147)
% 59.51/59.59 [115]P11(x1153,x1152,x1154,x1155,x1156,x1157)+~E(x1151,x1152)+~P11(x1153,x1151,x1154,x1155,x1156,x1157)
% 59.51/59.59 [116]P11(x1163,x1164,x1162,x1165,x1166,x1167)+~E(x1161,x1162)+~P11(x1163,x1164,x1161,x1165,x1166,x1167)
% 59.51/59.59 [117]P11(x1173,x1174,x1175,x1172,x1176,x1177)+~E(x1171,x1172)+~P11(x1173,x1174,x1175,x1171,x1176,x1177)
% 59.51/59.59 [118]P11(x1183,x1184,x1185,x1186,x1182,x1187)+~E(x1181,x1182)+~P11(x1183,x1184,x1185,x1186,x1181,x1187)
% 59.51/59.59 [119]P11(x1193,x1194,x1195,x1196,x1197,x1192)+~E(x1191,x1192)+~P11(x1193,x1194,x1195,x1196,x1197,x1191)
% 59.51/59.59 [120]P2(x1202,x1203,x1204,x1205)+~E(x1201,x1202)+~P2(x1201,x1203,x1204,x1205)
% 59.51/59.59 [121]P2(x1213,x1212,x1214,x1215)+~E(x1211,x1212)+~P2(x1213,x1211,x1214,x1215)
% 59.51/59.59 [122]P2(x1223,x1224,x1222,x1225)+~E(x1221,x1222)+~P2(x1223,x1224,x1221,x1225)
% 59.51/59.59 [123]P2(x1233,x1234,x1235,x1232)+~E(x1231,x1232)+~P2(x1233,x1234,x1235,x1231)
% 59.51/59.59 [124]P10(x1242,x1243,x1244,x1245)+~E(x1241,x1242)+~P10(x1241,x1243,x1244,x1245)
% 59.51/59.59 [125]P10(x1253,x1252,x1254,x1255)+~E(x1251,x1252)+~P10(x1253,x1251,x1254,x1255)
% 59.51/59.59 [126]P10(x1263,x1264,x1262,x1265)+~E(x1261,x1262)+~P10(x1263,x1264,x1261,x1265)
% 59.51/59.59 [127]P10(x1273,x1274,x1275,x1272)+~E(x1271,x1272)+~P10(x1273,x1274,x1275,x1271)
% 59.51/59.59 [128]P7(x1282,x1283,x1284,x1285,x1286,x1287)+~E(x1281,x1282)+~P7(x1281,x1283,x1284,x1285,x1286,x1287)
% 59.51/59.59 [129]P7(x1293,x1292,x1294,x1295,x1296,x1297)+~E(x1291,x1292)+~P7(x1293,x1291,x1294,x1295,x1296,x1297)
% 59.51/59.59 [130]P7(x1303,x1304,x1302,x1305,x1306,x1307)+~E(x1301,x1302)+~P7(x1303,x1304,x1301,x1305,x1306,x1307)
% 59.51/59.59 [131]P7(x1313,x1314,x1315,x1312,x1316,x1317)+~E(x1311,x1312)+~P7(x1313,x1314,x1315,x1311,x1316,x1317)
% 59.51/59.59 [132]P7(x1323,x1324,x1325,x1326,x1322,x1327)+~E(x1321,x1322)+~P7(x1323,x1324,x1325,x1326,x1321,x1327)
% 59.51/59.59 [133]P7(x1333,x1334,x1335,x1336,x1337,x1332)+~E(x1331,x1332)+~P7(x1333,x1334,x1335,x1336,x1337,x1331)
% 59.51/59.59 [134]P5(x1342,x1343,x1344,x1345,x1346,x1347,x1348,x1349)+~E(x1341,x1342)+~P5(x1341,x1343,x1344,x1345,x1346,x1347,x1348,x1349)
% 59.51/59.59 [135]P5(x1353,x1352,x1354,x1355,x1356,x1357,x1358,x1359)+~E(x1351,x1352)+~P5(x1353,x1351,x1354,x1355,x1356,x1357,x1358,x1359)
% 59.51/59.59 [136]P5(x1363,x1364,x1362,x1365,x1366,x1367,x1368,x1369)+~E(x1361,x1362)+~P5(x1363,x1364,x1361,x1365,x1366,x1367,x1368,x1369)
% 59.51/59.59 [137]P5(x1373,x1374,x1375,x1372,x1376,x1377,x1378,x1379)+~E(x1371,x1372)+~P5(x1373,x1374,x1375,x1371,x1376,x1377,x1378,x1379)
% 59.51/59.59 [138]P5(x1383,x1384,x1385,x1386,x1382,x1387,x1388,x1389)+~E(x1381,x1382)+~P5(x1383,x1384,x1385,x1386,x1381,x1387,x1388,x1389)
% 59.51/59.59 [139]P5(x1393,x1394,x1395,x1396,x1397,x1392,x1398,x1399)+~E(x1391,x1392)+~P5(x1393,x1394,x1395,x1396,x1397,x1391,x1398,x1399)
% 59.51/59.59 [140]P5(x1403,x1404,x1405,x1406,x1407,x1408,x1402,x1409)+~E(x1401,x1402)+~P5(x1403,x1404,x1405,x1406,x1407,x1408,x1401,x1409)
% 59.51/59.59 [141]P5(x1413,x1414,x1415,x1416,x1417,x1418,x1419,x1412)+~E(x1411,x1412)+~P5(x1413,x1414,x1415,x1416,x1417,x1418,x1419,x1411)
% 59.51/59.59
% 59.51/59.59 %-------------------------------------------
% 59.51/59.59 cnf(267,plain,
% 59.51/59.59 (~P3(a1,a18,a20)),
% 59.51/59.59 inference(scs_inference,[],[153,159])).
% 59.51/59.59 cnf(269,plain,
% 59.51/59.59 (~P4(a1,a20,a1,a18)),
% 59.51/59.59 inference(scs_inference,[],[153,159,170])).
% 59.51/59.59 cnf(271,plain,
% 59.51/59.59 (~P4(a1,a18,a20,a1)),
% 59.51/59.59 inference(scs_inference,[],[153,159,170,171])).
% 59.51/59.59 cnf(275,plain,
% 59.51/59.59 (~P7(a1,a20,x2751,a1,a18,x2752)),
% 59.51/59.59 inference(scs_inference,[],[153,159,170,171,205,220])).
% 59.51/59.59 cnf(277,plain,
% 59.51/59.59 (~P7(a18,a1,x2771,a20,a1,x2772)),
% 59.51/59.59 inference(scs_inference,[],[153,159,170,171,205,220,221])).
% 59.51/59.59 cnf(279,plain,
% 59.51/59.59 (~P7(a1,x2791,a18,a1,x2792,a20)),
% 59.51/59.59 inference(scs_inference,[],[153,159,170,171,205,220,221,222])).
% 59.51/59.59 cnf(281,plain,
% 59.51/59.59 (P1(a15,a15,a1)),
% 59.51/59.59 inference(scs_inference,[],[142,153,159,170,171,205,220,221,222,158])).
% 59.51/59.59 cnf(283,plain,
% 59.51/59.59 (P10(a1,a1,a17,a17)),
% 59.51/59.59 inference(scs_inference,[],[142,146,153,159,170,171,205,220,221,222,158,160])).
% 59.51/59.59 cnf(285,plain,
% 59.51/59.59 (P10(a19,a19,a17,a17)),
% 59.51/59.59 inference(scs_inference,[],[142,146,153,159,170,171,205,220,221,222,158,160,161])).
% 59.51/59.59 cnf(291,plain,
% 59.51/59.59 (~P8(a2,a16,a15,a16,a1,a18,a1,a20)),
% 59.51/59.59 inference(scs_inference,[],[142,146,148,153,159,170,171,205,220,221,222,158,160,161,246,157,259])).
% 59.51/59.59 cnf(293,plain,
% 59.51/59.59 (~P8(a1,a20,a1,a18,a15,a16,a2,a16)),
% 59.51/59.59 inference(scs_inference,[],[142,146,148,153,159,170,171,205,220,221,222,158,160,161,246,157,259,260])).
% 59.51/59.59 cnf(295,plain,
% 59.51/59.59 (~P8(a18,a1,a1,a20,a2,a16,a15,a16)),
% 59.51/59.59 inference(scs_inference,[],[142,146,148,153,159,170,171,205,220,221,222,158,160,161,246,157,259,260,261])).
% 59.51/59.59 cnf(297,plain,
% 59.51/59.59 (~P8(a1,a18,a2,a16,a1,a20,a15,a16)),
% 59.51/59.59 inference(scs_inference,[],[142,146,148,153,159,170,171,205,220,221,222,158,160,161,246,157,259,260,261,262])).
% 59.51/59.59 cnf(299,plain,
% 59.51/59.59 (~P3(x2991,a18,a20)+~P9(a1,x2991,a18,a20)),
% 59.51/59.59 inference(scs_inference,[],[142,146,148,153,159,170,171,205,220,221,222,158,160,161,246,157,259,260,261,262,176])).
% 59.51/59.59 cnf(303,plain,
% 59.51/59.59 (~P9(x3031,x3032,a16,a2)+P10(x3031,x3032,a16,a15)),
% 59.51/59.59 inference(scs_inference,[],[142,146,147,148,153,159,170,171,205,220,221,222,158,160,161,246,157,259,260,261,262,176,177,183])).
% 59.51/59.59 cnf(308,plain,
% 59.51/59.59 (~P4(a1,a20,a18,a1)),
% 59.51/59.59 inference(scs_inference,[],[269,171])).
% 59.51/59.59 cnf(310,plain,
% 59.51/59.59 (~P7(a20,a1,x3101,a18,a1,x3102)),
% 59.51/59.59 inference(scs_inference,[],[269,277,171,220])).
% 59.51/59.59 cnf(312,plain,
% 59.51/59.59 (~P7(a1,a18,x3121,a20,a1,x3122)),
% 59.51/59.59 inference(scs_inference,[],[269,271,277,171,220,205])).
% 59.51/59.59 cnf(314,plain,
% 59.51/59.59 (~P8(a16,a2,a15,a16,a1,a18,a1,a20)),
% 59.51/59.59 inference(scs_inference,[],[269,271,277,291,171,220,205,261])).
% 59.51/59.59 cnf(316,plain,
% 59.51/59.59 (~P7(a1,x3161,a20,a1,x3162,a18)),
% 59.51/59.59 inference(scs_inference,[],[269,271,275,277,291,171,220,205,261,222])).
% 59.51/59.59 cnf(318,plain,
% 59.51/59.59 (~P8(a15,a16,a2,a16,a1,a20,a1,a18)),
% 59.51/59.59 inference(scs_inference,[],[269,271,275,277,291,293,171,220,205,261,222,259])).
% 59.51/59.59 cnf(320,plain,
% 59.51/59.59 (~P4(a20,a1,a1,a18)),
% 59.51/59.59 inference(scs_inference,[],[269,271,275,277,291,293,171,220,205,261,222,259,170])).
% 59.51/59.59 cnf(322,plain,
% 59.51/59.59 (~P7(x3221,a1,a18,x3222,a1,a20)),
% 59.51/59.59 inference(scs_inference,[],[269,271,275,277,279,291,293,171,220,205,261,222,259,170,221])).
% 59.51/59.59 cnf(324,plain,
% 59.51/59.59 (~P8(a1,a20,a18,a1,a15,a16,a2,a16)),
% 59.51/59.59 inference(scs_inference,[],[269,271,275,277,279,291,293,295,171,220,205,261,222,259,170,221,260])).
% 59.51/59.59 cnf(326,plain,
% 59.51/59.59 (~P8(a2,a16,a1,a18,a15,a16,a1,a20)),
% 59.51/59.59 inference(scs_inference,[],[269,271,275,277,279,291,293,295,171,220,205,261,222,259,170,221,260,262])).
% 59.51/59.59 cnf(328,plain,
% 59.51/59.59 (~P8(a1,a20,a1,a18,a2,a16,a15,a16)),
% 59.51/59.59 inference(scs_inference,[],[148,269,271,275,277,279,291,293,295,171,220,205,261,222,259,170,221,260,262,246])).
% 59.51/59.59 cnf(330,plain,
% 59.51/59.59 (P1(a15,a15,a17)),
% 59.51/59.59 inference(scs_inference,[],[143,148,269,271,275,277,279,291,293,295,171,220,205,261,222,259,170,221,260,262,246,158])).
% 59.51/59.59 cnf(344,plain,
% 59.51/59.59 (~P7(a1,a20,x3441,a18,a1,x3442)),
% 59.51/59.59 inference(scs_inference,[],[308,205])).
% 59.51/59.59 cnf(346,plain,
% 59.51/59.59 (~P4(a20,a1,a18,a1)),
% 59.51/59.59 inference(scs_inference,[],[308,320,205,171])).
% 59.51/59.59 cnf(348,plain,
% 59.51/59.59 (~P8(a20,a1,a1,a18,a2,a16,a15,a16)),
% 59.51/59.59 inference(scs_inference,[],[308,320,328,205,171,261])).
% 59.51/59.59 cnf(350,plain,
% 59.51/59.59 (~P7(a20,x3501,a1,a18,x3502,a1)),
% 59.51/59.59 inference(scs_inference,[],[308,320,328,310,205,171,261,222])).
% 59.51/59.59 cnf(352,plain,
% 59.51/59.59 (~P7(a20,a1,x3521,a1,a18,x3522)),
% 59.51/59.59 inference(scs_inference,[],[308,320,328,310,312,205,171,261,222,220])).
% 59.51/59.59 cnf(354,plain,
% 59.51/59.59 (~P4(a18,a1,a1,a20)),
% 59.51/59.59 inference(scs_inference,[],[308,320,328,310,312,205,171,261,222,220,170])).
% 59.51/59.59 cnf(356,plain,
% 59.51/59.59 (~P7(a18,a1,x3561,a1,a20,x3562)),
% 59.51/59.59 inference(scs_inference,[],[308,320,328,310,312,205,171,261,222,220,170,221])).
% 59.51/59.59 cnf(358,plain,
% 59.51/59.59 (~P8(a1,a20,a2,a16,a1,a18,a15,a16)),
% 59.51/59.59 inference(scs_inference,[],[308,320,328,310,312,205,171,261,222,220,170,221,262])).
% 59.51/59.59 cnf(360,plain,
% 59.51/59.59 (~P8(a2,a16,a15,a16,a1,a20,a1,a18)),
% 59.51/59.59 inference(scs_inference,[],[308,320,328,310,312,205,171,261,222,220,170,221,262,259])).
% 59.51/59.59 cnf(362,plain,
% 59.51/59.59 (~P8(a1,a18,a1,a20,a15,a16,a2,a16)),
% 59.51/59.59 inference(scs_inference,[],[308,320,328,310,312,205,171,261,222,220,170,221,262,259,260])).
% 59.51/59.59 cnf(364,plain,
% 59.51/59.59 (~P8(a1,a20,a18,a1,a2,a16,a15,a16)),
% 59.51/59.59 inference(scs_inference,[],[148,308,320,328,310,312,205,171,261,222,220,170,221,262,259,260,246])).
% 59.51/59.59 cnf(366,plain,
% 59.51/59.59 (P1(a17,a17,a18)),
% 59.51/59.59 inference(scs_inference,[],[144,148,308,320,328,310,312,205,171,261,222,220,170,221,262,259,260,246,158])).
% 59.51/59.59 cnf(373,plain,
% 59.51/59.59 (~P10(x3731,x3732,a1,a1)+P10(x3731,x3732,a17,a17)+~E(a17,x3733)),
% 59.51/59.59 inference(scs_inference,[],[146,144,147,148,283,308,320,328,310,312,205,171,261,222,220,170,221,262,259,260,246,158,109,161,160,182])).
% 59.51/59.59 cnf(377,plain,
% 59.51/59.59 (P10(x3771,x3772,a17,a17)+~P10(x3771,x3772,a1,a1)),
% 59.51/59.59 inference(equality_inference,[],[373])).
% 59.51/59.59 cnf(378,plain,
% 59.51/59.59 (~P8(a20,a1,a18,a1,a2,a16,a15,a16)),
% 59.51/59.59 inference(scs_inference,[],[364,261])).
% 59.51/59.59 cnf(380,plain,
% 59.51/59.59 (~P4(a18,a1,a20,a1)),
% 59.51/59.59 inference(scs_inference,[],[354,364,261,171])).
% 59.51/59.59 cnf(382,plain,
% 59.51/59.59 (~P7(x3821,a18,a1,x3822,a20,a1)),
% 59.51/59.59 inference(scs_inference,[],[354,364,322,261,171,222])).
% 59.51/59.59 cnf(384,plain,
% 59.51/59.59 (~P7(x3841,a1,a20,x3842,a1,a18)),
% 59.51/59.59 inference(scs_inference,[],[354,364,322,261,171,222,220])).
% 59.51/59.59 cnf(386,plain,
% 59.51/59.59 (~P7(x3861,a20,a1,x3862,a18,a1)),
% 59.51/59.59 inference(scs_inference,[],[354,364,322,350,261,171,222,220,221])).
% 59.51/59.59 cnf(390,plain,
% 59.51/59.59 (~P8(a18,a1,a1,a20,a15,a16,a2,a16)),
% 59.51/59.59 inference(scs_inference,[],[354,364,322,350,261,171,222,220,221,262,260])).
% 59.51/59.59 cnf(392,plain,
% 59.51/59.59 (~P8(a2,a16,a15,a16,a1,a20,a18,a1)),
% 59.51/59.59 inference(scs_inference,[],[354,364,322,350,261,171,222,220,221,262,260,259])).
% 59.51/59.59 cnf(394,plain,
% 59.51/59.59 (~P8(a1,a18,a20,a1,a2,a16,a15,a16)),
% 59.51/59.59 inference(scs_inference,[],[148,354,364,271,322,350,261,171,222,220,221,262,260,259,246])).
% 59.51/59.59 cnf(396,plain,
% 59.51/59.59 (P1(a1,a1,a20)),
% 59.51/59.59 inference(scs_inference,[],[145,148,354,364,271,322,350,261,171,222,220,221,262,260,259,246,158])).
% 59.51/59.59 cnf(412,plain,
% 59.51/59.59 (~P8(a18,a1,a20,a1,a2,a16,a15,a16)),
% 59.51/59.59 inference(scs_inference,[],[394,261])).
% 59.51/59.60 cnf(414,plain,
% 59.51/59.60 (~P7(a1,x4141,a20,a18,x4142,a1)),
% 59.51/59.60 inference(scs_inference,[],[394,344,261,222])).
% 59.51/59.60 cnf(416,plain,
% 59.51/59.60 (~P7(a18,x4161,a1,a20,x4162,a1)),
% 59.51/59.60 inference(scs_inference,[],[394,344,350,261,222,220])).
% 59.51/59.60 cnf(418,plain,
% 59.51/59.60 (~P7(x4181,a1,a20,x4182,a18,a1)),
% 59.51/59.60 inference(scs_inference,[],[394,344,350,261,222,220,221])).
% 59.51/59.60 cnf(420,plain,
% 59.51/59.60 (~P8(a2,a16,a15,a16,a1,a18,a20,a1)),
% 59.51/59.60 inference(scs_inference,[],[394,344,350,261,222,220,221,259])).
% 59.51/59.60 cnf(422,plain,
% 59.51/59.60 (~P8(a20,a1,a1,a18,a15,a16,a2,a16)),
% 59.51/59.60 inference(scs_inference,[],[394,344,350,261,222,220,221,259,260])).
% 59.51/59.60 cnf(426,plain,
% 59.51/59.60 (P1(a1,a1,a15)),
% 59.51/59.60 inference(scs_inference,[],[281,394,344,350,261,222,220,221,259,260,262,158])).
% 59.51/59.60 cnf(437,plain,
% 59.51/59.60 (~P7(a20,x4371,a1,a1,x4372,a18)),
% 59.51/59.60 inference(scs_inference,[],[297,352,414,261,220,222])).
% 59.51/59.60 cnf(439,plain,
% 59.51/59.60 (~P7(x4391,a18,a1,x4392,a1,a20)),
% 59.51/59.60 inference(scs_inference,[],[297,352,414,261,220,222,221])).
% 59.51/59.60 cnf(441,plain,
% 59.51/59.60 (~P8(a1,a20,a15,a16,a1,a18,a2,a16)),
% 59.51/59.60 inference(scs_inference,[],[297,352,414,261,220,222,221,259])).
% 59.51/59.60 cnf(443,plain,
% 59.51/59.60 (~P8(a20,a1,a2,a16,a1,a18,a15,a16)),
% 59.51/59.60 inference(scs_inference,[],[297,348,352,414,261,220,222,221,259,262])).
% 59.51/59.60 cnf(445,plain,
% 59.51/59.60 (~P8(a1,a18,a20,a1,a15,a16,a2,a16)),
% 59.51/59.60 inference(scs_inference,[],[297,348,352,414,261,220,222,221,259,262,260])).
% 59.51/59.60 cnf(447,plain,
% 59.51/59.60 (P1(a17,a17,a15)),
% 59.51/59.60 inference(scs_inference,[],[330,297,348,352,414,261,220,222,221,259,262,260,158])).
% 59.51/59.60 cnf(461,plain,
% 59.51/59.60 (~P8(a16,a15,a2,a16,a1,a20,a1,a18)),
% 59.51/59.60 inference(scs_inference,[],[318,261])).
% 59.51/59.60 cnf(463,plain,
% 59.51/59.60 (~P7(x4631,a20,a1,x4632,a1,a18)),
% 59.51/59.60 inference(scs_inference,[],[318,418,261,222])).
% 59.51/59.60 cnf(467,plain,
% 59.51/59.60 (~P7(x4671,a1,a18,x4672,a20,a1)),
% 59.51/59.60 inference(scs_inference,[],[318,418,437,261,222,220,221])).
% 59.51/59.60 cnf(469,plain,
% 59.51/59.60 (~P8(a2,a16,a15,a16,a20,a1,a18,a1)),
% 59.51/59.60 inference(scs_inference,[],[378,318,418,437,261,222,220,221,259])).
% 59.51/59.60 cnf(471,plain,
% 59.51/59.60 (~P8(a18,a1,a20,a1,a15,a16,a2,a16)),
% 59.51/59.60 inference(scs_inference,[],[378,318,418,437,261,222,220,221,259,260])).
% 59.51/59.60 cnf(473,plain,
% 59.51/59.60 (~P8(a20,a1,a2,a16,a18,a1,a15,a16)),
% 59.51/59.60 inference(scs_inference,[],[378,318,418,437,261,222,220,221,259,260,262])).
% 59.51/59.60 cnf(475,plain,
% 59.51/59.60 (P1(a18,a18,a17)),
% 59.51/59.60 inference(scs_inference,[],[366,378,318,418,437,261,222,220,221,259,260,262,158])).
% 59.51/59.60 cnf(482,plain,
% 59.51/59.60 (~P8(a16,a2,a15,a16,a1,a20,a1,a18)),
% 59.51/59.60 inference(scs_inference,[],[360,261])).
% 59.51/59.60 cnf(484,plain,
% 59.51/59.60 (~P8(a2,a16,a15,a16,a18,a1,a20,a1)),
% 59.51/59.60 inference(scs_inference,[],[412,360,261,259])).
% 59.51/59.60 cnf(486,plain,
% 59.51/59.60 (~P8(a18,a1,a2,a16,a20,a1,a15,a16)),
% 59.51/59.60 inference(scs_inference,[],[412,360,261,259,262])).
% 59.51/59.60 cnf(488,plain,
% 59.51/59.60 (~P8(a20,a1,a18,a1,a15,a16,a2,a16)),
% 59.51/59.60 inference(scs_inference,[],[412,360,261,259,262,260])).
% 59.51/59.60 cnf(490,plain,
% 59.51/59.60 (P1(a20,a20,a1)),
% 59.51/59.60 inference(scs_inference,[],[396,412,360,261,259,262,260,158])).
% 59.51/59.60 cnf(504,plain,
% 59.51/59.60 (~P8(a16,a2,a15,a16,a1,a20,a18,a1)),
% 59.51/59.60 inference(scs_inference,[],[392,261])).
% 59.51/59.60 cnf(506,plain,
% 59.51/59.60 (~P8(a1,a18,a15,a16,a1,a20,a2,a16)),
% 59.51/59.60 inference(scs_inference,[],[358,392,261,259])).
% 59.51/59.60 cnf(508,plain,
% 59.51/59.60 (~P8(a18,a1,a15,a16,a1,a20,a2,a16)),
% 59.51/59.60 inference(scs_inference,[],[358,390,392,261,259,262])).
% 59.51/59.60 cnf(510,plain,
% 59.51/59.60 (~P8(a2,a16,a1,a20,a15,a16,a1,a18)),
% 59.51/59.60 inference(scs_inference,[],[358,390,392,261,259,262,260])).
% 59.51/59.60 cnf(512,plain,
% 59.51/59.60 (~P4(x5121,x5122,a2,a16)+P4(x5121,x5122,a15,a16)),
% 59.51/59.60 inference(scs_inference,[],[148,358,390,392,261,259,262,260,186])).
% 59.51/59.60 cnf(514,plain,
% 59.51/59.60 (~P4(a15,x5141,a2,a16)+P6(x5141,a16,a16,a16)),
% 59.51/59.60 inference(scs_inference,[],[148,358,390,392,261,259,262,260,186,199])).
% 59.51/59.60 cnf(519,plain,
% 59.51/59.60 (~P8(a16,a2,a15,a16,a1,a18,a20,a1)),
% 59.51/59.60 inference(scs_inference,[],[420,261])).
% 59.51/59.60 cnf(521,plain,
% 59.51/59.60 (~P8(a15,a16,a2,a16,a1,a18,a1,a20)),
% 59.51/59.60 inference(scs_inference,[],[362,420,261,259])).
% 59.51/59.60 cnf(523,plain,
% 59.51/59.60 (~P8(a2,a16,a1,a18,a15,a16,a20,a1)),
% 59.51/59.60 inference(scs_inference,[],[362,420,261,259,262])).
% 59.51/59.60 cnf(540,plain,
% 59.51/59.60 (~P8(a16,a2,a1,a18,a15,a16,a1,a20)),
% 59.51/59.60 inference(scs_inference,[],[326,261])).
% 59.51/59.60 cnf(542,plain,
% 59.51/59.60 (~P8(a20,a1,a15,a16,a1,a18,a2,a16)),
% 59.51/59.60 inference(scs_inference,[],[422,326,261,262])).
% 59.51/59.60 cnf(544,plain,
% 59.51/59.60 (~P8(a15,a16,a2,a16,a20,a1,a1,a18)),
% 59.51/59.60 inference(scs_inference,[],[422,326,261,262,259])).
% 59.51/59.60 cnf(546,plain,
% 59.51/59.60 (~P8(a2,a16,a20,a1,a15,a16,a1,a18)),
% 59.51/59.60 inference(scs_inference,[],[422,443,326,261,262,259,260])).
% 59.51/59.60 cnf(552,plain,
% 59.51/59.60 (~P8(a16,a2,a1,a18,a15,a16,a20,a1)),
% 59.51/59.60 inference(scs_inference,[],[523,261])).
% 59.51/59.60 cnf(554,plain,
% 59.51/59.60 (~P8(a18,a1,a15,a16,a20,a1,a2,a16)),
% 59.51/59.60 inference(scs_inference,[],[473,523,261,259])).
% 59.51/59.60 cnf(556,plain,
% 59.51/59.60 (~P8(a1,a20,a15,a16,a18,a1,a2,a16)),
% 59.51/59.60 inference(scs_inference,[],[473,523,324,261,259,262])).
% 59.51/59.60 cnf(564,plain,
% 59.51/59.60 (~P8(a16,a2,a15,a16,a20,a1,a18,a1)),
% 59.51/59.60 inference(scs_inference,[],[469,261])).
% 59.51/59.60 cnf(566,plain,
% 59.51/59.60 (~P8(a1,a18,a15,a16,a20,a1,a2,a16)),
% 59.51/59.60 inference(scs_inference,[],[445,469,261,262])).
% 59.51/59.60 cnf(568,plain,
% 59.51/59.60 (~P8(a20,a1,a15,a16,a18,a1,a2,a16)),
% 59.51/59.60 inference(scs_inference,[],[486,445,469,261,262,259])).
% 59.51/59.60 cnf(570,plain,
% 59.51/59.60 (~P8(a15,a16,a1,a18,a2,a16,a1,a20)),
% 59.51/59.60 inference(scs_inference,[],[506,486,445,469,261,262,259,260])).
% 59.51/59.60 cnf(581,plain,
% 59.51/59.60 (~P8(a16,a2,a15,a16,a18,a1,a20,a1)),
% 59.51/59.60 inference(scs_inference,[],[484,261])).
% 59.51/59.60 cnf(583,plain,
% 59.51/59.60 (~P8(a15,a16,a1,a20,a16,a2,a1,a18)),
% 59.51/59.60 inference(scs_inference,[],[540,484,261,259])).
% 59.51/59.60 cnf(585,plain,
% 59.51/59.60 (~P8(a16,a15,a1,a20,a2,a16,a1,a18)),
% 59.51/59.60 inference(scs_inference,[],[540,461,484,261,259,262])).
% 59.51/59.60 cnf(587,plain,
% 59.51/59.60 (~P8(a15,a16,a18,a1,a2,a16,a1,a20)),
% 59.51/59.60 inference(scs_inference,[],[508,540,461,484,261,259,262,260])).
% 59.51/59.60 cnf(597,plain,
% 59.51/59.60 (~P8(a16,a2,a1,a20,a15,a16,a1,a18)),
% 59.51/59.60 inference(scs_inference,[],[510,261])).
% 59.51/59.60 cnf(599,plain,
% 59.51/59.60 (~P8(a16,a2,a1,a20,a15,a16,a18,a1)),
% 59.51/59.60 inference(scs_inference,[],[504,510,261,262])).
% 59.51/59.60 cnf(601,plain,
% 59.51/59.60 (~P8(a15,a16,a20,a1,a2,a16,a1,a18)),
% 59.51/59.60 inference(scs_inference,[],[542,504,510,261,262,260])).
% 59.51/59.60 cnf(603,plain,
% 59.51/59.60 (~P8(a1,a18,a1,a20,a16,a2,a15,a16)),
% 59.51/59.60 inference(scs_inference,[],[542,314,504,510,261,262,260,259])).
% 59.51/59.60 cnf(617,plain,
% 59.51/59.60 (~P8(a15,a16,a2,a16,a18,a1,a20,a1)),
% 59.51/59.60 inference(scs_inference,[],[441,471,521,261,260,259])).
% 59.51/59.60 cnf(619,plain,
% 59.51/59.60 (~P8(a2,a16,a15,a16,a20,a1,a1,a18)),
% 59.51/59.60 inference(scs_inference,[],[441,471,521,546,261,260,259,262])).
% 59.51/59.60 cnf(623,plain,
% 59.51/59.60 (~P5(x6231,x6232,x6233,x6234,a17,a16,a16,a2)+P5(x6231,x6232,x6233,x6234,a2,a16,a16,a1)),
% 59.51/59.60 inference(scs_inference,[],[152,283,441,471,521,546,261,260,259,262,124,136,265])).
% 59.51/59.60 cnf(635,plain,
% 59.51/59.60 (~P8(a16,a15,a1,a18,a2,a16,a1,a20)),
% 59.51/59.60 inference(scs_inference,[],[570,261])).
% 59.51/59.60 cnf(637,plain,
% 59.51/59.60 (~P8(a15,a16,a1,a18,a16,a2,a1,a20)),
% 59.51/59.60 inference(scs_inference,[],[597,570,261,259])).
% 59.51/59.60 cnf(639,plain,
% 59.51/59.60 (~P8(a16,a2,a20,a1,a15,a16,a18,a1)),
% 59.51/59.60 inference(scs_inference,[],[597,570,564,261,259,262])).
% 59.51/59.60 cnf(641,plain,
% 59.51/59.60 (~P8(a15,a16,a18,a1,a2,a16,a20,a1)),
% 59.51/59.60 inference(scs_inference,[],[554,597,570,564,261,259,262,260])).
% 59.51/59.60 cnf(647,plain,
% 59.51/59.60 (~P8(a16,a15,a20,a1,a2,a16,a1,a18)),
% 59.51/59.60 inference(scs_inference,[],[601,261])).
% 59.51/59.60 cnf(649,plain,
% 59.51/59.60 (~P8(a16,a2,a18,a1,a15,a16,a20,a1)),
% 59.51/59.60 inference(scs_inference,[],[601,581,261,262])).
% 59.51/59.60 cnf(651,plain,
% 59.51/59.60 (~P8(a15,a16,a20,a1,a2,a16,a18,a1)),
% 59.51/59.60 inference(scs_inference,[],[568,601,581,261,262,260])).
% 59.51/59.60 cnf(653,plain,
% 59.51/59.60 (~P8(a1,a20,a1,a18,a16,a2,a15,a16)),
% 59.51/59.60 inference(scs_inference,[],[568,482,601,581,261,262,260,259])).
% 59.51/59.60 cnf(656,plain,
% 59.51/59.60 (~P9(a17,a17,x6561,x6562)+P9(a19,a19,x6561,x6562)),
% 59.51/59.60 inference(scs_inference,[],[149,285,568,482,601,581,261,262,260,259,120,185])).
% 59.51/59.60 cnf(660,plain,
% 59.51/59.60 (~P10(x6601,x6602,a19,a19)+P10(x6601,x6602,a17,a17)),
% 59.51/59.60 inference(scs_inference,[],[144,149,151,285,568,482,601,581,261,262,260,259,120,185,123,89,182])).
% 59.51/59.60 cnf(667,plain,
% 59.51/59.60 (~P8(a16,a15,a2,a16,a20,a1,a1,a18)),
% 59.51/59.60 inference(scs_inference,[],[544,261])).
% 59.51/59.60 cnf(669,plain,
% 59.51/59.60 (~P8(a1,a18,a16,a2,a20,a1,a15,a16)),
% 59.51/59.60 inference(scs_inference,[],[552,544,261,260])).
% 59.51/59.60 cnf(671,plain,
% 59.51/59.60 (~P8(a15,a16,a2,a16,a20,a1,a18,a1)),
% 59.51/59.60 inference(scs_inference,[],[488,552,544,261,260,259])).
% 59.51/59.60 cnf(673,plain,
% 59.51/59.60 (~P8(a15,a16,a16,a2,a1,a20,a1,a18)),
% 59.51/59.60 inference(scs_inference,[],[488,552,544,583,261,260,259,262])).
% 59.51/59.60 cnf(675,plain,
% 59.51/59.60 (~P3(x6751,a20,a18)+~P9(a1,x6751,a20,a18)),
% 59.51/59.60 inference(scs_inference,[],[269,488,552,544,583,261,260,259,262,176])).
% 59.51/59.60 cnf(677,plain,
% 59.51/59.60 (~P3(x6771,a18,a20)+~P9(a1,x6771,a20,a18)),
% 59.51/59.60 inference(scs_inference,[],[269,488,552,544,583,261,260,259,262,176,157])).
% 59.51/59.60 cnf(680,plain,
% 59.51/59.60 (~P8(a16,a15,a18,a1,a2,a16,a1,a20)),
% 59.51/59.60 inference(scs_inference,[],[587,261])).
% 59.51/59.60 cnf(682,plain,
% 59.51/59.60 (~P8(a1,a18,a20,a1,a16,a2,a15,a16)),
% 59.51/59.60 inference(scs_inference,[],[519,587,261,259])).
% 59.51/59.60 cnf(686,plain,
% 59.51/59.60 (~P8(a15,a16,a16,a2,a20,a1,a1,a18)),
% 59.51/59.60 inference(scs_inference,[],[519,587,261,259,262,260])).
% 59.51/59.60 cnf(693,plain,
% 59.51/59.60 (~P8(a18,a1,a1,a20,a16,a2,a15,a16)),
% 59.51/59.60 inference(scs_inference,[],[603,261])).
% 59.51/59.60 cnf(697,plain,
% 59.51/59.60 (~P8(a15,a16,a1,a20,a2,a16,a18,a1)),
% 59.51/59.60 inference(scs_inference,[],[556,603,261,262,260])).
% 59.51/59.60 cnf(699,plain,
% 59.51/59.60 (~P8(a15,a16,a18,a1,a16,a2,a1,a20)),
% 59.51/59.60 inference(scs_inference,[],[556,599,603,261,262,260,259])).
% 59.51/59.60 cnf(701,plain,
% 59.51/59.60 (~P4(a1,x7011,a1,x7012)+~P11(a1,x7011,a20,a1,x7012,a18)),
% 59.51/59.60 inference(scs_inference,[],[316,556,599,603,261,262,260,259,223])).
% 59.51/59.60 cnf(730,plain,
% 59.51/59.60 (~P8(a16,a15,a16,a2,a20,a1,a1,a18)),
% 59.51/59.60 inference(scs_inference,[],[686,261])).
% 59.51/59.60 cnf(732,plain,
% 59.51/59.60 (~P8(a15,a16,a1,a18,a2,a16,a20,a1)),
% 59.51/59.60 inference(scs_inference,[],[686,566,261,260])).
% 59.51/59.60 cnf(734,plain,
% 59.51/59.60 (~P8(a20,a1,a1,a18,a15,a16,a16,a2)),
% 59.51/59.60 inference(scs_inference,[],[686,566,261,260,259])).
% 59.51/59.60 cnf(739,plain,
% 59.51/59.60 (~P4(x7391,a18,x7392,a20)+~P11(x7391,a18,a1,x7392,a20,a1)),
% 59.51/59.60 inference(scs_inference,[],[145,382,686,566,261,260,259,262,88,223])).
% 59.51/59.60 cnf(741,plain,
% 59.51/59.60 (~P9(a17,a17,x7411,x7412)+P9(a1,a1,x7411,x7412)),
% 59.51/59.60 inference(scs_inference,[],[145,283,382,686,566,261,260,259,262,88,223,185])).
% 59.51/59.60 cnf(750,plain,
% 59.51/59.60 (~P8(a16,a15,a2,a16,a18,a1,a20,a1)),
% 59.51/59.60 inference(scs_inference,[],[617,261])).
% 59.51/59.60 cnf(752,plain,
% 59.51/59.60 (~P8(a15,a16,a18,a1,a16,a2,a20,a1)),
% 59.51/59.60 inference(scs_inference,[],[639,617,261,259])).
% 59.51/59.60 cnf(754,plain,
% 59.51/59.60 (~P8(a15,a16,a16,a2,a1,a18,a1,a20)),
% 59.51/59.60 inference(scs_inference,[],[639,617,637,261,259,262])).
% 59.51/59.60 cnf(759,plain,
% 59.51/59.60 (~P4(x7591,a1,x7592,a1)+~P11(x7591,a1,a20,x7592,a1,a18)),
% 59.51/59.60 inference(scs_inference,[],[143,384,639,617,637,261,259,262,260,88,223])).
% 59.51/59.60 cnf(772,plain,
% 59.51/59.60 (~P4(x7721,a20,x7722,a18)+~P11(x7721,a20,a1,x7722,a18,a1)),
% 59.51/59.60 inference(scs_inference,[],[144,386,734,585,261,262,260,259,88,223])).
% 59.51/59.60 cnf(780,plain,
% 59.51/59.60 (~P8(a20,a1,a1,a18,a16,a15,a16,a2)),
% 59.51/59.60 inference(scs_inference,[],[641,730,261,260,259])).
% 59.51/59.60 cnf(782,plain,
% 59.51/59.60 (~P8(a16,a15,a20,a1,a16,a2,a1,a18)),
% 59.51/59.60 inference(scs_inference,[],[641,730,261,260,259,262])).
% 59.51/59.60 cnf(789,plain,
% 59.51/59.60 (P8(x7891,a19,a19,a17,x7891,a19,a19,a17)+~P1(x7891,a19,a17)),
% 59.51/59.60 inference(scs_inference,[],[143,144,285,426,416,641,730,261,260,259,262,88,223,90,89,231])).
% 59.51/59.60 cnf(794,plain,
% 59.51/59.60 (~P8(a18,a1,a20,a1,a16,a2,a15,a16)),
% 59.51/59.60 inference(scs_inference,[],[682,261])).
% 59.51/59.60 cnf(812,plain,
% 59.51/59.60 (~P8(a18,a1,a16,a2,a20,a1,a15,a16)),
% 59.51/59.60 inference(scs_inference,[],[669,261])).
% 59.51/59.60 cnf(821,plain,
% 59.51/59.60 (~P4(x8211,a18,x8212,a1)+~P11(x8211,a18,a1,x8212,a1,a20)),
% 59.51/59.60 inference(scs_inference,[],[475,439,635,669,653,261,262,260,259,88,223])).
% 59.51/59.60 cnf(839,plain,
% 59.51/59.60 (~P4(x8391,a20,x8392,a1)+~P11(x8391,a20,a1,x8392,a1,a18)),
% 59.51/59.60 inference(scs_inference,[],[490,463,782,671,680,261,260,259,262,88,223])).
% 59.51/59.60 cnf(852,plain,
% 59.51/59.60 (~P8(a18,a1,a16,a2,a1,a20,a15,a16)),
% 59.51/59.60 inference(scs_inference,[],[667,651,693,261,259,262])).
% 59.51/59.60 cnf(875,plain,
% 59.51/59.60 (~P4(x8751,a1,x8752,a20)+~P11(x8751,a1,a18,x8752,a20,a1)),
% 59.51/59.60 inference(scs_inference,[],[330,467,647,619,697,261,262,260,259,88,223])).
% 59.51/59.60 cnf(887,plain,
% 59.51/59.60 (~P8(a18,a1,a15,a16,a1,a20,a16,a2)),
% 59.51/59.60 inference(scs_inference,[],[649,699,261,260])).
% 59.51/59.60 cnf(891,plain,
% 59.51/59.60 (~P8(a15,a16,a16,a2,a18,a1,a1,a20)),
% 59.51/59.60 inference(scs_inference,[],[649,699,261,260,259,262])).
% 59.51/59.60 cnf(898,plain,
% 59.51/59.60 (P1(a2,a15,a1)),
% 59.51/59.60 inference(scs_inference,[],[142,154,155])).
% 59.51/59.60 cnf(899,plain,
% 59.51/59.60 (~P8(a16,a15,a16,a2,a1,a20,a1,a18)),
% 59.51/59.60 inference(scs_inference,[],[673,261])).
% 59.51/59.60 cnf(907,plain,
% 59.51/59.60 (P1(a1,a1,a2)),
% 59.51/59.60 inference(scs_inference,[],[898,812,852,673,732,261,259,262,260,158])).
% 59.51/59.60 cnf(912,plain,
% 59.51/59.60 (~P11(a1,a20,a18,a16,a15,a2)),
% 59.51/59.60 inference(scs_inference,[],[366,898,812,852,673,732,261,259,262,260,158,235,88,217])).
% 59.51/59.60 cnf(914,plain,
% 59.51/59.60 (~P11(a15,a16,a2,a20,a1,a18)),
% 59.51/59.60 inference(scs_inference,[],[366,898,812,852,673,732,261,259,262,260,158,235,88,217,218])).
% 59.51/59.60 cnf(916,plain,
% 59.51/59.60 (~P11(a16,a2,a15,a1,a18,a20)),
% 59.51/59.60 inference(scs_inference,[],[366,898,812,852,673,732,261,259,262,260,158,235,88,217,218,219])).
% 59.51/59.60 cnf(918,plain,
% 59.51/59.60 (~P4(a1,x9181,a1,x9182)+~P11(a1,x9181,a18,a1,x9182,a20)),
% 59.51/59.60 inference(scs_inference,[],[366,898,279,812,852,673,732,261,259,262,260,158,235,88,217,218,219,223])).
% 59.51/59.60 cnf(927,plain,
% 59.51/59.60 (~P11(a20,a1,a18,a15,a16,a2)),
% 59.51/59.60 inference(scs_inference,[],[914,217])).
% 59.51/59.60 cnf(929,plain,
% 59.51/59.60 (~P11(a1,a18,a20,a16,a2,a15)),
% 59.51/59.60 inference(scs_inference,[],[912,914,217,219])).
% 59.51/59.60 cnf(931,plain,
% 59.51/59.60 (~P11(a2,a16,a15,a18,a1,a20)),
% 59.51/59.60 inference(scs_inference,[],[912,914,916,217,219,218])).
% 59.51/59.60 cnf(941,plain,
% 59.51/59.60 (P1(a2,a2,a1)),
% 59.51/59.60 inference(scs_inference,[],[907,891,794,752,912,914,916,217,219,218,261,262,260,259,158])).
% 59.51/59.60 cnf(966,plain,
% 59.51/59.60 (~P11(a20,a18,a1,a15,a2,a16)),
% 59.51/59.60 inference(scs_inference,[],[927,931,217,219])).
% 59.51/59.60 cnf(968,plain,
% 59.51/59.60 (~P8(a16,a15,a16,a2,a1,a18,a1,a20)),
% 59.51/59.60 inference(scs_inference,[],[927,754,931,217,219,261])).
% 59.51/59.60 cnf(972,plain,
% 59.51/59.60 (~P8(a1,a20,a1,a18,a16,a15,a16,a2)),
% 59.51/59.60 inference(scs_inference,[],[899,927,754,931,217,219,261,262,259])).
% 59.51/59.60 cnf(974,plain,
% 59.51/59.60 (~P8(a16,a2,a16,a15,a1,a18,a1,a20)),
% 59.51/59.60 inference(scs_inference,[],[899,927,754,931,217,219,261,262,259,260])).
% 59.51/59.60 cnf(976,plain,
% 59.51/59.60 (~P11(a18,a20,a1,a2,a15,a16)),
% 59.51/59.60 inference(scs_inference,[],[899,927,754,931,217,219,261,262,259,260,218])).
% 59.51/59.60 cnf(978,plain,
% 59.51/59.60 (~P11(a16,a15,a2,a1,a18,a20)),
% 59.51/59.60 inference(scs_inference,[],[899,927,754,931,217,219,261,262,259,260,218,235])).
% 59.51/59.60 cnf(981,plain,
% 59.51/59.60 (~P4(x9811,a1,x9812,a18)+~P11(x9811,a1,a20,x9812,a18,a1)),
% 59.51/59.60 inference(scs_inference,[],[396,418,899,927,754,931,217,219,261,262,259,260,218,235,88,223])).
% 59.51/59.60 cnf(992,plain,
% 59.51/59.60 (~P11(a15,a16,a2,a18,a1,a20)),
% 59.51/59.60 inference(scs_inference,[],[966,978,217,218])).
% 59.51/59.60 cnf(994,plain,
% 59.51/59.60 (~P11(a16,a2,a15,a1,a20,a18)),
% 59.51/59.60 inference(scs_inference,[],[966,978,217,218,219])).
% 59.51/59.60 cnf(1023,plain,
% 59.51/59.60 (~P11(a15,a2,a16,a18,a20,a1)),
% 59.51/59.60 inference(scs_inference,[],[976,992,217,219])).
% 59.51/59.60 cnf(1027,plain,
% 59.51/59.60 (~P8(a2,a16,a16,a15,a1,a18,a1,a20)),
% 59.51/59.60 inference(scs_inference,[],[974,976,992,994,217,219,218,261])).
% 59.51/59.60 cnf(1031,plain,
% 59.51/59.60 (~P8(a1,a18,a1,a20,a16,a15,a16,a2)),
% 59.51/59.60 inference(scs_inference,[],[972,968,974,976,992,994,217,219,218,261,262,259])).
% 59.51/59.60 cnf(1033,plain,
% 59.51/59.60 (~P8(a1,a18,a1,a20,a16,a2,a16,a15)),
% 59.51/59.60 inference(scs_inference,[],[972,968,974,976,992,994,217,219,218,261,262,259,260])).
% 59.51/59.60 cnf(1035,plain,
% 59.51/59.60 (~P11(a1,a18,a20,a16,a15,a2)),
% 59.51/59.60 inference(scs_inference,[],[972,968,974,976,992,994,217,219,218,261,262,259,260,235])).
% 59.51/59.60 cnf(1042,plain,
% 59.51/59.60 (~P11(a18,a20,a1,a15,a2,a16)),
% 59.51/59.60 inference(scs_inference,[],[1023,217])).
% 59.51/59.60 cnf(1044,plain,
% 59.51/59.60 (~P11(a2,a15,a16,a20,a18,a1)),
% 59.51/59.60 inference(scs_inference,[],[1023,217,218])).
% 59.51/59.60 cnf(1046,plain,
% 59.51/59.60 (~P11(a1,a20,a18,a16,a2,a15)),
% 59.51/59.60 inference(scs_inference,[],[1023,1035,217,218,219])).
% 59.51/59.60 cnf(1054,plain,
% 59.51/59.60 (~P8(a16,a2,a16,a15,a1,a20,a1,a18)),
% 59.51/59.60 inference(scs_inference,[],[974,968,887,1023,1035,217,218,219,261,262,259,260])).
% 59.51/59.60 cnf(1056,plain,
% 59.51/59.60 (~P4(x10561,a1,x10562,a1)+~P11(x10561,a1,a18,x10562,a1,a20)),
% 59.51/59.60 inference(scs_inference,[],[322,974,968,887,1023,1035,217,218,219,261,262,259,260,223])).
% 59.51/59.60 cnf(1058,plain,
% 59.51/59.60 (~P3(x10581,a1,a1)+~P11(x10581,a1,a18,x10581,a1,a20)),
% 59.51/59.60 inference(scs_inference,[],[322,974,968,887,1023,1035,217,218,219,261,262,259,260,223,159])).
% 59.51/59.60 cnf(1062,plain,
% 59.51/59.60 (~P4(x10621,a1,a1,x10621)+~P11(x10621,a1,a18,x10621,a1,a20)),
% 59.51/59.60 inference(scs_inference,[],[322,974,968,887,1023,1035,217,218,219,261,262,259,260,223,159,205,171])).
% 59.51/59.60 cnf(1070,plain,
% 59.51/59.60 (~P3(x10701,x10702,a1)+~P11(f29(a1,a17,x10702,a1,a19,x10701),a1,a18,f29(a1,a17,x10702,a1,a19,x10701),a1,a20)),
% 59.51/59.60 inference(scs_inference,[],[146,322,974,968,887,1023,1035,217,218,219,261,262,259,260,223,159,205,171,170,222,221,206])).
% 59.51/59.60 cnf(1081,plain,
% 59.51/59.60 (~P8(a18,a1,a1,a20,a16,a15,a16,a2)),
% 59.51/59.60 inference(scs_inference,[],[1031,1044,1042,1046,217,218,219,261])).
% 59.51/59.60 cnf(1087,plain,
% 59.51/59.60 (~P8(a1,a20,a1,a18,a16,a2,a16,a15)),
% 59.51/59.60 inference(scs_inference,[],[968,1031,750,1044,1042,1046,217,218,219,261,262,259,260])).
% 59.51/59.60 cnf(1104,plain,
% 59.51/59.60 (~P8(a18,a1,a1,a20,a16,a2,a16,a15)),
% 59.51/59.60 inference(scs_inference,[],[1033,261])).
% 59.51/59.60 cnf(1113,plain,
% 59.51/59.60 (P1(a15,a2,a1)),
% 59.51/59.60 inference(scs_inference,[],[426,907,1033,780,1027,261,262,259,260,88,158])).
% 59.51/59.60 cnf(1146,plain,
% 59.51/59.60 (P8(x11461,a1,a1,a17,x11461,a1,a1,a17)+~P1(x11461,a1,a17)),
% 59.51/59.60 inference(scs_inference,[],[152,283,941,1113,1054,1087,1081,1104,261,262,259,260,88,90,89,264,231])).
% 59.51/59.60 cnf(1216,plain,
% 59.51/59.60 (P8(a19,a1,a1,a17,a19,a1,a1,a17)),
% 59.51/59.60 inference(scs_inference,[],[146,156,1146])).
% 59.51/59.60 cnf(1703,plain,
% 59.51/59.60 (~P3(x17031,a20,a18)+~P9(a1,x17031,a18,a20)),
% 59.51/59.60 inference(scs_inference,[],[299,157])).
% 59.51/59.60 cnf(1784,plain,
% 59.51/59.60 (P5(a17,a17,x17841,x17842,a1,a1,x17841,x17842)),
% 59.51/59.60 inference(scs_inference,[],[283,166,228])).
% 59.51/59.60 cnf(1797,plain,
% 59.51/59.60 (~P5(x17971,x17972,x17973,x17974,a17,a17,x17975,x17976)+P5(x17971,x17972,x17973,x17974,a1,a1,x17975,x17976)),
% 59.51/59.60 inference(scs_inference,[],[1784,265])).
% 59.51/59.60 cnf(1817,plain,
% 59.51/59.60 (P10(a17,a17,a1,a1)),
% 59.51/59.60 inference(scs_inference,[],[283,167,166])).
% 59.51/59.60 cnf(1818,plain,
% 59.51/59.60 (P10(a17,a17,a17,a17)),
% 59.51/59.60 inference(scs_inference,[],[1817,377])).
% 59.51/59.60 cnf(1820,plain,
% 59.51/59.60 (P10(a1,a1,a1,a1)),
% 59.51/59.60 inference(scs_inference,[],[283,1817,377,182])).
% 59.51/59.60 cnf(1828,plain,
% 59.51/59.60 (P8(x18281,a17,a17,a1,x18281,a17,a17,a1)+~P1(x18281,a17,a1)),
% 59.51/59.60 inference(scs_inference,[],[283,1817,377,182,127,185,124,125,126,231])).
% 59.51/59.60 cnf(1863,plain,
% 59.51/59.60 (P8(x18631,a1,a1,a1,x18631,a1,a1,a1)+~P1(x18631,a1,a1)),
% 59.51/59.60 inference(scs_inference,[],[1820,231])).
% 59.51/59.60 cnf(1866,plain,
% 59.51/59.60 (P8(x18661,a17,a17,a17,x18661,a17,a17,a17)+~P1(x18661,a17,a17)),
% 59.51/59.60 inference(scs_inference,[],[1818,231])).
% 59.51/59.60 cnf(2017,plain,
% 59.51/59.60 (P1(a2,a1,a15)),
% 59.51/59.60 inference(scs_inference,[],[142,154])).
% 59.51/59.60 cnf(2019,plain,
% 59.51/59.60 (P1(a1,a15,a2)),
% 59.51/59.60 inference(scs_inference,[],[142,154,155])).
% 59.51/59.60 cnf(2021,plain,
% 59.51/59.60 (P1(a19,a1,a17)),
% 59.51/59.60 inference(scs_inference,[],[142,146,154,155,156])).
% 59.51/59.60 cnf(2023,plain,
% 59.51/59.60 (P1(a17,a17,a17)),
% 59.51/59.60 inference(scs_inference,[],[142,1818,146,154,155,156,163])).
% 59.51/59.60 cnf(2025,plain,
% 59.51/59.60 (P10(a17,a17,a19,a19)),
% 59.51/59.60 inference(scs_inference,[],[142,1818,146,285,154,155,156,163,166])).
% 59.51/59.60 cnf(2027,plain,
% 59.51/59.60 (P5(a17,a17,x20271,x20272,a17,a17,x20271,x20272)),
% 59.51/59.60 inference(scs_inference,[],[142,1818,146,285,154,155,156,163,166,228])).
% 59.51/59.60 cnf(2033,plain,
% 59.51/59.60 (P3(a19,a17,a1)),
% 59.51/59.60 inference(scs_inference,[],[142,151,1818,146,285,154,155,156,163,166,228,190,1866,157])).
% 59.51/59.60 cnf(2035,plain,
% 59.51/59.60 (P4(a2,a16,a16,a15)),
% 59.51/59.60 inference(scs_inference,[],[142,151,1818,148,146,285,154,155,156,163,166,228,190,1866,157,171])).
% 59.51/59.60 cnf(2037,plain,
% 59.51/59.60 (P9(a16,a2,a15,a16)),
% 59.51/59.60 inference(scs_inference,[],[142,151,1818,147,148,146,285,154,155,156,163,166,228,190,1866,157,171,169])).
% 59.51/59.60 cnf(2039,plain,
% 59.51/59.60 (P5(a16,a17,a16,a2,a2,a16,a16,a1)),
% 59.51/59.60 inference(scs_inference,[],[142,151,1818,147,148,146,152,285,154,155,156,163,166,228,190,1866,157,171,169,257])).
% 59.51/59.60 cnf(2043,plain,
% 59.51/59.60 (P9(a16,a15,a16,a2)),
% 59.51/59.60 inference(scs_inference,[],[142,151,1818,1784,147,148,146,152,285,154,155,156,163,166,228,190,1866,157,171,169,257,255,168])).
% 59.51/59.60 cnf(2045,plain,
% 59.51/59.60 (P4(a19,a1,a19,a17)),
% 59.51/59.60 inference(scs_inference,[],[142,151,1818,1784,147,148,146,152,285,154,155,156,163,166,228,190,1866,157,171,169,257,255,168,159])).
% 59.51/59.60 cnf(2047,plain,
% 59.51/59.60 (P5(a17,a17,a1,a1,x20471,x20472,x20471,x20472)),
% 59.51/59.60 inference(scs_inference,[],[142,151,1818,1784,147,148,146,152,285,154,155,156,163,166,228,190,1866,157,171,169,257,255,168,159,258])).
% 59.51/59.60 cnf(2049,plain,
% 59.51/59.60 (P5(x20491,x20492,a17,a17,x20491,x20492,a1,a1)),
% 59.51/59.60 inference(scs_inference,[],[142,151,1818,1784,147,148,146,152,285,154,155,156,163,166,228,190,1866,157,171,169,257,255,168,159,258,256])).
% 59.51/59.60 cnf(2051,plain,
% 59.51/59.60 (P8(a1,a17,a19,a1,a1,a17,a19,a1)),
% 59.51/59.60 inference(scs_inference,[],[142,151,1818,1784,147,1216,148,146,152,285,154,155,156,163,166,228,190,1866,157,171,169,257,255,168,159,258,256,260])).
% 59.51/59.60 cnf(2053,plain,
% 59.51/59.60 (P8(a19,a1,a19,a1,a1,a17,a1,a17)),
% 59.51/59.60 inference(scs_inference,[],[142,151,1818,1784,147,1216,148,146,152,285,154,155,156,163,166,228,190,1866,157,171,169,257,255,168,159,258,256,260,262])).
% 59.51/59.60 cnf(2057,plain,
% 59.51/59.60 (P8(a1,a19,a1,a17,a19,a1,a1,a17)),
% 59.51/59.60 inference(scs_inference,[],[142,151,1818,1784,147,1216,148,146,152,285,154,155,156,163,166,228,190,1866,157,171,169,257,255,168,159,258,256,260,262,259,261])).
% 59.51/59.60 cnf(2061,plain,
% 59.51/59.60 (P2(a19,a1,a17,a17)),
% 59.51/59.60 inference(scs_inference,[],[142,151,1818,1784,147,1216,148,146,152,285,154,155,156,163,166,228,190,1866,157,171,169,257,255,168,159,258,256,260,262,259,261,170,187])).
% 59.51/59.60 cnf(2065,plain,
% 59.51/59.60 (P10(f29(a1,a17,a1,a17,a19,a19),a19,a1,a1)),
% 59.51/59.60 inference(scs_inference,[],[142,151,1818,1784,147,1216,148,146,152,285,154,155,156,163,166,228,190,1866,157,171,169,257,255,168,159,258,256,260,262,259,261,170,187,181,207])).
% 59.51/59.60 cnf(2067,plain,
% 59.51/59.60 (P10(f29(a1,a17,a1,a17,a19,a19),a19,a17,a17)),
% 59.51/59.60 inference(scs_inference,[],[142,151,1818,1784,147,1216,148,146,152,285,154,155,156,163,166,228,190,1866,157,171,169,257,255,168,159,258,256,260,262,259,261,170,187,181,207,208])).
% 59.51/59.60 cnf(2069,plain,
% 59.51/59.60 (P8(a19,a1,a19,a1,a19,a1,a19,a1)),
% 59.51/59.60 inference(scs_inference,[],[142,151,1818,1784,147,1216,148,146,152,285,154,155,156,163,166,228,190,1866,157,171,169,257,255,168,159,258,256,260,262,259,261,170,187,181,207,208,266])).
% 59.51/59.60 cnf(2071,plain,
% 59.51/59.60 (P9(a1,a17,a17,a17)),
% 59.51/59.60 inference(scs_inference,[],[142,151,1818,1784,147,1216,148,146,152,285,154,155,156,163,166,228,190,1866,157,171,169,257,255,168,159,258,256,260,262,259,261,170,187,181,207,208,266,175])).
% 59.51/59.60 cnf(2083,plain,
% 59.51/59.60 (P9(a2,a15,a16,a16)),
% 59.51/59.60 inference(scs_inference,[],[142,447,151,1818,1784,147,1216,148,146,152,285,154,155,156,163,166,228,190,1866,157,171,169,257,255,168,159,258,256,260,262,259,261,170,187,181,207,208,266,175,239,193,192,180,188,184])).
% 59.51/59.60 cnf(2085,plain,
% 59.51/59.60 (P3(f29(a1,a17,a1,a17,a19,a19),a1,a17)),
% 59.51/59.60 inference(scs_inference,[],[142,447,151,1818,1784,147,1216,148,146,152,285,154,155,156,163,166,228,190,1866,157,171,169,257,255,168,159,258,256,260,262,259,261,170,187,181,207,208,266,175,239,193,192,180,188,184,206])).
% 59.51/59.60 cnf(2087,plain,
% 59.51/59.60 (P10(a19,a19,a1,a1)),
% 59.51/59.60 inference(scs_inference,[],[142,447,151,1818,1784,147,1216,148,146,152,285,154,155,156,163,166,228,190,1866,157,171,169,257,255,168,159,258,256,260,262,259,261,170,187,181,207,208,266,175,239,193,192,180,188,184,206,161])).
% 59.51/59.60 cnf(2089,plain,
% 59.51/59.60 (P1(a15,a15,a2)),
% 59.51/59.60 inference(scs_inference,[],[142,447,151,1818,1784,147,1216,148,146,152,285,154,155,156,163,166,228,190,1866,157,171,169,257,255,168,159,258,256,260,262,259,261,170,187,181,207,208,266,175,239,193,192,180,188,184,206,161,158])).
% 59.51/59.60 cnf(2093,plain,
% 59.51/59.60 (P4(a1,a19,a17,a19)),
% 59.51/59.60 inference(scs_inference,[],[142,380,447,151,1818,1784,147,1216,148,146,152,285,154,155,156,163,166,228,190,1866,157,171,169,257,255,168,159,258,256,260,262,259,261,170,187,181,207,208,266,175,239,193,192,180,188,184,206,161,158,246,177])).
% 59.51/59.60 cnf(2095,plain,
% 59.51/59.60 (P10(a16,a2,a16,a2)),
% 59.51/59.60 inference(scs_inference,[],[142,380,447,151,1818,1784,147,1216,148,146,152,285,154,155,156,163,166,228,190,1866,157,171,169,257,255,168,159,258,256,260,262,259,261,170,187,181,207,208,266,175,239,193,192,180,188,184,206,161,158,246,177,183])).
% 59.51/59.60 cnf(2097,plain,
% 59.51/59.60 (P8(a19,a17,a17,a1,a19,a17,a17,a1)),
% 59.51/59.60 inference(scs_inference,[],[142,380,447,151,1818,1784,147,1216,148,146,152,285,154,155,156,163,166,228,190,1866,157,171,169,257,255,168,159,258,256,260,262,259,261,170,187,181,207,208,266,175,239,193,192,180,188,184,206,161,158,246,177,183,226])).
% 59.51/59.60 cnf(2099,plain,
% 59.51/59.60 (P4(a2,a16,a2,a16)),
% 59.51/59.60 inference(scs_inference,[],[142,380,447,151,1818,1784,147,1216,148,146,152,285,154,155,156,163,166,228,190,1866,157,171,169,257,255,168,159,258,256,260,262,259,261,170,187,181,207,208,266,175,239,193,192,180,188,184,206,161,158,246,177,183,226,186])).
% 59.51/59.60 cnf(2109,plain,
% 59.51/59.60 (P10(a16,a2,a2,a16)),
% 59.51/59.60 inference(scs_inference,[],[142,380,447,151,1818,1784,147,1216,148,146,152,285,154,155,156,163,166,228,190,1866,157,171,169,257,255,168,159,258,256,260,262,259,261,170,187,181,207,208,266,175,239,193,192,180,188,184,206,161,158,246,177,183,226,186,265,199,209,210,167])).
% 59.51/59.60 cnf(2111,plain,
% 59.51/59.60 (P6(a17,a1,a17,a17)),
% 59.51/59.60 inference(scs_inference,[],[142,380,447,151,1818,1784,147,1216,148,146,152,285,154,155,156,163,166,228,190,1866,157,171,169,257,255,168,159,258,256,260,262,259,261,170,187,181,207,208,266,175,239,193,192,180,188,184,206,161,158,246,177,183,226,186,265,199,209,210,167,172])).
% 59.51/59.60 cnf(2113,plain,
% 59.51/59.60 (P6(a17,a17,a15,a17)),
% 59.51/59.60 inference(scs_inference,[],[142,380,447,151,1818,1784,147,1216,148,146,152,285,154,155,156,163,166,228,190,1866,157,171,169,257,255,168,159,258,256,260,262,259,261,170,187,181,207,208,266,175,239,193,192,180,188,184,206,161,158,246,177,183,226,186,265,199,209,210,167,172,173])).
% 59.51/59.60 cnf(2115,plain,
% 59.51/59.60 (P6(a17,a17,a17,a15)),
% 59.51/59.60 inference(scs_inference,[],[142,380,447,151,1818,1784,147,1216,148,146,152,285,154,155,156,163,166,228,190,1866,157,171,169,257,255,168,159,258,256,260,262,259,261,170,187,181,207,208,266,175,239,193,192,180,188,184,206,161,158,246,177,183,226,186,265,199,209,210,167,172,173,174])).
% 59.51/59.60 cnf(2117,plain,
% 59.51/59.60 (P5(a19,a1,a1,a17,a1,a17,a19,a17)),
% 59.51/59.60 inference(scs_inference,[],[142,380,447,151,1818,1784,147,1216,148,146,152,285,154,155,156,163,166,228,190,1866,157,171,169,257,255,168,159,258,256,260,262,259,261,170,187,181,207,208,266,175,239,193,192,180,188,184,206,161,158,246,177,183,226,186,265,199,209,210,167,172,173,174,229])).
% 59.51/59.60 cnf(2119,plain,
% 59.51/59.60 (P10(a16,a15,a16,a15)),
% 59.51/59.60 inference(scs_inference,[],[142,380,447,151,1818,1784,147,1216,148,146,152,285,154,155,156,163,166,228,190,1866,157,171,169,257,255,168,159,258,256,260,262,259,261,170,187,181,207,208,266,175,239,193,192,180,188,184,206,161,158,246,177,183,226,186,265,199,209,210,167,172,173,174,229,303])).
% 59.51/59.60 cnf(2121,plain,
% 59.51/59.60 (P4(a15,a16,a15,a16)),
% 59.51/59.60 inference(scs_inference,[],[142,380,447,151,1818,1784,147,1216,148,146,152,285,154,155,156,163,166,228,190,1866,157,171,169,257,255,168,159,258,256,260,262,259,261,170,187,181,207,208,266,175,239,193,192,180,188,184,206,161,158,246,177,183,226,186,265,199,209,210,167,172,173,174,229,303,512])).
% 59.51/59.60 cnf(2123,plain,
% 59.51/59.60 (P6(a16,a16,a16,a16)),
% 59.51/59.60 inference(scs_inference,[],[142,380,447,151,1818,1784,147,1216,148,146,152,285,154,155,156,163,166,228,190,1866,157,171,169,257,255,168,159,258,256,260,262,259,261,170,187,181,207,208,266,175,239,193,192,180,188,184,206,161,158,246,177,183,226,186,265,199,209,210,167,172,173,174,229,303,512,514])).
% 59.51/59.60 cnf(2133,plain,
% 59.51/59.60 (P2(f8(a1,a17,a17),a1,a17,a17)),
% 59.51/59.60 inference(scs_inference,[],[142,380,447,151,1818,1784,147,1216,148,146,152,285,154,155,156,163,166,228,190,1866,157,171,169,257,255,168,159,258,256,260,262,259,261,170,187,181,207,208,266,175,239,193,192,180,188,184,206,161,158,246,177,183,226,186,265,199,209,210,167,172,173,174,229,303,512,514,1797,1070,227,179,194])).
% 59.51/59.61 cnf(2141,plain,
% 59.51/59.61 (P9(f12(a1,a17,a17,a17,a15),a1,a17,a15)),
% 59.51/59.61 inference(scs_inference,[],[142,380,447,151,1818,1784,147,1216,148,146,152,285,154,155,156,163,166,228,190,1866,157,171,169,257,255,168,159,258,256,260,262,259,261,170,187,181,207,208,266,175,239,193,192,180,188,184,206,161,158,246,177,183,226,186,265,199,209,210,167,172,173,174,229,303,512,514,1797,1070,227,179,194,196,197,200,201])).
% 59.51/59.61 cnf(2149,plain,
% 59.51/59.61 (P10(a1,a1,a19,a19)),
% 59.51/59.61 inference(scs_inference,[],[2087,166])).
% 59.51/59.61 cnf(2153,plain,
% 59.51/59.61 (P1(a16,a2,a2)),
% 59.51/59.61 inference(scs_inference,[],[2087,2095,2119,166,167,163])).
% 59.51/59.61 cnf(2155,plain,
% 59.51/59.61 (P1(a15,a1,a2)),
% 59.51/59.61 inference(scs_inference,[],[2019,2087,2095,2119,166,167,163,154])).
% 59.51/59.61 cnf(2157,plain,
% 59.51/59.61 (P5(a17,a17,x21571,x21572,a19,a19,x21571,x21572)),
% 59.51/59.61 inference(scs_inference,[],[2019,2025,2087,2095,2119,166,167,163,154,228])).
% 59.51/59.61 cnf(2160,plain,
% 59.51/59.61 (P5(x21601,x21602,a17,a17,x21601,x21602,a1,a1)),
% 59.51/59.61 inference(rename_variables,[],[2049])).
% 59.51/59.61 cnf(2162,plain,
% 59.51/59.61 (P6(a17,a17,a1,a17)),
% 59.51/59.61 inference(scs_inference,[],[2049,2019,2025,2087,2095,2111,2119,166,167,163,154,228,1797,173])).
% 59.51/59.61 cnf(2164,plain,
% 59.51/59.61 (P3(f29(a1,a17,a1,a17,a19,a19),a17,a1)),
% 59.51/59.61 inference(scs_inference,[],[2049,2019,2025,2087,2095,2111,2119,2085,166,167,163,154,228,1797,173,157])).
% 59.51/59.61 cnf(2166,plain,
% 59.51/59.61 (P1(a19,a17,a1)),
% 59.51/59.61 inference(scs_inference,[],[2049,2019,2021,2025,2087,2095,2111,2119,2085,166,167,163,154,228,1797,173,157,155])).
% 59.51/59.61 cnf(2170,plain,
% 59.51/59.61 (P5(a2,a16,a16,a16,a16,a16,a2,a16)),
% 59.51/59.61 inference(scs_inference,[],[2049,2019,2021,2025,2087,2095,2099,2111,2119,2085,166,167,163,154,228,1797,173,157,155,156,229])).
% 59.51/59.61 cnf(2176,plain,
% 59.51/59.61 (P4(a1,a19,a19,a17)),
% 59.51/59.61 inference(scs_inference,[],[2093,2049,2019,2021,2025,2061,2087,2095,2099,2111,2119,2085,166,167,163,154,228,1797,173,157,155,156,229,174,190,171])).
% 59.51/59.61 cnf(2178,plain,
% 59.51/59.61 (P9(a16,a15,a2,a16)),
% 59.51/59.61 inference(scs_inference,[],[2093,2049,2019,2021,2025,2043,2061,2087,2095,2099,2111,2119,2085,166,167,163,154,228,1797,173,157,155,156,229,174,190,171,169])).
% 59.51/59.61 cnf(2180,plain,
% 59.51/59.61 (P5(x21801,x21802,x21801,x21802,a17,a17,a1,a1)),
% 59.51/59.61 inference(scs_inference,[],[2093,2047,2049,2019,2021,2025,2043,2061,2087,2095,2099,2111,2119,2085,166,167,163,154,228,1797,173,157,155,156,229,174,190,171,169,255])).
% 59.51/59.61 cnf(2182,plain,
% 59.51/59.61 (P4(a19,a17,a19,a1)),
% 59.51/59.61 inference(scs_inference,[],[2093,2047,2049,2019,2021,2025,2033,2043,2061,2087,2095,2099,2111,2119,2085,166,167,163,154,228,1797,173,157,155,156,229,174,190,171,169,255,159])).
% 59.51/59.61 cnf(2184,plain,
% 59.51/59.61 (P5(a16,a16,a16,a16,a16,a16,a16,a16)),
% 59.51/59.61 inference(scs_inference,[],[2093,2123,2047,2049,2019,2021,2025,2033,2043,2061,2087,2095,2099,2111,2119,2085,166,167,163,154,228,1797,173,157,155,156,229,174,190,171,169,255,159,227])).
% 59.51/59.61 cnf(2186,plain,
% 59.51/59.61 (P5(a17,a17,a17,a17,x21861,x21862,x21861,x21862)),
% 59.51/59.61 inference(scs_inference,[],[2093,2123,2027,2047,2049,2019,2021,2025,2033,2043,2061,2087,2095,2099,2111,2119,2085,166,167,163,154,228,1797,173,157,155,156,229,174,190,171,169,255,159,227,258])).
% 59.51/59.61 cnf(2188,plain,
% 59.51/59.61 (P9(a15,a16,a16,a2)),
% 59.51/59.61 inference(scs_inference,[],[2093,2123,2027,2047,2049,2019,2021,2025,2033,2037,2043,2061,2087,2095,2099,2111,2119,2085,166,167,163,154,228,1797,173,157,155,156,229,174,190,171,169,255,159,227,258,168])).
% 59.51/59.61 cnf(2190,plain,
% 59.51/59.61 (P5(x21901,x21902,a17,a17,x21902,x21901,a1,a1)),
% 59.51/59.61 inference(scs_inference,[],[2093,2123,2027,2047,2049,2160,2019,2021,2025,2033,2037,2043,2061,2087,2095,2099,2111,2119,2085,166,167,163,154,228,1797,173,157,155,156,229,174,190,171,169,255,159,227,258,168,257])).
% 59.51/59.61 cnf(2192,plain,
% 59.51/59.61 (P8(a1,a17,a1,a19,a1,a17,a19,a1)),
% 59.51/59.61 inference(scs_inference,[],[2093,2123,2027,2047,2049,2160,2019,2021,2025,2033,2037,2043,2057,2061,2087,2095,2099,2111,2119,2085,166,167,163,154,228,1797,173,157,155,156,229,174,190,171,169,255,159,227,258,168,257,260])).
% 59.51/59.61 cnf(2194,plain,
% 59.51/59.61 (P5(x21941,x21942,a17,a17,x21941,x21942,a17,a17)),
% 59.51/59.61 inference(scs_inference,[],[2093,2123,2027,2047,2049,2160,2019,2021,2025,2033,2037,2043,2057,2061,2087,2095,2099,2111,2119,2085,166,167,163,154,228,1797,173,157,155,156,229,174,190,171,169,255,159,227,258,168,257,260,256])).
% 59.51/59.61 cnf(2196,plain,
% 59.51/59.61 (P8(a17,a1,a19,a1,a1,a17,a19,a1)),
% 59.51/59.61 inference(scs_inference,[],[2093,2123,2051,2027,2047,2049,2160,2019,2021,2025,2033,2037,2043,2057,2061,2087,2095,2099,2111,2119,2085,166,167,163,154,228,1797,173,157,155,156,229,174,190,171,169,255,159,227,258,168,257,260,256,261])).
% 59.51/59.61 cnf(2202,plain,
% 59.51/59.61 (P4(a17,a19,a1,a19)),
% 59.51/59.61 inference(scs_inference,[],[2093,2123,2051,2027,2047,2049,2160,2019,2021,2025,2033,2037,2043,2057,2061,2087,2095,2099,2111,2119,2085,166,167,163,154,228,1797,173,157,155,156,229,174,190,171,169,255,159,227,258,168,257,260,256,261,259,262,170])).
% 59.51/59.61 cnf(2208,plain,
% 59.51/59.61 (P10(f31(a15,a16,a16,a16,a2),a16,a15,a16)),
% 59.51/59.61 inference(scs_inference,[],[2093,2123,2051,2027,2047,2049,2160,2019,2021,2025,2033,2037,2043,2057,2061,2087,2095,2099,2111,2119,2085,166,167,163,154,228,1797,173,157,155,156,229,174,190,171,169,255,159,227,258,168,257,260,256,261,259,262,170,202,203,204])).
% 59.51/59.61 cnf(2220,plain,
% 59.51/59.61 (P2(a2,a16,a16,a16)),
% 59.51/59.61 inference(scs_inference,[],[2093,2123,2017,2051,2027,2047,2049,2160,2019,2021,2025,2033,2037,2043,2057,2061,2087,2095,2099,2111,2119,2067,2085,166,167,163,154,228,1797,173,157,155,156,229,174,190,171,169,255,159,227,258,168,257,260,256,261,259,262,170,202,203,204,208,207,200,182,193,187])).
% 59.51/59.61 cnf(2226,plain,
% 59.51/59.61 (P6(a17,a17,a17,a17)),
% 59.51/59.61 inference(scs_inference,[],[2093,2123,2017,2051,2027,2047,2049,2160,2019,2021,2023,2025,2033,2037,2043,2057,2061,2087,2095,2099,2111,2119,2067,2085,166,167,163,154,228,1797,173,157,155,156,229,174,190,171,169,255,159,227,258,168,257,260,256,261,259,262,170,202,203,204,208,207,200,182,193,187,201,181,239])).
% 59.51/59.61 cnf(2233,plain,
% 59.51/59.61 (P9(a1,a17,a19,a19)),
% 59.51/59.61 inference(scs_inference,[],[2093,2123,2017,2051,2027,2047,2049,2160,2019,2021,2023,2025,2033,2037,2043,2057,2061,2087,2095,2099,2111,2119,2067,2085,166,167,163,154,228,1797,173,157,155,156,229,174,190,171,169,255,159,227,258,168,257,260,256,261,259,262,170,202,203,204,208,207,200,182,193,187,201,181,239,192,180,184])).
% 59.51/59.61 cnf(2235,plain,
% 59.51/59.61 (P3(f29(a17,a1,a17,a1,a19,a19),a17,a1)),
% 59.51/59.61 inference(scs_inference,[],[2093,2123,2017,2051,2027,2047,2049,2160,2019,2021,2023,2025,2033,2037,2043,2057,2061,2087,2095,2099,2111,2119,2067,2085,166,167,163,154,228,1797,173,157,155,156,229,174,190,171,169,255,159,227,258,168,257,260,256,261,259,262,170,202,203,204,208,207,200,182,193,187,201,181,239,192,180,184,206])).
% 59.51/59.61 cnf(2237,plain,
% 59.51/59.61 (P9(a2,a16,a16,a16)),
% 59.51/59.61 inference(scs_inference,[],[2093,2123,2017,2051,2027,2047,2049,2160,2019,2021,2023,2025,2033,2037,2043,2057,2061,2087,2095,2099,2111,2119,2067,2085,166,167,163,154,228,1797,173,157,155,156,229,174,190,171,169,255,159,227,258,168,257,260,256,261,259,262,170,202,203,204,208,207,200,182,193,187,201,181,239,192,180,184,206,245])).
% 59.51/59.61 cnf(2243,plain,
% 59.51/59.61 (P4(a16,a16,a16,a16)),
% 59.51/59.61 inference(scs_inference,[],[2093,2123,2017,2051,2027,2047,2049,2160,2019,2021,2023,2025,2033,2037,2043,2057,2061,2087,2095,2099,2111,2119,2067,2085,166,167,163,154,228,1797,173,157,155,156,229,174,190,171,169,255,159,227,258,168,257,260,256,261,259,262,170,202,203,204,208,207,200,182,193,187,201,181,239,192,180,184,206,245,226,199,254])).
% 59.51/59.61 cnf(2245,plain,
% 59.51/59.61 (P6(a1,a17,a1,a1)),
% 59.51/59.61 inference(scs_inference,[],[2093,2123,2017,2051,2027,2047,2049,2160,2019,2021,2023,2025,2033,2037,2043,2057,2061,2087,2095,2099,2111,2119,2067,2085,166,167,163,154,228,1797,173,157,155,156,229,174,190,171,169,255,159,227,258,168,257,260,256,261,259,262,170,202,203,204,208,207,200,182,193,187,201,181,239,192,180,184,206,245,226,199,254,172])).
% 59.51/59.61 cnf(2257,plain,
% 59.51/59.61 (P10(x22571,x22572,x22571,x22572)),
% 59.51/59.61 inference(scs_inference,[],[2093,2123,2017,2051,2027,2047,2049,2160,2019,2021,2023,2025,2033,2037,2043,2057,2061,2071,2087,2095,2099,2111,2119,2067,2085,1817,166,167,163,154,228,1797,173,157,155,156,229,174,190,171,169,255,159,227,258,168,257,260,256,261,259,262,170,202,203,204,208,207,200,182,193,187,201,181,239,192,180,184,206,245,226,199,254,172,236,303,191,248,252,243])).
% 59.51/59.61 cnf(2259,plain,
% 59.51/59.61 (P9(a16,a16,a16,a16)),
% 59.51/59.61 inference(scs_inference,[],[2093,2123,2017,2051,2027,2047,2049,2160,2019,2021,2023,2025,2033,2037,2043,2057,2061,2071,2087,2095,2099,2111,2119,2067,2085,1817,166,167,163,154,228,1797,173,157,155,156,229,174,190,171,169,255,159,227,258,168,257,260,256,261,259,262,170,202,203,204,208,207,200,182,193,187,201,181,239,192,180,184,206,245,226,199,254,172,236,303,191,248,252,243,198])).
% 59.51/59.61 cnf(2269,plain,
% 59.51/59.61 (P5(x22691,x22692,x22693,x22694,x22691,x22692,x22693,x22694)),
% 59.51/59.61 inference(scs_inference,[],[2257,2109,166,228])).
% 59.51/59.61 cnf(2271,plain,
% 59.51/59.61 (P1(a17,a19,a1)),
% 59.51/59.61 inference(scs_inference,[],[2257,2109,2166,166,228,154])).
% 59.51/59.61 cnf(2273,plain,
% 59.51/59.61 (P5(x22731,x22732,x22731,x22732,a1,a1,a1,a1)),
% 59.51/59.61 inference(scs_inference,[],[2257,2109,2166,2180,166,228,154,1797])).
% 59.51/59.61 cnf(2275,plain,
% 59.51/59.61 (P10(x22751,x22752,x22752,x22751)),
% 59.51/59.61 inference(scs_inference,[],[2257,2109,2166,2180,166,228,154,1797,167])).
% 59.51/59.61 cnf(2277,plain,
% 59.51/59.61 (P1(x22771,x22772,x22772)),
% 59.51/59.61 inference(scs_inference,[],[2257,2109,2166,2180,166,228,154,1797,167,163])).
% 59.51/59.61 cnf(2285,plain,
% 59.51/59.61 (P6(a1,a1,a17,a1)),
% 59.51/59.61 inference(scs_inference,[],[2257,2109,2166,2180,2089,2220,2245,2235,166,228,154,1797,167,163,155,190,157,173])).
% 59.51/59.61 cnf(2289,plain,
% 59.51/59.61 (P10(f7(a16,a16,a16,a2),a16,a16,a15)),
% 59.51/59.61 inference(scs_inference,[],[2257,2121,2109,2166,2180,2089,2220,2245,2235,166,228,154,1797,167,163,155,190,157,173,229,303])).
% 59.51/59.61 cnf(2293,plain,
% 59.51/59.61 (P9(a15,a16,a2,a16)),
% 59.51/59.61 inference(scs_inference,[],[2257,2121,2109,2166,2180,2089,2188,2220,2245,2164,2235,166,228,154,1797,167,163,155,190,157,173,229,303,156,169])).
% 59.51/59.61 cnf(2297,plain,
% 59.51/59.61 (P4(a15,a16,a16,a15)),
% 59.51/59.61 inference(scs_inference,[],[2257,2121,2109,2166,2180,2089,2188,2220,2245,2164,2235,166,228,154,1797,167,163,155,190,157,173,229,303,156,169,174,171])).
% 59.51/59.61 cnf(2305,plain,
% 59.51/59.61 (P9(a2,a16,a16,a15)),
% 59.51/59.61 inference(scs_inference,[],[2257,2121,2113,2117,2109,2178,2166,2180,2089,2188,2220,2245,2164,2235,166,228,154,1797,167,163,155,190,157,173,229,303,156,169,174,171,255,227,257,168])).
% 59.51/59.61 cnf(2311,plain,
% 59.51/59.61 (P5(a17,a17,a19,a19,x23111,x23112,x23111,x23112)),
% 59.51/59.61 inference(scs_inference,[],[2257,2097,2121,2113,2117,2109,2178,2166,2157,2180,2089,2188,2220,2245,2164,2235,166,228,154,1797,167,163,155,190,157,173,229,303,156,169,174,171,255,227,257,168,159,260,258])).
% 59.51/59.61 cnf(2340,plain,
% 59.51/59.61 (P2(f8(a16,a16,a16),a16,a16,a16)),
% 59.51/59.61 inference(scs_inference,[],[2257,2097,2184,2121,2113,2117,2109,2178,2259,2166,2157,2180,2190,2035,2089,2188,2192,2220,2243,2245,2065,2164,2235,2123,166,228,154,1797,167,163,155,190,157,173,229,303,156,169,174,171,255,227,257,168,159,260,258,256,259,262,261,170,249,204,196,202,179,243,203,191,194])).
% 59.51/59.61 cnf(2347,plain,
% 59.51/59.61 (P2(a15,a16,a16,a16)),
% 59.51/59.61 inference(scs_inference,[],[2257,2097,2184,2121,2113,2117,2109,2178,2259,2166,2157,2180,2190,2194,2035,2089,2188,2192,2220,2243,2245,2065,2164,2235,2023,2123,166,228,154,1797,167,163,155,190,157,173,229,303,156,169,174,171,255,227,257,168,159,260,258,256,259,262,261,170,249,204,196,202,179,243,203,191,194,200,239,187])).
% 59.51/59.61 cnf(2359,plain,
% 59.51/59.61 (P9(a15,a15,a16,a16)),
% 59.70/59.61 inference(scs_inference,[],[2257,2097,2184,2121,2113,2117,2109,2178,2259,2166,2157,2180,2190,2194,2035,2083,2089,2153,2188,2192,2220,2243,2245,2065,2164,2235,2023,2123,166,228,154,1797,167,163,155,190,157,173,229,303,156,169,174,171,255,227,257,168,159,260,258,256,259,262,261,170,249,204,196,202,179,243,203,191,194,200,239,187,201,193,181,192,180,184])).
% 59.70/59.61 cnf(2364,plain,
% 59.70/59.61 (P10(x23641,x23642,x23641,x23642)),
% 59.70/59.61 inference(rename_variables,[],[2257])).
% 59.70/59.61 cnf(2366,plain,
% 59.70/59.61 (P4(a17,a17,a17,a17)),
% 59.70/59.61 inference(scs_inference,[],[2257,2097,2184,2121,2113,2117,2109,2178,2259,2166,2157,2180,2190,2194,2035,2083,2089,2153,2188,2192,2220,2243,2245,2065,2164,2235,2023,2123,166,228,154,1797,167,163,155,190,157,173,229,303,156,169,174,171,255,227,257,168,159,260,258,256,259,262,261,170,249,204,196,202,179,243,203,191,194,200,239,187,201,193,181,192,180,184,226,231,254])).
% 59.70/59.61 cnf(2369,plain,
% 59.70/59.61 (P10(x23691,x23692,x23691,x23692)),
% 59.70/59.61 inference(rename_variables,[],[2257])).
% 59.70/59.61 cnf(2371,plain,
% 59.70/59.61 (P4(a16,a15,a15,a16)),
% 59.70/59.61 inference(scs_inference,[],[2257,2364,2097,2184,2121,2113,2117,2109,2178,2259,2166,2157,2180,2190,2194,2035,2083,2089,2153,2188,2192,2220,2243,2245,2065,2164,2235,2023,2123,166,228,154,1797,167,163,155,190,157,173,229,303,156,169,174,171,255,227,257,168,159,260,258,256,259,262,261,170,249,204,196,202,179,243,203,191,194,200,239,187,201,193,181,192,180,184,226,231,254,209,512])).
% 59.70/59.61 cnf(2373,plain,
% 59.70/59.61 (P6(a17,x23731,a17,a17)),
% 59.70/59.61 inference(scs_inference,[],[2257,2364,2097,2184,2121,2113,2117,2109,2178,2259,2166,2157,2180,2190,2194,2035,2083,2089,2153,2188,2192,2220,2243,2245,2065,2164,2235,2023,2123,166,228,154,1797,167,163,155,190,157,173,229,303,156,169,174,171,255,227,257,168,159,260,258,256,259,262,261,170,249,204,196,202,179,243,203,191,194,200,239,187,201,193,181,192,180,184,226,231,254,209,512,172])).
% 59.70/59.61 cnf(2379,plain,
% 59.70/59.61 (P4(a1,a17,a1,a17)),
% 59.70/59.61 inference(scs_inference,[],[2257,2364,2097,2184,2121,2113,2117,2109,2178,2259,2166,2157,2180,2190,2194,2035,2083,2089,2153,2188,2192,2220,2243,2245,2065,2164,2235,929,2071,2023,2123,166,228,154,1797,167,163,155,190,157,173,229,303,156,169,174,171,255,227,257,168,159,260,258,256,259,262,261,170,249,204,196,202,179,243,203,191,194,200,239,187,201,193,181,192,180,184,226,231,254,209,512,172,224,164,176])).
% 59.70/59.61 cnf(2382,plain,
% 59.70/59.61 (P5(a17,a17,a17,a17,x23821,x23822,x23821,x23822)),
% 59.70/59.61 inference(rename_variables,[],[2186])).
% 59.70/59.61 cnf(2384,plain,
% 59.70/59.61 (P9(a17,a17,a17,a17)),
% 59.70/59.61 inference(scs_inference,[],[2257,2364,2097,2184,2121,2113,2117,2109,2178,2259,2166,2157,2180,2186,2382,2190,2194,2035,2083,2089,2153,2188,2192,2220,2243,2245,2065,2164,2235,929,2071,2023,2123,166,228,154,1797,167,163,155,190,157,173,229,303,156,169,174,171,255,227,257,168,159,260,258,256,259,262,261,170,249,204,196,202,179,243,203,191,194,200,239,187,201,193,181,192,180,184,226,231,254,209,512,172,224,164,176,248,244])).
% 59.70/59.61 cnf(2387,plain,
% 59.70/59.61 (P10(f29(a17,a17,a17,a17,a17,a17),a17,a17,a17)),
% 59.70/59.61 inference(scs_inference,[],[2257,2364,2097,2184,2121,2113,2117,2109,2178,2259,2166,2157,2180,2186,2382,2190,2194,2035,2083,2089,2153,2188,2192,2220,2243,2245,2065,2164,2235,929,2071,2023,2123,166,228,154,1797,167,163,155,190,157,173,229,303,156,169,174,171,255,227,257,168,159,260,258,256,259,262,261,170,249,204,196,202,179,243,203,191,194,200,239,187,201,193,181,192,180,184,226,231,254,209,512,172,224,164,176,248,244,208])).
% 59.70/59.61 cnf(2395,plain,
% 59.70/59.61 (P4(a19,a1,a19,a1)),
% 59.70/59.61 inference(scs_inference,[],[2257,2364,2097,2184,2121,2113,2053,2117,2109,2178,2259,2166,2157,2180,2186,2382,2190,2194,2035,2083,2089,2153,2188,2192,2220,2243,2245,2133,2065,2164,2235,929,2071,2023,2123,166,228,154,1797,167,163,155,190,157,173,229,303,156,169,174,171,255,227,257,168,159,260,258,256,259,262,261,170,249,204,196,202,179,243,203,191,194,200,239,187,201,193,181,192,180,184,226,231,254,209,512,172,224,164,176,248,244,208,232,230,206,246])).
% 59.70/59.61 cnf(2400,plain,
% 59.70/59.61 (P10(x24001,x24002,x24001,x24002)),
% 59.70/59.61 inference(rename_variables,[],[2257])).
% 59.70/59.61 cnf(2402,plain,
% 59.70/59.61 (P3(a17,x24021,x24021)),
% 59.70/59.61 inference(scs_inference,[],[2257,2364,2369,2400,2097,2184,2121,2113,2053,2117,2109,2178,2259,2166,2157,2180,2186,2382,2190,2194,2035,2083,2089,2153,2188,2192,2220,2226,2243,2245,2133,2065,2164,2235,929,2071,2023,2123,166,228,154,1797,167,163,155,190,157,173,229,303,156,169,174,171,255,227,257,168,159,260,258,256,259,262,261,170,249,204,196,202,179,243,203,191,194,200,239,187,201,193,181,192,180,184,226,231,254,209,512,172,224,164,176,248,244,208,232,230,206,246,189,195,178])).
% 59.70/59.61 cnf(2406,plain,
% 59.70/59.61 (P3(f26(a17,x24061),a17,x24061)),
% 59.70/59.61 inference(scs_inference,[],[2257,2364,2369,2400,2097,2184,2121,2113,2053,2117,2109,2178,2259,2166,2157,2180,2186,2382,2190,2194,2035,2083,2089,2153,2188,2192,2220,2226,2243,2245,2133,2065,2164,2235,929,2071,2023,2123,166,228,154,1797,167,163,155,190,157,173,229,303,156,169,174,171,255,227,257,168,159,260,258,256,259,262,261,170,249,204,196,202,179,243,203,191,194,200,239,187,201,193,181,192,180,184,226,231,254,209,512,172,224,164,176,248,244,208,232,230,206,246,189,195,178,162])).
% 59.70/59.61 cnf(2408,plain,
% 59.70/59.61 (P9(a19,a19,a17,a17)),
% 59.70/59.61 inference(scs_inference,[],[2257,2364,2369,2400,2097,2184,2121,2113,2053,2117,2109,2178,2259,2166,2157,2180,2186,2382,2190,2194,2035,2083,2089,2153,2188,2192,2220,2226,2243,2245,2133,2065,2164,2235,929,2071,2023,2123,166,228,154,1797,167,163,155,190,157,173,229,303,156,169,174,171,255,227,257,168,159,260,258,256,259,262,261,170,249,204,196,202,179,243,203,191,194,200,239,187,201,193,181,192,180,184,226,231,254,209,512,172,224,164,176,248,244,208,232,230,206,246,189,195,178,162,656])).
% 59.70/59.61 cnf(2420,plain,
% 59.70/59.61 (P10(a16,a2,a16,a16)),
% 59.70/59.61 inference(scs_inference,[],[2257,2364,2369,2400,2097,2184,2121,2113,2053,2117,2109,2178,2259,2166,2157,2180,2186,2382,2190,2194,2035,2083,2089,2153,2188,2192,2220,2226,2243,2245,2133,2065,2164,2235,929,2071,2023,2123,166,228,154,1797,167,163,155,190,157,173,229,303,156,169,174,171,255,227,257,168,159,260,258,256,259,262,261,170,249,204,196,202,179,243,203,191,194,200,239,187,201,193,181,192,180,184,226,231,254,209,512,172,224,164,176,248,244,208,232,230,206,246,189,195,178,162,656,741,701,759,918,1056,236])).
% 59.70/59.61 cnf(2426,plain,
% 59.70/59.61 (P3(a17,x24261,x24261)),
% 59.70/59.61 inference(rename_variables,[],[2402])).
% 59.70/59.61 cnf(2428,plain,
% 59.70/59.61 (P8(x24281,a1,a1,a1,x24281,a1,a1,a1)),
% 59.70/59.61 inference(scs_inference,[],[2277,2402,1058,1863])).
% 59.70/59.61 cnf(2429,plain,
% 59.70/59.61 (P1(x24291,x24292,x24292)),
% 59.70/59.61 inference(rename_variables,[],[2277])).
% 59.70/59.61 cnf(2431,plain,
% 59.70/59.61 (P10(a16,a16,a16,a2)),
% 59.70/59.61 inference(scs_inference,[],[2277,2402,2420,1058,1863,166])).
% 59.70/59.61 cnf(2434,plain,
% 59.70/59.61 (P3(a17,x24341,x24341)),
% 59.70/59.61 inference(rename_variables,[],[2402])).
% 59.70/59.61 cnf(2437,plain,
% 59.70/59.61 (P1(x24371,x24372,x24372)),
% 59.70/59.61 inference(rename_variables,[],[2277])).
% 59.70/59.61 cnf(2441,plain,
% 59.70/59.61 (P5(x24411,x24412,x24413,x24414,x24412,x24411,x24413,x24414)),
% 59.70/59.61 inference(scs_inference,[],[2275,2277,2429,2402,2426,2420,2208,1058,1863,166,1070,1866,167,228])).
% 59.70/59.61 cnf(2444,plain,
% 59.70/59.61 (P5(a17,a17,a19,a19,x24441,x24442,x24441,x24442)),
% 59.70/59.61 inference(rename_variables,[],[2311])).
% 59.70/59.61 cnf(2446,plain,
% 59.70/59.61 (P1(x24461,x24462,x24461)),
% 59.70/59.61 inference(scs_inference,[],[2275,2277,2429,2437,2402,2426,2311,2420,2208,1058,1863,166,1070,1866,167,228,1797,154])).
% 59.70/59.61 cnf(2448,plain,
% 59.70/59.61 (P1(a16,a16,a2)),
% 59.70/59.61 inference(scs_inference,[],[2275,2277,2429,2437,2402,2426,2311,2420,2208,1058,1863,166,1070,1866,167,228,1797,154,163])).
% 59.70/59.61 cnf(2456,plain,
% 59.70/59.61 (P1(a17,a1,a19)),
% 59.70/59.61 inference(scs_inference,[],[2275,2277,2429,2437,2402,2426,2311,2271,2347,2420,2406,2208,1058,1863,166,1070,1866,167,228,1797,154,163,157,156,190,155])).
% 59.70/59.61 cnf(2460,plain,
% 59.70/59.61 (P6(a17,a17,x24601,a17)),
% 59.70/59.61 inference(scs_inference,[],[2275,2277,2429,2437,2402,2426,2311,2373,2182,2271,2347,2420,2406,2208,1058,1863,166,1070,1866,167,228,1797,154,163,157,156,190,155,229,173])).
% 59.70/59.61 cnf(2462,plain,
% 59.70/59.61 (P9(a2,a16,a15,a16)),
% 59.70/59.61 inference(scs_inference,[],[2275,2277,2429,2437,2305,2402,2426,2311,2373,2182,2271,2347,2420,2406,2208,1058,1863,166,1070,1866,167,228,1797,154,163,157,156,190,155,229,173,169])).
% 59.70/59.61 cnf(2464,plain,
% 59.70/59.61 (P4(a19,a1,a17,a19)),
% 59.70/59.61 inference(scs_inference,[],[2275,2277,2429,2437,2305,2402,2426,2311,2373,2045,2182,2271,2347,2420,2406,2208,1058,1863,166,1070,1866,167,228,1797,154,163,157,156,190,155,229,173,169,171])).
% 59.70/59.61 cnf(2466,plain,
% 59.70/59.61 (P4(a17,x24661,a17,x24661)),
% 59.70/59.61 inference(scs_inference,[],[2275,2277,2429,2437,2305,2402,2426,2434,2311,2373,2045,2182,2271,2347,2420,2406,2208,1058,1863,166,1070,1866,167,228,1797,154,163,157,156,190,155,229,173,169,171,159])).
% 59.70/59.61 cnf(2472,plain,
% 59.70/59.61 (P9(a19,a19,a1,a17)),
% 59.70/59.61 inference(scs_inference,[],[2275,2277,2429,2437,2162,2233,2305,2402,2426,2434,2273,2311,2373,2045,2182,2271,2347,2420,2406,2208,1058,1863,166,1070,1866,167,228,1797,154,163,157,156,190,155,229,173,169,171,159,227,255,168])).
% 59.70/59.61 cnf(2474,plain,
% 59.70/59.61 (P5(x24741,x24742,x24742,x24741,a1,a1,a1,a1)),
% 59.70/59.61 inference(scs_inference,[],[2275,2277,2429,2437,2162,2233,2305,2402,2426,2434,2273,2311,2373,2045,2182,2271,2347,2420,2406,2208,1058,1863,166,1070,1866,167,228,1797,154,163,157,156,190,155,229,173,169,171,159,227,255,168,257])).
% 59.70/59.61 cnf(2478,plain,
% 59.70/59.61 (P5(x24781,x24782,x24781,x24782,x24783,x24784,x24783,x24784)),
% 59.70/59.61 inference(scs_inference,[],[2269,2275,2277,2429,2437,2162,2233,2305,2402,2426,2434,2273,2311,2373,2045,2182,2196,2271,2347,2420,2406,2208,1058,1863,166,1070,1866,167,228,1797,154,163,157,156,190,155,229,173,169,171,159,227,255,168,257,260,258])).
% 59.70/59.61 cnf(2482,plain,
% 59.70/59.61 (P8(a17,a1,a1,a17,a19,a1,a19,a1)),
% 59.70/59.61 inference(scs_inference,[],[2269,2275,2277,2429,2437,2162,2233,2305,2402,2426,2434,2273,2311,2373,2045,2182,2196,2271,2347,2420,2406,2208,1058,1863,166,1070,1866,167,228,1797,154,163,157,156,190,155,229,173,169,171,159,227,255,168,257,260,258,259,262])).
% 59.70/59.61 cnf(2495,plain,
% 59.70/59.61 (P5(x24951,x24952,x24953,x24954,x24951,x24952,x24953,x24954)),
% 59.70/59.61 inference(rename_variables,[],[2269])).
% 59.70/59.61 cnf(2501,plain,
% 59.70/59.61 (P10(f29(x25011,x25011,x25011,x25011,a17,a17),a17,x25011,x25011)),
% 59.70/59.61 inference(scs_inference,[],[2269,2275,2277,2429,2437,2384,2162,2233,2237,2305,2366,2402,2426,2434,2273,2311,2444,2373,2045,2069,2176,2182,2196,2271,2347,2420,2406,2208,2099,1058,1863,166,1070,1866,167,228,1797,154,163,157,156,190,155,229,173,169,171,159,227,255,168,257,260,258,259,262,256,261,170,204,197,249,196,179,207])).
% 59.70/59.61 cnf(2512,plain,
% 59.70/59.61 (P3(a17,x25121,x25121)),
% 59.70/59.61 inference(rename_variables,[],[2402])).
% 59.70/59.61 cnf(2516,plain,
% 59.70/59.61 (P10(a17,a17,x25161,x25161)),
% 59.70/59.61 inference(scs_inference,[],[2269,2275,2277,2429,2437,2384,2115,2162,2233,2237,2305,2366,2402,2426,2434,2273,2311,2444,2373,2045,2069,2176,2182,2196,2271,2347,2379,2420,2406,2208,2071,2099,1058,1863,166,1070,1866,167,228,1797,154,163,157,156,190,155,229,173,169,171,159,227,255,168,257,260,258,259,262,256,261,170,204,197,249,196,179,207,202,248,191,194,230,203,160])).
% 59.70/59.61 cnf(2518,plain,
% 59.70/59.61 (P6(x25181,x25182,x25182,x25182)),
% 59.70/59.61 inference(scs_inference,[],[2269,2495,2275,2277,2429,2437,2384,2115,2162,2233,2237,2305,2366,2402,2426,2434,2273,2311,2444,2373,2045,2069,2176,2182,2196,2271,2347,2379,2420,2406,2208,2071,2099,1058,1863,166,1070,1866,167,228,1797,154,163,157,156,190,155,229,173,169,171,159,227,255,168,257,260,258,259,262,256,261,170,204,197,249,196,179,207,202,248,191,194,230,203,160,239])).
% 59.70/59.61 cnf(2519,plain,
% 59.70/59.61 (P1(x25191,x25192,x25192)),
% 59.70/59.61 inference(rename_variables,[],[2277])).
% 59.70/59.61 cnf(2524,plain,
% 59.70/59.61 (P9(f12(a17,a17,a17,x25241,x25241),a17,x25241,x25241)),
% 59.70/59.61 inference(scs_inference,[],[2269,2495,2275,2277,2429,2437,2519,2384,2115,2162,2233,2237,2305,2366,2402,2426,2434,2273,2311,2444,2373,2045,2069,2155,2176,2182,2196,2271,2347,2379,2420,2406,2208,2071,2099,1058,1863,166,1070,1866,167,228,1797,154,163,157,156,190,155,229,173,169,171,159,227,255,168,257,260,258,259,262,256,261,170,204,197,249,196,179,207,202,248,191,194,230,203,160,239,200,201])).
% 59.70/59.61 cnf(2525,plain,
% 59.70/59.61 (P1(x25251,x25252,x25252)),
% 59.70/59.61 inference(rename_variables,[],[2277])).
% 59.70/59.61 cnf(2527,plain,
% 59.70/59.61 (P2(a17,a17,a17,a17)),
% 59.70/59.61 inference(scs_inference,[],[2269,2495,2275,2277,2429,2437,2519,2384,2115,2162,2233,2237,2305,2366,2402,2426,2434,2273,2311,2444,2373,2045,2069,2155,2176,2182,2196,2271,2347,2379,2420,2406,2208,2071,2099,1058,1863,166,1070,1866,167,228,1797,154,163,157,156,190,155,229,173,169,171,159,227,255,168,257,260,258,259,262,256,261,170,204,197,249,196,179,207,202,248,191,194,230,203,160,239,200,201,187])).
% 59.70/59.61 cnf(2539,plain,
% 59.70/59.61 (P3(f29(x25391,x25391,x25391,x25391,a17,a17),x25391,x25391)),
% 59.70/59.61 inference(scs_inference,[],[2269,2495,2275,2277,2429,2437,2519,2384,2115,2162,2233,2237,2293,2305,2366,2402,2426,2434,2512,2273,2311,2444,2373,2045,2069,2155,2176,2182,2196,2271,2347,2379,2420,2387,2406,2208,2071,2099,1058,1863,166,1070,1866,167,228,1797,154,163,157,156,190,155,229,173,169,171,159,227,255,168,257,260,258,259,262,256,261,170,204,197,249,196,179,207,202,248,191,194,230,203,160,239,200,201,187,193,181,180,185,192,206])).
% 59.70/59.61 cnf(2541,plain,
% 59.70/59.61 (P9(a17,a1,a19,a19)),
% 59.70/59.61 inference(scs_inference,[],[2269,2495,2275,2277,2429,2437,2519,2384,2115,2162,2233,2237,2293,2305,2366,2402,2426,2434,2512,2273,2311,2444,2373,2045,2069,2155,2176,2182,2196,2202,2271,2347,2379,2420,2387,2406,2208,2071,2099,1058,1863,166,1070,1866,167,228,1797,154,163,157,156,190,155,229,173,169,171,159,227,255,168,257,260,258,259,262,256,261,170,204,197,249,196,179,207,202,248,191,194,230,203,160,239,200,201,187,193,181,180,185,192,206,184])).
% 59.70/59.61 cnf(2545,plain,
% 59.70/59.61 (P8(a17,x25451,x25451,x25451,a17,x25451,x25451,x25451)),
% 59.70/59.61 inference(scs_inference,[],[2269,2495,2275,2277,2429,2437,2519,2384,2115,2162,2233,2237,2293,2305,2366,2402,2426,2434,2512,2273,2311,2444,2373,2045,2069,2155,2176,2182,2196,2202,2271,2347,2379,2420,2387,2406,2208,346,2071,2099,1058,1863,166,1070,1866,167,228,1797,154,163,157,156,190,155,229,173,169,171,159,227,255,168,257,260,258,259,262,256,261,170,204,197,249,196,179,207,202,248,191,194,230,203,160,239,200,201,187,193,181,180,185,192,206,184,246,226])).
% 59.70/59.61 cnf(2547,plain,
% 59.70/59.61 (P9(a16,a17,a17,a17)),
% 59.70/59.61 inference(scs_inference,[],[2269,2495,2275,2277,2429,2437,2519,2384,2115,2162,2233,2237,2293,2305,2366,2402,2426,2434,2512,2273,2311,2444,2373,2045,2069,2155,2176,2182,2196,2202,2271,2347,2379,2420,2387,2406,2208,346,2071,2099,1058,1863,166,1070,1866,167,228,1797,154,163,157,156,190,155,229,173,169,171,159,227,255,168,257,260,258,259,262,256,261,170,204,197,249,196,179,207,202,248,191,194,230,203,160,239,200,201,187,193,181,180,185,192,206,184,246,226,198])).
% 59.70/59.61 cnf(2550,plain,
% 59.70/59.61 (P3(a17,x25501,x25501)),
% 59.70/59.61 inference(rename_variables,[],[2402])).
% 59.70/59.61 cnf(2553,plain,
% 59.70/59.61 (P1(x25531,x25532,x25532)),
% 59.70/59.61 inference(rename_variables,[],[2277])).
% 59.70/59.61 cnf(2554,plain,
% 59.70/59.61 (P3(a17,x25541,x25541)),
% 59.70/59.61 inference(rename_variables,[],[2402])).
% 59.70/59.61 cnf(2555,plain,
% 59.70/59.61 (P10(x25551,x25552,x25552,x25551)),
% 59.70/59.61 inference(rename_variables,[],[2275])).
% 59.70/59.61 cnf(2556,plain,
% 59.70/59.61 (P10(x25561,x25562,x25561,x25562)),
% 59.70/59.61 inference(rename_variables,[],[2257])).
% 59.70/59.61 cnf(2559,plain,
% 59.70/59.61 (P3(a17,x25591,x25591)),
% 59.70/59.61 inference(rename_variables,[],[2402])).
% 59.70/59.61 cnf(2563,plain,
% 59.70/59.61 (P3(f26(x25631,x25632),x25631,x25632)),
% 59.70/59.61 inference(scs_inference,[],[2269,2495,2275,2277,2429,2437,2519,2525,2553,2384,2115,2162,2233,2237,2293,2305,2366,2402,2426,2434,2512,2550,2554,2559,2273,2311,2444,2373,2045,2069,2155,2176,2182,2196,2202,2271,2347,2379,2420,2387,2406,2208,346,2071,2257,2556,366,2099,2259,1058,1863,166,1070,1866,167,228,1797,154,163,157,156,190,155,229,173,169,171,159,227,255,168,257,260,258,259,262,256,261,170,204,197,249,196,179,207,202,248,191,194,230,203,160,239,200,201,187,193,181,180,185,192,206,184,246,226,198,189,211,212,162])).
% 59.70/59.61 cnf(2566,plain,
% 59.70/59.61 (P1(x25661,x25662,x25662)),
% 59.70/59.61 inference(rename_variables,[],[2277])).
% 59.70/59.61 cnf(2568,plain,
% 59.70/59.61 (P4(a17,a17,a15,a15)),
% 59.70/59.61 inference(scs_inference,[],[2269,2495,2275,2277,2429,2437,2519,2525,2553,2384,2115,2162,2233,2237,2293,2305,2366,2402,2426,2434,2512,2550,2554,2559,2273,2311,2444,2373,2045,2069,2155,2176,2182,2196,2202,2271,2347,2379,2420,2387,2406,2208,346,2186,2071,2257,2556,366,2099,2259,1058,1863,166,1070,1866,167,228,1797,154,163,157,156,190,155,229,173,169,171,159,227,255,168,257,260,258,259,262,256,261,170,204,197,249,196,179,207,202,248,191,194,230,203,160,239,200,201,187,193,181,180,185,192,206,184,246,226,198,189,211,212,162,254])).
% 59.70/59.61 cnf(2572,plain,
% 59.70/59.61 (P10(x25721,x25722,x25722,x25721)),
% 59.70/59.61 inference(rename_variables,[],[2275])).
% 59.70/59.61 cnf(2579,plain,
% 59.70/59.61 (~P9(a1,f26(a18,a20),a18,a20)),
% 59.70/59.61 inference(scs_inference,[],[142,2269,2495,2275,2555,2572,2277,2429,2437,2519,2525,2553,2566,2384,2115,2162,2233,2237,2293,2305,2366,2402,2426,2434,2512,2550,2554,2559,2273,2311,2444,2373,2045,2069,2155,2176,2182,2196,2202,2271,2347,2379,2420,2387,2406,2208,346,2019,2186,2071,2257,2556,366,2099,2259,1058,1863,166,1070,1866,167,228,1797,154,163,157,156,190,155,229,173,169,171,159,227,255,168,257,260,258,259,262,256,261,170,204,197,249,196,179,207,202,248,191,194,230,203,160,239,200,201,187,193,181,180,185,192,206,184,246,226,198,189,211,212,162,254,210,209,299])).
% 59.70/59.61 cnf(2585,plain,
% 59.70/59.61 (P6(x25851,x25852,x25851,x25851)),
% 59.70/59.61 inference(scs_inference,[],[142,2269,2495,2275,2555,2572,2277,2429,2437,2519,2525,2553,2566,2384,2115,2162,2233,2237,2293,2305,2366,2402,2426,2434,2512,2550,2554,2559,2273,2311,2444,2373,2045,2069,2155,2176,2182,2196,2202,2271,2347,2379,2420,2387,2406,2208,346,2019,2186,2071,2257,2556,366,2099,2259,1058,1863,166,1070,1866,167,228,1797,154,163,157,156,190,155,229,173,169,171,159,227,255,168,257,260,258,259,262,256,261,170,204,197,249,196,179,207,202,248,191,194,230,203,160,239,200,201,187,193,181,180,185,192,206,184,246,226,198,189,211,212,162,254,210,209,299,677,1828,172])).
% 59.70/59.61 cnf(2627,plain,
% 59.70/59.61 (P3(f26(x26271,x26272),x26271,x26272)),
% 59.70/59.61 inference(rename_variables,[],[2563])).
% 59.70/59.61 cnf(2630,plain,
% 59.70/59.61 (P3(f26(x26301,x26302),x26301,x26302)),
% 59.70/59.61 inference(rename_variables,[],[2563])).
% 59.70/59.61 cnf(2633,plain,
% 59.70/59.61 (P1(x26331,x26332,x26331)),
% 59.70/59.61 inference(rename_variables,[],[2446])).
% 59.70/59.61 cnf(2639,plain,
% 59.70/59.61 (P1(x26391,x26392,x26391)),
% 59.70/59.61 inference(rename_variables,[],[2446])).
% 59.70/59.61 cnf(2642,plain,
% 59.70/59.61 (P3(f26(x26421,x26422),x26421,x26422)),
% 59.70/59.61 inference(rename_variables,[],[2563])).
% 59.70/59.61 cnf(2645,plain,
% 59.70/59.61 (P1(x26451,x26452,x26451)),
% 59.70/59.61 inference(rename_variables,[],[2446])).
% 59.70/59.61 cnf(2648,plain,
% 59.70/59.61 (P4(a17,x26481,a17,x26481)),
% 59.70/59.61 inference(rename_variables,[],[2466])).
% 59.70/59.61 cnf(2650,plain,
% 59.70/59.61 (P10(a16,a16,a2,a16)),
% 59.70/59.61 inference(scs_inference,[],[2446,2633,2639,2466,2431,2563,2627,2630,2501,675,1703,789,660,1146,1058,1828,759,167])).
% 59.70/59.61 cnf(2652,plain,
% 59.70/59.61 (P10(x26521,x26521,a17,a17)),
% 59.70/59.61 inference(scs_inference,[],[2446,2633,2639,2466,2516,2431,2563,2627,2630,2501,675,1703,789,660,1146,1058,1828,759,167,166])).
% 59.70/59.61 cnf(2654,plain,
% 59.70/59.61 (P1(a1,a17,a19)),
% 59.70/59.61 inference(scs_inference,[],[2446,2633,2639,2466,2516,2431,2456,2563,2627,2630,2501,675,1703,789,660,1146,1058,1828,759,167,166,154])).
% 59.70/59.61 cnf(2657,plain,
% 59.70/59.61 (P5(x26571,x26572,x26571,x26572,x26573,x26574,x26573,x26574)),
% 59.70/59.61 inference(rename_variables,[],[2478])).
% 59.70/59.61 cnf(2663,plain,
% 59.70/59.61 (P3(f26(x26631,x26632),x26632,x26631)),
% 59.70/59.61 inference(scs_inference,[],[2478,2446,2633,2639,2466,2516,2431,2456,2527,2563,2627,2630,2642,2501,675,1703,789,660,1146,1058,1828,759,167,166,154,1797,228,190,157])).
% 59.70/59.61 cnf(2669,plain,
% 59.70/59.61 (P1(x26691,x26691,x26692)),
% 59.70/59.61 inference(scs_inference,[],[2478,2446,2633,2639,2645,2466,2648,2516,2460,2431,2456,2527,2563,2627,2630,2642,2501,675,1703,789,660,1146,1058,1828,759,167,166,154,1797,228,190,157,229,174,155])).
% 59.70/59.61 cnf(2671,plain,
% 59.70/59.61 (P1(f26(x26711,x26712),x26711,x26712)),
% 59.70/59.61 inference(scs_inference,[],[2478,2446,2633,2639,2645,2466,2648,2516,2460,2431,2456,2527,2563,2627,2630,2642,2501,675,1703,789,660,1146,1058,1828,759,167,166,154,1797,228,190,157,229,174,155,156])).
% 59.70/59.61 cnf(2673,plain,
% 59.70/59.61 (P6(x26731,x26731,x26732,x26731)),
% 59.70/59.61 inference(scs_inference,[],[2478,2585,2446,2633,2639,2645,2466,2648,2516,2460,2431,2456,2527,2563,2627,2630,2642,2501,675,1703,789,660,1146,1058,1828,759,167,166,154,1797,228,190,157,229,174,155,156,173])).
% 59.70/59.61 cnf(2675,plain,
% 59.70/59.61 (P4(a16,a15,a16,a15)),
% 59.70/59.61 inference(scs_inference,[],[2478,2585,2446,2633,2639,2645,2371,2466,2648,2516,2460,2431,2456,2527,2563,2627,2630,2642,2501,675,1703,789,660,1146,1058,1828,759,167,166,154,1797,228,190,157,229,174,155,156,173,171])).
% 59.70/59.61 cnf(2681,plain,
% 59.70/59.61 (P4(f26(x26811,x26812),x26811,f26(x26811,x26812),x26812)),
% 59.70/59.61 inference(scs_inference,[],[2478,2585,2446,2633,2639,2645,2371,2466,2648,2474,2516,2460,2431,2456,2472,2527,2563,2627,2630,2642,2501,675,1703,789,660,1146,1058,1828,759,167,166,154,1797,228,190,157,229,174,155,156,173,171,255,169,159])).
% 59.70/59.61 cnf(2687,plain,
% 59.70/59.61 (P5(x26871,x26872,x26872,x26871,x26873,x26874,x26873,x26874)),
% 59.70/59.61 inference(scs_inference,[],[2441,2478,2585,2446,2633,2639,2645,2371,2408,2482,2466,2648,2474,2516,2460,2431,2456,2472,2527,2563,2627,2630,2642,2501,675,1703,789,660,1146,1058,1828,759,167,166,154,1797,228,190,157,229,174,155,156,173,171,255,169,159,168,259,258])).
% 59.70/59.61 cnf(2693,plain,
% 59.70/59.61 (P5(x26931,x26932,x26933,x26934,x26931,x26932,x26934,x26933)),
% 59.70/59.61 inference(scs_inference,[],[2441,2478,2585,2446,2633,2639,2645,2371,2408,2482,2466,2648,2474,2516,2460,2170,2431,2456,2472,2527,2563,2627,2630,2642,2501,675,1703,789,660,1146,1058,1828,759,167,166,154,1797,228,190,157,229,174,155,156,173,171,255,169,159,168,259,258,257,260,256])).
% 59.70/59.61 cnf(2695,plain,
% 59.70/59.61 (P8(a17,x26951,a17,x26951,x26951,x26951,x26951,x26951)),
% 59.70/59.61 inference(scs_inference,[],[2441,2478,2585,2446,2633,2639,2645,2371,2408,2482,2545,2466,2648,2474,2516,2460,2170,2431,2456,2472,2527,2563,2627,2630,2642,2501,675,1703,789,660,1146,1058,1828,759,167,166,154,1797,228,190,157,229,174,155,156,173,171,255,169,159,168,259,258,257,260,256,262])).
% 59.70/59.61 cnf(2697,plain,
% 59.70/59.61 (P8(x26971,a17,x26971,x26971,a17,x26971,x26971,x26971)),
% 59.70/59.61 inference(scs_inference,[],[2441,2478,2585,2446,2633,2639,2645,2371,2408,2482,2545,2466,2648,2474,2516,2460,2170,2431,2456,2472,2527,2563,2627,2630,2642,2501,675,1703,789,660,1146,1058,1828,759,167,166,154,1797,228,190,157,229,174,155,156,173,171,255,169,159,168,259,258,257,260,256,262,261])).
% 59.70/59.61 cnf(2702,plain,
% 59.70/59.61 (P5(x27021,x27022,x27023,x27024,x27022,x27021,x27023,x27024)),
% 59.70/59.61 inference(rename_variables,[],[2441])).
% 59.70/59.61 cnf(2705,plain,
% 59.70/59.61 (P5(x27051,x27052,x27051,x27052,x27053,x27054,x27053,x27054)),
% 59.70/59.61 inference(rename_variables,[],[2478])).
% 59.70/59.61 cnf(2707,plain,
% 59.70/59.61 (P10(f31(a16,a17,x27071,x27071,a17),x27071,a16,a17)),
% 59.70/59.61 inference(scs_inference,[],[2441,2478,2657,2585,2446,2633,2639,2645,2371,2408,2482,2545,2466,2648,2474,2516,2460,2170,2431,2456,2464,2472,2527,2547,2563,2627,2630,2642,2501,675,1703,789,660,1146,1058,1828,759,167,166,154,1797,228,190,157,229,174,155,156,173,171,255,169,159,168,259,258,257,260,256,262,261,170,253,250,204])).
% 59.70/59.61 cnf(2711,plain,
% 59.70/59.61 (P4(a16,a17,a16,a17)),
% 59.70/59.61 inference(scs_inference,[],[2441,2478,2657,2585,2446,2633,2639,2645,2371,2408,2482,2545,2466,2648,2474,2516,2460,2170,2431,2456,2464,2472,2527,2547,2563,2627,2630,2642,2501,2402,675,1703,789,660,1146,1058,1828,759,167,166,154,1797,228,190,157,229,174,155,156,173,171,255,169,159,168,259,258,257,260,256,262,261,170,253,250,204,243,176])).
% 59.70/59.61 cnf(2715,plain,
% 59.70/59.61 (P4(a17,x27151,a17,x27151)),
% 59.70/59.61 inference(rename_variables,[],[2466])).
% 59.70/59.61 cnf(2716,plain,
% 59.70/59.61 (P5(x27161,x27162,x27163,x27164,x27162,x27161,x27163,x27164)),
% 59.70/59.61 inference(rename_variables,[],[2441])).
% 59.70/59.61 cnf(2721,plain,
% 59.70/59.61 (P4(a17,x27211,a17,x27211)),
% 59.70/59.61 inference(rename_variables,[],[2466])).
% 59.70/59.61 cnf(2724,plain,
% 59.70/59.61 (P5(x27241,x27242,x27243,x27244,x27242,x27241,x27243,x27244)),
% 59.70/59.61 inference(rename_variables,[],[2441])).
% 59.70/59.61 cnf(2729,plain,
% 59.70/59.61 (P3(f26(x27291,x27292),x27291,x27292)),
% 59.70/59.61 inference(rename_variables,[],[2563])).
% 59.70/59.61 cnf(2732,plain,
% 59.70/59.61 (P6(x27321,x27322,x27322,x27322)),
% 59.70/59.61 inference(rename_variables,[],[2518])).
% 59.70/59.61 cnf(2736,plain,
% 59.70/59.61 (P2(a17,x27361,x27361,x27361)),
% 59.70/59.61 inference(scs_inference,[],[2441,2702,2716,2478,2657,2518,2585,2446,2633,2639,2645,2371,2408,2482,2545,2466,2648,2715,2721,2474,2516,2460,2170,2431,2456,2464,2472,2527,2541,2547,2563,2627,2630,2642,2501,2182,2402,2237,2243,675,1703,789,660,1146,1058,1828,759,167,166,154,1797,228,190,157,229,174,155,156,173,171,255,169,159,168,259,258,257,260,256,262,261,170,253,250,204,243,176,252,196,197,244,202,230,194,203,187])).
% 59.70/59.61 cnf(2739,plain,
% 59.70/59.61 (P1(x27391,x27392,x27391)),
% 59.70/59.61 inference(rename_variables,[],[2446])).
% 59.70/59.61 cnf(2741,plain,
% 59.70/59.61 (P6(a15,a15,a1,a2)),
% 59.70/59.61 inference(scs_inference,[],[142,2441,2702,2716,2478,2657,2705,2518,2585,2446,2633,2639,2645,2371,2408,2482,2545,2466,2648,2715,2721,2474,2516,2460,2170,2431,2456,2464,2472,2527,2541,2547,2563,2627,2630,2642,2501,2182,2402,2237,2243,675,1703,789,660,1146,1058,1828,759,167,166,154,1797,228,190,157,229,174,155,156,173,171,255,169,159,168,259,258,257,260,256,262,261,170,253,250,204,243,176,252,196,197,244,202,230,194,203,187,200,239])).
% 59.70/59.61 cnf(2742,plain,
% 59.70/59.61 (P5(x27421,x27422,x27421,x27422,x27423,x27424,x27423,x27424)),
% 59.70/59.61 inference(rename_variables,[],[2478])).
% 59.70/59.61 cnf(2747,plain,
% 59.70/59.61 (P1(x27471,x27472,x27471)),
% 59.70/59.61 inference(rename_variables,[],[2446])).
% 59.70/59.61 cnf(2752,plain,
% 59.70/59.61 (P3(f26(x27521,x27522),x27521,x27522)),
% 59.70/59.61 inference(rename_variables,[],[2563])).
% 59.70/59.61 cnf(2753,plain,
% 59.70/59.61 (P9(a15,f4(a15,a2,a16),a16,a2)),
% 59.70/59.61 inference(scs_inference,[],[142,2441,2702,2716,2478,2657,2705,2518,2585,2446,2633,2639,2645,2739,2371,2408,2482,2545,2466,2648,2715,2721,2474,2516,2460,2170,2431,2456,2462,2464,2472,2527,2541,2547,2563,2627,2630,2642,2729,2501,2182,2402,2293,2237,2243,267,675,1703,789,660,1146,1058,1828,759,167,166,154,1797,228,190,157,229,174,155,156,173,171,255,169,159,168,259,258,257,260,256,262,261,170,253,250,204,243,176,252,196,197,244,202,230,194,203,187,200,239,193,201,181,107,192])).
% 59.70/59.61 cnf(2756,plain,
% 59.70/59.61 (P10(x27561,x27562,x27562,x27561)),
% 59.70/59.61 inference(rename_variables,[],[2275])).
% 59.70/59.61 cnf(2760,plain,
% 59.70/59.61 (P9(a17,a17,x27601,x27601)),
% 59.70/59.61 inference(scs_inference,[],[142,2441,2702,2716,2478,2657,2705,2518,2585,2446,2633,2639,2645,2739,2371,2408,2482,2545,2466,2648,2715,2721,2474,2516,2460,2170,2431,2456,2462,2464,2472,2527,2541,2547,2563,2627,2630,2642,2729,2579,2501,2182,2402,2275,2293,2237,2243,267,675,1703,789,660,1146,1058,1828,759,167,166,154,1797,228,190,157,229,174,155,156,173,171,255,169,159,168,259,258,257,260,256,262,261,170,253,250,204,243,176,252,196,197,244,202,230,194,203,187,200,239,193,201,181,107,192,185,180,184])).
% 59.70/59.61 cnf(2767,plain,
% 59.70/59.61 (P3(f26(x27671,x27672),x27671,x27672)),
% 59.70/59.61 inference(rename_variables,[],[2563])).
% 59.70/59.61 cnf(2770,plain,
% 59.70/59.61 (P10(x27701,x27702,x27702,x27701)),
% 59.70/59.61 inference(rename_variables,[],[2275])).
% 59.70/59.61 cnf(2771,plain,
% 59.70/59.61 (P3(f26(x27711,x27712),x27711,x27712)),
% 59.70/59.61 inference(rename_variables,[],[2563])).
% 59.70/59.61 cnf(2772,plain,
% 59.70/59.61 (P6(x27721,x27722,x27722,x27722)),
% 59.70/59.61 inference(rename_variables,[],[2518])).
% 59.70/59.61 cnf(2774,plain,
% 59.70/59.61 (P3(a17,a17,f26(a17,a17))),
% 59.70/59.61 inference(scs_inference,[],[142,2441,2702,2716,2478,2657,2705,2518,2732,2585,2446,2633,2639,2645,2739,2371,2408,2482,2545,2466,2648,2715,2721,2474,2516,2460,2170,2431,2456,2462,2464,2472,2527,2541,2547,2563,2627,2630,2642,2729,2752,2767,2771,2579,2501,2395,2182,2402,2275,2756,2770,2293,2237,2243,2384,267,675,1703,789,660,1146,1058,1828,759,167,166,154,1797,228,190,157,229,174,155,156,173,171,255,169,159,168,259,258,257,260,256,262,261,170,253,250,204,243,176,252,196,197,244,202,230,194,203,187,200,239,193,201,181,107,192,185,180,184,246,226,189,195,165])).
% 59.70/59.61 cnf(2775,plain,
% 59.70/59.61 (P10(x27751,x27752,x27752,x27751)),
% 59.70/59.61 inference(rename_variables,[],[2275])).
% 59.70/59.61 cnf(2780,plain,
% 59.70/59.61 (P4(x27801,x27801,x27801,x27801)),
% 59.70/59.61 inference(scs_inference,[],[142,2441,2702,2716,2724,2478,2657,2705,2518,2732,2772,2585,2446,2633,2639,2645,2739,2371,2408,2482,2545,2466,2648,2715,2721,2474,2516,2460,2170,2431,2456,2462,2464,2472,2527,2541,2547,2563,2627,2630,2642,2729,2752,2767,2771,2579,2501,2149,2395,2182,2402,2275,2756,2770,2293,2237,2243,2384,146,283,267,675,1703,789,660,1146,1058,1828,759,167,166,154,1797,228,190,157,229,174,155,156,173,171,255,169,159,168,259,258,257,260,256,262,261,170,253,250,204,243,176,252,196,197,244,202,230,194,203,187,200,239,193,201,181,107,192,185,180,184,246,226,189,195,165,212,254])).
% 59.70/59.61 cnf(2787,plain,
% 59.70/59.61 (P1(x27871,x27872,x27871)),
% 59.70/59.61 inference(rename_variables,[],[2446])).
% 59.70/59.61 cnf(2789,plain,
% 59.70/59.61 (P1(a19,x27891,f13(a1,a1,a19,a19,a19,x27891))),
% 59.70/59.61 inference(scs_inference,[],[142,2441,2702,2716,2724,2478,2657,2705,2518,2732,2772,2585,2446,2633,2639,2645,2739,2747,2787,2371,2408,2482,2545,2466,2648,2715,2721,2474,2516,2460,2170,2431,2448,2456,2462,2464,2472,2527,2541,2547,2563,2627,2630,2642,2729,2752,2767,2771,2579,2501,2149,2395,2277,2182,2402,2275,2756,2770,2775,2293,2237,2243,2384,146,283,267,675,1703,789,660,1146,1058,1828,759,167,166,154,1797,228,190,157,229,174,155,156,173,171,255,169,159,168,259,258,257,260,256,262,261,170,253,250,204,243,176,252,196,197,244,202,230,194,203,187,200,239,193,201,181,107,192,185,180,184,246,226,189,195,165,212,254,210,209])).
% 59.70/59.61 cnf(2790,plain,
% 59.70/59.61 (P1(x27901,x27902,x27901)),
% 59.70/59.61 inference(rename_variables,[],[2446])).
% 59.70/59.61 cnf(2791,plain,
% 59.70/59.61 (P1(x27911,x27912,x27912)),
% 59.70/59.61 inference(rename_variables,[],[2277])).
% 59.70/59.61 cnf(2806,plain,
% 59.70/59.61 (P9(x28061,x28061,x28061,x28061)),
% 59.70/59.61 inference(scs_inference,[],[142,2441,2702,2716,2724,2478,2657,2705,2518,2732,2772,2585,2446,2633,2639,2645,2739,2747,2787,2371,2408,2482,2545,2466,2648,2715,2721,2474,2516,2460,2170,2431,2448,2456,2462,2464,2472,2527,2541,2547,2563,2627,2630,2642,2729,2752,2767,2771,2579,2501,2149,2395,356,2277,2791,2182,2402,2275,2756,2770,2775,2293,2237,2243,2384,146,283,267,675,1703,789,660,1146,1058,1828,759,167,166,154,1797,228,190,157,229,174,155,156,173,171,255,169,159,168,259,258,257,260,256,262,261,170,253,250,204,243,176,252,196,197,244,202,230,194,203,187,200,239,193,201,181,107,192,185,180,184,246,226,189,195,165,212,254,210,209,2,1062,741,656,701,303,225,175])).
% 59.70/59.61 cnf(2809,plain,
% 59.70/59.61 (P4(a1,a1,a1,f3(a1,a1,a1))),
% 59.70/59.61 inference(scs_inference,[],[142,2441,2702,2716,2724,2478,2657,2705,2518,2732,2772,2585,2446,2633,2639,2645,2739,2747,2787,2371,2408,2482,2545,2466,2648,2715,2721,2474,2516,2460,2170,2431,2448,2456,2462,2464,2472,2527,2541,2547,2563,2627,2630,2642,2729,2752,2767,2771,2579,2501,2149,2395,356,2277,2791,2182,2402,2275,2756,2770,2775,2293,2237,2243,2384,146,283,267,675,1703,789,660,1146,1058,1828,759,167,166,154,1797,228,190,157,229,174,155,156,173,171,255,169,159,168,259,258,257,260,256,262,261,170,253,250,204,243,176,252,196,197,244,202,230,194,203,187,200,239,193,201,181,107,192,185,180,184,246,226,189,195,165,212,254,210,209,2,1062,741,656,701,303,225,175,191])).
% 59.70/59.61 cnf(2811,plain,
% 59.70/59.61 (P9(a17,a1,a1,a1)),
% 59.70/59.61 inference(scs_inference,[],[142,2441,2702,2716,2724,2478,2657,2705,2518,2732,2772,2585,2446,2633,2639,2645,2739,2747,2787,2371,2408,2285,2482,2545,2466,2648,2715,2721,2474,2516,2460,2170,2431,2448,2456,2462,2464,2472,2527,2541,2547,2563,2627,2630,2642,2729,2752,2767,2771,2579,2501,2149,2395,356,2277,2791,2182,2402,2275,2756,2770,2775,2293,2237,2379,2243,2384,146,283,267,675,1703,789,660,1146,1058,1828,759,167,166,154,1797,228,190,157,229,174,155,156,173,171,255,169,159,168,259,258,257,260,256,262,261,170,253,250,204,243,176,252,196,197,244,202,230,194,203,187,200,239,193,201,181,107,192,185,180,184,246,226,189,195,165,212,254,210,209,2,1062,741,656,701,303,225,175,191,198])).
% 59.70/59.61 cnf(2813,plain,
% 59.70/59.61 (P3(a16,a16,a16)),
% 59.70/59.61 inference(scs_inference,[],[142,2441,2702,2716,2724,2478,2657,2705,2742,2518,2732,2772,2585,2446,2633,2639,2645,2739,2747,2787,2790,2371,2408,2285,2482,2545,2466,2648,2715,2721,2474,2516,2460,2170,2431,2448,2456,2462,2464,2472,2527,2541,2547,2563,2627,2630,2642,2729,2752,2767,2771,2579,2501,2340,2149,2395,356,2277,2791,2182,2402,2275,2756,2770,2775,2293,2237,2379,2243,2384,146,283,267,675,1703,789,660,1146,1058,1828,759,167,166,154,1797,228,190,157,229,174,155,156,173,171,255,169,159,168,259,258,257,260,256,262,261,170,253,250,204,243,176,252,196,197,244,202,230,194,203,187,200,239,193,201,181,107,192,185,180,184,246,226,189,195,165,212,254,210,209,2,1062,741,656,701,303,225,175,191,198,242])).
% 59.70/59.61 cnf(2823,plain,
% 59.70/59.61 (P4(f26(x28231,x28232),x28231,f26(x28231,x28232),x28232)),
% 59.70/59.61 inference(rename_variables,[],[2681])).
% 59.70/59.61 cnf(2826,plain,
% 59.70/59.61 (P4(f26(x28261,x28262),x28261,f26(x28261,x28262),x28262)),
% 59.70/59.61 inference(rename_variables,[],[2681])).
% 59.70/59.61 cnf(2829,plain,
% 59.70/59.61 (P4(f26(x28291,x28292),x28291,f26(x28291,x28292),x28292)),
% 59.70/59.61 inference(rename_variables,[],[2681])).
% 59.70/59.61 cnf(2832,plain,
% 59.70/59.61 (P4(f26(x28321,x28322),x28321,f26(x28321,x28322),x28322)),
% 59.70/59.61 inference(rename_variables,[],[2681])).
% 59.70/59.61 cnf(2835,plain,
% 59.70/59.61 (P4(f26(x28351,x28352),x28351,f26(x28351,x28352),x28352)),
% 59.70/59.61 inference(rename_variables,[],[2681])).
% 59.70/59.61 cnf(2838,plain,
% 59.70/59.61 (P4(f26(x28381,x28382),x28381,f26(x28381,x28382),x28382)),
% 59.70/59.61 inference(rename_variables,[],[2681])).
% 59.70/59.61 cnf(2841,plain,
% 59.70/59.61 (P5(x28411,x28412,x28413,x28414,x28411,x28412,x28414,x28413)),
% 59.70/59.61 inference(rename_variables,[],[2693])).
% 59.70/59.61 cnf(2844,plain,
% 59.70/59.61 (P1(x28441,x28441,x28442)),
% 59.70/59.61 inference(rename_variables,[],[2669])).
% 59.70/59.61 cnf(2849,plain,
% 59.70/59.61 (P1(x28491,x28491,x28492)),
% 59.70/59.61 inference(rename_variables,[],[2669])).
% 59.70/59.61 cnf(2852,plain,
% 59.70/59.61 (P1(x28521,x28521,x28522)),
% 59.70/59.61 inference(rename_variables,[],[2669])).
% 59.70/59.61 cnf(2862,plain,
% 59.70/59.61 (P4(f26(x28621,x28622),x28621,f26(x28621,x28622),x28622)),
% 59.70/59.61 inference(rename_variables,[],[2681])).
% 59.70/59.61 cnf(2873,plain,
% 59.70/59.61 (P5(x28731,x28732,x28732,x28731,x28733,x28734,x28733,x28734)),
% 59.70/59.61 inference(rename_variables,[],[2687])).
% 59.70/59.61 cnf(2918,plain,
% 59.70/59.61 (P5(x29181,x29182,x29182,x29181,x29183,x29184,x29183,x29184)),
% 59.70/59.61 inference(rename_variables,[],[2687])).
% 59.70/59.61 cnf(2921,plain,
% 59.70/59.61 (P5(x29211,x29212,x29211,x29212,x29213,x29214,x29213,x29214)),
% 59.70/59.61 inference(rename_variables,[],[2478])).
% 59.70/59.61 cnf(2935,plain,
% 59.70/59.61 (P9(x29351,x29351,x29351,x29351)),
% 59.70/59.61 inference(rename_variables,[],[2806])).
% 59.70/59.61 cnf(2942,plain,
% 59.70/59.61 (P5(x29421,x29422,x29422,x29421,x29423,x29424,x29423,x29424)),
% 59.70/59.61 inference(rename_variables,[],[2687])).
% 59.70/59.61 cnf(2945,plain,
% 59.70/59.61 (P9(x29451,x29451,x29451,x29451)),
% 59.70/59.61 inference(rename_variables,[],[2806])).
% 59.70/59.61 cnf(2948,plain,
% 59.70/59.61 (P9(x29481,x29481,x29481,x29481)),
% 59.70/59.61 inference(rename_variables,[],[2806])).
% 59.70/59.61 cnf(2951,plain,
% 59.70/59.61 (P9(x29511,x29511,x29511,x29511)),
% 59.70/59.61 inference(rename_variables,[],[2806])).
% 59.70/59.61 cnf(2954,plain,
% 59.70/59.61 (P3(f26(x29541,x29542),x29542,x29541)),
% 59.70/59.61 inference(rename_variables,[],[2663])).
% 59.70/59.61 cnf(2957,plain,
% 59.70/59.61 (P4(x29571,x29571,x29571,x29571)),
% 59.70/59.61 inference(rename_variables,[],[2780])).
% 59.70/59.61 cnf(2960,plain,
% 59.70/59.61 (P6(x29601,x29601,x29602,x29601)),
% 59.70/59.61 inference(rename_variables,[],[2673])).
% 59.70/59.61 cnf(2971,plain,
% 59.70/59.61 (P1(x29711,x29711,x29712)),
% 59.70/59.61 inference(rename_variables,[],[2669])).
% 59.70/59.61 cnf(2976,plain,
% 59.70/59.61 (P9(x29761,x29761,x29761,x29761)),
% 59.70/59.61 inference(rename_variables,[],[2806])).
% 59.70/59.61 cnf(2983,plain,
% 59.70/59.61 (P9(x29831,x29831,x29831,x29831)),
% 59.70/59.61 inference(rename_variables,[],[2806])).
% 59.70/59.61 cnf(3003,plain,
% 59.70/59.61 ($false),
% 59.70/59.61 inference(scs_inference,[],[142,2780,2957,2806,2935,2945,2948,2951,2976,2983,2673,2960,2687,2873,2918,2942,2693,2841,2669,2844,2849,2852,2971,2039,2297,2359,2695,2697,2736,2652,2760,2428,2568,2650,2654,2675,2711,2741,2811,2813,2681,2823,2826,2829,2832,2835,2838,2862,2663,2954,2671,2289,2141,2524,2789,2707,2774,2753,2809,2539,2478,2921,2472,380,2045,2402,2257,2547,739,772,821,839,875,981,623,1146,741,789,1828,1058,701,656,759,166,167,154,228,1797,190,229,155,303,174,157,156,255,171,169,159,173,258,259,168,257,260,256,262,261,170,253,250,196,176,208,207,197,204,243,244,191,202,200,230,203,194,239,187,177,158,193,201,206,192,185,184,246,226,189,195,242,178]),
% 59.70/59.61 ['proof']).
% 59.70/59.61 % SZS output end Proof
% 59.70/59.61 % Total time :58.860000s
%------------------------------------------------------------------------------