%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : GEO595+1 : TPTP v8.2.0. Released v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% Computer : 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:05:51 EDT 2024
% Result : Theorem 59.98s 60.11s
% Output : CNFRefutation 60.06s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.05/0.10 % Problem : GEO595+1 : TPTP v8.2.0. Released v7.5.0.
% 0.05/0.10 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% 0.09/0.30 % Computer : n021.cluster.edu
% 0.09/0.30 % Model : x86_64 x86_64
% 0.09/0.30 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.30 % Memory : 8042.1875MB
% 0.09/0.30 % OS : Linux 3.10.0-693.el7.x86_64
% 0.09/0.30 % CPULimit : 300
% 0.09/0.30 % WCLimit : 300
% 0.09/0.30 % DateTime : Fri Jun 21 07:10:39 EDT 2024
% 0.09/0.30 % CPUTime :
% 0.15/0.53 start to proof:theBenchmark
% 59.98/60.10 %-------------------------------------------
% 59.98/60.10 % File :CSE---1.7
% 59.98/60.10 % Problem :theBenchmark
% 59.98/60.10 % Transform :cnf
% 59.98/60.10 % Format :tptp:raw
% 59.98/60.10 % Command :java -jar mcs_scs.jar %d %s
% 59.98/60.10
% 59.98/60.10 % Result :Theorem 59.430000s
% 59.98/60.10 % Output :CNFRefutation 59.430000s
% 59.98/60.10 %-------------------------------------------
% 59.98/60.11 %------------------------------------------------------------------------------
% 59.98/60.11 % File : GEO595+1 : TPTP v8.2.0. Released v7.5.0.
% 59.98/60.11 % Domain : Geometry
% 59.98/60.11 % Problem : JGEX problem 57
% 59.98/60.11 % Version : [CGZ00] axioms.
% 59.98/60.11 % English :
% 59.98/60.11
% 59.98/60.11 % Refs : [CGZ00] Chou et al. (2000), A Deductive Database Approach to A
% 59.98/60.11 % : [YCG08] Ye et al. (2008), An Introduction to Java Geometry Exp
% 59.98/60.11 % : [Qua20] Quaresma (2020), Email to Geoff Sutcliffe
% 59.98/60.11 % Source : [Qua20]
% 59.98/60.11 % Names : 57.p [Qua20]
% 59.98/60.11
% 59.98/60.11 % Status : Theorem
% 59.98/60.11 % Rating : 0.36 v8.1.0, 0.47 v7.5.0
% 59.98/60.11 % Syntax : Number of formulae : 95 ( 0 unt; 0 def)
% 59.98/60.11 % Number of atoms : 292 ( 1 equ)
% 59.98/60.11 % Maximal formula atoms : 9 ( 3 avg)
% 59.98/60.11 % Number of connectives : 204 ( 7 ~; 0 |; 102 &)
% 59.98/60.11 % ( 0 <=>; 95 =>; 0 <=; 0 <~>)
% 59.98/60.11 % Maximal formula depth : 20 ( 9 avg)
% 59.98/60.11 % Maximal term depth : 1 ( 1 avg)
% 59.98/60.11 % Number of predicates : 12 ( 11 usr; 0 prp; 2-8 aty)
% 59.98/60.11 % Number of functors : 0 ( 0 usr; 0 con; --- aty)
% 59.98/60.11 % Number of variables : 533 ( 513 !; 20 ?)
% 59.98/60.11 % SPC : FOF_THM_RFO_SEQ
% 59.98/60.11
% 59.98/60.11 % Comments : Taken from JGEX [YCG08], converted by Pedro Quaresma.
% 59.98/60.11 %------------------------------------------------------------------------------
% 59.98/60.11 include('Axioms/GEO012+0.ax').
% 59.98/60.11 %------------------------------------------------------------------------------
% 59.98/60.11 fof(exemplo6GDDFULL416057,conjecture,
% 59.98/60.11 ! [A,B,C,D,O,E,F,NWPNT1,NWPNT2,NWPNT3,NWPNT4] :
% 59.98/60.11 ( ( perp(D,A,B,C)
% 59.98/60.11 & coll(D,B,C)
% 59.98/60.11 & midp(O,A,D)
% 59.98/60.11 & circle(O,D,NWPNT1,NWPNT2)
% 59.98/60.11 & coll(E,A,B)
% 59.98/60.11 & circle(O,D,E,NWPNT3)
% 59.98/60.11 & coll(F,A,C)
% 59.98/60.11 & circle(O,D,F,NWPNT4) )
% 59.98/60.11 => cyclic(B,C,E,F) ) ).
% 59.98/60.11
% 59.98/60.11 %------------------------------------------------------------------------------
% 59.98/60.11 %-------------------------------------------
% 59.98/60.11 % Proof found
% 59.98/60.11 % SZS status Theorem for theBenchmark
% 59.98/60.11 % SZS output start Proof
% 60.01/60.13 %ClaNum:263(EqnAxiom:141)
% 60.01/60.13 %VarNum:1613(SingletonVarNum:590)
% 60.01/60.13 %MaxLitNum:5
% 60.01/60.13 %MaxfuncDepth:1
% 60.01/60.13 %SharedTerms:20
% 60.01/60.13 %goalClause: 142 143 144 145 146 147 148 149 150
% 60.01/60.13 %singleGoalClaCount:9
% 60.01/60.13 [142]P1(a1,a2,a16)
% 60.01/60.13 [143]P1(a17,a3,a2)
% 60.01/60.13 [144]P1(a19,a3,a16)
% 60.01/60.13 [145]P3(a18,a3,a1)
% 60.01/60.13 [146]P9(a1,a3,a2,a16)
% 60.01/60.13 [147]P2(a18,a1,a17,a20)
% 60.01/60.13 [148]P2(a18,a1,a19,a24)
% 60.01/60.13 [149]P2(a18,a1,a21,a22)
% 60.01/60.13 [150]~P4(a2,a16,a17,a19)
% 60.01/60.13 [151]~P1(x1512,x1511,x1513)+P1(x1511,x1512,x1513)
% 60.01/60.13 [152]~P1(x1521,x1523,x1522)+P1(x1521,x1522,x1523)
% 60.01/60.13 [153]~P3(x1531,x1532,x1533)+P1(x1531,x1532,x1533)
% 60.01/60.13 [154]~P3(x1541,x1543,x1542)+P3(x1541,x1542,x1543)
% 60.01/60.13 [156]~P3(x1561,x1562,x1563)+P5(x1561,x1562,x1561,x1563)
% 60.01/60.13 [160]~P10(x1601,x1602,x1601,x1603)+P1(x1601,x1602,x1603)
% 60.01/60.13 [226]~P5(x2261,x2262,x2261,x2263)+P8(x2261,x2262,x2262,x2263,x2262,x2263,x2261,x2263)
% 60.01/60.13 [163]~P10(x1633,x1634,x1631,x1632)+P10(x1631,x1632,x1633,x1634)
% 60.01/60.13 [164]~P10(x1641,x1642,x1644,x1643)+P10(x1641,x1642,x1643,x1644)
% 60.01/60.13 [165]~P9(x1653,x1654,x1651,x1652)+P9(x1651,x1652,x1653,x1654)
% 60.01/60.13 [166]~P9(x1661,x1662,x1664,x1663)+P9(x1661,x1662,x1663,x1664)
% 60.01/60.13 [167]~P5(x1673,x1674,x1671,x1672)+P5(x1671,x1672,x1673,x1674)
% 60.01/60.13 [168]~P5(x1681,x1682,x1684,x1683)+P5(x1681,x1682,x1683,x1684)
% 60.01/60.13 [169]~P4(x1692,x1691,x1693,x1694)+P4(x1691,x1692,x1693,x1694)
% 60.01/60.13 [170]~P4(x1701,x1703,x1702,x1704)+P4(x1701,x1702,x1703,x1704)
% 60.01/60.13 [171]~P4(x1711,x1712,x1714,x1713)+P4(x1711,x1712,x1713,x1714)
% 60.01/60.13 [224]~P4(x2242,x2243,x2241,x2244)+P8(x2241,x2242,x2241,x2243,x2244,x2242,x2244,x2243)
% 60.01/60.13 [187]~P2(x1874,x1871,x1872,x1873)+P9(f8(x1871,x1872,x1873,x1874),x1871,x1871,x1874)
% 60.01/60.13 [202]P5(x2021,x2022,x2023,x2024)+~P6(x2021,x2022,x2025,x2023,x2024,x2026)
% 60.01/60.13 [214]~P11(x2144,x2145,x2146,x2141,x2142,x2143)+P11(x2141,x2142,x2143,x2144,x2145,x2146)
% 60.01/60.13 [215]~P11(x2152,x2151,x2153,x2155,x2154,x2156)+P11(x2151,x2152,x2153,x2154,x2155,x2156)
% 60.01/60.13 [216]~P11(x2161,x2163,x2162,x2164,x2166,x2165)+P11(x2161,x2162,x2163,x2164,x2165,x2166)
% 60.01/60.13 [217]~P6(x2174,x2175,x2176,x2171,x2172,x2173)+P6(x2171,x2172,x2173,x2174,x2175,x2176)
% 60.01/60.13 [218]~P6(x2182,x2181,x2183,x2185,x2184,x2186)+P6(x2181,x2182,x2183,x2184,x2185,x2186)
% 60.01/60.13 [219]~P6(x2191,x2193,x2192,x2194,x2196,x2195)+P6(x2191,x2192,x2193,x2194,x2195,x2196)
% 60.01/60.13 [225]~P10(x2251,x2252,x2255,x2256)+P8(x2251,x2252,x2253,x2254,x2255,x2256,x2253,x2254)
% 60.01/60.13 [231]~P11(x2311,x2312,x2313,x2314,x2315,x2316)+P8(x2311,x2312,x2312,x2313,x2314,x2315,x2315,x2316)
% 60.01/60.13 [232]~P11(x2321,x2322,x2323,x2324,x2325,x2326)+P7(x2321,x2322,x2321,x2323,x2324,x2325,x2324,x2326)
% 60.01/60.13 [233]~P8(x2331,x2332,x2335,x2336,x2333,x2334,x2335,x2336)+P10(x2331,x2332,x2333,x2334)
% 60.01/60.13 [252]~P8(x2525,x2526,x2527,x2528,x2521,x2522,x2523,x2524)+P8(x2521,x2522,x2523,x2524,x2525,x2526,x2527,x2528)
% 60.01/60.13 [253]~P8(x2533,x2534,x2531,x2532,x2537,x2538,x2535,x2536)+P8(x2531,x2532,x2533,x2534,x2535,x2536,x2537,x2538)
% 60.01/60.13 [254]~P8(x2542,x2541,x2543,x2544,x2545,x2546,x2547,x2548)+P8(x2541,x2542,x2543,x2544,x2545,x2546,x2547,x2548)
% 60.01/60.13 [255]~P8(x2551,x2552,x2555,x2556,x2553,x2554,x2557,x2558)+P8(x2551,x2552,x2553,x2554,x2555,x2556,x2557,x2558)
% 60.01/60.13 [256]~P7(x2565,x2566,x2567,x2568,x2561,x2562,x2563,x2564)+P7(x2561,x2562,x2563,x2564,x2565,x2566,x2567,x2568)
% 60.01/60.13 [257]~P7(x2573,x2574,x2571,x2572,x2577,x2578,x2575,x2576)+P7(x2571,x2572,x2573,x2574,x2575,x2576,x2577,x2578)
% 60.01/60.13 [258]~P7(x2582,x2581,x2583,x2584,x2585,x2586,x2587,x2588)+P7(x2581,x2582,x2583,x2584,x2585,x2586,x2587,x2588)
% 60.01/60.13 [259]~P7(x2591,x2592,x2595,x2596,x2593,x2594,x2597,x2598)+P7(x2591,x2592,x2593,x2594,x2595,x2596,x2597,x2598)
% 60.01/60.13 [161]~P1(x1611,x1612,x1613)+~P5(x1611,x1612,x1611,x1613)+P3(x1611,x1612,x1613)
% 60.01/60.13 [235]P5(x2351,x2352,x2351,x2353)+~P8(x2351,x2352,x2352,x2353,x2352,x2353,x2351,x2353)+P1(x2351,x2352,x2353)
% 60.01/60.13 [176]~P9(x1761,x1762,x1762,x1763)+~P5(x1762,x1761,x1762,x1763)+P1(x1761,x1762,f4(x1761,x1763,x1762))
% 60.01/60.13 [188]~P9(x1882,x1881,x1881,x1883)+~P5(x1881,x1882,x1881,x1883)+P5(x1881,x1882,x1881,f4(x1882,x1883,x1881))
% 60.01/60.13 [155]~P1(x1553,x1554,x1551)+P1(x1551,x1552,x1553)+~P1(x1553,x1554,x1552)
% 60.01/60.13 [172]~P2(x1724,x1721,x1722,x1723)+P9(x1721,x1722,x1722,x1723)+~P1(x1724,x1721,x1723)
% 60.01/60.13 [173]~P9(x1731,x1734,x1732,x1733)+P5(x1731,x1732,x1731,x1733)+~P3(x1734,x1732,x1733)
% 60.01/60.13 [174]~P9(x1741,x1743,x1743,x1744)+P5(x1741,x1742,x1743,x1742)+~P3(x1742,x1741,x1744)
% 60.01/60.13 [181]~P5(x1811,x1814,x1812,x1814)+~P5(x1811,x1813,x1812,x1813)+P9(x1811,x1812,x1813,x1814)
% 60.01/60.13 [184]~P5(x1841,x1842,x1841,x1844)+~P5(x1841,x1842,x1841,x1843)+P2(x1841,x1842,x1843,x1844)
% 60.01/60.13 [230]~P10(x2301,x2304,x2303,x2302)+~P4(x2301,x2304,x2303,x2302)+P8(x2301,x2302,x2303,x2302,x2303,x2302,x2303,x2304)
% 60.01/60.13 [234]~P8(x2341,x2343,x2341,x2344,x2342,x2343,x2342,x2344)+P1(x2341,x2342,x2343)+P4(x2343,x2344,x2341,x2342)
% 60.01/60.13 [236]~P1(x2363,x2364,x2362)+~P8(x2363,x2361,x2363,x2362,x2364,x2361,x2364,x2362)+P4(x2361,x2362,x2363,x2364)
% 60.01/60.13 [238]P9(x2381,x2382,x2383,x2384)+~P8(x2381,x2382,x2383,x2384,x2383,x2384,x2381,x2382)+P10(x2381,x2382,x2383,x2384)
% 60.01/60.13 [177]~P9(x1771,x1774,x1772,x1773)+~P9(x1772,x1774,x1771,x1773)+P1(f5(x1771,x1772,x1773),x1773,x1772)
% 60.01/60.13 [178]~P9(x1781,x1784,x1782,x1783)+~P9(x1782,x1784,x1781,x1783)+P1(f6(x1781,x1782,x1783),x1783,x1781)
% 60.01/60.13 [189]~P9(x1891,x1894,x1892,x1893)+~P9(x1892,x1894,x1891,x1893)+P9(x1891,f5(x1891,x1892,x1893),x1893,x1892)
% 60.01/60.13 [190]~P9(x1901,x1904,x1902,x1903)+~P9(x1902,x1904,x1901,x1903)+P9(x1901,f6(x1902,x1901,x1903),x1903,x1902)
% 60.01/60.13 [191]~P9(x1911,x1913,x1913,x1912)+~P4(x1911,x1912,x1913,x1914)+P2(f9(x1911,x1912,x1913),x1911,x1912,x1913)
% 60.01/60.13 [193]~P9(x1933,x1934,x1932,x1931)+~P5(x1933,x1932,x1933,x1931)+P1(x1931,x1932,f26(x1932,x1931,x1933,x1934))
% 60.01/60.13 [194]~P9(x1943,x1944,x1941,x1942)+~P5(x1943,x1941,x1943,x1942)+P1(f26(x1941,x1942,x1943,x1944),x1943,x1944)
% 60.01/60.13 [245]~P5(x2453,x2452,x2453,x2451)+~P8(x2452,x2453,x2453,x2454,x2453,x2454,x2453,x2451)+P1(x2451,x2452,f23(x2452,x2451,x2453,x2454))
% 60.01/60.13 [246]~P9(x2463,x2464,x2462,x2461)+~P8(x2462,x2463,x2463,x2464,x2463,x2464,x2463,x2461)+P1(x2461,x2462,f27(x2462,x2461,x2463,x2464))
% 60.01/60.13 [247]~P9(x2473,x2472,x2472,x2471)+~P8(x2474,x2473,x2472,x2473,x2472,x2473,x2471,x2473)+P1(f15(x2471,x2472,x2473,x2474),x2473,x2474)
% 60.01/60.13 [248]~P9(x2483,x2482,x2482,x2481)+~P8(x2484,x2483,x2482,x2483,x2482,x2483,x2481,x2483)+P1(f15(x2481,x2482,x2483,x2484),x2481,x2482)
% 60.01/60.13 [249]~P5(x2493,x2491,x2493,x2492)+~P8(x2491,x2493,x2493,x2494,x2493,x2494,x2493,x2492)+P1(f23(x2491,x2492,x2493,x2494),x2493,x2494)
% 60.01/60.13 [250]~P9(x2503,x2504,x2501,x2502)+~P8(x2501,x2503,x2503,x2504,x2503,x2504,x2503,x2502)+P1(f27(x2501,x2502,x2503,x2504),x2503,x2504)
% 60.01/60.13 [157]~P3(x1575,x1571,x1573)+P10(x1571,x1572,x1573,x1574)+~P3(x1575,x1572,x1574)
% 60.01/60.13 [158]~P3(x1581,x1585,x1583)+P10(x1581,x1582,x1583,x1584)+~P3(x1582,x1585,x1584)
% 60.01/60.13 [185]~P4(x1855,x1851,x1852,x1853)+P4(x1851,x1852,x1853,x1854)+~P4(x1855,x1851,x1852,x1854)
% 60.01/60.13 [227]~P3(x2275,x2272,x2273)+~P2(x2274,x2271,x2272,x2273)+P8(x2271,x2272,x2271,x2273,x2274,x2272,x2274,x2275)
% 60.01/60.13 [229]~P2(x2295,x2291,x2293,x2294)+P8(x2291,x2292,x2291,x2293,x2294,x2291,x2294,x2293)+~P9(x2295,x2291,x2291,x2292)
% 60.01/60.13 [242]~P8(x2422,x2423,x2422,x2424,x2425,x2422,x2425,x2424)+P9(x2421,x2422,x2422,x2423)+~P2(x2421,x2422,x2424,x2425)
% 60.01/60.13 [197]~P1(x1972,x1974,x1975)+~P9(x1971,x1973,x1973,x1972)+P1(f13(x1971,x1972,x1973,x1974,x1975),x1974,x1975)
% 60.01/60.13 [198]~P1(x1982,x1984,x1985)+~P9(x1981,x1983,x1983,x1982)+P9(f13(x1981,x1982,x1983,x1984,x1985),x1981,x1984,x1985)
% 60.01/60.13 [199]~P9(x1993,x1994,x1994,x1991)+~P5(x1991,x1992,x1991,x1995)+P5(x1991,x1992,x1991,f30(x1993,x1994,x1992,x1995,x1991))
% 60.01/60.13 [200]~P9(x2003,x2001,x2001,x2005)+~P5(x2005,x2002,x2005,x2004)+P5(x2001,x2002,x2001,f30(x2003,x2001,x2002,x2004,x2005))
% 60.01/60.13 [201]~P9(x2011,x2012,x2012,x2015)+~P5(x2015,x2013,x2015,x2014)+P10(f30(x2011,x2012,x2013,x2014,x2015),x2013,x2011,x2012)
% 60.01/60.13 [244]~P8(x2441,x2443,x2442,x2443,x2441,x2444,x2442,x2445)+P1(x2441,x2442,x2443)+P4(x2444,x2442,x2443,f29(x2441,x2442,x2443,x2444))
% 60.01/60.13 [260]~P8(x2601,x2603,x2602,x2603,x2601,x2604,x2602,x2605)+P1(x2601,x2602,x2603)+P8(x2601,x2603,x2602,x2603,x2601,f29(x2601,x2602,x2603,x2604),x2602,f29(x2601,x2602,x2603,x2604))
% 60.01/60.13 [179]~P10(x1791,x1792,x1795,x1796)+P10(x1791,x1792,x1793,x1794)+~P10(x1795,x1796,x1793,x1794)
% 60.01/60.13 [180]~P9(x1801,x1802,x1805,x1806)+P10(x1801,x1802,x1803,x1804)+~P9(x1805,x1806,x1803,x1804)
% 60.01/60.13 [182]~P9(x1825,x1826,x1823,x1824)+P9(x1821,x1822,x1823,x1824)+~P10(x1821,x1822,x1825,x1826)
% 60.01/60.13 [183]~P5(x1831,x1832,x1835,x1836)+P5(x1831,x1832,x1833,x1834)+~P5(x1835,x1836,x1833,x1834)
% 60.01/60.13 [220]~P5(x2201,x2202,x2204,x2205)+~P11(x2201,x2202,x2203,x2204,x2205,x2206)+P6(x2201,x2202,x2203,x2204,x2205,x2206)
% 60.01/60.13 [223]~P3(x2234,x2235,x2236)+~P3(x2231,x2232,x2233)+P7(x2231,x2232,x2232,x2233,x2234,x2235,x2235,x2236)
% 60.01/60.13 [203]~P3(x2036,x2033,x2034)+~P3(x2035,x2031,x2032)+P3(f28(x2031,x2032,x2033,x2034,x2035,x2036),x2031,x2034)
% 60.01/60.13 [204]~P3(x2046,x2043,x2044)+~P3(x2045,x2041,x2042)+P10(f28(x2041,x2042,x2043,x2044,x2045,x2046),x2046,x2041,x2043)
% 60.01/60.13 [205]~P3(x2056,x2053,x2054)+~P3(x2055,x2051,x2052)+P10(f28(x2051,x2052,x2053,x2054,x2055,x2056),x2055,x2052,x2054)
% 60.01/60.13 [240]~P8(x2401,x2402,x2403,x2404,x2405,x2406,x2407,x2408)+P10(x2401,x2402,x2403,x2404)+~P10(x2405,x2406,x2407,x2408)
% 60.01/60.13 [241]~P8(x2411,x2412,x2413,x2414,x2415,x2416,x2417,x2418)+P9(x2411,x2412,x2413,x2414)+~P9(x2415,x2416,x2417,x2418)
% 60.01/60.13 [243]~P7(x2431,x2432,x2433,x2434,x2435,x2436,x2437,x2438)+P5(x2431,x2432,x2433,x2434)+~P5(x2435,x2436,x2437,x2438)
% 60.01/60.13 [221]~P11(x2211,x2212,x2213,x2217,x2218,x2219)+P11(x2211,x2212,x2213,x2214,x2215,x2216)+~P11(x2217,x2218,x2219,x2214,x2215,x2216)
% 60.01/60.13 [222]~P6(x2221,x2222,x2223,x2227,x2228,x2229)+P6(x2221,x2222,x2223,x2224,x2225,x2226)+~P6(x2227,x2228,x2229,x2224,x2225,x2226)
% 60.01/60.13 [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.01/60.13 [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.01/60.13 [195]~P5(x1952,x1951,x1954,x1951)+~P4(x1952,x1954,x1951,x1953)+P9(x1951,x1952,x1952,x1953)+~P5(x1952,x1953,x1954,x1953)
% 60.01/60.13 [162]~P1(x1621,x1622,x1623)+~P10(x1624,x1621,x1625,x1623)+P3(x1621,x1622,x1623)+~P3(x1624,x1622,x1625)
% 60.01/60.13 [175]~P10(x1754,x1753,x1755,x1752)+~P10(x1754,x1752,x1755,x1753)+P3(x1751,x1752,x1753)+~P3(x1751,x1754,x1755)
% 60.01/60.13 [196]~P5(x1965,x1961,x1965,x1963)+~P5(x1965,x1961,x1965,x1962)+P4(x1961,x1962,x1963,x1964)+~P5(x1965,x1961,x1965,x1964)
% 60.01/60.13 [228]~P1(x2281,x2284,x2285)+~P1(x2281,x2282,x2283)+~P10(x2282,x2284,x2283,x2285)+P7(x2281,x2282,x2282,x2283,x2281,x2284,x2284,x2285)
% 60.01/60.13 [239]~P1(x2391,x2392,x2393)+~P8(x2395,x2392,x2395,x2393,x2394,x2392,x2394,x2391)+P3(x2391,x2392,x2393)+~P2(x2394,x2395,x2392,x2393)
% 60.01/60.13 [186]~P9(x1863,x1861,x1863,x1865)+~P9(x1861,x1862,x1861,x1863)+~P3(x1864,x1862,x1865)+P3(f7(x1861,x1862,x1863),x1861,x1863)
% 60.06/60.13 [192]~P4(x1921,x1922,x1923,x1925)+~P10(x1921,x1922,x1923,x1925)+~P3(x1924,x1921,x1922)+P2(f10(x1921,x1922,x1923),x1921,x1922,x1923)
% 60.06/60.13 [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.06/60.13 [251]~P4(x2511,x2512,x2515,x2514)+~P4(x2511,x2512,x2515,x2513)+~P8(x2515,x2511,x2515,x2512,x2516,x2513,x2516,x2514)+P5(x2511,x2512,x2513,x2514)+~P4(x2511,x2512,x2515,x2516)
% 60.06/60.13 [206]~P1(x2062,x2063,x2064)+~P1(x2061,x2064,x2066)+~P1(x2061,x2063,x2065)+~P10(x2063,x2064,x2065,x2066)+P1(x2061,x2062,f14(x2063,x2064,x2065,x2066,x2061,x2062))
% 60.06/60.13 [207]~P1(x2076,x2071,x2072)+~P1(x2075,x2072,x2074)+~P1(x2075,x2071,x2073)+~P10(x2071,x2072,x2073,x2074)+P1(f14(x2071,x2072,x2073,x2074,x2075,x2076),x2073,x2074)
% 60.06/60.13 [208]~P1(x2083,x2084,x2085)+~P3(x2086,x2081,x2082)+~P10(x2081,x2083,x2085,x2086)+~P10(x2081,x2083,x2082,x2084)+P1(f31(x2081,x2082,x2083,x2084,x2085,x2086),x2086,x2085)
% 60.06/60.13 [209]~P1(x2093,x2094,x2095)+~P3(x2096,x2091,x2092)+~P10(x2091,x2093,x2095,x2096)+~P10(x2091,x2093,x2092,x2094)+P1(f31(x2091,x2092,x2093,x2094,x2095,x2096),x2091,x2094)
% 60.06/60.13 [210]~P5(x2102,x2103,x2102,x2104)+~P5(x2101,x2103,x2101,x2106)+~P2(x2101,x2103,x2104,x2105)+E(x2101,x2102)+P1(f11(x2103,x2104,x2105,x2106,x2101,x2102),x2103,x2105)
% 60.06/60.13 [211]~P5(x2112,x2113,x2112,x2114)+~P5(x2111,x2113,x2111,x2116)+~P2(x2111,x2113,x2114,x2115)+E(x2111,x2112)+P1(f12(x2113,x2114,x2115,x2116,x2111,x2112),x2114,x2116)
% 60.06/60.13 [212]~P5(x2122,x2123,x2122,x2124)+~P5(x2121,x2123,x2121,x2126)+~P2(x2121,x2123,x2124,x2125)+E(x2121,x2122)+P5(f11(x2123,x2124,x2125,x2126,x2121,x2122),x2122,x2122,x2123)
% 60.06/60.13 [213]~P5(x2132,x2133,x2132,x2134)+~P5(x2131,x2133,x2131,x2136)+~P2(x2131,x2133,x2134,x2135)+E(x2131,x2132)+P5(f12(x2133,x2134,x2135,x2136,x2131,x2132),x2132,x2132,x2133)
% 60.06/60.13 [159]~P1(x1593,x1591,x1594)+~P1(x1595,x1591,x1594)+~P3(x1596,x1595,x1593)+~P3(x1597,x1591,x1594)+P3(f25(x1591,x1592),x1591,x1592)
% 60.06/60.13 %EqnAxiom
% 60.06/60.13 [1]E(x11,x11)
% 60.06/60.13 [2]E(x22,x21)+~E(x21,x22)
% 60.06/60.13 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 60.06/60.13 [4]~E(x41,x42)+E(f25(x41,x43),f25(x42,x43))
% 60.06/60.13 [5]~E(x51,x52)+E(f25(x53,x51),f25(x53,x52))
% 60.06/60.13 [6]~E(x61,x62)+E(f4(x61,x63,x64),f4(x62,x63,x64))
% 60.06/60.13 [7]~E(x71,x72)+E(f4(x73,x71,x74),f4(x73,x72,x74))
% 60.06/60.13 [8]~E(x81,x82)+E(f4(x83,x84,x81),f4(x83,x84,x82))
% 60.06/60.13 [9]~E(x91,x92)+E(f5(x91,x93,x94),f5(x92,x93,x94))
% 60.06/60.13 [10]~E(x101,x102)+E(f5(x103,x101,x104),f5(x103,x102,x104))
% 60.06/60.13 [11]~E(x111,x112)+E(f5(x113,x114,x111),f5(x113,x114,x112))
% 60.06/60.13 [12]~E(x121,x122)+E(f6(x121,x123,x124),f6(x122,x123,x124))
% 60.06/60.13 [13]~E(x131,x132)+E(f6(x133,x131,x134),f6(x133,x132,x134))
% 60.06/60.13 [14]~E(x141,x142)+E(f6(x143,x144,x141),f6(x143,x144,x142))
% 60.06/60.13 [15]~E(x151,x152)+E(f7(x151,x153,x154),f7(x152,x153,x154))
% 60.06/60.13 [16]~E(x161,x162)+E(f7(x163,x161,x164),f7(x163,x162,x164))
% 60.06/60.13 [17]~E(x171,x172)+E(f7(x173,x174,x171),f7(x173,x174,x172))
% 60.06/60.13 [18]~E(x181,x182)+E(f8(x181,x183,x184,x185),f8(x182,x183,x184,x185))
% 60.06/60.13 [19]~E(x191,x192)+E(f8(x193,x191,x194,x195),f8(x193,x192,x194,x195))
% 60.06/60.13 [20]~E(x201,x202)+E(f8(x203,x204,x201,x205),f8(x203,x204,x202,x205))
% 60.06/60.13 [21]~E(x211,x212)+E(f8(x213,x214,x215,x211),f8(x213,x214,x215,x212))
% 60.06/60.13 [22]~E(x221,x222)+E(f29(x221,x223,x224,x225),f29(x222,x223,x224,x225))
% 60.06/60.13 [23]~E(x231,x232)+E(f29(x233,x231,x234,x235),f29(x233,x232,x234,x235))
% 60.06/60.13 [24]~E(x241,x242)+E(f29(x243,x244,x241,x245),f29(x243,x244,x242,x245))
% 60.06/60.13 [25]~E(x251,x252)+E(f29(x253,x254,x255,x251),f29(x253,x254,x255,x252))
% 60.06/60.13 [26]~E(x261,x262)+E(f23(x261,x263,x264,x265),f23(x262,x263,x264,x265))
% 60.06/60.13 [27]~E(x271,x272)+E(f23(x273,x271,x274,x275),f23(x273,x272,x274,x275))
% 60.06/60.13 [28]~E(x281,x282)+E(f23(x283,x284,x281,x285),f23(x283,x284,x282,x285))
% 60.06/60.13 [29]~E(x291,x292)+E(f23(x293,x294,x295,x291),f23(x293,x294,x295,x292))
% 60.06/60.13 [30]~E(x301,x302)+E(f27(x301,x303,x304,x305),f27(x302,x303,x304,x305))
% 60.06/60.13 [31]~E(x311,x312)+E(f27(x313,x311,x314,x315),f27(x313,x312,x314,x315))
% 60.06/60.13 [32]~E(x321,x322)+E(f27(x323,x324,x321,x325),f27(x323,x324,x322,x325))
% 60.06/60.14 [33]~E(x331,x332)+E(f27(x333,x334,x335,x331),f27(x333,x334,x335,x332))
% 60.06/60.14 [34]~E(x341,x342)+E(f9(x341,x343,x344),f9(x342,x343,x344))
% 60.06/60.14 [35]~E(x351,x352)+E(f9(x353,x351,x354),f9(x353,x352,x354))
% 60.06/60.14 [36]~E(x361,x362)+E(f9(x363,x364,x361),f9(x363,x364,x362))
% 60.06/60.14 [37]~E(x371,x372)+E(f10(x371,x373,x374),f10(x372,x373,x374))
% 60.06/60.14 [38]~E(x381,x382)+E(f10(x383,x381,x384),f10(x383,x382,x384))
% 60.06/60.14 [39]~E(x391,x392)+E(f10(x393,x394,x391),f10(x393,x394,x392))
% 60.06/60.14 [40]~E(x401,x402)+E(f26(x401,x403,x404,x405),f26(x402,x403,x404,x405))
% 60.06/60.14 [41]~E(x411,x412)+E(f26(x413,x411,x414,x415),f26(x413,x412,x414,x415))
% 60.06/60.14 [42]~E(x421,x422)+E(f26(x423,x424,x421,x425),f26(x423,x424,x422,x425))
% 60.06/60.14 [43]~E(x431,x432)+E(f26(x433,x434,x435,x431),f26(x433,x434,x435,x432))
% 60.06/60.14 [44]~E(x441,x442)+E(f15(x441,x443,x444,x445),f15(x442,x443,x444,x445))
% 60.06/60.14 [45]~E(x451,x452)+E(f15(x453,x451,x454,x455),f15(x453,x452,x454,x455))
% 60.06/60.14 [46]~E(x461,x462)+E(f15(x463,x464,x461,x465),f15(x463,x464,x462,x465))
% 60.06/60.14 [47]~E(x471,x472)+E(f15(x473,x474,x475,x471),f15(x473,x474,x475,x472))
% 60.06/60.14 [48]~E(x481,x482)+E(f13(x481,x483,x484,x485,x486),f13(x482,x483,x484,x485,x486))
% 60.06/60.14 [49]~E(x491,x492)+E(f13(x493,x491,x494,x495,x496),f13(x493,x492,x494,x495,x496))
% 60.06/60.14 [50]~E(x501,x502)+E(f13(x503,x504,x501,x505,x506),f13(x503,x504,x502,x505,x506))
% 60.06/60.14 [51]~E(x511,x512)+E(f13(x513,x514,x515,x511,x516),f13(x513,x514,x515,x512,x516))
% 60.06/60.14 [52]~E(x521,x522)+E(f13(x523,x524,x525,x526,x521),f13(x523,x524,x525,x526,x522))
% 60.06/60.14 [53]~E(x531,x532)+E(f12(x531,x533,x534,x535,x536,x537),f12(x532,x533,x534,x535,x536,x537))
% 60.06/60.14 [54]~E(x541,x542)+E(f12(x543,x541,x544,x545,x546,x547),f12(x543,x542,x544,x545,x546,x547))
% 60.06/60.14 [55]~E(x551,x552)+E(f12(x553,x554,x551,x555,x556,x557),f12(x553,x554,x552,x555,x556,x557))
% 60.06/60.14 [56]~E(x561,x562)+E(f12(x563,x564,x565,x561,x566,x567),f12(x563,x564,x565,x562,x566,x567))
% 60.06/60.14 [57]~E(x571,x572)+E(f12(x573,x574,x575,x576,x571,x577),f12(x573,x574,x575,x576,x572,x577))
% 60.06/60.14 [58]~E(x581,x582)+E(f12(x583,x584,x585,x586,x587,x581),f12(x583,x584,x585,x586,x587,x582))
% 60.06/60.14 [59]~E(x591,x592)+E(f30(x591,x593,x594,x595,x596),f30(x592,x593,x594,x595,x596))
% 60.06/60.14 [60]~E(x601,x602)+E(f30(x603,x601,x604,x605,x606),f30(x603,x602,x604,x605,x606))
% 60.06/60.14 [61]~E(x611,x612)+E(f30(x613,x614,x611,x615,x616),f30(x613,x614,x612,x615,x616))
% 60.06/60.14 [62]~E(x621,x622)+E(f30(x623,x624,x625,x621,x626),f30(x623,x624,x625,x622,x626))
% 60.06/60.14 [63]~E(x631,x632)+E(f30(x633,x634,x635,x636,x631),f30(x633,x634,x635,x636,x632))
% 60.06/60.14 [64]~E(x641,x642)+E(f11(x641,x643,x644,x645,x646,x647),f11(x642,x643,x644,x645,x646,x647))
% 60.06/60.14 [65]~E(x651,x652)+E(f11(x653,x651,x654,x655,x656,x657),f11(x653,x652,x654,x655,x656,x657))
% 60.06/60.14 [66]~E(x661,x662)+E(f11(x663,x664,x661,x665,x666,x667),f11(x663,x664,x662,x665,x666,x667))
% 60.06/60.14 [67]~E(x671,x672)+E(f11(x673,x674,x675,x671,x676,x677),f11(x673,x674,x675,x672,x676,x677))
% 60.06/60.14 [68]~E(x681,x682)+E(f11(x683,x684,x685,x686,x681,x687),f11(x683,x684,x685,x686,x682,x687))
% 60.06/60.14 [69]~E(x691,x692)+E(f11(x693,x694,x695,x696,x697,x691),f11(x693,x694,x695,x696,x697,x692))
% 60.06/60.14 [70]~E(x701,x702)+E(f31(x701,x703,x704,x705,x706,x707),f31(x702,x703,x704,x705,x706,x707))
% 60.06/60.14 [71]~E(x711,x712)+E(f31(x713,x711,x714,x715,x716,x717),f31(x713,x712,x714,x715,x716,x717))
% 60.06/60.14 [72]~E(x721,x722)+E(f31(x723,x724,x721,x725,x726,x727),f31(x723,x724,x722,x725,x726,x727))
% 60.06/60.14 [73]~E(x731,x732)+E(f31(x733,x734,x735,x731,x736,x737),f31(x733,x734,x735,x732,x736,x737))
% 60.06/60.14 [74]~E(x741,x742)+E(f31(x743,x744,x745,x746,x741,x747),f31(x743,x744,x745,x746,x742,x747))
% 60.06/60.14 [75]~E(x751,x752)+E(f31(x753,x754,x755,x756,x757,x751),f31(x753,x754,x755,x756,x757,x752))
% 60.06/60.14 [76]~E(x761,x762)+E(f28(x761,x763,x764,x765,x766,x767),f28(x762,x763,x764,x765,x766,x767))
% 60.06/60.14 [77]~E(x771,x772)+E(f28(x773,x771,x774,x775,x776,x777),f28(x773,x772,x774,x775,x776,x777))
% 60.06/60.14 [78]~E(x781,x782)+E(f28(x783,x784,x781,x785,x786,x787),f28(x783,x784,x782,x785,x786,x787))
% 60.06/60.14 [79]~E(x791,x792)+E(f28(x793,x794,x795,x791,x796,x797),f28(x793,x794,x795,x792,x796,x797))
% 60.06/60.14 [80]~E(x801,x802)+E(f28(x803,x804,x805,x806,x801,x807),f28(x803,x804,x805,x806,x802,x807))
% 60.06/60.14 [81]~E(x811,x812)+E(f28(x813,x814,x815,x816,x817,x811),f28(x813,x814,x815,x816,x817,x812))
% 60.06/60.14 [82]~E(x821,x822)+E(f14(x821,x823,x824,x825,x826,x827),f14(x822,x823,x824,x825,x826,x827))
% 60.06/60.14 [83]~E(x831,x832)+E(f14(x833,x831,x834,x835,x836,x837),f14(x833,x832,x834,x835,x836,x837))
% 60.06/60.14 [84]~E(x841,x842)+E(f14(x843,x844,x841,x845,x846,x847),f14(x843,x844,x842,x845,x846,x847))
% 60.06/60.14 [85]~E(x851,x852)+E(f14(x853,x854,x855,x851,x856,x857),f14(x853,x854,x855,x852,x856,x857))
% 60.06/60.14 [86]~E(x861,x862)+E(f14(x863,x864,x865,x866,x861,x867),f14(x863,x864,x865,x866,x862,x867))
% 60.06/60.14 [87]~E(x871,x872)+E(f14(x873,x874,x875,x876,x877,x871),f14(x873,x874,x875,x876,x877,x872))
% 60.06/60.14 [88]P1(x882,x883,x884)+~E(x881,x882)+~P1(x881,x883,x884)
% 60.06/60.14 [89]P1(x893,x892,x894)+~E(x891,x892)+~P1(x893,x891,x894)
% 60.06/60.14 [90]P1(x903,x904,x902)+~E(x901,x902)+~P1(x903,x904,x901)
% 60.06/60.14 [91]P7(x912,x913,x914,x915,x916,x917,x918,x919)+~E(x911,x912)+~P7(x911,x913,x914,x915,x916,x917,x918,x919)
% 60.06/60.14 [92]P7(x923,x922,x924,x925,x926,x927,x928,x929)+~E(x921,x922)+~P7(x923,x921,x924,x925,x926,x927,x928,x929)
% 60.06/60.14 [93]P7(x933,x934,x932,x935,x936,x937,x938,x939)+~E(x931,x932)+~P7(x933,x934,x931,x935,x936,x937,x938,x939)
% 60.06/60.14 [94]P7(x943,x944,x945,x942,x946,x947,x948,x949)+~E(x941,x942)+~P7(x943,x944,x945,x941,x946,x947,x948,x949)
% 60.06/60.14 [95]P7(x953,x954,x955,x956,x952,x957,x958,x959)+~E(x951,x952)+~P7(x953,x954,x955,x956,x951,x957,x958,x959)
% 60.06/60.14 [96]P7(x963,x964,x965,x966,x967,x962,x968,x969)+~E(x961,x962)+~P7(x963,x964,x965,x966,x967,x961,x968,x969)
% 60.06/60.14 [97]P7(x973,x974,x975,x976,x977,x978,x972,x979)+~E(x971,x972)+~P7(x973,x974,x975,x976,x977,x978,x971,x979)
% 60.06/60.14 [98]P7(x983,x984,x985,x986,x987,x988,x989,x982)+~E(x981,x982)+~P7(x983,x984,x985,x986,x987,x988,x989,x981)
% 60.06/60.14 [99]P4(x992,x993,x994,x995)+~E(x991,x992)+~P4(x991,x993,x994,x995)
% 60.06/60.14 [100]P4(x1003,x1002,x1004,x1005)+~E(x1001,x1002)+~P4(x1003,x1001,x1004,x1005)
% 60.06/60.14 [101]P4(x1013,x1014,x1012,x1015)+~E(x1011,x1012)+~P4(x1013,x1014,x1011,x1015)
% 60.06/60.14 [102]P4(x1023,x1024,x1025,x1022)+~E(x1021,x1022)+~P4(x1023,x1024,x1025,x1021)
% 60.06/60.14 [103]P3(x1032,x1033,x1034)+~E(x1031,x1032)+~P3(x1031,x1033,x1034)
% 60.06/60.14 [104]P3(x1043,x1042,x1044)+~E(x1041,x1042)+~P3(x1043,x1041,x1044)
% 60.06/60.14 [105]P3(x1053,x1054,x1052)+~E(x1051,x1052)+~P3(x1053,x1054,x1051)
% 60.06/60.14 [106]P9(x1062,x1063,x1064,x1065)+~E(x1061,x1062)+~P9(x1061,x1063,x1064,x1065)
% 60.06/60.14 [107]P9(x1073,x1072,x1074,x1075)+~E(x1071,x1072)+~P9(x1073,x1071,x1074,x1075)
% 60.06/60.14 [108]P9(x1083,x1084,x1082,x1085)+~E(x1081,x1082)+~P9(x1083,x1084,x1081,x1085)
% 60.06/60.14 [109]P9(x1093,x1094,x1095,x1092)+~E(x1091,x1092)+~P9(x1093,x1094,x1095,x1091)
% 60.06/60.14 [110]P2(x1102,x1103,x1104,x1105)+~E(x1101,x1102)+~P2(x1101,x1103,x1104,x1105)
% 60.06/60.14 [111]P2(x1113,x1112,x1114,x1115)+~E(x1111,x1112)+~P2(x1113,x1111,x1114,x1115)
% 60.06/60.14 [112]P2(x1123,x1124,x1122,x1125)+~E(x1121,x1122)+~P2(x1123,x1124,x1121,x1125)
% 60.06/60.14 [113]P2(x1133,x1134,x1135,x1132)+~E(x1131,x1132)+~P2(x1133,x1134,x1135,x1131)
% 60.06/60.14 [114]P8(x1142,x1143,x1144,x1145,x1146,x1147,x1148,x1149)+~E(x1141,x1142)+~P8(x1141,x1143,x1144,x1145,x1146,x1147,x1148,x1149)
% 60.06/60.14 [115]P8(x1153,x1152,x1154,x1155,x1156,x1157,x1158,x1159)+~E(x1151,x1152)+~P8(x1153,x1151,x1154,x1155,x1156,x1157,x1158,x1159)
% 60.06/60.14 [116]P8(x1163,x1164,x1162,x1165,x1166,x1167,x1168,x1169)+~E(x1161,x1162)+~P8(x1163,x1164,x1161,x1165,x1166,x1167,x1168,x1169)
% 60.06/60.14 [117]P8(x1173,x1174,x1175,x1172,x1176,x1177,x1178,x1179)+~E(x1171,x1172)+~P8(x1173,x1174,x1175,x1171,x1176,x1177,x1178,x1179)
% 60.06/60.14 [118]P8(x1183,x1184,x1185,x1186,x1182,x1187,x1188,x1189)+~E(x1181,x1182)+~P8(x1183,x1184,x1185,x1186,x1181,x1187,x1188,x1189)
% 60.06/60.14 [119]P8(x1193,x1194,x1195,x1196,x1197,x1192,x1198,x1199)+~E(x1191,x1192)+~P8(x1193,x1194,x1195,x1196,x1197,x1191,x1198,x1199)
% 60.06/60.14 [120]P8(x1203,x1204,x1205,x1206,x1207,x1208,x1202,x1209)+~E(x1201,x1202)+~P8(x1203,x1204,x1205,x1206,x1207,x1208,x1201,x1209)
% 60.06/60.14 [121]P8(x1213,x1214,x1215,x1216,x1217,x1218,x1219,x1212)+~E(x1211,x1212)+~P8(x1213,x1214,x1215,x1216,x1217,x1218,x1219,x1211)
% 60.06/60.14 [122]P10(x1222,x1223,x1224,x1225)+~E(x1221,x1222)+~P10(x1221,x1223,x1224,x1225)
% 60.06/60.14 [123]P10(x1233,x1232,x1234,x1235)+~E(x1231,x1232)+~P10(x1233,x1231,x1234,x1235)
% 60.06/60.14 [124]P10(x1243,x1244,x1242,x1245)+~E(x1241,x1242)+~P10(x1243,x1244,x1241,x1245)
% 60.06/60.14 [125]P10(x1253,x1254,x1255,x1252)+~E(x1251,x1252)+~P10(x1253,x1254,x1255,x1251)
% 60.06/60.14 [126]P5(x1262,x1263,x1264,x1265)+~E(x1261,x1262)+~P5(x1261,x1263,x1264,x1265)
% 60.06/60.14 [127]P5(x1273,x1272,x1274,x1275)+~E(x1271,x1272)+~P5(x1273,x1271,x1274,x1275)
% 60.06/60.14 [128]P5(x1283,x1284,x1282,x1285)+~E(x1281,x1282)+~P5(x1283,x1284,x1281,x1285)
% 60.06/60.14 [129]P5(x1293,x1294,x1295,x1292)+~E(x1291,x1292)+~P5(x1293,x1294,x1295,x1291)
% 60.06/60.14 [130]P6(x1302,x1303,x1304,x1305,x1306,x1307)+~E(x1301,x1302)+~P6(x1301,x1303,x1304,x1305,x1306,x1307)
% 60.06/60.14 [131]P6(x1313,x1312,x1314,x1315,x1316,x1317)+~E(x1311,x1312)+~P6(x1313,x1311,x1314,x1315,x1316,x1317)
% 60.06/60.14 [132]P6(x1323,x1324,x1322,x1325,x1326,x1327)+~E(x1321,x1322)+~P6(x1323,x1324,x1321,x1325,x1326,x1327)
% 60.06/60.14 [133]P6(x1333,x1334,x1335,x1332,x1336,x1337)+~E(x1331,x1332)+~P6(x1333,x1334,x1335,x1331,x1336,x1337)
% 60.06/60.14 [134]P6(x1343,x1344,x1345,x1346,x1342,x1347)+~E(x1341,x1342)+~P6(x1343,x1344,x1345,x1346,x1341,x1347)
% 60.06/60.14 [135]P6(x1353,x1354,x1355,x1356,x1357,x1352)+~E(x1351,x1352)+~P6(x1353,x1354,x1355,x1356,x1357,x1351)
% 60.06/60.14 [136]P11(x1362,x1363,x1364,x1365,x1366,x1367)+~E(x1361,x1362)+~P11(x1361,x1363,x1364,x1365,x1366,x1367)
% 60.06/60.14 [137]P11(x1373,x1372,x1374,x1375,x1376,x1377)+~E(x1371,x1372)+~P11(x1373,x1371,x1374,x1375,x1376,x1377)
% 60.06/60.14 [138]P11(x1383,x1384,x1382,x1385,x1386,x1387)+~E(x1381,x1382)+~P11(x1383,x1384,x1381,x1385,x1386,x1387)
% 60.06/60.14 [139]P11(x1393,x1394,x1395,x1392,x1396,x1397)+~E(x1391,x1392)+~P11(x1393,x1394,x1395,x1391,x1396,x1397)
% 60.06/60.14 [140]P11(x1403,x1404,x1405,x1406,x1402,x1407)+~E(x1401,x1402)+~P11(x1403,x1404,x1405,x1406,x1401,x1407)
% 60.06/60.14 [141]P11(x1413,x1414,x1415,x1416,x1417,x1412)+~E(x1411,x1412)+~P11(x1413,x1414,x1415,x1416,x1417,x1411)
% 60.06/60.14
% 60.06/60.14 %-------------------------------------------
% 60.06/60.15 cnf(264,plain,
% 60.06/60.15 (~P4(a16,a2,a17,a19)),
% 60.06/60.15 inference(scs_inference,[],[150,169])).
% 60.06/60.15 cnf(266,plain,
% 60.06/60.15 (~P4(a2,a17,a16,a19)),
% 60.06/60.15 inference(scs_inference,[],[150,169,170])).
% 60.06/60.15 cnf(268,plain,
% 60.06/60.15 (~P4(a2,a16,a19,a17)),
% 60.06/60.15 inference(scs_inference,[],[150,169,170,171])).
% 60.06/60.15 cnf(270,plain,
% 60.06/60.15 (P1(a16,a16,a1)),
% 60.06/60.15 inference(scs_inference,[],[142,150,169,170,171,155])).
% 60.06/60.15 cnf(272,plain,
% 60.06/60.15 (P10(a3,a3,a1,a1)),
% 60.06/60.15 inference(scs_inference,[],[142,145,150,169,170,171,155,157])).
% 60.06/60.15 cnf(274,plain,
% 60.06/60.15 (P10(a18,a18,a1,a1)),
% 60.06/60.15 inference(scs_inference,[],[142,145,150,169,170,171,155,157,158])).
% 60.06/60.15 cnf(295,plain,
% 60.06/60.15 (~P4(a16,a2,a19,a17)),
% 60.06/60.15 inference(scs_inference,[],[264,171])).
% 60.06/60.15 cnf(297,plain,
% 60.06/60.15 (~P4(a17,a2,a16,a19)),
% 60.06/60.15 inference(scs_inference,[],[264,266,171,169])).
% 60.06/60.15 cnf(299,plain,
% 60.06/60.15 (~P4(a16,a17,a2,a19)),
% 60.06/60.15 inference(scs_inference,[],[264,266,171,169,170])).
% 60.06/60.15 cnf(301,plain,
% 60.06/60.15 (P1(a2,a2,a17)),
% 60.06/60.15 inference(scs_inference,[],[143,264,266,171,169,170,155])).
% 60.06/60.15 cnf(315,plain,
% 60.06/60.15 (~P4(a17,a2,a19,a16)),
% 60.06/60.15 inference(scs_inference,[],[297,171])).
% 60.06/60.15 cnf(317,plain,
% 60.06/60.15 (~P4(a2,a19,a16,a17)),
% 60.06/60.15 inference(scs_inference,[],[268,297,171,170])).
% 60.06/60.15 cnf(319,plain,
% 60.06/60.15 (~P4(a17,a16,a2,a19)),
% 60.06/60.15 inference(scs_inference,[],[268,297,299,171,170,169])).
% 60.06/60.15 cnf(321,plain,
% 60.06/60.15 (P1(a16,a16,a19)),
% 60.06/60.15 inference(scs_inference,[],[144,268,297,299,171,170,169,155])).
% 60.06/60.15 cnf(329,plain,
% 60.06/60.15 (~P4(a2,a19,a17,a16)),
% 60.06/60.15 inference(scs_inference,[],[317,171])).
% 60.06/60.15 cnf(331,plain,
% 60.06/60.15 (~P4(a2,a17,a19,a16)),
% 60.06/60.15 inference(scs_inference,[],[315,317,171,169])).
% 60.06/60.15 cnf(333,plain,
% 60.06/60.15 (~P4(a16,a19,a2,a17)),
% 60.06/60.15 inference(scs_inference,[],[295,315,317,171,169,170])).
% 60.06/60.15 cnf(342,plain,
% 60.06/60.15 (~P10(x3421,x3422,a3,a3)+P10(x3421,x3422,a1,a1)),
% 60.06/60.15 inference(scs_inference,[],[148,146,270,272,295,315,317,171,169,170,155,109,110,111,112,113,179])).
% 60.06/60.15 cnf(349,plain,
% 60.06/60.15 (~P4(a17,a16,a19,a2)),
% 60.06/60.15 inference(scs_inference,[],[319,171])).
% 60.06/60.15 cnf(353,plain,
% 60.06/60.15 (~P4(a19,a2,a17,a16)),
% 60.06/60.15 inference(scs_inference,[],[319,329,315,171,170,169])).
% 60.06/60.15 cnf(361,plain,
% 60.06/60.15 (~P9(a1,a1,x3611,x3612)+P9(a18,a18,x3611,x3612)),
% 60.06/60.15 inference(scs_inference,[],[274,301,319,329,272,315,171,170,169,155,122,123,124,125,182])).
% 60.06/60.15 cnf(370,plain,
% 60.06/60.15 (~P4(a16,a19,a17,a2)),
% 60.06/60.15 inference(scs_inference,[],[333,171])).
% 60.06/60.15 cnf(372,plain,
% 60.06/60.15 (~P4(a19,a16,a2,a17)),
% 60.06/60.15 inference(scs_inference,[],[333,171,169])).
% 60.06/60.15 cnf(391,plain,
% 60.06/60.15 (~P4(a19,a2,a16,a17)),
% 60.06/60.15 inference(scs_inference,[],[353,171])).
% 60.06/60.15 cnf(393,plain,
% 60.06/60.15 (~P4(a19,a17,a2,a16)),
% 60.06/60.15 inference(scs_inference,[],[353,171,170])).
% 60.06/60.15 cnf(397,plain,
% 60.06/60.15 (~P9(x3971,x3972,a1,a3)+P10(x3971,x3972,a2,a16)),
% 60.06/60.15 inference(scs_inference,[],[146,353,370,171,170,169,180])).
% 60.06/60.15 cnf(418,plain,
% 60.06/60.15 (~P4(a16,a17,a19,a2)),
% 60.06/60.15 inference(scs_inference,[],[393,349,171,169])).
% 60.06/60.15 cnf(420,plain,
% 60.06/60.15 (~P10(x4201,x4202,a18,a18)+P10(x4201,x4202,a1,a1)),
% 60.06/60.15 inference(scs_inference,[],[274,393,349,171,169,179])).
% 60.06/60.15 cnf(558,plain,
% 60.06/60.15 (~P9(a1,a1,x5581,x5582)+P9(a3,a3,x5581,x5582)),
% 60.06/60.15 inference(scs_inference,[],[272,182])).
% 60.06/60.15 cnf(752,plain,
% 60.06/60.15 (P1(a19,a1,a16)),
% 60.06/60.15 inference(scs_inference,[],[321,270,88,155])).
% 60.06/60.15 cnf(772,plain,
% 60.06/60.15 (P7(x7721,a18,a18,a1,x7721,a18,a18,a1)+~P1(x7721,a18,a1)),
% 60.06/60.15 inference(scs_inference,[],[274,317,752,90,236,89,88,228])).
% 60.06/60.15 cnf(932,plain,
% 60.06/60.15 (P7(x9321,a3,a3,a1,x9321,a3,a3,a1)+~P1(x9321,a3,a1)),
% 60.06/60.15 inference(scs_inference,[],[272,228])).
% 60.06/60.15 cnf(970,plain,
% 60.06/60.15 (P1(a2,a16,a1)),
% 60.06/60.15 inference(scs_inference,[],[142,151,152])).
% 60.06/60.15 cnf(971,plain,
% 60.06/60.15 (P1(a1,a1,a2)),
% 60.06/60.15 inference(scs_inference,[],[970,155])).
% 60.06/60.15 cnf(1130,plain,
% 60.06/60.15 (P5(a18,a1,a18,a3)),
% 60.06/60.15 inference(scs_inference,[],[145,154,156])).
% 60.06/60.15 cnf(1131,plain,
% 60.06/60.15 (P4(a1,a3,a3,a3)),
% 60.06/60.15 inference(scs_inference,[],[1130,196])).
% 60.06/60.15 cnf(1135,plain,
% 60.06/60.15 (P4(a3,a3,a3,a3)),
% 60.06/60.15 inference(scs_inference,[],[1130,196,161,185])).
% 60.06/60.15 cnf(1137,plain,
% 60.06/60.15 (~P1(a18,a1,a3)+P10(a1,a1,a3,a3)),
% 60.06/60.15 inference(scs_inference,[],[1130,196,161,185,157])).
% 60.06/60.15 cnf(1154,plain,
% 60.06/60.15 (~P5(x11541,x11542,a18,a1)+P5(x11541,x11542,a18,a3)),
% 60.06/60.15 inference(scs_inference,[],[1130,183])).
% 60.06/60.15 cnf(1333,plain,
% 60.06/60.15 (P1(x13331,x13332,x13333)+~P10(x13332,x13331,x13332,x13333)),
% 60.06/60.15 inference(scs_inference,[],[160,151])).
% 60.06/60.15 cnf(1365,plain,
% 60.06/60.15 (~P1(a18,a3,a1)+P10(a1,a1,a3,a3)),
% 60.06/60.15 inference(scs_inference,[],[1137,152])).
% 60.06/60.15 cnf(1397,plain,
% 60.06/60.15 (P1(x13971,x13972,x13973)+~P10(x13972,x13971,x13973,x13972)),
% 60.06/60.15 inference(scs_inference,[],[1333,164])).
% 60.06/60.15 cnf(1429,plain,
% 60.06/60.15 (P10(a1,a1,a3,a3)),
% 60.06/60.15 inference(scs_inference,[],[145,1365,153])).
% 60.06/60.15 cnf(1430,plain,
% 60.06/60.15 (P10(a1,a1,a1,a1)),
% 60.06/60.15 inference(scs_inference,[],[272,1429,179])).
% 60.06/60.15 cnf(1432,plain,
% 60.06/60.15 (P1(a1,a1,a1)),
% 60.06/60.15 inference(scs_inference,[],[272,1429,179,1333])).
% 60.06/60.15 cnf(1435,plain,
% 60.06/60.15 (P1(a2,x14351,a1)+~E(a1,x14351)),
% 60.06/60.15 inference(scs_inference,[],[272,971,1429,179,1333,90,155])).
% 60.06/60.15 cnf(1441,plain,
% 60.06/60.15 (P1(a2,a1,a1)),
% 60.06/60.15 inference(equality_inference,[],[1435])).
% 60.06/60.15 cnf(1442,plain,
% 60.06/60.15 (P10(a18,a18,a3,a3)),
% 60.06/60.15 inference(scs_inference,[],[274,1429,179])).
% 60.06/60.15 cnf(1458,plain,
% 60.06/60.15 (P7(a2,a1,a1,a1,a2,a1,a1,a1)),
% 60.06/60.15 inference(scs_inference,[],[1441,1430,228])).
% 60.06/60.15 cnf(1478,plain,
% 60.06/60.15 (~P10(x14781,x14782,a18,a18)+P10(x14781,x14782,a3,a3)),
% 60.06/60.15 inference(scs_inference,[],[1441,1442,88,179])).
% 60.06/60.16 cnf(1504,plain,
% 60.06/60.16 (~P9(a3,a3,x15041,x15042)+P9(a1,a1,x15041,x15042)),
% 60.06/60.16 inference(scs_inference,[],[1429,182])).
% 60.06/60.16 cnf(1531,plain,
% 60.06/60.16 (~P9(a3,a3,x15311,x15312)+P9(a18,a18,x15311,x15312)),
% 60.06/60.16 inference(scs_inference,[],[1442,182])).
% 60.06/60.16 cnf(1574,plain,
% 60.06/60.16 (P7(x15741,a1,a1,a3,x15741,a1,a1,a3)+~P1(x15741,a1,a3)),
% 60.06/60.16 inference(scs_inference,[],[1429,228])).
% 60.06/60.16 cnf(1577,plain,
% 60.06/60.16 (P7(x15771,a18,a18,a3,x15771,a18,a18,a3)+~P1(x15771,a18,a3)),
% 60.06/60.16 inference(scs_inference,[],[1442,228])).
% 60.06/60.16 cnf(1782,plain,
% 60.06/60.16 (P5(a18,a3,a1,a18)),
% 60.06/60.16 inference(scs_inference,[],[1130,167,168])).
% 60.06/60.16 cnf(1783,plain,
% 60.06/60.16 (P5(a18,a1,a1,a18)),
% 60.06/60.16 inference(scs_inference,[],[1130,1782,183])).
% 60.06/60.16 cnf(1855,plain,
% 60.06/60.16 (P10(a3,a3,a3,a3)),
% 60.06/60.16 inference(scs_inference,[],[272,1429,179])).
% 60.06/60.16 cnf(1857,plain,
% 60.06/60.16 (P8(a3,a3,a3,a3,a3,a3,a3,a3)),
% 60.06/60.16 inference(scs_inference,[],[272,1429,1135,179,230])).
% 60.06/60.16 cnf(1859,plain,
% 60.06/60.16 (P1(a3,a3,a3)),
% 60.06/60.16 inference(scs_inference,[],[272,1429,1135,179,230,1397])).
% 60.06/60.16 cnf(1862,plain,
% 60.06/60.16 (P7(a3,a3,a3,a3,a3,a3,a3,a3)),
% 60.06/60.16 inference(scs_inference,[],[272,1429,1135,179,230,1397,121,228])).
% 60.06/60.16 cnf(1913,plain,
% 60.06/60.16 (~P5(a1,x19131,a1,x19131)+~P5(a1,x19132,a1,x19132)+P9(a3,a3,x19132,x19131)+~E(a3,x19133)),
% 60.06/60.16 inference(scs_inference,[],[148,272,1862,1857,97,182,181])).
% 60.06/60.16 cnf(1915,plain,
% 60.06/60.16 (P9(a3,a3,x19151,x19152)+~P5(a1,x19152,a1,x19152)+~P5(a1,x19151,a1,x19151)),
% 60.06/60.16 inference(equality_inference,[],[1913])).
% 60.06/60.16 cnf(2039,plain,
% 60.06/60.16 (P8(a1,a1,x20391,x20392,a1,a1,x20391,x20392)),
% 60.06/60.16 inference(scs_inference,[],[1429,342,225])).
% 60.06/60.16 cnf(2383,plain,
% 60.06/60.16 (P5(a18,a3,a18,a3)),
% 60.06/60.16 inference(scs_inference,[],[145,1154,156])).
% 60.06/60.16 cnf(2385,plain,
% 60.06/60.16 (P3(a18,a3,a3)+~P1(a18,a3,a3)),
% 60.06/60.16 inference(scs_inference,[],[2383,128,161])).
% 60.06/60.16 cnf(4661,plain,
% 60.06/60.16 (P1(a2,a1,a16)),
% 60.06/60.16 inference(scs_inference,[],[142,151])).
% 60.06/60.16 cnf(4663,plain,
% 60.06/60.16 (P1(a1,a16,a2)),
% 60.06/60.16 inference(scs_inference,[],[142,151,152])).
% 60.06/60.16 cnf(4665,plain,
% 60.06/60.16 (P1(a18,a3,a1)),
% 60.06/60.16 inference(scs_inference,[],[142,145,151,152,153])).
% 60.06/60.16 cnf(4667,plain,
% 60.06/60.16 (P3(a18,a1,a3)),
% 60.06/60.16 inference(scs_inference,[],[142,145,151,152,153,154])).
% 60.06/60.16 cnf(4669,plain,
% 60.06/60.16 (P5(a18,a3,a18,a1)),
% 60.06/60.16 inference(scs_inference,[],[142,145,151,152,153,154,156])).
% 60.06/60.16 cnf(4671,plain,
% 60.06/60.16 (P10(a3,a3,a18,a18)),
% 60.06/60.16 inference(scs_inference,[],[142,1442,145,151,152,153,154,156,163])).
% 60.06/60.16 cnf(4675,plain,
% 60.06/60.16 (P5(a18,a1,a18,a1)),
% 60.06/60.16 inference(scs_inference,[],[142,1783,1442,145,151,152,153,154,156,163,167,168])).
% 60.06/60.16 cnf(4677,plain,
% 60.06/60.16 (P8(a18,a3,a3,a3,a3,a3,a18,a3)),
% 60.06/60.16 inference(scs_inference,[],[142,1783,2383,1442,145,151,152,153,154,156,163,167,168,226])).
% 60.06/60.16 cnf(4679,plain,
% 60.06/60.16 (P5(a1,a18,a18,a3)),
% 60.06/60.16 inference(scs_inference,[],[142,1783,2383,1442,145,151,152,153,154,156,163,167,168,226,1154])).
% 60.06/60.16 cnf(4685,plain,
% 60.06/60.16 (P7(a1,a2,a1,a1,a2,a1,a1,a1)),
% 60.06/60.16 inference(scs_inference,[],[142,1783,2383,1458,1442,148,145,151,152,153,154,156,163,167,168,226,1154,187,257,258])).
% 60.06/60.16 cnf(4687,plain,
% 60.06/60.16 (P7(a2,a1,a2,a1,a1,a1,a1,a1)),
% 60.06/60.16 inference(scs_inference,[],[142,1783,2383,1458,1442,148,145,151,152,153,154,156,163,167,168,226,1154,187,257,258,259])).
% 60.06/60.16 cnf(4689,plain,
% 60.06/60.16 (P8(x46891,x46892,a1,a1,x46891,x46892,a1,a1)),
% 60.06/60.16 inference(scs_inference,[],[142,1783,2383,1458,1442,148,2039,145,151,152,153,154,156,163,167,168,226,1154,187,257,258,259,253])).
% 60.06/60.16 cnf(4691,plain,
% 60.06/60.16 (P8(a3,a3,a18,a3,a18,a3,a3,a3)),
% 60.06/60.16 inference(scs_inference,[],[142,1783,2383,1458,1442,148,2039,145,151,152,153,154,156,163,167,168,226,1154,187,257,258,259,253,252])).
% 60.06/60.16 cnf(4693,plain,
% 60.06/60.16 (P8(a18,a18,x46931,x46932,a3,a3,x46931,x46932)),
% 60.06/60.16 inference(scs_inference,[],[142,1783,2383,1458,1442,148,2039,145,151,152,153,154,156,163,167,168,226,1154,187,257,258,259,253,252,225])).
% 60.06/60.16 cnf(4695,plain,
% 60.06/60.16 (P10(x46951,x46952,x46951,x46952)),
% 60.06/60.16 inference(scs_inference,[],[142,1783,2383,1458,1442,148,2039,145,151,152,153,154,156,163,167,168,226,1154,187,257,258,259,253,252,225,233])).
% 60.06/60.16 cnf(4697,plain,
% 60.06/60.16 (P8(a3,a18,a3,a3,a3,a3,a18,a3)),
% 60.06/60.16 inference(scs_inference,[],[142,1783,2383,1458,1442,148,2039,145,151,152,153,154,156,163,167,168,226,1154,187,257,258,259,253,252,225,233,254])).
% 60.06/60.16 cnf(4701,plain,
% 60.06/60.16 (P9(a1,a3,a16,a2)),
% 60.06/60.16 inference(scs_inference,[],[142,1783,2383,1458,1442,148,2039,1131,145,146,151,152,153,154,156,163,167,168,226,1154,187,257,258,259,253,252,225,233,254,169,166])).
% 60.06/60.16 cnf(4705,plain,
% 60.06/60.16 (P9(a2,a16,a1,a3)),
% 60.06/60.16 inference(scs_inference,[],[142,1783,2383,1458,1442,148,2039,1131,145,146,151,152,153,154,156,163,167,168,226,1154,187,257,258,259,253,252,225,233,254,169,166,224,165])).
% 60.06/60.16 cnf(4709,plain,
% 60.06/60.16 (P2(a18,a3,a3,a3)),
% 60.06/60.16 inference(scs_inference,[],[142,1783,2383,1458,1442,148,2039,1131,145,146,151,152,153,154,156,163,167,168,226,1154,187,257,258,259,253,252,225,233,254,169,166,224,165,255,184])).
% 60.06/60.16 cnf(4711,plain,
% 60.06/60.16 (P7(a18,a1,a1,a3,a18,a1,a1,a3)),
% 60.06/60.16 inference(scs_inference,[],[142,1783,2383,1458,1442,148,2039,1131,145,146,151,152,153,154,156,163,167,168,226,1154,187,257,258,259,253,252,225,233,254,169,166,224,165,255,184,223])).
% 60.06/60.16 cnf(4713,plain,
% 60.06/60.16 (P3(f28(a3,a1,a3,a1,a18,a18),a3,a1)),
% 60.06/60.16 inference(scs_inference,[],[142,1783,2383,1458,1442,148,2039,1131,145,146,151,152,153,154,156,163,167,168,226,1154,187,257,258,259,253,252,225,233,254,169,166,224,165,255,184,223,203])).
% 60.06/60.16 cnf(4717,plain,
% 60.06/60.16 (P10(f28(a3,a1,a3,a1,a18,a18),a18,a1,a1)),
% 60.06/60.16 inference(scs_inference,[],[142,1783,2383,1458,1442,148,2039,1131,145,146,151,152,153,154,156,163,167,168,226,1154,187,257,258,259,253,252,225,233,254,169,166,224,165,255,184,223,203,204,205])).
% 60.06/60.16 cnf(4721,plain,
% 60.06/60.16 (P9(a18,a18,a3,a3)),
% 60.06/60.16 inference(scs_inference,[],[142,1783,2383,1458,1442,148,2039,1131,145,146,151,152,153,154,156,163,167,168,226,1154,187,257,258,259,253,252,225,233,254,169,166,224,165,255,184,223,203,204,205,262,181])).
% 60.06/60.16 cnf(4723,plain,
% 60.06/60.16 (P1(a16,a16,a2)),
% 60.06/60.16 inference(scs_inference,[],[142,1783,2383,1458,1442,148,2039,1131,145,146,151,152,153,154,156,163,167,168,226,1154,187,257,258,259,253,252,225,233,254,169,166,224,165,255,184,223,203,204,205,262,181,155])).
% 60.06/60.16 cnf(4725,plain,
% 60.06/60.16 (P9(a18,a3,a3,a3)),
% 60.06/60.16 inference(scs_inference,[],[142,1783,2383,1458,1442,148,2039,1131,145,146,1857,151,152,153,154,156,163,167,168,226,1154,187,257,258,259,253,252,225,233,254,169,166,224,165,255,184,223,203,204,205,262,181,155,242])).
% 60.06/60.16 cnf(4727,plain,
% 60.06/60.16 (P9(a3,a3,a3,a3)),
% 60.06/60.16 inference(scs_inference,[],[142,1783,2383,1458,1442,148,2039,1131,145,146,1857,151,152,153,154,156,163,167,168,226,1154,187,257,258,259,253,252,225,233,254,169,166,224,165,255,184,223,203,204,205,262,181,155,242,182])).
% 60.06/60.16 cnf(4731,plain,
% 60.06/60.16 (P4(a1,a1,a1,a1)),
% 60.06/60.16 inference(scs_inference,[],[142,1432,1783,2383,1458,1442,148,2039,1131,145,146,1857,151,152,153,154,156,163,167,168,226,1154,187,257,258,259,253,252,225,233,254,169,166,224,165,255,184,223,203,204,205,262,181,155,242,182,158,236])).
% 60.06/60.16 cnf(4734,plain,
% 60.06/60.16 (P5(a1,a18,a1,a18)),
% 60.06/60.16 inference(scs_inference,[],[142,1432,1783,2383,1458,1442,148,2039,1131,145,146,1857,151,152,153,154,156,163,167,168,226,1154,187,257,258,259,253,252,225,233,254,169,166,224,165,255,184,223,203,204,205,262,181,155,242,182,158,236,183])).
% 60.06/60.16 cnf(4736,plain,
% 60.06/60.16 (P4(a3,a1,a1,a1)),
% 60.06/60.16 inference(scs_inference,[],[142,1432,1783,2383,1458,1442,148,2039,1131,145,146,1857,151,152,153,154,156,163,167,168,226,1154,187,257,258,259,253,252,225,233,254,169,166,224,165,255,184,223,203,204,205,262,181,155,242,182,158,236,183,196])).
% 60.06/60.16 cnf(4742,plain,
% 60.06/60.16 (P5(a3,a3,a3,a3)),
% 60.06/60.16 inference(scs_inference,[],[142,1432,1783,2383,1458,1442,1430,1135,148,2039,1131,145,146,1857,151,152,153,154,156,163,167,168,226,1154,187,257,258,259,253,252,225,233,254,169,166,224,165,255,184,223,203,204,205,262,181,155,242,182,158,236,183,196,206,207,251])).
% 60.06/60.16 cnf(4744,plain,
% 60.06/60.16 (P9(a1,a1,a3,a3)),
% 60.06/60.16 inference(scs_inference,[],[142,1432,1783,2383,1458,1442,1430,1135,148,2039,1131,145,146,1857,151,152,153,154,156,163,167,168,226,1154,187,257,258,259,253,252,225,233,254,169,166,224,165,255,184,223,203,204,205,262,181,155,242,182,158,236,183,196,206,207,251,1504])).
% 60.06/60.16 cnf(4746,plain,
% 60.06/60.16 (P7(a2,a1,a1,a1,a1,a2,a1,a1)),
% 60.06/60.16 inference(scs_inference,[],[142,1432,1783,2383,1458,1442,1430,1135,148,2039,1131,145,146,1857,151,152,153,154,156,163,167,168,226,1154,187,257,258,259,253,252,225,233,254,169,166,224,165,255,184,223,203,204,205,262,181,155,242,182,158,236,183,196,206,207,251,1504,256])).
% 60.06/60.16 cnf(4748,plain,
% 60.06/60.16 (P4(a3,a3,a1,a3)),
% 60.06/60.16 inference(scs_inference,[],[142,1432,1783,2383,1458,1442,1430,1135,148,2039,1131,145,146,1857,151,152,153,154,156,163,167,168,226,1154,187,257,258,259,253,252,225,233,254,169,166,224,165,255,184,223,203,204,205,262,181,155,242,182,158,236,183,196,206,207,251,1504,256,170])).
% 60.06/60.16 cnf(4750,plain,
% 60.06/60.16 (P4(a3,a3,a3,a1)),
% 60.06/60.16 inference(scs_inference,[],[142,1432,1783,2383,1458,1442,1430,1135,148,2039,1131,145,146,1857,151,152,153,154,156,163,167,168,226,1154,187,257,258,259,253,252,225,233,254,169,166,224,165,255,184,223,203,204,205,262,181,155,242,182,158,236,183,196,206,207,251,1504,256,170,171])).
% 60.06/60.16 cnf(4758,plain,
% 60.06/60.16 (P5(a3,a3,a3,f4(a3,a3,a3))),
% 60.06/60.16 inference(scs_inference,[],[142,1432,1783,2383,1458,1442,1430,1135,148,2039,1131,145,146,1857,151,152,153,154,156,163,167,168,226,1154,187,257,258,259,253,252,225,233,254,169,166,224,165,255,184,223,203,204,205,262,181,155,242,182,158,236,183,196,206,207,251,1504,256,170,171,173,176,178,188])).
% 60.06/60.16 cnf(4760,plain,
% 60.06/60.16 (P2(f9(a3,a3,a3),a3,a3,a3)),
% 60.06/60.16 inference(scs_inference,[],[142,1432,1783,2383,1458,1442,1430,1135,148,2039,1131,145,146,1857,151,152,153,154,156,163,167,168,226,1154,187,257,258,259,253,252,225,233,254,169,166,224,165,255,184,223,203,204,205,262,181,155,242,182,158,236,183,196,206,207,251,1504,256,170,171,173,176,178,188,191])).
% 60.06/60.16 cnf(4768,plain,
% 60.06/60.16 (P9(f13(a18,a3,a3,a3,a3),a18,a3,a3)),
% 60.06/60.16 inference(scs_inference,[],[142,1432,1859,1783,2383,1458,1442,1430,1135,148,2039,1131,145,146,1857,151,152,153,154,156,163,167,168,226,1154,187,257,258,259,253,252,225,233,254,169,166,224,165,255,184,223,203,204,205,262,181,155,242,182,158,236,183,196,206,207,251,1504,256,170,171,173,176,178,188,191,193,194,197,198])).
% 60.06/60.16 cnf(4770,plain,
% 60.06/60.16 (P5(a3,a3,a3,f30(a18,a3,a3,a3,a3))),
% 60.06/60.16 inference(scs_inference,[],[142,1432,1859,1783,2383,1458,1442,1430,1135,148,2039,1131,145,146,1857,151,152,153,154,156,163,167,168,226,1154,187,257,258,259,253,252,225,233,254,169,166,224,165,255,184,223,203,204,205,262,181,155,242,182,158,236,183,196,206,207,251,1504,256,170,171,173,176,178,188,191,193,194,197,198,199])).
% 60.06/60.16 cnf(4786,plain,
% 60.06/60.16 (P9(a3,f6(a3,a3,a3),a3,a3)),
% 60.06/60.16 inference(scs_inference,[],[142,1432,1859,1783,2383,1458,1442,1430,1135,148,2039,1131,145,146,1857,151,152,153,154,156,163,167,168,226,1154,187,257,258,259,253,252,225,233,254,169,166,224,165,255,184,223,203,204,205,262,181,155,242,182,158,236,183,196,206,207,251,1504,256,170,171,173,176,178,188,191,193,194,197,198,199,201,245,246,247,249,250,177,190])).
% 60.06/60.16 cnf(4790,plain,
% 60.06/60.16 (P9(a3,a3,a18,a3)),
% 60.06/60.16 inference(scs_inference,[],[142,1432,1859,1783,2383,1458,1442,1430,1135,148,2039,1131,145,146,1857,151,152,153,154,156,163,167,168,226,1154,187,257,258,259,253,252,225,233,254,169,166,224,165,255,184,223,203,204,205,262,181,155,242,182,158,236,183,196,206,207,251,1504,256,170,171,173,176,178,188,191,193,194,197,198,199,201,245,246,247,249,250,177,190,189,241])).
% 60.06/60.16 cnf(4792,plain,
% 60.06/60.16 (P3(a3,a3,a3)),
% 60.06/60.16 inference(scs_inference,[],[142,1432,1859,1783,2383,1458,1442,1430,1135,148,2039,1131,145,146,1857,151,152,153,154,156,163,167,168,226,1154,187,257,258,259,253,252,225,233,254,169,166,224,165,255,184,223,203,204,205,262,181,155,242,182,158,236,183,196,206,207,251,1504,256,170,171,173,176,178,188,191,193,194,197,198,199,201,245,246,247,249,250,177,190,189,241,161])).
% 60.06/60.16 cnf(4802,plain,
% 60.06/60.16 (P9(a18,a18,a18,a3)),
% 60.06/60.16 inference(scs_inference,[],[142,1432,1859,1783,2383,1458,1442,1430,1135,148,2039,1131,145,146,1857,1855,151,152,153,154,156,163,167,168,226,1154,187,257,258,259,253,252,225,233,254,169,166,224,165,255,184,223,203,204,205,262,181,155,242,182,158,236,183,196,206,207,251,1504,256,170,171,173,176,178,188,191,193,194,197,198,199,201,245,246,247,249,250,177,190,189,241,161,192,228,208,164,1531])).
% 60.06/60.16 cnf(4806,plain,
% 60.06/60.16 (P1(x48061,x48062,x48062)),
% 60.06/60.16 inference(scs_inference,[],[4695,160])).
% 60.06/60.16 cnf(4808,plain,
% 60.06/60.16 (P1(a18,a1,a3)),
% 60.06/60.16 inference(scs_inference,[],[4695,4665,160,152])).
% 60.06/60.16 cnf(4810,plain,
% 60.06/60.16 (P10(x48101,x48102,x48102,x48101)),
% 60.06/60.16 inference(scs_inference,[],[4695,4665,160,152,164])).
% 60.06/60.16 cnf(4812,plain,
% 60.06/60.16 (P10(a1,a1,f28(a3,a1,a3,a1,a18,a18),a18)),
% 60.06/60.16 inference(scs_inference,[],[4695,4665,4717,160,152,164,163])).
% 60.06/60.16 cnf(4814,plain,
% 60.06/60.16 (P7(a1,a1,a1,a2,a1,a1,a2,a1)),
% 60.06/60.16 inference(scs_inference,[],[4695,4685,4665,4717,160,152,164,163,257])).
% 60.06/60.16 cnf(4820,plain,
% 60.06/60.16 (P9(a1,a1,a18,a3)),
% 60.06/60.16 inference(scs_inference,[],[4695,4685,4687,4665,4790,4717,4770,160,152,164,163,257,167,256,1504])).
% 60.06/60.16 cnf(4822,plain,
% 60.06/60.16 (P1(a16,a1,a2)),
% 60.06/60.16 inference(scs_inference,[],[4695,4685,4687,4663,4665,4790,4717,4770,160,152,164,163,257,167,256,1504,151])).
% 60.06/60.16 cnf(4824,plain,
% 60.06/60.16 (P7(a1,a2,a2,a1,a1,a1,a1,a1)),
% 60.06/60.16 inference(scs_inference,[],[4695,4685,4687,4663,4665,4790,4717,4770,160,152,164,163,257,167,256,1504,151,258])).
% 60.06/60.16 cnf(4826,plain,
% 60.06/60.16 (P5(a1,a18,a3,a18)),
% 60.06/60.16 inference(scs_inference,[],[4695,4685,4687,4663,4665,4679,4790,4717,4770,160,152,164,163,257,167,256,1504,151,258,168])).
% 60.06/60.16 cnf(4828,plain,
% 60.06/60.16 (P8(x48281,x48282,x48283,x48284,x48281,x48282,x48283,x48284)),
% 60.06/60.16 inference(scs_inference,[],[4695,4685,4687,4663,4665,4679,4790,4717,4770,160,152,164,163,257,167,256,1504,151,258,168,225])).
% 60.06/60.16 cnf(4830,plain,
% 60.06/60.16 (P8(x48301,x48302,a18,a18,x48301,x48302,a3,a3)),
% 60.06/60.16 inference(scs_inference,[],[4695,4685,4687,4693,4663,4665,4679,4790,4717,4770,160,152,164,163,257,167,256,1504,151,258,168,225,253])).
% 60.06/60.16 cnf(4840,plain,
% 60.06/60.16 (P7(a18,a1,a18,a1,a1,a3,a1,a3)),
% 60.06/60.16 inference(scs_inference,[],[4695,4685,4687,4711,4693,4663,4665,4679,4709,4790,4717,4770,4713,160,152,164,163,257,167,256,1504,151,258,168,225,253,154,153,187,156,259])).
% 60.06/60.16 cnf(4844,plain,
% 60.06/60.16 (P8(a3,a3,x48441,x48442,a18,a18,x48441,x48442)),
% 60.06/60.16 inference(scs_inference,[],[4695,4685,4687,4711,4669,4693,4663,4665,4679,4709,4790,4717,4770,4713,160,152,164,163,257,167,256,1504,151,258,168,225,253,154,153,187,156,259,226,252])).
% 60.06/60.16 cnf(4846,plain,
% 60.06/60.16 (P8(x48461,x48462,a1,a1,x48462,x48461,a1,a1)),
% 60.06/60.16 inference(scs_inference,[],[4695,4685,4687,4711,4669,4689,4693,4663,4665,4679,4709,4790,4717,4770,4713,160,152,164,163,257,167,256,1504,151,258,168,225,253,154,153,187,156,259,226,252,254])).
% 60.06/60.16 cnf(4852,plain,
% 60.06/60.16 (P9(a3,a3,a18,a18)),
% 60.06/60.16 inference(scs_inference,[],[4695,4721,4685,4687,4711,4669,4689,4693,4663,4665,4679,4709,4736,4748,4790,4717,4770,4713,160,152,164,163,257,167,256,1504,151,258,168,225,253,154,153,187,156,259,226,252,254,169,224,165])).
% 60.06/60.16 cnf(4860,plain,
% 60.06/60.16 (P10(f28(a1,a3,a1,a3,a18,a18),a18,a1,a1)),
% 60.06/60.16 inference(scs_inference,[],[4667,4695,4727,4742,4721,4685,4687,4711,4669,4705,4689,4693,4663,4665,4679,4709,4736,4748,4790,4717,4770,4713,160,152,164,163,257,167,256,1504,151,258,168,225,253,154,153,187,156,259,226,252,254,169,224,165,166,255,200,204])).
% 60.06/60.16 cnf(4862,plain,
% 60.06/60.16 (P9(f13(a3,a3,a3,a3,a3),a3,a3,a3)),
% 60.06/60.16 inference(scs_inference,[],[4667,4695,4727,4742,4721,4685,4687,4711,4669,4705,4689,4693,4663,4665,4679,4709,4736,4748,4790,4717,4770,4713,1859,160,152,164,163,257,167,256,1504,151,258,168,225,253,154,153,187,156,259,226,252,254,169,224,165,166,255,200,204,198])).
% 60.06/60.16 cnf(4870,plain,
% 60.06/60.16 (P7(a1,a2,a1,a1,a1,a2,a1,a1)),
% 60.06/60.16 inference(scs_inference,[],[4667,4695,4727,4742,4721,4685,4687,4711,4669,4705,4689,4693,4663,4665,4679,4709,4725,4736,4746,4748,4790,4717,4770,4713,1859,160,152,164,163,257,167,256,1504,151,258,168,225,253,154,153,187,156,259,226,252,254,169,224,165,166,255,200,204,198,205,178,201,263])).
% 60.06/60.16 cnf(4874,plain,
% 60.06/60.16 (P3(f28(a1,a3,a1,a3,a18,a18),a1,a3)),
% 60.06/60.16 inference(scs_inference,[],[4667,4695,4727,4742,4721,4685,4687,4711,4669,4705,4689,4693,4663,4665,4679,4709,4725,4736,4746,4748,4790,4802,4717,4770,4713,1859,160,152,164,163,257,167,256,1504,151,258,168,225,253,154,153,187,156,259,226,252,254,169,224,165,166,255,200,204,198,205,178,201,263,199,203])).
% 60.06/60.16 cnf(4878,plain,
% 60.06/60.16 (P2(a3,a3,a3,a3)),
% 60.06/60.16 inference(scs_inference,[],[4667,4695,4727,4742,4721,4685,4687,4711,4669,4705,4689,4693,4663,4665,4679,4709,4725,4736,4746,4748,4790,4802,4717,4770,4713,1859,160,152,164,163,257,167,256,1504,151,258,168,225,253,154,153,187,156,259,226,252,254,169,224,165,166,255,200,204,198,205,178,201,263,199,203,193,184])).
% 60.06/60.16 cnf(4880,plain,
% 60.06/60.16 (P7(f28(a3,a1,a3,a1,a18,a18),a3,a3,a1,f28(a3,a1,a3,a1,a18,a18),a3,a3,a1)),
% 60.06/60.16 inference(scs_inference,[],[4667,4695,4727,4742,4721,4685,4687,4711,4669,4705,4689,4693,4663,4665,4679,4709,4725,4736,4746,4748,4790,4802,4717,4770,4713,1859,160,152,164,163,257,167,256,1504,151,258,168,225,253,154,153,187,156,259,226,252,254,169,224,165,166,255,200,204,198,205,178,201,263,199,203,193,184,223])).
% 60.06/60.16 cnf(4892,plain,
% 60.06/60.16 (P9(a18,a18,a1,a1)),
% 60.06/60.16 inference(scs_inference,[],[4667,4695,4727,4742,4721,4792,4685,4687,4711,4669,4675,4705,4689,4693,4663,4665,4679,4709,4725,4736,4746,4748,4750,4790,4802,4717,4770,4713,1859,160,152,164,163,257,167,256,1504,151,258,168,225,253,154,153,187,156,259,226,252,254,169,224,165,166,255,200,204,198,205,178,201,263,199,203,193,184,223,177,189,190,227,185,181])).
% 60.06/60.16 cnf(4894,plain,
% 60.06/60.16 (P9(a18,a18,a18,a18)),
% 60.06/60.16 inference(scs_inference,[],[4667,4695,4727,4742,4721,4792,4685,4687,4711,4669,4675,4705,4689,4693,4663,4665,4679,4709,4725,4736,4746,4748,4750,4790,4802,4717,4770,4713,1859,160,152,164,163,257,167,256,1504,151,258,168,225,253,154,153,187,156,259,226,252,254,169,224,165,166,255,200,204,198,205,178,201,263,199,203,193,184,223,177,189,190,227,185,181,241])).
% 60.06/60.16 cnf(4897,plain,
% 60.06/60.16 (P10(a18,a3,a3,a3)),
% 60.06/60.16 inference(scs_inference,[],[4667,4695,4727,4742,4721,4792,4685,4687,4711,4669,4675,4705,4689,4693,4663,4665,4679,4709,4725,4736,4746,4748,4750,4790,4802,4717,4770,4713,1859,160,152,164,163,257,167,256,1504,151,258,168,225,253,154,153,187,156,259,226,252,254,169,224,165,166,255,200,204,198,205,178,201,263,199,203,193,184,223,177,189,190,227,185,181,241,180])).
% 60.06/60.16 cnf(4899,plain,
% 60.06/60.16 (P4(x48991,a2,a16,a16)),
% 60.06/60.16 inference(scs_inference,[],[4667,4695,4727,4742,4721,4792,4685,4687,4711,4669,4675,4705,4689,4693,4663,4665,4679,4709,4723,4725,4736,4746,4748,4750,4790,4802,4717,4770,4713,1859,160,152,164,163,257,167,256,1504,151,258,168,225,253,154,153,187,156,259,226,252,254,169,224,165,166,255,200,204,198,205,178,201,263,199,203,193,184,223,177,189,190,227,185,181,241,180,236])).
% 60.06/60.16 cnf(4904,plain,
% 60.06/60.16 (P4(a18,a18,a18,a18)),
% 60.06/60.16 inference(scs_inference,[],[4667,4695,4727,4742,4721,4792,4685,4687,4711,4669,4675,4705,4689,4693,4663,4665,4679,4709,4723,4725,4734,4736,4746,4748,4750,4790,4802,4717,4770,4713,391,1859,160,152,164,163,257,167,256,1504,151,258,168,225,253,154,153,187,156,259,226,252,254,169,224,165,166,255,200,204,198,205,178,201,263,199,203,193,184,223,177,189,190,227,185,181,241,180,236,102,186,196])).
% 60.06/60.16 cnf(4908,plain,
% 60.06/60.16 (P5(a1,a1,a1,a1)),
% 60.06/60.16 inference(scs_inference,[],[4667,4695,4727,4742,4721,4792,4685,4687,4711,4669,4675,4705,4689,4693,4663,4665,4671,4679,4709,4723,4725,4731,4734,4736,4746,4748,4750,4790,4802,4717,4770,4713,391,1859,160,152,164,163,257,167,256,1504,151,258,168,225,253,154,153,187,156,259,226,252,254,169,224,165,166,255,200,204,198,205,178,201,263,199,203,193,184,223,177,189,190,227,185,181,241,180,236,102,186,196,228,251])).
% 60.06/60.16 cnf(4909,plain,
% 60.06/60.16 (P8(x49091,x49092,a1,a1,x49091,x49092,a1,a1)),
% 60.06/60.16 inference(rename_variables,[],[4689])).
% 60.06/60.16 cnf(4911,plain,
% 60.06/60.16 (P3(f25(a3,x49111),a3,x49111)),
% 60.06/60.16 inference(scs_inference,[],[4667,4695,4727,4742,4721,4792,4685,4687,4711,4669,4675,4705,4689,4693,4663,4665,4671,4679,4709,4723,4725,4731,4734,4736,4746,4748,4750,4790,4802,4717,4770,4713,391,1859,160,152,164,163,257,167,256,1504,151,258,168,225,253,154,153,187,156,259,226,252,254,169,224,165,166,255,200,204,198,205,178,201,263,199,203,193,184,223,177,189,190,227,185,181,241,180,236,102,186,196,228,251,159])).
% 60.06/60.16 cnf(4918,plain,
% 60.06/60.16 (P4(a1,a1,a1,a3)),
% 60.06/60.16 inference(scs_inference,[],[4667,4695,4727,4742,4721,4792,4685,4687,4711,4669,4675,4705,4689,4693,4663,4665,4671,4679,4709,4723,4725,4731,4734,4736,4746,4748,4750,4790,4802,4717,4770,4713,391,1859,160,152,164,163,257,167,256,1504,151,258,168,225,253,154,153,187,156,259,226,252,254,169,224,165,166,255,200,204,198,205,178,201,263,199,203,193,184,223,177,189,190,227,185,181,241,180,236,102,186,196,228,251,159,2,342,170,171])).
% 60.06/60.16 cnf(4926,plain,
% 60.06/60.16 (P10(a3,a3,a18,a3)),
% 60.06/60.16 inference(scs_inference,[],[4667,4695,4727,4742,4721,4792,4685,4687,4711,4669,4675,4705,4744,4689,4693,4663,4665,4671,4679,4691,4709,4723,4725,4731,4734,4736,4746,4748,4750,4790,4802,4717,4770,4713,391,1859,272,160,152,164,163,257,167,256,1504,151,258,168,225,253,154,153,187,156,259,226,252,254,169,224,165,166,255,200,204,198,205,178,201,263,199,203,193,184,223,177,189,190,227,185,181,241,180,236,102,186,196,228,251,159,2,342,170,171,220,230,246,240])).
% 60.06/60.16 cnf(4931,plain,
% 60.06/60.16 (P2(f9(a18,a18,a18),a18,a18,a18)),
% 60.06/60.16 inference(scs_inference,[],[4667,4695,4727,4742,4721,4792,4685,4687,4711,4669,4675,4705,4744,4689,4909,4693,4663,4665,4671,4679,4691,4709,4723,4725,4731,4734,4736,4746,4748,4750,4790,4802,4717,4770,4713,391,1859,272,160,152,164,163,257,167,256,1504,151,258,168,225,253,154,153,187,156,259,226,252,254,169,224,165,166,255,200,204,198,205,178,201,263,199,203,193,184,223,177,189,190,227,185,181,241,180,236,102,186,196,228,251,159,2,342,170,171,220,230,246,240,245,191])).
% 60.06/60.16 cnf(4933,plain,
% 60.06/60.16 (P5(a2,a1,a2,a1)),
% 60.06/60.16 inference(scs_inference,[],[4667,4695,4727,4742,4721,4792,4685,4687,4711,4669,4675,4705,4744,4689,4909,4693,4663,4665,4671,4679,4691,4709,4723,4725,4731,4734,4736,4746,4748,4750,4790,4802,4717,4770,4713,391,1859,272,160,152,164,163,257,167,256,1504,151,258,168,225,253,154,153,187,156,259,226,252,254,169,224,165,166,255,200,204,198,205,178,201,263,199,203,193,184,223,177,189,190,227,185,181,241,180,236,102,186,196,228,251,159,2,342,170,171,220,230,246,240,245,191,243])).
% 60.06/60.16 cnf(4935,plain,
% 60.06/60.16 (P9(a1,a1,a1,a1)),
% 60.06/60.16 inference(scs_inference,[],[4667,4695,4727,4742,4721,4792,4685,4687,4711,4669,4675,4705,4744,4689,4909,4693,4663,4665,4671,4679,4691,4709,4723,4725,4731,4734,4736,4746,4748,4750,4790,4802,4717,4770,4713,391,1859,272,160,152,164,163,257,167,256,1504,151,258,168,225,253,154,153,187,156,259,226,252,254,169,224,165,166,255,200,204,198,205,178,201,263,199,203,193,184,223,177,189,190,227,185,181,241,180,236,102,186,196,228,251,159,2,342,170,171,220,230,246,240,245,191,243,195])).
% 60.06/60.16 cnf(4937,plain,
% 60.06/60.16 (P2(f10(a3,a3,a1),a3,a3,a1)),
% 60.06/60.16 inference(scs_inference,[],[4667,4695,4727,4742,4721,4792,4685,4687,4711,4669,4675,4705,4744,4689,4909,4693,4663,4665,4671,4679,4691,4709,4723,4725,4731,4734,4736,4746,4748,4750,4790,4802,4717,4770,4713,391,1859,272,160,152,164,163,257,167,256,1504,151,258,168,225,253,154,153,187,156,259,226,252,254,169,224,165,166,255,200,204,198,205,178,201,263,199,203,193,184,223,177,189,190,227,185,181,241,180,236,102,186,196,228,251,159,2,342,170,171,220,230,246,240,245,191,243,195,192])).
% 60.06/60.16 cnf(4948,plain,
% 60.06/60.16 (P3(a18,a3,a3)),
% 60.06/60.16 inference(scs_inference,[],[4806,2385])).
% 60.06/60.16 cnf(4951,plain,
% 60.06/60.16 (P1(a16,a2,a1)),
% 60.06/60.16 inference(scs_inference,[],[4822,152])).
% 60.06/60.16 cnf(4953,plain,
% 60.06/60.16 (P10(a18,a3,a1,a1)),
% 60.06/60.16 inference(scs_inference,[],[4897,4822,152,342])).
% 60.06/60.16 cnf(4955,plain,
% 60.06/60.16 (P5(a3,a18,a1,a18)),
% 60.06/60.16 inference(scs_inference,[],[4897,4822,4826,152,342,167])).
% 60.06/60.16 cnf(4957,plain,
% 60.06/60.16 (P7(a1,a1,a1,a1,a1,a2,a2,a1)),
% 60.06/60.16 inference(scs_inference,[],[4824,4897,4822,4826,152,342,167,256])).
% 60.06/60.16 cnf(4959,plain,
% 60.06/60.16 (P5(f25(a3,x49591),a3,f25(a3,x49591),x49591)),
% 60.06/60.16 inference(scs_inference,[],[4824,4897,4822,4826,4911,152,342,167,256,156])).
% 60.06/60.16 cnf(4961,plain,
% 60.06/60.16 (P10(a1,a1,f28(a1,a3,a1,a3,a18,a18),a18)),
% 60.06/60.16 inference(scs_inference,[],[4824,4897,4822,4826,4860,4911,152,342,167,256,156,163])).
% 60.06/60.16 cnf(4963,plain,
% 60.06/60.16 (P10(a3,a3,a3,a18)),
% 60.06/60.16 inference(scs_inference,[],[4824,4897,4822,4826,4926,4860,4911,152,342,167,256,156,163,164])).
% 60.06/60.16 cnf(4965,plain,
% 60.06/60.16 (P8(x49651,x49652,x49653,x49654,x49652,x49651,x49653,x49654)),
% 60.06/60.16 inference(scs_inference,[],[4810,4824,4897,4822,4826,4926,4860,4911,152,342,167,256,156,163,164,225])).
% 60.06/60.16 cnf(4967,plain,
% 60.06/60.16 (P4(x49671,a16,a2,a16)),
% 60.06/60.16 inference(scs_inference,[],[4810,4824,4897,4899,4822,4826,4926,4860,4911,152,342,167,256,156,163,164,225,170])).
% 60.06/60.16 cnf(4971,plain,
% 60.06/60.16 (P8(a2,a1,a1,a1,a1,a1,a2,a1)),
% 60.06/60.16 inference(scs_inference,[],[4810,4852,4824,4897,4899,4822,4826,4926,4933,4860,4911,152,342,167,256,156,163,164,225,170,1504,226])).
% 60.06/60.16 cnf(4975,plain,
% 60.06/60.16 (P8(x49751,x49752,a3,a3,x49751,x49752,a18,a18)),
% 60.06/60.16 inference(scs_inference,[],[4810,4852,4824,4897,4844,4899,4822,4826,4926,4933,4860,4911,152,342,167,256,156,163,164,225,170,1504,226,257,253])).
% 60.06/60.16 cnf(4979,plain,
% 60.06/60.16 (P1(x49791,x49792,x49791)),
% 60.06/60.16 inference(scs_inference,[],[4810,4806,4852,4824,4897,4844,4899,4822,4826,4878,4926,4933,4860,4911,152,342,167,256,156,163,164,225,170,1504,226,257,253,187,151])).
% 60.06/60.16 cnf(4987,plain,
% 60.06/60.16 (P7(a1,a2,a1,a2,a1,a1,a1,a1)),
% 60.06/60.16 inference(scs_inference,[],[4810,4806,4852,4824,4897,4844,4899,4697,4822,4826,4870,4878,4926,4933,4860,4911,152,342,167,256,156,163,164,225,170,1504,226,257,253,187,151,153,252,168,259])).
% 60.06/60.16 cnf(4989,plain,
% 60.06/60.16 (P7(a1,a18,a18,a1,a1,a3,a1,a3)),
% 60.06/60.16 inference(scs_inference,[],[4810,4806,4852,4824,4897,4844,4899,4697,4822,4826,4840,4870,4878,4926,4933,4860,4911,152,342,167,256,156,163,164,225,170,1504,226,257,253,187,151,153,252,168,259,258])).
% 60.06/60.16 cnf(4991,plain,
% 60.06/60.16 (P3(f25(a3,x49911),x49911,a3)),
% 60.06/60.16 inference(scs_inference,[],[4810,4806,4852,4824,4897,4844,4899,4697,4822,4826,4840,4870,4878,4926,4933,4860,4911,152,342,167,256,156,163,164,225,170,1504,226,257,253,187,151,153,252,168,259,258,154])).
% 60.06/60.16 cnf(4993,plain,
% 60.06/60.16 (P4(a2,x49931,a16,a16)),
% 60.06/60.16 inference(scs_inference,[],[4810,4806,4852,4824,4897,4844,4899,4697,4822,4826,4840,4870,4878,4926,4933,4860,4911,152,342,167,256,156,163,164,225,170,1504,226,257,253,187,151,153,252,168,259,258,154,169])).
% 60.06/60.16 cnf(4995,plain,
% 60.06/60.16 (P8(x49951,x49952,a18,a18,x49952,x49951,a3,a3)),
% 60.06/60.16 inference(scs_inference,[],[4810,4806,4852,4824,4897,4830,4844,4899,4697,4822,4826,4840,4870,4878,4926,4933,4860,4911,152,342,167,256,156,163,164,225,170,1504,226,257,253,187,151,153,252,168,259,258,154,169,254])).
% 60.06/60.16 cnf(4997,plain,
% 60.06/60.16 (P4(x49971,a16,a16,a2)),
% 60.06/60.16 inference(scs_inference,[],[4810,4806,4852,4824,4897,4830,4844,4899,4697,4822,4826,4840,4870,4878,4926,4933,4860,4911,152,342,167,256,156,163,164,225,170,1504,226,257,253,187,151,153,252,168,259,258,154,169,254,171])).
% 60.06/60.16 cnf(5001,plain,
% 60.06/60.16 (P9(a16,a2,a1,a3)),
% 60.06/60.16 inference(scs_inference,[],[4810,4806,4852,4824,4701,4897,4830,4844,4899,4697,4822,4826,4840,4870,4878,4926,4933,4860,4911,4750,152,342,167,256,156,163,164,225,170,1504,226,257,253,187,151,153,252,168,259,258,154,169,254,171,224,165])).
% 60.06/60.16 cnf(5005,plain,
% 60.06/60.16 (P8(x50051,x50052,x50051,x50052,x50053,x50054,x50053,x50054)),
% 60.06/60.16 inference(scs_inference,[],[4810,4828,4806,4852,4824,4701,4897,4830,4844,4899,4697,4820,4822,4826,4840,4870,4878,4926,4933,4860,4911,4750,152,342,167,256,156,163,164,225,170,1504,226,257,253,187,151,153,252,168,259,258,154,169,254,171,224,165,166,255])).
% 60.06/60.16 cnf(5007,plain,
% 60.06/60.16 (P10(f28(a3,a3,a3,a3,a3,a3),a3,a3,a3)),
% 60.06/60.16 inference(scs_inference,[],[4810,4828,4806,4852,4824,4701,4897,4830,4844,4899,4697,4820,4822,4826,4840,4870,4878,4926,4933,4860,4911,4750,4792,152,342,167,256,156,163,164,225,170,1504,226,257,253,187,151,153,252,168,259,258,154,169,254,171,224,165,166,255,204])).
% 60.06/60.16 cnf(5011,plain,
% 60.06/60.16 (P9(f13(a1,a1,a1,a2,a16),a1,a2,a16)),
% 60.06/60.16 inference(scs_inference,[],[142,4810,4828,4806,4908,4935,4852,4824,4701,4897,4830,4844,4899,4697,4820,4822,4826,4840,4870,4878,4926,4933,4860,4911,4750,4792,152,342,167,256,156,163,164,225,170,1504,226,257,253,187,151,153,252,168,259,258,154,169,254,171,224,165,166,255,204,188,198])).
% 60.06/60.16 cnf(5016,plain,
% 60.06/60.16 (P8(x50161,x50162,x50163,x50164,x50161,x50162,x50163,x50164)),
% 60.06/60.16 inference(rename_variables,[],[4828])).
% 60.06/60.16 cnf(5022,plain,
% 60.06/60.16 (P1(f13(a1,a1,a1,a2,a16),a2,a16)),
% 60.06/60.16 inference(scs_inference,[],[142,4810,4828,4806,4908,4935,4852,4824,4701,4897,4830,4844,4899,4697,4820,4822,4826,4840,4870,4878,4926,4933,4860,4911,4802,4750,4792,152,342,167,256,156,163,164,225,170,1504,226,257,253,187,151,153,252,168,259,258,154,169,254,171,224,165,166,255,204,188,198,178,246,176,200,197])).
% 60.06/60.16 cnf(5026,plain,
% 60.06/60.16 (P5(f13(a3,a3,a3,a3,a3),a3,f13(a3,a3,a3,a3,a3),a3)),
% 60.06/60.16 inference(scs_inference,[],[142,4810,4828,4806,4908,4935,4852,4894,4824,4701,4897,4830,4844,4899,4697,4820,4822,4826,4840,4870,4878,4926,4933,4860,4911,4862,4802,4750,4669,4792,152,342,167,256,156,163,164,225,170,1504,226,257,253,187,151,153,252,168,259,258,154,169,254,171,224,165,166,255,204,188,198,178,246,176,200,197,199,173])).
% 60.06/60.16 cnf(5028,plain,
% 60.06/60.16 (P2(a1,a1,a1,a1)),
% 60.06/60.16 inference(scs_inference,[],[142,4810,4828,4806,4908,4935,4852,4894,4824,4701,4897,4830,4844,4899,4697,4820,4822,4826,4840,4870,4878,4926,4933,4860,4911,4862,4802,4750,4669,4792,152,342,167,256,156,163,164,225,170,1504,226,257,253,187,151,153,252,168,259,258,154,169,254,171,224,165,166,255,204,188,198,178,246,176,200,197,199,173,184])).
% 60.06/60.16 cnf(5047,plain,
% 60.06/60.16 (P3(f25(a3,x50471),a3,x50471)),
% 60.06/60.16 inference(rename_variables,[],[4911])).
% 60.06/60.16 cnf(5053,plain,
% 60.06/60.16 (P9(a1,a3,a18,a18)),
% 60.06/60.16 inference(scs_inference,[],[142,4810,4828,4806,4908,4935,4852,4894,4824,4701,4897,4830,4844,4899,4697,4820,4822,4826,4840,4870,4878,4918,4926,4933,4860,4911,4862,4802,4750,4669,4792,152,342,167,256,156,163,164,225,170,1504,226,257,253,187,151,153,252,168,259,258,154,169,254,171,224,165,166,255,204,188,198,178,246,176,200,197,199,173,184,203,193,201,189,223,191,245,177,227,190,243,181])).
% 60.06/60.16 cnf(5055,plain,
% 60.06/60.16 (P10(f28(a1,a3,a1,a3,a18,a18),a18,f28(a3,a1,a3,a1,a18,a18),a18)),
% 60.06/60.16 inference(scs_inference,[],[142,4810,4828,4806,4908,4935,4852,4894,4824,4701,4897,4830,4844,4899,4697,4820,4822,4826,4840,4870,4878,4918,4926,4933,4860,4812,4911,4862,4802,4750,4669,4792,152,342,167,256,156,163,164,225,170,1504,226,257,253,187,151,153,252,168,259,258,154,169,254,171,224,165,166,255,204,188,198,178,246,176,200,197,199,173,184,203,193,201,189,223,191,245,177,227,190,243,181,179])).
% 60.06/60.16 cnf(5058,plain,
% 60.06/60.16 (P3(f25(a3,x50581),a3,x50581)),
% 60.06/60.16 inference(rename_variables,[],[4911])).
% 60.06/60.16 cnf(5064,plain,
% 60.06/60.16 (P10(a3,a3,x50641,x50641)),
% 60.06/60.16 inference(scs_inference,[],[142,4810,4828,4806,4908,4935,4852,4894,4824,4701,4897,4830,4844,4899,4697,4820,4822,4826,4840,4870,4878,4918,4926,4933,4860,4812,4786,4911,5047,5058,4862,4802,4750,4669,331,4792,4727,152,342,167,256,156,163,164,225,170,1504,226,257,253,187,151,153,252,168,259,258,154,169,254,171,224,165,166,255,204,188,198,178,246,176,200,197,199,173,184,203,193,201,189,223,191,245,177,227,190,243,181,179,174,241,101,157])).
% 60.06/60.16 cnf(5066,plain,
% 60.06/60.16 (P4(x50661,x50662,x50662,x50662)),
% 60.06/60.16 inference(scs_inference,[],[142,4810,4828,5016,4806,4908,4935,4852,4894,4824,4701,4897,4830,4844,4899,4697,4820,4822,4826,4840,4870,4878,4918,4926,4933,4860,4812,4786,4911,5047,5058,4862,4802,4750,4669,331,4792,4727,152,342,167,256,156,163,164,225,170,1504,226,257,253,187,151,153,252,168,259,258,154,169,254,171,224,165,166,255,204,188,198,178,246,176,200,197,199,173,184,203,193,201,189,223,191,245,177,227,190,243,181,179,174,241,101,157,236])).
% 60.06/60.16 cnf(5067,plain,
% 60.06/60.16 (P8(x50671,x50672,x50673,x50674,x50671,x50672,x50673,x50674)),
% 60.06/60.16 inference(rename_variables,[],[4828])).
% 60.06/60.16 cnf(5068,plain,
% 60.06/60.16 (P1(x50681,x50682,x50682)),
% 60.06/60.16 inference(rename_variables,[],[4806])).
% 60.06/60.16 cnf(5070,plain,
% 60.06/60.16 (P3(a1,a1,a1)),
% 60.06/60.16 inference(scs_inference,[],[142,4810,4828,5016,4806,5068,4908,4935,4852,4894,4824,4701,4897,4830,4844,4846,4899,4697,4820,4822,4826,4840,4870,4878,4918,4926,4933,4860,4812,4786,4911,5047,5058,4862,4802,4750,4669,331,4792,4727,152,342,167,256,156,163,164,225,170,1504,226,257,253,187,151,153,252,168,259,258,154,169,254,171,224,165,166,255,204,188,198,178,246,176,200,197,199,173,184,203,193,201,189,223,191,245,177,227,190,243,181,179,174,241,101,157,236,239])).
% 60.06/60.16 cnf(5072,plain,
% 60.06/60.16 (P1(x50721,x50722,x50722)),
% 60.06/60.16 inference(rename_variables,[],[4806])).
% 60.06/60.16 cnf(5081,plain,
% 60.06/60.16 (P10(x50811,x50812,x50812,x50811)),
% 60.06/60.16 inference(rename_variables,[],[4810])).
% 60.06/60.16 cnf(5082,plain,
% 60.06/60.16 (P1(x50821,x50822,x50822)),
% 60.06/60.16 inference(rename_variables,[],[4806])).
% 60.06/60.16 cnf(5085,plain,
% 60.06/60.16 (P10(x50851,x50852,x50852,x50851)),
% 60.06/60.16 inference(rename_variables,[],[4810])).
% 60.06/60.16 cnf(5091,plain,
% 60.06/60.16 (P1(x50911,x50912,x50912)),
% 60.06/60.16 inference(rename_variables,[],[4806])).
% 60.06/60.16 cnf(5093,plain,
% 60.06/60.16 (P5(a18,a18,a18,a18)),
% 60.06/60.16 inference(scs_inference,[],[142,4810,5081,5085,4828,5016,5067,4806,5068,5072,5082,4908,4935,4852,4894,4824,4701,4897,4904,4830,4844,4846,4899,4697,4820,4822,4826,4840,4870,4878,4918,4926,4933,4860,4812,4786,4911,5047,5058,4862,4802,4663,4750,4669,331,4695,4792,4727,152,342,167,256,156,163,164,225,170,1504,226,257,253,187,151,153,252,168,259,258,154,169,254,171,224,165,166,255,204,188,198,178,246,176,200,197,199,173,184,203,193,201,189,223,191,245,177,227,190,243,181,179,174,241,101,157,236,239,186,175,209,207,206,208,251])).
% 60.06/60.16 cnf(5094,plain,
% 60.06/60.16 (P8(x50941,x50942,x50943,x50944,x50941,x50942,x50943,x50944)),
% 60.06/60.16 inference(rename_variables,[],[4828])).
% 60.06/60.16 cnf(5096,plain,
% 60.06/60.16 (P3(f25(a1,x50961),a1,x50961)),
% 60.06/60.16 inference(scs_inference,[],[142,4810,5081,5085,4828,5016,5067,4806,5068,5072,5082,5091,4908,4935,4852,4894,4824,4701,4897,4904,4830,4844,4846,4899,4697,4820,4822,4826,4840,4870,4878,4918,4926,4933,4860,4812,4786,4911,5047,5058,4862,4802,4663,4750,4669,331,4695,4792,4727,152,342,167,256,156,163,164,225,170,1504,226,257,253,187,151,153,252,168,259,258,154,169,254,171,224,165,166,255,204,188,198,178,246,176,200,197,199,173,184,203,193,201,189,223,191,245,177,227,190,243,181,179,174,241,101,157,236,239,186,175,209,207,206,208,251,159])).
% 60.06/60.16 cnf(5100,plain,
% 60.06/60.16 (P9(a18,a18,a3,a18)),
% 60.06/60.16 inference(scs_inference,[],[142,4810,5081,5085,4828,5016,5067,4806,5068,5072,5082,5091,4908,4935,4852,4894,4824,4701,4897,4904,4830,4844,4846,4899,4697,4820,4822,4826,4840,4870,4878,4918,4926,4933,4860,4812,4786,4911,5047,5058,4862,4802,4663,4750,4669,331,4695,4792,4727,152,342,167,256,156,163,164,225,170,1504,226,257,253,187,151,153,252,168,259,258,154,169,254,171,224,165,166,255,204,188,198,178,246,176,200,197,199,173,184,203,193,201,189,223,191,245,177,227,190,243,181,179,174,241,101,157,236,239,186,175,209,207,206,208,251,159,361])).
% 60.06/60.16 cnf(5105,plain,
% 60.06/60.16 (P9(a3,a3,a3,a18)),
% 60.06/60.16 inference(scs_inference,[],[142,4810,5081,5085,4828,5016,5067,4806,5068,5072,5082,5091,4908,4935,4852,4894,4824,4701,4897,4904,4830,4844,4846,4899,4697,4820,4822,4826,4840,4870,4878,4918,4926,4933,4860,4812,4786,4911,5047,5058,4862,4802,4663,4750,4669,331,4695,4792,4727,152,342,167,256,156,163,164,225,170,1504,226,257,253,187,151,153,252,168,259,258,154,169,254,171,224,165,166,255,204,188,198,178,246,176,200,197,199,173,184,203,193,201,189,223,191,245,177,227,190,243,181,179,174,241,101,157,236,239,186,175,209,207,206,208,251,159,361,160,2,558])).
% 60.06/60.16 cnf(5112,plain,
% 60.06/60.16 (P1(f15(a18,a3,a3,a18),a3,a18)),
% 60.06/60.16 inference(scs_inference,[],[142,4810,5081,5085,4828,5016,5067,5094,4806,5068,5072,5082,5091,4908,4935,4852,4894,4824,4701,4897,4904,4830,4844,4846,4899,4697,4820,4822,4826,4840,4870,4878,4918,4926,4933,4860,4812,4786,4911,5047,5058,4862,4802,4663,4750,4677,4669,331,4695,4792,4727,152,342,167,256,156,163,164,225,170,1504,226,257,253,187,151,153,252,168,259,258,154,169,254,171,224,165,166,255,204,188,198,178,246,176,200,197,199,173,184,203,193,201,189,223,191,245,177,227,190,243,181,179,174,241,101,157,236,239,186,175,209,207,206,208,251,159,361,160,2,558,260,249,247])).
% 60.06/60.16 cnf(5116,plain,
% 60.06/60.16 (P1(f15(a18,a3,a3,a18),a18,a3)),
% 60.06/60.16 inference(scs_inference,[],[142,4810,5081,5085,4828,5016,5067,5094,4806,5068,5072,5082,5091,4908,4935,4852,4894,4824,4701,4897,4904,4830,4844,4846,4899,4697,4820,4822,4826,4840,4870,4878,4918,4926,4933,4860,4812,4786,4911,5047,5058,4862,4802,4663,4750,4677,4669,331,4695,4792,4727,152,342,167,256,156,163,164,225,170,1504,226,257,253,187,151,153,252,168,259,258,154,169,254,171,224,165,166,255,204,188,198,178,246,176,200,197,199,173,184,203,193,201,189,223,191,245,177,227,190,243,181,179,174,241,101,157,236,239,186,175,209,207,206,208,251,159,361,160,2,558,260,249,247,205,248])).
% 60.06/60.16 cnf(5126,plain,
% 60.06/60.16 (P7(a1,a18,a18,a1,a1,a18,a18,a1)),
% 60.06/60.16 inference(scs_inference,[],[4979,772])).
% 60.06/60.16 cnf(5127,plain,
% 60.06/60.16 (P1(x51271,x51272,x51271)),
% 60.06/60.16 inference(rename_variables,[],[4979])).
% 60.06/60.16 cnf(5129,plain,
% 60.06/60.16 (P7(a3,a1,a1,a3,a3,a1,a1,a3)),
% 60.06/60.16 inference(scs_inference,[],[4979,5127,772,1574])).
% 60.06/60.16 cnf(5130,plain,
% 60.06/60.16 (P1(x51301,x51302,x51301)),
% 60.06/60.16 inference(rename_variables,[],[4979])).
% 60.06/60.16 cnf(5132,plain,
% 60.06/60.16 (P7(a1,a3,a3,a1,a1,a3,a3,a1)),
% 60.06/60.16 inference(scs_inference,[],[4979,5127,5130,772,1574,932])).
% 60.06/60.16 cnf(5133,plain,
% 60.06/60.16 (P1(x51331,x51332,x51331)),
% 60.06/60.16 inference(rename_variables,[],[4979])).
% 60.06/60.16 cnf(5135,plain,
% 60.06/60.16 (P7(a3,a18,a18,a3,a3,a18,a18,a3)),
% 60.06/60.16 inference(scs_inference,[],[4979,5127,5130,5133,772,1574,932,1577])).
% 60.06/60.16 cnf(5136,plain,
% 60.06/60.16 (P1(x51361,x51362,x51361)),
% 60.06/60.16 inference(rename_variables,[],[4979])).
% 60.06/60.16 cnf(5138,plain,
% 60.06/60.16 (P1(x51381,x51381,x51382)),
% 60.06/60.16 inference(scs_inference,[],[4979,5127,5130,5133,5136,772,1574,932,1577,152])).
% 60.06/60.16 cnf(5142,plain,
% 60.06/60.16 (P10(x51421,x51421,a3,a3)),
% 60.06/60.16 inference(scs_inference,[],[4979,5127,5130,5133,5136,5064,5007,772,1574,932,1577,152,342,163])).
% 60.06/60.16 cnf(5154,plain,
% 60.06/60.16 (P8(a3,a3,x51541,x51542,x51543,x51543,x51541,x51542)),
% 60.06/60.16 inference(scs_inference,[],[4979,5127,5130,5133,5136,4957,4995,5064,4814,4758,5007,5055,772,1574,932,1577,152,342,163,164,252,167,257,256,225])).
% 60.06/60.16 cnf(5158,plain,
% 60.06/60.16 (P7(a1,a18,a1,a3,a18,a1,a1,a3)),
% 60.06/60.16 inference(scs_inference,[],[4979,5127,5130,5133,5136,4957,4995,5064,4814,4989,4758,5007,4874,5055,772,1574,932,1577,152,342,163,164,252,167,257,256,225,156,259])).
% 60.06/60.16 cnf(5160,plain,
% 60.06/60.16 (P4(a2,a16,x51601,a16)),
% 60.06/60.16 inference(scs_inference,[],[4979,5127,5130,5133,5136,4957,4995,5064,4993,4814,4989,4758,5007,4874,5055,772,1574,932,1577,152,342,163,164,252,167,257,256,225,156,259,170])).
% 60.06/60.16 cnf(5162,plain,
% 60.06/60.16 (P8(x51621,x51622,x51623,x51624,x51621,x51622,x51624,x51623)),
% 60.06/60.16 inference(scs_inference,[],[4965,4979,5127,5130,5133,5136,4957,4995,5064,4993,4814,4989,4758,5007,4874,5055,772,1574,932,1577,152,342,163,164,252,167,257,256,225,156,259,170,253])).
% 60.06/60.16 cnf(5170,plain,
% 60.06/60.16 (P4(x51701,x51702,x51701,x51701)),
% 60.06/60.16 inference(scs_inference,[],[4965,5066,4979,5127,5130,5133,5136,4957,4995,5064,4993,4814,4989,4880,4758,5007,5116,4874,5055,772,1574,932,1577,152,342,163,164,252,167,257,256,225,156,259,170,253,153,258,151,169])).
% 60.06/60.16 cnf(5174,plain,
% 60.06/60.16 (P5(a3,a18,a18,a1)),
% 60.06/60.16 inference(scs_inference,[],[4965,5066,4979,5127,5130,5133,5136,4957,4955,4995,5064,4993,4814,4989,4880,4758,5007,5116,4874,5055,772,1574,932,1577,152,342,163,164,252,167,257,256,225,156,259,170,253,153,258,151,169,226,168])).
% 60.06/60.16 cnf(5176,plain,
% 60.06/60.16 (P9(f8(a1,a1,a1,a1),a1,a1,a1)),
% 60.06/60.16 inference(scs_inference,[],[4965,5066,4979,5127,5130,5133,5136,4957,4955,4995,5064,4993,4814,4989,5028,4880,4758,5007,5116,4874,5055,772,1574,932,1577,152,342,163,164,252,167,257,256,225,156,259,170,253,153,258,151,169,226,168,187])).
% 60.06/60.16 cnf(5178,plain,
% 60.06/60.16 (P3(f28(a1,a3,a1,a3,a18,a18),a3,a1)),
% 60.06/60.16 inference(scs_inference,[],[4965,5066,4979,5127,5130,5133,5136,4957,4955,4995,5064,4993,4814,4989,5028,4880,4758,5007,5116,4874,5055,772,1574,932,1577,152,342,163,164,252,167,257,256,225,156,259,170,253,153,258,151,169,226,168,187,154])).
% 60.06/60.16 cnf(5180,plain,
% 60.06/60.16 (P8(x51801,x51802,x51802,x51801,x51803,x51804,x51803,x51804)),
% 60.06/60.16 inference(scs_inference,[],[4965,5005,5066,4979,5127,5130,5133,5136,4957,4955,4995,5064,4993,4814,4989,5028,4880,4758,5007,5116,4874,5055,772,1574,932,1577,152,342,163,164,252,167,257,256,225,156,259,170,253,153,258,151,169,226,168,187,154,254])).
% 60.06/60.16 cnf(5182,plain,
% 60.06/60.16 (P4(a2,a16,a16,x51821)),
% 60.06/60.16 inference(scs_inference,[],[4965,5005,5066,4979,5127,5130,5133,5136,4957,4955,4995,5064,4993,4814,4989,5028,4880,4758,5007,5116,4874,5055,772,1574,932,1577,152,342,163,164,252,167,257,256,225,156,259,170,253,153,258,151,169,226,168,187,154,254,171])).
% 60.06/60.16 cnf(5186,plain,
% 60.06/60.16 (P9(a3,a18,a18,a18)),
% 60.06/60.16 inference(scs_inference,[],[4965,5005,5066,4979,5127,5130,5133,5136,4957,4955,5100,4995,5064,4967,4993,4814,4989,5028,4880,4758,5007,5116,4874,5055,772,1574,932,1577,152,342,163,164,252,167,257,256,225,156,259,170,253,153,258,151,169,226,168,187,154,254,171,224,165])).
% 60.06/60.16 cnf(5188,plain,
% 60.06/60.16 (P9(a16,a2,a3,a1)),
% 60.06/60.16 inference(scs_inference,[],[4965,5005,5066,4979,5127,5130,5133,5136,4957,4955,5100,4995,5064,4967,4993,4814,4989,5001,5028,4880,4758,5007,5116,4874,5055,772,1574,932,1577,152,342,163,164,252,167,257,256,225,156,259,170,253,153,258,151,169,226,168,187,154,254,171,224,165,166])).
% 60.06/60.16 cnf(5192,plain,
% 60.06/60.16 (P10(f28(a3,a3,a3,a3,a18,a18),a18,a3,a3)),
% 60.06/60.16 inference(scs_inference,[],[4948,4965,5005,5066,4979,5127,5130,5133,5136,4957,4955,5100,4975,4995,5064,4967,4993,4814,4989,5001,5028,4880,4758,5007,5116,4874,5055,772,1574,932,1577,152,342,163,164,252,167,257,256,225,156,259,170,253,153,258,151,169,226,168,187,154,254,171,224,165,166,255,204])).
% 60.06/60.16 cnf(5195,plain,
% 60.06/60.16 (P8(x51951,x51952,x51953,x51954,x51952,x51951,x51953,x51954)),
% 60.06/60.16 inference(rename_variables,[],[4965])).
% 60.06/60.16 cnf(5198,plain,
% 60.06/60.16 (P1(x51981,x51982,x51981)),
% 60.06/60.16 inference(rename_variables,[],[4979])).
% 60.06/60.16 cnf(5200,plain,
% 60.06/60.16 (P5(a18,a18,a18,f4(a18,a18,a18))),
% 60.06/60.16 inference(scs_inference,[],[4948,4965,5005,5066,4979,5127,5130,5133,5136,4957,4955,5100,4975,4995,5064,4967,4993,4814,4989,5001,5028,5093,5105,4880,4758,5007,5116,4874,5055,4894,4734,772,1574,932,1577,152,342,163,164,252,167,257,256,225,156,259,170,253,153,258,151,169,226,168,187,154,254,171,224,165,166,255,204,249,198,188])).
% 60.06/60.16 cnf(5207,plain,
% 60.06/60.16 (P1(x52071,x52072,x52071)),
% 60.06/60.16 inference(rename_variables,[],[4979])).
% 60.06/60.16 cnf(5210,plain,
% 60.06/60.16 (P8(x52101,x52102,x52101,x52102,x52103,x52104,x52103,x52104)),
% 60.06/60.16 inference(rename_variables,[],[5005])).
% 60.06/60.16 cnf(5214,plain,
% 60.06/60.16 (P10(a3,a18,a1,a1)),
% 60.06/60.16 inference(scs_inference,[],[4948,4965,5195,5005,5066,4979,5127,5130,5133,5136,5198,4957,4955,5100,4975,4995,5064,4967,4993,4814,4953,4989,5001,5028,5093,5105,4880,4758,5007,5116,4874,5055,4894,4734,4725,772,1574,932,1577,152,342,163,164,252,167,257,256,225,156,259,170,253,153,258,151,169,226,168,187,154,254,171,224,165,166,255,204,249,198,188,199,200,197,247,203,240])).
% 60.06/60.16 cnf(5215,plain,
% 60.06/60.16 (P8(x52151,x52152,x52153,x52154,x52152,x52151,x52153,x52154)),
% 60.06/60.16 inference(rename_variables,[],[4965])).
% 60.06/60.16 cnf(5221,plain,
% 60.06/60.16 (P9(a18,f5(a18,a3,a18),a18,a3)),
% 60.06/60.16 inference(scs_inference,[],[4948,4965,5195,5005,5066,4979,5127,5130,5133,5136,5198,4957,4955,5100,4975,4995,5064,4967,4993,4814,4953,4989,5001,5028,5093,5105,4880,4758,5007,5116,4874,5055,4768,4894,4734,4725,772,1574,932,1577,152,342,163,164,252,167,257,256,225,156,259,170,253,153,258,151,169,226,168,187,154,254,171,224,165,166,255,204,249,198,188,199,200,197,247,203,240,178,173,189])).
% 60.06/60.16 cnf(5227,plain,
% 60.06/60.16 (P2(a18,a18,a18,a18)),
% 60.06/60.16 inference(scs_inference,[],[4948,4965,5195,5005,5066,4979,5127,5130,5133,5136,5198,4957,4955,5100,4975,4995,5064,4967,4993,4814,4953,4989,5001,5028,5093,5105,4880,4758,5007,5116,4874,5055,4768,4894,4734,4725,772,1574,932,1577,152,342,163,164,252,167,257,256,225,156,259,170,253,153,258,151,169,226,168,187,154,254,171,224,165,166,255,204,249,198,188,199,200,197,247,203,240,178,173,189,201,223,184])).
% 60.06/60.16 cnf(5237,plain,
% 60.06/60.16 (P5(a1,a2,a1,a2)),
% 60.06/60.16 inference(scs_inference,[],[4948,4965,5195,5005,5066,4979,5127,5130,5133,5136,5198,4957,4955,5100,4975,4995,5064,4967,4993,4814,4953,4987,4989,5001,5028,5093,5105,4880,4758,5007,5116,4874,5055,4768,4760,4894,4734,4725,4908,772,1574,932,1577,152,342,163,164,252,167,257,256,225,156,259,170,253,153,258,151,169,226,168,187,154,254,171,224,165,166,255,204,249,198,188,199,200,197,247,203,240,178,173,189,201,223,184,191,177,227,190,243])).
% 60.06/60.16 cnf(5239,plain,
% 60.06/60.16 (P9(a3,a1,a18,a18)),
% 60.06/60.16 inference(scs_inference,[],[4948,4965,5195,5215,5005,5066,4979,5127,5130,5133,5136,5198,4957,4955,5100,4975,4995,5064,4967,4993,4814,4953,4987,4989,5001,5028,5053,5093,5105,4880,4758,5007,5116,4874,5055,4768,4760,4894,4734,4725,4908,772,1574,932,1577,152,342,163,164,252,167,257,256,225,156,259,170,253,153,258,151,169,226,168,187,154,254,171,224,165,166,255,204,249,198,188,199,200,197,247,203,240,178,173,189,201,223,184,191,177,227,190,243,241])).
% 60.06/60.16 cnf(5240,plain,
% 60.06/60.16 (P8(x52401,x52402,x52403,x52404,x52402,x52401,x52403,x52404)),
% 60.06/60.16 inference(rename_variables,[],[4965])).
% 60.06/60.16 cnf(5245,plain,
% 60.06/60.16 (P4(a16,a16,a1,a2)),
% 60.06/60.16 inference(scs_inference,[],[142,4948,4965,5195,5215,5005,5210,5066,4979,5127,5130,5133,5136,5198,4957,4955,5100,4975,4995,5064,4967,4993,4814,4953,4987,4989,5001,5028,5053,5093,5105,4880,4758,5007,5116,4874,4959,5055,4768,4760,4894,4734,4725,4908,772,1574,932,1577,152,342,163,164,252,167,257,256,225,156,259,170,253,153,258,151,169,226,168,187,154,254,171,224,165,166,255,204,249,198,188,199,200,197,247,203,240,178,173,189,201,223,184,191,177,227,190,243,241,181,236])).
% 60.06/60.16 cnf(5246,plain,
% 60.06/60.16 (P8(x52461,x52462,x52461,x52462,x52463,x52464,x52463,x52464)),
% 60.06/60.16 inference(rename_variables,[],[5005])).
% 60.06/60.16 cnf(5248,plain,
% 60.06/60.16 (P3(a3,a1,a3)),
% 60.06/60.16 inference(scs_inference,[],[142,4948,4965,5195,5215,5005,5210,5066,4979,5127,5130,5133,5136,5198,5207,4957,4955,5100,4975,4995,5064,4967,4993,4814,4953,4987,4989,5001,5028,5053,5093,5105,4880,4758,5007,5116,4874,4959,5055,4768,4760,4897,4894,4734,4667,4725,4908,772,1574,932,1577,152,342,163,164,252,167,257,256,225,156,259,170,253,153,258,151,169,226,168,187,154,254,171,224,165,166,255,204,249,198,188,199,200,197,247,203,240,178,173,189,201,223,184,191,177,227,190,243,241,181,236,162])).
% 60.06/60.16 cnf(5249,plain,
% 60.06/60.16 (P1(x52491,x52492,x52491)),
% 60.06/60.16 inference(rename_variables,[],[4979])).
% 60.06/60.16 cnf(5251,plain,
% 60.06/60.16 (P3(a18,a18,a18)),
% 60.06/60.16 inference(scs_inference,[],[142,4948,4965,5195,5215,5005,5210,5246,5066,4979,5127,5130,5133,5136,5198,5207,4957,4955,5100,4975,4995,5064,4967,4993,4814,4953,4987,4989,5001,5028,5053,5093,5105,4880,4758,5007,5116,4874,4959,5055,4768,4760,4931,4897,4894,4734,4667,4725,4908,772,1574,932,1577,152,342,163,164,252,167,257,256,225,156,259,170,253,153,258,151,169,226,168,187,154,254,171,224,165,166,255,204,249,198,188,199,200,197,247,203,240,178,173,189,201,223,184,191,177,227,190,243,241,181,236,162,239])).
% 60.06/60.16 cnf(5255,plain,
% 60.06/60.16 (P3(f25(a3,x52551),x52551,a3)),
% 60.06/60.16 inference(rename_variables,[],[4991])).
% 60.06/60.16 cnf(5256,plain,
% 60.06/60.16 (P4(x52561,x52562,x52562,x52562)),
% 60.06/60.16 inference(rename_variables,[],[5066])).
% 60.06/60.16 cnf(5262,plain,
% 60.06/60.16 (P1(x52621,x52622,x52621)),
% 60.06/60.16 inference(rename_variables,[],[4979])).
% 60.06/60.16 cnf(5265,plain,
% 60.06/60.16 (P1(x52651,x52652,x52651)),
% 60.06/60.16 inference(rename_variables,[],[4979])).
% 60.06/60.16 cnf(5266,plain,
% 60.06/60.16 (P10(x52661,x52662,x52662,x52661)),
% 60.06/60.16 inference(rename_variables,[],[4810])).
% 60.06/60.16 cnf(5269,plain,
% 60.06/60.16 (P1(x52691,x52692,x52691)),
% 60.06/60.16 inference(rename_variables,[],[4979])).
% 60.06/60.16 cnf(5272,plain,
% 60.06/60.16 (P1(a1,a2,f14(a16,a2,a2,a16,a1,a2))),
% 60.06/60.16 inference(scs_inference,[],[142,4948,4965,5195,5215,5005,5210,5246,5066,4979,5127,5130,5133,5136,5198,5207,5249,5262,5265,5269,4957,4955,5100,4975,4995,5064,4967,4993,4814,4953,4963,4987,4989,5001,5028,5053,5093,5105,4880,4758,5007,5116,4874,4959,4991,5255,5055,4768,4760,4931,4897,4894,4734,4810,5266,4802,4663,4667,4725,4908,772,1574,932,1577,152,342,163,164,252,167,257,256,225,156,259,170,253,153,258,151,169,226,168,187,154,254,171,224,165,166,255,204,249,198,188,199,200,197,247,203,240,178,173,189,201,223,184,191,177,227,190,243,241,181,236,162,239,192,186,209,207,208,206])).
% 60.06/60.16 cnf(5276,plain,
% 60.06/60.16 (P3(f25(a18,x52761),a18,x52761)),
% 60.06/60.16 inference(scs_inference,[],[142,4948,4965,5195,5215,5005,5210,5246,5066,4979,5127,5130,5133,5136,5198,5207,5249,5262,5265,5269,4957,4955,5100,4975,4995,5064,4967,4993,4814,4953,4963,4987,4989,5001,5028,5053,5093,5105,4880,4758,5007,5116,4874,4959,4991,5255,5055,4768,4760,4931,4897,4894,4734,4810,5266,4802,4663,4667,4725,4908,772,1574,932,1577,152,342,163,164,252,167,257,256,225,156,259,170,253,153,258,151,169,226,168,187,154,254,171,224,165,166,255,204,249,198,188,199,200,197,247,203,240,178,173,189,201,223,184,191,177,227,190,243,241,181,236,162,239,192,186,209,207,208,206,159])).
% 60.06/60.16 cnf(5278,plain,
% 60.06/60.16 (P5(x52781,x52781,x52781,x52781)),
% 60.06/60.16 inference(scs_inference,[],[142,4948,4965,5195,5215,5240,5005,5210,5246,5066,5256,4979,5127,5130,5133,5136,5198,5207,5249,5262,5265,5269,4957,4955,5100,4975,4995,5064,4967,4993,4814,4953,4963,4987,4989,5001,5028,5053,5093,5105,4880,4758,5007,5116,4874,4959,4991,5255,5055,4768,4760,4931,4897,4894,4734,4810,5266,4802,4663,4667,4725,4908,772,1574,932,1577,152,342,163,164,252,167,257,256,225,156,259,170,253,153,258,151,169,226,168,187,154,254,171,224,165,166,255,204,249,198,188,199,200,197,247,203,240,178,173,189,201,223,184,191,177,227,190,243,241,181,236,162,239,192,186,209,207,208,206,159,251])).
% 60.06/60.16 cnf(5284,plain,
% 60.06/60.16 (P5(a3,a18,a18,a3)),
% 60.06/60.16 inference(scs_inference,[],[142,4948,4965,5195,5215,5240,5005,5210,5246,5066,5256,4979,5127,5130,5133,5136,5198,5207,5249,5262,5265,5269,4957,4955,5100,4975,4995,5064,4967,4993,4814,4953,4963,4987,4989,5001,5028,5053,5093,5105,4880,4758,5007,5116,4874,4959,4991,5255,5055,4768,4760,4931,4897,4894,4734,4810,5266,4802,4663,4667,4725,4908,772,1574,932,1577,152,342,163,164,252,167,257,256,225,156,259,170,253,153,258,151,169,226,168,187,154,254,171,224,165,166,255,204,249,198,188,199,200,197,247,203,240,178,173,189,201,223,184,191,177,227,190,243,241,181,236,162,239,192,186,209,207,208,206,159,251,1154])).
% 60.06/60.16 cnf(5294,plain,
% 60.06/60.16 (P8(a3,a18,a3,a3,a3,a3,a3,a3)),
% 60.06/60.16 inference(scs_inference,[],[142,4948,4965,5195,5215,5240,5005,5210,5246,5066,5256,4979,5127,5130,5133,5136,5198,5207,5249,5262,5265,5269,4957,4955,5100,4975,4995,5064,4967,4993,4814,4953,4963,4987,4989,5001,5028,5053,5093,5105,4880,4758,5007,5116,4874,4959,4991,5255,5055,4768,4760,4931,4897,4894,4734,4810,5266,4669,4878,4802,4663,4667,4725,4908,772,1574,932,1577,152,342,163,164,252,167,257,256,225,156,259,170,253,153,258,151,169,226,168,187,154,254,171,224,165,166,255,204,249,198,188,199,200,197,247,203,240,178,173,189,201,223,184,191,177,227,190,243,241,181,236,162,239,192,186,209,207,208,206,159,251,1154,233,1915,194,250,229])).
% 60.06/60.16 cnf(5298,plain,
% 60.06/60.16 (P9(a18,a18,a2,a2)),
% 60.06/60.16 inference(scs_inference,[],[142,4948,4965,5195,5215,5240,5005,5210,5246,5066,5256,4979,5127,5130,5133,5136,5198,5207,5249,5262,5265,5269,4957,4955,5100,4975,4995,5064,4967,4993,4814,4953,4963,4987,4989,5001,5028,5053,5093,5105,4880,4758,5007,5116,4874,4959,4991,5255,5055,4768,4760,4931,4897,4894,4734,4810,5266,4669,4878,4802,4663,4667,4725,4908,772,1574,932,1577,152,342,163,164,252,167,257,256,225,156,259,170,253,153,258,151,169,226,168,187,154,254,171,224,165,166,255,204,249,198,188,199,200,197,247,203,240,178,173,189,201,223,184,191,177,227,190,243,241,181,236,162,239,192,186,209,207,208,206,159,251,1154,233,1915,194,250,229,205,1531])).
% 60.06/60.16 cnf(5306,plain,
% 60.06/60.16 (P1(x53061,x53061,x53062)),
% 60.06/60.16 inference(rename_variables,[],[5138])).
% 60.06/60.16 cnf(5309,plain,
% 60.06/60.16 (P1(x53091,x53091,x53092)),
% 60.06/60.16 inference(rename_variables,[],[5138])).
% 60.06/60.16 cnf(5312,plain,
% 60.06/60.16 (P1(x53121,x53121,x53122)),
% 60.06/60.16 inference(rename_variables,[],[5138])).
% 60.06/60.16 cnf(5314,plain,
% 60.06/60.16 (P7(a3,a3,a3,a1,a3,a3,a3,a1)),
% 60.06/60.16 inference(scs_inference,[],[5138,5306,5309,5312,1574,772,1577,932])).
% 60.06/60.16 cnf(5315,plain,
% 60.06/60.16 (P1(x53151,x53151,x53152)),
% 60.06/60.16 inference(rename_variables,[],[5138])).
% 60.06/60.16 cnf(5319,plain,
% 60.06/60.16 (P10(a3,a18,a3,a3)),
% 60.06/60.16 inference(scs_inference,[],[5138,5306,5309,5312,5142,5294,1574,772,1577,932,342,233])).
% 60.06/60.16 cnf(5323,plain,
% 60.06/60.16 (P10(a1,a1,a3,a18)),
% 60.06/60.16 inference(scs_inference,[],[5138,5306,5309,5312,5142,5214,5294,5022,1574,772,1577,932,342,233,152,163])).
% 60.06/60.16 cnf(5327,plain,
% 60.06/60.16 (P8(x53271,x53272,a3,a3,x53271,x53272,x53273,x53273)),
% 60.06/60.16 inference(scs_inference,[],[5138,5306,5309,5312,5154,5142,5158,5214,5294,5022,1574,772,1577,932,342,233,152,163,256,253])).
% 60.06/60.16 cnf(5333,plain,
% 60.06/60.16 (P7(a18,a1,a18,a1,a1,a18,a18,a1)),
% 60.06/60.16 inference(scs_inference,[],[5138,5306,5309,5312,5126,5154,5142,5158,5214,5237,5294,5022,4961,1574,772,1577,932,342,233,152,163,256,253,226,164,258])).
% 60.06/60.16 cnf(5335,plain,
% 60.06/60.16 (P8(x53351,x53351,x53352,x53353,a3,a3,x53352,x53353)),
% 60.06/60.16 inference(scs_inference,[],[5138,5306,5309,5312,5126,5154,5142,5158,5214,5237,5294,5022,4961,1574,772,1577,932,342,233,152,163,256,253,226,164,258,225])).
% 60.06/60.16 cnf(5339,plain,
% 60.06/60.16 (P8(x53391,x53392,x53391,x53392,x53393,x53394,x53394,x53393)),
% 60.06/60.16 inference(scs_inference,[],[5180,5138,5306,5309,5312,5126,5154,5142,5158,5214,5237,5294,5112,5022,4961,1574,772,1577,932,342,233,152,163,256,253,226,164,258,225,151,252])).
% 60.06/60.16 cnf(5341,plain,
% 60.06/60.16 (P7(a1,a18,a1,a18,a18,a1,a18,a1)),
% 60.06/60.16 inference(scs_inference,[],[5180,5138,5306,5309,5312,5126,5154,5142,5158,5214,5237,5294,5112,5022,4961,1574,772,1577,932,342,233,152,163,256,253,226,164,258,225,151,252,259])).
% 60.06/60.16 cnf(5343,plain,
% 60.06/60.16 (P4(x53431,x53431,x53432,x53431)),
% 60.06/60.16 inference(scs_inference,[],[5170,5180,5138,5306,5309,5312,5126,5154,5142,5158,5214,5237,5294,5112,5022,4961,1574,772,1577,932,342,233,152,163,256,253,226,164,258,225,151,252,259,170])).
% 60.06/60.16 cnf(5349,plain,
% 60.06/60.16 (P1(f25(a1,x53491),a1,x53491)),
% 60.06/60.16 inference(scs_inference,[],[5170,5180,5138,5306,5309,5312,5126,5154,5142,5158,5174,5214,5237,5294,5112,5022,5096,4961,1574,772,1577,932,342,233,152,163,256,253,226,164,258,225,151,252,259,170,257,167,153])).
% 60.06/60.16 cnf(5353,plain,
% 60.06/60.16 (P5(a3,a18,a3,a18)),
% 60.06/60.16 inference(scs_inference,[],[5170,5180,5138,5306,5309,5312,5126,5154,5142,5158,5174,5214,5227,5237,5284,5294,5112,5022,5096,4961,1574,772,1577,932,342,233,152,163,256,253,226,164,258,225,151,252,259,170,257,167,153,187,168])).
% 60.06/60.16 cnf(5355,plain,
% 60.06/60.16 (P5(a3,a1,a3,a3)),
% 60.06/60.16 inference(scs_inference,[],[5170,5180,5138,5306,5309,5312,5126,5154,5248,5142,5158,5174,5214,5227,5237,5284,5294,5112,5022,5096,4961,1574,772,1577,932,342,233,152,163,256,253,226,164,258,225,151,252,259,170,257,167,153,187,168,156])).
% 60.06/60.16 cnf(5357,plain,
% 60.06/60.16 (P4(a16,x53571,a16,a2)),
% 60.06/60.16 inference(scs_inference,[],[5170,5180,5138,5306,5309,5312,5126,5154,5248,5142,4997,5158,5174,5214,5227,5237,5284,5294,5112,5022,5096,4961,1574,772,1577,932,342,233,152,163,256,253,226,164,258,225,151,252,259,170,257,167,153,187,168,156,169])).
% 60.06/60.16 cnf(5359,plain,
% 60.06/60.16 (P3(a3,a3,a1)),
% 60.06/60.16 inference(scs_inference,[],[5170,5180,5138,5306,5309,5312,5126,5154,5248,5142,4997,5158,5174,5214,5227,5237,5284,5294,5112,5022,5096,4961,1574,772,1577,932,342,233,152,163,256,253,226,164,258,225,151,252,259,170,257,167,153,187,168,156,169,154])).
% 60.06/60.16 cnf(5361,plain,
% 60.06/60.16 (P8(x53611,x53612,x53613,x53614,x53612,x53611,x53614,x53613)),
% 60.06/60.16 inference(scs_inference,[],[5162,5170,5180,5138,5306,5309,5312,5126,5154,5248,5142,4997,5158,5174,5214,5227,5237,5284,5294,5112,5022,5096,4961,1574,772,1577,932,342,233,152,163,256,253,226,164,258,225,151,252,259,170,257,167,153,187,168,156,169,154,254])).
% 60.06/60.16 cnf(5367,plain,
% 60.06/60.16 (P9(a3,a1,a16,a2)),
% 60.06/60.16 inference(scs_inference,[],[5162,5170,5180,5138,5306,5309,5312,5126,5154,5188,5245,5248,5142,4997,5158,5174,5214,5227,5237,5284,5294,5112,5022,5096,4961,1574,772,1577,932,342,233,152,163,256,253,226,164,258,225,151,252,259,170,257,167,153,187,168,156,169,154,254,171,224,165])).
% 60.06/60.16 cnf(5371,plain,
% 60.06/60.16 (P8(a3,a3,x53711,x53711,x53712,x53713,x53712,x53713)),
% 60.06/60.16 inference(scs_inference,[],[5162,5170,5180,5138,5306,5309,5312,5126,5154,5188,5245,5248,5142,4997,5158,5174,5214,5227,5237,5284,5294,5011,5112,5022,5096,4961,1574,772,1577,932,342,233,152,163,256,253,226,164,258,225,151,252,259,170,257,167,153,187,168,156,169,154,254,171,224,165,166,255])).
% 60.06/60.16 cnf(5374,plain,
% 60.06/60.16 (P1(x53741,x53741,x53742)),
% 60.06/60.16 inference(rename_variables,[],[5138])).
% 60.06/60.16 cnf(5377,plain,
% 60.06/60.16 (P8(x53771,x53772,x53772,x53771,x53773,x53774,x53773,x53774)),
% 60.06/60.16 inference(rename_variables,[],[5180])).
% 60.06/60.16 cnf(5381,plain,
% 60.06/60.16 (P3(f28(a1,a3,a1,a3,a3,a3),a1,a3)),
% 60.06/60.16 inference(scs_inference,[],[5162,5170,5180,5138,5306,5309,5312,5315,5126,5154,5188,5245,5248,5142,4997,5158,5174,5186,5214,5227,5237,5284,5294,5011,5112,5022,5096,4961,4725,1574,772,1577,932,342,233,152,163,256,253,226,164,258,225,151,252,259,170,257,167,153,187,168,156,169,154,254,171,224,165,166,255,198,250,204,203])).
% 60.06/60.16 cnf(5383,plain,
% 60.06/60.16 (P1(f26(a18,a18,a3,a1),a3,a1)),
% 60.06/60.16 inference(scs_inference,[],[5162,5170,5180,5138,5306,5309,5312,5315,5126,5154,5188,5239,5245,5248,5142,4997,5158,5174,5186,5214,5227,5237,5284,5294,5011,5112,5022,5096,4961,4725,1574,772,1577,932,342,233,152,163,256,253,226,164,258,225,151,252,259,170,257,167,153,187,168,156,169,154,254,171,224,165,166,255,198,250,204,203,194])).
% 60.06/60.16 cnf(5386,plain,
% 60.06/60.16 (P5(x53861,x53861,x53861,x53861)),
% 60.06/60.16 inference(rename_variables,[],[5278])).
% 60.06/60.16 cnf(5394,plain,
% 60.06/60.16 (P1(f13(a3,a18,a18,a18,x53941),a18,x53941)),
% 60.06/60.16 inference(scs_inference,[],[5278,5162,5170,5180,5138,5306,5309,5312,5315,5374,5126,5154,5188,5239,5245,5248,5251,5142,4997,5158,5174,5186,5214,5227,5237,5284,5294,5011,5112,5022,5096,4961,4675,5100,4725,1574,772,1577,932,342,233,152,163,256,253,226,164,258,225,151,252,259,170,257,167,153,187,168,156,169,154,254,171,224,165,166,255,198,250,204,203,194,200,199,205,178,197])).
% 60.06/60.16 cnf(5395,plain,
% 60.06/60.16 (P1(x53951,x53951,x53952)),
% 60.06/60.16 inference(rename_variables,[],[5138])).
% 60.06/60.16 cnf(5400,plain,
% 60.06/60.16 (P8(x54001,x54002,x54001,x54002,x54003,x54004,x54003,x54004)),
% 60.06/60.16 inference(rename_variables,[],[5005])).
% 60.06/60.16 cnf(5402,plain,
% 60.06/60.16 (P10(x54021,x54021,a18,a18)),
% 60.06/60.16 inference(scs_inference,[],[5278,5162,5170,5180,5138,5306,5309,5312,5315,5374,5126,5154,5188,5239,5245,5248,5251,5142,4997,5158,5174,5186,5214,5227,5237,5284,5294,5011,5112,5022,5096,4961,5221,4995,4675,5005,5100,4725,1574,772,1577,932,342,233,152,163,256,253,226,164,258,225,151,252,259,170,257,167,153,187,168,156,169,154,254,171,224,165,166,255,198,250,204,203,194,200,199,205,178,197,189,247,240])).
% 60.06/60.16 cnf(5408,plain,
% 60.06/60.16 (P5(x54081,x54081,x54081,x54081)),
% 60.06/60.16 inference(rename_variables,[],[5278])).
% 60.06/60.16 cnf(5413,plain,
% 60.06/60.16 (P2(x54131,x54131,x54131,x54131)),
% 60.06/60.16 inference(scs_inference,[],[5278,5386,5408,5162,5170,5180,5138,5306,5309,5312,5315,5374,5126,5154,5188,5239,5245,5248,5251,5142,4997,5158,5174,5186,5214,5227,5237,5284,5294,5011,5112,5022,5096,4961,5176,5221,5070,4995,4675,5005,5066,5100,4725,1574,772,1577,932,342,233,152,163,256,253,226,164,258,225,151,252,259,170,257,167,153,187,168,156,169,154,254,171,224,165,166,255,198,250,204,203,194,200,199,205,178,197,189,247,240,173,201,191,184])).
% 60.06/60.16 cnf(5417,plain,
% 60.06/60.16 (~P4(a16,a19,a16,a17)),
% 60.06/60.16 inference(scs_inference,[],[5278,5386,5408,5162,5170,5180,5138,5306,5309,5312,5315,5374,5126,5154,5188,5239,5245,5248,5251,5142,4997,5158,5174,5186,5214,5227,5237,5284,5294,5011,5112,5022,5096,4961,5176,5221,5070,4995,4675,372,5005,5066,5100,4725,1574,772,1577,932,342,233,152,163,256,253,226,164,258,225,151,252,259,170,257,167,153,187,168,156,169,154,254,171,224,165,166,255,198,250,204,203,194,200,199,205,178,197,189,247,240,173,201,191,184,223,185])).
% 60.06/60.16 cnf(5427,plain,
% 60.06/60.16 (P9(x54271,x54272,x54272,x54271)),
% 60.06/60.16 inference(scs_inference,[],[5278,5386,5408,5162,5170,5180,5377,5138,5306,5309,5312,5315,5374,5126,5154,5188,5239,5245,5248,5251,5142,4997,5158,5174,5186,5214,5227,5237,5284,5294,4937,5011,5112,5022,5096,5178,4961,5176,5221,5070,4995,4675,372,5005,5066,4894,5100,4725,5105,1574,772,1577,932,342,233,152,163,256,253,226,164,258,225,151,252,259,170,257,167,153,187,168,156,169,154,254,171,224,165,166,255,198,250,204,203,194,200,199,205,178,197,189,247,240,173,201,191,184,223,185,177,227,190,181,241])).
% 60.06/60.16 cnf(5430,plain,
% 60.06/60.16 (P4(x54301,x54302,x54303,x54303)),
% 60.06/60.16 inference(scs_inference,[],[5278,5386,5408,5162,5170,5180,5377,5138,5306,5309,5312,5315,5374,5395,5126,5154,5188,5239,5245,5248,5251,5142,4997,5158,5174,5186,5214,5227,5237,5284,5294,4937,5011,5112,5022,5096,5178,4961,5176,5221,5070,4995,4675,372,5005,5066,4828,4894,5100,4725,5105,1574,772,1577,932,342,233,152,163,256,253,226,164,258,225,151,252,259,170,257,167,153,187,168,156,169,154,254,171,224,165,166,255,198,250,204,203,194,200,199,205,178,197,189,247,240,173,201,191,184,223,185,177,227,190,181,241,236])).
% 60.06/60.16 cnf(5433,plain,
% 60.06/60.16 (P9(a2,a1,a1,a1)),
% 60.06/60.16 inference(scs_inference,[],[5278,5386,5408,5162,5170,5180,5377,5138,5306,5309,5312,5315,5374,5395,5126,5154,5188,5239,5245,5248,5251,5142,4997,5158,5174,5186,5214,5227,5237,5284,5294,4937,5011,5112,5022,5096,5178,4961,5176,5221,5070,4995,4675,372,5005,5066,4828,4894,5100,4725,5105,1574,772,1577,932,342,233,152,163,256,253,226,164,258,225,151,252,259,170,257,167,153,187,168,156,169,154,254,171,224,165,166,255,198,250,204,203,194,200,199,205,178,197,189,247,240,173,201,191,184,223,185,177,227,190,181,241,236,195])).
% 60.06/60.16 cnf(5437,plain,
% 60.06/60.16 (P10(x54371,x54371,a3,a3)),
% 60.06/60.16 inference(rename_variables,[],[5142])).
% 60.06/60.16 cnf(5439,plain,
% 60.06/60.16 (P1(f31(a1,a3,a1,a3,a3,a3),a1,a3)),
% 60.06/60.16 inference(scs_inference,[],[5278,5386,5408,5162,5170,5180,5377,5138,5306,5309,5312,5315,5374,5395,5126,5154,5188,5239,5245,5248,5251,5142,5437,4997,5158,5174,5186,5214,5227,5237,5284,5294,4937,5011,5112,5022,5096,5178,4961,5176,5221,5070,4995,4675,372,5005,5066,4806,4828,4894,5100,4725,5105,1574,772,1577,932,342,233,152,163,256,253,226,164,258,225,151,252,259,170,257,167,153,187,168,156,169,154,254,171,224,165,166,255,198,250,204,203,194,200,199,205,178,197,189,247,240,173,201,191,184,223,185,177,227,190,181,241,236,195,192,209])).
% 60.06/60.16 cnf(5445,plain,
% 60.06/60.16 (P10(x54451,x54452,x54452,x54451)),
% 60.06/60.16 inference(rename_variables,[],[4810])).
% 60.06/60.16 cnf(5446,plain,
% 60.06/60.16 (P1(x54461,x54462,x54461)),
% 60.06/60.16 inference(rename_variables,[],[4979])).
% 60.06/60.16 cnf(5455,plain,
% 60.06/60.16 (P5(a16,a16,a2,a2)),
% 60.06/60.16 inference(scs_inference,[],[5278,5386,5408,5162,5170,5180,5377,5138,5306,5309,5312,5315,5374,5395,4661,5126,5154,5188,5239,5245,5248,5251,5142,5437,4997,5158,5174,5186,5214,5227,5237,5284,5294,4937,5011,5112,5022,5096,5178,4961,5176,5221,4808,5070,4979,5446,4995,4675,372,5005,5400,5066,4806,4828,4810,5445,4894,5100,4695,970,4725,5105,145,1574,772,1577,932,342,233,152,163,256,253,226,164,258,225,151,252,259,170,257,167,153,187,168,156,169,154,254,171,224,165,166,255,198,250,204,203,194,200,199,205,178,197,189,247,240,173,201,191,184,223,185,177,227,190,181,241,236,195,192,209,207,208,206,251])).
% 60.06/60.16 cnf(5458,plain,
% 60.06/60.16 (P10(a3,a1,a2,a16)),
% 60.06/60.16 inference(scs_inference,[],[5278,5386,5408,5162,5170,5180,5377,5138,5306,5309,5312,5315,5374,5395,4661,5126,5154,5188,5239,5245,5248,5251,5142,5437,4997,5158,5174,5186,5214,5227,5237,5284,5294,4937,5011,5112,5022,5096,5178,4961,5176,5221,4808,5070,4979,5446,4995,4675,372,5005,5400,5066,4806,4828,4810,5445,4894,5100,4695,970,4725,5105,145,1574,772,1577,932,342,233,152,163,256,253,226,164,258,225,151,252,259,170,257,167,153,187,168,156,169,154,254,171,224,165,166,255,198,250,204,203,194,200,199,205,178,197,189,247,240,173,201,191,184,223,185,177,227,190,181,241,236,195,192,209,207,208,206,251,397])).
% 60.06/60.16 cnf(5462,plain,
% 60.06/60.16 (P10(f28(a18,a18,a18,a18,a18,a18),a18,a3,a3)),
% 60.06/60.16 inference(scs_inference,[],[5278,5386,5408,5162,5170,5180,5377,5138,5306,5309,5312,5315,5374,5395,4661,5126,5154,5188,5239,5245,5248,5251,5142,5437,4997,5158,5174,5186,5214,5227,5237,5284,5294,4937,5011,5112,5022,5096,5178,4961,5176,5221,4808,5070,4979,5446,4995,4675,372,5005,5400,5066,4806,4828,4810,5445,4894,5100,4695,970,4725,5105,145,1574,772,1577,932,342,233,152,163,256,253,226,164,258,225,151,252,259,170,257,167,153,187,168,156,169,154,254,171,224,165,166,255,198,250,204,203,194,200,199,205,178,197,189,247,240,173,201,191,184,223,185,177,227,190,181,241,236,195,192,209,207,208,206,251,397,420,1478])).
% 60.06/60.16 cnf(5464,plain,
% 60.06/60.16 (~P9(a2,a1,a1,a2)+P1(a2,a1,f4(a2,a2,a1))),
% 60.06/60.16 inference(scs_inference,[],[5278,5386,5408,5162,5170,5180,5377,5138,5306,5309,5312,5315,5374,5395,4661,5126,5154,5188,5239,5245,5248,5251,5142,5437,4997,5158,5174,5186,5214,5227,5237,5284,5294,4937,5011,5112,5022,5096,5178,4961,5176,5221,4808,5070,4979,5446,4995,4675,372,5005,5400,5066,4806,4828,4810,5445,4894,5100,4695,970,4725,5105,145,1574,772,1577,932,342,233,152,163,256,253,226,164,258,225,151,252,259,170,257,167,153,187,168,156,169,154,254,171,224,165,166,255,198,250,204,203,194,200,199,205,178,197,189,247,240,173,201,191,184,223,185,177,227,190,181,241,236,195,192,209,207,208,206,251,397,420,1478,176])).
% 60.06/60.16 cnf(5478,plain,
% 60.06/60.16 (P9(x54781,x54782,x54782,x54781)),
% 60.06/60.16 inference(rename_variables,[],[5427])).
% 60.06/60.16 cnf(5483,plain,
% 60.06/60.16 (P1(f13(a3,a18,a18,a18,x54831),a18,x54831)),
% 60.06/60.16 inference(rename_variables,[],[5394])).
% 60.06/60.16 cnf(5492,plain,
% 60.06/60.16 (P8(x54921,x54922,x54923,x54923,x54921,x54922,a3,a3)),
% 60.06/60.16 inference(scs_inference,[],[5427,5335,5192,5349,5394,5483,5383,5464,1574,772,1577,932,342,253])).
% 60.06/60.16 cnf(5494,plain,
% 60.06/60.16 (P10(a3,a1,a16,a2)),
% 60.06/60.16 inference(scs_inference,[],[5427,5335,5458,5192,5349,5394,5483,5383,5464,1574,772,1577,932,342,253,164])).
% 60.06/60.16 cnf(5506,plain,
% 60.06/60.16 (P5(a3,a3,a3,a1)),
% 60.06/60.16 inference(scs_inference,[],[5427,5314,5319,5335,5458,5333,5355,5192,5272,5349,5394,5483,5383,5464,1574,772,1577,932,342,253,164,163,152,225,256,257,167])).
% 60.06/60.16 cnf(5516,plain,
% 60.06/60.16 (P8(a3,a18,a18,a18,a18,a18,a3,a18)),
% 60.06/60.16 inference(scs_inference,[],[5427,5353,5129,5314,5319,5335,5458,5333,5355,5192,5200,5272,5276,5349,5394,5483,5383,5464,1574,772,1577,932,342,253,164,163,152,225,256,257,167,258,156,168,151,226])).
% 60.06/60.16 cnf(5520,plain,
% 60.06/60.16 (P1(f25(a18,x55201),a18,x55201)),
% 60.06/60.16 inference(scs_inference,[],[5427,5353,5129,5314,5319,5335,5458,5333,5355,5192,5200,5272,5276,5349,5394,5483,5383,5464,1574,772,1577,932,342,253,164,163,152,225,256,257,167,258,156,168,151,226,259,153])).
% 60.06/60.16 cnf(5524,plain,
% 60.06/60.16 (P4(x55241,x55242,x55243,x55242)),
% 60.06/60.16 inference(scs_inference,[],[5427,5430,5353,5129,5314,5319,5335,5371,5458,5333,5355,5192,5200,5272,5276,5349,5394,5483,5383,5464,1574,772,1577,932,342,253,164,163,152,225,256,257,167,258,156,168,151,226,259,153,252,170])).
% 60.06/60.16 cnf(5532,plain,
% 60.06/60.16 (P3(f25(a18,x55321),x55321,a18)),
% 60.06/60.16 inference(scs_inference,[],[5413,5339,5427,5430,5353,5129,5314,5319,5335,5371,5458,5160,5333,5355,5192,5200,5272,5276,5349,5394,5483,5383,5464,1574,772,1577,932,342,253,164,163,152,225,256,257,167,258,156,168,151,226,259,153,252,170,187,254,169,154])).
% 60.06/60.16 cnf(5534,plain,
% 60.06/60.16 (P4(x55341,x55341,x55341,x55342)),
% 60.06/60.16 inference(scs_inference,[],[5413,5339,5343,5427,5430,5353,5129,5314,5319,5335,5371,5458,5160,5333,5355,5192,5200,5272,5276,5349,5394,5483,5383,5464,1574,772,1577,932,342,253,164,163,152,225,256,257,167,258,156,168,151,226,259,153,252,170,187,254,169,154,171])).
% 60.06/60.16 cnf(5540,plain,
% 60.06/60.16 (P9(x55401,x55402,x55401,x55402)),
% 60.06/60.16 inference(scs_inference,[],[5413,5339,5343,5427,5478,5430,5353,5298,5129,5314,5319,5335,5371,5458,5160,5333,5355,5192,5200,5272,5276,5349,5394,5483,5383,5464,1574,772,1577,932,342,253,164,163,152,225,256,257,167,258,156,168,151,226,259,153,252,170,187,254,169,154,171,224,165,166])).
% 60.06/60.16 cnf(5542,plain,
% 60.06/60.16 (P8(x55421,x55421,a3,a3,x55422,x55423,x55422,x55423)),
% 60.06/60.16 inference(scs_inference,[],[5413,5339,5343,5427,5478,5430,5353,5298,5129,5314,5319,5335,5371,5458,5160,5333,5355,5192,5200,5272,5276,5349,5394,5483,5383,5464,1574,772,1577,932,342,253,164,163,152,225,256,257,167,258,156,168,151,226,259,153,252,170,187,254,169,154,171,224,165,166,255])).
% 60.06/60.16 cnf(5545,plain,
% 60.06/60.16 (P9(x55451,x55452,x55452,x55451)),
% 60.06/60.16 inference(rename_variables,[],[5427])).
% 60.06/60.16 cnf(5548,plain,
% 60.06/60.16 (P9(x55481,x55482,x55482,x55481)),
% 60.06/60.16 inference(rename_variables,[],[5427])).
% 60.06/60.16 cnf(5551,plain,
% 60.06/60.16 (P9(x55511,x55512,x55512,x55511)),
% 60.06/60.16 inference(rename_variables,[],[5427])).
% 60.06/60.16 cnf(5557,plain,
% 60.06/60.16 (P9(x55571,x55572,x55572,x55571)),
% 60.06/60.16 inference(rename_variables,[],[5427])).
% 60.06/60.16 cnf(5562,plain,
% 60.06/60.16 (P9(x55621,x55622,x55622,x55621)),
% 60.06/60.16 inference(rename_variables,[],[5427])).
% 60.06/60.16 cnf(5569,plain,
% 60.06/60.16 (P9(x55691,x55692,x55692,x55691)),
% 60.06/60.16 inference(rename_variables,[],[5427])).
% 60.06/60.16 cnf(5573,plain,
% 60.06/60.16 (P5(a1,a3,a1,a1)),
% 60.06/60.16 inference(scs_inference,[],[142,5413,5339,5343,5427,5478,5545,5548,5551,5557,5562,5569,5430,4892,5353,5298,5129,5314,5319,5335,5371,5458,5359,5160,5333,5355,5192,5200,5272,5276,5349,5394,5483,5383,5180,4802,5464,1574,772,1577,932,342,253,164,163,152,225,256,257,167,258,156,168,151,226,259,153,252,170,187,254,169,154,171,224,165,166,255,198,176,188,249,200,248,199,204,203,178,205,173])).
% 60.06/60.16 cnf(5574,plain,
% 60.06/60.16 (P9(x55741,x55742,x55742,x55741)),
% 60.06/60.16 inference(rename_variables,[],[5427])).
% 60.06/60.16 cnf(5576,plain,
% 60.06/60.16 (P1(f26(a1,a3,a3,a1),a3,a1)),
% 60.06/60.16 inference(scs_inference,[],[142,5413,5339,5343,5427,5478,5545,5548,5551,5557,5562,5569,5574,5430,4892,5353,5298,5129,5314,5319,5335,5371,5458,5359,5160,5333,5355,5192,5200,5272,5276,5349,5394,5483,5383,5180,4802,5464,1574,772,1577,932,342,253,164,163,152,225,256,257,167,258,156,168,151,226,259,153,252,170,187,254,169,154,171,224,165,166,255,198,176,188,249,200,248,199,204,203,178,205,173,194])).
% 60.06/60.16 cnf(5577,plain,
% 60.06/60.16 (P9(x55771,x55772,x55772,x55771)),
% 60.06/60.16 inference(rename_variables,[],[5427])).
% 60.06/60.16 cnf(5579,plain,
% 60.06/60.16 (P10(f30(a3,x55791,a18,a18,a3),a18,a3,x55791)),
% 60.06/60.16 inference(scs_inference,[],[142,5413,5339,5343,5427,5478,5545,5548,5551,5557,5562,5569,5574,5577,5430,4892,5353,5298,5129,5314,5319,5335,5371,5458,5359,5160,5333,5355,5192,5200,5272,5276,5349,5394,5483,5383,5180,4802,5464,1574,772,1577,932,342,253,164,163,152,225,256,257,167,258,156,168,151,226,259,153,252,170,187,254,169,154,171,224,165,166,255,198,176,188,249,200,248,199,204,203,178,205,173,194,201])).
% 60.06/60.16 cnf(5580,plain,
% 60.06/60.16 (P9(x55801,x55802,x55802,x55801)),
% 60.06/60.16 inference(rename_variables,[],[5427])).
% 60.06/60.16 cnf(5583,plain,
% 60.06/60.16 (P8(x55831,x55832,x55831,x55832,x55833,x55834,x55833,x55834)),
% 60.06/60.16 inference(rename_variables,[],[5005])).
% 60.06/60.16 cnf(5587,plain,
% 60.06/60.16 (P9(x55871,x55872,x55872,x55871)),
% 60.06/60.16 inference(rename_variables,[],[5427])).
% 60.06/60.16 cnf(5590,plain,
% 60.06/60.17 (P9(x55901,x55902,x55902,x55901)),
% 60.06/60.17 inference(rename_variables,[],[5427])).
% 60.06/60.17 cnf(5593,plain,
% 60.06/60.17 (P8(x55931,x55932,x55933,x55934,x55932,x55931,x55934,x55933)),
% 60.06/60.17 inference(rename_variables,[],[5361])).
% 60.06/60.17 cnf(5597,plain,
% 60.06/60.17 (P2(f9(x55971,x55971,x55972),x55971,x55971,x55972)),
% 60.06/60.17 inference(scs_inference,[],[142,5413,5339,5343,5361,5427,5478,5545,5548,5551,5557,5562,5569,5574,5577,5580,5587,5590,5430,4892,5353,5298,5129,5314,5319,5335,5371,5458,5359,5160,5333,5355,5433,5192,5200,5272,5276,5349,5394,5483,5383,5180,5005,4802,5464,1574,772,1577,932,342,253,164,163,152,225,256,257,167,258,156,168,151,226,259,153,252,170,187,254,169,154,171,224,165,166,255,198,176,188,249,200,248,199,204,203,178,205,173,194,201,247,189,197,240,223,191])).
% 60.06/60.17 cnf(5598,plain,
% 60.06/60.17 (P9(x55981,x55982,x55982,x55981)),
% 60.06/60.17 inference(rename_variables,[],[5427])).
% 60.06/60.17 cnf(5600,plain,
% 60.06/60.17 (P2(a3,a18,a18,a18)),
% 60.06/60.17 inference(scs_inference,[],[142,5413,5339,5343,5361,5427,5478,5545,5548,5551,5557,5562,5569,5574,5577,5580,5587,5590,5430,4892,5353,5298,5129,5314,5319,5335,5371,5458,5359,5160,5333,5355,5433,5192,5200,5272,5276,5349,5394,5483,5383,5180,5005,4802,5464,1574,772,1577,932,342,253,164,163,152,225,256,257,167,258,156,168,151,226,259,153,252,170,187,254,169,154,171,224,165,166,255,198,176,188,249,200,248,199,204,203,178,205,173,194,201,247,189,197,240,223,191,184])).
% 60.06/60.17 cnf(5602,plain,
% 60.06/60.17 (~P4(a16,a16,a19,a17)),
% 60.06/60.17 inference(scs_inference,[],[142,5413,5339,5343,5361,5427,5478,5545,5548,5551,5557,5562,5569,5574,5577,5580,5587,5590,5430,4892,5353,5298,5129,5314,5319,5335,5371,5458,5359,5160,5333,5355,5417,5433,5192,5200,5272,5276,5349,5394,5483,5383,5180,5005,4802,5464,1574,772,1577,932,342,253,164,163,152,225,256,257,167,258,156,168,151,226,259,153,252,170,187,254,169,154,171,224,165,166,255,198,176,188,249,200,248,199,204,203,178,205,173,194,201,247,189,197,240,223,191,184,185])).
% 60.06/60.17 cnf(5603,plain,
% 60.06/60.17 (P4(x56031,x56031,x56032,x56031)),
% 60.06/60.17 inference(rename_variables,[],[5343])).
% 60.06/60.17 cnf(5608,plain,
% 60.06/60.17 (P9(x56081,x56082,x56082,x56081)),
% 60.06/60.17 inference(rename_variables,[],[5427])).
% 60.06/60.17 cnf(5617,plain,
% 60.06/60.17 (P9(a1,a2,a1,a1)),
% 60.06/60.17 inference(scs_inference,[],[142,5413,5339,5343,5361,5593,5427,5478,5545,5548,5551,5557,5562,5569,5574,5577,5580,5587,5590,5598,5608,5430,4892,5353,5298,5129,5314,5319,5335,5371,5458,5359,5160,5333,5355,5417,5433,5192,5200,5272,5276,5349,5394,5483,5026,5383,4937,5180,5005,4802,5464,1574,772,1577,932,342,253,164,163,152,225,256,257,167,258,156,168,151,226,259,153,252,170,187,254,169,154,171,224,165,166,255,198,176,188,249,200,248,199,204,203,178,205,173,194,201,247,189,197,240,223,191,184,185,227,182,100,190,181,241])).
% 60.06/60.17 cnf(5621,plain,
% 60.06/60.17 (P8(x56211,x56212,x56211,x56212,x56213,x56214,x56213,x56214)),
% 60.06/60.17 inference(rename_variables,[],[5005])).
% 60.06/60.17 cnf(5623,plain,
% 60.06/60.17 (P3(x56231,x56231,x56231)),
% 60.06/60.17 inference(scs_inference,[],[142,5413,5339,5343,5361,5593,5427,5478,5545,5548,5551,5557,5562,5569,5574,5577,5580,5587,5590,5598,5608,5430,4892,5353,5298,5129,5314,5319,5335,5371,5458,4951,5359,5160,5333,5355,5417,5433,5192,5200,5272,5276,5349,5394,5483,5026,5383,5138,4937,5180,5005,5583,4802,5464,1574,772,1577,932,342,253,164,163,152,225,256,257,167,258,156,168,151,226,259,153,252,170,187,254,169,154,171,224,165,166,255,198,176,188,249,200,248,199,204,203,178,205,173,194,201,247,189,197,240,223,191,184,185,227,182,100,190,181,241,236,239])).
% 60.06/60.17 cnf(5625,plain,
% 60.06/60.17 (P8(x56251,x56252,x56251,x56252,x56253,x56254,x56254,x56253)),
% 60.06/60.17 inference(rename_variables,[],[5339])).
% 60.06/60.17 cnf(5626,plain,
% 60.06/60.17 (P1(x56261,x56261,x56262)),
% 60.06/60.17 inference(rename_variables,[],[5138])).
% 60.06/60.17 cnf(5630,plain,
% 60.06/60.17 (P3(f25(a18,x56301),a18,x56301)),
% 60.06/60.17 inference(rename_variables,[],[5276])).
% 60.06/60.17 cnf(5641,plain,
% 60.06/60.17 (P5(a2,a16,a2,a16)),
% 60.06/60.17 inference(scs_inference,[],[142,5413,5339,5343,5603,5361,5593,5427,5478,5545,5548,5551,5557,5562,5569,5574,5577,5580,5587,5590,5598,5608,5430,4892,5353,5298,5129,5314,5319,5335,5371,5458,4951,5359,5402,5160,5182,5333,5355,5417,5433,5192,5200,5272,5276,5630,5349,5394,5483,5026,5383,5138,4937,4808,5180,4979,5214,4963,5005,5583,4802,4948,5464,1574,772,1577,932,342,253,164,163,152,225,256,257,167,258,156,168,151,226,259,153,252,170,187,254,169,154,171,224,165,166,255,198,176,188,249,200,248,199,204,203,178,205,173,194,201,247,189,197,240,223,191,184,185,227,182,100,190,181,241,236,239,192,186,209,208,251])).
% 60.06/60.17 cnf(5654,plain,
% 60.06/60.17 (P8(x56541,x56541,a3,a3,x56542,x56543,x56543,x56542)),
% 60.06/60.17 inference(scs_inference,[],[142,5413,5339,5625,5343,5603,5361,5593,5427,5478,5545,5548,5551,5557,5562,5569,5574,5577,5580,5587,5590,5598,5608,5430,4892,5353,5298,5129,5314,5319,5327,5335,5371,5458,4951,5359,5402,5160,5182,5333,5355,5417,5433,5192,5200,5272,5276,5630,5349,5394,5483,5026,5383,5138,5626,4937,4808,5180,4979,5214,4963,5005,5583,4810,4802,4663,970,4948,5464,1574,772,1577,932,342,253,164,163,152,225,256,257,167,258,156,168,151,226,259,153,252,170,187,254,169,154,171,224,165,166,255,198,176,188,249,200,248,199,204,203,178,205,173,194,201,247,189,197,240,223,191,184,185,227,182,100,190,181,241,236,239,192,186,209,208,251,207,206,397,2,262])).
% 60.06/60.17 cnf(5658,plain,
% 60.06/60.17 (P1(a19,a17,a16)),
% 60.06/60.17 inference(scs_inference,[],[142,5413,5339,5625,5343,5603,5361,5593,5427,5478,5545,5548,5551,5557,5562,5569,5574,5577,5580,5587,5590,5598,5608,5430,4892,5353,5298,5129,5314,5319,5327,5335,5371,5458,4951,5359,5402,5160,5182,5333,5355,5417,5433,5192,5200,5272,5276,5630,5349,5394,5483,5026,5383,5138,5626,4937,4808,5180,4979,5214,4963,5005,5583,5621,4810,4802,4663,970,4948,5464,1574,772,1577,932,342,253,164,163,152,225,256,257,167,258,156,168,151,226,259,153,252,170,187,254,169,154,171,224,165,166,255,198,176,188,249,200,248,199,204,203,178,205,173,194,201,247,189,197,240,223,191,184,185,227,182,100,190,181,241,236,239,192,186,209,208,251,207,206,397,2,262,234])).
% 60.06/60.17 cnf(5681,plain,
% 60.06/60.17 (P1(f25(a18,x56811),a18,x56811)),
% 60.06/60.17 inference(rename_variables,[],[5520])).
% 60.06/60.17 cnf(5733,plain,
% 60.06/60.17 (P4(x57331,x57332,x57332,x57333)),
% 60.06/60.17 inference(scs_inference,[],[5524,5132,5516,5506,5542,5600,5658,5357,5135,5323,5341,5455,5494,5520,5681,5532,5579,5381,5576,5439,1574,772,1577,932,342,152,256,164,167,253,163,257,226,259,258,170,225,156,153,168,151,187,252,154,169,254,171])).
% 60.06/60.17 cnf(5746,plain,
% 60.06/60.17 (P9(x57461,x57462,x57461,x57462)),
% 60.06/60.17 inference(rename_variables,[],[5540])).
% 60.06/60.17 cnf(5751,plain,
% 60.06/60.17 (P9(x57511,x57512,x57511,x57512)),
% 60.06/60.17 inference(rename_variables,[],[5540])).
% 60.06/60.17 cnf(5754,plain,
% 60.06/60.17 (P9(x57541,x57542,x57541,x57542)),
% 60.06/60.17 inference(rename_variables,[],[5540])).
% 60.06/60.17 cnf(5761,plain,
% 60.06/60.17 (P9(x57611,x57612,x57611,x57612)),
% 60.06/60.17 inference(rename_variables,[],[5540])).
% 60.06/60.17 cnf(5769,plain,
% 60.06/60.17 (P9(x57691,x57692,x57691,x57692)),
% 60.06/60.17 inference(rename_variables,[],[5540])).
% 60.06/60.17 cnf(5772,plain,
% 60.06/60.17 (P9(x57721,x57722,x57721,x57722)),
% 60.06/60.17 inference(rename_variables,[],[5540])).
% 60.06/60.17 cnf(5775,plain,
% 60.06/60.17 (P9(x57751,x57752,x57751,x57752)),
% 60.06/60.17 inference(rename_variables,[],[5540])).
% 60.06/60.17 cnf(5784,plain,
% 60.06/60.17 (P9(x57841,x57842,x57841,x57842)),
% 60.06/60.17 inference(rename_variables,[],[5540])).
% 60.06/60.17 cnf(5789,plain,
% 60.06/60.17 (P8(x57891,x57892,x57893,x57893,x57891,x57892,a3,a3)),
% 60.06/60.17 inference(rename_variables,[],[5492])).
% 60.06/60.17 cnf(5792,plain,
% 60.06/60.17 (P9(x57921,x57922,x57921,x57922)),
% 60.06/60.17 inference(rename_variables,[],[5540])).
% 60.06/60.17 cnf(5812,plain,
% 60.06/60.17 (~P4(a16,a16,a16,a17)),
% 60.06/60.17 inference(scs_inference,[],[142,5623,5534,5540,5746,5751,5754,5761,5769,5772,5775,5784,5792,5524,5132,5516,5492,5789,5506,5542,5600,5617,5654,5658,5357,4971,5135,5323,5341,5367,5455,5494,5573,5602,5641,5597,5462,5520,5681,5532,5579,5381,5576,5439,5278,5427,5433,418,4979,5248,4802,1574,772,1577,932,342,152,256,164,167,253,163,257,226,259,258,170,225,156,153,168,151,187,252,154,169,254,171,224,165,166,255,198,246,248,199,188,249,203,250,204,176,200,193,201,247,245,178,173,189,240,194,197,184,223,99,161,242,158,185])).
% 60.06/60.17 cnf(5908,plain,
% 60.06/60.17 ($false),
% 60.06/60.17 inference(scs_inference,[],[5733,5812]),
% 60.06/60.17 ['proof']).
% 60.06/60.17 % SZS output end Proof
% 60.06/60.17 % Total time :59.430000s
%------------------------------------------------------------------------------