%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : GEO547+1 : TPTP v8.2.0. Released v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% Computer : n023.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:41 EDT 2024
% Result : Theorem 59.45s 59.52s
% Output : CNFRefutation 59.61s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.06/0.12 % Problem : GEO547+1 : TPTP v8.2.0. Released v7.5.0.
% 0.06/0.12 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% 0.12/0.33 % Computer : n023.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 300
% 0.12/0.33 % DateTime : Fri Jun 21 08:14:39 EDT 2024
% 0.12/0.33 % CPUTime :
% 0.19/0.56 start to proof:theBenchmark
% 59.45/59.51 %-------------------------------------------
% 59.45/59.51 % File :CSE---1.7
% 59.45/59.51 % Problem :theBenchmark
% 59.45/59.51 % Transform :cnf
% 59.45/59.51 % Format :tptp:raw
% 59.45/59.51 % Command :java -jar mcs_scs.jar %d %s
% 59.45/59.51
% 59.45/59.51 % Result :Theorem 58.870000s
% 59.45/59.51 % Output :CNFRefutation 58.870000s
% 59.45/59.51 %-------------------------------------------
% 59.45/59.52 %------------------------------------------------------------------------------
% 59.45/59.52 % File : GEO547+1 : TPTP v8.2.0. Released v7.5.0.
% 59.45/59.52 % Domain : Geometry
% 59.45/59.52 % Problem : JGEX problem 07
% 59.45/59.52 % Version : [CGZ00] axioms.
% 59.45/59.52 % English :
% 59.45/59.52
% 59.45/59.52 % Refs : [CGZ00] Chou et al. (2000), A Deductive Database Approach to A
% 59.45/59.52 % : [YCG08] Ye et al. (2008), An Introduction to Java Geometry Exp
% 59.45/59.52 % : [Qua20] Quaresma (2020), Email to Geoff Sutcliffe
% 59.45/59.52 % Source : [Qua20]
% 59.45/59.52 % Names : 07.p [Qua20]
% 59.45/59.52
% 59.45/59.52 % Status : Theorem
% 59.45/59.52 % Rating : 0.22 v8.2.0, 0.19 v8.1.0, 0.25 v7.5.0
% 59.45/59.52 % Syntax : Number of formulae : 95 ( 0 unt; 0 def)
% 59.45/59.52 % Number of atoms : 292 ( 1 equ)
% 59.45/59.52 % Maximal formula atoms : 9 ( 3 avg)
% 59.45/59.52 % Number of connectives : 204 ( 7 ~; 0 |; 102 &)
% 59.45/59.52 % ( 0 <=>; 95 =>; 0 <=; 0 <~>)
% 59.45/59.52 % Maximal formula depth : 18 ( 9 avg)
% 59.45/59.52 % Maximal term depth : 1 ( 1 avg)
% 59.45/59.52 % Number of predicates : 12 ( 11 usr; 0 prp; 2-8 aty)
% 59.45/59.52 % Number of functors : 0 ( 0 usr; 0 con; --- aty)
% 59.45/59.52 % Number of variables : 531 ( 511 !; 20 ?)
% 59.45/59.52 % SPC : FOF_THM_RFO_SEQ
% 59.45/59.52
% 59.45/59.52 % Comments : Taken from JGEX [YCG08], converted by Pedro Quaresma.
% 59.45/59.52 %------------------------------------------------------------------------------
% 59.45/59.52 include('Axioms/GEO012+0.ax').
% 59.45/59.52 %------------------------------------------------------------------------------
% 59.45/59.52 fof(exemplo6GDDFULL012007,conjecture,
% 59.45/59.52 ! [A,B,C,O,D,E,F,G,NWPNT1] :
% 59.45/59.52 ( ( circle(O,A,B,C)
% 59.45/59.52 & circle(O,A,D,NWPNT1)
% 59.45/59.52 & perp(E,D,B,C)
% 59.45/59.52 & coll(E,B,C)
% 59.45/59.52 & perp(F,D,A,C)
% 59.45/59.52 & coll(F,A,C)
% 59.45/59.52 & perp(G,D,A,B)
% 59.45/59.52 & coll(G,A,B) )
% 59.45/59.52 => coll(E,F,G) ) ).
% 59.45/59.52
% 59.45/59.52 %------------------------------------------------------------------------------
% 59.45/59.52 %-------------------------------------------
% 59.45/59.52 % Proof found
% 59.45/59.52 % SZS status Theorem for theBenchmark
% 59.45/59.52 % SZS output start Proof
% 59.45/59.53 %ClaNum:263(EqnAxiom:141)
% 59.45/59.53 %VarNum:1613(SingletonVarNum:590)
% 59.45/59.53 %MaxLitNum:5
% 59.45/59.53 %MaxfuncDepth:1
% 59.45/59.53 %SharedTerms:18
% 59.45/59.53 %goalClause: 142 143 144 145 146 147 148 149 150
% 59.45/59.53 %singleGoalClaCount:9
% 59.45/59.53 [142]P1(a1,a2,a16)
% 59.45/59.53 [143]P1(a19,a3,a16)
% 59.45/59.53 [144]P1(a20,a3,a2)
% 59.45/59.53 [145]P3(a1,a17,a2,a16)
% 59.45/59.53 [146]P3(a19,a17,a3,a16)
% 59.45/59.53 [147]P3(a20,a17,a3,a2)
% 59.45/59.53 [148]P2(a18,a3,a2,a16)
% 59.45/59.53 [149]P2(a18,a3,a17,a21)
% 59.45/59.53 [150]~P1(a1,a19,a20)
% 59.45/59.53 [151]~P1(x1512,x1511,x1513)+P1(x1511,x1512,x1513)
% 59.45/59.53 [152]~P1(x1521,x1523,x1522)+P1(x1521,x1522,x1523)
% 59.45/59.53 [153]~P4(x1531,x1532,x1533)+P1(x1531,x1532,x1533)
% 59.45/59.53 [154]~P4(x1541,x1543,x1542)+P4(x1541,x1542,x1543)
% 59.45/59.53 [156]~P4(x1561,x1562,x1563)+P5(x1561,x1562,x1561,x1563)
% 59.45/59.53 [160]~P10(x1601,x1602,x1601,x1603)+P1(x1601,x1602,x1603)
% 59.45/59.53 [226]~P5(x2261,x2262,x2261,x2263)+P9(x2261,x2262,x2262,x2263,x2262,x2263,x2261,x2263)
% 59.45/59.53 [163]~P10(x1633,x1634,x1631,x1632)+P10(x1631,x1632,x1633,x1634)
% 59.45/59.53 [164]~P10(x1641,x1642,x1644,x1643)+P10(x1641,x1642,x1643,x1644)
% 59.45/59.53 [165]~P3(x1653,x1654,x1651,x1652)+P3(x1651,x1652,x1653,x1654)
% 59.45/59.53 [166]~P3(x1661,x1662,x1664,x1663)+P3(x1661,x1662,x1663,x1664)
% 59.45/59.53 [167]~P5(x1673,x1674,x1671,x1672)+P5(x1671,x1672,x1673,x1674)
% 59.45/59.53 [168]~P5(x1681,x1682,x1684,x1683)+P5(x1681,x1682,x1683,x1684)
% 59.45/59.53 [169]~P6(x1692,x1691,x1693,x1694)+P6(x1691,x1692,x1693,x1694)
% 59.45/59.53 [170]~P6(x1701,x1703,x1702,x1704)+P6(x1701,x1702,x1703,x1704)
% 59.45/59.53 [171]~P6(x1711,x1712,x1714,x1713)+P6(x1711,x1712,x1713,x1714)
% 59.45/59.53 [224]~P6(x2242,x2243,x2241,x2244)+P9(x2241,x2242,x2241,x2243,x2244,x2242,x2244,x2243)
% 59.45/59.53 [187]~P2(x1874,x1871,x1872,x1873)+P3(f8(x1871,x1872,x1873,x1874),x1871,x1871,x1874)
% 59.45/59.53 [202]P5(x2021,x2022,x2023,x2024)+~P7(x2021,x2022,x2025,x2023,x2024,x2026)
% 59.45/59.53 [214]~P11(x2144,x2145,x2146,x2141,x2142,x2143)+P11(x2141,x2142,x2143,x2144,x2145,x2146)
% 59.45/59.53 [215]~P11(x2152,x2151,x2153,x2155,x2154,x2156)+P11(x2151,x2152,x2153,x2154,x2155,x2156)
% 59.45/59.53 [216]~P11(x2161,x2163,x2162,x2164,x2166,x2165)+P11(x2161,x2162,x2163,x2164,x2165,x2166)
% 59.45/59.53 [217]~P7(x2174,x2175,x2176,x2171,x2172,x2173)+P7(x2171,x2172,x2173,x2174,x2175,x2176)
% 59.45/59.53 [218]~P7(x2182,x2181,x2183,x2185,x2184,x2186)+P7(x2181,x2182,x2183,x2184,x2185,x2186)
% 59.45/59.53 [219]~P7(x2191,x2193,x2192,x2194,x2196,x2195)+P7(x2191,x2192,x2193,x2194,x2195,x2196)
% 59.45/59.53 [225]~P10(x2251,x2252,x2255,x2256)+P9(x2251,x2252,x2253,x2254,x2255,x2256,x2253,x2254)
% 59.45/59.53 [231]~P11(x2311,x2312,x2313,x2314,x2315,x2316)+P9(x2311,x2312,x2312,x2313,x2314,x2315,x2315,x2316)
% 59.45/59.53 [232]~P11(x2321,x2322,x2323,x2324,x2325,x2326)+P8(x2321,x2322,x2321,x2323,x2324,x2325,x2324,x2326)
% 59.45/59.53 [233]~P9(x2331,x2332,x2335,x2336,x2333,x2334,x2335,x2336)+P10(x2331,x2332,x2333,x2334)
% 59.45/59.53 [252]~P9(x2525,x2526,x2527,x2528,x2521,x2522,x2523,x2524)+P9(x2521,x2522,x2523,x2524,x2525,x2526,x2527,x2528)
% 59.45/59.53 [253]~P9(x2533,x2534,x2531,x2532,x2537,x2538,x2535,x2536)+P9(x2531,x2532,x2533,x2534,x2535,x2536,x2537,x2538)
% 59.45/59.53 [254]~P9(x2542,x2541,x2543,x2544,x2545,x2546,x2547,x2548)+P9(x2541,x2542,x2543,x2544,x2545,x2546,x2547,x2548)
% 59.45/59.53 [255]~P9(x2551,x2552,x2555,x2556,x2553,x2554,x2557,x2558)+P9(x2551,x2552,x2553,x2554,x2555,x2556,x2557,x2558)
% 59.45/59.53 [256]~P8(x2565,x2566,x2567,x2568,x2561,x2562,x2563,x2564)+P8(x2561,x2562,x2563,x2564,x2565,x2566,x2567,x2568)
% 59.45/59.53 [257]~P8(x2573,x2574,x2571,x2572,x2577,x2578,x2575,x2576)+P8(x2571,x2572,x2573,x2574,x2575,x2576,x2577,x2578)
% 59.45/59.53 [258]~P8(x2582,x2581,x2583,x2584,x2585,x2586,x2587,x2588)+P8(x2581,x2582,x2583,x2584,x2585,x2586,x2587,x2588)
% 59.45/59.53 [259]~P8(x2591,x2592,x2595,x2596,x2593,x2594,x2597,x2598)+P8(x2591,x2592,x2593,x2594,x2595,x2596,x2597,x2598)
% 59.45/59.53 [161]~P1(x1611,x1612,x1613)+~P5(x1611,x1612,x1611,x1613)+P4(x1611,x1612,x1613)
% 59.45/59.53 [235]P5(x2351,x2352,x2351,x2353)+~P9(x2351,x2352,x2352,x2353,x2352,x2353,x2351,x2353)+P1(x2351,x2352,x2353)
% 59.45/59.53 [176]~P3(x1761,x1762,x1762,x1763)+~P5(x1762,x1761,x1762,x1763)+P1(x1761,x1762,f4(x1761,x1763,x1762))
% 59.45/59.53 [188]~P3(x1882,x1881,x1881,x1883)+~P5(x1881,x1882,x1881,x1883)+P5(x1881,x1882,x1881,f4(x1882,x1883,x1881))
% 59.45/59.53 [155]~P1(x1553,x1554,x1551)+P1(x1551,x1552,x1553)+~P1(x1553,x1554,x1552)
% 59.45/59.53 [172]~P2(x1724,x1721,x1722,x1723)+P3(x1721,x1722,x1722,x1723)+~P1(x1724,x1721,x1723)
% 59.45/59.53 [173]~P3(x1731,x1734,x1732,x1733)+P5(x1731,x1732,x1731,x1733)+~P4(x1734,x1732,x1733)
% 59.45/59.53 [174]~P3(x1741,x1743,x1743,x1744)+P5(x1741,x1742,x1743,x1742)+~P4(x1742,x1741,x1744)
% 59.45/59.53 [181]~P5(x1811,x1814,x1812,x1814)+~P5(x1811,x1813,x1812,x1813)+P3(x1811,x1812,x1813,x1814)
% 59.45/59.53 [184]~P5(x1841,x1842,x1841,x1844)+~P5(x1841,x1842,x1841,x1843)+P2(x1841,x1842,x1843,x1844)
% 59.45/59.53 [230]~P10(x2301,x2304,x2303,x2302)+~P6(x2301,x2304,x2303,x2302)+P9(x2301,x2302,x2303,x2302,x2303,x2302,x2303,x2304)
% 59.45/59.53 [234]~P9(x2341,x2343,x2341,x2344,x2342,x2343,x2342,x2344)+P1(x2341,x2342,x2343)+P6(x2343,x2344,x2341,x2342)
% 59.45/59.53 [236]~P1(x2363,x2364,x2362)+~P9(x2363,x2361,x2363,x2362,x2364,x2361,x2364,x2362)+P6(x2361,x2362,x2363,x2364)
% 59.45/59.53 [238]P3(x2381,x2382,x2383,x2384)+~P9(x2381,x2382,x2383,x2384,x2383,x2384,x2381,x2382)+P10(x2381,x2382,x2383,x2384)
% 59.45/59.53 [177]~P3(x1771,x1774,x1772,x1773)+~P3(x1772,x1774,x1771,x1773)+P1(f5(x1771,x1772,x1773),x1773,x1772)
% 59.45/59.53 [178]~P3(x1781,x1784,x1782,x1783)+~P3(x1782,x1784,x1781,x1783)+P1(f6(x1781,x1782,x1783),x1783,x1781)
% 59.45/59.53 [189]~P3(x1891,x1894,x1892,x1893)+~P3(x1892,x1894,x1891,x1893)+P3(x1891,f5(x1891,x1892,x1893),x1893,x1892)
% 59.45/59.53 [190]~P3(x1901,x1904,x1902,x1903)+~P3(x1902,x1904,x1901,x1903)+P3(x1901,f6(x1902,x1901,x1903),x1903,x1902)
% 59.45/59.53 [191]~P3(x1911,x1913,x1913,x1912)+~P6(x1911,x1912,x1913,x1914)+P2(f9(x1911,x1912,x1913),x1911,x1912,x1913)
% 59.45/59.53 [193]~P3(x1933,x1934,x1932,x1931)+~P5(x1933,x1932,x1933,x1931)+P1(x1931,x1932,f23(x1932,x1931,x1933,x1934))
% 59.45/59.53 [194]~P3(x1943,x1944,x1941,x1942)+~P5(x1943,x1941,x1943,x1942)+P1(f23(x1941,x1942,x1943,x1944),x1943,x1944)
% 59.45/59.53 [245]~P5(x2453,x2452,x2453,x2451)+~P9(x2452,x2453,x2453,x2454,x2453,x2454,x2453,x2451)+P1(x2451,x2452,f24(x2452,x2451,x2453,x2454))
% 59.45/59.53 [246]~P3(x2463,x2464,x2462,x2461)+~P9(x2462,x2463,x2463,x2464,x2463,x2464,x2463,x2461)+P1(x2461,x2462,f25(x2462,x2461,x2463,x2464))
% 59.45/59.53 [247]~P3(x2473,x2472,x2472,x2471)+~P9(x2474,x2473,x2472,x2473,x2472,x2473,x2471,x2473)+P1(f15(x2471,x2472,x2473,x2474),x2473,x2474)
% 59.45/59.53 [248]~P3(x2483,x2482,x2482,x2481)+~P9(x2484,x2483,x2482,x2483,x2482,x2483,x2481,x2483)+P1(f15(x2481,x2482,x2483,x2484),x2481,x2482)
% 59.45/59.53 [249]~P5(x2493,x2491,x2493,x2492)+~P9(x2491,x2493,x2493,x2494,x2493,x2494,x2493,x2492)+P1(f24(x2491,x2492,x2493,x2494),x2493,x2494)
% 59.45/59.53 [250]~P3(x2503,x2504,x2501,x2502)+~P9(x2501,x2503,x2503,x2504,x2503,x2504,x2503,x2502)+P1(f25(x2501,x2502,x2503,x2504),x2503,x2504)
% 59.45/59.53 [157]~P4(x1575,x1571,x1573)+P10(x1571,x1572,x1573,x1574)+~P4(x1575,x1572,x1574)
% 59.45/59.53 [158]~P4(x1581,x1585,x1583)+P10(x1581,x1582,x1583,x1584)+~P4(x1582,x1585,x1584)
% 59.45/59.53 [185]~P6(x1855,x1851,x1852,x1853)+P6(x1851,x1852,x1853,x1854)+~P6(x1855,x1851,x1852,x1854)
% 59.45/59.53 [227]~P4(x2275,x2272,x2273)+~P2(x2274,x2271,x2272,x2273)+P9(x2271,x2272,x2271,x2273,x2274,x2272,x2274,x2275)
% 59.45/59.53 [229]~P2(x2295,x2291,x2293,x2294)+P9(x2291,x2292,x2291,x2293,x2294,x2291,x2294,x2293)+~P3(x2295,x2291,x2291,x2292)
% 59.45/59.53 [242]~P9(x2422,x2423,x2422,x2424,x2425,x2422,x2425,x2424)+P3(x2421,x2422,x2422,x2423)+~P2(x2421,x2422,x2424,x2425)
% 59.45/59.53 [197]~P1(x1972,x1974,x1975)+~P3(x1971,x1973,x1973,x1972)+P1(f13(x1971,x1972,x1973,x1974,x1975),x1974,x1975)
% 59.45/59.53 [198]~P1(x1982,x1984,x1985)+~P3(x1981,x1983,x1983,x1982)+P3(f13(x1981,x1982,x1983,x1984,x1985),x1981,x1984,x1985)
% 59.45/59.53 [199]~P3(x1993,x1994,x1994,x1991)+~P5(x1991,x1992,x1991,x1995)+P5(x1991,x1992,x1991,f28(x1993,x1994,x1992,x1995,x1991))
% 59.45/59.53 [200]~P3(x2003,x2001,x2001,x2005)+~P5(x2005,x2002,x2005,x2004)+P5(x2001,x2002,x2001,f28(x2003,x2001,x2002,x2004,x2005))
% 59.45/59.53 [201]~P3(x2011,x2012,x2012,x2015)+~P5(x2015,x2013,x2015,x2014)+P10(f28(x2011,x2012,x2013,x2014,x2015),x2013,x2011,x2012)
% 59.45/59.53 [244]~P9(x2441,x2443,x2442,x2443,x2441,x2444,x2442,x2445)+P1(x2441,x2442,x2443)+P6(x2444,x2442,x2443,f27(x2441,x2442,x2443,x2444))
% 59.45/59.53 [260]~P9(x2601,x2603,x2602,x2603,x2601,x2604,x2602,x2605)+P1(x2601,x2602,x2603)+P9(x2601,x2603,x2602,x2603,x2601,f27(x2601,x2602,x2603,x2604),x2602,f27(x2601,x2602,x2603,x2604))
% 59.45/59.53 [179]~P10(x1791,x1792,x1795,x1796)+P10(x1791,x1792,x1793,x1794)+~P10(x1795,x1796,x1793,x1794)
% 59.45/59.53 [180]~P3(x1801,x1802,x1805,x1806)+P10(x1801,x1802,x1803,x1804)+~P3(x1805,x1806,x1803,x1804)
% 59.45/59.53 [182]~P3(x1825,x1826,x1823,x1824)+P3(x1821,x1822,x1823,x1824)+~P10(x1821,x1822,x1825,x1826)
% 59.45/59.53 [183]~P5(x1831,x1832,x1835,x1836)+P5(x1831,x1832,x1833,x1834)+~P5(x1835,x1836,x1833,x1834)
% 59.45/59.53 [220]~P5(x2201,x2202,x2204,x2205)+~P11(x2201,x2202,x2203,x2204,x2205,x2206)+P7(x2201,x2202,x2203,x2204,x2205,x2206)
% 59.45/59.53 [223]~P4(x2234,x2235,x2236)+~P4(x2231,x2232,x2233)+P8(x2231,x2232,x2232,x2233,x2234,x2235,x2235,x2236)
% 59.45/59.53 [203]~P4(x2036,x2033,x2034)+~P4(x2035,x2031,x2032)+P4(f26(x2031,x2032,x2033,x2034,x2035,x2036),x2031,x2034)
% 59.45/59.53 [204]~P4(x2046,x2043,x2044)+~P4(x2045,x2041,x2042)+P10(f26(x2041,x2042,x2043,x2044,x2045,x2046),x2046,x2041,x2043)
% 59.45/59.53 [205]~P4(x2056,x2053,x2054)+~P4(x2055,x2051,x2052)+P10(f26(x2051,x2052,x2053,x2054,x2055,x2056),x2055,x2052,x2054)
% 59.45/59.53 [240]~P9(x2401,x2402,x2403,x2404,x2405,x2406,x2407,x2408)+P10(x2401,x2402,x2403,x2404)+~P10(x2405,x2406,x2407,x2408)
% 59.45/59.53 [241]~P9(x2411,x2412,x2413,x2414,x2415,x2416,x2417,x2418)+P3(x2411,x2412,x2413,x2414)+~P3(x2415,x2416,x2417,x2418)
% 59.45/59.53 [243]~P8(x2431,x2432,x2433,x2434,x2435,x2436,x2437,x2438)+P5(x2431,x2432,x2433,x2434)+~P5(x2435,x2436,x2437,x2438)
% 59.45/59.53 [221]~P11(x2211,x2212,x2213,x2217,x2218,x2219)+P11(x2211,x2212,x2213,x2214,x2215,x2216)+~P11(x2217,x2218,x2219,x2214,x2215,x2216)
% 59.45/59.53 [222]~P7(x2221,x2222,x2223,x2227,x2228,x2229)+P7(x2221,x2222,x2223,x2224,x2225,x2226)+~P7(x2227,x2228,x2229,x2224,x2225,x2226)
% 59.45/59.53 [262]~P9(x2621,x2622,x2623,x2624,x2629,x26210,x26211,x26212)+P9(x2621,x2622,x2623,x2624,x2625,x2626,x2627,x2628)+~P9(x2629,x26210,x26211,x26212,x2625,x2626,x2627,x2628)
% 59.45/59.53 [263]~P8(x2631,x2632,x2633,x2634,x2639,x26310,x26311,x26312)+P8(x2631,x2632,x2633,x2634,x2635,x2636,x2637,x2638)+~P8(x2639,x26310,x26311,x26312,x2635,x2636,x2637,x2638)
% 59.45/59.53 [195]~P5(x1952,x1951,x1954,x1951)+~P6(x1952,x1954,x1951,x1953)+P3(x1951,x1952,x1952,x1953)+~P5(x1952,x1953,x1954,x1953)
% 59.45/59.53 [162]~P1(x1621,x1622,x1623)+~P10(x1624,x1621,x1625,x1623)+P4(x1621,x1622,x1623)+~P4(x1624,x1622,x1625)
% 59.45/59.53 [175]~P10(x1754,x1753,x1755,x1752)+~P10(x1754,x1752,x1755,x1753)+P4(x1751,x1752,x1753)+~P4(x1751,x1754,x1755)
% 59.45/59.53 [196]~P5(x1965,x1961,x1965,x1963)+~P5(x1965,x1961,x1965,x1962)+P6(x1961,x1962,x1963,x1964)+~P5(x1965,x1961,x1965,x1964)
% 59.45/59.53 [228]~P1(x2281,x2284,x2285)+~P1(x2281,x2282,x2283)+~P10(x2282,x2284,x2283,x2285)+P8(x2281,x2282,x2282,x2283,x2281,x2284,x2284,x2285)
% 59.45/59.53 [239]~P1(x2391,x2392,x2393)+~P9(x2395,x2392,x2395,x2393,x2394,x2392,x2394,x2391)+P4(x2391,x2392,x2393)+~P2(x2394,x2395,x2392,x2393)
% 59.45/59.53 [186]~P3(x1863,x1861,x1863,x1865)+~P3(x1861,x1862,x1861,x1863)+~P4(x1864,x1862,x1865)+P4(f7(x1861,x1862,x1863),x1861,x1863)
% 59.45/59.53 [192]~P6(x1921,x1922,x1923,x1925)+~P10(x1921,x1922,x1923,x1925)+~P4(x1924,x1921,x1922)+P2(f10(x1921,x1922,x1923),x1921,x1922,x1923)
% 59.45/59.53 [261]~P9(x2611,x2613,x2612,x2613,x2614,x2616,x2615,x2616)+~P9(x2611,x2612,x2612,x2613,x2614,x2615,x2615,x2616)+P1(x2611,x2612,x2613)+P11(x2611,x2612,x2613,x2614,x2615,x2616)
% 59.45/59.53 [251]~P6(x2511,x2512,x2515,x2514)+~P6(x2511,x2512,x2515,x2513)+~P9(x2515,x2511,x2515,x2512,x2516,x2513,x2516,x2514)+P5(x2511,x2512,x2513,x2514)+~P6(x2511,x2512,x2515,x2516)
% 59.45/59.53 [206]~P1(x2062,x2063,x2064)+~P1(x2061,x2064,x2066)+~P1(x2061,x2063,x2065)+~P10(x2063,x2064,x2065,x2066)+P1(x2061,x2062,f14(x2063,x2064,x2065,x2066,x2061,x2062))
% 59.45/59.53 [207]~P1(x2076,x2071,x2072)+~P1(x2075,x2072,x2074)+~P1(x2075,x2071,x2073)+~P10(x2071,x2072,x2073,x2074)+P1(f14(x2071,x2072,x2073,x2074,x2075,x2076),x2073,x2074)
% 59.45/59.53 [208]~P1(x2083,x2084,x2085)+~P4(x2086,x2081,x2082)+~P10(x2081,x2083,x2085,x2086)+~P10(x2081,x2083,x2082,x2084)+P1(f29(x2081,x2082,x2083,x2084,x2085,x2086),x2086,x2085)
% 59.45/59.53 [209]~P1(x2093,x2094,x2095)+~P4(x2096,x2091,x2092)+~P10(x2091,x2093,x2095,x2096)+~P10(x2091,x2093,x2092,x2094)+P1(f29(x2091,x2092,x2093,x2094,x2095,x2096),x2091,x2094)
% 59.45/59.53 [210]~P5(x2102,x2103,x2102,x2104)+~P5(x2101,x2103,x2101,x2106)+~P2(x2101,x2103,x2104,x2105)+E(x2101,x2102)+P1(f11(x2103,x2104,x2105,x2106,x2101,x2102),x2103,x2105)
% 59.45/59.53 [211]~P5(x2112,x2113,x2112,x2114)+~P5(x2111,x2113,x2111,x2116)+~P2(x2111,x2113,x2114,x2115)+E(x2111,x2112)+P1(f12(x2113,x2114,x2115,x2116,x2111,x2112),x2114,x2116)
% 59.45/59.53 [212]~P5(x2122,x2123,x2122,x2124)+~P5(x2121,x2123,x2121,x2126)+~P2(x2121,x2123,x2124,x2125)+E(x2121,x2122)+P5(f11(x2123,x2124,x2125,x2126,x2121,x2122),x2122,x2122,x2123)
% 59.45/59.53 [213]~P5(x2132,x2133,x2132,x2134)+~P5(x2131,x2133,x2131,x2136)+~P2(x2131,x2133,x2134,x2135)+E(x2131,x2132)+P5(f12(x2133,x2134,x2135,x2136,x2131,x2132),x2132,x2132,x2133)
% 59.45/59.53 [159]~P1(x1593,x1591,x1594)+~P1(x1595,x1591,x1594)+~P4(x1596,x1595,x1593)+~P4(x1597,x1591,x1594)+P4(f22(x1591,x1592),x1591,x1592)
% 59.45/59.53 %EqnAxiom
% 59.45/59.53 [1]E(x11,x11)
% 59.45/59.53 [2]E(x22,x21)+~E(x21,x22)
% 59.45/59.53 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 59.45/59.53 [4]~E(x41,x42)+E(f22(x41,x43),f22(x42,x43))
% 59.45/59.53 [5]~E(x51,x52)+E(f22(x53,x51),f22(x53,x52))
% 59.45/59.53 [6]~E(x61,x62)+E(f4(x61,x63,x64),f4(x62,x63,x64))
% 59.45/59.53 [7]~E(x71,x72)+E(f4(x73,x71,x74),f4(x73,x72,x74))
% 59.45/59.53 [8]~E(x81,x82)+E(f4(x83,x84,x81),f4(x83,x84,x82))
% 59.45/59.53 [9]~E(x91,x92)+E(f5(x91,x93,x94),f5(x92,x93,x94))
% 59.45/59.53 [10]~E(x101,x102)+E(f5(x103,x101,x104),f5(x103,x102,x104))
% 59.45/59.53 [11]~E(x111,x112)+E(f5(x113,x114,x111),f5(x113,x114,x112))
% 59.45/59.53 [12]~E(x121,x122)+E(f6(x121,x123,x124),f6(x122,x123,x124))
% 59.45/59.53 [13]~E(x131,x132)+E(f6(x133,x131,x134),f6(x133,x132,x134))
% 59.45/59.53 [14]~E(x141,x142)+E(f6(x143,x144,x141),f6(x143,x144,x142))
% 59.45/59.53 [15]~E(x151,x152)+E(f7(x151,x153,x154),f7(x152,x153,x154))
% 59.45/59.53 [16]~E(x161,x162)+E(f7(x163,x161,x164),f7(x163,x162,x164))
% 59.45/59.53 [17]~E(x171,x172)+E(f7(x173,x174,x171),f7(x173,x174,x172))
% 59.45/59.53 [18]~E(x181,x182)+E(f8(x181,x183,x184,x185),f8(x182,x183,x184,x185))
% 59.45/59.53 [19]~E(x191,x192)+E(f8(x193,x191,x194,x195),f8(x193,x192,x194,x195))
% 59.45/59.53 [20]~E(x201,x202)+E(f8(x203,x204,x201,x205),f8(x203,x204,x202,x205))
% 59.45/59.53 [21]~E(x211,x212)+E(f8(x213,x214,x215,x211),f8(x213,x214,x215,x212))
% 59.45/59.53 [22]~E(x221,x222)+E(f27(x221,x223,x224,x225),f27(x222,x223,x224,x225))
% 59.45/59.53 [23]~E(x231,x232)+E(f27(x233,x231,x234,x235),f27(x233,x232,x234,x235))
% 59.45/59.53 [24]~E(x241,x242)+E(f27(x243,x244,x241,x245),f27(x243,x244,x242,x245))
% 59.45/59.53 [25]~E(x251,x252)+E(f27(x253,x254,x255,x251),f27(x253,x254,x255,x252))
% 59.45/59.53 [26]~E(x261,x262)+E(f24(x261,x263,x264,x265),f24(x262,x263,x264,x265))
% 59.45/59.53 [27]~E(x271,x272)+E(f24(x273,x271,x274,x275),f24(x273,x272,x274,x275))
% 59.45/59.53 [28]~E(x281,x282)+E(f24(x283,x284,x281,x285),f24(x283,x284,x282,x285))
% 59.45/59.53 [29]~E(x291,x292)+E(f24(x293,x294,x295,x291),f24(x293,x294,x295,x292))
% 59.45/59.53 [30]~E(x301,x302)+E(f25(x301,x303,x304,x305),f25(x302,x303,x304,x305))
% 59.45/59.53 [31]~E(x311,x312)+E(f25(x313,x311,x314,x315),f25(x313,x312,x314,x315))
% 59.45/59.53 [32]~E(x321,x322)+E(f25(x323,x324,x321,x325),f25(x323,x324,x322,x325))
% 59.45/59.53 [33]~E(x331,x332)+E(f25(x333,x334,x335,x331),f25(x333,x334,x335,x332))
% 59.45/59.53 [34]~E(x341,x342)+E(f9(x341,x343,x344),f9(x342,x343,x344))
% 59.45/59.53 [35]~E(x351,x352)+E(f9(x353,x351,x354),f9(x353,x352,x354))
% 59.45/59.53 [36]~E(x361,x362)+E(f9(x363,x364,x361),f9(x363,x364,x362))
% 59.45/59.53 [37]~E(x371,x372)+E(f10(x371,x373,x374),f10(x372,x373,x374))
% 59.45/59.53 [38]~E(x381,x382)+E(f10(x383,x381,x384),f10(x383,x382,x384))
% 59.45/59.53 [39]~E(x391,x392)+E(f10(x393,x394,x391),f10(x393,x394,x392))
% 59.45/59.53 [40]~E(x401,x402)+E(f23(x401,x403,x404,x405),f23(x402,x403,x404,x405))
% 59.45/59.53 [41]~E(x411,x412)+E(f23(x413,x411,x414,x415),f23(x413,x412,x414,x415))
% 59.45/59.53 [42]~E(x421,x422)+E(f23(x423,x424,x421,x425),f23(x423,x424,x422,x425))
% 59.45/59.53 [43]~E(x431,x432)+E(f23(x433,x434,x435,x431),f23(x433,x434,x435,x432))
% 59.45/59.53 [44]~E(x441,x442)+E(f15(x441,x443,x444,x445),f15(x442,x443,x444,x445))
% 59.45/59.53 [45]~E(x451,x452)+E(f15(x453,x451,x454,x455),f15(x453,x452,x454,x455))
% 59.45/59.53 [46]~E(x461,x462)+E(f15(x463,x464,x461,x465),f15(x463,x464,x462,x465))
% 59.45/59.53 [47]~E(x471,x472)+E(f15(x473,x474,x475,x471),f15(x473,x474,x475,x472))
% 59.45/59.53 [48]~E(x481,x482)+E(f13(x481,x483,x484,x485,x486),f13(x482,x483,x484,x485,x486))
% 59.45/59.53 [49]~E(x491,x492)+E(f13(x493,x491,x494,x495,x496),f13(x493,x492,x494,x495,x496))
% 59.45/59.53 [50]~E(x501,x502)+E(f13(x503,x504,x501,x505,x506),f13(x503,x504,x502,x505,x506))
% 59.45/59.53 [51]~E(x511,x512)+E(f13(x513,x514,x515,x511,x516),f13(x513,x514,x515,x512,x516))
% 59.45/59.53 [52]~E(x521,x522)+E(f13(x523,x524,x525,x526,x521),f13(x523,x524,x525,x526,x522))
% 59.45/59.53 [53]~E(x531,x532)+E(f12(x531,x533,x534,x535,x536,x537),f12(x532,x533,x534,x535,x536,x537))
% 59.45/59.53 [54]~E(x541,x542)+E(f12(x543,x541,x544,x545,x546,x547),f12(x543,x542,x544,x545,x546,x547))
% 59.45/59.53 [55]~E(x551,x552)+E(f12(x553,x554,x551,x555,x556,x557),f12(x553,x554,x552,x555,x556,x557))
% 59.45/59.53 [56]~E(x561,x562)+E(f12(x563,x564,x565,x561,x566,x567),f12(x563,x564,x565,x562,x566,x567))
% 59.45/59.53 [57]~E(x571,x572)+E(f12(x573,x574,x575,x576,x571,x577),f12(x573,x574,x575,x576,x572,x577))
% 59.45/59.53 [58]~E(x581,x582)+E(f12(x583,x584,x585,x586,x587,x581),f12(x583,x584,x585,x586,x587,x582))
% 59.45/59.53 [59]~E(x591,x592)+E(f28(x591,x593,x594,x595,x596),f28(x592,x593,x594,x595,x596))
% 59.45/59.53 [60]~E(x601,x602)+E(f28(x603,x601,x604,x605,x606),f28(x603,x602,x604,x605,x606))
% 59.45/59.53 [61]~E(x611,x612)+E(f28(x613,x614,x611,x615,x616),f28(x613,x614,x612,x615,x616))
% 59.45/59.53 [62]~E(x621,x622)+E(f28(x623,x624,x625,x621,x626),f28(x623,x624,x625,x622,x626))
% 59.45/59.53 [63]~E(x631,x632)+E(f28(x633,x634,x635,x636,x631),f28(x633,x634,x635,x636,x632))
% 59.45/59.54 [64]~E(x641,x642)+E(f11(x641,x643,x644,x645,x646,x647),f11(x642,x643,x644,x645,x646,x647))
% 59.45/59.54 [65]~E(x651,x652)+E(f11(x653,x651,x654,x655,x656,x657),f11(x653,x652,x654,x655,x656,x657))
% 59.45/59.54 [66]~E(x661,x662)+E(f11(x663,x664,x661,x665,x666,x667),f11(x663,x664,x662,x665,x666,x667))
% 59.45/59.54 [67]~E(x671,x672)+E(f11(x673,x674,x675,x671,x676,x677),f11(x673,x674,x675,x672,x676,x677))
% 59.45/59.54 [68]~E(x681,x682)+E(f11(x683,x684,x685,x686,x681,x687),f11(x683,x684,x685,x686,x682,x687))
% 59.45/59.54 [69]~E(x691,x692)+E(f11(x693,x694,x695,x696,x697,x691),f11(x693,x694,x695,x696,x697,x692))
% 59.45/59.54 [70]~E(x701,x702)+E(f29(x701,x703,x704,x705,x706,x707),f29(x702,x703,x704,x705,x706,x707))
% 59.45/59.54 [71]~E(x711,x712)+E(f29(x713,x711,x714,x715,x716,x717),f29(x713,x712,x714,x715,x716,x717))
% 59.45/59.54 [72]~E(x721,x722)+E(f29(x723,x724,x721,x725,x726,x727),f29(x723,x724,x722,x725,x726,x727))
% 59.45/59.54 [73]~E(x731,x732)+E(f29(x733,x734,x735,x731,x736,x737),f29(x733,x734,x735,x732,x736,x737))
% 59.45/59.54 [74]~E(x741,x742)+E(f29(x743,x744,x745,x746,x741,x747),f29(x743,x744,x745,x746,x742,x747))
% 59.45/59.54 [75]~E(x751,x752)+E(f29(x753,x754,x755,x756,x757,x751),f29(x753,x754,x755,x756,x757,x752))
% 59.45/59.54 [76]~E(x761,x762)+E(f26(x761,x763,x764,x765,x766,x767),f26(x762,x763,x764,x765,x766,x767))
% 59.45/59.54 [77]~E(x771,x772)+E(f26(x773,x771,x774,x775,x776,x777),f26(x773,x772,x774,x775,x776,x777))
% 59.45/59.54 [78]~E(x781,x782)+E(f26(x783,x784,x781,x785,x786,x787),f26(x783,x784,x782,x785,x786,x787))
% 59.45/59.54 [79]~E(x791,x792)+E(f26(x793,x794,x795,x791,x796,x797),f26(x793,x794,x795,x792,x796,x797))
% 59.45/59.54 [80]~E(x801,x802)+E(f26(x803,x804,x805,x806,x801,x807),f26(x803,x804,x805,x806,x802,x807))
% 59.45/59.54 [81]~E(x811,x812)+E(f26(x813,x814,x815,x816,x817,x811),f26(x813,x814,x815,x816,x817,x812))
% 59.45/59.54 [82]~E(x821,x822)+E(f14(x821,x823,x824,x825,x826,x827),f14(x822,x823,x824,x825,x826,x827))
% 59.45/59.54 [83]~E(x831,x832)+E(f14(x833,x831,x834,x835,x836,x837),f14(x833,x832,x834,x835,x836,x837))
% 59.45/59.54 [84]~E(x841,x842)+E(f14(x843,x844,x841,x845,x846,x847),f14(x843,x844,x842,x845,x846,x847))
% 59.45/59.54 [85]~E(x851,x852)+E(f14(x853,x854,x855,x851,x856,x857),f14(x853,x854,x855,x852,x856,x857))
% 59.45/59.54 [86]~E(x861,x862)+E(f14(x863,x864,x865,x866,x861,x867),f14(x863,x864,x865,x866,x862,x867))
% 59.45/59.54 [87]~E(x871,x872)+E(f14(x873,x874,x875,x876,x877,x871),f14(x873,x874,x875,x876,x877,x872))
% 59.45/59.54 [88]P1(x882,x883,x884)+~E(x881,x882)+~P1(x881,x883,x884)
% 59.45/59.54 [89]P1(x893,x892,x894)+~E(x891,x892)+~P1(x893,x891,x894)
% 59.45/59.54 [90]P1(x903,x904,x902)+~E(x901,x902)+~P1(x903,x904,x901)
% 59.45/59.54 [91]P8(x912,x913,x914,x915,x916,x917,x918,x919)+~E(x911,x912)+~P8(x911,x913,x914,x915,x916,x917,x918,x919)
% 59.45/59.54 [92]P8(x923,x922,x924,x925,x926,x927,x928,x929)+~E(x921,x922)+~P8(x923,x921,x924,x925,x926,x927,x928,x929)
% 59.45/59.54 [93]P8(x933,x934,x932,x935,x936,x937,x938,x939)+~E(x931,x932)+~P8(x933,x934,x931,x935,x936,x937,x938,x939)
% 59.45/59.54 [94]P8(x943,x944,x945,x942,x946,x947,x948,x949)+~E(x941,x942)+~P8(x943,x944,x945,x941,x946,x947,x948,x949)
% 59.45/59.54 [95]P8(x953,x954,x955,x956,x952,x957,x958,x959)+~E(x951,x952)+~P8(x953,x954,x955,x956,x951,x957,x958,x959)
% 59.45/59.54 [96]P8(x963,x964,x965,x966,x967,x962,x968,x969)+~E(x961,x962)+~P8(x963,x964,x965,x966,x967,x961,x968,x969)
% 59.45/59.54 [97]P8(x973,x974,x975,x976,x977,x978,x972,x979)+~E(x971,x972)+~P8(x973,x974,x975,x976,x977,x978,x971,x979)
% 59.45/59.54 [98]P8(x983,x984,x985,x986,x987,x988,x989,x982)+~E(x981,x982)+~P8(x983,x984,x985,x986,x987,x988,x989,x981)
% 59.45/59.54 [99]P6(x992,x993,x994,x995)+~E(x991,x992)+~P6(x991,x993,x994,x995)
% 59.45/59.54 [100]P6(x1003,x1002,x1004,x1005)+~E(x1001,x1002)+~P6(x1003,x1001,x1004,x1005)
% 59.45/59.54 [101]P6(x1013,x1014,x1012,x1015)+~E(x1011,x1012)+~P6(x1013,x1014,x1011,x1015)
% 59.55/59.54 [102]P6(x1023,x1024,x1025,x1022)+~E(x1021,x1022)+~P6(x1023,x1024,x1025,x1021)
% 59.55/59.54 [103]P3(x1032,x1033,x1034,x1035)+~E(x1031,x1032)+~P3(x1031,x1033,x1034,x1035)
% 59.55/59.54 [104]P3(x1043,x1042,x1044,x1045)+~E(x1041,x1042)+~P3(x1043,x1041,x1044,x1045)
% 59.55/59.54 [105]P3(x1053,x1054,x1052,x1055)+~E(x1051,x1052)+~P3(x1053,x1054,x1051,x1055)
% 59.55/59.54 [106]P3(x1063,x1064,x1065,x1062)+~E(x1061,x1062)+~P3(x1063,x1064,x1065,x1061)
% 59.55/59.54 [107]P11(x1072,x1073,x1074,x1075,x1076,x1077)+~E(x1071,x1072)+~P11(x1071,x1073,x1074,x1075,x1076,x1077)
% 59.55/59.54 [108]P11(x1083,x1082,x1084,x1085,x1086,x1087)+~E(x1081,x1082)+~P11(x1083,x1081,x1084,x1085,x1086,x1087)
% 59.55/59.54 [109]P11(x1093,x1094,x1092,x1095,x1096,x1097)+~E(x1091,x1092)+~P11(x1093,x1094,x1091,x1095,x1096,x1097)
% 59.55/59.54 [110]P11(x1103,x1104,x1105,x1102,x1106,x1107)+~E(x1101,x1102)+~P11(x1103,x1104,x1105,x1101,x1106,x1107)
% 59.55/59.54 [111]P11(x1113,x1114,x1115,x1116,x1112,x1117)+~E(x1111,x1112)+~P11(x1113,x1114,x1115,x1116,x1111,x1117)
% 59.55/59.54 [112]P11(x1123,x1124,x1125,x1126,x1127,x1122)+~E(x1121,x1122)+~P11(x1123,x1124,x1125,x1126,x1127,x1121)
% 59.55/59.54 [113]P9(x1132,x1133,x1134,x1135,x1136,x1137,x1138,x1139)+~E(x1131,x1132)+~P9(x1131,x1133,x1134,x1135,x1136,x1137,x1138,x1139)
% 59.55/59.54 [114]P9(x1143,x1142,x1144,x1145,x1146,x1147,x1148,x1149)+~E(x1141,x1142)+~P9(x1143,x1141,x1144,x1145,x1146,x1147,x1148,x1149)
% 59.55/59.54 [115]P9(x1153,x1154,x1152,x1155,x1156,x1157,x1158,x1159)+~E(x1151,x1152)+~P9(x1153,x1154,x1151,x1155,x1156,x1157,x1158,x1159)
% 59.55/59.54 [116]P9(x1163,x1164,x1165,x1162,x1166,x1167,x1168,x1169)+~E(x1161,x1162)+~P9(x1163,x1164,x1165,x1161,x1166,x1167,x1168,x1169)
% 59.55/59.54 [117]P9(x1173,x1174,x1175,x1176,x1172,x1177,x1178,x1179)+~E(x1171,x1172)+~P9(x1173,x1174,x1175,x1176,x1171,x1177,x1178,x1179)
% 59.55/59.54 [118]P9(x1183,x1184,x1185,x1186,x1187,x1182,x1188,x1189)+~E(x1181,x1182)+~P9(x1183,x1184,x1185,x1186,x1187,x1181,x1188,x1189)
% 59.55/59.54 [119]P9(x1193,x1194,x1195,x1196,x1197,x1198,x1192,x1199)+~E(x1191,x1192)+~P9(x1193,x1194,x1195,x1196,x1197,x1198,x1191,x1199)
% 59.55/59.54 [120]P9(x1203,x1204,x1205,x1206,x1207,x1208,x1209,x1202)+~E(x1201,x1202)+~P9(x1203,x1204,x1205,x1206,x1207,x1208,x1209,x1201)
% 59.55/59.54 [121]P2(x1212,x1213,x1214,x1215)+~E(x1211,x1212)+~P2(x1211,x1213,x1214,x1215)
% 59.55/59.54 [122]P2(x1223,x1222,x1224,x1225)+~E(x1221,x1222)+~P2(x1223,x1221,x1224,x1225)
% 59.55/59.54 [123]P2(x1233,x1234,x1232,x1235)+~E(x1231,x1232)+~P2(x1233,x1234,x1231,x1235)
% 59.55/59.54 [124]P2(x1243,x1244,x1245,x1242)+~E(x1241,x1242)+~P2(x1243,x1244,x1245,x1241)
% 59.55/59.54 [125]P5(x1252,x1253,x1254,x1255)+~E(x1251,x1252)+~P5(x1251,x1253,x1254,x1255)
% 59.55/59.54 [126]P5(x1263,x1262,x1264,x1265)+~E(x1261,x1262)+~P5(x1263,x1261,x1264,x1265)
% 59.55/59.54 [127]P5(x1273,x1274,x1272,x1275)+~E(x1271,x1272)+~P5(x1273,x1274,x1271,x1275)
% 59.55/59.54 [128]P5(x1283,x1284,x1285,x1282)+~E(x1281,x1282)+~P5(x1283,x1284,x1285,x1281)
% 59.55/59.54 [129]P7(x1292,x1293,x1294,x1295,x1296,x1297)+~E(x1291,x1292)+~P7(x1291,x1293,x1294,x1295,x1296,x1297)
% 59.55/59.54 [130]P7(x1303,x1302,x1304,x1305,x1306,x1307)+~E(x1301,x1302)+~P7(x1303,x1301,x1304,x1305,x1306,x1307)
% 59.55/59.54 [131]P7(x1313,x1314,x1312,x1315,x1316,x1317)+~E(x1311,x1312)+~P7(x1313,x1314,x1311,x1315,x1316,x1317)
% 59.55/59.54 [132]P7(x1323,x1324,x1325,x1322,x1326,x1327)+~E(x1321,x1322)+~P7(x1323,x1324,x1325,x1321,x1326,x1327)
% 59.55/59.54 [133]P7(x1333,x1334,x1335,x1336,x1332,x1337)+~E(x1331,x1332)+~P7(x1333,x1334,x1335,x1336,x1331,x1337)
% 59.55/59.54 [134]P7(x1343,x1344,x1345,x1346,x1347,x1342)+~E(x1341,x1342)+~P7(x1343,x1344,x1345,x1346,x1347,x1341)
% 59.55/59.54 [135]P10(x1352,x1353,x1354,x1355)+~E(x1351,x1352)+~P10(x1351,x1353,x1354,x1355)
% 59.55/59.54 [136]P10(x1363,x1362,x1364,x1365)+~E(x1361,x1362)+~P10(x1363,x1361,x1364,x1365)
% 59.55/59.54 [137]P10(x1373,x1374,x1372,x1375)+~E(x1371,x1372)+~P10(x1373,x1374,x1371,x1375)
% 59.55/59.54 [138]P10(x1383,x1384,x1385,x1382)+~E(x1381,x1382)+~P10(x1383,x1384,x1385,x1381)
% 59.55/59.54 [139]P4(x1392,x1393,x1394)+~E(x1391,x1392)+~P4(x1391,x1393,x1394)
% 59.55/59.54 [140]P4(x1403,x1402,x1404)+~E(x1401,x1402)+~P4(x1403,x1401,x1404)
% 59.55/59.54 [141]P4(x1413,x1414,x1412)+~E(x1411,x1412)+~P4(x1413,x1414,x1411)
% 59.55/59.54
% 59.55/59.54 %-------------------------------------------
% 59.55/59.54 cnf(264,plain,
% 59.55/59.54 (~P1(a19,a1,a20)),
% 59.55/59.54 inference(scs_inference,[],[150,151])).
% 59.55/59.54 cnf(266,plain,
% 59.55/59.54 (~P1(a1,a20,a19)),
% 59.55/59.54 inference(scs_inference,[],[150,151,152])).
% 59.55/59.54 cnf(270,plain,
% 59.55/59.54 (~P10(a1,a19,a1,a20)),
% 59.55/59.54 inference(scs_inference,[],[150,151,152,153,160])).
% 59.55/59.54 cnf(274,plain,
% 59.55/59.54 (~P10(a1,a20,a1,a19)),
% 59.55/59.54 inference(scs_inference,[],[150,151,152,153,160,154,163])).
% 59.55/59.54 cnf(276,plain,
% 59.55/59.54 (~P10(a1,a19,a20,a1)),
% 59.55/59.54 inference(scs_inference,[],[150,151,152,153,160,154,163,164])).
% 59.55/59.54 cnf(280,plain,
% 59.55/59.54 (~P9(a1,a20,x2801,x2802,a1,a19,x2801,x2802)),
% 59.55/59.54 inference(scs_inference,[],[150,151,152,153,160,154,163,164,233,252])).
% 59.55/59.54 cnf(282,plain,
% 59.55/59.54 (~P9(x2821,x2822,a1,a19,x2821,x2822,a1,a20)),
% 59.55/59.54 inference(scs_inference,[],[150,151,152,153,160,154,163,164,233,252,253])).
% 59.55/59.54 cnf(284,plain,
% 59.55/59.54 (~P9(a19,a1,x2841,x2842,a1,a20,x2841,x2842)),
% 59.55/59.54 inference(scs_inference,[],[150,151,152,153,160,154,163,164,233,252,253,254])).
% 59.55/59.54 cnf(286,plain,
% 59.55/59.54 (~P9(a1,a19,a1,a20,x2861,x2862,x2861,x2862)),
% 59.55/59.54 inference(scs_inference,[],[150,151,152,153,160,154,163,164,233,252,253,254,255])).
% 59.55/59.54 cnf(288,plain,
% 59.55/59.54 (P1(a16,a16,a1)),
% 59.55/59.54 inference(scs_inference,[],[142,150,151,152,153,160,154,163,164,233,252,253,254,255,155])).
% 59.55/59.54 cnf(290,plain,
% 59.55/59.54 (~P10(a19,a1,a1,a20)),
% 59.55/59.54 inference(scs_inference,[],[142,150,151,152,153,160,154,163,164,233,252,253,254,255,155,225])).
% 59.55/59.54 cnf(292,plain,
% 59.55/59.54 (~P11(x2921,a1,a19,x2921,a1,a20)),
% 59.55/59.54 inference(scs_inference,[],[142,150,151,152,153,160,154,163,164,233,252,253,254,255,155,225,231])).
% 59.55/59.54 cnf(294,plain,
% 59.55/59.54 (~P3(x2941,x2942,a1,a17)+P10(x2941,x2942,a2,a16)),
% 59.55/59.54 inference(scs_inference,[],[142,145,150,151,152,153,160,154,163,164,233,252,253,254,255,155,225,231,180])).
% 59.55/59.54 cnf(308,plain,
% 59.55/59.54 (~P9(a20,a1,x3081,x3082,a1,a19,x3081,x3082)),
% 59.55/59.54 inference(scs_inference,[],[280,254])).
% 59.55/59.54 cnf(310,plain,
% 59.55/59.54 (~P10(a1,a20,a19,a1)),
% 59.55/59.54 inference(scs_inference,[],[274,280,254,164])).
% 59.55/59.54 cnf(312,plain,
% 59.55/59.54 (~P1(a20,a1,a19)),
% 59.55/59.54 inference(scs_inference,[],[266,274,280,254,164,151])).
% 59.55/59.54 cnf(314,plain,
% 59.55/59.54 (~P10(a19,a1,a19,a20)),
% 59.55/59.54 inference(scs_inference,[],[264,266,274,280,254,164,151,160])).
% 59.55/59.54 cnf(316,plain,
% 59.55/59.54 (~P9(x3161,x3162,a1,a20,x3161,x3162,a1,a19)),
% 59.55/59.54 inference(scs_inference,[],[264,266,274,280,282,254,164,151,160,252])).
% 59.55/59.54 cnf(320,plain,
% 59.55/59.54 (~P1(a19,a20,a1)),
% 59.55/59.54 inference(scs_inference,[],[264,266,274,280,282,254,164,151,160,252,231,152])).
% 59.55/59.54 cnf(322,plain,
% 59.55/59.54 (~P10(a20,a1,a1,a19)),
% 59.55/59.54 inference(scs_inference,[],[264,266,274,280,282,276,254,164,151,160,252,231,152,163])).
% 59.55/59.54 cnf(324,plain,
% 59.55/59.54 (~P9(a1,a19,x3241,x3242,a20,a1,x3241,x3242)),
% 59.55/59.54 inference(scs_inference,[],[264,266,274,280,282,276,254,164,151,160,252,231,152,163,233])).
% 59.55/59.54 cnf(326,plain,
% 59.55/59.54 (~P9(x3261,x3262,a19,a1,x3261,x3262,a1,a20)),
% 59.55/59.54 inference(scs_inference,[],[264,266,274,280,282,284,276,254,164,151,160,252,231,152,163,233,253])).
% 59.55/59.54 cnf(330,plain,
% 59.55/59.54 (~P11(a1,x3301,a19,a1,x3301,a20)),
% 59.55/59.54 inference(scs_inference,[],[264,266,274,280,282,284,292,276,254,164,151,160,252,231,152,163,233,253,153,215])).
% 59.55/59.54 cnf(332,plain,
% 59.55/59.54 (~P9(a1,a20,a1,a19,x3321,x3322,x3321,x3322)),
% 59.55/59.54 inference(scs_inference,[],[264,266,274,280,282,284,292,276,254,164,151,160,252,231,152,163,233,253,153,215,255])).
% 59.55/59.54 cnf(334,plain,
% 59.55/59.54 (~P11(x3341,a19,a1,x3341,a20,a1)),
% 59.55/59.54 inference(scs_inference,[],[264,266,274,280,282,284,292,276,254,164,151,160,252,231,152,163,233,253,153,215,255,216])).
% 59.55/59.54 cnf(336,plain,
% 59.55/59.54 (P1(a16,a16,a19)),
% 59.55/59.54 inference(scs_inference,[],[143,264,266,274,280,282,284,292,276,254,164,151,160,252,231,152,163,233,253,153,215,255,216,155])).
% 59.55/59.54 cnf(338,plain,
% 59.55/59.54 (~P11(a1,x3381,a20,a1,x3381,a19)),
% 59.55/59.54 inference(scs_inference,[],[143,264,266,274,280,282,284,292,276,254,164,151,160,252,231,152,163,233,253,153,215,255,216,155,214])).
% 59.55/59.54 cnf(346,plain,
% 59.55/59.54 (~P9(a19,a1,a1,a20,x3461,x3462,x3461,x3462)),
% 59.55/59.54 inference(scs_inference,[],[286,254])).
% 59.55/59.54 cnf(348,plain,
% 59.55/59.54 (~P10(a20,a1,a20,a19)),
% 59.55/59.54 inference(scs_inference,[],[312,286,254,160])).
% 59.55/59.54 cnf(350,plain,
% 59.55/59.54 (~P1(a20,a19,a1)),
% 59.55/59.54 inference(scs_inference,[],[312,286,254,160,152])).
% 59.55/59.54 cnf(352,plain,
% 59.55/59.54 (~P10(a19,a1,a20,a19)),
% 59.55/59.54 inference(scs_inference,[],[312,314,286,254,160,152,164])).
% 59.55/59.54 cnf(354,plain,
% 59.55/59.54 (~P9(x3541,x3542,x3541,x3542,a1,a19,a1,a20)),
% 59.55/59.54 inference(scs_inference,[],[312,314,286,254,160,152,164,252])).
% 59.55/59.54 cnf(358,plain,
% 59.55/59.54 (~P11(a19,a1,a20,x3581,x3581,x3581)),
% 59.55/59.54 inference(scs_inference,[],[312,314,286,254,160,152,164,252,153,231])).
% 59.55/59.54 cnf(360,plain,
% 59.55/59.54 (~P9(a19,a1,x3601,x3602,a19,a20,x3601,x3602)),
% 59.55/59.54 inference(scs_inference,[],[312,314,286,254,160,152,164,252,153,231,233])).
% 59.55/59.54 cnf(364,plain,
% 59.55/59.54 (~P10(a19,a20,a19,a1)),
% 59.55/59.54 inference(scs_inference,[],[312,314,286,254,160,152,164,252,153,231,233,154,163])).
% 59.55/59.54 cnf(366,plain,
% 59.55/59.54 (~P9(x3661,x3662,a20,a1,x3661,x3662,a1,a19)),
% 59.55/59.54 inference(scs_inference,[],[312,314,286,308,254,160,152,164,252,153,231,233,154,163,253])).
% 59.55/59.54 cnf(368,plain,
% 59.55/59.54 (~P11(x3681,a20,a1,x3681,a19,a1)),
% 59.55/59.54 inference(scs_inference,[],[312,314,286,308,334,254,160,152,164,252,153,231,233,154,163,253,214])).
% 59.55/59.54 cnf(372,plain,
% 59.55/59.54 (~P9(a20,a1,a1,a19,x3721,x3722,x3721,x3722)),
% 59.55/59.54 inference(scs_inference,[],[312,314,286,308,330,334,254,160,152,164,252,153,231,233,154,163,253,214,216,255])).
% 59.55/59.54 cnf(376,plain,
% 59.55/59.54 (P1(a2,a2,a20)),
% 59.55/59.54 inference(scs_inference,[],[144,312,314,286,308,330,334,254,160,152,164,252,153,231,233,154,163,253,214,216,255,215,155])).
% 59.55/59.54 cnf(381,plain,
% 59.55/59.54 (~P10(x3811,x3812,x3813,x3814)+~P9(a1,a19,a1,a20,x3811,x3812,x3813,x3814)),
% 59.55/59.54 inference(scs_inference,[],[144,312,148,270,314,286,308,330,334,254,160,152,164,252,153,231,233,154,163,253,214,216,255,215,155,122,123,124,240])).
% 59.55/59.54 cnf(390,plain,
% 59.55/59.54 (~P9(a19,a1,x3901,x3902,a20,a1,x3901,x3902)),
% 59.55/59.54 inference(scs_inference,[],[324,254])).
% 59.55/59.54 cnf(392,plain,
% 59.55/59.54 (~P10(a20,a1,a19,a20)),
% 59.55/59.54 inference(scs_inference,[],[348,324,254,164])).
% 59.55/59.54 cnf(394,plain,
% 59.55/59.54 (~P10(a20,a19,a20,a1)),
% 59.55/59.54 inference(scs_inference,[],[350,348,324,254,164,160])).
% 59.55/59.54 cnf(396,plain,
% 59.55/59.54 (~P10(a19,a1,a20,a1)),
% 59.55/59.54 inference(scs_inference,[],[350,348,324,254,164,160,225])).
% 59.55/59.54 cnf(398,plain,
% 59.55/59.54 (~P11(a20,a1,a19,x3981,x3981,x3981)),
% 59.55/59.54 inference(scs_inference,[],[350,348,324,372,254,164,160,225,231])).
% 59.55/59.54 cnf(401,plain,
% 59.55/59.54 (~P9(a1,a20,x4011,x4012,a19,a1,x4011,x4012)),
% 59.55/59.54 inference(scs_inference,[],[350,348,284,324,372,254,164,160,225,231,252])).
% 59.55/59.54 cnf(405,plain,
% 59.55/59.54 (~P9(a20,a1,x4051,x4052,a20,a19,x4051,x4052)),
% 59.55/59.54 inference(scs_inference,[],[350,348,284,324,372,254,164,160,225,231,252,253,233])).
% 59.55/59.54 cnf(407,plain,
% 59.55/59.54 (~P10(a20,a19,a19,a1)),
% 59.55/59.54 inference(scs_inference,[],[350,348,284,324,372,352,254,164,160,225,231,252,253,233,163])).
% 59.55/59.54 cnf(409,plain,
% 59.55/59.54 (~P11(x4091,x4091,x4091,a19,a1,a20)),
% 59.55/59.54 inference(scs_inference,[],[350,348,284,324,358,372,352,254,164,160,225,231,252,253,233,163,214])).
% 59.55/59.54 cnf(413,plain,
% 59.55/59.54 (~P9(a1,a19,a20,a1,x4131,x4132,x4131,x4132)),
% 59.55/59.54 inference(scs_inference,[],[350,348,284,324,358,372,352,254,164,160,225,231,252,253,233,163,214,215,255])).
% 59.55/59.54 cnf(415,plain,
% 59.55/59.54 (~P11(a19,a20,a1,x4151,x4151,x4151)),
% 59.55/59.54 inference(scs_inference,[],[350,348,284,324,358,372,352,254,164,160,225,231,252,253,233,163,214,215,255,216])).
% 59.55/59.54 cnf(417,plain,
% 59.55/59.54 (P1(a1,a1,a16)),
% 59.55/59.54 inference(scs_inference,[],[288,350,348,284,324,358,372,352,254,164,160,225,231,252,253,233,163,214,215,255,216,155])).
% 59.55/59.54 cnf(419,plain,
% 59.55/59.54 (~P10(x4191,x4192,x4193,x4194)+~P9(a20,a1,a20,a19,x4191,x4192,x4193,x4194)),
% 59.55/59.54 inference(scs_inference,[],[288,350,348,284,324,358,372,352,254,164,160,225,231,252,253,233,163,214,215,255,216,155,240])).
% 59.55/59.54 cnf(421,plain,
% 59.55/59.54 (~P3(x4211,x4212,a20,a17)+~P9(a20,a1,a20,a19,x4211,x4212,a3,a2)),
% 59.55/59.54 inference(scs_inference,[],[147,288,350,348,284,324,358,372,352,254,164,160,225,231,252,253,233,163,214,215,255,216,155,240,180])).
% 59.55/59.54 cnf(432,plain,
% 59.55/59.54 (~P10(a20,a19,a1,a20)),
% 59.55/59.54 inference(scs_inference,[],[394,316,254,164])).
% 59.55/59.54 cnf(437,plain,
% 59.55/59.54 (~P9(a1,a20,a19,a1,x4371,x4372,x4371,x4372)),
% 59.55/59.54 inference(scs_inference,[],[394,316,346,390,254,164,231,253])).
% 59.55/59.54 cnf(439,plain,
% 59.55/59.54 (~P9(x4391,x4392,x4391,x4392,a1,a20,a1,a19)),
% 59.55/59.54 inference(scs_inference,[],[394,332,316,346,390,254,164,231,253,252])).
% 59.55/59.54 cnf(441,plain,
% 59.55/59.54 (~P10(a19,a20,a20,a1)),
% 59.55/59.54 inference(scs_inference,[],[394,332,316,346,390,392,254,164,231,253,252,163])).
% 59.55/59.54 cnf(443,plain,
% 59.55/59.54 (~P9(a20,a19,x4431,x4432,a20,a1,x4431,x4432)),
% 59.55/59.54 inference(scs_inference,[],[394,332,316,346,390,392,254,164,231,253,252,163,233])).
% 59.55/59.54 cnf(445,plain,
% 59.55/59.54 (~P11(a1,a20,a19,x4451,x4451,x4451)),
% 59.55/59.54 inference(scs_inference,[],[394,332,398,316,346,390,392,254,164,231,253,252,163,233,215])).
% 59.55/59.54 cnf(447,plain,
% 59.55/59.54 (~P11(x4471,x4471,x4471,a20,a1,a19)),
% 59.55/59.54 inference(scs_inference,[],[394,332,398,316,346,390,392,254,164,231,253,252,163,233,215,214])).
% 59.55/59.54 cnf(451,plain,
% 59.55/59.54 (~P9(x4511,x4512,x4511,x4512,a19,a1,a1,a20)),
% 59.55/59.54 inference(scs_inference,[],[394,332,398,316,326,346,390,392,254,164,231,253,252,163,233,215,214,216,255])).
% 59.55/59.54 cnf(453,plain,
% 59.55/59.54 (P1(a19,a19,a16)),
% 59.55/59.54 inference(scs_inference,[],[394,336,332,398,316,326,346,390,392,254,164,231,253,252,163,233,215,214,216,255,155])).
% 59.55/59.54 cnf(457,plain,
% 59.55/59.54 (~P10(x4571,x4572,x4573,x4574)+~P9(a20,a19,a20,a1,x4571,x4572,x4573,x4574)),
% 59.55/59.54 inference(scs_inference,[],[142,149,394,336,332,398,316,326,346,390,392,254,164,231,253,252,163,233,215,214,216,255,155,124,88,240])).
% 59.55/59.54 cnf(467,plain,
% 59.55/59.54 (~P9(x4671,x4672,x4672,x4671,a1,a19,a1,a20)),
% 59.55/59.54 inference(scs_inference,[],[354,254])).
% 59.55/59.54 cnf(469,plain,
% 59.55/59.54 (~P9(x4691,x4692,a19,a1,x4691,x4692,a19,a20)),
% 59.55/59.54 inference(scs_inference,[],[354,360,254,253])).
% 59.55/59.54 cnf(471,plain,
% 59.55/59.54 (~P10(a20,a1,a19,a1)),
% 59.55/59.54 inference(scs_inference,[],[354,360,322,254,253,164])).
% 59.55/59.54 cnf(473,plain,
% 59.55/59.54 (~P11(x4731,a19,a1,x4731,a19,a20)),
% 59.55/59.54 inference(scs_inference,[],[354,360,322,254,253,164,231])).
% 59.55/59.54 cnf(475,plain,
% 59.55/59.54 (~P9(a19,a20,x4751,x4752,a19,a1,x4751,x4752)),
% 59.55/59.54 inference(scs_inference,[],[354,360,322,364,254,253,164,231,233])).
% 59.55/59.54 cnf(477,plain,
% 59.55/59.54 (~P9(x4771,x4772,x4771,x4772,a1,a19,a20,a1)),
% 59.55/59.54 inference(scs_inference,[],[354,360,413,322,364,254,253,164,231,233,252])).
% 59.55/59.54 cnf(479,plain,
% 59.55/59.54 (~P10(a1,a20,a20,a19)),
% 59.55/59.54 inference(scs_inference,[],[354,360,413,322,364,432,254,253,164,231,233,252,163])).
% 59.55/59.54 cnf(492,plain,
% 59.55/59.54 (~P10(x4921,x4922,x4923,x4924)+~P9(a19,a1,a19,a20,x4921,x4922,x4923,x4924)),
% 59.55/59.54 inference(scs_inference,[],[376,314,354,360,413,322,364,409,415,447,432,254,253,164,231,233,252,163,215,214,255,216,155,240])).
% 59.55/59.54 cnf(494,plain,
% 59.55/59.54 (~P3(x4941,x4942,a20,a17)+~P9(a19,a1,a19,a20,x4941,x4942,a3,a2)),
% 59.55/59.54 inference(scs_inference,[],[147,376,314,354,360,413,322,364,409,415,447,432,254,253,164,231,233,252,163,215,214,255,216,155,240,180])).
% 59.55/59.54 cnf(502,plain,
% 59.55/59.54 (~P9(a20,a1,x5021,x5022,a19,a1,x5021,x5022)),
% 59.55/59.54 inference(scs_inference,[],[401,254])).
% 59.55/59.54 cnf(508,plain,
% 59.55/59.54 (~P10(a20,a19,a1,a19)),
% 59.55/59.54 inference(scs_inference,[],[401,407,254,253,231,164])).
% 59.55/59.54 cnf(510,plain,
% 59.55/59.54 (~P10(a1,a19,a20,a19)),
% 59.55/59.54 inference(scs_inference,[],[401,407,254,253,231,164,163])).
% 59.55/59.54 cnf(512,plain,
% 59.55/59.54 (~P9(a20,a19,x5121,x5122,a19,a1,x5121,x5122)),
% 59.55/59.54 inference(scs_inference,[],[401,407,254,253,231,164,163,233])).
% 59.55/59.54 cnf(514,plain,
% 59.55/59.54 (~P9(x5141,x5142,x5141,x5142,a20,a1,a1,a19)),
% 59.55/59.54 inference(scs_inference,[],[401,372,407,254,253,231,164,163,233,252])).
% 59.55/59.54 cnf(522,plain,
% 59.55/59.54 (~P9(a20,a1,a20,a19,x5221,x5222,x5221,x5222)),
% 59.55/59.54 inference(scs_inference,[],[401,405,372,445,338,368,407,254,253,231,164,163,233,252,214,215,216,255])).
% 59.55/59.54 cnf(537,plain,
% 59.55/59.54 (~P9(a1,a20,x5371,x5372,a20,a19,x5371,x5372)),
% 59.55/59.54 inference(scs_inference,[],[405,254])).
% 59.55/59.54 cnf(539,plain,
% 59.55/59.54 (~P9(x5391,x5392,a20,a1,x5391,x5392,a20,a19)),
% 59.55/59.54 inference(scs_inference,[],[405,254,253])).
% 59.55/59.54 cnf(541,plain,
% 59.55/59.54 (~P10(a19,a20,a1,a20)),
% 59.55/59.54 inference(scs_inference,[],[405,441,254,253,164])).
% 59.55/59.54 cnf(543,plain,
% 59.55/59.54 (~P9(x5431,x5432,x5431,x5432,a1,a20,a19,a1)),
% 59.55/59.55 inference(scs_inference,[],[405,437,441,254,253,164,252])).
% 59.55/59.55 cnf(545,plain,
% 59.55/59.55 (~P11(x5451,a20,a1,x5451,a20,a19)),
% 59.55/59.55 inference(scs_inference,[],[405,437,441,254,253,164,252,231])).
% 59.55/59.55 cnf(547,plain,
% 59.55/59.55 (~P10(a1,a20,a19,a20)),
% 59.55/59.55 inference(scs_inference,[],[405,437,441,254,253,164,252,231,163])).
% 59.55/59.55 cnf(549,plain,
% 59.55/59.55 (~P9(a19,a20,x5491,x5492,a20,a1,x5491,x5492)),
% 59.55/59.55 inference(scs_inference,[],[405,437,441,254,253,164,252,231,163,233])).
% 59.55/59.55 cnf(553,plain,
% 59.55/59.55 (~P11(x5531,a19,a20,x5531,a19,a1)),
% 59.55/59.55 inference(scs_inference,[],[405,437,441,473,254,253,164,252,231,163,233,215,214])).
% 59.55/59.55 cnf(555,plain,
% 59.55/59.55 (~P9(a20,a19,a20,a1,x5551,x5552,x5551,x5552)),
% 59.55/59.55 inference(scs_inference,[],[405,437,443,441,473,254,253,164,252,231,163,233,215,214,255])).
% 59.55/59.55 cnf(557,plain,
% 59.55/59.55 (~P11(x5571,a1,a19,x5571,a20,a19)),
% 59.55/59.55 inference(scs_inference,[],[405,437,443,441,473,254,253,164,252,231,163,233,215,214,255,216])).
% 59.55/59.55 cnf(564,plain,
% 59.55/59.55 (~P9(a19,a1,a20,a1,x5641,x5642,x5641,x5642)),
% 59.55/59.55 inference(scs_inference,[],[413,254])).
% 59.55/59.55 cnf(568,plain,
% 59.55/59.55 (~P9(a1,a19,a1,a20,x5681,x5682,x5682,x5681)),
% 59.55/59.55 inference(scs_inference,[],[413,390,467,254,253,252])).
% 59.55/59.55 cnf(570,plain,
% 59.55/59.55 (~P9(a20,a19,x5701,x5702,a1,a19,x5701,x5702)),
% 59.55/59.55 inference(scs_inference,[],[413,390,467,508,254,253,252,233])).
% 59.55/59.55 cnf(572,plain,
% 59.55/59.55 (~P10(a1,a19,a19,a20)),
% 59.55/59.55 inference(scs_inference,[],[413,390,467,508,510,254,253,252,233,164])).
% 59.55/59.55 cnf(574,plain,
% 59.55/59.55 (~P11(a20,a19,x5741,a1,a19,x5741)),
% 59.55/59.55 inference(scs_inference,[],[413,390,467,508,510,254,253,252,233,164,231])).
% 59.55/59.55 cnf(576,plain,
% 59.55/59.55 (~P10(a19,a20,a1,a19)),
% 59.55/59.55 inference(scs_inference,[],[413,390,467,508,510,254,253,252,233,164,231,163])).
% 59.55/59.55 cnf(578,plain,
% 59.55/59.55 (~P11(x5781,a20,a19,x5781,a20,a1)),
% 59.55/59.55 inference(scs_inference,[],[413,390,467,508,510,545,254,253,252,233,164,231,163,214])).
% 59.55/59.55 cnf(582,plain,
% 59.55/59.55 (~P11(x5821,a1,a20,x5821,a19,a20)),
% 59.55/59.55 inference(scs_inference,[],[413,390,467,508,510,545,254,253,252,233,164,231,163,214,215,216])).
% 59.55/59.55 cnf(584,plain,
% 59.55/59.55 (~P9(a19,a1,a19,a20,x5841,x5842,x5841,x5842)),
% 59.55/59.55 inference(scs_inference,[],[413,390,360,467,508,510,545,254,253,252,233,164,231,163,214,215,216,255])).
% 59.55/59.55 cnf(590,plain,
% 59.55/59.55 (~P9(x5901,x5902,x5902,x5901,a1,a20,a1,a19)),
% 59.55/59.55 inference(scs_inference,[],[439,254])).
% 59.55/59.55 cnf(592,plain,
% 59.55/59.55 (~P9(a1,a20,x5921,x5922,a19,a20,x5921,x5922)),
% 59.55/59.55 inference(scs_inference,[],[439,547,254,233])).
% 59.55/59.55 cnf(594,plain,
% 59.55/59.55 (~P9(x5941,x5942,a20,a19,x5941,x5942,a20,a1)),
% 59.55/59.55 inference(scs_inference,[],[439,443,547,254,233,253])).
% 59.55/59.55 cnf(598,plain,
% 59.55/59.55 (~P11(a1,a20,x5981,a19,a20,x5981)),
% 59.55/59.55 inference(scs_inference,[],[439,443,512,547,254,233,253,252,231])).
% 59.55/59.55 cnf(604,plain,
% 59.55/59.55 (~P9(a19,a20,a19,a1,x6041,x6042,x6041,x6042)),
% 59.55/59.55 inference(scs_inference,[],[439,443,475,512,547,553,557,254,233,253,252,231,215,214,255])).
% 59.55/59.55 cnf(616,plain,
% 59.55/59.55 (~P9(x6161,x6162,x6161,x6162,a20,a1,a20,a19)),
% 59.55/59.55 inference(scs_inference,[],[451,522,254,252])).
% 59.55/59.55 cnf(618,plain,
% 59.55/59.55 (~P9(a19,a20,x6181,x6182,a1,a20,x6181,x6182)),
% 59.55/59.55 inference(scs_inference,[],[451,522,541,254,252,233])).
% 59.55/59.55 cnf(620,plain,
% 59.55/59.55 (~P9(x6201,x6202,a19,a20,x6201,x6202,a19,a1)),
% 59.55/59.55 inference(scs_inference,[],[451,475,522,541,254,252,233,253])).
% 59.55/59.55 cnf(622,plain,
% 59.55/59.55 (~P11(x6221,x6222,x6221,a19,a1,a20)),
% 59.55/59.55 inference(scs_inference,[],[451,475,522,541,254,252,233,253,231])).
% 59.55/59.55 cnf(630,plain,
% 59.55/59.55 (~P11(a20,x6301,a19,a1,x6301,a19)),
% 59.55/59.55 inference(scs_inference,[],[451,467,475,522,541,574,254,252,233,253,231,214,215,255,216])).
% 59.55/59.55 cnf(636,plain,
% 59.55/59.55 (~P3(x6361,x6362,a19,a17)+P10(x6361,x6362,a3,a16)),
% 59.55/59.55 inference(scs_inference,[],[146,332,451,467,475,522,541,574,254,252,233,253,231,214,215,255,216,106,227,180])).
% 59.55/59.55 cnf(641,plain,
% 59.55/59.55 (~P10(x6411,x6412,x6413,x6414)+~P9(a19,a1,a1,a20,x6411,x6412,x6413,x6414)),
% 59.55/59.55 inference(scs_inference,[],[264,146,332,451,467,475,522,290,541,574,254,252,233,253,231,214,215,255,216,106,227,180,103,234,240])).
% 59.55/59.55 cnf(645,plain,
% 59.55/59.55 (~P9(a20,a1,a19,a1,x6451,x6452,x6451,x6452)),
% 59.55/59.55 inference(scs_inference,[],[437,254])).
% 59.55/59.55 cnf(647,plain,
% 59.55/59.55 (~P9(x6471,x6472,a20,a1,x6471,x6472,a19,a1)),
% 59.55/59.55 inference(scs_inference,[],[437,502,254,253])).
% 59.55/59.55 cnf(649,plain,
% 59.55/59.55 (~P9(a20,a19,x6491,x6492,a1,a20,x6491,x6492)),
% 59.55/59.55 inference(scs_inference,[],[437,502,537,254,253,252])).
% 59.55/59.55 cnf(653,plain,
% 59.55/59.55 (~P11(a19,a20,x6531,a1,a20,x6531)),
% 59.55/59.55 inference(scs_inference,[],[437,572,502,537,618,254,253,252,233,231])).
% 59.55/59.55 cnf(656,plain,
% 59.55/59.55 (~P11(x6561,x6562,x6562,a1,a19,a20)),
% 59.55/59.55 inference(scs_inference,[],[437,572,502,537,618,622,254,253,252,233,231,215])).
% 59.55/59.55 cnf(660,plain,
% 59.55/59.55 (~P11(x6601,x6601,x6602,a19,a20,a1)),
% 59.55/59.55 inference(scs_inference,[],[437,572,502,537,618,622,254,253,252,233,231,215,214,216])).
% 59.55/59.55 cnf(662,plain,
% 59.55/59.55 (~P9(a20,a19,a19,a1,x6621,x6622,x6621,x6622)),
% 59.55/59.55 inference(scs_inference,[],[437,572,502,512,537,618,622,254,253,252,233,231,215,214,216,255])).
% 59.55/59.55 cnf(670,plain,
% 59.55/59.55 (~P10(x6701,x6702,x6703,x6704)+~P9(a1,a20,a19,a1,x6701,x6702,x6703,x6704)),
% 59.55/59.55 inference(scs_inference,[],[143,147,417,354,437,310,572,502,512,537,618,622,254,253,252,233,231,215,214,216,255,227,88,90,104,240])).
% 59.55/59.55 cnf(677,plain,
% 59.55/59.55 (~P9(x6771,x6772,x6772,x6771,a1,a19,a20,a1)),
% 59.55/59.55 inference(scs_inference,[],[477,254])).
% 59.55/59.55 cnf(679,plain,
% 59.55/59.55 (~P9(a19,a20,x6791,x6792,a1,a19,x6791,x6792)),
% 59.55/59.55 inference(scs_inference,[],[576,477,254,233])).
% 59.55/59.55 cnf(683,plain,
% 59.55/59.55 (~P9(a20,a1,x6831,x6832,a19,a20,x6831,x6832)),
% 59.55/59.55 inference(scs_inference,[],[576,477,512,549,254,233,253,252])).
% 59.55/59.55 cnf(687,plain,
% 59.55/59.55 (~P11(x6871,x6871,x6872,a20,a19,a1)),
% 59.55/59.55 inference(scs_inference,[],[576,477,512,549,656,660,254,233,253,252,214,215])).
% 59.55/59.55 cnf(689,plain,
% 59.55/59.55 (~P9(a19,a20,a20,a1,x6891,x6892,x6891,x6892)),
% 59.55/59.55 inference(scs_inference,[],[576,477,512,549,656,660,254,233,253,252,214,215,255])).
% 59.55/59.55 cnf(691,plain,
% 59.55/59.55 (~P11(x6911,x6912,x6912,a1,a20,a19)),
% 59.55/59.55 inference(scs_inference,[],[576,477,512,549,656,660,254,233,253,252,214,215,255,216])).
% 59.55/59.55 cnf(699,plain,
% 59.55/59.55 (~P3(x6991,x6992,a20,a17)+P10(x6991,x6992,a3,a2)),
% 59.55/59.55 inference(scs_inference,[],[144,145,147,439,576,477,512,549,656,660,254,233,253,252,214,215,255,216,227,105,89,106,180])).
% 59.55/59.55 cnf(706,plain,
% 59.55/59.55 (~P9(x7061,x7062,x7062,x7061,a20,a1,a1,a19)),
% 59.55/59.55 inference(scs_inference,[],[514,254])).
% 59.55/59.55 cnf(708,plain,
% 59.55/59.55 (~P9(x7081,x7082,x7081,x7082,a20,a19,a20,a1)),
% 59.55/59.55 inference(scs_inference,[],[514,555,254,252])).
% 59.55/59.55 cnf(720,plain,
% 59.55/59.55 (~P9(a20,a19,a1,a19,x7201,x7202,x7201,x7202)),
% 59.55/59.55 inference(scs_inference,[],[510,514,555,570,687,578,254,252,233,231,253,214,215,255])).
% 59.55/59.55 cnf(730,plain,
% 59.55/59.55 (~P9(x7301,x7302,x7302,x7301,a1,a20,a19,a1)),
% 59.55/59.55 inference(scs_inference,[],[543,254])).
% 59.55/59.55 cnf(732,plain,
% 59.55/59.55 (~P9(x7321,x7322,x7321,x7322,a19,a1,a20,a1)),
% 59.55/59.55 inference(scs_inference,[],[543,564,254,252])).
% 59.55/59.55 cnf(740,plain,
% 59.55/59.55 (~P9(a1,a20,a20,a19,x7401,x7402,x7401,x7402)),
% 59.55/59.55 inference(scs_inference,[],[543,537,564,691,582,254,252,253,215,214,255])).
% 59.55/59.55 cnf(750,plain,
% 59.55/59.55 (~P9(a19,a1,a1,a20,x7501,x7502,x7502,x7501)),
% 59.55/59.55 inference(scs_inference,[],[568,254])).
% 59.55/59.55 cnf(752,plain,
% 59.55/59.55 (~P9(x7521,x7522,x7521,x7522,a19,a1,a19,a20)),
% 59.55/59.55 inference(scs_inference,[],[568,584,254,252])).
% 59.55/59.55 cnf(762,plain,
% 59.55/59.55 (~P9(a1,a20,a19,a20,x7621,x7622,x7621,x7622)),
% 59.55/59.55 inference(scs_inference,[],[592,568,584,598,630,653,254,252,215,253,214,216,255])).
% 59.55/59.55 cnf(772,plain,
% 59.55/59.55 (~P9(a1,a19,a19,a20,x7721,x7722,x7721,x7722)),
% 59.55/59.55 inference(scs_inference,[],[584,254])).
% 59.55/59.55 cnf(774,plain,
% 59.55/59.55 (~P9(x7741,x7742,x7741,x7742,a20,a19,a19,a1)),
% 59.55/59.55 inference(scs_inference,[],[662,584,254,252])).
% 59.55/59.55 cnf(790,plain,
% 59.55/59.55 (~P9(x7901,x7902,x7902,x7901,a20,a1,a20,a19)),
% 59.55/59.55 inference(scs_inference,[],[616,254])).
% 59.55/59.55 cnf(802,plain,
% 59.55/59.55 (~P11(a1,a20,a19,a1,a19,a20)),
% 59.55/59.55 inference(scs_inference,[],[568,618,590,616,254,252,253,255,231,215,214])).
% 59.55/59.55 cnf(804,plain,
% 59.55/59.55 (~P11(a19,a20,a1,a20,a19,a1)),
% 59.55/59.55 inference(scs_inference,[],[568,618,590,616,254,252,253,255,231,215,214,216])).
% 59.55/59.55 cnf(812,plain,
% 59.55/59.55 (~P9(x8121,x8122,a19,a1,x8122,x8121,a19,a20)),
% 59.55/59.55 inference(scs_inference,[],[469,254])).
% 59.55/59.55 cnf(814,plain,
% 59.55/59.55 (~P9(x8141,x8142,x8141,x8142,a19,a20,a20,a1)),
% 59.55/59.55 inference(scs_inference,[],[689,469,254,252])).
% 59.55/59.55 cnf(822,plain,
% 59.55/59.55 (~P9(a19,a20,a1,a20,x8221,x8222,x8221,x8222)),
% 59.55/59.55 inference(scs_inference,[],[662,618,689,469,802,804,254,252,215,214,253,255])).
% 59.55/59.55 cnf(828,plain,
% 59.55/59.55 (~P10(x8281,x8282,x8283,x8284)+~P9(a19,a1,a20,a1,x8281,x8282,x8283,x8284)),
% 59.55/59.55 inference(scs_inference,[],[453,396,662,618,689,616,469,802,804,254,252,215,214,253,255,227,88,240])).
% 59.55/59.55 cnf(845,plain,
% 59.55/59.55 (~P4(a19,x8451,a1)+~P2(a20,a20,x8451,a1)),
% 59.55/59.55 inference(scs_inference,[],[689,706,539,254,252,253,255,227])).
% 59.55/59.55 cnf(853,plain,
% 59.55/59.55 (~P9(x8531,x8532,x8531,x8532,a19,a20,a19,a1)),
% 59.55/59.55 inference(scs_inference,[],[604,594,254,252])).
% 59.55/59.55 cnf(865,plain,
% 59.55/59.55 (~P9(x8651,x8652,a19,a20,x8652,x8651,a19,a1)),
% 59.55/59.55 inference(scs_inference,[],[620,254])).
% 59.55/59.55 cnf(867,plain,
% 59.55/59.55 (~P9(x8671,x8672,x8671,x8672,a1,a20,a20,a19)),
% 59.55/59.55 inference(scs_inference,[],[740,620,254,252])).
% 59.55/59.55 cnf(879,plain,
% 59.55/59.55 (~P9(x8791,x8792,x8792,x8791,a20,a19,a19,a1)),
% 59.55/59.55 inference(scs_inference,[],[774,254])).
% 59.55/59.55 cnf(883,plain,
% 59.55/59.55 (~P11(a20,a19,a1,x8831,x8832,x8831)),
% 59.55/59.55 inference(scs_inference,[],[774,254,231,214])).
% 59.55/59.55 cnf(885,plain,
% 59.55/59.55 (~P11(x8851,x8852,x8852,a19,a20,a1)),
% 59.55/59.55 inference(scs_inference,[],[774,254,231,214,215])).
% 59.55/59.55 cnf(887,plain,
% 59.55/59.55 (~P11(x8871,x8871,x8872,a20,a1,a19)),
% 59.55/59.55 inference(scs_inference,[],[774,254,231,214,215,216])).
% 59.55/59.55 cnf(889,plain,
% 59.55/59.55 (~P9(x8891,x8892,x8891,x8892,a20,a1,a19,a1)),
% 59.55/59.55 inference(scs_inference,[],[645,774,254,231,214,215,216,252])).
% 59.55/59.55 cnf(893,plain,
% 59.55/59.55 (~P9(a1,a20,a19,a1,x8931,x8932,x8932,x8931)),
% 59.55/59.55 inference(scs_inference,[],[750,645,774,254,231,214,215,216,252,255,253])).
% 59.55/59.55 cnf(907,plain,
% 59.55/59.55 (~P11(a19,a20,a1,x9071,x9072,x9072)),
% 59.55/59.55 inference(scs_inference,[],[720,883,254,215])).
% 59.55/59.55 cnf(909,plain,
% 59.55/59.55 (~P11(a20,a1,a19,x9091,x9091,x9092)),
% 59.55/59.55 inference(scs_inference,[],[720,883,887,254,215,214])).
% 59.55/59.55 cnf(913,plain,
% 59.55/59.55 (~P9(a1,a19,a20,a1,x9131,x9132,x9132,x9131)),
% 59.55/59.55 inference(scs_inference,[],[677,720,883,885,887,254,215,214,216,252])).
% 59.55/59.55 cnf(925,plain,
% 59.55/59.55 (~P9(x9251,x9252,x9252,x9251,a19,a1,a20,a1)),
% 59.55/59.55 inference(scs_inference,[],[732,254])).
% 59.55/59.55 cnf(933,plain,
% 59.55/59.55 (~P9(x9331,x9332,x9331,x9332,a1,a19,a19,a20)),
% 59.55/59.55 inference(scs_inference,[],[772,732,907,909,254,215,216,214,252])).
% 59.55/59.55 cnf(939,plain,
% 59.55/59.55 (~P10(x9391,x9392,x9393,x9394)+~P9(a20,a1,a19,a1,x9391,x9392,x9393,x9394)),
% 59.55/59.55 inference(scs_inference,[],[471,772,649,730,732,907,909,254,215,216,214,252,255,253,240])).
% 59.55/59.55 cnf(941,plain,
% 59.55/59.55 (~P9(a20,a1,a19,a1,x9411,x9412,a2,a16)+~P3(x9411,x9412,a1,a17)),
% 59.55/59.55 inference(scs_inference,[],[471,772,649,730,732,907,909,254,215,216,214,252,255,253,240,294])).
% 59.55/59.55 cnf(944,plain,
% 59.55/59.55 (~P9(x9441,x9442,x9442,x9441,a19,a20,a20,a1)),
% 59.55/59.55 inference(scs_inference,[],[814,254])).
% 59.55/59.55 cnf(946,plain,
% 59.55/59.55 (~P11(x9461,x9462,x9461,a19,a20,a1)),
% 59.55/59.55 inference(scs_inference,[],[814,254,231])).
% 59.55/59.55 cnf(948,plain,
% 59.55/59.55 (~P11(a19,a20,a1,x9481,x9482,x9481)),
% 59.55/59.55 inference(scs_inference,[],[814,254,231,214])).
% 59.55/59.55 cnf(966,plain,
% 59.55/59.55 (~P9(x9661,x9662,x9662,x9661,a20,a19,a20,a1)),
% 59.55/59.55 inference(scs_inference,[],[708,254])).
% 59.55/59.55 cnf(970,plain,
% 59.55/59.55 (~P11(a20,a19,a1,x9701,x9702,x9702)),
% 59.55/59.55 inference(scs_inference,[],[708,946,254,215,214])).
% 59.55/59.55 cnf(972,plain,
% 59.55/59.55 (~P11(x9721,x9721,x9722,a19,a1,a20)),
% 59.55/59.55 inference(scs_inference,[],[708,946,254,215,214,216])).
% 59.55/59.55 cnf(976,plain,
% 59.55/59.55 (~P9(x9761,x9762,x9761,x9762,a20,a19,a1,a19)),
% 59.55/59.55 inference(scs_inference,[],[679,720,708,946,254,215,214,216,253,252])).
% 59.55/59.55 cnf(984,plain,
% 59.55/59.55 (~P10(x9841,x9842,x9843,x9844)+~P9(a1,a20,a20,a19,x9841,x9842,x9843,x9844)),
% 59.55/59.55 inference(scs_inference,[],[288,479,679,720,708,752,879,946,254,215,214,216,253,252,255,227,90,240])).
% 59.55/59.55 cnf(993,plain,
% 59.55/59.55 (~P9(x9931,x9932,x9932,x9931,a19,a1,a19,a20)),
% 59.55/59.55 inference(scs_inference,[],[752,254])).
% 59.55/59.55 cnf(1003,plain,
% 59.55/59.55 (~P9(a1,a20,x10031,x10032,a19,a1,x10032,x10031)),
% 59.55/59.55 inference(scs_inference,[],[683,752,893,948,972,254,215,216,214,253,255])).
% 59.55/59.55 cnf(1005,plain,
% 59.55/59.55 (~P9(x10051,x10052,x10051,x10052,a1,a20,a19,a20)),
% 59.55/59.55 inference(scs_inference,[],[683,762,752,893,948,972,254,215,216,214,253,255,252])).
% 59.55/59.55 cnf(1013,plain,
% 59.55/59.55 (~P9(x10131,x10132,x10132,x10131,a1,a20,a20,a19)),
% 59.55/59.55 inference(scs_inference,[],[867,254])).
% 59.55/59.55 cnf(1025,plain,
% 59.55/59.55 (~P9(a20,a1,a20,a19,x10251,x10252,x10252,x10251)),
% 59.55/59.55 inference(scs_inference,[],[814,790,867,970,254,231,215,216,253,214,252])).
% 59.55/59.55 cnf(1027,plain,
% 59.55/59.55 (~P9(a1,a19,x10271,x10272,a20,a1,x10272,x10271)),
% 59.55/59.55 inference(scs_inference,[],[814,790,867,913,970,254,231,215,216,253,214,252,255])).
% 59.55/59.55 cnf(1034,plain,
% 59.55/59.55 (~P9(x10341,x10342,x10342,x10341,a19,a20,a19,a1)),
% 59.55/59.55 inference(scs_inference,[],[853,254])).
% 59.55/59.55 cnf(1040,plain,
% 59.55/59.55 (~P9(x10401,x10402,x10401,x10402,a19,a20,a1,a20)),
% 59.55/59.55 inference(scs_inference,[],[867,822,853,944,254,253,255,252])).
% 59.55/59.55 cnf(1042,plain,
% 59.55/59.55 (~P10(x10421,x10422,x10423,x10424)+~P9(a1,a20,a1,a19,x10421,x10422,x10423,x10424)),
% 59.55/59.55 inference(scs_inference,[],[274,867,822,853,944,254,253,255,252,240])).
% 59.55/59.55 cnf(1044,plain,
% 59.55/59.55 (~P9(a1,a20,a1,a19,x10441,x10442,a3,a16)+~P3(x10441,x10442,a19,a17)),
% 59.55/59.55 inference(scs_inference,[],[274,867,822,853,944,254,253,255,252,240,636])).
% 59.55/59.55 cnf(1059,plain,
% 59.55/59.55 (~P9(x10591,x10592,x10592,x10591,a1,a19,a19,a20)),
% 59.55/59.55 inference(scs_inference,[],[933,254])).
% 59.55/59.55 cnf(1061,plain,
% 59.55/59.55 (~P9(x10611,x10612,x10612,x10611,a19,a1,a20,a19)),
% 59.55/59.55 inference(scs_inference,[],[879,933,254,253])).
% 59.55/59.55 cnf(1063,plain,
% 59.55/59.55 (~P9(x10631,x10632,a19,a1,x10632,x10631,a20,a1)),
% 59.55/59.55 inference(scs_inference,[],[879,933,925,254,253,255])).
% 59.55/59.55 cnf(1065,plain,
% 59.55/59.55 (~P9(a20,a19,a19,a1,x10651,x10652,x10652,x10651)),
% 59.55/59.55 inference(scs_inference,[],[879,933,925,254,253,255,252])).
% 59.55/59.55 cnf(1071,plain,
% 59.55/59.55 (~P10(x10711,x10712,x10713,x10714)+~P9(a20,a1,a1,a19,x10711,x10712,x10713,x10714)),
% 59.55/59.55 inference(scs_inference,[],[376,322,879,853,933,925,254,253,255,252,90,227,240])).
% 59.55/59.55 cnf(1081,plain,
% 59.55/59.55 (~P9(x10811,x10812,x10812,x10811,a20,a1,a19,a1)),
% 59.55/59.55 inference(scs_inference,[],[889,254])).
% 59.55/59.55 cnf(1096,plain,
% 59.55/59.55 (~P9(a20,a1,x10961,x10962,a20,a19,x10962,x10961)),
% 59.55/59.55 inference(scs_inference,[],[893,1025,254,255])).
% 59.55/59.55 cnf(1098,plain,
% 59.55/59.55 (~P9(x10981,x10982,x10982,x10981,a20,a1,a19,a20)),
% 59.55/59.55 inference(scs_inference,[],[944,893,1025,254,255,253])).
% 59.55/59.55 cnf(1100,plain,
% 59.55/59.55 (~P9(a19,a20,a20,a1,x11001,x11002,x11002,x11001)),
% 59.55/59.55 inference(scs_inference,[],[944,893,1025,254,255,253,252])).
% 59.55/59.55 cnf(1104,plain,
% 59.55/59.55 (~P11(a1,a20,a19,a19,a20,a1)),
% 59.55/59.55 inference(scs_inference,[],[944,893,1025,254,255,253,252,231,215])).
% 59.55/59.55 cnf(1110,plain,
% 59.55/59.55 (~P10(x11101,x11102,x11103,x11104)+~P9(a19,a1,a20,a19,x11101,x11102,x11103,x11104)),
% 59.55/59.55 inference(scs_inference,[],[352,944,893,1025,254,255,253,252,231,215,216,214,240])).
% 59.55/59.55 cnf(1112,plain,
% 59.55/59.55 (~P9(a19,a1,a20,a19,x11121,x11122,a3,a2)+~P3(x11121,x11122,a20,a17)),
% 59.55/59.55 inference(scs_inference,[],[352,944,893,1025,254,255,253,252,231,215,216,214,240,699])).
% 59.55/59.55 cnf(1135,plain,
% 59.55/59.55 (~P9(x11351,x11352,x11352,x11351,a20,a19,a1,a20)),
% 59.55/59.55 inference(scs_inference,[],[913,1013,1104,254,216,214,253])).
% 59.55/59.55 cnf(1139,plain,
% 59.55/59.55 (~P9(a20,a19,a20,a1,x11391,x11392,x11392,x11391)),
% 59.55/59.55 inference(scs_inference,[],[913,966,1013,1059,1104,254,216,214,253,255,252])).
% 59.55/59.55 cnf(1148,plain,
% 59.55/59.55 (~P9(x11481,x11482,x11482,x11481,a20,a19,a1,a19)),
% 59.55/59.55 inference(scs_inference,[],[976,254])).
% 59.55/59.55 cnf(1152,plain,
% 59.55/59.55 (~P9(a19,a1,a20,a19,x11521,x11522,x11522,x11521)),
% 59.55/59.55 inference(scs_inference,[],[976,1065,254,255,253])).
% 59.55/59.55 cnf(1156,plain,
% 59.55/59.55 (~P10(x11561,x11562,x11563,x11564)+~P9(a19,a20,a19,a1,x11561,x11562,x11563,x11564)),
% 59.55/59.55 inference(scs_inference,[],[364,1013,976,1065,254,255,253,252,240])).
% 59.55/59.55 cnf(1158,plain,
% 59.55/59.55 (~P9(a19,a20,a19,a1,x11581,x11582,a2,a16)+~P3(x11581,x11582,a1,a17)),
% 59.55/59.55 inference(scs_inference,[],[364,1013,976,1065,254,255,253,252,240,294])).
% 59.55/59.55 cnf(1179,plain,
% 59.55/59.55 (~P9(x11791,x11792,x11792,x11791,a19,a20,a1,a19)),
% 59.55/59.55 inference(scs_inference,[],[1003,1059,1061,254,255,253])).
% 59.55/59.55 cnf(1183,plain,
% 59.55/59.55 (~P10(x11831,x11832,x11833,x11834)+~P9(a20,a1,a19,a20,x11831,x11832,x11833,x11834)),
% 59.55/59.55 inference(scs_inference,[],[392,993,1003,1059,1061,254,255,253,252,240])).
% 59.55/59.55 cnf(1185,plain,
% 59.55/59.55 (~P9(a20,a1,a19,a20,x11851,x11852,a3,a2)+~P3(x11851,x11852,a20,a17)),
% 59.55/59.55 inference(scs_inference,[],[392,993,1003,1059,1061,254,255,253,252,240,699])).
% 59.55/59.55 cnf(1187,plain,
% 59.55/59.55 (~P3(x11871,x11872,a17,a20)+~P9(a20,a1,a19,a20,x11871,x11872,a3,a2)),
% 59.55/59.55 inference(scs_inference,[],[392,993,1003,1059,1061,254,255,253,252,240,699,166])).
% 59.55/59.55 cnf(1206,plain,
% 59.55/59.55 (~P9(a19,a20,x12061,x12062,a20,a1,x12062,x12061)),
% 59.55/59.55 inference(scs_inference,[],[1065,1100,254,253,255])).
% 59.55/59.55 cnf(1208,plain,
% 59.55/59.55 (~P9(a1,a19,a19,a20,x12081,x12082,x12082,x12081)),
% 59.55/59.55 inference(scs_inference,[],[1059,1065,1100,254,253,255,252])).
% 59.55/59.55 cnf(1215,plain,
% 59.55/59.55 (~P9(x12151,x12152,x12152,x12151,a1,a20,a19,a20)),
% 59.55/59.55 inference(scs_inference,[],[1005,254])).
% 59.55/59.55 cnf(1219,plain,
% 59.55/59.55 (~P9(a19,a1,x12191,x12192,a19,a20,x12192,x12191)),
% 59.55/59.55 inference(scs_inference,[],[1005,1139,812,254,255,253])).
% 59.55/59.55 cnf(1225,plain,
% 59.55/59.55 (~P11(a1,a19,a20,a20,a19,a1)),
% 59.55/59.55 inference(scs_inference,[],[1005,1139,812,1063,254,255,253,252,231,215])).
% 59.55/59.55 cnf(1231,plain,
% 59.55/59.55 (~P10(x12311,x12312,x12313,x12314)+~P9(a20,a19,a1,a20,x12311,x12312,x12313,x12314)),
% 59.55/59.55 inference(scs_inference,[],[432,1005,1139,812,1063,254,255,253,252,231,215,216,214,240])).
% 59.55/59.55 cnf(1233,plain,
% 59.55/59.55 (~P9(a20,a19,a1,a20,x12331,x12332,a3,a16)+~P3(x12331,x12332,a19,a17)),
% 59.55/59.55 inference(scs_inference,[],[432,1005,1139,812,1063,254,255,253,252,231,215,216,214,240,636])).
% 59.55/59.55 cnf(1261,plain,
% 59.55/59.55 (~P9(a20,a19,a1,a20,x12611,x12612,x12612,x12611)),
% 59.55/59.55 inference(scs_inference,[],[1027,865,1098,1135,1225,254,216,214,253,255,252])).
% 59.55/59.55 cnf(1271,plain,
% 59.55/59.55 (~P9(x12711,x12712,a20,a19,x12712,x12711,a1,a20)),
% 59.55/59.55 inference(scs_inference,[],[1096,1135,254,255])).
% 59.55/59.55 cnf(1273,plain,
% 59.55/59.55 (~P9(x12731,x12732,x12732,x12731,a1,a19,a20,a19)),
% 59.55/59.55 inference(scs_inference,[],[1096,1135,1148,254,255,253])).
% 59.55/59.55 cnf(1275,plain,
% 59.55/59.55 (~P9(a20,a19,a1,a19,x12751,x12752,x12752,x12751)),
% 59.55/59.55 inference(scs_inference,[],[1096,1135,1148,254,255,253,252])).
% 59.55/59.55 cnf(1277,plain,
% 59.55/59.55 (~P10(x12771,x12772,x12773,x12774)+~P9(a20,a19,a1,a19,x12771,x12772,x12773,x12774)),
% 59.55/59.55 inference(scs_inference,[],[508,1096,1135,1148,254,255,253,252,240])).
% 59.55/59.55 cnf(1279,plain,
% 59.55/59.55 (~P9(a20,a19,a1,a19,x12791,x12792,a2,a16)+~P3(x12791,x12792,a1,a17)),
% 59.55/59.55 inference(scs_inference,[],[508,1096,1135,1148,254,255,253,252,240,294])).
% 59.55/59.55 cnf(1281,plain,
% 59.55/59.55 (~P3(x12811,x12812,a17,a1)+~P9(a20,a19,a1,a19,x12811,x12812,a2,a16)),
% 59.55/59.55 inference(scs_inference,[],[508,1096,1135,1148,254,255,253,252,240,294,166])).
% 59.55/59.55 cnf(1296,plain,
% 59.55/59.55 (~P9(x12961,x12962,x12962,x12961,a19,a20,a1,a20)),
% 59.55/59.55 inference(scs_inference,[],[1040,254])).
% 59.55/59.55 cnf(1302,plain,
% 59.55/59.55 (~P9(a20,a1,x13021,x13022,a19,a20,x13022,x13021)),
% 59.55/59.55 inference(scs_inference,[],[1040,1152,1208,1206,254,253,255,252])).
% 59.55/59.55 cnf(1309,plain,
% 59.55/59.55 (~P9(a1,a19,x13091,x13092,a19,a20,x13092,x13091)),
% 59.55/59.55 inference(scs_inference,[],[1219,254])).
% 59.55/59.55 cnf(1317,plain,
% 59.55/59.55 (~P10(x13171,x13172,x13173,x13174)+~P9(a19,a20,a1,a20,x13171,x13172,x13173,x13174)),
% 59.55/59.55 inference(scs_inference,[],[541,1219,1148,1215,1275,254,255,253,252,240])).
% 59.55/59.55 cnf(1319,plain,
% 59.55/59.55 (~P9(a19,a20,a1,a20,x13191,x13192,a3,a16)+~P3(x13191,x13192,a19,a17)),
% 59.55/59.55 inference(scs_inference,[],[541,1219,1148,1215,1275,254,255,253,252,240,636])).
% 59.55/59.55 cnf(1321,plain,
% 59.55/59.55 (~P3(x13211,x13212,a17,a19)+~P9(a19,a20,a1,a20,x13211,x13212,a3,a16)),
% 59.55/59.55 inference(scs_inference,[],[541,1219,1148,1215,1275,254,255,253,252,240,636,166])).
% 59.55/59.55 cnf(1344,plain,
% 59.55/59.55 (~P10(x13441,x13442,x13443,x13444)+~P9(a1,a20,a19,a20,x13441,x13442,x13443,x13444)),
% 59.55/59.55 inference(scs_inference,[],[547,1179,1261,1271,1309,254,253,255,252,240])).
% 59.55/59.55 cnf(1346,plain,
% 59.55/59.55 (~P9(a1,a20,a19,a20,x13461,x13462,a3,a2)+~P3(x13461,x13462,a20,a17)),
% 59.55/59.55 inference(scs_inference,[],[547,1179,1261,1271,1309,254,253,255,252,240,699])).
% 59.55/59.55 cnf(1348,plain,
% 59.55/59.55 (~P3(x13481,x13482,a17,a20)+~P9(a1,a20,a19,a20,x13481,x13482,a3,a2)),
% 59.55/59.55 inference(scs_inference,[],[547,1179,1261,1271,1309,254,253,255,252,240,699,166])).
% 59.55/59.55 cnf(1379,plain,
% 59.55/59.55 (~P9(x13791,x13792,a19,a20,x13792,x13791,a1,a20)),
% 59.55/59.55 inference(scs_inference,[],[1296,1302,254,255])).
% 59.55/59.55 cnf(1383,plain,
% 59.55/59.55 (~P10(x13831,x13832,x13833,x13834)+~P9(a1,a19,a19,a20,x13831,x13832,x13833,x13834)),
% 59.55/59.55 inference(scs_inference,[],[572,1296,1302,254,255,252,240])).
% 59.55/59.55 cnf(1385,plain,
% 59.55/59.55 (~P9(a1,a19,a19,a20,x13851,x13852,a2,a16)+~P3(x13851,x13852,a1,a17)),
% 59.55/59.55 inference(scs_inference,[],[572,1296,1302,254,255,252,240,294])).
% 59.55/59.55 cnf(1387,plain,
% 59.55/59.55 (~P3(x13871,x13872,a17,a1)+~P9(a1,a19,a19,a20,x13871,x13872,a2,a16)),
% 59.55/59.55 inference(scs_inference,[],[572,1296,1302,254,255,252,240,294,166])).
% 59.55/59.55 cnf(1405,plain,
% 59.55/59.55 (P1(a1,a19,a16)),
% 59.55/59.55 inference(scs_inference,[],[288,336,88,155])).
% 59.55/59.55 cnf(1411,plain,
% 59.55/59.55 (~E(a16,a20)),
% 59.55/59.55 inference(scs_inference,[],[150,1405,90])).
% 59.55/59.55 cnf(1413,plain,
% 59.55/59.55 (~P10(x14131,x14132,x14133,x14134)+~P9(a19,a20,a1,a19,x14131,x14132,x14133,x14134)),
% 59.55/59.55 inference(scs_inference,[],[150,1405,576,90,89,240])).
% 59.55/59.55 cnf(1420,plain,
% 59.55/59.55 (~P10(x14201,x14202,x14203,x14204)+~P9(a1,a19,a20,a1,x14201,x14202,x14203,x14204)),
% 59.55/59.55 inference(scs_inference,[],[276,240])).
% 59.55/59.55 cnf(1422,plain,
% 59.55/59.55 (~P9(a1,a19,a20,a1,x14221,x14222,a2,a16)+~P3(x14221,x14222,a1,a17)),
% 59.55/59.55 inference(scs_inference,[],[276,240,294])).
% 59.55/59.55 cnf(1445,plain,
% 59.55/59.55 (~P10(x14451,x14452,x14453,x14454)+~P9(a20,a19,a19,a1,x14451,x14452,x14453,x14454)),
% 59.55/59.55 inference(scs_inference,[],[407,240])).
% 59.55/59.55 cnf(1447,plain,
% 59.55/59.55 (~P9(a20,a19,a19,a1,x14471,x14472,a3,a16)+~P3(x14471,x14472,a19,a17)),
% 59.55/59.55 inference(scs_inference,[],[407,240,636])).
% 59.55/59.55 cnf(1449,plain,
% 59.55/59.55 (~P3(x14491,x14492,a17,a19)+~P9(a20,a19,a19,a1,x14491,x14492,a3,a16)),
% 59.55/59.55 inference(scs_inference,[],[407,240,636,166])).
% 59.55/59.55 cnf(1471,plain,
% 59.55/59.55 (~P10(x14711,x14712,x14713,x14714)+~P9(a19,a20,a20,a1,x14711,x14712,x14713,x14714)),
% 59.55/59.55 inference(scs_inference,[],[441,240])).
% 59.55/59.55 cnf(1473,plain,
% 59.55/59.55 (~P9(a19,a20,a20,a1,x14731,x14732,a3,a2)+~P3(x14731,x14732,a20,a17)),
% 59.55/59.55 inference(scs_inference,[],[441,240,699])).
% 59.55/59.55 cnf(1496,plain,
% 59.55/59.55 (~P10(x14961,x14962,x14963,x14964)+~P9(a1,a19,a20,a19,x14961,x14962,x14963,x14964)),
% 59.55/59.55 inference(scs_inference,[],[510,240])).
% 59.55/59.55 cnf(1498,plain,
% 59.55/59.55 (~P9(a1,a19,a20,a19,x14981,x14982,a2,a16)+~P3(x14981,x14982,a1,a17)),
% 59.55/59.55 inference(scs_inference,[],[510,240,294])).
% 59.55/59.55 cnf(1500,plain,
% 59.55/59.55 (~P3(x15001,x15002,a17,a1)+~P9(a1,a19,a20,a19,x15001,x15002,a2,a16)),
% 59.55/59.55 inference(scs_inference,[],[510,240,294,166])).
% 59.55/59.55 cnf(1938,plain,
% 59.55/59.55 (~P4(x19381,x19382,a1)+~E(x19381,a19)+~P2(a20,a20,x19382,a1)),
% 59.55/59.55 inference(scs_inference,[],[845,139])).
% 59.55/59.55 cnf(1978,plain,
% 59.55/59.55 (P1(a2,a1,a16)),
% 59.55/59.55 inference(scs_inference,[],[142,1411,2,151])).
% 59.55/59.55 cnf(1980,plain,
% 59.55/59.55 (P3(a3,a2,a20,a17)),
% 59.55/59.55 inference(scs_inference,[],[142,1411,147,2,151,165])).
% 59.55/59.55 cnf(1982,plain,
% 59.55/59.55 (P1(a1,a16,a2)),
% 59.55/59.55 inference(scs_inference,[],[142,1411,147,2,151,165,152])).
% 59.55/59.55 cnf(1986,plain,
% 59.55/59.55 (P3(f8(a3,a17,a21,a18),a3,a3,a18)),
% 59.55/59.55 inference(scs_inference,[],[142,1411,149,147,2,151,165,152,699,187])).
% 59.55/59.55 cnf(1988,plain,
% 59.55/59.55 (P3(a20,a17,a2,a3)),
% 59.55/59.55 inference(scs_inference,[],[142,1411,149,147,2,151,165,152,699,187,166])).
% 59.55/59.55 cnf(1992,plain,
% 59.55/59.55 (P1(a16,a16,a2)),
% 59.55/59.55 inference(scs_inference,[],[142,1411,149,147,2,151,165,152,699,187,166,180,155])).
% 59.55/59.55 cnf(1994,plain,
% 59.55/59.55 (P9(a3,a2,x19941,x19942,a3,a2,x19941,x19942)),
% 59.55/59.55 inference(scs_inference,[],[142,1411,149,147,2,151,165,152,699,187,166,180,155,225])).
% 59.55/59.55 cnf(1996,plain,
% 59.55/59.55 (P1(a3,a2,a2)),
% 59.55/59.55 inference(scs_inference,[],[142,1411,149,147,2,151,165,152,699,187,166,180,155,225,160])).
% 59.55/59.55 cnf(1998,plain,
% 59.55/59.55 (P9(x19981,x19982,a3,a2,x19981,x19982,a3,a2)),
% 59.55/59.55 inference(scs_inference,[],[142,1411,149,147,2,151,165,152,699,187,166,180,155,225,160,253])).
% 59.55/59.55 cnf(2000,plain,
% 59.55/59.55 (P9(a3,a2,a3,a2,x20001,x20002,x20001,x20002)),
% 59.55/59.55 inference(scs_inference,[],[142,1411,149,147,2,151,165,152,699,187,166,180,155,225,160,253,255])).
% 59.55/59.55 cnf(2002,plain,
% 59.55/59.55 (P10(x20021,x20022,x20021,x20022)),
% 59.55/59.55 inference(scs_inference,[],[142,1411,149,147,2,151,165,152,699,187,166,180,155,225,160,253,255,233])).
% 59.55/59.55 cnf(2006,plain,
% 59.55/59.55 (P10(a2,a3,a3,a2)),
% 59.55/59.55 inference(scs_inference,[],[142,1411,149,147,2,151,165,152,699,187,166,180,155,225,160,253,255,233,164,163])).
% 59.55/59.55 cnf(2008,plain,
% 59.55/59.55 (P9(a2,a3,x20081,x20082,a3,a2,x20081,x20082)),
% 59.55/59.55 inference(scs_inference,[],[142,1411,149,147,2,151,165,152,699,187,166,180,155,225,160,253,255,233,164,163,254])).
% 59.55/59.55 cnf(2012,plain,
% 59.55/59.55 (P6(a2,a2,a3,a2)),
% 59.55/59.55 inference(scs_inference,[],[142,1411,471,149,147,2,151,165,152,699,187,166,180,155,225,160,253,255,233,164,163,254,157,236])).
% 59.55/59.55 cnf(2016,plain,
% 59.55/59.55 (P1(a3,a3,f14(a2,a2,a2,a2,a3,a3))),
% 59.55/59.55 inference(scs_inference,[],[142,1411,471,149,147,2,151,165,152,699,187,166,180,155,225,160,253,255,233,164,163,254,157,236,228,206])).
% 59.55/59.55 cnf(2020,plain,
% 59.55/59.55 (P5(a2,a2,a2,a2)),
% 59.55/59.55 inference(scs_inference,[],[142,1411,471,149,147,2,151,165,152,699,187,166,180,155,225,160,253,255,233,164,163,254,157,236,228,206,207,251])).
% 59.55/59.55 cnf(2022,plain,
% 59.55/59.55 (P6(a2,a3,a2,a2)),
% 59.55/59.55 inference(scs_inference,[],[142,1411,471,149,147,2,151,165,152,699,187,166,180,155,225,160,253,255,233,164,163,254,157,236,228,206,207,251,170])).
% 59.55/59.55 cnf(2024,plain,
% 59.55/59.55 (P6(a2,a2,a2,a3)),
% 59.55/59.55 inference(scs_inference,[],[142,1411,471,149,147,2,151,165,152,699,187,166,180,155,225,160,253,255,233,164,163,254,157,236,228,206,207,251,170,171])).
% 59.55/59.55 cnf(2028,plain,
% 59.55/59.55 (P9(a2,a2,a2,a2,a2,a2,a2,a2)),
% 59.55/59.55 inference(scs_inference,[],[142,1411,471,149,147,2,151,165,152,699,187,166,180,155,225,160,253,255,233,164,163,254,157,236,228,206,207,251,170,171,224,226])).
% 59.55/59.55 cnf(2030,plain,
% 59.55/59.55 (P8(a2,a2,a3,a2,a2,a2,a3,a2)),
% 59.55/59.55 inference(scs_inference,[],[142,1411,471,149,147,2,151,165,152,699,187,166,180,155,225,160,253,255,233,164,163,254,157,236,228,206,207,251,170,171,224,226,257])).
% 59.55/59.55 cnf(2032,plain,
% 59.55/59.55 (P8(a2,a3,a2,a2,a3,a2,a2,a2)),
% 59.55/59.55 inference(scs_inference,[],[142,1411,471,149,147,2,151,165,152,699,187,166,180,155,225,160,253,255,233,164,163,254,157,236,228,206,207,251,170,171,224,226,257,258])).
% 59.55/59.55 cnf(2034,plain,
% 59.55/59.55 (P8(a3,a2,a3,a2,a2,a2,a2,a2)),
% 59.55/59.55 inference(scs_inference,[],[142,1411,471,149,147,2,151,165,152,699,187,166,180,155,225,160,253,255,233,164,163,254,157,236,228,206,207,251,170,171,224,226,257,258,259])).
% 59.55/59.55 cnf(2039,plain,
% 59.55/59.55 (P6(a3,a2,a2,a2)),
% 59.55/59.55 inference(scs_inference,[],[2022,169])).
% 59.55/59.55 cnf(2041,plain,
% 59.55/59.55 (P8(a3,a2,a2,a2,a2,a3,a2,a2)),
% 59.55/59.55 inference(scs_inference,[],[2022,2032,169,256])).
% 59.55/59.55 cnf(2043,plain,
% 59.55/59.55 (P8(a2,a3,a3,a2,a2,a2,a2,a2)),
% 59.55/59.55 inference(scs_inference,[],[2022,2032,2034,169,256,258])).
% 59.55/59.55 cnf(2047,plain,
% 59.55/59.55 (P8(a2,a2,a2,a3,a2,a2,a3,a2)),
% 59.55/59.55 inference(scs_inference,[],[2022,2032,2034,169,256,258,224,257])).
% 59.55/59.55 cnf(2049,plain,
% 59.55/59.55 (P9(x20491,x20492,x20491,x20492,a3,a2,a3,a2)),
% 59.55/59.55 inference(scs_inference,[],[2000,2022,2032,2034,169,256,258,224,257,252])).
% 59.55/59.55 cnf(2053,plain,
% 59.55/59.55 (P1(a16,a1,a2)),
% 59.55/59.55 inference(scs_inference,[],[2000,1982,2022,2030,2032,2034,169,256,258,224,257,252,259,151])).
% 59.55/59.55 cnf(2055,plain,
% 59.55/59.55 (P1(a2,a16,a1)),
% 59.55/59.55 inference(scs_inference,[],[2000,1978,1982,2022,2030,2032,2034,169,256,258,224,257,252,259,151,152])).
% 59.55/59.55 cnf(2059,plain,
% 59.55/59.55 (P9(x20591,x20592,x20593,x20594,x20591,x20592,x20593,x20594)),
% 59.55/59.55 inference(scs_inference,[],[2002,2000,1978,1982,1988,2022,2030,2032,2034,169,256,258,224,257,252,259,151,152,165,225])).
% 59.55/59.55 cnf(2061,plain,
% 59.55/59.55 (P9(x20611,x20612,a2,a3,x20611,x20612,a3,a2)),
% 59.55/59.55 inference(scs_inference,[],[2002,2000,2008,1978,1982,1988,2022,2030,2032,2034,169,256,258,224,257,252,259,151,152,165,225,253])).
% 59.55/59.55 cnf(2063,plain,
% 59.55/59.55 (P1(x20631,x20632,x20632)),
% 59.55/59.55 inference(scs_inference,[],[2002,2000,2008,1978,1982,1988,2022,2030,2032,2034,169,256,258,224,257,252,259,151,152,165,225,253,160])).
% 59.55/59.55 cnf(2065,plain,
% 59.55/59.55 (P9(a2,a3,a3,a2,x20651,x20652,x20651,x20652)),
% 59.55/59.55 inference(scs_inference,[],[2002,2000,2008,1978,1982,1988,2022,2030,2032,2034,169,256,258,224,257,252,259,151,152,165,225,253,160,255])).
% 59.55/59.55 cnf(2067,plain,
% 59.55/59.55 (P10(x20671,x20672,x20672,x20671)),
% 59.55/59.55 inference(scs_inference,[],[2002,2000,2008,1978,1982,1988,2022,2030,2032,2034,169,256,258,224,257,252,259,151,152,165,225,253,160,255,164])).
% 59.55/59.55 cnf(2069,plain,
% 59.55/59.55 (P3(a3,a2,a17,a20)),
% 59.55/59.55 inference(scs_inference,[],[2002,1980,2000,2008,1978,1982,1988,2022,2030,2032,2034,169,256,258,224,257,252,259,151,152,165,225,253,160,255,164,166])).
% 59.55/59.55 cnf(2077,plain,
% 59.55/59.55 (P6(a2,a2,a3,a3)),
% 59.55/59.55 inference(scs_inference,[],[2002,1980,1998,2000,2008,1978,1982,1988,2022,2024,2030,2032,2034,479,352,148,169,256,258,224,257,252,259,151,152,165,225,253,160,255,164,166,187,254,135,136,185])).
% 59.55/59.55 cnf(2085,plain,
% 59.55/59.55 (P9(a3,a2,x20851,x20852,a3,a2,x20851,x20852)),
% 59.55/59.55 inference(rename_variables,[],[1994])).
% 59.55/59.55 cnf(2094,plain,
% 59.55/59.55 (P6(a2,f14(a2,a2,a2,a2,a3,a3),a3,a3)),
% 59.55/59.55 inference(scs_inference,[],[2002,1980,1994,2085,1998,2000,2008,1978,1982,1988,2006,2020,2022,2024,2028,2030,2032,2034,2016,647,1081,1034,479,1100,352,148,169,256,258,224,257,252,259,151,152,165,225,253,160,255,164,166,187,254,135,136,185,117,118,119,120,245,263,182,236])).
% 59.55/59.55 cnf(2097,plain,
% 59.55/59.55 (P5(a3,a2,a3,a2)),
% 59.55/59.55 inference(scs_inference,[],[2002,1980,1994,2085,1998,2000,2008,1978,1982,1988,2006,2020,2022,2024,2028,2030,2032,2034,2016,647,1081,1034,479,1100,352,148,169,256,258,224,257,252,259,151,152,165,225,253,160,255,164,166,187,254,135,136,185,117,118,119,120,245,263,182,236,243])).
% 59.55/59.55 cnf(2099,plain,
% 59.55/59.55 (P4(a3,a2,a2)),
% 59.55/59.55 inference(scs_inference,[],[2002,1980,1994,2085,1998,2000,2008,1978,1982,1988,1996,2006,2020,2022,2024,2028,2030,2032,2034,2016,647,1081,1034,479,1100,352,148,169,256,258,224,257,252,259,151,152,165,225,253,160,255,164,166,187,254,135,136,185,117,118,119,120,245,263,182,236,243,161])).
% 59.55/59.55 cnf(2101,plain,
% 59.55/59.55 (P2(a2,a2,a2,a2)),
% 59.55/59.55 inference(scs_inference,[],[2002,1980,1994,2085,1998,2000,2008,1978,1982,1988,1996,2006,2020,2022,2024,2028,2030,2032,2034,2016,647,1081,1034,479,1100,352,148,169,256,258,224,257,252,259,151,152,165,225,253,160,255,164,166,187,254,135,136,185,117,118,119,120,245,263,182,236,243,161,184])).
% 59.55/59.55 cnf(2103,plain,
% 59.55/59.55 (P3(a2,a2,a2,a2)),
% 59.61/59.56 inference(scs_inference,[],[2002,1980,1994,2085,1998,2000,2008,1978,1982,1988,1996,2006,2020,2022,2024,2028,2030,2032,2034,2016,647,1081,1034,479,1100,352,148,169,256,258,224,257,252,259,151,152,165,225,253,160,255,164,166,187,254,135,136,185,117,118,119,120,245,263,182,236,243,161,184,242])).
% 59.61/59.56 cnf(2105,plain,
% 59.61/59.56 (P9(a2,a2,a2,a2,a2,a2,a2,a3)),
% 59.61/59.56 inference(scs_inference,[],[2002,1980,1994,2085,1998,2000,2008,1978,1982,1988,1996,2006,2020,2022,2024,2028,2030,2032,2034,2016,647,1081,1034,479,1100,352,148,169,256,258,224,257,252,259,151,152,165,225,253,160,255,164,166,187,254,135,136,185,117,118,119,120,245,263,182,236,243,161,184,242,227])).
% 59.61/59.56 cnf(2107,plain,
% 59.61/59.56 (P3(a3,a2,a3,a2)),
% 59.61/59.56 inference(scs_inference,[],[2002,1980,1994,2085,1998,2000,2008,1978,1982,1988,1996,2006,2020,2022,2024,2028,2030,2032,2034,2016,647,1081,1034,479,1100,352,148,169,256,258,224,257,252,259,151,152,165,225,253,160,255,164,166,187,254,135,136,185,117,118,119,120,245,263,182,236,243,161,184,242,227,241])).
% 59.61/59.56 cnf(2108,plain,
% 59.61/59.56 (P9(a3,a2,a3,a2,x21081,x21082,x21081,x21082)),
% 59.61/59.56 inference(rename_variables,[],[2000])).
% 59.61/59.56 cnf(2110,plain,
% 59.61/59.56 (P3(a3,a3,a2,a2)),
% 59.61/59.56 inference(scs_inference,[],[2002,1980,1994,2085,1998,2000,2008,1978,1982,1988,1996,2006,2020,2022,2024,2028,2030,2032,2034,2016,647,1081,1034,479,1100,352,148,169,256,258,224,257,252,259,151,152,165,225,253,160,255,164,166,187,254,135,136,185,117,118,119,120,245,263,182,236,243,161,184,242,227,241,181])).
% 59.61/59.56 cnf(2114,plain,
% 59.61/59.56 (P5(a2,a2,a3,a3)),
% 59.61/59.56 inference(scs_inference,[],[2002,1980,1994,2085,1998,2000,2108,2008,1978,1982,1988,1996,2006,2020,2022,2024,2028,2030,2032,2034,2016,647,1081,1034,479,1100,352,148,169,256,258,224,257,252,259,151,152,165,225,253,160,255,164,166,187,254,135,136,185,117,118,119,120,245,263,182,236,243,161,184,242,227,241,181,186,251])).
% 59.61/59.56 cnf(2117,plain,
% 59.61/59.56 (P5(f7(a2,a2,a2),a2,f7(a2,a2,a2),a2)),
% 59.61/59.56 inference(scs_inference,[],[2002,1980,1994,2085,1998,2000,2108,2008,1978,1982,1988,1996,2006,2020,2022,2024,2028,2030,2032,2034,2016,647,1081,1034,479,1100,352,148,169,256,258,224,257,252,259,151,152,165,225,253,160,255,164,166,187,254,135,136,185,117,118,119,120,245,263,182,236,243,161,184,242,227,241,181,186,251,156])).
% 59.61/59.56 cnf(2119,plain,
% 59.61/59.56 (P5(a3,a3,a2,a2)),
% 59.61/59.56 inference(scs_inference,[],[2002,1980,1994,2085,1998,2000,2108,2008,1978,1982,1988,1996,2006,2020,2022,2024,2028,2030,2032,2034,2016,647,1081,1034,479,1100,352,148,169,256,258,224,257,252,259,151,152,165,225,253,160,255,164,166,187,254,135,136,185,117,118,119,120,245,263,182,236,243,161,184,242,227,241,181,186,251,156,167])).
% 59.61/59.56 cnf(2121,plain,
% 59.61/59.56 (P5(a3,a2,a2,a3)),
% 59.61/59.56 inference(scs_inference,[],[2002,1980,1994,2085,1998,2000,2108,2008,1978,1982,1988,1996,2006,2020,2022,2024,2028,2030,2032,2034,2016,647,1081,1034,479,1100,352,148,169,256,258,224,257,252,259,151,152,165,225,253,160,255,164,166,187,254,135,136,185,117,118,119,120,245,263,182,236,243,161,184,242,227,241,181,186,251,156,167,168])).
% 59.61/59.56 cnf(2123,plain,
% 59.61/59.56 (P6(a2,a3,a2,a3)),
% 59.61/59.56 inference(scs_inference,[],[2002,1980,1994,2085,1998,2000,2108,2008,1978,1982,1988,1996,2006,2020,2022,2024,2028,2030,2032,2034,2016,647,1081,1034,479,1100,352,148,169,256,258,224,257,252,259,151,152,165,225,253,160,255,164,166,187,254,135,136,185,117,118,119,120,245,263,182,236,243,161,184,242,227,241,181,186,251,156,167,168,170])).
% 59.61/59.56 cnf(2125,plain,
% 59.61/59.56 (P9(a3,a2,a2,a2,a2,a2,a3,a2)),
% 59.61/59.56 inference(scs_inference,[],[2002,1980,1994,2085,1998,2000,2108,2008,1978,1982,1988,1996,2006,2020,2022,2024,2028,2030,2032,2034,2016,647,1081,1034,479,1100,352,148,169,256,258,224,257,252,259,151,152,165,225,253,160,255,164,166,187,254,135,136,185,117,118,119,120,245,263,182,236,243,161,184,242,227,241,181,186,251,156,167,168,170,226])).
% 59.61/59.56 cnf(2131,plain,
% 59.61/59.56 (P8(f7(a2,a2,a2),a2,a2,a2,f7(a2,a2,a2),a2,a2,a2)),
% 59.61/59.56 inference(scs_inference,[],[2002,1980,1994,2085,1998,2000,2108,2008,1978,1982,1988,1996,2006,2020,2022,2024,2028,2030,2032,2034,2016,647,1081,1034,479,1100,352,148,169,256,258,224,257,252,259,151,152,165,225,253,160,255,164,166,187,254,135,136,185,117,118,119,120,245,263,182,236,243,161,184,242,227,241,181,186,251,156,167,168,170,226,158,173,223])).
% 59.61/59.56 cnf(2133,plain,
% 59.61/59.56 (P1(a2,a2,f4(a2,a2,a2))),
% 59.61/59.56 inference(scs_inference,[],[2002,1980,1994,2085,1998,2000,2108,2008,1978,1982,1988,1996,2006,2020,2022,2024,2028,2030,2032,2034,2016,647,1081,1034,479,1100,352,148,169,256,258,224,257,252,259,151,152,165,225,253,160,255,164,166,187,254,135,136,185,117,118,119,120,245,263,182,236,243,161,184,242,227,241,181,186,251,156,167,168,170,226,158,173,223,176])).
% 59.61/59.56 cnf(2135,plain,
% 59.61/59.56 (P1(f6(a3,a3,a2),a2,a3)),
% 59.61/59.56 inference(scs_inference,[],[2002,1980,1994,2085,1998,2000,2108,2008,1978,1982,1988,1996,2006,2020,2022,2024,2028,2030,2032,2034,2016,647,1081,1034,479,1100,352,148,169,256,258,224,257,252,259,151,152,165,225,253,160,255,164,166,187,254,135,136,185,117,118,119,120,245,263,182,236,243,161,184,242,227,241,181,186,251,156,167,168,170,226,158,173,223,176,178])).
% 59.61/59.56 cnf(2137,plain,
% 59.61/59.56 (P5(a2,a2,a2,f4(a2,a2,a2))),
% 59.61/59.56 inference(scs_inference,[],[2002,1980,1994,2085,1998,2000,2108,2008,1978,1982,1988,1996,2006,2020,2022,2024,2028,2030,2032,2034,2016,647,1081,1034,479,1100,352,148,169,256,258,224,257,252,259,151,152,165,225,253,160,255,164,166,187,254,135,136,185,117,118,119,120,245,263,182,236,243,161,184,242,227,241,181,186,251,156,167,168,170,226,158,173,223,176,178,188])).
% 59.61/59.56 cnf(2139,plain,
% 59.61/59.56 (P2(f9(a2,a2,a2),a2,a2,a2)),
% 59.61/59.56 inference(scs_inference,[],[2002,1980,1994,2085,1998,2000,2108,2008,1978,1982,1988,1996,2006,2020,2022,2024,2028,2030,2032,2034,2016,647,1081,1034,479,1100,352,148,169,256,258,224,257,252,259,151,152,165,225,253,160,255,164,166,187,254,135,136,185,117,118,119,120,245,263,182,236,243,161,184,242,227,241,181,186,251,156,167,168,170,226,158,173,223,176,178,188,191])).
% 59.61/59.56 cnf(2145,plain,
% 59.61/59.56 (P4(f26(a2,a2,a2,a2,a3,a3),a2,a2)),
% 59.61/59.56 inference(scs_inference,[],[2002,1980,1994,2085,1998,2000,2108,2008,1978,1982,1988,1996,2006,2020,2022,2024,2028,2030,2032,2034,2016,647,1081,1034,479,1100,352,148,169,256,258,224,257,252,259,151,152,165,225,253,160,255,164,166,187,254,135,136,185,117,118,119,120,245,263,182,236,243,161,184,242,227,241,181,186,251,156,167,168,170,226,158,173,223,176,178,188,191,193,197,203])).
% 59.61/59.56 cnf(2149,plain,
% 59.61/59.56 (P10(f26(a2,a2,a2,a2,a3,a3),a3,a2,a2)),
% 59.61/59.56 inference(scs_inference,[],[2002,1980,1994,2085,1998,2000,2108,2008,1978,1982,1988,1996,2006,2020,2022,2024,2028,2030,2032,2034,2016,647,1081,1034,479,1100,352,148,169,256,258,224,257,252,259,151,152,165,225,253,160,255,164,166,187,254,135,136,185,117,118,119,120,245,263,182,236,243,161,184,242,227,241,181,186,251,156,167,168,170,226,158,173,223,176,178,188,191,193,197,203,198,204])).
% 59.61/59.56 cnf(2155,plain,
% 59.61/59.56 (P1(f24(a2,a2,a3,a2),a3,a2)),
% 59.61/59.56 inference(scs_inference,[],[2002,1980,1994,2085,1998,2000,2108,2008,1978,1982,1988,1996,2006,2020,2022,2024,2028,2030,2032,2034,2016,647,1081,1034,479,1100,352,148,169,256,258,224,257,252,259,151,152,165,225,253,160,255,164,166,187,254,135,136,185,117,118,119,120,245,263,182,236,243,161,184,242,227,241,181,186,251,156,167,168,170,226,158,173,223,176,178,188,191,193,197,203,198,204,201,246,249])).
% 59.61/59.56 cnf(2157,plain,
% 59.61/59.56 (P5(a2,a2,a2,f28(a2,a2,a2,a2,a2))),
% 59.61/59.56 inference(scs_inference,[],[2002,1980,1994,2085,1998,2000,2108,2008,1978,1982,1988,1996,2006,2020,2022,2024,2028,2030,2032,2034,2016,647,1081,1034,479,1100,352,148,169,256,258,224,257,252,259,151,152,165,225,253,160,255,164,166,187,254,135,136,185,117,118,119,120,245,263,182,236,243,161,184,242,227,241,181,186,251,156,167,168,170,226,158,173,223,176,178,188,191,193,197,203,198,204,201,246,249,199])).
% 59.61/59.56 cnf(2161,plain,
% 59.61/59.56 (P1(f5(a3,a3,a2),a2,a3)),
% 59.61/59.56 inference(scs_inference,[],[2002,1980,1994,2085,1998,2000,2108,2008,1978,1982,1988,1996,2006,2020,2022,2024,2028,2030,2032,2034,2016,647,1081,1034,479,1100,352,148,169,256,258,224,257,252,259,151,152,165,225,253,160,255,164,166,187,254,135,136,185,117,118,119,120,245,263,182,236,243,161,184,242,227,241,181,186,251,156,167,168,170,226,158,173,223,176,178,188,191,193,197,203,198,204,201,246,249,199,190,177])).
% 59.61/59.56 cnf(2215,plain,
% 59.61/59.56 (P6(a2,a3,a3,a2)),
% 59.61/59.56 inference(scs_inference,[],[2002,1980,1994,2085,1998,2000,2108,2008,1978,1982,1988,1996,2006,2020,2022,2024,2028,2030,2032,2034,2016,647,1081,1034,479,1100,352,148,169,256,258,224,257,252,259,151,152,165,225,253,160,255,164,166,187,254,135,136,185,117,118,119,120,245,263,182,236,243,161,184,242,227,241,181,186,251,156,167,168,170,226,158,173,223,176,178,188,191,193,197,203,198,204,201,246,249,199,190,177,189,196,381,419,457,492,641,670,828,939,984,1042,1071,1110,1156,1183,1231,1277,1317,1344,1383,1413,1420,1445,1471,1496,171])).
% 59.61/59.56 cnf(2217,plain,
% 59.61/59.56 (P10(a2,a2,a3,a3)),
% 59.61/59.56 inference(scs_inference,[],[2002,1980,1994,2085,1998,2000,2108,2008,1978,1982,1988,1996,2006,2020,2022,2024,2028,2030,2032,2034,2016,647,1081,1034,479,1100,352,148,169,256,258,224,257,252,259,151,152,165,225,253,160,255,164,166,187,254,135,136,185,117,118,119,120,245,263,182,236,243,161,184,242,227,241,181,186,251,156,167,168,170,226,158,173,223,176,178,188,191,193,197,203,198,204,201,246,249,199,190,177,189,196,381,419,457,492,641,670,828,939,984,1042,1071,1110,1156,1183,1231,1277,1317,1344,1383,1413,1420,1445,1471,1496,171,163])).
% 59.61/59.56 cnf(2233,plain,
% 59.61/59.56 (P6(a3,a2,a2,a3)),
% 59.61/59.56 inference(scs_inference,[],[2123,2217,1110,1413,1156,1445,939,1471,169])).
% 59.61/59.56 cnf(2251,plain,
% 59.61/59.56 (P8(a2,a3,a2,a2,a2,a3,a2,a2)),
% 59.61/59.56 inference(scs_inference,[],[2041,2043,2123,2217,2157,1110,1413,1156,1445,939,1471,169,256,224,1344,1277,670,168,1042,1496,258])).
% 59.61/59.56 cnf(2259,plain,
% 59.61/59.56 (P5(a2,a3,a3,a2)),
% 59.61/59.56 inference(scs_inference,[],[2041,2043,2121,2123,2217,2157,1110,1413,1156,1445,939,1471,169,256,224,1344,1277,670,168,1042,1496,258,828,257,1231,167])).
% 59.61/59.56 cnf(2261,plain,
% 59.61/59.56 (P5(f26(a2,a2,a2,a2,a3,a3),a2,f26(a2,a2,a2,a2,a3,a3),a2)),
% 59.61/59.56 inference(scs_inference,[],[2041,2043,2121,2123,2217,2157,2145,1110,1413,1156,1445,939,1471,169,256,224,1344,1277,670,168,1042,1496,258,828,257,1231,167,156])).
% 59.61/59.56 cnf(2277,plain,
% 59.61/59.56 (P6(a2,a3,f14(a2,a2,a2,a2,a3,a3),a3)),
% 59.61/59.56 inference(scs_inference,[],[2041,2043,2121,2123,2217,2157,2094,2145,1110,1413,1156,1445,939,1471,169,256,224,1344,1277,670,168,1042,1496,258,828,257,1231,167,156,381,1071,1317,419,641,1383,1420,170])).
% 59.61/59.56 cnf(2279,plain,
% 59.61/59.56 (P6(a3,a2,a3,a2)),
% 59.61/59.56 inference(scs_inference,[],[2041,2043,2121,2123,2217,2157,2094,2145,1110,1413,1156,1445,939,1471,169,256,224,1344,1277,670,168,1042,1496,258,828,257,1231,167,156,381,1071,1317,419,641,1383,1420,170,171])).
% 59.61/59.56 cnf(2291,plain,
% 59.61/59.56 (P1(x22911,x22912,x22911)),
% 59.61/59.56 inference(scs_inference,[],[2063,2061,2041,2043,2121,2123,2217,2157,2094,2145,1110,1413,1156,1445,939,1471,169,256,224,1344,1277,670,168,1042,1496,258,828,257,1231,167,156,381,1071,1317,419,641,1383,1420,170,171,457,984,492,1183,252,151])).
% 59.61/59.56 cnf(2293,plain,
% 59.61/59.56 (P8(a3,a2,a2,a3,a2,a2,a2,a2)),
% 59.61/59.56 inference(scs_inference,[],[2063,2061,2041,2043,2121,2123,2217,2157,2094,2145,1110,1413,1156,1445,939,1471,169,256,224,1344,1277,670,168,1042,1496,258,828,257,1231,167,156,381,1071,1317,419,641,1383,1420,170,171,457,984,492,1183,252,151,259])).
% 59.61/59.56 cnf(2297,plain,
% 59.61/59.56 (P1(a16,a2,a1)),
% 59.61/59.56 inference(scs_inference,[],[2063,2061,2041,2043,2053,2121,2123,2217,2157,2094,2145,1110,1413,1156,1445,939,1471,169,256,224,1344,1277,670,168,1042,1496,258,828,257,1231,167,156,381,1071,1317,419,641,1383,1420,170,171,457,984,492,1183,252,151,259,226,152])).
% 59.61/59.56 cnf(2301,plain,
% 59.61/59.56 (P3(a17,a20,a3,a2)),
% 59.61/59.56 inference(scs_inference,[],[2063,2061,2065,2041,2043,2053,2069,2121,2123,2217,2157,2094,2145,1110,1413,1156,1445,939,1471,169,256,224,1344,1277,670,168,1042,1496,258,828,257,1231,167,156,381,1071,1317,419,641,1383,1420,170,171,457,984,492,1183,252,151,259,226,152,253,165])).
% 59.61/59.56 cnf(2303,plain,
% 59.61/59.56 (P9(x23031,x23032,x23033,x23034,x23032,x23031,x23033,x23034)),
% 59.61/59.56 inference(scs_inference,[],[2067,2063,2061,2065,2041,2043,2053,2069,2121,2123,2217,2157,2094,2145,1110,1413,1156,1445,939,1471,169,256,224,1344,1277,670,168,1042,1496,258,828,257,1231,167,156,381,1071,1317,419,641,1383,1420,170,171,457,984,492,1183,252,151,259,226,152,253,165,225])).
% 59.61/59.56 cnf(2309,plain,
% 59.61/59.56 (P9(x23091,x23092,x23091,x23092,x23093,x23094,x23093,x23094)),
% 59.61/59.56 inference(scs_inference,[],[2059,2067,2063,2061,2065,2041,2043,2053,2069,2121,2123,2217,2157,2094,2145,1110,1413,1156,1445,939,1471,169,256,224,1344,1277,670,168,1042,1496,258,828,257,1231,167,156,381,1071,1317,419,641,1383,1420,170,171,457,984,492,1183,252,151,259,226,152,253,165,225,233,160,255])).
% 59.61/59.56 cnf(2313,plain,
% 59.61/59.56 (P3(a3,a2,a2,a3)),
% 59.61/59.56 inference(scs_inference,[],[2059,2067,2063,2061,2065,2041,2043,2053,2069,2107,2121,2123,2217,2157,2094,2145,1110,1413,1156,1445,939,1471,169,256,224,1344,1277,670,168,1042,1496,258,828,257,1231,167,156,381,1071,1317,419,641,1383,1420,170,171,457,984,492,1183,252,151,259,226,152,253,165,225,233,160,255,164,166])).
% 59.61/59.56 cnf(2315,plain,
% 59.61/59.56 (P9(x23151,x23152,x23152,x23151,a3,a2,a3,a2)),
% 59.61/59.56 inference(scs_inference,[],[2059,2067,2063,2049,2061,2065,2041,2043,2053,2069,2107,2121,2123,2217,2157,2094,2145,1110,1413,1156,1445,939,1471,169,256,224,1344,1277,670,168,1042,1496,258,828,257,1231,167,156,381,1071,1317,419,641,1383,1420,170,171,457,984,492,1183,252,151,259,226,152,253,165,225,233,160,255,164,166,254])).
% 59.61/59.56 cnf(2321,plain,
% 59.61/59.56 (P5(a2,a3,a2,a3)),
% 59.61/59.56 inference(scs_inference,[],[2059,2067,2063,2103,2099,2049,2061,2065,2041,2043,2053,2069,2101,2107,2121,2123,2217,2149,2157,2094,2145,1110,1413,1156,1445,939,1471,169,256,224,1344,1277,670,168,1042,1496,258,828,257,1231,167,156,381,1071,1317,419,641,1383,1420,170,171,457,984,492,1183,252,151,259,226,152,253,165,225,233,160,255,164,166,254,163,187,174])).
% 59.61/59.56 cnf(2324,plain,
% 59.61/59.56 (P9(x23241,x23242,x23243,x23244,x23241,x23242,x23243,x23244)),
% 59.61/59.56 inference(rename_variables,[],[2059])).
% 59.61/59.56 cnf(2327,plain,
% 59.61/59.56 (P9(x23271,x23272,x23273,x23274,x23271,x23272,x23273,x23274)),
% 59.61/59.56 inference(rename_variables,[],[2059])).
% 59.61/59.56 cnf(2329,plain,
% 59.61/59.56 (P5(a3,a3,a3,a3)),
% 59.61/59.56 inference(scs_inference,[],[2059,2324,2067,2063,2103,2099,2049,2061,2065,2041,2043,2053,2069,2101,2107,2114,2119,2121,2123,2217,2149,2157,2094,2145,350,1110,1413,1156,1445,939,1471,169,256,224,1344,1277,670,168,1042,1496,258,828,257,1231,167,156,381,1071,1317,419,641,1383,1420,170,171,457,984,492,1183,252,151,259,226,152,253,165,225,233,160,255,164,166,254,163,187,174,244,260,183])).
% 59.61/59.56 cnf(2332,plain,
% 59.61/59.56 (P10(x23321,x23322,x23322,x23321)),
% 59.61/59.56 inference(rename_variables,[],[2067])).
% 59.61/59.56 cnf(2337,plain,
% 59.61/59.56 (P6(x23371,x23372,x23372,x23372)),
% 59.61/59.56 inference(scs_inference,[],[2059,2324,2327,2067,2063,2097,2103,2099,2049,2061,2065,2041,2043,2053,2069,2101,2107,2114,2119,2121,2123,2217,2149,2157,2094,2145,350,1110,1413,1156,1445,939,1471,169,256,224,1344,1277,670,168,1042,1496,258,828,257,1231,167,156,381,1071,1317,419,641,1383,1420,170,171,457,984,492,1183,252,151,259,226,152,253,165,225,233,160,255,164,166,254,163,187,174,244,260,183,179,245,236])).
% 59.61/59.56 cnf(2338,plain,
% 59.61/59.56 (P1(x23381,x23382,x23382)),
% 59.61/59.56 inference(rename_variables,[],[2063])).
% 59.61/59.56 cnf(2339,plain,
% 59.61/59.56 (P9(x23391,x23392,x23393,x23394,x23391,x23392,x23393,x23394)),
% 59.61/59.56 inference(rename_variables,[],[2059])).
% 59.61/59.56 cnf(2341,plain,
% 59.61/59.56 (P8(f26(a2,a2,a2,a2,a3,a3),a2,a2,a2,f26(a2,a2,a2,a2,a3,a3),a2,a2,a2)),
% 59.61/59.56 inference(scs_inference,[],[2059,2324,2327,2067,2063,2097,2103,2099,2049,2061,2065,2041,2043,2053,2069,2101,2107,2114,2119,2121,2123,2217,2149,2157,2094,2145,350,1110,1413,1156,1445,939,1471,169,256,224,1344,1277,670,168,1042,1496,258,828,257,1231,167,156,381,1071,1317,419,641,1383,1420,170,171,457,984,492,1183,252,151,259,226,152,253,165,225,233,160,255,164,166,254,163,187,174,244,260,183,179,245,236,223])).
% 59.61/59.56 cnf(2345,plain,
% 59.61/59.56 (P3(f13(a2,a2,a2,x23451,x23451),a2,x23451,x23451)),
% 59.61/59.56 inference(scs_inference,[],[2059,2324,2327,2067,2063,2338,2097,2103,2099,2049,2061,2065,2041,2043,2053,2069,2101,2107,2110,2114,2119,2121,2123,2217,2149,2157,2094,2145,350,1110,1413,1156,1445,939,1471,169,256,224,1344,1277,670,168,1042,1496,258,828,257,1231,167,156,381,1071,1317,419,641,1383,1420,170,171,457,984,492,1183,252,151,259,226,152,253,165,225,233,160,255,164,166,254,163,187,174,244,260,183,179,245,236,223,193,198])).
% 59.61/59.56 cnf(2346,plain,
% 59.61/59.56 (P1(x23461,x23462,x23462)),
% 59.61/59.56 inference(rename_variables,[],[2063])).
% 59.61/59.56 cnf(2365,plain,
% 59.61/59.56 (P2(a3,a2,a2,a2)),
% 59.61/59.56 inference(scs_inference,[],[2059,2324,2327,2067,2063,2338,2097,2103,2099,2049,2061,2065,2041,2043,2053,2055,2069,2101,2105,2107,2110,2114,2119,2121,2123,2217,2149,2157,2094,2145,1273,350,1110,1413,1156,1445,939,1471,169,256,224,1344,1277,670,168,1042,1496,258,828,257,1231,167,156,381,1071,1317,419,641,1383,1420,170,171,457,984,492,1183,252,151,259,226,152,253,165,225,233,160,255,164,166,254,163,187,174,244,260,183,179,245,236,223,193,198,262,197,176,188,201,189,200,190,184])).
% 59.61/59.56 cnf(2371,plain,
% 59.61/59.56 (P3(x23711,x23712,x23711,x23712)),
% 59.61/59.56 inference(scs_inference,[],[2059,2324,2327,2067,2063,2338,2097,2103,2099,2049,2061,2065,2041,2043,2053,2055,2069,2101,2105,2107,2110,2114,2119,2121,2123,2217,2149,2157,2094,2145,2139,1273,350,1110,1413,1156,1445,939,1471,169,256,224,1344,1277,670,168,1042,1496,258,828,257,1231,167,156,381,1071,1317,419,641,1383,1420,170,171,457,984,492,1183,252,151,259,226,152,253,165,225,233,160,255,164,166,254,163,187,174,244,260,183,179,245,236,223,193,198,262,197,176,188,201,189,200,190,184,199,227,241])).
% 59.61/59.56 cnf(2379,plain,
% 59.61/59.56 (P4(a2,a2,a2)),
% 59.61/59.56 inference(scs_inference,[],[2059,2324,2327,2339,2067,2063,2338,2346,2097,2103,2099,2049,2061,2065,2041,2043,2053,2055,2069,2077,2101,2105,2107,2110,2114,2119,2121,2123,2217,2149,2157,2117,2094,2135,2145,2139,1273,350,1110,1413,1156,1445,939,1471,169,256,224,1344,1277,670,168,1042,1496,258,828,257,1231,167,156,381,1071,1317,419,641,1383,1420,170,171,457,984,492,1183,252,151,259,226,152,253,165,225,233,160,255,164,166,254,163,187,174,244,260,183,179,245,236,223,193,198,262,197,176,188,201,189,200,190,184,199,227,241,181,192,228,239])).
% 59.61/59.56 cnf(2381,plain,
% 59.61/59.56 (P1(x23811,x23812,x23812)),
% 59.61/59.56 inference(rename_variables,[],[2063])).
% 59.61/59.56 cnf(2385,plain,
% 59.61/59.56 (P10(x23851,x23852,x23852,x23851)),
% 59.61/59.56 inference(rename_variables,[],[2067])).
% 59.61/59.56 cnf(2386,plain,
% 59.61/59.56 (P1(x23861,x23862,x23862)),
% 59.61/59.56 inference(rename_variables,[],[2063])).
% 59.61/59.56 cnf(2389,plain,
% 59.61/59.56 (P10(x23891,x23892,x23892,x23891)),
% 59.61/59.56 inference(rename_variables,[],[2067])).
% 59.61/59.56 cnf(2394,plain,
% 59.61/59.56 (P4(f22(a2,x23941),a2,x23941)),
% 59.61/59.56 inference(scs_inference,[],[142,2059,2324,2327,2339,2067,2332,2385,2389,2063,2338,2346,2381,2386,2097,2103,2099,2049,2061,2065,1992,2041,2043,2053,2055,2069,2077,2101,2105,2107,2110,2114,2119,2121,2123,2217,2149,2157,2117,2094,2135,2145,2139,1273,1982,350,2002,1110,1413,1156,1445,939,1471,169,256,224,1344,1277,670,168,1042,1496,258,828,257,1231,167,156,381,1071,1317,419,641,1383,1420,170,171,457,984,492,1183,252,151,259,226,152,253,165,225,233,160,255,164,166,254,163,187,174,244,260,183,179,245,236,223,193,198,262,197,176,188,201,189,200,190,184,199,227,241,181,192,228,239,208,207,206,159])).
% 59.61/59.56 cnf(2410,plain,
% 59.61/59.56 (P4(f22(a2,x24101),x24101,a2)),
% 59.61/59.56 inference(scs_inference,[],[142,2059,2324,2327,2339,2067,2332,2385,2389,2063,2338,2346,2381,2386,2097,2103,2099,2049,2061,2065,1992,2041,2043,2053,2055,2069,2077,2101,2105,2107,2110,2114,2119,2121,2123,2217,2149,2157,2117,2094,2135,2145,2139,1273,1982,350,2002,1110,1413,1156,1445,939,1471,169,256,224,1344,1277,670,168,1042,1496,258,828,257,1231,167,156,381,1071,1317,419,641,1383,1420,170,171,457,984,492,1183,252,151,259,226,152,253,165,225,233,160,255,164,166,254,163,187,174,244,260,183,179,245,236,223,193,198,262,197,176,188,201,189,200,190,184,199,227,241,181,192,228,239,208,207,206,159,941,1158,1279,1385,1422,1498,154])).
% 59.61/59.56 cnf(2414,plain,
% 59.61/59.56 (P10(a1,a17,a2,a16)),
% 59.61/59.56 inference(scs_inference,[],[142,2059,2324,2327,2339,2067,2332,2385,2389,2063,2338,2346,2381,2386,2097,2103,2099,2049,2061,2065,1992,2041,2043,2053,2055,2069,2077,2101,2105,2107,2110,2114,2119,2121,2123,2217,2149,2157,2117,2094,2135,2145,2139,1273,1982,350,2002,1110,1413,1156,1445,939,1471,169,256,224,1344,1277,670,168,1042,1496,258,828,257,1231,167,156,381,1071,1317,419,641,1383,1420,170,171,457,984,492,1183,252,151,259,226,152,253,165,225,233,160,255,164,166,254,163,187,174,244,260,183,179,245,236,223,193,198,262,197,176,188,201,189,200,190,184,199,227,241,181,192,228,239,208,207,206,159,941,1158,1279,1385,1422,1498,154,153,294])).
% 59.61/59.56 cnf(2426,plain,
% 59.61/59.56 (P10(a2,a2,a1,a1)),
% 59.61/59.56 inference(scs_inference,[],[142,2059,2324,2327,2339,2067,2332,2385,2389,2063,2338,2346,2381,2386,2097,2103,2099,2049,2061,2065,1992,2041,2043,2053,2055,2069,2077,2101,2105,2107,2110,2114,2119,2121,2123,2217,2149,2157,2117,2094,2135,2145,2139,1273,1982,350,2002,1110,1413,1156,1445,939,1471,169,256,224,1344,1277,670,168,1042,1496,258,828,257,1231,167,156,381,1071,1317,419,641,1383,1420,170,171,457,984,492,1183,252,151,259,226,152,253,165,225,233,160,255,164,166,254,163,187,174,244,260,183,179,245,236,223,193,198,262,197,176,188,201,189,200,190,184,199,227,241,181,192,228,239,208,207,206,159,941,1158,1279,1385,1422,1498,154,153,294,1938,230,205,178,246,157])).
% 59.61/59.56 cnf(2430,plain,
% 59.61/59.56 (P4(f26(a2,a2,a2,a2,a2,a2),a2,a2)),
% 59.61/59.56 inference(scs_inference,[],[142,2059,2324,2327,2339,2067,2332,2385,2389,2063,2338,2346,2381,2386,2097,2103,2099,2049,2061,2065,1992,2041,2043,2053,2055,2069,2077,2101,2105,2107,2110,2114,2119,2121,2123,2217,2149,2157,2117,2094,2137,2133,2135,2145,2139,1273,1982,350,2002,1110,1413,1156,1445,939,1471,169,256,224,1344,1277,670,168,1042,1496,258,828,257,1231,167,156,381,1071,1317,419,641,1383,1420,170,171,457,984,492,1183,252,151,259,226,152,253,165,225,233,160,255,164,166,254,163,187,174,244,260,183,179,245,236,223,193,198,262,197,176,188,201,189,200,190,184,199,227,241,181,192,228,239,208,207,206,159,941,1158,1279,1385,1422,1498,154,153,294,1938,230,205,178,246,157,161,203])).
% 59.61/59.56 cnf(2432,plain,
% 59.61/59.56 (~P10(a20,f27(a20,a19,a1,a1),a19,f27(a20,a19,a1,a1))),
% 59.61/59.56 inference(scs_inference,[],[142,2059,2324,2327,2339,2067,2332,2385,2389,2063,2338,2346,2381,2386,2097,2103,2099,2049,2061,2065,1992,2041,2043,2053,2055,2069,2077,2101,2105,2107,2110,2114,2119,2121,2123,2217,2149,2157,2117,2094,2137,2133,2135,2145,2139,1273,1982,350,471,2002,1110,1413,1156,1445,939,1471,169,256,224,1344,1277,670,168,1042,1496,258,828,257,1231,167,156,381,1071,1317,419,641,1383,1420,170,171,457,984,492,1183,252,151,259,226,152,253,165,225,233,160,255,164,166,254,163,187,174,244,260,183,179,245,236,223,193,198,262,197,176,188,201,189,200,190,184,199,227,241,181,192,228,239,208,207,206,159,941,1158,1279,1385,1422,1498,154,153,294,1938,230,205,178,246,157,161,203,240])).
% 59.61/59.56 cnf(2436,plain,
% 59.61/59.56 (P9(a2,a3,a2,a2,a2,a2,a2,a2)),
% 59.61/59.56 inference(scs_inference,[],[142,2059,2324,2327,2339,2067,2332,2385,2389,2063,2338,2346,2381,2386,2097,2103,2099,2049,2061,2065,1992,2041,2043,2053,2055,2069,2077,2101,2105,2107,2110,2114,2119,2121,2123,2217,2149,2157,2117,2094,2137,2133,2135,2145,2139,1273,1982,350,471,2002,1110,1413,1156,1445,939,1471,169,256,224,1344,1277,670,168,1042,1496,258,828,257,1231,167,156,381,1071,1317,419,641,1383,1420,170,171,457,984,492,1183,252,151,259,226,152,253,165,225,233,160,255,164,166,254,163,187,174,244,260,183,179,245,236,223,193,198,262,197,176,188,201,189,200,190,184,199,227,241,181,192,228,239,208,207,206,159,941,1158,1279,1385,1422,1498,154,153,294,1938,230,205,178,246,157,161,203,240,177,229])).
% 59.61/59.56 cnf(2438,plain,
% 59.61/59.56 (P6(a1,a1,a20,a19)),
% 59.61/59.56 inference(scs_inference,[],[142,2059,2324,2327,2339,2067,2332,2385,2389,2063,2338,2346,2381,2386,2097,2103,2099,2049,2061,2065,1992,2041,2043,2053,2055,2069,2077,2101,2105,2107,2110,2114,2119,2121,2123,2217,2149,2157,2117,2094,2137,2133,2135,2145,2139,1273,1982,350,471,2002,1110,1413,1156,1445,939,1471,169,256,224,1344,1277,670,168,1042,1496,258,828,257,1231,167,156,381,1071,1317,419,641,1383,1420,170,171,457,984,492,1183,252,151,259,226,152,253,165,225,233,160,255,164,166,254,163,187,174,244,260,183,179,245,236,223,193,198,262,197,176,188,201,189,200,190,184,199,227,241,181,192,228,239,208,207,206,159,941,1158,1279,1385,1422,1498,154,153,294,1938,230,205,178,246,157,161,203,240,177,229,234])).
% 59.61/59.56 cnf(2440,plain,
% 59.61/59.56 (P3(a3,a2,a2,a2)),
% 59.61/59.56 inference(scs_inference,[],[142,2059,2324,2327,2339,2067,2332,2385,2389,2063,2338,2346,2381,2386,2097,2103,2099,2049,2061,2065,1992,2041,2043,2053,2055,2069,2077,2101,2105,2107,2110,2114,2119,2121,2123,2217,2149,2157,2117,2094,2137,2133,2135,2145,2139,2012,1273,1982,350,471,2002,2020,1110,1413,1156,1445,939,1471,169,256,224,1344,1277,670,168,1042,1496,258,828,257,1231,167,156,381,1071,1317,419,641,1383,1420,170,171,457,984,492,1183,252,151,259,226,152,253,165,225,233,160,255,164,166,254,163,187,174,244,260,183,179,245,236,223,193,198,262,197,176,188,201,189,200,190,184,199,227,241,181,192,228,239,208,207,206,159,941,1158,1279,1385,1422,1498,154,153,294,1938,230,205,178,246,157,161,203,240,177,229,234,195])).
% 59.61/59.56 cnf(2442,plain,
% 59.61/59.56 (P4(a2,a2,f28(a2,a2,a2,a2,a2))),
% 59.61/59.56 inference(scs_inference,[],[142,2059,2324,2327,2339,2067,2332,2385,2389,2063,2338,2346,2381,2386,2097,2103,2099,2049,2061,2065,1992,2041,2043,2053,2055,2069,2077,2101,2105,2107,2110,2114,2119,2121,2123,2217,2149,2157,2117,2094,2137,2133,2135,2145,2139,2012,1273,1982,350,471,2002,2020,1110,1413,1156,1445,939,1471,169,256,224,1344,1277,670,168,1042,1496,258,828,257,1231,167,156,381,1071,1317,419,641,1383,1420,170,171,457,984,492,1183,252,151,259,226,152,253,165,225,233,160,255,164,166,254,163,187,174,244,260,183,179,245,236,223,193,198,262,197,176,188,201,189,200,190,184,199,227,241,181,192,228,239,208,207,206,159,941,1158,1279,1385,1422,1498,154,153,294,1938,230,205,178,246,157,161,203,240,177,229,234,195,162])).
% 59.61/59.56 cnf(2444,plain,
% 59.61/59.56 (P5(a3,a2,a2,a2)),
% 59.61/59.56 inference(scs_inference,[],[142,2059,2324,2327,2339,2067,2332,2385,2389,2063,2338,2346,2381,2386,2039,2097,2103,2099,2049,2061,2065,1992,2041,2043,2053,2055,2069,2077,2101,2105,2107,2110,2114,2119,2121,2123,2217,2149,2157,2117,2094,2137,2133,2135,2145,2139,2012,1273,1982,350,471,2002,2020,1110,1413,1156,1445,939,1471,169,256,224,1344,1277,670,168,1042,1496,258,828,257,1231,167,156,381,1071,1317,419,641,1383,1420,170,171,457,984,492,1183,252,151,259,226,152,253,165,225,233,160,255,164,166,254,163,187,174,244,260,183,179,245,236,223,193,198,262,197,176,188,201,189,200,190,184,199,227,241,181,192,228,239,208,207,206,159,941,1158,1279,1385,1422,1498,154,153,294,1938,230,205,178,246,157,161,203,240,177,229,234,195,162,251])).
% 59.61/59.56 cnf(2451,plain,
% 59.61/59.56 (P3(x24511,x24512,x24511,x24512)),
% 59.61/59.56 inference(rename_variables,[],[2371])).
% 59.61/59.56 cnf(2454,plain,
% 59.61/59.56 (P3(x24541,x24542,x24541,x24542)),
% 59.61/59.56 inference(rename_variables,[],[2371])).
% 59.61/59.56 cnf(2457,plain,
% 59.61/59.56 (P3(x24571,x24572,x24571,x24572)),
% 59.61/59.56 inference(rename_variables,[],[2371])).
% 59.61/59.56 cnf(2460,plain,
% 59.61/59.56 (P3(x24601,x24602,x24601,x24602)),
% 59.61/59.56 inference(rename_variables,[],[2371])).
% 59.61/59.56 cnf(2463,plain,
% 59.61/59.56 (P3(x24631,x24632,x24631,x24632)),
% 59.61/59.56 inference(rename_variables,[],[2371])).
% 59.61/59.56 cnf(2466,plain,
% 59.61/59.56 (P3(x24661,x24662,x24661,x24662)),
% 59.61/59.56 inference(rename_variables,[],[2371])).
% 59.61/59.56 cnf(2469,plain,
% 59.61/59.56 (P3(x24691,x24692,x24691,x24692)),
% 59.61/59.56 inference(rename_variables,[],[2371])).
% 59.61/59.56 cnf(2472,plain,
% 59.61/59.56 (P3(x24721,x24722,x24721,x24722)),
% 59.61/59.56 inference(rename_variables,[],[2371])).
% 59.61/59.56 cnf(2475,plain,
% 59.61/59.56 (P3(x24751,x24752,x24751,x24752)),
% 59.61/59.56 inference(rename_variables,[],[2371])).
% 59.61/59.56 cnf(2478,plain,
% 59.61/59.56 (P3(x24781,x24782,x24781,x24782)),
% 59.61/59.56 inference(rename_variables,[],[2371])).
% 59.61/59.56 cnf(2481,plain,
% 59.61/59.56 (P3(x24811,x24812,x24811,x24812)),
% 59.61/59.56 inference(rename_variables,[],[2371])).
% 59.61/59.56 cnf(2484,plain,
% 59.61/59.56 (P3(x24841,x24842,x24841,x24842)),
% 59.61/59.56 inference(rename_variables,[],[2371])).
% 59.61/59.56 cnf(2487,plain,
% 59.61/59.56 (P3(x24871,x24872,x24871,x24872)),
% 59.61/59.56 inference(rename_variables,[],[2371])).
% 59.61/59.56 cnf(2490,plain,
% 59.61/59.56 (P3(x24901,x24902,x24901,x24902)),
% 59.61/59.56 inference(rename_variables,[],[2371])).
% 59.61/59.56 cnf(2493,plain,
% 59.61/59.56 (P3(x24931,x24932,x24931,x24932)),
% 59.61/59.56 inference(rename_variables,[],[2371])).
% 59.61/59.56 cnf(2496,plain,
% 59.61/59.56 (P3(x24961,x24962,x24961,x24962)),
% 59.61/59.56 inference(rename_variables,[],[2371])).
% 59.61/59.56 cnf(2499,plain,
% 59.61/59.56 (P3(x24991,x24992,x24991,x24992)),
% 59.61/59.56 inference(rename_variables,[],[2371])).
% 59.61/59.56 cnf(2515,plain,
% 59.61/59.56 (P6(x25151,x25152,x25151,x25151)),
% 59.61/59.56 inference(scs_inference,[],[2337,2371,2451,2454,2457,2460,2463,2466,2469,2472,2475,2478,2481,2484,2487,2490,2493,2496,2293,2414,2426,1044,1112,1185,1233,1281,1319,1321,1346,1387,1447,1449,1473,1500,1187,1348,421,494,1445,1110,1413,256,670,939,1156,169])).
% 59.61/59.56 cnf(2531,plain,
% 59.61/59.56 (P9(a3,a2,a3,a3,a2,a2,a2,a3)),
% 59.61/59.56 inference(scs_inference,[],[2337,2371,2451,2454,2457,2460,2463,2466,2469,2472,2475,2478,2481,2484,2487,2490,2493,2496,2215,2279,2293,2414,2426,2444,1044,1112,1185,1233,1281,1319,1321,1346,1387,1447,1449,1473,1500,1187,1348,421,494,1445,1110,1413,256,670,939,1156,169,1071,381,1471,1231,167,170,641,224])).
% 59.61/59.56 cnf(2539,plain,
% 59.61/59.56 (P8(a2,a3,a2,a3,a2,a2,a2,a2)),
% 59.61/59.56 inference(scs_inference,[],[2337,2371,2451,2454,2457,2460,2463,2466,2469,2472,2475,2478,2481,2484,2487,2490,2493,2496,2215,2279,2293,2414,2426,2444,1044,1112,1185,1233,1281,1319,1321,1346,1387,1447,1449,1473,1500,1187,1348,421,494,1445,1110,1413,256,670,939,1156,169,1071,381,1471,1231,167,170,641,224,1277,1420,492,258])).
% 59.61/59.56 cnf(2581,plain,
% 59.61/59.56 (P9(a1,a17,x25811,x25812,a2,a16,x25811,x25812)),
% 59.61/59.56 inference(scs_inference,[],[2337,2371,2451,2454,2457,2460,2463,2466,2469,2472,2475,2478,2481,2484,2487,2490,2493,2496,2125,2215,2321,2251,2279,2293,2414,2426,2438,2444,2155,2131,2394,2410,2261,2442,1044,1112,1185,1233,1281,1319,1321,1346,1387,1447,1449,1473,1500,1187,1348,421,494,1445,1110,1413,256,670,939,1156,169,1071,381,1471,1231,167,170,641,224,1277,1420,492,258,419,457,257,984,1042,154,1344,828,259,1317,156,1496,168,252,1383,1183,151,153,171,226,225])).
% 59.61/59.56 cnf(2583,plain,
% 59.61/59.56 (P1(x25831,x25831,x25832)),
% 59.61/59.56 inference(scs_inference,[],[2337,2371,2451,2454,2457,2460,2463,2466,2469,2472,2475,2478,2481,2484,2487,2490,2493,2496,2291,2125,2215,2321,2251,2279,2293,2414,2426,2438,2444,2155,2131,2394,2410,2261,2442,1044,1112,1185,1233,1281,1319,1321,1346,1387,1447,1449,1473,1500,1187,1348,421,494,1445,1110,1413,256,670,939,1156,169,1071,381,1471,1231,167,170,641,224,1277,1420,492,258,419,457,257,984,1042,154,1344,828,259,1317,156,1496,168,252,1383,1183,151,153,171,226,225,152])).
% 59.61/59.56 cnf(2585,plain,
% 59.61/59.56 (P9(x25851,x25852,x25853,x25854,x25851,x25852,x25854,x25853)),
% 59.61/59.56 inference(scs_inference,[],[2303,2337,2371,2451,2454,2457,2460,2463,2466,2469,2472,2475,2478,2481,2484,2487,2490,2493,2496,2291,2125,2215,2321,2251,2279,2293,2414,2426,2438,2444,2155,2131,2394,2410,2261,2442,1044,1112,1185,1233,1281,1319,1321,1346,1387,1447,1449,1473,1500,1187,1348,421,494,1445,1110,1413,256,670,939,1156,169,1071,381,1471,1231,167,170,641,224,1277,1420,492,258,419,457,257,984,1042,154,1344,828,259,1317,156,1496,168,252,1383,1183,151,153,171,226,225,152,253])).
% 59.61/59.56 cnf(2587,plain,
% 59.61/59.56 (P10(a19,a17,a3,a16)),
% 59.61/59.56 inference(scs_inference,[],[2303,2337,2371,2451,2454,2457,2460,2463,2466,2469,2472,2475,2478,2481,2484,2487,2490,2493,2496,2499,2291,2125,2215,2321,2251,2279,2293,2414,2426,2438,2444,2155,2131,2394,2410,2261,2442,1044,1112,1185,1233,1281,1319,1321,1346,1387,1447,1449,1473,1500,1187,1348,421,494,1445,1110,1413,256,670,939,1156,169,1071,381,1471,1231,167,170,641,224,1277,1420,492,258,419,457,257,984,1042,154,1344,828,259,1317,156,1496,168,252,1383,1183,151,153,171,226,225,152,253,636])).
% 59.61/59.56 cnf(2588,plain,
% 59.61/59.56 (P3(x25881,x25882,x25881,x25882)),
% 59.61/59.56 inference(rename_variables,[],[2371])).
% 59.61/59.56 cnf(2592,plain,
% 59.61/59.56 (P10(a20,a17,a3,a2)),
% 59.61/59.56 inference(scs_inference,[],[2303,2337,2371,2451,2454,2457,2460,2463,2466,2469,2472,2475,2478,2481,2484,2487,2490,2493,2496,2499,2588,2291,2313,2125,2215,2321,2251,2279,2293,2414,2426,2438,2444,2155,2131,2394,2410,2261,2442,1044,1112,1185,1233,1281,1319,1321,1346,1387,1447,1449,1473,1500,1187,1348,421,494,1445,1110,1413,256,670,939,1156,169,1071,381,1471,1231,167,170,641,224,1277,1420,492,258,419,457,257,984,1042,154,1344,828,259,1317,156,1496,168,252,1383,1183,151,153,171,226,225,152,253,636,165,699])).
% 59.61/59.56 cnf(2593,plain,
% 59.61/59.56 (P3(x25931,x25932,x25931,x25932)),
% 59.61/59.56 inference(rename_variables,[],[2371])).
% 59.61/59.56 cnf(2597,plain,
% 59.61/59.56 (P9(x25971,x25972,x25972,x25971,x25973,x25974,x25973,x25974)),
% 59.61/59.56 inference(scs_inference,[],[2303,2337,2371,2451,2454,2457,2460,2463,2466,2469,2472,2475,2478,2481,2484,2487,2490,2493,2496,2499,2588,2291,2313,2125,2215,2321,2251,2279,2293,2414,2426,2436,2438,2444,2155,2131,2394,2410,2261,2442,1044,1112,1185,1233,1281,1319,1321,1346,1387,1447,1449,1473,1500,1187,1348,421,494,1445,1110,1413,256,670,939,1156,169,1071,381,1471,1231,167,170,641,224,1277,1420,492,258,419,457,257,984,1042,154,1344,828,259,1317,156,1496,168,252,1383,1183,151,153,171,226,225,152,253,636,165,699,233,255])).
% 59.61/59.56 cnf(2603,plain,
% 59.61/59.56 (P3(x26031,x26032,x26032,x26031)),
% 59.61/59.56 inference(scs_inference,[],[2303,2337,2371,2451,2454,2457,2460,2463,2466,2469,2472,2475,2478,2481,2484,2487,2490,2493,2496,2499,2588,2593,2291,2313,2125,2215,2321,2251,2279,2293,2414,2426,2436,2438,2444,2155,2131,2394,2410,2261,2442,1044,1112,1185,1233,1281,1319,1321,1346,1387,1447,1449,1473,1500,1187,1348,421,494,1445,1110,1413,256,670,939,1156,169,1071,381,1471,1231,167,170,641,224,1277,1420,492,258,419,457,257,984,1042,154,1344,828,259,1317,156,1496,168,252,1383,1183,151,153,171,226,225,152,253,636,165,699,233,255,164,254,166])).
% 59.61/59.56 cnf(2616,plain,
% 59.61/59.56 (~P10(f27(a20,a19,a1,a1),a20,a19,f27(a20,a19,a1,a1))),
% 59.61/59.56 inference(scs_inference,[],[2303,2337,2371,2451,2454,2457,2460,2463,2466,2469,2472,2475,2478,2481,2484,2487,2490,2493,2496,2499,2588,2593,2291,2313,2125,2215,2321,2315,2251,2279,2293,2365,2414,2426,2436,2438,2440,2444,2155,2131,2394,2410,2261,2432,2442,2067,2097,1044,1112,1185,1233,1281,1319,1321,1346,1387,1447,1449,1473,1500,1187,1348,421,494,1445,1110,1413,256,670,939,1156,169,1071,381,1471,1231,167,170,641,224,1277,1420,492,258,419,457,257,984,1042,154,1344,828,259,1317,156,1496,168,252,1383,1183,151,153,171,226,225,152,253,636,165,699,233,255,164,254,166,163,187,194,248,250,179])).
% 59.61/59.56 cnf(2617,plain,
% 59.61/59.56 (P10(x26171,x26172,x26172,x26171)),
% 59.61/59.56 inference(rename_variables,[],[2067])).
% 59.61/59.56 cnf(2619,plain,
% 59.61/59.56 (P6(a16,a16,a1,a2)),
% 59.61/59.56 inference(scs_inference,[],[142,2303,2309,2337,2371,2451,2454,2457,2460,2463,2466,2469,2472,2475,2478,2481,2484,2487,2490,2493,2496,2499,2588,2593,2291,2313,2125,2215,2321,2315,2251,2279,2293,2365,2414,2426,2436,2438,2440,2444,2155,2131,2394,2410,2261,2432,2442,2067,2097,1044,1112,1185,1233,1281,1319,1321,1346,1387,1447,1449,1473,1500,1187,1348,421,494,1445,1110,1413,256,670,939,1156,169,1071,381,1471,1231,167,170,641,224,1277,1420,492,258,419,457,257,984,1042,154,1344,828,259,1317,156,1496,168,252,1383,1183,151,153,171,226,225,152,253,636,165,699,233,255,164,254,166,163,187,194,248,250,179,236])).
% 59.61/59.56 cnf(2620,plain,
% 59.61/59.56 (P9(x26201,x26202,x26201,x26202,x26203,x26204,x26203,x26204)),
% 59.61/59.56 inference(rename_variables,[],[2309])).
% 59.61/59.56 cnf(2623,plain,
% 59.61/59.56 (P9(x26231,x26232,x26233,x26234,x26231,x26232,x26233,x26234)),
% 59.61/59.56 inference(rename_variables,[],[2059])).
% 59.61/59.56 cnf(2633,plain,
% 59.61/59.56 (P1(x26331,x26332,x26331)),
% 59.61/59.56 inference(rename_variables,[],[2291])).
% 59.61/59.56 cnf(2638,plain,
% 59.61/59.56 (P1(x26381,x26382,x26381)),
% 59.61/59.56 inference(rename_variables,[],[2291])).
% 59.61/59.56 cnf(2641,plain,
% 59.61/59.56 (P9(x26411,x26412,x26413,x26414,x26412,x26411,x26413,x26414)),
% 59.61/59.56 inference(rename_variables,[],[2303])).
% 59.61/59.56 cnf(2643,plain,
% 59.61/59.56 (P5(a2,a2,a2,a3)),
% 59.61/59.56 inference(scs_inference,[],[142,2303,2309,2337,2371,2451,2454,2457,2460,2463,2466,2469,2472,2475,2478,2481,2484,2487,2490,2493,2496,2499,2588,2593,2291,2633,2313,2125,2215,2321,2315,2047,2251,2279,2293,2365,2414,2426,2436,2438,2440,2444,2155,2131,2394,2410,2261,2432,2442,2059,2623,2067,2110,266,2097,1044,1112,1185,1233,1281,1319,1321,1346,1387,1447,1449,1473,1500,1187,1348,421,494,1445,1110,1413,256,670,939,1156,169,1071,381,1471,1231,167,170,641,224,1277,1420,492,258,419,457,257,984,1042,154,1344,828,259,1317,156,1496,168,252,1383,1183,151,153,171,226,225,152,253,636,165,699,233,255,164,254,166,163,187,194,248,250,179,236,244,260,173,191,197,178,198,249,243])).
% 59.61/59.56 cnf(2648,plain,
% 59.61/59.56 (P9(x26481,x26482,x26483,x26484,x26482,x26481,x26483,x26484)),
% 59.61/59.56 inference(rename_variables,[],[2303])).
% 59.61/59.56 cnf(2660,plain,
% 59.61/59.56 (P2(a2,a3,a3,a3)),
% 59.61/59.56 inference(scs_inference,[],[142,2303,2641,2309,2337,2371,2451,2454,2457,2460,2463,2466,2469,2472,2475,2478,2481,2484,2487,2490,2493,2496,2499,2588,2593,2291,2633,2313,2125,2215,2321,2379,2315,2047,2251,2279,2293,2365,2414,2426,2436,2438,2440,2444,2155,2131,2394,2410,2261,2432,2442,2059,2623,2067,2110,266,2097,1044,1112,1185,1233,1281,1319,1321,1346,1387,1447,1449,1473,1500,1187,1348,421,494,1445,1110,1413,256,670,939,1156,169,1071,381,1471,1231,167,170,641,224,1277,1420,492,258,419,457,257,984,1042,154,1344,828,259,1317,156,1496,168,252,1383,1183,151,153,171,226,225,152,253,636,165,699,233,255,164,254,166,163,187,194,248,250,179,236,244,260,173,191,197,178,198,249,243,223,262,176,188,201,190,189,184])).
% 59.61/59.56 cnf(2662,plain,
% 59.61/59.56 (P5(a2,a3,a2,f28(a3,a2,a3,a3,a2))),
% 59.61/59.56 inference(scs_inference,[],[142,2303,2641,2309,2337,2371,2451,2454,2457,2460,2463,2466,2469,2472,2475,2478,2481,2484,2487,2490,2493,2496,2499,2588,2593,2291,2633,2313,2125,2215,2321,2379,2315,2047,2251,2279,2293,2365,2414,2426,2436,2438,2440,2444,2155,2131,2394,2410,2261,2432,2442,2059,2623,2067,2110,266,2097,1044,1112,1185,1233,1281,1319,1321,1346,1387,1447,1449,1473,1500,1187,1348,421,494,1445,1110,1413,256,670,939,1156,169,1071,381,1471,1231,167,170,641,224,1277,1420,492,258,419,457,257,984,1042,154,1344,828,259,1317,156,1496,168,252,1383,1183,151,153,171,226,225,152,253,636,165,699,233,255,164,254,166,163,187,194,248,250,179,236,244,260,173,191,197,178,198,249,243,223,262,176,188,201,190,189,184,200])).
% 59.61/59.56 cnf(2665,plain,
% 59.61/59.56 (P9(x26651,x26652,x26653,x26654,x26652,x26651,x26653,x26654)),
% 59.61/59.56 inference(rename_variables,[],[2303])).
% 59.61/59.56 cnf(2674,plain,
% 59.61/59.56 (P3(a2,a3,a2,a2)),
% 59.61/59.56 inference(scs_inference,[],[142,2303,2641,2648,2665,2309,2337,2371,2451,2454,2457,2460,2463,2466,2469,2472,2475,2478,2481,2484,2487,2490,2493,2496,2499,2588,2593,2291,2633,2313,2125,2215,2321,2379,2315,2047,2251,2279,2293,2329,2365,2414,2426,2436,2438,2440,2444,2155,2131,2394,2410,2261,2432,2442,2059,2623,2067,2110,266,2097,1044,1112,1185,1233,1281,1319,1321,1346,1387,1447,1449,1473,1500,1187,1348,421,494,1445,1110,1413,256,670,939,1156,169,1071,381,1471,1231,167,170,641,224,1277,1420,492,258,419,457,257,984,1042,154,1344,828,259,1317,156,1496,168,252,1383,1183,151,153,171,226,225,152,253,636,165,699,233,255,164,254,166,163,187,194,248,250,179,236,244,260,173,191,197,178,198,249,243,223,262,176,188,201,190,189,184,200,240,177,199,227,241])).
% 59.61/59.56 cnf(2675,plain,
% 59.61/59.56 (P9(x26751,x26752,x26753,x26754,x26752,x26751,x26753,x26754)),
% 59.61/59.56 inference(rename_variables,[],[2303])).
% 59.61/59.56 cnf(2677,plain,
% 59.61/59.56 (P3(a2,a2,a3,a3)),
% 59.61/59.56 inference(scs_inference,[],[142,2303,2641,2648,2665,2309,2337,2371,2451,2454,2457,2460,2463,2466,2469,2472,2475,2478,2481,2484,2487,2490,2493,2496,2499,2588,2593,2291,2633,2313,2125,2215,2321,2379,2315,2047,2251,2279,2293,2329,2365,2414,2426,2436,2438,2440,2444,2155,2131,2394,2410,2261,2432,2442,2059,2623,2067,2110,266,2097,1044,1112,1185,1233,1281,1319,1321,1346,1387,1447,1449,1473,1500,1187,1348,421,494,1445,1110,1413,256,670,939,1156,169,1071,381,1471,1231,167,170,641,224,1277,1420,492,258,419,457,257,984,1042,154,1344,828,259,1317,156,1496,168,252,1383,1183,151,153,171,226,225,152,253,636,165,699,233,255,164,254,166,163,187,194,248,250,179,236,244,260,173,191,197,178,198,249,243,223,262,176,188,201,190,189,184,200,240,177,199,227,241,181])).
% 59.61/59.56 cnf(2681,plain,
% 59.61/59.56 (P1(x26811,x26812,x26811)),
% 59.61/59.56 inference(rename_variables,[],[2291])).
% 59.61/59.56 cnf(2682,plain,
% 59.61/59.56 (P10(x26821,x26822,x26822,x26821)),
% 59.61/59.56 inference(rename_variables,[],[2067])).
% 59.61/59.56 cnf(2685,plain,
% 59.61/59.56 (P1(x26851,x26852,x26851)),
% 59.61/59.56 inference(rename_variables,[],[2291])).
% 59.61/59.56 cnf(2687,plain,
% 59.61/59.56 (P5(x26871,x26871,x26871,x26871)),
% 59.61/59.56 inference(scs_inference,[],[142,2303,2641,2648,2665,2675,2309,2337,2371,2451,2454,2457,2460,2463,2466,2469,2472,2475,2478,2481,2484,2487,2490,2493,2496,2499,2588,2593,2291,2633,2638,2681,2313,2125,2215,2321,2379,2315,2047,2251,2279,2293,2297,2329,2365,2414,2426,2436,2438,2440,2444,2155,2131,2394,2410,2261,2432,2442,2059,2623,2067,2617,2110,266,2097,1044,1112,1185,1233,1281,1319,1321,1346,1387,1447,1449,1473,1500,1187,1348,421,494,1445,1110,1413,256,670,939,1156,169,1071,381,1471,1231,167,170,641,224,1277,1420,492,258,419,457,257,984,1042,154,1344,828,259,1317,156,1496,168,252,1383,1183,151,153,171,226,225,152,253,636,165,699,233,255,164,254,166,163,187,194,248,250,179,236,244,260,173,191,197,178,198,249,243,223,262,176,188,201,190,189,184,200,240,177,199,227,241,181,207,206,251])).
% 59.61/59.56 cnf(2690,plain,
% 59.61/59.56 (P6(x26901,x26902,x26902,x26902)),
% 59.61/59.56 inference(rename_variables,[],[2337])).
% 59.61/59.56 cnf(2692,plain,
% 59.61/59.56 (P4(f22(a16,x26921),a16,x26921)),
% 59.61/59.56 inference(scs_inference,[],[142,2303,2641,2648,2665,2675,2309,2337,2371,2451,2454,2457,2460,2463,2466,2469,2472,2475,2478,2481,2484,2487,2490,2493,2496,2499,2588,2593,2291,2633,2638,2681,2685,2313,2125,2215,2321,2379,2315,2047,2251,2279,2293,2297,2329,2365,2414,2426,2436,2438,2440,2444,2155,2131,2394,2410,2261,2432,2442,2059,2623,2067,2617,1992,2110,266,2097,1044,1112,1185,1233,1281,1319,1321,1346,1387,1447,1449,1473,1500,1187,1348,421,494,1445,1110,1413,256,670,939,1156,169,1071,381,1471,1231,167,170,641,224,1277,1420,492,258,419,457,257,984,1042,154,1344,828,259,1317,156,1496,168,252,1383,1183,151,153,171,226,225,152,253,636,165,699,233,255,164,254,166,163,187,194,248,250,179,236,244,260,173,191,197,178,198,249,243,223,262,176,188,201,190,189,184,200,240,177,199,227,241,181,207,206,251,159])).
% 59.61/59.56 cnf(2695,plain,
% 59.61/59.56 (P1(x26951,x26952,x26951)),
% 59.61/59.56 inference(rename_variables,[],[2291])).
% 59.61/59.56 cnf(2700,plain,
% 59.61/59.56 (P9(x27001,x27002,x27001,x27002,x27003,x27004,x27003,x27004)),
% 59.61/59.56 inference(rename_variables,[],[2309])).
% 59.61/59.56 cnf(2708,plain,
% 59.61/59.56 (P3(a2,a2,a2,a3)),
% 59.61/59.56 inference(scs_inference,[],[142,2303,2641,2648,2665,2675,2309,2620,2337,2690,2371,2451,2454,2457,2460,2463,2466,2469,2472,2475,2478,2481,2484,2487,2490,2493,2496,2499,2588,2593,2291,2633,2638,2681,2685,2259,2313,2125,2215,2321,2379,2315,2047,2251,2279,2293,2297,2329,2365,2414,2426,2436,2438,2440,2444,2155,2131,2394,2410,2261,2432,2442,2105,2059,2623,2067,2617,2682,1992,2024,2110,266,2097,1044,1112,1185,1233,1281,1319,1321,1346,1387,1447,1449,1473,1500,1187,1348,421,494,1445,1110,1413,256,670,939,1156,169,1071,381,1471,1231,167,170,641,224,1277,1420,492,258,419,457,257,984,1042,154,1344,828,259,1317,156,1496,168,252,1383,1183,151,153,171,226,225,152,253,636,165,699,233,255,164,254,166,163,187,194,248,250,179,236,244,260,173,191,197,178,198,249,243,223,262,176,188,201,190,189,184,200,240,177,199,227,241,181,207,206,251,159,220,247,245,192,195])).
% 59.61/59.56 cnf(2710,plain,
% 59.61/59.56 (P4(a3,a3,a3)),
% 59.61/59.56 inference(scs_inference,[],[142,2303,2641,2648,2665,2675,2309,2620,2700,2337,2690,2371,2451,2454,2457,2460,2463,2466,2469,2472,2475,2478,2481,2484,2487,2490,2493,2496,2499,2588,2593,2291,2633,2638,2681,2685,2695,2259,2313,2125,2215,2321,2379,2315,2047,2251,2279,2293,2297,2329,2365,2414,2426,2436,2438,2440,2444,2155,2131,2394,2410,2261,2432,2442,2105,2059,2623,2067,2617,2682,1992,2024,2110,266,2097,1044,1112,1185,1233,1281,1319,1321,1346,1387,1447,1449,1473,1500,1187,1348,421,494,1445,1110,1413,256,670,939,1156,169,1071,381,1471,1231,167,170,641,224,1277,1420,492,258,419,457,257,984,1042,154,1344,828,259,1317,156,1496,168,252,1383,1183,151,153,171,226,225,152,253,636,165,699,233,255,164,254,166,163,187,194,248,250,179,236,244,260,173,191,197,178,198,249,243,223,262,176,188,201,190,189,184,200,240,177,199,227,241,181,207,206,251,159,220,247,245,192,195,239])).
% 59.61/59.56 cnf(2717,plain,
% 59.61/59.56 (P3(x27171,x27172,x27172,x27171)),
% 59.61/59.56 inference(rename_variables,[],[2603])).
% 59.61/59.56 cnf(2720,plain,
% 59.61/59.56 (P3(x27201,x27202,x27202,x27201)),
% 59.61/59.56 inference(rename_variables,[],[2603])).
% 59.61/59.56 cnf(2723,plain,
% 59.61/59.56 (P3(x27231,x27232,x27232,x27231)),
% 59.61/59.56 inference(rename_variables,[],[2603])).
% 59.61/59.56 cnf(2726,plain,
% 59.61/59.56 (P3(x27261,x27262,x27262,x27261)),
% 59.61/59.56 inference(rename_variables,[],[2603])).
% 59.61/59.56 cnf(2729,plain,
% 59.61/59.56 (P3(x27291,x27292,x27292,x27291)),
% 59.61/59.56 inference(rename_variables,[],[2603])).
% 59.61/59.56 cnf(2732,plain,
% 59.61/59.56 (P3(x27321,x27322,x27322,x27321)),
% 59.61/59.56 inference(rename_variables,[],[2603])).
% 59.61/59.56 cnf(2737,plain,
% 59.61/59.56 (P3(x27371,x27372,x27372,x27371)),
% 59.61/59.56 inference(rename_variables,[],[2603])).
% 59.61/59.56 cnf(2746,plain,
% 59.61/59.56 (P3(x27461,x27462,x27462,x27461)),
% 59.61/59.56 inference(rename_variables,[],[2603])).
% 59.61/59.56 cnf(2749,plain,
% 59.61/59.56 (P3(x27491,x27492,x27492,x27491)),
% 59.61/59.56 inference(rename_variables,[],[2603])).
% 59.61/59.56 cnf(2830,plain,
% 59.61/59.56 (P3(x28301,x28302,x28302,x28301)),
% 59.61/59.56 inference(rename_variables,[],[2603])).
% 59.61/59.56 cnf(2835,plain,
% 59.61/59.56 (P3(x28351,x28352,x28352,x28351)),
% 59.61/59.56 inference(rename_variables,[],[2603])).
% 59.61/59.56 cnf(2854,plain,
% 59.61/59.56 (P5(x28541,x28541,x28541,x28541)),
% 59.61/59.56 inference(rename_variables,[],[2687])).
% 59.61/59.56 cnf(2862,plain,
% 59.61/59.56 (P9(x28621,x28622,x28623,x28624,x28621,x28622,x28623,x28624)),
% 59.61/59.56 inference(rename_variables,[],[2059])).
% 59.61/59.56 cnf(2875,plain,
% 59.61/59.56 (P3(x28751,x28752,x28752,x28751)),
% 59.61/59.56 inference(rename_variables,[],[2603])).
% 59.61/59.56 cnf(2889,plain,
% 59.61/59.56 (P3(x28891,x28892,x28892,x28891)),
% 59.61/59.56 inference(rename_variables,[],[2603])).
% 59.61/59.56 cnf(2896,plain,
% 59.61/59.56 (P3(x28961,x28962,x28962,x28961)),
% 59.61/59.56 inference(rename_variables,[],[2603])).
% 59.61/59.56 cnf(2904,plain,
% 59.61/59.56 (P5(x29041,x29041,x29041,x29041)),
% 59.61/59.56 inference(rename_variables,[],[2687])).
% 59.61/59.56 cnf(2905,plain,
% 59.61/59.56 (P3(x29051,x29052,x29052,x29051)),
% 59.61/59.56 inference(rename_variables,[],[2603])).
% 59.61/59.56 cnf(2909,plain,
% 59.61/59.56 (P3(x29091,x29092,x29092,x29091)),
% 59.61/59.56 inference(rename_variables,[],[2603])).
% 59.61/59.56 cnf(2912,plain,
% 59.61/59.56 (P3(x29121,x29122,x29122,x29121)),
% 59.61/59.56 inference(rename_variables,[],[2603])).
% 59.61/59.56 cnf(2918,plain,
% 59.61/59.56 (P3(x29181,x29182,x29182,x29181)),
% 59.61/59.56 inference(rename_variables,[],[2603])).
% 59.61/59.56 cnf(2921,plain,
% 59.61/59.56 (P3(x29211,x29212,x29212,x29211)),
% 59.61/59.56 inference(rename_variables,[],[2603])).
% 59.61/59.56 cnf(2924,plain,
% 59.61/59.56 (P3(x29241,x29242,x29242,x29241)),
% 59.61/59.56 inference(rename_variables,[],[2603])).
% 59.61/59.56 cnf(2929,plain,
% 59.61/59.56 (P3(x29291,x29292,x29292,x29291)),
% 59.61/59.56 inference(rename_variables,[],[2603])).
% 59.61/59.56 cnf(2933,plain,
% 59.61/59.56 (P3(x29331,x29332,x29332,x29331)),
% 59.61/59.56 inference(rename_variables,[],[2603])).
% 59.61/59.56 cnf(2938,plain,
% 59.61/59.56 (~P1(a1,a1,a20)),
% 59.61/59.56 inference(scs_inference,[],[142,2687,2854,2904,2515,2585,2597,2603,2717,2720,2723,2726,2729,2732,2737,2746,2749,2830,2835,2875,2889,2896,2905,2909,2912,2918,2921,2924,2929,2933,2583,2539,2233,2581,2301,2531,2587,2592,2619,2643,2660,2674,2677,2708,2710,2430,2161,2662,1986,2345,2692,2616,2341,2277,366,1379,2309,2105,2125,2379,2059,2862,2067,320,2440,1422,1233,1473,1044,1112,941,1110,421,670,1413,939,1158,494,1231,1445,1071,1471,224,169,170,258,641,256,1420,1042,1156,492,381,1277,1344,259,984,419,457,167,156,257,153,252,154,828,1317,151,1383,168,1183,1496,226,171,165,253,225,636,152,699,233,255,164,166,163,254,187,204,194,247,236,244,246,179,203,248,191,178,173,245,223,193,197,262,198,260,176,188,229,177,184,190,199,201,240,200,189,180,155])).
% 59.61/59.56 cnf(2998,plain,
% 59.61/59.56 ($false),
% 59.61/59.56 inference(scs_inference,[],[2938,2583]),
% 59.61/59.56 ['proof']).
% 59.61/59.56 % SZS output end Proof
% 59.61/59.56 % Total time :58.870000s
%------------------------------------------------------------------------------