%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : GEO638+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 : n025.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:06:02 EDT 2024
% Result : Theorem 61.14s 61.27s
% Output : CNFRefutation 61.31s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.13 % Problem : GEO638+1 : TPTP v8.2.0. Released v7.5.0.
% 0.07/0.13 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% 0.13/0.34 % Computer : n025.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % WCLimit : 300
% 0.13/0.34 % DateTime : Fri Jun 21 08:03:54 EDT 2024
% 0.13/0.34 % CPUTime :
% 0.20/0.58 start to proof:theBenchmark
% 61.14/61.25 %-------------------------------------------
% 61.14/61.25 % File :CSE---1.7
% 61.14/61.25 % Problem :theBenchmark
% 61.14/61.26 % Transform :cnf
% 61.14/61.26 % Format :tptp:raw
% 61.14/61.26 % Command :java -jar mcs_scs.jar %d %s
% 61.14/61.26
% 61.14/61.26 % Result :Theorem 60.600000s
% 61.14/61.26 % Output :CNFRefutation 60.600000s
% 61.14/61.26 %-------------------------------------------
% 61.14/61.26 %------------------------------------------------------------------------------
% 61.14/61.27 % File : GEO638+1 : TPTP v8.2.0. Released v7.5.0.
% 61.14/61.27 % Domain : Geometry
% 61.14/61.27 % Problem : JGEX problem 104
% 61.14/61.27 % Version : [CGZ00] axioms.
% 61.14/61.27 % English :
% 61.14/61.27
% 61.14/61.27 % Refs : [CGZ00] Chou et al. (2000), A Deductive Database Approach to A
% 61.14/61.27 % : [YCG08] Ye et al. (2008), An Introduction to Java Geometry Exp
% 61.14/61.27 % : [Qua20] Quaresma (2020), Email to Geoff Sutcliffe
% 61.14/61.27 % Source : [Qua20]
% 61.14/61.27 % Names : 104.p [Qua20]
% 61.14/61.27
% 61.14/61.27 % Status : Theorem
% 61.14/61.27 % Rating : 0.33 v8.1.0, 0.36 v7.5.0
% 61.14/61.27 % Syntax : Number of formulae : 95 ( 0 unt; 0 def)
% 61.14/61.27 % Number of atoms : 293 ( 1 equ)
% 61.14/61.27 % Maximal formula atoms : 10 ( 3 avg)
% 61.14/61.27 % Number of connectives : 205 ( 7 ~; 0 |; 103 &)
% 61.14/61.27 % ( 0 <=>; 95 =>; 0 <=; 0 <~>)
% 61.14/61.27 % Maximal formula depth : 21 ( 9 avg)
% 61.14/61.27 % Maximal term depth : 1 ( 1 avg)
% 61.14/61.27 % Number of predicates : 12 ( 11 usr; 0 prp; 2-8 aty)
% 61.14/61.27 % Number of functors : 0 ( 0 usr; 0 con; --- aty)
% 61.14/61.27 % Number of variables : 533 ( 513 !; 20 ?)
% 61.14/61.27 % SPC : FOF_THM_RFO_SEQ
% 61.14/61.27
% 61.14/61.27 % Comments : Taken from JGEX [YCG08], converted by Pedro Quaresma.
% 61.14/61.27 %------------------------------------------------------------------------------
% 61.14/61.27 include('Axioms/GEO012+0.ax').
% 61.14/61.27 %------------------------------------------------------------------------------
% 61.14/61.27 fof(exemplo6GDDFULL81109104,conjecture,
% 61.14/61.27 ! [A,B,E,G,D,C,F,H,NWPNT1,NWPNT2,NWPNT3] :
% 61.14/61.27 ( ( midp(E,A,B)
% 61.14/61.27 & circle(E,A,NWPNT1,NWPNT2)
% 61.14/61.27 & circle(E,A,G,NWPNT3)
% 61.14/61.27 & perp(E,G,G,D)
% 61.14/61.27 & para(A,D,C,B)
% 61.14/61.27 & coll(C,G,D)
% 61.14/61.27 & midp(F,C,D)
% 61.14/61.27 & perp(H,F,A,B)
% 61.14/61.27 & coll(H,A,B) )
% 61.14/61.27 => perp(C,H,D,H) ) ).
% 61.14/61.27
% 61.14/61.27 %------------------------------------------------------------------------------
% 61.14/61.27 %-------------------------------------------
% 61.14/61.27 % Proof found
% 61.14/61.27 % SZS status Theorem for theBenchmark
% 61.14/61.27 % SZS output start Proof
% 61.23/61.27 %ClaNum:264(EqnAxiom:141)
% 61.23/61.27 %VarNum:1613(SingletonVarNum:590)
% 61.23/61.27 %MaxLitNum:5
% 61.23/61.27 %MaxfuncDepth:1
% 61.23/61.27 %SharedTerms:21
% 61.23/61.27 %goalClause: 142 143 144 145 146 147 148 149 150 151
% 61.23/61.27 %singleGoalClaCount:10
% 61.23/61.27 [142]P1(a1,a2,a18)
% 61.23/61.27 [143]P1(a19,a3,a16)
% 61.23/61.27 [144]P3(a17,a3,a16)
% 61.23/61.27 [145]P3(a20,a1,a18)
% 61.23/61.27 [146]P9(a3,a18,a1,a16)
% 61.23/61.27 [147]P10(a17,a2,a2,a18)
% 61.23/61.27 [148]P10(a19,a20,a3,a16)
% 61.23/61.27 [149]P2(a17,a3,a2,a21)
% 61.23/61.27 [150]P2(a17,a3,a22,a23)
% 61.23/61.27 [151]~P10(a1,a19,a18,a19)
% 61.23/61.27 [152]~P1(x1522,x1521,x1523)+P1(x1521,x1522,x1523)
% 61.23/61.27 [153]~P1(x1531,x1533,x1532)+P1(x1531,x1532,x1533)
% 61.23/61.27 [154]~P3(x1541,x1542,x1543)+P1(x1541,x1542,x1543)
% 61.23/61.27 [155]~P3(x1551,x1553,x1552)+P3(x1551,x1552,x1553)
% 61.23/61.27 [157]~P3(x1571,x1572,x1573)+P4(x1571,x1572,x1571,x1573)
% 61.23/61.27 [161]~P9(x1611,x1612,x1611,x1613)+P1(x1611,x1612,x1613)
% 61.23/61.27 [227]~P4(x2271,x2272,x2271,x2273)+P8(x2271,x2272,x2272,x2273,x2272,x2273,x2271,x2273)
% 61.23/61.27 [164]~P9(x1643,x1644,x1641,x1642)+P9(x1641,x1642,x1643,x1644)
% 61.23/61.27 [165]~P9(x1651,x1652,x1654,x1653)+P9(x1651,x1652,x1653,x1654)
% 61.23/61.27 [166]~P10(x1663,x1664,x1661,x1662)+P10(x1661,x1662,x1663,x1664)
% 61.23/61.27 [167]~P10(x1671,x1672,x1674,x1673)+P10(x1671,x1672,x1673,x1674)
% 61.23/61.27 [168]~P4(x1683,x1684,x1681,x1682)+P4(x1681,x1682,x1683,x1684)
% 61.23/61.27 [169]~P4(x1691,x1692,x1694,x1693)+P4(x1691,x1692,x1693,x1694)
% 61.23/61.27 [170]~P5(x1702,x1701,x1703,x1704)+P5(x1701,x1702,x1703,x1704)
% 61.23/61.27 [171]~P5(x1711,x1713,x1712,x1714)+P5(x1711,x1712,x1713,x1714)
% 61.23/61.27 [172]~P5(x1721,x1722,x1724,x1723)+P5(x1721,x1722,x1723,x1724)
% 61.23/61.27 [225]~P5(x2252,x2253,x2251,x2254)+P8(x2251,x2252,x2251,x2253,x2254,x2252,x2254,x2253)
% 61.23/61.27 [188]~P2(x1884,x1881,x1882,x1883)+P10(f8(x1881,x1882,x1883,x1884),x1881,x1881,x1884)
% 61.23/61.27 [203]P4(x2031,x2032,x2033,x2034)+~P6(x2031,x2032,x2035,x2033,x2034,x2036)
% 61.23/61.27 [215]~P11(x2154,x2155,x2156,x2151,x2152,x2153)+P11(x2151,x2152,x2153,x2154,x2155,x2156)
% 61.23/61.27 [216]~P11(x2162,x2161,x2163,x2165,x2164,x2166)+P11(x2161,x2162,x2163,x2164,x2165,x2166)
% 61.23/61.27 [217]~P11(x2171,x2173,x2172,x2174,x2176,x2175)+P11(x2171,x2172,x2173,x2174,x2175,x2176)
% 61.23/61.27 [218]~P6(x2184,x2185,x2186,x2181,x2182,x2183)+P6(x2181,x2182,x2183,x2184,x2185,x2186)
% 61.23/61.27 [219]~P6(x2192,x2191,x2193,x2195,x2194,x2196)+P6(x2191,x2192,x2193,x2194,x2195,x2196)
% 61.23/61.27 [220]~P6(x2201,x2203,x2202,x2204,x2206,x2205)+P6(x2201,x2202,x2203,x2204,x2205,x2206)
% 61.23/61.27 [226]~P9(x2261,x2262,x2265,x2266)+P8(x2261,x2262,x2263,x2264,x2265,x2266,x2263,x2264)
% 61.23/61.27 [232]~P11(x2321,x2322,x2323,x2324,x2325,x2326)+P8(x2321,x2322,x2322,x2323,x2324,x2325,x2325,x2326)
% 61.23/61.27 [233]~P11(x2331,x2332,x2333,x2334,x2335,x2336)+P7(x2331,x2332,x2331,x2333,x2334,x2335,x2334,x2336)
% 61.23/61.27 [234]~P8(x2341,x2342,x2345,x2346,x2343,x2344,x2345,x2346)+P9(x2341,x2342,x2343,x2344)
% 61.23/61.27 [253]~P8(x2535,x2536,x2537,x2538,x2531,x2532,x2533,x2534)+P8(x2531,x2532,x2533,x2534,x2535,x2536,x2537,x2538)
% 61.23/61.27 [254]~P8(x2543,x2544,x2541,x2542,x2547,x2548,x2545,x2546)+P8(x2541,x2542,x2543,x2544,x2545,x2546,x2547,x2548)
% 61.23/61.27 [255]~P8(x2552,x2551,x2553,x2554,x2555,x2556,x2557,x2558)+P8(x2551,x2552,x2553,x2554,x2555,x2556,x2557,x2558)
% 61.23/61.27 [256]~P8(x2561,x2562,x2565,x2566,x2563,x2564,x2567,x2568)+P8(x2561,x2562,x2563,x2564,x2565,x2566,x2567,x2568)
% 61.23/61.27 [257]~P7(x2575,x2576,x2577,x2578,x2571,x2572,x2573,x2574)+P7(x2571,x2572,x2573,x2574,x2575,x2576,x2577,x2578)
% 61.23/61.27 [258]~P7(x2583,x2584,x2581,x2582,x2587,x2588,x2585,x2586)+P7(x2581,x2582,x2583,x2584,x2585,x2586,x2587,x2588)
% 61.23/61.27 [259]~P7(x2592,x2591,x2593,x2594,x2595,x2596,x2597,x2598)+P7(x2591,x2592,x2593,x2594,x2595,x2596,x2597,x2598)
% 61.23/61.27 [260]~P7(x2601,x2602,x2605,x2606,x2603,x2604,x2607,x2608)+P7(x2601,x2602,x2603,x2604,x2605,x2606,x2607,x2608)
% 61.23/61.27 [162]~P1(x1621,x1622,x1623)+~P4(x1621,x1622,x1621,x1623)+P3(x1621,x1622,x1623)
% 61.23/61.27 [236]P4(x2361,x2362,x2361,x2363)+~P8(x2361,x2362,x2362,x2363,x2362,x2363,x2361,x2363)+P1(x2361,x2362,x2363)
% 61.23/61.27 [177]~P10(x1771,x1772,x1772,x1773)+~P4(x1772,x1771,x1772,x1773)+P1(x1771,x1772,f4(x1771,x1773,x1772))
% 61.23/61.27 [189]~P10(x1892,x1891,x1891,x1893)+~P4(x1891,x1892,x1891,x1893)+P4(x1891,x1892,x1891,f4(x1892,x1893,x1891))
% 61.23/61.27 [156]~P1(x1563,x1564,x1561)+P1(x1561,x1562,x1563)+~P1(x1563,x1564,x1562)
% 61.23/61.27 [173]~P2(x1734,x1731,x1732,x1733)+P10(x1731,x1732,x1732,x1733)+~P1(x1734,x1731,x1733)
% 61.23/61.27 [174]~P10(x1741,x1744,x1742,x1743)+P4(x1741,x1742,x1741,x1743)+~P3(x1744,x1742,x1743)
% 61.23/61.27 [175]~P10(x1751,x1753,x1753,x1754)+P4(x1751,x1752,x1753,x1752)+~P3(x1752,x1751,x1754)
% 61.23/61.27 [182]~P4(x1821,x1824,x1822,x1824)+~P4(x1821,x1823,x1822,x1823)+P10(x1821,x1822,x1823,x1824)
% 61.23/61.27 [185]~P4(x1851,x1852,x1851,x1854)+~P4(x1851,x1852,x1851,x1853)+P2(x1851,x1852,x1853,x1854)
% 61.23/61.27 [231]~P9(x2311,x2314,x2313,x2312)+~P5(x2311,x2314,x2313,x2312)+P8(x2311,x2312,x2313,x2312,x2313,x2312,x2313,x2314)
% 61.23/61.27 [235]~P8(x2351,x2353,x2351,x2354,x2352,x2353,x2352,x2354)+P1(x2351,x2352,x2353)+P5(x2353,x2354,x2351,x2352)
% 61.23/61.27 [237]~P1(x2373,x2374,x2372)+~P8(x2373,x2371,x2373,x2372,x2374,x2371,x2374,x2372)+P5(x2371,x2372,x2373,x2374)
% 61.23/61.27 [239]P10(x2391,x2392,x2393,x2394)+~P8(x2391,x2392,x2393,x2394,x2393,x2394,x2391,x2392)+P9(x2391,x2392,x2393,x2394)
% 61.23/61.27 [178]~P10(x1781,x1784,x1782,x1783)+~P10(x1782,x1784,x1781,x1783)+P1(f5(x1781,x1782,x1783),x1783,x1782)
% 61.23/61.28 [179]~P10(x1791,x1794,x1792,x1793)+~P10(x1792,x1794,x1791,x1793)+P1(f6(x1791,x1792,x1793),x1793,x1791)
% 61.23/61.28 [190]~P10(x1901,x1904,x1902,x1903)+~P10(x1902,x1904,x1901,x1903)+P10(x1901,f5(x1901,x1902,x1903),x1903,x1902)
% 61.23/61.28 [191]~P10(x1911,x1914,x1912,x1913)+~P10(x1912,x1914,x1911,x1913)+P10(x1911,f6(x1912,x1911,x1913),x1913,x1912)
% 61.23/61.28 [192]~P10(x1921,x1923,x1923,x1922)+~P5(x1921,x1922,x1923,x1924)+P2(f9(x1921,x1922,x1923),x1921,x1922,x1923)
% 61.23/61.28 [194]~P10(x1943,x1944,x1942,x1941)+~P4(x1943,x1942,x1943,x1941)+P1(x1941,x1942,f26(x1942,x1941,x1943,x1944))
% 61.23/61.28 [195]~P10(x1953,x1954,x1951,x1952)+~P4(x1953,x1951,x1953,x1952)+P1(f26(x1951,x1952,x1953,x1954),x1953,x1954)
% 61.23/61.28 [246]~P4(x2463,x2462,x2463,x2461)+~P8(x2462,x2463,x2463,x2464,x2463,x2464,x2463,x2461)+P1(x2461,x2462,f24(x2462,x2461,x2463,x2464))
% 61.23/61.28 [247]~P10(x2473,x2474,x2472,x2471)+~P8(x2472,x2473,x2473,x2474,x2473,x2474,x2473,x2471)+P1(x2471,x2472,f27(x2472,x2471,x2473,x2474))
% 61.23/61.28 [248]~P10(x2483,x2482,x2482,x2481)+~P8(x2484,x2483,x2482,x2483,x2482,x2483,x2481,x2483)+P1(f15(x2481,x2482,x2483,x2484),x2483,x2484)
% 61.23/61.28 [249]~P10(x2493,x2492,x2492,x2491)+~P8(x2494,x2493,x2492,x2493,x2492,x2493,x2491,x2493)+P1(f15(x2491,x2492,x2493,x2494),x2491,x2492)
% 61.23/61.28 [250]~P4(x2503,x2501,x2503,x2502)+~P8(x2501,x2503,x2503,x2504,x2503,x2504,x2503,x2502)+P1(f24(x2501,x2502,x2503,x2504),x2503,x2504)
% 61.23/61.28 [251]~P10(x2513,x2514,x2511,x2512)+~P8(x2511,x2513,x2513,x2514,x2513,x2514,x2513,x2512)+P1(f27(x2511,x2512,x2513,x2514),x2513,x2514)
% 61.23/61.28 [158]~P3(x1585,x1581,x1583)+P9(x1581,x1582,x1583,x1584)+~P3(x1585,x1582,x1584)
% 61.23/61.28 [159]~P3(x1591,x1595,x1593)+P9(x1591,x1592,x1593,x1594)+~P3(x1592,x1595,x1594)
% 61.23/61.28 [186]~P5(x1865,x1861,x1862,x1863)+P5(x1861,x1862,x1863,x1864)+~P5(x1865,x1861,x1862,x1864)
% 61.23/61.28 [228]~P3(x2285,x2282,x2283)+~P2(x2284,x2281,x2282,x2283)+P8(x2281,x2282,x2281,x2283,x2284,x2282,x2284,x2285)
% 61.23/61.28 [230]~P2(x2305,x2301,x2303,x2304)+P8(x2301,x2302,x2301,x2303,x2304,x2301,x2304,x2303)+~P10(x2305,x2301,x2301,x2302)
% 61.23/61.28 [243]~P8(x2432,x2433,x2432,x2434,x2435,x2432,x2435,x2434)+P10(x2431,x2432,x2432,x2433)+~P2(x2431,x2432,x2434,x2435)
% 61.23/61.28 [198]~P1(x1982,x1984,x1985)+~P10(x1981,x1983,x1983,x1982)+P1(f13(x1981,x1982,x1983,x1984,x1985),x1984,x1985)
% 61.23/61.28 [199]~P1(x1992,x1994,x1995)+~P10(x1991,x1993,x1993,x1992)+P10(f13(x1991,x1992,x1993,x1994,x1995),x1991,x1994,x1995)
% 61.23/61.28 [200]~P10(x2003,x2004,x2004,x2001)+~P4(x2001,x2002,x2001,x2005)+P4(x2001,x2002,x2001,f30(x2003,x2004,x2002,x2005,x2001))
% 61.23/61.28 [201]~P10(x2013,x2011,x2011,x2015)+~P4(x2015,x2012,x2015,x2014)+P4(x2011,x2012,x2011,f30(x2013,x2011,x2012,x2014,x2015))
% 61.23/61.28 [202]~P10(x2021,x2022,x2022,x2025)+~P4(x2025,x2023,x2025,x2024)+P9(f30(x2021,x2022,x2023,x2024,x2025),x2023,x2021,x2022)
% 61.23/61.28 [245]~P8(x2451,x2453,x2452,x2453,x2451,x2454,x2452,x2455)+P1(x2451,x2452,x2453)+P5(x2454,x2452,x2453,f29(x2451,x2452,x2453,x2454))
% 61.23/61.28 [261]~P8(x2611,x2613,x2612,x2613,x2611,x2614,x2612,x2615)+P1(x2611,x2612,x2613)+P8(x2611,x2613,x2612,x2613,x2611,f29(x2611,x2612,x2613,x2614),x2612,f29(x2611,x2612,x2613,x2614))
% 61.23/61.28 [180]~P9(x1801,x1802,x1805,x1806)+P9(x1801,x1802,x1803,x1804)+~P9(x1805,x1806,x1803,x1804)
% 61.23/61.28 [181]~P10(x1811,x1812,x1815,x1816)+P9(x1811,x1812,x1813,x1814)+~P10(x1815,x1816,x1813,x1814)
% 61.23/61.28 [183]~P10(x1835,x1836,x1833,x1834)+P10(x1831,x1832,x1833,x1834)+~P9(x1831,x1832,x1835,x1836)
% 61.23/61.28 [184]~P4(x1841,x1842,x1845,x1846)+P4(x1841,x1842,x1843,x1844)+~P4(x1845,x1846,x1843,x1844)
% 61.23/61.28 [221]~P4(x2211,x2212,x2214,x2215)+~P11(x2211,x2212,x2213,x2214,x2215,x2216)+P6(x2211,x2212,x2213,x2214,x2215,x2216)
% 61.23/61.28 [224]~P3(x2244,x2245,x2246)+~P3(x2241,x2242,x2243)+P7(x2241,x2242,x2242,x2243,x2244,x2245,x2245,x2246)
% 61.23/61.28 [204]~P3(x2046,x2043,x2044)+~P3(x2045,x2041,x2042)+P3(f28(x2041,x2042,x2043,x2044,x2045,x2046),x2041,x2044)
% 61.23/61.28 [205]~P3(x2056,x2053,x2054)+~P3(x2055,x2051,x2052)+P9(f28(x2051,x2052,x2053,x2054,x2055,x2056),x2056,x2051,x2053)
% 61.23/61.28 [206]~P3(x2066,x2063,x2064)+~P3(x2065,x2061,x2062)+P9(f28(x2061,x2062,x2063,x2064,x2065,x2066),x2065,x2062,x2064)
% 61.23/61.28 [241]~P8(x2411,x2412,x2413,x2414,x2415,x2416,x2417,x2418)+P9(x2411,x2412,x2413,x2414)+~P9(x2415,x2416,x2417,x2418)
% 61.23/61.28 [242]~P8(x2421,x2422,x2423,x2424,x2425,x2426,x2427,x2428)+P10(x2421,x2422,x2423,x2424)+~P10(x2425,x2426,x2427,x2428)
% 61.23/61.28 [244]~P7(x2441,x2442,x2443,x2444,x2445,x2446,x2447,x2448)+P4(x2441,x2442,x2443,x2444)+~P4(x2445,x2446,x2447,x2448)
% 61.23/61.28 [222]~P11(x2221,x2222,x2223,x2227,x2228,x2229)+P11(x2221,x2222,x2223,x2224,x2225,x2226)+~P11(x2227,x2228,x2229,x2224,x2225,x2226)
% 61.23/61.28 [223]~P6(x2231,x2232,x2233,x2237,x2238,x2239)+P6(x2231,x2232,x2233,x2234,x2235,x2236)+~P6(x2237,x2238,x2239,x2234,x2235,x2236)
% 61.23/61.28 [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)
% 61.23/61.28 [264]~P7(x2641,x2642,x2643,x2644,x2649,x26410,x26411,x26412)+P7(x2641,x2642,x2643,x2644,x2645,x2646,x2647,x2648)+~P7(x2649,x26410,x26411,x26412,x2645,x2646,x2647,x2648)
% 61.23/61.28 [196]~P4(x1962,x1961,x1964,x1961)+~P5(x1962,x1964,x1961,x1963)+P10(x1961,x1962,x1962,x1963)+~P4(x1962,x1963,x1964,x1963)
% 61.23/61.28 [163]~P1(x1631,x1632,x1633)+~P9(x1634,x1631,x1635,x1633)+P3(x1631,x1632,x1633)+~P3(x1634,x1632,x1635)
% 61.23/61.28 [176]~P9(x1764,x1763,x1765,x1762)+~P9(x1764,x1762,x1765,x1763)+P3(x1761,x1762,x1763)+~P3(x1761,x1764,x1765)
% 61.23/61.28 [197]~P4(x1975,x1971,x1975,x1973)+~P4(x1975,x1971,x1975,x1972)+P5(x1971,x1972,x1973,x1974)+~P4(x1975,x1971,x1975,x1974)
% 61.23/61.28 [229]~P1(x2291,x2294,x2295)+~P1(x2291,x2292,x2293)+~P9(x2292,x2294,x2293,x2295)+P7(x2291,x2292,x2292,x2293,x2291,x2294,x2294,x2295)
% 61.23/61.28 [240]~P1(x2401,x2402,x2403)+~P8(x2405,x2402,x2405,x2403,x2404,x2402,x2404,x2401)+P3(x2401,x2402,x2403)+~P2(x2404,x2405,x2402,x2403)
% 61.23/61.28 [187]~P10(x1873,x1871,x1873,x1875)+~P10(x1871,x1872,x1871,x1873)+~P3(x1874,x1872,x1875)+P3(f7(x1871,x1872,x1873),x1871,x1873)
% 61.23/61.28 [193]~P5(x1931,x1932,x1933,x1935)+~P9(x1931,x1932,x1933,x1935)+~P3(x1934,x1931,x1932)+P2(f10(x1931,x1932,x1933),x1931,x1932,x1933)
% 61.23/61.28 [262]~P8(x2621,x2623,x2622,x2623,x2624,x2626,x2625,x2626)+~P8(x2621,x2622,x2622,x2623,x2624,x2625,x2625,x2626)+P1(x2621,x2622,x2623)+P11(x2621,x2622,x2623,x2624,x2625,x2626)
% 61.23/61.28 [252]~P5(x2521,x2522,x2525,x2524)+~P5(x2521,x2522,x2525,x2523)+~P8(x2525,x2521,x2525,x2522,x2526,x2523,x2526,x2524)+P4(x2521,x2522,x2523,x2524)+~P5(x2521,x2522,x2525,x2526)
% 61.23/61.28 [207]~P1(x2072,x2073,x2074)+~P1(x2071,x2074,x2076)+~P1(x2071,x2073,x2075)+~P9(x2073,x2074,x2075,x2076)+P1(x2071,x2072,f14(x2073,x2074,x2075,x2076,x2071,x2072))
% 61.23/61.28 [208]~P1(x2086,x2081,x2082)+~P1(x2085,x2082,x2084)+~P1(x2085,x2081,x2083)+~P9(x2081,x2082,x2083,x2084)+P1(f14(x2081,x2082,x2083,x2084,x2085,x2086),x2083,x2084)
% 61.23/61.28 [209]~P1(x2093,x2094,x2095)+~P3(x2096,x2091,x2092)+~P9(x2091,x2093,x2095,x2096)+~P9(x2091,x2093,x2092,x2094)+P1(f31(x2091,x2092,x2093,x2094,x2095,x2096),x2096,x2095)
% 61.23/61.28 [210]~P1(x2103,x2104,x2105)+~P3(x2106,x2101,x2102)+~P9(x2101,x2103,x2105,x2106)+~P9(x2101,x2103,x2102,x2104)+P1(f31(x2101,x2102,x2103,x2104,x2105,x2106),x2101,x2104)
% 61.23/61.28 [211]~P4(x2112,x2113,x2112,x2114)+~P4(x2111,x2113,x2111,x2116)+~P2(x2111,x2113,x2114,x2115)+E(x2111,x2112)+P1(f11(x2113,x2114,x2115,x2116,x2111,x2112),x2113,x2115)
% 61.23/61.28 [212]~P4(x2122,x2123,x2122,x2124)+~P4(x2121,x2123,x2121,x2126)+~P2(x2121,x2123,x2124,x2125)+E(x2121,x2122)+P1(f12(x2123,x2124,x2125,x2126,x2121,x2122),x2124,x2126)
% 61.23/61.28 [213]~P4(x2132,x2133,x2132,x2134)+~P4(x2131,x2133,x2131,x2136)+~P2(x2131,x2133,x2134,x2135)+E(x2131,x2132)+P4(f11(x2133,x2134,x2135,x2136,x2131,x2132),x2132,x2132,x2133)
% 61.23/61.28 [214]~P4(x2142,x2143,x2142,x2144)+~P4(x2141,x2143,x2141,x2146)+~P2(x2141,x2143,x2144,x2145)+E(x2141,x2142)+P4(f12(x2143,x2144,x2145,x2146,x2141,x2142),x2142,x2142,x2143)
% 61.23/61.28 [160]~P1(x1603,x1601,x1604)+~P1(x1605,x1601,x1604)+~P3(x1606,x1605,x1603)+~P3(x1607,x1601,x1604)+P3(f25(x1601,x1602),x1601,x1602)
% 61.23/61.28 %EqnAxiom
% 61.23/61.28 [1]E(x11,x11)
% 61.23/61.28 [2]E(x22,x21)+~E(x21,x22)
% 61.23/61.28 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 61.23/61.28 [4]~E(x41,x42)+E(f25(x41,x43),f25(x42,x43))
% 61.23/61.28 [5]~E(x51,x52)+E(f25(x53,x51),f25(x53,x52))
% 61.23/61.28 [6]~E(x61,x62)+E(f4(x61,x63,x64),f4(x62,x63,x64))
% 61.23/61.28 [7]~E(x71,x72)+E(f4(x73,x71,x74),f4(x73,x72,x74))
% 61.23/61.28 [8]~E(x81,x82)+E(f4(x83,x84,x81),f4(x83,x84,x82))
% 61.23/61.28 [9]~E(x91,x92)+E(f5(x91,x93,x94),f5(x92,x93,x94))
% 61.23/61.28 [10]~E(x101,x102)+E(f5(x103,x101,x104),f5(x103,x102,x104))
% 61.23/61.28 [11]~E(x111,x112)+E(f5(x113,x114,x111),f5(x113,x114,x112))
% 61.23/61.28 [12]~E(x121,x122)+E(f6(x121,x123,x124),f6(x122,x123,x124))
% 61.23/61.28 [13]~E(x131,x132)+E(f6(x133,x131,x134),f6(x133,x132,x134))
% 61.23/61.28 [14]~E(x141,x142)+E(f6(x143,x144,x141),f6(x143,x144,x142))
% 61.23/61.28 [15]~E(x151,x152)+E(f7(x151,x153,x154),f7(x152,x153,x154))
% 61.23/61.28 [16]~E(x161,x162)+E(f7(x163,x161,x164),f7(x163,x162,x164))
% 61.23/61.28 [17]~E(x171,x172)+E(f7(x173,x174,x171),f7(x173,x174,x172))
% 61.23/61.28 [18]~E(x181,x182)+E(f8(x181,x183,x184,x185),f8(x182,x183,x184,x185))
% 61.23/61.28 [19]~E(x191,x192)+E(f8(x193,x191,x194,x195),f8(x193,x192,x194,x195))
% 61.23/61.28 [20]~E(x201,x202)+E(f8(x203,x204,x201,x205),f8(x203,x204,x202,x205))
% 61.23/61.28 [21]~E(x211,x212)+E(f8(x213,x214,x215,x211),f8(x213,x214,x215,x212))
% 61.23/61.28 [22]~E(x221,x222)+E(f29(x221,x223,x224,x225),f29(x222,x223,x224,x225))
% 61.23/61.28 [23]~E(x231,x232)+E(f29(x233,x231,x234,x235),f29(x233,x232,x234,x235))
% 61.23/61.28 [24]~E(x241,x242)+E(f29(x243,x244,x241,x245),f29(x243,x244,x242,x245))
% 61.23/61.28 [25]~E(x251,x252)+E(f29(x253,x254,x255,x251),f29(x253,x254,x255,x252))
% 61.23/61.28 [26]~E(x261,x262)+E(f24(x261,x263,x264,x265),f24(x262,x263,x264,x265))
% 61.23/61.28 [27]~E(x271,x272)+E(f24(x273,x271,x274,x275),f24(x273,x272,x274,x275))
% 61.23/61.28 [28]~E(x281,x282)+E(f24(x283,x284,x281,x285),f24(x283,x284,x282,x285))
% 61.23/61.28 [29]~E(x291,x292)+E(f24(x293,x294,x295,x291),f24(x293,x294,x295,x292))
% 61.23/61.28 [30]~E(x301,x302)+E(f27(x301,x303,x304,x305),f27(x302,x303,x304,x305))
% 61.23/61.28 [31]~E(x311,x312)+E(f27(x313,x311,x314,x315),f27(x313,x312,x314,x315))
% 61.23/61.28 [32]~E(x321,x322)+E(f27(x323,x324,x321,x325),f27(x323,x324,x322,x325))
% 61.23/61.28 [33]~E(x331,x332)+E(f27(x333,x334,x335,x331),f27(x333,x334,x335,x332))
% 61.23/61.28 [34]~E(x341,x342)+E(f9(x341,x343,x344),f9(x342,x343,x344))
% 61.23/61.28 [35]~E(x351,x352)+E(f9(x353,x351,x354),f9(x353,x352,x354))
% 61.23/61.28 [36]~E(x361,x362)+E(f9(x363,x364,x361),f9(x363,x364,x362))
% 61.23/61.28 [37]~E(x371,x372)+E(f10(x371,x373,x374),f10(x372,x373,x374))
% 61.23/61.28 [38]~E(x381,x382)+E(f10(x383,x381,x384),f10(x383,x382,x384))
% 61.23/61.28 [39]~E(x391,x392)+E(f10(x393,x394,x391),f10(x393,x394,x392))
% 61.23/61.28 [40]~E(x401,x402)+E(f26(x401,x403,x404,x405),f26(x402,x403,x404,x405))
% 61.23/61.28 [41]~E(x411,x412)+E(f26(x413,x411,x414,x415),f26(x413,x412,x414,x415))
% 61.23/61.28 [42]~E(x421,x422)+E(f26(x423,x424,x421,x425),f26(x423,x424,x422,x425))
% 61.23/61.28 [43]~E(x431,x432)+E(f26(x433,x434,x435,x431),f26(x433,x434,x435,x432))
% 61.23/61.28 [44]~E(x441,x442)+E(f15(x441,x443,x444,x445),f15(x442,x443,x444,x445))
% 61.23/61.28 [45]~E(x451,x452)+E(f15(x453,x451,x454,x455),f15(x453,x452,x454,x455))
% 61.23/61.28 [46]~E(x461,x462)+E(f15(x463,x464,x461,x465),f15(x463,x464,x462,x465))
% 61.23/61.28 [47]~E(x471,x472)+E(f15(x473,x474,x475,x471),f15(x473,x474,x475,x472))
% 61.23/61.28 [48]~E(x481,x482)+E(f13(x481,x483,x484,x485,x486),f13(x482,x483,x484,x485,x486))
% 61.23/61.28 [49]~E(x491,x492)+E(f13(x493,x491,x494,x495,x496),f13(x493,x492,x494,x495,x496))
% 61.23/61.28 [50]~E(x501,x502)+E(f13(x503,x504,x501,x505,x506),f13(x503,x504,x502,x505,x506))
% 61.23/61.28 [51]~E(x511,x512)+E(f13(x513,x514,x515,x511,x516),f13(x513,x514,x515,x512,x516))
% 61.23/61.28 [52]~E(x521,x522)+E(f13(x523,x524,x525,x526,x521),f13(x523,x524,x525,x526,x522))
% 61.23/61.28 [53]~E(x531,x532)+E(f12(x531,x533,x534,x535,x536,x537),f12(x532,x533,x534,x535,x536,x537))
% 61.23/61.28 [54]~E(x541,x542)+E(f12(x543,x541,x544,x545,x546,x547),f12(x543,x542,x544,x545,x546,x547))
% 61.23/61.28 [55]~E(x551,x552)+E(f12(x553,x554,x551,x555,x556,x557),f12(x553,x554,x552,x555,x556,x557))
% 61.23/61.28 [56]~E(x561,x562)+E(f12(x563,x564,x565,x561,x566,x567),f12(x563,x564,x565,x562,x566,x567))
% 61.23/61.28 [57]~E(x571,x572)+E(f12(x573,x574,x575,x576,x571,x577),f12(x573,x574,x575,x576,x572,x577))
% 61.23/61.28 [58]~E(x581,x582)+E(f12(x583,x584,x585,x586,x587,x581),f12(x583,x584,x585,x586,x587,x582))
% 61.23/61.28 [59]~E(x591,x592)+E(f30(x591,x593,x594,x595,x596),f30(x592,x593,x594,x595,x596))
% 61.23/61.28 [60]~E(x601,x602)+E(f30(x603,x601,x604,x605,x606),f30(x603,x602,x604,x605,x606))
% 61.23/61.28 [61]~E(x611,x612)+E(f30(x613,x614,x611,x615,x616),f30(x613,x614,x612,x615,x616))
% 61.23/61.28 [62]~E(x621,x622)+E(f30(x623,x624,x625,x621,x626),f30(x623,x624,x625,x622,x626))
% 61.23/61.28 [63]~E(x631,x632)+E(f30(x633,x634,x635,x636,x631),f30(x633,x634,x635,x636,x632))
% 61.23/61.28 [64]~E(x641,x642)+E(f11(x641,x643,x644,x645,x646,x647),f11(x642,x643,x644,x645,x646,x647))
% 61.23/61.28 [65]~E(x651,x652)+E(f11(x653,x651,x654,x655,x656,x657),f11(x653,x652,x654,x655,x656,x657))
% 61.23/61.28 [66]~E(x661,x662)+E(f11(x663,x664,x661,x665,x666,x667),f11(x663,x664,x662,x665,x666,x667))
% 61.23/61.28 [67]~E(x671,x672)+E(f11(x673,x674,x675,x671,x676,x677),f11(x673,x674,x675,x672,x676,x677))
% 61.23/61.28 [68]~E(x681,x682)+E(f11(x683,x684,x685,x686,x681,x687),f11(x683,x684,x685,x686,x682,x687))
% 61.23/61.28 [69]~E(x691,x692)+E(f11(x693,x694,x695,x696,x697,x691),f11(x693,x694,x695,x696,x697,x692))
% 61.23/61.28 [70]~E(x701,x702)+E(f31(x701,x703,x704,x705,x706,x707),f31(x702,x703,x704,x705,x706,x707))
% 61.23/61.28 [71]~E(x711,x712)+E(f31(x713,x711,x714,x715,x716,x717),f31(x713,x712,x714,x715,x716,x717))
% 61.23/61.28 [72]~E(x721,x722)+E(f31(x723,x724,x721,x725,x726,x727),f31(x723,x724,x722,x725,x726,x727))
% 61.23/61.28 [73]~E(x731,x732)+E(f31(x733,x734,x735,x731,x736,x737),f31(x733,x734,x735,x732,x736,x737))
% 61.23/61.28 [74]~E(x741,x742)+E(f31(x743,x744,x745,x746,x741,x747),f31(x743,x744,x745,x746,x742,x747))
% 61.23/61.28 [75]~E(x751,x752)+E(f31(x753,x754,x755,x756,x757,x751),f31(x753,x754,x755,x756,x757,x752))
% 61.23/61.28 [76]~E(x761,x762)+E(f28(x761,x763,x764,x765,x766,x767),f28(x762,x763,x764,x765,x766,x767))
% 61.23/61.28 [77]~E(x771,x772)+E(f28(x773,x771,x774,x775,x776,x777),f28(x773,x772,x774,x775,x776,x777))
% 61.23/61.28 [78]~E(x781,x782)+E(f28(x783,x784,x781,x785,x786,x787),f28(x783,x784,x782,x785,x786,x787))
% 61.23/61.28 [79]~E(x791,x792)+E(f28(x793,x794,x795,x791,x796,x797),f28(x793,x794,x795,x792,x796,x797))
% 61.23/61.28 [80]~E(x801,x802)+E(f28(x803,x804,x805,x806,x801,x807),f28(x803,x804,x805,x806,x802,x807))
% 61.23/61.28 [81]~E(x811,x812)+E(f28(x813,x814,x815,x816,x817,x811),f28(x813,x814,x815,x816,x817,x812))
% 61.23/61.28 [82]~E(x821,x822)+E(f14(x821,x823,x824,x825,x826,x827),f14(x822,x823,x824,x825,x826,x827))
% 61.23/61.28 [83]~E(x831,x832)+E(f14(x833,x831,x834,x835,x836,x837),f14(x833,x832,x834,x835,x836,x837))
% 61.23/61.28 [84]~E(x841,x842)+E(f14(x843,x844,x841,x845,x846,x847),f14(x843,x844,x842,x845,x846,x847))
% 61.23/61.28 [85]~E(x851,x852)+E(f14(x853,x854,x855,x851,x856,x857),f14(x853,x854,x855,x852,x856,x857))
% 61.23/61.28 [86]~E(x861,x862)+E(f14(x863,x864,x865,x866,x861,x867),f14(x863,x864,x865,x866,x862,x867))
% 61.23/61.28 [87]~E(x871,x872)+E(f14(x873,x874,x875,x876,x877,x871),f14(x873,x874,x875,x876,x877,x872))
% 61.23/61.28 [88]P1(x882,x883,x884)+~E(x881,x882)+~P1(x881,x883,x884)
% 61.23/61.28 [89]P1(x893,x892,x894)+~E(x891,x892)+~P1(x893,x891,x894)
% 61.23/61.28 [90]P1(x903,x904,x902)+~E(x901,x902)+~P1(x903,x904,x901)
% 61.23/61.28 [91]P7(x912,x913,x914,x915,x916,x917,x918,x919)+~E(x911,x912)+~P7(x911,x913,x914,x915,x916,x917,x918,x919)
% 61.23/61.28 [92]P7(x923,x922,x924,x925,x926,x927,x928,x929)+~E(x921,x922)+~P7(x923,x921,x924,x925,x926,x927,x928,x929)
% 61.23/61.28 [93]P7(x933,x934,x932,x935,x936,x937,x938,x939)+~E(x931,x932)+~P7(x933,x934,x931,x935,x936,x937,x938,x939)
% 61.23/61.28 [94]P7(x943,x944,x945,x942,x946,x947,x948,x949)+~E(x941,x942)+~P7(x943,x944,x945,x941,x946,x947,x948,x949)
% 61.23/61.28 [95]P7(x953,x954,x955,x956,x952,x957,x958,x959)+~E(x951,x952)+~P7(x953,x954,x955,x956,x951,x957,x958,x959)
% 61.23/61.28 [96]P7(x963,x964,x965,x966,x967,x962,x968,x969)+~E(x961,x962)+~P7(x963,x964,x965,x966,x967,x961,x968,x969)
% 61.23/61.28 [97]P7(x973,x974,x975,x976,x977,x978,x972,x979)+~E(x971,x972)+~P7(x973,x974,x975,x976,x977,x978,x971,x979)
% 61.23/61.28 [98]P7(x983,x984,x985,x986,x987,x988,x989,x982)+~E(x981,x982)+~P7(x983,x984,x985,x986,x987,x988,x989,x981)
% 61.23/61.28 [99]P3(x992,x993,x994)+~E(x991,x992)+~P3(x991,x993,x994)
% 61.23/61.28 [100]P3(x1003,x1002,x1004)+~E(x1001,x1002)+~P3(x1003,x1001,x1004)
% 61.23/61.28 [101]P3(x1013,x1014,x1012)+~E(x1011,x1012)+~P3(x1013,x1014,x1011)
% 61.23/61.28 [102]P9(x1022,x1023,x1024,x1025)+~E(x1021,x1022)+~P9(x1021,x1023,x1024,x1025)
% 61.23/61.28 [103]P9(x1033,x1032,x1034,x1035)+~E(x1031,x1032)+~P9(x1033,x1031,x1034,x1035)
% 61.23/61.28 [104]P9(x1043,x1044,x1042,x1045)+~E(x1041,x1042)+~P9(x1043,x1044,x1041,x1045)
% 61.23/61.28 [105]P9(x1053,x1054,x1055,x1052)+~E(x1051,x1052)+~P9(x1053,x1054,x1055,x1051)
% 61.23/61.28 [106]P8(x1062,x1063,x1064,x1065,x1066,x1067,x1068,x1069)+~E(x1061,x1062)+~P8(x1061,x1063,x1064,x1065,x1066,x1067,x1068,x1069)
% 61.23/61.28 [107]P8(x1073,x1072,x1074,x1075,x1076,x1077,x1078,x1079)+~E(x1071,x1072)+~P8(x1073,x1071,x1074,x1075,x1076,x1077,x1078,x1079)
% 61.23/61.28 [108]P8(x1083,x1084,x1082,x1085,x1086,x1087,x1088,x1089)+~E(x1081,x1082)+~P8(x1083,x1084,x1081,x1085,x1086,x1087,x1088,x1089)
% 61.23/61.28 [109]P8(x1093,x1094,x1095,x1092,x1096,x1097,x1098,x1099)+~E(x1091,x1092)+~P8(x1093,x1094,x1095,x1091,x1096,x1097,x1098,x1099)
% 61.23/61.28 [110]P8(x1103,x1104,x1105,x1106,x1102,x1107,x1108,x1109)+~E(x1101,x1102)+~P8(x1103,x1104,x1105,x1106,x1101,x1107,x1108,x1109)
% 61.23/61.28 [111]P8(x1113,x1114,x1115,x1116,x1117,x1112,x1118,x1119)+~E(x1111,x1112)+~P8(x1113,x1114,x1115,x1116,x1117,x1111,x1118,x1119)
% 61.23/61.28 [112]P8(x1123,x1124,x1125,x1126,x1127,x1128,x1122,x1129)+~E(x1121,x1122)+~P8(x1123,x1124,x1125,x1126,x1127,x1128,x1121,x1129)
% 61.23/61.28 [113]P8(x1133,x1134,x1135,x1136,x1137,x1138,x1139,x1132)+~E(x1131,x1132)+~P8(x1133,x1134,x1135,x1136,x1137,x1138,x1139,x1131)
% 61.23/61.28 [114]P10(x1142,x1143,x1144,x1145)+~E(x1141,x1142)+~P10(x1141,x1143,x1144,x1145)
% 61.23/61.28 [115]P10(x1153,x1152,x1154,x1155)+~E(x1151,x1152)+~P10(x1153,x1151,x1154,x1155)
% 61.23/61.28 [116]P10(x1163,x1164,x1162,x1165)+~E(x1161,x1162)+~P10(x1163,x1164,x1161,x1165)
% 61.23/61.28 [117]P10(x1173,x1174,x1175,x1172)+~E(x1171,x1172)+~P10(x1173,x1174,x1175,x1171)
% 61.23/61.28 [118]P6(x1182,x1183,x1184,x1185,x1186,x1187)+~E(x1181,x1182)+~P6(x1181,x1183,x1184,x1185,x1186,x1187)
% 61.23/61.28 [119]P6(x1193,x1192,x1194,x1195,x1196,x1197)+~E(x1191,x1192)+~P6(x1193,x1191,x1194,x1195,x1196,x1197)
% 61.23/61.28 [120]P6(x1203,x1204,x1202,x1205,x1206,x1207)+~E(x1201,x1202)+~P6(x1203,x1204,x1201,x1205,x1206,x1207)
% 61.23/61.28 [121]P6(x1213,x1214,x1215,x1212,x1216,x1217)+~E(x1211,x1212)+~P6(x1213,x1214,x1215,x1211,x1216,x1217)
% 61.23/61.28 [122]P6(x1223,x1224,x1225,x1226,x1222,x1227)+~E(x1221,x1222)+~P6(x1223,x1224,x1225,x1226,x1221,x1227)
% 61.23/61.28 [123]P6(x1233,x1234,x1235,x1236,x1237,x1232)+~E(x1231,x1232)+~P6(x1233,x1234,x1235,x1236,x1237,x1231)
% 61.23/61.28 [124]P2(x1242,x1243,x1244,x1245)+~E(x1241,x1242)+~P2(x1241,x1243,x1244,x1245)
% 61.23/61.28 [125]P2(x1253,x1252,x1254,x1255)+~E(x1251,x1252)+~P2(x1253,x1251,x1254,x1255)
% 61.23/61.28 [126]P2(x1263,x1264,x1262,x1265)+~E(x1261,x1262)+~P2(x1263,x1264,x1261,x1265)
% 61.23/61.28 [127]P2(x1273,x1274,x1275,x1272)+~E(x1271,x1272)+~P2(x1273,x1274,x1275,x1271)
% 61.23/61.28 [128]P11(x1282,x1283,x1284,x1285,x1286,x1287)+~E(x1281,x1282)+~P11(x1281,x1283,x1284,x1285,x1286,x1287)
% 61.23/61.28 [129]P11(x1293,x1292,x1294,x1295,x1296,x1297)+~E(x1291,x1292)+~P11(x1293,x1291,x1294,x1295,x1296,x1297)
% 61.23/61.28 [130]P11(x1303,x1304,x1302,x1305,x1306,x1307)+~E(x1301,x1302)+~P11(x1303,x1304,x1301,x1305,x1306,x1307)
% 61.23/61.28 [131]P11(x1313,x1314,x1315,x1312,x1316,x1317)+~E(x1311,x1312)+~P11(x1313,x1314,x1315,x1311,x1316,x1317)
% 61.23/61.28 [132]P11(x1323,x1324,x1325,x1326,x1322,x1327)+~E(x1321,x1322)+~P11(x1323,x1324,x1325,x1326,x1321,x1327)
% 61.23/61.28 [133]P11(x1333,x1334,x1335,x1336,x1337,x1332)+~E(x1331,x1332)+~P11(x1333,x1334,x1335,x1336,x1337,x1331)
% 61.23/61.28 [134]P5(x1342,x1343,x1344,x1345)+~E(x1341,x1342)+~P5(x1341,x1343,x1344,x1345)
% 61.23/61.28 [135]P5(x1353,x1352,x1354,x1355)+~E(x1351,x1352)+~P5(x1353,x1351,x1354,x1355)
% 61.23/61.28 [136]P5(x1363,x1364,x1362,x1365)+~E(x1361,x1362)+~P5(x1363,x1364,x1361,x1365)
% 61.23/61.28 [137]P5(x1373,x1374,x1375,x1372)+~E(x1371,x1372)+~P5(x1373,x1374,x1375,x1371)
% 61.23/61.28 [138]P4(x1382,x1383,x1384,x1385)+~E(x1381,x1382)+~P4(x1381,x1383,x1384,x1385)
% 61.23/61.28 [139]P4(x1393,x1392,x1394,x1395)+~E(x1391,x1392)+~P4(x1393,x1391,x1394,x1395)
% 61.23/61.28 [140]P4(x1403,x1404,x1402,x1405)+~E(x1401,x1402)+~P4(x1403,x1404,x1401,x1405)
% 61.23/61.28 [141]P4(x1413,x1414,x1415,x1412)+~E(x1411,x1412)+~P4(x1413,x1414,x1415,x1411)
% 61.23/61.28
% 61.23/61.28 %-------------------------------------------
% 61.23/61.28 cnf(265,plain,
% 61.23/61.28 (~P10(a18,a19,a1,a19)),
% 61.23/61.28 inference(scs_inference,[],[151,166])).
% 61.23/61.28 cnf(267,plain,
% 61.23/61.28 (~P10(a1,a19,a19,a18)),
% 61.23/61.28 inference(scs_inference,[],[151,166,167])).
% 61.23/61.28 cnf(269,plain,
% 61.23/61.28 (P1(a18,a18,a1)),
% 61.23/61.28 inference(scs_inference,[],[142,151,166,167,156])).
% 61.23/61.28 cnf(271,plain,
% 61.23/61.28 (P9(a3,a3,a16,a16)),
% 61.23/61.28 inference(scs_inference,[],[142,144,151,166,167,156,158])).
% 61.23/61.28 cnf(273,plain,
% 61.23/61.28 (P9(a17,a17,a16,a16)),
% 61.23/61.28 inference(scs_inference,[],[142,144,151,166,167,156,158,159])).
% 61.23/61.28 cnf(277,plain,
% 61.23/61.29 (P7(a19,a3,a3,a16,a19,a3,a3,a16)),
% 61.23/61.29 inference(scs_inference,[],[142,143,144,147,151,166,167,156,158,159,242,229])).
% 61.23/61.29 cnf(279,plain,
% 61.23/61.29 (~P8(a17,a2,a2,a18,a1,a19,a18,a19)),
% 61.23/61.29 inference(scs_inference,[],[142,143,144,147,151,166,167,156,158,159,242,229,253])).
% 61.23/61.29 cnf(283,plain,
% 61.23/61.29 (~P8(a19,a1,a18,a19,a17,a2,a2,a18)),
% 61.23/61.29 inference(scs_inference,[],[142,143,144,147,151,166,167,156,158,159,242,229,253,254,255])).
% 61.23/61.29 cnf(285,plain,
% 61.23/61.29 (~P8(a1,a19,a17,a2,a18,a19,a2,a18)),
% 61.23/61.29 inference(scs_inference,[],[142,143,144,147,151,166,167,156,158,159,242,229,253,254,255,256])).
% 61.23/61.29 cnf(287,plain,
% 61.23/61.29 (~P1(x2871,a1,a18)+~P2(x2871,a1,a19,a18)),
% 61.23/61.29 inference(scs_inference,[],[142,143,144,147,151,166,167,156,158,159,242,229,253,254,255,256,173])).
% 61.23/61.29 cnf(310,plain,
% 61.23/61.29 (~P8(a2,a18,a17,a2,a18,a19,a1,a19)),
% 61.23/61.29 inference(scs_inference,[],[279,256,254])).
% 61.23/61.29 cnf(312,plain,
% 61.23/61.29 (~P8(a17,a2,a2,a18,a19,a1,a18,a19)),
% 61.23/61.29 inference(scs_inference,[],[279,283,256,254,253])).
% 61.23/61.29 cnf(314,plain,
% 61.23/61.29 (~P8(a2,a17,a2,a18,a1,a19,a18,a19)),
% 61.23/61.29 inference(scs_inference,[],[279,283,256,254,253,255])).
% 61.23/61.29 cnf(316,plain,
% 61.23/61.29 (~P10(a18,a19,a19,a1)),
% 61.23/61.29 inference(scs_inference,[],[265,279,283,256,254,253,255,167])).
% 61.23/61.29 cnf(318,plain,
% 61.23/61.29 (~P10(a19,a18,a1,a19)),
% 61.23/61.29 inference(scs_inference,[],[265,267,279,283,256,254,253,255,167,166])).
% 61.23/61.29 cnf(320,plain,
% 61.23/61.29 (P9(a1,a1,a18,a18)),
% 61.23/61.29 inference(scs_inference,[],[145,265,267,279,283,256,254,253,255,167,166,158])).
% 61.23/61.29 cnf(322,plain,
% 61.23/61.29 (P1(a16,a16,a19)),
% 61.23/61.29 inference(scs_inference,[],[145,143,265,267,279,283,256,254,253,255,167,166,158,156])).
% 61.23/61.29 cnf(324,plain,
% 61.23/61.29 (P9(a20,a20,a18,a18)),
% 61.23/61.29 inference(scs_inference,[],[145,143,265,267,279,283,256,254,253,255,167,166,158,156,159])).
% 61.23/61.29 cnf(328,plain,
% 61.23/61.29 (~P8(a1,a19,a18,a19,a19,a20,a3,a16)),
% 61.23/61.29 inference(scs_inference,[],[145,148,143,151,269,265,267,279,283,256,254,253,255,167,166,158,156,159,173,242])).
% 61.23/61.29 cnf(337,plain,
% 61.23/61.29 (P3(x3371,a1,a18)+~E(a20,x3371)),
% 61.23/61.29 inference(scs_inference,[],[142,145,148,149,143,147,151,269,265,267,279,283,256,254,253,255,167,166,158,156,159,173,242,230,243,88,89,90,99])).
% 61.23/61.29 cnf(342,plain,
% 61.23/61.29 (~P8(a1,a19,a19,a20,a18,a19,a3,a16)),
% 61.23/61.29 inference(scs_inference,[],[328,256])).
% 61.23/61.29 cnf(344,plain,
% 61.23/61.29 (~P8(a18,a19,a1,a19,a3,a16,a19,a20)),
% 61.23/61.29 inference(scs_inference,[],[328,256,254])).
% 61.23/61.29 cnf(346,plain,
% 61.23/61.29 (~P8(a19,a20,a3,a16,a1,a19,a18,a19)),
% 61.23/61.29 inference(scs_inference,[],[328,256,254,253])).
% 61.23/61.29 cnf(348,plain,
% 61.23/61.29 (~P8(a19,a1,a18,a19,a19,a20,a3,a16)),
% 61.23/61.29 inference(scs_inference,[],[328,256,254,253,255])).
% 61.23/61.29 cnf(350,plain,
% 61.23/61.29 (~P10(a19,a18,a19,a1)),
% 61.23/61.29 inference(scs_inference,[],[318,328,256,254,253,255,167])).
% 61.23/61.29 cnf(352,plain,
% 61.23/61.29 (~P10(a19,a1,a18,a19)),
% 61.23/61.29 inference(scs_inference,[],[316,318,328,256,254,253,255,167,166])).
% 61.23/61.29 cnf(354,plain,
% 61.23/61.29 (~P8(a18,a19,a19,a1,a19,a20,a3,a16)),
% 61.23/61.29 inference(scs_inference,[],[148,316,318,328,256,254,253,255,167,166,242])).
% 61.23/61.29 cnf(356,plain,
% 61.23/61.29 (P1(a19,a19,a16)),
% 61.23/61.29 inference(scs_inference,[],[148,316,318,322,328,256,254,253,255,167,166,242,156])).
% 61.23/61.29 cnf(366,plain,
% 61.23/61.29 (~P8(a19,a18,a19,a1,a19,a20,a3,a16)),
% 61.23/61.29 inference(scs_inference,[],[354,255])).
% 61.23/61.29 cnf(368,plain,
% 61.23/61.29 (~P8(a19,a20,a3,a16,a18,a19,a19,a1)),
% 61.23/61.29 inference(scs_inference,[],[354,255,253])).
% 61.23/61.29 cnf(370,plain,
% 61.23/61.29 (~P8(a18,a19,a19,a20,a19,a1,a3,a16)),
% 61.23/61.29 inference(scs_inference,[],[354,255,253,256])).
% 61.23/61.29 cnf(374,plain,
% 61.23/61.29 (~P10(a19,a1,a19,a18)),
% 61.23/61.29 inference(scs_inference,[],[352,354,255,253,256,254,167])).
% 61.23/61.29 cnf(376,plain,
% 61.23/61.29 (~P8(a18,a19,a1,a19,a19,a20,a3,a16)),
% 61.23/61.29 inference(scs_inference,[],[148,352,354,265,255,253,256,254,167,242])).
% 61.23/61.29 cnf(380,plain,
% 61.23/61.29 (P7(a1,a1,a1,a18,a1,a1,a1,a18)),
% 61.23/61.29 inference(scs_inference,[],[148,320,352,354,269,265,255,253,256,254,167,242,156,229])).
% 61.23/61.29 cnf(383,plain,
% 61.23/61.29 (~P2(a1,a1,a19,a18)),
% 61.23/61.29 inference(scs_inference,[],[148,320,352,354,269,265,267,255,253,256,254,167,242,156,229,114,173])).
% 61.23/61.29 cnf(396,plain,
% 61.23/61.29 (~P8(a1,a19,a18,a19,a3,a16,a19,a20)),
% 61.23/61.29 inference(scs_inference,[],[376,254])).
% 61.23/61.29 cnf(398,plain,
% 61.23/61.29 (~P8(a18,a19,a19,a20,a1,a19,a3,a16)),
% 61.23/61.29 inference(scs_inference,[],[376,254,256])).
% 61.23/61.29 cnf(400,plain,
% 61.23/61.29 (~P8(a19,a20,a3,a16,a18,a19,a1,a19)),
% 61.23/61.29 inference(scs_inference,[],[376,254,256,253])).
% 61.23/61.29 cnf(402,plain,
% 61.23/61.29 (~P8(a19,a18,a1,a19,a19,a20,a3,a16)),
% 61.23/61.29 inference(scs_inference,[],[376,254,256,253,255])).
% 61.23/61.29 cnf(404,plain,
% 61.23/61.29 (~P8(a18,a19,a19,a1,a17,a2,a2,a18)),
% 61.23/61.29 inference(scs_inference,[],[147,316,376,254,256,253,255,242])).
% 61.23/61.29 cnf(409,plain,
% 61.23/61.29 (~P11(a17,a2,a18,a18,a19,a1)),
% 61.23/61.29 inference(scs_inference,[],[149,147,316,376,254,256,253,255,242,232,126,215])).
% 61.23/61.29 cnf(411,plain,
% 61.23/61.29 (~P11(a19,a18,a1,a2,a17,a18)),
% 61.23/61.29 inference(scs_inference,[],[149,147,316,376,254,256,253,255,242,232,126,215,216])).
% 61.23/61.29 cnf(413,plain,
% 61.23/61.29 (~P11(a18,a1,a19,a17,a18,a2)),
% 61.23/61.29 inference(scs_inference,[],[149,147,316,376,254,256,253,255,242,232,126,215,216,217])).
% 61.23/61.29 cnf(422,plain,
% 61.23/61.29 (~P11(a2,a17,a18,a19,a18,a1)),
% 61.23/61.29 inference(scs_inference,[],[409,216])).
% 61.23/61.29 cnf(424,plain,
% 61.23/61.29 (~P11(a17,a18,a2,a18,a1,a19)),
% 61.23/61.29 inference(scs_inference,[],[409,413,216,215])).
% 61.23/61.29 cnf(426,plain,
% 61.23/61.29 (~P11(a19,a1,a18,a2,a18,a17)),
% 61.23/61.29 inference(scs_inference,[],[409,411,413,216,215,217])).
% 61.23/61.29 cnf(428,plain,
% 61.23/61.29 (~P8(a19,a18,a19,a1,a17,a2,a2,a18)),
% 61.23/61.29 inference(scs_inference,[],[404,409,411,413,216,215,217,255])).
% 61.23/61.29 cnf(430,plain,
% 61.23/61.29 (~P8(a19,a1,a18,a19,a2,a18,a17,a2)),
% 61.23/61.29 inference(scs_inference,[],[404,409,411,413,216,215,217,255,254])).
% 61.23/61.29 cnf(432,plain,
% 61.23/61.29 (~P8(a17,a2,a2,a18,a18,a19,a19,a1)),
% 61.23/61.29 inference(scs_inference,[],[404,409,411,413,216,215,217,255,254,253])).
% 61.23/61.29 cnf(436,plain,
% 61.23/61.29 (~P8(a1,a19,a19,a18,a17,a2,a2,a18)),
% 61.23/61.29 inference(scs_inference,[],[147,267,404,409,411,413,216,215,217,255,254,253,256,242])).
% 61.23/61.29 cnf(438,plain,
% 61.23/61.29 (~P11(a1,a19,a18,a17,a2,a18)),
% 61.23/61.29 inference(scs_inference,[],[147,267,404,409,411,413,216,215,217,255,254,253,256,242,232])).
% 61.23/61.29 cnf(452,plain,
% 61.23/61.29 (~P11(a18,a17,a2,a1,a18,a19)),
% 61.23/61.29 inference(scs_inference,[],[424,216])).
% 61.23/61.29 cnf(454,plain,
% 61.23/61.29 (~P11(a2,a18,a17,a19,a1,a18)),
% 61.23/61.29 inference(scs_inference,[],[422,424,216,217])).
% 61.23/61.29 cnf(456,plain,
% 61.23/61.29 (~P11(a17,a2,a18,a1,a19,a18)),
% 61.23/61.29 inference(scs_inference,[],[422,424,438,216,217,215])).
% 61.23/61.29 cnf(460,plain,
% 61.23/61.29 (~P8(a19,a1,a19,a18,a17,a2,a2,a18)),
% 61.23/61.29 inference(scs_inference,[],[436,422,424,438,216,217,215,256,255])).
% 61.23/61.29 cnf(462,plain,
% 61.23/61.29 (~P8(a19,a18,a1,a19,a2,a18,a17,a2)),
% 61.23/61.29 inference(scs_inference,[],[436,422,424,438,216,217,215,256,255,254])).
% 61.23/61.29 cnf(464,plain,
% 61.23/61.29 (~P8(a17,a2,a2,a18,a1,a19,a19,a18)),
% 61.23/61.29 inference(scs_inference,[],[436,422,424,438,216,217,215,256,255,254,253])).
% 61.23/61.29 cnf(466,plain,
% 61.23/61.29 (~P8(a1,a19,a19,a18,a19,a20,a3,a16)),
% 61.23/61.29 inference(scs_inference,[],[148,267,436,422,424,438,216,217,215,256,255,254,253,242])).
% 61.23/61.29 cnf(474,plain,
% 61.23/61.29 (~P11(a2,a17,a18,a19,a1,a18)),
% 61.23/61.29 inference(scs_inference,[],[456,216])).
% 61.23/61.29 cnf(478,plain,
% 61.23/61.29 (~P11(a17,a18,a2,a1,a18,a19)),
% 61.23/61.29 inference(scs_inference,[],[456,452,216,215,217])).
% 61.23/61.29 cnf(480,plain,
% 61.23/61.29 (~P8(a1,a19,a19,a20,a19,a18,a3,a16)),
% 61.23/61.29 inference(scs_inference,[],[466,456,452,216,215,217,256])).
% 61.23/61.29 cnf(482,plain,
% 61.23/61.29 (~P8(a19,a1,a19,a18,a19,a20,a3,a16)),
% 61.23/61.29 inference(scs_inference,[],[466,456,452,216,215,217,256,255])).
% 61.23/61.29 cnf(484,plain,
% 61.23/61.29 (~P8(a19,a20,a3,a16,a1,a19,a19,a18)),
% 61.23/61.29 inference(scs_inference,[],[466,456,452,216,215,217,256,255,253])).
% 61.23/61.29 cnf(486,plain,
% 61.23/61.29 (~P8(a19,a18,a1,a19,a3,a16,a19,a20)),
% 61.23/61.29 inference(scs_inference,[],[466,456,452,216,215,217,256,255,253,254])).
% 61.23/61.29 cnf(488,plain,
% 61.23/61.29 (~P8(a19,a18,a1,a19,a17,a2,a2,a18)),
% 61.23/61.29 inference(scs_inference,[],[147,318,466,456,452,216,215,217,256,255,253,254,242])).
% 61.23/61.29 cnf(490,plain,
% 61.23/61.29 (~P9(x4901,x4902,a3,a18)+P9(x4901,x4902,a1,a16)),
% 61.23/61.29 inference(scs_inference,[],[147,146,318,466,456,452,216,215,217,256,255,253,254,242,180])).
% 61.23/61.29 cnf(500,plain,
% 61.23/61.29 (~P11(a2,a18,a17,a19,a18,a1)),
% 61.23/61.29 inference(scs_inference,[],[474,217])).
% 61.23/61.29 cnf(504,plain,
% 61.23/61.29 (~P11(a19,a1,a18,a2,a17,a18)),
% 61.23/61.29 inference(scs_inference,[],[454,474,217,216,215])).
% 61.23/61.29 cnf(506,plain,
% 61.23/61.29 (~P8(a19,a18,a17,a2,a1,a19,a2,a18)),
% 61.23/61.29 inference(scs_inference,[],[488,454,474,217,216,215,256])).
% 61.23/61.29 cnf(508,plain,
% 61.23/61.29 (~P8(a18,a19,a1,a19,a17,a2,a2,a18)),
% 61.23/61.29 inference(scs_inference,[],[488,454,474,217,216,215,256,255])).
% 61.23/61.29 cnf(510,plain,
% 61.23/61.29 (~P8(a1,a19,a19,a18,a2,a18,a17,a2)),
% 61.23/61.29 inference(scs_inference,[],[488,454,474,217,216,215,256,255,254])).
% 61.23/61.29 cnf(512,plain,
% 61.23/61.29 (~P8(a17,a2,a2,a18,a19,a18,a1,a19)),
% 61.23/61.29 inference(scs_inference,[],[488,454,474,217,216,215,256,255,254,253])).
% 61.23/61.29 cnf(514,plain,
% 61.23/61.29 (~P9(x5141,x5142,a3,a3)+P9(x5141,x5142,a16,a16)),
% 61.23/61.29 inference(scs_inference,[],[271,488,454,474,217,216,215,256,255,254,253,180])).
% 61.23/61.29 cnf(528,plain,
% 61.23/61.29 (~P11(a1,a19,a18,a18,a2,a17)),
% 61.23/61.29 inference(scs_inference,[],[426,478,215,216])).
% 61.23/61.29 cnf(532,plain,
% 61.23/61.29 (~P8(a17,a2,a18,a19,a2,a18,a19,a1)),
% 61.23/61.29 inference(scs_inference,[],[432,426,478,504,215,216,217,256])).
% 61.23/61.29 cnf(534,plain,
% 61.23/61.29 (~P8(a18,a19,a2,a18,a1,a19,a17,a2)),
% 61.23/61.29 inference(scs_inference,[],[432,285,426,478,504,215,216,217,256,253])).
% 61.23/61.29 cnf(536,plain,
% 61.23/61.29 (~P8(a2,a17,a2,a18,a18,a19,a19,a1)),
% 61.23/61.29 inference(scs_inference,[],[432,285,426,478,504,215,216,217,256,253,255])).
% 61.23/61.29 cnf(538,plain,
% 61.23/61.29 (~P8(a2,a18,a17,a2,a19,a1,a18,a19)),
% 61.23/61.29 inference(scs_inference,[],[432,285,426,478,504,215,216,217,256,253,255,254])).
% 61.23/61.29 cnf(555,plain,
% 61.23/61.29 (~P8(a17,a2,a1,a19,a2,a18,a19,a18)),
% 61.23/61.29 inference(scs_inference,[],[464,500,216,256])).
% 61.23/61.29 cnf(557,plain,
% 61.23/61.29 (~P8(a2,a18,a17,a2,a19,a18,a1,a19)),
% 61.23/61.29 inference(scs_inference,[],[464,500,216,256,254])).
% 61.23/61.29 cnf(559,plain,
% 61.23/61.29 (~P8(a17,a2,a2,a18,a19,a18,a19,a1)),
% 61.23/61.29 inference(scs_inference,[],[464,428,500,216,256,254,253])).
% 61.23/61.29 cnf(561,plain,
% 61.23/61.29 (~P8(a2,a17,a2,a18,a1,a19,a19,a18)),
% 61.23/61.29 inference(scs_inference,[],[464,428,500,216,256,254,253,255])).
% 61.23/61.29 cnf(563,plain,
% 61.23/61.29 (~P11(a18,a17,a2,a18,a1,a19)),
% 61.23/61.29 inference(scs_inference,[],[464,428,500,216,256,254,253,255,217])).
% 61.23/61.29 cnf(571,plain,
% 61.23/61.29 (~P4(a1,a1,a1,a19)+~E(a20,a1)),
% 61.23/61.29 inference(scs_inference,[],[383,464,428,500,216,256,254,253,255,217,215,185,157,337])).
% 61.23/61.29 cnf(592,plain,
% 61.23/61.29 (~P8(a19,a1,a17,a2,a19,a18,a2,a18)),
% 61.23/61.29 inference(scs_inference,[],[460,563,215,256])).
% 61.23/61.29 cnf(594,plain,
% 61.23/61.29 (~P8(a17,a2,a2,a18,a19,a1,a19,a18)),
% 61.23/61.29 inference(scs_inference,[],[460,563,215,256,253])).
% 61.23/61.29 cnf(596,plain,
% 61.23/61.29 (~P8(a19,a18,a19,a1,a2,a18,a17,a2)),
% 61.23/61.29 inference(scs_inference,[],[460,563,215,256,253,254])).
% 61.23/61.29 cnf(598,plain,
% 61.23/61.29 (~P8(a1,a19,a18,a19,a2,a18,a17,a2)),
% 61.23/61.29 inference(scs_inference,[],[460,430,563,215,256,253,254,255])).
% 61.23/61.29 cnf(604,plain,
% 61.23/61.29 (~P10(x6041,x6042,a17,a2)+P9(x6041,x6042,a2,a18)),
% 61.23/61.29 inference(scs_inference,[],[147,316,277,460,430,563,215,256,253,254,255,91,97,182,181])).
% 61.23/61.29 cnf(606,plain,
% 61.23/61.29 (~P10(a3,x6061,x6061,a16)+P4(a3,a17,x6061,a17)),
% 61.23/61.29 inference(scs_inference,[],[144,147,316,277,460,430,563,215,256,253,254,255,91,97,182,181,175])).
% 61.23/61.29 cnf(608,plain,
% 61.23/61.29 (~P9(x6081,x6082,a1,a1)+P9(x6081,x6082,a18,a18)),
% 61.23/61.29 inference(scs_inference,[],[144,147,316,320,277,460,430,563,215,256,253,254,255,91,97,182,181,175,180])).
% 61.23/61.29 cnf(614,plain,
% 61.23/61.29 (~P8(a18,a19,a19,a1,a3,a16,a19,a20)),
% 61.23/61.29 inference(scs_inference,[],[508,348,256,254])).
% 61.23/61.29 cnf(616,plain,
% 61.23/61.29 (~P8(a17,a2,a2,a18,a18,a19,a1,a19)),
% 61.23/61.29 inference(scs_inference,[],[508,348,256,254,253])).
% 61.23/61.29 cnf(626,plain,
% 61.23/61.29 (~P8(a19,a20,a3,a16,a19,a18,a19,a1)),
% 61.23/61.29 inference(scs_inference,[],[366,253])).
% 61.23/61.29 cnf(630,plain,
% 61.23/61.29 (~P8(a19,a1,a19,a18,a3,a16,a19,a20)),
% 61.23/61.29 inference(scs_inference,[],[462,366,253,256,254])).
% 61.23/61.29 cnf(632,plain,
% 61.23/61.29 (~P8(a18,a2,a17,a2,a18,a19,a1,a19)),
% 61.23/61.29 inference(scs_inference,[],[462,366,310,253,256,254,255])).
% 61.23/61.29 cnf(636,plain,
% 61.23/61.29 (~P9(x6361,x6362,a20,a20)+P9(x6361,x6362,a18,a18)),
% 61.23/61.29 inference(scs_inference,[],[324,380,277,462,366,310,253,256,254,255,92,96,180])).
% 61.23/61.29 cnf(646,plain,
% 61.23/61.29 (~P8(a1,a19,a19,a18,a3,a16,a19,a20)),
% 61.23/61.29 inference(scs_inference,[],[402,254])).
% 61.23/61.29 cnf(648,plain,
% 61.23/61.29 (~P8(a19,a20,a3,a16,a19,a18,a1,a19)),
% 61.23/61.29 inference(scs_inference,[],[402,254,253])).
% 61.23/61.29 cnf(650,plain,
% 61.23/61.29 (~P8(a19,a1,a19,a20,a18,a19,a3,a16)),
% 61.23/61.29 inference(scs_inference,[],[402,342,254,253,255])).
% 61.23/61.29 cnf(652,plain,
% 61.23/61.29 (~P8(a19,a18,a19,a20,a1,a19,a3,a16)),
% 61.23/61.29 inference(scs_inference,[],[402,342,254,253,255,256])).
% 61.23/61.29 cnf(660,plain,
% 61.23/61.29 (~P8(a19,a1,a19,a20,a19,a18,a3,a16)),
% 61.23/61.29 inference(scs_inference,[],[482,256])).
% 61.23/61.29 cnf(662,plain,
% 61.23/61.29 (~P8(a20,a19,a3,a16,a1,a19,a18,a19)),
% 61.23/61.29 inference(scs_inference,[],[482,346,256,255])).
% 61.23/61.29 cnf(664,plain,
% 61.23/61.29 (~P8(a19,a18,a19,a1,a3,a16,a19,a20)),
% 61.23/61.29 inference(scs_inference,[],[482,346,256,255,254])).
% 61.23/61.29 cnf(666,plain,
% 61.23/61.29 (~P8(a19,a20,a3,a16,a19,a1,a19,a18)),
% 61.23/61.29 inference(scs_inference,[],[482,346,256,255,254,253])).
% 61.23/61.29 cnf(670,plain,
% 61.23/61.29 (~P9(x6701,x6702,a17,a17)+P9(x6701,x6702,a16,a16)),
% 61.23/61.29 inference(scs_inference,[],[147,273,277,482,346,256,255,254,253,93,117,180])).
% 61.23/61.29 cnf(683,plain,
% 61.23/61.29 (~P8(a19,a18,a3,a16,a1,a19,a19,a20)),
% 61.23/61.29 inference(scs_inference,[],[486,368,253,254,256])).
% 61.23/61.29 cnf(685,plain,
% 61.23/61.29 (~P8(a20,a19,a3,a16,a18,a19,a19,a1)),
% 61.23/61.29 inference(scs_inference,[],[486,368,253,254,256,255])).
% 61.23/61.29 cnf(689,plain,
% 61.23/61.29 (~P10(a1,x6891,x6891,a18)+P4(a1,a20,x6891,a20)),
% 61.23/61.29 inference(scs_inference,[],[145,147,277,486,368,253,254,256,255,98,115,175])).
% 61.23/61.29 cnf(705,plain,
% 61.23/61.29 (~P10(x7051,x7052,a19,a20)+P9(x7051,x7052,a3,a16)),
% 61.23/61.29 inference(scs_inference,[],[148,344,370,255,256,253,254,181])).
% 61.23/61.29 cnf(719,plain,
% 61.23/61.29 (~P8(a2,a18,a19,a18,a17,a2,a1,a19)),
% 61.23/61.29 inference(scs_inference,[],[555,398,254,253])).
% 61.23/61.29 cnf(721,plain,
% 61.23/61.29 (~P8(a2,a17,a1,a19,a2,a18,a19,a18)),
% 61.23/61.29 inference(scs_inference,[],[555,398,254,253,255])).
% 61.23/61.29 cnf(736,plain,
% 61.23/61.29 (~P8(a3,a16,a19,a20,a1,a19,a18,a19)),
% 61.23/61.29 inference(scs_inference,[],[396,400,256,255,254])).
% 61.23/61.29 cnf(738,plain,
% 61.23/61.29 (~P8(a1,a19,a2,a18,a19,a18,a17,a2)),
% 61.23/61.29 inference(scs_inference,[],[396,400,506,256,255,254,253])).
% 61.23/61.29 cnf(747,plain,
% 61.23/61.29 (~P8(a19,a20,a1,a19,a3,a16,a19,a18)),
% 61.23/61.29 inference(scs_inference,[],[480,510,253,254])).
% 61.23/61.29 cnf(751,plain,
% 61.23/61.29 (~P8(a20,a19,a3,a16,a1,a19,a19,a18)),
% 61.23/61.29 inference(scs_inference,[],[480,484,510,512,253,254,256,255])).
% 61.23/61.29 cnf(763,plain,
% 61.23/61.29 (~P8(a2,a17,a18,a19,a2,a18,a19,a1)),
% 61.23/61.29 inference(scs_inference,[],[532,255])).
% 61.23/61.29 cnf(765,plain,
% 61.23/61.29 (~P8(a2,a18,a19,a1,a17,a2,a18,a19)),
% 61.23/61.29 inference(scs_inference,[],[532,538,255,256])).
% 61.23/61.29 cnf(767,plain,
% 61.23/61.29 (~P8(a18,a19,a19,a1,a2,a17,a2,a18)),
% 61.23/61.29 inference(scs_inference,[],[532,536,538,255,256,253])).
% 61.23/61.29 cnf(784,plain,
% 61.23/61.29 (~P8(a2,a18,a18,a19,a17,a2,a1,a19)),
% 61.23/61.29 inference(scs_inference,[],[534,254])).
% 61.23/61.29 cnf(790,plain,
% 61.23/61.29 (~P8(a1,a19,a2,a18,a18,a19,a17,a2)),
% 61.23/61.29 inference(scs_inference,[],[557,534,561,598,254,253,255,256])).
% 61.23/61.29 cnf(799,plain,
% 61.23/61.29 (~P8(a18,a2,a19,a18,a17,a2,a1,a19)),
% 61.23/61.29 inference(scs_inference,[],[719,736,256,255])).
% 61.23/61.29 cnf(801,plain,
% 61.23/61.29 (~P8(a17,a2,a19,a1,a2,a18,a19,a18)),
% 61.23/61.29 inference(scs_inference,[],[592,719,736,256,255,254])).
% 61.23/61.29 cnf(803,plain,
% 61.23/61.29 (~P8(a19,a18,a2,a18,a19,a1,a17,a2)),
% 61.23/61.29 inference(scs_inference,[],[592,719,736,256,255,254,253])).
% 61.23/61.29 cnf(819,plain,
% 61.23/61.29 (~P8(a17,a2,a19,a1,a2,a18,a18,a19)),
% 61.23/61.29 inference(scs_inference,[],[683,660,312,253,254,256])).
% 61.23/61.29 cnf(821,plain,
% 61.23/61.29 (~P8(a19,a1,a2,a18,a19,a18,a17,a2)),
% 61.23/61.29 inference(scs_inference,[],[683,660,738,312,253,254,256,255])).
% 61.23/61.29 cnf(829,plain,
% 61.23/61.29 (~P8(a2,a17,a1,a19,a2,a18,a18,a19)),
% 61.23/61.29 inference(scs_inference,[],[747,314,255,256])).
% 61.23/61.29 cnf(831,plain,
% 61.23/61.29 (~P8(a2,a18,a19,a18,a2,a17,a1,a19)),
% 61.23/61.29 inference(scs_inference,[],[721,747,314,255,256,253])).
% 61.23/61.29 cnf(845,plain,
% 61.23/61.29 (~P8(a18,a2,a19,a1,a17,a2,a18,a19)),
% 61.23/61.29 inference(scs_inference,[],[763,765,254,253,255])).
% 61.23/61.29 cnf(847,plain,
% 61.23/61.29 (~P8(a17,a2,a19,a18,a2,a18,a19,a1)),
% 61.23/61.29 inference(scs_inference,[],[763,765,559,254,253,255,256])).
% 61.23/61.29 cnf(854,plain,
% 61.23/61.29 (~P8(a18,a19,a3,a16,a19,a1,a19,a20)),
% 61.23/61.29 inference(scs_inference,[],[614,256])).
% 61.23/61.29 cnf(858,plain,
% 61.23/61.29 (~P8(a2,a18,a17,a2,a19,a18,a19,a1)),
% 61.23/61.29 inference(scs_inference,[],[594,614,256,255,254])).
% 61.23/61.29 cnf(864,plain,
% 61.23/61.29 (~P10(a1,a16,x8641,x8642)+P10(a3,a18,x8641,x8642)),
% 61.23/61.29 inference(scs_inference,[],[146,271,356,594,614,256,255,254,253,102,89,183])).
% 61.23/61.29 cnf(869,plain,
% 61.23/61.29 (~P8(a2,a18,a19,a18,a17,a2,a19,a1)),
% 61.23/61.29 inference(scs_inference,[],[801,253])).
% 61.23/61.29 cnf(871,plain,
% 61.23/61.29 (~P8(a2,a18,a1,a19,a17,a2,a18,a19)),
% 61.23/61.29 inference(scs_inference,[],[790,801,253,254])).
% 61.23/61.29 cnf(873,plain,
% 61.23/61.29 (~P8(a17,a2,a18,a19,a2,a18,a1,a19)),
% 61.23/61.29 inference(scs_inference,[],[790,801,616,253,254,256])).
% 61.23/61.29 cnf(877,plain,
% 61.23/61.29 (~P10(a16,a16,x8771,x8772)+P10(a3,a3,x8771,x8772)),
% 61.23/61.29 inference(scs_inference,[],[271,784,790,801,616,253,254,256,255,183])).
% 61.23/61.29 cnf(898,plain,
% 61.23/61.29 (~P8(a19,a20,a19,a18,a3,a16,a19,a1)),
% 61.23/61.29 inference(scs_inference,[],[803,626,255,256])).
% 61.23/61.29 cnf(908,plain,
% 61.23/61.29 (~P10(a18,a18,x9081,x9082)+P10(a1,a1,x9081,x9082)),
% 61.23/61.29 inference(scs_inference,[],[271,320,322,324,803,829,626,255,256,253,254,88,105,90,104,183])).
% 61.23/61.29 cnf(916,plain,
% 61.23/61.29 (~P8(a17,a2,a18,a2,a1,a19,a18,a19)),
% 61.23/61.29 inference(scs_inference,[],[632,254])).
% 61.23/61.29 cnf(918,plain,
% 61.23/61.29 (~P8(a3,a16,a19,a20,a19,a1,a19,a18)),
% 61.23/61.29 inference(scs_inference,[],[630,632,254,253])).
% 61.23/61.29 cnf(924,plain,
% 61.23/61.29 (~P10(a18,a18,x9241,x9242)+P10(a20,a20,x9241,x9242)),
% 61.23/61.29 inference(scs_inference,[],[324,858,630,632,254,253,255,256,183])).
% 61.23/61.29 cnf(936,plain,
% 61.23/61.29 (~P10(a2,a18,a18,a18)+P10(a20,a20,a2,a18)),
% 61.23/61.29 inference(scs_inference,[],[147,324,858,630,632,254,253,255,256,183,242,226,234,165,164,166])).
% 61.23/61.29 cnf(946,plain,
% 61.23/61.29 (~P8(a18,a2,a19,a18,a17,a2,a19,a1)),
% 61.23/61.29 inference(scs_inference,[],[869,821,256,255])).
% 61.23/61.29 cnf(948,plain,
% 61.23/61.29 (~P8(a2,a18,a19,a1,a17,a2,a19,a18)),
% 61.23/61.29 inference(scs_inference,[],[869,821,256,255,254])).
% 61.23/61.29 cnf(950,plain,
% 61.23/61.29 (~P8(a3,a16,a19,a20,a1,a19,a19,a18)),
% 61.23/61.29 inference(scs_inference,[],[869,821,646,256,255,254,253])).
% 61.23/61.29 cnf(962,plain,
% 61.23/61.29 (~P8(a2,a17,a18,a19,a2,a18,a1,a19)),
% 61.23/61.29 inference(scs_inference,[],[873,871,650,652,253,254,256,255])).
% 61.23/61.29 cnf(978,plain,
% 61.23/61.29 (~P10(a16,a16,x9781,x9782)+P10(a17,a17,x9781,x9782)),
% 61.23/61.29 inference(scs_inference,[],[269,273,596,948,854,662,255,256,253,254,90,183])).
% 61.23/61.30 cnf(989,plain,
% 61.23/61.30 (~P8(a3,a16,a19,a20,a19,a18,a19,a1)),
% 61.23/61.30 inference(scs_inference,[],[666,254])).
% 61.23/61.30 cnf(995,plain,
% 61.23/61.30 (~P8(a3,a16,a1,a19,a19,a20,a19,a18)),
% 61.31/61.30 inference(scs_inference,[],[847,950,666,685,254,253,255,256])).
% 61.31/61.30 cnf(1003,plain,
% 61.31/61.30 (~P8(a19,a20,a19,a18,a3,a16,a1,a19)),
% 61.31/61.30 inference(scs_inference,[],[648,256])).
% 61.31/61.30 cnf(1015,plain,
% 61.31/61.30 (~P8(a3,a16,a19,a1,a19,a20,a19,a18)),
% 61.31/61.30 inference(scs_inference,[],[898,253])).
% 61.31/61.30 cnf(1019,plain,
% 61.31/61.30 (~P8(a3,a16,a19,a18,a19,a20,a19,a1)),
% 61.31/61.30 inference(scs_inference,[],[989,898,751,253,254,256])).
% 61.31/61.30 cnf(1060,plain,
% 61.31/61.30 (P7(x10601,a17,a17,a16,x10601,a17,a17,a16)+~P1(x10601,a17,a16)),
% 61.31/61.30 inference(scs_inference,[],[273,1015,1019,799,831,256,255,254,253,229])).
% 61.31/61.30 cnf(1071,plain,
% 61.31/61.30 (P7(x10711,a20,a20,a18,x10711,a20,a20,a18)+~P1(x10711,a20,a18)),
% 61.31/61.30 inference(scs_inference,[],[324,918,819,845,253,254,256,255,229])).
% 61.31/61.30 cnf(1107,plain,
% 61.31/61.30 (~P8(a16,a3,a1,a19,a19,a20,a19,a18)),
% 61.31/61.30 inference(scs_inference,[],[995,916,946,962,253,254,256,255])).
% 61.31/61.30 cnf(1119,plain,
% 61.31/61.30 (~P3(a1,a1,a19)+~E(a20,a1)),
% 61.31/61.30 inference(scs_inference,[],[571,157])).
% 61.31/61.30 cnf(1183,plain,
% 61.31/61.30 (~P8(a19,a18,a19,a1,a2,a17,a2,a18)),
% 61.31/61.30 inference(scs_inference,[],[767,255])).
% 61.31/61.30 cnf(1209,plain,
% 61.31/61.30 (~P4(a19,a1,x12091,a1)+~P4(a19,a18,x12091,a18)+~P5(a19,x12091,a18,a1)),
% 61.31/61.30 inference(scs_inference,[],[146,316,1003,1183,1107,256,255,253,254,196])).
% 61.31/61.30 cnf(1255,plain,
% 61.31/61.30 (~P3(a1,a19,a1)+~E(a20,a1)),
% 61.31/61.30 inference(scs_inference,[],[1119,155])).
% 61.31/61.30 cnf(1395,plain,
% 61.31/61.30 (~P3(x13951,a19,a1)+~E(x13951,a1)+~E(a20,a1)),
% 61.31/61.30 inference(scs_inference,[],[1255,99])).
% 61.31/61.30 cnf(1997,plain,
% 61.31/61.30 (P7(a3,a16,a19,a3,a3,a16,a19,a3)),
% 61.31/61.30 inference(scs_inference,[],[149,277,188,258])).
% 61.31/61.30 cnf(1999,plain,
% 61.31/61.30 (P7(a3,a19,a3,a16,a19,a3,a3,a16)),
% 61.31/61.30 inference(scs_inference,[],[149,277,188,258,259])).
% 61.31/61.30 cnf(2001,plain,
% 61.31/61.30 (P7(a19,a3,a19,a3,a3,a16,a3,a16)),
% 61.31/61.30 inference(scs_inference,[],[149,277,188,258,259,260])).
% 61.31/61.30 cnf(2003,plain,
% 61.31/61.30 (P1(a1,a18,a2)),
% 61.31/61.30 inference(scs_inference,[],[142,149,277,188,258,259,260,153])).
% 61.31/61.30 cnf(2005,plain,
% 61.31/61.30 (P4(a20,a1,a20,a18)),
% 61.31/61.30 inference(scs_inference,[],[142,149,145,277,188,258,259,260,153,157])).
% 61.31/61.30 cnf(2007,plain,
% 61.31/61.30 (P1(a2,a1,a18)),
% 61.31/61.30 inference(scs_inference,[],[142,149,145,277,188,258,259,260,153,157,152])).
% 61.31/61.30 cnf(2011,plain,
% 61.31/61.30 (P1(a20,a1,a18)),
% 61.31/61.30 inference(scs_inference,[],[142,273,149,145,277,188,258,259,260,153,157,152,226,154])).
% 61.31/61.30 cnf(2013,plain,
% 61.31/61.30 (P4(a20,a1,a18,a20)),
% 61.31/61.30 inference(scs_inference,[],[142,273,149,145,277,188,258,259,260,153,157,152,226,154,169])).
% 61.31/61.30 cnf(2015,plain,
% 61.31/61.30 (P8(a16,a16,x20151,x20152,a17,a17,x20151,x20152)),
% 61.31/61.30 inference(scs_inference,[],[142,273,149,145,277,188,258,259,260,153,157,152,226,154,169,253])).
% 61.31/61.30 cnf(2017,plain,
% 61.31/61.30 (P9(a3,a18,a16,a1)),
% 61.31/61.30 inference(scs_inference,[],[142,273,149,145,277,146,188,258,259,260,153,157,152,226,154,169,253,165])).
% 61.31/61.30 cnf(2019,plain,
% 61.31/61.30 (P10(a19,a20,a16,a3)),
% 61.31/61.30 inference(scs_inference,[],[142,273,149,145,148,277,146,188,258,259,260,153,157,152,226,154,169,253,165,167])).
% 61.31/61.30 cnf(2021,plain,
% 61.31/61.30 (P8(a17,a17,a16,a16,x20211,x20212,x20211,x20212)),
% 61.31/61.30 inference(scs_inference,[],[142,273,149,145,148,277,146,188,258,259,260,153,157,152,226,154,169,253,165,167,256])).
% 61.31/61.30 cnf(2025,plain,
% 61.31/61.30 (P3(a20,a18,a1)),
% 61.31/61.30 inference(scs_inference,[],[142,273,149,145,148,277,146,188,258,259,260,153,157,152,226,154,169,253,165,167,256,234,155])).
% 61.31/61.30 cnf(2027,plain,
% 61.31/61.30 (P9(a18,a18,a1,a1)),
% 61.31/61.30 inference(scs_inference,[],[142,273,320,149,145,148,277,146,188,258,259,260,153,157,152,226,154,169,253,165,167,256,234,155,164])).
% 61.31/61.30 cnf(2029,plain,
% 61.31/61.30 (P8(x20291,x20292,a17,a17,x20291,x20292,a16,a16)),
% 61.31/61.30 inference(scs_inference,[],[142,273,320,149,145,148,277,146,188,258,259,260,153,157,152,226,154,169,253,165,167,256,234,155,164,254])).
% 61.31/61.30 cnf(2031,plain,
% 61.31/61.30 (P10(a3,a16,a19,a20)),
% 61.31/61.30 inference(scs_inference,[],[142,273,320,149,145,148,277,146,188,258,259,260,153,157,152,226,154,169,253,165,167,256,234,155,164,254,166])).
% 61.31/61.30 cnf(2033,plain,
% 61.31/61.30 (P7(a20,a1,a1,a18,a20,a1,a1,a18)),
% 61.31/61.30 inference(scs_inference,[],[142,273,320,149,145,148,277,146,188,258,259,260,153,157,152,226,154,169,253,165,167,256,234,155,164,254,166,224])).
% 61.31/61.30 cnf(2035,plain,
% 61.31/61.30 (P3(f28(a1,a18,a1,a18,a20,a20),a1,a18)),
% 61.31/61.30 inference(scs_inference,[],[142,273,320,149,145,148,277,146,188,258,259,260,153,157,152,226,154,169,253,165,167,256,234,155,164,254,166,224,204])).
% 61.31/61.30 cnf(2037,plain,
% 61.31/61.30 (P10(f13(a17,a18,a2,a18,a1),a17,a18,a1)),
% 61.31/61.30 inference(scs_inference,[],[142,269,273,320,149,145,148,277,147,146,188,258,259,260,153,157,152,226,154,169,253,165,167,256,234,155,164,254,166,224,204,199])).
% 61.31/61.30 cnf(2041,plain,
% 61.31/61.30 (P9(f28(a1,a18,a1,a18,a20,a20),a20,a18,a18)),
% 61.31/61.30 inference(scs_inference,[],[142,269,273,320,149,145,148,277,147,146,188,258,259,260,153,157,152,226,154,169,253,165,167,256,234,155,164,254,166,224,204,199,205,206])).
% 61.31/61.30 cnf(2043,plain,
% 61.31/61.30 (P8(a17,a17,x20431,x20432,a17,a17,x20431,x20432)),
% 61.31/61.30 inference(scs_inference,[],[142,269,273,320,149,145,148,277,147,146,188,258,259,260,153,157,152,226,154,169,253,165,167,256,234,155,164,254,166,224,204,199,205,206,263])).
% 61.31/61.30 cnf(2045,plain,
% 61.31/61.30 (P1(f13(a17,a18,a2,a18,a1),a18,a1)),
% 61.31/61.30 inference(scs_inference,[],[142,269,273,320,149,145,148,277,147,146,188,258,259,260,153,157,152,226,154,169,253,165,167,256,234,155,164,254,166,224,204,199,205,206,263,198])).
% 61.31/61.30 cnf(2047,plain,
% 61.31/61.30 (P9(a16,a16,a16,a16)),
% 61.31/61.30 inference(scs_inference,[],[142,269,273,320,149,145,148,277,147,146,188,258,259,260,153,157,152,226,154,169,253,165,167,256,234,155,164,254,166,224,204,199,205,206,263,198,241])).
% 61.31/61.30 cnf(2051,plain,
% 61.31/61.30 (P9(a17,a17,a17,a17)),
% 61.31/61.30 inference(scs_inference,[],[142,269,273,320,149,145,148,277,147,146,188,258,259,260,153,157,152,226,154,169,253,165,167,256,234,155,164,254,166,224,204,199,205,206,263,198,241,159,180])).
% 61.31/61.30 cnf(2053,plain,
% 61.31/61.30 (P9(a19,a20,a19,a20)),
% 61.31/61.30 inference(scs_inference,[],[142,269,273,320,149,145,148,277,147,146,188,258,259,260,153,157,152,226,154,169,253,165,167,256,234,155,164,254,166,224,204,199,205,206,263,198,241,159,180,181])).
% 61.31/61.30 cnf(2055,plain,
% 61.31/61.30 (~P8(a19,a1,a19,a18,f8(a3,a2,a21,a17),a3,a3,a17)),
% 61.31/61.30 inference(scs_inference,[],[142,374,269,273,320,149,145,148,277,147,146,188,258,259,260,153,157,152,226,154,169,253,165,167,256,234,155,164,254,166,224,204,199,205,206,263,198,241,159,180,181,242])).
% 61.31/61.30 cnf(2057,plain,
% 61.31/61.30 (P2(a20,a1,a18,a18)),
% 61.31/61.30 inference(scs_inference,[],[142,374,269,273,320,149,145,148,277,147,146,188,258,259,260,153,157,152,226,154,169,253,165,167,256,234,155,164,254,166,224,204,199,205,206,263,198,241,159,180,181,242,185])).
% 61.31/61.30 cnf(2059,plain,
% 61.31/61.30 (P1(a2,a2,a1)),
% 61.31/61.30 inference(scs_inference,[],[142,374,269,273,320,149,145,148,277,147,146,188,258,259,260,153,157,152,226,154,169,253,165,167,256,234,155,164,254,166,224,204,199,205,206,263,198,241,159,180,181,242,185,156])).
% 61.31/61.30 cnf(2063,plain,
% 61.31/61.30 (P5(a1,a18,a18,a18)),
% 61.31/61.30 inference(scs_inference,[],[142,374,267,269,273,320,149,145,148,277,147,146,188,258,259,260,153,157,152,226,154,169,253,165,167,256,234,155,164,254,166,224,204,199,205,206,263,198,241,159,180,181,242,185,156,173,197])).
% 61.31/61.30 cnf(2065,plain,
% 61.31/61.30 (P5(a18,a1,a18,a18)),
% 61.31/61.30 inference(scs_inference,[],[142,374,267,269,273,320,149,145,148,277,147,146,188,258,259,260,153,157,152,226,154,169,253,165,167,256,234,155,164,254,166,224,204,199,205,206,263,198,241,159,180,181,242,185,156,173,197,170])).
% 61.31/61.30 cnf(2071,plain,
% 61.31/61.30 (P8(a20,a1,a1,a18,a1,a18,a20,a18)),
% 61.31/61.30 inference(scs_inference,[],[142,374,267,269,273,320,149,145,148,277,147,146,188,258,259,260,153,157,152,226,154,169,253,165,167,256,234,155,164,254,166,224,204,199,205,206,263,198,241,159,180,181,242,185,156,173,197,170,171,172,227])).
% 61.31/61.30 cnf(2073,plain,
% 61.31/61.30 (~P2(a20,a1,a19,a18)),
% 61.31/61.30 inference(scs_inference,[],[142,374,267,269,273,320,149,145,148,277,147,146,188,258,259,260,153,157,152,226,154,169,253,165,167,256,234,155,164,254,166,224,204,199,205,206,263,198,241,159,180,181,242,185,156,173,197,170,171,172,227,287])).
% 61.31/61.30 cnf(2075,plain,
% 61.31/61.30 (P9(a18,a18,a18,a18)),
% 61.31/61.30 inference(scs_inference,[],[142,374,267,269,273,320,149,145,148,277,147,146,188,258,259,260,153,157,152,226,154,169,253,165,167,256,234,155,164,254,166,224,204,199,205,206,263,198,241,159,180,181,242,185,156,173,197,170,171,172,227,287,608])).
% 61.31/61.30 cnf(2079,plain,
% 61.31/61.30 (P7(a19,a3,a3,a16,a3,a19,a3,a16)),
% 61.31/61.30 inference(scs_inference,[],[142,374,267,269,273,320,149,145,148,277,147,146,188,258,259,260,153,157,152,226,154,169,253,165,167,256,234,155,164,254,166,224,204,199,205,206,263,198,241,159,180,181,242,185,156,173,197,170,171,172,227,287,608,705,257])).
% 61.31/61.30 cnf(2081,plain,
% 61.31/61.30 (P4(a20,a18,a20,a1)),
% 61.31/61.30 inference(scs_inference,[],[142,374,267,269,273,320,149,145,148,277,147,146,188,258,259,260,153,157,152,226,154,169,253,165,167,256,234,155,164,254,166,224,204,199,205,206,263,198,241,159,180,181,242,185,156,173,197,170,171,172,227,287,608,705,257,168])).
% 61.31/61.30 cnf(2083,plain,
% 61.31/61.30 (P1(a16,a16,a16)),
% 61.31/61.30 inference(scs_inference,[],[142,374,267,269,273,320,149,145,148,277,147,146,188,258,259,260,153,157,152,226,154,169,253,165,167,256,234,155,164,254,166,224,204,199,205,206,263,198,241,159,180,181,242,185,156,173,197,170,171,172,227,287,608,705,257,168,161])).
% 61.31/61.30 cnf(2085,plain,
% 61.31/61.30 (P8(a18,a1,a18,a18,a18,a1,a18,a18)),
% 61.31/61.30 inference(scs_inference,[],[142,374,267,269,273,320,149,145,148,277,147,146,188,258,259,260,153,157,152,226,154,169,253,165,167,256,234,155,164,254,166,224,204,199,205,206,263,198,241,159,180,181,242,185,156,173,197,170,171,172,227,287,608,705,257,168,161,225])).
% 61.31/61.30 cnf(2087,plain,
% 61.31/61.30 (P8(a1,a20,a1,a18,a1,a18,a20,a18)),
% 61.31/61.30 inference(scs_inference,[],[142,374,267,269,273,320,149,145,148,277,147,146,188,258,259,260,153,157,152,226,154,169,253,165,167,256,234,155,164,254,166,224,204,199,205,206,263,198,241,159,180,181,242,185,156,173,197,170,171,172,227,287,608,705,257,168,161,225,255])).
% 61.31/61.30 cnf(2091,plain,
% 61.31/61.30 (P7(a18,a18,a18,a1,a18,a18,a18,a1)),
% 61.31/61.30 inference(scs_inference,[],[142,374,267,269,273,320,149,145,148,277,147,146,188,258,259,260,153,157,152,226,154,169,253,165,167,256,234,155,164,254,166,224,204,199,205,206,263,198,241,159,180,181,242,185,156,173,197,170,171,172,227,287,608,705,257,168,161,225,255,162,229])).
% 61.31/61.30 cnf(2097,plain,
% 61.31/61.30 (P4(a20,a1,a20,a1)),
% 61.31/61.30 inference(scs_inference,[],[142,374,267,269,273,320,149,145,148,277,147,146,188,258,259,260,153,157,152,226,154,169,253,165,167,256,234,155,164,254,166,224,204,199,205,206,263,198,241,159,180,181,242,185,156,173,197,170,171,172,227,287,608,705,257,168,161,225,255,162,229,207,208,184])).
% 61.31/61.30 cnf(2099,plain,
% 61.31/61.30 (P5(a18,a18,a18,a18)),
% 61.31/61.30 inference(scs_inference,[],[142,374,267,269,273,320,149,145,148,277,147,146,188,258,259,260,153,157,152,226,154,169,253,165,167,256,234,155,164,254,166,224,204,199,205,206,263,198,241,159,180,181,242,185,156,173,197,170,171,172,227,287,608,705,257,168,161,225,255,162,229,207,208,184,186])).
% 61.31/61.30 cnf(2105,plain,
% 61.31/61.30 (P7(a3,a16,a3,a16,a19,a3,a19,a3)),
% 61.31/61.30 inference(scs_inference,[],[1997,2057,188,260])).
% 61.31/61.30 cnf(2107,plain,
% 61.31/61.30 (P4(f28(a1,a18,a1,a18,a20,a20),a1,f28(a1,a18,a1,a18,a20,a20),a18)),
% 61.31/61.30 inference(scs_inference,[],[1997,2057,2035,188,260,157])).
% 61.31/61.30 cnf(2109,plain,
% 61.31/61.30 (P7(a16,a3,a19,a3,a3,a16,a19,a3)),
% 61.31/61.30 inference(scs_inference,[],[1997,2057,2035,188,260,157,259])).
% 61.31/61.30 cnf(2111,plain,
% 61.31/61.30 (P7(a3,a16,a19,a3,a16,a3,a19,a3)),
% 61.31/61.30 inference(scs_inference,[],[1997,2057,2035,188,260,157,259,257])).
% 61.31/61.30 cnf(2113,plain,
% 61.31/61.30 (P7(a3,a16,a3,a19,a3,a16,a19,a3)),
% 61.31/61.30 inference(scs_inference,[],[1997,1999,2057,2035,188,260,157,259,257,258])).
% 61.31/61.30 cnf(2115,plain,
% 61.31/61.30 (P8(a16,a16,x21151,x21152,a16,a16,x21151,x21152)),
% 61.31/61.30 inference(scs_inference,[],[2047,1997,1999,2057,2035,188,260,157,259,257,258,226])).
% 61.31/61.30 cnf(2117,plain,
% 61.31/61.30 (P8(a20,a18,a18,a1,a18,a1,a20,a1)),
% 61.31/61.30 inference(scs_inference,[],[2047,1997,1999,2057,2081,2035,188,260,157,259,257,258,226,227])).
% 61.31/61.30 cnf(2119,plain,
% 61.31/61.30 (P4(a18,a20,a20,a1)),
% 61.31/61.30 inference(scs_inference,[],[2047,1997,1999,2013,2057,2081,2035,188,260,157,259,257,258,226,227,168])).
% 61.31/61.30 cnf(2121,plain,
% 61.31/61.30 (P1(a2,a18,a1)),
% 61.31/61.30 inference(scs_inference,[],[2047,1997,1999,2007,2013,2057,2081,2035,188,260,157,259,257,258,226,227,168,153])).
% 61.31/61.30 cnf(2123,plain,
% 61.31/61.30 (P1(a20,a18,a1)),
% 61.31/61.30 inference(scs_inference,[],[2047,1997,1999,2007,2013,2025,2057,2081,2035,188,260,157,259,257,258,226,227,168,153,154])).
% 61.31/61.30 cnf(2125,plain,
% 61.31/61.30 (P4(a20,a18,a1,a20)),
% 61.31/61.30 inference(scs_inference,[],[2047,1997,1999,2007,2013,2025,2057,2081,2035,188,260,157,259,257,258,226,227,168,153,154,169])).
% 61.31/61.30 cnf(2127,plain,
% 61.31/61.30 (P1(a17,a17,a17)),
% 61.31/61.30 inference(scs_inference,[],[2047,1997,1999,2007,2013,2025,2051,2057,2081,2035,188,260,157,259,257,258,226,227,168,153,154,169,161])).
% 61.31/61.30 cnf(2131,plain,
% 61.31/61.30 (P1(a18,a1,a2)),
% 61.31/61.30 inference(scs_inference,[],[2047,2003,1997,1999,2007,2013,2025,2051,2057,2065,2081,2035,188,260,157,259,257,258,226,227,168,153,154,169,161,225,152])).
% 61.31/61.30 cnf(2133,plain,
% 61.31/61.30 (P10(a3,a16,a20,a19)),
% 61.31/61.30 inference(scs_inference,[],[2047,2003,1997,1999,2007,2013,2025,2031,2051,2057,2065,2081,2035,188,260,157,259,257,258,226,227,168,153,154,169,161,225,152,167])).
% 61.31/61.30 cnf(2135,plain,
% 61.31/61.30 (P8(x21351,x21352,x21351,x21352,a17,a17,a16,a16)),
% 61.31/61.30 inference(scs_inference,[],[2047,2003,1997,1999,2021,2007,2013,2025,2031,2051,2057,2065,2081,2035,188,260,157,259,257,258,226,227,168,153,154,169,161,225,152,167,253])).
% 61.31/61.30 cnf(2139,plain,
% 61.31/61.30 (P8(a16,a16,a17,a17,x21391,x21392,x21391,x21392)),
% 61.31/61.30 inference(scs_inference,[],[2047,2003,1997,1999,2015,2021,2007,2013,2025,2031,2051,2053,2057,2065,2081,2035,188,260,157,259,257,258,226,227,168,153,154,169,161,225,152,167,253,165,256])).
% 61.31/61.30 cnf(2145,plain,
% 61.31/61.30 (P3(f28(a1,a18,a1,a18,a20,a20),a18,a1)),
% 61.31/61.30 inference(scs_inference,[],[2047,2003,1997,1999,2015,2021,2007,2013,2017,2025,2031,2051,2053,2057,2065,2081,2085,2035,188,260,157,259,257,258,226,227,168,153,154,169,161,225,152,167,253,165,256,234,164,155])).
% 61.31/61.30 cnf(2147,plain,
% 61.31/61.30 (P8(x21471,x21472,a17,a17,x21472,x21471,a16,a16)),
% 61.31/61.30 inference(scs_inference,[],[2047,2003,1997,1999,2015,2021,2029,2007,2013,2017,2025,2031,2051,2053,2057,2065,2081,2085,2035,188,260,157,259,257,258,226,227,168,153,154,169,161,225,152,167,253,165,256,234,164,155,255])).
% 61.31/61.30 cnf(2149,plain,
% 61.31/61.30 (P8(x21491,x21492,a16,a16,x21491,x21492,a17,a17)),
% 61.31/61.30 inference(scs_inference,[],[2047,2003,1997,1999,2015,2021,2029,2007,2013,2017,2025,2031,2051,2053,2057,2065,2081,2085,2035,188,260,157,259,257,258,226,227,168,153,154,169,161,225,152,167,253,165,256,234,164,155,255,254])).
% 61.31/61.30 cnf(2151,plain,
% 61.31/61.30 (P10(a16,a3,a19,a20)),
% 61.31/61.30 inference(scs_inference,[],[2047,2003,1997,1999,2015,2021,2029,2007,2013,2017,2019,2025,2031,2051,2053,2057,2065,2081,2085,2035,188,260,157,259,257,258,226,227,168,153,154,169,161,225,152,167,253,165,256,234,164,155,255,254,166])).
% 61.31/61.30 cnf(2153,plain,
% 61.31/61.30 (P7(a3,a19,a3,a16,a3,a19,a3,a16)),
% 61.31/61.30 inference(scs_inference,[],[2047,2003,1997,1999,2015,2021,2029,2007,2013,2017,2019,2025,2031,2051,2053,2057,2065,2079,2081,2085,2035,188,260,157,259,257,258,226,227,168,153,154,169,161,225,152,167,253,165,256,234,164,155,255,254,166,264])).
% 61.31/61.30 cnf(2155,plain,
% 61.31/61.30 (P3(f28(a18,a1,a18,a1,a20,a20),a18,a1)),
% 61.31/61.30 inference(scs_inference,[],[2047,2003,1997,1999,2015,2021,2029,2007,2013,2017,2019,2025,2031,2051,2053,2057,2065,2079,2081,2085,2035,188,260,157,259,257,258,226,227,168,153,154,169,161,225,152,167,253,165,256,234,164,155,255,254,166,264,204])).
% 61.31/61.30 cnf(2157,plain,
% 61.31/61.30 (P9(x21571,x21572,x21571,x21572)),
% 61.31/61.30 inference(scs_inference,[],[2047,2003,1997,1999,2015,2021,2029,2007,2013,2017,2019,2025,2031,2051,2053,2057,2065,2079,2081,2085,2035,273,188,260,157,259,257,258,226,227,168,153,154,169,161,225,152,167,253,165,256,234,164,155,255,254,166,264,204,241])).
% 61.31/61.30 cnf(2162,plain,
% 61.31/61.30 (P7(a20,a18,a18,a1,a20,a18,a18,a1)),
% 61.31/61.30 inference(scs_inference,[],[2047,2003,1997,1999,2015,2021,2029,2007,2013,2017,2019,2025,2031,2051,2053,2057,2065,2073,2079,2081,2085,2035,273,188,260,157,259,257,258,226,227,168,153,154,169,161,225,152,167,253,165,256,234,164,155,255,254,166,264,204,241,126,205,224])).
% 61.31/61.30 cnf(2164,plain,
% 61.31/61.30 (P5(a17,a17,a17,a17)),
% 61.31/61.30 inference(scs_inference,[],[2047,2003,1997,1999,2015,2021,2029,2043,2007,2013,2017,2019,2025,2031,2051,2053,2057,2065,2073,2079,2081,2085,2035,273,188,260,157,259,257,258,226,227,168,153,154,169,161,225,152,167,253,165,256,234,164,155,255,254,166,264,204,241,126,205,224,237])).
% 61.31/61.30 cnf(2165,plain,
% 61.31/61.30 (P8(a17,a17,x21651,x21652,a17,a17,x21651,x21652)),
% 61.31/61.30 inference(rename_variables,[],[2043])).
% 61.31/61.30 cnf(2169,plain,
% 61.31/61.30 (P2(a20,a18,a1,a1)),
% 61.31/61.30 inference(scs_inference,[],[2047,2003,1997,1999,2015,2021,2029,2043,2007,2013,2017,2019,2025,2031,2051,2053,2057,2065,2073,2079,2081,2085,2035,273,188,260,157,259,257,258,226,227,168,153,154,169,161,225,152,167,253,165,256,234,164,155,255,254,166,264,204,241,126,205,224,237,206,185])).
% 61.31/61.30 cnf(2171,plain,
% 61.31/61.30 (P10(a20,a20,a1,a1)),
% 61.31/61.30 inference(scs_inference,[],[2047,2003,1997,1999,2015,2021,2029,2043,2007,2013,2017,2019,2025,2031,2051,2053,2057,2065,2073,2079,2081,2085,2097,2035,273,188,260,157,259,257,258,226,227,168,153,154,169,161,225,152,167,253,165,256,234,164,155,255,254,166,264,204,241,126,205,224,237,206,185,182])).
% 61.31/61.30 cnf(2173,plain,
% 61.31/61.30 (P10(a1,a18,a18,a18)),
% 61.31/61.30 inference(scs_inference,[],[2047,2003,1997,1999,2015,2021,2029,2043,2007,2011,2013,2017,2019,2025,2031,2051,2053,2057,2065,2073,2079,2081,2085,2097,2035,273,188,260,157,259,257,258,226,227,168,153,154,169,161,225,152,167,253,165,256,234,164,155,255,254,166,264,204,241,126,205,224,237,206,185,182,173])).
% 61.31/61.30 cnf(2177,plain,
% 61.31/61.30 (P7(a2,a1,a1,a18,a2,a1,a1,a18)),
% 61.31/61.30 inference(scs_inference,[],[2047,2003,1997,1999,2015,2021,2029,2043,2007,2011,2013,2017,2019,2025,2031,2051,2053,2057,2065,2073,2079,2081,2085,2097,2035,320,273,188,260,157,259,257,258,226,227,168,153,154,169,161,225,152,167,253,165,256,234,164,155,255,254,166,264,204,241,126,205,224,237,206,185,182,173,197,229])).
% 61.31/61.30 cnf(2179,plain,
% 61.31/61.30 (P4(a17,a17,a17,a17)),
% 61.31/61.30 inference(scs_inference,[],[2047,2003,1997,1999,2015,2021,2029,2043,2165,2007,2011,2013,2017,2019,2025,2031,2051,2053,2057,2065,2073,2079,2081,2085,2097,2035,320,273,188,260,157,259,257,258,226,227,168,153,154,169,161,225,152,167,253,165,256,234,164,155,255,254,166,264,204,241,126,205,224,237,206,185,182,173,197,229,252])).
% 61.31/61.30 cnf(2180,plain,
% 61.31/61.30 (P8(a17,a17,x21801,x21802,a17,a17,x21801,x21802)),
% 61.31/61.30 inference(rename_variables,[],[2043])).
% 61.31/61.30 cnf(2189,plain,
% 61.31/61.30 (P4(a1,a20,a18,a20)),
% 61.31/61.30 inference(scs_inference,[],[2047,2003,1997,1999,2015,2021,2029,2043,2165,2007,2011,2013,2017,2019,2025,2031,2051,2053,2057,2065,2073,2079,2081,2085,2097,2035,320,273,188,260,157,259,257,258,226,227,168,153,154,169,161,225,152,167,253,165,256,234,164,155,255,254,166,264,204,241,126,205,224,237,206,185,182,173,197,229,252,208,207,2,490,689])).
% 61.31/61.30 cnf(2195,plain,
% 61.31/61.30 (P5(a1,a1,a18,a1)),
% 61.31/61.30 inference(scs_inference,[],[2047,2003,1997,1999,2015,2021,2029,2043,2165,2007,2011,2013,2017,2019,2025,2031,2051,2053,2057,2065,2073,2079,2081,2085,2097,2035,320,273,188,260,157,259,257,258,226,227,168,153,154,169,161,225,152,167,253,165,256,234,164,155,255,254,166,264,204,241,126,205,224,237,206,185,182,173,197,229,252,208,207,2,490,689,170,705,171])).
% 61.31/61.30 cnf(2199,plain,
% 61.31/61.30 (P2(f9(a1,a18,a18),a1,a18,a18)),
% 61.31/61.30 inference(scs_inference,[],[2047,2003,1997,1999,2015,2021,2029,2043,2165,2007,2011,2013,2017,2019,2025,2031,2051,2053,2057,2063,2065,2073,2079,2081,2085,2097,2035,320,273,147,188,260,157,259,257,258,226,227,168,153,154,169,161,225,152,167,253,165,256,234,164,155,255,254,166,264,204,241,126,205,224,237,206,185,182,173,197,229,252,208,207,2,490,689,170,705,171,177,192])).
% 61.31/61.30 cnf(2208,plain,
% 61.31/61.30 (P8(a17,a17,x22081,x22082,a17,a17,x22081,x22082)),
% 61.31/61.30 inference(rename_variables,[],[2043])).
% 61.31/61.30 cnf(2217,plain,
% 61.31/61.30 (P10(a17,a17,a17,a17)),
% 61.31/61.30 inference(scs_inference,[],[2047,2003,1997,1999,2015,2021,2029,2043,2165,2180,2208,2007,2011,2013,2017,2019,2025,2031,2051,2053,2057,2063,2065,2073,2075,2079,2081,2085,2097,2099,2035,269,320,273,147,188,260,157,259,257,258,226,227,168,153,154,169,161,225,152,167,253,165,256,234,164,155,255,254,166,264,204,241,126,205,224,237,206,185,182,173,197,229,252,208,207,2,490,689,170,705,171,177,192,194,195,231,246,250,199,198,196])).
% 61.31/61.30 cnf(2219,plain,
% 61.31/61.30 (P5(a1,a1,a1,a18)),
% 61.31/61.30 inference(scs_inference,[],[2047,2003,1997,1999,2015,2021,2029,2043,2165,2180,2208,2007,2011,2013,2017,2019,2025,2031,2051,2053,2057,2063,2065,2073,2075,2079,2081,2085,2097,2099,2035,269,320,273,147,188,260,157,259,257,258,226,227,168,153,154,169,161,225,152,167,253,165,256,234,164,155,255,254,166,264,204,241,126,205,224,237,206,185,182,173,197,229,252,208,207,2,490,689,170,705,171,177,192,194,195,231,246,250,199,198,196,172])).
% 61.31/61.30 cnf(2225,plain,
% 61.31/61.30 (P7(a3,a19,a19,a3,a3,a16,a3,a16)),
% 61.31/61.30 inference(scs_inference,[],[2001,2169,188,259])).
% 61.31/61.30 cnf(2227,plain,
% 61.31/61.30 (P7(a1,a18,a20,a1,a1,a18,a20,a1)),
% 61.31/61.30 inference(scs_inference,[],[2001,2033,2169,188,259,258])).
% 61.31/61.30 cnf(2233,plain,
% 61.31/61.30 (P1(x22331,x22332,x22332)),
% 61.31/61.30 inference(scs_inference,[],[2157,2001,2033,2169,2145,188,259,258,157,260,161])).
% 61.31/61.30 cnf(2239,plain,
% 61.31/61.30 (P4(a1,a20,a20,a18)),
% 61.31/61.30 inference(scs_inference,[],[2157,2001,2033,2059,2125,2169,2107,2145,188,259,258,157,260,161,153,227,168])).
% 61.31/61.30 cnf(2241,plain,
% 61.31/61.30 (P4(a18,a20,a1,a20)),
% 61.31/61.30 inference(scs_inference,[],[2157,2001,2033,2059,2119,2125,2169,2107,2145,188,259,258,157,260,161,153,227,168,169])).
% 61.31/61.30 cnf(2245,plain,
% 61.31/61.30 (P8(x22451,x22452,x22453,x22454,x22451,x22452,x22453,x22454)),
% 61.31/61.30 inference(scs_inference,[],[2157,2001,2033,2059,2113,2119,2125,2169,2107,2145,188,259,258,157,260,161,153,227,168,169,257,226])).
% 61.31/61.30 cnf(2253,plain,
% 61.31/61.30 (P10(a16,a3,a20,a19)),
% 61.31/61.30 inference(scs_inference,[],[2157,2001,2033,2071,2151,2059,2113,2119,2125,2169,2195,2107,2145,188,259,258,157,260,161,153,227,168,169,257,226,154,225,253,167])).
% 61.31/61.30 cnf(2257,plain,
% 61.31/61.30 (P9(x22571,x22572,x22572,x22571)),
% 61.31/61.30 inference(scs_inference,[],[2157,2001,2033,2071,2151,2059,2113,2119,2121,2125,2169,2195,2107,2145,188,259,258,157,260,161,153,227,168,169,257,226,154,225,253,167,152,165])).
% 61.31/61.30 cnf(2259,plain,
% 61.31/61.30 (P9(a18,a18,f28(a1,a18,a1,a18,a20,a20),a20)),
% 61.31/61.30 inference(scs_inference,[],[2157,2001,2033,2071,2151,2059,2113,2119,2121,2125,2169,2195,2041,2107,2145,188,259,258,157,260,161,153,227,168,169,257,226,154,225,253,167,152,165,164])).
% 61.31/61.30 cnf(2261,plain,
% 61.31/61.30 (P3(f28(a18,a1,a18,a1,a20,a20),a1,a18)),
% 61.31/61.30 inference(scs_inference,[],[2157,2001,2033,2071,2151,2059,2113,2119,2121,2125,2169,2195,2041,2107,2145,2155,188,259,258,157,260,161,153,227,168,169,257,226,154,225,253,167,152,165,164,155])).
% 61.31/61.30 cnf(2265,plain,
% 61.31/61.30 (P8(x22651,x22652,x22652,x22651,a17,a17,a16,a16)),
% 61.31/61.30 inference(scs_inference,[],[2157,2001,2033,2071,2151,2115,2135,2059,2113,2119,2121,2125,2169,2195,2041,2107,2145,2155,188,259,258,157,260,161,153,227,168,169,257,226,154,225,253,167,152,165,164,155,256,255])).
% 61.31/61.30 cnf(2267,plain,
% 61.31/61.30 (P8(a1,a18,a20,a1,a20,a18,a1,a18)),
% 61.31/61.30 inference(scs_inference,[],[2157,2001,2033,2071,2151,2115,2135,2059,2113,2119,2121,2125,2169,2195,2041,2107,2145,2155,188,259,258,157,260,161,153,227,168,169,257,226,154,225,253,167,152,165,164,155,256,255,254])).
% 61.31/61.30 cnf(2269,plain,
% 61.31/61.30 (P10(a20,a19,a3,a16)),
% 61.31/61.30 inference(scs_inference,[],[2157,2001,2033,2071,2133,2151,2115,2135,2059,2113,2119,2121,2125,2169,2195,2041,2107,2145,2155,188,259,258,157,260,161,153,227,168,169,257,226,154,225,253,167,152,165,164,155,256,255,254,166])).
% 61.31/61.30 cnf(2271,plain,
% 61.31/61.30 (P4(a17,a17,a17,f4(a17,a17,a17))),
% 61.31/61.30 inference(scs_inference,[],[2157,2001,2033,2071,2133,2151,2115,2135,2059,2113,2119,2121,2125,2169,2179,2195,2217,2041,2107,2145,2155,188,259,258,157,260,161,153,227,168,169,257,226,154,225,253,167,152,165,164,155,256,255,254,166,189])).
% 61.31/61.30 cnf(2275,plain,
% 61.31/61.30 (P4(a17,a17,a17,f30(a17,a17,a17,a17,a17))),
% 61.31/61.30 inference(scs_inference,[],[2157,2001,2033,2071,2133,2151,2115,2135,2059,2113,2119,2121,2125,2169,2179,2195,2217,2041,2107,2145,2155,188,259,258,157,260,161,153,227,168,169,257,226,154,225,253,167,152,165,164,155,256,255,254,166,189,191,200])).
% 61.31/61.30 cnf(2280,plain,
% 61.31/61.30 (P8(a17,a17,x22801,x22802,a17,a17,x22801,x22802)),
% 61.31/61.30 inference(rename_variables,[],[2043])).
% 61.31/61.30 cnf(2282,plain,
% 61.31/61.30 (P1(f15(a18,a18,a1,a18),a1,a18)),
% 61.31/61.30 inference(scs_inference,[],[2157,2001,2033,2071,2133,2151,2115,2135,2059,2113,2119,2121,2125,2169,2173,2179,2195,2217,2041,2107,2145,2155,2043,188,259,258,157,260,161,153,227,168,169,257,226,154,225,253,167,152,165,164,155,256,255,254,166,189,191,200,202,247,248])).
% 61.31/61.30 cnf(2290,plain,
% 61.31/61.30 (P3(f28(a3,a16,a3,a16,a17,a17),a3,a16)),
% 61.31/61.30 inference(scs_inference,[],[2157,2001,2033,2071,2133,2151,2115,2135,2059,2113,2119,2121,2125,2127,2164,2169,2173,2179,2195,2217,2041,2107,2145,2155,2043,144,188,259,258,157,260,161,153,227,168,169,257,226,154,225,253,167,152,165,164,155,256,255,254,166,189,191,200,202,247,248,177,199,192,204])).
% 61.31/61.30 cnf(2292,plain,
% 61.31/61.30 (P9(a3,a3,a17,a17)),
% 61.31/61.30 inference(scs_inference,[],[2157,2001,2033,2071,2133,2151,2115,2135,2147,2059,2113,2119,2121,2125,2127,2164,2169,2173,2179,2195,2217,2041,2107,2145,2155,2043,271,144,188,259,258,157,260,161,153,227,168,169,257,226,154,225,253,167,152,165,164,155,256,255,254,166,189,191,200,202,247,248,177,199,192,204,241])).
% 61.31/61.30 cnf(2303,plain,
% 61.31/61.30 (P5(a16,a16,a16,a16)),
% 61.31/61.30 inference(scs_inference,[],[2157,2001,2033,2071,2133,2151,2083,2115,2135,2147,2059,2113,2119,2121,2125,2127,2131,2164,2169,2173,2179,2195,2217,2041,2107,2145,2155,2043,271,144,188,259,258,157,260,161,153,227,168,169,257,226,154,225,253,167,152,165,164,155,256,255,254,166,189,191,200,202,247,248,177,199,192,204,241,198,224,194,190,237])).
% 61.31/61.30 cnf(2308,plain,
% 61.31/61.30 (P9(f28(a3,a16,a3,a16,a17,a17),a17,a16,a16)),
% 61.31/61.30 inference(scs_inference,[],[2157,2001,2033,2071,2133,2151,2083,2115,2135,2147,2059,2113,2119,2121,2125,2127,2131,2164,2169,2173,2179,2195,2217,2041,2107,2145,2155,2043,271,144,188,259,258,157,260,161,153,227,168,169,257,226,154,225,253,167,152,165,164,155,256,255,254,166,189,191,200,202,247,248,177,199,192,204,241,198,224,194,190,237,205,206])).
% 61.31/61.30 cnf(2310,plain,
% 61.31/61.30 (P10(a18,a1,a18,a18)),
% 61.31/61.30 inference(scs_inference,[],[2157,2001,2033,2071,2133,2151,2083,2115,2135,2147,2059,2113,2119,2121,2125,2127,2131,2164,2169,2173,2179,2195,2217,2041,2107,2145,2155,2043,271,144,188,259,258,157,260,161,153,227,168,169,257,226,154,225,253,167,152,165,164,155,256,255,254,166,189,191,200,202,247,248,177,199,192,204,241,198,224,194,190,237,205,206,183])).
% 61.31/61.30 cnf(2315,plain,
% 61.31/61.30 (P10(f9(a17,a17,a17),a17,a17,a17)),
% 61.31/61.30 inference(scs_inference,[],[2157,2001,2033,2071,2133,2151,2083,2115,2135,2139,2147,2059,2113,2119,2121,2125,2127,2131,2164,2169,2173,2179,2195,2217,2041,2107,2145,2155,2043,2280,271,144,188,259,258,157,260,161,153,227,168,169,257,226,154,225,253,167,152,165,164,155,256,255,254,166,189,191,200,202,247,248,177,199,192,204,241,198,224,194,190,237,205,206,183,242,243])).
% 61.31/61.30 cnf(2316,plain,
% 61.31/61.30 (P8(a17,a17,x23161,x23162,a17,a17,x23161,x23162)),
% 61.31/61.30 inference(rename_variables,[],[2043])).
% 61.31/61.30 cnf(2320,plain,
% 61.31/61.30 (P2(a17,a17,a17,a17)),
% 61.31/61.30 inference(scs_inference,[],[2157,2001,2033,2071,2133,2151,2083,2115,2135,2139,2147,2059,2113,2119,2121,2125,2127,2131,2164,2169,2173,2179,2195,2217,2041,2107,2145,2155,2043,2280,2035,271,144,188,259,258,157,260,161,153,227,168,169,257,226,154,225,253,167,152,165,164,155,256,255,254,166,189,191,200,202,247,248,177,199,192,204,241,198,224,194,190,237,205,206,183,242,243,175,185])).
% 61.31/61.30 cnf(2322,plain,
% 61.31/61.30 (P10(a1,a18,a20,a20)),
% 61.31/61.30 inference(scs_inference,[],[2157,2001,2033,2071,2133,2151,2083,2115,2135,2139,2147,2059,2113,2119,2121,2125,2127,2131,2164,2169,2173,2179,2189,2195,2217,2041,2107,2145,2155,2043,2280,2035,271,144,188,259,258,157,260,161,153,227,168,169,257,226,154,225,253,167,152,165,164,155,256,255,254,166,189,191,200,202,247,248,177,199,192,204,241,198,224,194,190,237,205,206,183,242,243,175,185,182])).
% 61.31/61.30 cnf(2326,plain,
% 61.31/61.30 (P3(a17,a17,a17)),
% 61.31/61.30 inference(scs_inference,[],[2157,2001,2033,2071,2133,2151,2083,2115,2135,2139,2147,2059,2113,2119,2121,2125,2127,2131,2164,2169,2173,2179,2189,2195,2217,2041,2107,2145,2155,2043,2280,2316,2035,271,144,316,188,259,258,157,260,161,153,227,168,169,257,226,154,225,253,167,152,165,164,155,256,255,254,166,189,191,200,202,247,248,177,199,192,204,241,198,224,194,190,237,205,206,183,242,243,175,185,182,173,240])).
% 61.31/61.30 cnf(2331,plain,
% 61.31/61.30 (P3(f25(a17,x23311),a17,x23311)),
% 61.31/61.30 inference(scs_inference,[],[2157,2001,2033,2071,2133,2151,2083,2115,2135,2139,2147,2059,2113,2119,2121,2125,2127,2131,2164,2169,2173,2179,2189,2195,2217,2041,2107,2145,2155,2043,2280,2316,2035,271,144,316,188,259,258,157,260,161,153,227,168,169,257,226,154,225,253,167,152,165,164,155,256,255,254,166,189,191,200,202,247,248,177,199,192,204,241,198,224,194,190,237,205,206,183,242,243,175,185,182,173,240,187,160])).
% 61.31/61.30 cnf(2333,plain,
% 61.31/61.30 (P4(a1,a1,a1,a1)),
% 61.31/61.30 inference(scs_inference,[],[2157,2001,2033,2071,2133,2151,2083,2115,2135,2139,2147,2059,2113,2119,2121,2125,2127,2131,2164,2169,2173,2179,2189,2195,2217,2041,2107,2145,2155,2043,2280,2316,2035,271,144,316,188,259,258,157,260,161,153,227,168,169,257,226,154,225,253,167,152,165,164,155,256,255,254,166,189,191,200,202,247,248,177,199,192,204,241,198,224,194,190,237,205,206,183,242,243,175,185,182,173,240,187,160,252])).
% 61.31/61.30 cnf(2337,plain,
% 61.31/61.30 (P10(a3,a3,a17,a17)),
% 61.31/61.30 inference(scs_inference,[],[2157,2001,2033,2071,2133,2151,2083,2115,2135,2139,2147,2059,2113,2119,2121,2125,2127,2131,2164,2169,2173,2179,2189,2195,2217,2041,2107,2145,2155,2043,2280,2316,2011,2035,271,320,144,316,188,259,258,157,260,161,153,227,168,169,257,226,154,225,253,167,152,165,164,155,256,255,254,166,189,191,200,202,247,248,177,199,192,204,241,198,224,194,190,237,205,206,183,242,243,175,185,182,173,240,187,160,252,207,877])).
% 61.31/61.30 cnf(2339,plain,
% 61.31/61.30 (P9(f30(a17,a17,a17,a17,a17),a17,a16,a16)),
% 61.31/61.30 inference(scs_inference,[],[2157,2001,2033,2071,2133,2151,2083,2115,2135,2139,2147,2059,2113,2119,2121,2125,2127,2131,2164,2169,2173,2179,2189,2195,2217,2041,2107,2145,2155,2043,2280,2316,2011,2035,271,320,144,316,188,259,258,157,260,161,153,227,168,169,257,226,154,225,253,167,152,165,164,155,256,255,254,166,189,191,200,202,247,248,177,199,192,204,241,198,224,194,190,237,205,206,183,242,243,175,185,182,173,240,187,160,252,207,877,670])).
% 61.31/61.30 cnf(2349,plain,
% 61.31/61.30 (P1(f14(a18,a1,a1,a18,a2,a2),a1,a18)),
% 61.31/61.30 inference(scs_inference,[],[2157,2001,2033,2071,2133,2151,2083,2115,2135,2139,2147,2059,2113,2119,2121,2125,2127,2131,2164,2169,2173,2179,2189,2195,2217,2041,2107,2145,2155,2043,2280,2316,2011,2035,2007,271,320,144,316,188,259,258,157,260,161,153,227,168,169,257,226,154,225,253,167,152,165,164,155,256,255,254,166,189,191,200,202,247,248,177,199,192,204,241,198,224,194,190,237,205,206,183,242,243,175,185,182,173,240,187,160,252,207,877,670,287,178,174,228,208])).
% 61.31/61.30 cnf(2352,plain,
% 61.31/61.30 (P10(f8(a17,a17,a17,a17),a17,a17,a17)),
% 61.31/61.30 inference(scs_inference,[],[2320,188])).
% 61.31/61.30 cnf(2354,plain,
% 61.31/61.30 (P9(a18,a3,a1,a16)),
% 61.31/61.30 inference(scs_inference,[],[2257,2320,188,490])).
% 61.31/61.30 cnf(2355,plain,
% 61.31/61.30 (P9(x23551,x23552,x23552,x23551)),
% 61.31/61.30 inference(rename_variables,[],[2257])).
% 61.31/61.30 cnf(2361,plain,
% 61.31/61.30 (P7(a19,a3,a16,a3,a19,a3,a3,a16)),
% 61.31/61.30 inference(scs_inference,[],[2257,2109,2320,2331,2349,188,490,287,157,258])).
% 61.31/61.30 cnf(2363,plain,
% 61.31/61.30 (P7(a16,a3,a3,a16,a19,a3,a19,a3)),
% 61.31/61.30 inference(scs_inference,[],[2257,2105,2109,2320,2331,2349,188,490,287,157,258,259])).
% 61.31/61.30 cnf(2373,plain,
% 61.31/61.30 (P7(a3,a16,a16,a3,a19,a3,a19,a3)),
% 61.31/61.30 inference(scs_inference,[],[2257,2105,2109,2111,2320,2275,2331,2349,188,490,287,157,258,259,227,168,154,169,260])).
% 61.31/61.30 cnf(2375,plain,
% 61.31/61.30 (P1(x23751,x23752,x23751)),
% 61.31/61.30 inference(scs_inference,[],[2257,2233,2105,2109,2111,2320,2275,2331,2349,188,490,287,157,258,259,227,168,154,169,260,152])).
% 61.31/61.30 cnf(2379,plain,
% 61.31/61.30 (P1(f13(a17,a18,a2,a18,a1),a1,a18)),
% 61.31/61.30 inference(scs_inference,[],[2257,2233,2105,2109,2111,2269,2320,2275,2045,2331,2349,188,490,287,157,258,259,227,168,154,169,260,152,167,153])).
% 61.31/61.30 cnf(2381,plain,
% 61.31/61.30 (P8(x23811,x23812,x23813,x23814,x23812,x23811,x23813,x23814)),
% 61.31/61.30 inference(scs_inference,[],[2257,2355,2233,2105,2109,2111,2269,2320,2275,2045,2331,2349,188,490,287,157,258,259,227,168,154,169,260,152,167,153,226])).
% 61.31/61.30 cnf(2389,plain,
% 61.31/61.30 (P8(x23891,x23892,x23891,x23892,x23893,x23894,x23893,x23894)),
% 61.31/61.30 inference(scs_inference,[],[2245,2257,2355,2233,2105,2087,2109,2111,2225,2269,2320,2275,2045,2331,2349,2219,188,490,287,157,258,259,227,168,154,169,260,152,167,153,226,257,225,253,256])).
% 61.31/61.30 cnf(2391,plain,
% 61.31/61.30 (P9(a17,a17,a17,f30(a17,a17,a17,a17,a17))),
% 61.31/61.30 inference(scs_inference,[],[2245,2257,2355,2233,2105,2087,2109,2111,2225,2269,2320,2275,2045,2331,2349,2219,188,490,287,157,258,259,227,168,154,169,260,152,167,153,226,257,225,253,256,234])).
% 61.31/61.30 cnf(2395,plain,
% 61.31/61.30 (P3(f25(a17,x23951),x23951,a17)),
% 61.31/61.30 inference(scs_inference,[],[2245,2257,2355,2233,2105,2087,2109,2111,2225,2269,2292,2320,2275,2045,2331,2349,2219,188,490,287,157,258,259,227,168,154,169,260,152,167,153,226,257,225,253,256,234,164,155])).
% 61.31/61.30 cnf(2410,plain,
% 61.31/61.30 (P1(x24101,x24102,x24102)),
% 61.31/61.30 inference(rename_variables,[],[2233])).
% 61.31/61.30 cnf(2415,plain,
% 61.31/61.30 (P8(x24151,x24152,x24153,x24154,x24151,x24152,x24153,x24154)),
% 61.31/61.30 inference(rename_variables,[],[2245])).
% 61.31/61.30 cnf(2423,plain,
% 61.31/61.30 (P3(f25(a17,x24231),a17,x24231)),
% 61.31/61.30 inference(rename_variables,[],[2331])).
% 61.31/61.30 cnf(2425,plain,
% 61.31/61.30 (P5(x24251,x24252,x24252,x24252)),
% 61.31/61.30 inference(scs_inference,[],[2245,2415,2257,2355,2233,2410,2105,2087,2109,2111,2149,2171,2225,2269,2292,2310,2320,2326,2333,2308,2275,2045,2331,2259,2315,2349,2219,2029,2173,188,490,287,157,258,259,227,168,154,169,260,152,167,153,226,257,225,253,256,234,164,155,255,165,254,166,174,247,199,191,246,204,241,228,237])).
% 61.31/61.30 cnf(2426,plain,
% 61.31/61.30 (P8(x24261,x24262,x24263,x24264,x24261,x24262,x24263,x24264)),
% 61.31/61.30 inference(rename_variables,[],[2245])).
% 61.31/61.30 cnf(2427,plain,
% 61.31/61.30 (P1(x24271,x24272,x24272)),
% 61.31/61.30 inference(rename_variables,[],[2233])).
% 61.31/61.30 cnf(2429,plain,
% 61.31/61.30 (P9(a17,a17,x24291,x24291)),
% 61.31/61.30 inference(scs_inference,[],[2245,2415,2257,2355,2233,2410,2105,2087,2109,2111,2149,2171,2225,2269,2292,2310,2320,2326,2333,2308,2275,2045,2331,2423,2259,2315,2349,2219,2029,2173,188,490,287,157,258,259,227,168,154,169,260,152,167,153,226,257,225,253,256,234,164,155,255,165,254,166,174,247,199,191,246,204,241,228,237,158])).
% 61.31/61.30 cnf(2437,plain,
% 61.31/61.30 (P2(a1,a1,a1,a1)),
% 61.31/61.30 inference(scs_inference,[],[2245,2415,2257,2355,2233,2410,2105,2087,2109,2111,2149,2171,2225,2269,2292,2310,2320,2326,2333,2308,2275,2045,2331,2423,2259,2315,2349,2219,2029,2173,188,490,287,157,258,259,227,168,154,169,260,152,167,153,226,257,225,253,256,234,164,155,255,165,254,166,174,247,199,191,246,204,241,228,237,158,224,190,206,185])).
% 61.31/61.30 cnf(2439,plain,
% 61.31/61.30 (P10(a18,a1,a20,a20)),
% 61.31/61.30 inference(scs_inference,[],[2245,2415,2257,2355,2233,2410,2105,2087,2109,2111,2149,2171,2225,2241,2269,2292,2310,2320,2326,2333,2308,2275,2045,2331,2423,2259,2315,2349,2219,2029,2173,188,490,287,157,258,259,227,168,154,169,260,152,167,153,226,257,225,253,256,234,164,155,255,165,254,166,174,247,199,191,246,204,241,228,237,158,224,190,206,185,182])).
% 61.31/61.30 cnf(2441,plain,
% 61.31/61.30 (P10(a18,a1,a1,a1)),
% 61.31/61.30 inference(scs_inference,[],[2245,2415,2257,2355,2233,2410,2105,2087,2109,2111,2149,2123,2171,2225,2241,2269,2292,2310,2320,2326,2333,2308,2275,2045,2331,2423,2259,2315,2349,2219,2029,2169,2173,188,490,287,157,258,259,227,168,154,169,260,152,167,153,226,257,225,253,256,234,164,155,255,165,254,166,174,247,199,191,246,204,241,228,237,158,224,190,206,185,182,173])).
% 61.31/61.30 cnf(2445,plain,
% 61.31/61.30 (P3(a17,x24451,x24451)),
% 61.31/61.30 inference(scs_inference,[],[2245,2415,2257,2355,2233,2410,2105,2087,2109,2111,2149,2123,2171,2225,2241,2269,2292,2310,2320,2326,2333,2308,2275,2045,2331,2423,2259,2315,2349,2219,2029,2169,2164,2157,2173,188,490,287,157,258,259,227,168,154,169,260,152,167,153,226,257,225,253,256,234,164,155,255,165,254,166,174,247,199,191,246,204,241,228,237,158,224,190,206,185,182,173,193,176])).
% 61.31/61.30 cnf(2449,plain,
% 61.31/61.30 (P3(f25(a18,x24491),a18,x24491)),
% 61.31/61.30 inference(scs_inference,[],[2245,2415,2257,2355,2233,2410,2105,2087,2109,2111,2149,2123,2171,2225,2241,2269,2292,2310,2320,2326,2333,2308,2275,2045,2331,2423,2259,2315,2349,2219,2029,2169,2155,2164,2157,2173,188,490,287,157,258,259,227,168,154,169,260,152,167,153,226,257,225,253,256,234,164,155,255,165,254,166,174,247,199,191,246,204,241,228,237,158,224,190,206,185,182,173,193,176,160])).
% 61.31/61.30 cnf(2451,plain,
% 61.31/61.30 (P4(a16,a16,a16,a16)),
% 61.31/61.30 inference(scs_inference,[],[2245,2415,2426,2257,2355,2233,2410,2105,2087,2109,2111,2149,2123,2171,2225,2241,2269,2292,2303,2310,2320,2326,2333,2308,2275,2045,2331,2423,2259,2315,2349,2219,2029,2169,2155,2164,2157,2173,188,490,287,157,258,259,227,168,154,169,260,152,167,153,226,257,225,253,256,234,164,155,255,165,254,166,174,247,199,191,246,204,241,228,237,158,224,190,206,185,182,173,193,176,160,252])).
% 61.31/61.30 cnf(2454,plain,
% 61.31/61.30 (P1(a20,x24541,f14(a18,a18,a1,a1,a20,x24541))),
% 61.31/61.30 inference(scs_inference,[],[2245,2415,2426,2257,2355,2233,2410,2427,2105,2087,2109,2111,2149,2123,2171,2225,2241,2269,2292,2303,2310,2320,2326,2333,2308,2275,2045,2331,2423,2259,2315,2349,2219,2027,2029,2169,2155,2164,2157,2173,188,490,287,157,258,259,227,168,154,169,260,152,167,153,226,257,225,253,256,234,164,155,255,165,254,166,174,247,199,191,246,204,241,228,237,158,224,190,206,185,182,173,193,176,160,252,207])).
% 61.31/61.30 cnf(2457,plain,
% 61.31/61.30 (P9(f28(a17,a17,a17,a17,a17,a17),a17,a16,a16)),
% 61.31/61.30 inference(scs_inference,[],[2245,2415,2426,2257,2355,2233,2410,2427,2105,2087,2109,2111,2149,2123,2171,2225,2241,2269,2292,2303,2310,2320,2326,2333,2308,2275,2045,2331,2423,2259,2315,2349,2219,2027,2029,2169,2155,2164,2157,2173,188,490,287,157,258,259,227,168,154,169,260,152,167,153,226,257,225,253,256,234,164,155,255,165,254,166,174,247,199,191,246,204,241,228,237,158,224,190,206,185,182,173,193,176,160,252,207,670])).
% 61.31/61.30 cnf(2459,plain,
% 61.31/61.30 (P5(x24591,x24592,x24591,x24591)),
% 61.31/61.30 inference(scs_inference,[],[2245,2415,2426,2257,2355,2233,2410,2427,2105,2087,2109,2111,2149,2123,2171,2225,2241,2269,2292,2303,2310,2320,2326,2333,2308,2275,2045,2331,2423,2259,2315,2349,2219,2027,2029,2169,2155,2164,2157,2173,188,490,287,157,258,259,227,168,154,169,260,152,167,153,226,257,225,253,256,234,164,155,255,165,254,166,174,247,199,191,246,204,241,228,237,158,224,190,206,185,182,173,193,176,160,252,207,670,170])).
% 61.31/61.30 cnf(2461,plain,
% 61.31/61.30 (P1(a17,a17,f30(a17,a17,a17,a17,a17))),
% 61.31/61.30 inference(scs_inference,[],[2245,2415,2426,2257,2355,2233,2410,2427,2105,2087,2109,2111,2149,2123,2171,2225,2241,2269,2292,2303,2310,2320,2326,2333,2308,2275,2045,2331,2423,2259,2315,2349,2219,2027,2029,2169,2155,2164,2157,2173,188,490,287,157,258,259,227,168,154,169,260,152,167,153,226,257,225,253,256,234,164,155,255,165,254,166,174,247,199,191,246,204,241,228,237,158,224,190,206,185,182,173,193,176,160,252,207,670,170,161])).
% 61.31/61.30 cnf(2497,plain,
% 61.31/61.30 (P1(x24971,x24972,x24971)),
% 61.31/61.30 inference(rename_variables,[],[2375])).
% 61.31/61.30 cnf(2500,plain,
% 61.31/61.30 (P1(x25001,x25002,x25001)),
% 61.31/61.30 inference(rename_variables,[],[2375])).
% 61.31/61.30 cnf(2504,plain,
% 61.31/61.30 (P5(x25041,x25041,x25042,x25041)),
% 61.31/61.30 inference(scs_inference,[],[2459,2375,2497,2437,1060,1071,188,171])).
% 61.31/61.30 cnf(2507,plain,
% 61.31/61.30 (P1(x25071,x25072,x25071)),
% 61.31/61.30 inference(rename_variables,[],[2375])).
% 61.31/61.30 cnf(2509,plain,
% 61.31/61.30 (P4(a17,x25091,a17,x25091)),
% 61.31/61.30 inference(scs_inference,[],[2459,2375,2497,2500,2445,2437,1060,1071,188,171,287,157])).
% 61.31/61.30 cnf(2531,plain,
% 61.31/61.30 (P1(x25311,x25311,x25312)),
% 61.31/61.30 inference(scs_inference,[],[2459,2375,2497,2500,2507,2363,2445,2091,2162,2437,2037,2271,2282,2395,1060,1071,188,171,287,157,259,168,169,167,154,258,152,227,257,260,153])).
% 61.31/61.30 cnf(2533,plain,
% 61.31/61.30 (P8(a17,a17,x25331,x25332,x25333,x25333,x25331,x25332)),
% 61.31/61.30 inference(scs_inference,[],[2459,2375,2497,2500,2507,2363,2445,2429,2091,2162,2437,2037,2271,2282,2395,1060,1071,188,171,287,157,259,168,169,167,154,258,152,227,257,260,153,226])).
% 61.31/61.30 cnf(2537,plain,
% 61.31/61.30 (P9(x25371,x25371,a17,a17)),
% 61.31/61.30 inference(scs_inference,[],[2459,2375,2497,2500,2507,2363,2445,2265,2429,2091,2162,2437,2037,2271,2282,2395,1060,1071,188,171,287,157,259,168,169,167,154,258,152,227,257,260,153,226,253,164])).
% 61.31/61.30 cnf(2541,plain,
% 61.31/61.30 (P8(x25411,x25412,x25412,x25411,x25413,x25414,x25413,x25414)),
% 61.31/61.30 inference(scs_inference,[],[2381,2459,2375,2497,2500,2507,2363,2445,2265,2429,2091,2162,2437,2037,2271,2282,2395,2449,1060,1071,188,171,287,157,259,168,169,167,154,258,152,227,257,260,153,226,253,164,155,256])).
% 61.31/61.30 cnf(2543,plain,
% 61.31/61.30 (P9(a17,a17,a17,f4(a17,a17,a17))),
% 61.31/61.30 inference(scs_inference,[],[2381,2459,2375,2497,2500,2507,2363,2445,2265,2429,2091,2162,2437,2037,2271,2282,2395,2449,1060,1071,188,171,287,157,259,168,169,167,154,258,152,227,257,260,153,226,253,164,155,256,234])).
% 61.31/61.30 cnf(2547,plain,
% 61.31/61.30 (P9(a18,a3,a16,a1)),
% 61.31/61.30 inference(scs_inference,[],[2381,2459,2375,2497,2500,2507,2363,2445,2265,2429,2091,2117,2162,2354,2437,2037,2271,2282,2395,2449,1060,1071,188,171,287,157,259,168,169,167,154,258,152,227,257,260,153,226,253,164,155,256,234,255,165])).
% 61.31/61.30 cnf(2549,plain,
% 61.31/61.30 (P8(x25491,x25492,x25493,x25494,x25491,x25492,x25494,x25493)),
% 61.31/61.30 inference(scs_inference,[],[2381,2459,2375,2497,2500,2507,2363,2445,2265,2429,2091,2117,2162,2354,2437,2037,2271,2282,2395,2449,1060,1071,188,171,287,157,259,168,169,167,154,258,152,227,257,260,153,226,253,164,155,256,234,255,165,254])).
% 61.31/61.30 cnf(2553,plain,
% 61.31/61.30 (P4(a1,a1,a1,f30(a18,a1,a1,a1,a1))),
% 61.31/61.30 inference(scs_inference,[],[2381,2459,2375,2497,2500,2507,2337,2363,2445,2265,2429,2091,2117,2162,2354,2437,2441,2037,2271,2282,2395,2449,2333,1060,1071,188,171,287,157,259,168,169,167,154,258,152,227,257,260,153,226,253,164,155,256,234,255,165,254,166,201])).
% 61.31/61.30 cnf(2558,plain,
% 61.31/61.30 (P8(x25581,x25582,x25583,x25584,x25582,x25581,x25583,x25584)),
% 61.31/61.30 inference(rename_variables,[],[2381])).
% 61.31/61.30 cnf(2561,plain,
% 61.31/61.30 (P3(a17,x25611,x25611)),
% 61.31/61.30 inference(rename_variables,[],[2445])).
% 61.31/61.30 cnf(2563,plain,
% 61.31/61.30 (~P8(a1,a19,a19,a18,f8(a3,a2,a21,a17),a3,a3,a17)),
% 61.31/61.30 inference(scs_inference,[],[2381,2558,2459,2375,2497,2500,2507,2337,2363,2445,2265,2429,2091,2117,2162,2354,2437,2441,2037,2271,2282,2395,2449,2352,2055,2333,1060,1071,188,171,287,157,259,168,169,167,154,258,152,227,257,260,153,226,253,164,155,256,234,255,165,254,166,201,202,251,174,263])).
% 61.31/61.30 cnf(2564,plain,
% 61.31/61.30 (P8(x25641,x25642,x25643,x25644,x25642,x25641,x25643,x25644)),
% 61.31/61.30 inference(rename_variables,[],[2381])).
% 61.31/61.30 cnf(2566,plain,
% 61.31/61.30 (P10(f13(a18,a1,a1,a2,a18),a18,a2,a18)),
% 61.31/61.30 inference(scs_inference,[],[142,2381,2558,2459,2375,2497,2500,2507,2337,2363,2445,2265,2429,2091,2117,2162,2354,2437,2441,2037,2271,2282,2395,2449,2352,2055,2333,1060,1071,188,171,287,157,259,168,169,167,154,258,152,227,257,260,153,226,253,164,155,256,234,255,165,254,166,201,202,251,174,263,199])).
% 61.31/61.30 cnf(2568,plain,
% 61.31/61.30 (P1(f13(a18,a1,a1,a2,a18),a2,a18)),
% 61.31/61.30 inference(scs_inference,[],[142,2381,2558,2459,2375,2497,2500,2507,2337,2363,2445,2265,2429,2091,2117,2162,2354,2437,2441,2037,2271,2282,2395,2449,2352,2055,2333,1060,1071,188,171,287,157,259,168,169,167,154,258,152,227,257,260,153,226,253,164,155,256,234,255,165,254,166,201,202,251,174,263,199,198])).
% 61.31/61.30 cnf(2573,plain,
% 61.31/61.30 (P8(x25731,x25732,x25731,x25732,x25733,x25734,x25733,x25734)),
% 61.31/61.30 inference(rename_variables,[],[2389])).
% 61.31/61.30 cnf(2576,plain,
% 61.31/61.30 (P8(x25761,x25762,x25763,x25764,x25762,x25761,x25763,x25764)),
% 61.31/61.30 inference(rename_variables,[],[2381])).
% 61.31/61.30 cnf(2579,plain,
% 61.31/61.30 (P5(x25791,x25792,x25792,x25792)),
% 61.31/61.30 inference(rename_variables,[],[2425])).
% 61.31/61.30 cnf(2582,plain,
% 61.31/61.30 (P3(a17,x25821,x25821)),
% 61.31/61.30 inference(rename_variables,[],[2445])).
% 61.31/61.30 cnf(2584,plain,
% 61.31/61.30 (P5(a18,a18,a1,a2)),
% 61.31/61.30 inference(scs_inference,[],[142,2381,2558,2564,2389,2573,2425,2459,2375,2497,2500,2507,2337,2363,2445,2561,2265,2429,2091,2117,2162,2354,2437,2441,2037,2339,2271,2282,2395,2449,2352,2055,2333,1060,1071,188,171,287,157,259,168,169,167,154,258,152,227,257,260,153,226,253,164,155,256,234,255,165,254,166,201,202,251,174,263,199,198,204,248,241,192,228,237])).
% 61.31/61.30 cnf(2587,plain,
% 61.31/61.30 (P7(a17,x25871,x25871,x25871,a17,x25871,x25871,x25871)),
% 61.31/61.30 inference(scs_inference,[],[142,2381,2558,2564,2389,2573,2425,2459,2375,2497,2500,2507,2337,2363,2445,2561,2582,2265,2429,2091,2117,2162,2354,2437,2441,2037,2339,2271,2282,2395,2449,2352,2055,2333,1060,1071,188,171,287,157,259,168,169,167,154,258,152,227,257,260,153,226,253,164,155,256,234,255,165,254,166,201,202,251,174,263,199,198,204,248,241,192,228,237,224])).
% 61.31/61.30 cnf(2591,plain,
% 61.31/61.30 (P10(a1,a18,a1,a1)),
% 61.31/61.30 inference(scs_inference,[],[142,2381,2558,2564,2576,2389,2573,2425,2459,2375,2497,2500,2507,2337,2363,2445,2561,2582,2265,2429,2091,2117,2162,2354,2437,2441,2037,2339,2271,2282,2395,2449,2352,2055,2333,1060,1071,188,171,287,157,259,168,169,167,154,258,152,227,257,260,153,226,253,164,155,256,234,255,165,254,166,201,202,251,174,263,199,198,204,248,241,192,228,237,224,205,242])).
% 61.31/61.30 cnf(2592,plain,
% 61.31/61.30 (P8(x25921,x25922,x25923,x25924,x25922,x25921,x25923,x25924)),
% 61.31/61.30 inference(rename_variables,[],[2381])).
% 61.31/61.30 cnf(2594,plain,
% 61.31/61.30 (P2(a16,a16,a16,a16)),
% 61.31/61.30 inference(scs_inference,[],[142,2381,2558,2564,2576,2389,2573,2425,2459,2375,2497,2500,2507,2337,2363,2445,2561,2582,2265,2429,2091,2117,2162,2354,2437,2441,2451,2037,2339,2271,2282,2395,2449,2352,2055,2333,1060,1071,188,171,287,157,259,168,169,167,154,258,152,227,257,260,153,226,253,164,155,256,234,255,165,254,166,201,202,251,174,263,199,198,204,248,241,192,228,237,224,205,242,185])).
% 61.31/61.30 cnf(2596,plain,
% 61.31/61.30 (P10(a16,a16,a16,a16)),
% 61.31/61.30 inference(scs_inference,[],[142,2381,2558,2564,2576,2389,2573,2425,2459,2375,2497,2500,2507,2337,2363,2445,2561,2582,2265,2429,2091,2117,2162,2354,2437,2441,2451,2037,2339,2271,2282,2395,2449,2352,2055,2333,1060,1071,188,171,287,157,259,168,169,167,154,258,152,227,257,260,153,226,253,164,155,256,234,255,165,254,166,201,202,251,174,263,199,198,204,248,241,192,228,237,224,205,242,185,182])).
% 61.31/61.30 cnf(2598,plain,
% 61.31/61.30 (P10(a1,a1,a1,a1)),
% 61.31/61.30 inference(scs_inference,[],[142,2381,2558,2564,2576,2389,2573,2425,2459,2375,2497,2500,2507,2337,2363,2445,2561,2582,2265,2429,2091,2117,2162,2354,2437,2441,2451,2037,2339,2271,2282,2395,2449,2352,2055,2333,1060,1071,188,171,287,157,259,168,169,167,154,258,152,227,257,260,153,226,253,164,155,256,234,255,165,254,166,201,202,251,174,263,199,198,204,248,241,192,228,237,224,205,242,185,182,173])).
% 61.31/61.30 cnf(2599,plain,
% 61.31/61.30 (P1(x25991,x25992,x25991)),
% 61.31/61.30 inference(rename_variables,[],[2375])).
% 61.31/61.30 cnf(2601,plain,
% 61.31/61.30 (P3(a17,a17,f30(a17,a17,a17,a17,a17))),
% 61.31/61.30 inference(scs_inference,[],[142,2381,2558,2564,2576,2389,2573,2425,2459,2375,2497,2500,2507,2337,2363,2445,2561,2582,2265,2429,2091,2117,2162,2354,2437,2441,2451,2037,2339,2271,2282,2395,2449,2461,2391,2352,2055,2333,1060,1071,188,171,287,157,259,168,169,167,154,258,152,227,257,260,153,226,253,164,155,256,234,255,165,254,166,201,202,251,174,263,199,198,204,248,241,192,228,237,224,205,242,185,182,173,163])).
% 61.31/61.30 cnf(2602,plain,
% 61.31/61.30 (P3(a17,x26021,x26021)),
% 61.31/61.30 inference(rename_variables,[],[2445])).
% 61.31/61.30 cnf(2604,plain,
% 61.31/61.30 (P3(a1,a1,a1)),
% 61.31/61.30 inference(scs_inference,[],[142,2381,2558,2564,2576,2592,2389,2573,2425,2459,2375,2497,2500,2507,2599,2337,2363,2445,2561,2582,2265,2429,2091,2117,2162,2354,2437,2441,2451,2037,2339,2271,2282,2395,2449,2461,2391,2352,2055,2333,1060,1071,188,171,287,157,259,168,169,167,154,258,152,227,257,260,153,226,253,164,155,256,234,255,165,254,166,201,202,251,174,263,199,198,204,248,241,192,228,237,224,205,242,185,182,173,163,240])).
% 61.31/61.30 cnf(2605,plain,
% 61.31/61.30 (P1(x26051,x26052,x26051)),
% 61.31/61.30 inference(rename_variables,[],[2375])).
% 61.31/61.30 cnf(2606,plain,
% 61.31/61.30 (P8(x26061,x26062,x26063,x26064,x26062,x26061,x26063,x26064)),
% 61.31/61.30 inference(rename_variables,[],[2381])).
% 61.31/61.30 cnf(2608,plain,
% 61.31/61.30 (P3(f28(a3,a16,a3,a16,a17,a17),a16,a3)),
% 61.31/61.30 inference(scs_inference,[],[142,2381,2558,2564,2576,2592,2389,2573,2425,2459,2375,2497,2500,2507,2599,2337,2363,2445,2561,2582,2265,2429,2091,2117,2162,2354,2437,2441,2451,2037,2339,2271,2282,2395,2449,2461,2391,2290,2352,2055,2257,2333,271,1060,1071,188,171,287,157,259,168,169,167,154,258,152,227,257,260,153,226,253,164,155,256,234,255,165,254,166,201,202,251,174,263,199,198,204,248,241,192,228,237,224,205,242,185,182,173,163,240,176])).
% 61.31/61.30 cnf(2609,plain,
% 61.31/61.30 (P9(x26091,x26092,x26092,x26091)),
% 61.31/61.30 inference(rename_variables,[],[2257])).
% 61.31/61.30 cnf(2611,plain,
% 61.31/61.30 (P3(f25(x26111,x26112),x26111,x26112)),
% 61.31/61.30 inference(scs_inference,[],[142,2381,2558,2564,2576,2592,2389,2573,2425,2459,2375,2497,2500,2507,2599,2605,2337,2363,2445,2561,2582,2602,2265,2429,2091,2117,2162,2354,2437,2441,2451,2037,2339,2271,2282,2395,2449,2461,2391,2290,2352,2055,2257,2333,271,1060,1071,188,171,287,157,259,168,169,167,154,258,152,227,257,260,153,226,253,164,155,256,234,255,165,254,166,201,202,251,174,263,199,198,204,248,241,192,228,237,224,205,242,185,182,173,163,240,176,160])).
% 61.31/61.30 cnf(2612,plain,
% 61.31/61.30 (P3(a17,x26121,x26121)),
% 61.31/61.30 inference(rename_variables,[],[2445])).
% 61.31/61.30 cnf(2613,plain,
% 61.31/61.30 (P3(a17,x26131,x26131)),
% 61.31/61.30 inference(rename_variables,[],[2445])).
% 61.31/61.30 cnf(2617,plain,
% 61.31/61.30 (P9(x26171,x26172,x26172,x26171)),
% 61.31/61.30 inference(rename_variables,[],[2257])).
% 61.31/61.30 cnf(2619,plain,
% 61.31/61.30 (P4(x26191,x26191,x26191,x26191)),
% 61.31/61.30 inference(scs_inference,[],[142,2381,2558,2564,2576,2592,2606,2389,2573,2425,2579,2459,2375,2497,2500,2507,2599,2605,2337,2363,2445,2561,2582,2602,2265,2429,2091,2117,2162,2354,2437,2441,2451,2037,2339,2271,2282,2395,2449,2461,2391,2290,2352,2055,2257,2609,2003,2333,271,1060,1071,188,171,287,157,259,168,169,167,154,258,152,227,257,260,153,226,253,164,155,256,234,255,165,254,166,201,202,251,174,263,199,198,204,248,241,192,228,237,224,205,242,185,182,173,163,240,176,160,208,252])).
% 61.31/61.30 cnf(2622,plain,
% 61.31/61.30 (P5(x26221,x26222,x26222,x26222)),
% 61.31/61.30 inference(rename_variables,[],[2425])).
% 61.31/61.30 cnf(2624,plain,
% 61.31/61.30 (P10(a17,a17,a16,a16)),
% 61.31/61.30 inference(scs_inference,[],[142,2381,2558,2564,2576,2592,2606,2389,2573,2425,2579,2459,2375,2497,2500,2507,2599,2605,2337,2363,2445,2561,2582,2602,2265,2429,2091,2117,2162,2354,2437,2441,2451,2037,2339,2271,2282,2395,2449,2461,2391,2290,2352,2055,2257,2609,2003,2333,271,1060,1071,188,171,287,157,259,168,169,167,154,258,152,227,257,260,153,226,253,164,155,256,234,255,165,254,166,201,202,251,174,263,199,198,204,248,241,192,228,237,224,205,242,185,182,173,163,240,176,160,208,252,978])).
% 61.31/61.30 cnf(2626,plain,
% 61.31/61.30 (P9(x26261,x26261,a16,a16)),
% 61.31/61.30 inference(scs_inference,[],[142,2381,2558,2564,2576,2592,2606,2389,2573,2425,2579,2459,2375,2497,2500,2507,2599,2605,2337,2363,2445,2561,2582,2602,2265,2429,2091,2117,2162,2354,2437,2441,2451,2037,2339,2271,2282,2395,2449,2461,2391,2290,2352,2055,2257,2609,2003,2333,271,1060,1071,188,171,287,157,259,168,169,167,154,258,152,227,257,260,153,226,253,164,155,256,234,255,165,254,166,201,202,251,174,263,199,198,204,248,241,192,228,237,224,205,242,185,182,173,163,240,176,160,208,252,978,670])).
% 61.31/61.30 cnf(2628,plain,
% 61.31/61.30 (P10(a3,a3,a16,a16)),
% 61.31/61.30 inference(scs_inference,[],[142,2381,2558,2564,2576,2592,2606,2389,2573,2425,2579,2459,2375,2497,2500,2507,2599,2605,2337,2363,2445,2561,2582,2602,2265,2429,2091,2117,2162,2354,2437,2441,2451,2037,2339,2271,2282,2395,2449,2461,2391,2290,2352,2055,2257,2609,2003,2333,271,1060,1071,188,171,287,157,259,168,169,167,154,258,152,227,257,260,153,226,253,164,155,256,234,255,165,254,166,201,202,251,174,263,199,198,204,248,241,192,228,237,224,205,242,185,182,173,163,240,176,160,208,252,978,670,877])).
% 61.31/61.30 cnf(2630,plain,
% 61.31/61.30 (P5(x26301,x26301,x26301,x26302)),
% 61.31/61.30 inference(scs_inference,[],[142,2381,2558,2564,2576,2592,2606,2389,2573,2425,2579,2459,2375,2497,2500,2507,2599,2605,2337,2363,2445,2561,2582,2602,2265,2429,2091,2117,2162,2354,2437,2441,2451,2037,2339,2271,2282,2395,2449,2461,2391,2290,2352,2055,2257,2609,2003,2333,271,1060,1071,188,171,287,157,259,168,169,167,154,258,152,227,257,260,153,226,253,164,155,256,234,255,165,254,166,201,202,251,174,263,199,198,204,248,241,192,228,237,224,205,242,185,182,173,163,240,176,160,208,252,978,670,877,172])).
% 61.31/61.30 cnf(2644,plain,
% 61.31/61.30 (P9(f28(x26441,x26441,x26442,x26442,a17,a17),a17,x26441,x26442)),
% 61.31/61.30 inference(scs_inference,[],[142,2381,2558,2564,2576,2592,2606,2389,2573,2425,2579,2459,2375,2497,2500,2507,2599,2605,2337,2363,2445,2561,2582,2602,2613,2612,2265,2429,2091,2117,2162,2354,2437,2441,2451,2037,2339,2271,2282,2395,2449,2461,2391,2290,2352,2055,2257,2609,2003,2333,271,1060,1071,188,171,287,157,259,168,169,167,154,258,152,227,257,260,153,226,253,164,155,256,234,255,165,254,166,201,202,251,174,263,199,198,204,248,241,192,228,237,224,205,242,185,182,173,163,240,176,160,208,252,978,670,877,172,1395,200,189,195,191,190,206])).
% 61.31/61.30 cnf(2651,plain,
% 61.31/61.30 (P3(f7(a16,a16,a16),a16,a16)),
% 61.31/61.30 inference(scs_inference,[],[142,2381,2558,2564,2576,2592,2606,2389,2573,2425,2579,2622,2459,2375,2497,2500,2507,2599,2605,2337,2363,2445,2561,2582,2602,2613,2612,2265,2429,2091,2117,2162,2354,2437,2441,2451,2037,2339,2271,2282,2395,2449,2461,2391,2290,2352,2055,2257,2609,2617,2003,2333,271,1060,1071,188,171,287,157,259,168,169,167,154,258,152,227,257,260,153,226,253,164,155,256,234,255,165,254,166,201,202,251,174,263,199,198,204,248,241,192,228,237,224,205,242,185,182,173,163,240,176,160,208,252,978,670,877,172,1395,200,189,195,191,190,206,193,187])).
% 61.31/61.30 cnf(2660,plain,
% 61.31/61.30 (P9(f28(x26601,x26601,x26602,x26602,a17,a17),a17,x26601,x26602)),
% 61.31/61.30 inference(rename_variables,[],[2644])).
% 61.31/61.30 cnf(2663,plain,
% 61.31/61.30 (P1(x26631,x26631,x26632)),
% 61.31/61.30 inference(rename_variables,[],[2531])).
% 61.31/61.30 cnf(2668,plain,
% 61.31/61.30 (P1(x26681,x26681,x26682)),
% 61.31/61.30 inference(rename_variables,[],[2531])).
% 61.31/61.30 cnf(2671,plain,
% 61.31/61.30 (P9(f28(x26711,x26711,x26712,x26712,a17,a17),a17,x26711,x26712)),
% 61.31/61.30 inference(rename_variables,[],[2644])).
% 61.31/61.30 cnf(2673,plain,
% 61.31/61.30 (P5(a18,a18,a2,a1)),
% 61.31/61.30 inference(scs_inference,[],[2531,2663,2584,2594,2644,2660,514,1060,188,1071,608,172])).
% 61.31/61.30 cnf(2676,plain,
% 61.31/61.30 (P9(f28(x26761,x26761,x26762,x26762,a17,a17),a17,x26761,x26762)),
% 61.31/61.30 inference(rename_variables,[],[2644])).
% 61.31/61.30 cnf(2679,plain,
% 61.31/61.30 (P9(f28(x26791,x26791,x26792,x26792,a17,a17),a17,x26791,x26792)),
% 61.31/61.30 inference(rename_variables,[],[2644])).
% 61.31/61.30 cnf(2681,plain,
% 61.31/61.30 (P5(a18,a1,a18,a2)),
% 61.31/61.30 inference(scs_inference,[],[2531,2663,2584,2594,2644,2660,2671,2676,514,1060,188,1071,608,172,636,490,171])).
% 61.31/61.30 cnf(2683,plain,
% 61.31/61.30 (P1(f25(x26831,x26832),x26831,x26832)),
% 61.31/61.30 inference(scs_inference,[],[2531,2663,2584,2594,2611,2644,2660,2671,2676,514,1060,188,1071,608,172,636,490,171,154])).
% 61.31/61.30 cnf(2685,plain,
% 61.31/61.30 (P4(f25(x26851,x26852),x26851,f25(x26851,x26852),x26852)),
% 61.31/61.30 inference(scs_inference,[],[2531,2663,2584,2594,2611,2644,2660,2671,2676,514,1060,188,1071,608,172,636,490,171,154,157])).
% 61.31/61.30 cnf(2691,plain,
% 61.31/61.30 (P8(a18,a18,a18,a1,a2,a18,a2,a1)),
% 61.31/61.30 inference(scs_inference,[],[2531,2663,2584,2594,2611,2566,2644,2660,2671,2676,2379,514,1060,188,1071,608,172,636,490,171,154,157,167,287,225])).
% 61.31/61.30 cnf(2697,plain,
% 61.31/61.30 (P4(a17,x26971,x26971,a17)),
% 61.31/61.30 inference(scs_inference,[],[2531,2663,2373,2509,2584,2594,2611,2568,2566,2644,2660,2671,2676,2379,514,1060,188,1071,608,172,636,490,171,154,157,167,287,225,259,152,169])).
% 61.31/61.30 cnf(2699,plain,
% 61.31/61.30 (P7(a17,x26991,a17,x26991,x26991,x26991,x26991,x26991)),
% 61.31/61.30 inference(scs_inference,[],[2531,2663,2373,2587,2509,2584,2594,2611,2568,2566,2644,2660,2671,2676,2379,514,1060,188,1071,608,172,636,490,171,154,157,167,287,225,259,152,169,260])).
% 61.31/61.30 cnf(2701,plain,
% 61.31/61.30 (P8(a17,x27011,x27011,x27011,x27011,x27011,a17,x27011)),
% 61.31/61.30 inference(scs_inference,[],[2531,2663,2373,2587,2509,2584,2594,2611,2568,2566,2644,2660,2671,2676,2379,514,1060,188,1071,608,172,636,490,171,154,157,167,287,225,259,152,169,260,227])).
% 61.31/61.30 cnf(2711,plain,
% 61.31/61.30 (P8(x27111,x27112,x27111,x27112,x27113,x27114,x27114,x27113)),
% 61.31/61.30 inference(scs_inference,[],[2549,2531,2663,2373,2587,2509,2584,2594,2611,2568,2566,2553,2644,2660,2671,2676,2379,514,1060,188,1071,608,172,636,490,171,154,157,167,287,225,259,152,169,260,227,168,258,153,257,256])).
% 61.31/61.30 cnf(2713,plain,
% 61.31/61.30 (P9(a16,a16,x27131,x27131)),
% 61.31/61.30 inference(scs_inference,[],[2549,2531,2663,2373,2587,2509,2626,2584,2594,2611,2568,2566,2553,2644,2660,2671,2676,2379,514,1060,188,1071,608,172,636,490,171,154,157,167,287,225,259,152,169,260,227,168,258,153,257,256,164])).
% 61.31/61.30 cnf(2715,plain,
% 61.31/61.30 (P8(x27151,x27151,x27152,x27153,a17,a17,x27152,x27153)),
% 61.31/61.30 inference(scs_inference,[],[2549,2531,2663,2373,2587,2509,2537,2626,2584,2594,2611,2568,2566,2553,2644,2660,2671,2676,2379,514,1060,188,1071,608,172,636,490,171,154,157,167,287,225,259,152,169,260,227,168,258,153,257,256,164,226])).
% 61.31/61.30 cnf(2719,plain,
% 61.31/61.30 (P3(f25(x27191,x27192),x27192,x27191)),
% 61.31/61.30 inference(scs_inference,[],[2549,2531,2663,2373,2587,2509,2537,2626,2267,2584,2594,2611,2568,2566,2553,2644,2660,2671,2676,2379,514,1060,188,1071,608,172,636,490,171,154,157,167,287,225,259,152,169,260,227,168,258,153,257,256,164,226,253,155])).
% 61.31/61.30 cnf(2721,plain,
% 61.31/61.30 (P8(x27211,x27212,x27213,x27214,x27212,x27211,x27214,x27213)),
% 61.31/61.30 inference(scs_inference,[],[2549,2531,2663,2373,2587,2509,2537,2626,2267,2584,2594,2611,2568,2566,2553,2644,2660,2671,2676,2379,514,1060,188,1071,608,172,636,490,171,154,157,167,287,225,259,152,169,260,227,168,258,153,257,256,164,226,253,155,255])).
% 61.31/61.30 cnf(2723,plain,
% 61.31/61.30 (P9(f28(x27231,x27231,x27232,x27232,a17,a17),a17,x27232,x27231)),
% 61.31/61.30 inference(scs_inference,[],[2549,2531,2663,2373,2587,2509,2537,2626,2267,2584,2594,2611,2568,2566,2553,2644,2660,2671,2676,2679,2379,514,1060,188,1071,608,172,636,490,171,154,157,167,287,225,259,152,169,260,227,168,258,153,257,256,164,226,253,155,255,165])).
% 61.31/61.30 cnf(2727,plain,
% 61.31/61.30 (P10(a20,a20,a1,a18)),
% 61.31/61.30 inference(scs_inference,[],[2549,2531,2663,2373,2322,2587,2533,2509,2537,2626,2267,2584,2594,2611,2568,2566,2553,2644,2660,2671,2676,2679,2379,514,1060,188,1071,608,172,636,490,171,154,157,167,287,225,259,152,169,260,227,168,258,153,257,256,164,226,253,155,255,165,254,166])).
% 61.31/61.30 cnf(2730,plain,
% 61.31/61.30 (P4(x27301,x27301,x27301,x27301)),
% 61.31/61.30 inference(rename_variables,[],[2619])).
% 61.31/61.30 cnf(2733,plain,
% 61.31/61.30 (P4(x27331,x27331,x27331,x27331)),
% 61.31/61.30 inference(rename_variables,[],[2619])).
% 61.31/61.30 cnf(2737,plain,
% 61.31/61.30 (P8(x27371,x27372,x27372,x27371,x27373,x27374,x27373,x27374)),
% 61.31/61.30 inference(rename_variables,[],[2541])).
% 61.31/61.30 cnf(2740,plain,
% 61.31/61.30 (P4(x27401,x27401,x27401,x27401)),
% 61.31/61.30 inference(rename_variables,[],[2619])).
% 61.31/61.30 cnf(2745,plain,
% 61.31/61.30 (P1(x27451,x27451,x27452)),
% 61.31/61.30 inference(rename_variables,[],[2531])).
% 61.31/61.30 cnf(2748,plain,
% 61.31/61.30 (P1(x27481,x27481,x27482)),
% 61.31/61.30 inference(rename_variables,[],[2531])).
% 61.31/61.30 cnf(2755,plain,
% 61.31/61.30 (P5(x27551,x27551,x27552,x27551)),
% 61.31/61.30 inference(rename_variables,[],[2504])).
% 61.31/61.30 cnf(2760,plain,
% 61.31/61.30 (P5(x27601,x27602,x27603,x27603)),
% 61.31/61.30 inference(scs_inference,[],[2619,2730,2733,2504,2541,2549,2531,2663,2668,2745,2748,2596,2598,2373,2005,2322,2587,2533,2604,2509,2537,2626,2267,2584,2594,2611,2568,2566,2553,2644,2660,2671,2676,2679,2379,2245,2310,514,1060,188,1071,608,172,636,490,171,154,157,167,287,225,259,152,169,260,227,168,258,153,257,256,164,226,253,155,255,165,254,166,202,200,263,195,194,198,199,204,191,192,228,237])).
% 61.31/61.30 cnf(2763,plain,
% 61.31/61.30 (P9(f28(a1,a1,a1,a1,a1,a1),a1,a1,a1)),
% 61.31/61.30 inference(scs_inference,[],[2619,2730,2733,2504,2541,2549,2531,2663,2668,2745,2748,2596,2598,2373,2005,2322,2587,2533,2604,2509,2537,2626,2267,2584,2594,2611,2568,2566,2553,2644,2660,2671,2676,2679,2379,2245,2310,514,1060,188,1071,608,172,636,490,171,154,157,167,287,225,259,152,169,260,227,168,258,153,257,256,164,226,253,155,255,165,254,166,202,200,263,195,194,198,199,204,191,192,228,237,205])).
% 61.31/61.30 cnf(2769,plain,
% 61.31/61.30 (P9(f28(a1,a1,x27691,x27691,a1,a17),a1,a1,x27691)),
% 61.31/61.30 inference(scs_inference,[],[2619,2730,2733,2504,2541,2549,2531,2663,2668,2745,2748,2596,2598,2373,2005,2322,2587,2533,2604,2509,2537,2626,2267,2584,2594,2611,2568,2566,2553,2644,2660,2671,2676,2679,2379,2445,2245,2310,514,1060,188,1071,608,172,636,490,171,154,157,167,287,225,259,152,169,260,227,168,258,153,257,256,164,226,253,155,255,165,254,166,202,200,263,195,194,198,199,204,191,192,228,237,205,190,224,206])).
% 61.31/61.30 cnf(2771,plain,
% 61.31/61.30 (P10(x27711,x27712,x27712,x27711)),
% 61.31/61.30 inference(scs_inference,[],[2619,2730,2733,2504,2541,2737,2549,2531,2663,2668,2745,2748,2596,2598,2373,2005,2322,2587,2533,2604,2509,2537,2626,2267,2584,2594,2611,2568,2566,2553,2644,2660,2671,2676,2679,2379,2445,2245,2310,514,1060,188,1071,608,172,636,490,171,154,157,167,287,225,259,152,169,260,227,168,258,153,257,256,164,226,253,155,255,165,254,166,202,200,263,195,194,198,199,204,191,192,228,237,205,190,224,206,242])).
% 61.31/61.30 cnf(2772,plain,
% 61.31/61.30 (P8(x27721,x27722,x27722,x27721,x27723,x27724,x27723,x27724)),
% 61.31/61.30 inference(rename_variables,[],[2541])).
% 61.31/61.30 cnf(2774,plain,
% 61.31/61.30 (P2(x27741,x27741,x27741,x27741)),
% 61.31/61.30 inference(scs_inference,[],[2619,2730,2733,2740,2504,2541,2737,2549,2531,2663,2668,2745,2748,2596,2598,2373,2005,2322,2587,2533,2604,2509,2537,2626,2267,2584,2594,2611,2568,2566,2553,2644,2660,2671,2676,2679,2379,2445,2245,2310,514,1060,188,1071,608,172,636,490,171,154,157,167,287,225,259,152,169,260,227,168,258,153,257,256,164,226,253,155,255,165,254,166,202,200,263,195,194,198,199,204,191,192,228,237,205,190,224,206,242,185])).
% 61.31/61.30 cnf(2776,plain,
% 61.31/61.30 (P10(a17,a17,a17,x27761)),
% 61.31/61.30 inference(scs_inference,[],[2619,2730,2733,2740,2504,2541,2737,2549,2531,2663,2668,2745,2748,2596,2598,2373,2005,2322,2587,2533,2604,2509,2537,2626,2267,2584,2594,2611,2568,2566,2553,2644,2660,2671,2676,2679,2379,2445,2245,2310,514,1060,188,1071,608,172,636,490,171,154,157,167,287,225,259,152,169,260,227,168,258,153,257,256,164,226,253,155,255,165,254,166,202,200,263,195,194,198,199,204,191,192,228,237,205,190,224,206,242,185,182])).
% 61.31/61.30 cnf(2777,plain,
% 61.31/61.30 (P4(x27771,x27771,x27771,x27771)),
% 61.31/61.30 inference(rename_variables,[],[2619])).
% 61.31/61.30 cnf(2782,plain,
% 61.31/61.30 (P3(a16,a16,a16)),
% 61.31/61.30 inference(scs_inference,[],[2619,2730,2733,2740,2504,2541,2737,2772,2549,2531,2663,2668,2745,2748,2596,2598,2373,2005,2322,2587,2533,2604,2509,2537,2626,2267,2584,2594,2611,2568,2566,2553,2644,2660,2671,2676,2679,2379,2375,2445,2245,2310,514,1060,188,1071,608,172,636,490,171,154,157,167,287,225,259,152,169,260,227,168,258,153,257,256,164,226,253,155,255,165,254,166,202,200,263,195,194,198,199,204,191,192,228,237,205,190,224,206,242,185,182,193,240])).
% 61.31/61.30 cnf(2784,plain,
% 61.31/61.30 (P1(x27841,x27842,x27841)),
% 61.31/61.30 inference(rename_variables,[],[2375])).
% 61.31/61.30 cnf(2795,plain,
% 61.31/61.31 (P1(x27951,x27952,x27951)),
% 61.31/61.31 inference(rename_variables,[],[2375])).
% 61.31/61.31 cnf(2804,plain,
% 61.31/61.31 (P9(a2,a17,a2,a18)),
% 61.31/61.31 inference(scs_inference,[],[142,2619,2730,2733,2740,2777,2504,2755,2541,2737,2772,2549,2531,2663,2668,2745,2748,2596,2598,2373,2005,2322,2587,2533,2604,2509,2537,2626,2267,2584,2594,2611,2568,2566,2553,2644,2660,2671,2676,2679,2379,2389,2375,2784,2795,2257,2003,2445,2245,2310,143,514,1060,188,1071,608,172,636,490,171,154,157,167,287,225,259,152,169,260,227,168,258,153,257,256,164,226,253,155,255,165,254,166,202,200,263,195,194,198,199,204,191,192,228,237,205,190,224,206,242,185,182,193,240,187,196,207,208,252,604])).
% 61.31/61.31 cnf(2806,plain,
% 61.31/61.31 (P5(a1,a18,a18,a2)),
% 61.31/61.31 inference(scs_inference,[],[142,2619,2730,2733,2740,2777,2504,2755,2541,2737,2772,2549,2531,2663,2668,2745,2748,2596,2598,2373,2005,2322,2587,2533,2604,2509,2537,2626,2267,2584,2594,2611,2568,2566,2553,2644,2660,2671,2676,2679,2379,2389,2375,2784,2795,2257,2003,2445,2245,2310,143,514,1060,188,1071,608,172,636,490,171,154,157,167,287,225,259,152,169,260,227,168,258,153,257,256,164,226,253,155,255,165,254,166,202,200,263,195,194,198,199,204,191,192,228,237,205,190,224,206,242,185,182,193,240,187,196,207,208,252,604,170])).
% 61.31/61.31 cnf(2808,plain,
% 61.31/61.31 (P1(a2,a17,a18)),
% 61.31/61.31 inference(scs_inference,[],[142,2619,2730,2733,2740,2777,2504,2755,2541,2737,2772,2549,2531,2663,2668,2745,2748,2596,2598,2373,2005,2322,2587,2533,2604,2509,2537,2626,2267,2584,2594,2611,2568,2566,2553,2644,2660,2671,2676,2679,2379,2389,2375,2784,2795,2257,2003,2445,2245,2310,143,514,1060,188,1071,608,172,636,490,171,154,157,167,287,225,259,152,169,260,227,168,258,153,257,256,164,226,253,155,255,165,254,166,202,200,263,195,194,198,199,204,191,192,228,237,205,190,224,206,242,185,182,193,240,187,196,207,208,252,604,170,161])).
% 61.31/61.31 cnf(2815,plain,
% 61.31/61.31 (P10(x28151,x28152,x28152,x28151)),
% 61.31/61.31 inference(rename_variables,[],[2771])).
% 61.31/61.31 cnf(2817,plain,
% 61.31/61.31 (P10(a1,a1,a18,a18)),
% 61.31/61.31 inference(scs_inference,[],[2771,2815,864,908])).
% 61.31/61.31 cnf(2818,plain,
% 61.31/61.31 (P10(x28181,x28182,x28182,x28181)),
% 61.31/61.31 inference(rename_variables,[],[2771])).
% 61.31/61.31 cnf(2821,plain,
% 61.31/61.31 (P10(x28211,x28212,x28212,x28211)),
% 61.31/61.31 inference(rename_variables,[],[2771])).
% 61.31/61.31 cnf(2823,plain,
% 61.31/61.31 (P9(a17,a17,a2,a18)),
% 61.31/61.31 inference(scs_inference,[],[2771,2815,2818,2776,864,908,924,604])).
% 61.31/61.31 cnf(2828,plain,
% 61.31/61.31 (P9(a20,a19,a3,a16)),
% 61.31/61.31 inference(scs_inference,[],[2774,2771,2815,2818,2821,2776,864,908,924,604,188,705])).
% 61.31/61.31 cnf(2829,plain,
% 61.31/61.31 (P10(x28291,x28292,x28292,x28291)),
% 61.31/61.31 inference(rename_variables,[],[2771])).
% 61.31/61.31 cnf(2832,plain,
% 61.31/61.31 (P1(f25(x28321,x28322),x28321,x28322)),
% 61.31/61.31 inference(rename_variables,[],[2683])).
% 61.31/61.31 cnf(2835,plain,
% 61.31/61.31 (P1(f25(x28351,x28352),x28351,x28352)),
% 61.31/61.31 inference(rename_variables,[],[2683])).
% 61.31/61.31 cnf(2848,plain,
% 61.31/61.31 (P1(f25(x28481,x28482),x28482,x28481)),
% 61.31/61.31 inference(scs_inference,[],[2774,2771,2815,2818,2821,2776,2681,2683,2832,2719,2763,2723,864,908,924,604,188,705,1060,1071,172,608,170,490,157,154])).
% 61.31/61.31 cnf(2851,plain,
% 61.31/61.31 (P1(f25(x28511,x28512),x28511,x28512)),
% 61.31/61.31 inference(rename_variables,[],[2683])).
% 61.31/61.31 cnf(2853,plain,
% 61.31/61.31 (P5(x28531,x28532,x28533,x28532)),
% 61.31/61.31 inference(scs_inference,[],[2774,2771,2815,2818,2821,2760,2776,2681,2683,2832,2835,2719,2763,2723,864,908,924,604,188,705,1060,1071,172,608,170,490,157,154,287,171])).
% 61.31/61.31 cnf(2857,plain,
% 61.31/61.31 (P1(a17,a2,a18)),
% 61.31/61.31 inference(scs_inference,[],[2774,2771,2815,2818,2821,2760,2776,2681,2806,2808,2683,2832,2835,2719,2763,2723,864,908,924,604,188,705,1060,1071,172,608,170,490,157,154,287,171,225,152])).
% 61.31/61.31 cnf(2859,plain,
% 61.31/61.31 (P10(x28591,x28592,x28591,x28592)),
% 61.31/61.31 inference(scs_inference,[],[2774,2771,2815,2818,2821,2829,2760,2776,2681,2806,2808,2683,2832,2835,2719,2763,2723,864,908,924,604,188,705,1060,1071,172,608,170,490,157,154,287,171,225,152,167])).
% 61.31/61.31 cnf(2863,plain,
% 61.31/61.31 (P1(a2,a18,a17)),
% 61.31/61.31 inference(scs_inference,[],[2774,2771,2815,2818,2821,2829,2760,2776,2681,2806,2808,2685,2683,2832,2835,2719,2763,2723,864,908,924,604,188,705,1060,1071,172,608,170,490,157,154,287,171,225,152,167,169,153])).
% 61.31/61.31 cnf(2865,plain,
% 61.31/61.31 (P4(x28651,a17,a17,x28651)),
% 61.31/61.31 inference(scs_inference,[],[2774,2771,2815,2818,2821,2829,2760,2697,2776,2681,2806,2808,2685,2683,2832,2835,2719,2763,2723,864,908,924,604,188,705,1060,1071,172,608,170,490,157,154,287,171,225,152,167,169,153,168])).
% 61.31/61.31 cnf(2869,plain,
% 61.31/61.31 (P7(x28691,a17,a17,x28691,x28691,x28691,x28691,x28691)),
% 61.31/61.31 inference(scs_inference,[],[2774,2771,2815,2818,2821,2829,2760,2699,2697,2776,2681,2806,2808,2685,2683,2832,2835,2719,2763,2723,864,908,924,604,188,705,1060,1071,172,608,170,490,157,154,287,171,225,152,167,169,153,168,227,259])).
% 61.31/61.31 cnf(2881,plain,
% 61.31/61.31 (P8(a16,a16,x28811,x28812,x28813,x28813,x28811,x28812)),
% 61.31/61.31 inference(scs_inference,[],[2774,2721,2771,2815,2818,2821,2829,2760,2699,2697,2713,2776,2153,2547,2681,2806,2808,2685,2683,2832,2835,2719,2763,2723,864,908,924,604,188,705,1060,1071,172,608,170,490,157,154,287,171,225,152,167,169,153,168,227,259,257,260,258,256,164,226])).
% 61.31/61.31 cnf(2883,plain,
% 61.31/61.31 (P8(x28831,a17,x28831,x28831,x28831,x28831,a17,x28831)),
% 61.31/61.31 inference(scs_inference,[],[2774,2721,2771,2815,2818,2821,2829,2760,2699,2701,2697,2713,2776,2153,2547,2681,2806,2808,2685,2683,2832,2835,2719,2763,2723,864,908,924,604,188,705,1060,1071,172,608,170,490,157,154,287,171,225,152,167,169,153,168,227,259,257,260,258,256,164,226,255])).
% 61.31/61.31 cnf(2889,plain,
% 61.31/61.31 (P9(a2,a17,a18,a2)),
% 61.31/61.31 inference(scs_inference,[],[2774,2721,2771,2815,2818,2821,2829,2760,2699,2701,2697,2713,2776,2153,2547,2681,2804,2806,2808,2685,2683,2832,2835,2719,2763,2723,2601,864,908,924,604,188,705,1060,1071,172,608,170,490,157,154,287,171,225,152,167,169,153,168,227,259,257,260,258,256,164,226,255,155,253,165])).
% 61.31/61.31 cnf(2891,plain,
% 61.31/61.31 (P8(x28911,x28912,x28913,x28913,x28911,x28912,a17,a17)),
% 61.31/61.31 inference(scs_inference,[],[2774,2721,2771,2815,2818,2821,2829,2760,2699,2701,2715,2697,2713,2776,2153,2547,2681,2804,2806,2808,2685,2683,2832,2835,2719,2763,2723,2601,864,908,924,604,188,705,1060,1071,172,608,170,490,157,154,287,171,225,152,167,169,153,168,227,259,257,260,258,256,164,226,255,155,253,165,254])).
% 61.31/61.31 cnf(2895,plain,
% 61.31/61.31 (P1(f15(x28951,a17,x28951,x28951),x28951,a17)),
% 61.31/61.31 inference(scs_inference,[],[2774,2721,2771,2815,2818,2821,2829,2760,2628,2699,2701,2715,2697,2713,2776,2153,2547,2681,2804,2806,2808,2685,2683,2832,2835,2719,2763,2723,2601,864,908,924,604,188,705,1060,1071,172,608,170,490,157,154,287,171,225,152,167,169,153,168,227,259,257,260,258,256,164,226,255,155,253,165,254,166,249])).
% 61.31/61.31 cnf(2896,plain,
% 61.31/61.31 (P10(x28961,x28962,x28962,x28961)),
% 61.31/61.31 inference(rename_variables,[],[2771])).
% 61.31/61.31 cnf(2899,plain,
% 61.31/61.31 (P10(x28991,x28992,x28992,x28991)),
% 61.31/61.31 inference(rename_variables,[],[2771])).
% 61.31/61.31 cnf(2901,plain,
% 61.31/61.31 (P10(x29011,x29012,x29012,x29011)),
% 61.31/61.31 inference(rename_variables,[],[2771])).
% 61.31/61.31 cnf(2903,plain,
% 61.31/61.31 (P10(x29031,x29032,x29032,x29031)),
% 61.31/61.31 inference(rename_variables,[],[2771])).
% 61.31/61.31 cnf(2905,plain,
% 61.31/61.31 (P4(a1,a20,a1,a20)),
% 61.31/61.31 inference(scs_inference,[],[2774,2721,2771,2815,2818,2821,2829,2896,2899,2901,2760,2624,2628,2699,2701,2715,2697,2713,2776,2153,2239,2547,2681,2804,2806,2808,2685,2683,2832,2835,2719,2763,2723,2601,2125,318,267,864,908,924,604,188,705,1060,1071,172,608,170,490,157,154,287,171,225,152,167,169,153,168,227,259,257,260,258,256,164,226,255,155,253,165,254,166,249,117,116,178,184])).
% 61.31/61.31 cnf(2908,plain,
% 61.31/61.31 (P4(a17,x29081,x29081,a17)),
% 61.31/61.31 inference(rename_variables,[],[2697])).
% 61.31/61.31 cnf(2909,plain,
% 61.31/61.31 (P10(x29091,x29092,x29092,x29091)),
% 61.31/61.31 inference(rename_variables,[],[2771])).
% 61.31/61.31 cnf(2912,plain,
% 61.31/61.31 (P10(x29121,x29122,x29122,x29121)),
% 61.31/61.31 inference(rename_variables,[],[2771])).
% 61.31/61.31 cnf(2915,plain,
% 61.31/61.31 (P4(a17,x29151,x29151,a17)),
% 61.31/61.31 inference(rename_variables,[],[2697])).
% 61.31/61.31 cnf(2916,plain,
% 61.31/61.31 (P10(x29161,x29162,x29162,x29161)),
% 61.31/61.31 inference(rename_variables,[],[2771])).
% 61.31/61.31 cnf(2918,plain,
% 61.31/61.31 (P4(x29181,x29181,x29181,f4(x29181,x29181,x29181))),
% 61.31/61.31 inference(scs_inference,[],[2774,2721,2771,2815,2818,2821,2829,2896,2899,2901,2903,2909,2912,2916,2760,2624,2628,2699,2701,2715,2697,2908,2713,2776,2153,2239,2547,2681,2804,2806,2808,2685,2683,2832,2835,2719,2763,2723,2601,2619,2125,318,267,864,908,924,604,188,705,1060,1071,172,608,170,490,157,154,287,171,225,152,167,169,153,168,227,259,257,260,258,256,164,226,255,155,253,165,254,166,249,117,116,178,184,201,174,200,189])).
% 61.31/61.31 cnf(2919,plain,
% 61.31/61.31 (P4(x29191,x29191,x29191,x29191)),
% 61.31/61.31 inference(rename_variables,[],[2619])).
% 61.31/61.31 cnf(2920,plain,
% 61.31/61.31 (P10(x29201,x29202,x29202,x29201)),
% 61.31/61.31 inference(rename_variables,[],[2771])).
% 61.31/61.31 cnf(2924,plain,
% 61.31/61.31 (P10(x29241,x29242,x29242,x29241)),
% 61.31/61.31 inference(rename_variables,[],[2771])).
% 61.31/61.31 cnf(2927,plain,
% 61.31/61.31 (P8(x29271,x29272,x29273,x29274,x29272,x29271,x29274,x29273)),
% 61.31/61.31 inference(rename_variables,[],[2721])).
% 61.31/61.31 cnf(2930,plain,
% 61.31/61.31 (P3(f25(x29301,x29302),x29302,x29301)),
% 61.31/61.31 inference(rename_variables,[],[2719])).
% 61.31/61.31 cnf(2933,plain,
% 61.31/61.31 (P10(x29331,x29332,x29332,x29331)),
% 61.31/61.31 inference(rename_variables,[],[2771])).
% 61.31/61.31 cnf(2936,plain,
% 61.31/61.31 (P10(x29361,x29362,x29362,x29361)),
% 61.31/61.31 inference(rename_variables,[],[2771])).
% 61.31/61.31 cnf(2939,plain,
% 61.31/61.31 (P3(f25(x29391,x29392),x29392,x29391)),
% 61.31/61.31 inference(rename_variables,[],[2719])).
% 61.31/61.31 cnf(2946,plain,
% 61.31/61.31 (P2(f9(x29461,x29461,x29461),x29461,x29461,x29461)),
% 61.31/61.31 inference(scs_inference,[],[142,2774,2630,2721,2771,2815,2818,2821,2829,2896,2899,2901,2903,2909,2912,2916,2920,2924,2933,2936,2760,2624,2628,2699,2701,2715,2697,2908,2915,2713,2776,2153,2239,2547,2681,2782,2804,2806,2808,2685,2683,2832,2835,2719,2930,2543,2199,2763,2723,2563,2601,2619,2125,318,267,864,908,924,604,188,705,1060,1071,172,608,170,490,157,154,287,171,225,152,167,169,153,168,227,259,257,260,258,256,164,226,255,155,253,165,254,166,249,117,116,178,184,201,174,200,189,202,263,159,199,198,228,241,204,192])).
% 61.31/61.31 cnf(2947,plain,
% 61.31/61.31 (P5(x29471,x29471,x29471,x29472)),
% 61.31/61.31 inference(rename_variables,[],[2630])).
% 61.31/61.31 cnf(2948,plain,
% 61.31/61.31 (P10(x29481,x29482,x29482,x29481)),
% 61.31/61.31 inference(rename_variables,[],[2771])).
% 61.31/61.31 cnf(2952,plain,
% 61.31/61.31 (P10(x29521,x29522,x29522,x29521)),
% 61.31/61.31 inference(rename_variables,[],[2771])).
% 61.31/61.31 cnf(2954,plain,
% 61.31/61.31 (P9(f28(a17,a17,a17,a17,a17,a17),a17,x29541,x29541)),
% 61.31/61.31 inference(scs_inference,[],[142,2774,2630,2721,2771,2815,2818,2821,2829,2896,2899,2901,2903,2909,2912,2916,2920,2924,2933,2936,2948,2760,2624,2628,2699,2701,2715,2697,2908,2915,2713,2776,2153,2239,2547,2681,2782,2804,2806,2808,2685,2683,2832,2835,2719,2930,2457,2543,2199,2763,2723,2563,2601,2619,2125,318,267,864,908,924,604,188,705,1060,1071,172,608,170,490,157,154,287,171,225,152,167,169,153,168,227,259,257,260,258,256,164,226,255,155,253,165,254,166,249,117,116,178,184,201,174,200,189,202,263,159,199,198,228,241,204,192,191,180])).
% 61.31/61.31 cnf(2958,plain,
% 61.31/61.31 (P10(x29581,x29582,x29582,x29581)),
% 61.31/61.31 inference(rename_variables,[],[2771])).
% 61.31/61.31 cnf(2960,plain,
% 61.31/61.31 (P5(a18,a18,a2,a17)),
% 61.31/61.31 inference(scs_inference,[],[142,2774,2630,2721,2771,2815,2818,2821,2829,2896,2899,2901,2903,2909,2912,2916,2920,2924,2933,2936,2948,2952,2760,2624,2628,2699,2701,2715,2697,2908,2915,2713,2776,2153,2239,2547,2681,2782,2804,2806,2808,2685,2683,2832,2835,2719,2930,2457,2543,2199,2763,2723,2563,2601,2619,2125,2389,318,267,864,908,924,604,188,705,1060,1071,172,608,170,490,157,154,287,171,225,152,167,169,153,168,227,259,257,260,258,256,164,226,255,155,253,165,254,166,249,117,116,178,184,201,174,200,189,202,263,159,199,198,228,241,204,192,191,180,190,237])).
% 61.31/61.31 cnf(2967,plain,
% 61.31/61.31 (~P9(a19,a1,a18,a19)),
% 61.31/61.31 inference(scs_inference,[],[142,2774,2630,2721,2771,2815,2818,2821,2829,2896,2899,2901,2903,2909,2912,2916,2920,2924,2933,2936,2948,2952,2958,2760,2624,2628,2699,2701,2715,2697,2908,2915,2713,2776,2153,2239,2547,2681,2782,2804,2806,2808,2685,2683,2832,2835,2719,2930,2457,2543,2199,2763,2723,2563,2601,2619,2125,2389,374,318,2445,267,864,908,924,604,188,705,1060,1071,172,608,170,490,157,154,287,171,225,152,167,169,153,168,227,259,257,260,258,256,164,226,255,155,253,165,254,166,249,117,116,178,184,201,174,200,189,202,263,159,199,198,228,241,204,192,191,180,190,237,206,205,183])).
% 61.31/61.31 cnf(2968,plain,
% 61.31/61.31 (P10(x29681,x29682,x29682,x29681)),
% 61.31/61.31 inference(rename_variables,[],[2771])).
% 61.31/61.31 cnf(2973,plain,
% 61.31/61.31 (P10(x29731,x29732,x29732,x29731)),
% 61.31/61.31 inference(rename_variables,[],[2771])).
% 61.31/61.31 cnf(2976,plain,
% 61.31/61.31 (P1(x29761,x29761,x29762)),
% 61.31/61.31 inference(rename_variables,[],[2531])).
% 61.31/61.31 cnf(2982,plain,
% 61.31/61.31 (P2(f25(x29821,x29822),x29821,x29822,x29822)),
% 61.31/61.31 inference(scs_inference,[],[142,2774,2630,2721,2927,2771,2815,2818,2821,2829,2896,2899,2901,2903,2909,2912,2916,2920,2924,2933,2936,2948,2952,2958,2968,2760,2624,2628,2253,2699,2701,2715,2697,2908,2915,2713,2776,2153,2239,2547,2681,2727,2782,2804,2806,2808,2685,2683,2832,2835,2719,2930,2457,2543,2199,2763,2723,2454,2563,2601,2619,2531,2125,2389,374,318,2445,267,864,908,924,604,188,705,1060,1071,172,608,170,490,157,154,287,171,225,152,167,169,153,168,227,259,257,260,258,256,164,226,255,155,253,165,254,166,249,117,116,178,184,201,174,200,189,202,263,159,199,198,228,241,204,192,191,180,190,237,206,205,183,224,181,156,242,185])).
% 61.31/61.31 cnf(2984,plain,
% 61.31/61.31 (P10(x29841,x29842,x29842,x29842)),
% 61.31/61.31 inference(scs_inference,[],[142,2774,2630,2721,2927,2771,2815,2818,2821,2829,2896,2899,2901,2903,2909,2912,2916,2920,2924,2933,2936,2948,2952,2958,2968,2760,2624,2628,2253,2699,2701,2715,2697,2908,2915,2713,2776,2153,2239,2547,2681,2727,2782,2804,2806,2808,2685,2683,2832,2835,2851,2719,2930,2457,2543,2199,2763,2723,2454,2563,2601,2619,2531,2125,2389,374,318,2445,267,864,908,924,604,188,705,1060,1071,172,608,170,490,157,154,287,171,225,152,167,169,153,168,227,259,257,260,258,256,164,226,255,155,253,165,254,166,249,117,116,178,184,201,174,200,189,202,263,159,199,198,228,241,204,192,191,180,190,237,206,205,183,224,181,156,242,185,173])).
% 61.31/61.31 cnf(2988,plain,
% 61.31/61.31 (P4(f25(x29881,x29882),x29881,f25(x29881,x29882),x29882)),
% 61.31/61.31 inference(rename_variables,[],[2685])).
% 61.31/61.31 cnf(2992,plain,
% 61.31/61.31 (P5(x29921,x29921,x29921,x29922)),
% 61.31/61.31 inference(rename_variables,[],[2630])).
% 61.31/61.31 cnf(2995,plain,
% 61.31/61.31 (P10(x29951,x29952,x29952,x29951)),
% 61.31/61.31 inference(rename_variables,[],[2771])).
% 61.31/61.31 cnf(2996,plain,
% 61.31/61.31 (P3(f25(x29961,x29962),x29962,x29961)),
% 61.31/61.31 inference(rename_variables,[],[2719])).
% 61.31/61.31 cnf(2998,plain,
% 61.31/61.31 (P10(f25(x29981,x29981),f25(x29981,x29981),f25(x29981,x29981),x29981)),
% 61.31/61.31 inference(scs_inference,[],[142,2774,2630,2947,2992,2721,2927,2771,2815,2818,2821,2829,2896,2899,2901,2903,2909,2912,2916,2920,2924,2933,2936,2948,2952,2958,2968,2973,2760,2624,2628,2253,2699,2701,2715,2697,2908,2915,2713,2776,2153,2239,2547,2681,2727,2782,2804,2806,2808,2685,2988,2683,2832,2835,2851,2719,2930,2939,2457,2543,2199,2763,2723,2454,2563,2601,2591,2619,2919,2531,2125,2389,374,318,2445,267,864,908,924,604,188,705,1060,1071,172,608,170,490,157,154,287,171,225,152,167,169,153,168,227,259,257,260,258,256,164,226,255,155,253,165,254,166,249,117,116,178,184,201,174,200,189,202,263,159,199,198,228,241,204,192,191,180,190,237,206,205,183,224,181,156,242,185,173,182,193,187,196])).
% 61.31/61.31 cnf(3000,plain,
% 61.31/61.31 (P5(x30001,x30001,x30001,x30002)),
% 61.31/61.31 inference(rename_variables,[],[2630])).
% 61.31/61.31 cnf(3006,plain,
% 61.31/61.31 (P4(x30061,x30061,x30062,x30062)),
% 61.31/61.31 inference(scs_inference,[],[142,2774,2630,2947,2992,3000,2711,2721,2927,2771,2815,2818,2821,2829,2896,2899,2901,2903,2909,2912,2916,2920,2924,2933,2936,2948,2952,2958,2968,2973,2760,2624,2628,2253,2699,2701,2715,2697,2908,2915,2713,2776,2153,2239,2547,2681,2727,2782,2804,2806,2808,2685,2988,2683,2832,2835,2851,2719,2930,2939,2457,2543,2199,2763,2723,2454,2563,2601,2591,2619,2919,2531,2125,2389,374,318,2257,2003,2445,267,864,908,924,604,188,705,1060,1071,172,608,170,490,157,154,287,171,225,152,167,169,153,168,227,259,257,260,258,256,164,226,255,155,253,165,254,166,249,117,116,178,184,201,174,200,189,202,263,159,199,198,228,241,204,192,191,180,190,237,206,205,183,224,181,156,242,185,173,182,193,187,196,208,252])).
% 61.31/61.31 cnf(3009,plain,
% 61.31/61.31 (P8(x30091,x30092,x30091,x30092,x30093,x30094,x30094,x30093)),
% 61.31/61.31 inference(rename_variables,[],[2711])).
% 61.31/61.31 cnf(3015,plain,
% 61.31/61.31 (P10(x30151,x30152,x30152,x30151)),
% 61.31/61.31 inference(rename_variables,[],[2771])).
% 61.31/61.31 cnf(3017,plain,
% 61.31/61.31 (P8(a1,f9(a1,a18,a18),a1,a18,a18,a1,a18,a18)),
% 61.31/61.31 inference(scs_inference,[],[142,2774,2630,2947,2992,3000,2711,2721,2927,2771,2815,2818,2821,2829,2896,2899,2901,2903,2909,2912,2916,2920,2924,2933,2936,2948,2952,2958,2968,2973,2995,3015,2760,2624,2628,2253,2699,2701,2715,2697,2908,2915,2713,2776,2153,2239,2547,2681,2727,2782,2804,2806,2808,2685,2988,2683,2832,2835,2851,2719,2930,2939,2457,2543,2199,2763,2723,2454,2563,2601,2591,528,2619,2919,2531,2125,2389,374,318,2257,2003,2445,267,864,908,924,604,188,705,1060,1071,172,608,170,490,157,154,287,171,225,152,167,169,153,168,227,259,257,260,258,256,164,226,255,155,253,165,254,166,249,117,116,178,184,201,174,200,189,202,263,159,199,198,228,241,204,192,191,180,190,237,206,205,183,224,181,156,242,185,173,182,193,187,196,208,252,222,179,230])).
% 61.31/61.31 cnf(3018,plain,
% 61.31/61.31 (P10(x30181,x30182,x30182,x30181)),
% 61.31/61.31 inference(rename_variables,[],[2771])).
% 61.31/61.31 cnf(3026,plain,
% 61.31/61.31 (P3(f25(x30261,x30262),x30262,x30261)),
% 61.31/61.31 inference(rename_variables,[],[2719])).
% 61.31/61.31 cnf(3032,plain,
% 61.31/61.31 (P3(x30321,x30321,x30321)),
% 61.31/61.31 inference(scs_inference,[],[142,2774,2630,2947,2992,3000,2711,3009,2721,2927,2771,2815,2818,2821,2829,2896,2899,2901,2903,2909,2912,2916,2920,2924,2933,2936,2948,2952,2958,2968,2973,2995,3015,3018,2760,2624,2628,2253,2699,2701,2715,2697,2908,2915,2713,2776,2153,2239,2547,2681,2727,2782,2804,2806,2808,2685,2988,2683,2832,2835,2851,2719,2930,2939,2996,3026,2457,2543,2199,2763,2723,2454,2563,2601,2591,528,2619,2919,2531,2976,2125,2389,374,318,352,2257,2003,2445,2097,2081,267,864,908,924,604,188,705,1060,1071,172,608,170,490,157,154,287,171,225,152,167,169,153,168,227,259,257,260,258,256,164,226,255,155,253,165,254,166,249,117,116,178,184,201,174,200,189,202,263,159,199,198,228,241,204,192,191,180,190,237,206,205,183,224,181,156,242,185,173,182,193,187,196,208,252,222,179,230,177,239,158,194,99,240])).
% 61.31/61.31 cnf(3048,plain,
% 61.31/61.31 (P10(a20,a20,a2,a18)),
% 61.31/61.31 inference(scs_inference,[],[2984,936])).
% 61.31/61.31 cnf(3049,plain,
% 61.31/61.31 (P4(a3,a17,a16,a17)),
% 61.31/61.31 inference(scs_inference,[],[2984,606])).
% 61.31/61.31 cnf(3050,plain,
% 61.31/61.31 (P10(x30501,x30502,x30502,x30502)),
% 61.31/61.31 inference(rename_variables,[],[2984])).
% 61.31/61.31 cnf(3053,plain,
% 61.31/61.31 (P10(x30531,x30532,x30531,x30532)),
% 61.31/61.31 inference(rename_variables,[],[2859])).
% 61.31/61.31 cnf(3055,plain,
% 61.31/61.31 (P9(a17,a2,a2,a18)),
% 61.31/61.31 inference(scs_inference,[],[2859,3053,2984,606,864,604])).
% 61.31/61.31 cnf(3056,plain,
% 61.31/61.31 (P10(x30561,x30562,x30561,x30562)),
% 61.31/61.31 inference(rename_variables,[],[2859])).
% 61.31/61.31 cnf(3061,plain,
% 61.31/61.31 (P10(x30611,x30612,x30611,x30612)),
% 61.31/61.31 inference(rename_variables,[],[2859])).
% 61.31/61.31 cnf(3067,plain,
% 61.31/61.31 (P1(f25(x30671,x30672),x30672,x30671)),
% 61.31/61.31 inference(rename_variables,[],[2848])).
% 61.31/61.31 cnf(3069,plain,
% 61.31/61.31 (P5(x30691,x30692,x30693,x30691)),
% 61.31/61.31 inference(scs_inference,[],[2859,3053,3056,2984,2853,2848,2769,150,606,864,604,188,705,608,1060,170])).
% 61.31/61.31 cnf(3071,plain,
% 61.31/61.31 (P5(x30711,x30712,x30712,x30713)),
% 61.31/61.31 inference(scs_inference,[],[2859,3053,3056,2984,2853,2848,2769,150,606,864,604,188,705,608,1060,170,172])).
% 61.31/61.31 cnf(3074,plain,
% 61.31/61.31 (P1(f25(x30741,x30742),x30742,x30741)),
% 61.31/61.31 inference(rename_variables,[],[2848])).
% 61.31/61.31 cnf(3082,plain,
% 61.31/61.31 (P8(x30821,x30822,x30821,x30823,x30823,x30822,x30823,x30823)),
% 61.31/61.31 inference(scs_inference,[],[2859,3053,3056,2984,2853,2673,2848,3067,2651,2769,2608,150,606,864,604,188,705,608,1060,170,172,1071,157,171,154,225])).
% 61.31/61.31 cnf(3095,plain,
% 61.31/61.31 (P1(a18,a2,a17)),
% 61.31/61.31 inference(scs_inference,[],[2859,3053,3056,2984,2853,2865,2673,2863,2905,2998,2918,2848,3067,3074,2651,2769,2608,150,606,864,604,188,705,608,1060,170,172,1071,157,171,154,225,168,287,169,167,227,152])).
% 61.31/61.31 cnf(3101,plain,
% 61.31/61.31 (P7(x31011,x31011,x31011,x31011,x31011,a17,a17,x31011)),
% 61.31/61.31 inference(scs_inference,[],[2859,3053,3056,2984,2853,2869,2865,2177,2673,2857,2863,2905,2998,2918,2848,3067,3074,2651,2769,2608,150,606,864,604,188,705,608,1060,170,172,1071,157,171,154,225,168,287,169,167,227,152,153,259,257])).
% 61.31/61.31 cnf(3105,plain,
% 61.31/61.31 (P7(x31051,a17,x31051,x31051,a17,x31051,x31051,x31051)),
% 61.31/61.31 inference(scs_inference,[],[2859,3053,3056,2984,2853,2828,2869,2865,2177,2673,2857,2863,2905,2998,2918,2848,3067,3074,2651,2769,2608,150,606,864,604,188,705,608,1060,170,172,1071,157,171,154,225,168,287,169,167,227,152,153,259,257,164,260])).
% 61.31/61.31 cnf(3113,plain,
% 61.31/61.31 (P3(a17,a16,a3)),
% 61.31/61.31 inference(scs_inference,[],[2859,3053,3056,2984,2853,2691,2828,2869,2865,2177,2673,2857,2863,2905,2998,2918,2848,3067,3074,2651,2769,2608,144,150,606,864,604,188,705,608,1060,170,172,1071,157,171,154,225,168,287,169,167,227,152,153,259,257,164,260,256,226,258,155])).
% 61.31/61.31 cnf(3115,plain,
% 61.31/61.31 (P8(x31151,x31152,x31153,x31153,x31152,x31151,a17,a17)),
% 61.31/61.31 inference(scs_inference,[],[2859,3053,3056,2984,2853,2691,2828,2869,2891,2865,2177,2673,2857,2863,2905,2998,2918,2848,3067,3074,2651,2769,2608,144,150,606,864,604,188,705,608,1060,170,172,1071,157,171,154,225,168,287,169,167,227,152,153,259,257,164,260,256,226,258,155,255])).
% 61.31/61.31 cnf(3123,plain,
% 61.31/61.31 (P10(x31231,x31231,x31232,x31231)),
% 61.31/61.31 inference(scs_inference,[],[2859,3053,3056,2984,3050,2853,2691,2828,2869,2883,2891,2865,2177,2673,2857,2863,2905,2998,2918,2848,3067,3074,2651,2769,2608,144,150,606,864,604,188,705,608,1060,170,172,1071,157,171,154,225,168,287,169,167,227,152,153,259,257,164,260,256,226,258,155,255,165,253,254,166])).
% 61.31/61.31 cnf(3135,plain,
% 61.31/61.31 (P1(f5(x31351,x31351,x31352),x31352,x31351)),
% 61.31/61.31 inference(scs_inference,[],[2859,3053,3056,3061,2984,3050,2853,2691,2828,2869,2883,2889,2891,2865,2177,2361,2673,2857,2863,2905,2998,2918,2848,3067,3074,2651,2895,2769,2608,2079,2541,144,150,606,864,604,188,705,608,1060,170,172,1071,157,171,154,225,168,287,169,167,227,152,153,259,257,164,260,256,226,258,155,255,165,253,254,166,162,231,250,264,178])).
% 61.31/61.31 cnf(3137,plain,
% 61.31/61.31 (P4(x31371,x31372,x31371,x31372)),
% 61.31/61.31 inference(scs_inference,[],[3032,2859,3053,3056,3061,2984,3050,2853,2691,2828,2869,2883,2889,2891,2865,2177,2361,2673,2857,2863,2905,2998,2918,2848,3067,3074,2651,2895,2769,2608,2079,2541,144,150,606,864,604,188,705,608,1060,170,172,1071,157,171,154,225,168,287,169,167,227,152,153,259,257,164,260,256,226,258,155,255,165,253,254,166,162,231,250,264,178,174])).
% 61.31/61.31 cnf(3138,plain,
% 61.31/61.31 (P10(x31381,x31382,x31382,x31382)),
% 61.31/61.31 inference(rename_variables,[],[2984])).
% 61.31/61.31 cnf(3141,plain,
% 61.31/61.31 (P10(x31411,x31412,x31411,x31412)),
% 61.31/61.31 inference(rename_variables,[],[2859])).
% 61.31/61.31 cnf(3142,plain,
% 61.31/61.31 (P4(x31421,x31421,x31422,x31422)),
% 61.31/61.31 inference(rename_variables,[],[3006])).
% 61.31/61.31 cnf(3146,plain,
% 61.31/61.31 (P9(f30(x31461,x31461,x31461,x31461,x31461),x31461,x31461,x31461)),
% 61.31/61.31 inference(scs_inference,[],[3032,2859,3053,3056,3061,3141,2984,3050,3006,3142,2853,2691,2828,2869,2883,2889,2891,2865,2177,2361,2673,2857,2863,2905,2998,2918,2848,3067,3074,2651,2895,2769,2608,2079,2541,144,150,606,864,604,188,705,608,1060,170,172,1071,157,171,154,225,168,287,169,167,227,152,153,259,257,164,260,256,226,258,155,255,165,253,254,166,162,231,250,264,178,174,201,179,202])).
% 61.31/61.31 cnf(3147,plain,
% 61.31/61.31 (P10(x31471,x31472,x31471,x31472)),
% 61.31/61.31 inference(rename_variables,[],[2859])).
% 61.31/61.31 cnf(3148,plain,
% 61.31/61.31 (P4(x31481,x31481,x31482,x31482)),
% 61.31/61.31 inference(rename_variables,[],[3006])).
% 61.31/61.31 cnf(3151,plain,
% 61.31/61.31 (P10(x31511,x31512,x31512,x31512)),
% 61.31/61.31 inference(rename_variables,[],[2984])).
% 61.31/61.31 cnf(3154,plain,
% 61.31/61.31 (P10(x31541,x31542,x31542,x31542)),
% 61.31/61.31 inference(rename_variables,[],[2984])).
% 61.31/61.31 cnf(3161,plain,
% 61.31/61.31 (P10(x31611,x31612,x31612,x31612)),
% 61.31/61.31 inference(rename_variables,[],[2984])).
% 61.31/61.31 cnf(3164,plain,
% 61.31/61.31 (P8(x31641,x31642,x31643,x31644,x31642,x31641,x31644,x31643)),
% 61.31/61.31 inference(rename_variables,[],[2721])).
% 61.31/61.31 cnf(3169,plain,
% 61.31/61.31 (P3(f28(x31691,x31691,x31691,x31691,x31691,x31691),x31691,x31691)),
% 61.31/61.31 inference(scs_inference,[],[142,3032,2859,3053,3056,3061,3141,2984,3050,3138,3151,3154,3006,3142,3148,2853,2691,2828,2869,2883,2889,2891,2865,2177,2361,2673,2857,2863,2905,2967,2998,2918,2946,2848,3067,3074,2651,2895,2769,2608,2079,2541,2721,2611,144,150,606,864,604,188,705,608,1060,170,172,1071,157,171,154,225,168,287,169,167,227,152,153,259,257,164,260,256,226,258,155,255,165,253,254,166,162,231,250,264,178,174,201,179,202,195,200,158,198,263,228,204])).
% 61.31/61.31 cnf(3171,plain,
% 61.31/61.31 (~P9(a1,a19,a18,a19)),
% 61.31/61.31 inference(scs_inference,[],[142,3032,2859,3053,3056,3061,3141,2984,3050,3138,3151,3154,3006,3142,3148,2853,2691,2828,2869,2883,2889,2891,2865,2177,2361,2673,2857,2863,2905,2967,2998,2918,2946,2848,3067,3074,2651,2895,2769,2608,2079,2541,2721,2257,2611,144,150,606,864,604,188,705,608,1060,170,172,1071,157,171,154,225,168,287,169,167,227,152,153,259,257,164,260,256,226,258,155,255,165,253,254,166,162,231,250,264,178,174,201,179,202,195,200,158,198,263,228,204,180])).
% 61.31/61.31 cnf(3187,plain,
% 61.31/61.31 (P9(f28(x31871,x31871,x31871,x31871,x31871,x31871),x31871,x31871,x31871)),
% 61.31/61.31 inference(scs_inference,[],[142,3032,2859,3053,3056,3061,3141,3147,2984,3050,3138,3151,3154,3161,3006,3142,3148,2853,2691,2828,2869,2883,2889,2891,2865,2177,2361,2673,2857,2863,2905,2967,2998,2918,2946,2848,3067,3074,2651,2895,2769,2608,2771,2079,2541,2721,3164,2257,2611,144,150,606,864,604,188,705,608,1060,170,172,1071,157,171,154,225,168,287,169,167,227,152,153,259,257,164,260,256,226,258,155,255,165,253,254,166,162,231,250,264,178,174,201,179,202,195,200,158,198,263,228,204,180,199,192,241,191,190,205])).
% 61.31/61.31 cnf(3189,plain,
% 61.31/61.31 (P9(f28(x31891,x31891,x31892,x31892,x31891,a17),x31891,x31891,x31892)),
% 61.31/61.31 inference(scs_inference,[],[142,3032,2859,3053,3056,3061,3141,3147,2984,3050,3138,3151,3154,3161,3006,3142,3148,2853,2691,2828,2869,2883,2889,2891,2865,2177,2361,2673,2857,2863,2905,2967,2998,2918,2946,2848,3067,3074,2651,2895,2769,2608,2771,2079,2541,2721,3164,2257,2611,2445,144,150,606,864,604,188,705,608,1060,170,172,1071,157,171,154,225,168,287,169,167,227,152,153,259,257,164,260,256,226,258,155,255,165,253,254,166,162,231,250,264,178,174,201,179,202,195,200,158,198,263,228,204,180,199,192,241,191,190,205,206])).
% 61.31/61.31 cnf(3192,plain,
% 61.31/61.31 (P10(x31921,x31922,x31921,x31922)),
% 61.31/61.31 inference(rename_variables,[],[2859])).
% 61.31/61.31 cnf(3200,plain,
% 61.31/61.31 (P2(a1,a20,a20,a20)),
% 61.31/61.31 inference(scs_inference,[],[142,3032,2859,3053,3056,3061,3141,3147,3192,2984,3050,3138,3151,3154,3161,3006,3142,3148,2853,2691,2828,2869,2883,2881,2889,2891,2865,2177,2361,2673,2857,2863,2905,2967,2998,2918,2946,2848,3067,3074,2651,2895,2769,2608,2771,2079,2541,2721,3164,265,2257,2611,2445,144,150,606,864,604,188,705,608,1060,170,172,1071,157,171,154,225,168,287,169,167,227,152,153,259,257,164,260,256,226,258,155,255,165,253,254,166,162,231,250,264,178,174,201,179,202,195,200,158,198,263,228,204,180,199,192,241,191,190,205,206,183,224,242,185])).
% 61.31/61.31 cnf(3256,plain,
% 61.31/61.31 (P10(x32561,x32561,x32562,x32561)),
% 61.31/61.31 inference(rename_variables,[],[3123])).
% 61.31/61.31 cnf(3259,plain,
% 61.31/61.31 (P10(x32591,x32591,x32592,x32591)),
% 61.31/61.31 inference(rename_variables,[],[3123])).
% 61.31/61.31 cnf(3262,plain,
% 61.31/61.31 (P10(x32621,x32621,x32622,x32621)),
% 61.31/61.31 inference(rename_variables,[],[3123])).
% 61.31/61.31 cnf(3265,plain,
% 61.31/61.31 (P10(x32651,x32652,x32652,x32652)),
% 61.31/61.31 inference(rename_variables,[],[2984])).
% 61.31/61.31 cnf(3268,plain,
% 61.31/61.31 (P9(f28(x32681,x32681,x32681,x32681,x32681,x32681),x32681,x32681,x32681)),
% 61.31/61.31 inference(rename_variables,[],[3187])).
% 61.31/61.31 cnf(3271,plain,
% 61.31/61.31 (P10(x32711,x32711,x32712,x32711)),
% 61.31/61.31 inference(rename_variables,[],[3123])).
% 61.31/61.31 cnf(3276,plain,
% 61.31/61.31 (P10(x32761,x32761,x32762,x32761)),
% 61.31/61.31 inference(rename_variables,[],[3123])).
% 61.31/61.31 cnf(3282,plain,
% 61.31/61.31 (P1(f5(x32821,x32821,x32822),x32822,x32821)),
% 61.31/61.31 inference(rename_variables,[],[3135])).
% 61.31/61.31 cnf(3285,plain,
% 61.31/61.31 (P10(x32851,x32851,x32852,x32851)),
% 61.31/61.31 inference(rename_variables,[],[3123])).
% 61.31/61.31 cnf(3293,plain,
% 61.31/61.31 (P1(f5(x32931,x32931,x32932),x32932,x32931)),
% 61.31/61.31 inference(rename_variables,[],[3135])).
% 61.31/61.31 cnf(3313,plain,
% 61.31/61.31 (P1(f5(x33131,x33131,x33132),x33132,x33131)),
% 61.31/61.31 inference(rename_variables,[],[3135])).
% 61.31/61.31 cnf(3348,plain,
% 61.31/61.31 (P4(x33481,x33482,x33481,x33482)),
% 61.31/61.31 inference(rename_variables,[],[3137])).
% 61.31/61.31 cnf(3351,plain,
% 61.31/61.31 (P10(x33511,x33512,x33512,x33511)),
% 61.31/61.31 inference(rename_variables,[],[2771])).
% 61.31/61.31 cnf(3357,plain,
% 61.31/61.31 (P10(x33571,x33572,x33572,x33571)),
% 61.31/61.31 inference(rename_variables,[],[2771])).
% 61.31/61.31 cnf(3360,plain,
% 61.31/61.31 (P4(x33601,x33602,x33601,x33602)),
% 61.31/61.31 inference(rename_variables,[],[3137])).
% 61.31/61.31 cnf(3361,plain,
% 61.31/61.31 (P10(x33611,x33611,x33612,x33611)),
% 61.31/61.31 inference(rename_variables,[],[3123])).
% 61.31/61.31 cnf(3367,plain,
% 61.31/61.31 (P3(f28(x33671,x33671,x33671,x33671,x33671,x33671),x33671,x33671)),
% 61.31/61.31 inference(rename_variables,[],[3169])).
% 61.31/61.31 cnf(3370,plain,
% 61.31/61.31 (P4(x33701,x33702,x33701,x33702)),
% 61.31/61.31 inference(rename_variables,[],[3137])).
% 61.31/61.31 cnf(3371,plain,
% 61.31/61.31 (P10(x33711,x33711,x33712,x33711)),
% 61.31/61.31 inference(rename_variables,[],[3123])).
% 61.31/61.31 cnf(3374,plain,
% 61.31/61.31 (P10(x33741,x33742,x33742,x33741)),
% 61.31/61.31 inference(rename_variables,[],[2771])).
% 61.31/61.31 cnf(3377,plain,
% 61.31/61.31 (P10(x33771,x33772,x33772,x33771)),
% 61.31/61.31 inference(rename_variables,[],[2771])).
% 61.31/61.31 cnf(3382,plain,
% 61.31/61.31 (P4(x33821,x33822,x33821,x33822)),
% 61.31/61.31 inference(rename_variables,[],[3137])).
% 61.31/61.31 cnf(3387,plain,
% 61.31/61.31 (P3(f28(x33871,x33871,x33871,x33871,x33871,x33871),x33871,x33871)),
% 61.31/61.31 inference(rename_variables,[],[3169])).
% 61.31/61.31 cnf(3390,plain,
% 61.31/61.31 (P10(x33901,x33901,x33902,x33901)),
% 61.31/61.31 inference(rename_variables,[],[3123])).
% 61.31/61.31 cnf(3393,plain,
% 61.31/61.31 (P8(x33931,x33932,x33931,x33933,x33933,x33932,x33933,x33933)),
% 61.31/61.31 inference(rename_variables,[],[3082])).
% 61.31/61.31 cnf(3401,plain,
% 61.31/61.31 (P10(x34011,x34011,x34012,x34011)),
% 61.31/61.31 inference(rename_variables,[],[3123])).
% 61.31/61.31 cnf(3404,plain,
% 61.31/61.31 (P10(x34041,x34041,x34042,x34041)),
% 61.31/61.31 inference(rename_variables,[],[3123])).
% 61.31/61.31 cnf(3407,plain,
% 61.31/61.31 (P10(x34071,x34072,x34072,x34071)),
% 61.31/61.31 inference(rename_variables,[],[2771])).
% 61.31/61.31 cnf(3417,plain,
% 61.31/61.31 (P5(x34171,x34172,x34172,x34173)),
% 61.31/61.31 inference(rename_variables,[],[3071])).
% 61.31/61.31 cnf(3424,plain,
% 61.31/61.31 (P10(x34241,x34241,x34242,x34241)),
% 61.31/61.31 inference(rename_variables,[],[3123])).
% 61.31/61.31 cnf(3428,plain,
% 61.31/61.31 (P10(x34281,x34281,x34282,x34281)),
% 61.31/61.31 inference(rename_variables,[],[3123])).
% 61.31/61.31 cnf(3457,plain,
% 61.31/61.31 ($false),
% 61.31/61.31 inference(scs_inference,[],[664,3048,3082,3393,3123,3256,3259,3262,3271,3276,3285,3361,3371,3390,3401,3404,3424,3428,3137,3348,3360,3370,3382,3069,3071,3417,2817,2227,2439,3101,3105,3115,2823,2960,3049,3055,3095,3113,3171,3200,3187,3268,3146,3169,3367,3387,3135,3282,3293,3313,3189,2261,3017,2982,2954,2984,3265,2881,2005,2771,3351,3357,3374,3377,3407,2541,350,2537,374,352,2719,2257,2157,3032,151,316,924,908,978,864,514,604,188,877,636,1060,705,608,170,1071,172,490,157,171,225,168,169,154,287,167,227,153,164,152,260,226,257,259,256,255,258,253,165,166,254,1209,177,244,114,178,202,250,174,201,189,179,239,195,158,159,200,263,204,228,198,199,191,241,180,192,190,115,205,175,206,183,243,224,242,185,182,193,196,229,176]),
% 61.31/61.31 ['proof']).
% 61.31/61.31 % SZS output end Proof
% 61.31/61.31 % Total time :60.600000s
%------------------------------------------------------------------------------