%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : GEO572+1 : TPTP v8.2.0. Released v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% Computer : n024.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:46 EDT 2024
% Result : Theorem 69.42s 69.45s
% Output : CNFRefutation 69.42s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.05/0.14 % Problem : GEO572+1 : TPTP v8.2.0. Released v7.5.0.
% 0.05/0.14 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% 0.14/0.35 % Computer : n024.cluster.edu
% 0.14/0.35 % Model : x86_64 x86_64
% 0.14/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.35 % Memory : 8042.1875MB
% 0.14/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.36 % CPULimit : 300
% 0.14/0.36 % WCLimit : 300
% 0.14/0.36 % DateTime : Fri Jun 21 06:01:39 EDT 2024
% 0.14/0.36 % CPUTime :
% 0.52/0.59 start to proof:theBenchmark
% 69.36/69.44 %-------------------------------------------
% 69.36/69.44 % File :CSE---1.7
% 69.36/69.44 % Problem :theBenchmark
% 69.36/69.44 % Transform :cnf
% 69.36/69.44 % Format :tptp:raw
% 69.36/69.44 % Command :java -jar mcs_scs.jar %d %s
% 69.36/69.44
% 69.36/69.44 % Result :Theorem 68.780000s
% 69.36/69.44 % Output :CNFRefutation 68.780000s
% 69.36/69.44 %-------------------------------------------
% 69.36/69.44 %------------------------------------------------------------------------------
% 69.36/69.44 % File : GEO572+1 : TPTP v8.2.0. Released v7.5.0.
% 69.36/69.44 % Domain : Geometry
% 69.36/69.44 % Problem : JGEX problem 34
% 69.36/69.44 % Version : [CGZ00] axioms.
% 69.36/69.44 % English :
% 69.36/69.44
% 69.36/69.44 % Refs : [CGZ00] Chou et al. (2000), A Deductive Database Approach to A
% 69.36/69.44 % : [YCG08] Ye et al. (2008), An Introduction to Java Geometry Exp
% 69.36/69.44 % : [Qua20] Quaresma (2020), Email to Geoff Sutcliffe
% 69.42/69.44 % Source : [Qua20]
% 69.42/69.44 % Names : 34.p [Qua20]
% 69.42/69.44
% 69.42/69.44 % Status : Theorem
% 69.42/69.44 % Rating : 0.36 v8.2.0, 0.33 v8.1.0, 0.39 v7.5.0
% 69.42/69.44 % Syntax : Number of formulae : 95 ( 0 unt; 0 def)
% 69.42/69.44 % Number of atoms : 290 ( 1 equ)
% 69.42/69.44 % Maximal formula atoms : 8 ( 3 avg)
% 69.42/69.44 % Number of connectives : 202 ( 7 ~; 0 |; 100 &)
% 69.42/69.44 % ( 0 <=>; 95 =>; 0 <=; 0 <~>)
% 69.42/69.44 % Maximal formula depth : 15 ( 9 avg)
% 69.42/69.44 % Maximal term depth : 1 ( 1 avg)
% 69.42/69.44 % Number of predicates : 12 ( 11 usr; 0 prp; 2-8 aty)
% 69.42/69.44 % Number of functors : 0 ( 0 usr; 0 con; --- aty)
% 69.42/69.44 % Number of variables : 529 ( 509 !; 20 ?)
% 69.42/69.44 % SPC : FOF_THM_RFO_SEQ
% 69.42/69.44
% 69.42/69.45 % Comments : Taken from JGEX [YCG08], converted by Pedro Quaresma.
% 69.42/69.45 %------------------------------------------------------------------------------
% 69.42/69.45 include('Axioms/GEO012+0.ax').
% 69.42/69.45 %------------------------------------------------------------------------------
% 69.42/69.45 fof(exemplo6GDDFULL214034,conjecture,
% 69.42/69.45 ! [A,B,C,H,O,P,NWPNT1] :
% 69.42/69.45 ( ( perp(A,B,C,H)
% 69.42/69.45 & perp(A,C,B,H)
% 69.42/69.45 & perp(B,C,A,H)
% 69.42/69.45 & perp(C,H,H,P)
% 69.42/69.45 & circle(O,H,B,C)
% 69.42/69.45 & circle(O,B,P,NWPNT1) )
% 69.42/69.45 => para(A,H,B,P) ) ).
% 69.42/69.45
% 69.42/69.45 %------------------------------------------------------------------------------
% 69.42/69.45 %-------------------------------------------
% 69.42/69.45 % Proof found
% 69.42/69.45 % SZS status Theorem for theBenchmark
% 69.42/69.45 % SZS output start Proof
% 69.42/69.45 %ClaNum:261(EqnAxiom:141)
% 69.42/69.45 %VarNum:1613(SingletonVarNum:590)
% 69.42/69.45 %MaxLitNum:5
% 69.42/69.45 %MaxfuncDepth:1
% 69.42/69.45 %SharedTerms:14
% 69.42/69.45 %goalClause: 142 143 144 145 146 147 148
% 69.42/69.45 %singleGoalClaCount:7
% 69.42/69.45 [142]P1(a1,a14,a15,a16)
% 69.42/69.45 [143]P1(a1,a15,a14,a16)
% 69.42/69.45 [144]P1(a14,a15,a1,a16)
% 69.42/69.45 [145]P1(a15,a16,a16,a17)
% 69.42/69.45 [146]P2(a18,a14,a17,a19)
% 69.42/69.45 [147]P2(a18,a16,a14,a15)
% 69.42/69.45 [148]~P3(a1,a16,a14,a17)
% 69.42/69.45 [149]~P4(x1492,x1491,x1493)+P4(x1491,x1492,x1493)
% 69.42/69.45 [150]~P4(x1501,x1503,x1502)+P4(x1501,x1502,x1503)
% 69.42/69.45 [151]~P5(x1511,x1512,x1513)+P4(x1511,x1512,x1513)
% 69.42/69.45 [152]~P5(x1521,x1523,x1522)+P5(x1521,x1522,x1523)
% 69.42/69.45 [154]~P5(x1541,x1542,x1543)+P6(x1541,x1542,x1541,x1543)
% 69.42/69.45 [158]~P3(x1581,x1582,x1581,x1583)+P4(x1581,x1582,x1583)
% 69.42/69.45 [224]~P6(x2241,x2242,x2241,x2243)+P10(x2241,x2242,x2242,x2243,x2242,x2243,x2241,x2243)
% 69.42/69.45 [161]~P3(x1613,x1614,x1611,x1612)+P3(x1611,x1612,x1613,x1614)
% 69.42/69.45 [162]~P3(x1621,x1622,x1624,x1623)+P3(x1621,x1622,x1623,x1624)
% 69.42/69.45 [163]~P1(x1633,x1634,x1631,x1632)+P1(x1631,x1632,x1633,x1634)
% 69.42/69.45 [164]~P1(x1641,x1642,x1644,x1643)+P1(x1641,x1642,x1643,x1644)
% 69.42/69.45 [165]~P6(x1653,x1654,x1651,x1652)+P6(x1651,x1652,x1653,x1654)
% 69.42/69.45 [166]~P6(x1661,x1662,x1664,x1663)+P6(x1661,x1662,x1663,x1664)
% 69.42/69.45 [167]~P7(x1672,x1671,x1673,x1674)+P7(x1671,x1672,x1673,x1674)
% 69.42/69.45 [168]~P7(x1681,x1683,x1682,x1684)+P7(x1681,x1682,x1683,x1684)
% 69.42/69.45 [169]~P7(x1691,x1692,x1694,x1693)+P7(x1691,x1692,x1693,x1694)
% 69.42/69.45 [222]~P7(x2222,x2223,x2221,x2224)+P10(x2221,x2222,x2221,x2223,x2224,x2222,x2224,x2223)
% 69.42/69.45 [185]~P2(x1854,x1851,x1852,x1853)+P1(f6(x1851,x1852,x1853,x1854),x1851,x1851,x1854)
% 69.42/69.45 [200]P6(x2001,x2002,x2003,x2004)+~P8(x2001,x2002,x2005,x2003,x2004,x2006)
% 69.42/69.45 [212]~P11(x2124,x2125,x2126,x2121,x2122,x2123)+P11(x2121,x2122,x2123,x2124,x2125,x2126)
% 69.42/69.45 [213]~P11(x2132,x2131,x2133,x2135,x2134,x2136)+P11(x2131,x2132,x2133,x2134,x2135,x2136)
% 69.42/69.45 [214]~P11(x2141,x2143,x2142,x2144,x2146,x2145)+P11(x2141,x2142,x2143,x2144,x2145,x2146)
% 69.42/69.45 [215]~P8(x2154,x2155,x2156,x2151,x2152,x2153)+P8(x2151,x2152,x2153,x2154,x2155,x2156)
% 69.42/69.45 [216]~P8(x2162,x2161,x2163,x2165,x2164,x2166)+P8(x2161,x2162,x2163,x2164,x2165,x2166)
% 69.42/69.45 [217]~P8(x2171,x2173,x2172,x2174,x2176,x2175)+P8(x2171,x2172,x2173,x2174,x2175,x2176)
% 69.42/69.45 [223]~P3(x2231,x2232,x2235,x2236)+P10(x2231,x2232,x2233,x2234,x2235,x2236,x2233,x2234)
% 69.42/69.45 [229]~P11(x2291,x2292,x2293,x2294,x2295,x2296)+P10(x2291,x2292,x2292,x2293,x2294,x2295,x2295,x2296)
% 69.42/69.45 [230]~P11(x2301,x2302,x2303,x2304,x2305,x2306)+P9(x2301,x2302,x2301,x2303,x2304,x2305,x2304,x2306)
% 69.42/69.45 [231]~P10(x2311,x2312,x2315,x2316,x2313,x2314,x2315,x2316)+P3(x2311,x2312,x2313,x2314)
% 69.42/69.45 [250]~P10(x2505,x2506,x2507,x2508,x2501,x2502,x2503,x2504)+P10(x2501,x2502,x2503,x2504,x2505,x2506,x2507,x2508)
% 69.42/69.45 [251]~P10(x2513,x2514,x2511,x2512,x2517,x2518,x2515,x2516)+P10(x2511,x2512,x2513,x2514,x2515,x2516,x2517,x2518)
% 69.42/69.45 [252]~P10(x2522,x2521,x2523,x2524,x2525,x2526,x2527,x2528)+P10(x2521,x2522,x2523,x2524,x2525,x2526,x2527,x2528)
% 69.42/69.45 [253]~P10(x2531,x2532,x2535,x2536,x2533,x2534,x2537,x2538)+P10(x2531,x2532,x2533,x2534,x2535,x2536,x2537,x2538)
% 69.42/69.45 [254]~P9(x2545,x2546,x2547,x2548,x2541,x2542,x2543,x2544)+P9(x2541,x2542,x2543,x2544,x2545,x2546,x2547,x2548)
% 69.42/69.45 [255]~P9(x2553,x2554,x2551,x2552,x2557,x2558,x2555,x2556)+P9(x2551,x2552,x2553,x2554,x2555,x2556,x2557,x2558)
% 69.42/69.45 [256]~P9(x2562,x2561,x2563,x2564,x2565,x2566,x2567,x2568)+P9(x2561,x2562,x2563,x2564,x2565,x2566,x2567,x2568)
% 69.42/69.45 [257]~P9(x2571,x2572,x2575,x2576,x2573,x2574,x2577,x2578)+P9(x2571,x2572,x2573,x2574,x2575,x2576,x2577,x2578)
% 69.42/69.45 [159]~P4(x1591,x1592,x1593)+~P6(x1591,x1592,x1591,x1593)+P5(x1591,x1592,x1593)
% 69.42/69.45 [233]P6(x2331,x2332,x2331,x2333)+~P10(x2331,x2332,x2332,x2333,x2332,x2333,x2331,x2333)+P4(x2331,x2332,x2333)
% 69.42/69.45 [174]~P1(x1741,x1742,x1742,x1743)+~P6(x1742,x1741,x1742,x1743)+P4(x1741,x1742,f2(x1741,x1743,x1742))
% 69.42/69.45 [186]~P1(x1862,x1861,x1861,x1863)+~P6(x1861,x1862,x1861,x1863)+P6(x1861,x1862,x1861,f2(x1862,x1863,x1861))
% 69.42/69.45 [153]~P4(x1533,x1534,x1531)+P4(x1531,x1532,x1533)+~P4(x1533,x1534,x1532)
% 69.42/69.45 [170]~P2(x1704,x1701,x1702,x1703)+P1(x1701,x1702,x1702,x1703)+~P4(x1704,x1701,x1703)
% 69.42/69.45 [171]~P1(x1711,x1714,x1712,x1713)+P6(x1711,x1712,x1711,x1713)+~P5(x1714,x1712,x1713)
% 69.42/69.45 [172]~P1(x1721,x1723,x1723,x1724)+P6(x1721,x1722,x1723,x1722)+~P5(x1722,x1721,x1724)
% 69.42/69.45 [179]~P6(x1791,x1794,x1792,x1794)+~P6(x1791,x1793,x1792,x1793)+P1(x1791,x1792,x1793,x1794)
% 69.42/69.45 [182]~P6(x1821,x1822,x1821,x1824)+~P6(x1821,x1822,x1821,x1823)+P2(x1821,x1822,x1823,x1824)
% 69.42/69.45 [228]~P3(x2281,x2284,x2283,x2282)+~P7(x2281,x2284,x2283,x2282)+P10(x2281,x2282,x2283,x2282,x2283,x2282,x2283,x2284)
% 69.42/69.45 [232]~P10(x2321,x2323,x2321,x2324,x2322,x2323,x2322,x2324)+P4(x2321,x2322,x2323)+P7(x2323,x2324,x2321,x2322)
% 69.42/69.45 [234]~P4(x2343,x2344,x2342)+~P10(x2343,x2341,x2343,x2342,x2344,x2341,x2344,x2342)+P7(x2341,x2342,x2343,x2344)
% 69.42/69.45 [236]P1(x2361,x2362,x2363,x2364)+~P10(x2361,x2362,x2363,x2364,x2363,x2364,x2361,x2362)+P3(x2361,x2362,x2363,x2364)
% 69.42/69.45 [175]~P1(x1751,x1754,x1752,x1753)+~P1(x1752,x1754,x1751,x1753)+P4(f3(x1751,x1752,x1753),x1753,x1752)
% 69.42/69.45 [176]~P1(x1761,x1764,x1762,x1763)+~P1(x1762,x1764,x1761,x1763)+P4(f4(x1761,x1762,x1763),x1763,x1761)
% 69.42/69.45 [187]~P1(x1871,x1874,x1872,x1873)+~P1(x1872,x1874,x1871,x1873)+P1(x1871,f3(x1871,x1872,x1873),x1873,x1872)
% 69.42/69.45 [188]~P1(x1881,x1884,x1882,x1883)+~P1(x1882,x1884,x1881,x1883)+P1(x1881,f4(x1882,x1881,x1883),x1883,x1882)
% 69.42/69.45 [189]~P1(x1891,x1893,x1893,x1892)+~P7(x1891,x1892,x1893,x1894)+P2(f7(x1891,x1892,x1893),x1891,x1892,x1893)
% 69.42/69.45 [191]~P1(x1913,x1914,x1912,x1911)+~P6(x1913,x1912,x1913,x1911)+P4(x1911,x1912,f21(x1912,x1911,x1913,x1914))
% 69.42/69.45 [192]~P1(x1923,x1924,x1921,x1922)+~P6(x1923,x1921,x1923,x1922)+P4(f21(x1921,x1922,x1923,x1924),x1923,x1924)
% 69.42/69.45 [243]~P6(x2433,x2432,x2433,x2431)+~P10(x2432,x2433,x2433,x2434,x2433,x2434,x2433,x2431)+P4(x2431,x2432,f22(x2432,x2431,x2433,x2434))
% 69.42/69.45 [244]~P1(x2443,x2444,x2442,x2441)+~P10(x2442,x2443,x2443,x2444,x2443,x2444,x2443,x2441)+P4(x2441,x2442,f23(x2442,x2441,x2443,x2444))
% 69.42/69.45 [245]~P1(x2453,x2452,x2452,x2451)+~P10(x2454,x2453,x2452,x2453,x2452,x2453,x2451,x2453)+P4(f13(x2451,x2452,x2453,x2454),x2453,x2454)
% 69.42/69.45 [246]~P1(x2463,x2462,x2462,x2461)+~P10(x2464,x2463,x2462,x2463,x2462,x2463,x2461,x2463)+P4(f13(x2461,x2462,x2463,x2464),x2461,x2462)
% 69.42/69.45 [247]~P6(x2473,x2471,x2473,x2472)+~P10(x2471,x2473,x2473,x2474,x2473,x2474,x2473,x2472)+P4(f22(x2471,x2472,x2473,x2474),x2473,x2474)
% 69.42/69.45 [248]~P1(x2483,x2484,x2481,x2482)+~P10(x2481,x2483,x2483,x2484,x2483,x2484,x2483,x2482)+P4(f23(x2481,x2482,x2483,x2484),x2483,x2484)
% 69.42/69.45 [155]~P5(x1555,x1551,x1553)+P3(x1551,x1552,x1553,x1554)+~P5(x1555,x1552,x1554)
% 69.42/69.45 [156]~P5(x1561,x1565,x1563)+P3(x1561,x1562,x1563,x1564)+~P5(x1562,x1565,x1564)
% 69.42/69.45 [183]~P7(x1835,x1831,x1832,x1833)+P7(x1831,x1832,x1833,x1834)+~P7(x1835,x1831,x1832,x1834)
% 69.42/69.45 [225]~P5(x2255,x2252,x2253)+~P2(x2254,x2251,x2252,x2253)+P10(x2251,x2252,x2251,x2253,x2254,x2252,x2254,x2255)
% 69.42/69.45 [227]~P2(x2275,x2271,x2273,x2274)+P10(x2271,x2272,x2271,x2273,x2274,x2271,x2274,x2273)+~P1(x2275,x2271,x2271,x2272)
% 69.42/69.45 [240]~P10(x2402,x2403,x2402,x2404,x2405,x2402,x2405,x2404)+P1(x2401,x2402,x2402,x2403)+~P2(x2401,x2402,x2404,x2405)
% 69.42/69.45 [195]~P4(x1952,x1954,x1955)+~P1(x1951,x1953,x1953,x1952)+P4(f11(x1951,x1952,x1953,x1954,x1955),x1954,x1955)
% 69.42/69.45 [196]~P4(x1962,x1964,x1965)+~P1(x1961,x1963,x1963,x1962)+P1(f11(x1961,x1962,x1963,x1964,x1965),x1961,x1964,x1965)
% 69.42/69.45 [197]~P1(x1973,x1974,x1974,x1971)+~P6(x1971,x1972,x1971,x1975)+P6(x1971,x1972,x1971,f26(x1973,x1974,x1972,x1975,x1971))
% 69.42/69.45 [198]~P1(x1983,x1981,x1981,x1985)+~P6(x1985,x1982,x1985,x1984)+P6(x1981,x1982,x1981,f26(x1983,x1981,x1982,x1984,x1985))
% 69.42/69.45 [199]~P1(x1991,x1992,x1992,x1995)+~P6(x1995,x1993,x1995,x1994)+P3(f26(x1991,x1992,x1993,x1994,x1995),x1993,x1991,x1992)
% 69.42/69.45 [242]~P10(x2421,x2423,x2422,x2423,x2421,x2424,x2422,x2425)+P4(x2421,x2422,x2423)+P7(x2424,x2422,x2423,f25(x2421,x2422,x2423,x2424))
% 69.42/69.45 [258]~P10(x2581,x2583,x2582,x2583,x2581,x2584,x2582,x2585)+P4(x2581,x2582,x2583)+P10(x2581,x2583,x2582,x2583,x2581,f25(x2581,x2582,x2583,x2584),x2582,f25(x2581,x2582,x2583,x2584))
% 69.42/69.45 [177]~P3(x1771,x1772,x1775,x1776)+P3(x1771,x1772,x1773,x1774)+~P3(x1775,x1776,x1773,x1774)
% 69.42/69.45 [178]~P1(x1781,x1782,x1785,x1786)+P3(x1781,x1782,x1783,x1784)+~P1(x1785,x1786,x1783,x1784)
% 69.42/69.45 [180]~P1(x1805,x1806,x1803,x1804)+P1(x1801,x1802,x1803,x1804)+~P3(x1801,x1802,x1805,x1806)
% 69.42/69.45 [181]~P6(x1811,x1812,x1815,x1816)+P6(x1811,x1812,x1813,x1814)+~P6(x1815,x1816,x1813,x1814)
% 69.42/69.45 [218]~P6(x2181,x2182,x2184,x2185)+~P11(x2181,x2182,x2183,x2184,x2185,x2186)+P8(x2181,x2182,x2183,x2184,x2185,x2186)
% 69.42/69.45 [221]~P5(x2214,x2215,x2216)+~P5(x2211,x2212,x2213)+P9(x2211,x2212,x2212,x2213,x2214,x2215,x2215,x2216)
% 69.42/69.45 [201]~P5(x2016,x2013,x2014)+~P5(x2015,x2011,x2012)+P5(f24(x2011,x2012,x2013,x2014,x2015,x2016),x2011,x2014)
% 69.42/69.45 [202]~P5(x2026,x2023,x2024)+~P5(x2025,x2021,x2022)+P3(f24(x2021,x2022,x2023,x2024,x2025,x2026),x2026,x2021,x2023)
% 69.42/69.45 [203]~P5(x2036,x2033,x2034)+~P5(x2035,x2031,x2032)+P3(f24(x2031,x2032,x2033,x2034,x2035,x2036),x2035,x2032,x2034)
% 69.42/69.45 [238]~P10(x2381,x2382,x2383,x2384,x2385,x2386,x2387,x2388)+P3(x2381,x2382,x2383,x2384)+~P3(x2385,x2386,x2387,x2388)
% 69.42/69.45 [239]~P10(x2391,x2392,x2393,x2394,x2395,x2396,x2397,x2398)+P1(x2391,x2392,x2393,x2394)+~P1(x2395,x2396,x2397,x2398)
% 69.42/69.45 [241]~P9(x2411,x2412,x2413,x2414,x2415,x2416,x2417,x2418)+P6(x2411,x2412,x2413,x2414)+~P6(x2415,x2416,x2417,x2418)
% 69.42/69.45 [219]~P11(x2191,x2192,x2193,x2197,x2198,x2199)+P11(x2191,x2192,x2193,x2194,x2195,x2196)+~P11(x2197,x2198,x2199,x2194,x2195,x2196)
% 69.42/69.45 [220]~P8(x2201,x2202,x2203,x2207,x2208,x2209)+P8(x2201,x2202,x2203,x2204,x2205,x2206)+~P8(x2207,x2208,x2209,x2204,x2205,x2206)
% 69.42/69.45 [260]~P10(x2601,x2602,x2603,x2604,x2609,x26010,x26011,x26012)+P10(x2601,x2602,x2603,x2604,x2605,x2606,x2607,x2608)+~P10(x2609,x26010,x26011,x26012,x2605,x2606,x2607,x2608)
% 69.42/69.45 [261]~P9(x2611,x2612,x2613,x2614,x2619,x26110,x26111,x26112)+P9(x2611,x2612,x2613,x2614,x2615,x2616,x2617,x2618)+~P9(x2619,x26110,x26111,x26112,x2615,x2616,x2617,x2618)
% 69.42/69.45 [193]~P6(x1932,x1931,x1934,x1931)+~P7(x1932,x1934,x1931,x1933)+P1(x1931,x1932,x1932,x1933)+~P6(x1932,x1933,x1934,x1933)
% 69.42/69.45 [160]~P4(x1601,x1602,x1603)+~P3(x1604,x1601,x1605,x1603)+P5(x1601,x1602,x1603)+~P5(x1604,x1602,x1605)
% 69.42/69.45 [173]~P3(x1734,x1733,x1735,x1732)+~P3(x1734,x1732,x1735,x1733)+P5(x1731,x1732,x1733)+~P5(x1731,x1734,x1735)
% 69.42/69.45 [194]~P6(x1945,x1941,x1945,x1943)+~P6(x1945,x1941,x1945,x1942)+P7(x1941,x1942,x1943,x1944)+~P6(x1945,x1941,x1945,x1944)
% 69.42/69.45 [226]~P4(x2261,x2264,x2265)+~P4(x2261,x2262,x2263)+~P3(x2262,x2264,x2263,x2265)+P9(x2261,x2262,x2262,x2263,x2261,x2264,x2264,x2265)
% 69.42/69.45 [237]~P4(x2371,x2372,x2373)+~P10(x2375,x2372,x2375,x2373,x2374,x2372,x2374,x2371)+P5(x2371,x2372,x2373)+~P2(x2374,x2375,x2372,x2373)
% 69.42/69.45 [184]~P1(x1843,x1841,x1843,x1845)+~P1(x1841,x1842,x1841,x1843)+~P5(x1844,x1842,x1845)+P5(f5(x1841,x1842,x1843),x1841,x1843)
% 69.42/69.45 [190]~P7(x1901,x1902,x1903,x1905)+~P3(x1901,x1902,x1903,x1905)+~P5(x1904,x1901,x1902)+P2(f8(x1901,x1902,x1903),x1901,x1902,x1903)
% 69.42/69.45 [259]~P10(x2591,x2593,x2592,x2593,x2594,x2596,x2595,x2596)+~P10(x2591,x2592,x2592,x2593,x2594,x2595,x2595,x2596)+P4(x2591,x2592,x2593)+P11(x2591,x2592,x2593,x2594,x2595,x2596)
% 69.42/69.45 [249]~P7(x2491,x2492,x2495,x2494)+~P7(x2491,x2492,x2495,x2493)+~P10(x2495,x2491,x2495,x2492,x2496,x2493,x2496,x2494)+P6(x2491,x2492,x2493,x2494)+~P7(x2491,x2492,x2495,x2496)
% 69.42/69.45 [204]~P4(x2042,x2043,x2044)+~P4(x2041,x2044,x2046)+~P4(x2041,x2043,x2045)+~P3(x2043,x2044,x2045,x2046)+P4(x2041,x2042,f12(x2043,x2044,x2045,x2046,x2041,x2042))
% 69.42/69.45 [205]~P4(x2056,x2051,x2052)+~P4(x2055,x2052,x2054)+~P4(x2055,x2051,x2053)+~P3(x2051,x2052,x2053,x2054)+P4(f12(x2051,x2052,x2053,x2054,x2055,x2056),x2053,x2054)
% 69.42/69.45 [206]~P4(x2063,x2064,x2065)+~P5(x2066,x2061,x2062)+~P3(x2061,x2063,x2065,x2066)+~P3(x2061,x2063,x2062,x2064)+P4(f27(x2061,x2062,x2063,x2064,x2065,x2066),x2066,x2065)
% 69.42/69.45 [207]~P4(x2073,x2074,x2075)+~P5(x2076,x2071,x2072)+~P3(x2071,x2073,x2075,x2076)+~P3(x2071,x2073,x2072,x2074)+P4(f27(x2071,x2072,x2073,x2074,x2075,x2076),x2071,x2074)
% 69.42/69.45 [208]~P6(x2082,x2083,x2082,x2084)+~P6(x2081,x2083,x2081,x2086)+~P2(x2081,x2083,x2084,x2085)+E(x2081,x2082)+P4(f9(x2083,x2084,x2085,x2086,x2081,x2082),x2083,x2085)
% 69.42/69.46 [209]~P6(x2092,x2093,x2092,x2094)+~P6(x2091,x2093,x2091,x2096)+~P2(x2091,x2093,x2094,x2095)+E(x2091,x2092)+P4(f10(x2093,x2094,x2095,x2096,x2091,x2092),x2094,x2096)
% 69.42/69.46 [210]~P6(x2102,x2103,x2102,x2104)+~P6(x2101,x2103,x2101,x2106)+~P2(x2101,x2103,x2104,x2105)+E(x2101,x2102)+P6(f9(x2103,x2104,x2105,x2106,x2101,x2102),x2102,x2102,x2103)
% 69.42/69.46 [211]~P6(x2112,x2113,x2112,x2114)+~P6(x2111,x2113,x2111,x2116)+~P2(x2111,x2113,x2114,x2115)+E(x2111,x2112)+P6(f10(x2113,x2114,x2115,x2116,x2111,x2112),x2112,x2112,x2113)
% 69.42/69.46 [157]~P4(x1573,x1571,x1574)+~P4(x1575,x1571,x1574)+~P5(x1576,x1575,x1573)+~P5(x1577,x1571,x1574)+P5(f20(x1571,x1572),x1571,x1572)
% 69.42/69.46 %EqnAxiom
% 69.42/69.46 [1]E(x11,x11)
% 69.42/69.46 [2]E(x22,x21)+~E(x21,x22)
% 69.42/69.46 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 69.42/69.46 [4]~E(x41,x42)+E(f20(x41,x43),f20(x42,x43))
% 69.42/69.46 [5]~E(x51,x52)+E(f20(x53,x51),f20(x53,x52))
% 69.42/69.46 [6]~E(x61,x62)+E(f2(x61,x63,x64),f2(x62,x63,x64))
% 69.42/69.46 [7]~E(x71,x72)+E(f2(x73,x71,x74),f2(x73,x72,x74))
% 69.42/69.46 [8]~E(x81,x82)+E(f2(x83,x84,x81),f2(x83,x84,x82))
% 69.42/69.46 [9]~E(x91,x92)+E(f3(x91,x93,x94),f3(x92,x93,x94))
% 69.42/69.46 [10]~E(x101,x102)+E(f3(x103,x101,x104),f3(x103,x102,x104))
% 69.42/69.46 [11]~E(x111,x112)+E(f3(x113,x114,x111),f3(x113,x114,x112))
% 69.42/69.46 [12]~E(x121,x122)+E(f4(x121,x123,x124),f4(x122,x123,x124))
% 69.42/69.46 [13]~E(x131,x132)+E(f4(x133,x131,x134),f4(x133,x132,x134))
% 69.42/69.46 [14]~E(x141,x142)+E(f4(x143,x144,x141),f4(x143,x144,x142))
% 69.42/69.46 [15]~E(x151,x152)+E(f5(x151,x153,x154),f5(x152,x153,x154))
% 69.42/69.46 [16]~E(x161,x162)+E(f5(x163,x161,x164),f5(x163,x162,x164))
% 69.42/69.46 [17]~E(x171,x172)+E(f5(x173,x174,x171),f5(x173,x174,x172))
% 69.42/69.46 [18]~E(x181,x182)+E(f6(x181,x183,x184,x185),f6(x182,x183,x184,x185))
% 69.42/69.46 [19]~E(x191,x192)+E(f6(x193,x191,x194,x195),f6(x193,x192,x194,x195))
% 69.42/69.46 [20]~E(x201,x202)+E(f6(x203,x204,x201,x205),f6(x203,x204,x202,x205))
% 69.42/69.46 [21]~E(x211,x212)+E(f6(x213,x214,x215,x211),f6(x213,x214,x215,x212))
% 69.42/69.46 [22]~E(x221,x222)+E(f25(x221,x223,x224,x225),f25(x222,x223,x224,x225))
% 69.42/69.46 [23]~E(x231,x232)+E(f25(x233,x231,x234,x235),f25(x233,x232,x234,x235))
% 69.42/69.46 [24]~E(x241,x242)+E(f25(x243,x244,x241,x245),f25(x243,x244,x242,x245))
% 69.42/69.46 [25]~E(x251,x252)+E(f25(x253,x254,x255,x251),f25(x253,x254,x255,x252))
% 69.42/69.46 [26]~E(x261,x262)+E(f22(x261,x263,x264,x265),f22(x262,x263,x264,x265))
% 69.42/69.46 [27]~E(x271,x272)+E(f22(x273,x271,x274,x275),f22(x273,x272,x274,x275))
% 69.42/69.46 [28]~E(x281,x282)+E(f22(x283,x284,x281,x285),f22(x283,x284,x282,x285))
% 69.42/69.46 [29]~E(x291,x292)+E(f22(x293,x294,x295,x291),f22(x293,x294,x295,x292))
% 69.42/69.46 [30]~E(x301,x302)+E(f23(x301,x303,x304,x305),f23(x302,x303,x304,x305))
% 69.42/69.46 [31]~E(x311,x312)+E(f23(x313,x311,x314,x315),f23(x313,x312,x314,x315))
% 69.42/69.46 [32]~E(x321,x322)+E(f23(x323,x324,x321,x325),f23(x323,x324,x322,x325))
% 69.42/69.46 [33]~E(x331,x332)+E(f23(x333,x334,x335,x331),f23(x333,x334,x335,x332))
% 69.42/69.46 [34]~E(x341,x342)+E(f7(x341,x343,x344),f7(x342,x343,x344))
% 69.42/69.46 [35]~E(x351,x352)+E(f7(x353,x351,x354),f7(x353,x352,x354))
% 69.42/69.46 [36]~E(x361,x362)+E(f7(x363,x364,x361),f7(x363,x364,x362))
% 69.42/69.46 [37]~E(x371,x372)+E(f8(x371,x373,x374),f8(x372,x373,x374))
% 69.42/69.46 [38]~E(x381,x382)+E(f8(x383,x381,x384),f8(x383,x382,x384))
% 69.42/69.46 [39]~E(x391,x392)+E(f8(x393,x394,x391),f8(x393,x394,x392))
% 69.42/69.46 [40]~E(x401,x402)+E(f21(x401,x403,x404,x405),f21(x402,x403,x404,x405))
% 69.42/69.46 [41]~E(x411,x412)+E(f21(x413,x411,x414,x415),f21(x413,x412,x414,x415))
% 69.42/69.46 [42]~E(x421,x422)+E(f21(x423,x424,x421,x425),f21(x423,x424,x422,x425))
% 69.42/69.46 [43]~E(x431,x432)+E(f21(x433,x434,x435,x431),f21(x433,x434,x435,x432))
% 69.42/69.46 [44]~E(x441,x442)+E(f13(x441,x443,x444,x445),f13(x442,x443,x444,x445))
% 69.42/69.46 [45]~E(x451,x452)+E(f13(x453,x451,x454,x455),f13(x453,x452,x454,x455))
% 69.42/69.46 [46]~E(x461,x462)+E(f13(x463,x464,x461,x465),f13(x463,x464,x462,x465))
% 69.42/69.46 [47]~E(x471,x472)+E(f13(x473,x474,x475,x471),f13(x473,x474,x475,x472))
% 69.42/69.46 [48]~E(x481,x482)+E(f11(x481,x483,x484,x485,x486),f11(x482,x483,x484,x485,x486))
% 69.42/69.46 [49]~E(x491,x492)+E(f11(x493,x491,x494,x495,x496),f11(x493,x492,x494,x495,x496))
% 69.42/69.46 [50]~E(x501,x502)+E(f11(x503,x504,x501,x505,x506),f11(x503,x504,x502,x505,x506))
% 69.42/69.46 [51]~E(x511,x512)+E(f11(x513,x514,x515,x511,x516),f11(x513,x514,x515,x512,x516))
% 69.42/69.46 [52]~E(x521,x522)+E(f11(x523,x524,x525,x526,x521),f11(x523,x524,x525,x526,x522))
% 69.42/69.46 [53]~E(x531,x532)+E(f10(x531,x533,x534,x535,x536,x537),f10(x532,x533,x534,x535,x536,x537))
% 69.42/69.46 [54]~E(x541,x542)+E(f10(x543,x541,x544,x545,x546,x547),f10(x543,x542,x544,x545,x546,x547))
% 69.42/69.46 [55]~E(x551,x552)+E(f10(x553,x554,x551,x555,x556,x557),f10(x553,x554,x552,x555,x556,x557))
% 69.42/69.46 [56]~E(x561,x562)+E(f10(x563,x564,x565,x561,x566,x567),f10(x563,x564,x565,x562,x566,x567))
% 69.42/69.46 [57]~E(x571,x572)+E(f10(x573,x574,x575,x576,x571,x577),f10(x573,x574,x575,x576,x572,x577))
% 69.42/69.46 [58]~E(x581,x582)+E(f10(x583,x584,x585,x586,x587,x581),f10(x583,x584,x585,x586,x587,x582))
% 69.42/69.46 [59]~E(x591,x592)+E(f26(x591,x593,x594,x595,x596),f26(x592,x593,x594,x595,x596))
% 69.42/69.46 [60]~E(x601,x602)+E(f26(x603,x601,x604,x605,x606),f26(x603,x602,x604,x605,x606))
% 69.42/69.46 [61]~E(x611,x612)+E(f26(x613,x614,x611,x615,x616),f26(x613,x614,x612,x615,x616))
% 69.42/69.46 [62]~E(x621,x622)+E(f26(x623,x624,x625,x621,x626),f26(x623,x624,x625,x622,x626))
% 69.42/69.46 [63]~E(x631,x632)+E(f26(x633,x634,x635,x636,x631),f26(x633,x634,x635,x636,x632))
% 69.42/69.46 [64]~E(x641,x642)+E(f9(x641,x643,x644,x645,x646,x647),f9(x642,x643,x644,x645,x646,x647))
% 69.42/69.46 [65]~E(x651,x652)+E(f9(x653,x651,x654,x655,x656,x657),f9(x653,x652,x654,x655,x656,x657))
% 69.42/69.46 [66]~E(x661,x662)+E(f9(x663,x664,x661,x665,x666,x667),f9(x663,x664,x662,x665,x666,x667))
% 69.42/69.46 [67]~E(x671,x672)+E(f9(x673,x674,x675,x671,x676,x677),f9(x673,x674,x675,x672,x676,x677))
% 69.42/69.46 [68]~E(x681,x682)+E(f9(x683,x684,x685,x686,x681,x687),f9(x683,x684,x685,x686,x682,x687))
% 69.42/69.46 [69]~E(x691,x692)+E(f9(x693,x694,x695,x696,x697,x691),f9(x693,x694,x695,x696,x697,x692))
% 69.42/69.46 [70]~E(x701,x702)+E(f27(x701,x703,x704,x705,x706,x707),f27(x702,x703,x704,x705,x706,x707))
% 69.42/69.46 [71]~E(x711,x712)+E(f27(x713,x711,x714,x715,x716,x717),f27(x713,x712,x714,x715,x716,x717))
% 69.42/69.46 [72]~E(x721,x722)+E(f27(x723,x724,x721,x725,x726,x727),f27(x723,x724,x722,x725,x726,x727))
% 69.42/69.46 [73]~E(x731,x732)+E(f27(x733,x734,x735,x731,x736,x737),f27(x733,x734,x735,x732,x736,x737))
% 69.42/69.46 [74]~E(x741,x742)+E(f27(x743,x744,x745,x746,x741,x747),f27(x743,x744,x745,x746,x742,x747))
% 69.42/69.46 [75]~E(x751,x752)+E(f27(x753,x754,x755,x756,x757,x751),f27(x753,x754,x755,x756,x757,x752))
% 69.42/69.46 [76]~E(x761,x762)+E(f24(x761,x763,x764,x765,x766,x767),f24(x762,x763,x764,x765,x766,x767))
% 69.42/69.46 [77]~E(x771,x772)+E(f24(x773,x771,x774,x775,x776,x777),f24(x773,x772,x774,x775,x776,x777))
% 69.42/69.46 [78]~E(x781,x782)+E(f24(x783,x784,x781,x785,x786,x787),f24(x783,x784,x782,x785,x786,x787))
% 69.42/69.46 [79]~E(x791,x792)+E(f24(x793,x794,x795,x791,x796,x797),f24(x793,x794,x795,x792,x796,x797))
% 69.42/69.46 [80]~E(x801,x802)+E(f24(x803,x804,x805,x806,x801,x807),f24(x803,x804,x805,x806,x802,x807))
% 69.42/69.46 [81]~E(x811,x812)+E(f24(x813,x814,x815,x816,x817,x811),f24(x813,x814,x815,x816,x817,x812))
% 69.42/69.46 [82]~E(x821,x822)+E(f12(x821,x823,x824,x825,x826,x827),f12(x822,x823,x824,x825,x826,x827))
% 69.42/69.46 [83]~E(x831,x832)+E(f12(x833,x831,x834,x835,x836,x837),f12(x833,x832,x834,x835,x836,x837))
% 69.42/69.46 [84]~E(x841,x842)+E(f12(x843,x844,x841,x845,x846,x847),f12(x843,x844,x842,x845,x846,x847))
% 69.42/69.46 [85]~E(x851,x852)+E(f12(x853,x854,x855,x851,x856,x857),f12(x853,x854,x855,x852,x856,x857))
% 69.42/69.46 [86]~E(x861,x862)+E(f12(x863,x864,x865,x866,x861,x867),f12(x863,x864,x865,x866,x862,x867))
% 69.42/69.46 [87]~E(x871,x872)+E(f12(x873,x874,x875,x876,x877,x871),f12(x873,x874,x875,x876,x877,x872))
% 69.42/69.46 [88]P1(x882,x883,x884,x885)+~E(x881,x882)+~P1(x881,x883,x884,x885)
% 69.42/69.46 [89]P1(x893,x892,x894,x895)+~E(x891,x892)+~P1(x893,x891,x894,x895)
% 69.42/69.46 [90]P1(x903,x904,x902,x905)+~E(x901,x902)+~P1(x903,x904,x901,x905)
% 69.42/69.46 [91]P1(x913,x914,x915,x912)+~E(x911,x912)+~P1(x913,x914,x915,x911)
% 69.42/69.46 [92]P9(x922,x923,x924,x925,x926,x927,x928,x929)+~E(x921,x922)+~P9(x921,x923,x924,x925,x926,x927,x928,x929)
% 69.42/69.46 [93]P9(x933,x932,x934,x935,x936,x937,x938,x939)+~E(x931,x932)+~P9(x933,x931,x934,x935,x936,x937,x938,x939)
% 69.42/69.46 [94]P9(x943,x944,x942,x945,x946,x947,x948,x949)+~E(x941,x942)+~P9(x943,x944,x941,x945,x946,x947,x948,x949)
% 69.42/69.46 [95]P9(x953,x954,x955,x952,x956,x957,x958,x959)+~E(x951,x952)+~P9(x953,x954,x955,x951,x956,x957,x958,x959)
% 69.42/69.46 [96]P9(x963,x964,x965,x966,x962,x967,x968,x969)+~E(x961,x962)+~P9(x963,x964,x965,x966,x961,x967,x968,x969)
% 69.42/69.46 [97]P9(x973,x974,x975,x976,x977,x972,x978,x979)+~E(x971,x972)+~P9(x973,x974,x975,x976,x977,x971,x978,x979)
% 69.42/69.46 [98]P9(x983,x984,x985,x986,x987,x988,x982,x989)+~E(x981,x982)+~P9(x983,x984,x985,x986,x987,x988,x981,x989)
% 69.42/69.46 [99]P9(x993,x994,x995,x996,x997,x998,x999,x992)+~E(x991,x992)+~P9(x993,x994,x995,x996,x997,x998,x999,x991)
% 69.42/69.46 [100]P6(x1002,x1003,x1004,x1005)+~E(x1001,x1002)+~P6(x1001,x1003,x1004,x1005)
% 69.42/69.46 [101]P6(x1013,x1012,x1014,x1015)+~E(x1011,x1012)+~P6(x1013,x1011,x1014,x1015)
% 69.42/69.46 [102]P6(x1023,x1024,x1022,x1025)+~E(x1021,x1022)+~P6(x1023,x1024,x1021,x1025)
% 69.42/69.46 [103]P6(x1033,x1034,x1035,x1032)+~E(x1031,x1032)+~P6(x1033,x1034,x1035,x1031)
% 69.42/69.46 [104]P4(x1042,x1043,x1044)+~E(x1041,x1042)+~P4(x1041,x1043,x1044)
% 69.42/69.46 [105]P4(x1053,x1052,x1054)+~E(x1051,x1052)+~P4(x1053,x1051,x1054)
% 69.42/69.46 [106]P4(x1063,x1064,x1062)+~E(x1061,x1062)+~P4(x1063,x1064,x1061)
% 69.42/69.46 [107]P2(x1072,x1073,x1074,x1075)+~E(x1071,x1072)+~P2(x1071,x1073,x1074,x1075)
% 69.42/69.46 [108]P2(x1083,x1082,x1084,x1085)+~E(x1081,x1082)+~P2(x1083,x1081,x1084,x1085)
% 69.42/69.46 [109]P2(x1093,x1094,x1092,x1095)+~E(x1091,x1092)+~P2(x1093,x1094,x1091,x1095)
% 69.42/69.46 [110]P2(x1103,x1104,x1105,x1102)+~E(x1101,x1102)+~P2(x1103,x1104,x1105,x1101)
% 69.42/69.46 [111]P3(x1112,x1113,x1114,x1115)+~E(x1111,x1112)+~P3(x1111,x1113,x1114,x1115)
% 69.42/69.46 [112]P3(x1123,x1122,x1124,x1125)+~E(x1121,x1122)+~P3(x1123,x1121,x1124,x1125)
% 69.42/69.46 [113]P3(x1133,x1134,x1132,x1135)+~E(x1131,x1132)+~P3(x1133,x1134,x1131,x1135)
% 69.42/69.46 [114]P3(x1143,x1144,x1145,x1142)+~E(x1141,x1142)+~P3(x1143,x1144,x1145,x1141)
% 69.42/69.46 [115]P5(x1152,x1153,x1154)+~E(x1151,x1152)+~P5(x1151,x1153,x1154)
% 69.42/69.46 [116]P5(x1163,x1162,x1164)+~E(x1161,x1162)+~P5(x1163,x1161,x1164)
% 69.42/69.46 [117]P5(x1173,x1174,x1172)+~E(x1171,x1172)+~P5(x1173,x1174,x1171)
% 69.42/69.46 [118]P7(x1182,x1183,x1184,x1185)+~E(x1181,x1182)+~P7(x1181,x1183,x1184,x1185)
% 69.42/69.46 [119]P7(x1193,x1192,x1194,x1195)+~E(x1191,x1192)+~P7(x1193,x1191,x1194,x1195)
% 69.42/69.46 [120]P7(x1203,x1204,x1202,x1205)+~E(x1201,x1202)+~P7(x1203,x1204,x1201,x1205)
% 69.42/69.46 [121]P7(x1213,x1214,x1215,x1212)+~E(x1211,x1212)+~P7(x1213,x1214,x1215,x1211)
% 69.42/69.46 [122]P10(x1222,x1223,x1224,x1225,x1226,x1227,x1228,x1229)+~E(x1221,x1222)+~P10(x1221,x1223,x1224,x1225,x1226,x1227,x1228,x1229)
% 69.42/69.46 [123]P10(x1233,x1232,x1234,x1235,x1236,x1237,x1238,x1239)+~E(x1231,x1232)+~P10(x1233,x1231,x1234,x1235,x1236,x1237,x1238,x1239)
% 69.42/69.46 [124]P10(x1243,x1244,x1242,x1245,x1246,x1247,x1248,x1249)+~E(x1241,x1242)+~P10(x1243,x1244,x1241,x1245,x1246,x1247,x1248,x1249)
% 69.42/69.46 [125]P10(x1253,x1254,x1255,x1252,x1256,x1257,x1258,x1259)+~E(x1251,x1252)+~P10(x1253,x1254,x1255,x1251,x1256,x1257,x1258,x1259)
% 69.42/69.46 [126]P10(x1263,x1264,x1265,x1266,x1262,x1267,x1268,x1269)+~E(x1261,x1262)+~P10(x1263,x1264,x1265,x1266,x1261,x1267,x1268,x1269)
% 69.42/69.46 [127]P10(x1273,x1274,x1275,x1276,x1277,x1272,x1278,x1279)+~E(x1271,x1272)+~P10(x1273,x1274,x1275,x1276,x1277,x1271,x1278,x1279)
% 69.42/69.46 [128]P10(x1283,x1284,x1285,x1286,x1287,x1288,x1282,x1289)+~E(x1281,x1282)+~P10(x1283,x1284,x1285,x1286,x1287,x1288,x1281,x1289)
% 69.42/69.46 [129]P10(x1293,x1294,x1295,x1296,x1297,x1298,x1299,x1292)+~E(x1291,x1292)+~P10(x1293,x1294,x1295,x1296,x1297,x1298,x1299,x1291)
% 69.42/69.46 [130]P8(x1302,x1303,x1304,x1305,x1306,x1307)+~E(x1301,x1302)+~P8(x1301,x1303,x1304,x1305,x1306,x1307)
% 69.42/69.46 [131]P8(x1313,x1312,x1314,x1315,x1316,x1317)+~E(x1311,x1312)+~P8(x1313,x1311,x1314,x1315,x1316,x1317)
% 69.42/69.46 [132]P8(x1323,x1324,x1322,x1325,x1326,x1327)+~E(x1321,x1322)+~P8(x1323,x1324,x1321,x1325,x1326,x1327)
% 69.42/69.46 [133]P8(x1333,x1334,x1335,x1332,x1336,x1337)+~E(x1331,x1332)+~P8(x1333,x1334,x1335,x1331,x1336,x1337)
% 69.42/69.46 [134]P8(x1343,x1344,x1345,x1346,x1342,x1347)+~E(x1341,x1342)+~P8(x1343,x1344,x1345,x1346,x1341,x1347)
% 69.42/69.46 [135]P8(x1353,x1354,x1355,x1356,x1357,x1352)+~E(x1351,x1352)+~P8(x1353,x1354,x1355,x1356,x1357,x1351)
% 69.42/69.46 [136]P11(x1362,x1363,x1364,x1365,x1366,x1367)+~E(x1361,x1362)+~P11(x1361,x1363,x1364,x1365,x1366,x1367)
% 69.42/69.46 [137]P11(x1373,x1372,x1374,x1375,x1376,x1377)+~E(x1371,x1372)+~P11(x1373,x1371,x1374,x1375,x1376,x1377)
% 69.42/69.46 [138]P11(x1383,x1384,x1382,x1385,x1386,x1387)+~E(x1381,x1382)+~P11(x1383,x1384,x1381,x1385,x1386,x1387)
% 69.42/69.46 [139]P11(x1393,x1394,x1395,x1392,x1396,x1397)+~E(x1391,x1392)+~P11(x1393,x1394,x1395,x1391,x1396,x1397)
% 69.42/69.46 [140]P11(x1403,x1404,x1405,x1406,x1402,x1407)+~E(x1401,x1402)+~P11(x1403,x1404,x1405,x1406,x1401,x1407)
% 69.42/69.46 [141]P11(x1413,x1414,x1415,x1416,x1417,x1412)+~E(x1411,x1412)+~P11(x1413,x1414,x1415,x1416,x1417,x1411)
% 69.42/69.46
% 69.42/69.46 %-------------------------------------------
% 69.42/69.46 cnf(262,plain,
% 69.42/69.46 (~P3(a14,a17,a1,a16)),
% 69.42/69.46 inference(scs_inference,[],[148,161])).
% 69.42/69.46 cnf(264,plain,
% 69.42/69.46 (~P3(a1,a16,a17,a14)),
% 69.42/69.46 inference(scs_inference,[],[148,161,162])).
% 69.42/69.46 cnf(268,plain,
% 69.42/69.46 (~P10(a14,a17,x2681,x2682,a1,a16,x2681,x2682)),
% 69.42/69.46 inference(scs_inference,[],[148,161,162,231,250])).
% 69.42/69.46 cnf(272,plain,
% 69.42/69.46 (~P10(a16,a1,x2721,x2722,a14,a17,x2721,x2722)),
% 69.42/69.46 inference(scs_inference,[],[148,161,162,231,250,251,252])).
% 69.42/69.46 cnf(274,plain,
% 69.42/69.46 (~P10(a1,a16,a14,a17,x2741,x2742,x2741,x2742)),
% 69.42/69.46 inference(scs_inference,[],[148,161,162,231,250,251,252,253])).
% 69.42/69.46 cnf(278,plain,
% 69.42/69.46 (~P10(a14,a17,a14,a15,a1,a14,a15,a16)),
% 69.42/69.46 inference(scs_inference,[],[142,144,148,161,162,231,250,251,252,253,178,239])).
% 69.42/69.46 cnf(280,plain,
% 69.42/69.46 (~P1(a14,a15,a14,a17)),
% 69.42/69.46 inference(scs_inference,[],[142,144,148,161,162,231,250,251,252,253,178,239,163])).
% 69.42/69.46 cnf(282,plain,
% 69.42/69.46 (~P1(a14,a17,a15,a14)),
% 69.42/69.46 inference(scs_inference,[],[142,144,148,161,162,231,250,251,252,253,178,239,163,164])).
% 69.42/69.46 cnf(284,plain,
% 69.42/69.46 (~P3(a16,a1,a14,a17)),
% 69.42/69.46 inference(scs_inference,[],[142,144,148,161,162,231,250,251,252,253,178,239,163,164,223])).
% 69.42/69.46 cnf(301,plain,
% 69.42/69.46 (~P3(a17,a14,a1,a16)),
% 69.42/69.46 inference(scs_inference,[],[264,161])).
% 69.42/69.46 cnf(303,plain,
% 69.42/69.46 (~P1(a14,a15,a17,a14)),
% 69.42/69.46 inference(scs_inference,[],[280,264,161,164])).
% 69.42/69.46 cnf(305,plain,
% 69.42/69.46 (~P3(a14,a17,a16,a1)),
% 69.42/69.46 inference(scs_inference,[],[280,262,264,161,164,162])).
% 69.42/69.46 cnf(307,plain,
% 69.42/69.46 (~P1(a15,a14,a14,a17)),
% 69.42/69.46 inference(scs_inference,[],[280,262,264,282,161,164,162,163])).
% 69.42/69.46 cnf(309,plain,
% 69.42/69.46 (~P10(a1,a16,x3091,x3092,a17,a14,x3091,x3092)),
% 69.42/69.46 inference(scs_inference,[],[280,262,264,282,161,164,162,163,231])).
% 69.42/69.46 cnf(313,plain,
% 69.42/69.46 (~P10(a1,a14,a15,a16,a14,a17,a14,a15)),
% 69.42/69.46 inference(scs_inference,[],[280,262,264,278,282,161,164,162,163,231,251,250])).
% 69.42/69.46 cnf(315,plain,
% 69.42/69.46 (~P10(a14,a17,a1,a14,a14,a15,a15,a16)),
% 69.42/69.46 inference(scs_inference,[],[280,262,264,278,282,161,164,162,163,231,251,250,253])).
% 69.42/69.46 cnf(319,plain,
% 69.42/69.46 (P3(a1,a14,a16,a17)),
% 69.42/69.46 inference(scs_inference,[],[142,280,145,262,264,278,282,161,164,162,163,231,251,250,253,252,178])).
% 69.42/69.46 cnf(321,plain,
% 69.42/69.46 (~P10(a1,a16,a14,a17,a1,a14,a16,a17)),
% 69.42/69.46 inference(scs_inference,[],[142,280,145,148,262,264,278,282,161,164,162,163,231,251,250,253,252,178,238])).
% 69.42/69.46 cnf(323,plain,
% 69.42/69.46 (~P10(a14,a15,a14,a17,a1,a14,a15,a16)),
% 69.42/69.46 inference(scs_inference,[],[142,280,145,148,262,264,278,282,161,164,162,163,231,251,250,253,252,178,238,239])).
% 69.42/69.46 cnf(325,plain,
% 69.42/69.46 (~P4(x3251,a15,a17)+~P2(x3251,a15,a14,a17)),
% 69.42/69.46 inference(scs_inference,[],[142,280,145,148,262,264,278,282,161,164,162,163,231,251,250,253,252,178,238,239,170])).
% 69.42/69.46 cnf(339,plain,
% 69.42/69.46 (~P1(a15,a14,a17,a14)),
% 69.42/69.46 inference(scs_inference,[],[307,164])).
% 69.42/69.46 cnf(341,plain,
% 69.42/69.46 (~P3(a17,a14,a16,a1)),
% 69.42/69.46 inference(scs_inference,[],[307,301,164,162])).
% 69.42/69.46 cnf(343,plain,
% 69.42/69.46 (~P10(a1,a16,a17,a14,x3431,x3432,x3431,x3432)),
% 69.42/69.46 inference(scs_inference,[],[307,309,301,164,162,253])).
% 69.42/69.46 cnf(345,plain,
% 69.42/69.46 (~P1(a17,a14,a14,a15)),
% 69.42/69.46 inference(scs_inference,[],[307,309,301,303,164,162,253,163])).
% 69.42/69.46 cnf(347,plain,
% 69.42/69.46 (~P10(a17,a14,x3471,x3472,a1,a16,x3471,x3472)),
% 69.42/69.46 inference(scs_inference,[],[307,309,301,303,164,162,253,163,231])).
% 69.42/69.46 cnf(349,plain,
% 69.42/69.46 (~P10(a1,a14,a16,a17,a1,a16,a14,a17)),
% 69.42/69.46 inference(scs_inference,[],[307,309,301,303,321,164,162,253,163,231,250])).
% 69.42/69.46 cnf(353,plain,
% 69.42/69.46 (~P10(a16,a1,x3531,x3532,a17,a14,x3531,x3532)),
% 69.42/69.46 inference(scs_inference,[],[307,309,301,303,321,164,162,253,163,231,250,251,252])).
% 69.42/69.46 cnf(355,plain,
% 69.42/69.46 (~P10(a15,a14,a14,a17,a1,a14,a15,a16)),
% 69.42/69.46 inference(scs_inference,[],[142,307,309,301,303,321,164,162,253,163,231,250,251,252,239])).
% 69.42/69.46 cnf(357,plain,
% 69.42/69.46 (~P10(a17,a14,a1,a16,a1,a14,a16,a17)),
% 69.42/69.46 inference(scs_inference,[],[142,307,309,301,303,319,321,164,162,253,163,231,250,251,252,239,238])).
% 69.42/69.46 cnf(359,plain,
% 69.42/69.46 (~P3(a16,a1,a17,a14)),
% 69.42/69.46 inference(scs_inference,[],[142,307,309,301,303,319,321,164,162,253,163,231,250,251,252,239,238,223])).
% 69.42/69.46 cnf(366,plain,
% 69.42/69.46 (~P1(a17,a14,a15,a14)),
% 69.42/69.46 inference(scs_inference,[],[345,164])).
% 69.42/69.46 cnf(368,plain,
% 69.42/69.46 (~P10(a17,a14,a1,a16,x3681,x3682,x3681,x3682)),
% 69.42/69.46 inference(scs_inference,[],[345,347,164,253])).
% 69.42/69.46 cnf(370,plain,
% 69.42/69.46 (~P10(a14,a17,x3701,x3702,a16,a1,x3701,x3702)),
% 69.42/69.46 inference(scs_inference,[],[345,305,347,164,253,231])).
% 69.42/69.46 cnf(372,plain,
% 69.42/69.46 (~P10(a14,a17,a1,a16,a1,a14,a16,a17)),
% 69.42/69.46 inference(scs_inference,[],[345,305,347,357,164,253,231,252])).
% 69.42/69.46 cnf(376,plain,
% 69.42/69.46 (~P10(a1,a14,a15,a16,a14,a15,a14,a17)),
% 69.42/69.46 inference(scs_inference,[],[345,305,347,323,357,164,253,231,252,251,250])).
% 69.42/69.46 cnf(378,plain,
% 69.42/69.46 (~P10(a14,a17,a16,a1,a1,a14,a16,a17)),
% 69.42/69.46 inference(scs_inference,[],[345,305,347,323,357,319,164,253,231,252,251,250,238])).
% 69.42/69.46 cnf(380,plain,
% 69.42/69.46 (~P10(a15,a14,a17,a14,a1,a14,a15,a16)),
% 69.42/69.46 inference(scs_inference,[],[142,345,305,347,323,339,357,319,164,253,231,252,251,250,238,239])).
% 69.42/69.46 cnf(383,plain,
% 69.42/69.46 (~E(a17,a1)+~E(a1,a17)),
% 69.42/69.46 inference(scs_inference,[],[142,345,305,341,347,323,339,357,319,164,253,231,252,251,250,238,239,111,114])).
% 69.42/69.46 cnf(392,plain,
% 69.42/69.46 (~P10(a17,a14,x3921,x3922,a16,a1,x3921,x3922)),
% 69.42/69.46 inference(scs_inference,[],[341,355,253,231])).
% 69.42/69.46 cnf(396,plain,
% 69.42/69.46 (~P10(a14,a17,a15,a14,a15,a16,a1,a14)),
% 69.42/69.46 inference(scs_inference,[],[341,355,378,253,231,252,251])).
% 69.42/69.46 cnf(398,plain,
% 69.42/69.46 (~P10(a1,a14,a15,a16,a15,a14,a14,a17)),
% 69.42/69.46 inference(scs_inference,[],[341,355,378,253,231,252,251,250])).
% 69.42/69.46 cnf(400,plain,
% 69.42/69.46 (~P10(a14,a17,a15,a14,a1,a14,a15,a16)),
% 69.42/69.46 inference(scs_inference,[],[142,341,282,355,378,253,231,252,251,250,239])).
% 69.42/69.46 cnf(402,plain,
% 69.42/69.46 (~P10(a1,a16,a17,a14,a1,a14,a16,a17)),
% 69.42/69.46 inference(scs_inference,[],[142,264,341,282,355,378,319,253,231,252,251,250,239,238])).
% 69.42/69.46 cnf(404,plain,
% 69.42/69.46 (~P3(x4041,x4042,a1,a14)+P3(x4041,x4042,a16,a17)),
% 69.42/69.46 inference(scs_inference,[],[142,264,341,282,355,378,319,253,231,252,251,250,239,238,177])).
% 69.42/69.46 cnf(410,plain,
% 69.42/69.46 (~P10(a14,a17,a16,a1,x4101,x4102,x4101,x4102)),
% 69.42/69.46 inference(scs_inference,[],[370,253])).
% 69.42/69.46 cnf(412,plain,
% 69.42/69.46 (~P10(a14,a15,a17,a14,a1,a14,a15,a16)),
% 69.42/69.46 inference(scs_inference,[],[370,380,253,252])).
% 69.42/69.46 cnf(418,plain,
% 69.42/69.46 (~P10(a16,a1,a14,a17,a1,a14,a16,a17)),
% 69.42/69.46 inference(scs_inference,[],[370,380,319,284,253,252,251,250,238])).
% 69.42/69.46 cnf(420,plain,
% 69.42/69.46 (~P10(a17,a14,a15,a14,a1,a14,a15,a16)),
% 69.42/69.46 inference(scs_inference,[],[142,366,370,380,319,284,253,252,251,250,238,239])).
% 69.42/69.46 cnf(428,plain,
% 69.42/69.46 (~P10(a17,a14,a16,a1,x4281,x4282,x4281,x4282)),
% 69.42/69.46 inference(scs_inference,[],[392,253])).
% 69.42/69.46 cnf(434,plain,
% 69.42/69.46 (~P10(a1,a14,a15,a16,a14,a17,a15,a14)),
% 69.42/69.46 inference(scs_inference,[],[392,400,402,253,252,251,250])).
% 69.42/69.46 cnf(437,plain,
% 69.42/69.46 (~P6(a14,a17,a15,a17)+~P6(a14,a14,a15,a14)),
% 69.42/69.46 inference(scs_inference,[],[280,146,392,400,402,253,252,251,250,108,179])).
% 69.42/69.46 cnf(440,plain,
% 69.42/69.46 (~P4(x4401,a17,a15)+~P2(x4401,a17,a14,a15)),
% 69.42/69.46 inference(scs_inference,[],[280,345,146,392,319,400,402,253,252,251,250,108,179,112,170])).
% 69.42/69.46 cnf(450,plain,
% 69.42/69.46 (~P10(a16,a1,a14,a17,x4501,x4502,x4501,x4502)),
% 69.42/69.46 inference(scs_inference,[],[420,274,253,252])).
% 69.42/69.46 cnf(452,plain,
% 69.42/69.46 (~P10(a15,a14,a17,a14,a15,a16,a1,a14)),
% 69.42/69.46 inference(scs_inference,[],[420,274,253,252,251])).
% 69.42/69.46 cnf(454,plain,
% 69.42/69.46 (~P10(a1,a14,a15,a16,a17,a14,a15,a14)),
% 69.42/69.46 inference(scs_inference,[],[420,274,253,252,251,250])).
% 69.42/69.46 cnf(456,plain,
% 69.42/69.46 (~P1(x4561,x4562,a1,a15)+P3(x4561,x4562,a14,a16)),
% 69.42/69.46 inference(scs_inference,[],[143,420,274,253,252,251,250,178])).
% 69.42/69.46 cnf(468,plain,
% 69.42/69.46 (~P10(a16,a1,a1,a14,a14,a17,a16,a17)),
% 69.42/69.46 inference(scs_inference,[],[418,253])).
% 69.42/69.46 cnf(470,plain,
% 69.42/69.46 (~P10(a16,a1,a17,a14,x4701,x4702,x4701,x4702)),
% 69.42/69.46 inference(scs_inference,[],[418,343,253,252])).
% 69.42/69.46 cnf(472,plain,
% 69.42/69.46 (~P10(a14,a17,a16,a1,a16,a17,a1,a14)),
% 69.42/69.46 inference(scs_inference,[],[418,343,253,252,251])).
% 69.42/69.46 cnf(482,plain,
% 69.42/69.46 (~P10(a14,a15,a1,a14,a14,a17,a15,a16)),
% 69.42/69.46 inference(scs_inference,[],[323,253])).
% 69.42/69.46 cnf(488,plain,
% 69.42/69.46 (~P10(a1,a14,a16,a17,a17,a14,a1,a16)),
% 69.42/69.46 inference(scs_inference,[],[323,357,368,253,252,251,250])).
% 69.42/69.46 cnf(491,plain,
% 69.42/69.46 (~E(a16,a14)),
% 69.42/69.46 inference(scs_inference,[],[307,145,323,357,368,253,252,251,250,90,89])).
% 69.42/69.46 cnf(499,plain,
% 69.42/69.46 (~P10(a14,a17,a1,a16,a16,a17,a1,a14)),
% 69.42/69.46 inference(scs_inference,[],[321,349,253,252,251])).
% 69.42/69.47 cnf(519,plain,
% 69.42/69.47 (~P10(a14,a17,a1,a14,a15,a14,a15,a16)),
% 69.42/69.47 inference(scs_inference,[],[400,253])).
% 69.42/69.47 cnf(525,plain,
% 69.42/69.47 (~P10(a1,a14,a16,a17,a1,a16,a17,a14)),
% 69.42/69.47 inference(scs_inference,[],[400,402,434,253,252,251,250])).
% 69.42/69.47 cnf(548,plain,
% 69.42/69.47 (~P10(a1,a16,a17,a14,a16,a17,a1,a14)),
% 69.42/69.47 inference(scs_inference,[],[357,376,253,252,251])).
% 69.42/69.47 cnf(550,plain,
% 69.42/69.47 (~P10(x5501,x5502,x5501,x5502,a1,a16,a14,a17)),
% 69.42/69.47 inference(scs_inference,[],[357,274,376,253,252,251,250])).
% 69.42/69.47 cnf(553,plain,
% 69.42/69.47 (~P1(a16,a17,x5531,x5532)+P1(a1,a14,x5531,x5532)),
% 69.42/69.47 inference(scs_inference,[],[142,319,357,274,376,253,252,251,250,88,180])).
% 69.42/69.47 cnf(564,plain,
% 69.42/69.47 (~P10(a14,a17,a1,a14,a16,a1,a16,a17)),
% 69.42/69.47 inference(scs_inference,[],[378,253])).
% 69.42/69.47 cnf(570,plain,
% 69.42/69.47 (~P10(x5701,x5702,x5701,x5702,a1,a16,a17,a14)),
% 69.42/69.47 inference(scs_inference,[],[378,343,313,253,252,251,250])).
% 69.42/69.47 cnf(578,plain,
% 69.42/69.47 (~P10(x5781,x5782,x5782,x5781,a1,a16,a14,a17)),
% 69.42/69.47 inference(scs_inference,[],[380,550,253,252])).
% 69.42/69.47 cnf(580,plain,
% 69.42/69.47 (~P10(a17,a14,a15,a14,a15,a16,a1,a14)),
% 69.42/69.47 inference(scs_inference,[],[380,550,253,252,251])).
% 69.42/69.47 cnf(582,plain,
% 69.42/69.47 (~P10(x5821,x5822,x5821,x5822,a17,a14,a1,a16)),
% 69.42/69.47 inference(scs_inference,[],[380,368,550,253,252,251,250])).
% 69.42/69.47 cnf(591,plain,
% 69.42/69.47 (~P10(x5911,x5912,x5912,x5911,a1,a16,a17,a14)),
% 69.42/69.47 inference(scs_inference,[],[402,570,253,252])).
% 69.42/69.47 cnf(595,plain,
% 69.42/69.47 (~P10(x5951,x5952,x5951,x5952,a14,a17,a16,a1)),
% 69.42/69.47 inference(scs_inference,[],[402,410,570,253,252,251,250])).
% 69.42/69.47 cnf(614,plain,
% 69.42/69.47 (~P10(x6141,x6142,x6142,x6141,a17,a14,a1,a16)),
% 69.42/69.47 inference(scs_inference,[],[578,582,253,252])).
% 69.42/69.47 cnf(618,plain,
% 69.42/69.47 (~P10(x6181,x6182,x6181,x6182,a17,a14,a16,a1)),
% 69.42/69.47 inference(scs_inference,[],[268,428,578,582,253,252,251,250])).
% 69.42/69.47 cnf(620,plain,
% 69.42/69.47 (~P11(a14,a1,a16,a1,a14,a17)),
% 69.42/69.47 inference(scs_inference,[],[268,428,578,582,253,252,251,250,229])).
% 69.42/69.47 cnf(636,plain,
% 69.42/69.47 (~P11(a14,a16,a1,a1,a17,a14)),
% 69.42/69.47 inference(scs_inference,[],[620,214])).
% 69.42/69.47 cnf(638,plain,
% 69.42/69.47 (~P11(a1,a14,a16,a14,a1,a17)),
% 69.42/69.47 inference(scs_inference,[],[620,214,213])).
% 69.42/69.47 cnf(640,plain,
% 69.42/69.47 (~P11(a1,a14,a17,a14,a1,a16)),
% 69.42/69.47 inference(scs_inference,[],[620,214,213,212])).
% 69.42/69.47 cnf(642,plain,
% 69.42/69.47 (~P10(x6421,x6422,a1,a16,x6422,x6421,a17,a14)),
% 69.42/69.47 inference(scs_inference,[],[591,620,214,213,212,253])).
% 69.42/69.47 cnf(644,plain,
% 69.42/69.47 (~P10(x6441,x6442,x6442,x6441,a14,a17,a16,a1)),
% 69.42/69.47 inference(scs_inference,[],[591,595,620,214,213,212,253,252])).
% 69.42/69.47 cnf(648,plain,
% 69.42/69.47 (~P10(x6481,x6482,x6481,x6482,a16,a1,a14,a17)),
% 69.42/69.47 inference(scs_inference,[],[272,450,591,595,620,214,213,212,253,252,251,250])).
% 69.42/69.47 cnf(650,plain,
% 69.42/69.47 (~P11(a17,a1,a16,a1,a17,a14)),
% 69.42/69.47 inference(scs_inference,[],[272,450,591,595,620,214,213,212,253,252,251,250,229])).
% 69.42/69.47 cnf(657,plain,
% 69.42/69.47 (~P11(a1,a16,a14,a14,a17,a1)),
% 69.42/69.47 inference(scs_inference,[],[638,214])).
% 69.42/69.47 cnf(659,plain,
% 69.42/69.47 (~P11(a16,a14,a1,a17,a1,a14)),
% 69.42/69.47 inference(scs_inference,[],[636,638,214,213])).
% 69.42/69.47 cnf(663,plain,
% 69.42/69.47 (~P10(x6631,x6632,a17,a14,x6632,x6631,a1,a16)),
% 69.42/69.47 inference(scs_inference,[],[614,636,638,214,213,212,253])).
% 69.42/69.47 cnf(665,plain,
% 69.42/69.47 (~P10(x6651,x6652,x6652,x6651,a17,a14,a16,a1)),
% 69.42/69.47 inference(scs_inference,[],[614,618,636,638,214,213,212,253,252])).
% 69.42/69.47 cnf(669,plain,
% 69.42/69.47 (~P10(x6691,x6692,x6691,x6692,a16,a1,a17,a14)),
% 69.42/69.47 inference(scs_inference,[],[353,470,614,618,636,638,214,213,212,253,252,251,250])).
% 69.42/69.47 cnf(671,plain,
% 69.42/69.47 (~P11(a1,a17,a14,a17,a1,a16)),
% 69.42/69.47 inference(scs_inference,[],[353,470,614,618,636,638,214,213,212,253,252,251,250,229])).
% 69.42/69.47 cnf(688,plain,
% 69.42/69.47 (~P11(a1,a17,a16,a17,a1,a14)),
% 69.42/69.47 inference(scs_inference,[],[650,214,213])).
% 69.42/69.47 cnf(692,plain,
% 69.42/69.47 (~P10(x6921,x6922,a14,a17,x6922,x6921,a16,a1)),
% 69.42/69.47 inference(scs_inference,[],[644,650,657,214,213,212,253])).
% 69.42/69.47 cnf(698,plain,
% 69.42/69.47 (~P10(a1,a16,a14,a17,x6981,x6982,x6982,x6981)),
% 69.42/69.47 inference(scs_inference,[],[550,578,644,648,650,657,214,213,212,253,252,251,250])).
% 69.42/69.47 cnf(700,plain,
% 69.42/69.47 (~P11(a16,a14,a17,a14,a16,a1)),
% 69.42/69.47 inference(scs_inference,[],[550,578,644,648,650,657,214,213,212,253,252,251,250,229])).
% 69.42/69.47 cnf(706,plain,
% 69.42/69.47 (~P11(a1,a14,a17,a17,a16,a1)),
% 69.42/69.47 inference(scs_inference,[],[671,214])).
% 69.42/69.47 cnf(714,plain,
% 69.42/69.47 (~P10(x7141,x7142,x7142,x7141,a16,a1,a17,a14)),
% 69.42/69.47 inference(scs_inference,[],[665,669,671,659,214,213,212,253,252])).
% 69.42/69.47 cnf(716,plain,
% 69.42/69.47 (~P10(x7161,x7162,x7162,x7161,a14,a17,a1,a16)),
% 69.42/69.47 inference(scs_inference,[],[578,665,669,671,659,214,213,212,253,252,251])).
% 69.42/69.47 cnf(718,plain,
% 69.42/69.47 (~P10(a1,a16,a17,a14,x7181,x7182,x7182,x7181)),
% 69.42/69.47 inference(scs_inference,[],[578,591,665,669,671,659,214,213,212,253,252,251,250])).
% 69.42/69.47 cnf(720,plain,
% 69.42/69.47 (~P11(a16,a17,a14,a17,a16,a1)),
% 69.42/69.47 inference(scs_inference,[],[578,591,665,669,671,659,214,213,212,253,252,251,250,229])).
% 69.42/69.47 cnf(732,plain,
% 69.42/69.47 (~P11(a14,a16,a1,a16,a14,a17)),
% 69.42/69.47 inference(scs_inference,[],[700,214,213,212])).
% 69.42/69.47 cnf(747,plain,
% 69.42/69.47 (~P11(a16,a14,a17,a17,a1,a16)),
% 69.42/69.47 inference(scs_inference,[],[720,214])).
% 69.42/69.47 cnf(753,plain,
% 69.42/69.47 (~P10(a1,a16,x7531,x7532,a14,a17,x7532,x7531)),
% 69.42/69.47 inference(scs_inference,[],[698,720,214,213,212,253])).
% 69.42/69.47 cnf(757,plain,
% 69.42/69.47 (~P10(a1,a16,x7571,x7572,a17,a14,x7572,x7571)),
% 69.42/69.47 inference(scs_inference,[],[698,642,718,720,214,213,212,253,252,251])).
% 69.42/69.47 cnf(761,plain,
% 69.42/69.47 (~P11(a1,a16,a17,a14,a17,a16)),
% 69.42/69.47 inference(scs_inference,[],[644,698,642,718,720,214,213,212,253,252,251,250,229])).
% 69.42/69.47 cnf(769,plain,
% 69.42/69.47 (~P11(a16,a14,a1,a14,a16,a17)),
% 69.42/69.47 inference(scs_inference,[],[732,214,213])).
% 69.42/69.47 cnf(774,plain,
% 69.42/69.47 (~P11(a17,a1,a16,a16,a14,a17)),
% 69.42/69.47 inference(scs_inference,[],[732,757,747,214,213,229,212])).
% 69.42/69.47 cnf(782,plain,
% 69.42/69.47 (~P10(a17,a14,x7821,x7822,a1,a16,x7822,x7821)),
% 69.42/69.47 inference(scs_inference,[],[665,714,663,398,732,757,747,214,213,229,212,253,252,250,251])).
% 69.42/69.47 cnf(796,plain,
% 69.42/69.47 (~P11(a14,a17,a16,a1,a16,a17)),
% 69.42/69.47 inference(scs_inference,[],[640,688,761,782,214,213,229,212])).
% 69.42/69.47 cnf(802,plain,
% 69.42/69.47 (~P10(a14,a17,x8021,x8022,a16,a1,x8022,x8021)),
% 69.42/69.47 inference(scs_inference,[],[716,692,753,640,688,761,782,214,213,229,212,253,252,251])).
% 69.42/69.47 cnf(847,plain,
% 69.42/69.47 (~P10(a1,a14,a16,a17,a14,a17,a1,a16)),
% 69.42/69.47 inference(scs_inference,[],[802,372,454,706,769,214,213,229,212,253,252,251,250])).
% 69.42/69.47 cnf(877,plain,
% 69.42/69.47 (~P10(a14,a1,a16,a17,a17,a14,a1,a16)),
% 69.42/69.47 inference(scs_inference,[],[412,488,774,796,214,213,253,252])).
% 69.42/69.47 cnf(879,plain,
% 69.42/69.47 (~P10(a17,a14,a14,a15,a15,a16,a1,a14)),
% 69.42/69.47 inference(scs_inference,[],[412,488,774,796,214,213,253,252,251])).
% 69.42/69.47 cnf(901,plain,
% 69.42/69.47 (~P10(a16,a17,a1,a14,a17,a14,a1,a16)),
% 69.42/69.47 inference(scs_inference,[],[525,253,252,251])).
% 69.42/69.47 cnf(906,plain,
% 69.42/69.47 (~E(a17,a1)),
% 69.42/69.47 inference(scs_inference,[],[383,2])).
% 69.42/69.47 cnf(907,plain,
% 69.42/69.47 (~P10(a14,a17,a15,a16,a15,a14,a1,a14)),
% 69.42/69.47 inference(scs_inference,[],[396,253])).
% 69.42/69.47 cnf(909,plain,
% 69.42/69.47 (~P10(a17,a14,a1,a14,a14,a15,a15,a16)),
% 69.42/69.47 inference(scs_inference,[],[315,396,253,252])).
% 69.42/69.47 cnf(911,plain,
% 69.42/69.47 (~P10(a1,a14,a14,a17,a15,a16,a14,a15)),
% 69.42/69.47 inference(scs_inference,[],[315,396,253,252,251])).
% 69.42/69.47 cnf(913,plain,
% 69.42/69.47 (~P10(a14,a15,a15,a16,a14,a17,a1,a14)),
% 69.42/69.47 inference(scs_inference,[],[315,396,253,252,251,250])).
% 69.42/69.47 cnf(916,plain,
% 69.42/69.47 (~P10(a15,a14,a15,a16,a17,a14,a1,a14)),
% 69.42/69.47 inference(scs_inference,[],[452,253])).
% 69.42/69.47 cnf(929,plain,
% 69.42/69.47 (~P10(a1,a14,a14,a15,a15,a16,a14,a17)),
% 69.42/69.47 inference(scs_inference,[],[482,472,907,253,252,251])).
% 69.42/69.47 cnf(938,plain,
% 69.42/69.47 (~P10(a1,a14,a14,a17,a15,a16,a15,a14)),
% 69.42/69.47 inference(scs_inference,[],[519,499,916,253,252,251])).
% 69.42/69.47 cnf(958,plain,
% 69.42/69.47 (~P10(a16,a17,a1,a14,a1,a16,a17,a14)),
% 69.42/69.47 inference(scs_inference,[],[468,548,901,253,252,251,250])).
% 69.42/69.47 cnf(979,plain,
% 69.42/69.47 (~P10(a17,a14,a15,a16,a14,a15,a1,a14)),
% 69.42/69.47 inference(scs_inference,[],[879,253])).
% 69.42/69.47 cnf(981,plain,
% 69.42/69.47 (~P10(a14,a1,a16,a17,a14,a17,a1,a16)),
% 69.42/69.47 inference(scs_inference,[],[879,847,253,252])).
% 69.42/69.47 cnf(985,plain,
% 69.42/69.47 (~P10(a15,a16,a1,a14,a17,a14,a15,a14)),
% 69.42/69.47 inference(scs_inference,[],[564,580,879,847,253,252,251,250])).
% 69.42/69.47 cnf(1065,plain,
% 69.42/69.47 (~P10(a15,a16,a14,a15,a1,a14,a14,a17)),
% 69.42/69.47 inference(scs_inference,[],[913,877,958,253,252,251])).
% 69.42/69.47 cnf(1092,plain,
% 69.42/69.47 (~P10(a15,a16,a17,a14,a1,a14,a14,a15)),
% 69.42/69.47 inference(scs_inference,[],[979,981,985,253,252,251])).
% 69.42/69.47 cnf(1206,plain,
% 69.42/69.47 (~P10(a15,a16,a1,a14,a17,a14,a14,a15)),
% 69.42/69.47 inference(scs_inference,[],[1092,253])).
% 69.42/69.47 cnf(2693,plain,
% 69.42/69.47 (P1(f6(a14,a17,a19,a18),a14,a14,a18)),
% 69.42/69.47 inference(scs_inference,[],[491,146,2,185])).
% 69.42/69.47 cnf(2695,plain,
% 69.42/69.47 (P3(a16,a17,a1,a14)),
% 69.42/69.47 inference(scs_inference,[],[491,146,319,2,185,161])).
% 69.42/69.47 cnf(2697,plain,
% 69.42/69.47 (P10(a1,a14,x26971,x26972,a16,a17,x26971,x26972)),
% 69.42/69.47 inference(scs_inference,[],[491,146,319,2,185,161,223])).
% 69.42/69.47 cnf(2699,plain,
% 69.42/69.47 (P1(a1,a14,a16,a15)),
% 69.42/69.47 inference(scs_inference,[],[142,491,146,319,2,185,161,223,164])).
% 69.42/69.47 cnf(2701,plain,
% 69.42/69.47 (P3(a1,a14,a17,a16)),
% 69.42/69.47 inference(scs_inference,[],[142,491,146,319,2,185,161,223,164,162])).
% 69.42/69.47 cnf(2703,plain,
% 69.42/69.47 (P1(a15,a16,a1,a14)),
% 69.42/69.47 inference(scs_inference,[],[142,491,146,319,2,185,161,223,164,162,163])).
% 69.42/69.47 cnf(2705,plain,
% 69.42/69.47 (P10(a14,a1,x27051,x27052,a16,a17,x27051,x27052)),
% 69.42/69.47 inference(scs_inference,[],[142,491,146,319,2,185,161,223,164,162,163,252])).
% 69.42/69.47 cnf(2707,plain,
% 69.42/69.47 (P10(x27071,x27072,a1,a14,x27071,x27072,a16,a17)),
% 69.42/69.47 inference(scs_inference,[],[142,491,146,319,2,185,161,223,164,162,163,252,251])).
% 69.42/69.47 cnf(2711,plain,
% 69.42/69.47 (P10(a16,a17,x27111,x27112,a1,a14,x27111,x27112)),
% 69.42/69.47 inference(scs_inference,[],[142,491,146,319,2,185,161,223,164,162,163,252,251,253,250])).
% 69.42/69.47 cnf(2713,plain,
% 69.42/69.47 (P4(f3(a1,a14,a16),a16,a14)),
% 69.42/69.47 inference(scs_inference,[],[142,491,144,143,146,319,2,185,161,223,164,162,163,252,251,253,250,175])).
% 69.42/69.47 cnf(2715,plain,
% 69.42/69.47 (P4(f4(a1,a14,a16),a16,a1)),
% 69.42/69.47 inference(scs_inference,[],[142,491,144,143,146,319,2,185,161,223,164,162,163,252,251,253,250,175,176])).
% 69.42/69.47 cnf(2717,plain,
% 69.42/69.47 (P1(a1,f3(a1,a14,a16),a16,a14)),
% 69.42/69.47 inference(scs_inference,[],[142,491,144,143,146,319,2,185,161,223,164,162,163,252,251,253,250,175,176,187])).
% 69.42/69.47 cnf(2719,plain,
% 69.42/69.47 (P1(a16,a17,a15,a16)),
% 69.42/69.47 inference(scs_inference,[],[142,491,144,143,146,319,2,185,161,223,164,162,163,252,251,253,250,175,176,187,180])).
% 69.42/69.47 cnf(2721,plain,
% 69.42/69.47 (~P10(a16,a17,a14,a17,a15,a16,a14,a15)),
% 69.42/69.47 inference(scs_inference,[],[142,911,491,144,143,146,319,2,185,161,223,164,162,163,252,251,253,250,175,176,187,180,260])).
% 69.42/69.47 cnf(2727,plain,
% 69.42/69.47 (P3(a1,a14,a1,a14)),
% 69.42/69.47 inference(scs_inference,[],[142,911,491,144,143,146,145,319,2,185,161,223,164,162,163,252,251,253,250,175,176,187,180,260,188,178,177])).
% 69.42/69.47 cnf(2731,plain,
% 69.42/69.47 (P3(a16,a17,a16,a17)),
% 69.42/69.47 inference(scs_inference,[],[142,911,491,366,144,143,146,145,319,2,185,161,223,164,162,163,252,251,253,250,175,176,187,180,260,188,178,177,239,404])).
% 69.42/69.47 cnf(2733,plain,
% 69.42/69.47 (P4(a16,f3(a1,a14,a16),a14)),
% 69.42/69.47 inference(scs_inference,[],[142,911,491,366,144,143,146,145,319,2,185,161,223,164,162,163,252,251,253,250,175,176,187,180,260,188,178,177,239,404,149])).
% 69.42/69.47 cnf(2735,plain,
% 69.42/69.47 (P4(a15,a16,a16)),
% 69.42/69.47 inference(scs_inference,[],[142,911,491,366,144,143,146,145,319,2,185,161,223,164,162,163,252,251,253,250,175,176,187,180,260,188,178,177,239,404,149,158])).
% 69.42/69.47 cnf(2737,plain,
% 69.42/69.47 (P4(f3(a1,a14,a16),a14,a16)),
% 69.42/69.47 inference(scs_inference,[],[142,911,491,366,144,143,146,145,319,2,185,161,223,164,162,163,252,251,253,250,175,176,187,180,260,188,178,177,239,404,149,158,150])).
% 69.42/69.47 cnf(2739,plain,
% 69.42/69.47 (P3(a14,a1,a16,a17)),
% 69.42/69.47 inference(scs_inference,[],[142,911,491,366,144,143,146,145,319,2,185,161,223,164,162,163,252,251,253,250,175,176,187,180,260,188,178,177,239,404,149,158,150,231])).
% 69.42/69.47 cnf(2741,plain,
% 69.42/69.47 (~P5(x27411,a1,a14)+~P5(x27411,a16,a17)),
% 69.42/69.47 inference(scs_inference,[],[142,911,491,359,366,144,143,146,145,319,2,185,161,223,164,162,163,252,251,253,250,175,176,187,180,260,188,178,177,239,404,149,158,150,231,155])).
% 69.42/69.47 cnf(2743,plain,
% 69.42/69.47 (~P5(x27431,a1,a14)+~P5(x27432,a16,a17)+~E(x27432,x27431)),
% 69.42/69.47 inference(scs_inference,[],[142,911,491,359,366,144,143,146,145,319,2,185,161,223,164,162,163,252,251,253,250,175,176,187,180,260,188,178,177,239,404,149,158,150,231,155,115])).
% 69.42/69.47 cnf(2745,plain,
% 69.42/69.47 (P1(f6(a16,a14,a15,a18),a16,a16,a18)),
% 69.42/69.47 inference(scs_inference,[],[147,185])).
% 69.42/69.47 cnf(2750,plain,
% 69.42/69.47 (P10(a1,a14,x27501,x27502,a17,a16,x27501,x27502)),
% 69.42/69.47 inference(scs_inference,[],[906,2701,147,185,2,161,223])).
% 69.42/69.47 cnf(2754,plain,
% 69.42/69.47 (P1(a15,a16,a14,a1)),
% 69.42/69.47 inference(scs_inference,[],[2703,906,2695,2701,147,185,2,161,223,162,164])).
% 69.42/69.47 cnf(2756,plain,
% 69.42/69.47 (P4(a16,a15,a16)),
% 69.42/69.47 inference(scs_inference,[],[2703,906,2695,2701,2735,147,185,2,161,223,162,164,149])).
% 69.42/69.47 cnf(2760,plain,
% 69.42/69.47 (P4(a1,a14,a14)),
% 69.42/69.47 inference(scs_inference,[],[2703,906,2695,2701,2727,2735,2733,147,185,2,161,223,162,164,149,150,158])).
% 69.42/69.47 cnf(2762,plain,
% 69.42/69.47 (P1(a16,a15,a1,a14)),
% 69.42/69.47 inference(scs_inference,[],[2699,2703,906,2695,2701,2727,2735,2733,147,185,2,161,223,162,164,149,150,158,163])).
% 69.42/69.47 cnf(2764,plain,
% 69.42/69.47 (P10(x27641,x27642,a1,a14,x27642,x27641,a16,a17)),
% 69.42/69.47 inference(scs_inference,[],[2699,2703,906,2707,2695,2701,2727,2735,2733,147,185,2,161,223,162,164,149,150,158,163,252])).
% 69.42/69.47 cnf(2766,plain,
% 69.42/69.47 (P10(x27661,x27662,a14,a1,x27661,x27662,a16,a17)),
% 69.42/69.47 inference(scs_inference,[],[2699,2703,906,2705,2707,2695,2701,2727,2735,2733,147,185,2,161,223,162,164,149,150,158,163,252,251])).
% 69.42/69.47 cnf(2770,plain,
% 69.42/69.47 (P10(a16,a17,x27701,x27702,a14,a1,x27701,x27702)),
% 69.42/69.47 inference(scs_inference,[],[2699,2703,906,2705,2707,2695,2701,2727,2735,2733,147,185,2,161,223,162,164,149,150,158,163,252,251,253,250])).
% 69.42/69.47 cnf(2772,plain,
% 69.42/69.47 (P4(a16,a16,a15)),
% 69.42/69.47 inference(scs_inference,[],[2699,2703,906,2705,2707,2695,2701,2727,2735,2733,147,185,2,161,223,162,164,149,150,158,163,252,251,253,250,153])).
% 69.42/69.47 cnf(2774,plain,
% 69.42/69.47 (P4(f3(a14,a1,a16),a16,a1)),
% 69.42/69.47 inference(scs_inference,[],[2699,2703,906,2705,2707,2695,2701,2727,2735,2733,144,143,147,185,2,161,223,162,164,149,150,158,163,252,251,253,250,153,175])).
% 69.42/69.47 cnf(2776,plain,
% 69.42/69.47 (P1(a14,f3(a14,a1,a16),a16,a1)),
% 69.42/69.47 inference(scs_inference,[],[2699,2703,906,2705,2707,2695,2701,2727,2735,2733,144,143,147,185,2,161,223,162,164,149,150,158,163,252,251,253,250,153,175,187])).
% 69.42/69.47 cnf(2778,plain,
% 69.42/69.47 (P4(f4(a14,a1,a16),a16,a14)),
% 69.42/69.47 inference(scs_inference,[],[2699,2703,906,2705,2707,2695,2701,2727,2735,2733,144,143,147,185,2,161,223,162,164,149,150,158,163,252,251,253,250,153,175,187,176])).
% 69.42/69.47 cnf(2780,plain,
% 69.42/69.47 (P1(a14,f4(a1,a14,a16),a16,a1)),
% 69.42/69.47 inference(scs_inference,[],[2699,2703,906,2705,2707,2695,2701,2727,2735,2733,144,143,147,185,2,161,223,162,164,149,150,158,163,252,251,253,250,153,175,187,176,188])).
% 69.42/69.47 cnf(2785,plain,
% 69.42/69.47 (~P1(a17,a14,a14,f3(a14,a1,a16))),
% 69.42/69.47 inference(scs_inference,[],[909,2699,2703,906,2705,2707,2695,2701,2727,2735,2733,341,144,143,147,185,2,161,223,162,164,149,150,158,163,252,251,253,250,153,175,187,176,188,260,178])).
% 69.42/69.47 cnf(2790,plain,
% 69.42/69.47 (P1(a14,a1,a15,a16)),
% 69.42/69.47 inference(scs_inference,[],[909,2699,2703,906,2719,2705,2707,2711,2695,2701,2727,2735,2733,341,144,143,147,185,2,161,223,162,164,149,150,158,163,252,251,253,250,153,175,187,176,188,260,178,238,239])).
% 69.42/69.47 cnf(2793,plain,
% 69.42/69.47 (P3(a17,a16,a16,a17)),
% 69.42/69.47 inference(scs_inference,[],[909,2699,2703,906,2719,2705,2707,2711,2695,2701,2727,2735,2733,341,144,143,147,185,2,161,223,162,164,149,150,158,163,252,251,253,250,153,175,187,176,188,260,178,238,239,404])).
% 69.42/69.47 cnf(2799,plain,
% 69.42/69.47 (P1(a16,a15,a14,a1)),
% 69.42/69.47 inference(scs_inference,[],[2762,164])).
% 69.42/69.47 cnf(2803,plain,
% 69.42/69.47 (P4(a14,a1,a14)),
% 69.42/69.47 inference(scs_inference,[],[2739,2760,2762,164,162,149])).
% 69.42/69.47 cnf(2807,plain,
% 69.42/69.47 (P4(a16,a17,a17)),
% 69.42/69.47 inference(scs_inference,[],[2739,2731,2760,2762,164,162,149,223,158])).
% 69.42/69.47 cnf(2815,plain,
% 69.42/69.47 (P10(x28151,x28152,a1,a14,x28151,x28152,a17,a16)),
% 69.42/69.47 inference(scs_inference,[],[2739,2731,2750,2760,2762,2693,2715,164,162,149,223,158,150,163,252,251])).
% 69.42/69.47 cnf(2819,plain,
% 69.42/69.47 (P10(a17,a16,x28191,x28192,a1,a14,x28191,x28192)),
% 69.42/69.47 inference(scs_inference,[],[2739,2731,2750,2760,2762,2693,2715,164,162,149,223,158,150,163,252,251,253,250])).
% 69.42/69.47 cnf(2821,plain,
% 69.42/69.47 (P7(a17,a15,a16,a16)),
% 69.42/69.47 inference(scs_inference,[],[2739,2731,2750,2760,2762,2772,2693,2715,164,162,149,223,158,150,163,252,251,253,250,234])).
% 69.42/69.47 cnf(2826,plain,
% 69.42/69.47 (P3(a1,a14,a14,a1)),
% 69.42/69.47 inference(scs_inference,[],[142,929,2739,2731,2750,2754,2760,2762,2772,2693,2715,164,162,149,223,158,150,163,252,251,253,250,234,260,178])).
% 69.42/69.47 cnf(2828,plain,
% 69.42/69.47 (P3(a14,a1,a14,a1)),
% 69.42/69.47 inference(scs_inference,[],[142,929,2739,2731,2750,2766,2754,2760,2762,2772,2693,2715,164,162,149,223,158,150,163,252,251,253,250,234,260,178,238])).
% 69.42/69.47 cnf(2833,plain,
% 69.42/69.47 (P7(a15,a17,a16,a16)),
% 69.42/69.47 inference(scs_inference,[],[142,929,2739,2731,2750,2766,2754,2760,2762,2772,2693,2715,2785,164,162,149,223,158,150,163,252,251,253,250,234,260,178,238,239,167])).
% 69.42/69.47 cnf(2835,plain,
% 69.42/69.47 (P7(a17,a16,a15,a16)),
% 69.42/69.47 inference(scs_inference,[],[142,929,2739,2731,2750,2766,2754,2760,2762,2772,2693,2715,2785,164,162,149,223,158,150,163,252,251,253,250,234,260,178,238,239,167,168])).
% 69.42/69.47 cnf(2837,plain,
% 69.42/69.47 (P7(a17,a16,a16,a15)),
% 69.42/69.47 inference(scs_inference,[],[142,929,2739,2731,2750,2766,2754,2760,2762,2772,2693,2715,2785,164,162,149,223,158,150,163,252,251,253,250,234,260,178,238,239,167,168,169])).
% 69.42/69.47 cnf(2841,plain,
% 69.42/69.47 (P3(a17,a16,a14,a1)),
% 69.42/69.47 inference(scs_inference,[],[142,929,2739,2731,2750,2766,2754,2760,2762,2772,2693,2715,2785,164,162,149,223,158,150,163,252,251,253,250,234,260,178,238,239,167,168,169,222,161])).
% 69.42/69.47 cnf(2852,plain,
% 69.42/69.47 (P7(a15,a16,a17,a16)),
% 69.42/69.47 inference(scs_inference,[],[2833,168])).
% 69.42/69.47 cnf(2854,plain,
% 69.42/69.47 (P7(a15,a16,a16,a17)),
% 69.42/69.47 inference(scs_inference,[],[2833,168,169])).
% 69.42/69.47 cnf(2856,plain,
% 69.42/69.47 (P7(a16,a17,a15,a16)),
% 69.42/69.47 inference(scs_inference,[],[2833,2835,168,169,167])).
% 69.42/69.47 cnf(2858,plain,
% 69.42/69.47 (P10(a15,a17,a15,a16,a16,a17,a16,a16)),
% 69.42/69.47 inference(scs_inference,[],[2833,2835,168,169,167,222])).
% 69.42/69.47 cnf(2862,plain,
% 69.42/69.47 (P10(a17,a16,x28621,x28622,a16,a17,x28621,x28622)),
% 69.42/69.47 inference(scs_inference,[],[2793,2790,2833,2835,168,169,167,222,164,223])).
% 69.42/69.47 cnf(2864,plain,
% 69.42/69.47 (P4(a17,a16,a17)),
% 69.42/69.47 inference(scs_inference,[],[2793,2790,2807,2833,2835,168,169,167,222,164,223,149])).
% 69.42/69.47 cnf(2868,plain,
% 69.42/69.47 (P4(a14,a1,a1)),
% 69.42/69.47 inference(scs_inference,[],[2793,2790,2826,2807,2828,2833,2835,168,169,167,222,164,223,149,161,158])).
% 69.42/69.47 cnf(2872,plain,
% 69.42/69.47 (P4(a14,a14,a1)),
% 69.42/69.47 inference(scs_inference,[],[2793,2790,2826,2803,2807,2828,2833,2835,168,169,167,222,164,223,149,161,158,162,150])).
% 69.42/69.47 cnf(2876,plain,
% 69.42/69.47 (P10(a17,a16,x28761,x28762,a14,a1,x28761,x28762)),
% 69.42/69.47 inference(scs_inference,[],[2793,2790,2826,2770,2803,2807,2828,2833,2835,2745,168,169,167,222,164,223,149,161,158,162,150,163,252])).
% 69.42/69.47 cnf(2878,plain,
% 69.42/69.47 (P10(a1,a14,x28781,x28782,a16,a17,x28782,x28781)),
% 69.42/69.47 inference(scs_inference,[],[2793,2790,2826,2764,2770,2803,2807,2828,2833,2835,2745,168,169,167,222,164,223,149,161,158,162,150,163,252,251])).
% 69.42/69.47 cnf(2882,plain,
% 69.42/69.47 (P10(x28821,x28822,a16,a17,x28822,x28821,a1,a14)),
% 69.42/69.47 inference(scs_inference,[],[2793,2790,2826,2764,2770,2803,2807,2828,2833,2835,2745,168,169,167,222,164,223,149,161,158,162,150,163,252,251,253,250])).
% 69.42/69.47 cnf(2884,plain,
% 69.42/69.47 (P7(a15,a16,a16,a16)),
% 69.42/69.47 inference(scs_inference,[],[2793,2790,2826,2764,2770,2803,2807,2821,2828,2833,2835,2745,168,169,167,222,164,223,149,161,158,162,150,163,252,251,253,250,183])).
% 69.42/69.47 cnf(2888,plain,
% 69.42/69.47 (P1(f11(a15,a17,a16,a16,a17),a15,a16,a17)),
% 69.42/69.47 inference(scs_inference,[],[2793,2790,2826,2764,2770,2803,2807,2821,2828,2833,2835,2745,145,168,169,167,222,164,223,149,161,158,162,150,163,252,251,253,250,183,195,196])).
% 69.42/69.47 cnf(2893,plain,
% 69.42/69.47 (~P1(a14,a17,a14,f4(a1,a14,a16))),
% 69.42/69.47 inference(scs_inference,[],[938,2793,2790,2826,2764,2770,2803,2807,2821,2828,2833,2835,2745,2780,2697,305,145,168,169,167,222,164,223,149,161,158,162,150,163,252,251,253,250,183,195,196,260,178])).
% 69.42/69.47 cnf(2895,plain,
% 69.42/69.47 (P1(a17,a16,a15,a16)),
% 69.42/69.47 inference(scs_inference,[],[142,938,2793,2790,2826,2764,2770,2819,2803,2807,2821,2828,2833,2835,2745,2780,2697,305,145,168,169,167,222,164,223,149,161,158,162,150,163,252,251,253,250,183,195,196,260,178,239])).
% 69.42/69.47 cnf(2900,plain,
% 69.42/69.47 (P3(x29001,x29002,x29002,x29001)),
% 69.42/69.47 inference(scs_inference,[],[142,938,2793,2790,2826,2764,2770,2819,2803,2807,2821,2828,2833,2835,2745,2780,2697,305,145,319,168,169,167,222,164,223,149,161,158,162,150,163,252,251,253,250,183,195,196,260,178,239,174,238])).
% 69.42/69.47 cnf(2908,plain,
% 69.42/69.47 (P9(a17,a17,a16,a17,a17,a17,a16,a17)),
% 69.42/69.47 inference(scs_inference,[],[142,938,2793,2790,2826,2764,2770,2819,2803,2807,2821,2828,2833,2835,2745,2780,2697,305,145,319,168,169,167,222,164,223,149,161,158,162,150,163,252,251,253,250,183,195,196,260,178,239,174,238,226,204,205,255])).
% 69.42/69.47 cnf(2910,plain,
% 69.42/69.47 (P9(a17,a16,a17,a17,a16,a17,a17,a17)),
% 69.42/69.47 inference(scs_inference,[],[142,938,2793,2790,2826,2764,2770,2819,2803,2807,2821,2828,2833,2835,2745,2780,2697,305,145,319,168,169,167,222,164,223,149,161,158,162,150,163,252,251,253,250,183,195,196,260,178,239,174,238,226,204,205,255,256])).
% 69.42/69.47 cnf(2912,plain,
% 69.42/69.47 (P9(a16,a17,a16,a17,a17,a17,a17,a17)),
% 69.42/69.47 inference(scs_inference,[],[142,938,2793,2790,2826,2764,2770,2819,2803,2807,2821,2828,2833,2835,2745,2780,2697,305,145,319,168,169,167,222,164,223,149,161,158,162,150,163,252,251,253,250,183,195,196,260,178,239,174,238,226,204,205,255,256,257])).
% 69.42/69.47 cnf(2916,plain,
% 69.42/69.47 (P9(a16,a17,a17,a17,a17,a16,a17,a17)),
% 69.42/69.47 inference(scs_inference,[],[2910,254])).
% 69.42/69.47 cnf(2920,plain,
% 69.42/69.47 (P7(a16,a15,a17,a16)),
% 69.42/69.47 inference(scs_inference,[],[2856,2908,2910,254,257,168])).
% 69.42/69.47 cnf(2924,plain,
% 69.42/69.47 (P7(a16,a17,a16,a15)),
% 69.42/69.47 inference(scs_inference,[],[2856,2908,2910,254,257,168,255,169])).
% 69.42/69.47 cnf(2926,plain,
% 69.42/69.47 (P9(a17,a16,a16,a17,a17,a17,a17,a17)),
% 69.42/69.47 inference(scs_inference,[],[2856,2908,2910,2912,254,257,168,255,169,256])).
% 69.42/69.47 cnf(2928,plain,
% 69.42/69.47 (P7(a16,a15,a16,a17)),
% 69.42/69.47 inference(scs_inference,[],[2854,2856,2908,2910,2912,254,257,168,255,169,256,167])).
% 69.42/69.47 cnf(2930,plain,
% 69.42/69.47 (P10(a16,a17,a16,a16,a15,a17,a15,a16)),
% 69.42/69.47 inference(scs_inference,[],[2837,2854,2856,2908,2910,2912,254,257,168,255,169,256,167,222])).
% 69.42/69.47 cnf(2932,plain,
% 69.42/69.47 (P4(a1,a14,a1)),
% 69.42/69.47 inference(scs_inference,[],[2837,2854,2856,2868,2908,2910,2912,254,257,168,255,169,256,167,222,149])).
% 69.42/69.47 cnf(2934,plain,
% 69.42/69.47 (P1(a17,a16,a16,a15)),
% 69.42/69.47 inference(scs_inference,[],[2837,2854,2856,2868,2895,2908,2910,2912,254,257,168,255,169,256,167,222,149,164])).
% 69.42/69.47 cnf(2936,plain,
% 69.42/69.47 (P3(x29361,x29362,x29361,x29362)),
% 69.42/69.47 inference(scs_inference,[],[2900,2837,2854,2856,2868,2895,2908,2910,2912,254,257,168,255,169,256,167,222,149,164,162])).
% 69.42/69.47 cnf(2938,plain,
% 69.42/69.47 (P10(x29381,x29382,x29383,x29384,x29382,x29381,x29383,x29384)),
% 69.42/69.47 inference(scs_inference,[],[2900,2837,2854,2856,2868,2895,2908,2910,2912,254,257,168,255,169,256,167,222,149,164,162,223])).
% 69.42/69.47 cnf(2940,plain,
% 69.42/69.47 (P4(a17,a17,a16)),
% 69.42/69.47 inference(scs_inference,[],[2900,2837,2854,2856,2864,2868,2895,2908,2910,2912,254,257,168,255,169,256,167,222,149,164,162,223,150])).
% 69.42/69.47 cnf(2942,plain,
% 69.42/69.47 (P4(x29421,x29421,x29421)),
% 69.42/69.47 inference(scs_inference,[],[2900,2837,2854,2856,2864,2868,2895,2908,2910,2912,254,257,168,255,169,256,167,222,149,164,162,223,150,158])).
% 69.42/69.47 cnf(2943,plain,
% 69.42/69.47 (P3(x29431,x29432,x29432,x29431)),
% 69.42/69.47 inference(rename_variables,[],[2900])).
% 69.42/69.47 cnf(2945,plain,
% 69.42/69.47 (P1(a15,a16,a17,a16)),
% 69.42/69.47 inference(scs_inference,[],[2900,2837,2854,2856,2864,2868,2895,2908,2910,2912,254,257,168,255,169,256,167,222,149,164,162,223,150,158,163])).
% 69.42/69.47 cnf(2947,plain,
% 69.42/69.47 (P10(a14,a1,x29471,x29472,a16,a17,x29472,x29471)),
% 69.42/69.47 inference(scs_inference,[],[2900,2837,2878,2854,2856,2864,2868,2895,2908,2910,2912,254,257,168,255,169,256,167,222,149,164,162,223,150,158,163,252])).
% 69.42/69.47 cnf(2955,plain,
% 69.42/69.47 (P9(a16,a17,a16,a17,a16,a17,a16,a17)),
% 69.42/69.47 inference(scs_inference,[],[2900,2837,2862,2878,2854,2856,2864,2868,2895,2908,2910,2912,254,257,168,255,169,256,167,222,149,164,162,223,150,158,163,252,251,253,250,261])).
% 69.42/69.47 cnf(2957,plain,
% 69.42/69.47 (P2(f7(a17,a15,a16),a17,a15,a16)),
% 69.42/69.47 inference(scs_inference,[],[2900,2837,2862,2878,2854,2856,2864,2868,2895,2908,2910,2912,2821,254,257,168,255,169,256,167,222,149,164,162,223,150,158,163,252,251,253,250,261,189])).
% 69.42/69.47 cnf(2959,plain,
% 69.42/69.47 (P7(a14,a1,a14,a14)),
% 69.42/69.47 inference(scs_inference,[],[2900,2837,2862,2878,2854,2856,2864,2868,2872,2895,2908,2910,2912,2821,254,257,168,255,169,256,167,222,149,164,162,223,150,158,163,252,251,253,250,261,189,234])).
% 69.42/69.47 cnf(2963,plain,
% 69.42/69.47 (~P1(a17,a14,a14,f4(a1,a14,a16))),
% 69.42/69.47 inference(scs_inference,[],[2900,2943,2837,2862,2878,2854,2856,2864,2868,2872,2895,2908,2910,2912,2893,2821,2735,254,257,168,255,169,256,167,222,149,164,162,223,150,158,163,252,251,253,250,261,189,234,196,180])).
% 69.42/69.47 cnf(2964,plain,
% 69.42/69.47 (P3(x29641,x29642,x29642,x29641)),
% 69.42/69.47 inference(rename_variables,[],[2900])).
% 69.42/69.47 cnf(2972,plain,
% 69.42/69.47 (P4(f3(a15,a17,a16),a16,a17)),
% 69.42/69.47 inference(scs_inference,[],[2900,2943,2837,2862,2878,2854,2856,2864,2868,2872,2895,2908,2910,2912,2893,2821,2735,254,257,168,255,169,256,167,222,149,164,162,223,150,158,163,252,251,253,250,261,189,234,196,180,195,176,187,175])).
% 69.42/69.47 cnf(2976,plain,
% 69.42/69.47 (P3(f11(a15,a17,a16,a16,a17),a15,a15,a16)),
% 69.42/69.47 inference(scs_inference,[],[2900,2943,2837,2862,2878,2854,2856,2864,2868,2872,2895,2908,2910,2912,2893,2888,2821,2719,2735,254,257,168,255,169,256,167,222,149,164,162,223,150,158,163,252,251,253,250,261,189,234,196,180,195,176,187,175,188,178])).
% 69.42/69.47 cnf(2982,plain,
% 69.42/69.47 (P9(a14,a1,a1,a1,a14,a1,a1,a1)),
% 69.42/69.47 inference(scs_inference,[],[2900,2943,2964,2837,2862,2878,2799,2854,2856,2864,2868,2872,2895,2908,2910,2912,2893,2888,2821,2719,284,2735,254,257,168,255,169,256,167,222,149,164,162,223,150,158,163,252,251,253,250,261,189,234,196,180,195,176,187,175,188,178,238,239,226])).
% 69.42/69.47 cnf(2983,plain,
% 69.42/69.47 (P3(x29831,x29832,x29832,x29831)),
% 69.42/69.47 inference(rename_variables,[],[2900])).
% 69.42/69.47 cnf(2986,plain,
% 69.42/69.47 (P3(x29861,x29862,x29862,x29861)),
% 69.42/69.47 inference(rename_variables,[],[2900])).
% 69.42/69.47 cnf(2991,plain,
% 69.42/69.47 (P3(a15,a16,f11(a15,a17,a16,a16,a17),a15)),
% 69.42/69.47 inference(scs_inference,[],[2900,2943,2964,2983,2986,2837,2862,2878,2799,2854,2856,2864,2868,2872,2895,2908,2910,2912,2893,2888,2821,2719,284,2735,254,257,168,255,169,256,167,222,149,164,162,223,150,158,163,252,251,253,250,261,189,234,196,180,195,176,187,175,188,178,238,239,226,204,205,161])).
% 69.42/69.47 cnf(3000,plain,
% 69.42/69.47 (P9(a16,a17,a17,a16,a17,a17,a17,a17)),
% 69.42/69.47 inference(scs_inference,[],[2916,257])).
% 69.42/69.47 cnf(3002,plain,
% 69.42/69.47 (P9(a17,a17,a16,a17,a17,a17,a17,a16)),
% 69.42/69.47 inference(scs_inference,[],[2916,257,255])).
% 69.42/69.47 cnf(3004,plain,
% 69.42/69.47 (P7(a16,a16,a17,a15)),
% 69.42/69.47 inference(scs_inference,[],[2924,2916,257,255,168])).
% 69.42/69.47 cnf(3008,plain,
% 69.42/69.47 (P7(a16,a16,a15,a17)),
% 69.42/69.47 inference(scs_inference,[],[2924,2916,2926,257,255,168,254,169])).
% 69.42/69.47 cnf(3010,plain,
% 69.42/69.47 (P9(a17,a16,a17,a17,a17,a16,a17,a17)),
% 69.42/69.47 inference(scs_inference,[],[2924,2916,2926,257,255,168,254,169,256])).
% 69.42/69.47 cnf(3012,plain,
% 69.42/69.47 (P7(a16,a15,a16,a16)),
% 69.42/69.47 inference(scs_inference,[],[2924,2884,2916,2926,257,255,168,254,169,256,167])).
% 69.42/69.47 cnf(3020,plain,
% 69.42/69.47 (P3(f11(a15,a17,a16,a16,a17),a15,a16,a15)),
% 69.42/69.47 inference(scs_inference,[],[2852,2924,2884,2916,2926,2717,2778,2976,257,255,168,254,169,256,167,222,149,164,162])).
% 69.42/69.47 cnf(3026,plain,
% 69.42/69.47 (P10(x30261,x30262,x30263,x30264,x30261,x30262,x30263,x30264)),
% 69.42/69.47 inference(scs_inference,[],[2936,2852,2924,2884,2916,2926,2932,2717,2778,2976,257,255,168,254,169,256,167,222,149,164,162,161,150,223])).
% 69.42/69.47 cnf(3028,plain,
% 69.42/69.47 (P4(x30281,x30282,x30282)),
% 69.42/69.47 inference(scs_inference,[],[2936,2852,2924,2884,2916,2926,2932,2717,2778,2976,257,255,168,254,169,256,167,222,149,164,162,161,150,223,158])).
% 69.42/69.47 cnf(3030,plain,
% 69.42/69.47 (P1(a16,a15,a17,a16)),
% 69.42/69.47 inference(scs_inference,[],[2936,2852,2924,2934,2884,2916,2926,2932,2717,2778,2976,257,255,168,254,169,256,167,222,149,164,162,161,150,223,158,163])).
% 69.42/69.47 cnf(3034,plain,
% 69.42/69.47 (P10(x30341,x30342,x30343,x30344,x30341,x30342,x30344,x30343)),
% 69.42/69.47 inference(scs_inference,[],[2936,2938,2858,2852,2924,2934,2884,2916,2926,2932,2717,2778,2976,257,255,168,254,169,256,167,222,149,164,162,161,150,223,158,163,252,251])).
% 69.42/69.47 cnf(3036,plain,
% 69.42/69.47 (P10(x30361,x30362,x30362,x30361,x30363,x30364,x30363,x30364)),
% 69.42/69.47 inference(scs_inference,[],[2936,2938,2858,2852,2924,2934,2884,2916,2926,2932,2717,2778,2976,257,255,168,254,169,256,167,222,149,164,162,161,150,223,158,163,252,251,253])).
% 69.42/69.47 cnf(3040,plain,
% 69.42/69.47 (P7(x30401,x30401,x30401,x30401)),
% 69.42/69.47 inference(scs_inference,[],[2942,2936,2938,2858,2852,2924,2934,2947,2884,2916,2926,2932,2717,2778,2976,257,255,168,254,169,256,167,222,149,164,162,161,150,223,158,163,252,251,253,250,234])).
% 69.42/69.47 cnf(3041,plain,
% 69.42/69.47 (P10(x30411,x30412,x30413,x30414,x30412,x30411,x30413,x30414)),
% 69.42/69.47 inference(rename_variables,[],[2938])).
% 69.42/69.47 cnf(3046,plain,
% 69.42/69.47 (P4(x30461,x30461,x30461)),
% 69.42/69.47 inference(rename_variables,[],[2942])).
% 69.42/69.47 cnf(3054,plain,
% 69.42/69.47 (P1(a17,f4(a15,a17,a16),a16,a15)),
% 69.42/69.47 inference(scs_inference,[],[2942,2936,2938,2858,2852,2924,2934,2947,2884,2916,2926,2932,2940,2945,2717,2778,2976,2895,145,257,255,168,254,169,256,167,222,149,164,162,161,150,223,158,163,252,251,253,250,234,176,196,175,187,195,188])).
% 69.42/69.47 cnf(3056,plain,
% 69.42/69.47 (~P1(a14,a17,a14,f3(a14,a1,a16))),
% 69.42/69.47 inference(scs_inference,[],[2942,2936,2938,2858,2852,2924,2934,2947,2884,2916,2926,2932,2940,2945,2717,2776,2778,2976,305,2895,145,257,255,168,254,169,256,167,222,149,164,162,161,150,223,158,163,252,251,253,250,234,176,196,175,187,195,188,178])).
% 69.42/69.47 cnf(3059,plain,
% 69.42/69.47 (P10(x30591,x30592,x30593,x30594,x30592,x30591,x30593,x30594)),
% 69.42/69.47 inference(rename_variables,[],[2938])).
% 69.42/69.47 cnf(3061,plain,
% 69.42/69.47 (P1(a16,a15,a16,a17)),
% 69.42/69.47 inference(scs_inference,[],[2942,2936,2938,3041,2858,2852,2924,2934,2882,2947,2884,2916,2926,2932,2940,2945,2717,2776,2778,2976,2703,305,2895,145,257,255,168,254,169,256,167,222,149,164,162,161,150,223,158,163,252,251,253,250,234,176,196,175,187,195,188,178,260,239])).
% 69.42/69.47 cnf(3064,plain,
% 69.42/69.47 (P6(a15,a15,a15,a15)),
% 69.42/69.47 inference(scs_inference,[],[2942,2936,2938,3041,3059,2858,2852,2924,2934,2882,2947,2884,2916,2926,2932,2940,2945,2717,2776,2778,2976,2703,305,2895,145,257,255,168,254,169,256,167,222,149,164,162,161,150,223,158,163,252,251,253,250,234,176,196,175,187,195,188,178,260,239,249])).
% 69.42/69.47 cnf(3065,plain,
% 69.42/69.48 (P10(x30651,x30652,x30653,x30654,x30652,x30651,x30653,x30654)),
% 69.42/69.48 inference(rename_variables,[],[2938])).
% 69.42/69.48 cnf(3070,plain,
% 69.42/69.48 (P4(x30701,x30701,x30701)),
% 69.42/69.48 inference(rename_variables,[],[2942])).
% 69.42/69.48 cnf(3071,plain,
% 69.42/69.48 (P3(x30711,x30712,x30711,x30712)),
% 69.42/69.48 inference(rename_variables,[],[2936])).
% 69.42/69.48 cnf(3074,plain,
% 69.42/69.48 (P4(x30741,x30741,x30741)),
% 69.42/69.48 inference(rename_variables,[],[2942])).
% 69.42/69.48 cnf(3075,plain,
% 69.42/69.48 (P3(x30751,x30752,x30751,x30752)),
% 69.42/69.48 inference(rename_variables,[],[2936])).
% 69.42/69.48 cnf(3077,plain,
% 69.42/69.48 (P2(a15,a15,a15,a15)),
% 69.42/69.48 inference(scs_inference,[],[2942,3046,3070,2936,3071,2938,3041,3059,2858,2852,2924,2934,2882,2947,2884,2916,2926,2932,2940,2945,2717,2776,2778,2976,2703,2807,305,2895,145,257,255,168,254,169,256,167,222,149,164,162,161,150,223,158,163,252,251,253,250,234,176,196,175,187,195,188,178,260,239,249,204,205,182])).
% 69.42/69.48 cnf(3085,plain,
% 69.42/69.48 (P3(f26(a17,a16,a15,a15,a15),a15,a17,a16)),
% 69.42/69.48 inference(scs_inference,[],[142,2942,3046,3070,2936,3071,2938,3041,3059,2858,2852,2924,2934,2882,2947,2884,2916,2926,2932,2940,2945,2717,2776,2778,2976,2703,2807,305,2895,145,257,255,168,254,169,256,167,222,149,164,162,161,150,223,158,163,252,251,253,250,234,176,196,175,187,195,188,178,260,239,249,204,205,182,191,197,198,199])).
% 69.42/69.48 cnf(3088,plain,
% 69.42/69.48 (P10(x30881,x30882,x30883,x30884,x30882,x30881,x30883,x30884)),
% 69.42/69.48 inference(rename_variables,[],[2938])).
% 69.42/69.48 cnf(3090,plain,
% 69.42/69.48 (P1(a15,a15,a15,a15)),
% 69.42/69.48 inference(scs_inference,[],[142,2942,3046,3070,2936,3071,2938,3041,3059,3065,2858,2852,2924,2934,2882,2947,2884,2916,2926,2932,2940,2945,2717,2776,2778,2976,2703,2807,305,2895,145,257,255,168,254,169,256,167,222,149,164,162,161,150,223,158,163,252,251,253,250,234,176,196,175,187,195,188,178,260,239,249,204,205,182,191,197,198,199,243,179])).
% 69.42/69.48 cnf(3094,plain,
% 69.42/69.48 (P3(a15,f11(a15,a17,a16,a16,a17),a15,a16)),
% 69.42/69.48 inference(scs_inference,[],[142,2942,3046,3070,2936,3071,2938,3041,3059,3065,3088,2858,2852,2924,2934,2882,2947,2884,2916,2926,2932,2940,2945,2717,2776,2778,2976,2703,2807,305,2895,145,257,255,168,254,169,256,167,222,149,164,162,161,150,223,158,163,252,251,253,250,234,176,196,175,187,195,188,178,260,239,249,204,205,182,191,197,198,199,243,179,189,238])).
% 69.42/69.48 cnf(3095,plain,
% 69.42/69.48 (P10(x30951,x30952,x30953,x30954,x30952,x30951,x30953,x30954)),
% 69.42/69.48 inference(rename_variables,[],[2938])).
% 69.42/69.48 cnf(3097,plain,
% 69.42/69.48 (P5(a15,a15,a15)),
% 69.42/69.48 inference(scs_inference,[],[142,2942,3046,3070,3074,2936,3071,2938,3041,3059,3065,3088,3095,2858,2852,2924,2934,2882,2947,2884,2916,2926,2932,2940,2945,2717,2776,2778,2976,2703,2807,305,2895,145,257,255,168,254,169,256,167,222,149,164,162,161,150,223,158,163,252,251,253,250,234,176,196,175,187,195,188,178,260,239,249,204,205,182,191,197,198,199,243,179,189,238,237])).
% 69.42/69.48 cnf(3098,plain,
% 69.42/69.48 (P4(x30981,x30981,x30981)),
% 69.42/69.48 inference(rename_variables,[],[2942])).
% 69.42/69.48 cnf(3104,plain,
% 69.42/69.48 (P5(f20(a15,x31041),a15,x31041)),
% 69.42/69.48 inference(scs_inference,[],[142,2942,3046,3070,3074,3098,2936,3071,3075,2938,3041,3059,3065,3088,3095,2858,2852,2924,2934,2882,2947,2884,2916,2926,2932,2940,2945,2717,2776,2778,2976,2703,2807,305,2895,145,257,255,168,254,169,256,167,222,149,164,162,161,150,223,158,163,252,251,253,250,234,176,196,175,187,195,188,178,260,239,249,204,205,182,191,197,198,199,243,179,189,238,237,190,157])).
% 69.42/69.48 cnf(3108,plain,
% 69.42/69.48 (P6(f20(a15,x31081),a15,f20(a15,x31081),x31081)),
% 69.42/69.48 inference(scs_inference,[],[142,2942,3046,3070,3074,3098,2936,3071,3075,2938,3041,3059,3065,3088,3095,2858,2852,2924,2934,2882,2947,2884,2916,2926,2932,2940,2945,2717,2776,2778,2976,2703,2807,305,2895,145,257,255,168,254,169,256,167,222,149,164,162,161,150,223,158,163,252,251,253,250,234,176,196,175,187,195,188,178,260,239,249,204,205,182,191,197,198,199,243,179,189,238,237,190,157,154])).
% 69.42/69.48 cnf(3112,plain,
% 69.42/69.48 (P5(f20(a15,x31121),x31121,a15)),
% 69.42/69.48 inference(scs_inference,[],[142,2942,3046,3070,3074,3098,2936,3071,3075,2938,3041,3059,3065,3088,3095,2858,2852,2924,2934,2882,2947,2884,2916,2926,2932,2940,2945,2717,2776,2778,2976,2703,2807,305,2895,145,257,255,168,254,169,256,167,222,149,164,162,161,150,223,158,163,252,251,253,250,234,176,196,175,187,195,188,178,260,239,249,204,205,182,191,197,198,199,243,179,189,238,237,190,157,154,224,152])).
% 69.42/69.48 cnf(3114,plain,
% 69.42/69.48 (P1(f6(a15,a15,a15,a15),a15,a15,a15)),
% 69.42/69.48 inference(scs_inference,[],[142,2942,3046,3070,3074,3098,2936,3071,3075,2938,3041,3059,3065,3088,3095,2858,2852,2924,2934,2882,2947,2884,2916,2926,2932,2940,2945,2717,2776,2778,2976,2703,2807,305,2895,145,257,255,168,254,169,256,167,222,149,164,162,161,150,223,158,163,252,251,253,250,234,176,196,175,187,195,188,178,260,239,249,204,205,182,191,197,198,199,243,179,189,238,237,190,157,154,224,152,185])).
% 69.42/69.48 cnf(3116,plain,
% 69.42/69.48 (P6(a15,a15,f26(a17,a16,a15,a15,a15),a15)),
% 69.42/69.48 inference(scs_inference,[],[142,2942,3046,3070,3074,3098,2936,3071,3075,2938,3041,3059,3065,3088,3095,2858,2852,2924,2934,2882,2947,2884,2916,2926,2932,2940,2945,2717,2776,2778,2976,2703,2807,305,2895,145,257,255,168,254,169,256,167,222,149,164,162,161,150,223,158,163,252,251,253,250,234,176,196,175,187,195,188,178,260,239,249,204,205,182,191,197,198,199,243,179,189,238,237,190,157,154,224,152,185,166])).
% 69.42/69.48 cnf(3118,plain,
% 69.42/69.48 (P4(f20(a15,x31181),a15,x31181)),
% 69.42/69.48 inference(scs_inference,[],[142,2942,3046,3070,3074,3098,2936,3071,3075,2938,3041,3059,3065,3088,3095,2858,2852,2924,2934,2882,2947,2884,2916,2926,2932,2940,2945,2717,2776,2778,2976,2703,2807,305,2895,145,257,255,168,254,169,256,167,222,149,164,162,161,150,223,158,163,252,251,253,250,234,176,196,175,187,195,188,178,260,239,249,204,205,182,191,197,198,199,243,179,189,238,237,190,157,154,224,152,185,166,151])).
% 69.42/69.48 cnf(3122,plain,
% 69.42/69.48 (P3(a15,a15,a15,f26(a17,a16,a15,a15,a15))),
% 69.42/69.48 inference(scs_inference,[],[142,2942,3046,3070,3074,3098,2936,3071,3075,2938,3041,3059,3065,3088,3095,2858,2852,2924,2934,2882,2947,2884,2916,2926,2932,2940,2945,2717,2776,2778,2976,2703,2807,305,2895,145,257,255,168,254,169,256,167,222,149,164,162,161,150,223,158,163,252,251,253,250,234,176,196,175,187,195,188,178,260,239,249,204,205,182,191,197,198,199,243,179,189,238,237,190,157,154,224,152,185,166,151,165,231])).
% 69.42/69.48 cnf(3126,plain,
% 69.42/69.48 (~P2(f20(a15,a17),a15,a14,a17)),
% 69.42/69.48 inference(scs_inference,[],[3118,325])).
% 69.42/69.48 cnf(3133,plain,
% 69.42/69.48 (P6(f20(a15,x31331),x31331,f20(a15,x31331),a15)),
% 69.42/69.48 inference(scs_inference,[],[3002,3108,3112,3118,325,224,257,154])).
% 69.42/69.48 cnf(3137,plain,
% 69.42/69.48 (P9(a1,a1,a14,a1,a1,a1,a14,a1)),
% 69.42/69.48 inference(scs_inference,[],[3002,2959,2982,3108,3112,3118,325,224,257,154,168,255])).
% 69.42/69.48 cnf(3145,plain,
% 69.42/69.48 (P9(a17,a16,a16,a17,a16,a17,a16,a17)),
% 69.42/69.48 inference(scs_inference,[],[3002,2955,2959,2982,3108,3112,3118,325,224,257,154,168,255,166,151,169,256])).
% 69.42/69.48 cnf(3149,plain,
% 69.42/69.48 (P10(a17,a16,a17,a15,a16,a16,a16,a15)),
% 69.42/69.48 inference(scs_inference,[],[2920,3002,2955,2959,2982,3108,3112,3118,3116,325,224,257,154,168,255,166,151,169,256,165,222])).
% 69.42/69.48 cnf(3155,plain,
% 69.42/69.48 (P4(x31551,x31552,x31551)),
% 69.42/69.48 inference(scs_inference,[],[3028,2920,3002,2955,2959,2982,3054,3108,3112,3118,3116,325,224,257,154,168,255,166,151,169,256,165,222,164,167,149])).
% 69.42/69.48 cnf(3159,plain,
% 69.42/69.48 (P3(a15,a16,a15,f11(a15,a17,a16,a16,a17))),
% 69.42/69.48 inference(scs_inference,[],[3028,2920,3002,2955,2959,2982,2991,3054,3108,3112,3118,3122,3116,325,224,257,154,168,255,166,151,169,256,165,222,164,167,149,161,162])).
% 69.42/69.48 cnf(3161,plain,
% 69.42/69.48 (P10(a15,a16,x31611,x31612,f11(a15,a17,a16,a16,a17),a15,x31611,x31612)),
% 69.42/69.48 inference(scs_inference,[],[3028,2920,3002,2955,2959,2982,2991,3054,3108,3112,3118,3122,3116,325,224,257,154,168,255,166,151,169,256,165,222,164,167,149,161,162,223])).
% 69.42/69.48 cnf(3167,plain,
% 69.42/69.48 (P1(a16,a17,a16,a15)),
% 69.42/69.48 inference(scs_inference,[],[3028,2920,3002,3061,2955,2959,2982,2774,2991,3054,3108,3112,3118,3122,3116,325,224,257,154,168,255,166,151,169,256,165,222,164,167,149,161,162,223,150,158,163])).
% 69.42/69.48 cnf(3169,plain,
% 69.42/69.48 (P10(x31691,x31692,x31693,x31694,x31692,x31691,x31694,x31693)),
% 69.42/69.48 inference(scs_inference,[],[3034,3028,2920,3002,3061,2955,2959,2982,2774,2991,3054,3108,3112,3118,3122,3116,325,224,257,154,168,255,166,151,169,256,165,222,164,167,149,161,162,223,150,158,163,252])).
% 69.42/69.48 cnf(3171,plain,
% 69.42/69.48 (P10(a16,a16,a16,a17,a15,a16,a15,a17)),
% 69.42/69.48 inference(scs_inference,[],[3034,3028,2920,2930,3002,3061,2955,2959,2982,2774,2991,3054,3108,3112,3118,3122,3116,325,224,257,154,168,255,166,151,169,256,165,222,164,167,149,161,162,223,150,158,163,252,251])).
% 69.42/69.48 cnf(3173,plain,
% 69.42/69.48 (P10(x31731,x31732,x31731,x31732,x31733,x31734,x31733,x31734)),
% 69.42/69.48 inference(scs_inference,[],[3026,3034,3028,2920,2930,3002,3061,2955,2959,2982,2774,2991,3054,3108,3112,3118,3122,3116,325,224,257,154,168,255,166,151,169,256,165,222,164,167,149,161,162,223,150,158,163,252,251,253])).
% 69.42/69.48 cnf(3175,plain,
% 69.42/69.48 (P10(x31751,x31752,x31751,x31752,x31753,x31754,x31754,x31753)),
% 69.42/69.48 inference(scs_inference,[],[3026,3034,3036,3028,2920,2930,3002,3061,2955,2959,2982,2774,2991,3054,3108,3112,3118,3122,3116,325,224,257,154,168,255,166,151,169,256,165,222,164,167,149,161,162,223,150,158,163,252,251,253,250])).
% 69.42/69.48 cnf(3177,plain,
% 69.42/69.48 (P6(f20(a15,x31771),x31771,f20(a15,x31771),x31771)),
% 69.42/69.48 inference(scs_inference,[],[3026,3034,3036,3028,2920,2930,3002,3061,2955,2959,2982,2774,2991,3054,3108,3112,3118,3122,3116,325,224,257,154,168,255,166,151,169,256,165,222,164,167,149,161,162,223,150,158,163,252,251,253,250,181])).
% 69.42/69.48 cnf(3181,plain,
% 69.42/69.48 (P5(f24(a15,a15,a15,a15,a15,a15),a15,a15)),
% 69.42/69.48 inference(scs_inference,[],[3026,3034,3036,3028,2920,2930,3002,3061,2955,2959,2982,3097,2774,2991,3054,3108,3112,3118,3122,3116,325,224,257,154,168,255,166,151,169,256,165,222,164,167,149,161,162,223,150,158,163,252,251,253,250,181,221,201])).
% 69.42/69.48 cnf(3183,plain,
% 69.42/69.48 (P3(f24(a15,a15,a15,a15,a15,a15),a15,a15,a15)),
% 69.42/69.48 inference(scs_inference,[],[3026,3034,3036,3028,2920,2930,3002,3061,2955,2959,2982,3097,2774,2991,3054,3108,3112,3118,3122,3116,325,224,257,154,168,255,166,151,169,256,165,222,164,167,149,161,162,223,150,158,163,252,251,253,250,181,221,201,202])).
% 69.42/69.48 cnf(3186,plain,
% 69.42/69.48 (P10(x31861,x31862,x31863,x31864,x31861,x31862,x31863,x31864)),
% 69.42/69.48 inference(rename_variables,[],[3026])).
% 69.42/69.48 cnf(3188,plain,
% 69.42/69.48 (P6(a15,a15,a15,f26(a15,a15,a15,a15,a15))),
% 69.42/69.48 inference(scs_inference,[],[3026,3034,3036,3028,2920,3090,2930,3002,3061,3064,2955,2959,2982,3097,2774,2991,3054,3108,3112,3118,3122,3116,325,224,257,154,168,255,166,151,169,256,165,222,164,167,149,161,162,223,150,158,163,252,251,253,250,181,221,201,202,244,197])).
% 69.42/69.48 cnf(3190,plain,
% 69.42/69.48 (P3(f20(a15,x31901),a15,x31901,a15)),
% 69.42/69.48 inference(scs_inference,[],[3026,3034,3036,3028,2920,3090,2930,3002,3061,3064,2955,2959,2982,3097,2774,2991,3054,3108,3104,3112,3118,3122,3116,325,224,257,154,168,255,166,151,169,256,165,222,164,167,149,161,162,223,150,158,163,252,251,253,250,181,221,201,202,244,197,156])).
% 69.42/69.48 cnf(3194,plain,
% 69.42/69.48 (P2(f20(a15,x31941),a15,x31941,x31941)),
% 69.42/69.48 inference(scs_inference,[],[3026,3034,3036,3028,2920,3090,2930,3002,3061,3064,2955,2959,2982,3097,2774,2991,3054,3108,3104,3112,3118,3122,3116,325,224,257,154,168,255,166,151,169,256,165,222,164,167,149,161,162,223,150,158,163,252,251,253,250,181,221,201,202,244,197,156,186,182])).
% 69.42/69.48 cnf(3201,plain,
% 69.42/69.48 (P10(a15,a15,a15,a15,a15,a15,a15,f20(a15,a15))),
% 69.42/69.48 inference(scs_inference,[],[3026,3034,3036,3028,2920,3090,2930,3002,3061,3064,2955,2959,2982,3077,3097,2774,2991,3054,3108,3104,3112,3118,3122,3116,325,224,257,154,168,255,166,151,169,256,165,222,164,167,149,161,162,223,150,158,163,252,251,253,250,181,221,201,202,244,197,156,186,182,174,179,225])).
% 69.42/69.48 cnf(3202,plain,
% 69.42/69.48 (P5(f20(a15,x32021),a15,x32021)),
% 69.42/69.48 inference(rename_variables,[],[3104])).
% 69.42/69.48 cnf(3210,plain,
% 69.42/69.48 (P7(x32101,x32102,x32102,x32102)),
% 69.42/69.48 inference(scs_inference,[],[3026,3186,3034,3036,3028,2920,3090,3030,2930,3002,3061,3064,2955,2959,2982,3077,3097,2774,2991,3054,3108,3104,3112,3118,3122,3116,3020,325,224,257,154,168,255,166,151,169,256,165,222,164,167,149,161,162,223,150,158,163,252,251,253,250,181,221,201,202,244,197,156,186,182,174,179,225,191,199,180,234])).
% 69.42/69.48 cnf(3211,plain,
% 69.42/69.48 (P4(x32111,x32112,x32112)),
% 69.42/69.48 inference(rename_variables,[],[3028])).
% 69.42/69.48 cnf(3212,plain,
% 69.42/69.48 (P10(x32121,x32122,x32123,x32124,x32121,x32122,x32123,x32124)),
% 69.42/69.48 inference(rename_variables,[],[3026])).
% 69.42/69.48 cnf(3214,plain,
% 69.42/69.48 (P1(f11(a15,a15,a15,x32141,x32141),a15,x32141,x32141)),
% 69.42/69.48 inference(scs_inference,[],[3026,3186,3034,3036,3028,3211,2920,3090,3030,2930,3002,3061,3064,2955,2959,2982,3077,3097,2774,2991,3054,3108,3104,3112,3118,3122,3116,3020,325,224,257,154,168,255,166,151,169,256,165,222,164,167,149,161,162,223,150,158,163,252,251,253,250,181,221,201,202,244,197,156,186,182,174,179,225,191,199,180,234,196])).
% 69.42/69.48 cnf(3215,plain,
% 69.42/69.48 (P4(x32151,x32152,x32152)),
% 69.42/69.48 inference(rename_variables,[],[3028])).
% 69.42/69.48 cnf(3227,plain,
% 69.42/69.48 (P3(a17,f4(a15,a17,a16),a17,a16)),
% 69.42/69.48 inference(scs_inference,[],[3026,3186,3034,3036,3028,3211,2920,3090,3030,2930,3002,3061,3064,2955,2959,2982,3077,3097,2774,2991,3054,3108,3104,3112,3118,3122,3116,3020,3085,2841,325,224,257,154,168,255,166,151,169,256,165,222,164,167,149,161,162,223,150,158,163,252,251,253,250,181,221,201,202,244,197,156,186,182,174,179,225,191,199,180,234,196,175,176,187,188,177,178])).
% 69.42/69.48 cnf(3229,plain,
% 69.42/69.48 (P3(f26(a17,a16,a15,a15,a15),a15,a1,a14)),
% 69.42/69.48 inference(scs_inference,[],[3026,3186,3034,3036,3028,3211,2920,3090,3030,2930,3002,3061,3064,2955,2959,2982,3077,3097,2774,2991,3054,3108,3104,3112,3118,3122,3116,3020,3085,2841,2815,325,224,257,154,168,255,166,151,169,256,165,222,164,167,149,161,162,223,150,158,163,252,251,253,250,181,221,201,202,244,197,156,186,182,174,179,225,191,199,180,234,196,175,176,187,188,177,178,238])).
% 69.42/69.48 cnf(3230,plain,
% 69.42/69.48 (P10(x32301,x32302,a1,a14,x32301,x32302,a17,a16)),
% 69.42/69.48 inference(rename_variables,[],[2815])).
% 69.42/69.48 cnf(3236,plain,
% 69.42/69.48 (P5(a15,f26(a17,a16,a15,a15,a15),a15)),
% 69.42/69.48 inference(scs_inference,[],[3026,3186,3034,3036,3028,3211,2920,3090,3030,2930,3002,3061,3064,2955,2959,2982,3077,3097,2774,2991,3054,3108,3104,3112,3118,3122,3116,3020,3085,2841,2815,325,224,257,154,168,255,166,151,169,256,165,222,164,167,149,161,162,223,150,158,163,252,251,253,250,181,221,201,202,244,197,156,186,182,174,179,225,191,199,180,234,196,175,176,187,188,177,178,238,184,193,173])).
% 69.42/69.48 cnf(3238,plain,
% 69.42/69.48 (P6(x32381,x32381,x32381,x32381)),
% 69.42/69.48 inference(scs_inference,[],[3040,3026,3186,3212,3034,3036,3028,3211,2920,3090,3030,2930,3002,3061,3064,2955,2959,2982,3077,3097,2774,2991,3054,3108,3104,3112,3118,3122,3116,3020,3085,2841,2815,325,224,257,154,168,255,166,151,169,256,165,222,164,167,149,161,162,223,150,158,163,252,251,253,250,181,221,201,202,244,197,156,186,182,174,179,225,191,199,180,234,196,175,176,187,188,177,178,238,184,193,173,249])).
% 69.42/69.48 cnf(3247,plain,
% 69.42/69.48 (P3(x32471,x32472,x32471,x32472)),
% 69.42/69.48 inference(rename_variables,[],[2936])).
% 69.42/69.48 cnf(3248,plain,
% 69.42/69.48 (P4(x32481,x32482,x32482)),
% 69.42/69.48 inference(rename_variables,[],[3028])).
% 69.42/69.48 cnf(3254,plain,
% 69.42/69.48 (P9(a16,a17,a16,a17,a17,a16,a16,a17)),
% 69.42/69.48 inference(scs_inference,[],[3040,3026,3186,3212,3034,3036,3028,3211,3215,2920,3090,3030,2930,3002,3061,3064,2955,2959,2982,3077,3097,2774,2991,3054,3108,3104,3112,3118,3122,3116,3020,3085,2841,2815,2936,325,224,257,154,168,255,166,151,169,256,165,222,164,167,149,161,162,223,150,158,163,252,251,253,250,181,221,201,202,244,197,156,186,182,174,179,225,191,199,180,234,196,175,176,187,188,177,178,238,184,193,173,249,204,152,404,254])).
% 69.42/69.48 cnf(3258,plain,
% 69.42/69.48 (P6(a16,a17,a17,a16)),
% 69.42/69.48 inference(scs_inference,[],[142,3040,3026,3186,3212,3034,3036,3028,3211,3215,2920,3090,3030,2930,3002,3061,3064,2955,2959,2982,3000,3077,3097,2774,2991,3054,3108,3104,3112,3118,3122,3116,3020,3085,2841,2815,2936,325,224,257,154,168,255,166,151,169,256,165,222,164,167,149,161,162,223,150,158,163,252,251,253,250,181,221,201,202,244,197,156,186,182,174,179,225,191,199,180,234,196,175,176,187,188,177,178,238,184,193,173,249,204,152,404,254,192,241])).
% 69.42/69.48 cnf(3260,plain,
% 69.42/69.48 (P3(a15,a15,x32601,x32601)),
% 69.42/69.48 inference(scs_inference,[],[142,3040,3026,3186,3212,3034,3036,3028,3211,3215,2920,3090,3030,2930,3002,3061,3064,2955,2959,2982,3000,3077,3097,2774,2991,3054,3108,3104,3202,3112,3118,3122,3116,3020,3085,2841,2815,2936,325,224,257,154,168,255,166,151,169,256,165,222,164,167,149,161,162,223,150,158,163,252,251,253,250,181,221,201,202,244,197,156,186,182,174,179,225,191,199,180,234,196,175,176,187,188,177,178,238,184,193,173,249,204,152,404,254,192,241,155])).
% 69.42/69.48 cnf(3267,plain,
% 69.42/69.48 (P1(x32671,x32672,x32672,x32671)),
% 69.42/69.48 inference(scs_inference,[],[142,1206,3040,3026,3186,3212,3034,3036,3028,3211,3215,2920,3090,3030,2930,3002,3061,3064,2955,2959,2982,3000,3077,3097,2774,2991,3054,3108,3104,3202,3112,3118,3122,3116,3020,3085,2841,2815,3230,2936,145,325,224,257,154,168,255,166,151,169,256,165,222,164,167,149,161,162,223,150,158,163,252,251,253,250,181,221,201,202,244,197,156,186,182,174,179,225,191,199,180,234,196,175,176,187,188,177,178,238,184,193,173,249,204,152,404,254,192,241,155,198,260,239])).
% 69.42/69.48 cnf(3270,plain,
% 69.42/69.48 (P5(a16,a15,a16)),
% 69.42/69.48 inference(scs_inference,[],[142,1206,3040,3026,3186,3212,3034,3036,3028,3211,3215,2920,3090,3030,2930,3002,3061,3064,2955,2959,2982,3000,3077,3097,2774,2991,3054,3108,3104,3202,3112,3118,3122,3116,3020,3085,2841,2815,3230,2756,2936,3247,145,325,224,257,154,168,255,166,151,169,256,165,222,164,167,149,161,162,223,150,158,163,252,251,253,250,181,221,201,202,244,197,156,186,182,174,179,225,191,199,180,234,196,175,176,187,188,177,178,238,184,193,173,249,204,152,404,254,192,241,155,198,260,239,160])).
% 69.42/69.48 cnf(3271,plain,
% 69.42/69.48 (P3(x32711,x32712,x32711,x32712)),
% 69.42/69.48 inference(rename_variables,[],[2936])).
% 69.42/69.48 cnf(3273,plain,
% 69.42/69.48 (P4(f27(a15,a15,x32731,x32731,x32731,a15),a15,x32731)),
% 69.42/69.48 inference(scs_inference,[],[142,1206,3040,3026,3186,3212,3034,3036,3028,3211,3215,3248,2920,3090,3030,2930,3002,3061,3064,2955,2959,2982,3000,3077,3097,2774,2991,3054,3108,3104,3202,3112,3118,3122,3116,3020,3085,2841,2815,3230,2756,2936,3247,3271,2900,145,325,224,257,154,168,255,166,151,169,256,165,222,164,167,149,161,162,223,150,158,163,252,251,253,250,181,221,201,202,244,197,156,186,182,174,179,225,191,199,180,234,196,175,176,187,188,177,178,238,184,193,173,249,204,152,404,254,192,241,155,198,260,239,160,206])).
% 69.42/69.48 cnf(3278,plain,
% 69.42/69.48 (P3(a15,a1,a14,a16)),
% 69.42/69.48 inference(scs_inference,[],[142,1206,3040,3026,3186,3212,3034,3036,3028,3211,3215,3248,2920,3090,3030,2930,3002,3061,3064,2955,2959,2982,3000,3077,3097,2774,2991,3054,3108,3104,3202,3112,3118,3122,3116,3020,3085,2841,2815,3230,2756,2936,3247,3271,2900,145,325,224,257,154,168,255,166,151,169,256,165,222,164,167,149,161,162,223,150,158,163,252,251,253,250,181,221,201,202,244,197,156,186,182,174,179,225,191,199,180,234,196,175,176,187,188,177,178,238,184,193,173,249,204,152,404,254,192,241,155,198,260,239,160,206,456])).
% 69.42/69.48 cnf(3285,plain,
% 69.42/69.48 (P4(x32851,x32852,x32851)),
% 69.42/69.48 inference(rename_variables,[],[3155])).
% 69.42/69.48 cnf(3287,plain,
% 69.42/69.48 (P1(a1,a14,a17,a16)),
% 69.42/69.48 inference(scs_inference,[],[3267,3155,440,553])).
% 69.42/69.48 cnf(3288,plain,
% 69.42/69.48 (P1(x32881,x32882,x32882,x32881)),
% 69.42/69.48 inference(rename_variables,[],[3267])).
% 69.42/69.48 cnf(3291,plain,
% 69.42/69.48 (P4(x32911,x32912,x32911)),
% 69.42/69.48 inference(rename_variables,[],[3155])).
% 69.42/69.48 cnf(3299,plain,
% 69.42/69.48 (P6(a16,a15,a16,a16)),
% 69.42/69.48 inference(scs_inference,[],[3267,3155,3285,3270,3010,3188,440,553,325,257,224,255,154])).
% 69.42/69.48 cnf(3301,plain,
% 69.42/69.48 (P6(a16,a17,a16,a17)),
% 69.42/69.48 inference(scs_inference,[],[3267,3155,3285,3270,3010,3258,3188,440,553,325,257,224,255,154,166])).
% 69.42/69.48 cnf(3305,plain,
% 69.42/69.48 (P5(a16,a16,a15)),
% 69.42/69.48 inference(scs_inference,[],[3267,3155,3285,3270,3010,3012,3258,3188,440,553,325,257,224,255,154,166,168,152])).
% 69.42/69.48 cnf(3307,plain,
% 69.42/69.48 (P9(a17,a16,a16,a17,a17,a16,a16,a17)),
% 69.42/69.48 inference(scs_inference,[],[3267,3155,3285,3270,3010,3012,3254,3258,3188,440,553,325,257,224,255,154,166,168,152,256])).
% 69.42/69.48 cnf(3313,plain,
% 69.42/69.48 (P10(a16,a16,a16,a15,a17,a16,a17,a15)),
% 69.42/69.48 inference(scs_inference,[],[3267,3155,3285,2928,3270,3010,3012,3254,3258,3188,440,553,325,257,224,255,154,166,168,152,256,254,169,222])).
% 69.42/69.48 cnf(3315,plain,
% 69.42/69.48 (P6(a17,a16,a16,a17)),
% 69.42/69.48 inference(scs_inference,[],[3267,3155,3285,2928,3270,3010,3012,3254,3258,3188,440,553,325,257,224,255,154,166,168,152,256,254,169,222,165])).
% 69.42/69.48 cnf(3319,plain,
% 69.42/69.48 (P1(x33191,x33192,x33191,x33192)),
% 69.42/69.48 inference(scs_inference,[],[3267,3288,3155,3285,2928,3270,3010,3012,3254,3258,3188,2737,440,553,325,257,224,255,154,166,168,152,256,254,169,222,165,149,164])).
% 69.42/69.48 cnf(3321,plain,
% 69.42/69.48 (P7(x33211,x33212,x33211,x33211)),
% 69.42/69.48 inference(scs_inference,[],[3210,3267,3288,3155,3285,2928,3270,3010,3012,3254,3258,3188,2737,440,553,325,257,224,255,154,166,168,152,256,254,169,222,165,149,164,167])).
% 69.42/69.48 cnf(3323,plain,
% 69.42/69.48 (P3(x33231,x33231,a15,a15)),
% 69.42/69.48 inference(scs_inference,[],[3210,3267,3288,3155,3285,2928,3270,3260,3010,3012,3254,3258,3188,2737,440,553,325,257,224,255,154,166,168,152,256,254,169,222,165,149,164,167,161])).
% 69.42/69.48 cnf(3325,plain,
% 69.42/69.48 (P10(a15,a15,x33251,x33252,x33253,x33253,x33251,x33252)),
% 69.42/69.48 inference(scs_inference,[],[3210,3267,3288,3155,3285,2928,3270,3260,3010,3012,3254,3258,3188,2737,440,553,325,257,224,255,154,166,168,152,256,254,169,222,165,149,164,167,161,223])).
% 69.42/69.48 cnf(3327,plain,
% 69.42/69.48 (P3(a15,a1,a16,a14)),
% 69.42/69.48 inference(scs_inference,[],[3210,3267,3288,3155,3285,2928,3270,3260,3010,3012,3254,3258,3278,3188,2737,440,553,325,257,224,255,154,166,168,152,256,254,169,222,165,149,164,167,161,223,162])).
% 69.42/69.48 cnf(3333,plain,
% 69.42/69.48 (P4(x33331,x33331,x33332)),
% 69.42/69.48 inference(scs_inference,[],[3210,3267,3288,3155,3285,3291,2928,3270,3260,3010,3012,3254,3258,3278,3188,2737,3159,440,553,325,257,224,255,154,166,168,152,256,254,169,222,165,149,164,167,161,223,162,231,158,150])).
% 69.42/69.48 cnf(3341,plain,
% 69.42/69.48 (P10(a17,a16,a16,a16,a17,a15,a16,a15)),
% 69.42/69.48 inference(scs_inference,[],[3175,3210,3267,3288,3155,3285,3291,2928,3270,3260,3010,3012,3149,3254,3258,3278,3114,3188,2737,3159,3161,440,553,325,257,224,255,154,166,168,152,256,254,169,222,165,149,164,167,161,223,162,231,158,150,163,252,251,253])).
% 69.42/69.48 cnf(3343,plain,
% 69.42/69.48 (P10(a15,a16,a15,a17,a16,a16,a16,a17)),
% 69.42/69.48 inference(scs_inference,[],[3175,3210,3267,3288,3155,3285,3291,2928,3270,3260,3010,3012,3149,3171,3254,3258,3278,3114,3188,2737,3159,3161,440,553,325,257,224,255,154,166,168,152,256,254,169,222,165,149,164,167,161,223,162,231,158,150,163,252,251,253,250])).
% 69.42/69.48 cnf(3351,plain,
% 69.42/69.48 (P6(a17,a15,a17,a16)),
% 69.42/69.48 inference(scs_inference,[],[3175,3210,3267,3288,3155,3285,3291,2928,3270,3260,3010,3012,3149,3171,3254,3258,3278,3114,3188,2737,3159,3161,2895,440,553,325,257,224,255,154,166,168,152,256,254,169,222,165,149,164,167,161,223,162,231,158,150,163,252,251,253,250,203,201,202,171])).
% 69.42/69.48 cnf(3358,plain,
% 69.42/69.48 (P9(a16,a15,a15,a16,a16,a15,a15,a16)),
% 69.42/69.48 inference(scs_inference,[],[3175,3210,3267,3288,3155,3285,3291,2928,3270,3260,3010,3012,3149,3171,3254,3258,3278,3114,3188,2737,3159,3161,3056,2719,2895,145,440,553,325,257,224,255,154,166,168,152,256,254,169,222,165,149,164,167,161,223,162,231,158,150,163,252,251,253,250,203,201,202,171,89,197,192,221])).
% 69.42/69.48 cnf(3361,plain,
% 69.42/69.48 (P10(x33611,x33612,x33613,x33614,x33612,x33611,x33614,x33613)),
% 69.42/69.48 inference(rename_variables,[],[3169])).
% 69.42/69.48 cnf(3362,plain,
% 69.42/69.48 (P2(f20(a15,x33621),a15,x33621,x33621)),
% 69.42/69.48 inference(rename_variables,[],[3194])).
% 69.42/69.48 cnf(3364,plain,
% 69.42/69.48 (P2(x33641,x33641,x33641,x33641)),
% 69.42/69.48 inference(scs_inference,[],[3238,3169,3175,3210,3267,3288,3155,3285,3291,2928,3270,3260,3010,3012,3149,3171,3254,3258,3278,3114,3188,2737,3159,3194,3161,3056,2719,2895,145,440,553,325,257,224,255,154,166,168,152,256,254,169,222,165,149,164,167,161,223,162,231,158,150,163,252,251,253,250,203,201,202,171,89,197,192,221,240,182])).
% 69.42/69.48 cnf(3366,plain,
% 69.42/69.48 (P1(f20(a15,x33661),f20(a15,x33661),x33661,f20(a15,x33661))),
% 69.42/69.48 inference(scs_inference,[],[3238,3169,3175,3210,3267,3288,3155,3285,3291,2928,3270,3260,3010,3012,3149,3171,3254,3258,3278,3114,3188,2737,3177,3159,3194,3161,3056,2719,2895,145,440,553,325,257,224,255,154,166,168,152,256,254,169,222,165,149,164,167,161,223,162,231,158,150,163,252,251,253,250,203,201,202,171,89,197,192,221,240,182,179])).
% 69.42/69.48 cnf(3377,plain,
% 69.42/69.48 (~P3(a14,a17,a14,f3(a14,a1,a16))),
% 69.42/69.48 inference(scs_inference,[],[3238,3169,3175,3210,3267,3288,3155,3285,3291,2928,3270,3260,3010,3012,3149,3171,3254,3258,3278,2957,3114,3188,2737,3177,3159,3194,3161,3056,2719,2895,145,440,553,325,257,224,255,154,166,168,152,256,254,169,222,165,149,164,167,161,223,162,231,158,150,163,252,251,253,250,203,201,202,171,89,197,192,221,240,182,179,225,191,198,199,180])).
% 69.42/69.48 cnf(3383,plain,
% 69.42/69.48 (P7(x33831,x33831,x33831,x33832)),
% 69.42/69.48 inference(scs_inference,[],[3238,3169,3173,3175,3210,3267,3288,3155,3285,3291,2928,3270,3260,3010,3012,3149,3167,3171,3254,3258,3278,2957,3114,3188,2737,3177,3159,3194,3161,3056,2940,2719,2895,145,440,553,325,257,224,255,154,166,168,152,256,254,169,222,165,149,164,167,161,223,162,231,158,150,163,252,251,253,250,203,201,202,171,89,197,192,221,240,182,179,225,191,198,199,180,196,176,234])).
% 69.42/69.48 cnf(3384,plain,
% 69.42/69.48 (P10(x33841,x33842,x33841,x33842,x33843,x33844,x33843,x33844)),
% 69.42/69.48 inference(rename_variables,[],[3173])).
% 69.42/69.48 cnf(3388,plain,
% 69.42/69.48 (~E(a17,a14)),
% 69.42/69.48 inference(scs_inference,[],[3238,3169,3173,3175,3210,3267,3288,3155,3285,3291,2928,3270,3260,3010,3012,3149,3167,3171,3254,3258,3278,2957,3114,3188,2737,3177,3159,3194,3362,3161,3056,3126,2940,2719,2895,145,440,553,325,257,224,255,154,166,168,152,256,254,169,222,165,149,164,167,161,223,162,231,158,150,163,252,251,253,250,203,201,202,171,89,197,192,221,240,182,179,225,191,198,199,180,196,176,234,175,109])).
% 69.42/69.48 cnf(3389,plain,
% 69.42/69.48 (P2(f20(a15,x33891),a15,x33891,x33891)),
% 69.42/69.48 inference(rename_variables,[],[3194])).
% 69.42/69.48 cnf(3390,plain,
% 69.42/69.48 (P4(f11(a17,a15,a16,x33901,a15),x33901,a15)),
% 69.42/69.48 inference(scs_inference,[],[3238,3169,3173,3175,3210,3267,3288,3155,3285,3291,2928,3270,3260,3010,3012,3149,3167,3171,3254,3258,3278,2957,3114,3188,2737,3177,3159,3194,3362,3161,3056,3126,2940,2719,2934,2895,145,440,553,325,257,224,255,154,166,168,152,256,254,169,222,165,149,164,167,161,223,162,231,158,150,163,252,251,253,250,203,201,202,171,89,197,192,221,240,182,179,225,191,198,199,180,196,176,234,175,109,195])).
% 69.42/69.48 cnf(3391,plain,
% 69.42/69.48 (P4(x33911,x33912,x33911)),
% 69.42/69.48 inference(rename_variables,[],[3155])).
% 69.42/69.48 cnf(3401,plain,
% 69.42/69.48 (P10(x34011,x34012,x34013,x34014,x34012,x34011,x34014,x34013)),
% 69.42/69.48 inference(rename_variables,[],[3169])).
% 69.42/69.48 cnf(3403,plain,
% 69.42/69.48 (P3(a1,a15,a16,a14)),
% 69.42/69.48 inference(scs_inference,[],[3238,3169,3361,3401,3173,3175,3210,3267,3288,3155,3285,3291,2928,3270,3260,2721,3010,3012,3149,3167,3171,3254,3258,3278,2957,3114,3188,2737,3177,3159,3194,3362,3161,3273,3056,3126,2940,2719,2934,2895,145,307,440,553,325,257,224,255,154,166,168,152,256,254,169,222,165,149,164,167,161,223,162,231,158,150,163,252,251,253,250,203,201,202,171,89,197,192,221,240,182,179,225,191,198,199,180,196,176,234,175,109,195,187,188,170,260,238])).
% 69.42/69.48 cnf(3404,plain,
% 69.42/69.48 (P10(x34041,x34042,x34043,x34044,x34042,x34041,x34044,x34043)),
% 69.42/69.48 inference(rename_variables,[],[3169])).
% 69.42/69.48 cnf(3409,plain,
% 69.42/69.48 (P5(x34091,x34091,x34091)),
% 69.42/69.48 inference(scs_inference,[],[3238,3169,3361,3401,3404,3173,3384,3175,3210,3267,3288,3155,3285,3291,3391,2928,3270,3260,2721,3010,3012,3149,3167,3171,3254,3258,3278,2957,3114,3188,2737,3177,3159,3194,3362,3389,3161,3273,3056,3126,2940,2719,2934,2895,145,307,440,553,325,257,224,255,154,166,168,152,256,254,169,222,165,149,164,167,161,223,162,231,158,150,163,252,251,253,250,203,201,202,171,89,197,192,221,240,182,179,225,191,198,199,180,196,176,234,175,109,195,187,188,170,260,238,239,237])).
% 69.42/69.48 cnf(3411,plain,
% 69.42/69.48 (P10(x34111,x34112,x34111,x34112,x34113,x34114,x34113,x34114)),
% 69.42/69.48 inference(rename_variables,[],[3173])).
% 69.42/69.48 cnf(3412,plain,
% 69.42/69.48 (P4(x34121,x34122,x34121)),
% 69.42/69.48 inference(rename_variables,[],[3155])).
% 69.42/69.48 cnf(3414,plain,
% 69.42/69.48 (P5(a15,f26(a17,a16,a15,a15,a15),f26(a17,a16,a15,a15,a15))),
% 69.42/69.48 inference(scs_inference,[],[3238,3169,3361,3401,3404,3173,3384,3175,3210,3267,3288,3155,3285,3291,3391,2928,3270,3260,2721,3010,3012,3149,3167,3171,3254,3258,3278,2957,3114,3188,2737,3177,3159,3194,3362,3389,3161,3273,3236,3056,3126,3028,2940,2719,3122,2934,2895,145,307,440,553,325,257,224,255,154,166,168,152,256,254,169,222,165,149,164,167,161,223,162,231,158,150,163,252,251,253,250,203,201,202,171,89,197,192,221,240,182,179,225,191,198,199,180,196,176,234,175,109,195,187,188,170,260,238,239,237,160])).
% 69.42/69.48 cnf(3415,plain,
% 69.42/69.48 (P4(x34151,x34152,x34152)),
% 69.42/69.48 inference(rename_variables,[],[3028])).
% 69.42/69.48 cnf(3417,plain,
% 69.42/69.48 (P5(f24(a15,a15,a15,a15,a15,a15),f11(a15,a17,a16,a16,a17),a16)),
% 69.42/69.48 inference(scs_inference,[],[3238,3169,3361,3401,3404,3173,3384,3175,3210,3267,3288,3155,3285,3291,3391,2928,3270,3260,2721,3010,3012,3149,3167,3171,3254,3258,3278,2957,3114,3188,2737,3177,3159,3194,3362,3389,3161,3273,3236,3056,3094,3181,3126,3028,2940,2719,3122,2934,2895,145,307,440,553,325,257,224,255,154,166,168,152,256,254,169,222,165,149,164,167,161,223,162,231,158,150,163,252,251,253,250,203,201,202,171,89,197,192,221,240,182,179,225,191,198,199,180,196,176,234,175,109,195,187,188,170,260,238,239,237,160,173])).
% 69.42/69.48 cnf(3420,plain,
% 69.42/69.48 (P4(x34201,x34202,x34202)),
% 69.42/69.48 inference(rename_variables,[],[3028])).
% 69.42/69.48 cnf(3428,plain,
% 69.42/69.48 (P6(a16,a16,a17,a17)),
% 69.42/69.48 inference(scs_inference,[],[3238,3169,3361,3401,3404,3173,3384,3411,3175,3210,3267,3288,3155,3285,3291,3391,3412,2928,3008,3270,3260,2721,3010,3012,3149,3167,3171,3254,3258,3278,2957,3114,3188,2737,3177,3159,3194,3362,3389,3161,3273,3236,3056,3094,3181,3126,3028,3415,3420,2940,2719,3122,2934,2895,145,307,440,553,325,257,224,255,154,166,168,152,256,254,169,222,165,149,164,167,161,223,162,231,158,150,163,252,251,253,250,203,201,202,171,89,197,192,221,240,182,179,225,191,198,199,180,196,176,234,175,109,195,187,188,170,260,238,239,237,160,173,207,157,249])).
% 69.42/69.48 cnf(3434,plain,
% 69.42/69.48 (~E(f20(a16,a17),x34341)+~P5(x34341,a1,a14)),
% 69.42/69.48 inference(scs_inference,[],[3238,3169,3361,3401,3404,3173,3384,3411,3175,3210,3267,3288,3155,3285,3291,3391,3412,2928,3008,3270,3260,2721,3010,3012,3149,3167,3171,3254,3258,3278,2957,3114,3188,2737,3177,3159,3194,3362,3389,3161,3273,3236,3056,3094,3181,3126,3028,3415,3420,2940,2719,3122,2934,2895,145,307,440,553,325,257,224,255,154,166,168,152,256,254,169,222,165,149,164,167,161,223,162,231,158,150,163,252,251,253,250,203,201,202,171,89,197,192,221,240,182,179,225,191,198,199,180,196,176,234,175,109,195,187,188,170,260,238,239,237,160,173,207,157,249,151,2,2743])).
% 69.42/69.48 cnf(3444,plain,
% 69.42/69.48 (~P5(f20(a16,a17),a1,a14)),
% 69.42/69.48 inference(scs_inference,[],[3238,3169,3361,3401,3404,3173,3384,3411,3175,3210,3267,3288,3155,3285,3291,3391,3412,2928,3008,3270,3260,2721,3010,3012,3149,3167,3171,3254,3258,3278,2957,3114,3183,3188,2737,3177,3159,3194,3362,3389,3161,3273,3236,3056,3094,3181,3126,3028,3415,3420,2940,3036,2719,359,3122,2934,2895,145,307,440,553,325,257,224,255,154,166,168,152,256,254,169,222,165,149,164,167,161,223,162,231,158,150,163,252,251,253,250,203,201,202,171,89,197,192,221,240,182,179,225,191,198,199,180,196,176,234,175,109,195,187,188,170,260,238,239,237,160,173,207,157,249,151,2,2743,228,236,247,155])).
% 69.42/69.48 cnf(3446,plain,
% 69.42/69.48 (P7(x34461,x34461,a15,x34461)),
% 69.42/69.48 inference(scs_inference,[],[3238,3169,3361,3401,3404,3173,3384,3411,3175,3210,3267,3288,3155,3285,3291,3391,3412,2928,3008,3270,3260,2721,3010,3012,3149,3167,3171,3254,3258,3278,2957,3114,3183,3188,2737,3177,3159,3194,3362,3389,3133,3161,3273,3236,3056,3094,3181,3126,3028,3415,3420,2940,3036,2719,359,3122,2934,2895,145,307,440,553,325,257,224,255,154,166,168,152,256,254,169,222,165,149,164,167,161,223,162,231,158,150,163,252,251,253,250,203,201,202,171,89,197,192,221,240,182,179,225,191,198,199,180,196,176,234,175,109,195,187,188,170,260,238,239,237,160,173,207,157,249,151,2,2743,228,236,247,155,194])).
% 69.42/69.48 cnf(3460,plain,
% 69.42/69.48 (P4(x34601,x34601,x34602)),
% 69.42/69.48 inference(rename_variables,[],[3333])).
% 69.42/69.48 cnf(3462,plain,
% 69.42/69.48 (P1(a1,a14,a16,a17)),
% 69.42/69.48 inference(scs_inference,[],[3319,3333,440,553])).
% 69.42/69.48 cnf(3463,plain,
% 69.42/69.48 (P1(x34631,x34632,x34631,x34632)),
% 69.42/69.48 inference(rename_variables,[],[3319])).
% 69.42/69.48 cnf(3465,plain,
% 69.42/69.48 (P3(a1,a15,a14,a16)),
% 69.42/69.48 inference(scs_inference,[],[3319,3463,3333,440,553,456])).
% 69.42/69.48 cnf(3466,plain,
% 69.42/69.48 (P1(x34661,x34662,x34661,x34662)),
% 69.42/69.48 inference(rename_variables,[],[3319])).
% 69.42/69.48 cnf(3468,plain,
% 69.42/69.48 (P10(a16,a15,a15,a16,a15,a16,a16,a16)),
% 69.42/69.48 inference(scs_inference,[],[3319,3463,3333,3299,440,553,456,224])).
% 69.42/69.48 cnf(3471,plain,
% 69.42/69.48 (P4(x34711,x34711,x34712)),
% 69.42/69.48 inference(rename_variables,[],[3333])).
% 69.42/69.48 cnf(3475,plain,
% 69.42/69.48 (P1(f6(x34751,x34751,x34751,x34751),x34751,x34751,x34751)),
% 69.42/69.48 inference(scs_inference,[],[3364,3319,3463,3333,3460,3137,3299,440,553,456,224,325,257,185])).
% 69.42/69.48 cnf(3477,plain,
% 69.42/69.48 (P6(a17,a16,a17,a16)),
% 69.42/69.48 inference(scs_inference,[],[3364,3319,3463,3333,3460,3137,3299,3315,440,553,456,224,325,257,185,166])).
% 69.42/69.48 cnf(3479,plain,
% 69.42/69.48 (P9(a16,a17,a17,a16,a16,a17,a16,a17)),
% 69.42/69.48 inference(scs_inference,[],[3364,3319,3463,3333,3460,3145,3137,3299,3315,440,553,456,224,325,257,185,166,255])).
% 69.42/69.48 cnf(3481,plain,
% 69.42/69.48 (P6(a16,a16,a16,a15)),
% 69.42/69.48 inference(scs_inference,[],[3364,3319,3463,3333,3460,3145,3305,3137,3299,3315,440,553,456,224,325,257,185,166,255,154])).
% 69.42/69.48 cnf(3487,plain,
% 69.42/69.48 (P9(a14,a1,a14,a1,a1,a1,a1,a1)),
% 69.42/69.48 inference(scs_inference,[],[3364,3319,3463,3321,3333,3460,3145,3305,3137,3299,3315,3417,440,553,456,224,325,257,185,166,255,154,168,151,254])).
% 69.42/69.48 cnf(3489,plain,
% 69.42/69.48 (P9(a15,a16,a15,a16,a16,a15,a15,a16)),
% 69.42/69.48 inference(scs_inference,[],[3364,3319,3463,3321,3333,3460,3145,3305,3137,3299,3315,3358,3417,440,553,456,224,325,257,185,166,255,154,168,151,254,256])).
% 69.42/69.48 cnf(3493,plain,
% 69.42/69.48 (P10(a16,a15,a16,a16,a17,a15,a17,a16)),
% 69.42/69.48 inference(scs_inference,[],[3364,3319,3463,3321,3333,3460,3145,3305,3137,3299,3315,3358,3417,2854,440,553,456,224,325,257,185,166,255,154,168,151,254,256,152,222])).
% 69.42/69.48 cnf(3496,plain,
% 69.42/69.48 (P6(a17,a16,a17,a15)),
% 69.42/69.48 inference(scs_inference,[],[3364,3319,3463,3321,3333,3460,3145,3305,3137,3299,3315,3351,3358,3388,3417,2854,440,553,456,224,325,257,185,166,255,154,168,151,254,256,152,222,2,165])).
% 69.42/69.48 cnf(3504,plain,
% 69.42/69.48 (P3(a16,a14,a15,a1)),
% 69.42/69.48 inference(scs_inference,[],[3364,3319,3463,3321,3333,3460,3145,3305,3137,3299,3315,3327,3351,3358,3388,3366,2972,3417,3190,2854,440,553,456,224,325,257,185,166,255,154,168,151,254,256,152,222,2,165,149,164,162,161])).
% 69.42/69.48 cnf(3506,plain,
% 69.42/69.48 (P10(x35061,x35061,x35062,x35063,a15,a15,x35062,x35063)),
% 69.42/69.48 inference(scs_inference,[],[3364,3319,3463,3321,3333,3460,3145,3305,3323,3137,3299,3315,3327,3351,3358,3388,3366,2972,3417,3190,2854,440,553,456,224,325,257,185,166,255,154,168,151,254,256,152,222,2,165,149,164,162,161,223])).
% 69.42/69.48 cnf(3512,plain,
% 69.42/69.48 (P1(a17,a16,a1,a14)),
% 69.42/69.48 inference(scs_inference,[],[3364,3319,3463,3321,3333,3460,3145,3305,3323,3137,3287,3299,3315,3327,3351,3358,3388,3366,2972,3417,3190,3227,2854,440,553,456,224,325,257,185,166,255,154,168,151,254,256,152,222,2,165,149,164,162,161,223,158,150,163])).
% 69.42/69.48 cnf(3516,plain,
% 69.42/69.48 (P10(x35161,x35162,a15,a15,x35161,x35162,x35163,x35163)),
% 69.42/69.48 inference(scs_inference,[],[3364,3319,3463,3321,3333,3460,3145,3325,3305,3323,3137,3287,3299,3315,3327,3341,3351,3358,3388,3366,2972,3417,3190,3227,2854,440,553,456,224,325,257,185,166,255,154,168,151,254,256,152,222,2,165,149,164,162,161,223,158,150,163,252,251])).
% 69.42/69.48 cnf(3520,plain,
% 69.42/69.48 (P10(a17,a15,a16,a15,a17,a16,a16,a16)),
% 69.42/69.48 inference(scs_inference,[],[3364,3319,3463,3321,3333,3460,3145,3313,3325,3305,3323,3137,3287,3299,3315,3327,3341,3351,3358,3388,3366,2972,3417,3190,3227,2854,440,553,456,224,325,257,185,166,255,154,168,151,254,256,152,222,2,165,149,164,162,161,223,158,150,163,252,251,253,250])).
% 69.42/69.48 cnf(3522,plain,
% 69.42/69.48 (P6(x35221,x35221,x35222,x35221)),
% 69.42/69.48 inference(scs_inference,[],[3364,3409,3319,3463,3321,3333,3460,3145,3313,3325,3305,3323,3137,3287,3299,3315,3327,3341,3351,3358,3388,3366,2972,3417,3190,3227,3267,2854,440,553,456,224,325,257,185,166,255,154,168,151,254,256,152,222,2,165,149,164,162,161,223,158,150,163,252,251,253,250,172])).
% 69.42/69.48 cnf(3523,plain,
% 69.42/69.48 (P1(x35231,x35232,x35232,x35231)),
% 69.42/69.48 inference(rename_variables,[],[3267])).
% 69.42/69.48 cnf(3525,plain,
% 69.42/69.48 (P5(f24(x35251,x35251,x35251,x35251,x35251,x35251),x35251,x35251)),
% 69.42/69.48 inference(scs_inference,[],[3364,3409,3319,3463,3321,3333,3460,3145,3313,3325,3305,3323,3137,3287,3299,3315,3327,3341,3351,3358,3388,3366,2972,3417,3190,3227,3267,2854,440,553,456,224,325,257,185,166,255,154,168,151,254,256,152,222,2,165,149,164,162,161,223,158,150,163,252,251,253,250,172,201])).
% 69.42/69.48 cnf(3528,plain,
% 69.42/69.48 (P5(x35281,x35281,x35281)),
% 69.42/69.48 inference(rename_variables,[],[3409])).
% 69.42/69.48 cnf(3530,plain,
% 69.42/69.48 (P6(f11(a15,a15,a15,a15,a15),a15,f11(a15,a15,a15,a15,a15),a15)),
% 69.42/69.48 inference(scs_inference,[],[3364,3409,3528,3319,3463,3321,3333,3460,3145,3313,3325,3305,3323,3137,3287,3299,3315,3327,3341,3351,3358,3388,3366,2972,3214,3417,3190,3377,3227,3267,2854,440,553,456,224,325,257,185,166,255,154,168,151,254,256,152,222,2,165,149,164,162,161,223,158,150,163,252,251,253,250,172,201,156,171])).
% 69.42/69.48 cnf(3532,plain,
% 69.42/69.48 (P5(x35321,x35321,x35321)),
% 69.42/69.48 inference(rename_variables,[],[3409])).
% 69.42/69.48 cnf(3534,plain,
% 69.42/69.48 (P3(f24(x35341,x35341,x35341,x35341,x35341,x35341),x35341,x35341,x35341)),
% 69.42/69.48 inference(scs_inference,[],[3364,3409,3528,3532,3319,3463,3321,3333,3460,3145,3313,3325,3305,3323,3137,3287,3299,3315,3327,3341,3351,3358,3388,3366,2972,3214,3417,3190,3377,3227,3267,2854,440,553,456,224,325,257,185,166,255,154,168,151,254,256,152,222,2,165,149,164,162,161,223,158,150,163,252,251,253,250,172,201,156,171,203])).
% 69.42/69.48 cnf(3537,plain,
% 69.42/69.48 (P1(x35371,x35372,x35372,x35371)),
% 69.42/69.48 inference(rename_variables,[],[3267])).
% 69.42/69.48 cnf(3540,plain,
% 69.42/69.48 (P1(x35401,x35402,x35401,x35402)),
% 69.42/69.48 inference(rename_variables,[],[3319])).
% 69.42/69.48 cnf(3543,plain,
% 69.42/69.48 (P1(x35431,x35432,x35431,x35432)),
% 69.42/69.48 inference(rename_variables,[],[3319])).
% 69.42/69.48 cnf(3548,plain,
% 69.42/69.48 (P1(x35481,x35482,x35482,x35481)),
% 69.42/69.48 inference(rename_variables,[],[3267])).
% 69.42/69.48 cnf(3553,plain,
% 69.42/69.48 (P1(x35531,x35532,x35531,x35532)),
% 69.42/69.48 inference(rename_variables,[],[3319])).
% 69.42/69.48 cnf(3554,plain,
% 69.42/69.48 (P7(x35541,x35542,x35541,x35541)),
% 69.42/69.48 inference(rename_variables,[],[3321])).
% 69.42/69.48 cnf(3556,plain,
% 69.42/69.48 (P2(a16,a15,a16,a16)),
% 69.42/69.48 inference(scs_inference,[],[3364,3409,3528,3532,3319,3463,3466,3540,3543,3321,3333,3460,3145,3313,3325,3305,3323,3137,3287,3299,3301,3315,3327,3341,3351,3358,3388,3366,2972,3214,3417,3190,3377,3227,3267,3523,3537,2854,3238,440,553,456,224,325,257,185,166,255,154,168,151,254,256,152,222,2,165,149,164,162,161,223,158,150,163,252,251,253,250,172,201,156,171,203,192,186,197,202,174,221,189,182])).
% 69.42/69.48 cnf(3559,plain,
% 69.42/69.48 (P1(x35591,x35592,x35591,x35592)),
% 69.42/69.48 inference(rename_variables,[],[3319])).
% 69.42/69.48 cnf(3562,plain,
% 69.42/69.48 (P1(x35621,x35622,x35621,x35622)),
% 69.42/69.48 inference(rename_variables,[],[3319])).
% 69.42/69.48 cnf(3570,plain,
% 69.42/69.48 (P1(x35701,x35702,x35702,x35701)),
% 69.42/69.48 inference(rename_variables,[],[3267])).
% 69.42/69.48 cnf(3573,plain,
% 69.42/69.48 (P5(x35731,x35731,x35731)),
% 69.42/69.48 inference(rename_variables,[],[3409])).
% 69.42/69.48 cnf(3575,plain,
% 69.42/69.48 (~E(a15,a17)),
% 69.42/69.48 inference(scs_inference,[],[142,3364,3409,3528,3532,3319,3463,3466,3540,3543,3553,3559,3562,3321,3333,3460,3145,3313,3325,3305,3323,3137,3287,3299,3301,3315,3327,3341,3351,3358,3388,3366,2972,3214,3414,3417,3190,3377,3227,3229,3267,3523,3537,3548,2854,339,3238,440,553,456,224,325,257,185,166,255,154,168,151,254,256,152,222,2,165,149,164,162,161,223,158,150,163,252,251,253,250,172,201,156,171,203,192,186,197,202,174,221,189,182,191,199,180,225,198,155,90])).
% 69.42/69.48 cnf(3576,plain,
% 69.42/69.48 (P1(x35761,x35762,x35761,x35762)),
% 69.42/69.48 inference(rename_variables,[],[3319])).
% 69.42/69.48 cnf(3577,plain,
% 69.42/69.48 (P1(a16,a16,a17,a17)),
% 69.42/69.48 inference(scs_inference,[],[142,3364,3409,3528,3532,3319,3463,3466,3540,3543,3553,3559,3562,3321,3333,3460,3145,3313,3325,3305,3323,3137,3287,3299,3301,3315,3327,3341,3351,3358,3388,3366,2972,3214,3414,3417,3190,3377,3227,3229,3267,3523,3537,3548,2854,339,3238,440,553,456,224,325,257,185,166,255,154,168,151,254,256,152,222,2,165,149,164,162,161,223,158,150,163,252,251,253,250,172,201,156,171,203,192,186,197,202,174,221,189,182,191,199,180,225,198,155,90,179])).
% 69.42/69.48 cnf(3587,plain,
% 69.42/69.48 (P1(x35871,x35872,x35872,x35871)),
% 69.42/69.48 inference(rename_variables,[],[3267])).
% 69.42/69.48 cnf(3588,plain,
% 69.42/69.48 (P1(f11(x35881,x35881,x35881,x35881,x35882),x35881,x35881,x35882)),
% 69.42/69.48 inference(scs_inference,[],[142,3364,3409,3528,3532,3319,3463,3466,3540,3543,3553,3559,3562,3576,3321,3333,3460,3471,3145,3313,3325,3305,3323,3137,3287,3299,3301,3315,3327,3341,3351,3358,3388,2713,2963,3366,2972,3214,3414,3417,3190,3377,3227,3229,3173,3267,3523,3537,3548,3570,2854,339,3238,440,553,456,224,325,257,185,166,255,154,168,151,254,256,152,222,2,165,149,164,162,161,223,158,150,163,252,251,253,250,172,201,156,171,203,192,186,197,202,174,221,189,182,191,199,180,225,198,155,90,179,234,176,175,88,196])).
% 69.42/69.48 cnf(3589,plain,
% 69.42/69.48 (P1(x35891,x35892,x35891,x35892)),
% 69.42/69.48 inference(rename_variables,[],[3319])).
% 69.42/69.48 cnf(3593,plain,
% 69.42/69.48 (P4(f11(x35931,x35931,x35931,x35931,x35932),x35931,x35932)),
% 69.42/69.48 inference(scs_inference,[],[142,3364,3409,3528,3532,3319,3463,3466,3540,3543,3553,3559,3562,3576,3589,3321,3333,3460,3471,3145,3313,3325,3305,3323,3137,3287,3299,3301,3315,3327,3341,3351,3358,3388,2713,2963,3366,2972,3214,3414,3417,3190,3377,3227,3229,3173,3267,3523,3537,3548,3570,3587,2854,339,3238,440,553,456,224,325,257,185,166,255,154,168,151,254,256,152,222,2,165,149,164,162,161,223,158,150,163,252,251,253,250,172,201,156,171,203,192,186,197,202,174,221,189,182,191,199,180,225,198,155,90,179,234,176,175,88,196,91,195])).
% 69.42/69.48 cnf(3594,plain,
% 69.42/69.48 (P4(x35941,x35941,x35942)),
% 69.42/69.48 inference(rename_variables,[],[3333])).
% 69.42/69.48 cnf(3595,plain,
% 69.42/69.48 (P1(x35951,x35952,x35951,x35952)),
% 69.42/69.48 inference(rename_variables,[],[3319])).
% 69.42/69.48 cnf(3597,plain,
% 69.42/69.48 (P1(x35971,f3(x35971,x35971,x35972),x35972,x35971)),
% 69.42/69.48 inference(scs_inference,[],[142,3364,3409,3528,3532,3319,3463,3466,3540,3543,3553,3559,3562,3576,3589,3595,3321,3333,3460,3471,3145,3313,3325,3305,3323,3137,3287,3299,3301,3315,3327,3341,3351,3358,3388,2713,2963,3366,2972,3214,3414,3417,3190,3377,3227,3229,3173,3267,3523,3537,3548,3570,3587,2854,339,3238,440,553,456,224,325,257,185,166,255,154,168,151,254,256,152,222,2,165,149,164,162,161,223,158,150,163,252,251,253,250,172,201,156,171,203,192,186,197,202,174,221,189,182,191,199,180,225,198,155,90,179,234,176,175,88,196,91,195,187])).
% 69.42/69.48 cnf(3601,plain,
% 69.42/69.48 (P1(a15,a16,a16,a16)),
% 69.42/69.48 inference(scs_inference,[],[142,3364,3409,3528,3532,3319,3463,3466,3540,3543,3553,3559,3562,3576,3589,3595,3321,3333,3460,3471,3145,3313,3325,3305,3323,3137,3287,3299,3301,3315,3327,3341,3351,3358,3388,2713,2963,3366,2972,3214,3414,3417,3190,3377,3227,3229,3173,3267,3523,3537,3548,3570,3587,3155,2854,339,3238,440,553,456,224,325,257,185,166,255,154,168,151,254,256,152,222,2,165,149,164,162,161,223,158,150,163,252,251,253,250,172,201,156,171,203,192,186,197,202,174,221,189,182,191,199,180,225,198,155,90,179,234,176,175,88,196,91,195,187,188,170])).
% 69.42/69.48 cnf(3602,plain,
% 69.42/69.48 (P4(x36021,x36022,x36021)),
% 69.42/69.48 inference(rename_variables,[],[3155])).
% 69.42/69.48 cnf(3607,plain,
% 69.42/69.48 (~P1(a16,a1,a14,a17)),
% 69.42/69.48 inference(scs_inference,[],[142,3364,3409,3528,3532,3319,3463,3466,3540,3543,3553,3559,3562,3576,3589,3595,3321,3333,3460,3471,3145,3313,3325,3305,3323,3137,3287,3299,3301,3315,3327,3341,3351,3358,3388,2713,2963,3366,2972,3214,3414,3417,3190,3377,3227,3229,2876,3173,3267,3523,3537,3548,3570,3587,3155,2854,339,284,3238,440,553,456,224,325,257,185,166,255,154,168,151,254,256,152,222,2,165,149,164,162,161,223,158,150,163,252,251,253,250,172,201,156,171,203,192,186,197,202,174,221,189,182,191,199,180,225,198,155,90,179,234,176,175,88,196,91,195,187,188,170,260,178])).
% 69.42/69.48 cnf(3608,plain,
% 69.42/69.48 (P1(x36081,x36082,x36081,x36082)),
% 69.42/69.48 inference(rename_variables,[],[3319])).
% 69.42/69.48 cnf(3613,plain,
% 69.42/69.48 (P1(a15,a15,x36131,x36131)),
% 69.42/69.48 inference(scs_inference,[],[142,3364,3409,3528,3532,3319,3463,3466,3540,3543,3553,3559,3562,3576,3589,3595,3608,3321,3333,3460,3471,3145,3313,3325,3305,3323,3137,3287,3299,3301,3315,3327,3341,3351,3358,3388,2713,2963,3366,2972,3214,3414,3417,3190,3377,3227,3229,2876,3173,3267,3523,3537,3548,3570,3587,3155,2854,2882,339,284,3238,440,553,456,224,325,257,185,166,255,154,168,151,254,256,152,222,2,165,149,164,162,161,223,158,150,163,252,251,253,250,172,201,156,171,203,192,186,197,202,174,221,189,182,191,199,180,225,198,155,90,179,234,176,175,88,196,91,195,187,188,170,260,178,238,239])).
% 69.42/69.48 cnf(3615,plain,
% 69.42/69.48 (P1(x36151,x36152,x36151,x36152)),
% 69.42/69.48 inference(rename_variables,[],[3319])).
% 69.42/69.48 cnf(3617,plain,
% 69.42/69.48 (P5(f5(x36171,x36171,x36171),x36171,x36171)),
% 69.42/69.48 inference(scs_inference,[],[142,3364,3409,3528,3532,3573,3319,3463,3466,3540,3543,3553,3559,3562,3576,3589,3595,3608,3615,3321,3333,3460,3471,3145,3313,3325,3305,3323,3137,3287,3299,3301,3315,3327,3341,3351,3358,3388,2713,2963,3366,2972,3214,3414,3417,3190,3377,3227,3229,2876,3173,3267,3523,3537,3548,3570,3587,3155,2854,2882,339,284,3238,440,553,456,224,325,257,185,166,255,154,168,151,254,256,152,222,2,165,149,164,162,161,223,158,150,163,252,251,253,250,172,201,156,171,203,192,186,197,202,174,221,189,182,191,199,180,225,198,155,90,179,234,176,175,88,196,91,195,187,188,170,260,178,238,239,184])).
% 69.42/69.48 cnf(3619,plain,
% 69.42/69.48 (P5(x36191,x36191,x36191)),
% 69.42/69.48 inference(rename_variables,[],[3409])).
% 69.42/69.48 cnf(3622,plain,
% 69.42/69.48 (P7(x36221,x36221,a15,a15)),
% 69.42/69.48 inference(scs_inference,[],[142,3364,3409,3528,3532,3573,3319,3463,3466,3540,3543,3553,3559,3562,3576,3589,3595,3608,3615,3321,3333,3460,3471,3145,3313,3325,3305,3323,3137,3287,3299,3301,3315,3327,3341,3351,3358,3388,2713,2963,3366,2972,3214,3414,3417,3190,3377,3227,3229,2876,3173,3267,3523,3537,3548,3570,3587,3155,2854,2882,3133,339,284,3238,3177,440,553,456,224,325,257,185,166,255,154,168,151,254,256,152,222,2,165,149,164,162,161,223,158,150,163,252,251,253,250,172,201,156,171,203,192,186,197,202,174,221,189,182,191,199,180,225,198,155,90,179,234,176,175,88,196,91,195,187,188,170,260,178,238,239,184,194])).
% 69.42/69.48 cnf(3626,plain,
% 69.42/69.48 (P3(x36261,x36262,x36261,x36262)),
% 69.42/69.48 inference(rename_variables,[],[2936])).
% 69.42/69.48 cnf(3627,plain,
% 69.42/69.48 (P7(x36271,x36272,x36271,x36271)),
% 69.42/69.48 inference(rename_variables,[],[3321])).
% 69.42/69.48 cnf(3630,plain,
% 69.42/69.48 (P4(x36301,x36301,x36302)),
% 69.42/69.48 inference(rename_variables,[],[3333])).
% 69.42/69.48 cnf(3631,plain,
% 69.42/69.48 (P3(x36311,x36312,x36312,x36311)),
% 69.42/69.48 inference(rename_variables,[],[2900])).
% 69.42/69.48 cnf(3640,plain,
% 69.42/69.48 (P3(x36401,x36401,a15,a15)),
% 69.42/69.48 inference(rename_variables,[],[3323])).
% 69.42/69.48 cnf(3641,plain,
% 69.42/69.48 (P4(x36411,x36412,x36411)),
% 69.42/69.48 inference(rename_variables,[],[3155])).
% 69.42/69.48 cnf(3647,plain,
% 69.42/69.48 (P5(f20(x36471,x36472),x36471,x36472)),
% 69.42/69.48 inference(scs_inference,[],[142,3364,3409,3528,3532,3573,3619,3319,3463,3466,3540,3543,3553,3559,3562,3576,3589,3595,3608,3615,3321,3554,3627,3383,3333,3460,3471,3594,3630,3145,3313,3446,3325,3305,3323,3137,3287,3299,3301,3315,3327,3341,3351,3358,3388,2713,2963,3366,2972,3214,3414,3417,3190,3377,3227,3201,3229,2876,3173,3267,3523,3537,3548,3570,3587,3155,3602,2854,2882,3133,339,284,3238,3177,2936,3626,2900,440,553,456,224,325,257,185,166,255,154,168,151,254,256,152,222,2,165,149,164,162,161,223,158,150,163,252,251,253,250,172,201,156,171,203,192,186,197,202,174,221,189,182,191,199,180,225,198,155,90,179,234,176,175,88,196,91,195,187,188,170,260,178,238,239,184,194,190,160,193,207,249,157])).
% 69.42/69.48 cnf(3649,plain,
% 69.42/69.48 (P4(x36491,x36491,x36492)),
% 69.42/69.48 inference(rename_variables,[],[3333])).
% 69.42/69.48 cnf(3655,plain,
% 69.42/69.48 (P4(x36551,x36552,f12(x36551,x36551,a15,a15,x36551,x36552))),
% 69.42/69.48 inference(scs_inference,[],[142,3364,3409,3528,3532,3573,3619,3319,3463,3466,3540,3543,3553,3559,3562,3576,3589,3595,3608,3615,3321,3554,3627,3383,3333,3460,3471,3594,3630,3649,3145,3313,3446,3325,3305,3323,3640,3137,3287,3299,3301,3315,3327,3341,3351,3358,3388,2713,2963,3366,2972,3214,3414,3417,3190,3377,3227,3201,3229,2876,3173,3267,3523,3537,3548,3570,3587,3155,3602,3641,2854,2882,3133,339,284,3238,3028,3177,2936,3626,2900,3631,440,553,456,224,325,257,185,166,255,154,168,151,254,256,152,222,2,165,149,164,162,161,223,158,150,163,252,251,253,250,172,201,156,171,203,192,186,197,202,174,221,189,182,191,199,180,225,198,155,90,179,234,176,175,88,196,91,195,187,188,170,260,178,238,239,184,194,190,160,193,207,249,157,206,204])).
% 69.42/69.48 cnf(3682,plain,
% 69.42/69.48 (~P6(a14,a17,a15,a17)),
% 69.42/69.48 inference(scs_inference,[],[3522,437])).
% 69.42/69.48 cnf(3685,plain,
% 69.42/69.48 (P4(f11(x36851,x36851,x36851,x36851,x36852),x36851,x36852)),
% 69.42/69.48 inference(rename_variables,[],[3593])).
% 69.42/69.48 cnf(3688,plain,
% 69.42/69.48 (P1(f11(x36881,x36881,x36881,x36881,x36882),x36881,x36881,x36882)),
% 69.42/69.48 inference(rename_variables,[],[3588])).
% 69.42/69.48 cnf(3691,plain,
% 69.42/69.48 (P4(f11(x36911,x36911,x36911,x36911,x36912),x36911,x36912)),
% 69.42/69.48 inference(rename_variables,[],[3593])).
% 69.42/69.48 cnf(3697,plain,
% 69.42/69.48 (P9(a17,a16,a17,a16,a16,a17,a16,a17)),
% 69.42/69.48 inference(scs_inference,[],[3481,3307,3556,3588,3593,3685,440,456,325,224,185,257])).
% 69.42/69.48 cnf(3699,plain,
% 69.42/69.48 (P6(x36991,x36991,x36991,x36992)),
% 69.42/69.48 inference(scs_inference,[],[3522,3481,3307,3556,3588,3593,3685,440,456,325,224,185,257,166])).
% 69.42/69.48 cnf(3703,plain,
% 69.42/69.48 (P9(a16,a17,a17,a16,a16,a17,a17,a16)),
% 69.42/69.48 inference(scs_inference,[],[3522,3481,3307,3556,3588,3593,3685,3647,440,456,325,224,185,257,166,151,255])).
% 69.42/69.48 cnf(3709,plain,
% 69.42/69.48 (P5(f20(x37091,x37092),x37092,x37091)),
% 69.42/69.48 inference(scs_inference,[],[3522,3481,3622,3307,3556,3525,3588,3593,3685,3647,440,456,325,224,185,257,166,151,255,168,154,152])).
% 69.42/69.48 cnf(3713,plain,
% 69.42/69.48 (P9(a16,a17,a16,a17,a16,a17,a17,a16)),
% 69.42/69.48 inference(scs_inference,[],[3522,3481,3622,3307,3479,3487,3556,3525,3588,3593,3685,3647,440,456,325,224,185,257,166,151,255,168,154,152,256,254])).
% 69.42/69.48 cnf(3715,plain,
% 69.42/69.48 (P4(x37151,f11(x37151,x37151,x37151,x37151,x37152),x37152)),
% 69.42/69.48 inference(scs_inference,[],[3522,3481,3622,3307,3479,3487,3556,3525,3588,3593,3685,3691,3647,440,456,325,224,185,257,166,151,255,168,154,152,256,254,149])).
% 69.42/69.48 cnf(3717,plain,
% 69.42/69.48 (P7(x37171,a15,a15,x37171)),
% 69.42/69.48 inference(scs_inference,[],[3522,3481,3622,3307,3479,3487,3556,3525,3588,3593,3685,3691,3647,440,456,325,224,185,257,166,151,255,168,154,152,256,254,149,169])).
% 69.42/69.48 cnf(3719,plain,
% 69.42/69.48 (P10(x37191,x37191,x37191,a15,a15,x37191,a15,a15)),
% 69.42/69.48 inference(scs_inference,[],[3522,3481,3622,3307,3479,3487,3556,3525,3588,3593,3685,3691,3647,440,456,325,224,185,257,166,151,255,168,154,152,256,254,149,169,222])).
% 69.42/69.48 cnf(3722,plain,
% 69.42/69.48 (P6(x37221,x37222,x37222,x37222)),
% 69.42/69.48 inference(scs_inference,[],[3522,3481,3622,3307,3479,3487,3556,3575,3525,3588,3593,3685,3691,3647,440,456,325,224,185,257,166,151,255,168,154,152,256,254,149,169,222,2,165])).
% 69.42/69.48 cnf(3724,plain,
% 69.42/69.48 (P7(a15,x37241,x37241,a15)),
% 69.42/69.48 inference(scs_inference,[],[3522,3481,3622,3307,3479,3487,3556,3575,3525,3588,3593,3685,3691,3647,440,456,325,224,185,257,166,151,255,168,154,152,256,254,149,169,222,2,165,167])).
% 69.42/69.48 cnf(3726,plain,
% 69.42/69.48 (P3(a16,a16,a16,a15)),
% 69.42/69.48 inference(scs_inference,[],[3522,3481,3622,3307,3479,3487,3556,3575,3525,3588,3593,3685,3691,3647,440,456,325,224,185,257,166,151,255,168,154,152,256,254,149,169,222,2,165,167,231])).
% 69.42/69.48 cnf(3728,plain,
% 69.42/69.48 (P3(a14,a16,a1,a15)),
% 69.42/69.48 inference(scs_inference,[],[3522,3465,3481,3622,3307,3479,3487,3556,3575,3525,3588,3593,3685,3691,3647,440,456,325,224,185,257,166,151,255,168,154,152,256,254,149,169,222,2,165,167,231,161])).
% 69.42/69.48 cnf(3732,plain,
% 69.42/69.48 (P1(a17,a16,a14,a1)),
% 69.42/69.48 inference(scs_inference,[],[3522,3465,3481,3622,3307,3479,3487,3512,3556,3575,3525,3588,3593,3685,3691,3647,3094,440,456,325,224,185,257,166,151,255,168,154,152,256,254,149,169,222,2,165,167,231,161,158,164])).
% 69.42/69.48 cnf(3734,plain,
% 69.42/69.48 (P10(a1,a15,x37341,x37342,a14,a16,x37341,x37342)),
% 69.42/69.48 inference(scs_inference,[],[3522,3465,3481,3622,3307,3479,3487,3512,3556,3575,3525,3588,3593,3685,3691,3647,3094,440,456,325,224,185,257,166,151,255,168,154,152,256,254,149,169,222,2,165,167,231,161,158,164,223])).
% 69.42/69.48 cnf(3738,plain,
% 69.42/69.48 (P4(f11(x37381,x37381,x37381,x37381,x37382),x37382,x37381)),
% 69.42/69.48 inference(scs_inference,[],[3522,3465,3481,3622,3307,3479,3487,3504,3512,3556,3575,3525,3588,3593,3685,3691,3647,3094,440,456,325,224,185,257,166,151,255,168,154,152,256,254,149,169,222,2,165,167,231,161,158,164,223,162,150])).
% 69.42/69.48 cnf(3740,plain,
% 69.42/69.48 (P1(a16,a17,a1,a14)),
% 69.42/69.48 inference(scs_inference,[],[3522,3462,3465,3481,3622,3307,3479,3487,3504,3512,3556,3575,3525,3588,3593,3685,3691,3647,3094,440,456,325,224,185,257,166,151,255,168,154,152,256,254,149,169,222,2,165,167,231,161,158,164,223,162,150,163])).
% 69.42/69.48 cnf(3753,plain,
% 69.42/69.48 (P1(x37531,x37532,x37531,x37532)),
% 69.42/69.48 inference(rename_variables,[],[3319])).
% 69.42/69.48 cnf(3756,plain,
% 69.42/69.48 (P1(a15,a15,x37561,x37561)),
% 69.42/69.48 inference(rename_variables,[],[3613])).
% 69.42/69.48 cnf(3759,plain,
% 69.42/69.48 (P4(x37591,x37591,x37592)),
% 69.42/69.48 inference(rename_variables,[],[3333])).
% 69.42/69.48 cnf(3762,plain,
% 69.42/69.48 (P7(a16,a17,a15,a15)),
% 69.42/69.48 inference(scs_inference,[],[3522,3004,3493,3462,3465,3481,3506,3613,3622,3307,3468,3479,3487,3504,3512,3556,3575,3525,3588,3593,3685,3691,3647,3655,3319,3333,3094,3414,440,456,325,224,185,257,166,151,255,168,154,152,256,254,149,169,222,2,165,167,231,161,158,164,223,162,150,163,252,251,253,250,243,248,171,153,183])).
% 69.42/69.48 cnf(3765,plain,
% 69.42/69.48 (P4(f11(x37651,x37651,x37651,x37651,x37652),x37651,x37652)),
% 69.42/69.48 inference(rename_variables,[],[3593])).
% 69.42/69.48 cnf(3781,plain,
% 69.42/69.48 (P1(x37811,x37812,x37812,x37811)),
% 69.42/69.48 inference(rename_variables,[],[3267])).
% 69.42/69.48 cnf(3786,plain,
% 69.42/69.48 (P1(x37861,x37862,x37862,x37861)),
% 69.42/69.48 inference(rename_variables,[],[3267])).
% 69.42/69.48 cnf(3792,plain,
% 69.42/69.48 (P2(a16,a16,a15,a15)),
% 69.42/69.48 inference(scs_inference,[],[3522,3004,3493,3462,3465,3481,3506,3613,3622,3307,3468,3477,3479,3487,3504,3512,3556,3575,3601,3525,3588,3593,3685,3691,3647,3444,3655,3530,3319,3753,3333,3094,3267,3781,3414,3301,3061,3305,440,456,325,224,185,257,166,151,255,168,154,152,256,254,149,169,222,2,165,167,231,161,158,164,223,162,150,163,252,251,253,250,243,248,171,153,183,159,203,201,247,115,156,192,174,197,186,221,191,182])).
% 69.42/69.48 cnf(3797,plain,
% 69.42/69.48 (P1(x37971,x37972,x37972,x37971)),
% 69.42/69.48 inference(rename_variables,[],[3267])).
% 69.42/69.48 cnf(3800,plain,
% 69.42/69.48 (P5(f24(x38001,x38001,x38001,x38001,x38001,x38001),x38001,x38001)),
% 69.42/69.48 inference(rename_variables,[],[3525])).
% 69.42/69.48 cnf(3808,plain,
% 69.42/69.48 (P5(f24(x38081,x38081,x38081,x38081,x38081,x38081),x38081,x38081)),
% 69.42/69.48 inference(rename_variables,[],[3525])).
% 69.42/69.48 cnf(3818,plain,
% 69.42/69.48 (P1(a15,a15,x38181,x38181)),
% 69.42/69.48 inference(rename_variables,[],[3613])).
% 69.42/69.48 cnf(3821,plain,
% 69.42/69.48 (P1(x38211,x38212,x38212,x38211)),
% 69.42/69.48 inference(rename_variables,[],[3267])).
% 69.42/69.48 cnf(3824,plain,
% 69.42/69.48 (P1(x38241,x38242,x38242,x38241)),
% 69.42/69.48 inference(rename_variables,[],[3267])).
% 69.42/69.48 cnf(3827,plain,
% 69.42/69.48 (P1(x38271,x38272,x38272,x38271)),
% 69.42/69.48 inference(rename_variables,[],[3267])).
% 69.42/69.48 cnf(3850,plain,
% 69.42/69.48 (P5(f24(x38501,x38501,x38501,x38501,x38501,x38501),x38501,x38501)),
% 69.42/69.48 inference(rename_variables,[],[3525])).
% 69.42/69.48 cnf(3859,plain,
% 69.42/69.48 (P5(x38591,x38591,f24(x38591,x38591,x38591,x38591,x38591,x38591))),
% 69.42/69.48 inference(scs_inference,[],[142,1065,3522,3004,3493,3462,3465,3481,3506,3516,3613,3756,3818,3622,3307,3468,3477,3479,3487,3504,3512,3520,3556,3575,3577,3601,3607,3534,3525,3800,3808,3850,3588,3688,3593,3685,3691,3765,3647,3444,3655,3390,3530,3319,3753,3333,3759,3094,3161,3175,3173,3267,3781,3786,3797,3821,3824,3827,3155,3323,3414,3301,3377,3061,3305,3299,2900,345,440,456,325,224,185,257,166,151,255,168,154,152,256,254,149,169,222,2,165,167,231,161,158,164,223,162,150,163,252,251,253,250,243,248,171,153,183,159,203,201,247,115,156,192,174,197,186,221,191,182,199,189,225,198,179,155,234,180,196,176,187,175,170,188,260,178,238,239,190,249,553,242,160])).
% 69.42/69.48 cnf(3880,plain,
% 69.42/69.48 (P5(f20(x38801,x38802),x38802,x38801)),
% 69.42/69.48 inference(rename_variables,[],[3709])).
% 69.42/69.48 cnf(3883,plain,
% 69.42/69.48 (P4(f11(x38831,x38831,x38831,x38831,x38832),x38832,x38831)),
% 69.42/69.48 inference(rename_variables,[],[3738])).
% 69.42/69.48 cnf(3886,plain,
% 69.42/69.48 (P5(f20(x38861,x38862),x38862,x38861)),
% 69.42/69.48 inference(rename_variables,[],[3709])).
% 69.42/69.48 cnf(3889,plain,
% 69.42/69.48 (P4(f11(x38891,x38891,x38891,x38891,x38892),x38892,x38891)),
% 69.42/69.48 inference(rename_variables,[],[3738])).
% 69.42/69.48 cnf(3956,plain,
% 69.42/69.48 ($false),
% 69.42/69.48 inference(scs_inference,[],[3682,3699,3722,3343,3697,3403,3728,3719,3717,3724,3734,3428,3489,3496,3703,3713,3726,3732,3740,3762,3792,3859,3475,3617,3715,3738,3883,3889,3597,3709,3880,3886,3145,3522,3409,3434,440,2741,325,456,224,166,185,151,257,154,168,255,152,254,256,149,222,165,169,167,2,231,161,223,164,162,150,163,252,253,251,250,261,241,171,181]),
% 69.42/69.48 ['proof']).
% 69.42/69.48 % SZS output end Proof
% 69.42/69.48 % Total time :68.780000s
%------------------------------------------------------------------------------