%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : GEO644+1 : TPTP v8.2.0. Released v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% Computer : n021.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:03 EDT 2024
% Result : Theorem 60.43s 60.48s
% Output : CNFRefutation 60.51s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.04/0.13 % Problem : GEO644+1 : TPTP v8.2.0. Released v7.5.0.
% 0.04/0.13 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% 0.14/0.35 % Computer : n021.cluster.edu
% 0.14/0.35 % Model : x86_64 x86_64
% 0.14/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.35 % Memory : 8042.1875MB
% 0.14/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.35 % CPULimit : 300
% 0.14/0.35 % WCLimit : 300
% 0.14/0.35 % DateTime : Fri Jun 21 09:30:39 EDT 2024
% 0.14/0.35 % CPUTime :
% 0.53/0.60 start to proof:theBenchmark
% 60.34/60.47 %-------------------------------------------
% 60.34/60.47 % File :CSE---1.7
% 60.34/60.47 % Problem :theBenchmark
% 60.34/60.47 % Transform :cnf
% 60.34/60.47 % Format :tptp:raw
% 60.34/60.47 % Command :java -jar mcs_scs.jar %d %s
% 60.34/60.47
% 60.34/60.47 % Result :Theorem 59.760000s
% 60.34/60.47 % Output :CNFRefutation 59.760000s
% 60.34/60.47 %-------------------------------------------
% 60.43/60.48 %------------------------------------------------------------------------------
% 60.43/60.48 % File : GEO644+1 : TPTP v8.2.0. Released v7.5.0.
% 60.43/60.48 % Domain : Geometry
% 60.43/60.48 % Problem : JGEX problem E006-1
% 60.43/60.48 % Version : [CGZ00] axioms.
% 60.43/60.48 % English :
% 60.43/60.48
% 60.43/60.48 % Refs : [CGZ00] Chou et al. (2000), A Deductive Database Approach to A
% 60.43/60.48 % : [YCG08] Ye et al. (2008), An Introduction to Java Geometry Exp
% 60.43/60.48 % : [Qua20] Quaresma (2020), Email to Geoff Sutcliffe
% 60.43/60.48 % Source : [Qua20]
% 60.43/60.48 % Names : E006-1.p [Qua20]
% 60.43/60.48
% 60.43/60.48 % Status : Theorem
% 60.43/60.48 % Rating : 0.36 v8.2.0, 0.33 v8.1.0, 0.39 v7.5.0
% 60.43/60.48 % Syntax : Number of formulae : 95 ( 0 unt; 0 def)
% 60.43/60.48 % Number of atoms : 292 ( 1 equ)
% 60.43/60.48 % Maximal formula atoms : 9 ( 3 avg)
% 60.43/60.48 % Number of connectives : 204 ( 7 ~; 0 |; 102 &)
% 60.43/60.48 % ( 0 <=>; 95 =>; 0 <=; 0 <~>)
% 60.43/60.48 % Maximal formula depth : 17 ( 9 avg)
% 60.43/60.48 % Maximal term depth : 1 ( 1 avg)
% 60.43/60.48 % Number of predicates : 12 ( 11 usr; 0 prp; 2-8 aty)
% 60.43/60.48 % Number of functors : 0 ( 0 usr; 0 con; --- aty)
% 60.43/60.48 % Number of variables : 530 ( 510 !; 20 ?)
% 60.43/60.48 % SPC : FOF_THM_RFO_SEQ
% 60.43/60.48
% 60.43/60.48 % Comments : Taken from JGEX [YCG08], converted by Pedro Quaresma.
% 60.43/60.48 %------------------------------------------------------------------------------
% 60.43/60.48 include('Axioms/GEO012+0.ax').
% 60.43/60.48 %------------------------------------------------------------------------------
% 60.43/60.48 fof(exemplo6GDDFULLmoreE0061,conjecture,
% 60.43/60.48 ! [A,B,C,D,E,F,G,H] :
% 60.43/60.48 ( ( para(B,C,A,D)
% 60.43/60.48 & para(A,B,C,D)
% 60.43/60.48 & midp(E,C,D)
% 60.43/60.48 & midp(F,B,A)
% 60.43/60.48 & coll(G,A,C)
% 60.43/60.48 & coll(G,D,F)
% 60.43/60.48 & coll(H,B,E)
% 60.43/60.48 & coll(H,A,C) )
% 60.43/60.48 => cong(A,G,G,H) ) ).
% 60.43/60.48
% 60.43/60.48 %------------------------------------------------------------------------------
% 60.43/60.48 %-------------------------------------------
% 60.43/60.48 % Proof found
% 60.43/60.48 % SZS status Theorem for theBenchmark
% 60.43/60.48 % SZS output start Proof
% 60.45/60.49 %ClaNum:263(EqnAxiom:141)
% 60.45/60.49 %VarNum:1613(SingletonVarNum:590)
% 60.45/60.49 %MaxLitNum:5
% 60.45/60.49 %MaxfuncDepth:1
% 60.45/60.49 %SharedTerms:17
% 60.45/60.49 %goalClause: 142 143 144 145 146 147 148 149 150
% 60.45/60.49 %singleGoalClaCount:9
% 60.45/60.49 [142]P1(a1,a2,a15)
% 60.45/60.49 [143]P1(a1,a17,a18)
% 60.45/60.49 [144]P1(a20,a2,a15)
% 60.45/60.49 [145]P1(a20,a16,a19)
% 60.45/60.49 [146]P3(a19,a15,a17)
% 60.45/60.49 [147]P3(a18,a16,a2)
% 60.45/60.49 [148]P9(a2,a16,a15,a17)
% 60.45/60.49 [149]P9(a16,a15,a2,a17)
% 60.45/60.49 [150]~P4(a2,a1,a1,a20)
% 60.45/60.49 [151]~P1(x1512,x1511,x1513)+P1(x1511,x1512,x1513)
% 60.45/60.49 [152]~P1(x1521,x1523,x1522)+P1(x1521,x1522,x1523)
% 60.45/60.49 [153]~P3(x1531,x1532,x1533)+P1(x1531,x1532,x1533)
% 60.45/60.49 [154]~P3(x1541,x1543,x1542)+P3(x1541,x1542,x1543)
% 60.45/60.49 [156]~P3(x1561,x1562,x1563)+P4(x1561,x1562,x1561,x1563)
% 60.45/60.49 [160]~P9(x1601,x1602,x1601,x1603)+P1(x1601,x1602,x1603)
% 60.45/60.49 [226]~P4(x2261,x2262,x2261,x2263)+P8(x2261,x2262,x2262,x2263,x2262,x2263,x2261,x2263)
% 60.45/60.49 [163]~P9(x1633,x1634,x1631,x1632)+P9(x1631,x1632,x1633,x1634)
% 60.45/60.49 [164]~P9(x1641,x1642,x1644,x1643)+P9(x1641,x1642,x1643,x1644)
% 60.45/60.49 [165]~P10(x1653,x1654,x1651,x1652)+P10(x1651,x1652,x1653,x1654)
% 60.45/60.49 [166]~P10(x1661,x1662,x1664,x1663)+P10(x1661,x1662,x1663,x1664)
% 60.45/60.49 [167]~P4(x1673,x1674,x1671,x1672)+P4(x1671,x1672,x1673,x1674)
% 60.45/60.49 [168]~P4(x1681,x1682,x1684,x1683)+P4(x1681,x1682,x1683,x1684)
% 60.45/60.49 [169]~P5(x1692,x1691,x1693,x1694)+P5(x1691,x1692,x1693,x1694)
% 60.45/60.49 [170]~P5(x1701,x1703,x1702,x1704)+P5(x1701,x1702,x1703,x1704)
% 60.45/60.49 [171]~P5(x1711,x1712,x1714,x1713)+P5(x1711,x1712,x1713,x1714)
% 60.45/60.49 [224]~P5(x2242,x2243,x2241,x2244)+P8(x2241,x2242,x2241,x2243,x2244,x2242,x2244,x2243)
% 60.45/60.49 [187]~P2(x1874,x1871,x1872,x1873)+P10(f7(x1871,x1872,x1873,x1874),x1871,x1871,x1874)
% 60.45/60.49 [202]P4(x2021,x2022,x2023,x2024)+~P6(x2021,x2022,x2025,x2023,x2024,x2026)
% 60.45/60.49 [214]~P11(x2144,x2145,x2146,x2141,x2142,x2143)+P11(x2141,x2142,x2143,x2144,x2145,x2146)
% 60.45/60.49 [215]~P11(x2152,x2151,x2153,x2155,x2154,x2156)+P11(x2151,x2152,x2153,x2154,x2155,x2156)
% 60.45/60.49 [216]~P11(x2161,x2163,x2162,x2164,x2166,x2165)+P11(x2161,x2162,x2163,x2164,x2165,x2166)
% 60.45/60.49 [217]~P6(x2174,x2175,x2176,x2171,x2172,x2173)+P6(x2171,x2172,x2173,x2174,x2175,x2176)
% 60.45/60.49 [218]~P6(x2182,x2181,x2183,x2185,x2184,x2186)+P6(x2181,x2182,x2183,x2184,x2185,x2186)
% 60.45/60.49 [219]~P6(x2191,x2193,x2192,x2194,x2196,x2195)+P6(x2191,x2192,x2193,x2194,x2195,x2196)
% 60.45/60.49 [225]~P9(x2251,x2252,x2255,x2256)+P8(x2251,x2252,x2253,x2254,x2255,x2256,x2253,x2254)
% 60.45/60.49 [231]~P11(x2311,x2312,x2313,x2314,x2315,x2316)+P8(x2311,x2312,x2312,x2313,x2314,x2315,x2315,x2316)
% 60.45/60.49 [232]~P11(x2321,x2322,x2323,x2324,x2325,x2326)+P7(x2321,x2322,x2321,x2323,x2324,x2325,x2324,x2326)
% 60.45/60.49 [233]~P8(x2331,x2332,x2335,x2336,x2333,x2334,x2335,x2336)+P9(x2331,x2332,x2333,x2334)
% 60.45/60.49 [252]~P8(x2525,x2526,x2527,x2528,x2521,x2522,x2523,x2524)+P8(x2521,x2522,x2523,x2524,x2525,x2526,x2527,x2528)
% 60.45/60.49 [253]~P8(x2533,x2534,x2531,x2532,x2537,x2538,x2535,x2536)+P8(x2531,x2532,x2533,x2534,x2535,x2536,x2537,x2538)
% 60.45/60.49 [254]~P8(x2542,x2541,x2543,x2544,x2545,x2546,x2547,x2548)+P8(x2541,x2542,x2543,x2544,x2545,x2546,x2547,x2548)
% 60.45/60.49 [255]~P8(x2551,x2552,x2555,x2556,x2553,x2554,x2557,x2558)+P8(x2551,x2552,x2553,x2554,x2555,x2556,x2557,x2558)
% 60.45/60.49 [256]~P7(x2565,x2566,x2567,x2568,x2561,x2562,x2563,x2564)+P7(x2561,x2562,x2563,x2564,x2565,x2566,x2567,x2568)
% 60.45/60.49 [257]~P7(x2573,x2574,x2571,x2572,x2577,x2578,x2575,x2576)+P7(x2571,x2572,x2573,x2574,x2575,x2576,x2577,x2578)
% 60.45/60.49 [258]~P7(x2582,x2581,x2583,x2584,x2585,x2586,x2587,x2588)+P7(x2581,x2582,x2583,x2584,x2585,x2586,x2587,x2588)
% 60.45/60.49 [259]~P7(x2591,x2592,x2595,x2596,x2593,x2594,x2597,x2598)+P7(x2591,x2592,x2593,x2594,x2595,x2596,x2597,x2598)
% 60.45/60.49 [161]~P1(x1611,x1612,x1613)+~P4(x1611,x1612,x1611,x1613)+P3(x1611,x1612,x1613)
% 60.45/60.49 [235]P4(x2351,x2352,x2351,x2353)+~P8(x2351,x2352,x2352,x2353,x2352,x2353,x2351,x2353)+P1(x2351,x2352,x2353)
% 60.45/60.49 [176]~P10(x1761,x1762,x1762,x1763)+~P4(x1762,x1761,x1762,x1763)+P1(x1761,x1762,f3(x1761,x1763,x1762))
% 60.45/60.49 [188]~P10(x1882,x1881,x1881,x1883)+~P4(x1881,x1882,x1881,x1883)+P4(x1881,x1882,x1881,f3(x1882,x1883,x1881))
% 60.45/60.49 [155]~P1(x1553,x1554,x1551)+P1(x1551,x1552,x1553)+~P1(x1553,x1554,x1552)
% 60.45/60.49 [172]~P2(x1724,x1721,x1722,x1723)+P10(x1721,x1722,x1722,x1723)+~P1(x1724,x1721,x1723)
% 60.45/60.49 [173]~P10(x1731,x1734,x1732,x1733)+P4(x1731,x1732,x1731,x1733)+~P3(x1734,x1732,x1733)
% 60.45/60.49 [174]~P10(x1741,x1743,x1743,x1744)+P4(x1741,x1742,x1743,x1742)+~P3(x1742,x1741,x1744)
% 60.45/60.49 [181]~P4(x1811,x1814,x1812,x1814)+~P4(x1811,x1813,x1812,x1813)+P10(x1811,x1812,x1813,x1814)
% 60.45/60.49 [184]~P4(x1841,x1842,x1841,x1844)+~P4(x1841,x1842,x1841,x1843)+P2(x1841,x1842,x1843,x1844)
% 60.45/60.49 [230]~P9(x2301,x2304,x2303,x2302)+~P5(x2301,x2304,x2303,x2302)+P8(x2301,x2302,x2303,x2302,x2303,x2302,x2303,x2304)
% 60.45/60.49 [234]~P8(x2341,x2343,x2341,x2344,x2342,x2343,x2342,x2344)+P1(x2341,x2342,x2343)+P5(x2343,x2344,x2341,x2342)
% 60.45/60.49 [236]~P1(x2363,x2364,x2362)+~P8(x2363,x2361,x2363,x2362,x2364,x2361,x2364,x2362)+P5(x2361,x2362,x2363,x2364)
% 60.45/60.49 [238]P10(x2381,x2382,x2383,x2384)+~P8(x2381,x2382,x2383,x2384,x2383,x2384,x2381,x2382)+P9(x2381,x2382,x2383,x2384)
% 60.45/60.49 [177]~P10(x1771,x1774,x1772,x1773)+~P10(x1772,x1774,x1771,x1773)+P1(f4(x1771,x1772,x1773),x1773,x1772)
% 60.45/60.49 [178]~P10(x1781,x1784,x1782,x1783)+~P10(x1782,x1784,x1781,x1783)+P1(f5(x1781,x1782,x1783),x1783,x1781)
% 60.45/60.49 [189]~P10(x1891,x1894,x1892,x1893)+~P10(x1892,x1894,x1891,x1893)+P10(x1891,f4(x1891,x1892,x1893),x1893,x1892)
% 60.45/60.49 [190]~P10(x1901,x1904,x1902,x1903)+~P10(x1902,x1904,x1901,x1903)+P10(x1901,f5(x1902,x1901,x1903),x1903,x1902)
% 60.45/60.49 [191]~P10(x1911,x1913,x1913,x1912)+~P5(x1911,x1912,x1913,x1914)+P2(f8(x1911,x1912,x1913),x1911,x1912,x1913)
% 60.45/60.49 [193]~P10(x1933,x1934,x1932,x1931)+~P4(x1933,x1932,x1933,x1931)+P1(x1931,x1932,f22(x1932,x1931,x1933,x1934))
% 60.45/60.49 [194]~P10(x1943,x1944,x1941,x1942)+~P4(x1943,x1941,x1943,x1942)+P1(f22(x1941,x1942,x1943,x1944),x1943,x1944)
% 60.45/60.49 [245]~P4(x2453,x2452,x2453,x2451)+~P8(x2452,x2453,x2453,x2454,x2453,x2454,x2453,x2451)+P1(x2451,x2452,f23(x2452,x2451,x2453,x2454))
% 60.45/60.49 [246]~P10(x2463,x2464,x2462,x2461)+~P8(x2462,x2463,x2463,x2464,x2463,x2464,x2463,x2461)+P1(x2461,x2462,f24(x2462,x2461,x2463,x2464))
% 60.45/60.49 [247]~P10(x2473,x2472,x2472,x2471)+~P8(x2474,x2473,x2472,x2473,x2472,x2473,x2471,x2473)+P1(f14(x2471,x2472,x2473,x2474),x2473,x2474)
% 60.45/60.49 [248]~P10(x2483,x2482,x2482,x2481)+~P8(x2484,x2483,x2482,x2483,x2482,x2483,x2481,x2483)+P1(f14(x2481,x2482,x2483,x2484),x2481,x2482)
% 60.45/60.49 [249]~P4(x2493,x2491,x2493,x2492)+~P8(x2491,x2493,x2493,x2494,x2493,x2494,x2493,x2492)+P1(f23(x2491,x2492,x2493,x2494),x2493,x2494)
% 60.45/60.49 [250]~P10(x2503,x2504,x2501,x2502)+~P8(x2501,x2503,x2503,x2504,x2503,x2504,x2503,x2502)+P1(f24(x2501,x2502,x2503,x2504),x2503,x2504)
% 60.45/60.49 [157]~P3(x1575,x1571,x1573)+P9(x1571,x1572,x1573,x1574)+~P3(x1575,x1572,x1574)
% 60.45/60.49 [158]~P3(x1581,x1585,x1583)+P9(x1581,x1582,x1583,x1584)+~P3(x1582,x1585,x1584)
% 60.45/60.49 [185]~P5(x1855,x1851,x1852,x1853)+P5(x1851,x1852,x1853,x1854)+~P5(x1855,x1851,x1852,x1854)
% 60.45/60.49 [227]~P3(x2275,x2272,x2273)+~P2(x2274,x2271,x2272,x2273)+P8(x2271,x2272,x2271,x2273,x2274,x2272,x2274,x2275)
% 60.45/60.49 [229]~P2(x2295,x2291,x2293,x2294)+P8(x2291,x2292,x2291,x2293,x2294,x2291,x2294,x2293)+~P10(x2295,x2291,x2291,x2292)
% 60.45/60.49 [242]~P8(x2422,x2423,x2422,x2424,x2425,x2422,x2425,x2424)+P10(x2421,x2422,x2422,x2423)+~P2(x2421,x2422,x2424,x2425)
% 60.45/60.49 [197]~P1(x1972,x1974,x1975)+~P10(x1971,x1973,x1973,x1972)+P1(f12(x1971,x1972,x1973,x1974,x1975),x1974,x1975)
% 60.45/60.49 [198]~P1(x1982,x1984,x1985)+~P10(x1981,x1983,x1983,x1982)+P10(f12(x1981,x1982,x1983,x1984,x1985),x1981,x1984,x1985)
% 60.45/60.49 [199]~P10(x1993,x1994,x1994,x1991)+~P4(x1991,x1992,x1991,x1995)+P4(x1991,x1992,x1991,f27(x1993,x1994,x1992,x1995,x1991))
% 60.45/60.49 [200]~P10(x2003,x2001,x2001,x2005)+~P4(x2005,x2002,x2005,x2004)+P4(x2001,x2002,x2001,f27(x2003,x2001,x2002,x2004,x2005))
% 60.45/60.49 [201]~P10(x2011,x2012,x2012,x2015)+~P4(x2015,x2013,x2015,x2014)+P9(f27(x2011,x2012,x2013,x2014,x2015),x2013,x2011,x2012)
% 60.45/60.50 [244]~P8(x2441,x2443,x2442,x2443,x2441,x2444,x2442,x2445)+P1(x2441,x2442,x2443)+P5(x2444,x2442,x2443,f26(x2441,x2442,x2443,x2444))
% 60.45/60.50 [260]~P8(x2601,x2603,x2602,x2603,x2601,x2604,x2602,x2605)+P1(x2601,x2602,x2603)+P8(x2601,x2603,x2602,x2603,x2601,f26(x2601,x2602,x2603,x2604),x2602,f26(x2601,x2602,x2603,x2604))
% 60.45/60.50 [179]~P9(x1791,x1792,x1795,x1796)+P9(x1791,x1792,x1793,x1794)+~P9(x1795,x1796,x1793,x1794)
% 60.45/60.50 [180]~P10(x1801,x1802,x1805,x1806)+P9(x1801,x1802,x1803,x1804)+~P10(x1805,x1806,x1803,x1804)
% 60.45/60.50 [182]~P10(x1825,x1826,x1823,x1824)+P10(x1821,x1822,x1823,x1824)+~P9(x1821,x1822,x1825,x1826)
% 60.45/60.50 [183]~P4(x1831,x1832,x1835,x1836)+P4(x1831,x1832,x1833,x1834)+~P4(x1835,x1836,x1833,x1834)
% 60.45/60.50 [220]~P4(x2201,x2202,x2204,x2205)+~P11(x2201,x2202,x2203,x2204,x2205,x2206)+P6(x2201,x2202,x2203,x2204,x2205,x2206)
% 60.45/60.50 [223]~P3(x2234,x2235,x2236)+~P3(x2231,x2232,x2233)+P7(x2231,x2232,x2232,x2233,x2234,x2235,x2235,x2236)
% 60.45/60.50 [203]~P3(x2036,x2033,x2034)+~P3(x2035,x2031,x2032)+P3(f25(x2031,x2032,x2033,x2034,x2035,x2036),x2031,x2034)
% 60.45/60.50 [204]~P3(x2046,x2043,x2044)+~P3(x2045,x2041,x2042)+P9(f25(x2041,x2042,x2043,x2044,x2045,x2046),x2046,x2041,x2043)
% 60.45/60.50 [205]~P3(x2056,x2053,x2054)+~P3(x2055,x2051,x2052)+P9(f25(x2051,x2052,x2053,x2054,x2055,x2056),x2055,x2052,x2054)
% 60.45/60.50 [240]~P8(x2401,x2402,x2403,x2404,x2405,x2406,x2407,x2408)+P9(x2401,x2402,x2403,x2404)+~P9(x2405,x2406,x2407,x2408)
% 60.45/60.50 [241]~P8(x2411,x2412,x2413,x2414,x2415,x2416,x2417,x2418)+P10(x2411,x2412,x2413,x2414)+~P10(x2415,x2416,x2417,x2418)
% 60.45/60.50 [243]~P7(x2431,x2432,x2433,x2434,x2435,x2436,x2437,x2438)+P4(x2431,x2432,x2433,x2434)+~P4(x2435,x2436,x2437,x2438)
% 60.45/60.50 [221]~P11(x2211,x2212,x2213,x2217,x2218,x2219)+P11(x2211,x2212,x2213,x2214,x2215,x2216)+~P11(x2217,x2218,x2219,x2214,x2215,x2216)
% 60.45/60.50 [222]~P6(x2221,x2222,x2223,x2227,x2228,x2229)+P6(x2221,x2222,x2223,x2224,x2225,x2226)+~P6(x2227,x2228,x2229,x2224,x2225,x2226)
% 60.45/60.50 [262]~P8(x2621,x2622,x2623,x2624,x2629,x26210,x26211,x26212)+P8(x2621,x2622,x2623,x2624,x2625,x2626,x2627,x2628)+~P8(x2629,x26210,x26211,x26212,x2625,x2626,x2627,x2628)
% 60.45/60.50 [263]~P7(x2631,x2632,x2633,x2634,x2639,x26310,x26311,x26312)+P7(x2631,x2632,x2633,x2634,x2635,x2636,x2637,x2638)+~P7(x2639,x26310,x26311,x26312,x2635,x2636,x2637,x2638)
% 60.45/60.50 [195]~P4(x1952,x1951,x1954,x1951)+~P5(x1952,x1954,x1951,x1953)+P10(x1951,x1952,x1952,x1953)+~P4(x1952,x1953,x1954,x1953)
% 60.45/60.50 [162]~P1(x1621,x1622,x1623)+~P9(x1624,x1621,x1625,x1623)+P3(x1621,x1622,x1623)+~P3(x1624,x1622,x1625)
% 60.45/60.50 [175]~P9(x1754,x1753,x1755,x1752)+~P9(x1754,x1752,x1755,x1753)+P3(x1751,x1752,x1753)+~P3(x1751,x1754,x1755)
% 60.45/60.50 [196]~P4(x1965,x1961,x1965,x1963)+~P4(x1965,x1961,x1965,x1962)+P5(x1961,x1962,x1963,x1964)+~P4(x1965,x1961,x1965,x1964)
% 60.45/60.50 [228]~P1(x2281,x2284,x2285)+~P1(x2281,x2282,x2283)+~P9(x2282,x2284,x2283,x2285)+P7(x2281,x2282,x2282,x2283,x2281,x2284,x2284,x2285)
% 60.45/60.50 [239]~P1(x2391,x2392,x2393)+~P8(x2395,x2392,x2395,x2393,x2394,x2392,x2394,x2391)+P3(x2391,x2392,x2393)+~P2(x2394,x2395,x2392,x2393)
% 60.45/60.50 [186]~P10(x1863,x1861,x1863,x1865)+~P10(x1861,x1862,x1861,x1863)+~P3(x1864,x1862,x1865)+P3(f6(x1861,x1862,x1863),x1861,x1863)
% 60.45/60.50 [192]~P5(x1921,x1922,x1923,x1925)+~P9(x1921,x1922,x1923,x1925)+~P3(x1924,x1921,x1922)+P2(f9(x1921,x1922,x1923),x1921,x1922,x1923)
% 60.45/60.50 [261]~P8(x2611,x2613,x2612,x2613,x2614,x2616,x2615,x2616)+~P8(x2611,x2612,x2612,x2613,x2614,x2615,x2615,x2616)+P1(x2611,x2612,x2613)+P11(x2611,x2612,x2613,x2614,x2615,x2616)
% 60.45/60.50 [251]~P5(x2511,x2512,x2515,x2514)+~P5(x2511,x2512,x2515,x2513)+~P8(x2515,x2511,x2515,x2512,x2516,x2513,x2516,x2514)+P4(x2511,x2512,x2513,x2514)+~P5(x2511,x2512,x2515,x2516)
% 60.45/60.50 [206]~P1(x2062,x2063,x2064)+~P1(x2061,x2064,x2066)+~P1(x2061,x2063,x2065)+~P9(x2063,x2064,x2065,x2066)+P1(x2061,x2062,f13(x2063,x2064,x2065,x2066,x2061,x2062))
% 60.45/60.50 [207]~P1(x2076,x2071,x2072)+~P1(x2075,x2072,x2074)+~P1(x2075,x2071,x2073)+~P9(x2071,x2072,x2073,x2074)+P1(f13(x2071,x2072,x2073,x2074,x2075,x2076),x2073,x2074)
% 60.45/60.50 [208]~P1(x2083,x2084,x2085)+~P3(x2086,x2081,x2082)+~P9(x2081,x2083,x2085,x2086)+~P9(x2081,x2083,x2082,x2084)+P1(f28(x2081,x2082,x2083,x2084,x2085,x2086),x2086,x2085)
% 60.45/60.50 [209]~P1(x2093,x2094,x2095)+~P3(x2096,x2091,x2092)+~P9(x2091,x2093,x2095,x2096)+~P9(x2091,x2093,x2092,x2094)+P1(f28(x2091,x2092,x2093,x2094,x2095,x2096),x2091,x2094)
% 60.45/60.50 [210]~P4(x2102,x2103,x2102,x2104)+~P4(x2101,x2103,x2101,x2106)+~P2(x2101,x2103,x2104,x2105)+E(x2101,x2102)+P1(f10(x2103,x2104,x2105,x2106,x2101,x2102),x2103,x2105)
% 60.45/60.50 [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),x2114,x2116)
% 60.45/60.50 [212]~P4(x2122,x2123,x2122,x2124)+~P4(x2121,x2123,x2121,x2126)+~P2(x2121,x2123,x2124,x2125)+E(x2121,x2122)+P4(f10(x2123,x2124,x2125,x2126,x2121,x2122),x2122,x2122,x2123)
% 60.45/60.50 [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)
% 60.45/60.50 [159]~P1(x1593,x1591,x1594)+~P1(x1595,x1591,x1594)+~P3(x1596,x1595,x1593)+~P3(x1597,x1591,x1594)+P3(f21(x1591,x1592),x1591,x1592)
% 60.45/60.50 %EqnAxiom
% 60.45/60.50 [1]E(x11,x11)
% 60.45/60.50 [2]E(x22,x21)+~E(x21,x22)
% 60.45/60.50 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 60.45/60.50 [4]~E(x41,x42)+E(f21(x41,x43),f21(x42,x43))
% 60.45/60.50 [5]~E(x51,x52)+E(f21(x53,x51),f21(x53,x52))
% 60.45/60.50 [6]~E(x61,x62)+E(f3(x61,x63,x64),f3(x62,x63,x64))
% 60.45/60.50 [7]~E(x71,x72)+E(f3(x73,x71,x74),f3(x73,x72,x74))
% 60.45/60.50 [8]~E(x81,x82)+E(f3(x83,x84,x81),f3(x83,x84,x82))
% 60.45/60.50 [9]~E(x91,x92)+E(f4(x91,x93,x94),f4(x92,x93,x94))
% 60.45/60.50 [10]~E(x101,x102)+E(f4(x103,x101,x104),f4(x103,x102,x104))
% 60.45/60.50 [11]~E(x111,x112)+E(f4(x113,x114,x111),f4(x113,x114,x112))
% 60.45/60.50 [12]~E(x121,x122)+E(f5(x121,x123,x124),f5(x122,x123,x124))
% 60.45/60.50 [13]~E(x131,x132)+E(f5(x133,x131,x134),f5(x133,x132,x134))
% 60.45/60.50 [14]~E(x141,x142)+E(f5(x143,x144,x141),f5(x143,x144,x142))
% 60.45/60.50 [15]~E(x151,x152)+E(f6(x151,x153,x154),f6(x152,x153,x154))
% 60.45/60.50 [16]~E(x161,x162)+E(f6(x163,x161,x164),f6(x163,x162,x164))
% 60.45/60.50 [17]~E(x171,x172)+E(f6(x173,x174,x171),f6(x173,x174,x172))
% 60.45/60.50 [18]~E(x181,x182)+E(f7(x181,x183,x184,x185),f7(x182,x183,x184,x185))
% 60.45/60.50 [19]~E(x191,x192)+E(f7(x193,x191,x194,x195),f7(x193,x192,x194,x195))
% 60.45/60.50 [20]~E(x201,x202)+E(f7(x203,x204,x201,x205),f7(x203,x204,x202,x205))
% 60.45/60.50 [21]~E(x211,x212)+E(f7(x213,x214,x215,x211),f7(x213,x214,x215,x212))
% 60.45/60.50 [22]~E(x221,x222)+E(f26(x221,x223,x224,x225),f26(x222,x223,x224,x225))
% 60.45/60.50 [23]~E(x231,x232)+E(f26(x233,x231,x234,x235),f26(x233,x232,x234,x235))
% 60.45/60.50 [24]~E(x241,x242)+E(f26(x243,x244,x241,x245),f26(x243,x244,x242,x245))
% 60.45/60.50 [25]~E(x251,x252)+E(f26(x253,x254,x255,x251),f26(x253,x254,x255,x252))
% 60.45/60.50 [26]~E(x261,x262)+E(f23(x261,x263,x264,x265),f23(x262,x263,x264,x265))
% 60.45/60.50 [27]~E(x271,x272)+E(f23(x273,x271,x274,x275),f23(x273,x272,x274,x275))
% 60.45/60.50 [28]~E(x281,x282)+E(f23(x283,x284,x281,x285),f23(x283,x284,x282,x285))
% 60.45/60.50 [29]~E(x291,x292)+E(f23(x293,x294,x295,x291),f23(x293,x294,x295,x292))
% 60.45/60.50 [30]~E(x301,x302)+E(f24(x301,x303,x304,x305),f24(x302,x303,x304,x305))
% 60.45/60.50 [31]~E(x311,x312)+E(f24(x313,x311,x314,x315),f24(x313,x312,x314,x315))
% 60.45/60.50 [32]~E(x321,x322)+E(f24(x323,x324,x321,x325),f24(x323,x324,x322,x325))
% 60.45/60.50 [33]~E(x331,x332)+E(f24(x333,x334,x335,x331),f24(x333,x334,x335,x332))
% 60.45/60.50 [34]~E(x341,x342)+E(f8(x341,x343,x344),f8(x342,x343,x344))
% 60.45/60.50 [35]~E(x351,x352)+E(f8(x353,x351,x354),f8(x353,x352,x354))
% 60.45/60.50 [36]~E(x361,x362)+E(f8(x363,x364,x361),f8(x363,x364,x362))
% 60.45/60.50 [37]~E(x371,x372)+E(f9(x371,x373,x374),f9(x372,x373,x374))
% 60.45/60.50 [38]~E(x381,x382)+E(f9(x383,x381,x384),f9(x383,x382,x384))
% 60.45/60.50 [39]~E(x391,x392)+E(f9(x393,x394,x391),f9(x393,x394,x392))
% 60.45/60.50 [40]~E(x401,x402)+E(f22(x401,x403,x404,x405),f22(x402,x403,x404,x405))
% 60.45/60.50 [41]~E(x411,x412)+E(f22(x413,x411,x414,x415),f22(x413,x412,x414,x415))
% 60.45/60.50 [42]~E(x421,x422)+E(f22(x423,x424,x421,x425),f22(x423,x424,x422,x425))
% 60.45/60.50 [43]~E(x431,x432)+E(f22(x433,x434,x435,x431),f22(x433,x434,x435,x432))
% 60.45/60.50 [44]~E(x441,x442)+E(f14(x441,x443,x444,x445),f14(x442,x443,x444,x445))
% 60.45/60.50 [45]~E(x451,x452)+E(f14(x453,x451,x454,x455),f14(x453,x452,x454,x455))
% 60.45/60.50 [46]~E(x461,x462)+E(f14(x463,x464,x461,x465),f14(x463,x464,x462,x465))
% 60.45/60.50 [47]~E(x471,x472)+E(f14(x473,x474,x475,x471),f14(x473,x474,x475,x472))
% 60.45/60.50 [48]~E(x481,x482)+E(f12(x481,x483,x484,x485,x486),f12(x482,x483,x484,x485,x486))
% 60.45/60.50 [49]~E(x491,x492)+E(f12(x493,x491,x494,x495,x496),f12(x493,x492,x494,x495,x496))
% 60.45/60.50 [50]~E(x501,x502)+E(f12(x503,x504,x501,x505,x506),f12(x503,x504,x502,x505,x506))
% 60.45/60.50 [51]~E(x511,x512)+E(f12(x513,x514,x515,x511,x516),f12(x513,x514,x515,x512,x516))
% 60.45/60.50 [52]~E(x521,x522)+E(f12(x523,x524,x525,x526,x521),f12(x523,x524,x525,x526,x522))
% 60.45/60.50 [53]~E(x531,x532)+E(f11(x531,x533,x534,x535,x536,x537),f11(x532,x533,x534,x535,x536,x537))
% 60.45/60.50 [54]~E(x541,x542)+E(f11(x543,x541,x544,x545,x546,x547),f11(x543,x542,x544,x545,x546,x547))
% 60.45/60.50 [55]~E(x551,x552)+E(f11(x553,x554,x551,x555,x556,x557),f11(x553,x554,x552,x555,x556,x557))
% 60.45/60.50 [56]~E(x561,x562)+E(f11(x563,x564,x565,x561,x566,x567),f11(x563,x564,x565,x562,x566,x567))
% 60.45/60.50 [57]~E(x571,x572)+E(f11(x573,x574,x575,x576,x571,x577),f11(x573,x574,x575,x576,x572,x577))
% 60.45/60.50 [58]~E(x581,x582)+E(f11(x583,x584,x585,x586,x587,x581),f11(x583,x584,x585,x586,x587,x582))
% 60.45/60.50 [59]~E(x591,x592)+E(f27(x591,x593,x594,x595,x596),f27(x592,x593,x594,x595,x596))
% 60.45/60.50 [60]~E(x601,x602)+E(f27(x603,x601,x604,x605,x606),f27(x603,x602,x604,x605,x606))
% 60.45/60.50 [61]~E(x611,x612)+E(f27(x613,x614,x611,x615,x616),f27(x613,x614,x612,x615,x616))
% 60.45/60.50 [62]~E(x621,x622)+E(f27(x623,x624,x625,x621,x626),f27(x623,x624,x625,x622,x626))
% 60.45/60.50 [63]~E(x631,x632)+E(f27(x633,x634,x635,x636,x631),f27(x633,x634,x635,x636,x632))
% 60.45/60.50 [64]~E(x641,x642)+E(f10(x641,x643,x644,x645,x646,x647),f10(x642,x643,x644,x645,x646,x647))
% 60.45/60.50 [65]~E(x651,x652)+E(f10(x653,x651,x654,x655,x656,x657),f10(x653,x652,x654,x655,x656,x657))
% 60.45/60.50 [66]~E(x661,x662)+E(f10(x663,x664,x661,x665,x666,x667),f10(x663,x664,x662,x665,x666,x667))
% 60.45/60.50 [67]~E(x671,x672)+E(f10(x673,x674,x675,x671,x676,x677),f10(x673,x674,x675,x672,x676,x677))
% 60.45/60.50 [68]~E(x681,x682)+E(f10(x683,x684,x685,x686,x681,x687),f10(x683,x684,x685,x686,x682,x687))
% 60.45/60.50 [69]~E(x691,x692)+E(f10(x693,x694,x695,x696,x697,x691),f10(x693,x694,x695,x696,x697,x692))
% 60.45/60.50 [70]~E(x701,x702)+E(f28(x701,x703,x704,x705,x706,x707),f28(x702,x703,x704,x705,x706,x707))
% 60.45/60.50 [71]~E(x711,x712)+E(f28(x713,x711,x714,x715,x716,x717),f28(x713,x712,x714,x715,x716,x717))
% 60.45/60.50 [72]~E(x721,x722)+E(f28(x723,x724,x721,x725,x726,x727),f28(x723,x724,x722,x725,x726,x727))
% 60.45/60.50 [73]~E(x731,x732)+E(f28(x733,x734,x735,x731,x736,x737),f28(x733,x734,x735,x732,x736,x737))
% 60.45/60.50 [74]~E(x741,x742)+E(f28(x743,x744,x745,x746,x741,x747),f28(x743,x744,x745,x746,x742,x747))
% 60.45/60.50 [75]~E(x751,x752)+E(f28(x753,x754,x755,x756,x757,x751),f28(x753,x754,x755,x756,x757,x752))
% 60.45/60.50 [76]~E(x761,x762)+E(f25(x761,x763,x764,x765,x766,x767),f25(x762,x763,x764,x765,x766,x767))
% 60.45/60.50 [77]~E(x771,x772)+E(f25(x773,x771,x774,x775,x776,x777),f25(x773,x772,x774,x775,x776,x777))
% 60.45/60.50 [78]~E(x781,x782)+E(f25(x783,x784,x781,x785,x786,x787),f25(x783,x784,x782,x785,x786,x787))
% 60.45/60.50 [79]~E(x791,x792)+E(f25(x793,x794,x795,x791,x796,x797),f25(x793,x794,x795,x792,x796,x797))
% 60.45/60.50 [80]~E(x801,x802)+E(f25(x803,x804,x805,x806,x801,x807),f25(x803,x804,x805,x806,x802,x807))
% 60.45/60.50 [81]~E(x811,x812)+E(f25(x813,x814,x815,x816,x817,x811),f25(x813,x814,x815,x816,x817,x812))
% 60.45/60.50 [82]~E(x821,x822)+E(f13(x821,x823,x824,x825,x826,x827),f13(x822,x823,x824,x825,x826,x827))
% 60.45/60.50 [83]~E(x831,x832)+E(f13(x833,x831,x834,x835,x836,x837),f13(x833,x832,x834,x835,x836,x837))
% 60.45/60.50 [84]~E(x841,x842)+E(f13(x843,x844,x841,x845,x846,x847),f13(x843,x844,x842,x845,x846,x847))
% 60.45/60.50 [85]~E(x851,x852)+E(f13(x853,x854,x855,x851,x856,x857),f13(x853,x854,x855,x852,x856,x857))
% 60.45/60.50 [86]~E(x861,x862)+E(f13(x863,x864,x865,x866,x861,x867),f13(x863,x864,x865,x866,x862,x867))
% 60.45/60.50 [87]~E(x871,x872)+E(f13(x873,x874,x875,x876,x877,x871),f13(x873,x874,x875,x876,x877,x872))
% 60.45/60.50 [88]P1(x882,x883,x884)+~E(x881,x882)+~P1(x881,x883,x884)
% 60.45/60.50 [89]P1(x893,x892,x894)+~E(x891,x892)+~P1(x893,x891,x894)
% 60.45/60.50 [90]P1(x903,x904,x902)+~E(x901,x902)+~P1(x903,x904,x901)
% 60.45/60.50 [91]P7(x912,x913,x914,x915,x916,x917,x918,x919)+~E(x911,x912)+~P7(x911,x913,x914,x915,x916,x917,x918,x919)
% 60.45/60.50 [92]P7(x923,x922,x924,x925,x926,x927,x928,x929)+~E(x921,x922)+~P7(x923,x921,x924,x925,x926,x927,x928,x929)
% 60.45/60.50 [93]P7(x933,x934,x932,x935,x936,x937,x938,x939)+~E(x931,x932)+~P7(x933,x934,x931,x935,x936,x937,x938,x939)
% 60.45/60.50 [94]P7(x943,x944,x945,x942,x946,x947,x948,x949)+~E(x941,x942)+~P7(x943,x944,x945,x941,x946,x947,x948,x949)
% 60.45/60.50 [95]P7(x953,x954,x955,x956,x952,x957,x958,x959)+~E(x951,x952)+~P7(x953,x954,x955,x956,x951,x957,x958,x959)
% 60.45/60.50 [96]P7(x963,x964,x965,x966,x967,x962,x968,x969)+~E(x961,x962)+~P7(x963,x964,x965,x966,x967,x961,x968,x969)
% 60.45/60.50 [97]P7(x973,x974,x975,x976,x977,x978,x972,x979)+~E(x971,x972)+~P7(x973,x974,x975,x976,x977,x978,x971,x979)
% 60.45/60.50 [98]P7(x983,x984,x985,x986,x987,x988,x989,x982)+~E(x981,x982)+~P7(x983,x984,x985,x986,x987,x988,x989,x981)
% 60.45/60.50 [99]P5(x992,x993,x994,x995)+~E(x991,x992)+~P5(x991,x993,x994,x995)
% 60.45/60.50 [100]P5(x1003,x1002,x1004,x1005)+~E(x1001,x1002)+~P5(x1003,x1001,x1004,x1005)
% 60.45/60.50 [101]P5(x1013,x1014,x1012,x1015)+~E(x1011,x1012)+~P5(x1013,x1014,x1011,x1015)
% 60.45/60.50 [102]P5(x1023,x1024,x1025,x1022)+~E(x1021,x1022)+~P5(x1023,x1024,x1025,x1021)
% 60.45/60.50 [103]P4(x1032,x1033,x1034,x1035)+~E(x1031,x1032)+~P4(x1031,x1033,x1034,x1035)
% 60.45/60.50 [104]P4(x1043,x1042,x1044,x1045)+~E(x1041,x1042)+~P4(x1043,x1041,x1044,x1045)
% 60.45/60.50 [105]P4(x1053,x1054,x1052,x1055)+~E(x1051,x1052)+~P4(x1053,x1054,x1051,x1055)
% 60.45/60.50 [106]P4(x1063,x1064,x1065,x1062)+~E(x1061,x1062)+~P4(x1063,x1064,x1065,x1061)
% 60.45/60.50 [107]P3(x1072,x1073,x1074)+~E(x1071,x1072)+~P3(x1071,x1073,x1074)
% 60.45/60.50 [108]P3(x1083,x1082,x1084)+~E(x1081,x1082)+~P3(x1083,x1081,x1084)
% 60.45/60.50 [109]P3(x1093,x1094,x1092)+~E(x1091,x1092)+~P3(x1093,x1094,x1091)
% 60.45/60.50 [110]P2(x1102,x1103,x1104,x1105)+~E(x1101,x1102)+~P2(x1101,x1103,x1104,x1105)
% 60.45/60.50 [111]P2(x1113,x1112,x1114,x1115)+~E(x1111,x1112)+~P2(x1113,x1111,x1114,x1115)
% 60.45/60.50 [112]P2(x1123,x1124,x1122,x1125)+~E(x1121,x1122)+~P2(x1123,x1124,x1121,x1125)
% 60.45/60.50 [113]P2(x1133,x1134,x1135,x1132)+~E(x1131,x1132)+~P2(x1133,x1134,x1135,x1131)
% 60.45/60.50 [114]P9(x1142,x1143,x1144,x1145)+~E(x1141,x1142)+~P9(x1141,x1143,x1144,x1145)
% 60.45/60.50 [115]P9(x1153,x1152,x1154,x1155)+~E(x1151,x1152)+~P9(x1153,x1151,x1154,x1155)
% 60.45/60.50 [116]P9(x1163,x1164,x1162,x1165)+~E(x1161,x1162)+~P9(x1163,x1164,x1161,x1165)
% 60.45/60.50 [117]P9(x1173,x1174,x1175,x1172)+~E(x1171,x1172)+~P9(x1173,x1174,x1175,x1171)
% 60.45/60.50 [118]P6(x1182,x1183,x1184,x1185,x1186,x1187)+~E(x1181,x1182)+~P6(x1181,x1183,x1184,x1185,x1186,x1187)
% 60.45/60.50 [119]P6(x1193,x1192,x1194,x1195,x1196,x1197)+~E(x1191,x1192)+~P6(x1193,x1191,x1194,x1195,x1196,x1197)
% 60.45/60.50 [120]P6(x1203,x1204,x1202,x1205,x1206,x1207)+~E(x1201,x1202)+~P6(x1203,x1204,x1201,x1205,x1206,x1207)
% 60.45/60.50 [121]P6(x1213,x1214,x1215,x1212,x1216,x1217)+~E(x1211,x1212)+~P6(x1213,x1214,x1215,x1211,x1216,x1217)
% 60.45/60.50 [122]P6(x1223,x1224,x1225,x1226,x1222,x1227)+~E(x1221,x1222)+~P6(x1223,x1224,x1225,x1226,x1221,x1227)
% 60.45/60.50 [123]P6(x1233,x1234,x1235,x1236,x1237,x1232)+~E(x1231,x1232)+~P6(x1233,x1234,x1235,x1236,x1237,x1231)
% 60.45/60.50 [124]P11(x1242,x1243,x1244,x1245,x1246,x1247)+~E(x1241,x1242)+~P11(x1241,x1243,x1244,x1245,x1246,x1247)
% 60.45/60.50 [125]P11(x1253,x1252,x1254,x1255,x1256,x1257)+~E(x1251,x1252)+~P11(x1253,x1251,x1254,x1255,x1256,x1257)
% 60.45/60.50 [126]P11(x1263,x1264,x1262,x1265,x1266,x1267)+~E(x1261,x1262)+~P11(x1263,x1264,x1261,x1265,x1266,x1267)
% 60.45/60.50 [127]P11(x1273,x1274,x1275,x1272,x1276,x1277)+~E(x1271,x1272)+~P11(x1273,x1274,x1275,x1271,x1276,x1277)
% 60.45/60.50 [128]P11(x1283,x1284,x1285,x1286,x1282,x1287)+~E(x1281,x1282)+~P11(x1283,x1284,x1285,x1286,x1281,x1287)
% 60.45/60.50 [129]P11(x1293,x1294,x1295,x1296,x1297,x1292)+~E(x1291,x1292)+~P11(x1293,x1294,x1295,x1296,x1297,x1291)
% 60.45/60.50 [130]P8(x1302,x1303,x1304,x1305,x1306,x1307,x1308,x1309)+~E(x1301,x1302)+~P8(x1301,x1303,x1304,x1305,x1306,x1307,x1308,x1309)
% 60.45/60.50 [131]P8(x1313,x1312,x1314,x1315,x1316,x1317,x1318,x1319)+~E(x1311,x1312)+~P8(x1313,x1311,x1314,x1315,x1316,x1317,x1318,x1319)
% 60.45/60.50 [132]P8(x1323,x1324,x1322,x1325,x1326,x1327,x1328,x1329)+~E(x1321,x1322)+~P8(x1323,x1324,x1321,x1325,x1326,x1327,x1328,x1329)
% 60.45/60.50 [133]P8(x1333,x1334,x1335,x1332,x1336,x1337,x1338,x1339)+~E(x1331,x1332)+~P8(x1333,x1334,x1335,x1331,x1336,x1337,x1338,x1339)
% 60.45/60.50 [134]P8(x1343,x1344,x1345,x1346,x1342,x1347,x1348,x1349)+~E(x1341,x1342)+~P8(x1343,x1344,x1345,x1346,x1341,x1347,x1348,x1349)
% 60.45/60.50 [135]P8(x1353,x1354,x1355,x1356,x1357,x1352,x1358,x1359)+~E(x1351,x1352)+~P8(x1353,x1354,x1355,x1356,x1357,x1351,x1358,x1359)
% 60.45/60.50 [136]P8(x1363,x1364,x1365,x1366,x1367,x1368,x1362,x1369)+~E(x1361,x1362)+~P8(x1363,x1364,x1365,x1366,x1367,x1368,x1361,x1369)
% 60.45/60.50 [137]P8(x1373,x1374,x1375,x1376,x1377,x1378,x1379,x1372)+~E(x1371,x1372)+~P8(x1373,x1374,x1375,x1376,x1377,x1378,x1379,x1371)
% 60.45/60.50 [138]P10(x1382,x1383,x1384,x1385)+~E(x1381,x1382)+~P10(x1381,x1383,x1384,x1385)
% 60.45/60.50 [139]P10(x1393,x1392,x1394,x1395)+~E(x1391,x1392)+~P10(x1393,x1391,x1394,x1395)
% 60.45/60.50 [140]P10(x1403,x1404,x1402,x1405)+~E(x1401,x1402)+~P10(x1403,x1404,x1401,x1405)
% 60.45/60.50 [141]P10(x1413,x1414,x1415,x1412)+~E(x1411,x1412)+~P10(x1413,x1414,x1415,x1411)
% 60.45/60.50
% 60.45/60.50 %-------------------------------------------
% 60.49/60.51 cnf(264,plain,
% 60.49/60.51 (~P4(a1,a20,a2,a1)),
% 60.49/60.51 inference(scs_inference,[],[150,167])).
% 60.49/60.51 cnf(266,plain,
% 60.49/60.51 (~P4(a2,a1,a20,a1)),
% 60.49/60.51 inference(scs_inference,[],[150,167,168])).
% 60.49/60.51 cnf(270,plain,
% 60.49/60.51 (~P6(a1,a20,x2701,a2,a1,x2702)),
% 60.49/60.51 inference(scs_inference,[],[150,167,168,202,217])).
% 60.49/60.51 cnf(274,plain,
% 60.49/60.51 (~P6(a2,x2741,a1,a1,x2742,a20)),
% 60.49/60.51 inference(scs_inference,[],[150,167,168,202,217,218,219])).
% 60.49/60.51 cnf(276,plain,
% 60.49/60.51 (P1(a15,a15,a1)),
% 60.49/60.51 inference(scs_inference,[],[142,150,167,168,202,217,218,219,155])).
% 60.49/60.51 cnf(278,plain,
% 60.49/60.51 (P9(a15,a15,a17,a17)),
% 60.49/60.51 inference(scs_inference,[],[142,146,150,167,168,202,217,218,219,155,157])).
% 60.49/60.51 cnf(280,plain,
% 60.49/60.51 (P9(a19,a19,a17,a17)),
% 60.49/60.51 inference(scs_inference,[],[142,146,150,167,168,202,217,218,219,155,157,158])).
% 60.49/60.51 cnf(296,plain,
% 60.49/60.51 (~P6(a2,a1,x2961,a20,a1,x2962)),
% 60.49/60.51 inference(scs_inference,[],[266,270,219,218,202])).
% 60.49/60.51 cnf(298,plain,
% 60.49/60.51 (~P4(a20,a1,a2,a1)),
% 60.49/60.51 inference(scs_inference,[],[266,270,219,218,202,167])).
% 60.49/60.51 cnf(302,plain,
% 60.49/60.51 (~P4(a1,a20,a1,a2)),
% 60.49/60.51 inference(scs_inference,[],[264,266,270,219,218,202,167,217,168])).
% 60.49/60.51 cnf(306,plain,
% 60.49/60.51 (P9(a16,a16,a2,a2)),
% 60.49/60.51 inference(scs_inference,[],[143,147,264,266,270,219,218,202,167,217,168,155,157])).
% 60.49/60.51 cnf(308,plain,
% 60.49/60.51 (P9(a18,a18,a2,a2)),
% 60.49/60.51 inference(scs_inference,[],[143,147,264,266,270,219,218,202,167,217,168,155,157,158])).
% 60.49/60.51 cnf(310,plain,
% 60.49/60.51 (~P3(a1,a20,a2)),
% 60.49/60.51 inference(scs_inference,[],[143,147,264,266,270,219,218,202,167,217,168,155,157,158,156])).
% 60.49/60.51 cnf(312,plain,
% 60.49/60.51 (~P3(x3121,a20,a2)+~P10(a1,x3121,a20,a2)),
% 60.49/60.51 inference(scs_inference,[],[143,147,264,266,270,219,218,202,167,217,168,155,157,158,156,173])).
% 60.49/60.51 cnf(321,plain,
% 60.49/60.51 (~P6(a2,x3211,a1,a20,x3212,a1)),
% 60.49/60.51 inference(scs_inference,[],[296,219])).
% 60.49/60.51 cnf(323,plain,
% 60.49/60.51 (~P6(a1,a20,x3231,a1,a2,x3232)),
% 60.49/60.51 inference(scs_inference,[],[296,302,219,202])).
% 60.49/60.51 cnf(325,plain,
% 60.49/60.51 (~P6(a20,x3251,a1,a2,x3252,a1)),
% 60.49/60.51 inference(scs_inference,[],[296,302,219,202,217])).
% 60.49/60.51 cnf(327,plain,
% 60.49/60.51 (~P4(a1,a2,a1,a20)),
% 60.49/60.51 inference(scs_inference,[],[296,302,219,202,217,167])).
% 60.49/60.51 cnf(329,plain,
% 60.49/60.51 (~P4(a20,a1,a1,a2)),
% 60.49/60.51 inference(scs_inference,[],[296,298,302,219,202,217,167,168])).
% 60.49/60.51 cnf(333,plain,
% 60.49/60.51 (~P3(a1,a2,a20)),
% 60.49/60.51 inference(scs_inference,[],[296,298,302,310,219,202,217,167,168,218,154])).
% 60.49/60.51 cnf(342,plain,
% 60.49/60.51 (~P6(a1,x3421,a20,a1,x3422,a2)),
% 60.49/60.51 inference(scs_inference,[],[323,219])).
% 60.49/60.51 cnf(344,plain,
% 60.49/60.51 (~P6(a1,x3441,a2,a1,x3442,a20)),
% 60.49/60.51 inference(scs_inference,[],[323,219,217])).
% 60.49/60.51 cnf(346,plain,
% 60.49/60.51 (~P4(a1,a2,a20,a1)),
% 60.49/60.51 inference(scs_inference,[],[323,327,219,217,168])).
% 60.49/60.51 cnf(348,plain,
% 60.49/60.51 (~P6(x3481,a2,a1,x3482,a1,a20)),
% 60.49/60.51 inference(scs_inference,[],[323,327,274,219,217,168,218])).
% 60.49/60.51 cnf(380,plain,
% 60.49/60.51 (~P6(x3801,a20,a1,x3802,a1,a2)),
% 60.49/60.51 inference(scs_inference,[],[348,219,217])).
% 60.49/60.51 cnf(382,plain,
% 60.49/60.51 (~P6(x3821,a2,a1,x3822,a20,a1)),
% 60.49/60.51 inference(scs_inference,[],[321,348,219,217,218])).
% 60.49/60.51 cnf(398,plain,
% 60.49/60.51 (~P6(x3981,a20,a1,x3982,a2,a1)),
% 60.49/60.51 inference(scs_inference,[],[325,382,219,218])).
% 60.49/60.51 cnf(415,plain,
% 60.49/60.51 (~P4(a1,x4151,a1,x4152)+~P11(a1,x4151,a20,a1,x4152,a2)),
% 60.49/60.51 inference(scs_inference,[],[276,342,155,220])).
% 60.49/60.51 cnf(438,plain,
% 60.49/60.51 (~P3(x4381,a2,a20)+~P10(a1,x4381,a2,a20)),
% 60.49/60.51 inference(scs_inference,[],[327,173])).
% 60.49/60.51 cnf(444,plain,
% 60.49/60.51 (~P10(a16,x4441,x4441,a2)+P4(a16,a18,x4441,a18)),
% 60.49/60.51 inference(scs_inference,[],[147,174])).
% 60.49/60.51 cnf(456,plain,
% 60.49/60.51 (~P4(a1,x4561,a1,x4562)+~P11(a1,x4561,a2,a1,x4562,a20)),
% 60.49/60.51 inference(scs_inference,[],[142,148,344,89,116,220])).
% 60.49/60.51 cnf(480,plain,
% 60.49/60.51 (~P9(x4801,x4802,a16,a15)+P9(x4801,x4802,a2,a17)),
% 60.49/60.51 inference(scs_inference,[],[149,179])).
% 60.49/60.51 cnf(489,plain,
% 60.49/60.51 (~P10(a2,a17,x4891,x4892)+P10(a16,a15,x4891,x4892)),
% 60.49/60.51 inference(scs_inference,[],[149,182])).
% 60.49/60.51 cnf(491,plain,
% 60.49/60.51 (~P10(x4911,x4912,a2,a17)+P10(a16,a15,x4911,x4912)),
% 60.49/60.51 inference(scs_inference,[],[149,182,165])).
% 60.49/60.51 cnf(493,plain,
% 60.49/60.51 (~P10(a2,a17,x4931,x4932)+P10(a16,a15,x4932,x4931)),
% 60.49/60.51 inference(scs_inference,[],[149,182,165,166])).
% 60.49/60.51 cnf(497,plain,
% 60.49/60.51 (~P9(x4971,x4972,a2,a16)+P9(x4971,x4972,a15,a17)),
% 60.49/60.51 inference(scs_inference,[],[149,148,114,179])).
% 60.49/60.51 cnf(527,plain,
% 60.49/60.51 (~P10(a15,a17,x5271,x5272)+P10(a2,a16,x5271,x5272)),
% 60.49/60.51 inference(scs_inference,[],[148,182])).
% 60.49/60.51 cnf(529,plain,
% 60.49/60.51 (~P10(a15,a17,x5291,x5292)+P10(a2,a16,x5292,x5291)),
% 60.49/60.51 inference(scs_inference,[],[148,182,166])).
% 60.49/60.51 cnf(531,plain,
% 60.49/60.51 (~P10(x5311,x5312,a15,a17)+P10(a2,a16,x5311,x5312)),
% 60.49/60.51 inference(scs_inference,[],[148,182,166,165])).
% 60.49/60.51 cnf(534,plain,
% 60.49/60.51 (~P4(x5341,x5342,x5343,x5344)+~P7(a2,a1,a1,a20,x5341,x5342,x5343,x5344)),
% 60.49/60.51 inference(scs_inference,[],[150,243])).
% 60.49/60.51 cnf(569,plain,
% 60.49/60.51 (~P4(x5691,x5692,x5693,x5694)+~P7(a1,a20,a1,a2,x5691,x5692,x5693,x5694)),
% 60.49/60.51 inference(scs_inference,[],[143,302,306,117,89,115,243])).
% 60.49/60.51 cnf(578,plain,
% 60.49/60.51 (~P9(x5781,x5782,a19,a19)+P9(x5781,x5782,a17,a17)),
% 60.49/60.51 inference(scs_inference,[],[280,179])).
% 60.49/60.51 cnf(585,plain,
% 60.49/60.51 (~P10(a2,a2,x5851,x5852)+P10(a18,a18,x5851,x5852)),
% 60.49/60.51 inference(scs_inference,[],[308,182])).
% 60.49/60.51 cnf(587,plain,
% 60.49/60.51 (~P10(x5871,x5872,a2,a2)+P10(a18,a18,x5871,x5872)),
% 60.49/60.51 inference(scs_inference,[],[308,182,165])).
% 60.49/60.51 cnf(589,plain,
% 60.49/60.51 (~P10(a2,a2,x5891,x5892)+P10(a18,a18,x5892,x5891)),
% 60.49/60.51 inference(scs_inference,[],[308,182,165,166])).
% 60.49/60.51 cnf(592,plain,
% 60.49/60.51 (~P4(x5921,x5922,x5923,x5924)+~P7(a1,a2,a1,a20,x5921,x5922,x5923,x5924)),
% 60.49/60.51 inference(scs_inference,[],[327,243])).
% 60.49/60.51 cnf(612,plain,
% 60.49/60.51 (~P4(x6121,x6122,x6123,x6124)+~P7(a20,a1,a1,a2,x6121,x6122,x6123,x6124)),
% 60.49/60.51 inference(scs_inference,[],[144,329,278,88,90,117,243])).
% 60.49/60.51 cnf(614,plain,
% 60.49/60.51 (~P9(x6141,x6142,a15,a15)+P9(x6141,x6142,a17,a17)),
% 60.49/60.51 inference(scs_inference,[],[144,329,278,88,90,117,243,179])).
% 60.49/60.51 cnf(625,plain,
% 60.49/60.51 (~P9(x6251,x6252,a18,a18)+P9(x6251,x6252,a2,a2)),
% 60.49/60.51 inference(scs_inference,[],[308,179])).
% 60.49/60.51 cnf(632,plain,
% 60.49/60.51 (~P4(x6321,x6322,x6323,x6324)+~P7(a1,a20,a2,a1,x6321,x6322,x6323,x6324)),
% 60.49/60.51 inference(scs_inference,[],[264,243])).
% 60.49/60.51 cnf(648,plain,
% 60.49/60.51 (~P10(a2,a2,x6481,x6482)+P10(a16,a16,x6481,x6482)),
% 60.49/60.51 inference(scs_inference,[],[145,306,88,182])).
% 60.49/60.51 cnf(652,plain,
% 60.49/60.51 (~P4(x6521,x6522,x6523,x6524)+~P7(a20,a1,a2,a1,x6521,x6522,x6523,x6524)),
% 60.49/60.51 inference(scs_inference,[],[145,298,306,280,308,88,182,115,117,243])).
% 60.49/60.51 cnf(662,plain,
% 60.49/60.51 (~P4(x6621,x6622,x6623,x6624)+~P7(a2,a1,a20,a1,x6621,x6622,x6623,x6624)),
% 60.49/60.51 inference(scs_inference,[],[147,143,266,306,114,108,90,243])).
% 60.49/60.51 cnf(671,plain,
% 60.49/60.51 (~P9(x6711,x6712,a16,a16)+P9(x6711,x6712,a2,a2)),
% 60.49/60.51 inference(scs_inference,[],[306,179])).
% 60.49/60.51 cnf(679,plain,
% 60.49/60.51 (~P10(a17,a17,x6791,x6792)+P10(a19,a19,x6791,x6792)),
% 60.49/60.51 inference(scs_inference,[],[143,280,88,182])).
% 60.49/60.51 cnf(681,plain,
% 60.49/60.51 (~P4(x6811,x6812,x6813,x6814)+~P7(a1,a2,a20,a1,x6811,x6812,x6813,x6814)),
% 60.49/60.51 inference(scs_inference,[],[143,346,280,88,182,243])).
% 60.49/60.51 cnf(696,plain,
% 60.49/60.51 (~P10(a17,a17,x6961,x6962)+P10(a15,a15,x6961,x6962)),
% 60.49/60.51 inference(scs_inference,[],[144,145,278,380,89,90,220,182])).
% 60.49/60.51 cnf(724,plain,
% 60.49/60.51 (~P3(x7241,a20,a2)+~P11(x7241,a20,a1,x7241,a2,a1)),
% 60.49/60.51 inference(scs_inference,[],[398,220,156])).
% 60.49/60.51 cnf(751,plain,
% 60.49/60.51 (~P3(x7511,a2,a1)+~P11(x7511,a2,a1,x7511,a1,a20)),
% 60.49/60.51 inference(scs_inference,[],[348,220,156])).
% 60.49/60.51 cnf(824,plain,
% 60.49/60.51 (P7(x8241,a16,a16,a2,x8241,a16,a16,a2)+~P1(x8241,a16,a2)),
% 60.49/60.51 inference(scs_inference,[],[306,228])).
% 60.49/60.51 cnf(828,plain,
% 60.49/60.51 (P7(x8281,a19,a19,a17,x8281,a19,a19,a17)+~P1(x8281,a19,a17)),
% 60.49/60.51 inference(scs_inference,[],[280,228])).
% 60.49/60.51 cnf(832,plain,
% 60.49/60.51 (P7(x8321,a18,a18,a2,x8321,a18,a18,a2)+~P1(x8321,a18,a2)),
% 60.49/60.51 inference(scs_inference,[],[308,228])).
% 60.49/60.51 cnf(836,plain,
% 60.49/60.51 (P7(x8361,a15,a15,a17,x8361,a15,a15,a17)+~P1(x8361,a15,a17)),
% 60.49/60.51 inference(scs_inference,[],[278,228])).
% 60.49/60.51 cnf(840,plain,
% 60.49/60.51 (~P3(x8401,a2,a15)+~P9(a2,a17,a15,a16)+P3(x8401,a16,a17)),
% 60.49/60.51 inference(scs_inference,[],[148,310,175])).
% 60.49/60.51 cnf(1053,plain,
% 60.49/60.51 (~P3(x10531,a2,a20)+~P10(a1,x10531,a20,a2)),
% 60.49/60.51 inference(scs_inference,[],[312,154])).
% 60.49/60.51 cnf(1374,plain,
% 60.49/60.51 (P5(x13741,x13742,x13743,x13744)+~P5(x13743,x13741,x13742,x13744)),
% 60.49/60.51 inference(scs_inference,[],[169,170])).
% 60.49/60.51 cnf(1502,plain,
% 60.49/60.51 (P9(x15021,x15022,a17,a2)+~P9(x15021,x15022,a16,a15)),
% 60.49/60.51 inference(scs_inference,[],[480,164])).
% 60.49/60.51 cnf(1614,plain,
% 60.49/60.51 (P10(x16141,x16142,a2,a16)+~P10(a15,a17,x16142,x16141)),
% 60.49/60.51 inference(scs_inference,[],[529,165])).
% 60.49/60.51 cnf(1918,plain,
% 60.49/60.51 (P5(x19181,x19182,x19183,x19184)+~P5(x19183,x19182,x19181,x19184)),
% 60.49/60.51 inference(scs_inference,[],[1374,170])).
% 60.49/60.51 cnf(1998,plain,
% 60.49/60.52 (P9(a2,a17,a17,a2)),
% 60.49/60.52 inference(scs_inference,[],[149,1502,163])).
% 60.49/60.52 cnf(1999,plain,
% 60.49/60.52 (P9(a16,a15,a17,a2)),
% 60.49/60.52 inference(scs_inference,[],[149,1998,179])).
% 60.49/60.52 cnf(2002,plain,
% 60.49/60.52 (~P10(a17,a2,x20021,x20022)+P10(a2,a17,x20021,x20022)),
% 60.49/60.52 inference(scs_inference,[],[149,1998,179,117,182])).
% 60.49/60.52 cnf(2011,plain,
% 60.49/60.52 (~P10(a17,a2,x20111,x20112)+P10(a16,a15,x20111,x20112)),
% 60.49/60.52 inference(scs_inference,[],[1999,117,182])).
% 60.49/60.52 cnf(2034,plain,
% 60.49/60.52 (~P10(x20341,x20342,x20343,x20344)+~P8(x20345,a2,x20346,x20347,x20341,x20342,x20343,x20344)+P10(a2,a17,x20346,x20347)+~E(a17,x20345)),
% 60.49/60.52 inference(scs_inference,[],[264,142,302,1998,116,182,241])).
% 60.49/60.52 cnf(2036,plain,
% 60.49/60.52 (~P10(x20361,x20362,x20363,x20364)+~P8(a17,a2,x20365,x20366,x20361,x20362,x20363,x20364)+P10(a2,a17,x20365,x20366)),
% 60.49/60.52 inference(equality_inference,[],[2034])).
% 60.49/60.52 cnf(2173,plain,
% 60.49/60.52 (~P10(x21731,x21732,a15,a17)+P10(x21732,x21731,a2,a16)),
% 60.49/60.52 inference(scs_inference,[],[1614,165])).
% 60.49/60.52 cnf(2301,plain,
% 60.49/60.52 (P5(x23011,x23012,x23013,x23014)+~P5(x23012,x23013,x23011,x23014)),
% 60.49/60.52 inference(scs_inference,[],[1918,169])).
% 60.49/60.52 cnf(2493,plain,
% 60.49/60.52 (P5(x24931,x24932,x24933,x24934)+~P5(x24932,x24933,x24934,x24931)),
% 60.49/60.52 inference(scs_inference,[],[2301,171])).
% 60.49/60.52 cnf(2686,plain,
% 60.49/60.52 (~P5(x26861,x26862,x26863,x26864)+P5(x26864,x26862,x26863,x26861)),
% 60.49/60.52 inference(scs_inference,[],[2493,1374])).
% 60.49/60.52 cnf(3217,plain,
% 60.49/60.52 (~P11(x32171,a2,a1,x32171,a20,a1)+~P3(x32171,a20,a2)),
% 60.49/60.52 inference(scs_inference,[],[724,214])).
% 60.49/60.52 cnf(3233,plain,
% 60.49/60.52 (~P11(a2,x32331,a1,a1,x32331,a20)+~P3(x32331,a2,a1)),
% 60.49/60.52 inference(scs_inference,[],[751,215])).
% 60.49/60.52 cnf(3297,plain,
% 60.49/60.52 (~P3(x32971,a2,a20)+~P11(x32971,a2,a1,x32971,a20,a1)),
% 60.49/60.52 inference(scs_inference,[],[3217,154])).
% 60.49/60.52 cnf(3313,plain,
% 60.49/60.52 (~P3(x33131,a1,a2)+~P11(a2,x33131,a1,a1,x33131,a20)),
% 60.49/60.52 inference(scs_inference,[],[3233,154])).
% 60.49/60.52 cnf(4210,plain,
% 60.49/60.52 (~P4(a1,x42101,a1,x42102)+~P11(a1,x42102,a20,a1,x42101,a2)),
% 60.49/60.52 inference(scs_inference,[],[415,167])).
% 60.49/60.52 cnf(4273,plain,
% 60.49/60.52 (P1(a18,a16,a2)),
% 60.49/60.52 inference(scs_inference,[],[1999,147,225,153])).
% 60.49/60.52 cnf(4275,plain,
% 60.49/60.52 (P8(a17,a2,x42751,x42752,a16,a15,x42751,x42752)),
% 60.49/60.52 inference(scs_inference,[],[1999,147,225,153,252])).
% 60.49/60.52 cnf(4277,plain,
% 60.49/60.52 (P8(a16,a15,a17,a2,x42771,x42772,x42771,x42772)),
% 60.49/60.52 inference(scs_inference,[],[1999,147,225,153,252,255])).
% 60.49/60.52 cnf(4279,plain,
% 60.49/60.52 (P1(a1,a15,a2)),
% 60.49/60.52 inference(scs_inference,[],[142,1999,147,225,153,252,255,152])).
% 60.49/60.52 cnf(4281,plain,
% 60.49/60.52 (P9(a17,a2,a16,a15)),
% 60.49/60.52 inference(scs_inference,[],[142,1999,147,225,153,252,255,152,163])).
% 60.49/60.52 cnf(4283,plain,
% 60.49/60.52 (P9(a2,a17,a2,a17)),
% 60.49/60.52 inference(scs_inference,[],[142,1999,1998,147,225,153,252,255,152,163,164])).
% 60.49/60.52 cnf(4285,plain,
% 60.49/60.52 (P1(a2,a1,a15)),
% 60.49/60.52 inference(scs_inference,[],[142,1999,1998,147,225,153,252,255,152,163,164,151])).
% 60.49/60.52 cnf(4287,plain,
% 60.49/60.52 (P8(a15,a16,x42871,x42872,a17,a2,x42871,x42872)),
% 60.49/60.52 inference(scs_inference,[],[142,1999,1998,147,225,153,252,255,152,163,164,151,254])).
% 60.49/60.52 cnf(4289,plain,
% 60.49/60.52 (P1(a2,a17,a17)),
% 60.49/60.52 inference(scs_inference,[],[142,1999,1998,147,225,153,252,255,152,163,164,151,254,160])).
% 60.49/60.52 cnf(4293,plain,
% 60.49/60.52 (P3(a18,a2,a16)),
% 60.49/60.52 inference(scs_inference,[],[142,1999,1998,147,225,153,252,255,152,163,164,151,254,160,253,154])).
% 60.49/60.52 cnf(4295,plain,
% 60.49/60.52 (P4(a18,a16,a18,a2)),
% 60.49/60.52 inference(scs_inference,[],[142,1999,1998,147,225,153,252,255,152,163,164,151,254,160,253,154,156])).
% 60.49/60.52 cnf(4297,plain,
% 60.49/60.52 (P4(a18,a2,a18,a16)),
% 60.49/60.52 inference(scs_inference,[],[142,1999,1998,147,225,153,252,255,152,163,164,151,254,160,253,154,156,167])).
% 60.49/60.52 cnf(4299,plain,
% 60.49/60.52 (P4(a18,a16,a18,a16)),
% 60.49/60.52 inference(scs_inference,[],[142,1999,1998,147,225,153,252,255,152,163,164,151,254,160,253,154,156,167,183])).
% 60.49/60.52 cnf(4309,plain,
% 60.49/60.52 (P8(a16,a15,x43091,x43092,a16,a15,x43091,x43092)),
% 60.49/60.52 inference(scs_inference,[],[142,1999,1998,147,225,153,252,255,152,163,164,151,254,160,253,154,156,167,183,184,223,204,205,262])).
% 60.49/60.52 cnf(4311,plain,
% 60.49/60.52 (P9(a17,a2,a17,a2)),
% 60.49/60.52 inference(scs_inference,[],[142,1999,1998,147,225,153,252,255,152,163,164,151,254,160,253,154,156,167,183,184,223,204,205,262,240])).
% 60.49/60.52 cnf(4313,plain,
% 60.49/60.52 (P9(a18,a18,a16,a16)),
% 60.49/60.52 inference(scs_inference,[],[142,1999,1998,147,225,153,252,255,152,163,164,151,254,160,253,154,156,167,183,184,223,204,205,262,240,158])).
% 60.49/60.52 cnf(4315,plain,
% 60.49/60.52 (P3(f25(a16,a2,a16,a2,a18,a18),a16,a2)),
% 60.49/60.52 inference(scs_inference,[],[142,1999,1998,147,225,153,252,255,152,163,164,151,254,160,253,154,156,167,183,184,223,204,205,262,240,158,203])).
% 60.49/60.52 cnf(4317,plain,
% 60.49/60.52 (P9(a2,a2,a16,a16)),
% 60.49/60.52 inference(scs_inference,[],[142,1999,1998,147,225,153,252,255,152,163,164,151,254,160,253,154,156,167,183,184,223,204,205,262,240,158,203,157])).
% 60.49/60.52 cnf(4319,plain,
% 60.49/60.52 (P10(a18,a18,a16,a16)),
% 60.49/60.52 inference(scs_inference,[],[142,1999,1998,147,225,153,252,255,152,163,164,151,254,160,253,154,156,167,183,184,223,204,205,262,240,158,203,157,181])).
% 60.49/60.52 cnf(4321,plain,
% 60.49/60.52 (P10(a16,a2,a2,a2)),
% 60.49/60.52 inference(scs_inference,[],[142,1999,1998,147,225,153,252,255,152,163,164,151,254,160,253,154,156,167,183,184,223,204,205,262,240,158,203,157,181,172])).
% 60.49/60.52 cnf(4327,plain,
% 60.49/60.52 (P9(a16,a15,a16,a15)),
% 60.49/60.52 inference(scs_inference,[],[142,346,1999,1998,147,225,153,252,255,152,163,164,151,254,160,253,154,156,167,183,184,223,204,205,262,240,158,203,157,181,172,243,198,179])).
% 60.49/60.52 cnf(4329,plain,
% 60.49/60.52 (P4(a16,a18,a2,a18)),
% 60.49/60.52 inference(scs_inference,[],[142,346,1999,1998,147,225,153,252,255,152,163,164,151,254,160,253,154,156,167,183,184,223,204,205,262,240,158,203,157,181,172,243,198,179,174])).
% 60.49/60.52 cnf(4331,plain,
% 60.49/60.52 (P5(a16,a2,a2,a2)),
% 60.49/60.52 inference(scs_inference,[],[142,346,1999,1998,147,225,153,252,255,152,163,164,151,254,160,253,154,156,167,183,184,223,204,205,262,240,158,203,157,181,172,243,198,179,174,196])).
% 60.49/60.52 cnf(4335,plain,
% 60.49/60.52 (P5(a2,a2,a16,a2)),
% 60.49/60.52 inference(scs_inference,[],[142,346,1999,1998,147,225,153,252,255,152,163,164,151,254,160,253,154,156,167,183,184,223,204,205,262,240,158,203,157,181,172,243,198,179,174,196,169,170])).
% 60.49/60.52 cnf(4337,plain,
% 60.49/60.52 (P5(a2,a2,a2,a16)),
% 60.49/60.52 inference(scs_inference,[],[142,346,1999,1998,147,225,153,252,255,152,163,164,151,254,160,253,154,156,167,183,184,223,204,205,262,240,158,203,157,181,172,243,198,179,174,196,169,170,171])).
% 60.49/60.52 cnf(4339,plain,
% 60.49/60.52 (P8(a2,a16,a2,a2,a2,a16,a2,a2)),
% 60.49/60.52 inference(scs_inference,[],[142,346,1999,1998,147,225,153,252,255,152,163,164,151,254,160,253,154,156,167,183,184,223,204,205,262,240,158,203,157,181,172,243,198,179,174,196,169,170,171,224])).
% 60.49/60.52 cnf(4341,plain,
% 60.49/60.52 (P8(a18,a16,a16,a2,a16,a2,a18,a2)),
% 60.49/60.52 inference(scs_inference,[],[142,346,1999,1998,147,225,153,252,255,152,163,164,151,254,160,253,154,156,167,183,184,223,204,205,262,240,158,203,157,181,172,243,198,179,174,196,169,170,171,224,226])).
% 60.49/60.52 cnf(4343,plain,
% 60.49/60.52 (P9(a17,a2,a2,a17)),
% 60.49/60.52 inference(scs_inference,[],[142,346,1999,1998,147,225,153,252,255,152,163,164,151,254,160,253,154,156,167,183,184,223,204,205,262,240,158,203,157,181,172,243,198,179,174,196,169,170,171,224,226,480])).
% 60.49/60.52 cnf(4345,plain,
% 60.49/60.52 (P10(a18,a18,a16,a2)),
% 60.49/60.52 inference(scs_inference,[],[142,346,1999,1998,147,225,153,252,255,152,163,164,151,254,160,253,154,156,167,183,184,223,204,205,262,240,158,203,157,181,172,243,198,179,174,196,169,170,171,224,226,480,587])).
% 60.49/60.52 cnf(4347,plain,
% 60.49/60.52 (P9(a2,a2,a2,a2)),
% 60.49/60.52 inference(scs_inference,[],[142,346,1999,1998,147,225,153,252,255,152,163,164,151,254,160,253,154,156,167,183,184,223,204,205,262,240,158,203,157,181,172,243,198,179,174,196,169,170,171,224,226,480,587,671])).
% 60.49/60.52 cnf(4349,plain,
% 60.49/60.52 (P10(f7(a16,a2,a2,a18),a16,a16,a18)),
% 60.49/60.52 inference(scs_inference,[],[142,346,1999,1998,147,225,153,252,255,152,163,164,151,254,160,253,154,156,167,183,184,223,204,205,262,240,158,203,157,181,172,243,198,179,174,196,169,170,171,224,226,480,587,671,187])).
% 60.49/60.52 cnf(4351,plain,
% 60.49/60.52 (P7(a16,a2,a18,a16,a16,a2,a18,a16)),
% 60.49/60.52 inference(scs_inference,[],[142,346,1999,1998,147,225,153,252,255,152,163,164,151,254,160,253,154,156,167,183,184,223,204,205,262,240,158,203,157,181,172,243,198,179,174,196,169,170,171,224,226,480,587,671,187,257])).
% 60.49/60.52 cnf(4353,plain,
% 60.49/60.52 (P7(a16,a18,a16,a2,a18,a16,a16,a2)),
% 60.49/60.52 inference(scs_inference,[],[142,346,1999,1998,147,225,153,252,255,152,163,164,151,254,160,253,154,156,167,183,184,223,204,205,262,240,158,203,157,181,172,243,198,179,174,196,169,170,171,224,226,480,587,671,187,257,258])).
% 60.49/60.52 cnf(4355,plain,
% 60.49/60.52 (P7(a18,a16,a18,a16,a16,a2,a16,a2)),
% 60.49/60.52 inference(scs_inference,[],[142,346,1999,1998,147,225,153,252,255,152,163,164,151,254,160,253,154,156,167,183,184,223,204,205,262,240,158,203,157,181,172,243,198,179,174,196,169,170,171,224,226,480,587,671,187,257,258,259])).
% 60.49/60.52 cnf(4375,plain,
% 60.49/60.52 (P4(a18,a16,a2,a18)),
% 60.49/60.52 inference(scs_inference,[],[142,346,1999,1998,147,225,153,252,255,152,163,164,151,254,160,253,154,156,167,183,184,223,204,205,262,240,158,203,157,181,172,243,198,179,174,196,169,170,171,224,226,480,587,671,187,257,258,259,534,569,592,612,632,652,662,681,233,168])).
% 60.49/60.52 cnf(4377,plain,
% 60.49/60.52 (P10(a16,a16,a18,a18)),
% 60.49/60.52 inference(scs_inference,[],[142,346,1999,1998,147,225,153,252,255,152,163,164,151,254,160,253,154,156,167,183,184,223,204,205,262,240,158,203,157,181,172,243,198,179,174,196,169,170,171,224,226,480,587,671,187,257,258,259,534,569,592,612,632,652,662,681,233,168,165])).
% 60.49/60.52 cnf(4383,plain,
% 60.49/60.52 (P2(f8(a16,a2,a2),a16,a2,a2)),
% 60.49/60.52 inference(scs_inference,[],[142,346,1999,1998,147,225,153,252,255,152,163,164,151,254,160,253,154,156,167,183,184,223,204,205,262,240,158,203,157,181,172,243,198,179,174,196,169,170,171,224,226,480,587,671,187,257,258,259,534,569,592,612,632,652,662,681,233,168,165,166,161,191])).
% 60.49/60.52 cnf(4385,plain,
% 60.49/60.52 (P1(a16,a16,f22(a16,a16,a18,a18))),
% 60.49/60.52 inference(scs_inference,[],[142,346,1999,1998,147,225,153,252,255,152,163,164,151,254,160,253,154,156,167,183,184,223,204,205,262,240,158,203,157,181,172,243,198,179,174,196,169,170,171,224,226,480,587,671,187,257,258,259,534,569,592,612,632,652,662,681,233,168,165,166,161,191,193])).
% 60.49/60.52 cnf(4391,plain,
% 60.49/60.52 (P7(a18,a16,a16,a2,a16,a18,a16,a2)),
% 60.49/60.52 inference(scs_inference,[],[142,346,1999,1998,147,225,153,252,255,152,163,164,151,254,160,253,154,156,167,183,184,223,204,205,262,240,158,203,157,181,172,243,198,179,174,196,169,170,171,224,226,480,587,671,187,257,258,259,534,569,592,612,632,652,662,681,233,168,165,166,161,191,193,194,197,256])).
% 60.49/60.52 cnf(4397,plain,
% 60.49/60.52 (P7(a16,a2,a16,a18,a16,a2,a18,a16)),
% 60.49/60.52 inference(scs_inference,[],[4329,4353,534,257])).
% 60.49/60.52 cnf(4399,plain,
% 60.49/60.52 (P8(a2,a2,x43991,x43992,a2,a2,x43991,x43992)),
% 60.49/60.52 inference(scs_inference,[],[4329,4347,4353,534,257,225])).
% 60.49/60.52 cnf(4401,plain,
% 60.49/60.52 (P7(a16,a2,a16,a2,a18,a16,a18,a16)),
% 60.49/60.52 inference(scs_inference,[],[4329,4347,4351,4353,534,257,225,259])).
% 60.49/60.52 cnf(4403,plain,
% 60.49/60.52 (P7(a16,a2,a18,a16,a16,a2,a16,a18)),
% 60.49/60.52 inference(scs_inference,[],[4329,4347,4351,4353,534,257,225,259,256])).
% 60.49/60.52 cnf(4405,plain,
% 60.49/60.52 (P7(a2,a16,a18,a16,a16,a2,a18,a16)),
% 60.49/60.52 inference(scs_inference,[],[4329,4347,4351,4353,534,257,225,259,256,258])).
% 60.49/60.52 cnf(4409,plain,
% 60.49/60.52 (P8(a17,a2,a16,a15,x44091,x44092,x44091,x44092)),
% 60.49/60.52 inference(scs_inference,[],[4329,4347,4275,4351,4353,534,257,225,259,256,258,681,255])).
% 60.49/60.52 cnf(4413,plain,
% 60.49/60.52 (P1(a18,a2,a16)),
% 60.49/60.52 inference(scs_inference,[],[4329,4347,4275,4293,4297,4351,4353,534,257,225,259,256,258,681,255,226,153])).
% 60.49/60.52 cnf(4425,plain,
% 60.49/60.52 (P9(a2,a16,a2,a16)),
% 60.49/60.52 inference(scs_inference,[],[4329,4337,4347,4275,4293,4297,4339,4351,4353,534,257,225,259,256,258,681,255,226,153,592,224,652,612,662,233])).
% 60.49/60.52 cnf(4427,plain,
% 60.49/60.52 (P4(a16,a18,a18,a2)),
% 60.49/60.52 inference(scs_inference,[],[4329,4337,4347,4275,4293,4297,4339,4351,4353,534,257,225,259,256,258,681,255,226,153,592,224,652,612,662,233,168])).
% 60.49/60.52 cnf(4435,plain,
% 60.49/60.52 (P8(a2,a17,x44351,x44352,a16,a15,x44351,x44352)),
% 60.49/60.52 inference(scs_inference,[],[4329,4337,4347,4275,4277,4293,4297,4339,4351,4353,534,257,225,259,256,258,681,255,226,153,592,224,652,612,662,233,168,632,252,569,254])).
% 60.49/60.52 cnf(4437,plain,
% 60.49/60.52 (P1(a2,a2,a2)),
% 60.49/60.52 inference(scs_inference,[],[4329,4337,4347,4275,4277,4293,4297,4339,4351,4353,534,257,225,259,256,258,681,255,226,153,592,224,652,612,662,233,168,632,252,569,254,160])).
% 60.49/60.52 cnf(4439,plain,
% 60.49/60.52 (P1(a16,a18,a2)),
% 60.49/60.52 inference(scs_inference,[],[4329,4337,4347,4275,4277,4273,4293,4297,4339,4351,4353,534,257,225,259,256,258,681,255,226,153,592,224,652,612,662,233,168,632,252,569,254,160,151])).
% 60.49/60.52 cnf(4441,plain,
% 60.49/60.52 (P1(a2,a15,a1)),
% 60.49/60.52 inference(scs_inference,[],[4329,4337,4347,4275,4277,4273,4285,4293,4297,4339,4351,4353,534,257,225,259,256,258,681,255,226,153,592,224,652,612,662,233,168,632,252,569,254,160,151,152])).
% 60.49/60.52 cnf(4443,plain,
% 60.49/60.52 (P9(a16,a16,a18,a18)),
% 60.49/60.52 inference(scs_inference,[],[4329,4337,4347,4275,4277,4273,4285,4293,4297,4313,4339,4351,4353,534,257,225,259,256,258,681,255,226,153,592,224,652,612,662,233,168,632,252,569,254,160,151,152,163])).
% 60.49/60.52 cnf(4447,plain,
% 60.49/60.52 (P8(x44471,x44472,a17,a2,x44471,x44472,a16,a15)),
% 60.49/60.52 inference(scs_inference,[],[4329,4337,4347,4281,4275,4277,4273,4285,4293,4297,4313,4339,4351,4353,534,257,225,259,256,258,681,255,226,153,592,224,652,612,662,233,168,632,252,569,254,160,151,152,163,164,253])).
% 60.49/60.52 cnf(4449,plain,
% 60.49/60.52 (P3(f25(a16,a2,a16,a2,a18,a18),a2,a16)),
% 60.49/60.52 inference(scs_inference,[],[4329,4337,4347,4281,4275,4277,4273,4285,4293,4297,4313,4339,4351,4353,4315,534,257,225,259,256,258,681,255,226,153,592,224,652,612,662,233,168,632,252,569,254,160,151,152,163,164,253,154])).
% 60.49/60.52 cnf(4451,plain,
% 60.49/60.52 (P10(a16,a2,a18,a18)),
% 60.49/60.52 inference(scs_inference,[],[4329,4337,4345,4347,4281,4275,4277,4273,4285,4293,4297,4313,4339,4351,4353,4315,534,257,225,259,256,258,681,255,226,153,592,224,652,612,662,233,168,632,252,569,254,160,151,152,163,164,253,154,165])).
% 60.49/60.52 cnf(4453,plain,
% 60.49/60.52 (P10(a18,a18,a2,a16)),
% 60.49/60.52 inference(scs_inference,[],[4329,4337,4345,4347,4281,4275,4277,4273,4285,4293,4297,4313,4339,4351,4353,4315,534,257,225,259,256,258,681,255,226,153,592,224,652,612,662,233,168,632,252,569,254,160,151,152,163,164,253,154,165,166])).
% 60.49/60.52 cnf(4459,plain,
% 60.49/60.52 (P9(a18,a18,a18,a18)),
% 60.49/60.52 inference(scs_inference,[],[4329,4337,4345,4347,4281,4275,4277,4273,4285,4293,4297,4313,4319,4339,4351,4353,4377,4315,534,257,225,259,256,258,681,255,226,153,592,224,652,612,662,233,168,632,252,569,254,160,151,152,163,164,253,154,165,166,167,156,180])).
% 60.49/60.52 cnf(4464,plain,
% 60.49/60.52 (P7(a18,a16,a18,a16,a18,a16,a18,a16)),
% 60.49/60.52 inference(scs_inference,[],[4329,4337,4345,4347,4281,4275,4277,4309,4273,4285,4293,4297,4313,4319,4339,4351,4353,4355,4377,4315,4385,534,257,225,259,256,258,681,255,226,153,592,224,652,612,662,233,168,632,252,569,254,160,151,152,163,164,253,154,165,166,167,156,180,236,263])).
% 60.49/60.52 cnf(4468,plain,
% 60.51/60.52 (P7(a18,a2,a2,a16,a18,a2,a2,a16)),
% 60.51/60.52 inference(scs_inference,[],[4329,4337,4345,4347,4281,4275,4277,4309,4273,4285,4293,4297,4313,4319,4339,4351,4353,4355,4377,4315,4385,534,257,225,259,256,258,681,255,226,153,592,224,652,612,662,233,168,632,252,569,254,160,151,152,163,164,253,154,165,166,167,156,180,236,263,205,223])).
% 60.51/60.52 cnf(4476,plain,
% 60.51/60.52 (P5(a2,a2,a2,a2)),
% 60.51/60.52 inference(scs_inference,[],[4329,4331,4337,4345,4347,4281,4295,4275,4277,4309,4273,4285,4293,4297,4313,4319,4339,4351,4353,4355,4377,4315,4385,534,257,225,259,256,258,681,255,226,153,592,224,652,612,662,233,168,632,252,569,254,160,151,152,163,164,253,154,165,166,167,156,180,236,263,205,223,204,194,184,185])).
% 60.51/60.52 cnf(4483,plain,
% 60.51/60.52 (P1(f12(a16,a2,a2,a17,a17),a17,a17)),
% 60.51/60.52 inference(scs_inference,[],[4329,4331,4337,4345,4347,4281,4295,4275,4277,4287,4309,4273,4285,4289,4293,4297,4313,4319,4321,4339,4351,4353,4355,4377,4315,4385,534,257,225,259,256,258,681,255,226,153,592,224,652,612,662,233,168,632,252,569,254,160,151,152,163,164,253,154,165,166,167,156,180,236,263,205,223,204,194,184,185,193,240,197])).
% 60.51/60.52 cnf(4485,plain,
% 60.51/60.52 (P1(a2,a2,a18)),
% 60.51/60.52 inference(scs_inference,[],[4329,4331,4337,4345,4347,4281,4295,4275,4277,4287,4309,4273,4285,4289,4293,4297,4313,4319,4321,4339,4351,4353,4355,4377,4315,4385,534,257,225,259,256,258,681,255,226,153,592,224,652,612,662,233,168,632,252,569,254,160,151,152,163,164,253,154,165,166,167,156,180,236,263,205,223,204,194,184,185,193,240,197,155])).
% 60.51/60.52 cnf(4487,plain,
% 60.51/60.52 (P10(a16,a16,a16,a2)),
% 60.51/60.52 inference(scs_inference,[],[4329,4331,4337,4345,4347,4281,4295,4275,4277,4287,4309,4273,4285,4289,4293,4297,4313,4319,4321,4339,4351,4353,4355,4377,4315,4385,534,257,225,259,256,258,681,255,226,153,592,224,652,612,662,233,168,632,252,569,254,160,151,152,163,164,253,154,165,166,167,156,180,236,263,205,223,204,194,184,185,193,240,197,155,182])).
% 60.51/60.52 cnf(4489,plain,
% 60.51/60.52 (P3(f25(a2,a16,a2,a16,a18,a18),a2,a16)),
% 60.51/60.52 inference(scs_inference,[],[4329,4331,4337,4345,4347,4281,4295,4275,4277,4287,4309,4273,4285,4289,4293,4297,4313,4319,4321,4339,4351,4353,4355,4377,4315,4385,534,257,225,259,256,258,681,255,226,153,592,224,652,612,662,233,168,632,252,569,254,160,151,152,163,164,253,154,165,166,167,156,180,236,263,205,223,204,194,184,185,193,240,197,155,182,203])).
% 60.51/60.52 cnf(4491,plain,
% 60.51/60.52 (P10(a2,a16,a16,a16)),
% 60.51/60.52 inference(scs_inference,[],[4329,4331,4337,4345,4347,4281,4295,4275,4277,4287,4309,4273,4285,4289,4293,4297,4313,4319,4321,4339,4351,4353,4355,4377,4315,4385,534,257,225,259,256,258,681,255,226,153,592,224,652,612,662,233,168,632,252,569,254,160,151,152,163,164,253,154,165,166,167,156,180,236,263,205,223,204,194,184,185,193,240,197,155,182,203,172])).
% 60.51/60.52 cnf(4495,plain,
% 60.51/60.52 (P10(a2,a16,a18,a18)),
% 60.51/60.52 inference(scs_inference,[],[4329,4331,4337,4345,4347,4281,4295,4275,4277,4287,4309,4273,4285,4289,4293,4297,4313,4319,4321,4339,4351,4353,4355,4377,4315,4385,534,257,225,259,256,258,681,255,226,153,592,224,652,612,662,233,168,632,252,569,254,160,151,152,163,164,253,154,165,166,167,156,180,236,263,205,223,204,194,184,185,193,240,197,155,182,203,172,198,181])).
% 60.51/60.52 cnf(4497,plain,
% 60.51/60.52 (P4(a16,a2,a16,a2)),
% 60.51/60.52 inference(scs_inference,[],[4329,4331,4337,4345,4347,4281,4295,4275,4277,4287,4309,4273,4285,4289,4293,4297,4299,4313,4319,4321,4339,4351,4353,4355,4377,4315,4385,534,257,225,259,256,258,681,255,226,153,592,224,652,612,662,233,168,632,252,569,254,160,151,152,163,164,253,154,165,166,167,156,180,236,263,205,223,204,194,184,185,193,240,197,155,182,203,172,198,181,243])).
% 60.51/60.52 cnf(4499,plain,
% 60.51/60.52 (P5(a2,a16,a16,a16)),
% 60.51/60.52 inference(scs_inference,[],[4329,4331,4337,4345,4347,4281,4295,4275,4277,4287,4309,4273,4285,4289,4293,4297,4299,4313,4319,4321,4339,4351,4353,4355,4377,4315,4385,534,257,225,259,256,258,681,255,226,153,592,224,652,612,662,233,168,632,252,569,254,160,151,152,163,164,253,154,165,166,167,156,180,236,263,205,223,204,194,184,185,193,240,197,155,182,203,172,198,181,243,196])).
% 60.51/60.52 cnf(4505,plain,
% 60.51/60.52 (P4(a2,a2,a2,a2)),
% 60.51/60.52 inference(scs_inference,[],[4329,4331,4337,4345,4347,4281,4295,4275,4277,4287,4309,4273,4285,4289,4293,4297,4299,4313,4317,4319,4321,4339,4351,4353,4355,4377,4315,4385,534,257,225,259,256,258,681,255,226,153,592,224,652,612,662,233,168,632,252,569,254,160,151,152,163,164,253,154,165,166,167,156,180,236,263,205,223,204,194,184,185,193,240,197,155,182,203,172,198,181,243,196,206,207,251])).
% 60.51/60.52 cnf(4507,plain,
% 60.51/60.52 (P7(a16,a18,a18,a2,a16,a18,a18,a2)),
% 60.51/60.52 inference(scs_inference,[],[4329,4331,4337,4345,4347,4281,4295,4275,4277,4287,4309,4273,4285,4289,4293,4297,4299,4313,4317,4319,4321,4339,4351,4353,4355,4377,4315,4385,534,257,225,259,256,258,681,255,226,153,592,224,652,612,662,233,168,632,252,569,254,160,151,152,163,164,253,154,165,166,167,156,180,236,263,205,223,204,194,184,185,193,240,197,155,182,203,172,198,181,243,196,206,207,251,832])).
% 60.51/60.52 cnf(4509,plain,
% 60.51/60.52 (P4(a16,a18,a16,a18)),
% 60.51/60.52 inference(scs_inference,[],[4329,4331,4337,4345,4347,4281,4295,4275,4277,4287,4309,4273,4285,4289,4293,4297,4299,4313,4317,4319,4321,4339,4351,4353,4355,4377,4315,4385,534,257,225,259,256,258,681,255,226,153,592,224,652,612,662,233,168,632,252,569,254,160,151,152,163,164,253,154,165,166,167,156,180,236,263,205,223,204,194,184,185,193,240,197,155,182,203,172,198,181,243,196,206,207,251,832,444])).
% 60.51/60.52 cnf(4511,plain,
% 60.51/60.52 (P5(a16,f22(a16,a16,a18,a18),a16,a15)),
% 60.51/60.52 inference(scs_inference,[],[4329,4331,4337,4345,4347,4281,4295,4275,4277,4287,4309,4273,4285,4289,4293,4297,4299,4313,4317,4319,4321,4339,4351,4353,4355,4377,4315,4385,534,257,225,259,256,258,681,255,226,153,592,224,652,612,662,233,168,632,252,569,254,160,151,152,163,164,253,154,165,166,167,156,180,236,263,205,223,204,194,184,185,193,240,197,155,182,203,172,198,181,243,196,206,207,251,832,444,2686])).
% 60.51/60.52 cnf(4513,plain,
% 60.51/60.52 (P5(a16,f22(a16,a16,a18,a18),a15,a16)),
% 60.51/60.52 inference(scs_inference,[],[4329,4331,4337,4345,4347,4281,4295,4275,4277,4287,4309,4273,4285,4289,4293,4297,4299,4313,4317,4319,4321,4339,4351,4353,4355,4377,4315,4385,534,257,225,259,256,258,681,255,226,153,592,224,652,612,662,233,168,632,252,569,254,160,151,152,163,164,253,154,165,166,167,156,180,236,263,205,223,204,194,184,185,193,240,197,155,182,203,172,198,181,243,196,206,207,251,832,444,2686,171])).
% 60.51/60.52 cnf(4515,plain,
% 60.51/60.52 (P5(f22(a16,a16,a18,a18),a15,a16,a16)),
% 60.51/60.52 inference(scs_inference,[],[4329,4331,4337,4345,4347,4281,4295,4275,4277,4287,4309,4273,4285,4289,4293,4297,4299,4313,4317,4319,4321,4339,4351,4353,4355,4377,4315,4385,534,257,225,259,256,258,681,255,226,153,592,224,652,612,662,233,168,632,252,569,254,160,151,152,163,164,253,154,165,166,167,156,180,236,263,205,223,204,194,184,185,193,240,197,155,182,203,172,198,181,243,196,206,207,251,832,444,2686,171,169])).
% 60.51/60.52 cnf(4517,plain,
% 60.51/60.52 (P5(a15,a16,f22(a16,a16,a18,a18),a16)),
% 60.51/60.52 inference(scs_inference,[],[4329,4331,4337,4345,4347,4281,4295,4275,4277,4287,4309,4273,4285,4289,4293,4297,4299,4313,4317,4319,4321,4339,4351,4353,4355,4377,4315,4385,534,257,225,259,256,258,681,255,226,153,592,224,652,612,662,233,168,632,252,569,254,160,151,152,163,164,253,154,165,166,167,156,180,236,263,205,223,204,194,184,185,193,240,197,155,182,203,172,198,181,243,196,206,207,251,832,444,2686,171,169,170])).
% 60.51/60.52 cnf(4519,plain,
% 60.51/60.52 (P9(a15,a16,a2,a17)),
% 60.51/60.52 inference(scs_inference,[],[4329,4331,4337,4345,4347,4281,4295,4275,4277,4287,4309,4273,4285,4289,4293,4297,4299,4313,4317,4319,4321,4339,4351,4353,4355,4377,4315,4385,534,257,225,259,256,258,681,255,226,153,592,224,652,612,662,233,168,632,252,569,254,160,151,152,163,164,253,154,165,166,167,156,180,236,263,205,223,204,194,184,185,193,240,197,155,182,203,172,198,181,243,196,206,207,251,832,444,2686,171,169,170,480])).
% 60.51/60.52 cnf(4529,plain,
% 60.51/60.52 (P4(a16,a2,a16,f27(a2,a16,a2,a2,a16))),
% 60.51/60.52 inference(scs_inference,[],[4329,4331,4337,4345,4347,4281,4295,4275,4277,4287,4309,4273,4285,4289,4293,4297,4299,4313,4317,4319,4321,4339,4351,4353,4355,4377,4315,4385,534,257,225,259,256,258,681,255,226,153,592,224,652,612,662,233,168,632,252,569,254,160,151,152,163,164,253,154,165,166,167,156,180,236,263,205,223,204,194,184,185,193,240,197,155,182,203,172,198,181,243,196,206,207,251,832,444,2686,171,169,170,480,187,176,177,178,199])).
% 60.51/60.52 cnf(4533,plain,
% 60.51/60.52 (P9(f27(a2,a16,a2,a2,a16),a2,a2,a16)),
% 60.51/60.52 inference(scs_inference,[],[4329,4331,4337,4345,4347,4281,4295,4275,4277,4287,4309,4273,4285,4289,4293,4297,4299,4313,4317,4319,4321,4339,4351,4353,4355,4377,4315,4385,534,257,225,259,256,258,681,255,226,153,592,224,652,612,662,233,168,632,252,569,254,160,151,152,163,164,253,154,165,166,167,156,180,236,263,205,223,204,194,184,185,193,240,197,155,182,203,172,198,181,243,196,206,207,251,832,444,2686,171,169,170,480,187,176,177,178,199,200,201])).
% 60.51/60.52 cnf(4535,plain,
% 60.51/60.52 (P1(a2,a2,f23(a2,a2,a2,a2))),
% 60.51/60.52 inference(scs_inference,[],[4329,4331,4337,4345,4347,4281,4295,4275,4277,4287,4309,4273,4285,4289,4293,4297,4299,4313,4317,4319,4321,4339,4351,4353,4355,4377,4315,4385,534,257,225,259,256,258,681,255,226,153,592,224,652,612,662,233,168,632,252,569,254,160,151,152,163,164,253,154,165,166,167,156,180,236,263,205,223,204,194,184,185,193,240,197,155,182,203,172,198,181,243,196,206,207,251,832,444,2686,171,169,170,480,187,176,177,178,199,200,201,245])).
% 60.51/60.52 cnf(4537,plain,
% 60.51/60.52 (P1(f23(a2,a2,a2,a2),a2,a2)),
% 60.51/60.52 inference(scs_inference,[],[4329,4331,4337,4345,4347,4281,4295,4275,4277,4287,4309,4273,4285,4289,4293,4297,4299,4313,4317,4319,4321,4339,4351,4353,4355,4377,4315,4385,534,257,225,259,256,258,681,255,226,153,592,224,652,612,662,233,168,632,252,569,254,160,151,152,163,164,253,154,165,166,167,156,180,236,263,205,223,204,194,184,185,193,240,197,155,182,203,172,198,181,243,196,206,207,251,832,444,2686,171,169,170,480,187,176,177,178,199,200,201,245,249])).
% 60.51/60.52 cnf(4563,plain,
% 60.51/60.52 (P7(a18,a16,a16,a18,a16,a2,a16,a2)),
% 60.51/60.52 inference(scs_inference,[],[4391,259])).
% 60.51/60.52 cnf(4565,plain,
% 60.51/60.52 (~P7(a2,a1,a1,a20,a16,a18,a16,a18)),
% 60.51/60.52 inference(scs_inference,[],[4391,4509,259,534])).
% 60.51/60.52 cnf(4567,plain,
% 60.51/60.52 (P9(f27(a2,a16,a2,a2,a16),a2,a15,a17)),
% 60.51/60.52 inference(scs_inference,[],[4391,4509,4533,259,534,497])).
% 60.51/60.52 cnf(4569,plain,
% 60.51/60.52 (P7(a18,a16,a2,a16,a18,a16,a16,a2)),
% 60.51/60.52 inference(scs_inference,[],[4391,4509,4405,4533,259,534,497,257])).
% 60.51/60.52 cnf(4571,plain,
% 60.51/60.52 (P8(a2,a2,a2,a2,x45711,x45712,x45711,x45712)),
% 60.51/60.52 inference(scs_inference,[],[4391,4509,4399,4405,4533,259,534,497,257,255])).
% 60.51/60.52 cnf(4577,plain,
% 60.51/60.52 (P5(a15,a16,a16,f22(a16,a16,a18,a18))),
% 60.51/60.52 inference(scs_inference,[],[4391,4509,4399,4405,4449,4533,4517,259,534,497,257,255,226,153,171])).
% 60.51/60.52 cnf(4579,plain,
% 60.51/60.52 (P8(a17,a2,x45791,x45792,a2,a17,x45791,x45792)),
% 60.51/60.52 inference(scs_inference,[],[4343,4391,4509,4399,4405,4449,4533,4517,259,534,497,257,255,226,153,171,225])).
% 60.51/60.52 cnf(4583,plain,
% 60.51/60.52 (P5(a16,a16,a16,a2)),
% 60.51/60.52 inference(scs_inference,[],[4335,4343,4391,4509,4399,4405,4499,4449,4533,4517,259,534,497,257,255,226,153,171,225,224,2686])).
% 60.51/60.52 cnf(4585,plain,
% 60.51/60.52 (P4(a16,a18,a18,a16)),
% 60.51/60.52 inference(scs_inference,[],[4335,4343,4391,4509,4399,4405,4499,4449,4533,4517,259,534,497,257,255,226,153,171,225,224,2686,168])).
% 60.51/60.52 cnf(4587,plain,
% 60.51/60.52 (P7(a16,a2,a18,a16,a2,a16,a18,a16)),
% 60.51/60.52 inference(scs_inference,[],[4335,4343,4391,4509,4399,4405,4499,4449,4533,4517,259,534,497,257,255,226,153,171,225,224,2686,168,256])).
% 60.51/60.52 cnf(4591,plain,
% 60.51/60.52 (P7(a16,a18,a16,a2,a16,a18,a16,a2)),
% 60.51/60.52 inference(scs_inference,[],[4335,4343,4341,4391,4509,4399,4405,4499,4449,4533,4517,259,534,497,257,255,226,153,171,225,224,2686,168,256,252,258])).
% 60.51/60.52 cnf(4607,plain,
% 60.51/60.52 (P5(a16,a2,a16,a16)),
% 60.51/60.52 inference(scs_inference,[],[4335,4343,4341,4391,4509,4399,4405,4499,4449,4533,4511,4517,259,534,497,257,255,226,153,171,225,224,2686,168,256,252,258,632,681,170,662,612,592,569,169])).
% 60.51/60.52 cnf(4611,plain,
% 60.51/60.52 (P1(a16,a15,a15)),
% 60.51/60.52 inference(scs_inference,[],[4335,4327,4343,4341,4391,4509,4399,4435,4405,4499,4449,4533,4511,4517,259,534,497,257,255,226,153,171,225,224,2686,168,256,252,258,632,681,170,662,612,592,569,169,233,160])).
% 60.51/60.52 cnf(4613,plain,
% 60.51/60.52 (~P7(a20,a1,a2,a1,a16,a18,a16,a18)),
% 60.51/60.52 inference(scs_inference,[],[4335,4327,4343,4341,4391,4509,4399,4435,4405,4499,4449,4533,4511,4517,259,534,497,257,255,226,153,171,225,224,2686,168,256,252,258,632,681,170,662,612,592,569,169,233,160,652])).
% 60.51/60.52 cnf(4615,plain,
% 60.51/60.52 (P1(a15,a1,a2)),
% 60.51/60.52 inference(scs_inference,[],[4335,4327,4343,4279,4341,4391,4509,4399,4435,4405,4499,4449,4533,4511,4517,259,534,497,257,255,226,153,171,225,224,2686,168,256,252,258,632,681,170,662,612,592,569,169,233,160,652,151])).
% 60.51/60.52 cnf(4617,plain,
% 60.51/60.52 (P1(a16,a2,a18)),
% 60.51/60.52 inference(scs_inference,[],[4335,4327,4343,4279,4341,4391,4509,4399,4435,4405,4439,4499,4449,4533,4511,4517,259,534,497,257,255,226,153,171,225,224,2686,168,256,252,258,632,681,170,662,612,592,569,169,233,160,652,151,152])).
% 60.51/60.52 cnf(4621,plain,
% 60.51/60.52 (P9(a16,a15,a15,a16)),
% 60.51/60.52 inference(scs_inference,[],[4335,4327,4343,4279,4341,4391,4509,4399,4435,4405,4439,4499,4449,4533,4511,4517,259,534,497,257,255,226,153,171,225,224,2686,168,256,252,258,632,681,170,662,612,592,569,169,233,160,652,151,152,254,164])).
% 60.51/60.52 cnf(4623,plain,
% 60.51/60.52 (P9(a2,a17,a15,a16)),
% 60.51/60.52 inference(scs_inference,[],[4335,4327,4343,4279,4341,4391,4509,4399,4435,4405,4439,4499,4519,4449,4533,4511,4517,259,534,497,257,255,226,153,171,225,224,2686,168,256,252,258,632,681,170,662,612,592,569,169,233,160,652,151,152,254,164,163])).
% 60.51/60.52 cnf(4627,plain,
% 60.51/60.52 (P3(f25(a2,a16,a2,a16,a18,a18),a16,a2)),
% 60.51/60.52 inference(scs_inference,[],[4335,4327,4343,4279,4341,4391,4509,4399,4435,4405,4439,4499,4519,4449,4489,4533,4511,4517,259,534,497,257,255,226,153,171,225,224,2686,168,256,252,258,632,681,170,662,612,592,569,169,233,160,652,151,152,254,164,163,253,154])).
% 60.51/60.52 cnf(4633,plain,
% 60.51/60.52 (P4(a2,a18,a18,a16)),
% 60.51/60.52 inference(scs_inference,[],[4335,4327,4343,4279,4341,4391,4509,4399,4435,4375,4405,4439,4487,4499,4519,4449,4489,4533,4511,4517,259,534,497,257,255,226,153,171,225,224,2686,168,256,252,258,632,681,170,662,612,592,569,169,233,160,652,151,152,254,164,163,253,154,165,166,167])).
% 60.51/60.52 cnf(4645,plain,
% 60.51/60.52 (P5(a2,a18,a2,a2)),
% 60.51/60.52 inference(scs_inference,[],[4335,4327,4343,4279,4341,4391,4509,4399,4435,4375,4405,4439,4485,4487,4491,4499,4505,4519,4449,4489,4533,4511,4517,146,259,534,497,257,255,226,153,171,225,224,2686,168,256,252,258,632,681,170,662,612,592,569,169,233,160,652,151,152,254,164,163,253,154,165,166,167,156,200,177,199,204,236])).
% 60.51/60.52 cnf(4648,plain,
% 60.51/60.52 (P9(f25(a15,a17,a15,a17,a19,a19),a19,a17,a17)),
% 60.51/60.52 inference(scs_inference,[],[4335,4327,4343,4279,4341,4391,4509,4399,4435,4375,4405,4439,4485,4487,4491,4499,4505,4519,4449,4489,4533,4511,4517,146,259,534,497,257,255,226,153,171,225,224,2686,168,256,252,258,632,681,170,662,612,592,569,169,233,160,652,151,152,254,164,163,253,154,165,166,167,156,200,177,199,204,236,205])).
% 60.51/60.52 cnf(4652,plain,
% 60.51/60.52 (P1(f22(a18,a18,a16,a2),a16,a2)),
% 60.51/60.52 inference(scs_inference,[],[4335,4451,4327,4343,4279,4341,4391,4509,4399,4435,4375,4405,4439,4485,4487,4491,4499,4505,4519,4449,4489,4533,4511,4517,146,259,534,497,257,255,226,153,171,225,224,2686,168,256,252,258,632,681,170,662,612,592,569,169,233,160,652,151,152,254,164,163,253,154,165,166,167,156,200,177,199,204,236,205,178,194])).
% 60.51/60.52 cnf(4664,plain,
% 60.51/60.52 (P2(f8(a16,a2,a16),a16,a2,a16)),
% 60.51/60.52 inference(scs_inference,[],[4335,4451,4327,4343,4279,4341,4391,4509,4399,4435,4375,4405,4437,4439,4485,4487,4491,4499,4505,4519,4449,4489,4533,4511,4517,146,259,534,497,257,255,226,153,171,225,224,2686,168,256,252,258,632,681,170,662,612,592,569,169,233,160,652,151,152,254,164,163,253,154,165,166,167,156,200,177,199,204,236,205,178,194,201,223,193,197,189,191])).
% 60.51/60.52 cnf(4670,plain,
% 60.51/60.52 (P3(f25(a15,a17,a15,a17,a19,a19),a15,a17)),
% 60.51/60.52 inference(scs_inference,[],[4335,4451,4327,4343,4279,4341,4391,4509,4399,4435,4375,4405,4437,4439,4485,4487,4491,4499,4505,4519,4449,4489,4533,4511,4517,146,259,534,497,257,255,226,153,171,225,224,2686,168,256,252,258,632,681,170,662,612,592,569,169,233,160,652,151,152,254,164,163,253,154,165,166,167,156,200,177,199,204,236,205,178,194,201,223,193,197,189,191,184,190,203])).
% 60.51/60.52 cnf(4676,plain,
% 60.51/60.52 (P10(a16,a16,a2,a2)),
% 60.51/60.52 inference(scs_inference,[],[4335,4451,4327,4343,4279,4341,4391,4509,4399,4435,4375,4405,4437,4439,4485,4487,4491,4497,4499,4505,4519,4449,4489,4533,4511,4517,298,146,259,534,497,257,255,226,153,171,225,224,2686,168,256,252,258,632,681,170,662,612,592,569,169,233,160,652,151,152,254,164,163,253,154,165,166,167,156,200,177,199,204,236,205,178,194,201,223,193,197,189,191,184,190,203,198,243,181])).
% 60.51/60.52 cnf(4678,plain,
% 60.51/60.52 (P10(a2,a2,a2,a2)),
% 60.51/60.52 inference(scs_inference,[],[4335,4451,4327,4343,4279,4341,4391,4509,4399,4435,4375,4405,4437,4439,4476,4485,4487,4491,4497,4499,4505,4519,4449,4489,4533,4511,4517,298,146,259,534,497,257,255,226,153,171,225,224,2686,168,256,252,258,632,681,170,662,612,592,569,169,233,160,652,151,152,254,164,163,253,154,165,166,167,156,200,177,199,204,236,205,178,194,201,223,193,197,189,191,184,190,203,198,243,181,195])).
% 60.51/60.52 cnf(4680,plain,
% 60.51/60.52 (P10(a18,a18,a2,a2)),
% 60.51/60.52 inference(scs_inference,[],[4335,4451,4327,4343,4279,4341,4391,4509,4399,4435,4375,4405,4437,4439,4476,4485,4487,4491,4497,4499,4505,4519,4449,4489,4533,4511,4517,298,146,259,534,497,257,255,226,153,171,225,224,2686,168,256,252,258,632,681,170,662,612,592,569,169,233,160,652,151,152,254,164,163,253,154,165,166,167,156,200,177,199,204,236,205,178,194,201,223,193,197,189,191,184,190,203,198,243,181,195,589])).
% 60.51/60.52 cnf(4692,plain,
% 60.51/60.52 (P4(a2,a2,a2,f3(a2,a2,a2))),
% 60.51/60.52 inference(scs_inference,[],[4335,4451,4327,4343,4279,4341,4391,4509,4399,4435,4375,4405,4437,4439,4476,4485,4487,4491,4497,4499,4505,4519,4449,4489,4533,4511,4517,298,327,146,259,534,497,257,255,226,153,171,225,224,2686,168,256,252,258,632,681,170,662,612,592,569,169,233,160,652,151,152,254,164,163,253,154,165,166,167,156,200,177,199,204,236,205,178,194,201,223,193,197,189,191,184,190,203,198,243,181,195,589,824,587,671,187,235,188])).
% 60.51/60.52 cnf(4731,plain,
% 60.51/60.52 (P3(x47311,a16,a17)+~P3(x47311,a2,a15)),
% 60.51/60.52 inference(scs_inference,[],[4623,840])).
% 60.51/60.52 cnf(4732,plain,
% 60.51/60.52 (P7(a16,a18,a16,a18,a18,a2,a18,a2)),
% 60.51/60.52 inference(scs_inference,[],[4507,259])).
% 60.51/60.52 cnf(4736,plain,
% 60.51/60.52 (P10(a18,a18,a18,a18)),
% 60.51/60.52 inference(scs_inference,[],[4680,4507,259,257,587])).
% 60.51/60.52 cnf(4742,plain,
% 60.51/60.52 (P5(a16,a16,a2,a16)),
% 60.51/60.52 inference(scs_inference,[],[4680,4507,4427,4583,4652,259,257,587,534,824,171])).
% 60.51/60.52 cnf(4744,plain,
% 60.51/60.52 (P8(a16,a16,a16,a16,a2,a16,a2,a16)),
% 60.51/60.52 inference(scs_inference,[],[4680,4507,4427,4583,4652,259,257,587,534,824,171,224])).
% 60.51/60.52 cnf(4746,plain,
% 60.51/60.52 (P8(a2,a17,x47461,x47462,a2,a17,x47461,x47462)),
% 60.51/60.52 inference(scs_inference,[],[4680,4507,4283,4427,4583,4652,259,257,587,534,824,171,224,225])).
% 60.51/60.52 cnf(4752,plain,
% 60.51/60.52 (P8(x47521,x47522,x47521,x47522,a17,a2,a16,a15)),
% 60.51/60.52 inference(scs_inference,[],[4680,4507,4283,4447,4427,4583,4529,4652,259,257,587,534,824,171,224,225,681,168,255])).
% 60.51/60.52 cnf(4754,plain,
% 60.51/60.52 (P5(a2,a2,a18,a2)),
% 60.51/60.52 inference(scs_inference,[],[4680,4507,4283,4447,4427,4583,4645,4529,4652,259,257,587,534,824,171,224,225,681,168,255,170])).
% 60.51/60.52 cnf(4762,plain,
% 60.51/60.52 (P7(a18,a16,a18,a2,a16,a18,a18,a2)),
% 60.51/60.52 inference(scs_inference,[],[4680,4507,4283,4447,4427,4583,4645,4529,4627,4652,259,257,587,534,824,171,224,225,681,168,255,170,662,226,153,258])).
% 60.51/60.52 cnf(4764,plain,
% 60.51/60.52 (P8(x47641,x47642,x47641,x47642,a2,a2,a2,a2)),
% 60.51/60.52 inference(scs_inference,[],[4680,4507,4283,4447,4571,4427,4583,4645,4529,4627,4652,259,257,587,534,824,171,224,225,681,168,255,170,662,226,153,258,252])).
% 60.51/60.52 cnf(4772,plain,
% 60.51/60.52 (P7(a16,a2,a16,a2,a18,a16,a16,a18)),
% 60.51/60.52 inference(scs_inference,[],[4680,4507,4283,4447,4571,4427,4563,4583,4645,4529,4627,4515,4652,259,257,587,534,824,171,224,225,681,168,255,170,662,226,153,258,252,632,2686,612,256])).
% 60.51/60.52 cnf(4780,plain,
% 60.51/60.52 (P1(a15,a2,a1)),
% 60.51/60.52 inference(scs_inference,[],[4680,4507,4283,4447,4571,4427,4563,4583,4615,4645,4529,4627,4515,4652,259,257,587,534,824,171,224,225,681,168,255,170,662,226,153,258,252,632,2686,612,256,569,169,652,152])).
% 60.51/60.52 cnf(4784,plain,
% 60.51/60.52 (P9(a2,a16,a16,a2)),
% 60.51/60.52 inference(scs_inference,[],[4680,4507,4283,4447,4571,4425,4427,4563,4583,4615,4645,4529,4627,4515,4652,259,257,587,534,824,171,224,225,681,168,255,170,662,226,153,258,252,632,2686,612,256,569,169,652,152,592,164])).
% 60.51/60.52 cnf(4786,plain,
% 60.51/60.52 (P8(x47861,x47862,a17,a2,x47862,x47861,a16,a15)),
% 60.51/60.52 inference(scs_inference,[],[4680,4507,4283,4447,4571,4425,4427,4563,4583,4615,4645,4529,4627,4515,4652,259,257,587,534,824,171,224,225,681,168,255,170,662,226,153,258,252,632,2686,612,256,569,169,652,152,592,164,254])).
% 60.51/60.52 cnf(4788,plain,
% 60.51/60.52 (P1(a17,a2,a2)),
% 60.51/60.52 inference(scs_inference,[],[4680,4507,4283,4447,4571,4311,4425,4427,4563,4583,4615,4645,4529,4627,4515,4652,259,257,587,534,824,171,224,225,681,168,255,170,662,226,153,258,252,632,2686,612,256,569,169,652,152,592,164,254,160])).
% 60.51/60.52 cnf(4790,plain,
% 60.51/60.52 (P1(a2,a18,a16)),
% 60.51/60.52 inference(scs_inference,[],[4680,4507,4283,4413,4447,4571,4311,4425,4427,4563,4583,4615,4645,4529,4627,4515,4652,259,257,587,534,824,171,224,225,681,168,255,170,662,226,153,258,252,632,2686,612,256,569,169,652,152,592,164,254,160,151])).
% 60.51/60.52 cnf(4794,plain,
% 60.51/60.52 (P8(x47941,x47942,a17,a2,x47941,x47942,a2,a17)),
% 60.51/60.52 inference(scs_inference,[],[4680,4507,4283,4413,4447,4571,4579,4311,4425,4427,4563,4583,4615,4645,4648,4529,4627,4515,4652,259,257,587,534,824,171,224,225,681,168,255,170,662,226,153,258,252,632,2686,612,256,569,169,652,152,592,164,254,160,151,163,253])).
% 60.51/60.52 cnf(4802,plain,
% 60.51/60.52 (P4(a18,a2,a16,a18)),
% 60.51/60.52 inference(scs_inference,[],[4680,4507,4283,4413,4447,4571,4579,4311,4425,4427,4563,4583,4615,4645,4349,4648,4529,4627,4670,4515,4652,259,257,587,534,824,171,224,225,681,168,255,170,662,226,153,258,252,632,2686,612,256,569,169,652,152,592,164,254,160,151,163,253,154,165,166,167])).
% 60.51/60.52 cnf(4806,plain,
% 60.51/60.52 (P1(f14(a2,a2,a2,a2),a2,a2)),
% 60.51/60.52 inference(scs_inference,[],[4680,4507,4283,4678,4413,4447,4571,4579,4311,4425,4427,4563,4583,4615,4645,4349,4648,4529,4627,4670,4515,4652,259,257,587,534,824,171,224,225,681,168,255,170,662,226,153,258,252,632,2686,612,256,569,169,652,152,592,164,254,160,151,163,253,154,165,166,167,156,248])).
% 60.51/60.52 cnf(4807,plain,
% 60.51/60.52 (P8(a2,a2,a2,a2,x48071,x48072,x48071,x48072)),
% 60.51/60.52 inference(rename_variables,[],[4571])).
% 60.51/60.52 cnf(4809,plain,
% 60.51/60.52 (P1(a2,a2,f3(a2,a2,a2))),
% 60.51/60.52 inference(scs_inference,[],[4680,4507,4283,4678,4413,4447,4571,4579,4311,4425,4427,4563,4583,4615,4645,4349,4648,4529,4627,4670,4515,4652,4505,259,257,587,534,824,171,224,225,681,168,255,170,662,226,153,258,252,632,2686,612,256,569,169,652,152,592,164,254,160,151,163,253,154,165,166,167,156,248,176])).
% 60.51/60.52 cnf(4811,plain,
% 60.51/60.52 (P4(a2,a2,a2,f27(a2,a2,a2,a2,a2))),
% 60.51/60.52 inference(scs_inference,[],[4680,4507,4283,4678,4413,4447,4571,4579,4311,4425,4427,4563,4583,4615,4645,4349,4648,4529,4627,4670,4515,4652,4505,259,257,587,534,824,171,224,225,681,168,255,170,662,226,153,258,252,632,2686,612,256,569,169,652,152,592,164,254,160,151,163,253,154,165,166,167,156,248,176,200])).
% 60.51/60.52 cnf(4814,plain,
% 60.51/60.52 (P8(a2,a2,a2,a2,x48141,x48142,x48141,x48142)),
% 60.51/60.52 inference(rename_variables,[],[4571])).
% 60.51/60.52 cnf(4816,plain,
% 60.51/60.52 (P5(a2,f23(a2,a2,a2,a2),a2,a2)),
% 60.51/60.52 inference(scs_inference,[],[4680,4507,4283,4678,4413,4447,4571,4807,4579,4311,4425,4427,4563,4583,4615,4645,4349,4648,4535,4529,4627,4670,4515,4652,4399,4505,259,257,587,534,824,171,224,225,681,168,255,170,662,226,153,258,252,632,2686,612,256,569,169,652,152,592,164,254,160,151,163,253,154,165,166,167,156,248,176,200,246,236])).
% 60.51/60.52 cnf(4821,plain,
% 60.51/60.52 (P10(a2,a17,a16,a15)),
% 60.51/60.52 inference(scs_inference,[],[4680,4507,4283,4678,4413,4447,4571,4807,4579,4311,4425,4427,4563,4583,4615,4645,4349,4648,4535,4529,4627,4670,4515,4652,4409,4399,4505,259,257,587,534,824,171,224,225,681,168,255,170,662,226,153,258,252,632,2686,612,256,569,169,652,152,592,164,254,160,151,163,253,154,165,166,167,156,248,176,200,246,236,177,2036])).
% 60.51/60.52 cnf(4827,plain,
% 60.51/60.52 (P8(a2,a2,a2,a2,x48271,x48272,x48271,x48272)),
% 60.51/60.52 inference(rename_variables,[],[4571])).
% 60.51/60.52 cnf(4835,plain,
% 60.51/60.52 (P2(f8(a2,a2,a2),a2,a2,a2)),
% 60.51/60.52 inference(scs_inference,[],[4680,4507,4283,4676,4678,4413,4447,4571,4807,4814,4579,4311,4425,4427,4563,4583,4615,4645,4349,4648,4535,4529,4627,4670,4515,4652,4664,4409,4497,4489,4337,4399,4505,259,257,587,534,824,171,224,225,681,168,255,170,662,226,153,258,252,632,2686,612,256,569,169,652,152,592,164,254,160,151,163,253,154,165,166,167,156,248,176,200,246,236,177,2036,178,250,227,201,194,191])).
% 60.51/60.52 cnf(4845,plain,
% 60.51/60.52 (P10(a2,f4(a2,a2,a2),a2,a2)),
% 60.51/60.52 inference(scs_inference,[],[4680,4507,4283,4676,4678,4413,4447,4571,4807,4814,4579,4311,4425,4427,4441,4563,4583,4615,4645,4349,4648,4535,4529,4627,4670,4515,4652,4664,4409,4497,4489,4337,4399,4505,259,257,587,534,824,171,224,225,681,168,255,170,662,226,153,258,252,632,2686,612,256,569,169,652,152,592,164,254,160,151,163,253,154,165,166,167,156,248,176,200,246,236,177,2036,178,250,227,201,194,191,223,197,190,193,189])).
% 60.51/60.52 cnf(4849,plain,
% 60.51/60.52 (P10(a2,a17,a17,a2)),
% 60.51/60.52 inference(scs_inference,[],[4680,4507,4283,4676,4678,4413,4447,4571,4807,4814,4579,4311,4425,4427,4441,4563,4583,4615,4645,4349,4648,4535,4529,4627,4670,4515,4652,4664,4409,4497,4489,4337,4399,4505,259,257,587,534,824,171,224,225,681,168,255,170,662,226,153,258,252,632,2686,612,256,569,169,652,152,592,164,254,160,151,163,253,154,165,166,167,156,248,176,200,246,236,177,2036,178,250,227,201,194,191,223,197,190,193,189,184,241])).
% 60.51/60.52 cnf(4852,plain,
% 60.51/60.52 (P4(a18,a16,a16,a18)),
% 60.51/60.52 inference(scs_inference,[],[4680,4507,4283,4676,4678,4413,4447,4571,4807,4814,4579,4311,4425,4427,4441,4563,4583,4615,4645,4349,4648,4535,4529,4627,4670,4515,4652,4664,4409,4497,4489,4337,4399,4505,259,257,587,534,824,171,224,225,681,168,255,170,662,226,153,258,252,632,2686,612,256,569,169,652,152,592,164,254,160,151,163,253,154,165,166,167,156,248,176,200,246,236,177,2036,178,250,227,201,194,191,223,197,190,193,189,184,241,243])).
% 60.51/60.52 cnf(4856,plain,
% 60.51/60.52 (P3(a2,a2,a2)),
% 60.51/60.52 inference(scs_inference,[],[4680,4507,4283,4676,4678,4413,4447,4571,4807,4814,4827,4579,4311,4425,4427,4441,4563,4583,4615,4645,4349,4648,4535,4529,4627,4670,4515,4652,4664,4409,4497,4489,4337,4399,4505,4437,259,257,587,534,824,171,224,225,681,168,255,170,662,226,153,258,252,632,2686,612,256,569,169,652,152,592,164,254,160,151,163,253,154,165,166,167,156,248,176,200,246,236,177,2036,178,250,227,201,194,191,223,197,190,193,189,184,241,243,198,239])).
% 60.51/60.52 cnf(4857,plain,
% 60.51/60.52 (P8(a2,a2,a2,a2,x48571,x48572,x48571,x48572)),
% 60.51/60.52 inference(rename_variables,[],[4571])).
% 60.51/60.52 cnf(4859,plain,
% 60.51/60.52 (P3(a2,a17,a17)),
% 60.51/60.52 inference(scs_inference,[],[4680,4507,4283,4676,4678,4413,4447,4571,4807,4814,4827,4579,4311,4425,4427,4441,4563,4583,4615,4645,4349,4648,4535,4529,4627,4670,4515,4652,4664,4409,4497,4489,4337,4399,4505,4437,259,257,587,534,824,171,224,225,681,168,255,170,662,226,153,258,252,632,2686,612,256,569,169,652,152,592,164,254,160,151,163,253,154,165,166,167,156,248,176,200,246,236,177,2036,178,250,227,201,194,191,223,197,190,193,189,184,241,243,198,239,175])).
% 60.51/60.52 cnf(4861,plain,
% 60.51/60.52 (P3(f21(a2,x48611),a2,x48611)),
% 60.51/60.52 inference(scs_inference,[],[4680,4507,4283,4676,4678,4413,4447,4571,4807,4814,4827,4579,4311,4425,4427,4441,4563,4583,4615,4645,4349,4648,4535,4529,4627,4670,4515,4652,4664,4409,4497,4489,4337,4399,4505,4437,259,257,587,534,824,171,224,225,681,168,255,170,662,226,153,258,252,632,2686,612,256,569,169,652,152,592,164,254,160,151,163,253,154,165,166,167,156,248,176,200,246,236,177,2036,178,250,227,201,194,191,223,197,190,193,189,184,241,243,198,239,175,159])).
% 60.51/60.52 cnf(4865,plain,
% 60.51/60.52 (P1(f13(a2,a16,a16,a2,a18,a18),a16,a2)),
% 60.51/60.52 inference(scs_inference,[],[4680,4507,4283,4676,4678,4413,4447,4571,4807,4814,4827,4579,4311,4425,4427,4441,4563,4583,4615,4645,4349,4648,4535,4529,4627,4670,4515,4652,4664,4409,4497,4489,4337,4399,4273,4505,4437,259,257,587,534,824,171,224,225,681,168,255,170,662,226,153,258,252,632,2686,612,256,569,169,652,152,592,164,254,160,151,163,253,154,165,166,167,156,248,176,200,246,236,177,2036,178,250,227,201,194,191,223,197,190,193,189,184,241,243,198,239,175,159,206,207])).
% 60.51/60.52 cnf(4867,plain,
% 60.51/60.52 (P4(a2,a2,a16,a16)),
% 60.51/60.52 inference(scs_inference,[],[4680,4507,4283,4676,4678,4413,4447,4571,4807,4814,4827,4857,4579,4311,4425,4427,4441,4563,4583,4615,4645,4349,4648,4535,4529,4627,4670,4515,4652,4664,4409,4497,4489,4337,4399,4273,4505,4437,259,257,587,534,824,171,224,225,681,168,255,170,662,226,153,258,252,632,2686,612,256,569,169,652,152,592,164,254,160,151,163,253,154,165,166,167,156,248,176,200,246,236,177,2036,178,250,227,201,194,191,223,197,190,193,189,184,241,243,198,239,175,159,206,207,251])).
% 60.51/60.52 cnf(4872,plain,
% 60.51/60.52 (~P10(a1,f21(a2,a20),a20,a2)),
% 60.51/60.52 inference(scs_inference,[],[4680,4507,4283,4676,4678,4413,4447,4571,4807,4814,4827,4857,4579,4311,4425,4427,4441,4563,4583,4615,4645,4349,4648,4535,4529,4627,4670,4515,4652,4664,4409,4497,4489,4337,4399,4273,4505,4437,259,257,587,534,824,171,224,225,681,168,255,170,662,226,153,258,252,632,2686,612,256,569,169,652,152,592,164,254,160,151,163,253,154,165,166,167,156,248,176,200,246,236,177,2036,178,250,227,201,194,191,223,197,190,193,189,184,241,243,198,239,175,159,206,207,251,438,1053])).
% 60.51/60.52 cnf(4874,plain,
% 60.51/60.52 (~P11(f21(a2,a20),a2,a1,f21(a2,a20),a20,a1)),
% 60.51/60.52 inference(scs_inference,[],[4680,4507,4283,4676,4678,4413,4447,4571,4807,4814,4827,4857,4579,4311,4425,4427,4441,4563,4583,4615,4645,4349,4648,4535,4529,4627,4670,4515,4652,4664,4409,4497,4489,4337,4399,4273,4505,4437,259,257,587,534,824,171,224,225,681,168,255,170,662,226,153,258,252,632,2686,612,256,569,169,652,152,592,164,254,160,151,163,253,154,165,166,167,156,248,176,200,246,236,177,2036,178,250,227,201,194,191,223,197,190,193,189,184,241,243,198,239,175,159,206,207,251,438,1053,3297])).
% 60.51/60.52 cnf(4876,plain,
% 60.51/60.52 (P10(a16,a15,a15,a16)),
% 60.51/60.52 inference(scs_inference,[],[4680,4507,4283,4676,4678,4413,4447,4571,4807,4814,4827,4857,4579,4311,4425,4427,4441,4563,4583,4615,4645,4349,4648,4535,4529,4627,4670,4515,4652,4664,4409,4497,4489,4337,4399,4273,4505,4437,259,257,587,534,824,171,224,225,681,168,255,170,662,226,153,258,252,632,2686,612,256,569,169,652,152,592,164,254,160,151,163,253,154,165,166,167,156,248,176,200,246,236,177,2036,178,250,227,201,194,191,223,197,190,193,189,184,241,243,198,239,175,159,206,207,251,438,1053,3297,493])).
% 60.51/60.52 cnf(4889,plain,
% 60.51/60.52 (P3(f25(a2,a2,a2,a2,a2,a2),a2,a2)),
% 60.51/60.52 inference(scs_inference,[],[4680,4507,4283,4676,4678,4413,4447,4571,4807,4814,4827,4857,4579,4311,4425,4427,4441,4563,4583,4615,4645,4349,4648,4535,4529,4627,4670,4515,4652,4664,4409,4299,4497,4489,4337,4399,4273,4321,4505,4437,259,257,587,534,824,171,224,225,681,168,255,170,662,226,153,258,252,632,2686,612,256,569,169,652,152,592,164,254,160,151,163,253,154,165,166,167,156,248,176,200,246,236,177,2036,178,250,227,201,194,191,223,197,190,193,189,184,241,243,198,239,175,159,206,207,251,438,1053,3297,493,489,140,229,204,205,199,203])).
% 60.51/60.52 cnf(4891,plain,
% 60.51/60.52 (P2(f9(a2,a2,a2),a2,a2,a2)),
% 60.51/60.52 inference(scs_inference,[],[4680,4507,4283,4676,4678,4413,4447,4571,4807,4814,4827,4857,4579,4311,4425,4427,4441,4563,4583,4615,4645,4349,4648,4535,4529,4627,4670,4515,4652,4664,4409,4299,4497,4489,4337,4476,4399,4273,4321,4347,4505,4437,259,257,587,534,824,171,224,225,681,168,255,170,662,226,153,258,252,632,2686,612,256,569,169,652,152,592,164,254,160,151,163,253,154,165,166,167,156,248,176,200,246,236,177,2036,178,250,227,201,194,191,223,197,190,193,189,184,241,243,198,239,175,159,206,207,251,438,1053,3297,493,489,140,229,204,205,199,203,192])).
% 60.51/60.52 cnf(4895,plain,
% 60.51/60.52 (P1(f28(a16,a2,a16,a2,a18,a18),a16,a2)),
% 60.51/60.52 inference(scs_inference,[],[4680,4507,4283,4676,4678,4413,4447,4571,4807,4814,4827,4857,4579,4311,4425,4427,4441,4563,4583,4615,4617,4645,4349,4537,4648,4535,4529,4627,4670,4515,4652,4664,4409,4299,4497,4489,4337,4476,4399,4443,4273,4321,4347,4505,4437,306,147,259,257,587,534,824,171,224,225,681,168,255,170,662,226,153,258,252,632,2686,612,256,569,169,652,152,592,164,254,160,151,163,253,154,165,166,167,156,248,176,200,246,236,177,2036,178,250,227,201,194,191,223,197,190,193,189,184,241,243,198,239,175,159,206,207,251,438,1053,3297,493,489,140,229,204,205,199,203,192,228,209])).
% 60.51/60.52 cnf(4903,plain,
% 60.51/60.52 (P3(f21(a2,x49031),a2,x49031)),
% 60.51/60.52 inference(rename_variables,[],[4861])).
% 60.51/60.52 cnf(4905,plain,
% 60.51/60.52 (P7(a16,a2,a16,a2,a16,a18,a18,a16)),
% 60.51/60.52 inference(scs_inference,[],[4397,4861,751,259])).
% 60.51/60.52 cnf(4909,plain,
% 60.51/60.52 (P7(a2,a16,a18,a2,a2,a16,a18,a2)),
% 60.51/60.52 inference(scs_inference,[],[4397,4468,4633,4861,751,259,534,257])).
% 60.51/60.52 cnf(4911,plain,
% 60.51/60.52 (P10(a16,a15,a17,a2)),
% 60.51/60.52 inference(scs_inference,[],[4397,4468,4633,4849,4861,751,259,534,257,489])).
% 60.51/60.52 cnf(4917,plain,
% 60.51/60.52 (P8(a16,a15,x49171,x49172,a15,a16,x49171,x49172)),
% 60.51/60.52 inference(scs_inference,[],[4621,4397,4468,4633,4849,4861,4845,751,259,534,257,489,493,587,225])).
% 60.51/60.52 cnf(4925,plain,
% 60.51/60.52 (P5(a16,a15,f22(a16,a16,a18,a18),a16)),
% 60.51/60.53 inference(scs_inference,[],[4621,4397,4468,4633,4849,4692,4513,4895,4861,4845,751,259,534,257,489,493,587,225,168,681,824,170])).
% 60.51/60.53 cnf(4929,plain,
% 60.51/60.53 (P5(a2,a2,a2,a18)),
% 60.51/60.53 inference(scs_inference,[],[4621,4397,4468,4633,4786,4754,4849,4692,4513,4895,4861,4845,751,259,534,257,489,493,587,225,168,681,824,170,252,171])).
% 60.51/60.53 cnf(4939,plain,
% 60.51/60.53 (P8(a2,a2,a2,f3(a2,a2,a2),a2,f3(a2,a2,a2),a2,f3(a2,a2,a2))),
% 60.51/60.53 inference(scs_inference,[],[4621,4397,4468,4633,4742,4786,4754,4849,4692,4513,4895,4861,4903,4845,4577,751,259,534,257,489,493,587,225,168,681,824,170,252,171,224,2686,153,632,226])).
% 60.51/60.53 cnf(4943,plain,
% 60.51/60.53 (P8(a2,a17,a2,a17,x49431,x49432,x49431,x49432)),
% 60.51/60.53 inference(scs_inference,[],[4621,4397,4468,4633,4742,4746,4786,4754,4849,4692,4513,4895,4861,4903,4845,4577,751,259,534,257,489,493,587,225,168,681,824,170,252,171,224,2686,153,632,226,233,255])).
% 60.51/60.53 cnf(4945,plain,
% 60.51/60.53 (P7(a2,a16,a18,a16,a16,a2,a16,a18)),
% 60.51/60.53 inference(scs_inference,[],[4403,4621,4397,4468,4633,4742,4746,4786,4754,4849,4692,4513,4895,4861,4903,4845,4577,751,259,534,257,489,493,587,225,168,681,824,170,252,171,224,2686,153,632,226,233,255,258])).
% 60.51/60.53 cnf(4955,plain,
% 60.51/60.53 (P7(a18,a16,a16,a2,a18,a16,a2,a16)),
% 60.51/60.53 inference(scs_inference,[],[4403,4621,4397,4468,4633,4742,4746,4786,4569,4754,4849,4692,4513,4895,4861,4903,4845,4577,751,259,534,257,489,493,587,225,168,681,824,170,252,171,224,2686,153,632,226,233,255,258,612,662,569,652,256])).
% 60.51/60.53 cnf(4959,plain,
% 60.51/60.53 (P5(f22(a16,a16,a18,a18),a16,a15,a16)),
% 60.51/60.53 inference(scs_inference,[],[4403,4621,4397,4468,4633,4742,4746,4786,4569,4754,4849,4692,4513,4895,4861,4903,4845,4577,751,259,534,257,489,493,587,225,168,681,824,170,252,171,224,2686,153,632,226,233,255,258,612,662,569,652,256,592,169])).
% 60.51/60.53 cnf(4961,plain,
% 60.51/60.53 (P8(x49611,x49612,x49612,x49611,a17,a2,a16,a15)),
% 60.51/60.53 inference(scs_inference,[],[4403,4621,4397,4468,4633,4742,4746,4752,4786,4569,4754,4849,4692,4513,4895,4861,4903,4845,4577,751,259,534,257,489,493,587,225,168,681,824,170,252,171,224,2686,153,632,226,233,255,258,612,662,569,652,256,592,169,254])).
% 60.51/60.53 cnf(4965,plain,
% 60.51/60.53 (P1(a15,a16,a15)),
% 60.51/60.53 inference(scs_inference,[],[4403,4621,4397,4468,4633,4742,4746,4752,4786,4569,4611,4754,4849,4692,4513,4895,4861,4903,4845,4577,4459,751,259,534,257,489,493,587,225,168,681,824,170,252,171,224,2686,153,632,226,233,255,258,612,662,569,652,256,592,169,254,160,151])).
% 60.51/60.53 cnf(4967,plain,
% 60.51/60.53 (P1(a2,a16,a18)),
% 60.51/60.53 inference(scs_inference,[],[4403,4621,4397,4468,4633,4742,4746,4752,4786,4569,4611,4754,4790,4849,4692,4513,4895,4861,4903,4845,4577,4459,751,259,534,257,489,493,587,225,168,681,824,170,252,171,224,2686,153,632,226,233,255,258,612,662,569,652,256,592,169,254,160,151,152])).
% 60.51/60.53 cnf(4971,plain,
% 60.51/60.53 (P9(a16,a2,a2,a16)),
% 60.51/60.53 inference(scs_inference,[],[4403,4621,4397,4468,4633,4742,4746,4752,4786,4569,4611,4754,4784,4790,4849,4567,4692,4513,4895,4861,4903,4845,4577,4459,751,259,534,257,489,493,587,225,168,681,824,170,252,171,224,2686,153,632,226,233,255,258,612,662,569,652,256,592,169,254,160,151,152,164,163])).
% 60.51/60.53 cnf(4973,plain,
% 60.51/60.53 (P8(x49731,x49732,a2,a17,x49731,x49732,a2,a17)),
% 60.51/60.53 inference(scs_inference,[],[4403,4621,4397,4468,4633,4742,4746,4752,4786,4569,4611,4754,4784,4790,4849,4567,4692,4513,4895,4861,4903,4845,4577,4459,751,259,534,257,489,493,587,225,168,681,824,170,252,171,224,2686,153,632,226,233,255,258,612,662,569,652,256,592,169,254,160,151,152,164,163,253])).
% 60.51/60.53 cnf(4975,plain,
% 60.51/60.53 (P3(f21(a2,x49751),x49751,a2)),
% 60.51/60.53 inference(scs_inference,[],[4403,4621,4397,4468,4633,4742,4746,4752,4786,4569,4611,4754,4784,4790,4849,4567,4692,4513,4895,4861,4903,4845,4577,4459,751,259,534,257,489,493,587,225,168,681,824,170,252,171,224,2686,153,632,226,233,255,258,612,662,569,652,256,592,169,254,160,151,152,164,163,253,154])).
% 60.51/60.53 cnf(4977,plain,
% 60.51/60.53 (P10(a15,a16,a16,a15)),
% 60.51/60.53 inference(scs_inference,[],[4403,4621,4397,4876,4468,4633,4742,4746,4752,4786,4569,4611,4754,4784,4790,4849,4567,4692,4513,4895,4861,4903,4845,4577,4459,751,259,534,257,489,493,587,225,168,681,824,170,252,171,224,2686,153,632,226,233,255,258,612,662,569,652,256,592,169,254,160,151,152,164,163,253,154,165])).
% 60.51/60.53 cnf(4979,plain,
% 60.51/60.53 (P10(a2,a17,a15,a16)),
% 60.51/60.53 inference(scs_inference,[],[4403,4621,4397,4821,4876,4468,4633,4742,4746,4752,4786,4569,4611,4754,4784,4790,4849,4567,4692,4513,4895,4861,4903,4845,4577,4459,751,259,534,257,489,493,587,225,168,681,824,170,252,171,224,2686,153,632,226,233,255,258,612,662,569,652,256,592,169,254,160,151,152,164,163,253,154,165,166])).
% 60.51/60.53 cnf(4981,plain,
% 60.51/60.53 (P4(a16,a16,a2,a2)),
% 60.51/60.53 inference(scs_inference,[],[4403,4621,4397,4821,4876,4468,4633,4742,4746,4752,4786,4569,4611,4754,4784,4790,4849,4867,4567,4692,4513,4895,4861,4903,4845,4577,4459,751,259,534,257,489,493,587,225,168,681,824,170,252,171,224,2686,153,632,226,233,255,258,612,662,569,652,256,592,169,254,160,151,152,164,163,253,154,165,166,167])).
% 60.51/60.53 cnf(4983,plain,
% 60.51/60.53 (P4(a2,a17,a2,a17)),
% 60.51/60.53 inference(scs_inference,[],[4403,4621,4397,4821,4876,4468,4633,4742,4746,4752,4786,4569,4611,4754,4784,4790,4849,4859,4867,4567,4692,4513,4895,4861,4903,4845,4577,4459,751,259,534,257,489,493,587,225,168,681,824,170,252,171,224,2686,153,632,226,233,255,258,612,662,569,652,256,592,169,254,160,151,152,164,163,253,154,165,166,167,156])).
% 60.51/60.53 cnf(4986,plain,
% 60.51/60.53 (P8(x49861,x49862,x49861,x49862,a2,a2,a2,a2)),
% 60.51/60.53 inference(rename_variables,[],[4764])).
% 60.51/60.53 cnf(4989,plain,
% 60.51/60.53 (P8(a17,a2,x49891,x49892,a2,a17,x49891,x49892)),
% 60.51/60.53 inference(rename_variables,[],[4579])).
% 60.51/60.53 cnf(4999,plain,
% 60.51/60.53 (P5(a2,a2,a17,a2)),
% 60.51/60.53 inference(scs_inference,[],[4736,4403,4621,4397,4821,4876,4468,4633,4742,4746,4752,4764,4986,4786,4569,4611,4754,4784,4788,4790,4849,4859,4867,4567,4692,4513,4895,4861,4903,4845,4577,4835,4459,4579,4989,4275,751,259,534,257,489,493,587,225,168,681,824,170,252,171,224,2686,153,632,226,233,255,258,612,662,569,652,256,592,169,254,160,151,152,164,163,253,154,165,166,167,156,242,249,245,2036,177,236])).
% 60.51/60.53 cnf(5000,plain,
% 60.51/60.53 (P8(x50001,x50002,x50001,x50002,a2,a2,a2,a2)),
% 60.51/60.53 inference(rename_variables,[],[4764])).
% 60.51/60.53 cnf(5008,plain,
% 60.51/60.53 (P9(a16,a16,a16,a16)),
% 60.51/60.53 inference(scs_inference,[],[4736,4403,4621,4397,4821,4876,4468,4633,4742,4746,4752,4764,4986,4786,4569,4611,4744,4754,4784,4788,4790,4849,4856,4859,4867,4567,4383,4692,4513,4895,4861,4903,4845,4577,4835,4459,4579,4989,4425,4275,751,259,534,257,489,493,587,225,168,681,824,170,252,171,224,2686,153,632,226,233,255,258,612,662,569,652,256,592,169,254,160,151,152,164,163,253,154,165,166,167,156,242,249,245,2036,177,236,178,227,223,240])).
% 60.51/60.53 cnf(5022,plain,
% 60.51/60.53 (P2(f8(a2,a2,a17),a2,a2,a17)),
% 60.51/60.53 inference(scs_inference,[],[4736,4403,4621,4397,4821,4876,4468,4633,4742,4746,4752,4764,4986,4786,4569,4611,4744,4754,4784,4788,4790,4849,4856,4859,4867,4567,4383,4692,4513,4895,4861,4903,4845,4577,4835,4453,4459,4579,4989,4425,4295,4297,4275,751,259,534,257,489,493,587,225,168,681,824,170,252,171,224,2686,153,632,226,233,255,258,612,662,569,652,256,592,169,254,160,151,152,164,163,253,154,165,166,167,156,242,249,245,2036,177,236,178,227,223,240,193,190,199,184,194,197,191])).
% 60.51/60.53 cnf(5026,plain,
% 60.51/60.53 (P3(f25(a17,a17,a17,a17,a2,a2),a17,a17)),
% 60.51/60.53 inference(scs_inference,[],[4736,4403,4621,4397,4821,4876,4468,4633,4742,4746,4752,4764,4986,4786,4569,4611,4744,4754,4784,4788,4790,4849,4856,4859,4867,4567,4383,4692,4513,4895,4861,4903,4845,4577,4835,4453,4459,4579,4989,4425,4295,4297,4275,751,259,534,257,489,493,587,225,168,681,824,170,252,171,224,2686,153,632,226,233,255,258,612,662,569,652,256,592,169,254,160,151,152,164,163,253,154,165,166,167,156,242,249,245,2036,177,236,178,227,223,240,193,190,199,184,194,197,191,189,203])).
% 60.51/60.53 cnf(5029,plain,
% 60.51/60.53 (P3(f21(a2,x50291),a2,x50291)),
% 60.51/60.53 inference(rename_variables,[],[4861])).
% 60.51/60.53 cnf(5030,plain,
% 60.51/60.53 (P10(x50301,x50302,x50301,x50302)),
% 60.51/60.53 inference(scs_inference,[],[4736,4403,4621,4397,4821,4876,4468,4633,4742,4746,4752,4764,4986,5000,4786,4569,4611,4744,4754,4784,4788,4790,4849,4856,4859,4867,4567,4383,4692,4513,4895,4861,4903,4845,4577,4835,4453,4459,4579,4989,4425,4295,4297,4275,4678,333,751,259,534,257,489,493,587,225,168,681,824,170,252,171,224,2686,153,632,226,233,255,258,612,662,569,652,256,592,169,254,160,151,152,164,163,253,154,165,166,167,156,242,249,245,2036,177,236,178,227,223,240,193,190,199,184,194,197,191,189,203,107,241])).
% 60.51/60.53 cnf(5042,plain,
% 60.51/60.53 (P10(a17,a2,a2,a2)),
% 60.51/60.53 inference(scs_inference,[],[142,4736,4403,4621,4397,4821,4876,4468,4633,4742,4746,4752,4764,4986,5000,4786,4569,4611,4744,4754,4784,4788,4790,4849,4856,4859,4867,4567,4383,4692,4513,4895,4809,4861,4903,4845,4577,4835,4453,4459,4579,4989,4425,4295,4297,4275,346,4505,4678,333,751,259,534,257,489,493,587,225,168,681,824,170,252,171,224,2686,153,632,226,233,255,258,612,662,569,652,256,592,169,254,160,151,152,164,163,253,154,165,166,167,156,242,249,245,2036,177,236,178,227,223,240,193,190,199,184,194,197,191,189,203,107,241,173,172,181,243,198,195])).
% 60.51/60.53 cnf(5044,plain,
% 60.51/60.53 (P3(a2,a2,f3(a2,a2,a2))),
% 60.51/60.53 inference(scs_inference,[],[142,4736,4403,4621,4397,4821,4876,4468,4633,4742,4746,4752,4764,4986,5000,4786,4569,4611,4744,4754,4784,4788,4790,4849,4856,4859,4867,4567,4383,4692,4513,4895,4809,4861,4903,4845,4577,4835,4453,4459,4579,4989,4425,4295,4297,4275,346,4505,4678,333,751,259,534,257,489,493,587,225,168,681,824,170,252,171,224,2686,153,632,226,233,255,258,612,662,569,652,256,592,169,254,160,151,152,164,163,253,154,165,166,167,156,242,249,245,2036,177,236,178,227,223,240,193,190,199,184,194,197,191,189,203,107,241,173,172,181,243,198,195,162])).
% 60.51/60.53 cnf(5050,plain,
% 60.51/60.53 (P4(a16,a16,a16,a16)),
% 60.51/60.53 inference(scs_inference,[],[142,4736,4403,4621,4397,4821,4876,4468,4633,4742,4746,4752,4764,4986,5000,4786,4569,4611,4744,4754,4784,4788,4790,4849,4856,4859,4867,4567,4383,4692,4513,4895,4809,4861,4903,4845,4577,4835,4453,4459,4579,4989,4425,4295,4297,4275,346,4347,4505,4678,333,751,259,534,257,489,493,587,225,168,681,824,170,252,171,224,2686,153,632,226,233,255,258,612,662,569,652,256,592,169,254,160,151,152,164,163,253,154,165,166,167,156,242,249,245,2036,177,236,178,227,223,240,193,190,199,184,194,197,191,189,203,107,241,173,172,181,243,198,195,162,207,206,251])).
% 60.51/60.53 cnf(5056,plain,
% 60.51/60.53 (P10(a2,a17,a2,a2)),
% 60.51/60.53 inference(scs_inference,[],[142,4736,4403,4621,4397,4821,4876,4468,4633,4742,4746,4752,4764,4986,5000,4786,4569,4611,4744,4754,4784,4788,4790,4849,4856,4859,4867,4567,4383,4692,4513,4895,4809,4861,4903,5029,4845,4577,4835,4453,4459,4579,4989,4425,4295,4297,4275,346,4347,4505,4678,333,751,259,534,257,489,493,587,225,168,681,824,170,252,171,224,2686,153,632,226,233,255,258,612,662,569,652,256,592,169,254,160,151,152,164,163,253,154,165,166,167,156,242,249,245,2036,177,236,178,227,223,240,193,190,199,184,194,197,191,189,203,107,241,173,172,181,243,198,195,162,207,206,251,2,4731,2002])).
% 60.51/60.53 cnf(5058,plain,
% 60.51/60.53 (P10(a16,a15,a2,a2)),
% 60.51/60.53 inference(scs_inference,[],[142,4736,4403,4621,4397,4821,4876,4468,4633,4742,4746,4752,4764,4986,5000,4786,4569,4611,4744,4754,4784,4788,4790,4849,4856,4859,4867,4567,4383,4692,4513,4895,4809,4861,4903,5029,4845,4577,4835,4453,4459,4579,4989,4425,4295,4297,4275,346,4347,4505,4678,333,751,259,534,257,489,493,587,225,168,681,824,170,252,171,224,2686,153,632,226,233,255,258,612,662,569,652,256,592,169,254,160,151,152,164,163,253,154,165,166,167,156,242,249,245,2036,177,236,178,227,223,240,193,190,199,184,194,197,191,189,203,107,241,173,172,181,243,198,195,162,207,206,251,2,4731,2002,2011])).
% 60.51/60.53 cnf(5062,plain,
% 60.51/60.53 (P9(a16,a2,a15,a17)),
% 60.51/60.53 inference(scs_inference,[],[142,4736,4403,4621,4397,4821,4876,4468,4633,4742,4746,4752,4764,4986,5000,4786,4569,4611,4744,4754,4784,4788,4790,4849,4856,4859,4867,4567,4383,4692,4513,4895,4809,4861,4903,5029,4845,4577,4835,4453,4459,4579,4989,4425,4295,4297,4275,346,4347,4505,4678,333,751,259,534,257,489,493,587,225,168,681,824,170,252,171,224,2686,153,632,226,233,255,258,612,662,569,652,256,592,169,254,160,151,152,164,163,253,154,165,166,167,156,242,249,245,2036,177,236,178,227,223,240,193,190,199,184,194,197,191,189,203,107,241,173,172,181,243,198,195,162,207,206,251,2,4731,2002,2011,724,497])).
% 60.51/60.53 cnf(5085,plain,
% 60.51/60.53 (P10(a2,a16,a15,a17)),
% 60.51/60.53 inference(scs_inference,[],[5030,527])).
% 60.51/60.53 cnf(5086,plain,
% 60.51/60.53 (P10(x50861,x50862,x50861,x50862)),
% 60.51/60.53 inference(rename_variables,[],[5030])).
% 60.51/60.53 cnf(5089,plain,
% 60.51/60.53 (P10(x50891,x50892,x50891,x50892)),
% 60.51/60.53 inference(rename_variables,[],[5030])).
% 60.51/60.53 cnf(5091,plain,
% 60.51/60.53 (P10(a19,a19,a17,a17)),
% 60.51/60.53 inference(scs_inference,[],[5030,5086,5089,527,529,679])).
% 60.51/60.53 cnf(5092,plain,
% 60.51/60.53 (P10(x50921,x50922,x50921,x50922)),
% 60.51/60.53 inference(rename_variables,[],[5030])).
% 60.51/60.53 cnf(5095,plain,
% 60.51/60.53 (P10(x50951,x50952,x50951,x50952)),
% 60.51/60.53 inference(rename_variables,[],[5030])).
% 60.51/60.53 cnf(5097,plain,
% 60.51/60.53 (P10(a17,a15,a2,a16)),
% 60.51/60.53 inference(scs_inference,[],[5030,5086,5089,5092,5095,527,529,679,696,2173])).
% 60.51/60.53 cnf(5098,plain,
% 60.51/60.53 (P10(x50981,x50982,x50981,x50982)),
% 60.51/60.53 inference(rename_variables,[],[5030])).
% 60.51/60.53 cnf(5101,plain,
% 60.51/60.53 (P3(f21(a2,x51011),x51011,a2)),
% 60.51/60.53 inference(rename_variables,[],[4975])).
% 60.51/60.53 cnf(5107,plain,
% 60.51/60.53 (P8(a16,a2,x51071,x51072,a2,a16,x51071,x51072)),
% 60.51/60.53 inference(scs_inference,[],[5030,5086,5089,5092,5095,4585,4587,4971,4975,527,529,679,696,2173,3313,259,534,225])).
% 60.51/60.53 cnf(5109,plain,
% 60.51/60.53 (P5(a2,a2,a2,a17)),
% 60.51/60.53 inference(scs_inference,[],[5030,5086,5089,5092,5095,4585,4587,4971,4999,4975,527,529,679,696,2173,3313,259,534,225,171])).
% 60.51/60.53 cnf(5125,plain,
% 60.51/60.53 (P4(a2,a17,a17,a2)),
% 60.51/60.53 inference(scs_inference,[],[5030,5086,5089,5092,5095,4585,4607,4587,4591,4971,4983,4999,5042,4889,4975,4865,527,529,679,696,2173,3313,259,534,225,171,681,170,587,153,257,224,824,168])).
% 60.51/60.53 cnf(5131,plain,
% 60.51/60.53 (P8(x51311,x51312,a2,a17,x51311,x51312,a17,a2)),
% 60.51/60.53 inference(scs_inference,[],[5030,5086,5089,5092,5095,4585,4607,4794,4587,4591,4971,4983,4999,5042,4889,4975,4865,4959,527,529,679,696,2173,3313,259,534,225,171,681,170,587,153,257,224,824,168,226,2686,252])).
% 60.51/60.53 cnf(5133,plain,
% 60.51/60.53 (P9(x51331,x51332,x51331,x51332)),
% 60.51/60.53 inference(scs_inference,[],[5030,5086,5089,5092,5095,4585,4607,4794,4973,4587,4591,4971,4983,4999,5042,4889,4975,4865,4959,527,529,679,696,2173,3313,259,534,225,171,681,170,587,153,257,224,824,168,226,2686,252,233])).
% 60.51/60.53 cnf(5139,plain,
% 60.51/60.53 (P8(x51391,x51392,x51391,x51392,a17,a2,a2,a17)),
% 60.51/60.53 inference(scs_inference,[],[5030,5086,5089,5092,5095,4585,4607,4794,4973,4587,4591,4971,4983,4999,5042,4889,4975,4865,4959,527,529,679,696,2173,3313,259,534,225,171,681,170,587,153,257,224,824,168,226,2686,252,233,612,632,255])).
% 60.51/60.53 cnf(5147,plain,
% 60.51/60.53 (P1(a16,a16,a16)),
% 60.51/60.53 inference(scs_inference,[],[5030,5086,5089,5092,5095,4401,4585,4607,4794,4973,4587,4591,4971,4983,4999,5008,5042,4889,4975,4865,4959,527,529,679,696,2173,3313,259,534,225,171,681,170,587,153,257,224,824,168,226,2686,252,233,612,632,255,662,258,592,160])).
% 60.51/60.53 cnf(5153,plain,
% 60.51/60.53 (P8(x51531,x51532,a17,a2,x51532,x51531,a2,a17)),
% 60.51/60.53 inference(scs_inference,[],[5030,5086,5089,5092,5095,4401,4585,4607,4794,4973,4587,4591,4971,4983,4999,5008,5042,4889,4975,4865,4816,4959,527,529,679,696,2173,3313,259,534,225,171,681,170,587,153,257,224,824,168,226,2686,252,233,612,632,255,662,258,592,160,169,652,254])).
% 60.51/60.53 cnf(5155,plain,
% 60.51/60.53 (P1(a15,a15,a16)),
% 60.51/60.53 inference(scs_inference,[],[5030,5086,5089,5092,5095,4401,4585,4607,4794,4973,4587,4591,4965,4971,4983,4999,5008,5042,4889,4975,4865,4816,4959,527,529,679,696,2173,3313,259,534,225,171,681,170,587,153,257,224,824,168,226,2686,252,233,612,632,255,662,258,592,160,169,652,254,152])).
% 60.51/60.53 cnf(5161,plain,
% 60.51/60.53 (P7(a18,a2,a18,a2,a16,a18,a16,a18)),
% 60.51/60.53 inference(scs_inference,[],[5030,5086,5089,5092,5095,4401,4585,4607,4794,4973,4587,4591,4732,4965,4971,4983,4999,5008,5042,4806,4889,4975,4865,4816,4959,527,529,679,696,2173,3313,259,534,225,171,681,170,587,153,257,224,824,168,226,2686,252,233,612,632,255,662,258,592,160,169,652,254,152,151,569,256])).
% 60.51/60.53 cnf(5163,plain,
% 60.51/60.53 (P9(a15,a17,a16,a2)),
% 60.51/60.53 inference(scs_inference,[],[5030,5086,5089,5092,5095,4401,4585,4607,4794,4973,4587,4591,4732,4965,4971,4983,4999,5008,5042,5062,4806,4889,4975,4865,4816,4959,527,529,679,696,2173,3313,259,534,225,171,681,170,587,153,257,224,824,168,226,2686,252,233,612,632,255,662,258,592,160,169,652,254,152,151,569,256,163])).
% 60.51/60.53 cnf(5165,plain,
% 60.51/60.53 (P9(a16,a2,a17,a15)),
% 60.51/60.53 inference(scs_inference,[],[5030,5086,5089,5092,5095,4401,4585,4607,4794,4973,4587,4591,4732,4965,4971,4983,4999,5008,5042,5062,4806,4889,4975,4865,4816,4959,527,529,679,696,2173,3313,259,534,225,171,681,170,587,153,257,224,824,168,226,2686,252,233,612,632,255,662,258,592,160,169,652,254,152,151,569,256,163,164])).
% 60.51/60.53 cnf(5167,plain,
% 60.51/60.53 (P8(x51671,x51672,a16,a15,x51671,x51672,a15,a16)),
% 60.51/60.53 inference(scs_inference,[],[5030,5086,5089,5092,5095,4401,4585,4607,4794,4917,4973,4587,4591,4732,4965,4971,4983,4999,5008,5042,5062,4806,4889,4975,4865,4816,4959,527,529,679,696,2173,3313,259,534,225,171,681,170,587,153,257,224,824,168,226,2686,252,233,612,632,255,662,258,592,160,169,652,254,152,151,569,256,163,164,253])).
% 60.51/60.53 cnf(5171,plain,
% 60.51/60.53 (P10(a15,a16,a2,a17)),
% 60.51/60.53 inference(scs_inference,[],[5030,5086,5089,5092,5095,4401,4585,4607,4979,4794,4917,4973,4587,4591,4732,4965,4971,4983,4999,5008,5042,5062,4806,4889,4975,5044,4865,4816,4959,527,529,679,696,2173,3313,259,534,225,171,681,170,587,153,257,224,824,168,226,2686,252,233,612,632,255,662,258,592,160,169,652,254,152,151,569,256,163,164,253,154,165])).
% 60.51/60.53 cnf(5175,plain,
% 60.51/60.53 (P10(x51751,x51752,x51752,x51751)),
% 60.51/60.53 inference(scs_inference,[],[5030,5086,5089,5092,5095,5098,4401,4585,4607,4979,4794,4917,4973,4587,4591,4732,4965,4971,4983,4999,5008,5042,5062,4806,4811,4889,4975,5044,4865,4816,4959,527,529,679,696,2173,3313,259,534,225,171,681,170,587,153,257,224,824,168,226,2686,252,233,612,632,255,662,258,592,160,169,652,254,152,151,569,256,163,164,253,154,165,167,166])).
% 60.51/60.53 cnf(5177,plain,
% 60.51/60.53 (P4(f25(a2,a2,a2,a2,a2,a2),a2,f25(a2,a2,a2,a2,a2,a2),a2)),
% 60.51/60.53 inference(scs_inference,[],[5030,5086,5089,5092,5095,5098,4401,4585,4607,4979,4794,4917,4973,4587,4591,4732,4965,4971,4983,4999,5008,5042,5062,4806,4811,4889,4975,5044,4865,4816,4959,527,529,679,696,2173,3313,259,534,225,171,681,170,587,153,257,224,824,168,226,2686,252,233,612,632,255,662,258,592,160,169,652,254,152,151,569,256,163,164,253,154,165,167,166,156])).
% 60.51/60.53 cnf(5187,plain,
% 60.51/60.53 (P5(a17,a17,a2,a17)),
% 60.51/60.53 inference(scs_inference,[],[5030,5086,5089,5092,5095,5098,4401,4613,4585,4607,4979,4794,4917,4943,4973,4587,4591,4732,4965,4971,4983,4999,5008,5042,5062,4806,4811,4889,4975,5044,4865,4816,4959,4289,4491,527,529,679,696,2173,3313,259,534,225,171,681,170,587,153,257,224,824,168,226,2686,252,233,612,632,255,662,258,592,160,169,652,254,152,151,569,256,163,164,253,154,165,167,166,156,188,246,176,263,236])).
% 60.51/60.53 cnf(5195,plain,
% 60.51/60.53 (P10(x51951,x51952,x51951,x51952)),
% 60.51/60.53 inference(rename_variables,[],[5030])).
% 60.51/60.53 cnf(5199,plain,
% 60.51/60.53 (P10(x51991,f5(x51991,x51991,x51992),x51992,x51991)),
% 60.51/60.53 inference(scs_inference,[],[5030,5086,5089,5092,5095,5098,5195,4401,4613,4585,4607,4979,4794,4917,4943,4973,4587,4591,4732,4965,4971,4983,4999,5008,5042,5062,4806,4811,4891,4889,4975,5044,4865,4816,4959,4289,4491,527,529,679,696,2173,3313,259,534,225,171,681,170,587,153,257,224,824,168,226,2686,252,233,612,632,255,662,258,592,160,169,652,254,152,151,569,256,163,164,253,154,165,167,166,156,188,246,176,263,236,200,250,177,227,190])).
% 60.51/60.53 cnf(5202,plain,
% 60.51/60.53 (P10(x52021,x52022,x52021,x52022)),
% 60.51/60.53 inference(rename_variables,[],[5030])).
% 60.51/60.53 cnf(5204,plain,
% 60.51/60.53 (P9(x52041,x52042,x52042,x52041)),
% 60.51/60.53 inference(scs_inference,[],[5030,5086,5089,5092,5095,5098,5195,4401,4613,4585,4607,4979,4794,4917,4943,4961,4973,4587,4591,4732,4965,4971,4983,4999,5008,5042,5062,4806,4811,4891,4889,4975,5044,4865,4816,4959,4289,4281,4491,527,529,679,696,2173,3313,259,534,225,171,681,170,587,153,257,224,824,168,226,2686,252,233,612,632,255,662,258,592,160,169,652,254,152,151,569,256,163,164,253,154,165,167,166,156,188,246,176,263,236,200,250,177,227,190,201,240])).
% 60.51/60.53 cnf(5208,plain,
% 60.51/60.53 (P2(a2,a17,a17,a17)),
% 60.51/60.53 inference(scs_inference,[],[5030,5086,5089,5092,5095,5098,5195,4401,4613,4585,4607,4979,4794,4917,4943,4961,4973,4587,4591,4732,4965,4971,4983,4999,5008,5042,5062,4806,4811,4891,4889,4975,5044,4865,4816,4959,4289,4281,4491,527,529,679,696,2173,3313,259,534,225,171,681,170,587,153,257,224,824,168,226,2686,252,233,612,632,255,662,258,592,160,169,652,254,152,151,569,256,163,164,253,154,165,167,166,156,188,246,176,263,236,200,250,177,227,190,201,240,223,184])).
% 60.51/60.53 cnf(5213,plain,
% 60.51/60.53 (P10(x52131,x52132,x52131,x52132)),
% 60.51/60.53 inference(rename_variables,[],[5030])).
% 60.51/60.53 cnf(5215,plain,
% 60.51/60.53 (P1(f5(x52151,x52151,x52152),x52152,x52151)),
% 60.51/60.53 inference(scs_inference,[],[5030,5086,5089,5092,5095,5098,5195,5202,5213,4401,4613,4585,4607,4979,4794,4917,4943,4961,4973,4587,4591,4732,4965,4971,4983,4999,5008,5042,5062,4806,4811,4891,4889,4975,5044,4865,4816,4959,4876,4289,4281,4491,527,529,679,696,2173,3313,259,534,225,171,681,170,587,153,257,224,824,168,226,2686,252,233,612,632,255,662,258,592,160,169,652,254,152,151,569,256,163,164,253,154,165,167,166,156,188,246,176,263,236,200,250,177,227,190,201,240,223,184,191,199,178])).
% 60.51/60.53 cnf(5218,plain,
% 60.51/60.53 (P10(x52181,x52182,x52181,x52182)),
% 60.51/60.53 inference(rename_variables,[],[5030])).
% 60.51/60.53 cnf(5221,plain,
% 60.51/60.53 (P10(x52211,x52212,x52211,x52212)),
% 60.51/60.53 inference(rename_variables,[],[5030])).
% 60.51/60.53 cnf(5223,plain,
% 60.51/60.53 (P10(x52231,f4(x52231,x52231,x52232),x52232,x52231)),
% 60.51/60.53 inference(scs_inference,[],[142,5030,5086,5089,5092,5095,5098,5195,5202,5213,5218,5221,4401,4613,4585,4607,4979,4794,4917,4943,4961,4973,4587,4591,4732,4965,4971,4983,4999,5008,5042,5050,5062,4806,4811,4891,4889,4975,5044,4865,4816,4959,4876,4289,4281,4491,527,529,679,696,2173,3313,259,534,225,171,681,170,587,153,257,224,824,168,226,2686,252,233,612,632,255,662,258,592,160,169,652,254,152,151,569,256,163,164,253,154,165,167,166,156,188,246,176,263,236,200,250,177,227,190,201,240,223,184,191,199,178,193,197,189])).
% 60.51/60.53 cnf(5226,plain,
% 60.51/60.53 (P10(x52261,x52262,x52261,x52262)),
% 60.51/60.53 inference(rename_variables,[],[5030])).
% 60.51/60.53 cnf(5228,plain,
% 60.51/60.53 (~P9(a1,f21(a2,a20),a20,a2)),
% 60.51/60.53 inference(scs_inference,[],[142,5030,5086,5089,5092,5095,5098,5195,5202,5213,5218,5221,5226,4401,4613,4585,4607,4979,4794,4917,4943,4961,4973,4587,4591,4732,4965,4971,4983,4999,5008,5042,5050,5062,4806,4872,4811,4891,4889,4975,5044,4865,4816,4959,4876,4289,4281,4491,527,529,679,696,2173,3313,259,534,225,171,681,170,587,153,257,224,824,168,226,2686,252,233,612,632,255,662,258,592,160,169,652,254,152,151,569,256,163,164,253,154,165,167,166,156,188,246,176,263,236,200,250,177,227,190,201,240,223,184,191,199,178,193,197,189,194,182])).
% 60.51/60.53 cnf(5229,plain,
% 60.51/60.53 (P10(x52291,x52292,x52291,x52292)),
% 60.51/60.53 inference(rename_variables,[],[5030])).
% 60.51/60.53 cnf(5233,plain,
% 60.51/60.53 (P4(f3(a2,a2,a2),f3(a2,a2,a2),f3(a2,a2,a2),a2)),
% 60.51/60.53 inference(scs_inference,[],[142,5030,5086,5089,5092,5095,5098,5195,5202,5213,5218,5221,5226,5229,4495,4401,4613,4585,4607,4979,4794,4917,4943,4961,4973,4587,4591,4732,4965,4971,4983,4999,5008,5042,5050,5062,4806,4872,4811,4891,4889,4975,5044,4865,4816,4959,4876,4289,4281,4491,527,529,679,696,2173,3313,259,534,225,171,681,170,587,153,257,224,824,168,226,2686,252,233,612,632,255,662,258,592,160,169,652,254,152,151,569,256,163,164,253,154,165,167,166,156,188,246,176,263,236,200,250,177,227,190,201,240,223,184,191,199,178,193,197,189,194,182,241,173])).
% 60.51/60.53 cnf(5234,plain,
% 60.51/60.53 (P10(x52341,x52342,x52341,x52342)),
% 60.51/60.53 inference(rename_variables,[],[5030])).
% 60.51/60.53 cnf(5236,plain,
% 60.51/60.53 (P10(a2,a2,a17,a17)),
% 60.51/60.53 inference(scs_inference,[],[142,5030,5086,5089,5092,5095,5098,5195,5202,5213,5218,5221,5226,5229,4495,4401,4613,4585,4607,4979,4794,4917,4943,4961,4973,4587,4591,4732,4965,4971,4983,4999,5008,5042,5050,5062,4806,4872,4811,4891,4889,4975,5044,4865,4816,4959,4876,4289,4281,4491,527,529,679,696,2173,3313,259,534,225,171,681,170,587,153,257,224,824,168,226,2686,252,233,612,632,255,662,258,592,160,169,652,254,152,151,569,256,163,164,253,154,165,167,166,156,188,246,176,263,236,200,250,177,227,190,201,240,223,184,191,199,178,193,197,189,194,182,241,173,181])).
% 60.51/60.53 cnf(5238,plain,
% 60.51/60.53 (P4(a16,a2,a2,a16)),
% 60.51/60.53 inference(scs_inference,[],[142,5030,5086,5089,5092,5095,5098,5195,5202,5213,5218,5221,5226,5229,4495,4401,4613,4585,4607,4979,4794,4917,4943,4961,4973,4587,4591,4732,4965,4971,4983,4999,5008,5042,5050,5062,4806,4872,4811,4891,4889,4975,5044,4865,4816,4959,4876,4289,4299,4281,4491,527,529,679,696,2173,3313,259,534,225,171,681,170,587,153,257,224,824,168,226,2686,252,233,612,632,255,662,258,592,160,169,652,254,152,151,569,256,163,164,253,154,165,167,166,156,188,246,176,263,236,200,250,177,227,190,201,240,223,184,191,199,178,193,197,189,194,182,241,173,181,243])).
% 60.51/60.53 cnf(5242,plain,
% 60.51/60.53 (P3(f6(a2,a2,a2),a2,a2)),
% 60.51/60.53 inference(scs_inference,[],[142,5030,5086,5089,5092,5095,5098,5195,5202,5213,5218,5221,5226,5229,5234,4495,4401,4613,4585,4607,4977,4979,4794,4917,4943,4961,4973,4587,4591,4732,4780,4965,4971,4983,4999,5008,5042,5050,5062,4806,4872,4811,4891,4889,4975,5044,4865,4816,4959,4876,4289,4299,4281,4491,527,529,679,696,2173,3313,259,534,225,171,681,170,587,153,257,224,824,168,226,2686,252,233,612,632,255,662,258,592,160,169,652,254,152,151,569,256,163,164,253,154,165,167,166,156,188,246,176,263,236,200,250,177,227,190,201,240,223,184,191,199,178,193,197,189,194,182,241,173,181,243,198,186])).
% 60.51/60.53 cnf(5246,plain,
% 60.51/60.53 (P3(f21(a17,x52461),a17,x52461)),
% 60.51/60.53 inference(scs_inference,[],[142,5030,5086,5089,5092,5095,5098,5195,5202,5213,5218,5221,5226,5229,5234,4495,4401,4613,4585,4607,4977,4979,4794,4917,4943,4961,4973,4587,4591,4732,4780,4965,4971,4983,4999,5008,5042,5050,5062,4806,4872,4811,4891,4889,4975,5101,5044,5026,4865,4816,4959,4483,4876,4289,4299,4281,4491,527,529,679,696,2173,3313,259,534,225,171,681,170,587,153,257,224,824,168,226,2686,252,233,612,632,255,662,258,592,160,169,652,254,152,151,569,256,163,164,253,154,165,167,166,156,188,246,176,263,236,200,250,177,227,190,201,240,223,184,191,199,178,193,197,189,194,182,241,173,181,243,198,186,159])).
% 60.51/60.53 cnf(5247,plain,
% 60.51/60.53 (P3(f21(a2,x52471),x52471,a2)),
% 60.51/60.53 inference(rename_variables,[],[4975])).
% 60.51/60.53 cnf(5253,plain,
% 60.51/60.53 (P4(a2,a2,a18,a18)),
% 60.51/60.53 inference(scs_inference,[],[142,5030,5086,5089,5092,5095,5098,5195,5202,5213,5218,5221,5226,5229,5234,4495,4401,4613,4585,4607,4929,4977,4979,4794,4917,4943,4961,4973,4587,4591,4732,4780,4965,4971,4983,4999,5008,5042,5050,5062,4806,4872,4811,4891,4889,4975,5101,5044,5026,4865,4816,4959,4483,4615,4876,4289,4299,4571,4281,4491,527,529,679,696,2173,3313,259,534,225,171,681,170,587,153,257,224,824,168,226,2686,252,233,612,632,255,662,258,592,160,169,652,254,152,151,569,256,163,164,253,154,165,167,166,156,188,246,176,263,236,200,250,177,227,190,201,240,223,184,191,199,178,193,197,189,194,182,241,173,181,243,198,186,159,207,206,251])).
% 60.51/60.53 cnf(5268,plain,
% 60.51/60.53 (~P3(a1,x52681,x52681)),
% 60.51/60.53 inference(scs_inference,[],[142,5030,5086,5089,5092,5095,5098,5195,5202,5213,5218,5221,5226,5229,5234,4495,4401,4613,4585,4607,4929,4977,4979,4794,4917,4943,4961,4973,4587,4591,4732,4780,4965,4971,4983,4999,5008,5042,5050,5062,4806,4872,4874,4811,4891,4889,4975,5101,5247,5044,5026,4865,4816,4959,4483,4615,4876,4289,4299,4571,4281,4491,527,529,679,696,2173,3313,259,534,225,171,681,170,587,153,257,224,824,168,226,2686,252,233,612,632,255,662,258,592,160,169,652,254,152,151,569,256,163,164,253,154,165,167,166,156,188,246,176,263,236,200,250,177,227,190,201,240,223,184,191,199,178,193,197,189,194,182,241,173,181,243,198,186,159,207,206,251,648,589,187,124,238,158,175])).
% 60.51/60.53 cnf(5280,plain,
% 60.51/60.53 (P1(f5(x52801,x52801,x52802),x52802,x52801)),
% 60.51/60.53 inference(rename_variables,[],[5215])).
% 60.51/60.53 cnf(5283,plain,
% 60.51/60.53 (P1(f5(x52831,x52831,x52832),x52832,x52831)),
% 60.51/60.53 inference(rename_variables,[],[5215])).
% 60.51/60.53 cnf(5286,plain,
% 60.51/60.53 (P10(x52861,f5(x52861,x52861,x52862),x52862,x52861)),
% 60.51/60.53 inference(rename_variables,[],[5199])).
% 60.51/60.53 cnf(5288,plain,
% 60.51/60.53 (P10(a16,a15,a17,f5(a17,a17,a2))),
% 60.51/60.53 inference(scs_inference,[],[5199,5286,5215,5280,828,836,531,491])).
% 60.51/60.53 cnf(5292,plain,
% 60.51/60.53 (P1(f5(x52921,x52921,x52922),x52922,x52921)),
% 60.51/60.53 inference(rename_variables,[],[5215])).
% 60.51/60.53 cnf(5295,plain,
% 60.51/60.53 (P10(x52951,x52952,x52952,x52951)),
% 60.51/60.53 inference(rename_variables,[],[5175])).
% 60.51/60.53 cnf(5304,plain,
% 60.51/60.53 (P1(f5(x53041,x53041,x53042),x53042,x53041)),
% 60.51/60.53 inference(rename_variables,[],[5215])).
% 60.51/60.53 cnf(5306,plain,
% 60.51/60.53 (P8(x53061,x53062,x53063,x53064,x53061,x53062,x53063,x53064)),
% 60.51/60.53 inference(scs_inference,[],[5133,5175,4852,4955,5199,5286,5215,5280,5283,5292,5246,828,836,531,491,832,2173,534,259,153,824,225])).
% 60.51/60.53 cnf(5310,plain,
% 60.51/60.53 (P5(a17,a17,a17,a2)),
% 60.51/60.53 inference(scs_inference,[],[5133,5175,4852,4955,5187,5199,5286,5215,5280,5283,5292,5246,828,836,531,491,832,2173,534,259,153,824,225,170,171])).
% 60.51/60.53 cnf(5320,plain,
% 60.51/60.53 (P10(a18,a18,a16,a15)),
% 60.51/60.53 inference(scs_inference,[],[5133,5175,5058,4852,4955,4762,5187,5199,5286,5215,5280,5283,5292,5233,5246,4925,828,836,531,491,832,2173,534,259,153,824,225,170,171,257,226,681,224,587])).
% 60.51/60.53 cnf(5326,plain,
% 60.51/60.53 (P4(f3(a2,a2,a2),f3(a2,a2,a2),a2,f3(a2,a2,a2))),
% 60.51/60.53 inference(scs_inference,[],[5133,5175,5058,4852,4955,4762,5109,5187,5199,5286,5215,5280,5283,5292,5233,5246,4925,828,836,531,491,832,2173,534,259,153,824,225,170,171,257,226,681,224,587,2686,612,168])).
% 60.51/60.53 cnf(5330,plain,
% 60.51/60.53 (P8(a2,a16,x53301,x53302,a16,a2,x53301,x53302)),
% 60.51/60.53 inference(scs_inference,[],[5133,5175,5058,4852,4955,5107,4762,5109,5187,5199,5286,5215,5280,5283,5292,5233,5246,4925,828,836,531,491,832,2173,534,259,153,824,225,170,171,257,226,681,224,587,2686,612,168,662,252])).
% 60.51/60.53 cnf(5338,plain,
% 60.51/60.53 (P1(x53381,x53382,x53382)),
% 60.51/60.53 inference(scs_inference,[],[5133,5175,5058,4852,4955,5107,4762,5109,5187,5199,5286,5215,5280,5283,5292,5233,5246,4925,828,836,531,491,832,2173,534,259,153,824,225,170,171,257,226,681,224,587,2686,612,168,662,252,652,592,632,160])).
% 60.51/60.53 cnf(5340,plain,
% 60.51/60.53 (P9(f3(a2,a2,a2),f3(a2,a2,a2),f3(a2,a2,a2),a2)),
% 60.51/60.53 inference(scs_inference,[],[5133,5175,5058,4852,4955,5107,4762,5109,5187,5199,5286,5215,5280,5283,5292,5233,5246,4925,828,836,531,491,832,2173,534,259,153,824,225,170,171,257,226,681,224,587,2686,612,168,662,252,652,592,632,160,233])).
% 60.51/60.53 cnf(5342,plain,
% 60.51/60.53 (P1(f5(x53421,x53421,x53422),x53421,x53422)),
% 60.51/60.53 inference(scs_inference,[],[5133,5175,5058,4852,4955,5107,4762,5109,5187,5199,5286,5215,5280,5283,5292,5304,5233,5246,4925,828,836,531,491,832,2173,534,259,153,824,225,170,171,257,226,681,224,587,2686,612,168,662,252,652,592,632,160,233,152])).
% 60.51/60.53 cnf(5356,plain,
% 60.51/60.53 (P9(a17,a15,a16,a2)),
% 60.51/60.53 inference(scs_inference,[],[5133,5175,5058,4852,4772,4905,4955,5107,5131,4762,5109,5165,5187,5199,5286,5215,5280,5283,5292,5304,5233,5246,4925,828,836,531,491,832,2173,534,259,153,824,225,170,171,257,226,681,224,587,2686,612,168,662,252,652,592,632,160,233,152,169,254,569,258,255,256,163])).
% 60.51/60.53 cnf(5358,plain,
% 60.51/60.53 (P1(x53581,f5(x53582,x53582,x53581),x53582)),
% 60.51/60.53 inference(scs_inference,[],[5133,5175,5058,4852,4772,4905,4955,5107,5131,4762,5109,5165,5187,5199,5286,5215,5280,5283,5292,5304,5233,5246,4925,828,836,531,491,832,2173,534,259,153,824,225,170,171,257,226,681,224,587,2686,612,168,662,252,652,592,632,160,233,152,169,254,569,258,255,256,163,151])).
% 60.51/60.53 cnf(5364,plain,
% 60.51/60.53 (P3(f21(a17,x53641),x53641,a17)),
% 60.51/60.53 inference(scs_inference,[],[5133,5175,5058,4852,4772,4905,4955,5107,5131,4762,5109,5163,5165,5187,5199,5286,5215,5280,5283,5292,5304,5233,5246,4925,828,836,531,491,832,2173,534,259,153,824,225,170,171,257,226,681,224,587,2686,612,168,662,252,652,592,632,160,233,152,169,254,569,258,255,256,163,151,253,164,154])).
% 60.51/60.53 cnf(5370,plain,
% 60.51/60.53 (P4(a17,a2,a2,a17)),
% 60.51/60.53 inference(scs_inference,[],[5133,5175,4911,5058,4852,4772,4905,4955,5107,5131,4762,5097,5109,5125,5163,5165,5187,5199,5286,5215,5280,5283,5292,5304,5233,5246,4925,828,836,531,491,832,2173,534,259,153,824,225,170,171,257,226,681,224,587,2686,612,168,662,252,652,592,632,160,233,152,169,254,569,258,255,256,163,151,253,164,154,165,166,167])).
% 60.51/60.53 cnf(5374,plain,
% 60.51/60.53 (P3(a16,a16,a16)),
% 60.51/60.53 inference(scs_inference,[],[5133,5175,4911,5058,4852,4772,4905,4955,5107,5131,4762,5097,5109,5125,5147,5163,5165,5187,5199,5286,5215,5280,5283,5292,5304,5233,5246,4925,5050,828,836,531,491,832,2173,534,259,153,824,225,170,171,257,226,681,224,587,2686,612,168,662,252,652,592,632,160,233,152,169,254,569,258,255,256,163,151,253,164,154,165,166,167,156,161])).
% 60.51/60.53 cnf(5377,plain,
% 60.51/60.53 (P10(x53771,x53772,x53771,x53772)),
% 60.51/60.53 inference(rename_variables,[],[5030])).
% 60.51/60.53 cnf(5389,plain,
% 60.51/60.53 (P10(x53891,x53892,x53891,x53892)),
% 60.51/60.53 inference(rename_variables,[],[5030])).
% 60.51/60.53 cnf(5391,plain,
% 60.51/60.53 (~P10(f21(a2,a20),a1,a20,a2)),
% 60.51/60.53 inference(scs_inference,[],[5133,5175,5295,4911,5058,4852,4772,4905,4955,5107,5131,5139,4762,4981,5097,5109,5125,5147,5163,5165,5187,5253,5199,5286,5215,5280,5283,5292,5304,5233,5246,5228,4925,5030,5377,5050,4497,4321,828,836,531,491,832,2173,534,259,153,824,225,170,171,257,226,681,224,587,2686,612,168,662,252,652,592,632,160,233,152,169,254,569,258,255,256,163,151,253,164,154,165,166,167,156,161,188,249,183,262,247,176,180])).
% 60.51/60.53 cnf(5392,plain,
% 60.51/60.53 (P10(x53921,x53922,x53922,x53921)),
% 60.51/60.53 inference(rename_variables,[],[5175])).
% 60.51/60.53 cnf(5398,plain,
% 60.51/60.53 (P5(a15,a16,a16,a16)),
% 60.51/60.53 inference(scs_inference,[],[5133,5175,5295,4911,5058,4852,4772,4905,4955,5107,5131,5139,4762,4981,5097,5109,5125,5147,5163,5165,5187,5253,5199,5286,5215,5280,5283,5292,5304,5233,5246,5228,4925,5030,5377,4309,5050,4497,4321,828,836,531,491,832,2173,534,259,153,824,225,170,171,257,226,681,224,587,2686,612,168,662,252,652,592,632,160,233,152,169,254,569,258,255,256,163,151,253,164,154,165,166,167,156,161,188,249,183,262,247,176,180,205,246,236])).
% 60.51/60.53 cnf(5405,plain,
% 60.51/60.53 (P4(x54051,a16,x54051,f27(a16,x54051,a16,a16,a16))),
% 60.51/60.53 inference(scs_inference,[],[5133,5175,5295,5392,4911,5058,4852,4772,4905,4955,5107,5131,5139,4762,4981,5097,5109,5125,5147,5163,5165,5187,5253,5199,5286,5215,5280,5283,5292,5304,5233,5246,5228,4925,5030,5377,4309,4563,5050,4497,4321,828,836,531,491,832,2173,534,259,153,824,225,170,171,257,226,681,224,587,2686,612,168,662,252,652,592,632,160,233,152,169,254,569,258,255,256,163,151,253,164,154,165,166,167,156,161,188,249,183,262,247,176,180,205,246,236,245,263,200])).
% 60.51/60.53 cnf(5406,plain,
% 60.51/60.53 (P10(x54061,x54062,x54062,x54061)),
% 60.51/60.53 inference(rename_variables,[],[5175])).
% 60.51/60.53 cnf(5411,plain,
% 60.51/60.53 (P3(f21(a17,x54111),a17,x54111)),
% 60.51/60.53 inference(rename_variables,[],[5246])).
% 60.51/60.53 cnf(5415,plain,
% 60.51/60.53 (P9(f21(a17,x54151),f21(a17,x54151),x54151,x54151)),
% 60.51/60.53 inference(scs_inference,[],[5133,5175,5295,5392,4911,5058,4852,4772,4905,4955,5107,5131,5139,4762,4981,5097,5109,5125,5147,5163,5165,5187,5208,5253,5199,5286,5215,5280,5283,5292,5304,5233,5246,5411,5228,4925,5030,5377,4309,4563,5050,4497,4321,828,836,531,491,832,2173,534,259,153,824,225,170,171,257,226,681,224,587,2686,612,168,662,252,652,592,632,160,233,152,169,254,569,258,255,256,163,151,253,164,154,165,166,167,156,161,188,249,183,262,247,176,180,205,246,236,245,263,200,250,227,177,158])).
% 60.51/60.53 cnf(5418,plain,
% 60.51/60.53 (P10(x54181,x54182,x54182,x54181)),
% 60.51/60.53 inference(rename_variables,[],[5175])).
% 60.51/60.53 cnf(5423,plain,
% 60.51/60.53 (P10(x54231,x54232,x54232,x54231)),
% 60.51/60.53 inference(rename_variables,[],[5175])).
% 60.51/60.53 cnf(5425,plain,
% 60.51/60.53 (P2(f3(a2,a2,a2),f3(a2,a2,a2),a2,a2)),
% 60.51/60.53 inference(scs_inference,[],[5133,5175,5295,5392,5406,5418,4911,5058,4852,4772,4905,4955,5107,5131,5139,4762,4981,5097,5109,5125,5147,5163,5165,5187,5208,5253,5199,5286,5215,5280,5283,5292,5304,5233,5246,5411,5228,4925,5030,5377,4309,4563,5050,4497,4321,828,836,531,491,832,2173,534,259,153,824,225,170,171,257,226,681,224,587,2686,612,168,662,252,652,592,632,160,233,152,169,254,569,258,255,256,163,151,253,164,154,165,166,167,156,161,188,249,183,262,247,176,180,205,246,236,245,263,200,250,227,177,158,201,190,191,184])).
% 60.51/60.53 cnf(5427,plain,
% 60.51/60.53 (P9(a17,a17,x54271,x54271)),
% 60.51/60.53 inference(scs_inference,[],[5133,5175,5295,5392,5406,5418,4911,5058,4852,4772,4905,4955,5107,5131,5139,4762,4981,5097,5109,5125,5147,5163,5165,5187,5208,5253,5199,5286,5215,5280,5283,5292,5304,5233,5246,5411,5228,4925,5030,5377,4309,4563,5050,4497,4321,828,836,531,491,832,2173,534,259,153,824,225,170,171,257,226,681,224,587,2686,612,168,662,252,652,592,632,160,233,152,169,254,569,258,255,256,163,151,253,164,154,165,166,167,156,161,188,249,183,262,247,176,180,205,246,236,245,263,200,250,227,177,158,201,190,191,184,157])).
% 60.51/60.53 cnf(5436,plain,
% 60.51/60.53 (P10(x54361,x54362,x54362,x54361)),
% 60.51/60.53 inference(rename_variables,[],[5175])).
% 60.51/60.53 cnf(5442,plain,
% 60.51/60.53 (~P9(a1,f21(a2,a20),a2,a20)),
% 60.51/60.53 inference(scs_inference,[],[142,5133,5175,5295,5392,5406,5418,5423,5436,4911,5058,4852,4772,4905,4955,5107,5131,5139,4762,4981,5097,5109,5125,5147,5163,5165,5187,5208,5253,5199,5286,5215,5280,5283,5292,5304,5233,5246,5411,5228,4925,5030,5377,4309,4563,5050,4872,4497,4321,828,836,531,491,832,2173,534,259,153,824,225,170,171,257,226,681,224,587,2686,612,168,662,252,652,592,632,160,233,152,169,254,569,258,255,256,163,151,253,164,154,165,166,167,156,161,188,249,183,262,247,176,180,205,246,236,245,263,200,250,227,177,158,201,190,191,184,157,178,223,193,197,240,194,182])).
% 60.51/60.53 cnf(5443,plain,
% 60.51/60.53 (P10(x54431,x54432,x54432,x54431)),
% 60.51/60.53 inference(rename_variables,[],[5175])).
% 60.51/60.53 cnf(5448,plain,
% 60.51/60.53 (P10(x54481,x54482,x54482,x54481)),
% 60.51/60.53 inference(rename_variables,[],[5175])).
% 60.51/60.53 cnf(5452,plain,
% 60.51/60.53 (~P9(f21(a2,a20),a1,a20,a2)),
% 60.51/60.53 inference(scs_inference,[],[142,5133,5175,5295,5392,5406,5418,5423,5436,5443,5204,4911,5058,4852,4772,4905,4955,5107,5131,5139,4762,4981,5097,5109,5125,5147,5163,5165,5187,5208,5253,5199,5286,5215,5280,5283,5292,5304,5233,5246,5411,5228,4925,5030,5377,4309,4563,5050,4872,4497,4321,828,836,531,491,832,2173,534,259,153,824,225,170,171,257,226,681,224,587,2686,612,168,662,252,652,592,632,160,233,152,169,254,569,258,255,256,163,151,253,164,154,165,166,167,156,161,188,249,183,262,247,176,180,205,246,236,245,263,200,250,227,177,158,201,190,191,184,157,178,223,193,197,240,194,182,189,199,203,179])).
% 60.51/60.53 cnf(5453,plain,
% 60.51/60.53 (P9(x54531,x54532,x54532,x54531)),
% 60.51/60.53 inference(rename_variables,[],[5204])).
% 60.51/60.53 cnf(5456,plain,
% 60.51/60.53 (P10(x54561,x54562,x54561,x54562)),
% 60.51/60.53 inference(rename_variables,[],[5030])).
% 60.51/60.53 cnf(5457,plain,
% 60.51/60.53 (P3(f21(a17,x54571),a17,x54571)),
% 60.51/60.53 inference(rename_variables,[],[5246])).
% 60.51/60.53 cnf(5459,plain,
% 60.51/60.53 (P4(f3(a2,a2,a2),a2,f3(a2,a2,a2),f3(a2,a2,a2))),
% 60.51/60.53 inference(scs_inference,[],[142,5133,5175,5295,5392,5406,5418,5423,5436,5443,5448,5204,4911,5058,4852,4772,4905,4955,5107,5131,5139,4762,4981,5097,5109,5125,5147,5163,5165,5187,5208,5253,5199,5286,5215,5280,5283,5292,5304,5233,5246,5411,5228,4925,5030,5377,5389,5044,4309,4563,5050,4872,4497,4321,828,836,531,491,832,2173,534,259,153,824,225,170,171,257,226,681,224,587,2686,612,168,662,252,652,592,632,160,233,152,169,254,569,258,255,256,163,151,253,164,154,165,166,167,156,161,188,249,183,262,247,176,180,205,246,236,245,263,200,250,227,177,158,201,190,191,184,157,178,223,193,197,240,194,182,189,199,203,179,174,173])).
% 60.51/60.53 cnf(5460,plain,
% 60.51/60.53 (P10(x54601,x54602,x54602,x54601)),
% 60.51/60.53 inference(rename_variables,[],[5175])).
% 60.51/60.53 cnf(5467,plain,
% 60.51/60.53 (P10(f25(a2,a2,a2,a2,a2,a2),f25(a2,a2,a2,a2,a2,a2),a2,a2)),
% 60.51/60.53 inference(scs_inference,[],[142,5133,5175,5295,5392,5406,5418,5423,5436,5443,5448,5204,4911,5058,4852,4772,4905,4955,5107,5131,5139,4762,4981,5097,5109,5125,5147,5163,5165,5187,5208,5253,5199,5286,5215,5280,5283,5292,5304,5233,5246,5411,5177,4939,5228,4925,5030,5377,5389,5456,5044,4309,4563,5050,266,4872,4497,4321,828,836,531,491,832,2173,534,259,153,824,225,170,171,257,226,681,224,587,2686,612,168,662,252,652,592,632,160,233,152,169,254,569,258,255,256,163,151,253,164,154,165,166,167,156,161,188,249,183,262,247,176,180,205,246,236,245,263,200,250,227,177,158,201,190,191,184,157,178,223,193,197,240,194,182,189,199,203,179,174,173,241,243,181])).
% 60.51/60.53 cnf(5470,plain,
% 60.51/60.53 (P10(x54701,x54702,x54702,x54701)),
% 60.51/60.53 inference(rename_variables,[],[5175])).
% 60.51/60.53 cnf(5477,plain,
% 60.51/60.53 (P3(a2,a16,a18)),
% 60.51/60.53 inference(scs_inference,[],[142,5133,5175,5295,5392,5406,5418,5423,5436,5443,5448,5460,5470,5204,5453,4911,5058,4852,4772,4905,4955,5107,5131,5139,4762,4967,4981,5097,5109,5125,5147,5163,5165,5187,5208,5253,5199,5286,5215,5280,5283,5292,5304,5233,5246,5411,5457,5177,4939,5228,4925,5030,5377,5389,5456,5044,4309,4563,5050,266,4872,4497,4321,147,828,836,531,491,832,2173,534,259,153,824,225,170,171,257,226,681,224,587,2686,612,168,662,252,652,592,632,160,233,152,169,254,569,258,255,256,163,151,253,164,154,165,166,167,156,161,188,249,183,262,247,176,180,205,246,236,245,263,200,250,227,177,158,201,190,191,184,157,178,223,193,197,240,194,182,189,199,203,179,174,173,241,243,181,198,186,162])).
% 60.51/60.53 cnf(5478,plain,
% 60.51/60.53 (P9(x54781,x54782,x54782,x54781)),
% 60.51/60.53 inference(rename_variables,[],[5204])).
% 60.51/60.53 cnf(5485,plain,
% 60.51/60.53 (P3(f21(a16,x54851),a16,x54851)),
% 60.51/60.53 inference(scs_inference,[],[142,5133,5175,5295,5392,5406,5418,5423,5436,5443,5448,5460,5470,5204,5453,4911,5058,4852,4772,4905,4955,5107,5131,5139,4762,4967,4981,5097,5109,5125,5147,5163,5165,5187,5208,5253,5199,5286,5215,5280,5283,5292,5304,5233,5246,5411,5457,5177,4939,5228,4925,5242,5030,5377,5389,5456,5044,4309,4439,4563,5050,266,4872,4497,4443,4321,306,147,828,836,531,491,832,2173,534,259,153,824,225,170,171,257,226,681,224,587,2686,612,168,662,252,652,592,632,160,233,152,169,254,569,258,255,256,163,151,253,164,154,165,166,167,156,161,188,249,183,262,247,176,180,205,246,236,245,263,200,250,227,177,158,201,190,191,184,157,178,223,193,197,240,194,182,189,199,203,179,174,173,241,243,181,198,186,162,175,209,159])).
% 60.51/60.53 cnf(5488,plain,
% 60.51/60.53 (P9(x54881,x54882,x54882,x54881)),
% 60.51/60.53 inference(rename_variables,[],[5204])).
% 60.51/60.53 cnf(5510,plain,
% 60.51/60.53 (P9(f27(a16,a15,a16,a16,a16),a16,a2,a17)),
% 60.51/60.53 inference(scs_inference,[],[142,5133,5175,5295,5392,5406,5418,5423,5436,5443,5448,5460,5470,5204,5453,5478,5488,4911,5058,4852,4772,4905,4955,5107,5131,5139,4762,4967,4981,5097,5109,5125,5147,5163,5165,5187,5208,5253,5199,5286,5215,5280,5283,5292,5304,5233,5246,5411,5457,5177,4939,5228,4925,5242,5030,5377,5389,5456,4279,5044,4309,4439,4563,5050,4571,266,4872,4497,4443,4321,306,147,828,836,531,491,832,2173,534,259,153,824,225,170,171,257,226,681,224,587,2686,612,168,662,252,652,592,632,160,233,152,169,254,569,258,255,256,163,151,253,164,154,165,166,167,156,161,188,249,183,262,247,176,180,205,246,236,245,263,200,250,227,177,158,201,190,191,184,157,178,223,193,197,240,194,182,189,199,203,179,174,173,241,243,181,198,186,162,175,209,159,207,206,251,415,456,4210,585,671,648,589,480])).
% 60.51/60.53 cnf(5524,plain,
% 60.51/60.53 (P9(f21(a17,x55241),f21(a17,x55241),x55241,x55241)),
% 60.51/60.53 inference(rename_variables,[],[5415])).
% 60.51/60.53 cnf(5527,plain,
% 60.51/60.53 (P9(f21(a17,x55271),f21(a17,x55271),x55271,x55271)),
% 60.51/60.53 inference(rename_variables,[],[5415])).
% 60.51/60.53 cnf(5530,plain,
% 60.51/60.53 (P9(f21(a17,x55301),f21(a17,x55301),x55301,x55301)),
% 60.51/60.53 inference(rename_variables,[],[5415])).
% 60.51/60.53 cnf(5533,plain,
% 60.51/60.53 (P1(f5(x55331,x55331,x55332),x55331,x55332)),
% 60.51/60.53 inference(rename_variables,[],[5342])).
% 60.51/60.53 cnf(5536,plain,
% 60.51/60.53 (P1(f5(x55361,x55361,x55362),x55361,x55362)),
% 60.51/60.53 inference(rename_variables,[],[5342])).
% 60.51/60.53 cnf(5539,plain,
% 60.51/60.53 (P10(x55391,f4(x55391,x55391,x55392),x55392,x55391)),
% 60.51/60.53 inference(rename_variables,[],[5223])).
% 60.51/60.53 cnf(5542,plain,
% 60.51/60.53 (P1(f5(x55421,x55421,x55422),x55421,x55422)),
% 60.51/60.53 inference(rename_variables,[],[5342])).
% 60.51/60.53 cnf(5545,plain,
% 60.51/60.53 (P10(x55451,f4(x55451,x55451,x55452),x55452,x55451)),
% 60.51/60.53 inference(rename_variables,[],[5223])).
% 60.51/60.53 cnf(5630,plain,
% 60.51/60.53 (P1(x56301,x56302,x56302)),
% 60.51/60.53 inference(rename_variables,[],[5338])).
% 60.51/60.53 cnf(5633,plain,
% 60.51/60.53 (P4(x56331,a16,x56331,f27(a16,x56331,a16,a16,a16))),
% 60.51/60.53 inference(rename_variables,[],[5405])).
% 60.51/60.53 cnf(5637,plain,
% 60.51/60.53 (P10(x56371,x56372,x56372,x56371)),
% 60.51/60.53 inference(rename_variables,[],[5175])).
% 60.51/60.53 cnf(5647,plain,
% 60.51/60.53 (P10(x56471,x56472,x56472,x56471)),
% 60.51/60.53 inference(rename_variables,[],[5175])).
% 60.51/60.53 cnf(5653,plain,
% 60.51/60.53 (P10(x56531,x56532,x56532,x56531)),
% 60.51/60.53 inference(rename_variables,[],[5175])).
% 60.51/60.53 cnf(5654,plain,
% 60.51/60.53 (P8(x56541,x56542,x56543,x56544,x56541,x56542,x56543,x56544)),
% 60.51/60.53 inference(rename_variables,[],[5306])).
% 60.51/60.53 cnf(5659,plain,
% 60.51/60.53 (P8(x56591,x56592,x56593,x56594,x56591,x56592,x56593,x56594)),
% 60.51/60.53 inference(rename_variables,[],[5306])).
% 60.51/60.53 cnf(5660,plain,
% 60.51/60.53 (P1(x56601,x56602,x56602)),
% 60.51/60.53 inference(rename_variables,[],[5338])).
% 60.51/60.53 cnf(5674,plain,
% 60.51/60.53 (P10(x56741,x56742,x56742,x56741)),
% 60.51/60.53 inference(rename_variables,[],[5175])).
% 60.51/60.53 cnf(5688,plain,
% 60.51/60.53 (P10(x56881,x56882,x56882,x56881)),
% 60.51/60.53 inference(rename_variables,[],[5175])).
% 60.51/60.53 cnf(5708,plain,
% 60.51/60.53 (P9(x57081,x57082,x57082,x57081)),
% 60.51/60.53 inference(rename_variables,[],[5204])).
% 60.51/60.53 cnf(5723,plain,
% 60.51/60.53 (P1(x57231,x57232,x57232)),
% 60.51/60.53 inference(rename_variables,[],[5338])).
% 60.51/60.53 cnf(5734,plain,
% 60.51/60.53 ($false),
% 60.51/60.53 inference(scs_inference,[],[5306,5654,5659,5338,5630,5660,5723,5085,5091,4802,5320,5268,5167,5330,5427,4464,4565,4909,4945,5155,5161,5171,5236,5238,5310,5356,5370,5374,5398,5477,5223,5539,5545,5342,5533,5536,5542,5358,5415,5524,5527,5530,5459,5326,5340,5405,5633,5364,5485,5467,5425,5391,5442,5452,5022,5288,5510,5153,5056,5175,5637,5647,5653,5674,5688,5204,5708,4816,5242,5208,4975,5030,5042,5133,4299,4275,5050,4983,4509,578,614,625,828,836,531,832,2173,491,671,259,534,257,224,170,824,226,225,153,681,2686,171,612,254,252,587,632,168,152,169,652,258,569,160,662,256,592,163,255,151,154,165,164,253,167,166,156,161,106,238,188,2036,185,205,176,183,246,180,236,204,155,263,245,177,191,184,190,227,193,178,197,189,223,157,240,182,194,203,179,172,174,173,181,243,198,192,186,239,175]),
% 60.51/60.53 ['proof']).
% 60.51/60.53 % SZS output end Proof
% 60.51/60.53 % Total time :59.760000s
%------------------------------------------------------------------------------