%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : GEO618+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 : n032.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:57 EDT 2024
% Result : Theorem 59.12s 59.21s
% Output : CNFRefutation 59.14s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.09 % Problem : GEO618+1 : TPTP v8.2.0. Released v7.5.0.
% 0.00/0.09 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% 0.08/0.27 % Computer : n032.cluster.edu
% 0.08/0.27 % Model : x86_64 x86_64
% 0.08/0.27 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.27 % Memory : 8042.1875MB
% 0.08/0.27 % OS : Linux 3.10.0-693.el7.x86_64
% 0.08/0.27 % CPULimit : 300
% 0.08/0.27 % WCLimit : 300
% 0.08/0.27 % DateTime : Fri Jun 21 08:40:38 EDT 2024
% 0.08/0.27 % CPUTime :
% 0.13/0.45 start to proof:theBenchmark
% 59.12/59.20 %-------------------------------------------
% 59.12/59.20 % File :CSE---1.7
% 59.12/59.20 % Problem :theBenchmark
% 59.12/59.20 % Transform :cnf
% 59.12/59.20 % Format :tptp:raw
% 59.12/59.20 % Command :java -jar mcs_scs.jar %d %s
% 59.12/59.20
% 59.12/59.20 % Result :Theorem 58.690000s
% 59.12/59.20 % Output :CNFRefutation 58.690000s
% 59.12/59.20 %-------------------------------------------
% 59.12/59.21 %------------------------------------------------------------------------------
% 59.12/59.21 % File : GEO618+1 : TPTP v8.2.0. Released v7.5.0.
% 59.12/59.21 % Domain : Geometry
% 59.12/59.21 % Problem : JGEX problem 80
% 59.12/59.21 % Version : [CGZ00] axioms.
% 59.12/59.21 % English :
% 59.12/59.21
% 59.12/59.21 % Refs : [CGZ00] Chou et al. (2000), A Deductive Database Approach to A
% 59.12/59.21 % : [YCG08] Ye et al. (2008), An Introduction to Java Geometry Exp
% 59.12/59.21 % : [Qua20] Quaresma (2020), Email to Geoff Sutcliffe
% 59.12/59.21 % Source : [Qua20]
% 59.12/59.21 % Names : 80.p [Qua20]
% 59.12/59.21
% 59.12/59.21 % Status : Theorem
% 59.12/59.21 % Rating : 0.39 v8.2.0, 0.33 v8.1.0, 0.42 v7.5.0
% 59.12/59.21 % Syntax : Number of formulae : 95 ( 0 unt; 0 def)
% 59.12/59.21 % Number of atoms : 289 ( 1 equ)
% 59.12/59.21 % Maximal formula atoms : 8 ( 3 avg)
% 59.12/59.21 % Number of connectives : 201 ( 7 ~; 0 |; 99 &)
% 59.12/59.21 % ( 0 <=>; 95 =>; 0 <=; 0 <~>)
% 59.12/59.21 % Maximal formula depth : 15 ( 9 avg)
% 59.12/59.21 % Maximal term depth : 1 ( 1 avg)
% 59.12/59.21 % Number of predicates : 12 ( 11 usr; 0 prp; 2-8 aty)
% 59.12/59.21 % Number of functors : 0 ( 0 usr; 0 con; --- aty)
% 59.12/59.21 % Number of variables : 528 ( 508 !; 20 ?)
% 59.12/59.21 % SPC : FOF_THM_RFO_SEQ
% 59.12/59.21
% 59.12/59.21 % Comments : Taken from JGEX [YCG08], converted by Pedro Quaresma.
% 59.12/59.21 %------------------------------------------------------------------------------
% 59.12/59.21 include('Axioms/GEO012+0.ax').
% 59.12/59.21 %------------------------------------------------------------------------------
% 59.12/59.21 fof(exemplo6GDDFULL618080,conjecture,
% 59.12/59.21 ! [A,B,C,U,O,T] :
% 59.12/59.21 ( ( eqangle(U,A,A,C,U,A,A,B)
% 59.12/59.21 & coll(U,B,C)
% 59.12/59.21 & circle(O,A,B,C)
% 59.12/59.21 & perp(A,O,A,T)
% 59.12/59.21 & coll(T,B,C) )
% 59.12/59.21 => cong(T,A,T,U) ) ).
% 59.12/59.21
% 59.12/59.21 %------------------------------------------------------------------------------
% 59.12/59.21 %-------------------------------------------
% 59.12/59.21 % Proof found
% 59.12/59.21 % SZS status Theorem for theBenchmark
% 59.12/59.21 % SZS output start Proof
% 59.13/59.22 %ClaNum:260(EqnAxiom:141)
% 59.13/59.22 %VarNum:1613(SingletonVarNum:590)
% 59.13/59.22 %MaxLitNum:5
% 59.13/59.22 %MaxfuncDepth:1
% 59.13/59.22 %SharedTerms:12
% 59.13/59.22 %goalClause: 142 143 144 145 146 147
% 59.14/59.22 %singleGoalClaCount:6
% 59.14/59.22 [142]P1(a1,a2,a16)
% 59.14/59.22 [143]P1(a17,a2,a16)
% 59.14/59.22 [144]P3(a3,a18,a3,a17)
% 59.14/59.22 [145]P2(a18,a3,a2,a16)
% 59.14/59.22 [146]P4(a1,a3,a3,a16,a1,a3,a3,a2)
% 59.14/59.22 [147]~P5(a17,a3,a17,a1)
% 59.14/59.22 [148]~P1(x1482,x1481,x1483)+P1(x1481,x1482,x1483)
% 59.14/59.22 [149]~P1(x1491,x1493,x1492)+P1(x1491,x1492,x1493)
% 59.14/59.22 [150]~P8(x1501,x1502,x1503)+P1(x1501,x1502,x1503)
% 59.14/59.22 [151]~P8(x1511,x1513,x1512)+P8(x1511,x1512,x1513)
% 59.14/59.22 [153]~P8(x1531,x1532,x1533)+P5(x1531,x1532,x1531,x1533)
% 59.14/59.22 [157]~P10(x1571,x1572,x1571,x1573)+P1(x1571,x1572,x1573)
% 59.14/59.22 [223]~P5(x2231,x2232,x2231,x2233)+P4(x2231,x2232,x2232,x2233,x2232,x2233,x2231,x2233)
% 59.14/59.22 [160]~P10(x1603,x1604,x1601,x1602)+P10(x1601,x1602,x1603,x1604)
% 59.14/59.22 [161]~P10(x1611,x1612,x1614,x1613)+P10(x1611,x1612,x1613,x1614)
% 59.14/59.22 [162]~P3(x1623,x1624,x1621,x1622)+P3(x1621,x1622,x1623,x1624)
% 59.14/59.22 [163]~P3(x1631,x1632,x1634,x1633)+P3(x1631,x1632,x1633,x1634)
% 59.14/59.22 [164]~P5(x1643,x1644,x1641,x1642)+P5(x1641,x1642,x1643,x1644)
% 59.14/59.22 [165]~P5(x1651,x1652,x1654,x1653)+P5(x1651,x1652,x1653,x1654)
% 59.14/59.22 [166]~P6(x1662,x1661,x1663,x1664)+P6(x1661,x1662,x1663,x1664)
% 59.14/59.22 [167]~P6(x1671,x1673,x1672,x1674)+P6(x1671,x1672,x1673,x1674)
% 59.14/59.22 [168]~P6(x1681,x1682,x1684,x1683)+P6(x1681,x1682,x1683,x1684)
% 59.14/59.22 [221]~P6(x2212,x2213,x2211,x2214)+P4(x2211,x2212,x2211,x2213,x2214,x2212,x2214,x2213)
% 59.14/59.22 [184]~P2(x1844,x1841,x1842,x1843)+P3(f8(x1841,x1842,x1843,x1844),x1841,x1841,x1844)
% 59.14/59.22 [199]P5(x1991,x1992,x1993,x1994)+~P7(x1991,x1992,x1995,x1993,x1994,x1996)
% 59.14/59.22 [211]~P11(x2114,x2115,x2116,x2111,x2112,x2113)+P11(x2111,x2112,x2113,x2114,x2115,x2116)
% 59.14/59.22 [212]~P11(x2122,x2121,x2123,x2125,x2124,x2126)+P11(x2121,x2122,x2123,x2124,x2125,x2126)
% 59.14/59.22 [213]~P11(x2131,x2133,x2132,x2134,x2136,x2135)+P11(x2131,x2132,x2133,x2134,x2135,x2136)
% 59.14/59.22 [214]~P7(x2144,x2145,x2146,x2141,x2142,x2143)+P7(x2141,x2142,x2143,x2144,x2145,x2146)
% 59.14/59.22 [215]~P7(x2152,x2151,x2153,x2155,x2154,x2156)+P7(x2151,x2152,x2153,x2154,x2155,x2156)
% 59.14/59.22 [216]~P7(x2161,x2163,x2162,x2164,x2166,x2165)+P7(x2161,x2162,x2163,x2164,x2165,x2166)
% 59.14/59.22 [222]~P10(x2221,x2222,x2225,x2226)+P4(x2221,x2222,x2223,x2224,x2225,x2226,x2223,x2224)
% 59.14/59.22 [228]~P11(x2281,x2282,x2283,x2284,x2285,x2286)+P4(x2281,x2282,x2282,x2283,x2284,x2285,x2285,x2286)
% 59.14/59.22 [229]~P11(x2291,x2292,x2293,x2294,x2295,x2296)+P9(x2291,x2292,x2291,x2293,x2294,x2295,x2294,x2296)
% 59.14/59.22 [230]~P4(x2301,x2302,x2305,x2306,x2303,x2304,x2305,x2306)+P10(x2301,x2302,x2303,x2304)
% 59.14/59.22 [249]~P4(x2495,x2496,x2497,x2498,x2491,x2492,x2493,x2494)+P4(x2491,x2492,x2493,x2494,x2495,x2496,x2497,x2498)
% 59.14/59.22 [250]~P4(x2503,x2504,x2501,x2502,x2507,x2508,x2505,x2506)+P4(x2501,x2502,x2503,x2504,x2505,x2506,x2507,x2508)
% 59.14/59.22 [251]~P4(x2512,x2511,x2513,x2514,x2515,x2516,x2517,x2518)+P4(x2511,x2512,x2513,x2514,x2515,x2516,x2517,x2518)
% 59.14/59.22 [252]~P4(x2521,x2522,x2525,x2526,x2523,x2524,x2527,x2528)+P4(x2521,x2522,x2523,x2524,x2525,x2526,x2527,x2528)
% 59.14/59.22 [253]~P9(x2535,x2536,x2537,x2538,x2531,x2532,x2533,x2534)+P9(x2531,x2532,x2533,x2534,x2535,x2536,x2537,x2538)
% 59.14/59.22 [254]~P9(x2543,x2544,x2541,x2542,x2547,x2548,x2545,x2546)+P9(x2541,x2542,x2543,x2544,x2545,x2546,x2547,x2548)
% 59.14/59.22 [255]~P9(x2552,x2551,x2553,x2554,x2555,x2556,x2557,x2558)+P9(x2551,x2552,x2553,x2554,x2555,x2556,x2557,x2558)
% 59.14/59.22 [256]~P9(x2561,x2562,x2565,x2566,x2563,x2564,x2567,x2568)+P9(x2561,x2562,x2563,x2564,x2565,x2566,x2567,x2568)
% 59.14/59.22 [158]~P1(x1581,x1582,x1583)+~P5(x1581,x1582,x1581,x1583)+P8(x1581,x1582,x1583)
% 59.14/59.22 [232]P5(x2321,x2322,x2321,x2323)+~P4(x2321,x2322,x2322,x2323,x2322,x2323,x2321,x2323)+P1(x2321,x2322,x2323)
% 59.14/59.22 [173]~P3(x1731,x1732,x1732,x1733)+~P5(x1732,x1731,x1732,x1733)+P1(x1731,x1732,f4(x1731,x1733,x1732))
% 59.14/59.22 [185]~P3(x1852,x1851,x1851,x1853)+~P5(x1851,x1852,x1851,x1853)+P5(x1851,x1852,x1851,f4(x1852,x1853,x1851))
% 59.14/59.22 [152]~P1(x1523,x1524,x1521)+P1(x1521,x1522,x1523)+~P1(x1523,x1524,x1522)
% 59.14/59.22 [169]~P2(x1694,x1691,x1692,x1693)+P3(x1691,x1692,x1692,x1693)+~P1(x1694,x1691,x1693)
% 59.14/59.22 [170]~P3(x1701,x1704,x1702,x1703)+P5(x1701,x1702,x1701,x1703)+~P8(x1704,x1702,x1703)
% 59.14/59.22 [171]~P3(x1711,x1713,x1713,x1714)+P5(x1711,x1712,x1713,x1712)+~P8(x1712,x1711,x1714)
% 59.14/59.22 [178]~P5(x1781,x1784,x1782,x1784)+~P5(x1781,x1783,x1782,x1783)+P3(x1781,x1782,x1783,x1784)
% 59.14/59.22 [181]~P5(x1811,x1812,x1811,x1814)+~P5(x1811,x1812,x1811,x1813)+P2(x1811,x1812,x1813,x1814)
% 59.14/59.22 [227]~P10(x2271,x2274,x2273,x2272)+~P6(x2271,x2274,x2273,x2272)+P4(x2271,x2272,x2273,x2272,x2273,x2272,x2273,x2274)
% 59.14/59.22 [231]~P4(x2311,x2313,x2311,x2314,x2312,x2313,x2312,x2314)+P1(x2311,x2312,x2313)+P6(x2313,x2314,x2311,x2312)
% 59.14/59.22 [233]~P1(x2333,x2334,x2332)+~P4(x2333,x2331,x2333,x2332,x2334,x2331,x2334,x2332)+P6(x2331,x2332,x2333,x2334)
% 59.14/59.22 [235]P3(x2351,x2352,x2353,x2354)+~P4(x2351,x2352,x2353,x2354,x2353,x2354,x2351,x2352)+P10(x2351,x2352,x2353,x2354)
% 59.14/59.22 [174]~P3(x1741,x1744,x1742,x1743)+~P3(x1742,x1744,x1741,x1743)+P1(f5(x1741,x1742,x1743),x1743,x1742)
% 59.14/59.22 [175]~P3(x1751,x1754,x1752,x1753)+~P3(x1752,x1754,x1751,x1753)+P1(f6(x1751,x1752,x1753),x1753,x1751)
% 59.14/59.22 [186]~P3(x1861,x1864,x1862,x1863)+~P3(x1862,x1864,x1861,x1863)+P3(x1861,f5(x1861,x1862,x1863),x1863,x1862)
% 59.14/59.22 [187]~P3(x1871,x1874,x1872,x1873)+~P3(x1872,x1874,x1871,x1873)+P3(x1871,f6(x1872,x1871,x1873),x1873,x1872)
% 59.14/59.22 [188]~P3(x1881,x1883,x1883,x1882)+~P6(x1881,x1882,x1883,x1884)+P2(f9(x1881,x1882,x1883),x1881,x1882,x1883)
% 59.14/59.22 [190]~P3(x1903,x1904,x1902,x1901)+~P5(x1903,x1902,x1903,x1901)+P1(x1901,x1902,f20(x1902,x1901,x1903,x1904))
% 59.14/59.22 [191]~P3(x1913,x1914,x1911,x1912)+~P5(x1913,x1911,x1913,x1912)+P1(f20(x1911,x1912,x1913,x1914),x1913,x1914)
% 59.14/59.22 [242]~P5(x2423,x2422,x2423,x2421)+~P4(x2422,x2423,x2423,x2424,x2423,x2424,x2423,x2421)+P1(x2421,x2422,f21(x2422,x2421,x2423,x2424))
% 59.14/59.22 [243]~P3(x2433,x2434,x2432,x2431)+~P4(x2432,x2433,x2433,x2434,x2433,x2434,x2433,x2431)+P1(x2431,x2432,f22(x2432,x2431,x2433,x2434))
% 59.14/59.22 [244]~P3(x2443,x2442,x2442,x2441)+~P4(x2444,x2443,x2442,x2443,x2442,x2443,x2441,x2443)+P1(f15(x2441,x2442,x2443,x2444),x2443,x2444)
% 59.14/59.22 [245]~P3(x2453,x2452,x2452,x2451)+~P4(x2454,x2453,x2452,x2453,x2452,x2453,x2451,x2453)+P1(f15(x2451,x2452,x2453,x2454),x2451,x2452)
% 59.14/59.22 [246]~P5(x2463,x2461,x2463,x2462)+~P4(x2461,x2463,x2463,x2464,x2463,x2464,x2463,x2462)+P1(f21(x2461,x2462,x2463,x2464),x2463,x2464)
% 59.14/59.22 [247]~P3(x2473,x2474,x2471,x2472)+~P4(x2471,x2473,x2473,x2474,x2473,x2474,x2473,x2472)+P1(f22(x2471,x2472,x2473,x2474),x2473,x2474)
% 59.14/59.22 [154]~P8(x1545,x1541,x1543)+P10(x1541,x1542,x1543,x1544)+~P8(x1545,x1542,x1544)
% 59.14/59.22 [155]~P8(x1551,x1555,x1553)+P10(x1551,x1552,x1553,x1554)+~P8(x1552,x1555,x1554)
% 59.14/59.22 [182]~P6(x1825,x1821,x1822,x1823)+P6(x1821,x1822,x1823,x1824)+~P6(x1825,x1821,x1822,x1824)
% 59.14/59.22 [224]~P8(x2245,x2242,x2243)+~P2(x2244,x2241,x2242,x2243)+P4(x2241,x2242,x2241,x2243,x2244,x2242,x2244,x2245)
% 59.14/59.22 [226]~P2(x2265,x2261,x2263,x2264)+P4(x2261,x2262,x2261,x2263,x2264,x2261,x2264,x2263)+~P3(x2265,x2261,x2261,x2262)
% 59.14/59.22 [239]~P4(x2392,x2393,x2392,x2394,x2395,x2392,x2395,x2394)+P3(x2391,x2392,x2392,x2393)+~P2(x2391,x2392,x2394,x2395)
% 59.14/59.22 [194]~P1(x1942,x1944,x1945)+~P3(x1941,x1943,x1943,x1942)+P1(f13(x1941,x1942,x1943,x1944,x1945),x1944,x1945)
% 59.14/59.22 [195]~P1(x1952,x1954,x1955)+~P3(x1951,x1953,x1953,x1952)+P3(f13(x1951,x1952,x1953,x1954,x1955),x1951,x1954,x1955)
% 59.14/59.22 [196]~P3(x1963,x1964,x1964,x1961)+~P5(x1961,x1962,x1961,x1965)+P5(x1961,x1962,x1961,f25(x1963,x1964,x1962,x1965,x1961))
% 59.14/59.22 [197]~P3(x1973,x1971,x1971,x1975)+~P5(x1975,x1972,x1975,x1974)+P5(x1971,x1972,x1971,f25(x1973,x1971,x1972,x1974,x1975))
% 59.14/59.22 [198]~P3(x1981,x1982,x1982,x1985)+~P5(x1985,x1983,x1985,x1984)+P10(f25(x1981,x1982,x1983,x1984,x1985),x1983,x1981,x1982)
% 59.14/59.22 [241]~P4(x2411,x2413,x2412,x2413,x2411,x2414,x2412,x2415)+P1(x2411,x2412,x2413)+P6(x2414,x2412,x2413,f24(x2411,x2412,x2413,x2414))
% 59.14/59.22 [257]~P4(x2571,x2573,x2572,x2573,x2571,x2574,x2572,x2575)+P1(x2571,x2572,x2573)+P4(x2571,x2573,x2572,x2573,x2571,f24(x2571,x2572,x2573,x2574),x2572,f24(x2571,x2572,x2573,x2574))
% 59.14/59.22 [176]~P10(x1761,x1762,x1765,x1766)+P10(x1761,x1762,x1763,x1764)+~P10(x1765,x1766,x1763,x1764)
% 59.14/59.22 [177]~P3(x1771,x1772,x1775,x1776)+P10(x1771,x1772,x1773,x1774)+~P3(x1775,x1776,x1773,x1774)
% 59.14/59.22 [179]~P3(x1795,x1796,x1793,x1794)+P3(x1791,x1792,x1793,x1794)+~P10(x1791,x1792,x1795,x1796)
% 59.14/59.22 [180]~P5(x1801,x1802,x1805,x1806)+P5(x1801,x1802,x1803,x1804)+~P5(x1805,x1806,x1803,x1804)
% 59.14/59.22 [217]~P5(x2171,x2172,x2174,x2175)+~P11(x2171,x2172,x2173,x2174,x2175,x2176)+P7(x2171,x2172,x2173,x2174,x2175,x2176)
% 59.14/59.22 [220]~P8(x2204,x2205,x2206)+~P8(x2201,x2202,x2203)+P9(x2201,x2202,x2202,x2203,x2204,x2205,x2205,x2206)
% 59.14/59.22 [200]~P8(x2006,x2003,x2004)+~P8(x2005,x2001,x2002)+P8(f23(x2001,x2002,x2003,x2004,x2005,x2006),x2001,x2004)
% 59.14/59.22 [201]~P8(x2016,x2013,x2014)+~P8(x2015,x2011,x2012)+P10(f23(x2011,x2012,x2013,x2014,x2015,x2016),x2016,x2011,x2013)
% 59.14/59.22 [202]~P8(x2026,x2023,x2024)+~P8(x2025,x2021,x2022)+P10(f23(x2021,x2022,x2023,x2024,x2025,x2026),x2025,x2022,x2024)
% 59.14/59.22 [237]~P4(x2371,x2372,x2373,x2374,x2375,x2376,x2377,x2378)+P10(x2371,x2372,x2373,x2374)+~P10(x2375,x2376,x2377,x2378)
% 59.14/59.22 [238]~P4(x2381,x2382,x2383,x2384,x2385,x2386,x2387,x2388)+P3(x2381,x2382,x2383,x2384)+~P3(x2385,x2386,x2387,x2388)
% 59.14/59.22 [240]~P9(x2401,x2402,x2403,x2404,x2405,x2406,x2407,x2408)+P5(x2401,x2402,x2403,x2404)+~P5(x2405,x2406,x2407,x2408)
% 59.14/59.22 [218]~P11(x2181,x2182,x2183,x2187,x2188,x2189)+P11(x2181,x2182,x2183,x2184,x2185,x2186)+~P11(x2187,x2188,x2189,x2184,x2185,x2186)
% 59.14/59.22 [219]~P7(x2191,x2192,x2193,x2197,x2198,x2199)+P7(x2191,x2192,x2193,x2194,x2195,x2196)+~P7(x2197,x2198,x2199,x2194,x2195,x2196)
% 59.14/59.22 [259]~P4(x2591,x2592,x2593,x2594,x2599,x25910,x25911,x25912)+P4(x2591,x2592,x2593,x2594,x2595,x2596,x2597,x2598)+~P4(x2599,x25910,x25911,x25912,x2595,x2596,x2597,x2598)
% 59.14/59.22 [260]~P9(x2601,x2602,x2603,x2604,x2609,x26010,x26011,x26012)+P9(x2601,x2602,x2603,x2604,x2605,x2606,x2607,x2608)+~P9(x2609,x26010,x26011,x26012,x2605,x2606,x2607,x2608)
% 59.14/59.22 [192]~P5(x1922,x1921,x1924,x1921)+~P6(x1922,x1924,x1921,x1923)+P3(x1921,x1922,x1922,x1923)+~P5(x1922,x1923,x1924,x1923)
% 59.14/59.22 [159]~P1(x1591,x1592,x1593)+~P10(x1594,x1591,x1595,x1593)+P8(x1591,x1592,x1593)+~P8(x1594,x1592,x1595)
% 59.14/59.22 [172]~P10(x1724,x1723,x1725,x1722)+~P10(x1724,x1722,x1725,x1723)+P8(x1721,x1722,x1723)+~P8(x1721,x1724,x1725)
% 59.14/59.22 [193]~P5(x1935,x1931,x1935,x1933)+~P5(x1935,x1931,x1935,x1932)+P6(x1931,x1932,x1933,x1934)+~P5(x1935,x1931,x1935,x1934)
% 59.14/59.22 [225]~P1(x2251,x2254,x2255)+~P1(x2251,x2252,x2253)+~P10(x2252,x2254,x2253,x2255)+P9(x2251,x2252,x2252,x2253,x2251,x2254,x2254,x2255)
% 59.14/59.22 [236]~P1(x2361,x2362,x2363)+~P4(x2365,x2362,x2365,x2363,x2364,x2362,x2364,x2361)+P8(x2361,x2362,x2363)+~P2(x2364,x2365,x2362,x2363)
% 59.14/59.22 [183]~P3(x1833,x1831,x1833,x1835)+~P3(x1831,x1832,x1831,x1833)+~P8(x1834,x1832,x1835)+P8(f7(x1831,x1832,x1833),x1831,x1833)
% 59.14/59.22 [189]~P6(x1891,x1892,x1893,x1895)+~P10(x1891,x1892,x1893,x1895)+~P8(x1894,x1891,x1892)+P2(f10(x1891,x1892,x1893),x1891,x1892,x1893)
% 59.14/59.22 [258]~P4(x2581,x2583,x2582,x2583,x2584,x2586,x2585,x2586)+~P4(x2581,x2582,x2582,x2583,x2584,x2585,x2585,x2586)+P1(x2581,x2582,x2583)+P11(x2581,x2582,x2583,x2584,x2585,x2586)
% 59.14/59.22 [248]~P6(x2481,x2482,x2485,x2484)+~P6(x2481,x2482,x2485,x2483)+~P4(x2485,x2481,x2485,x2482,x2486,x2483,x2486,x2484)+P5(x2481,x2482,x2483,x2484)+~P6(x2481,x2482,x2485,x2486)
% 59.14/59.22 [203]~P1(x2032,x2033,x2034)+~P1(x2031,x2034,x2036)+~P1(x2031,x2033,x2035)+~P10(x2033,x2034,x2035,x2036)+P1(x2031,x2032,f14(x2033,x2034,x2035,x2036,x2031,x2032))
% 59.14/59.22 [204]~P1(x2046,x2041,x2042)+~P1(x2045,x2042,x2044)+~P1(x2045,x2041,x2043)+~P10(x2041,x2042,x2043,x2044)+P1(f14(x2041,x2042,x2043,x2044,x2045,x2046),x2043,x2044)
% 59.14/59.22 [205]~P1(x2053,x2054,x2055)+~P8(x2056,x2051,x2052)+~P10(x2051,x2053,x2055,x2056)+~P10(x2051,x2053,x2052,x2054)+P1(f26(x2051,x2052,x2053,x2054,x2055,x2056),x2056,x2055)
% 59.14/59.22 [206]~P1(x2063,x2064,x2065)+~P8(x2066,x2061,x2062)+~P10(x2061,x2063,x2065,x2066)+~P10(x2061,x2063,x2062,x2064)+P1(f26(x2061,x2062,x2063,x2064,x2065,x2066),x2061,x2064)
% 59.14/59.22 [207]~P5(x2072,x2073,x2072,x2074)+~P5(x2071,x2073,x2071,x2076)+~P2(x2071,x2073,x2074,x2075)+E(x2071,x2072)+P1(f11(x2073,x2074,x2075,x2076,x2071,x2072),x2073,x2075)
% 59.14/59.22 [208]~P5(x2082,x2083,x2082,x2084)+~P5(x2081,x2083,x2081,x2086)+~P2(x2081,x2083,x2084,x2085)+E(x2081,x2082)+P1(f12(x2083,x2084,x2085,x2086,x2081,x2082),x2084,x2086)
% 59.14/59.22 [209]~P5(x2092,x2093,x2092,x2094)+~P5(x2091,x2093,x2091,x2096)+~P2(x2091,x2093,x2094,x2095)+E(x2091,x2092)+P5(f11(x2093,x2094,x2095,x2096,x2091,x2092),x2092,x2092,x2093)
% 59.14/59.22 [210]~P5(x2102,x2103,x2102,x2104)+~P5(x2101,x2103,x2101,x2106)+~P2(x2101,x2103,x2104,x2105)+E(x2101,x2102)+P5(f12(x2103,x2104,x2105,x2106,x2101,x2102),x2102,x2102,x2103)
% 59.14/59.22 [156]~P1(x1563,x1561,x1564)+~P1(x1565,x1561,x1564)+~P8(x1566,x1565,x1563)+~P8(x1567,x1561,x1564)+P8(f19(x1561,x1562),x1561,x1562)
% 59.14/59.22 %EqnAxiom
% 59.14/59.22 [1]E(x11,x11)
% 59.14/59.22 [2]E(x22,x21)+~E(x21,x22)
% 59.14/59.22 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 59.14/59.22 [4]~E(x41,x42)+E(f19(x41,x43),f19(x42,x43))
% 59.14/59.22 [5]~E(x51,x52)+E(f19(x53,x51),f19(x53,x52))
% 59.14/59.22 [6]~E(x61,x62)+E(f4(x61,x63,x64),f4(x62,x63,x64))
% 59.14/59.22 [7]~E(x71,x72)+E(f4(x73,x71,x74),f4(x73,x72,x74))
% 59.14/59.22 [8]~E(x81,x82)+E(f4(x83,x84,x81),f4(x83,x84,x82))
% 59.14/59.22 [9]~E(x91,x92)+E(f5(x91,x93,x94),f5(x92,x93,x94))
% 59.14/59.22 [10]~E(x101,x102)+E(f5(x103,x101,x104),f5(x103,x102,x104))
% 59.14/59.22 [11]~E(x111,x112)+E(f5(x113,x114,x111),f5(x113,x114,x112))
% 59.14/59.22 [12]~E(x121,x122)+E(f6(x121,x123,x124),f6(x122,x123,x124))
% 59.14/59.22 [13]~E(x131,x132)+E(f6(x133,x131,x134),f6(x133,x132,x134))
% 59.14/59.22 [14]~E(x141,x142)+E(f6(x143,x144,x141),f6(x143,x144,x142))
% 59.14/59.22 [15]~E(x151,x152)+E(f7(x151,x153,x154),f7(x152,x153,x154))
% 59.14/59.22 [16]~E(x161,x162)+E(f7(x163,x161,x164),f7(x163,x162,x164))
% 59.14/59.22 [17]~E(x171,x172)+E(f7(x173,x174,x171),f7(x173,x174,x172))
% 59.14/59.22 [18]~E(x181,x182)+E(f8(x181,x183,x184,x185),f8(x182,x183,x184,x185))
% 59.14/59.22 [19]~E(x191,x192)+E(f8(x193,x191,x194,x195),f8(x193,x192,x194,x195))
% 59.14/59.22 [20]~E(x201,x202)+E(f8(x203,x204,x201,x205),f8(x203,x204,x202,x205))
% 59.14/59.22 [21]~E(x211,x212)+E(f8(x213,x214,x215,x211),f8(x213,x214,x215,x212))
% 59.14/59.22 [22]~E(x221,x222)+E(f24(x221,x223,x224,x225),f24(x222,x223,x224,x225))
% 59.14/59.22 [23]~E(x231,x232)+E(f24(x233,x231,x234,x235),f24(x233,x232,x234,x235))
% 59.14/59.22 [24]~E(x241,x242)+E(f24(x243,x244,x241,x245),f24(x243,x244,x242,x245))
% 59.14/59.22 [25]~E(x251,x252)+E(f24(x253,x254,x255,x251),f24(x253,x254,x255,x252))
% 59.14/59.22 [26]~E(x261,x262)+E(f21(x261,x263,x264,x265),f21(x262,x263,x264,x265))
% 59.14/59.22 [27]~E(x271,x272)+E(f21(x273,x271,x274,x275),f21(x273,x272,x274,x275))
% 59.14/59.22 [28]~E(x281,x282)+E(f21(x283,x284,x281,x285),f21(x283,x284,x282,x285))
% 59.14/59.22 [29]~E(x291,x292)+E(f21(x293,x294,x295,x291),f21(x293,x294,x295,x292))
% 59.14/59.22 [30]~E(x301,x302)+E(f22(x301,x303,x304,x305),f22(x302,x303,x304,x305))
% 59.14/59.22 [31]~E(x311,x312)+E(f22(x313,x311,x314,x315),f22(x313,x312,x314,x315))
% 59.14/59.22 [32]~E(x321,x322)+E(f22(x323,x324,x321,x325),f22(x323,x324,x322,x325))
% 59.14/59.22 [33]~E(x331,x332)+E(f22(x333,x334,x335,x331),f22(x333,x334,x335,x332))
% 59.14/59.22 [34]~E(x341,x342)+E(f9(x341,x343,x344),f9(x342,x343,x344))
% 59.14/59.22 [35]~E(x351,x352)+E(f9(x353,x351,x354),f9(x353,x352,x354))
% 59.14/59.22 [36]~E(x361,x362)+E(f9(x363,x364,x361),f9(x363,x364,x362))
% 59.14/59.22 [37]~E(x371,x372)+E(f10(x371,x373,x374),f10(x372,x373,x374))
% 59.14/59.22 [38]~E(x381,x382)+E(f10(x383,x381,x384),f10(x383,x382,x384))
% 59.14/59.22 [39]~E(x391,x392)+E(f10(x393,x394,x391),f10(x393,x394,x392))
% 59.14/59.22 [40]~E(x401,x402)+E(f20(x401,x403,x404,x405),f20(x402,x403,x404,x405))
% 59.14/59.22 [41]~E(x411,x412)+E(f20(x413,x411,x414,x415),f20(x413,x412,x414,x415))
% 59.14/59.22 [42]~E(x421,x422)+E(f20(x423,x424,x421,x425),f20(x423,x424,x422,x425))
% 59.14/59.22 [43]~E(x431,x432)+E(f20(x433,x434,x435,x431),f20(x433,x434,x435,x432))
% 59.14/59.22 [44]~E(x441,x442)+E(f15(x441,x443,x444,x445),f15(x442,x443,x444,x445))
% 59.14/59.22 [45]~E(x451,x452)+E(f15(x453,x451,x454,x455),f15(x453,x452,x454,x455))
% 59.14/59.22 [46]~E(x461,x462)+E(f15(x463,x464,x461,x465),f15(x463,x464,x462,x465))
% 59.14/59.22 [47]~E(x471,x472)+E(f15(x473,x474,x475,x471),f15(x473,x474,x475,x472))
% 59.14/59.22 [48]~E(x481,x482)+E(f13(x481,x483,x484,x485,x486),f13(x482,x483,x484,x485,x486))
% 59.14/59.22 [49]~E(x491,x492)+E(f13(x493,x491,x494,x495,x496),f13(x493,x492,x494,x495,x496))
% 59.14/59.22 [50]~E(x501,x502)+E(f13(x503,x504,x501,x505,x506),f13(x503,x504,x502,x505,x506))
% 59.14/59.22 [51]~E(x511,x512)+E(f13(x513,x514,x515,x511,x516),f13(x513,x514,x515,x512,x516))
% 59.14/59.22 [52]~E(x521,x522)+E(f13(x523,x524,x525,x526,x521),f13(x523,x524,x525,x526,x522))
% 59.14/59.22 [53]~E(x531,x532)+E(f12(x531,x533,x534,x535,x536,x537),f12(x532,x533,x534,x535,x536,x537))
% 59.14/59.22 [54]~E(x541,x542)+E(f12(x543,x541,x544,x545,x546,x547),f12(x543,x542,x544,x545,x546,x547))
% 59.14/59.22 [55]~E(x551,x552)+E(f12(x553,x554,x551,x555,x556,x557),f12(x553,x554,x552,x555,x556,x557))
% 59.14/59.22 [56]~E(x561,x562)+E(f12(x563,x564,x565,x561,x566,x567),f12(x563,x564,x565,x562,x566,x567))
% 59.14/59.22 [57]~E(x571,x572)+E(f12(x573,x574,x575,x576,x571,x577),f12(x573,x574,x575,x576,x572,x577))
% 59.14/59.22 [58]~E(x581,x582)+E(f12(x583,x584,x585,x586,x587,x581),f12(x583,x584,x585,x586,x587,x582))
% 59.14/59.22 [59]~E(x591,x592)+E(f25(x591,x593,x594,x595,x596),f25(x592,x593,x594,x595,x596))
% 59.14/59.22 [60]~E(x601,x602)+E(f25(x603,x601,x604,x605,x606),f25(x603,x602,x604,x605,x606))
% 59.14/59.22 [61]~E(x611,x612)+E(f25(x613,x614,x611,x615,x616),f25(x613,x614,x612,x615,x616))
% 59.14/59.22 [62]~E(x621,x622)+E(f25(x623,x624,x625,x621,x626),f25(x623,x624,x625,x622,x626))
% 59.14/59.22 [63]~E(x631,x632)+E(f25(x633,x634,x635,x636,x631),f25(x633,x634,x635,x636,x632))
% 59.14/59.22 [64]~E(x641,x642)+E(f11(x641,x643,x644,x645,x646,x647),f11(x642,x643,x644,x645,x646,x647))
% 59.14/59.22 [65]~E(x651,x652)+E(f11(x653,x651,x654,x655,x656,x657),f11(x653,x652,x654,x655,x656,x657))
% 59.14/59.22 [66]~E(x661,x662)+E(f11(x663,x664,x661,x665,x666,x667),f11(x663,x664,x662,x665,x666,x667))
% 59.14/59.22 [67]~E(x671,x672)+E(f11(x673,x674,x675,x671,x676,x677),f11(x673,x674,x675,x672,x676,x677))
% 59.14/59.22 [68]~E(x681,x682)+E(f11(x683,x684,x685,x686,x681,x687),f11(x683,x684,x685,x686,x682,x687))
% 59.14/59.22 [69]~E(x691,x692)+E(f11(x693,x694,x695,x696,x697,x691),f11(x693,x694,x695,x696,x697,x692))
% 59.14/59.22 [70]~E(x701,x702)+E(f26(x701,x703,x704,x705,x706,x707),f26(x702,x703,x704,x705,x706,x707))
% 59.14/59.22 [71]~E(x711,x712)+E(f26(x713,x711,x714,x715,x716,x717),f26(x713,x712,x714,x715,x716,x717))
% 59.14/59.23 [72]~E(x721,x722)+E(f26(x723,x724,x721,x725,x726,x727),f26(x723,x724,x722,x725,x726,x727))
% 59.14/59.23 [73]~E(x731,x732)+E(f26(x733,x734,x735,x731,x736,x737),f26(x733,x734,x735,x732,x736,x737))
% 59.14/59.23 [74]~E(x741,x742)+E(f26(x743,x744,x745,x746,x741,x747),f26(x743,x744,x745,x746,x742,x747))
% 59.14/59.23 [75]~E(x751,x752)+E(f26(x753,x754,x755,x756,x757,x751),f26(x753,x754,x755,x756,x757,x752))
% 59.14/59.23 [76]~E(x761,x762)+E(f23(x761,x763,x764,x765,x766,x767),f23(x762,x763,x764,x765,x766,x767))
% 59.14/59.23 [77]~E(x771,x772)+E(f23(x773,x771,x774,x775,x776,x777),f23(x773,x772,x774,x775,x776,x777))
% 59.14/59.23 [78]~E(x781,x782)+E(f23(x783,x784,x781,x785,x786,x787),f23(x783,x784,x782,x785,x786,x787))
% 59.14/59.23 [79]~E(x791,x792)+E(f23(x793,x794,x795,x791,x796,x797),f23(x793,x794,x795,x792,x796,x797))
% 59.14/59.23 [80]~E(x801,x802)+E(f23(x803,x804,x805,x806,x801,x807),f23(x803,x804,x805,x806,x802,x807))
% 59.14/59.23 [81]~E(x811,x812)+E(f23(x813,x814,x815,x816,x817,x811),f23(x813,x814,x815,x816,x817,x812))
% 59.14/59.23 [82]~E(x821,x822)+E(f14(x821,x823,x824,x825,x826,x827),f14(x822,x823,x824,x825,x826,x827))
% 59.14/59.23 [83]~E(x831,x832)+E(f14(x833,x831,x834,x835,x836,x837),f14(x833,x832,x834,x835,x836,x837))
% 59.14/59.23 [84]~E(x841,x842)+E(f14(x843,x844,x841,x845,x846,x847),f14(x843,x844,x842,x845,x846,x847))
% 59.14/59.23 [85]~E(x851,x852)+E(f14(x853,x854,x855,x851,x856,x857),f14(x853,x854,x855,x852,x856,x857))
% 59.14/59.23 [86]~E(x861,x862)+E(f14(x863,x864,x865,x866,x861,x867),f14(x863,x864,x865,x866,x862,x867))
% 59.14/59.23 [87]~E(x871,x872)+E(f14(x873,x874,x875,x876,x877,x871),f14(x873,x874,x875,x876,x877,x872))
% 59.14/59.23 [88]P1(x882,x883,x884)+~E(x881,x882)+~P1(x881,x883,x884)
% 59.14/59.23 [89]P1(x893,x892,x894)+~E(x891,x892)+~P1(x893,x891,x894)
% 59.14/59.23 [90]P1(x903,x904,x902)+~E(x901,x902)+~P1(x903,x904,x901)
% 59.14/59.23 [91]P9(x912,x913,x914,x915,x916,x917,x918,x919)+~E(x911,x912)+~P9(x911,x913,x914,x915,x916,x917,x918,x919)
% 59.14/59.23 [92]P9(x923,x922,x924,x925,x926,x927,x928,x929)+~E(x921,x922)+~P9(x923,x921,x924,x925,x926,x927,x928,x929)
% 59.14/59.23 [93]P9(x933,x934,x932,x935,x936,x937,x938,x939)+~E(x931,x932)+~P9(x933,x934,x931,x935,x936,x937,x938,x939)
% 59.14/59.23 [94]P9(x943,x944,x945,x942,x946,x947,x948,x949)+~E(x941,x942)+~P9(x943,x944,x945,x941,x946,x947,x948,x949)
% 59.14/59.23 [95]P9(x953,x954,x955,x956,x952,x957,x958,x959)+~E(x951,x952)+~P9(x953,x954,x955,x956,x951,x957,x958,x959)
% 59.14/59.23 [96]P9(x963,x964,x965,x966,x967,x962,x968,x969)+~E(x961,x962)+~P9(x963,x964,x965,x966,x967,x961,x968,x969)
% 59.14/59.23 [97]P9(x973,x974,x975,x976,x977,x978,x972,x979)+~E(x971,x972)+~P9(x973,x974,x975,x976,x977,x978,x971,x979)
% 59.14/59.23 [98]P9(x983,x984,x985,x986,x987,x988,x989,x982)+~E(x981,x982)+~P9(x983,x984,x985,x986,x987,x988,x989,x981)
% 59.14/59.23 [99]P3(x992,x993,x994,x995)+~E(x991,x992)+~P3(x991,x993,x994,x995)
% 59.14/59.23 [100]P3(x1003,x1002,x1004,x1005)+~E(x1001,x1002)+~P3(x1003,x1001,x1004,x1005)
% 59.14/59.23 [101]P3(x1013,x1014,x1012,x1015)+~E(x1011,x1012)+~P3(x1013,x1014,x1011,x1015)
% 59.14/59.23 [102]P3(x1023,x1024,x1025,x1022)+~E(x1021,x1022)+~P3(x1023,x1024,x1025,x1021)
% 59.14/59.23 [103]P2(x1032,x1033,x1034,x1035)+~E(x1031,x1032)+~P2(x1031,x1033,x1034,x1035)
% 59.14/59.23 [104]P2(x1043,x1042,x1044,x1045)+~E(x1041,x1042)+~P2(x1043,x1041,x1044,x1045)
% 59.14/59.23 [105]P2(x1053,x1054,x1052,x1055)+~E(x1051,x1052)+~P2(x1053,x1054,x1051,x1055)
% 59.14/59.23 [106]P2(x1063,x1064,x1065,x1062)+~E(x1061,x1062)+~P2(x1063,x1064,x1065,x1061)
% 59.14/59.23 [107]P4(x1072,x1073,x1074,x1075,x1076,x1077,x1078,x1079)+~E(x1071,x1072)+~P4(x1071,x1073,x1074,x1075,x1076,x1077,x1078,x1079)
% 59.14/59.23 [108]P4(x1083,x1082,x1084,x1085,x1086,x1087,x1088,x1089)+~E(x1081,x1082)+~P4(x1083,x1081,x1084,x1085,x1086,x1087,x1088,x1089)
% 59.14/59.23 [109]P4(x1093,x1094,x1092,x1095,x1096,x1097,x1098,x1099)+~E(x1091,x1092)+~P4(x1093,x1094,x1091,x1095,x1096,x1097,x1098,x1099)
% 59.14/59.23 [110]P4(x1103,x1104,x1105,x1102,x1106,x1107,x1108,x1109)+~E(x1101,x1102)+~P4(x1103,x1104,x1105,x1101,x1106,x1107,x1108,x1109)
% 59.14/59.23 [111]P4(x1113,x1114,x1115,x1116,x1112,x1117,x1118,x1119)+~E(x1111,x1112)+~P4(x1113,x1114,x1115,x1116,x1111,x1117,x1118,x1119)
% 59.14/59.23 [112]P4(x1123,x1124,x1125,x1126,x1127,x1122,x1128,x1129)+~E(x1121,x1122)+~P4(x1123,x1124,x1125,x1126,x1127,x1121,x1128,x1129)
% 59.14/59.23 [113]P4(x1133,x1134,x1135,x1136,x1137,x1138,x1132,x1139)+~E(x1131,x1132)+~P4(x1133,x1134,x1135,x1136,x1137,x1138,x1131,x1139)
% 59.14/59.23 [114]P4(x1143,x1144,x1145,x1146,x1147,x1148,x1149,x1142)+~E(x1141,x1142)+~P4(x1143,x1144,x1145,x1146,x1147,x1148,x1149,x1141)
% 59.14/59.23 [115]P5(x1152,x1153,x1154,x1155)+~E(x1151,x1152)+~P5(x1151,x1153,x1154,x1155)
% 59.14/59.23 [116]P5(x1163,x1162,x1164,x1165)+~E(x1161,x1162)+~P5(x1163,x1161,x1164,x1165)
% 59.14/59.23 [117]P5(x1173,x1174,x1172,x1175)+~E(x1171,x1172)+~P5(x1173,x1174,x1171,x1175)
% 59.14/59.23 [118]P5(x1183,x1184,x1185,x1182)+~E(x1181,x1182)+~P5(x1183,x1184,x1185,x1181)
% 59.14/59.23 [119]P7(x1192,x1193,x1194,x1195,x1196,x1197)+~E(x1191,x1192)+~P7(x1191,x1193,x1194,x1195,x1196,x1197)
% 59.14/59.23 [120]P7(x1203,x1202,x1204,x1205,x1206,x1207)+~E(x1201,x1202)+~P7(x1203,x1201,x1204,x1205,x1206,x1207)
% 59.14/59.23 [121]P7(x1213,x1214,x1212,x1215,x1216,x1217)+~E(x1211,x1212)+~P7(x1213,x1214,x1211,x1215,x1216,x1217)
% 59.14/59.23 [122]P7(x1223,x1224,x1225,x1222,x1226,x1227)+~E(x1221,x1222)+~P7(x1223,x1224,x1225,x1221,x1226,x1227)
% 59.14/59.23 [123]P7(x1233,x1234,x1235,x1236,x1232,x1237)+~E(x1231,x1232)+~P7(x1233,x1234,x1235,x1236,x1231,x1237)
% 59.14/59.23 [124]P7(x1243,x1244,x1245,x1246,x1247,x1242)+~E(x1241,x1242)+~P7(x1243,x1244,x1245,x1246,x1247,x1241)
% 59.14/59.23 [125]P6(x1252,x1253,x1254,x1255)+~E(x1251,x1252)+~P6(x1251,x1253,x1254,x1255)
% 59.14/59.23 [126]P6(x1263,x1262,x1264,x1265)+~E(x1261,x1262)+~P6(x1263,x1261,x1264,x1265)
% 59.14/59.23 [127]P6(x1273,x1274,x1272,x1275)+~E(x1271,x1272)+~P6(x1273,x1274,x1271,x1275)
% 59.14/59.23 [128]P6(x1283,x1284,x1285,x1282)+~E(x1281,x1282)+~P6(x1283,x1284,x1285,x1281)
% 59.14/59.23 [129]P10(x1292,x1293,x1294,x1295)+~E(x1291,x1292)+~P10(x1291,x1293,x1294,x1295)
% 59.14/59.23 [130]P10(x1303,x1302,x1304,x1305)+~E(x1301,x1302)+~P10(x1303,x1301,x1304,x1305)
% 59.14/59.23 [131]P10(x1313,x1314,x1312,x1315)+~E(x1311,x1312)+~P10(x1313,x1314,x1311,x1315)
% 59.14/59.23 [132]P10(x1323,x1324,x1325,x1322)+~E(x1321,x1322)+~P10(x1323,x1324,x1325,x1321)
% 59.14/59.23 [133]P11(x1332,x1333,x1334,x1335,x1336,x1337)+~E(x1331,x1332)+~P11(x1331,x1333,x1334,x1335,x1336,x1337)
% 59.14/59.23 [134]P11(x1343,x1342,x1344,x1345,x1346,x1347)+~E(x1341,x1342)+~P11(x1343,x1341,x1344,x1345,x1346,x1347)
% 59.14/59.23 [135]P11(x1353,x1354,x1352,x1355,x1356,x1357)+~E(x1351,x1352)+~P11(x1353,x1354,x1351,x1355,x1356,x1357)
% 59.14/59.23 [136]P11(x1363,x1364,x1365,x1362,x1366,x1367)+~E(x1361,x1362)+~P11(x1363,x1364,x1365,x1361,x1366,x1367)
% 59.14/59.23 [137]P11(x1373,x1374,x1375,x1376,x1372,x1377)+~E(x1371,x1372)+~P11(x1373,x1374,x1375,x1376,x1371,x1377)
% 59.14/59.23 [138]P11(x1383,x1384,x1385,x1386,x1387,x1382)+~E(x1381,x1382)+~P11(x1383,x1384,x1385,x1386,x1387,x1381)
% 59.14/59.23 [139]P8(x1392,x1393,x1394)+~E(x1391,x1392)+~P8(x1391,x1393,x1394)
% 59.14/59.23 [140]P8(x1403,x1402,x1404)+~E(x1401,x1402)+~P8(x1403,x1401,x1404)
% 59.14/59.23 [141]P8(x1413,x1414,x1412)+~E(x1411,x1412)+~P8(x1413,x1414,x1411)
% 59.14/59.23
% 59.14/59.23 %-------------------------------------------
% 59.14/59.23 cnf(261,plain,
% 59.14/59.23 (~P8(a17,a3,a1)),
% 59.14/59.23 inference(scs_inference,[],[147,153])).
% 59.14/59.23 cnf(263,plain,
% 59.14/59.23 (~P5(a17,a1,a17,a3)),
% 59.14/59.23 inference(scs_inference,[],[147,153,164])).
% 59.14/59.23 cnf(265,plain,
% 59.14/59.23 (~P5(a17,a3,a1,a17)),
% 59.14/59.23 inference(scs_inference,[],[147,153,164,165])).
% 59.14/59.23 cnf(271,plain,
% 59.14/59.23 (~P7(a17,a1,x2711,a17,a3,x2712)),
% 59.14/59.23 inference(scs_inference,[],[147,153,164,165,199,151,214])).
% 59.14/59.23 cnf(273,plain,
% 59.14/59.23 (~P7(a3,a17,x2731,a1,a17,x2732)),
% 59.14/59.23 inference(scs_inference,[],[147,153,164,165,199,151,214,215])).
% 59.14/59.23 cnf(275,plain,
% 59.14/59.23 (~P7(a17,x2751,a3,a17,x2752,a1)),
% 59.14/59.23 inference(scs_inference,[],[147,153,164,165,199,151,214,215,216])).
% 59.14/59.23 cnf(277,plain,
% 59.14/59.23 (P1(a16,a16,a1)),
% 59.14/59.23 inference(scs_inference,[],[142,147,153,164,165,199,151,214,215,216,152])).
% 59.14/59.23 cnf(279,plain,
% 59.14/59.23 (~P8(x2791,a3,a1)+~P3(a17,x2791,a3,a1)),
% 59.14/59.23 inference(scs_inference,[],[142,147,153,164,165,199,151,214,215,216,152,170])).
% 59.14/59.23 cnf(281,plain,
% 59.14/59.23 (~P3(x2811,x2812,a3,a18)+P10(x2811,x2812,a3,a17)),
% 59.14/59.23 inference(scs_inference,[],[142,144,147,153,164,165,199,151,214,215,216,152,170,177])).
% 59.14/59.23 cnf(287,plain,
% 59.14/59.23 (~P5(a17,a1,a3,a17)),
% 59.14/59.23 inference(scs_inference,[],[263,271,215,165])).
% 59.14/59.23 cnf(289,plain,
% 59.14/59.23 (~P7(a17,x2891,a1,a17,x2892,a3)),
% 59.14/59.23 inference(scs_inference,[],[263,271,275,215,165,214])).
% 59.14/59.23 cnf(291,plain,
% 59.14/59.23 (~P7(a17,a3,x2911,a1,a17,x2912)),
% 59.14/59.23 inference(scs_inference,[],[263,265,271,275,215,165,214,199])).
% 59.14/59.23 cnf(293,plain,
% 59.14/59.23 (~P5(a1,a17,a17,a3)),
% 59.14/59.23 inference(scs_inference,[],[263,265,271,275,215,165,214,199,164])).
% 59.14/59.23 cnf(295,plain,
% 59.14/59.23 (~P7(a3,x2951,a17,a1,x2952,a17)),
% 59.14/59.23 inference(scs_inference,[],[263,265,271,273,275,215,165,214,199,164,216])).
% 59.14/59.23 cnf(297,plain,
% 59.14/59.23 (P1(a16,a16,a17)),
% 59.14/59.23 inference(scs_inference,[],[143,263,265,271,273,275,215,165,214,199,164,216,152])).
% 59.14/59.23 cnf(311,plain,
% 59.14/59.23 (~P7(a3,a17,x3111,a17,a1,x3112)),
% 59.14/59.23 inference(scs_inference,[],[291,215])).
% 59.14/59.23 cnf(315,plain,
% 59.14/59.23 (~P7(a17,a1,x3151,a3,a17,x3152)),
% 59.14/59.23 inference(scs_inference,[],[291,287,215,214,199])).
% 59.14/59.23 cnf(317,plain,
% 59.14/59.23 (~P5(a1,a17,a3,a17)),
% 59.14/59.23 inference(scs_inference,[],[291,287,293,215,214,199,165])).
% 59.14/59.23 cnf(319,plain,
% 59.14/59.23 (~P5(a3,a17,a17,a1)),
% 59.14/59.23 inference(scs_inference,[],[291,287,293,215,214,199,165,164])).
% 59.14/59.23 cnf(321,plain,
% 59.14/59.23 (~P7(a17,x3211,a3,a1,x3212,a17)),
% 59.14/59.23 inference(scs_inference,[],[291,287,293,215,214,199,165,164,216])).
% 59.14/59.23 cnf(323,plain,
% 59.14/59.23 (P1(a1,a1,a16)),
% 59.14/59.23 inference(scs_inference,[],[277,291,287,293,215,214,199,165,164,216,152])).
% 59.14/59.23 cnf(337,plain,
% 59.14/59.23 (~P7(x3371,a17,a1,x3372,a17,a3)),
% 59.14/59.23 inference(scs_inference,[],[289,215])).
% 59.14/59.23 cnf(339,plain,
% 59.14/59.23 (~P7(a1,x3391,a17,a3,x3392,a17)),
% 59.14/59.23 inference(scs_inference,[],[289,295,215,214])).
% 59.14/59.23 cnf(341,plain,
% 59.14/59.23 (~P5(a3,a17,a1,a17)),
% 59.14/59.23 inference(scs_inference,[],[319,289,295,215,214,165])).
% 59.14/59.23 cnf(343,plain,
% 59.14/59.23 (~P7(a17,x3431,a1,a3,x3432,a17)),
% 59.14/59.23 inference(scs_inference,[],[315,319,289,295,215,214,165,216])).
% 59.14/59.23 cnf(345,plain,
% 59.14/59.23 (P1(a17,a17,a16)),
% 59.14/59.23 inference(scs_inference,[],[297,315,319,289,295,215,214,165,216,152])).
% 59.14/59.23 cnf(359,plain,
% 59.14/59.23 (~P7(x3591,a17,a3,x3592,a1,a17)),
% 59.14/59.23 inference(scs_inference,[],[321,215])).
% 59.14/59.23 cnf(361,plain,
% 59.14/59.23 (~P7(a3,x3611,a17,a17,x3612,a1)),
% 59.14/59.23 inference(scs_inference,[],[311,321,215,216])).
% 59.14/59.23 cnf(374,plain,
% 59.14/59.23 (~P7(x3741,a1,a17,x3742,a3,a17)),
% 59.14/59.23 inference(scs_inference,[],[339,215])).
% 59.14/59.23 cnf(376,plain,
% 59.14/59.23 (~P7(x3761,a17,a3,x3762,a17,a1)),
% 59.14/59.23 inference(scs_inference,[],[337,339,215,214])).
% 59.14/59.23 cnf(378,plain,
% 59.14/59.23 (~P7(x3781,a3,a17,x3782,a17,a1)),
% 59.14/59.23 inference(scs_inference,[],[337,339,359,215,214,216])).
% 59.14/59.23 cnf(380,plain,
% 59.14/59.23 (~P5(x3801,a17,x3802,a17)+~P11(x3801,a17,a1,x3802,a17,a3)),
% 59.14/59.23 inference(scs_inference,[],[337,339,359,215,214,216,217])).
% 59.14/59.23 cnf(382,plain,
% 59.14/59.23 (~P8(x3821,a17,a17)+~P11(x3821,a17,a1,x3821,a17,a3)),
% 59.14/59.23 inference(scs_inference,[],[337,339,359,215,214,216,217,153])).
% 59.14/59.23 cnf(391,plain,
% 59.14/59.23 (~P7(x3911,a17,a1,x3912,a3,a17)),
% 59.14/59.23 inference(scs_inference,[],[343,215])).
% 59.14/59.23 cnf(393,plain,
% 59.14/59.23 (~P7(x3931,a3,a17,x3932,a1,a17)),
% 59.14/59.23 inference(scs_inference,[],[343,376,215,216])).
% 59.14/59.23 cnf(395,plain,
% 59.14/59.23 (~P7(x3951,a1,a17,x3952,a17,a3)),
% 59.14/59.23 inference(scs_inference,[],[343,376,359,215,216,214])).
% 59.14/59.23 cnf(397,plain,
% 59.14/59.23 (~P4(x3971,x3972,x3973,x3974,a1,a3,a3,a16)+P4(x3971,x3972,x3973,x3974,a1,a3,a3,a2)),
% 59.14/59.23 inference(scs_inference,[],[146,343,376,359,215,216,214,259])).
% 59.14/59.23 cnf(401,plain,
% 59.14/59.23 (~P5(a3,x4011,a17,x4012)+~P11(a3,x4011,a17,a17,x4012,a1)),
% 59.14/59.23 inference(scs_inference,[],[361,217])).
% 59.14/59.23 cnf(405,plain,
% 59.14/59.23 (~P5(a3,x4051,x4052,a17)+~P11(a3,x4051,a17,a17,x4052,a1)),
% 59.14/59.23 inference(scs_inference,[],[361,217,199,165])).
% 59.14/59.23 cnf(416,plain,
% 59.14/59.23 (~P8(x4161,a3,a1)+~P3(a17,x4161,a1,a3)),
% 59.14/59.23 inference(scs_inference,[],[263,170,151])).
% 59.14/59.23 cnf(436,plain,
% 59.14/59.23 (~P8(x4361,a3,a1)+~P11(x4361,a1,a17,x4361,a3,a17)),
% 59.14/59.23 inference(scs_inference,[],[374,217,153,151])).
% 59.14/59.23 cnf(457,plain,
% 59.14/59.23 (~P5(a3,a3,a17,a3)+~P11(a3,a3,a17,a3,a17,a1)),
% 59.14/59.23 inference(scs_inference,[],[144,378,217,170,151,153,165])).
% 59.14/59.23 cnf(470,plain,
% 59.14/59.23 (~P8(x4701,a17,a3)+~P11(x4701,a17,a1,x4701,a3,a17)),
% 59.14/59.24 inference(scs_inference,[],[391,217,153])).
% 59.14/59.24 cnf(474,plain,
% 59.14/59.24 (~P5(x4741,a17,a3,x4741)+~P11(x4741,a17,a1,x4741,a3,a17)),
% 59.14/59.24 inference(scs_inference,[],[391,217,153,199,165])).
% 59.14/59.24 cnf(476,plain,
% 59.14/59.24 (~P5(x4761,a3,x4761,a17)+~P11(x4761,a17,a1,x4761,a3,a17)),
% 59.14/59.24 inference(scs_inference,[],[391,217,153,199,165,164])).
% 59.14/59.24 cnf(485,plain,
% 59.14/59.24 (~P8(x4851,a3,a1)+~P11(x4851,a3,a17,x4851,a1,a17)),
% 59.14/59.24 inference(scs_inference,[],[393,217,153])).
% 59.14/59.24 cnf(502,plain,
% 59.14/59.24 (~P8(x5021,a1,a17)+~P11(x5021,a1,a17,x5021,a17,a3)),
% 59.14/59.24 inference(scs_inference,[],[395,217,199,153])).
% 59.14/59.24 cnf(536,plain,
% 59.14/59.24 (~P5(a17,x5361,x5362,a17)+~P11(a17,x5361,a1,a17,x5362,a3)),
% 59.14/59.24 inference(scs_inference,[],[289,217,199,153,165])).
% 59.14/59.24 cnf(545,plain,
% 59.14/59.24 (~P5(a3,x5451,a1,x5452)+~P11(a3,x5451,a17,a1,x5452,a17)),
% 59.14/59.24 inference(scs_inference,[],[295,217])).
% 59.14/59.24 cnf(571,plain,
% 59.14/59.24 (~P5(a17,x5711,a3,x5712)+~P11(a17,x5711,a1,a3,x5712,a17)),
% 59.14/59.24 inference(scs_inference,[],[343,217])).
% 59.14/59.24 cnf(575,plain,
% 59.14/59.24 (~P5(a3,x5751,a17,x5752)+~P11(a17,x5752,a1,a3,x5751,a17)),
% 59.14/59.24 inference(scs_inference,[],[343,217,165,164])).
% 59.14/59.24 cnf(584,plain,
% 59.14/59.24 (~P5(x5841,a17,x5842,a17)+~P11(x5841,a17,a3,x5842,a17,a1)),
% 59.14/59.24 inference(scs_inference,[],[376,217])).
% 59.14/59.24 cnf(586,plain,
% 59.14/59.24 (~P8(x5861,a17,a17)+~P11(x5861,a17,a3,x5861,a17,a1)),
% 59.14/59.24 inference(scs_inference,[],[376,217,153])).
% 59.14/59.24 cnf(597,plain,
% 59.14/59.24 (~P8(x5971,a17,a1)+~P11(x5971,a17,a3,x5971,a1,a17)),
% 59.14/59.24 inference(scs_inference,[],[359,217,153])).
% 59.14/59.24 cnf(615,plain,
% 59.14/59.24 (~P5(x6151,x6152,x6153,x6154)+~P9(a17,a3,a17,a1,x6151,x6152,x6153,x6154)),
% 59.14/59.24 inference(scs_inference,[],[142,147,145,88,239,240])).
% 59.14/59.24 cnf(621,plain,
% 59.14/59.24 (~P5(x6211,x6212,x6213,x6214)+~P9(a17,a1,a17,a3,x6211,x6212,x6213,x6214)),
% 59.14/59.24 inference(scs_inference,[],[263,240])).
% 59.14/59.24 cnf(636,plain,
% 59.14/59.24 (~P5(x6361,x6362,x6363,x6364)+~P9(a1,a17,a3,a17,x6361,x6362,x6363,x6364)),
% 59.14/59.24 inference(scs_inference,[],[317,240])).
% 59.14/59.24 cnf(651,plain,
% 59.14/59.24 (~P5(x6511,x6512,x6513,x6514)+~P9(a1,a17,a17,a3,x6511,x6512,x6513,x6514)),
% 59.14/59.24 inference(scs_inference,[],[293,240])).
% 59.14/59.24 cnf(667,plain,
% 59.14/59.24 (~P5(x6671,x6672,x6673,x6674)+~P9(a3,a17,a17,a1,x6671,x6672,x6673,x6674)),
% 59.14/59.24 inference(scs_inference,[],[143,319,88,240])).
% 59.14/59.24 cnf(679,plain,
% 59.14/59.24 (~P5(x6791,x6792,x6793,x6794)+~P9(a17,a3,a1,a17,x6791,x6792,x6793,x6794)),
% 59.14/59.24 inference(scs_inference,[],[265,345,88,89,240])).
% 59.14/59.24 cnf(688,plain,
% 59.14/59.24 (~P5(x6881,x6882,x6883,x6884)+~P9(a17,a1,a3,a17,x6881,x6882,x6883,x6884)),
% 59.14/59.24 inference(scs_inference,[],[287,240])).
% 59.14/59.24 cnf(703,plain,
% 59.14/59.24 (~P5(x7031,x7032,x7033,x7034)+~P9(a3,a17,a1,a17,x7031,x7032,x7033,x7034)),
% 59.14/59.24 inference(scs_inference,[],[341,240])).
% 59.14/59.24 cnf(718,plain,
% 59.14/59.24 (P1(a2,a16,a1)),
% 59.14/59.24 inference(scs_inference,[],[142,148,149])).
% 59.14/59.24 cnf(719,plain,
% 59.14/59.24 (P1(a1,a1,a2)),
% 59.14/59.24 inference(scs_inference,[],[718,152])).
% 59.14/59.24 cnf(729,plain,
% 59.14/59.24 (P1(a2,a2,a1)),
% 59.14/59.24 inference(scs_inference,[],[719,152])).
% 59.14/59.24 cnf(761,plain,
% 59.14/59.24 (P1(a16,a2,a1)),
% 59.14/59.24 inference(scs_inference,[],[323,719,88,152])).
% 59.14/59.24 cnf(869,plain,
% 59.14/59.24 (P1(x8691,x8692,x8693)+~P10(x8691,x8693,x8691,x8692)),
% 59.14/59.24 inference(scs_inference,[],[157,149])).
% 59.14/59.24 cnf(917,plain,
% 59.14/59.24 (~P8(x9171,a3,a1)+~E(x9171,x9172)+~P3(a17,x9172,a1,a3)),
% 59.14/59.24 inference(scs_inference,[],[416,139])).
% 59.14/59.24 cnf(950,plain,
% 59.14/59.24 (P1(x9501,x9502,x9503)+~P10(x9501,x9503,x9502,x9501)),
% 59.14/59.24 inference(scs_inference,[],[869,161])).
% 59.14/59.24 cnf(998,plain,
% 59.14/59.24 (P1(x9981,x9982,x9983)+~P10(x9982,x9981,x9981,x9983)),
% 59.14/59.24 inference(scs_inference,[],[950,160])).
% 59.14/59.24 cnf(1030,plain,
% 59.14/59.24 (~P4(x10301,x10302,x10303,x10304,x10302,x10305,x10303,x10304)+P1(x10302,x10301,x10305)),
% 59.14/59.24 inference(scs_inference,[],[998,230])).
% 59.14/59.24 cnf(1063,plain,
% 59.14/59.24 (P3(a3,a17,a18,a3)),
% 59.14/59.24 inference(scs_inference,[],[144,162,163])).
% 59.14/59.24 cnf(1064,plain,
% 59.14/59.24 (P10(a3,a18,a18,a3)),
% 59.14/59.24 inference(scs_inference,[],[144,1063,177])).
% 59.14/59.24 cnf(1065,plain,
% 59.14/59.24 (~P3(x10651,x10652,x10653,x10654)+~P3(x10655,x10656,x10651,x10652)+P10(x10655,x10656,x10653,x10654)),
% 59.14/59.24 inference(rename_variables,[],[177])).
% 59.14/59.24 cnf(1066,plain,
% 59.14/59.24 (P1(a3,a18,a18)),
% 59.14/59.24 inference(scs_inference,[],[144,1063,177,950])).
% 59.14/59.24 cnf(1068,plain,
% 59.14/59.24 (P1(a18,a3,a3)),
% 59.14/59.24 inference(scs_inference,[],[144,1063,177,950,998])).
% 59.14/59.24 cnf(1070,plain,
% 59.14/59.24 (~P3(a18,a3,x10701,x10702)+P3(a3,a18,x10701,x10702)),
% 59.14/59.24 inference(scs_inference,[],[144,1063,177,950,998,179])).
% 59.14/59.24 cnf(1072,plain,
% 59.14/59.24 (P10(a3,a18,a3,a17)+~P3(a18,a3,a3,a18)),
% 59.14/59.24 inference(scs_inference,[],[144,1063,177,950,998,179,1065])).
% 59.14/59.24 cnf(1076,plain,
% 59.14/59.24 (P1(a3,a17,a18)+~P3(a18,a3,a3,a18)),
% 59.14/59.24 inference(scs_inference,[],[144,1063,177,950,998,179,1065,152,869])).
% 59.14/59.24 cnf(1079,plain,
% 59.14/59.24 (P1(a18,a18,a3)),
% 59.14/59.24 inference(scs_inference,[],[1066,152])).
% 59.14/59.24 cnf(1091,plain,
% 59.14/59.24 (P1(a3,a3,a18)),
% 59.14/59.24 inference(scs_inference,[],[1079,152])).
% 59.14/59.24 cnf(1175,plain,
% 59.14/59.24 (P6(x11751,x11752,x11753,x11754)+~P6(x11753,x11751,x11752,x11754)),
% 59.14/59.24 inference(scs_inference,[],[166,167])).
% 59.14/59.24 cnf(1207,plain,
% 59.14/59.24 (P4(x12071,x12072,x12073,x12074,a3,a17,x12073,x12074)+~P3(x12071,x12072,a3,a18)),
% 59.14/59.24 inference(scs_inference,[],[281,222])).
% 59.14/59.24 cnf(1223,plain,
% 59.14/59.24 (P4(a3,a18,x12231,x12232,a3,a17,x12231,x12232)+~P3(a18,a3,a3,a18)),
% 59.14/59.24 inference(scs_inference,[],[1070,1207])).
% 59.14/59.24 cnf(1239,plain,
% 59.14/59.24 (~P3(a3,a18,a18,a3)+P10(a3,a18,a3,a17)),
% 59.14/59.24 inference(scs_inference,[],[1072,162])).
% 59.14/59.24 cnf(1255,plain,
% 59.14/59.24 (P6(x12551,x12552,x12553,x12554)+~P6(x12553,x12552,x12551,x12554)),
% 59.14/59.24 inference(scs_inference,[],[1175,167])).
% 59.14/59.24 cnf(1271,plain,
% 59.14/59.24 (P1(a3,a18,a17)+~P3(a3,a18,a18,a3)),
% 59.14/59.24 inference(scs_inference,[],[1239,157])).
% 59.14/59.24 cnf(1287,plain,
% 59.14/59.24 (P1(a18,a3,a17)+~P3(a3,a18,a18,a3)),
% 59.14/59.24 inference(scs_inference,[],[1271,148])).
% 59.14/59.24 cnf(1303,plain,
% 59.14/59.24 (P1(a18,a17,a3)+~P3(a3,a18,a18,a3)),
% 59.14/59.24 inference(scs_inference,[],[1287,149])).
% 59.14/59.24 cnf(1319,plain,
% 59.14/59.24 (P1(a17,a18,a3)+~P3(a3,a18,a18,a3)),
% 59.14/59.24 inference(scs_inference,[],[1303,148])).
% 59.14/59.24 cnf(1335,plain,
% 59.14/59.24 (P1(a17,a3,a18)+~P3(a3,a18,a18,a3)),
% 59.14/59.24 inference(scs_inference,[],[1319,149])).
% 59.14/59.24 cnf(1383,plain,
% 59.14/59.24 (P6(x13831,x13832,x13833,x13834)+~P6(x13832,x13833,x13831,x13834)),
% 59.14/59.24 inference(scs_inference,[],[1255,166])).
% 59.14/59.24 cnf(1399,plain,
% 59.14/59.24 (P6(x13991,x13992,x13993,x13994)+~P6(x13992,x13993,x13994,x13991)),
% 59.14/59.24 inference(scs_inference,[],[1383,168])).
% 59.14/59.24 cnf(1415,plain,
% 59.14/59.24 (~P6(x14151,x14152,x14153,x14154)+P6(x14154,x14152,x14153,x14151)),
% 59.14/59.24 inference(scs_inference,[],[1399,1175])).
% 59.14/59.24 cnf(1447,plain,
% 59.14/59.24 (~P11(a17,x14471,a1,a17,x14471,a3)+~P8(x14471,a17,a17)),
% 59.14/59.24 inference(scs_inference,[],[382,212])).
% 59.14/59.24 cnf(1479,plain,
% 59.14/59.24 (~P11(x14791,a17,a1,x14791,a17,a3)+~P8(x14791,a3,a1)),
% 59.14/59.24 inference(scs_inference,[],[436,213])).
% 59.14/59.24 cnf(1543,plain,
% 59.14/59.24 (~P11(x15431,a3,a17,x15431,a17,a1)+~P8(x15431,a17,a3)),
% 59.14/59.24 inference(scs_inference,[],[470,211])).
% 59.14/59.24 cnf(1559,plain,
% 59.14/59.24 (~P11(a3,x15591,a17,a1,x15591,a17)+~P8(x15591,a3,a1)),
% 59.14/59.24 inference(scs_inference,[],[485,212])).
% 59.14/59.24 cnf(1575,plain,
% 59.14/59.24 (~P11(x15751,a17,a1,x15751,a3,a17)+~P8(x15751,a1,a17)),
% 59.14/59.24 inference(scs_inference,[],[502,213])).
% 59.14/59.24 cnf(1623,plain,
% 59.14/59.24 (~P11(a17,x16231,a3,a17,x16231,a1)+~P8(x16231,a17,a17)),
% 59.14/59.24 inference(scs_inference,[],[586,212])).
% 59.14/59.24 cnf(1639,plain,
% 59.14/59.24 (~P11(x16391,a1,a17,x16391,a17,a3)+~P8(x16391,a17,a1)),
% 59.14/59.24 inference(scs_inference,[],[597,211])).
% 59.14/59.24 cnf(1671,plain,
% 59.14/59.24 (~P8(x16711,x16712,x16713)+~P10(x16712,a17,x16713,a17)+~P11(a17,x16711,a1,a17,x16711,a3)),
% 59.14/59.24 inference(scs_inference,[],[1447,172])).
% 59.14/59.24 cnf(1703,plain,
% 59.14/59.24 (~P8(x17031,a1,a3)+~P11(x17031,a17,a1,x17031,a17,a3)),
% 59.14/59.24 inference(scs_inference,[],[1479,151])).
% 59.14/59.24 cnf(1767,plain,
% 59.14/59.24 (~P8(x17671,a3,a17)+~P11(x17671,a3,a17,x17671,a17,a1)),
% 59.14/59.24 inference(scs_inference,[],[1543,151])).
% 59.14/59.24 cnf(1783,plain,
% 59.14/59.24 (~P8(x17831,a1,a3)+~P11(a3,x17831,a17,a1,x17831,a17)),
% 59.14/59.24 inference(scs_inference,[],[1559,151])).
% 59.14/59.24 cnf(1799,plain,
% 59.14/59.24 (~P8(x17991,a17,a1)+~P11(x17991,a17,a1,x17991,a3,a17)),
% 59.14/59.24 inference(scs_inference,[],[1575,151])).
% 59.14/59.24 cnf(1847,plain,
% 59.14/59.24 (~P8(x18471,x18472,x18473)+~P10(x18472,a17,x18473,a17)+~P11(a17,x18471,a3,a17,x18471,a1)),
% 59.14/59.24 inference(scs_inference,[],[1623,172])).
% 59.14/59.24 cnf(1863,plain,
% 59.14/59.24 (~P8(x18631,a17,a17)+~P8(x18632,a17,a16)+~P11(f19(a17,a1),a1,a17,f19(a17,a1),a17,a3)),
% 59.14/59.24 inference(scs_inference,[],[345,1639,156])).
% 59.14/59.24 cnf(1895,plain,
% 59.14/59.24 (~P11(x18951,a17,a3,x18951,a17,a1)+~P8(x18951,a1,a3)),
% 59.14/59.24 inference(scs_inference,[],[1703,211])).
% 59.14/59.24 cnf(1962,plain,
% 59.14/59.24 (~P11(x19621,a17,a3,x19621,a1,a17)+~P8(x19621,a3,a17)),
% 59.14/59.24 inference(scs_inference,[],[1767,213])).
% 59.14/59.24 cnf(1978,plain,
% 59.14/59.24 (~P11(a3,a17,x19781,a1,a17,x19781)+~P8(x19781,a1,a3)),
% 59.14/59.24 inference(scs_inference,[],[1783,213])).
% 59.14/59.24 cnf(1994,plain,
% 59.14/59.24 (~P11(a17,x19941,a1,a3,x19941,a17)+~P8(x19941,a17,a1)),
% 59.14/59.24 inference(scs_inference,[],[1799,212])).
% 59.14/59.24 cnf(2026,plain,
% 59.14/59.24 (~P8(x20261,a3,a1)+~P11(x20261,a17,a3,x20261,a17,a1)),
% 59.14/59.24 inference(scs_inference,[],[1895,151])).
% 59.14/59.24 cnf(2042,plain,
% 59.14/59.24 (~P8(x20421,a17,a3)+~P11(x20421,a17,a3,x20421,a1,a17)),
% 59.14/59.24 inference(scs_inference,[],[1962,151])).
% 59.14/59.24 cnf(2058,plain,
% 59.14/59.24 (~P8(x20581,a3,a1)+~P11(a3,a17,x20581,a1,a17,x20581)),
% 59.14/59.24 inference(scs_inference,[],[1978,151])).
% 59.14/59.24 cnf(2074,plain,
% 59.14/59.24 (~P8(x20741,a1,a17)+~P11(a17,x20741,a1,a3,x20741,a17)),
% 59.14/59.24 inference(scs_inference,[],[1994,151])).
% 59.14/59.24 cnf(2106,plain,
% 59.14/59.24 (~P11(a17,x21061,a3,a17,x21061,a1)+~P8(x21061,a3,a1)),
% 59.14/59.24 inference(scs_inference,[],[2026,212])).
% 59.14/59.24 cnf(2122,plain,
% 59.14/59.24 (~P11(x21221,a1,a17,x21221,a17,a3)+~P8(x21221,a17,a3)),
% 59.14/59.24 inference(scs_inference,[],[2042,211])).
% 59.14/59.24 cnf(2138,plain,
% 59.14/59.24 (~P11(a1,a17,x21381,a3,a17,x21381)+~P8(x21381,a3,a1)),
% 59.14/59.24 inference(scs_inference,[],[2058,211])).
% 59.14/59.24 cnf(2154,plain,
% 59.14/59.24 (~P11(a17,a1,x21541,a3,a17,x21541)+~P8(x21541,a1,a17)),
% 59.14/59.24 inference(scs_inference,[],[2074,213])).
% 59.14/59.24 cnf(2186,plain,
% 59.14/59.24 (~P8(x21861,a1,a3)+~P11(a17,x21861,a3,a17,x21861,a1)),
% 59.14/59.24 inference(scs_inference,[],[2106,151])).
% 59.14/59.24 cnf(2202,plain,
% 59.14/59.24 (~P8(x22021,a3,a17)+~P11(x22021,a1,a17,x22021,a17,a3)),
% 59.14/59.24 inference(scs_inference,[],[2122,151])).
% 59.14/59.24 cnf(2218,plain,
% 59.14/59.24 (~P8(x22181,a1,a3)+~P11(a1,a17,x22181,a3,a17,x22181)),
% 59.14/59.24 inference(scs_inference,[],[2138,151])).
% 59.14/59.24 cnf(2234,plain,
% 59.14/59.24 (~P8(x22341,a17,a1)+~P11(a17,a1,x22341,a3,a17,x22341)),
% 59.14/59.24 inference(scs_inference,[],[2154,151])).
% 59.14/59.24 cnf(2266,plain,
% 59.14/59.24 (~P11(a17,a3,x22661,a17,a1,x22661)+~P8(x22661,a1,a3)),
% 59.14/59.24 inference(scs_inference,[],[2186,213])).
% 59.14/59.24 cnf(2282,plain,
% 59.14/59.24 (~P11(a1,x22821,a17,a17,x22821,a3)+~P8(x22821,a3,a17)),
% 59.14/59.24 inference(scs_inference,[],[2202,212])).
% 59.14/59.24 cnf(2298,plain,
% 59.14/59.24 (~P11(a17,a1,x22981,a17,a3,x22981)+~P8(x22981,a1,a3)),
% 59.14/59.24 inference(scs_inference,[],[2218,212])).
% 59.14/59.24 cnf(2314,plain,
% 59.14/59.24 (~P11(a3,a17,x23141,a17,a1,x23141)+~P8(x23141,a17,a1)),
% 59.14/59.24 inference(scs_inference,[],[2234,211])).
% 59.14/59.24 cnf(2346,plain,
% 59.14/59.24 (~P8(x23461,a3,a1)+~P11(a17,a3,x23461,a17,a1,x23461)),
% 59.14/59.24 inference(scs_inference,[],[2266,151])).
% 59.14/59.24 cnf(2362,plain,
% 59.14/59.24 (~P8(x23621,a17,a3)+~P11(a1,x23621,a17,a17,x23621,a3)),
% 59.14/59.24 inference(scs_inference,[],[2282,151])).
% 59.14/59.24 cnf(2378,plain,
% 59.14/59.24 (~P8(x23781,a3,a1)+~P11(a17,a1,x23781,a17,a3,x23781)),
% 59.14/59.24 inference(scs_inference,[],[2298,151])).
% 59.14/59.24 cnf(2394,plain,
% 59.14/59.24 (~P8(x23941,a1,a17)+~P11(a3,a17,x23941,a17,a1,x23941)),
% 59.14/59.24 inference(scs_inference,[],[2314,151])).
% 59.14/59.24 cnf(2443,plain,
% 59.14/59.24 (~P11(a1,a17,x24431,a17,a3,x24431)+~P8(x24431,a17,a3)),
% 59.14/59.24 inference(scs_inference,[],[2362,213])).
% 59.14/59.24 cnf(2459,plain,
% 59.14/59.24 (~P11(a17,x24591,a1,a17,x24591,a3)+~P8(x24591,a3,a1)),
% 59.14/59.24 inference(scs_inference,[],[2378,213])).
% 59.14/59.24 cnf(2475,plain,
% 59.14/59.24 (~P11(a17,a3,x24751,a1,a17,x24751)+~P8(x24751,a1,a17)),
% 59.14/59.24 inference(scs_inference,[],[2394,212])).
% 59.14/59.24 cnf(2507,plain,
% 59.14/59.24 (~P8(x25071,a3,a17)+~P11(a1,a17,x25071,a17,a3,x25071)),
% 59.14/59.24 inference(scs_inference,[],[2443,151])).
% 59.14/59.24 cnf(2523,plain,
% 59.14/59.24 (~P8(x25231,a1,a3)+~P11(a17,x25231,a1,a17,x25231,a3)),
% 59.14/59.24 inference(scs_inference,[],[2459,151])).
% 59.14/59.24 cnf(2539,plain,
% 59.14/59.24 (~P8(x25391,a17,a1)+~P11(a17,a3,x25391,a1,a17,x25391)),
% 59.14/59.24 inference(scs_inference,[],[2475,151])).
% 59.14/59.24 cnf(2572,plain,
% 59.14/59.24 (~P11(a17,a3,x25721,a1,a17,x25721)+~P8(x25721,a3,a17)),
% 59.14/59.24 inference(scs_inference,[],[2507,211])).
% 59.14/59.24 cnf(2605,plain,
% 59.14/59.24 (~P11(a1,a17,x26051,a17,a3,x26051)+~P8(x26051,a17,a1)),
% 59.14/59.24 inference(scs_inference,[],[2539,211])).
% 59.14/59.24 cnf(2621,plain,
% 59.14/59.24 (~P8(x26211,a17,a3)+~P11(a17,a3,x26211,a1,a17,x26211)),
% 59.14/59.24 inference(scs_inference,[],[2572,151])).
% 59.14/59.24 cnf(2637,plain,
% 59.14/59.24 (~P8(x26371,a1,a17)+~P11(a1,a17,x26371,a17,a3,x26371)),
% 59.14/59.24 inference(scs_inference,[],[2605,151])).
% 59.14/59.24 cnf(2653,plain,
% 59.14/59.24 (~P11(a3,a17,x26531,a17,a1,x26531)+~P8(x26531,a17,a3)),
% 59.14/59.24 inference(scs_inference,[],[2621,212])).
% 59.14/59.24 cnf(2669,plain,
% 59.14/59.24 (~P11(a1,x26691,a17,a17,x26691,a3)+~P8(x26691,a1,a17)),
% 59.14/59.24 inference(scs_inference,[],[2637,213])).
% 59.14/59.24 cnf(2685,plain,
% 59.14/59.24 (~P8(x26851,a3,a17)+~P11(a3,a17,x26851,a17,a1,x26851)),
% 59.14/59.24 inference(scs_inference,[],[2653,151])).
% 59.14/59.24 cnf(2701,plain,
% 59.14/59.24 (~P8(x27011,a17,a1)+~P11(a1,x27011,a17,a17,x27011,a3)),
% 59.14/59.24 inference(scs_inference,[],[2669,151])).
% 59.14/59.24 cnf(2717,plain,
% 59.14/59.24 (~P11(a17,a1,x27171,a3,a17,x27171)+~P8(x27171,a3,a17)),
% 59.14/59.24 inference(scs_inference,[],[2685,211])).
% 59.14/59.24 cnf(2749,plain,
% 59.14/59.24 (~P8(x27491,a17,a3)+~P11(a17,a1,x27491,a3,a17,x27491)),
% 59.14/59.24 inference(scs_inference,[],[2717,151])).
% 59.14/59.24 cnf(2781,plain,
% 59.14/59.24 (~P11(a17,x27811,a1,a3,x27811,a17)+~P8(x27811,a17,a3)),
% 59.14/59.24 inference(scs_inference,[],[2749,213])).
% 59.14/59.24 cnf(2813,plain,
% 59.14/59.24 (~P8(x28131,a3,a17)+~P11(a17,x28131,a1,a3,x28131,a17)),
% 59.14/59.24 inference(scs_inference,[],[2781,151])).
% 59.14/59.24 cnf(2845,plain,
% 59.14/59.24 (~P11(x28451,a17,a1,x28451,a3,a17)+~P8(x28451,a3,a17)),
% 59.14/59.24 inference(scs_inference,[],[2813,212])).
% 59.14/59.24 cnf(2861,plain,
% 59.14/59.24 (~P3(a17,a3,a17,x28611)+~P8(x28612,a18,x28611)+~P11(f7(a3,a18,a17),a17,a1,f7(a3,a18,a17),a3,a17)),
% 59.14/59.24 inference(scs_inference,[],[144,2845,183])).
% 59.14/59.24 cnf(3163,plain,
% 59.14/59.24 (~P5(x31631,a17,x31632,a17)+~P11(x31632,a17,a1,x31631,a17,a3)),
% 59.14/59.24 inference(scs_inference,[],[380,164])).
% 59.14/59.24 cnf(3228,plain,
% 59.14/59.24 (~P8(a3,x32281,a17)+~P11(a3,x32281,a17,a17,a3,a1)),
% 59.14/59.24 inference(scs_inference,[],[405,153])).
% 59.14/59.24 cnf(3244,plain,
% 59.14/59.24 (~P8(a3,a17,x32441)+~P11(a3,x32441,a17,a17,a3,a1)),
% 59.14/59.24 inference(scs_inference,[],[3228,151])).
% 59.14/59.24 cnf(3422,plain,
% 59.14/59.24 (~P11(a3,a17,a3,a3,a1,a17)+~P5(a3,a3,a17,a3)),
% 59.14/59.24 inference(scs_inference,[],[457,213])).
% 59.14/59.24 cnf(3454,plain,
% 59.14/59.24 (~P5(a3,x34541,x34541,a17)+~P11(x34541,a17,a1,x34541,a3,a17)),
% 59.14/59.24 inference(scs_inference,[],[474,164])).
% 59.14/59.24 cnf(3470,plain,
% 59.14/59.24 (~P5(x34701,a3,a17,x34701)+~P11(x34701,a17,a1,x34701,a3,a17)),
% 59.14/59.24 inference(scs_inference,[],[476,165])).
% 59.14/59.24 cnf(3631,plain,
% 59.14/59.24 (~P5(x36311,a17,a17,x36312)+~P11(a17,x36312,a1,a17,x36311,a3)),
% 59.14/59.24 inference(scs_inference,[],[536,164])).
% 59.14/59.24 cnf(3663,plain,
% 59.14/59.24 (~P8(x36631,a3,x36632)+~P3(a3,a1,a1,x36632)+~P11(a3,x36631,a17,a1,x36631,a17)),
% 59.14/59.24 inference(scs_inference,[],[545,171])).
% 59.14/59.24 cnf(4113,plain,
% 59.14/59.24 (~P5(x41131,x41132,x41133,x41134)+~P9(a17,x41135,a3,x41136,x41131,x41132,x41133,x41134)+~P11(a17,x41135,a1,a3,x41136,a17)),
% 59.14/59.24 inference(scs_inference,[],[571,240])).
% 59.14/59.24 cnf(4406,plain,
% 59.14/59.24 (P1(a1,a16,a2)),
% 59.14/59.24 inference(scs_inference,[],[142,148,149])).
% 59.14/59.24 cnf(4408,plain,
% 59.14/59.24 (P3(a3,a18,a17,a3)),
% 59.14/59.24 inference(scs_inference,[],[144,142,148,149,163])).
% 59.14/59.24 cnf(4410,plain,
% 59.14/59.24 (P4(a3,a18,x44101,x44102,a18,a3,x44101,x44102)),
% 59.14/59.24 inference(scs_inference,[],[144,142,1064,148,149,163,222])).
% 59.14/59.24 cnf(4413,plain,
% 59.14/59.24 (P1(a16,a16,a2)),
% 59.14/59.24 inference(scs_inference,[],[144,142,1064,148,149,163,222,108,152])).
% 59.14/59.24 cnf(4419,plain,
% 59.14/59.24 (~P3(x44191,x44192,a3,a18)+P10(x44191,x44192,a17,a3)),
% 59.14/59.24 inference(scs_inference,[],[144,142,1064,148,149,163,222,108,152,109,114,112,113,177])).
% 59.14/59.24 cnf(4426,plain,
% 59.14/59.24 (P3(a3,a17,a3,a18)),
% 59.14/59.24 inference(scs_inference,[],[1063,163])).
% 59.14/59.24 cnf(4428,plain,
% 59.14/59.24 (P1(a2,a17,a16)),
% 59.14/59.24 inference(scs_inference,[],[143,1063,163,148])).
% 59.14/59.24 cnf(4430,plain,
% 59.14/59.24 (P1(a17,a16,a2)),
% 59.14/59.24 inference(scs_inference,[],[143,1063,163,148,149])).
% 59.14/59.24 cnf(4432,plain,
% 59.14/59.24 (P10(a3,a17,a3,a17)),
% 59.14/59.24 inference(scs_inference,[],[144,143,1063,163,148,149,177])).
% 59.14/59.24 cnf(4434,plain,
% 59.14/59.24 (P1(a2,a2,a16)),
% 59.14/59.24 inference(scs_inference,[],[144,143,1063,4413,163,148,149,177,152])).
% 59.14/59.24 cnf(4438,plain,
% 59.14/59.24 (P1(a3,a17,a17)),
% 59.14/59.24 inference(scs_inference,[],[144,143,1063,4413,163,148,149,177,152,1207,157])).
% 59.14/59.24 cnf(4448,plain,
% 59.14/59.24 (P1(a16,a17,a16)),
% 59.14/59.24 inference(scs_inference,[],[297,149])).
% 59.14/59.24 cnf(4450,plain,
% 59.14/59.24 (P1(a18,a3,a18)),
% 59.14/59.24 inference(scs_inference,[],[297,1066,149,148])).
% 59.14/59.24 cnf(4452,plain,
% 59.14/59.24 (P10(a3,a17,a17,a3)),
% 59.14/59.24 inference(scs_inference,[],[297,1066,4408,4426,149,148,177])).
% 59.14/59.24 cnf(4454,plain,
% 59.14/59.24 (P1(a2,a2,a17)),
% 59.14/59.24 inference(scs_inference,[],[297,1066,4408,4426,4430,149,148,177,152])).
% 59.14/59.24 cnf(4456,plain,
% 59.14/59.24 (P9(a18,a3,a3,a18,a18,a18,a18,a3)),
% 59.14/59.24 inference(scs_inference,[],[1064,297,1079,1066,4408,4426,4430,149,148,177,152,225])).
% 59.14/59.24 cnf(4458,plain,
% 59.14/59.24 (P1(a17,a3,a3)),
% 59.14/59.24 inference(scs_inference,[],[1064,297,1079,1066,4408,4426,4430,149,148,177,152,225,998])).
% 59.14/59.24 cnf(4460,plain,
% 59.14/59.24 (P4(a3,a17,x44601,x44602,a17,a3,x44601,x44602)),
% 59.14/59.24 inference(scs_inference,[],[1064,297,1079,1066,4408,4426,4430,149,148,177,152,225,998,222])).
% 59.14/59.24 cnf(4467,plain,
% 59.14/59.24 (P1(a16,a1,a16)),
% 59.14/59.24 inference(scs_inference,[],[277,149])).
% 59.14/59.24 cnf(4469,plain,
% 59.14/59.24 (P1(a3,a18,a3)),
% 59.14/59.24 inference(scs_inference,[],[277,1068,149,148])).
% 59.14/59.24 cnf(4471,plain,
% 59.14/59.24 (P10(a3,a18,a3,a18)),
% 59.14/59.24 inference(scs_inference,[],[144,277,1068,4426,149,148,177])).
% 59.14/59.24 cnf(4473,plain,
% 59.14/59.24 (P1(a18,a18,a18)),
% 59.14/59.24 inference(scs_inference,[],[144,277,1068,4426,4450,149,148,177,152])).
% 59.14/59.24 cnf(4475,plain,
% 59.14/59.24 (P4(a3,a18,x44751,x44752,a3,a18,x44751,x44752)),
% 59.14/59.24 inference(scs_inference,[],[144,277,1068,4426,4450,149,148,177,152,222])).
% 59.14/59.24 cnf(4483,plain,
% 59.14/59.24 (P1(a17,a16,a17)),
% 59.14/59.24 inference(scs_inference,[],[345,149])).
% 59.14/59.24 cnf(4487,plain,
% 59.14/59.24 (P1(a3,a3,a17)),
% 59.14/59.24 inference(scs_inference,[],[345,4406,4458,149,148,152])).
% 59.14/59.24 cnf(4501,plain,
% 59.14/59.24 (P1(a1,a16,a1)),
% 59.14/59.24 inference(scs_inference,[],[323,149])).
% 59.14/59.24 cnf(4503,plain,
% 59.14/59.24 (P1(a17,a16,a16)),
% 59.14/59.24 inference(scs_inference,[],[323,4448,149,148])).
% 59.14/59.24 cnf(4519,plain,
% 59.14/59.24 (P1(a2,a1,a2)),
% 59.14/59.24 inference(scs_inference,[],[729,149])).
% 59.14/59.24 cnf(4521,plain,
% 59.14/59.24 (P1(a1,a16,a16)),
% 59.14/59.24 inference(scs_inference,[],[729,4467,149,148])).
% 59.14/59.24 cnf(4523,plain,
% 59.14/59.24 (P1(a3,a3,a3)),
% 59.14/59.24 inference(scs_inference,[],[729,4467,4469,149,148,152])).
% 59.14/59.24 cnf(4525,plain,
% 59.14/59.24 (P9(a3,a3,a3,a3,a3,a17,a17,a17)),
% 59.14/59.24 inference(scs_inference,[],[729,4432,4467,4469,4438,149,148,152,225])).
% 59.14/59.24 cnf(4532,plain,
% 59.14/59.24 (P1(a1,a2,a1)),
% 59.14/59.24 inference(scs_inference,[],[719,149])).
% 59.14/59.24 cnf(4534,plain,
% 59.14/59.24 (P1(a16,a17,a17)),
% 59.14/59.24 inference(scs_inference,[],[719,4483,149,148])).
% 59.14/59.24 cnf(4536,plain,
% 59.14/59.24 (P1(a17,a17,a17)),
% 59.14/59.24 inference(scs_inference,[],[719,4483,149,148,152])).
% 59.14/59.24 cnf(4538,plain,
% 59.14/59.24 (P9(a3,a3,a3,a3,a3,a18,a18,a18)),
% 59.14/59.24 inference(scs_inference,[],[719,1066,4471,4483,4523,149,148,152,225])).
% 59.14/59.24 cnf(4540,plain,
% 59.14/59.24 (~P9(x45401,x45402,x45403,x45404,a3,a3,a3,a3)+P9(x45401,x45402,x45403,x45404,a3,a17,a17,a17)),
% 59.14/59.24 inference(scs_inference,[],[719,1066,4471,4483,4523,4525,149,148,152,225,260])).
% 59.14/59.24 cnf(4549,plain,
% 59.14/59.24 (P1(a2,a16,a17)),
% 59.14/59.24 inference(scs_inference,[],[4428,149])).
% 59.14/59.24 cnf(4551,plain,
% 59.14/59.24 (P1(a16,a1,a1)),
% 59.14/59.24 inference(scs_inference,[],[4428,4501,149,148])).
% 59.14/59.24 cnf(4561,plain,
% 59.14/59.24 (~P5(x45611,x45612,a17,a3)+~P5(a17,a1,x45611,x45612)),
% 59.14/59.24 inference(scs_inference,[],[263,341,4432,4428,4501,4538,149,148,152,93,96,97,171,130,180])).
% 59.14/59.24 cnf(4567,plain,
% 59.14/59.24 (P1(a2,a16,a2)),
% 59.14/59.24 inference(scs_inference,[],[4434,149])).
% 59.14/59.24 cnf(4569,plain,
% 59.14/59.24 (P1(a1,a2,a2)),
% 59.14/59.24 inference(scs_inference,[],[4519,4434,149,148])).
% 59.14/59.24 cnf(4585,plain,
% 59.14/59.24 (P1(a2,a17,a2)),
% 59.14/59.24 inference(scs_inference,[],[4454,149])).
% 59.14/59.24 cnf(4589,plain,
% 59.14/59.24 (P1(a17,a17,a2)),
% 59.14/59.24 inference(scs_inference,[],[4532,4454,149,148,152])).
% 59.14/59.24 cnf(4601,plain,
% 59.14/59.24 (P1(a3,a17,a3)),
% 59.14/59.24 inference(scs_inference,[],[4487,149])).
% 59.14/59.24 cnf(4603,plain,
% 59.14/59.24 (P1(a16,a2,a17)),
% 59.14/59.24 inference(scs_inference,[],[4487,4549,149,148])).
% 59.14/59.24 cnf(4605,plain,
% 59.14/59.24 (P1(a17,a17,a3)),
% 59.14/59.24 inference(scs_inference,[],[4487,4549,149,148,152])).
% 59.14/59.24 cnf(4607,plain,
% 59.14/59.24 (P9(a3,a3,a3,a17,a3,a17,a17,a3)),
% 59.14/59.24 inference(scs_inference,[],[4452,4487,4549,149,148,152,225])).
% 59.14/59.24 cnf(4609,plain,
% 59.14/59.24 (~P3(a17,a3,x46091,x46092)+P3(a3,a17,x46091,x46092)),
% 59.14/59.24 inference(scs_inference,[],[4452,4487,4549,149,148,152,225,179])).
% 59.14/59.24 cnf(4611,plain,
% 59.14/59.24 (~P3(a17,a3,x46111,x46112)+P10(a3,a18,x46111,x46112)),
% 59.14/59.24 inference(scs_inference,[],[144,4452,4487,4549,149,148,152,225,179,177])).
% 59.14/59.24 cnf(4622,plain,
% 59.14/59.24 (P1(a17,a2,a17)),
% 59.14/59.24 inference(scs_inference,[],[4589,149])).
% 59.14/59.24 cnf(4639,plain,
% 59.14/59.24 (P1(a17,a3,a17)),
% 59.14/59.24 inference(scs_inference,[],[4605,149])).
% 59.14/59.24 cnf(4643,plain,
% 59.14/59.24 (P9(a17,a3,a3,a17,a17,a17,a17,a3)),
% 59.14/59.24 inference(scs_inference,[],[4452,4605,4585,149,148,225])).
% 59.14/59.24 cnf(4659,plain,
% 59.14/59.24 (P1(a2,a17,a17)),
% 59.14/59.24 inference(scs_inference,[],[4603,4622,149,148])).
% 59.14/59.24 cnf(4720,plain,
% 59.14/59.24 (~P9(x47201,x47202,x47203,x47204,a17,a3,a3,a17)+P9(x47201,x47202,x47203,x47204,a17,a17,a17,a3)),
% 59.14/59.24 inference(scs_inference,[],[4643,260])).
% 59.14/59.24 cnf(4786,plain,
% 59.14/59.24 (~P5(x47861,x47862,a17,a3)+~P5(a1,a17,x47861,x47862)),
% 59.14/59.24 inference(scs_inference,[],[293,180])).
% 59.14/59.24 cnf(4885,plain,
% 59.14/59.24 (P9(a3,a3,a3,a18,a3,a18,a18,a3)),
% 59.14/59.24 inference(scs_inference,[],[1064,1091,4469,225])).
% 59.14/59.24 cnf(4894,plain,
% 59.14/59.24 (P9(a17,a3,a3,a3,a17,a17,a17,a17)),
% 59.14/59.24 inference(scs_inference,[],[4432,4458,4536,225])).
% 59.14/59.24 cnf(4908,plain,
% 59.14/59.24 (P9(a18,a3,a3,a3,a18,a18,a18,a18)),
% 59.14/59.24 inference(scs_inference,[],[1068,4471,4473,225])).
% 59.14/59.24 cnf(5095,plain,
% 59.14/59.24 (~P9(x50951,x50952,x50953,x50954,a18,a3,a3,a3)+P9(x50951,x50952,x50953,x50954,a18,a18,a18,a18)),
% 59.14/59.24 inference(scs_inference,[],[4467,4456,4894,4885,4908,94,96,89,98,260])).
% 59.14/59.24 cnf(5358,plain,
% 59.14/59.24 (P1(a1,x53581,a16)+~E(a17,x53581)),
% 59.14/59.24 inference(scs_inference,[],[761,4603,90,149,148,152])).
% 59.14/59.24 cnf(5365,plain,
% 59.14/59.24 (P1(a1,a17,a16)),
% 59.14/59.24 inference(equality_inference,[],[5358])).
% 59.14/59.24 cnf(5366,plain,
% 59.14/59.24 (P1(a1,a16,a17)),
% 59.14/59.24 inference(scs_inference,[],[5365,149])).
% 59.14/59.24 cnf(5368,plain,
% 59.14/59.24 (P1(a17,a1,a16)),
% 59.14/59.24 inference(scs_inference,[],[5365,149,148])).
% 59.14/59.24 cnf(5370,plain,
% 59.14/59.24 (P1(a17,a17,a1)),
% 59.14/59.24 inference(scs_inference,[],[5365,149,148,152])).
% 59.14/59.24 cnf(5384,plain,
% 59.14/59.24 (P1(a1,a1,a17)),
% 59.14/59.24 inference(scs_inference,[],[5368,5366,5370,149,148,152])).
% 59.14/59.24 cnf(5412,plain,
% 59.14/59.24 (~P8(x54121,a3,a3)+P8(x54121,a18,a18)),
% 59.14/59.24 inference(scs_inference,[],[146,4471,4532,4448,5384,149,148,88,89,90,258,172])).
% 59.14/59.24 cnf(5425,plain,
% 59.14/59.24 (~P8(x54251,a3,a3)+P8(x54251,a17,a17)),
% 59.14/59.24 inference(scs_inference,[],[4432,261,4567,4585,4622,5370,149,148,88,89,90,159,172])).
% 59.14/59.24 cnf(5513,plain,
% 59.14/59.24 (~P8(x55131,a3,x55132)+~P10(x55131,a17,x55132,a1)+~E(a3,a1)),
% 59.14/59.24 inference(scs_inference,[],[146,261,4503,4458,90,159])).
% 59.14/59.24 cnf(5906,plain,
% 59.14/59.24 (~P10(a16,a16,a16,a16)+P9(a1,a16,a16,a16,a1,a16,a16,a16)),
% 59.14/59.24 inference(scs_inference,[],[4521,225])).
% 59.14/59.24 cnf(5911,plain,
% 59.14/59.24 (~P10(a2,a2,a2,a2)+P9(a1,a2,a2,a2,a1,a2,a2,a2)),
% 59.14/59.24 inference(scs_inference,[],[4569,225])).
% 59.14/59.24 cnf(5916,plain,
% 59.14/59.24 (~P10(a16,a16,a16,a16)+P9(a17,a16,a16,a16,a17,a16,a16,a16)),
% 59.14/59.24 inference(scs_inference,[],[4503,225])).
% 59.14/59.24 cnf(5922,plain,
% 59.14/59.24 (~P10(a1,a1,a1,a1)+P9(a16,a1,a1,a1,a16,a1,a1,a1)),
% 59.14/59.24 inference(scs_inference,[],[4551,225])).
% 59.14/59.24 cnf(5927,plain,
% 59.14/59.24 (P9(a16,a3,a3,a3,a16,a17,a17,a17)+~P1(a16,a3,a3)),
% 59.14/59.24 inference(scs_inference,[],[4534,4432,225])).
% 59.14/59.24 cnf(5990,plain,
% 59.14/59.24 (P9(a2,a3,a3,a3,a2,a17,a17,a17)+~P1(a2,a3,a3)),
% 59.14/59.24 inference(scs_inference,[],[4659,4432,225])).
% 59.14/59.24 cnf(6445,plain,
% 59.14/59.24 (P10(a17,a3,a3,a17)),
% 59.14/59.24 inference(scs_inference,[],[4426,4419,160])).
% 59.14/59.24 cnf(6446,plain,
% 59.14/59.24 (P4(a17,a3,x64461,x64462,a3,a17,x64461,x64462)),
% 59.14/59.24 inference(scs_inference,[],[6445,222])).
% 59.14/59.24 cnf(6448,plain,
% 59.14/59.24 (P3(a17,a3,a18,a3)),
% 59.14/59.24 inference(scs_inference,[],[1063,6445,222,179])).
% 59.14/59.24 cnf(6450,plain,
% 59.14/59.24 (P9(a17,a17,a17,a3,a17,a3,a3,a17)),
% 59.14/59.24 inference(scs_inference,[],[4639,4605,1063,6445,222,179,225])).
% 59.14/59.24 cnf(6452,plain,
% 59.14/59.24 (P3(a17,a3,a3,a18)),
% 59.14/59.24 inference(scs_inference,[],[4639,4605,1063,6445,222,179,225,163])).
% 59.14/59.24 cnf(6455,plain,
% 59.14/59.24 (P9(a17,a17,a17,a3,a17,a17,a17,a3)),
% 59.14/59.24 inference(scs_inference,[],[4643,4639,4605,1063,6445,222,179,225,163,108,260])).
% 59.14/59.24 cnf(6468,plain,
% 59.14/59.24 (P9(a17,a3,a3,a17,a17,a3,a3,a17)),
% 59.14/59.24 inference(scs_inference,[],[4643,6450,260])).
% 59.14/59.24 cnf(6470,plain,
% 59.14/59.24 (P9(a3,a17,a17,a3,a3,a3,a3,a17)),
% 59.14/59.24 inference(scs_inference,[],[4643,4487,4601,6450,6445,260,225])).
% 59.14/59.24 cnf(6479,plain,
% 59.14/59.24 (P9(a3,a17,a17,a3,a3,a17,a17,a3)),
% 59.14/59.24 inference(scs_inference,[],[4607,6470,260])).
% 59.14/59.24 cnf(6493,plain,
% 59.14/59.24 (P9(a3,a3,a3,a17,a3,a3,a3,a17)),
% 59.14/59.24 inference(scs_inference,[],[4607,6470,260])).
% 59.14/59.24 cnf(6509,plain,
% 59.14/59.24 (P3(a18,a3,a17,a3)),
% 59.14/59.24 inference(scs_inference,[],[6448,6445,161,162])).
% 59.14/59.24 cnf(6511,plain,
% 59.14/59.24 (P3(f8(a3,a2,a16,a18),a3,a3,a18)),
% 59.14/59.24 inference(scs_inference,[],[6448,6445,145,161,162,184])).
% 59.14/59.24 cnf(6513,plain,
% 59.14/59.24 (P4(a18,a3,x65131,x65132,a3,a18,x65131,x65132)),
% 59.14/59.24 inference(scs_inference,[],[6448,4410,6445,145,161,162,184,249])).
% 59.14/59.24 cnf(6515,plain,
% 59.14/59.24 (P4(x65151,x65152,a3,a18,x65151,x65152,a18,a3)),
% 59.14/59.24 inference(scs_inference,[],[6448,4410,6445,145,161,162,184,249,250])).
% 59.14/59.24 cnf(6517,plain,
% 59.14/59.24 (P4(a18,a3,x65171,x65172,a18,a3,x65171,x65172)),
% 59.14/59.24 inference(scs_inference,[],[6448,4410,6445,145,161,162,184,249,250,251])).
% 59.14/59.24 cnf(6519,plain,
% 59.14/59.24 (P4(a3,a18,a18,a3,x65191,x65192,x65191,x65192)),
% 59.14/59.24 inference(scs_inference,[],[6448,4410,6445,145,161,162,184,249,250,251,252])).
% 59.14/59.24 cnf(6525,plain,
% 59.14/59.24 (P9(a3,a17,a3,a17,a17,a3,a3,a17)),
% 59.14/59.24 inference(scs_inference,[],[6468,6493,6448,4410,6445,4908,145,161,162,184,249,250,251,252,253,254,255])).
% 59.14/59.24 cnf(6527,plain,
% 59.14/59.24 (P9(a17,a3,a17,a3,a3,a17,a3,a17)),
% 59.14/59.24 inference(scs_inference,[],[6468,6493,6448,4410,6445,4908,145,161,162,184,249,250,251,252,253,254,255,256])).
% 59.14/59.24 cnf(6529,plain,
% 59.14/59.24 (P9(a3,a17,a3,a17,a17,a17,a17,a3)),
% 59.14/59.24 inference(scs_inference,[],[6468,6493,6448,4410,6445,4908,145,161,162,184,249,250,251,252,253,254,255,256,4720])).
% 59.14/59.24 cnf(6533,plain,
% 59.14/59.24 (P10(a18,a3,a3,a18)),
% 59.14/59.24 inference(scs_inference,[],[6468,6493,6448,4410,6445,4908,145,161,162,184,249,250,251,252,253,254,255,256,4720,5095,230])).
% 59.14/59.24 cnf(6544,plain,
% 59.14/59.24 (P3(f13(a17,a18,a3,a18,a18),a17,a18,a18)),
% 59.14/59.24 inference(scs_inference,[],[6468,6493,6448,6452,4410,4473,4523,6445,4475,4908,145,161,162,184,249,250,251,252,253,254,255,256,4720,5095,230,174,175,233,194,195])).
% 59.14/59.24 cnf(6546,plain,
% 59.14/59.24 (P3(a18,f6(a17,a18,a3),a3,a17)),
% 59.14/59.24 inference(scs_inference,[],[6468,6493,6448,6452,4410,4473,4523,6445,4475,4908,145,161,162,184,249,250,251,252,253,254,255,256,4720,5095,230,174,175,233,194,195,187])).
% 59.14/59.24 cnf(6548,plain,
% 59.14/59.24 (P3(a18,f5(a18,a17,a3),a3,a17)),
% 59.14/59.24 inference(scs_inference,[],[6468,6493,6448,6452,4410,4473,4523,6445,4475,4908,145,161,162,184,249,250,251,252,253,254,255,256,4720,5095,230,174,175,233,194,195,187,186])).
% 59.14/59.24 cnf(6550,plain,
% 59.14/59.24 (P1(a17,a17,f5(a18,a17,a3))),
% 59.14/59.24 inference(scs_inference,[],[6468,6493,6448,6452,4410,4473,4523,6445,4475,4908,145,161,162,184,249,250,251,252,253,254,255,256,4720,5095,230,174,175,233,194,195,187,186,152])).
% 59.14/59.24 cnf(6552,plain,
% 59.14/59.24 (P4(a17,a3,x65521,x65522,a17,a3,x65521,x65522)),
% 59.14/59.24 inference(scs_inference,[],[6468,6493,6448,6452,4410,6446,4473,4523,6445,4460,4475,4908,145,161,162,184,249,250,251,252,253,254,255,256,4720,5095,230,174,175,233,194,195,187,186,152,259])).
% 59.14/59.24 cnf(6555,plain,
% 59.14/59.24 (P9(a18,a3,a3,a3,a18,a3,a3,a3)),
% 59.14/59.24 inference(scs_inference,[],[6468,6493,6448,6452,4410,6446,4473,4523,6445,4460,4475,4908,145,161,162,184,249,250,251,252,253,254,255,256,4720,5095,230,174,175,233,194,195,187,186,152,259,260])).
% 59.14/59.24 cnf(6559,plain,
% 59.14/59.24 (P9(a3,a17,a17,a17,a3,a3,a3,a3)),
% 59.14/59.24 inference(scs_inference,[],[6468,6493,6448,4438,6452,4410,6446,4473,4523,6445,4460,4475,4908,145,161,162,184,249,250,251,252,253,254,255,256,4720,5095,230,174,175,233,194,195,187,186,152,259,260,177,225])).
% 59.14/59.24 cnf(6565,plain,
% 59.14/59.24 (P6(a3,a18,a3,a3)),
% 59.14/59.24 inference(scs_inference,[],[6468,6493,6448,4438,6452,4410,6446,4473,4605,4523,4601,4487,4639,6445,4460,4475,4908,145,161,162,184,249,250,251,252,253,254,255,256,4720,5095,230,174,175,233,194,195,187,186,152,259,260,177,225,203,204,166])).
% 59.14/59.24 cnf(6567,plain,
% 59.14/59.24 (P6(a3,a3,a18,a3)),
% 59.14/59.24 inference(scs_inference,[],[6468,6493,6448,4438,6452,4410,6446,4473,4605,4523,4601,4487,4639,6445,4460,4475,4908,145,161,162,184,249,250,251,252,253,254,255,256,4720,5095,230,174,175,233,194,195,187,186,152,259,260,177,225,203,204,166,1175])).
% 59.14/59.24 cnf(6569,plain,
% 59.14/59.24 (P6(a3,a3,a3,a18)),
% 59.14/59.24 inference(scs_inference,[],[6468,6493,6448,4438,6452,4410,6446,4473,4605,4523,4601,4487,4639,6445,4460,4475,4908,145,161,162,184,249,250,251,252,253,254,255,256,4720,5095,230,174,175,233,194,195,187,186,152,259,260,177,225,203,204,166,1175,1415])).
% 59.14/59.24 cnf(6573,plain,
% 59.14/59.24 (P10(f8(a3,a2,a16,a18),a3,a17,a3)),
% 59.14/59.24 inference(scs_inference,[],[6468,6493,6448,4438,6452,4410,6446,4473,4605,4523,4601,4487,4639,6445,4460,4475,4908,145,161,162,184,249,250,251,252,253,254,255,256,4720,5095,230,174,175,233,194,195,187,186,152,259,260,177,225,203,204,166,1175,1415,281,4419])).
% 59.14/59.24 cnf(6577,plain,
% 59.14/59.24 (P10(a3,a17,f8(a3,a2,a16,a18),a3)),
% 59.14/59.24 inference(scs_inference,[],[6468,6493,6448,4438,6452,4410,6446,4473,4605,4523,4601,4487,4639,6445,4460,4475,4908,145,161,162,184,249,250,251,252,253,254,255,256,4720,5095,230,174,175,233,194,195,187,186,152,259,260,177,225,203,204,166,1175,1415,281,4419,4540,160])).
% 59.14/59.24 cnf(6600,plain,
% 59.14/59.24 (P4(x66001,x66002,a18,a3,x66001,x66002,a3,a18)),
% 59.14/59.24 inference(scs_inference,[],[6515,249])).
% 59.14/59.24 cnf(6602,plain,
% 59.14/59.24 (P10(a3,a17,a3,f8(a3,a2,a16,a18))),
% 59.14/59.24 inference(scs_inference,[],[6515,6577,249,161])).
% 59.14/59.24 cnf(6604,plain,
% 59.14/59.24 (P4(x66041,x66042,a3,a18,x66042,x66041,a18,a3)),
% 59.14/59.24 inference(scs_inference,[],[6515,6577,249,161,251])).
% 59.14/59.24 cnf(6608,plain,
% 59.14/59.24 (P9(a3,a18,a3,a3,a18,a18,a18,a18)),
% 59.14/59.24 inference(scs_inference,[],[6555,6515,6577,249,161,251,255,5095])).
% 59.14/59.24 cnf(6610,plain,
% 59.14/59.24 (P9(a17,a3,a3,a17,a3,a17,a3,a17)),
% 59.14/59.24 inference(scs_inference,[],[6555,6515,6525,6577,249,161,251,255,5095,253])).
% 59.14/59.24 cnf(6612,plain,
% 59.14/59.24 (P9(a18,a3,a18,a3,a3,a3,a3,a3)),
% 59.14/59.24 inference(scs_inference,[],[6555,6515,6525,6577,249,161,251,255,5095,253,256])).
% 59.14/59.24 cnf(6614,plain,
% 59.14/59.24 (P4(x66141,x66142,a18,a3,x66141,x66142,a18,a3)),
% 59.14/59.24 inference(scs_inference,[],[6555,6515,6517,6525,6577,249,161,251,255,5095,253,256,250])).
% 59.14/59.24 cnf(6616,plain,
% 59.14/59.24 (P4(a18,a3,a3,a18,x66161,x66162,x66161,x66162)),
% 59.14/59.24 inference(scs_inference,[],[6555,6513,6515,6517,6525,6577,249,161,251,255,5095,253,256,250,252])).
% 59.14/59.24 cnf(6622,plain,
% 59.14/59.24 (P9(a18,a3,a18,a3,a3,a17,a17,a17)),
% 59.14/59.24 inference(scs_inference,[],[6555,6513,6515,6517,6525,6577,6544,249,161,251,255,5095,253,256,250,252,254,162,4540])).
% 59.14/59.24 cnf(6624,plain,
% 59.14/59.24 (P10(x66241,x66242,x66241,x66242)),
% 59.14/59.24 inference(scs_inference,[],[6555,6513,6515,6517,6525,6577,6544,249,161,251,255,5095,253,256,250,252,254,162,4540,230])).
% 59.14/59.24 cnf(6626,plain,
% 59.14/59.24 (P10(a17,a3,f8(a3,a2,a16,a18),a3)),
% 59.14/59.24 inference(scs_inference,[],[6555,6513,6515,6517,6525,6577,6573,6544,249,161,251,255,5095,253,256,250,252,254,162,4540,230,160])).
% 59.14/59.24 cnf(6628,plain,
% 59.14/59.24 (P3(f8(a3,a2,a16,a18),a3,a18,a3)),
% 59.14/59.24 inference(scs_inference,[],[6555,6513,6515,6517,6525,6577,6573,6544,6511,249,161,251,255,5095,253,256,250,252,254,162,4540,230,160,238])).
% 59.14/59.24 cnf(6637,plain,
% 59.14/59.24 (P3(a17,f6(a18,a17,a3),a3,a18)),
% 59.14/59.24 inference(scs_inference,[],[6555,6509,6513,6515,6517,6552,6525,6550,6577,6573,6544,6511,6448,249,161,251,255,5095,253,256,250,252,254,162,4540,230,160,238,174,175,233,187])).
% 59.14/59.24 cnf(6642,plain,
% 59.14/59.24 (P3(a17,f5(a17,a18,a3),a3,a18)),
% 59.14/59.24 inference(scs_inference,[],[6555,6509,6513,6515,6517,6552,6525,6550,6577,6573,6544,6511,6446,6448,249,161,251,255,5095,253,256,250,252,254,162,4540,230,160,238,174,175,233,187,237,186])).
% 59.14/59.24 cnf(6644,plain,
% 59.14/59.24 (P3(a18,a3,a3,a17)),
% 59.14/59.24 inference(scs_inference,[],[6555,6533,6509,6513,6515,6517,6552,6525,6550,6577,6573,6544,6511,6446,6448,144,249,161,251,255,5095,253,256,250,252,254,162,4540,230,160,238,174,175,233,187,237,186,179])).
% 59.14/59.24 cnf(6652,plain,
% 59.14/59.24 (P10(a17,f6(a18,a17,a3),a17,a3)),
% 59.14/59.24 inference(scs_inference,[],[6555,6533,6509,6513,6515,6517,6552,6525,6550,6577,6573,6544,6511,4438,6446,6448,144,249,161,251,255,5095,253,256,250,252,254,162,4540,230,160,238,174,175,233,187,237,186,179,204,203,1415,4419])).
% 59.14/59.24 cnf(6654,plain,
% 59.14/59.24 (P6(f5(a18,a17,a3),a17,a3,a17)),
% 59.14/59.24 inference(scs_inference,[],[6555,6533,6509,6513,6515,6517,6552,6525,6550,6577,6573,6544,6511,4438,6446,6448,144,249,161,251,255,5095,253,256,250,252,254,162,4540,230,160,238,174,175,233,187,237,186,179,204,203,1415,4419,1175])).
% 59.14/59.24 cnf(6658,plain,
% 59.14/59.24 (P10(a17,f6(a18,a17,a3),a3,a17)),
% 59.14/59.24 inference(scs_inference,[],[6555,6533,6509,6513,6515,6517,6552,6525,6550,6577,6573,6544,6511,4438,6446,6448,144,249,161,251,255,5095,253,256,250,252,254,162,4540,230,160,238,174,175,233,187,237,186,179,204,203,1415,4419,1175,166,281])).
% 59.14/59.24 cnf(6672,plain,
% 59.14/59.24 (P9(a1,a16,a16,a16,a1,a16,a16,a16)),
% 59.14/59.24 inference(scs_inference,[],[6624,5906])).
% 59.14/59.24 cnf(6673,plain,
% 59.14/59.24 (P9(a1,a2,a2,a2,a1,a2,a2,a2)),
% 59.14/59.24 inference(scs_inference,[],[6624,5911])).
% 59.14/59.24 cnf(6674,plain,
% 59.14/59.24 (P9(a17,a16,a16,a16,a17,a16,a16,a16)),
% 59.14/59.24 inference(scs_inference,[],[6624,5916])).
% 59.14/59.24 cnf(6675,plain,
% 59.14/59.24 (P9(a16,a1,a1,a1,a16,a1,a1,a1)),
% 59.14/59.24 inference(scs_inference,[],[6624,5922])).
% 59.14/59.24 cnf(6686,plain,
% 59.14/59.24 (P1(x66861,x66861,x66861)),
% 59.14/59.24 inference(scs_inference,[],[6614,1030])).
% 59.14/59.24 cnf(6687,plain,
% 59.14/59.24 (P4(x66871,x66872,a18,a3,x66871,x66872,a18,a3)),
% 59.14/59.24 inference(rename_variables,[],[6614])).
% 59.14/59.24 cnf(6689,plain,
% 59.14/59.24 (P4(x66891,x66892,a18,a3,x66892,x66891,a3,a18)),
% 59.14/59.24 inference(scs_inference,[],[6604,6614,1030,249])).
% 59.14/59.24 cnf(6697,plain,
% 59.14/59.24 (P4(x66971,x66972,a18,a3,x66972,x66971,a18,a3)),
% 59.14/59.24 inference(scs_inference,[],[6479,6529,6604,6614,6687,6654,1030,249,255,253,168,251])).
% 59.14/59.24 cnf(6699,plain,
% 59.14/59.24 (P4(a3,a18,x66991,x66992,a18,a3,x66992,x66991)),
% 59.14/59.24 inference(scs_inference,[],[6479,6529,6604,6614,6687,6654,1030,249,255,253,168,251,250])).
% 59.14/59.24 cnf(6701,plain,
% 59.14/59.24 (P6(a17,a17,a3,f5(a18,a17,a3))),
% 59.14/59.24 inference(scs_inference,[],[6479,6529,6604,6614,6687,6654,1030,249,255,253,168,251,250,1415])).
% 59.14/59.24 cnf(6705,plain,
% 59.14/59.24 (P10(x67051,x67052,x67052,x67051)),
% 59.14/59.24 inference(scs_inference,[],[6624,6479,6529,6604,6614,6687,6654,6642,1030,249,255,253,168,251,250,1415,4419,161])).
% 59.14/59.24 cnf(6715,plain,
% 59.14/59.24 (P4(x67151,x67152,x67151,x67152,a18,a3,a3,a18)),
% 59.14/59.24 inference(scs_inference,[],[6624,6479,6455,6529,6600,6604,6614,6687,6548,6654,6642,1030,249,255,253,168,251,250,1415,4419,161,254,256,162,1175,252])).
% 59.14/59.24 cnf(6719,plain,
% 59.14/59.24 (P10(a3,f8(a3,a2,a16,a18),a3,a17)),
% 59.14/59.24 inference(scs_inference,[],[6624,6479,6455,6529,6600,6604,6614,6687,6548,6602,6654,6642,1030,249,255,253,168,251,250,1415,4419,161,254,256,162,1175,252,281,160])).
% 59.14/59.24 cnf(6728,plain,
% 59.14/59.24 (P6(x67281,a3,a18,a18)),
% 59.14/59.24 inference(scs_inference,[],[6624,6479,6455,6529,6600,6604,6614,6687,6548,6602,6654,6637,6642,1079,4426,1030,249,255,253,168,251,250,1415,4419,161,254,256,162,1175,252,281,160,238,174,175,233])).
% 59.14/59.24 cnf(6731,plain,
% 59.14/59.24 (P3(a3,f6(a3,a3,a18),a18,a3)),
% 59.14/59.24 inference(scs_inference,[],[6624,6479,6455,6529,6600,6604,6614,6687,6548,6602,6654,6637,6642,1079,4426,1030,249,255,253,168,251,250,1415,4419,161,254,256,162,1175,252,281,160,238,174,175,233,187])).
% 59.14/59.24 cnf(6735,plain,
% 59.14/59.24 (P5(a3,a3,a18,a18)),
% 59.14/59.24 inference(scs_inference,[],[6624,6479,6455,6529,6600,6604,6614,6687,6548,6602,6654,6637,6642,6567,1079,4426,1030,249,255,253,168,251,250,1415,4419,161,254,256,162,1175,252,281,160,238,174,175,233,187,186,248])).
% 59.14/59.24 cnf(6757,plain,
% 59.14/59.24 (P5(a18,a18,a3,a3)),
% 59.14/59.24 inference(scs_inference,[],[142,6624,6479,6455,6529,6600,6604,6614,6687,6548,6602,6654,6637,6642,6567,4406,1079,4426,1030,249,255,253,168,251,250,1415,4419,161,254,256,162,1175,252,281,160,238,174,175,233,187,186,248,203,621,636,651,667,679,688,703,615,166,164])).
% 59.14/59.24 cnf(6852,plain,
% 59.14/59.24 (P1(x68521,x68522,x68522)),
% 59.14/59.24 inference(scs_inference,[],[6697,1030])).
% 59.14/59.24 cnf(6882,plain,
% 59.14/59.24 (P6(a18,a3,a18,x68821)),
% 59.14/59.24 inference(scs_inference,[],[6672,6608,6697,6699,6728,6757,6719,6701,1030,688,621,651,253,636,679,667,703,615,251,255,249,168,161,1415])).
% 59.14/59.24 cnf(6884,plain,
% 59.14/59.24 (P6(a3,a18,x68841,a18)),
% 59.14/59.24 inference(scs_inference,[],[6672,6608,6697,6699,6728,6757,6719,6701,1030,688,621,651,253,636,679,667,703,615,251,255,249,168,161,1415,1175])).
% 59.14/59.24 cnf(6894,plain,
% 59.14/59.24 (P4(x68941,x68942,x68942,x68941,a18,a3,a3,a18)),
% 59.14/59.24 inference(scs_inference,[],[6672,6608,6689,6697,6699,6715,6728,6757,6546,6719,6701,1030,688,621,651,253,636,679,667,703,615,251,255,249,168,161,1415,1175,254,256,250,162,252])).
% 59.14/59.24 cnf(6896,plain,
% 59.14/59.24 (P6(a3,x68961,a18,a18)),
% 59.14/59.24 inference(scs_inference,[],[6672,6608,6689,6697,6699,6715,6728,6757,6546,6719,6701,1030,688,621,651,253,636,679,667,703,615,251,255,249,168,161,1415,1175,254,256,250,162,252,166])).
% 59.14/59.24 cnf(6898,plain,
% 59.14/59.24 (P10(a3,a17,a17,f6(a18,a17,a3))),
% 59.14/59.24 inference(scs_inference,[],[6672,6608,6689,6697,6699,6715,6728,6757,6658,6546,6719,6701,1030,688,621,651,253,636,679,667,703,615,251,255,249,168,161,1415,1175,254,256,250,162,252,166,160])).
% 59.14/59.24 cnf(6901,plain,
% 59.14/59.24 (P1(x69011,x69011,x69011)),
% 59.14/59.24 inference(rename_variables,[],[6686])).
% 59.14/59.24 cnf(6904,plain,
% 59.14/59.24 (P10(x69041,x69042,x69042,x69041)),
% 59.14/59.24 inference(rename_variables,[],[6705])).
% 59.14/59.24 cnf(6911,plain,
% 59.14/59.24 (P5(a18,a18,a18,a18)),
% 59.14/59.24 inference(scs_inference,[],[6672,6686,6705,6608,6689,6697,6699,6715,6728,6735,6757,6658,6546,6719,6628,6701,6644,144,1030,688,621,651,253,636,679,667,703,615,251,255,249,168,161,1415,1175,254,256,250,162,252,166,160,195,176,174,238,180])).
% 59.14/59.24 cnf(6913,plain,
% 59.14/59.24 (P8(a18,a18,a18)),
% 59.14/59.24 inference(scs_inference,[],[6672,6686,6901,6705,6608,6689,6697,6699,6715,6728,6735,6757,6658,6546,6719,6628,6701,6644,144,1030,688,621,651,253,636,679,667,703,615,251,255,249,168,161,1415,1175,254,256,250,162,252,166,160,195,176,174,238,180,158])).
% 59.14/59.24 cnf(6914,plain,
% 59.14/59.24 (P1(x69141,x69141,x69141)),
% 59.14/59.24 inference(rename_variables,[],[6686])).
% 59.14/59.24 cnf(6920,plain,
% 59.14/59.24 (P4(x69201,x69202,x69201,x69202,x69203,x69204,x69203,x69204)),
% 59.14/59.24 inference(scs_inference,[],[6672,6686,6901,6705,6608,6689,6697,6699,6715,6728,6735,6757,6658,6546,6719,6628,6701,6644,6616,6452,144,1030,688,621,651,253,636,679,667,703,615,251,255,249,168,161,1415,1175,254,256,250,162,252,166,160,195,176,174,238,180,158,196,175,259])).
% 59.14/59.24 cnf(6922,plain,
% 59.14/59.24 (P6(a16,a16,a1,a2)),
% 59.14/59.24 inference(scs_inference,[],[142,6672,6686,6901,6705,6608,6689,6697,6699,6715,6728,6735,6757,6658,6546,6719,6628,6701,6644,6616,6452,144,1030,688,621,651,253,636,679,667,703,615,251,255,249,168,161,1415,1175,254,256,250,162,252,166,160,195,176,174,238,180,158,196,175,259,233])).
% 59.14/59.24 cnf(6928,plain,
% 59.14/59.24 (P8(f23(a18,a18,a18,a18,a18,a18),a18,a18)),
% 59.14/59.24 inference(scs_inference,[],[142,6672,6686,6901,6705,6608,6689,6697,6699,6715,6728,6735,6757,6658,6546,6719,6628,6701,6644,6616,6452,319,144,1030,688,621,651,253,636,679,667,703,615,251,255,249,168,161,1415,1175,254,256,250,162,252,166,160,195,176,174,238,180,158,196,175,259,233,240,187,200])).
% 59.14/59.24 cnf(6931,plain,
% 59.14/59.24 (P10(x69311,x69312,x69312,x69311)),
% 59.14/59.24 inference(rename_variables,[],[6705])).
% 59.14/59.24 cnf(6938,plain,
% 59.14/59.24 (P10(x69381,x69382,x69382,x69381)),
% 59.14/59.24 inference(rename_variables,[],[6705])).
% 59.14/59.24 cnf(6940,plain,
% 59.14/59.24 (P3(a18,a18,a18,a18)),
% 59.14/59.24 inference(scs_inference,[],[142,6672,6686,6901,6705,6904,6931,6608,6689,6697,6699,6715,6728,6735,6757,6658,6546,6719,6628,6701,6644,6616,6452,319,144,1030,688,621,651,253,636,679,667,703,615,251,255,249,168,161,1415,1175,254,256,250,162,252,166,160,195,176,174,238,180,158,196,175,259,233,240,187,200,179,186,193,189,192])).
% 59.14/59.24 cnf(6942,plain,
% 59.14/59.24 (P5(a3,a3,a3,a3)),
% 59.14/59.24 inference(scs_inference,[],[142,6672,6686,6901,6705,6904,6931,6608,6689,6697,6699,6715,6728,6735,6757,6658,6546,6719,6628,6701,6644,6616,6614,6567,6452,319,144,1030,688,621,651,253,636,679,667,703,615,251,255,249,168,161,1415,1175,254,256,250,162,252,166,160,195,176,174,238,180,158,196,175,259,233,240,187,200,179,186,193,189,192,248])).
% 59.14/59.24 cnf(6946,plain,
% 59.14/59.24 (P8(f19(a18,x69461),a18,x69461)),
% 59.14/59.24 inference(scs_inference,[],[142,6672,6686,6901,6914,6705,6904,6931,6608,6689,6697,6699,6715,6728,6735,6757,6658,6546,6719,6628,6701,6644,6616,6614,6567,6452,319,144,1030,688,621,651,253,636,679,667,703,615,251,255,249,168,161,1415,1175,254,256,250,162,252,166,160,195,176,174,238,180,158,196,175,259,233,240,187,200,179,186,193,189,192,248,156])).
% 59.14/59.24 cnf(6952,plain,
% 59.14/59.24 (P4(a18,a18,a18,f25(a17,a3,a18,a18,a18),a18,f25(a17,a3,a18,a18,a18),a18,f25(a17,a3,a18,a18,a18))),
% 59.14/59.24 inference(scs_inference,[],[142,6672,6686,6901,6914,6705,6904,6931,6938,6608,6689,6697,6699,6715,6728,6735,6757,6658,6546,6719,6628,6701,6644,6616,6614,6567,4430,6452,319,143,144,1030,688,621,651,253,636,679,667,703,615,251,255,249,168,161,1415,1175,254,256,250,162,252,166,160,195,176,174,238,180,158,196,175,259,233,240,187,200,179,186,193,189,192,248,156,203,223])).
% 59.14/59.24 cnf(6956,plain,
% 59.14/59.24 (P8(f19(a18,x69561),x69561,a18)),
% 59.14/59.24 inference(scs_inference,[],[142,6672,6686,6901,6914,6705,6904,6931,6938,6608,6689,6697,6699,6715,6728,6735,6757,6658,6546,6719,6628,6701,6644,6616,6614,6567,4430,6452,319,143,144,1030,688,621,651,253,636,679,667,703,615,251,255,249,168,161,1415,1175,254,256,250,162,252,166,160,195,176,174,238,180,158,196,175,259,233,240,187,200,179,186,193,189,192,248,156,203,223,150,151])).
% 59.14/59.24 cnf(6958,plain,
% 59.14/59.24 (P10(a18,a18,a18,f25(a17,a3,a18,a18,a18))),
% 59.14/59.24 inference(scs_inference,[],[142,6672,6686,6901,6914,6705,6904,6931,6938,6608,6689,6697,6699,6715,6728,6735,6757,6658,6546,6719,6628,6701,6644,6616,6614,6567,4430,6452,319,143,144,1030,688,621,651,253,636,679,667,703,615,251,255,249,168,161,1415,1175,254,256,250,162,252,166,160,195,176,174,238,180,158,196,175,259,233,240,187,200,179,186,193,189,192,248,156,203,223,150,151,230])).
% 59.14/59.24 cnf(6960,plain,
% 59.14/59.24 (P5(f23(a18,a18,a18,a18,a18,a18),a18,f23(a18,a18,a18,a18,a18,a18),a18)),
% 59.14/59.24 inference(scs_inference,[],[142,6672,6686,6901,6914,6705,6904,6931,6938,6608,6689,6697,6699,6715,6728,6735,6757,6658,6546,6719,6628,6701,6644,6616,6614,6567,4430,6452,319,143,144,1030,688,621,651,253,636,679,667,703,615,251,255,249,168,161,1415,1175,254,256,250,162,252,166,160,195,176,174,238,180,158,196,175,259,233,240,187,200,179,186,193,189,192,248,156,203,223,150,151,230,153])).
% 59.14/59.24 cnf(6962,plain,
% 59.14/59.24 (P5(a18,a18,f25(a17,a3,a18,a18,a18),a18)),
% 59.14/59.24 inference(scs_inference,[],[142,6672,6686,6901,6914,6705,6904,6931,6938,6608,6689,6697,6699,6715,6728,6735,6757,6658,6546,6719,6628,6701,6644,6616,6614,6567,4430,6452,319,143,144,1030,688,621,651,253,636,679,667,703,615,251,255,249,168,161,1415,1175,254,256,250,162,252,166,160,195,176,174,238,180,158,196,175,259,233,240,187,200,179,186,193,189,192,248,156,203,223,150,151,230,153,165])).
% 59.14/59.24 cnf(6966,plain,
% 59.14/59.24 (P3(a3,a3,a3,a3)),
% 59.14/59.24 inference(scs_inference,[],[142,6672,6686,6901,6914,6705,6904,6931,6938,6608,6689,6697,6699,6715,6728,6735,6757,6658,6546,6719,6628,6701,6644,6616,6614,6567,4430,6452,319,143,144,1030,688,621,651,253,636,679,667,703,615,251,255,249,168,161,1415,1175,254,256,250,162,252,166,160,195,176,174,238,180,158,196,175,259,233,240,187,200,179,186,193,189,192,248,156,203,223,150,151,230,153,165,164,178])).
% 59.14/59.24 cnf(6968,plain,
% 59.14/59.24 (P2(a18,a18,a18,a18)),
% 59.14/59.24 inference(scs_inference,[],[142,6672,6686,6901,6914,6705,6904,6931,6938,6608,6689,6697,6699,6715,6728,6735,6757,6658,6546,6719,6628,6701,6644,6616,6614,6567,4430,6452,319,143,144,1030,688,621,651,253,636,679,667,703,615,251,255,249,168,161,1415,1175,254,256,250,162,252,166,160,195,176,174,238,180,158,196,175,259,233,240,187,200,179,186,193,189,192,248,156,203,223,150,151,230,153,165,164,178,181])).
% 59.14/59.25 cnf(6979,plain,
% 59.14/59.25 (P10(x69791,x69792,x69791,x69792)),
% 59.14/59.25 inference(rename_variables,[],[6624])).
% 59.14/59.25 cnf(6986,plain,
% 59.14/59.25 (P1(a18,a18,f4(a18,a18,a18))),
% 59.14/59.25 inference(scs_inference,[],[142,6672,6686,6901,6914,6705,6904,6931,6938,6608,6689,6697,6699,6715,6728,6735,6757,6658,6546,6719,6628,6701,6644,6616,6624,6979,6614,6567,4430,6452,319,143,144,1030,688,621,651,253,636,679,667,703,615,251,255,249,168,161,1415,1175,254,256,250,162,252,166,160,195,176,174,238,180,158,196,175,259,233,240,187,200,179,186,193,189,192,248,156,203,223,150,151,230,153,165,164,178,181,220,190,201,198,1671,1847,188,173])).
% 59.14/59.25 cnf(7005,plain,
% 59.14/59.25 (P9(a16,a3,a3,a3,a16,a17,a17,a17)),
% 59.14/59.25 inference(scs_inference,[],[6852,5927])).
% 59.14/59.25 cnf(7006,plain,
% 59.14/59.25 (P9(a2,a3,a3,a3,a2,a17,a17,a17)),
% 59.14/59.25 inference(scs_inference,[],[6852,5990])).
% 59.14/59.25 cnf(7018,plain,
% 59.14/59.25 (P9(a3,a17,a17,a17,a18,a3,a18,a3)),
% 59.14/59.25 inference(scs_inference,[],[6622,6942,6960,6952,1030,651,636,223,253])).
% 59.14/59.25 cnf(7026,plain,
% 59.14/59.25 (P6(a16,a16,a2,a1)),
% 59.14/59.25 inference(scs_inference,[],[6622,6922,6942,6968,6960,6952,1030,651,636,223,253,621,688,184,168])).
% 59.14/59.25 cnf(7036,plain,
% 59.14/59.25 (P4(a18,a3,a3,a18,x70361,x70362,x70362,x70361)),
% 59.14/59.25 inference(scs_inference,[],[6673,6622,6922,6942,6894,6968,6956,6960,6952,1030,651,636,223,253,621,688,184,168,150,667,615,255,249])).
% 59.14/59.25 cnf(7038,plain,
% 59.14/59.25 (P4(x70381,x70382,x70382,x70381,x70383,x70384,x70383,x70384)),
% 59.14/59.25 inference(scs_inference,[],[6673,6920,6622,6922,6942,6894,6968,6956,6960,6952,1030,651,636,223,253,621,688,184,168,150,667,615,255,249,251])).
% 59.14/59.25 cnf(7046,plain,
% 59.14/59.25 (P6(a2,a16,a1,a16)),
% 59.14/59.25 inference(scs_inference,[],[6673,6920,6622,6922,6942,6894,6968,6958,6956,6960,6952,1030,651,636,223,253,621,688,184,168,150,667,615,255,249,251,679,703,161,1415])).
% 59.14/59.25 cnf(7058,plain,
% 59.14/59.25 (P10(a17,a3,a17,f6(a18,a17,a3))),
% 59.14/59.25 inference(scs_inference,[],[6673,6920,6622,6922,6942,6894,6968,6652,6958,6731,6956,6960,6952,1030,651,636,223,253,621,688,184,168,150,667,615,255,249,251,679,703,161,1415,1175,256,162,254,250,160])).
% 59.14/59.25 cnf(7060,plain,
% 59.14/59.25 (P4(x70601,x70602,x70603,x70604,x70601,x70602,x70603,x70604)),
% 59.14/59.25 inference(scs_inference,[],[6673,6920,6622,6922,6942,6894,6968,6652,6958,6731,6956,6960,6952,1030,651,636,223,253,621,688,184,168,150,667,615,255,249,251,679,703,161,1415,1175,256,162,254,250,160,252])).
% 59.14/59.25 cnf(7062,plain,
% 59.14/59.25 (P6(a3,a18,a18,x70621)),
% 59.14/59.25 inference(scs_inference,[],[6673,6920,6622,6922,6942,6894,6882,6968,6652,6958,6731,6956,6960,6952,1030,651,636,223,253,621,688,184,168,150,667,615,255,249,251,679,703,161,1415,1175,256,162,254,250,160,252,166])).
% 59.14/59.25 cnf(7071,plain,
% 59.14/59.25 (P4(x70711,x70712,x70711,x70712,x70713,x70714,x70713,x70714)),
% 59.14/59.25 inference(rename_variables,[],[6920])).
% 59.14/59.25 cnf(7074,plain,
% 59.14/59.25 (P4(x70741,x70742,x70741,x70742,x70743,x70744,x70743,x70744)),
% 59.14/59.25 inference(rename_variables,[],[6920])).
% 59.14/59.25 cnf(7078,plain,
% 59.14/59.25 (P2(a3,a3,a3,a3)),
% 59.14/59.25 inference(scs_inference,[],[6673,6920,7071,6622,6922,6940,6942,6894,6882,6966,6968,6652,6958,6731,6946,6956,6960,6952,6962,1030,651,636,223,253,621,688,184,168,150,667,615,255,249,251,679,703,161,1415,1175,256,162,254,250,160,252,166,153,165,164,242,243,190,181])).
% 59.14/59.25 cnf(7093,plain,
% 59.14/59.25 (P1(x70931,x70932,x70932)),
% 59.14/59.25 inference(rename_variables,[],[6852])).
% 59.14/59.25 cnf(7095,plain,
% 59.14/59.25 (P5(a18,f23(a18,a18,a18,a18,a18,a18),a18,f23(a18,a18,a18,a18,a18,a18))),
% 59.14/59.25 inference(scs_inference,[],[6673,6920,7071,6852,6622,6922,6940,6942,6913,6911,6894,6882,6966,6968,6652,6958,6731,6928,6946,6956,6960,6952,6962,6569,1030,651,636,223,253,621,688,184,168,150,667,615,255,249,251,679,703,161,1415,1175,256,162,254,250,160,252,166,153,165,164,242,243,190,181,178,220,198,188,173,197,195,171])).
% 59.14/59.25 cnf(7099,plain,
% 59.14/59.25 (P3(x70991,x70992,x70991,x70992)),
% 59.14/59.25 inference(scs_inference,[],[6673,6920,7071,7074,6852,6622,6922,6940,6942,6913,6911,6894,6882,6966,6968,6652,6958,6731,6928,6946,6956,6960,6952,6962,6569,1030,651,636,223,253,621,688,184,168,150,667,615,255,249,251,679,703,161,1415,1175,256,162,254,250,160,252,166,153,165,164,242,243,190,181,178,220,198,188,173,197,195,171,196,238])).
% 59.14/59.25 cnf(7100,plain,
% 59.14/59.25 (P4(x71001,x71002,x71001,x71002,x71003,x71004,x71003,x71004)),
% 59.14/59.25 inference(rename_variables,[],[6920])).
% 59.14/59.25 cnf(7105,plain,
% 59.14/59.25 (P8(a3,a3,a3)),
% 59.14/59.25 inference(scs_inference,[],[6673,6920,7071,7074,6852,7093,6622,6922,6940,6942,6913,6911,6894,6882,6966,6968,6652,6958,6731,6928,6946,6956,6960,6952,6962,6569,6559,1030,651,636,223,253,621,688,184,168,150,667,615,255,249,251,679,703,161,1415,1175,256,162,254,250,160,252,166,153,165,164,242,243,190,181,178,220,198,188,173,197,195,171,196,238,93,185,158])).
% 59.14/59.25 cnf(7106,plain,
% 59.14/59.25 (P1(x71061,x71062,x71062)),
% 59.14/59.25 inference(rename_variables,[],[6852])).
% 59.14/59.25 cnf(7112,plain,
% 59.14/59.25 (P1(x71121,x71122,x71122)),
% 59.14/59.25 inference(rename_variables,[],[6852])).
% 59.14/59.25 cnf(7114,plain,
% 59.14/59.25 (P5(a18,a3,a18,a3)),
% 59.14/59.25 inference(scs_inference,[],[6673,6920,7071,7074,6852,7093,7106,6622,6922,6940,6942,6913,6911,6894,6882,6966,6968,6652,6958,6731,6928,6946,6956,6960,6952,6962,6569,6612,6559,6552,1030,651,636,223,253,621,688,184,168,150,667,615,255,249,251,679,703,161,1415,1175,256,162,254,250,160,252,166,153,165,164,242,243,190,181,178,220,198,188,173,197,195,171,196,238,93,185,158,187,233,240])).
% 59.14/59.25 cnf(7120,plain,
% 59.14/59.25 (P2(f10(a18,a3,a18),a18,a3,a18)),
% 59.14/59.25 inference(scs_inference,[],[6673,6920,7071,7074,6852,7093,7106,6622,6922,6940,6942,6913,6911,6894,6882,6966,6968,6652,6958,6731,6928,6946,6956,6960,6952,6962,6569,6612,6559,6552,6624,1030,651,636,223,253,621,688,184,168,150,667,615,255,249,251,679,703,161,1415,1175,256,162,254,250,160,252,166,153,165,164,242,243,190,181,178,220,198,188,173,197,195,171,196,238,93,185,158,187,233,240,186,224,189])).
% 59.14/59.25 cnf(7122,plain,
% 59.14/59.25 (P8(f19(a18,x71221),a18,x71221)),
% 59.14/59.25 inference(rename_variables,[],[6946])).
% 59.14/59.25 cnf(7123,plain,
% 59.14/59.25 (P10(x71231,x71232,x71231,x71232)),
% 59.14/59.25 inference(rename_variables,[],[6624])).
% 59.14/59.25 cnf(7125,plain,
% 59.14/59.25 (P8(f7(a18,a18,a18),a18,a18)),
% 59.14/59.25 inference(scs_inference,[],[6673,6920,7071,7074,6852,7093,7106,6622,6922,6940,6942,6913,6911,6894,6882,6966,6968,6652,6958,6731,6928,6946,6956,6960,6952,6962,6569,6612,6559,6552,6624,1030,651,636,223,253,621,688,184,168,150,667,615,255,249,251,679,703,161,1415,1175,256,162,254,250,160,252,166,153,165,164,242,243,190,181,178,220,198,188,173,197,195,171,196,238,93,185,158,187,233,240,186,224,189,183])).
% 59.14/59.25 cnf(7127,plain,
% 59.14/59.25 (P6(a3,a3,a3,a3)),
% 59.14/59.25 inference(scs_inference,[],[6673,6920,7071,7074,6852,7093,7106,6622,6922,6940,6942,6913,6911,6894,6882,6966,6968,6652,6958,6731,6928,6946,6956,6960,6952,6962,6569,6612,6559,6552,6624,1030,651,636,223,253,621,688,184,168,150,667,615,255,249,251,679,703,161,1415,1175,256,162,254,250,160,252,166,153,165,164,242,243,190,181,178,220,198,188,173,197,195,171,196,238,93,185,158,187,233,240,186,224,189,183,193])).
% 59.14/59.25 cnf(7129,plain,
% 59.14/59.25 (P8(a18,a18,f25(a17,a3,a18,a18,a18))),
% 59.14/59.25 inference(scs_inference,[],[6673,6920,7071,7074,6852,7093,7106,6622,6922,6940,6942,6913,6911,6894,6882,6966,6968,6652,6958,6731,6928,6946,6956,6960,6952,6962,6569,6612,6559,6552,6624,1030,651,636,223,253,621,688,184,168,150,667,615,255,249,251,679,703,161,1415,1175,256,162,254,250,160,252,166,153,165,164,242,243,190,181,178,220,198,188,173,197,195,171,196,238,93,185,158,187,233,240,186,224,189,183,193,159])).
% 59.14/59.25 cnf(7131,plain,
% 59.14/59.25 (P5(a16,a16,a2,a2)),
% 59.14/59.25 inference(scs_inference,[],[6673,6920,7071,7074,7100,6852,7093,7106,6622,6922,6940,6942,6913,6911,6894,6882,6966,6968,6652,6958,6731,6928,6946,6956,6960,6952,6962,6569,6612,6559,6552,6624,1030,651,636,223,253,621,688,184,168,150,667,615,255,249,251,679,703,161,1415,1175,256,162,254,250,160,252,166,153,165,164,242,243,190,181,178,220,198,188,173,197,195,171,196,238,93,185,158,187,233,240,186,224,189,183,193,159,248])).
% 59.14/59.25 cnf(7134,plain,
% 59.14/59.25 (P8(f19(a3,x71341),a3,x71341)),
% 59.14/59.25 inference(scs_inference,[],[6673,6920,7071,7074,7100,6852,7093,7106,7112,6622,6922,6940,6942,6913,6911,6894,6882,6966,6968,6652,6958,6731,6928,6946,6956,6960,6952,6962,6569,6612,6559,6552,6624,1030,651,636,223,253,621,688,184,168,150,667,615,255,249,251,679,703,161,1415,1175,256,162,254,250,160,252,166,153,165,164,242,243,190,181,178,220,198,188,173,197,195,171,196,238,93,185,158,187,233,240,186,224,189,183,193,159,248,156])).
% 59.14/59.25 cnf(7136,plain,
% 59.14/59.25 (P1(x71361,x71362,x71362)),
% 59.14/59.25 inference(rename_variables,[],[6852])).
% 59.14/59.25 cnf(7139,plain,
% 59.14/59.25 (P10(x71391,x71392,x71392,x71391)),
% 59.14/59.25 inference(rename_variables,[],[6705])).
% 59.14/59.25 cnf(7153,plain,
% 59.14/59.25 (P3(a3,a17,a17,a3)),
% 59.14/59.25 inference(scs_inference,[],[142,6673,6920,7071,7074,7100,6852,7093,7106,7112,6622,6922,6940,6942,6913,6911,6894,6882,6966,6968,6652,6958,6731,6928,6946,6956,6960,6952,6962,6569,6612,6705,6559,6552,6624,4413,4406,1030,651,636,223,253,621,688,184,168,150,667,615,255,249,251,679,703,161,1415,1175,256,162,254,250,160,252,166,153,165,164,242,243,190,181,178,220,198,188,173,197,195,171,196,238,93,185,158,187,233,240,186,224,189,183,193,159,248,156,203,1767,2202,2507,2685,2813,1070,4609])).
% 59.14/59.25 cnf(7155,plain,
% 59.14/59.25 (P10(a3,a18,a17,a3)),
% 59.14/59.25 inference(scs_inference,[],[142,6673,6920,7071,7074,7100,6852,7093,7106,7112,6622,6922,6940,6942,6913,6911,6894,6882,6966,6968,6652,6958,6731,6928,6946,6956,6960,6952,6962,6569,6612,6705,6559,6552,6624,4413,4406,1030,651,636,223,253,621,688,184,168,150,667,615,255,249,251,679,703,161,1415,1175,256,162,254,250,160,252,166,153,165,164,242,243,190,181,178,220,198,188,173,197,195,171,196,238,93,185,158,187,233,240,186,224,189,183,193,159,248,156,203,1767,2202,2507,2685,2813,1070,4609,4611])).
% 59.14/59.25 cnf(7157,plain,
% 59.14/59.25 (P8(a3,a17,a17)),
% 59.14/59.25 inference(scs_inference,[],[142,6673,6920,7071,7074,7100,6852,7093,7106,7112,6622,6922,6940,6942,6913,6911,6894,6882,6966,6968,6652,6958,6731,6928,6946,6956,6960,6952,6962,6569,6612,6705,6559,6552,6624,4413,4406,1030,651,636,223,253,621,688,184,168,150,667,615,255,249,251,679,703,161,1415,1175,256,162,254,250,160,252,166,153,165,164,242,243,190,181,178,220,198,188,173,197,195,171,196,238,93,185,158,187,233,240,186,224,189,183,193,159,248,156,203,1767,2202,2507,2685,2813,1070,4609,4611,5425])).
% 59.14/59.25 cnf(7161,plain,
% 59.14/59.25 (P8(a3,a18,a18)),
% 59.14/59.25 inference(scs_inference,[],[142,6673,6920,7071,7074,7100,6852,7093,7106,7112,6622,6922,6940,6942,6913,6911,6894,6882,6966,6968,6652,6958,6731,6928,6946,6956,6960,6952,6962,6569,6612,6705,6559,6552,6624,4413,4406,1030,651,636,223,253,621,688,184,168,150,667,615,255,249,251,679,703,161,1415,1175,256,162,254,250,160,252,166,153,165,164,242,243,190,181,178,220,198,188,173,197,195,171,196,238,93,185,158,187,233,240,186,224,189,183,193,159,248,156,203,1767,2202,2507,2685,2813,1070,4609,4611,5425,382,5412])).
% 59.14/59.25 cnf(7163,plain,
% 59.14/59.25 (P8(a18,f25(a17,a3,a18,a18,a18),a18)),
% 59.14/59.25 inference(scs_inference,[],[142,6673,6920,7071,7074,7100,6852,7093,7106,7112,6622,6922,6940,6942,6913,6911,6894,6882,6966,6968,6652,6958,6731,6928,6946,6956,6960,6952,6962,6569,6612,6705,6559,6552,6624,4413,4406,1030,651,636,223,253,621,688,184,168,150,667,615,255,249,251,679,703,161,1415,1175,256,162,254,250,160,252,166,153,165,164,242,243,190,181,178,220,198,188,173,197,195,171,196,238,93,185,158,187,233,240,186,224,189,183,193,159,248,156,203,1767,2202,2507,2685,2813,1070,4609,4611,5425,382,5412,151])).
% 59.14/59.25 cnf(7176,plain,
% 59.14/59.25 (P3(a18,a3,a3,a18)),
% 59.14/59.25 inference(scs_inference,[],[142,6673,6920,7071,7074,7100,6852,7093,7106,7112,7136,6622,6922,6940,6942,6913,6911,6894,6882,6966,6968,6652,6958,6731,6928,6946,7122,6956,6960,6952,6962,6569,6612,6519,6705,6559,6552,6624,4413,4406,1030,651,636,223,253,621,688,184,168,150,667,615,255,249,251,679,703,161,1415,1175,256,162,254,250,160,252,166,153,165,164,242,243,190,181,178,220,198,188,173,197,195,171,196,238,93,185,158,187,233,240,186,224,189,183,193,159,248,156,203,1767,2202,2507,2685,2813,1070,4609,4611,5425,382,5412,151,5513,202,246,2861,169])).
% 59.14/59.25 cnf(7177,plain,
% 59.14/59.25 (P1(x71771,x71772,x71772)),
% 59.14/59.25 inference(rename_variables,[],[6852])).
% 59.14/59.25 cnf(7180,plain,
% 59.14/59.25 (P10(x71801,x71802,x71802,x71801)),
% 59.14/59.25 inference(rename_variables,[],[6705])).
% 59.14/59.25 cnf(7185,plain,
% 59.14/59.25 (P10(x71851,x71852,x71852,x71851)),
% 59.14/59.25 inference(rename_variables,[],[6705])).
% 59.14/59.25 cnf(7192,plain,
% 59.14/59.25 (P8(f23(a3,a3,a3,a3,a3,a3),a3,a3)),
% 59.14/59.25 inference(scs_inference,[],[142,6673,6920,7071,7074,7100,6852,7093,7106,7112,7136,6622,6922,6940,6942,6913,6911,6894,6882,6966,6968,6652,6958,6731,6928,6946,7122,6956,6960,6952,6962,6569,6612,6519,6705,7139,7180,6559,6552,6614,6624,4413,4406,1030,651,636,223,253,621,688,184,168,150,667,615,255,249,251,679,703,161,1415,1175,256,162,254,250,160,252,166,153,165,164,242,243,190,181,178,220,198,188,173,197,195,171,196,238,93,185,158,187,233,240,186,224,189,183,193,159,248,156,203,1767,2202,2507,2685,2813,1070,4609,4611,5425,382,5412,151,5513,202,246,2861,169,1847,201,1671,239,174,200])).
% 59.14/59.25 cnf(7201,plain,
% 59.14/59.25 (P1(a3,a17,a18)),
% 59.14/59.25 inference(scs_inference,[],[142,6673,6920,7071,7074,7100,6852,7093,7106,7112,7136,7177,6622,6922,6940,6942,6913,6911,6894,6882,6966,6968,6652,6958,6731,6928,6946,7122,6956,6960,6952,6962,6569,6612,6519,6705,7139,7180,7185,6559,6552,6614,6624,7123,4413,4406,1030,651,636,223,253,621,688,184,168,150,667,615,255,249,251,679,703,161,1415,1175,256,162,254,250,160,252,166,153,165,164,242,243,190,181,178,220,198,188,173,197,195,171,196,238,93,185,158,187,233,240,186,224,189,183,193,159,248,156,203,1767,2202,2507,2685,2813,1070,4609,4611,5425,382,5412,151,5513,202,246,2861,169,1847,201,1671,239,174,200,175,205,1076])).
% 59.14/59.25 cnf(7202,plain,
% 59.14/59.25 (P10(a3,a18,a3,a17)),
% 59.14/59.25 inference(scs_inference,[],[142,6673,6920,7071,7074,7100,6852,7093,7106,7112,7136,7177,6622,6922,6940,6942,6913,6911,6894,6882,6966,6968,6652,6958,6731,6928,6946,7122,6956,6960,6952,6962,6569,6612,6519,6705,7139,7180,7185,6559,6552,6614,6624,7123,4413,4406,1030,651,636,223,253,621,688,184,168,150,667,615,255,249,251,679,703,161,1415,1175,256,162,254,250,160,252,166,153,165,164,242,243,190,181,178,220,198,188,173,197,195,171,196,238,93,185,158,187,233,240,186,224,189,183,193,159,248,156,203,1767,2202,2507,2685,2813,1070,4609,4611,5425,382,5412,151,5513,202,246,2861,169,1847,201,1671,239,174,200,175,205,1076,1072])).
% 59.14/59.25 cnf(7203,plain,
% 59.14/59.25 (P4(a3,a18,x72031,x72032,a3,a17,x72031,x72032)),
% 59.14/59.25 inference(scs_inference,[],[142,6673,6920,7071,7074,7100,6852,7093,7106,7112,7136,7177,6622,6922,6940,6942,6913,6911,6894,6882,6966,6968,6652,6958,6731,6928,6946,7122,6956,6960,6952,6962,6569,6612,6519,6705,7139,7180,7185,6559,6552,6614,6624,7123,4413,4406,1030,651,636,223,253,621,688,184,168,150,667,615,255,249,251,679,703,161,1415,1175,256,162,254,250,160,252,166,153,165,164,242,243,190,181,178,220,198,188,173,197,195,171,196,238,93,185,158,187,233,240,186,224,189,183,193,159,248,156,203,1767,2202,2507,2685,2813,1070,4609,4611,5425,382,5412,151,5513,202,246,2861,169,1847,201,1671,239,174,200,175,205,1076,1072,1223])).
% 59.14/59.25 cnf(7208,plain,
% 59.14/59.25 (P10(a18,a3,a17,a3)),
% 59.14/59.25 inference(scs_inference,[],[142,6673,6920,7071,7074,7100,6852,7093,7106,7112,7136,7177,6622,6922,6940,6942,6913,6911,6894,6882,6966,6968,6652,6958,6731,6928,6946,7122,6956,6960,6952,6962,6569,6612,6519,6705,7139,7180,7185,6559,6552,6614,6624,7123,4413,4406,1030,651,636,223,253,621,688,184,168,150,667,615,255,249,251,679,703,161,1415,1175,256,162,254,250,160,252,166,153,165,164,242,243,190,181,178,220,198,188,173,197,195,171,196,238,93,185,158,187,233,240,186,224,189,183,193,159,248,156,203,1767,2202,2507,2685,2813,1070,4609,4611,5425,382,5412,151,5513,202,246,2861,169,1847,201,1671,239,174,200,175,205,1076,1072,1223,3228,586,4419])).
% 59.14/59.25 cnf(7213,plain,
% 59.14/59.25 (~P8(x72131,a17,a16)+~P11(f19(a17,a1),a1,a17,f19(a17,a1),a17,a3)),
% 59.14/59.25 inference(scs_inference,[],[7157,1863])).
% 59.14/59.25 cnf(7217,plain,
% 59.14/59.25 (P8(f19(a3,x72171),a3,x72171)),
% 59.14/59.25 inference(rename_variables,[],[7134])).
% 59.14/59.25 cnf(7219,plain,
% 59.14/59.25 (~P3(a17,f19(a3,a1),a1,a3)),
% 59.14/59.25 inference(scs_inference,[],[7134,7217,2346,416])).
% 59.14/59.25 cnf(7220,plain,
% 59.14/59.25 (P8(f19(a3,x72201),a3,x72201)),
% 59.14/59.25 inference(rename_variables,[],[7134])).
% 59.14/59.25 cnf(7223,plain,
% 59.14/59.25 (P8(f19(a3,x72231),a3,x72231)),
% 59.14/59.25 inference(rename_variables,[],[7134])).
% 59.14/59.25 cnf(7226,plain,
% 59.14/59.25 (P8(f19(a3,x72261),a3,x72261)),
% 59.14/59.25 inference(rename_variables,[],[7134])).
% 59.14/59.25 cnf(7229,plain,
% 59.14/59.25 (P3(x72291,x72292,x72291,x72292)),
% 59.14/59.25 inference(rename_variables,[],[7099])).
% 59.14/59.25 cnf(7232,plain,
% 59.14/59.25 (P8(f19(a3,x72321),a3,x72321)),
% 59.14/59.25 inference(rename_variables,[],[7134])).
% 59.14/59.25 cnf(7235,plain,
% 59.14/59.25 (P8(f19(a3,x72351),a3,x72351)),
% 59.14/59.25 inference(rename_variables,[],[7134])).
% 59.14/59.25 cnf(7240,plain,
% 59.14/59.25 (P8(f19(a3,x72401),a3,x72401)),
% 59.14/59.25 inference(rename_variables,[],[7134])).
% 59.14/59.25 cnf(7243,plain,
% 59.14/59.25 (P8(f19(a3,x72431),a3,x72431)),
% 59.14/59.25 inference(rename_variables,[],[7134])).
% 59.14/59.25 cnf(7253,plain,
% 59.14/59.25 (P4(x72531,x72532,x72531,x72532,x72533,x72534,x72534,x72533)),
% 59.14/59.25 inference(scs_inference,[],[7038,7099,7114,7192,7134,7217,7220,7223,7226,7232,7235,7240,2346,416,2378,279,1070,485,2058,5412,2026,436,223,5425,621,651,249])).
% 59.14/59.25 cnf(7263,plain,
% 59.14/59.25 (P8(f19(a3,x72631),x72631,a3)),
% 59.14/59.25 inference(scs_inference,[],[7005,7038,7099,7078,7114,7192,7134,7217,7220,7223,7226,7232,7235,7240,7243,2346,416,2378,279,1070,485,2058,5412,2026,436,223,5425,621,651,249,636,150,184,253,151])).
% 59.14/59.25 cnf(7273,plain,
% 59.14/59.25 (P4(x72731,x72732,x72733,x72734,x72732,x72731,x72733,x72734)),
% 59.14/59.25 inference(scs_inference,[],[6674,7005,7038,7060,7099,7078,7114,7192,7134,7217,7220,7223,7226,7232,7235,7240,7243,2346,416,2378,279,1070,485,2058,5412,2026,436,223,5425,621,651,249,636,150,184,253,151,667,615,255,688,251])).
% 59.14/59.25 cnf(7281,plain,
% 59.14/59.25 (P6(a18,a18,x72811,a3)),
% 59.14/59.25 inference(scs_inference,[],[6674,7005,7038,7060,7099,6884,7046,7078,7114,7192,7134,7217,7220,7223,7226,7232,7235,7240,7243,2346,416,2378,279,1070,485,2058,5412,2026,436,223,5425,621,651,249,636,150,184,253,151,667,615,255,688,251,168,679,703,1415])).
% 59.14/59.25 cnf(7287,plain,
% 59.14/59.25 (P6(a18,x72871,a3,a18)),
% 59.14/59.25 inference(scs_inference,[],[6674,7005,7038,7060,7099,7036,6884,7046,7078,7114,7058,7192,7134,7217,7220,7223,7226,7232,7235,7240,7243,2346,416,2378,279,1070,485,2058,5412,2026,436,223,5425,621,651,249,636,150,184,253,151,667,615,255,688,251,168,679,703,1415,250,161,1175])).
% 59.14/59.25 cnf(7293,plain,
% 59.14/59.25 (P4(a3,a18,a3,a17,x72931,x72932,x72931,x72932)),
% 59.14/59.25 inference(scs_inference,[],[6674,7005,7038,7060,7099,7036,7203,6884,7046,7078,7114,7153,7058,7192,7134,7217,7220,7223,7226,7232,7235,7240,7243,2346,416,2378,279,1070,485,2058,5412,2026,436,223,5425,621,651,249,636,150,184,253,151,667,615,255,688,251,168,679,703,1415,250,161,1175,256,162,252])).
% 59.14/59.25 cnf(7299,plain,
% 59.14/59.25 (P10(a3,a17,a3,a18)),
% 59.14/59.25 inference(scs_inference,[],[6674,7005,7038,7060,7099,7202,7036,7203,6884,7046,7078,7114,7153,7058,7192,7134,7217,7220,7223,7226,7232,7235,7240,7243,2346,416,2378,279,1070,485,2058,5412,2026,436,223,5425,621,651,249,636,150,184,253,151,667,615,255,688,251,168,679,703,1415,250,161,1175,256,162,252,254,166,160])).
% 59.14/59.25 cnf(7301,plain,
% 59.14/59.25 (P5(a3,a17,a3,a17)),
% 59.14/59.25 inference(scs_inference,[],[6674,7005,7038,7060,7099,7202,7157,7036,7203,6884,7046,7078,7114,7153,7058,7192,7134,7217,7220,7223,7226,7232,7235,7240,7243,2346,416,2378,279,1070,485,2058,5412,2026,436,223,5425,621,651,249,636,150,184,253,151,667,615,255,688,251,168,679,703,1415,250,161,1175,256,162,252,254,166,160,153])).
% 59.14/59.25 cnf(7310,plain,
% 59.14/59.25 (P4(x73101,x73102,x73102,x73101,x73103,x73104,x73103,x73104)),
% 59.14/59.25 inference(rename_variables,[],[7038])).
% 59.14/59.25 cnf(7318,plain,
% 59.14/59.25 (P10(x73181,x73182,x73181,x73182)),
% 59.14/59.25 inference(rename_variables,[],[6624])).
% 59.14/59.25 cnf(7321,plain,
% 59.14/59.25 (P3(x73211,x73212,x73211,x73212)),
% 59.14/59.25 inference(rename_variables,[],[7099])).
% 59.14/59.25 cnf(7326,plain,
% 59.14/59.25 (P3(x73261,x73262,x73261,x73262)),
% 59.14/59.25 inference(rename_variables,[],[7099])).
% 59.14/59.25 cnf(7327,plain,
% 59.14/59.25 (P4(x73271,x73272,x73272,x73271,x73273,x73274,x73273,x73274)),
% 59.14/59.25 inference(rename_variables,[],[7038])).
% 59.14/59.25 cnf(7330,plain,
% 59.14/59.25 (P3(x73301,x73302,x73301,x73302)),
% 59.14/59.25 inference(rename_variables,[],[7099])).
% 59.14/59.25 cnf(7332,plain,
% 59.14/59.25 (P2(a18,a3,a3,a3)),
% 59.14/59.25 inference(scs_inference,[],[142,6674,7005,7038,7310,7060,7099,7229,7321,7326,7202,7157,7161,7036,7203,6884,6610,7046,7078,7114,7131,7153,7058,7125,7192,7134,7217,7220,7223,7226,7232,7235,7240,7243,6624,6446,2346,416,2378,279,1070,485,2058,5412,2026,436,223,5425,621,651,249,636,150,184,253,151,667,615,255,688,251,168,679,703,1415,250,161,1175,256,162,252,254,166,160,153,165,164,4113,242,246,220,1671,198,202,243,194,181])).
% 59.14/59.25 cnf(7334,plain,
% 59.14/59.25 (P3(a18,a18,a3,a3)),
% 59.14/59.25 inference(scs_inference,[],[142,6674,7005,7038,7310,7060,7099,7229,7321,7326,7202,7157,7161,7036,7203,6884,6610,7046,7078,7114,7131,7153,7058,7125,7192,7134,7217,7220,7223,7226,7232,7235,7240,7243,6624,6446,2346,416,2378,279,1070,485,2058,5412,2026,436,223,5425,621,651,249,636,150,184,253,151,667,615,255,688,251,168,679,703,1415,250,161,1175,256,162,252,254,166,160,153,165,164,4113,242,246,220,1671,198,202,243,194,181,178])).
% 59.14/59.25 cnf(7340,plain,
% 59.14/59.25 (P8(f19(a3,x73401),a3,x73401)),
% 59.14/59.25 inference(rename_variables,[],[7134])).
% 59.14/59.25 cnf(7342,plain,
% 59.14/59.25 (P3(x73421,x73422,x73421,x73422)),
% 59.14/59.25 inference(rename_variables,[],[7099])).
% 59.14/59.25 cnf(7347,plain,
% 59.14/59.25 (P3(x73471,x73472,x73471,x73472)),
% 59.14/59.25 inference(rename_variables,[],[7099])).
% 59.14/59.25 cnf(7351,plain,
% 59.14/59.25 (P5(a3,a3,a17,a3)),
% 59.14/59.25 inference(scs_inference,[],[142,6674,7005,7038,7310,7060,7099,7229,7321,7326,7330,7342,7105,7202,7157,7161,7036,7203,6884,6610,7046,7078,7114,7131,7153,7176,7058,7125,7192,7134,7217,7220,7223,7226,7232,7235,7240,7243,7163,6624,7318,6446,261,2346,416,2378,279,1070,485,2058,5412,2026,436,223,5425,621,651,249,636,150,184,253,151,667,615,255,688,251,168,679,703,1415,250,161,1175,256,162,252,254,166,160,153,165,164,4113,242,246,220,1671,198,202,243,194,181,178,1847,139,170,188,195,173,171])).
% 59.14/59.25 cnf(7357,plain,
% 59.14/59.25 (P3(x73571,x73572,x73571,x73572)),
% 59.14/59.25 inference(rename_variables,[],[7099])).
% 59.14/59.25 cnf(7363,plain,
% 59.14/59.25 (P3(x73631,x73632,x73632,x73631)),
% 59.14/59.25 inference(scs_inference,[],[142,6674,7005,7038,7310,7327,7060,7099,7229,7321,7326,7330,7342,7347,7357,7105,7202,7157,7161,7036,7203,6884,6610,7018,7046,7078,7114,7131,7153,7176,7058,6898,7125,7192,7134,7217,7220,7223,7226,7232,7235,7240,7243,7163,6624,7318,6446,261,2346,416,2378,279,1070,485,2058,5412,2026,436,223,5425,621,651,249,636,150,184,253,151,667,615,255,688,251,168,679,703,1415,250,161,1175,256,162,252,254,166,160,153,165,164,4113,242,246,220,1671,198,202,243,194,181,178,1847,139,170,188,195,173,171,237,197,260,196,238])).
% 59.14/59.25 cnf(7364,plain,
% 59.14/59.25 (P3(x73641,x73642,x73641,x73642)),
% 59.14/59.25 inference(rename_variables,[],[7099])).
% 59.14/59.25 cnf(7366,plain,
% 59.14/59.25 (P5(a16,a16,a16,a16)),
% 59.14/59.25 inference(scs_inference,[],[142,6674,7005,7038,7310,7327,7060,7099,7229,7321,7326,7330,7342,7347,7357,7105,7202,7157,7161,7036,7203,6884,6610,7018,7046,7078,7114,7131,7153,7176,7058,6898,7125,7192,7134,7217,7220,7223,7226,7232,7235,7240,7243,7163,6624,7318,6446,261,2346,416,2378,279,1070,485,2058,5412,2026,436,223,5425,621,651,249,636,150,184,253,151,667,615,255,688,251,168,679,703,1415,250,161,1175,256,162,252,254,166,160,153,165,164,4113,242,246,220,1671,198,202,243,194,181,178,1847,139,170,188,195,173,171,237,197,260,196,238,180])).
% 59.14/59.25 cnf(7370,plain,
% 59.14/59.25 (P5(a18,a18,a18,f4(a18,a18,a18))),
% 59.14/59.25 inference(scs_inference,[],[142,6674,7005,7038,7310,7327,7060,7099,7229,7321,7326,7330,7342,7347,7357,7364,7105,7202,7157,7161,7036,7203,6884,6610,7018,7046,7078,7114,7131,7153,7176,7058,6898,7125,7192,7134,7217,7220,7223,7226,7232,7235,7240,7243,7163,6911,6624,7318,6446,261,2346,416,2378,279,1070,485,2058,5412,2026,436,223,5425,621,651,249,636,150,184,253,151,667,615,255,688,251,168,679,703,1415,250,161,1175,256,162,252,254,166,160,153,165,164,4113,242,246,220,1671,198,202,243,194,181,178,1847,139,170,188,195,173,171,237,197,260,196,238,180,200,185])).
% 59.14/59.25 cnf(7371,plain,
% 59.14/59.25 (P3(x73711,x73712,x73711,x73712)),
% 59.14/59.25 inference(rename_variables,[],[7099])).
% 59.14/59.25 cnf(7373,plain,
% 59.14/59.25 (P1(f5(x73731,x73731,x73732),x73732,x73731)),
% 59.14/59.25 inference(scs_inference,[],[142,6674,7005,7038,7310,7327,7060,7099,7229,7321,7326,7330,7342,7347,7357,7364,7371,7105,7202,7157,7161,7036,7203,6884,6610,7018,7046,7078,7114,7131,7153,7176,7058,6898,7125,7192,7134,7217,7220,7223,7226,7232,7235,7240,7243,7163,6911,6624,7318,6446,261,2346,416,2378,279,1070,485,2058,5412,2026,436,223,5425,621,651,249,636,150,184,253,151,667,615,255,688,251,168,679,703,1415,250,161,1175,256,162,252,254,166,160,153,165,164,4113,242,246,220,1671,198,202,243,194,181,178,1847,139,170,188,195,173,171,237,197,260,196,238,180,200,185,174])).
% 59.14/59.25 cnf(7375,plain,
% 59.14/59.25 (P3(x73751,f6(x73751,x73751,x73752),x73752,x73751)),
% 59.14/59.25 inference(scs_inference,[],[142,6674,7005,7038,7310,7327,7060,7099,7229,7321,7326,7330,7342,7347,7357,7364,7371,7105,7202,7157,7161,7036,7203,6884,6610,7018,7046,7078,7114,7131,7153,7176,7058,6898,7125,7192,7134,7217,7220,7223,7226,7232,7235,7240,7243,7163,6911,6624,7318,6446,261,2346,416,2378,279,1070,485,2058,5412,2026,436,223,5425,621,651,249,636,150,184,253,151,667,615,255,688,251,168,679,703,1415,250,161,1175,256,162,252,254,166,160,153,165,164,4113,242,246,220,1671,198,202,243,194,181,178,1847,139,170,188,195,173,171,237,197,260,196,238,180,200,185,174,187])).
% 59.14/59.25 cnf(7379,plain,
% 59.14/59.25 (P8(a18,a3,a3)),
% 59.14/59.25 inference(scs_inference,[],[142,6674,7005,7038,7310,7327,7060,7099,7229,7321,7326,7330,7342,7347,7357,7364,7371,7105,7202,7157,7161,7036,7203,6884,6610,7018,7046,7078,7114,7131,7153,7176,7058,6898,7125,7192,7134,7217,7220,7223,7226,7232,7235,7240,7243,7163,6852,6911,6624,7318,6446,261,2346,416,2378,279,1070,485,2058,5412,2026,436,223,5425,621,651,249,636,150,184,253,151,667,615,255,688,251,168,679,703,1415,250,161,1175,256,162,252,254,166,160,153,165,164,4113,242,246,220,1671,198,202,243,194,181,178,1847,139,170,188,195,173,171,237,197,260,196,238,180,200,185,174,187,175,158])).
% 59.14/59.25 cnf(7380,plain,
% 59.14/59.25 (P1(x73801,x73802,x73802)),
% 59.14/59.25 inference(rename_variables,[],[6852])).
% 59.14/59.25 cnf(7382,plain,
% 59.14/59.25 (P5(a3,a17,a17,a17)),
% 59.14/59.25 inference(scs_inference,[],[142,6674,7005,7038,7310,7327,7060,7099,7229,7321,7326,7330,7342,7347,7357,7364,7371,7105,7202,7157,7161,7036,7203,6884,6610,7018,7046,7078,7114,7131,7153,7176,7058,6898,7125,7192,7134,7217,7220,7223,7226,7232,7235,7240,7243,7163,6852,6911,6624,7318,6446,261,2346,416,2378,279,1070,485,2058,5412,2026,436,223,5425,621,651,249,636,150,184,253,151,667,615,255,688,251,168,679,703,1415,250,161,1175,256,162,252,254,166,160,153,165,164,4113,242,246,220,1671,198,202,243,194,181,178,1847,139,170,188,195,173,171,237,197,260,196,238,180,200,185,174,187,175,158,240])).
% 59.14/59.25 cnf(7384,plain,
% 59.14/59.25 (~P10(a17,f19(a3,a1),a1,a3)),
% 59.14/59.25 inference(scs_inference,[],[142,6674,7005,7038,7310,7327,7060,7099,7229,7321,7326,7330,7342,7347,7357,7364,7371,7105,7202,7157,7161,7036,7203,6884,6610,7018,7046,7078,7114,7131,7153,7176,7058,6898,7125,7192,7134,7217,7220,7223,7226,7232,7235,7240,7243,7163,6852,6911,6624,7318,6446,261,2346,416,2378,279,1070,485,2058,5412,2026,436,223,5425,621,651,249,636,150,184,253,151,667,615,255,688,251,168,679,703,1415,250,161,1175,256,162,252,254,166,160,153,165,164,4113,242,246,220,1671,198,202,243,194,181,178,1847,139,170,188,195,173,171,237,197,260,196,238,180,200,185,174,187,175,158,240,179])).
% 59.14/59.25 cnf(7385,plain,
% 59.14/59.25 (P3(x73851,x73852,x73851,x73852)),
% 59.14/59.25 inference(rename_variables,[],[7099])).
% 59.14/59.25 cnf(7392,plain,
% 59.14/59.25 (P4(a18,a3,a18,a18,f10(a18,a3,a18),a3,f10(a18,a3,a18),f19(a3,a18))),
% 59.14/59.25 inference(scs_inference,[],[142,6674,7005,7038,7310,7327,7060,7099,7229,7321,7326,7330,7342,7347,7357,7364,7371,7385,7105,7202,7157,7161,7201,7036,7203,6884,6610,7018,7046,7078,7114,7131,7153,7176,7058,6898,7125,7192,7134,7217,7220,7223,7226,7232,7235,7240,7243,7340,7163,7120,6852,6911,6920,6624,7318,6446,261,2346,416,2378,279,1070,485,2058,5412,2026,436,223,5425,621,651,249,636,150,184,253,151,667,615,255,688,251,168,679,703,1415,250,161,1175,256,162,252,254,166,160,153,165,164,4113,242,246,220,1671,198,202,243,194,181,178,1847,139,170,188,195,173,171,237,197,260,196,238,180,200,185,174,187,175,158,240,179,233,186,224])).
% 59.14/59.25 cnf(7393,plain,
% 59.14/59.25 (P8(f19(a3,x73931),a3,x73931)),
% 59.14/59.25 inference(rename_variables,[],[7134])).
% 59.14/59.25 cnf(7396,plain,
% 59.14/59.25 (P10(x73961,x73962,x73962,x73961)),
% 59.14/59.25 inference(rename_variables,[],[6705])).
% 59.14/59.25 cnf(7400,plain,
% 59.14/59.25 (P3(x74001,x74002,x74001,x74002)),
% 59.14/59.25 inference(rename_variables,[],[7099])).
% 59.14/59.25 cnf(7402,plain,
% 59.14/59.25 (P8(a3,a17,a18)),
% 59.14/59.25 inference(scs_inference,[],[142,6674,7005,7038,7310,7327,7060,7099,7229,7321,7326,7330,7342,7347,7357,7364,7371,7385,7105,7202,7127,7157,7161,7201,7036,7203,6884,6610,7018,7046,7078,7114,7131,7153,7176,7058,6898,7125,7192,7134,7217,7220,7223,7226,7232,7235,7240,7243,7340,7163,7120,6852,6705,6911,6920,6624,7318,6446,261,2346,416,2378,279,1070,485,2058,5412,2026,436,223,5425,621,651,249,636,150,184,253,151,667,615,255,688,251,168,679,703,1415,250,161,1175,256,162,252,254,166,160,153,165,164,4113,242,246,220,1671,198,202,243,194,181,178,1847,139,170,188,195,173,171,237,197,260,196,238,180,200,185,174,187,175,158,240,179,233,186,224,189,183,172])).
% 59.14/59.25 cnf(7407,plain,
% 59.14/59.25 (P5(a3,a18,a3,a18)),
% 59.14/59.25 inference(scs_inference,[],[142,6674,7005,7038,7310,7327,7060,7099,7229,7321,7326,7330,7342,7347,7357,7364,7371,7385,6565,7105,7202,7127,7155,7157,7161,7201,7036,7203,6884,6610,7018,7046,7078,7114,7131,7153,7176,7058,6898,7125,7192,7134,7217,7220,7223,7226,7232,7235,7240,7243,7340,7163,7120,6852,7380,6705,6911,6920,6624,7318,6446,261,2346,416,2378,279,1070,485,2058,5412,2026,436,223,5425,621,651,249,636,150,184,253,151,667,615,255,688,251,168,679,703,1415,250,161,1175,256,162,252,254,166,160,153,165,164,4113,242,246,220,1671,198,202,243,194,181,178,1847,139,170,188,195,173,171,237,197,260,196,238,180,200,185,174,187,175,158,240,179,233,186,224,189,183,172,206,248])).
% 59.14/59.25 cnf(7411,plain,
% 59.14/59.25 (P8(f19(a17,x74111),a17,x74111)),
% 59.14/59.25 inference(scs_inference,[],[142,6674,7005,7038,7310,7327,7060,7099,7229,7321,7326,7330,7342,7347,7357,7364,7371,7385,6565,7105,7202,7127,7155,7157,7161,7201,7036,7203,6884,6610,7018,7046,7078,7114,7131,7153,7176,7058,6898,7125,7192,7134,7217,7220,7223,7226,7232,7235,7240,7243,7340,7163,7120,6852,7380,6705,6956,6911,6920,6624,7318,6446,261,2346,416,2378,279,1070,485,2058,5412,2026,436,223,5425,621,651,249,636,150,184,253,151,667,615,255,688,251,168,679,703,1415,250,161,1175,256,162,252,254,166,160,153,165,164,4113,242,246,220,1671,198,202,243,194,181,178,1847,139,170,188,195,173,171,237,197,260,196,238,180,200,185,174,187,175,158,240,179,233,186,224,189,183,172,206,248,156])).
% 59.14/59.25 cnf(7419,plain,
% 59.14/59.25 (P1(a18,a3,a17)),
% 59.14/59.25 inference(scs_inference,[],[142,6674,7005,7038,7310,7327,7060,7099,7229,7321,7326,7330,7342,7347,7357,7364,7371,7385,6565,7105,7202,7127,7155,7157,7161,7201,7036,7203,6884,6610,7018,7046,7078,7114,7131,7153,7176,7058,6898,7125,7192,7134,7217,7220,7223,7226,7232,7235,7240,7243,7340,7163,7120,6852,7380,6705,6956,6911,6920,6624,7318,6446,261,2346,416,2378,279,1070,485,2058,5412,2026,436,223,5425,621,651,249,636,150,184,253,151,667,615,255,688,251,168,679,703,1415,250,161,1175,256,162,252,254,166,160,153,165,164,4113,242,246,220,1671,198,202,243,194,181,178,1847,139,170,188,195,173,171,237,197,260,196,238,180,200,185,174,187,175,158,240,179,233,186,224,189,183,172,206,248,156,4561,4786,1271,1287])).
% 59.14/59.25 cnf(7476,plain,
% 59.14/59.25 (~P8(a17,a1,a1)),
% 59.14/59.25 inference(scs_inference,[],[142,6674,7005,7038,7310,7327,7060,7099,7229,7321,7326,7330,7342,7347,7357,7364,7371,7385,6565,7105,7202,7127,7155,7157,7161,7201,7036,7203,6884,6610,7018,7046,7078,7114,7131,7153,7176,7058,6898,7125,7192,7134,7217,7220,7223,7226,7232,7235,7240,7243,7340,7393,7163,7120,6852,7380,6705,6956,6911,6920,6624,7318,6728,6446,261,2346,416,2378,279,1070,485,2058,5412,2026,436,223,5425,621,651,249,636,150,184,253,151,667,615,255,688,251,168,679,703,1415,250,161,1175,256,162,252,254,166,160,153,165,164,4113,242,246,220,1671,198,202,243,194,181,178,1847,139,170,188,195,173,171,237,197,260,196,238,180,200,185,174,187,175,158,240,179,233,186,224,189,183,172,206,248,156,4561,4786,1271,1287,1303,1319,1335,470,1703,1783,2042,2186,2218,2362,2523,2621,2749,405,3470,3422,3244,3454,380,584,3163,575,586,401,3631,382,917,227,3663,155])).
% 59.14/59.25 cnf(7482,plain,
% 59.14/59.25 (~P4(a17,f19(a3,a1),a1,a3,a1,a3,a17,f19(a3,a1))),
% 59.14/59.25 inference(scs_inference,[],[142,6674,7005,7038,7310,7327,7060,7099,7229,7321,7326,7330,7342,7347,7357,7364,7371,7385,6565,7105,7202,7127,7155,7157,7161,7201,7036,7203,6884,6610,7018,7046,7078,7114,7131,7153,7176,7058,6898,7125,7192,7134,7217,7220,7223,7226,7232,7235,7240,7243,7340,7393,7163,7120,6852,7380,6705,6956,6911,6920,6624,7318,6728,6446,261,2346,416,2378,279,1070,485,2058,5412,2026,436,223,5425,621,651,249,636,150,184,253,151,667,615,255,688,251,168,679,703,1415,250,161,1175,256,162,252,254,166,160,153,165,164,4113,242,246,220,1671,198,202,243,194,181,178,1847,139,170,188,195,173,171,237,197,260,196,238,180,200,185,174,187,175,158,240,179,233,186,224,189,183,172,206,248,156,4561,4786,1271,1287,1303,1319,1335,470,1703,1783,2042,2186,2218,2362,2523,2621,2749,405,3470,3422,3244,3454,380,584,3163,575,586,401,3631,382,917,227,3663,155,190,201,235])).
% 59.14/59.25 cnf(7484,plain,
% 59.14/59.25 (~P10(f19(a3,a1),a17,a1,a3)),
% 59.14/59.25 inference(scs_inference,[],[142,6674,7005,7038,7310,7327,7060,7099,7229,7321,7326,7330,7342,7347,7357,7364,7371,7385,6565,7105,7202,7127,7155,7157,7161,7201,7036,7203,6884,6610,7018,7046,7078,7114,7131,7153,7176,7058,6898,7125,7192,7134,7217,7220,7223,7226,7232,7235,7240,7243,7340,7393,7163,7120,6852,7380,6705,7396,6956,6911,6920,6624,7318,6728,6446,261,2346,416,2378,279,1070,485,2058,5412,2026,436,223,5425,621,651,249,636,150,184,253,151,667,615,255,688,251,168,679,703,1415,250,161,1175,256,162,252,254,166,160,153,165,164,4113,242,246,220,1671,198,202,243,194,181,178,1847,139,170,188,195,173,171,237,197,260,196,238,180,200,185,174,187,175,158,240,179,233,186,224,189,183,172,206,248,156,4561,4786,1271,1287,1303,1319,1335,470,1703,1783,2042,2186,2218,2362,2523,2621,2749,405,3470,3422,3244,3454,380,584,3163,575,586,401,3631,382,917,227,3663,155,190,201,235,176])).
% 59.14/59.25 cnf(7487,plain,
% 59.14/59.25 (~P3(f19(a3,a1),a17,a1,a3)),
% 59.14/59.25 inference(scs_inference,[],[142,6674,7005,7038,7310,7327,7060,7099,7229,7321,7326,7330,7342,7347,7357,7364,7371,7385,7400,6565,7105,7202,7127,7155,7157,7161,7201,7036,7203,6884,6610,7018,7046,7078,7114,7131,7153,7176,7058,6898,7125,7192,7134,7217,7220,7223,7226,7232,7235,7240,7243,7340,7393,7163,7120,6852,7380,6705,7396,6956,6911,6920,6624,7318,6728,6446,261,2346,416,2378,279,1070,485,2058,5412,2026,436,223,5425,621,651,249,636,150,184,253,151,667,615,255,688,251,168,679,703,1415,250,161,1175,256,162,252,254,166,160,153,165,164,4113,242,246,220,1671,198,202,243,194,181,178,1847,139,170,188,195,173,171,237,197,260,196,238,180,200,185,174,187,175,158,240,179,233,186,224,189,183,172,206,248,156,4561,4786,1271,1287,1303,1319,1335,470,1703,1783,2042,2186,2218,2362,2523,2621,2749,405,3470,3422,3244,3454,380,584,3163,575,586,401,3631,382,917,227,3663,155,190,201,235,176,177])).
% 59.14/59.25 cnf(7513,plain,
% 59.14/59.25 (P8(f19(a17,x75131),a17,x75131)),
% 59.14/59.25 inference(rename_variables,[],[7411])).
% 59.14/59.25 cnf(7516,plain,
% 59.14/59.25 (P8(f19(a17,x75161),a17,x75161)),
% 59.14/59.25 inference(rename_variables,[],[7411])).
% 59.14/59.25 cnf(7519,plain,
% 59.14/59.25 (P8(f19(a17,x75191),a17,x75191)),
% 59.14/59.25 inference(rename_variables,[],[7411])).
% 59.14/59.25 cnf(7522,plain,
% 59.14/59.25 (P8(f19(a17,x75221),a17,x75221)),
% 59.14/59.25 inference(rename_variables,[],[7411])).
% 59.14/59.25 cnf(7525,plain,
% 59.14/59.25 (P8(f19(a17,x75251),a17,x75251)),
% 59.14/59.25 inference(rename_variables,[],[7411])).
% 59.14/59.25 cnf(7528,plain,
% 59.14/59.25 (P8(f19(a17,x75281),a17,x75281)),
% 59.14/59.25 inference(rename_variables,[],[7411])).
% 59.14/59.25 cnf(7531,plain,
% 59.14/59.25 (P4(x75311,x75312,x75313,x75314,x75312,x75311,x75313,x75314)),
% 59.14/59.25 inference(rename_variables,[],[7273])).
% 59.14/59.25 cnf(7534,plain,
% 59.14/59.25 (P8(f19(a3,x75341),x75341,a3)),
% 59.14/59.25 inference(rename_variables,[],[7263])).
% 59.14/59.25 cnf(7537,plain,
% 59.14/59.25 (P8(f19(a3,x75371),x75371,a3)),
% 59.14/59.25 inference(rename_variables,[],[7263])).
% 59.14/59.25 cnf(7540,plain,
% 59.14/59.25 (P8(f19(a3,x75401),x75401,a3)),
% 59.14/59.25 inference(rename_variables,[],[7263])).
% 59.14/59.25 cnf(7545,plain,
% 59.14/59.25 (P8(f19(a3,x75451),x75451,a3)),
% 59.14/59.25 inference(rename_variables,[],[7263])).
% 59.14/59.25 cnf(7548,plain,
% 59.14/59.25 (P8(f19(a3,x75481),x75481,a3)),
% 59.14/59.25 inference(rename_variables,[],[7263])).
% 59.14/59.25 cnf(7551,plain,
% 59.14/59.25 (P8(f19(a3,x75511),x75511,a3)),
% 59.14/59.25 inference(rename_variables,[],[7263])).
% 59.14/59.25 cnf(7554,plain,
% 59.14/59.25 (P8(f19(a17,x75541),a17,x75541)),
% 59.14/59.25 inference(rename_variables,[],[7411])).
% 59.14/59.25 cnf(7557,plain,
% 59.14/59.25 (P8(f19(a17,x75571),a17,x75571)),
% 59.14/59.25 inference(rename_variables,[],[7411])).
% 59.14/59.25 cnf(7576,plain,
% 59.14/59.25 (P3(x75761,f6(x75761,x75761,x75762),x75762,x75761)),
% 59.14/59.25 inference(rename_variables,[],[7375])).
% 59.14/59.25 cnf(7587,plain,
% 59.14/59.25 (P3(x75871,f6(x75871,x75871,x75872),x75872,x75871)),
% 59.14/59.25 inference(rename_variables,[],[7375])).
% 59.14/59.25 cnf(7630,plain,
% 59.14/59.25 (P8(f19(a17,x76301),a17,x76301)),
% 59.14/59.25 inference(rename_variables,[],[7411])).
% 59.14/59.25 cnf(7633,plain,
% 59.14/59.25 (P4(x76331,x76332,x76331,x76332,x76333,x76334,x76334,x76333)),
% 59.14/59.25 inference(rename_variables,[],[7253])).
% 59.14/59.25 cnf(7636,plain,
% 59.14/59.25 (P4(x76361,x76362,x76363,x76364,x76362,x76361,x76363,x76364)),
% 59.14/59.25 inference(rename_variables,[],[7273])).
% 59.14/59.25 cnf(7650,plain,
% 59.14/59.25 (P10(x76501,x76502,x76502,x76501)),
% 59.14/59.25 inference(rename_variables,[],[6705])).
% 59.14/59.25 cnf(7651,plain,
% 59.14/59.25 (P8(f19(a17,x76511),a17,x76511)),
% 59.14/59.25 inference(rename_variables,[],[7411])).
% 59.14/59.25 cnf(7660,plain,
% 59.14/59.25 (P10(x76601,x76602,x76602,x76601)),
% 59.14/59.25 inference(rename_variables,[],[6705])).
% 59.14/59.25 cnf(7664,plain,
% 59.14/59.25 (P3(x76641,x76642,x76642,x76641)),
% 59.14/59.25 inference(rename_variables,[],[7363])).
% 59.14/59.25 cnf(7667,plain,
% 59.14/59.25 (P3(x76671,x76672,x76672,x76671)),
% 59.14/59.25 inference(rename_variables,[],[7363])).
% 59.14/59.25 cnf(7672,plain,
% 59.14/59.25 (P3(x76721,x76722,x76722,x76721)),
% 59.14/59.25 inference(rename_variables,[],[7363])).
% 59.14/59.25 cnf(7676,plain,
% 59.14/59.25 (P3(x76761,x76762,x76762,x76761)),
% 59.14/59.25 inference(rename_variables,[],[7363])).
% 59.14/59.25 cnf(7679,plain,
% 59.14/59.25 (P3(x76791,x76792,x76792,x76791)),
% 59.14/59.25 inference(rename_variables,[],[7363])).
% 59.14/59.25 cnf(7686,plain,
% 59.14/59.25 (P3(x76861,x76862,x76862,x76861)),
% 59.14/59.25 inference(rename_variables,[],[7363])).
% 59.14/59.25 cnf(7689,plain,
% 59.14/59.25 (P4(x76891,x76892,x76893,x76894,x76892,x76891,x76893,x76894)),
% 59.14/59.25 inference(rename_variables,[],[7273])).
% 59.14/59.25 cnf(7692,plain,
% 59.14/59.25 (P3(x76921,x76922,x76922,x76921)),
% 59.14/59.25 inference(rename_variables,[],[7363])).
% 59.14/59.25 cnf(7695,plain,
% 59.14/59.25 (P3(x76951,x76952,x76952,x76951)),
% 59.14/59.25 inference(rename_variables,[],[7363])).
% 59.14/59.25 cnf(7698,plain,
% 59.14/59.25 (P3(x76981,x76982,x76982,x76981)),
% 59.14/59.25 inference(rename_variables,[],[7363])).
% 59.14/59.25 cnf(7704,plain,
% 59.14/59.25 (P3(x77041,x77042,x77041,x77042)),
% 59.14/59.25 inference(rename_variables,[],[7099])).
% 59.14/59.25 cnf(7709,plain,
% 59.14/59.25 (P3(x77091,x77092,x77092,x77091)),
% 59.14/59.25 inference(rename_variables,[],[7363])).
% 59.14/59.25 cnf(7714,plain,
% 59.14/59.25 (P3(x77141,x77142,x77142,x77141)),
% 59.14/59.25 inference(rename_variables,[],[7363])).
% 59.14/59.25 cnf(7717,plain,
% 59.14/59.25 (P3(x77171,x77172,x77172,x77171)),
% 59.14/59.25 inference(rename_variables,[],[7363])).
% 59.14/59.25 cnf(7720,plain,
% 59.14/59.25 (P3(x77201,x77202,x77202,x77201)),
% 59.14/59.25 inference(rename_variables,[],[7363])).
% 59.14/59.25 cnf(7733,plain,
% 59.14/59.25 (P3(x77331,x77332,x77332,x77331)),
% 59.14/59.25 inference(rename_variables,[],[7363])).
% 59.14/59.25 cnf(7738,plain,
% 59.14/59.25 (P3(x77381,x77382,x77382,x77381)),
% 59.14/59.25 inference(rename_variables,[],[7363])).
% 59.14/59.25 cnf(7759,plain,
% 59.14/59.25 ($false),
% 59.14/59.25 inference(scs_inference,[],[142,6675,7006,7253,7633,7273,7531,7636,7689,7363,7664,7667,7672,7676,7679,7686,7692,7695,7698,7709,7714,7717,7720,7733,7738,7208,7382,7293,6896,7062,7281,7287,6527,7026,7299,7301,7332,7334,7351,7366,7379,7402,7407,7419,7476,7375,7576,7587,7373,7219,6626,7370,6986,7263,7534,7537,7540,7545,7548,7551,7411,7513,7516,7519,7522,7525,7528,7554,7557,7630,7651,7095,7129,7392,7384,7482,7484,7487,7099,7704,7134,6952,7038,6852,391,6705,7650,7660,6624,6757,7114,144,597,1799,2234,2539,2701,7213,397,2042,2362,470,575,2621,2749,5412,586,382,651,223,5425,621,249,688,636,150,281,163,253,667,168,4419,184,151,615,255,703,251,679,161,1415,250,254,166,256,1175,162,252,153,160,165,164,154,242,246,182,217,155,201,202,1671,178,181,220,1847,194,190,176,170,188,198,235,152,195,237,171,196,173,259,238,260,197,180,175,185,187,200,158,240,233,179,224,186,177,192,183,189,236,172]),
% 59.14/59.25 ['proof']).
% 59.14/59.25 % SZS output end Proof
% 59.14/59.25 % Total time :58.690000s
%------------------------------------------------------------------------------