%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : GEO554+1 : TPTP v8.2.0. Released v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% Computer : n017.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:42 EDT 2024
% Result : Theorem 59.88s 59.91s
% Output : CNFRefutation 59.88s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.04/0.13 % Problem : GEO554+1 : TPTP v8.2.0. Released v7.5.0.
% 0.04/0.13 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% 0.12/0.34 % Computer : n017.cluster.edu
% 0.12/0.34 % Model : x86_64 x86_64
% 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.34 % Memory : 8042.1875MB
% 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.34 % CPULimit : 300
% 0.12/0.34 % WCLimit : 300
% 0.12/0.34 % DateTime : Fri Jun 21 07:56:09 EDT 2024
% 0.12/0.34 % CPUTime :
% 0.54/0.58 start to proof:theBenchmark
% 59.88/59.89 %-------------------------------------------
% 59.88/59.89 % File :CSE---1.7
% 59.88/59.89 % Problem :theBenchmark
% 59.88/59.89 % Transform :cnf
% 59.88/59.89 % Format :tptp:raw
% 59.88/59.89 % Command :java -jar mcs_scs.jar %d %s
% 59.88/59.89
% 59.88/59.89 % Result :Theorem 59.260000s
% 59.88/59.89 % Output :CNFRefutation 59.260000s
% 59.88/59.89 %-------------------------------------------
% 59.88/59.90 %------------------------------------------------------------------------------
% 59.88/59.90 % File : GEO554+1 : TPTP v8.2.0. Released v7.5.0.
% 59.88/59.90 % Domain : Geometry
% 59.88/59.90 % Problem : JGEX problem 14
% 59.88/59.90 % Version : [CGZ00] axioms.
% 59.88/59.90 % English :
% 59.88/59.90
% 59.88/59.90 % Refs : [CGZ00] Chou et al. (2000), A Deductive Database Approach to A
% 59.88/59.90 % : [YCG08] Ye et al. (2008), An Introduction to Java Geometry Exp
% 59.88/59.90 % : [Qua20] Quaresma (2020), Email to Geoff Sutcliffe
% 59.88/59.90 % Source : [Qua20]
% 59.88/59.90 % Names : 14.p [Qua20]
% 59.88/59.90
% 59.88/59.90 % Status : Theorem
% 59.88/59.90 % Rating : 0.42 v8.1.0, 0.44 v7.5.0
% 59.88/59.90 % Syntax : Number of formulae : 95 ( 0 unt; 0 def)
% 59.88/59.90 % Number of atoms : 294 ( 1 equ)
% 59.88/59.90 % Maximal formula atoms : 11 ( 3 avg)
% 59.88/59.91 % Number of connectives : 206 ( 7 ~; 0 |; 104 &)
% 59.88/59.91 % ( 0 <=>; 95 =>; 0 <=; 0 <~>)
% 59.88/59.91 % Maximal formula depth : 27 ( 9 avg)
% 59.88/59.91 % Maximal term depth : 1 ( 1 avg)
% 59.88/59.91 % Number of predicates : 12 ( 11 usr; 0 prp; 2-8 aty)
% 59.88/59.91 % Number of functors : 0 ( 0 usr; 0 con; --- aty)
% 59.88/59.91 % Number of variables : 538 ( 518 !; 20 ?)
% 59.88/59.91 % SPC : FOF_THM_RFO_SEQ
% 59.88/59.91
% 59.88/59.91 % Comments : Taken from JGEX [YCG08], converted by Pedro Quaresma.
% 59.88/59.91 %------------------------------------------------------------------------------
% 59.88/59.91 include('Axioms/GEO012+0.ax').
% 59.88/59.91 %------------------------------------------------------------------------------
% 59.88/59.91 fof(exemplo6GDDFULL012014,conjecture,
% 59.88/59.91 ! [A,B,C,D,E,F,G,NWPNT1,NWPNT2,NWPNT3,NWPNT4,NWPNT5,NWPNT6,NWPNT7,NWPNT8,NWPNT9] :
% 59.88/59.91 ( ( perp(C,A,C,B)
% 59.88/59.91 & circle(A,C,NWPNT1,NWPNT2)
% 59.88/59.91 & circle(B,C,NWPNT3,NWPNT4)
% 59.88/59.91 & circle(A,C,D,NWPNT5)
% 59.88/59.91 & coll(C,D,E)
% 59.88/59.91 & circle(B,C,E,NWPNT6)
% 59.88/59.91 & coll(B,E,F)
% 59.88/59.91 & circle(B,C,F,NWPNT7)
% 59.88/59.91 & circle(A,C,G,NWPNT8)
% 59.88/59.91 & circle(B,C,G,NWPNT9) )
% 59.88/59.91 => coll(D,F,G) ) ).
% 59.88/59.91
% 59.88/59.91 %------------------------------------------------------------------------------
% 59.88/59.91 %-------------------------------------------
% 59.88/59.91 % Proof found
% 59.88/59.91 % SZS status Theorem for theBenchmark
% 59.88/59.91 % SZS output start Proof
% 59.88/59.91 %ClaNum:265(EqnAxiom:141)
% 59.88/59.91 %VarNum:1613(SingletonVarNum:590)
% 59.88/59.91 %MaxLitNum:5
% 59.88/59.91 %MaxfuncDepth:1
% 59.88/59.91 %SharedTerms:27
% 59.88/59.91 %goalClause: 142 143 144 145 146 147 148 149 150 151 152
% 59.88/59.91 %singleGoalClaCount:11
% 59.88/59.91 [142]P1(a1,a15,a18)
% 59.88/59.91 [143]P1(a16,a17,a15)
% 59.88/59.91 [144]P3(a16,a2,a16,a1)
% 59.88/59.91 [145]P2(a2,a16,a17,a19)
% 59.88/59.91 [146]P2(a2,a16,a20,a26)
% 59.88/59.91 [147]P2(a2,a16,a21,a22)
% 59.88/59.91 [148]P2(a1,a16,a15,a27)
% 59.88/59.91 [149]P2(a1,a16,a18,a28)
% 59.88/59.91 [150]P2(a1,a16,a20,a29)
% 59.88/59.91 [151]P2(a1,a16,a23,a25)
% 59.88/59.91 [152]~P1(a17,a18,a20)
% 59.88/59.91 [153]~P1(x1532,x1531,x1533)+P1(x1531,x1532,x1533)
% 59.88/59.91 [154]~P1(x1541,x1543,x1542)+P1(x1541,x1542,x1543)
% 59.88/59.91 [155]~P4(x1551,x1552,x1553)+P1(x1551,x1552,x1553)
% 59.88/59.91 [156]~P4(x1561,x1563,x1562)+P4(x1561,x1562,x1563)
% 59.88/59.91 [158]~P4(x1581,x1582,x1583)+P5(x1581,x1582,x1581,x1583)
% 59.88/59.91 [162]~P10(x1621,x1622,x1621,x1623)+P1(x1621,x1622,x1623)
% 59.88/59.91 [228]~P5(x2281,x2282,x2281,x2283)+P9(x2281,x2282,x2282,x2283,x2282,x2283,x2281,x2283)
% 59.88/59.91 [165]~P10(x1653,x1654,x1651,x1652)+P10(x1651,x1652,x1653,x1654)
% 59.88/59.91 [166]~P10(x1661,x1662,x1664,x1663)+P10(x1661,x1662,x1663,x1664)
% 59.88/59.91 [167]~P3(x1673,x1674,x1671,x1672)+P3(x1671,x1672,x1673,x1674)
% 59.88/59.91 [168]~P3(x1681,x1682,x1684,x1683)+P3(x1681,x1682,x1683,x1684)
% 59.88/59.91 [169]~P5(x1693,x1694,x1691,x1692)+P5(x1691,x1692,x1693,x1694)
% 59.88/59.91 [170]~P5(x1701,x1702,x1704,x1703)+P5(x1701,x1702,x1703,x1704)
% 59.88/59.91 [171]~P6(x1712,x1711,x1713,x1714)+P6(x1711,x1712,x1713,x1714)
% 59.88/59.91 [172]~P6(x1721,x1723,x1722,x1724)+P6(x1721,x1722,x1723,x1724)
% 59.88/59.91 [173]~P6(x1731,x1732,x1734,x1733)+P6(x1731,x1732,x1733,x1734)
% 59.88/59.91 [226]~P6(x2262,x2263,x2261,x2264)+P9(x2261,x2262,x2261,x2263,x2264,x2262,x2264,x2263)
% 59.88/59.91 [189]~P2(x1894,x1891,x1892,x1893)+P3(f7(x1891,x1892,x1893,x1894),x1891,x1891,x1894)
% 59.88/59.91 [204]P5(x2041,x2042,x2043,x2044)+~P7(x2041,x2042,x2045,x2043,x2044,x2046)
% 59.88/59.91 [216]~P11(x2164,x2165,x2166,x2161,x2162,x2163)+P11(x2161,x2162,x2163,x2164,x2165,x2166)
% 59.88/59.91 [217]~P11(x2172,x2171,x2173,x2175,x2174,x2176)+P11(x2171,x2172,x2173,x2174,x2175,x2176)
% 59.88/59.91 [218]~P11(x2181,x2183,x2182,x2184,x2186,x2185)+P11(x2181,x2182,x2183,x2184,x2185,x2186)
% 59.88/59.91 [219]~P7(x2194,x2195,x2196,x2191,x2192,x2193)+P7(x2191,x2192,x2193,x2194,x2195,x2196)
% 59.88/59.91 [220]~P7(x2202,x2201,x2203,x2205,x2204,x2206)+P7(x2201,x2202,x2203,x2204,x2205,x2206)
% 59.88/59.91 [221]~P7(x2211,x2213,x2212,x2214,x2216,x2215)+P7(x2211,x2212,x2213,x2214,x2215,x2216)
% 59.88/59.91 [227]~P10(x2271,x2272,x2275,x2276)+P9(x2271,x2272,x2273,x2274,x2275,x2276,x2273,x2274)
% 59.88/59.91 [233]~P11(x2331,x2332,x2333,x2334,x2335,x2336)+P9(x2331,x2332,x2332,x2333,x2334,x2335,x2335,x2336)
% 59.88/59.91 [234]~P11(x2341,x2342,x2343,x2344,x2345,x2346)+P8(x2341,x2342,x2341,x2343,x2344,x2345,x2344,x2346)
% 59.88/59.91 [235]~P9(x2351,x2352,x2355,x2356,x2353,x2354,x2355,x2356)+P10(x2351,x2352,x2353,x2354)
% 59.88/59.91 [254]~P9(x2545,x2546,x2547,x2548,x2541,x2542,x2543,x2544)+P9(x2541,x2542,x2543,x2544,x2545,x2546,x2547,x2548)
% 59.88/59.91 [255]~P9(x2553,x2554,x2551,x2552,x2557,x2558,x2555,x2556)+P9(x2551,x2552,x2553,x2554,x2555,x2556,x2557,x2558)
% 59.88/59.91 [256]~P9(x2562,x2561,x2563,x2564,x2565,x2566,x2567,x2568)+P9(x2561,x2562,x2563,x2564,x2565,x2566,x2567,x2568)
% 59.88/59.91 [257]~P9(x2571,x2572,x2575,x2576,x2573,x2574,x2577,x2578)+P9(x2571,x2572,x2573,x2574,x2575,x2576,x2577,x2578)
% 59.88/59.91 [258]~P8(x2585,x2586,x2587,x2588,x2581,x2582,x2583,x2584)+P8(x2581,x2582,x2583,x2584,x2585,x2586,x2587,x2588)
% 59.88/59.91 [259]~P8(x2593,x2594,x2591,x2592,x2597,x2598,x2595,x2596)+P8(x2591,x2592,x2593,x2594,x2595,x2596,x2597,x2598)
% 59.88/59.91 [260]~P8(x2602,x2601,x2603,x2604,x2605,x2606,x2607,x2608)+P8(x2601,x2602,x2603,x2604,x2605,x2606,x2607,x2608)
% 59.88/59.91 [261]~P8(x2611,x2612,x2615,x2616,x2613,x2614,x2617,x2618)+P8(x2611,x2612,x2613,x2614,x2615,x2616,x2617,x2618)
% 59.88/59.91 [163]~P1(x1631,x1632,x1633)+~P5(x1631,x1632,x1631,x1633)+P4(x1631,x1632,x1633)
% 59.88/59.91 [237]P5(x2371,x2372,x2371,x2373)+~P9(x2371,x2372,x2372,x2373,x2372,x2373,x2371,x2373)+P1(x2371,x2372,x2373)
% 59.88/59.91 [178]~P3(x1781,x1782,x1782,x1783)+~P5(x1782,x1781,x1782,x1783)+P1(x1781,x1782,f3(x1781,x1783,x1782))
% 59.88/59.91 [190]~P3(x1902,x1901,x1901,x1903)+~P5(x1901,x1902,x1901,x1903)+P5(x1901,x1902,x1901,f3(x1902,x1903,x1901))
% 59.88/59.91 [157]~P1(x1573,x1574,x1571)+P1(x1571,x1572,x1573)+~P1(x1573,x1574,x1572)
% 59.88/59.91 [174]~P2(x1744,x1741,x1742,x1743)+P3(x1741,x1742,x1742,x1743)+~P1(x1744,x1741,x1743)
% 59.88/59.91 [175]~P3(x1751,x1754,x1752,x1753)+P5(x1751,x1752,x1751,x1753)+~P4(x1754,x1752,x1753)
% 59.88/59.91 [176]~P3(x1761,x1763,x1763,x1764)+P5(x1761,x1762,x1763,x1762)+~P4(x1762,x1761,x1764)
% 59.88/59.91 [183]~P5(x1831,x1834,x1832,x1834)+~P5(x1831,x1833,x1832,x1833)+P3(x1831,x1832,x1833,x1834)
% 59.88/59.91 [186]~P5(x1861,x1862,x1861,x1864)+~P5(x1861,x1862,x1861,x1863)+P2(x1861,x1862,x1863,x1864)
% 59.88/59.91 [232]~P10(x2321,x2324,x2323,x2322)+~P6(x2321,x2324,x2323,x2322)+P9(x2321,x2322,x2323,x2322,x2323,x2322,x2323,x2324)
% 59.88/59.92 [236]~P9(x2361,x2363,x2361,x2364,x2362,x2363,x2362,x2364)+P1(x2361,x2362,x2363)+P6(x2363,x2364,x2361,x2362)
% 59.88/59.92 [238]~P1(x2383,x2384,x2382)+~P9(x2383,x2381,x2383,x2382,x2384,x2381,x2384,x2382)+P6(x2381,x2382,x2383,x2384)
% 59.88/59.92 [240]P3(x2401,x2402,x2403,x2404)+~P9(x2401,x2402,x2403,x2404,x2403,x2404,x2401,x2402)+P10(x2401,x2402,x2403,x2404)
% 59.88/59.92 [179]~P3(x1791,x1794,x1792,x1793)+~P3(x1792,x1794,x1791,x1793)+P1(f4(x1791,x1792,x1793),x1793,x1792)
% 59.88/59.92 [180]~P3(x1801,x1804,x1802,x1803)+~P3(x1802,x1804,x1801,x1803)+P1(f5(x1801,x1802,x1803),x1803,x1801)
% 59.88/59.92 [191]~P3(x1911,x1914,x1912,x1913)+~P3(x1912,x1914,x1911,x1913)+P3(x1911,f4(x1911,x1912,x1913),x1913,x1912)
% 59.88/59.92 [192]~P3(x1921,x1924,x1922,x1923)+~P3(x1922,x1924,x1921,x1923)+P3(x1921,f5(x1922,x1921,x1923),x1923,x1922)
% 59.88/59.92 [193]~P3(x1931,x1933,x1933,x1932)+~P6(x1931,x1932,x1933,x1934)+P2(f8(x1931,x1932,x1933),x1931,x1932,x1933)
% 59.88/59.92 [195]~P3(x1953,x1954,x1952,x1951)+~P5(x1953,x1952,x1953,x1951)+P1(x1951,x1952,f31(x1952,x1951,x1953,x1954))
% 59.88/59.92 [196]~P3(x1963,x1964,x1961,x1962)+~P5(x1963,x1961,x1963,x1962)+P1(f31(x1961,x1962,x1963,x1964),x1963,x1964)
% 59.88/59.92 [247]~P5(x2473,x2472,x2473,x2471)+~P9(x2472,x2473,x2473,x2474,x2473,x2474,x2473,x2471)+P1(x2471,x2472,f24(x2472,x2471,x2473,x2474))
% 59.88/59.92 [248]~P3(x2483,x2484,x2482,x2481)+~P9(x2482,x2483,x2483,x2484,x2483,x2484,x2483,x2481)+P1(x2481,x2482,f32(x2482,x2481,x2483,x2484))
% 59.88/59.92 [249]~P3(x2493,x2492,x2492,x2491)+~P9(x2494,x2493,x2492,x2493,x2492,x2493,x2491,x2493)+P1(f14(x2491,x2492,x2493,x2494),x2493,x2494)
% 59.88/59.92 [250]~P3(x2503,x2502,x2502,x2501)+~P9(x2504,x2503,x2502,x2503,x2502,x2503,x2501,x2503)+P1(f14(x2501,x2502,x2503,x2504),x2501,x2502)
% 59.88/59.92 [251]~P5(x2513,x2511,x2513,x2512)+~P9(x2511,x2513,x2513,x2514,x2513,x2514,x2513,x2512)+P1(f24(x2511,x2512,x2513,x2514),x2513,x2514)
% 59.88/59.92 [252]~P3(x2523,x2524,x2521,x2522)+~P9(x2521,x2523,x2523,x2524,x2523,x2524,x2523,x2522)+P1(f32(x2521,x2522,x2523,x2524),x2523,x2524)
% 59.88/59.92 [159]~P4(x1595,x1591,x1593)+P10(x1591,x1592,x1593,x1594)+~P4(x1595,x1592,x1594)
% 59.88/59.92 [160]~P4(x1601,x1605,x1603)+P10(x1601,x1602,x1603,x1604)+~P4(x1602,x1605,x1604)
% 59.88/59.92 [187]~P6(x1875,x1871,x1872,x1873)+P6(x1871,x1872,x1873,x1874)+~P6(x1875,x1871,x1872,x1874)
% 59.88/59.92 [229]~P4(x2295,x2292,x2293)+~P2(x2294,x2291,x2292,x2293)+P9(x2291,x2292,x2291,x2293,x2294,x2292,x2294,x2295)
% 59.88/59.92 [231]~P2(x2315,x2311,x2313,x2314)+P9(x2311,x2312,x2311,x2313,x2314,x2311,x2314,x2313)+~P3(x2315,x2311,x2311,x2312)
% 59.88/59.92 [244]~P9(x2442,x2443,x2442,x2444,x2445,x2442,x2445,x2444)+P3(x2441,x2442,x2442,x2443)+~P2(x2441,x2442,x2444,x2445)
% 59.88/59.92 [199]~P1(x1992,x1994,x1995)+~P3(x1991,x1993,x1993,x1992)+P1(f12(x1991,x1992,x1993,x1994,x1995),x1994,x1995)
% 59.88/59.92 [200]~P1(x2002,x2004,x2005)+~P3(x2001,x2003,x2003,x2002)+P3(f12(x2001,x2002,x2003,x2004,x2005),x2001,x2004,x2005)
% 59.88/59.92 [201]~P3(x2013,x2014,x2014,x2011)+~P5(x2011,x2012,x2011,x2015)+P5(x2011,x2012,x2011,f35(x2013,x2014,x2012,x2015,x2011))
% 59.88/59.92 [202]~P3(x2023,x2021,x2021,x2025)+~P5(x2025,x2022,x2025,x2024)+P5(x2021,x2022,x2021,f35(x2023,x2021,x2022,x2024,x2025))
% 59.88/59.92 [203]~P3(x2031,x2032,x2032,x2035)+~P5(x2035,x2033,x2035,x2034)+P10(f35(x2031,x2032,x2033,x2034,x2035),x2033,x2031,x2032)
% 59.88/59.92 [246]~P9(x2461,x2463,x2462,x2463,x2461,x2464,x2462,x2465)+P1(x2461,x2462,x2463)+P6(x2464,x2462,x2463,f34(x2461,x2462,x2463,x2464))
% 59.88/59.92 [262]~P9(x2621,x2623,x2622,x2623,x2621,x2624,x2622,x2625)+P1(x2621,x2622,x2623)+P9(x2621,x2623,x2622,x2623,x2621,f34(x2621,x2622,x2623,x2624),x2622,f34(x2621,x2622,x2623,x2624))
% 59.88/59.92 [181]~P10(x1811,x1812,x1815,x1816)+P10(x1811,x1812,x1813,x1814)+~P10(x1815,x1816,x1813,x1814)
% 59.88/59.92 [182]~P3(x1821,x1822,x1825,x1826)+P10(x1821,x1822,x1823,x1824)+~P3(x1825,x1826,x1823,x1824)
% 59.88/59.92 [184]~P3(x1845,x1846,x1843,x1844)+P3(x1841,x1842,x1843,x1844)+~P10(x1841,x1842,x1845,x1846)
% 59.88/59.92 [185]~P5(x1851,x1852,x1855,x1856)+P5(x1851,x1852,x1853,x1854)+~P5(x1855,x1856,x1853,x1854)
% 59.88/59.92 [222]~P5(x2221,x2222,x2224,x2225)+~P11(x2221,x2222,x2223,x2224,x2225,x2226)+P7(x2221,x2222,x2223,x2224,x2225,x2226)
% 59.88/59.92 [225]~P4(x2254,x2255,x2256)+~P4(x2251,x2252,x2253)+P8(x2251,x2252,x2252,x2253,x2254,x2255,x2255,x2256)
% 59.88/59.92 [205]~P4(x2056,x2053,x2054)+~P4(x2055,x2051,x2052)+P4(f33(x2051,x2052,x2053,x2054,x2055,x2056),x2051,x2054)
% 59.88/59.92 [206]~P4(x2066,x2063,x2064)+~P4(x2065,x2061,x2062)+P10(f33(x2061,x2062,x2063,x2064,x2065,x2066),x2066,x2061,x2063)
% 59.88/59.92 [207]~P4(x2076,x2073,x2074)+~P4(x2075,x2071,x2072)+P10(f33(x2071,x2072,x2073,x2074,x2075,x2076),x2075,x2072,x2074)
% 59.88/59.92 [242]~P9(x2421,x2422,x2423,x2424,x2425,x2426,x2427,x2428)+P10(x2421,x2422,x2423,x2424)+~P10(x2425,x2426,x2427,x2428)
% 59.88/59.92 [243]~P9(x2431,x2432,x2433,x2434,x2435,x2436,x2437,x2438)+P3(x2431,x2432,x2433,x2434)+~P3(x2435,x2436,x2437,x2438)
% 59.88/59.92 [245]~P8(x2451,x2452,x2453,x2454,x2455,x2456,x2457,x2458)+P5(x2451,x2452,x2453,x2454)+~P5(x2455,x2456,x2457,x2458)
% 59.88/59.92 [223]~P11(x2231,x2232,x2233,x2237,x2238,x2239)+P11(x2231,x2232,x2233,x2234,x2235,x2236)+~P11(x2237,x2238,x2239,x2234,x2235,x2236)
% 59.88/59.92 [224]~P7(x2241,x2242,x2243,x2247,x2248,x2249)+P7(x2241,x2242,x2243,x2244,x2245,x2246)+~P7(x2247,x2248,x2249,x2244,x2245,x2246)
% 59.88/59.92 [264]~P9(x2641,x2642,x2643,x2644,x2649,x26410,x26411,x26412)+P9(x2641,x2642,x2643,x2644,x2645,x2646,x2647,x2648)+~P9(x2649,x26410,x26411,x26412,x2645,x2646,x2647,x2648)
% 59.88/59.92 [265]~P8(x2651,x2652,x2653,x2654,x2659,x26510,x26511,x26512)+P8(x2651,x2652,x2653,x2654,x2655,x2656,x2657,x2658)+~P8(x2659,x26510,x26511,x26512,x2655,x2656,x2657,x2658)
% 59.88/59.92 [197]~P5(x1972,x1971,x1974,x1971)+~P6(x1972,x1974,x1971,x1973)+P3(x1971,x1972,x1972,x1973)+~P5(x1972,x1973,x1974,x1973)
% 59.88/59.92 [164]~P1(x1641,x1642,x1643)+~P10(x1644,x1641,x1645,x1643)+P4(x1641,x1642,x1643)+~P4(x1644,x1642,x1645)
% 59.88/59.92 [177]~P10(x1774,x1773,x1775,x1772)+~P10(x1774,x1772,x1775,x1773)+P4(x1771,x1772,x1773)+~P4(x1771,x1774,x1775)
% 59.88/59.92 [198]~P5(x1985,x1981,x1985,x1983)+~P5(x1985,x1981,x1985,x1982)+P6(x1981,x1982,x1983,x1984)+~P5(x1985,x1981,x1985,x1984)
% 59.88/59.92 [230]~P1(x2301,x2304,x2305)+~P1(x2301,x2302,x2303)+~P10(x2302,x2304,x2303,x2305)+P8(x2301,x2302,x2302,x2303,x2301,x2304,x2304,x2305)
% 59.88/59.92 [241]~P1(x2411,x2412,x2413)+~P9(x2415,x2412,x2415,x2413,x2414,x2412,x2414,x2411)+P4(x2411,x2412,x2413)+~P2(x2414,x2415,x2412,x2413)
% 59.88/59.92 [188]~P3(x1883,x1881,x1883,x1885)+~P3(x1881,x1882,x1881,x1883)+~P4(x1884,x1882,x1885)+P4(f6(x1881,x1882,x1883),x1881,x1883)
% 59.88/59.92 [194]~P6(x1941,x1942,x1943,x1945)+~P10(x1941,x1942,x1943,x1945)+~P4(x1944,x1941,x1942)+P2(f9(x1941,x1942,x1943),x1941,x1942,x1943)
% 59.88/59.92 [263]~P9(x2631,x2633,x2632,x2633,x2634,x2636,x2635,x2636)+~P9(x2631,x2632,x2632,x2633,x2634,x2635,x2635,x2636)+P1(x2631,x2632,x2633)+P11(x2631,x2632,x2633,x2634,x2635,x2636)
% 59.88/59.92 [253]~P6(x2531,x2532,x2535,x2534)+~P6(x2531,x2532,x2535,x2533)+~P9(x2535,x2531,x2535,x2532,x2536,x2533,x2536,x2534)+P5(x2531,x2532,x2533,x2534)+~P6(x2531,x2532,x2535,x2536)
% 59.88/59.92 [208]~P1(x2082,x2083,x2084)+~P1(x2081,x2084,x2086)+~P1(x2081,x2083,x2085)+~P10(x2083,x2084,x2085,x2086)+P1(x2081,x2082,f13(x2083,x2084,x2085,x2086,x2081,x2082))
% 59.88/59.92 [209]~P1(x2096,x2091,x2092)+~P1(x2095,x2092,x2094)+~P1(x2095,x2091,x2093)+~P10(x2091,x2092,x2093,x2094)+P1(f13(x2091,x2092,x2093,x2094,x2095,x2096),x2093,x2094)
% 59.88/59.92 [210]~P1(x2103,x2104,x2105)+~P4(x2106,x2101,x2102)+~P10(x2101,x2103,x2105,x2106)+~P10(x2101,x2103,x2102,x2104)+P1(f36(x2101,x2102,x2103,x2104,x2105,x2106),x2106,x2105)
% 59.88/59.92 [211]~P1(x2113,x2114,x2115)+~P4(x2116,x2111,x2112)+~P10(x2111,x2113,x2115,x2116)+~P10(x2111,x2113,x2112,x2114)+P1(f36(x2111,x2112,x2113,x2114,x2115,x2116),x2111,x2114)
% 59.88/59.92 [212]~P5(x2122,x2123,x2122,x2124)+~P5(x2121,x2123,x2121,x2126)+~P2(x2121,x2123,x2124,x2125)+E(x2121,x2122)+P1(f10(x2123,x2124,x2125,x2126,x2121,x2122),x2123,x2125)
% 59.88/59.92 [213]~P5(x2132,x2133,x2132,x2134)+~P5(x2131,x2133,x2131,x2136)+~P2(x2131,x2133,x2134,x2135)+E(x2131,x2132)+P1(f11(x2133,x2134,x2135,x2136,x2131,x2132),x2134,x2136)
% 59.88/59.92 [214]~P5(x2142,x2143,x2142,x2144)+~P5(x2141,x2143,x2141,x2146)+~P2(x2141,x2143,x2144,x2145)+E(x2141,x2142)+P5(f10(x2143,x2144,x2145,x2146,x2141,x2142),x2142,x2142,x2143)
% 59.88/59.92 [215]~P5(x2152,x2153,x2152,x2154)+~P5(x2151,x2153,x2151,x2156)+~P2(x2151,x2153,x2154,x2155)+E(x2151,x2152)+P5(f11(x2153,x2154,x2155,x2156,x2151,x2152),x2152,x2152,x2153)
% 59.88/59.92 [161]~P1(x1613,x1611,x1614)+~P1(x1615,x1611,x1614)+~P4(x1616,x1615,x1613)+~P4(x1617,x1611,x1614)+P4(f30(x1611,x1612),x1611,x1612)
% 59.88/59.92 %EqnAxiom
% 59.88/59.92 [1]E(x11,x11)
% 59.88/59.92 [2]E(x22,x21)+~E(x21,x22)
% 59.88/59.92 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 59.88/59.92 [4]~E(x41,x42)+E(f30(x41,x43),f30(x42,x43))
% 59.88/59.92 [5]~E(x51,x52)+E(f30(x53,x51),f30(x53,x52))
% 59.88/59.92 [6]~E(x61,x62)+E(f3(x61,x63,x64),f3(x62,x63,x64))
% 59.88/59.92 [7]~E(x71,x72)+E(f3(x73,x71,x74),f3(x73,x72,x74))
% 59.88/59.92 [8]~E(x81,x82)+E(f3(x83,x84,x81),f3(x83,x84,x82))
% 59.88/59.92 [9]~E(x91,x92)+E(f4(x91,x93,x94),f4(x92,x93,x94))
% 59.88/59.92 [10]~E(x101,x102)+E(f4(x103,x101,x104),f4(x103,x102,x104))
% 59.88/59.92 [11]~E(x111,x112)+E(f4(x113,x114,x111),f4(x113,x114,x112))
% 59.88/59.92 [12]~E(x121,x122)+E(f5(x121,x123,x124),f5(x122,x123,x124))
% 59.88/59.92 [13]~E(x131,x132)+E(f5(x133,x131,x134),f5(x133,x132,x134))
% 59.88/59.92 [14]~E(x141,x142)+E(f5(x143,x144,x141),f5(x143,x144,x142))
% 59.88/59.92 [15]~E(x151,x152)+E(f6(x151,x153,x154),f6(x152,x153,x154))
% 59.88/59.92 [16]~E(x161,x162)+E(f6(x163,x161,x164),f6(x163,x162,x164))
% 59.88/59.92 [17]~E(x171,x172)+E(f6(x173,x174,x171),f6(x173,x174,x172))
% 59.88/59.92 [18]~E(x181,x182)+E(f7(x181,x183,x184,x185),f7(x182,x183,x184,x185))
% 59.88/59.92 [19]~E(x191,x192)+E(f7(x193,x191,x194,x195),f7(x193,x192,x194,x195))
% 59.88/59.92 [20]~E(x201,x202)+E(f7(x203,x204,x201,x205),f7(x203,x204,x202,x205))
% 59.88/59.92 [21]~E(x211,x212)+E(f7(x213,x214,x215,x211),f7(x213,x214,x215,x212))
% 59.88/59.92 [22]~E(x221,x222)+E(f34(x221,x223,x224,x225),f34(x222,x223,x224,x225))
% 59.88/59.92 [23]~E(x231,x232)+E(f34(x233,x231,x234,x235),f34(x233,x232,x234,x235))
% 59.88/59.92 [24]~E(x241,x242)+E(f34(x243,x244,x241,x245),f34(x243,x244,x242,x245))
% 59.88/59.92 [25]~E(x251,x252)+E(f34(x253,x254,x255,x251),f34(x253,x254,x255,x252))
% 59.88/59.92 [26]~E(x261,x262)+E(f24(x261,x263,x264,x265),f24(x262,x263,x264,x265))
% 59.88/59.92 [27]~E(x271,x272)+E(f24(x273,x271,x274,x275),f24(x273,x272,x274,x275))
% 59.88/59.92 [28]~E(x281,x282)+E(f24(x283,x284,x281,x285),f24(x283,x284,x282,x285))
% 59.88/59.92 [29]~E(x291,x292)+E(f24(x293,x294,x295,x291),f24(x293,x294,x295,x292))
% 59.88/59.92 [30]~E(x301,x302)+E(f32(x301,x303,x304,x305),f32(x302,x303,x304,x305))
% 59.88/59.92 [31]~E(x311,x312)+E(f32(x313,x311,x314,x315),f32(x313,x312,x314,x315))
% 59.88/59.92 [32]~E(x321,x322)+E(f32(x323,x324,x321,x325),f32(x323,x324,x322,x325))
% 59.88/59.92 [33]~E(x331,x332)+E(f32(x333,x334,x335,x331),f32(x333,x334,x335,x332))
% 59.88/59.92 [34]~E(x341,x342)+E(f8(x341,x343,x344),f8(x342,x343,x344))
% 59.88/59.92 [35]~E(x351,x352)+E(f8(x353,x351,x354),f8(x353,x352,x354))
% 59.88/59.92 [36]~E(x361,x362)+E(f8(x363,x364,x361),f8(x363,x364,x362))
% 59.88/59.92 [37]~E(x371,x372)+E(f9(x371,x373,x374),f9(x372,x373,x374))
% 59.88/59.92 [38]~E(x381,x382)+E(f9(x383,x381,x384),f9(x383,x382,x384))
% 59.88/59.92 [39]~E(x391,x392)+E(f9(x393,x394,x391),f9(x393,x394,x392))
% 59.88/59.92 [40]~E(x401,x402)+E(f31(x401,x403,x404,x405),f31(x402,x403,x404,x405))
% 59.88/59.92 [41]~E(x411,x412)+E(f31(x413,x411,x414,x415),f31(x413,x412,x414,x415))
% 59.88/59.92 [42]~E(x421,x422)+E(f31(x423,x424,x421,x425),f31(x423,x424,x422,x425))
% 59.88/59.92 [43]~E(x431,x432)+E(f31(x433,x434,x435,x431),f31(x433,x434,x435,x432))
% 59.88/59.92 [44]~E(x441,x442)+E(f14(x441,x443,x444,x445),f14(x442,x443,x444,x445))
% 59.88/59.92 [45]~E(x451,x452)+E(f14(x453,x451,x454,x455),f14(x453,x452,x454,x455))
% 59.88/59.92 [46]~E(x461,x462)+E(f14(x463,x464,x461,x465),f14(x463,x464,x462,x465))
% 59.88/59.92 [47]~E(x471,x472)+E(f14(x473,x474,x475,x471),f14(x473,x474,x475,x472))
% 59.88/59.92 [48]~E(x481,x482)+E(f12(x481,x483,x484,x485,x486),f12(x482,x483,x484,x485,x486))
% 59.88/59.92 [49]~E(x491,x492)+E(f12(x493,x491,x494,x495,x496),f12(x493,x492,x494,x495,x496))
% 59.88/59.92 [50]~E(x501,x502)+E(f12(x503,x504,x501,x505,x506),f12(x503,x504,x502,x505,x506))
% 59.88/59.92 [51]~E(x511,x512)+E(f12(x513,x514,x515,x511,x516),f12(x513,x514,x515,x512,x516))
% 59.88/59.92 [52]~E(x521,x522)+E(f12(x523,x524,x525,x526,x521),f12(x523,x524,x525,x526,x522))
% 59.88/59.92 [53]~E(x531,x532)+E(f11(x531,x533,x534,x535,x536,x537),f11(x532,x533,x534,x535,x536,x537))
% 59.88/59.92 [54]~E(x541,x542)+E(f11(x543,x541,x544,x545,x546,x547),f11(x543,x542,x544,x545,x546,x547))
% 59.88/59.92 [55]~E(x551,x552)+E(f11(x553,x554,x551,x555,x556,x557),f11(x553,x554,x552,x555,x556,x557))
% 59.88/59.92 [56]~E(x561,x562)+E(f11(x563,x564,x565,x561,x566,x567),f11(x563,x564,x565,x562,x566,x567))
% 59.88/59.92 [57]~E(x571,x572)+E(f11(x573,x574,x575,x576,x571,x577),f11(x573,x574,x575,x576,x572,x577))
% 59.88/59.92 [58]~E(x581,x582)+E(f11(x583,x584,x585,x586,x587,x581),f11(x583,x584,x585,x586,x587,x582))
% 59.88/59.92 [59]~E(x591,x592)+E(f35(x591,x593,x594,x595,x596),f35(x592,x593,x594,x595,x596))
% 59.88/59.92 [60]~E(x601,x602)+E(f35(x603,x601,x604,x605,x606),f35(x603,x602,x604,x605,x606))
% 59.88/59.92 [61]~E(x611,x612)+E(f35(x613,x614,x611,x615,x616),f35(x613,x614,x612,x615,x616))
% 59.88/59.92 [62]~E(x621,x622)+E(f35(x623,x624,x625,x621,x626),f35(x623,x624,x625,x622,x626))
% 59.88/59.92 [63]~E(x631,x632)+E(f35(x633,x634,x635,x636,x631),f35(x633,x634,x635,x636,x632))
% 59.88/59.92 [64]~E(x641,x642)+E(f10(x641,x643,x644,x645,x646,x647),f10(x642,x643,x644,x645,x646,x647))
% 59.88/59.92 [65]~E(x651,x652)+E(f10(x653,x651,x654,x655,x656,x657),f10(x653,x652,x654,x655,x656,x657))
% 59.88/59.92 [66]~E(x661,x662)+E(f10(x663,x664,x661,x665,x666,x667),f10(x663,x664,x662,x665,x666,x667))
% 59.88/59.92 [67]~E(x671,x672)+E(f10(x673,x674,x675,x671,x676,x677),f10(x673,x674,x675,x672,x676,x677))
% 59.88/59.92 [68]~E(x681,x682)+E(f10(x683,x684,x685,x686,x681,x687),f10(x683,x684,x685,x686,x682,x687))
% 59.88/59.92 [69]~E(x691,x692)+E(f10(x693,x694,x695,x696,x697,x691),f10(x693,x694,x695,x696,x697,x692))
% 59.88/59.92 [70]~E(x701,x702)+E(f36(x701,x703,x704,x705,x706,x707),f36(x702,x703,x704,x705,x706,x707))
% 59.88/59.92 [71]~E(x711,x712)+E(f36(x713,x711,x714,x715,x716,x717),f36(x713,x712,x714,x715,x716,x717))
% 59.88/59.92 [72]~E(x721,x722)+E(f36(x723,x724,x721,x725,x726,x727),f36(x723,x724,x722,x725,x726,x727))
% 59.88/59.92 [73]~E(x731,x732)+E(f36(x733,x734,x735,x731,x736,x737),f36(x733,x734,x735,x732,x736,x737))
% 59.88/59.92 [74]~E(x741,x742)+E(f36(x743,x744,x745,x746,x741,x747),f36(x743,x744,x745,x746,x742,x747))
% 59.88/59.92 [75]~E(x751,x752)+E(f36(x753,x754,x755,x756,x757,x751),f36(x753,x754,x755,x756,x757,x752))
% 59.88/59.92 [76]~E(x761,x762)+E(f33(x761,x763,x764,x765,x766,x767),f33(x762,x763,x764,x765,x766,x767))
% 59.88/59.92 [77]~E(x771,x772)+E(f33(x773,x771,x774,x775,x776,x777),f33(x773,x772,x774,x775,x776,x777))
% 59.88/59.92 [78]~E(x781,x782)+E(f33(x783,x784,x781,x785,x786,x787),f33(x783,x784,x782,x785,x786,x787))
% 59.88/59.92 [79]~E(x791,x792)+E(f33(x793,x794,x795,x791,x796,x797),f33(x793,x794,x795,x792,x796,x797))
% 59.88/59.92 [80]~E(x801,x802)+E(f33(x803,x804,x805,x806,x801,x807),f33(x803,x804,x805,x806,x802,x807))
% 59.88/59.92 [81]~E(x811,x812)+E(f33(x813,x814,x815,x816,x817,x811),f33(x813,x814,x815,x816,x817,x812))
% 59.88/59.92 [82]~E(x821,x822)+E(f13(x821,x823,x824,x825,x826,x827),f13(x822,x823,x824,x825,x826,x827))
% 59.88/59.92 [83]~E(x831,x832)+E(f13(x833,x831,x834,x835,x836,x837),f13(x833,x832,x834,x835,x836,x837))
% 59.88/59.92 [84]~E(x841,x842)+E(f13(x843,x844,x841,x845,x846,x847),f13(x843,x844,x842,x845,x846,x847))
% 59.88/59.92 [85]~E(x851,x852)+E(f13(x853,x854,x855,x851,x856,x857),f13(x853,x854,x855,x852,x856,x857))
% 59.88/59.92 [86]~E(x861,x862)+E(f13(x863,x864,x865,x866,x861,x867),f13(x863,x864,x865,x866,x862,x867))
% 59.88/59.92 [87]~E(x871,x872)+E(f13(x873,x874,x875,x876,x877,x871),f13(x873,x874,x875,x876,x877,x872))
% 59.88/59.92 [88]P1(x882,x883,x884)+~E(x881,x882)+~P1(x881,x883,x884)
% 59.88/59.92 [89]P1(x893,x892,x894)+~E(x891,x892)+~P1(x893,x891,x894)
% 59.88/59.92 [90]P1(x903,x904,x902)+~E(x901,x902)+~P1(x903,x904,x901)
% 59.88/59.92 [91]P8(x912,x913,x914,x915,x916,x917,x918,x919)+~E(x911,x912)+~P8(x911,x913,x914,x915,x916,x917,x918,x919)
% 59.88/59.92 [92]P8(x923,x922,x924,x925,x926,x927,x928,x929)+~E(x921,x922)+~P8(x923,x921,x924,x925,x926,x927,x928,x929)
% 59.88/59.92 [93]P8(x933,x934,x932,x935,x936,x937,x938,x939)+~E(x931,x932)+~P8(x933,x934,x931,x935,x936,x937,x938,x939)
% 59.88/59.92 [94]P8(x943,x944,x945,x942,x946,x947,x948,x949)+~E(x941,x942)+~P8(x943,x944,x945,x941,x946,x947,x948,x949)
% 59.88/59.92 [95]P8(x953,x954,x955,x956,x952,x957,x958,x959)+~E(x951,x952)+~P8(x953,x954,x955,x956,x951,x957,x958,x959)
% 59.88/59.92 [96]P8(x963,x964,x965,x966,x967,x962,x968,x969)+~E(x961,x962)+~P8(x963,x964,x965,x966,x967,x961,x968,x969)
% 59.88/59.92 [97]P8(x973,x974,x975,x976,x977,x978,x972,x979)+~E(x971,x972)+~P8(x973,x974,x975,x976,x977,x978,x971,x979)
% 59.88/59.92 [98]P8(x983,x984,x985,x986,x987,x988,x989,x982)+~E(x981,x982)+~P8(x983,x984,x985,x986,x987,x988,x989,x981)
% 59.88/59.92 [99]P3(x992,x993,x994,x995)+~E(x991,x992)+~P3(x991,x993,x994,x995)
% 59.88/59.92 [100]P3(x1003,x1002,x1004,x1005)+~E(x1001,x1002)+~P3(x1003,x1001,x1004,x1005)
% 59.88/59.92 [101]P3(x1013,x1014,x1012,x1015)+~E(x1011,x1012)+~P3(x1013,x1014,x1011,x1015)
% 59.88/59.92 [102]P3(x1023,x1024,x1025,x1022)+~E(x1021,x1022)+~P3(x1023,x1024,x1025,x1021)
% 59.88/59.92 [103]P2(x1032,x1033,x1034,x1035)+~E(x1031,x1032)+~P2(x1031,x1033,x1034,x1035)
% 59.88/59.92 [104]P2(x1043,x1042,x1044,x1045)+~E(x1041,x1042)+~P2(x1043,x1041,x1044,x1045)
% 59.88/59.92 [105]P2(x1053,x1054,x1052,x1055)+~E(x1051,x1052)+~P2(x1053,x1054,x1051,x1055)
% 59.88/59.92 [106]P2(x1063,x1064,x1065,x1062)+~E(x1061,x1062)+~P2(x1063,x1064,x1065,x1061)
% 59.88/59.92 [107]P7(x1072,x1073,x1074,x1075,x1076,x1077)+~E(x1071,x1072)+~P7(x1071,x1073,x1074,x1075,x1076,x1077)
% 59.88/59.92 [108]P7(x1083,x1082,x1084,x1085,x1086,x1087)+~E(x1081,x1082)+~P7(x1083,x1081,x1084,x1085,x1086,x1087)
% 59.88/59.92 [109]P7(x1093,x1094,x1092,x1095,x1096,x1097)+~E(x1091,x1092)+~P7(x1093,x1094,x1091,x1095,x1096,x1097)
% 59.88/59.92 [110]P7(x1103,x1104,x1105,x1102,x1106,x1107)+~E(x1101,x1102)+~P7(x1103,x1104,x1105,x1101,x1106,x1107)
% 59.88/59.92 [111]P7(x1113,x1114,x1115,x1116,x1112,x1117)+~E(x1111,x1112)+~P7(x1113,x1114,x1115,x1116,x1111,x1117)
% 59.88/59.92 [112]P7(x1123,x1124,x1125,x1126,x1127,x1122)+~E(x1121,x1122)+~P7(x1123,x1124,x1125,x1126,x1127,x1121)
% 59.88/59.92 [113]P11(x1132,x1133,x1134,x1135,x1136,x1137)+~E(x1131,x1132)+~P11(x1131,x1133,x1134,x1135,x1136,x1137)
% 59.88/59.92 [114]P11(x1143,x1142,x1144,x1145,x1146,x1147)+~E(x1141,x1142)+~P11(x1143,x1141,x1144,x1145,x1146,x1147)
% 59.88/59.92 [115]P11(x1153,x1154,x1152,x1155,x1156,x1157)+~E(x1151,x1152)+~P11(x1153,x1154,x1151,x1155,x1156,x1157)
% 59.88/59.92 [116]P11(x1163,x1164,x1165,x1162,x1166,x1167)+~E(x1161,x1162)+~P11(x1163,x1164,x1165,x1161,x1166,x1167)
% 59.88/59.92 [117]P11(x1173,x1174,x1175,x1176,x1172,x1177)+~E(x1171,x1172)+~P11(x1173,x1174,x1175,x1176,x1171,x1177)
% 59.88/59.92 [118]P11(x1183,x1184,x1185,x1186,x1187,x1182)+~E(x1181,x1182)+~P11(x1183,x1184,x1185,x1186,x1187,x1181)
% 59.88/59.92 [119]P5(x1192,x1193,x1194,x1195)+~E(x1191,x1192)+~P5(x1191,x1193,x1194,x1195)
% 59.88/59.92 [120]P5(x1203,x1202,x1204,x1205)+~E(x1201,x1202)+~P5(x1203,x1201,x1204,x1205)
% 59.88/59.92 [121]P5(x1213,x1214,x1212,x1215)+~E(x1211,x1212)+~P5(x1213,x1214,x1211,x1215)
% 59.88/59.92 [122]P5(x1223,x1224,x1225,x1222)+~E(x1221,x1222)+~P5(x1223,x1224,x1225,x1221)
% 59.88/59.92 [123]P9(x1232,x1233,x1234,x1235,x1236,x1237,x1238,x1239)+~E(x1231,x1232)+~P9(x1231,x1233,x1234,x1235,x1236,x1237,x1238,x1239)
% 59.88/59.92 [124]P9(x1243,x1242,x1244,x1245,x1246,x1247,x1248,x1249)+~E(x1241,x1242)+~P9(x1243,x1241,x1244,x1245,x1246,x1247,x1248,x1249)
% 59.88/59.92 [125]P9(x1253,x1254,x1252,x1255,x1256,x1257,x1258,x1259)+~E(x1251,x1252)+~P9(x1253,x1254,x1251,x1255,x1256,x1257,x1258,x1259)
% 59.88/59.92 [126]P9(x1263,x1264,x1265,x1262,x1266,x1267,x1268,x1269)+~E(x1261,x1262)+~P9(x1263,x1264,x1265,x1261,x1266,x1267,x1268,x1269)
% 59.88/59.92 [127]P9(x1273,x1274,x1275,x1276,x1272,x1277,x1278,x1279)+~E(x1271,x1272)+~P9(x1273,x1274,x1275,x1276,x1271,x1277,x1278,x1279)
% 59.88/59.92 [128]P9(x1283,x1284,x1285,x1286,x1287,x1282,x1288,x1289)+~E(x1281,x1282)+~P9(x1283,x1284,x1285,x1286,x1287,x1281,x1288,x1289)
% 59.88/59.92 [129]P9(x1293,x1294,x1295,x1296,x1297,x1298,x1292,x1299)+~E(x1291,x1292)+~P9(x1293,x1294,x1295,x1296,x1297,x1298,x1291,x1299)
% 59.88/59.92 [130]P9(x1303,x1304,x1305,x1306,x1307,x1308,x1309,x1302)+~E(x1301,x1302)+~P9(x1303,x1304,x1305,x1306,x1307,x1308,x1309,x1301)
% 59.88/59.92 [131]P6(x1312,x1313,x1314,x1315)+~E(x1311,x1312)+~P6(x1311,x1313,x1314,x1315)
% 59.88/59.92 [132]P6(x1323,x1322,x1324,x1325)+~E(x1321,x1322)+~P6(x1323,x1321,x1324,x1325)
% 59.88/59.92 [133]P6(x1333,x1334,x1332,x1335)+~E(x1331,x1332)+~P6(x1333,x1334,x1331,x1335)
% 59.88/59.92 [134]P6(x1343,x1344,x1345,x1342)+~E(x1341,x1342)+~P6(x1343,x1344,x1345,x1341)
% 59.88/59.92 [135]P10(x1352,x1353,x1354,x1355)+~E(x1351,x1352)+~P10(x1351,x1353,x1354,x1355)
% 59.88/59.92 [136]P10(x1363,x1362,x1364,x1365)+~E(x1361,x1362)+~P10(x1363,x1361,x1364,x1365)
% 59.88/59.92 [137]P10(x1373,x1374,x1372,x1375)+~E(x1371,x1372)+~P10(x1373,x1374,x1371,x1375)
% 59.88/59.92 [138]P10(x1383,x1384,x1385,x1382)+~E(x1381,x1382)+~P10(x1383,x1384,x1385,x1381)
% 59.88/59.92 [139]P4(x1392,x1393,x1394)+~E(x1391,x1392)+~P4(x1391,x1393,x1394)
% 59.88/59.92 [140]P4(x1403,x1402,x1404)+~E(x1401,x1402)+~P4(x1403,x1401,x1404)
% 59.88/59.92 [141]P4(x1413,x1414,x1412)+~E(x1411,x1412)+~P4(x1413,x1414,x1411)
% 59.88/59.92
% 59.88/59.92 %-------------------------------------------
% 59.88/59.93 cnf(266,plain,
% 59.88/59.93 (~P1(a18,a17,a20)),
% 59.88/59.93 inference(scs_inference,[],[152,153])).
% 59.88/59.93 cnf(268,plain,
% 59.88/59.93 (~P1(a17,a20,a18)),
% 59.88/59.93 inference(scs_inference,[],[152,153,154])).
% 59.88/59.93 cnf(272,plain,
% 59.88/59.93 (~P10(a17,a18,a17,a20)),
% 59.88/59.93 inference(scs_inference,[],[152,153,154,155,162])).
% 59.88/59.93 cnf(276,plain,
% 59.88/59.93 (~P10(a17,a20,a17,a18)),
% 59.88/59.93 inference(scs_inference,[],[152,153,154,155,162,156,165])).
% 59.88/59.93 cnf(278,plain,
% 59.88/59.93 (~P10(a17,a18,a20,a17)),
% 59.88/59.93 inference(scs_inference,[],[152,153,154,155,162,156,165,166])).
% 59.88/59.93 cnf(282,plain,
% 59.88/59.93 (~P9(a17,a20,x2821,x2822,a17,a18,x2821,x2822)),
% 59.88/59.93 inference(scs_inference,[],[152,153,154,155,162,156,165,166,235,254])).
% 59.88/59.93 cnf(284,plain,
% 59.88/59.93 (~P9(x2841,x2842,a17,a18,x2841,x2842,a17,a20)),
% 59.88/59.93 inference(scs_inference,[],[152,153,154,155,162,156,165,166,235,254,255])).
% 59.88/59.93 cnf(286,plain,
% 59.88/59.93 (~P9(a18,a17,x2861,x2862,a17,a20,x2861,x2862)),
% 59.88/59.93 inference(scs_inference,[],[152,153,154,155,162,156,165,166,235,254,255,256])).
% 59.88/59.93 cnf(288,plain,
% 59.88/59.93 (~P9(a17,a18,a17,a20,x2881,x2882,x2881,x2882)),
% 59.88/59.93 inference(scs_inference,[],[152,153,154,155,162,156,165,166,235,254,255,256,257])).
% 59.88/59.93 cnf(290,plain,
% 59.88/59.93 (P1(a18,a18,a1)),
% 59.88/59.93 inference(scs_inference,[],[142,152,153,154,155,162,156,165,166,235,254,255,256,257,157])).
% 59.88/59.93 cnf(292,plain,
% 59.88/59.93 (~P10(a18,a17,a17,a20)),
% 59.88/59.93 inference(scs_inference,[],[142,152,153,154,155,162,156,165,166,235,254,255,256,257,157,227])).
% 59.88/59.93 cnf(294,plain,
% 59.88/59.93 (~P11(x2941,a17,a18,x2941,a17,a20)),
% 59.88/59.93 inference(scs_inference,[],[142,152,153,154,155,162,156,165,166,235,254,255,256,257,157,227,233])).
% 59.88/59.93 cnf(296,plain,
% 59.88/59.93 (~P3(x2961,x2962,a16,a2)+P10(x2961,x2962,a16,a1)),
% 59.88/59.93 inference(scs_inference,[],[142,144,152,153,154,155,162,156,165,166,235,254,255,256,257,157,227,233,182])).
% 59.88/59.93 cnf(302,plain,
% 59.88/59.93 (~P3(a16,a2,a2,a16)+P10(a2,a16,a16,a1)),
% 59.88/59.93 inference(scs_inference,[],[142,144,145,152,153,154,155,162,156,165,166,235,254,255,256,257,157,227,233,182,243,244,167])).
% 59.88/59.93 cnf(313,plain,
% 59.88/59.93 (~P9(a20,a17,x3131,x3132,a17,a18,x3131,x3132)),
% 59.88/59.93 inference(scs_inference,[],[282,256])).
% 59.88/59.93 cnf(315,plain,
% 59.88/59.93 (~P1(a18,a20,a17)),
% 59.88/59.93 inference(scs_inference,[],[266,282,256,154])).
% 59.88/59.93 cnf(317,plain,
% 59.88/59.93 (~P9(x3171,x3172,a17,a20,x3171,x3172,a17,a18)),
% 59.88/59.93 inference(scs_inference,[],[266,282,284,256,154,254])).
% 59.88/59.93 cnf(319,plain,
% 59.88/59.93 (~P11(x3191,a17,a20,x3191,a17,a18)),
% 59.88/59.93 inference(scs_inference,[],[266,282,284,294,256,154,254,216])).
% 59.88/59.93 cnf(321,plain,
% 59.88/59.93 (~P10(a18,a17,a18,a20)),
% 59.88/59.93 inference(scs_inference,[],[266,282,284,294,256,154,254,216,162])).
% 59.88/59.93 cnf(323,plain,
% 59.88/59.93 (~P1(a20,a17,a18)),
% 59.88/59.93 inference(scs_inference,[],[266,268,282,284,294,256,154,254,216,162,153])).
% 59.88/59.93 cnf(327,plain,
% 59.88/59.93 (~P9(a17,a20,a17,a18,x3271,x3272,x3271,x3272)),
% 59.88/59.93 inference(scs_inference,[],[266,268,282,284,286,294,256,154,254,216,162,153,255,257])).
% 59.88/59.93 cnf(329,plain,
% 59.88/59.93 (~P10(a20,a17,a17,a18)),
% 59.88/59.93 inference(scs_inference,[],[266,268,282,284,286,294,278,256,154,254,216,162,153,255,257,165])).
% 59.88/59.93 cnf(331,plain,
% 59.88/59.93 (~P11(x3311,a18,a17,x3311,a20,a17)),
% 59.88/59.93 inference(scs_inference,[],[266,268,282,284,286,294,278,256,154,254,216,162,153,255,257,165,218])).
% 59.88/59.93 cnf(333,plain,
% 59.88/59.93 (~P10(a17,a20,a18,a17)),
% 59.88/59.93 inference(scs_inference,[],[266,268,276,282,284,286,294,278,256,154,254,216,162,153,255,257,165,218,166])).
% 59.88/59.93 cnf(335,plain,
% 59.88/59.93 (~P11(a17,x3351,a18,a17,x3351,a20)),
% 59.88/59.93 inference(scs_inference,[],[266,268,276,282,284,286,294,278,256,154,254,216,162,153,255,257,165,218,166,217])).
% 59.88/59.93 cnf(337,plain,
% 59.88/59.93 (~P9(a17,a18,x3371,x3372,a20,a17,x3371,x3372)),
% 59.88/59.93 inference(scs_inference,[],[266,268,276,282,284,286,294,278,256,154,254,216,162,153,255,257,165,218,166,217,235])).
% 59.88/59.93 cnf(341,plain,
% 59.88/59.93 (P1(a15,a15,a16)),
% 59.88/59.93 inference(scs_inference,[],[143,266,268,276,282,284,286,294,278,256,154,254,216,162,153,255,257,165,218,166,217,235,155,157])).
% 59.88/59.93 cnf(347,plain,
% 59.88/59.93 (~P9(a18,a20,a18,x3471,a17,a20,a17,x3471)+P6(x3471,a18,a17,a17)),
% 59.88/59.93 inference(scs_inference,[],[143,266,268,276,282,284,286,294,278,256,154,254,216,162,153,255,257,165,218,166,217,235,155,157,156,236,187])).
% 59.88/59.93 cnf(351,plain,
% 59.88/59.93 (~P1(a20,a18,a17)),
% 59.88/59.93 inference(scs_inference,[],[323,154])).
% 59.88/59.93 cnf(353,plain,
% 59.88/59.93 (~P9(a18,a17,a17,a20,x3531,x3532,x3531,x3532)),
% 59.88/59.93 inference(scs_inference,[],[323,288,154,256])).
% 59.88/59.93 cnf(355,plain,
% 59.88/59.93 (~P10(a20,a17,a20,a18)),
% 59.88/59.93 inference(scs_inference,[],[323,288,154,256,162])).
% 59.88/59.93 cnf(357,plain,
% 59.88/59.93 (~P11(x3571,a20,a17,x3571,a18,a17)),
% 59.88/59.93 inference(scs_inference,[],[323,288,331,154,256,162,216])).
% 59.88/59.93 cnf(359,plain,
% 59.88/59.93 (~P10(a18,a17,a20,a18)),
% 59.88/59.93 inference(scs_inference,[],[323,321,288,331,154,256,162,216,166])).
% 59.88/59.93 cnf(361,plain,
% 59.88/59.93 (~P10(a18,a20,a18,a17)),
% 59.88/59.93 inference(scs_inference,[],[323,321,288,331,154,256,162,216,166,165])).
% 59.88/59.93 cnf(363,plain,
% 59.88/59.93 (~P11(a18,a17,a20,x3631,x3631,x3631)),
% 59.88/59.93 inference(scs_inference,[],[323,321,288,331,154,256,162,216,166,165,233])).
% 59.88/59.93 cnf(365,plain,
% 59.88/59.93 (~P11(a17,a18,x3651,a17,a20,x3651)),
% 59.88/59.93 inference(scs_inference,[],[323,321,288,331,335,154,256,162,216,166,165,233,218])).
% 59.88/59.93 cnf(370,plain,
% 59.88/59.93 (~P9(x3701,x3702,a20,a17,x3701,x3702,a17,a18)),
% 59.88/59.93 inference(scs_inference,[],[323,321,288,313,331,335,154,256,162,216,166,165,233,218,254,255])).
% 59.88/59.93 cnf(374,plain,
% 59.88/59.93 (~P9(x3741,x3742,x3741,x3742,a17,a18,a17,a20)),
% 59.88/59.93 inference(scs_inference,[],[323,321,288,284,313,319,331,335,154,256,162,216,166,165,233,218,254,255,217,257])).
% 59.88/59.93 cnf(376,plain,
% 59.88/59.93 (~P9(a18,a17,x3761,x3762,a18,a20,x3761,x3762)),
% 59.88/59.93 inference(scs_inference,[],[323,321,288,284,313,319,331,335,154,256,162,216,166,165,233,218,254,255,217,257,235])).
% 59.88/59.93 cnf(390,plain,
% 59.88/59.93 (~P10(a20,a17,a18,a20)),
% 59.88/59.93 inference(scs_inference,[],[355,327,256,166])).
% 59.88/59.93 cnf(392,plain,
% 59.88/59.93 (~P11(x3921,x3921,x3921,a18,a17,a20)),
% 59.88/59.93 inference(scs_inference,[],[355,327,363,256,166,216])).
% 59.88/59.93 cnf(394,plain,
% 59.88/59.93 (~P11(a17,a18,a20,x3941,x3941,x3941)),
% 59.88/59.93 inference(scs_inference,[],[355,327,363,256,166,216,217])).
% 59.88/59.93 cnf(396,plain,
% 59.88/59.93 (~P9(a17,a20,x3961,x3962,a18,a17,x3961,x3962)),
% 59.88/59.93 inference(scs_inference,[],[355,286,327,363,256,166,216,217,254])).
% 59.88/59.93 cnf(398,plain,
% 59.88/59.93 (~P10(a20,a18,a20,a17)),
% 59.88/59.93 inference(scs_inference,[],[351,355,286,327,363,256,166,216,217,254,162])).
% 59.88/59.93 cnf(400,plain,
% 59.88/59.93 (~P10(a20,a18,a18,a17)),
% 59.88/59.93 inference(scs_inference,[],[351,355,286,327,363,359,256,166,216,217,254,162,165])).
% 59.88/59.93 cnf(402,plain,
% 59.88/59.93 (~P11(a20,a17,a18,x4021,x4021,x4021)),
% 59.88/59.93 inference(scs_inference,[],[351,355,286,327,363,359,256,166,216,217,254,162,165,233])).
% 59.88/59.93 cnf(406,plain,
% 59.88/59.93 (~P9(a17,a18,a20,a17,x4061,x4062,x4061,x4062)),
% 59.88/59.93 inference(scs_inference,[],[351,355,286,327,337,363,359,256,166,216,217,254,162,165,233,255,257])).
% 59.88/59.93 cnf(408,plain,
% 59.88/59.93 (~P11(a18,a20,a17,x4081,x4081,x4081)),
% 59.88/59.93 inference(scs_inference,[],[351,355,286,327,337,363,359,256,166,216,217,254,162,165,233,255,257,218])).
% 59.88/59.93 cnf(410,plain,
% 59.88/59.93 (~P9(a20,a17,x4101,x4102,a20,a18,x4101,x4102)),
% 59.88/59.93 inference(scs_inference,[],[351,355,286,327,337,363,359,256,166,216,217,254,162,165,233,255,257,218,235])).
% 59.88/59.93 cnf(412,plain,
% 59.88/59.93 (P1(a16,a16,a15)),
% 59.88/59.93 inference(scs_inference,[],[351,341,355,286,327,337,363,359,256,166,216,217,254,162,165,233,255,257,218,235,157])).
% 59.88/59.93 cnf(415,plain,
% 59.88/59.93 (~P10(x4151,x4152,x4153,x4154)+~P9(a17,a18,a17,a20,x4151,x4152,x4153,x4154)),
% 59.88/59.93 inference(scs_inference,[],[147,272,351,341,355,286,327,337,363,359,256,166,216,217,254,162,165,233,255,257,218,235,157,106,242])).
% 59.88/59.93 cnf(426,plain,
% 59.88/59.93 (~P9(a18,a17,x4261,x4262,a20,a17,x4261,x4262)),
% 59.88/59.93 inference(scs_inference,[],[337,256])).
% 59.88/59.93 cnf(428,plain,
% 59.88/59.93 (~P10(a20,a18,a17,a20)),
% 59.88/59.93 inference(scs_inference,[],[398,337,256,166])).
% 59.88/59.93 cnf(430,plain,
% 59.88/59.93 (~P10(a18,a17,a20,a17)),
% 59.88/59.93 inference(scs_inference,[],[398,337,256,166,227])).
% 59.88/59.93 cnf(432,plain,
% 59.88/59.93 (~P9(x4321,x4322,x4321,x4322,a18,a17,a17,a20)),
% 59.88/59.93 inference(scs_inference,[],[398,337,353,256,166,227,254])).
% 59.88/59.93 cnf(436,plain,
% 59.88/59.93 (~P9(a17,a20,a18,a17,x4361,x4362,x4361,x4362)),
% 59.88/59.93 inference(scs_inference,[],[398,337,353,392,256,166,227,254,217,255])).
% 59.88/59.93 cnf(438,plain,
% 59.88/59.93 (~P11(x4381,x4381,x4381,a20,a17,a18)),
% 59.88/59.93 inference(scs_inference,[],[398,337,353,392,402,256,166,227,254,217,255,216])).
% 59.88/59.93 cnf(442,plain,
% 59.88/59.93 (~P10(a18,a20,a20,a17)),
% 59.88/59.93 inference(scs_inference,[],[398,337,353,392,402,390,256,166,227,254,217,255,216,218,165])).
% 59.88/59.93 cnf(444,plain,
% 59.88/59.93 (~P9(a18,a17,a18,a20,x4441,x4442,x4441,x4442)),
% 59.88/59.93 inference(scs_inference,[],[398,337,353,376,392,402,390,256,166,227,254,217,255,216,218,165,257])).
% 59.88/59.93 cnf(446,plain,
% 59.88/59.93 (~P11(a18,a17,x4461,a20,a17,x4461)),
% 59.88/59.93 inference(scs_inference,[],[398,337,353,376,392,402,390,256,166,227,254,217,255,216,218,165,257,233])).
% 59.88/59.93 cnf(448,plain,
% 59.88/59.93 (~P9(a20,a18,x4481,x4482,a20,a17,x4481,x4482)),
% 59.88/59.93 inference(scs_inference,[],[398,337,353,376,392,402,390,256,166,227,254,217,255,216,218,165,257,233,235])).
% 59.88/59.93 cnf(457,plain,
% 59.88/59.93 (~P10(a20,a17,a18,a17)),
% 59.88/59.93 inference(scs_inference,[],[329,166])).
% 59.88/59.93 cnf(459,plain,
% 59.88/59.93 (~P9(x4591,x4592,x4592,x4591,a17,a18,a17,a20)),
% 59.88/59.93 inference(scs_inference,[],[374,329,166,256])).
% 59.88/59.93 cnf(461,plain,
% 59.88/59.93 (~P11(a20,a18,a17,x4611,x4611,x4611)),
% 59.88/59.93 inference(scs_inference,[],[374,329,408,166,256,217])).
% 59.88/59.93 cnf(463,plain,
% 59.88/59.93 (~P9(x4631,x4632,x4631,x4632,a17,a20,a17,a18)),
% 59.88/59.93 inference(scs_inference,[],[374,327,329,408,166,256,217,254])).
% 59.88/59.93 cnf(465,plain,
% 59.88/59.93 (~P10(a17,a20,a20,a18)),
% 59.88/59.93 inference(scs_inference,[],[374,327,329,408,428,166,256,217,254,165])).
% 59.88/59.93 cnf(467,plain,
% 59.88/59.93 (~P9(x4671,x4672,a18,a17,x4671,x4672,a18,a20)),
% 59.88/59.93 inference(scs_inference,[],[374,327,376,329,408,428,166,256,217,254,165,255])).
% 59.88/59.93 cnf(469,plain,
% 59.88/59.93 (~P11(x4691,a18,a17,x4691,a18,a20)),
% 59.88/59.93 inference(scs_inference,[],[374,327,376,329,408,428,166,256,217,254,165,255,233])).
% 59.88/59.93 cnf(471,plain,
% 59.88/59.93 (~P9(x4711,x4712,x4711,x4712,a20,a17,a17,a18)),
% 59.88/59.93 inference(scs_inference,[],[374,327,376,329,408,370,428,166,256,217,254,165,255,233,257])).
% 59.88/59.93 cnf(477,plain,
% 59.88/59.93 (~P9(a18,a20,x4771,x4772,a18,a17,x4771,x4772)),
% 59.88/59.93 inference(scs_inference,[],[374,327,376,329,361,394,408,370,365,428,166,256,217,254,165,255,233,257,216,218,235])).
% 59.88/59.93 cnf(484,plain,
% 59.88/59.93 (~P9(a17,a18,x4841,x4842,a18,a20,x4841,x4842)),
% 59.88/59.93 inference(scs_inference,[],[376,256])).
% 59.88/59.93 cnf(486,plain,
% 59.88/59.93 (~P10(a20,a18,a17,a18)),
% 59.88/59.93 inference(scs_inference,[],[376,400,256,166])).
% 59.88/59.93 cnf(488,plain,
% 59.88/59.93 (~P10(a17,a18,a18,a20)),
% 59.88/59.93 inference(scs_inference,[],[376,400,256,166,227])).
% 59.88/59.93 cnf(490,plain,
% 59.88/59.93 (~P9(x4901,x4902,x4901,x4902,a17,a18,a20,a17)),
% 59.88/59.93 inference(scs_inference,[],[376,406,400,256,166,227,254])).
% 59.88/59.93 cnf(492,plain,
% 59.88/59.93 (~P10(a17,a18,a20,a18)),
% 59.88/59.93 inference(scs_inference,[],[376,406,400,256,166,227,254,165])).
% 59.88/59.93 cnf(502,plain,
% 59.88/59.93 (~P9(a20,a18,x5021,x5022,a18,a17,x5021,x5022)),
% 59.88/59.93 inference(scs_inference,[],[376,396,406,438,461,446,400,256,166,227,254,165,217,216,255,218,235])).
% 59.88/59.93 cnf(504,plain,
% 59.88/59.93 (~P9(a20,a17,a20,a18,x5041,x5042,x5041,x5042)),
% 59.88/59.93 inference(scs_inference,[],[376,396,406,410,438,461,446,400,256,166,227,254,165,217,216,255,218,235,257])).
% 59.88/59.93 cnf(506,plain,
% 59.88/59.93 (~P10(x5061,x5062,x5063,x5064)+~P9(a20,a17,a20,a18,x5061,x5062,x5063,x5064)),
% 59.88/59.93 inference(scs_inference,[],[355,376,396,406,410,438,461,446,400,256,166,227,254,165,217,216,255,218,235,257,242])).
% 59.88/59.93 cnf(508,plain,
% 59.88/59.93 (~P3(x5081,x5082,a16,a2)+~P9(a20,a17,a20,a18,x5081,x5082,a16,a1)),
% 59.88/59.93 inference(scs_inference,[],[144,355,376,396,406,410,438,461,446,400,256,166,227,254,165,217,216,255,218,235,257,242,182])).
% 59.88/59.93 cnf(516,plain,
% 59.88/59.93 (~P10(a18,a20,a17,a20)),
% 59.88/59.93 inference(scs_inference,[],[442,166])).
% 59.88/59.93 cnf(518,plain,
% 59.88/59.93 (~P9(x5181,x5182,x5182,x5181,a18,a17,a17,a20)),
% 59.88/59.93 inference(scs_inference,[],[432,442,166,256])).
% 59.88/59.93 cnf(520,plain,
% 59.88/59.93 (~P9(a20,a17,x5201,x5202,a18,a17,x5201,x5202)),
% 59.88/59.93 inference(scs_inference,[],[426,432,442,166,256,254])).
% 59.88/59.93 cnf(522,plain,
% 59.88/59.93 (~P10(a18,a20,a17,a18)),
% 59.88/59.93 inference(scs_inference,[],[426,432,442,488,166,256,254,165])).
% 59.88/59.93 cnf(524,plain,
% 59.88/59.93 (~P11(x5241,x5242,x5241,a18,a17,a20)),
% 59.88/59.93 inference(scs_inference,[],[426,432,442,488,166,256,254,165,233])).
% 59.88/59.93 cnf(528,plain,
% 59.88/59.93 (~P11(x5281,a17,a18,x5281,a20,a18)),
% 59.88/59.93 inference(scs_inference,[],[426,432,442,357,469,488,166,256,254,165,233,217,218])).
% 59.88/59.93 cnf(530,plain,
% 59.88/59.93 (~P9(a18,a17,a20,a17,x5301,x5302,x5301,x5302)),
% 59.88/59.93 inference(scs_inference,[],[426,432,442,357,469,488,166,256,254,165,233,217,218,257])).
% 59.88/59.93 cnf(532,plain,
% 59.88/59.93 (~P11(x5321,a18,a20,x5321,a18,a17)),
% 59.88/59.93 inference(scs_inference,[],[426,432,442,357,469,488,166,256,254,165,233,217,218,257,216])).
% 59.88/59.93 cnf(534,plain,
% 59.88/59.93 (~P9(a18,a20,x5341,x5342,a20,a17,x5341,x5342)),
% 59.88/59.93 inference(scs_inference,[],[426,432,442,357,469,488,166,256,254,165,233,217,218,257,216,235])).
% 59.88/59.93 cnf(536,plain,
% 59.88/59.93 (~P9(x5361,x5362,a18,a17,x5361,x5362,a20,a17)),
% 59.88/59.93 inference(scs_inference,[],[426,432,442,357,469,488,166,256,254,165,233,217,218,257,216,235,255])).
% 59.88/59.93 cnf(551,plain,
% 59.88/59.93 (~P9(a20,a17,a18,a17,x5511,x5512,x5511,x5512)),
% 59.88/59.93 inference(scs_inference,[],[436,256])).
% 59.88/59.93 cnf(553,plain,
% 59.88/59.93 (~P10(a17,a20,a18,a20)),
% 59.88/59.93 inference(scs_inference,[],[436,465,256,166])).
% 59.88/59.93 cnf(558,plain,
% 59.88/59.93 (~P9(x5581,x5582,x5581,x5582,a17,a20,a18,a17)),
% 59.88/59.93 inference(scs_inference,[],[436,465,520,256,166,233,254])).
% 59.88/59.93 cnf(560,plain,
% 59.88/59.93 (~P11(a18,a17,a20,x5601,x5602,x5601)),
% 59.88/59.93 inference(scs_inference,[],[436,465,520,524,256,166,233,254,216])).
% 59.88/59.93 cnf(562,plain,
% 59.88/59.93 (~P9(a18,a20,a18,a17,x5621,x5622,x5621,x5622)),
% 59.88/59.93 inference(scs_inference,[],[436,444,465,520,524,256,166,233,254,216,255])).
% 59.88/59.93 cnf(564,plain,
% 59.88/59.93 (~P11(x5641,x5642,x5642,a17,a18,a20)),
% 59.88/59.93 inference(scs_inference,[],[436,444,465,520,524,256,166,233,254,216,255,217])).
% 59.88/59.93 cnf(568,plain,
% 59.88/59.93 (~P11(x5681,x5681,x5682,a18,a20,a17)),
% 59.88/59.93 inference(scs_inference,[],[436,444,465,520,524,256,166,233,254,216,255,217,235,218])).
% 59.88/59.93 cnf(570,plain,
% 59.88/59.93 (~P9(a20,a18,a20,a17,x5701,x5702,x5701,x5702)),
% 59.88/59.93 inference(scs_inference,[],[436,444,448,465,520,524,256,166,233,254,216,255,217,235,218,257])).
% 59.88/59.93 cnf(572,plain,
% 59.88/59.93 (~P10(x5721,x5722,x5723,x5724)+~P9(a18,a17,a18,a20,x5721,x5722,x5723,x5724)),
% 59.88/59.93 inference(scs_inference,[],[321,436,444,448,465,520,524,256,166,233,254,216,255,217,235,218,257,242])).
% 59.88/59.93 cnf(574,plain,
% 59.88/59.93 (~P3(x5741,x5742,a16,a2)+~P9(a18,a17,a18,a20,x5741,x5742,a16,a1)),
% 59.88/59.93 inference(scs_inference,[],[144,321,436,444,448,465,520,524,256,166,233,254,216,255,217,235,218,257,242,182])).
% 59.88/59.93 cnf(585,plain,
% 59.88/59.93 (~P9(x5851,x5852,x5852,x5851,a20,a17,a17,a18)),
% 59.88/59.93 inference(scs_inference,[],[471,256])).
% 59.88/59.93 cnf(587,plain,
% 59.88/59.93 (~P9(x5871,x5872,x5871,x5872,a18,a17,a18,a20)),
% 59.88/59.93 inference(scs_inference,[],[471,444,256,254])).
% 59.88/59.93 cnf(589,plain,
% 59.88/59.93 (~P11(a17,a18,a20,x5891,x5892,x5892)),
% 59.88/59.93 inference(scs_inference,[],[471,444,564,256,254,216])).
% 59.88/59.93 cnf(591,plain,
% 59.88/59.93 (~P11(x5911,x5912,x5911,a20,a17,a18)),
% 59.88/59.93 inference(scs_inference,[],[471,444,564,256,254,216,233])).
% 59.88/59.93 cnf(595,plain,
% 59.88/59.93 (~P9(x5951,x5952,a20,a17,x5951,x5952,a20,a18)),
% 59.88/59.93 inference(scs_inference,[],[471,410,444,560,564,256,254,216,233,218,255])).
% 59.88/59.93 cnf(597,plain,
% 59.88/59.93 (~P11(x5971,x5971,x5972,a20,a18,a17)),
% 59.88/59.93 inference(scs_inference,[],[471,410,444,560,564,568,256,254,216,233,218,255,217])).
% 59.88/59.93 cnf(601,plain,
% 59.88/59.93 (~P9(a17,a18,x6011,x6012,a20,a18,x6011,x6012)),
% 59.88/59.93 inference(scs_inference,[],[471,410,444,459,492,560,564,568,256,254,216,233,218,255,217,257,235])).
% 59.88/59.93 cnf(603,plain,
% 59.88/59.93 (~P10(x6031,x6032,x6033,x6034)+~P9(a20,a18,a20,a17,x6031,x6032,x6033,x6034)),
% 59.88/59.93 inference(scs_inference,[],[398,471,410,444,459,492,560,564,568,256,254,216,233,218,255,217,257,235,242])).
% 59.88/59.93 cnf(605,plain,
% 59.88/59.93 (~P3(x6051,x6052,a16,a2)+~P9(a20,a18,a20,a17,x6051,x6052,a16,a1)),
% 59.88/59.93 inference(scs_inference,[],[144,398,471,410,444,459,492,560,564,568,256,254,216,233,218,255,217,257,235,242,182])).
% 59.88/59.93 cnf(608,plain,
% 59.88/59.93 (~P9(a17,a18,a18,a20,x6081,x6082,x6081,x6082)),
% 59.88/59.93 inference(scs_inference,[],[444,256])).
% 59.88/59.93 cnf(610,plain,
% 59.88/59.93 (~P9(a18,a20,x6101,x6102,a17,a18,x6101,x6102)),
% 59.88/59.93 inference(scs_inference,[],[444,484,256,254])).
% 59.88/59.93 cnf(614,plain,
% 59.88/59.93 (~P11(x6141,a20,a17,x6141,a20,a18)),
% 59.88/59.93 inference(scs_inference,[],[444,484,595,589,256,254,218,233])).
% 59.88/59.93 cnf(619,plain,
% 59.88/59.93 (~P9(x6191,x6192,a20,a18,x6191,x6192,a20,a17)),
% 59.88/59.93 inference(scs_inference,[],[448,444,484,595,589,591,256,254,218,233,216,255])).
% 59.88/59.93 cnf(621,plain,
% 59.88/59.93 (~P9(a20,a18,x6211,x6212,a17,a18,x6211,x6212)),
% 59.88/59.93 inference(scs_inference,[],[448,444,486,484,595,589,591,256,254,218,233,216,255,235])).
% 59.88/59.93 cnf(625,plain,
% 59.88/59.93 (~P9(a20,a18,a18,a17,x6251,x6252,x6251,x6252)),
% 59.88/59.93 inference(scs_inference,[],[448,444,486,484,502,595,589,591,256,254,218,233,216,255,235,217,257])).
% 59.88/59.93 cnf(627,plain,
% 59.88/59.93 (~P10(x6271,x6272,x6273,x6274)+~P9(a18,a17,a17,a20,x6271,x6272,x6273,x6274)),
% 59.88/59.93 inference(scs_inference,[],[448,444,292,486,484,502,595,589,591,256,254,218,233,216,255,235,217,257,242])).
% 59.88/59.93 cnf(629,plain,
% 59.88/59.93 (~P3(x6291,x6292,a16,a2)+~P9(a18,a17,a17,a20,x6291,x6292,a16,a1)),
% 59.88/59.93 inference(scs_inference,[],[144,448,444,292,486,484,502,595,589,591,256,254,218,233,216,255,235,217,257,242,182])).
% 59.88/59.93 cnf(647,plain,
% 59.88/59.93 (~P9(x6471,x6472,x6471,x6472,a20,a17,a20,a18)),
% 59.88/59.93 inference(scs_inference,[],[463,504,256,254])).
% 59.88/59.93 cnf(651,plain,
% 59.88/59.93 (~P11(a17,a18,x6511,a20,a18,x6511)),
% 59.88/59.93 inference(scs_inference,[],[463,504,601,597,256,254,216,233])).
% 59.88/59.93 cnf(656,plain,
% 59.88/59.93 (~P9(x6561,x6562,a18,a20,x6561,x6562,a18,a17)),
% 59.88/59.93 inference(scs_inference,[],[463,477,504,601,597,532,256,254,216,233,218,255])).
% 59.88/59.93 cnf(660,plain,
% 59.88/59.93 (~P9(a18,a20,x6601,x6602,a17,a20,x6601,x6602)),
% 59.88/59.93 inference(scs_inference,[],[516,463,477,504,518,601,597,532,256,254,216,233,218,255,257,235])).
% 59.88/59.93 cnf(664,plain,
% 59.88/59.93 (~P10(x6641,x6642,x6643,x6644)+~P9(a17,a20,a18,a17,x6641,x6642,x6643,x6644)),
% 59.88/59.93 inference(scs_inference,[],[333,516,463,477,504,518,601,597,528,532,256,254,216,233,218,255,257,235,217,242])).
% 59.88/59.93 cnf(666,plain,
% 59.88/59.93 (~P3(x6661,x6662,a16,a2)+~P9(a17,a20,a18,a17,x6661,x6662,a16,a1)),
% 59.88/59.93 inference(scs_inference,[],[144,333,516,463,477,504,518,601,597,528,532,256,254,216,233,218,255,257,235,217,242,182])).
% 59.88/59.93 cnf(682,plain,
% 59.88/59.93 (~P9(x6821,x6822,x6822,x6821,a17,a18,a20,a17)),
% 59.88/59.93 inference(scs_inference,[],[490,256])).
% 59.88/59.93 cnf(684,plain,
% 59.88/59.93 (~P9(a17,a18,a17,a20,x6841,x6842,x6842,x6841)),
% 59.88/59.93 inference(scs_inference,[],[490,459,256,254])).
% 59.88/59.93 cnf(686,plain,
% 59.88/59.93 (~P11(a20,a18,x6861,a17,a18,x6861)),
% 59.88/59.93 inference(scs_inference,[],[490,459,621,256,254,233])).
% 59.88/59.93 cnf(689,plain,
% 59.88/59.93 (~P11(x6891,a17,a20,x6891,a18,a20)),
% 59.88/59.93 inference(scs_inference,[],[490,459,621,614,256,254,233,218])).
% 59.88/59.93 cnf(695,plain,
% 59.88/59.93 (~P11(a20,x6951,a17,a20,x6951,a18)),
% 59.88/59.93 inference(scs_inference,[],[490,459,484,621,614,256,254,233,218,216,255,217])).
% 59.88/59.93 cnf(697,plain,
% 59.88/59.93 (~P9(a18,a20,a20,a17,x6971,x6972,x6971,x6972)),
% 59.88/59.93 inference(scs_inference,[],[490,459,484,534,621,614,256,254,233,218,216,255,217,257])).
% 59.88/59.93 cnf(699,plain,
% 59.88/59.93 (~P9(a18,a17,x6991,x6992,a20,a18,x6991,x6992)),
% 59.88/59.93 inference(scs_inference,[],[359,490,459,484,534,621,614,256,254,233,218,216,255,217,257,235])).
% 59.88/59.93 cnf(706,plain,
% 59.88/59.93 (~P10(x7061,x7062,x7063,x7064)+~P9(a18,a17,a20,a17,x7061,x7062,x7063,x7064)),
% 59.88/59.93 inference(scs_inference,[],[143,148,315,430,359,490,459,484,534,621,614,256,254,233,218,216,255,217,257,235,89,88,236,106,242])).
% 59.88/59.93 cnf(708,plain,
% 59.88/59.93 (~P3(x7081,x7082,a16,a2)+~P9(a18,a17,a20,a17,x7081,x7082,a16,a1)),
% 59.88/59.93 inference(scs_inference,[],[143,144,148,315,430,359,490,459,484,534,621,614,256,254,233,218,216,255,217,257,235,89,88,236,106,242,182])).
% 59.88/59.93 cnf(715,plain,
% 59.88/59.93 (~P9(a17,a20,a20,a18,x7151,x7152,x7151,x7152)),
% 59.88/59.93 inference(scs_inference,[],[504,256])).
% 59.88/59.93 cnf(717,plain,
% 59.88/59.93 (~P9(x7171,x7172,x7171,x7172,a18,a17,a20,a17)),
% 59.88/59.93 inference(scs_inference,[],[504,530,256,254])).
% 59.88/59.93 cnf(721,plain,
% 59.88/59.93 (~P11(x7211,a18,a20,x7211,a17,a20)),
% 59.88/59.93 inference(scs_inference,[],[504,530,686,689,256,254,218,216])).
% 59.88/59.93 cnf(723,plain,
% 59.88/59.93 (~P11(a18,a20,x7231,a17,a20,x7231)),
% 59.88/59.93 inference(scs_inference,[],[504,530,660,686,689,256,254,218,216,233])).
% 59.88/59.93 cnf(726,plain,
% 59.88/59.93 (~P9(a20,a17,x7261,x7262,a18,a20,x7261,x7262)),
% 59.88/59.93 inference(scs_inference,[],[390,504,530,660,686,689,256,254,218,216,233,235])).
% 59.88/59.93 cnf(730,plain,
% 59.88/59.93 (~P11(a18,a17,x7301,a18,a20,x7301)),
% 59.88/59.93 inference(scs_inference,[],[390,502,504,530,660,651,686,689,256,254,218,216,233,235,255,217])).
% 59.88/59.93 cnf(739,plain,
% 59.88/59.93 (~P9(x7391,x7392,x7392,x7391,a17,a20,a18,a17)),
% 59.88/59.93 inference(scs_inference,[],[558,256])).
% 59.88/59.93 cnf(741,plain,
% 59.88/59.93 (~P9(a18,a17,a17,a20,x7411,x7412,x7412,x7411)),
% 59.88/59.93 inference(scs_inference,[],[518,558,256,254])).
% 59.88/59.93 cnf(749,plain,
% 59.88/59.93 (~P9(a18,a20,a17,a18,x7491,x7492,x7491,x7492)),
% 59.88/59.93 inference(scs_inference,[],[428,518,558,610,695,256,254,216,218,235,257])).
% 59.88/59.93 cnf(753,plain,
% 59.88/59.93 (~P11(a18,x7531,a20,a17,x7531,a20)),
% 59.88/59.93 inference(scs_inference,[],[428,518,534,558,610,695,721,256,254,216,218,235,257,255,217])).
% 59.88/59.93 cnf(767,plain,
% 59.88/59.93 (~P9(x7671,x7672,x7671,x7672,a20,a17,a18,a17)),
% 59.88/59.93 inference(scs_inference,[],[551,254])).
% 59.88/59.93 cnf(769,plain,
% 59.88/59.93 (~P9(x7691,x7692,x7692,x7691,a18,a17,a18,a20)),
% 59.88/59.93 inference(scs_inference,[],[551,587,254,256])).
% 59.88/59.93 cnf(775,plain,
% 59.88/59.93 (~P9(a17,a20,x7751,x7752,a18,a20,x7751,x7752)),
% 59.88/59.93 inference(scs_inference,[],[553,551,587,723,730,254,256,218,216,235])).
% 59.88/59.93 cnf(777,plain,
% 59.88/59.93 (~P9(a17,a18,a20,a18,x7771,x7772,x7771,x7772)),
% 59.88/59.93 inference(scs_inference,[],[553,551,587,601,723,730,254,256,218,216,235,257])).
% 59.88/59.93 cnf(790,plain,
% 59.88/59.93 (~P10(x7901,x7902,x7903,x7904)+~P9(a20,a17,a18,a17,x7901,x7902,x7903,x7904)),
% 59.88/59.94 inference(scs_inference,[],[143,351,412,457,553,374,520,551,587,601,723,730,254,256,218,216,235,257,255,217,229,89,236,90,242])).
% 59.88/59.94 cnf(792,plain,
% 59.88/59.94 (~P3(x7921,x7922,a16,a2)+~P9(a20,a17,a18,a17,x7921,x7922,a16,a1)),
% 59.88/59.94 inference(scs_inference,[],[143,144,351,412,457,553,374,520,551,587,601,723,730,254,256,218,216,235,257,255,217,229,89,236,90,242,182])).
% 59.88/59.94 cnf(800,plain,
% 59.88/59.94 (~P9(x8001,x8002,x8002,x8001,a20,a17,a20,a18)),
% 59.88/59.94 inference(scs_inference,[],[647,256])).
% 59.88/59.94 cnf(802,plain,
% 59.88/59.94 (~P9(a20,a17,a17,a18,x8021,x8022,x8022,x8021)),
% 59.88/59.94 inference(scs_inference,[],[585,647,256,254])).
% 59.88/59.94 cnf(806,plain,
% 59.88/59.94 (~P9(a20,a18,a17,a18,x8061,x8062,x8061,x8062)),
% 59.88/59.94 inference(scs_inference,[],[585,621,647,753,256,254,216,257])).
% 59.88/59.94 cnf(821,plain,
% 59.88/59.94 (~P9(x8211,x8212,x8211,x8212,a17,a18,a18,a20)),
% 59.88/59.94 inference(scs_inference,[],[608,254])).
% 59.88/59.94 cnf(825,plain,
% 59.88/59.94 (~P9(a18,a20,a17,a20,x8251,x8252,x8251,x8252)),
% 59.88/59.94 inference(scs_inference,[],[608,660,317,254,256,257])).
% 59.88/59.94 cnf(832,plain,
% 59.88/59.94 (~P10(x8321,x8322,x8323,x8324)+~P9(a18,a20,a17,a18,x8321,x8322,x8323,x8324)),
% 59.88/59.94 inference(scs_inference,[],[151,290,522,608,625,660,317,254,256,257,255,105,106,89,242])).
% 59.88/59.94 cnf(844,plain,
% 59.88/59.94 (~P9(x8441,x8442,x8441,x8442,a20,a18,a18,a17)),
% 59.88/59.94 inference(scs_inference,[],[625,467,256,254])).
% 59.88/59.94 cnf(855,plain,
% 59.88/59.94 (~P9(x8551,x8552,x8551,x8552,a18,a20,a20,a17)),
% 59.88/59.94 inference(scs_inference,[],[697,254])).
% 59.88/59.94 cnf(876,plain,
% 59.88/59.94 (~P9(x8761,x8762,x8761,x8762,a17,a20,a20,a18)),
% 59.88/59.94 inference(scs_inference,[],[715,254])).
% 59.88/59.94 cnf(880,plain,
% 59.88/59.94 (~P9(a17,a20,a18,a20,x8801,x8802,x8801,x8802)),
% 59.88/59.94 inference(scs_inference,[],[715,775,656,254,256,257])).
% 59.88/59.94 cnf(890,plain,
% 59.88/59.94 (~P9(a17,a20,a17,a18,x8901,x8902,x8902,x8901)),
% 59.88/59.94 inference(scs_inference,[],[802,256])).
% 59.88/59.94 cnf(892,plain,
% 59.88/59.94 (~P9(x8921,x8922,x8921,x8922,a18,a20,a18,a17)),
% 59.88/59.94 inference(scs_inference,[],[562,802,256,254])).
% 59.88/59.94 cnf(896,plain,
% 59.88/59.94 (~P9(x8961,x8962,a18,a20,x8961,x8962,a17,a20)),
% 59.88/59.94 inference(scs_inference,[],[660,562,684,802,256,254,257,255])).
% 59.88/59.94 cnf(912,plain,
% 59.88/59.94 (~P9(x9121,x9122,x9121,x9122,a20,a18,a20,a17)),
% 59.88/59.94 inference(scs_inference,[],[570,254])).
% 59.88/59.94 cnf(914,plain,
% 59.88/59.94 (~P9(x9141,x9142,x9142,x9141,a18,a17,a20,a17)),
% 59.88/59.94 inference(scs_inference,[],[570,717,254,256])).
% 59.88/59.94 cnf(932,plain,
% 59.88/59.94 (~P9(x9321,x9322,x9322,x9321,a17,a18,a18,a20)),
% 59.88/59.94 inference(scs_inference,[],[821,256])).
% 59.88/59.94 cnf(934,plain,
% 59.88/59.94 (~P9(a17,a18,a20,a17,x9341,x9342,x9342,x9341)),
% 59.88/59.94 inference(scs_inference,[],[682,821,256,254])).
% 59.88/59.94 cnf(938,plain,
% 59.88/59.94 (~P9(a17,a20,a18,a17,x9381,x9382,x9382,x9381)),
% 59.88/59.94 inference(scs_inference,[],[741,682,821,739,256,254,257,255])).
% 59.88/59.94 cnf(942,plain,
% 59.88/59.94 (~P11(x9421,x9421,x9422,a17,a20,a18)),
% 59.88/59.94 inference(scs_inference,[],[741,682,821,739,256,254,257,255,233,218])).
% 59.88/59.94 cnf(944,plain,
% 59.88/59.94 (~P11(a17,a18,a20,x9441,x9442,x9441)),
% 59.88/59.94 inference(scs_inference,[],[741,682,821,739,256,254,257,255,233,218,216])).
% 59.88/59.94 cnf(946,plain,
% 59.88/59.94 (~P11(x9461,x9462,x9462,a18,a17,a20)),
% 59.88/59.94 inference(scs_inference,[],[741,682,821,739,256,254,257,255,233,218,216,217])).
% 59.88/59.94 cnf(951,plain,
% 59.88/59.94 (~P10(x9511,x9512,x9513,x9514)+~P9(a17,a20,a17,a18,x9511,x9512,x9513,x9514)),
% 59.88/59.94 inference(scs_inference,[],[276,741,587,682,821,739,256,254,257,255,233,218,216,217,229,242])).
% 59.88/59.94 cnf(954,plain,
% 59.88/59.94 (~P3(x9541,x9542,a16,a2)+~P9(a17,a20,a17,a18,x9541,x9542,a16,a1)),
% 59.88/59.94 inference(scs_inference,[],[144,146,276,741,587,682,821,739,256,254,257,255,233,218,216,217,229,242,106,182])).
% 59.88/59.94 cnf(961,plain,
% 59.88/59.94 (~P9(x9611,x9612,x9611,x9612,a18,a20,a17,a18)),
% 59.88/59.94 inference(scs_inference,[],[749,254])).
% 59.88/59.94 cnf(963,plain,
% 59.88/59.94 (~P9(x9631,x9632,x9632,x9631,a20,a17,a18,a17)),
% 59.88/59.94 inference(scs_inference,[],[749,767,254,256])).
% 59.88/59.94 cnf(965,plain,
% 59.88/59.94 (~P11(a17,a20,a18,x9651,x9651,x9652)),
% 59.88/59.94 inference(scs_inference,[],[749,767,944,254,256,218])).
% 59.88/59.94 cnf(967,plain,
% 59.88/59.94 (~P11(a18,a17,a20,x9671,x9672,x9672)),
% 59.88/59.94 inference(scs_inference,[],[749,767,944,946,254,256,218,216])).
% 59.88/59.94 cnf(975,plain,
% 59.88/59.94 (~P10(x9751,x9752,x9753,x9754)+~P9(a20,a17,a17,a18,x9751,x9752,x9753,x9754)),
% 59.88/59.94 inference(scs_inference,[],[329,775,749,767,800,942,944,946,254,256,218,216,217,257,255,242])).
% 59.88/59.94 cnf(977,plain,
% 59.88/59.94 (~P3(x9771,x9772,a16,a2)+~P9(a20,a17,a17,a18,x9771,x9772,a16,a1)),
% 59.88/59.94 inference(scs_inference,[],[144,329,775,749,767,800,942,944,946,254,256,218,216,217,257,255,242,182])).
% 59.88/59.94 cnf(992,plain,
% 59.88/59.94 (~P9(x9921,x9922,x9922,x9921,a20,a18,a18,a17)),
% 59.88/59.94 inference(scs_inference,[],[844,256])).
% 59.88/59.94 cnf(994,plain,
% 59.88/59.94 (~P9(a18,a17,a18,a20,x9941,x9942,x9942,x9941)),
% 59.88/59.94 inference(scs_inference,[],[844,769,256,254])).
% 59.88/59.94 cnf(998,plain,
% 59.88/59.94 (~P11(a20,a17,a18,x9981,x9981,x9982)),
% 59.88/59.94 inference(scs_inference,[],[844,769,965,967,256,254,218,217])).
% 59.88/59.94 cnf(1008,plain,
% 59.88/59.94 (~P10(x10081,x10082,x10083,x10084)+~P9(a18,a20,a18,a17,x10081,x10082,x10083,x10084)),
% 59.88/59.94 inference(scs_inference,[],[361,610,844,769,890,965,967,256,254,218,217,216,257,255,233,242])).
% 59.88/59.94 cnf(1010,plain,
% 59.88/59.94 (~P3(x10101,x10102,a16,a2)+~P9(a18,a20,a18,a17,x10101,x10102,a16,a1)),
% 59.88/59.94 inference(scs_inference,[],[144,361,610,844,769,890,965,967,256,254,218,217,216,257,255,233,242,182])).
% 59.88/59.94 cnf(1026,plain,
% 59.88/59.94 (~P9(x10261,x10262,x10261,x10262,a17,a18,a20,a18)),
% 59.88/59.94 inference(scs_inference,[],[777,254])).
% 59.88/59.94 cnf(1028,plain,
% 59.88/59.94 (~P9(x10281,x10282,x10282,x10281,a18,a20,a20,a17)),
% 59.88/59.94 inference(scs_inference,[],[777,855,254,256])).
% 59.88/59.94 cnf(1036,plain,
% 59.88/59.94 (~P11(x10361,x10362,x10361,a18,a20,a17)),
% 59.88/59.94 inference(scs_inference,[],[699,777,855,914,998,254,256,218,257,255,233])).
% 59.88/59.94 cnf(1038,plain,
% 59.88/59.94 (~P11(a18,a20,a17,x10381,x10382,x10381)),
% 59.88/59.94 inference(scs_inference,[],[699,777,855,914,998,254,256,218,257,255,233,216])).
% 59.88/59.94 cnf(1040,plain,
% 59.88/59.94 (~P11(x10401,x10402,x10402,a20,a18,a17)),
% 59.88/59.94 inference(scs_inference,[],[699,777,855,914,998,254,256,218,257,255,233,216,217])).
% 59.88/59.94 cnf(1054,plain,
% 59.88/59.94 (~P9(x10541,x10542,x10542,x10541,a17,a20,a20,a18)),
% 59.88/59.94 inference(scs_inference,[],[876,256])).
% 59.88/59.94 cnf(1056,plain,
% 59.88/59.94 (~P9(x10561,x10562,x10561,x10562,a20,a18,a17,a18)),
% 59.88/59.94 inference(scs_inference,[],[806,876,256,254])).
% 59.88/59.94 cnf(1058,plain,
% 59.88/59.94 (~P11(x10581,x10581,x10582,a18,a17,a20)),
% 59.88/59.94 inference(scs_inference,[],[806,876,1036,256,254,218])).
% 59.88/59.94 cnf(1062,plain,
% 59.88/59.94 (~P11(a18,a17,a20,x10621,x10621,x10622)),
% 59.88/59.94 inference(scs_inference,[],[806,876,1036,1038,256,254,218,217,216])).
% 59.88/59.94 cnf(1068,plain,
% 59.88/59.94 (~P11(x10681,x10682,x10681,a17,a20,a18)),
% 59.88/59.94 inference(scs_inference,[],[726,806,876,932,1036,1038,256,254,218,217,216,257,255,233])).
% 59.88/59.94 cnf(1070,plain,
% 59.88/59.94 (~P10(x10701,x10702,x10703,x10704)+~P9(a20,a18,a17,a18,x10701,x10702,x10703,x10704)),
% 59.88/59.94 inference(scs_inference,[],[486,726,806,876,932,1036,1038,256,254,218,217,216,257,255,233,242])).
% 59.88/59.94 cnf(1072,plain,
% 59.88/59.94 (~P3(x10721,x10722,a16,a2)+~P9(a20,a18,a17,a18,x10721,x10722,a16,a1)),
% 59.88/59.94 inference(scs_inference,[],[144,486,726,806,876,932,1036,1038,256,254,218,217,216,257,255,233,242,182])).
% 59.88/59.94 cnf(1087,plain,
% 59.88/59.94 (~P9(a20,a17,a20,a18,x10871,x10872,x10872,x10871)),
% 59.88/59.94 inference(scs_inference,[],[800,254])).
% 59.88/59.94 cnf(1089,plain,
% 59.88/59.94 (~P9(x10891,x10892,x10892,x10891,a18,a20,a18,a17)),
% 59.88/59.94 inference(scs_inference,[],[800,892,254,256])).
% 59.88/59.94 cnf(1093,plain,
% 59.88/59.94 (~P11(x10931,x10932,x10932,a20,a17,a18)),
% 59.88/59.94 inference(scs_inference,[],[800,892,1040,1068,254,256,216,218])).
% 59.88/59.94 cnf(1097,plain,
% 59.88/59.94 (~P9(a17,a18,x10971,x10972,a20,a17,x10972,x10971)),
% 59.88/59.94 inference(scs_inference,[],[800,892,934,1040,1058,1068,254,256,216,218,217,257])).
% 59.88/59.94 cnf(1116,plain,
% 59.88/59.94 (~P9(x11161,x11162,x11161,x11162,a18,a20,a17,a20)),
% 59.88/59.94 inference(scs_inference,[],[825,912,256,254])).
% 59.88/59.94 cnf(1126,plain,
% 59.88/59.94 (~P4(a20,x11261,a18)+~P2(a17,a17,x11261,a18)),
% 59.88/59.94 inference(scs_inference,[],[844,284,825,912,938,1062,1093,256,254,217,216,257,255,229])).
% 59.88/59.94 cnf(1132,plain,
% 59.88/59.94 (~P9(x11321,x11322,x11321,x11322,a17,a20,a18,a20)),
% 59.88/59.94 inference(scs_inference,[],[880,254])).
% 59.88/59.94 cnf(1147,plain,
% 59.88/59.94 (~P9(a17,a18,a18,a20,x11471,x11472,x11472,x11471)),
% 59.88/59.94 inference(scs_inference,[],[932,938,256,254])).
% 59.88/59.94 cnf(1153,plain,
% 59.88/59.94 (~P10(x11531,x11532,x11533,x11534)+~P9(a17,a18,a18,a20,x11531,x11532,x11533,x11534)),
% 59.88/59.94 inference(scs_inference,[],[488,876,932,1028,938,256,254,257,255,242])).
% 59.88/59.94 cnf(1155,plain,
% 59.88/59.94 (~P3(x11551,x11552,a16,a2)+~P9(a17,a18,a18,a20,x11551,x11552,a16,a1)),
% 59.88/59.94 inference(scs_inference,[],[144,488,876,932,1028,938,256,254,257,255,242,182])).
% 59.88/59.94 cnf(1170,plain,
% 59.88/59.94 (~P9(a20,a18,a18,a17,x11701,x11702,x11702,x11701)),
% 59.88/59.94 inference(scs_inference,[],[992,254])).
% 59.88/59.94 cnf(1172,plain,
% 59.88/59.94 (~P9(x11721,x11722,x11722,x11721,a18,a20,a17,a18)),
% 59.88/59.94 inference(scs_inference,[],[992,961,254,256])).
% 59.88/59.94 cnf(1176,plain,
% 59.88/59.94 (~P9(x11761,x11762,x11762,x11761,a18,a17,a20,a18)),
% 59.88/59.94 inference(scs_inference,[],[992,1054,961,254,256,257,255])).
% 59.88/59.94 cnf(1178,plain,
% 59.88/59.94 (~P10(x11781,x11782,x11783,x11784)+~P9(a17,a18,a20,a18,x11781,x11782,x11783,x11784)),
% 59.88/59.94 inference(scs_inference,[],[492,992,1054,961,254,256,257,255,242])).
% 59.88/59.94 cnf(1180,plain,
% 59.88/59.94 (~P3(x11801,x11802,a16,a2)+~P9(a17,a18,a20,a18,x11801,x11802,a16,a1)),
% 59.88/59.94 inference(scs_inference,[],[144,492,992,1054,961,254,256,257,255,242,182])).
% 59.88/59.94 cnf(1195,plain,
% 59.88/59.94 (~P9(x11951,x11952,x11952,x11951,a17,a18,a20,a18)),
% 59.88/59.94 inference(scs_inference,[],[1026,256])).
% 59.88/59.94 cnf(1203,plain,
% 59.88/59.94 (~P10(x12031,x12032,x12033,x12034)+~P9(a18,a20,a17,a20,x12031,x12032,x12033,x12034)),
% 59.88/59.94 inference(scs_inference,[],[516,1028,963,1026,256,254,257,255,242])).
% 59.88/59.94 cnf(1205,plain,
% 59.88/59.94 (~P3(x12051,x12052,a16,a2)+~P9(a18,a20,a17,a20,x12051,x12052,a16,a1)),
% 59.88/59.94 inference(scs_inference,[],[144,516,1028,963,1026,256,254,257,255,242,182])).
% 59.88/59.94 cnf(1224,plain,
% 59.88/59.94 (~P9(a18,a17,x12241,x12242,a18,a20,x12242,x12241)),
% 59.88/59.94 inference(scs_inference,[],[1054,994,1056,254,256,257])).
% 59.88/59.94 cnf(1232,plain,
% 59.88/59.94 (~P11(a17,a18,a20,a20,a18,a17)),
% 59.88/59.94 inference(scs_inference,[],[1054,994,1056,254,256,257,255,233,218,217])).
% 59.88/59.94 cnf(1236,plain,
% 59.88/59.94 (~P10(x12361,x12362,x12363,x12364)+~P9(a17,a18,a20,a17,x12361,x12362,x12363,x12364)),
% 59.88/59.94 inference(scs_inference,[],[278,1054,994,1056,254,256,257,255,233,218,217,216,242])).
% 59.88/59.94 cnf(1238,plain,
% 59.88/59.94 (~P3(x12381,x12382,a16,a2)+~P9(a17,a18,a20,a17,x12381,x12382,a16,a1)),
% 59.88/59.94 inference(scs_inference,[],[144,278,1054,994,1056,254,256,257,255,233,218,217,216,242,182])).
% 59.88/59.94 cnf(1261,plain,
% 59.88/59.94 (~P9(a20,a17,x12611,x12612,a20,a18,x12612,x12611)),
% 59.88/59.94 inference(scs_inference,[],[1087,1089,1097,1232,218,254,216,256,257])).
% 59.88/59.94 cnf(1265,plain,
% 59.88/59.94 (~P11(a20,a17,a18,a20,a18,a17)),
% 59.88/59.94 inference(scs_inference,[],[1087,1089,1097,1232,218,254,216,256,257,255,233])).
% 59.88/59.94 cnf(1267,plain,
% 59.88/59.94 (~P11(a17,a20,a18,a18,a20,a17)),
% 59.88/59.94 inference(scs_inference,[],[1087,1089,1097,1232,218,254,216,256,257,255,233,217])).
% 59.88/59.94 cnf(1269,plain,
% 59.88/59.94 (~P10(x12691,x12692,x12693,x12694)+~P9(a18,a17,a20,a18,x12691,x12692,x12693,x12694)),
% 59.88/59.94 inference(scs_inference,[],[359,1087,1089,1097,1232,218,254,216,256,257,255,233,217,242])).
% 59.88/59.94 cnf(1271,plain,
% 59.88/59.94 (~P3(x12711,x12712,a16,a2)+~P9(a18,a17,a20,a18,x12711,x12712,a16,a1)),
% 59.88/59.94 inference(scs_inference,[],[144,359,1087,1089,1097,1232,218,254,216,256,257,255,233,217,242,182])).
% 59.88/59.94 cnf(1299,plain,
% 59.88/59.94 (~P10(x12991,x12992,x12993,x12994)+~P9(a20,a17,a18,a20,x12991,x12992,x12993,x12994)),
% 59.88/59.94 inference(scs_inference,[],[390,1116,1147,1170,1172,1265,1267,218,216,254,256,257,255,242])).
% 59.88/59.94 cnf(1301,plain,
% 59.88/59.94 (~P3(x13011,x13012,a16,a2)+~P9(a20,a17,a18,a20,x13011,x13012,a16,a1)),
% 59.88/59.94 inference(scs_inference,[],[144,390,1116,1147,1170,1172,1265,1267,218,216,254,256,257,255,242,182])).
% 59.88/59.94 cnf(1318,plain,
% 59.88/59.94 (~P9(a17,a18,a20,a18,x13181,x13182,x13182,x13181)),
% 59.88/59.94 inference(scs_inference,[],[1195,1267,218,254])).
% 59.88/59.94 cnf(1336,plain,
% 59.88/59.94 (~P9(x13361,x13362,x13362,x13361,a17,a20,a18,a20)),
% 59.88/59.94 inference(scs_inference,[],[1132,1224,254,256])).
% 59.88/59.94 cnf(1350,plain,
% 59.88/59.94 (~P9(a17,a20,x13501,x13502,a20,a18,x13502,x13501)),
% 59.88/59.94 inference(scs_inference,[],[1261,254,256])).
% 59.88/59.94 cnf(1356,plain,
% 59.88/59.94 (~P10(x13561,x13562,x13563,x13564)+~P9(a20,a18,a18,a17,x13561,x13562,x13563,x13564)),
% 59.88/59.94 inference(scs_inference,[],[400,1176,1261,1318,254,256,257,255,242])).
% 59.88/59.94 cnf(1358,plain,
% 59.88/59.94 (~P3(x13581,x13582,a16,a2)+~P9(a20,a18,a18,a17,x13581,x13582,a16,a1)),
% 59.88/59.94 inference(scs_inference,[],[144,400,1176,1261,1318,254,256,257,255,242,182])).
% 59.88/59.94 cnf(1417,plain,
% 59.88/59.94 (~P9(x14171,x14172,a18,a20,x14172,x14171,a17,a20)),
% 59.88/59.94 inference(scs_inference,[],[1350,896,254,256])).
% 59.88/59.94 cnf(1421,plain,
% 59.88/59.94 (~P9(a18,a20,x14211,x14212,a17,a20,x14212,x14211)),
% 59.88/59.94 inference(scs_inference,[],[1336,1350,896,254,256,257,255])).
% 59.88/59.94 cnf(1436,plain,
% 59.88/59.94 (~P10(x14361,x14362,x14363,x14364)+~P9(a20,a18,a17,a20,x14361,x14362,x14363,x14364)),
% 59.88/59.94 inference(scs_inference,[],[146,428,619,1421,254,103,229,105,242])).
% 59.88/59.94 cnf(1441,plain,
% 59.88/59.94 (~P10(x14411,x14412,x14413,x14414)+~P9(a18,a20,a20,a17,x14411,x14412,x14413,x14414)),
% 59.88/59.94 inference(scs_inference,[],[442,242])).
% 59.88/59.94 cnf(1443,plain,
% 59.88/59.94 (~P9(a18,a20,a20,a17,x14431,x14432,a16,a1)+~P3(x14431,x14432,a16,a2)),
% 59.88/59.94 inference(scs_inference,[],[442,242,296])).
% 59.88/59.94 cnf(1470,plain,
% 59.88/59.94 (~P10(x14701,x14702,x14703,x14704)+~P9(a17,a20,a20,a18,x14701,x14702,x14703,x14704)),
% 59.88/59.94 inference(scs_inference,[],[146,465,656,104,229,242])).
% 59.88/59.94 cnf(1477,plain,
% 59.88/59.94 (~P10(x14771,x14772,x14773,x14774)+~P9(a17,a20,a18,a20,x14771,x14772,x14773,x14774)),
% 59.88/59.94 inference(scs_inference,[],[553,892,229,242])).
% 59.88/59.94 cnf(1834,plain,
% 59.88/59.94 (~P4(x18341,x18342,a18)+~E(x18341,a20)+~P2(a17,a17,x18342,a18)),
% 59.88/59.94 inference(scs_inference,[],[1126,139])).
% 59.88/59.94 cnf(1924,plain,
% 59.88/59.94 (P1(a1,a18,a15)),
% 59.88/59.94 inference(scs_inference,[],[142,154])).
% 59.88/59.94 cnf(1926,plain,
% 59.88/59.94 (P1(a15,a1,a18)),
% 59.88/59.94 inference(scs_inference,[],[142,154,153])).
% 59.88/59.94 cnf(1930,plain,
% 59.88/59.94 (P3(a16,a1,a16,a2)),
% 59.88/59.94 inference(scs_inference,[],[142,150,144,154,153,189,167])).
% 59.88/59.94 cnf(1932,plain,
% 59.88/59.94 (P3(a16,a2,a1,a16)),
% 59.88/59.94 inference(scs_inference,[],[142,150,144,154,153,189,167,168])).
% 59.88/59.94 cnf(1940,plain,
% 59.88/59.94 (P1(a15,a15,a1)),
% 59.88/59.94 inference(scs_inference,[],[142,150,144,154,153,189,167,168,180,179,191,157])).
% 59.88/59.94 cnf(1946,plain,
% 59.88/59.94 (P10(a16,a1,a16,a1)),
% 59.88/59.94 inference(scs_inference,[],[142,150,144,154,153,189,167,168,180,179,191,157,192,182,296])).
% 59.88/59.94 cnf(1948,plain,
% 59.88/59.94 (P1(a16,a2,a2)),
% 59.88/59.94 inference(scs_inference,[],[142,150,144,154,153,189,167,168,180,179,191,157,192,182,296,162])).
% 59.88/59.94 cnf(1950,plain,
% 59.88/59.94 (P9(a16,a2,x19501,x19502,a16,a2,x19501,x19502)),
% 59.88/59.94 inference(scs_inference,[],[142,150,144,154,153,189,167,168,180,179,191,157,192,182,296,162,227])).
% 59.88/59.94 cnf(1956,plain,
% 59.88/59.94 (P6(a2,a15,a16,a16)),
% 59.88/59.94 inference(scs_inference,[],[142,522,412,150,144,154,153,189,167,168,180,179,191,157,192,182,296,162,227,166,159,238])).
% 59.88/59.94 cnf(1958,plain,
% 59.88/59.94 (P6(a15,a2,a16,a16)),
% 59.88/59.94 inference(scs_inference,[],[142,522,412,150,144,154,153,189,167,168,180,179,191,157,192,182,296,162,227,166,159,238,171])).
% 59.88/59.94 cnf(1960,plain,
% 59.88/59.94 (P6(a2,a16,a15,a16)),
% 59.88/59.94 inference(scs_inference,[],[142,522,412,150,144,154,153,189,167,168,180,179,191,157,192,182,296,162,227,166,159,238,171,172])).
% 59.88/59.94 cnf(1962,plain,
% 59.88/59.94 (P6(a2,a16,a16,a15)),
% 59.88/59.94 inference(scs_inference,[],[142,522,412,150,144,154,153,189,167,168,180,179,191,157,192,182,296,162,227,166,159,238,171,172,173])).
% 59.88/59.94 cnf(1970,plain,
% 59.88/59.94 (P9(a2,a16,a16,a15,a16,a2,a16,a15)),
% 59.88/59.94 inference(scs_inference,[],[142,522,412,150,144,154,153,189,167,168,180,179,191,157,192,182,296,162,227,166,159,238,171,172,173,257,254,165,256])).
% 59.88/59.94 cnf(1972,plain,
% 59.88/59.94 (P9(a16,a15,a16,a2,a16,a15,a16,a2)),
% 59.88/59.94 inference(scs_inference,[],[142,522,412,150,144,154,153,189,167,168,180,179,191,157,192,182,296,162,227,166,159,238,171,172,173,257,254,165,256,255])).
% 59.88/59.94 cnf(1974,plain,
% 59.88/59.94 (P9(a15,a2,a15,a16,a16,a2,a16,a16)),
% 59.88/59.94 inference(scs_inference,[],[142,522,412,150,144,154,153,189,167,168,180,179,191,157,192,182,296,162,227,166,159,238,171,172,173,257,254,165,256,255,226])).
% 59.88/59.94 cnf(1977,plain,
% 59.88/59.94 (P6(a16,a2,a15,a16)),
% 59.88/59.94 inference(scs_inference,[],[1960,171])).
% 59.88/59.94 cnf(1979,plain,
% 59.88/59.94 (P10(a16,a15,a16,a15)),
% 59.88/59.94 inference(scs_inference,[],[1972,1960,171,235])).
% 59.88/59.94 cnf(1985,plain,
% 59.88/59.94 (P6(a16,a2,a16,a15)),
% 59.88/59.94 inference(scs_inference,[],[1972,1926,1960,1970,171,235,154,254,173])).
% 59.88/59.94 cnf(1987,plain,
% 59.88/59.94 (P9(a16,a2,a16,a2,x19871,x19872,x19871,x19872)),
% 59.88/59.94 inference(scs_inference,[],[1972,1950,1926,1960,1970,171,235,154,254,173,257])).
% 59.88/59.94 cnf(1989,plain,
% 59.88/59.94 (P6(a15,a16,a2,a16)),
% 59.88/59.94 inference(scs_inference,[],[1972,1950,1926,1958,1960,1970,171,235,154,254,173,257,172])).
% 59.88/59.94 cnf(1993,plain,
% 59.88/59.94 (P9(a16,a2,a16,a16,a15,a2,a15,a16)),
% 59.88/59.94 inference(scs_inference,[],[1972,1950,1926,1958,1960,1962,1970,171,235,154,254,173,257,172,256,226])).
% 59.88/59.94 cnf(1995,plain,
% 59.88/59.94 (P9(x19951,x19952,a16,a2,x19951,x19952,a16,a2)),
% 59.88/59.94 inference(scs_inference,[],[1972,1950,1926,1958,1960,1962,1970,171,235,154,254,173,257,172,256,226,255])).
% 59.88/59.94 cnf(1997,plain,
% 59.88/59.94 (P1(a18,a1,a15)),
% 59.88/59.94 inference(scs_inference,[],[1924,1972,1950,1926,1958,1960,1962,1970,171,235,154,254,173,257,172,256,226,255,153])).
% 59.88/59.94 cnf(1999,plain,
% 59.88/59.94 (P1(a16,a1,a1)),
% 59.88/59.94 inference(scs_inference,[],[1924,1972,1950,1926,1946,1958,1960,1962,1970,171,235,154,254,173,257,172,256,226,255,153,162])).
% 59.88/59.94 cnf(2001,plain,
% 59.88/59.94 (P9(a16,a1,x20011,x20012,a16,a1,x20011,x20012)),
% 59.88/59.94 inference(scs_inference,[],[1924,1972,1950,1926,1946,1958,1960,1962,1970,171,235,154,254,173,257,172,256,226,255,153,162,227])).
% 59.88/59.94 cnf(2005,plain,
% 59.88/59.94 (P3(a1,a16,a16,a2)),
% 59.88/59.94 inference(scs_inference,[],[1924,1972,1950,1926,1932,1946,1958,1960,1962,1970,151,171,235,154,254,173,257,172,256,226,255,153,162,227,189,167])).
% 59.88/59.94 cnf(2007,plain,
% 59.88/59.94 (P10(a16,a1,a1,a16)),
% 59.88/59.94 inference(scs_inference,[],[1924,1972,1950,1926,1932,1946,1958,1960,1962,1970,151,171,235,154,254,173,257,172,256,226,255,153,162,227,189,167,166])).
% 59.88/59.94 cnf(2009,plain,
% 59.88/59.94 (P3(a16,a1,a2,a16)),
% 59.88/59.94 inference(scs_inference,[],[1924,1972,1950,1926,1930,1932,1946,1958,1960,1962,1970,151,171,235,154,254,173,257,172,256,226,255,153,162,227,189,167,166,168])).
% 59.88/59.94 cnf(2015,plain,
% 59.88/59.94 (~E(a20,a18)),
% 59.88/59.94 inference(scs_inference,[],[1924,1972,1950,1926,1930,1932,1946,1958,1960,1962,1970,536,775,376,151,171,235,154,254,173,257,172,256,226,255,153,162,227,189,167,166,168,123,124,125])).
% 59.88/59.94 cnf(2025,plain,
% 59.88/59.94 (P6(a15,a16,a16,a16)),
% 59.88/59.94 inference(scs_inference,[],[1924,1972,1950,1926,1930,1932,1946,1956,1958,1960,1962,1970,536,775,619,376,151,171,235,154,254,173,257,172,256,226,255,153,162,227,189,167,166,168,123,124,125,126,264,180,179,187])).
% 59.88/59.94 cnf(2036,plain,
% 59.88/59.94 (P9(a16,a2,a16,a20,a29,a16,a29,a20)),
% 59.88/59.94 inference(scs_inference,[],[1924,1972,1950,1926,1930,1932,1946,1956,1958,1960,1962,1970,536,775,619,376,150,151,171,235,154,254,173,257,172,256,226,255,153,162,227,189,167,166,168,123,124,125,126,264,180,179,187,191,192,2,165,175,231])).
% 59.88/59.94 cnf(2039,plain,
% 59.88/59.94 (P6(a16,a15,a2,a16)),
% 59.88/59.94 inference(scs_inference,[],[1989,171])).
% 59.88/59.94 cnf(2044,plain,
% 59.88/59.94 (P6(a16,a16,a2,a15)),
% 59.88/59.94 inference(scs_inference,[],[1974,2015,1985,1989,171,2,257,172])).
% 59.88/59.94 cnf(2046,plain,
% 59.88/59.94 (P9(x20461,x20462,x20461,x20462,a16,a2,a16,a2)),
% 59.88/59.94 inference(scs_inference,[],[1974,1987,2015,1985,1989,171,2,257,172,254])).
% 59.88/59.94 cnf(2048,plain,
% 59.88/59.94 (P10(x20481,x20482,x20481,x20482)),
% 59.88/59.94 inference(scs_inference,[],[1974,1987,1995,2015,1985,1989,171,2,257,172,254,235])).
% 59.88/59.94 cnf(2052,plain,
% 59.88/59.94 (P6(a15,a16,a16,a2)),
% 59.88/59.94 inference(scs_inference,[],[1974,1987,1995,2015,1940,1985,1989,171,2,257,172,254,235,154,173])).
% 59.88/59.94 cnf(2056,plain,
% 59.88/59.94 (P9(a15,a16,a15,a2,a16,a16,a16,a2)),
% 59.88/59.94 inference(scs_inference,[],[1974,1987,1995,2015,1940,1977,1985,1989,171,2,257,172,254,235,154,173,256,226])).
% 59.88/59.94 cnf(2060,plain,
% 59.88/59.94 (P1(a2,a16,a2)),
% 59.88/59.94 inference(scs_inference,[],[1974,1948,1987,1995,2001,2015,1940,1977,1985,1989,171,2,257,172,254,235,154,173,256,226,255,153])).
% 59.88/59.94 cnf(2064,plain,
% 59.88/59.94 (P3(a2,a16,a16,a1)),
% 59.88/59.94 inference(scs_inference,[],[1979,1974,2009,1948,1987,1995,2001,2015,1940,1977,1985,1989,171,2,257,172,254,235,154,173,256,226,255,153,162,167])).
% 59.88/59.94 cnf(2066,plain,
% 59.88/59.94 (P9(a16,a15,x20661,x20662,a16,a15,x20661,x20662)),
% 59.88/59.94 inference(scs_inference,[],[1979,1974,2009,1948,1987,1995,2001,2015,1940,1977,1985,1989,171,2,257,172,254,235,154,173,256,226,255,153,162,167,227])).
% 59.88/59.94 cnf(2072,plain,
% 59.88/59.94 (P3(a1,a16,a2,a16)),
% 59.88/59.94 inference(scs_inference,[],[1979,1974,2009,1948,1987,1995,2001,2015,1940,1977,1985,1989,2005,148,171,2,257,172,254,235,154,173,256,226,255,153,162,167,227,189,166,168])).
% 59.88/59.94 cnf(2074,plain,
% 59.88/59.94 (P1(f12(a1,a2,a16,a16,a2),a16,a2)),
% 59.88/59.94 inference(scs_inference,[],[1979,1974,2009,1948,1987,1995,2001,2015,1940,1977,1985,1989,2005,148,171,2,257,172,254,235,154,173,256,226,255,153,162,167,227,189,166,168,199])).
% 59.88/59.94 cnf(2078,plain,
% 59.88/59.94 (P6(a2,a2,a16,a2)),
% 59.88/59.94 inference(scs_inference,[],[1979,1974,2009,1948,1987,1995,2001,2015,1940,1977,1985,1989,2005,148,171,2,257,172,254,235,154,173,256,226,255,153,162,167,227,189,166,168,199,200,238])).
% 59.88/59.94 cnf(2079,plain,
% 59.88/59.94 (P9(a16,a2,a16,a2,x20791,x20792,x20791,x20792)),
% 59.88/59.94 inference(rename_variables,[],[1987])).
% 59.88/59.94 cnf(2087,plain,
% 59.88/59.94 (P5(a2,a2,a2,a2)),
% 59.88/59.94 inference(scs_inference,[],[1979,1974,2009,1948,1987,2079,1995,2001,2015,1940,1977,1985,1989,2005,148,171,2,257,172,254,235,154,173,256,226,255,153,162,167,227,189,166,168,199,200,238,230,208,209,253])).
% 59.88/59.94 cnf(2088,plain,
% 59.88/59.94 (P9(a16,a2,a16,a2,x20881,x20882,x20881,x20882)),
% 59.88/59.94 inference(rename_variables,[],[1987])).
% 59.88/59.94 cnf(2090,plain,
% 59.88/59.94 (P9(a2,a2,a2,a2,a2,a2,a2,a2)),
% 59.88/59.94 inference(scs_inference,[],[1979,1974,2009,1948,1987,2079,1995,2001,2015,1940,1977,1985,1989,2005,148,171,2,257,172,254,235,154,173,256,226,255,153,162,167,227,189,166,168,199,200,238,230,208,209,253,228])).
% 59.88/59.94 cnf(2092,plain,
% 59.88/59.94 (P8(a2,a2,a16,a2,a2,a2,a16,a2)),
% 59.88/59.94 inference(scs_inference,[],[1979,1974,2009,1948,1987,2079,1995,2001,2015,1940,1977,1985,1989,2005,148,171,2,257,172,254,235,154,173,256,226,255,153,162,167,227,189,166,168,199,200,238,230,208,209,253,228,259])).
% 59.88/59.94 cnf(2094,plain,
% 59.88/59.94 (P8(a2,a16,a2,a2,a16,a2,a2,a2)),
% 59.88/59.94 inference(scs_inference,[],[1979,1974,2009,1948,1987,2079,1995,2001,2015,1940,1977,1985,1989,2005,148,171,2,257,172,254,235,154,173,256,226,255,153,162,167,227,189,166,168,199,200,238,230,208,209,253,228,259,260])).
% 59.88/59.94 cnf(2096,plain,
% 59.88/59.94 (P8(a16,a2,a16,a2,a2,a2,a2,a2)),
% 59.88/59.94 inference(scs_inference,[],[1979,1974,2009,1948,1987,2079,1995,2001,2015,1940,1977,1985,1989,2005,148,171,2,257,172,254,235,154,173,256,226,255,153,162,167,227,189,166,168,199,200,238,230,208,209,253,228,259,260,261])).
% 59.88/59.94 cnf(2136,plain,
% 59.88/59.94 (P10(f12(a1,a2,a16,a16,a2),a1,a16,a1)),
% 59.88/59.94 inference(scs_inference,[],[1979,1974,2009,1948,1987,2079,1995,2001,2015,1940,1977,1985,1989,2005,148,171,2,257,172,254,235,154,173,256,226,255,153,162,167,227,189,166,168,199,200,238,230,208,209,253,228,259,260,261,1443,508,574,605,629,666,708,792,954,977,1010,1072,1155,1180,1205,1238,1271,1301,1358,296])).
% 59.88/59.94 cnf(2140,plain,
% 59.88/59.94 (P2(a2,a2,a2,a2)),
% 59.88/59.94 inference(scs_inference,[],[1979,1974,2009,1948,1987,2079,1995,2001,2015,1940,1977,1985,1989,2005,148,171,2,257,172,254,235,154,173,256,226,255,153,162,167,227,189,166,168,199,200,238,230,208,209,253,228,259,260,261,1443,508,574,605,629,666,708,792,954,977,1010,1072,1155,1180,1205,1238,1271,1301,1358,296,165,186])).
% 59.88/59.94 cnf(2146,plain,
% 59.88/59.94 (P5(a16,a2,a16,f35(a1,a16,a2,a2,a2))),
% 59.88/59.94 inference(scs_inference,[],[1979,1974,2009,1948,1987,2079,1995,2001,2015,1940,1977,1985,1989,2005,148,171,2,257,172,254,235,154,173,256,226,255,153,162,167,227,189,166,168,199,200,238,230,208,209,253,228,259,260,261,1443,508,574,605,629,666,708,792,954,977,1010,1072,1155,1180,1205,1238,1271,1301,1358,296,165,186,178,201,202])).
% 59.88/59.94 cnf(2148,plain,
% 59.88/59.94 (P10(f35(a1,a16,a2,a2,a2),a2,a1,a16)),
% 59.88/59.94 inference(scs_inference,[],[1979,1974,2009,1948,1987,2079,1995,2001,2015,1940,1977,1985,1989,2005,148,171,2,257,172,254,235,154,173,256,226,255,153,162,167,227,189,166,168,199,200,238,230,208,209,253,228,259,260,261,1443,508,574,605,629,666,708,792,954,977,1010,1072,1155,1180,1205,1238,1271,1301,1358,296,165,186,178,201,202,203])).
% 59.88/59.94 cnf(2154,plain,
% 59.88/59.94 (P5(a16,a2,a16,a2)),
% 59.88/59.94 inference(scs_inference,[],[1979,1974,2009,1948,1987,2079,1995,2001,2015,1940,1977,1985,1989,2005,148,171,2,257,172,254,235,154,173,256,226,255,153,162,167,227,189,166,168,199,200,238,230,208,209,253,228,259,260,261,1443,508,574,605,629,666,708,792,954,977,1010,1072,1155,1180,1205,1238,1271,1301,1358,296,165,186,178,201,202,203,247,251,245])).
% 59.88/59.94 cnf(2156,plain,
% 59.88/59.94 (P3(a2,a2,a2,a2)),
% 59.88/59.94 inference(scs_inference,[],[1979,1974,2009,1948,1987,2079,1995,2001,2015,1940,1977,1985,1989,2005,148,171,2,257,172,254,235,154,173,256,226,255,153,162,167,227,189,166,168,199,200,238,230,208,209,253,228,259,260,261,1443,508,574,605,629,666,708,792,954,977,1010,1072,1155,1180,1205,1238,1271,1301,1358,296,165,186,178,201,202,203,247,251,245,183])).
% 59.88/59.94 cnf(2160,plain,
% 59.88/59.94 (P3(a16,a2,a16,a2)),
% 59.88/59.94 inference(scs_inference,[],[1979,1974,2009,1948,1987,2079,2088,1995,2001,2015,1940,1977,1985,1989,2005,148,171,2,257,172,254,235,154,173,256,226,255,153,162,167,227,189,166,168,199,200,238,230,208,209,253,228,259,260,261,1443,508,574,605,629,666,708,792,954,977,1010,1072,1155,1180,1205,1238,1271,1301,1358,296,165,186,178,201,202,203,247,251,245,183,192,243])).
% 59.88/59.94 cnf(2225,plain,
% 59.88/59.94 (P9(a16,a2,a2,a2,a2,a2,a16,a2)),
% 59.88/59.94 inference(scs_inference,[],[2154,2148,1070,1153,228])).
% 59.88/59.94 cnf(2237,plain,
% 59.88/59.94 (~P9(a20,a18,a17,a18,a16,a2,a16,a1)),
% 59.88/59.94 inference(scs_inference,[],[2094,2154,2160,2148,1070,1153,228,975,629,1010,259,664,1072])).
% 59.88/59.94 cnf(2243,plain,
% 59.88/59.94 (P5(a16,f35(a1,a16,a2,a2,a2),a16,a2)),
% 59.88/59.94 inference(scs_inference,[],[2094,2154,2160,2148,2146,1070,1153,228,975,629,1010,259,664,1072,1358,572,169])).
% 59.88/59.94 cnf(2251,plain,
% 59.88/59.94 (P6(a16,a15,a16,a16)),
% 59.88/59.94 inference(scs_inference,[],[2025,2094,2154,2160,2148,2146,1070,1153,228,975,629,1010,259,664,1072,1358,572,169,1203,1271,666,171])).
% 59.88/59.94 cnf(2259,plain,
% 59.88/59.94 (P5(a16,a2,a2,a16)),
% 59.88/59.94 inference(scs_inference,[],[2025,2094,2154,2160,2148,2146,1070,1153,228,975,629,1010,259,664,1072,1358,572,169,1203,1271,666,171,508,1301,1180,170])).
% 59.88/59.94 cnf(2273,plain,
% 59.88/59.94 (P8(a2,a16,a16,a2,a2,a2,a2,a2)),
% 59.88/59.94 inference(scs_inference,[],[2025,2094,2096,2154,2160,2136,2148,2146,1070,1153,228,975,629,1010,259,664,1072,1358,572,169,1203,1271,666,171,508,1301,1180,170,792,1470,415,832,954,1238,260])).
% 59.88/59.94 cnf(2293,plain,
% 59.88/59.94 (P8(a16,a2,a2,a2,a2,a16,a2,a2)),
% 59.88/59.94 inference(scs_inference,[],[2025,2094,2096,2154,2160,2136,2148,2146,1070,1153,228,975,629,1010,259,664,1072,1358,572,169,1203,1271,666,171,508,1301,1180,170,792,1470,415,832,954,1238,260,708,790,1356,627,1008,951,1269,1436,605,258])).
% 59.88/59.94 cnf(2323,plain,
% 59.88/59.94 (P10(a16,a2,a16,a1)),
% 59.88/59.94 inference(scs_inference,[],[2025,2092,2094,2096,2154,2160,2136,2148,2146,1070,1153,228,975,629,1010,259,664,1072,1358,572,169,1203,1271,666,171,508,1301,1180,170,792,1470,415,832,954,1238,260,708,790,1356,627,1008,951,1269,1436,605,258,1443,1236,261,603,1477,574,506,1441,1299,706,1155,1178,1205,977,296])).
% 59.88/59.94 cnf(2327,plain,
% 59.88/59.94 (P6(a2,a16,a2,a2)),
% 59.88/59.94 inference(scs_inference,[],[1997,2025,2078,2092,2094,2096,2154,2160,2136,2148,2146,1070,1153,228,975,629,1010,259,664,1072,1358,572,169,1203,1271,666,171,508,1301,1180,170,792,1470,415,832,954,1238,260,708,790,1356,627,1008,951,1269,1436,605,258,1443,1236,261,603,1477,574,506,1441,1299,706,1155,1178,1205,977,296,154,172])).
% 59.88/59.94 cnf(2331,plain,
% 59.88/59.94 (P10(a16,a1,f12(a1,a2,a16,a16,a2),a1)),
% 59.88/59.94 inference(scs_inference,[],[1993,1997,2025,2078,2092,2094,2096,2154,2160,2136,2148,2146,1070,1153,228,975,629,1010,259,664,1072,1358,572,169,1203,1271,666,171,508,1301,1180,170,792,1470,415,832,954,1238,260,708,790,1356,627,1008,951,1269,1436,605,258,1443,1236,261,603,1477,574,506,1441,1299,706,1155,1178,1205,977,296,154,172,257,165])).
% 59.88/59.94 cnf(2333,plain,
% 59.88/59.94 (P9(a16,a16,a16,a2,a15,a16,a15,a2)),
% 59.88/59.94 inference(scs_inference,[],[1993,2056,1997,2025,2078,2092,2094,2096,2154,2160,2136,2148,2146,1070,1153,228,975,629,1010,259,664,1072,1358,572,169,1203,1271,666,171,508,1301,1180,170,792,1470,415,832,954,1238,260,708,790,1356,627,1008,951,1269,1436,605,258,1443,1236,261,603,1477,574,506,1441,1299,706,1155,1178,1205,977,296,154,172,257,165,254])).
% 59.88/59.94 cnf(2335,plain,
% 59.88/59.94 (P6(a16,a15,a16,a2)),
% 59.88/59.94 inference(scs_inference,[],[1993,2056,2039,1997,2025,2078,2092,2094,2096,2154,2160,2136,2148,2146,1070,1153,228,975,629,1010,259,664,1072,1358,572,169,1203,1271,666,171,508,1301,1180,170,792,1470,415,832,954,1238,260,708,790,1356,627,1008,951,1269,1436,605,258,1443,1236,261,603,1477,574,506,1441,1299,706,1155,1178,1205,977,296,154,172,257,165,254,173])).
% 59.88/59.94 cnf(2341,plain,
% 59.88/59.94 (P1(a1,a16,a1)),
% 59.88/59.94 inference(scs_inference,[],[1993,2056,2039,1997,1999,2025,2078,2092,2094,2096,2154,2160,2136,2148,2146,1070,1153,228,975,629,1010,259,664,1072,1358,572,169,1203,1271,666,171,508,1301,1180,170,792,1470,415,832,954,1238,260,708,790,1356,627,1008,951,1269,1436,605,258,1443,1236,261,603,1477,574,506,1441,1299,706,1155,1178,1205,977,296,154,172,257,165,254,173,256,226,153])).
% 59.88/59.94 cnf(2345,plain,
% 59.88/59.94 (P1(x23451,x23452,x23452)),
% 59.88/59.94 inference(scs_inference,[],[2048,1993,2056,2039,2066,1997,1999,2025,2078,2092,2094,2096,2154,2160,2136,2148,2146,1070,1153,228,975,629,1010,259,664,1072,1358,572,169,1203,1271,666,171,508,1301,1180,170,792,1470,415,832,954,1238,260,708,790,1356,627,1008,951,1269,1436,605,258,1443,1236,261,603,1477,574,506,1441,1299,706,1155,1178,1205,977,296,154,172,257,165,254,173,256,226,153,255,162])).
% 59.88/59.94 cnf(2347,plain,
% 59.88/59.94 (P9(x23471,x23472,x23473,x23474,x23471,x23472,x23473,x23474)),
% 59.88/59.94 inference(scs_inference,[],[2048,1993,2056,2039,2066,1997,1999,2025,2078,2092,2094,2096,2154,2160,2136,2148,2146,1070,1153,228,975,629,1010,259,664,1072,1358,572,169,1203,1271,666,171,508,1301,1180,170,792,1470,415,832,954,1238,260,708,790,1356,627,1008,951,1269,1436,605,258,1443,1236,261,603,1477,574,506,1441,1299,706,1155,1178,1205,977,296,154,172,257,165,254,173,256,226,153,255,162,227])).
% 59.88/59.94 cnf(2349,plain,
% 59.88/59.94 (P3(a2,a16,a1,a16)),
% 59.88/59.94 inference(scs_inference,[],[2048,1993,2056,2039,2072,2066,1997,1999,2025,2078,2092,2094,2096,2154,2160,2136,2148,2146,1070,1153,228,975,629,1010,259,664,1072,1358,572,169,1203,1271,666,171,508,1301,1180,170,792,1470,415,832,954,1238,260,708,790,1356,627,1008,951,1269,1436,605,258,1443,1236,261,603,1477,574,506,1441,1299,706,1155,1178,1205,977,296,154,172,257,165,254,173,256,226,153,255,162,227,167])).
% 59.88/59.94 cnf(2353,plain,
% 59.88/59.94 (P10(x23531,x23532,x23532,x23531)),
% 59.88/59.94 inference(scs_inference,[],[2048,1993,2056,2039,2072,2066,1997,1999,2025,2078,2092,2094,2096,2140,2154,2160,2136,2148,2146,1070,1153,228,975,629,1010,259,664,1072,1358,572,169,1203,1271,666,171,508,1301,1180,170,792,1470,415,832,954,1238,260,708,790,1356,627,1008,951,1269,1436,605,258,1443,1236,261,603,1477,574,506,1441,1299,706,1155,1178,1205,977,296,154,172,257,165,254,173,256,226,153,255,162,227,167,189,166])).
% 59.88/59.94 cnf(2355,plain,
% 59.88/59.94 (P3(a16,a2,a2,a16)),
% 59.88/59.94 inference(scs_inference,[],[2048,1993,2056,2039,2072,2066,1997,1999,2025,2078,2092,2094,2096,2140,2154,2160,2136,2148,2146,1070,1153,228,975,629,1010,259,664,1072,1358,572,169,1203,1271,666,171,508,1301,1180,170,792,1470,415,832,954,1238,260,708,790,1356,627,1008,951,1269,1436,605,258,1443,1236,261,603,1477,574,506,1441,1299,706,1155,1178,1205,977,296,154,172,257,165,254,173,256,226,153,255,162,227,167,189,166,168])).
% 59.88/59.94 cnf(2357,plain,
% 59.88/59.94 (P5(a2,a2,a2,f3(a2,a2,a2))),
% 59.88/59.94 inference(scs_inference,[],[2048,1993,2056,2039,2072,2066,1997,1999,2025,2078,2087,2092,2094,2096,2140,2154,2156,2160,2136,2148,2146,1070,1153,228,975,629,1010,259,664,1072,1358,572,169,1203,1271,666,171,508,1301,1180,170,792,1470,415,832,954,1238,260,708,790,1356,627,1008,951,1269,1436,605,258,1443,1236,261,603,1477,574,506,1441,1299,706,1155,1178,1205,977,296,154,172,257,165,254,173,256,226,153,255,162,227,167,189,166,168,190])).
% 59.88/59.94 cnf(2359,plain,
% 59.88/59.94 (P2(f8(a16,a16,a2),a16,a16,a2)),
% 59.88/59.94 inference(scs_inference,[],[2048,1993,2056,2039,2072,2066,1997,1999,2025,2044,2078,2087,2092,2094,2096,2140,2154,2156,2160,2136,2148,2146,1070,1153,228,975,629,1010,259,664,1072,1358,572,169,1203,1271,666,171,508,1301,1180,170,792,1470,415,832,954,1238,260,708,790,1356,627,1008,951,1269,1436,605,258,1443,1236,261,603,1477,574,506,1441,1299,706,1155,1178,1205,977,296,154,172,257,165,254,173,256,226,153,255,162,227,167,189,166,168,190,193])).
% 59.88/59.94 cnf(2363,plain,
% 59.88/59.94 (P6(a17,a20,a17,f34(a18,a20,a17,a17))),
% 59.88/59.94 inference(scs_inference,[],[2048,1993,2056,2039,2072,2066,1997,1999,2025,2044,2078,2087,2092,2094,2096,2140,2154,2156,2160,2136,2148,2146,315,1070,1153,228,975,629,1010,259,664,1072,1358,572,169,1203,1271,666,171,508,1301,1180,170,792,1470,415,832,954,1238,260,708,790,1356,627,1008,951,1269,1436,605,258,1443,1236,261,603,1477,574,506,1441,1299,706,1155,1178,1205,977,296,154,172,257,165,254,173,256,226,153,255,162,227,167,189,166,168,190,193,195,246])).
% 59.88/59.94 cnf(2369,plain,
% 59.88/59.94 (P9(a18,a17,a20,a17,a18,f34(a18,a20,a17,a17),a20,f34(a18,a20,a17,a17))),
% 59.88/59.94 inference(scs_inference,[],[2048,1993,2056,2039,2072,2066,1997,1999,2025,2044,2078,2087,2090,2092,2094,2096,2140,2154,2156,2160,2136,2148,2146,315,1070,1153,228,975,629,1010,259,664,1072,1358,572,169,1203,1271,666,171,508,1301,1180,170,792,1470,415,832,954,1238,260,708,790,1356,627,1008,951,1269,1436,605,258,1443,1236,261,603,1477,574,506,1441,1299,706,1155,1178,1205,977,296,154,172,257,165,254,173,256,226,153,255,162,227,167,189,166,168,190,193,195,246,248,265,262])).
% 59.88/59.94 cnf(2371,plain,
% 59.88/59.94 (P3(f35(a1,a16,a2,a2,a2),a2,a2,a16)),
% 59.88/59.94 inference(scs_inference,[],[2048,1993,2056,2039,2072,2066,1997,1999,2025,2044,2078,2087,2090,2092,2094,2096,2140,2154,2156,2160,2136,2148,2146,315,1070,1153,228,975,629,1010,259,664,1072,1358,572,169,1203,1271,666,171,508,1301,1180,170,792,1470,415,832,954,1238,260,708,790,1356,627,1008,951,1269,1436,605,258,1443,1236,261,603,1477,574,506,1441,1299,706,1155,1178,1205,977,296,154,172,257,165,254,173,256,226,153,255,162,227,167,189,166,168,190,193,195,246,248,265,262,184])).
% 59.88/59.94 cnf(2373,plain,
% 59.88/59.94 (P4(a16,a2,a2)),
% 59.88/59.94 inference(scs_inference,[],[2048,1993,2056,2039,2072,2066,1997,1999,2025,2044,2078,2087,2090,2092,2094,2096,2140,2154,2156,2160,2136,2148,2146,315,1948,1070,1153,228,975,629,1010,259,664,1072,1358,572,169,1203,1271,666,171,508,1301,1180,170,792,1470,415,832,954,1238,260,708,790,1356,627,1008,951,1269,1436,605,258,1443,1236,261,603,1477,574,506,1441,1299,706,1155,1178,1205,977,296,154,172,257,165,254,173,256,226,153,255,162,227,167,189,166,168,190,193,195,246,248,265,262,184,163])).
% 59.88/59.94 cnf(2375,plain,
% 59.88/59.94 (P10(f35(a2,a2,a2,a2,a2),a2,a2,a2)),
% 59.88/59.94 inference(scs_inference,[],[2048,1993,2056,2039,2072,2066,1997,1999,2025,2044,2078,2087,2090,2092,2094,2096,2140,2154,2156,2160,2136,2148,2146,315,1948,1070,1153,228,975,629,1010,259,664,1072,1358,572,169,1203,1271,666,171,508,1301,1180,170,792,1470,415,832,954,1238,260,708,790,1356,627,1008,951,1269,1436,605,258,1443,1236,261,603,1477,574,506,1441,1299,706,1155,1178,1205,977,296,154,172,257,165,254,173,256,226,153,255,162,227,167,189,166,168,190,193,195,246,248,265,262,184,163,203])).
% 59.88/59.94 cnf(2381,plain,
% 59.88/59.94 (P1(f5(a2,a1,a16),a16,a2)),
% 59.88/59.94 inference(scs_inference,[],[2048,1993,2056,2039,2072,2066,1997,1999,2025,2044,2078,2087,2090,2092,2094,2096,2140,2154,2156,2160,2136,2148,2146,2007,430,315,1948,1070,1153,228,975,629,1010,259,664,1072,1358,572,169,1203,1271,666,171,508,1301,1180,170,792,1470,415,832,954,1238,260,708,790,1356,627,1008,951,1269,1436,605,258,1443,1236,261,603,1477,574,506,1441,1299,706,1155,1178,1205,977,296,154,172,257,165,254,173,256,226,153,255,162,227,167,189,166,168,190,193,195,246,248,265,262,184,163,203,242,181,180])).
% 59.88/59.94 cnf(2383,plain,
% 59.88/59.94 (P5(a2,a2,a2,f35(a2,a2,a2,a2,a2))),
% 59.88/59.94 inference(scs_inference,[],[2048,1993,2056,2039,2072,2066,1997,1999,2025,2044,2078,2087,2090,2092,2094,2096,2140,2154,2156,2160,2136,2148,2146,2007,430,315,1948,1070,1153,228,975,629,1010,259,664,1072,1358,572,169,1203,1271,666,171,508,1301,1180,170,792,1470,415,832,954,1238,260,708,790,1356,627,1008,951,1269,1436,605,258,1443,1236,261,603,1477,574,506,1441,1299,706,1155,1178,1205,977,296,154,172,257,165,254,173,256,226,153,255,162,227,167,189,166,168,190,193,195,246,248,265,262,184,163,203,242,181,180,201])).
% 59.88/59.94 cnf(2387,plain,
% 59.88/59.94 (P9(a2,a2,a2,a2,a2,a2,a2,a16)),
% 59.88/59.94 inference(scs_inference,[],[2048,1993,2056,2039,2072,2066,1997,1999,2025,2044,2078,2087,2090,2092,2094,2096,2140,2154,2156,2160,2136,2148,2146,2007,430,315,1948,1070,1153,228,975,629,1010,259,664,1072,1358,572,169,1203,1271,666,171,508,1301,1180,170,792,1470,415,832,954,1238,260,708,790,1356,627,1008,951,1269,1436,605,258,1443,1236,261,603,1477,574,506,1441,1299,706,1155,1178,1205,977,296,154,172,257,165,254,173,256,226,153,255,162,227,167,189,166,168,190,193,195,246,248,265,262,184,163,203,242,181,180,201,179,229])).
% 59.88/59.94 cnf(2389,plain,
% 59.88/59.94 (P2(a16,a2,a2,a2)),
% 59.88/59.94 inference(scs_inference,[],[2048,1993,2056,2039,2072,2066,1997,1999,2025,2044,2078,2087,2090,2092,2094,2096,2140,2154,2156,2160,2136,2148,2146,2007,430,315,1948,1070,1153,228,975,629,1010,259,664,1072,1358,572,169,1203,1271,666,171,508,1301,1180,170,792,1470,415,832,954,1238,260,708,790,1356,627,1008,951,1269,1436,605,258,1443,1236,261,603,1477,574,506,1441,1299,706,1155,1178,1205,977,296,154,172,257,165,254,173,256,226,153,255,162,227,167,189,166,168,190,193,195,246,248,265,262,184,163,203,242,181,180,201,179,229,186])).
% 59.88/59.94 cnf(2403,plain,
% 59.88/59.94 (P6(a2,a2,a2,a16)),
% 59.88/59.94 inference(scs_inference,[],[142,2048,1993,2056,2039,2072,2046,2066,1997,1999,2025,2044,2060,2064,2078,2087,2090,2092,2094,2096,2140,2154,2156,2160,2136,2148,2146,2007,430,315,1948,1070,1153,228,975,629,1010,259,664,1072,1358,572,169,1203,1271,666,171,508,1301,1180,170,792,1470,415,832,954,1238,260,708,790,1356,627,1008,951,1269,1436,605,258,1443,1236,261,603,1477,574,506,1441,1299,706,1155,1178,1205,977,296,154,172,257,165,254,173,256,226,153,255,162,227,167,189,166,168,190,193,195,246,248,265,262,184,163,203,242,181,180,201,179,229,186,202,178,191,199,200,183,238])).
% 59.88/59.94 cnf(2404,plain,
% 59.88/59.94 (P9(x24041,x24042,x24041,x24042,a16,a2,a16,a2)),
% 59.88/59.94 inference(rename_variables,[],[2046])).
% 59.88/59.94 cnf(2408,plain,
% 59.88/59.94 (P3(x24081,x24082,x24081,x24082)),
% 59.88/59.94 inference(scs_inference,[],[142,2048,1993,2056,2039,2072,2046,2404,2066,1997,1999,2025,2044,2060,2064,2078,2087,2090,2092,2094,2096,2140,2154,2156,2160,2136,2148,2146,2007,430,315,1948,1070,1153,228,975,629,1010,259,664,1072,1358,572,169,1203,1271,666,171,508,1301,1180,170,792,1470,415,832,954,1238,260,708,790,1356,627,1008,951,1269,1436,605,258,1443,1236,261,603,1477,574,506,1441,1299,706,1155,1178,1205,977,296,154,172,257,165,254,173,256,226,153,255,162,227,167,189,166,168,190,193,195,246,248,265,262,184,163,203,242,181,180,201,179,229,186,202,178,191,199,200,183,238,192,243])).
% 59.88/59.94 cnf(2410,plain,
% 59.88/59.94 (P6(a2,a2,a2,a2)),
% 59.88/59.94 inference(scs_inference,[],[142,2048,1993,2056,2039,2072,2046,2404,2066,1997,1999,2025,2044,2060,2064,2078,2087,2090,2092,2094,2096,2140,2154,2156,2160,2136,2148,2146,2007,430,315,1948,1070,1153,228,975,629,1010,259,664,1072,1358,572,169,1203,1271,666,171,508,1301,1180,170,792,1470,415,832,954,1238,260,708,790,1356,627,1008,951,1269,1436,605,258,1443,1236,261,603,1477,574,506,1441,1299,706,1155,1178,1205,977,296,154,172,257,165,254,173,256,226,153,255,162,227,167,189,166,168,190,193,195,246,248,265,262,184,163,203,242,181,180,201,179,229,186,202,178,191,199,200,183,238,192,243,198])).
% 59.88/59.94 cnf(2414,plain,
% 59.88/59.94 (P5(a2,a2,a2,a16)),
% 59.88/59.94 inference(scs_inference,[],[142,2048,1993,2056,2039,2072,2046,2404,2066,1997,1999,2025,2044,2060,2064,2078,2087,2090,2092,2094,2096,2140,2154,2156,2160,2136,2148,2146,2007,430,315,1948,1070,1153,228,975,629,1010,259,664,1072,1358,572,169,1203,1271,666,171,508,1301,1180,170,792,1470,415,832,954,1238,260,708,790,1356,627,1008,951,1269,1436,605,258,1443,1236,261,603,1477,574,506,1441,1299,706,1155,1178,1205,977,296,154,172,257,165,254,173,256,226,153,255,162,227,167,189,166,168,190,193,195,246,248,265,262,184,163,203,242,181,180,201,179,229,186,202,178,191,199,200,183,238,192,243,198,188,253])).
% 59.88/59.94 cnf(2416,plain,
% 59.88/59.94 (P5(f6(a2,a2,a2),a2,f6(a2,a2,a2),a2)),
% 59.88/59.94 inference(scs_inference,[],[142,2048,1993,2056,2039,2072,2046,2404,2066,1997,1999,2025,2044,2060,2064,2078,2087,2090,2092,2094,2096,2140,2154,2156,2160,2136,2148,2146,2007,430,315,1948,1070,1153,228,975,629,1010,259,664,1072,1358,572,169,1203,1271,666,171,508,1301,1180,170,792,1470,415,832,954,1238,260,708,790,1356,627,1008,951,1269,1436,605,258,1443,1236,261,603,1477,574,506,1441,1299,706,1155,1178,1205,977,296,154,172,257,165,254,173,256,226,153,255,162,227,167,189,166,168,190,193,195,246,248,265,262,184,163,203,242,181,180,201,179,229,186,202,178,191,199,200,183,238,192,243,198,188,253,158])).
% 59.88/59.94 cnf(2418,plain,
% 59.88/59.94 (P10(a2,a16,a16,a1)),
% 59.88/59.94 inference(scs_inference,[],[142,2048,1993,2056,2039,2072,2046,2404,2066,1997,1999,2025,2044,2060,2064,2078,2087,2090,2092,2094,2096,2140,2154,2156,2160,2136,2148,2146,2007,430,315,1948,1070,1153,228,975,629,1010,259,664,1072,1358,572,169,1203,1271,666,171,508,1301,1180,170,792,1470,415,832,954,1238,260,708,790,1356,627,1008,951,1269,1436,605,258,1443,1236,261,603,1477,574,506,1441,1299,706,1155,1178,1205,977,296,154,172,257,165,254,173,256,226,153,255,162,227,167,189,166,168,190,193,195,246,248,265,262,184,163,203,242,181,180,201,179,229,186,202,178,191,199,200,183,238,192,243,198,188,253,158,302])).
% 59.88/59.94 cnf(2419,plain,
% 59.88/59.94 (P10(a16,a16,a2,a2)),
% 59.88/59.94 inference(scs_inference,[],[142,2048,1993,2056,2039,2072,2046,2404,2066,1997,1999,2025,2044,2060,2064,2078,2087,2090,2092,2094,2096,2140,2154,2156,2160,2136,2148,2146,2007,430,315,1948,1070,1153,228,975,629,1010,259,664,1072,1358,572,169,1203,1271,666,171,508,1301,1180,170,792,1470,415,832,954,1238,260,708,790,1356,627,1008,951,1269,1436,605,258,1443,1236,261,603,1477,574,506,1441,1299,706,1155,1178,1205,977,296,154,172,257,165,254,173,256,226,153,255,162,227,167,189,166,168,190,193,195,246,248,265,262,184,163,203,242,181,180,201,179,229,186,202,178,191,199,200,183,238,192,243,198,188,253,158,302,160])).
% 59.88/59.94 cnf(2421,plain,
% 59.88/59.94 (P8(f6(a2,a2,a2),a2,a2,a2,f6(a2,a2,a2),a2,a2,a2)),
% 59.88/59.94 inference(scs_inference,[],[142,2048,1993,2056,2039,2072,2046,2404,2066,1997,1999,2025,2044,2060,2064,2078,2087,2090,2092,2094,2096,2140,2154,2156,2160,2136,2148,2146,2007,430,315,1948,1070,1153,228,975,629,1010,259,664,1072,1358,572,169,1203,1271,666,171,508,1301,1180,170,792,1470,415,832,954,1238,260,708,790,1356,627,1008,951,1269,1436,605,258,1443,1236,261,603,1477,574,506,1441,1299,706,1155,1178,1205,977,296,154,172,257,165,254,173,256,226,153,255,162,227,167,189,166,168,190,193,195,246,248,265,262,184,163,203,242,181,180,201,179,229,186,202,178,191,199,200,183,238,192,243,198,188,253,158,302,160,225])).
% 59.88/59.94 cnf(2425,plain,
% 59.88/59.94 (P4(f33(a2,a2,a2,a2,a16,a16),a2,a2)),
% 59.88/59.94 inference(scs_inference,[],[142,2048,1993,2056,2039,2072,2046,2404,2066,1997,1999,2025,2044,2060,2064,2078,2087,2090,2092,2094,2096,2140,2154,2156,2160,2136,2148,2146,2007,430,315,1948,1070,1153,228,975,629,1010,259,664,1072,1358,572,169,1203,1271,666,171,508,1301,1180,170,792,1470,415,832,954,1238,260,708,790,1356,627,1008,951,1269,1436,605,258,1443,1236,261,603,1477,574,506,1441,1299,706,1155,1178,1205,977,296,154,172,257,165,254,173,256,226,153,255,162,227,167,189,166,168,190,193,195,246,248,265,262,184,163,203,242,181,180,201,179,229,186,202,178,191,199,200,183,238,192,243,198,188,253,158,302,160,225,196,205])).
% 59.88/59.94 cnf(2447,plain,
% 59.88/59.94 (P8(a2,a2,a16,a2,a2,a2,a2,a16)),
% 59.88/59.94 inference(scs_inference,[],[2418,2293,1070,259])).
% 59.88/59.94 cnf(2457,plain,
% 59.88/59.94 (P8(a2,a16,a2,a2,a2,a16,a2,a2)),
% 59.88/59.94 inference(scs_inference,[],[2418,2293,2259,2425,1070,259,158,169,415,975,260])).
% 59.88/59.94 cnf(2467,plain,
% 59.88/59.94 (P8(a16,a2,a2,a16,a2,a2,a2,a2)),
% 59.88/59.94 inference(scs_inference,[],[2418,2293,2259,2327,2419,2425,1070,259,158,169,415,975,260,664,832,1269,171,261])).
% 59.88/59.94 cnf(2477,plain,
% 59.88/59.94 (P9(a2,a2,a2,a16,a2,a16,a2,a16)),
% 59.88/59.94 inference(scs_inference,[],[2418,2293,2259,2327,2414,2419,2425,1070,259,158,169,415,975,260,664,832,1269,171,261,603,1470,1436,627,228])).
% 59.88/59.94 cnf(2487,plain,
% 59.88/59.94 (P5(a2,a2,a16,a2)),
% 59.88/59.94 inference(scs_inference,[],[2418,2293,2259,2327,2414,2419,2425,1070,259,158,169,415,975,260,664,832,1269,171,261,603,1470,1436,627,228,1153,1203,1299,572,170])).
% 59.88/59.94 cnf(2509,plain,
% 59.88/59.94 (P10(a2,a2,a2,a16)),
% 59.88/59.94 inference(scs_inference,[],[2418,2293,2259,2273,2327,2414,2419,2425,1070,259,158,169,415,975,260,664,832,1269,171,261,603,1470,1436,627,228,1153,1203,1299,572,170,258,706,1441,790,1178,1356,951,1008,1477,1236,235])).
% 59.88/59.94 cnf(2513,plain,
% 59.88/59.94 (P9(x25131,x25132,x25131,x25132,x25133,x25134,x25133,x25134)),
% 59.88/59.94 inference(scs_inference,[],[2347,2418,2293,2259,2273,2327,2414,2419,2425,1070,259,158,169,415,975,260,664,832,1269,171,261,603,1470,1436,627,228,1153,1203,1299,572,170,258,706,1441,790,1178,1356,951,1008,1477,1236,235,506,257])).
% 59.88/59.94 cnf(2519,plain,
% 59.88/59.94 (P6(a16,a16,a15,a16)),
% 59.88/59.94 inference(scs_inference,[],[2347,2418,2293,2251,2259,2273,2327,2341,2414,2419,2425,2363,1070,259,158,169,415,975,260,664,832,1269,171,261,603,1470,1436,627,228,1153,1203,1299,572,170,258,706,1441,790,1178,1356,951,1008,1477,1236,235,506,257,154,173,172])).
% 59.88/59.94 cnf(2521,plain,
% 59.88/59.94 (P9(x25211,x25212,x25213,x25214,x25212,x25211,x25213,x25214)),
% 59.88/59.94 inference(scs_inference,[],[2347,2418,2293,2251,2259,2273,2327,2341,2414,2419,2425,2363,1070,259,158,169,415,975,260,664,832,1269,171,261,603,1470,1436,627,228,1153,1203,1299,572,170,258,706,1441,790,1178,1356,951,1008,1477,1236,235,506,257,154,173,172,256])).
% 59.88/59.94 cnf(2525,plain,
% 59.88/59.94 (P10(a16,a1,a2,a16)),
% 59.88/59.94 inference(scs_inference,[],[2347,2418,2293,2036,2251,2259,2273,2327,2341,2414,2419,2425,2363,1070,259,158,169,415,975,260,664,832,1269,171,261,603,1470,1436,627,228,1153,1203,1299,572,170,258,706,1441,790,1178,1356,951,1008,1477,1236,235,506,257,154,173,172,256,254,165])).
% 59.88/59.94 cnf(2529,plain,
% 59.88/59.94 (P1(x25291,x25292,x25291)),
% 59.88/59.94 inference(scs_inference,[],[2347,2345,2418,2293,2036,2052,2251,2259,2273,2327,2341,2414,2419,2425,2363,1070,259,158,169,415,975,260,664,832,1269,171,261,603,1470,1436,627,228,1153,1203,1299,572,170,258,706,1441,790,1178,1356,951,1008,1477,1236,235,506,257,154,173,172,256,254,165,226,153])).
% 59.88/59.94 cnf(2533,plain,
% 59.88/59.94 (P1(a16,a2,a1)),
% 59.88/59.94 inference(scs_inference,[],[2347,2345,2418,2293,2323,2036,2052,2251,2259,2273,2327,2341,2414,2419,2425,2363,1070,259,158,169,415,975,260,664,832,1269,171,261,603,1470,1436,627,228,1153,1203,1299,572,170,258,706,1441,790,1178,1356,951,1008,1477,1236,235,506,257,154,173,172,256,254,165,226,153,255,162])).
% 59.88/59.94 cnf(2535,plain,
% 59.88/59.94 (P9(a2,a16,x25351,x25352,a16,a1,x25351,x25352)),
% 59.88/59.94 inference(scs_inference,[],[2347,2345,2418,2293,2323,2036,2052,2251,2259,2273,2327,2341,2414,2419,2425,2363,1070,259,158,169,415,975,260,664,832,1269,171,261,603,1470,1436,627,228,1153,1203,1299,572,170,258,706,1441,790,1178,1356,951,1008,1477,1236,235,506,257,154,173,172,256,254,165,226,153,255,162,227])).
% 59.88/59.94 cnf(2541,plain,
% 59.88/59.94 (P3(x25411,x25412,x25412,x25411)),
% 59.88/59.94 inference(scs_inference,[],[2347,2408,2345,2418,2293,2323,2036,2052,2251,2259,2273,2327,2341,2355,2389,2414,2419,2425,2363,1070,259,158,169,415,975,260,664,832,1269,171,261,603,1470,1436,627,228,1153,1203,1299,572,170,258,706,1441,790,1178,1356,951,1008,1477,1236,235,506,257,154,173,172,256,254,165,226,153,255,162,227,167,189,168])).
% 59.88/59.94 cnf(2543,plain,
% 59.88/59.94 (P10(a2,a16,a1,a16)),
% 59.88/59.94 inference(scs_inference,[],[2347,2408,2345,2418,2293,2323,2036,2052,2251,2259,2273,2327,2341,2355,2389,2414,2419,2425,2363,1070,259,158,169,415,975,260,664,832,1269,171,261,603,1470,1436,627,228,1153,1203,1299,572,170,258,706,1441,790,1178,1356,951,1008,1477,1236,235,506,257,154,173,172,256,254,165,226,153,255,162,227,167,189,168,166])).
% 59.88/59.94 cnf(2545,plain,
% 59.88/59.94 (P5(a2,a16,a2,a16)),
% 59.88/59.94 inference(scs_inference,[],[2347,2408,2345,2418,2293,2323,2373,2036,2052,2251,2259,2273,2327,2341,2355,2389,2414,2419,2425,2363,1070,259,158,169,415,975,260,664,832,1269,171,261,603,1470,1436,627,228,1153,1203,1299,572,170,258,706,1441,790,1178,1356,951,1008,1477,1236,235,506,257,154,173,172,256,254,165,226,153,255,162,227,167,189,168,166,176])).
% 59.88/59.94 cnf(2546,plain,
% 59.88/59.94 (P3(x25461,x25462,x25461,x25462)),
% 59.88/59.94 inference(rename_variables,[],[2408])).
% 59.88/59.94 cnf(2549,plain,
% 59.88/59.94 (P3(x25491,x25492,x25491,x25492)),
% 59.88/59.94 inference(rename_variables,[],[2408])).
% 59.88/59.94 cnf(2556,plain,
% 59.88/59.94 (P3(x25561,x25562,x25561,x25562)),
% 59.88/59.94 inference(rename_variables,[],[2408])).
% 59.88/59.94 cnf(2559,plain,
% 59.88/59.94 (P3(x25591,x25592,x25591,x25592)),
% 59.88/59.94 inference(rename_variables,[],[2408])).
% 59.88/59.94 cnf(2561,plain,
% 59.88/59.94 (~P10(a18,f34(a18,a20,a17,a17),a20,f34(a18,a20,a17,a17))),
% 59.88/59.94 inference(scs_inference,[],[2347,2408,2546,2549,2556,2345,2418,2293,2323,2373,2036,2052,2251,2259,2273,2327,2341,2355,2389,2414,2419,2243,2369,2425,2363,430,1070,259,158,169,415,975,260,664,832,1269,171,261,603,1470,1436,627,228,1153,1203,1299,572,170,258,706,1441,790,1178,1356,951,1008,1477,1236,235,506,257,154,173,172,256,254,165,226,153,255,162,227,167,189,168,166,176,252,185,225,195,203,242])).
% 59.88/59.94 cnf(2564,plain,
% 59.88/59.94 (P3(x25641,x25642,x25641,x25642)),
% 59.88/59.94 inference(rename_variables,[],[2408])).
% 59.88/59.94 cnf(2565,plain,
% 59.88/59.94 (P9(x25651,x25652,x25653,x25654,x25651,x25652,x25653,x25654)),
% 59.88/59.94 inference(rename_variables,[],[2347])).
% 59.88/59.94 cnf(2568,plain,
% 59.88/59.94 (P3(x25681,x25682,x25681,x25682)),
% 59.88/59.94 inference(rename_variables,[],[2408])).
% 59.88/59.94 cnf(2571,plain,
% 59.88/59.94 (P9(x25711,x25712,x25713,x25714,x25711,x25712,x25713,x25714)),
% 59.88/59.94 inference(rename_variables,[],[2347])).
% 59.88/59.94 cnf(2574,plain,
% 59.88/59.94 (P3(x25741,x25742,x25741,x25742)),
% 59.88/59.94 inference(rename_variables,[],[2408])).
% 59.88/59.94 cnf(2576,plain,
% 59.88/59.94 (P1(f5(x25761,x25761,x25762),x25762,x25761)),
% 59.88/59.94 inference(scs_inference,[],[2347,2565,2408,2546,2549,2556,2559,2564,2568,2574,2345,2418,2293,2323,2373,2036,2052,2251,2259,2273,2327,2341,2355,2389,2403,2414,2419,2243,2369,2425,2363,351,430,1070,259,158,169,415,975,260,664,832,1269,171,261,603,1470,1436,627,228,1153,1203,1299,572,170,258,706,1441,790,1178,1356,951,1008,1477,1236,235,506,257,154,173,172,256,254,165,226,153,255,162,227,167,189,168,166,176,252,185,225,195,203,242,248,193,262,196,180])).
% 59.88/59.94 cnf(2581,plain,
% 59.88/59.94 (P9(x25811,x25812,x25813,x25814,x25811,x25812,x25813,x25814)),
% 59.88/59.94 inference(rename_variables,[],[2347])).
% 59.88/59.94 cnf(2585,plain,
% 59.88/59.94 (P3(a16,a2,a2,a2)),
% 59.88/59.94 inference(scs_inference,[],[2347,2565,2571,2581,2408,2546,2549,2556,2559,2564,2568,2574,2345,2418,2293,2323,2373,2036,2052,2251,2259,2273,2327,2341,2355,2389,2403,2414,2419,2243,2369,2425,2363,351,430,1070,259,158,169,415,975,260,664,832,1269,171,261,603,1470,1436,627,228,1153,1203,1299,572,170,258,706,1441,790,1178,1356,951,1008,1477,1236,235,506,257,154,173,172,256,254,165,226,153,255,162,227,167,189,168,166,176,252,185,225,195,203,242,248,193,262,196,180,190,246,251,244])).
% 59.88/59.94 cnf(2586,plain,
% 59.88/59.94 (P9(x25861,x25862,x25863,x25864,x25861,x25862,x25863,x25864)),
% 59.88/59.94 inference(rename_variables,[],[2347])).
% 59.88/59.94 cnf(2588,plain,
% 59.88/59.94 (P3(x25881,f4(x25881,x25881,x25882),x25882,x25881)),
% 59.88/59.94 inference(scs_inference,[],[2347,2565,2571,2581,2408,2546,2549,2556,2559,2564,2568,2574,2345,2418,2293,2323,2373,2036,2052,2251,2259,2273,2327,2341,2355,2389,2403,2414,2419,2243,2369,2425,2363,351,430,1070,259,158,169,415,975,260,664,832,1269,171,261,603,1470,1436,627,228,1153,1203,1299,572,170,258,706,1441,790,1178,1356,951,1008,1477,1236,235,506,257,154,173,172,256,254,165,226,153,255,162,227,167,189,168,166,176,252,185,225,195,203,242,248,193,262,196,180,190,246,251,244,191])).
% 59.88/59.94 cnf(2590,plain,
% 59.88/59.94 (~P10(f34(a18,a20,a17,a17),a18,a20,f34(a18,a20,a17,a17))),
% 59.88/59.94 inference(scs_inference,[],[2347,2565,2571,2581,2353,2408,2546,2549,2556,2559,2564,2568,2574,2345,2418,2293,2323,2373,2036,2052,2251,2259,2273,2327,2341,2355,2389,2403,2414,2419,2243,2369,2425,2363,351,430,1070,259,158,169,415,975,260,664,832,1269,171,261,603,1470,1436,627,228,1153,1203,1299,572,170,258,706,1441,790,1178,1356,951,1008,1477,1236,235,506,257,154,173,172,256,254,165,226,153,255,162,227,167,189,168,166,176,252,185,225,195,203,242,248,193,262,196,180,190,246,251,244,191,181])).
% 59.88/59.94 cnf(2591,plain,
% 59.88/59.94 (P10(x25911,x25912,x25912,x25911)),
% 59.88/59.94 inference(rename_variables,[],[2353])).
% 59.88/59.94 cnf(2596,plain,
% 59.88/59.94 (P3(x25961,x25962,x25961,x25962)),
% 59.88/59.94 inference(rename_variables,[],[2408])).
% 59.88/59.94 cnf(2598,plain,
% 59.88/59.94 (P2(a2,a2,a16,a16)),
% 59.88/59.94 inference(scs_inference,[],[2347,2565,2571,2581,2353,2408,2546,2549,2556,2559,2564,2568,2574,2345,2418,2293,2323,2373,2036,2052,2251,2259,2273,2327,2341,2355,2389,2403,2414,2419,2243,2369,2425,2363,351,430,1070,259,158,169,415,975,260,664,832,1269,171,261,603,1470,1436,627,228,1153,1203,1299,572,170,258,706,1441,790,1178,1356,951,1008,1477,1236,235,506,257,154,173,172,256,254,165,226,153,255,162,227,167,189,168,166,176,252,185,225,195,203,242,248,193,262,196,180,190,246,251,244,191,181,179,201,186])).
% 59.88/59.94 cnf(2601,plain,
% 59.88/59.94 (P3(x26011,x26012,x26011,x26012)),
% 59.88/59.94 inference(rename_variables,[],[2408])).
% 59.88/59.94 cnf(2604,plain,
% 59.88/59.94 (P3(x26041,x26042,x26041,x26042)),
% 59.88/59.94 inference(rename_variables,[],[2408])).
% 59.88/59.94 cnf(2611,plain,
% 59.88/59.94 (P3(x26111,x26112,x26111,x26112)),
% 59.88/59.94 inference(rename_variables,[],[2408])).
% 59.88/59.94 cnf(2613,plain,
% 59.88/59.94 (P6(x26131,x26132,x26132,x26132)),
% 59.88/59.94 inference(scs_inference,[],[142,2347,2565,2571,2581,2586,2353,2408,2546,2549,2556,2559,2564,2568,2574,2596,2601,2604,2345,2418,2293,2323,2373,2036,2052,2251,2259,2273,2327,2341,2355,2389,2403,2414,2419,2243,2369,2425,2363,351,430,2154,1070,259,158,169,415,975,260,664,832,1269,171,261,603,1470,1436,627,228,1153,1203,1299,572,170,258,706,1441,790,1178,1356,951,1008,1477,1236,235,506,257,154,173,172,256,254,165,226,153,255,162,227,167,189,168,166,176,252,185,225,195,203,242,248,193,262,196,180,190,246,251,244,191,181,179,201,186,200,202,229,178,199,238])).
% 59.88/59.94 cnf(2614,plain,
% 59.88/59.94 (P9(x26141,x26142,x26143,x26144,x26141,x26142,x26143,x26144)),
% 59.88/59.94 inference(rename_variables,[],[2347])).
% 59.88/59.94 cnf(2615,plain,
% 59.88/59.94 (P1(x26151,x26152,x26152)),
% 59.88/59.94 inference(rename_variables,[],[2345])).
% 59.88/59.94 cnf(2620,plain,
% 59.88/59.94 (P3(x26201,x26202,x26201,x26202)),
% 59.88/59.94 inference(rename_variables,[],[2408])).
% 59.88/59.94 cnf(2622,plain,
% 59.88/59.94 (P3(x26221,f5(x26221,x26221,x26222),x26222,x26221)),
% 59.88/59.94 inference(scs_inference,[],[142,2347,2565,2571,2581,2586,2353,2408,2546,2549,2556,2559,2564,2568,2574,2596,2601,2604,2611,2620,2345,2418,2293,2323,2373,2036,2052,2251,2259,2273,2327,2341,2355,2389,2403,2414,2419,2243,2416,2369,2425,2363,457,351,430,2154,1070,259,158,169,415,975,260,664,832,1269,171,261,603,1470,1436,627,228,1153,1203,1299,572,170,258,706,1441,790,1178,1356,951,1008,1477,1236,235,506,257,154,173,172,256,254,165,226,153,255,162,227,167,189,168,166,176,252,185,225,195,203,242,248,193,262,196,180,190,246,251,244,191,181,179,201,186,200,202,229,178,199,238,183,182,192])).
% 59.88/59.94 cnf(2624,plain,
% 59.88/59.94 (P3(a2,a2,a2,a16)),
% 59.88/59.94 inference(scs_inference,[],[142,2347,2565,2571,2581,2586,2353,2408,2546,2549,2556,2559,2564,2568,2574,2596,2601,2604,2611,2620,2345,2418,2293,2323,2373,2036,2052,2251,2259,2273,2327,2341,2355,2389,2403,2414,2419,2243,2416,2369,2425,2363,457,351,430,2154,1070,259,158,169,415,975,260,664,832,1269,171,261,603,1470,1436,627,228,1153,1203,1299,572,170,258,706,1441,790,1178,1356,951,1008,1477,1236,235,506,257,154,173,172,256,254,165,226,153,255,162,227,167,189,168,166,176,252,185,225,195,203,242,248,193,262,196,180,190,246,251,244,191,181,179,201,186,200,202,229,178,199,238,183,182,192,243])).
% 59.88/59.94 cnf(2625,plain,
% 59.88/59.94 (P3(x26251,x26252,x26251,x26252)),
% 59.88/59.94 inference(rename_variables,[],[2408])).
% 59.88/59.94 cnf(2628,plain,
% 59.88/59.94 (P10(x26281,x26282,x26282,x26281)),
% 59.88/59.94 inference(rename_variables,[],[2353])).
% 59.88/59.94 cnf(2635,plain,
% 59.88/59.94 (P4(a2,a2,a2)),
% 59.88/59.94 inference(scs_inference,[],[142,2347,2565,2571,2581,2586,2353,2591,2408,2546,2549,2556,2559,2564,2568,2574,2596,2601,2604,2611,2620,2625,2345,2615,2418,2293,2323,2373,2036,2052,2251,2259,2273,2327,2341,2355,2389,2403,2410,2414,2419,2243,2416,2369,2074,2425,2363,2046,457,351,430,2154,1070,259,158,169,415,975,260,664,832,1269,171,261,603,1470,1436,627,228,1153,1203,1299,572,170,258,706,1441,790,1178,1356,951,1008,1477,1236,235,506,257,154,173,172,256,254,165,226,153,255,162,227,167,189,168,166,176,252,185,225,195,203,242,248,193,262,196,180,190,246,251,244,191,181,179,201,186,200,202,229,178,199,238,183,182,192,243,194,230,188,241])).
% 59.88/59.94 cnf(2636,plain,
% 59.88/59.94 (P1(x26361,x26362,x26362)),
% 59.88/59.94 inference(rename_variables,[],[2345])).
% 59.88/59.94 cnf(2644,plain,
% 59.88/59.94 (P10(x26441,x26442,x26442,x26441)),
% 59.88/59.94 inference(rename_variables,[],[2353])).
% 59.88/59.94 cnf(2649,plain,
% 59.88/59.94 (P4(f30(a2,x26491),a2,x26491)),
% 59.88/59.94 inference(scs_inference,[],[142,2347,2565,2571,2581,2586,2353,2591,2628,2644,2408,2546,2549,2556,2559,2564,2568,2574,2596,2601,2604,2611,2620,2625,2345,2615,2636,2418,2293,2323,2373,2036,2052,2251,2259,2273,2327,2341,2355,2389,2403,2410,2414,2419,2243,2416,2369,2074,2425,2363,1924,2046,2060,457,351,430,2154,1070,259,158,169,415,975,260,664,832,1269,171,261,603,1470,1436,627,228,1153,1203,1299,572,170,258,706,1441,790,1178,1356,951,1008,1477,1236,235,506,257,154,173,172,256,254,165,226,153,255,162,227,167,189,168,166,176,252,185,225,195,203,242,248,193,262,196,180,190,246,251,244,191,181,179,201,186,200,202,229,178,199,238,183,182,192,243,194,230,188,241,210,211,208,209,161])).
% 59.88/59.94 cnf(2661,plain,
% 59.88/59.94 (P4(f6(a2,a2,a16),a16,a2)),
% 59.88/59.94 inference(scs_inference,[],[142,2347,2565,2571,2581,2586,2353,2591,2628,2644,2408,2546,2549,2556,2559,2564,2568,2574,2596,2601,2604,2611,2620,2625,2345,2615,2636,2418,2293,2323,2373,2036,2052,2251,2259,2273,2327,2341,2355,2389,2403,2410,2414,2419,2243,2416,2369,2074,2425,2363,1924,2046,2060,457,351,430,2154,1070,259,158,169,415,975,260,664,832,1269,171,261,603,1470,1436,627,228,1153,1203,1299,572,170,258,706,1441,790,1178,1356,951,1008,1477,1236,235,506,257,154,173,172,256,254,165,226,153,255,162,227,167,189,168,166,176,252,185,225,195,203,242,248,193,262,196,180,190,246,251,244,191,181,179,201,186,200,202,229,178,199,238,183,182,192,243,194,230,188,241,210,211,208,209,161,666,1010,1238,1301,156])).
% 59.88/59.94 cnf(2710,plain,
% 59.88/59.94 (P10(a2,a2,a16,a16)),
% 59.88/59.94 inference(scs_inference,[],[142,2347,2565,2571,2581,2586,2614,2353,2591,2628,2644,2408,2546,2549,2556,2559,2564,2568,2574,2596,2601,2604,2611,2620,2625,2345,2615,2636,2418,2293,2323,2373,2036,2052,2225,2251,2259,2273,2327,2341,2355,2389,2403,2410,2414,2419,2243,2416,2369,2074,2425,2363,2375,1924,2046,2060,457,351,430,2154,1070,259,158,169,415,975,260,664,832,1269,171,261,603,1470,1436,627,228,1153,1203,1299,572,170,258,706,1441,790,1178,1356,951,1008,1477,1236,235,506,257,154,173,172,256,254,165,226,153,255,162,227,167,189,168,166,176,252,185,225,195,203,242,248,193,262,196,180,190,246,251,244,191,181,179,201,186,200,202,229,178,199,238,183,182,192,243,194,230,188,241,210,211,208,209,161,666,1010,1238,1301,156,1072,954,1358,1271,508,629,1155,792,708,574,1443,1205,605,1180,977,296,155,1834,232,240,207,249,250,159])).
% 59.88/59.94 cnf(2712,plain,
% 59.88/59.94 (P4(f33(a2,a2,a2,a2,a2,a2),a2,a2)),
% 59.88/59.94 inference(scs_inference,[],[142,2347,2565,2571,2581,2586,2614,2353,2591,2628,2644,2408,2546,2549,2556,2559,2564,2568,2574,2596,2601,2604,2611,2620,2625,2345,2615,2636,2418,2293,2323,2373,2036,2052,2225,2251,2259,2273,2327,2341,2355,2389,2403,2410,2414,2419,2243,2416,2369,2074,2425,2363,2375,1924,2046,2060,457,351,430,2154,1070,259,158,169,415,975,260,664,832,1269,171,261,603,1470,1436,627,228,1153,1203,1299,572,170,258,706,1441,790,1178,1356,951,1008,1477,1236,235,506,257,154,173,172,256,254,165,226,153,255,162,227,167,189,168,166,176,252,185,225,195,203,242,248,193,262,196,180,190,246,251,244,191,181,179,201,186,200,202,229,178,199,238,183,182,192,243,194,230,188,241,210,211,208,209,161,666,1010,1238,1301,156,1072,954,1358,1271,508,629,1155,792,708,574,1443,1205,605,1180,977,296,155,1834,232,240,207,249,250,159,205])).
% 59.88/59.94 cnf(2725,plain,
% 59.88/59.94 (P6(a20,a18,a17,a17)),
% 59.88/59.94 inference(scs_inference,[],[2513,347])).
% 59.88/59.94 cnf(2726,plain,
% 59.88/59.94 (P9(x27261,x27262,x27261,x27262,x27263,x27264,x27263,x27264)),
% 59.88/59.94 inference(rename_variables,[],[2513])).
% 59.88/59.94 cnf(2730,plain,
% 59.88/59.94 (P9(a2,a2,x27301,x27302,a2,a16,x27301,x27302)),
% 59.88/59.94 inference(scs_inference,[],[2513,2509,347,1070,227])).
% 59.88/59.94 cnf(2734,plain,
% 59.88/59.94 (P9(x27341,x27342,x27343,x27344,x27341,x27342,x27344,x27343)),
% 59.88/59.94 inference(scs_inference,[],[2513,2521,2509,2661,347,1070,227,158,255])).
% 59.88/59.94 cnf(2737,plain,
% 59.88/59.94 (P3(x27371,f4(x27371,x27371,x27372),x27372,x27371)),
% 59.88/59.94 inference(rename_variables,[],[2588])).
% 59.88/59.94 cnf(2740,plain,
% 59.88/59.94 (P3(x27401,f4(x27401,x27401,x27402),x27402,x27401)),
% 59.88/59.94 inference(rename_variables,[],[2588])).
% 59.88/59.94 cnf(2747,plain,
% 59.88/59.94 (P3(x27471,f4(x27471,x27471,x27472),x27472,x27471)),
% 59.88/59.94 inference(rename_variables,[],[2588])).
% 59.88/59.94 cnf(2754,plain,
% 59.88/59.94 (P3(x27541,f4(x27541,x27541,x27542),x27542,x27541)),
% 59.88/59.94 inference(rename_variables,[],[2588])).
% 59.88/59.94 cnf(2757,plain,
% 59.88/59.94 (P3(x27571,f4(x27571,x27571,x27572),x27572,x27571)),
% 59.88/59.94 inference(rename_variables,[],[2588])).
% 59.88/59.94 cnf(2760,plain,
% 59.88/59.94 (P3(x27601,f4(x27601,x27601,x27602),x27602,x27601)),
% 59.88/59.94 inference(rename_variables,[],[2588])).
% 59.88/59.94 cnf(2774,plain,
% 59.88/59.94 (P6(x27741,x27742,x27741,x27741)),
% 59.88/59.94 inference(scs_inference,[],[2513,2521,2613,2447,2457,2467,2509,2598,2588,2737,2740,2747,2754,2757,2383,2661,347,1070,227,158,255,1301,666,415,260,1358,259,1470,708,792,1238,170,706,1203,261,975,189,171])).
% 59.88/59.94 cnf(2776,plain,
% 59.88/59.94 (P3(a2,a2,a16,a2)),
% 59.88/59.94 inference(scs_inference,[],[2513,2521,2613,2447,2585,2457,2467,2509,2598,2588,2737,2740,2747,2754,2757,2383,2661,347,1070,227,158,255,1301,666,415,260,1358,259,1470,708,792,1238,170,706,1203,261,975,189,171,167])).
% 59.88/59.94 cnf(2778,plain,
% 59.88/59.94 (P4(f30(a2,x27781),x27781,a2)),
% 59.88/59.94 inference(scs_inference,[],[2513,2521,2613,2447,2585,2457,2467,2509,2598,2588,2737,2740,2747,2754,2757,2383,2661,2649,347,1070,227,158,255,1301,666,415,260,1358,259,1470,708,792,1238,170,706,1203,261,975,189,171,167,156])).
% 59.88/59.94 cnf(2783,plain,
% 59.88/59.94 (P3(x27831,f4(x27831,x27831,x27832),x27832,x27831)),
% 59.88/59.94 inference(rename_variables,[],[2588])).
% 59.88/59.94 cnf(2786,plain,
% 59.88/59.94 (P3(x27861,f4(x27861,x27861,x27862),x27862,x27861)),
% 59.88/59.94 inference(rename_variables,[],[2588])).
% 59.88/59.94 cnf(2789,plain,
% 59.88/59.94 (P3(x27891,f4(x27891,x27891,x27892),x27892,x27891)),
% 59.88/59.94 inference(rename_variables,[],[2588])).
% 59.88/59.94 cnf(2794,plain,
% 59.88/59.94 (P3(x27941,f4(x27941,x27941,x27942),x27942,x27941)),
% 59.88/59.94 inference(rename_variables,[],[2588])).
% 59.88/59.94 cnf(2799,plain,
% 59.88/59.94 (P3(x27991,f4(x27991,x27991,x27992),x27992,x27991)),
% 59.88/59.94 inference(rename_variables,[],[2588])).
% 59.88/59.94 cnf(2806,plain,
% 59.88/59.94 (P3(x28061,f4(x28061,x28061,x28062),x28062,x28061)),
% 59.88/59.94 inference(rename_variables,[],[2588])).
% 59.88/59.94 cnf(2821,plain,
% 59.88/59.94 (P3(x28211,f4(x28211,x28211,x28212),x28212,x28211)),
% 59.88/59.94 inference(rename_variables,[],[2588])).
% 59.88/59.94 cnf(2824,plain,
% 59.88/59.94 (P3(x28241,f4(x28241,x28241,x28242),x28242,x28241)),
% 59.88/59.94 inference(rename_variables,[],[2588])).
% 59.88/59.94 cnf(2827,plain,
% 59.88/59.94 (P3(x28271,f4(x28271,x28271,x28272),x28272,x28271)),
% 59.88/59.94 inference(rename_variables,[],[2588])).
% 59.88/59.94 cnf(2832,plain,
% 59.88/59.94 (P3(x28321,f4(x28321,x28321,x28322),x28322,x28321)),
% 59.88/59.94 inference(rename_variables,[],[2588])).
% 59.88/59.94 cnf(2839,plain,
% 59.88/59.95 (P3(x28391,f4(x28391,x28391,x28392),x28392,x28391)),
% 59.88/59.95 inference(rename_variables,[],[2588])).
% 59.88/59.95 cnf(2850,plain,
% 59.88/59.95 (P3(x28501,f4(x28501,x28501,x28502),x28502,x28501)),
% 59.88/59.95 inference(rename_variables,[],[2588])).
% 59.88/59.95 cnf(2853,plain,
% 59.88/59.95 (P3(x28531,f4(x28531,x28531,x28532),x28532,x28531)),
% 59.88/59.95 inference(rename_variables,[],[2588])).
% 59.88/59.95 cnf(2861,plain,
% 59.88/59.95 (P9(x28611,x28612,x28612,x28611,x28613,x28614,x28613,x28614)),
% 59.88/59.95 inference(scs_inference,[],[2513,2521,2613,2487,2447,2585,2457,2467,2509,2545,2598,2588,2737,2740,2747,2754,2757,2760,2783,2786,2789,2794,2799,2806,2821,2824,2827,2832,2839,2850,2383,2661,2649,347,1070,227,158,255,1301,666,415,260,1358,259,1470,708,792,1238,170,706,1203,261,975,189,171,167,156,228,1010,1180,574,664,1072,603,1443,832,1299,954,169,1356,790,627,572,1269,629,508,1271,951,1205,1153,1436,1155,1236,1008,1178,258,977,605,1477,1441,506,257])).
% 59.88/59.95 cnf(2870,plain,
% 59.88/59.95 (P10(a2,a2,a16,a2)),
% 59.88/59.95 inference(scs_inference,[],[2513,2521,2613,2487,2447,2585,2457,2467,2509,2519,2545,2598,2588,2737,2740,2747,2754,2757,2760,2783,2786,2789,2794,2799,2806,2821,2824,2827,2832,2839,2850,2853,2383,2661,2649,347,1070,227,158,255,1301,666,415,260,1358,259,1470,708,792,1238,170,706,1203,261,975,189,171,167,156,228,1010,1180,574,664,1072,603,1443,832,1299,954,169,1356,790,627,572,1269,629,508,1271,951,1205,1153,1436,1155,1236,1008,1178,258,977,605,1477,1441,506,257,173,168,296,166])).
% 59.88/59.95 cnf(2872,plain,
% 59.88/59.95 (P1(x28721,x28721,x28722)),
% 59.88/59.95 inference(scs_inference,[],[2513,2521,2613,2529,2487,2447,2585,2457,2467,2509,2519,2545,2598,2588,2737,2740,2747,2754,2757,2760,2783,2786,2789,2794,2799,2806,2821,2824,2827,2832,2839,2850,2853,2383,2661,2649,347,1070,227,158,255,1301,666,415,260,1358,259,1470,708,792,1238,170,706,1203,261,975,189,171,167,156,228,1010,1180,574,664,1072,603,1443,832,1299,954,169,1356,790,627,572,1269,629,508,1271,951,1205,1153,1436,1155,1236,1008,1178,258,977,605,1477,1441,506,257,173,168,296,166,154])).
% 59.88/59.95 cnf(2876,plain,
% 59.88/59.95 (P9(a16,a2,x28761,x28762,a16,a1,x28761,x28762)),
% 59.88/59.95 inference(scs_inference,[],[2513,2521,2613,2529,2487,2447,2335,2585,2535,2457,2467,2509,2519,2545,2598,2588,2737,2740,2747,2754,2757,2760,2783,2786,2789,2794,2799,2806,2821,2824,2827,2832,2839,2850,2853,2383,2661,2649,347,1070,227,158,255,1301,666,415,260,1358,259,1470,708,792,1238,170,706,1203,261,975,189,171,167,156,228,1010,1180,574,664,1072,603,1443,832,1299,954,169,1356,790,627,572,1269,629,508,1271,951,1205,1153,1436,1155,1236,1008,1178,258,977,605,1477,1441,506,257,173,168,296,166,154,172,256])).
% 59.88/59.95 cnf(2882,plain,
% 59.88/59.95 (P9(a16,a1,x28821,x28822,a2,a16,x28821,x28822)),
% 59.88/59.95 inference(scs_inference,[],[2513,2521,2613,2529,2487,2447,2335,2585,2535,2457,2467,2509,2519,2545,2598,2588,2737,2740,2747,2754,2757,2760,2783,2786,2789,2794,2799,2806,2821,2824,2827,2832,2839,2850,2853,2383,2661,2649,347,1070,227,158,255,1301,666,415,260,1358,259,1470,708,792,1238,170,706,1203,261,975,189,171,167,156,228,1010,1180,574,664,1072,603,1443,832,1299,954,169,1356,790,627,572,1269,629,508,1271,951,1205,1153,1436,1155,1236,1008,1178,258,977,605,1477,1441,506,257,173,168,296,166,154,172,256,155,165,254])).
% 59.88/59.95 cnf(2888,plain,
% 59.88/59.95 (P3(a2,a16,a16,a16)),
% 59.88/59.95 inference(scs_inference,[],[2513,2521,2613,2529,2487,2447,2335,2585,2535,2457,2467,2509,2519,2533,2545,2598,2588,2737,2740,2747,2754,2757,2760,2783,2786,2789,2794,2799,2806,2821,2824,2827,2832,2839,2850,2853,2383,2661,2649,347,1070,227,158,255,1301,666,415,260,1358,259,1470,708,792,1238,170,706,1203,261,975,189,171,167,156,228,1010,1180,574,664,1072,603,1443,832,1299,954,169,1356,790,627,572,1269,629,508,1271,951,1205,1153,1436,1155,1236,1008,1178,258,977,605,1477,1441,506,257,173,168,296,166,154,172,256,155,165,254,226,153,174])).
% 59.88/59.95 cnf(2892,plain,
% 59.88/59.95 (P10(a1,a16,a2,a16)),
% 59.88/59.95 inference(scs_inference,[],[2513,2521,2613,2529,2487,2447,2335,2349,2585,2535,2457,2467,2509,2519,2525,2533,2545,2598,2588,2737,2740,2747,2754,2757,2760,2783,2786,2789,2794,2799,2806,2821,2824,2827,2832,2839,2850,2853,2383,2661,2649,2072,347,1070,227,158,255,1301,666,415,260,1358,259,1470,708,792,1238,170,706,1203,261,975,189,171,167,156,228,1010,1180,574,664,1072,603,1443,832,1299,954,169,1356,790,627,572,1269,629,508,1271,951,1205,1153,1436,1155,1236,1008,1178,258,977,605,1477,1441,506,257,173,168,296,166,154,172,256,155,165,254,226,153,174,192,242])).
% 59.88/59.95 cnf(2893,plain,
% 59.88/59.95 (P9(x28931,x28932,x28933,x28934,x28932,x28931,x28933,x28934)),
% 59.88/59.95 inference(rename_variables,[],[2521])).
% 59.88/59.95 cnf(2895,plain,
% 59.88/59.95 (P3(a2,a16,a2,a2)),
% 59.88/59.95 inference(scs_inference,[],[2513,2521,2893,2613,2529,2487,2447,2335,2349,2585,2535,2457,2467,2509,2519,2525,2533,2545,2598,2588,2737,2740,2747,2754,2757,2760,2783,2786,2789,2794,2799,2806,2821,2824,2827,2832,2839,2850,2853,2383,2661,2649,2072,347,1070,227,158,255,1301,666,415,260,1358,259,1470,708,792,1238,170,706,1203,261,975,189,171,167,156,228,1010,1180,574,664,1072,603,1443,832,1299,954,169,1356,790,627,572,1269,629,508,1271,951,1205,1153,1436,1155,1236,1008,1178,258,977,605,1477,1441,506,257,173,168,296,166,154,172,256,155,165,254,226,153,174,192,242,243])).
% 59.88/59.95 cnf(2896,plain,
% 59.88/59.95 (P9(x28961,x28962,x28963,x28964,x28962,x28961,x28963,x28964)),
% 59.88/59.95 inference(rename_variables,[],[2521])).
% 59.88/59.95 cnf(2901,plain,
% 59.88/59.95 (P9(x29011,x29012,x29013,x29014,x29012,x29011,x29013,x29014)),
% 59.88/59.95 inference(rename_variables,[],[2521])).
% 59.88/59.95 cnf(2904,plain,
% 59.88/59.95 (P9(x29041,x29042,x29043,x29044,x29042,x29041,x29043,x29044)),
% 59.88/59.95 inference(rename_variables,[],[2521])).
% 59.88/59.95 cnf(2910,plain,
% 59.88/59.95 (P2(f8(x29101,x29101,x29101),x29101,x29101,x29101)),
% 59.88/59.95 inference(scs_inference,[],[2237,2513,2521,2893,2896,2901,2541,2613,2529,2487,2447,2335,2349,2585,2624,2535,2387,2457,2467,2509,2519,2525,2533,2545,2598,2588,2737,2740,2747,2754,2757,2760,2783,2786,2789,2794,2799,2806,2821,2824,2827,2832,2839,2850,2853,2383,2661,2649,2225,2072,2414,347,1070,227,158,255,1301,666,415,260,1358,259,1470,708,792,1238,170,706,1203,261,975,189,171,167,156,228,1010,1180,574,664,1072,603,1443,832,1299,954,169,1356,790,627,572,1269,629,508,1271,951,1205,1153,1436,1155,1236,1008,1178,258,977,605,1477,1441,506,257,173,168,296,166,154,172,256,155,165,254,226,153,174,192,242,243,249,264,252,195,248,193])).
% 59.88/59.95 cnf(2911,plain,
% 59.88/59.95 (P3(x29111,x29112,x29112,x29111)),
% 59.88/59.95 inference(rename_variables,[],[2541])).
% 59.88/59.95 cnf(2912,plain,
% 59.88/59.95 (P6(x29121,x29122,x29122,x29122)),
% 59.88/59.95 inference(rename_variables,[],[2613])).
% 59.88/59.95 cnf(2917,plain,
% 59.88/59.95 (P3(x29171,x29172,x29172,x29171)),
% 59.88/59.95 inference(rename_variables,[],[2541])).
% 59.88/59.95 cnf(2921,plain,
% 59.88/59.95 (P3(x29211,x29212,x29212,x29211)),
% 59.88/59.95 inference(rename_variables,[],[2541])).
% 59.88/59.95 cnf(2924,plain,
% 59.88/59.95 (P9(x29241,x29242,x29243,x29244,x29241,x29242,x29243,x29244)),
% 59.88/59.95 inference(rename_variables,[],[2347])).
% 59.88/59.95 cnf(2934,plain,
% 59.88/59.95 (P3(x29341,x29342,x29342,x29341)),
% 59.88/59.95 inference(rename_variables,[],[2541])).
% 59.88/59.95 cnf(2942,plain,
% 59.88/59.95 (P2(a2,a16,a16,a16)),
% 59.88/59.95 inference(scs_inference,[],[2237,2513,2521,2893,2896,2901,2904,2541,2911,2917,2921,2613,2529,2487,2635,2447,2335,2349,2585,2624,2535,2387,2457,2467,2477,2509,2519,2525,2533,2543,2545,2598,2588,2737,2740,2747,2754,2757,2760,2783,2786,2789,2794,2799,2806,2821,2824,2827,2832,2839,2850,2853,2383,2661,2649,1417,2225,268,2347,2072,2154,2414,347,1070,227,158,255,1301,666,415,260,1358,259,1470,708,792,1238,170,706,1203,261,975,189,171,167,156,228,1010,1180,574,664,1072,603,1443,832,1299,954,169,1356,790,627,572,1269,629,508,1271,951,1205,1153,1436,1155,1236,1008,1178,258,977,605,1477,1441,506,257,173,168,296,166,154,172,256,155,165,254,226,153,174,192,242,243,249,264,252,195,248,193,225,203,231,262,247,251,180,190,196,179,181,186])).
% 59.88/59.95 cnf(2950,plain,
% 59.88/59.95 (P3(x29501,x29502,x29502,x29501)),
% 59.88/59.95 inference(rename_variables,[],[2541])).
% 59.88/59.95 cnf(2953,plain,
% 59.88/59.95 (P3(x29531,x29532,x29532,x29531)),
% 59.88/59.95 inference(rename_variables,[],[2541])).
% 59.88/59.95 cnf(2956,plain,
% 59.88/59.95 (P3(x29561,x29562,x29562,x29561)),
% 59.88/59.95 inference(rename_variables,[],[2541])).
% 59.88/59.95 cnf(2961,plain,
% 59.88/59.95 (P3(x29611,x29612,x29612,x29611)),
% 59.88/59.95 inference(rename_variables,[],[2541])).
% 59.88/59.95 cnf(2964,plain,
% 59.88/59.95 (P3(x29641,x29642,x29642,x29641)),
% 59.88/59.95 inference(rename_variables,[],[2541])).
% 59.88/59.95 cnf(2968,plain,
% 59.88/59.95 (P6(a18,a18,a1,a15)),
% 59.88/59.95 inference(scs_inference,[],[142,2237,2513,2726,2521,2893,2896,2901,2904,2541,2911,2917,2921,2934,2950,2953,2956,2961,2613,2529,2487,2635,2447,2335,2349,2585,2624,2535,2387,2457,2467,2477,2509,2519,2525,2533,2543,2545,2598,2588,2737,2740,2747,2754,2757,2760,2783,2786,2789,2794,2799,2806,2821,2824,2827,2832,2839,2850,2853,2576,2383,2661,2649,2359,1417,2225,268,2347,2924,2072,2154,2414,347,1070,227,158,255,1301,666,415,260,1358,259,1470,708,792,1238,170,706,1203,261,975,189,171,167,156,228,1010,1180,574,664,1072,603,1443,832,1299,954,169,1356,790,627,572,1269,629,508,1271,951,1205,1153,1436,1155,1236,1008,1178,258,977,605,1477,1441,506,257,173,168,296,166,154,172,256,155,165,254,226,153,174,192,242,243,249,264,252,195,248,193,225,203,231,262,247,251,180,190,196,179,181,186,246,191,200,202,178,229,201,199,88,238])).
% 59.88/59.95 cnf(2969,plain,
% 59.88/59.95 (P9(x29691,x29692,x29691,x29692,x29693,x29694,x29693,x29694)),
% 59.88/59.95 inference(rename_variables,[],[2513])).
% 59.88/59.95 cnf(2972,plain,
% 59.88/59.95 (P3(x29721,x29722,x29722,x29721)),
% 59.88/59.95 inference(rename_variables,[],[2541])).
% 59.88/59.95 cnf(2976,plain,
% 59.88/59.95 (P6(a16,f35(a2,a2,a16,a16,a2),a16,f35(a2,a2,a16,a16,a2))),
% 59.88/59.95 inference(scs_inference,[],[142,2237,2513,2726,2521,2893,2896,2901,2904,2541,2911,2917,2921,2934,2950,2953,2956,2961,2964,2613,2529,2487,2635,2447,2335,2349,2585,2624,2535,2387,2457,2467,2477,2509,2519,2525,2533,2543,2545,2598,2588,2737,2740,2747,2754,2757,2760,2783,2786,2789,2794,2799,2806,2821,2824,2827,2832,2839,2850,2853,2576,2383,2661,2649,2561,2359,1417,2225,268,2347,2924,2072,2154,2414,347,1070,227,158,255,1301,666,415,260,1358,259,1470,708,792,1238,170,706,1203,261,975,189,171,167,156,228,1010,1180,574,664,1072,603,1443,832,1299,954,169,1356,790,627,572,1269,629,508,1271,951,1205,1153,1436,1155,1236,1008,1178,258,977,605,1477,1441,506,257,173,168,296,166,154,172,256,155,165,254,226,153,174,192,242,243,249,264,252,195,248,193,225,203,231,262,247,251,180,190,196,179,181,186,246,191,200,202,178,229,201,199,88,238,182,183,198])).
% 59.88/59.95 cnf(2981,plain,
% 59.88/59.95 (P3(x29811,x29812,x29812,x29811)),
% 59.88/59.95 inference(rename_variables,[],[2541])).
% 59.88/59.95 cnf(2983,plain,
% 59.88/59.95 (P4(a2,a2,a16)),
% 59.88/59.95 inference(scs_inference,[],[142,2237,2513,2726,2521,2893,2896,2901,2904,2541,2911,2917,2921,2934,2950,2953,2956,2961,2964,2972,2613,2529,2487,2635,2447,2335,2349,2585,2624,2535,2387,2457,2467,2477,2509,2519,2525,2533,2543,2545,2598,2588,2737,2740,2747,2754,2757,2760,2783,2786,2789,2794,2799,2806,2821,2824,2827,2832,2839,2850,2853,2576,2383,2661,2649,2561,2359,1417,2225,2078,268,2347,2924,2072,2154,2414,347,1070,227,158,255,1301,666,415,260,1358,259,1470,708,792,1238,170,706,1203,261,975,189,171,167,156,228,1010,1180,574,664,1072,603,1443,832,1299,954,169,1356,790,627,572,1269,629,508,1271,951,1205,1153,1436,1155,1236,1008,1178,258,977,605,1477,1441,506,257,173,168,296,166,154,172,256,155,165,254,226,153,174,192,242,243,249,264,252,195,248,193,225,203,231,262,247,251,180,190,196,179,181,186,246,191,200,202,178,229,201,199,88,238,182,183,198,194,188,164])).
% 59.88/59.95 cnf(2985,plain,
% 59.88/59.95 (P4(a16,a16,a16)),
% 59.88/59.95 inference(scs_inference,[],[142,2237,2513,2726,2969,2521,2893,2896,2901,2904,2541,2911,2917,2921,2934,2950,2953,2956,2961,2964,2972,2613,2529,2487,2635,2447,2335,2349,2585,2624,2535,2387,2457,2467,2477,2509,2519,2525,2533,2543,2545,2598,2588,2737,2740,2747,2754,2757,2760,2783,2786,2789,2794,2799,2806,2821,2824,2827,2832,2839,2850,2853,2576,2383,2661,2649,2561,2359,1417,2225,2078,2345,268,2347,2924,2072,2154,2414,347,1070,227,158,255,1301,666,415,260,1358,259,1470,708,792,1238,170,706,1203,261,975,189,171,167,156,228,1010,1180,574,664,1072,603,1443,832,1299,954,169,1356,790,627,572,1269,629,508,1271,951,1205,1153,1436,1155,1236,1008,1178,258,977,605,1477,1441,506,257,173,168,296,166,154,172,256,155,165,254,226,153,174,192,242,243,249,264,252,195,248,193,225,203,231,262,247,251,180,190,196,179,181,186,246,191,200,202,178,229,201,199,88,238,182,183,198,194,188,164,241])).
% 59.88/59.95 cnf(2986,plain,
% 59.88/59.95 (P9(x29861,x29862,x29861,x29862,x29863,x29864,x29863,x29864)),
% 59.88/59.95 inference(rename_variables,[],[2513])).
% 59.88/59.95 cnf(2990,plain,
% 59.88/59.95 (P1(x29901,x29902,x29901)),
% 59.88/59.95 inference(rename_variables,[],[2529])).
% 59.88/59.95 cnf(2991,plain,
% 59.88/59.95 (P10(x29911,x29912,x29912,x29911)),
% 59.88/59.95 inference(rename_variables,[],[2353])).
% 59.88/59.95 cnf(2994,plain,
% 59.88/59.95 (P1(x29941,x29942,x29941)),
% 59.88/59.95 inference(rename_variables,[],[2529])).
% 59.88/59.95 cnf(2995,plain,
% 59.88/59.95 (P10(x29951,x29952,x29952,x29951)),
% 59.88/59.95 inference(rename_variables,[],[2353])).
% 59.88/59.95 cnf(2998,plain,
% 59.88/59.95 (P1(x29981,x29982,x29981)),
% 59.88/59.95 inference(rename_variables,[],[2529])).
% 59.88/59.95 cnf(2999,plain,
% 59.88/59.95 (P10(x29991,x29992,x29992,x29991)),
% 59.88/59.95 inference(rename_variables,[],[2353])).
% 59.88/59.95 cnf(3002,plain,
% 59.88/59.95 (P1(x30021,x30022,x30021)),
% 59.88/59.95 inference(rename_variables,[],[2529])).
% 59.88/59.95 cnf(3005,plain,
% 59.88/59.95 (P5(x30051,x30051,x30051,x30051)),
% 59.88/59.95 inference(scs_inference,[],[142,2237,2513,2726,2969,2986,2521,2893,2896,2901,2904,2541,2911,2917,2921,2934,2950,2953,2956,2961,2964,2972,2613,2912,2529,2990,2994,2998,2487,2635,2447,2335,2349,2585,2624,2535,2387,2457,2467,2477,2509,2519,2525,2533,2543,2545,2598,2588,2737,2740,2747,2754,2757,2760,2783,2786,2789,2794,2799,2806,2821,2824,2827,2832,2839,2850,2853,2576,2383,2661,2649,2561,2359,1417,2353,2991,2995,2999,2323,2225,2078,2345,268,2347,2924,1924,2072,2154,2414,347,1070,227,158,255,1301,666,415,260,1358,259,1470,708,792,1238,170,706,1203,261,975,189,171,167,156,228,1010,1180,574,664,1072,603,1443,832,1299,954,169,1356,790,627,572,1269,629,508,1271,951,1205,1153,1436,1155,1236,1008,1178,258,977,605,1477,1441,506,257,173,168,296,166,154,172,256,155,165,254,226,153,174,192,242,243,249,264,252,195,248,193,225,203,231,262,247,251,180,190,196,179,181,186,246,191,200,202,178,229,201,199,88,238,182,183,198,194,188,164,241,211,210,208,209,253])).
% 59.88/59.95 cnf(3009,plain,
% 59.88/59.95 (P9(x30091,x30092,x30091,x30092,x30093,x30094,x30093,x30094)),
% 59.88/59.95 inference(rename_variables,[],[2513])).
% 59.88/59.95 cnf(3011,plain,
% 59.88/59.95 (P4(f30(a16,x30111),a16,x30111)),
% 59.88/59.95 inference(scs_inference,[],[142,2237,2513,2726,2969,2986,2521,2893,2896,2901,2904,2541,2911,2917,2921,2934,2950,2953,2956,2961,2964,2972,2613,2912,2529,2990,2994,2998,3002,2487,2635,2447,2335,2349,2585,2624,2535,2387,2457,2467,2477,2509,2519,2525,2533,2543,2545,2598,2588,2737,2740,2747,2754,2757,2760,2783,2786,2789,2794,2799,2806,2821,2824,2827,2832,2839,2850,2853,2576,2383,2661,2649,2561,2381,2359,1417,2353,2991,2995,2999,2323,2225,2078,2345,268,2347,2924,1924,2072,2154,2414,347,1070,227,158,255,1301,666,415,260,1358,259,1470,708,792,1238,170,706,1203,261,975,189,171,167,156,228,1010,1180,574,664,1072,603,1443,832,1299,954,169,1356,790,627,572,1269,629,508,1271,951,1205,1153,1436,1155,1236,1008,1178,258,977,605,1477,1441,506,257,173,168,296,166,154,172,256,155,165,254,226,153,174,192,242,243,249,264,252,195,248,193,225,203,231,262,247,251,180,190,196,179,181,186,246,191,200,202,178,229,201,199,88,238,182,183,198,194,188,164,241,211,210,208,209,253,161])).
% 59.88/59.95 cnf(3018,plain,
% 59.88/59.95 (P3(x30181,x30182,x30182,x30181)),
% 59.88/59.95 inference(rename_variables,[],[2541])).
% 59.88/59.95 cnf(3026,plain,
% 59.88/59.95 (P5(a16,a2,a16,a16)),
% 59.88/59.95 inference(scs_inference,[],[142,2237,2513,2726,2969,2986,2521,2893,2896,2901,2904,2541,2911,2917,2921,2934,2950,2953,2956,2961,2964,2972,2981,3018,2613,2912,2529,2990,2994,2998,3002,2487,2635,2447,2335,2349,2585,2624,2535,2387,2457,2467,2477,2509,2519,2525,2533,2543,2545,2598,2588,2737,2740,2747,2754,2757,2760,2783,2786,2789,2794,2799,2806,2821,2824,2827,2832,2839,2850,2853,2576,2383,2661,2649,2561,2590,2381,2359,1417,2353,2991,2995,2999,2323,2225,2078,2345,268,2347,2924,1924,2072,2154,2414,347,1070,227,158,255,1301,666,415,260,1358,259,1470,708,792,1238,170,706,1203,261,975,189,171,167,156,228,1010,1180,574,664,1072,603,1443,832,1299,954,169,1356,790,627,572,1269,629,508,1271,951,1205,1153,1436,1155,1236,1008,1178,258,977,605,1477,1441,506,257,173,168,296,166,154,172,256,155,165,254,226,153,174,192,242,243,249,264,252,195,248,193,225,203,231,262,247,251,180,190,196,179,181,186,246,191,200,202,178,229,201,199,88,238,182,183,198,194,188,164,241,211,210,208,209,253,161,2,222,184,207,240,206,175])).
% 59.88/59.95 cnf(3031,plain,
% 59.88/59.95 (P5(a2,a16,a2,a2)),
% 59.88/59.95 inference(scs_inference,[],[142,2237,2513,2726,2969,2986,2521,2893,2896,2901,2904,2541,2911,2917,2921,2934,2950,2953,2956,2961,2964,2972,2981,3018,2613,2912,2529,2990,2994,2998,3002,2487,2635,2447,2335,2349,2585,2624,2535,2387,2457,2467,2477,2509,2519,2525,2533,2543,2545,2598,2588,2737,2740,2747,2754,2757,2760,2783,2786,2789,2794,2799,2806,2821,2824,2827,2832,2839,2850,2853,2576,2383,2661,2649,2561,2590,2381,2359,1417,2353,2991,2995,2999,2323,2225,2078,2345,2094,268,2347,2924,1924,2072,2154,2414,347,1070,227,158,255,1301,666,415,260,1358,259,1470,708,792,1238,170,706,1203,261,975,189,171,167,156,228,1010,1180,574,664,1072,603,1443,832,1299,954,169,1356,790,627,572,1269,629,508,1271,951,1205,1153,1436,1155,1236,1008,1178,258,977,605,1477,1441,506,257,173,168,296,166,154,172,256,155,165,254,226,153,174,192,242,243,249,264,252,195,248,193,225,203,231,262,247,251,180,190,196,179,181,186,246,191,200,202,178,229,201,199,88,238,182,183,198,194,188,164,241,211,210,208,209,253,161,2,222,184,207,240,206,175,205,245])).
% 59.88/59.95 cnf(3036,plain,
% 59.88/59.95 (P4(a2,a16,a2)),
% 59.88/59.95 inference(scs_inference,[],[142,2237,2513,2726,2969,2986,3009,2521,2893,2896,2901,2904,2541,2911,2917,2921,2934,2950,2953,2956,2961,2964,2972,2981,3018,2613,2912,2529,2990,2994,2998,3002,2487,2635,2447,2335,2349,2585,2624,2535,2387,2457,2467,2477,2509,2519,2525,2533,2543,2545,2598,2588,2737,2740,2747,2754,2757,2760,2783,2786,2789,2794,2799,2806,2821,2824,2827,2832,2839,2850,2853,2576,2383,2661,2649,2561,2590,2381,2359,1417,2353,2991,2995,2999,2323,2225,2078,2345,2094,268,2347,2924,1924,2072,2154,2414,347,1070,227,158,255,1301,666,415,260,1358,259,1470,708,792,1238,170,706,1203,261,975,189,171,167,156,228,1010,1180,574,664,1072,603,1443,832,1299,954,169,1356,790,627,572,1269,629,508,1271,951,1205,1153,1436,1155,1236,1008,1178,258,977,605,1477,1441,506,257,173,168,296,166,154,172,256,155,165,254,226,153,174,192,242,243,249,264,252,195,248,193,225,203,231,262,247,251,180,190,196,179,181,186,246,191,200,202,178,229,201,199,88,238,182,183,198,194,188,164,241,211,210,208,209,253,161,2,222,184,207,240,206,175,205,245,236,177])).
% 59.88/59.95 cnf(3193,plain,
% 59.88/59.95 (P5(x31931,x31931,x31931,x31931)),
% 59.88/59.95 inference(rename_variables,[],[3005])).
% 59.88/59.95 cnf(3204,plain,
% 59.88/59.95 (P3(x32041,x32042,x32042,x32041)),
% 59.88/59.95 inference(rename_variables,[],[2541])).
% 59.88/59.95 cnf(3228,plain,
% 59.88/59.95 (~P1(a17,a17,a20)),
% 59.88/59.95 inference(scs_inference,[],[143,3005,3193,2734,2774,2861,2872,2888,2333,2776,2895,2968,2730,2876,2882,2710,2725,2870,2892,2942,2983,2985,3026,3031,3036,2910,2622,2357,2712,2421,2778,3011,2976,2331,2371,2513,2541,3204,315,227,1070,255,666,1301,156,792,158,171,261,1470,259,706,1010,574,832,1443,415,975,954,1356,951,260,708,664,189,1358,603,170,1205,1269,1072,508,627,790,1299,169,1180,1203,1238,167,1441,228,1436,257,506,1153,629,605,572,1178,1271,977,173,1236,1155,1477,258,1008,168,296,172,166,154,165,155,256,254,153,226,192,184,206,243,242,203,249,207,264,193,195,231,175,252,225,196,180,190,205,157])).
% 59.88/59.95 cnf(3310,plain,
% 59.88/59.95 ($false),
% 59.88/59.95 inference(scs_inference,[],[3228,2872]),
% 59.88/59.95 ['proof']).
% 59.88/59.95 % SZS output end Proof
% 59.88/59.95 % Total time :59.260000s
%------------------------------------------------------------------------------