%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : GEO550+1 : TPTP v8.2.0. Released v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% Computer : n017.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Mon Jun 24 06:05:42 EDT 2024
% Result : Theorem 61.04s 61.31s
% Output : CNFRefutation 61.18s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.06/0.12 % Problem : GEO550+1 : TPTP v8.2.0. Released v7.5.0.
% 0.06/0.12 % Command : java -jar /export/starexec/sandbox/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 09:40:54 EDT 2024
% 0.12/0.34 % CPUTime :
% 0.20/0.56 start to proof:theBenchmark
% 61.04/61.30 %-------------------------------------------
% 61.04/61.30 % File :CSE---1.7
% 61.04/61.30 % Problem :theBenchmark
% 61.04/61.30 % Transform :cnf
% 61.04/61.30 % Format :tptp:raw
% 61.04/61.30 % Command :java -jar mcs_scs.jar %d %s
% 61.04/61.30
% 61.04/61.30 % Result :Theorem 60.490000s
% 61.04/61.30 % Output :CNFRefutation 60.490000s
% 61.04/61.30 %-------------------------------------------
% 61.04/61.31 %------------------------------------------------------------------------------
% 61.04/61.31 % File : GEO550+1 : TPTP v8.2.0. Released v7.5.0.
% 61.04/61.31 % Domain : Geometry
% 61.04/61.31 % Problem : JGEX problem 10
% 61.04/61.31 % Version : [CGZ00] axioms.
% 61.04/61.31 % English :
% 61.04/61.31
% 61.04/61.31 % Refs : [CGZ00] Chou et al. (2000), A Deductive Database Approach to A
% 61.04/61.31 % : [YCG08] Ye et al. (2008), An Introduction to Java Geometry Exp
% 61.04/61.31 % : [Qua20] Quaresma (2020), Email to Geoff Sutcliffe
% 61.04/61.31 % Source : [Qua20]
% 61.04/61.31 % Names : 10.p [Qua20]
% 61.04/61.31
% 61.04/61.31 % Status : Theorem
% 61.04/61.31 % Rating : 0.39 v8.1.0, 0.50 v7.5.0
% 61.04/61.31 % Syntax : Number of formulae : 95 ( 0 unt; 0 def)
% 61.04/61.31 % Number of atoms : 292 ( 1 equ)
% 61.04/61.31 % Maximal formula atoms : 9 ( 3 avg)
% 61.04/61.31 % Number of connectives : 204 ( 7 ~; 0 |; 102 &)
% 61.04/61.31 % ( 0 <=>; 95 =>; 0 <=; 0 <~>)
% 61.04/61.31 % Maximal formula depth : 20 ( 9 avg)
% 61.04/61.31 % Maximal term depth : 1 ( 1 avg)
% 61.04/61.31 % Number of predicates : 12 ( 11 usr; 0 prp; 2-8 aty)
% 61.04/61.31 % Number of functors : 0 ( 0 usr; 0 con; --- aty)
% 61.04/61.31 % Number of variables : 533 ( 513 !; 20 ?)
% 61.04/61.31 % SPC : FOF_THM_RFO_SEQ
% 61.04/61.31
% 61.04/61.31 % Comments : Taken from JGEX [YCG08], converted by Pedro Quaresma.
% 61.04/61.31 %------------------------------------------------------------------------------
% 61.04/61.31 include('Axioms/GEO012+0.ax').
% 61.04/61.31 %------------------------------------------------------------------------------
% 61.04/61.31 fof(exemplo6GDDFULL012010,conjecture,
% 61.04/61.31 ! [A,B,C,D,P,E,O1,O,Q,NWPNT1,NWPNT2] :
% 61.04/61.31 ( ( coll(P,C,D)
% 61.04/61.31 & coll(P,A,B)
% 61.04/61.31 & coll(E,B,C)
% 61.04/61.31 & coll(E,A,D)
% 61.04/61.31 & circle(O1,C,D,E)
% 61.04/61.31 & circle(O,E,B,A)
% 61.04/61.31 & circle(O1,C,Q,NWPNT1)
% 61.04/61.31 & circle(O,A,Q,NWPNT2) )
% 61.04/61.31 => cyclic(P,D,Q,A) ) ).
% 61.04/61.31
% 61.04/61.31 %------------------------------------------------------------------------------
% 61.04/61.31 %-------------------------------------------
% 61.04/61.31 % Proof found
% 61.04/61.31 % SZS status Theorem for theBenchmark
% 61.04/61.31 % SZS output start Proof
% 61.04/61.32 %ClaNum:263(EqnAxiom:141)
% 61.04/61.32 %VarNum:1613(SingletonVarNum:590)
% 61.04/61.32 %MaxLitNum:5
% 61.04/61.32 %MaxfuncDepth:1
% 61.04/61.32 %SharedTerms:20
% 61.04/61.32 %goalClause: 142 143 144 145 146 147 148 149 150
% 61.04/61.32 %singleGoalClaCount:9
% 61.04/61.32 [142]P1(a1,a2,a15)
% 61.04/61.32 [143]P1(a1,a16,a17)
% 61.04/61.32 [144]P1(a18,a2,a17)
% 61.04/61.32 [145]P1(a18,a15,a16)
% 61.04/61.32 [146]P2(a19,a16,a17,a18)
% 61.04/61.32 [147]P2(a19,a16,a20,a22)
% 61.04/61.32 [148]P2(a21,a2,a20,a24)
% 61.04/61.32 [149]P2(a21,a18,a15,a2)
% 61.04/61.32 [150]~P3(a1,a17,a20,a2)
% 61.04/61.32 [151]~P1(x1512,x1511,x1513)+P1(x1511,x1512,x1513)
% 61.04/61.32 [152]~P1(x1521,x1523,x1522)+P1(x1521,x1522,x1523)
% 61.04/61.32 [153]~P6(x1531,x1532,x1533)+P1(x1531,x1532,x1533)
% 61.04/61.32 [154]~P6(x1541,x1543,x1542)+P6(x1541,x1542,x1543)
% 61.04/61.32 [156]~P6(x1561,x1562,x1563)+P4(x1561,x1562,x1561,x1563)
% 61.04/61.33 [160]~P9(x1601,x1602,x1601,x1603)+P1(x1601,x1602,x1603)
% 61.04/61.33 [226]~P4(x2261,x2262,x2261,x2263)+P8(x2261,x2262,x2262,x2263,x2262,x2263,x2261,x2263)
% 61.04/61.33 [163]~P9(x1633,x1634,x1631,x1632)+P9(x1631,x1632,x1633,x1634)
% 61.04/61.33 [164]~P9(x1641,x1642,x1644,x1643)+P9(x1641,x1642,x1643,x1644)
% 61.04/61.33 [165]~P10(x1653,x1654,x1651,x1652)+P10(x1651,x1652,x1653,x1654)
% 61.04/61.33 [166]~P10(x1661,x1662,x1664,x1663)+P10(x1661,x1662,x1663,x1664)
% 61.04/61.33 [167]~P4(x1673,x1674,x1671,x1672)+P4(x1671,x1672,x1673,x1674)
% 61.04/61.33 [168]~P4(x1681,x1682,x1684,x1683)+P4(x1681,x1682,x1683,x1684)
% 61.04/61.33 [169]~P3(x1692,x1691,x1693,x1694)+P3(x1691,x1692,x1693,x1694)
% 61.04/61.33 [170]~P3(x1701,x1703,x1702,x1704)+P3(x1701,x1702,x1703,x1704)
% 61.04/61.33 [171]~P3(x1711,x1712,x1714,x1713)+P3(x1711,x1712,x1713,x1714)
% 61.04/61.33 [224]~P3(x2242,x2243,x2241,x2244)+P8(x2241,x2242,x2241,x2243,x2244,x2242,x2244,x2243)
% 61.04/61.33 [187]~P2(x1874,x1871,x1872,x1873)+P10(f7(x1871,x1872,x1873,x1874),x1871,x1871,x1874)
% 61.04/61.33 [202]P4(x2021,x2022,x2023,x2024)+~P5(x2021,x2022,x2025,x2023,x2024,x2026)
% 61.04/61.33 [214]~P11(x2144,x2145,x2146,x2141,x2142,x2143)+P11(x2141,x2142,x2143,x2144,x2145,x2146)
% 61.04/61.33 [215]~P11(x2152,x2151,x2153,x2155,x2154,x2156)+P11(x2151,x2152,x2153,x2154,x2155,x2156)
% 61.04/61.33 [216]~P11(x2161,x2163,x2162,x2164,x2166,x2165)+P11(x2161,x2162,x2163,x2164,x2165,x2166)
% 61.04/61.33 [217]~P5(x2174,x2175,x2176,x2171,x2172,x2173)+P5(x2171,x2172,x2173,x2174,x2175,x2176)
% 61.04/61.33 [218]~P5(x2182,x2181,x2183,x2185,x2184,x2186)+P5(x2181,x2182,x2183,x2184,x2185,x2186)
% 61.04/61.33 [219]~P5(x2191,x2193,x2192,x2194,x2196,x2195)+P5(x2191,x2192,x2193,x2194,x2195,x2196)
% 61.04/61.33 [225]~P9(x2251,x2252,x2255,x2256)+P8(x2251,x2252,x2253,x2254,x2255,x2256,x2253,x2254)
% 61.04/61.33 [231]~P11(x2311,x2312,x2313,x2314,x2315,x2316)+P8(x2311,x2312,x2312,x2313,x2314,x2315,x2315,x2316)
% 61.04/61.33 [232]~P11(x2321,x2322,x2323,x2324,x2325,x2326)+P7(x2321,x2322,x2321,x2323,x2324,x2325,x2324,x2326)
% 61.04/61.33 [233]~P8(x2331,x2332,x2335,x2336,x2333,x2334,x2335,x2336)+P9(x2331,x2332,x2333,x2334)
% 61.04/61.33 [252]~P8(x2525,x2526,x2527,x2528,x2521,x2522,x2523,x2524)+P8(x2521,x2522,x2523,x2524,x2525,x2526,x2527,x2528)
% 61.04/61.33 [253]~P8(x2533,x2534,x2531,x2532,x2537,x2538,x2535,x2536)+P8(x2531,x2532,x2533,x2534,x2535,x2536,x2537,x2538)
% 61.04/61.33 [254]~P8(x2542,x2541,x2543,x2544,x2545,x2546,x2547,x2548)+P8(x2541,x2542,x2543,x2544,x2545,x2546,x2547,x2548)
% 61.04/61.33 [255]~P8(x2551,x2552,x2555,x2556,x2553,x2554,x2557,x2558)+P8(x2551,x2552,x2553,x2554,x2555,x2556,x2557,x2558)
% 61.04/61.33 [256]~P7(x2565,x2566,x2567,x2568,x2561,x2562,x2563,x2564)+P7(x2561,x2562,x2563,x2564,x2565,x2566,x2567,x2568)
% 61.04/61.33 [257]~P7(x2573,x2574,x2571,x2572,x2577,x2578,x2575,x2576)+P7(x2571,x2572,x2573,x2574,x2575,x2576,x2577,x2578)
% 61.04/61.33 [258]~P7(x2582,x2581,x2583,x2584,x2585,x2586,x2587,x2588)+P7(x2581,x2582,x2583,x2584,x2585,x2586,x2587,x2588)
% 61.04/61.33 [259]~P7(x2591,x2592,x2595,x2596,x2593,x2594,x2597,x2598)+P7(x2591,x2592,x2593,x2594,x2595,x2596,x2597,x2598)
% 61.04/61.33 [161]~P1(x1611,x1612,x1613)+~P4(x1611,x1612,x1611,x1613)+P6(x1611,x1612,x1613)
% 61.04/61.33 [235]P4(x2351,x2352,x2351,x2353)+~P8(x2351,x2352,x2352,x2353,x2352,x2353,x2351,x2353)+P1(x2351,x2352,x2353)
% 61.04/61.33 [176]~P10(x1761,x1762,x1762,x1763)+~P4(x1762,x1761,x1762,x1763)+P1(x1761,x1762,f3(x1761,x1763,x1762))
% 61.04/61.33 [188]~P10(x1882,x1881,x1881,x1883)+~P4(x1881,x1882,x1881,x1883)+P4(x1881,x1882,x1881,f3(x1882,x1883,x1881))
% 61.04/61.33 [155]~P1(x1553,x1554,x1551)+P1(x1551,x1552,x1553)+~P1(x1553,x1554,x1552)
% 61.04/61.33 [172]~P2(x1724,x1721,x1722,x1723)+P10(x1721,x1722,x1722,x1723)+~P1(x1724,x1721,x1723)
% 61.04/61.33 [173]~P10(x1731,x1734,x1732,x1733)+P4(x1731,x1732,x1731,x1733)+~P6(x1734,x1732,x1733)
% 61.04/61.33 [174]~P10(x1741,x1743,x1743,x1744)+P4(x1741,x1742,x1743,x1742)+~P6(x1742,x1741,x1744)
% 61.04/61.33 [181]~P4(x1811,x1814,x1812,x1814)+~P4(x1811,x1813,x1812,x1813)+P10(x1811,x1812,x1813,x1814)
% 61.04/61.33 [184]~P4(x1841,x1842,x1841,x1844)+~P4(x1841,x1842,x1841,x1843)+P2(x1841,x1842,x1843,x1844)
% 61.04/61.33 [230]~P9(x2301,x2304,x2303,x2302)+~P3(x2301,x2304,x2303,x2302)+P8(x2301,x2302,x2303,x2302,x2303,x2302,x2303,x2304)
% 61.04/61.33 [234]~P8(x2341,x2343,x2341,x2344,x2342,x2343,x2342,x2344)+P1(x2341,x2342,x2343)+P3(x2343,x2344,x2341,x2342)
% 61.04/61.33 [236]~P1(x2363,x2364,x2362)+~P8(x2363,x2361,x2363,x2362,x2364,x2361,x2364,x2362)+P3(x2361,x2362,x2363,x2364)
% 61.04/61.33 [238]P10(x2381,x2382,x2383,x2384)+~P8(x2381,x2382,x2383,x2384,x2383,x2384,x2381,x2382)+P9(x2381,x2382,x2383,x2384)
% 61.04/61.33 [177]~P10(x1771,x1774,x1772,x1773)+~P10(x1772,x1774,x1771,x1773)+P1(f4(x1771,x1772,x1773),x1773,x1772)
% 61.04/61.33 [178]~P10(x1781,x1784,x1782,x1783)+~P10(x1782,x1784,x1781,x1783)+P1(f5(x1781,x1782,x1783),x1783,x1781)
% 61.04/61.33 [189]~P10(x1891,x1894,x1892,x1893)+~P10(x1892,x1894,x1891,x1893)+P10(x1891,f4(x1891,x1892,x1893),x1893,x1892)
% 61.04/61.33 [190]~P10(x1901,x1904,x1902,x1903)+~P10(x1902,x1904,x1901,x1903)+P10(x1901,f5(x1902,x1901,x1903),x1903,x1902)
% 61.04/61.33 [191]~P10(x1911,x1913,x1913,x1912)+~P3(x1911,x1912,x1913,x1914)+P2(f8(x1911,x1912,x1913),x1911,x1912,x1913)
% 61.04/61.33 [193]~P10(x1933,x1934,x1932,x1931)+~P4(x1933,x1932,x1933,x1931)+P1(x1931,x1932,f26(x1932,x1931,x1933,x1934))
% 61.04/61.33 [194]~P10(x1943,x1944,x1941,x1942)+~P4(x1943,x1941,x1943,x1942)+P1(f26(x1941,x1942,x1943,x1944),x1943,x1944)
% 61.04/61.33 [245]~P4(x2453,x2452,x2453,x2451)+~P8(x2452,x2453,x2453,x2454,x2453,x2454,x2453,x2451)+P1(x2451,x2452,f23(x2452,x2451,x2453,x2454))
% 61.04/61.33 [246]~P10(x2463,x2464,x2462,x2461)+~P8(x2462,x2463,x2463,x2464,x2463,x2464,x2463,x2461)+P1(x2461,x2462,f27(x2462,x2461,x2463,x2464))
% 61.04/61.33 [247]~P10(x2473,x2472,x2472,x2471)+~P8(x2474,x2473,x2472,x2473,x2472,x2473,x2471,x2473)+P1(f14(x2471,x2472,x2473,x2474),x2473,x2474)
% 61.04/61.33 [248]~P10(x2483,x2482,x2482,x2481)+~P8(x2484,x2483,x2482,x2483,x2482,x2483,x2481,x2483)+P1(f14(x2481,x2482,x2483,x2484),x2481,x2482)
% 61.04/61.33 [249]~P4(x2493,x2491,x2493,x2492)+~P8(x2491,x2493,x2493,x2494,x2493,x2494,x2493,x2492)+P1(f23(x2491,x2492,x2493,x2494),x2493,x2494)
% 61.04/61.33 [250]~P10(x2503,x2504,x2501,x2502)+~P8(x2501,x2503,x2503,x2504,x2503,x2504,x2503,x2502)+P1(f27(x2501,x2502,x2503,x2504),x2503,x2504)
% 61.04/61.33 [157]~P6(x1575,x1571,x1573)+P9(x1571,x1572,x1573,x1574)+~P6(x1575,x1572,x1574)
% 61.04/61.33 [158]~P6(x1581,x1585,x1583)+P9(x1581,x1582,x1583,x1584)+~P6(x1582,x1585,x1584)
% 61.04/61.33 [185]~P3(x1855,x1851,x1852,x1853)+P3(x1851,x1852,x1853,x1854)+~P3(x1855,x1851,x1852,x1854)
% 61.04/61.33 [227]~P6(x2275,x2272,x2273)+~P2(x2274,x2271,x2272,x2273)+P8(x2271,x2272,x2271,x2273,x2274,x2272,x2274,x2275)
% 61.04/61.33 [229]~P2(x2295,x2291,x2293,x2294)+P8(x2291,x2292,x2291,x2293,x2294,x2291,x2294,x2293)+~P10(x2295,x2291,x2291,x2292)
% 61.04/61.33 [242]~P8(x2422,x2423,x2422,x2424,x2425,x2422,x2425,x2424)+P10(x2421,x2422,x2422,x2423)+~P2(x2421,x2422,x2424,x2425)
% 61.04/61.33 [197]~P1(x1972,x1974,x1975)+~P10(x1971,x1973,x1973,x1972)+P1(f12(x1971,x1972,x1973,x1974,x1975),x1974,x1975)
% 61.04/61.33 [198]~P1(x1982,x1984,x1985)+~P10(x1981,x1983,x1983,x1982)+P10(f12(x1981,x1982,x1983,x1984,x1985),x1981,x1984,x1985)
% 61.04/61.33 [199]~P10(x1993,x1994,x1994,x1991)+~P4(x1991,x1992,x1991,x1995)+P4(x1991,x1992,x1991,f30(x1993,x1994,x1992,x1995,x1991))
% 61.04/61.33 [200]~P10(x2003,x2001,x2001,x2005)+~P4(x2005,x2002,x2005,x2004)+P4(x2001,x2002,x2001,f30(x2003,x2001,x2002,x2004,x2005))
% 61.04/61.33 [201]~P10(x2011,x2012,x2012,x2015)+~P4(x2015,x2013,x2015,x2014)+P9(f30(x2011,x2012,x2013,x2014,x2015),x2013,x2011,x2012)
% 61.04/61.33 [244]~P8(x2441,x2443,x2442,x2443,x2441,x2444,x2442,x2445)+P1(x2441,x2442,x2443)+P3(x2444,x2442,x2443,f29(x2441,x2442,x2443,x2444))
% 61.04/61.33 [260]~P8(x2601,x2603,x2602,x2603,x2601,x2604,x2602,x2605)+P1(x2601,x2602,x2603)+P8(x2601,x2603,x2602,x2603,x2601,f29(x2601,x2602,x2603,x2604),x2602,f29(x2601,x2602,x2603,x2604))
% 61.04/61.33 [179]~P9(x1791,x1792,x1795,x1796)+P9(x1791,x1792,x1793,x1794)+~P9(x1795,x1796,x1793,x1794)
% 61.04/61.33 [180]~P10(x1801,x1802,x1805,x1806)+P9(x1801,x1802,x1803,x1804)+~P10(x1805,x1806,x1803,x1804)
% 61.04/61.33 [182]~P10(x1825,x1826,x1823,x1824)+P10(x1821,x1822,x1823,x1824)+~P9(x1821,x1822,x1825,x1826)
% 61.04/61.33 [183]~P4(x1831,x1832,x1835,x1836)+P4(x1831,x1832,x1833,x1834)+~P4(x1835,x1836,x1833,x1834)
% 61.04/61.33 [220]~P4(x2201,x2202,x2204,x2205)+~P11(x2201,x2202,x2203,x2204,x2205,x2206)+P5(x2201,x2202,x2203,x2204,x2205,x2206)
% 61.04/61.33 [223]~P6(x2234,x2235,x2236)+~P6(x2231,x2232,x2233)+P7(x2231,x2232,x2232,x2233,x2234,x2235,x2235,x2236)
% 61.04/61.33 [203]~P6(x2036,x2033,x2034)+~P6(x2035,x2031,x2032)+P6(f28(x2031,x2032,x2033,x2034,x2035,x2036),x2031,x2034)
% 61.04/61.33 [204]~P6(x2046,x2043,x2044)+~P6(x2045,x2041,x2042)+P9(f28(x2041,x2042,x2043,x2044,x2045,x2046),x2046,x2041,x2043)
% 61.04/61.33 [205]~P6(x2056,x2053,x2054)+~P6(x2055,x2051,x2052)+P9(f28(x2051,x2052,x2053,x2054,x2055,x2056),x2055,x2052,x2054)
% 61.04/61.33 [240]~P8(x2401,x2402,x2403,x2404,x2405,x2406,x2407,x2408)+P9(x2401,x2402,x2403,x2404)+~P9(x2405,x2406,x2407,x2408)
% 61.04/61.33 [241]~P8(x2411,x2412,x2413,x2414,x2415,x2416,x2417,x2418)+P10(x2411,x2412,x2413,x2414)+~P10(x2415,x2416,x2417,x2418)
% 61.04/61.33 [243]~P7(x2431,x2432,x2433,x2434,x2435,x2436,x2437,x2438)+P4(x2431,x2432,x2433,x2434)+~P4(x2435,x2436,x2437,x2438)
% 61.04/61.33 [221]~P11(x2211,x2212,x2213,x2217,x2218,x2219)+P11(x2211,x2212,x2213,x2214,x2215,x2216)+~P11(x2217,x2218,x2219,x2214,x2215,x2216)
% 61.04/61.33 [222]~P5(x2221,x2222,x2223,x2227,x2228,x2229)+P5(x2221,x2222,x2223,x2224,x2225,x2226)+~P5(x2227,x2228,x2229,x2224,x2225,x2226)
% 61.04/61.33 [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)
% 61.04/61.33 [263]~P7(x2631,x2632,x2633,x2634,x2639,x26310,x26311,x26312)+P7(x2631,x2632,x2633,x2634,x2635,x2636,x2637,x2638)+~P7(x2639,x26310,x26311,x26312,x2635,x2636,x2637,x2638)
% 61.04/61.33 [195]~P4(x1952,x1951,x1954,x1951)+~P3(x1952,x1954,x1951,x1953)+P10(x1951,x1952,x1952,x1953)+~P4(x1952,x1953,x1954,x1953)
% 61.04/61.33 [162]~P1(x1621,x1622,x1623)+~P9(x1624,x1621,x1625,x1623)+P6(x1621,x1622,x1623)+~P6(x1624,x1622,x1625)
% 61.04/61.33 [175]~P9(x1754,x1753,x1755,x1752)+~P9(x1754,x1752,x1755,x1753)+P6(x1751,x1752,x1753)+~P6(x1751,x1754,x1755)
% 61.04/61.33 [196]~P4(x1965,x1961,x1965,x1963)+~P4(x1965,x1961,x1965,x1962)+P3(x1961,x1962,x1963,x1964)+~P4(x1965,x1961,x1965,x1964)
% 61.04/61.33 [228]~P1(x2281,x2284,x2285)+~P1(x2281,x2282,x2283)+~P9(x2282,x2284,x2283,x2285)+P7(x2281,x2282,x2282,x2283,x2281,x2284,x2284,x2285)
% 61.04/61.33 [239]~P1(x2391,x2392,x2393)+~P8(x2395,x2392,x2395,x2393,x2394,x2392,x2394,x2391)+P6(x2391,x2392,x2393)+~P2(x2394,x2395,x2392,x2393)
% 61.04/61.33 [186]~P10(x1863,x1861,x1863,x1865)+~P10(x1861,x1862,x1861,x1863)+~P6(x1864,x1862,x1865)+P6(f6(x1861,x1862,x1863),x1861,x1863)
% 61.04/61.33 [192]~P3(x1921,x1922,x1923,x1925)+~P9(x1921,x1922,x1923,x1925)+~P6(x1924,x1921,x1922)+P2(f9(x1921,x1922,x1923),x1921,x1922,x1923)
% 61.04/61.33 [261]~P8(x2611,x2613,x2612,x2613,x2614,x2616,x2615,x2616)+~P8(x2611,x2612,x2612,x2613,x2614,x2615,x2615,x2616)+P1(x2611,x2612,x2613)+P11(x2611,x2612,x2613,x2614,x2615,x2616)
% 61.04/61.33 [251]~P3(x2511,x2512,x2515,x2514)+~P3(x2511,x2512,x2515,x2513)+~P8(x2515,x2511,x2515,x2512,x2516,x2513,x2516,x2514)+P4(x2511,x2512,x2513,x2514)+~P3(x2511,x2512,x2515,x2516)
% 61.04/61.33 [206]~P1(x2062,x2063,x2064)+~P1(x2061,x2064,x2066)+~P1(x2061,x2063,x2065)+~P9(x2063,x2064,x2065,x2066)+P1(x2061,x2062,f13(x2063,x2064,x2065,x2066,x2061,x2062))
% 61.04/61.33 [207]~P1(x2076,x2071,x2072)+~P1(x2075,x2072,x2074)+~P1(x2075,x2071,x2073)+~P9(x2071,x2072,x2073,x2074)+P1(f13(x2071,x2072,x2073,x2074,x2075,x2076),x2073,x2074)
% 61.04/61.33 [208]~P1(x2083,x2084,x2085)+~P6(x2086,x2081,x2082)+~P9(x2081,x2083,x2085,x2086)+~P9(x2081,x2083,x2082,x2084)+P1(f31(x2081,x2082,x2083,x2084,x2085,x2086),x2086,x2085)
% 61.04/61.33 [209]~P1(x2093,x2094,x2095)+~P6(x2096,x2091,x2092)+~P9(x2091,x2093,x2095,x2096)+~P9(x2091,x2093,x2092,x2094)+P1(f31(x2091,x2092,x2093,x2094,x2095,x2096),x2091,x2094)
% 61.04/61.33 [210]~P4(x2102,x2103,x2102,x2104)+~P4(x2101,x2103,x2101,x2106)+~P2(x2101,x2103,x2104,x2105)+E(x2101,x2102)+P1(f10(x2103,x2104,x2105,x2106,x2101,x2102),x2103,x2105)
% 61.04/61.33 [211]~P4(x2112,x2113,x2112,x2114)+~P4(x2111,x2113,x2111,x2116)+~P2(x2111,x2113,x2114,x2115)+E(x2111,x2112)+P1(f11(x2113,x2114,x2115,x2116,x2111,x2112),x2114,x2116)
% 61.04/61.33 [212]~P4(x2122,x2123,x2122,x2124)+~P4(x2121,x2123,x2121,x2126)+~P2(x2121,x2123,x2124,x2125)+E(x2121,x2122)+P4(f10(x2123,x2124,x2125,x2126,x2121,x2122),x2122,x2122,x2123)
% 61.04/61.33 [213]~P4(x2132,x2133,x2132,x2134)+~P4(x2131,x2133,x2131,x2136)+~P2(x2131,x2133,x2134,x2135)+E(x2131,x2132)+P4(f11(x2133,x2134,x2135,x2136,x2131,x2132),x2132,x2132,x2133)
% 61.04/61.33 [159]~P1(x1593,x1591,x1594)+~P1(x1595,x1591,x1594)+~P6(x1596,x1595,x1593)+~P6(x1597,x1591,x1594)+P6(f25(x1591,x1592),x1591,x1592)
% 61.04/61.33 %EqnAxiom
% 61.04/61.33 [1]E(x11,x11)
% 61.04/61.33 [2]E(x22,x21)+~E(x21,x22)
% 61.04/61.33 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 61.04/61.33 [4]~E(x41,x42)+E(f25(x41,x43),f25(x42,x43))
% 61.04/61.33 [5]~E(x51,x52)+E(f25(x53,x51),f25(x53,x52))
% 61.04/61.33 [6]~E(x61,x62)+E(f3(x61,x63,x64),f3(x62,x63,x64))
% 61.04/61.33 [7]~E(x71,x72)+E(f3(x73,x71,x74),f3(x73,x72,x74))
% 61.04/61.33 [8]~E(x81,x82)+E(f3(x83,x84,x81),f3(x83,x84,x82))
% 61.04/61.33 [9]~E(x91,x92)+E(f4(x91,x93,x94),f4(x92,x93,x94))
% 61.04/61.33 [10]~E(x101,x102)+E(f4(x103,x101,x104),f4(x103,x102,x104))
% 61.04/61.33 [11]~E(x111,x112)+E(f4(x113,x114,x111),f4(x113,x114,x112))
% 61.04/61.33 [12]~E(x121,x122)+E(f5(x121,x123,x124),f5(x122,x123,x124))
% 61.04/61.33 [13]~E(x131,x132)+E(f5(x133,x131,x134),f5(x133,x132,x134))
% 61.04/61.33 [14]~E(x141,x142)+E(f5(x143,x144,x141),f5(x143,x144,x142))
% 61.04/61.33 [15]~E(x151,x152)+E(f6(x151,x153,x154),f6(x152,x153,x154))
% 61.04/61.33 [16]~E(x161,x162)+E(f6(x163,x161,x164),f6(x163,x162,x164))
% 61.04/61.33 [17]~E(x171,x172)+E(f6(x173,x174,x171),f6(x173,x174,x172))
% 61.04/61.33 [18]~E(x181,x182)+E(f7(x181,x183,x184,x185),f7(x182,x183,x184,x185))
% 61.04/61.33 [19]~E(x191,x192)+E(f7(x193,x191,x194,x195),f7(x193,x192,x194,x195))
% 61.04/61.33 [20]~E(x201,x202)+E(f7(x203,x204,x201,x205),f7(x203,x204,x202,x205))
% 61.04/61.33 [21]~E(x211,x212)+E(f7(x213,x214,x215,x211),f7(x213,x214,x215,x212))
% 61.04/61.33 [22]~E(x221,x222)+E(f29(x221,x223,x224,x225),f29(x222,x223,x224,x225))
% 61.04/61.33 [23]~E(x231,x232)+E(f29(x233,x231,x234,x235),f29(x233,x232,x234,x235))
% 61.04/61.33 [24]~E(x241,x242)+E(f29(x243,x244,x241,x245),f29(x243,x244,x242,x245))
% 61.04/61.33 [25]~E(x251,x252)+E(f29(x253,x254,x255,x251),f29(x253,x254,x255,x252))
% 61.04/61.33 [26]~E(x261,x262)+E(f23(x261,x263,x264,x265),f23(x262,x263,x264,x265))
% 61.04/61.33 [27]~E(x271,x272)+E(f23(x273,x271,x274,x275),f23(x273,x272,x274,x275))
% 61.04/61.33 [28]~E(x281,x282)+E(f23(x283,x284,x281,x285),f23(x283,x284,x282,x285))
% 61.04/61.33 [29]~E(x291,x292)+E(f23(x293,x294,x295,x291),f23(x293,x294,x295,x292))
% 61.04/61.33 [30]~E(x301,x302)+E(f27(x301,x303,x304,x305),f27(x302,x303,x304,x305))
% 61.04/61.33 [31]~E(x311,x312)+E(f27(x313,x311,x314,x315),f27(x313,x312,x314,x315))
% 61.04/61.33 [32]~E(x321,x322)+E(f27(x323,x324,x321,x325),f27(x323,x324,x322,x325))
% 61.04/61.33 [33]~E(x331,x332)+E(f27(x333,x334,x335,x331),f27(x333,x334,x335,x332))
% 61.04/61.33 [34]~E(x341,x342)+E(f8(x341,x343,x344),f8(x342,x343,x344))
% 61.04/61.33 [35]~E(x351,x352)+E(f8(x353,x351,x354),f8(x353,x352,x354))
% 61.04/61.33 [36]~E(x361,x362)+E(f8(x363,x364,x361),f8(x363,x364,x362))
% 61.04/61.33 [37]~E(x371,x372)+E(f9(x371,x373,x374),f9(x372,x373,x374))
% 61.04/61.33 [38]~E(x381,x382)+E(f9(x383,x381,x384),f9(x383,x382,x384))
% 61.04/61.33 [39]~E(x391,x392)+E(f9(x393,x394,x391),f9(x393,x394,x392))
% 61.04/61.33 [40]~E(x401,x402)+E(f26(x401,x403,x404,x405),f26(x402,x403,x404,x405))
% 61.04/61.33 [41]~E(x411,x412)+E(f26(x413,x411,x414,x415),f26(x413,x412,x414,x415))
% 61.04/61.33 [42]~E(x421,x422)+E(f26(x423,x424,x421,x425),f26(x423,x424,x422,x425))
% 61.04/61.33 [43]~E(x431,x432)+E(f26(x433,x434,x435,x431),f26(x433,x434,x435,x432))
% 61.04/61.33 [44]~E(x441,x442)+E(f14(x441,x443,x444,x445),f14(x442,x443,x444,x445))
% 61.04/61.33 [45]~E(x451,x452)+E(f14(x453,x451,x454,x455),f14(x453,x452,x454,x455))
% 61.04/61.33 [46]~E(x461,x462)+E(f14(x463,x464,x461,x465),f14(x463,x464,x462,x465))
% 61.04/61.33 [47]~E(x471,x472)+E(f14(x473,x474,x475,x471),f14(x473,x474,x475,x472))
% 61.04/61.33 [48]~E(x481,x482)+E(f12(x481,x483,x484,x485,x486),f12(x482,x483,x484,x485,x486))
% 61.04/61.33 [49]~E(x491,x492)+E(f12(x493,x491,x494,x495,x496),f12(x493,x492,x494,x495,x496))
% 61.04/61.33 [50]~E(x501,x502)+E(f12(x503,x504,x501,x505,x506),f12(x503,x504,x502,x505,x506))
% 61.04/61.33 [51]~E(x511,x512)+E(f12(x513,x514,x515,x511,x516),f12(x513,x514,x515,x512,x516))
% 61.04/61.33 [52]~E(x521,x522)+E(f12(x523,x524,x525,x526,x521),f12(x523,x524,x525,x526,x522))
% 61.04/61.33 [53]~E(x531,x532)+E(f11(x531,x533,x534,x535,x536,x537),f11(x532,x533,x534,x535,x536,x537))
% 61.04/61.33 [54]~E(x541,x542)+E(f11(x543,x541,x544,x545,x546,x547),f11(x543,x542,x544,x545,x546,x547))
% 61.04/61.33 [55]~E(x551,x552)+E(f11(x553,x554,x551,x555,x556,x557),f11(x553,x554,x552,x555,x556,x557))
% 61.04/61.33 [56]~E(x561,x562)+E(f11(x563,x564,x565,x561,x566,x567),f11(x563,x564,x565,x562,x566,x567))
% 61.04/61.33 [57]~E(x571,x572)+E(f11(x573,x574,x575,x576,x571,x577),f11(x573,x574,x575,x576,x572,x577))
% 61.04/61.33 [58]~E(x581,x582)+E(f11(x583,x584,x585,x586,x587,x581),f11(x583,x584,x585,x586,x587,x582))
% 61.04/61.33 [59]~E(x591,x592)+E(f30(x591,x593,x594,x595,x596),f30(x592,x593,x594,x595,x596))
% 61.04/61.33 [60]~E(x601,x602)+E(f30(x603,x601,x604,x605,x606),f30(x603,x602,x604,x605,x606))
% 61.04/61.33 [61]~E(x611,x612)+E(f30(x613,x614,x611,x615,x616),f30(x613,x614,x612,x615,x616))
% 61.04/61.33 [62]~E(x621,x622)+E(f30(x623,x624,x625,x621,x626),f30(x623,x624,x625,x622,x626))
% 61.04/61.33 [63]~E(x631,x632)+E(f30(x633,x634,x635,x636,x631),f30(x633,x634,x635,x636,x632))
% 61.04/61.33 [64]~E(x641,x642)+E(f10(x641,x643,x644,x645,x646,x647),f10(x642,x643,x644,x645,x646,x647))
% 61.04/61.33 [65]~E(x651,x652)+E(f10(x653,x651,x654,x655,x656,x657),f10(x653,x652,x654,x655,x656,x657))
% 61.04/61.33 [66]~E(x661,x662)+E(f10(x663,x664,x661,x665,x666,x667),f10(x663,x664,x662,x665,x666,x667))
% 61.04/61.33 [67]~E(x671,x672)+E(f10(x673,x674,x675,x671,x676,x677),f10(x673,x674,x675,x672,x676,x677))
% 61.04/61.33 [68]~E(x681,x682)+E(f10(x683,x684,x685,x686,x681,x687),f10(x683,x684,x685,x686,x682,x687))
% 61.04/61.33 [69]~E(x691,x692)+E(f10(x693,x694,x695,x696,x697,x691),f10(x693,x694,x695,x696,x697,x692))
% 61.04/61.33 [70]~E(x701,x702)+E(f31(x701,x703,x704,x705,x706,x707),f31(x702,x703,x704,x705,x706,x707))
% 61.04/61.33 [71]~E(x711,x712)+E(f31(x713,x711,x714,x715,x716,x717),f31(x713,x712,x714,x715,x716,x717))
% 61.04/61.33 [72]~E(x721,x722)+E(f31(x723,x724,x721,x725,x726,x727),f31(x723,x724,x722,x725,x726,x727))
% 61.04/61.33 [73]~E(x731,x732)+E(f31(x733,x734,x735,x731,x736,x737),f31(x733,x734,x735,x732,x736,x737))
% 61.04/61.33 [74]~E(x741,x742)+E(f31(x743,x744,x745,x746,x741,x747),f31(x743,x744,x745,x746,x742,x747))
% 61.04/61.33 [75]~E(x751,x752)+E(f31(x753,x754,x755,x756,x757,x751),f31(x753,x754,x755,x756,x757,x752))
% 61.04/61.33 [76]~E(x761,x762)+E(f28(x761,x763,x764,x765,x766,x767),f28(x762,x763,x764,x765,x766,x767))
% 61.04/61.33 [77]~E(x771,x772)+E(f28(x773,x771,x774,x775,x776,x777),f28(x773,x772,x774,x775,x776,x777))
% 61.04/61.33 [78]~E(x781,x782)+E(f28(x783,x784,x781,x785,x786,x787),f28(x783,x784,x782,x785,x786,x787))
% 61.04/61.33 [79]~E(x791,x792)+E(f28(x793,x794,x795,x791,x796,x797),f28(x793,x794,x795,x792,x796,x797))
% 61.04/61.33 [80]~E(x801,x802)+E(f28(x803,x804,x805,x806,x801,x807),f28(x803,x804,x805,x806,x802,x807))
% 61.04/61.33 [81]~E(x811,x812)+E(f28(x813,x814,x815,x816,x817,x811),f28(x813,x814,x815,x816,x817,x812))
% 61.04/61.33 [82]~E(x821,x822)+E(f13(x821,x823,x824,x825,x826,x827),f13(x822,x823,x824,x825,x826,x827))
% 61.04/61.33 [83]~E(x831,x832)+E(f13(x833,x831,x834,x835,x836,x837),f13(x833,x832,x834,x835,x836,x837))
% 61.04/61.33 [84]~E(x841,x842)+E(f13(x843,x844,x841,x845,x846,x847),f13(x843,x844,x842,x845,x846,x847))
% 61.04/61.33 [85]~E(x851,x852)+E(f13(x853,x854,x855,x851,x856,x857),f13(x853,x854,x855,x852,x856,x857))
% 61.04/61.33 [86]~E(x861,x862)+E(f13(x863,x864,x865,x866,x861,x867),f13(x863,x864,x865,x866,x862,x867))
% 61.04/61.33 [87]~E(x871,x872)+E(f13(x873,x874,x875,x876,x877,x871),f13(x873,x874,x875,x876,x877,x872))
% 61.04/61.33 [88]P1(x882,x883,x884)+~E(x881,x882)+~P1(x881,x883,x884)
% 61.04/61.33 [89]P1(x893,x892,x894)+~E(x891,x892)+~P1(x893,x891,x894)
% 61.04/61.33 [90]P1(x903,x904,x902)+~E(x901,x902)+~P1(x903,x904,x901)
% 61.04/61.33 [91]P7(x912,x913,x914,x915,x916,x917,x918,x919)+~E(x911,x912)+~P7(x911,x913,x914,x915,x916,x917,x918,x919)
% 61.04/61.33 [92]P7(x923,x922,x924,x925,x926,x927,x928,x929)+~E(x921,x922)+~P7(x923,x921,x924,x925,x926,x927,x928,x929)
% 61.04/61.33 [93]P7(x933,x934,x932,x935,x936,x937,x938,x939)+~E(x931,x932)+~P7(x933,x934,x931,x935,x936,x937,x938,x939)
% 61.04/61.33 [94]P7(x943,x944,x945,x942,x946,x947,x948,x949)+~E(x941,x942)+~P7(x943,x944,x945,x941,x946,x947,x948,x949)
% 61.04/61.33 [95]P7(x953,x954,x955,x956,x952,x957,x958,x959)+~E(x951,x952)+~P7(x953,x954,x955,x956,x951,x957,x958,x959)
% 61.04/61.33 [96]P7(x963,x964,x965,x966,x967,x962,x968,x969)+~E(x961,x962)+~P7(x963,x964,x965,x966,x967,x961,x968,x969)
% 61.04/61.33 [97]P7(x973,x974,x975,x976,x977,x978,x972,x979)+~E(x971,x972)+~P7(x973,x974,x975,x976,x977,x978,x971,x979)
% 61.04/61.33 [98]P7(x983,x984,x985,x986,x987,x988,x989,x982)+~E(x981,x982)+~P7(x983,x984,x985,x986,x987,x988,x989,x981)
% 61.04/61.33 [99]P3(x992,x993,x994,x995)+~E(x991,x992)+~P3(x991,x993,x994,x995)
% 61.04/61.33 [100]P3(x1003,x1002,x1004,x1005)+~E(x1001,x1002)+~P3(x1003,x1001,x1004,x1005)
% 61.04/61.33 [101]P3(x1013,x1014,x1012,x1015)+~E(x1011,x1012)+~P3(x1013,x1014,x1011,x1015)
% 61.04/61.33 [102]P3(x1023,x1024,x1025,x1022)+~E(x1021,x1022)+~P3(x1023,x1024,x1025,x1021)
% 61.04/61.33 [103]P4(x1032,x1033,x1034,x1035)+~E(x1031,x1032)+~P4(x1031,x1033,x1034,x1035)
% 61.04/61.33 [104]P4(x1043,x1042,x1044,x1045)+~E(x1041,x1042)+~P4(x1043,x1041,x1044,x1045)
% 61.04/61.33 [105]P4(x1053,x1054,x1052,x1055)+~E(x1051,x1052)+~P4(x1053,x1054,x1051,x1055)
% 61.04/61.33 [106]P4(x1063,x1064,x1065,x1062)+~E(x1061,x1062)+~P4(x1063,x1064,x1065,x1061)
% 61.04/61.33 [107]P2(x1072,x1073,x1074,x1075)+~E(x1071,x1072)+~P2(x1071,x1073,x1074,x1075)
% 61.04/61.33 [108]P2(x1083,x1082,x1084,x1085)+~E(x1081,x1082)+~P2(x1083,x1081,x1084,x1085)
% 61.04/61.33 [109]P2(x1093,x1094,x1092,x1095)+~E(x1091,x1092)+~P2(x1093,x1094,x1091,x1095)
% 61.04/61.33 [110]P2(x1103,x1104,x1105,x1102)+~E(x1101,x1102)+~P2(x1103,x1104,x1105,x1101)
% 61.04/61.33 [111]P11(x1112,x1113,x1114,x1115,x1116,x1117)+~E(x1111,x1112)+~P11(x1111,x1113,x1114,x1115,x1116,x1117)
% 61.04/61.33 [112]P11(x1123,x1122,x1124,x1125,x1126,x1127)+~E(x1121,x1122)+~P11(x1123,x1121,x1124,x1125,x1126,x1127)
% 61.04/61.33 [113]P11(x1133,x1134,x1132,x1135,x1136,x1137)+~E(x1131,x1132)+~P11(x1133,x1134,x1131,x1135,x1136,x1137)
% 61.04/61.33 [114]P11(x1143,x1144,x1145,x1142,x1146,x1147)+~E(x1141,x1142)+~P11(x1143,x1144,x1145,x1141,x1146,x1147)
% 61.04/61.33 [115]P11(x1153,x1154,x1155,x1156,x1152,x1157)+~E(x1151,x1152)+~P11(x1153,x1154,x1155,x1156,x1151,x1157)
% 61.04/61.33 [116]P11(x1163,x1164,x1165,x1166,x1167,x1162)+~E(x1161,x1162)+~P11(x1163,x1164,x1165,x1166,x1167,x1161)
% 61.04/61.33 [117]P6(x1172,x1173,x1174)+~E(x1171,x1172)+~P6(x1171,x1173,x1174)
% 61.04/61.33 [118]P6(x1183,x1182,x1184)+~E(x1181,x1182)+~P6(x1183,x1181,x1184)
% 61.04/61.33 [119]P6(x1193,x1194,x1192)+~E(x1191,x1192)+~P6(x1193,x1194,x1191)
% 61.04/61.33 [120]P8(x1202,x1203,x1204,x1205,x1206,x1207,x1208,x1209)+~E(x1201,x1202)+~P8(x1201,x1203,x1204,x1205,x1206,x1207,x1208,x1209)
% 61.04/61.33 [121]P8(x1213,x1212,x1214,x1215,x1216,x1217,x1218,x1219)+~E(x1211,x1212)+~P8(x1213,x1211,x1214,x1215,x1216,x1217,x1218,x1219)
% 61.04/61.33 [122]P8(x1223,x1224,x1222,x1225,x1226,x1227,x1228,x1229)+~E(x1221,x1222)+~P8(x1223,x1224,x1221,x1225,x1226,x1227,x1228,x1229)
% 61.04/61.33 [123]P8(x1233,x1234,x1235,x1232,x1236,x1237,x1238,x1239)+~E(x1231,x1232)+~P8(x1233,x1234,x1235,x1231,x1236,x1237,x1238,x1239)
% 61.04/61.33 [124]P8(x1243,x1244,x1245,x1246,x1242,x1247,x1248,x1249)+~E(x1241,x1242)+~P8(x1243,x1244,x1245,x1246,x1241,x1247,x1248,x1249)
% 61.04/61.33 [125]P8(x1253,x1254,x1255,x1256,x1257,x1252,x1258,x1259)+~E(x1251,x1252)+~P8(x1253,x1254,x1255,x1256,x1257,x1251,x1258,x1259)
% 61.04/61.33 [126]P8(x1263,x1264,x1265,x1266,x1267,x1268,x1262,x1269)+~E(x1261,x1262)+~P8(x1263,x1264,x1265,x1266,x1267,x1268,x1261,x1269)
% 61.04/61.33 [127]P8(x1273,x1274,x1275,x1276,x1277,x1278,x1279,x1272)+~E(x1271,x1272)+~P8(x1273,x1274,x1275,x1276,x1277,x1278,x1279,x1271)
% 61.04/61.33 [128]P5(x1282,x1283,x1284,x1285,x1286,x1287)+~E(x1281,x1282)+~P5(x1281,x1283,x1284,x1285,x1286,x1287)
% 61.04/61.33 [129]P5(x1293,x1292,x1294,x1295,x1296,x1297)+~E(x1291,x1292)+~P5(x1293,x1291,x1294,x1295,x1296,x1297)
% 61.04/61.33 [130]P5(x1303,x1304,x1302,x1305,x1306,x1307)+~E(x1301,x1302)+~P5(x1303,x1304,x1301,x1305,x1306,x1307)
% 61.04/61.33 [131]P5(x1313,x1314,x1315,x1312,x1316,x1317)+~E(x1311,x1312)+~P5(x1313,x1314,x1315,x1311,x1316,x1317)
% 61.04/61.33 [132]P5(x1323,x1324,x1325,x1326,x1322,x1327)+~E(x1321,x1322)+~P5(x1323,x1324,x1325,x1326,x1321,x1327)
% 61.04/61.33 [133]P5(x1333,x1334,x1335,x1336,x1337,x1332)+~E(x1331,x1332)+~P5(x1333,x1334,x1335,x1336,x1337,x1331)
% 61.04/61.33 [134]P10(x1342,x1343,x1344,x1345)+~E(x1341,x1342)+~P10(x1341,x1343,x1344,x1345)
% 61.04/61.33 [135]P10(x1353,x1352,x1354,x1355)+~E(x1351,x1352)+~P10(x1353,x1351,x1354,x1355)
% 61.04/61.33 [136]P10(x1363,x1364,x1362,x1365)+~E(x1361,x1362)+~P10(x1363,x1364,x1361,x1365)
% 61.04/61.33 [137]P10(x1373,x1374,x1375,x1372)+~E(x1371,x1372)+~P10(x1373,x1374,x1375,x1371)
% 61.04/61.33 [138]P9(x1382,x1383,x1384,x1385)+~E(x1381,x1382)+~P9(x1381,x1383,x1384,x1385)
% 61.04/61.33 [139]P9(x1393,x1392,x1394,x1395)+~E(x1391,x1392)+~P9(x1393,x1391,x1394,x1395)
% 61.04/61.33 [140]P9(x1403,x1404,x1402,x1405)+~E(x1401,x1402)+~P9(x1403,x1404,x1401,x1405)
% 61.04/61.34 [141]P9(x1413,x1414,x1415,x1412)+~E(x1411,x1412)+~P9(x1413,x1414,x1415,x1411)
% 61.04/61.34
% 61.04/61.34 %-------------------------------------------
% 61.18/61.35 cnf(264,plain,
% 61.18/61.35 (~P3(a17,a1,a20,a2)),
% 61.18/61.35 inference(scs_inference,[],[150,169])).
% 61.18/61.35 cnf(266,plain,
% 61.18/61.35 (~P3(a1,a20,a17,a2)),
% 61.18/61.35 inference(scs_inference,[],[150,169,170])).
% 61.18/61.35 cnf(268,plain,
% 61.18/61.35 (~P3(a1,a17,a2,a20)),
% 61.18/61.35 inference(scs_inference,[],[150,169,170,171])).
% 61.18/61.35 cnf(284,plain,
% 61.18/61.35 (~P3(a20,a1,a17,a2)),
% 61.18/61.35 inference(scs_inference,[],[266,169])).
% 61.18/61.35 cnf(286,plain,
% 61.18/61.35 (~P3(a17,a20,a1,a2)),
% 61.18/61.35 inference(scs_inference,[],[264,266,169,170])).
% 61.18/61.35 cnf(288,plain,
% 61.18/61.35 (~P3(a17,a1,a2,a20)),
% 61.18/61.35 inference(scs_inference,[],[264,266,169,170,171])).
% 61.18/61.35 cnf(292,plain,
% 61.18/61.35 (P2(x2921,a16,a20,a22)+~E(a19,x2921)),
% 61.18/61.35 inference(scs_inference,[],[143,147,264,266,169,170,171,155,107])).
% 61.18/61.35 cnf(303,plain,
% 61.18/61.35 (~P3(a20,a17,a1,a2)),
% 61.18/61.35 inference(scs_inference,[],[286,169])).
% 61.18/61.35 cnf(305,plain,
% 61.18/61.35 (~P3(a1,a2,a17,a20)),
% 61.18/61.35 inference(scs_inference,[],[268,286,169,170])).
% 61.18/61.35 cnf(307,plain,
% 61.18/61.35 (~P3(a20,a1,a2,a17)),
% 61.18/61.35 inference(scs_inference,[],[268,284,286,169,170,171])).
% 61.18/61.35 cnf(325,plain,
% 61.18/61.35 (~P3(a17,a2,a1,a20)),
% 61.18/61.35 inference(scs_inference,[],[288,305,169,170])).
% 61.18/61.35 cnf(327,plain,
% 61.18/61.35 (~P3(a20,a17,a2,a1)),
% 61.18/61.35 inference(scs_inference,[],[288,303,305,169,170,171])).
% 61.18/61.35 cnf(329,plain,
% 61.18/61.35 (P1(a16,a16,a18)),
% 61.18/61.35 inference(scs_inference,[],[145,288,303,305,169,170,171,155])).
% 61.18/61.35 cnf(344,plain,
% 61.18/61.35 (~P3(a1,a20,a2,a17)),
% 61.18/61.35 inference(scs_inference,[],[307,169])).
% 61.18/61.35 cnf(346,plain,
% 61.18/61.35 (~P3(a20,a2,a1,a17)),
% 61.18/61.35 inference(scs_inference,[],[307,169,170])).
% 61.18/61.35 cnf(365,plain,
% 61.18/61.35 (~P3(a2,a17,a1,a20)),
% 61.18/61.35 inference(scs_inference,[],[325,169])).
% 61.18/61.35 cnf(367,plain,
% 61.18/61.35 (~P3(a20,a2,a17,a1)),
% 61.18/61.35 inference(scs_inference,[],[325,327,169,170])).
% 61.18/61.35 cnf(369,plain,
% 61.18/61.35 (~P3(a17,a2,a20,a1)),
% 61.18/61.35 inference(scs_inference,[],[325,327,169,170,171])).
% 61.18/61.35 cnf(387,plain,
% 61.18/61.35 (~P3(a2,a20,a1,a17)),
% 61.18/61.35 inference(scs_inference,[],[346,169])).
% 61.18/61.35 cnf(389,plain,
% 61.18/61.35 (~P3(a1,a2,a20,a17)),
% 61.18/61.35 inference(scs_inference,[],[344,346,169,170])).
% 61.18/61.35 cnf(391,plain,
% 61.18/61.35 (~P3(a2,a17,a20,a1)),
% 61.18/61.35 inference(scs_inference,[],[344,346,365,169,170,171])).
% 61.18/61.35 cnf(408,plain,
% 61.18/61.35 (~P3(a2,a20,a17,a1)),
% 61.18/61.35 inference(scs_inference,[],[367,169])).
% 61.18/61.35 cnf(410,plain,
% 61.18/61.35 (~P3(a17,a20,a2,a1)),
% 61.18/61.35 inference(scs_inference,[],[367,369,169,170])).
% 61.18/61.35 cnf(752,plain,
% 61.18/61.35 (P4(x7521,x7522,x7521,x7523)+~P6(x7521,x7523,x7522)),
% 61.18/61.35 inference(scs_inference,[],[154,156])).
% 61.18/61.35 cnf(754,plain,
% 61.18/61.35 (~P8(a2,a20,a2,a24,a21,a20,a21,x7541)+P4(x7541,a24,x7541,a20)+~P1(x7541,a20,a24)),
% 61.18/61.35 inference(scs_inference,[],[148,752,239])).
% 61.18/61.35 cnf(759,plain,
% 61.18/61.35 (P10(x7591,x7592,x7593,x7594)+~P10(x7594,x7593,x7591,x7592)),
% 61.18/61.35 inference(scs_inference,[],[165,166])).
% 61.18/61.35 cnf(1645,plain,
% 61.18/61.35 (P10(f7(a16,a20,a22,x16451),a16,a16,x16451)+~E(a19,x16451)),
% 61.18/61.35 inference(scs_inference,[],[187,292])).
% 61.18/61.35 cnf(1646,plain,
% 61.18/61.35 (P10(f7(a16,a20,a22,a19),a16,a16,a19)),
% 61.18/61.35 inference(equality_inference,[],[1645])).
% 61.18/61.35 cnf(1647,plain,
% 61.18/61.35 (P10(a16,a19,a16,f7(a16,a20,a22,a19))),
% 61.18/61.35 inference(scs_inference,[],[1646,759])).
% 61.18/61.35 cnf(1649,plain,
% 61.18/61.35 (P9(f7(a16,a20,a22,a19),a16,a16,f7(a16,a20,a22,a19))),
% 61.18/61.35 inference(scs_inference,[],[1646,759,180])).
% 61.18/61.35 cnf(1657,plain,
% 61.18/61.35 (P10(a16,f7(a16,a20,a22,a19),a19,a16)),
% 61.18/61.35 inference(scs_inference,[],[1647,759])).
% 61.18/61.35 cnf(1659,plain,
% 61.18/61.35 (P10(f7(a16,a20,a22,a19),a16,a19,a16)),
% 61.18/61.35 inference(scs_inference,[],[1649,1647,759,182])).
% 61.18/61.35 cnf(1661,plain,
% 61.18/61.35 (P9(a16,a19,a19,a16)),
% 61.18/61.35 inference(scs_inference,[],[1649,1647,759,182,180])).
% 61.18/61.35 cnf(1669,plain,
% 61.18/61.35 (P10(a19,a16,f7(a16,a20,a22,a19),a16)),
% 61.18/61.35 inference(scs_inference,[],[1657,759])).
% 61.18/61.35 cnf(1671,plain,
% 61.18/61.35 (P10(a16,a19,f7(a16,a20,a22,a19),a16)),
% 61.18/61.35 inference(scs_inference,[],[1657,1661,759,182])).
% 61.18/61.35 cnf(1673,plain,
% 61.18/61.35 (P9(a19,a16,a16,a19)),
% 61.18/61.35 inference(scs_inference,[],[1646,1657,1661,759,182,180])).
% 61.18/61.35 cnf(1675,plain,
% 61.18/61.35 (P9(a19,a16,a19,a16)),
% 61.18/61.35 inference(scs_inference,[],[1646,1657,1661,759,182,180,179])).
% 61.18/61.35 cnf(1695,plain,
% 61.18/61.35 (P10(a19,a16,a16,f7(a16,a20,a22,a19))),
% 61.18/61.35 inference(scs_inference,[],[1659,759])).
% 61.18/61.35 cnf(1699,plain,
% 61.18/61.35 (P9(f7(a16,a20,a22,a19),a16,f7(a16,a20,a22,a19),a16)),
% 61.18/61.35 inference(scs_inference,[],[146,1659,1669,759,229,180])).
% 61.18/61.35 cnf(1701,plain,
% 61.18/61.35 (~P8(x17011,x17012,x17013,x17014,a16,f7(a16,a20,a22,a19),a16,a17)+P8(x17011,x17012,x17013,x17014,a18,a16,a18,a17)),
% 61.18/61.35 inference(scs_inference,[],[146,1659,1669,759,229,180,262])).
% 61.18/61.35 cnf(1706,plain,
% 61.18/61.35 (P10(a16,f7(a16,a20,a22,a19),a16,a19)),
% 61.18/61.35 inference(scs_inference,[],[1695,759])).
% 61.18/61.35 cnf(1708,plain,
% 61.18/61.35 (P9(a16,a19,a16,a19)),
% 61.18/61.35 inference(scs_inference,[],[1646,1695,1671,759,180])).
% 61.18/61.35 cnf(1715,plain,
% 61.18/61.35 (P9(a16,f7(a16,a20,a22,a19),a16,f7(a16,a20,a22,a19))),
% 61.18/61.35 inference(scs_inference,[],[1695,1657,180])).
% 61.18/61.35 cnf(1840,plain,
% 61.18/61.35 (P8(f7(a16,a20,a22,a19),a16,a16,a17,a18,a16,a18,a17)),
% 61.18/61.35 inference(scs_inference,[],[1649,225,1701])).
% 61.18/61.35 cnf(1841,plain,
% 61.18/61.35 (~P8(x18411,x18412,x18413,x18414,f7(a16,a20,a22,a19),a16,a16,a17)+P8(x18411,x18412,x18413,x18414,a18,a16,a18,a17)),
% 61.18/61.35 inference(scs_inference,[],[1840,262])).
% 61.18/61.35 cnf(1876,plain,
% 61.18/61.35 (P8(a16,f7(a16,a20,a22,a19),a16,a20,a22,a16,a22,a20)),
% 61.18/61.35 inference(scs_inference,[],[147,1695,229])).
% 61.18/61.35 cnf(1878,plain,
% 61.18/61.35 (~P8(x18781,x18782,x18783,x18784,a16,f7(a16,a20,a22,a19),a16,a20)+P8(x18781,x18782,x18783,x18784,a22,a16,a22,a20)),
% 61.18/61.35 inference(scs_inference,[],[147,1695,229,262])).
% 61.18/61.35 cnf(1989,plain,
% 61.18/61.35 (~P6(x19891,a19,a19)+P6(x19891,a16,a16)),
% 61.18/61.35 inference(scs_inference,[],[1675,175])).
% 61.18/61.35 cnf(1993,plain,
% 61.18/61.35 (~P6(x19931,f7(a16,a20,a22,a19),f7(a16,a20,a22,a19))+P6(x19931,a16,a16)),
% 61.18/61.35 inference(scs_inference,[],[1699,175])).
% 61.18/61.35 cnf(1996,plain,
% 61.18/61.35 (~P6(x19961,a16,a16)+P6(x19961,a19,a19)),
% 61.18/61.35 inference(scs_inference,[],[1708,175])).
% 61.18/61.35 cnf(1998,plain,
% 61.18/61.35 (P6(x19981,a19,a19)+~P6(x19981,f7(a16,a20,a22,a19),f7(a16,a20,a22,a19))),
% 61.18/61.35 inference(scs_inference,[],[1708,175,1993])).
% 61.18/61.35 cnf(2018,plain,
% 61.18/61.35 (P4(x20181,a19,x20181,a19)+~P6(x20181,a16,a16)),
% 61.18/61.35 inference(scs_inference,[],[1996,752])).
% 61.18/61.35 cnf(2050,plain,
% 61.18/61.35 (P8(x20501,a19,a19,a19,a19,a19,x20501,a19)+~P6(x20501,a16,a16)),
% 61.18/61.35 inference(scs_inference,[],[2018,226])).
% 61.18/61.35 cnf(2114,plain,
% 61.18/61.35 (~P6(x21141,f7(a16,a20,a22,a19),f7(a16,a20,a22,a19))+P8(x21141,a19,a19,a19,a19,a19,x21141,a19)),
% 61.18/61.35 inference(scs_inference,[],[2050,1993])).
% 61.18/61.35 cnf(3449,plain,
% 61.18/61.35 (P1(a2,a1,a15)),
% 61.18/61.35 inference(scs_inference,[],[142,151])).
% 61.18/61.35 cnf(3451,plain,
% 61.18/61.35 (P1(a1,a15,a2)),
% 61.18/61.35 inference(scs_inference,[],[142,151,152])).
% 61.18/61.35 cnf(3455,plain,
% 61.18/61.35 (P8(a16,f7(a16,a20,a22,a19),x34551,x34552,a16,f7(a16,a20,a22,a19),x34551,x34552)),
% 61.18/61.35 inference(scs_inference,[],[142,1715,151,152,160,225])).
% 61.18/61.35 cnf(3459,plain,
% 61.18/61.35 (P8(f7(a16,a20,a22,a19),a16,a16,a20,a22,a16,a22,a20)),
% 61.18/61.35 inference(scs_inference,[],[142,1876,146,1715,151,152,160,225,187,254])).
% 61.18/61.35 cnf(3467,plain,
% 61.18/61.35 (P1(f4(a16,a16,a19),a19,a16)),
% 61.18/61.35 inference(scs_inference,[],[142,1876,146,1706,1715,151,152,160,225,187,254,253,252,255,177])).
% 61.18/61.35 cnf(3469,plain,
% 61.18/61.35 (P1(f5(a16,a16,a19),a19,a16)),
% 61.18/61.35 inference(scs_inference,[],[142,1876,146,1706,1715,151,152,160,225,187,254,253,252,255,177,178])).
% 61.18/61.35 cnf(3471,plain,
% 61.18/61.35 (P10(a16,f4(a16,a16,a19),a19,a16)),
% 61.18/61.35 inference(scs_inference,[],[142,1876,146,1706,1715,151,152,160,225,187,254,253,252,255,177,178,189])).
% 61.18/61.35 cnf(3473,plain,
% 61.18/61.35 (P10(a16,f5(a16,a16,a19),a19,a16)),
% 61.18/61.35 inference(scs_inference,[],[142,1876,146,1706,1715,151,152,160,225,187,254,253,252,255,177,178,189,190])).
% 61.18/61.35 cnf(3475,plain,
% 61.18/61.35 (P8(f7(a16,a20,a22,a19),a16,a16,a20,a16,f7(a16,a20,a22,a19),a16,a20)),
% 61.18/61.35 inference(scs_inference,[],[142,1876,146,1706,1715,151,152,160,225,187,254,253,252,255,177,178,189,190,262])).
% 61.18/61.35 cnf(3477,plain,
% 61.18/61.35 (P3(f7(a16,a20,a22,a19),a18,a16,a16)),
% 61.18/61.35 inference(scs_inference,[],[142,329,1876,146,1706,1715,151,152,160,225,187,254,253,252,255,177,178,189,190,262,236])).
% 61.18/61.35 cnf(3479,plain,
% 61.18/61.35 (P9(f7(a16,a17,a18,a19),a16,f7(a16,a20,a22,a19),a16)),
% 61.18/61.35 inference(scs_inference,[],[142,329,1671,1876,146,1706,1715,151,152,160,225,187,254,253,252,255,177,178,189,190,262,236,180])).
% 61.18/61.35 cnf(3481,plain,
% 61.18/61.35 (P9(f7(a16,a20,a22,a19),a16,f7(a16,a17,a18,a19),a16)),
% 61.18/61.35 inference(scs_inference,[],[142,329,1671,1876,146,1706,1715,151,152,160,225,187,254,253,252,255,177,178,189,190,262,236,180,163])).
% 61.18/61.35 cnf(3483,plain,
% 61.18/61.35 (P9(f7(a16,a17,a18,a19),a16,a16,f7(a16,a20,a22,a19))),
% 61.18/61.35 inference(scs_inference,[],[142,329,1671,1876,146,1706,1715,151,152,160,225,187,254,253,252,255,177,178,189,190,262,236,180,163,164])).
% 61.18/61.35 cnf(3485,plain,
% 61.18/61.35 (P10(a16,a19,f7(a16,a17,a18,a19),a16)),
% 61.18/61.35 inference(scs_inference,[],[142,329,1671,1876,146,1706,1715,151,152,160,225,187,254,253,252,255,177,178,189,190,262,236,180,163,164,165])).
% 61.18/61.35 cnf(3487,plain,
% 61.18/61.35 (P10(f7(a16,a17,a18,a19),a16,a19,a16)),
% 61.18/61.35 inference(scs_inference,[],[142,329,1671,1876,146,1706,1715,151,152,160,225,187,254,253,252,255,177,178,189,190,262,236,180,163,164,165,166])).
% 61.18/61.35 cnf(3489,plain,
% 61.18/61.35 (P8(a22,a16,a22,a20,a22,a16,a22,a20)),
% 61.18/61.35 inference(scs_inference,[],[142,329,1671,1876,146,1706,1715,151,152,160,225,187,254,253,252,255,177,178,189,190,262,236,180,163,164,165,166,1878])).
% 61.18/61.35 cnf(3491,plain,
% 61.18/61.35 (P3(a18,f7(a16,a20,a22,a19),a16,a16)),
% 61.18/61.35 inference(scs_inference,[],[142,329,1671,1876,146,1706,1715,151,152,160,225,187,254,253,252,255,177,178,189,190,262,236,180,163,164,165,166,1878,169])).
% 61.18/61.35 cnf(3493,plain,
% 61.18/61.35 (P3(f7(a16,a20,a22,a19),a16,a18,a16)),
% 61.18/61.35 inference(scs_inference,[],[142,329,1671,1876,146,1706,1715,151,152,160,225,187,254,253,252,255,177,178,189,190,262,236,180,163,164,165,166,1878,169,170])).
% 61.18/61.35 cnf(3535,plain,
% 61.18/61.35 (P9(a22,a16,a22,a16)),
% 61.18/61.35 inference(scs_inference,[],[3489,3487,165,233])).
% 61.18/61.35 cnf(3537,plain,
% 61.18/61.35 (P1(a2,a15,a1)),
% 61.18/61.35 inference(scs_inference,[],[3449,3489,3487,165,233,152])).
% 61.18/61.35 cnf(3539,plain,
% 61.18/61.35 (P9(f7(a16,a20,a22,a19),a16,a16,f7(a16,a17,a18,a19))),
% 61.18/61.35 inference(scs_inference,[],[3449,3489,3481,3487,165,233,152,164])).
% 61.18/61.35 cnf(3541,plain,
% 61.18/61.35 (P1(a15,a1,a2)),
% 61.18/61.35 inference(scs_inference,[],[3449,3451,3489,3481,3487,165,233,152,164,151])).
% 61.18/61.35 cnf(3543,plain,
% 61.18/61.35 (P8(f7(a16,a17,a18,a19),a16,x35431,x35432,a16,f7(a16,a20,a22,a19),x35431,x35432)),
% 61.18/61.35 inference(scs_inference,[],[3449,3451,3489,3483,3481,3487,165,233,152,164,151,225])).
% 61.18/61.35 cnf(3547,plain,
% 61.18/61.35 (P1(a19,a16,a16)),
% 61.18/61.35 inference(scs_inference,[],[3449,3451,3489,3483,3481,3487,3485,1675,165,233,152,164,151,225,166,160])).
% 61.18/61.35 cnf(3549,plain,
% 61.18/61.35 (P8(a16,a22,a22,a20,a22,a16,a22,a20)),
% 61.18/61.35 inference(scs_inference,[],[3449,3451,3489,3483,3481,3487,3485,1675,165,233,152,164,151,225,166,160,254])).
% 61.18/61.35 cnf(3553,plain,
% 61.18/61.35 (P9(a16,f7(a16,a20,a22,a19),f7(a16,a17,a18,a19),a16)),
% 61.18/61.35 inference(scs_inference,[],[3449,3451,3489,3483,3481,3487,3485,1675,165,233,152,164,151,225,166,160,254,1878,163])).
% 61.18/61.35 cnf(3557,plain,
% 61.18/61.35 (P8(a22,a20,a22,a16,a22,a20,a22,a16)),
% 61.18/61.35 inference(scs_inference,[],[3449,3451,3489,3483,3481,3487,3485,3491,1675,165,233,152,164,151,225,166,160,254,1878,163,224,253])).
% 61.18/61.35 cnf(3559,plain,
% 61.18/61.35 (P10(f7(a2,a20,a24,a21),a2,a2,a21)),
% 61.18/61.35 inference(scs_inference,[],[3449,3451,3489,3483,3481,3487,3485,3491,1675,148,165,233,152,164,151,225,166,160,254,1878,163,224,253,187])).
% 61.18/61.35 cnf(3561,plain,
% 61.18/61.35 (P3(a16,f7(a16,a20,a22,a19),a18,a16)),
% 61.18/61.35 inference(scs_inference,[],[3449,3451,3489,3483,3481,3487,3485,3491,3493,1675,148,165,233,152,164,151,225,166,160,254,1878,163,224,253,187,169])).
% 61.18/61.35 cnf(3565,plain,
% 61.18/61.35 (P3(f7(a16,a20,a22,a19),a16,a16,a18)),
% 61.18/61.35 inference(scs_inference,[],[3449,3451,3489,3483,3481,3487,3485,3475,3491,3493,1675,148,165,233,152,164,151,225,166,160,254,1878,163,224,253,187,169,252,171])).
% 61.18/61.35 cnf(3567,plain,
% 61.18/61.35 (P8(a22,a16,a22,a16,a22,a20,a22,a20)),
% 61.18/61.35 inference(scs_inference,[],[3449,3451,3489,3483,3481,3487,3485,3475,3491,3493,1675,148,165,233,152,164,151,225,166,160,254,1878,163,224,253,187,169,252,171,255])).
% 61.18/61.35 cnf(3569,plain,
% 61.18/61.35 (P3(a18,a16,f7(a16,a20,a22,a19),a16)),
% 61.18/61.35 inference(scs_inference,[],[3449,3451,3489,3483,3481,3487,3485,3475,3491,3493,1675,148,165,233,152,164,151,225,166,160,254,1878,163,224,253,187,169,252,171,255,170])).
% 61.18/61.35 cnf(3571,plain,
% 61.18/61.35 (P3(a18,a16,a16,a16)),
% 61.18/61.35 inference(scs_inference,[],[3449,3451,3489,3483,3481,3487,3485,3475,3477,3491,3493,1675,148,165,233,152,164,151,225,166,160,254,1878,163,224,253,187,169,252,171,255,170,185])).
% 61.18/61.35 cnf(3575,plain,
% 61.18/61.35 (P9(f7(a16,a17,a18,a19),a16,f7(a16,a17,a18,a19),a16)),
% 61.18/61.35 inference(scs_inference,[],[3449,3451,3489,3483,3481,3479,3487,3485,3475,3477,3491,3493,1675,148,1673,165,233,152,164,151,225,166,160,254,1878,163,224,253,187,169,252,171,255,170,185,182,179])).
% 61.18/61.35 cnf(3579,plain,
% 61.18/61.35 (~P3(a17,x35791,a2,a1)+~E(x35791,a20)),
% 61.18/61.35 inference(scs_inference,[],[3449,3451,3489,3483,3481,3479,3487,3485,3475,3477,3491,3493,410,147,1675,148,1673,165,233,152,164,151,225,166,160,254,1878,163,224,253,187,169,252,171,255,170,185,182,179,172,100])).
% 61.18/61.35 cnf(3583,plain,
% 61.18/61.35 (P8(f7(a16,a17,a18,a19),a16,a16,a17,a18,a16,a18,a17)),
% 61.18/61.35 inference(scs_inference,[],[3543,1701])).
% 61.18/61.35 cnf(3586,plain,
% 61.18/61.35 (P9(a16,a22,a22,a16)),
% 61.18/61.35 inference(scs_inference,[],[3549,3543,1701,233])).
% 61.18/61.35 cnf(3590,plain,
% 61.18/61.35 (P8(a22,a16,x35901,x35902,a22,a16,x35901,x35902)),
% 61.18/61.35 inference(scs_inference,[],[3535,3549,3471,3543,1701,233,165,225])).
% 61.18/61.35 cnf(3592,plain,
% 61.18/61.35 (P9(a22,a16,a16,a22)),
% 61.18/61.35 inference(scs_inference,[],[3535,3549,3471,3543,1701,233,165,225,164])).
% 61.18/61.35 cnf(3594,plain,
% 61.18/61.35 (P1(a15,a2,a1)),
% 61.18/61.35 inference(scs_inference,[],[3535,3541,3549,3471,3543,1701,233,165,225,164,152])).
% 61.18/61.35 cnf(3598,plain,
% 61.18/61.35 (P8(a20,a22,a22,a16,a22,a20,a22,a16)),
% 61.18/61.35 inference(scs_inference,[],[3535,3541,3549,3557,3471,3543,1701,233,165,225,164,152,166,254])).
% 61.18/61.35 cnf(3600,plain,
% 61.18/61.35 (P9(a16,f7(a16,a17,a18,a19),f7(a16,a20,a22,a19),a16)),
% 61.18/61.35 inference(scs_inference,[],[3535,3541,3549,3557,3471,3543,3539,1701,233,165,225,164,152,166,254,163])).
% 61.18/61.35 cnf(3602,plain,
% 61.18/61.35 (P8(a22,a20,a16,a22,a22,a20,a22,a16)),
% 61.18/61.35 inference(scs_inference,[],[3535,3541,3549,3557,3471,3543,3539,1701,233,165,225,164,152,166,254,163,253])).
% 61.18/61.35 cnf(3604,plain,
% 61.18/61.35 (P1(a16,a19,a16)),
% 61.18/61.35 inference(scs_inference,[],[3535,3541,3547,3549,3557,3471,3543,3539,1701,233,165,225,164,152,166,254,163,253,151])).
% 61.18/61.35 cnf(3606,plain,
% 61.18/61.35 (P1(a22,a16,a16)),
% 61.18/61.35 inference(scs_inference,[],[3535,3541,3547,3549,3557,3471,3543,3539,1701,233,165,225,164,152,166,254,163,253,151,160])).
% 61.18/61.35 cnf(3608,plain,
% 61.18/61.35 (P3(a16,a18,a16,a16)),
% 61.18/61.35 inference(scs_inference,[],[3535,3541,3547,3549,3557,3571,3471,3543,3539,1701,233,165,225,164,152,166,254,163,253,151,160,169])).
% 61.18/61.35 cnf(3614,plain,
% 61.18/61.35 (P10(f7(a18,a15,a2,a21),a18,a18,a21)),
% 61.18/61.35 inference(scs_inference,[],[3535,3541,3547,3549,3557,3571,3471,3543,3539,149,1701,233,165,225,164,152,166,254,163,253,151,160,169,224,252,187])).
% 61.18/61.35 cnf(3616,plain,
% 61.18/61.35 (P3(a16,f7(a16,a20,a22,a19),a16,a18)),
% 61.18/61.35 inference(scs_inference,[],[3535,3541,3547,3549,3557,3571,3471,3543,3539,3561,149,1701,233,165,225,164,152,166,254,163,253,151,160,169,224,252,187,171])).
% 61.18/61.35 cnf(3618,plain,
% 61.18/61.35 (P8(a16,a22,a22,a16,a22,a20,a22,a20)),
% 61.18/61.35 inference(scs_inference,[],[3535,3541,3547,3549,3557,3571,3471,3543,3539,3561,149,1701,233,165,225,164,152,166,254,163,253,151,160,169,224,252,187,171,255])).
% 61.18/61.35 cnf(3620,plain,
% 61.18/61.35 (P3(a16,a18,f7(a16,a20,a22,a19),a16)),
% 61.18/61.35 inference(scs_inference,[],[3535,3541,3547,3549,3557,3571,3471,3543,3539,3561,149,1701,233,165,225,164,152,166,254,163,253,151,160,169,224,252,187,171,255,170])).
% 61.18/61.35 cnf(3631,plain,
% 61.18/61.35 (P1(a16,a16,a19)),
% 61.18/61.35 inference(scs_inference,[],[3598,3604,233,152])).
% 61.18/61.35 cnf(3635,plain,
% 61.18/61.35 (P8(a16,a22,x36351,x36352,a22,a16,x36351,x36352)),
% 61.18/61.35 inference(scs_inference,[],[3586,3598,3604,3473,233,152,165,225])).
% 61.18/61.35 cnf(3641,plain,
% 61.18/61.35 (P8(x36411,x36412,a22,a16,x36411,x36412,a22,a16)),
% 61.18/61.35 inference(scs_inference,[],[3590,3586,3598,3604,3473,233,152,165,225,166,163,253])).
% 61.18/61.35 cnf(3645,plain,
% 61.18/61.35 (P9(a16,a22,a16,a22)),
% 61.18/61.35 inference(scs_inference,[],[3590,3586,3598,3602,3604,3473,233,152,165,225,166,163,253,254,164])).
% 61.18/61.35 cnf(3647,plain,
% 61.18/61.35 (P1(a16,a22,a16)),
% 61.18/61.35 inference(scs_inference,[],[3590,3586,3598,3602,3604,3606,3473,233,152,165,225,166,163,253,254,164,151])).
% 61.18/61.35 cnf(3649,plain,
% 61.18/61.35 (P8(a22,a20,a22,a20,a22,a16,a22,a16)),
% 61.18/61.35 inference(scs_inference,[],[3590,3567,3586,3598,3602,3604,3606,3473,233,152,165,225,166,163,253,254,164,151,252])).
% 61.18/61.35 cnf(3655,plain,
% 61.18/61.35 (P3(a16,a18,a16,f7(a16,a20,a22,a19))),
% 61.18/61.35 inference(scs_inference,[],[3590,3567,3586,3598,3602,3604,3606,3608,3473,3575,3620,233,152,165,225,166,163,253,254,164,151,252,160,224,171])).
% 61.18/61.35 cnf(3657,plain,
% 61.18/61.35 (P8(a22,a16,a22,a16,x36571,x36572,x36571,x36572)),
% 61.18/61.35 inference(scs_inference,[],[3590,3567,3586,3598,3602,3604,3606,3608,3473,3575,3620,233,152,165,225,166,163,253,254,164,151,252,160,224,171,255])).
% 61.18/61.35 cnf(3659,plain,
% 61.18/61.35 (P3(a16,a16,a18,a16)),
% 61.18/61.35 inference(scs_inference,[],[3590,3567,3586,3598,3602,3604,3606,3608,3473,3575,3620,233,152,165,225,166,163,253,254,164,151,252,160,224,171,255,170])).
% 61.18/61.35 cnf(3661,plain,
% 61.18/61.35 (P3(a16,a16,a22,a16)),
% 61.18/61.35 inference(scs_inference,[],[3590,3567,3586,3598,3602,3604,3606,3608,3473,3575,3620,233,152,165,225,166,163,253,254,164,151,252,160,224,171,255,170,236])).
% 61.18/61.35 cnf(3663,plain,
% 61.18/61.35 (P4(a16,a16,a16,a16)),
% 61.18/61.35 inference(scs_inference,[],[3590,3567,3586,3598,3602,3604,3606,3608,3473,3575,3620,233,152,165,225,166,163,253,254,164,151,252,160,224,171,255,170,236,251])).
% 61.18/61.35 cnf(3665,plain,
% 61.18/61.35 (P8(a16,a16,a16,a16,a16,a16,a16,a16)),
% 61.18/61.35 inference(scs_inference,[],[3590,3567,3586,3598,3602,3604,3606,3608,3473,3575,3620,233,152,165,225,166,163,253,254,164,151,252,160,224,171,255,170,236,251,226])).
% 61.18/61.35 cnf(3667,plain,
% 61.18/61.35 (P3(a18,a16,a16,f7(a16,a20,a22,a19))),
% 61.18/61.35 inference(scs_inference,[],[3590,3567,3586,3598,3602,3604,3606,3608,3473,3575,3620,233,152,165,225,166,163,253,254,164,151,252,160,224,171,255,170,236,251,226,169])).
% 61.18/61.35 cnf(3669,plain,
% 61.18/61.35 (P10(a16,a16,a16,a16)),
% 61.18/61.35 inference(scs_inference,[],[3590,3567,3586,3598,3602,3604,3606,3608,3473,3575,3620,233,152,165,225,166,163,253,254,164,151,252,160,224,171,255,170,236,251,226,169,181])).
% 61.18/61.35 cnf(3671,plain,
% 61.18/61.35 (P2(a16,a16,a16,a16)),
% 61.18/61.35 inference(scs_inference,[],[3590,3567,3586,3598,3602,3604,3606,3608,3473,3575,3620,233,152,165,225,166,163,253,254,164,151,252,160,224,171,255,170,236,251,226,169,181,184])).
% 61.18/61.35 cnf(3673,plain,
% 61.18/61.35 (P1(a16,a16,f3(a16,a16,a16))),
% 61.18/61.35 inference(scs_inference,[],[3590,3567,3586,3598,3602,3604,3606,3608,3473,3575,3620,233,152,165,225,166,163,253,254,164,151,252,160,224,171,255,170,236,251,226,169,181,184,176])).
% 61.18/61.35 cnf(3678,plain,
% 61.18/61.35 (P4(a16,a16,a16,f3(a16,a16,a16))),
% 61.18/61.35 inference(scs_inference,[],[3590,3567,3586,3598,3602,3604,3606,3608,3473,3575,3620,3455,233,152,165,225,166,163,253,254,164,151,252,160,224,171,255,170,236,251,226,169,181,184,176,234,188])).
% 61.18/61.35 cnf(3688,plain,
% 61.18/61.35 (P4(a16,a16,a16,f30(a16,a16,a16,a16,a16))),
% 61.18/61.35 inference(scs_inference,[],[3590,3567,3586,3598,3602,3604,3606,3608,3473,3575,3620,3455,233,152,165,225,166,163,253,254,164,151,252,160,224,171,255,170,236,251,226,169,181,184,176,234,188,193,194,197,198,199])).
% 61.18/61.35 cnf(3690,plain,
% 61.18/61.35 (P9(f30(a16,a16,a16,a16,a16),a16,a16,a16)),
% 61.18/61.35 inference(scs_inference,[],[3590,3567,3586,3598,3602,3604,3606,3608,3473,3575,3620,3455,233,152,165,225,166,163,253,254,164,151,252,160,224,171,255,170,236,251,226,169,181,184,176,234,188,193,194,197,198,199,201])).
% 61.18/61.35 cnf(3696,plain,
% 61.18/61.35 (P1(f14(a16,a16,a16,a16),a16,a16)),
% 61.18/61.35 inference(scs_inference,[],[3590,3567,3586,3598,3602,3604,3606,3608,3473,3575,3620,3455,233,152,165,225,166,163,253,254,164,151,252,160,224,171,255,170,236,251,226,169,181,184,176,234,188,193,194,197,198,199,201,245,246,247])).
% 61.18/61.35 cnf(3702,plain,
% 61.18/61.35 (P10(a22,a16,a22,a16)),
% 61.18/61.35 inference(scs_inference,[],[3590,3567,3586,3598,3602,3604,3606,3608,3473,3575,3620,3455,233,152,165,225,166,163,253,254,164,151,252,160,224,171,255,170,236,251,226,169,181,184,176,234,188,193,194,197,198,199,201,245,246,247,249,250,241])).
% 61.18/61.35 cnf(3708,plain,
% 61.18/61.35 (P10(a16,f5(a16,a16,a16),a16,a16)),
% 61.18/61.35 inference(scs_inference,[],[3590,3567,3586,3598,3602,3604,3606,3608,3473,3575,3620,3455,3535,233,152,165,225,166,163,253,254,164,151,252,160,224,171,255,170,236,251,226,169,181,184,176,234,188,193,194,197,198,199,201,245,246,247,249,250,241,240,177,190])).
% 61.18/61.35 cnf(3712,plain,
% 61.18/61.35 (P10(a16,f4(a16,a16,a16),a16,a16)),
% 61.18/61.35 inference(scs_inference,[],[3590,3567,3586,3598,3602,3604,3606,3608,3473,3575,3620,3455,3535,233,152,165,225,166,163,253,254,164,151,252,160,224,171,255,170,236,251,226,169,181,184,176,234,188,193,194,197,198,199,201,245,246,247,249,250,241,240,177,190,178,189])).
% 61.18/61.35 cnf(3714,plain,
% 61.18/61.35 (P3(a16,a16,a16,a16)),
% 61.18/61.35 inference(scs_inference,[],[3590,3567,3586,3598,3602,3604,3606,3608,3473,3575,3620,3455,3535,233,152,165,225,166,163,253,254,164,151,252,160,224,171,255,170,236,251,226,169,181,184,176,234,188,193,194,197,198,199,201,245,246,247,249,250,241,240,177,190,178,189,196])).
% 61.18/61.35 cnf(3720,plain,
% 61.18/61.35 (P4(a16,f3(a16,a16,a16),a16,a16)),
% 61.18/61.35 inference(scs_inference,[],[3590,3567,3586,3598,3602,3604,3606,3608,3473,3575,3620,3455,3535,1673,233,152,165,225,166,163,253,254,164,151,252,160,224,171,255,170,236,251,226,169,181,184,176,234,188,193,194,197,198,199,201,245,246,247,249,250,241,240,177,190,178,189,196,206,207,167])).
% 61.18/61.35 cnf(3722,plain,
% 61.18/61.35 (P4(a16,a16,f3(a16,a16,a16),a16)),
% 61.18/61.35 inference(scs_inference,[],[3590,3567,3586,3598,3602,3604,3606,3608,3473,3575,3620,3455,3535,1673,233,152,165,225,166,163,253,254,164,151,252,160,224,171,255,170,236,251,226,169,181,184,176,234,188,193,194,197,198,199,201,245,246,247,249,250,241,240,177,190,178,189,196,206,207,167,168])).
% 61.18/61.35 cnf(3724,plain,
% 61.18/61.35 (P10(f7(a16,a16,a16,a16),a16,a16,a16)),
% 61.18/61.35 inference(scs_inference,[],[3590,3567,3586,3598,3602,3604,3606,3608,3473,3575,3620,3455,3535,1673,233,152,165,225,166,163,253,254,164,151,252,160,224,171,255,170,236,251,226,169,181,184,176,234,188,193,194,197,198,199,201,245,246,247,249,250,241,240,177,190,178,189,196,206,207,167,168,187])).
% 61.18/61.35 cnf(3726,plain,
% 61.18/61.35 (~P3(a2,a20,x37261,a17)+~E(x37261,a1)),
% 61.18/61.35 inference(scs_inference,[],[3590,3567,3586,3598,3602,3604,3606,3608,3473,3575,3620,3455,387,3535,1673,233,152,165,225,166,163,253,254,164,151,252,160,224,171,255,170,236,251,226,169,181,184,176,234,188,193,194,197,198,199,201,245,246,247,249,250,241,240,177,190,178,189,196,206,207,167,168,187,101])).
% 61.18/61.35 cnf(3729,plain,
% 61.18/61.35 (P8(a16,a16,a16,f30(a16,a16,a16,a16,a16),a16,f30(a16,a16,a16,a16,a16),a16,f30(a16,a16,a16,a16,a16))),
% 61.18/61.35 inference(scs_inference,[],[3688,226])).
% 61.18/61.35 cnf(3731,plain,
% 61.18/61.35 (P4(a16,f30(a16,a16,a16,a16,a16),a16,a16)),
% 61.18/61.35 inference(scs_inference,[],[3688,226,167])).
% 61.18/61.35 cnf(3733,plain,
% 61.18/61.35 (P9(x37331,x37332,x37331,x37332)),
% 61.18/61.35 inference(scs_inference,[],[3641,3688,226,167,233])).
% 61.18/61.35 cnf(3735,plain,
% 61.18/61.35 (P4(a16,a16,f30(a16,a16,a16,a16,a16),a16)),
% 61.18/61.35 inference(scs_inference,[],[3641,3688,226,167,233,168])).
% 61.18/61.35 cnf(3737,plain,
% 61.18/61.35 (P1(a16,a16,a22)),
% 61.18/61.35 inference(scs_inference,[],[3641,3647,3688,226,167,233,168,152])).
% 61.18/61.35 cnf(3739,plain,
% 61.18/61.35 (P8(a22,a16,x37391,x37392,a16,a22,x37391,x37392)),
% 61.18/61.35 inference(scs_inference,[],[3592,3641,3647,3688,226,167,233,168,152,225])).
% 61.18/61.35 cnf(3743,plain,
% 61.18/61.35 (P9(a16,a16,f30(a16,a16,a16,a16,a16),a16)),
% 61.18/61.35 inference(scs_inference,[],[3592,3641,3647,3559,3688,3690,226,167,233,168,152,225,165,163])).
% 61.18/61.35 cnf(3747,plain,
% 61.18/61.35 (P9(a16,f7(a16,a20,a22,a19),a16,f7(a16,a17,a18,a19))),
% 61.18/61.35 inference(scs_inference,[],[3618,3592,3641,3647,3559,3553,3688,3690,226,167,233,168,152,225,165,163,253,164])).
% 61.18/61.35 cnf(3751,plain,
% 61.18/61.35 (P10(a22,a16,a16,a22)),
% 61.18/61.35 inference(scs_inference,[],[3618,3592,3641,3647,3702,3467,3559,3553,3688,3690,226,167,233,168,152,225,165,163,253,164,151,166])).
% 61.18/61.35 cnf(3753,plain,
% 61.18/61.35 (P8(x37531,x37532,a22,a16,x37532,x37531,a22,a16)),
% 61.18/61.35 inference(scs_inference,[],[3618,3592,3641,3647,3702,3467,3559,3553,3688,3690,226,167,233,168,152,225,165,163,253,164,151,166,254])).
% 61.18/61.35 cnf(3755,plain,
% 61.18/61.35 (P8(a22,a20,a22,a20,a16,a22,a22,a16)),
% 61.18/61.35 inference(scs_inference,[],[3618,3592,3641,3647,3702,3467,3559,3553,3688,3690,226,167,233,168,152,225,165,163,253,164,151,166,254,252])).
% 61.18/61.35 cnf(3759,plain,
% 61.18/61.35 (P1(a16,a22,a22)),
% 61.18/61.35 inference(scs_inference,[],[3618,3592,3645,3641,3647,3659,3702,3467,3559,3553,3688,3690,226,167,233,168,152,225,165,163,253,164,151,166,254,252,224,160])).
% 61.18/61.35 cnf(3765,plain,
% 61.18/61.35 (P3(a16,a16,a16,a18)),
% 61.18/61.35 inference(scs_inference,[],[3618,3592,3645,3635,3641,3647,3659,3661,3702,3467,3559,3553,3688,3690,226,167,233,168,152,225,165,163,253,164,151,166,254,252,224,160,255,170,171])).
% 61.18/61.35 cnf(3767,plain,
% 61.18/61.35 (P2(f8(a16,a16,a16),a16,a16,a16)),
% 61.18/61.35 inference(scs_inference,[],[3618,3592,3645,3635,3641,3647,3659,3661,3669,3702,3714,3467,3559,3553,3688,3690,226,167,233,168,152,225,165,163,253,164,151,166,254,252,224,160,255,170,171,191])).
% 61.18/61.35 cnf(3774,plain,
% 61.18/61.35 (P10(a16,a22,a22,a16)),
% 61.18/61.35 inference(scs_inference,[],[3618,3592,3645,3635,3641,3631,3647,3659,3661,3669,3702,3714,3467,3559,3553,3688,3690,3543,226,167,233,168,152,225,165,163,253,164,151,166,254,252,224,160,255,170,171,191,197,240,241])).
% 61.18/61.35 cnf(3779,plain,
% 61.18/61.35 (P2(a16,a16,f30(a16,a16,a16,a16,a16),f30(a16,a16,a16,a16,a16))),
% 61.18/61.35 inference(scs_inference,[],[3618,3592,3645,3635,3641,3631,3647,3659,3661,3669,3702,3714,3467,3559,3553,3688,3690,3722,3543,226,167,233,168,152,225,165,163,253,164,151,166,254,252,224,160,255,170,171,191,197,240,241,181,184])).
% 61.18/61.35 cnf(3781,plain,
% 61.18/61.35 (P1(f4(a22,a22,a16),a16,a22)),
% 61.18/61.35 inference(scs_inference,[],[3618,3592,3645,3635,3641,3631,3647,3659,3661,3669,3702,3714,3467,3559,3553,3688,3690,3722,3543,226,167,233,168,152,225,165,163,253,164,151,166,254,252,224,160,255,170,171,191,197,240,241,181,184,177])).
% 61.18/61.35 cnf(3783,plain,
% 61.18/61.35 (P1(f5(a22,a22,a16),a16,a22)),
% 61.18/61.35 inference(scs_inference,[],[3618,3592,3645,3635,3641,3631,3647,3659,3661,3669,3702,3714,3467,3559,3553,3688,3690,3722,3543,226,167,233,168,152,225,165,163,253,164,151,166,254,252,224,160,255,170,171,191,197,240,241,181,184,177,178])).
% 61.18/61.35 cnf(3785,plain,
% 61.18/61.35 (P10(a22,f5(a22,a22,a16),a16,a22)),
% 61.18/61.35 inference(scs_inference,[],[3618,3592,3645,3635,3641,3631,3647,3659,3661,3669,3702,3714,3467,3559,3553,3688,3690,3722,3543,226,167,233,168,152,225,165,163,253,164,151,166,254,252,224,160,255,170,171,191,197,240,241,181,184,177,178,190])).
% 61.18/61.35 cnf(3789,plain,
% 61.18/61.35 (P10(a22,f4(a22,a22,a16),a16,a22)),
% 61.18/61.35 inference(scs_inference,[],[3618,3592,3645,3635,3641,3631,3647,3659,3661,3669,3702,3714,3467,3559,3553,3688,3690,3722,3543,226,167,233,168,152,225,165,163,253,164,151,166,254,252,224,160,255,170,171,191,197,240,241,181,184,177,178,190,198,189])).
% 61.18/61.35 cnf(3802,plain,
% 61.18/61.35 (P9(f30(a16,a22,a16,a16,a16),a16,a16,a22)),
% 61.18/61.35 inference(scs_inference,[],[3618,3592,3645,3635,3641,3631,3647,3659,3661,3663,3669,3702,3714,3467,3559,3553,3688,3690,3722,3543,3455,226,167,233,168,152,225,165,163,253,164,151,166,254,252,224,160,255,170,171,191,197,240,241,181,184,177,178,190,198,189,236,206,207,169,230,201])).
% 61.18/61.35 cnf(3804,plain,
% 61.18/61.35 (P4(a16,a16,a16,f30(a16,a22,a16,a16,a16))),
% 61.18/61.35 inference(scs_inference,[],[3618,3592,3645,3635,3641,3631,3647,3659,3661,3663,3669,3702,3714,3467,3559,3553,3688,3690,3722,3543,3455,226,167,233,168,152,225,165,163,253,164,151,166,254,252,224,160,255,170,171,191,197,240,241,181,184,177,178,190,198,189,236,206,207,169,230,201,199])).
% 61.18/61.35 cnf(3806,plain,
% 61.18/61.35 (P6(a16,a16,f3(a16,a16,a16))),
% 61.18/61.35 inference(scs_inference,[],[3618,3592,3645,3635,3641,3631,3647,3659,3661,3663,3669,3702,3714,3467,3559,3553,3688,3690,3722,3678,3673,3543,3455,226,167,233,168,152,225,165,163,253,164,151,166,254,252,224,160,255,170,171,191,197,240,241,181,184,177,178,190,198,189,236,206,207,169,230,201,199,161])).
% 61.18/61.35 cnf(3810,plain,
% 61.18/61.35 (P3(a16,f30(a16,a16,a16,a16,a16),f30(a16,a16,a16,a16,a16),f30(a16,a16,a16,a16,a16))),
% 61.18/61.35 inference(scs_inference,[],[3618,3592,3645,3635,3641,3631,3647,3659,3661,3663,3669,3702,3714,3467,3559,3553,3688,3690,3722,3678,3673,3543,3455,226,167,233,168,152,225,165,163,253,164,151,166,254,252,224,160,255,170,171,191,197,240,241,181,184,177,178,190,198,189,236,206,207,169,230,201,199,161,223,196])).
% 61.18/61.35 cnf(3812,plain,
% 61.18/61.35 (P7(f14(a16,a16,a16,a16),a16,a16,a16,f14(a16,a16,a16,a16),a16,a16,a16)),
% 61.18/61.35 inference(scs_inference,[],[3618,3592,3645,3635,3641,3631,3647,3659,3661,3663,3669,3702,3714,3467,3559,3553,3688,3696,3690,3722,3678,3673,3543,3455,226,167,233,168,152,225,165,163,253,164,151,166,254,252,224,160,255,170,171,191,197,240,241,181,184,177,178,190,198,189,236,206,207,169,230,201,199,161,223,196,228])).
% 61.18/61.35 cnf(3814,plain,
% 61.18/61.35 (P6(a16,f3(a16,a16,a16),a16)),
% 61.18/61.35 inference(scs_inference,[],[3618,3592,3645,3635,3641,3631,3647,3659,3661,3663,3669,3702,3714,3467,3559,3553,3688,3696,3690,3722,3678,3673,3543,3455,226,167,233,168,152,225,165,163,253,164,151,166,254,252,224,160,255,170,171,191,197,240,241,181,184,177,178,190,198,189,236,206,207,169,230,201,199,161,223,196,228,154])).
% 61.18/61.35 cnf(3816,plain,
% 61.18/61.35 (P7(a16,a16,a16,a16,a16,f3(a16,a16,a16),a16,f3(a16,a16,a16))),
% 61.18/61.35 inference(scs_inference,[],[3618,3592,3645,3635,3641,3631,3647,3659,3661,3663,3669,3702,3714,3467,3559,3553,3688,3696,3690,3722,3678,3673,3543,3455,226,167,233,168,152,225,165,163,253,164,151,166,254,252,224,160,255,170,171,191,197,240,241,181,184,177,178,190,198,189,236,206,207,169,230,201,199,161,223,196,228,154,259])).
% 61.18/61.35 cnf(3822,plain,
% 61.18/61.35 (P7(a16,f3(a16,a16,a16),a16,a16,a16,f3(a16,a16,a16),a16,a16)),
% 61.18/61.35 inference(scs_inference,[],[3618,3592,3645,3635,3641,3631,3647,3659,3661,3663,3669,3702,3714,3467,3559,3553,3688,3696,3690,3722,3678,3673,3543,3455,226,167,233,168,152,225,165,163,253,164,151,166,254,252,224,160,255,170,171,191,197,240,241,181,184,177,178,190,198,189,236,206,207,169,230,201,199,161,223,196,228,154,259,153,258,257])).
% 61.18/61.35 cnf(3824,plain,
% 61.18/61.35 (~P3(a1,a2,a20,x38241)+~E(x38241,a17)),
% 61.18/61.35 inference(scs_inference,[],[3618,3592,3645,3635,3641,3631,3647,3659,3661,3663,3669,3702,3714,3467,3559,3553,3688,3696,3690,3722,3678,3673,3543,3455,389,226,167,233,168,152,225,165,163,253,164,151,166,254,252,224,160,255,170,171,191,197,240,241,181,184,177,178,190,198,189,236,206,207,169,230,201,199,161,223,196,228,154,259,153,258,257,102])).
% 61.18/61.35 cnf(3827,plain,
% 61.18/61.35 (P7(a16,f3(a16,a16,a16),a16,f3(a16,a16,a16),a16,a16,a16,a16)),
% 61.18/61.35 inference(scs_inference,[],[3816,256])).
% 61.18/61.35 cnf(3833,plain,
% 61.18/61.35 (P4(f30(a16,a16,a16,a16,a16),a16,a16,a16)),
% 61.18/61.35 inference(scs_inference,[],[3731,3816,3812,3735,256,259,226,167])).
% 61.18/61.35 cnf(3837,plain,
% 61.18/61.35 (P9(x38371,x38372,x38372,x38371)),
% 61.18/61.35 inference(scs_inference,[],[3753,3731,3816,3812,3735,256,259,226,167,257,233])).
% 61.18/61.35 cnf(3839,plain,
% 61.18/61.35 (P7(f3(a16,a16,a16),a16,a16,a16,a16,f3(a16,a16,a16),a16,a16)),
% 61.18/61.35 inference(scs_inference,[],[3753,3731,3816,3822,3812,3735,256,259,226,167,257,233,258])).
% 61.18/61.35 cnf(3843,plain,
% 61.18/61.35 (P8(x38431,x38432,x38433,x38434,x38431,x38432,x38433,x38434)),
% 61.18/61.35 inference(scs_inference,[],[3733,3753,3731,3816,3822,3812,3735,3804,256,259,226,167,257,233,258,168,225])).
% 61.18/61.35 cnf(3847,plain,
% 61.18/61.35 (P8(x38471,x38472,a22,a16,x38471,x38472,a16,a22)),
% 61.18/61.35 inference(scs_inference,[],[3733,3739,3753,3614,3731,3816,3822,3812,3735,3804,256,259,226,167,257,233,258,168,225,165,253])).
% 61.18/61.35 cnf(3851,plain,
% 61.18/61.35 (P9(a16,f7(a16,a17,a18,a19),a16,f7(a16,a20,a22,a19))),
% 61.18/61.35 inference(scs_inference,[],[3733,3739,3753,3469,3614,3600,3731,3816,3822,3812,3735,3804,256,259,226,167,257,233,258,168,225,165,253,152,164])).
% 61.18/61.35 cnf(3853,plain,
% 61.18/61.35 (P9(a16,a22,f30(a16,a22,a16,a16,a16),a16)),
% 61.18/61.35 inference(scs_inference,[],[3733,3739,3753,3469,3614,3600,3731,3816,3822,3812,3735,3804,3802,256,259,226,167,257,233,258,168,225,165,253,152,164,163])).
% 61.18/61.35 cnf(3855,plain,
% 61.18/61.35 (P1(a22,a16,a22)),
% 61.18/61.35 inference(scs_inference,[],[3733,3739,3753,3759,3469,3614,3600,3731,3816,3822,3812,3735,3804,3802,256,259,226,167,257,233,258,168,225,165,253,152,164,163,151])).
% 61.18/61.35 cnf(3857,plain,
% 61.18/61.35 (P10(a16,a22,a16,a22)),
% 61.18/61.35 inference(scs_inference,[],[3733,3739,3753,3759,3774,3469,3614,3600,3731,3816,3822,3812,3735,3804,3802,256,259,226,167,257,233,258,168,225,165,253,152,164,163,151,166])).
% 61.18/61.35 cnf(3861,plain,
% 61.18/61.35 (P3(f30(a16,a16,a16,a16,a16),a16,f30(a16,a16,a16,a16,a16),f30(a16,a16,a16,a16,a16))),
% 61.18/61.35 inference(scs_inference,[],[3733,3739,3753,3649,3759,3774,3469,3614,3600,3731,3810,3816,3822,3812,3735,3804,3802,256,259,226,167,257,233,258,168,225,165,253,152,164,163,151,166,254,169])).
% 61.18/61.35 cnf(3865,plain,
% 61.18/61.35 (P1(x38651,x38652,x38652)),
% 61.18/61.35 inference(scs_inference,[],[3733,3739,3753,3649,3759,3765,3774,3469,3614,3600,3731,3810,3816,3822,3812,3735,3804,3802,256,259,226,167,257,233,258,168,225,165,253,152,164,163,151,166,254,169,224,160])).
% 61.18/61.35 cnf(3875,plain,
% 61.18/61.35 (P4(a16,f3(a16,a16,a16),a16,f3(a16,a16,a16))),
% 61.18/61.35 inference(scs_inference,[],[3733,3657,3739,3753,3649,3759,3765,3774,3469,3614,3616,3600,3731,3810,3816,3822,3812,3735,3804,3802,3661,3663,256,259,226,167,257,233,258,168,225,165,253,152,164,163,151,166,254,169,224,160,252,171,255,170,243])).
% 61.18/61.35 cnf(3879,plain,
% 61.18/61.35 (P4(a16,f30(a16,a16,a16,a16,a16),f30(a16,a16,a16,a16,a16),a16)),
% 61.18/61.35 inference(scs_inference,[],[3733,3657,3739,3753,3649,3759,3765,3774,3469,3614,3616,3600,3731,3810,3816,3822,3812,3735,3804,3802,3661,3663,256,259,226,167,257,233,258,168,225,165,253,152,164,163,151,166,254,169,224,160,252,171,255,170,243,263,183])).
% 61.18/61.35 cnf(3881,plain,
% 61.18/61.35 (P2(f8(a16,a16,a22),a16,a16,a22)),
% 61.18/61.35 inference(scs_inference,[],[3733,3657,3739,3753,3649,3759,3765,3774,3469,3614,3616,3600,3731,3810,3816,3822,3812,3735,3804,3802,3661,3663,256,259,226,167,257,233,258,168,225,165,253,152,164,163,151,166,254,169,224,160,252,171,255,170,243,263,183,191])).
% 61.18/61.35 cnf(3887,plain,
% 61.18/61.35 (P10(a16,f5(a16,a16,a22),a22,a16)),
% 61.18/61.35 inference(scs_inference,[],[3733,3657,3739,3753,3649,3737,3759,3765,3774,3469,3614,3616,3600,3731,3810,3816,3822,3812,3735,3804,3802,3661,3663,256,259,226,167,257,233,258,168,225,165,253,152,164,163,151,166,254,169,224,160,252,171,255,170,243,263,183,191,197,181,190])).
% 61.18/61.35 cnf(3889,plain,
% 61.18/61.35 (P10(a22,a20,a22,a20)),
% 61.18/61.35 inference(scs_inference,[],[3733,3657,3739,3753,3649,3737,3759,3765,3774,3469,3614,3616,3600,3731,3810,3816,3822,3812,3735,3804,3802,3661,3663,3702,256,259,226,167,257,233,258,168,225,165,253,152,164,163,151,166,254,169,224,160,252,171,255,170,243,263,183,191,197,181,190,241])).
% 61.18/61.35 cnf(3891,plain,
% 61.18/61.35 (P7(a16,f3(a16,a16,a16),f3(a16,a16,a16),a16,a16,f3(a16,a16,a16),f3(a16,a16,a16),a16)),
% 61.18/61.35 inference(scs_inference,[],[3733,3657,3739,3753,3649,3737,3759,3765,3774,3469,3614,3616,3600,3731,3810,3814,3816,3822,3812,3735,3804,3802,3661,3663,3702,256,259,226,167,257,233,258,168,225,165,253,152,164,163,151,166,254,169,224,160,252,171,255,170,243,263,183,191,197,181,190,241,223])).
% 61.18/61.35 cnf(3893,plain,
% 61.18/61.35 (P2(a16,f30(a16,a16,a16,a16,a16),a16,a16)),
% 61.18/61.35 inference(scs_inference,[],[3733,3657,3739,3753,3649,3737,3759,3765,3774,3469,3614,3616,3600,3731,3810,3814,3816,3822,3812,3735,3804,3802,3661,3663,3702,256,259,226,167,257,233,258,168,225,165,253,152,164,163,151,166,254,169,224,160,252,171,255,170,243,263,183,191,197,181,190,241,223,184])).
% 61.18/61.35 cnf(3895,plain,
% 61.18/61.35 (P9(a16,a16,a16,f30(a16,a16,a16,a16,a16))),
% 61.18/61.35 inference(scs_inference,[],[3733,3657,3739,3753,3649,3737,3759,3765,3774,3469,3614,3616,3600,3731,3810,3729,3814,3816,3822,3812,3735,3804,3802,3661,3663,3702,256,259,226,167,257,233,258,168,225,165,253,152,164,163,151,166,254,169,224,160,252,171,255,170,243,263,183,191,197,181,190,241,223,184,240])).
% 61.18/61.35 cnf(3896,plain,
% 61.18/61.35 (P9(x38961,x38962,x38961,x38962)),
% 61.18/61.35 inference(rename_variables,[],[3733])).
% 61.18/61.35 cnf(3898,plain,
% 61.18/61.35 (P10(a16,f4(a16,a16,a22),a22,a16)),
% 61.18/61.35 inference(scs_inference,[],[3733,3657,3739,3753,3649,3737,3759,3765,3774,3469,3614,3616,3600,3731,3810,3729,3814,3816,3822,3812,3735,3804,3802,3661,3663,3702,256,259,226,167,257,233,258,168,225,165,253,152,164,163,151,166,254,169,224,160,252,171,255,170,243,263,183,191,197,181,190,241,223,184,240,189])).
% 61.18/61.35 cnf(3900,plain,
% 61.18/61.35 (P1(f4(a16,a16,a22),a22,a16)),
% 61.18/61.35 inference(scs_inference,[],[3733,3657,3739,3753,3649,3737,3759,3765,3774,3469,3614,3616,3600,3731,3810,3729,3814,3816,3822,3812,3735,3804,3802,3661,3663,3702,256,259,226,167,257,233,258,168,225,165,253,152,164,163,151,166,254,169,224,160,252,171,255,170,243,263,183,191,197,181,190,241,223,184,240,189,177])).
% 61.18/61.35 cnf(3902,plain,
% 61.18/61.35 (P1(f5(a16,a16,a22),a22,a16)),
% 61.18/61.35 inference(scs_inference,[],[3733,3657,3739,3753,3649,3737,3759,3765,3774,3469,3614,3616,3600,3731,3810,3729,3814,3816,3822,3812,3735,3804,3802,3661,3663,3702,256,259,226,167,257,233,258,168,225,165,253,152,164,163,151,166,254,169,224,160,252,171,255,170,243,263,183,191,197,181,190,241,223,184,240,189,177,178])).
% 61.18/61.35 cnf(3906,plain,
% 61.18/61.35 (P3(f7(a16,a20,a22,a19),a22,a16,a16)),
% 61.18/61.35 inference(scs_inference,[],[3733,3657,3739,3753,3649,3737,3751,3759,3765,3774,3469,3614,3616,3600,3731,3810,3729,3814,3816,3822,3812,3735,3804,3802,3661,3606,3455,3663,3702,256,259,226,167,257,233,258,168,225,165,253,152,164,163,151,166,254,169,224,160,252,171,255,170,243,263,183,191,197,181,190,241,223,184,240,189,177,178,198,236])).
% 61.18/61.35 cnf(3911,plain,
% 61.18/61.35 (P7(a16,a22,a22,a22,a16,a22,a22,a22)),
% 61.18/61.35 inference(scs_inference,[],[3733,3896,3657,3739,3753,3649,3737,3751,3759,3765,3774,3469,3614,3616,3600,3731,3810,3729,3814,3816,3822,3812,3735,3804,3767,3802,3665,3661,3606,3455,3663,3702,256,259,226,167,257,233,258,168,225,165,253,152,164,163,151,166,254,169,224,160,252,171,255,170,243,263,183,191,197,181,190,241,223,184,240,189,177,178,198,236,242,228])).
% 61.18/61.35 cnf(3920,plain,
% 61.18/61.35 (P4(a22,a16,a22,f30(a16,a22,a16,a16,a16))),
% 61.18/61.35 inference(scs_inference,[],[3733,3896,3537,3657,3739,3753,3649,3737,3751,3759,3765,3774,3469,3614,3616,3600,3731,3810,3729,3814,3816,3822,3812,3735,3804,3767,3802,3665,3449,3661,3606,3455,3663,3702,256,259,226,167,257,233,258,168,225,165,253,152,164,163,151,166,254,169,224,160,252,171,255,170,243,263,183,191,197,181,190,241,223,184,240,189,177,178,198,236,242,228,206,207,220,200])).
% 61.18/61.35 cnf(3924,plain,
% 61.18/61.35 (~P6(x39241,a22,a22)+P4(a22,x39241,a16,x39241)),
% 61.18/61.35 inference(scs_inference,[],[3733,3896,3537,3657,3739,3753,3649,3737,3751,3759,3765,3774,3469,3614,3616,3600,3731,3810,3729,3814,3816,3822,3812,3735,3804,3767,3802,3665,3449,3661,3606,3455,3663,3702,256,259,226,167,257,233,258,168,225,165,253,152,164,163,151,166,254,169,224,160,252,171,255,170,243,263,183,191,197,181,190,241,223,184,240,189,177,178,198,236,242,228,206,207,220,200,262,174])).
% 61.18/61.35 cnf(3948,plain,
% 61.18/61.35 (P7(a16,a22,a16,a22,a22,a22,a22,a22)),
% 61.18/61.35 inference(scs_inference,[],[3911,3839,256,259])).
% 61.18/61.36 cnf(3952,plain,
% 61.18/61.36 (P4(f30(a16,a16,a16,a16,a16),a16,a16,f30(a16,a16,a16,a16,a16))),
% 61.18/61.36 inference(scs_inference,[],[3911,3720,3879,3839,256,259,226,167])).
% 61.18/61.36 cnf(3954,plain,
% 61.18/61.36 (P7(a22,a16,a22,a22,a16,a22,a22,a22)),
% 61.18/61.36 inference(scs_inference,[],[3911,3720,3879,3839,256,259,226,167,258])).
% 61.18/61.36 cnf(3956,plain,
% 61.18/61.36 (P8(x39561,x39562,x39563,x39564,x39562,x39561,x39563,x39564)),
% 61.18/61.36 inference(scs_inference,[],[3837,3911,3720,3879,3839,256,259,226,167,258,225])).
% 61.18/61.36 cnf(3960,plain,
% 61.18/61.36 (P4(a16,f30(a16,a16,a16,a16,a16),a16,f30(a16,a16,a16,a16,a16))),
% 61.18/61.36 inference(scs_inference,[],[3837,3911,3724,3720,3879,3839,256,259,226,167,258,225,165,168])).
% 61.18/61.36 cnf(3966,plain,
% 61.18/61.36 (P9(a16,a22,a16,f30(a16,a22,a16,a16,a16))),
% 61.18/61.36 inference(scs_inference,[],[3837,3755,3911,3724,3720,3879,3839,3853,256,259,226,167,258,225,165,168,257,253,164])).
% 61.18/61.36 cnf(3968,plain,
% 61.18/61.36 (P1(x39681,x39682,x39681)),
% 61.18/61.36 inference(scs_inference,[],[3837,3865,3755,3911,3724,3720,3879,3839,3853,256,259,226,167,258,225,165,168,257,253,164,151])).
% 61.18/61.36 cnf(3970,plain,
% 61.18/61.36 (P1(a22,a22,a16)),
% 61.18/61.36 inference(scs_inference,[],[3837,3865,3755,3855,3911,3724,3720,3879,3839,3853,256,259,226,167,258,225,165,168,257,253,164,151,152])).
% 61.18/61.36 cnf(3972,plain,
% 61.18/61.36 (P10(a22,a20,a20,a22)),
% 61.18/61.36 inference(scs_inference,[],[3837,3865,3755,3855,3889,3911,3724,3720,3879,3839,3853,256,259,226,167,258,225,165,168,257,253,164,151,152,166])).
% 61.18/61.36 cnf(3974,plain,
% 61.18/61.36 (P9(a16,f30(a16,a16,a16,a16,a16),a16,a16)),
% 61.18/61.36 inference(scs_inference,[],[3837,3865,3755,3855,3889,3911,3724,3720,3879,3895,3839,3853,256,259,226,167,258,225,165,168,257,253,164,151,152,166,163])).
% 61.18/61.36 cnf(3980,plain,
% 61.18/61.36 (P8(x39801,x39802,a22,a16,x39802,x39801,a16,a22)),
% 61.18/61.36 inference(scs_inference,[],[3837,3865,3847,3755,3855,3889,3911,3565,3724,3720,3879,3895,3906,3839,3853,256,259,226,167,258,225,165,168,257,253,164,151,152,166,163,169,224,254])).
% 61.18/61.36 cnf(3986,plain,
% 61.18/61.36 (P3(a16,a16,a18,f7(a16,a20,a22,a19))),
% 61.18/61.36 inference(scs_inference,[],[3837,3865,3847,3755,3855,3889,3911,3565,3724,3655,3720,3851,3879,3895,3906,3839,3853,256,259,226,167,258,225,165,168,257,253,164,151,152,166,163,169,224,254,160,252,170])).
% 61.18/61.36 cnf(3988,plain,
% 61.18/61.36 (P8(x39881,x39882,x39881,x39882,x39883,x39884,x39883,x39884)),
% 61.18/61.36 inference(scs_inference,[],[3837,3843,3865,3847,3755,3855,3889,3911,3565,3724,3655,3720,3851,3879,3895,3906,3839,3853,256,259,226,167,258,225,165,168,257,253,164,151,152,166,163,169,224,254,160,252,170,255])).
% 61.18/61.36 cnf(3990,plain,
% 61.18/61.36 (P4(f3(a16,a16,a16),a16,a16,a16)),
% 61.18/61.36 inference(scs_inference,[],[3837,3843,3865,3847,3755,3855,3889,3911,3565,3724,3655,3720,3851,3879,3895,3906,3839,3853,256,259,226,167,258,225,165,168,257,253,164,151,152,166,163,169,224,254,160,252,170,255,243])).
% 61.18/61.36 cnf(3992,plain,
% 61.18/61.36 (P9(a16,a16,f3(a16,a16,a16),f3(a16,a16,a16))),
% 61.18/61.36 inference(scs_inference,[],[3837,3843,3865,3847,3755,3855,3889,3911,3565,3724,3655,3720,3851,3879,3895,3906,3839,3853,3806,256,259,226,167,258,225,165,168,257,253,164,151,152,166,163,169,224,254,160,252,170,255,243,158])).
% 61.18/61.36 cnf(3996,plain,
% 61.18/61.36 (P9(f3(a16,a16,a16),f3(a16,a16,a16),a16,a16)),
% 61.18/61.36 inference(scs_inference,[],[3837,3843,3865,3847,3755,3855,3889,3911,3565,3724,3655,3720,3851,3879,3893,3895,3906,3839,3853,3806,3814,256,259,226,167,258,225,165,168,257,253,164,151,152,166,163,169,224,254,160,252,170,255,243,158,172,157])).
% 61.18/61.36 cnf(4004,plain,
% 61.18/61.36 (P2(a16,f3(a16,a16,a16),a16,a16)),
% 61.18/61.36 inference(scs_inference,[],[3837,3843,3865,3847,3755,3855,3889,3911,3565,3724,3655,3720,3851,3879,3875,3893,3895,3906,3839,3853,3806,3814,256,259,226,167,258,225,165,168,257,253,164,151,152,166,163,169,224,254,160,252,170,255,243,158,172,157,181,190,189,184])).
% 61.18/61.36 cnf(4008,plain,
% 61.18/61.36 (P1(f4(a22,a22,a20),a20,a22)),
% 61.18/61.36 inference(scs_inference,[],[3837,3843,3865,3847,3755,3855,3889,3911,3565,3724,3655,3720,3851,3879,3875,3893,3895,3906,3839,3853,3806,3814,3751,256,259,226,167,258,225,165,168,257,253,164,151,152,166,163,169,224,254,160,252,170,255,243,158,172,157,181,190,189,184,197,177])).
% 61.18/61.36 cnf(4014,plain,
% 61.18/61.36 (P1(a16,a16,f30(a16,a16,a16,a16,a16))),
% 61.18/61.36 inference(scs_inference,[],[3837,3843,3865,3847,3755,3855,3889,3911,3565,3724,3655,3720,3851,3879,3875,3893,3895,3906,3839,3853,3806,3814,3751,256,259,226,167,258,225,165,168,257,253,164,151,152,166,163,169,224,254,160,252,170,255,243,158,172,157,181,190,189,184,197,177,178,198,155])).
% 61.18/61.36 cnf(4015,plain,
% 61.18/61.36 (P1(x40151,x40152,x40152)),
% 61.18/61.36 inference(rename_variables,[],[3865])).
% 61.18/61.36 cnf(4017,plain,
% 61.18/61.36 (P3(x40171,x40172,x40172,x40172)),
% 61.18/61.36 inference(scs_inference,[],[3837,3843,3865,4015,3847,3755,3855,3889,3911,3565,3724,3655,3720,3851,3879,3875,3893,3895,3906,3839,3853,3806,3814,3751,256,259,226,167,258,225,165,168,257,253,164,151,152,166,163,169,224,254,160,252,170,255,243,158,172,157,181,190,189,184,197,177,178,198,155,236])).
% 61.18/61.36 cnf(4018,plain,
% 61.18/61.36 (P8(x40181,x40182,x40183,x40184,x40181,x40182,x40183,x40184)),
% 61.18/61.36 inference(rename_variables,[],[3843])).
% 61.18/61.36 cnf(4019,plain,
% 61.18/61.36 (P1(x40191,x40192,x40192)),
% 61.18/61.36 inference(rename_variables,[],[3865])).
% 61.18/61.36 cnf(4027,plain,
% 61.18/61.36 (P1(x40271,x40272,x40272)),
% 61.18/61.36 inference(rename_variables,[],[3865])).
% 61.18/61.36 cnf(4029,plain,
% 61.18/61.36 (P6(f3(a16,a16,a16),a16,a16)),
% 61.18/61.36 inference(scs_inference,[],[3837,3843,4018,3865,4015,4019,4027,3847,3755,3855,3889,3911,3565,3724,3655,3720,3851,3879,3779,3875,3833,3893,3895,3906,3839,3853,3806,3814,3751,3669,256,259,226,167,258,225,165,168,257,253,164,151,152,166,163,169,224,254,160,252,170,255,243,158,172,157,181,190,189,184,197,177,178,198,155,236,180,195,239,162])).
% 61.18/61.36 cnf(4033,plain,
% 61.18/61.36 (P6(f25(a16,x40331),a16,x40331)),
% 61.18/61.36 inference(scs_inference,[],[3837,3843,4018,3865,4015,4019,4027,3847,3755,3855,3889,3911,3565,3724,3655,3720,3851,3879,3779,3875,3833,3893,3895,3906,3839,3853,3806,3673,3814,3751,3669,256,259,226,167,258,225,165,168,257,253,164,151,152,166,163,169,224,254,160,252,170,255,243,158,172,157,181,190,189,184,197,177,178,198,155,236,180,195,239,162,159])).
% 61.18/61.36 cnf(4035,plain,
% 61.18/61.36 (P6(f3(a16,a16,a16),a19,a19)),
% 61.18/61.36 inference(scs_inference,[],[3837,3843,4018,3865,4015,4019,4027,3847,3755,3855,3889,3911,3565,3724,3655,3720,3851,3879,3779,3875,3833,3893,3895,3906,3839,3853,3806,3673,3814,3751,3669,256,259,226,167,258,225,165,168,257,253,164,151,152,166,163,169,224,254,160,252,170,255,243,158,172,157,181,190,189,184,197,177,178,198,155,236,180,195,239,162,159,1996])).
% 61.18/61.36 cnf(4039,plain,
% 61.18/61.36 (P4(f30(a16,a16,a16,a16,a16),f30(a16,a16,a16,a16,a16),f30(a16,a16,a16,a16,a16),f30(a16,a16,a16,a16,a16))),
% 61.18/61.36 inference(scs_inference,[],[3837,3843,4018,3865,4015,4019,4027,3847,3755,3855,3889,3911,3565,3724,3655,3720,3851,3879,3779,3875,3833,3893,3895,3906,3839,3853,3806,3673,3814,3751,3669,256,259,226,167,258,225,165,168,257,253,164,151,152,166,163,169,224,254,160,252,170,255,243,158,172,157,181,190,189,184,197,177,178,198,155,236,180,195,239,162,159,1996,2050,156])).
% 61.18/61.36 cnf(4041,plain,
% 61.18/61.36 (P6(f25(a16,x40411),x40411,a16)),
% 61.18/61.36 inference(scs_inference,[],[3837,3843,4018,3865,4015,4019,4027,3847,3755,3855,3889,3911,3565,3724,3655,3720,3851,3879,3779,3875,3833,3893,3895,3906,3839,3853,3806,3673,3814,3751,3669,256,259,226,167,258,225,165,168,257,253,164,151,152,166,163,169,224,254,160,252,170,255,243,158,172,157,181,190,189,184,197,177,178,198,155,236,180,195,239,162,159,1996,2050,156,154])).
% 61.18/61.36 cnf(4098,plain,
% 61.18/61.36 (P4(f3(a16,a16,a16),a16,f3(a16,a16,a16),a16)),
% 61.18/61.36 inference(scs_inference,[],[4029,156])).
% 61.18/61.36 cnf(4102,plain,
% 61.18/61.36 (P6(f25(a16,a16),a19,a19)),
% 61.18/61.36 inference(scs_inference,[],[3948,4029,4033,156,256,1996])).
% 61.18/61.36 cnf(4103,plain,
% 61.18/61.36 (P6(f25(a16,x41031),a16,x41031)),
% 61.18/61.36 inference(rename_variables,[],[4033])).
% 61.18/61.36 cnf(4106,plain,
% 61.18/61.36 (P6(f25(a16,x41061),a16,x41061)),
% 61.18/61.36 inference(rename_variables,[],[4033])).
% 61.18/61.36 cnf(4112,plain,
% 61.18/61.36 (P7(a22,a16,a16,a22,a22,a22,a22,a22)),
% 61.18/61.36 inference(scs_inference,[],[3948,3954,4029,4033,4103,3960,3920,156,256,1996,2050,226,167,259])).
% 61.18/61.36 cnf(4114,plain,
% 61.18/61.36 (P1(f25(a16,x41141),x41141,a16)),
% 61.18/61.36 inference(scs_inference,[],[3948,3954,4029,4033,4103,4041,3960,3920,156,256,1996,2050,226,167,259,153])).
% 61.18/61.36 cnf(4120,plain,
% 61.18/61.36 (P7(a22,a22,a22,a16,a22,a22,a16,a22)),
% 61.18/61.36 inference(scs_inference,[],[3948,3954,3891,4029,3992,4033,4103,4041,3960,3920,156,256,1996,2050,226,167,259,153,258,225,257])).
% 61.18/61.36 cnf(4122,plain,
% 61.18/61.36 (P4(f30(a16,a16,a16,a16,a16),a16,f30(a16,a16,a16,a16,a16),a16)),
% 61.18/61.36 inference(scs_inference,[],[3948,3954,3891,4029,3992,4033,4103,4041,3952,3960,3920,156,256,1996,2050,226,167,259,153,258,225,257,168])).
% 61.18/61.36 cnf(4124,plain,
% 61.18/61.36 (P10(a20,a22,a22,a20)),
% 61.18/61.36 inference(scs_inference,[],[3948,3954,3972,3891,4029,3992,4033,4103,4041,3952,3960,3920,156,256,1996,2050,226,167,259,153,258,225,257,168,165])).
% 61.18/61.36 cnf(4126,plain,
% 61.18/61.36 (P9(f30(a16,a22,a16,a16,a16),a16,a22,a16)),
% 61.18/61.36 inference(scs_inference,[],[3948,3954,3972,3891,4029,3992,4033,4103,4041,3952,3960,3920,3802,156,256,1996,2050,226,167,259,153,258,225,257,168,165,164])).
% 61.18/61.36 cnf(4128,plain,
% 61.18/61.36 (P8(x41281,x41282,x41283,x41284,x41281,x41282,x41284,x41283)),
% 61.18/61.36 inference(scs_inference,[],[3956,3948,3954,3972,3891,4029,3992,4033,4103,4041,3952,3960,3920,3802,156,256,1996,2050,226,167,259,153,258,225,257,168,165,164,253])).
% 61.18/61.36 cnf(4132,plain,
% 61.18/61.36 (P9(a16,f30(a16,a22,a16,a16,a16),a16,a22)),
% 61.18/61.36 inference(scs_inference,[],[3956,3948,3954,3972,3891,4029,3992,3785,4033,4103,4041,3952,3960,3966,3920,3802,156,256,1996,2050,226,167,259,153,258,225,257,168,165,164,253,166,163])).
% 61.18/61.36 cnf(4134,plain,
% 61.18/61.36 (P8(x41341,x41342,x41342,x41341,x41343,x41344,x41343,x41344)),
% 61.18/61.36 inference(scs_inference,[],[3956,3988,3948,3954,3972,3891,4029,3992,3785,4033,4103,4041,3952,3960,3966,3920,3802,156,256,1996,2050,226,167,259,153,258,225,257,168,165,164,253,166,163,254])).
% 61.18/61.36 cnf(4138,plain,
% 61.18/61.36 (P1(x41381,x41381,x41382)),
% 61.18/61.36 inference(scs_inference,[],[3956,3988,3968,3948,3954,3972,3891,4029,3992,3785,3900,4033,4103,4041,3952,3960,3966,3920,3802,156,256,1996,2050,226,167,259,153,258,225,257,168,165,164,253,166,163,254,151,152])).
% 61.18/61.36 cnf(4140,plain,
% 61.18/61.36 (P3(x41401,x41402,x41401,x41401)),
% 61.18/61.36 inference(scs_inference,[],[3956,3988,4017,3968,3948,3954,3972,3891,4029,3992,3785,3900,4033,4103,4041,3952,3960,3966,3920,3802,156,256,1996,2050,226,167,259,153,258,225,257,168,165,164,253,166,163,254,151,152,169])).
% 61.18/61.36 cnf(4146,plain,
% 61.18/61.36 (P8(x41461,x41462,a16,a22,x41462,x41461,a22,a16)),
% 61.18/61.36 inference(scs_inference,[],[3956,3988,4017,3968,3980,3948,3954,3972,3891,4029,3992,3785,3900,4033,4103,4041,3952,3960,3966,3920,3667,3802,156,256,1996,2050,226,167,259,153,258,225,257,168,165,164,253,166,163,254,151,152,169,224,160,252])).
% 61.18/61.36 cnf(4148,plain,
% 61.18/61.36 (P3(f30(a16,a16,a16,a16,a16),f30(a16,a16,a16,a16,a16),a16,f30(a16,a16,a16,a16,a16))),
% 61.18/61.36 inference(scs_inference,[],[3956,3988,4017,3968,3980,3948,3954,3972,3891,4029,3992,3785,3900,3861,4033,4103,4041,3952,3960,3966,3920,3667,3802,156,256,1996,2050,226,167,259,153,258,225,257,168,165,164,253,166,163,254,151,152,169,224,160,252,170])).
% 61.18/61.36 cnf(4152,plain,
% 61.18/61.36 (P3(a16,a18,f7(a16,a20,a22,a19),f7(a16,a20,a22,a19))),
% 61.18/61.36 inference(scs_inference,[],[3956,3988,4017,3968,3980,3948,3954,3972,3891,3986,4029,3992,3785,3900,3861,4033,4103,4041,3952,3960,3966,3920,3667,3802,156,256,1996,2050,226,167,259,153,258,225,257,168,165,164,253,166,163,254,151,152,169,224,160,252,170,255,185])).
% 61.18/61.36 cnf(4154,plain,
% 61.18/61.36 (P10(a20,a22,a20,a22)),
% 61.18/61.36 inference(scs_inference,[],[3956,3988,4017,3968,3980,3948,3954,3972,3891,3986,4029,3992,3785,3900,3861,4033,4103,4041,3952,3960,3966,3920,3667,3802,156,256,1996,2050,226,167,259,153,258,225,257,168,165,164,253,166,163,254,151,152,169,224,160,252,170,255,185,241])).
% 61.18/61.36 cnf(4155,plain,
% 61.18/61.36 (P8(x41551,x41552,x41553,x41554,x41552,x41551,x41553,x41554)),
% 61.18/61.36 inference(rename_variables,[],[3956])).
% 61.18/61.36 cnf(4161,plain,
% 61.18/61.36 (P9(a22,a16,a16,f30(a16,a22,a16,a16,a16))),
% 61.18/61.36 inference(scs_inference,[],[3956,4155,3988,4017,3968,3980,3948,3954,3972,4039,3891,3986,4029,3992,3785,3900,3861,4033,4103,4041,3952,3960,3966,3920,3667,3802,156,256,1996,2050,226,167,259,153,258,225,257,168,165,164,253,166,163,254,151,152,169,224,160,252,170,255,185,241,181,189,240])).
% 61.18/61.36 cnf(4162,plain,
% 61.18/61.36 (P8(x41621,x41622,x41623,x41624,x41622,x41621,x41623,x41624)),
% 61.18/61.36 inference(rename_variables,[],[3956])).
% 61.18/61.36 cnf(4165,plain,
% 61.18/61.36 (P1(x41651,x41652,x41651)),
% 61.18/61.36 inference(rename_variables,[],[3968])).
% 61.18/61.36 cnf(4168,plain,
% 61.18/61.36 (P1(x41681,x41682,x41681)),
% 61.18/61.36 inference(rename_variables,[],[3968])).
% 61.18/61.36 cnf(4172,plain,
% 61.18/61.36 (P7(f3(a16,a16,a16),a16,a16,a16,f3(a16,a16,a16),a16,a16,a16)),
% 61.18/61.36 inference(scs_inference,[],[3956,4155,3988,4017,3968,4165,3980,3948,3954,3972,4039,3891,3986,4029,3992,3785,3900,3861,4033,4103,4041,3952,3960,4004,3966,3920,3667,3802,156,256,1996,2050,226,167,259,153,258,225,257,168,165,164,253,166,163,254,151,152,169,224,160,252,170,255,185,241,181,189,240,172,197,190,223])).
% 61.18/61.36 cnf(4178,plain,
% 61.18/61.36 (P10(f4(a16,a16,a16),a16,a16,a16)),
% 61.18/61.36 inference(scs_inference,[],[3956,4155,3988,4017,3968,4165,3980,3948,3954,3972,4039,3712,3891,3986,4029,3992,3785,3900,3861,4033,4103,4041,3952,3960,4004,3966,3920,3667,3802,3837,156,256,1996,2050,226,167,259,153,258,225,257,168,165,164,253,166,163,254,151,152,169,224,160,252,170,255,185,241,181,189,240,172,197,190,223,177,184,182])).
% 61.18/61.36 cnf(4179,plain,
% 61.18/61.36 (P9(x41791,x41792,x41792,x41791)),
% 61.18/61.36 inference(rename_variables,[],[3837])).
% 61.18/61.36 cnf(4184,plain,
% 61.18/61.36 (P1(x41841,x41842,x41841)),
% 61.18/61.36 inference(rename_variables,[],[3968])).
% 61.18/61.36 cnf(4188,plain,
% 61.18/61.36 (P9(a16,f30(a16,a16,a16,a16,a16),f3(a16,a16,a16),f3(a16,a16,a16))),
% 61.18/61.36 inference(scs_inference,[],[3956,4155,3988,4017,3968,4165,4168,3980,3948,3954,3972,4039,3712,3891,3986,4029,3992,3785,3900,3861,4033,4103,4041,3952,3960,4004,3974,3966,3920,3667,3802,3837,156,256,1996,2050,226,167,259,153,258,225,257,168,165,164,253,166,163,254,151,152,169,224,160,252,170,255,185,241,181,189,240,172,197,190,223,177,184,182,178,198,227,179])).
% 61.18/61.36 cnf(4190,plain,
% 61.18/61.36 (P3(a15,a15,a1,a2)),
% 61.18/61.36 inference(scs_inference,[],[142,3956,4155,3988,4017,3968,4165,4168,3980,3948,3954,3972,4039,3712,3891,3986,4029,3992,3785,3900,3861,4033,4103,4041,3952,3960,4004,3974,3966,3920,3667,3802,3837,156,256,1996,2050,226,167,259,153,258,225,257,168,165,164,253,166,163,254,151,152,169,224,160,252,170,255,185,241,181,189,240,172,197,190,223,177,184,182,178,198,227,179,236])).
% 61.18/61.36 cnf(4195,plain,
% 61.18/61.36 (P3(x41951,x41952,x41952,x41952)),
% 61.18/61.36 inference(rename_variables,[],[4017])).
% 61.18/61.36 cnf(4197,plain,
% 61.18/61.36 (P6(a16,a16,a16)),
% 61.18/61.36 inference(scs_inference,[],[142,3956,4155,4162,3988,4017,3968,4165,4168,4184,3980,3948,3954,3972,4039,3712,3891,3986,4029,3992,3785,3900,3861,4033,4103,4041,3952,3960,4035,4004,3974,3966,3920,3667,3671,3802,3837,4179,156,256,1996,2050,226,167,259,153,258,225,257,168,165,164,253,166,163,254,151,152,169,224,160,252,170,255,185,241,181,189,240,172,197,190,223,177,184,182,178,198,227,179,236,192,239])).
% 61.18/61.36 cnf(4198,plain,
% 61.18/61.36 (P8(x41981,x41982,x41983,x41984,x41982,x41981,x41983,x41984)),
% 61.18/61.36 inference(rename_variables,[],[3956])).
% 61.18/61.36 cnf(4199,plain,
% 61.18/61.36 (P1(x41991,x41992,x41991)),
% 61.18/61.36 inference(rename_variables,[],[3968])).
% 61.18/61.36 cnf(4202,plain,
% 61.18/61.36 (P3(x42021,x42022,x42022,x42022)),
% 61.18/61.36 inference(rename_variables,[],[4017])).
% 61.18/61.36 cnf(4204,plain,
% 61.18/61.36 (P6(a16,a16,f30(a16,a16,a16,a16,a16))),
% 61.18/61.36 inference(scs_inference,[],[142,3956,4155,4162,3988,4017,4195,3968,4165,4168,4184,3980,3948,3954,3972,4039,3712,3891,3986,4029,3992,3785,3900,3861,4033,4103,4041,3952,3960,4035,4014,4004,3974,3990,3966,3920,3667,3671,3895,3802,3837,4179,156,256,1996,2050,226,167,259,153,258,225,257,168,165,164,253,166,163,254,151,152,169,224,160,252,170,255,185,241,181,189,240,172,197,190,223,177,184,182,178,198,227,179,236,192,239,195,162])).
% 61.18/61.36 cnf(4206,plain,
% 61.18/61.36 (P4(x42061,x42061,x42061,x42061)),
% 61.18/61.36 inference(scs_inference,[],[142,3956,4155,4162,4198,3988,4017,4195,4202,3968,4165,4168,4184,3980,3948,3954,3972,4039,3712,3891,3986,4029,3992,3785,3900,3861,4033,4103,4041,3952,3960,4035,4014,4004,3974,3990,3966,3920,3667,3671,3895,3802,3837,4179,156,256,1996,2050,226,167,259,153,258,225,257,168,165,164,253,166,163,254,151,152,169,224,160,252,170,255,185,241,181,189,240,172,197,190,223,177,184,182,178,198,227,179,236,192,239,195,162,251])).
% 61.18/61.36 cnf(4212,plain,
% 61.18/61.36 (P6(f25(a22,x42121),a22,x42121)),
% 61.18/61.36 inference(scs_inference,[],[142,3956,4155,4162,4198,3988,4017,4195,4202,3968,4165,4168,4184,4199,3980,3948,3954,3970,3972,4039,3712,3891,3986,4029,3992,3785,3900,3861,4033,4103,4041,3952,3960,4035,4014,4004,3974,3990,3966,3920,3667,3671,3895,3802,3837,4179,156,256,1996,2050,226,167,259,153,258,225,257,168,165,164,253,166,163,254,151,152,169,224,160,252,170,255,185,241,181,189,240,172,197,190,223,177,184,182,178,198,227,179,236,192,239,195,162,251,159])).
% 61.18/61.36 cnf(4215,plain,
% 61.18/61.36 (P1(x42151,x42152,x42151)),
% 61.18/61.36 inference(rename_variables,[],[3968])).
% 61.18/61.36 cnf(4217,plain,
% 61.18/61.36 (P4(a22,f25(a22,a22),a16,f25(a22,a22))),
% 61.18/61.36 inference(scs_inference,[],[142,3956,4155,4162,4198,3988,4017,4195,4202,3968,4165,4168,4184,4199,3980,3948,3954,3970,3972,4039,3712,3891,3986,4029,3992,3785,3900,3861,4033,4103,4041,3952,3960,4035,4014,4004,3974,3990,3966,3920,3667,3671,3895,3802,3837,4179,156,256,1996,2050,226,167,259,153,258,225,257,168,165,164,253,166,163,254,151,152,169,224,160,252,170,255,185,241,181,189,240,172,197,190,223,177,184,182,178,198,227,179,236,192,239,195,162,251,159,3924])).
% 61.18/61.36 cnf(4219,plain,
% 61.18/61.36 (P6(a16,f30(a16,a16,a16,a16,a16),a16)),
% 61.18/61.36 inference(scs_inference,[],[142,3956,4155,4162,4198,3988,4017,4195,4202,3968,4165,4168,4184,4199,3980,3948,3954,3970,3972,4039,3712,3891,3986,4029,3992,3785,3900,3861,4033,4103,4041,3952,3960,4035,4014,4004,3974,3990,3966,3920,3667,3671,3895,3802,3837,4179,156,256,1996,2050,226,167,259,153,258,225,257,168,165,164,253,166,163,254,151,152,169,224,160,252,170,255,185,241,181,189,240,172,197,190,223,177,184,182,178,198,227,179,236,192,239,195,162,251,159,3924,154])).
% 61.18/61.36 cnf(4228,plain,
% 61.18/61.36 (P9(f28(a16,a16,a16,a16,a16,a16),a16,a16,a16)),
% 61.18/61.36 inference(scs_inference,[],[142,3956,4155,4162,4198,3988,4017,4195,4202,3968,4165,4168,4184,4199,4215,3980,3948,3954,3970,3972,4039,3712,3891,3986,4029,3992,3785,3900,3861,4033,4103,4041,3952,3960,4035,4014,4004,3974,3990,3966,3920,3667,3671,3895,3802,3837,4179,156,256,1996,2050,226,167,259,153,258,225,257,168,165,164,253,166,163,254,151,152,169,224,160,252,170,255,185,241,181,189,240,172,197,190,223,177,184,182,178,198,227,179,236,192,239,195,162,251,159,3924,154,171,754,201,204])).
% 61.18/61.36 cnf(4232,plain,
% 61.18/61.36 (P4(a16,a22,a16,a22)),
% 61.18/61.36 inference(scs_inference,[],[142,3956,4155,4162,4198,3988,4017,4195,4202,3968,4165,4168,4184,4199,4215,3980,3948,3954,3970,3972,4039,3712,3891,3986,4029,3992,3785,3900,3861,4033,4103,4041,3952,3960,4035,4014,4004,3974,3990,3966,3920,3667,3671,3895,3802,3837,4179,156,256,1996,2050,226,167,259,153,258,225,257,168,165,164,253,166,163,254,151,152,169,224,160,252,170,255,185,241,181,189,240,172,197,190,223,177,184,182,178,198,227,179,236,192,239,195,162,251,159,3924,154,171,754,201,204,199,243])).
% 61.18/61.36 cnf(4234,plain,
% 61.18/61.36 (P6(f28(a16,a16,a16,a16,a16,a16),a16,a16)),
% 61.18/61.36 inference(scs_inference,[],[142,3956,4155,4162,4198,3988,4017,4195,4202,3968,4165,4168,4184,4199,4215,3980,3948,3954,3970,3972,4039,3712,3891,3986,4029,3992,3785,3900,3861,4033,4103,4041,3952,3960,4035,4014,4004,3974,3990,3966,3920,3667,3671,3895,3802,3837,4179,156,256,1996,2050,226,167,259,153,258,225,257,168,165,164,253,166,163,254,151,152,169,224,160,252,170,255,185,241,181,189,240,172,197,190,223,177,184,182,178,198,227,179,236,192,239,195,162,251,159,3924,154,171,754,201,204,199,243,203])).
% 61.18/61.36 cnf(4236,plain,
% 61.18/61.36 (P6(f6(a22,a16,a16),a22,a16)),
% 61.18/61.36 inference(scs_inference,[],[142,3956,4155,4162,4198,3988,4017,4195,4202,3968,4165,4168,4184,4199,4215,3980,3948,3954,3970,3972,4039,3712,3891,3986,4029,3992,3785,3900,3861,4033,4103,4106,4041,3952,3960,4035,4014,4004,3974,3990,3966,3920,3667,3671,3857,3895,3802,3837,4179,3702,156,256,1996,2050,226,167,259,153,258,225,257,168,165,164,253,166,163,254,151,152,169,224,160,252,170,255,185,241,181,189,240,172,197,190,223,177,184,182,178,198,227,179,236,192,239,195,162,251,159,3924,154,171,754,201,204,199,243,203,186])).
% 61.18/61.36 cnf(4239,plain,
% 61.18/61.36 (P6(f3(a16,a16,a16),a16,f30(a16,a16,a16,a16,a16))),
% 61.18/61.36 inference(scs_inference,[],[142,3956,4155,4162,4198,3988,4017,4195,4202,3968,4165,4168,4184,4199,4215,3980,3948,3954,3970,3972,4039,3712,3891,3986,4029,3992,3785,3900,3861,4033,4103,4106,4041,3952,3960,4035,4014,4004,3974,3990,3966,3920,3667,3671,3857,3895,3802,3837,4179,3702,156,256,1996,2050,226,167,259,153,258,225,257,168,165,164,253,166,163,254,151,152,169,224,160,252,170,255,185,241,181,189,240,172,197,190,223,177,184,182,178,198,227,179,236,192,239,195,162,251,159,3924,154,171,754,201,204,199,243,203,186,175])).
% 61.18/61.36 cnf(4250,plain,
% 61.18/61.36 (P8(x42501,x42502,x42503,x42504,x42501,x42502,x42504,x42503)),
% 61.18/61.36 inference(rename_variables,[],[4128])).
% 61.18/61.36 cnf(4253,plain,
% 61.18/61.36 (P8(x42531,x42532,x42533,x42534,x42531,x42532,x42534,x42533)),
% 61.18/61.36 inference(rename_variables,[],[4128])).
% 61.18/61.36 cnf(4257,plain,
% 61.18/61.36 (P6(a16,a19,a19)),
% 61.18/61.36 inference(scs_inference,[],[4128,4250,4197,4239,1841,1701,156,1996])).
% 61.18/61.36 cnf(4260,plain,
% 61.18/61.36 (P8(x42601,x42602,x42603,x42604,x42601,x42602,x42604,x42603)),
% 61.18/61.36 inference(rename_variables,[],[4128])).
% 61.18/61.36 cnf(4262,plain,
% 61.18/61.36 (P8(a16,a19,a19,a19,a19,a19,a16,a19)),
% 61.18/61.36 inference(scs_inference,[],[4128,4250,4253,4197,4239,1841,1701,156,1996,1878,2050])).
% 61.18/61.36 cnf(4264,plain,
% 61.18/61.36 (P6(f3(a16,a16,a16),f30(a16,a16,a16,a16,a16),a16)),
% 61.18/61.36 inference(scs_inference,[],[4128,4250,4253,4197,4239,1841,1701,156,1996,1878,2050,154])).
% 61.18/61.36 cnf(4266,plain,
% 61.18/61.36 (P7(a22,a22,a22,a22,a22,a16,a16,a22)),
% 61.18/61.36 inference(scs_inference,[],[4128,4250,4253,4112,4197,4239,1841,1701,156,1996,1878,2050,154,256])).
% 61.18/61.36 cnf(4268,plain,
% 61.18/61.36 (P8(a16,a22,a22,a22,a22,a22,a16,a22)),
% 61.18/61.36 inference(scs_inference,[],[4128,4250,4253,4112,4197,4232,4239,1841,1701,156,1996,1878,2050,154,256,226])).
% 61.18/61.36 cnf(4274,plain,
% 61.18/61.36 (P7(f3(a16,a16,a16),a16,a16,f3(a16,a16,a16),a16,a16,a16,a16)),
% 61.18/61.36 inference(scs_inference,[],[4128,4250,4253,4112,4197,4232,4172,3827,4239,4217,1841,1701,156,1996,1878,2050,154,256,226,167,259,258])).
% 61.18/61.36 cnf(4278,plain,
% 61.18/61.36 (P7(a16,a22,a22,a16,a22,a22,a22,a22)),
% 61.18/61.36 inference(scs_inference,[],[4128,4250,4253,4112,4197,4232,4172,3827,4239,4217,1841,1701,156,1996,1878,2050,154,256,226,167,259,258,153,257])).
% 61.18/61.36 cnf(4280,plain,
% 61.18/61.36 (P8(a16,a16,x42801,x42802,f30(a16,a16,a16,a16,a16),a16,x42801,x42802)),
% 61.18/61.36 inference(scs_inference,[],[4128,4250,4253,4112,4197,4232,3743,4172,3827,4239,4217,1841,1701,156,1996,1878,2050,154,256,226,167,259,258,153,257,225])).
% 61.18/61.36 cnf(4288,plain,
% 61.18/61.36 (P10(a16,a16,a16,f5(a16,a16,a16))),
% 61.18/61.36 inference(scs_inference,[],[4128,4250,4253,4112,4146,4197,4232,3708,3743,4172,3827,4239,4217,4161,1841,1701,156,1996,1878,2050,154,256,226,167,259,258,153,257,225,164,253,168,165])).
% 61.18/61.36 cnf(4290,plain,
% 61.18/61.36 (P8(x42901,x42902,x42903,x42904,x42902,x42901,x42904,x42903)),
% 61.18/61.36 inference(scs_inference,[],[4128,4250,4253,4260,4112,4146,4197,4232,3708,3743,4172,3827,4239,4217,4161,1841,1701,156,1996,1878,2050,154,256,226,167,259,258,153,257,225,164,253,168,165,254])).
% 61.18/61.36 cnf(4292,plain,
% 61.18/61.36 (P9(a16,a16,f28(a16,a16,a16,a16,a16,a16),a16)),
% 61.18/61.36 inference(scs_inference,[],[4128,4250,4253,4260,4112,4146,4197,4232,3708,3743,4172,3827,4228,4239,4217,4161,1841,1701,156,1996,1878,2050,154,256,226,167,259,258,153,257,225,164,253,168,165,254,163])).
% 61.18/61.36 cnf(4302,plain,
% 61.18/61.36 (P8(x43021,x43022,x43021,x43022,x43023,x43024,x43024,x43023)),
% 61.18/61.36 inference(scs_inference,[],[4128,4250,4253,4260,4134,4112,4146,4197,4232,3708,3789,3781,3743,4172,3827,4228,4239,4217,4161,4132,1841,1701,156,1996,1878,2050,154,256,226,167,259,258,153,257,225,164,253,168,165,254,163,152,166,151,160,252])).
% 61.18/61.36 cnf(4308,plain,
% 61.18/61.36 (P3(a15,a15,a2,a1)),
% 61.18/61.36 inference(scs_inference,[],[4128,4250,4253,4260,4134,4112,4190,4146,4197,4232,3708,3789,3781,3743,4172,3827,4228,4239,4152,4217,4161,4132,3569,1841,1701,156,1996,1878,2050,154,256,226,167,259,258,153,257,225,164,253,168,165,254,163,152,166,151,160,252,169,224,171])).
% 61.18/61.36 cnf(4310,plain,
% 61.18/61.36 (P3(x43101,x43101,x43102,x43101)),
% 61.18/61.36 inference(scs_inference,[],[4128,4250,4253,4260,4134,4140,4112,4190,4146,4197,4232,3708,3789,3781,3743,4172,3827,4228,4239,4152,4217,4161,4132,3569,1841,1701,156,1996,1878,2050,154,256,226,167,259,258,153,257,225,164,253,168,165,254,163,152,166,151,160,252,169,224,171,170])).
% 61.18/61.36 cnf(4317,plain,
% 61.18/61.36 (P4(x43171,x43171,x43171,x43171)),
% 61.18/61.36 inference(rename_variables,[],[4206])).
% 61.18/61.36 cnf(4321,plain,
% 61.18/61.36 (P2(f8(a20,a20,a22),a20,a20,a22)),
% 61.18/61.36 inference(scs_inference,[],[4206,4128,4250,4253,4260,4134,4140,4112,4190,4146,4124,4197,4232,3708,3789,3781,3743,4172,3827,4228,4239,4152,4217,4178,4161,4132,3569,3751,1841,1701,156,1996,1878,2050,154,256,226,167,259,258,153,257,225,164,253,168,165,254,163,152,166,151,160,252,169,224,171,170,255,188,200,173,191])).
% 61.18/61.36 cnf(4326,plain,
% 61.18/61.36 (P4(x43261,x43261,x43261,x43261)),
% 61.18/61.36 inference(rename_variables,[],[4206])).
% 61.18/61.36 cnf(4330,plain,
% 61.18/61.36 (P9(f28(a19,a19,a19,a19,a16,a16),a16,a19,a19)),
% 61.18/61.36 inference(scs_inference,[],[4206,4317,4128,4250,4253,4260,4134,4140,4112,4190,4146,4124,4197,4232,3708,3789,3781,3743,4172,3827,4228,4239,4152,4217,4178,4161,4132,3569,3779,3751,3669,1841,1701,156,1996,1878,2050,154,256,226,167,259,258,153,257,225,164,253,168,165,254,163,152,166,151,160,252,169,224,171,170,255,188,200,173,191,176,201,229,205])).
% 61.18/61.36 cnf(4335,plain,
% 61.18/61.36 (P4(x43351,x43351,x43351,x43351)),
% 61.18/61.36 inference(rename_variables,[],[4206])).
% 61.18/61.36 cnf(4337,plain,
% 61.18/61.36 (P4(a22,a16,a16,a22)),
% 61.18/61.36 inference(scs_inference,[],[4206,4317,4326,4335,4128,4250,4253,4260,4134,4140,4112,4190,4146,4124,4197,4232,3708,3789,3781,3743,4172,3827,4228,4239,4152,4217,4178,4161,4132,3569,3779,3751,3669,1841,1701,156,1996,1878,2050,154,256,226,167,259,258,153,257,225,164,253,168,165,254,163,152,166,151,160,252,169,224,171,170,255,188,200,173,191,176,201,229,205,181,199,243])).
% 61.18/61.36 cnf(4338,plain,
% 61.18/61.36 (P4(x43381,x43381,x43381,x43381)),
% 61.18/61.36 inference(rename_variables,[],[4206])).
% 61.18/61.36 cnf(4340,plain,
% 61.18/61.36 (P10(x43401,x43402,x43402,x43401)),
% 61.18/61.36 inference(scs_inference,[],[4206,4317,4326,4335,4128,4250,4253,4260,4134,4140,4112,4154,4190,4146,4124,4197,4232,3708,3789,3781,3743,4172,3827,4228,4239,4152,4217,4178,4161,4132,3569,3779,3751,3669,1841,1701,156,1996,1878,2050,154,256,226,167,259,258,153,257,225,164,253,168,165,254,163,152,166,151,160,252,169,224,171,170,255,188,200,173,191,176,201,229,205,181,199,243,241])).
% 61.18/61.36 cnf(4343,plain,
% 61.18/61.36 (P7(f3(a16,a16,a16),a16,a16,f30(a16,a16,a16,a16,a16),f3(a16,a16,a16),a16,a16,f30(a16,a16,a16,a16,a16))),
% 61.18/61.36 inference(scs_inference,[],[4206,4317,4326,4335,4128,4250,4253,4260,4134,4140,4112,4154,4190,4146,4124,4197,4232,3708,3789,3781,3743,4172,3827,4228,4239,4152,4217,4178,4161,4132,3569,3779,3751,3669,1841,1701,156,1996,1878,2050,154,256,226,167,259,258,153,257,225,164,253,168,165,254,163,152,166,151,160,252,169,224,171,170,255,188,200,173,191,176,201,229,205,181,199,243,241,223])).
% 61.18/61.36 cnf(4351,plain,
% 61.18/61.36 (P2(x43511,x43511,x43511,x43511)),
% 61.18/61.36 inference(scs_inference,[],[142,4206,4317,4326,4335,4338,4128,4250,4253,4260,4134,4140,4112,4154,4190,4146,4124,4197,4232,3708,3789,3781,3743,4172,3827,4228,4239,4152,4217,4178,4161,4132,3569,3779,3751,3669,1841,1701,156,1996,1878,2050,154,256,226,167,259,258,153,257,225,164,253,168,165,254,163,152,166,151,160,252,169,224,171,170,255,188,200,173,191,176,201,229,205,181,199,243,241,223,190,189,197,184])).
% 61.18/61.36 cnf(4360,plain,
% 61.18/61.36 (P3(x43601,x43602,x43603,x43603)),
% 61.18/61.36 inference(scs_inference,[],[142,4206,4317,4326,4335,4338,4128,4250,4253,4260,4134,4140,4138,4112,4154,4190,4146,4124,4197,4232,3708,3881,3789,3781,3743,4172,3827,4228,4239,4152,4217,4178,4161,4132,3569,4033,3779,3843,3751,3669,1841,1701,156,1996,1878,2050,154,256,226,167,259,258,153,257,225,164,253,168,165,254,163,152,166,151,160,252,169,224,171,170,255,188,200,173,191,176,201,229,205,181,199,243,241,223,190,189,197,184,203,198,227,236])).
% 61.18/61.36 cnf(4372,plain,
% 61.18/61.36 (P6(f30(a16,a16,a16,a16,a16),a16,a16)),
% 61.18/61.36 inference(scs_inference,[],[142,4206,4317,4326,4335,4338,4128,4250,4253,4260,4134,4140,4138,4112,4154,4190,4146,4124,4197,4232,3708,3881,3789,3781,3743,4172,3827,4122,4228,4148,4239,4152,4217,4178,4161,4132,3569,4033,3779,4017,3865,3974,3733,3843,3751,3669,1841,1701,156,1996,1878,2050,154,256,226,167,259,258,153,257,225,164,253,168,165,254,163,152,166,151,160,252,169,224,171,170,255,188,200,173,191,176,201,229,205,181,199,243,241,223,190,189,197,184,203,198,227,236,192,195,186,162])).
% 61.18/61.36 cnf(4375,plain,
% 61.18/61.36 (P4(a15,a15,a2,a2)),
% 61.18/61.36 inference(scs_inference,[],[142,4206,4317,4326,4335,4338,4128,4250,4253,4260,4134,4140,4138,4112,4154,4190,4146,4124,4197,4232,3708,3881,3789,3781,3743,4172,3827,4122,4228,4148,4239,4152,4217,4178,4161,4132,3569,4033,3779,3988,4017,3865,3974,3733,3843,3751,3669,1841,1701,156,1996,1878,2050,154,256,226,167,259,258,153,257,225,164,253,168,165,254,163,152,166,151,160,252,169,224,171,170,255,188,200,173,191,176,201,229,205,181,199,243,241,223,190,189,197,184,203,198,227,236,192,195,186,162,251])).
% 61.18/61.36 cnf(4378,plain,
% 61.18/61.36 (P6(f25(a19,x43781),a19,x43781)),
% 61.18/61.36 inference(scs_inference,[],[142,4206,4317,4326,4335,4338,4128,4250,4253,4260,4134,4140,4138,4112,4154,4190,4146,4124,4197,4232,3708,3881,3789,3781,3743,4172,3827,4122,4228,4148,4239,4152,4217,4178,4161,4132,4102,3569,4033,3779,3988,4017,3865,3974,3733,3843,3751,3669,1841,1701,156,1996,1878,2050,154,256,226,167,259,258,153,257,225,164,253,168,165,254,163,152,166,151,160,252,169,224,171,170,255,188,200,173,191,176,201,229,205,181,199,243,241,223,190,189,197,184,203,198,227,236,192,195,186,162,251,159])).
% 61.18/61.36 cnf(4381,plain,
% 61.18/61.36 (P6(f28(a19,a19,a19,a19,a16,a16),a16,a16)),
% 61.18/61.36 inference(scs_inference,[],[142,4206,4317,4326,4335,4338,4128,4250,4253,4260,4134,4140,4138,4112,4154,4190,4146,4124,4197,4232,3708,3881,3789,3781,3743,4172,3827,4122,4228,4148,4239,4152,4217,4178,4161,4132,4102,3569,4033,3779,3988,4017,3865,3974,3733,3843,3751,3669,1841,1701,156,1996,1878,2050,154,256,226,167,259,258,153,257,225,164,253,168,165,254,163,152,166,151,160,252,169,224,171,170,255,188,200,173,191,176,201,229,205,181,199,243,241,223,190,189,197,184,203,198,227,236,192,195,186,162,251,159,1989])).
% 61.18/61.36 cnf(4392,plain,
% 61.18/61.36 (P3(x43921,x43922,x43923,x43923)),
% 61.18/61.36 inference(rename_variables,[],[4360])).
% 61.18/61.36 cnf(4393,plain,
% 61.18/61.36 (P4(a16,a19,a16,a19)),
% 61.18/61.36 inference(scs_inference,[],[4360,4257,3824,156])).
% 61.18/61.36 cnf(4402,plain,
% 61.18/61.36 (P8(x44021,x44022,x44023,x44024,x44022,x44021,x44024,x44023)),
% 61.18/61.36 inference(rename_variables,[],[4290])).
% 61.18/61.36 cnf(4410,plain,
% 61.18/61.36 (P6(f25(a22,x44101),x44101,a22)),
% 61.18/61.36 inference(scs_inference,[],[4290,4360,4120,4257,4098,4234,4212,4378,3824,156,1996,2,1989,1878,2050,256,226,154])).
% 61.18/61.36 cnf(4412,plain,
% 61.18/61.36 (P10(f7(x44121,x44121,x44121,x44121),x44121,x44121,x44121)),
% 61.18/61.36 inference(scs_inference,[],[4351,4290,4360,4120,4257,4098,4234,4212,4378,3824,156,1996,2,1989,1878,2050,256,226,154,187])).
% 61.18/61.36 cnf(4420,plain,
% 61.18/61.36 (P8(f30(a16,a22,a16,a16,a16),a16,x44201,x44202,a22,a16,x44201,x44202)),
% 61.18/61.36 inference(scs_inference,[],[4351,4290,4360,4266,4120,4257,4278,4375,4126,4098,4234,4212,4378,3824,156,1996,2,1989,1878,2050,256,226,154,187,259,167,257,225])).
% 61.18/61.36 cnf(4422,plain,
% 61.18/61.36 (P7(a22,a16,a22,a16,a22,a22,a22,a22)),
% 61.18/61.36 inference(scs_inference,[],[4351,4290,4360,4266,4120,4257,4278,4375,4126,4098,4234,4212,4378,3824,156,1996,2,1989,1878,2050,256,226,154,187,259,167,257,225,258])).
% 61.18/61.36 cnf(4426,plain,
% 61.18/61.36 (P4(a22,a16,a22,a16)),
% 61.18/61.36 inference(scs_inference,[],[4351,4290,4360,4266,4120,4257,4278,4337,4375,4126,4098,4234,4264,4212,4378,3824,156,1996,2,1989,1878,2050,256,226,154,187,259,167,257,225,258,153,168])).
% 61.18/61.36 cnf(4428,plain,
% 61.18/61.36 (P9(a16,a16,a16,f28(a16,a16,a16,a16,a16,a16))),
% 61.18/61.36 inference(scs_inference,[],[4351,4290,4360,4266,4120,4257,4278,4337,4375,4126,4098,4234,4264,4212,4378,4292,3824,156,1996,2,1989,1878,2050,256,226,154,187,259,167,257,225,258,153,168,164])).
% 61.18/61.37 cnf(4430,plain,
% 61.18/61.37 (P8(x44301,x44302,x44302,x44301,x44303,x44304,x44304,x44303)),
% 61.18/61.37 inference(scs_inference,[],[4351,4290,4302,4360,4266,4120,4257,4278,4337,4375,4126,4098,4234,4264,4212,4378,4292,3824,156,1996,2,1989,1878,2050,256,226,154,187,259,167,257,225,258,153,168,164,254])).
% 61.18/61.37 cnf(4432,plain,
% 61.18/61.37 (P8(a19,a19,a16,a19,a16,a19,a19,a19)),
% 61.18/61.37 inference(scs_inference,[],[4351,4290,4302,4360,4266,4120,4257,4262,4278,4337,4375,4126,4098,4234,4264,4212,4378,4292,3824,156,1996,2,1989,1878,2050,256,226,154,187,259,167,257,225,258,153,168,164,254,253])).
% 61.18/61.37 cnf(4436,plain,
% 61.18/61.37 (P10(x44361,x44362,x44361,x44362)),
% 61.18/61.37 inference(scs_inference,[],[4351,4290,4302,4340,4360,4266,4120,4257,4262,4278,4337,4375,3887,4126,4098,4234,4264,4212,4378,4292,3824,156,1996,2,1989,1878,2050,256,226,154,187,259,167,257,225,258,153,168,164,254,253,165,166])).
% 61.18/61.37 cnf(4450,plain,
% 61.18/61.37 (P3(x44501,x44501,x44501,x44502)),
% 61.18/61.37 inference(scs_inference,[],[4351,4290,4302,4310,4340,4360,4266,4120,4257,4262,4268,4278,4337,4375,3783,3887,4126,4330,4098,4234,4264,4212,4378,4292,3747,3620,3824,156,1996,2,1989,1878,2050,256,226,154,187,259,167,257,225,258,153,168,164,254,253,165,166,151,163,152,252,160,224,171])).
% 61.18/61.37 cnf(4454,plain,
% 61.18/61.37 (P3(x44541,x44542,x44543,x44542)),
% 61.18/61.37 inference(scs_inference,[],[4351,4290,4302,4310,4340,4360,4392,4266,4120,4257,4262,4268,4278,4337,4375,3459,3783,3887,4126,4330,4098,4234,4264,4212,4378,4292,3747,3620,3824,156,1996,2,1989,1878,2050,256,226,154,187,259,167,257,225,258,153,168,164,254,253,165,166,151,163,152,252,160,224,171,255,170])).
% 61.18/61.37 cnf(4459,plain,
% 61.18/61.37 (P4(x44591,x44591,x44591,f3(x44591,x44591,x44591))),
% 61.18/61.37 inference(scs_inference,[],[4351,4290,4302,4310,4340,4360,4392,4266,4120,4257,4262,4268,4278,4337,4375,3459,3783,3887,4126,4330,4098,4234,4264,4212,4378,4292,4206,3747,3620,4134,4232,3824,156,1996,2,1989,1878,2050,256,226,154,187,259,167,257,225,258,153,168,164,254,253,165,166,151,163,152,252,160,224,171,255,170,249,188])).
% 61.18/61.37 cnf(4461,plain,
% 61.18/61.37 (P2(f8(x44611,x44611,x44611),x44611,x44611,x44611)),
% 61.18/61.37 inference(scs_inference,[],[4351,4290,4302,4310,4340,4360,4392,4266,4120,4257,4262,4268,4278,4337,4375,3459,3783,3887,4126,4330,4098,4234,4264,4212,4378,4292,4206,3747,3620,4134,4232,3824,156,1996,2,1989,1878,2050,256,226,154,187,259,167,257,225,258,153,168,164,254,253,165,166,151,163,152,252,160,224,171,255,170,249,188,191])).
% 61.18/61.37 cnf(4462,plain,
% 61.18/61.37 (P3(x44621,x44621,x44622,x44621)),
% 61.18/61.37 inference(rename_variables,[],[4310])).
% 61.18/61.37 cnf(4463,plain,
% 61.18/61.37 (P10(x44631,x44632,x44632,x44631)),
% 61.18/61.37 inference(rename_variables,[],[4340])).
% 61.18/61.37 cnf(4465,plain,
% 61.18/61.37 (P4(f30(a16,a16,a16,a16,a16),a16,f30(a16,a16,a16,a16,a16),f30(a16,a16,a16,a16,a16))),
% 61.18/61.37 inference(scs_inference,[],[4351,4290,4302,4310,4340,4463,4360,4392,4266,4120,4257,4262,4268,4278,4337,4375,3459,3783,3887,4126,4330,4098,4234,4264,4212,4378,4204,4292,4206,3747,3620,4134,4232,3824,156,1996,2,1989,1878,2050,256,226,154,187,259,167,257,225,258,153,168,164,254,253,165,166,151,163,152,252,160,224,171,255,170,249,188,191,173])).
% 61.18/61.37 cnf(4466,plain,
% 61.18/61.37 (P10(x44661,x44662,x44662,x44661)),
% 61.18/61.37 inference(rename_variables,[],[4340])).
% 61.18/61.37 cnf(4469,plain,
% 61.18/61.37 (P4(x44691,x44692,x44691,f30(x44692,x44691,x44692,x44692,x44692))),
% 61.18/61.37 inference(scs_inference,[],[4351,4290,4302,4310,4340,4463,4466,4360,4392,4266,4120,4257,4262,4268,4278,4337,4375,3459,3783,3887,4126,4330,4098,4234,4264,4212,4378,4204,4292,4206,3747,3620,391,4134,4232,3824,156,1996,2,1989,1878,2050,256,226,154,187,259,167,257,225,258,153,168,164,254,253,165,166,151,163,152,252,160,224,171,255,170,249,188,191,173,100,200])).
% 61.18/61.37 cnf(4470,plain,
% 61.18/61.37 (P4(x44701,x44701,x44701,x44701)),
% 61.18/61.37 inference(rename_variables,[],[4206])).
% 61.18/61.37 cnf(4472,plain,
% 61.18/61.37 (P9(f30(x44721,x44722,x44721,x44721,x44721),x44721,x44721,x44722)),
% 61.18/61.37 inference(scs_inference,[],[4351,4290,4302,4310,4340,4463,4466,4360,4392,4266,4120,4257,4262,4268,4278,4337,4375,3459,3783,3887,4126,4330,4098,4234,4264,4212,4378,4204,4292,4206,4470,3747,3620,391,4134,4232,3824,156,1996,2,1989,1878,2050,256,226,154,187,259,167,257,225,258,153,168,164,254,253,165,166,151,163,152,252,160,224,171,255,170,249,188,191,173,100,200,201])).
% 61.18/61.37 cnf(4473,plain,
% 61.18/61.37 (P4(x44731,x44731,x44731,x44731)),
% 61.18/61.37 inference(rename_variables,[],[4206])).
% 61.18/61.37 cnf(4479,plain,
% 61.18/61.37 (P4(x44791,x44791,x44791,x44791)),
% 61.18/61.37 inference(rename_variables,[],[4206])).
% 61.18/61.37 cnf(4481,plain,
% 61.18/61.37 (P7(a16,a19,a19,a19,a16,a19,a19,a19)),
% 61.18/61.37 inference(scs_inference,[],[4351,4290,4302,4310,4340,4463,4466,4360,4392,4266,4120,4257,4262,4268,4278,4337,4375,3459,3783,3887,4126,4330,4098,4234,4264,4212,4378,4204,4292,4206,4470,4473,3747,3620,391,4134,3956,4232,3824,156,1996,2,1989,1878,2050,256,226,154,187,259,167,257,225,258,153,168,164,254,253,165,166,151,163,152,252,160,224,171,255,170,249,188,191,173,100,200,201,240,199,223])).
% 61.18/61.37 cnf(4484,plain,
% 61.18/61.37 (P4(x44841,x44841,x44841,x44841)),
% 61.18/61.37 inference(rename_variables,[],[4206])).
% 61.18/61.37 cnf(4489,plain,
% 61.18/61.37 (P8(x44891,x44892,x44893,x44894,x44892,x44891,x44894,x44893)),
% 61.18/61.37 inference(rename_variables,[],[4290])).
% 61.18/61.37 cnf(4493,plain,
% 61.18/61.37 (P10(x44931,x44932,x44932,x44931)),
% 61.18/61.37 inference(rename_variables,[],[4340])).
% 61.18/61.37 cnf(4497,plain,
% 61.18/61.37 (P10(x44971,x44972,x44972,x44971)),
% 61.18/61.37 inference(rename_variables,[],[4340])).
% 61.18/61.37 cnf(4501,plain,
% 61.18/61.37 (P8(a19,a19,a19,a19,a19,a19,a19,a16)),
% 61.18/61.37 inference(scs_inference,[],[4351,4290,4402,4302,4310,4340,4463,4466,4493,4360,4392,4266,4120,4257,4262,4268,4278,4337,4375,3459,3783,3887,4126,4330,4098,4234,4264,4212,4378,4204,4274,4292,4206,4470,4473,4479,3747,3620,391,4134,3956,4232,3824,156,1996,2,1989,1878,2050,256,226,154,187,259,167,257,225,258,153,168,164,254,253,165,166,151,163,152,252,160,224,171,255,170,249,188,191,173,100,200,201,240,199,223,243,181,241,190,189,184,227])).
% 61.18/61.37 cnf(4502,plain,
% 61.18/61.37 (P2(x45021,x45021,x45021,x45021)),
% 61.18/61.37 inference(rename_variables,[],[4351])).
% 61.18/61.37 cnf(4504,plain,
% 61.18/61.37 (P3(a1,a1,a15,a2)),
% 61.18/61.37 inference(scs_inference,[],[4351,4290,4402,4302,4310,4340,4463,4466,4493,4360,4392,3594,4266,4120,4257,4262,4268,4278,4337,4375,3459,3783,3887,4126,4330,4098,4234,4264,4212,4378,4204,4274,4292,4206,4470,4473,4479,3747,3620,391,4134,3956,3988,4232,3824,156,1996,2,1989,1878,2050,256,226,154,187,259,167,257,225,258,153,168,164,254,253,165,166,151,163,152,252,160,224,171,255,170,249,188,191,173,100,200,201,240,199,223,243,181,241,190,189,184,227,236])).
% 61.18/61.37 cnf(4507,plain,
% 61.18/61.37 (P6(x45071,x45071,x45071)),
% 61.18/61.37 inference(scs_inference,[],[4351,4502,4290,4402,4489,4302,4310,4340,4463,4466,4493,4360,4392,3594,4266,4120,4257,4262,4268,4278,4337,4375,3459,3783,3887,4126,4330,4098,4234,4264,4212,4378,4204,4274,4292,4206,4470,4473,4479,3747,3620,391,4134,4138,3956,3988,4232,3824,156,1996,2,1989,1878,2050,256,226,154,187,259,167,257,225,258,153,168,164,254,253,165,166,151,163,152,252,160,224,171,255,170,249,188,191,173,100,200,201,240,199,223,243,181,241,190,189,184,227,236,239])).
% 61.18/61.37 cnf(4518,plain,
% 61.18/61.37 (P10(x45181,x45182,x45182,x45181)),
% 61.18/61.37 inference(rename_variables,[],[4340])).
% 61.18/61.37 cnf(4520,plain,
% 61.18/61.37 (P6(f7(a16,a20,a22,a19),a19,a19)),
% 61.18/61.37 inference(scs_inference,[],[4351,4502,4290,4402,4489,4302,4310,4462,4340,4463,4466,4493,4497,4360,4392,3594,4266,4120,4257,4262,4268,4278,4337,4375,3459,3783,3887,4126,4330,4098,4234,4264,4212,4378,4204,4274,4292,4206,4470,4473,4479,4484,3747,3620,391,4134,4138,3956,3988,4232,3824,156,1996,2,1989,1878,2050,256,226,154,187,259,167,257,225,258,153,168,164,254,253,165,166,151,163,152,252,160,224,171,255,170,249,188,191,173,100,200,201,240,199,223,243,181,241,190,189,184,227,236,239,195,186,1998])).
% 61.18/61.37 cnf(4534,plain,
% 61.18/61.37 (P10(x45341,x45342,x45342,x45341)),
% 61.18/61.37 inference(rename_variables,[],[4340])).
% 61.18/61.37 cnf(4536,plain,
% 61.18/61.37 (~P9(a19,a19,a16,a19)+P1(a16,a19,f27(a19,a16,a19,a19))),
% 61.18/61.37 inference(scs_inference,[],[4351,4502,4290,4402,4489,4302,4310,4462,4340,4463,4466,4493,4497,4518,4534,4360,4392,3594,4266,4120,4257,4262,4268,4278,4337,4375,3459,3783,3887,4126,4330,4098,4234,4264,4114,4212,4378,4204,4274,4292,4206,4470,4473,4479,4484,3747,3620,391,4134,4138,3956,3988,4232,3824,156,1996,2,1989,1878,2050,256,226,154,187,259,167,257,225,258,153,168,164,254,253,165,166,151,163,152,252,160,224,171,255,170,249,188,191,173,100,200,201,240,199,223,243,181,241,190,189,184,227,236,239,195,186,1998,2114,1993,169,246,172,197,182])).
% 61.18/61.37 cnf(4582,plain,
% 61.18/61.37 (P3(x45821,x45822,x45823,x45822)),
% 61.18/61.37 inference(rename_variables,[],[4454])).
% 61.18/61.37 cnf(4584,plain,
% 61.18/61.37 (P3(x45841,x45842,x45843,x45843)),
% 61.18/61.37 inference(rename_variables,[],[4360])).
% 61.18/61.37 cnf(4590,plain,
% 61.18/61.37 (P6(a19,a16,a16)),
% 61.18/61.37 inference(scs_inference,[],[4507,4454,4410,4372,4360,3579,3726,1996,156,2,1989])).
% 61.18/61.37 cnf(4591,plain,
% 61.18/61.37 (P6(x45911,x45911,x45911)),
% 61.18/61.37 inference(rename_variables,[],[4507])).
% 61.18/61.37 cnf(4593,plain,
% 61.18/61.37 (P8(a22,a16,a16,a16,a16,a16,a22,a16)),
% 61.18/61.37 inference(scs_inference,[],[4507,4454,4426,4410,4372,4360,3579,3726,1996,156,2,1989,226])).
% 61.18/61.37 cnf(4595,plain,
% 61.18/61.37 (P7(a22,a22,a22,a22,a22,a16,a22,a16)),
% 61.18/61.37 inference(scs_inference,[],[4507,4454,4422,4426,4410,4372,4360,3579,3726,1996,156,2,1989,226,256])).
% 61.18/61.37 cnf(4601,plain,
% 61.18/61.37 (P8(f30(x46011,x46012,x46011,x46011,x46011),x46011,x46013,x46014,x46011,x46012,x46013,x46014)),
% 61.18/61.37 inference(scs_inference,[],[4507,4454,4422,4426,4472,4410,4372,4236,4360,3579,3726,1996,156,2,1989,226,256,2050,154,225])).
% 61.18/61.37 cnf(4603,plain,
% 61.18/61.37 (P7(a19,a19,a16,a19,a19,a19,a16,a19)),
% 61.18/61.37 inference(scs_inference,[],[4507,4454,4422,4426,4481,4472,4410,4372,4236,4360,3579,3726,1996,156,2,1989,226,256,2050,154,225,257])).
% 61.18/61.37 cnf(4607,plain,
% 61.18/61.37 (P4(a16,a19,a19,a16)),
% 61.18/61.37 inference(scs_inference,[],[4507,4454,4393,4422,4426,4481,4472,4410,4372,4236,4360,3579,3726,1996,156,2,1989,226,256,2050,154,225,257,259,168])).
% 61.18/61.37 cnf(4611,plain,
% 61.18/61.37 (P7(a19,a16,a19,a19,a16,a19,a19,a19)),
% 61.18/61.37 inference(scs_inference,[],[4507,4454,4393,4422,4426,4481,4459,4472,4410,4372,4236,4360,3579,3726,1996,156,2,1989,226,256,2050,154,225,257,259,168,167,258])).
% 61.18/61.37 cnf(4613,plain,
% 61.18/61.37 (P1(f25(a22,x46131),x46131,a22)),
% 61.18/61.37 inference(scs_inference,[],[4507,4454,4393,4422,4426,4481,4459,4472,4410,4372,4236,4360,3579,3726,1996,156,2,1989,226,256,2050,154,225,257,259,168,167,258,153])).
% 61.18/61.37 cnf(4631,plain,
% 61.18/61.37 (P9(x46311,x46312,f30(x46311,x46312,x46311,x46311,x46311),x46311)),
% 61.18/61.37 inference(scs_inference,[],[4507,4454,4393,4422,4426,4481,4501,4412,4459,4472,3583,3902,3898,4410,4372,4236,4360,3579,3726,1996,156,2,1989,226,256,2050,154,225,257,259,168,167,258,153,254,164,166,253,151,165,252,152,163])).
% 61.18/61.37 cnf(4633,plain,
% 61.18/61.37 (P8(x46331,x46332,x46331,x46333,x46333,x46332,x46333,x46333)),
% 61.18/61.37 inference(scs_inference,[],[4507,4454,4582,4393,4422,4426,4481,4501,4412,4459,4472,3583,3902,3898,4410,4372,4236,4360,3579,3726,1996,156,2,1989,226,256,2050,154,225,257,259,168,167,258,153,254,164,166,253,151,165,252,152,163,224])).
% 61.18/61.37 cnf(4635,plain,
% 61.18/61.37 (P3(x46351,x46352,x46353,x46351)),
% 61.18/61.37 inference(scs_inference,[],[4507,4454,4582,4393,4422,4426,4481,4501,4412,4459,4472,3583,3902,3898,4410,4372,4236,4360,3579,3726,1996,156,2,1989,226,256,2050,154,225,257,259,168,167,258,153,254,164,166,253,151,165,252,152,163,224,169])).
% 61.18/61.37 cnf(4637,plain,
% 61.18/61.37 (P3(x46371,x46372,x46372,x46373)),
% 61.18/61.37 inference(scs_inference,[],[4507,4454,4582,4393,4422,4426,4481,4501,4412,4459,4472,3583,3902,3898,4410,4372,4236,4360,3579,3726,1996,156,2,1989,226,256,2050,154,225,257,259,168,167,258,153,254,164,166,253,151,165,252,152,163,224,169,171])).
% 61.18/61.37 cnf(4641,plain,
% 61.18/61.37 (P3(a15,a2,a15,a1)),
% 61.18/61.37 inference(scs_inference,[],[4507,4454,4582,4308,4393,4422,4426,4481,4501,4412,4459,4472,3583,3902,3898,4410,4372,4236,4360,3579,3726,1996,156,2,1989,226,256,2050,154,225,257,259,168,167,258,153,254,164,166,253,151,165,252,152,163,224,169,171,255,170])).
% 61.18/61.37 cnf(4644,plain,
% 61.18/61.37 (P3(x46441,x46442,x46443,x46443)),
% 61.18/61.37 inference(rename_variables,[],[4360])).
% 61.18/61.37 cnf(4647,plain,
% 61.18/61.37 (P10(x46471,x46472,x46472,x46471)),
% 61.18/61.37 inference(rename_variables,[],[4340])).
% 61.18/61.37 cnf(4649,plain,
% 61.18/61.37 (P6(f30(a16,a16,a16,a16,a16),a16,f30(a16,a16,a16,a16,a16))),
% 61.18/61.37 inference(scs_inference,[],[4507,4454,4582,4308,4393,4422,4426,4481,4501,4412,4459,4472,3583,3902,3898,3996,4465,4410,4372,4236,4360,4584,4340,3968,3579,3726,1996,156,2,1989,226,256,2050,154,225,257,259,168,167,258,153,254,164,166,253,151,165,252,152,163,224,169,171,255,170,230,188,161])).
% 61.18/61.37 cnf(4656,plain,
% 61.18/61.37 (~E(a17,a2)),
% 61.18/61.37 inference(scs_inference,[],[4507,4454,4582,4308,4393,4422,4426,4481,4501,4412,4459,4472,3583,3902,3898,3996,4465,4410,4372,4236,4360,4584,4644,4340,3968,408,344,4134,3579,3726,1996,156,2,1989,226,256,2050,154,225,257,259,168,167,258,153,254,164,166,253,151,165,252,152,163,224,169,171,255,170,230,188,161,249,99,101])).
% 61.18/61.37 cnf(4657,plain,
% 61.18/61.37 (P3(x46571,x46572,x46573,x46573)),
% 61.18/61.37 inference(rename_variables,[],[4360])).
% 61.18/61.37 cnf(4665,plain,
% 61.18/61.37 (P10(x46651,x46652,x46652,x46651)),
% 61.18/61.37 inference(rename_variables,[],[4340])).
% 61.18/61.37 cnf(4668,plain,
% 61.18/61.37 (P10(x46681,x46682,x46681,x46682)),
% 61.18/61.37 inference(rename_variables,[],[4436])).
% 61.18/61.37 cnf(4670,plain,
% 61.18/61.37 (P4(f7(x46701,x46701,x46701,x46701),x46701,f7(x46701,x46701,x46701,x46701),x46701)),
% 61.18/61.37 inference(scs_inference,[],[4507,4591,4436,4454,4582,4308,4393,4422,4426,4481,4501,4412,4459,4472,3583,3902,3898,3996,4465,4410,4372,4236,4360,4584,4644,4657,4340,4647,3968,410,408,344,4134,3579,3726,1996,156,2,1989,226,256,2050,154,225,257,259,168,167,258,153,254,164,166,253,151,165,252,152,163,224,169,171,255,170,230,188,161,249,99,101,205,102,204,176,201,173])).
% 61.18/61.37 cnf(4671,plain,
% 61.18/61.37 (P10(f7(x46711,x46711,x46711,x46711),x46711,x46711,x46711)),
% 61.18/61.37 inference(rename_variables,[],[4412])).
% 61.18/61.37 cnf(4674,plain,
% 61.18/61.37 (P10(x46741,x46742,x46741,x46742)),
% 61.18/61.37 inference(rename_variables,[],[4436])).
% 61.18/61.37 cnf(4679,plain,
% 61.18/61.37 (P10(a16,a16,a19,a19)),
% 61.18/61.37 inference(scs_inference,[],[4507,4591,4436,4668,4454,4582,4308,4393,4422,4426,4481,4501,4412,4459,4472,3583,3902,3898,3996,4465,4410,4372,4236,4360,4584,4644,4657,4340,4647,4665,3968,410,408,344,4134,3579,3726,1996,156,2,1989,226,256,2050,154,225,257,259,168,167,258,153,254,164,166,253,151,165,252,152,163,224,169,171,255,170,230,188,161,249,99,101,205,102,204,176,201,173,200,199,181])).
% 61.18/61.37 cnf(4686,plain,
% 61.18/61.37 (P1(f5(x46861,x46861,x46862),x46862,x46861)),
% 61.18/61.37 inference(scs_inference,[],[4507,4591,4436,4668,4674,4454,4582,4308,4393,4422,4426,4481,4501,4412,4459,4472,3583,3902,3898,3996,4188,4465,4410,4372,4236,4290,4360,4584,4644,4657,4340,4647,4665,3968,410,408,344,4134,3579,3726,1996,156,2,1989,226,256,2050,154,225,257,259,168,167,258,153,254,164,166,253,151,165,252,152,163,224,169,171,255,170,230,188,161,249,99,101,205,102,204,176,201,173,200,199,181,223,240,178])).
% 61.18/61.37 cnf(4688,plain,
% 61.18/61.37 (P1(f4(x46881,x46881,x46882),x46882,x46881)),
% 61.18/61.37 inference(scs_inference,[],[4507,4591,4436,4668,4674,4454,4582,4308,4393,4422,4426,4481,4501,4412,4459,4472,3583,3902,3898,3996,4188,4465,4410,4372,4236,4290,4360,4584,4644,4657,4340,4647,4665,3968,410,408,344,4134,3579,3726,1996,156,2,1989,226,256,2050,154,225,257,259,168,167,258,153,254,164,166,253,151,165,252,152,163,224,169,171,255,170,230,188,161,249,99,101,205,102,204,176,201,173,200,199,181,223,240,178,177])).
% 61.18/61.37 cnf(4692,plain,
% 61.18/61.37 (P10(x46921,x46922,x46921,x46922)),
% 61.18/61.37 inference(rename_variables,[],[4436])).
% 61.18/61.37 cnf(4701,plain,
% 61.18/61.37 (P10(x47011,x47012,x47011,x47012)),
% 61.18/61.37 inference(rename_variables,[],[4436])).
% 61.18/61.37 cnf(4703,plain,
% 61.18/61.37 (P6(f28(x47031,x47031,x47031,x47031,x47031,x47031),x47031,x47031)),
% 61.18/61.37 inference(scs_inference,[],[4507,4591,4436,4668,4674,4692,4454,4582,4308,4393,4422,4426,4481,4501,4412,4459,4472,3583,3902,3898,3996,4188,4465,4420,4410,4372,4236,4290,4360,4584,4644,4657,4340,4647,4665,3968,410,408,344,4134,3579,3726,1996,156,2,1989,226,256,2050,154,225,257,259,168,167,258,153,254,164,166,253,151,165,252,152,163,224,169,171,255,170,230,188,161,249,99,101,205,102,204,176,201,173,200,199,181,223,240,178,177,241,190,184,189,182,203])).
% 61.18/61.37 cnf(4707,plain,
% 61.18/61.37 (P10(x47071,x47072,x47071,x47072)),
% 61.18/61.37 inference(rename_variables,[],[4436])).
% 61.18/61.37 cnf(4710,plain,
% 61.18/61.37 (P6(f25(a22,x47101),x47101,a22)),
% 61.18/61.37 inference(rename_variables,[],[4410])).
% 61.18/61.37 cnf(4712,plain,
% 61.18/61.37 (P10(f8(x47121,x47121,x47121),x47121,x47121,x47121)),
% 61.18/61.37 inference(scs_inference,[],[4507,4591,4430,4436,4668,4674,4692,4701,4454,4582,4308,4393,4422,4426,4481,4501,4412,4671,4459,4461,4472,3583,3902,3898,3996,4188,4465,4420,4410,4372,4236,4321,4290,4360,4584,4644,4657,4340,4647,4665,3968,410,408,344,4134,3579,3726,1996,156,2,1989,226,256,2050,154,225,257,259,168,167,258,153,254,164,166,253,151,165,252,152,163,224,169,171,255,170,230,188,161,249,99,101,205,102,204,176,201,173,200,199,181,223,240,178,177,241,190,184,189,182,203,180,227,242])).
% 61.18/61.37 cnf(4713,plain,
% 61.18/61.37 (P8(x47131,x47132,x47132,x47131,x47133,x47134,x47134,x47133)),
% 61.18/61.37 inference(rename_variables,[],[4430])).
% 61.18/61.37 cnf(4715,plain,
% 61.18/61.37 (P2(f9(x47151,x47151,x47151),x47151,x47151,x47151)),
% 61.18/61.37 inference(scs_inference,[],[4507,4591,4430,4436,4668,4674,4692,4701,4450,4454,4582,4308,4393,4422,4426,4481,4501,4412,4671,4459,4461,4472,3583,3902,3898,3996,4188,4465,4420,4410,4372,4236,4321,4290,4360,4584,4644,4657,4340,4647,4665,3968,410,408,344,3837,4134,3579,3726,1996,156,2,1989,226,256,2050,154,225,257,259,168,167,258,153,254,164,166,253,151,165,252,152,163,224,169,171,255,170,230,188,161,249,99,101,205,102,204,176,201,173,200,199,181,223,240,178,177,241,190,184,189,182,203,180,227,242,192])).
% 61.18/61.37 cnf(4717,plain,
% 61.18/61.37 (P3(x47171,x47171,x47171,x47172)),
% 61.18/61.37 inference(rename_variables,[],[4450])).
% 61.18/61.37 cnf(4719,plain,
% 61.18/61.37 (P10(a16,a16,a16,a19)),
% 61.18/61.37 inference(scs_inference,[],[4507,4591,4430,4436,4668,4674,4692,4701,4450,4717,4454,4582,4308,4393,4422,4426,4481,4501,4412,4671,4459,4461,4472,3583,3902,3898,3996,4188,4465,4420,4410,4372,4236,4321,4290,4360,4584,4644,4657,4340,4647,4665,3968,410,408,344,4206,3837,4134,3579,3726,1996,156,2,1989,226,256,2050,154,225,257,259,168,167,258,153,254,164,166,253,151,165,252,152,163,224,169,171,255,170,230,188,161,249,99,101,205,102,204,176,201,173,200,199,181,223,240,178,177,241,190,184,189,182,203,180,227,242,192,195])).
% 61.18/61.37 cnf(4721,plain,
% 61.18/61.37 (P3(x47211,x47211,x47211,x47212)),
% 61.18/61.37 inference(rename_variables,[],[4450])).
% 61.18/61.37 cnf(4723,plain,
% 61.18/61.37 (P6(f6(x47231,x47231,x47231),x47231,x47231)),
% 61.18/61.37 inference(scs_inference,[],[4507,4591,4430,4436,4668,4674,4692,4701,4707,4450,4717,4454,4582,4308,4393,4422,4426,4481,4501,4412,4671,4459,4461,4472,3583,3902,3898,3996,4188,4465,4420,4410,4372,4236,4321,4290,4360,4584,4644,4657,4340,4647,4665,3968,410,408,344,4206,3837,4134,3579,3726,1996,156,2,1989,226,256,2050,154,225,257,259,168,167,258,153,254,164,166,253,151,165,252,152,163,224,169,171,255,170,230,188,161,249,99,101,205,102,204,176,201,173,200,199,181,223,240,178,177,241,190,184,189,182,203,180,227,242,192,195,186])).
% 61.18/61.37 cnf(4725,plain,
% 61.18/61.37 (P6(x47251,x47251,x47251)),
% 61.18/61.37 inference(rename_variables,[],[4507])).
% 61.18/61.37 cnf(4729,plain,
% 61.18/61.37 (P6(x47291,x47291,x47291)),
% 61.18/61.37 inference(rename_variables,[],[4507])).
% 61.18/61.37 cnf(4732,plain,
% 61.18/61.37 (P4(x47321,x47321,x47322,x47322)),
% 61.18/61.37 inference(scs_inference,[],[4507,4591,4725,4430,4713,4436,4668,4674,4692,4701,4707,4450,4717,4721,4454,4582,4308,4393,4422,4426,4481,4501,4412,4671,4459,4461,4472,3583,3902,3898,3996,4188,4465,4420,4410,4372,4428,4236,4321,4290,4360,4584,4644,4657,4340,4647,4665,3968,410,408,344,4206,3837,4134,4138,3579,3726,1996,156,2,1989,226,256,2050,154,225,257,259,168,167,258,153,254,164,166,253,151,165,252,152,163,224,169,171,255,170,230,188,161,249,99,101,205,102,204,176,201,173,200,199,181,223,240,178,177,241,190,184,189,182,203,180,227,242,192,195,186,162,251])).
% 61.18/61.37 cnf(4735,plain,
% 61.18/61.37 (P6(f25(a20,x47351),a20,x47351)),
% 61.18/61.37 inference(scs_inference,[],[4507,4591,4725,4729,4430,4713,4436,4668,4674,4692,4701,4707,4450,4717,4721,4454,4582,4308,4393,4422,4426,4481,4501,4412,4671,4459,4461,4472,3583,3902,4008,3898,3996,4188,4465,4420,4410,4710,4372,4428,4236,4321,4290,4360,4584,4644,4657,4340,4647,4665,3968,410,408,344,4206,3837,4134,4138,3579,3726,1996,156,2,1989,226,256,2050,154,225,257,259,168,167,258,153,254,164,166,253,151,165,252,152,163,224,169,171,255,170,230,188,161,249,99,101,205,102,204,176,201,173,200,199,181,223,240,178,177,241,190,184,189,182,203,180,227,242,192,195,186,162,251,159])).
% 61.18/61.37 cnf(4739,plain,
% 61.18/61.37 (P9(a19,a19,a19,a16)),
% 61.18/61.37 inference(scs_inference,[],[4507,4591,4725,4729,4430,4713,4436,4668,4674,4692,4701,4707,4450,4717,4721,4454,4582,4308,4393,4422,4426,4481,4501,4412,4671,4459,4461,4472,3583,3902,4008,3898,3996,4188,4465,4420,4410,4710,4372,4428,4236,4321,4290,4360,4584,4644,4657,4340,4647,4665,3968,410,408,344,4206,3837,4134,4138,3579,3726,1996,156,2,1989,226,256,2050,154,225,257,259,168,167,258,153,254,164,166,253,151,165,252,152,163,224,169,171,255,170,230,188,161,249,99,101,205,102,204,176,201,173,200,199,181,223,240,178,177,241,190,184,189,182,203,180,227,242,192,195,186,162,251,159,233])).
% 61.18/61.37 cnf(4761,plain,
% 61.18/61.37 (P6(f6(x47611,x47611,x47611),x47611,x47611)),
% 61.18/61.37 inference(rename_variables,[],[4723])).
% 61.18/61.37 cnf(4763,plain,
% 61.18/61.37 (P4(a19,a16,a19,a16)),
% 61.18/61.37 inference(scs_inference,[],[4590,4723,1996,156])).
% 61.18/61.37 cnf(4766,plain,
% 61.18/61.37 (P6(f28(x47661,x47661,x47661,x47661,x47661,x47661),x47661,x47661)),
% 61.18/61.37 inference(rename_variables,[],[4703])).
% 61.18/61.37 cnf(4771,plain,
% 61.18/61.37 (P7(a16,a19,a19,a19,a19,a16,a19,a19)),
% 61.18/61.37 inference(scs_inference,[],[4590,4611,4703,4723,4761,1996,156,1989,2050,256])).
% 61.18/61.37 cnf(4780,plain,
% 61.18/61.37 (P6(f30(a16,a16,a16,a16,a16),f30(a16,a16,a16,a16,a16),a16)),
% 61.18/61.37 inference(scs_inference,[],[4656,4739,4590,4595,4611,4670,4703,4723,4761,4649,1996,156,1989,2050,256,226,225,2,259,154])).
% 61.18/61.37 cnf(4784,plain,
% 61.18/61.37 (P7(a19,a19,a19,a16,a19,a19,a16,a19)),
% 61.18/61.37 inference(scs_inference,[],[4656,4739,4590,4595,4607,4611,4670,4703,4723,4761,4649,1996,156,1989,2050,256,226,225,2,259,154,167,257])).
% 61.18/61.37 cnf(4788,plain,
% 61.18/61.37 (P4(f7(x47881,x47881,x47881,x47881),x47881,x47881,f7(x47881,x47881,x47881,x47881))),
% 61.18/61.37 inference(scs_inference,[],[4656,4739,4590,4595,4607,4611,4670,4703,4723,4761,4649,4735,1996,156,1989,2050,256,226,225,2,259,154,167,257,153,168])).
% 61.18/61.37 cnf(4792,plain,
% 61.18/61.37 (P8(x47921,x47922,x47922,x47923,x47923,x47921,x47923,x47923)),
% 61.18/61.37 inference(scs_inference,[],[4633,4656,4739,4590,4595,4607,4611,4670,4703,4723,4761,4649,4735,4343,1996,156,1989,2050,256,226,225,2,259,154,167,257,153,168,258,254])).
% 61.18/61.37 cnf(4794,plain,
% 61.18/61.37 (P9(a19,a19,a16,a19)),
% 61.18/61.37 inference(scs_inference,[],[4633,4656,4739,4590,4595,4607,4611,4670,4703,4723,4761,4649,4735,4343,1996,156,1989,2050,256,226,225,2,259,154,167,257,153,168,258,254,164])).
% 61.18/61.37 cnf(4798,plain,
% 61.18/61.37 (P10(a16,a16,a19,a16)),
% 61.18/61.37 inference(scs_inference,[],[4633,4719,4656,4739,4590,4595,4607,4611,4670,4703,4723,4761,4686,4649,4735,4343,1996,156,1989,2050,256,226,225,2,259,154,167,257,153,168,258,254,164,151,166])).
% 61.18/61.37 cnf(4800,plain,
% 61.18/61.37 (P8(x48001,x48002,x48001,x48003,x48002,x48002,x48002,x48003)),
% 61.18/61.37 inference(scs_inference,[],[4633,4719,4656,4739,4590,4595,4607,4611,4670,4703,4723,4761,4686,4649,4735,4343,1996,156,1989,2050,256,226,225,2,259,154,167,257,153,168,258,254,164,151,166,253])).
% 61.18/61.37 cnf(4802,plain,
% 61.18/61.37 (P10(a16,a19,a16,a16)),
% 61.18/61.37 inference(scs_inference,[],[4633,4719,4656,4739,4590,4595,4607,4611,4670,4703,4723,4761,4686,4649,4735,4343,1996,156,1989,2050,256,226,225,2,259,154,167,257,153,168,258,254,164,151,166,253,165])).
% 61.18/61.37 cnf(4804,plain,
% 61.18/61.37 (P8(x48041,x48042,x48041,x48041,x48043,x48042,x48043,x48041)),
% 61.18/61.37 inference(scs_inference,[],[4633,4719,4656,4739,4590,4595,4607,4611,4670,4703,4723,4761,4686,4649,4735,4343,1996,156,1989,2050,256,226,225,2,259,154,167,257,153,168,258,254,164,151,166,253,165,252])).
% 61.18/61.37 cnf(4808,plain,
% 61.18/61.37 (P9(a19,a16,a19,a19)),
% 61.18/61.37 inference(scs_inference,[],[4633,4719,4656,4739,4590,4595,4607,4611,4670,4703,4723,4761,4686,4649,4735,4343,1996,156,1989,2050,256,226,225,2,259,154,167,257,153,168,258,254,164,151,166,253,165,252,152,163])).
% 61.18/61.37 cnf(4810,plain,
% 61.18/61.37 (P3(x48101,x48102,x48101,x48103)),
% 61.18/61.37 inference(scs_inference,[],[4633,4637,4719,4656,4739,4590,4595,4607,4611,4670,4703,4723,4761,4686,4649,4735,4343,1996,156,1989,2050,256,226,225,2,259,154,167,257,153,168,258,254,164,151,166,253,165,252,152,163,169])).
% 61.18/61.37 cnf(4818,plain,
% 61.18/61.37 (P3(x48181,x48181,x48182,x48183)),
% 61.18/61.37 inference(scs_inference,[],[4633,4637,4719,4656,4739,4504,4590,4595,4607,4611,4641,4670,4703,4723,4761,4686,4649,4735,4343,1996,156,1989,2050,256,226,225,2,259,154,167,257,153,168,258,254,164,151,166,253,165,252,152,163,169,224,255,171,170])).
% 61.18/61.37 cnf(4824,plain,
% 61.18/61.37 (P10(x48241,x48242,x48241,x48242)),
% 61.18/61.37 inference(rename_variables,[],[4436])).
% 61.18/61.37 cnf(4827,plain,
% 61.18/61.37 (P4(x48271,x48271,x48272,x48272)),
% 61.18/61.37 inference(rename_variables,[],[4732])).
% 61.18/61.37 cnf(4835,plain,
% 61.18/61.37 (P2(f8(a16,a19,a16),a16,a19,a16)),
% 61.18/61.37 inference(scs_inference,[],[4633,4732,4635,4637,4719,4656,4739,4504,4590,4595,4607,4611,4641,4670,4703,4723,4761,4686,4649,4735,4343,4469,4436,4426,4033,3956,1996,156,1989,2050,256,226,225,2,259,154,167,257,153,168,258,254,164,151,166,253,165,252,152,163,169,224,255,171,170,174,250,194,183,249,191])).
% 61.18/61.37 cnf(4843,plain,
% 61.18/61.37 (P4(x48431,x48431,x48432,x48432)),
% 61.18/61.37 inference(rename_variables,[],[4732])).
% 61.18/61.37 cnf(4846,plain,
% 61.18/61.37 (P4(x48461,x48461,x48462,x48462)),
% 61.18/61.37 inference(rename_variables,[],[4732])).
% 61.18/61.37 cnf(4851,plain,
% 61.18/61.37 (P10(f7(x48511,x48511,x48511,x48511),f7(x48511,x48511,x48511,x48511),x48511,f7(x48511,x48511,x48511,x48511))),
% 61.18/61.37 inference(scs_inference,[],[4633,4732,4827,4843,4846,4635,4637,4719,4656,4739,4504,4590,4593,4595,4607,4611,4641,4670,4703,4723,4761,4686,4649,4735,4343,4469,4280,4507,4436,4426,4033,3956,1996,156,1989,2050,256,226,225,2,259,154,167,257,153,168,258,254,164,151,166,253,165,252,152,163,169,224,255,171,170,174,250,194,183,249,191,205,204,200,201,262,181])).
% 61.18/61.37 cnf(4852,plain,
% 61.18/61.37 (P4(x48521,x48521,x48522,x48522)),
% 61.18/61.37 inference(rename_variables,[],[4732])).
% 61.18/61.37 cnf(4857,plain,
% 61.18/61.37 (P4(f30(a16,a16,a16,a16,a16),f30(a16,a16,a16,a16,a16),f30(a16,a16,a16,a16,a16),a16)),
% 61.18/61.37 inference(scs_inference,[],[4633,4732,4827,4843,4846,4635,4637,4719,4656,4739,4504,4590,4593,4595,4607,4611,4641,4670,4703,4723,4761,4686,4649,4735,4343,4219,4469,4280,4507,4436,4824,4426,4033,3974,3956,1996,156,1989,2050,256,226,225,2,259,154,167,257,153,168,258,254,164,151,166,253,165,252,152,163,169,224,255,171,170,174,250,194,183,249,191,205,204,200,201,262,181,240,173])).
% 61.18/61.37 cnf(4858,plain,
% 61.18/61.37 (P10(x48581,x48582,x48581,x48582)),
% 61.18/61.37 inference(rename_variables,[],[4436])).
% 61.18/61.37 cnf(4861,plain,
% 61.18/61.37 (P10(x48611,x48612,x48612,x48611)),
% 61.18/61.37 inference(rename_variables,[],[4340])).
% 61.18/61.37 cnf(4863,plain,
% 61.18/61.37 (P7(a19,a16,a16,a16,a19,a16,a16,a16)),
% 61.18/61.37 inference(scs_inference,[],[4633,4732,4827,4843,4846,4635,4637,4719,4656,4739,4504,4590,4593,4595,4607,4611,4641,4670,4703,4723,4761,4686,4649,4735,4343,4219,4469,4280,4507,4436,4824,4426,4033,4340,3974,3956,1996,156,1989,2050,256,226,225,2,259,154,167,257,153,168,258,254,164,151,166,253,165,252,152,163,169,224,255,171,170,174,250,194,183,249,191,205,204,200,201,262,181,240,173,176,223])).
% 61.18/61.37 cnf(4869,plain,
% 61.18/61.37 (P10(x48691,x48692,x48692,x48691)),
% 61.18/61.37 inference(rename_variables,[],[4340])).
% 61.18/61.37 cnf(4872,plain,
% 61.18/61.37 (P10(x48721,x48722,x48722,x48721)),
% 61.18/61.37 inference(rename_variables,[],[4340])).
% 61.18/61.37 cnf(4875,plain,
% 61.18/61.37 (P10(x48751,x48752,x48752,x48751)),
% 61.18/61.37 inference(rename_variables,[],[4340])).
% 61.18/61.37 cnf(4883,plain,
% 61.18/61.37 (P2(f7(x48831,x48831,x48831,x48831),x48831,x48831,x48831)),
% 61.18/61.37 inference(scs_inference,[],[4633,4732,4827,4843,4846,4852,4635,4637,4719,4656,4739,4504,4590,4593,4595,4607,4611,4641,4679,4670,4703,4723,4761,4601,4686,4649,4735,4343,4219,4469,4280,4507,4436,4824,4426,4033,4340,4861,4869,4872,4875,3974,3956,1996,156,1989,2050,256,226,225,2,259,154,167,257,153,168,258,254,164,151,166,253,165,252,152,163,169,224,255,171,170,174,250,194,183,249,191,205,204,200,201,262,181,240,173,176,223,199,178,177,190,241,189,184])).
% 61.18/61.37 cnf(4885,plain,
% 61.18/61.37 (P6(f28(a16,a16,a16,a16,a19,a19),a16,a16)),
% 61.18/61.37 inference(scs_inference,[],[4633,4732,4827,4843,4846,4852,4635,4637,4719,4656,4739,4504,4590,4593,4595,4607,4611,4641,4679,4670,4703,4723,4761,4601,4686,4649,4735,4343,4219,4469,4280,4507,4436,4824,4426,4033,4340,4861,4869,4872,4875,3974,3956,1996,156,1989,2050,256,226,225,2,259,154,167,257,153,168,258,254,164,151,166,253,165,252,152,163,169,224,255,171,170,174,250,194,183,249,191,205,204,200,201,262,181,240,173,176,223,199,178,177,190,241,189,184,203])).
% 61.18/61.37 cnf(4896,plain,
% 61.18/61.37 (P9(x48961,x48962,x48962,x48961)),
% 61.18/61.37 inference(rename_variables,[],[3837])).
% 61.18/61.37 cnf(4901,plain,
% 61.18/61.37 (P6(f25(a15,x49011),a15,x49011)),
% 61.18/61.37 inference(scs_inference,[],[142,4633,4732,4827,4843,4846,4852,4635,4637,4719,4656,4739,4504,4590,4593,4595,4607,4611,4641,4679,4670,4703,4766,4715,4723,4761,4601,4686,4649,4613,4735,4343,4219,4469,4280,4507,4436,4824,4858,3451,4426,4033,4340,4861,4869,4872,4875,4041,3974,3956,3837,4896,145,1996,156,1989,2050,256,226,225,2,259,154,167,257,153,168,258,254,164,151,166,253,165,252,152,163,169,224,255,171,170,174,250,194,183,249,191,205,204,200,201,262,181,240,173,176,223,199,178,177,190,241,189,184,203,227,186,228,207,159])).
% 61.18/61.37 cnf(4902,plain,
% 61.18/61.37 (P6(f28(x49021,x49021,x49021,x49021,x49021,x49021),x49021,x49021)),
% 61.18/61.37 inference(rename_variables,[],[4703])).
% 61.18/61.37 cnf(4909,plain,
% 61.18/61.37 (P1(x49091,f30(a16,a16,a16,a16,a16),a16)),
% 61.18/61.37 inference(scs_inference,[],[142,4633,4732,4827,4843,4846,4852,4635,4637,4719,4656,4739,4504,4590,4593,4595,4607,4611,4641,4679,4670,4703,4766,4902,4715,4723,4761,4601,4686,4649,4613,4735,4343,4219,4469,4280,4507,4436,4824,4858,3451,4426,4033,4340,4861,4869,4872,4875,4041,3974,3956,3837,4896,145,1996,156,1989,2050,256,226,225,2,259,154,167,257,153,168,258,254,164,151,166,253,165,252,152,163,169,224,255,171,170,174,250,194,183,249,191,205,204,200,201,262,181,240,173,176,223,199,178,177,190,241,189,184,203,227,186,228,207,159,4536,3924,160])).
% 61.18/61.37 cnf(4944,plain,
% 61.18/61.37 (P8(x49441,x49442,x49441,x49441,x49443,x49442,x49443,x49441)),
% 61.18/61.37 inference(rename_variables,[],[4804])).
% 61.18/61.37 cnf(4947,plain,
% 61.18/61.37 (P8(x49471,x49472,x49471,x49471,x49473,x49472,x49473,x49471)),
% 61.18/61.37 inference(rename_variables,[],[4804])).
% 61.18/61.37 cnf(5006,plain,
% 61.18/61.37 (P10(x50061,x50062,x50062,x50061)),
% 61.18/61.37 inference(rename_variables,[],[4340])).
% 61.18/61.37 cnf(5013,plain,
% 61.18/61.37 (P10(x50131,x50132,x50132,x50131)),
% 61.18/61.37 inference(rename_variables,[],[4340])).
% 61.18/61.37 cnf(5018,plain,
% 61.18/61.37 (P10(x50181,x50182,x50181,x50182)),
% 61.18/61.37 inference(rename_variables,[],[4436])).
% 61.18/61.37 cnf(5027,plain,
% 61.18/61.37 (P10(x50271,x50272,x50272,x50271)),
% 61.18/61.37 inference(rename_variables,[],[4340])).
% 61.18/61.37 cnf(5030,plain,
% 61.18/61.37 (P8(x50301,x50302,x50302,x50303,x50303,x50301,x50303,x50303)),
% 61.18/61.37 inference(rename_variables,[],[4792])).
% 61.18/61.37 cnf(5033,plain,
% 61.18/61.37 (P10(x50331,x50332,x50332,x50331)),
% 61.18/61.37 inference(rename_variables,[],[4340])).
% 61.18/61.37 cnf(5041,plain,
% 61.18/61.37 (P10(x50411,x50412,x50412,x50411)),
% 61.18/61.37 inference(rename_variables,[],[4340])).
% 61.18/61.38 cnf(5054,plain,
% 61.18/61.38 (P1(x50541,x50541,x50542)),
% 61.18/61.38 inference(rename_variables,[],[4138])).
% 61.18/61.38 cnf(5089,plain,
% 61.18/61.38 ($false),
% 61.18/61.38 inference(scs_inference,[],[142,4792,5030,4800,4804,4944,4947,4810,4818,4798,4802,4603,4784,4763,4771,4794,4808,4863,4851,4788,4883,4712,4631,4688,4520,4857,4780,4909,4901,4381,4885,4288,4835,4432,4732,4703,4723,4378,4454,4637,4436,5018,367,4507,4340,5006,5013,5027,5033,5041,4138,5054,4679,3733,3968,4134,3837,4719,1701,1878,1996,156,1989,2050,226,256,259,167,225,153,154,257,254,164,258,168,151,166,252,253,165,160,163,152,224,255,185,248,158,157,188,247,200,249,201,176,240,199,181,173,177,223,190,241,184,155,189,227,192,239,195,186,162,228,159,187,169]),
% 61.18/61.38 ['proof']).
% 61.18/61.38 % SZS output end Proof
% 61.18/61.38 % Total time :60.490000s
%------------------------------------------------------------------------------