%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : GEO561+1 : TPTP v8.2.0. Released v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% Computer : 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:44 EDT 2024
% Result : Theorem 59.34s 59.37s
% Output : CNFRefutation 59.38s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.13 % Problem : GEO561+1 : TPTP v8.2.0. Released v7.5.0.
% 0.03/0.13 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% 0.12/0.34 % Computer : n022.cluster.edu
% 0.12/0.34 % Model : x86_64 x86_64
% 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.34 % Memory : 8042.1875MB
% 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.34 % CPULimit : 300
% 0.12/0.34 % WCLimit : 300
% 0.12/0.34 % DateTime : Fri Jun 21 07:23:24 EDT 2024
% 0.12/0.34 % CPUTime :
% 0.57/0.59 start to proof:theBenchmark
% 59.34/59.36 %-------------------------------------------
% 59.34/59.36 % File :CSE---1.7
% 59.34/59.36 % Problem :theBenchmark
% 59.34/59.36 % Transform :cnf
% 59.34/59.36 % Format :tptp:raw
% 59.34/59.36 % Command :java -jar mcs_scs.jar %d %s
% 59.34/59.36
% 59.34/59.36 % Result :Theorem 58.710000s
% 59.34/59.36 % Output :CNFRefutation 58.710000s
% 59.34/59.36 %-------------------------------------------
% 59.34/59.37 %------------------------------------------------------------------------------
% 59.34/59.37 % File : GEO561+1 : TPTP v8.2.0. Released v7.5.0.
% 59.34/59.37 % Domain : Geometry
% 59.34/59.37 % Problem : JGEX problem 22
% 59.34/59.37 % Version : [CGZ00] axioms.
% 59.34/59.37 % English :
% 59.34/59.37
% 59.34/59.37 % Refs : [CGZ00] Chou et al. (2000), A Deductive Database Approach to A
% 59.34/59.37 % : [YCG08] Ye et al. (2008), An Introduction to Java Geometry Exp
% 59.34/59.37 % : [Qua20] Quaresma (2020), Email to Geoff Sutcliffe
% 59.34/59.37 % Source : [Qua20]
% 59.34/59.37 % Names : 22.p [Qua20]
% 59.34/59.37
% 59.34/59.37 % Status : Theorem
% 59.34/59.37 % Rating : 0.39 v8.1.0, 0.47 v7.5.0
% 59.34/59.37 % Syntax : Number of formulae : 95 ( 0 unt; 0 def)
% 59.34/59.37 % Number of atoms : 297 ( 1 equ)
% 59.34/59.37 % Maximal formula atoms : 14 ( 3 avg)
% 59.34/59.37 % Number of connectives : 209 ( 7 ~; 0 |; 107 &)
% 59.34/59.37 % ( 0 <=>; 95 =>; 0 <=; 0 <~>)
% 59.34/59.37 % Maximal formula depth : 26 ( 9 avg)
% 59.34/59.37 % Maximal term depth : 1 ( 1 avg)
% 59.34/59.37 % Number of predicates : 12 ( 11 usr; 0 prp; 2-8 aty)
% 59.34/59.37 % Number of functors : 0 ( 0 usr; 0 con; --- aty)
% 59.34/59.37 % Number of variables : 534 ( 514 !; 20 ?)
% 59.34/59.37 % SPC : FOF_THM_RFO_SEQ
% 59.34/59.37
% 59.34/59.37 % Comments : Taken from JGEX [YCG08], converted by Pedro Quaresma.
% 59.34/59.37 %------------------------------------------------------------------------------
% 59.34/59.37 include('Axioms/GEO012+0.ax').
% 59.34/59.37 %------------------------------------------------------------------------------
% 59.34/59.37 fof(exemplo6GDDFULL214022,conjecture,
% 59.34/59.37 ! [A,B,C,O,P,Q,N,M,E,D,NWPNT1,NWPNT2] :
% 59.34/59.37 ( ( circle(O,A,B,C)
% 59.34/59.37 & perp(P,O,A,C)
% 59.34/59.37 & coll(P,A,C)
% 59.34/59.37 & perp(Q,O,A,B)
% 59.34/59.37 & coll(Q,A,B)
% 59.34/59.37 & coll(N,O,P)
% 59.34/59.37 & circle(O,A,N,NWPNT1)
% 59.34/59.37 & coll(M,O,Q)
% 59.34/59.37 & circle(O,A,M,NWPNT2)
% 59.34/59.37 & coll(E,A,C)
% 59.34/59.37 & coll(E,N,M)
% 59.34/59.37 & coll(D,A,B)
% 59.34/59.37 & coll(D,N,M) )
% 59.34/59.37 => eqangle(A,D,D,E,D,E,E,A) ) ).
% 59.34/59.37
% 59.34/59.37 %------------------------------------------------------------------------------
% 59.34/59.37 %-------------------------------------------
% 59.34/59.37 % Proof found
% 59.34/59.37 % SZS status Theorem for theBenchmark
% 59.34/59.37 % SZS output start Proof
% 59.38/59.38 %ClaNum:268(EqnAxiom:141)
% 59.38/59.38 %VarNum:1613(SingletonVarNum:590)
% 59.38/59.38 %MaxLitNum:5
% 59.38/59.38 %MaxfuncDepth:1
% 59.38/59.38 %SharedTerms:26
% 59.38/59.38 %goalClause: 142 143 144 145 146 147 148 149 150 151 152 153 154 155
% 59.38/59.38 %singleGoalClaCount:14
% 59.38/59.38 [142]P1(a1,a2,a15)
% 59.38/59.38 [143]P1(a18,a2,a16)
% 59.38/59.38 [144]P1(a19,a17,a1)
% 59.38/59.38 [145]P1(a20,a17,a18)
% 59.38/59.38 [146]P1(a21,a2,a15)
% 59.38/59.38 [147]P1(a21,a19,a20)
% 59.38/59.38 [148]P1(a22,a2,a16)
% 59.38/59.38 [149]P1(a22,a19,a20)
% 59.38/59.38 [150]P3(a1,a17,a2,a15)
% 59.38/59.38 [151]P3(a18,a17,a2,a16)
% 59.38/59.38 [152]P2(a17,a2,a16,a15)
% 59.38/59.38 [153]P2(a17,a2,a19,a24)
% 59.38/59.38 [154]P2(a17,a2,a20,a25)
% 59.38/59.38 [155]~P4(a2,a22,a22,a21,a22,a21,a21,a2)
% 59.38/59.38 [156]~P1(x1562,x1561,x1563)+P1(x1561,x1562,x1563)
% 59.38/59.38 [157]~P1(x1571,x1573,x1572)+P1(x1571,x1572,x1573)
% 59.38/59.38 [158]~P8(x1581,x1582,x1583)+P1(x1581,x1582,x1583)
% 59.38/59.38 [159]~P8(x1591,x1593,x1592)+P8(x1591,x1592,x1593)
% 59.38/59.38 [161]~P8(x1611,x1612,x1613)+P5(x1611,x1612,x1611,x1613)
% 59.38/59.38 [165]~P10(x1651,x1652,x1651,x1653)+P1(x1651,x1652,x1653)
% 59.38/59.38 [231]~P5(x2311,x2312,x2311,x2313)+P4(x2311,x2312,x2312,x2313,x2312,x2313,x2311,x2313)
% 59.38/59.38 [168]~P10(x1683,x1684,x1681,x1682)+P10(x1681,x1682,x1683,x1684)
% 59.38/59.38 [169]~P10(x1691,x1692,x1694,x1693)+P10(x1691,x1692,x1693,x1694)
% 59.38/59.38 [170]~P3(x1703,x1704,x1701,x1702)+P3(x1701,x1702,x1703,x1704)
% 59.38/59.38 [171]~P3(x1711,x1712,x1714,x1713)+P3(x1711,x1712,x1713,x1714)
% 59.38/59.38 [172]~P5(x1723,x1724,x1721,x1722)+P5(x1721,x1722,x1723,x1724)
% 59.38/59.38 [173]~P5(x1731,x1732,x1734,x1733)+P5(x1731,x1732,x1733,x1734)
% 59.38/59.38 [174]~P6(x1742,x1741,x1743,x1744)+P6(x1741,x1742,x1743,x1744)
% 59.38/59.38 [175]~P6(x1751,x1753,x1752,x1754)+P6(x1751,x1752,x1753,x1754)
% 59.38/59.38 [176]~P6(x1761,x1762,x1764,x1763)+P6(x1761,x1762,x1763,x1764)
% 59.38/59.38 [229]~P6(x2292,x2293,x2291,x2294)+P4(x2291,x2292,x2291,x2293,x2294,x2292,x2294,x2293)
% 59.38/59.38 [192]~P2(x1924,x1921,x1922,x1923)+P3(f7(x1921,x1922,x1923,x1924),x1921,x1921,x1924)
% 59.38/59.38 [207]P5(x2071,x2072,x2073,x2074)+~P7(x2071,x2072,x2075,x2073,x2074,x2076)
% 59.38/59.38 [219]~P11(x2194,x2195,x2196,x2191,x2192,x2193)+P11(x2191,x2192,x2193,x2194,x2195,x2196)
% 59.38/59.38 [220]~P11(x2202,x2201,x2203,x2205,x2204,x2206)+P11(x2201,x2202,x2203,x2204,x2205,x2206)
% 59.38/59.38 [221]~P11(x2211,x2213,x2212,x2214,x2216,x2215)+P11(x2211,x2212,x2213,x2214,x2215,x2216)
% 59.38/59.39 [222]~P7(x2224,x2225,x2226,x2221,x2222,x2223)+P7(x2221,x2222,x2223,x2224,x2225,x2226)
% 59.38/59.39 [223]~P7(x2232,x2231,x2233,x2235,x2234,x2236)+P7(x2231,x2232,x2233,x2234,x2235,x2236)
% 59.38/59.39 [224]~P7(x2241,x2243,x2242,x2244,x2246,x2245)+P7(x2241,x2242,x2243,x2244,x2245,x2246)
% 59.38/59.39 [230]~P10(x2301,x2302,x2305,x2306)+P4(x2301,x2302,x2303,x2304,x2305,x2306,x2303,x2304)
% 59.38/59.39 [236]~P11(x2361,x2362,x2363,x2364,x2365,x2366)+P4(x2361,x2362,x2362,x2363,x2364,x2365,x2365,x2366)
% 59.38/59.39 [237]~P11(x2371,x2372,x2373,x2374,x2375,x2376)+P9(x2371,x2372,x2371,x2373,x2374,x2375,x2374,x2376)
% 59.38/59.39 [238]~P4(x2381,x2382,x2385,x2386,x2383,x2384,x2385,x2386)+P10(x2381,x2382,x2383,x2384)
% 59.38/59.39 [257]~P4(x2575,x2576,x2577,x2578,x2571,x2572,x2573,x2574)+P4(x2571,x2572,x2573,x2574,x2575,x2576,x2577,x2578)
% 59.38/59.39 [258]~P4(x2583,x2584,x2581,x2582,x2587,x2588,x2585,x2586)+P4(x2581,x2582,x2583,x2584,x2585,x2586,x2587,x2588)
% 59.38/59.39 [259]~P4(x2592,x2591,x2593,x2594,x2595,x2596,x2597,x2598)+P4(x2591,x2592,x2593,x2594,x2595,x2596,x2597,x2598)
% 59.38/59.39 [260]~P4(x2601,x2602,x2605,x2606,x2603,x2604,x2607,x2608)+P4(x2601,x2602,x2603,x2604,x2605,x2606,x2607,x2608)
% 59.38/59.39 [261]~P9(x2615,x2616,x2617,x2618,x2611,x2612,x2613,x2614)+P9(x2611,x2612,x2613,x2614,x2615,x2616,x2617,x2618)
% 59.38/59.39 [262]~P9(x2623,x2624,x2621,x2622,x2627,x2628,x2625,x2626)+P9(x2621,x2622,x2623,x2624,x2625,x2626,x2627,x2628)
% 59.38/59.39 [263]~P9(x2632,x2631,x2633,x2634,x2635,x2636,x2637,x2638)+P9(x2631,x2632,x2633,x2634,x2635,x2636,x2637,x2638)
% 59.38/59.39 [264]~P9(x2641,x2642,x2645,x2646,x2643,x2644,x2647,x2648)+P9(x2641,x2642,x2643,x2644,x2645,x2646,x2647,x2648)
% 59.38/59.39 [166]~P1(x1661,x1662,x1663)+~P5(x1661,x1662,x1661,x1663)+P8(x1661,x1662,x1663)
% 59.38/59.39 [240]P5(x2401,x2402,x2401,x2403)+~P4(x2401,x2402,x2402,x2403,x2402,x2403,x2401,x2403)+P1(x2401,x2402,x2403)
% 59.38/59.39 [181]~P3(x1811,x1812,x1812,x1813)+~P5(x1812,x1811,x1812,x1813)+P1(x1811,x1812,f3(x1811,x1813,x1812))
% 59.38/59.39 [193]~P3(x1932,x1931,x1931,x1933)+~P5(x1931,x1932,x1931,x1933)+P5(x1931,x1932,x1931,f3(x1932,x1933,x1931))
% 59.38/59.39 [160]~P1(x1603,x1604,x1601)+P1(x1601,x1602,x1603)+~P1(x1603,x1604,x1602)
% 59.38/59.39 [177]~P2(x1774,x1771,x1772,x1773)+P3(x1771,x1772,x1772,x1773)+~P1(x1774,x1771,x1773)
% 59.38/59.39 [178]~P3(x1781,x1784,x1782,x1783)+P5(x1781,x1782,x1781,x1783)+~P8(x1784,x1782,x1783)
% 59.38/59.39 [179]~P3(x1791,x1793,x1793,x1794)+P5(x1791,x1792,x1793,x1792)+~P8(x1792,x1791,x1794)
% 59.38/59.39 [186]~P5(x1861,x1864,x1862,x1864)+~P5(x1861,x1863,x1862,x1863)+P3(x1861,x1862,x1863,x1864)
% 59.38/59.39 [189]~P5(x1891,x1892,x1891,x1894)+~P5(x1891,x1892,x1891,x1893)+P2(x1891,x1892,x1893,x1894)
% 59.38/59.39 [235]~P10(x2351,x2354,x2353,x2352)+~P6(x2351,x2354,x2353,x2352)+P4(x2351,x2352,x2353,x2352,x2353,x2352,x2353,x2354)
% 59.38/59.39 [239]~P4(x2391,x2393,x2391,x2394,x2392,x2393,x2392,x2394)+P1(x2391,x2392,x2393)+P6(x2393,x2394,x2391,x2392)
% 59.38/59.39 [241]~P1(x2413,x2414,x2412)+~P4(x2413,x2411,x2413,x2412,x2414,x2411,x2414,x2412)+P6(x2411,x2412,x2413,x2414)
% 59.38/59.39 [243]P3(x2431,x2432,x2433,x2434)+~P4(x2431,x2432,x2433,x2434,x2433,x2434,x2431,x2432)+P10(x2431,x2432,x2433,x2434)
% 59.38/59.39 [182]~P3(x1821,x1824,x1822,x1823)+~P3(x1822,x1824,x1821,x1823)+P1(f4(x1821,x1822,x1823),x1823,x1822)
% 59.38/59.39 [183]~P3(x1831,x1834,x1832,x1833)+~P3(x1832,x1834,x1831,x1833)+P1(f5(x1831,x1832,x1833),x1833,x1831)
% 59.38/59.39 [194]~P3(x1941,x1944,x1942,x1943)+~P3(x1942,x1944,x1941,x1943)+P3(x1941,f4(x1941,x1942,x1943),x1943,x1942)
% 59.38/59.39 [195]~P3(x1951,x1954,x1952,x1953)+~P3(x1952,x1954,x1951,x1953)+P3(x1951,f5(x1952,x1951,x1953),x1953,x1952)
% 59.38/59.39 [196]~P3(x1961,x1963,x1963,x1962)+~P6(x1961,x1962,x1963,x1964)+P2(f8(x1961,x1962,x1963),x1961,x1962,x1963)
% 59.38/59.39 [198]~P3(x1983,x1984,x1982,x1981)+~P5(x1983,x1982,x1983,x1981)+P1(x1981,x1982,f27(x1982,x1981,x1983,x1984))
% 59.38/59.39 [199]~P3(x1993,x1994,x1991,x1992)+~P5(x1993,x1991,x1993,x1992)+P1(f27(x1991,x1992,x1993,x1994),x1993,x1994)
% 59.38/59.39 [250]~P5(x2503,x2502,x2503,x2501)+~P4(x2502,x2503,x2503,x2504,x2503,x2504,x2503,x2501)+P1(x2501,x2502,f23(x2502,x2501,x2503,x2504))
% 59.38/59.39 [251]~P3(x2513,x2514,x2512,x2511)+~P4(x2512,x2513,x2513,x2514,x2513,x2514,x2513,x2511)+P1(x2511,x2512,f28(x2512,x2511,x2513,x2514))
% 59.38/59.39 [252]~P3(x2523,x2522,x2522,x2521)+~P4(x2524,x2523,x2522,x2523,x2522,x2523,x2521,x2523)+P1(f14(x2521,x2522,x2523,x2524),x2523,x2524)
% 59.38/59.39 [253]~P3(x2533,x2532,x2532,x2531)+~P4(x2534,x2533,x2532,x2533,x2532,x2533,x2531,x2533)+P1(f14(x2531,x2532,x2533,x2534),x2531,x2532)
% 59.38/59.39 [254]~P5(x2543,x2541,x2543,x2542)+~P4(x2541,x2543,x2543,x2544,x2543,x2544,x2543,x2542)+P1(f23(x2541,x2542,x2543,x2544),x2543,x2544)
% 59.38/59.39 [255]~P3(x2553,x2554,x2551,x2552)+~P4(x2551,x2553,x2553,x2554,x2553,x2554,x2553,x2552)+P1(f28(x2551,x2552,x2553,x2554),x2553,x2554)
% 59.38/59.39 [162]~P8(x1625,x1621,x1623)+P10(x1621,x1622,x1623,x1624)+~P8(x1625,x1622,x1624)
% 59.38/59.39 [163]~P8(x1631,x1635,x1633)+P10(x1631,x1632,x1633,x1634)+~P8(x1632,x1635,x1634)
% 59.38/59.39 [190]~P6(x1905,x1901,x1902,x1903)+P6(x1901,x1902,x1903,x1904)+~P6(x1905,x1901,x1902,x1904)
% 59.38/59.39 [232]~P8(x2325,x2322,x2323)+~P2(x2324,x2321,x2322,x2323)+P4(x2321,x2322,x2321,x2323,x2324,x2322,x2324,x2325)
% 59.38/59.39 [234]~P2(x2345,x2341,x2343,x2344)+P4(x2341,x2342,x2341,x2343,x2344,x2341,x2344,x2343)+~P3(x2345,x2341,x2341,x2342)
% 59.38/59.39 [247]~P4(x2472,x2473,x2472,x2474,x2475,x2472,x2475,x2474)+P3(x2471,x2472,x2472,x2473)+~P2(x2471,x2472,x2474,x2475)
% 59.38/59.39 [202]~P1(x2022,x2024,x2025)+~P3(x2021,x2023,x2023,x2022)+P1(f12(x2021,x2022,x2023,x2024,x2025),x2024,x2025)
% 59.38/59.39 [203]~P1(x2032,x2034,x2035)+~P3(x2031,x2033,x2033,x2032)+P3(f12(x2031,x2032,x2033,x2034,x2035),x2031,x2034,x2035)
% 59.38/59.39 [204]~P3(x2043,x2044,x2044,x2041)+~P5(x2041,x2042,x2041,x2045)+P5(x2041,x2042,x2041,f31(x2043,x2044,x2042,x2045,x2041))
% 59.38/59.39 [205]~P3(x2053,x2051,x2051,x2055)+~P5(x2055,x2052,x2055,x2054)+P5(x2051,x2052,x2051,f31(x2053,x2051,x2052,x2054,x2055))
% 59.38/59.39 [206]~P3(x2061,x2062,x2062,x2065)+~P5(x2065,x2063,x2065,x2064)+P10(f31(x2061,x2062,x2063,x2064,x2065),x2063,x2061,x2062)
% 59.38/59.39 [249]~P4(x2491,x2493,x2492,x2493,x2491,x2494,x2492,x2495)+P1(x2491,x2492,x2493)+P6(x2494,x2492,x2493,f30(x2491,x2492,x2493,x2494))
% 59.38/59.39 [265]~P4(x2651,x2653,x2652,x2653,x2651,x2654,x2652,x2655)+P1(x2651,x2652,x2653)+P4(x2651,x2653,x2652,x2653,x2651,f30(x2651,x2652,x2653,x2654),x2652,f30(x2651,x2652,x2653,x2654))
% 59.38/59.39 [184]~P10(x1841,x1842,x1845,x1846)+P10(x1841,x1842,x1843,x1844)+~P10(x1845,x1846,x1843,x1844)
% 59.38/59.39 [185]~P3(x1851,x1852,x1855,x1856)+P10(x1851,x1852,x1853,x1854)+~P3(x1855,x1856,x1853,x1854)
% 59.38/59.39 [187]~P3(x1875,x1876,x1873,x1874)+P3(x1871,x1872,x1873,x1874)+~P10(x1871,x1872,x1875,x1876)
% 59.38/59.39 [188]~P5(x1881,x1882,x1885,x1886)+P5(x1881,x1882,x1883,x1884)+~P5(x1885,x1886,x1883,x1884)
% 59.38/59.39 [225]~P5(x2251,x2252,x2254,x2255)+~P11(x2251,x2252,x2253,x2254,x2255,x2256)+P7(x2251,x2252,x2253,x2254,x2255,x2256)
% 59.38/59.39 [228]~P8(x2284,x2285,x2286)+~P8(x2281,x2282,x2283)+P9(x2281,x2282,x2282,x2283,x2284,x2285,x2285,x2286)
% 59.38/59.39 [208]~P8(x2086,x2083,x2084)+~P8(x2085,x2081,x2082)+P8(f29(x2081,x2082,x2083,x2084,x2085,x2086),x2081,x2084)
% 59.38/59.39 [209]~P8(x2096,x2093,x2094)+~P8(x2095,x2091,x2092)+P10(f29(x2091,x2092,x2093,x2094,x2095,x2096),x2096,x2091,x2093)
% 59.38/59.39 [210]~P8(x2106,x2103,x2104)+~P8(x2105,x2101,x2102)+P10(f29(x2101,x2102,x2103,x2104,x2105,x2106),x2105,x2102,x2104)
% 59.38/59.39 [245]~P4(x2451,x2452,x2453,x2454,x2455,x2456,x2457,x2458)+P10(x2451,x2452,x2453,x2454)+~P10(x2455,x2456,x2457,x2458)
% 59.38/59.39 [246]~P4(x2461,x2462,x2463,x2464,x2465,x2466,x2467,x2468)+P3(x2461,x2462,x2463,x2464)+~P3(x2465,x2466,x2467,x2468)
% 59.38/59.39 [248]~P9(x2481,x2482,x2483,x2484,x2485,x2486,x2487,x2488)+P5(x2481,x2482,x2483,x2484)+~P5(x2485,x2486,x2487,x2488)
% 59.38/59.39 [226]~P11(x2261,x2262,x2263,x2267,x2268,x2269)+P11(x2261,x2262,x2263,x2264,x2265,x2266)+~P11(x2267,x2268,x2269,x2264,x2265,x2266)
% 59.38/59.39 [227]~P7(x2271,x2272,x2273,x2277,x2278,x2279)+P7(x2271,x2272,x2273,x2274,x2275,x2276)+~P7(x2277,x2278,x2279,x2274,x2275,x2276)
% 59.38/59.39 [267]~P4(x2671,x2672,x2673,x2674,x2679,x26710,x26711,x26712)+P4(x2671,x2672,x2673,x2674,x2675,x2676,x2677,x2678)+~P4(x2679,x26710,x26711,x26712,x2675,x2676,x2677,x2678)
% 59.38/59.39 [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.38/59.39 [200]~P5(x2002,x2001,x2004,x2001)+~P6(x2002,x2004,x2001,x2003)+P3(x2001,x2002,x2002,x2003)+~P5(x2002,x2003,x2004,x2003)
% 59.38/59.39 [167]~P1(x1671,x1672,x1673)+~P10(x1674,x1671,x1675,x1673)+P8(x1671,x1672,x1673)+~P8(x1674,x1672,x1675)
% 59.38/59.39 [180]~P10(x1804,x1803,x1805,x1802)+~P10(x1804,x1802,x1805,x1803)+P8(x1801,x1802,x1803)+~P8(x1801,x1804,x1805)
% 59.38/59.39 [201]~P5(x2015,x2011,x2015,x2013)+~P5(x2015,x2011,x2015,x2012)+P6(x2011,x2012,x2013,x2014)+~P5(x2015,x2011,x2015,x2014)
% 59.38/59.39 [233]~P1(x2331,x2334,x2335)+~P1(x2331,x2332,x2333)+~P10(x2332,x2334,x2333,x2335)+P9(x2331,x2332,x2332,x2333,x2331,x2334,x2334,x2335)
% 59.38/59.39 [244]~P1(x2441,x2442,x2443)+~P4(x2445,x2442,x2445,x2443,x2444,x2442,x2444,x2441)+P8(x2441,x2442,x2443)+~P2(x2444,x2445,x2442,x2443)
% 59.38/59.39 [191]~P3(x1913,x1911,x1913,x1915)+~P3(x1911,x1912,x1911,x1913)+~P8(x1914,x1912,x1915)+P8(f6(x1911,x1912,x1913),x1911,x1913)
% 59.38/59.39 [197]~P6(x1971,x1972,x1973,x1975)+~P10(x1971,x1972,x1973,x1975)+~P8(x1974,x1971,x1972)+P2(f9(x1971,x1972,x1973),x1971,x1972,x1973)
% 59.38/59.39 [266]~P4(x2661,x2663,x2662,x2663,x2664,x2666,x2665,x2666)+~P4(x2661,x2662,x2662,x2663,x2664,x2665,x2665,x2666)+P1(x2661,x2662,x2663)+P11(x2661,x2662,x2663,x2664,x2665,x2666)
% 59.38/59.39 [256]~P6(x2561,x2562,x2565,x2564)+~P6(x2561,x2562,x2565,x2563)+~P4(x2565,x2561,x2565,x2562,x2566,x2563,x2566,x2564)+P5(x2561,x2562,x2563,x2564)+~P6(x2561,x2562,x2565,x2566)
% 59.38/59.39 [211]~P1(x2112,x2113,x2114)+~P1(x2111,x2114,x2116)+~P1(x2111,x2113,x2115)+~P10(x2113,x2114,x2115,x2116)+P1(x2111,x2112,f13(x2113,x2114,x2115,x2116,x2111,x2112))
% 59.38/59.39 [212]~P1(x2126,x2121,x2122)+~P1(x2125,x2122,x2124)+~P1(x2125,x2121,x2123)+~P10(x2121,x2122,x2123,x2124)+P1(f13(x2121,x2122,x2123,x2124,x2125,x2126),x2123,x2124)
% 59.38/59.39 [213]~P1(x2133,x2134,x2135)+~P8(x2136,x2131,x2132)+~P10(x2131,x2133,x2135,x2136)+~P10(x2131,x2133,x2132,x2134)+P1(f32(x2131,x2132,x2133,x2134,x2135,x2136),x2136,x2135)
% 59.38/59.39 [214]~P1(x2143,x2144,x2145)+~P8(x2146,x2141,x2142)+~P10(x2141,x2143,x2145,x2146)+~P10(x2141,x2143,x2142,x2144)+P1(f32(x2141,x2142,x2143,x2144,x2145,x2146),x2141,x2144)
% 59.38/59.39 [215]~P5(x2152,x2153,x2152,x2154)+~P5(x2151,x2153,x2151,x2156)+~P2(x2151,x2153,x2154,x2155)+E(x2151,x2152)+P1(f10(x2153,x2154,x2155,x2156,x2151,x2152),x2153,x2155)
% 59.38/59.39 [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),x2164,x2166)
% 59.38/59.39 [217]~P5(x2172,x2173,x2172,x2174)+~P5(x2171,x2173,x2171,x2176)+~P2(x2171,x2173,x2174,x2175)+E(x2171,x2172)+P5(f10(x2173,x2174,x2175,x2176,x2171,x2172),x2172,x2172,x2173)
% 59.38/59.39 [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.38/59.39 [164]~P1(x1643,x1641,x1644)+~P1(x1645,x1641,x1644)+~P8(x1646,x1645,x1643)+~P8(x1647,x1641,x1644)+P8(f26(x1641,x1642),x1641,x1642)
% 59.38/59.39 %EqnAxiom
% 59.38/59.39 [1]E(x11,x11)
% 59.38/59.39 [2]E(x22,x21)+~E(x21,x22)
% 59.38/59.39 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 59.38/59.39 [4]~E(x41,x42)+E(f26(x41,x43),f26(x42,x43))
% 59.38/59.39 [5]~E(x51,x52)+E(f26(x53,x51),f26(x53,x52))
% 59.38/59.39 [6]~E(x61,x62)+E(f3(x61,x63,x64),f3(x62,x63,x64))
% 59.38/59.39 [7]~E(x71,x72)+E(f3(x73,x71,x74),f3(x73,x72,x74))
% 59.38/59.39 [8]~E(x81,x82)+E(f3(x83,x84,x81),f3(x83,x84,x82))
% 59.38/59.39 [9]~E(x91,x92)+E(f4(x91,x93,x94),f4(x92,x93,x94))
% 59.38/59.39 [10]~E(x101,x102)+E(f4(x103,x101,x104),f4(x103,x102,x104))
% 59.38/59.39 [11]~E(x111,x112)+E(f4(x113,x114,x111),f4(x113,x114,x112))
% 59.38/59.39 [12]~E(x121,x122)+E(f5(x121,x123,x124),f5(x122,x123,x124))
% 59.38/59.39 [13]~E(x131,x132)+E(f5(x133,x131,x134),f5(x133,x132,x134))
% 59.38/59.39 [14]~E(x141,x142)+E(f5(x143,x144,x141),f5(x143,x144,x142))
% 59.38/59.39 [15]~E(x151,x152)+E(f6(x151,x153,x154),f6(x152,x153,x154))
% 59.38/59.39 [16]~E(x161,x162)+E(f6(x163,x161,x164),f6(x163,x162,x164))
% 59.38/59.39 [17]~E(x171,x172)+E(f6(x173,x174,x171),f6(x173,x174,x172))
% 59.38/59.39 [18]~E(x181,x182)+E(f7(x181,x183,x184,x185),f7(x182,x183,x184,x185))
% 59.38/59.39 [19]~E(x191,x192)+E(f7(x193,x191,x194,x195),f7(x193,x192,x194,x195))
% 59.38/59.39 [20]~E(x201,x202)+E(f7(x203,x204,x201,x205),f7(x203,x204,x202,x205))
% 59.38/59.39 [21]~E(x211,x212)+E(f7(x213,x214,x215,x211),f7(x213,x214,x215,x212))
% 59.38/59.39 [22]~E(x221,x222)+E(f30(x221,x223,x224,x225),f30(x222,x223,x224,x225))
% 59.38/59.39 [23]~E(x231,x232)+E(f30(x233,x231,x234,x235),f30(x233,x232,x234,x235))
% 59.38/59.39 [24]~E(x241,x242)+E(f30(x243,x244,x241,x245),f30(x243,x244,x242,x245))
% 59.38/59.39 [25]~E(x251,x252)+E(f30(x253,x254,x255,x251),f30(x253,x254,x255,x252))
% 59.38/59.39 [26]~E(x261,x262)+E(f23(x261,x263,x264,x265),f23(x262,x263,x264,x265))
% 59.38/59.39 [27]~E(x271,x272)+E(f23(x273,x271,x274,x275),f23(x273,x272,x274,x275))
% 59.38/59.39 [28]~E(x281,x282)+E(f23(x283,x284,x281,x285),f23(x283,x284,x282,x285))
% 59.38/59.39 [29]~E(x291,x292)+E(f23(x293,x294,x295,x291),f23(x293,x294,x295,x292))
% 59.38/59.39 [30]~E(x301,x302)+E(f28(x301,x303,x304,x305),f28(x302,x303,x304,x305))
% 59.38/59.39 [31]~E(x311,x312)+E(f28(x313,x311,x314,x315),f28(x313,x312,x314,x315))
% 59.38/59.39 [32]~E(x321,x322)+E(f28(x323,x324,x321,x325),f28(x323,x324,x322,x325))
% 59.38/59.39 [33]~E(x331,x332)+E(f28(x333,x334,x335,x331),f28(x333,x334,x335,x332))
% 59.38/59.39 [34]~E(x341,x342)+E(f8(x341,x343,x344),f8(x342,x343,x344))
% 59.38/59.39 [35]~E(x351,x352)+E(f8(x353,x351,x354),f8(x353,x352,x354))
% 59.38/59.39 [36]~E(x361,x362)+E(f8(x363,x364,x361),f8(x363,x364,x362))
% 59.38/59.39 [37]~E(x371,x372)+E(f9(x371,x373,x374),f9(x372,x373,x374))
% 59.38/59.39 [38]~E(x381,x382)+E(f9(x383,x381,x384),f9(x383,x382,x384))
% 59.38/59.39 [39]~E(x391,x392)+E(f9(x393,x394,x391),f9(x393,x394,x392))
% 59.38/59.39 [40]~E(x401,x402)+E(f27(x401,x403,x404,x405),f27(x402,x403,x404,x405))
% 59.38/59.39 [41]~E(x411,x412)+E(f27(x413,x411,x414,x415),f27(x413,x412,x414,x415))
% 59.38/59.39 [42]~E(x421,x422)+E(f27(x423,x424,x421,x425),f27(x423,x424,x422,x425))
% 59.38/59.39 [43]~E(x431,x432)+E(f27(x433,x434,x435,x431),f27(x433,x434,x435,x432))
% 59.38/59.39 [44]~E(x441,x442)+E(f14(x441,x443,x444,x445),f14(x442,x443,x444,x445))
% 59.38/59.39 [45]~E(x451,x452)+E(f14(x453,x451,x454,x455),f14(x453,x452,x454,x455))
% 59.38/59.39 [46]~E(x461,x462)+E(f14(x463,x464,x461,x465),f14(x463,x464,x462,x465))
% 59.38/59.39 [47]~E(x471,x472)+E(f14(x473,x474,x475,x471),f14(x473,x474,x475,x472))
% 59.38/59.39 [48]~E(x481,x482)+E(f12(x481,x483,x484,x485,x486),f12(x482,x483,x484,x485,x486))
% 59.38/59.39 [49]~E(x491,x492)+E(f12(x493,x491,x494,x495,x496),f12(x493,x492,x494,x495,x496))
% 59.38/59.39 [50]~E(x501,x502)+E(f12(x503,x504,x501,x505,x506),f12(x503,x504,x502,x505,x506))
% 59.38/59.39 [51]~E(x511,x512)+E(f12(x513,x514,x515,x511,x516),f12(x513,x514,x515,x512,x516))
% 59.38/59.39 [52]~E(x521,x522)+E(f12(x523,x524,x525,x526,x521),f12(x523,x524,x525,x526,x522))
% 59.38/59.39 [53]~E(x531,x532)+E(f11(x531,x533,x534,x535,x536,x537),f11(x532,x533,x534,x535,x536,x537))
% 59.38/59.39 [54]~E(x541,x542)+E(f11(x543,x541,x544,x545,x546,x547),f11(x543,x542,x544,x545,x546,x547))
% 59.38/59.39 [55]~E(x551,x552)+E(f11(x553,x554,x551,x555,x556,x557),f11(x553,x554,x552,x555,x556,x557))
% 59.38/59.39 [56]~E(x561,x562)+E(f11(x563,x564,x565,x561,x566,x567),f11(x563,x564,x565,x562,x566,x567))
% 59.38/59.39 [57]~E(x571,x572)+E(f11(x573,x574,x575,x576,x571,x577),f11(x573,x574,x575,x576,x572,x577))
% 59.38/59.39 [58]~E(x581,x582)+E(f11(x583,x584,x585,x586,x587,x581),f11(x583,x584,x585,x586,x587,x582))
% 59.38/59.39 [59]~E(x591,x592)+E(f31(x591,x593,x594,x595,x596),f31(x592,x593,x594,x595,x596))
% 59.38/59.39 [60]~E(x601,x602)+E(f31(x603,x601,x604,x605,x606),f31(x603,x602,x604,x605,x606))
% 59.38/59.39 [61]~E(x611,x612)+E(f31(x613,x614,x611,x615,x616),f31(x613,x614,x612,x615,x616))
% 59.38/59.39 [62]~E(x621,x622)+E(f31(x623,x624,x625,x621,x626),f31(x623,x624,x625,x622,x626))
% 59.38/59.39 [63]~E(x631,x632)+E(f31(x633,x634,x635,x636,x631),f31(x633,x634,x635,x636,x632))
% 59.38/59.39 [64]~E(x641,x642)+E(f10(x641,x643,x644,x645,x646,x647),f10(x642,x643,x644,x645,x646,x647))
% 59.38/59.39 [65]~E(x651,x652)+E(f10(x653,x651,x654,x655,x656,x657),f10(x653,x652,x654,x655,x656,x657))
% 59.38/59.39 [66]~E(x661,x662)+E(f10(x663,x664,x661,x665,x666,x667),f10(x663,x664,x662,x665,x666,x667))
% 59.38/59.39 [67]~E(x671,x672)+E(f10(x673,x674,x675,x671,x676,x677),f10(x673,x674,x675,x672,x676,x677))
% 59.38/59.39 [68]~E(x681,x682)+E(f10(x683,x684,x685,x686,x681,x687),f10(x683,x684,x685,x686,x682,x687))
% 59.38/59.39 [69]~E(x691,x692)+E(f10(x693,x694,x695,x696,x697,x691),f10(x693,x694,x695,x696,x697,x692))
% 59.38/59.39 [70]~E(x701,x702)+E(f32(x701,x703,x704,x705,x706,x707),f32(x702,x703,x704,x705,x706,x707))
% 59.38/59.39 [71]~E(x711,x712)+E(f32(x713,x711,x714,x715,x716,x717),f32(x713,x712,x714,x715,x716,x717))
% 59.38/59.39 [72]~E(x721,x722)+E(f32(x723,x724,x721,x725,x726,x727),f32(x723,x724,x722,x725,x726,x727))
% 59.38/59.39 [73]~E(x731,x732)+E(f32(x733,x734,x735,x731,x736,x737),f32(x733,x734,x735,x732,x736,x737))
% 59.38/59.39 [74]~E(x741,x742)+E(f32(x743,x744,x745,x746,x741,x747),f32(x743,x744,x745,x746,x742,x747))
% 59.38/59.39 [75]~E(x751,x752)+E(f32(x753,x754,x755,x756,x757,x751),f32(x753,x754,x755,x756,x757,x752))
% 59.38/59.39 [76]~E(x761,x762)+E(f29(x761,x763,x764,x765,x766,x767),f29(x762,x763,x764,x765,x766,x767))
% 59.38/59.39 [77]~E(x771,x772)+E(f29(x773,x771,x774,x775,x776,x777),f29(x773,x772,x774,x775,x776,x777))
% 59.38/59.39 [78]~E(x781,x782)+E(f29(x783,x784,x781,x785,x786,x787),f29(x783,x784,x782,x785,x786,x787))
% 59.38/59.39 [79]~E(x791,x792)+E(f29(x793,x794,x795,x791,x796,x797),f29(x793,x794,x795,x792,x796,x797))
% 59.38/59.39 [80]~E(x801,x802)+E(f29(x803,x804,x805,x806,x801,x807),f29(x803,x804,x805,x806,x802,x807))
% 59.38/59.39 [81]~E(x811,x812)+E(f29(x813,x814,x815,x816,x817,x811),f29(x813,x814,x815,x816,x817,x812))
% 59.38/59.39 [82]~E(x821,x822)+E(f13(x821,x823,x824,x825,x826,x827),f13(x822,x823,x824,x825,x826,x827))
% 59.38/59.39 [83]~E(x831,x832)+E(f13(x833,x831,x834,x835,x836,x837),f13(x833,x832,x834,x835,x836,x837))
% 59.38/59.39 [84]~E(x841,x842)+E(f13(x843,x844,x841,x845,x846,x847),f13(x843,x844,x842,x845,x846,x847))
% 59.38/59.39 [85]~E(x851,x852)+E(f13(x853,x854,x855,x851,x856,x857),f13(x853,x854,x855,x852,x856,x857))
% 59.38/59.39 [86]~E(x861,x862)+E(f13(x863,x864,x865,x866,x861,x867),f13(x863,x864,x865,x866,x862,x867))
% 59.38/59.39 [87]~E(x871,x872)+E(f13(x873,x874,x875,x876,x877,x871),f13(x873,x874,x875,x876,x877,x872))
% 59.38/59.39 [88]P1(x882,x883,x884)+~E(x881,x882)+~P1(x881,x883,x884)
% 59.38/59.39 [89]P1(x893,x892,x894)+~E(x891,x892)+~P1(x893,x891,x894)
% 59.38/59.39 [90]P1(x903,x904,x902)+~E(x901,x902)+~P1(x903,x904,x901)
% 59.38/59.39 [91]P9(x912,x913,x914,x915,x916,x917,x918,x919)+~E(x911,x912)+~P9(x911,x913,x914,x915,x916,x917,x918,x919)
% 59.38/59.39 [92]P9(x923,x922,x924,x925,x926,x927,x928,x929)+~E(x921,x922)+~P9(x923,x921,x924,x925,x926,x927,x928,x929)
% 59.38/59.39 [93]P9(x933,x934,x932,x935,x936,x937,x938,x939)+~E(x931,x932)+~P9(x933,x934,x931,x935,x936,x937,x938,x939)
% 59.38/59.39 [94]P9(x943,x944,x945,x942,x946,x947,x948,x949)+~E(x941,x942)+~P9(x943,x944,x945,x941,x946,x947,x948,x949)
% 59.38/59.39 [95]P9(x953,x954,x955,x956,x952,x957,x958,x959)+~E(x951,x952)+~P9(x953,x954,x955,x956,x951,x957,x958,x959)
% 59.38/59.39 [96]P9(x963,x964,x965,x966,x967,x962,x968,x969)+~E(x961,x962)+~P9(x963,x964,x965,x966,x967,x961,x968,x969)
% 59.38/59.39 [97]P9(x973,x974,x975,x976,x977,x978,x972,x979)+~E(x971,x972)+~P9(x973,x974,x975,x976,x977,x978,x971,x979)
% 59.38/59.39 [98]P9(x983,x984,x985,x986,x987,x988,x989,x982)+~E(x981,x982)+~P9(x983,x984,x985,x986,x987,x988,x989,x981)
% 59.38/59.39 [99]P4(x992,x993,x994,x995,x996,x997,x998,x999)+~E(x991,x992)+~P4(x991,x993,x994,x995,x996,x997,x998,x999)
% 59.38/59.39 [100]P4(x1003,x1002,x1004,x1005,x1006,x1007,x1008,x1009)+~E(x1001,x1002)+~P4(x1003,x1001,x1004,x1005,x1006,x1007,x1008,x1009)
% 59.38/59.39 [101]P4(x1013,x1014,x1012,x1015,x1016,x1017,x1018,x1019)+~E(x1011,x1012)+~P4(x1013,x1014,x1011,x1015,x1016,x1017,x1018,x1019)
% 59.38/59.39 [102]P4(x1023,x1024,x1025,x1022,x1026,x1027,x1028,x1029)+~E(x1021,x1022)+~P4(x1023,x1024,x1025,x1021,x1026,x1027,x1028,x1029)
% 59.38/59.39 [103]P4(x1033,x1034,x1035,x1036,x1032,x1037,x1038,x1039)+~E(x1031,x1032)+~P4(x1033,x1034,x1035,x1036,x1031,x1037,x1038,x1039)
% 59.38/59.39 [104]P4(x1043,x1044,x1045,x1046,x1047,x1042,x1048,x1049)+~E(x1041,x1042)+~P4(x1043,x1044,x1045,x1046,x1047,x1041,x1048,x1049)
% 59.38/59.39 [105]P4(x1053,x1054,x1055,x1056,x1057,x1058,x1052,x1059)+~E(x1051,x1052)+~P4(x1053,x1054,x1055,x1056,x1057,x1058,x1051,x1059)
% 59.38/59.39 [106]P4(x1063,x1064,x1065,x1066,x1067,x1068,x1069,x1062)+~E(x1061,x1062)+~P4(x1063,x1064,x1065,x1066,x1067,x1068,x1069,x1061)
% 59.38/59.39 [107]P2(x1072,x1073,x1074,x1075)+~E(x1071,x1072)+~P2(x1071,x1073,x1074,x1075)
% 59.38/59.39 [108]P2(x1083,x1082,x1084,x1085)+~E(x1081,x1082)+~P2(x1083,x1081,x1084,x1085)
% 59.38/59.39 [109]P2(x1093,x1094,x1092,x1095)+~E(x1091,x1092)+~P2(x1093,x1094,x1091,x1095)
% 59.38/59.39 [110]P2(x1103,x1104,x1105,x1102)+~E(x1101,x1102)+~P2(x1103,x1104,x1105,x1101)
% 59.38/59.39 [111]P3(x1112,x1113,x1114,x1115)+~E(x1111,x1112)+~P3(x1111,x1113,x1114,x1115)
% 59.38/59.39 [112]P3(x1123,x1122,x1124,x1125)+~E(x1121,x1122)+~P3(x1123,x1121,x1124,x1125)
% 59.38/59.39 [113]P3(x1133,x1134,x1132,x1135)+~E(x1131,x1132)+~P3(x1133,x1134,x1131,x1135)
% 59.38/59.39 [114]P3(x1143,x1144,x1145,x1142)+~E(x1141,x1142)+~P3(x1143,x1144,x1145,x1141)
% 59.38/59.39 [115]P10(x1152,x1153,x1154,x1155)+~E(x1151,x1152)+~P10(x1151,x1153,x1154,x1155)
% 59.38/59.39 [116]P10(x1163,x1162,x1164,x1165)+~E(x1161,x1162)+~P10(x1163,x1161,x1164,x1165)
% 59.38/59.39 [117]P10(x1173,x1174,x1172,x1175)+~E(x1171,x1172)+~P10(x1173,x1174,x1171,x1175)
% 59.38/59.39 [118]P10(x1183,x1184,x1185,x1182)+~E(x1181,x1182)+~P10(x1183,x1184,x1185,x1181)
% 59.38/59.39 [119]P7(x1192,x1193,x1194,x1195,x1196,x1197)+~E(x1191,x1192)+~P7(x1191,x1193,x1194,x1195,x1196,x1197)
% 59.38/59.39 [120]P7(x1203,x1202,x1204,x1205,x1206,x1207)+~E(x1201,x1202)+~P7(x1203,x1201,x1204,x1205,x1206,x1207)
% 59.38/59.39 [121]P7(x1213,x1214,x1212,x1215,x1216,x1217)+~E(x1211,x1212)+~P7(x1213,x1214,x1211,x1215,x1216,x1217)
% 59.38/59.39 [122]P7(x1223,x1224,x1225,x1222,x1226,x1227)+~E(x1221,x1222)+~P7(x1223,x1224,x1225,x1221,x1226,x1227)
% 59.38/59.39 [123]P7(x1233,x1234,x1235,x1236,x1232,x1237)+~E(x1231,x1232)+~P7(x1233,x1234,x1235,x1236,x1231,x1237)
% 59.38/59.39 [124]P7(x1243,x1244,x1245,x1246,x1247,x1242)+~E(x1241,x1242)+~P7(x1243,x1244,x1245,x1246,x1247,x1241)
% 59.38/59.39 [125]P8(x1252,x1253,x1254)+~E(x1251,x1252)+~P8(x1251,x1253,x1254)
% 59.38/59.39 [126]P8(x1263,x1262,x1264)+~E(x1261,x1262)+~P8(x1263,x1261,x1264)
% 59.38/59.39 [127]P8(x1273,x1274,x1272)+~E(x1271,x1272)+~P8(x1273,x1274,x1271)
% 59.38/59.39 [128]P5(x1282,x1283,x1284,x1285)+~E(x1281,x1282)+~P5(x1281,x1283,x1284,x1285)
% 59.38/59.39 [129]P5(x1293,x1292,x1294,x1295)+~E(x1291,x1292)+~P5(x1293,x1291,x1294,x1295)
% 59.38/59.39 [130]P5(x1303,x1304,x1302,x1305)+~E(x1301,x1302)+~P5(x1303,x1304,x1301,x1305)
% 59.38/59.39 [131]P5(x1313,x1314,x1315,x1312)+~E(x1311,x1312)+~P5(x1313,x1314,x1315,x1311)
% 59.38/59.39 [132]P11(x1322,x1323,x1324,x1325,x1326,x1327)+~E(x1321,x1322)+~P11(x1321,x1323,x1324,x1325,x1326,x1327)
% 59.38/59.39 [133]P11(x1333,x1332,x1334,x1335,x1336,x1337)+~E(x1331,x1332)+~P11(x1333,x1331,x1334,x1335,x1336,x1337)
% 59.38/59.39 [134]P11(x1343,x1344,x1342,x1345,x1346,x1347)+~E(x1341,x1342)+~P11(x1343,x1344,x1341,x1345,x1346,x1347)
% 59.38/59.39 [135]P11(x1353,x1354,x1355,x1352,x1356,x1357)+~E(x1351,x1352)+~P11(x1353,x1354,x1355,x1351,x1356,x1357)
% 59.38/59.39 [136]P11(x1363,x1364,x1365,x1366,x1362,x1367)+~E(x1361,x1362)+~P11(x1363,x1364,x1365,x1366,x1361,x1367)
% 59.38/59.39 [137]P11(x1373,x1374,x1375,x1376,x1377,x1372)+~E(x1371,x1372)+~P11(x1373,x1374,x1375,x1376,x1377,x1371)
% 59.38/59.39 [138]P6(x1382,x1383,x1384,x1385)+~E(x1381,x1382)+~P6(x1381,x1383,x1384,x1385)
% 59.38/59.39 [139]P6(x1393,x1392,x1394,x1395)+~E(x1391,x1392)+~P6(x1393,x1391,x1394,x1395)
% 59.38/59.39 [140]P6(x1403,x1404,x1402,x1405)+~E(x1401,x1402)+~P6(x1403,x1404,x1401,x1405)
% 59.38/59.39 [141]P6(x1413,x1414,x1415,x1412)+~E(x1411,x1412)+~P6(x1413,x1414,x1415,x1411)
% 59.38/59.40
% 59.38/59.40 %-------------------------------------------
% 59.38/59.40 cnf(271,plain,
% 59.38/59.40 (~P4(a22,a21,a21,a2,a2,a22,a22,a21)),
% 59.38/59.40 inference(scs_inference,[],[155,236,257])).
% 59.38/59.40 cnf(275,plain,
% 59.38/59.40 (~P4(a22,a2,a22,a21,a22,a21,a21,a2)),
% 59.38/59.40 inference(scs_inference,[],[155,236,257,258,259])).
% 59.38/59.40 cnf(277,plain,
% 59.38/59.40 (~P11(a22,a21,a2,a2,a22,a21)),
% 59.38/59.40 inference(scs_inference,[],[155,236,257,258,259,219])).
% 59.38/59.40 cnf(279,plain,
% 59.38/59.40 (~P11(a22,a2,a21,a21,a22,a2)),
% 59.38/59.40 inference(scs_inference,[],[155,236,257,258,259,219,220])).
% 59.38/59.40 cnf(281,plain,
% 59.38/59.40 (~P11(a2,a21,a22,a22,a2,a21)),
% 59.38/59.40 inference(scs_inference,[],[155,236,257,258,259,219,220,221])).
% 59.38/59.40 cnf(283,plain,
% 59.38/59.40 (P1(a15,a15,a1)),
% 59.38/59.40 inference(scs_inference,[],[142,155,236,257,258,259,219,220,221,160])).
% 59.38/59.40 cnf(285,plain,
% 59.38/59.40 (~P3(x2851,x2852,a1,a17)+P10(x2851,x2852,a2,a15)),
% 59.38/59.40 inference(scs_inference,[],[142,150,155,236,257,258,259,219,220,221,160,185])).
% 59.38/59.40 cnf(289,plain,
% 59.38/59.40 (~P3(a2,a15,a17,a1)+P10(a2,a15,a2,a15)),
% 59.38/59.40 inference(scs_inference,[],[142,150,155,236,257,258,259,219,220,221,160,185,246,170,171])).
% 59.38/59.40 cnf(297,plain,
% 59.38/59.40 (~P4(a21,a22,a21,a2,a2,a22,a22,a21)),
% 59.38/59.40 inference(scs_inference,[],[271,277,221,220,259])).
% 59.38/59.40 cnf(299,plain,
% 59.38/59.40 (~P4(a21,a2,a22,a21,a22,a21,a2,a22)),
% 59.38/59.40 inference(scs_inference,[],[271,277,221,220,259,258])).
% 59.38/59.40 cnf(301,plain,
% 59.38/59.40 (~P4(a22,a21,a21,a2,a22,a2,a22,a21)),
% 59.38/59.40 inference(scs_inference,[],[271,275,277,221,220,259,258,257])).
% 59.38/59.40 cnf(303,plain,
% 59.38/59.40 (P1(a16,a16,a18)),
% 59.38/59.40 inference(scs_inference,[],[143,271,275,277,221,220,259,258,257,160])).
% 59.38/59.40 cnf(305,plain,
% 59.38/59.40 (~P4(a21,a22,a2,a22,a21,a2,a22,a21)),
% 59.38/59.40 inference(scs_inference,[],[143,271,275,277,221,220,259,258,257,160,260])).
% 59.38/59.40 cnf(319,plain,
% 59.38/59.40 (~P4(a22,a21,a22,a2,a21,a2,a22,a21)),
% 59.38/59.40 inference(scs_inference,[],[301,260])).
% 59.38/59.40 cnf(323,plain,
% 59.38/59.40 (~P11(a21,a2,a22,a22,a21,a2)),
% 59.38/59.40 inference(scs_inference,[],[301,279,260,221,219])).
% 59.38/59.40 cnf(325,plain,
% 59.38/59.40 (~P11(a21,a2,a22,a2,a22,a21)),
% 59.38/59.40 inference(scs_inference,[],[301,279,281,260,221,219,220])).
% 59.38/59.40 cnf(327,plain,
% 59.38/59.40 (~P4(a2,a22,a22,a21,a21,a22,a21,a2)),
% 59.38/59.40 inference(scs_inference,[],[297,301,279,281,260,221,219,220,257])).
% 59.38/59.40 cnf(329,plain,
% 59.38/59.40 (~P4(a2,a21,a22,a21,a22,a21,a2,a22)),
% 59.38/59.40 inference(scs_inference,[],[299,297,301,279,281,260,221,219,220,257,259])).
% 59.38/59.40 cnf(331,plain,
% 59.38/59.40 (~P4(a21,a2,a21,a22,a22,a21,a2,a22)),
% 59.38/59.40 inference(scs_inference,[],[299,297,301,279,281,260,221,219,220,257,259,258])).
% 59.38/59.40 cnf(333,plain,
% 59.38/59.40 (P1(a1,a1,a19)),
% 59.38/59.40 inference(scs_inference,[],[144,299,297,301,279,281,260,221,219,220,257,259,258,160])).
% 59.38/59.40 cnf(347,plain,
% 59.38/59.40 (~P4(a2,a22,a21,a22,a22,a21,a21,a2)),
% 59.38/59.40 inference(scs_inference,[],[327,260])).
% 59.38/59.40 cnf(353,plain,
% 59.38/59.40 (~P4(a21,a2,a22,a21,a21,a22,a2,a22)),
% 59.38/59.40 inference(scs_inference,[],[305,327,325,260,219,221,257])).
% 59.38/59.40 cnf(355,plain,
% 59.38/59.40 (~P4(a22,a21,a2,a22,a21,a2,a21,a22)),
% 59.38/59.40 inference(scs_inference,[],[305,327,325,260,219,221,257,258])).
% 59.38/59.40 cnf(357,plain,
% 59.38/59.40 (~P4(a21,a22,a22,a2,a21,a2,a22,a21)),
% 59.38/59.40 inference(scs_inference,[],[305,319,327,325,260,219,221,257,258,259])).
% 59.38/59.40 cnf(361,plain,
% 59.38/59.40 (P1(a18,a18,a20)),
% 59.38/59.40 inference(scs_inference,[],[145,305,319,327,323,325,260,219,221,257,258,259,220,160])).
% 59.38/59.40 cnf(367,plain,
% 59.38/59.40 (~P3(x3671,x3672,a18,a17)+P10(x3671,x3672,a2,a16)),
% 59.38/59.40 inference(scs_inference,[],[151,145,154,150,305,319,327,323,325,260,219,221,257,258,259,220,160,111,247,110,185])).
% 59.38/59.40 cnf(375,plain,
% 59.38/59.40 (~P4(a22,a21,a21,a2,a2,a22,a21,a22)),
% 59.38/59.40 inference(scs_inference,[],[355,260])).
% 59.38/59.40 cnf(377,plain,
% 59.38/59.40 (~P4(a22,a2,a21,a22,a22,a21,a21,a2)),
% 59.38/59.40 inference(scs_inference,[],[347,355,260,259])).
% 59.38/59.40 cnf(381,plain,
% 59.38/59.40 (~P4(a22,a21,a2,a22,a2,a21,a22,a21)),
% 59.38/59.40 inference(scs_inference,[],[347,329,355,260,259,258,257])).
% 59.38/59.40 cnf(383,plain,
% 59.38/59.40 (P1(a15,a15,a21)),
% 59.38/59.40 inference(scs_inference,[],[146,347,329,355,260,259,258,257,160])).
% 59.38/59.40 cnf(390,plain,
% 59.38/59.40 (~P4(a21,a22,a21,a2,a22,a2,a22,a21)),
% 59.38/59.40 inference(scs_inference,[],[357,260])).
% 59.38/59.40 cnf(392,plain,
% 59.38/59.40 (~P4(a2,a22,a22,a21,a22,a21,a2,a21)),
% 59.38/59.40 inference(scs_inference,[],[357,381,260,258])).
% 59.38/59.40 cnf(394,plain,
% 59.38/59.40 (~P4(a2,a21,a21,a22,a22,a21,a2,a22)),
% 59.38/59.40 inference(scs_inference,[],[331,357,381,260,258,259])).
% 59.38/59.40 cnf(396,plain,
% 59.38/59.40 (~P4(a21,a2,a22,a21,a21,a22,a22,a2)),
% 59.38/59.40 inference(scs_inference,[],[331,357,381,260,258,259,257])).
% 59.38/59.40 cnf(398,plain,
% 59.38/59.40 (P1(a20,a20,a21)),
% 59.38/59.40 inference(scs_inference,[],[147,331,357,381,260,258,259,257,160])).
% 59.38/59.40 cnf(400,plain,
% 59.38/59.40 (~P5(a2,a22,a2,a21)),
% 59.38/59.40 inference(scs_inference,[],[147,331,357,381,260,258,259,257,160,231])).
% 59.38/59.40 cnf(402,plain,
% 59.38/59.40 (~P8(x4021,a22,a21)+~P3(a2,x4021,a22,a21)),
% 59.38/59.40 inference(scs_inference,[],[147,331,357,381,260,258,259,257,160,231,178])).
% 59.38/59.40 cnf(404,plain,
% 59.38/59.40 (~P8(a2,a22,a21)),
% 59.38/59.40 inference(scs_inference,[],[147,331,357,381,260,258,259,257,160,231,178,161])).
% 59.38/59.40 cnf(406,plain,
% 59.38/59.40 (~P5(a2,a21,a2,a22)),
% 59.38/59.40 inference(scs_inference,[],[147,331,357,381,260,258,259,257,160,231,178,161,172])).
% 59.38/59.40 cnf(408,plain,
% 59.38/59.40 (~P5(a2,a22,a21,a2)),
% 59.38/59.40 inference(scs_inference,[],[147,331,357,381,260,258,259,257,160,231,178,161,172,173])).
% 59.38/59.40 cnf(410,plain,
% 59.38/59.40 (~P7(a2,a22,x4101,a2,a21,x4102)),
% 59.38/59.40 inference(scs_inference,[],[147,331,357,381,260,258,259,257,160,231,178,161,172,173,207])).
% 59.38/59.40 cnf(412,plain,
% 59.38/59.40 (~P8(x4121,a21,a22)+~P3(a2,x4121,a22,a21)),
% 59.38/59.40 inference(scs_inference,[],[147,331,357,381,260,258,259,257,160,231,178,161,172,173,207,159])).
% 59.38/59.40 cnf(421,plain,
% 59.38/59.40 (~P8(a2,a21,a22)),
% 59.38/59.40 inference(scs_inference,[],[404,159])).
% 59.38/59.40 cnf(423,plain,
% 59.38/59.40 (~P7(a22,a2,x4231,a21,a2,x4232)),
% 59.38/59.40 inference(scs_inference,[],[410,404,159,223])).
% 59.38/59.40 cnf(425,plain,
% 59.38/59.40 (~P7(a2,x4251,a22,a2,x4252,a21)),
% 59.38/59.40 inference(scs_inference,[],[410,404,159,223,224])).
% 59.38/59.40 cnf(427,plain,
% 59.38/59.40 (~P7(a2,a21,x4271,a2,a22,x4272)),
% 59.38/59.40 inference(scs_inference,[],[410,404,406,159,223,224,207])).
% 59.38/59.40 cnf(429,plain,
% 59.38/59.40 (~P5(a2,a21,a22,a2)),
% 59.38/59.40 inference(scs_inference,[],[410,404,406,159,223,224,207,173])).
% 59.38/59.40 cnf(433,plain,
% 59.38/59.40 (~P7(a21,a2,x4331,a22,a2,x4332)),
% 59.38/59.40 inference(scs_inference,[],[377,410,404,406,159,223,224,207,173,260,222])).
% 59.38/59.40 cnf(435,plain,
% 59.38/59.40 (~P5(a21,a2,a2,a22)),
% 59.38/59.40 inference(scs_inference,[],[377,410,404,406,408,159,223,224,207,173,260,222,172])).
% 59.38/59.40 cnf(437,plain,
% 59.38/59.40 (~P4(a2,a21,a22,a21,a21,a22,a2,a22)),
% 59.38/59.40 inference(scs_inference,[],[353,377,410,404,406,408,159,223,224,207,173,260,222,172,259])).
% 59.38/59.40 cnf(439,plain,
% 59.38/59.40 (~P4(a22,a21,a21,a2,a22,a2,a21,a22)),
% 59.38/59.40 inference(scs_inference,[],[353,377,410,404,406,408,159,223,224,207,173,260,222,172,259,257])).
% 59.38/59.40 cnf(441,plain,
% 59.38/59.40 (~P4(a21,a2,a21,a22,a22,a21,a22,a2)),
% 59.38/59.40 inference(scs_inference,[],[353,377,390,410,404,406,408,159,223,224,207,173,260,222,172,259,257,258])).
% 59.38/59.40 cnf(443,plain,
% 59.38/59.40 (P1(a16,a16,a22)),
% 59.38/59.40 inference(scs_inference,[],[148,353,377,390,410,404,406,408,159,223,224,207,173,260,222,172,259,257,258,160])).
% 59.38/59.40 cnf(445,plain,
% 59.38/59.40 (~P8(x4451,a21,a22)+~P3(a2,x4451,a21,a22)),
% 59.38/59.40 inference(scs_inference,[],[148,353,377,390,410,404,406,408,159,223,224,207,173,260,222,172,259,257,258,160,178])).
% 59.38/59.40 cnf(447,plain,
% 59.38/59.40 (~P5(x4471,x4472,x4473,x4474)+~P9(a2,a21,a2,a22,x4471,x4472,x4473,x4474)),
% 59.38/59.40 inference(scs_inference,[],[148,353,377,390,410,404,406,408,159,223,224,207,173,260,222,172,259,257,258,160,178,248])).
% 59.38/59.40 cnf(452,plain,
% 59.38/59.40 (~P5(a21,a2,a22,a2)),
% 59.38/59.40 inference(scs_inference,[],[435,173])).
% 59.38/59.40 cnf(454,plain,
% 59.38/59.40 (~P4(a22,a21,a22,a2,a21,a2,a21,a22)),
% 59.38/59.40 inference(scs_inference,[],[439,435,173,260])).
% 59.38/59.40 cnf(456,plain,
% 59.38/59.40 (~P7(a2,x4561,a21,a2,x4562,a22)),
% 59.38/59.40 inference(scs_inference,[],[439,427,435,173,260,224])).
% 59.38/59.40 cnf(458,plain,
% 59.38/59.40 (~P7(a2,a21,x4581,a22,a2,x4582)),
% 59.38/59.40 inference(scs_inference,[],[439,427,429,435,173,260,224,207])).
% 59.38/59.40 cnf(460,plain,
% 59.38/59.40 (~P7(x4601,a2,a22,x4602,a2,a21)),
% 59.38/59.40 inference(scs_inference,[],[439,427,429,435,425,173,260,224,207,223])).
% 59.38/59.40 cnf(462,plain,
% 59.38/59.40 (~P5(a22,a2,a2,a21)),
% 59.38/59.40 inference(scs_inference,[],[439,427,429,435,425,173,260,224,207,223,172])).
% 59.38/59.40 cnf(464,plain,
% 59.38/59.40 (~P4(a21,a22,a2,a21,a2,a22,a22,a21)),
% 59.38/59.40 inference(scs_inference,[],[394,439,427,429,435,425,173,260,224,207,223,172,258])).
% 59.38/59.40 cnf(468,plain,
% 59.38/59.40 (~P4(a22,a2,a22,a21,a22,a21,a2,a21)),
% 59.38/59.40 inference(scs_inference,[],[392,394,439,427,429,435,425,173,260,224,207,223,172,258,257,259])).
% 59.38/59.40 cnf(470,plain,
% 59.38/59.40 (P1(a20,a20,a22)),
% 59.38/59.40 inference(scs_inference,[],[149,392,394,439,427,429,435,425,173,260,224,207,223,172,258,257,259,160])).
% 59.38/59.40 cnf(474,plain,
% 59.38/59.40 (~P5(x4741,x4742,x4743,x4744)+~P9(a2,a21,a22,a2,x4741,x4742,x4743,x4744)),
% 59.38/59.40 inference(scs_inference,[],[149,392,394,439,427,429,435,425,173,260,224,207,223,172,258,257,259,160,222,248])).
% 59.38/59.40 cnf(483,plain,
% 59.38/59.40 (~P5(a22,a2,a21,a2)),
% 59.38/59.40 inference(scs_inference,[],[462,173])).
% 59.38/59.40 cnf(485,plain,
% 59.38/59.40 (~P7(x4851,a2,a21,x4852,a2,a22)),
% 59.38/59.40 inference(scs_inference,[],[462,460,173,222])).
% 59.38/59.40 cnf(489,plain,
% 59.38/59.40 (~P7(a2,x4891,a21,a22,x4892,a2)),
% 59.38/59.40 inference(scs_inference,[],[458,462,460,173,222,223,224])).
% 59.38/59.40 cnf(491,plain,
% 59.38/59.40 (~P7(a2,a22,x4911,a21,a2,x4912)),
% 59.38/59.40 inference(scs_inference,[],[458,462,408,460,173,222,223,224,207])).
% 59.38/59.40 cnf(495,plain,
% 59.38/59.40 (~P4(a22,a21,a2,a21,a2,a22,a21,a22)),
% 59.38/59.40 inference(scs_inference,[],[437,464,458,462,408,460,173,222,223,224,207,260,258])).
% 59.38/59.40 cnf(497,plain,
% 59.38/59.40 (~P4(a2,a22,a22,a21,a21,a22,a2,a21)),
% 59.38/59.40 inference(scs_inference,[],[437,464,458,462,408,460,173,222,223,224,207,260,258,257])).
% 59.38/59.40 cnf(499,plain,
% 59.38/59.40 (~P4(a21,a22,a21,a2,a2,a22,a21,a22)),
% 59.38/59.40 inference(scs_inference,[],[375,437,464,458,462,408,460,173,222,223,224,207,260,258,257,259])).
% 59.38/59.40 cnf(503,plain,
% 59.38/59.40 (~P5(x5031,x5032,x5033,x5034)+~P9(a21,a2,a22,a2,x5031,x5032,x5033,x5034)),
% 59.38/59.40 inference(scs_inference,[],[283,375,437,464,458,452,462,408,460,173,222,223,224,207,260,258,257,259,160,248])).
% 59.38/59.40 cnf(514,plain,
% 59.38/59.40 (~P4(a2,a22,a21,a22,a22,a21,a2,a21)),
% 59.38/59.40 inference(scs_inference,[],[497,260])).
% 59.38/59.40 cnf(516,plain,
% 59.38/59.40 (~P7(x5161,a2,a21,x5162,a22,a2)),
% 59.38/59.40 inference(scs_inference,[],[497,489,260,223])).
% 59.38/59.40 cnf(520,plain,
% 59.38/59.40 (~P7(a2,x5201,a22,a21,x5202,a2)),
% 59.38/59.40 inference(scs_inference,[],[497,491,489,260,223,222,224])).
% 59.38/59.40 cnf(524,plain,
% 59.38/59.40 (~P4(a22,a21,a2,a21,a22,a2,a22,a21)),
% 59.38/59.40 inference(scs_inference,[],[468,497,491,489,260,223,222,224,258,257])).
% 59.38/59.40 cnf(526,plain,
% 59.38/59.40 (~P4(a2,a21,a21,a22,a22,a21,a22,a2)),
% 59.38/59.40 inference(scs_inference,[],[441,468,497,491,489,260,223,222,224,258,257,259])).
% 59.38/59.40 cnf(530,plain,
% 59.38/59.40 (~P5(x5301,x5302,x5303,x5304)+~P9(a21,a2,a2,a22,x5301,x5302,x5303,x5304)),
% 59.38/59.40 inference(scs_inference,[],[441,468,303,497,435,491,489,260,223,222,224,258,257,259,160,248])).
% 59.38/59.40 cnf(547,plain,
% 59.38/59.40 (~P7(x5471,a22,a2,x5472,a2,a21)),
% 59.38/59.40 inference(scs_inference,[],[499,516,260,222])).
% 59.38/59.40 cnf(549,plain,
% 59.38/59.40 (~P7(a22,x5491,a2,a21,x5492,a2)),
% 59.38/59.40 inference(scs_inference,[],[499,423,516,260,222,224])).
% 59.38/59.40 cnf(551,plain,
% 59.38/59.40 (~P7(x5511,a2,a22,x5512,a21,a2)),
% 59.38/59.40 inference(scs_inference,[],[499,423,516,520,260,222,224,223])).
% 59.38/59.40 cnf(557,plain,
% 59.38/59.40 (~P4(a2,a21,a22,a21,a21,a22,a22,a2)),
% 59.38/59.40 inference(scs_inference,[],[396,499,423,516,520,260,222,224,223,258,257,259])).
% 59.38/59.40 cnf(561,plain,
% 59.38/59.40 (~P5(x5611,x5612,x5613,x5614)+~P9(a22,a2,a2,a21,x5611,x5612,x5613,x5614)),
% 59.38/59.40 inference(scs_inference,[],[396,333,499,462,423,516,520,260,222,224,223,258,257,259,160,248])).
% 59.38/59.40 cnf(577,plain,
% 59.38/59.40 (~P7(x5771,a22,a2,x5772,a21,a2)),
% 59.38/59.40 inference(scs_inference,[],[549,223])).
% 59.38/59.40 cnf(579,plain,
% 59.38/59.40 (~P7(a21,x5791,a2,a22,x5792,a2)),
% 59.38/59.40 inference(scs_inference,[],[433,549,223,224])).
% 59.38/59.40 cnf(581,plain,
% 59.38/59.40 (~P7(x5811,a21,a2,x5812,a2,a22)),
% 59.38/59.40 inference(scs_inference,[],[433,549,551,223,224,222])).
% 59.38/59.40 cnf(583,plain,
% 59.38/59.40 (~P4(a2,a21,a22,a21,a22,a21,a22,a2)),
% 59.38/59.40 inference(scs_inference,[],[524,433,549,551,223,224,222,258])).
% 59.38/59.41 cnf(585,plain,
% 59.38/59.41 (~P4(a22,a21,a22,a2,a2,a21,a21,a22)),
% 59.38/59.41 inference(scs_inference,[],[524,526,433,549,551,223,224,222,258,257])).
% 59.38/59.41 cnf(587,plain,
% 59.38/59.41 (~P4(a21,a22,a22,a2,a21,a2,a21,a22)),
% 59.38/59.41 inference(scs_inference,[],[454,524,526,433,549,551,223,224,222,258,257,259])).
% 59.38/59.41 cnf(591,plain,
% 59.38/59.41 (~P4(a22,a21,a2,a21,a22,a2,a21,a22)),
% 59.38/59.41 inference(scs_inference,[],[454,361,524,526,433,549,551,223,224,222,258,257,259,160,260])).
% 59.38/59.41 cnf(593,plain,
% 59.38/59.41 (~P5(x5931,x5932,x5933,x5934)+~P9(a2,a22,a21,a2,x5931,x5932,x5933,x5934)),
% 59.38/59.41 inference(scs_inference,[],[454,361,524,526,408,433,549,551,223,224,222,258,257,259,160,260,248])).
% 59.38/59.41 cnf(608,plain,
% 59.38/59.41 (~P4(a21,a22,a21,a2,a22,a2,a21,a22)),
% 59.38/59.41 inference(scs_inference,[],[587,260])).
% 59.38/59.41 cnf(614,plain,
% 59.38/59.41 (~P4(a21,a22,a22,a2,a2,a21,a22,a21)),
% 59.38/59.41 inference(scs_inference,[],[557,587,579,520,260,223,222,257])).
% 59.38/59.41 cnf(620,plain,
% 59.38/59.41 (P1(a21,a21,a15)),
% 59.38/59.41 inference(scs_inference,[],[514,383,557,585,587,579,520,260,223,222,257,258,259,160])).
% 59.38/59.41 cnf(636,plain,
% 59.38/59.41 (~P4(a21,a22,a2,a21,a2,a22,a21,a22)),
% 59.38/59.41 inference(scs_inference,[],[495,608,614,260,258,257,259])).
% 59.38/59.41 cnf(638,plain,
% 59.38/59.41 (P1(a21,a21,a20)),
% 59.38/59.41 inference(scs_inference,[],[495,398,608,614,260,258,257,259,160])).
% 59.38/59.41 cnf(640,plain,
% 59.38/59.41 (~P5(a2,x6401,a2,x6402)+~P11(a2,x6401,a21,a2,x6402,a22)),
% 59.38/59.41 inference(scs_inference,[],[495,398,608,614,456,260,258,257,259,160,225])).
% 59.38/59.41 cnf(642,plain,
% 59.38/59.41 (~P5(a2,x6421,x6422,a2)+~P11(a2,x6421,a21,a2,x6422,a22)),
% 59.38/59.41 inference(scs_inference,[],[495,398,608,614,456,260,258,257,259,160,225,173])).
% 59.38/59.41 cnf(644,plain,
% 59.38/59.41 (~P8(a2,x6441,x6442)+~P11(a2,x6441,a21,a2,x6442,a22)),
% 59.38/59.41 inference(scs_inference,[],[495,398,608,614,456,260,258,257,259,160,225,173,161])).
% 59.38/59.41 cnf(648,plain,
% 59.38/59.41 (~P5(a2,x6481,a2,x6482)+~P11(a2,x6482,a21,a2,x6481,a22)),
% 59.38/59.41 inference(scs_inference,[],[495,398,608,614,456,260,258,257,259,160,225,173,161,207,172])).
% 59.38/59.41 cnf(650,plain,
% 59.38/59.41 (~P8(a2,x6501,x6502)+~P11(a2,x6502,a21,a2,x6501,a22)),
% 59.38/59.41 inference(scs_inference,[],[495,398,608,614,456,260,258,257,259,160,225,173,161,207,172,159])).
% 59.38/59.41 cnf(670,plain,
% 59.38/59.41 (~P5(x6701,x6702,x6703,x6704)+~P9(a22,a2,a21,a2,x6701,x6702,x6703,x6704)),
% 59.38/59.41 inference(scs_inference,[],[144,443,583,636,483,260,257,258,259,160,88,248])).
% 59.38/59.41 cnf(672,plain,
% 59.38/59.41 (~P5(x6721,a2,x6722,a2)+~P11(x6721,a2,a21,x6722,a2,a22)),
% 59.38/59.41 inference(scs_inference,[],[144,443,583,636,483,485,260,257,258,259,160,88,248,225])).
% 59.38/59.41 cnf(680,plain,
% 59.38/59.41 (P1(a22,a22,a20)),
% 59.38/59.41 inference(scs_inference,[],[470,591,259,160])).
% 59.38/59.41 cnf(688,plain,
% 59.38/59.41 (~P5(x6881,x6882,x6883,x6884)+~P9(a2,a22,a2,a21,x6881,x6882,x6883,x6884)),
% 59.38/59.41 inference(scs_inference,[],[470,591,400,259,160,260,258,257,248])).
% 59.38/59.41 cnf(742,plain,
% 59.38/59.41 (~P5(x7421,a22,x7422,a2)+~P11(x7421,a22,a2,x7422,a2,a21)),
% 59.38/59.41 inference(scs_inference,[],[152,147,547,88,110,225])).
% 59.38/59.41 cnf(761,plain,
% 59.38/59.41 (~P8(x7611,a22,a21)+~P11(x7611,a22,a2,x7611,a21,a2)),
% 59.38/59.41 inference(scs_inference,[],[577,225,173,161])).
% 59.38/59.41 cnf(767,plain,
% 59.38/59.41 (~P8(x7671,a21,a22)+~P11(x7671,a22,a2,x7671,a21,a2)),
% 59.38/59.41 inference(scs_inference,[],[577,225,173,161,207,172,159])).
% 59.38/59.41 cnf(780,plain,
% 59.38/59.41 (~P8(x7801,a21,a2)+~P11(x7801,a21,a2,x7801,a2,a22)),
% 59.38/59.41 inference(scs_inference,[],[581,225,173,161])).
% 59.38/59.41 cnf(782,plain,
% 59.38/59.41 (~P8(x7821,a2,a21)+~P11(x7821,a21,a2,x7821,a2,a22)),
% 59.38/59.41 inference(scs_inference,[],[581,225,173,161,159])).
% 59.38/59.41 cnf(797,plain,
% 59.38/59.41 (~P5(a2,x7971,a2,x7972)+~P11(a2,x7971,a22,a2,x7972,a21)),
% 59.38/59.41 inference(scs_inference,[],[149,425,88,90,225])).
% 59.38/59.41 cnf(809,plain,
% 59.38/59.41 (~P5(x8091,a2,a2,x8092)+~P11(x8091,a2,a22,x8092,a2,a21)),
% 59.38/59.41 inference(scs_inference,[],[460,225,173])).
% 59.38/59.41 cnf(811,plain,
% 59.38/59.41 (~P5(x8111,a2,x8112,a2)+~P11(x8112,a2,a22,x8111,a2,a21)),
% 59.38/59.41 inference(scs_inference,[],[460,225,173,172])).
% 59.38/59.41 cnf(815,plain,
% 59.38/59.41 (~P8(x8151,a2,a2)+~P11(x8151,a2,a22,x8151,a2,a21)),
% 59.38/59.41 inference(scs_inference,[],[460,225,173,172,207,161])).
% 59.38/59.41 cnf(826,plain,
% 59.38/59.41 (~P8(x8261,a2,a22)+~P11(x8261,a2,a21,x8261,a22,a2)),
% 59.38/59.41 inference(scs_inference,[],[516,225,173,161])).
% 59.38/59.41 cnf(855,plain,
% 59.38/59.41 (~P5(x8551,a2,x8552,a21)+~P11(x8551,a2,a22,x8552,a21,a2)),
% 59.38/59.41 inference(scs_inference,[],[144,551,89,225])).
% 59.38/59.41 cnf(1510,plain,
% 59.38/59.41 (P1(x15101,x15102,x15103)+~P10(x15101,x15103,x15101,x15102)),
% 59.38/59.41 inference(scs_inference,[],[165,157])).
% 59.38/59.41 cnf(1558,plain,
% 59.38/59.41 (~P8(x15581,a22,a21)+~P3(a2,x15581,a21,a22)),
% 59.38/59.41 inference(scs_inference,[],[445,159])).
% 59.38/59.41 cnf(1590,plain,
% 59.38/59.41 (P1(x15901,x15902,x15903)+~P10(x15901,x15903,x15902,x15901)),
% 59.38/59.41 inference(scs_inference,[],[1510,169])).
% 59.38/59.41 cnf(1638,plain,
% 59.38/59.41 (P1(x16381,x16382,x16383)+~P10(x16382,x16381,x16381,x16383)),
% 59.38/59.41 inference(scs_inference,[],[1590,168])).
% 59.38/59.41 cnf(1670,plain,
% 59.38/59.41 (~P4(x16701,x16702,x16703,x16704,x16702,x16705,x16703,x16704)+P1(x16702,x16701,x16705)),
% 59.38/59.41 inference(scs_inference,[],[1638,238])).
% 59.38/59.41 cnf(1703,plain,
% 59.38/59.41 (P6(x17031,x17032,x17033,x17034)+~P6(x17033,x17031,x17032,x17034)),
% 59.38/59.41 inference(scs_inference,[],[174,175])).
% 59.38/59.41 cnf(1751,plain,
% 59.38/59.41 (P1(a2,a15,a15)+~P3(a2,a15,a17,a1)),
% 59.38/59.41 inference(scs_inference,[],[289,165])).
% 59.38/59.41 cnf(1767,plain,
% 59.38/59.41 (P1(a15,a2,a15)+~P3(a2,a15,a17,a1)),
% 59.38/59.41 inference(scs_inference,[],[1751,156])).
% 59.38/59.41 cnf(1783,plain,
% 59.38/59.41 (P1(a15,a15,a2)+~P3(a2,a15,a17,a1)),
% 59.38/59.41 inference(scs_inference,[],[1767,157])).
% 59.38/59.41 cnf(1799,plain,
% 59.38/59.41 (P1(a2,a2,a15)+~P3(a2,a15,a17,a1)),
% 59.38/59.41 inference(scs_inference,[],[1783,160])).
% 59.38/59.41 cnf(1815,plain,
% 59.38/59.41 (P1(a2,a15,a2)+~P3(a2,a15,a17,a1)),
% 59.38/59.41 inference(scs_inference,[],[1799,157])).
% 59.38/59.41 cnf(1831,plain,
% 59.38/59.41 (P1(a15,a2,a2)+~P3(a2,a15,a17,a1)),
% 59.38/59.41 inference(scs_inference,[],[1815,156])).
% 59.38/59.41 cnf(1847,plain,
% 59.38/59.41 (~P10(a2,a2,a2,a2)+P9(a15,a2,a2,a2,a15,a2,a2,a2)+~P3(a2,a15,a17,a1)),
% 59.38/59.41 inference(scs_inference,[],[1831,233])).
% 59.38/59.41 cnf(1863,plain,
% 59.38/59.41 (P10(a2,a16,x18631,x18632)+~P3(x18631,x18632,a18,a17)),
% 59.38/59.41 inference(scs_inference,[],[367,168])).
% 59.38/59.41 cnf(1911,plain,
% 59.38/59.41 (P6(x19111,x19112,x19113,x19114)+~P6(x19113,x19112,x19111,x19114)),
% 59.38/59.41 inference(scs_inference,[],[1703,175])).
% 59.38/59.41 cnf(1927,plain,
% 59.38/59.41 (P10(a2,a16,a2,a16)),
% 59.38/59.41 inference(scs_inference,[],[151,1863,170])).
% 59.38/59.41 cnf(1928,plain,
% 59.38/59.41 (P1(a2,a16,a16)),
% 59.38/59.41 inference(scs_inference,[],[1927,1510])).
% 59.38/59.41 cnf(1930,plain,
% 59.38/59.41 (P1(a16,a16,a2)),
% 59.38/59.41 inference(scs_inference,[],[1927,1510,160])).
% 59.38/59.41 cnf(1950,plain,
% 59.38/59.41 (P1(a2,a2,a16)),
% 59.38/59.41 inference(scs_inference,[],[1930,160])).
% 59.38/59.41 cnf(1975,plain,
% 59.38/59.41 (P9(a2,a2,a2,a2,a2,a16,a16,a16)+~P1(a2,a2,a2)),
% 59.38/59.41 inference(scs_inference,[],[1930,1928,1927,89,88,90,233])).
% 59.38/59.41 cnf(1977,plain,
% 59.38/59.41 (~P8(x19771,a2,a2)+P8(x19771,a16,a16)),
% 59.38/59.41 inference(scs_inference,[],[1930,1928,1927,89,88,90,233,180])).
% 59.38/59.41 cnf(2001,plain,
% 59.38/59.41 (P5(x20011,a16,x20011,a16)+~P8(x20011,a2,a2)),
% 59.38/59.41 inference(scs_inference,[],[1977,161])).
% 59.38/59.41 cnf(2017,plain,
% 59.38/59.41 (P4(x20171,a16,a16,a16,a16,a16,x20171,a16)+~P8(x20171,a2,a2)),
% 59.38/59.41 inference(scs_inference,[],[2001,231])).
% 59.38/59.41 cnf(2065,plain,
% 59.38/59.41 (P6(x20651,x20652,x20653,x20654)+~P6(x20652,x20653,x20651,x20654)),
% 59.38/59.41 inference(scs_inference,[],[1911,174])).
% 59.38/59.41 cnf(2144,plain,
% 59.38/59.41 (P6(x21441,x21442,x21443,x21444)+~P6(x21442,x21443,x21444,x21441)),
% 59.38/59.41 inference(scs_inference,[],[2065,176])).
% 59.38/59.41 cnf(2208,plain,
% 59.38/59.41 (P6(x22081,x22082,x22083,x22084)+~P6(x22083,x22082,x22084,x22081)),
% 59.38/59.41 inference(scs_inference,[],[2144,174])).
% 59.38/59.41 cnf(2240,plain,
% 59.38/59.41 (P6(x22401,x22402,x22403,x22404)+~P6(x22403,x22404,x22402,x22401)),
% 59.38/59.41 inference(scs_inference,[],[2208,175])).
% 59.38/59.41 cnf(2272,plain,
% 59.38/59.41 (~P6(x22721,x22722,x22723,x22724)+P6(x22724,x22721,x22723,x22722)),
% 59.38/59.41 inference(scs_inference,[],[2240,1911])).
% 59.38/59.41 cnf(2400,plain,
% 59.38/59.41 (~P11(x24001,a21,a2,x24001,a22,a2)+~P8(x24001,a22,a21)),
% 59.38/59.41 inference(scs_inference,[],[761,219])).
% 59.38/59.41 cnf(2416,plain,
% 59.38/59.41 (~P11(a22,x24161,a2,a21,x24161,a2)+~P8(x24161,a21,a22)),
% 59.38/59.41 inference(scs_inference,[],[767,220])).
% 59.38/59.41 cnf(2432,plain,
% 59.38/59.41 (~P11(x24321,a2,a21,x24321,a22,a2)+~P8(x24321,a21,a2)),
% 59.38/59.41 inference(scs_inference,[],[780,221])).
% 59.38/59.41 cnf(2448,plain,
% 59.38/59.41 (~P11(x24481,a2,a22,x24481,a21,a2)+~P8(x24481,a2,a21)),
% 59.38/59.41 inference(scs_inference,[],[782,219])).
% 59.38/59.41 cnf(2464,plain,
% 59.38/59.41 (~P11(a2,x24641,a22,a2,x24641,a21)+~P8(x24641,a2,a2)),
% 59.38/59.41 inference(scs_inference,[],[815,220])).
% 59.38/59.41 cnf(2480,plain,
% 59.38/59.41 (~P11(x24801,a21,a2,x24801,a2,a22)+~P8(x24801,a2,a22)),
% 59.38/59.41 inference(scs_inference,[],[826,221])).
% 59.38/59.41 cnf(2528,plain,
% 59.38/59.41 (~P8(x25281,a21,a22)+~P11(x25281,a21,a2,x25281,a22,a2)),
% 59.38/59.41 inference(scs_inference,[],[2400,159])).
% 59.38/59.41 cnf(2544,plain,
% 59.38/59.41 (~P8(x25441,a22,a21)+~P11(a22,x25441,a2,a21,x25441,a2)),
% 59.38/59.41 inference(scs_inference,[],[2416,159])).
% 59.38/59.41 cnf(2560,plain,
% 59.38/59.41 (~P8(x25601,a2,a21)+~P11(x25601,a2,a21,x25601,a22,a2)),
% 59.38/59.41 inference(scs_inference,[],[2432,159])).
% 59.38/59.41 cnf(2576,plain,
% 59.38/59.41 (~P8(x25761,a21,a2)+~P11(x25761,a2,a22,x25761,a21,a2)),
% 59.38/59.41 inference(scs_inference,[],[2448,159])).
% 59.38/59.41 cnf(2592,plain,
% 59.38/59.41 (~P8(x25921,x25922,x25923)+~P10(x25922,a2,x25923,a2)+~P11(a2,x25921,a22,a2,x25921,a21)),
% 59.38/59.41 inference(scs_inference,[],[2464,180])).
% 59.38/59.41 cnf(2608,plain,
% 59.38/59.41 (~P8(x26081,a22,a2)+~P11(x26081,a21,a2,x26081,a2,a22)),
% 59.38/59.41 inference(scs_inference,[],[2480,159])).
% 59.38/59.41 cnf(2656,plain,
% 59.38/59.41 (~P11(a21,x26561,a2,a22,x26561,a2)+~P8(x26561,a21,a22)),
% 59.38/59.41 inference(scs_inference,[],[2528,220])).
% 59.38/59.41 cnf(2672,plain,
% 59.38/59.41 (~P11(a22,a2,x26721,a21,a2,x26721)+~P8(x26721,a22,a21)),
% 59.38/59.41 inference(scs_inference,[],[2544,221])).
% 59.38/59.41 cnf(2688,plain,
% 59.38/59.41 (~P11(x26881,a22,a2,x26881,a2,a21)+~P8(x26881,a2,a21)),
% 59.38/59.41 inference(scs_inference,[],[2560,219])).
% 59.38/59.41 cnf(2704,plain,
% 59.38/59.41 (~P11(a2,x27041,a22,a21,x27041,a2)+~P8(x27041,a21,a2)),
% 59.38/59.41 inference(scs_inference,[],[2576,220])).
% 59.38/59.41 cnf(2720,plain,
% 59.38/59.41 (~P11(x27201,a2,a21,x27201,a22,a2)+~P8(x27201,a22,a2)),
% 59.38/59.41 inference(scs_inference,[],[2608,221])).
% 59.38/59.41 cnf(2752,plain,
% 59.38/59.41 (~P8(x27521,a22,a21)+~P11(a21,x27521,a2,a22,x27521,a2)),
% 59.38/59.41 inference(scs_inference,[],[2656,159])).
% 59.38/59.41 cnf(2768,plain,
% 59.38/59.41 (~P8(x27681,a21,a22)+~P11(a22,a2,x27681,a21,a2,x27681)),
% 59.38/59.41 inference(scs_inference,[],[2672,159])).
% 59.38/59.41 cnf(2784,plain,
% 59.38/59.41 (~P8(x27841,a21,a2)+~P11(x27841,a22,a2,x27841,a2,a21)),
% 59.38/59.41 inference(scs_inference,[],[2688,159])).
% 59.38/59.41 cnf(2800,plain,
% 59.38/59.41 (~P8(x28001,a2,a21)+~P11(a2,x28001,a22,a21,x28001,a2)),
% 59.38/59.41 inference(scs_inference,[],[2704,159])).
% 59.38/59.41 cnf(2816,plain,
% 59.38/59.41 (~P8(x28161,a22,a22)+~P8(x28162,a22,a20)+~P11(f26(a22,a2),a2,a21,f26(a22,a2),a22,a2)),
% 59.38/59.41 inference(scs_inference,[],[680,2720,164])).
% 59.38/59.41 cnf(2848,plain,
% 59.38/59.41 (~P11(a21,a2,x28481,a22,a2,x28481)+~P8(x28481,a22,a21)),
% 59.38/59.41 inference(scs_inference,[],[2752,221])).
% 59.38/59.41 cnf(2864,plain,
% 59.38/59.41 (~P11(a21,a2,x28641,a22,a2,x28641)+~P8(x28641,a21,a22)),
% 59.38/59.41 inference(scs_inference,[],[2768,219])).
% 59.38/59.41 cnf(2880,plain,
% 59.38/59.41 (~P11(a22,x28801,a2,a2,x28801,a21)+~P8(x28801,a21,a2)),
% 59.38/59.41 inference(scs_inference,[],[2784,220])).
% 59.38/59.41 cnf(2896,plain,
% 59.38/59.41 (~P11(a21,x28961,a2,a2,x28961,a22)+~P8(x28961,a2,a21)),
% 59.38/59.41 inference(scs_inference,[],[2800,219])).
% 59.38/59.41 cnf(2928,plain,
% 59.38/59.41 (~P8(x29281,a22,a22)+~P8(x29282,a22,a20)+~P11(a21,a2,f26(a22,a21),a22,a2,f26(a22,a21))),
% 59.38/59.41 inference(scs_inference,[],[680,2848,164])).
% 59.38/59.41 cnf(2944,plain,
% 59.38/59.41 (~P8(x29441,a21,a21)+~P8(x29442,a21,a20)+~P11(a21,a2,f26(a21,a22),a22,a2,f26(a21,a22))),
% 59.38/59.41 inference(scs_inference,[],[638,2864,164])).
% 59.38/59.41 cnf(2960,plain,
% 59.38/59.41 (~P8(x29601,a2,a21)+~P11(a22,x29601,a2,a2,x29601,a21)),
% 59.38/59.41 inference(scs_inference,[],[2880,159])).
% 59.38/59.41 cnf(2976,plain,
% 59.38/59.41 (~P8(x29761,a21,a2)+~P11(a21,x29761,a2,a2,x29761,a22)),
% 59.38/59.41 inference(scs_inference,[],[2896,159])).
% 59.38/59.41 cnf(3008,plain,
% 59.38/59.41 (~P11(a22,a2,x30081,a2,a21,x30081)+~P8(x30081,a2,a21)),
% 59.38/59.41 inference(scs_inference,[],[2960,221])).
% 59.38/59.41 cnf(3024,plain,
% 59.38/59.41 (~P11(a21,a2,x30241,a2,a22,x30241)+~P8(x30241,a21,a2)),
% 59.38/59.41 inference(scs_inference,[],[2976,221])).
% 59.38/59.41 cnf(3056,plain,
% 59.38/59.41 (~P8(x30561,a21,a2)+~P11(a22,a2,x30561,a2,a21,x30561)),
% 59.38/59.41 inference(scs_inference,[],[3008,159])).
% 59.38/59.41 cnf(3072,plain,
% 59.38/59.41 (~P8(x30721,a2,a21)+~P11(a21,a2,x30721,a2,a22,x30721)),
% 59.38/59.41 inference(scs_inference,[],[3024,159])).
% 59.38/59.41 cnf(3104,plain,
% 59.38/59.41 (~P11(a2,a22,x31041,a21,a2,x31041)+~P8(x31041,a21,a2)),
% 59.38/59.41 inference(scs_inference,[],[3056,220])).
% 59.38/59.41 cnf(3120,plain,
% 59.38/59.41 (~P11(a2,a22,x31201,a21,a2,x31201)+~P8(x31201,a2,a21)),
% 59.38/59.41 inference(scs_inference,[],[3072,219])).
% 59.38/59.41 cnf(3152,plain,
% 59.38/59.41 (~P8(x31521,a21,a21)+~P8(x31522,a21,a15)+~P11(a2,a22,f26(a21,a2),a21,a2,f26(a21,a2))),
% 59.38/59.41 inference(scs_inference,[],[620,3104,164])).
% 59.38/59.41 cnf(3168,plain,
% 59.38/59.41 (~P8(x31681,a1,a1)+~P8(x31682,a2,a15)+~P11(a2,a22,f26(a2,a21),a21,a2,f26(a2,a21))),
% 59.38/59.41 inference(scs_inference,[],[142,3120,164])).
% 59.38/59.41 cnf(3456,plain,
% 59.38/59.41 (~P5(x34561,a2,a2,x34562)+~P11(a2,x34562,a21,a2,x34561,a22)),
% 59.38/59.41 inference(scs_inference,[],[642,172])).
% 59.38/59.41 cnf(3488,plain,
% 59.38/59.41 (~P8(x34881,a2,a2)+~P11(x34881,a2,a21,x34881,a2,a22)),
% 59.38/59.41 inference(scs_inference,[],[672,161])).
% 59.38/59.41 cnf(3489,plain,
% 59.38/59.41 (P1(a2,a1,a15)),
% 59.38/59.41 inference(scs_inference,[],[142,156])).
% 59.38/59.41 cnf(3491,plain,
% 59.38/59.41 (P1(a1,a15,a2)),
% 59.38/59.41 inference(scs_inference,[],[142,156,157])).
% 59.38/59.41 cnf(3497,plain,
% 59.38/59.41 (P3(a1,a17,a15,a2)),
% 59.38/59.41 inference(scs_inference,[],[142,150,153,1927,156,157,169,192,171])).
% 59.38/59.41 cnf(3499,plain,
% 59.38/59.41 (P3(a2,a15,a1,a17)),
% 59.38/59.41 inference(scs_inference,[],[142,150,153,1927,156,157,169,192,171,170])).
% 59.38/59.41 cnf(3501,plain,
% 59.38/59.41 (P4(a2,a16,x35011,x35012,a2,a16,x35011,x35012)),
% 59.38/59.41 inference(scs_inference,[],[142,150,153,1927,156,157,169,192,171,170,230])).
% 59.38/59.41 cnf(3503,plain,
% 59.38/59.41 (P4(x35031,x35032,a2,a16,x35031,x35032,a2,a16)),
% 59.38/59.41 inference(scs_inference,[],[142,150,153,1927,156,157,169,192,171,170,230,258])).
% 59.38/59.41 cnf(3505,plain,
% 59.38/59.41 (P4(a16,a2,x35051,x35052,a2,a16,x35051,x35052)),
% 59.38/59.41 inference(scs_inference,[],[142,150,153,1927,156,157,169,192,171,170,230,258,259])).
% 59.38/59.41 cnf(3507,plain,
% 59.38/59.41 (P6(a16,a16,a2,a2)),
% 59.38/59.41 inference(scs_inference,[],[142,1950,150,153,1927,156,157,169,192,171,170,230,258,259,241])).
% 59.38/59.41 cnf(3509,plain,
% 59.38/59.41 (P10(a16,a2,a2,a16)),
% 59.38/59.41 inference(scs_inference,[],[142,1950,150,153,1927,156,157,169,192,171,170,230,258,259,241,168])).
% 59.38/59.41 cnf(3511,plain,
% 59.38/59.41 (P6(a16,a2,a16,a2)),
% 59.38/59.41 inference(scs_inference,[],[142,1950,150,153,1927,156,157,169,192,171,170,230,258,259,241,168,175])).
% 59.38/59.41 cnf(3513,plain,
% 59.38/59.41 (P6(a16,a2,a2,a16)),
% 59.38/59.41 inference(scs_inference,[],[142,1950,150,153,1927,156,157,169,192,171,170,230,258,259,241,168,175,176])).
% 59.38/59.41 cnf(3515,plain,
% 59.38/59.41 (P6(a2,a16,a2,a16)),
% 59.38/59.41 inference(scs_inference,[],[142,1950,150,153,1927,156,157,169,192,171,170,230,258,259,241,168,175,176,2272])).
% 59.38/59.41 cnf(3517,plain,
% 59.38/59.41 (P10(a2,a15,a2,a15)),
% 59.38/59.41 inference(scs_inference,[],[142,1950,150,153,1927,156,157,169,192,171,170,230,258,259,241,168,175,176,2272,285])).
% 59.38/59.41 cnf(3523,plain,
% 59.38/59.41 (P4(a16,a16,a16,a2,a2,a16,a2,a2)),
% 59.38/59.41 inference(scs_inference,[],[142,1950,150,153,1927,156,157,169,192,171,170,230,258,259,241,168,175,176,2272,285,257,260,229])).
% 59.38/59.41 cnf(3526,plain,
% 59.38/59.41 (P4(a16,a16,a2,a16,a2,a16,a2,a2)),
% 59.38/59.41 inference(scs_inference,[],[142,483,1950,150,153,1927,156,157,169,192,171,170,230,258,259,241,168,175,176,2272,285,257,260,229,128,235])).
% 59.38/59.41 cnf(3528,plain,
% 59.38/59.41 (P10(a1,a17,a1,a17)),
% 59.38/59.41 inference(scs_inference,[],[142,483,1950,150,153,1927,156,157,169,192,171,170,230,258,259,241,168,175,176,2272,285,257,260,229,128,235,185])).
% 59.38/59.41 cnf(3530,plain,
% 59.38/59.41 (P1(a2,a15,a15)),
% 59.38/59.41 inference(scs_inference,[],[142,483,1950,150,153,1927,156,157,169,192,171,170,230,258,259,241,168,175,176,2272,285,257,260,229,128,235,185,165])).
% 59.38/59.41 cnf(3532,plain,
% 59.38/59.41 (P6(a2,a16,a16,a2)),
% 59.38/59.41 inference(scs_inference,[],[142,483,1950,150,153,1927,156,157,169,192,171,170,230,258,259,241,168,175,176,2272,285,257,260,229,128,235,185,165,174])).
% 59.38/59.41 cnf(3534,plain,
% 59.38/59.41 (P1(a16,a2,a2)),
% 59.38/59.41 inference(scs_inference,[],[142,483,1950,150,153,1927,156,157,169,192,171,170,230,258,259,241,168,175,176,2272,285,257,260,229,128,235,185,165,174,1670])).
% 59.38/59.41 cnf(3539,plain,
% 59.38/59.41 (P3(a2,a15,a17,a1)),
% 59.38/59.41 inference(scs_inference,[],[3499,171])).
% 59.38/59.41 cnf(3541,plain,
% 59.38/59.41 (P1(x35411,x35411,x35411)),
% 59.38/59.41 inference(scs_inference,[],[3503,3499,171,1670])).
% 59.38/59.41 cnf(3542,plain,
% 59.38/59.41 (P4(x35421,x35422,a2,a16,x35421,x35422,a2,a16)),
% 59.38/59.41 inference(rename_variables,[],[3503])).
% 59.38/59.41 cnf(3546,plain,
% 59.38/59.41 (P1(a2,a15,a1)),
% 59.38/59.41 inference(scs_inference,[],[3489,3503,3499,3528,171,1670,165,157])).
% 59.38/59.41 cnf(3548,plain,
% 59.38/59.41 (P4(a2,a16,x35481,x35482,a16,a2,x35481,x35482)),
% 59.38/59.41 inference(scs_inference,[],[3489,3503,3505,3499,3528,171,1670,165,157,257])).
% 59.38/59.41 cnf(3550,plain,
% 59.38/59.41 (P1(a15,a2,a15)),
% 59.38/59.41 inference(scs_inference,[],[3489,3530,3503,3505,3499,3528,171,1670,165,157,257,156])).
% 59.38/59.41 cnf(3554,plain,
% 59.38/59.41 (P6(a2,a2,a16,a16)),
% 59.38/59.41 inference(scs_inference,[],[3489,3530,3503,3505,3499,3515,3528,152,171,1670,165,157,257,156,192,175])).
% 59.38/59.41 cnf(3556,plain,
% 59.38/59.41 (P3(a15,a2,a1,a17)),
% 59.38/59.41 inference(scs_inference,[],[3489,3530,3503,3505,3497,3499,3515,3528,152,171,1670,165,157,257,156,192,175,170])).
% 59.38/59.41 cnf(3558,plain,
% 59.38/59.41 (P4(a2,a15,x35581,x35582,a2,a15,x35581,x35582)),
% 59.38/59.41 inference(scs_inference,[],[3517,3489,3530,3503,3505,3497,3499,3515,3528,152,171,1670,165,157,257,156,192,175,170,230])).
% 59.38/59.41 cnf(3560,plain,
% 59.38/59.41 (P10(a2,a15,a15,a2)),
% 59.38/59.41 inference(scs_inference,[],[3517,3489,3530,3503,3505,3497,3499,3515,3528,152,171,1670,165,157,257,156,192,175,170,230,169])).
% 59.38/59.41 cnf(3562,plain,
% 59.38/59.41 (P10(x35621,x35622,x35621,x35622)),
% 59.38/59.41 inference(scs_inference,[],[3517,3489,3530,3503,3542,3505,3497,3499,3515,3528,152,171,1670,165,157,257,156,192,175,170,230,169,238])).
% 59.38/59.41 cnf(3564,plain,
% 59.38/59.41 (P4(a2,a16,a2,a16,x35641,x35642,x35641,x35642)),
% 59.38/59.41 inference(scs_inference,[],[3517,3489,3530,3501,3503,3542,3505,3497,3499,3515,3528,152,171,1670,165,157,257,156,192,175,170,230,169,238,260])).
% 59.38/59.41 cnf(3566,plain,
% 59.38/59.41 (P4(a2,a16,a2,a2,a16,a16,a16,a2)),
% 59.38/59.41 inference(scs_inference,[],[3517,3489,3530,3501,3503,3542,3505,3497,3499,3513,3515,3528,152,171,1670,165,157,257,156,192,175,170,230,169,238,260,229])).
% 59.38/59.41 cnf(3568,plain,
% 59.38/59.41 (P4(x35681,x35682,a2,a16,x35682,x35681,a2,a16)),
% 59.38/59.41 inference(scs_inference,[],[3517,3489,3530,3501,3503,3542,3505,3497,3499,3513,3515,3528,152,171,1670,165,157,257,156,192,175,170,230,169,238,260,229,259])).
% 59.38/59.41 cnf(3575,plain,
% 59.38/59.41 (P3(a18,a17,a16,a2)),
% 59.38/59.41 inference(scs_inference,[],[3517,3489,3530,3501,3503,3542,3505,3497,3499,3507,3513,3515,3528,152,151,171,1670,165,157,257,156,192,175,170,230,169,238,260,229,259,258,190,1847,246])).
% 59.38/59.41 cnf(3577,plain,
% 59.38/59.41 (P6(a16,a16,a2,a16)),
% 59.38/59.41 inference(scs_inference,[],[3517,3489,3530,3501,3503,3542,3505,3497,3499,3507,3513,3515,3528,1928,152,151,171,1670,165,157,257,156,192,175,170,230,169,238,260,229,259,258,190,1847,246,241])).
% 59.38/59.41 cnf(3579,plain,
% 59.38/59.41 (P1(a16,a16,f13(a2,a2,a2,a2,a16,a16))),
% 59.38/59.41 inference(scs_inference,[],[3517,3489,3530,3534,3501,3503,3542,3505,3497,3499,3507,3513,3515,3528,1928,152,151,171,1670,165,157,257,156,192,175,170,230,169,238,260,229,259,258,190,1847,246,241,211])).
% 59.38/59.41 cnf(3583,plain,
% 59.38/59.41 (P5(a16,a16,a16,a16)),
% 59.38/59.41 inference(scs_inference,[],[3517,3489,3530,3534,3501,3503,3542,3505,3497,3499,3507,3513,3515,3528,1928,152,151,171,1670,165,157,257,156,192,175,170,230,169,238,260,229,259,258,190,1847,246,241,211,212,256])).
% 59.38/59.41 cnf(3585,plain,
% 59.38/59.41 (P1(a15,a15,a2)),
% 59.38/59.41 inference(scs_inference,[],[3517,3489,3530,3534,3501,3503,3542,3505,3497,3499,3507,3513,3515,3528,1928,152,151,171,1670,165,157,257,156,192,175,170,230,169,238,260,229,259,258,190,1847,246,241,211,212,256,1783])).
% 59.38/59.41 cnf(3588,plain,
% 59.38/59.41 (P9(a2,a2,a15,a2,a2,a2,a15,a2)),
% 59.38/59.41 inference(scs_inference,[],[3517,3489,3530,3534,3501,3503,3542,3505,3497,3499,3507,3513,3515,3528,1928,152,151,171,1670,165,157,257,156,192,175,170,230,169,238,260,229,259,258,190,1847,246,241,211,212,256,1783,1815,1831,262])).
% 59.38/59.41 cnf(3590,plain,
% 59.38/59.41 (P9(a2,a15,a2,a2,a15,a2,a2,a2)),
% 59.38/59.41 inference(scs_inference,[],[3517,3489,3530,3534,3501,3503,3542,3505,3497,3499,3507,3513,3515,3528,1928,152,151,171,1670,165,157,257,156,192,175,170,230,169,238,260,229,259,258,190,1847,246,241,211,212,256,1783,1815,1831,262,263])).
% 59.38/59.41 cnf(3592,plain,
% 59.38/59.41 (P9(a15,a2,a15,a2,a2,a2,a2,a2)),
% 59.38/59.41 inference(scs_inference,[],[3517,3489,3530,3534,3501,3503,3542,3505,3497,3499,3507,3513,3515,3528,1928,152,151,171,1670,165,157,257,156,192,175,170,230,169,238,260,229,259,258,190,1847,246,241,211,212,256,1783,1815,1831,262,263,264])).
% 59.38/59.41 cnf(3612,plain,
% 59.38/59.41 (P4(a16,a16,a16,a16,a16,a16,a16,a16)),
% 59.38/59.41 inference(scs_inference,[],[3517,3489,3530,3534,3501,3503,3542,3505,3497,3499,3507,3513,3515,3528,1928,152,151,171,1670,165,157,257,156,192,175,170,230,169,238,260,229,259,258,190,1847,246,241,211,212,256,1783,1815,1831,262,263,264,447,474,503,530,561,593,670,688,168,231])).
% 59.38/59.41 cnf(3614,plain,
% 59.38/59.41 (P6(a16,a16,a16,a2)),
% 59.38/59.41 inference(scs_inference,[],[3517,3489,3530,3534,3501,3503,3542,3505,3497,3499,3507,3513,3515,3528,1928,152,151,171,1670,165,157,257,156,192,175,170,230,169,238,260,229,259,258,190,1847,246,241,211,212,256,1783,1815,1831,262,263,264,447,474,503,530,561,593,670,688,168,231,176])).
% 59.38/59.41 cnf(3616,plain,
% 59.38/59.41 (P6(a2,a16,a2,a2)),
% 59.38/59.41 inference(scs_inference,[],[3517,3489,3530,3534,3501,3503,3542,3505,3497,3499,3507,3513,3515,3528,1928,152,151,171,1670,165,157,257,156,192,175,170,230,169,238,260,229,259,258,190,1847,246,241,211,212,256,1783,1815,1831,262,263,264,447,474,503,530,561,593,670,688,168,231,176,174])).
% 59.38/59.41 cnf(3618,plain,
% 59.38/59.41 (P6(a2,a16,a16,a16)),
% 59.38/59.41 inference(scs_inference,[],[3517,3489,3530,3534,3501,3503,3542,3505,3497,3499,3507,3513,3515,3528,1928,152,151,171,1670,165,157,257,156,192,175,170,230,169,238,260,229,259,258,190,1847,246,241,211,212,256,1783,1815,1831,262,263,264,447,474,503,530,561,593,670,688,168,231,176,174,2272])).
% 59.38/59.41 cnf(3622,plain,
% 59.38/59.41 (P2(a16,a16,a16,a16)),
% 59.38/59.41 inference(scs_inference,[],[3517,3489,3530,3534,3501,3503,3542,3505,3497,3499,3507,3513,3515,3528,1928,153,152,151,171,1670,165,157,257,156,192,175,170,230,169,238,260,229,259,258,190,1847,246,241,211,212,256,1783,1815,1831,262,263,264,447,474,503,530,561,593,670,688,168,231,176,174,2272,177,189])).
% 59.38/59.41 cnf(3628,plain,
% 59.38/59.41 (P3(a16,a16,a16,a16)),
% 59.38/59.41 inference(scs_inference,[],[3517,3489,3530,3534,3501,3503,3542,3505,3497,3499,3507,3513,3515,3528,1928,153,152,151,171,1670,165,157,257,156,192,175,170,230,169,238,260,229,259,258,190,1847,246,241,211,212,256,1783,1815,1831,262,263,264,447,474,503,530,561,593,670,688,168,231,176,174,2272,177,189,250,254,186])).
% 59.38/59.41 cnf(3630,plain,
% 59.38/59.41 (P5(a16,a16,a16,f31(a16,a16,a16,a16,a16))),
% 59.38/59.41 inference(scs_inference,[],[3517,3489,3530,3534,3501,3503,3542,3505,3497,3499,3507,3513,3515,3528,1928,153,152,151,171,1670,165,157,257,156,192,175,170,230,169,238,260,229,259,258,190,1847,246,241,211,212,256,1783,1815,1831,262,263,264,447,474,503,530,561,593,670,688,168,231,176,174,2272,177,189,250,254,186,204])).
% 59.38/59.41 cnf(3632,plain,
% 59.38/59.41 (P6(a16,a16,a16,a16)),
% 59.38/59.41 inference(scs_inference,[],[3517,3489,3530,3534,3501,3503,3542,3505,3497,3499,3507,3513,3515,3528,1928,153,152,151,171,1670,165,157,257,156,192,175,170,230,169,238,260,229,259,258,190,1847,246,241,211,212,256,1783,1815,1831,262,263,264,447,474,503,530,561,593,670,688,168,231,176,174,2272,177,189,250,254,186,204,201])).
% 59.38/59.41 cnf(3636,plain,
% 59.38/59.41 (P8(a16,a16,a16)),
% 59.38/59.41 inference(scs_inference,[],[3517,3489,3530,3534,3501,3503,3542,3505,3497,3499,3507,3513,3515,3528,1928,153,152,151,171,1670,165,157,257,156,192,175,170,230,169,238,260,229,259,258,190,1847,246,241,211,212,256,1783,1815,1831,262,263,264,447,474,503,530,561,593,670,688,168,231,176,174,2272,177,189,250,254,186,204,201,233,244])).
% 59.38/59.41 cnf(3659,plain,
% 59.38/59.41 (P9(a2,a2,a2,a2,a2,a16,a16,a16)),
% 59.38/59.41 inference(scs_inference,[],[3541,1975])).
% 59.38/59.41 cnf(3666,plain,
% 59.38/59.41 (P9(a2,a2,a2,a15,a2,a2,a15,a2)),
% 59.38/59.41 inference(scs_inference,[],[3590,3630,670,530,503,262])).
% 59.38/59.41 cnf(3668,plain,
% 59.38/59.41 (P9(a15,a2,a2,a2,a2,a15,a2,a2)),
% 59.38/59.41 inference(scs_inference,[],[3590,3630,670,530,503,262,261])).
% 59.38/59.41 cnf(3672,plain,
% 59.38/59.41 (P1(x36721,x36722,x36722)),
% 59.38/59.41 inference(scs_inference,[],[3526,3568,3590,3630,670,530,503,262,261,257,1670])).
% 59.38/59.41 cnf(3674,plain,
% 59.38/59.41 (P9(a2,a15,a15,a2,a2,a2,a2,a2)),
% 59.38/59.41 inference(scs_inference,[],[3526,3568,3590,3592,3630,670,530,503,262,261,257,1670,263])).
% 59.38/59.41 cnf(3678,plain,
% 59.38/59.41 (P9(a2,a2,a2,a2,a15,a2,a15,a2)),
% 59.38/59.41 inference(scs_inference,[],[3526,3568,3588,3590,3592,3630,670,530,503,262,261,257,1670,263,688,264])).
% 59.38/59.41 cnf(3682,plain,
% 59.38/59.41 (P3(a15,a2,a17,a1)),
% 59.38/59.41 inference(scs_inference,[],[3526,3568,3556,3588,3590,3592,3622,3630,670,530,503,262,261,257,1670,263,688,264,192,171])).
% 59.38/59.41 cnf(3690,plain,
% 59.38/59.41 (P4(x36901,x36902,x36903,x36904,x36901,x36902,x36903,x36904)),
% 59.38/59.41 inference(scs_inference,[],[3562,3526,3568,3556,3588,3590,3592,3622,3579,3630,670,530,503,262,261,257,1670,263,688,264,192,171,593,157,447,230])).
% 59.38/59.41 cnf(3698,plain,
% 59.38/59.41 (P10(x36981,x36982,x36982,x36981)),
% 59.38/59.41 inference(scs_inference,[],[3562,3526,3568,3556,3588,3590,3592,3622,3579,3630,670,530,503,262,261,257,1670,263,688,264,192,171,593,157,447,230,561,474,231,169])).
% 59.38/59.41 cnf(3702,plain,
% 59.38/59.41 (P1(a15,a1,a2)),
% 59.38/59.41 inference(scs_inference,[],[3562,3491,3526,3539,3568,3556,3588,3590,3592,3622,3579,3630,670,530,503,262,261,257,1670,263,688,264,192,171,593,157,447,230,561,474,231,169,170,156])).
% 59.38/59.41 cnf(3706,plain,
% 59.38/59.41 (P6(a2,a2,a16,a2)),
% 59.38/59.41 inference(scs_inference,[],[3562,3491,3526,3539,3616,3568,3556,3588,3590,3592,3618,3622,3579,3630,670,530,503,262,261,257,1670,263,688,264,192,171,593,157,447,230,561,474,231,169,170,156,174,175])).
% 59.38/59.41 cnf(3708,plain,
% 59.38/59.41 (P10(a16,a16,a16,f31(a16,a16,a16,a16,a16))),
% 59.38/59.41 inference(scs_inference,[],[3562,3491,3526,3539,3616,3568,3556,3588,3590,3592,3618,3622,3579,3630,670,530,503,262,261,257,1670,263,688,264,192,171,593,157,447,230,561,474,231,169,170,156,174,175,238])).
% 59.38/59.41 cnf(3710,plain,
% 59.38/59.41 (P4(a16,a16,a2,a16,a16,a2,a2,a2)),
% 59.38/59.41 inference(scs_inference,[],[3562,3523,3491,3526,3539,3616,3568,3556,3588,3590,3592,3618,3622,3579,3630,670,530,503,262,261,257,1670,263,688,264,192,171,593,157,447,230,561,474,231,169,170,156,174,175,238,260])).
% 59.38/59.41 cnf(3714,plain,
% 59.38/59.41 (P4(a16,a2,a16,a16,a2,a2,a2,a16)),
% 59.38/59.41 inference(scs_inference,[],[3562,3532,3523,3491,3526,3539,3616,3568,3556,3588,3590,3592,3618,3622,3579,3630,670,530,503,262,261,257,1670,263,688,264,192,171,593,157,447,230,561,474,231,169,170,156,174,175,238,260,2272,229])).
% 59.38/59.41 cnf(3716,plain,
% 59.38/59.41 (P5(a16,a16,f31(a16,a16,a16,a16,a16),a16)),
% 59.38/59.41 inference(scs_inference,[],[3562,3532,3523,3491,3526,3539,3616,3568,3556,3588,3590,3592,3618,3622,3579,3630,670,530,503,262,261,257,1670,263,688,264,192,171,593,157,447,230,561,474,231,169,170,156,174,175,238,260,2272,229,173])).
% 59.38/59.41 cnf(3718,plain,
% 59.38/59.41 (P5(a16,f31(a16,a16,a16,a16,a16),a16,a16)),
% 59.38/59.41 inference(scs_inference,[],[3562,3532,3523,3491,3526,3539,3616,3568,3556,3588,3590,3592,3618,3622,3579,3630,670,530,503,262,261,257,1670,263,688,264,192,171,593,157,447,230,561,474,231,169,170,156,174,175,238,260,2272,229,173,172])).
% 59.38/59.41 cnf(3722,plain,
% 59.38/59.41 (P4(a15,a2,x37221,x37222,a2,a15,x37221,x37222)),
% 59.38/59.41 inference(scs_inference,[],[3562,3532,3523,3491,3526,3539,3616,3558,3568,3556,3588,3590,3592,3618,3622,3579,3630,670,530,503,262,261,257,1670,263,688,264,192,171,593,157,447,230,561,474,231,169,170,156,174,175,238,260,2272,229,173,172,258,259])).
% 59.38/59.41 cnf(3732,plain,
% 59.38/59.41 (P2(f8(a16,a16,a16),a16,a16,a16)),
% 59.38/59.41 inference(scs_inference,[],[3562,3532,3523,3491,3526,3539,3583,3616,3636,3558,3568,3556,3588,3590,3592,3614,3618,3622,3628,3579,3630,670,530,503,262,261,257,1670,263,688,264,192,171,593,157,447,230,561,474,231,169,170,156,174,175,238,260,2272,229,173,172,258,259,228,181,194,195,196])).
% 59.38/59.41 cnf(3738,plain,
% 59.38/59.41 (P3(f12(a16,a16,a16,a16,a16),a16,a16,a16)),
% 59.38/59.41 inference(scs_inference,[],[3541,3562,3532,3523,3491,3526,3539,3583,3616,3636,3558,3568,3556,3588,3590,3592,3614,3618,3622,3628,3579,3630,443,670,530,503,262,261,257,1670,263,688,264,192,171,593,157,447,230,561,474,231,169,170,156,174,175,238,260,2272,229,173,172,258,259,228,181,194,195,196,198,202,203])).
% 59.38/59.41 cnf(3739,plain,
% 59.38/59.41 (P1(x37391,x37391,x37391)),
% 59.38/59.41 inference(rename_variables,[],[3541])).
% 59.38/59.41 cnf(3741,plain,
% 59.38/59.41 (P10(f29(a16,a16,a16,a16,a16,a16),a16,a16,a16)),
% 59.38/59.41 inference(scs_inference,[],[3541,3562,3532,3523,3491,3526,3539,3583,3616,3636,3558,3568,3556,3588,3590,3592,3614,3618,3622,3628,3579,3630,443,670,530,503,262,261,257,1670,263,688,264,192,171,593,157,447,230,561,474,231,169,170,156,174,175,238,260,2272,229,173,172,258,259,228,181,194,195,196,198,202,203,209])).
% 59.38/59.41 cnf(3743,plain,
% 59.38/59.41 (P10(f31(a16,a16,a16,a16,a16),a16,a16,a16)),
% 59.38/59.41 inference(scs_inference,[],[3541,3562,3532,3523,3491,3526,3539,3583,3616,3636,3558,3568,3556,3588,3590,3592,3614,3618,3622,3628,3579,3630,443,670,530,503,262,261,257,1670,263,688,264,192,171,593,157,447,230,561,474,231,169,170,156,174,175,238,260,2272,229,173,172,258,259,228,181,194,195,196,198,202,203,209,206])).
% 59.38/59.41 cnf(3746,plain,
% 59.38/59.41 (P10(x37461,x37462,x37461,x37462)),
% 59.38/59.41 inference(rename_variables,[],[3562])).
% 59.38/59.41 cnf(3757,plain,
% 59.38/59.41 (P9(a15,a2,a15,a2,a15,a2,a15,a2)),
% 59.38/59.41 inference(scs_inference,[],[3541,3562,3532,3523,3491,3526,3539,3583,3616,3636,3548,3558,3568,3556,3588,3590,3592,3612,3614,3618,3622,3628,3579,3630,400,443,670,530,503,262,261,257,1670,263,688,264,192,171,593,157,447,230,561,474,231,169,170,156,174,175,238,260,2272,229,173,172,258,259,228,181,194,195,196,198,202,203,209,206,2592,251,267,193,248,268])).
% 59.38/59.41 cnf(3759,plain,
% 59.38/59.41 (P2(a16,a16,f31(a16,a16,a16,a16,a16),f31(a16,a16,a16,a16,a16))),
% 59.38/59.41 inference(scs_inference,[],[3541,3562,3532,3523,3491,3526,3539,3583,3616,3636,3548,3558,3568,3556,3588,3590,3592,3612,3614,3618,3622,3628,3579,3630,400,443,670,530,503,262,261,257,1670,263,688,264,192,171,593,157,447,230,561,474,231,169,170,156,174,175,238,260,2272,229,173,172,258,259,228,181,194,195,196,198,202,203,209,206,2592,251,267,193,248,268,189])).
% 59.38/59.41 cnf(3763,plain,
% 59.38/59.41 (P3(a2,a16,a2,a16)),
% 59.38/59.41 inference(scs_inference,[],[3541,3562,3532,3523,3491,3526,3539,3583,3616,3636,3548,3558,3564,3568,3556,3588,3590,3592,3612,3614,3618,3622,3628,3579,3630,400,443,670,530,503,262,261,257,1670,263,688,264,192,171,593,157,447,230,561,474,231,169,170,156,174,175,238,260,2272,229,173,172,258,259,228,181,194,195,196,198,202,203,209,206,2592,251,267,193,248,268,189,186,246])).
% 59.38/59.41 cnf(3768,plain,
% 59.38/59.41 (P6(a15,a2,a2,a2)),
% 59.38/59.41 inference(scs_inference,[],[3541,3739,3562,3532,3523,3491,3526,3539,3583,3616,3636,3548,3558,3564,3568,3556,3588,3590,3592,3612,3614,3618,3622,3628,3579,3630,400,443,670,530,503,262,261,257,1670,263,688,264,192,171,593,157,447,230,561,474,231,169,170,156,174,175,238,260,2272,229,173,172,258,259,228,181,194,195,196,198,202,203,209,206,2592,251,267,193,248,268,189,186,246,160,241])).
% 59.38/59.41 cnf(3770,plain,
% 59.38/59.41 (P1(x37701,x37701,x37701)),
% 59.38/59.41 inference(rename_variables,[],[3541])).
% 59.38/59.41 cnf(3777,plain,
% 59.38/59.41 (P10(x37771,x37772,x37771,x37772)),
% 59.38/59.41 inference(rename_variables,[],[3562])).
% 59.38/59.41 cnf(3779,plain,
% 59.38/59.41 (P8(a16,x37791,x37791)),
% 59.38/59.41 inference(scs_inference,[],[3541,3739,3562,3746,3777,3532,3523,3491,3526,3539,3583,3616,3636,3548,3558,3564,3568,3556,3588,3590,3592,3612,3614,3618,3622,3628,3632,3579,3630,400,443,670,530,503,262,261,257,1670,263,688,264,192,171,593,157,447,230,561,474,231,169,170,156,174,175,238,260,2272,229,173,172,258,259,228,181,194,195,196,198,202,203,209,206,2592,251,267,193,248,268,189,186,246,160,241,208,191,197,180])).
% 59.38/59.41 cnf(3783,plain,
% 59.38/59.41 (P6(a16,f31(a16,a16,a16,a16,a16),f31(a16,a16,a16,a16,a16),f31(a16,a16,a16,a16,a16))),
% 59.38/59.41 inference(scs_inference,[],[3541,3739,3562,3746,3777,3532,3523,3491,3526,3539,3583,3616,3636,3548,3558,3564,3568,3556,3588,3590,3592,3612,3614,3618,3622,3628,3632,3579,3630,400,443,670,530,503,262,261,257,1670,263,688,264,192,171,593,157,447,230,561,474,231,169,170,156,174,175,238,260,2272,229,173,172,258,259,228,181,194,195,196,198,202,203,209,206,2592,251,267,193,248,268,189,186,246,160,241,208,191,197,180,201])).
% 59.38/59.41 cnf(3785,plain,
% 59.38/59.41 (P8(a2,a2,a16)),
% 59.38/59.41 inference(scs_inference,[],[3541,3739,3562,3746,3777,3532,3509,3523,3491,3526,3539,3583,3616,3636,3548,3558,3564,3568,3556,3588,3590,3592,3612,3614,3618,3622,3628,3632,3579,3630,400,443,1950,670,530,503,262,261,257,1670,263,688,264,192,171,593,157,447,230,561,474,231,169,170,156,174,175,238,260,2272,229,173,172,258,259,228,181,194,195,196,198,202,203,209,206,2592,251,267,193,248,268,189,186,246,160,241,208,191,197,180,201,167])).
% 59.38/59.41 cnf(3789,plain,
% 59.38/59.41 (P5(a2,a16,a2,a16)),
% 59.38/59.41 inference(scs_inference,[],[142,3541,3739,3562,3746,3777,3532,3509,3523,3491,3526,3539,3583,3616,3636,3548,3558,3564,3568,3556,3560,3588,3590,3592,3612,3614,3618,3622,3628,3632,3579,3630,400,443,1950,670,530,503,262,261,257,1670,263,688,264,192,171,593,157,447,230,561,474,231,169,170,156,174,175,238,260,2272,229,173,172,258,259,228,181,194,195,196,198,202,203,209,206,2592,251,267,193,248,268,189,186,246,160,241,208,191,197,180,201,167,212,256])).
% 59.38/59.41 cnf(3793,plain,
% 59.38/59.41 (P8(f26(a16,x37931),a16,x37931)),
% 59.38/59.41 inference(scs_inference,[],[142,3541,3739,3770,3562,3746,3777,3532,3509,3523,3491,3526,3539,3583,3616,3636,3548,3558,3564,3568,3556,3560,3588,3590,3592,3612,3614,3618,3622,3628,3632,3579,3630,400,443,1950,670,530,503,262,261,257,1670,263,688,264,192,171,593,157,447,230,561,474,231,169,170,156,174,175,238,260,2272,229,173,172,258,259,228,181,194,195,196,198,202,203,209,206,2592,251,267,193,248,268,189,186,246,160,241,208,191,197,180,201,167,212,256,211,164])).
% 59.38/59.41 cnf(3797,plain,
% 59.38/59.41 (P1(f26(a16,x37971),a16,x37971)),
% 59.38/59.41 inference(scs_inference,[],[142,3541,3739,3770,3562,3746,3777,3532,3509,3523,3491,3526,3539,3583,3616,3636,3548,3558,3564,3568,3556,3560,3588,3590,3592,3612,3614,3618,3622,3628,3632,3579,3630,400,443,1950,670,530,503,262,261,257,1670,263,688,264,192,171,593,157,447,230,561,474,231,169,170,156,174,175,238,260,2272,229,173,172,258,259,228,181,194,195,196,198,202,203,209,206,2592,251,267,193,248,268,189,186,246,160,241,208,191,197,180,201,167,212,256,211,164,158])).
% 59.38/59.41 cnf(3811,plain,
% 59.38/59.41 (P10(a16,f31(a16,a16,a16,a16,a16),a16,a16)),
% 59.38/59.41 inference(scs_inference,[],[142,3541,3739,3770,3562,3746,3777,3532,3509,3523,3491,3526,3539,3583,3616,3636,3548,3558,3564,3568,3556,3560,3588,3590,3592,3612,3614,3618,3622,3628,3632,3579,3630,400,443,1950,670,530,503,262,261,257,1670,263,688,264,192,171,593,157,447,230,561,474,231,169,170,156,174,175,238,260,2272,229,173,172,258,259,228,181,194,195,196,198,202,203,209,206,2592,251,267,193,248,268,189,186,246,160,241,208,191,197,180,201,167,212,256,211,164,158,644,650,815,3488,640,161,168])).
% 59.38/59.41 cnf(3813,plain,
% 59.38/59.41 (P1(a16,a16,f31(a16,a16,a16,a16,a16))),
% 59.38/59.41 inference(scs_inference,[],[142,3541,3739,3770,3562,3746,3777,3532,3509,3523,3491,3526,3539,3583,3616,3636,3548,3558,3564,3568,3556,3560,3588,3590,3592,3612,3614,3618,3622,3628,3632,3579,3630,400,443,1950,670,530,503,262,261,257,1670,263,688,264,192,171,593,157,447,230,561,474,231,169,170,156,174,175,238,260,2272,229,173,172,258,259,228,181,194,195,196,198,202,203,209,206,2592,251,267,193,248,268,189,186,246,160,241,208,191,197,180,201,167,212,256,211,164,158,644,650,815,3488,640,161,168,165])).
% 59.38/59.41 cnf(3815,plain,
% 59.38/59.41 (P8(a2,a16,a2)),
% 59.38/59.41 inference(scs_inference,[],[142,3541,3739,3770,3562,3746,3777,3532,3509,3523,3491,3526,3539,3583,3616,3636,3548,3558,3564,3568,3556,3560,3588,3590,3592,3612,3614,3618,3622,3628,3632,3579,3630,400,443,1950,670,530,503,262,261,257,1670,263,688,264,192,171,593,157,447,230,561,474,231,169,170,156,174,175,238,260,2272,229,173,172,258,259,228,181,194,195,196,198,202,203,209,206,2592,251,267,193,248,268,189,186,246,160,241,208,191,197,180,201,167,212,256,211,164,158,644,650,815,3488,640,161,168,165,159])).
% 59.38/59.41 cnf(3819,plain,
% 59.38/59.41 (P1(f4(a2,a2,a16),a16,a2)),
% 59.38/59.41 inference(scs_inference,[],[142,3541,3739,3770,3562,3746,3777,3532,3509,3523,3491,3526,3539,3583,3616,3636,3548,3558,3564,3568,3556,3560,3588,3590,3592,3612,3614,3618,3622,3628,3632,3579,3630,400,452,443,1950,670,530,503,262,261,257,1670,263,688,264,192,171,593,157,447,230,561,474,231,169,170,156,174,175,238,260,2272,229,173,172,258,259,228,181,194,195,196,198,202,203,209,206,2592,251,267,193,248,268,189,186,246,160,241,208,191,197,180,201,167,212,256,211,164,158,644,650,815,3488,640,161,168,165,159,179,182])).
% 59.38/59.41 cnf(3821,plain,
% 59.38/59.41 (P1(f5(a2,a2,a16),a16,a2)),
% 59.38/59.41 inference(scs_inference,[],[142,3541,3739,3770,3562,3746,3777,3532,3509,3523,3491,3526,3539,3583,3616,3636,3548,3558,3564,3568,3556,3560,3588,3590,3592,3612,3614,3618,3622,3628,3632,3579,3630,400,452,443,1950,670,530,503,262,261,257,1670,263,688,264,192,171,593,157,447,230,561,474,231,169,170,156,174,175,238,260,2272,229,173,172,258,259,228,181,194,195,196,198,202,203,209,206,2592,251,267,193,248,268,189,186,246,160,241,208,191,197,180,201,167,212,256,211,164,158,644,650,815,3488,640,161,168,165,159,179,182,183])).
% 59.38/59.41 cnf(3823,plain,
% 59.38/59.41 (P4(a16,a16,a16,f31(a16,a16,a16,a16,a16),f31(a16,a16,a16,a16,a16),a16,f31(a16,a16,a16,a16,a16),f31(a16,a16,a16,a16,a16))),
% 59.38/59.41 inference(scs_inference,[],[142,3541,3739,3770,3562,3746,3777,3532,3509,3523,3491,3526,3539,3583,3616,3636,3548,3558,3564,3568,3556,3560,3588,3590,3592,3612,3614,3618,3622,3628,3632,3579,3630,400,452,443,1950,670,530,503,262,261,257,1670,263,688,264,192,171,593,157,447,230,561,474,231,169,170,156,174,175,238,260,2272,229,173,172,258,259,228,181,194,195,196,198,202,203,209,206,2592,251,267,193,248,268,189,186,246,160,241,208,191,197,180,201,167,212,256,211,164,158,644,650,815,3488,640,161,168,165,159,179,182,183,234])).
% 59.38/59.41 cnf(3827,plain,
% 59.38/59.41 (P3(a16,f31(a16,a16,a16,a16,a16),f31(a16,a16,a16,a16,a16),f31(a16,a16,a16,a16,a16))),
% 59.38/59.41 inference(scs_inference,[],[142,3541,3739,3770,3562,3746,3777,3532,3509,3523,3491,3526,3539,3583,3616,3636,3548,3558,3564,3568,3556,3560,3588,3590,3592,3612,3614,3618,3622,3628,3632,3579,3630,400,452,443,1950,670,530,503,262,261,257,1670,263,688,264,192,171,593,157,447,230,561,474,231,169,170,156,174,175,238,260,2272,229,173,172,258,259,228,181,194,195,196,198,202,203,209,206,2592,251,267,193,248,268,189,186,246,160,241,208,191,197,180,201,167,212,256,211,164,158,644,650,815,3488,640,161,168,165,159,179,182,183,234,210,177])).
% 59.38/59.41 cnf(3832,plain,
% 59.38/59.41 (P4(x38321,x38322,a2,a16,x38322,x38321,a2,a16)),
% 59.38/59.41 inference(rename_variables,[],[3568])).
% 59.38/59.41 cnf(3839,plain,
% 59.38/59.41 (P3(a16,a2,a2,a16)),
% 59.38/59.41 inference(scs_inference,[],[142,3541,3739,3770,3562,3746,3777,3532,3509,3523,3491,3554,3526,3539,3583,3616,3636,3548,3558,3564,3568,3832,3556,3560,3588,3590,3592,3612,3614,3618,3622,3628,3632,3579,3630,400,452,443,1950,152,670,530,503,262,261,257,1670,263,688,264,192,171,593,157,447,230,561,474,231,169,170,156,174,175,238,260,2272,229,173,172,258,259,228,181,194,195,196,198,202,203,209,206,2592,251,267,193,248,268,189,186,246,160,241,208,191,197,180,201,167,212,256,211,164,158,644,650,815,3488,640,161,168,165,159,179,182,183,234,210,177,232,254,250,178,200])).
% 59.38/59.41 cnf(3852,plain,
% 59.38/59.41 (~P8(x38521,a22,a20)+~P11(f26(a22,a2),a2,a21,f26(a22,a2),a22,a2)),
% 59.38/59.41 inference(scs_inference,[],[3779,2816])).
% 59.38/59.41 cnf(3853,plain,
% 59.38/59.41 (~P8(x38531,a22,a20)+~P11(a21,a2,f26(a22,a21),a22,a2,f26(a22,a21))),
% 59.38/59.41 inference(scs_inference,[],[3779,2928])).
% 59.38/59.41 cnf(3854,plain,
% 59.38/59.41 (~P8(x38541,a21,a20)+~P11(a21,a2,f26(a21,a22),a22,a2,f26(a21,a22))),
% 59.38/59.41 inference(scs_inference,[],[3779,2944])).
% 59.38/59.41 cnf(3855,plain,
% 59.38/59.41 (~P8(x38551,a21,a15)+~P11(a2,a22,f26(a21,a2),a21,a2,f26(a21,a2))),
% 59.38/59.41 inference(scs_inference,[],[3779,3152])).
% 59.38/59.41 cnf(3856,plain,
% 59.38/59.41 (~P8(x38561,a2,a15)+~P11(a2,a22,f26(a2,a21),a21,a2,f26(a2,a21))),
% 59.38/59.41 inference(scs_inference,[],[3779,3168])).
% 59.38/59.41 cnf(3861,plain,
% 59.38/59.41 (P9(a2,a16,a16,a16,a2,a2,a2,a2)),
% 59.38/59.41 inference(scs_inference,[],[3659,3789,3815,158,530,261])).
% 59.38/59.41 cnf(3871,plain,
% 59.38/59.41 (P4(a2,a2,a2,a16,a16,a2,a16,a16)),
% 59.38/59.41 inference(scs_inference,[],[3659,3714,3789,3815,154,158,530,261,264,670,688,192,257])).
% 59.38/59.41 cnf(3877,plain,
% 59.38/59.41 (P4(x38771,x38772,x38773,x38774,x38772,x38771,x38773,x38774)),
% 59.38/59.41 inference(scs_inference,[],[3659,3698,3714,3789,3815,3741,154,158,530,261,264,670,688,192,257,168,262,230])).
% 59.38/59.41 cnf(3889,plain,
% 59.38/59.41 (P1(x38891,x38892,x38891)),
% 59.38/59.41 inference(scs_inference,[],[3659,3698,3672,3668,3714,3789,3815,3741,3811,154,158,530,261,264,670,688,192,257,168,262,230,503,447,593,263,165,156])).
% 59.38/59.41 cnf(3891,plain,
% 59.38/59.41 (P3(a2,a16,a16,a2)),
% 59.38/59.41 inference(scs_inference,[],[3659,3698,3672,3763,3668,3714,3789,3815,3741,3811,154,158,530,261,264,670,688,192,257,168,262,230,503,447,593,263,165,156,171])).
% 59.38/59.41 cnf(3893,plain,
% 59.38/59.41 (P5(a16,x38931,a16,x38931)),
% 59.38/59.41 inference(scs_inference,[],[3659,3698,3672,3763,3668,3714,3779,3789,3815,3741,3811,154,158,530,261,264,670,688,192,257,168,262,230,503,447,593,263,165,156,171,161])).
% 59.38/59.41 cnf(3897,plain,
% 59.38/59.41 (P4(a2,a16,a16,a16,a16,a16,a2,a16)),
% 59.38/59.41 inference(scs_inference,[],[3659,3698,3672,3763,3668,3714,3779,3789,3815,3741,3811,154,158,530,261,264,670,688,192,257,168,262,230,503,447,593,263,165,156,171,161,474,231])).
% 59.38/59.41 cnf(3907,plain,
% 59.38/59.41 (P3(a16,a2,a18,a17)),
% 59.38/59.41 inference(scs_inference,[],[3659,3698,3672,3763,3668,3714,3575,3779,3702,3768,3789,3815,3741,3708,3811,154,158,530,261,264,670,688,192,257,168,262,230,503,447,593,263,165,156,171,161,474,231,174,157,169,561,170])).
% 59.38/59.41 cnf(3909,plain,
% 59.38/59.41 (P6(f31(a16,a16,a16,a16,a16),a16,f31(a16,a16,a16,a16,a16),f31(a16,a16,a16,a16,a16))),
% 59.38/59.41 inference(scs_inference,[],[3659,3698,3672,3763,3668,3714,3575,3779,3702,3768,3789,3815,3741,3708,3783,3811,154,158,530,261,264,670,688,192,257,168,262,230,503,447,593,263,165,156,171,161,474,231,174,157,169,561,170,2272])).
% 59.38/59.41 cnf(3911,plain,
% 59.38/59.41 (P4(x39111,x39112,x39111,x39112,x39113,x39114,x39113,x39114)),
% 59.38/59.41 inference(scs_inference,[],[3659,3690,3698,3672,3763,3668,3714,3575,3779,3702,3768,3789,3815,3741,3708,3783,3811,154,158,530,261,264,670,688,192,257,168,262,230,503,447,593,263,165,156,171,161,474,231,174,157,169,561,170,2272,260])).
% 59.38/59.41 cnf(3921,plain,
% 59.38/59.41 (P4(x39211,x39212,a15,a2,x39211,x39212,a2,a15)),
% 59.38/59.41 inference(scs_inference,[],[3659,3690,3698,3672,3763,3566,3668,3714,3575,3779,3722,3702,3768,3789,3815,3741,3708,3716,3783,3793,3811,154,158,530,261,264,670,688,192,257,168,262,230,503,447,593,263,165,156,171,161,474,231,174,157,169,561,170,2272,260,173,159,172,259,258])).
% 59.38/59.41 cnf(3923,plain,
% 59.38/59.41 (P10(a2,a2,a16,a16)),
% 59.38/59.41 inference(scs_inference,[],[3659,3690,3698,3672,3763,3566,3668,3714,3575,3779,3722,3702,3768,3785,3789,3815,3741,3708,3716,3783,3793,3811,154,158,530,261,264,670,688,192,257,168,262,230,503,447,593,263,165,156,171,161,474,231,174,157,169,561,170,2272,260,173,159,172,259,258,162])).
% 59.38/59.41 cnf(3925,plain,
% 59.38/59.41 (P10(a16,a16,x39251,x39251)),
% 59.38/59.41 inference(scs_inference,[],[3659,3690,3698,3672,3763,3566,3668,3714,3575,3779,3722,3702,3768,3785,3789,3815,3741,3708,3716,3783,3793,3811,154,158,530,261,264,670,688,192,257,168,262,230,503,447,593,263,165,156,171,161,474,231,174,157,169,561,170,2272,260,173,159,172,259,258,162,163])).
% 59.38/59.41 cnf(3927,plain,
% 59.38/59.41 (P8(a2,a16,a16)),
% 59.38/59.41 inference(scs_inference,[],[3659,3690,3698,3672,3763,3566,3668,3714,3575,3779,3722,3702,3768,3785,3789,3815,3741,3708,3716,3783,3793,3811,154,158,530,261,264,670,688,192,257,168,262,230,503,447,593,263,165,156,171,161,474,231,174,157,169,561,170,2272,260,173,159,172,259,258,162,163,166])).
% 59.38/59.41 cnf(3928,plain,
% 59.38/59.41 (P1(x39281,x39282,x39282)),
% 59.38/59.41 inference(rename_variables,[],[3672])).
% 59.38/59.41 cnf(3932,plain,
% 59.38/59.41 (P10(a16,a16,a16,f29(a16,a16,a16,a16,a16,a16))),
% 59.38/59.41 inference(scs_inference,[],[3659,3690,3698,3672,3763,3566,3668,3714,3575,3779,3722,3702,3768,3785,3789,3815,3741,3708,3718,3716,3783,3793,3811,154,158,530,261,264,670,688,192,257,168,262,230,503,447,593,263,165,156,171,161,474,231,174,157,169,561,170,2272,260,173,159,172,259,258,162,163,166,188,184])).
% 59.38/59.41 cnf(3933,plain,
% 59.38/59.41 (P10(x39331,x39332,x39332,x39331)),
% 59.38/59.41 inference(rename_variables,[],[3698])).
% 59.38/59.41 cnf(3937,plain,
% 59.38/59.41 (P9(a16,x39371,x39371,x39371,a16,x39371,x39371,x39371)),
% 59.38/59.41 inference(scs_inference,[],[3659,3690,3698,3672,3763,3566,3668,3714,3575,3779,3722,3702,3768,3785,3789,3815,3741,3708,3718,3716,3783,3793,3811,154,158,530,261,264,670,688,192,257,168,262,230,503,447,593,263,165,156,171,161,474,231,174,157,169,561,170,2272,260,173,159,172,259,258,162,163,166,188,184,195,228])).
% 59.38/59.41 cnf(3941,plain,
% 59.38/59.41 (P10(x39411,x39412,x39411,x39412)),
% 59.38/59.41 inference(rename_variables,[],[3562])).
% 59.38/59.41 cnf(3943,plain,
% 59.38/59.41 (P5(a16,a16,a2,a16)),
% 59.38/59.41 inference(scs_inference,[],[3659,3690,3698,3672,3763,3566,3668,3714,3575,3839,3779,3722,3702,3768,3785,3789,3815,3741,3708,3718,3716,3783,3793,3811,3562,154,158,530,261,264,670,688,192,257,168,262,230,503,447,593,263,165,156,171,161,474,231,174,157,169,561,170,2272,260,173,159,172,259,258,162,163,166,188,184,195,228,2592,179])).
% 59.38/59.41 cnf(3944,plain,
% 59.38/59.41 (P8(a16,x39441,x39441)),
% 59.38/59.41 inference(rename_variables,[],[3779])).
% 59.38/59.41 cnf(3948,plain,
% 59.38/59.41 (P2(f8(a2,a2,a16),a2,a2,a16)),
% 59.38/59.41 inference(scs_inference,[],[3659,3690,3698,3672,3763,3706,3566,3668,3714,3575,3839,3779,3722,3702,3768,3785,3789,3815,3741,3708,3718,3716,3783,3793,3811,3562,154,158,530,261,264,670,688,192,257,168,262,230,503,447,593,263,165,156,171,161,474,231,174,157,169,561,170,2272,260,173,159,172,259,258,162,163,166,188,184,195,228,2592,179,205,196])).
% 59.38/59.41 cnf(3953,plain,
% 59.38/59.41 (P8(a16,x39531,x39531)),
% 59.38/59.41 inference(rename_variables,[],[3779])).
% 59.38/59.41 cnf(3955,plain,
% 59.38/59.41 (P3(f12(a16,a16,a2,x39551,x39551),a16,x39551,x39551)),
% 59.38/59.41 inference(scs_inference,[],[3659,3690,3698,3672,3928,3763,3706,3566,3668,3714,3575,3839,3779,3944,3722,3702,3768,3785,3789,3815,3741,3708,3718,3716,3783,3793,3759,3811,3562,154,158,530,261,264,670,688,192,257,168,262,230,503,447,593,263,165,156,171,161,474,231,174,157,169,561,170,2272,260,173,159,172,259,258,162,163,166,188,184,195,228,2592,179,205,196,193,232,203])).
% 59.38/59.41 cnf(3956,plain,
% 59.38/59.41 (P1(x39561,x39562,x39562)),
% 59.38/59.41 inference(rename_variables,[],[3672])).
% 59.38/59.41 cnf(3958,plain,
% 59.38/59.41 (P10(f29(x39581,x39581,x39581,x39581,a16,a16),a16,x39581,x39581)),
% 59.38/59.41 inference(scs_inference,[],[3659,3690,3698,3672,3928,3763,3706,3566,3668,3714,3575,3839,3779,3944,3953,3722,3702,3768,3785,3789,3815,3741,3708,3718,3716,3783,3793,3759,3811,3562,154,158,530,261,264,670,688,192,257,168,262,230,503,447,593,263,165,156,171,161,474,231,174,157,169,561,170,2272,260,173,159,172,259,258,162,163,166,188,184,195,228,2592,179,205,196,193,232,203,209])).
% 59.38/59.41 cnf(3961,plain,
% 59.38/59.41 (P4(x39611,x39612,x39613,x39614,x39611,x39612,x39613,x39614)),
% 59.38/59.41 inference(rename_variables,[],[3690])).
% 59.38/59.41 cnf(3969,plain,
% 59.38/59.41 (P10(f31(a2,a16,a16,a16,a2),a16,a2,a16)),
% 59.38/59.41 inference(scs_inference,[],[3659,3690,3698,3672,3928,3763,3706,3566,3668,3714,3575,3839,3779,3944,3953,3722,3702,3768,3785,3789,3815,3741,3708,3718,3716,3783,3793,3759,3811,3732,3562,154,158,530,261,264,670,688,192,257,168,262,230,503,447,593,263,165,156,171,161,474,231,174,157,169,561,170,2272,260,173,159,172,259,258,162,163,166,188,184,195,228,2592,179,205,196,193,232,203,209,247,210,194,181,206])).
% 59.38/59.41 cnf(3971,plain,
% 59.38/59.41 (P5(a2,a2,a2,a2)),
% 59.38/59.41 inference(scs_inference,[],[3659,3690,3698,3672,3928,3763,3706,3566,3668,3714,3575,3839,3779,3944,3953,3722,3702,3768,3785,3789,3815,3741,3708,3718,3716,3783,3793,3759,3811,3732,3562,154,158,530,261,264,670,688,192,257,168,262,230,503,447,593,263,165,156,171,161,474,231,174,157,169,561,170,2272,260,173,159,172,259,258,162,163,166,188,184,195,228,2592,179,205,196,193,232,203,209,247,210,194,181,206,248])).
% 59.38/59.41 cnf(3973,plain,
% 59.38/59.41 (P5(a2,a16,a2,f31(a2,a16,a16,a16,a2))),
% 59.38/59.41 inference(scs_inference,[],[3659,3690,3698,3672,3928,3763,3706,3566,3668,3714,3575,3839,3779,3944,3953,3722,3702,3768,3785,3789,3815,3741,3708,3718,3716,3783,3793,3759,3811,3732,3562,154,158,530,261,264,670,688,192,257,168,262,230,503,447,593,263,165,156,171,161,474,231,174,157,169,561,170,2272,260,173,159,172,259,258,162,163,166,188,184,195,228,2592,179,205,196,193,232,203,209,247,210,194,181,206,248,204])).
% 59.38/59.41 cnf(3975,plain,
% 59.38/59.41 (P3(a2,a2,a16,a16)),
% 59.38/59.41 inference(scs_inference,[],[3659,3690,3698,3672,3928,3763,3706,3566,3668,3714,3575,3839,3779,3944,3953,3722,3702,3768,3785,3789,3815,3741,3708,3718,3716,3783,3793,3759,3811,3732,3562,154,158,530,261,264,670,688,192,257,168,262,230,503,447,593,263,165,156,171,161,474,231,174,157,169,561,170,2272,260,173,159,172,259,258,162,163,166,188,184,195,228,2592,179,205,196,193,232,203,209,247,210,194,181,206,248,204,186])).
% 59.38/59.41 cnf(3977,plain,
% 59.38/59.41 (P2(a2,a16,a16,a16)),
% 59.38/59.41 inference(scs_inference,[],[3659,3690,3698,3672,3928,3763,3706,3566,3668,3714,3575,3839,3779,3944,3953,3722,3702,3768,3785,3789,3815,3741,3708,3718,3716,3783,3793,3759,3811,3732,3562,154,158,530,261,264,670,688,192,257,168,262,230,503,447,593,263,165,156,171,161,474,231,174,157,169,561,170,2272,260,173,159,172,259,258,162,163,166,188,184,195,228,2592,179,205,196,193,232,203,209,247,210,194,181,206,248,204,186,189])).
% 59.38/59.41 cnf(3980,plain,
% 59.38/59.41 (P8(a16,x39801,x39801)),
% 59.38/59.41 inference(rename_variables,[],[3779])).
% 59.38/59.41 cnf(3982,plain,
% 59.38/59.41 (P6(x39821,x39822,x39822,x39822)),
% 59.38/59.41 inference(scs_inference,[],[3659,3690,3961,3698,3672,3928,3956,3763,3706,3566,3668,3714,3575,3839,3779,3944,3953,3722,3702,3768,3785,3789,3815,3741,3708,3718,3716,3738,3783,3793,3759,3811,3732,3562,154,158,530,261,264,670,688,192,257,168,262,230,503,447,593,263,165,156,171,161,474,231,174,157,169,561,170,2272,260,173,159,172,259,258,162,163,166,188,184,195,228,2592,179,205,196,193,232,203,209,247,210,194,181,206,248,204,186,189,178,241])).
% 59.38/59.41 cnf(3983,plain,
% 59.38/59.41 (P1(x39831,x39832,x39832)),
% 59.38/59.41 inference(rename_variables,[],[3672])).
% 59.38/59.41 cnf(3984,plain,
% 59.38/59.41 (P4(x39841,x39842,x39843,x39844,x39841,x39842,x39843,x39844)),
% 59.38/59.41 inference(rename_variables,[],[3690])).
% 59.38/59.41 cnf(3986,plain,
% 59.38/59.41 (P3(a17,a18,a16,a2)),
% 59.38/59.41 inference(scs_inference,[],[3659,3690,3961,3698,3933,3672,3928,3956,3763,3706,3566,3668,3714,3575,3839,3779,3944,3953,3722,3702,3768,3785,3789,3815,3741,3708,3718,3716,3738,3783,3793,3759,3811,3732,3562,154,158,530,261,264,670,688,192,257,168,262,230,503,447,593,263,165,156,171,161,474,231,174,157,169,561,170,2272,260,173,159,172,259,258,162,163,166,188,184,195,228,2592,179,205,196,193,232,203,209,247,210,194,181,206,248,204,186,189,178,241,187])).
% 59.38/59.41 cnf(3987,plain,
% 59.38/59.41 (P10(x39871,x39872,x39872,x39871)),
% 59.38/59.41 inference(rename_variables,[],[3698])).
% 59.38/59.41 cnf(3989,plain,
% 59.38/59.41 (P8(f29(x39891,x39891,x39891,x39891,a16,a16),x39891,x39891)),
% 59.38/59.41 inference(scs_inference,[],[3659,3690,3961,3698,3933,3672,3928,3956,3763,3706,3566,3668,3714,3575,3839,3779,3944,3953,3980,3722,3702,3768,3785,3789,3815,3741,3708,3718,3716,3738,3783,3793,3759,3811,3732,3562,154,158,530,261,264,670,688,192,257,168,262,230,503,447,593,263,165,156,171,161,474,231,174,157,169,561,170,2272,260,173,159,172,259,258,162,163,166,188,184,195,228,2592,179,205,196,193,232,203,209,247,210,194,181,206,248,204,186,189,178,241,187,208])).
% 59.38/59.41 cnf(3992,plain,
% 59.38/59.41 (P10(x39921,x39922,x39922,x39921)),
% 59.38/59.41 inference(rename_variables,[],[3698])).
% 59.38/59.41 cnf(3996,plain,
% 59.38/59.41 (P8(a16,f31(a16,a16,a16,a16,a16),a16)),
% 59.38/59.41 inference(scs_inference,[],[3659,3690,3961,3698,3933,3987,3672,3928,3956,3763,3706,3566,3668,3714,3575,3839,3779,3944,3953,3980,3722,3702,3768,3785,3789,3815,3741,3708,3718,3716,3738,3783,3793,3759,3811,3732,3532,3562,154,158,530,261,264,670,688,192,257,168,262,230,503,447,593,263,165,156,171,161,474,231,174,157,169,561,170,2272,260,173,159,172,259,258,162,163,166,188,184,195,228,2592,179,205,196,193,232,203,209,247,210,194,181,206,248,204,186,189,178,241,187,208,197,200,180])).
% 59.38/59.41 cnf(3997,plain,
% 59.38/59.41 (P8(a16,x39971,x39971)),
% 59.38/59.41 inference(rename_variables,[],[3779])).
% 59.38/59.41 cnf(4001,plain,
% 59.38/59.41 (P1(x40011,x40012,x40012)),
% 59.38/59.41 inference(rename_variables,[],[3672])).
% 59.38/59.41 cnf(4002,plain,
% 59.38/59.41 (P10(x40021,x40022,x40022,x40021)),
% 59.38/59.41 inference(rename_variables,[],[3698])).
% 59.38/59.41 cnf(4004,plain,
% 59.38/59.41 (P8(f31(a16,a16,a16,a16,a16),f31(a16,a16,a16,a16,a16),f31(a16,a16,a16,a16,a16))),
% 59.38/59.41 inference(scs_inference,[],[3659,3690,3961,3984,3698,3933,3987,3992,3672,3928,3956,3983,4001,3763,3706,3566,3668,3714,3575,3839,3779,3944,3953,3980,3722,3702,3768,3785,3789,3815,3741,3708,3718,3716,3738,3783,3793,3797,3759,3811,3732,3532,3562,154,158,530,261,264,670,688,192,257,168,262,230,503,447,593,263,165,156,171,161,474,231,174,157,169,561,170,2272,260,173,159,172,259,258,162,163,166,188,184,195,228,2592,179,205,196,193,232,203,209,247,210,194,181,206,248,204,186,189,178,241,187,208,197,200,180,233,244])).
% 59.38/59.41 cnf(4006,plain,
% 59.38/59.41 (P1(x40061,x40062,x40062)),
% 59.38/59.41 inference(rename_variables,[],[3672])).
% 59.38/59.41 cnf(4008,plain,
% 59.38/59.41 (P8(a16,a16,f31(a16,a16,a16,a16,a16))),
% 59.38/59.41 inference(scs_inference,[],[3659,3690,3961,3984,3698,3933,3987,3992,3672,3928,3956,3983,4001,3763,3706,3566,3668,3714,3575,3839,3779,3944,3953,3980,3997,3722,3702,3768,3785,3789,3815,3741,3708,3718,3716,3738,3783,3793,3797,3759,3813,3811,3732,3532,3562,154,158,530,261,264,670,688,192,257,168,262,230,503,447,593,263,165,156,171,161,474,231,174,157,169,561,170,2272,260,173,159,172,259,258,162,163,166,188,184,195,228,2592,179,205,196,193,232,203,209,247,210,194,181,206,248,204,186,189,178,241,187,208,197,200,180,233,244,167])).
% 59.38/59.41 cnf(4009,plain,
% 59.38/59.41 (P8(a16,x40091,x40091)),
% 59.38/59.41 inference(rename_variables,[],[3779])).
% 59.38/59.41 cnf(4012,plain,
% 59.38/59.41 (P8(a16,x40121,x40121)),
% 59.38/59.41 inference(rename_variables,[],[3779])).
% 59.38/59.41 cnf(4017,plain,
% 59.38/59.41 (P10(x40171,x40172,x40172,x40171)),
% 59.38/59.41 inference(rename_variables,[],[3698])).
% 59.38/59.41 cnf(4022,plain,
% 59.38/59.41 (P8(f26(x40221,x40222),x40221,x40222)),
% 59.38/59.41 inference(scs_inference,[],[142,3659,3690,3961,3984,3698,3933,3987,3992,4002,4017,3672,3928,3956,3983,4001,4006,3763,3706,3550,3566,3668,3714,3575,3839,3585,3779,3944,3953,3980,3997,4009,4012,3722,3702,3768,3785,3789,3815,3741,3708,3718,3716,3738,3783,3793,3797,3759,3813,3811,3732,3532,3562,3941,303,154,158,530,261,264,670,688,192,257,168,262,230,503,447,593,263,165,156,171,161,474,231,174,157,169,561,170,2272,260,173,159,172,259,258,162,163,166,188,184,195,228,2592,179,205,196,193,232,203,209,247,210,194,181,206,248,204,186,189,178,241,187,208,197,200,180,233,244,167,214,212,211,164])).
% 59.38/59.41 cnf(4026,plain,
% 59.38/59.41 (~P3(a2,f26(a22,a21),a22,a21)),
% 59.38/59.41 inference(scs_inference,[],[142,3659,3690,3961,3984,3698,3933,3987,3992,4002,4017,3672,3928,3956,3983,4001,4006,3763,3706,3550,3566,3668,3714,3575,3839,3585,3779,3944,3953,3980,3997,4009,4012,3722,3702,3768,3785,3789,3815,3741,3708,3718,3716,3738,3783,3793,3797,3759,3813,3811,3732,3532,3562,3941,303,154,158,530,261,264,670,688,192,257,168,262,230,503,447,593,263,165,156,171,161,474,231,174,157,169,561,170,2272,260,173,159,172,259,258,162,163,166,188,184,195,228,2592,179,205,196,193,232,203,209,247,210,194,181,206,248,204,186,189,178,241,187,208,197,200,180,233,244,167,214,212,211,164,402])).
% 59.38/59.41 cnf(4028,plain,
% 59.38/59.41 (~P3(a2,f26(a22,a21),a21,a22)),
% 59.38/59.41 inference(scs_inference,[],[142,3659,3690,3961,3984,3698,3933,3987,3992,4002,4017,3672,3928,3956,3983,4001,4006,3763,3706,3550,3566,3668,3714,3575,3839,3585,3779,3944,3953,3980,3997,4009,4012,3722,3702,3768,3785,3789,3815,3741,3708,3718,3716,3738,3783,3793,3797,3759,3813,3811,3732,3532,3562,3941,303,154,158,530,261,264,670,688,192,257,168,262,230,503,447,593,263,165,156,171,161,474,231,174,157,169,561,170,2272,260,173,159,172,259,258,162,163,166,188,184,195,228,2592,179,205,196,193,232,203,209,247,210,194,181,206,248,204,186,189,178,241,187,208,197,200,180,233,244,167,214,212,211,164,402,1558])).
% 59.38/59.41 cnf(4074,plain,
% 59.38/59.41 (P8(f26(x40741,x40742),x40741,x40742)),
% 59.38/59.41 inference(rename_variables,[],[4022])).
% 59.38/59.41 cnf(4077,plain,
% 59.38/59.41 (P8(f26(x40771,x40772),x40771,x40772)),
% 59.38/59.41 inference(rename_variables,[],[4022])).
% 59.38/59.41 cnf(4080,plain,
% 59.38/59.41 (P8(f26(x40801,x40802),x40801,x40802)),
% 59.38/59.41 inference(rename_variables,[],[4022])).
% 59.38/59.41 cnf(4083,plain,
% 59.38/59.41 (P8(f26(x40831,x40832),x40831,x40832)),
% 59.38/59.41 inference(rename_variables,[],[4022])).
% 59.38/59.41 cnf(4086,plain,
% 59.38/59.41 (P8(f26(x40861,x40862),x40861,x40862)),
% 59.38/59.41 inference(rename_variables,[],[4022])).
% 59.38/59.41 cnf(4089,plain,
% 59.38/59.41 (P8(f26(x40891,x40892),x40891,x40892)),
% 59.38/59.41 inference(rename_variables,[],[4022])).
% 59.38/59.41 cnf(4092,plain,
% 59.38/59.41 (P8(f26(x40921,x40922),x40921,x40922)),
% 59.38/59.41 inference(rename_variables,[],[4022])).
% 59.38/59.41 cnf(4095,plain,
% 59.38/59.41 (P8(f26(x40951,x40952),x40951,x40952)),
% 59.38/59.42 inference(rename_variables,[],[4022])).
% 59.38/59.42 cnf(4098,plain,
% 59.38/59.42 (P8(f26(x40981,x40982),x40981,x40982)),
% 59.38/59.42 inference(rename_variables,[],[4022])).
% 59.38/59.42 cnf(4101,plain,
% 59.38/59.42 (P8(f26(x41011,x41012),x41011,x41012)),
% 59.38/59.42 inference(rename_variables,[],[4022])).
% 59.38/59.42 cnf(4104,plain,
% 59.38/59.42 (P8(f26(x41041,x41042),x41041,x41042)),
% 59.38/59.42 inference(rename_variables,[],[4022])).
% 59.38/59.42 cnf(4107,plain,
% 59.38/59.42 (P8(f26(x41071,x41072),x41071,x41072)),
% 59.38/59.42 inference(rename_variables,[],[4022])).
% 59.38/59.42 cnf(4110,plain,
% 59.38/59.42 (P8(f26(x41101,x41102),x41101,x41102)),
% 59.38/59.42 inference(rename_variables,[],[4022])).
% 59.38/59.42 cnf(4113,plain,
% 59.38/59.42 (P8(f26(x41131,x41132),x41131,x41132)),
% 59.38/59.42 inference(rename_variables,[],[4022])).
% 59.38/59.42 cnf(4116,plain,
% 59.38/59.42 (P8(f26(x41161,x41162),x41161,x41162)),
% 59.38/59.42 inference(rename_variables,[],[4022])).
% 59.38/59.42 cnf(4119,plain,
% 59.38/59.42 (P8(f26(x41191,x41192),x41191,x41192)),
% 59.38/59.42 inference(rename_variables,[],[4022])).
% 59.38/59.42 cnf(4122,plain,
% 59.38/59.42 (P8(f26(x41221,x41222),x41221,x41222)),
% 59.38/59.42 inference(rename_variables,[],[4022])).
% 59.38/59.42 cnf(4125,plain,
% 59.38/59.42 (P8(f26(x41251,x41252),x41251,x41252)),
% 59.38/59.42 inference(rename_variables,[],[4022])).
% 59.38/59.42 cnf(4128,plain,
% 59.38/59.42 (P8(f26(x41281,x41282),x41281,x41282)),
% 59.38/59.42 inference(rename_variables,[],[4022])).
% 59.38/59.42 cnf(4131,plain,
% 59.38/59.42 (P8(f26(x41311,x41312),x41311,x41312)),
% 59.38/59.42 inference(rename_variables,[],[4022])).
% 59.38/59.42 cnf(4134,plain,
% 59.38/59.42 (P8(f26(x41341,x41342),x41341,x41342)),
% 59.38/59.42 inference(rename_variables,[],[4022])).
% 59.38/59.42 cnf(4137,plain,
% 59.38/59.42 (P8(f26(x41371,x41372),x41371,x41372)),
% 59.38/59.42 inference(rename_variables,[],[4022])).
% 59.38/59.42 cnf(4140,plain,
% 59.38/59.42 (P8(f26(x41401,x41402),x41401,x41402)),
% 59.38/59.42 inference(rename_variables,[],[4022])).
% 59.38/59.42 cnf(4142,plain,
% 59.38/59.42 (P8(f26(a2,a2),a16,a16)),
% 59.38/59.42 inference(scs_inference,[],[4022,4074,4077,4080,4083,4086,4089,4092,4095,4098,4101,4104,4107,4110,4113,4116,4119,4122,4125,4128,4131,4134,4137,4140,412,445,767,780,782,826,2528,2560,2576,2608,2768,2784,2800,2960,2976,3056,3072,2017,3852,3853,3854,3855,3856,1977])).
% 59.38/59.42 cnf(4143,plain,
% 59.38/59.42 (P8(f26(x41431,x41432),x41431,x41432)),
% 59.38/59.42 inference(rename_variables,[],[4022])).
% 59.38/59.42 cnf(4149,plain,
% 59.38/59.42 (P1(f26(x41491,x41492),x41491,x41492)),
% 59.38/59.42 inference(scs_inference,[],[3971,4022,4074,4077,4080,4083,4086,4089,4092,4095,4098,4101,4104,4107,4110,4113,4116,4119,4122,4125,4128,4131,4134,4137,4140,4143,3973,412,445,767,780,782,826,2528,2560,2576,2608,2768,2784,2800,2960,2976,3056,3072,2017,3852,3853,3854,3855,3856,1977,797,530,158])).
% 59.38/59.42 cnf(4158,plain,
% 59.38/59.42 (P8(f26(x41581,x41582),x41581,x41582)),
% 59.38/59.42 inference(rename_variables,[],[4022])).
% 59.38/59.42 cnf(4164,plain,
% 59.38/59.42 (P10(x41641,x41641,a16,a16)),
% 59.38/59.42 inference(scs_inference,[],[3937,3971,3925,3977,4022,4074,4077,4080,4083,4086,4089,4092,4095,4098,4101,4104,4107,4110,4113,4116,4119,4122,4125,4128,4131,4134,4137,4140,4143,3973,412,445,767,780,782,826,2528,2560,2576,2608,2768,2784,2800,2960,2976,3056,3072,2017,3852,3853,3854,3855,3856,1977,797,530,158,670,648,192,815,262,230,168])).
% 59.38/59.42 cnf(4172,plain,
% 59.38/59.42 (P9(a16,x41721,a16,x41721,x41721,x41721,x41721,x41721)),
% 59.38/59.42 inference(scs_inference,[],[3937,3971,3925,3666,3977,4022,4074,4077,4080,4083,4086,4089,4092,4095,4098,4101,4104,4107,4110,4113,4116,4119,4122,4125,4128,4131,4134,4137,4140,4143,3932,3973,412,445,767,780,782,826,2528,2560,2576,2608,2768,2784,2800,2960,2976,3056,3072,2017,3852,3853,3854,3855,3856,1977,797,530,158,670,648,192,815,262,230,168,688,165,261,264])).
% 59.38/59.42 cnf(4174,plain,
% 59.38/59.42 (P9(x41741,a16,x41741,x41741,a16,x41741,x41741,x41741)),
% 59.38/59.42 inference(scs_inference,[],[3937,3971,3925,3666,3977,4022,4074,4077,4080,4083,4086,4089,4092,4095,4098,4101,4104,4107,4110,4113,4116,4119,4122,4125,4128,4131,4134,4137,4140,4143,3932,3973,412,445,767,780,782,826,2528,2560,2576,2608,2768,2784,2800,2960,2976,3056,3072,2017,3852,3853,3854,3855,3856,1977,797,530,158,670,648,192,815,262,230,168,688,165,261,264,263])).
% 59.38/59.42 cnf(4186,plain,
% 59.38/59.42 (P3(a16,a2,a17,a18)),
% 59.38/59.42 inference(scs_inference,[],[3937,3971,3921,3925,3666,3907,3977,4022,4074,4077,4080,4083,4086,4089,4092,4095,4098,4101,4104,4107,4110,4113,4116,4119,4122,4125,4128,4131,4134,4137,4140,4143,3909,3932,3973,412,445,767,780,782,826,2528,2560,2576,2608,2768,2784,2800,2960,2976,3056,3072,2017,3852,3853,3854,3855,3856,1977,797,530,158,670,648,192,815,262,230,168,688,165,261,264,263,447,257,175,503,176,171])).
% 59.38/59.42 cnf(4188,plain,
% 59.38/59.42 (P6(x41881,x41882,x41881,x41881)),
% 59.38/59.42 inference(scs_inference,[],[3982,3937,3971,3921,3925,3666,3907,3977,4022,4074,4077,4080,4083,4086,4089,4092,4095,4098,4101,4104,4107,4110,4113,4116,4119,4122,4125,4128,4131,4134,4137,4140,4143,3909,3932,3973,412,445,767,780,782,826,2528,2560,2576,2608,2768,2784,2800,2960,2976,3056,3072,2017,3852,3853,3854,3855,3856,1977,797,530,158,670,648,192,815,262,230,168,688,165,261,264,263,447,257,175,503,176,171,174])).
% 59.38/59.42 cnf(4192,plain,
% 59.38/59.42 (P5(f26(x41921,x41922),x41921,f26(x41921,x41922),x41922)),
% 59.38/59.42 inference(scs_inference,[],[3982,3937,3971,3921,3925,3666,3907,3977,4022,4074,4077,4080,4083,4086,4089,4092,4095,4098,4101,4104,4107,4110,4113,4116,4119,4122,4125,4128,4131,4134,4137,4140,4143,4158,3909,3932,3973,3969,412,445,767,780,782,826,2528,2560,2576,2608,2768,2784,2800,2960,2976,3056,3072,2017,3852,3853,3854,3855,3856,1977,797,530,158,670,648,192,815,262,230,168,688,165,261,264,263,447,257,175,503,176,171,174,169,161])).
% 59.38/59.42 cnf(4200,plain,
% 59.38/59.42 (P1(x42001,x42001,x42002)),
% 59.38/59.42 inference(scs_inference,[],[3982,3889,3937,3971,3921,3925,3666,3907,3977,4022,4074,4077,4080,4083,4086,4089,4092,4095,4098,4101,4104,4107,4110,4113,4116,4119,4122,4125,4128,4131,4134,4137,4140,4143,4158,3819,3909,3932,3973,3969,412,445,767,780,782,826,2528,2560,2576,2608,2768,2784,2800,2960,2976,3056,3072,2017,3852,3853,3854,3855,3856,1977,797,530,158,670,648,192,815,262,230,168,688,165,261,264,263,447,257,175,503,176,171,174,169,161,593,156,474,157])).
% 59.38/59.42 cnf(4202,plain,
% 59.38/59.42 (P6(x42021,x42021,x42021,x42022)),
% 59.38/59.42 inference(scs_inference,[],[3982,3889,3937,3971,3921,3925,3666,3907,3977,4022,4074,4077,4080,4083,4086,4089,4092,4095,4098,4101,4104,4107,4110,4113,4116,4119,4122,4125,4128,4131,4134,4137,4140,4143,4158,3819,3909,3932,3973,3969,412,445,767,780,782,826,2528,2560,2576,2608,2768,2784,2800,2960,2976,3056,3072,2017,3852,3853,3854,3855,3856,1977,797,530,158,670,648,192,815,262,230,168,688,165,261,264,263,447,257,175,503,176,171,174,169,161,593,156,474,157,2272])).
% 59.38/59.42 cnf(4204,plain,
% 59.38/59.42 (P4(a16,x42041,x42041,x42041,x42041,x42041,a16,x42041)),
% 59.38/59.42 inference(scs_inference,[],[3982,3889,3937,3971,3893,3921,3925,3666,3907,3977,4022,4074,4077,4080,4083,4086,4089,4092,4095,4098,4101,4104,4107,4110,4113,4116,4119,4122,4125,4128,4131,4134,4137,4140,4143,4158,3819,3909,3932,3973,3969,412,445,767,780,782,826,2528,2560,2576,2608,2768,2784,2800,2960,2976,3056,3072,2017,3852,3853,3854,3855,3856,1977,797,530,158,670,648,192,815,262,230,168,688,165,261,264,263,447,257,175,503,176,171,174,169,161,593,156,474,157,2272,231])).
% 59.38/59.42 cnf(4210,plain,
% 59.38/59.42 (P4(x42101,x42102,x42102,x42101,x42103,x42104,x42103,x42104)),
% 59.38/59.42 inference(scs_inference,[],[3877,3982,3889,3937,3971,3893,3921,3925,3666,3907,3975,3977,4022,4074,4077,4080,4083,4086,4089,4092,4095,4098,4101,4104,4107,4110,4113,4116,4119,4122,4125,4128,4131,4134,4137,4140,4143,4158,3819,3909,3932,3973,3969,412,445,767,780,782,826,2528,2560,2576,2608,2768,2784,2800,2960,2976,3056,3072,2017,3852,3853,3854,3855,3856,1977,797,530,158,670,648,192,815,262,230,168,688,165,261,264,263,447,257,175,503,176,171,174,169,161,593,156,474,157,2272,231,561,170,260])).
% 59.38/59.42 cnf(4212,plain,
% 59.38/59.42 (P5(a16,x42121,x42121,a16)),
% 59.38/59.42 inference(scs_inference,[],[3877,3982,3889,3937,3971,3893,3921,3925,3666,3907,3975,3977,4022,4074,4077,4080,4083,4086,4089,4092,4095,4098,4101,4104,4107,4110,4113,4116,4119,4122,4125,4128,4131,4134,4137,4140,4143,4158,3819,3909,3932,3973,3969,412,445,767,780,782,826,2528,2560,2576,2608,2768,2784,2800,2960,2976,3056,3072,2017,3852,3853,3854,3855,3856,1977,797,530,158,670,648,192,815,262,230,168,688,165,261,264,263,447,257,175,503,176,171,174,169,161,593,156,474,157,2272,231,561,170,260,173])).
% 59.38/59.42 cnf(4216,plain,
% 59.38/59.42 (P8(f26(x42161,x42162),x42162,x42161)),
% 59.38/59.42 inference(scs_inference,[],[3877,3982,3889,3937,3971,3893,3921,3925,3666,3907,3975,3977,4022,4074,4077,4080,4083,4086,4089,4092,4095,4098,4101,4104,4107,4110,4113,4116,4119,4122,4125,4128,4131,4134,4137,4140,4143,4158,3819,3909,3932,3973,3969,412,445,767,780,782,826,2528,2560,2576,2608,2768,2784,2800,2960,2976,3056,3072,2017,3852,3853,3854,3855,3856,1977,797,530,158,670,648,192,815,262,230,168,688,165,261,264,263,447,257,175,503,176,171,174,169,161,593,156,474,157,2272,231,561,170,260,173,259,159])).
% 59.38/59.42 cnf(4218,plain,
% 59.38/59.42 (P4(x42181,x42182,x42183,x42184,x42181,x42182,x42184,x42183)),
% 59.38/59.42 inference(scs_inference,[],[3877,3982,3889,3937,3971,3893,3921,3925,3666,3907,3975,3977,4022,4074,4077,4080,4083,4086,4089,4092,4095,4098,4101,4104,4107,4110,4113,4116,4119,4122,4125,4128,4131,4134,4137,4140,4143,4158,3819,3909,3932,3973,3969,412,445,767,780,782,826,2528,2560,2576,2608,2768,2784,2800,2960,2976,3056,3072,2017,3852,3853,3854,3855,3856,1977,797,530,158,670,648,192,815,262,230,168,688,165,261,264,263,447,257,175,503,176,171,174,169,161,593,156,474,157,2272,231,561,170,260,173,259,159,258])).
% 59.38/59.42 cnf(4220,plain,
% 59.38/59.42 (P5(a2,a16,a16,a16)),
% 59.38/59.42 inference(scs_inference,[],[3877,3982,3889,3937,3971,3893,3921,3925,3666,3907,3943,3975,3977,4022,4074,4077,4080,4083,4086,4089,4092,4095,4098,4101,4104,4107,4110,4113,4116,4119,4122,4125,4128,4131,4134,4137,4140,4143,4158,3819,3909,3932,3973,3969,412,445,767,780,782,826,2528,2560,2576,2608,2768,2784,2800,2960,2976,3056,3072,2017,3852,3853,3854,3855,3856,1977,797,530,158,670,648,192,815,262,230,168,688,165,261,264,263,447,257,175,503,176,171,174,169,161,593,156,474,157,2272,231,561,170,260,173,259,159,258,172])).
% 59.38/59.42 cnf(4222,plain,
% 59.38/59.42 (P10(a16,f29(x42221,x42221,x42221,x42221,a16,a16),x42221,x42221)),
% 59.38/59.42 inference(scs_inference,[],[3877,3982,3889,3937,3971,3893,3921,3925,3666,3907,3943,3975,3977,4022,4074,4077,4080,4083,4086,4089,4092,4095,4098,4101,4104,4107,4110,4113,4116,4119,4122,4125,4128,4131,4134,4137,4140,4143,4158,3819,3909,3958,3932,3973,3969,412,445,767,780,782,826,2528,2560,2576,2608,2768,2784,2800,2960,2976,3056,3072,2017,3852,3853,3854,3855,3856,1977,797,530,158,670,648,192,815,262,230,168,688,165,261,264,263,447,257,175,503,176,171,174,169,161,593,156,474,157,2272,231,561,170,260,173,259,159,258,172,245])).
% 59.38/59.42 cnf(4224,plain,
% 59.38/59.42 (P4(x42241,x42242,x42243,x42244,x42242,x42241,x42243,x42244)),
% 59.38/59.42 inference(rename_variables,[],[3877])).
% 59.38/59.42 cnf(4228,plain,
% 59.38/59.42 (P9(a2,a16,a16,a16,a2,a16,a16,a16)),
% 59.38/59.42 inference(scs_inference,[],[3877,3982,3889,3891,3937,3971,3893,3921,3925,3666,3907,3927,3943,3975,3977,4022,4074,4077,4080,4083,4086,4089,4092,4095,4098,4101,4104,4107,4110,4113,4116,4119,4122,4125,4128,4131,4134,4137,4140,4143,4158,3819,3909,3958,3932,3973,3969,412,445,767,780,782,826,2528,2560,2576,2608,2768,2784,2800,2960,2976,3056,3072,2017,3852,3853,3854,3855,3856,1977,797,530,158,670,648,192,815,262,230,168,688,165,261,264,263,447,257,175,503,176,171,174,169,161,593,156,474,157,2272,231,561,170,260,173,259,159,258,172,245,205,228])).
% 59.38/59.42 cnf(4231,plain,
% 59.38/59.42 (P10(x42311,x42312,x42312,x42311)),
% 59.38/59.42 inference(rename_variables,[],[3698])).
% 59.38/59.42 cnf(4232,plain,
% 59.38/59.42 (P8(f26(x42321,x42322),x42321,x42322)),
% 59.38/59.42 inference(rename_variables,[],[4022])).
% 59.38/59.42 cnf(4235,plain,
% 59.38/59.42 (P1(x42351,x42352,x42351)),
% 59.38/59.42 inference(rename_variables,[],[3889])).
% 59.38/59.42 cnf(4241,plain,
% 59.38/59.42 (P4(a16,a16,a16,a16,a2,a16,a2,a2)),
% 59.38/59.42 inference(scs_inference,[],[3877,3982,3889,3891,3937,3971,3893,3921,3925,3666,3907,3927,3943,3975,3977,4022,4074,4077,4080,4083,4086,4089,4092,4095,4098,4101,4104,4107,4110,4113,4116,4119,4122,4125,4128,4131,4134,4137,4140,4143,4158,3819,3909,3958,3932,3973,3969,3698,412,445,767,780,782,826,2528,2560,2576,2608,2768,2784,2800,2960,2976,3056,3072,2017,3852,3853,3854,3855,3856,1977,797,530,158,670,648,192,815,262,230,168,688,165,261,264,263,447,257,175,503,176,171,174,169,161,593,156,474,157,2272,231,561,170,260,173,259,159,258,172,245,205,228,2592,202,195,183,232])).
% 59.38/59.42 cnf(4246,plain,
% 59.38/59.42 (P5(a16,x42461,a16,x42461)),
% 59.38/59.42 inference(rename_variables,[],[3893])).
% 59.38/59.42 cnf(4248,plain,
% 59.38/59.42 (P10(f29(a16,a16,a16,a16,a2,a2),a2,a16,a16)),
% 59.38/59.42 inference(scs_inference,[],[3877,3982,3889,3891,3937,3971,3893,3921,3925,3666,3907,3927,3943,3975,3977,4022,4074,4077,4080,4083,4086,4089,4092,4095,4098,4101,4104,4107,4110,4113,4116,4119,4122,4125,4128,4131,4134,4137,4140,4143,4158,3819,3909,3958,3932,3973,3969,3698,412,445,767,780,782,826,2528,2560,2576,2608,2768,2784,2800,2960,2976,3056,3072,2017,3852,3853,3854,3855,3856,1977,797,530,158,670,648,192,815,262,230,168,688,165,261,264,263,447,257,175,503,176,171,174,169,161,593,156,474,157,2272,231,561,170,260,173,259,159,258,172,245,205,228,2592,202,195,183,232,194,193,210])).
% 59.38/59.42 cnf(4259,plain,
% 59.38/59.42 (P10(f31(a2,a16,a2,a2,a2),a2,a2,a16)),
% 59.38/59.42 inference(scs_inference,[],[3877,3982,3889,4235,3891,3937,3971,3893,3921,3925,3666,3674,3907,3927,3943,3975,3977,4022,4074,4077,4080,4083,4086,4089,4092,4095,4098,4101,4104,4107,4110,4113,4116,4119,4122,4125,4128,4131,4134,4137,4140,4143,4158,3819,3909,3958,3932,3973,3969,3577,3698,3815,3839,412,445,767,780,782,826,2528,2560,2576,2608,2768,2784,2800,2960,2976,3056,3072,2017,3852,3853,3854,3855,3856,1977,797,530,158,670,648,192,815,262,230,168,688,165,261,264,263,447,257,175,503,176,171,174,169,161,593,156,474,157,2272,231,561,170,260,173,259,159,258,172,245,205,228,2592,202,195,183,232,194,193,210,209,196,203,268,206])).
% 59.38/59.42 cnf(4266,plain,
% 59.38/59.42 (P5(a2,a15,a15,a2)),
% 59.38/59.42 inference(scs_inference,[],[3877,3982,3889,4235,3891,3937,3971,3893,4246,3921,3925,3666,3674,3907,3927,3943,3975,3977,4022,4074,4077,4080,4083,4086,4089,4092,4095,4098,4101,4104,4107,4110,4113,4116,4119,4122,4125,4128,4131,4134,4137,4140,4143,4158,3819,3909,3958,3932,3973,3969,3577,3698,3815,3839,412,445,767,780,782,826,2528,2560,2576,2608,2768,2784,2800,2960,2976,3056,3072,2017,3852,3853,3854,3855,3856,1977,797,530,158,670,648,192,815,262,230,168,688,165,261,264,263,447,257,175,503,176,171,174,169,161,593,156,474,157,2272,231,561,170,260,173,259,159,258,172,245,205,228,2592,202,195,183,232,194,193,210,209,196,203,268,206,181,182,248])).
% 59.38/59.42 cnf(4268,plain,
% 59.38/59.42 (P3(a2,a2,a2,a2)),
% 59.38/59.42 inference(scs_inference,[],[3877,3982,3889,4235,3891,3937,3971,3893,4246,3921,3925,3666,3674,3907,3927,3943,3975,3977,4022,4074,4077,4080,4083,4086,4089,4092,4095,4098,4101,4104,4107,4110,4113,4116,4119,4122,4125,4128,4131,4134,4137,4140,4143,4158,3819,3909,3958,3932,3973,3969,3577,3698,3815,3839,412,445,767,780,782,826,2528,2560,2576,2608,2768,2784,2800,2960,2976,3056,3072,2017,3852,3853,3854,3855,3856,1977,797,530,158,670,648,192,815,262,230,168,688,165,261,264,263,447,257,175,503,176,171,174,169,161,593,156,474,157,2272,231,561,170,260,173,259,159,258,172,245,205,228,2592,202,195,183,232,194,193,210,209,196,203,268,206,181,182,248,186])).
% 59.38/59.42 cnf(4270,plain,
% 59.38/59.42 (P2(a2,a2,a2,a2)),
% 59.38/59.42 inference(scs_inference,[],[3877,3982,3889,4235,3891,3937,3971,3893,4246,3921,3925,3666,3674,3907,3927,3943,3975,3977,4022,4074,4077,4080,4083,4086,4089,4092,4095,4098,4101,4104,4107,4110,4113,4116,4119,4122,4125,4128,4131,4134,4137,4140,4143,4158,3819,3909,3958,3932,3973,3969,3577,3698,3815,3839,412,445,767,780,782,826,2528,2560,2576,2608,2768,2784,2800,2960,2976,3056,3072,2017,3852,3853,3854,3855,3856,1977,797,530,158,670,648,192,815,262,230,168,688,165,261,264,263,447,257,175,503,176,171,174,169,161,593,156,474,157,2272,231,561,170,260,173,259,159,258,172,245,205,228,2592,202,195,183,232,194,193,210,209,196,203,268,206,181,182,248,186,189])).
% 59.38/59.42 cnf(4272,plain,
% 59.38/59.42 (P5(f12(a16,a16,a2,x42721,x42721),x42721,f12(a16,a16,a2,x42721,x42721),x42721)),
% 59.38/59.42 inference(scs_inference,[],[3877,3982,3889,4235,3891,3937,3971,3893,4246,3921,3925,3666,3674,3907,3927,3943,3975,3977,4022,4074,4077,4080,4083,4086,4089,4092,4095,4098,4101,4104,4107,4110,4113,4116,4119,4122,4125,4128,4131,4134,4137,4140,4143,4158,3819,3909,3958,3955,3932,3973,3969,3577,3698,3815,3779,3839,412,445,767,780,782,826,2528,2560,2576,2608,2768,2784,2800,2960,2976,3056,3072,2017,3852,3853,3854,3855,3856,1977,797,530,158,670,648,192,815,262,230,168,688,165,261,264,263,447,257,175,503,176,171,174,169,161,593,156,474,157,2272,231,561,170,260,173,259,159,258,172,245,205,228,2592,202,195,183,232,194,193,210,209,196,203,268,206,181,182,248,186,189,178])).
% 59.38/59.42 cnf(4275,plain,
% 59.38/59.42 (P5(a2,a2,a2,f31(a2,a16,a2,a2,a2))),
% 59.38/59.42 inference(scs_inference,[],[3877,3982,3889,4235,3891,3937,3971,3893,4246,3921,3925,3666,3674,3907,3927,3943,3975,3977,4022,4074,4077,4080,4083,4086,4089,4092,4095,4098,4101,4104,4107,4110,4113,4116,4119,4122,4125,4128,4131,4134,4137,4140,4143,4158,3819,3909,3958,3955,3932,3973,3969,3577,3698,3815,3779,3839,412,445,767,780,782,826,2528,2560,2576,2608,2768,2784,2800,2960,2976,3056,3072,2017,3852,3853,3854,3855,3856,1977,797,530,158,670,648,192,815,262,230,168,688,165,261,264,263,447,257,175,503,176,171,174,169,161,593,156,474,157,2272,231,561,170,260,173,259,159,258,172,245,205,228,2592,202,195,183,232,194,193,210,209,196,203,268,206,181,182,248,186,189,178,204])).
% 59.38/59.42 cnf(4277,plain,
% 59.38/59.42 (P3(a16,a2,a16,a2)),
% 59.38/59.42 inference(scs_inference,[],[3877,4224,3982,3889,4235,3891,3937,3971,3893,4246,3921,3925,3666,3674,3907,3927,3943,3975,3977,4022,4074,4077,4080,4083,4086,4089,4092,4095,4098,4101,4104,4107,4110,4113,4116,4119,4122,4125,4128,4131,4134,4137,4140,4143,4158,3819,3909,3958,3955,3932,3973,3969,3577,3698,3815,3779,3839,412,445,767,780,782,826,2528,2560,2576,2608,2768,2784,2800,2960,2976,3056,3072,2017,3852,3853,3854,3855,3856,1977,797,530,158,670,648,192,815,262,230,168,688,165,261,264,263,447,257,175,503,176,171,174,169,161,593,156,474,157,2272,231,561,170,260,173,259,159,258,172,245,205,228,2592,202,195,183,232,194,193,210,209,196,203,268,206,181,182,248,186,189,178,204,246])).
% 59.38/59.42 cnf(4278,plain,
% 59.38/59.42 (P4(x42781,x42782,x42783,x42784,x42782,x42781,x42783,x42784)),
% 59.38/59.42 inference(rename_variables,[],[3877])).
% 59.38/59.42 cnf(4280,plain,
% 59.38/59.42 (P6(a15,a15,a1,a2)),
% 59.38/59.42 inference(scs_inference,[],[142,3877,4224,3911,3982,3889,4235,3891,3937,3971,3893,4246,3921,3925,3666,3674,3907,3927,3943,3975,3977,4022,4074,4077,4080,4083,4086,4089,4092,4095,4098,4101,4104,4107,4110,4113,4116,4119,4122,4125,4128,4131,4134,4137,4140,4143,4158,3819,3909,3958,3955,3932,3973,3969,3577,3698,3815,3779,3839,412,445,767,780,782,826,2528,2560,2576,2608,2768,2784,2800,2960,2976,3056,3072,2017,3852,3853,3854,3855,3856,1977,797,530,158,670,648,192,815,262,230,168,688,165,261,264,263,447,257,175,503,176,171,174,169,161,593,156,474,157,2272,231,561,170,260,173,259,159,258,172,245,205,228,2592,202,195,183,232,194,193,210,209,196,203,268,206,181,182,248,186,189,178,204,246,241])).
% 59.38/59.42 cnf(4291,plain,
% 59.38/59.42 (P8(f6(a2,a2,a2),a2,a2)),
% 59.38/59.42 inference(scs_inference,[],[142,3877,4224,3911,3982,3889,4235,3891,3937,3971,3893,4246,3921,3925,3666,3674,3907,3923,3927,3943,3975,3977,4022,4074,4077,4080,4083,4086,4089,4092,4095,4098,4101,4104,4107,4110,4113,4116,4119,4122,4125,4128,4131,4134,4137,4140,4143,4158,4232,3819,4028,3909,3958,3955,3932,3973,3969,3577,3554,3698,4231,3815,3779,3839,412,445,767,780,782,826,2528,2560,2576,2608,2768,2784,2800,2960,2976,3056,3072,2017,3852,3853,3854,3855,3856,1977,797,530,158,670,648,192,815,262,230,168,688,165,261,264,263,447,257,175,503,176,171,174,169,161,593,156,474,157,2272,231,561,170,260,173,259,159,258,172,245,205,228,2592,202,195,183,232,194,193,210,209,196,203,268,206,181,182,248,186,189,178,204,246,241,187,208,197,191])).
% 59.38/59.42 cnf(4298,plain,
% 59.38/59.42 (P5(x42981,x42981,x42981,x42981)),
% 59.38/59.42 inference(scs_inference,[],[142,3877,4224,4278,3911,3982,3889,4235,3891,3937,3971,3893,4246,3921,3925,3666,3674,3907,3923,3927,3943,3975,3977,4022,4074,4077,4080,4083,4086,4089,4092,4095,4098,4101,4104,4107,4110,4113,4116,4119,4122,4125,4128,4131,4134,4137,4140,4143,4158,4232,3819,4028,3909,3958,3955,3932,3973,3969,3577,3554,3698,4231,3672,3815,3779,3839,412,445,767,780,782,826,2528,2560,2576,2608,2768,2784,2800,2960,2976,3056,3072,2017,3852,3853,3854,3855,3856,1977,797,530,158,670,648,192,815,262,230,168,688,165,261,264,263,447,257,175,503,176,171,174,169,161,593,156,474,157,2272,231,561,170,260,173,259,159,258,172,245,205,228,2592,202,195,183,232,194,193,210,209,196,203,268,206,181,182,248,186,189,178,204,246,241,187,208,197,191,214,256])).
% 59.38/59.42 cnf(4335,plain,
% 59.38/59.42 (P5(f26(x43351,x43352),x43351,f26(x43351,x43352),x43352)),
% 59.38/59.42 inference(rename_variables,[],[4192])).
% 59.38/59.42 cnf(4338,plain,
% 59.38/59.42 (P5(f26(x43381,x43382),x43381,f26(x43381,x43382),x43382)),
% 59.38/59.42 inference(rename_variables,[],[4192])).
% 59.38/59.42 cnf(4341,plain,
% 59.38/59.42 (P8(f26(x43411,x43412),x43412,x43411)),
% 59.38/59.42 inference(rename_variables,[],[4216])).
% 59.38/59.42 cnf(4344,plain,
% 59.38/59.42 (P8(f26(x43441,x43442),x43442,x43441)),
% 59.38/59.42 inference(rename_variables,[],[4216])).
% 59.38/59.42 cnf(4347,plain,
% 59.38/59.42 (P8(f26(x43471,x43472),x43472,x43471)),
% 59.38/59.42 inference(rename_variables,[],[4216])).
% 59.38/59.42 cnf(4350,plain,
% 59.38/59.42 (P8(f26(x43501,x43502),x43502,x43501)),
% 59.38/59.42 inference(rename_variables,[],[4216])).
% 59.38/59.42 cnf(4353,plain,
% 59.38/59.42 (P8(f29(x43531,x43531,x43531,x43531,a16,a16),x43531,x43531)),
% 59.38/59.42 inference(rename_variables,[],[3989])).
% 59.38/59.42 cnf(4359,plain,
% 59.38/59.42 (P8(f26(x43591,x43592),x43592,x43591)),
% 59.38/59.42 inference(rename_variables,[],[4216])).
% 59.38/59.42 cnf(4362,plain,
% 59.38/59.42 (P8(f26(x43621,x43622),x43622,x43621)),
% 59.38/59.42 inference(rename_variables,[],[4216])).
% 59.38/59.42 cnf(4365,plain,
% 59.38/59.42 (P8(f26(x43651,x43652),x43652,x43651)),
% 59.38/59.42 inference(rename_variables,[],[4216])).
% 59.38/59.42 cnf(4368,plain,
% 59.38/59.42 (P8(f29(x43681,x43681,x43681,x43681,a16,a16),x43681,x43681)),
% 59.38/59.42 inference(rename_variables,[],[3989])).
% 59.38/59.42 cnf(4371,plain,
% 59.38/59.42 (P8(f26(x43711,x43712),x43712,x43711)),
% 59.38/59.42 inference(rename_variables,[],[4216])).
% 59.38/59.42 cnf(4374,plain,
% 59.38/59.42 (P8(f26(x43741,x43742),x43742,x43741)),
% 59.38/59.42 inference(rename_variables,[],[4216])).
% 59.38/59.42 cnf(4377,plain,
% 59.38/59.42 (P8(f26(x43771,x43772),x43772,x43771)),
% 59.38/59.42 inference(rename_variables,[],[4216])).
% 59.38/59.42 cnf(4380,plain,
% 59.38/59.42 (P8(f26(x43801,x43802),x43802,x43801)),
% 59.38/59.42 inference(rename_variables,[],[4216])).
% 59.38/59.42 cnf(4382,plain,
% 59.38/59.42 (P1(f26(x43821,x43822),x43822,x43821)),
% 59.38/59.42 inference(scs_inference,[],[4192,4335,4216,4341,4344,4347,4350,4359,4362,4365,4371,4374,4377,4380,3989,4353,4272,742,855,3056,2608,2528,2768,1977,672,2752,2976,2800,2017,2784,2560,3072,2960,158])).
% 59.38/59.42 cnf(4385,plain,
% 59.38/59.42 (P8(f26(x43851,x43852),x43852,x43851)),
% 59.38/59.42 inference(rename_variables,[],[4216])).
% 59.38/59.42 cnf(4389,plain,
% 59.38/59.42 (P9(x43891,x43891,x43891,a16,x43891,x43891,a16,x43891)),
% 59.38/59.42 inference(scs_inference,[],[4174,4192,4335,4216,4341,4344,4347,4350,4359,4362,4365,4371,4374,4377,4380,3989,4353,4272,4275,742,855,3056,2608,2528,2768,1977,672,2752,2976,2800,2017,2784,2560,3072,2960,158,2544,797,262])).
% 59.38/59.42 cnf(4391,plain,
% 59.38/59.42 (P4(x43911,x43911,x43912,x43913,a16,a16,x43912,x43913)),
% 59.38/59.42 inference(scs_inference,[],[4174,4164,4192,4335,4216,4341,4344,4347,4350,4359,4362,4365,4371,4374,4377,4380,3989,4353,4272,4275,742,855,3056,2608,2528,2768,1977,672,2752,2976,2800,2017,2784,2560,3072,2960,158,2544,797,262,230])).
% 59.38/59.42 cnf(4406,plain,
% 59.38/59.42 (P9(x44061,a16,a16,x44061,x44061,x44061,x44061,x44061)),
% 59.38/59.42 inference(scs_inference,[],[4298,4172,4174,4164,4270,4192,4335,4216,4341,4344,4347,4350,4359,4362,4365,4371,4374,4377,4380,3989,4353,4368,4272,4275,742,855,3056,2608,2528,2768,1977,672,2752,2976,2800,2017,2784,2560,3072,2960,158,2544,797,262,230,670,530,261,192,815,503,264])).
% 59.38/59.42 cnf(4420,plain,
% 59.38/59.42 (P3(a17,a18,a2,a16)),
% 59.38/59.42 inference(scs_inference,[],[4298,4210,4172,4174,4164,3757,3986,4270,4192,4335,4216,4341,4344,4347,4350,4359,4362,4365,4371,4374,4377,4380,3989,4353,4368,4272,4248,4275,742,855,3056,2608,2528,2768,1977,672,2752,2976,2800,2017,2784,2560,3072,2960,158,2544,797,262,230,670,530,261,192,815,503,264,688,168,447,257,263,474,171])).
% 59.38/59.42 cnf(4422,plain,
% 59.38/59.42 (P6(x44221,x44221,x44222,x44221)),
% 59.38/59.42 inference(scs_inference,[],[4298,4188,4210,4172,4174,4164,3757,3986,4270,4192,4335,4216,4341,4344,4347,4350,4359,4362,4365,4371,4374,4377,4380,3989,4353,4368,4272,4248,4275,742,855,3056,2608,2528,2768,1977,672,2752,2976,2800,2017,2784,2560,3072,2960,158,2544,797,262,230,670,530,261,192,815,503,264,688,168,447,257,263,474,171,175])).
% 59.38/59.42 cnf(4424,plain,
% 59.38/59.42 (P1(x44241,f26(x44241,x44242),x44242)),
% 59.38/59.42 inference(scs_inference,[],[4298,4188,4210,4172,4174,4164,3757,3986,4270,4192,4335,4149,4216,4341,4344,4347,4350,4359,4362,4365,4371,4374,4377,4380,3989,4353,4368,4272,4248,4275,742,855,3056,2608,2528,2768,1977,672,2752,2976,2800,2017,2784,2560,3072,2960,158,2544,797,262,230,670,530,261,192,815,503,264,688,168,447,257,263,474,171,175,156])).
% 59.38/59.42 cnf(4426,plain,
% 59.38/59.42 (P5(f26(x44261,x44262),x44262,f26(x44261,x44262),x44261)),
% 59.38/59.42 inference(scs_inference,[],[4298,4188,4210,4172,4174,4164,3757,3986,4270,4192,4335,4149,4216,4341,4344,4347,4350,4359,4362,4365,4371,4374,4377,4380,4385,3989,4353,4368,4272,4248,4275,742,855,3056,2608,2528,2768,1977,672,2752,2976,2800,2017,2784,2560,3072,2960,158,2544,797,262,230,670,530,261,192,815,503,264,688,168,447,257,263,474,171,175,156,161])).
% 59.38/59.42 cnf(4428,plain,
% 59.38/59.42 (P6(a15,a15,a2,a1)),
% 59.38/59.42 inference(scs_inference,[],[4298,4188,4210,4172,4174,4164,3757,3986,4270,4280,4192,4335,4149,4216,4341,4344,4347,4350,4359,4362,4365,4371,4374,4377,4380,4385,3989,4353,4368,4272,4248,4275,742,855,3056,2608,2528,2768,1977,672,2752,2976,2800,2017,2784,2560,3072,2960,158,2544,797,262,230,670,530,261,192,815,503,264,688,168,447,257,263,474,171,175,156,161,176])).
% 59.38/59.42 cnf(4438,plain,
% 59.38/59.42 (P3(f31(a16,a16,a16,a16,a16),f31(a16,a16,a16,a16,a16),a16,f31(a16,a16,a16,a16,a16))),
% 59.38/59.42 inference(scs_inference,[],[4298,4188,4210,4172,4174,4164,3757,3986,4270,4280,4192,4335,4149,4216,4341,4344,4347,4350,4359,4362,4365,4371,4374,4377,4380,4385,3827,3989,4353,4368,4272,3821,4248,4275,4259,742,855,3056,2608,2528,2768,1977,672,2752,2976,2800,2017,2784,2560,3072,2960,158,2544,797,262,230,670,530,261,192,815,503,264,688,168,447,257,263,474,171,175,156,161,176,169,2272,593,157,170])).
% 59.38/59.42 cnf(4446,plain,
% 59.38/59.42 (P5(a2,a15,a2,a15)),
% 59.38/59.42 inference(scs_inference,[],[4298,4188,4210,3871,4172,4174,4164,3757,3986,4266,4270,4280,4192,4335,4338,4149,4216,4341,4344,4347,4350,4359,4362,4365,4371,4374,4377,4380,4385,3827,3989,4353,4368,4272,3821,4248,4275,4259,742,855,3056,2608,2528,2768,1977,672,2752,2976,2800,2017,2784,2560,3072,2960,158,2544,797,262,230,670,530,261,192,815,503,264,688,168,447,257,263,474,171,175,156,161,176,169,2272,593,157,170,260,231,561,173])).
% 59.38/59.42 cnf(4448,plain,
% 59.38/59.42 (P4(x44481,x44482,x44483,x44484,x44482,x44481,x44484,x44483)),
% 59.38/59.42 inference(scs_inference,[],[4298,4188,4210,4218,3871,4172,4174,4164,3757,3986,4266,4270,4280,4192,4335,4338,4149,4216,4341,4344,4347,4350,4359,4362,4365,4371,4374,4377,4380,4385,3827,3989,4353,4368,4272,3821,4248,4275,4259,742,855,3056,2608,2528,2768,1977,672,2752,2976,2800,2017,2784,2560,3072,2960,158,2544,797,262,230,670,530,261,192,815,503,264,688,168,447,257,263,474,171,175,156,161,176,169,2272,593,157,170,260,231,561,173,259])).
% 59.38/59.42 cnf(4450,plain,
% 59.38/59.42 (P5(x44501,a16,a16,x44501)),
% 59.38/59.42 inference(scs_inference,[],[4298,4188,4210,4218,3871,4172,4174,4164,4212,3757,3986,4266,4270,4280,4192,4335,4338,4149,4216,4341,4344,4347,4350,4359,4362,4365,4371,4374,4377,4380,4385,3827,3989,4353,4368,4272,3821,4248,4275,4259,742,855,3056,2608,2528,2768,1977,672,2752,2976,2800,2017,2784,2560,3072,2960,158,2544,797,262,230,670,530,261,192,815,503,264,688,168,447,257,263,474,171,175,156,161,176,169,2272,593,157,170,260,231,561,173,259,172])).
% 59.38/59.42 cnf(4456,plain,
% 59.38/59.42 (P5(a2,a2,a2,f31(a2,a2,a2,a2,a2))),
% 59.38/59.42 inference(scs_inference,[],[4298,4188,4210,4218,3871,4268,4172,4174,4204,4164,4212,3757,3986,4266,4270,4280,4192,4335,4338,4149,4216,4341,4344,4347,4350,4359,4362,4365,4371,4374,4377,4380,4385,3827,3989,4353,4368,4272,3821,4248,4275,4259,3891,742,855,3056,2608,2528,2768,1977,672,2752,2976,2800,2017,2784,2560,3072,2960,158,2544,797,262,230,670,530,261,192,815,503,264,688,168,447,257,263,474,171,175,156,161,176,169,2272,593,157,170,260,231,561,173,259,172,258,253,205])).
% 59.38/59.42 cnf(4457,plain,
% 59.38/59.42 (P5(x44571,x44571,x44571,x44571)),
% 59.38/59.42 inference(rename_variables,[],[4298])).
% 59.38/59.42 cnf(4463,plain,
% 59.38/59.42 (P5(a2,a2,a2,f3(a2,a2,a2))),
% 59.38/59.42 inference(scs_inference,[],[4298,4457,4188,4210,4218,3871,4268,4172,4174,4204,4164,4212,3757,3986,4266,4270,4280,4192,4335,4338,4149,4216,4341,4344,4347,4350,4359,4362,4365,4371,4374,4377,4380,4385,3827,3989,4353,4368,4272,3821,4248,4275,4259,3891,742,855,3056,2608,2528,2768,1977,672,2752,2976,2800,2017,2784,2560,3072,2960,158,2544,797,262,230,670,530,261,192,815,503,264,688,168,447,257,263,474,171,175,156,161,176,169,2272,593,157,170,260,231,561,173,259,172,258,253,205,228,194,193])).
% 59.38/59.42 cnf(4464,plain,
% 59.38/59.42 (P5(x44641,x44641,x44641,x44641)),
% 59.38/59.42 inference(rename_variables,[],[4298])).
% 59.38/59.42 cnf(4473,plain,
% 59.38/59.42 (P10(x44731,x44732,x44731,x44732)),
% 59.38/59.42 inference(rename_variables,[],[3562])).
% 59.38/59.42 cnf(4476,plain,
% 59.38/59.42 (P1(x44761,x44761,x44762)),
% 59.38/59.42 inference(rename_variables,[],[4200])).
% 59.38/59.42 cnf(4479,plain,
% 59.38/59.42 (P1(x44791,x44791,x44792)),
% 59.38/59.42 inference(rename_variables,[],[4200])).
% 59.38/59.42 cnf(4482,plain,
% 59.38/59.42 (P8(f26(x44821,x44822),x44822,x44821)),
% 59.38/59.42 inference(rename_variables,[],[4216])).
% 59.38/59.42 cnf(4488,plain,
% 59.38/59.42 (P5(a15,a2,a15,a2)),
% 59.38/59.42 inference(scs_inference,[],[4298,4457,4464,4188,4210,4218,4200,4476,3871,4268,4172,4174,4204,4277,4164,4212,3678,3757,3861,3986,4266,4270,4280,4192,4335,4338,4149,4216,4341,4344,4347,4350,4359,4362,4365,4371,4374,4377,4380,4385,4004,3827,3989,4353,4368,4272,3821,4248,4275,4259,3592,3785,3562,3815,3891,742,855,3056,2608,2528,2768,1977,672,2752,2976,2800,2017,2784,2560,3072,2960,158,2544,797,262,230,670,530,261,192,815,503,264,688,168,447,257,263,474,171,175,156,161,176,169,2272,593,157,170,260,231,561,173,259,172,258,253,205,228,194,193,183,195,209,2592,203,202,232,210,268,248])).
% 59.38/59.42 cnf(4489,plain,
% 59.38/59.42 (P5(x44891,x44891,x44891,x44891)),
% 59.38/59.42 inference(rename_variables,[],[4298])).
% 59.38/59.42 cnf(4496,plain,
% 59.38/59.42 (P6(x44961,x44962,x44961,x44961)),
% 59.38/59.42 inference(rename_variables,[],[4188])).
% 59.38/59.42 cnf(4499,plain,
% 59.38/59.42 (P5(x44991,x44991,x44991,x44991)),
% 59.38/59.42 inference(rename_variables,[],[4298])).
% 59.38/59.42 cnf(4501,plain,
% 59.38/59.42 (P2(x45011,x45011,x45011,x45011)),
% 59.38/59.42 inference(scs_inference,[],[4298,4457,4464,4489,4499,4188,4210,4218,4200,4476,3871,4268,4172,4174,4204,4277,4164,4212,3678,3757,3861,3986,4266,4270,4280,4192,4335,4338,4149,4216,4341,4344,4347,4350,4359,4362,4365,4371,4374,4377,4380,4385,4004,3827,3989,4353,4368,4272,3821,4248,4275,4259,3592,3785,3562,3815,3891,742,855,3056,2608,2528,2768,1977,672,2752,2976,2800,2017,2784,2560,3072,2960,158,2544,797,262,230,670,530,261,192,815,503,264,688,168,447,257,263,474,171,175,156,161,176,169,2272,593,157,170,260,231,561,173,259,172,258,253,205,228,194,193,183,195,209,2592,203,202,232,210,268,248,182,186,196,206,189])).
% 59.38/59.42 cnf(4503,plain,
% 59.38/59.42 (P5(a16,a2,a16,a16)),
% 59.38/59.42 inference(scs_inference,[],[4298,4457,4464,4489,4499,4188,4210,4218,4200,4476,3871,4268,4172,4174,4204,4277,4164,4212,3678,3757,3861,3986,4266,4270,4280,4192,4335,4338,4149,4216,4341,4344,4347,4350,4359,4362,4365,4371,4374,4377,4380,4385,4004,3827,3989,4353,4368,4272,3821,4248,4275,4259,3592,3785,3562,3815,3839,3891,742,855,3056,2608,2528,2768,1977,672,2752,2976,2800,2017,2784,2560,3072,2960,158,2544,797,262,230,670,530,261,192,815,503,264,688,168,447,257,263,474,171,175,156,161,176,169,2272,593,157,170,260,231,561,173,259,172,258,253,205,228,194,193,183,195,209,2592,203,202,232,210,268,248,182,186,196,206,189,178])).
% 59.38/59.42 cnf(4506,plain,
% 59.38/59.42 (P5(x45061,x45061,x45061,x45061)),
% 59.38/59.42 inference(rename_variables,[],[4298])).
% 59.38/59.42 cnf(4508,plain,
% 59.38/59.42 (P3(x45081,x45082,x45082,x45081)),
% 59.38/59.42 inference(scs_inference,[],[4298,4457,4464,4489,4499,4188,4210,4218,4200,4476,3871,4268,4172,4174,4204,4277,4164,4212,3678,3757,3861,3986,4266,4270,4280,4192,4335,4338,4149,4216,4341,4344,4347,4350,4359,4362,4365,4371,4374,4377,4380,4385,4004,3827,3989,4353,4368,4272,3821,4248,4275,4259,3592,3785,3562,3815,3839,3891,742,855,3056,2608,2528,2768,1977,672,2752,2976,2800,2017,2784,2560,3072,2960,158,2544,797,262,230,670,530,261,192,815,503,264,688,168,447,257,263,474,171,175,156,161,176,169,2272,593,157,170,260,231,561,173,259,172,258,253,205,228,194,193,183,195,209,2592,203,202,232,210,268,248,182,186,196,206,189,178,204,246])).
% 59.38/59.42 cnf(4509,plain,
% 59.38/59.42 (P4(x45091,x45092,x45092,x45091,x45093,x45094,x45093,x45094)),
% 59.38/59.42 inference(rename_variables,[],[4210])).
% 59.38/59.42 cnf(4511,plain,
% 59.38/59.42 (P6(a1,a1,a2,a15)),
% 59.38/59.42 inference(scs_inference,[],[4298,4457,4464,4489,4499,4188,4210,4218,4200,4476,3871,4268,4172,4174,4204,4277,3546,4164,4212,3678,3757,3861,3986,4266,4270,4280,4192,4335,4338,4149,4216,4341,4344,4347,4350,4359,4362,4365,4371,4374,4377,4380,4385,4004,3827,3989,4353,4368,4272,3821,4248,4275,4259,3911,3592,3785,3562,3815,3839,3891,742,855,3056,2608,2528,2768,1977,672,2752,2976,2800,2017,2784,2560,3072,2960,158,2544,797,262,230,670,530,261,192,815,503,264,688,168,447,257,263,474,171,175,156,161,176,169,2272,593,157,170,260,231,561,173,259,172,258,253,205,228,194,193,183,195,209,2592,203,202,232,210,268,248,182,186,196,206,189,178,204,246,241])).
% 59.38/59.42 cnf(4517,plain,
% 59.38/59.42 (P8(f29(a2,a16,a2,a16,a2,a2),a2,a16)),
% 59.38/59.42 inference(scs_inference,[],[4298,4457,4464,4489,4499,4188,4210,4218,4200,4476,3871,4268,4172,4174,4204,4277,3546,4164,4212,3678,3757,3861,3986,4266,4270,4280,4192,4335,4338,4149,4216,4341,4344,4347,4350,4359,4362,4365,4371,4374,4377,4380,4385,4004,3827,3989,4353,4368,4272,3821,4248,4222,4275,4259,3911,3592,3785,3562,3815,3839,3891,742,855,3056,2608,2528,2768,1977,672,2752,2976,2800,2017,2784,2560,3072,2960,158,2544,797,262,230,670,530,261,192,815,503,264,688,168,447,257,263,474,171,175,156,161,176,169,2272,593,157,170,260,231,561,173,259,172,258,253,205,228,194,193,183,195,209,2592,203,202,232,210,268,248,182,186,196,206,189,178,204,246,241,187,208])).
% 59.38/59.42 cnf(4523,plain,
% 59.38/59.42 (P8(f26(x45231,x45232),x45232,x45231)),
% 59.38/59.42 inference(rename_variables,[],[4216])).
% 59.38/59.42 cnf(4529,plain,
% 59.38/59.42 (P8(a2,a2,a2)),
% 59.38/59.42 inference(scs_inference,[],[4298,4457,4464,4489,4499,4506,4188,4210,4509,4218,4200,4476,4479,3871,4268,4172,4174,4204,4277,3546,4164,4212,3678,3757,3861,3986,4266,4270,4280,4192,4335,4338,4149,4216,4341,4344,4347,4350,4359,4362,4365,4371,4374,4377,4380,4385,4482,4523,4004,3827,3989,4353,4368,4272,3821,4248,4222,4275,4259,3511,3911,3706,3592,3763,3785,3562,4473,3815,3839,3891,3789,742,855,3056,2608,2528,2768,1977,672,2752,2976,2800,2017,2784,2560,3072,2960,158,2544,797,262,230,670,530,261,192,815,503,264,688,168,447,257,263,474,171,175,156,161,176,169,2272,593,157,170,260,231,561,173,259,172,258,253,205,228,194,193,183,195,209,2592,203,202,232,210,268,248,182,186,196,206,189,178,204,246,241,187,208,200,197,191,244])).
% 59.38/59.42 cnf(4530,plain,
% 59.38/59.42 (P1(x45301,x45301,x45302)),
% 59.38/59.42 inference(rename_variables,[],[4200])).
% 59.38/59.42 cnf(4533,plain,
% 59.38/59.42 (P8(f31(a16,a16,a16,a16,a16),f31(a16,a16,a16,a16,a16),a16)),
% 59.38/59.42 inference(scs_inference,[],[4298,4457,4464,4489,4499,4506,4188,4210,4509,4218,4200,4476,4479,4530,3871,4268,4172,4174,4204,4277,3546,4164,4212,3678,3757,3861,3986,4266,4270,4280,4192,4335,4338,4149,4216,4341,4344,4347,4350,4359,4362,4365,4371,4374,4377,4380,4385,4482,4523,4004,3827,3989,4353,4368,4272,3821,4248,4222,3996,4275,4259,3511,3911,3706,3592,3811,3763,3785,3562,4473,3815,3839,3891,3789,742,855,3056,2608,2528,2768,1977,672,2752,2976,2800,2017,2784,2560,3072,2960,158,2544,797,262,230,670,530,261,192,815,503,264,688,168,447,257,263,474,171,175,156,161,176,169,2272,593,157,170,260,231,561,173,259,172,258,253,205,228,194,193,183,195,209,2592,203,202,232,210,268,248,182,186,196,206,189,178,204,246,241,187,208,200,197,191,244,167])).
% 59.38/59.42 cnf(4534,plain,
% 59.38/59.42 (P1(x45341,x45341,x45342)),
% 59.38/59.42 inference(rename_variables,[],[4200])).
% 59.38/59.42 cnf(4536,plain,
% 59.38/59.42 (P5(a16,a16,a16,a2)),
% 59.38/59.42 inference(scs_inference,[],[4298,4457,4464,4489,4499,4506,4188,4496,4202,4210,4509,4218,4200,4476,4479,4530,3871,4268,4172,4174,4204,4277,3546,4164,4212,3678,3757,3861,3986,4241,4266,4270,4280,4192,4335,4338,4149,4216,4341,4344,4347,4350,4359,4362,4365,4371,4374,4377,4380,4385,4482,4523,4004,3827,3989,4353,4368,4272,3821,4248,4222,3996,4275,4259,3511,3911,3706,3592,3811,3763,3785,3562,4473,3815,3839,3891,3789,742,855,3056,2608,2528,2768,1977,672,2752,2976,2800,2017,2784,2560,3072,2960,158,2544,797,262,230,670,530,261,192,815,503,264,688,168,447,257,263,474,171,175,156,161,176,169,2272,593,157,170,260,231,561,173,259,172,258,253,205,228,194,193,183,195,209,2592,203,202,232,210,268,248,182,186,196,206,189,178,204,246,241,187,208,200,197,191,244,167,256])).
% 59.38/59.42 cnf(4545,plain,
% 59.38/59.42 (P10(a17,a18,a2,a16)),
% 59.38/59.42 inference(scs_inference,[],[4298,4457,4464,4489,4499,4506,4188,4496,4202,4210,4509,4218,4200,4476,4479,4530,4534,3871,4268,4172,4174,4204,4277,3546,4164,4212,3678,3757,3861,3986,4241,4266,4270,4280,4192,4335,4338,4149,4216,4341,4344,4347,4350,4359,4362,4365,4371,4374,4377,4380,4385,4482,4523,4004,3827,3989,4353,4368,4272,3821,4248,4222,3996,4275,4259,3511,3911,3706,3889,3592,3811,3698,3763,3785,3562,4473,3815,3839,3891,3789,742,855,3056,2608,2528,2768,1977,672,2752,2976,2800,2017,2784,2560,3072,2960,158,2544,797,262,230,670,530,261,192,815,503,264,688,168,447,257,263,474,171,175,156,161,176,169,2272,593,157,170,260,231,561,173,259,172,258,253,205,228,194,193,183,195,209,2592,203,202,232,210,268,248,182,186,196,206,189,178,204,246,241,187,208,200,197,191,244,167,256,211,367])).
% 59.38/59.42 cnf(4557,plain,
% 59.38/59.42 (P6(a15,a2,a1,a15)),
% 59.38/59.42 inference(scs_inference,[],[4298,4457,4464,4489,4499,4506,4188,4496,4202,4210,4509,4218,4200,4476,4479,4530,4534,3871,4268,4172,4174,4204,4277,3546,4164,4212,3678,3757,3861,3986,4241,4266,4270,4280,4192,4335,4338,4149,4216,4341,4344,4347,4350,4359,4362,4365,4371,4374,4377,4380,4385,4482,4523,4004,3827,3989,4353,4368,4272,3821,4248,4222,3996,4275,4259,3511,3911,3706,3889,3592,3811,3698,3763,3785,3562,4473,3815,3839,3891,3789,742,855,3056,2608,2528,2768,1977,672,2752,2976,2800,2017,2784,2560,3072,2960,158,2544,797,262,230,670,530,261,192,815,503,264,688,168,447,257,263,474,171,175,156,161,176,169,2272,593,157,170,260,231,561,173,259,172,258,253,205,228,194,193,183,195,209,2592,203,202,232,210,268,248,182,186,196,206,189,178,204,246,241,187,208,200,197,191,244,167,256,211,367,811,809,640,3456,648,174])).
% 59.38/59.42 cnf(4561,plain,
% 59.38/59.42 (P8(f29(a2,a16,a2,a16,a2,a2),a16,a2)),
% 59.38/59.42 inference(scs_inference,[],[4298,4457,4464,4489,4499,4506,4188,4496,4202,4210,4509,4218,4200,4476,4479,4530,4534,3871,4268,4172,4174,4204,4277,3546,4164,4212,3678,3757,3861,3986,4241,4266,4270,4280,4192,4335,4338,4149,4216,4341,4344,4347,4350,4359,4362,4365,4371,4374,4377,4380,4385,4482,4523,4004,3827,3989,4353,4368,4272,3821,4248,4222,3996,4275,4259,3511,3911,3706,3889,3592,3811,3698,3763,3785,3562,4473,3815,3839,3891,3789,742,855,3056,2608,2528,2768,1977,672,2752,2976,2800,2017,2784,2560,3072,2960,158,2544,797,262,230,670,530,261,192,815,503,264,688,168,447,257,263,474,171,175,156,161,176,169,2272,593,157,170,260,231,561,173,259,172,258,253,205,228,194,193,183,195,209,2592,203,202,232,210,268,248,182,186,196,206,189,178,204,246,241,187,208,200,197,191,244,167,256,211,367,811,809,640,3456,648,174,229,159])).
% 59.38/59.42 cnf(4591,plain,
% 59.38/59.42 (P3(x45911,x45912,x45912,x45911)),
% 59.38/59.42 inference(rename_variables,[],[4508])).
% 59.38/59.42 cnf(4679,plain,
% 59.38/59.42 (P4(x46791,x46792,x46793,x46794,x46792,x46791,x46794,x46793)),
% 59.38/59.42 inference(rename_variables,[],[4448])).
% 59.38/59.42 cnf(4682,plain,
% 59.38/59.42 (P3(x46821,x46822,x46822,x46821)),
% 59.38/59.42 inference(rename_variables,[],[4508])).
% 59.38/59.42 cnf(4685,plain,
% 59.38/59.42 (P5(x46851,a16,a16,x46851)),
% 59.38/59.42 inference(rename_variables,[],[4450])).
% 59.38/59.42 cnf(4686,plain,
% 59.38/59.42 (P3(x46861,x46862,x46862,x46861)),
% 59.38/59.42 inference(rename_variables,[],[4508])).
% 59.38/59.42 cnf(4694,plain,
% 59.38/59.42 (P3(x46941,x46942,x46942,x46941)),
% 59.38/59.42 inference(rename_variables,[],[4508])).
% 59.38/59.42 cnf(4700,plain,
% 59.38/59.42 (P3(x47001,x47002,x47002,x47001)),
% 59.38/59.42 inference(rename_variables,[],[4508])).
% 59.38/59.42 cnf(4703,plain,
% 59.38/59.42 (P3(x47031,x47032,x47032,x47031)),
% 59.38/59.42 inference(rename_variables,[],[4508])).
% 59.38/59.42 cnf(4708,plain,
% 59.38/59.42 (P3(x47081,x47082,x47082,x47081)),
% 59.38/59.42 inference(rename_variables,[],[4508])).
% 59.38/59.42 cnf(4718,plain,
% 59.38/59.42 (P3(x47181,x47182,x47182,x47181)),
% 59.38/59.42 inference(rename_variables,[],[4508])).
% 59.38/59.42 cnf(4723,plain,
% 59.38/59.42 (P3(x47231,x47232,x47232,x47231)),
% 59.38/59.42 inference(rename_variables,[],[4508])).
% 59.38/59.42 cnf(4726,plain,
% 59.38/59.42 (P3(x47261,x47262,x47262,x47261)),
% 59.38/59.42 inference(rename_variables,[],[4508])).
% 59.38/59.42 cnf(4733,plain,
% 59.38/59.42 (P3(x47331,x47332,x47332,x47331)),
% 59.38/59.42 inference(rename_variables,[],[4508])).
% 59.38/59.42 cnf(4736,plain,
% 59.38/59.42 (P3(x47361,x47362,x47362,x47361)),
% 59.38/59.42 inference(rename_variables,[],[4508])).
% 59.38/59.42 cnf(4737,plain,
% 59.38/59.42 (P5(x47371,a16,a16,x47371)),
% 59.38/59.42 inference(rename_variables,[],[4450])).
% 59.38/59.42 cnf(4748,plain,
% 59.38/59.42 (P3(x47481,x47482,x47482,x47481)),
% 59.38/59.42 inference(rename_variables,[],[4508])).
% 59.38/59.42 cnf(4758,plain,
% 59.38/59.42 ($false),
% 59.38/59.42 inference(scs_inference,[],[142,4501,4422,4448,4679,4508,4591,4682,4686,4694,4700,4703,4708,4718,4723,4726,4733,4736,4748,3682,4220,4186,4389,4406,4391,4450,4685,4737,3710,3897,4228,4420,4428,4446,4488,4503,4511,4529,4536,4545,4557,4426,4382,4424,4026,3743,3948,4456,4142,4438,4291,4533,4561,4517,4463,4008,3823,4216,435,452,3982,3672,4277,3562,421,3779,1977,285,742,672,2017,670,809,640,797,530,261,158,262,230,503,264,192,263,257,815,175,688,168,156,174,447,157,161,169,171,474,229,176,231,2272,260,593,170,561,173,159,172,259,258,245,199,205,235,125,185,198,195,193,228,179,162,232,210,194,209,202,203,186,248,196,206,189,178,246,204,187,241,208,180]),
% 59.38/59.42 ['proof']).
% 59.38/59.42 % SZS output end Proof
% 59.38/59.42 % Total time :58.710000s
%------------------------------------------------------------------------------