%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : GEO609+1 : TPTP v8.2.0. Released v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% Computer : n017.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Mon Jun 24 06:05:55 EDT 2024
% Result : Theorem 60.62s 60.68s
% Output : CNFRefutation 60.70s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.12/0.12 % Problem : GEO609+1 : TPTP v8.2.0. Released v7.5.0.
% 0.12/0.12 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% 0.12/0.33 % Computer : n017.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 300
% 0.12/0.33 % DateTime : Fri Jun 21 08:15:24 EDT 2024
% 0.12/0.33 % CPUTime :
% 0.20/0.56 start to proof:theBenchmark
% 60.62/60.67 %-------------------------------------------
% 60.62/60.67 % File :CSE---1.7
% 60.62/60.67 % Problem :theBenchmark
% 60.62/60.67 % Transform :cnf
% 60.62/60.67 % Format :tptp:raw
% 60.62/60.67 % Command :java -jar mcs_scs.jar %d %s
% 60.62/60.67
% 60.62/60.67 % Result :Theorem 60.050000s
% 60.62/60.67 % Output :CNFRefutation 60.050000s
% 60.62/60.67 %-------------------------------------------
% 60.62/60.68 %------------------------------------------------------------------------------
% 60.62/60.68 % File : GEO609+1 : TPTP v8.2.0. Released v7.5.0.
% 60.62/60.68 % Domain : Geometry
% 60.62/60.68 % Problem : JGEX problem 71
% 60.62/60.68 % Version : [CGZ00] axioms.
% 60.62/60.68 % English :
% 60.62/60.68
% 60.62/60.68 % Refs : [CGZ00] Chou et al. (2000), A Deductive Database Approach to A
% 60.62/60.68 % : [YCG08] Ye et al. (2008), An Introduction to Java Geometry Exp
% 60.62/60.68 % : [Qua20] Quaresma (2020), Email to Geoff Sutcliffe
% 60.62/60.68 % Source : [Qua20]
% 60.62/60.68 % Names : 71.p [Qua20]
% 60.62/60.68
% 60.62/60.68 % Status : Theorem
% 60.62/60.68 % Rating : 0.36 v8.1.0, 0.44 v7.5.0
% 60.62/60.68 % Syntax : Number of formulae : 95 ( 0 unt; 0 def)
% 60.62/60.68 % Number of atoms : 291 ( 1 equ)
% 60.62/60.68 % Maximal formula atoms : 8 ( 3 avg)
% 60.62/60.68 % Number of connectives : 203 ( 7 ~; 0 |; 101 &)
% 60.62/60.68 % ( 0 <=>; 95 =>; 0 <=; 0 <~>)
% 60.62/60.68 % Maximal formula depth : 16 ( 9 avg)
% 60.62/60.68 % Maximal term depth : 1 ( 1 avg)
% 60.62/60.68 % Number of predicates : 12 ( 11 usr; 0 prp; 2-8 aty)
% 60.62/60.68 % Number of functors : 0 ( 0 usr; 0 con; --- aty)
% 60.62/60.68 % Number of variables : 530 ( 510 !; 20 ?)
% 60.62/60.68 % SPC : FOF_THM_RFO_SEQ
% 60.62/60.68
% 60.62/60.68 % Comments : Taken from JGEX [YCG08], converted by Pedro Quaresma.
% 60.62/60.68 %------------------------------------------------------------------------------
% 60.62/60.68 include('Axioms/GEO012+0.ax').
% 60.62/60.68 %------------------------------------------------------------------------------
% 60.62/60.68 fof(exemplo6GDDFULL618071,conjecture,
% 60.62/60.68 ! [A,B,C,O,E,F,G,NWPNT1] :
% 60.62/60.68 ( ( circle(O,A,B,C)
% 60.62/60.68 & para(B,C,E,A)
% 60.62/60.68 & circle(O,A,E,NWPNT1)
% 60.62/60.68 & perp(F,E,A,B)
% 60.62/60.68 & coll(F,A,B)
% 60.62/60.68 & perp(G,E,A,C)
% 60.62/60.68 & coll(G,A,C) )
% 60.62/60.68 => para(F,G,A,O) ) ).
% 60.62/60.68
% 60.62/60.68 %------------------------------------------------------------------------------
% 60.62/60.68 %-------------------------------------------
% 60.62/60.68 % Proof found
% 60.62/60.68 % SZS status Theorem for theBenchmark
% 60.62/60.68 % SZS output start Proof
% 60.62/60.69 %ClaNum:262(EqnAxiom:141)
% 60.62/60.69 %VarNum:1613(SingletonVarNum:590)
% 60.62/60.69 %MaxLitNum:5
% 60.62/60.69 %MaxfuncDepth:1
% 60.62/60.69 %SharedTerms:16
% 60.62/60.69 %goalClause: 142 143 144 145 146 147 148 149
% 60.62/60.69 %singleGoalClaCount:8
% 60.62/60.69 [142]P1(a1,a2,a15)
% 60.62/60.69 [143]P1(a19,a2,a16)
% 60.62/60.69 [144]P3(a15,a16,a17,a2)
% 60.62/60.69 [145]P10(a1,a17,a2,a15)
% 60.62/60.69 [146]P10(a19,a17,a2,a16)
% 60.62/60.69 [147]P2(a18,a2,a15,a16)
% 60.62/60.69 [148]P2(a18,a2,a17,a20)
% 60.62/60.69 [149]~P3(a1,a19,a2,a18)
% 60.62/60.69 [150]~P1(x1502,x1501,x1503)+P1(x1501,x1502,x1503)
% 60.62/60.69 [151]~P1(x1511,x1513,x1512)+P1(x1511,x1512,x1513)
% 60.62/60.69 [152]~P4(x1521,x1522,x1523)+P1(x1521,x1522,x1523)
% 60.62/60.69 [153]~P4(x1531,x1533,x1532)+P4(x1531,x1532,x1533)
% 60.62/60.69 [155]~P4(x1551,x1552,x1553)+P5(x1551,x1552,x1551,x1553)
% 60.62/60.69 [159]~P3(x1591,x1592,x1591,x1593)+P1(x1591,x1592,x1593)
% 60.62/60.69 [225]~P5(x2251,x2252,x2251,x2253)+P9(x2251,x2252,x2252,x2253,x2252,x2253,x2251,x2253)
% 60.62/60.69 [162]~P3(x1623,x1624,x1621,x1622)+P3(x1621,x1622,x1623,x1624)
% 60.62/60.69 [163]~P3(x1631,x1632,x1634,x1633)+P3(x1631,x1632,x1633,x1634)
% 60.62/60.69 [164]~P10(x1643,x1644,x1641,x1642)+P10(x1641,x1642,x1643,x1644)
% 60.62/60.69 [165]~P10(x1651,x1652,x1654,x1653)+P10(x1651,x1652,x1653,x1654)
% 60.62/60.69 [166]~P5(x1663,x1664,x1661,x1662)+P5(x1661,x1662,x1663,x1664)
% 60.62/60.69 [167]~P5(x1671,x1672,x1674,x1673)+P5(x1671,x1672,x1673,x1674)
% 60.62/60.69 [168]~P6(x1682,x1681,x1683,x1684)+P6(x1681,x1682,x1683,x1684)
% 60.62/60.69 [169]~P6(x1691,x1693,x1692,x1694)+P6(x1691,x1692,x1693,x1694)
% 60.62/60.69 [170]~P6(x1701,x1702,x1704,x1703)+P6(x1701,x1702,x1703,x1704)
% 60.62/60.69 [223]~P6(x2232,x2233,x2231,x2234)+P9(x2231,x2232,x2231,x2233,x2234,x2232,x2234,x2233)
% 60.62/60.69 [186]~P2(x1864,x1861,x1862,x1863)+P10(f7(x1861,x1862,x1863,x1864),x1861,x1861,x1864)
% 60.62/60.69 [201]P5(x2011,x2012,x2013,x2014)+~P7(x2011,x2012,x2015,x2013,x2014,x2016)
% 60.62/60.69 [213]~P11(x2134,x2135,x2136,x2131,x2132,x2133)+P11(x2131,x2132,x2133,x2134,x2135,x2136)
% 60.62/60.69 [214]~P11(x2142,x2141,x2143,x2145,x2144,x2146)+P11(x2141,x2142,x2143,x2144,x2145,x2146)
% 60.62/60.69 [215]~P11(x2151,x2153,x2152,x2154,x2156,x2155)+P11(x2151,x2152,x2153,x2154,x2155,x2156)
% 60.62/60.69 [216]~P7(x2164,x2165,x2166,x2161,x2162,x2163)+P7(x2161,x2162,x2163,x2164,x2165,x2166)
% 60.62/60.69 [217]~P7(x2172,x2171,x2173,x2175,x2174,x2176)+P7(x2171,x2172,x2173,x2174,x2175,x2176)
% 60.62/60.69 [218]~P7(x2181,x2183,x2182,x2184,x2186,x2185)+P7(x2181,x2182,x2183,x2184,x2185,x2186)
% 60.62/60.69 [224]~P3(x2241,x2242,x2245,x2246)+P9(x2241,x2242,x2243,x2244,x2245,x2246,x2243,x2244)
% 60.62/60.69 [230]~P11(x2301,x2302,x2303,x2304,x2305,x2306)+P9(x2301,x2302,x2302,x2303,x2304,x2305,x2305,x2306)
% 60.62/60.69 [231]~P11(x2311,x2312,x2313,x2314,x2315,x2316)+P8(x2311,x2312,x2311,x2313,x2314,x2315,x2314,x2316)
% 60.62/60.69 [232]~P9(x2321,x2322,x2325,x2326,x2323,x2324,x2325,x2326)+P3(x2321,x2322,x2323,x2324)
% 60.62/60.69 [251]~P9(x2515,x2516,x2517,x2518,x2511,x2512,x2513,x2514)+P9(x2511,x2512,x2513,x2514,x2515,x2516,x2517,x2518)
% 60.62/60.69 [252]~P9(x2523,x2524,x2521,x2522,x2527,x2528,x2525,x2526)+P9(x2521,x2522,x2523,x2524,x2525,x2526,x2527,x2528)
% 60.62/60.69 [253]~P9(x2532,x2531,x2533,x2534,x2535,x2536,x2537,x2538)+P9(x2531,x2532,x2533,x2534,x2535,x2536,x2537,x2538)
% 60.62/60.69 [254]~P9(x2541,x2542,x2545,x2546,x2543,x2544,x2547,x2548)+P9(x2541,x2542,x2543,x2544,x2545,x2546,x2547,x2548)
% 60.62/60.69 [255]~P8(x2555,x2556,x2557,x2558,x2551,x2552,x2553,x2554)+P8(x2551,x2552,x2553,x2554,x2555,x2556,x2557,x2558)
% 60.62/60.69 [256]~P8(x2563,x2564,x2561,x2562,x2567,x2568,x2565,x2566)+P8(x2561,x2562,x2563,x2564,x2565,x2566,x2567,x2568)
% 60.62/60.69 [257]~P8(x2572,x2571,x2573,x2574,x2575,x2576,x2577,x2578)+P8(x2571,x2572,x2573,x2574,x2575,x2576,x2577,x2578)
% 60.62/60.69 [258]~P8(x2581,x2582,x2585,x2586,x2583,x2584,x2587,x2588)+P8(x2581,x2582,x2583,x2584,x2585,x2586,x2587,x2588)
% 60.62/60.69 [160]~P1(x1601,x1602,x1603)+~P5(x1601,x1602,x1601,x1603)+P4(x1601,x1602,x1603)
% 60.62/60.69 [234]P5(x2341,x2342,x2341,x2343)+~P9(x2341,x2342,x2342,x2343,x2342,x2343,x2341,x2343)+P1(x2341,x2342,x2343)
% 60.62/60.69 [175]~P10(x1751,x1752,x1752,x1753)+~P5(x1752,x1751,x1752,x1753)+P1(x1751,x1752,f3(x1751,x1753,x1752))
% 60.62/60.69 [187]~P10(x1872,x1871,x1871,x1873)+~P5(x1871,x1872,x1871,x1873)+P5(x1871,x1872,x1871,f3(x1872,x1873,x1871))
% 60.62/60.69 [154]~P1(x1543,x1544,x1541)+P1(x1541,x1542,x1543)+~P1(x1543,x1544,x1542)
% 60.62/60.69 [171]~P2(x1714,x1711,x1712,x1713)+P10(x1711,x1712,x1712,x1713)+~P1(x1714,x1711,x1713)
% 60.62/60.69 [172]~P10(x1721,x1724,x1722,x1723)+P5(x1721,x1722,x1721,x1723)+~P4(x1724,x1722,x1723)
% 60.62/60.69 [173]~P10(x1731,x1733,x1733,x1734)+P5(x1731,x1732,x1733,x1732)+~P4(x1732,x1731,x1734)
% 60.62/60.69 [180]~P5(x1801,x1804,x1802,x1804)+~P5(x1801,x1803,x1802,x1803)+P10(x1801,x1802,x1803,x1804)
% 60.62/60.69 [183]~P5(x1831,x1832,x1831,x1834)+~P5(x1831,x1832,x1831,x1833)+P2(x1831,x1832,x1833,x1834)
% 60.62/60.69 [229]~P3(x2291,x2294,x2293,x2292)+~P6(x2291,x2294,x2293,x2292)+P9(x2291,x2292,x2293,x2292,x2293,x2292,x2293,x2294)
% 60.62/60.69 [233]~P9(x2331,x2333,x2331,x2334,x2332,x2333,x2332,x2334)+P1(x2331,x2332,x2333)+P6(x2333,x2334,x2331,x2332)
% 60.62/60.69 [235]~P1(x2353,x2354,x2352)+~P9(x2353,x2351,x2353,x2352,x2354,x2351,x2354,x2352)+P6(x2351,x2352,x2353,x2354)
% 60.62/60.69 [237]P10(x2371,x2372,x2373,x2374)+~P9(x2371,x2372,x2373,x2374,x2373,x2374,x2371,x2372)+P3(x2371,x2372,x2373,x2374)
% 60.62/60.69 [176]~P10(x1761,x1764,x1762,x1763)+~P10(x1762,x1764,x1761,x1763)+P1(f4(x1761,x1762,x1763),x1763,x1762)
% 60.62/60.69 [177]~P10(x1771,x1774,x1772,x1773)+~P10(x1772,x1774,x1771,x1773)+P1(f5(x1771,x1772,x1773),x1773,x1771)
% 60.62/60.69 [188]~P10(x1881,x1884,x1882,x1883)+~P10(x1882,x1884,x1881,x1883)+P10(x1881,f4(x1881,x1882,x1883),x1883,x1882)
% 60.62/60.69 [189]~P10(x1891,x1894,x1892,x1893)+~P10(x1892,x1894,x1891,x1893)+P10(x1891,f5(x1892,x1891,x1893),x1893,x1892)
% 60.62/60.69 [190]~P10(x1901,x1903,x1903,x1902)+~P6(x1901,x1902,x1903,x1904)+P2(f8(x1901,x1902,x1903),x1901,x1902,x1903)
% 60.62/60.69 [192]~P10(x1923,x1924,x1922,x1921)+~P5(x1923,x1922,x1923,x1921)+P1(x1921,x1922,f22(x1922,x1921,x1923,x1924))
% 60.62/60.69 [193]~P10(x1933,x1934,x1931,x1932)+~P5(x1933,x1931,x1933,x1932)+P1(f22(x1931,x1932,x1933,x1934),x1933,x1934)
% 60.62/60.69 [244]~P5(x2443,x2442,x2443,x2441)+~P9(x2442,x2443,x2443,x2444,x2443,x2444,x2443,x2441)+P1(x2441,x2442,f23(x2442,x2441,x2443,x2444))
% 60.62/60.69 [245]~P10(x2453,x2454,x2452,x2451)+~P9(x2452,x2453,x2453,x2454,x2453,x2454,x2453,x2451)+P1(x2451,x2452,f24(x2452,x2451,x2453,x2454))
% 60.62/60.69 [246]~P10(x2463,x2462,x2462,x2461)+~P9(x2464,x2463,x2462,x2463,x2462,x2463,x2461,x2463)+P1(f14(x2461,x2462,x2463,x2464),x2463,x2464)
% 60.62/60.69 [247]~P10(x2473,x2472,x2472,x2471)+~P9(x2474,x2473,x2472,x2473,x2472,x2473,x2471,x2473)+P1(f14(x2471,x2472,x2473,x2474),x2471,x2472)
% 60.62/60.69 [248]~P5(x2483,x2481,x2483,x2482)+~P9(x2481,x2483,x2483,x2484,x2483,x2484,x2483,x2482)+P1(f23(x2481,x2482,x2483,x2484),x2483,x2484)
% 60.62/60.69 [249]~P10(x2493,x2494,x2491,x2492)+~P9(x2491,x2493,x2493,x2494,x2493,x2494,x2493,x2492)+P1(f24(x2491,x2492,x2493,x2494),x2493,x2494)
% 60.62/60.69 [156]~P4(x1565,x1561,x1563)+P3(x1561,x1562,x1563,x1564)+~P4(x1565,x1562,x1564)
% 60.62/60.69 [157]~P4(x1571,x1575,x1573)+P3(x1571,x1572,x1573,x1574)+~P4(x1572,x1575,x1574)
% 60.62/60.69 [184]~P6(x1845,x1841,x1842,x1843)+P6(x1841,x1842,x1843,x1844)+~P6(x1845,x1841,x1842,x1844)
% 60.62/60.69 [226]~P4(x2265,x2262,x2263)+~P2(x2264,x2261,x2262,x2263)+P9(x2261,x2262,x2261,x2263,x2264,x2262,x2264,x2265)
% 60.62/60.69 [228]~P2(x2285,x2281,x2283,x2284)+P9(x2281,x2282,x2281,x2283,x2284,x2281,x2284,x2283)+~P10(x2285,x2281,x2281,x2282)
% 60.62/60.69 [241]~P9(x2412,x2413,x2412,x2414,x2415,x2412,x2415,x2414)+P10(x2411,x2412,x2412,x2413)+~P2(x2411,x2412,x2414,x2415)
% 60.62/60.69 [196]~P1(x1962,x1964,x1965)+~P10(x1961,x1963,x1963,x1962)+P1(f12(x1961,x1962,x1963,x1964,x1965),x1964,x1965)
% 60.62/60.69 [197]~P1(x1972,x1974,x1975)+~P10(x1971,x1973,x1973,x1972)+P10(f12(x1971,x1972,x1973,x1974,x1975),x1971,x1974,x1975)
% 60.62/60.69 [198]~P10(x1983,x1984,x1984,x1981)+~P5(x1981,x1982,x1981,x1985)+P5(x1981,x1982,x1981,f27(x1983,x1984,x1982,x1985,x1981))
% 60.62/60.69 [199]~P10(x1993,x1991,x1991,x1995)+~P5(x1995,x1992,x1995,x1994)+P5(x1991,x1992,x1991,f27(x1993,x1991,x1992,x1994,x1995))
% 60.62/60.69 [200]~P10(x2001,x2002,x2002,x2005)+~P5(x2005,x2003,x2005,x2004)+P3(f27(x2001,x2002,x2003,x2004,x2005),x2003,x2001,x2002)
% 60.62/60.69 [243]~P9(x2431,x2433,x2432,x2433,x2431,x2434,x2432,x2435)+P1(x2431,x2432,x2433)+P6(x2434,x2432,x2433,f26(x2431,x2432,x2433,x2434))
% 60.62/60.69 [259]~P9(x2591,x2593,x2592,x2593,x2591,x2594,x2592,x2595)+P1(x2591,x2592,x2593)+P9(x2591,x2593,x2592,x2593,x2591,f26(x2591,x2592,x2593,x2594),x2592,f26(x2591,x2592,x2593,x2594))
% 60.62/60.69 [178]~P3(x1781,x1782,x1785,x1786)+P3(x1781,x1782,x1783,x1784)+~P3(x1785,x1786,x1783,x1784)
% 60.62/60.69 [179]~P10(x1791,x1792,x1795,x1796)+P3(x1791,x1792,x1793,x1794)+~P10(x1795,x1796,x1793,x1794)
% 60.62/60.69 [181]~P10(x1815,x1816,x1813,x1814)+P10(x1811,x1812,x1813,x1814)+~P3(x1811,x1812,x1815,x1816)
% 60.62/60.69 [182]~P5(x1821,x1822,x1825,x1826)+P5(x1821,x1822,x1823,x1824)+~P5(x1825,x1826,x1823,x1824)
% 60.62/60.69 [219]~P5(x2191,x2192,x2194,x2195)+~P11(x2191,x2192,x2193,x2194,x2195,x2196)+P7(x2191,x2192,x2193,x2194,x2195,x2196)
% 60.62/60.69 [222]~P4(x2224,x2225,x2226)+~P4(x2221,x2222,x2223)+P8(x2221,x2222,x2222,x2223,x2224,x2225,x2225,x2226)
% 60.62/60.69 [202]~P4(x2026,x2023,x2024)+~P4(x2025,x2021,x2022)+P4(f25(x2021,x2022,x2023,x2024,x2025,x2026),x2021,x2024)
% 60.62/60.69 [203]~P4(x2036,x2033,x2034)+~P4(x2035,x2031,x2032)+P3(f25(x2031,x2032,x2033,x2034,x2035,x2036),x2036,x2031,x2033)
% 60.62/60.69 [204]~P4(x2046,x2043,x2044)+~P4(x2045,x2041,x2042)+P3(f25(x2041,x2042,x2043,x2044,x2045,x2046),x2045,x2042,x2044)
% 60.62/60.69 [239]~P9(x2391,x2392,x2393,x2394,x2395,x2396,x2397,x2398)+P3(x2391,x2392,x2393,x2394)+~P3(x2395,x2396,x2397,x2398)
% 60.62/60.69 [240]~P9(x2401,x2402,x2403,x2404,x2405,x2406,x2407,x2408)+P10(x2401,x2402,x2403,x2404)+~P10(x2405,x2406,x2407,x2408)
% 60.62/60.69 [242]~P8(x2421,x2422,x2423,x2424,x2425,x2426,x2427,x2428)+P5(x2421,x2422,x2423,x2424)+~P5(x2425,x2426,x2427,x2428)
% 60.62/60.69 [220]~P11(x2201,x2202,x2203,x2207,x2208,x2209)+P11(x2201,x2202,x2203,x2204,x2205,x2206)+~P11(x2207,x2208,x2209,x2204,x2205,x2206)
% 60.62/60.69 [221]~P7(x2211,x2212,x2213,x2217,x2218,x2219)+P7(x2211,x2212,x2213,x2214,x2215,x2216)+~P7(x2217,x2218,x2219,x2214,x2215,x2216)
% 60.62/60.69 [261]~P9(x2611,x2612,x2613,x2614,x2619,x26110,x26111,x26112)+P9(x2611,x2612,x2613,x2614,x2615,x2616,x2617,x2618)+~P9(x2619,x26110,x26111,x26112,x2615,x2616,x2617,x2618)
% 60.62/60.69 [262]~P8(x2621,x2622,x2623,x2624,x2629,x26210,x26211,x26212)+P8(x2621,x2622,x2623,x2624,x2625,x2626,x2627,x2628)+~P8(x2629,x26210,x26211,x26212,x2625,x2626,x2627,x2628)
% 60.62/60.69 [194]~P5(x1942,x1941,x1944,x1941)+~P6(x1942,x1944,x1941,x1943)+P10(x1941,x1942,x1942,x1943)+~P5(x1942,x1943,x1944,x1943)
% 60.62/60.69 [161]~P1(x1611,x1612,x1613)+~P3(x1614,x1611,x1615,x1613)+P4(x1611,x1612,x1613)+~P4(x1614,x1612,x1615)
% 60.62/60.69 [174]~P3(x1744,x1743,x1745,x1742)+~P3(x1744,x1742,x1745,x1743)+P4(x1741,x1742,x1743)+~P4(x1741,x1744,x1745)
% 60.62/60.69 [195]~P5(x1955,x1951,x1955,x1953)+~P5(x1955,x1951,x1955,x1952)+P6(x1951,x1952,x1953,x1954)+~P5(x1955,x1951,x1955,x1954)
% 60.62/60.69 [227]~P1(x2271,x2274,x2275)+~P1(x2271,x2272,x2273)+~P3(x2272,x2274,x2273,x2275)+P8(x2271,x2272,x2272,x2273,x2271,x2274,x2274,x2275)
% 60.62/60.69 [238]~P1(x2381,x2382,x2383)+~P9(x2385,x2382,x2385,x2383,x2384,x2382,x2384,x2381)+P4(x2381,x2382,x2383)+~P2(x2384,x2385,x2382,x2383)
% 60.62/60.69 [185]~P10(x1853,x1851,x1853,x1855)+~P10(x1851,x1852,x1851,x1853)+~P4(x1854,x1852,x1855)+P4(f6(x1851,x1852,x1853),x1851,x1853)
% 60.62/60.69 [191]~P6(x1911,x1912,x1913,x1915)+~P3(x1911,x1912,x1913,x1915)+~P4(x1914,x1911,x1912)+P2(f9(x1911,x1912,x1913),x1911,x1912,x1913)
% 60.62/60.69 [260]~P9(x2601,x2603,x2602,x2603,x2604,x2606,x2605,x2606)+~P9(x2601,x2602,x2602,x2603,x2604,x2605,x2605,x2606)+P1(x2601,x2602,x2603)+P11(x2601,x2602,x2603,x2604,x2605,x2606)
% 60.62/60.69 [250]~P6(x2501,x2502,x2505,x2504)+~P6(x2501,x2502,x2505,x2503)+~P9(x2505,x2501,x2505,x2502,x2506,x2503,x2506,x2504)+P5(x2501,x2502,x2503,x2504)+~P6(x2501,x2502,x2505,x2506)
% 60.62/60.69 [205]~P1(x2052,x2053,x2054)+~P1(x2051,x2054,x2056)+~P1(x2051,x2053,x2055)+~P3(x2053,x2054,x2055,x2056)+P1(x2051,x2052,f13(x2053,x2054,x2055,x2056,x2051,x2052))
% 60.62/60.69 [206]~P1(x2066,x2061,x2062)+~P1(x2065,x2062,x2064)+~P1(x2065,x2061,x2063)+~P3(x2061,x2062,x2063,x2064)+P1(f13(x2061,x2062,x2063,x2064,x2065,x2066),x2063,x2064)
% 60.62/60.69 [207]~P1(x2073,x2074,x2075)+~P4(x2076,x2071,x2072)+~P3(x2071,x2073,x2075,x2076)+~P3(x2071,x2073,x2072,x2074)+P1(f28(x2071,x2072,x2073,x2074,x2075,x2076),x2076,x2075)
% 60.62/60.69 [208]~P1(x2083,x2084,x2085)+~P4(x2086,x2081,x2082)+~P3(x2081,x2083,x2085,x2086)+~P3(x2081,x2083,x2082,x2084)+P1(f28(x2081,x2082,x2083,x2084,x2085,x2086),x2081,x2084)
% 60.62/60.69 [209]~P5(x2092,x2093,x2092,x2094)+~P5(x2091,x2093,x2091,x2096)+~P2(x2091,x2093,x2094,x2095)+E(x2091,x2092)+P1(f10(x2093,x2094,x2095,x2096,x2091,x2092),x2093,x2095)
% 60.62/60.69 [210]~P5(x2102,x2103,x2102,x2104)+~P5(x2101,x2103,x2101,x2106)+~P2(x2101,x2103,x2104,x2105)+E(x2101,x2102)+P1(f11(x2103,x2104,x2105,x2106,x2101,x2102),x2104,x2106)
% 60.62/60.69 [211]~P5(x2112,x2113,x2112,x2114)+~P5(x2111,x2113,x2111,x2116)+~P2(x2111,x2113,x2114,x2115)+E(x2111,x2112)+P5(f10(x2113,x2114,x2115,x2116,x2111,x2112),x2112,x2112,x2113)
% 60.62/60.69 [212]~P5(x2122,x2123,x2122,x2124)+~P5(x2121,x2123,x2121,x2126)+~P2(x2121,x2123,x2124,x2125)+E(x2121,x2122)+P5(f11(x2123,x2124,x2125,x2126,x2121,x2122),x2122,x2122,x2123)
% 60.62/60.69 [158]~P1(x1583,x1581,x1584)+~P1(x1585,x1581,x1584)+~P4(x1586,x1585,x1583)+~P4(x1587,x1581,x1584)+P4(f21(x1581,x1582),x1581,x1582)
% 60.62/60.69 %EqnAxiom
% 60.62/60.69 [1]E(x11,x11)
% 60.62/60.69 [2]E(x22,x21)+~E(x21,x22)
% 60.62/60.69 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 60.62/60.69 [4]~E(x41,x42)+E(f21(x41,x43),f21(x42,x43))
% 60.62/60.69 [5]~E(x51,x52)+E(f21(x53,x51),f21(x53,x52))
% 60.62/60.69 [6]~E(x61,x62)+E(f3(x61,x63,x64),f3(x62,x63,x64))
% 60.70/60.69 [7]~E(x71,x72)+E(f3(x73,x71,x74),f3(x73,x72,x74))
% 60.70/60.69 [8]~E(x81,x82)+E(f3(x83,x84,x81),f3(x83,x84,x82))
% 60.70/60.69 [9]~E(x91,x92)+E(f4(x91,x93,x94),f4(x92,x93,x94))
% 60.70/60.69 [10]~E(x101,x102)+E(f4(x103,x101,x104),f4(x103,x102,x104))
% 60.70/60.69 [11]~E(x111,x112)+E(f4(x113,x114,x111),f4(x113,x114,x112))
% 60.70/60.69 [12]~E(x121,x122)+E(f5(x121,x123,x124),f5(x122,x123,x124))
% 60.70/60.69 [13]~E(x131,x132)+E(f5(x133,x131,x134),f5(x133,x132,x134))
% 60.70/60.69 [14]~E(x141,x142)+E(f5(x143,x144,x141),f5(x143,x144,x142))
% 60.70/60.69 [15]~E(x151,x152)+E(f6(x151,x153,x154),f6(x152,x153,x154))
% 60.70/60.69 [16]~E(x161,x162)+E(f6(x163,x161,x164),f6(x163,x162,x164))
% 60.70/60.69 [17]~E(x171,x172)+E(f6(x173,x174,x171),f6(x173,x174,x172))
% 60.70/60.69 [18]~E(x181,x182)+E(f7(x181,x183,x184,x185),f7(x182,x183,x184,x185))
% 60.70/60.69 [19]~E(x191,x192)+E(f7(x193,x191,x194,x195),f7(x193,x192,x194,x195))
% 60.70/60.69 [20]~E(x201,x202)+E(f7(x203,x204,x201,x205),f7(x203,x204,x202,x205))
% 60.70/60.70 [21]~E(x211,x212)+E(f7(x213,x214,x215,x211),f7(x213,x214,x215,x212))
% 60.70/60.70 [22]~E(x221,x222)+E(f26(x221,x223,x224,x225),f26(x222,x223,x224,x225))
% 60.70/60.70 [23]~E(x231,x232)+E(f26(x233,x231,x234,x235),f26(x233,x232,x234,x235))
% 60.70/60.70 [24]~E(x241,x242)+E(f26(x243,x244,x241,x245),f26(x243,x244,x242,x245))
% 60.70/60.70 [25]~E(x251,x252)+E(f26(x253,x254,x255,x251),f26(x253,x254,x255,x252))
% 60.70/60.70 [26]~E(x261,x262)+E(f23(x261,x263,x264,x265),f23(x262,x263,x264,x265))
% 60.70/60.70 [27]~E(x271,x272)+E(f23(x273,x271,x274,x275),f23(x273,x272,x274,x275))
% 60.70/60.70 [28]~E(x281,x282)+E(f23(x283,x284,x281,x285),f23(x283,x284,x282,x285))
% 60.70/60.70 [29]~E(x291,x292)+E(f23(x293,x294,x295,x291),f23(x293,x294,x295,x292))
% 60.70/60.70 [30]~E(x301,x302)+E(f24(x301,x303,x304,x305),f24(x302,x303,x304,x305))
% 60.70/60.70 [31]~E(x311,x312)+E(f24(x313,x311,x314,x315),f24(x313,x312,x314,x315))
% 60.70/60.70 [32]~E(x321,x322)+E(f24(x323,x324,x321,x325),f24(x323,x324,x322,x325))
% 60.70/60.70 [33]~E(x331,x332)+E(f24(x333,x334,x335,x331),f24(x333,x334,x335,x332))
% 60.70/60.70 [34]~E(x341,x342)+E(f8(x341,x343,x344),f8(x342,x343,x344))
% 60.70/60.70 [35]~E(x351,x352)+E(f8(x353,x351,x354),f8(x353,x352,x354))
% 60.70/60.70 [36]~E(x361,x362)+E(f8(x363,x364,x361),f8(x363,x364,x362))
% 60.70/60.70 [37]~E(x371,x372)+E(f9(x371,x373,x374),f9(x372,x373,x374))
% 60.70/60.70 [38]~E(x381,x382)+E(f9(x383,x381,x384),f9(x383,x382,x384))
% 60.70/60.70 [39]~E(x391,x392)+E(f9(x393,x394,x391),f9(x393,x394,x392))
% 60.70/60.70 [40]~E(x401,x402)+E(f22(x401,x403,x404,x405),f22(x402,x403,x404,x405))
% 60.70/60.70 [41]~E(x411,x412)+E(f22(x413,x411,x414,x415),f22(x413,x412,x414,x415))
% 60.70/60.70 [42]~E(x421,x422)+E(f22(x423,x424,x421,x425),f22(x423,x424,x422,x425))
% 60.70/60.70 [43]~E(x431,x432)+E(f22(x433,x434,x435,x431),f22(x433,x434,x435,x432))
% 60.70/60.70 [44]~E(x441,x442)+E(f14(x441,x443,x444,x445),f14(x442,x443,x444,x445))
% 60.70/60.70 [45]~E(x451,x452)+E(f14(x453,x451,x454,x455),f14(x453,x452,x454,x455))
% 60.70/60.70 [46]~E(x461,x462)+E(f14(x463,x464,x461,x465),f14(x463,x464,x462,x465))
% 60.70/60.70 [47]~E(x471,x472)+E(f14(x473,x474,x475,x471),f14(x473,x474,x475,x472))
% 60.70/60.70 [48]~E(x481,x482)+E(f12(x481,x483,x484,x485,x486),f12(x482,x483,x484,x485,x486))
% 60.70/60.70 [49]~E(x491,x492)+E(f12(x493,x491,x494,x495,x496),f12(x493,x492,x494,x495,x496))
% 60.70/60.70 [50]~E(x501,x502)+E(f12(x503,x504,x501,x505,x506),f12(x503,x504,x502,x505,x506))
% 60.70/60.70 [51]~E(x511,x512)+E(f12(x513,x514,x515,x511,x516),f12(x513,x514,x515,x512,x516))
% 60.70/60.70 [52]~E(x521,x522)+E(f12(x523,x524,x525,x526,x521),f12(x523,x524,x525,x526,x522))
% 60.70/60.70 [53]~E(x531,x532)+E(f11(x531,x533,x534,x535,x536,x537),f11(x532,x533,x534,x535,x536,x537))
% 60.70/60.70 [54]~E(x541,x542)+E(f11(x543,x541,x544,x545,x546,x547),f11(x543,x542,x544,x545,x546,x547))
% 60.70/60.70 [55]~E(x551,x552)+E(f11(x553,x554,x551,x555,x556,x557),f11(x553,x554,x552,x555,x556,x557))
% 60.70/60.70 [56]~E(x561,x562)+E(f11(x563,x564,x565,x561,x566,x567),f11(x563,x564,x565,x562,x566,x567))
% 60.70/60.70 [57]~E(x571,x572)+E(f11(x573,x574,x575,x576,x571,x577),f11(x573,x574,x575,x576,x572,x577))
% 60.70/60.70 [58]~E(x581,x582)+E(f11(x583,x584,x585,x586,x587,x581),f11(x583,x584,x585,x586,x587,x582))
% 60.70/60.70 [59]~E(x591,x592)+E(f27(x591,x593,x594,x595,x596),f27(x592,x593,x594,x595,x596))
% 60.70/60.70 [60]~E(x601,x602)+E(f27(x603,x601,x604,x605,x606),f27(x603,x602,x604,x605,x606))
% 60.70/60.70 [61]~E(x611,x612)+E(f27(x613,x614,x611,x615,x616),f27(x613,x614,x612,x615,x616))
% 60.70/60.70 [62]~E(x621,x622)+E(f27(x623,x624,x625,x621,x626),f27(x623,x624,x625,x622,x626))
% 60.70/60.70 [63]~E(x631,x632)+E(f27(x633,x634,x635,x636,x631),f27(x633,x634,x635,x636,x632))
% 60.70/60.70 [64]~E(x641,x642)+E(f10(x641,x643,x644,x645,x646,x647),f10(x642,x643,x644,x645,x646,x647))
% 60.70/60.70 [65]~E(x651,x652)+E(f10(x653,x651,x654,x655,x656,x657),f10(x653,x652,x654,x655,x656,x657))
% 60.70/60.70 [66]~E(x661,x662)+E(f10(x663,x664,x661,x665,x666,x667),f10(x663,x664,x662,x665,x666,x667))
% 60.70/60.70 [67]~E(x671,x672)+E(f10(x673,x674,x675,x671,x676,x677),f10(x673,x674,x675,x672,x676,x677))
% 60.70/60.70 [68]~E(x681,x682)+E(f10(x683,x684,x685,x686,x681,x687),f10(x683,x684,x685,x686,x682,x687))
% 60.70/60.70 [69]~E(x691,x692)+E(f10(x693,x694,x695,x696,x697,x691),f10(x693,x694,x695,x696,x697,x692))
% 60.70/60.70 [70]~E(x701,x702)+E(f28(x701,x703,x704,x705,x706,x707),f28(x702,x703,x704,x705,x706,x707))
% 60.70/60.70 [71]~E(x711,x712)+E(f28(x713,x711,x714,x715,x716,x717),f28(x713,x712,x714,x715,x716,x717))
% 60.70/60.70 [72]~E(x721,x722)+E(f28(x723,x724,x721,x725,x726,x727),f28(x723,x724,x722,x725,x726,x727))
% 60.70/60.70 [73]~E(x731,x732)+E(f28(x733,x734,x735,x731,x736,x737),f28(x733,x734,x735,x732,x736,x737))
% 60.70/60.70 [74]~E(x741,x742)+E(f28(x743,x744,x745,x746,x741,x747),f28(x743,x744,x745,x746,x742,x747))
% 60.70/60.70 [75]~E(x751,x752)+E(f28(x753,x754,x755,x756,x757,x751),f28(x753,x754,x755,x756,x757,x752))
% 60.70/60.70 [76]~E(x761,x762)+E(f25(x761,x763,x764,x765,x766,x767),f25(x762,x763,x764,x765,x766,x767))
% 60.70/60.70 [77]~E(x771,x772)+E(f25(x773,x771,x774,x775,x776,x777),f25(x773,x772,x774,x775,x776,x777))
% 60.70/60.70 [78]~E(x781,x782)+E(f25(x783,x784,x781,x785,x786,x787),f25(x783,x784,x782,x785,x786,x787))
% 60.70/60.70 [79]~E(x791,x792)+E(f25(x793,x794,x795,x791,x796,x797),f25(x793,x794,x795,x792,x796,x797))
% 60.70/60.70 [80]~E(x801,x802)+E(f25(x803,x804,x805,x806,x801,x807),f25(x803,x804,x805,x806,x802,x807))
% 60.70/60.70 [81]~E(x811,x812)+E(f25(x813,x814,x815,x816,x817,x811),f25(x813,x814,x815,x816,x817,x812))
% 60.70/60.70 [82]~E(x821,x822)+E(f13(x821,x823,x824,x825,x826,x827),f13(x822,x823,x824,x825,x826,x827))
% 60.70/60.70 [83]~E(x831,x832)+E(f13(x833,x831,x834,x835,x836,x837),f13(x833,x832,x834,x835,x836,x837))
% 60.70/60.70 [84]~E(x841,x842)+E(f13(x843,x844,x841,x845,x846,x847),f13(x843,x844,x842,x845,x846,x847))
% 60.70/60.70 [85]~E(x851,x852)+E(f13(x853,x854,x855,x851,x856,x857),f13(x853,x854,x855,x852,x856,x857))
% 60.70/60.70 [86]~E(x861,x862)+E(f13(x863,x864,x865,x866,x861,x867),f13(x863,x864,x865,x866,x862,x867))
% 60.70/60.70 [87]~E(x871,x872)+E(f13(x873,x874,x875,x876,x877,x871),f13(x873,x874,x875,x876,x877,x872))
% 60.70/60.70 [88]P1(x882,x883,x884)+~E(x881,x882)+~P1(x881,x883,x884)
% 60.70/60.70 [89]P1(x893,x892,x894)+~E(x891,x892)+~P1(x893,x891,x894)
% 60.70/60.70 [90]P1(x903,x904,x902)+~E(x901,x902)+~P1(x903,x904,x901)
% 60.70/60.70 [91]P8(x912,x913,x914,x915,x916,x917,x918,x919)+~E(x911,x912)+~P8(x911,x913,x914,x915,x916,x917,x918,x919)
% 60.70/60.70 [92]P8(x923,x922,x924,x925,x926,x927,x928,x929)+~E(x921,x922)+~P8(x923,x921,x924,x925,x926,x927,x928,x929)
% 60.70/60.70 [93]P8(x933,x934,x932,x935,x936,x937,x938,x939)+~E(x931,x932)+~P8(x933,x934,x931,x935,x936,x937,x938,x939)
% 60.70/60.70 [94]P8(x943,x944,x945,x942,x946,x947,x948,x949)+~E(x941,x942)+~P8(x943,x944,x945,x941,x946,x947,x948,x949)
% 60.70/60.70 [95]P8(x953,x954,x955,x956,x952,x957,x958,x959)+~E(x951,x952)+~P8(x953,x954,x955,x956,x951,x957,x958,x959)
% 60.70/60.70 [96]P8(x963,x964,x965,x966,x967,x962,x968,x969)+~E(x961,x962)+~P8(x963,x964,x965,x966,x967,x961,x968,x969)
% 60.70/60.70 [97]P8(x973,x974,x975,x976,x977,x978,x972,x979)+~E(x971,x972)+~P8(x973,x974,x975,x976,x977,x978,x971,x979)
% 60.70/60.70 [98]P8(x983,x984,x985,x986,x987,x988,x989,x982)+~E(x981,x982)+~P8(x983,x984,x985,x986,x987,x988,x989,x981)
% 60.70/60.70 [99]P3(x992,x993,x994,x995)+~E(x991,x992)+~P3(x991,x993,x994,x995)
% 60.70/60.70 [100]P3(x1003,x1002,x1004,x1005)+~E(x1001,x1002)+~P3(x1003,x1001,x1004,x1005)
% 60.70/60.70 [101]P3(x1013,x1014,x1012,x1015)+~E(x1011,x1012)+~P3(x1013,x1014,x1011,x1015)
% 60.70/60.70 [102]P3(x1023,x1024,x1025,x1022)+~E(x1021,x1022)+~P3(x1023,x1024,x1025,x1021)
% 60.70/60.70 [103]P10(x1032,x1033,x1034,x1035)+~E(x1031,x1032)+~P10(x1031,x1033,x1034,x1035)
% 60.70/60.70 [104]P10(x1043,x1042,x1044,x1045)+~E(x1041,x1042)+~P10(x1043,x1041,x1044,x1045)
% 60.70/60.70 [105]P10(x1053,x1054,x1052,x1055)+~E(x1051,x1052)+~P10(x1053,x1054,x1051,x1055)
% 60.70/60.70 [106]P10(x1063,x1064,x1065,x1062)+~E(x1061,x1062)+~P10(x1063,x1064,x1065,x1061)
% 60.70/60.70 [107]P9(x1072,x1073,x1074,x1075,x1076,x1077,x1078,x1079)+~E(x1071,x1072)+~P9(x1071,x1073,x1074,x1075,x1076,x1077,x1078,x1079)
% 60.70/60.70 [108]P9(x1083,x1082,x1084,x1085,x1086,x1087,x1088,x1089)+~E(x1081,x1082)+~P9(x1083,x1081,x1084,x1085,x1086,x1087,x1088,x1089)
% 60.70/60.70 [109]P9(x1093,x1094,x1092,x1095,x1096,x1097,x1098,x1099)+~E(x1091,x1092)+~P9(x1093,x1094,x1091,x1095,x1096,x1097,x1098,x1099)
% 60.70/60.70 [110]P9(x1103,x1104,x1105,x1102,x1106,x1107,x1108,x1109)+~E(x1101,x1102)+~P9(x1103,x1104,x1105,x1101,x1106,x1107,x1108,x1109)
% 60.70/60.70 [111]P9(x1113,x1114,x1115,x1116,x1112,x1117,x1118,x1119)+~E(x1111,x1112)+~P9(x1113,x1114,x1115,x1116,x1111,x1117,x1118,x1119)
% 60.70/60.70 [112]P9(x1123,x1124,x1125,x1126,x1127,x1122,x1128,x1129)+~E(x1121,x1122)+~P9(x1123,x1124,x1125,x1126,x1127,x1121,x1128,x1129)
% 60.70/60.70 [113]P9(x1133,x1134,x1135,x1136,x1137,x1138,x1132,x1139)+~E(x1131,x1132)+~P9(x1133,x1134,x1135,x1136,x1137,x1138,x1131,x1139)
% 60.70/60.70 [114]P9(x1143,x1144,x1145,x1146,x1147,x1148,x1149,x1142)+~E(x1141,x1142)+~P9(x1143,x1144,x1145,x1146,x1147,x1148,x1149,x1141)
% 60.70/60.70 [115]P2(x1152,x1153,x1154,x1155)+~E(x1151,x1152)+~P2(x1151,x1153,x1154,x1155)
% 60.70/60.70 [116]P2(x1163,x1162,x1164,x1165)+~E(x1161,x1162)+~P2(x1163,x1161,x1164,x1165)
% 60.70/60.70 [117]P2(x1173,x1174,x1172,x1175)+~E(x1171,x1172)+~P2(x1173,x1174,x1171,x1175)
% 60.70/60.70 [118]P2(x1183,x1184,x1185,x1182)+~E(x1181,x1182)+~P2(x1183,x1184,x1185,x1181)
% 60.70/60.70 [119]P5(x1192,x1193,x1194,x1195)+~E(x1191,x1192)+~P5(x1191,x1193,x1194,x1195)
% 60.70/60.70 [120]P5(x1203,x1202,x1204,x1205)+~E(x1201,x1202)+~P5(x1203,x1201,x1204,x1205)
% 60.70/60.70 [121]P5(x1213,x1214,x1212,x1215)+~E(x1211,x1212)+~P5(x1213,x1214,x1211,x1215)
% 60.70/60.70 [122]P5(x1223,x1224,x1225,x1222)+~E(x1221,x1222)+~P5(x1223,x1224,x1225,x1221)
% 60.70/60.70 [123]P6(x1232,x1233,x1234,x1235)+~E(x1231,x1232)+~P6(x1231,x1233,x1234,x1235)
% 60.70/60.70 [124]P6(x1243,x1242,x1244,x1245)+~E(x1241,x1242)+~P6(x1243,x1241,x1244,x1245)
% 60.70/60.70 [125]P6(x1253,x1254,x1252,x1255)+~E(x1251,x1252)+~P6(x1253,x1254,x1251,x1255)
% 60.70/60.70 [126]P6(x1263,x1264,x1265,x1262)+~E(x1261,x1262)+~P6(x1263,x1264,x1265,x1261)
% 60.70/60.70 [127]P11(x1272,x1273,x1274,x1275,x1276,x1277)+~E(x1271,x1272)+~P11(x1271,x1273,x1274,x1275,x1276,x1277)
% 60.70/60.70 [128]P11(x1283,x1282,x1284,x1285,x1286,x1287)+~E(x1281,x1282)+~P11(x1283,x1281,x1284,x1285,x1286,x1287)
% 60.70/60.70 [129]P11(x1293,x1294,x1292,x1295,x1296,x1297)+~E(x1291,x1292)+~P11(x1293,x1294,x1291,x1295,x1296,x1297)
% 60.70/60.70 [130]P11(x1303,x1304,x1305,x1302,x1306,x1307)+~E(x1301,x1302)+~P11(x1303,x1304,x1305,x1301,x1306,x1307)
% 60.70/60.70 [131]P11(x1313,x1314,x1315,x1316,x1312,x1317)+~E(x1311,x1312)+~P11(x1313,x1314,x1315,x1316,x1311,x1317)
% 60.70/60.70 [132]P11(x1323,x1324,x1325,x1326,x1327,x1322)+~E(x1321,x1322)+~P11(x1323,x1324,x1325,x1326,x1327,x1321)
% 60.70/60.70 [133]P4(x1332,x1333,x1334)+~E(x1331,x1332)+~P4(x1331,x1333,x1334)
% 60.70/60.70 [134]P4(x1343,x1342,x1344)+~E(x1341,x1342)+~P4(x1343,x1341,x1344)
% 60.70/60.70 [135]P4(x1353,x1354,x1352)+~E(x1351,x1352)+~P4(x1353,x1354,x1351)
% 60.70/60.70 [136]P7(x1362,x1363,x1364,x1365,x1366,x1367)+~E(x1361,x1362)+~P7(x1361,x1363,x1364,x1365,x1366,x1367)
% 60.70/60.70 [137]P7(x1373,x1372,x1374,x1375,x1376,x1377)+~E(x1371,x1372)+~P7(x1373,x1371,x1374,x1375,x1376,x1377)
% 60.70/60.70 [138]P7(x1383,x1384,x1382,x1385,x1386,x1387)+~E(x1381,x1382)+~P7(x1383,x1384,x1381,x1385,x1386,x1387)
% 60.70/60.70 [139]P7(x1393,x1394,x1395,x1392,x1396,x1397)+~E(x1391,x1392)+~P7(x1393,x1394,x1395,x1391,x1396,x1397)
% 60.70/60.70 [140]P7(x1403,x1404,x1405,x1406,x1402,x1407)+~E(x1401,x1402)+~P7(x1403,x1404,x1405,x1406,x1401,x1407)
% 60.70/60.70 [141]P7(x1413,x1414,x1415,x1416,x1417,x1412)+~E(x1411,x1412)+~P7(x1413,x1414,x1415,x1416,x1417,x1411)
% 60.70/60.70
% 60.70/60.70 %-------------------------------------------
% 60.70/60.70 cnf(263,plain,
% 60.70/60.70 (~P3(a2,a18,a1,a19)),
% 60.70/60.70 inference(scs_inference,[],[149,162])).
% 60.70/60.70 cnf(265,plain,
% 60.70/60.70 (~P3(a1,a19,a18,a2)),
% 60.70/60.70 inference(scs_inference,[],[149,162,163])).
% 60.70/60.70 cnf(269,plain,
% 60.70/60.70 (~P9(a2,a18,x2691,x2692,a1,a19,x2691,x2692)),
% 60.70/60.70 inference(scs_inference,[],[149,162,163,232,251])).
% 60.70/60.70 cnf(271,plain,
% 60.70/60.70 (~P9(x2711,x2712,a1,a19,x2711,x2712,a2,a18)),
% 60.70/60.70 inference(scs_inference,[],[149,162,163,232,251,252])).
% 60.70/60.70 cnf(273,plain,
% 60.70/60.70 (~P9(a19,a1,x2731,x2732,a2,a18,x2731,x2732)),
% 60.70/60.70 inference(scs_inference,[],[149,162,163,232,251,252,253])).
% 60.70/60.70 cnf(275,plain,
% 60.70/60.70 (~P9(a1,a19,a2,a18,x2751,x2752,x2751,x2752)),
% 60.70/60.70 inference(scs_inference,[],[149,162,163,232,251,252,253,254])).
% 60.70/60.70 cnf(277,plain,
% 60.70/60.70 (P1(a15,a15,a1)),
% 60.70/60.70 inference(scs_inference,[],[142,149,162,163,232,251,252,253,254,154])).
% 60.70/60.70 cnf(279,plain,
% 60.70/60.70 (~P9(a1,a19,a2,a18,a15,a16,a17,a2)),
% 60.70/60.70 inference(scs_inference,[],[142,144,149,162,163,232,251,252,253,254,154,239])).
% 60.70/60.70 cnf(281,plain,
% 60.70/60.70 (~P3(a19,a1,a2,a18)),
% 60.70/60.70 inference(scs_inference,[],[142,144,149,162,163,232,251,252,253,254,154,239,224])).
% 60.70/60.70 cnf(283,plain,
% 60.70/60.70 (~P3(x2831,x2832,a15,a16)+P3(x2831,x2832,a17,a2)),
% 60.70/60.70 inference(scs_inference,[],[142,144,149,162,163,232,251,252,253,254,154,239,224,178])).
% 60.70/60.70 cnf(289,plain,
% 60.70/60.70 (~P9(a15,a16,a17,a2,a1,a19,a2,a18)),
% 60.70/60.70 inference(scs_inference,[],[279,251])).
% 60.70/60.70 cnf(291,plain,
% 60.70/60.70 (~P9(a1,a19,x2911,x2912,a18,a2,x2911,x2912)),
% 60.70/60.70 inference(scs_inference,[],[265,279,251,232])).
% 60.70/60.70 cnf(293,plain,
% 60.70/60.70 (~P9(a19,a1,a2,a18,a15,a16,a17,a2)),
% 60.70/60.70 inference(scs_inference,[],[265,279,251,232,253])).
% 60.70/60.70 cnf(297,plain,
% 60.70/60.70 (~P3(a18,a2,a1,a19)),
% 60.70/60.70 inference(scs_inference,[],[265,279,251,232,253,254,162])).
% 60.70/60.70 cnf(299,plain,
% 60.70/60.70 (~P3(a2,a18,a19,a1)),
% 60.70/60.70 inference(scs_inference,[],[263,265,279,251,232,253,254,162,163])).
% 60.70/60.70 cnf(303,plain,
% 60.70/60.70 (~P9(a2,a18,a1,a19,a15,a16,a17,a2)),
% 60.70/60.70 inference(scs_inference,[],[144,263,265,279,251,232,253,254,162,163,252,239])).
% 60.70/60.70 cnf(305,plain,
% 60.70/60.70 (P1(a16,a16,a19)),
% 60.70/60.70 inference(scs_inference,[],[143,144,263,265,279,251,232,253,254,162,163,252,239,154])).
% 60.70/60.70 cnf(319,plain,
% 60.70/60.70 (~P9(a19,a1,x3191,x3192,a18,a2,x3191,x3192)),
% 60.70/60.70 inference(scs_inference,[],[291,253])).
% 60.70/60.70 cnf(321,plain,
% 60.70/60.70 (~P9(a1,a19,a18,a2,x3211,x3212,x3211,x3212)),
% 60.70/60.70 inference(scs_inference,[],[291,253,254])).
% 60.70/60.70 cnf(323,plain,
% 60.70/60.70 (~P9(a18,a2,x3231,x3232,a1,a19,x3231,x3232)),
% 60.70/60.70 inference(scs_inference,[],[291,253,254,251])).
% 60.70/60.70 cnf(325,plain,
% 60.70/60.70 (~P3(a19,a1,a18,a2)),
% 60.70/60.70 inference(scs_inference,[],[291,253,254,251,224])).
% 60.70/60.70 cnf(327,plain,
% 60.70/60.70 (~P9(a2,a18,x3271,x3272,a19,a1,x3271,x3272)),
% 60.70/60.70 inference(scs_inference,[],[291,299,253,254,251,224,232])).
% 60.70/60.70 cnf(329,plain,
% 60.70/60.70 (~P3(a18,a2,a19,a1)),
% 60.70/60.70 inference(scs_inference,[],[291,297,299,253,254,251,224,232,163])).
% 60.70/60.70 cnf(331,plain,
% 60.70/60.70 (~P9(x3311,x3312,a1,a19,x3311,x3312,a18,a2)),
% 60.70/60.70 inference(scs_inference,[],[291,297,299,253,254,251,224,232,163,252])).
% 60.70/60.70 cnf(333,plain,
% 60.70/60.70 (P1(a1,a1,a15)),
% 60.70/60.70 inference(scs_inference,[],[277,291,297,299,253,254,251,224,232,163,252,154])).
% 60.70/60.70 cnf(348,plain,
% 60.70/60.70 (~P9(a15,a16,a17,a2,a2,a18,a1,a19)),
% 60.70/60.70 inference(scs_inference,[],[303,251])).
% 60.70/60.70 cnf(350,plain,
% 60.70/60.70 (~P9(a18,a2,x3501,x3502,a19,a1,x3501,x3502)),
% 60.70/60.70 inference(scs_inference,[],[327,303,251,253])).
% 60.70/60.70 cnf(352,plain,
% 60.70/60.70 (~P9(a2,a18,a19,a1,x3521,x3522,x3521,x3522)),
% 60.70/60.70 inference(scs_inference,[],[327,303,251,253,254])).
% 60.70/60.70 cnf(356,plain,
% 60.70/60.70 (~P9(a2,a18,a19,a1,a15,a16,a17,a2)),
% 60.70/60.70 inference(scs_inference,[],[144,299,327,303,251,253,254,252,239])).
% 60.70/60.70 cnf(360,plain,
% 60.70/60.70 (~P10(a17,a2,x3601,x3602)+P10(a15,a16,x3601,x3602)),
% 60.70/60.70 inference(scs_inference,[],[144,299,305,327,303,251,253,254,252,239,154,181])).
% 60.70/60.70 cnf(364,plain,
% 60.70/60.70 (~P10(a17,a2,x3641,x3642)+P10(a15,a16,x3642,x3641)),
% 60.70/60.70 inference(scs_inference,[],[146,144,299,305,327,303,251,253,254,252,239,154,181,240,165])).
% 60.70/60.70 cnf(366,plain,
% 60.70/60.70 (~P10(x3661,x3662,a17,a2)+P10(a15,a16,x3661,x3662)),
% 60.70/60.70 inference(scs_inference,[],[146,144,299,305,327,303,251,253,254,252,239,154,181,240,165,164])).
% 60.70/60.70 cnf(409,plain,
% 60.70/60.70 (~P9(a19,a1,a2,a18,x4091,x4092,x4091,x4092)),
% 60.70/60.70 inference(scs_inference,[],[303,356,275,254,251,253])).
% 60.70/60.70 cnf(418,plain,
% 60.70/60.70 (~P9(a19,a1,a18,a2,x4181,x4182,x4181,x4182)),
% 60.70/60.70 inference(scs_inference,[],[321,253])).
% 60.70/60.70 cnf(424,plain,
% 60.70/60.70 (~P9(x4241,x4242,x4241,x4242,a1,a19,a2,a18)),
% 60.70/60.70 inference(scs_inference,[],[356,275,321,253,252,254,251])).
% 60.70/60.70 cnf(426,plain,
% 60.70/60.70 (~P10(x4261,x4262,a19,a17)+P3(x4261,x4262,a2,a16)),
% 60.70/60.70 inference(scs_inference,[],[146,356,275,321,253,252,254,251,179])).
% 60.70/60.70 cnf(442,plain,
% 60.70/60.70 (~P9(a2,a18,a1,a19,x4421,x4422,x4421,x4422)),
% 60.70/60.70 inference(scs_inference,[],[269,254])).
% 60.70/60.70 cnf(444,plain,
% 60.70/60.70 (~P9(x4441,x4442,x4441,x4442,a1,a19,a18,a2)),
% 60.70/60.70 inference(scs_inference,[],[269,321,254,251])).
% 60.70/60.70 cnf(446,plain,
% 60.70/60.70 (~P9(a18,a2,a19,a1,x4461,x4462,x4461,x4462)),
% 60.70/60.70 inference(scs_inference,[],[269,321,352,254,251,253])).
% 60.70/60.70 cnf(460,plain,
% 60.70/60.70 (~P9(x4601,x4602,x4602,x4601,a1,a19,a2,a18)),
% 60.70/60.70 inference(scs_inference,[],[424,253])).
% 60.70/60.70 cnf(466,plain,
% 60.70/60.70 (~P9(x4661,x4662,x4661,x4662,a2,a18,a19,a1)),
% 60.70/60.70 inference(scs_inference,[],[273,323,352,424,253,252,254,251])).
% 60.70/60.70 cnf(476,plain,
% 60.70/60.70 (~P9(x4761,x4762,x4761,x4762,a19,a1,a2,a18)),
% 60.70/60.70 inference(scs_inference,[],[409,293,254,251])).
% 60.70/60.70 cnf(478,plain,
% 60.70/60.70 (~P9(x4781,x4782,x4782,x4781,a1,a19,a18,a2)),
% 60.70/60.70 inference(scs_inference,[],[409,444,293,254,251,253])).
% 60.70/60.70 cnf(485,plain,
% 60.70/60.70 (~P10(x4851,x4852,a1,a17)+P3(x4851,x4852,a2,a15)),
% 60.70/60.70 inference(scs_inference,[],[142,148,145,319,409,444,293,254,251,253,252,118,88,104,179])).
% 60.70/60.70 cnf(496,plain,
% 60.70/60.70 (~P9(x4961,x4962,x4962,x4961,a2,a18,a19,a1)),
% 60.70/60.70 inference(scs_inference,[],[323,466,252,253])).
% 60.70/60.70 cnf(500,plain,
% 60.70/60.70 (~P9(x5001,x5002,x5001,x5002,a19,a1,a18,a2)),
% 60.70/60.70 inference(scs_inference,[],[323,418,460,466,252,253,254,251])).
% 60.70/60.70 cnf(505,plain,
% 60.70/60.70 (~P11(a1,a2,a18,a2,a1,a19)),
% 60.70/60.70 inference(scs_inference,[],[148,323,418,460,466,252,253,254,251,230,116,213])).
% 60.70/60.70 cnf(507,plain,
% 60.70/60.70 (~P11(a1,a2,a19,a2,a1,a18)),
% 60.70/60.70 inference(scs_inference,[],[148,323,418,460,466,252,253,254,251,230,116,213,214])).
% 60.70/60.70 cnf(509,plain,
% 60.70/60.70 (~P11(a2,a19,a1,a1,a18,a2)),
% 60.70/60.70 inference(scs_inference,[],[148,323,418,460,466,252,253,254,251,230,116,213,214,215])).
% 60.70/60.70 cnf(516,plain,
% 60.70/60.70 (~P11(a1,a18,a2,a2,a19,a1)),
% 60.70/60.70 inference(scs_inference,[],[505,215])).
% 60.70/60.70 cnf(518,plain,
% 60.70/60.70 (~P11(a2,a1,a18,a1,a2,a19)),
% 60.70/60.70 inference(scs_inference,[],[505,507,215,213])).
% 60.70/60.70 cnf(522,plain,
% 60.70/60.70 (~P9(x5221,x5222,a1,a19,x5222,x5221,a18,a2)),
% 60.70/60.70 inference(scs_inference,[],[478,505,507,509,215,213,214,254])).
% 60.70/60.70 cnf(524,plain,
% 60.70/60.70 (~P9(x5241,x5242,x5241,x5242,a2,a18,a1,a19)),
% 60.70/60.70 inference(scs_inference,[],[442,478,505,507,509,215,213,214,254,251])).
% 60.70/60.70 cnf(528,plain,
% 60.70/60.70 (~P9(x5281,x5282,x5282,x5281,a19,a1,a2,a18)),
% 60.70/60.70 inference(scs_inference,[],[350,442,476,478,505,507,509,215,213,214,254,251,252,253])).
% 60.70/60.70 cnf(530,plain,
% 60.70/60.70 (~P11(a18,a1,a19,a1,a18,a2)),
% 60.70/60.70 inference(scs_inference,[],[350,442,476,478,505,507,509,215,213,214,254,251,252,253,230])).
% 60.70/60.70 cnf(537,plain,
% 60.70/60.70 (~P11(a2,a18,a1,a1,a19,a2)),
% 60.70/60.70 inference(scs_inference,[],[518,215])).
% 60.70/60.70 cnf(539,plain,
% 60.70/60.70 (~P11(a18,a1,a2,a19,a2,a1)),
% 60.70/60.70 inference(scs_inference,[],[518,516,215,214])).
% 60.70/60.70 cnf(541,plain,
% 60.70/60.70 (~P11(a1,a18,a2,a18,a1,a19)),
% 60.70/60.70 inference(scs_inference,[],[518,516,530,215,214,213])).
% 60.70/60.70 cnf(547,plain,
% 60.70/60.70 (~P9(x5471,x5472,x5472,x5471,a19,a1,a18,a2)),
% 60.70/60.70 inference(scs_inference,[],[444,496,500,518,516,530,215,214,213,254,252,253])).
% 60.70/60.70 cnf(551,plain,
% 60.70/60.70 (~P11(a19,a2,a18,a2,a19,a1)),
% 60.70/60.70 inference(scs_inference,[],[446,444,496,500,518,516,530,215,214,213,254,252,253,251,230])).
% 60.70/60.70 cnf(561,plain,
% 60.70/60.70 (~P11(a18,a2,a1,a19,a1,a2)),
% 60.70/60.70 inference(scs_inference,[],[539,537,213,215])).
% 60.70/60.70 cnf(573,plain,
% 60.70/60.70 (~P11(a2,a19,a1,a19,a2,a18)),
% 60.70/60.70 inference(scs_inference,[],[460,478,524,528,539,537,541,213,215,214,254,253,251,252,230])).
% 60.70/60.70 cnf(581,plain,
% 60.70/60.70 (~P11(a2,a19,a18,a19,a2,a1)),
% 60.70/60.70 inference(scs_inference,[],[551,561,213,214])).
% 60.70/60.70 cnf(583,plain,
% 60.70/60.70 (~P11(a19,a18,a2,a2,a1,a19)),
% 60.70/60.70 inference(scs_inference,[],[551,561,213,214,215])).
% 60.70/60.70 cnf(589,plain,
% 60.70/60.70 (~P9(x5891,x5892,x5892,x5891,a18,a2,a19,a1)),
% 60.70/60.70 inference(scs_inference,[],[478,547,551,561,213,214,215,254,251,252])).
% 60.70/60.70 cnf(593,plain,
% 60.70/60.70 (~P11(a18,a19,a1,a19,a18,a2)),
% 60.70/60.70 inference(scs_inference,[],[478,547,348,551,561,213,214,215,254,251,252,253,230])).
% 60.70/60.70 cnf(605,plain,
% 60.70/60.70 (~P11(a2,a1,a19,a19,a18,a2)),
% 60.70/60.70 inference(scs_inference,[],[573,215])).
% 60.70/60.70 cnf(627,plain,
% 60.70/60.71 (~P11(a19,a18,a1,a18,a19,a2)),
% 60.70/60.71 inference(scs_inference,[],[593,214])).
% 60.70/60.71 cnf(669,plain,
% 60.70/60.71 (P8(x6691,a15,a15,a17,x6691,a16,a16,a2)+~P1(x6691,a16,a2)+~P1(x6691,a15,a17)+~E(a1,x6692)),
% 60.70/60.71 inference(scs_inference,[],[142,144,333,589,522,289,581,583,627,213,214,215,254,251,252,253,230,88,227])).
% 60.70/60.71 cnf(671,plain,
% 60.70/60.71 (~P1(x6711,a16,a2)+~P1(x6711,a15,a17)+P8(x6711,a15,a15,a17,x6711,a16,a16,a2)),
% 60.70/60.71 inference(equality_inference,[],[669])).
% 60.70/60.71 cnf(1581,plain,
% 60.70/60.71 (P1(a2,a1,a15)),
% 60.70/60.71 inference(scs_inference,[],[142,150])).
% 60.70/60.71 cnf(1583,plain,
% 60.70/60.71 (P1(a1,a15,a2)),
% 60.70/60.71 inference(scs_inference,[],[142,150,151])).
% 60.70/60.71 cnf(1585,plain,
% 60.70/60.71 (P10(f7(a2,a17,a20,a18),a2,a2,a18)),
% 60.70/60.71 inference(scs_inference,[],[142,148,150,151,186])).
% 60.70/60.71 cnf(1587,plain,
% 60.70/60.71 (P10(a1,a17,a15,a2)),
% 60.70/60.71 inference(scs_inference,[],[142,148,145,150,151,186,165])).
% 60.70/60.71 cnf(1589,plain,
% 60.70/60.71 (P9(a15,a16,x15891,x15892,a17,a2,x15891,x15892)),
% 60.70/60.71 inference(scs_inference,[],[142,148,145,144,150,151,186,165,224])).
% 60.70/60.71 cnf(1591,plain,
% 60.70/60.71 (P3(a15,a16,a2,a17)),
% 60.70/60.71 inference(scs_inference,[],[142,148,145,144,150,151,186,165,224,163])).
% 60.70/60.71 cnf(1593,plain,
% 60.70/60.71 (P10(a2,a15,a1,a17)),
% 60.70/60.71 inference(scs_inference,[],[142,148,145,144,150,151,186,165,224,163,164])).
% 60.70/60.71 cnf(1595,plain,
% 60.70/60.71 (P3(a17,a2,a15,a16)),
% 60.70/60.71 inference(scs_inference,[],[142,148,145,144,150,151,186,165,224,163,164,162])).
% 60.70/60.71 cnf(1597,plain,
% 60.70/60.71 (P9(x15971,x15972,a15,a16,x15971,x15972,a17,a2)),
% 60.70/60.71 inference(scs_inference,[],[142,148,145,144,150,151,186,165,224,163,164,162,252])).
% 60.70/60.71 cnf(1599,plain,
% 60.70/60.71 (P9(a15,a16,a17,a2,x15991,x15992,x15991,x15992)),
% 60.70/60.71 inference(scs_inference,[],[142,148,145,144,150,151,186,165,224,163,164,162,252,254])).
% 60.70/60.71 cnf(1601,plain,
% 60.70/60.71 (P9(a17,a2,x16011,x16012,a15,a16,x16011,x16012)),
% 60.70/60.71 inference(scs_inference,[],[142,148,145,144,150,151,186,165,224,163,164,162,252,254,251])).
% 60.70/60.71 cnf(1603,plain,
% 60.70/60.71 (P9(a16,a15,x16031,x16032,a17,a2,x16031,x16032)),
% 60.70/60.71 inference(scs_inference,[],[142,148,145,144,150,151,186,165,224,163,164,162,252,254,251,253])).
% 60.70/60.71 cnf(1605,plain,
% 60.70/60.71 (P1(a15,a15,a2)),
% 60.70/60.71 inference(scs_inference,[],[142,148,145,144,150,151,186,165,224,163,164,162,252,254,251,253,154])).
% 60.70/60.71 cnf(1607,plain,
% 60.70/60.71 (P3(a15,a16,a15,a16)),
% 60.70/60.71 inference(scs_inference,[],[142,148,145,144,150,151,186,165,224,163,164,162,252,254,251,253,154,178])).
% 60.70/60.71 cnf(1611,plain,
% 60.70/60.71 (P3(a1,a17,a1,a17)),
% 60.70/60.71 inference(scs_inference,[],[142,148,145,144,150,151,186,165,224,163,164,162,252,254,251,253,154,178,239,179])).
% 60.70/60.71 cnf(1613,plain,
% 60.70/60.71 (P1(a15,a16,a16)),
% 60.70/60.71 inference(scs_inference,[],[142,148,145,144,150,151,186,165,224,163,164,162,252,254,251,253,154,178,239,179,159])).
% 60.70/60.71 cnf(1615,plain,
% 60.70/60.71 (P3(a17,a2,a17,a2)),
% 60.70/60.71 inference(scs_inference,[],[142,148,145,144,150,151,186,165,224,163,164,162,252,254,251,253,154,178,239,179,159,283])).
% 60.70/60.71 cnf(1617,plain,
% 60.70/60.71 (P3(a2,a15,a2,a15)),
% 60.70/60.71 inference(scs_inference,[],[142,148,145,144,150,151,186,165,224,163,164,162,252,254,251,253,154,178,239,179,159,283,485])).
% 60.70/60.71 cnf(1619,plain,
% 60.70/60.71 (P3(a16,a15,a17,a2)),
% 60.70/60.71 inference(scs_inference,[],[142,148,145,144,150,151,186,165,224,163,164,162,252,254,251,253,154,178,239,179,159,283,485,232])).
% 60.70/60.71 cnf(1621,plain,
% 60.70/60.71 (~P4(x16211,a1,a2)+~P4(x16211,a19,a18)),
% 60.70/60.71 inference(scs_inference,[],[142,325,148,145,144,150,151,186,165,224,163,164,162,252,254,251,253,154,178,239,179,159,283,485,232,156])).
% 60.70/60.71 cnf(1623,plain,
% 60.70/60.71 (~P4(x16231,a1,a2)+~P4(x16232,a19,a18)+~E(x16232,x16231)),
% 60.70/60.71 inference(scs_inference,[],[142,325,148,145,144,150,151,186,165,224,163,164,162,252,254,251,253,154,178,239,179,159,283,485,232,156,133])).
% 60.70/60.71 cnf(1625,plain,
% 60.70/60.71 (P10(f7(a2,a15,a16,a18),a2,a2,a18)),
% 60.70/60.71 inference(scs_inference,[],[147,186])).
% 60.70/60.71 cnf(1627,plain,
% 60.70/60.71 (P1(a15,a1,a2)),
% 60.70/60.71 inference(scs_inference,[],[1583,147,186,150])).
% 60.70/60.71 cnf(1629,plain,
% 60.70/60.71 (P1(a1,a17,a17)),
% 60.70/60.71 inference(scs_inference,[],[1583,1611,147,186,150,159])).
% 60.70/60.71 cnf(1633,plain,
% 60.70/60.71 (P10(a2,a15,a17,a1)),
% 60.70/60.71 inference(scs_inference,[],[1583,1593,1605,1611,147,186,150,159,151,165])).
% 60.70/60.71 cnf(1637,plain,
% 60.70/60.71 (P3(a2,a17,a15,a16)),
% 60.70/60.71 inference(scs_inference,[],[1595,1583,1591,1593,1605,1611,147,186,150,159,151,165,163,162])).
% 60.70/60.71 cnf(1639,plain,
% 60.70/60.71 (P9(a15,a16,x16391,x16392,a15,a16,x16391,x16392)),
% 60.70/60.71 inference(scs_inference,[],[1595,1607,1583,1591,1593,1605,1611,147,186,150,159,151,165,163,162,224])).
% 60.70/60.71 cnf(1641,plain,
% 60.70/60.71 (P10(a15,a2,a1,a17)),
% 60.70/60.71 inference(scs_inference,[],[1595,1607,1583,1587,1591,1593,1605,1611,147,186,150,159,151,165,163,162,224,164])).
% 60.70/60.71 cnf(1643,plain,
% 60.70/60.71 (P9(a17,a2,a15,a16,x16431,x16432,x16431,x16432)),
% 60.70/60.71 inference(scs_inference,[],[1595,1607,1599,1583,1587,1591,1593,1605,1611,147,186,150,159,151,165,163,162,224,164,252])).
% 60.70/60.71 cnf(1645,plain,
% 60.70/60.71 (P9(x16451,x16452,a15,a16,x16452,x16451,a17,a2)),
% 60.70/60.71 inference(scs_inference,[],[1595,1607,1597,1599,1583,1587,1591,1593,1605,1611,147,186,150,159,151,165,163,162,224,164,252,253])).
% 60.70/60.71 cnf(1647,plain,
% 60.70/60.71 (P9(x16471,x16472,x16471,x16472,a15,a16,a17,a2)),
% 60.70/60.71 inference(scs_inference,[],[1595,1607,1597,1599,1583,1587,1591,1593,1605,1611,147,186,150,159,151,165,163,162,224,164,252,253,254])).
% 60.70/60.71 cnf(1649,plain,
% 60.70/60.71 (P9(x16491,x16492,a17,a2,x16491,x16492,a15,a16)),
% 60.70/60.71 inference(scs_inference,[],[1595,1607,1597,1599,1583,1587,1591,1593,1605,1611,147,186,150,159,151,165,163,162,224,164,252,253,254,251])).
% 60.70/60.71 cnf(1651,plain,
% 60.70/60.71 (P6(a16,a2,a15,a15)),
% 60.70/60.71 inference(scs_inference,[],[1595,1607,1597,1599,1583,1587,1591,1593,1605,1611,147,186,150,159,151,165,163,162,224,164,252,253,254,251,235])).
% 60.70/60.71 cnf(1653,plain,
% 60.70/60.71 (P3(a16,a15,a15,a16)),
% 60.70/60.71 inference(scs_inference,[],[1595,1607,1597,1599,1603,1583,1587,1591,1593,1605,1611,147,186,150,159,151,165,163,162,224,164,252,253,254,251,235,239])).
% 60.70/60.71 cnf(1656,plain,
% 60.70/60.71 (~P10(a19,a1,f7(a2,a17,a20,a18),a2)),
% 60.70/60.71 inference(scs_inference,[],[1595,1607,1597,1599,1603,1583,1587,1591,1593,1605,1611,1585,281,147,186,150,159,151,165,163,162,224,164,252,253,254,251,235,239,179])).
% 60.70/60.71 cnf(1658,plain,
% 60.70/60.71 (P6(a2,a16,a15,a15)),
% 60.70/60.71 inference(scs_inference,[],[1595,1607,1597,1599,1603,1583,1587,1591,1593,1605,1611,1585,281,147,186,150,159,151,165,163,162,224,164,252,253,254,251,235,239,179,168])).
% 60.70/60.71 cnf(1660,plain,
% 60.70/60.71 (P6(a16,a15,a2,a15)),
% 60.70/60.71 inference(scs_inference,[],[1595,1607,1597,1599,1603,1583,1587,1591,1593,1605,1611,1585,281,147,186,150,159,151,165,163,162,224,164,252,253,254,251,235,239,179,168,169])).
% 60.70/60.71 cnf(1662,plain,
% 60.70/60.71 (P6(a16,a15,a15,a2)),
% 60.70/60.71 inference(scs_inference,[],[1595,1607,1597,1599,1603,1583,1587,1591,1593,1605,1611,1585,281,147,186,150,159,151,165,163,162,224,164,252,253,254,251,235,239,179,168,169,170])).
% 60.70/60.71 cnf(1666,plain,
% 60.70/60.71 (P3(a15,a2,a2,a15)),
% 60.70/60.71 inference(scs_inference,[],[1595,1607,1597,1599,1603,1583,1587,1591,1593,1605,1611,1585,281,147,186,150,159,151,165,163,162,224,164,252,253,254,251,235,239,179,168,169,170,283,485])).
% 60.70/60.71 cnf(1676,plain,
% 60.70/60.71 (P6(a2,a15,a16,a15)),
% 60.70/60.71 inference(scs_inference,[],[1658,169])).
% 60.70/60.71 cnf(1678,plain,
% 60.70/60.71 (P6(a15,a16,a2,a15)),
% 60.70/60.71 inference(scs_inference,[],[1658,1660,169,168])).
% 60.70/60.71 cnf(1680,plain,
% 60.70/60.71 (P6(a2,a15,a15,a16)),
% 60.70/60.71 inference(scs_inference,[],[1658,1660,169,168,170])).
% 60.70/60.71 cnf(1684,plain,
% 60.70/60.71 (P1(a15,a2,a1)),
% 60.70/60.71 inference(scs_inference,[],[1615,1627,1658,1660,169,168,170,159,151])).
% 60.70/60.71 cnf(1686,plain,
% 60.70/60.71 (P9(a2,a16,a2,a15,a15,a16,a15,a15)),
% 60.70/60.71 inference(scs_inference,[],[1615,1627,1658,1660,169,168,170,159,151,223])).
% 60.70/60.71 cnf(1688,plain,
% 60.70/60.71 (P1(a16,a15,a16)),
% 60.70/60.71 inference(scs_inference,[],[1615,1613,1627,1658,1660,169,168,170,159,151,223,150])).
% 60.70/60.71 cnf(1690,plain,
% 60.70/60.71 (P10(a15,a2,a17,a1)),
% 60.70/60.71 inference(scs_inference,[],[1615,1613,1627,1641,1658,1660,169,168,170,159,151,223,150,165])).
% 60.70/60.71 cnf(1692,plain,
% 60.70/60.71 (P9(a17,a2,x16921,x16922,a17,a2,x16921,x16922)),
% 60.70/60.71 inference(scs_inference,[],[1615,1613,1627,1641,1658,1660,169,168,170,159,151,223,150,165,224])).
% 60.70/60.71 cnf(1696,plain,
% 60.70/60.71 (P3(a15,a16,a16,a15)),
% 60.70/60.71 inference(scs_inference,[],[1615,1617,1613,1627,1641,1653,1658,1660,169,168,170,159,151,223,150,165,224,163,162])).
% 60.70/60.71 cnf(1698,plain,
% 60.70/60.71 (P10(a17,a1,a2,a15)),
% 60.70/60.71 inference(scs_inference,[],[1615,1617,1633,1613,1627,1641,1653,1658,1660,169,168,170,159,151,223,150,165,224,163,162,164])).
% 60.70/60.71 cnf(1702,plain,
% 60.70/60.71 (P9(a15,a16,a15,a16,x17021,x17022,x17021,x17022)),
% 60.70/60.71 inference(scs_inference,[],[1615,1617,1633,1613,1627,1639,1641,1653,1658,1660,169,168,170,159,151,223,150,165,224,163,162,164,252,254])).
% 60.70/60.71 cnf(1704,plain,
% 60.70/60.71 (P9(x17041,x17042,x17041,x17042,a17,a2,a15,a16)),
% 60.70/60.71 inference(scs_inference,[],[1615,1617,1633,1613,1627,1639,1643,1641,1653,1658,1660,169,168,170,159,151,223,150,165,224,163,162,164,252,254,251])).
% 60.70/60.71 cnf(1706,plain,
% 60.70/60.71 (P9(a2,a17,x17061,x17062,a15,a16,x17061,x17062)),
% 60.70/60.71 inference(scs_inference,[],[1615,1617,1633,1613,1627,1601,1639,1643,1641,1653,1658,1660,169,168,170,159,151,223,150,165,224,163,162,164,252,254,251,253])).
% 60.70/60.71 cnf(1708,plain,
% 60.70/60.71 (P6(a2,a15,a15,a15)),
% 60.70/60.71 inference(scs_inference,[],[1615,1617,1633,1613,1627,1601,1639,1643,1641,1651,1653,1658,1660,169,168,170,159,151,223,150,165,224,163,162,164,252,254,251,253,184])).
% 60.70/60.71 cnf(1710,plain,
% 60.70/60.71 (P9(a2,a16,a2,a15,a17,a2,a15,a15)),
% 60.70/60.71 inference(scs_inference,[],[1615,1617,1633,1613,1627,1589,1601,1639,1643,1641,1651,1653,1658,1660,169,168,170,159,151,223,150,165,224,163,162,164,252,254,251,253,184,261])).
% 60.70/60.71 cnf(1713,plain,
% 60.70/60.71 (P6(a16,a16,a15,a16)),
% 60.70/60.71 inference(scs_inference,[],[1615,1617,1633,1613,1627,1589,1601,1639,1643,1641,1651,1653,1658,1660,169,168,170,159,151,223,150,165,224,163,162,164,252,254,251,253,184,261,235])).
% 60.70/60.71 cnf(1723,plain,
% 60.70/60.71 (P5(a16,a16,a16,a16)),
% 60.70/60.71 inference(scs_inference,[],[142,1615,1617,1633,1613,1627,1589,1601,1639,1643,1641,1651,1653,1658,1660,1666,1656,1583,145,169,168,170,159,151,223,150,165,224,163,162,164,252,254,251,253,184,261,235,240,179,205,206,250])).
% 60.70/60.71 cnf(1725,plain,
% 60.70/60.71 (P9(a16,a16,a16,a16,a16,a16,a16,a16)),
% 60.70/60.71 inference(scs_inference,[],[142,1615,1617,1633,1613,1627,1589,1601,1639,1643,1641,1651,1653,1658,1660,1666,1656,1583,145,169,168,170,159,151,223,150,165,224,163,162,164,252,254,251,253,184,261,235,240,179,205,206,250,225])).
% 60.70/60.71 cnf(1731,plain,
% 60.70/60.71 (P2(a16,a16,a16,a16)),
% 60.70/60.71 inference(scs_inference,[],[142,1615,1617,1633,1613,1627,1589,1601,1639,1643,1641,1651,1653,1658,1660,1666,1656,1583,145,169,168,170,159,151,223,150,165,224,163,162,164,252,254,251,253,184,261,235,240,179,205,206,250,225,232,172,183])).
% 60.70/60.71 cnf(1737,plain,
% 60.70/60.71 (P10(a16,a16,a16,a16)),
% 60.70/60.71 inference(scs_inference,[],[142,1615,1617,1633,1613,1627,1589,1601,1639,1643,1641,1651,1653,1658,1660,1666,1656,1583,145,169,168,170,159,151,223,150,165,224,163,162,164,252,254,251,253,184,261,235,240,179,205,206,250,225,232,172,183,244,248,180])).
% 60.70/60.71 cnf(1741,plain,
% 60.70/60.71 (P3(x17411,x17412,x17411,x17412)),
% 60.70/60.71 inference(scs_inference,[],[142,1615,1617,1633,1613,1627,1589,1601,1639,1643,1647,1641,1651,1653,1658,1660,1666,1656,1583,145,144,169,168,170,159,151,223,150,165,224,163,162,164,252,254,251,253,184,261,235,240,179,205,206,250,225,232,172,183,244,248,180,189,239])).
% 60.70/60.71 cnf(1745,plain,
% 60.70/60.71 (P8(a16,a16,a15,a16,a16,a16,a15,a16)),
% 60.70/60.71 inference(scs_inference,[],[142,1615,1617,1633,1613,1627,1589,1601,1639,1643,1647,1641,1651,1653,1658,1660,1666,1656,1583,145,144,169,168,170,159,151,223,150,165,224,163,162,164,252,254,251,253,184,261,235,240,179,205,206,250,225,232,172,183,244,248,180,189,239,227,256])).
% 60.70/60.71 cnf(1747,plain,
% 60.70/60.71 (P8(a16,a15,a16,a16,a15,a16,a16,a16)),
% 60.70/60.71 inference(scs_inference,[],[142,1615,1617,1633,1613,1627,1589,1601,1639,1643,1647,1641,1651,1653,1658,1660,1666,1656,1583,145,144,169,168,170,159,151,223,150,165,224,163,162,164,252,254,251,253,184,261,235,240,179,205,206,250,225,232,172,183,244,248,180,189,239,227,256,257])).
% 60.70/60.71 cnf(1749,plain,
% 60.70/60.71 (P8(a15,a16,a15,a16,a16,a16,a16,a16)),
% 60.70/60.71 inference(scs_inference,[],[142,1615,1617,1633,1613,1627,1589,1601,1639,1643,1647,1641,1651,1653,1658,1660,1666,1656,1583,145,144,169,168,170,159,151,223,150,165,224,163,162,164,252,254,251,253,184,261,235,240,179,205,206,250,225,232,172,183,244,248,180,189,239,227,256,257,258])).
% 60.70/60.71 cnf(1751,plain,
% 60.70/60.71 (P10(f7(a16,a16,a16,a16),a16,a16,a16)),
% 60.70/60.71 inference(scs_inference,[],[142,1615,1617,1633,1613,1627,1589,1601,1639,1643,1647,1641,1651,1653,1658,1660,1666,1656,1583,145,144,169,168,170,159,151,223,150,165,224,163,162,164,252,254,251,253,184,261,235,240,179,205,206,250,225,232,172,183,244,248,180,189,239,227,256,257,258,186])).
% 60.70/60.71 cnf(1755,plain,
% 60.70/60.71 (P8(a15,a16,a16,a16,a16,a15,a16,a16)),
% 60.70/60.71 inference(scs_inference,[],[1747,255])).
% 60.70/60.71 cnf(1759,plain,
% 60.70/60.71 (P8(a16,a15,a15,a16,a16,a16,a16,a16)),
% 60.70/60.71 inference(scs_inference,[],[1745,1747,1749,255,258,257])).
% 60.70/60.71 cnf(1761,plain,
% 60.70/60.71 (P6(a15,a2,a16,a15)),
% 60.70/60.71 inference(scs_inference,[],[1678,1745,1747,1749,255,258,257,169])).
% 60.70/60.71 cnf(1763,plain,
% 60.70/60.71 (P6(a15,a16,a15,a2)),
% 60.70/60.71 inference(scs_inference,[],[1678,1745,1747,1749,255,258,257,169,170])).
% 60.70/60.71 cnf(1765,plain,
% 60.70/60.71 (P1(x17651,x17652,x17652)),
% 60.70/60.71 inference(scs_inference,[],[1741,1678,1745,1747,1749,255,258,257,169,170,159])).
% 60.70/60.71 cnf(1767,plain,
% 60.70/60.71 (P8(a16,a16,a16,a15,a16,a16,a15,a16)),
% 60.70/60.71 inference(scs_inference,[],[1741,1678,1745,1747,1749,255,258,257,169,170,159,256])).
% 60.70/60.71 cnf(1769,plain,
% 60.70/60.71 (P6(a15,a2,a15,a16)),
% 60.70/60.71 inference(scs_inference,[],[1741,1678,1680,1745,1747,1749,255,258,257,169,170,159,256,168])).
% 60.70/60.71 cnf(1771,plain,
% 60.70/60.71 (P9(a15,a16,a15,a15,a2,a16,a2,a15)),
% 60.70/60.71 inference(scs_inference,[],[1741,1662,1678,1680,1745,1747,1749,255,258,257,169,170,159,256,168,223])).
% 60.70/60.71 cnf(1773,plain,
% 60.70/60.71 (P1(a17,a1,a17)),
% 60.70/60.71 inference(scs_inference,[],[1741,1662,1629,1678,1680,1745,1747,1749,255,258,257,169,170,159,256,168,223,150])).
% 60.70/60.71 cnf(1775,plain,
% 60.70/60.71 (P1(a16,a16,a15)),
% 60.70/60.71 inference(scs_inference,[],[1741,1662,1629,1678,1680,1688,1745,1747,1749,255,258,257,169,170,159,256,168,223,150,151])).
% 60.70/60.71 cnf(1779,plain,
% 60.70/60.71 (P9(x17791,x17792,x17793,x17794,x17791,x17792,x17793,x17794)),
% 60.70/60.71 inference(scs_inference,[],[1741,1662,1629,1678,1680,1688,1698,1745,1747,1749,255,258,257,169,170,159,256,168,223,150,151,165,224])).
% 60.70/60.71 cnf(1781,plain,
% 60.70/60.71 (P10(a2,a18,f7(a2,a15,a16,a18),a2)),
% 60.70/60.71 inference(scs_inference,[],[1741,1662,1629,1678,1680,1688,1698,1745,1747,1749,1625,255,258,257,169,170,159,256,168,223,150,151,165,224,164])).
% 60.70/60.71 cnf(1783,plain,
% 60.70/60.71 (P3(x17831,x17832,x17832,x17831)),
% 60.70/60.71 inference(scs_inference,[],[1741,1662,1629,1678,1680,1688,1698,1745,1747,1749,1625,255,258,257,169,170,159,256,168,223,150,151,165,224,164,163])).
% 60.70/60.71 cnf(1785,plain,
% 60.70/60.71 (P9(x17851,x17852,a2,a17,x17851,x17852,a15,a16)),
% 60.70/60.71 inference(scs_inference,[],[1741,1662,1706,1629,1678,1680,1688,1698,1745,1747,1749,1625,255,258,257,169,170,159,256,168,223,150,151,165,224,164,163,252])).
% 60.70/60.71 cnf(1789,plain,
% 60.70/60.71 (P9(x17891,x17892,a17,a2,x17892,x17891,a15,a16)),
% 60.70/60.71 inference(scs_inference,[],[1741,1662,1649,1692,1706,1629,1678,1680,1688,1698,1745,1747,1749,1625,255,258,257,169,170,159,256,168,223,150,151,165,224,164,163,252,254,253])).
% 60.70/60.71 cnf(1794,plain,
% 60.70/60.71 (~P1(x17941,x17942,x17943)+P4(x17941,x17942,x17943)+~P5(x17941,x17942,x17941,x17943)),
% 60.70/60.71 inference(rename_variables,[],[160])).
% 60.70/60.71 cnf(1797,plain,
% 60.70/60.71 (P1(a16,a16,f3(a16,a16,a16))),
% 60.70/60.71 inference(scs_inference,[],[1741,1662,1649,1692,1702,1706,1629,1678,1680,1688,1698,1723,1737,1745,1747,1749,1625,255,258,257,169,170,159,256,168,223,150,151,165,224,164,163,252,254,253,251,160,222,175])).
% 60.70/60.71 cnf(1807,plain,
% 60.70/60.71 (P5(a15,a16,a15,a16)),
% 60.70/60.71 inference(scs_inference,[],[1741,1662,1649,1692,1702,1706,1629,1678,1680,1688,1698,1723,1737,1745,1747,1749,1625,255,258,257,169,170,159,256,168,223,150,151,165,224,164,163,252,254,253,251,160,222,175,187,192,196,202,242])).
% 60.70/60.71 cnf(1813,plain,
% 60.70/60.71 (P5(a16,a16,a16,f27(a16,a16,a16,a16,a16))),
% 60.70/60.71 inference(scs_inference,[],[1741,1662,1649,1692,1702,1706,1629,1678,1680,1688,1698,1723,1737,1745,1747,1749,1625,255,258,257,169,170,159,256,168,223,150,151,165,224,164,163,252,254,253,251,160,222,175,187,192,196,202,242,197,203,198])).
% 60.70/60.71 cnf(1825,plain,
% 60.70/60.71 (P2(a16,a16,f3(a16,a16,a16),f3(a16,a16,a16))),
% 60.70/60.71 inference(scs_inference,[],[1741,1662,1649,1692,1702,1706,1629,1678,1680,1688,1698,1723,1725,1737,1745,1747,1749,1625,255,258,257,169,170,159,256,168,223,150,151,165,224,164,163,252,254,253,251,160,222,175,187,192,196,202,242,197,203,198,200,245,262,188,157,183])).
% 60.70/60.71 cnf(1827,plain,
% 60.70/60.71 (P10(a15,a15,a16,a16)),
% 60.70/60.71 inference(scs_inference,[],[1741,1662,1649,1692,1702,1706,1629,1678,1680,1688,1698,1723,1725,1737,1745,1747,1749,1625,255,258,257,169,170,159,256,168,223,150,151,165,224,164,163,252,254,253,251,160,222,175,187,192,196,202,242,197,203,198,200,245,262,188,157,183,180])).
% 60.70/60.71 cnf(1831,plain,
% 60.70/60.71 (P10(a16,f3(a16,a16,a16),f3(a16,a16,a16),f3(a16,a16,a16))),
% 60.70/60.71 inference(scs_inference,[],[1741,1662,1649,1692,1702,1706,1629,1678,1680,1688,1698,1723,1725,1737,1745,1747,1749,1625,255,258,257,169,170,159,256,168,223,150,151,165,224,164,163,252,254,253,251,160,222,175,187,192,196,202,242,197,203,198,200,245,262,188,157,183,180,235,171])).
% 60.70/60.71 cnf(1838,plain,
% 60.70/60.71 (~P10(a19,a1,f7(a2,a15,a16,a18),a2)),
% 60.70/60.71 inference(scs_inference,[],[1741,1662,1649,1692,1702,1706,1629,1678,1680,1688,1698,1723,1725,1731,1737,1745,1747,1749,1625,281,255,258,257,169,170,159,256,168,223,150,151,165,224,164,163,252,254,253,251,160,222,175,187,192,196,202,242,197,203,198,200,245,262,188,157,183,180,235,171,226,240,179])).
% 60.70/60.71 cnf(1843,plain,
% 60.70/60.71 (P6(a16,f3(a16,a16,a16),f3(a16,a16,a16),f3(a16,a16,a16))),
% 60.70/60.71 inference(scs_inference,[],[1741,1662,1696,1649,1692,1702,1706,1629,1678,1680,1688,1698,1723,1725,1731,1737,1745,1747,1749,1625,281,255,258,257,169,170,159,256,168,223,150,151,165,224,164,163,252,254,253,251,160,222,175,187,192,196,202,242,197,203,198,200,245,262,188,157,183,180,235,171,226,240,179,239,195])).
% 60.70/60.71 cnf(1845,plain,
% 60.70/60.71 (P4(f6(a16,a16,a16),a16,a16)),
% 60.70/60.71 inference(scs_inference,[],[1741,1662,1696,1649,1692,1702,1706,1629,1678,1680,1688,1698,1723,1725,1731,1737,1745,1747,1749,1625,281,255,258,257,169,170,159,256,168,223,150,151,165,224,164,163,252,254,253,251,160,222,175,187,192,196,202,242,197,203,198,200,245,262,188,157,183,180,235,171,226,240,179,239,195,185])).
% 60.70/60.71 cnf(1848,plain,
% 60.70/60.71 (P3(x18481,x18482,x18481,x18482)),
% 60.70/60.71 inference(rename_variables,[],[1741])).
% 60.70/60.71 cnf(1850,plain,
% 60.70/60.71 (P4(a16,x18501,x18501)),
% 60.70/60.71 inference(scs_inference,[],[1741,1848,1662,1696,1649,1692,1702,1706,1629,1678,1680,1688,1698,1723,1725,1731,1737,1745,1747,1749,1625,281,255,258,257,169,170,159,256,168,223,150,151,165,224,164,163,252,254,253,251,160,222,175,187,192,196,202,242,197,203,198,200,245,262,188,157,183,180,235,171,226,240,179,239,195,185,191,174])).
% 60.70/60.71 cnf(1852,plain,
% 60.70/60.71 (P3(x18521,x18522,x18521,x18522)),
% 60.70/60.71 inference(rename_variables,[],[1741])).
% 60.70/60.71 cnf(1861,plain,
% 60.70/60.71 (P1(f21(a16,x18611),a16,x18611)),
% 60.70/60.71 inference(scs_inference,[],[142,1741,1848,1852,1662,1696,1649,1692,1702,1706,1629,1678,1680,1688,1698,1723,1725,1731,1737,1745,1747,1749,1625,281,1666,1605,1583,255,258,257,169,170,159,256,168,223,150,151,165,224,164,163,252,254,253,251,160,222,175,187,192,196,202,242,197,203,198,200,245,262,188,157,183,180,235,171,226,240,179,239,195,185,191,174,205,206,158,152])).
% 60.70/60.71 cnf(1863,plain,
% 60.70/60.71 (P4(f21(a16,x18631),x18631,a16)),
% 60.70/60.71 inference(scs_inference,[],[142,1741,1848,1852,1662,1696,1649,1692,1702,1706,1629,1678,1680,1688,1698,1723,1725,1731,1737,1745,1747,1749,1625,281,1666,1605,1583,255,258,257,169,170,159,256,168,223,150,151,165,224,164,163,252,254,253,251,160,222,175,187,192,196,202,242,197,203,198,200,245,262,188,157,183,180,235,171,226,240,179,239,195,185,191,174,205,206,158,152,153])).
% 60.70/60.71 cnf(1865,plain,
% 60.70/60.71 (P5(f25(a16,a16,a16,a16,a16,a16),a16,f25(a16,a16,a16,a16,a16,a16),a16)),
% 60.70/60.71 inference(scs_inference,[],[142,1741,1848,1852,1662,1696,1649,1692,1702,1706,1629,1678,1680,1688,1698,1723,1725,1731,1737,1745,1747,1749,1625,281,1666,1605,1583,255,258,257,169,170,159,256,168,223,150,151,165,224,164,163,252,254,253,251,160,222,175,187,192,196,202,242,197,203,198,200,245,262,188,157,183,180,235,171,226,240,179,239,195,185,191,174,205,206,158,152,153,155])).
% 60.70/60.71 cnf(1867,plain,
% 60.70/60.71 (P5(a16,f3(a16,a16,a16),a16,a16)),
% 60.70/60.71 inference(scs_inference,[],[142,1741,1848,1852,1662,1696,1649,1692,1702,1706,1629,1678,1680,1688,1698,1723,1725,1731,1737,1745,1747,1749,1625,281,1666,1605,1583,255,258,257,169,170,159,256,168,223,150,151,165,224,164,163,252,254,253,251,160,222,175,187,192,196,202,242,197,203,198,200,245,262,188,157,183,180,235,171,226,240,179,239,195,185,191,174,205,206,158,152,153,155,166])).
% 60.70/60.71 cnf(1871,plain,
% 60.70/60.71 (P10(a15,a16,f12(a16,a16,a16,a15,a16),a16)),
% 60.70/60.71 inference(scs_inference,[],[142,1741,1848,1852,1662,1696,1649,1692,1702,1706,1629,1678,1680,1688,1698,1723,1725,1731,1737,1745,1747,1749,1625,281,1666,1605,1583,255,258,257,169,170,159,256,168,223,150,151,165,224,164,163,252,254,253,251,160,222,175,187,192,196,202,242,197,203,198,200,245,262,188,157,183,180,235,171,226,240,179,239,195,185,191,174,205,206,158,152,153,155,166,167,366])).
% 60.70/60.71 cnf(1875,plain,
% 60.70/60.71 (P3(a16,a16,a16,f3(a16,a16,a16))),
% 60.70/60.71 inference(scs_inference,[],[142,1741,1848,1852,1662,1696,1649,1692,1702,1706,1629,1678,1680,1688,1698,1723,1725,1731,1737,1745,1747,1749,1625,281,1666,1605,1583,255,258,257,169,170,159,256,168,223,150,151,165,224,164,163,252,254,253,251,160,222,175,187,192,196,202,242,197,203,198,200,245,262,188,157,183,180,235,171,226,240,179,239,195,185,191,174,205,206,158,152,153,155,166,167,366,225,232])).
% 60.70/60.71 cnf(1877,plain,
% 60.70/60.71 (P3(a16,a16,f25(a16,a16,a16,a16,a16,a16),a16)),
% 60.70/60.71 inference(scs_inference,[],[142,1741,1848,1852,1662,1696,1649,1692,1702,1706,1629,1678,1680,1688,1698,1723,1725,1731,1737,1745,1747,1749,1625,281,1666,1605,1583,255,258,257,169,170,159,256,168,223,150,151,165,224,164,163,252,254,253,251,160,222,175,187,192,196,202,242,197,203,198,200,245,262,188,157,183,180,235,171,226,240,179,239,195,185,191,174,205,206,158,152,153,155,166,167,366,225,232,162])).
% 60.70/60.71 cnf(1883,plain,
% 60.70/60.71 (P9(a16,a16,a16,f3(a16,a16,a16),f3(a16,a16,a16),a16,f3(a16,a16,a16),f3(a16,a16,a16))),
% 60.70/60.71 inference(scs_inference,[],[142,1741,1848,1852,1662,1696,1649,1692,1702,1706,1629,1678,1680,1688,1698,1723,1725,1731,1737,1745,1747,1749,1625,281,1666,1605,1583,255,258,257,169,170,159,256,168,223,150,151,165,224,164,163,252,254,253,251,160,222,175,187,192,196,202,242,197,203,198,200,245,262,188,157,183,180,235,171,226,240,179,239,195,185,191,174,205,206,158,152,153,155,166,167,366,225,232,162,1794,190,228])).
% 60.70/60.71 cnf(1885,plain,
% 60.70/60.71 (P3(f25(x18851,x18851,a16,a16,a16,a16),a16,x18851,a16)),
% 60.70/60.71 inference(scs_inference,[],[142,1741,1848,1852,1662,1696,1649,1692,1702,1706,1629,1678,1680,1688,1698,1723,1725,1731,1737,1745,1747,1749,1625,281,1666,1605,1583,255,258,257,169,170,159,256,168,223,150,151,165,224,164,163,252,254,253,251,160,222,175,187,192,196,202,242,197,203,198,200,245,262,188,157,183,180,235,171,226,240,179,239,195,185,191,174,205,206,158,152,153,155,166,167,366,225,232,162,1794,190,228,204])).
% 60.70/60.71 cnf(1887,plain,
% 60.70/60.71 (P3(a16,a16,x18871,x18871)),
% 60.70/60.71 inference(scs_inference,[],[142,1741,1848,1852,1662,1696,1649,1692,1702,1706,1629,1678,1680,1688,1698,1723,1725,1731,1737,1745,1747,1749,1625,281,1666,1605,1583,255,258,257,169,170,159,256,168,223,150,151,165,224,164,163,252,254,253,251,160,222,175,187,192,196,202,242,197,203,198,200,245,262,188,157,183,180,235,171,226,240,179,239,195,185,191,174,205,206,158,152,153,155,166,167,366,225,232,162,1794,190,228,204,156])).
% 60.70/60.71 cnf(1905,plain,
% 60.70/60.71 (P3(f25(a15,a15,a16,a16,a16,a16),a16,a17,a2)),
% 60.70/60.71 inference(scs_inference,[],[1807,1863,1885,152,167,283])).
% 60.70/60.71 cnf(1910,plain,
% 60.70/60.71 (P9(a15,a16,a16,a16,a16,a16,a15,a16)),
% 60.70/60.71 inference(scs_inference,[],[1759,1807,1863,1885,152,167,283,255,225])).
% 60.70/60.71 cnf(1912,plain,
% 60.70/60.71 (P8(a16,a15,a16,a16,a16,a15,a16,a16)),
% 60.70/60.71 inference(scs_inference,[],[1755,1759,1807,1863,1885,152,167,283,255,225,257])).
% 60.70/60.71 cnf(1914,plain,
% 60.70/60.71 (P5(a16,x19141,a16,x19141)),
% 60.70/60.71 inference(scs_inference,[],[1850,1755,1759,1807,1863,1885,152,167,283,255,225,257,155])).
% 60.70/60.71 cnf(1916,plain,
% 60.70/60.71 (P8(a15,a16,a16,a15,a16,a16,a16,a16)),
% 60.70/60.71 inference(scs_inference,[],[1850,1755,1759,1807,1863,1885,152,167,283,255,225,257,155,258])).
% 60.70/60.71 cnf(1918,plain,
% 60.70/60.71 (P6(a16,a15,a16,a16)),
% 60.70/60.71 inference(scs_inference,[],[1713,1850,1755,1759,1807,1863,1885,152,167,283,255,225,257,155,258,169])).
% 60.70/60.71 cnf(1922,plain,
% 60.70/60.71 (P6(a15,a2,a15,a15)),
% 60.70/60.71 inference(scs_inference,[],[1713,1850,1708,1755,1759,1807,1813,1863,1885,152,167,283,255,225,257,155,258,169,166,168])).
% 60.70/60.71 cnf(1924,plain,
% 60.70/60.71 (P6(a16,a16,a16,a15)),
% 60.70/60.71 inference(scs_inference,[],[1713,1850,1708,1755,1759,1807,1813,1863,1885,152,167,283,255,225,257,155,258,169,166,168,170])).
% 60.70/60.71 cnf(1926,plain,
% 60.70/60.71 (P8(a16,a16,a15,a16,a16,a16,a16,a15)),
% 60.70/60.71 inference(scs_inference,[],[1713,1850,1708,1755,1759,1807,1813,1863,1885,152,167,283,255,225,257,155,258,169,166,168,170,256])).
% 60.70/60.71 cnf(1928,plain,
% 60.70/60.71 (P9(a16,a15,a16,a2,a15,a15,a15,a2)),
% 60.70/60.71 inference(scs_inference,[],[1713,1761,1850,1708,1755,1759,1807,1813,1863,1885,152,167,283,255,225,257,155,258,169,166,168,170,256,223])).
% 60.70/60.71 cnf(1930,plain,
% 60.70/60.71 (P10(a2,a18,a2,f7(a2,a15,a16,a18))),
% 60.70/60.71 inference(scs_inference,[],[1713,1761,1850,1708,1755,1759,1807,1813,1863,1885,1781,152,167,283,255,225,257,155,258,169,166,168,170,256,223,165])).
% 60.70/60.71 cnf(1932,plain,
% 60.70/60.71 (P1(x19321,x19322,x19321)),
% 60.70/60.71 inference(scs_inference,[],[1765,1713,1761,1850,1708,1755,1759,1807,1813,1863,1885,1781,152,167,283,255,225,257,155,258,169,166,168,170,256,223,165,150])).
% 60.70/60.71 cnf(1936,plain,
% 60.70/60.71 (P9(x19361,x19362,x19363,x19364,x19362,x19361,x19363,x19364)),
% 60.70/60.71 inference(scs_inference,[],[1783,1765,1713,1761,1850,1708,1755,1759,1773,1807,1813,1863,1885,1781,152,167,283,255,225,257,155,258,169,166,168,170,256,223,165,150,151,224])).
% 60.70/60.71 cnf(1940,plain,
% 60.70/60.71 (P3(x19401,x19401,a16,a16)),
% 60.70/60.71 inference(scs_inference,[],[1783,1765,1713,1761,1850,1887,1708,1755,1759,1773,1807,1827,1813,1863,1885,1781,152,167,283,255,225,257,155,258,169,166,168,170,256,223,165,150,151,224,164,162])).
% 60.70/60.71 cnf(1942,plain,
% 60.70/60.71 (P3(a16,a15,a2,a17)),
% 60.70/60.71 inference(scs_inference,[],[1783,1765,1619,1713,1761,1850,1887,1708,1755,1759,1773,1807,1827,1813,1863,1885,1781,152,167,283,255,225,257,155,258,169,166,168,170,256,223,165,150,151,224,164,162,163])).
% 60.70/60.71 cnf(1944,plain,
% 60.70/60.71 (P9(a17,a2,x19441,x19442,a15,a16,x19442,x19441)),
% 60.70/60.71 inference(scs_inference,[],[1783,1765,1619,1713,1761,1850,1789,1887,1708,1755,1759,1773,1807,1827,1813,1863,1885,1781,152,167,283,255,225,257,155,258,169,166,168,170,256,223,165,150,151,224,164,162,163,252])).
% 60.70/60.71 cnf(1946,plain,
% 60.70/60.71 (P9(x19461,x19462,x19461,x19462,x19463,x19464,x19463,x19464)),
% 60.70/60.71 inference(scs_inference,[],[1779,1783,1765,1619,1713,1761,1850,1789,1887,1708,1755,1759,1773,1807,1827,1813,1863,1885,1781,152,167,283,255,225,257,155,258,169,166,168,170,256,223,165,150,151,224,164,162,163,252,254])).
% 60.70/60.71 cnf(1950,plain,
% 60.70/60.71 (P9(x19501,x19502,a15,a16,x19501,x19502,a2,a17)),
% 60.70/60.71 inference(scs_inference,[],[1779,1783,1765,1619,1713,1761,1850,1704,1785,1789,1887,1708,1755,1759,1773,1807,1827,1813,1863,1885,1781,152,167,283,255,225,257,155,258,169,166,168,170,256,223,165,150,151,224,164,162,163,252,254,253,251])).
% 60.70/60.71 cnf(1952,plain,
% 60.70/60.71 (P5(a16,f3(a16,a16,a16),a16,f27(a16,a16,a16,a16,a16))),
% 60.70/60.71 inference(scs_inference,[],[1779,1783,1765,1619,1713,1761,1850,1704,1785,1789,1887,1708,1755,1759,1773,1807,1827,1813,1863,1885,1867,1781,152,167,283,255,225,257,155,258,169,166,168,170,256,223,165,150,151,224,164,162,163,252,254,253,251,182])).
% 60.70/60.71 cnf(1962,plain,
% 60.70/60.71 (P8(a16,x19621,x19621,x19621,a16,x19621,x19621,x19621)),
% 60.70/60.71 inference(scs_inference,[],[1779,1783,1765,1619,1713,1761,1850,1704,1785,1789,1887,1708,1755,1759,1773,1807,1827,1813,1863,1885,1867,1781,152,167,283,255,225,257,155,258,169,166,168,170,256,223,165,150,151,224,164,162,163,252,254,253,251,182,192,248,203,244,222])).
% 60.70/60.71 cnf(1964,plain,
% 60.70/60.71 (P4(f25(x19641,x19641,x19641,x19641,a16,a16),x19641,x19641)),
% 60.70/60.71 inference(scs_inference,[],[1779,1783,1765,1619,1713,1761,1850,1704,1785,1789,1887,1708,1755,1759,1773,1807,1827,1813,1863,1885,1867,1781,152,167,283,255,225,257,155,258,169,166,168,170,256,223,165,150,151,224,164,162,163,252,254,253,251,182,192,248,203,244,222,202])).
% 60.70/60.71 cnf(1968,plain,
% 60.70/60.71 (P10(f12(a16,a16,a16,x19681,x19681),a16,x19681,x19681)),
% 60.70/60.71 inference(scs_inference,[],[1779,1783,1765,1619,1713,1761,1850,1704,1785,1789,1887,1708,1755,1759,1773,1807,1827,1813,1863,1885,1867,1781,1723,1737,152,167,283,255,225,257,155,258,169,166,168,170,256,223,165,150,151,224,164,162,163,252,254,253,251,182,192,248,203,244,222,202,242,197])).
% 60.70/60.71 cnf(1969,plain,
% 60.70/60.71 (P1(x19691,x19692,x19692)),
% 60.70/60.71 inference(rename_variables,[],[1765])).
% 60.70/60.71 cnf(1972,plain,
% 60.70/60.71 (P4(a16,x19721,x19721)),
% 60.70/60.71 inference(rename_variables,[],[1850])).
% 60.70/60.71 cnf(1974,plain,
% 60.70/60.71 (P2(a15,a16,a16,a16)),
% 60.70/60.71 inference(scs_inference,[],[1779,1783,1765,1619,1713,1761,1850,1704,1785,1789,1887,1708,1755,1759,1773,1807,1827,1751,1813,1863,1885,1867,1781,1723,1737,152,167,283,255,225,257,155,258,169,166,168,170,256,223,165,150,151,224,164,162,163,252,254,253,251,182,192,248,203,244,222,202,242,197,172,183])).
% 60.70/60.71 cnf(1978,plain,
% 60.70/60.71 (P6(a15,a15,a1,a2)),
% 60.70/60.71 inference(scs_inference,[],[142,1779,1783,1765,1619,1713,1761,1850,1704,1785,1789,1887,1708,1755,1759,1773,1807,1827,1751,1813,1863,1865,1885,1867,1781,1723,1737,152,167,283,255,225,257,155,258,169,166,168,170,256,223,165,150,151,224,164,162,163,252,254,253,251,182,192,248,203,244,222,202,242,197,172,183,180,235])).
% 60.70/60.71 cnf(1983,plain,
% 60.70/60.71 (P4(a16,x19831,x19831)),
% 60.70/60.71 inference(rename_variables,[],[1850])).
% 60.70/60.71 cnf(1985,plain,
% 60.70/60.71 (~P9(a19,a1,f7(a2,a15,a16,a18),a2,a15,a2,a17,a1)),
% 60.70/60.71 inference(scs_inference,[],[142,1779,1783,1765,1619,1690,1713,1761,1850,1972,1704,1785,1789,1887,1708,1755,1759,1773,1807,1827,1751,1813,1831,1863,1865,1825,1885,1875,1867,1781,1838,1723,1737,152,167,283,255,225,257,155,258,169,166,168,170,256,223,165,150,151,224,164,162,163,252,254,253,251,182,192,248,203,244,222,202,242,197,172,183,180,235,181,226,240])).
% 60.70/60.71 cnf(1989,plain,
% 60.70/60.71 (P4(a16,a16,f3(a16,a16,a16))),
% 60.70/60.71 inference(scs_inference,[],[142,1779,1783,1765,1619,1690,1713,1761,1850,1972,1983,1704,1785,1789,1887,1708,1755,1759,1773,1807,1827,1751,1813,1831,1863,1865,1825,1885,1875,1867,1781,1838,1797,1723,1737,152,167,283,255,225,257,155,258,169,166,168,170,256,223,165,150,151,224,164,162,163,252,254,253,251,182,192,248,203,244,222,202,242,197,172,183,180,235,181,226,240,179,161])).
% 60.70/60.71 cnf(1990,plain,
% 60.70/60.71 (P4(a16,x19901,x19901)),
% 60.70/60.71 inference(rename_variables,[],[1850])).
% 60.70/60.71 cnf(1994,plain,
% 60.70/60.71 (P1(a16,x19941,f13(a16,a16,a15,a15,a16,x19941))),
% 60.70/60.71 inference(scs_inference,[],[142,1779,1783,1765,1969,1619,1690,1713,1761,1850,1972,1983,1704,1785,1789,1887,1708,1755,1759,1773,1775,1807,1827,1751,1813,1831,1863,1865,1825,1885,1875,1867,1781,1838,1797,1723,1737,152,167,283,255,225,257,155,258,169,166,168,170,256,223,165,150,151,224,164,162,163,252,254,253,251,182,192,248,203,244,222,202,242,197,172,183,180,235,181,226,240,179,161,195,205])).
% 60.70/60.71 cnf(1996,plain,
% 60.70/60.71 (P1(x19961,x19962,x19962)),
% 60.70/60.71 inference(rename_variables,[],[1765])).
% 60.70/60.71 cnf(1998,plain,
% 60.70/60.71 (P4(f21(x19981,x19982),x19981,x19982)),
% 60.70/60.71 inference(scs_inference,[],[142,1779,1783,1765,1969,1996,1619,1690,1713,1761,1850,1972,1983,1990,1704,1785,1789,1887,1708,1755,1759,1773,1775,1807,1827,1751,1813,1831,1863,1865,1825,1885,1875,1867,1781,1838,1797,1723,1737,152,167,283,255,225,257,155,258,169,166,168,170,256,223,165,150,151,224,164,162,163,252,254,253,251,182,192,248,203,244,222,202,242,197,172,183,180,235,181,226,240,179,161,195,205,158])).
% 60.70/60.71 cnf(2004,plain,
% 60.70/60.71 (~P4(f21(a19,a18),a1,a2)),
% 60.70/60.71 inference(scs_inference,[],[142,1779,1783,1765,1969,1996,1619,1690,1713,1761,1850,1972,1983,1990,1704,1785,1789,1887,1708,1755,1759,1773,1775,1807,1827,1751,1813,1831,1863,1865,1825,1885,1875,1867,1781,1838,1797,1723,1737,152,167,283,255,225,257,155,258,169,166,168,170,256,223,165,150,151,224,164,162,163,252,254,253,251,182,192,248,203,244,222,202,242,197,172,183,180,235,181,226,240,179,161,195,205,158,1621])).
% 60.70/60.71 cnf(2006,plain,
% 60.70/60.71 (P4(a16,f3(a16,a16,a16),a16)),
% 60.70/60.71 inference(scs_inference,[],[142,1779,1783,1765,1969,1996,1619,1690,1713,1761,1850,1972,1983,1990,1704,1785,1789,1887,1708,1755,1759,1773,1775,1807,1827,1751,1813,1831,1863,1865,1825,1885,1875,1867,1781,1838,1797,1723,1737,152,167,283,255,225,257,155,258,169,166,168,170,256,223,165,150,151,224,164,162,163,252,254,253,251,182,192,248,203,244,222,202,242,197,172,183,180,235,181,226,240,179,161,195,205,158,1621,153])).
% 60.70/60.71 cnf(2010,plain,
% 60.70/60.71 (~E(f21(a19,a18),x20101)+~P4(x20101,a1,a2)),
% 60.70/60.71 inference(scs_inference,[],[142,1779,1783,1765,1969,1996,1619,1690,1713,1761,1850,1972,1983,1990,1704,1785,1789,1887,1708,1755,1759,1773,1775,1807,1827,1751,1813,1831,1863,1865,1825,1885,1875,1867,1781,1838,1797,1723,1737,152,167,283,255,225,257,155,258,169,166,168,170,256,223,165,150,151,224,164,162,163,252,254,253,251,182,192,248,203,244,222,202,242,197,172,183,180,235,181,226,240,179,161,195,205,158,1621,153,186,1623])).
% 60.70/60.71 cnf(2035,plain,
% 60.70/60.71 (P4(f21(x20351,x20352),x20351,x20352)),
% 60.70/60.71 inference(rename_variables,[],[1998])).
% 60.70/60.71 cnf(2037,plain,
% 60.70/60.71 (P4(f21(x20371,x20372),x20372,x20371)),
% 60.70/60.71 inference(scs_inference,[],[1998,2035,2010,153])).
% 60.70/60.71 cnf(2039,plain,
% 60.70/60.71 (P1(f21(x20391,x20392),x20391,x20392)),
% 60.70/60.71 inference(scs_inference,[],[1998,2035,2010,153,152])).
% 60.70/60.71 cnf(2043,plain,
% 60.70/60.71 (P5(a16,x20431,x20431,a16)),
% 60.70/60.71 inference(scs_inference,[],[1914,1916,1998,2035,2010,153,152,255,167])).
% 60.70/60.71 cnf(2045,plain,
% 60.70/60.71 (P8(a16,x20451,a16,x20451,x20451,x20451,x20451,x20451)),
% 60.70/60.71 inference(scs_inference,[],[1962,1914,1916,1998,2035,2010,153,152,255,167,258])).
% 60.70/60.71 cnf(2047,plain,
% 60.70/60.71 (P8(x20471,a16,x20471,x20471,a16,x20471,x20471,x20471)),
% 60.70/60.71 inference(scs_inference,[],[1962,1914,1916,1998,2035,2010,153,152,255,167,258,257])).
% 60.70/60.71 cnf(2050,plain,
% 60.70/60.71 (P4(f21(x20501,x20502),x20501,x20502)),
% 60.70/60.71 inference(rename_variables,[],[1998])).
% 60.70/60.71 cnf(2052,plain,
% 60.70/60.71 (P9(a16,x20521,x20521,x20521,x20521,x20521,a16,x20521)),
% 60.70/60.71 inference(scs_inference,[],[1962,1914,1916,1998,2035,2010,153,152,255,167,258,257,1621,225])).
% 60.70/60.71 cnf(2054,plain,
% 60.70/60.71 (P5(f21(x20541,x20542),x20541,f21(x20541,x20542),x20542)),
% 60.70/60.71 inference(scs_inference,[],[1962,1914,1916,1998,2035,2050,2010,153,152,255,167,258,257,1621,225,155])).
% 60.70/60.71 cnf(2066,plain,
% 60.70/60.71 (P9(a16,a2,a16,a15,a15,a2,a15,a15)),
% 60.70/60.71 inference(scs_inference,[],[1676,1763,1962,1978,1914,1916,1918,1998,2035,2050,1952,2010,153,152,255,167,258,257,1621,225,155,170,169,166,256,168,223])).
% 60.70/60.71 cnf(2070,plain,
% 60.70/60.71 (P1(x20701,x20701,x20702)),
% 60.70/60.71 inference(scs_inference,[],[1932,1676,1763,1962,1978,1914,1916,1918,1998,2035,2050,1861,1952,2010,153,152,255,167,258,257,1621,225,155,170,169,166,256,168,223,150,151])).
% 60.70/60.71 cnf(2074,plain,
% 60.70/60.71 (P9(a16,a15,x20741,x20742,a2,a17,x20741,x20742)),
% 60.70/60.71 inference(scs_inference,[],[1932,1942,1676,1763,1962,1978,1914,1916,1918,1998,2035,2050,1871,1861,1952,2010,153,152,255,167,258,257,1621,225,155,170,169,166,256,168,223,150,151,165,224])).
% 60.70/60.71 cnf(2082,plain,
% 60.70/60.71 (P9(x20821,x20822,x20823,x20824,x20821,x20822,x20824,x20823)),
% 60.70/60.72 inference(scs_inference,[],[1936,1932,1942,1676,1763,1962,1978,1914,1916,1918,1998,2035,2050,1871,1905,1968,1861,1952,2010,153,152,255,167,258,257,1621,225,155,170,169,166,256,168,223,150,151,165,224,162,164,163,252])).
% 60.70/60.72 cnf(2084,plain,
% 60.70/60.72 (P9(x20841,x20842,x20842,x20841,x20843,x20844,x20843,x20844)),
% 60.70/60.72 inference(scs_inference,[],[1936,1946,1932,1942,1676,1763,1962,1978,1914,1916,1918,1998,2035,2050,1871,1905,1968,1861,1952,2010,153,152,255,167,258,257,1621,225,155,170,169,166,256,168,223,150,151,165,224,162,164,163,252,253])).
% 60.70/60.72 cnf(2093,plain,
% 60.70/60.72 (P9(x20931,x20932,x20933,x20934,x20932,x20931,x20933,x20934)),
% 60.70/60.72 inference(rename_variables,[],[1936])).
% 60.70/60.72 cnf(2096,plain,
% 60.70/60.72 (P1(x20961,x20962,x20961)),
% 60.70/60.72 inference(rename_variables,[],[1932])).
% 60.70/60.72 cnf(2098,plain,
% 60.70/60.72 (P1(f23(x20981,x20981,a16,x20981),a16,x20981)),
% 60.70/60.72 inference(scs_inference,[],[1936,2093,1946,1932,1942,1676,1763,1962,1978,1914,1944,1916,1918,1998,2035,2050,1871,1905,1968,1861,1952,1985,1737,2010,153,152,255,167,258,257,1621,225,155,170,169,166,256,168,223,150,151,165,224,162,164,163,252,253,254,251,199,261,196,248])).
% 60.70/60.72 cnf(2099,plain,
% 60.70/60.72 (P5(a16,x20991,a16,x20991)),
% 60.70/60.72 inference(rename_variables,[],[1914])).
% 60.70/60.72 cnf(2100,plain,
% 60.70/60.72 (P9(x21001,x21002,x21003,x21004,x21002,x21001,x21003,x21004)),
% 60.70/60.72 inference(rename_variables,[],[1936])).
% 60.70/60.72 cnf(2102,plain,
% 60.70/60.72 (P8(f21(x21021,x21022),x21021,x21021,x21022,f21(x21021,x21022),x21021,x21021,x21022)),
% 60.70/60.72 inference(scs_inference,[],[1936,2093,1946,1932,1942,1676,1763,1962,1978,1914,1944,1916,1918,1998,2035,2050,1871,1905,1968,1861,1952,1985,1737,2010,153,152,255,167,258,257,1621,225,155,170,169,166,256,168,223,150,151,165,224,162,164,163,252,253,254,251,199,261,196,248,222])).
% 60.70/60.72 cnf(2105,plain,
% 60.70/60.72 (P4(f21(x21051,x21052),x21051,x21052)),
% 60.70/60.72 inference(rename_variables,[],[1998])).
% 60.70/60.72 cnf(2107,plain,
% 60.70/60.72 (P10(a16,a16,x21071,x21071)),
% 60.70/60.72 inference(scs_inference,[],[1936,2093,1946,1932,1942,1676,1763,1962,1978,1914,2099,1944,1916,1918,1998,2035,2050,1871,1905,1968,1861,1952,1985,329,1737,2010,153,152,255,167,258,257,1621,225,155,170,169,166,256,168,223,150,151,165,224,162,164,163,252,253,254,251,199,261,196,248,222,156,180])).
% 60.70/60.72 cnf(2109,plain,
% 60.70/60.72 (P2(a16,x21091,x21091,x21091)),
% 60.70/60.72 inference(scs_inference,[],[1936,2093,1946,1932,1942,1676,1763,1962,1978,1914,2099,1944,1916,1918,1998,2035,2050,1871,1905,1968,1861,1952,1985,329,1737,2010,153,152,255,167,258,257,1621,225,155,170,169,166,256,168,223,150,151,165,224,162,164,163,252,253,254,251,199,261,196,248,222,156,180,183])).
% 60.70/60.72 cnf(2111,plain,
% 60.70/60.72 (P6(x21111,x21111,x21111,x21111)),
% 60.70/60.72 inference(scs_inference,[],[1936,2093,2100,1946,1932,2096,1942,1676,1763,1962,1978,1914,2099,1944,1916,1918,1998,2035,2050,1871,1905,1968,1861,1952,1985,329,1737,2010,153,152,255,167,258,257,1621,225,155,170,169,166,256,168,223,150,151,165,224,162,164,163,252,253,254,251,199,261,196,248,222,156,180,183,235])).
% 60.70/60.72 cnf(2112,plain,
% 60.70/60.72 (P9(x21121,x21122,x21123,x21124,x21122,x21121,x21123,x21124)),
% 60.70/60.72 inference(rename_variables,[],[1936])).
% 60.70/60.72 cnf(2113,plain,
% 60.70/60.72 (P1(x21131,x21132,x21131)),
% 60.70/60.72 inference(rename_variables,[],[1932])).
% 60.70/60.72 cnf(2115,plain,
% 60.70/60.72 (~P10(a1,a19,f7(a2,a17,a20,a18),a2)),
% 60.70/60.72 inference(scs_inference,[],[1936,2093,2100,1946,1932,2096,1942,1676,1763,1962,1978,1914,2099,1944,1916,1918,1998,2035,2050,1871,1905,1968,1861,1952,1985,1656,329,1783,1737,2010,153,152,255,167,258,257,1621,225,155,170,169,166,256,168,223,150,151,165,224,162,164,163,252,253,254,251,199,261,196,248,222,156,180,183,235,181])).
% 60.70/60.72 cnf(2118,plain,
% 60.70/60.72 (P10(x21181,x21182,x21181,x21182)),
% 60.70/60.72 inference(scs_inference,[],[1936,2093,2100,1946,1932,2096,1942,1676,1763,1962,1978,1914,2099,1944,1916,1918,1998,2035,2050,1871,1905,1968,1861,1952,1985,1656,329,1783,1737,2010,153,152,255,167,258,257,1621,225,155,170,169,166,256,168,223,150,151,165,224,162,164,163,252,253,254,251,199,261,196,248,222,156,180,183,235,181,240])).
% 60.70/60.72 cnf(2119,plain,
% 60.70/60.72 (P9(x21191,x21192,x21191,x21192,x21193,x21194,x21193,x21194)),
% 60.70/60.72 inference(rename_variables,[],[1946])).
% 60.70/60.72 cnf(2122,plain,
% 60.70/60.72 (P4(f21(x21221,x21222),x21221,x21222)),
% 60.70/60.72 inference(rename_variables,[],[1998])).
% 60.70/60.72 cnf(2125,plain,
% 60.70/60.72 (P9(x21251,x21252,x21253,x21254,x21252,x21251,x21253,x21254)),
% 60.70/60.72 inference(rename_variables,[],[1936])).
% 60.70/60.72 cnf(2127,plain,
% 60.70/60.72 (~P10(a18,a2,a19,a1)),
% 60.70/60.72 inference(scs_inference,[],[1936,2093,2100,2112,1946,1932,2096,1942,1676,1763,1962,1978,1914,2099,1944,1916,1918,1974,1998,2035,2050,2105,1871,1905,1968,1861,1952,1985,1656,329,1783,1737,2010,153,152,255,167,258,257,1621,225,155,170,169,166,256,168,223,150,151,165,224,162,164,163,252,253,254,251,199,261,196,248,222,156,180,183,235,181,240,226,241,179])).
% 60.70/60.72 cnf(2132,plain,
% 60.70/60.72 (P4(f3(a16,a16,a16),f3(a16,a16,a16),f3(a16,a16,a16))),
% 60.70/60.72 inference(scs_inference,[],[1936,2093,2100,2112,1946,1932,2096,2113,1942,1676,1763,1962,1978,1914,2099,1944,1916,1918,1974,1998,2035,2050,2105,1871,1905,1968,1861,1952,1985,1645,1779,1656,1825,329,1783,1737,2010,153,152,255,167,258,257,1621,225,155,170,169,166,256,168,223,150,151,165,224,162,164,163,252,253,254,251,199,261,196,248,222,156,180,183,235,181,240,226,241,179,239,238])).
% 60.70/60.72 cnf(2134,plain,
% 60.70/60.72 (P1(x21341,x21342,x21341)),
% 60.70/60.72 inference(rename_variables,[],[1932])).
% 60.70/60.72 cnf(2136,plain,
% 60.70/60.72 (P4(f6(a18,a2,a2),a18,a2)),
% 60.70/60.72 inference(scs_inference,[],[1936,2093,2100,2112,1946,1932,2096,2113,1942,1676,1763,1962,1978,1914,2099,1944,1916,1918,1974,1998,2035,2050,2105,2122,1871,1905,1968,1861,1952,1930,1985,1645,1779,1656,1825,329,1783,1737,2010,153,152,255,167,258,257,1621,225,155,170,169,166,256,168,223,150,151,165,224,162,164,163,252,253,254,251,199,261,196,248,222,156,180,183,235,181,240,226,241,179,239,238,185])).
% 60.70/60.72 cnf(2137,plain,
% 60.70/60.72 (P4(f21(x21371,x21372),x21371,x21372)),
% 60.70/60.72 inference(rename_variables,[],[1998])).
% 60.70/60.72 cnf(2139,plain,
% 60.70/60.72 (P5(a15,a15,a2,a2)),
% 60.70/60.72 inference(scs_inference,[],[1936,2093,2100,2112,1946,2119,1932,2096,2113,1942,1676,1763,1962,1978,1914,2099,1944,1916,1918,1974,1998,2035,2050,2105,2122,1871,1905,1968,1861,1952,1930,1985,1645,1779,1656,1825,329,1783,1737,2010,153,152,255,167,258,257,1621,225,155,170,169,166,256,168,223,150,151,165,224,162,164,163,252,253,254,251,199,261,196,248,222,156,180,183,235,181,240,226,241,179,239,238,185,250])).
% 60.70/60.72 cnf(2140,plain,
% 60.70/60.72 (P9(x21401,x21402,x21401,x21402,x21403,x21404,x21403,x21404)),
% 60.70/60.72 inference(rename_variables,[],[1946])).
% 60.70/60.72 cnf(2144,plain,
% 60.70/60.72 (P1(x21441,x21442,x21441)),
% 60.70/60.72 inference(rename_variables,[],[1932])).
% 60.70/60.72 cnf(2147,plain,
% 60.70/60.72 (P3(a16,f25(a15,a15,a16,a16,a16,a16),a17,a2)),
% 60.70/60.72 inference(scs_inference,[],[1936,2093,2100,2112,1946,2119,1932,2096,2113,2134,1942,1676,1763,1962,1978,1914,2099,1940,1944,1916,1918,1974,1998,2035,2050,2105,2122,1871,1905,1968,1861,1952,1930,1985,1645,1779,1656,1825,329,1783,143,1737,2010,153,152,255,167,258,257,1621,225,155,170,169,166,256,168,223,150,151,165,224,162,164,163,252,253,254,251,199,261,196,248,222,156,180,183,235,181,240,226,241,179,239,238,185,250,205,2,283])).
% 60.70/60.72 cnf(2152,plain,
% 60.70/60.72 (~P9(a18,a2,a19,a1,a19,a1,a18,a2)),
% 60.70/60.72 inference(scs_inference,[],[1936,2093,2100,2112,1946,2119,1932,2096,2113,2134,1942,1676,1763,1962,1978,1914,2099,1940,1944,1916,1918,1974,1998,2035,2050,2105,2122,1871,1905,1968,1861,1952,1930,1985,1645,1779,1656,1825,329,1783,143,1737,2010,153,152,255,167,258,257,1621,225,155,170,169,166,256,168,223,150,151,165,224,162,164,163,252,253,254,251,199,261,196,248,222,156,180,183,235,181,240,226,241,179,239,238,185,250,205,2,283,186,3,237])).
% 60.70/60.72 cnf(2170,plain,
% 60.70/60.72 (P3(f21(x21701,x21702),f21(x21701,x21702),x21702,x21702)),
% 60.70/60.72 inference(scs_inference,[],[1936,2093,2100,2112,2125,1946,2119,2140,1932,2096,2113,2134,1942,1676,1763,1962,1978,1914,2099,1940,1944,1916,1918,1974,1998,2035,2050,2105,2122,2137,1871,1905,1968,1861,1952,1930,1985,1645,1779,1656,1825,329,1783,143,1807,1737,2010,153,152,255,167,258,257,1621,225,155,170,169,166,256,168,223,150,151,165,224,162,164,163,252,253,254,251,199,261,196,248,222,156,180,183,235,181,240,226,241,179,239,238,185,250,205,2,283,186,3,237,193,246,249,177,176,188,190,157])).
% 60.70/60.72 cnf(2177,plain,
% 60.70/60.72 (P10(a16,a16,a16,a15)),
% 60.70/60.72 inference(scs_inference,[],[1936,2093,2100,2112,2125,1946,2119,2140,1932,2096,2113,2134,2144,1942,1676,1763,1962,1978,1914,2099,1940,1944,1916,1918,1924,1974,1998,2035,2050,2105,2122,2137,1871,1905,1968,1861,1952,1930,1985,1645,1779,1656,1825,329,1783,143,1807,1737,2010,153,152,255,167,258,257,1621,225,155,170,169,166,256,168,223,150,151,165,224,162,164,163,252,253,254,251,199,261,196,248,222,156,180,183,235,181,240,226,241,179,239,238,185,250,205,2,283,186,3,237,193,246,249,177,176,188,190,157,197,189,194])).
% 60.70/60.72 cnf(2186,plain,
% 60.70/60.72 (P10(x21861,x21862,x21861,x21862)),
% 60.70/60.72 inference(rename_variables,[],[2118])).
% 60.70/60.72 cnf(2188,plain,
% 60.70/60.72 (P3(a19,a17,a2,a16)),
% 60.70/60.72 inference(scs_inference,[],[2118,2186,360,426])).
% 60.70/60.72 cnf(2189,plain,
% 60.70/60.72 (P10(x21891,x21892,x21891,x21892)),
% 60.70/60.72 inference(rename_variables,[],[2118])).
% 60.70/60.72 cnf(2191,plain,
% 60.70/60.72 (P4(f6(a18,a2,a2),a2,a18)),
% 60.70/60.72 inference(scs_inference,[],[2118,2186,2136,360,426,153])).
% 60.70/60.72 cnf(2195,plain,
% 60.70/60.72 (P10(a15,a16,a2,a17)),
% 60.70/60.72 inference(scs_inference,[],[2118,2186,2189,2045,2136,360,426,153,255,364])).
% 60.70/60.72 cnf(2196,plain,
% 60.70/60.72 (P10(x21961,x21962,x21961,x21962)),
% 60.70/60.72 inference(rename_variables,[],[2118])).
% 60.70/60.72 cnf(2198,plain,
% 60.70/60.72 (P3(a1,a17,a2,a15)),
% 60.70/60.72 inference(scs_inference,[],[2118,2186,2189,2196,2045,2136,360,426,153,255,364,485])).
% 60.70/60.72 cnf(2199,plain,
% 60.70/60.72 (P10(x21991,x21992,x21991,x21992)),
% 60.70/60.72 inference(rename_variables,[],[2118])).
% 60.70/60.72 cnf(2201,plain,
% 60.70/60.72 (P8(x22011,a16,a16,x22011,x22011,x22011,x22011,x22011)),
% 60.70/60.72 inference(scs_inference,[],[2118,2186,2189,2196,2045,2136,360,426,153,255,364,485,257])).
% 60.70/60.72 cnf(2204,plain,
% 60.70/60.72 (P4(f21(x22041,x22042),x22042,x22041)),
% 60.70/60.72 inference(rename_variables,[],[2037])).
% 60.70/60.72 cnf(2212,plain,
% 60.70/60.72 (P5(f21(x22121,x22122),x22122,f21(x22121,x22122),x22121)),
% 60.70/60.72 inference(scs_inference,[],[2118,2186,2189,2196,2045,2054,2037,2204,2136,360,426,153,255,364,485,257,1621,225,152,167,155])).
% 60.70/60.72 cnf(2216,plain,
% 60.70/60.72 (P6(a15,a15,a2,a16)),
% 60.70/60.72 inference(scs_inference,[],[2118,2186,2189,2196,2045,1769,1912,2054,2037,2204,2136,360,426,153,255,364,485,257,1621,225,152,167,155,258,169])).
% 60.70/60.72 cnf(2222,plain,
% 60.70/60.72 (P5(x22221,a16,a16,x22221)),
% 60.70/60.72 inference(scs_inference,[],[2118,2186,2189,2196,2045,2047,2043,1769,1912,2054,2037,2204,1843,2136,360,426,153,255,364,485,257,1621,225,152,167,155,258,169,256,168,166])).
% 60.70/60.72 cnf(2224,plain,
% 60.70/60.72 (P1(x22241,f21(x22241,x22242),x22242)),
% 60.70/60.72 inference(scs_inference,[],[2118,2186,2189,2196,2045,2047,2043,1769,1912,2054,2037,2204,2039,1843,2136,360,426,153,255,364,485,257,1621,225,152,167,155,258,169,256,168,166,150])).
% 60.70/60.72 cnf(2230,plain,
% 60.70/60.72 (P10(x22301,x22302,x22302,x22301)),
% 60.70/60.72 inference(scs_inference,[],[2118,2186,2189,2196,2199,2045,2047,2043,1769,1912,2054,2037,2204,2039,1843,2098,2136,360,426,153,255,364,485,257,1621,225,152,167,155,258,169,256,168,166,150,151,223,165])).
% 60.70/60.72 cnf(2236,plain,
% 60.70/60.72 (P10(x22361,x22361,a16,a16)),
% 60.70/60.72 inference(scs_inference,[],[2118,2186,2189,2196,2199,2045,2047,2043,2107,1769,1912,2054,2170,2037,2204,2039,1843,2098,2136,360,426,153,255,364,485,257,1621,225,152,167,155,258,169,256,168,166,150,151,223,165,224,162,164])).
% 60.70/60.72 cnf(2238,plain,
% 60.70/60.72 (P3(a16,a16,a16,f25(a16,a16,a16,a16,a16,a16))),
% 60.70/60.72 inference(scs_inference,[],[2118,2186,2189,2196,2199,2045,2047,2043,2107,1769,1912,2054,2170,2037,2204,2039,1843,2098,1877,2136,360,426,153,255,364,485,257,1621,225,152,167,155,258,169,256,168,166,150,151,223,165,224,162,164,163])).
% 60.70/60.72 cnf(2242,plain,
% 60.70/60.72 (P9(x22421,x22422,x22423,x22424,x22422,x22421,x22424,x22423)),
% 60.70/60.72 inference(scs_inference,[],[2082,2118,2186,2189,2196,2199,2045,2047,2052,2043,2107,1769,1912,2054,2170,2037,2204,2039,1843,2098,1877,2136,360,426,153,255,364,485,257,1621,225,152,167,155,258,169,256,168,166,150,151,223,165,224,162,164,163,252,253])).
% 60.70/60.72 cnf(2244,plain,
% 60.70/60.72 (P9(x22441,x22442,x22441,x22442,x22443,x22444,x22444,x22443)),
% 60.70/60.72 inference(scs_inference,[],[2082,2118,2186,2189,2196,2199,2045,2047,2052,2043,2107,1769,1912,2054,2170,2037,2204,2039,1843,2098,1877,2136,360,426,153,255,364,485,257,1621,225,152,167,155,258,169,256,168,166,150,151,223,165,224,162,164,163,252,253,254])).
% 60.70/60.72 cnf(2246,plain,
% 60.70/60.72 (P9(a2,a17,x22461,x22462,a16,a15,x22461,x22462)),
% 60.70/60.72 inference(scs_inference,[],[2082,2118,2186,2189,2196,2199,2045,2047,2052,2043,2074,2107,1769,1912,2054,2170,2037,2204,2039,1843,2098,1877,2136,360,426,153,255,364,485,257,1621,225,152,167,155,258,169,256,168,166,150,151,223,165,224,162,164,163,252,253,254,251])).
% 60.70/60.72 cnf(2253,plain,
% 60.70/60.72 (P10(x22531,x22532,x22531,x22532)),
% 60.70/60.72 inference(rename_variables,[],[2118])).
% 60.70/60.72 cnf(2256,plain,
% 60.70/60.72 (P10(x22561,x22562,x22561,x22562)),
% 60.70/60.72 inference(rename_variables,[],[2118])).
% 60.70/60.72 cnf(2259,plain,
% 60.70/60.72 (P9(x22591,x22592,x22593,x22594,x22591,x22592,x22594,x22593)),
% 60.70/60.72 inference(rename_variables,[],[2082])).
% 60.70/60.72 cnf(2262,plain,
% 60.70/60.72 (P10(x22621,x22622,x22621,x22622)),
% 60.70/60.72 inference(rename_variables,[],[2118])).
% 60.70/60.72 cnf(2266,plain,
% 60.70/60.72 (P1(x22661,x22661,x22662)),
% 60.70/60.72 inference(rename_variables,[],[2070])).
% 60.70/60.72 cnf(2268,plain,
% 60.70/60.72 (P1(f5(x22681,x22681,x22682),x22682,x22681)),
% 60.70/60.72 inference(scs_inference,[],[142,2082,2118,2186,2189,2196,2199,2253,2256,2262,2070,2045,2047,2052,2043,2074,2107,1769,1771,1910,1912,2177,2054,2170,2037,2204,2039,1843,2098,1994,1877,2136,1914,1807,360,426,153,255,364,485,257,1621,225,152,167,155,258,169,256,168,166,150,151,223,165,224,162,164,163,252,253,254,251,247,246,198,196,261,200,154,177])).
% 60.70/60.72 cnf(2271,plain,
% 60.70/60.72 (P4(f21(x22711,x22712),x22712,x22711)),
% 60.70/60.72 inference(rename_variables,[],[2037])).
% 60.70/60.72 cnf(2272,plain,
% 60.70/60.72 (P1(f4(x22721,x22721,x22722),x22722,x22721)),
% 60.70/60.72 inference(scs_inference,[],[142,2082,2118,2186,2189,2196,2199,2253,2256,2262,2070,2045,2047,2052,2043,2074,2107,1769,1771,1910,1912,2177,2054,2170,2037,2204,2039,2004,1843,2098,1994,1877,2136,1914,1807,360,426,153,255,364,485,257,1621,225,152,167,155,258,169,256,168,166,150,151,223,165,224,162,164,163,252,253,254,251,247,246,198,196,261,200,154,177,133,176])).
% 60.70/60.72 cnf(2274,plain,
% 60.70/60.72 (P8(f21(x22741,x22742),x22742,x22742,x22741,f21(x22741,x22742),x22742,x22742,x22741)),
% 60.70/60.72 inference(scs_inference,[],[142,2082,2118,2186,2189,2196,2199,2253,2256,2262,2070,2045,2047,2052,2043,2074,2107,1769,1771,1910,1912,2177,2054,2170,2037,2204,2271,2039,2004,1843,2098,1994,1877,2136,1914,1807,360,426,153,255,364,485,257,1621,225,152,167,155,258,169,256,168,166,150,151,223,165,224,162,164,163,252,253,254,251,247,246,198,196,261,200,154,177,133,176,222])).
% 60.70/60.72 cnf(2277,plain,
% 60.70/60.72 (P4(f21(x22771,x22772),x22772,x22771)),
% 60.70/60.72 inference(rename_variables,[],[2037])).
% 60.70/60.72 cnf(2280,plain,
% 60.70/60.72 (P10(x22801,x22802,x22801,x22802)),
% 60.70/60.72 inference(rename_variables,[],[2118])).
% 60.70/60.72 cnf(2282,plain,
% 60.70/60.72 (P2(f8(x22821,x22821,x22821),x22821,x22821,x22821)),
% 60.70/60.72 inference(scs_inference,[],[142,2111,2082,2118,2186,2189,2196,2199,2253,2256,2262,2280,2070,2045,2047,2052,2043,2074,2107,1769,1771,1910,1912,2177,2054,2170,2037,2204,2271,2039,2004,1843,2098,1994,1877,2136,263,1914,1807,360,426,153,255,364,485,257,1621,225,152,167,155,258,169,256,168,166,150,151,223,165,224,162,164,163,252,253,254,251,247,246,198,196,261,200,154,177,133,176,222,156,197,190])).
% 60.70/60.72 cnf(2283,plain,
% 60.70/60.72 (P6(x22831,x22831,x22831,x22831)),
% 60.70/60.72 inference(rename_variables,[],[2111])).
% 60.70/60.72 cnf(2284,plain,
% 60.70/60.72 (P10(x22841,x22842,x22841,x22842)),
% 60.70/60.72 inference(rename_variables,[],[2118])).
% 60.70/60.72 cnf(2289,plain,
% 60.70/60.72 (P10(x22891,x22892,x22891,x22892)),
% 60.70/60.72 inference(rename_variables,[],[2118])).
% 60.70/60.72 cnf(2291,plain,
% 60.70/60.72 (P10(x22911,f4(x22911,x22911,x22912),x22912,x22911)),
% 60.70/60.72 inference(scs_inference,[],[142,2111,2082,2118,2186,2189,2196,2199,2253,2256,2262,2280,2284,2289,2070,2045,2047,2052,2043,2074,2107,1769,1771,1910,1912,2177,2054,2170,2037,2204,2271,2039,2132,2004,1843,2098,1994,1877,2136,263,1914,1807,360,426,153,255,364,485,257,1621,225,152,167,155,258,169,256,168,166,150,151,223,165,224,162,164,163,252,253,254,251,247,246,198,196,261,200,154,177,133,176,222,156,197,190,183,172,188])).
% 60.70/60.72 cnf(2293,plain,
% 60.70/60.72 (P10(x22931,x22932,x22932,x22932)),
% 60.70/60.72 inference(scs_inference,[],[142,2111,2082,2118,2186,2189,2196,2199,2253,2256,2262,2280,2284,2289,2070,2045,2047,2052,2043,2074,2107,1769,1771,1910,1912,2177,2054,2170,2037,2204,2271,2039,2132,2004,1843,2098,1994,1877,2136,263,1914,1807,360,426,153,255,364,485,257,1621,225,152,167,155,258,169,256,168,166,150,151,223,165,224,162,164,163,252,253,254,251,247,246,198,196,261,200,154,177,133,176,222,156,197,190,183,172,188,171])).
% 60.70/60.72 cnf(2300,plain,
% 60.70/60.72 (P3(f21(x23001,x23002),f21(x23001,x23002),x23002,x23002)),
% 60.70/60.72 inference(rename_variables,[],[2170])).
% 60.70/60.72 cnf(2302,plain,
% 60.70/60.72 (P10(x23021,f5(x23021,x23021,x23022),x23022,x23021)),
% 60.70/60.72 inference(scs_inference,[],[142,2111,2082,2118,2186,2189,2196,2199,2253,2256,2262,2280,2284,2289,2070,2045,2047,2052,2043,2074,2107,1769,1771,1910,1912,2177,2054,2170,2037,2204,2271,2039,2132,2004,1843,2098,1994,1877,2136,263,1914,1807,360,426,153,255,364,485,257,1621,225,152,167,155,258,169,256,168,166,150,151,223,165,224,162,164,163,252,253,254,251,247,246,198,196,261,200,154,177,133,176,222,156,197,190,183,172,188,171,180,178,189])).
% 60.70/60.72 cnf(2305,plain,
% 60.70/60.72 (P3(f21(x23051,x23052),f21(x23051,x23052),x23052,x23052)),
% 60.70/60.72 inference(rename_variables,[],[2170])).
% 60.70/60.72 cnf(2307,plain,
% 60.70/60.72 (P6(x23071,x23072,x23072,x23072)),
% 60.70/60.72 inference(scs_inference,[],[142,2111,2082,2259,2118,2186,2189,2196,2199,2253,2256,2262,2280,2284,2289,2070,2266,2045,2047,2052,2043,2074,2107,1769,1771,1910,1912,2177,2054,2170,2300,2037,2204,2271,2039,2132,2004,1843,2098,1994,1877,2136,263,1914,1807,360,426,153,255,364,485,257,1621,225,152,167,155,258,169,256,168,166,150,151,223,165,224,162,164,163,252,253,254,251,247,246,198,196,261,200,154,177,133,176,222,156,197,190,183,172,188,171,180,178,189,181,235])).
% 60.70/60.72 cnf(2308,plain,
% 60.70/60.72 (P1(x23081,x23081,x23082)),
% 60.70/60.72 inference(rename_variables,[],[2070])).
% 60.70/60.72 cnf(2309,plain,
% 60.70/60.72 (P9(x23091,x23092,x23093,x23094,x23091,x23092,x23094,x23093)),
% 60.70/60.72 inference(rename_variables,[],[2082])).
% 60.70/60.72 cnf(2311,plain,
% 60.70/60.72 (P10(a16,a16,a15,a16)),
% 60.70/60.72 inference(scs_inference,[],[142,2111,2082,2259,2309,2118,2186,2189,2196,2199,2253,2256,2262,2280,2284,2289,2070,2266,2045,2047,2052,2043,2074,2107,1769,1771,1910,1912,2177,2054,2170,2300,2037,2204,2271,2039,2132,2004,1843,2098,1994,1877,2136,263,1914,1807,360,426,153,255,364,485,257,1621,225,152,167,155,258,169,256,168,166,150,151,223,165,224,162,164,163,252,253,254,251,247,246,198,196,261,200,154,177,133,176,222,156,197,190,183,172,188,171,180,178,189,181,235,240])).
% 60.70/60.72 cnf(2312,plain,
% 60.70/60.72 (P9(x23121,x23122,x23123,x23124,x23121,x23122,x23124,x23123)),
% 60.70/60.72 inference(rename_variables,[],[2082])).
% 60.70/60.72 cnf(2316,plain,
% 60.70/60.72 (P4(f21(x23161,x23162),x23162,x23161)),
% 60.70/60.72 inference(rename_variables,[],[2037])).
% 60.70/60.72 cnf(2319,plain,
% 60.70/60.72 (P10(x23191,x23192,x23191,x23192)),
% 60.70/60.72 inference(rename_variables,[],[2118])).
% 60.70/60.72 cnf(2322,plain,
% 60.70/60.72 (P9(x23221,x23222,x23223,x23224,x23221,x23222,x23224,x23223)),
% 60.70/60.72 inference(rename_variables,[],[2082])).
% 60.70/60.72 cnf(2324,plain,
% 60.70/60.72 (P4(f6(x23241,x23241,x23241),x23241,x23241)),
% 60.70/60.72 inference(scs_inference,[],[142,2111,2082,2259,2309,2312,2118,2186,2189,2196,2199,2253,2256,2262,2280,2284,2289,2319,2070,2266,2045,2047,2052,2109,2043,2074,2107,1769,1771,1910,1912,2177,2054,2170,2300,2037,2204,2271,2277,2316,2039,2132,2004,1843,2098,1994,1877,2147,2136,263,1914,1807,360,426,153,255,364,485,257,1621,225,152,167,155,258,169,256,168,166,150,151,223,165,224,162,164,163,252,253,254,251,247,246,198,196,261,200,154,177,133,176,222,156,197,190,183,172,188,171,180,178,189,181,235,240,226,179,239,185])).
% 60.70/60.72 cnf(2325,plain,
% 60.70/60.72 (P4(f21(x23251,x23252),x23252,x23251)),
% 60.70/60.72 inference(rename_variables,[],[2037])).
% 60.70/60.72 cnf(2327,plain,
% 60.70/60.72 (P10(x23271,x23272,x23271,x23272)),
% 60.70/60.72 inference(rename_variables,[],[2118])).
% 60.70/60.72 cnf(2329,plain,
% 60.70/60.72 (P4(a16,a16,f6(a16,a16,a16))),
% 60.70/60.72 inference(scs_inference,[],[142,2111,2082,2259,2309,2312,2118,2186,2189,2196,2199,2253,2256,2262,2280,2284,2289,2319,2070,2266,2308,2045,2047,2052,2109,2043,2074,2107,1769,1771,1910,1912,2177,2054,2170,2300,2037,2204,2271,2277,2316,2039,2132,2004,1843,2098,1994,1877,2147,2136,1845,263,1783,1914,1807,360,426,153,255,364,485,257,1621,225,152,167,155,258,169,256,168,166,150,151,223,165,224,162,164,163,252,253,254,251,247,246,198,196,261,200,154,177,133,176,222,156,197,190,183,172,188,171,180,178,189,181,235,240,226,179,239,185,161])).
% 60.70/60.72 cnf(2330,plain,
% 60.70/60.72 (P1(x23301,x23301,x23302)),
% 60.70/60.72 inference(rename_variables,[],[2070])).
% 60.70/60.72 cnf(2331,plain,
% 60.70/60.72 (P3(x23311,x23312,x23312,x23311)),
% 60.70/60.72 inference(rename_variables,[],[1783])).
% 60.70/60.72 cnf(2334,plain,
% 60.70/60.72 (P1(x23341,x23341,x23342)),
% 60.70/60.72 inference(rename_variables,[],[2070])).
% 60.70/60.72 cnf(2335,plain,
% 60.70/60.72 (P4(a16,x23351,x23351)),
% 60.70/60.72 inference(rename_variables,[],[1850])).
% 60.70/60.72 cnf(2336,plain,
% 60.70/60.72 (P3(x23361,x23362,x23361,x23362)),
% 60.70/60.72 inference(rename_variables,[],[1741])).
% 60.70/60.72 cnf(2338,plain,
% 60.70/60.72 (P5(x23381,x23381,x23381,x23381)),
% 60.70/60.72 inference(scs_inference,[],[142,2111,2283,2082,2259,2309,2312,2322,2118,2186,2189,2196,2199,2253,2256,2262,2280,2284,2289,2319,2070,2266,2308,2330,2045,2047,2052,2109,2043,2074,2107,1769,1771,1910,1912,2177,2054,2170,2300,2037,2204,2271,2277,2316,2039,2132,2004,1843,2098,1994,1877,2147,2136,1845,1637,263,1783,1914,1741,1807,1850,360,426,153,255,364,485,257,1621,225,152,167,155,258,169,256,168,166,150,151,223,165,224,162,164,163,252,253,254,251,247,246,198,196,261,200,154,177,133,176,222,156,197,190,183,172,188,171,180,178,189,181,235,240,226,179,239,185,161,208,250])).
% 60.70/60.72 cnf(2344,plain,
% 60.70/60.72 (P1(x23441,x23441,x23442)),
% 60.70/60.72 inference(rename_variables,[],[2070])).
% 60.70/60.72 cnf(2350,plain,
% 60.70/60.72 (P1(x23501,x23501,x23502)),
% 60.70/60.72 inference(rename_variables,[],[2070])).
% 60.70/60.72 cnf(2356,plain,
% 60.70/60.72 (~P9(a2,a18,a1,a19,a1,a19,a2,a18)),
% 60.70/60.72 inference(scs_inference,[],[142,2111,2283,2082,2259,2309,2312,2322,2118,2186,2189,2196,2199,2253,2256,2262,2280,2284,2289,2319,2070,2266,2308,2330,2334,2344,2045,2047,2052,2109,2043,2074,2107,1769,1771,1910,1912,2177,2054,2170,2300,2305,2037,2204,2271,2277,2316,2039,2132,2004,1843,2098,1994,1877,2147,2136,1845,1637,1932,263,1783,2331,1914,1741,2336,1807,1850,2335,360,426,153,255,364,485,257,1621,225,152,167,155,258,169,256,168,166,150,151,223,165,224,162,164,163,252,253,254,251,247,246,198,196,261,200,154,177,133,176,222,156,197,190,183,172,188,171,180,178,189,181,235,240,226,179,239,185,161,208,250,207,205,2,229,237])).
% 60.70/60.72 cnf(2358,plain,
% 60.70/60.72 (~E(f21(a18,a19),f21(a1,a2))),
% 60.70/60.72 inference(scs_inference,[],[142,2111,2283,2082,2259,2309,2312,2322,2118,2186,2189,2196,2199,2253,2256,2262,2280,2284,2289,2319,2070,2266,2308,2330,2334,2344,2045,2047,2052,2109,2043,2074,2107,1769,1771,1910,1912,2177,2054,2170,2300,2305,2037,2204,2271,2277,2316,2325,2039,2132,2004,1843,2098,1994,1877,2147,2136,1845,1637,1998,1932,263,1783,2331,1914,1741,2336,1807,1850,2335,360,426,153,255,364,485,257,1621,225,152,167,155,258,169,256,168,166,150,151,223,165,224,162,164,163,252,253,254,251,247,246,198,196,261,200,154,177,133,176,222,156,197,190,183,172,188,171,180,178,189,181,235,240,226,179,239,185,161,208,250,207,205,2,229,237,1623])).
% 60.70/60.72 cnf(2362,plain,
% 60.70/60.72 (P5(x23621,x23621,x23621,f27(x23621,x23621,x23621,x23621,x23621))),
% 60.70/60.72 inference(scs_inference,[],[142,2111,2283,2082,2259,2309,2312,2322,2118,2186,2189,2196,2199,2253,2256,2262,2280,2284,2289,2319,2327,2070,2266,2308,2330,2334,2344,2045,2047,2052,2109,2043,2074,2107,1769,1771,1910,1912,2177,2054,2170,2300,2305,2037,2204,2271,2277,2316,2325,2039,2132,2004,1843,2098,1994,1877,2147,2136,1845,1637,1998,1932,263,1783,2331,1914,1741,2336,1807,1850,2335,360,426,153,255,364,485,257,1621,225,152,167,155,258,169,256,168,166,150,151,223,165,224,162,164,163,252,253,254,251,247,246,198,196,261,200,154,177,133,176,222,156,197,190,183,172,188,171,180,178,189,181,235,240,226,179,239,185,161,208,250,207,205,2,229,237,1623,199])).
% 60.70/60.72 cnf(2367,plain,
% 60.70/60.72 (P4(x23671,x23671,x23671)),
% 60.70/60.72 inference(scs_inference,[],[142,2111,2283,2082,2259,2309,2312,2322,2084,2118,2186,2189,2196,2199,2253,2256,2262,2280,2284,2289,2319,2327,2070,2266,2308,2330,2334,2344,2350,2045,2047,2052,2109,2043,2074,2107,1769,1771,1910,1912,2177,2054,2170,2300,2305,2037,2204,2271,2277,2316,2325,2039,2132,2004,1843,2098,1994,1877,2147,2136,1845,1637,1998,1932,263,1783,2331,1914,1741,2336,1807,1850,2335,360,426,153,255,364,485,257,1621,225,152,167,155,258,169,256,168,166,150,151,223,165,224,162,164,163,252,253,254,251,247,246,198,196,261,200,154,177,133,176,222,156,197,190,183,172,188,171,180,178,189,181,235,240,226,179,239,185,161,208,250,207,205,2,229,237,1623,199,187,238])).
% 60.70/60.72 cnf(2373,plain,
% 60.70/60.72 (P3(a17,a19,a2,a16)),
% 60.70/60.72 inference(scs_inference,[],[2230,426])).
% 60.70/60.72 cnf(2374,plain,
% 60.70/60.72 (P10(x23741,x23742,x23742,x23741)),
% 60.70/60.72 inference(rename_variables,[],[2230])).
% 60.70/60.72 cnf(2377,plain,
% 60.70/60.72 (P10(x23771,f4(x23771,x23771,x23772),x23772,x23771)),
% 60.70/60.72 inference(rename_variables,[],[2291])).
% 60.70/60.72 cnf(2381,plain,
% 60.70/60.72 (P10(a15,a16,a2,a2)),
% 60.70/60.72 inference(scs_inference,[],[2230,2293,2201,2291,426,366,255,360])).
% 60.70/60.72 cnf(2382,plain,
% 60.70/60.72 (P10(x23821,x23822,x23822,x23822)),
% 60.70/60.72 inference(rename_variables,[],[2293])).
% 60.70/60.72 cnf(2389,plain,
% 60.70/60.72 (P4(f21(x23891,x23892),x23892,x23891)),
% 60.70/60.72 inference(rename_variables,[],[2037])).
% 60.70/60.72 cnf(2397,plain,
% 60.70/60.72 (P3(a17,a1,a2,a15)),
% 60.70/60.72 inference(scs_inference,[],[2230,2374,2293,2201,2362,2102,2324,2291,2329,2191,2037,426,366,255,360,153,257,1621,225,152,155,485])).
% 60.70/60.72 cnf(2398,plain,
% 60.70/60.72 (P10(x23981,x23982,x23982,x23981)),
% 60.70/60.72 inference(rename_variables,[],[2230])).
% 60.70/60.72 cnf(2407,plain,
% 60.70/60.72 (P8(a16,x24071,x24071,a16,x24071,x24071,x24071,x24071)),
% 60.70/60.72 inference(scs_inference,[],[2230,2374,2293,2201,2222,1922,2362,2102,2324,2291,2358,2329,2191,2037,426,366,255,360,153,257,1621,225,152,155,485,167,2,169,258,256])).
% 60.70/60.72 cnf(2409,plain,
% 60.70/60.72 (P5(a2,a2,a15,a15)),
% 60.70/60.72 inference(scs_inference,[],[2230,2374,2293,2201,2222,1922,2139,2362,2102,2324,2291,2358,2329,2191,2037,426,366,255,360,153,257,1621,225,152,155,485,167,2,169,258,256,166])).
% 60.70/60.72 cnf(2411,plain,
% 60.70/60.72 (P6(x24111,x24112,x24111,x24111)),
% 60.70/60.72 inference(scs_inference,[],[2230,2374,2293,2307,2201,2222,1922,2139,2362,2102,2324,2291,2358,2329,2191,2037,426,366,255,360,153,257,1621,225,152,155,485,167,2,169,258,256,166,168])).
% 60.70/60.72 cnf(2423,plain,
% 60.70/60.72 (P3(a2,a16,a19,a17)),
% 60.70/60.72 inference(scs_inference,[],[2230,2374,2293,2307,2201,2222,1922,2139,2188,2362,2102,2324,2291,2377,2268,2358,2329,2191,2037,1680,426,366,255,360,153,257,1621,225,152,155,485,167,2,169,258,256,166,168,150,232,223,151,165,162])).
% 60.70/60.72 cnf(2425,plain,
% 60.70/60.72 (P9(a19,a17,x24251,x24252,a2,a16,x24251,x24252)),
% 60.70/60.72 inference(scs_inference,[],[2230,2374,2293,2307,2201,2222,1922,2139,2188,2362,2102,2324,2291,2377,2268,2358,2329,2191,2037,1680,426,366,255,360,153,257,1621,225,152,155,485,167,2,169,258,256,166,168,150,232,223,151,165,162,224])).
% 60.70/60.72 cnf(2427,plain,
% 60.70/60.72 (P3(a19,a17,a16,a2)),
% 60.70/60.72 inference(scs_inference,[],[2230,2374,2293,2307,2201,2222,1922,2139,2188,2362,2102,2324,2291,2377,2268,2358,2329,2191,2037,1680,426,366,255,360,153,257,1621,225,152,155,485,167,2,169,258,256,166,168,150,232,223,151,165,162,224,163])).
% 60.70/60.72 cnf(2429,plain,
% 60.70/60.72 (P10(x24291,x24291,x24292,x24291)),
% 60.70/60.72 inference(scs_inference,[],[2230,2374,2293,2382,2307,2201,2222,1922,2139,2188,2362,2102,2324,2291,2377,2268,2358,2329,2191,2037,1680,426,366,255,360,153,257,1621,225,152,155,485,167,2,169,258,256,166,168,150,232,223,151,165,162,224,163,164])).
% 60.70/60.72 cnf(2439,plain,
% 60.70/60.72 (P5(x24391,x24391,x24391,f27(x24391,x24392,x24391,x24391,x24391))),
% 60.70/60.72 inference(scs_inference,[],[2338,2230,2374,2398,2242,2293,2382,2307,1686,1710,2201,2222,1922,2139,2188,2362,2102,2324,2291,2377,2268,2358,2329,2191,2037,1680,426,366,255,360,153,257,1621,225,152,155,485,167,2,169,258,256,166,168,150,232,223,151,165,162,224,163,164,252,254,253,251,198])).
% 60.70/60.72 cnf(2440,plain,
% 60.70/60.72 (P10(x24401,x24402,x24402,x24401)),
% 60.70/60.72 inference(rename_variables,[],[2230])).
% 60.70/60.72 cnf(2443,plain,
% 60.70/60.72 (P10(x24431,x24432,x24432,x24431)),
% 60.70/60.72 inference(rename_variables,[],[2230])).
% 60.70/60.72 cnf(2445,plain,
% 60.70/60.72 (P3(f25(x24451,x24451,x24451,x24451,x24451,x24451),x24451,x24451,x24451)),
% 60.70/60.72 inference(scs_inference,[],[142,2338,2367,2230,2374,2398,2440,2242,2293,2382,2307,1686,1710,2201,2222,1922,2139,2188,2362,2102,2324,2291,2377,2268,2358,2329,2191,2037,1680,426,366,255,360,153,257,1621,225,152,155,485,167,2,169,258,256,166,168,150,232,223,151,165,162,224,163,164,252,254,253,251,198,196,204])).
% 60.70/60.72 cnf(2447,plain,
% 60.70/60.72 (P3(f27(x24471,x24472,x24471,x24471,x24471),x24471,x24471,x24472)),
% 60.70/60.72 inference(scs_inference,[],[142,2338,2367,2230,2374,2398,2440,2443,2242,2293,2382,2307,1686,1710,2201,2222,1922,2139,2188,2362,2102,2324,2291,2377,2268,2358,2329,2191,2037,1680,426,366,255,360,153,257,1621,225,152,155,485,167,2,169,258,256,166,168,150,232,223,151,165,162,224,163,164,252,254,253,251,198,196,204,200])).
% 60.70/60.72 cnf(2448,plain,
% 60.70/60.72 (P10(x24481,x24482,x24482,x24481)),
% 60.70/60.72 inference(rename_variables,[],[2230])).
% 60.70/60.72 cnf(2450,plain,
% 60.70/60.72 (P3(f25(x24501,x24501,x24502,x24502,x24501,a16),a16,x24501,x24502)),
% 60.70/60.72 inference(scs_inference,[],[142,2338,2367,2230,2374,2398,2440,2443,2242,2293,2382,2307,1686,1710,2201,2222,1922,2139,2188,2362,2102,2324,2291,2377,2268,2358,2329,2191,2037,1680,1850,426,366,255,360,153,257,1621,225,152,155,485,167,2,169,258,256,166,168,150,232,223,151,165,162,224,163,164,252,254,253,251,198,196,204,200,203])).
% 60.70/60.72 cnf(2453,plain,
% 60.70/60.72 (P10(x24531,x24532,x24532,x24531)),
% 60.70/60.72 inference(rename_variables,[],[2230])).
% 60.70/60.72 cnf(2456,plain,
% 60.70/60.72 (P9(x24561,x24562,x24563,x24564,x24562,x24561,x24564,x24563)),
% 60.70/60.72 inference(rename_variables,[],[2242])).
% 60.70/60.72 cnf(2459,plain,
% 60.70/60.72 (P10(x24591,x24591,a16,a16)),
% 60.70/60.72 inference(rename_variables,[],[2236])).
% 60.70/60.72 cnf(2460,plain,
% 60.70/60.72 (P10(x24601,x24602,x24602,x24601)),
% 60.70/60.72 inference(rename_variables,[],[2230])).
% 60.70/60.72 cnf(2462,plain,
% 60.70/60.72 (P4(f25(x24621,x24621,x24621,x24621,x24621,x24621),x24621,x24621)),
% 60.70/60.72 inference(scs_inference,[],[142,2338,2367,2230,2374,2398,2440,2443,2448,2453,2242,2293,2382,2307,1686,1710,2152,2201,2222,2236,1922,2139,2188,2362,2102,2324,2291,2377,2268,2358,2329,2191,2037,1680,1850,426,366,255,360,153,257,1621,225,152,155,485,167,2,169,258,256,166,168,150,232,223,151,165,162,224,163,164,252,254,253,251,198,196,204,200,203,199,261,177,202])).
% 60.70/60.72 cnf(2464,plain,
% 60.70/60.72 (P5(x24641,x24641,x24641,f3(x24641,x24641,x24641))),
% 60.70/60.72 inference(scs_inference,[],[142,2338,2367,2230,2374,2398,2440,2443,2448,2453,2460,2242,2293,2382,2307,1686,1710,2152,2201,2222,2236,1922,2139,2188,2362,2102,2324,2291,2377,2268,2358,2329,2191,2037,1680,1850,426,366,255,360,153,257,1621,225,152,155,485,167,2,169,258,256,166,168,150,232,223,151,165,162,224,163,164,252,254,253,251,198,196,204,200,203,199,261,177,202,187])).
% 60.70/60.72 cnf(2465,plain,
% 60.70/60.72 (P5(x24651,x24651,x24651,x24651)),
% 60.70/60.72 inference(rename_variables,[],[2338])).
% 60.70/60.72 cnf(2466,plain,
% 60.70/60.72 (P10(x24661,x24662,x24662,x24661)),
% 60.70/60.72 inference(rename_variables,[],[2230])).
% 60.70/60.72 cnf(2469,plain,
% 60.70/60.72 (P10(x24691,x24692,x24692,x24692)),
% 60.70/60.72 inference(rename_variables,[],[2293])).
% 60.70/60.72 cnf(2476,plain,
% 60.70/60.72 (P2(x24761,x24761,x24761,x24761)),
% 60.70/60.72 inference(scs_inference,[],[142,2338,2465,2367,2230,2374,2398,2440,2443,2448,2453,2460,2242,2293,2382,2307,1686,1710,2152,2201,2222,2236,1922,2139,2188,2311,2362,2102,2324,2291,2377,2268,2358,2329,2191,2037,2389,1680,281,1850,426,366,255,360,153,257,1621,225,152,155,485,167,2,169,258,256,166,168,150,232,223,151,165,162,224,163,164,252,254,253,251,198,196,204,200,203,199,261,177,202,187,176,156,222,183])).
% 60.70/60.72 cnf(2478,plain,
% 60.70/60.72 (P5(x24781,x24782,x24781,x24782)),
% 60.70/60.72 inference(scs_inference,[],[142,2338,2465,2367,2230,2374,2398,2440,2443,2448,2453,2460,2242,2293,2382,2469,2307,1686,1710,2152,2201,2222,2236,1922,2139,2188,2311,2362,2102,2324,2291,2377,2268,2358,2329,2191,2037,2389,1680,281,1850,426,366,255,360,153,257,1621,225,152,155,485,167,2,169,258,256,166,168,150,232,223,151,165,162,224,163,164,252,254,253,251,198,196,204,200,203,199,261,177,202,187,176,156,222,183,172])).
% 60.70/60.72 cnf(2479,plain,
% 60.70/60.72 (P10(x24791,x24792,x24792,x24792)),
% 60.70/60.72 inference(rename_variables,[],[2293])).
% 60.70/60.72 cnf(2482,plain,
% 60.70/60.72 (P10(x24821,x24821,a16,a16)),
% 60.70/60.72 inference(rename_variables,[],[2236])).
% 60.70/60.72 cnf(2483,plain,
% 60.70/60.72 (P10(x24831,x24832,x24832,x24831)),
% 60.70/60.72 inference(rename_variables,[],[2230])).
% 60.70/60.72 cnf(2486,plain,
% 60.70/60.72 (P10(x24861,x24862,x24862,x24861)),
% 60.70/60.72 inference(rename_variables,[],[2230])).
% 60.70/60.72 cnf(2493,plain,
% 60.70/60.72 (P5(x24931,x24931,x24931,x24931)),
% 60.70/60.72 inference(rename_variables,[],[2338])).
% 60.70/60.72 cnf(2496,plain,
% 60.70/60.72 (P10(x24961,x24962,x24962,x24961)),
% 60.70/60.72 inference(rename_variables,[],[2230])).
% 60.70/60.72 cnf(2501,plain,
% 60.70/60.72 (P6(x25011,x25011,f5(x25011,x25011,x25011),x25011)),
% 60.70/60.72 inference(scs_inference,[],[142,2338,2465,2367,2230,2374,2398,2440,2443,2448,2453,2460,2466,2483,2486,2242,2244,2293,2382,2469,2479,2307,1686,1710,2152,2201,2222,2236,2459,1922,2139,2188,2311,2362,2102,2324,2212,2291,2377,2268,2358,2329,2191,2115,2037,2389,1680,281,1783,1850,426,366,255,360,153,257,1621,225,152,155,485,167,2,169,258,256,166,168,150,232,223,151,165,162,224,163,164,252,254,253,251,198,196,204,200,203,199,261,177,202,187,176,156,222,183,172,188,197,190,180,181,178,235])).
% 60.70/60.72 cnf(2503,plain,
% 60.70/60.72 (P1(f5(x25031,x25031,x25032),x25032,x25031)),
% 60.70/60.72 inference(rename_variables,[],[2268])).
% 60.70/60.72 cnf(2507,plain,
% 60.70/60.72 (P10(x25071,x25072,x25072,x25071)),
% 60.70/60.72 inference(rename_variables,[],[2230])).
% 60.70/60.72 cnf(2511,plain,
% 60.70/60.72 (P10(x25111,x25112,x25112,x25111)),
% 60.70/60.72 inference(rename_variables,[],[2230])).
% 60.70/60.72 cnf(2516,plain,
% 60.70/60.72 (~P10(a1,a19,a2,a18)),
% 60.70/60.72 inference(scs_inference,[],[142,2338,2465,2367,2230,2374,2398,2440,2443,2448,2453,2460,2466,2483,2486,2496,2507,2511,2242,2244,2293,2382,2469,2479,2307,1686,1710,2152,2201,1950,2222,2236,2459,2482,1922,2139,2188,2311,2362,2282,2102,2324,2212,2291,2377,2268,2358,2329,2191,2115,2037,2389,1680,281,1783,1850,426,366,255,360,153,257,1621,225,152,155,485,167,2,169,258,256,166,168,150,232,223,151,165,162,224,163,164,252,254,253,251,198,196,204,200,203,199,261,177,202,187,176,156,222,183,172,188,197,190,180,181,178,235,189,240,226,179])).
% 60.70/60.72 cnf(2528,plain,
% 60.70/60.72 (P4(f5(a16,a16,a16),a16,a16)),
% 60.70/60.72 inference(scs_inference,[],[142,2338,2465,2493,2367,2230,2374,2398,2440,2443,2448,2453,2460,2466,2483,2486,2496,2507,2511,2242,2456,2244,2293,2382,2469,2479,2307,1686,1710,2152,2201,1950,2222,2236,2459,2482,1922,2139,2188,2311,2362,2282,2102,2324,2212,2291,2377,2268,2503,2358,2329,2191,2115,2037,2389,1680,281,1783,1850,426,366,255,360,153,257,1621,225,152,155,485,167,2,169,258,256,166,168,150,232,223,151,165,162,224,163,164,252,254,253,251,198,196,204,200,203,199,261,177,202,187,176,156,222,183,172,188,197,190,180,181,178,235,189,240,226,179,239,283,170,219,160])).
% 60.70/60.72 cnf(2533,plain,
% 60.70/60.72 (P4(x25331,f21(x25331,x25331),x25331)),
% 60.70/60.72 inference(scs_inference,[],[142,2338,2465,2493,2367,2230,2374,2398,2440,2443,2448,2453,2460,2466,2483,2486,2496,2507,2511,2242,2456,2244,2293,2382,2469,2479,2307,1686,1710,2152,2201,1950,2222,2236,2459,2482,1922,2139,2188,2311,2362,2282,2102,2324,2212,2291,2377,2268,2503,2224,2358,2329,2191,2115,2037,2389,1680,281,1783,149,1741,1850,426,366,255,360,153,257,1621,225,152,155,485,167,2,169,258,256,166,168,150,232,223,151,165,162,224,163,164,252,254,253,251,198,196,204,200,203,199,261,177,202,187,176,156,222,183,172,188,197,190,180,181,178,235,189,240,226,179,239,283,170,219,160,237,161])).
% 60.70/60.72 cnf(2541,plain,
% 60.70/60.72 (P10(x25411,f5(x25411,x25411,x25412),x25412,x25411)),
% 60.70/60.72 inference(rename_variables,[],[2302])).
% 60.70/60.72 cnf(2544,plain,
% 60.70/60.72 (P10(x25441,x25441,x25442,x25441)),
% 60.70/60.72 inference(rename_variables,[],[2429])).
% 60.70/60.72 cnf(2546,plain,
% 60.70/60.72 (P9(x25461,x25462,x25462,x25462,x25462,x25462,x25461,x25462)),
% 60.70/60.72 inference(scs_inference,[],[2429,2478,2302,366,426,225])).
% 60.70/60.72 cnf(2548,plain,
% 60.70/60.72 (P8(x25481,x25481,x25481,x25481,a16,x25481,x25481,a16)),
% 60.70/60.72 inference(scs_inference,[],[2429,2478,2407,2302,366,426,225,255])).
% 60.70/60.72 cnf(2550,plain,
% 60.70/60.72 (P4(x25501,x25501,f21(x25501,x25501))),
% 60.70/60.72 inference(scs_inference,[],[2429,2478,2407,2533,2302,366,426,225,255,153])).
% 60.70/60.72 cnf(2557,plain,
% 60.70/60.72 (P8(x25571,a16,x25571,a16,x25571,x25571,x25571,x25571)),
% 60.70/60.72 inference(scs_inference,[],[2429,2478,2407,2533,2302,2450,2136,366,426,225,255,153,283,152,257])).
% 60.70/60.72 cnf(2563,plain,
% 60.70/60.72 (P5(x25631,x25632,x25632,x25631)),
% 60.70/60.72 inference(scs_inference,[],[2429,2478,2407,2501,2533,2302,2450,2136,366,426,225,255,153,283,152,257,155,170,167])).
% 60.70/60.72 cnf(2566,plain,
% 60.70/60.72 (P10(x25661,x25661,x25662,x25661)),
% 60.70/60.72 inference(rename_variables,[],[2429])).
% 60.70/60.72 cnf(2568,plain,
% 60.70/60.72 (P8(a16,x25681,x25681,x25681,x25681,a16,x25681,x25681)),
% 60.70/60.72 inference(scs_inference,[],[2429,2544,2478,2407,2501,2533,2302,2450,2136,366,426,225,255,153,283,152,257,155,170,167,485,258])).
% 60.70/60.72 cnf(2570,plain,
% 60.70/60.72 (P6(x25701,x25701,x25702,x25701)),
% 60.70/60.72 inference(scs_inference,[],[2411,2429,2544,2478,2407,2501,2533,2302,2450,2136,366,426,225,255,153,283,152,257,155,170,167,485,258,169])).
% 60.70/60.72 cnf(2572,plain,
% 60.70/60.72 (P5(x25721,f3(x25721,x25721,x25721),x25721,x25721)),
% 60.70/60.72 inference(scs_inference,[],[2411,2429,2544,2478,2407,2464,2501,2533,2302,2450,2136,366,426,225,255,153,283,152,257,155,170,167,485,258,169,166])).
% 60.70/60.72 cnf(2580,plain,
% 60.70/60.72 (P10(x25801,x25801,x25801,x25802)),
% 60.70/60.72 inference(scs_inference,[],[2411,2429,2544,2566,2478,2407,2464,2501,2274,2533,2302,2272,2450,2136,366,426,225,255,153,283,152,257,155,170,167,485,258,169,166,256,150,151,165])).
% 60.70/60.72 cnf(2584,plain,
% 60.70/60.72 (P9(a1,a17,x25841,x25842,a2,a15,x25841,x25842)),
% 60.70/60.72 inference(scs_inference,[],[2411,2429,2544,2566,2478,2407,2198,2464,2501,2274,2533,2302,2272,2450,2136,1763,366,426,225,255,153,283,152,257,155,170,167,485,258,169,166,256,150,151,165,223,224])).
% 60.70/60.72 cnf(2586,plain,
% 60.70/60.72 (P3(a2,a15,a1,a17)),
% 60.70/60.72 inference(scs_inference,[],[2411,2429,2544,2566,2478,2407,2198,2464,2501,2274,2533,2302,2272,2450,2136,1763,366,426,225,255,153,283,152,257,155,170,167,485,258,169,166,256,150,151,165,223,224,162])).
% 60.70/60.72 cnf(2588,plain,
% 60.70/60.72 (P3(a1,a17,a15,a2)),
% 60.70/60.72 inference(scs_inference,[],[2411,2429,2544,2566,2478,2407,2198,2464,2501,2274,2533,2302,2272,2450,2136,1763,366,426,225,255,153,283,152,257,155,170,167,485,258,169,166,256,150,151,165,223,224,162,163])).
% 60.70/60.72 cnf(2590,plain,
% 60.70/60.72 (P10(a2,a17,a15,a16)),
% 60.70/60.72 inference(scs_inference,[],[2411,2429,2544,2566,2478,2195,2407,2198,2464,2501,2274,2533,2302,2272,2450,2136,1763,366,426,225,255,153,283,152,257,155,170,167,485,258,169,166,256,150,151,165,223,224,162,163,164])).
% 60.70/60.72 cnf(2592,plain,
% 60.70/60.72 (P9(x25921,x25922,a2,a17,x25921,x25922,a16,a15)),
% 60.70/60.72 inference(scs_inference,[],[2411,2429,2544,2566,2478,2195,2407,2246,2198,2464,2501,2274,2533,2302,2272,2450,2136,1763,366,426,225,255,153,283,152,257,155,170,167,485,258,169,166,256,150,151,165,223,224,162,163,164,252])).
% 60.70/60.72 cnf(2600,plain,
% 60.70/60.72 (P1(x26001,x26002,f3(x26001,x26001,x26002))),
% 60.70/60.72 inference(scs_inference,[],[2411,2429,2544,2566,2478,2195,2407,2246,2425,2198,2464,2501,2274,2533,2302,2272,2450,2230,2136,1763,366,426,225,255,153,283,152,257,155,170,167,485,258,169,166,256,150,151,165,223,224,162,163,164,252,253,254,251,175])).
% 60.70/60.72 cnf(2601,plain,
% 60.70/60.72 (P10(x26011,x26012,x26012,x26011)),
% 60.70/60.72 inference(rename_variables,[],[2230])).
% 60.70/60.72 cnf(2603,plain,
% 60.70/60.72 (P6(a15,a2,a16,a16)),
% 60.70/60.72 inference(scs_inference,[],[2411,2429,2544,2566,2478,2195,2216,2407,2246,2425,2198,2464,2501,2274,2533,2302,2272,2450,2230,2136,1763,366,426,225,255,153,283,152,257,155,170,167,485,258,169,166,256,150,151,165,223,224,162,163,164,252,253,254,251,175,184])).
% 60.70/60.72 cnf(2606,plain,
% 60.70/60.72 (P5(x26061,x26062,x26061,x26062)),
% 60.70/60.72 inference(rename_variables,[],[2478])).
% 60.70/60.72 cnf(2607,plain,
% 60.70/60.72 (P10(x26071,x26071,x26072,x26071)),
% 60.70/60.72 inference(rename_variables,[],[2429])).
% 60.70/60.72 cnf(2610,plain,
% 60.70/60.72 (P10(x26101,x26101,x26102,x26101)),
% 60.70/60.72 inference(rename_variables,[],[2429])).
% 60.70/60.72 cnf(2613,plain,
% 60.70/60.72 (P5(x26131,x26132,x26131,x26132)),
% 60.70/60.72 inference(rename_variables,[],[2478])).
% 60.70/60.72 cnf(2614,plain,
% 60.70/60.72 (P10(x26141,x26141,x26142,x26141)),
% 60.70/60.72 inference(rename_variables,[],[2429])).
% 60.70/60.72 cnf(2624,plain,
% 60.70/60.72 (P10(x26241,x26242,x26242,x26241)),
% 60.70/60.72 inference(rename_variables,[],[2230])).
% 60.70/60.72 cnf(2628,plain,
% 60.70/60.72 (P2(x26281,x26282,x26282,x26282)),
% 60.70/60.72 inference(scs_inference,[],[2411,2429,2544,2566,2607,2610,2478,2606,2613,1581,2195,2216,2407,2246,2425,2198,2462,2464,2501,2274,2533,2302,2272,2450,271,2230,2601,2136,1763,2084,366,426,225,255,153,283,152,257,155,170,167,485,258,169,166,256,150,151,165,223,224,162,163,164,252,253,254,251,175,184,198,196,200,261,248,187,222,183])).
% 60.70/60.72 cnf(2630,plain,
% 60.70/60.72 (P5(f3(a16,a16,a16),a16,f3(a16,a16,a16),f3(a16,a16,a16))),
% 60.70/60.72 inference(scs_inference,[],[2411,2429,2544,2566,2607,2610,2478,2606,2613,1581,2195,2216,2407,2246,2425,2198,2462,2464,2501,2274,2533,2302,2272,1989,2450,271,2230,2601,2624,2136,1763,2084,366,426,225,255,153,283,152,257,155,170,167,485,258,169,166,256,150,151,165,223,224,162,163,164,252,253,254,251,175,184,198,196,200,261,248,187,222,183,172])).
% 60.70/60.72 cnf(2631,plain,
% 60.70/60.72 (P10(x26311,x26312,x26312,x26311)),
% 60.70/60.72 inference(rename_variables,[],[2230])).
% 60.70/60.72 cnf(2634,plain,
% 60.70/60.72 (P10(x26341,x26342,x26342,x26342)),
% 60.70/60.72 inference(rename_variables,[],[2293])).
% 60.70/60.72 cnf(2639,plain,
% 60.70/60.72 (P10(x26391,x26391,x26392,x26391)),
% 60.70/60.72 inference(rename_variables,[],[2429])).
% 60.70/60.72 cnf(2645,plain,
% 60.70/60.72 (P10(x26451,x26452,x26452,x26452)),
% 60.70/60.72 inference(rename_variables,[],[2293])).
% 60.70/60.72 cnf(2647,plain,
% 60.70/60.72 (~P3(a1,a19,a18,a18)),
% 60.70/60.72 inference(scs_inference,[],[2411,2429,2544,2566,2607,2610,2614,2639,2478,2606,2613,1581,2195,2216,2407,2246,2425,2198,2516,2462,2464,2501,2274,2533,2302,2272,1989,2450,271,2230,2601,2624,2631,2293,2634,2136,1763,2084,366,426,225,255,153,283,152,257,155,170,167,485,258,169,166,256,150,151,165,223,224,162,163,164,252,253,254,251,175,184,198,196,200,261,248,187,222,183,172,176,156,197,190,188,181])).
% 60.70/60.72 cnf(2648,plain,
% 60.70/60.72 (P10(x26481,x26481,x26482,x26481)),
% 60.70/60.72 inference(rename_variables,[],[2429])).
% 60.70/60.72 cnf(2653,plain,
% 60.70/60.72 (P10(x26531,x26531,x26532,x26532)),
% 60.70/60.72 inference(scs_inference,[],[2411,2429,2544,2566,2607,2610,2614,2639,2478,2606,2613,1581,2195,2216,2407,2246,2425,2198,2397,2516,2462,2464,2501,2274,2533,2302,2272,1989,2450,271,2230,2601,2624,2631,2293,2634,2136,1763,2084,1783,366,426,225,255,153,283,152,257,155,170,167,485,258,169,166,256,150,151,165,223,224,162,163,164,252,253,254,251,175,184,198,196,200,261,248,187,222,183,172,176,156,197,190,188,181,178,180])).
% 60.70/60.72 cnf(2655,plain,
% 60.70/60.72 (P6(a1,a1,a15,a2)),
% 60.70/60.72 inference(scs_inference,[],[2411,2429,2544,2566,2607,2610,2614,2639,2478,2606,2613,1581,2195,2216,2407,2246,2425,1684,2198,2397,2516,2462,2464,2501,2274,2533,2302,2272,1989,2450,271,2230,2601,2624,2631,2293,2634,2136,1763,2084,1946,1783,366,426,225,255,153,283,152,257,155,170,167,485,258,169,166,256,150,151,165,223,224,162,163,164,252,253,254,251,175,184,198,196,200,261,248,187,222,183,172,176,156,197,190,188,181,178,180,235])).
% 60.70/60.72 cnf(2658,plain,
% 60.70/60.72 (P10(x26581,f5(x26582,x26581,x26582),x26582,x26582)),
% 60.70/60.72 inference(scs_inference,[],[2411,2429,2544,2566,2607,2610,2614,2639,2648,2478,2606,2613,1581,2195,2216,2407,2246,2425,1684,2198,2397,2516,2462,2464,2501,2274,2533,2302,2272,1989,2450,271,2230,2601,2624,2631,2293,2634,2645,2136,1763,2084,1946,1783,366,426,225,255,153,283,152,257,155,170,167,485,258,169,166,256,150,151,165,223,224,162,163,164,252,253,254,251,175,184,198,196,200,261,248,187,222,183,172,176,156,197,190,188,181,178,180,235,189])).
% 60.70/60.72 cnf(2666,plain,
% 60.70/60.72 (P9(x26661,x26661,x26661,x26661,x26661,x26661,x26661,f25(x26661,x26661,x26661,x26661,x26661,x26661))),
% 60.70/60.72 inference(scs_inference,[],[2476,2411,2429,2544,2566,2607,2610,2614,2639,2648,2478,2606,2613,1581,2195,2216,2407,2246,2425,1684,2198,2397,2516,2462,2464,2501,2274,2533,2302,2541,2272,1989,2450,271,2230,2601,2624,2631,2293,2634,2645,1785,2136,1763,2084,1946,1783,366,426,225,255,153,283,152,257,155,170,167,485,258,169,166,256,150,151,165,223,224,162,163,164,252,253,254,251,175,184,198,196,200,261,248,187,222,183,172,176,156,197,190,188,181,178,180,235,189,99,240,226])).
% 60.70/60.72 cnf(2679,plain,
% 60.70/60.72 (P4(f6(a16,a16,a15),a16,a15)),
% 60.70/60.72 inference(scs_inference,[],[2476,2411,2429,2544,2566,2607,2610,2614,2639,2648,2478,2606,2613,1581,2195,2216,2381,2407,2246,2425,1684,2198,2397,2516,2445,2462,2464,2501,2274,2533,2302,2541,2272,1989,2450,271,2230,2601,2624,2631,2293,2634,2645,1785,2136,1763,2118,2084,2242,1998,1946,2177,1783,366,426,225,255,153,283,152,257,155,170,167,485,258,169,166,256,150,151,165,223,224,162,163,164,252,253,254,251,175,184,198,196,200,261,248,187,222,183,172,176,156,197,190,188,181,178,180,235,189,99,240,226,179,239,191,185])).
% 60.70/60.72 cnf(2680,plain,
% 60.70/60.72 (P4(f25(x26801,x26801,x26801,x26801,x26801,x26801),x26801,x26801)),
% 60.70/60.72 inference(rename_variables,[],[2462])).
% 60.70/60.72 cnf(2683,plain,
% 60.70/60.72 (P4(f25(a16,a16,a16,a16,a16,a16),f25(a16,a16,a16,a16,a16,a16),a16)),
% 60.70/60.72 inference(scs_inference,[],[2476,2411,2429,2544,2566,2607,2610,2614,2639,2648,2478,2606,2613,1581,2195,2216,2381,2407,2246,2425,1684,2198,2397,2516,2445,2462,2680,2464,2501,2274,2533,2302,2541,2272,1989,2450,2238,271,2230,2601,2624,2631,2293,2634,2645,1785,2136,1763,2118,2084,2242,1998,1946,2177,1783,366,426,225,255,153,283,152,257,155,170,167,485,258,169,166,256,150,151,165,223,224,162,163,164,252,253,254,251,175,184,198,196,200,261,248,187,222,183,172,176,156,197,190,188,181,178,180,235,189,99,240,226,179,239,191,185,174])).
% 60.70/60.72 cnf(2687,plain,
% 60.70/60.72 (P1(x26871,x26871,x26872)),
% 60.70/60.72 inference(rename_variables,[],[2070])).
% 60.70/60.72 cnf(2691,plain,
% 60.70/60.72 (P1(a15,a16,a2)),
% 60.70/60.72 inference(scs_inference,[],[142,2476,2411,2429,2544,2566,2607,2610,2614,2639,2648,2478,2606,2613,1581,2195,2216,2381,2407,2246,2425,1684,2198,2397,2516,2445,2462,2680,2464,2501,2274,2533,2302,2541,2272,1989,2450,2238,271,2230,2601,2624,2631,2293,2634,2645,1785,2136,1763,2070,2118,2084,2242,1998,1765,1946,2177,1783,1741,366,426,225,255,153,283,152,257,155,170,167,485,258,169,166,256,150,151,165,223,224,162,163,164,252,253,254,251,175,184,198,196,200,261,248,187,222,183,172,176,156,197,190,188,181,178,180,235,189,99,240,226,179,239,191,185,174,205,159])).
% 60.70/60.72 cnf(2693,plain,
% 60.70/60.72 (P10(f7(x26931,x26931,x26931,x26932),x26931,x26931,x26932)),
% 60.70/60.72 inference(scs_inference,[],[142,2476,2411,2429,2544,2566,2607,2610,2614,2639,2648,2478,2606,2613,1581,2195,2216,2381,2407,2246,2425,1684,2198,2397,2516,2445,2462,2680,2464,2501,2274,2533,2302,2541,2272,1989,2450,2238,271,2230,2601,2624,2631,2293,2634,2645,1785,2136,1763,2070,2118,2084,2242,1998,1765,1946,2177,1783,1741,366,426,225,255,153,283,152,257,155,170,167,485,258,169,166,256,150,151,165,223,224,162,163,164,252,253,254,251,175,184,198,196,200,261,248,187,222,183,172,176,156,197,190,188,181,178,180,235,189,99,240,226,179,239,191,185,174,205,159,186])).
% 60.70/60.72 cnf(2696,plain,
% 60.70/60.72 (P6(a2,a15,a16,a16)),
% 60.70/60.72 inference(scs_inference,[],[142,2476,2411,2429,2544,2566,2607,2610,2614,2639,2648,2478,2606,2613,1581,2195,2216,2381,2407,2246,2425,1684,2198,2397,2516,2445,2462,2680,2464,2501,2274,2533,2302,2541,2272,1989,2450,2238,271,2230,2601,2624,2631,2293,2634,2645,1785,2136,1763,2070,2118,2084,2242,1998,1765,1946,2177,1783,1741,366,426,225,255,153,283,152,257,155,170,167,485,258,169,166,256,150,151,165,223,224,162,163,164,252,253,254,251,175,184,198,196,200,261,248,187,222,183,172,176,156,197,190,188,181,178,180,235,189,99,240,226,179,239,191,185,174,205,159,186,2,168])).
% 60.70/60.72 cnf(2700,plain,
% 60.70/60.72 (P8(a15,a15,a15,a17,a15,a16,a16,a2)),
% 60.70/60.72 inference(scs_inference,[],[142,2476,2411,2429,2544,2566,2607,2610,2614,2639,2648,2478,2606,2613,1581,2195,2216,2381,2407,2246,2425,1684,2198,2397,2516,2445,2462,2680,2464,2501,2274,2533,2302,2541,2272,1989,2450,2238,271,605,2230,2601,2624,2631,2293,2634,2645,1785,2136,1763,2070,2687,2118,2084,2242,1998,1765,1946,2177,1783,1741,366,426,225,255,153,283,152,257,155,170,167,485,258,169,166,256,150,151,165,223,224,162,163,164,252,253,254,251,175,184,198,196,200,261,248,187,222,183,172,176,156,197,190,188,181,178,180,235,189,99,240,226,179,239,191,185,174,205,159,186,2,168,220,671])).
% 60.70/60.72 cnf(2709,plain,
% 60.70/60.72 (P10(x27091,x27091,x27091,x27092)),
% 60.70/60.72 inference(rename_variables,[],[2580])).
% 60.70/60.72 cnf(2711,plain,
% 60.70/60.72 (P8(a15,a16,a16,a2,a15,a15,a15,a17)),
% 60.70/60.72 inference(scs_inference,[],[2580,2700,426,255])).
% 60.70/60.72 cnf(2713,plain,
% 60.70/60.72 (P10(a15,a16,a17,a17)),
% 60.70/60.72 inference(scs_inference,[],[2580,2709,2700,426,255,366])).
% 60.70/60.72 cnf(2714,plain,
% 60.70/60.72 (P10(x27141,x27141,x27141,x27142)),
% 60.70/60.72 inference(rename_variables,[],[2580])).
% 60.70/60.72 cnf(2718,plain,
% 60.70/60.72 (P8(x27181,a16,x27181,x27181,x27181,a16,x27181,x27181)),
% 60.70/60.72 inference(scs_inference,[],[2580,2709,2700,2568,2679,426,255,366,152,257])).
% 60.70/60.72 cnf(2722,plain,
% 60.70/60.72 (P4(f25(a16,a16,a16,a16,a16,a16),a16,f25(a16,a16,a16,a16,a16,a16))),
% 60.70/60.72 inference(scs_inference,[],[2580,2709,2700,2568,2550,2683,2679,426,255,366,152,257,155,153])).
% 60.70/60.72 cnf(2729,plain,
% 60.70/60.72 (P10(x27291,x27291,x27291,x27292)),
% 60.70/60.72 inference(rename_variables,[],[2580])).
% 60.70/60.72 cnf(2733,plain,
% 60.70/60.72 (P5(x27331,x27331,f27(x27331,x27332,x27331,x27331,x27331),x27331)),
% 60.70/60.72 inference(scs_inference,[],[2570,2580,2709,2714,2700,2568,2603,2572,2439,2550,2683,2679,426,255,366,152,257,155,153,225,170,485,169,167])).
% 60.70/60.72 cnf(2741,plain,
% 60.70/60.72 (P6(a16,a15,a2,a16)),
% 60.70/60.72 inference(scs_inference,[],[2570,2580,2709,2714,2700,2568,2603,2572,2439,2550,2683,2679,426,255,366,152,257,155,153,225,170,485,169,167,258,166,256,168])).
% 60.70/60.72 cnf(2743,plain,
% 60.70/60.72 (P1(a16,a15,a2)),
% 60.70/60.72 inference(scs_inference,[],[2570,2580,2709,2714,2700,2568,2603,2691,2572,2439,2550,2683,2679,426,255,366,152,257,155,153,225,170,485,169,167,258,166,256,168,150])).
% 60.70/60.72 cnf(2745,plain,
% 60.70/60.72 (P1(a15,a2,a16)),
% 60.70/60.72 inference(scs_inference,[],[2570,2580,2709,2714,2700,2568,2603,2691,2572,2439,2550,2683,2679,426,255,366,152,257,155,153,225,170,485,169,167,258,166,256,168,150,151])).
% 60.70/60.72 cnf(2757,plain,
% 60.70/60.72 (P10(x27571,x27572,x27571,x27571)),
% 60.70/60.72 inference(scs_inference,[],[2570,2580,2709,2714,2729,2423,2588,2700,2568,2590,2603,2691,2572,2439,2550,2683,2679,426,255,366,152,257,155,153,225,170,485,169,167,258,166,256,168,150,151,223,165,162,224,163,164])).
% 60.70/60.72 cnf(2759,plain,
% 60.70/60.72 (P9(x27591,x27591,x27592,x27591,x27592,x27591,x27591,x27591)),
% 60.70/60.72 inference(scs_inference,[],[2546,2570,2580,2709,2714,2729,2423,2588,2700,2568,2590,2603,2691,2572,2439,2550,2683,2679,426,255,366,152,257,155,153,225,170,485,169,167,258,166,256,168,150,151,223,165,162,224,163,164,252])).
% 60.70/60.72 cnf(2761,plain,
% 60.70/60.72 (P9(x27611,x27612,x27611,x27611,x27611,x27611,x27612,x27611)),
% 60.70/60.72 inference(scs_inference,[],[2546,2570,2580,2709,2714,2729,2423,2588,2700,2568,2590,2603,2691,2572,2439,2550,2683,2679,426,255,366,152,257,155,153,225,170,485,169,167,258,166,256,168,150,151,223,165,162,224,163,164,252,253])).
% 60.70/60.72 cnf(2768,plain,
% 60.70/60.72 (P10(x27681,x27681,x27681,x27682)),
% 60.70/60.72 inference(rename_variables,[],[2580])).
% 60.70/60.72 cnf(2770,plain,
% 60.70/60.72 (P5(a16,f5(a16,a16,a16),x27701,f5(a16,a16,a16))),
% 60.70/60.72 inference(scs_inference,[],[2546,2570,2580,2709,2714,2729,2423,2588,1928,2700,2568,2584,2590,2603,2691,2572,2439,2550,2528,2683,2679,2230,426,255,366,152,257,155,153,225,170,485,169,167,258,166,256,168,150,151,223,165,162,224,163,164,252,253,254,251,247,173])).
% 60.70/60.72 cnf(2771,plain,
% 60.70/60.72 (P10(x27711,x27712,x27712,x27711)),
% 60.70/60.72 inference(rename_variables,[],[2230])).
% 60.70/60.72 cnf(2773,plain,
% 60.70/60.72 (P9(x27731,x27732,x27731,x27731,x27731,x27731,x27731,x27731)),
% 60.70/60.72 inference(scs_inference,[],[2546,2570,2580,2709,2714,2729,2768,2628,2423,2588,1928,2700,2568,2584,2590,2603,2691,2572,2439,2550,2528,2683,2679,2230,426,255,366,152,257,155,153,225,170,485,169,167,258,166,256,168,150,151,223,165,162,224,163,164,252,253,254,251,247,173,228])).
% 60.70/60.72 cnf(2774,plain,
% 60.70/60.72 (P2(x27741,x27742,x27742,x27742)),
% 60.70/60.72 inference(rename_variables,[],[2628])).
% 60.70/60.72 cnf(2779,plain,
% 60.70/60.72 (P10(x27791,x27791,x27791,x27792)),
% 60.70/60.72 inference(rename_variables,[],[2580])).
% 60.70/60.72 cnf(2782,plain,
% 60.70/60.72 (P10(x27821,x27821,x27821,x27822)),
% 60.70/60.72 inference(rename_variables,[],[2580])).
% 60.70/60.72 cnf(2783,plain,
% 60.70/60.72 (P5(x27831,x27832,x27832,x27831)),
% 60.70/60.72 inference(rename_variables,[],[2563])).
% 60.70/60.72 cnf(2786,plain,
% 60.70/60.72 (P10(x27861,x27861,x27861,x27862)),
% 60.70/60.72 inference(rename_variables,[],[2580])).
% 60.70/60.72 cnf(2792,plain,
% 60.70/60.72 (P5(x27921,x27922,x27922,x27921)),
% 60.70/60.72 inference(rename_variables,[],[2563])).
% 60.70/60.72 cnf(2795,plain,
% 60.70/60.72 (P10(x27951,x27951,x27951,x27952)),
% 60.70/60.72 inference(rename_variables,[],[2580])).
% 60.70/60.72 cnf(2801,plain,
% 60.70/60.72 (P2(x28011,f3(x28011,x28011,x28011),x28011,x28011)),
% 60.70/60.72 inference(scs_inference,[],[142,2546,2563,2783,2792,2570,2580,2709,2714,2729,2768,2779,2782,2786,2628,2356,1767,1926,2423,2588,1928,2700,2568,2584,2590,2603,2691,2572,2439,2550,2528,2630,2683,2679,2230,1936,426,255,366,152,257,155,153,225,170,485,169,167,258,166,256,168,150,151,223,165,162,224,163,164,252,253,254,251,247,173,228,262,196,200,246,242,199,198,261,183])).
% 60.70/60.72 cnf(2805,plain,
% 60.70/60.72 (~P4(f21(a18,a1),a19,a18)),
% 60.70/60.72 inference(scs_inference,[],[142,2546,2563,2783,2792,2570,2580,2709,2714,2729,2768,2779,2782,2786,2628,2356,1767,1926,2423,2588,1928,2700,2568,2584,2590,2603,2647,2691,2572,2439,2550,2528,2630,2683,2679,2230,2037,1936,426,255,366,152,257,155,153,225,170,485,169,167,258,166,256,168,150,151,223,165,162,224,163,164,252,253,254,251,247,173,228,262,196,200,246,242,199,198,261,183,222,156])).
% 60.70/60.72 cnf(2809,plain,
% 60.70/60.72 (P10(x28091,x28092,x28092,x28091)),
% 60.70/60.72 inference(rename_variables,[],[2230])).
% 60.70/60.72 cnf(2811,plain,
% 60.70/60.72 (~P3(a18,a2,a19,a19)),
% 60.70/60.72 inference(scs_inference,[],[142,2546,2563,2783,2792,2570,2580,2709,2714,2729,2768,2779,2782,2786,2795,2628,2356,1767,1926,2423,2588,1928,2700,2568,2584,2590,2603,2647,2691,2572,2439,2550,2528,2630,2683,2679,2127,2230,2771,2037,1936,426,255,366,152,257,155,153,225,170,485,169,167,258,166,256,168,150,151,223,165,162,224,163,164,252,253,254,251,247,173,228,262,196,200,246,242,199,198,261,183,222,156,172,181])).
% 60.70/60.72 cnf(2812,plain,
% 60.70/60.72 (P10(x28121,x28121,x28121,x28122)),
% 60.70/60.72 inference(rename_variables,[],[2580])).
% 60.70/60.72 cnf(2814,plain,
% 60.70/60.72 (~P3(a19,a1,a18,a18)),
% 60.70/60.72 inference(scs_inference,[],[142,2546,2563,2783,2792,2570,2580,2709,2714,2729,2768,2779,2782,2786,2795,2628,2356,1767,1926,2423,2588,1928,2700,2568,2584,2590,2603,2647,2691,2572,2439,2550,2528,2630,2683,2679,2127,2230,2771,2037,1936,1783,426,255,366,152,257,155,153,225,170,485,169,167,258,166,256,168,150,151,223,165,162,224,163,164,252,253,254,251,247,173,228,262,196,200,246,242,199,198,261,183,222,156,172,181,178])).
% 60.70/60.72 cnf(2815,plain,
% 60.70/60.72 (P3(x28151,x28152,x28152,x28151)),
% 60.70/60.72 inference(rename_variables,[],[1783])).
% 60.70/60.72 cnf(2817,plain,
% 60.70/60.72 (P10(f12(x28171,a1,x28171,a2,a15),x28171,a2,a15)),
% 60.70/60.72 inference(scs_inference,[],[142,2546,2563,2783,2792,2570,2580,2709,2714,2729,2768,2779,2782,2786,2795,2812,2628,2356,1767,1926,2423,2588,1928,2700,2568,2584,2590,2603,2647,2691,2572,2439,2550,2528,2630,2683,2679,2127,2230,2771,2037,1936,1783,426,255,366,152,257,155,153,225,170,485,169,167,258,166,256,168,150,151,223,165,162,224,163,164,252,253,254,251,247,173,228,262,196,200,246,242,199,198,261,183,222,156,172,181,178,197])).
% 60.70/60.72 cnf(2818,plain,
% 60.70/60.72 (P10(x28181,x28181,x28181,x28182)),
% 60.70/60.72 inference(rename_variables,[],[2580])).
% 60.70/60.72 cnf(2821,plain,
% 60.70/60.72 (P10(x28211,x28212,x28212,x28211)),
% 60.70/60.72 inference(rename_variables,[],[2230])).
% 60.70/60.72 cnf(2823,plain,
% 60.70/60.72 (P6(a16,f3(a16,a16,a16),a16,f3(a16,a16,a16))),
% 60.70/60.72 inference(scs_inference,[],[142,2546,2563,2783,2792,2570,2580,2709,2714,2729,2768,2779,2782,2786,2795,2812,2628,2356,1767,1926,2423,2588,1928,2700,2568,2584,2590,2603,2647,2691,2572,2439,2550,2528,2630,2683,1883,2679,2127,2230,2771,2809,2037,1936,1765,1783,426,255,366,152,257,155,153,225,170,485,169,167,258,166,256,168,150,151,223,165,162,224,163,164,252,253,254,251,247,173,228,262,196,200,246,242,199,198,261,183,222,156,172,181,178,197,190,235])).
% 60.70/60.72 cnf(2826,plain,
% 60.70/60.72 (P10(a16,a15,a16,a2)),
% 60.70/60.72 inference(scs_inference,[],[142,2546,2563,2783,2792,2570,2580,2709,2714,2729,2768,2779,2782,2786,2795,2812,2818,2628,2356,1767,1926,2423,2588,1928,2700,2568,2584,2590,2603,2647,2691,2572,2439,2550,2528,2630,2683,1883,2679,2127,2230,2771,2809,2037,1936,1765,1783,426,255,366,152,257,155,153,225,170,485,169,167,258,166,256,168,150,151,223,165,162,224,163,164,252,253,254,251,247,173,228,262,196,200,246,242,199,198,261,183,222,156,172,181,178,197,190,235,240])).
% 60.70/60.72 cnf(2832,plain,
% 60.70/60.72 (~P10(a19,a1,a18,a18)),
% 60.70/60.72 inference(scs_inference,[],[142,2546,2563,2783,2792,2570,2580,2709,2714,2729,2768,2779,2782,2786,2795,2812,2818,2628,2774,2356,1767,1926,2423,2588,1928,2700,2568,2584,2590,2603,2647,2691,2572,2439,2550,2528,2630,2683,1883,2679,2127,2230,2771,2809,2821,2037,1936,1765,1783,426,255,366,152,257,155,153,225,170,485,169,167,258,166,256,168,150,151,223,165,162,224,163,164,252,253,254,251,247,173,228,262,196,200,246,242,199,198,261,183,222,156,172,181,178,197,190,235,240,226,179])).
% 60.70/60.72 cnf(2839,plain,
% 60.70/60.72 (P5(x28391,x28391,x28391,f25(x28391,x28391,x28391,x28391,x28391,x28391))),
% 60.70/60.72 inference(scs_inference,[],[142,2546,2563,2783,2792,2570,2580,2709,2714,2729,2768,2779,2782,2786,2795,2812,2818,2628,2774,2356,1767,1926,2423,2588,1928,2700,2568,2584,2592,2590,2603,2647,2691,2666,2572,2439,2447,2550,2528,2630,2683,1883,2679,2127,2411,2230,2771,2809,2821,2037,1936,1765,1783,426,255,366,152,257,155,153,225,170,485,169,167,258,166,256,168,150,151,223,165,162,224,163,164,252,253,254,251,247,173,228,262,196,200,246,242,199,198,261,183,222,156,172,181,178,197,190,235,240,226,179,239,250])).
% 60.70/60.72 cnf(2846,plain,
% 60.70/60.72 (P3(x28461,a1,x28461,x28461)),
% 60.70/60.72 inference(scs_inference,[],[142,2546,2563,2783,2792,2570,2580,2709,2714,2729,2768,2779,2782,2786,2795,2812,2818,2628,2774,2356,1767,1926,2423,2588,1928,2700,2568,2584,2592,2590,2603,2647,2691,2666,2572,2439,2447,2550,2528,2630,2683,1883,2679,2127,2411,2230,2771,2809,2821,2037,1936,1765,1783,2815,143,426,255,366,152,257,155,153,225,170,485,169,167,258,166,256,168,150,151,223,165,162,224,163,164,252,253,254,251,247,173,228,262,196,200,246,242,199,198,261,183,222,156,172,181,178,197,190,235,240,226,179,239,250,205,232])).
% 60.70/60.72 cnf(2866,plain,
% 60.70/60.72 (P10(f7(x28661,x28661,x28661,x28662),x28661,x28661,x28662)),
% 60.70/60.72 inference(rename_variables,[],[2693])).
% 60.70/60.72 cnf(2871,plain,
% 60.70/60.72 (P10(f7(x28711,x28711,x28711,x28712),x28711,x28711,x28712)),
% 60.70/60.72 inference(rename_variables,[],[2693])).
% 60.70/60.72 cnf(2928,plain,
% 60.70/60.72 (P5(x29281,x29281,x29281,f25(x29281,x29281,x29281,x29281,x29281,x29281))),
% 60.70/60.72 inference(rename_variables,[],[2839])).
% 60.70/60.72 cnf(2933,plain,
% 60.70/60.72 (P10(x29331,x29332,x29331,x29331)),
% 60.70/60.72 inference(rename_variables,[],[2757])).
% 60.70/60.72 cnf(2940,plain,
% 60.70/60.72 (P10(x29401,x29402,x29401,x29401)),
% 60.70/60.72 inference(rename_variables,[],[2757])).
% 60.70/60.72 cnf(2944,plain,
% 60.70/60.72 (P5(a16,f5(a16,a16,a16),x29441,f5(a16,a16,a16))),
% 60.70/60.72 inference(rename_variables,[],[2770])).
% 60.70/60.72 cnf(2951,plain,
% 60.70/60.72 (P10(x29511,x29512,x29511,x29511)),
% 60.70/60.72 inference(rename_variables,[],[2757])).
% 60.70/60.72 cnf(2955,plain,
% 60.70/60.72 (P10(x29551,x29552,x29551,x29551)),
% 60.70/60.72 inference(rename_variables,[],[2757])).
% 60.70/60.72 cnf(2958,plain,
% 60.70/60.72 (P10(x29581,x29582,x29581,x29581)),
% 60.70/60.72 inference(rename_variables,[],[2757])).
% 60.70/60.72 cnf(2983,plain,
% 60.70/60.72 ($false),
% 60.70/60.72 inference(scs_inference,[],[2759,2761,2773,2757,2933,2940,2951,2955,2958,2713,2066,2373,2427,2548,2557,2586,2696,2718,2846,2409,2655,2711,2741,2743,2745,2811,2814,2826,2832,2839,2928,2801,2733,2693,2866,2871,2600,2006,2770,2944,2722,2823,2817,2805,331,2658,1964,2653,2563,2580,2191,2679,2047,1769,2037,2242,1946,426,255,366,153,225,257,155,485,170,169,166,258,167,256,232,168,150,151,165,223,162,163,164,224,252,253,254,251,193,182,134,196,261,246,242,183,222,103,156,197,181,178,180,104,240,235,190,226,179]),
% 60.70/60.72 ['proof']).
% 60.70/60.72 % SZS output end Proof
% 60.70/60.72 % Total time :60.050000s
%------------------------------------------------------------------------------