%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : GEO579+1 : TPTP v8.2.0. Released v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% Computer : n025.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Mon Jun 24 06:05:48 EDT 2024
% Result : Theorem 59.84s 59.93s
% Output : CNFRefutation 59.88s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.02/0.09 % Problem : GEO579+1 : TPTP v8.2.0. Released v7.5.0.
% 0.02/0.09 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% 0.09/0.31 % Computer : n025.cluster.edu
% 0.09/0.31 % Model : x86_64 x86_64
% 0.09/0.31 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.31 % Memory : 8042.1875MB
% 0.09/0.31 % OS : Linux 3.10.0-693.el7.x86_64
% 0.09/0.31 % CPULimit : 300
% 0.09/0.31 % WCLimit : 300
% 0.09/0.31 % DateTime : Fri Jun 21 08:31:09 EDT 2024
% 0.09/0.31 % CPUTime :
% 0.16/0.48 start to proof:theBenchmark
% 59.84/59.91 %-------------------------------------------
% 59.84/59.91 % File :CSE---1.7
% 59.84/59.91 % Problem :theBenchmark
% 59.84/59.91 % Transform :cnf
% 59.84/59.91 % Format :tptp:raw
% 59.84/59.91 % Command :java -jar mcs_scs.jar %d %s
% 59.84/59.91
% 59.84/59.91 % Result :Theorem 59.330000s
% 59.84/59.91 % Output :CNFRefutation 59.330000s
% 59.84/59.91 %-------------------------------------------
% 59.84/59.92 %------------------------------------------------------------------------------
% 59.84/59.92 % File : GEO579+1 : TPTP v8.2.0. Released v7.5.0.
% 59.84/59.92 % Domain : Geometry
% 59.84/59.92 % Problem : JGEX problem 41
% 59.84/59.93 % Version : [CGZ00] axioms.
% 59.84/59.93 % English :
% 59.84/59.93
% 59.84/59.93 % Refs : [CGZ00] Chou et al. (2000), A Deductive Database Approach to A
% 59.84/59.93 % : [YCG08] Ye et al. (2008), An Introduction to Java Geometry Exp
% 59.84/59.93 % : [Qua20] Quaresma (2020), Email to Geoff Sutcliffe
% 59.84/59.93 % Source : [Qua20]
% 59.84/59.93 % Names : 41.p [Qua20]
% 59.84/59.93
% 59.84/59.93 % Status : Theorem
% 59.84/59.93 % Rating : 0.25 v8.1.0, 0.31 v7.5.0
% 59.84/59.93 % Syntax : Number of formulae : 95 ( 0 unt; 0 def)
% 59.84/59.93 % Number of atoms : 293 ( 1 equ)
% 59.84/59.93 % Maximal formula atoms : 10 ( 3 avg)
% 59.84/59.93 % Number of connectives : 205 ( 7 ~; 0 |; 103 &)
% 59.84/59.93 % ( 0 <=>; 95 =>; 0 <=; 0 <~>)
% 59.84/59.93 % Maximal formula depth : 17 ( 9 avg)
% 59.84/59.93 % Maximal term depth : 1 ( 1 avg)
% 59.84/59.93 % Number of predicates : 12 ( 11 usr; 0 prp; 2-8 aty)
% 59.84/59.93 % Number of functors : 0 ( 0 usr; 0 con; --- aty)
% 59.84/59.93 % Number of variables : 529 ( 509 !; 20 ?)
% 59.84/59.93 % SPC : FOF_THM_RFO_SEQ
% 59.84/59.93
% 59.84/59.93 % Comments : Taken from JGEX [YCG08], converted by Pedro Quaresma.
% 59.84/59.93 %------------------------------------------------------------------------------
% 59.84/59.93 include('Axioms/GEO012+0.ax').
% 59.84/59.93 %------------------------------------------------------------------------------
% 59.84/59.93 fof(exemplo6GDDFULL416041,conjecture,
% 59.84/59.93 ! [A,B,C,I,Y,L,X] :
% 59.84/59.93 ( ( eqangle(I,A,A,B,I,A,A,C)
% 59.84/59.93 & eqangle(I,B,B,C,I,B,B,A)
% 59.84/59.93 & eqangle(I,C,C,A,I,C,C,B)
% 59.84/59.93 & perp(Y,I,A,C)
% 59.84/59.93 & coll(Y,A,C)
% 59.84/59.93 & perp(L,I,B,C)
% 59.84/59.93 & coll(L,B,C)
% 59.84/59.93 & perp(X,B,A,I)
% 59.84/59.93 & coll(X,A,I) )
% 59.84/59.93 => coll(X,Y,L) ) ).
% 59.84/59.93
% 59.84/59.93 %------------------------------------------------------------------------------
% 59.84/59.93 %-------------------------------------------
% 59.84/59.93 % Proof found
% 59.84/59.93 % SZS status Theorem for theBenchmark
% 59.84/59.93 % SZS output start Proof
% 59.88/59.94 %ClaNum:264(EqnAxiom:141)
% 59.88/59.94 %VarNum:1613(SingletonVarNum:590)
% 59.88/59.94 %MaxLitNum:5
% 59.88/59.94 %MaxfuncDepth:1
% 59.88/59.94 %SharedTerms:17
% 59.88/59.94 %goalClause: 142 143 144 145 146 147 148 149 150 151
% 59.88/59.94 %singleGoalClaCount:10
% 59.88/59.94 [142]P1(a1,a2,a15)
% 59.88/59.94 [143]P1(a18,a16,a15)
% 59.88/59.94 [144]P1(a19,a2,a17)
% 59.88/59.94 [145]P3(a1,a17,a2,a15)
% 59.88/59.94 [146]P3(a18,a17,a16,a15)
% 59.88/59.94 [147]P3(a19,a16,a2,a17)
% 59.88/59.94 [148]P4(a17,a2,a2,a16,a17,a2,a2,a15)
% 59.88/59.94 [149]P4(a17,a16,a16,a15,a17,a16,a16,a2)
% 59.88/59.94 [150]P4(a17,a15,a15,a2,a17,a15,a15,a16)
% 59.88/59.94 [151]~P1(a19,a1,a18)
% 59.88/59.94 [152]~P1(x1522,x1521,x1523)+P1(x1521,x1522,x1523)
% 59.88/59.94 [153]~P1(x1531,x1533,x1532)+P1(x1531,x1532,x1533)
% 59.88/59.94 [154]~P8(x1541,x1542,x1543)+P1(x1541,x1542,x1543)
% 59.88/59.94 [155]~P8(x1551,x1553,x1552)+P8(x1551,x1552,x1553)
% 59.88/59.94 [157]~P8(x1571,x1572,x1573)+P5(x1571,x1572,x1571,x1573)
% 59.88/59.95 [161]~P10(x1611,x1612,x1611,x1613)+P1(x1611,x1612,x1613)
% 59.88/59.95 [227]~P5(x2271,x2272,x2271,x2273)+P4(x2271,x2272,x2272,x2273,x2272,x2273,x2271,x2273)
% 59.88/59.95 [164]~P10(x1643,x1644,x1641,x1642)+P10(x1641,x1642,x1643,x1644)
% 59.88/59.95 [165]~P10(x1651,x1652,x1654,x1653)+P10(x1651,x1652,x1653,x1654)
% 59.88/59.95 [166]~P3(x1663,x1664,x1661,x1662)+P3(x1661,x1662,x1663,x1664)
% 59.88/59.95 [167]~P3(x1671,x1672,x1674,x1673)+P3(x1671,x1672,x1673,x1674)
% 59.88/59.95 [168]~P5(x1683,x1684,x1681,x1682)+P5(x1681,x1682,x1683,x1684)
% 59.88/59.95 [169]~P5(x1691,x1692,x1694,x1693)+P5(x1691,x1692,x1693,x1694)
% 59.88/59.95 [170]~P6(x1702,x1701,x1703,x1704)+P6(x1701,x1702,x1703,x1704)
% 59.88/59.95 [171]~P6(x1711,x1713,x1712,x1714)+P6(x1711,x1712,x1713,x1714)
% 59.88/59.95 [172]~P6(x1721,x1722,x1724,x1723)+P6(x1721,x1722,x1723,x1724)
% 59.88/59.95 [225]~P6(x2252,x2253,x2251,x2254)+P4(x2251,x2252,x2251,x2253,x2254,x2252,x2254,x2253)
% 59.88/59.95 [188]~P2(x1884,x1881,x1882,x1883)+P3(f7(x1881,x1882,x1883,x1884),x1881,x1881,x1884)
% 59.88/59.95 [203]P5(x2031,x2032,x2033,x2034)+~P7(x2031,x2032,x2035,x2033,x2034,x2036)
% 59.88/59.95 [215]~P11(x2154,x2155,x2156,x2151,x2152,x2153)+P11(x2151,x2152,x2153,x2154,x2155,x2156)
% 59.88/59.95 [216]~P11(x2162,x2161,x2163,x2165,x2164,x2166)+P11(x2161,x2162,x2163,x2164,x2165,x2166)
% 59.88/59.95 [217]~P11(x2171,x2173,x2172,x2174,x2176,x2175)+P11(x2171,x2172,x2173,x2174,x2175,x2176)
% 59.88/59.95 [218]~P7(x2184,x2185,x2186,x2181,x2182,x2183)+P7(x2181,x2182,x2183,x2184,x2185,x2186)
% 59.88/59.95 [219]~P7(x2192,x2191,x2193,x2195,x2194,x2196)+P7(x2191,x2192,x2193,x2194,x2195,x2196)
% 59.88/59.95 [220]~P7(x2201,x2203,x2202,x2204,x2206,x2205)+P7(x2201,x2202,x2203,x2204,x2205,x2206)
% 59.88/59.95 [226]~P10(x2261,x2262,x2265,x2266)+P4(x2261,x2262,x2263,x2264,x2265,x2266,x2263,x2264)
% 59.88/59.95 [232]~P11(x2321,x2322,x2323,x2324,x2325,x2326)+P4(x2321,x2322,x2322,x2323,x2324,x2325,x2325,x2326)
% 59.88/59.95 [233]~P11(x2331,x2332,x2333,x2334,x2335,x2336)+P9(x2331,x2332,x2331,x2333,x2334,x2335,x2334,x2336)
% 59.88/59.95 [234]~P4(x2341,x2342,x2345,x2346,x2343,x2344,x2345,x2346)+P10(x2341,x2342,x2343,x2344)
% 59.88/59.95 [253]~P4(x2535,x2536,x2537,x2538,x2531,x2532,x2533,x2534)+P4(x2531,x2532,x2533,x2534,x2535,x2536,x2537,x2538)
% 59.88/59.95 [254]~P4(x2543,x2544,x2541,x2542,x2547,x2548,x2545,x2546)+P4(x2541,x2542,x2543,x2544,x2545,x2546,x2547,x2548)
% 59.88/59.95 [255]~P4(x2552,x2551,x2553,x2554,x2555,x2556,x2557,x2558)+P4(x2551,x2552,x2553,x2554,x2555,x2556,x2557,x2558)
% 59.88/59.95 [256]~P4(x2561,x2562,x2565,x2566,x2563,x2564,x2567,x2568)+P4(x2561,x2562,x2563,x2564,x2565,x2566,x2567,x2568)
% 59.88/59.95 [257]~P9(x2575,x2576,x2577,x2578,x2571,x2572,x2573,x2574)+P9(x2571,x2572,x2573,x2574,x2575,x2576,x2577,x2578)
% 59.88/59.95 [258]~P9(x2583,x2584,x2581,x2582,x2587,x2588,x2585,x2586)+P9(x2581,x2582,x2583,x2584,x2585,x2586,x2587,x2588)
% 59.88/59.95 [259]~P9(x2592,x2591,x2593,x2594,x2595,x2596,x2597,x2598)+P9(x2591,x2592,x2593,x2594,x2595,x2596,x2597,x2598)
% 59.88/59.95 [260]~P9(x2601,x2602,x2605,x2606,x2603,x2604,x2607,x2608)+P9(x2601,x2602,x2603,x2604,x2605,x2606,x2607,x2608)
% 59.88/59.95 [162]~P1(x1621,x1622,x1623)+~P5(x1621,x1622,x1621,x1623)+P8(x1621,x1622,x1623)
% 59.88/59.95 [236]P5(x2361,x2362,x2361,x2363)+~P4(x2361,x2362,x2362,x2363,x2362,x2363,x2361,x2363)+P1(x2361,x2362,x2363)
% 59.88/59.95 [177]~P3(x1771,x1772,x1772,x1773)+~P5(x1772,x1771,x1772,x1773)+P1(x1771,x1772,f3(x1771,x1773,x1772))
% 59.88/59.95 [189]~P3(x1892,x1891,x1891,x1893)+~P5(x1891,x1892,x1891,x1893)+P5(x1891,x1892,x1891,f3(x1892,x1893,x1891))
% 59.88/59.95 [156]~P1(x1563,x1564,x1561)+P1(x1561,x1562,x1563)+~P1(x1563,x1564,x1562)
% 59.88/59.95 [173]~P2(x1734,x1731,x1732,x1733)+P3(x1731,x1732,x1732,x1733)+~P1(x1734,x1731,x1733)
% 59.88/59.95 [174]~P3(x1741,x1744,x1742,x1743)+P5(x1741,x1742,x1741,x1743)+~P8(x1744,x1742,x1743)
% 59.88/59.95 [175]~P3(x1751,x1753,x1753,x1754)+P5(x1751,x1752,x1753,x1752)+~P8(x1752,x1751,x1754)
% 59.88/59.95 [182]~P5(x1821,x1824,x1822,x1824)+~P5(x1821,x1823,x1822,x1823)+P3(x1821,x1822,x1823,x1824)
% 59.88/59.95 [185]~P5(x1851,x1852,x1851,x1854)+~P5(x1851,x1852,x1851,x1853)+P2(x1851,x1852,x1853,x1854)
% 59.88/59.95 [231]~P10(x2311,x2314,x2313,x2312)+~P6(x2311,x2314,x2313,x2312)+P4(x2311,x2312,x2313,x2312,x2313,x2312,x2313,x2314)
% 59.88/59.95 [235]~P4(x2351,x2353,x2351,x2354,x2352,x2353,x2352,x2354)+P1(x2351,x2352,x2353)+P6(x2353,x2354,x2351,x2352)
% 59.88/59.95 [237]~P1(x2373,x2374,x2372)+~P4(x2373,x2371,x2373,x2372,x2374,x2371,x2374,x2372)+P6(x2371,x2372,x2373,x2374)
% 59.88/59.95 [239]P3(x2391,x2392,x2393,x2394)+~P4(x2391,x2392,x2393,x2394,x2393,x2394,x2391,x2392)+P10(x2391,x2392,x2393,x2394)
% 59.88/59.95 [178]~P3(x1781,x1784,x1782,x1783)+~P3(x1782,x1784,x1781,x1783)+P1(f4(x1781,x1782,x1783),x1783,x1782)
% 59.88/59.95 [179]~P3(x1791,x1794,x1792,x1793)+~P3(x1792,x1794,x1791,x1793)+P1(f5(x1791,x1792,x1793),x1793,x1791)
% 59.88/59.95 [190]~P3(x1901,x1904,x1902,x1903)+~P3(x1902,x1904,x1901,x1903)+P3(x1901,f4(x1901,x1902,x1903),x1903,x1902)
% 59.88/59.95 [191]~P3(x1911,x1914,x1912,x1913)+~P3(x1912,x1914,x1911,x1913)+P3(x1911,f5(x1912,x1911,x1913),x1913,x1912)
% 59.88/59.95 [192]~P3(x1921,x1923,x1923,x1922)+~P6(x1921,x1922,x1923,x1924)+P2(f8(x1921,x1922,x1923),x1921,x1922,x1923)
% 59.88/59.95 [194]~P3(x1943,x1944,x1942,x1941)+~P5(x1943,x1942,x1943,x1941)+P1(x1941,x1942,f21(x1942,x1941,x1943,x1944))
% 59.88/59.95 [195]~P3(x1953,x1954,x1951,x1952)+~P5(x1953,x1951,x1953,x1952)+P1(f21(x1951,x1952,x1953,x1954),x1953,x1954)
% 59.88/59.95 [246]~P5(x2463,x2462,x2463,x2461)+~P4(x2462,x2463,x2463,x2464,x2463,x2464,x2463,x2461)+P1(x2461,x2462,f22(x2462,x2461,x2463,x2464))
% 59.88/59.95 [247]~P3(x2473,x2474,x2472,x2471)+~P4(x2472,x2473,x2473,x2474,x2473,x2474,x2473,x2471)+P1(x2471,x2472,f23(x2472,x2471,x2473,x2474))
% 59.88/59.95 [248]~P3(x2483,x2482,x2482,x2481)+~P4(x2484,x2483,x2482,x2483,x2482,x2483,x2481,x2483)+P1(f14(x2481,x2482,x2483,x2484),x2483,x2484)
% 59.88/59.95 [249]~P3(x2493,x2492,x2492,x2491)+~P4(x2494,x2493,x2492,x2493,x2492,x2493,x2491,x2493)+P1(f14(x2491,x2492,x2493,x2494),x2491,x2492)
% 59.88/59.95 [250]~P5(x2503,x2501,x2503,x2502)+~P4(x2501,x2503,x2503,x2504,x2503,x2504,x2503,x2502)+P1(f22(x2501,x2502,x2503,x2504),x2503,x2504)
% 59.88/59.95 [251]~P3(x2513,x2514,x2511,x2512)+~P4(x2511,x2513,x2513,x2514,x2513,x2514,x2513,x2512)+P1(f23(x2511,x2512,x2513,x2514),x2513,x2514)
% 59.88/59.95 [158]~P8(x1585,x1581,x1583)+P10(x1581,x1582,x1583,x1584)+~P8(x1585,x1582,x1584)
% 59.88/59.95 [159]~P8(x1591,x1595,x1593)+P10(x1591,x1592,x1593,x1594)+~P8(x1592,x1595,x1594)
% 59.88/59.95 [186]~P6(x1865,x1861,x1862,x1863)+P6(x1861,x1862,x1863,x1864)+~P6(x1865,x1861,x1862,x1864)
% 59.88/59.95 [228]~P8(x2285,x2282,x2283)+~P2(x2284,x2281,x2282,x2283)+P4(x2281,x2282,x2281,x2283,x2284,x2282,x2284,x2285)
% 59.88/59.95 [230]~P2(x2305,x2301,x2303,x2304)+P4(x2301,x2302,x2301,x2303,x2304,x2301,x2304,x2303)+~P3(x2305,x2301,x2301,x2302)
% 59.88/59.95 [243]~P4(x2432,x2433,x2432,x2434,x2435,x2432,x2435,x2434)+P3(x2431,x2432,x2432,x2433)+~P2(x2431,x2432,x2434,x2435)
% 59.88/59.95 [198]~P1(x1982,x1984,x1985)+~P3(x1981,x1983,x1983,x1982)+P1(f12(x1981,x1982,x1983,x1984,x1985),x1984,x1985)
% 59.88/59.95 [199]~P1(x1992,x1994,x1995)+~P3(x1991,x1993,x1993,x1992)+P3(f12(x1991,x1992,x1993,x1994,x1995),x1991,x1994,x1995)
% 59.88/59.95 [200]~P3(x2003,x2004,x2004,x2001)+~P5(x2001,x2002,x2001,x2005)+P5(x2001,x2002,x2001,f26(x2003,x2004,x2002,x2005,x2001))
% 59.88/59.95 [201]~P3(x2013,x2011,x2011,x2015)+~P5(x2015,x2012,x2015,x2014)+P5(x2011,x2012,x2011,f26(x2013,x2011,x2012,x2014,x2015))
% 59.88/59.95 [202]~P3(x2021,x2022,x2022,x2025)+~P5(x2025,x2023,x2025,x2024)+P10(f26(x2021,x2022,x2023,x2024,x2025),x2023,x2021,x2022)
% 59.88/59.95 [245]~P4(x2451,x2453,x2452,x2453,x2451,x2454,x2452,x2455)+P1(x2451,x2452,x2453)+P6(x2454,x2452,x2453,f25(x2451,x2452,x2453,x2454))
% 59.88/59.95 [261]~P4(x2611,x2613,x2612,x2613,x2611,x2614,x2612,x2615)+P1(x2611,x2612,x2613)+P4(x2611,x2613,x2612,x2613,x2611,f25(x2611,x2612,x2613,x2614),x2612,f25(x2611,x2612,x2613,x2614))
% 59.88/59.95 [180]~P10(x1801,x1802,x1805,x1806)+P10(x1801,x1802,x1803,x1804)+~P10(x1805,x1806,x1803,x1804)
% 59.88/59.95 [181]~P3(x1811,x1812,x1815,x1816)+P10(x1811,x1812,x1813,x1814)+~P3(x1815,x1816,x1813,x1814)
% 59.88/59.95 [183]~P3(x1835,x1836,x1833,x1834)+P3(x1831,x1832,x1833,x1834)+~P10(x1831,x1832,x1835,x1836)
% 59.88/59.95 [184]~P5(x1841,x1842,x1845,x1846)+P5(x1841,x1842,x1843,x1844)+~P5(x1845,x1846,x1843,x1844)
% 59.88/59.95 [221]~P5(x2211,x2212,x2214,x2215)+~P11(x2211,x2212,x2213,x2214,x2215,x2216)+P7(x2211,x2212,x2213,x2214,x2215,x2216)
% 59.88/59.95 [224]~P8(x2244,x2245,x2246)+~P8(x2241,x2242,x2243)+P9(x2241,x2242,x2242,x2243,x2244,x2245,x2245,x2246)
% 59.88/59.95 [204]~P8(x2046,x2043,x2044)+~P8(x2045,x2041,x2042)+P8(f24(x2041,x2042,x2043,x2044,x2045,x2046),x2041,x2044)
% 59.88/59.95 [205]~P8(x2056,x2053,x2054)+~P8(x2055,x2051,x2052)+P10(f24(x2051,x2052,x2053,x2054,x2055,x2056),x2056,x2051,x2053)
% 59.88/59.95 [206]~P8(x2066,x2063,x2064)+~P8(x2065,x2061,x2062)+P10(f24(x2061,x2062,x2063,x2064,x2065,x2066),x2065,x2062,x2064)
% 59.88/59.95 [241]~P4(x2411,x2412,x2413,x2414,x2415,x2416,x2417,x2418)+P10(x2411,x2412,x2413,x2414)+~P10(x2415,x2416,x2417,x2418)
% 59.88/59.95 [242]~P4(x2421,x2422,x2423,x2424,x2425,x2426,x2427,x2428)+P3(x2421,x2422,x2423,x2424)+~P3(x2425,x2426,x2427,x2428)
% 59.88/59.95 [244]~P9(x2441,x2442,x2443,x2444,x2445,x2446,x2447,x2448)+P5(x2441,x2442,x2443,x2444)+~P5(x2445,x2446,x2447,x2448)
% 59.88/59.95 [222]~P11(x2221,x2222,x2223,x2227,x2228,x2229)+P11(x2221,x2222,x2223,x2224,x2225,x2226)+~P11(x2227,x2228,x2229,x2224,x2225,x2226)
% 59.88/59.95 [223]~P7(x2231,x2232,x2233,x2237,x2238,x2239)+P7(x2231,x2232,x2233,x2234,x2235,x2236)+~P7(x2237,x2238,x2239,x2234,x2235,x2236)
% 59.88/59.95 [263]~P4(x2631,x2632,x2633,x2634,x2639,x26310,x26311,x26312)+P4(x2631,x2632,x2633,x2634,x2635,x2636,x2637,x2638)+~P4(x2639,x26310,x26311,x26312,x2635,x2636,x2637,x2638)
% 59.88/59.95 [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.95 [196]~P5(x1962,x1961,x1964,x1961)+~P6(x1962,x1964,x1961,x1963)+P3(x1961,x1962,x1962,x1963)+~P5(x1962,x1963,x1964,x1963)
% 59.88/59.95 [163]~P1(x1631,x1632,x1633)+~P10(x1634,x1631,x1635,x1633)+P8(x1631,x1632,x1633)+~P8(x1634,x1632,x1635)
% 59.88/59.95 [176]~P10(x1764,x1763,x1765,x1762)+~P10(x1764,x1762,x1765,x1763)+P8(x1761,x1762,x1763)+~P8(x1761,x1764,x1765)
% 59.88/59.95 [197]~P5(x1975,x1971,x1975,x1973)+~P5(x1975,x1971,x1975,x1972)+P6(x1971,x1972,x1973,x1974)+~P5(x1975,x1971,x1975,x1974)
% 59.88/59.95 [229]~P1(x2291,x2294,x2295)+~P1(x2291,x2292,x2293)+~P10(x2292,x2294,x2293,x2295)+P9(x2291,x2292,x2292,x2293,x2291,x2294,x2294,x2295)
% 59.88/59.95 [240]~P1(x2401,x2402,x2403)+~P4(x2405,x2402,x2405,x2403,x2404,x2402,x2404,x2401)+P8(x2401,x2402,x2403)+~P2(x2404,x2405,x2402,x2403)
% 59.88/59.95 [187]~P3(x1873,x1871,x1873,x1875)+~P3(x1871,x1872,x1871,x1873)+~P8(x1874,x1872,x1875)+P8(f6(x1871,x1872,x1873),x1871,x1873)
% 59.88/59.95 [193]~P6(x1931,x1932,x1933,x1935)+~P10(x1931,x1932,x1933,x1935)+~P8(x1934,x1931,x1932)+P2(f9(x1931,x1932,x1933),x1931,x1932,x1933)
% 59.88/59.95 [262]~P4(x2621,x2623,x2622,x2623,x2624,x2626,x2625,x2626)+~P4(x2621,x2622,x2622,x2623,x2624,x2625,x2625,x2626)+P1(x2621,x2622,x2623)+P11(x2621,x2622,x2623,x2624,x2625,x2626)
% 59.88/59.95 [252]~P6(x2521,x2522,x2525,x2524)+~P6(x2521,x2522,x2525,x2523)+~P4(x2525,x2521,x2525,x2522,x2526,x2523,x2526,x2524)+P5(x2521,x2522,x2523,x2524)+~P6(x2521,x2522,x2525,x2526)
% 59.88/59.95 [207]~P1(x2072,x2073,x2074)+~P1(x2071,x2074,x2076)+~P1(x2071,x2073,x2075)+~P10(x2073,x2074,x2075,x2076)+P1(x2071,x2072,f13(x2073,x2074,x2075,x2076,x2071,x2072))
% 59.88/59.95 [208]~P1(x2086,x2081,x2082)+~P1(x2085,x2082,x2084)+~P1(x2085,x2081,x2083)+~P10(x2081,x2082,x2083,x2084)+P1(f13(x2081,x2082,x2083,x2084,x2085,x2086),x2083,x2084)
% 59.88/59.95 [209]~P1(x2093,x2094,x2095)+~P8(x2096,x2091,x2092)+~P10(x2091,x2093,x2095,x2096)+~P10(x2091,x2093,x2092,x2094)+P1(f27(x2091,x2092,x2093,x2094,x2095,x2096),x2096,x2095)
% 59.88/59.95 [210]~P1(x2103,x2104,x2105)+~P8(x2106,x2101,x2102)+~P10(x2101,x2103,x2105,x2106)+~P10(x2101,x2103,x2102,x2104)+P1(f27(x2101,x2102,x2103,x2104,x2105,x2106),x2101,x2104)
% 59.88/59.95 [211]~P5(x2112,x2113,x2112,x2114)+~P5(x2111,x2113,x2111,x2116)+~P2(x2111,x2113,x2114,x2115)+E(x2111,x2112)+P1(f10(x2113,x2114,x2115,x2116,x2111,x2112),x2113,x2115)
% 59.88/59.95 [212]~P5(x2122,x2123,x2122,x2124)+~P5(x2121,x2123,x2121,x2126)+~P2(x2121,x2123,x2124,x2125)+E(x2121,x2122)+P1(f11(x2123,x2124,x2125,x2126,x2121,x2122),x2124,x2126)
% 59.88/59.95 [213]~P5(x2132,x2133,x2132,x2134)+~P5(x2131,x2133,x2131,x2136)+~P2(x2131,x2133,x2134,x2135)+E(x2131,x2132)+P5(f10(x2133,x2134,x2135,x2136,x2131,x2132),x2132,x2132,x2133)
% 59.88/59.95 [214]~P5(x2142,x2143,x2142,x2144)+~P5(x2141,x2143,x2141,x2146)+~P2(x2141,x2143,x2144,x2145)+E(x2141,x2142)+P5(f11(x2143,x2144,x2145,x2146,x2141,x2142),x2142,x2142,x2143)
% 59.88/59.95 [160]~P1(x1603,x1601,x1604)+~P1(x1605,x1601,x1604)+~P8(x1606,x1605,x1603)+~P8(x1607,x1601,x1604)+P8(f20(x1601,x1602),x1601,x1602)
% 59.88/59.95 %EqnAxiom
% 59.88/59.95 [1]E(x11,x11)
% 59.88/59.95 [2]E(x22,x21)+~E(x21,x22)
% 59.88/59.95 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 59.88/59.95 [4]~E(x41,x42)+E(f20(x41,x43),f20(x42,x43))
% 59.88/59.95 [5]~E(x51,x52)+E(f20(x53,x51),f20(x53,x52))
% 59.88/59.95 [6]~E(x61,x62)+E(f3(x61,x63,x64),f3(x62,x63,x64))
% 59.88/59.95 [7]~E(x71,x72)+E(f3(x73,x71,x74),f3(x73,x72,x74))
% 59.88/59.95 [8]~E(x81,x82)+E(f3(x83,x84,x81),f3(x83,x84,x82))
% 59.88/59.95 [9]~E(x91,x92)+E(f4(x91,x93,x94),f4(x92,x93,x94))
% 59.88/59.95 [10]~E(x101,x102)+E(f4(x103,x101,x104),f4(x103,x102,x104))
% 59.88/59.95 [11]~E(x111,x112)+E(f4(x113,x114,x111),f4(x113,x114,x112))
% 59.88/59.95 [12]~E(x121,x122)+E(f5(x121,x123,x124),f5(x122,x123,x124))
% 59.88/59.95 [13]~E(x131,x132)+E(f5(x133,x131,x134),f5(x133,x132,x134))
% 59.88/59.95 [14]~E(x141,x142)+E(f5(x143,x144,x141),f5(x143,x144,x142))
% 59.88/59.95 [15]~E(x151,x152)+E(f6(x151,x153,x154),f6(x152,x153,x154))
% 59.88/59.95 [16]~E(x161,x162)+E(f6(x163,x161,x164),f6(x163,x162,x164))
% 59.88/59.95 [17]~E(x171,x172)+E(f6(x173,x174,x171),f6(x173,x174,x172))
% 59.88/59.95 [18]~E(x181,x182)+E(f7(x181,x183,x184,x185),f7(x182,x183,x184,x185))
% 59.88/59.95 [19]~E(x191,x192)+E(f7(x193,x191,x194,x195),f7(x193,x192,x194,x195))
% 59.88/59.95 [20]~E(x201,x202)+E(f7(x203,x204,x201,x205),f7(x203,x204,x202,x205))
% 59.88/59.95 [21]~E(x211,x212)+E(f7(x213,x214,x215,x211),f7(x213,x214,x215,x212))
% 59.88/59.95 [22]~E(x221,x222)+E(f25(x221,x223,x224,x225),f25(x222,x223,x224,x225))
% 59.88/59.95 [23]~E(x231,x232)+E(f25(x233,x231,x234,x235),f25(x233,x232,x234,x235))
% 59.88/59.95 [24]~E(x241,x242)+E(f25(x243,x244,x241,x245),f25(x243,x244,x242,x245))
% 59.88/59.95 [25]~E(x251,x252)+E(f25(x253,x254,x255,x251),f25(x253,x254,x255,x252))
% 59.88/59.95 [26]~E(x261,x262)+E(f22(x261,x263,x264,x265),f22(x262,x263,x264,x265))
% 59.88/59.95 [27]~E(x271,x272)+E(f22(x273,x271,x274,x275),f22(x273,x272,x274,x275))
% 59.88/59.95 [28]~E(x281,x282)+E(f22(x283,x284,x281,x285),f22(x283,x284,x282,x285))
% 59.88/59.95 [29]~E(x291,x292)+E(f22(x293,x294,x295,x291),f22(x293,x294,x295,x292))
% 59.88/59.95 [30]~E(x301,x302)+E(f23(x301,x303,x304,x305),f23(x302,x303,x304,x305))
% 59.88/59.95 [31]~E(x311,x312)+E(f23(x313,x311,x314,x315),f23(x313,x312,x314,x315))
% 59.88/59.95 [32]~E(x321,x322)+E(f23(x323,x324,x321,x325),f23(x323,x324,x322,x325))
% 59.88/59.95 [33]~E(x331,x332)+E(f23(x333,x334,x335,x331),f23(x333,x334,x335,x332))
% 59.88/59.95 [34]~E(x341,x342)+E(f8(x341,x343,x344),f8(x342,x343,x344))
% 59.88/59.95 [35]~E(x351,x352)+E(f8(x353,x351,x354),f8(x353,x352,x354))
% 59.88/59.95 [36]~E(x361,x362)+E(f8(x363,x364,x361),f8(x363,x364,x362))
% 59.88/59.95 [37]~E(x371,x372)+E(f9(x371,x373,x374),f9(x372,x373,x374))
% 59.88/59.95 [38]~E(x381,x382)+E(f9(x383,x381,x384),f9(x383,x382,x384))
% 59.88/59.95 [39]~E(x391,x392)+E(f9(x393,x394,x391),f9(x393,x394,x392))
% 59.88/59.95 [40]~E(x401,x402)+E(f21(x401,x403,x404,x405),f21(x402,x403,x404,x405))
% 59.88/59.95 [41]~E(x411,x412)+E(f21(x413,x411,x414,x415),f21(x413,x412,x414,x415))
% 59.88/59.95 [42]~E(x421,x422)+E(f21(x423,x424,x421,x425),f21(x423,x424,x422,x425))
% 59.88/59.95 [43]~E(x431,x432)+E(f21(x433,x434,x435,x431),f21(x433,x434,x435,x432))
% 59.88/59.95 [44]~E(x441,x442)+E(f14(x441,x443,x444,x445),f14(x442,x443,x444,x445))
% 59.88/59.95 [45]~E(x451,x452)+E(f14(x453,x451,x454,x455),f14(x453,x452,x454,x455))
% 59.88/59.95 [46]~E(x461,x462)+E(f14(x463,x464,x461,x465),f14(x463,x464,x462,x465))
% 59.88/59.95 [47]~E(x471,x472)+E(f14(x473,x474,x475,x471),f14(x473,x474,x475,x472))
% 59.88/59.95 [48]~E(x481,x482)+E(f12(x481,x483,x484,x485,x486),f12(x482,x483,x484,x485,x486))
% 59.88/59.95 [49]~E(x491,x492)+E(f12(x493,x491,x494,x495,x496),f12(x493,x492,x494,x495,x496))
% 59.88/59.95 [50]~E(x501,x502)+E(f12(x503,x504,x501,x505,x506),f12(x503,x504,x502,x505,x506))
% 59.88/59.95 [51]~E(x511,x512)+E(f12(x513,x514,x515,x511,x516),f12(x513,x514,x515,x512,x516))
% 59.88/59.95 [52]~E(x521,x522)+E(f12(x523,x524,x525,x526,x521),f12(x523,x524,x525,x526,x522))
% 59.88/59.95 [53]~E(x531,x532)+E(f11(x531,x533,x534,x535,x536,x537),f11(x532,x533,x534,x535,x536,x537))
% 59.88/59.95 [54]~E(x541,x542)+E(f11(x543,x541,x544,x545,x546,x547),f11(x543,x542,x544,x545,x546,x547))
% 59.88/59.95 [55]~E(x551,x552)+E(f11(x553,x554,x551,x555,x556,x557),f11(x553,x554,x552,x555,x556,x557))
% 59.88/59.95 [56]~E(x561,x562)+E(f11(x563,x564,x565,x561,x566,x567),f11(x563,x564,x565,x562,x566,x567))
% 59.88/59.95 [57]~E(x571,x572)+E(f11(x573,x574,x575,x576,x571,x577),f11(x573,x574,x575,x576,x572,x577))
% 59.88/59.95 [58]~E(x581,x582)+E(f11(x583,x584,x585,x586,x587,x581),f11(x583,x584,x585,x586,x587,x582))
% 59.88/59.95 [59]~E(x591,x592)+E(f26(x591,x593,x594,x595,x596),f26(x592,x593,x594,x595,x596))
% 59.88/59.95 [60]~E(x601,x602)+E(f26(x603,x601,x604,x605,x606),f26(x603,x602,x604,x605,x606))
% 59.88/59.95 [61]~E(x611,x612)+E(f26(x613,x614,x611,x615,x616),f26(x613,x614,x612,x615,x616))
% 59.88/59.95 [62]~E(x621,x622)+E(f26(x623,x624,x625,x621,x626),f26(x623,x624,x625,x622,x626))
% 59.88/59.95 [63]~E(x631,x632)+E(f26(x633,x634,x635,x636,x631),f26(x633,x634,x635,x636,x632))
% 59.88/59.95 [64]~E(x641,x642)+E(f10(x641,x643,x644,x645,x646,x647),f10(x642,x643,x644,x645,x646,x647))
% 59.88/59.95 [65]~E(x651,x652)+E(f10(x653,x651,x654,x655,x656,x657),f10(x653,x652,x654,x655,x656,x657))
% 59.88/59.95 [66]~E(x661,x662)+E(f10(x663,x664,x661,x665,x666,x667),f10(x663,x664,x662,x665,x666,x667))
% 59.88/59.95 [67]~E(x671,x672)+E(f10(x673,x674,x675,x671,x676,x677),f10(x673,x674,x675,x672,x676,x677))
% 59.88/59.95 [68]~E(x681,x682)+E(f10(x683,x684,x685,x686,x681,x687),f10(x683,x684,x685,x686,x682,x687))
% 59.88/59.95 [69]~E(x691,x692)+E(f10(x693,x694,x695,x696,x697,x691),f10(x693,x694,x695,x696,x697,x692))
% 59.88/59.95 [70]~E(x701,x702)+E(f27(x701,x703,x704,x705,x706,x707),f27(x702,x703,x704,x705,x706,x707))
% 59.88/59.95 [71]~E(x711,x712)+E(f27(x713,x711,x714,x715,x716,x717),f27(x713,x712,x714,x715,x716,x717))
% 59.88/59.95 [72]~E(x721,x722)+E(f27(x723,x724,x721,x725,x726,x727),f27(x723,x724,x722,x725,x726,x727))
% 59.88/59.95 [73]~E(x731,x732)+E(f27(x733,x734,x735,x731,x736,x737),f27(x733,x734,x735,x732,x736,x737))
% 59.88/59.95 [74]~E(x741,x742)+E(f27(x743,x744,x745,x746,x741,x747),f27(x743,x744,x745,x746,x742,x747))
% 59.88/59.95 [75]~E(x751,x752)+E(f27(x753,x754,x755,x756,x757,x751),f27(x753,x754,x755,x756,x757,x752))
% 59.88/59.95 [76]~E(x761,x762)+E(f24(x761,x763,x764,x765,x766,x767),f24(x762,x763,x764,x765,x766,x767))
% 59.88/59.95 [77]~E(x771,x772)+E(f24(x773,x771,x774,x775,x776,x777),f24(x773,x772,x774,x775,x776,x777))
% 59.88/59.95 [78]~E(x781,x782)+E(f24(x783,x784,x781,x785,x786,x787),f24(x783,x784,x782,x785,x786,x787))
% 59.88/59.95 [79]~E(x791,x792)+E(f24(x793,x794,x795,x791,x796,x797),f24(x793,x794,x795,x792,x796,x797))
% 59.88/59.95 [80]~E(x801,x802)+E(f24(x803,x804,x805,x806,x801,x807),f24(x803,x804,x805,x806,x802,x807))
% 59.88/59.95 [81]~E(x811,x812)+E(f24(x813,x814,x815,x816,x817,x811),f24(x813,x814,x815,x816,x817,x812))
% 59.88/59.95 [82]~E(x821,x822)+E(f13(x821,x823,x824,x825,x826,x827),f13(x822,x823,x824,x825,x826,x827))
% 59.88/59.95 [83]~E(x831,x832)+E(f13(x833,x831,x834,x835,x836,x837),f13(x833,x832,x834,x835,x836,x837))
% 59.88/59.95 [84]~E(x841,x842)+E(f13(x843,x844,x841,x845,x846,x847),f13(x843,x844,x842,x845,x846,x847))
% 59.88/59.95 [85]~E(x851,x852)+E(f13(x853,x854,x855,x851,x856,x857),f13(x853,x854,x855,x852,x856,x857))
% 59.88/59.95 [86]~E(x861,x862)+E(f13(x863,x864,x865,x866,x861,x867),f13(x863,x864,x865,x866,x862,x867))
% 59.88/59.95 [87]~E(x871,x872)+E(f13(x873,x874,x875,x876,x877,x871),f13(x873,x874,x875,x876,x877,x872))
% 59.88/59.95 [88]P1(x882,x883,x884)+~E(x881,x882)+~P1(x881,x883,x884)
% 59.88/59.95 [89]P1(x893,x892,x894)+~E(x891,x892)+~P1(x893,x891,x894)
% 59.88/59.95 [90]P1(x903,x904,x902)+~E(x901,x902)+~P1(x903,x904,x901)
% 59.88/59.95 [91]P9(x912,x913,x914,x915,x916,x917,x918,x919)+~E(x911,x912)+~P9(x911,x913,x914,x915,x916,x917,x918,x919)
% 59.88/59.95 [92]P9(x923,x922,x924,x925,x926,x927,x928,x929)+~E(x921,x922)+~P9(x923,x921,x924,x925,x926,x927,x928,x929)
% 59.88/59.95 [93]P9(x933,x934,x932,x935,x936,x937,x938,x939)+~E(x931,x932)+~P9(x933,x934,x931,x935,x936,x937,x938,x939)
% 59.88/59.95 [94]P9(x943,x944,x945,x942,x946,x947,x948,x949)+~E(x941,x942)+~P9(x943,x944,x945,x941,x946,x947,x948,x949)
% 59.88/59.95 [95]P9(x953,x954,x955,x956,x952,x957,x958,x959)+~E(x951,x952)+~P9(x953,x954,x955,x956,x951,x957,x958,x959)
% 59.88/59.95 [96]P9(x963,x964,x965,x966,x967,x962,x968,x969)+~E(x961,x962)+~P9(x963,x964,x965,x966,x967,x961,x968,x969)
% 59.88/59.95 [97]P9(x973,x974,x975,x976,x977,x978,x972,x979)+~E(x971,x972)+~P9(x973,x974,x975,x976,x977,x978,x971,x979)
% 59.88/59.95 [98]P9(x983,x984,x985,x986,x987,x988,x989,x982)+~E(x981,x982)+~P9(x983,x984,x985,x986,x987,x988,x989,x981)
% 59.88/59.95 [99]P6(x992,x993,x994,x995)+~E(x991,x992)+~P6(x991,x993,x994,x995)
% 59.88/59.95 [100]P6(x1003,x1002,x1004,x1005)+~E(x1001,x1002)+~P6(x1003,x1001,x1004,x1005)
% 59.88/59.95 [101]P6(x1013,x1014,x1012,x1015)+~E(x1011,x1012)+~P6(x1013,x1014,x1011,x1015)
% 59.88/59.95 [102]P6(x1023,x1024,x1025,x1022)+~E(x1021,x1022)+~P6(x1023,x1024,x1025,x1021)
% 59.88/59.95 [103]P3(x1032,x1033,x1034,x1035)+~E(x1031,x1032)+~P3(x1031,x1033,x1034,x1035)
% 59.88/59.95 [104]P3(x1043,x1042,x1044,x1045)+~E(x1041,x1042)+~P3(x1043,x1041,x1044,x1045)
% 59.88/59.95 [105]P3(x1053,x1054,x1052,x1055)+~E(x1051,x1052)+~P3(x1053,x1054,x1051,x1055)
% 59.88/59.95 [106]P3(x1063,x1064,x1065,x1062)+~E(x1061,x1062)+~P3(x1063,x1064,x1065,x1061)
% 59.88/59.95 [107]P11(x1072,x1073,x1074,x1075,x1076,x1077)+~E(x1071,x1072)+~P11(x1071,x1073,x1074,x1075,x1076,x1077)
% 59.88/59.95 [108]P11(x1083,x1082,x1084,x1085,x1086,x1087)+~E(x1081,x1082)+~P11(x1083,x1081,x1084,x1085,x1086,x1087)
% 59.88/59.95 [109]P11(x1093,x1094,x1092,x1095,x1096,x1097)+~E(x1091,x1092)+~P11(x1093,x1094,x1091,x1095,x1096,x1097)
% 59.88/59.95 [110]P11(x1103,x1104,x1105,x1102,x1106,x1107)+~E(x1101,x1102)+~P11(x1103,x1104,x1105,x1101,x1106,x1107)
% 59.88/59.95 [111]P11(x1113,x1114,x1115,x1116,x1112,x1117)+~E(x1111,x1112)+~P11(x1113,x1114,x1115,x1116,x1111,x1117)
% 59.88/59.95 [112]P11(x1123,x1124,x1125,x1126,x1127,x1122)+~E(x1121,x1122)+~P11(x1123,x1124,x1125,x1126,x1127,x1121)
% 59.88/59.95 [113]P4(x1132,x1133,x1134,x1135,x1136,x1137,x1138,x1139)+~E(x1131,x1132)+~P4(x1131,x1133,x1134,x1135,x1136,x1137,x1138,x1139)
% 59.88/59.95 [114]P4(x1143,x1142,x1144,x1145,x1146,x1147,x1148,x1149)+~E(x1141,x1142)+~P4(x1143,x1141,x1144,x1145,x1146,x1147,x1148,x1149)
% 59.88/59.95 [115]P4(x1153,x1154,x1152,x1155,x1156,x1157,x1158,x1159)+~E(x1151,x1152)+~P4(x1153,x1154,x1151,x1155,x1156,x1157,x1158,x1159)
% 59.88/59.95 [116]P4(x1163,x1164,x1165,x1162,x1166,x1167,x1168,x1169)+~E(x1161,x1162)+~P4(x1163,x1164,x1165,x1161,x1166,x1167,x1168,x1169)
% 59.88/59.95 [117]P4(x1173,x1174,x1175,x1176,x1172,x1177,x1178,x1179)+~E(x1171,x1172)+~P4(x1173,x1174,x1175,x1176,x1171,x1177,x1178,x1179)
% 59.88/59.95 [118]P4(x1183,x1184,x1185,x1186,x1187,x1182,x1188,x1189)+~E(x1181,x1182)+~P4(x1183,x1184,x1185,x1186,x1187,x1181,x1188,x1189)
% 59.88/59.95 [119]P4(x1193,x1194,x1195,x1196,x1197,x1198,x1192,x1199)+~E(x1191,x1192)+~P4(x1193,x1194,x1195,x1196,x1197,x1198,x1191,x1199)
% 59.88/59.95 [120]P4(x1203,x1204,x1205,x1206,x1207,x1208,x1209,x1202)+~E(x1201,x1202)+~P4(x1203,x1204,x1205,x1206,x1207,x1208,x1209,x1201)
% 59.88/59.95 [121]P5(x1212,x1213,x1214,x1215)+~E(x1211,x1212)+~P5(x1211,x1213,x1214,x1215)
% 59.88/59.95 [122]P5(x1223,x1222,x1224,x1225)+~E(x1221,x1222)+~P5(x1223,x1221,x1224,x1225)
% 59.88/59.95 [123]P5(x1233,x1234,x1232,x1235)+~E(x1231,x1232)+~P5(x1233,x1234,x1231,x1235)
% 59.88/59.95 [124]P5(x1243,x1244,x1245,x1242)+~E(x1241,x1242)+~P5(x1243,x1244,x1245,x1241)
% 59.88/59.95 [125]P2(x1252,x1253,x1254,x1255)+~E(x1251,x1252)+~P2(x1251,x1253,x1254,x1255)
% 59.88/59.95 [126]P2(x1263,x1262,x1264,x1265)+~E(x1261,x1262)+~P2(x1263,x1261,x1264,x1265)
% 59.88/59.95 [127]P2(x1273,x1274,x1272,x1275)+~E(x1271,x1272)+~P2(x1273,x1274,x1271,x1275)
% 59.88/59.95 [128]P2(x1283,x1284,x1285,x1282)+~E(x1281,x1282)+~P2(x1283,x1284,x1285,x1281)
% 59.88/59.95 [129]P10(x1292,x1293,x1294,x1295)+~E(x1291,x1292)+~P10(x1291,x1293,x1294,x1295)
% 59.88/59.95 [130]P10(x1303,x1302,x1304,x1305)+~E(x1301,x1302)+~P10(x1303,x1301,x1304,x1305)
% 59.88/59.95 [131]P10(x1313,x1314,x1312,x1315)+~E(x1311,x1312)+~P10(x1313,x1314,x1311,x1315)
% 59.88/59.95 [132]P10(x1323,x1324,x1325,x1322)+~E(x1321,x1322)+~P10(x1323,x1324,x1325,x1321)
% 59.88/59.95 [133]P7(x1332,x1333,x1334,x1335,x1336,x1337)+~E(x1331,x1332)+~P7(x1331,x1333,x1334,x1335,x1336,x1337)
% 59.88/59.95 [134]P7(x1343,x1342,x1344,x1345,x1346,x1347)+~E(x1341,x1342)+~P7(x1343,x1341,x1344,x1345,x1346,x1347)
% 59.88/59.95 [135]P7(x1353,x1354,x1352,x1355,x1356,x1357)+~E(x1351,x1352)+~P7(x1353,x1354,x1351,x1355,x1356,x1357)
% 59.88/59.95 [136]P7(x1363,x1364,x1365,x1362,x1366,x1367)+~E(x1361,x1362)+~P7(x1363,x1364,x1365,x1361,x1366,x1367)
% 59.88/59.95 [137]P7(x1373,x1374,x1375,x1376,x1372,x1377)+~E(x1371,x1372)+~P7(x1373,x1374,x1375,x1376,x1371,x1377)
% 59.88/59.95 [138]P7(x1383,x1384,x1385,x1386,x1387,x1382)+~E(x1381,x1382)+~P7(x1383,x1384,x1385,x1386,x1387,x1381)
% 59.88/59.95 [139]P8(x1392,x1393,x1394)+~E(x1391,x1392)+~P8(x1391,x1393,x1394)
% 59.88/59.95 [140]P8(x1403,x1402,x1404)+~E(x1401,x1402)+~P8(x1403,x1401,x1404)
% 59.88/59.95 [141]P8(x1413,x1414,x1412)+~E(x1411,x1412)+~P8(x1413,x1414,x1411)
% 59.88/59.95
% 59.88/59.95 %-------------------------------------------
% 59.88/59.96 cnf(265,plain,
% 59.88/59.96 (~P1(a1,a19,a18)),
% 59.88/59.96 inference(scs_inference,[],[151,152])).
% 59.88/59.96 cnf(267,plain,
% 59.88/59.96 (~P1(a19,a18,a1)),
% 59.88/59.96 inference(scs_inference,[],[151,152,153])).
% 59.88/59.96 cnf(271,plain,
% 59.88/59.96 (~P10(a19,a1,a19,a18)),
% 59.88/59.96 inference(scs_inference,[],[151,152,153,154,161])).
% 59.88/59.96 cnf(273,plain,
% 59.88/59.96 (~P8(a19,a18,a1)),
% 59.88/59.96 inference(scs_inference,[],[151,152,153,154,161,155])).
% 59.88/59.96 cnf(275,plain,
% 59.88/59.96 (~P10(a19,a18,a19,a1)),
% 59.88/59.96 inference(scs_inference,[],[151,152,153,154,161,155,164])).
% 59.88/59.96 cnf(277,plain,
% 59.88/59.96 (~P10(a19,a1,a18,a19)),
% 59.88/59.96 inference(scs_inference,[],[151,152,153,154,161,155,164,165])).
% 59.88/59.96 cnf(281,plain,
% 59.88/59.96 (P1(a15,a15,a1)),
% 59.88/59.96 inference(scs_inference,[],[142,151,152,153,154,161,155,164,165,234,156])).
% 59.88/59.96 cnf(283,plain,
% 59.88/59.96 (~P4(a19,a18,x2831,x2832,a19,a1,x2831,x2832)),
% 59.88/59.96 inference(scs_inference,[],[142,151,152,153,154,161,155,164,165,234,156,253])).
% 59.88/59.96 cnf(285,plain,
% 59.88/59.96 (~P4(x2851,x2852,a19,a1,x2851,x2852,a19,a18)),
% 59.88/59.96 inference(scs_inference,[],[142,151,152,153,154,161,155,164,165,234,156,253,254])).
% 59.88/59.96 cnf(287,plain,
% 59.88/59.96 (~P4(a1,a19,x2871,x2872,a19,a18,x2871,x2872)),
% 59.88/59.96 inference(scs_inference,[],[142,151,152,153,154,161,155,164,165,234,156,253,254,255])).
% 59.88/59.96 cnf(289,plain,
% 59.88/59.96 (~P4(a19,a1,a19,a18,x2891,x2892,x2891,x2892)),
% 59.88/59.96 inference(scs_inference,[],[142,151,152,153,154,161,155,164,165,234,156,253,254,255,256])).
% 59.88/59.96 cnf(291,plain,
% 59.88/59.96 (~P10(a1,a19,a19,a18)),
% 59.88/59.96 inference(scs_inference,[],[142,151,152,153,154,161,155,164,165,234,156,253,254,255,256,226])).
% 59.88/59.96 cnf(293,plain,
% 59.88/59.96 (~P11(x2931,a19,a1,x2931,a19,a18)),
% 59.88/59.96 inference(scs_inference,[],[142,151,152,153,154,161,155,164,165,234,156,253,254,255,256,226,232])).
% 59.88/59.96 cnf(312,plain,
% 59.88/59.96 (~P11(x3121,a19,a18,x3121,a19,a1)),
% 59.88/59.96 inference(scs_inference,[],[293,215])).
% 59.88/59.96 cnf(314,plain,
% 59.88/59.96 (~P11(x3141,a1,a19,x3141,a18,a19)),
% 59.88/59.96 inference(scs_inference,[],[293,215,217])).
% 59.88/59.96 cnf(316,plain,
% 59.88/59.96 (~P4(a19,a18,a19,a1,x3161,x3162,x3161,x3162)),
% 59.88/59.96 inference(scs_inference,[],[283,293,215,217,256])).
% 59.88/59.96 cnf(318,plain,
% 59.88/59.96 (~P1(a1,a18,a19)),
% 59.88/59.96 inference(scs_inference,[],[265,283,293,215,217,256,153])).
% 59.88/59.96 cnf(320,plain,
% 59.88/59.96 (~P10(a19,a18,a1,a19)),
% 59.88/59.96 inference(scs_inference,[],[265,283,275,293,215,217,256,153,165])).
% 59.88/59.96 cnf(322,plain,
% 59.88/59.96 (~P10(a18,a19,a19,a1)),
% 59.88/59.96 inference(scs_inference,[],[265,283,275,293,277,215,217,256,153,165,164])).
% 59.88/59.96 cnf(324,plain,
% 59.88/59.96 (~P11(a19,x3241,a1,a19,x3241,a18)),
% 59.88/59.96 inference(scs_inference,[],[265,283,275,293,277,215,217,256,153,165,164,216])).
% 59.88/59.96 cnf(326,plain,
% 59.88/59.96 (~P10(a1,a19,a1,a18)),
% 59.88/59.96 inference(scs_inference,[],[265,283,275,293,277,215,217,256,153,165,164,216,161])).
% 59.88/59.96 cnf(330,plain,
% 59.88/59.96 (~P1(a18,a19,a1)),
% 59.88/59.96 inference(scs_inference,[],[265,283,267,275,293,277,215,217,256,153,165,164,216,161,154,152])).
% 59.88/59.96 cnf(334,plain,
% 59.88/59.96 (~P4(x3341,x3342,a1,a19,x3341,x3342,a19,a18)),
% 59.88/59.96 inference(scs_inference,[],[265,283,285,287,267,275,293,277,215,217,256,153,165,164,216,161,154,152,253,254])).
% 59.88/59.96 cnf(336,plain,
% 59.88/59.96 (~P4(a18,a19,x3361,x3362,a19,a1,x3361,x3362)),
% 59.88/59.96 inference(scs_inference,[],[265,283,285,287,267,275,293,277,215,217,256,153,165,164,216,161,154,152,253,254,255])).
% 59.88/59.96 cnf(340,plain,
% 59.88/59.96 (P1(a15,a15,a18)),
% 59.88/59.96 inference(scs_inference,[],[143,265,283,285,287,267,275,293,277,215,217,256,153,165,164,216,161,154,152,253,254,255,234,156])).
% 59.88/59.96 cnf(348,plain,
% 59.88/59.96 (~P11(x3481,a18,a19,x3481,a1,a19)),
% 59.88/59.96 inference(scs_inference,[],[312,217])).
% 59.88/59.96 cnf(350,plain,
% 59.88/59.96 (~P11(a19,x3501,a18,a19,x3501,a1)),
% 59.88/59.96 inference(scs_inference,[],[312,217,216])).
% 59.88/59.96 cnf(352,plain,
% 59.88/59.96 (~P10(a1,a19,a18,a1)),
% 59.88/59.96 inference(scs_inference,[],[326,312,217,216,165])).
% 59.88/59.96 cnf(354,plain,
% 59.88/59.96 (~P10(a1,a18,a1,a19)),
% 59.88/59.96 inference(scs_inference,[],[326,312,217,216,165,164])).
% 59.88/59.96 cnf(356,plain,
% 59.88/59.96 (~P1(a18,a1,a19)),
% 59.88/59.96 inference(scs_inference,[],[330,326,312,217,216,165,164,153])).
% 59.88/59.96 cnf(358,plain,
% 59.88/59.96 (~P4(x3581,x3582,x3581,x3582,a19,a1,a19,a18)),
% 59.88/59.96 inference(scs_inference,[],[330,285,326,312,217,216,165,164,153,256])).
% 59.88/59.96 cnf(360,plain,
% 59.88/59.96 (~P4(a1,a19,a19,a18,x3601,x3602,x3601,x3602)),
% 59.88/59.96 inference(scs_inference,[],[330,289,285,326,312,217,216,165,164,153,256,255])).
% 59.88/59.96 cnf(364,plain,
% 59.88/59.96 (~P4(a1,a19,x3641,x3642,a1,a18,x3641,x3642)),
% 59.88/59.96 inference(scs_inference,[],[330,289,285,326,312,217,216,165,164,153,256,255,154,234])).
% 59.88/59.96 cnf(366,plain,
% 59.88/59.96 (~P10(a18,a19,a18,a1)),
% 59.88/59.96 inference(scs_inference,[],[330,289,285,326,312,217,216,165,164,153,256,255,154,234,161])).
% 59.88/59.96 cnf(368,plain,
% 59.88/59.96 (~P4(a19,a18,x3681,x3682,a1,a19,x3681,x3682)),
% 59.88/59.96 inference(scs_inference,[],[330,289,285,287,326,312,217,216,165,164,153,256,255,154,234,161,253])).
% 59.88/59.96 cnf(370,plain,
% 59.88/59.96 (~P4(x3701,x3702,a18,a19,x3701,x3702,a19,a1)),
% 59.88/59.96 inference(scs_inference,[],[330,289,285,287,336,326,312,217,216,165,164,153,256,255,154,234,161,253,254])).
% 59.88/59.96 cnf(372,plain,
% 59.88/59.96 (P1(a17,a17,a19)),
% 59.88/59.96 inference(scs_inference,[],[144,330,289,285,287,336,326,312,217,216,165,164,153,256,255,154,234,161,253,254,156])).
% 59.88/59.96 cnf(374,plain,
% 59.88/59.96 (~P11(a1,a19,a18,x3741,x3741,x3741)),
% 59.88/59.96 inference(scs_inference,[],[144,330,289,285,287,336,326,312,217,216,165,164,153,256,255,154,234,161,253,254,156,232])).
% 59.88/59.96 cnf(376,plain,
% 59.88/59.96 (~P11(x3761,x3761,x3761,a1,a19,a18)),
% 59.88/59.96 inference(scs_inference,[],[144,330,289,285,287,336,326,312,217,216,165,164,153,256,255,154,234,161,253,254,156,232,215])).
% 59.88/59.96 cnf(392,plain,
% 59.88/59.96 (~P11(a19,a1,a18,x3921,x3921,x3921)),
% 59.88/59.96 inference(scs_inference,[],[374,216])).
% 59.88/59.96 cnf(394,plain,
% 59.88/59.96 (~P11(a1,a18,a19,x3941,x3941,x3941)),
% 59.88/59.96 inference(scs_inference,[],[374,216,217])).
% 59.88/59.96 cnf(398,plain,
% 59.88/59.96 (~P4(a18,a19,a19,a1,x3981,x3982,x3981,x3982)),
% 59.88/59.96 inference(scs_inference,[],[336,374,216,217,215,256])).
% 59.88/59.96 cnf(400,plain,
% 59.88/59.96 (~P10(a18,a1,a18,a19)),
% 59.88/59.96 inference(scs_inference,[],[336,366,374,216,217,215,256,164])).
% 59.88/59.96 cnf(402,plain,
% 59.88/59.96 (~P10(a18,a19,a1,a18)),
% 59.88/59.96 inference(scs_inference,[],[336,366,374,216,217,215,256,164,165])).
% 59.88/59.96 cnf(404,plain,
% 59.88/59.96 (~P4(x4041,x4042,a19,a1,x4042,x4041,a19,a18)),
% 59.88/59.96 inference(scs_inference,[],[336,285,366,374,216,217,215,256,164,165,255])).
% 59.88/59.96 cnf(406,plain,
% 59.88/59.96 (~P4(a18,a19,x4061,x4062,a18,a1,x4061,x4062)),
% 59.88/59.96 inference(scs_inference,[],[336,285,366,374,216,217,215,256,164,165,255,234])).
% 59.88/59.96 cnf(408,plain,
% 59.88/59.96 (~P4(x4081,x4082,x4081,x4082,a19,a18,a19,a1)),
% 59.88/59.96 inference(scs_inference,[],[316,336,285,366,374,216,217,215,256,164,165,255,234,253])).
% 59.88/59.96 cnf(410,plain,
% 59.88/59.96 (~P4(a19,a18,a1,a19,x4101,x4102,x4101,x4102)),
% 59.88/59.96 inference(scs_inference,[],[316,336,285,360,366,374,216,217,215,256,164,165,255,234,253,254])).
% 59.88/59.96 cnf(414,plain,
% 59.88/59.96 (~P11(a18,a19,a1,x4141,x4141,x4141)),
% 59.88/59.96 inference(scs_inference,[],[316,336,285,281,360,366,374,216,217,215,256,164,165,255,234,253,254,156,232])).
% 59.88/59.96 cnf(425,plain,
% 59.88/59.96 (~P4(x4251,x4252,x4252,x4251,a19,a1,a19,a18)),
% 59.88/59.96 inference(scs_inference,[],[358,376,217,255])).
% 59.88/59.96 cnf(427,plain,
% 59.88/59.96 (~P10(a18,a1,a1,a19)),
% 59.88/59.96 inference(scs_inference,[],[358,376,352,217,255,164])).
% 59.88/59.96 cnf(429,plain,
% 59.88/59.96 (~P11(a18,a1,a19,x4291,x4291,x4291)),
% 59.88/59.96 inference(scs_inference,[],[358,376,394,352,217,255,164,216])).
% 59.88/59.96 cnf(431,plain,
% 59.88/59.96 (~P10(a1,a19,a18,a19)),
% 59.88/59.96 inference(scs_inference,[],[358,291,376,394,352,217,255,164,216,165])).
% 59.88/59.96 cnf(433,plain,
% 59.88/59.96 (~P4(x4331,x4332,x4331,x4332,a1,a19,a19,a18)),
% 59.88/59.96 inference(scs_inference,[],[358,334,291,376,394,352,217,255,164,216,165,256])).
% 59.88/59.96 cnf(435,plain,
% 59.88/59.96 (~P11(x4351,x4351,x4351,a18,a19,a1)),
% 59.88/59.96 inference(scs_inference,[],[358,334,291,376,394,414,352,217,255,164,216,165,256,215])).
% 59.88/59.96 cnf(439,plain,
% 59.88/59.96 (~P4(x4391,x4392,a19,a18,x4391,x4392,a1,a19)),
% 59.88/59.96 inference(scs_inference,[],[358,334,291,354,376,394,414,352,217,255,164,216,165,256,215,234,253])).
% 59.88/59.96 cnf(441,plain,
% 59.88/59.96 (~P4(a19,a1,a18,a19,x4411,x4412,x4411,x4412)),
% 59.88/59.96 inference(scs_inference,[],[358,334,398,291,354,376,394,414,352,217,255,164,216,165,256,215,234,253,254])).
% 59.88/59.96 cnf(452,plain,
% 59.88/59.96 (~P4(a18,a19,x4521,x4522,a1,a19,x4521,x4522)),
% 59.88/59.96 inference(scs_inference,[],[368,255])).
% 59.88/59.96 cnf(454,plain,
% 59.88/59.96 (~P10(a18,a19,a1,a19)),
% 59.88/59.96 inference(scs_inference,[],[368,322,255,165])).
% 59.88/59.96 cnf(460,plain,
% 59.88/59.96 (~P4(x4601,x4602,x4601,x4602,a18,a19,a19,a1)),
% 59.88/59.96 inference(scs_inference,[],[368,370,322,392,429,255,165,215,217,256])).
% 59.88/59.96 cnf(464,plain,
% 59.88/59.96 (~P10(a1,a18,a18,a19)),
% 59.88/59.96 inference(scs_inference,[],[368,370,322,402,392,429,435,255,165,215,217,256,216,164])).
% 59.88/59.96 cnf(466,plain,
% 59.88/59.96 (~P4(x4661,x4662,x4661,x4662,a19,a18,a1,a19)),
% 59.88/59.96 inference(scs_inference,[],[368,410,370,322,402,392,429,435,255,165,215,217,256,216,164,253])).
% 59.88/59.96 cnf(470,plain,
% 59.88/59.96 (~P4(a19,a1,x4701,x4702,a19,a18,x4702,x4701)),
% 59.88/59.96 inference(scs_inference,[],[368,410,370,404,322,400,402,392,429,435,255,165,215,217,256,216,164,253,234,254])).
% 59.88/59.96 cnf(472,plain,
% 59.88/59.96 (P1(a19,a19,a17)),
% 59.88/59.96 inference(scs_inference,[],[368,410,372,370,404,322,400,402,392,429,435,255,165,215,217,256,216,164,253,234,254,156])).
% 59.88/59.96 cnf(474,plain,
% 59.88/59.96 (~P11(a18,a19,x4741,a1,a19,x4741)),
% 59.88/59.96 inference(scs_inference,[],[368,410,372,370,404,322,400,402,392,429,435,255,165,215,217,256,216,164,253,234,254,156,232])).
% 59.88/59.96 cnf(477,plain,
% 59.88/59.96 (~P10(x4771,x4772,x4773,x4774)+~P4(a19,a1,a19,a18,x4771,x4772,x4773,x4774)),
% 59.88/59.96 inference(scs_inference,[],[148,368,410,271,372,370,404,322,400,402,392,429,435,255,165,215,217,256,216,164,253,234,254,156,232,120,241])).
% 59.88/59.96 cnf(489,plain,
% 59.88/59.96 (~P10(a18,a1,a19,a1)),
% 59.88/59.96 inference(scs_inference,[],[427,165])).
% 59.88/59.96 cnf(491,plain,
% 59.88/59.96 (~P4(a18,a19,a1,a19,x4911,x4912,x4911,x4912)),
% 59.88/59.96 inference(scs_inference,[],[452,427,165,256])).
% 59.88/59.96 cnf(495,plain,
% 59.88/59.96 (~P10(a19,a1,a18,a1)),
% 59.88/59.96 inference(scs_inference,[],[452,314,427,165,256,216,164])).
% 59.88/59.96 cnf(497,plain,
% 59.88/59.96 (~P4(x4971,x4972,x4972,x4971,a19,a18,a19,a1)),
% 59.88/59.96 inference(scs_inference,[],[408,452,314,427,165,256,216,164,255])).
% 59.88/59.96 cnf(501,plain,
% 59.88/59.96 (~P11(a19,a1,a18,a19,a18,a1)),
% 59.88/59.96 inference(scs_inference,[],[408,452,470,314,324,427,165,256,216,164,255,217,232])).
% 59.88/59.96 cnf(506,plain,
% 59.88/59.96 (~P4(a18,a1,x5061,x5062,a1,a19,x5061,x5062)),
% 59.88/59.96 inference(scs_inference,[],[408,452,470,314,324,474,427,165,256,216,164,255,217,232,215,234])).
% 59.88/59.96 cnf(508,plain,
% 59.88/59.96 (~P4(a19,a1,a19,a18,x5081,x5082,x5082,x5081)),
% 59.88/59.96 inference(scs_inference,[],[408,425,452,470,314,324,474,427,165,256,216,164,255,217,232,215,234,253])).
% 59.88/59.96 cnf(510,plain,
% 59.88/59.96 (~P4(x5101,x5102,a18,a19,x5101,x5102,a1,a19)),
% 59.88/59.96 inference(scs_inference,[],[408,425,452,470,314,324,474,427,165,256,216,164,255,217,232,215,234,253,254])).
% 59.88/59.96 cnf(526,plain,
% 59.88/59.96 (~P4(x5261,x5262,x5262,x5261,a1,a19,a19,a18)),
% 59.88/59.96 inference(scs_inference,[],[433,497,256,255])).
% 59.88/59.96 cnf(530,plain,
% 59.88/59.96 (~P10(a1,a18,a19,a18)),
% 59.88/59.96 inference(scs_inference,[],[433,497,464,350,256,255,217,165])).
% 59.88/59.96 cnf(532,plain,
% 59.88/59.96 (~P10(a19,a18,a1,a18)),
% 59.88/59.96 inference(scs_inference,[],[433,497,464,350,256,255,217,165,164])).
% 59.88/59.96 cnf(536,plain,
% 59.88/59.96 (~P11(a19,a18,a1,a19,a1,a18)),
% 59.88/59.96 inference(scs_inference,[],[433,497,464,348,350,501,256,255,217,165,164,216,215])).
% 59.88/59.96 cnf(540,plain,
% 59.88/59.96 (~P4(x5401,x5402,x5401,x5402,a19,a1,a18,a19)),
% 59.88/59.96 inference(scs_inference,[],[433,441,497,431,464,348,350,501,256,255,217,165,164,216,215,234,253])).
% 59.88/59.97 cnf(542,plain,
% 59.88/59.97 (~P4(a1,a19,a18,a19,x5421,x5422,x5421,x5422)),
% 59.88/59.97 inference(scs_inference,[],[433,441,491,497,431,464,348,350,501,256,255,217,165,164,216,215,234,253,254])).
% 59.88/59.97 cnf(544,plain,
% 59.88/59.97 (~P11(x5441,x5442,x5441,a1,a19,a18)),
% 59.88/59.97 inference(scs_inference,[],[433,441,491,497,431,464,348,350,501,256,255,217,165,164,216,215,234,253,254,232])).
% 59.88/59.97 cnf(550,plain,
% 59.88/59.97 (~P4(x5501,x5502,x5502,x5501,a18,a19,a19,a1)),
% 59.88/59.97 inference(scs_inference,[],[460,255])).
% 59.88/59.97 cnf(552,plain,
% 59.88/59.97 (~P4(x5521,x5522,x5521,x5522,a18,a19,a1,a19)),
% 59.88/59.97 inference(scs_inference,[],[460,510,255,256])).
% 59.88/59.97 cnf(554,plain,
% 59.88/59.97 (~P11(x5541,x5542,x5542,a19,a1,a18)),
% 59.88/59.97 inference(scs_inference,[],[460,510,544,255,256,216])).
% 59.88/59.97 cnf(556,plain,
% 59.88/59.97 (~P10(a19,a1,a1,a18)),
% 59.88/59.97 inference(scs_inference,[],[460,510,495,544,255,256,216,165])).
% 59.88/59.97 cnf(558,plain,
% 59.88/59.97 (~P11(x5581,x5581,x5582,a1,a18,a19)),
% 59.88/59.97 inference(scs_inference,[],[460,510,495,544,255,256,216,165,217])).
% 59.88/59.97 cnf(560,plain,
% 59.88/59.97 (~P11(x5601,x5602,x5601,a18,a19,a1)),
% 59.88/59.97 inference(scs_inference,[],[460,510,495,544,255,256,216,165,217,232])).
% 59.88/59.97 cnf(562,plain,
% 59.88/59.97 (~P11(a1,a19,a18,x5621,x5622,x5621)),
% 59.88/59.97 inference(scs_inference,[],[460,510,495,544,255,256,216,165,217,232,215])).
% 59.88/59.97 cnf(564,plain,
% 59.88/59.97 (~P4(a18,a1,x5641,x5642,a19,a1,x5641,x5642)),
% 59.88/59.97 inference(scs_inference,[],[460,510,489,495,544,255,256,216,165,217,232,215,234])).
% 59.88/59.97 cnf(566,plain,
% 59.88/59.97 (~P4(a19,a18,x5661,x5662,a19,a1,x5662,x5661)),
% 59.88/59.97 inference(scs_inference,[],[460,470,510,489,495,544,255,256,216,165,217,232,215,234,253])).
% 59.88/59.97 cnf(570,plain,
% 59.88/59.97 (~P10(a1,a18,a19,a1)),
% 59.88/59.97 inference(scs_inference,[],[460,508,470,510,489,495,544,255,256,216,165,217,232,215,234,253,254,164])).
% 59.88/59.97 cnf(577,plain,
% 59.88/59.97 (~P4(x5771,x5772,x5773,x5774,a17,a16,a16,a15)+P4(x5771,x5772,x5773,x5774,a17,a16,a16,a2)),
% 59.88/59.97 inference(scs_inference,[],[145,149,408,460,508,470,510,489,495,544,255,256,216,165,217,232,215,234,253,254,164,106,114,228,263])).
% 59.88/59.97 cnf(580,plain,
% 59.88/59.97 (~P3(x5801,x5802,a19,a16)+P10(x5801,x5802,a2,a17)),
% 59.88/59.97 inference(scs_inference,[],[142,145,147,149,408,460,508,470,510,489,495,544,255,256,216,165,217,232,215,234,253,254,164,106,114,228,263,89,181])).
% 59.88/59.97 cnf(585,plain,
% 59.88/59.97 (~P4(x5851,x5852,a1,a19,x5852,x5851,a19,a18)),
% 59.88/59.97 inference(scs_inference,[],[526,256])).
% 59.88/59.97 cnf(587,plain,
% 59.88/59.97 (~P4(x5871,x5872,x5872,x5871,a19,a18,a1,a19)),
% 59.88/59.97 inference(scs_inference,[],[466,526,256,255])).
% 59.88/59.97 cnf(589,plain,
% 59.88/59.97 (~P11(x5891,x5892,x5892,a19,a18,a1)),
% 59.88/59.97 inference(scs_inference,[],[466,526,554,256,255,217])).
% 59.88/59.97 cnf(591,plain,
% 59.88/59.97 (~P10(a19,a18,a18,a1)),
% 59.88/59.97 inference(scs_inference,[],[466,526,532,554,256,255,217,165])).
% 59.88/59.97 cnf(593,plain,
% 59.88/59.97 (~P11(a18,a1,x5931,a19,a1,x5931)),
% 59.88/59.97 inference(scs_inference,[],[466,526,532,564,554,256,255,217,165,232])).
% 59.88/59.97 cnf(600,plain,
% 59.88/59.97 (~P10(a18,a1,a19,a18)),
% 59.88/59.97 inference(scs_inference,[],[466,526,532,564,554,558,256,255,217,165,232,215,216,164])).
% 59.88/59.97 cnf(602,plain,
% 59.88/59.97 (~P4(a1,a19,a19,a18,x6021,x6022,x6022,x6021)),
% 59.88/59.97 inference(scs_inference,[],[466,526,532,564,554,558,256,255,217,165,232,215,216,164,253])).
% 59.88/59.97 cnf(604,plain,
% 59.88/59.97 (~P4(a1,a18,x6041,x6042,a19,a18,x6041,x6042)),
% 59.88/59.97 inference(scs_inference,[],[466,526,530,532,564,554,558,256,255,217,165,232,215,216,164,253,234])).
% 59.88/59.97 cnf(606,plain,
% 59.88/59.97 (~P4(x6061,x6062,x6062,x6061,a19,a1,a18,a19)),
% 59.88/59.97 inference(scs_inference,[],[466,526,550,530,532,564,554,558,256,255,217,165,232,215,216,164,253,234,254])).
% 59.88/59.97 cnf(614,plain,
% 59.88/59.97 (~P4(a1,a19,x6141,x6142,a19,a18,x6142,x6141)),
% 59.88/59.97 inference(scs_inference,[],[470,255])).
% 59.88/59.97 cnf(616,plain,
% 59.88/59.97 (~P4(x6161,x6162,a19,a1,x6161,x6162,a18,a19)),
% 59.88/59.97 inference(scs_inference,[],[470,540,255,256])).
% 59.88/59.97 cnf(618,plain,
% 59.88/59.97 (~P11(a18,a19,a1,a1,a19,a18)),
% 59.88/59.97 inference(scs_inference,[],[470,540,536,255,256,216])).
% 59.88/59.97 cnf(620,plain,
% 59.88/59.97 (~P11(a1,a18,x6201,a19,a18,x6201)),
% 59.88/59.97 inference(scs_inference,[],[470,540,536,604,255,256,216,232])).
% 59.88/59.97 cnf(623,plain,
% 59.88/59.97 (~P11(a18,a19,a1,x6231,x6232,x6231)),
% 59.88/59.97 inference(scs_inference,[],[470,540,536,604,560,255,256,216,232,215])).
% 59.88/59.97 cnf(627,plain,
% 59.88/59.97 (~P4(x6271,x6272,x6271,x6272,a1,a19,a18,a19)),
% 59.88/59.97 inference(scs_inference,[],[470,540,542,536,604,560,562,255,256,216,232,215,217,253])).
% 59.88/59.97 cnf(631,plain,
% 59.88/59.97 (~P4(a19,a18,a1,a19,x6311,x6312,x6312,x6311)),
% 59.88/59.97 inference(scs_inference,[],[470,540,542,602,536,556,604,560,562,255,256,216,232,215,217,253,234,254])).
% 59.88/59.97 cnf(635,plain,
% 59.88/59.97 (~P4(a19,a18,a19,x6351,a1,a18,a1,x6351)+P6(x6351,a19,a1,a1)),
% 59.88/59.97 inference(scs_inference,[],[151,470,540,542,602,536,556,604,560,562,255,256,216,232,215,217,253,234,254,235,186])).
% 59.88/59.97 cnf(643,plain,
% 59.88/59.97 (~P4(x6431,x6432,x6432,x6431,a18,a19,a1,a19)),
% 59.88/59.97 inference(scs_inference,[],[552,550,589,256,215,255])).
% 59.88/59.97 cnf(647,plain,
% 59.88/59.97 (~P11(a1,a18,x6471,a1,a19,x6471)),
% 59.88/59.97 inference(scs_inference,[],[552,550,589,623,593,256,215,255,217,216])).
% 59.88/59.97 cnf(653,plain,
% 59.88/59.97 (~P4(x6531,x6532,a1,a19,x6531,x6532,a1,a18)),
% 59.88/59.97 inference(scs_inference,[],[552,550,364,570,589,623,593,256,215,255,217,216,253,234,254])).
% 59.88/59.97 cnf(655,plain,
% 59.88/59.97 (~P11(x6551,a1,a19,x6551,a1,a18)),
% 59.88/59.97 inference(scs_inference,[],[552,550,364,570,589,623,593,256,215,255,217,216,253,234,254,232])).
% 59.88/59.97 cnf(657,plain,
% 59.88/59.97 (~P4(x6571,x6572,x6573,x6574,a17,a15,a15,a2)+P4(x6571,x6572,x6573,x6574,a17,a15,a15,a16)),
% 59.88/59.97 inference(scs_inference,[],[150,552,550,364,570,589,623,593,256,215,255,217,216,253,234,254,232,263])).
% 59.88/59.97 cnf(671,plain,
% 59.88/59.97 (~P11(a19,a18,x6711,a1,a18,x6711)),
% 59.88/59.97 inference(scs_inference,[],[620,215])).
% 59.88/59.97 cnf(675,plain,
% 59.88/59.97 (~P11(a18,a1,x6751,a18,a19,x6751)),
% 59.88/59.97 inference(scs_inference,[],[587,620,215,256,216])).
% 59.88/59.97 cnf(677,plain,
% 59.88/59.97 (~P11(a1,x6771,a18,a19,x6771,a18)),
% 59.88/59.97 inference(scs_inference,[],[587,620,215,256,216,217])).
% 59.88/59.97 cnf(681,plain,
% 59.88/59.97 (~P4(a19,a1,a18,a19,x6811,x6812,x6812,x6811)),
% 59.88/59.97 inference(scs_inference,[],[566,587,606,620,215,256,216,217,255,253])).
% 59.88/59.97 cnf(685,plain,
% 59.88/59.97 (~P4(x6851,x6852,x6852,x6851,a1,a19,a18,a19)),
% 59.88/59.97 inference(scs_inference,[],[566,587,606,643,591,620,215,256,216,217,255,253,234,254])).
% 59.88/59.97 cnf(693,plain,
% 59.88/59.97 (~P4(x6931,x6932,a19,a1,x6932,x6931,a18,a19)),
% 59.88/59.97 inference(scs_inference,[],[606,256])).
% 59.88/59.97 cnf(695,plain,
% 59.88/59.97 (~P11(a1,a19,x6951,a1,a18,x6951)),
% 59.88/59.97 inference(scs_inference,[],[606,647,256,215])).
% 59.88/59.97 cnf(703,plain,
% 59.88/59.97 (~P4(a19,a18,x7031,x7032,a1,a19,x7032,x7031)),
% 59.88/59.97 inference(scs_inference,[],[606,614,631,647,655,256,215,255,217,216,253])).
% 59.88/59.97 cnf(707,plain,
% 59.88/59.97 (~P4(x7071,x7072,a18,a19,x7071,x7072,a18,a1)),
% 59.88/59.97 inference(scs_inference,[],[606,614,631,406,600,647,655,256,215,255,217,216,253,234,254])).
% 59.88/59.97 cnf(709,plain,
% 59.88/59.97 (~P11(x7091,a18,a19,x7091,a18,a1)),
% 59.88/59.97 inference(scs_inference,[],[606,614,631,406,600,647,655,256,215,255,217,216,253,234,254,232])).
% 59.88/59.97 cnf(715,plain,
% 59.88/59.97 (~P4(x7151,x7152,x7153,x7154,a17,a2,a2,a16)+P4(x7151,x7152,x7153,x7154,a17,a2,a2,a15)),
% 59.88/59.97 inference(scs_inference,[],[146,149,148,318,606,614,631,406,600,647,655,256,215,255,217,216,253,234,254,232,113,103,235,263])).
% 59.88/59.97 cnf(723,plain,
% 59.88/59.97 (~P11(a18,a19,x7231,a18,a1,x7231)),
% 59.88/59.97 inference(scs_inference,[],[675,215])).
% 59.88/59.97 cnf(729,plain,
% 59.88/59.97 (~P4(x7291,x7292,a1,a19,x7292,x7291,a1,a18)),
% 59.88/59.97 inference(scs_inference,[],[627,653,675,677,215,256,216,255])).
% 59.88/59.97 cnf(733,plain,
% 59.88/59.97 (~P4(x7331,x7332,a1,a18,x7331,x7332,a1,a19)),
% 59.88/59.97 inference(scs_inference,[],[627,653,671,675,677,215,256,216,255,217,253])).
% 59.88/59.97 cnf(739,plain,
% 59.88/59.97 (~P11(x7391,a1,a18,x7391,a1,a19)),
% 59.88/59.97 inference(scs_inference,[],[627,653,693,352,671,675,677,215,256,216,255,217,253,234,254,232])).
% 59.88/59.97 cnf(742,plain,
% 59.88/59.97 (~P10(x7421,x7422,x7423,x7424)+~P4(a1,a19,a1,a18,x7421,x7422,x7423,x7424)),
% 59.88/59.97 inference(scs_inference,[],[149,326,627,653,693,352,671,675,677,215,256,216,255,217,253,234,254,232,116,241])).
% 59.88/59.97 cnf(757,plain,
% 59.88/59.97 (~P11(x7571,a18,a1,x7571,a18,a19)),
% 59.88/59.97 inference(scs_inference,[],[643,709,256,215])).
% 59.88/59.97 cnf(759,plain,
% 59.88/59.97 (~P11(a1,a18,a19,a18,a1,a19)),
% 59.88/59.97 inference(scs_inference,[],[643,709,256,215,232])).
% 59.88/59.97 cnf(763,plain,
% 59.88/59.97 (~P11(a19,a1,x7631,a18,a1,x7631)),
% 59.88/59.97 inference(scs_inference,[],[643,695,709,256,215,232,217,216])).
% 59.88/59.97 cnf(765,plain,
% 59.88/59.97 (~P4(a1,a19,a18,a19,x7651,x7652,x7652,x7651)),
% 59.88/59.97 inference(scs_inference,[],[643,681,695,709,256,215,232,217,216,255])).
% 59.88/59.97 cnf(767,plain,
% 59.88/59.97 (~P4(x7671,x7672,a18,a1,x7671,x7672,a18,a19)),
% 59.88/59.97 inference(scs_inference,[],[643,681,707,695,709,256,215,232,217,216,255,253])).
% 59.88/59.97 cnf(771,plain,
% 59.88/59.97 (~P4(a1,a19,x7711,x7712,a1,a18,x7712,x7711)),
% 59.88/59.97 inference(scs_inference,[],[643,681,707,729,402,695,709,256,215,232,217,216,255,253,234,254])).
% 59.88/59.97 cnf(789,plain,
% 59.88/59.97 (~P11(a1,a19,a18,a1,a18,a19)),
% 59.88/59.97 inference(scs_inference,[],[685,703,771,723,757,618,215,256,216,255,217,232])).
% 59.88/59.97 cnf(790,plain,
% 59.88/59.97 (~P4(a1,a19,x7901,x7902,a1,a18,x7902,x7901)),
% 59.88/59.97 inference(rename_variables,[],[771])).
% 59.88/59.97 cnf(792,plain,
% 59.88/59.97 (~P4(a1,a18,x7921,x7922,a1,a19,x7922,x7921)),
% 59.88/59.97 inference(scs_inference,[],[685,703,771,790,723,757,618,215,256,216,255,217,232,253])).
% 59.88/59.97 cnf(796,plain,
% 59.88/59.97 (~P4(x7961,x7962,a18,a1,x7961,x7962,a1,a19)),
% 59.88/59.97 inference(scs_inference,[],[685,703,771,790,464,506,723,757,618,215,256,216,255,217,232,253,234,254])).
% 59.88/59.97 cnf(808,plain,
% 59.88/59.97 (~P11(x8081,a18,a1,x8081,a19,a1)),
% 59.88/59.97 inference(scs_inference,[],[765,759,739,256,215,217])).
% 59.88/59.97 cnf(815,plain,
% 59.88/59.97 (~P11(a19,a1,a18,a18,a1,a19)),
% 59.88/59.97 inference(scs_inference,[],[765,733,792,759,739,789,256,215,217,232,255,216])).
% 59.88/59.97 cnf(817,plain,
% 59.88/59.97 (~P4(x8171,x8172,a1,a19,x8171,x8172,a18,a1)),
% 59.88/59.97 inference(scs_inference,[],[765,733,792,796,759,739,789,256,215,217,232,255,216,253])).
% 59.88/59.97 cnf(821,plain,
% 59.88/59.97 (~P4(x8211,x8212,a18,a1,x8211,x8212,a19,a1)),
% 59.88/59.97 inference(scs_inference,[],[765,733,792,796,495,564,759,739,789,256,215,217,232,255,216,253,234,254])).
% 59.88/59.97 cnf(829,plain,
% 59.88/59.97 (~P10(x8291,x8292,x8293,x8294)+~P4(a18,a19,a18,a1,x8291,x8292,x8293,x8294)),
% 59.88/59.97 inference(scs_inference,[],[147,267,366,285,765,733,792,796,495,564,759,739,789,256,215,217,232,255,216,253,234,254,106,235,228,241])).
% 59.88/59.97 cnf(840,plain,
% 59.88/59.97 (~P4(a1,a19,a1,a18,x8401,x8402,x8402,x8401)),
% 59.88/59.97 inference(scs_inference,[],[771,808,215,256])).
% 59.88/59.97 cnf(842,plain,
% 59.88/59.97 (~P4(a19,a1,x8421,x8422,a1,a18,x8422,x8421)),
% 59.88/59.97 inference(scs_inference,[],[771,808,215,256,255])).
% 59.88/59.97 cnf(844,plain,
% 59.88/59.97 (~P11(a19,a1,a18,a1,a18,a1)),
% 59.88/59.97 inference(scs_inference,[],[771,808,215,256,255,232])).
% 59.88/59.97 cnf(850,plain,
% 59.88/59.97 (~P4(x8501,x8502,a19,a1,x8501,x8502,a18,a1)),
% 59.88/59.97 inference(scs_inference,[],[771,821,763,808,215,256,255,232,216,217,253])).
% 59.88/59.97 cnf(852,plain,
% 59.88/59.97 (~P4(a19,a18,x8521,x8522,a1,a18,x8521,x8522)),
% 59.88/59.97 inference(scs_inference,[],[771,821,532,763,808,215,256,255,232,216,217,253,234])).
% 59.88/59.97 cnf(854,plain,
% 59.88/59.97 (~P4(x8541,x8542,a1,a18,x8541,x8542,a19,a18)),
% 59.88/59.97 inference(scs_inference,[],[771,821,532,604,763,808,215,256,255,232,216,217,253,234,254])).
% 59.88/59.97 cnf(856,plain,
% 59.88/59.97 (~P10(x8561,x8562,x8563,x8564)+~P4(a19,a18,a1,a19,x8561,x8562,x8563,x8564)),
% 59.88/59.97 inference(scs_inference,[],[771,821,320,532,604,763,808,215,256,255,232,216,217,253,234,254,241])).
% 59.88/59.97 cnf(870,plain,
% 59.88/59.97 (~P4(a1,a18,a1,a19,x8701,x8702,x8702,x8701)),
% 59.88/59.97 inference(scs_inference,[],[792,256])).
% 59.88/59.97 cnf(872,plain,
% 59.88/59.97 (~P11(a18,a1,a19,a19,a1,a18)),
% 59.88/59.97 inference(scs_inference,[],[792,815,256,215])).
% 59.88/59.97 cnf(874,plain,
% 59.88/59.97 (~P11(a1,a19,a18,a18,a1,a1)),
% 59.88/59.97 inference(scs_inference,[],[792,815,844,256,215,216])).
% 59.88/59.97 cnf(878,plain,
% 59.88/59.97 (~P4(a18,a1,x8781,x8782,a1,a19,x8782,x8781)),
% 59.88/59.97 inference(scs_inference,[],[792,815,844,256,215,216,217,255])).
% 59.88/59.97 cnf(880,plain,
% 59.88/59.97 (~P4(x8801,x8802,x8802,x8801,a1,a19,a1,a18)),
% 59.88/59.97 inference(scs_inference,[],[792,840,815,844,256,215,216,217,255,253])).
% 59.88/59.97 cnf(882,plain,
% 59.88/59.97 (~P4(x8821,x8822,a19,a1,x8822,x8821,a1,a18)),
% 59.88/59.97 inference(scs_inference,[],[792,840,842,815,844,256,215,216,217,255,253,254])).
% 59.88/59.97 cnf(884,plain,
% 59.88/59.97 (~P11(a18,a1,a19,a1,a19,a1)),
% 59.88/59.97 inference(scs_inference,[],[792,840,842,815,844,256,215,216,217,255,253,254,232])).
% 59.88/59.97 cnf(892,plain,
% 59.88/59.97 (~P11(a18,a1,a1,a1,a19,a18)),
% 59.88/59.97 inference(scs_inference,[],[874,215])).
% 59.88/59.97 cnf(894,plain,
% 59.88/59.97 (~P4(a19,a1,a1,a18,x8941,x8942,x8942,x8941)),
% 59.88/59.97 inference(scs_inference,[],[842,874,215,256])).
% 59.88/59.97 cnf(896,plain,
% 59.88/59.97 (~P4(x8961,x8962,a18,a1,x8962,x8961,a18,a19)),
% 59.88/59.97 inference(scs_inference,[],[842,767,874,215,256,255])).
% 59.88/59.97 cnf(900,plain,
% 59.88/59.97 (~P11(a1,a18,a19,a19,a1,a1)),
% 59.88/59.97 inference(scs_inference,[],[842,767,872,874,884,215,256,255,217,216])).
% 59.88/59.97 cnf(905,plain,
% 59.88/59.97 (~P4(a1,a18,x9051,x9052,a19,a1,x9052,x9051)),
% 59.88/59.97 inference(scs_inference,[],[842,767,882,872,874,884,215,256,255,217,216,232,253])).
% 59.88/59.97 cnf(907,plain,
% 59.88/59.97 (~P4(x9071,x9072,a18,a1,x9072,x9071,a1,a19)),
% 59.88/59.97 inference(scs_inference,[],[842,767,878,882,872,874,884,215,256,255,217,216,232,253,254])).
% 59.88/59.97 cnf(916,plain,
% 59.88/59.97 (~P4(a18,a1,a1,a19,x9161,x9162,x9162,x9161)),
% 59.88/59.97 inference(scs_inference,[],[878,256])).
% 59.88/59.97 cnf(924,plain,
% 59.88/59.97 (~P4(x9241,x9242,x9241,x9242,a1,a19,a1,a18)),
% 59.88/59.97 inference(scs_inference,[],[880,878,892,900,256,215,216,217,255])).
% 59.88/59.97 cnf(926,plain,
% 59.88/59.97 (~P11(a19,a1,a18,x9261,x9262,x9261)),
% 59.88/59.97 inference(scs_inference,[],[880,878,894,892,900,256,215,216,217,255,232])).
% 59.88/59.97 cnf(928,plain,
% 59.88/59.97 (~P4(x9281,x9282,x9282,x9281,a1,a18,a1,a19)),
% 59.88/59.97 inference(scs_inference,[],[870,880,878,894,892,900,256,215,216,217,255,232,253])).
% 59.88/59.97 cnf(930,plain,
% 59.88/59.97 (~P4(a1,a18,a19,a1,x9301,x9302,x9302,x9301)),
% 59.88/59.97 inference(scs_inference,[],[870,880,878,894,892,900,256,215,216,217,255,232,253,254])).
% 59.88/59.97 cnf(934,plain,
% 59.88/59.97 (~P4(a18,a19,a18,x9341,a1,a19,a1,x9341)+P6(x9341,a18,a1,a1)),
% 59.88/59.97 inference(scs_inference,[],[356,870,880,878,894,892,900,256,215,216,217,255,232,253,254,235,99,101,186])).
% 59.88/59.97 cnf(938,plain,
% 59.88/59.97 (~P11(x9381,x9382,x9381,a19,a1,a18)),
% 59.88/59.97 inference(scs_inference,[],[926,215])).
% 59.88/59.97 cnf(940,plain,
% 59.88/59.97 (~P4(x9401,x9402,x9401,x9402,a1,a19,a18,a1)),
% 59.88/59.97 inference(scs_inference,[],[817,926,215,256])).
% 59.88/59.97 cnf(942,plain,
% 59.88/59.97 (~P4(a18,a1,x9421,x9422,a19,a1,x9422,x9421)),
% 59.88/59.97 inference(scs_inference,[],[905,817,926,215,256,255])).
% 59.88/59.97 cnf(944,plain,
% 59.88/59.97 (~P11(a1,a19,a18,x9441,x9442,x9442)),
% 59.88/59.97 inference(scs_inference,[],[905,817,926,215,256,255,216])).
% 59.88/59.97 cnf(946,plain,
% 59.88/59.97 (~P11(a19,a18,a1,x9461,x9461,x9462)),
% 59.88/59.97 inference(scs_inference,[],[905,817,926,215,256,255,216,217])).
% 59.88/59.97 cnf(951,plain,
% 59.88/59.97 (~P4(a1,a19,x9511,x9512,a18,a1,x9512,x9511)),
% 59.88/59.97 inference(scs_inference,[],[878,905,817,907,926,215,256,255,216,217,232,253])).
% 59.88/59.97 cnf(961,plain,
% 59.88/59.97 (~P4(x9611,x9612,x9611,x9612,a19,a1,a18,a1)),
% 59.88/59.97 inference(scs_inference,[],[850,256])).
% 59.88/59.97 cnf(963,plain,
% 59.88/59.97 (~P11(x9631,x9632,x9632,a1,a19,a18)),
% 59.88/59.97 inference(scs_inference,[],[850,944,256,215])).
% 59.88/59.97 cnf(965,plain,
% 59.88/59.97 (~P11(x9651,x9651,x9652,a19,a18,a1)),
% 59.88/59.97 inference(scs_inference,[],[850,938,944,256,215,217])).
% 59.88/59.97 cnf(967,plain,
% 59.88/59.97 (~P11(a18,a1,a19,x9671,x9672,x9671)),
% 59.88/59.97 inference(scs_inference,[],[916,850,938,944,256,215,217,232])).
% 59.88/59.97 cnf(971,plain,
% 59.88/59.97 (~P4(x9711,x9712,x9711,x9712,a1,a18,a1,a19)),
% 59.88/59.97 inference(scs_inference,[],[916,928,850,938,944,946,256,215,217,232,216,255])).
% 59.88/59.97 cnf(973,plain,
% 59.88/59.97 (~P4(x9731,x9732,x9732,x9731,a19,a1,a1,a18)),
% 59.88/59.97 inference(scs_inference,[],[894,916,928,850,938,944,946,256,215,217,232,216,255,253])).
% 59.88/59.97 cnf(977,plain,
% 59.88/59.97 (~P10(x9771,x9772,x9773,x9774)+~P4(a18,a19,a1,a19,x9771,x9772,x9773,x9774)),
% 59.88/59.97 inference(scs_inference,[],[894,916,928,850,454,938,944,946,256,215,217,232,216,255,253,254,241])).
% 59.88/59.97 cnf(1004,plain,
% 59.88/59.97 (~P4(a1,a19,a1,a18,x10041,x10042,x10041,x10042)),
% 59.88/59.97 inference(scs_inference,[],[924,940,942,965,967,215,256,216,255,253])).
% 59.88/59.97 cnf(1006,plain,
% 59.88/59.97 (~P11(x10061,x10062,x10062,a1,a18,a19)),
% 59.88/59.97 inference(scs_inference,[],[924,940,942,963,965,967,215,256,216,255,253,217])).
% 59.88/59.97 cnf(1008,plain,
% 59.88/59.97 (~P4(x10081,x10082,x10081,x10082,a18,a1,a1,a19)),
% 59.88/59.97 inference(scs_inference,[],[924,940,942,963,965,967,215,256,216,255,253,217,254])).
% 59.88/59.97 cnf(1016,plain,
% 59.88/59.97 (~P4(x10161,x10162,x10161,x10162,a18,a19,a18,a1)),
% 59.88/59.97 inference(scs_inference,[],[707,256])).
% 59.88/59.97 cnf(1022,plain,
% 59.88/59.97 (~P4(a19,a1,x10221,x10222,a18,a1,x10222,x10221)),
% 59.88/59.97 inference(scs_inference,[],[916,951,707,1006,256,253,215,255])).
% 59.88/59.97 cnf(1026,plain,
% 59.88/59.97 (~P10(x10261,x10262,x10263,x10264)+~P4(a19,a18,a19,a1,x10261,x10262,x10263,x10264)),
% 59.88/59.97 inference(scs_inference,[],[916,951,707,275,1006,256,253,215,255,254,241])).
% 59.88/59.97 cnf(1046,plain,
% 59.88/59.97 (~P4(x10461,x10462,x10461,x10462,a18,a1,a18,a19)),
% 59.88/59.97 inference(scs_inference,[],[930,767,253,256])).
% 59.88/59.97 cnf(1050,plain,
% 59.88/59.97 (~P4(x10501,x10502,a18,a1,x10502,x10501,a19,a1)),
% 59.88/59.97 inference(scs_inference,[],[930,973,942,767,253,256,255,254])).
% 59.88/59.97 cnf(1061,plain,
% 59.88/59.97 (~P4(x10611,x10612,x10612,x10611,a19,a1,a18,a1)),
% 59.88/59.97 inference(scs_inference,[],[1008,961,1022,256,253,255])).
% 59.88/59.97 cnf(1087,plain,
% 59.88/59.97 (~P4(a19,a1,a1,a18,x10871,x10872,x10871,x10872)),
% 59.88/59.97 inference(scs_inference,[],[961,1004,1050,253,256,255])).
% 59.88/59.97 cnf(1095,plain,
% 59.88/59.97 (~P4(a18,a19,a18,a1,x10951,x10952,x10951,x10952)),
% 59.88/59.97 inference(scs_inference,[],[1016,253])).
% 59.88/59.97 cnf(1099,plain,
% 59.88/59.97 (~P4(x10991,x10992,x10992,x10991,a18,a19,a18,a1)),
% 59.88/59.97 inference(scs_inference,[],[1016,1061,253,256,255])).
% 59.88/59.97 cnf(1101,plain,
% 59.88/59.97 (~P4(a18,a1,x11011,x11012,a18,a19,x11012,x11011)),
% 59.88/59.97 inference(scs_inference,[],[1016,1061,896,253,256,255,254])).
% 59.88/59.97 cnf(1107,plain,
% 59.88/59.97 (~P11(a1,a18,a19,a19,a18,a1)),
% 59.88/59.97 inference(scs_inference,[],[1016,1061,896,253,256,255,254,232,217,216])).
% 59.88/59.97 cnf(1130,plain,
% 59.88/59.97 (~P4(a18,a1,a18,a19,x11301,x11302,x11301,x11302)),
% 59.88/59.97 inference(scs_inference,[],[1046,1107,217,216,253])).
% 59.88/59.97 cnf(1144,plain,
% 59.88/59.97 (~P4(a18,a19,x11441,x11442,a18,a1,x11442,x11441)),
% 59.88/59.97 inference(scs_inference,[],[1101,256,253])).
% 59.88/59.97 cnf(1146,plain,
% 59.88/59.97 (~P4(a1,a18,x11461,x11462,a18,a19,x11462,x11461)),
% 59.88/59.97 inference(scs_inference,[],[1101,256,253,255])).
% 59.88/59.97 cnf(1152,plain,
% 59.88/59.97 (~P11(a1,a19,a18,a18,a18,a19)),
% 59.88/59.97 inference(scs_inference,[],[1087,1101,256,253,255,254,232,217])).
% 59.88/59.97 cnf(1154,plain,
% 59.88/59.97 (~P11(a18,a1,a19,a19,a18,a18)),
% 59.88/59.97 inference(scs_inference,[],[1087,1101,256,253,255,254,232,217,216])).
% 59.88/59.97 cnf(1156,plain,
% 59.88/59.97 (~P11(a18,a19,a18,a1,a18,a19)),
% 59.88/59.97 inference(scs_inference,[],[1087,1101,256,253,255,254,232,217,216,215])).
% 59.88/59.97 cnf(1163,plain,
% 59.88/59.97 (~P10(x11631,x11632,x11633,x11634)+~P4(a1,a19,a19,a18,x11631,x11632,x11633,x11634)),
% 59.88/59.97 inference(scs_inference,[],[146,472,924,1087,1101,291,256,253,255,254,232,217,216,215,228,88,104,241])).
% 59.88/59.97 cnf(1171,plain,
% 59.88/59.97 (~P11(a18,a19,a1,a19,a18,a18)),
% 59.88/59.97 inference(scs_inference,[],[1154,217])).
% 59.88/59.97 cnf(1173,plain,
% 59.88/59.97 (~P11(a19,a1,a18,a18,a18,a19)),
% 59.88/59.97 inference(scs_inference,[],[1152,1154,217,216])).
% 59.88/59.97 cnf(1175,plain,
% 59.88/59.97 (~P11(a18,a18,a19,a1,a19,a18)),
% 59.88/59.97 inference(scs_inference,[],[1152,1154,217,216,215])).
% 59.88/59.97 cnf(1177,plain,
% 59.88/59.97 (~P4(x11771,x11772,x11771,x11772,a1,a18,a19,a18)),
% 59.88/59.97 inference(scs_inference,[],[854,1152,1154,217,216,215,256])).
% 59.88/59.97 cnf(1179,plain,
% 59.88/59.97 (~P4(a18,a19,a18,a1,x11791,x11792,x11792,x11791)),
% 59.88/59.97 inference(scs_inference,[],[1099,854,1152,1154,217,216,215,256,253])).
% 59.88/59.97 cnf(1181,plain,
% 59.88/59.97 (~P4(a19,a18,a18,a1,x11811,x11812,x11811,x11812)),
% 59.88/59.97 inference(scs_inference,[],[1095,1099,854,1152,1154,217,216,215,256,253,255])).
% 59.88/59.97 cnf(1183,plain,
% 59.88/59.97 (~P4(x11831,x11832,a1,a18,x11832,x11831,a18,a19)),
% 59.88/59.97 inference(scs_inference,[],[1095,1099,854,1146,1152,1154,217,216,215,256,253,255,254])).
% 59.88/59.97 cnf(1190,plain,
% 59.88/59.97 (~P10(x11901,x11902,x11903,x11904)+~P4(a18,a19,a19,a1,x11901,x11902,x11903,x11904)),
% 59.88/59.97 inference(scs_inference,[],[928,1095,1099,854,1146,322,1152,1154,217,216,215,256,253,255,254,232,228,241])).
% 59.88/59.97 cnf(1198,plain,
% 59.88/59.97 (~P11(a19,a18,a1,a18,a19,a18)),
% 59.88/59.97 inference(scs_inference,[],[1173,217])).
% 59.88/59.97 cnf(1204,plain,
% 59.88/59.97 (~P4(x12041,x12042,x12042,x12041,a1,a18,a18,a19)),
% 59.88/59.97 inference(scs_inference,[],[1183,1156,1171,1173,217,216,215,256])).
% 59.88/59.97 cnf(1206,plain,
% 59.88/59.97 (~P4(a1,a18,a19,a18,x12061,x12062,x12061,x12062)),
% 59.88/59.97 inference(scs_inference,[],[1177,1183,1156,1171,1173,217,216,215,256,253])).
% 59.88/59.97 cnf(1208,plain,
% 59.88/59.97 (~P4(a1,a18,a18,a19,x12081,x12082,x12081,x12082)),
% 59.88/59.97 inference(scs_inference,[],[1130,1177,1183,1156,1171,1173,217,216,215,256,253,255])).
% 59.88/59.97 cnf(1210,plain,
% 59.88/59.97 (~P4(x12101,x12102,x12101,x12102,a19,a18,a1,a18)),
% 59.88/59.97 inference(scs_inference,[],[1130,1177,1183,1156,1171,1173,217,216,215,256,253,255,254])).
% 59.88/59.97 cnf(1212,plain,
% 59.88/59.97 (~P11(x12121,x12122,x12121,a1,a18,a19)),
% 59.88/59.97 inference(scs_inference,[],[1130,1177,1183,1156,1171,1173,217,216,215,256,253,255,254,232])).
% 59.88/59.97 cnf(1218,plain,
% 59.88/59.97 (~P10(x12181,x12182,x12183,x12184)+~P4(a1,a18,a1,a19,x12181,x12182,x12183,x12184)),
% 59.88/59.97 inference(scs_inference,[],[340,971,1130,1177,1183,354,1156,1171,1173,217,216,215,256,253,255,254,232,228,89,241])).
% 59.88/59.97 cnf(1225,plain,
% 59.88/59.97 (~P11(x12251,x12251,x12252,a1,a19,a18)),
% 59.88/59.97 inference(scs_inference,[],[1212,217])).
% 59.88/59.97 cnf(1229,plain,
% 59.88/59.97 (~P11(a1,a18,a19,x12291,x12292,x12291)),
% 59.88/59.97 inference(scs_inference,[],[1175,1212,217,216,215])).
% 59.88/59.97 cnf(1233,plain,
% 59.88/59.97 (~P4(x12331,x12332,x12331,x12332,a19,a18,a18,a1)),
% 59.88/59.97 inference(scs_inference,[],[1181,1146,1175,1212,217,216,215,256,253])).
% 59.88/59.97 cnf(1235,plain,
% 59.88/59.97 (~P4(a19,a18,x12351,x12352,a18,a1,x12352,x12351)),
% 59.88/59.97 inference(scs_inference,[],[1144,1181,1146,1175,1212,217,216,215,256,253,255])).
% 59.88/59.97 cnf(1247,plain,
% 59.88/59.97 (~P11(a1,a19,a18,x12471,x12471,x12472)),
% 59.88/59.97 inference(scs_inference,[],[1229,217])).
% 59.88/59.97 cnf(1249,plain,
% 59.88/59.97 (~P11(x12491,x12491,x12492,a19,a1,a18)),
% 59.88/59.97 inference(scs_inference,[],[1225,1229,217,216])).
% 59.88/59.97 cnf(1255,plain,
% 59.88/59.97 (~P4(a18,a19,x12551,x12552,a1,a18,x12552,x12551)),
% 59.88/59.97 inference(scs_inference,[],[1146,1210,1225,1229,1198,217,216,215,256,253])).
% 59.88/59.97 cnf(1257,plain,
% 59.88/59.97 (~P4(a19,a18,a18,a1,x12571,x12572,x12572,x12571)),
% 59.88/59.97 inference(scs_inference,[],[1179,1146,1210,1225,1229,1198,217,216,215,256,253,255])).
% 59.88/59.97 cnf(1259,plain,
% 59.88/59.97 (~P4(x12591,x12592,x12592,x12591,a18,a19,a1,a18)),
% 59.88/59.97 inference(scs_inference,[],[1179,1146,1204,1210,1225,1229,1198,217,216,215,256,253,255,254])).
% 59.88/59.97 cnf(1261,plain,
% 59.88/59.97 (~P11(a19,a18,a1,x12611,x12612,x12611)),
% 59.88/59.97 inference(scs_inference,[],[1179,1146,1204,1210,1225,1229,1198,217,216,215,256,253,255,254,232])).
% 59.88/59.97 cnf(1266,plain,
% 59.88/59.97 (~P10(x12661,x12662,x12663,x12664)+~P4(a18,a1,a18,a19,x12661,x12662,x12663,x12664)),
% 59.88/59.97 inference(scs_inference,[],[1016,1179,1146,1204,1210,400,1225,1229,1198,217,216,215,256,253,255,254,232,228,241])).
% 59.88/59.97 cnf(1280,plain,
% 59.88/59.97 (~P4(x12801,x12802,x12801,x12802,a1,a18,a18,a19)),
% 59.88/59.97 inference(scs_inference,[],[1208,1233,1247,1249,217,216,256,253])).
% 59.88/59.97 cnf(1282,plain,
% 59.88/59.97 (~P4(x12821,x12822,x12822,x12821,a1,a18,a19,a18)),
% 59.88/59.97 inference(scs_inference,[],[1177,1208,1233,1247,1249,217,216,256,253,255])).
% 59.88/59.97 cnf(1289,plain,
% 59.88/59.97 (~P10(x12891,x12892,x12893,x12894)+~P4(a1,a19,a18,a19,x12891,x12892,x12893,x12894)),
% 59.88/59.97 inference(scs_inference,[],[1046,1177,1206,1208,1233,431,1247,1249,217,216,256,253,255,254,228,241])).
% 59.88/59.97 cnf(1299,plain,
% 59.88/59.97 (~P11(x12991,x12992,x12992,a18,a19,a1)),
% 59.88/59.97 inference(scs_inference,[],[1261,216,215])).
% 59.88/59.97 cnf(1303,plain,
% 59.88/59.97 (~P4(a18,a1,x13031,x13032,a19,a18,x13032,x13031)),
% 59.88/59.97 inference(scs_inference,[],[1235,1255,1261,216,215,256,253])).
% 59.88/59.97 cnf(1305,plain,
% 59.88/59.97 (~P4(x13051,x13052,x13052,x13051,a19,a18,a1,a18)),
% 59.88/59.97 inference(scs_inference,[],[1210,1235,1255,1261,216,215,256,253,255])).
% 59.88/59.97 cnf(1317,plain,
% 59.88/59.97 (~P11(x13171,x13172,x13172,a18,a1,a19)),
% 59.88/59.97 inference(scs_inference,[],[1299,217])).
% 59.88/59.97 cnf(1325,plain,
% 59.88/59.97 (~P4(x13251,x13252,x13251,x13252,a18,a1,a19,a18)),
% 59.88/59.97 inference(scs_inference,[],[1233,1257,1259,1299,217,256,253,255,254])).
% 59.88/59.97 cnf(1327,plain,
% 59.88/59.97 (~P10(x13271,x13272,x13273,x13274)+~P4(a18,a1,a19,a1,x13271,x13272,x13273,x13274)),
% 59.88/59.97 inference(scs_inference,[],[1233,1257,1259,489,1299,217,256,253,255,254,241])).
% 59.88/59.97 cnf(1351,plain,
% 59.88/59.97 (~P4(a18,a1,a19,a18,x13511,x13512,x13512,x13511)),
% 59.88/59.97 inference(scs_inference,[],[1257,1280,1255,1282,256,253,255,254])).
% 59.88/59.97 cnf(1367,plain,
% 59.88/59.97 (~P10(x13671,x13672,x13673,x13674)+~P4(a1,a18,a19,a18,x13671,x13672,x13673,x13674)),
% 59.88/59.97 inference(scs_inference,[],[1235,1282,1303,1305,530,256,253,255,254,241])).
% 59.88/59.97 cnf(1385,plain,
% 59.88/59.97 (~P4(x13851,x13852,a19,a18,x13852,x13851,a1,a18)),
% 59.88/59.97 inference(scs_inference,[],[1305,256])).
% 59.88/59.97 cnf(1387,plain,
% 59.88/59.97 (~P4(x13871,x13872,x13872,x13871,a18,a1,a19,a18)),
% 59.88/59.97 inference(scs_inference,[],[1305,1351,256,253])).
% 59.88/59.97 cnf(1398,plain,
% 59.88/59.97 (~P4(x13981,x13982,a18,a1,x13981,x13982,a19,a18)),
% 59.88/59.97 inference(scs_inference,[],[1325,256])).
% 59.88/59.97 cnf(1406,plain,
% 59.88/59.97 (~P10(x14061,x14062,x14063,x14064)+~P4(a19,a1,a1,a18,x14061,x14062,x14063,x14064)),
% 59.88/59.97 inference(scs_inference,[],[556,241])).
% 59.88/59.97 cnf(1408,plain,
% 59.88/59.97 (~P4(a19,a1,a1,a18,x14081,x14082,a2,a17)+~P3(x14081,x14082,a19,a16)),
% 59.88/59.97 inference(scs_inference,[],[556,241,580])).
% 59.88/59.97 cnf(1462,plain,
% 59.88/59.97 (~P10(x14621,x14622,x14623,x14624)+~P4(a1,a18,a19,a1,x14621,x14622,x14623,x14624)),
% 59.88/59.97 inference(scs_inference,[],[570,241])).
% 59.88/59.97 cnf(1487,plain,
% 59.88/59.97 (~P10(x14871,x14872,x14873,x14874)+~P4(a19,a18,a18,a1,x14871,x14872,x14873,x14874)),
% 59.88/59.97 inference(scs_inference,[],[591,241])).
% 59.88/59.97 cnf(1489,plain,
% 59.88/59.97 (~P4(a19,a18,a18,a1,x14891,x14892,a2,a17)+~P3(x14891,x14892,a19,a16)),
% 59.88/59.97 inference(scs_inference,[],[591,241,580])).
% 59.88/59.97 cnf(1514,plain,
% 59.88/59.97 (~P10(x15141,x15142,x15143,x15144)+~P4(a18,a1,a19,a18,x15141,x15142,x15143,x15144)),
% 59.88/59.97 inference(scs_inference,[],[600,241])).
% 59.88/59.97 cnf(1545,plain,
% 59.88/59.97 (~P10(x15451,x15452,x15453,x15454)+~P4(a19,a1,a18,a19,x15451,x15452,x15453,x15454)),
% 59.88/59.97 inference(scs_inference,[],[277,241])).
% 59.88/59.97 cnf(1576,plain,
% 59.88/59.97 (~P10(x15761,x15762,x15763,x15764)+~P4(a1,a19,a18,a1,x15761,x15762,x15763,x15764)),
% 59.88/59.97 inference(scs_inference,[],[352,241])).
% 59.88/59.97 cnf(1603,plain,
% 59.88/59.97 (~P10(x16031,x16032,x16033,x16034)+~P4(a18,a19,a1,a18,x16031,x16032,x16033,x16034)),
% 59.88/59.97 inference(scs_inference,[],[402,241])).
% 59.88/59.97 cnf(1629,plain,
% 59.88/59.97 (~P10(x16291,x16292,x16293,x16294)+~P4(a18,a1,a1,a19,x16291,x16292,x16293,x16294)),
% 59.88/59.97 inference(scs_inference,[],[427,241])).
% 59.88/59.97 cnf(1656,plain,
% 59.88/59.97 (~P10(x16561,x16562,x16563,x16564)+~P4(a1,a18,a18,a19,x16561,x16562,x16563,x16564)),
% 59.88/59.97 inference(scs_inference,[],[464,241])).
% 59.88/59.97 cnf(1682,plain,
% 59.88/59.97 (~P10(x16821,x16822,x16823,x16824)+~P4(a19,a1,a18,a1,x16821,x16822,x16823,x16824)),
% 59.88/59.97 inference(scs_inference,[],[495,241])).
% 59.88/59.97 cnf(1709,plain,
% 59.88/59.97 (~P10(x17091,x17092,x17093,x17094)+~P4(a19,a18,a1,a18,x17091,x17092,x17093,x17094)),
% 59.88/59.97 inference(scs_inference,[],[532,241])).
% 59.88/59.97 cnf(2101,plain,
% 59.88/59.97 (P1(a1,a15,a2)),
% 59.88/59.97 inference(scs_inference,[],[142,153])).
% 59.88/59.97 cnf(2103,plain,
% 59.88/59.97 (P1(a2,a1,a15)),
% 59.88/59.97 inference(scs_inference,[],[142,153,152])).
% 59.88/59.97 cnf(2107,plain,
% 59.88/59.97 (P4(a17,a2,a17,a2,a2,a16,a2,a15)),
% 59.88/59.97 inference(scs_inference,[],[142,148,153,152,253,256])).
% 59.88/59.97 cnf(2111,plain,
% 59.88/59.97 (P3(a19,a16,a17,a2)),
% 59.88/59.97 inference(scs_inference,[],[142,147,148,153,152,253,256,254,167])).
% 59.88/59.97 cnf(2113,plain,
% 59.88/59.97 (P4(a2,a17,a2,a16,a17,a2,a2,a15)),
% 59.88/59.97 inference(scs_inference,[],[142,147,148,153,152,253,256,254,167,255])).
% 59.88/59.97 cnf(2115,plain,
% 59.88/59.97 (P3(a2,a17,a19,a16)),
% 59.88/59.97 inference(scs_inference,[],[142,147,148,153,152,253,256,254,167,255,166])).
% 59.88/59.97 cnf(2121,plain,
% 59.88/59.97 (P1(a2,a2,a1)),
% 59.88/59.97 inference(scs_inference,[],[142,147,148,153,152,253,256,254,167,255,166,181,263,156])).
% 59.88/59.97 cnf(2123,plain,
% 59.88/59.97 (P4(a17,a2,a2,a15,a17,a2,a2,a15)),
% 59.88/59.97 inference(scs_inference,[],[142,147,148,153,152,253,256,254,167,255,166,181,263,156,715])).
% 59.88/59.97 cnf(2125,plain,
% 59.88/59.97 (P10(a2,a16,a2,a15)),
% 59.88/59.97 inference(scs_inference,[],[142,147,148,153,152,253,256,254,167,255,166,181,263,156,715,234])).
% 59.88/59.97 cnf(2127,plain,
% 59.88/59.97 (P4(a19,a16,x21271,x21272,a19,a16,x21271,x21272)),
% 59.88/59.97 inference(scs_inference,[],[142,147,148,153,152,253,256,254,167,255,166,181,263,156,715,234,226])).
% 59.88/59.97 cnf(2129,plain,
% 59.88/59.97 (P10(a2,a15,a2,a16)),
% 59.88/59.97 inference(scs_inference,[],[142,147,148,153,152,253,256,254,167,255,166,181,263,156,715,234,226,164])).
% 59.88/59.97 cnf(2131,plain,
% 59.88/59.97 (P10(a2,a17,a2,a17)),
% 59.88/59.97 inference(scs_inference,[],[142,147,148,153,152,253,256,254,167,255,166,181,263,156,715,234,226,164,580])).
% 59.88/59.97 cnf(2133,plain,
% 59.88/59.97 (P1(a19,a16,a16)),
% 59.88/59.97 inference(scs_inference,[],[142,147,148,153,152,253,256,254,167,255,166,181,263,156,715,234,226,164,580,161])).
% 59.88/59.97 cnf(2135,plain,
% 59.88/59.97 (P10(a19,a16,a16,a19)),
% 59.88/59.97 inference(scs_inference,[],[142,147,148,153,152,253,256,254,167,255,166,181,263,156,715,234,226,164,580,161,165])).
% 59.88/59.97 cnf(2138,plain,
% 59.88/59.97 (P6(a16,a17,a19,a19)),
% 59.88/59.97 inference(scs_inference,[],[142,273,472,147,148,153,152,253,256,254,167,255,166,181,263,156,715,234,226,164,580,161,165,139,237])).
% 59.88/59.97 cnf(2140,plain,
% 59.88/59.97 (P10(a17,a2,a17,a2)),
% 59.88/59.97 inference(scs_inference,[],[142,273,472,147,148,153,152,253,256,254,167,255,166,181,263,156,715,234,226,164,580,161,165,139,237,241])).
% 59.88/59.97 cnf(2142,plain,
% 59.88/59.97 (P6(a17,a16,a19,a19)),
% 59.88/59.97 inference(scs_inference,[],[142,273,472,147,148,153,152,253,256,254,167,255,166,181,263,156,715,234,226,164,580,161,165,139,237,241,170])).
% 59.88/59.97 cnf(2144,plain,
% 59.88/59.97 (P6(a16,a19,a17,a19)),
% 59.88/59.97 inference(scs_inference,[],[142,273,472,147,148,153,152,253,256,254,167,255,166,181,263,156,715,234,226,164,580,161,165,139,237,241,170,171])).
% 59.88/59.97 cnf(2146,plain,
% 59.88/59.97 (P6(a16,a19,a19,a17)),
% 59.88/59.97 inference(scs_inference,[],[142,273,472,147,148,153,152,253,256,254,167,255,166,181,263,156,715,234,226,164,580,161,165,139,237,241,170,171,172])).
% 59.88/59.97 cnf(2148,plain,
% 59.88/59.97 (P4(a19,a17,a19,a16,a19,a17,a19,a16)),
% 59.88/59.97 inference(scs_inference,[],[142,273,472,147,148,153,152,253,256,254,167,255,166,181,263,156,715,234,226,164,580,161,165,139,237,241,170,171,172,225])).
% 59.88/59.97 cnf(2201,plain,
% 59.88/59.97 (P6(a19,a16,a17,a19)),
% 59.88/59.97 inference(scs_inference,[],[2144,170])).
% 59.88/59.97 cnf(2213,plain,
% 59.88/59.97 (P6(a17,a19,a16,a19)),
% 59.88/59.97 inference(scs_inference,[],[2129,2142,2144,2148,170,1289,829,856,225,234,171])).
% 59.88/59.97 cnf(2239,plain,
% 59.88/59.97 (P6(a19,a16,a19,a17)),
% 59.88/59.97 inference(scs_inference,[],[2129,2142,2144,2148,170,1289,829,856,225,234,171,1327,1545,1266,977,1218,1367,1514,1163,1190,1462,477,742,172])).
% 59.88/59.97 cnf(2255,plain,
% 59.88/59.97 (P4(a2,a16,x22551,x22552,a2,a15,x22551,x22552)),
% 59.88/59.97 inference(scs_inference,[],[2125,2129,2142,2144,2148,170,1289,829,856,225,234,171,1327,1545,1266,977,1218,1367,1514,1163,1190,1462,477,742,172,1603,1709,1682,1629,1026,1656,1406,226])).
% 59.88/59.97 cnf(2263,plain,
% 59.88/59.97 (P1(a2,a15,a1)),
% 59.88/59.97 inference(scs_inference,[],[2103,2125,2129,2135,2142,2144,2148,170,1289,829,856,225,234,171,1327,1545,1266,977,1218,1367,1514,1163,1190,1462,477,742,172,1603,1709,1682,1629,1026,1656,1406,226,1487,1576,164,153])).
% 59.88/59.97 cnf(2269,plain,
% 59.88/59.97 (P1(a2,a16,a15)),
% 59.88/59.97 inference(scs_inference,[],[2101,2103,2107,2125,2129,2135,2142,2144,2148,170,1289,829,856,225,234,171,1327,1545,1266,977,1218,1367,1514,1163,1190,1462,477,742,172,1603,1709,1682,1629,1026,1656,1406,226,1487,1576,164,153,152,253,161])).
% 59.88/59.97 cnf(2271,plain,
% 59.88/59.97 (P4(a19,a16,a19,a16,x22711,x22712,x22711,x22712)),
% 59.88/59.97 inference(scs_inference,[],[2127,2101,2103,2107,2125,2129,2135,2142,2144,2148,170,1289,829,856,225,234,171,1327,1545,1266,977,1218,1367,1514,1163,1190,1462,477,742,172,1603,1709,1682,1629,1026,1656,1406,226,1487,1576,164,153,152,253,161,256])).
% 59.88/59.97 cnf(2273,plain,
% 59.88/59.97 (P4(a16,a19,x22731,x22732,a19,a16,x22731,x22732)),
% 59.88/59.97 inference(scs_inference,[],[2127,2101,2103,2107,2125,2129,2135,2142,2144,2148,170,1289,829,856,225,234,171,1327,1545,1266,977,1218,1367,1514,1163,1190,1462,477,742,172,1603,1709,1682,1629,1026,1656,1406,226,1487,1576,164,153,152,253,161,256,255])).
% 59.88/59.97 cnf(2275,plain,
% 59.88/59.97 (P4(x22751,x22752,a19,a16,x22751,x22752,a19,a16)),
% 59.88/59.97 inference(scs_inference,[],[2127,2101,2103,2107,2125,2129,2135,2142,2144,2148,170,1289,829,856,225,234,171,1327,1545,1266,977,1218,1367,1514,1163,1190,1462,477,742,172,1603,1709,1682,1629,1026,1656,1406,226,1487,1576,164,153,152,253,161,256,255,254])).
% 59.88/59.97 cnf(2277,plain,
% 59.88/59.97 (P3(a2,a17,a16,a19)),
% 59.88/59.97 inference(scs_inference,[],[2127,2101,2103,2107,2115,2125,2129,2135,2142,2144,2148,170,1289,829,856,225,234,171,1327,1545,1266,977,1218,1367,1514,1163,1190,1462,477,742,172,1603,1709,1682,1629,1026,1656,1406,226,1487,1576,164,153,152,253,161,256,255,254,167])).
% 59.88/59.97 cnf(2279,plain,
% 59.88/59.97 (P3(a17,a2,a19,a16)),
% 59.88/59.97 inference(scs_inference,[],[2127,2101,2103,2107,2111,2115,2125,2129,2135,2142,2144,2148,170,1289,829,856,225,234,171,1327,1545,1266,977,1218,1367,1514,1163,1190,1462,477,742,172,1603,1709,1682,1629,1026,1656,1406,226,1487,1576,164,153,152,253,161,256,255,254,167,166])).
% 59.88/59.97 cnf(2281,plain,
% 59.88/59.97 (P10(a2,a16,a15,a2)),
% 59.88/59.97 inference(scs_inference,[],[2127,2101,2103,2107,2111,2115,2125,2129,2135,2142,2144,2148,170,1289,829,856,225,234,171,1327,1545,1266,977,1218,1367,1514,1163,1190,1462,477,742,172,1603,1709,1682,1629,1026,1656,1406,226,1487,1576,164,153,152,253,161,256,255,254,167,166,165])).
% 59.88/59.97 cnf(2287,plain,
% 59.88/59.97 (~E(a18,a19)),
% 59.88/59.97 inference(scs_inference,[],[2127,2101,2103,2107,2111,2115,2125,2129,2135,2142,2144,2148,852,364,170,1289,829,856,225,234,171,1327,1545,1266,977,1218,1367,1514,1163,1190,1462,477,742,172,1603,1709,1682,1629,1026,1656,1406,226,1487,1576,164,153,152,253,161,256,255,254,167,166,165,180,113,114])).
% 59.88/59.97 cnf(2291,plain,
% 59.88/59.97 (~P4(a2,a15,a18,a1,a2,a16,a19,a18)),
% 59.88/59.97 inference(scs_inference,[],[2127,2101,2103,2107,2111,2115,2125,2129,2135,2142,2144,2148,1398,852,364,454,170,1289,829,856,225,234,171,1327,1545,1266,977,1218,1367,1514,1163,1190,1462,477,742,172,1603,1709,1682,1629,1026,1656,1406,226,1487,1576,164,153,152,253,161,256,255,254,167,166,165,180,113,114,241,263])).
% 59.88/59.97 cnf(2294,plain,
% 59.88/59.97 (P6(a17,a19,a19,a19)),
% 59.88/59.97 inference(scs_inference,[],[2127,2101,2103,2107,2111,2115,2125,2129,2135,2138,2142,2144,2148,1398,852,364,454,170,1289,829,856,225,234,171,1327,1545,1266,977,1218,1367,1514,1163,1190,1462,477,742,172,1603,1709,1682,1629,1026,1656,1406,226,1487,1576,164,153,152,253,161,256,255,254,167,166,165,180,113,114,241,263,186])).
% 59.88/59.97 cnf(2307,plain,
% 59.88/59.97 (P6(a19,a17,a16,a19)),
% 59.88/59.97 inference(scs_inference,[],[2201,2281,1289,1367,171])).
% 59.88/59.97 cnf(2311,plain,
% 59.88/59.97 (P6(a19,a17,a19,a19)),
% 59.88/59.97 inference(scs_inference,[],[2201,2281,2294,1289,1367,171,1190,170])).
% 59.88/59.97 cnf(2335,plain,
% 59.88/59.97 (P4(a17,a2,x23351,x23352,a17,a2,x23351,x23352)),
% 59.88/59.97 inference(scs_inference,[],[2140,2146,2201,2281,2294,1289,1367,171,1190,170,829,1545,1709,1462,1603,1514,1266,1682,225,856,1026,226])).
% 59.88/59.97 cnf(2337,plain,
% 59.88/59.97 (P6(a17,a19,a19,a16)),
% 59.88/59.97 inference(scs_inference,[],[2140,2146,2201,2213,2281,2294,1289,1367,171,1190,170,829,1545,1709,1462,1603,1514,1266,1682,225,856,1026,226,172])).
% 59.88/59.97 cnf(2345,plain,
% 59.88/59.97 (P10(x23451,x23452,x23451,x23452)),
% 59.88/59.97 inference(scs_inference,[],[2140,2146,2275,2201,2213,2281,2294,1289,1367,171,1190,170,829,1545,1709,1462,1603,1514,1266,1682,225,856,1026,226,172,1487,1218,1163,234])).
% 59.88/59.97 cnf(2364,plain,
% 59.88/59.97 (P1(a16,a19,a16)),
% 59.88/59.97 inference(scs_inference,[],[2287,2140,2146,2133,2275,2121,2201,2213,2281,2294,1289,1367,171,1190,170,829,1545,1709,1462,1603,1514,1266,1682,225,856,1026,226,172,1487,1218,1163,234,742,1327,1576,2,1629,1656,1406,477,153,152])).
% 59.88/59.97 cnf(2366,plain,
% 59.88/59.97 (P10(a15,a2,a2,a16)),
% 59.88/59.97 inference(scs_inference,[],[2287,2140,2146,2133,2275,2121,2201,2213,2281,2294,1289,1367,171,1190,170,829,1545,1709,1462,1603,1514,1266,1682,225,856,1026,226,172,1487,1218,1163,234,742,1327,1576,2,1629,1656,1406,477,153,152,164])).
% 59.88/59.97 cnf(2368,plain,
% 59.88/59.97 (P1(a17,a2,a2)),
% 59.88/59.97 inference(scs_inference,[],[2287,2140,2146,2133,2275,2121,2201,2213,2281,2294,1289,1367,171,1190,170,829,1545,1709,1462,1603,1514,1266,1682,225,856,1026,226,172,1487,1218,1163,234,742,1327,1576,2,1629,1656,1406,477,153,152,164,161])).
% 59.88/59.97 cnf(2370,plain,
% 59.88/59.97 (P4(a2,a15,x23701,x23702,a2,a16,x23701,x23702)),
% 59.88/59.97 inference(scs_inference,[],[2287,2140,2146,2133,2255,2275,2121,2201,2213,2281,2294,1289,1367,171,1190,170,829,1545,1709,1462,1603,1514,1266,1682,225,856,1026,226,172,1487,1218,1163,234,742,1327,1576,2,1629,1656,1406,477,153,152,164,161,253])).
% 59.88/59.97 cnf(2380,plain,
% 59.88/59.97 (P3(a17,a2,a16,a19)),
% 59.88/59.97 inference(scs_inference,[],[2287,2123,2140,2146,2277,2279,2133,2255,2275,2121,2201,2213,2281,2294,1289,1367,171,1190,170,829,1545,1709,1462,1603,1514,1266,1682,225,856,1026,226,172,1487,1218,1163,234,742,1327,1576,2,1629,1656,1406,477,153,152,164,161,253,256,255,254,166,167])).
% 59.88/59.97 cnf(2387,plain,
% 59.88/59.97 (P4(a16,a19,x23871,x23872,a19,a16,x23871,x23872)),
% 59.88/59.97 inference(rename_variables,[],[2273])).
% 59.88/59.97 cnf(2388,plain,
% 59.88/59.97 (P6(a16,a16,a19,a16)),
% 59.88/59.97 inference(scs_inference,[],[2287,2123,2140,2131,2146,2277,2279,2133,2255,2271,2273,2275,2121,2201,2213,2281,2294,404,431,1289,1367,171,1190,170,829,1545,1709,1462,1603,1514,1266,1682,225,856,1026,226,172,1487,1218,1163,234,742,1327,1576,2,1629,1656,1406,477,153,152,164,161,253,256,255,254,166,167,165,129,120,237])).
% 59.88/59.97 cnf(2389,plain,
% 59.88/59.97 (P4(a19,a16,a19,a16,x23891,x23892,x23891,x23892)),
% 59.88/59.97 inference(rename_variables,[],[2271])).
% 59.88/59.97 cnf(2398,plain,
% 59.88/59.97 (P5(a16,a16,a16,a16)),
% 59.88/59.97 inference(scs_inference,[],[2287,2123,2140,2131,2146,2277,2279,2133,2255,2271,2389,2273,2387,2275,2121,2201,2213,2281,2294,439,404,2111,431,1289,1367,171,1190,170,829,1545,1709,1462,1603,1514,1266,1682,225,856,1026,226,172,1487,1218,1163,234,742,1327,1576,2,1629,1656,1406,477,153,152,164,161,253,256,255,254,166,167,165,129,120,237,263,242,252])).
% 59.88/59.97 cnf(2401,plain,
% 59.88/59.97 (P4(a16,a16,a16,a16,a16,a16,a16,a16)),
% 59.88/59.97 inference(scs_inference,[],[2287,2123,2140,2131,2146,2277,2279,2133,2255,2271,2389,2273,2387,2275,2121,2201,2213,2281,2294,439,404,2111,431,1289,1367,171,1190,170,829,1545,1709,1462,1603,1514,1266,1682,225,856,1026,226,172,1487,1218,1163,234,742,1327,1576,2,1629,1656,1406,477,153,152,164,161,253,256,255,254,166,167,165,129,120,237,263,242,252,227])).
% 59.88/59.97 cnf(2415,plain,
% 59.88/59.97 (P3(a16,a16,a16,a16)),
% 59.88/59.97 inference(scs_inference,[],[2287,2123,2140,2131,2146,2277,2279,2133,2255,2271,2389,2273,2387,2275,2121,2201,2213,2281,2294,439,404,320,2111,431,1289,1367,171,1190,170,829,1545,1709,1462,1603,1514,1266,1682,225,856,1026,226,172,1487,1218,1163,234,742,1327,1576,2,1629,1656,1406,477,153,152,164,161,253,256,255,254,166,167,165,129,120,237,263,242,252,227,977,179,246,250,241,185,182])).
% 59.88/59.97 cnf(2417,plain,
% 59.88/59.97 (P3(f7(a16,a16,a16,a16),a16,a16,a16)),
% 59.88/59.97 inference(scs_inference,[],[2287,2123,2140,2131,2146,2277,2279,2133,2255,2271,2389,2273,2387,2275,2121,2201,2213,2281,2294,439,404,320,2111,431,1289,1367,171,1190,170,829,1545,1709,1462,1603,1514,1266,1682,225,856,1026,226,172,1487,1218,1163,234,742,1327,1576,2,1629,1656,1406,477,153,152,164,161,253,256,255,254,166,167,165,129,120,237,263,242,252,227,977,179,246,250,241,185,182,188])).
% 59.88/59.97 cnf(2426,plain,
% 59.88/59.97 (P6(a19,a19,a16,a17)),
% 59.88/59.97 inference(scs_inference,[],[2239,2366,1367,1289,1545,171])).
% 59.88/59.97 cnf(2434,plain,
% 59.88/59.97 (P4(x24341,x24342,x24343,x24344,x24341,x24342,x24343,x24344)),
% 59.88/59.97 inference(scs_inference,[],[2345,2239,2366,1367,1289,1545,171,1682,1026,1462,226])).
% 59.88/59.97 cnf(2444,plain,
% 59.88/59.97 (P6(a19,a17,a19,a16)),
% 59.88/59.97 inference(scs_inference,[],[2345,2239,2337,2366,1367,1289,1545,171,1682,1026,1462,226,1163,225,1190,1576,170])).
% 59.88/59.97 cnf(2476,plain,
% 59.88/59.97 (P1(a2,a15,a16)),
% 59.88/59.97 inference(scs_inference,[],[2345,2239,2263,2269,2337,2366,2388,1367,1289,1545,171,1682,1026,1462,226,1163,225,1190,1576,170,1514,1656,742,1603,1406,1218,829,1266,1709,1487,477,1629,1327,172,152,153])).
% 59.88/59.97 cnf(2478,plain,
% 59.88/59.97 (P4(a17,a2,a17,a2,x24781,x24782,x24781,x24782)),
% 59.88/59.97 inference(scs_inference,[],[2345,2239,2335,2263,2269,2337,2366,2388,1367,1289,1545,171,1682,1026,1462,226,1163,225,1190,1576,170,1514,1656,742,1603,1406,1218,829,1266,1709,1487,477,1629,1327,172,152,153,256])).
% 59.88/59.97 cnf(2482,plain,
% 59.88/59.97 (P1(x24821,x24822,x24822)),
% 59.88/59.97 inference(scs_inference,[],[2345,2239,2335,2113,2263,2269,2337,2366,2388,1367,1289,1545,171,1682,1026,1462,226,1163,225,1190,1576,170,1514,1656,742,1603,1406,1218,829,1266,1709,1487,477,1629,1327,172,152,153,256,253,161])).
% 59.88/59.97 cnf(2484,plain,
% 59.88/59.97 (P4(a2,a17,x24841,x24842,a17,a2,x24841,x24842)),
% 59.88/59.97 inference(scs_inference,[],[2345,2239,2335,2113,2263,2269,2337,2366,2388,1367,1289,1545,171,1682,1026,1462,226,1163,225,1190,1576,170,1514,1656,742,1603,1406,1218,829,1266,1709,1487,477,1629,1327,172,152,153,256,253,161,255])).
% 59.88/59.97 cnf(2486,plain,
% 59.88/59.97 (P4(x24861,x24862,a2,a15,x24861,x24862,a2,a16)),
% 59.88/59.97 inference(scs_inference,[],[2345,2239,2335,2370,2113,2263,2269,2337,2366,2388,1367,1289,1545,171,1682,1026,1462,226,1163,225,1190,1576,170,1514,1656,742,1603,1406,1218,829,1266,1709,1487,477,1629,1327,172,152,153,256,253,161,255,254])).
% 59.88/59.97 cnf(2488,plain,
% 59.88/59.97 (P3(a18,a17,a15,a16)),
% 59.88/59.97 inference(scs_inference,[],[2345,2239,2335,2370,2113,2263,2269,2337,2366,2388,146,1367,1289,1545,171,1682,1026,1462,226,1163,225,1190,1576,170,1514,1656,742,1603,1406,1218,829,1266,1709,1487,477,1629,1327,172,152,153,256,253,161,255,254,167])).
% 59.88/59.97 cnf(2492,plain,
% 59.88/59.97 (P10(x24921,x24922,x24922,x24921)),
% 59.88/59.97 inference(scs_inference,[],[2345,2239,2335,2370,2113,2263,2269,2337,2366,2388,2417,146,1367,1289,1545,171,1682,1026,1462,226,1163,225,1190,1576,170,1514,1656,742,1603,1406,1218,829,1266,1709,1487,477,1629,1327,172,152,153,256,253,161,255,254,167,166,165])).
% 59.88/59.97 cnf(2498,plain,
% 59.88/59.97 (P2(f8(a16,a16,a16),a16,a16,a16)),
% 59.88/59.97 inference(scs_inference,[],[2345,2239,2335,2370,2113,2263,2269,2337,2366,2388,2398,2415,2417,146,1367,1289,1545,171,1682,1026,1462,226,1163,225,1190,1576,170,1514,1656,742,1603,1406,1218,829,1266,1709,1487,477,1629,1327,172,152,153,256,253,161,255,254,167,166,165,177,189,192])).
% 59.88/59.97 cnf(2502,plain,
% 59.88/59.97 (P1(f12(a16,a16,a16,a19,a16),a19,a16)),
% 59.88/59.97 inference(scs_inference,[],[2345,2239,2335,2370,2113,2263,2269,2337,2364,2366,2388,2398,2415,2417,146,1367,1289,1545,171,1682,1026,1462,226,1163,225,1190,1576,170,1514,1656,742,1603,1406,1218,829,1266,1709,1487,477,1629,1327,172,152,153,256,253,161,255,254,167,166,165,177,189,192,194,198])).
% 59.88/59.97 cnf(2506,plain,
% 59.88/59.97 (P5(a16,a16,a16,f26(a16,a16,a16,a16,a16))),
% 59.88/59.97 inference(scs_inference,[],[2345,2239,2335,2370,2113,2263,2269,2337,2364,2366,2388,2398,2415,2417,146,1367,1289,1545,171,1682,1026,1462,226,1163,225,1190,1576,170,1514,1656,742,1603,1406,1218,829,1266,1709,1487,477,1629,1327,172,152,153,256,253,161,255,254,167,166,165,177,189,192,194,198,199,200])).
% 59.88/59.97 cnf(2508,plain,
% 59.88/59.97 (P10(f26(a16,a16,a16,a16,a16),a16,a16,a16)),
% 59.88/59.97 inference(scs_inference,[],[2345,2239,2335,2370,2113,2263,2269,2337,2364,2366,2388,2398,2415,2417,146,1367,1289,1545,171,1682,1026,1462,226,1163,225,1190,1576,170,1514,1656,742,1603,1406,1218,829,1266,1709,1487,477,1629,1327,172,152,153,256,253,161,255,254,167,166,165,177,189,192,194,198,199,200,202])).
% 59.88/59.97 cnf(2510,plain,
% 59.88/59.97 (P6(a19,a1,a19,f25(a18,a1,a19,a19))),
% 59.88/59.97 inference(scs_inference,[],[2345,2239,2335,2370,2113,2263,2269,2337,2364,2366,2388,2398,2415,2417,356,146,1367,1289,1545,171,1682,1026,1462,226,1163,225,1190,1576,170,1514,1656,742,1603,1406,1218,829,1266,1709,1487,477,1629,1327,172,152,153,256,253,161,255,254,167,166,165,177,189,192,194,198,199,200,202,245])).
% 59.88/59.97 cnf(2522,plain,
% 59.88/59.97 (P6(a2,a2,a17,a2)),
% 59.88/59.97 inference(scs_inference,[],[2345,2239,2335,2370,2113,2263,2269,2337,2364,2366,2368,2388,2398,2401,2415,2417,356,146,1367,1289,1545,171,1682,1026,1462,226,1163,225,1190,1576,170,1514,1656,742,1603,1406,1218,829,1266,1709,1487,477,1629,1327,172,152,153,256,253,161,255,254,167,166,165,177,189,192,194,198,199,200,202,245,247,261,183,191,190,237])).
% 59.88/59.97 cnf(2524,plain,
% 59.88/59.97 (~P10(a18,f25(a18,a1,a19,a19),a1,f25(a18,a1,a19,a19))),
% 59.88/59.97 inference(scs_inference,[],[2345,2239,2335,2370,2113,2263,2269,2337,2364,2366,2368,2388,2398,2401,2415,2417,356,454,146,1367,1289,1545,171,1682,1026,1462,226,1163,225,1190,1576,170,1514,1656,742,1603,1406,1218,829,1266,1709,1487,477,1629,1327,172,152,153,256,253,161,255,254,167,166,165,177,189,192,194,198,199,200,202,245,247,261,183,191,190,237,241])).
% 59.88/59.97 cnf(2530,plain,
% 59.88/59.97 (P2(a16,a16,f3(a16,a16,a16),f3(a16,a16,a16))),
% 59.88/59.97 inference(scs_inference,[],[2345,2239,2335,2370,2113,2263,2269,2337,2364,2366,2368,2388,2398,2401,2415,2417,585,356,454,146,1367,1289,1545,171,1682,1026,1462,226,1163,225,1190,1576,170,1514,1656,742,1603,1406,1218,829,1266,1709,1487,477,1629,1327,172,152,153,256,253,161,255,254,167,166,165,177,189,192,194,198,199,200,202,245,247,261,183,191,190,237,241,263,185])).
% 59.88/59.97 cnf(2532,plain,
% 59.88/59.97 (P3(a19,a16,a19,a16)),
% 59.88/59.97 inference(scs_inference,[],[2345,2239,2335,2370,2113,2263,2269,2337,2364,2366,2368,2388,2398,2401,2415,2417,585,2271,356,454,146,1367,1289,1545,171,1682,1026,1462,226,1163,225,1190,1576,170,1514,1656,742,1603,1406,1218,829,1266,1709,1487,477,1629,1327,172,152,153,256,253,161,255,254,167,166,165,177,189,192,194,198,199,200,202,245,247,261,183,191,190,237,241,263,185,242])).
% 59.88/59.97 cnf(2537,plain,
% 59.88/59.97 (P5(a2,a2,a2,a2)),
% 59.88/59.97 inference(scs_inference,[],[2345,2239,2335,2370,2113,2263,2269,2337,2364,2366,2368,2388,2398,2401,2415,2417,585,2271,356,454,146,1367,1289,1545,171,1682,1026,1462,226,1163,225,1190,1576,170,1514,1656,742,1603,1406,1218,829,1266,1709,1487,477,1629,1327,172,152,153,256,253,161,255,254,167,166,165,177,189,192,194,198,199,200,202,245,247,261,183,191,190,237,241,263,185,242,197,252])).
% 59.88/59.97 cnf(2539,plain,
% 59.88/59.97 (P5(a16,f3(a16,a16,a16),a16,a16)),
% 59.88/59.97 inference(scs_inference,[],[2345,2239,2335,2370,2113,2263,2269,2337,2364,2366,2368,2388,2398,2401,2415,2417,585,2271,356,454,146,1367,1289,1545,171,1682,1026,1462,226,1163,225,1190,1576,170,1514,1656,742,1603,1406,1218,829,1266,1709,1487,477,1629,1327,172,152,153,256,253,161,255,254,167,166,165,177,189,192,194,198,199,200,202,245,247,261,183,191,190,237,241,263,185,242,197,252,168])).
% 59.88/59.97 cnf(2541,plain,
% 59.88/59.97 (P5(a16,a16,f3(a16,a16,a16),a16)),
% 59.88/59.97 inference(scs_inference,[],[2345,2239,2335,2370,2113,2263,2269,2337,2364,2366,2368,2388,2398,2401,2415,2417,585,2271,356,454,146,1367,1289,1545,171,1682,1026,1462,226,1163,225,1190,1576,170,1514,1656,742,1603,1406,1218,829,1266,1709,1487,477,1629,1327,172,152,153,256,253,161,255,254,167,166,165,177,189,192,194,198,199,200,202,245,247,261,183,191,190,237,241,263,185,242,197,252,168,169])).
% 59.88/59.97 cnf(2549,plain,
% 59.88/59.97 (P10(a16,a16,a16,f3(a16,a16,a16))),
% 59.88/59.97 inference(scs_inference,[],[2345,2239,2335,2370,2113,2263,2269,2337,2364,2366,2368,2388,2398,2401,2415,2417,585,2271,356,454,146,1367,1289,1545,171,1682,1026,1462,226,1163,225,1190,1576,170,1514,1656,742,1603,1406,1218,829,1266,1709,1487,477,1629,1327,172,152,153,256,253,161,255,254,167,166,165,177,189,192,194,198,199,200,202,245,247,261,183,191,190,237,241,263,185,242,197,252,168,169,1408,1489,227,234])).
% 59.88/59.97 cnf(2561,plain,
% 59.88/59.97 (P4(a16,a16,a16,f3(a16,a16,a16),f3(a16,a16,a16),a16,f3(a16,a16,a16),f3(a16,a16,a16))),
% 59.88/59.97 inference(scs_inference,[],[2345,2239,2380,2335,2370,2113,2263,2269,2337,2364,2366,2368,2388,2398,2401,2415,2417,585,2271,356,454,146,1367,1289,1545,171,1682,1026,1462,226,1163,225,1190,1576,170,1514,1656,742,1603,1406,1218,829,1266,1709,1487,477,1629,1327,172,152,153,256,253,161,255,254,167,166,165,177,189,192,194,198,199,200,202,245,247,261,183,191,190,237,241,263,185,242,197,252,168,169,1408,1489,227,234,977,856,580,164,195,230])).
% 59.88/59.97 cnf(2563,plain,
% 59.88/59.97 (P1(f5(a19,a19,a16),a16,a19)),
% 59.88/59.97 inference(scs_inference,[],[2345,2239,2380,2335,2370,2113,2263,2269,2337,2364,2366,2368,2388,2398,2401,2415,2417,585,2271,356,454,146,1367,1289,1545,171,1682,1026,1462,226,1163,225,1190,1576,170,1514,1656,742,1603,1406,1218,829,1266,1709,1487,477,1629,1327,172,152,153,256,253,161,255,254,167,166,165,177,189,192,194,198,199,200,202,245,247,261,183,191,190,237,241,263,185,242,197,252,168,169,1408,1489,227,234,977,856,580,164,195,230,179])).
% 59.88/59.97 cnf(2567,plain,
% 59.88/59.97 (P3(a16,f3(a16,a16,a16),f3(a16,a16,a16),f3(a16,a16,a16))),
% 59.88/59.97 inference(scs_inference,[],[2345,2239,2380,2335,2370,2113,2263,2269,2337,2364,2366,2368,2388,2398,2401,2415,2417,585,2271,356,454,146,1367,1289,1545,171,1682,1026,1462,226,1163,225,1190,1576,170,1514,1656,742,1603,1406,1218,829,1266,1709,1487,477,1629,1327,172,152,153,256,253,161,255,254,167,166,165,177,189,192,194,198,199,200,202,245,247,261,183,191,190,237,241,263,185,242,197,252,168,169,1408,1489,227,234,977,856,580,164,195,230,179,178,173])).
% 59.88/59.97 cnf(2569,plain,
% 59.88/59.97 (P3(a2,a2,a2,a2)),
% 59.88/59.97 inference(scs_inference,[],[2345,2239,2380,2335,2370,2113,2263,2269,2337,2364,2366,2368,2388,2398,2401,2415,2417,585,2271,356,454,146,1367,1289,1545,171,1682,1026,1462,226,1163,225,1190,1576,170,1514,1656,742,1603,1406,1218,829,1266,1709,1487,477,1629,1327,172,152,153,256,253,161,255,254,167,166,165,177,189,192,194,198,199,200,202,245,247,261,183,191,190,237,241,263,185,242,197,252,168,169,1408,1489,227,234,977,856,580,164,195,230,179,178,173,182])).
% 59.88/59.97 cnf(2592,plain,
% 59.88/59.97 (P6(a1,a19,a19,f25(a18,a1,a19,a19))),
% 59.88/59.97 inference(scs_inference,[],[2532,2506,2549,2510,1489,168,169,1408,1289,1367,1545,1462,170])).
% 59.88/59.97 cnf(2636,plain,
% 59.88/59.97 (P4(x26361,x26362,x26363,x26364,x26362,x26361,x26363,x26364)),
% 59.88/59.97 inference(scs_inference,[],[2492,2307,2444,2532,2506,2549,2510,1489,168,169,1408,1289,1367,1545,1462,170,742,1603,1163,1514,227,1709,171,1682,856,977,1266,1629,1190,1487,225,829,1026,1656,1576,234,1218,226])).
% 59.88/59.97 cnf(2646,plain,
% 59.88/59.97 (P1(x26461,x26462,x26461)),
% 59.88/59.97 inference(scs_inference,[],[2492,2482,2307,2444,2522,2532,2506,2549,2510,1489,168,169,1408,1289,1367,1545,1462,170,742,1603,1163,1514,227,1709,171,1682,856,977,1266,1629,1190,1487,225,829,1026,1656,1576,234,1218,226,1327,477,172,1406,152])).
% 59.88/59.97 cnf(2652,plain,
% 59.88/59.97 (P10(a19,a16,a2,a17)),
% 59.88/59.97 inference(scs_inference,[],[2492,2482,2307,2444,2522,2532,2506,2549,2502,2510,1489,168,169,1408,1289,1367,1545,1462,170,742,1603,1163,1514,227,1709,171,1682,856,977,1266,1629,1190,1487,225,829,1026,1656,1576,234,1218,226,1327,477,172,1406,152,153,164,580])).
% 59.88/59.97 cnf(2654,plain,
% 59.88/59.97 (P4(x26541,x26542,x26541,x26542,x26543,x26544,x26543,x26544)),
% 59.88/59.97 inference(scs_inference,[],[2434,2492,2482,2307,2444,2522,2532,2506,2549,2502,2510,1489,168,169,1408,1289,1367,1545,1462,170,742,1603,1163,1514,227,1709,171,1682,856,977,1266,1629,1190,1487,225,829,1026,1656,1576,234,1218,226,1327,477,172,1406,152,153,164,580,256])).
% 59.88/59.97 cnf(2658,plain,
% 59.88/59.97 (P4(x26581,x26582,a2,a16,x26581,x26582,a2,a15)),
% 59.88/59.97 inference(scs_inference,[],[2434,2492,2482,2307,2444,2486,2522,2532,2506,2549,2502,2510,1489,168,169,1408,1289,1367,1545,1462,170,742,1603,1163,1514,227,1709,171,1682,856,977,1266,1629,1190,1487,225,829,1026,1656,1576,234,1218,226,1327,477,172,1406,152,153,164,580,256,161,253])).
% 59.88/59.97 cnf(2660,plain,
% 59.88/59.97 (P4(a2,a17,a17,a2,x26601,x26602,x26601,x26602)),
% 59.88/59.97 inference(scs_inference,[],[2434,2492,2482,2307,2444,2478,2486,2522,2532,2506,2549,2502,2510,1489,168,169,1408,1289,1367,1545,1462,170,742,1603,1163,1514,227,1709,171,1682,856,977,1266,1629,1190,1487,225,829,1026,1656,1576,234,1218,226,1327,477,172,1406,152,153,164,580,256,161,253,255])).
% 59.88/59.97 cnf(2664,plain,
% 59.88/59.97 (P3(a19,a16,a16,a19)),
% 59.88/59.97 inference(scs_inference,[],[2434,2492,2482,2307,2444,2478,2484,2486,2522,2532,2506,2549,2502,2510,1489,168,169,1408,1289,1367,1545,1462,170,742,1603,1163,1514,227,1709,171,1682,856,977,1266,1629,1190,1487,225,829,1026,1656,1576,234,1218,226,1327,477,172,1406,152,153,164,580,256,161,253,255,254,167])).
% 59.88/59.97 cnf(2666,plain,
% 59.88/59.97 (P3(a15,a16,a18,a17)),
% 59.88/59.97 inference(scs_inference,[],[2434,2492,2482,2307,2444,2478,2484,2486,2488,2522,2532,2506,2549,2502,2510,1489,168,169,1408,1289,1367,1545,1462,170,742,1603,1163,1514,227,1709,171,1682,856,977,1266,1629,1190,1487,225,829,1026,1656,1576,234,1218,226,1327,477,172,1406,152,153,164,580,256,161,253,255,254,167,166])).
% 59.88/59.97 cnf(2672,plain,
% 59.88/59.97 (P5(a2,a2,a2,f26(a2,a2,a2,a2,a2))),
% 59.88/59.97 inference(scs_inference,[],[2434,2492,2482,2307,2444,2478,2484,2486,2488,2522,2532,2537,2569,2506,2549,2539,2502,2510,1489,168,169,1408,1289,1367,1545,1462,170,742,1603,1163,1514,227,1709,171,1682,856,977,1266,1629,1190,1487,225,829,1026,1656,1576,234,1218,226,1327,477,172,1406,152,153,164,580,256,161,253,255,254,167,166,165,184,201])).
% 59.88/59.97 cnf(2675,plain,
% 59.88/59.97 (P4(x26751,x26752,x26753,x26754,x26751,x26752,x26753,x26754)),
% 59.88/59.97 inference(rename_variables,[],[2434])).
% 59.88/59.97 cnf(2678,plain,
% 59.88/59.97 (P4(x26781,x26782,x26783,x26784,x26781,x26782,x26783,x26784)),
% 59.88/59.97 inference(rename_variables,[],[2434])).
% 59.88/59.97 cnf(2680,plain,
% 59.88/59.97 (P3(f12(a2,a2,a2,x26801,x26801),a2,x26801,x26801)),
% 59.88/59.97 inference(scs_inference,[],[2434,2675,2492,2482,2307,2444,2478,2484,2486,2488,2522,2532,2537,2569,2506,2549,2539,2502,2498,2510,1489,168,169,1408,1289,1367,1545,1462,170,742,1603,1163,1514,227,1709,171,1682,856,977,1266,1629,1190,1487,225,829,1026,1656,1576,234,1218,226,1327,477,172,1406,152,153,164,580,256,161,253,255,254,167,166,165,184,201,243,246,199])).
% 59.88/59.97 cnf(2681,plain,
% 59.88/59.97 (P1(x26811,x26812,x26812)),
% 59.88/59.97 inference(rename_variables,[],[2482])).
% 59.88/59.97 cnf(2686,plain,
% 59.88/59.97 (P10(x26861,x26862,x26862,x26861)),
% 59.88/59.97 inference(rename_variables,[],[2492])).
% 59.88/59.97 cnf(2693,plain,
% 59.88/59.97 (P4(x26931,x26932,x26933,x26934,x26931,x26932,x26933,x26934)),
% 59.88/59.97 inference(rename_variables,[],[2434])).
% 59.88/59.97 cnf(2696,plain,
% 59.88/59.97 (P4(x26961,x26962,x26963,x26964,x26961,x26962,x26963,x26964)),
% 59.88/59.97 inference(rename_variables,[],[2434])).
% 59.88/59.97 cnf(2703,plain,
% 59.88/59.97 (P4(x27031,x27032,x27033,x27034,x27031,x27032,x27033,x27034)),
% 59.88/59.97 inference(rename_variables,[],[2434])).
% 59.88/59.97 cnf(2705,plain,
% 59.88/59.97 (P5(a2,a2,a2,f3(a2,a2,a2))),
% 59.88/59.97 inference(scs_inference,[],[2434,2675,2678,2693,2696,2492,2482,2307,2444,2478,2484,2486,2426,2488,2522,2532,2537,2569,2506,2524,2549,2539,2502,2498,2510,267,1489,168,169,1408,1289,1367,1545,1462,170,742,1603,1163,1514,227,1709,171,1682,856,977,1266,1629,1190,1487,225,829,1026,1656,1576,234,1218,226,1327,477,172,1406,152,153,164,580,256,161,253,255,254,167,166,165,184,201,243,246,199,177,180,192,202,261,245,190,191,247,189])).
% 59.88/59.97 cnf(2709,plain,
% 59.88/59.97 (P6(x27091,x27092,x27092,x27092)),
% 59.88/59.97 inference(scs_inference,[],[2434,2675,2678,2693,2696,2703,2492,2482,2681,2307,2444,2478,2484,2486,2426,2488,2522,2532,2537,2569,2506,2524,2549,2539,2502,2498,2510,267,1489,168,169,1408,1289,1367,1545,1462,170,742,1603,1163,1514,227,1709,171,1682,856,977,1266,1629,1190,1487,225,829,1026,1656,1576,234,1218,226,1327,477,172,1406,152,153,164,580,256,161,253,255,254,167,166,165,184,201,243,246,199,177,180,192,202,261,245,190,191,247,189,194,237])).
% 59.88/59.97 cnf(2710,plain,
% 59.88/59.97 (P4(x27101,x27102,x27103,x27104,x27101,x27102,x27103,x27104)),
% 59.88/59.97 inference(rename_variables,[],[2434])).
% 59.88/59.97 cnf(2711,plain,
% 59.88/59.97 (P1(x27111,x27112,x27112)),
% 59.88/59.97 inference(rename_variables,[],[2482])).
% 59.88/59.97 cnf(2714,plain,
% 59.88/59.97 (P4(x27141,x27142,a2,a15,x27141,x27142,a2,a16)),
% 59.88/59.97 inference(rename_variables,[],[2486])).
% 59.88/59.97 cnf(2717,plain,
% 59.88/59.97 (P2(a2,a2,a2,a2)),
% 59.88/59.97 inference(scs_inference,[],[2434,2675,2678,2693,2696,2703,2492,2482,2681,2307,2444,2478,2484,2486,2426,2488,2522,2532,2537,2569,2506,2524,2549,2539,2502,2498,2510,1387,267,1489,168,169,1408,1289,1367,1545,1462,170,742,1603,1163,1514,227,1709,171,1682,856,977,1266,1629,1190,1487,225,829,1026,1656,1576,234,1218,226,1327,477,172,1406,152,153,164,580,256,161,253,255,254,167,166,165,184,201,243,246,199,177,180,192,202,261,245,190,191,247,189,194,237,263,185])).
% 59.88/59.97 cnf(2721,plain,
% 59.88/59.97 (P8(f3(a16,a16,a16),f3(a16,a16,a16),f3(a16,a16,a16))),
% 59.88/59.97 inference(scs_inference,[],[2434,2675,2678,2693,2696,2703,2710,2492,2482,2681,2711,2307,2444,2478,2484,2486,2426,2488,2522,2532,2537,2569,2506,2524,2530,2549,2541,2539,2502,2498,2510,1387,267,1489,168,169,1408,1289,1367,1545,1462,170,742,1603,1163,1514,227,1709,171,1682,856,977,1266,1629,1190,1487,225,829,1026,1656,1576,234,1218,226,1327,477,172,1406,152,153,164,580,256,161,253,255,254,167,166,165,184,201,243,246,199,177,180,192,202,261,245,190,191,247,189,194,237,263,185,182,240])).
% 59.88/59.97 cnf(2726,plain,
% 59.88/59.97 (P10(x27261,x27262,x27262,x27261)),
% 59.88/59.97 inference(rename_variables,[],[2492])).
% 59.88/59.97 cnf(2729,plain,
% 59.88/59.97 (P10(x27291,x27292,x27292,x27291)),
% 59.88/59.97 inference(rename_variables,[],[2492])).
% 59.88/59.97 cnf(2731,plain,
% 59.88/59.97 (P5(f3(a16,a16,a16),f3(a16,a16,a16),f3(a16,a16,a16),f3(a16,a16,a16))),
% 59.88/59.97 inference(scs_inference,[],[142,2434,2675,2678,2693,2696,2703,2710,2492,2686,2726,2482,2681,2711,2307,2444,2478,2484,2486,2426,2488,2522,2532,2537,2569,2506,2524,2530,2549,2541,2539,2502,2498,2510,1387,2101,267,1489,168,169,1408,1289,1367,1545,1462,170,742,1603,1163,1514,227,1709,171,1682,856,977,1266,1629,1190,1487,225,829,1026,1656,1576,234,1218,226,1327,477,172,1406,152,153,164,580,256,161,253,255,254,167,166,165,184,201,243,246,199,177,180,192,202,261,245,190,191,247,189,194,237,263,185,182,240,207,208,157])).
% 59.88/59.97 cnf(2733,plain,
% 59.88/59.97 (P3(f7(a2,a2,a2,a2),a2,a2,a2)),
% 59.88/59.97 inference(scs_inference,[],[142,2434,2675,2678,2693,2696,2703,2710,2492,2686,2726,2482,2681,2711,2307,2444,2478,2484,2486,2426,2488,2522,2532,2537,2569,2506,2524,2530,2549,2541,2539,2502,2498,2510,1387,2101,267,1489,168,169,1408,1289,1367,1545,1462,170,742,1603,1163,1514,227,1709,171,1682,856,977,1266,1629,1190,1487,225,829,1026,1656,1576,234,1218,226,1327,477,172,1406,152,153,164,580,256,161,253,255,254,167,166,165,184,201,243,246,199,177,180,192,202,261,245,190,191,247,189,194,237,263,185,182,240,207,208,157,188])).
% 59.88/59.97 cnf(2741,plain,
% 59.88/59.97 (P10(a16,a2,a2,a15)),
% 59.88/59.97 inference(scs_inference,[],[142,2434,2675,2678,2693,2696,2703,2710,2492,2686,2726,2729,2482,2681,2711,2307,2444,2478,2484,2486,2714,2426,2488,2522,2532,2537,2569,2506,2567,2524,2530,2549,2541,2539,2508,2502,2498,2510,1317,1387,2101,267,1489,168,169,1408,1289,1367,1545,1462,170,742,1603,1163,1514,227,1709,171,1682,856,977,1266,1629,1190,1487,225,829,1026,1656,1576,234,1218,226,1327,477,172,1406,152,153,164,580,256,161,253,255,254,167,166,165,184,201,243,246,199,177,180,192,202,261,245,190,191,247,189,194,237,263,185,182,240,207,208,157,188,222,174,231,241])).
% 59.88/59.97 cnf(2745,plain,
% 59.88/59.97 (P3(a17,a2,a17,a2)),
% 59.88/59.97 inference(scs_inference,[],[142,2434,2675,2678,2693,2696,2703,2710,2492,2686,2726,2729,2482,2681,2711,2307,2444,2478,2484,2486,2714,2426,2488,2522,2532,2537,2569,2506,2567,2524,2530,2549,2541,2539,2508,2502,2498,2510,1317,1387,2101,267,1489,168,169,1408,1289,1367,1545,1462,170,742,1603,1163,1514,227,1709,171,1682,856,977,1266,1629,1190,1487,225,829,1026,1656,1576,234,1218,226,1327,477,172,1406,152,153,164,580,256,161,253,255,254,167,166,165,184,201,243,246,199,177,180,192,202,261,245,190,191,247,189,194,237,263,185,182,240,207,208,157,188,222,174,231,241,242])).
% 59.88/59.97 cnf(2752,plain,
% 59.88/59.97 (P4(x27521,x27522,x27521,x27522,x27523,x27524,x27523,x27524)),
% 59.88/59.97 inference(rename_variables,[],[2654])).
% 59.88/59.97 cnf(2755,plain,
% 59.88/59.97 (P4(x27551,x27552,x27551,x27552,x27553,x27554,x27553,x27554)),
% 59.88/59.97 inference(rename_variables,[],[2654])).
% 59.88/59.97 cnf(2758,plain,
% 59.88/59.97 (P4(x27581,x27582,x27583,x27584,x27582,x27581,x27583,x27584)),
% 59.88/59.97 inference(rename_variables,[],[2636])).
% 59.88/59.97 cnf(2761,plain,
% 59.88/59.97 (P4(x27611,x27612,x27613,x27614,x27612,x27611,x27613,x27614)),
% 59.88/59.97 inference(rename_variables,[],[2636])).
% 59.88/59.97 cnf(2773,plain,
% 59.88/59.97 (P6(a19,a19,a17,a19)),
% 59.88/59.97 inference(scs_inference,[],[2636,2758,2654,2752,2311,2652,2672,635,934,577,657,168,169,1545,1289,1514,171])).
% 59.88/59.97 cnf(2775,plain,
% 59.88/59.97 (P6(x27751,x27752,x27751,x27751)),
% 59.88/59.97 inference(scs_inference,[],[2636,2758,2654,2752,2709,2311,2652,2672,635,934,577,657,168,169,1545,1289,1514,171,170])).
% 59.88/59.97 cnf(2821,plain,
% 59.88/59.97 (P6(a1,a19,f25(a18,a1,a19,a19),a19)),
% 59.88/59.97 inference(scs_inference,[],[2636,2758,2654,2752,2709,2311,2652,2741,2672,2592,635,934,577,657,168,169,1545,1289,1514,171,170,1190,1629,1682,829,1367,742,1487,227,1576,1266,234,1603,1462,1026,1709,1218,225,1163,977,1656,1406,1327,172])).
% 59.88/59.97 cnf(2827,plain,
% 59.88/59.97 (P1(a15,a2,a16)),
% 59.88/59.97 inference(scs_inference,[],[2636,2758,2654,2752,2709,2476,2311,2652,2741,2672,2592,635,934,577,657,168,169,1545,1289,1514,171,170,1190,1629,1682,829,1367,742,1487,227,1576,1266,234,1603,1462,1026,1709,1218,225,1163,977,1656,1406,1327,172,477,856,152])).
% 59.88/59.97 cnf(2829,plain,
% 59.88/59.97 (P4(a19,a16,x28291,x28292,a2,a17,x28291,x28292)),
% 59.88/59.97 inference(scs_inference,[],[2636,2758,2654,2752,2709,2476,2311,2652,2741,2672,2592,635,934,577,657,168,169,1545,1289,1514,171,170,1190,1629,1682,829,1367,742,1487,227,1576,1266,234,1603,1462,1026,1709,1218,225,1163,977,1656,1406,1327,172,477,856,152,226])).
% 59.88/59.97 cnf(2831,plain,
% 59.88/59.97 (P1(x28311,x28311,x28312)),
% 59.88/59.97 inference(scs_inference,[],[2636,2758,2654,2752,2709,2646,2476,2311,2652,2741,2672,2592,635,934,577,657,168,169,1545,1289,1514,171,170,1190,1629,1682,829,1367,742,1487,227,1576,1266,234,1603,1462,1026,1709,1218,225,1163,977,1656,1406,1327,172,477,856,152,226,153])).
% 59.88/59.97 cnf(2835,plain,
% 59.88/59.97 (P4(x28351,x28352,x28352,x28351,x28353,x28354,x28353,x28354)),
% 59.88/59.97 inference(scs_inference,[],[2636,2758,2761,2654,2752,2709,2646,2476,2311,2652,2741,2672,2592,635,934,577,657,168,169,1545,1289,1514,171,170,1190,1629,1682,829,1367,742,1487,227,1576,1266,234,1603,1462,1026,1709,1218,225,1163,977,1656,1406,1327,172,477,856,152,226,153,164,256])).
% 59.88/59.97 cnf(2841,plain,
% 59.88/59.97 (P4(x28411,x28412,x28413,x28414,x28411,x28412,x28414,x28413)),
% 59.88/59.97 inference(scs_inference,[],[2636,2758,2761,2654,2752,2709,2646,2476,2658,2660,2311,2652,2741,2672,2592,635,934,577,657,168,169,1545,1289,1514,171,170,1190,1629,1682,829,1367,742,1487,227,1576,1266,234,1603,1462,1026,1709,1218,225,1163,977,1656,1406,1327,172,477,856,152,226,153,164,256,253,255,254])).
% 59.88/59.97 cnf(2843,plain,
% 59.88/59.97 (P3(a15,a16,a17,a18)),
% 59.88/59.97 inference(scs_inference,[],[2636,2758,2761,2654,2752,2709,2646,2476,2658,2660,2311,2652,2666,2741,2672,2592,635,934,577,657,168,169,1545,1289,1514,171,170,1190,1629,1682,829,1367,742,1487,227,1576,1266,234,1603,1462,1026,1709,1218,225,1163,977,1656,1406,1327,172,477,856,152,226,153,164,256,253,255,254,167])).
% 59.88/59.97 cnf(2845,plain,
% 59.88/59.97 (P3(a16,a19,a19,a16)),
% 59.88/59.97 inference(scs_inference,[],[2636,2758,2761,2654,2752,2709,2646,2476,2658,2660,2311,2652,2664,2666,2741,2672,2592,635,934,577,657,168,169,1545,1289,1514,171,170,1190,1629,1682,829,1367,742,1487,227,1576,1266,234,1603,1462,1026,1709,1218,225,1163,977,1656,1406,1327,172,477,856,152,226,153,164,256,253,255,254,167,166])).
% 59.88/59.97 cnf(2847,plain,
% 59.88/59.97 (P10(a19,a16,a17,a2)),
% 59.88/59.97 inference(scs_inference,[],[2636,2758,2761,2654,2752,2709,2646,2476,2658,2660,2311,2652,2664,2666,2741,2672,2592,635,934,577,657,168,169,1545,1289,1514,171,170,1190,1629,1682,829,1367,742,1487,227,1576,1266,234,1603,1462,1026,1709,1218,225,1163,977,1656,1406,1327,172,477,856,152,226,153,164,256,253,255,254,167,166,165])).
% 59.88/59.97 cnf(2850,plain,
% 59.88/59.97 (P1(x28501,x28502,x28501)),
% 59.88/59.97 inference(rename_variables,[],[2646])).
% 59.88/59.97 cnf(2853,plain,
% 59.88/59.97 (P10(x28531,x28532,x28532,x28531)),
% 59.88/59.97 inference(rename_variables,[],[2492])).
% 59.88/59.97 cnf(2855,plain,
% 59.88/59.97 (P2(f8(a2,a2,a2),a2,a2,a2)),
% 59.88/59.97 inference(scs_inference,[],[2636,2758,2761,2654,2752,2709,2646,2476,2658,2660,2311,2652,2664,2666,2741,2672,2592,2492,2569,635,934,577,657,168,169,1545,1289,1514,171,170,1190,1629,1682,829,1367,742,1487,227,1576,1266,234,1603,1462,1026,1709,1218,225,1163,977,1656,1406,1327,172,477,856,152,226,153,164,256,253,255,254,167,166,165,198,180,192])).
% 59.88/59.97 cnf(2856,plain,
% 59.88/59.97 (P6(x28561,x28562,x28562,x28562)),
% 59.88/59.97 inference(rename_variables,[],[2709])).
% 59.88/59.97 cnf(2858,plain,
% 59.88/59.97 (P3(f12(a19,a19,a16,x28581,a19),a19,x28581,a19)),
% 59.88/59.97 inference(scs_inference,[],[2636,2758,2761,2654,2752,2709,2646,2850,2476,2658,2660,2311,2652,2664,2666,2741,2672,2592,2492,2569,635,934,577,657,168,169,1545,1289,1514,171,170,1190,1629,1682,829,1367,742,1487,227,1576,1266,234,1603,1462,1026,1709,1218,225,1163,977,1656,1406,1327,172,477,856,152,226,153,164,256,253,255,254,167,166,165,198,180,192,199])).
% 59.88/59.97 cnf(2859,plain,
% 59.88/59.97 (P1(x28591,x28592,x28591)),
% 59.88/59.97 inference(rename_variables,[],[2646])).
% 59.88/59.97 cnf(2864,plain,
% 59.88/59.97 (P4(x28641,x28642,x28643,x28644,x28641,x28642,x28643,x28644)),
% 59.88/59.97 inference(rename_variables,[],[2434])).
% 59.88/59.97 cnf(2866,plain,
% 59.88/59.97 (P4(a1,a19,a18,a19,a1,f25(a1,a18,a19,a19),a18,f25(a1,a18,a19,a19))),
% 59.88/59.97 inference(scs_inference,[],[2636,2758,2761,2654,2752,2709,2646,2850,2476,2658,2660,2311,2652,2664,2666,2741,2745,2672,2592,2434,2864,2492,318,2569,635,934,577,657,168,169,1545,1289,1514,171,170,1190,1629,1682,829,1367,742,1487,227,1576,1266,234,1603,1462,1026,1709,1218,225,1163,977,1656,1406,1327,172,477,856,152,226,153,164,256,253,255,254,167,166,165,198,180,192,199,190,245,261])).
% 59.88/59.97 cnf(2875,plain,
% 59.88/59.97 (P10(a16,a19,a2,a17)),
% 59.88/59.97 inference(scs_inference,[],[2636,2758,2761,2654,2752,2709,2646,2850,2476,2658,2660,2311,2652,2664,2666,2741,2745,2672,2592,2434,2864,2492,318,2569,635,934,577,657,168,169,1545,1289,1514,171,170,1190,1629,1682,829,1367,742,1487,227,1576,1266,234,1603,1462,1026,1709,1218,225,1163,977,1656,1406,1327,172,477,856,152,226,153,164,256,253,255,254,167,166,165,198,180,192,199,190,245,261,179,191,178,241])).
% 59.88/59.97 cnf(2876,plain,
% 59.88/59.97 (P4(x28761,x28762,x28763,x28764,x28762,x28761,x28763,x28764)),
% 59.88/59.97 inference(rename_variables,[],[2636])).
% 59.88/59.97 cnf(2879,plain,
% 59.88/59.97 (P4(x28791,x28792,x28793,x28794,x28792,x28791,x28793,x28794)),
% 59.88/59.97 inference(rename_variables,[],[2636])).
% 59.88/59.97 cnf(2882,plain,
% 59.88/59.97 (P4(x28821,x28822,x28821,x28822,x28823,x28824,x28823,x28824)),
% 59.88/59.97 inference(rename_variables,[],[2654])).
% 59.88/59.97 cnf(2886,plain,
% 59.88/59.97 (P3(a16,a19,a16,a19)),
% 59.88/59.97 inference(scs_inference,[],[142,2636,2758,2761,2876,2879,2654,2752,2755,2709,2646,2850,2476,2658,2660,2291,2311,2652,2664,2666,2741,2745,2731,2672,2592,2434,2864,2492,318,2569,635,934,577,657,168,169,1545,1289,1514,171,170,1190,1629,1682,829,1367,742,1487,227,1576,1266,234,1603,1462,1026,1709,1218,225,1163,977,1656,1406,1327,172,477,856,152,226,153,164,256,253,255,254,167,166,165,198,180,192,199,190,245,261,179,191,178,241,263,237,185,242])).
% 59.88/59.97 cnf(2887,plain,
% 59.88/59.97 (P4(x28871,x28872,x28873,x28874,x28872,x28871,x28873,x28874)),
% 59.88/59.97 inference(rename_variables,[],[2636])).
% 59.88/59.97 cnf(2891,plain,
% 59.88/59.97 (P9(a19,x28911,x28911,a19,a19,a19,a19,x28911)),
% 59.88/59.97 inference(scs_inference,[],[142,2636,2758,2761,2876,2879,2654,2752,2755,2709,2646,2850,2859,2476,2658,2660,2291,2311,2652,2664,2666,2741,2745,2731,2672,2592,2434,2864,2492,2853,318,2569,635,934,577,657,168,169,1545,1289,1514,171,170,1190,1629,1682,829,1367,742,1487,227,1576,1266,234,1603,1462,1026,1709,1218,225,1163,977,1656,1406,1327,172,477,856,152,226,153,164,256,253,255,254,167,166,165,198,180,192,199,190,245,261,179,191,178,241,263,237,185,242,182,229])).
% 59.88/59.97 cnf(2892,plain,
% 59.88/59.97 (P1(x28921,x28922,x28921)),
% 59.88/59.97 inference(rename_variables,[],[2646])).
% 59.88/59.97 cnf(2893,plain,
% 59.88/59.97 (P10(x28931,x28932,x28932,x28931)),
% 59.88/59.97 inference(rename_variables,[],[2492])).
% 59.88/59.97 cnf(2894,plain,
% 59.88/59.97 (~P1(x28941,x28942,x28943)+~P1(x28941,x28944,x28945)+P9(x28941,x28944,x28944,x28945,x28941,x28942,x28942,x28943)+~P10(x28944,x28942,x28945,x28943)),
% 59.88/59.97 inference(rename_variables,[],[229])).
% 59.88/59.97 cnf(2895,plain,
% 59.88/59.97 (P8(a2,a2,a2)),
% 59.88/59.97 inference(scs_inference,[],[142,2636,2758,2761,2876,2879,2887,2654,2752,2755,2709,2646,2850,2859,2892,2476,2658,2660,2291,2311,2652,2664,2666,2717,2741,2745,2731,2672,2592,2434,2864,2492,2853,318,2569,635,934,577,657,168,169,1545,1289,1514,171,170,1190,1629,1682,829,1367,742,1487,227,1576,1266,234,1603,1462,1026,1709,1218,225,1163,977,1656,1406,1327,172,477,856,152,226,153,164,256,253,255,254,167,166,165,198,180,192,199,190,245,261,179,191,178,241,263,237,185,242,182,229,240])).
% 59.88/59.97 cnf(2896,plain,
% 59.88/59.97 (P4(x28961,x28962,x28963,x28964,x28962,x28961,x28963,x28964)),
% 59.88/59.97 inference(rename_variables,[],[2636])).
% 59.88/59.97 cnf(2897,plain,
% 59.88/59.97 (P1(x28971,x28972,x28971)),
% 59.88/59.97 inference(rename_variables,[],[2646])).
% 59.88/59.97 cnf(2899,plain,
% 59.88/59.97 (P8(f20(a2,x28991),a2,x28991)),
% 59.88/59.97 inference(scs_inference,[],[142,2636,2758,2761,2876,2879,2887,2654,2752,2755,2709,2646,2850,2859,2892,2897,2476,2658,2660,2291,2311,2652,2664,2666,2717,2741,2745,2731,2672,2592,2434,2864,2492,2853,318,2569,635,934,577,657,168,169,1545,1289,1514,171,170,1190,1629,1682,829,1367,742,1487,227,1576,1266,234,1603,1462,1026,1709,1218,225,1163,977,1656,1406,1327,172,477,856,152,226,153,164,256,253,255,254,167,166,165,198,180,192,199,190,245,261,179,191,178,241,263,237,185,242,182,229,240,160])).
% 59.88/59.97 cnf(2900,plain,
% 59.88/59.97 (P1(x29001,x29002,x29001)),
% 59.88/59.97 inference(rename_variables,[],[2646])).
% 59.88/59.97 cnf(2903,plain,
% 59.88/59.97 (P1(x29031,x29032,x29031)),
% 59.88/59.97 inference(rename_variables,[],[2646])).
% 59.88/59.97 cnf(2904,plain,
% 59.88/59.97 (P10(x29041,x29042,x29042,x29041)),
% 59.88/59.97 inference(rename_variables,[],[2492])).
% 59.88/59.97 cnf(2906,plain,
% 59.88/59.97 (P5(x29061,x29061,x29061,x29061)),
% 59.88/59.97 inference(scs_inference,[],[142,2636,2758,2761,2876,2879,2887,2896,2654,2752,2755,2709,2856,2646,2850,2859,2892,2897,2900,2476,2658,2660,2291,2311,2652,2664,2666,2717,2741,2745,2731,2672,2592,2121,2434,2864,2492,2853,2893,318,2569,635,934,577,657,168,169,1545,1289,1514,171,170,1190,1629,1682,829,1367,742,1487,227,1576,1266,234,1603,1462,1026,1709,1218,225,1163,977,1656,1406,1327,172,477,856,152,226,153,164,256,253,255,254,167,166,165,198,180,192,199,190,245,261,179,191,178,241,263,237,185,242,182,229,240,160,208,252])).
% 59.88/59.97 cnf(2909,plain,
% 59.88/59.97 (P6(x29091,x29092,x29092,x29092)),
% 59.88/59.97 inference(rename_variables,[],[2709])).
% 59.88/59.97 cnf(2912,plain,
% 59.88/59.97 (P9(a19,a19,a19,x29121,a19,x29121,x29121,a19)),
% 59.88/59.97 inference(scs_inference,[],[142,2636,2758,2761,2876,2879,2887,2896,2654,2752,2755,2709,2856,2646,2850,2859,2892,2897,2900,2476,2658,2660,2291,2311,2652,2664,2666,2717,2741,2745,2731,2672,2592,2121,2434,2864,2492,2853,2893,318,2569,635,934,577,657,168,169,1545,1289,1514,171,170,1190,1629,1682,829,1367,742,1487,227,1576,1266,234,1603,1462,1026,1709,1218,225,1163,977,1656,1406,1327,172,477,856,152,226,153,164,256,253,255,254,167,166,165,198,180,192,199,190,245,261,179,191,178,241,263,237,185,242,182,229,240,160,208,252,257])).
% 59.88/59.97 cnf(2914,plain,
% 59.88/59.97 (P9(x29141,a19,a19,x29141,a19,x29141,a19,a19)),
% 59.88/59.97 inference(scs_inference,[],[142,2636,2758,2761,2876,2879,2887,2896,2654,2752,2755,2709,2856,2646,2850,2859,2892,2897,2900,2476,2658,2660,2291,2311,2652,2664,2666,2717,2741,2745,2731,2672,2592,2121,2434,2864,2492,2853,2893,318,2569,635,934,577,657,168,169,1545,1289,1514,171,170,1190,1629,1682,829,1367,742,1487,227,1576,1266,234,1603,1462,1026,1709,1218,225,1163,977,1656,1406,1327,172,477,856,152,226,153,164,256,253,255,254,167,166,165,198,180,192,199,190,245,261,179,191,178,241,263,237,185,242,182,229,240,160,208,252,257,258])).
% 59.88/59.97 cnf(2916,plain,
% 59.88/59.97 (P9(x29161,a19,x29161,a19,a19,a19,a19,x29161)),
% 59.88/59.97 inference(scs_inference,[],[142,2636,2758,2761,2876,2879,2887,2896,2654,2752,2755,2709,2856,2646,2850,2859,2892,2897,2900,2476,2658,2660,2291,2311,2652,2664,2666,2717,2741,2745,2731,2672,2592,2121,2434,2864,2492,2853,2893,318,2569,635,934,577,657,168,169,1545,1289,1514,171,170,1190,1629,1682,829,1367,742,1487,227,1576,1266,234,1603,1462,1026,1709,1218,225,1163,977,1656,1406,1327,172,477,856,152,226,153,164,256,253,255,254,167,166,165,198,180,192,199,190,245,261,179,191,178,241,263,237,185,242,182,229,240,160,208,252,257,258,259])).
% 59.88/59.97 cnf(2924,plain,
% 59.88/59.97 (P8(f20(a2,x29241),x29241,a2)),
% 59.88/59.97 inference(scs_inference,[],[142,2636,2758,2761,2876,2879,2887,2896,2654,2752,2755,2709,2856,2646,2850,2859,2892,2897,2900,2476,2658,2660,2291,2311,2652,2664,2666,2717,2741,2745,2731,2672,2592,2121,2434,2864,2492,2853,2893,318,2569,635,934,577,657,168,169,1545,1289,1514,171,170,1190,1629,1682,829,1367,742,1487,227,1576,1266,234,1603,1462,1026,1709,1218,225,1163,977,1656,1406,1327,172,477,856,152,226,153,164,256,253,255,254,167,166,165,198,180,192,199,190,245,261,179,191,178,241,263,237,185,242,182,229,240,160,208,252,257,258,259,260,1489,157,155])).
% 59.88/59.97 cnf(2951,plain,
% 59.88/59.97 (P5(a19,a19,a19,f26(a19,a16,a19,a19,a19))),
% 59.88/59.97 inference(scs_inference,[],[142,2636,2758,2761,2876,2879,2887,2896,2654,2752,2755,2882,2709,2856,2646,2850,2859,2892,2897,2900,2476,2658,2660,2291,2311,2652,2664,2666,2717,2741,2745,2731,2672,2592,2121,2434,2864,2492,2853,2893,354,318,2569,635,934,577,657,168,169,1545,1289,1514,171,170,1190,1629,1682,829,1367,742,1487,227,1576,1266,234,1603,1462,1026,1709,1218,225,1163,977,1656,1406,1327,172,477,856,152,226,153,164,256,253,255,254,167,166,165,198,180,192,199,190,245,261,179,191,178,241,263,237,185,242,182,229,240,160,208,252,257,258,259,260,1489,157,155,1408,154,224,204,221,205,159,235,201,158,181,202,200])).
% 59.88/59.97 cnf(2956,plain,
% 59.88/59.97 (P8(a2,a15,a16)),
% 59.88/59.97 inference(scs_inference,[],[142,2636,2758,2761,2876,2879,2887,2896,2654,2752,2755,2882,2709,2856,2646,2850,2859,2892,2897,2900,2476,2658,2660,2291,2311,2652,2664,2666,2717,2741,2745,2731,2672,2680,2592,2121,2434,2864,2492,2853,2893,354,318,2125,2569,2129,635,934,577,657,168,169,1545,1289,1514,171,170,1190,1629,1682,829,1367,742,1487,227,1576,1266,234,1603,1462,1026,1709,1218,225,1163,977,1656,1406,1327,172,477,856,152,226,153,164,256,253,255,254,167,166,165,198,180,192,199,190,245,261,179,191,178,241,263,237,185,242,182,229,240,160,208,252,257,258,259,260,1489,157,155,1408,154,224,204,221,205,159,235,201,158,181,202,200,174,176])).
% 59.88/59.97 cnf(2964,plain,
% 59.88/59.97 (P8(x29641,f3(a16,a16,a16),x29641)),
% 59.88/59.97 inference(scs_inference,[],[142,2636,2758,2761,2876,2879,2887,2896,2654,2752,2755,2882,2709,2856,2909,2646,2850,2859,2892,2897,2900,2903,2476,2658,2660,2291,2311,2652,2664,2666,2717,2741,2745,2721,2731,2672,2680,2592,2121,2434,2864,2492,2853,2893,2904,354,318,2345,2125,2569,2129,635,934,577,657,168,169,1545,1289,1514,171,170,1190,1629,1682,829,1367,742,1487,227,1576,1266,234,1603,1462,1026,1709,1218,225,1163,977,1656,1406,1327,172,477,856,152,226,153,164,256,253,255,254,167,166,165,198,180,192,199,190,245,261,179,191,178,241,263,237,185,242,182,229,240,160,208,252,257,258,259,260,1489,157,155,1408,154,224,204,221,205,159,235,201,158,181,202,200,174,176,2894,193,163])).
% 59.88/59.97 cnf(2974,plain,
% 59.88/59.97 (P4(x29741,x29742,x29743,x29744,x29741,x29742,x29744,x29743)),
% 59.88/59.97 inference(rename_variables,[],[2841])).
% 59.88/59.97 cnf(2981,plain,
% 59.88/59.97 (P4(x29811,x29812,x29813,x29814,x29811,x29812,x29814,x29813)),
% 59.88/59.97 inference(rename_variables,[],[2841])).
% 59.88/59.97 cnf(2984,plain,
% 59.88/59.97 (P4(x29841,x29842,x29843,x29844,x29841,x29842,x29844,x29843)),
% 59.88/59.97 inference(rename_variables,[],[2841])).
% 59.88/59.97 cnf(3095,plain,
% 59.88/59.97 (P1(x30951,x30951,x30952)),
% 59.88/59.97 inference(rename_variables,[],[2831])).
% 59.88/59.97 cnf(3098,plain,
% 59.88/59.97 (P1(x30981,x30981,x30982)),
% 59.88/59.97 inference(rename_variables,[],[2831])).
% 59.88/59.97 cnf(3118,plain,
% 59.88/59.97 (P1(x31181,x31181,x31182)),
% 59.88/59.97 inference(rename_variables,[],[2831])).
% 59.88/59.97 cnf(3139,plain,
% 59.88/59.97 (~P1(a19,a19,a1)),
% 59.88/59.97 inference(scs_inference,[],[2906,2775,2835,2841,2974,2981,2984,2831,3095,3098,3118,2875,2847,2829,2891,2912,2914,2916,2773,2827,2843,2845,2886,2895,2956,2964,2733,2705,2563,2899,2924,2561,2858,2821,2951,2866,2855,616,1385,2388,2524,2482,431,356,2569,577,258,259,657,715,260,257,168,157,169,1514,170,1545,1289,155,1487,1629,1367,1682,227,1026,1709,1218,742,977,225,1603,1576,1406,829,1190,1163,171,1462,234,152,226,1656,1266,856,154,172,164,1327,477,153,253,256,254,255,167,166,165,206,264,224,204,228,198,162,205,244,159,192,230,158,181,199,174,190,191,179,178,241,263,237,156])).
% 59.88/59.97 cnf(3228,plain,
% 59.88/59.97 ($false),
% 59.88/59.97 inference(scs_inference,[],[3139,2831]),
% 59.88/59.97 ['proof']).
% 59.88/59.97 % SZS output end Proof
% 59.88/59.97 % Total time :59.330000s
%------------------------------------------------------------------------------