%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : GEO555+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 : n022.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:43 EDT 2024
% Result : Theorem 59.34s 59.51s
% Output : CNFRefutation 59.42s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.02/0.09 % Problem : GEO555+1 : TPTP v8.2.0. Released v7.5.0.
% 0.02/0.09 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% 0.09/0.29 % Computer : n022.cluster.edu
% 0.09/0.29 % Model : x86_64 x86_64
% 0.09/0.29 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.29 % Memory : 8042.1875MB
% 0.09/0.29 % OS : Linux 3.10.0-693.el7.x86_64
% 0.09/0.29 % CPULimit : 300
% 0.09/0.29 % WCLimit : 300
% 0.09/0.29 % DateTime : Fri Jun 21 10:09:38 EDT 2024
% 0.09/0.29 % CPUTime :
% 0.15/0.50 start to proof:theBenchmark
% 59.34/59.50 %-------------------------------------------
% 59.34/59.50 % File :CSE---1.7
% 59.34/59.50 % Problem :theBenchmark
% 59.34/59.50 % Transform :cnf
% 59.34/59.50 % Format :tptp:raw
% 59.34/59.50 % Command :java -jar mcs_scs.jar %d %s
% 59.34/59.50
% 59.34/59.50 % Result :Theorem 58.870000s
% 59.34/59.50 % Output :CNFRefutation 58.870000s
% 59.34/59.50 %-------------------------------------------
% 59.34/59.51 %------------------------------------------------------------------------------
% 59.34/59.51 % File : GEO555+1 : TPTP v8.2.0. Released v7.5.0.
% 59.34/59.51 % Domain : Geometry
% 59.34/59.51 % Problem : JGEX problem 15
% 59.34/59.51 % Version : [CGZ00] axioms.
% 59.34/59.51 % English :
% 59.34/59.51
% 59.34/59.51 % Refs : [CGZ00] Chou et al. (2000), A Deductive Database Approach to A
% 59.34/59.51 % : [YCG08] Ye et al. (2008), An Introduction to Java Geometry Exp
% 59.34/59.51 % : [Qua20] Quaresma (2020), Email to Geoff Sutcliffe
% 59.34/59.51 % Source : [Qua20]
% 59.34/59.51 % Names : 15.p [Qua20]
% 59.34/59.51
% 59.34/59.51 % Status : Theorem
% 59.34/59.51 % Rating : 0.33 v8.2.0, 0.39 v8.1.0, 0.44 v7.5.0
% 59.34/59.51 % Syntax : Number of formulae : 95 ( 0 unt; 0 def)
% 59.34/59.51 % Number of atoms : 298 ( 1 equ)
% 59.34/59.51 % Maximal formula atoms : 15 ( 3 avg)
% 59.34/59.51 % Number of connectives : 210 ( 7 ~; 0 |; 108 &)
% 59.34/59.51 % ( 0 <=>; 95 =>; 0 <=; 0 <~>)
% 59.34/59.51 % Maximal formula depth : 25 ( 9 avg)
% 59.34/59.51 % Maximal term depth : 1 ( 1 avg)
% 59.34/59.51 % Number of predicates : 12 ( 11 usr; 0 prp; 2-8 aty)
% 59.34/59.51 % Number of functors : 0 ( 0 usr; 0 con; --- aty)
% 59.34/59.51 % Number of variables : 532 ( 512 !; 20 ?)
% 59.34/59.51 % SPC : FOF_THM_RFO_SEQ
% 59.34/59.51
% 59.34/59.51 % Comments : Taken from JGEX [YCG08], converted by Pedro Quaresma.
% 59.34/59.51 %------------------------------------------------------------------------------
% 59.34/59.51 include('Axioms/GEO012+0.ax').
% 59.34/59.51 %------------------------------------------------------------------------------
% 59.34/59.51 fof(exemplo6GDDFULL012015,conjecture,
% 59.34/59.51 ! [A,B,C,D,E,F,G,H,K,I] :
% 59.34/59.51 ( ( perp(D,A,B,C)
% 59.34/59.51 & coll(D,B,C)
% 59.34/59.51 & perp(E,B,A,C)
% 59.34/59.51 & coll(E,A,C)
% 59.34/59.51 & perp(F,C,A,B)
% 59.34/59.51 & coll(F,A,B)
% 59.34/59.51 & perp(G,F,B,C)
% 59.34/59.51 & coll(G,B,C)
% 59.34/59.51 & perp(H,F,A,C)
% 59.34/59.51 & coll(H,A,C)
% 59.34/59.51 & perp(K,E,A,B)
% 59.34/59.51 & coll(K,A,B)
% 59.34/59.51 & perp(I,D,A,B)
% 59.34/59.51 & coll(I,A,B) )
% 59.34/59.51 => cyclic(H,K,I,G) ) ).
% 59.34/59.51
% 59.34/59.51 %------------------------------------------------------------------------------
% 59.34/59.51 %-------------------------------------------
% 59.34/59.51 % Proof found
% 59.34/59.51 % SZS status Theorem for theBenchmark
% 59.34/59.51 % SZS output start Proof
% 59.34/59.52 %ClaNum:269(EqnAxiom:141)
% 59.34/59.52 %VarNum:1613(SingletonVarNum:590)
% 59.34/59.52 %MaxLitNum:5
% 59.34/59.52 %MaxfuncDepth:1
% 59.34/59.52 %SharedTerms:25
% 59.34/59.52 %goalClause: 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156
% 59.34/59.52 %singleGoalClaCount:15
% 59.34/59.52 [142]P1(a1,a2,a16)
% 59.34/59.52 [143]P1(a17,a3,a16)
% 59.34/59.52 [144]P1(a18,a3,a2)
% 59.34/59.52 [145]P1(a19,a2,a16)
% 59.34/59.52 [146]P1(a20,a3,a16)
% 59.34/59.52 [147]P1(a21,a3,a2)
% 59.34/59.52 [148]P1(a22,a3,a2)
% 59.34/59.52 [149]P3(a1,a3,a2,a16)
% 59.34/59.52 [150]P3(a17,a2,a3,a16)
% 59.34/59.52 [151]P3(a18,a16,a3,a2)
% 59.34/59.52 [152]P3(a19,a18,a2,a16)
% 59.34/59.52 [153]P3(a20,a18,a3,a16)
% 59.34/59.52 [154]P3(a21,a17,a3,a2)
% 59.34/59.52 [155]P3(a22,a1,a3,a2)
% 59.34/59.52 [156]~P4(a20,a21,a22,a19)
% 59.34/59.52 [157]~P1(x1572,x1571,x1573)+P1(x1571,x1572,x1573)
% 59.34/59.52 [158]~P1(x1581,x1583,x1582)+P1(x1581,x1582,x1583)
% 59.34/59.52 [159]~P7(x1591,x1592,x1593)+P1(x1591,x1592,x1593)
% 59.34/59.52 [160]~P7(x1601,x1603,x1602)+P7(x1601,x1602,x1603)
% 59.34/59.52 [162]~P7(x1621,x1622,x1623)+P5(x1621,x1622,x1621,x1623)
% 59.34/59.52 [166]~P10(x1661,x1662,x1661,x1663)+P1(x1661,x1662,x1663)
% 59.34/59.52 [232]~P5(x2321,x2322,x2321,x2323)+P9(x2321,x2322,x2322,x2323,x2322,x2323,x2321,x2323)
% 59.42/59.52 [169]~P10(x1693,x1694,x1691,x1692)+P10(x1691,x1692,x1693,x1694)
% 59.42/59.52 [170]~P10(x1701,x1702,x1704,x1703)+P10(x1701,x1702,x1703,x1704)
% 59.42/59.52 [171]~P3(x1713,x1714,x1711,x1712)+P3(x1711,x1712,x1713,x1714)
% 59.42/59.52 [172]~P3(x1721,x1722,x1724,x1723)+P3(x1721,x1722,x1723,x1724)
% 59.42/59.52 [173]~P5(x1733,x1734,x1731,x1732)+P5(x1731,x1732,x1733,x1734)
% 59.42/59.52 [174]~P5(x1741,x1742,x1744,x1743)+P5(x1741,x1742,x1743,x1744)
% 59.42/59.52 [175]~P4(x1752,x1751,x1753,x1754)+P4(x1751,x1752,x1753,x1754)
% 59.42/59.52 [176]~P4(x1761,x1763,x1762,x1764)+P4(x1761,x1762,x1763,x1764)
% 59.42/59.52 [177]~P4(x1771,x1772,x1774,x1773)+P4(x1771,x1772,x1773,x1774)
% 59.42/59.52 [230]~P4(x2302,x2303,x2301,x2304)+P9(x2301,x2302,x2301,x2303,x2304,x2302,x2304,x2303)
% 59.42/59.52 [193]~P2(x1934,x1931,x1932,x1933)+P3(f8(x1931,x1932,x1933,x1934),x1931,x1931,x1934)
% 59.42/59.52 [208]P5(x2081,x2082,x2083,x2084)+~P6(x2081,x2082,x2085,x2083,x2084,x2086)
% 59.42/59.52 [220]~P11(x2204,x2205,x2206,x2201,x2202,x2203)+P11(x2201,x2202,x2203,x2204,x2205,x2206)
% 59.42/59.52 [221]~P11(x2212,x2211,x2213,x2215,x2214,x2216)+P11(x2211,x2212,x2213,x2214,x2215,x2216)
% 59.42/59.52 [222]~P11(x2221,x2223,x2222,x2224,x2226,x2225)+P11(x2221,x2222,x2223,x2224,x2225,x2226)
% 59.42/59.52 [223]~P6(x2234,x2235,x2236,x2231,x2232,x2233)+P6(x2231,x2232,x2233,x2234,x2235,x2236)
% 59.42/59.52 [224]~P6(x2242,x2241,x2243,x2245,x2244,x2246)+P6(x2241,x2242,x2243,x2244,x2245,x2246)
% 59.42/59.52 [225]~P6(x2251,x2253,x2252,x2254,x2256,x2255)+P6(x2251,x2252,x2253,x2254,x2255,x2256)
% 59.42/59.52 [231]~P10(x2311,x2312,x2315,x2316)+P9(x2311,x2312,x2313,x2314,x2315,x2316,x2313,x2314)
% 59.42/59.52 [237]~P11(x2371,x2372,x2373,x2374,x2375,x2376)+P9(x2371,x2372,x2372,x2373,x2374,x2375,x2375,x2376)
% 59.42/59.52 [238]~P11(x2381,x2382,x2383,x2384,x2385,x2386)+P8(x2381,x2382,x2381,x2383,x2384,x2385,x2384,x2386)
% 59.42/59.52 [239]~P9(x2391,x2392,x2395,x2396,x2393,x2394,x2395,x2396)+P10(x2391,x2392,x2393,x2394)
% 59.42/59.52 [258]~P9(x2585,x2586,x2587,x2588,x2581,x2582,x2583,x2584)+P9(x2581,x2582,x2583,x2584,x2585,x2586,x2587,x2588)
% 59.42/59.52 [259]~P9(x2593,x2594,x2591,x2592,x2597,x2598,x2595,x2596)+P9(x2591,x2592,x2593,x2594,x2595,x2596,x2597,x2598)
% 59.42/59.52 [260]~P9(x2602,x2601,x2603,x2604,x2605,x2606,x2607,x2608)+P9(x2601,x2602,x2603,x2604,x2605,x2606,x2607,x2608)
% 59.42/59.52 [261]~P9(x2611,x2612,x2615,x2616,x2613,x2614,x2617,x2618)+P9(x2611,x2612,x2613,x2614,x2615,x2616,x2617,x2618)
% 59.42/59.52 [262]~P8(x2625,x2626,x2627,x2628,x2621,x2622,x2623,x2624)+P8(x2621,x2622,x2623,x2624,x2625,x2626,x2627,x2628)
% 59.42/59.52 [263]~P8(x2633,x2634,x2631,x2632,x2637,x2638,x2635,x2636)+P8(x2631,x2632,x2633,x2634,x2635,x2636,x2637,x2638)
% 59.42/59.52 [264]~P8(x2642,x2641,x2643,x2644,x2645,x2646,x2647,x2648)+P8(x2641,x2642,x2643,x2644,x2645,x2646,x2647,x2648)
% 59.42/59.52 [265]~P8(x2651,x2652,x2655,x2656,x2653,x2654,x2657,x2658)+P8(x2651,x2652,x2653,x2654,x2655,x2656,x2657,x2658)
% 59.42/59.52 [167]~P1(x1671,x1672,x1673)+~P5(x1671,x1672,x1671,x1673)+P7(x1671,x1672,x1673)
% 59.42/59.52 [241]P5(x2411,x2412,x2411,x2413)+~P9(x2411,x2412,x2412,x2413,x2412,x2413,x2411,x2413)+P1(x2411,x2412,x2413)
% 59.42/59.52 [182]~P3(x1821,x1822,x1822,x1823)+~P5(x1822,x1821,x1822,x1823)+P1(x1821,x1822,f4(x1821,x1823,x1822))
% 59.42/59.52 [194]~P3(x1942,x1941,x1941,x1943)+~P5(x1941,x1942,x1941,x1943)+P5(x1941,x1942,x1941,f4(x1942,x1943,x1941))
% 59.42/59.52 [161]~P1(x1613,x1614,x1611)+P1(x1611,x1612,x1613)+~P1(x1613,x1614,x1612)
% 59.42/59.52 [178]~P2(x1784,x1781,x1782,x1783)+P3(x1781,x1782,x1782,x1783)+~P1(x1784,x1781,x1783)
% 59.42/59.52 [179]~P3(x1791,x1794,x1792,x1793)+P5(x1791,x1792,x1791,x1793)+~P7(x1794,x1792,x1793)
% 59.42/59.52 [180]~P3(x1801,x1803,x1803,x1804)+P5(x1801,x1802,x1803,x1802)+~P7(x1802,x1801,x1804)
% 59.42/59.52 [187]~P5(x1871,x1874,x1872,x1874)+~P5(x1871,x1873,x1872,x1873)+P3(x1871,x1872,x1873,x1874)
% 59.42/59.52 [190]~P5(x1901,x1902,x1901,x1904)+~P5(x1901,x1902,x1901,x1903)+P2(x1901,x1902,x1903,x1904)
% 59.42/59.52 [236]~P10(x2361,x2364,x2363,x2362)+~P4(x2361,x2364,x2363,x2362)+P9(x2361,x2362,x2363,x2362,x2363,x2362,x2363,x2364)
% 59.42/59.52 [240]~P9(x2401,x2403,x2401,x2404,x2402,x2403,x2402,x2404)+P1(x2401,x2402,x2403)+P4(x2403,x2404,x2401,x2402)
% 59.42/59.52 [242]~P1(x2423,x2424,x2422)+~P9(x2423,x2421,x2423,x2422,x2424,x2421,x2424,x2422)+P4(x2421,x2422,x2423,x2424)
% 59.42/59.52 [244]P3(x2441,x2442,x2443,x2444)+~P9(x2441,x2442,x2443,x2444,x2443,x2444,x2441,x2442)+P10(x2441,x2442,x2443,x2444)
% 59.42/59.52 [183]~P3(x1831,x1834,x1832,x1833)+~P3(x1832,x1834,x1831,x1833)+P1(f5(x1831,x1832,x1833),x1833,x1832)
% 59.42/59.52 [184]~P3(x1841,x1844,x1842,x1843)+~P3(x1842,x1844,x1841,x1843)+P1(f6(x1841,x1842,x1843),x1843,x1841)
% 59.42/59.52 [195]~P3(x1951,x1954,x1952,x1953)+~P3(x1952,x1954,x1951,x1953)+P3(x1951,f5(x1951,x1952,x1953),x1953,x1952)
% 59.42/59.52 [196]~P3(x1961,x1964,x1962,x1963)+~P3(x1962,x1964,x1961,x1963)+P3(x1961,f6(x1962,x1961,x1963),x1963,x1962)
% 59.42/59.52 [197]~P3(x1971,x1973,x1973,x1972)+~P4(x1971,x1972,x1973,x1974)+P2(f9(x1971,x1972,x1973),x1971,x1972,x1973)
% 59.42/59.52 [199]~P3(x1993,x1994,x1992,x1991)+~P5(x1993,x1992,x1993,x1991)+P1(x1991,x1992,f25(x1992,x1991,x1993,x1994))
% 59.42/59.52 [200]~P3(x2003,x2004,x2001,x2002)+~P5(x2003,x2001,x2003,x2002)+P1(f25(x2001,x2002,x2003,x2004),x2003,x2004)
% 59.42/59.52 [251]~P5(x2513,x2512,x2513,x2511)+~P9(x2512,x2513,x2513,x2514,x2513,x2514,x2513,x2511)+P1(x2511,x2512,f23(x2512,x2511,x2513,x2514))
% 59.42/59.52 [252]~P3(x2523,x2524,x2522,x2521)+~P9(x2522,x2523,x2523,x2524,x2523,x2524,x2523,x2521)+P1(x2521,x2522,f26(x2522,x2521,x2523,x2524))
% 59.42/59.52 [253]~P3(x2533,x2532,x2532,x2531)+~P9(x2534,x2533,x2532,x2533,x2532,x2533,x2531,x2533)+P1(f15(x2531,x2532,x2533,x2534),x2533,x2534)
% 59.42/59.52 [254]~P3(x2543,x2542,x2542,x2541)+~P9(x2544,x2543,x2542,x2543,x2542,x2543,x2541,x2543)+P1(f15(x2541,x2542,x2543,x2544),x2541,x2542)
% 59.42/59.52 [255]~P5(x2553,x2551,x2553,x2552)+~P9(x2551,x2553,x2553,x2554,x2553,x2554,x2553,x2552)+P1(f23(x2551,x2552,x2553,x2554),x2553,x2554)
% 59.42/59.52 [256]~P3(x2563,x2564,x2561,x2562)+~P9(x2561,x2563,x2563,x2564,x2563,x2564,x2563,x2562)+P1(f26(x2561,x2562,x2563,x2564),x2563,x2564)
% 59.42/59.52 [163]~P7(x1635,x1631,x1633)+P10(x1631,x1632,x1633,x1634)+~P7(x1635,x1632,x1634)
% 59.42/59.52 [164]~P7(x1641,x1645,x1643)+P10(x1641,x1642,x1643,x1644)+~P7(x1642,x1645,x1644)
% 59.42/59.52 [191]~P4(x1915,x1911,x1912,x1913)+P4(x1911,x1912,x1913,x1914)+~P4(x1915,x1911,x1912,x1914)
% 59.42/59.52 [233]~P7(x2335,x2332,x2333)+~P2(x2334,x2331,x2332,x2333)+P9(x2331,x2332,x2331,x2333,x2334,x2332,x2334,x2335)
% 59.42/59.52 [235]~P2(x2355,x2351,x2353,x2354)+P9(x2351,x2352,x2351,x2353,x2354,x2351,x2354,x2353)+~P3(x2355,x2351,x2351,x2352)
% 59.42/59.52 [248]~P9(x2482,x2483,x2482,x2484,x2485,x2482,x2485,x2484)+P3(x2481,x2482,x2482,x2483)+~P2(x2481,x2482,x2484,x2485)
% 59.42/59.52 [203]~P1(x2032,x2034,x2035)+~P3(x2031,x2033,x2033,x2032)+P1(f13(x2031,x2032,x2033,x2034,x2035),x2034,x2035)
% 59.42/59.52 [204]~P1(x2042,x2044,x2045)+~P3(x2041,x2043,x2043,x2042)+P3(f13(x2041,x2042,x2043,x2044,x2045),x2041,x2044,x2045)
% 59.42/59.52 [205]~P3(x2053,x2054,x2054,x2051)+~P5(x2051,x2052,x2051,x2055)+P5(x2051,x2052,x2051,f29(x2053,x2054,x2052,x2055,x2051))
% 59.42/59.52 [206]~P3(x2063,x2061,x2061,x2065)+~P5(x2065,x2062,x2065,x2064)+P5(x2061,x2062,x2061,f29(x2063,x2061,x2062,x2064,x2065))
% 59.42/59.52 [207]~P3(x2071,x2072,x2072,x2075)+~P5(x2075,x2073,x2075,x2074)+P10(f29(x2071,x2072,x2073,x2074,x2075),x2073,x2071,x2072)
% 59.42/59.52 [250]~P9(x2501,x2503,x2502,x2503,x2501,x2504,x2502,x2505)+P1(x2501,x2502,x2503)+P4(x2504,x2502,x2503,f28(x2501,x2502,x2503,x2504))
% 59.42/59.52 [266]~P9(x2661,x2663,x2662,x2663,x2661,x2664,x2662,x2665)+P1(x2661,x2662,x2663)+P9(x2661,x2663,x2662,x2663,x2661,f28(x2661,x2662,x2663,x2664),x2662,f28(x2661,x2662,x2663,x2664))
% 59.42/59.52 [185]~P10(x1851,x1852,x1855,x1856)+P10(x1851,x1852,x1853,x1854)+~P10(x1855,x1856,x1853,x1854)
% 59.42/59.52 [186]~P3(x1861,x1862,x1865,x1866)+P10(x1861,x1862,x1863,x1864)+~P3(x1865,x1866,x1863,x1864)
% 59.42/59.52 [188]~P3(x1885,x1886,x1883,x1884)+P3(x1881,x1882,x1883,x1884)+~P10(x1881,x1882,x1885,x1886)
% 59.42/59.52 [189]~P5(x1891,x1892,x1895,x1896)+P5(x1891,x1892,x1893,x1894)+~P5(x1895,x1896,x1893,x1894)
% 59.42/59.52 [226]~P5(x2261,x2262,x2264,x2265)+~P11(x2261,x2262,x2263,x2264,x2265,x2266)+P6(x2261,x2262,x2263,x2264,x2265,x2266)
% 59.42/59.52 [229]~P7(x2294,x2295,x2296)+~P7(x2291,x2292,x2293)+P8(x2291,x2292,x2292,x2293,x2294,x2295,x2295,x2296)
% 59.42/59.52 [209]~P7(x2096,x2093,x2094)+~P7(x2095,x2091,x2092)+P7(f27(x2091,x2092,x2093,x2094,x2095,x2096),x2091,x2094)
% 59.42/59.52 [210]~P7(x2106,x2103,x2104)+~P7(x2105,x2101,x2102)+P10(f27(x2101,x2102,x2103,x2104,x2105,x2106),x2106,x2101,x2103)
% 59.42/59.52 [211]~P7(x2116,x2113,x2114)+~P7(x2115,x2111,x2112)+P10(f27(x2111,x2112,x2113,x2114,x2115,x2116),x2115,x2112,x2114)
% 59.42/59.52 [246]~P9(x2461,x2462,x2463,x2464,x2465,x2466,x2467,x2468)+P10(x2461,x2462,x2463,x2464)+~P10(x2465,x2466,x2467,x2468)
% 59.42/59.52 [247]~P9(x2471,x2472,x2473,x2474,x2475,x2476,x2477,x2478)+P3(x2471,x2472,x2473,x2474)+~P3(x2475,x2476,x2477,x2478)
% 59.42/59.52 [249]~P8(x2491,x2492,x2493,x2494,x2495,x2496,x2497,x2498)+P5(x2491,x2492,x2493,x2494)+~P5(x2495,x2496,x2497,x2498)
% 59.42/59.52 [227]~P11(x2271,x2272,x2273,x2277,x2278,x2279)+P11(x2271,x2272,x2273,x2274,x2275,x2276)+~P11(x2277,x2278,x2279,x2274,x2275,x2276)
% 59.42/59.52 [228]~P6(x2281,x2282,x2283,x2287,x2288,x2289)+P6(x2281,x2282,x2283,x2284,x2285,x2286)+~P6(x2287,x2288,x2289,x2284,x2285,x2286)
% 59.42/59.52 [268]~P9(x2681,x2682,x2683,x2684,x2689,x26810,x26811,x26812)+P9(x2681,x2682,x2683,x2684,x2685,x2686,x2687,x2688)+~P9(x2689,x26810,x26811,x26812,x2685,x2686,x2687,x2688)
% 59.42/59.52 [269]~P8(x2691,x2692,x2693,x2694,x2699,x26910,x26911,x26912)+P8(x2691,x2692,x2693,x2694,x2695,x2696,x2697,x2698)+~P8(x2699,x26910,x26911,x26912,x2695,x2696,x2697,x2698)
% 59.42/59.52 [201]~P5(x2012,x2011,x2014,x2011)+~P4(x2012,x2014,x2011,x2013)+P3(x2011,x2012,x2012,x2013)+~P5(x2012,x2013,x2014,x2013)
% 59.42/59.52 [168]~P1(x1681,x1682,x1683)+~P10(x1684,x1681,x1685,x1683)+P7(x1681,x1682,x1683)+~P7(x1684,x1682,x1685)
% 59.42/59.52 [181]~P10(x1814,x1813,x1815,x1812)+~P10(x1814,x1812,x1815,x1813)+P7(x1811,x1812,x1813)+~P7(x1811,x1814,x1815)
% 59.42/59.52 [202]~P5(x2025,x2021,x2025,x2023)+~P5(x2025,x2021,x2025,x2022)+P4(x2021,x2022,x2023,x2024)+~P5(x2025,x2021,x2025,x2024)
% 59.42/59.52 [234]~P1(x2341,x2344,x2345)+~P1(x2341,x2342,x2343)+~P10(x2342,x2344,x2343,x2345)+P8(x2341,x2342,x2342,x2343,x2341,x2344,x2344,x2345)
% 59.42/59.52 [245]~P1(x2451,x2452,x2453)+~P9(x2455,x2452,x2455,x2453,x2454,x2452,x2454,x2451)+P7(x2451,x2452,x2453)+~P2(x2454,x2455,x2452,x2453)
% 59.42/59.52 [192]~P3(x1923,x1921,x1923,x1925)+~P3(x1921,x1922,x1921,x1923)+~P7(x1924,x1922,x1925)+P7(f7(x1921,x1922,x1923),x1921,x1923)
% 59.42/59.52 [198]~P4(x1981,x1982,x1983,x1985)+~P10(x1981,x1982,x1983,x1985)+~P7(x1984,x1981,x1982)+P2(f10(x1981,x1982,x1983),x1981,x1982,x1983)
% 59.42/59.52 [267]~P9(x2671,x2673,x2672,x2673,x2674,x2676,x2675,x2676)+~P9(x2671,x2672,x2672,x2673,x2674,x2675,x2675,x2676)+P1(x2671,x2672,x2673)+P11(x2671,x2672,x2673,x2674,x2675,x2676)
% 59.42/59.52 [257]~P4(x2571,x2572,x2575,x2574)+~P4(x2571,x2572,x2575,x2573)+~P9(x2575,x2571,x2575,x2572,x2576,x2573,x2576,x2574)+P5(x2571,x2572,x2573,x2574)+~P4(x2571,x2572,x2575,x2576)
% 59.42/59.52 [212]~P1(x2122,x2123,x2124)+~P1(x2121,x2124,x2126)+~P1(x2121,x2123,x2125)+~P10(x2123,x2124,x2125,x2126)+P1(x2121,x2122,f14(x2123,x2124,x2125,x2126,x2121,x2122))
% 59.42/59.52 [213]~P1(x2136,x2131,x2132)+~P1(x2135,x2132,x2134)+~P1(x2135,x2131,x2133)+~P10(x2131,x2132,x2133,x2134)+P1(f14(x2131,x2132,x2133,x2134,x2135,x2136),x2133,x2134)
% 59.42/59.52 [214]~P1(x2143,x2144,x2145)+~P7(x2146,x2141,x2142)+~P10(x2141,x2143,x2145,x2146)+~P10(x2141,x2143,x2142,x2144)+P1(f30(x2141,x2142,x2143,x2144,x2145,x2146),x2146,x2145)
% 59.42/59.52 [215]~P1(x2153,x2154,x2155)+~P7(x2156,x2151,x2152)+~P10(x2151,x2153,x2155,x2156)+~P10(x2151,x2153,x2152,x2154)+P1(f30(x2151,x2152,x2153,x2154,x2155,x2156),x2151,x2154)
% 59.42/59.52 [216]~P5(x2162,x2163,x2162,x2164)+~P5(x2161,x2163,x2161,x2166)+~P2(x2161,x2163,x2164,x2165)+E(x2161,x2162)+P1(f11(x2163,x2164,x2165,x2166,x2161,x2162),x2163,x2165)
% 59.42/59.52 [217]~P5(x2172,x2173,x2172,x2174)+~P5(x2171,x2173,x2171,x2176)+~P2(x2171,x2173,x2174,x2175)+E(x2171,x2172)+P1(f12(x2173,x2174,x2175,x2176,x2171,x2172),x2174,x2176)
% 59.42/59.52 [218]~P5(x2182,x2183,x2182,x2184)+~P5(x2181,x2183,x2181,x2186)+~P2(x2181,x2183,x2184,x2185)+E(x2181,x2182)+P5(f11(x2183,x2184,x2185,x2186,x2181,x2182),x2182,x2182,x2183)
% 59.42/59.52 [219]~P5(x2192,x2193,x2192,x2194)+~P5(x2191,x2193,x2191,x2196)+~P2(x2191,x2193,x2194,x2195)+E(x2191,x2192)+P5(f12(x2193,x2194,x2195,x2196,x2191,x2192),x2192,x2192,x2193)
% 59.42/59.52 [165]~P1(x1653,x1651,x1654)+~P1(x1655,x1651,x1654)+~P7(x1656,x1655,x1653)+~P7(x1657,x1651,x1654)+P7(f24(x1651,x1652),x1651,x1652)
% 59.42/59.52 %EqnAxiom
% 59.42/59.52 [1]E(x11,x11)
% 59.42/59.52 [2]E(x22,x21)+~E(x21,x22)
% 59.42/59.52 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 59.42/59.52 [4]~E(x41,x42)+E(f24(x41,x43),f24(x42,x43))
% 59.42/59.52 [5]~E(x51,x52)+E(f24(x53,x51),f24(x53,x52))
% 59.42/59.52 [6]~E(x61,x62)+E(f4(x61,x63,x64),f4(x62,x63,x64))
% 59.42/59.52 [7]~E(x71,x72)+E(f4(x73,x71,x74),f4(x73,x72,x74))
% 59.42/59.52 [8]~E(x81,x82)+E(f4(x83,x84,x81),f4(x83,x84,x82))
% 59.42/59.52 [9]~E(x91,x92)+E(f5(x91,x93,x94),f5(x92,x93,x94))
% 59.42/59.52 [10]~E(x101,x102)+E(f5(x103,x101,x104),f5(x103,x102,x104))
% 59.42/59.52 [11]~E(x111,x112)+E(f5(x113,x114,x111),f5(x113,x114,x112))
% 59.42/59.52 [12]~E(x121,x122)+E(f6(x121,x123,x124),f6(x122,x123,x124))
% 59.42/59.52 [13]~E(x131,x132)+E(f6(x133,x131,x134),f6(x133,x132,x134))
% 59.42/59.52 [14]~E(x141,x142)+E(f6(x143,x144,x141),f6(x143,x144,x142))
% 59.42/59.52 [15]~E(x151,x152)+E(f7(x151,x153,x154),f7(x152,x153,x154))
% 59.42/59.52 [16]~E(x161,x162)+E(f7(x163,x161,x164),f7(x163,x162,x164))
% 59.42/59.52 [17]~E(x171,x172)+E(f7(x173,x174,x171),f7(x173,x174,x172))
% 59.42/59.52 [18]~E(x181,x182)+E(f8(x181,x183,x184,x185),f8(x182,x183,x184,x185))
% 59.42/59.52 [19]~E(x191,x192)+E(f8(x193,x191,x194,x195),f8(x193,x192,x194,x195))
% 59.42/59.52 [20]~E(x201,x202)+E(f8(x203,x204,x201,x205),f8(x203,x204,x202,x205))
% 59.42/59.52 [21]~E(x211,x212)+E(f8(x213,x214,x215,x211),f8(x213,x214,x215,x212))
% 59.42/59.52 [22]~E(x221,x222)+E(f28(x221,x223,x224,x225),f28(x222,x223,x224,x225))
% 59.42/59.52 [23]~E(x231,x232)+E(f28(x233,x231,x234,x235),f28(x233,x232,x234,x235))
% 59.42/59.52 [24]~E(x241,x242)+E(f28(x243,x244,x241,x245),f28(x243,x244,x242,x245))
% 59.42/59.52 [25]~E(x251,x252)+E(f28(x253,x254,x255,x251),f28(x253,x254,x255,x252))
% 59.42/59.52 [26]~E(x261,x262)+E(f23(x261,x263,x264,x265),f23(x262,x263,x264,x265))
% 59.42/59.52 [27]~E(x271,x272)+E(f23(x273,x271,x274,x275),f23(x273,x272,x274,x275))
% 59.42/59.52 [28]~E(x281,x282)+E(f23(x283,x284,x281,x285),f23(x283,x284,x282,x285))
% 59.42/59.52 [29]~E(x291,x292)+E(f23(x293,x294,x295,x291),f23(x293,x294,x295,x292))
% 59.42/59.52 [30]~E(x301,x302)+E(f26(x301,x303,x304,x305),f26(x302,x303,x304,x305))
% 59.42/59.52 [31]~E(x311,x312)+E(f26(x313,x311,x314,x315),f26(x313,x312,x314,x315))
% 59.42/59.52 [32]~E(x321,x322)+E(f26(x323,x324,x321,x325),f26(x323,x324,x322,x325))
% 59.42/59.52 [33]~E(x331,x332)+E(f26(x333,x334,x335,x331),f26(x333,x334,x335,x332))
% 59.42/59.52 [34]~E(x341,x342)+E(f9(x341,x343,x344),f9(x342,x343,x344))
% 59.42/59.52 [35]~E(x351,x352)+E(f9(x353,x351,x354),f9(x353,x352,x354))
% 59.42/59.52 [36]~E(x361,x362)+E(f9(x363,x364,x361),f9(x363,x364,x362))
% 59.42/59.52 [37]~E(x371,x372)+E(f10(x371,x373,x374),f10(x372,x373,x374))
% 59.42/59.52 [38]~E(x381,x382)+E(f10(x383,x381,x384),f10(x383,x382,x384))
% 59.42/59.52 [39]~E(x391,x392)+E(f10(x393,x394,x391),f10(x393,x394,x392))
% 59.42/59.52 [40]~E(x401,x402)+E(f25(x401,x403,x404,x405),f25(x402,x403,x404,x405))
% 59.42/59.52 [41]~E(x411,x412)+E(f25(x413,x411,x414,x415),f25(x413,x412,x414,x415))
% 59.42/59.52 [42]~E(x421,x422)+E(f25(x423,x424,x421,x425),f25(x423,x424,x422,x425))
% 59.42/59.52 [43]~E(x431,x432)+E(f25(x433,x434,x435,x431),f25(x433,x434,x435,x432))
% 59.42/59.52 [44]~E(x441,x442)+E(f15(x441,x443,x444,x445),f15(x442,x443,x444,x445))
% 59.42/59.52 [45]~E(x451,x452)+E(f15(x453,x451,x454,x455),f15(x453,x452,x454,x455))
% 59.42/59.52 [46]~E(x461,x462)+E(f15(x463,x464,x461,x465),f15(x463,x464,x462,x465))
% 59.42/59.52 [47]~E(x471,x472)+E(f15(x473,x474,x475,x471),f15(x473,x474,x475,x472))
% 59.42/59.52 [48]~E(x481,x482)+E(f13(x481,x483,x484,x485,x486),f13(x482,x483,x484,x485,x486))
% 59.42/59.52 [49]~E(x491,x492)+E(f13(x493,x491,x494,x495,x496),f13(x493,x492,x494,x495,x496))
% 59.42/59.53 [50]~E(x501,x502)+E(f13(x503,x504,x501,x505,x506),f13(x503,x504,x502,x505,x506))
% 59.42/59.53 [51]~E(x511,x512)+E(f13(x513,x514,x515,x511,x516),f13(x513,x514,x515,x512,x516))
% 59.42/59.53 [52]~E(x521,x522)+E(f13(x523,x524,x525,x526,x521),f13(x523,x524,x525,x526,x522))
% 59.42/59.53 [53]~E(x531,x532)+E(f12(x531,x533,x534,x535,x536,x537),f12(x532,x533,x534,x535,x536,x537))
% 59.42/59.53 [54]~E(x541,x542)+E(f12(x543,x541,x544,x545,x546,x547),f12(x543,x542,x544,x545,x546,x547))
% 59.42/59.53 [55]~E(x551,x552)+E(f12(x553,x554,x551,x555,x556,x557),f12(x553,x554,x552,x555,x556,x557))
% 59.42/59.53 [56]~E(x561,x562)+E(f12(x563,x564,x565,x561,x566,x567),f12(x563,x564,x565,x562,x566,x567))
% 59.42/59.53 [57]~E(x571,x572)+E(f12(x573,x574,x575,x576,x571,x577),f12(x573,x574,x575,x576,x572,x577))
% 59.42/59.53 [58]~E(x581,x582)+E(f12(x583,x584,x585,x586,x587,x581),f12(x583,x584,x585,x586,x587,x582))
% 59.42/59.53 [59]~E(x591,x592)+E(f29(x591,x593,x594,x595,x596),f29(x592,x593,x594,x595,x596))
% 59.42/59.53 [60]~E(x601,x602)+E(f29(x603,x601,x604,x605,x606),f29(x603,x602,x604,x605,x606))
% 59.42/59.53 [61]~E(x611,x612)+E(f29(x613,x614,x611,x615,x616),f29(x613,x614,x612,x615,x616))
% 59.42/59.53 [62]~E(x621,x622)+E(f29(x623,x624,x625,x621,x626),f29(x623,x624,x625,x622,x626))
% 59.42/59.53 [63]~E(x631,x632)+E(f29(x633,x634,x635,x636,x631),f29(x633,x634,x635,x636,x632))
% 59.42/59.53 [64]~E(x641,x642)+E(f11(x641,x643,x644,x645,x646,x647),f11(x642,x643,x644,x645,x646,x647))
% 59.42/59.53 [65]~E(x651,x652)+E(f11(x653,x651,x654,x655,x656,x657),f11(x653,x652,x654,x655,x656,x657))
% 59.42/59.53 [66]~E(x661,x662)+E(f11(x663,x664,x661,x665,x666,x667),f11(x663,x664,x662,x665,x666,x667))
% 59.42/59.53 [67]~E(x671,x672)+E(f11(x673,x674,x675,x671,x676,x677),f11(x673,x674,x675,x672,x676,x677))
% 59.42/59.53 [68]~E(x681,x682)+E(f11(x683,x684,x685,x686,x681,x687),f11(x683,x684,x685,x686,x682,x687))
% 59.42/59.53 [69]~E(x691,x692)+E(f11(x693,x694,x695,x696,x697,x691),f11(x693,x694,x695,x696,x697,x692))
% 59.42/59.53 [70]~E(x701,x702)+E(f30(x701,x703,x704,x705,x706,x707),f30(x702,x703,x704,x705,x706,x707))
% 59.42/59.53 [71]~E(x711,x712)+E(f30(x713,x711,x714,x715,x716,x717),f30(x713,x712,x714,x715,x716,x717))
% 59.42/59.53 [72]~E(x721,x722)+E(f30(x723,x724,x721,x725,x726,x727),f30(x723,x724,x722,x725,x726,x727))
% 59.42/59.53 [73]~E(x731,x732)+E(f30(x733,x734,x735,x731,x736,x737),f30(x733,x734,x735,x732,x736,x737))
% 59.42/59.53 [74]~E(x741,x742)+E(f30(x743,x744,x745,x746,x741,x747),f30(x743,x744,x745,x746,x742,x747))
% 59.42/59.53 [75]~E(x751,x752)+E(f30(x753,x754,x755,x756,x757,x751),f30(x753,x754,x755,x756,x757,x752))
% 59.42/59.53 [76]~E(x761,x762)+E(f27(x761,x763,x764,x765,x766,x767),f27(x762,x763,x764,x765,x766,x767))
% 59.42/59.53 [77]~E(x771,x772)+E(f27(x773,x771,x774,x775,x776,x777),f27(x773,x772,x774,x775,x776,x777))
% 59.42/59.53 [78]~E(x781,x782)+E(f27(x783,x784,x781,x785,x786,x787),f27(x783,x784,x782,x785,x786,x787))
% 59.42/59.53 [79]~E(x791,x792)+E(f27(x793,x794,x795,x791,x796,x797),f27(x793,x794,x795,x792,x796,x797))
% 59.42/59.53 [80]~E(x801,x802)+E(f27(x803,x804,x805,x806,x801,x807),f27(x803,x804,x805,x806,x802,x807))
% 59.42/59.53 [81]~E(x811,x812)+E(f27(x813,x814,x815,x816,x817,x811),f27(x813,x814,x815,x816,x817,x812))
% 59.42/59.53 [82]~E(x821,x822)+E(f14(x821,x823,x824,x825,x826,x827),f14(x822,x823,x824,x825,x826,x827))
% 59.42/59.53 [83]~E(x831,x832)+E(f14(x833,x831,x834,x835,x836,x837),f14(x833,x832,x834,x835,x836,x837))
% 59.42/59.53 [84]~E(x841,x842)+E(f14(x843,x844,x841,x845,x846,x847),f14(x843,x844,x842,x845,x846,x847))
% 59.42/59.53 [85]~E(x851,x852)+E(f14(x853,x854,x855,x851,x856,x857),f14(x853,x854,x855,x852,x856,x857))
% 59.42/59.53 [86]~E(x861,x862)+E(f14(x863,x864,x865,x866,x861,x867),f14(x863,x864,x865,x866,x862,x867))
% 59.42/59.53 [87]~E(x871,x872)+E(f14(x873,x874,x875,x876,x877,x871),f14(x873,x874,x875,x876,x877,x872))
% 59.42/59.53 [88]P1(x882,x883,x884)+~E(x881,x882)+~P1(x881,x883,x884)
% 59.42/59.53 [89]P1(x893,x892,x894)+~E(x891,x892)+~P1(x893,x891,x894)
% 59.42/59.53 [90]P1(x903,x904,x902)+~E(x901,x902)+~P1(x903,x904,x901)
% 59.42/59.53 [91]P8(x912,x913,x914,x915,x916,x917,x918,x919)+~E(x911,x912)+~P8(x911,x913,x914,x915,x916,x917,x918,x919)
% 59.42/59.53 [92]P8(x923,x922,x924,x925,x926,x927,x928,x929)+~E(x921,x922)+~P8(x923,x921,x924,x925,x926,x927,x928,x929)
% 59.42/59.53 [93]P8(x933,x934,x932,x935,x936,x937,x938,x939)+~E(x931,x932)+~P8(x933,x934,x931,x935,x936,x937,x938,x939)
% 59.42/59.53 [94]P8(x943,x944,x945,x942,x946,x947,x948,x949)+~E(x941,x942)+~P8(x943,x944,x945,x941,x946,x947,x948,x949)
% 59.42/59.53 [95]P8(x953,x954,x955,x956,x952,x957,x958,x959)+~E(x951,x952)+~P8(x953,x954,x955,x956,x951,x957,x958,x959)
% 59.42/59.53 [96]P8(x963,x964,x965,x966,x967,x962,x968,x969)+~E(x961,x962)+~P8(x963,x964,x965,x966,x967,x961,x968,x969)
% 59.42/59.53 [97]P8(x973,x974,x975,x976,x977,x978,x972,x979)+~E(x971,x972)+~P8(x973,x974,x975,x976,x977,x978,x971,x979)
% 59.42/59.53 [98]P8(x983,x984,x985,x986,x987,x988,x989,x982)+~E(x981,x982)+~P8(x983,x984,x985,x986,x987,x988,x989,x981)
% 59.42/59.53 [99]P5(x992,x993,x994,x995)+~E(x991,x992)+~P5(x991,x993,x994,x995)
% 59.42/59.53 [100]P5(x1003,x1002,x1004,x1005)+~E(x1001,x1002)+~P5(x1003,x1001,x1004,x1005)
% 59.42/59.53 [101]P5(x1013,x1014,x1012,x1015)+~E(x1011,x1012)+~P5(x1013,x1014,x1011,x1015)
% 59.42/59.53 [102]P5(x1023,x1024,x1025,x1022)+~E(x1021,x1022)+~P5(x1023,x1024,x1025,x1021)
% 59.42/59.53 [103]P9(x1032,x1033,x1034,x1035,x1036,x1037,x1038,x1039)+~E(x1031,x1032)+~P9(x1031,x1033,x1034,x1035,x1036,x1037,x1038,x1039)
% 59.42/59.53 [104]P9(x1043,x1042,x1044,x1045,x1046,x1047,x1048,x1049)+~E(x1041,x1042)+~P9(x1043,x1041,x1044,x1045,x1046,x1047,x1048,x1049)
% 59.42/59.53 [105]P9(x1053,x1054,x1052,x1055,x1056,x1057,x1058,x1059)+~E(x1051,x1052)+~P9(x1053,x1054,x1051,x1055,x1056,x1057,x1058,x1059)
% 59.42/59.53 [106]P9(x1063,x1064,x1065,x1062,x1066,x1067,x1068,x1069)+~E(x1061,x1062)+~P9(x1063,x1064,x1065,x1061,x1066,x1067,x1068,x1069)
% 59.42/59.53 [107]P9(x1073,x1074,x1075,x1076,x1072,x1077,x1078,x1079)+~E(x1071,x1072)+~P9(x1073,x1074,x1075,x1076,x1071,x1077,x1078,x1079)
% 59.42/59.53 [108]P9(x1083,x1084,x1085,x1086,x1087,x1082,x1088,x1089)+~E(x1081,x1082)+~P9(x1083,x1084,x1085,x1086,x1087,x1081,x1088,x1089)
% 59.42/59.53 [109]P9(x1093,x1094,x1095,x1096,x1097,x1098,x1092,x1099)+~E(x1091,x1092)+~P9(x1093,x1094,x1095,x1096,x1097,x1098,x1091,x1099)
% 59.42/59.53 [110]P9(x1103,x1104,x1105,x1106,x1107,x1108,x1109,x1102)+~E(x1101,x1102)+~P9(x1103,x1104,x1105,x1106,x1107,x1108,x1109,x1101)
% 59.42/59.53 [111]P11(x1112,x1113,x1114,x1115,x1116,x1117)+~E(x1111,x1112)+~P11(x1111,x1113,x1114,x1115,x1116,x1117)
% 59.42/59.53 [112]P11(x1123,x1122,x1124,x1125,x1126,x1127)+~E(x1121,x1122)+~P11(x1123,x1121,x1124,x1125,x1126,x1127)
% 59.42/59.53 [113]P11(x1133,x1134,x1132,x1135,x1136,x1137)+~E(x1131,x1132)+~P11(x1133,x1134,x1131,x1135,x1136,x1137)
% 59.42/59.53 [114]P11(x1143,x1144,x1145,x1142,x1146,x1147)+~E(x1141,x1142)+~P11(x1143,x1144,x1145,x1141,x1146,x1147)
% 59.42/59.53 [115]P11(x1153,x1154,x1155,x1156,x1152,x1157)+~E(x1151,x1152)+~P11(x1153,x1154,x1155,x1156,x1151,x1157)
% 59.42/59.53 [116]P11(x1163,x1164,x1165,x1166,x1167,x1162)+~E(x1161,x1162)+~P11(x1163,x1164,x1165,x1166,x1167,x1161)
% 59.42/59.53 [117]P7(x1172,x1173,x1174)+~E(x1171,x1172)+~P7(x1171,x1173,x1174)
% 59.42/59.53 [118]P7(x1183,x1182,x1184)+~E(x1181,x1182)+~P7(x1183,x1181,x1184)
% 59.42/59.53 [119]P7(x1193,x1194,x1192)+~E(x1191,x1192)+~P7(x1193,x1194,x1191)
% 59.42/59.53 [120]P3(x1202,x1203,x1204,x1205)+~E(x1201,x1202)+~P3(x1201,x1203,x1204,x1205)
% 59.42/59.53 [121]P3(x1213,x1212,x1214,x1215)+~E(x1211,x1212)+~P3(x1213,x1211,x1214,x1215)
% 59.42/59.53 [122]P3(x1223,x1224,x1222,x1225)+~E(x1221,x1222)+~P3(x1223,x1224,x1221,x1225)
% 59.42/59.53 [123]P3(x1233,x1234,x1235,x1232)+~E(x1231,x1232)+~P3(x1233,x1234,x1235,x1231)
% 59.42/59.53 [124]P10(x1242,x1243,x1244,x1245)+~E(x1241,x1242)+~P10(x1241,x1243,x1244,x1245)
% 59.42/59.53 [125]P10(x1253,x1252,x1254,x1255)+~E(x1251,x1252)+~P10(x1253,x1251,x1254,x1255)
% 59.42/59.53 [126]P10(x1263,x1264,x1262,x1265)+~E(x1261,x1262)+~P10(x1263,x1264,x1261,x1265)
% 59.42/59.53 [127]P10(x1273,x1274,x1275,x1272)+~E(x1271,x1272)+~P10(x1273,x1274,x1275,x1271)
% 59.42/59.53 [128]P4(x1282,x1283,x1284,x1285)+~E(x1281,x1282)+~P4(x1281,x1283,x1284,x1285)
% 59.42/59.53 [129]P4(x1293,x1292,x1294,x1295)+~E(x1291,x1292)+~P4(x1293,x1291,x1294,x1295)
% 59.42/59.53 [130]P4(x1303,x1304,x1302,x1305)+~E(x1301,x1302)+~P4(x1303,x1304,x1301,x1305)
% 59.42/59.53 [131]P4(x1313,x1314,x1315,x1312)+~E(x1311,x1312)+~P4(x1313,x1314,x1315,x1311)
% 59.42/59.53 [132]P2(x1322,x1323,x1324,x1325)+~E(x1321,x1322)+~P2(x1321,x1323,x1324,x1325)
% 59.42/59.53 [133]P2(x1333,x1332,x1334,x1335)+~E(x1331,x1332)+~P2(x1333,x1331,x1334,x1335)
% 59.42/59.53 [134]P2(x1343,x1344,x1342,x1345)+~E(x1341,x1342)+~P2(x1343,x1344,x1341,x1345)
% 59.42/59.53 [135]P2(x1353,x1354,x1355,x1352)+~E(x1351,x1352)+~P2(x1353,x1354,x1355,x1351)
% 59.42/59.53 [136]P6(x1362,x1363,x1364,x1365,x1366,x1367)+~E(x1361,x1362)+~P6(x1361,x1363,x1364,x1365,x1366,x1367)
% 59.42/59.53 [137]P6(x1373,x1372,x1374,x1375,x1376,x1377)+~E(x1371,x1372)+~P6(x1373,x1371,x1374,x1375,x1376,x1377)
% 59.42/59.53 [138]P6(x1383,x1384,x1382,x1385,x1386,x1387)+~E(x1381,x1382)+~P6(x1383,x1384,x1381,x1385,x1386,x1387)
% 59.42/59.53 [139]P6(x1393,x1394,x1395,x1392,x1396,x1397)+~E(x1391,x1392)+~P6(x1393,x1394,x1395,x1391,x1396,x1397)
% 59.42/59.53 [140]P6(x1403,x1404,x1405,x1406,x1402,x1407)+~E(x1401,x1402)+~P6(x1403,x1404,x1405,x1406,x1401,x1407)
% 59.42/59.53 [141]P6(x1413,x1414,x1415,x1416,x1417,x1412)+~E(x1411,x1412)+~P6(x1413,x1414,x1415,x1416,x1417,x1411)
% 59.42/59.53
% 59.42/59.53 %-------------------------------------------
% 59.42/59.53 cnf(270,plain,
% 59.42/59.53 (~P4(a21,a20,a22,a19)),
% 59.42/59.53 inference(scs_inference,[],[156,175])).
% 59.42/59.53 cnf(272,plain,
% 59.42/59.53 (~P4(a20,a22,a21,a19)),
% 59.42/59.53 inference(scs_inference,[],[156,175,176])).
% 59.42/59.53 cnf(274,plain,
% 59.42/59.53 (~P4(a20,a21,a19,a22)),
% 59.42/59.53 inference(scs_inference,[],[156,175,176,177])).
% 59.42/59.53 cnf(278,plain,
% 59.42/59.53 (~P3(x2781,x2782,a1,a3)+P10(x2781,x2782,a2,a16)),
% 59.42/59.53 inference(scs_inference,[],[142,149,156,175,176,177,161,186])).
% 59.42/59.53 cnf(290,plain,
% 59.42/59.53 (~P4(a21,a20,a19,a22)),
% 59.42/59.53 inference(scs_inference,[],[270,177])).
% 59.42/59.53 cnf(292,plain,
% 59.42/59.53 (~P4(a21,a22,a20,a19)),
% 59.42/59.53 inference(scs_inference,[],[270,177,176])).
% 59.42/59.53 cnf(294,plain,
% 59.42/59.53 (~P4(a22,a20,a21,a19)),
% 59.42/59.53 inference(scs_inference,[],[270,272,177,176,175])).
% 59.42/59.53 cnf(296,plain,
% 59.42/59.53 (P1(a16,a16,a17)),
% 59.42/59.53 inference(scs_inference,[],[143,270,272,177,176,175,161])).
% 59.42/59.53 cnf(306,plain,
% 59.42/59.53 (~P4(a21,a22,a19,a20)),
% 59.42/59.53 inference(scs_inference,[],[292,177])).
% 59.42/59.53 cnf(308,plain,
% 59.42/59.53 (~P4(a22,a21,a20,a19)),
% 59.42/59.53 inference(scs_inference,[],[292,177,175])).
% 59.42/59.53 cnf(310,plain,
% 59.42/59.53 (~P4(a20,a19,a21,a22)),
% 59.42/59.53 inference(scs_inference,[],[274,292,177,175,176])).
% 59.42/59.53 cnf(312,plain,
% 59.42/59.53 (P1(a2,a2,a18)),
% 59.42/59.53 inference(scs_inference,[],[144,274,292,177,175,176,161])).
% 59.42/59.53 cnf(314,plain,
% 59.42/59.53 (~P3(x3141,x3142,a18,a16)+P10(x3141,x3142,a3,a2)),
% 59.42/59.53 inference(scs_inference,[],[144,151,274,292,177,175,176,161,186])).
% 59.42/59.53 cnf(333,plain,
% 59.42/59.53 (~P4(a21,a19,a20,a22)),
% 59.42/59.53 inference(scs_inference,[],[290,176])).
% 59.42/59.53 cnf(335,plain,
% 59.42/59.53 (~P4(a22,a21,a19,a20)),
% 59.42/59.53 inference(scs_inference,[],[290,306,176,175])).
% 59.42/59.53 cnf(337,plain,
% 59.42/59.53 (~P4(a22,a20,a19,a21)),
% 59.42/59.53 inference(scs_inference,[],[290,294,306,176,175,177])).
% 59.42/59.53 cnf(341,plain,
% 59.42/59.53 (~P3(x3411,x3412,a20,a18)+P10(x3411,x3412,a3,a16)),
% 59.42/59.53 inference(scs_inference,[],[145,153,290,294,306,176,175,177,161,186])).
% 59.42/59.53 cnf(360,plain,
% 59.42/59.53 (~P4(a20,a19,a22,a21)),
% 59.42/59.53 inference(scs_inference,[],[310,177])).
% 59.42/59.53 cnf(362,plain,
% 59.42/59.53 (~P4(a22,a19,a21,a20)),
% 59.42/59.53 inference(scs_inference,[],[310,335,177,176])).
% 59.42/59.53 cnf(364,plain,
% 59.42/59.53 (~P4(a19,a20,a21,a22)),
% 59.42/59.53 inference(scs_inference,[],[310,335,177,176,175])).
% 59.42/59.53 cnf(370,plain,
% 59.42/59.53 (~P3(x3701,x3702,a21,a17)+P10(x3701,x3702,a3,a2)),
% 59.42/59.53 inference(scs_inference,[],[142,146,154,310,335,177,176,175,161,89,121,186])).
% 59.42/59.53 cnf(380,plain,
% 59.42/59.53 (~P4(a19,a21,a20,a22)),
% 59.42/59.53 inference(scs_inference,[],[333,175])).
% 59.42/59.53 cnf(382,plain,
% 59.42/59.53 (~P4(a22,a19,a20,a21)),
% 59.42/59.53 inference(scs_inference,[],[333,337,175,176])).
% 59.42/59.53 cnf(384,plain,
% 59.42/59.53 (~P4(a21,a19,a22,a20)),
% 59.42/59.53 inference(scs_inference,[],[333,337,175,176,177])).
% 59.42/59.53 cnf(386,plain,
% 59.42/59.53 (P1(a2,a2,a21)),
% 59.42/59.53 inference(scs_inference,[],[147,333,337,175,176,177,161])).
% 59.42/59.53 cnf(388,plain,
% 59.42/59.53 (~P3(x3881,x3882,a22,a1)+P10(x3881,x3882,a3,a2)),
% 59.42/59.53 inference(scs_inference,[],[147,155,333,337,175,176,177,161,186])).
% 59.42/59.53 cnf(405,plain,
% 59.42/59.53 (~P4(a19,a20,a22,a21)),
% 59.42/59.53 inference(scs_inference,[],[364,177])).
% 59.42/59.53 cnf(409,plain,
% 59.42/59.53 (~P4(a20,a22,a19,a21)),
% 59.42/59.53 inference(scs_inference,[],[360,362,364,177,175,176])).
% 59.42/59.53 cnf(411,plain,
% 59.42/59.53 (P1(a2,a2,a22)),
% 59.42/59.53 inference(scs_inference,[],[148,360,362,364,177,175,176,161])).
% 59.42/59.53 cnf(417,plain,
% 59.42/59.53 (~P3(x4171,x4172,a19,a18)+P10(x4171,x4172,a2,a16)),
% 59.42/59.53 inference(scs_inference,[],[142,148,151,152,308,360,362,364,177,175,176,161,88,120,242,186])).
% 59.42/59.53 cnf(427,plain,
% 59.42/59.53 (~P4(a19,a22,a20,a21)),
% 59.42/59.53 inference(scs_inference,[],[405,176])).
% 59.42/59.53 cnf(429,plain,
% 59.42/59.53 (~P4(a19,a21,a22,a20)),
% 59.42/59.53 inference(scs_inference,[],[405,384,176,175])).
% 59.42/59.53 cnf(442,plain,
% 59.42/59.53 (~P3(x4421,x4422,a17,a2)+P10(x4421,x4422,a3,a16)),
% 59.42/59.53 inference(scs_inference,[],[150,296,161,186])).
% 59.42/59.53 cnf(492,plain,
% 59.42/59.53 (P1(a21,a21,a2)),
% 59.42/59.53 inference(scs_inference,[],[386,161])).
% 59.42/59.53 cnf(860,plain,
% 59.42/59.53 (P5(x8601,x8602,x8601,x8603)+~P7(x8601,x8603,x8602)),
% 59.42/59.53 inference(scs_inference,[],[160,162])).
% 59.42/59.53 cnf(894,plain,
% 59.42/59.53 (P10(a3,a2,x8941,x8942)+~P3(x8941,x8942,a18,a16)),
% 59.42/59.53 inference(scs_inference,[],[314,169])).
% 59.42/59.53 cnf(913,plain,
% 59.42/59.53 (P10(x9131,x9132,a2,a3)+~P3(x9131,x9132,a21,a17)),
% 59.42/59.53 inference(scs_inference,[],[370,170])).
% 59.42/59.53 cnf(922,plain,
% 59.42/59.53 (P10(a3,a16,x9221,x9222)+~P3(x9221,x9222,a17,a2)),
% 59.42/59.53 inference(scs_inference,[],[442,169])).
% 59.42/59.53 cnf(927,plain,
% 59.42/59.53 (P10(a3,a2,a3,a2)),
% 59.42/59.53 inference(scs_inference,[],[151,894,171])).
% 59.42/59.53 cnf(986,plain,
% 59.42/59.53 (~P7(x9861,a3,a3)+P7(x9861,a2,a2)),
% 59.42/59.53 inference(scs_inference,[],[927,181])).
% 59.42/59.53 cnf(1233,plain,
% 59.42/59.53 (P10(a3,a2,a2,a3)),
% 59.42/59.53 inference(scs_inference,[],[154,913,171])).
% 59.42/59.53 cnf(1238,plain,
% 59.42/59.53 (~P3(a2,a3,x12381,x12382)+P3(a3,a2,x12381,x12382)),
% 59.42/59.53 inference(scs_inference,[],[1233,127,126,125,124,188])).
% 59.42/59.53 cnf(1287,plain,
% 59.42/59.53 (P10(a3,a16,a3,a16)),
% 59.42/59.53 inference(scs_inference,[],[150,922,171])).
% 59.42/59.53 cnf(1328,plain,
% 59.42/59.53 (~P7(x13281,a3,a3)+P7(x13281,a16,a16)),
% 59.42/59.53 inference(scs_inference,[],[1287,181])).
% 59.42/59.53 cnf(1330,plain,
% 59.42/59.53 (~P7(x13301,a3,a3)+P5(x13301,a16,x13301,a16)),
% 59.42/59.53 inference(scs_inference,[],[1287,181,860])).
% 59.42/59.53 cnf(1424,plain,
% 59.42/59.53 (P9(x14241,a16,a16,a16,a16,a16,x14241,a16)+~P7(x14241,a3,a3)),
% 59.42/59.53 inference(scs_inference,[],[1330,232])).
% 59.42/59.53 cnf(1941,plain,
% 59.42/59.53 (P8(a18,a3,a3,a2,a18,a3,a3,a2)+~P10(a2,a2,a3,a3)),
% 59.42/59.53 inference(scs_inference,[],[144,234,169])).
% 59.42/59.53 cnf(1948,plain,
% 59.42/59.53 (~P10(a2,a2,a16,a16)+P8(a1,a2,a2,a16,a1,a2,a2,a16)),
% 59.42/59.53 inference(scs_inference,[],[142,234])).
% 59.42/59.53 cnf(2070,plain,
% 59.42/59.53 (P8(a2,a2,a2,a21,a2,a2,a2,a21)+~P10(a21,a21,a2,a2)),
% 59.42/59.53 inference(scs_inference,[],[386,234,169])).
% 59.42/59.53 cnf(2091,plain,
% 59.42/59.53 (~P10(a21,a21,a2,a2)+P8(a21,a21,a21,a2,a21,a21,a21,a2)),
% 59.42/59.53 inference(scs_inference,[],[492,234])).
% 59.42/59.53 cnf(4396,plain,
% 59.42/59.53 (P10(a3,a16,a16,a3)),
% 59.42/59.53 inference(scs_inference,[],[1287,170])).
% 59.42/59.53 cnf(4398,plain,
% 59.42/59.53 (P9(a3,a2,x43981,x43982,a2,a3,x43981,x43982)),
% 59.42/59.53 inference(scs_inference,[],[1233,1287,170,231])).
% 59.42/59.53 cnf(4400,plain,
% 59.42/59.53 (P1(a2,a1,a16)),
% 59.42/59.53 inference(scs_inference,[],[142,1233,1287,170,231,157])).
% 59.42/59.53 cnf(4402,plain,
% 59.42/59.53 (P1(a1,a16,a2)),
% 59.42/59.53 inference(scs_inference,[],[142,1233,1287,170,231,157,158])).
% 59.42/59.53 cnf(4404,plain,
% 59.42/59.53 (P9(x44041,x44042,a3,a2,x44041,x44042,a2,a3)),
% 59.42/59.53 inference(scs_inference,[],[142,1233,1287,170,231,157,158,259])).
% 59.42/59.53 cnf(4406,plain,
% 59.42/59.53 (P9(a2,a3,x44061,x44062,a3,a2,x44061,x44062)),
% 59.42/59.53 inference(scs_inference,[],[142,1233,1287,170,231,157,158,259,258])).
% 59.42/59.53 cnf(4408,plain,
% 59.42/59.53 (P1(a3,a2,a2)),
% 59.42/59.53 inference(scs_inference,[],[142,1233,927,1287,170,231,157,158,259,258,166])).
% 59.42/59.53 cnf(4410,plain,
% 59.42/59.53 (P10(a2,a3,a3,a2)),
% 59.42/59.53 inference(scs_inference,[],[142,1233,927,1287,170,231,157,158,259,258,166,169])).
% 59.42/59.53 cnf(4412,plain,
% 59.42/59.53 (P3(a3,a2,a21,a17)),
% 59.42/59.53 inference(scs_inference,[],[142,154,1233,927,1287,170,231,157,158,259,258,166,169,171])).
% 59.42/59.53 cnf(4414,plain,
% 59.42/59.53 (P9(a2,a3,x44141,x44142,a2,a3,x44141,x44142)),
% 59.42/59.53 inference(scs_inference,[],[142,154,1233,927,1287,170,231,157,158,259,258,166,169,171,260])).
% 59.42/59.53 cnf(4416,plain,
% 59.42/59.53 (P3(a21,a17,a2,a3)),
% 59.42/59.53 inference(scs_inference,[],[142,154,1233,927,1287,170,231,157,158,259,258,166,169,171,260,172])).
% 59.42/59.54 cnf(4418,plain,
% 59.42/59.54 (P10(a2,a3,a2,a3)),
% 59.42/59.54 inference(scs_inference,[],[142,154,1233,927,1287,170,231,157,158,259,258,166,169,171,260,172,185])).
% 59.42/59.54 cnf(4420,plain,
% 59.42/59.54 (P4(a3,a21,a2,a2)),
% 59.42/59.54 inference(scs_inference,[],[142,386,154,1233,927,1287,170,231,157,158,259,258,166,169,171,260,172,185,242])).
% 59.42/59.54 cnf(4424,plain,
% 59.42/59.54 (P10(a21,a17,a21,a17)),
% 59.42/59.54 inference(scs_inference,[],[142,386,154,1233,927,1287,170,231,157,158,259,258,166,169,171,260,172,185,242,268,186])).
% 59.42/59.54 cnf(4426,plain,
% 59.42/59.54 (P9(a3,a2,a2,a3,a2,a21,a2,a21)),
% 59.42/59.54 inference(scs_inference,[],[142,386,154,1233,927,1287,170,231,157,158,259,258,166,169,171,260,172,185,242,268,186,261])).
% 59.42/59.54 cnf(4428,plain,
% 59.42/59.54 (P4(a3,a2,a21,a2)),
% 59.42/59.54 inference(scs_inference,[],[142,386,154,1233,927,1287,170,231,157,158,259,258,166,169,171,260,172,185,242,268,186,261,176])).
% 59.42/59.54 cnf(4430,plain,
% 59.42/59.54 (P4(a21,a3,a2,a2)),
% 59.42/59.54 inference(scs_inference,[],[142,386,154,1233,927,1287,170,231,157,158,259,258,166,169,171,260,172,185,242,268,186,261,176,175])).
% 59.42/59.54 cnf(4432,plain,
% 59.42/59.54 (~P4(x44321,a19,a22,a21)+~P4(x44321,a19,a22,a20)),
% 59.42/59.54 inference(scs_inference,[],[142,427,386,154,1233,927,1287,170,231,157,158,259,258,166,169,171,260,172,185,242,268,186,261,176,175,191])).
% 59.42/59.54 cnf(4434,plain,
% 59.42/59.54 (P9(a21,a3,a21,a2,a2,a3,a2,a2)),
% 59.42/59.54 inference(scs_inference,[],[142,427,386,154,1233,927,1287,170,231,157,158,259,258,166,169,171,260,172,185,242,268,186,261,176,175,191,230])).
% 59.42/59.54 cnf(4436,plain,
% 59.42/59.54 (P4(a3,a2,a2,a21)),
% 59.42/59.54 inference(scs_inference,[],[142,427,386,154,1233,927,1287,170,231,157,158,259,258,166,169,171,260,172,185,242,268,186,261,176,175,191,230,177])).
% 59.42/59.54 cnf(4440,plain,
% 59.42/59.54 (P9(a3,a16,x44401,x44402,a16,a3,x44401,x44402)),
% 59.42/59.54 inference(scs_inference,[],[4396,231])).
% 59.42/59.54 cnf(4446,plain,
% 59.42/59.54 (P10(a21,a17,a17,a21)),
% 59.42/59.54 inference(scs_inference,[],[4398,4396,4424,4430,231,261,230,170])).
% 59.42/59.54 cnf(4448,plain,
% 59.42/59.54 (P10(a2,a21,a2,a21)),
% 59.42/59.54 inference(scs_inference,[],[4398,4396,4424,4430,231,261,230,170,239])).
% 59.42/59.54 cnf(4450,plain,
% 59.42/59.54 (P9(x44501,x44502,a2,a3,x44501,x44502,a3,a2)),
% 59.42/59.54 inference(scs_inference,[],[4398,4406,4396,4424,4430,231,261,230,170,239,259])).
% 59.42/59.54 cnf(4452,plain,
% 59.42/59.54 (P1(a2,a16,a1)),
% 59.42/59.54 inference(scs_inference,[],[4400,4398,4406,4396,4424,4430,231,261,230,170,239,259,158])).
% 59.42/59.54 cnf(4454,plain,
% 59.42/59.54 (P1(a2,a3,a3)),
% 59.42/59.54 inference(scs_inference,[],[4418,4400,4398,4406,4396,4424,4430,231,261,230,170,239,259,158,166])).
% 59.42/59.54 cnf(4456,plain,
% 59.42/59.54 (P4(a2,a3,a21,a2)),
% 59.42/59.54 inference(scs_inference,[],[4418,4400,4398,4406,4396,4424,4428,4430,231,261,230,170,239,259,158,166,175])).
% 59.42/59.54 cnf(4458,plain,
% 59.42/59.54 (P1(a16,a1,a2)),
% 59.42/59.54 inference(scs_inference,[],[4418,4400,4402,4398,4406,4396,4424,4428,4430,231,261,230,170,239,259,158,166,175,157])).
% 59.42/59.54 cnf(4460,plain,
% 59.42/59.54 (P4(a21,a2,a3,a2)),
% 59.42/59.54 inference(scs_inference,[],[4418,4400,4402,4398,4406,4396,4424,4428,4430,231,261,230,170,239,259,158,166,175,157,176])).
% 59.42/59.54 cnf(4466,plain,
% 59.42/59.54 (P9(x44661,x44662,a3,a2,x44662,x44661,a2,a3)),
% 59.42/59.54 inference(scs_inference,[],[4418,4400,4402,4398,4404,4406,4396,4424,4426,4428,4430,231,261,230,170,239,259,158,166,175,157,176,258,169,260])).
% 59.42/59.54 cnf(4470,plain,
% 59.42/59.54 (P3(a3,a2,a17,a21)),
% 59.42/59.54 inference(scs_inference,[],[4418,4400,4402,4412,4398,4404,4406,4396,4416,4424,4426,4428,4430,231,261,230,170,239,259,158,166,175,157,176,258,169,260,171,172])).
% 59.42/59.54 cnf(4474,plain,
% 59.42/59.54 (P4(a3,a22,a2,a2)),
% 59.42/59.54 inference(scs_inference,[],[4410,4418,4400,4402,4412,4398,4404,4406,4414,4396,4416,4424,4426,4428,4430,411,231,261,230,170,239,259,158,166,175,157,176,258,169,260,171,172,188,242])).
% 59.42/59.54 cnf(4477,plain,
% 59.42/59.54 (P3(a22,a1,a2,a3)),
% 59.42/59.54 inference(scs_inference,[],[4410,4418,4400,4402,4412,4398,4404,4406,4414,4396,4416,4424,4426,4428,4430,411,155,231,261,230,170,239,259,158,166,175,157,176,258,169,260,171,172,188,242,247])).
% 59.42/59.54 cnf(4479,plain,
% 59.42/59.54 (P4(a21,a2,a2,a2)),
% 59.42/59.54 inference(scs_inference,[],[4410,4418,4400,4402,4412,4398,4404,4406,4414,4396,4416,4420,4424,4426,4428,4430,411,155,231,261,230,170,239,259,158,166,175,157,176,258,169,260,171,172,188,242,247,191])).
% 59.42/59.54 cnf(4481,plain,
% 59.42/59.54 (P4(a2,a3,a2,a21)),
% 59.42/59.54 inference(scs_inference,[],[4410,4418,4400,4402,4412,4398,4404,4406,4414,4396,4416,4420,4424,4426,4428,4430,411,155,231,261,230,170,239,259,158,166,175,157,176,258,169,260,171,172,188,242,247,191,177])).
% 59.42/59.54 cnf(4485,plain,
% 59.42/59.54 (~P4(a19,a21,x44851,a20)+~E(x44851,a22)),
% 59.42/59.54 inference(scs_inference,[],[4410,4418,4400,4402,4412,4398,4404,4406,4414,4396,4416,4420,4424,4426,4428,4430,429,411,155,231,261,230,170,239,259,158,166,175,157,176,258,169,260,171,172,188,242,247,191,177,184,130])).
% 59.42/59.54 cnf(4488,plain,
% 59.42/59.54 (P9(a21,a3,a2,a3,a21,a2,a2,a2)),
% 59.42/59.54 inference(scs_inference,[],[4434,261])).
% 59.42/59.54 cnf(4490,plain,
% 59.42/59.54 (P4(a21,a2,a2,a3)),
% 59.42/59.54 inference(scs_inference,[],[4434,4460,261,177])).
% 59.42/59.54 cnf(4492,plain,
% 59.42/59.54 (P9(a2,a21,x44921,x44922,a2,a21,x44921,x44922)),
% 59.42/59.54 inference(scs_inference,[],[4434,4448,4460,261,177,231])).
% 59.42/59.54 cnf(4494,plain,
% 59.42/59.54 (P10(a2,a21,a21,a2)),
% 59.42/59.54 inference(scs_inference,[],[4434,4448,4460,261,177,231,170])).
% 59.42/59.54 cnf(4496,plain,
% 59.42/59.54 (P1(a16,a2,a1)),
% 59.42/59.54 inference(scs_inference,[],[4434,4448,4458,4460,261,177,231,170,158])).
% 59.42/59.54 cnf(4498,plain,
% 59.42/59.54 (P9(a21,a2,a21,a3,a2,a2,a2,a3)),
% 59.42/59.54 inference(scs_inference,[],[4434,4448,4458,4460,261,177,231,170,158,259])).
% 59.42/59.54 cnf(4500,plain,
% 59.42/59.54 (P9(a2,a3,a2,a2,a21,a3,a21,a2)),
% 59.42/59.54 inference(scs_inference,[],[4436,4434,4448,4458,4460,261,177,231,170,158,259,230])).
% 59.42/59.54 cnf(4504,plain,
% 59.42/59.54 (P1(a2,a3,a2)),
% 59.42/59.54 inference(scs_inference,[],[4436,4434,4448,4440,4408,4458,4460,261,177,231,170,158,259,230,258,157])).
% 59.42/59.54 cnf(4506,plain,
% 59.42/59.54 (P1(a2,a21,a21)),
% 59.42/59.54 inference(scs_inference,[],[4436,4434,4448,4440,4408,4458,4460,261,177,231,170,158,259,230,258,157,166])).
% 59.42/59.54 cnf(4508,plain,
% 59.42/59.54 (P4(a2,a21,a3,a2)),
% 59.42/59.54 inference(scs_inference,[],[4436,4434,4448,4440,4408,4456,4458,4460,261,177,231,170,158,259,230,258,157,166,176])).
% 59.42/59.54 cnf(4510,plain,
% 59.42/59.54 (P10(a17,a21,a21,a17)),
% 59.42/59.54 inference(scs_inference,[],[4436,4434,4448,4440,4408,4446,4456,4458,4460,261,177,231,170,158,259,230,258,157,166,176,169])).
% 59.42/59.54 cnf(4512,plain,
% 59.42/59.54 (P4(a22,a3,a2,a2)),
% 59.42/59.54 inference(scs_inference,[],[4436,4434,4448,4440,4408,4446,4456,4458,4460,4474,261,177,231,170,158,259,230,258,157,166,176,169,175])).
% 59.42/59.54 cnf(4514,plain,
% 59.42/59.54 (P9(a3,a21,a21,a2,a2,a3,a2,a2)),
% 59.42/59.54 inference(scs_inference,[],[4436,4434,4448,4440,4408,4446,4456,4458,4460,4474,261,177,231,170,158,259,230,258,157,166,176,169,175,260])).
% 59.42/59.54 cnf(4516,plain,
% 59.42/59.54 (P3(a17,a21,a3,a2)),
% 59.42/59.54 inference(scs_inference,[],[4436,4470,4434,4448,4440,4408,4446,4456,4458,4460,4474,261,177,231,170,158,259,230,258,157,166,176,169,175,260,171])).
% 59.42/59.54 cnf(4518,plain,
% 59.42/59.54 (P3(a20,a18,a16,a3)),
% 59.42/59.54 inference(scs_inference,[],[4436,4470,4434,4448,4440,4408,4446,4456,4458,4460,4474,153,261,177,231,170,158,259,230,258,157,166,176,169,175,260,171,172])).
% 59.42/59.54 cnf(4520,plain,
% 59.42/59.54 (P10(a16,a3,a16,a3)),
% 59.42/59.54 inference(scs_inference,[],[4436,4470,4434,4448,4440,4408,4446,4456,4458,4460,4474,4396,153,261,177,231,170,158,259,230,258,157,166,176,169,175,260,171,172,246])).
% 59.42/59.54 cnf(4522,plain,
% 59.42/59.54 (P4(a3,a18,a2,a2)),
% 59.42/59.54 inference(scs_inference,[],[4436,4470,4434,4448,4440,4408,4446,4456,4458,4460,4474,4414,4396,153,312,261,177,231,170,158,259,230,258,157,166,176,169,175,260,171,172,246,242])).
% 59.42/59.54 cnf(4525,plain,
% 59.42/59.54 (P3(a1,a22,a3,a2)),
% 59.42/59.54 inference(scs_inference,[],[4436,4470,4434,4448,4440,4466,4408,4446,4456,4458,4460,4474,4477,4414,4396,153,312,261,177,231,170,158,259,230,258,157,166,176,169,175,260,171,172,246,242,247])).
% 59.42/59.54 cnf(4571,plain,
% 59.42/59.54 (P4(a2,a21,a2,a3)),
% 59.42/59.54 inference(scs_inference,[],[4508,177])).
% 59.42/59.54 cnf(4573,plain,
% 59.42/59.54 (P9(a2,a3,a21,a3,a2,a2,a21,a2)),
% 59.42/59.54 inference(scs_inference,[],[4500,4508,177,261])).
% 59.42/59.54 cnf(4575,plain,
% 59.42/59.54 (P1(a2,a2,a3)),
% 59.42/59.54 inference(scs_inference,[],[4500,4508,4504,177,261,158])).
% 59.42/59.54 cnf(4577,plain,
% 59.42/59.54 (P10(a17,a21,a17,a21)),
% 59.42/59.54 inference(scs_inference,[],[4500,4508,4504,4510,177,261,158,170])).
% 59.42/59.54 cnf(4579,plain,
% 59.42/59.54 (P9(a2,a2,a2,a3,a21,a2,a21,a3)),
% 59.42/59.54 inference(scs_inference,[],[4481,4500,4508,4504,4510,177,261,158,170,230])).
% 59.42/59.54 cnf(4581,plain,
% 59.42/59.54 (P9(a2,a21,x45811,x45812,a21,a2,x45811,x45812)),
% 59.42/59.54 inference(scs_inference,[],[4481,4500,4508,4494,4504,4510,177,261,158,170,230,231])).
% 59.42/59.54 cnf(4585,plain,
% 59.42/59.54 (P9(x45851,x45852,a2,a21,x45851,x45852,a2,a21)),
% 59.42/59.54 inference(scs_inference,[],[4481,4500,4508,4492,4494,4504,4510,177,261,158,170,230,231,169,259])).
% 59.42/59.54 cnf(4589,plain,
% 59.42/59.54 (P1(a16,a3,a3)),
% 59.42/59.54 inference(scs_inference,[],[4481,4500,4508,4492,4479,4494,4504,4510,4520,177,261,158,170,230,231,169,259,175,166])).
% 59.42/59.54 cnf(4591,plain,
% 59.42/59.54 (P4(a2,a2,a3,a21)),
% 59.42/59.54 inference(scs_inference,[],[4481,4500,4508,4492,4479,4494,4504,4510,4520,177,261,158,170,230,231,169,259,175,166,176])).
% 59.42/59.54 cnf(4593,plain,
% 59.42/59.54 (P9(a21,a2,a2,a2,a21,a3,a2,a3)),
% 59.42/59.54 inference(scs_inference,[],[4481,4500,4508,4492,4479,4488,4494,4504,4510,4520,177,261,158,170,230,231,169,259,175,166,176,258])).
% 59.42/59.54 cnf(4595,plain,
% 59.42/59.54 (P1(a3,a2,a3)),
% 59.42/59.54 inference(scs_inference,[],[4481,4500,4508,4492,4454,4479,4488,4494,4504,4510,4520,177,261,158,170,230,231,169,259,175,166,176,258,157])).
% 59.42/59.54 cnf(4597,plain,
% 59.42/59.54 (P9(a3,a2,a2,a2,a21,a3,a21,a2)),
% 59.42/59.54 inference(scs_inference,[],[4481,4500,4508,4492,4454,4479,4488,4494,4504,4510,4520,177,261,158,170,230,231,169,259,175,166,176,258,157,260])).
% 59.42/59.54 cnf(4601,plain,
% 59.42/59.54 (P3(a16,a3,a20,a18)),
% 59.42/59.54 inference(scs_inference,[],[4481,4500,4508,4492,4454,4479,4488,4494,4504,4510,4516,4518,4520,177,261,158,170,230,231,169,259,175,166,176,258,157,260,172,171])).
% 59.42/59.54 cnf(4606,plain,
% 59.42/59.54 (P3(a1,a22,a2,a3)),
% 59.42/59.54 inference(scs_inference,[],[4481,4500,4508,4450,4492,4454,4479,4488,4494,4504,4510,4516,4518,4520,4525,386,177,261,158,170,230,231,169,259,175,166,176,258,157,260,172,171,242,247])).
% 59.42/59.54 cnf(4609,plain,
% 59.42/59.54 (P8(a2,a2,a2,a3,a2,a3,a3,a2)),
% 59.42/59.54 inference(scs_inference,[],[4481,4500,4508,4450,4492,4454,4479,4488,4494,4504,4510,4516,4518,4520,4525,4410,386,177,261,158,170,230,231,169,259,175,166,176,258,157,260,172,171,242,247,234])).
% 59.42/59.54 cnf(4611,plain,
% 59.42/59.54 (P8(a2,a3,a2,a2,a3,a2,a2,a3)),
% 59.42/59.54 inference(scs_inference,[],[4481,4500,4508,4450,4492,4454,4479,4488,4494,4504,4510,4516,4518,4520,4525,4410,386,177,261,158,170,230,231,169,259,175,166,176,258,157,260,172,171,242,247,234,263])).
% 59.42/59.54 cnf(4613,plain,
% 59.42/59.54 (P8(a2,a3,a3,a2,a2,a2,a2,a3)),
% 59.42/59.54 inference(scs_inference,[],[4481,4500,4508,4450,4492,4454,4479,4488,4494,4504,4510,4516,4518,4520,4525,4410,386,177,261,158,170,230,231,169,259,175,166,176,258,157,260,172,171,242,247,234,263,262])).
% 59.42/59.54 cnf(4632,plain,
% 59.42/59.54 (P8(a3,a2,a2,a3,a2,a3,a2,a2)),
% 59.42/59.54 inference(scs_inference,[],[4611,262])).
% 59.42/59.54 cnf(4634,plain,
% 59.42/59.54 (P8(a3,a2,a2,a2,a3,a2,a2,a3)),
% 59.42/59.54 inference(scs_inference,[],[4611,262,264])).
% 59.42/59.54 cnf(4636,plain,
% 59.42/59.54 (P10(x46361,x46362,x46361,x46362)),
% 59.42/59.54 inference(scs_inference,[],[4611,4585,262,264,239])).
% 59.42/59.54 cnf(4638,plain,
% 59.42/59.54 (P8(a2,a2,a3,a2,a2,a3,a3,a2)),
% 59.42/59.54 inference(scs_inference,[],[4611,4585,262,264,239,263])).
% 59.42/59.54 cnf(4640,plain,
% 59.42/59.54 (P9(a2,a2,a21,a2,a2,a3,a21,a3)),
% 59.42/59.54 inference(scs_inference,[],[4611,4579,4585,262,264,239,263,261])).
% 59.42/59.54 cnf(4642,plain,
% 59.42/59.54 (P4(a2,a2,a21,a3)),
% 59.42/59.54 inference(scs_inference,[],[4611,4579,4585,4591,262,264,239,263,261,177])).
% 59.42/59.54 cnf(4644,plain,
% 59.42/59.54 (P10(x46441,x46442,x46442,x46441)),
% 59.42/59.54 inference(scs_inference,[],[4611,4579,4585,4591,262,264,239,263,261,177,170])).
% 59.42/59.54 cnf(4646,plain,
% 59.42/59.54 (P9(a2,a21,a2,a2,a3,a21,a3,a2)),
% 59.42/59.54 inference(scs_inference,[],[4611,4579,4585,4490,4591,262,264,239,263,261,177,170,230])).
% 59.42/59.54 cnf(4648,plain,
% 59.42/59.54 (P1(a3,a3,a2)),
% 59.42/59.54 inference(scs_inference,[],[4611,4579,4585,4490,4591,4595,262,264,239,263,261,177,170,230,158])).
% 59.42/59.54 cnf(4650,plain,
% 59.42/59.54 (P9(a21,a2,x46501,x46502,a2,a21,x46501,x46502)),
% 59.42/59.54 inference(scs_inference,[],[4611,4579,4581,4585,4490,4591,4595,262,264,239,263,261,177,170,230,158,258])).
% 59.42/59.54 cnf(4656,plain,
% 59.42/59.54 (P4(a22,a2,a3,a2)),
% 59.42/59.54 inference(scs_inference,[],[4611,4579,4581,4585,4490,4512,4577,4591,4595,262,264,239,263,261,177,170,230,158,258,231,166,176])).
% 59.42/59.54 cnf(4660,plain,
% 59.42/59.54 (P9(x46601,x46602,a2,a21,x46601,x46602,a21,a2)),
% 59.42/59.54 inference(scs_inference,[],[4611,4579,4581,4585,4490,4506,4512,4577,4591,4595,262,264,239,263,261,177,170,230,158,258,231,166,176,157,259])).
% 59.42/59.54 cnf(4666,plain,
% 59.42/59.54 (P3(a2,a3,a1,a22)),
% 59.42/59.54 inference(scs_inference,[],[4611,4579,4581,4585,4490,4506,4512,4522,4577,4591,4595,4606,262,264,239,263,261,177,170,230,158,258,231,166,176,157,259,175,260,171])).
% 59.42/59.54 cnf(4668,plain,
% 59.42/59.54 (P3(a16,a3,a18,a20)),
% 59.42/59.54 inference(scs_inference,[],[4611,4601,4579,4581,4585,4490,4506,4512,4522,4577,4591,4595,4606,262,264,239,263,261,177,170,230,158,258,231,166,176,157,259,175,260,171,172])).
% 59.42/59.54 cnf(4670,plain,
% 59.42/59.54 (P8(a2,a3,a2,a2,a2,a3,a2,a2)),
% 59.42/59.54 inference(scs_inference,[],[4611,4601,4579,4581,4585,4490,4506,4512,4522,4577,4591,4595,4606,262,264,239,263,261,177,170,230,158,258,231,166,176,157,259,175,260,171,172,269])).
% 59.42/59.54 cnf(4672,plain,
% 59.42/59.54 (P4(x46721,a21,a2,a2)),
% 59.42/59.54 inference(scs_inference,[],[4611,4601,4579,4581,4585,4490,4506,4512,4522,4577,4591,4595,4606,386,262,264,239,263,261,177,170,230,158,258,231,166,176,157,259,175,260,171,172,269,242])).
% 59.42/59.54 cnf(4680,plain,
% 59.42/59.54 (P1(f14(a2,a3,a3,a2,a2,a2),a3,a2)),
% 59.42/59.54 inference(scs_inference,[],[4611,4601,4579,4575,4581,4585,4490,4506,4512,4522,4577,4591,4595,4606,4440,4410,4504,386,262,264,239,263,261,177,170,230,158,258,231,166,176,157,259,175,260,171,172,269,242,247,212,213])).
% 59.42/59.54 cnf(4684,plain,
% 59.42/59.54 (P8(a3,a2,a3,a2,a2,a2,a2,a3)),
% 59.42/59.54 inference(scs_inference,[],[4611,4601,4579,4575,4581,4585,4490,4506,4512,4522,4577,4591,4595,4606,4440,4410,4504,386,262,264,239,263,261,177,170,230,158,258,231,166,176,157,259,175,260,171,172,269,242,247,212,213,1238,265])).
% 59.42/59.54 cnf(4688,plain,
% 59.42/59.54 (P3(a2,a17,a3,a16)),
% 59.42/59.54 inference(scs_inference,[],[142,4611,4601,4579,4575,4581,4585,4490,4506,4512,4522,4577,4591,4595,4606,4440,4410,4504,386,150,262,264,239,263,261,177,170,230,158,258,231,166,176,157,259,175,260,171,172,269,242,247,212,213,1238,265,203,188])).
% 59.42/59.54 cnf(4694,plain,
% 59.42/59.54 (P8(a2,a2,a2,a3,a3,a2,a3,a2)),
% 59.42/59.54 inference(scs_inference,[],[4638,265])).
% 59.42/59.54 cnf(4696,plain,
% 59.42/59.54 (P8(a2,a3,a2,a3,a2,a3,a2,a2)),
% 59.42/59.54 inference(scs_inference,[],[4632,4638,265,264])).
% 59.42/59.54 cnf(4698,plain,
% 59.42/59.54 (P8(a3,a2,a2,a3,a3,a2,a2,a2)),
% 59.42/59.54 inference(scs_inference,[],[4632,4634,4638,265,264,262])).
% 59.42/59.54 cnf(4700,plain,
% 59.42/59.54 (P9(a21,a2,a2,a21,x47001,x47002,x47001,x47002)),
% 59.42/59.54 inference(scs_inference,[],[4632,4634,4650,4638,265,264,262,261])).
% 59.42/59.54 cnf(4702,plain,
% 59.42/59.54 (P8(a3,a2,a3,a2,a2,a3,a2,a2)),
% 59.42/59.54 inference(scs_inference,[],[4632,4634,4684,4650,4638,265,264,262,261,263])).
% 59.42/59.54 cnf(4706,plain,
% 59.42/59.54 (P9(a2,a2,a2,a21,a3,a2,a3,a21)),
% 59.42/59.54 inference(scs_inference,[],[4632,4634,4684,4571,4650,4638,4656,265,264,262,261,263,177,230])).
% 59.42/59.54 cnf(4708,plain,
% 59.42/59.54 (P1(x47081,x47082,x47082)),
% 59.42/59.54 inference(scs_inference,[],[4636,4632,4634,4684,4571,4650,4638,4656,265,264,262,261,263,177,230,166])).
% 59.42/59.54 cnf(4712,plain,
% 59.42/59.54 (P4(x47121,a2,a21,a2)),
% 59.42/59.54 inference(scs_inference,[],[4636,4632,4634,4684,4571,4650,4660,4672,4638,4656,265,264,262,261,263,177,230,166,258,176])).
% 59.42/59.54 cnf(4714,plain,
% 59.42/59.54 (P1(a3,a16,a3)),
% 59.42/59.54 inference(scs_inference,[],[4636,4632,4634,4684,4571,4650,4660,4672,4589,4638,4656,265,264,262,261,263,177,230,166,258,176,157])).
% 59.42/59.54 cnf(4716,plain,
% 59.42/59.54 (P1(f14(a2,a3,a3,a2,a2,a2),a2,a3)),
% 59.42/59.54 inference(scs_inference,[],[4636,4632,4634,4684,4571,4650,4660,4672,4589,4638,4656,4680,265,264,262,261,263,177,230,166,258,176,157,158])).
% 59.42/59.54 cnf(4718,plain,
% 59.42/59.54 (P9(x47181,x47182,x47183,x47184,x47181,x47182,x47183,x47184)),
% 59.42/59.54 inference(scs_inference,[],[4636,4632,4634,4684,4571,4650,4660,4672,4589,4638,4656,4680,265,264,262,261,263,177,230,166,258,176,157,158,231])).
% 59.42/59.54 cnf(4720,plain,
% 59.42/59.54 (P4(a21,x47201,a2,a2)),
% 59.42/59.54 inference(scs_inference,[],[4636,4632,4634,4684,4571,4650,4660,4672,4589,4638,4656,4680,265,264,262,261,263,177,230,166,258,176,157,158,231,175])).
% 59.42/59.54 cnf(4722,plain,
% 59.42/59.54 (P9(a21,a2,a3,a21,a2,a2,a2,a3)),
% 59.42/59.54 inference(scs_inference,[],[4636,4632,4634,4684,4571,4650,4660,4672,4514,4589,4638,4656,4680,265,264,262,261,263,177,230,166,258,176,157,158,231,175,259])).
% 59.42/59.54 cnf(4724,plain,
% 59.42/59.54 (P9(a2,a21,a21,a3,a2,a2,a2,a3)),
% 59.42/59.54 inference(scs_inference,[],[4636,4632,4498,4634,4684,4571,4650,4660,4672,4514,4589,4638,4656,4680,265,264,262,261,263,177,230,166,258,176,157,158,231,175,259,260])).
% 59.42/59.54 cnf(4726,plain,
% 59.42/59.54 (P3(a18,a20,a16,a3)),
% 59.42/59.54 inference(scs_inference,[],[4636,4632,4498,4634,4684,4571,4650,4660,4672,4514,4589,4638,4656,4668,4680,265,264,262,261,263,177,230,166,258,176,157,158,231,175,259,260,171])).
% 59.42/59.54 cnf(4730,plain,
% 59.42/59.54 (P4(x47301,a2,a3,a3)),
% 59.42/59.54 inference(scs_inference,[],[4636,4632,4498,4634,4684,4571,4650,4660,4672,4514,4589,4638,4648,4656,4666,4668,4680,265,264,262,261,263,177,230,166,258,176,157,158,231,175,259,260,171,172,242])).
% 59.42/59.54 cnf(4732,plain,
% 59.42/59.54 (P3(a3,a16,a18,a20)),
% 59.42/59.54 inference(scs_inference,[],[4636,4632,4498,4634,4684,4571,4650,4660,4672,4514,4589,4638,4648,4656,4666,4668,4680,4440,265,264,262,261,263,177,230,166,258,176,157,158,231,175,259,260,171,172,242,247])).
% 59.42/59.54 cnf(4758,plain,
% 59.42/59.54 (P8(a3,a2,a2,a2,a2,a3,a2,a2)),
% 59.42/59.54 inference(scs_inference,[],[4670,264])).
% 59.42/59.54 cnf(4760,plain,
% 59.42/59.54 (P8(a2,a3,a2,a3,a2,a2,a2,a2)),
% 59.42/59.54 inference(scs_inference,[],[4670,264,265])).
% 59.42/59.54 cnf(4764,plain,
% 59.42/59.54 (P9(x47641,x47642,x47641,x47642,x47643,x47644,x47643,x47644)),
% 59.42/59.54 inference(scs_inference,[],[4718,4670,264,265,263,261])).
% 59.42/59.54 cnf(4768,plain,
% 59.42/59.54 (P4(x47681,a2,a2,a21)),
% 59.42/59.54 inference(scs_inference,[],[4718,4712,4670,4696,264,265,263,261,262,177])).
% 59.42/59.54 cnf(4774,plain,
% 59.42/59.54 (P9(x47741,x47742,x47743,x47744,x47742,x47741,x47743,x47744)),
% 59.42/59.54 inference(scs_inference,[],[4718,4712,4670,4696,4714,4644,264,265,263,261,262,177,230,158,231])).
% 59.42/59.54 cnf(4776,plain,
% 59.42/59.54 (P4(a21,a2,x47761,a2)),
% 59.42/59.54 inference(scs_inference,[],[4718,4712,4720,4670,4696,4714,4644,264,265,263,261,262,177,230,158,231,176])).
% 59.42/59.54 cnf(4778,plain,
% 59.42/59.54 (P1(x47781,x47782,x47781)),
% 59.42/59.54 inference(scs_inference,[],[4718,4708,4712,4720,4670,4696,4714,4644,264,265,263,261,262,177,230,158,231,176,157])).
% 59.42/59.54 cnf(4780,plain,
% 59.42/59.54 (P4(a2,x47801,a21,a2)),
% 59.42/59.54 inference(scs_inference,[],[4718,4708,4712,4720,4670,4696,4714,4644,264,265,263,261,262,177,230,158,231,176,157,175])).
% 59.42/59.54 cnf(4786,plain,
% 59.42/59.54 (P9(a2,a21,a2,a2,a21,a3,a2,a3)),
% 59.42/59.54 inference(scs_inference,[],[4718,4708,4593,4700,4712,4720,4670,4696,4714,4644,264,265,263,261,262,177,230,158,231,176,157,175,258,259,260])).
% 59.42/59.54 cnf(4790,plain,
% 59.42/59.54 (P3(a2,a17,a16,a3)),
% 59.42/59.54 inference(scs_inference,[],[4718,4708,4593,4700,4712,4720,4670,4688,4696,4714,4644,264,265,263,261,262,177,230,158,231,176,157,175,258,259,260,171,172])).
% 59.42/59.54 cnf(4792,plain,
% 59.42/59.54 (P10(a2,a17,a18,a20)),
% 59.42/59.54 inference(scs_inference,[],[4718,4708,4593,4700,4712,4720,4670,4688,4696,4714,4732,4644,264,265,263,261,262,177,230,158,231,176,157,175,258,259,260,171,172,186])).
% 59.42/59.54 cnf(4794,plain,
% 59.42/59.54 (P4(x47941,x47942,x47942,x47942)),
% 59.42/59.54 inference(scs_inference,[],[4718,4708,4593,4700,4712,4720,4670,4688,4696,4714,4732,4644,264,265,263,261,262,177,230,158,231,176,157,175,258,259,260,171,172,186,242])).
% 59.42/59.54 cnf(4795,plain,
% 59.42/59.54 (P9(x47951,x47952,x47953,x47954,x47951,x47952,x47953,x47954)),
% 59.42/59.54 inference(rename_variables,[],[4718])).
% 59.42/59.54 cnf(4796,plain,
% 59.42/59.54 (P1(x47961,x47962,x47962)),
% 59.42/59.54 inference(rename_variables,[],[4708])).
% 59.42/59.54 cnf(4798,plain,
% 59.42/59.54 (P5(a21,a2,a21,a2)),
% 59.42/59.54 inference(scs_inference,[],[4718,4795,4708,4593,4700,4712,4720,4670,4688,4696,4714,4732,4644,264,265,263,261,262,177,230,158,231,176,157,175,258,259,260,171,172,186,242,257])).
% 59.42/59.54 cnf(4803,plain,
% 59.42/59.54 (P9(a21,a2,a2,a2,a2,a2,a21,a2)),
% 59.42/59.54 inference(scs_inference,[],[4718,4795,4708,4593,4700,4712,4720,4670,4688,4696,4714,4732,4644,264,265,263,261,262,177,230,158,231,176,157,175,258,259,260,171,172,186,242,257,232])).
% 59.42/59.54 cnf(4807,plain,
% 59.42/59.54 (P5(a2,a21,a21,a2)),
% 59.42/59.54 inference(scs_inference,[],[4718,4795,4708,4593,4700,4712,4720,4670,4688,4696,4714,4732,4644,264,265,263,261,262,177,230,158,231,176,157,175,258,259,260,171,172,186,242,257,232,174,173])).
% 59.42/59.54 cnf(4809,plain,
% 59.42/59.54 (P10(a2,a17,a20,a18)),
% 59.42/59.54 inference(scs_inference,[],[4718,4795,4708,4593,4700,4712,4720,4670,4688,4696,4714,4732,4644,264,265,263,261,262,177,230,158,231,176,157,175,258,259,260,171,172,186,242,257,232,174,173,170])).
% 59.42/59.54 cnf(4811,plain,
% 59.42/59.54 (P10(a18,a20,a2,a17)),
% 59.42/59.54 inference(scs_inference,[],[4718,4795,4708,4593,4700,4712,4720,4670,4688,4696,4714,4732,4644,264,265,263,261,262,177,230,158,231,176,157,175,258,259,260,171,172,186,242,257,232,174,173,170,169])).
% 59.42/59.54 cnf(4816,plain,
% 59.42/59.54 (P9(a2,a21,x48161,x48162,a21,a2,x48161,x48162)),
% 59.42/59.54 inference(rename_variables,[],[4581])).
% 59.42/59.54 cnf(4821,plain,
% 59.42/59.54 (P7(a21,a2,a2)),
% 59.42/59.54 inference(scs_inference,[],[4718,4795,4708,4796,4593,4700,4712,4720,4670,4688,4696,4714,4732,4644,4581,4816,264,265,263,261,262,177,230,158,231,176,157,175,258,259,260,171,172,186,242,257,232,174,173,170,169,182,251,255,167])).
% 59.42/59.54 cnf(4824,plain,
% 59.42/59.54 (P7(f27(a2,a2,a2,a2,a21,a21),a2,a2)),
% 59.42/59.54 inference(scs_inference,[],[4718,4795,4708,4796,4593,4700,4712,4720,4670,4688,4696,4714,4732,4644,4581,4816,264,265,263,261,262,177,230,158,231,176,157,175,258,259,260,171,172,186,242,257,232,174,173,170,169,182,251,255,167,209])).
% 59.42/59.54 cnf(4866,plain,
% 59.42/59.54 (~P4(a19,x48661,a22,a20)+~P4(x48661,a19,a22,a21)),
% 59.42/59.54 inference(scs_inference,[],[4432,175])).
% 59.42/59.54 cnf(4874,plain,
% 59.42/59.54 (P5(a2,a21,a2,a21)),
% 59.42/59.54 inference(scs_inference,[],[4807,174])).
% 59.42/59.54 cnf(4878,plain,
% 59.42/59.54 (P8(a3,a2,a2,a3,a2,a2,a2,a2)),
% 59.42/59.54 inference(scs_inference,[],[4807,4758,4824,174,162,265])).
% 59.42/59.54 cnf(4880,plain,
% 59.42/59.54 (P8(a2,a3,a2,a3,a3,a2,a2,a2)),
% 59.42/59.54 inference(scs_inference,[],[4807,4698,4758,4824,174,162,265,264])).
% 59.42/59.54 cnf(4882,plain,
% 59.42/59.54 (P9(x48821,x48822,x48822,x48821,x48823,x48824,x48823,x48824)),
% 59.42/59.54 inference(scs_inference,[],[4774,4807,4698,4758,4824,174,162,265,264,261])).
% 59.42/59.54 cnf(4884,plain,
% 59.42/59.54 (P8(a2,a3,a2,a2,a3,a2,a3,a2)),
% 59.42/59.54 inference(scs_inference,[],[4774,4807,4698,4702,4758,4824,174,162,265,264,261,262])).
% 59.42/59.54 cnf(4886,plain,
% 59.42/59.54 (P8(a2,a3,a3,a2,a2,a2,a3,a2)),
% 59.42/59.54 inference(scs_inference,[],[4774,4807,4698,4702,4758,4824,174,162,265,264,261,262,263])).
% 59.42/59.54 cnf(4888,plain,
% 59.42/59.54 (P10(a18,a20,a17,a2)),
% 59.42/59.54 inference(scs_inference,[],[4774,4807,4698,4702,4758,4811,4824,174,162,265,264,261,262,263,170])).
% 59.42/59.54 cnf(4892,plain,
% 59.42/59.54 (P10(a20,a18,a2,a17)),
% 59.42/59.54 inference(scs_inference,[],[4774,4807,4768,4698,4702,4758,4809,4811,4824,174,162,265,264,261,262,263,170,230,169])).
% 59.42/59.54 cnf(4894,plain,
% 59.42/59.54 (P4(a21,a2,a2,x48941)),
% 59.42/59.54 inference(scs_inference,[],[4774,4807,4768,4776,4698,4702,4758,4809,4811,4824,174,162,265,264,261,262,263,170,230,169,177])).
% 59.42/59.54 cnf(4896,plain,
% 59.42/59.54 (P4(x48961,x48962,x48961,x48961)),
% 59.42/59.54 inference(scs_inference,[],[4774,4794,4807,4768,4776,4698,4702,4758,4809,4811,4824,174,162,265,264,261,262,263,170,230,169,177,175])).
% 59.42/59.54 cnf(4898,plain,
% 59.42/59.54 (P4(x48981,a3,a2,a3)),
% 59.42/59.54 inference(scs_inference,[],[4774,4794,4807,4730,4768,4776,4698,4702,4758,4809,4811,4824,174,162,265,264,261,262,263,170,230,169,177,175,176])).
% 59.42/59.54 cnf(4900,plain,
% 59.42/59.54 (P1(x49001,x49001,x49002)),
% 59.42/59.54 inference(scs_inference,[],[4774,4794,4778,4807,4730,4768,4776,4698,4702,4758,4809,4811,4824,174,162,265,264,261,262,263,170,230,169,177,175,176,158])).
% 59.42/59.54 cnf(4908,plain,
% 59.42/59.54 (P9(x49081,x49082,x49083,x49084,x49081,x49082,x49084,x49083)),
% 59.42/59.54 inference(scs_inference,[],[4774,4794,4778,4597,4807,4730,4768,4776,4698,4702,4758,4792,4809,4811,4716,4824,174,162,265,264,261,262,263,170,230,169,177,175,176,158,258,157,231,259])).
% 59.42/59.54 cnf(4912,plain,
% 59.42/59.54 (P3(a16,a3,a2,a17)),
% 59.42/59.54 inference(scs_inference,[],[4774,4794,4778,4573,4597,4807,4730,4768,4776,4698,4702,4758,4790,4792,4809,4811,4716,4824,174,162,265,264,261,262,263,170,230,169,177,175,176,158,258,157,231,259,260,171])).
% 59.42/59.54 cnf(4918,plain,
% 59.42/59.54 (P10(a17,a2,a18,a20)),
% 59.42/59.54 inference(scs_inference,[],[4774,4794,4778,4573,4597,4807,4821,4730,4768,4776,4698,4702,4726,4758,4790,4792,4809,4811,4716,4824,4644,174,162,265,264,261,262,263,170,230,169,177,175,176,158,258,157,231,259,260,171,172,210,185])).
% 59.42/59.54 cnf(4921,plain,
% 59.42/59.54 (P8(a21,a2,a2,a2,a21,a2,a2,a2)),
% 59.42/59.54 inference(scs_inference,[],[4774,4794,4778,4573,4597,4807,4821,4730,4768,4776,4698,4702,4726,4758,4790,4792,4809,4811,4716,4824,4644,174,162,265,264,261,262,263,170,230,169,177,175,176,158,258,157,231,259,260,171,172,210,185,229])).
% 59.42/59.54 cnf(4923,plain,
% 59.42/59.54 (P1(f23(a21,a21,a2,a21),a2,a21)),
% 59.42/59.54 inference(scs_inference,[],[4774,4794,4778,4573,4597,4807,4821,4730,4768,4776,4698,4702,4726,4758,4790,4792,4809,4811,4716,4824,4700,4644,174,162,265,264,261,262,263,170,230,169,177,175,176,158,258,157,231,259,260,171,172,210,185,229,255])).
% 59.42/59.54 cnf(4926,plain,
% 59.42/59.54 (P10(a21,a21,a2,a2)),
% 59.42/59.54 inference(scs_inference,[],[4774,4794,4778,4573,4597,4807,4821,4730,4768,4776,4698,4702,4726,4758,4790,4792,4809,4811,4716,4824,4700,4644,174,162,265,264,261,262,263,170,230,169,177,175,176,158,258,157,231,259,260,171,172,210,185,229,255,164])).
% 59.42/59.54 cnf(4929,plain,
% 59.42/59.54 (P9(x49291,x49292,x49293,x49294,x49292,x49291,x49293,x49294)),
% 59.42/59.54 inference(rename_variables,[],[4774])).
% 59.42/59.54 cnf(4931,plain,
% 59.42/59.54 (P3(a21,a21,a2,a2)),
% 59.42/59.54 inference(scs_inference,[],[4774,4794,4778,4640,4798,4573,4597,4807,4821,4730,4768,4776,4698,4702,4726,4758,4790,4792,4809,4811,4716,4824,4700,4644,174,162,265,264,261,262,263,170,230,169,177,175,176,158,258,157,231,259,260,171,172,210,185,229,255,164,268,187])).
% 59.42/59.54 cnf(4937,plain,
% 59.42/59.54 (P4(a16,a16,a1,a2)),
% 59.42/59.54 inference(scs_inference,[],[142,4764,4774,4794,4778,4640,4798,4573,4597,4807,4821,4730,4768,4776,4698,4702,4726,4758,4790,4792,4809,4811,4716,4824,4700,4644,174,162,265,264,261,262,263,170,230,169,177,175,176,158,258,157,231,259,260,171,172,210,185,229,255,164,268,187,190,233,242])).
% 59.42/59.54 cnf(4938,plain,
% 59.42/59.54 (P9(x49381,x49382,x49381,x49382,x49383,x49384,x49383,x49384)),
% 59.42/59.54 inference(rename_variables,[],[4764])).
% 59.42/59.54 cnf(4940,plain,
% 59.42/59.54 (P3(a17,a2,a16,a3)),
% 59.42/59.54 inference(scs_inference,[],[142,4764,4774,4929,4794,4778,4640,4798,4573,4597,4807,4821,4730,4768,4776,4698,4702,4726,4758,4790,4792,4809,4811,4716,4824,4700,4644,174,162,265,264,261,262,263,170,230,169,177,175,176,158,258,157,231,259,260,171,172,210,185,229,255,164,268,187,190,233,242,247])).
% 59.42/59.54 cnf(4943,plain,
% 59.42/59.54 (P2(f10(a2,a2,a2),a2,a2,a2)),
% 59.42/59.54 inference(scs_inference,[],[142,4764,4774,4929,4794,4778,4640,4798,4573,4597,4807,4821,4730,4768,4776,4698,4702,4726,4758,4790,4792,4809,4811,4716,4824,4700,4636,4644,174,162,265,264,261,262,263,170,230,169,177,175,176,158,258,157,231,259,260,171,172,210,185,229,255,164,268,187,190,233,242,247,198])).
% 59.42/59.54 cnf(4944,plain,
% 59.42/59.54 (P10(x49441,x49442,x49441,x49442)),
% 59.42/59.54 inference(rename_variables,[],[4636])).
% 59.42/59.54 cnf(4945,plain,
% 59.42/59.54 (P4(x49451,x49452,x49452,x49452)),
% 59.42/59.54 inference(rename_variables,[],[4794])).
% 59.42/59.54 cnf(4947,plain,
% 59.42/59.54 (P3(a2,a21,a21,a2)),
% 59.42/59.54 inference(scs_inference,[],[142,4764,4774,4929,4794,4778,4640,4798,4573,4597,4807,4821,4730,4768,4776,4698,4702,4726,4758,4790,4792,4809,4811,4716,4824,4672,4700,4636,4644,174,162,265,264,261,262,263,170,230,169,177,175,176,158,258,157,231,259,260,171,172,210,185,229,255,164,268,187,190,233,242,247,198,201])).
% 59.42/59.54 cnf(4951,plain,
% 59.42/59.54 (P1(x49511,x49512,x49511)),
% 59.42/59.54 inference(rename_variables,[],[4778])).
% 59.42/59.54 cnf(4952,plain,
% 59.42/59.54 (P9(x49521,x49522,x49521,x49522,x49523,x49524,x49523,x49524)),
% 59.42/59.54 inference(rename_variables,[],[4764])).
% 59.42/59.54 cnf(4954,plain,
% 59.42/59.54 (P7(x49541,a2,x49541)),
% 59.42/59.54 inference(scs_inference,[],[142,4764,4938,4774,4929,4794,4778,4951,4640,4798,4573,4597,4807,4821,4730,4768,4776,4698,4702,4726,4758,4790,4792,4809,4811,4716,4824,4672,4700,4636,4944,4644,174,162,265,264,261,262,263,170,230,169,177,175,176,158,258,157,231,259,260,171,172,210,185,229,255,164,268,187,190,233,242,247,198,201,245,168])).
% 59.42/59.54 cnf(4955,plain,
% 59.42/59.54 (P10(x49551,x49552,x49551,x49552)),
% 59.42/59.54 inference(rename_variables,[],[4636])).
% 59.42/59.54 cnf(4956,plain,
% 59.42/59.54 (P1(x49561,x49562,x49561)),
% 59.42/59.54 inference(rename_variables,[],[4778])).
% 59.42/59.54 cnf(4958,plain,
% 59.42/59.54 (P7(a21,x49581,x49581)),
% 59.42/59.54 inference(scs_inference,[],[142,4764,4938,4774,4929,4794,4778,4951,4640,4798,4573,4597,4807,4821,4730,4768,4776,4698,4702,4726,4758,4790,4792,4809,4811,4716,4824,4672,4700,4636,4944,4955,4644,174,162,265,264,261,262,263,170,230,169,177,175,176,158,258,157,231,259,260,171,172,210,185,229,255,164,268,187,190,233,242,247,198,201,245,168,181])).
% 59.42/59.54 cnf(4960,plain,
% 59.42/59.54 (P10(x49601,x49602,x49601,x49602)),
% 59.42/59.54 inference(rename_variables,[],[4636])).
% 59.42/59.54 cnf(4963,plain,
% 59.42/59.54 (P1(x49631,x49632,x49632)),
% 59.42/59.54 inference(rename_variables,[],[4708])).
% 59.42/59.54 cnf(4964,plain,
% 59.42/59.54 (P10(x49641,x49642,x49641,x49642)),
% 59.42/59.54 inference(rename_variables,[],[4636])).
% 59.42/59.54 cnf(4965,plain,
% 59.42/59.54 (P1(x49651,x49652,x49651)),
% 59.42/59.54 inference(rename_variables,[],[4778])).
% 59.42/59.54 cnf(4968,plain,
% 59.42/59.54 (P10(x49681,x49682,x49681,x49682)),
% 59.42/59.54 inference(rename_variables,[],[4636])).
% 59.42/59.54 cnf(4973,plain,
% 59.42/59.54 (P7(f24(a2,x49731),a2,x49731)),
% 59.42/59.54 inference(scs_inference,[],[142,4764,4938,4774,4929,4794,4778,4951,4956,4965,4640,4798,4573,4597,4807,4821,4730,4768,4776,4698,4702,4726,4758,4790,4792,4809,4811,4716,4824,4708,4672,4700,4636,4944,4955,4960,4964,4968,4644,492,174,162,265,264,261,262,263,170,230,169,177,175,176,158,258,157,231,259,260,171,172,210,185,229,255,164,268,187,190,233,242,247,198,201,245,168,181,212,214,215,165])).
% 59.42/59.54 cnf(4974,plain,
% 59.42/59.54 (P1(x49741,x49742,x49741)),
% 59.42/59.54 inference(rename_variables,[],[4778])).
% 59.42/59.54 cnf(4976,plain,
% 59.42/59.54 (P5(x49761,x49761,x49761,x49761)),
% 59.42/59.54 inference(scs_inference,[],[142,4764,4938,4952,4774,4929,4794,4945,4778,4951,4956,4965,4640,4798,4573,4597,4807,4821,4730,4768,4776,4698,4702,4726,4758,4790,4792,4809,4811,4716,4824,4708,4672,4700,4636,4944,4955,4960,4964,4968,4644,492,174,162,265,264,261,262,263,170,230,169,177,175,176,158,258,157,231,259,260,171,172,210,185,229,255,164,268,187,190,233,242,247,198,201,245,168,181,212,214,215,165,257])).
% 59.42/59.54 cnf(4977,plain,
% 59.42/59.54 (P9(x49771,x49772,x49771,x49772,x49773,x49774,x49773,x49774)),
% 59.42/59.54 inference(rename_variables,[],[4764])).
% 59.42/59.54 cnf(4981,plain,
% 59.42/59.54 (P9(a21,a16,a16,a16,a16,a16,a21,a16)),
% 59.42/59.54 inference(scs_inference,[],[142,4764,4938,4952,4774,4929,4794,4945,4778,4951,4956,4965,4640,4798,4573,4597,4807,4821,4730,4768,4776,4698,4702,4726,4758,4790,4792,4809,4811,4716,4824,4708,4672,4700,4636,4944,4955,4960,4964,4968,4644,492,174,162,265,264,261,262,263,170,230,169,177,175,176,158,258,157,231,259,260,171,172,210,185,229,255,164,268,187,190,233,242,247,198,201,245,168,181,212,214,215,165,257,1424])).
% 59.42/59.54 cnf(4987,plain,
% 59.42/59.54 (P3(f8(a2,a2,a2,a21),a2,a2,a21)),
% 59.42/59.54 inference(scs_inference,[],[142,4764,4938,4952,4774,4929,4794,4945,4778,4951,4956,4965,4640,4798,4573,4597,4807,4821,4730,4768,4776,4698,4702,4726,4758,4790,4792,4809,4811,4716,4824,4708,4672,4700,4636,4944,4955,4960,4964,4968,4644,492,174,162,265,264,261,262,263,170,230,169,177,175,176,158,258,157,231,259,260,171,172,210,185,229,255,164,268,187,190,233,242,247,198,201,245,168,181,212,214,215,165,257,1424,232,159,193])).
% 59.42/59.54 cnf(4989,plain,
% 59.42/59.54 (P7(x49891,x49891,a2)),
% 59.42/59.54 inference(scs_inference,[],[142,4764,4938,4952,4774,4929,4794,4945,4778,4951,4956,4965,4640,4798,4573,4597,4807,4821,4730,4768,4776,4698,4702,4726,4758,4790,4792,4809,4811,4716,4824,4708,4672,4700,4636,4944,4955,4960,4964,4968,4644,492,174,162,265,264,261,262,263,170,230,169,177,175,176,158,258,157,231,259,260,171,172,210,185,229,255,164,268,187,190,233,242,247,198,201,245,168,181,212,214,215,165,257,1424,232,159,193,160])).
% 59.42/59.54 cnf(4991,plain,
% 59.42/59.54 (P3(f13(a2,a2,a21,x49911,a2),a2,x49911,a2)),
% 59.42/59.54 inference(scs_inference,[],[142,4764,4938,4952,4774,4929,4794,4945,4778,4951,4956,4965,4974,4640,4798,4573,4597,4807,4821,4730,4768,4776,4698,4702,4726,4758,4790,4792,4809,4811,4716,4824,4708,4672,4700,4636,4944,4955,4960,4964,4968,4644,492,174,162,265,264,261,262,263,170,230,169,177,175,176,158,258,157,231,259,260,171,172,210,185,229,255,164,268,187,190,233,242,247,198,201,245,168,181,212,214,215,165,257,1424,232,159,193,160,204])).
% 59.42/59.54 cnf(4992,plain,
% 59.42/59.54 (P1(x49921,x49922,x49921)),
% 59.42/59.54 inference(rename_variables,[],[4778])).
% 59.42/59.54 cnf(4996,plain,
% 59.42/59.54 (P10(f29(a2,a21,a21,a21,a2),a21,a2,a21)),
% 59.42/59.54 inference(scs_inference,[],[142,4764,4938,4952,4774,4929,4794,4945,4778,4951,4956,4965,4974,4640,4798,4573,4597,4807,4821,4730,4768,4776,4698,4702,4726,4758,4790,4792,4809,4811,4716,4824,4708,4672,4700,4636,4944,4955,4960,4964,4968,4644,492,174,162,265,264,261,262,263,170,230,169,177,175,176,158,258,157,231,259,260,171,172,210,185,229,255,164,268,187,190,233,242,247,198,201,245,168,181,212,214,215,165,257,1424,232,159,193,160,204,211,207])).
% 59.42/59.54 cnf(5005,plain,
% 59.42/59.54 (P1(a2,a21,f4(a2,a2,a21))),
% 59.42/59.54 inference(scs_inference,[],[142,4764,4938,4952,4774,4929,4794,4945,4778,4951,4956,4965,4974,4992,4640,4798,4573,4597,4807,4821,4730,4768,4776,4698,4702,4726,4758,4790,4792,4809,4811,4716,4824,4708,4672,4700,4636,4944,4955,4960,4964,4968,4644,492,174,162,265,264,261,262,263,170,230,169,177,175,176,158,258,157,231,259,260,171,172,210,185,229,255,164,268,187,190,233,242,247,198,201,245,168,181,212,214,215,165,257,1424,232,159,193,160,204,211,207,250,184,203,182])).
% 59.42/59.54 cnf(5011,plain,
% 59.42/59.54 (P5(a21,a2,a21,f4(a2,a2,a21))),
% 59.42/59.54 inference(scs_inference,[],[142,4764,4938,4952,4774,4929,4794,4945,4778,4951,4956,4965,4974,4992,4640,4798,4573,4597,4807,4821,4730,4768,4776,4698,4702,4726,4758,4790,4792,4809,4811,4716,4824,4708,4672,4700,4636,4944,4955,4960,4964,4968,4644,492,174,162,265,264,261,262,263,170,230,169,177,175,176,158,258,157,231,259,260,171,172,210,185,229,255,164,268,187,190,233,242,247,198,201,245,168,181,212,214,215,165,257,1424,232,159,193,160,204,211,207,250,184,203,182,195,209,194])).
% 59.42/59.54 cnf(5017,plain,
% 59.42/59.54 (P2(f9(a2,a2,a21),a2,a2,a21)),
% 59.42/59.54 inference(scs_inference,[],[142,4764,4938,4952,4774,4929,4794,4945,4778,4951,4956,4965,4974,4992,4640,4798,4573,4597,4642,4807,4821,4730,4768,4776,4698,4702,4726,4758,4790,4792,4809,4811,4716,4824,4708,4672,4700,4636,4944,4955,4960,4964,4968,4644,492,174,162,265,264,261,262,263,170,230,169,177,175,176,158,258,157,231,259,260,171,172,210,185,229,255,164,268,187,190,233,242,247,198,201,245,168,181,212,214,215,165,257,1424,232,159,193,160,204,211,207,250,184,203,182,195,209,194,206,179,197])).
% 59.42/59.54 cnf(5019,plain,
% 59.42/59.54 (P5(a2,a3,a2,a3)),
% 59.42/59.54 inference(scs_inference,[],[142,4764,4938,4952,4774,4929,4794,4945,4778,4951,4956,4965,4974,4992,4640,4798,4573,4597,4642,4807,4821,4730,4768,4776,4698,4702,4726,4758,4760,4790,4792,4809,4811,4716,4824,4708,4672,4700,4636,4944,4955,4960,4964,4968,4644,492,174,162,265,264,261,262,263,170,230,169,177,175,176,158,258,157,231,259,260,171,172,210,185,229,255,164,268,187,190,233,242,247,198,201,245,168,181,212,214,215,165,257,1424,232,159,193,160,204,211,207,250,184,203,182,195,209,194,206,179,197,249])).
% 59.42/59.54 cnf(5021,plain,
% 59.42/59.54 (P5(a2,a21,a2,f29(a2,a21,a21,a21,a2))),
% 59.42/59.54 inference(scs_inference,[],[142,4764,4938,4952,4774,4929,4794,4945,4778,4951,4956,4965,4974,4992,4640,4798,4573,4597,4642,4807,4821,4730,4768,4776,4698,4702,4726,4758,4760,4790,4792,4809,4811,4716,4824,4708,4672,4700,4636,4944,4955,4960,4964,4968,4644,492,174,162,265,264,261,262,263,170,230,169,177,175,176,158,258,157,231,259,260,171,172,210,185,229,255,164,268,187,190,233,242,247,198,201,245,168,181,212,214,215,165,257,1424,232,159,193,160,204,211,207,250,184,203,182,195,209,194,206,179,197,249,205])).
% 59.42/59.54 cnf(5023,plain,
% 59.42/59.54 (P3(a2,f6(a21,a2,a2),a2,a21)),
% 59.42/59.54 inference(scs_inference,[],[142,4764,4938,4952,4774,4929,4794,4945,4778,4951,4956,4965,4974,4992,4640,4798,4573,4597,4642,4807,4821,4730,4768,4776,4698,4702,4726,4758,4760,4790,4792,4809,4811,4716,4824,4708,4672,4700,4636,4944,4955,4960,4964,4968,4644,492,174,162,265,264,261,262,263,170,230,169,177,175,176,158,258,157,231,259,260,171,172,210,185,229,255,164,268,187,190,233,242,247,198,201,245,168,181,212,214,215,165,257,1424,232,159,193,160,204,211,207,250,184,203,182,195,209,194,206,179,197,249,205,196])).
% 59.42/59.54 cnf(5027,plain,
% 59.42/59.54 (P3(a2,a2,a2,a2)),
% 59.42/59.54 inference(scs_inference,[],[142,4764,4938,4952,4774,4929,4794,4945,4778,4951,4956,4965,4974,4992,4640,4798,4573,4597,4642,4807,4821,4730,4768,4776,4698,4702,4726,4758,4760,4790,4792,4809,4811,4716,4824,4708,4963,4672,4700,4636,4944,4955,4960,4964,4968,4644,492,174,162,265,264,261,262,263,170,230,169,177,175,176,158,258,157,231,259,260,171,172,210,185,229,255,164,268,187,190,233,242,247,198,201,245,168,181,212,214,215,165,257,1424,232,159,193,160,204,211,207,250,184,203,182,195,209,194,206,179,197,249,205,196,183,178])).
% 59.42/59.54 cnf(5032,plain,
% 59.42/59.54 (P5(a21,f4(a2,a2,a21),a21,a2)),
% 59.42/59.54 inference(scs_inference,[],[142,4764,4938,4952,4774,4929,4794,4945,4778,4951,4956,4965,4974,4992,4640,4798,4573,4597,4642,4807,4821,4730,4768,4776,4698,4702,4726,4758,4760,4790,4792,4809,4811,4716,4824,4708,4963,4672,4700,4636,4944,4955,4960,4964,4968,4644,492,174,162,265,264,261,262,263,170,230,169,177,175,176,158,258,157,231,259,260,171,172,210,185,229,255,164,268,187,190,233,242,247,198,201,245,168,181,212,214,215,165,257,1424,232,159,193,160,204,211,207,250,184,203,182,195,209,194,206,179,197,249,205,196,183,178,192,173])).
% 59.42/59.54 cnf(5034,plain,
% 59.42/59.54 (P3(a21,a2,a2,a2)),
% 59.42/59.54 inference(scs_inference,[],[142,4764,4938,4952,4977,4774,4929,4794,4945,4778,4951,4956,4965,4974,4992,4640,4798,4573,4597,4642,4807,4821,4730,4768,4776,4698,4702,4726,4758,4760,4790,4792,4809,4811,4716,4824,4708,4963,4672,4700,4636,4944,4955,4960,4964,4968,4644,492,174,162,265,264,261,262,263,170,230,169,177,175,176,158,258,157,231,259,260,171,172,210,185,229,255,164,268,187,190,233,242,247,198,201,245,168,181,212,214,215,165,257,1424,232,159,193,160,204,211,207,250,184,203,182,195,209,194,206,179,197,249,205,196,183,178,192,173,248])).
% 59.42/59.54 cnf(5062,plain,
% 59.42/59.54 (P8(a2,a2,a2,a21,a2,a2,a2,a21)),
% 59.42/59.54 inference(scs_inference,[],[4926,2070])).
% 59.42/59.54 cnf(5066,plain,
% 59.42/59.54 (P8(a21,a21,a21,a2,a21,a21,a21,a2)),
% 59.42/59.54 inference(scs_inference,[],[4926,2091])).
% 59.42/59.54 cnf(5081,plain,
% 59.42/59.54 (P5(a2,a3,a3,a2)),
% 59.42/59.54 inference(scs_inference,[],[5019,4991,442,232,174])).
% 59.42/59.54 cnf(5085,plain,
% 59.42/59.54 (P5(x50851,a2,x50851,x50851)),
% 59.42/59.54 inference(scs_inference,[],[4954,5019,4991,5021,442,232,174,173,162])).
% 59.42/59.54 cnf(5087,plain,
% 59.42/59.54 (P8(a3,a2,a2,a2,a3,a2,a3,a2)),
% 59.42/59.54 inference(scs_inference,[],[4884,4954,5019,4991,5021,442,232,174,173,162,264])).
% 59.42/59.55 cnf(5089,plain,
% 59.42/59.55 (P8(a21,a2,a21,a2,a2,a2,a2,a2)),
% 59.42/59.55 inference(scs_inference,[],[4884,4921,4954,5019,4991,5021,442,232,174,173,162,264,265])).
% 59.42/59.55 cnf(5091,plain,
% 59.42/59.55 (P9(x50911,x50912,x50911,x50912,x50913,x50914,x50914,x50913)),
% 59.42/59.55 inference(scs_inference,[],[4908,4884,4921,4954,5019,4991,5021,442,232,174,173,162,264,265,261])).
% 59.42/59.55 cnf(5099,plain,
% 59.42/59.55 (P10(a17,a2,a20,a18)),
% 59.42/59.55 inference(scs_inference,[],[4908,4918,4884,4921,4954,4878,5019,4973,4991,5021,442,232,174,173,162,264,265,261,160,263,262,170])).
% 59.42/59.55 cnf(5103,plain,
% 59.42/59.55 (P4(a16,a16,a2,a1)),
% 59.42/59.55 inference(scs_inference,[],[4908,4918,4884,4921,4937,4954,4878,4926,5019,4973,4991,5021,442,232,174,173,162,264,265,261,160,263,262,170,169,177])).
% 59.42/59.55 cnf(5105,plain,
% 59.42/59.55 (P4(a2,a21,a2,x51051)),
% 59.42/59.55 inference(scs_inference,[],[4908,4918,4884,4921,4937,4954,4894,4878,4926,5019,4973,4991,5021,442,232,174,173,162,264,265,261,160,263,262,170,169,177,175])).
% 59.42/59.55 cnf(5109,plain,
% 59.42/59.55 (P4(x51091,x51091,x51092,x51091)),
% 59.42/59.55 inference(scs_inference,[],[4896,4908,4918,4884,4921,4937,4954,4780,4894,4878,4926,5019,4973,4991,5021,442,232,174,173,162,264,265,261,160,263,262,170,169,177,175,230,176])).
% 59.42/59.55 cnf(5121,plain,
% 59.42/59.55 (P9(x51211,x51212,x51213,x51214,x51212,x51211,x51214,x51213)),
% 59.42/59.55 inference(scs_inference,[],[4896,4908,4918,4646,4724,4884,4921,4937,4954,4780,4894,4878,4926,5019,5005,4973,4991,5021,442,232,174,173,162,264,265,261,160,263,262,170,169,177,175,230,176,158,157,258,231,259,260])).
% 59.42/59.55 cnf(5123,plain,
% 59.42/59.55 (P3(a2,a2,a21,a21)),
% 59.42/59.55 inference(scs_inference,[],[4896,4908,4918,4931,4646,4724,4884,4921,4937,4954,4780,4894,4878,4926,5019,5005,4973,4991,5021,442,232,174,173,162,264,265,261,160,263,262,170,169,177,175,230,176,158,157,258,231,259,260,171])).
% 59.42/59.55 cnf(5129,plain,
% 59.42/59.55 (P5(a2,a2,a21,a2)),
% 59.42/59.55 inference(scs_inference,[],[4896,4908,4912,4918,4931,4646,4724,4884,4921,4937,4947,4954,4780,4894,4878,4926,5019,5005,4973,4991,5011,5032,5021,442,232,174,173,162,264,265,261,160,263,262,170,169,177,175,230,176,158,157,258,231,259,260,171,172,189,180])).
% 59.42/59.55 cnf(5130,plain,
% 59.42/59.55 (P7(x51301,a2,x51301)),
% 59.42/59.55 inference(rename_variables,[],[4954])).
% 59.42/59.55 cnf(5132,plain,
% 59.42/59.55 (P3(f13(a2,a2,a21,a2,x51321),a2,a2,x51321)),
% 59.42/59.55 inference(scs_inference,[],[4896,4908,4900,4912,4918,4931,4646,4724,4884,4921,4937,4947,4954,4780,4894,4878,4926,5019,5005,4973,4991,5011,5032,5021,442,232,174,173,162,264,265,261,160,263,262,170,169,177,175,230,176,158,157,258,231,259,260,171,172,189,180,204])).
% 59.42/59.55 cnf(5133,plain,
% 59.42/59.55 (P1(x51331,x51331,x51332)),
% 59.42/59.55 inference(rename_variables,[],[4900])).
% 59.42/59.55 cnf(5138,plain,
% 59.42/59.55 (P9(x51381,x51382,x51381,x51382,x51383,x51384,x51383,x51384)),
% 59.42/59.55 inference(rename_variables,[],[4764])).
% 59.42/59.55 cnf(5141,plain,
% 59.42/59.55 (P5(x51411,x51411,x51411,x51411)),
% 59.42/59.55 inference(rename_variables,[],[4976])).
% 59.42/59.55 cnf(5143,plain,
% 59.42/59.55 (P10(a2,a2,x51431,x51431)),
% 59.42/59.55 inference(scs_inference,[],[4976,4896,4908,4900,4912,4918,4931,4646,4724,4884,4921,4937,4947,4954,5130,4780,4894,4878,4926,5019,5034,5005,4973,4991,5011,5032,5021,4764,442,232,174,173,162,264,265,261,160,263,262,170,169,177,175,230,176,158,157,258,231,259,260,171,172,189,180,204,210,253,207,163])).
% 59.42/59.55 cnf(5147,plain,
% 59.42/59.55 (P10(a20,a18,a17,a2)),
% 59.42/59.55 inference(scs_inference,[],[4976,4896,4908,4900,4912,4918,4931,4646,4724,4884,4921,4937,4947,4954,5130,4780,4894,4878,4892,4926,5019,5034,5005,4973,4991,5011,5032,5021,4764,442,232,174,173,162,264,265,261,160,263,262,170,169,177,175,230,176,158,157,258,231,259,260,171,172,189,180,204,210,253,207,163,211,246])).
% 59.42/59.55 cnf(5151,plain,
% 59.42/59.55 (P1(x51511,x51511,x51512)),
% 59.42/59.55 inference(rename_variables,[],[4900])).
% 59.42/59.55 cnf(5153,plain,
% 59.42/59.55 (P1(f6(a2,a2,a21),a21,a2)),
% 59.42/59.55 inference(scs_inference,[],[4976,4896,4908,4900,5133,4912,4918,4931,4646,4724,4884,4921,4937,4947,4954,5130,4780,4894,4878,4892,4926,5019,5034,5005,5023,4973,4991,5011,5032,5021,4764,442,232,174,173,162,264,265,261,160,263,262,170,169,177,175,230,176,158,157,258,231,259,260,171,172,189,180,204,210,253,207,163,211,246,203,184])).
% 59.42/59.55 cnf(5159,plain,
% 59.42/59.55 (P5(x51591,x51591,x51591,x51591)),
% 59.42/59.55 inference(rename_variables,[],[4976])).
% 59.42/59.55 cnf(5161,plain,
% 59.42/59.55 (P7(f27(a2,x51611,a2,x51611,x51611,x51611),a2,x51611)),
% 59.42/59.55 inference(scs_inference,[],[4976,5141,4896,4908,4900,5133,4912,4918,4931,4646,4724,4884,4921,4937,4947,4954,5130,4780,4894,4878,4892,4926,5019,5027,5034,5005,5023,4973,4991,5011,5032,5021,4764,442,232,174,173,162,264,265,261,160,263,262,170,169,177,175,230,176,158,157,258,231,259,260,171,172,189,180,204,210,253,207,163,211,246,203,184,197,249,209])).
% 59.42/59.55 cnf(5168,plain,
% 59.42/59.55 (P5(x51681,x51681,x51681,x51681)),
% 59.42/59.55 inference(rename_variables,[],[4976])).
% 59.42/59.55 cnf(5171,plain,
% 59.42/59.55 (P9(x51711,x51712,x51712,x51711,x51713,x51714,x51713,x51714)),
% 59.42/59.55 inference(rename_variables,[],[4882])).
% 59.42/59.55 cnf(5174,plain,
% 59.42/59.55 (P5(x51741,x51741,x51741,x51741)),
% 59.42/59.55 inference(rename_variables,[],[4976])).
% 59.42/59.55 cnf(5177,plain,
% 59.42/59.55 (P5(x51771,x51771,x51771,x51771)),
% 59.42/59.55 inference(rename_variables,[],[4976])).
% 59.42/59.55 cnf(5179,plain,
% 59.42/59.55 (P5(a2,a21,a2,a2)),
% 59.42/59.55 inference(scs_inference,[],[4976,5141,5159,5168,5174,4882,4896,4908,4900,5133,4912,4918,4931,4646,4724,4884,4921,4937,4947,4954,5130,4989,4780,4894,4878,4892,4926,5019,5027,5034,5005,5023,4973,4991,5011,5032,5021,4764,442,232,174,173,162,264,265,261,160,263,262,170,169,177,175,230,176,158,157,258,231,259,260,171,172,189,180,204,210,253,207,163,211,246,203,184,197,249,209,195,229,205,255,206,194,179])).
% 59.42/59.55 cnf(5192,plain,
% 59.42/59.55 (P2(x51921,x51921,x51921,x51921)),
% 59.42/59.55 inference(scs_inference,[],[4976,5141,5159,5168,5174,5177,4882,4896,4908,4900,5133,4912,4918,4931,4646,4724,4884,4921,4937,4947,4954,5130,4989,4780,4894,4878,4892,4926,5019,5027,5034,5005,5023,4973,4991,5011,5032,5021,4996,4764,442,232,174,173,162,264,265,261,160,263,262,170,169,177,175,230,176,158,157,258,231,259,260,171,172,189,180,204,210,253,207,163,211,246,203,184,197,249,209,195,229,205,255,206,194,179,188,183,191,196,187,190])).
% 59.42/59.55 cnf(5195,plain,
% 59.42/59.55 (P7(x51951,a2,x51951)),
% 59.42/59.55 inference(rename_variables,[],[4954])).
% 59.42/59.55 cnf(5197,plain,
% 59.42/59.55 (P4(x51971,x51972,x51973,x51973)),
% 59.42/59.55 inference(scs_inference,[],[4976,5141,5159,5168,5174,5177,4882,4896,4908,4900,5133,5151,4912,4918,4931,4646,4724,4884,4921,4937,4947,4954,5130,4989,4780,4894,4878,4892,4926,5019,5027,5034,5005,5023,4973,4991,5011,5032,5021,4996,5017,4764,4718,442,232,174,173,162,264,265,261,160,263,262,170,169,177,175,230,176,158,157,258,231,259,260,171,172,189,180,204,210,253,207,163,211,246,203,184,197,249,209,195,229,205,255,206,194,179,188,183,191,196,187,190,233,242])).
% 59.42/59.55 cnf(5200,plain,
% 59.42/59.55 (P3(x52001,x52002,x52002,x52001)),
% 59.42/59.55 inference(scs_inference,[],[4976,5141,5159,5168,5174,5177,4882,5171,4896,4908,4900,5133,5151,4912,4918,4931,4646,4724,4884,4921,4937,4947,4954,5130,4989,4780,4894,4878,4892,4926,5019,5027,5034,5005,5023,4973,4991,5011,5032,5021,4996,5017,4764,4718,442,232,174,173,162,264,265,261,160,263,262,170,169,177,175,230,176,158,157,258,231,259,260,171,172,189,180,204,210,253,207,163,211,246,203,184,197,249,209,195,229,205,255,206,194,179,188,183,191,196,187,190,233,242,247])).
% 59.42/59.55 cnf(5201,plain,
% 59.42/59.55 (P9(x52011,x52012,x52012,x52011,x52013,x52014,x52013,x52014)),
% 59.42/59.55 inference(rename_variables,[],[4882])).
% 59.42/59.55 cnf(5207,plain,
% 59.42/59.55 (P7(x52071,x52071,x52071)),
% 59.42/59.55 inference(scs_inference,[],[4976,5141,5159,5168,5174,5177,4882,5171,5201,4896,4908,4900,5133,5151,4912,4918,4931,4646,4724,4884,4921,4937,4947,4954,5130,4958,4989,4780,4894,4878,4892,4926,5019,5027,5034,5005,5023,4973,4991,5011,5032,5021,4996,5017,4764,4718,4672,442,232,174,173,162,264,265,261,160,263,262,170,169,177,175,230,176,158,157,258,231,259,260,171,172,189,180,204,210,253,207,163,211,246,203,184,197,249,209,195,229,205,255,206,194,179,188,183,191,196,187,190,233,242,247,198,245])).
% 59.42/59.55 cnf(5209,plain,
% 59.42/59.55 (P1(x52091,x52091,x52092)),
% 59.42/59.55 inference(rename_variables,[],[4900])).
% 59.42/59.55 cnf(5217,plain,
% 59.42/59.55 (P7(x52171,a2,x52171)),
% 59.42/59.55 inference(rename_variables,[],[4954])).
% 59.42/59.55 cnf(5218,plain,
% 59.42/59.55 (P1(x52181,x52182,x52182)),
% 59.42/59.55 inference(rename_variables,[],[4708])).
% 59.42/59.55 cnf(5227,plain,
% 59.42/59.55 (P10(a3,a1,a2,a16)),
% 59.42/59.55 inference(scs_inference,[],[142,4976,5141,5159,5168,5174,5177,4882,5171,5201,4896,4908,4900,5133,5151,5209,4912,4918,4931,4646,4724,4884,4921,4937,4947,4954,5130,5195,5217,4958,4989,4780,4894,4878,4892,4926,5019,5027,5034,5005,5023,4973,4991,5011,5032,5021,4996,5017,4764,5138,4809,4778,4792,4718,4708,5218,4672,4644,442,232,174,173,162,264,265,261,160,263,262,170,169,177,175,230,176,158,157,258,231,259,260,171,172,189,180,204,210,253,207,163,211,246,203,184,197,249,209,195,229,205,255,206,194,179,188,183,191,196,187,190,233,242,247,198,245,212,214,215,257,278])).
% 59.42/59.55 cnf(5229,plain,
% 59.42/59.55 (P7(a3,a2,a2)),
% 59.42/59.55 inference(scs_inference,[],[142,4976,5141,5159,5168,5174,5177,4882,5171,5201,4896,4908,4900,5133,5151,5209,4912,4918,4931,4646,4724,4884,4921,4937,4947,4954,5130,5195,5217,4958,4989,4780,4894,4878,4892,4926,5019,5027,5034,5005,5023,4973,4991,5011,5032,5021,4996,5017,4764,5138,4809,4778,4792,4718,4708,5218,4672,4644,442,232,174,173,162,264,265,261,160,263,262,170,169,177,175,230,176,158,157,258,231,259,260,171,172,189,180,204,210,253,207,163,211,246,203,184,197,249,209,195,229,205,255,206,194,179,188,183,191,196,187,190,233,242,247,198,245,212,214,215,257,278,986])).
% 59.42/59.55 cnf(5231,plain,
% 59.42/59.55 (P7(a3,a16,a16)),
% 59.42/59.55 inference(scs_inference,[],[142,4976,5141,5159,5168,5174,5177,4882,5171,5201,4896,4908,4900,5133,5151,5209,4912,4918,4931,4646,4724,4884,4921,4937,4947,4954,5130,5195,5217,4958,4989,4780,4894,4878,4892,4926,5019,5027,5034,5005,5023,4973,4991,5011,5032,5021,4996,5017,4764,5138,4809,4778,4792,4718,4708,5218,4672,4644,442,232,174,173,162,264,265,261,160,263,262,170,169,177,175,230,176,158,157,258,231,259,260,171,172,189,180,204,210,253,207,163,211,246,203,184,197,249,209,195,229,205,255,206,194,179,188,183,191,196,187,190,233,242,247,198,245,212,214,215,257,278,986,1328])).
% 59.42/59.55 cnf(5233,plain,
% 59.42/59.55 (P9(a3,a16,a16,a16,a16,a16,a3,a16)),
% 59.42/59.55 inference(scs_inference,[],[142,4976,5141,5159,5168,5174,5177,4882,5171,5201,4896,4908,4900,5133,5151,5209,4912,4918,4931,4646,4724,4884,4921,4937,4947,4954,5130,5195,5217,4958,4989,4780,4894,4878,4892,4926,5019,5027,5034,5005,5023,4973,4991,5011,5032,5021,4996,5017,4764,5138,4809,4778,4792,4718,4708,5218,4672,4644,442,232,174,173,162,264,265,261,160,263,262,170,169,177,175,230,176,158,157,258,231,259,260,171,172,189,180,204,210,253,207,163,211,246,203,184,197,249,209,195,229,205,255,206,194,179,188,183,191,196,187,190,233,242,247,198,245,212,214,215,257,278,986,1328,1424])).
% 59.42/59.55 cnf(5265,plain,
% 59.42/59.55 (P8(a18,a3,a3,a2,a18,a3,a3,a2)),
% 59.42/59.55 inference(scs_inference,[],[5143,1941])).
% 59.42/59.55 cnf(5266,plain,
% 59.42/59.55 (P8(a1,a2,a2,a16,a1,a2,a2,a16)),
% 59.42/59.55 inference(scs_inference,[],[5143,1948])).
% 59.42/59.55 cnf(5276,plain,
% 59.42/59.55 (P10(a16,a18,a3,a2)),
% 59.42/59.55 inference(scs_inference,[],[5200,314])).
% 59.42/59.55 cnf(5277,plain,
% 59.42/59.55 (P3(x52771,x52772,x52772,x52771)),
% 59.42/59.55 inference(rename_variables,[],[5200])).
% 59.42/59.55 cnf(5280,plain,
% 59.42/59.55 (P3(x52801,x52802,x52802,x52801)),
% 59.42/59.55 inference(rename_variables,[],[5200])).
% 59.42/59.55 cnf(5283,plain,
% 59.42/59.55 (P3(x52831,x52832,x52832,x52831)),
% 59.42/59.55 inference(rename_variables,[],[5200])).
% 59.42/59.55 cnf(5286,plain,
% 59.42/59.55 (P3(x52861,x52862,x52862,x52861)),
% 59.42/59.55 inference(rename_variables,[],[5200])).
% 59.42/59.55 cnf(5289,plain,
% 59.42/59.55 (P3(x52891,x52892,x52892,x52891)),
% 59.42/59.55 inference(rename_variables,[],[5200])).
% 59.42/59.55 cnf(5291,plain,
% 59.42/59.55 (P10(a2,a17,a3,a16)),
% 59.42/59.55 inference(scs_inference,[],[5200,5277,5280,5283,5286,5289,314,417,388,341,370,442])).
% 59.42/59.55 cnf(5292,plain,
% 59.42/59.55 (P3(x52921,x52922,x52922,x52921)),
% 59.42/59.55 inference(rename_variables,[],[5200])).
% 59.42/59.55 cnf(5297,plain,
% 59.42/59.55 (P3(x52971,x52972,x52972,x52971)),
% 59.42/59.55 inference(rename_variables,[],[5200])).
% 59.42/59.55 cnf(5299,plain,
% 59.42/59.55 (P5(a3,a2,a3,a2)),
% 59.42/59.55 inference(scs_inference,[],[5200,5277,5280,5283,5286,5289,5292,5085,5229,314,417,388,341,370,442,232,1238,162])).
% 59.42/59.55 cnf(5303,plain,
% 59.42/59.55 (P5(x53031,x53031,x53031,a2)),
% 59.42/59.55 inference(scs_inference,[],[5200,5277,5280,5283,5286,5289,5292,5085,5229,5161,314,417,388,341,370,442,232,1238,162,159,173])).
% 59.42/59.55 cnf(5305,plain,
% 59.42/59.55 (P3(f8(x53051,x53051,x53051,x53051),x53051,x53051,x53051)),
% 59.42/59.55 inference(scs_inference,[],[5192,5200,5277,5280,5283,5286,5289,5292,5085,5229,5161,314,417,388,341,370,442,232,1238,162,159,173,193])).
% 59.42/59.55 cnf(5313,plain,
% 59.42/59.55 (P9(x53131,x53132,x53132,x53131,x53133,x53134,x53134,x53133)),
% 59.42/59.55 inference(scs_inference,[],[5062,5192,5121,5200,5277,5280,5283,5286,5289,5292,4886,5085,5129,5229,5161,314,417,388,341,370,442,232,1238,162,159,173,193,174,265,264,261])).
% 59.42/59.55 cnf(5317,plain,
% 59.42/59.55 (P7(f27(a2,x53171,a2,x53171,x53171,x53171),x53171,a2)),
% 59.42/59.55 inference(scs_inference,[],[5062,5192,5121,5200,5277,5280,5283,5286,5289,5292,4886,5085,5129,5229,5161,314,417,388,341,370,442,232,1238,162,159,173,193,174,265,264,261,263,160])).
% 59.42/59.55 cnf(5323,plain,
% 59.42/59.55 (P10(x53231,x53231,a2,a2)),
% 59.42/59.55 inference(scs_inference,[],[5062,5192,5121,5200,5277,5280,5283,5286,5289,5292,4886,5085,5143,4880,5129,5227,5229,5161,314,417,388,341,370,442,232,1238,162,159,173,193,174,265,264,261,263,160,262,170,169])).
% 59.42/59.55 cnf(5325,plain,
% 59.42/59.55 (P4(x53251,x53251,x53251,x53252)),
% 59.42/59.55 inference(scs_inference,[],[5062,5192,5109,5121,5200,5277,5280,5283,5286,5289,5292,4886,5085,5143,4880,5129,5227,5229,5161,314,417,388,341,370,442,232,1238,162,159,173,193,174,265,264,261,263,160,262,170,169,177])).
% 59.42/59.55 cnf(5329,plain,
% 59.42/59.55 (P4(a3,x53291,a2,a3)),
% 59.42/59.55 inference(scs_inference,[],[5062,5192,5109,5121,5200,5277,5280,5283,5286,5289,5292,4886,5085,5143,4898,4880,5129,5227,5229,5161,314,417,388,341,370,442,232,1238,162,159,173,193,174,265,264,261,263,160,262,170,169,177,230,175])).
% 59.42/59.55 cnf(5333,plain,
% 59.42/59.55 (P4(x53331,x53332,x53333,x53332)),
% 59.42/59.55 inference(scs_inference,[],[5062,5192,5109,5121,5200,5277,5280,5283,5286,5289,5292,5197,4886,5085,5143,4898,4880,5129,5227,5229,4923,5161,314,417,388,341,370,442,232,1238,162,159,173,193,174,265,264,261,263,160,262,170,169,177,230,175,158,176])).
% 59.42/59.55 cnf(5337,plain,
% 59.42/59.55 (P9(a18,a20,x53371,x53372,a17,a2,x53371,x53372)),
% 59.42/59.55 inference(scs_inference,[],[5062,5192,5109,5121,5200,5277,5280,5283,5286,5289,5292,5197,4886,4888,5085,5143,4898,4880,5129,5227,5229,4923,5161,314,417,388,341,370,442,232,1238,162,159,173,193,174,265,264,261,263,160,262,170,169,177,230,175,158,176,157,231])).
% 59.42/59.55 cnf(5341,plain,
% 59.42/59.55 (P9(a3,a2,a3,a21,a2,a2,a2,a21)),
% 59.42/59.55 inference(scs_inference,[],[5062,5192,5109,5121,5200,5277,5280,5283,5286,5289,5292,5197,4706,4981,4886,4888,5085,5143,4898,4880,5129,5227,5229,4923,5161,314,417,388,341,370,442,232,1238,162,159,173,193,174,265,264,261,263,160,262,170,169,177,230,175,158,176,157,231,259,258])).
% 59.42/59.55 cnf(5345,plain,
% 59.42/59.55 (P3(x53451,x53452,x53451,x53452)),
% 59.42/59.55 inference(scs_inference,[],[5062,5192,5109,5121,5200,5277,5280,5283,5286,5289,5292,5297,5197,4706,4981,4886,4888,5085,5143,4898,4880,5129,5227,5229,4923,5161,314,417,388,341,370,442,232,1238,162,159,173,193,174,265,264,261,263,160,262,170,169,177,230,175,158,176,157,231,259,258,260,172])).
% 59.42/59.55 cnf(5349,plain,
% 59.42/59.55 (P10(f27(x53491,x53491,x53491,x53491,x53491,x53491),x53491,x53491,x53491)),
% 59.42/59.55 inference(scs_inference,[],[5062,5192,5207,5109,5121,5200,5277,5280,5283,5286,5289,5292,5297,5197,4706,4981,4886,4888,5085,5143,4898,4880,5129,5227,5229,4987,4923,5161,314,417,388,341,370,442,232,1238,162,159,173,193,174,265,264,261,263,160,262,170,169,177,230,175,158,176,157,231,259,258,260,172,171,210])).
% 59.42/59.55 cnf(5352,plain,
% 59.42/59.55 (P3(x53521,x53522,x53522,x53521)),
% 59.42/59.55 inference(rename_variables,[],[5200])).
% 59.42/59.55 cnf(5356,plain,
% 59.42/59.55 (P3(x53561,x53562,x53562,x53561)),
% 59.42/59.55 inference(rename_variables,[],[5200])).
% 59.42/59.55 cnf(5359,plain,
% 59.42/59.55 (P5(x53591,a2,x53591,x53591)),
% 59.42/59.55 inference(rename_variables,[],[5085])).
% 59.42/59.55 cnf(5364,plain,
% 59.42/59.55 (P3(x53641,x53642,x53642,x53641)),
% 59.42/59.55 inference(rename_variables,[],[5200])).
% 59.42/59.55 cnf(5366,plain,
% 59.42/59.55 (P7(f27(x53661,x53661,x53661,x53661,x53661,x53661),x53661,x53661)),
% 59.42/59.55 inference(scs_inference,[],[142,5062,5192,5207,5109,5121,5200,5277,5280,5283,5286,5289,5292,5297,5352,5356,5197,4706,4981,4886,4888,5085,5143,4898,4880,5129,5227,5229,4987,4923,5161,409,314,417,388,341,370,442,232,1238,162,159,173,193,174,265,264,261,263,160,262,170,169,177,230,175,158,176,157,231,259,258,260,172,171,210,200,129,204,207,211,254,209])).
% 59.42/59.55 cnf(5369,plain,
% 59.42/59.55 (P3(x53691,x53692,x53692,x53691)),
% 59.42/59.55 inference(rename_variables,[],[5200])).
% 59.42/59.55 cnf(5376,plain,
% 59.42/59.55 (P3(x53761,x53762,x53762,x53761)),
% 59.42/59.55 inference(rename_variables,[],[5200])).
% 59.42/59.55 cnf(5383,plain,
% 59.42/59.55 (P5(x53831,a2,x53831,x53831)),
% 59.42/59.55 inference(rename_variables,[],[5085])).
% 59.42/59.55 cnf(5384,plain,
% 59.42/59.55 (P3(x53841,x53842,x53842,x53841)),
% 59.42/59.55 inference(rename_variables,[],[5200])).
% 59.42/59.55 cnf(5386,plain,
% 59.42/59.55 (P2(f9(x53861,x53861,x53862),x53861,x53861,x53862)),
% 59.42/59.55 inference(scs_inference,[],[142,5062,5192,5207,5109,5121,5200,5277,5280,5283,5286,5289,5292,5297,5352,5356,5364,5369,5376,5384,5197,4609,4706,4981,4886,4888,5085,5359,5143,4898,4880,5081,5129,5227,5229,4987,4923,5161,409,314,417,388,341,370,442,232,1238,162,159,173,193,174,265,264,261,263,160,262,170,169,177,230,175,158,176,157,231,259,258,260,172,171,210,200,129,204,207,211,254,209,203,184,249,199,161,229,205,197])).
% 59.42/59.55 cnf(5387,plain,
% 59.42/59.55 (P3(x53871,x53872,x53872,x53871)),
% 59.42/59.55 inference(rename_variables,[],[5200])).
% 59.42/59.55 cnf(5391,plain,
% 59.42/59.55 (P3(x53911,x53912,x53912,x53911)),
% 59.42/59.55 inference(rename_variables,[],[5200])).
% 59.42/59.55 cnf(5393,plain,
% 59.42/59.55 (P5(a2,x53931,a2,a2)),
% 59.42/59.55 inference(scs_inference,[],[142,5062,5192,5207,5109,5121,5200,5277,5280,5283,5286,5289,5292,5297,5352,5356,5364,5369,5376,5384,5387,5391,5197,4609,4706,4981,4886,4888,5085,5359,5143,4898,4880,5081,5129,5227,5229,4987,4923,5161,4989,409,314,417,388,341,370,442,232,1238,162,159,173,193,174,265,264,261,263,160,262,170,169,177,230,175,158,176,157,231,259,258,260,172,171,210,200,129,204,207,211,254,209,203,184,249,199,161,229,205,197,195,179])).
% 59.42/59.55 cnf(5395,plain,
% 59.42/59.55 (P3(x53951,x53952,x53952,x53951)),
% 59.42/59.55 inference(rename_variables,[],[5200])).
% 59.42/59.55 cnf(5398,plain,
% 59.42/59.55 (P9(x53981,x53982,x53983,x53984,x53982,x53981,x53984,x53983)),
% 59.42/59.55 inference(rename_variables,[],[5121])).
% 59.42/59.55 cnf(5403,plain,
% 59.42/59.55 (P5(x54031,a2,x54031,x54031)),
% 59.42/59.55 inference(rename_variables,[],[5085])).
% 59.42/59.55 cnf(5409,plain,
% 59.42/59.55 (P3(x54091,x54092,x54092,x54091)),
% 59.42/59.55 inference(rename_variables,[],[5200])).
% 59.42/59.55 cnf(5411,plain,
% 59.42/59.55 (P3(a2,a21,a2,a2)),
% 59.42/59.55 inference(scs_inference,[],[142,5062,5192,5207,5109,5121,5200,5277,5280,5283,5286,5289,5292,5297,5352,5356,5364,5369,5376,5384,5387,5391,5395,5197,4609,4706,4981,4886,4888,5085,5359,5383,5143,4898,4880,5081,5129,5179,5227,5229,4987,4923,5161,4989,409,5034,314,417,388,341,370,442,232,1238,162,159,173,193,174,265,264,261,263,160,262,170,169,177,230,175,158,176,157,231,259,258,260,172,171,210,200,129,204,207,211,254,209,203,184,249,199,161,229,205,197,195,179,268,194,206,183,196,187])).
% 59.42/59.55 cnf(5416,plain,
% 59.42/59.55 (P2(x54161,a2,x54161,x54161)),
% 59.42/59.55 inference(scs_inference,[],[142,5062,5192,5207,5109,5121,5200,5277,5280,5283,5286,5289,5292,5297,5352,5356,5364,5369,5376,5384,5387,5391,5395,5197,4609,4706,4981,4886,4888,5085,5359,5383,5403,5143,4898,4880,5081,5129,5179,5227,5229,4987,4923,5161,4989,409,5034,314,417,388,341,370,442,232,1238,162,159,173,193,174,265,264,261,263,160,262,170,169,177,230,175,158,176,157,231,259,258,260,172,171,210,200,129,204,207,211,254,209,203,184,249,199,161,229,205,197,195,179,268,194,206,183,196,187,233,190])).
% 59.42/59.55 cnf(5429,plain,
% 59.42/59.55 (P7(f7(x54291,x54291,x54291),x54291,x54291)),
% 59.42/59.55 inference(scs_inference,[],[142,5062,5192,5207,5109,5121,5398,5200,5277,5280,5283,5286,5289,5292,5297,5352,5356,5364,5369,5376,5384,5387,5391,5395,5409,5197,4609,4706,4981,4886,4888,5085,5359,5383,5403,5143,4898,5105,4880,5081,5129,5179,5227,5229,4987,4923,5161,4989,409,4764,5034,4636,314,417,388,341,370,442,232,1238,162,159,173,193,174,265,264,261,263,160,262,170,169,177,230,175,158,176,157,231,259,258,260,172,171,210,200,129,204,207,211,254,209,203,184,249,199,161,229,205,197,195,179,268,194,206,183,196,187,233,190,242,247,198,192])).
% 59.42/59.55 cnf(5431,plain,
% 59.42/59.55 (P3(x54311,x54312,x54312,x54311)),
% 59.42/59.55 inference(rename_variables,[],[5200])).
% 59.42/59.55 cnf(5434,plain,
% 59.42/59.55 (P10(a2,a2,x54341,x54341)),
% 59.42/59.55 inference(rename_variables,[],[5143])).
% 59.42/59.55 cnf(5437,plain,
% 59.42/59.55 (P1(x54371,x54371,x54372)),
% 59.42/59.55 inference(rename_variables,[],[4900])).
% 59.42/59.55 cnf(5440,plain,
% 59.42/59.55 (P7(f24(a16,x54401),a16,x54401)),
% 59.42/59.55 inference(scs_inference,[],[142,5062,5192,5207,5109,5121,5398,5200,5277,5280,5283,5286,5289,5292,5297,5352,5356,5364,5369,5376,5384,5387,5391,5395,5409,5197,4609,4706,4981,4886,4888,5085,5359,5383,5403,5143,5434,4898,5105,4880,5081,5129,5179,5227,5229,5231,4987,4923,5161,4900,5437,4989,409,4764,5034,4636,314,417,388,341,370,442,232,1238,162,159,173,193,174,265,264,261,263,160,262,170,169,177,230,175,158,176,157,231,259,258,260,172,171,210,200,129,204,207,211,254,209,203,184,249,199,161,229,205,197,195,179,268,194,206,183,196,187,233,190,242,247,198,192,234,212,165])).
% 59.42/59.55 cnf(5458,plain,
% 59.42/59.55 (P9(a2,f10(a2,a2,a2),a2,a2,a2,a2,a2,a2)),
% 59.42/59.55 inference(scs_inference,[],[142,5062,5192,5207,5091,5109,5121,5398,5200,5277,5280,5283,5286,5289,5292,5297,5352,5356,5364,5369,5376,5384,5387,5391,5395,5409,5431,5197,4609,4706,4981,4886,4888,5085,5359,5383,5403,5143,5434,4898,5105,4880,5081,5103,5129,5179,5227,5229,5231,4987,4943,4923,5161,4900,5437,4488,4989,409,4764,5034,4636,314,417,388,341,370,442,232,1238,162,159,173,193,174,265,264,261,263,160,262,170,169,177,230,175,158,176,157,231,259,258,260,172,171,210,200,129,204,207,211,254,209,203,184,249,199,161,229,205,197,195,179,268,194,206,183,196,187,233,190,242,247,198,192,234,212,165,257,2,1328,986,1424,266,251,235])).
% 59.42/59.55 cnf(5461,plain,
% 59.42/59.55 (P7(a1,a2,a16)),
% 59.42/59.55 inference(scs_inference,[],[142,5062,5192,5207,5091,5109,5121,5398,5200,5277,5280,5283,5286,5289,5292,5297,5352,5356,5364,5369,5376,5384,5387,5391,5395,5409,5431,5197,4609,4706,4981,4886,4888,5085,5359,5383,5403,5143,5434,4898,5105,4880,5081,5103,5129,5179,5227,5229,5231,4987,4943,4923,5161,4900,5437,4488,4989,409,4764,5034,4636,314,417,388,341,370,442,232,1238,162,159,173,193,174,265,264,261,263,160,262,170,169,177,230,175,158,176,157,231,259,258,260,172,171,210,200,129,204,207,211,254,209,203,184,249,199,161,229,205,197,195,179,268,194,206,183,196,187,233,190,242,247,198,192,234,212,165,257,2,1328,986,1424,266,251,235,168])).
% 59.42/59.55 cnf(5477,plain,
% 59.42/59.55 (P4(x54771,x54772,x54773,x54773)),
% 59.42/59.55 inference(rename_variables,[],[5197])).
% 59.42/59.55 cnf(5479,plain,
% 59.42/59.55 (P3(x54791,x54792,x54791,x54792)),
% 59.42/59.55 inference(rename_variables,[],[5345])).
% 59.42/59.55 cnf(5482,plain,
% 59.42/59.55 (P3(x54821,x54822,x54821,x54822)),
% 59.42/59.55 inference(rename_variables,[],[5345])).
% 59.42/59.55 cnf(5485,plain,
% 59.42/59.55 (P3(x54851,x54852,x54851,x54852)),
% 59.42/59.55 inference(rename_variables,[],[5345])).
% 59.42/59.55 cnf(5488,plain,
% 59.42/59.55 (P3(x54881,x54882,x54881,x54882)),
% 59.42/59.55 inference(rename_variables,[],[5345])).
% 59.42/59.55 cnf(5491,plain,
% 59.42/59.55 (P7(f7(x54911,x54911,x54911),x54911,x54911)),
% 59.42/59.55 inference(rename_variables,[],[5429])).
% 59.42/59.55 cnf(5494,plain,
% 59.42/59.55 (P3(x54941,x54942,x54941,x54942)),
% 59.42/59.55 inference(rename_variables,[],[5345])).
% 59.42/59.55 cnf(5499,plain,
% 59.42/59.55 (P3(x54991,x54992,x54991,x54992)),
% 59.42/59.55 inference(rename_variables,[],[5345])).
% 59.42/59.55 cnf(5502,plain,
% 59.42/59.55 (P7(f7(x55021,x55021,x55021),x55021,x55021)),
% 59.42/59.55 inference(rename_variables,[],[5429])).
% 59.42/59.55 cnf(5505,plain,
% 59.42/59.55 (P3(x55051,x55052,x55051,x55052)),
% 59.42/59.55 inference(rename_variables,[],[5345])).
% 59.42/59.55 cnf(5513,plain,
% 59.42/59.55 (P5(a2,a2,a2,x55131)),
% 59.42/59.55 inference(scs_inference,[],[5345,5479,5482,5485,5488,5494,5499,5303,5393,5429,5491,5502,5317,5197,4485,417,370,278,341,1328,314,232,388,986,442,2,1424,159,173])).
% 59.42/59.55 cnf(5517,plain,
% 59.42/59.55 (P5(x55171,x55171,a2,x55171)),
% 59.42/59.55 inference(scs_inference,[],[5345,5479,5482,5485,5488,5494,5499,5303,5416,5393,5429,5491,5502,5317,5197,4485,417,370,278,341,1328,314,232,388,986,442,2,1424,159,173,193,174])).
% 59.42/59.55 cnf(5519,plain,
% 59.42/59.55 (P10(x55191,x55191,x55191,a2)),
% 59.42/59.55 inference(scs_inference,[],[5345,5479,5482,5485,5488,5494,5499,5303,5416,5393,5429,5491,5502,5317,5197,4485,417,370,278,341,1328,314,232,388,986,442,2,1424,159,173,193,174,239])).
% 59.42/59.55 cnf(5521,plain,
% 59.42/59.55 (P5(a1,a2,a1,a16)),
% 59.42/59.55 inference(scs_inference,[],[5345,5479,5482,5485,5488,5494,5499,5303,5416,5393,5461,5429,5491,5502,5317,5197,4485,417,370,278,341,1328,314,232,388,986,442,2,1424,159,173,193,174,239,162])).
% 59.42/59.55 cnf(5533,plain,
% 59.42/59.55 (P7(a1,a16,a2)),
% 59.42/59.55 inference(scs_inference,[],[5066,5265,5345,5479,5482,5485,5488,5494,5499,4722,5303,5416,5393,5276,5461,5429,5491,5502,5317,5197,4485,417,370,278,341,1328,314,232,388,986,442,2,1424,159,173,193,174,239,162,265,264,261,263,169,160])).
% 59.42/59.55 cnf(5537,plain,
% 59.42/59.55 (P4(x55371,x55372,x55372,x55373)),
% 59.42/59.55 inference(scs_inference,[],[5066,5265,5345,5479,5482,5485,5488,5494,5499,5333,4722,5303,5416,5393,5087,5276,5461,5429,5491,5502,5317,5197,4485,417,370,278,341,1328,314,232,388,986,442,2,1424,159,173,193,174,239,162,265,264,261,263,169,160,262,177])).
% 59.42/59.55 cnf(5541,plain,
% 59.42/59.55 (P9(x55411,x55412,x55411,x55413,x55413,x55412,x55413,x55413)),
% 59.42/59.55 inference(scs_inference,[],[5066,5265,5345,5479,5482,5485,5488,5494,5499,5333,4722,5303,5416,5393,5087,5276,5461,5429,5491,5502,5317,5197,4485,417,370,278,341,1328,314,232,388,986,442,2,1424,159,173,193,174,239,162,265,264,261,263,169,160,262,177,170,230])).
% 59.42/59.55 cnf(5545,plain,
% 59.42/59.55 (P4(x55451,x55452,x55453,x55451)),
% 59.42/59.55 inference(scs_inference,[],[5066,5265,5345,5479,5482,5485,5488,5494,5499,5333,4722,5303,5416,5329,5393,5087,5276,5461,5429,5491,5502,5317,5197,4485,417,370,278,341,1328,314,232,388,986,442,2,1424,159,173,193,174,239,162,265,264,261,263,169,160,262,177,170,230,176,175])).
% 59.42/59.55 cnf(5549,plain,
% 59.42/59.55 (P9(a16,a16,a3,a16,a3,a16,a16,a16)),
% 59.42/59.55 inference(scs_inference,[],[5066,5265,5345,5479,5482,5485,5488,5494,5499,5333,5233,4722,5303,5416,5329,5393,5087,5276,5461,5429,5491,5502,5153,5317,5197,4485,417,370,278,341,1328,314,232,388,986,442,2,1424,159,173,193,174,239,162,265,264,261,263,169,160,262,177,170,230,176,175,157,259])).
% 59.42/59.55 cnf(5559,plain,
% 59.42/59.55 (P3(a2,a2,a2,a21)),
% 59.42/59.55 inference(scs_inference,[],[5066,5265,5345,5479,5482,5485,5488,5494,5499,5333,5147,5233,4722,5303,5416,5329,5393,5087,5276,5411,5461,5429,5491,5502,5153,5317,5197,4485,417,370,278,341,1328,314,232,388,986,442,2,1424,159,173,193,174,239,162,265,264,261,263,169,160,262,177,170,230,176,175,157,259,158,231,258,260,171])).
% 59.42/59.55 cnf(5564,plain,
% 59.42/59.55 (P3(x55641,x55642,x55641,x55642)),
% 59.42/59.55 inference(rename_variables,[],[5345])).
% 59.42/59.55 cnf(5567,plain,
% 59.42/59.55 (P3(x55671,x55672,x55671,x55672)),
% 59.42/59.55 inference(rename_variables,[],[5345])).
% 59.42/59.55 cnf(5574,plain,
% 59.42/59.55 (P5(x55741,x55741,x55741,a2)),
% 59.42/59.55 inference(rename_variables,[],[5303])).
% 59.42/59.55 cnf(5575,plain,
% 59.42/59.55 (P3(x55751,x55752,x55751,x55752)),
% 59.42/59.55 inference(rename_variables,[],[5345])).
% 59.42/59.55 cnf(5581,plain,
% 59.42/59.55 (~E(a21,a20)),
% 59.42/59.55 inference(scs_inference,[],[5066,5265,5345,5479,5482,5485,5488,5494,5499,5505,5564,5567,5333,4613,5147,5233,4694,4722,5303,5416,5329,5393,5087,5276,5411,5461,5429,5491,5502,5153,5317,5132,5197,5477,4803,382,4485,417,370,278,341,1328,314,232,388,986,442,2,1424,159,173,193,174,239,162,265,264,261,263,169,160,262,177,170,230,176,175,157,259,158,231,258,260,171,172,256,252,253,210,200,211,269,130])).
% 59.42/59.55 cnf(5582,plain,
% 59.42/59.55 (P4(x55821,x55822,x55823,x55823)),
% 59.42/59.55 inference(rename_variables,[],[5197])).
% 59.42/59.55 cnf(5584,plain,
% 59.42/59.55 (P3(x55841,x55842,x55841,x55842)),
% 59.42/59.55 inference(rename_variables,[],[5345])).
% 59.42/59.55 cnf(5588,plain,
% 59.42/59.55 (P3(f13(a16,a16,a16,a2,a1),a16,a2,a1)),
% 59.42/59.55 inference(scs_inference,[],[5066,5265,5345,5479,5482,5485,5488,5494,5499,5505,5564,5567,5575,5584,5333,4613,5147,5233,4694,4722,5303,5574,5416,5329,5393,5087,5276,5411,5461,5429,5491,5502,5153,5317,5132,4496,5197,5477,4803,382,4485,417,370,278,341,1328,314,232,388,986,442,2,1424,159,173,193,174,239,162,265,264,261,263,169,160,262,177,170,230,176,175,157,259,158,231,258,260,171,172,256,252,253,210,200,211,269,130,207,131,204])).
% 59.42/59.55 cnf(5589,plain,
% 59.42/59.55 (P3(x55891,x55892,x55891,x55892)),
% 59.42/59.55 inference(rename_variables,[],[5345])).
% 59.42/59.55 cnf(5594,plain,
% 59.42/59.55 (P3(x55941,x55942,x55941,x55942)),
% 59.42/59.55 inference(rename_variables,[],[5345])).
% 59.42/59.55 cnf(5599,plain,
% 59.42/59.55 (P5(x55991,x55991,x55991,a2)),
% 59.42/59.55 inference(rename_variables,[],[5303])).
% 59.42/59.55 cnf(5600,plain,
% 59.42/59.55 (P3(x56001,x56002,x56001,x56002)),
% 59.42/59.55 inference(rename_variables,[],[5345])).
% 59.42/59.55 cnf(5603,plain,
% 59.42/59.55 (P3(x56031,x56032,x56031,x56032)),
% 59.42/59.55 inference(rename_variables,[],[5345])).
% 59.42/59.55 cnf(5605,plain,
% 59.42/59.55 (P1(f6(x56051,x56051,x56052),x56052,x56051)),
% 59.42/59.55 inference(scs_inference,[],[5066,5265,5345,5479,5482,5485,5488,5494,5499,5505,5564,5567,5575,5584,5589,5594,5600,5603,5333,4613,5147,5233,4694,4722,5303,5574,5599,5416,5329,5393,5087,5276,5411,5461,5429,5491,5502,5153,5317,5132,4496,5197,5477,4803,382,4485,417,370,278,341,1328,314,232,388,986,442,2,1424,159,173,193,174,239,162,265,264,261,263,169,160,262,177,170,230,176,175,157,259,158,231,258,260,171,172,256,252,253,210,200,211,269,130,207,131,204,254,203,209,199,205,184])).
% 59.42/59.55 cnf(5607,plain,
% 59.42/59.55 (P5(f8(a21,a21,a21,a21),a21,f8(a21,a21,a21,a21),a21)),
% 59.42/59.55 inference(scs_inference,[],[5066,5265,5345,5479,5482,5485,5488,5494,5499,5505,5564,5567,5575,5584,5589,5594,5600,5603,5333,4613,5147,5233,4694,4722,5303,5574,5599,5416,5329,5393,5087,5276,5411,5461,5305,5429,5491,5502,5153,5317,5132,4496,5197,5477,4803,4958,382,4485,417,370,278,341,1328,314,232,388,986,442,2,1424,159,173,193,174,239,162,265,264,261,263,169,160,262,177,170,230,176,175,157,259,158,231,258,260,171,172,256,252,253,210,200,211,269,130,207,131,204,254,203,209,199,205,184,179])).
% 59.42/59.55 cnf(5613,plain,
% 59.42/59.55 (P3(a2,x56131,x56131,x56131)),
% 59.42/59.55 inference(scs_inference,[],[5066,5265,5345,5479,5482,5485,5488,5494,5499,5505,5564,5567,5575,5584,5589,5594,5600,5603,5333,4613,5147,5233,4694,4722,5303,5574,5599,5416,5329,5393,5087,5276,5411,5461,5305,5429,5491,5502,5153,5317,5132,4496,5197,5477,4803,4958,382,4778,4485,417,370,278,341,1328,314,232,388,986,442,2,1424,159,173,193,174,239,162,265,264,261,263,169,160,262,177,170,230,176,175,157,259,158,231,258,260,171,172,256,252,253,210,200,211,269,130,207,131,204,254,203,209,199,205,184,179,255,178])).
% 59.42/59.55 cnf(5616,plain,
% 59.42/59.55 (P3(x56161,f5(x56161,x56161,x56162),x56162,x56161)),
% 59.42/59.55 inference(scs_inference,[],[5066,5265,5345,5479,5482,5485,5488,5494,5499,5505,5564,5567,5575,5584,5589,5594,5600,5603,5333,4613,5147,5233,4694,4722,5303,5574,5599,5416,5329,5393,5087,5276,5411,5461,5305,5429,5491,5502,5153,5317,5132,4496,5197,5477,4803,4958,382,4778,4485,417,370,278,341,1328,314,232,388,986,442,2,1424,159,173,193,174,239,162,265,264,261,263,169,160,262,177,170,230,176,175,157,259,158,231,258,260,171,172,256,252,253,210,200,211,269,130,207,131,204,254,203,209,199,205,184,179,255,178,195])).
% 59.42/59.55 cnf(5634,plain,
% 59.42/59.55 (P2(x56341,x56341,a2,a2)),
% 59.42/59.55 inference(scs_inference,[],[5066,5265,5345,5479,5482,5485,5488,5494,5499,5505,5564,5567,5575,5584,5589,5594,5600,5603,5333,4613,5147,5233,4694,4722,5303,5574,5599,5416,5329,5393,5087,5276,5299,5411,5461,5366,5305,5429,5491,5502,5153,5317,5132,4496,5200,5197,5477,4803,4958,4894,382,4778,5034,4485,417,370,278,341,1328,314,232,388,986,442,2,1424,159,173,193,174,239,162,265,264,261,263,169,160,262,177,170,230,176,175,157,259,158,231,258,260,171,172,256,252,253,210,200,211,269,130,207,131,204,254,203,209,199,205,184,179,255,178,195,197,229,206,183,196,187,233,190])).
% 59.42/59.55 cnf(5636,plain,
% 59.42/59.55 (P3(a18,a20,a17,a2)),
% 59.42/59.55 inference(scs_inference,[],[5066,5265,5345,5479,5482,5485,5488,5494,5499,5505,5564,5567,5575,5584,5589,5594,5600,5603,5333,4613,5147,5233,4694,4722,5303,5574,5599,5416,5337,5329,5393,5087,5276,5299,5411,5461,5366,5305,5429,5491,5502,5153,5317,5132,4496,5200,5197,5477,4803,4958,4894,382,4778,5034,4485,417,370,278,341,1328,314,232,388,986,442,2,1424,159,173,193,174,239,162,265,264,261,263,169,160,262,177,170,230,176,175,157,259,158,231,258,260,171,172,256,252,253,210,200,211,269,130,207,131,204,254,203,209,199,205,184,179,255,178,195,197,229,206,183,196,187,233,190,247])).
% 59.42/59.55 cnf(5638,plain,
% 59.42/59.55 (P3(x56381,x56382,x56381,x56382)),
% 59.42/59.55 inference(rename_variables,[],[5345])).
% 59.42/59.55 cnf(5642,plain,
% 59.42/59.55 (P10(x56421,x56421,a2,a2)),
% 59.42/59.55 inference(rename_variables,[],[5323])).
% 59.42/59.55 cnf(5646,plain,
% 59.42/59.55 (P7(f27(x56461,x56461,x56461,x56461,x56461,x56461),x56461,x56461)),
% 59.42/59.55 inference(rename_variables,[],[5366])).
% 59.42/59.55 cnf(5649,plain,
% 59.42/59.55 (P7(a16,a2,a1)),
% 59.42/59.55 inference(scs_inference,[],[5066,5265,5345,5479,5482,5485,5488,5494,5499,5505,5564,5567,5575,5584,5589,5594,5600,5603,5638,5333,4613,5147,5233,4694,4722,5303,5574,5599,5416,5323,5337,5329,5393,5087,5276,5299,5411,5461,5366,5305,5429,5491,5502,5153,5317,5440,5132,4496,5200,5197,5477,5582,4803,4958,4894,382,4778,5034,4644,4485,417,370,278,341,1328,314,232,388,986,442,2,1424,159,173,193,174,239,162,265,264,261,263,169,160,262,177,170,230,176,175,157,259,158,231,258,260,171,172,256,252,253,210,200,211,269,130,207,131,204,254,203,209,199,205,184,179,255,178,195,197,229,206,183,196,187,233,190,247,198,192,168])).
% 59.42/59.55 cnf(5656,plain,
% 59.42/59.55 (P7(f24(a21,x56561),a21,x56561)),
% 59.42/59.55 inference(scs_inference,[],[5066,5265,5345,5479,5482,5485,5488,5494,5499,5505,5564,5567,5575,5584,5589,5594,5600,5603,5638,5333,4613,5147,5233,4694,4722,5303,5574,5599,5416,5323,5642,5337,5329,5393,5087,5276,5299,5411,5461,5366,5646,5305,5429,5491,5502,5153,5317,5440,5132,4496,5200,5197,5477,5582,4402,4803,4958,4894,382,4900,4778,5034,4644,4485,417,370,278,341,1328,314,232,388,986,442,2,1424,159,173,193,174,239,162,265,264,261,263,169,160,262,177,170,230,176,175,157,259,158,231,258,260,171,172,256,252,253,210,200,211,269,130,207,131,204,254,203,209,199,205,184,179,255,178,195,197,229,206,183,196,187,233,190,247,198,192,168,212,165])).
% 59.42/59.55 cnf(5660,plain,
% 59.42/59.55 (P5(x56601,x56601,x56602,x56602)),
% 59.42/59.55 inference(scs_inference,[],[5066,5265,5313,5325,5345,5479,5482,5485,5488,5494,5499,5505,5564,5567,5575,5584,5589,5594,5600,5603,5638,5333,4613,5147,5233,4694,4722,5303,5574,5599,5416,5323,5642,5337,5329,5393,5087,5276,5299,5411,5461,5366,5646,5305,5429,5491,5502,5153,5317,5440,5132,4496,5200,5197,5477,5582,4402,4803,4958,4894,382,4900,4778,5034,4644,4485,417,370,278,341,1328,314,232,388,986,442,2,1424,159,173,193,174,239,162,265,264,261,263,169,160,262,177,170,230,176,175,157,259,158,231,258,260,171,172,256,252,253,210,200,211,269,130,207,131,204,254,203,209,199,205,184,179,255,178,195,197,229,206,183,196,187,233,190,247,198,192,168,212,165,257])).
% 59.42/59.55 cnf(5713,plain,
% 59.42/59.55 (P3(x57131,f5(x57131,x57131,x57132),x57132,x57131)),
% 59.42/59.55 inference(rename_variables,[],[5616])).
% 59.42/59.55 cnf(5716,plain,
% 59.42/59.55 (P3(x57161,f5(x57161,x57161,x57162),x57162,x57161)),
% 59.42/59.55 inference(rename_variables,[],[5616])).
% 59.42/59.55 cnf(5719,plain,
% 59.42/59.55 (P3(x57191,f5(x57191,x57191,x57192),x57192,x57191)),
% 59.42/59.55 inference(rename_variables,[],[5616])).
% 59.42/59.55 cnf(5722,plain,
% 59.42/59.55 (P3(x57221,f5(x57221,x57221,x57222),x57222,x57221)),
% 59.42/59.55 inference(rename_variables,[],[5616])).
% 59.42/59.55 cnf(5725,plain,
% 59.42/59.55 (P3(x57251,f5(x57251,x57251,x57252),x57252,x57251)),
% 59.42/59.55 inference(rename_variables,[],[5616])).
% 59.42/59.55 cnf(5730,plain,
% 59.42/59.55 (P3(x57301,f5(x57301,x57301,x57302),x57302,x57301)),
% 59.42/59.55 inference(rename_variables,[],[5616])).
% 59.42/59.55 cnf(5739,plain,
% 59.42/59.55 (P3(a2,x57391,x57391,x57391)),
% 59.42/59.55 inference(rename_variables,[],[5613])).
% 59.42/59.55 cnf(5791,plain,
% 59.42/59.55 (P4(x57911,x57912,x57912,x57913)),
% 59.42/59.55 inference(rename_variables,[],[5537])).
% 59.42/59.55 cnf(5796,plain,
% 59.42/59.55 (P5(x57961,x57961,x57962,x57962)),
% 59.42/59.55 inference(rename_variables,[],[5660])).
% 59.42/59.55 cnf(5799,plain,
% 59.42/59.55 (P5(x57991,x57991,x57992,x57992)),
% 59.42/59.55 inference(rename_variables,[],[5660])).
% 59.42/59.55 cnf(5811,plain,
% 59.42/59.55 (P3(x58111,x58112,x58112,x58111)),
% 59.42/59.55 inference(rename_variables,[],[5200])).
% 59.42/59.55 cnf(5814,plain,
% 59.42/59.55 (P3(a2,x58141,x58141,x58141)),
% 59.42/59.55 inference(rename_variables,[],[5613])).
% 59.42/59.55 cnf(5817,plain,
% 59.42/59.55 (P3(a2,x58171,x58171,x58171)),
% 59.42/59.55 inference(rename_variables,[],[5613])).
% 59.42/59.55 cnf(5822,plain,
% 59.42/59.55 (P3(a2,x58221,x58221,x58221)),
% 59.42/59.55 inference(rename_variables,[],[5613])).
% 59.42/59.55 cnf(5825,plain,
% 59.42/59.55 (P5(a2,a2,a2,x58251)),
% 59.42/59.55 inference(rename_variables,[],[5513])).
% 59.42/59.55 cnf(5828,plain,
% 59.42/59.55 (P3(x58281,x58282,x58282,x58281)),
% 59.42/59.55 inference(rename_variables,[],[5200])).
% 59.42/59.55 cnf(5831,plain,
% 59.42/59.55 (P3(a2,x58311,x58311,x58311)),
% 59.42/59.55 inference(rename_variables,[],[5613])).
% 59.42/59.55 cnf(5832,plain,
% 59.42/59.55 (P4(x58321,x58322,x58322,x58323)),
% 59.42/59.55 inference(rename_variables,[],[5537])).
% 59.42/59.55 cnf(5835,plain,
% 59.42/59.55 (P5(x58351,x58351,x58352,x58352)),
% 59.42/59.55 inference(rename_variables,[],[5660])).
% 59.42/59.55 cnf(5842,plain,
% 59.42/59.55 (P3(x58421,x58422,x58422,x58421)),
% 59.42/59.55 inference(rename_variables,[],[5200])).
% 59.42/59.55 cnf(5852,plain,
% 59.42/59.55 (P3(a2,x58521,x58521,x58521)),
% 59.42/59.55 inference(rename_variables,[],[5613])).
% 59.42/59.55 cnf(5855,plain,
% 59.42/59.55 (P2(x58551,x58551,a2,a2)),
% 59.42/59.55 inference(rename_variables,[],[5634])).
% 59.42/59.55 cnf(5875,plain,
% 59.42/59.55 (P10(x58751,x58752,x58752,x58751)),
% 59.42/59.55 inference(rename_variables,[],[4644])).
% 59.42/59.55 cnf(5876,plain,
% 59.42/59.55 (P4(x58761,x58762,x58762,x58763)),
% 59.42/59.55 inference(rename_variables,[],[5537])).
% 59.42/59.55 cnf(5885,plain,
% 59.42/59.55 (P1(x58851,x58852,x58851)),
% 59.42/59.55 inference(rename_variables,[],[4778])).
% 59.42/59.55 cnf(5889,plain,
% 59.42/59.55 (P10(x58891,x58892,x58892,x58891)),
% 59.42/59.55 inference(rename_variables,[],[4644])).
% 59.42/59.55 cnf(5892,plain,
% 59.42/59.55 (P1(x58921,x58922,x58921)),
% 59.42/59.55 inference(rename_variables,[],[4778])).
% 59.42/59.55 cnf(5893,plain,
% 59.42/59.55 (P7(a21,x58931,x58931)),
% 59.42/59.55 inference(rename_variables,[],[4958])).
% 59.42/59.55 cnf(5903,plain,
% 59.42/59.55 (P4(x59031,x59032,x59032,x59033)),
% 59.42/59.55 inference(rename_variables,[],[5537])).
% 59.42/59.55 cnf(5906,plain,
% 59.42/59.55 (P4(x59061,x59062,x59062,x59063)),
% 59.42/59.55 inference(rename_variables,[],[5537])).
% 59.42/59.55 cnf(5908,plain,
% 59.42/59.55 ($false),
% 59.42/59.55 inference(scs_inference,[],[142,5266,5541,5660,5796,5799,5835,5537,5791,5832,5876,5903,5906,5545,4940,5099,4786,5549,5291,5517,5519,5613,5739,5814,5817,5822,5831,5852,5581,5634,5855,5513,5825,5089,5123,5341,5521,5533,5559,5636,5649,5349,5386,5616,5713,5716,5719,5722,5725,5730,5605,5656,5607,5588,5458,4874,5105,5440,5299,4882,380,5200,5811,5828,5842,4452,4958,5893,4989,5411,5121,4900,4400,4778,5885,5892,4644,5875,5889,417,341,278,314,370,232,442,388,159,2,1238,193,173,239,174,162,264,265,261,263,177,160,262,169,230,170,176,259,158,231,258,157,260,171,172,236,164,207,200,211,246,210,163,254,204,184,209,203,199,195,197,205,229,128,194,255,179,186,183,178,196,206,187,233,190,247,198,245,168,181,215,214,213,257,4866,175]),
% 59.42/59.55 ['proof']).
% 59.42/59.55 % SZS output end Proof
% 59.42/59.55 % Total time :58.870000s
%------------------------------------------------------------------------------