%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : GEO631+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 : n026.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:06:00 EDT 2024
% Result : Theorem 59.40s 59.56s
% Output : CNFRefutation 59.47s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : GEO631+1 : TPTP v8.2.0. Released v7.5.0.
% 0.03/0.12 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% 0.12/0.33 % Computer : n026.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 300
% 0.12/0.33 % DateTime : Fri Jun 21 06:14:09 EDT 2024
% 0.12/0.33 % CPUTime :
% 0.51/0.59 start to proof:theBenchmark
% 59.40/59.55 %-------------------------------------------
% 59.40/59.55 % File :CSE---1.7
% 59.40/59.55 % Problem :theBenchmark
% 59.40/59.55 % Transform :cnf
% 59.40/59.55 % Format :tptp:raw
% 59.40/59.55 % Command :java -jar mcs_scs.jar %d %s
% 59.40/59.55
% 59.40/59.55 % Result :Theorem 58.760000s
% 59.40/59.55 % Output :CNFRefutation 58.760000s
% 59.40/59.55 %-------------------------------------------
% 59.40/59.56 %------------------------------------------------------------------------------
% 59.40/59.56 % File : GEO631+1 : TPTP v8.2.0. Released v7.5.0.
% 59.40/59.56 % Domain : Geometry
% 59.40/59.56 % Problem : JGEX problem 94
% 59.40/59.56 % Version : [CGZ00] axioms.
% 59.40/59.56 % English :
% 59.40/59.56
% 59.40/59.56 % Refs : [CGZ00] Chou et al. (2000), A Deductive Database Approach to A
% 59.40/59.56 % : [YCG08] Ye et al. (2008), An Introduction to Java Geometry Exp
% 59.40/59.56 % : [Qua20] Quaresma (2020), Email to Geoff Sutcliffe
% 59.40/59.56 % Source : [Qua20]
% 59.40/59.56 % Names : 94.p [Qua20]
% 59.40/59.56
% 59.40/59.56 % Status : Theorem
% 59.40/59.56 % Rating : 0.36 v8.1.0, 0.44 v7.5.0
% 59.40/59.56 % Syntax : Number of formulae : 95 ( 0 unt; 0 def)
% 59.40/59.56 % Number of atoms : 297 ( 1 equ)
% 59.40/59.56 % Maximal formula atoms : 14 ( 3 avg)
% 59.40/59.56 % Number of connectives : 209 ( 7 ~; 0 |; 107 &)
% 59.40/59.56 % ( 0 <=>; 95 =>; 0 <=; 0 <~>)
% 59.40/59.56 % Maximal formula depth : 27 ( 9 avg)
% 59.40/59.56 % Maximal term depth : 1 ( 1 avg)
% 59.40/59.56 % Number of predicates : 12 ( 11 usr; 0 prp; 2-8 aty)
% 59.40/59.56 % Number of functors : 0 ( 0 usr; 0 con; --- aty)
% 59.40/59.56 % Number of variables : 535 ( 515 !; 20 ?)
% 59.40/59.56 % SPC : FOF_THM_RFO_SEQ
% 59.40/59.56
% 59.40/59.56 % Comments : Taken from JGEX [YCG08], converted by Pedro Quaresma.
% 59.40/59.56 %------------------------------------------------------------------------------
% 59.40/59.56 include('Axioms/GEO012+0.ax').
% 59.40/59.56 %------------------------------------------------------------------------------
% 59.40/59.56 fof(exemplo6GDDFULL8110994,conjecture,
% 59.40/59.56 ! [A,B,C,O,D,P,F,G,H,E,I,NWPNT1,NWPNT2] :
% 59.40/59.56 ( ( circle(O,A,B,C)
% 59.40/59.56 & circle(O,A,D,NWPNT1)
% 59.40/59.56 & circle(O,A,P,NWPNT2)
% 59.40/59.56 & perp(F,P,A,D)
% 59.40/59.56 & coll(F,A,D)
% 59.40/59.56 & perp(G,P,A,B)
% 59.40/59.56 & coll(G,A,B)
% 59.40/59.56 & perp(H,P,B,C)
% 59.40/59.56 & coll(H,B,C)
% 59.40/59.56 & perp(E,P,C,D)
% 59.40/59.56 & coll(E,C,D)
% 59.40/59.56 & coll(I,F,G)
% 59.40/59.56 & coll(I,H,E) )
% 59.40/59.56 => cyclic(P,G,I,H) ) ).
% 59.40/59.56
% 59.40/59.56 %------------------------------------------------------------------------------
% 59.40/59.56 %-------------------------------------------
% 59.40/59.56 % Proof found
% 59.40/59.56 % SZS status Theorem for theBenchmark
% 59.40/59.56 % SZS output start Proof
% 59.40/59.57 %ClaNum:268(EqnAxiom:141)
% 59.40/59.57 %VarNum:1613(SingletonVarNum:590)
% 59.40/59.57 %MaxLitNum:5
% 59.40/59.57 %MaxfuncDepth:1
% 59.40/59.57 %SharedTerms:27
% 59.40/59.57 %goalClause: 142 143 144 145 146 147 148 149 150 151 152 153 154 155
% 59.40/59.57 %singleGoalClaCount:14
% 59.40/59.57 [142]P1(a1,a2,a15)
% 59.40/59.57 [143]P1(a20,a2,a16)
% 59.40/59.57 [144]P1(a21,a16,a17)
% 59.40/59.57 [145]P1(a22,a17,a15)
% 59.40/59.57 [146]P1(a24,a1,a20)
% 59.40/59.57 [147]P1(a24,a21,a22)
% 59.40/59.57 [148]P3(a1,a19,a2,a15)
% 59.40/59.57 [149]P3(a20,a19,a2,a16)
% 59.40/59.57 [150]P3(a21,a19,a16,a17)
% 59.40/59.57 [151]P3(a22,a19,a17,a15)
% 59.40/59.57 [152]P2(a18,a2,a16,a17)
% 59.40/59.57 [153]P2(a18,a2,a15,a25)
% 59.40/59.57 [154]P2(a18,a2,a19,a26)
% 59.40/59.57 [155]~P4(a19,a20,a24,a21)
% 59.40/59.57 [156]~P1(x1562,x1561,x1563)+P1(x1561,x1562,x1563)
% 59.40/59.57 [157]~P1(x1571,x1573,x1572)+P1(x1571,x1572,x1573)
% 59.40/59.57 [158]~P7(x1581,x1582,x1583)+P1(x1581,x1582,x1583)
% 59.40/59.57 [159]~P7(x1591,x1593,x1592)+P7(x1591,x1592,x1593)
% 59.40/59.57 [161]~P7(x1611,x1612,x1613)+P5(x1611,x1612,x1611,x1613)
% 59.40/59.57 [165]~P10(x1651,x1652,x1651,x1653)+P1(x1651,x1652,x1653)
% 59.40/59.57 [231]~P5(x2311,x2312,x2311,x2313)+P9(x2311,x2312,x2312,x2313,x2312,x2313,x2311,x2313)
% 59.40/59.57 [168]~P10(x1683,x1684,x1681,x1682)+P10(x1681,x1682,x1683,x1684)
% 59.40/59.57 [169]~P10(x1691,x1692,x1694,x1693)+P10(x1691,x1692,x1693,x1694)
% 59.40/59.57 [170]~P3(x1703,x1704,x1701,x1702)+P3(x1701,x1702,x1703,x1704)
% 59.40/59.57 [171]~P3(x1711,x1712,x1714,x1713)+P3(x1711,x1712,x1713,x1714)
% 59.40/59.57 [172]~P5(x1723,x1724,x1721,x1722)+P5(x1721,x1722,x1723,x1724)
% 59.40/59.57 [173]~P5(x1731,x1732,x1734,x1733)+P5(x1731,x1732,x1733,x1734)
% 59.40/59.57 [174]~P4(x1742,x1741,x1743,x1744)+P4(x1741,x1742,x1743,x1744)
% 59.40/59.57 [175]~P4(x1751,x1753,x1752,x1754)+P4(x1751,x1752,x1753,x1754)
% 59.40/59.57 [176]~P4(x1761,x1762,x1764,x1763)+P4(x1761,x1762,x1763,x1764)
% 59.40/59.57 [229]~P4(x2292,x2293,x2291,x2294)+P9(x2291,x2292,x2291,x2293,x2294,x2292,x2294,x2293)
% 59.40/59.57 [192]~P2(x1924,x1921,x1922,x1923)+P3(f7(x1921,x1922,x1923,x1924),x1921,x1921,x1924)
% 59.40/59.57 [207]P5(x2071,x2072,x2073,x2074)+~P6(x2071,x2072,x2075,x2073,x2074,x2076)
% 59.40/59.57 [219]~P11(x2194,x2195,x2196,x2191,x2192,x2193)+P11(x2191,x2192,x2193,x2194,x2195,x2196)
% 59.40/59.57 [220]~P11(x2202,x2201,x2203,x2205,x2204,x2206)+P11(x2201,x2202,x2203,x2204,x2205,x2206)
% 59.40/59.57 [221]~P11(x2211,x2213,x2212,x2214,x2216,x2215)+P11(x2211,x2212,x2213,x2214,x2215,x2216)
% 59.40/59.57 [222]~P6(x2224,x2225,x2226,x2221,x2222,x2223)+P6(x2221,x2222,x2223,x2224,x2225,x2226)
% 59.40/59.57 [223]~P6(x2232,x2231,x2233,x2235,x2234,x2236)+P6(x2231,x2232,x2233,x2234,x2235,x2236)
% 59.40/59.57 [224]~P6(x2241,x2243,x2242,x2244,x2246,x2245)+P6(x2241,x2242,x2243,x2244,x2245,x2246)
% 59.40/59.57 [230]~P10(x2301,x2302,x2305,x2306)+P9(x2301,x2302,x2303,x2304,x2305,x2306,x2303,x2304)
% 59.40/59.57 [236]~P11(x2361,x2362,x2363,x2364,x2365,x2366)+P9(x2361,x2362,x2362,x2363,x2364,x2365,x2365,x2366)
% 59.40/59.57 [237]~P11(x2371,x2372,x2373,x2374,x2375,x2376)+P8(x2371,x2372,x2371,x2373,x2374,x2375,x2374,x2376)
% 59.40/59.57 [238]~P9(x2381,x2382,x2385,x2386,x2383,x2384,x2385,x2386)+P10(x2381,x2382,x2383,x2384)
% 59.40/59.57 [257]~P9(x2575,x2576,x2577,x2578,x2571,x2572,x2573,x2574)+P9(x2571,x2572,x2573,x2574,x2575,x2576,x2577,x2578)
% 59.40/59.57 [258]~P9(x2583,x2584,x2581,x2582,x2587,x2588,x2585,x2586)+P9(x2581,x2582,x2583,x2584,x2585,x2586,x2587,x2588)
% 59.40/59.57 [259]~P9(x2592,x2591,x2593,x2594,x2595,x2596,x2597,x2598)+P9(x2591,x2592,x2593,x2594,x2595,x2596,x2597,x2598)
% 59.40/59.57 [260]~P9(x2601,x2602,x2605,x2606,x2603,x2604,x2607,x2608)+P9(x2601,x2602,x2603,x2604,x2605,x2606,x2607,x2608)
% 59.40/59.57 [261]~P8(x2615,x2616,x2617,x2618,x2611,x2612,x2613,x2614)+P8(x2611,x2612,x2613,x2614,x2615,x2616,x2617,x2618)
% 59.40/59.57 [262]~P8(x2623,x2624,x2621,x2622,x2627,x2628,x2625,x2626)+P8(x2621,x2622,x2623,x2624,x2625,x2626,x2627,x2628)
% 59.40/59.57 [263]~P8(x2632,x2631,x2633,x2634,x2635,x2636,x2637,x2638)+P8(x2631,x2632,x2633,x2634,x2635,x2636,x2637,x2638)
% 59.40/59.57 [264]~P8(x2641,x2642,x2645,x2646,x2643,x2644,x2647,x2648)+P8(x2641,x2642,x2643,x2644,x2645,x2646,x2647,x2648)
% 59.40/59.57 [166]~P1(x1661,x1662,x1663)+~P5(x1661,x1662,x1661,x1663)+P7(x1661,x1662,x1663)
% 59.40/59.57 [240]P5(x2401,x2402,x2401,x2403)+~P9(x2401,x2402,x2402,x2403,x2402,x2403,x2401,x2403)+P1(x2401,x2402,x2403)
% 59.40/59.57 [181]~P3(x1811,x1812,x1812,x1813)+~P5(x1812,x1811,x1812,x1813)+P1(x1811,x1812,f3(x1811,x1813,x1812))
% 59.40/59.57 [193]~P3(x1932,x1931,x1931,x1933)+~P5(x1931,x1932,x1931,x1933)+P5(x1931,x1932,x1931,f3(x1932,x1933,x1931))
% 59.40/59.57 [160]~P1(x1603,x1604,x1601)+P1(x1601,x1602,x1603)+~P1(x1603,x1604,x1602)
% 59.40/59.57 [177]~P2(x1774,x1771,x1772,x1773)+P3(x1771,x1772,x1772,x1773)+~P1(x1774,x1771,x1773)
% 59.40/59.57 [178]~P3(x1781,x1784,x1782,x1783)+P5(x1781,x1782,x1781,x1783)+~P7(x1784,x1782,x1783)
% 59.40/59.57 [179]~P3(x1791,x1793,x1793,x1794)+P5(x1791,x1792,x1793,x1792)+~P7(x1792,x1791,x1794)
% 59.40/59.57 [186]~P5(x1861,x1864,x1862,x1864)+~P5(x1861,x1863,x1862,x1863)+P3(x1861,x1862,x1863,x1864)
% 59.40/59.57 [189]~P5(x1891,x1892,x1891,x1894)+~P5(x1891,x1892,x1891,x1893)+P2(x1891,x1892,x1893,x1894)
% 59.40/59.57 [235]~P10(x2351,x2354,x2353,x2352)+~P4(x2351,x2354,x2353,x2352)+P9(x2351,x2352,x2353,x2352,x2353,x2352,x2353,x2354)
% 59.40/59.57 [239]~P9(x2391,x2393,x2391,x2394,x2392,x2393,x2392,x2394)+P1(x2391,x2392,x2393)+P4(x2393,x2394,x2391,x2392)
% 59.40/59.57 [241]~P1(x2413,x2414,x2412)+~P9(x2413,x2411,x2413,x2412,x2414,x2411,x2414,x2412)+P4(x2411,x2412,x2413,x2414)
% 59.40/59.57 [243]P3(x2431,x2432,x2433,x2434)+~P9(x2431,x2432,x2433,x2434,x2433,x2434,x2431,x2432)+P10(x2431,x2432,x2433,x2434)
% 59.40/59.57 [182]~P3(x1821,x1824,x1822,x1823)+~P3(x1822,x1824,x1821,x1823)+P1(f4(x1821,x1822,x1823),x1823,x1822)
% 59.40/59.57 [183]~P3(x1831,x1834,x1832,x1833)+~P3(x1832,x1834,x1831,x1833)+P1(f5(x1831,x1832,x1833),x1833,x1831)
% 59.40/59.57 [194]~P3(x1941,x1944,x1942,x1943)+~P3(x1942,x1944,x1941,x1943)+P3(x1941,f4(x1941,x1942,x1943),x1943,x1942)
% 59.40/59.57 [195]~P3(x1951,x1954,x1952,x1953)+~P3(x1952,x1954,x1951,x1953)+P3(x1951,f5(x1952,x1951,x1953),x1953,x1952)
% 59.40/59.57 [196]~P3(x1961,x1963,x1963,x1962)+~P4(x1961,x1962,x1963,x1964)+P2(f8(x1961,x1962,x1963),x1961,x1962,x1963)
% 59.40/59.57 [198]~P3(x1983,x1984,x1982,x1981)+~P5(x1983,x1982,x1983,x1981)+P1(x1981,x1982,f28(x1982,x1981,x1983,x1984))
% 59.40/59.57 [199]~P3(x1993,x1994,x1991,x1992)+~P5(x1993,x1991,x1993,x1992)+P1(f28(x1991,x1992,x1993,x1994),x1993,x1994)
% 59.40/59.57 [250]~P5(x2503,x2502,x2503,x2501)+~P9(x2502,x2503,x2503,x2504,x2503,x2504,x2503,x2501)+P1(x2501,x2502,f23(x2502,x2501,x2503,x2504))
% 59.40/59.57 [251]~P3(x2513,x2514,x2512,x2511)+~P9(x2512,x2513,x2513,x2514,x2513,x2514,x2513,x2511)+P1(x2511,x2512,f29(x2512,x2511,x2513,x2514))
% 59.40/59.57 [252]~P3(x2523,x2522,x2522,x2521)+~P9(x2524,x2523,x2522,x2523,x2522,x2523,x2521,x2523)+P1(f14(x2521,x2522,x2523,x2524),x2523,x2524)
% 59.40/59.57 [253]~P3(x2533,x2532,x2532,x2531)+~P9(x2534,x2533,x2532,x2533,x2532,x2533,x2531,x2533)+P1(f14(x2531,x2532,x2533,x2534),x2531,x2532)
% 59.40/59.57 [254]~P5(x2543,x2541,x2543,x2542)+~P9(x2541,x2543,x2543,x2544,x2543,x2544,x2543,x2542)+P1(f23(x2541,x2542,x2543,x2544),x2543,x2544)
% 59.40/59.57 [255]~P3(x2553,x2554,x2551,x2552)+~P9(x2551,x2553,x2553,x2554,x2553,x2554,x2553,x2552)+P1(f29(x2551,x2552,x2553,x2554),x2553,x2554)
% 59.40/59.57 [162]~P7(x1625,x1621,x1623)+P10(x1621,x1622,x1623,x1624)+~P7(x1625,x1622,x1624)
% 59.40/59.57 [163]~P7(x1631,x1635,x1633)+P10(x1631,x1632,x1633,x1634)+~P7(x1632,x1635,x1634)
% 59.40/59.57 [190]~P4(x1905,x1901,x1902,x1903)+P4(x1901,x1902,x1903,x1904)+~P4(x1905,x1901,x1902,x1904)
% 59.40/59.57 [232]~P7(x2325,x2322,x2323)+~P2(x2324,x2321,x2322,x2323)+P9(x2321,x2322,x2321,x2323,x2324,x2322,x2324,x2325)
% 59.40/59.57 [234]~P2(x2345,x2341,x2343,x2344)+P9(x2341,x2342,x2341,x2343,x2344,x2341,x2344,x2343)+~P3(x2345,x2341,x2341,x2342)
% 59.40/59.57 [247]~P9(x2472,x2473,x2472,x2474,x2475,x2472,x2475,x2474)+P3(x2471,x2472,x2472,x2473)+~P2(x2471,x2472,x2474,x2475)
% 59.40/59.57 [202]~P1(x2022,x2024,x2025)+~P3(x2021,x2023,x2023,x2022)+P1(f12(x2021,x2022,x2023,x2024,x2025),x2024,x2025)
% 59.40/59.57 [203]~P1(x2032,x2034,x2035)+~P3(x2031,x2033,x2033,x2032)+P3(f12(x2031,x2032,x2033,x2034,x2035),x2031,x2034,x2035)
% 59.40/59.57 [204]~P3(x2043,x2044,x2044,x2041)+~P5(x2041,x2042,x2041,x2045)+P5(x2041,x2042,x2041,f32(x2043,x2044,x2042,x2045,x2041))
% 59.40/59.57 [205]~P3(x2053,x2051,x2051,x2055)+~P5(x2055,x2052,x2055,x2054)+P5(x2051,x2052,x2051,f32(x2053,x2051,x2052,x2054,x2055))
% 59.40/59.57 [206]~P3(x2061,x2062,x2062,x2065)+~P5(x2065,x2063,x2065,x2064)+P10(f32(x2061,x2062,x2063,x2064,x2065),x2063,x2061,x2062)
% 59.40/59.57 [249]~P9(x2491,x2493,x2492,x2493,x2491,x2494,x2492,x2495)+P1(x2491,x2492,x2493)+P4(x2494,x2492,x2493,f31(x2491,x2492,x2493,x2494))
% 59.40/59.57 [265]~P9(x2651,x2653,x2652,x2653,x2651,x2654,x2652,x2655)+P1(x2651,x2652,x2653)+P9(x2651,x2653,x2652,x2653,x2651,f31(x2651,x2652,x2653,x2654),x2652,f31(x2651,x2652,x2653,x2654))
% 59.40/59.57 [184]~P10(x1841,x1842,x1845,x1846)+P10(x1841,x1842,x1843,x1844)+~P10(x1845,x1846,x1843,x1844)
% 59.40/59.57 [185]~P3(x1851,x1852,x1855,x1856)+P10(x1851,x1852,x1853,x1854)+~P3(x1855,x1856,x1853,x1854)
% 59.40/59.57 [187]~P3(x1875,x1876,x1873,x1874)+P3(x1871,x1872,x1873,x1874)+~P10(x1871,x1872,x1875,x1876)
% 59.40/59.57 [188]~P5(x1881,x1882,x1885,x1886)+P5(x1881,x1882,x1883,x1884)+~P5(x1885,x1886,x1883,x1884)
% 59.40/59.57 [225]~P5(x2251,x2252,x2254,x2255)+~P11(x2251,x2252,x2253,x2254,x2255,x2256)+P6(x2251,x2252,x2253,x2254,x2255,x2256)
% 59.40/59.57 [228]~P7(x2284,x2285,x2286)+~P7(x2281,x2282,x2283)+P8(x2281,x2282,x2282,x2283,x2284,x2285,x2285,x2286)
% 59.40/59.57 [208]~P7(x2086,x2083,x2084)+~P7(x2085,x2081,x2082)+P7(f30(x2081,x2082,x2083,x2084,x2085,x2086),x2081,x2084)
% 59.40/59.57 [209]~P7(x2096,x2093,x2094)+~P7(x2095,x2091,x2092)+P10(f30(x2091,x2092,x2093,x2094,x2095,x2096),x2096,x2091,x2093)
% 59.40/59.57 [210]~P7(x2106,x2103,x2104)+~P7(x2105,x2101,x2102)+P10(f30(x2101,x2102,x2103,x2104,x2105,x2106),x2105,x2102,x2104)
% 59.40/59.57 [245]~P9(x2451,x2452,x2453,x2454,x2455,x2456,x2457,x2458)+P10(x2451,x2452,x2453,x2454)+~P10(x2455,x2456,x2457,x2458)
% 59.40/59.57 [246]~P9(x2461,x2462,x2463,x2464,x2465,x2466,x2467,x2468)+P3(x2461,x2462,x2463,x2464)+~P3(x2465,x2466,x2467,x2468)
% 59.40/59.57 [248]~P8(x2481,x2482,x2483,x2484,x2485,x2486,x2487,x2488)+P5(x2481,x2482,x2483,x2484)+~P5(x2485,x2486,x2487,x2488)
% 59.40/59.57 [226]~P11(x2261,x2262,x2263,x2267,x2268,x2269)+P11(x2261,x2262,x2263,x2264,x2265,x2266)+~P11(x2267,x2268,x2269,x2264,x2265,x2266)
% 59.40/59.57 [227]~P6(x2271,x2272,x2273,x2277,x2278,x2279)+P6(x2271,x2272,x2273,x2274,x2275,x2276)+~P6(x2277,x2278,x2279,x2274,x2275,x2276)
% 59.40/59.57 [267]~P9(x2671,x2672,x2673,x2674,x2679,x26710,x26711,x26712)+P9(x2671,x2672,x2673,x2674,x2675,x2676,x2677,x2678)+~P9(x2679,x26710,x26711,x26712,x2675,x2676,x2677,x2678)
% 59.40/59.57 [268]~P8(x2681,x2682,x2683,x2684,x2689,x26810,x26811,x26812)+P8(x2681,x2682,x2683,x2684,x2685,x2686,x2687,x2688)+~P8(x2689,x26810,x26811,x26812,x2685,x2686,x2687,x2688)
% 59.40/59.57 [200]~P5(x2002,x2001,x2004,x2001)+~P4(x2002,x2004,x2001,x2003)+P3(x2001,x2002,x2002,x2003)+~P5(x2002,x2003,x2004,x2003)
% 59.40/59.57 [167]~P1(x1671,x1672,x1673)+~P10(x1674,x1671,x1675,x1673)+P7(x1671,x1672,x1673)+~P7(x1674,x1672,x1675)
% 59.40/59.57 [180]~P10(x1804,x1803,x1805,x1802)+~P10(x1804,x1802,x1805,x1803)+P7(x1801,x1802,x1803)+~P7(x1801,x1804,x1805)
% 59.40/59.57 [201]~P5(x2015,x2011,x2015,x2013)+~P5(x2015,x2011,x2015,x2012)+P4(x2011,x2012,x2013,x2014)+~P5(x2015,x2011,x2015,x2014)
% 59.40/59.57 [233]~P1(x2331,x2334,x2335)+~P1(x2331,x2332,x2333)+~P10(x2332,x2334,x2333,x2335)+P8(x2331,x2332,x2332,x2333,x2331,x2334,x2334,x2335)
% 59.40/59.57 [244]~P1(x2441,x2442,x2443)+~P9(x2445,x2442,x2445,x2443,x2444,x2442,x2444,x2441)+P7(x2441,x2442,x2443)+~P2(x2444,x2445,x2442,x2443)
% 59.40/59.57 [191]~P3(x1913,x1911,x1913,x1915)+~P3(x1911,x1912,x1911,x1913)+~P7(x1914,x1912,x1915)+P7(f6(x1911,x1912,x1913),x1911,x1913)
% 59.40/59.57 [197]~P4(x1971,x1972,x1973,x1975)+~P10(x1971,x1972,x1973,x1975)+~P7(x1974,x1971,x1972)+P2(f9(x1971,x1972,x1973),x1971,x1972,x1973)
% 59.40/59.57 [266]~P9(x2661,x2663,x2662,x2663,x2664,x2666,x2665,x2666)+~P9(x2661,x2662,x2662,x2663,x2664,x2665,x2665,x2666)+P1(x2661,x2662,x2663)+P11(x2661,x2662,x2663,x2664,x2665,x2666)
% 59.40/59.57 [256]~P4(x2561,x2562,x2565,x2564)+~P4(x2561,x2562,x2565,x2563)+~P9(x2565,x2561,x2565,x2562,x2566,x2563,x2566,x2564)+P5(x2561,x2562,x2563,x2564)+~P4(x2561,x2562,x2565,x2566)
% 59.40/59.57 [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.40/59.57 [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.40/59.57 [213]~P1(x2133,x2134,x2135)+~P7(x2136,x2131,x2132)+~P10(x2131,x2133,x2135,x2136)+~P10(x2131,x2133,x2132,x2134)+P1(f33(x2131,x2132,x2133,x2134,x2135,x2136),x2136,x2135)
% 59.40/59.57 [214]~P1(x2143,x2144,x2145)+~P7(x2146,x2141,x2142)+~P10(x2141,x2143,x2145,x2146)+~P10(x2141,x2143,x2142,x2144)+P1(f33(x2141,x2142,x2143,x2144,x2145,x2146),x2141,x2144)
% 59.40/59.57 [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.40/59.57 [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.40/59.57 [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.40/59.58 [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.40/59.58 [164]~P1(x1643,x1641,x1644)+~P1(x1645,x1641,x1644)+~P7(x1646,x1645,x1643)+~P7(x1647,x1641,x1644)+P7(f27(x1641,x1642),x1641,x1642)
% 59.40/59.58 %EqnAxiom
% 59.40/59.58 [1]E(x11,x11)
% 59.40/59.58 [2]E(x22,x21)+~E(x21,x22)
% 59.40/59.58 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 59.40/59.58 [4]~E(x41,x42)+E(f27(x41,x43),f27(x42,x43))
% 59.40/59.58 [5]~E(x51,x52)+E(f27(x53,x51),f27(x53,x52))
% 59.40/59.58 [6]~E(x61,x62)+E(f3(x61,x63,x64),f3(x62,x63,x64))
% 59.40/59.58 [7]~E(x71,x72)+E(f3(x73,x71,x74),f3(x73,x72,x74))
% 59.40/59.58 [8]~E(x81,x82)+E(f3(x83,x84,x81),f3(x83,x84,x82))
% 59.40/59.58 [9]~E(x91,x92)+E(f4(x91,x93,x94),f4(x92,x93,x94))
% 59.40/59.58 [10]~E(x101,x102)+E(f4(x103,x101,x104),f4(x103,x102,x104))
% 59.40/59.58 [11]~E(x111,x112)+E(f4(x113,x114,x111),f4(x113,x114,x112))
% 59.40/59.58 [12]~E(x121,x122)+E(f5(x121,x123,x124),f5(x122,x123,x124))
% 59.40/59.58 [13]~E(x131,x132)+E(f5(x133,x131,x134),f5(x133,x132,x134))
% 59.40/59.58 [14]~E(x141,x142)+E(f5(x143,x144,x141),f5(x143,x144,x142))
% 59.40/59.58 [15]~E(x151,x152)+E(f6(x151,x153,x154),f6(x152,x153,x154))
% 59.40/59.58 [16]~E(x161,x162)+E(f6(x163,x161,x164),f6(x163,x162,x164))
% 59.40/59.58 [17]~E(x171,x172)+E(f6(x173,x174,x171),f6(x173,x174,x172))
% 59.40/59.58 [18]~E(x181,x182)+E(f7(x181,x183,x184,x185),f7(x182,x183,x184,x185))
% 59.40/59.58 [19]~E(x191,x192)+E(f7(x193,x191,x194,x195),f7(x193,x192,x194,x195))
% 59.40/59.58 [20]~E(x201,x202)+E(f7(x203,x204,x201,x205),f7(x203,x204,x202,x205))
% 59.40/59.58 [21]~E(x211,x212)+E(f7(x213,x214,x215,x211),f7(x213,x214,x215,x212))
% 59.40/59.58 [22]~E(x221,x222)+E(f31(x221,x223,x224,x225),f31(x222,x223,x224,x225))
% 59.40/59.58 [23]~E(x231,x232)+E(f31(x233,x231,x234,x235),f31(x233,x232,x234,x235))
% 59.40/59.58 [24]~E(x241,x242)+E(f31(x243,x244,x241,x245),f31(x243,x244,x242,x245))
% 59.40/59.58 [25]~E(x251,x252)+E(f31(x253,x254,x255,x251),f31(x253,x254,x255,x252))
% 59.40/59.58 [26]~E(x261,x262)+E(f23(x261,x263,x264,x265),f23(x262,x263,x264,x265))
% 59.40/59.58 [27]~E(x271,x272)+E(f23(x273,x271,x274,x275),f23(x273,x272,x274,x275))
% 59.40/59.58 [28]~E(x281,x282)+E(f23(x283,x284,x281,x285),f23(x283,x284,x282,x285))
% 59.40/59.58 [29]~E(x291,x292)+E(f23(x293,x294,x295,x291),f23(x293,x294,x295,x292))
% 59.40/59.58 [30]~E(x301,x302)+E(f29(x301,x303,x304,x305),f29(x302,x303,x304,x305))
% 59.40/59.58 [31]~E(x311,x312)+E(f29(x313,x311,x314,x315),f29(x313,x312,x314,x315))
% 59.40/59.58 [32]~E(x321,x322)+E(f29(x323,x324,x321,x325),f29(x323,x324,x322,x325))
% 59.40/59.58 [33]~E(x331,x332)+E(f29(x333,x334,x335,x331),f29(x333,x334,x335,x332))
% 59.40/59.58 [34]~E(x341,x342)+E(f8(x341,x343,x344),f8(x342,x343,x344))
% 59.40/59.58 [35]~E(x351,x352)+E(f8(x353,x351,x354),f8(x353,x352,x354))
% 59.40/59.58 [36]~E(x361,x362)+E(f8(x363,x364,x361),f8(x363,x364,x362))
% 59.40/59.58 [37]~E(x371,x372)+E(f9(x371,x373,x374),f9(x372,x373,x374))
% 59.40/59.58 [38]~E(x381,x382)+E(f9(x383,x381,x384),f9(x383,x382,x384))
% 59.40/59.58 [39]~E(x391,x392)+E(f9(x393,x394,x391),f9(x393,x394,x392))
% 59.40/59.58 [40]~E(x401,x402)+E(f28(x401,x403,x404,x405),f28(x402,x403,x404,x405))
% 59.40/59.58 [41]~E(x411,x412)+E(f28(x413,x411,x414,x415),f28(x413,x412,x414,x415))
% 59.40/59.58 [42]~E(x421,x422)+E(f28(x423,x424,x421,x425),f28(x423,x424,x422,x425))
% 59.40/59.58 [43]~E(x431,x432)+E(f28(x433,x434,x435,x431),f28(x433,x434,x435,x432))
% 59.40/59.58 [44]~E(x441,x442)+E(f14(x441,x443,x444,x445),f14(x442,x443,x444,x445))
% 59.40/59.58 [45]~E(x451,x452)+E(f14(x453,x451,x454,x455),f14(x453,x452,x454,x455))
% 59.40/59.58 [46]~E(x461,x462)+E(f14(x463,x464,x461,x465),f14(x463,x464,x462,x465))
% 59.40/59.58 [47]~E(x471,x472)+E(f14(x473,x474,x475,x471),f14(x473,x474,x475,x472))
% 59.40/59.58 [48]~E(x481,x482)+E(f12(x481,x483,x484,x485,x486),f12(x482,x483,x484,x485,x486))
% 59.40/59.58 [49]~E(x491,x492)+E(f12(x493,x491,x494,x495,x496),f12(x493,x492,x494,x495,x496))
% 59.40/59.58 [50]~E(x501,x502)+E(f12(x503,x504,x501,x505,x506),f12(x503,x504,x502,x505,x506))
% 59.40/59.58 [51]~E(x511,x512)+E(f12(x513,x514,x515,x511,x516),f12(x513,x514,x515,x512,x516))
% 59.40/59.58 [52]~E(x521,x522)+E(f12(x523,x524,x525,x526,x521),f12(x523,x524,x525,x526,x522))
% 59.40/59.58 [53]~E(x531,x532)+E(f11(x531,x533,x534,x535,x536,x537),f11(x532,x533,x534,x535,x536,x537))
% 59.40/59.58 [54]~E(x541,x542)+E(f11(x543,x541,x544,x545,x546,x547),f11(x543,x542,x544,x545,x546,x547))
% 59.40/59.58 [55]~E(x551,x552)+E(f11(x553,x554,x551,x555,x556,x557),f11(x553,x554,x552,x555,x556,x557))
% 59.40/59.58 [56]~E(x561,x562)+E(f11(x563,x564,x565,x561,x566,x567),f11(x563,x564,x565,x562,x566,x567))
% 59.40/59.58 [57]~E(x571,x572)+E(f11(x573,x574,x575,x576,x571,x577),f11(x573,x574,x575,x576,x572,x577))
% 59.40/59.58 [58]~E(x581,x582)+E(f11(x583,x584,x585,x586,x587,x581),f11(x583,x584,x585,x586,x587,x582))
% 59.40/59.58 [59]~E(x591,x592)+E(f32(x591,x593,x594,x595,x596),f32(x592,x593,x594,x595,x596))
% 59.40/59.58 [60]~E(x601,x602)+E(f32(x603,x601,x604,x605,x606),f32(x603,x602,x604,x605,x606))
% 59.40/59.58 [61]~E(x611,x612)+E(f32(x613,x614,x611,x615,x616),f32(x613,x614,x612,x615,x616))
% 59.40/59.58 [62]~E(x621,x622)+E(f32(x623,x624,x625,x621,x626),f32(x623,x624,x625,x622,x626))
% 59.40/59.58 [63]~E(x631,x632)+E(f32(x633,x634,x635,x636,x631),f32(x633,x634,x635,x636,x632))
% 59.40/59.58 [64]~E(x641,x642)+E(f10(x641,x643,x644,x645,x646,x647),f10(x642,x643,x644,x645,x646,x647))
% 59.40/59.58 [65]~E(x651,x652)+E(f10(x653,x651,x654,x655,x656,x657),f10(x653,x652,x654,x655,x656,x657))
% 59.40/59.58 [66]~E(x661,x662)+E(f10(x663,x664,x661,x665,x666,x667),f10(x663,x664,x662,x665,x666,x667))
% 59.40/59.58 [67]~E(x671,x672)+E(f10(x673,x674,x675,x671,x676,x677),f10(x673,x674,x675,x672,x676,x677))
% 59.40/59.58 [68]~E(x681,x682)+E(f10(x683,x684,x685,x686,x681,x687),f10(x683,x684,x685,x686,x682,x687))
% 59.40/59.58 [69]~E(x691,x692)+E(f10(x693,x694,x695,x696,x697,x691),f10(x693,x694,x695,x696,x697,x692))
% 59.40/59.58 [70]~E(x701,x702)+E(f33(x701,x703,x704,x705,x706,x707),f33(x702,x703,x704,x705,x706,x707))
% 59.40/59.58 [71]~E(x711,x712)+E(f33(x713,x711,x714,x715,x716,x717),f33(x713,x712,x714,x715,x716,x717))
% 59.40/59.58 [72]~E(x721,x722)+E(f33(x723,x724,x721,x725,x726,x727),f33(x723,x724,x722,x725,x726,x727))
% 59.40/59.58 [73]~E(x731,x732)+E(f33(x733,x734,x735,x731,x736,x737),f33(x733,x734,x735,x732,x736,x737))
% 59.40/59.58 [74]~E(x741,x742)+E(f33(x743,x744,x745,x746,x741,x747),f33(x743,x744,x745,x746,x742,x747))
% 59.40/59.58 [75]~E(x751,x752)+E(f33(x753,x754,x755,x756,x757,x751),f33(x753,x754,x755,x756,x757,x752))
% 59.40/59.58 [76]~E(x761,x762)+E(f30(x761,x763,x764,x765,x766,x767),f30(x762,x763,x764,x765,x766,x767))
% 59.40/59.58 [77]~E(x771,x772)+E(f30(x773,x771,x774,x775,x776,x777),f30(x773,x772,x774,x775,x776,x777))
% 59.40/59.58 [78]~E(x781,x782)+E(f30(x783,x784,x781,x785,x786,x787),f30(x783,x784,x782,x785,x786,x787))
% 59.40/59.58 [79]~E(x791,x792)+E(f30(x793,x794,x795,x791,x796,x797),f30(x793,x794,x795,x792,x796,x797))
% 59.40/59.58 [80]~E(x801,x802)+E(f30(x803,x804,x805,x806,x801,x807),f30(x803,x804,x805,x806,x802,x807))
% 59.40/59.58 [81]~E(x811,x812)+E(f30(x813,x814,x815,x816,x817,x811),f30(x813,x814,x815,x816,x817,x812))
% 59.40/59.58 [82]~E(x821,x822)+E(f13(x821,x823,x824,x825,x826,x827),f13(x822,x823,x824,x825,x826,x827))
% 59.40/59.58 [83]~E(x831,x832)+E(f13(x833,x831,x834,x835,x836,x837),f13(x833,x832,x834,x835,x836,x837))
% 59.40/59.58 [84]~E(x841,x842)+E(f13(x843,x844,x841,x845,x846,x847),f13(x843,x844,x842,x845,x846,x847))
% 59.40/59.58 [85]~E(x851,x852)+E(f13(x853,x854,x855,x851,x856,x857),f13(x853,x854,x855,x852,x856,x857))
% 59.40/59.58 [86]~E(x861,x862)+E(f13(x863,x864,x865,x866,x861,x867),f13(x863,x864,x865,x866,x862,x867))
% 59.40/59.58 [87]~E(x871,x872)+E(f13(x873,x874,x875,x876,x877,x871),f13(x873,x874,x875,x876,x877,x872))
% 59.40/59.58 [88]P1(x882,x883,x884)+~E(x881,x882)+~P1(x881,x883,x884)
% 59.40/59.58 [89]P1(x893,x892,x894)+~E(x891,x892)+~P1(x893,x891,x894)
% 59.40/59.58 [90]P1(x903,x904,x902)+~E(x901,x902)+~P1(x903,x904,x901)
% 59.40/59.58 [91]P8(x912,x913,x914,x915,x916,x917,x918,x919)+~E(x911,x912)+~P8(x911,x913,x914,x915,x916,x917,x918,x919)
% 59.40/59.58 [92]P8(x923,x922,x924,x925,x926,x927,x928,x929)+~E(x921,x922)+~P8(x923,x921,x924,x925,x926,x927,x928,x929)
% 59.40/59.58 [93]P8(x933,x934,x932,x935,x936,x937,x938,x939)+~E(x931,x932)+~P8(x933,x934,x931,x935,x936,x937,x938,x939)
% 59.40/59.58 [94]P8(x943,x944,x945,x942,x946,x947,x948,x949)+~E(x941,x942)+~P8(x943,x944,x945,x941,x946,x947,x948,x949)
% 59.40/59.58 [95]P8(x953,x954,x955,x956,x952,x957,x958,x959)+~E(x951,x952)+~P8(x953,x954,x955,x956,x951,x957,x958,x959)
% 59.40/59.58 [96]P8(x963,x964,x965,x966,x967,x962,x968,x969)+~E(x961,x962)+~P8(x963,x964,x965,x966,x967,x961,x968,x969)
% 59.40/59.58 [97]P8(x973,x974,x975,x976,x977,x978,x972,x979)+~E(x971,x972)+~P8(x973,x974,x975,x976,x977,x978,x971,x979)
% 59.40/59.58 [98]P8(x983,x984,x985,x986,x987,x988,x989,x982)+~E(x981,x982)+~P8(x983,x984,x985,x986,x987,x988,x989,x981)
% 59.40/59.58 [99]P5(x992,x993,x994,x995)+~E(x991,x992)+~P5(x991,x993,x994,x995)
% 59.40/59.58 [100]P5(x1003,x1002,x1004,x1005)+~E(x1001,x1002)+~P5(x1003,x1001,x1004,x1005)
% 59.40/59.58 [101]P5(x1013,x1014,x1012,x1015)+~E(x1011,x1012)+~P5(x1013,x1014,x1011,x1015)
% 59.40/59.58 [102]P5(x1023,x1024,x1025,x1022)+~E(x1021,x1022)+~P5(x1023,x1024,x1025,x1021)
% 59.40/59.58 [103]P7(x1032,x1033,x1034)+~E(x1031,x1032)+~P7(x1031,x1033,x1034)
% 59.40/59.58 [104]P7(x1043,x1042,x1044)+~E(x1041,x1042)+~P7(x1043,x1041,x1044)
% 59.40/59.58 [105]P7(x1053,x1054,x1052)+~E(x1051,x1052)+~P7(x1053,x1054,x1051)
% 59.40/59.58 [106]P9(x1062,x1063,x1064,x1065,x1066,x1067,x1068,x1069)+~E(x1061,x1062)+~P9(x1061,x1063,x1064,x1065,x1066,x1067,x1068,x1069)
% 59.40/59.58 [107]P9(x1073,x1072,x1074,x1075,x1076,x1077,x1078,x1079)+~E(x1071,x1072)+~P9(x1073,x1071,x1074,x1075,x1076,x1077,x1078,x1079)
% 59.40/59.58 [108]P9(x1083,x1084,x1082,x1085,x1086,x1087,x1088,x1089)+~E(x1081,x1082)+~P9(x1083,x1084,x1081,x1085,x1086,x1087,x1088,x1089)
% 59.40/59.58 [109]P9(x1093,x1094,x1095,x1092,x1096,x1097,x1098,x1099)+~E(x1091,x1092)+~P9(x1093,x1094,x1095,x1091,x1096,x1097,x1098,x1099)
% 59.40/59.58 [110]P9(x1103,x1104,x1105,x1106,x1102,x1107,x1108,x1109)+~E(x1101,x1102)+~P9(x1103,x1104,x1105,x1106,x1101,x1107,x1108,x1109)
% 59.40/59.58 [111]P9(x1113,x1114,x1115,x1116,x1117,x1112,x1118,x1119)+~E(x1111,x1112)+~P9(x1113,x1114,x1115,x1116,x1117,x1111,x1118,x1119)
% 59.40/59.58 [112]P9(x1123,x1124,x1125,x1126,x1127,x1128,x1122,x1129)+~E(x1121,x1122)+~P9(x1123,x1124,x1125,x1126,x1127,x1128,x1121,x1129)
% 59.40/59.58 [113]P9(x1133,x1134,x1135,x1136,x1137,x1138,x1139,x1132)+~E(x1131,x1132)+~P9(x1133,x1134,x1135,x1136,x1137,x1138,x1139,x1131)
% 59.40/59.58 [114]P10(x1142,x1143,x1144,x1145)+~E(x1141,x1142)+~P10(x1141,x1143,x1144,x1145)
% 59.40/59.58 [115]P10(x1153,x1152,x1154,x1155)+~E(x1151,x1152)+~P10(x1153,x1151,x1154,x1155)
% 59.40/59.58 [116]P10(x1163,x1164,x1162,x1165)+~E(x1161,x1162)+~P10(x1163,x1164,x1161,x1165)
% 59.40/59.58 [117]P10(x1173,x1174,x1175,x1172)+~E(x1171,x1172)+~P10(x1173,x1174,x1175,x1171)
% 59.40/59.58 [118]P3(x1182,x1183,x1184,x1185)+~E(x1181,x1182)+~P3(x1181,x1183,x1184,x1185)
% 59.40/59.58 [119]P3(x1193,x1192,x1194,x1195)+~E(x1191,x1192)+~P3(x1193,x1191,x1194,x1195)
% 59.40/59.58 [120]P3(x1203,x1204,x1202,x1205)+~E(x1201,x1202)+~P3(x1203,x1204,x1201,x1205)
% 59.40/59.58 [121]P3(x1213,x1214,x1215,x1212)+~E(x1211,x1212)+~P3(x1213,x1214,x1215,x1211)
% 59.40/59.58 [122]P11(x1222,x1223,x1224,x1225,x1226,x1227)+~E(x1221,x1222)+~P11(x1221,x1223,x1224,x1225,x1226,x1227)
% 59.40/59.58 [123]P11(x1233,x1232,x1234,x1235,x1236,x1237)+~E(x1231,x1232)+~P11(x1233,x1231,x1234,x1235,x1236,x1237)
% 59.40/59.58 [124]P11(x1243,x1244,x1242,x1245,x1246,x1247)+~E(x1241,x1242)+~P11(x1243,x1244,x1241,x1245,x1246,x1247)
% 59.40/59.58 [125]P11(x1253,x1254,x1255,x1252,x1256,x1257)+~E(x1251,x1252)+~P11(x1253,x1254,x1255,x1251,x1256,x1257)
% 59.40/59.58 [126]P11(x1263,x1264,x1265,x1266,x1262,x1267)+~E(x1261,x1262)+~P11(x1263,x1264,x1265,x1266,x1261,x1267)
% 59.40/59.58 [127]P11(x1273,x1274,x1275,x1276,x1277,x1272)+~E(x1271,x1272)+~P11(x1273,x1274,x1275,x1276,x1277,x1271)
% 59.40/59.58 [128]P2(x1282,x1283,x1284,x1285)+~E(x1281,x1282)+~P2(x1281,x1283,x1284,x1285)
% 59.40/59.58 [129]P2(x1293,x1292,x1294,x1295)+~E(x1291,x1292)+~P2(x1293,x1291,x1294,x1295)
% 59.40/59.58 [130]P2(x1303,x1304,x1302,x1305)+~E(x1301,x1302)+~P2(x1303,x1304,x1301,x1305)
% 59.40/59.58 [131]P2(x1313,x1314,x1315,x1312)+~E(x1311,x1312)+~P2(x1313,x1314,x1315,x1311)
% 59.40/59.58 [132]P4(x1322,x1323,x1324,x1325)+~E(x1321,x1322)+~P4(x1321,x1323,x1324,x1325)
% 59.40/59.58 [133]P4(x1333,x1332,x1334,x1335)+~E(x1331,x1332)+~P4(x1333,x1331,x1334,x1335)
% 59.40/59.58 [134]P4(x1343,x1344,x1342,x1345)+~E(x1341,x1342)+~P4(x1343,x1344,x1341,x1345)
% 59.40/59.58 [135]P4(x1353,x1354,x1355,x1352)+~E(x1351,x1352)+~P4(x1353,x1354,x1355,x1351)
% 59.40/59.58 [136]P6(x1362,x1363,x1364,x1365,x1366,x1367)+~E(x1361,x1362)+~P6(x1361,x1363,x1364,x1365,x1366,x1367)
% 59.40/59.58 [137]P6(x1373,x1372,x1374,x1375,x1376,x1377)+~E(x1371,x1372)+~P6(x1373,x1371,x1374,x1375,x1376,x1377)
% 59.40/59.58 [138]P6(x1383,x1384,x1382,x1385,x1386,x1387)+~E(x1381,x1382)+~P6(x1383,x1384,x1381,x1385,x1386,x1387)
% 59.40/59.58 [139]P6(x1393,x1394,x1395,x1392,x1396,x1397)+~E(x1391,x1392)+~P6(x1393,x1394,x1395,x1391,x1396,x1397)
% 59.40/59.58 [140]P6(x1403,x1404,x1405,x1406,x1402,x1407)+~E(x1401,x1402)+~P6(x1403,x1404,x1405,x1406,x1401,x1407)
% 59.40/59.58 [141]P6(x1413,x1414,x1415,x1416,x1417,x1412)+~E(x1411,x1412)+~P6(x1413,x1414,x1415,x1416,x1417,x1411)
% 59.40/59.58
% 59.40/59.58 %-------------------------------------------
% 59.40/59.58 cnf(269,plain,
% 59.40/59.58 (~P4(a20,a19,a24,a21)),
% 59.40/59.58 inference(scs_inference,[],[155,174])).
% 59.40/59.58 cnf(271,plain,
% 59.40/59.58 (~P4(a19,a24,a20,a21)),
% 59.40/59.58 inference(scs_inference,[],[155,174,175])).
% 59.40/59.58 cnf(273,plain,
% 59.40/59.58 (~P4(a19,a20,a21,a24)),
% 59.40/59.58 inference(scs_inference,[],[155,174,175,176])).
% 59.40/59.58 cnf(275,plain,
% 59.40/59.58 (P1(a15,a15,a1)),
% 59.40/59.58 inference(scs_inference,[],[142,155,174,175,176,160])).
% 59.40/59.58 cnf(277,plain,
% 59.40/59.58 (~P3(x2771,x2772,a1,a19)+P10(x2771,x2772,a2,a15)),
% 59.40/59.58 inference(scs_inference,[],[142,148,155,174,175,176,160,185])).
% 59.40/59.58 cnf(289,plain,
% 59.40/59.58 (~P4(a24,a19,a20,a21)),
% 59.40/59.58 inference(scs_inference,[],[271,174])).
% 59.40/59.58 cnf(291,plain,
% 59.40/59.58 (~P4(a20,a19,a21,a24)),
% 59.40/59.58 inference(scs_inference,[],[269,271,174,176])).
% 59.40/59.58 cnf(293,plain,
% 59.40/59.58 (~P4(a20,a24,a19,a21)),
% 59.40/59.58 inference(scs_inference,[],[269,271,174,176,175])).
% 59.40/59.58 cnf(309,plain,
% 59.40/59.58 (~P4(a24,a20,a19,a21)),
% 59.40/59.58 inference(scs_inference,[],[293,174])).
% 59.40/59.58 cnf(311,plain,
% 59.40/59.58 (~P4(a19,a21,a20,a24)),
% 59.40/59.58 inference(scs_inference,[],[273,293,174,175])).
% 59.40/59.58 cnf(313,plain,
% 59.40/59.58 (~P4(a24,a19,a21,a20)),
% 59.40/59.58 inference(scs_inference,[],[273,289,293,174,175,176])).
% 59.40/59.58 cnf(315,plain,
% 59.40/59.58 (P1(a17,a17,a21)),
% 59.40/59.58 inference(scs_inference,[],[144,273,289,293,174,175,176,160])).
% 59.40/59.58 cnf(319,plain,
% 59.40/59.58 (~P3(x3191,x3192,a21,a19)+P10(x3191,x3192,a16,a17)),
% 59.40/59.58 inference(scs_inference,[],[144,150,154,273,289,293,174,175,176,160,130,131,185])).
% 59.40/59.58 cnf(328,plain,
% 59.40/59.58 (~P4(a21,a19,a20,a24)),
% 59.40/59.58 inference(scs_inference,[],[311,174])).
% 59.40/59.58 cnf(330,plain,
% 59.40/59.58 (~P4(a24,a20,a21,a19)),
% 59.40/59.58 inference(scs_inference,[],[309,311,174,176])).
% 59.40/59.58 cnf(332,plain,
% 59.40/59.58 (~P4(a20,a21,a19,a24)),
% 59.40/59.58 inference(scs_inference,[],[291,309,311,174,176,175])).
% 59.40/59.58 cnf(334,plain,
% 59.40/59.58 (P1(a15,a15,a22)),
% 59.40/59.58 inference(scs_inference,[],[145,291,309,311,174,176,175,160])).
% 59.40/59.58 cnf(348,plain,
% 59.40/59.58 (~P4(a19,a24,a21,a20)),
% 59.40/59.58 inference(scs_inference,[],[313,174])).
% 59.40/59.58 cnf(350,plain,
% 59.47/59.58 (~P4(a24,a21,a19,a20)),
% 59.47/59.58 inference(scs_inference,[],[313,174,175])).
% 59.47/59.58 cnf(356,plain,
% 59.47/59.58 (~P3(x3561,x3562,a22,a19)+P10(x3561,x3562,a17,a15)),
% 59.47/59.58 inference(scs_inference,[],[146,151,313,328,174,175,176,160,185])).
% 59.47/59.58 cnf(365,plain,
% 59.47/59.58 (~P4(a20,a24,a21,a19)),
% 59.47/59.58 inference(scs_inference,[],[330,174])).
% 59.47/59.58 cnf(367,plain,
% 59.47/59.58 (~P4(a20,a21,a24,a19)),
% 59.47/59.58 inference(scs_inference,[],[330,332,174,176])).
% 59.47/59.58 cnf(373,plain,
% 59.47/59.58 (~P3(x3731,x3732,a20,a19)+P10(x3731,x3732,a2,a16)),
% 59.47/59.58 inference(scs_inference,[],[147,149,330,332,174,176,175,160,185])).
% 59.47/59.58 cnf(382,plain,
% 59.47/59.58 (~P4(a21,a24,a19,a20)),
% 59.47/59.58 inference(scs_inference,[],[350,174])).
% 59.47/59.58 cnf(384,plain,
% 59.47/59.58 (~P4(a19,a21,a24,a20)),
% 59.47/59.58 inference(scs_inference,[],[348,350,174,175])).
% 59.47/59.58 cnf(386,plain,
% 59.47/59.58 (~P4(a21,a24,a20,a19)),
% 59.47/59.58 inference(scs_inference,[],[348,350,174,175,176])).
% 59.47/59.58 cnf(388,plain,
% 59.47/59.58 (P1(a1,a1,a15)),
% 59.47/59.58 inference(scs_inference,[],[275,348,350,174,175,176,160])).
% 59.47/59.58 cnf(394,plain,
% 59.47/59.58 (~P4(a21,a20,a24,a19)),
% 59.47/59.58 inference(scs_inference,[],[367,174])).
% 59.47/59.58 cnf(396,plain,
% 59.47/59.58 (~P4(a21,a20,a19,a24)),
% 59.47/59.58 inference(scs_inference,[],[367,174,176])).
% 59.47/59.58 cnf(647,plain,
% 59.47/59.58 (P1(a2,a15,a1)),
% 59.47/59.58 inference(scs_inference,[],[142,156,157])).
% 59.47/59.58 cnf(648,plain,
% 59.47/59.58 (P1(a1,a1,a2)),
% 59.47/59.58 inference(scs_inference,[],[647,160])).
% 59.47/59.58 cnf(661,plain,
% 59.47/59.58 (P1(a2,a2,a1)),
% 59.47/59.58 inference(scs_inference,[],[648,160])).
% 59.47/59.58 cnf(850,plain,
% 59.47/59.58 (P1(a15,x8501,a1)+~E(a2,x8501)),
% 59.47/59.58 inference(scs_inference,[],[388,648,90,160])).
% 59.47/59.58 cnf(854,plain,
% 59.47/59.58 (P1(a15,a2,a1)),
% 59.47/59.58 inference(equality_inference,[],[850])).
% 59.47/59.58 cnf(891,plain,
% 59.47/59.58 (P10(a17,a15,x8911,x8912)+~P3(x8911,x8912,a22,a19)),
% 59.47/59.58 inference(scs_inference,[],[356,168])).
% 59.47/59.58 cnf(892,plain,
% 59.47/59.58 (P10(x8921,x8922,a16,a2)+~P3(x8921,x8922,a20,a19)),
% 59.47/59.58 inference(scs_inference,[],[373,169])).
% 59.47/59.58 cnf(898,plain,
% 59.47/59.58 (P10(a17,a15,a17,a15)),
% 59.47/59.58 inference(scs_inference,[],[151,891,170])).
% 59.47/59.58 cnf(949,plain,
% 59.47/59.58 (~P7(x9491,a17,a17)+P7(x9491,a15,a15)),
% 59.47/59.58 inference(scs_inference,[],[898,180])).
% 59.47/59.58 cnf(954,plain,
% 59.47/59.58 (P8(f33(a15,x9541,a15,a15,a1,x9542),a17,a17,a17,f33(a15,x9541,a15,a15,a1,x9542),a15,a15,a15)+~P10(a15,a15,x9541,a15)+~P10(a15,a15,a1,x9542)+~P1(f33(a15,x9541,a15,a15,a1,x9542),a17,a17)+~P7(x9542,a15,x9541)),
% 59.47/59.58 inference(scs_inference,[],[275,898,233,214])).
% 59.47/59.58 cnf(959,plain,
% 59.47/59.58 (P8(f33(a15,x9591,a15,a15,a22,x9592),a17,a17,a17,f33(a15,x9591,a15,a15,a22,x9592),a15,a15,a15)+~P10(a15,a15,x9591,a15)+~P10(a15,a15,a22,x9592)+~P1(f33(a15,x9591,a15,a15,a22,x9592),a17,a17)+~P7(x9592,a15,x9591)),
% 59.47/59.58 inference(scs_inference,[],[334,898,233,214])).
% 59.47/59.58 cnf(1170,plain,
% 59.47/59.58 (P10(a2,a16,a16,a2)),
% 59.47/59.58 inference(scs_inference,[],[149,892,170])).
% 59.47/59.58 cnf(1180,plain,
% 59.47/59.58 (~P3(a16,a2,x11801,x11802)+P3(a2,a16,x11801,x11802)),
% 59.47/59.58 inference(scs_inference,[],[1170,187])).
% 59.47/59.58 cnf(1184,plain,
% 59.47/59.58 (~P3(x11841,x11842,a16,a2)+P3(a2,a16,x11841,x11842)),
% 59.47/59.58 inference(scs_inference,[],[1170,187,171,170])).
% 59.47/59.58 cnf(1422,plain,
% 59.47/59.58 (P3(a2,a16,x14221,x14222)+~P3(x14222,x14221,a16,a2)),
% 59.47/59.58 inference(scs_inference,[],[1184,171])).
% 59.47/59.58 cnf(1758,plain,
% 59.47/59.58 (P3(a2,a16,a19,a20)),
% 59.47/59.58 inference(scs_inference,[],[149,1422,171])).
% 59.47/59.58 cnf(1759,plain,
% 59.47/59.58 (P10(a20,a19,a19,a20)),
% 59.47/59.58 inference(scs_inference,[],[149,1758,185])).
% 59.47/59.58 cnf(1782,plain,
% 59.47/59.58 (~P3(a19,a20,x17821,x17822)+P3(a20,a19,x17821,x17822)),
% 59.47/59.58 inference(scs_inference,[],[1759,187])).
% 59.47/59.58 cnf(4290,plain,
% 59.47/59.58 (P1(a17,a15,a15)),
% 59.47/59.58 inference(scs_inference,[],[898,230,165])).
% 59.47/59.58 cnf(4292,plain,
% 59.47/59.58 (P1(a2,a1,a15)),
% 59.47/59.58 inference(scs_inference,[],[142,898,230,165,156])).
% 59.47/59.58 cnf(4296,plain,
% 59.47/59.58 (P9(x42961,x42962,a17,a15,x42961,x42962,a17,a15)),
% 59.47/59.58 inference(scs_inference,[],[142,898,1759,230,165,156,168,258])).
% 59.47/59.58 cnf(4298,plain,
% 59.47/59.58 (P10(a17,a15,a15,a17)),
% 59.47/59.58 inference(scs_inference,[],[142,898,1759,230,165,156,168,258,169])).
% 59.47/59.58 cnf(4300,plain,
% 59.47/59.58 (P1(a1,a15,a2)),
% 59.47/59.58 inference(scs_inference,[],[142,898,1759,230,165,156,168,258,169,157])).
% 59.47/59.58 cnf(4302,plain,
% 59.47/59.58 (P3(f7(a2,a16,a17,a18),a2,a2,a18)),
% 59.47/59.58 inference(scs_inference,[],[142,152,898,1759,230,165,156,168,258,169,157,192])).
% 59.47/59.58 cnf(4306,plain,
% 59.47/59.58 (P3(a19,a20,a2,a16)),
% 59.47/59.58 inference(scs_inference,[],[142,1758,152,898,1759,230,165,156,168,258,169,157,192,171,170])).
% 59.47/59.58 cnf(4308,plain,
% 59.47/59.58 (P9(a17,a15,a17,a15,x43081,x43082,x43081,x43082)),
% 59.47/59.58 inference(scs_inference,[],[142,1758,152,898,1759,230,165,156,168,258,169,157,192,171,170,260])).
% 59.47/59.58 cnf(4310,plain,
% 59.47/59.58 (P9(a15,a17,x43101,x43102,a17,a15,x43101,x43102)),
% 59.47/59.58 inference(scs_inference,[],[142,1758,152,898,1759,230,165,156,168,258,169,157,192,171,170,260,259])).
% 59.47/59.58 cnf(4312,plain,
% 59.47/59.58 (P10(a2,a16,a2,a16)),
% 59.47/59.58 inference(scs_inference,[],[142,1758,152,898,1759,230,165,156,168,258,169,157,192,171,170,260,259,185])).
% 59.47/59.58 cnf(4316,plain,
% 59.47/59.58 (P4(a15,a21,a17,a17)),
% 59.47/59.58 inference(scs_inference,[],[142,315,1758,152,898,1759,230,165,156,168,258,169,157,192,171,170,260,259,185,184,241])).
% 59.47/59.58 cnf(4318,plain,
% 59.47/59.58 (P10(a17,a21,a17,a21)),
% 59.47/59.58 inference(scs_inference,[],[142,315,1758,152,898,1759,230,165,156,168,258,169,157,192,171,170,260,259,185,184,241,238])).
% 59.47/59.58 cnf(4322,plain,
% 59.47/59.58 (P4(a21,a15,a17,a17)),
% 59.47/59.58 inference(scs_inference,[],[142,315,1758,152,898,1759,230,165,156,168,258,169,157,192,171,170,260,259,185,184,241,238,257,174])).
% 59.47/59.58 cnf(4324,plain,
% 59.47/59.58 (P4(a15,a17,a21,a17)),
% 59.47/59.58 inference(scs_inference,[],[142,315,1758,152,898,1759,230,165,156,168,258,169,157,192,171,170,260,259,185,184,241,238,257,174,175])).
% 59.47/59.58 cnf(4326,plain,
% 59.47/59.58 (P4(a15,a17,a17,a21)),
% 59.47/59.58 inference(scs_inference,[],[142,315,1758,152,898,1759,230,165,156,168,258,169,157,192,171,170,260,259,185,184,241,238,257,174,175,176])).
% 59.47/59.58 cnf(4359,plain,
% 59.47/59.58 (P9(a21,a15,a21,a17,a17,a15,a17,a17)),
% 59.47/59.58 inference(scs_inference,[],[4324,229])).
% 59.47/59.58 cnf(4361,plain,
% 59.47/59.58 (P9(a2,a16,x43611,x43612,a2,a16,x43611,x43612)),
% 59.47/59.58 inference(scs_inference,[],[4312,4324,229,230])).
% 59.47/59.58 cnf(4363,plain,
% 59.47/59.58 (P1(a2,a16,a16)),
% 59.47/59.59 inference(scs_inference,[],[4312,4324,229,230,165])).
% 59.47/59.59 cnf(4365,plain,
% 59.47/59.59 (P9(x43651,x43652,a15,a17,x43651,x43652,a17,a15)),
% 59.47/59.59 inference(scs_inference,[],[4312,4310,4324,229,230,165,258])).
% 59.47/59.59 cnf(4369,plain,
% 59.47/59.59 (P1(a15,a17,a15)),
% 59.47/59.59 inference(scs_inference,[],[4312,4310,4290,4298,4324,229,230,165,258,168,156])).
% 59.47/59.59 cnf(4371,plain,
% 59.47/59.59 (P10(a17,a21,a21,a17)),
% 59.47/59.59 inference(scs_inference,[],[4312,4318,4310,4290,4298,4324,229,230,165,258,168,156,169])).
% 59.47/59.59 cnf(4373,plain,
% 59.47/59.59 (P10(x43731,x43732,x43731,x43732)),
% 59.47/59.59 inference(scs_inference,[],[4312,4318,4296,4310,4290,4298,4324,229,230,165,258,168,156,169,238])).
% 59.47/59.59 cnf(4377,plain,
% 59.47/59.59 (P1(a15,a1,a2)),
% 59.47/59.59 inference(scs_inference,[],[4312,4318,4296,4308,4310,4290,4298,4324,854,229,230,165,258,168,156,169,238,257,157])).
% 59.47/59.59 cnf(4379,plain,
% 59.47/59.59 (P3(f7(a2,a15,a25,a18),a2,a2,a18)),
% 59.47/59.59 inference(scs_inference,[],[4312,4318,4296,4308,4310,4290,4298,4324,854,153,229,230,165,258,168,156,169,238,257,157,192])).
% 59.47/59.59 cnf(4385,plain,
% 59.47/59.59 (P4(a21,a17,a15,a17)),
% 59.47/59.59 inference(scs_inference,[],[4312,4306,4318,4296,4308,4310,4290,4298,4322,4324,854,153,229,230,165,258,168,156,169,238,257,157,192,171,174,175])).
% 59.47/59.59 cnf(4389,plain,
% 59.47/59.59 (P9(a15,a17,a17,a15,x43891,x43892,x43891,x43892)),
% 59.47/59.59 inference(scs_inference,[],[4312,4306,4318,4296,4308,4310,4290,4298,4322,4324,4302,854,153,229,230,165,258,168,156,169,238,257,157,192,171,174,175,170,260])).
% 59.47/59.59 cnf(4391,plain,
% 59.47/59.59 (P4(a17,a15,a17,a21)),
% 59.47/59.59 inference(scs_inference,[],[4312,4306,4318,4296,4308,4310,4290,4298,4322,4324,4302,854,153,229,230,165,258,168,156,169,238,257,157,192,171,174,175,170,260,176])).
% 59.47/59.59 cnf(4393,plain,
% 59.47/59.59 (P9(x43931,x43932,a17,a15,x43932,x43931,a17,a15)),
% 59.47/59.59 inference(scs_inference,[],[4312,4306,4318,4296,4308,4310,4290,4298,4322,4324,4302,854,153,229,230,165,258,168,156,169,238,257,157,192,171,174,175,170,260,176,259])).
% 59.47/59.59 cnf(4395,plain,
% 59.47/59.59 (P4(a21,a17,a17,a17)),
% 59.47/59.59 inference(scs_inference,[],[4312,4306,4318,4296,4308,4310,4290,4298,4316,4322,4324,4302,854,153,229,230,165,258,168,156,169,238,257,157,192,171,174,175,170,260,176,259,190])).
% 59.47/59.59 cnf(4397,plain,
% 59.47/59.59 (P3(a20,a19,a16,a2)),
% 59.47/59.59 inference(scs_inference,[],[4312,4306,4318,4296,4308,4310,4290,4298,4316,4322,4324,4302,854,1759,153,229,230,165,258,168,156,169,238,257,157,192,171,174,175,170,260,176,259,190,187])).
% 59.47/59.59 cnf(4399,plain,
% 59.47/59.59 (P4(a15,a15,a17,a15)),
% 59.47/59.59 inference(scs_inference,[],[4312,4306,4318,4296,4308,4310,4290,4298,4316,4322,4324,4302,854,1759,153,229,230,165,258,168,156,169,238,257,157,192,171,174,175,170,260,176,259,190,187,241])).
% 59.47/59.59 cnf(4400,plain,
% 59.47/59.59 (P9(a17,a15,a17,a15,x44001,x44002,x44001,x44002)),
% 59.47/59.59 inference(rename_variables,[],[4308])).
% 59.47/59.59 cnf(4404,plain,
% 59.47/59.59 (P5(a15,a15,a15,a15)),
% 59.47/59.59 inference(scs_inference,[],[4312,4306,4318,4296,4308,4400,4310,4290,4298,4316,4322,4324,4302,854,1759,153,229,230,165,258,168,156,169,238,257,157,192,171,174,175,170,260,176,259,190,187,241,211,256])).
% 59.47/59.59 cnf(4409,plain,
% 59.47/59.59 (P9(a15,a15,a15,a15,a15,a15,a15,a15)),
% 59.47/59.59 inference(scs_inference,[],[4312,4306,4318,4296,4308,4400,4310,4290,4298,4316,4322,4324,4302,854,1759,153,229,230,165,258,168,156,169,238,257,157,192,171,174,175,170,260,176,259,190,187,241,211,256,212,231])).
% 59.47/59.59 cnf(4417,plain,
% 59.47/59.59 (P3(a22,a19,a15,a17)),
% 59.47/59.59 inference(scs_inference,[],[4312,4306,4318,4296,4308,4400,4310,4290,4298,4316,4322,4324,4302,854,1759,151,153,229,230,165,258,168,156,169,238,257,157,192,171,174,175,170,260,176,259,190,187,241,211,256,212,231,183,250,254,246])).
% 59.47/59.59 cnf(4419,plain,
% 59.47/59.59 (P2(a15,a15,a15,a15)),
% 59.47/59.59 inference(scs_inference,[],[4312,4306,4318,4296,4308,4400,4310,4290,4298,4316,4322,4324,4302,854,1759,151,153,229,230,165,258,168,156,169,238,257,157,192,171,174,175,170,260,176,259,190,187,241,211,256,212,231,183,250,254,246,189])).
% 59.47/59.59 cnf(4421,plain,
% 59.47/59.59 (P3(a15,a15,a15,a15)),
% 59.47/59.59 inference(scs_inference,[],[4312,4306,4318,4296,4308,4400,4310,4290,4298,4316,4322,4324,4302,854,1759,151,153,229,230,165,258,168,156,169,238,257,157,192,171,174,175,170,260,176,259,190,187,241,211,256,212,231,183,250,254,246,189,186])).
% 59.47/59.59 cnf(4423,plain,
% 59.47/59.59 (P4(a15,a15,a15,a15)),
% 59.47/59.59 inference(scs_inference,[],[4312,4306,4318,4296,4308,4400,4310,4290,4298,4316,4322,4324,4302,854,1759,151,153,229,230,165,258,168,156,169,238,257,157,192,171,174,175,170,260,176,259,190,187,241,211,256,212,231,183,250,254,246,189,186,201])).
% 59.47/59.59 cnf(4429,plain,
% 59.47/59.59 (P8(a17,a15,a17,a15,a15,a15,a15,a15)),
% 59.47/59.59 inference(scs_inference,[],[4312,4306,4318,4296,4308,4400,4310,4290,4298,4316,4322,4324,4302,854,1759,151,153,229,230,165,258,168,156,169,238,257,157,192,171,174,175,170,260,176,259,190,187,241,211,256,212,231,183,250,254,246,189,186,201,233,262,264])).
% 59.47/59.59 cnf(4431,plain,
% 59.47/59.59 (P8(a15,a17,a15,a15,a17,a15,a15,a15)),
% 59.47/59.59 inference(scs_inference,[],[4312,4306,4318,4296,4308,4400,4310,4290,4298,4316,4322,4324,4302,854,1759,151,153,229,230,165,258,168,156,169,238,257,157,192,171,174,175,170,260,176,259,190,187,241,211,256,212,231,183,250,254,246,189,186,201,233,262,264,263])).
% 59.47/59.59 cnf(4433,plain,
% 59.47/59.59 (~P4(a21,x44331,a19,a24)+~E(x44331,a20)),
% 59.47/59.59 inference(scs_inference,[],[4312,4306,4318,4296,4308,4400,4310,4290,4298,4316,4322,4324,4302,396,854,1759,151,153,229,230,165,258,168,156,169,238,257,157,192,171,174,175,170,260,176,259,190,187,241,211,256,212,231,183,250,254,246,189,186,201,233,262,264,263,133])).
% 59.47/59.59 cnf(4438,plain,
% 59.47/59.59 (P8(a15,a15,a15,a17,a15,a15,a17,a15)),
% 59.47/59.59 inference(scs_inference,[],[4429,4431,261,262])).
% 59.47/59.59 cnf(4440,plain,
% 59.47/59.59 (P8(a15,a17,a17,a15,a15,a15,a15,a15)),
% 59.47/59.59 inference(scs_inference,[],[4429,4431,261,262,264])).
% 59.47/59.59 cnf(4442,plain,
% 59.47/59.59 (P9(a17,a15,a17,a17,a21,a15,a21,a17)),
% 59.47/59.59 inference(scs_inference,[],[4326,4429,4431,261,262,264,229])).
% 59.47/59.59 cnf(4446,plain,
% 59.47/59.59 (P9(x44461,x44462,x44463,x44464,x44461,x44462,x44463,x44464)),
% 59.47/59.59 inference(scs_inference,[],[4373,4326,4371,4429,4431,261,262,264,229,168,230])).
% 59.47/59.59 cnf(4448,plain,
% 59.47/59.59 (P9(a21,a17,a21,a15,a17,a17,a17,a15)),
% 59.47/59.59 inference(scs_inference,[],[4373,4359,4326,4371,4429,4431,261,262,264,229,168,230,258])).
% 59.47/59.59 cnf(4452,plain,
% 59.47/59.59 (P1(x44521,x44522,x44522)),
% 59.47/59.59 inference(scs_inference,[],[4373,4359,4326,4365,4371,4429,4431,261,262,264,229,168,230,258,257,165])).
% 59.47/59.59 cnf(4454,plain,
% 59.47/59.59 (P1(a16,a2,a16)),
% 59.47/59.59 inference(scs_inference,[],[4373,4359,4326,4363,4365,4371,4429,4431,261,262,264,229,168,230,258,257,165,156])).
% 59.47/59.59 cnf(4456,plain,
% 59.47/59.59 (P10(x44561,x44562,x44562,x44561)),
% 59.47/59.59 inference(scs_inference,[],[4373,4359,4326,4363,4365,4371,4429,4431,261,262,264,229,168,230,258,257,165,156,169])).
% 59.47/59.59 cnf(4458,plain,
% 59.47/59.59 (P3(f7(a15,a15,a15,a15),a15,a15,a15)),
% 59.47/59.59 inference(scs_inference,[],[4373,4359,4326,4363,4365,4371,4419,4429,4431,261,262,264,229,168,230,258,257,165,156,169,192])).
% 59.47/59.59 cnf(4460,plain,
% 59.47/59.59 (P1(a15,a15,a17)),
% 59.47/59.59 inference(scs_inference,[],[4373,4359,4326,4363,4365,4369,4371,4419,4429,4431,261,262,264,229,168,230,258,257,165,156,169,192,157])).
% 59.47/59.59 cnf(4464,plain,
% 59.47/59.59 (P4(a17,a21,a15,a17)),
% 59.47/59.59 inference(scs_inference,[],[4373,4359,4326,4363,4365,4369,4371,4385,4419,4429,4431,4379,261,262,264,229,168,230,258,257,165,156,169,192,157,171,174])).
% 59.47/59.59 cnf(4466,plain,
% 59.47/59.59 (P3(a16,a2,a20,a19)),
% 59.47/59.59 inference(scs_inference,[],[4373,4359,4397,4326,4363,4365,4369,4371,4385,4419,4429,4431,4379,261,262,264,229,168,230,258,257,165,156,169,192,157,171,174,170])).
% 59.47/59.59 cnf(4468,plain,
% 59.47/59.59 (P4(a17,a17,a15,a21)),
% 59.47/59.59 inference(scs_inference,[],[4373,4359,4397,4326,4363,4365,4369,4371,4385,4391,4419,4429,4431,4379,261,262,264,229,168,230,258,257,165,156,169,192,157,171,174,170,175])).
% 59.47/59.59 cnf(4470,plain,
% 59.47/59.59 (P9(a21,a15,a17,a15,a21,a17,a17,a17)),
% 59.47/59.59 inference(scs_inference,[],[4373,4359,4397,4326,4363,4365,4369,4371,4385,4391,4419,4429,4431,4379,261,262,264,229,168,230,258,257,165,156,169,192,157,171,174,170,175,260])).
% 59.47/59.59 cnf(4472,plain,
% 59.47/59.59 (P4(a21,a17,a17,a15)),
% 59.47/59.59 inference(scs_inference,[],[4373,4359,4397,4326,4363,4365,4369,4371,4385,4391,4419,4429,4431,4379,261,262,264,229,168,230,258,257,165,156,169,192,157,171,174,170,175,260,176])).
% 59.47/59.59 cnf(4474,plain,
% 59.47/59.59 (P9(a15,a21,a21,a17,a17,a15,a17,a17)),
% 59.47/59.59 inference(scs_inference,[],[4373,4359,4397,4326,4363,4365,4369,4371,4385,4391,4419,4429,4431,4379,261,262,264,229,168,230,258,257,165,156,169,192,157,171,174,170,175,260,176,259])).
% 59.47/59.59 cnf(4476,plain,
% 59.47/59.59 (P1(a15,a15,f3(a15,a15,a15))),
% 59.47/59.59 inference(scs_inference,[],[4373,4359,4397,4326,4421,4363,4365,4369,4371,4385,4391,4404,4419,4429,4431,4379,261,262,264,229,168,230,258,257,165,156,169,192,157,171,174,170,175,260,176,259,181])).
% 59.47/59.59 cnf(4480,plain,
% 59.47/59.59 (P2(f8(a15,a15,a15),a15,a15,a15)),
% 59.47/59.59 inference(scs_inference,[],[4373,4359,4397,4326,4421,4363,4365,4369,4371,4385,4391,4404,4419,4423,4429,4431,4379,261,262,264,229,168,230,258,257,165,156,169,192,157,171,174,170,175,260,176,259,181,193,196])).
% 59.47/59.59 cnf(4494,plain,
% 59.47/59.59 (P5(a15,a15,a15,f32(a15,a15,a15,a15,a15))),
% 59.47/59.59 inference(scs_inference,[],[4373,4359,4397,4409,4326,4421,4363,4365,4369,4371,4385,4391,4404,4419,4423,4429,4431,4379,261,262,264,229,168,230,258,257,165,156,169,192,157,171,174,170,175,260,176,259,181,193,196,198,202,206,251,268,194,204])).
% 59.47/59.59 cnf(4498,plain,
% 59.47/59.59 (P3(f12(a15,a15,a15,a17,a15),a15,a17,a15)),
% 59.47/59.59 inference(scs_inference,[],[4373,4359,4397,4409,4326,4421,4363,4365,4369,4371,4385,4391,4404,4419,4423,4429,4431,4379,261,262,264,229,168,230,258,257,165,156,169,192,157,171,174,170,175,260,176,259,181,193,196,198,202,206,251,268,194,204,195,203])).
% 59.47/59.59 cnf(4503,plain,
% 59.47/59.59 (P2(a15,a15,f3(a15,a15,a15),f3(a15,a15,a15))),
% 59.47/59.59 inference(scs_inference,[],[4373,4359,4397,4409,4326,4421,4363,4365,4369,4371,4385,4391,4404,4419,4423,4429,4431,4379,261,262,264,229,168,230,258,257,165,156,169,192,157,171,174,170,175,260,176,259,181,193,196,198,202,206,251,268,194,204,195,203,246,189])).
% 59.47/59.59 cnf(4505,plain,
% 59.47/59.59 (P5(a17,a15,a17,a15)),
% 59.47/59.59 inference(scs_inference,[],[4373,4359,4397,4409,4326,4421,4363,4365,4369,4371,4385,4391,4404,4419,4423,4429,4431,4379,261,262,264,229,168,230,258,257,165,156,169,192,157,171,174,170,175,260,176,259,181,193,196,198,202,206,251,268,194,204,195,203,246,189,248])).
% 59.47/59.59 cnf(4507,plain,
% 59.47/59.59 (P3(a17,a17,a15,a15)),
% 59.47/59.59 inference(scs_inference,[],[4373,4359,4397,4409,4326,4421,4363,4365,4369,4371,4385,4391,4404,4419,4423,4429,4431,4379,261,262,264,229,168,230,258,257,165,156,169,192,157,171,174,170,175,260,176,259,181,193,196,198,202,206,251,268,194,204,195,203,246,189,248,186])).
% 59.47/59.59 cnf(4509,plain,
% 59.47/59.59 (P4(a16,a1,a2,a2)),
% 59.47/59.59 inference(scs_inference,[],[4373,4359,4397,4409,4326,4421,4363,4361,4365,4369,4371,4385,4391,4404,4419,4423,4429,4431,4379,661,261,262,264,229,168,230,258,257,165,156,169,192,157,171,174,170,175,260,176,259,181,193,196,198,202,206,251,268,194,204,195,203,246,189,248,186,241])).
% 59.47/59.59 cnf(4514,plain,
% 59.47/59.59 (P7(a15,a15,a15)),
% 59.47/59.59 inference(scs_inference,[],[4373,4359,4397,4409,4326,4421,4363,4361,4365,4369,4371,4385,4391,4404,4419,4423,4429,4431,4379,661,261,262,264,229,168,230,258,257,165,156,169,192,157,171,174,170,175,260,176,259,181,193,196,198,202,206,251,268,194,204,195,203,246,189,248,186,241,201,244])).
% 59.47/59.59 cnf(4518,plain,
% 59.47/59.59 (P7(f27(a15,x45181),a15,x45181)),
% 59.47/59.59 inference(scs_inference,[],[4373,4359,4397,4409,4326,4421,4363,4361,4365,4369,4371,4385,4391,4404,4419,4423,4429,4431,4379,4298,661,261,262,264,229,168,230,258,257,165,156,169,192,157,171,174,170,175,260,176,259,181,193,196,198,202,206,251,268,194,204,195,203,246,189,248,186,241,201,244,211,164])).
% 59.47/59.59 cnf(4522,plain,
% 59.47/59.59 (P5(a15,a15,f3(a15,a15,a15),a15)),
% 59.47/59.59 inference(scs_inference,[],[4373,4359,4397,4409,4326,4421,4363,4361,4365,4369,4371,4385,4391,4404,4419,4423,4429,4431,4379,4298,661,261,262,264,229,168,230,258,257,165,156,169,192,157,171,174,170,175,260,176,259,181,193,196,198,202,206,251,268,194,204,195,203,246,189,248,186,241,201,244,211,164,212,173])).
% 59.47/59.59 cnf(4524,plain,
% 59.47/59.59 (P5(a15,f3(a15,a15,a15),a15,a15)),
% 59.47/59.59 inference(scs_inference,[],[4373,4359,4397,4409,4326,4421,4363,4361,4365,4369,4371,4385,4391,4404,4419,4423,4429,4431,4379,4298,661,261,262,264,229,168,230,258,257,165,156,169,192,157,171,174,170,175,260,176,259,181,193,196,198,202,206,251,268,194,204,195,203,246,189,248,186,241,201,244,211,164,212,173,172])).
% 59.47/59.59 cnf(4526,plain,
% 59.47/59.59 (P5(f27(a15,x45261),a15,f27(a15,x45261),x45261)),
% 59.47/59.59 inference(scs_inference,[],[4373,4359,4397,4409,4326,4421,4363,4361,4365,4369,4371,4385,4391,4404,4419,4423,4429,4431,4379,4298,661,261,262,264,229,168,230,258,257,165,156,169,192,157,171,174,170,175,260,176,259,181,193,196,198,202,206,251,268,194,204,195,203,246,189,248,186,241,201,244,211,164,212,173,172,161])).
% 59.47/59.59 cnf(4532,plain,
% 59.47/59.59 (P7(f27(a15,x45321),x45321,a15)),
% 59.47/59.59 inference(scs_inference,[],[4373,4359,4397,4409,4326,4421,4363,4361,4365,4369,4371,4385,4391,4404,4419,4423,4429,4431,4379,4298,661,261,262,264,229,168,230,258,257,165,156,169,192,157,171,174,170,175,260,176,259,181,193,196,198,202,206,251,268,194,204,195,203,246,189,248,186,241,201,244,211,164,212,173,172,161,231,158,159])).
% 59.47/59.59 cnf(4534,plain,
% 59.47/59.59 (P8(a15,a17,a17,a15,a17,a15,a17,a15)),
% 59.47/59.59 inference(scs_inference,[],[4373,4359,4397,4409,4326,4421,4363,4361,4365,4369,4371,4385,4391,4404,4419,4423,4429,4431,4379,4298,661,261,262,264,229,168,230,258,257,165,156,169,192,157,171,174,170,175,260,176,259,181,193,196,198,202,206,251,268,194,204,195,203,246,189,248,186,241,201,244,211,164,212,173,172,161,231,158,159,263])).
% 59.47/59.59 cnf(4536,plain,
% 59.47/59.59 (P10(a15,a15,a15,f3(a15,a15,a15))),
% 59.47/59.59 inference(scs_inference,[],[4373,4359,4397,4409,4326,4421,4363,4361,4365,4369,4371,4385,4391,4404,4419,4423,4429,4431,4379,4298,661,261,262,264,229,168,230,258,257,165,156,169,192,157,171,174,170,175,260,176,259,181,193,196,198,202,206,251,268,194,204,195,203,246,189,248,186,241,201,244,211,164,212,173,172,161,231,158,159,263,238])).
% 59.47/59.59 cnf(4540,plain,
% 59.47/59.59 (P1(f23(a15,a15,a17,a15),a17,a15)),
% 59.47/59.59 inference(scs_inference,[],[4373,4359,4397,4409,4326,4421,4363,4361,4365,4389,4369,4371,4385,4391,4404,4419,4423,4429,4431,4379,4298,661,261,262,264,229,168,230,258,257,165,156,169,192,157,171,174,170,175,260,176,259,181,193,196,198,202,206,251,268,194,204,195,203,246,189,248,186,241,201,244,211,164,212,173,172,161,231,158,159,263,238,199,254])).
% 59.47/59.59 cnf(4595,plain,
% 59.47/59.59 (P1(f27(a15,x45951),x45951,a15)),
% 59.47/59.59 inference(scs_inference,[],[4440,4505,4494,4532,261,172,173,158])).
% 59.47/59.59 cnf(4597,plain,
% 59.47/59.59 (P5(f27(a15,x45971),x45971,f27(a15,x45971),a15)),
% 59.47/59.59 inference(scs_inference,[],[4440,4505,4494,4532,261,172,173,158,161])).
% 59.47/59.59 cnf(4601,plain,
% 59.47/59.59 (P8(a15,a17,a15,a17,a15,a15,a15,a15)),
% 59.47/59.59 inference(scs_inference,[],[4440,4505,4494,4532,261,172,173,158,161,262,263])).
% 59.47/59.59 cnf(4603,plain,
% 59.47/59.59 (P9(a17,a15,a15,a15,a15,a15,a17,a15)),
% 59.47/59.59 inference(scs_inference,[],[4440,4505,4494,4532,261,172,173,158,161,262,263,231])).
% 59.47/59.59 cnf(4605,plain,
% 59.47/59.59 (P10(a15,f3(a15,a15,a15),a15,a15)),
% 59.47/59.59 inference(scs_inference,[],[4440,4505,4494,4532,4536,261,172,173,158,161,262,263,231,168])).
% 59.47/59.59 cnf(4607,plain,
% 59.47/59.59 (P8(a17,a15,a15,a15,a15,a17,a15,a15)),
% 59.47/59.59 inference(scs_inference,[],[4440,4505,4494,4532,4536,261,172,173,158,161,262,263,231,168,264])).
% 59.47/59.59 cnf(4611,plain,
% 59.47/59.59 (P9(a15,a17,a15,a21,a17,a17,a17,a21)),
% 59.47/59.59 inference(scs_inference,[],[4440,4464,4505,4494,4532,4536,261,172,173,158,161,262,263,231,168,264,165,229])).
% 59.47/59.59 cnf(4613,plain,
% 59.47/59.59 (P9(x46131,x46132,x46133,x46134,x46132,x46131,x46133,x46134)),
% 59.47/59.59 inference(scs_inference,[],[4456,4440,4464,4505,4494,4532,4536,261,172,173,158,161,262,263,231,168,264,165,229,230])).
% 59.47/59.59 cnf(4615,plain,
% 59.47/59.59 (P9(a17,a17,a17,a15,a21,a17,a21,a15)),
% 59.47/59.59 inference(scs_inference,[],[4456,4440,4442,4464,4505,4494,4532,4536,261,172,173,158,161,262,263,231,168,264,165,229,230,258])).
% 59.47/59.59 cnf(4617,plain,
% 59.47/59.59 (P10(a15,a15,f3(a15,a15,a15),a15)),
% 59.47/59.59 inference(scs_inference,[],[4456,4440,4442,4464,4505,4494,4532,4536,261,172,173,158,161,262,263,231,168,264,165,229,230,258,169])).
% 59.47/59.59 cnf(4619,plain,
% 59.47/59.59 (P1(x46191,x46192,x46191)),
% 59.47/59.59 inference(scs_inference,[],[4456,4452,4440,4442,4464,4505,4494,4532,4536,261,172,173,158,161,262,263,231,168,264,165,229,230,258,169,156])).
% 59.47/59.59 cnf(4627,plain,
% 59.47/59.59 (P4(a17,a21,a17,a17)),
% 59.47/59.59 inference(scs_inference,[],[4456,4452,4440,4442,4470,4464,4454,4395,4505,4494,4532,4536,154,261,172,173,158,161,262,263,231,168,264,165,229,230,258,169,156,257,157,192,174])).
% 59.47/59.59 cnf(4631,plain,
% 59.47/59.59 (P3(a15,a17,a22,a19)),
% 59.47/59.59 inference(scs_inference,[],[4456,4452,4440,4442,4470,4417,4464,4454,4395,4466,4505,4494,4532,4536,154,261,172,173,158,161,262,263,231,168,264,165,229,230,258,169,156,257,157,192,174,171,170])).
% 59.47/59.59 cnf(4633,plain,
% 59.47/59.59 (P4(a16,a2,a1,a2)),
% 59.47/59.59 inference(scs_inference,[],[4456,4452,4440,4442,4470,4417,4464,4454,4395,4466,4505,4509,4494,4532,4536,154,261,172,173,158,161,262,263,231,168,264,165,229,230,258,169,156,257,157,192,174,171,170,175])).
% 59.47/59.59 cnf(4635,plain,
% 59.47/59.59 (P9(x46351,x46352,x46351,x46352,x46353,x46354,x46353,x46354)),
% 59.47/59.59 inference(scs_inference,[],[4446,4456,4452,4440,4442,4470,4417,4464,4454,4395,4466,4505,4509,4494,4532,4536,154,261,172,173,158,161,262,263,231,168,264,165,229,230,258,169,156,257,157,192,174,171,170,175,260])).
% 59.47/59.59 cnf(4637,plain,
% 59.47/59.59 (P9(a15,a17,a17,a17,a21,a15,a21,a17)),
% 59.47/59.59 inference(scs_inference,[],[4446,4456,4452,4440,4442,4470,4417,4464,4454,4395,4466,4505,4509,4494,4532,4536,154,261,172,173,158,161,262,263,231,168,264,165,229,230,258,169,156,257,157,192,174,171,170,175,260,259])).
% 59.47/59.59 cnf(4641,plain,
% 59.47/59.59 (P5(a15,f3(a15,a15,a15),a15,f32(a15,a15,a15,a15,a15))),
% 59.47/59.59 inference(scs_inference,[],[4446,4456,4452,4440,4442,4470,4417,4464,4454,4395,4466,4505,4509,4494,4532,4536,4524,154,261,172,173,158,161,262,263,231,168,264,165,229,230,258,169,156,257,157,192,174,171,170,175,260,259,176,188])).
% 59.47/59.59 cnf(4643,plain,
% 59.47/59.59 (P5(f7(a15,a15,a15,a15),a15,f7(a15,a15,a15,a15),a15)),
% 59.47/59.59 inference(scs_inference,[],[4446,4456,4452,4514,4440,4442,4470,4417,4464,4454,4395,4466,4505,4509,4494,4532,4536,4524,4458,154,261,172,173,158,161,262,263,231,168,264,165,229,230,258,169,156,257,157,192,174,171,170,175,260,259,176,188,178])).
% 59.47/59.59 cnf(4647,plain,
% 59.47/59.59 (P10(f30(a15,a15,a15,a15,a15,a15),a15,a15,a15)),
% 59.47/59.59 inference(scs_inference,[],[4446,4456,4452,4514,4440,4442,4470,4417,4464,4454,4395,4466,4505,4507,4509,4494,4532,4536,4524,4458,154,261,172,173,158,161,262,263,231,168,264,165,229,230,258,169,156,257,157,192,174,171,170,175,260,259,176,188,178,198,210])).
% 59.47/59.59 cnf(4650,plain,
% 59.47/59.59 (P1(x46501,x46502,x46502)),
% 59.47/59.59 inference(rename_variables,[],[4452])).
% 59.47/59.59 cnf(4653,plain,
% 59.47/59.59 (P9(x46531,x46532,a17,a15,x46532,x46531,a17,a15)),
% 59.47/59.59 inference(rename_variables,[],[4393])).
% 59.47/59.59 cnf(4660,plain,
% 59.47/59.59 (P7(f30(a15,a15,a15,a15,a15,a15),a15,a15)),
% 59.47/59.59 inference(scs_inference,[],[4446,4456,4452,4514,4440,4442,4470,4417,4464,4454,4395,4466,4505,4507,4509,4494,4532,4536,4524,4498,4458,4393,4653,4421,154,261,172,173,158,161,262,263,231,168,264,165,229,230,258,169,156,257,157,192,174,171,170,175,260,259,176,188,178,198,210,203,250,228,246,208])).
% 59.47/59.59 cnf(4662,plain,
% 59.47/59.59 (P2(a17,a15,a15,a15)),
% 59.47/59.59 inference(scs_inference,[],[4446,4456,4452,4514,4440,4442,4470,4417,4464,4454,4395,4466,4505,4507,4509,4494,4532,4536,4524,4498,4458,4393,4653,4421,154,261,172,173,158,161,262,263,231,168,264,165,229,230,258,169,156,257,157,192,174,171,170,175,260,259,176,188,178,198,210,203,250,228,246,208,189])).
% 59.47/59.59 cnf(4667,plain,
% 59.47/59.59 (P3(a15,f3(a15,a15,a15),f3(a15,a15,a15),f3(a15,a15,a15))),
% 59.47/59.59 inference(scs_inference,[],[4446,4456,4452,4514,4440,4442,4470,4417,4464,4454,4395,4466,4505,4507,4509,4494,4526,4532,4503,4536,4524,4498,4476,4458,4393,4653,4421,154,261,172,173,158,161,262,263,231,168,264,165,229,230,258,169,156,257,157,192,174,171,170,175,260,259,176,188,178,198,210,203,250,228,246,208,189,186,177])).
% 59.47/59.59 cnf(4669,plain,
% 59.47/59.59 (P5(a15,a17,a17,a15)),
% 59.47/59.59 inference(scs_inference,[],[4446,4456,4452,4514,4440,4442,4470,4417,4464,4454,4395,4466,4505,4507,4509,4494,4526,4532,4503,4536,4524,4498,4476,4458,4393,4653,4404,4421,154,261,172,173,158,161,262,263,231,168,264,165,229,230,258,169,156,257,157,192,174,171,170,175,260,259,176,188,178,198,210,203,250,228,246,208,189,186,177,248])).
% 59.47/59.59 cnf(4672,plain,
% 59.47/59.59 (P9(x46721,x46722,x46723,x46724,x46721,x46722,x46723,x46724)),
% 59.47/59.59 inference(rename_variables,[],[4446])).
% 59.47/59.59 cnf(4674,plain,
% 59.47/59.59 (P4(x46741,x46742,x46742,x46742)),
% 59.47/59.59 inference(scs_inference,[],[4446,4672,4456,4452,4650,4514,4440,4442,4470,4417,4464,4454,4395,4466,4505,4507,4509,4494,4526,4532,4503,4536,4524,4498,4476,4458,4480,4393,4653,4404,4421,154,261,172,173,158,161,262,263,231,168,264,165,229,230,258,169,156,257,157,192,174,171,170,175,260,259,176,188,178,198,210,203,250,228,246,208,189,186,177,248,247,241])).
% 59.47/59.59 cnf(4675,plain,
% 59.47/59.59 (P1(x46751,x46752,x46752)),
% 59.47/59.59 inference(rename_variables,[],[4452])).
% 59.47/59.59 cnf(4676,plain,
% 59.47/59.59 (P9(x46761,x46762,x46763,x46764,x46761,x46762,x46763,x46764)),
% 59.47/59.59 inference(rename_variables,[],[4446])).
% 59.47/59.59 cnf(4682,plain,
% 59.47/59.59 (P10(x46821,x46822,x46822,x46821)),
% 59.47/59.59 inference(rename_variables,[],[4456])).
% 59.47/59.59 cnf(4684,plain,
% 59.47/59.59 (P7(f3(a15,a15,a15),f3(a15,a15,a15),f3(a15,a15,a15))),
% 59.47/59.59 inference(scs_inference,[],[4446,4672,4676,4456,4452,4650,4675,4514,4440,4442,4470,4417,4464,4454,4395,4466,4505,4507,4509,4494,4526,4518,4532,4503,4536,4524,4498,4476,4458,4480,4393,4653,4423,4404,4421,154,261,172,173,158,161,262,263,231,168,264,165,229,230,258,169,156,257,157,192,174,171,170,175,260,259,176,188,178,198,210,203,250,228,246,208,189,186,177,248,247,241,232,197,244])).
% 59.47/59.59 cnf(4690,plain,
% 59.47/59.59 (P7(a15,f3(a15,a15,a15),a15)),
% 59.47/59.59 inference(scs_inference,[],[4446,4672,4676,4456,4452,4650,4675,4514,4440,4442,4470,4417,4464,4454,4395,4466,4505,4507,4509,4494,4526,4518,4532,4503,4536,4524,4498,4476,4458,4480,4393,4653,4423,4404,4421,154,261,172,173,158,161,262,263,231,168,264,165,229,230,258,169,156,257,157,192,174,171,170,175,260,259,176,188,178,198,210,203,250,228,246,208,189,186,177,248,247,241,232,197,244,191,180])).
% 59.47/59.59 cnf(4693,plain,
% 59.47/59.59 (P10(x46931,x46932,x46932,x46931)),
% 59.47/59.59 inference(rename_variables,[],[4456])).
% 59.47/59.59 cnf(4695,plain,
% 59.47/59.59 (P7(f27(a17,x46951),a17,x46951)),
% 59.47/59.59 inference(scs_inference,[],[142,4446,4672,4676,4456,4682,4452,4650,4675,4514,4300,4440,4442,4470,4417,4464,4454,4395,4466,4505,4507,4509,4494,4526,4518,4532,4503,4536,4524,4498,4476,4458,4480,4393,4653,4423,4369,4404,4421,154,261,172,173,158,161,262,263,231,168,264,165,229,230,258,169,156,257,157,192,174,171,170,175,260,259,176,188,178,198,210,203,250,228,246,208,189,186,177,248,247,241,232,197,244,191,180,211,164])).
% 59.47/59.59 cnf(4698,plain,
% 59.47/59.59 (P1(f13(a2,a15,a15,a2,a1,a1),a15,a2)),
% 59.47/59.59 inference(scs_inference,[],[142,4446,4672,4676,4456,4682,4693,4452,4650,4675,4514,4300,4440,4442,4470,4417,4464,4454,4395,4466,4505,4507,4509,4494,4526,4518,4532,4503,4536,4524,4498,4476,4458,4480,4393,4653,4423,4369,4404,4421,154,261,172,173,158,161,262,263,231,168,264,165,229,230,258,169,156,257,157,192,174,171,170,175,260,259,176,188,178,198,210,203,250,228,246,208,189,186,177,248,247,241,232,197,244,191,180,211,164,212])).
% 59.47/59.59 cnf(4703,plain,
% 59.47/59.59 (P7(a15,a15,f3(a15,a15,a15))),
% 59.47/59.59 inference(scs_inference,[],[142,4446,4672,4676,4456,4682,4693,4452,4650,4675,4514,4300,4440,4442,4470,4417,4464,4454,4395,4466,4505,4507,4509,4494,4526,4518,4532,4503,4536,4524,4498,4476,4458,4480,4393,4653,4423,4369,4404,4421,154,261,172,173,158,161,262,263,231,168,264,165,229,230,258,169,156,257,157,192,174,171,170,175,260,259,176,188,178,198,210,203,250,228,246,208,189,186,177,248,247,241,232,197,244,191,180,211,164,212,949,159])).
% 59.47/59.59 cnf(4705,plain,
% 59.47/59.59 (P9(a15,f3(a15,a15,a15),a15,f3(a15,a15,a15),a15,f3(a15,a15,a15),a15,a15)+~P4(a15,a15,a15,f3(a15,a15,a15))),
% 59.47/59.59 inference(scs_inference,[],[142,4446,4672,4676,4456,4682,4693,4452,4650,4675,4514,4300,4440,4442,4470,4417,4464,4454,4395,4466,4505,4507,4509,4494,4526,4518,4532,4503,4536,4524,4498,4476,4458,4480,4393,4653,4423,4369,4404,4421,154,261,172,173,158,161,262,263,231,168,264,165,229,230,258,169,156,257,157,192,174,171,170,175,260,259,176,188,178,198,210,203,250,228,246,208,189,186,177,248,247,241,232,197,244,191,180,211,164,212,949,159,235])).
% 59.47/59.59 cnf(4717,plain,
% 59.47/59.59 (P5(a15,a17,a15,a17)),
% 59.47/59.59 inference(scs_inference,[],[4438,4669,4684,4641,261,161,172,173])).
% 59.47/59.59 cnf(4719,plain,
% 59.47/59.59 (P10(a15,a15,f30(a15,a15,a15,a15,a15,a15),a15)),
% 59.47/59.59 inference(scs_inference,[],[4438,4669,4684,4647,4641,261,161,172,173,168])).
% 59.47/59.59 cnf(4721,plain,
% 59.47/59.59 (P8(a17,a15,a15,a17,a17,a15,a17,a15)),
% 59.47/59.59 inference(scs_inference,[],[4438,4534,4669,4684,4647,4641,261,161,172,173,168,262])).
% 59.47/59.59 cnf(4723,plain,
% 59.47/59.59 (P1(f27(a17,x47231),a17,x47231)),
% 59.47/59.59 inference(scs_inference,[],[4438,4534,4669,4684,4647,4695,4641,261,161,172,173,168,262,158])).
% 59.47/59.59 cnf(4725,plain,
% 59.47/59.59 (P7(f27(a17,x47251),x47251,a17)),
% 59.47/59.59 inference(scs_inference,[],[4438,4534,4669,4684,4647,4695,4641,261,161,172,173,168,262,158,159])).
% 59.47/59.59 cnf(4727,plain,
% 59.47/59.59 (P8(a15,a17,a15,a15,a15,a17,a15,a15)),
% 59.47/59.59 inference(scs_inference,[],[4438,4534,4607,4669,4684,4647,4695,4641,261,161,172,173,168,262,158,159,263])).
% 59.47/59.59 cnf(4729,plain,
% 59.47/59.59 (P9(f30(a15,a15,a15,a15,a15,a15),a15,x47291,x47292,a15,a15,x47291,x47292)),
% 59.47/59.59 inference(scs_inference,[],[4438,4534,4607,4669,4684,4647,4695,4641,261,161,172,173,168,262,158,159,263,230])).
% 59.47/59.59 cnf(4733,plain,
% 59.47/59.59 (P9(f27(a15,x47331),x47331,x47331,a15,x47331,a15,f27(a15,x47331),a15)),
% 59.47/59.59 inference(scs_inference,[],[4438,4534,4607,4669,4684,4647,4597,4695,4641,261,161,172,173,168,262,158,159,263,230,169,231])).
% 59.47/59.59 cnf(4737,plain,
% 59.47/59.59 (P9(a17,a21,a17,a17,a15,a21,a15,a17)),
% 59.47/59.59 inference(scs_inference,[],[4438,4534,4472,4607,4669,4684,4647,4597,4695,4641,261,161,172,173,168,262,158,159,263,230,169,231,264,229])).
% 59.47/59.59 cnf(4739,plain,
% 59.47/59.59 (P9(x47391,x47392,x47393,x47394,x47391,x47392,x47394,x47393)),
% 59.47/59.59 inference(scs_inference,[],[4613,4438,4534,4472,4607,4669,4684,4647,4597,4695,4641,261,161,172,173,168,262,158,159,263,230,169,231,264,229,258])).
% 59.47/59.59 cnf(4741,plain,
% 59.47/59.59 (P4(x47411,x47412,x47411,x47411)),
% 59.47/59.59 inference(scs_inference,[],[4613,4674,4438,4534,4472,4607,4669,4684,4647,4597,4695,4641,261,161,172,173,168,262,158,159,263,230,169,231,264,229,258,174])).
% 59.47/59.59 cnf(4743,plain,
% 59.47/59.59 (P1(x47431,x47431,x47432)),
% 59.47/59.59 inference(scs_inference,[],[4613,4674,4619,4438,4534,4472,4607,4669,4684,4647,4597,4695,4641,261,161,172,173,168,262,158,159,263,230,169,231,264,229,258,174,157])).
% 59.47/59.59 cnf(4745,plain,
% 59.47/59.59 (P3(a15,a17,a19,a22)),
% 59.47/59.59 inference(scs_inference,[],[4613,4674,4619,4438,4534,4472,4607,4631,4669,4684,4647,4597,4695,4641,261,161,172,173,168,262,158,159,263,230,169,231,264,229,258,174,157,171])).
% 59.47/59.59 cnf(4749,plain,
% 59.47/59.59 (P1(a17,f23(a15,a15,a17,a15),a15)),
% 59.47/59.59 inference(scs_inference,[],[4613,4674,4619,4438,4534,4472,4607,4631,4662,4669,4684,4647,4540,4597,4695,4641,261,161,172,173,168,262,158,159,263,230,169,231,264,229,258,174,157,171,192,156])).
% 59.47/59.59 cnf(4753,plain,
% 59.47/59.59 (P3(f3(a15,a15,a15),f3(a15,a15,a15),a15,f3(a15,a15,a15))),
% 59.47/59.59 inference(scs_inference,[],[4613,4674,4619,4474,4438,4534,4472,4607,4631,4662,4669,4684,4647,4667,4540,4597,4695,4641,261,161,172,173,168,262,158,159,263,230,169,231,264,229,258,174,157,171,192,156,257,170])).
% 59.47/59.59 cnf(4755,plain,
% 59.47/59.59 (P4(a17,a17,a21,a15)),
% 59.47/59.59 inference(scs_inference,[],[4613,4674,4619,4474,4438,4534,4468,4472,4607,4631,4662,4669,4684,4647,4667,4540,4597,4695,4641,261,161,172,173,168,262,158,159,263,230,169,231,264,229,258,174,157,171,192,156,257,170,176])).
% 59.47/59.59 cnf(4757,plain,
% 59.47/59.59 (P9(x47571,x47572,x47572,x47571,x47573,x47574,x47573,x47574)),
% 59.47/59.59 inference(scs_inference,[],[4613,4674,4619,4474,4438,4534,4468,4472,4607,4631,4662,4669,4684,4647,4667,4540,4597,4695,4641,261,161,172,173,168,262,158,159,263,230,169,231,264,229,258,174,157,171,192,156,257,170,176,260])).
% 59.47/59.59 cnf(4763,plain,
% 59.47/59.59 (P5(a15,f30(a15,a15,a15,a15,a15,a15),a15,f30(a15,a15,a15,a15,a15,a15))),
% 59.47/59.59 inference(scs_inference,[],[4613,4674,4619,4448,4474,4438,4534,4468,4472,4607,4627,4631,4662,4669,4684,4647,4667,4540,4660,4597,4695,4641,4421,261,161,172,173,168,262,158,159,263,230,169,231,264,229,258,174,157,171,192,156,257,170,176,260,259,175,179])).
% 59.47/59.59 cnf(4765,plain,
% 59.47/59.59 (P10(a15,f30(a15,a15,a15,a15,a15,a15),a15,a15)),
% 59.47/59.59 inference(scs_inference,[],[4613,4674,4619,4448,4474,4438,4534,4468,4472,4607,4627,4631,4662,4669,4684,4647,4667,4540,4660,4597,4695,4641,4421,261,161,172,173,168,262,158,159,263,230,169,231,264,229,258,174,157,171,192,156,257,170,176,260,259,175,179,245])).
% 59.47/59.59 cnf(4766,plain,
% 59.47/59.59 (P9(x47661,x47662,x47663,x47664,x47662,x47661,x47663,x47664)),
% 59.47/59.59 inference(rename_variables,[],[4613])).
% 59.47/59.59 cnf(4768,plain,
% 59.47/59.59 (P5(a15,f3(a15,a15,a15),a15,f3(a15,a15,a15))),
% 59.47/59.59 inference(scs_inference,[],[4613,4674,4619,4448,4474,4438,4534,4468,4472,4607,4627,4631,4662,4669,4684,4647,4667,4540,4660,4597,4695,4641,4421,261,161,172,173,168,262,158,159,263,230,169,231,264,229,258,174,157,171,192,156,257,170,176,260,259,175,179,245,178])).
% 59.47/59.59 cnf(4770,plain,
% 59.47/59.59 (P9(x47701,x47702,x47701,x47702,x47703,x47704,x47704,x47703)),
% 59.47/59.59 inference(scs_inference,[],[4613,4766,4635,4674,4619,4448,4474,4438,4534,4468,4472,4607,4627,4631,4662,4669,4684,4647,4667,4540,4660,4597,4695,4641,4421,261,161,172,173,168,262,158,159,263,230,169,231,264,229,258,174,157,171,192,156,257,170,176,260,259,175,179,245,178,267])).
% 59.47/59.59 cnf(4771,plain,
% 59.47/59.59 (P9(x47711,x47712,x47711,x47712,x47713,x47714,x47713,x47714)),
% 59.47/59.59 inference(rename_variables,[],[4635])).
% 59.47/59.59 cnf(4772,plain,
% 59.47/59.59 (P9(x47721,x47722,x47723,x47724,x47722,x47721,x47723,x47724)),
% 59.47/59.59 inference(rename_variables,[],[4613])).
% 59.47/59.59 cnf(4776,plain,
% 59.47/59.59 (P3(a17,a15,a22,a19)),
% 59.47/59.59 inference(scs_inference,[],[4613,4766,4772,4635,4674,4619,4448,4474,4438,4534,4468,4472,4607,4627,4631,4662,4669,4684,4647,4667,4703,4540,4660,4597,4695,4641,4421,261,161,172,173,168,262,158,159,263,230,169,231,264,229,258,174,157,171,192,156,257,170,176,260,259,175,179,245,178,267,228,246])).
% 59.47/59.59 cnf(4777,plain,
% 59.47/59.59 (P9(x47771,x47772,x47773,x47774,x47772,x47771,x47773,x47774)),
% 59.47/59.59 inference(rename_variables,[],[4613])).
% 59.47/59.59 cnf(4783,plain,
% 59.47/59.59 (P4(a15,a15,a1,a2)),
% 59.47/59.59 inference(scs_inference,[],[142,4613,4766,4772,4635,4771,4674,4619,4448,4474,4438,4534,4468,4472,4607,4627,4631,4662,4669,4684,4647,4667,4703,4540,4660,4597,4695,4641,4643,4421,261,161,172,173,168,262,158,159,263,230,169,231,264,229,258,174,157,171,192,156,257,170,176,260,259,175,179,245,178,267,228,246,189,186,241])).
% 59.47/59.59 cnf(4784,plain,
% 59.47/59.59 (P9(x47841,x47842,x47841,x47842,x47843,x47844,x47843,x47844)),
% 59.47/59.59 inference(rename_variables,[],[4635])).
% 59.47/59.59 cnf(4790,plain,
% 59.47/59.59 (P5(x47901,x47901,x47901,x47901)),
% 59.47/59.59 inference(scs_inference,[],[142,4613,4766,4772,4777,4635,4771,4674,4619,4448,4474,4438,4534,4468,4472,4607,4627,4631,4662,4669,4684,4647,4667,4703,4540,4660,4597,4695,4641,4643,4399,4404,4421,261,161,172,173,168,262,158,159,263,230,169,231,264,229,258,174,157,171,192,156,257,170,176,260,259,175,179,245,178,267,228,246,189,186,241,232,200,256])).
% 59.47/59.59 cnf(4792,plain,
% 59.47/59.59 (P9(x47921,x47922,x47923,x47924,x47922,x47921,x47923,x47924)),
% 59.47/59.59 inference(rename_variables,[],[4613])).
% 59.47/59.59 cnf(4796,plain,
% 59.47/59.59 (P1(x47961,x47962,x47961)),
% 59.47/59.59 inference(rename_variables,[],[4619])).
% 59.47/59.59 cnf(4805,plain,
% 59.47/59.59 (P9(x48051,x48052,x48053,x48054,x48052,x48051,x48053,x48054)),
% 59.47/59.59 inference(rename_variables,[],[4613])).
% 59.47/59.59 cnf(4807,plain,
% 59.47/59.59 (P1(f23(a17,a17,a15,a17),a15,a17)),
% 59.47/59.59 inference(scs_inference,[],[142,4613,4766,4772,4777,4792,4805,4635,4771,4784,4674,4619,4448,4474,4438,4534,4460,4468,4472,4607,4627,4631,4662,4669,4684,4647,4667,4703,4540,4660,4597,4695,4641,4643,4399,4470,4456,4404,4421,261,161,172,173,168,262,158,159,263,230,169,231,264,229,258,174,157,171,192,156,257,170,176,260,259,175,179,245,178,267,228,246,189,186,241,232,200,256,212,249,252,255,254])).
% 59.47/59.59 cnf(4813,plain,
% 59.47/59.59 (P3(x48131,a15,a15,a15)),
% 59.47/59.59 inference(scs_inference,[],[142,4613,4766,4772,4777,4792,4805,4635,4771,4784,4674,4619,4796,4448,4474,4438,4534,4460,4468,4472,4607,4627,4631,4662,4669,4684,4647,4667,4703,4540,4660,4597,4595,4695,4641,4643,4399,4470,4456,4404,4421,261,161,172,173,168,262,158,159,263,230,169,231,264,229,258,174,157,171,192,156,257,170,176,260,259,175,179,245,178,267,228,246,189,186,241,232,200,256,212,249,252,255,254,203,177])).
% 59.47/59.59 cnf(4816,plain,
% 59.47/59.59 (~P4(a21,a24,a19,x48161)+~E(x48161,a20)),
% 59.47/59.59 inference(scs_inference,[],[142,4613,4766,4772,4777,4792,4805,4635,4771,4784,4674,4619,4796,4448,4474,4438,4534,4460,4468,4472,4607,4627,4631,4662,4669,4684,4647,4667,4703,4540,4660,4597,4595,4695,4641,4643,4399,4470,382,4456,4404,4421,261,161,172,173,168,262,158,159,263,230,169,231,264,229,258,174,157,171,192,156,257,170,176,260,259,175,179,245,178,267,228,246,189,186,241,232,200,256,212,249,252,255,254,203,177,135])).
% 59.47/59.59 cnf(4822,plain,
% 59.47/59.59 (P8(a17,a15,a17,a15,a17,a15,a15,a17)),
% 59.47/59.59 inference(scs_inference,[],[4721,261])).
% 59.47/59.59 cnf(4826,plain,
% 59.47/59.59 (P5(f27(a17,x48261),x48261,f27(a17,x48261),a17)),
% 59.47/59.59 inference(scs_inference,[],[4721,4617,4725,261,168,161])).
% 59.47/59.59 cnf(4828,plain,
% 59.47/59.59 (P8(a15,a17,a15,a17,a17,a15,a17,a15)),
% 59.47/59.59 inference(scs_inference,[],[4721,4617,4725,261,168,161,263])).
% 59.47/59.59 cnf(4830,plain,
% 59.47/59.59 (P8(a15,a15,a15,a17,a15,a15,a15,a17)),
% 59.47/59.59 inference(scs_inference,[],[4727,4721,4617,4725,261,168,161,263,262])).
% 59.47/59.59 cnf(4840,plain,
% 59.47/59.59 (P9(a15,a15,a17,a15,a17,a15,a15,a15)),
% 59.47/59.59 inference(scs_inference,[],[4603,4727,4721,4617,4522,4725,4763,261,168,161,263,262,173,172,158,264,258])).
% 59.47/59.59 cnf(4846,plain,
% 59.47/59.59 (P9(a15,a17,a17,a17,a17,a17,a15,a17)),
% 59.47/59.59 inference(scs_inference,[],[4603,4727,4717,4633,4721,4617,4522,4725,4763,261,168,161,263,262,173,172,158,264,258,230,229,231])).
% 59.47/59.59 cnf(4850,plain,
% 59.47/59.59 (P9(a17,a17,a17,a21,a15,a17,a15,a21)),
% 59.47/59.59 inference(scs_inference,[],[4603,4611,4727,4717,4633,4721,4617,4522,4723,4725,4763,261,168,161,263,262,173,172,158,264,258,230,229,231,156,257])).
% 59.47/59.59 cnf(4854,plain,
% 59.47/59.59 (P4(a2,a16,a1,a2)),
% 59.47/59.59 inference(scs_inference,[],[4603,4611,4727,4717,4633,4721,4776,4617,4522,4723,4725,4763,261,168,161,263,262,173,172,158,264,258,230,229,231,156,257,171,174])).
% 59.47/59.59 cnf(4858,plain,
% 59.47/59.59 (P3(a15,a15,x48581,a15)),
% 59.47/59.59 inference(scs_inference,[],[4603,4611,4727,4717,4813,4633,4721,4776,4617,4522,4723,4725,4763,4749,261,168,161,263,262,173,172,158,264,258,230,229,231,156,257,171,174,157,170])).
% 59.47/59.59 cnf(4860,plain,
% 59.47/59.59 (P4(x48601,x48601,x48602,x48601)),
% 59.47/59.59 inference(scs_inference,[],[4741,4603,4611,4727,4717,4813,4633,4721,4776,4617,4522,4723,4725,4763,4749,261,168,161,263,262,173,172,158,264,258,230,229,231,156,257,171,174,157,170,175])).
% 59.47/59.59 cnf(4862,plain,
% 59.47/59.59 (P4(a16,a2,a2,a1)),
% 59.47/59.59 inference(scs_inference,[],[4741,4603,4611,4727,4717,4813,4633,4721,4776,4617,4522,4723,4725,4763,4749,261,168,161,263,262,173,172,158,264,258,230,229,231,156,257,171,174,157,170,175,176])).
% 59.47/59.59 cnf(4866,plain,
% 59.47/59.59 (P9(x48661,x48662,x48663,x48664,x48662,x48661,x48664,x48663)),
% 59.47/59.59 inference(scs_inference,[],[4739,4741,4615,4603,4611,4727,4717,4813,4633,4721,4776,4617,4522,4723,4725,4763,4749,261,168,161,263,262,173,172,158,264,258,230,229,231,156,257,171,174,157,170,175,176,260,259])).
% 59.47/59.59 cnf(4868,plain,
% 59.47/59.59 (P10(f32(x48681,a15,a15,a15,a15),a15,x48681,a15)),
% 59.47/59.59 inference(scs_inference,[],[4790,4739,4741,4615,4603,4611,4727,4717,4813,4633,4721,4776,4617,4522,4723,4725,4763,4749,261,168,161,263,262,173,172,158,264,258,230,229,231,156,257,171,174,157,170,175,176,260,259,206])).
% 59.47/59.59 cnf(4869,plain,
% 59.47/59.59 (P5(x48691,x48691,x48691,x48691)),
% 59.47/59.59 inference(rename_variables,[],[4790])).
% 59.47/59.59 cnf(4872,plain,
% 59.47/59.59 (P9(x48721,x48722,x48721,x48722,x48723,x48724,x48723,x48724)),
% 59.47/59.59 inference(rename_variables,[],[4635])).
% 59.47/59.59 cnf(4875,plain,
% 59.47/59.59 (P9(x48751,x48752,x48752,x48751,x48753,x48754,x48753,x48754)),
% 59.47/59.59 inference(rename_variables,[],[4757])).
% 59.47/59.59 cnf(4883,plain,
% 59.47/59.59 (P5(x48831,x48831,x48831,x48831)),
% 59.47/59.59 inference(rename_variables,[],[4790])).
% 59.47/59.59 cnf(4885,plain,
% 59.47/59.59 (P1(f12(x48851,a15,a15,a15,x48852),a15,x48852)),
% 59.47/59.59 inference(scs_inference,[],[4790,4869,4739,4741,4757,4743,4615,4603,4611,4727,4717,4813,4633,4721,4776,4617,4522,4729,4723,4725,4763,4749,4635,261,168,161,263,262,173,172,158,264,258,230,229,231,156,257,171,174,157,170,175,176,260,259,206,252,255,182,245,205,202])).
% 59.47/59.59 cnf(4886,plain,
% 59.47/59.59 (P1(x48861,x48861,x48862)),
% 59.47/59.59 inference(rename_variables,[],[4743])).
% 59.47/59.59 cnf(4889,plain,
% 59.47/59.59 (P3(x48891,a15,a15,a15)),
% 59.47/59.59 inference(rename_variables,[],[4813])).
% 59.47/59.59 cnf(4894,plain,
% 59.47/59.59 (P3(x48941,a15,a15,a15)),
% 59.47/59.59 inference(rename_variables,[],[4813])).
% 59.47/59.59 cnf(4896,plain,
% 59.47/59.59 (P5(x48961,a15,x48961,a15)),
% 59.47/59.59 inference(scs_inference,[],[4790,4869,4739,4741,4757,4743,4615,4603,4611,4727,4717,4813,4889,4894,4633,4721,4776,4617,4522,4729,4723,4725,4763,4749,4635,4505,4514,261,168,161,263,262,173,172,158,264,258,230,229,231,156,257,171,174,157,170,175,176,260,259,206,252,255,182,245,205,202,199,204,194,178])).
% 59.47/59.59 cnf(4902,plain,
% 59.47/59.59 (P3(x49021,a15,a15,a15)),
% 59.47/59.59 inference(rename_variables,[],[4813])).
% 59.47/59.59 cnf(4904,plain,
% 59.47/59.59 (P8(a15,f3(a15,a15,a15),f3(a15,a15,a15),a15,a15,f3(a15,a15,a15),f3(a15,a15,a15),a15)),
% 59.47/59.59 inference(scs_inference,[],[4790,4869,4739,4741,4757,4743,4615,4603,4611,4727,4717,4813,4889,4894,4633,4721,4776,4617,4522,4690,4729,4723,4725,4763,4749,4635,4674,4505,4514,261,168,161,263,262,173,172,158,264,258,230,229,231,156,257,171,174,157,170,175,176,260,259,206,252,255,182,245,205,202,199,204,194,178,196,195,228])).
% 59.47/59.59 cnf(4906,plain,
% 59.47/59.59 (P3(f12(x49061,a15,a15,a15,x49062),x49061,a15,x49062)),
% 59.47/59.59 inference(scs_inference,[],[4790,4869,4739,4741,4757,4743,4886,4615,4603,4611,4727,4717,4813,4889,4894,4902,4633,4721,4776,4617,4522,4690,4729,4723,4725,4763,4749,4635,4674,4505,4514,261,168,161,263,262,173,172,158,264,258,230,229,231,156,257,171,174,157,170,175,176,260,259,206,252,255,182,245,205,202,199,204,194,178,196,195,228,203])).
% 59.47/59.59 cnf(4907,plain,
% 59.47/59.59 (P1(x49071,x49071,x49072)),
% 59.47/59.59 inference(rename_variables,[],[4743])).
% 59.47/59.59 cnf(4909,plain,
% 59.47/59.59 (P3(x49091,x49092,x49092,x49091)),
% 59.47/59.59 inference(scs_inference,[],[4790,4869,4739,4741,4757,4875,4743,4886,4615,4603,4611,4727,4717,4813,4889,4894,4902,4633,4721,4776,4617,4522,4690,4729,4723,4725,4763,4749,4635,4674,4505,4514,261,168,161,263,262,173,172,158,264,258,230,229,231,156,257,171,174,157,170,175,176,260,259,206,252,255,182,245,205,202,199,204,194,178,196,195,228,203,246])).
% 59.47/59.59 cnf(4913,plain,
% 59.47/59.59 (P2(x49131,x49131,x49131,x49131)),
% 59.47/59.59 inference(scs_inference,[],[4790,4869,4883,4739,4741,4757,4875,4743,4886,4615,4603,4611,4727,4717,4813,4889,4894,4902,4633,4721,4776,4617,4522,4690,4729,4723,4725,4763,4749,4635,4674,4505,4514,261,168,161,263,262,173,172,158,264,258,230,229,231,156,257,171,174,157,170,175,176,260,259,206,252,255,182,245,205,202,199,204,194,178,196,195,228,203,246,189])).
% 59.47/59.59 cnf(4915,plain,
% 59.47/59.59 (P3(a15,a15,a17,a17)),
% 59.47/59.59 inference(scs_inference,[],[4790,4869,4883,4739,4741,4757,4875,4743,4886,4615,4603,4611,4727,4717,4813,4889,4894,4902,4633,4721,4776,4617,4522,4690,4729,4723,4725,4763,4749,4635,4674,4505,4514,261,168,161,263,262,173,172,158,264,258,230,229,231,156,257,171,174,157,170,175,176,260,259,206,252,255,182,245,205,202,199,204,194,178,196,195,228,203,246,189,186])).
% 59.47/59.59 cnf(4921,plain,
% 59.47/59.59 (P7(f27(a17,x49211),x49211,a17)),
% 59.47/59.59 inference(rename_variables,[],[4725])).
% 59.47/59.59 cnf(4923,plain,
% 59.47/59.59 (P7(f3(a15,a15,a15),f3(a15,a15,a15),a15)),
% 59.47/59.59 inference(scs_inference,[],[4790,4869,4883,4739,4741,4757,4875,4743,4886,4907,4292,4615,4603,4611,4727,4717,4813,4889,4894,4902,4633,4721,4776,4617,4522,4690,4729,4723,4725,4763,4749,4605,4635,4872,4674,4505,4514,152,261,168,161,263,262,173,172,158,264,258,230,229,231,156,257,171,174,157,170,175,176,260,259,206,252,255,182,245,205,202,199,204,194,178,196,195,228,203,246,189,186,241,232,167])).
% 59.47/59.59 cnf(4924,plain,
% 59.47/59.59 (P1(x49241,x49241,x49242)),
% 59.47/59.59 inference(rename_variables,[],[4743])).
% 59.47/59.59 cnf(4928,plain,
% 59.47/59.59 (P10(x49281,x49282,x49282,x49281)),
% 59.47/59.59 inference(rename_variables,[],[4456])).
% 59.47/59.59 cnf(4930,plain,
% 59.47/59.59 (P7(x49301,x49301,x49301)),
% 59.47/59.59 inference(scs_inference,[],[4790,4869,4883,4739,4741,4757,4875,4743,4886,4907,4924,4292,4615,4603,4611,4727,4717,4813,4889,4894,4902,4633,4721,4776,4617,4522,4690,4729,4723,4725,4921,4763,4749,4605,4635,4872,4456,4674,4505,4514,152,261,168,161,263,262,173,172,158,264,258,230,229,231,156,257,171,174,157,170,175,176,260,259,206,252,255,182,245,205,202,199,204,194,178,196,195,228,203,246,189,186,241,232,167,197,244])).
% 59.47/59.59 cnf(4932,plain,
% 59.47/59.59 (P1(x49321,x49321,x49322)),
% 59.47/59.59 inference(rename_variables,[],[4743])).
% 59.47/59.59 cnf(4934,plain,
% 59.47/59.59 (P1(a15,a1,f13(a2,a15,a15,a2,a15,a1))),
% 59.47/59.59 inference(scs_inference,[],[142,4790,4869,4883,4739,4741,4757,4875,4743,4886,4907,4924,4932,4292,4615,4603,4611,4727,4717,4813,4889,4894,4902,4633,4721,4776,4617,4522,4690,4729,4723,4725,4921,4763,4749,4605,4635,4872,4619,4456,4928,4674,4505,4514,152,261,168,161,263,262,173,172,158,264,258,230,229,231,156,257,171,174,157,170,175,176,260,259,206,252,255,182,245,205,202,199,204,194,178,196,195,228,203,246,189,186,241,232,167,197,244,211])).
% 59.47/59.59 cnf(4937,plain,
% 59.47/59.59 (P10(x49371,x49372,x49372,x49371)),
% 59.47/59.59 inference(rename_variables,[],[4456])).
% 59.47/59.59 cnf(4939,plain,
% 59.47/59.59 (P10(a19,a1,a2,a15)),
% 59.47/59.59 inference(scs_inference,[],[142,4790,4869,4883,4739,4741,4757,4875,4743,4886,4907,4924,4932,4292,4615,4603,4611,4727,4717,4813,4889,4894,4902,4633,4721,4776,4617,4522,4690,4729,4723,4725,4921,4763,4749,4605,4635,4872,4619,4456,4928,4674,4505,4514,152,261,168,161,263,262,173,172,158,264,258,230,229,231,156,257,171,174,157,170,175,176,260,259,206,252,255,182,245,205,202,199,204,194,178,196,195,228,203,246,189,186,241,232,167,197,244,211,277])).
% 59.47/59.59 cnf(4941,plain,
% 59.47/59.59 (P7(a17,a15,a15)),
% 59.47/59.59 inference(scs_inference,[],[142,4790,4869,4883,4739,4741,4757,4875,4743,4886,4907,4924,4932,4292,4615,4603,4611,4727,4717,4813,4889,4894,4902,4633,4721,4776,4617,4522,4690,4729,4723,4725,4921,4763,4749,4605,4635,4872,4619,4456,4928,4674,4505,4514,152,261,168,161,263,262,173,172,158,264,258,230,229,231,156,257,171,174,157,170,175,176,260,259,206,252,255,182,245,205,202,199,204,194,178,196,195,228,203,246,189,186,241,232,167,197,244,211,277,949])).
% 59.47/59.59 cnf(4945,plain,
% 59.47/59.59 (P7(f3(a15,a15,a15),a15,f3(a15,a15,a15))),
% 59.47/59.59 inference(scs_inference,[],[142,4790,4869,4883,4739,4741,4757,4875,4743,4886,4907,4924,4932,4292,4615,4603,4611,4727,4717,4813,4889,4894,4902,4633,4721,4776,4617,4522,4690,4729,4723,4725,4921,4763,4749,4605,4635,4872,4619,4456,4928,4674,4505,4514,152,261,168,161,263,262,173,172,158,264,258,230,229,231,156,257,171,174,157,170,175,176,260,259,206,252,255,182,245,205,202,199,204,194,178,196,195,228,203,246,189,186,241,232,167,197,244,211,277,949,169,159])).
% 59.47/59.59 cnf(4957,plain,
% 59.47/59.59 (P7(f30(a17,a17,a17,a17,a17,a17),a17,a17)),
% 59.47/59.60 inference(scs_inference,[],[142,4790,4869,4883,4739,4741,4757,4875,4743,4886,4907,4924,4932,4292,4615,4603,4611,4727,4717,4813,4889,4894,4902,4633,4721,4776,4617,4522,4690,4729,4723,4725,4921,4763,4749,4605,4635,4872,4619,4470,4456,4928,4674,4505,4514,152,261,168,161,263,262,173,172,158,264,258,230,229,231,156,257,171,174,157,170,175,176,260,259,206,252,255,182,245,205,202,199,204,194,178,196,195,228,203,246,189,186,241,232,167,197,244,211,277,949,169,159,192,265,183,209,210,208])).
% 59.47/59.60 cnf(4959,plain,
% 59.47/59.60 (P5(a17,a17,a15,a15)),
% 59.47/59.60 inference(scs_inference,[],[142,4790,4869,4883,4739,4741,4757,4875,4770,4743,4886,4907,4924,4932,4292,4615,4603,4611,4727,4717,4813,4889,4894,4902,4633,4721,4755,4776,4617,4522,4690,4729,4723,4725,4921,4763,4749,4605,4635,4872,4619,4470,4456,4928,4674,4505,4514,152,261,168,161,263,262,173,172,158,264,258,230,229,231,156,257,171,174,157,170,175,176,260,259,206,252,255,182,245,205,202,199,204,194,178,196,195,228,203,246,189,186,241,232,167,197,244,211,277,949,169,159,192,265,183,209,210,208,256])).
% 59.47/59.60 cnf(4965,plain,
% 59.47/59.60 (~P3(a15,a15,a15,a17)+P1(f14(a17,a15,a15,a17),a17,a15)),
% 59.47/59.60 inference(scs_inference,[],[142,4790,4869,4883,4739,4741,4757,4875,4770,4743,4886,4907,4924,4932,4292,4615,4603,4611,4727,4717,4813,4889,4894,4902,4633,4721,4755,4776,4617,4522,4690,4729,4723,4725,4921,4763,4749,4605,4635,4872,4619,4470,4456,4928,4937,4674,647,4505,4514,152,261,168,161,263,262,173,172,158,264,258,230,229,231,156,257,171,174,157,170,175,176,260,259,206,252,255,182,245,205,202,199,204,194,178,196,195,228,203,246,189,186,241,232,167,197,244,211,277,949,169,159,192,265,183,209,210,208,256,212,253])).
% 59.47/59.60 cnf(4968,plain,
% 59.47/59.60 (P10(a19,a21,a16,a17)),
% 59.47/59.60 inference(scs_inference,[],[4909,319])).
% 59.47/59.60 cnf(4969,plain,
% 59.47/59.60 (P3(x49691,x49692,x49692,x49691)),
% 59.47/59.60 inference(rename_variables,[],[4909])).
% 59.47/59.60 cnf(4971,plain,
% 59.47/59.60 (P10(a19,a22,a17,a15)),
% 59.47/59.60 inference(scs_inference,[],[4909,4969,319,356])).
% 59.47/59.60 cnf(4972,plain,
% 59.47/59.60 (P3(x49721,x49722,x49722,x49721)),
% 59.47/59.60 inference(rename_variables,[],[4909])).
% 59.47/59.60 cnf(4975,plain,
% 59.47/59.60 (P3(x49751,x49752,x49752,x49751)),
% 59.47/59.60 inference(rename_variables,[],[4909])).
% 59.47/59.60 cnf(4978,plain,
% 59.47/59.60 (P3(x49781,x49782,x49782,x49781)),
% 59.47/59.60 inference(rename_variables,[],[4909])).
% 59.47/59.60 cnf(4981,plain,
% 59.47/59.60 (P3(x49811,x49812,x49812,x49811)),
% 59.47/59.60 inference(rename_variables,[],[4909])).
% 59.47/59.60 cnf(4985,plain,
% 59.47/59.60 (P8(a17,a15,a17,a15,a15,a17,a15,a17)),
% 59.47/59.60 inference(scs_inference,[],[4909,4969,4972,4975,4978,4828,4957,319,356,1180,373,1782,949,261])).
% 59.47/59.60 cnf(4991,plain,
% 59.47/59.60 (P8(a15,a17,a17,a15,a15,a17,a17,a15)),
% 59.47/59.60 inference(scs_inference,[],[4909,4969,4972,4975,4978,4828,4939,4904,4957,319,356,1180,373,1782,949,261,262,168,264])).
% 59.47/59.60 cnf(4993,plain,
% 59.47/59.60 (P5(f3(a15,a15,a15),f3(a15,a15,a15),f3(a15,a15,a15),a15)),
% 59.47/59.60 inference(scs_inference,[],[4909,4969,4972,4975,4978,4828,4939,4923,4904,4957,319,356,1180,373,1782,949,261,262,168,264,161])).
% 59.47/59.60 cnf(4995,plain,
% 59.47/59.60 (P8(a15,a17,a17,a15,a17,a15,a15,a17)),
% 59.47/59.60 inference(scs_inference,[],[4909,4969,4972,4975,4978,4822,4828,4939,4923,4904,4957,319,356,1180,373,1782,949,261,262,168,264,161,263])).
% 59.47/59.60 cnf(4997,plain,
% 59.47/59.60 (P5(x49971,a15,a15,x49971)),
% 59.47/59.60 inference(scs_inference,[],[4909,4969,4972,4975,4978,4896,4822,4828,4939,4923,4904,4957,319,356,1180,373,1782,949,261,262,168,264,161,263,173])).
% 59.47/59.60 cnf(4999,plain,
% 59.47/59.60 (P9(a19,a1,x49991,x49992,a2,a15,x49991,x49992)),
% 59.47/59.60 inference(scs_inference,[],[4909,4969,4972,4975,4978,4896,4822,4828,4939,4923,4904,4957,319,356,1180,373,1782,949,261,262,168,264,161,263,173,230])).
% 59.47/59.60 cnf(5003,plain,
% 59.47/59.60 (P9(x50031,a15,a15,a15,a15,a15,x50031,a15)),
% 59.47/59.60 inference(scs_inference,[],[4909,4969,4972,4975,4978,4896,4822,4828,4939,4959,4923,4904,4957,319,356,1180,373,1782,949,261,262,168,264,161,263,173,230,172,231])).
% 59.47/59.60 cnf(5005,plain,
% 59.47/59.60 (P10(a19,a1,a15,a2)),
% 59.47/59.60 inference(scs_inference,[],[4909,4969,4972,4975,4978,4896,4822,4828,4939,4959,4923,4904,4957,319,356,1180,373,1782,949,261,262,168,264,161,263,173,230,172,231,169])).
% 59.47/59.60 cnf(5007,plain,
% 59.47/59.60 (P9(a17,a17,a15,a17,a21,a17,a21,a15)),
% 59.47/59.60 inference(scs_inference,[],[4909,4969,4972,4975,4978,4637,4896,4822,4828,4939,4959,4923,4904,4957,319,356,1180,373,1782,949,261,262,168,264,161,263,173,230,172,231,169,258])).
% 59.47/59.60 cnf(5019,plain,
% 59.47/59.60 (P3(x50191,x50192,x50191,x50192)),
% 59.47/59.60 inference(scs_inference,[],[4913,4909,4969,4972,4975,4978,4981,4637,4896,4822,4828,4854,4939,4959,4698,4923,4904,4957,319,356,1180,373,1782,949,261,262,168,264,161,263,173,230,172,231,169,258,229,257,156,192,157,171])).
% 59.47/59.60 cnf(5021,plain,
% 59.47/59.60 (P4(a2,a16,a2,a1)),
% 59.47/59.60 inference(scs_inference,[],[4913,4909,4969,4972,4975,4978,4981,4637,4896,4822,4828,4854,4862,4939,4959,4698,4923,4904,4957,319,356,1180,373,1782,949,261,262,168,264,161,263,173,230,172,231,169,258,229,257,156,192,157,171,174])).
% 59.47/59.60 cnf(5023,plain,
% 59.47/59.60 (P3(a19,a22,a15,a17)),
% 59.47/59.60 inference(scs_inference,[],[4913,4909,4969,4972,4975,4978,4981,4637,4896,4745,4822,4828,4854,4862,4939,4959,4698,4923,4904,4957,319,356,1180,373,1782,949,261,262,168,264,161,263,173,230,172,231,169,258,229,257,156,192,157,171,174,170])).
% 59.47/59.60 cnf(5025,plain,
% 59.47/59.60 (P4(a15,a1,a15,a2)),
% 59.47/59.60 inference(scs_inference,[],[4913,4909,4969,4972,4975,4978,4981,4783,4637,4896,4745,4822,4828,4854,4862,4939,4959,4698,4923,4904,4957,319,356,1180,373,1782,949,261,262,168,264,161,263,173,230,172,231,169,258,229,257,156,192,157,171,174,170,175])).
% 59.47/59.60 cnf(5027,plain,
% 59.47/59.60 (P4(x50271,x50271,x50271,x50272)),
% 59.47/59.60 inference(scs_inference,[],[4913,4860,4909,4969,4972,4975,4978,4981,4783,4637,4896,4745,4822,4828,4854,4862,4939,4959,4698,4923,4904,4957,319,356,1180,373,1782,949,261,262,168,264,161,263,173,230,172,231,169,258,229,257,156,192,157,171,174,170,175,176])).
% 59.47/59.60 cnf(5029,plain,
% 59.47/59.60 (P9(x50291,x50292,x50292,x50291,x50293,x50294,x50294,x50293)),
% 59.47/59.60 inference(scs_inference,[],[4913,4860,4866,4909,4969,4972,4975,4978,4981,4783,4637,4896,4745,4822,4828,4854,4862,4939,4959,4698,4923,4904,4957,319,356,1180,373,1782,949,261,262,168,264,161,263,173,230,172,231,169,258,229,257,156,192,157,171,174,170,175,176,260])).
% 59.47/59.60 cnf(5037,plain,
% 59.47/59.60 (P5(x50371,a15,x50371,a15)),
% 59.47/59.60 inference(rename_variables,[],[4896])).
% 59.47/59.60 cnf(5040,plain,
% 59.47/59.60 (P3(x50401,x50402,x50402,x50401)),
% 59.47/59.60 inference(rename_variables,[],[4909])).
% 59.47/59.60 cnf(5045,plain,
% 59.47/59.60 (P3(x50451,x50452,x50452,x50451)),
% 59.47/59.60 inference(rename_variables,[],[4909])).
% 59.47/59.60 cnf(5047,plain,
% 59.47/59.60 (P10(a1,a19,a15,a2)),
% 59.47/59.60 inference(scs_inference,[],[4913,4860,4866,4909,4969,4972,4975,4978,4981,5040,4783,4637,4896,5037,4737,4745,4822,4828,4854,4862,4939,4941,4959,4698,4923,4885,4904,4957,319,356,1180,373,1782,949,261,262,168,264,161,263,173,230,172,231,169,258,229,257,156,192,157,171,174,170,175,176,260,259,162,166,181,163,193,245])).
% 59.47/59.60 cnf(5048,plain,
% 59.47/59.60 (P9(x50481,x50482,x50483,x50484,x50482,x50481,x50484,x50483)),
% 59.47/59.60 inference(rename_variables,[],[4866])).
% 59.47/59.60 cnf(5053,plain,
% 59.47/59.60 (P3(x50531,x50532,x50532,x50531)),
% 59.47/59.60 inference(rename_variables,[],[4909])).
% 59.47/59.60 cnf(5056,plain,
% 59.47/59.60 (P3(x50561,x50562,x50562,x50561)),
% 59.47/59.60 inference(rename_variables,[],[4909])).
% 59.47/59.60 cnf(5059,plain,
% 59.47/59.60 (P5(x50591,a15,x50591,a15)),
% 59.47/59.60 inference(rename_variables,[],[4896])).
% 59.47/59.60 cnf(5063,plain,
% 59.47/59.60 (P3(x50631,x50632,x50632,x50631)),
% 59.47/59.60 inference(rename_variables,[],[4909])).
% 59.47/59.60 cnf(5066,plain,
% 59.47/59.60 (P3(x50661,x50662,x50662,x50661)),
% 59.47/59.60 inference(rename_variables,[],[4909])).
% 59.47/59.60 cnf(5074,plain,
% 59.47/59.60 (P3(x50741,x50742,x50742,x50741)),
% 59.47/59.60 inference(rename_variables,[],[4909])).
% 59.47/59.60 cnf(5078,plain,
% 59.47/59.60 (P3(x50781,x50782,x50782,x50781)),
% 59.47/59.60 inference(rename_variables,[],[4909])).
% 59.47/59.60 cnf(5080,plain,
% 59.47/59.60 (P10(a15,a15,a15,x50801)),
% 59.47/59.60 inference(scs_inference,[],[142,4913,4930,4860,4866,4909,4969,4972,4975,4978,4981,5040,5045,5053,5056,5063,5066,5074,5078,4783,4637,4896,5037,5059,4858,4737,4745,4822,4828,4854,4862,4915,4939,4941,4959,4698,4923,4885,4904,4957,4813,319,356,1180,373,1782,949,261,262,168,264,161,263,173,230,172,231,169,258,229,257,156,192,157,171,174,170,175,176,260,259,162,166,181,163,193,245,183,206,204,205,194,202,209,199,182,195,185])).
% 59.47/59.60 cnf(5081,plain,
% 59.47/59.60 (P3(a15,a15,x50811,a15)),
% 59.47/59.60 inference(rename_variables,[],[4858])).
% 59.47/59.60 cnf(5082,plain,
% 59.47/59.60 (P3(x50821,x50822,x50822,x50821)),
% 59.47/59.60 inference(rename_variables,[],[4909])).
% 59.47/59.60 cnf(5089,plain,
% 59.47/59.60 (P2(f8(x50891,x50891,x50892),x50891,x50891,x50892)),
% 59.47/59.60 inference(scs_inference,[],[142,4913,4930,4860,4866,4909,4969,4972,4975,4978,4981,5040,5045,5053,5056,5063,5066,5074,5078,5082,4783,4637,4896,5037,5059,4858,4737,4745,4822,4828,4854,4862,4915,4939,4941,4959,4698,4753,4923,4945,4885,4904,4957,4757,4813,319,356,1180,373,1782,949,261,262,168,264,161,263,173,230,172,231,169,258,229,257,156,192,157,171,174,170,175,176,260,259,162,166,181,163,193,245,183,206,204,205,194,202,209,199,182,195,185,178,254,196])).
% 59.47/59.60 cnf(5090,plain,
% 59.47/59.60 (P3(x50901,x50902,x50902,x50901)),
% 59.47/59.60 inference(rename_variables,[],[4909])).
% 59.47/59.60 cnf(5100,plain,
% 59.47/59.60 (P3(x51001,x51002,x51002,x51001)),
% 59.47/59.60 inference(rename_variables,[],[4909])).
% 59.47/59.60 cnf(5102,plain,
% 59.47/59.60 (P3(a15,a15,a15,x51021)),
% 59.47/59.60 inference(scs_inference,[],[142,4913,4930,4860,4866,5048,4909,4969,4972,4975,4978,4981,5040,5045,5053,5056,5063,5066,5074,5078,5082,5090,4783,4637,4377,4896,5037,5059,4858,5081,4737,4745,4822,4828,4854,4862,4915,4939,4941,4959,4719,4698,4753,4923,4945,4885,4904,4868,4957,4757,4813,319,356,1180,373,1782,949,261,262,168,264,161,263,173,230,172,231,169,258,229,257,156,192,157,171,174,170,175,176,260,259,162,166,181,163,193,245,183,206,204,205,194,202,209,199,182,195,185,178,254,196,184,228,160,203,246])).
% 59.47/59.60 cnf(5106,plain,
% 59.47/59.60 (P2(x51061,a15,a15,a15)),
% 59.47/59.60 inference(scs_inference,[],[142,4913,4930,4860,4866,5048,4909,4969,4972,4975,4978,4981,5040,5045,5053,5056,5063,5066,5074,5078,5082,5090,4783,4637,4377,4896,5037,5059,4858,5081,4737,4745,4822,4828,4854,4862,4915,4939,4941,4959,4719,4698,4753,4923,4945,4885,4904,4868,4957,4757,4813,319,356,1180,373,1782,949,261,262,168,264,161,263,173,230,172,231,169,258,229,257,156,192,157,171,174,170,175,176,260,259,162,166,181,163,193,245,183,206,204,205,194,202,209,199,182,195,185,178,254,196,184,228,160,203,246,189])).
% 59.47/59.60 cnf(5110,plain,
% 59.47/59.60 (P7(f30(x51101,x51101,x51101,x51101,x51101,x51101),x51101,x51101)),
% 59.47/59.60 inference(scs_inference,[],[142,4913,4930,4860,4866,5048,4909,4969,4972,4975,4978,4981,5040,5045,5053,5056,5063,5066,5074,5078,5082,5090,4783,4637,4377,4896,5037,5059,4858,5081,4737,4745,4822,4828,4854,4862,4915,4939,4941,4959,4719,4698,4753,4923,4945,4885,4904,4868,4957,4757,4813,319,356,1180,373,1782,949,261,262,168,264,161,263,173,230,172,231,169,258,229,257,156,192,157,171,174,170,175,176,260,259,162,166,181,163,193,245,183,206,204,205,194,202,209,199,182,195,185,178,254,196,184,228,160,203,246,189,186,208])).
% 59.47/59.60 cnf(5112,plain,
% 59.47/59.60 (P4(x51121,x51122,x51123,x51123)),
% 59.47/59.60 inference(scs_inference,[],[142,4913,4930,4860,4866,5048,4909,4969,4972,4975,4978,4981,5040,5045,5053,5056,5063,5066,5074,5078,5082,5090,4783,4637,4377,4896,5037,5059,4858,5081,4737,4745,4822,4828,4854,4862,4915,4939,4941,4959,4719,4698,4753,4923,4945,4885,4904,4868,4957,4757,4743,4446,4813,319,356,1180,373,1782,949,261,262,168,264,161,263,173,230,172,231,169,258,229,257,156,192,157,171,174,170,175,176,260,259,162,166,181,163,193,245,183,206,204,205,194,202,209,199,182,195,185,178,254,196,184,228,160,203,246,189,186,208,241])).
% 59.47/59.60 cnf(5118,plain,
% 59.47/59.60 (P7(f6(x51181,x51181,x51181),x51181,x51181)),
% 59.47/59.60 inference(scs_inference,[],[142,4913,4930,4860,4866,5048,4909,4969,4972,4975,4978,4981,5040,5045,5053,5056,5063,5066,5074,5078,5082,5090,5100,4783,4637,4377,4896,5037,5059,4858,5081,4737,4745,4822,4828,4854,4862,4915,4939,4941,4959,4719,4698,4753,4923,4945,4885,4904,4868,4957,4757,4743,4518,4446,4813,153,319,356,1180,373,1782,949,261,262,168,264,161,263,173,230,172,231,169,258,229,257,156,192,157,171,174,170,175,176,260,259,162,166,181,163,193,245,183,206,204,205,194,202,209,199,182,195,185,178,254,196,184,228,160,203,246,189,186,208,241,232,191])).
% 59.47/59.60 cnf(5122,plain,
% 59.47/59.60 (P3(a15,x51221,x51221,x51221)),
% 59.47/59.60 inference(scs_inference,[],[142,4913,4930,4860,4866,5048,4909,4969,4972,4975,4978,4981,5040,5045,5053,5056,5063,5066,5074,5078,5082,5090,5100,4783,4637,4377,4896,5037,5059,4858,5081,4737,4745,4822,4828,4854,4862,4915,4939,4941,4959,4719,4698,4753,4923,4945,4885,4904,4868,4957,4790,4757,4743,4518,4446,4813,153,319,356,1180,373,1782,949,261,262,168,264,161,263,173,230,172,231,169,258,229,257,156,192,157,171,174,170,175,176,260,259,162,166,181,163,193,245,183,206,204,205,194,202,209,199,182,195,185,178,254,196,184,228,160,203,246,189,186,208,241,232,191,200])).
% 59.47/59.60 cnf(5127,plain,
% 59.47/59.60 (P7(f27(x51271,x51272),x51271,x51272)),
% 59.47/59.60 inference(scs_inference,[],[142,4913,4930,4860,4866,5048,4909,4969,4972,4975,4978,4981,5040,5045,5053,5056,5063,5066,5074,5078,5082,5090,5100,4783,4637,4377,4896,5037,5059,4858,5081,4737,4745,4822,4828,4854,4862,4915,4939,4941,4959,4719,4698,4753,4923,4945,4885,4904,4868,4957,4790,4757,4743,4518,4446,4813,153,319,356,1180,373,1782,949,261,262,168,264,161,263,173,230,172,231,169,258,229,257,156,192,157,171,174,170,175,176,260,259,162,166,181,163,193,245,183,206,204,205,194,202,209,199,182,195,185,178,254,196,184,228,160,203,246,189,186,208,241,232,191,200,164])).
% 59.47/59.60 cnf(5130,plain,
% 59.47/59.60 (P1(x51301,x51301,x51302)),
% 59.47/59.60 inference(rename_variables,[],[4743])).
% 59.47/59.60 cnf(5136,plain,
% 59.47/59.60 (P1(f14(a17,a15,a15,a17),a17,a15)),
% 59.47/59.60 inference(scs_inference,[],[142,4913,4930,4860,4866,5048,4909,4969,4972,4975,4978,4981,5040,5045,5053,5056,5063,5066,5074,5078,5082,5090,5100,4783,4637,4377,4896,5037,5059,4858,5081,4737,4745,4822,4828,4854,4862,4915,4939,4941,4959,4719,4698,4753,4923,4945,4885,4904,4868,4957,4790,4757,4743,5130,4518,4446,4619,4813,153,319,356,1180,373,1782,949,261,262,168,264,161,263,173,230,172,231,169,258,229,257,156,192,157,171,174,170,175,176,260,259,162,166,181,163,193,245,183,206,204,205,194,202,209,199,182,195,185,178,254,196,184,228,160,203,246,189,186,208,241,232,191,200,164,212,4965])).
% 59.47/59.60 cnf(5137,plain,
% 59.47/59.60 (P1(f27(x51371,x51372),x51371,x51372)),
% 59.47/59.60 inference(scs_inference,[],[142,4913,4930,4860,4866,5048,4909,4969,4972,4975,4978,4981,5040,5045,5053,5056,5063,5066,5074,5078,5082,5090,5100,4783,4637,4377,4896,5037,5059,4858,5081,4737,4745,4822,4828,4854,4862,4915,4939,4941,4959,4719,4698,4753,4923,4945,4885,4904,4868,4957,4790,4757,4743,5130,4518,4446,4619,4813,153,319,356,1180,373,1782,949,261,262,168,264,161,263,173,230,172,231,169,258,229,257,156,192,157,171,174,170,175,176,260,259,162,166,181,163,193,245,183,206,204,205,194,202,209,199,182,195,185,178,254,196,184,228,160,203,246,189,186,208,241,232,191,200,164,212,4965,158])).
% 59.47/59.60 cnf(5139,plain,
% 59.47/59.60 (P7(f27(x51391,x51392),x51392,x51391)),
% 59.47/59.60 inference(scs_inference,[],[142,4913,4930,4860,4866,5048,4909,4969,4972,4975,4978,4981,5040,5045,5053,5056,5063,5066,5074,5078,5082,5090,5100,4783,4637,4377,4896,5037,5059,4858,5081,4737,4745,4822,4828,4854,4862,4915,4939,4941,4959,4719,4698,4753,4923,4945,4885,4904,4868,4957,4790,4757,4743,5130,4518,4446,4619,4813,153,319,356,1180,373,1782,949,261,262,168,264,161,263,173,230,172,231,169,258,229,257,156,192,157,171,174,170,175,176,260,259,162,166,181,163,193,245,183,206,204,205,194,202,209,199,182,195,185,178,254,196,184,228,160,203,246,189,186,208,241,232,191,200,164,212,4965,158,159])).
% 59.47/59.60 cnf(5141,plain,
% 59.47/59.60 (~P4(x51411,a19,a21,a20)+~P4(x51411,a19,a21,a24)),
% 59.47/59.60 inference(scs_inference,[],[142,4913,4930,4860,4866,5048,4909,4969,4972,4975,4978,4981,5040,5045,5053,5056,5063,5066,5074,5078,5082,5090,5100,4783,4637,4377,4896,5037,5059,4858,5081,4737,4745,4822,4828,4854,4862,4915,4939,4941,4959,4719,4698,4753,4923,4945,4885,4904,4868,4957,4790,4757,4743,5130,4518,384,4446,4619,4813,153,319,356,1180,373,1782,949,261,262,168,264,161,263,173,230,172,231,169,258,229,257,156,192,157,171,174,170,175,176,260,259,162,166,181,163,193,245,183,206,204,205,194,202,209,199,182,195,185,178,254,196,184,228,160,203,246,189,186,208,241,232,191,200,164,212,4965,158,159,190])).
% 59.47/59.60 cnf(5160,plain,
% 59.47/59.60 (P9(a15,f3(a15,a15,a15),a15,f3(a15,a15,a15),a15,f3(a15,a15,a15),a15,a15)),
% 59.47/59.60 inference(scs_inference,[],[5027,4705])).
% 59.47/59.60 cnf(5163,plain,
% 59.47/59.60 (P4(x51631,x51632,x51633,x51633)),
% 59.47/59.60 inference(rename_variables,[],[5112])).
% 59.47/59.60 cnf(5164,plain,
% 59.47/59.60 (P10(a1,a19,a2,a15)),
% 59.47/59.60 inference(scs_inference,[],[5019,5112,4816,277])).
% 59.47/59.60 cnf(5165,plain,
% 59.47/59.60 (P3(x51651,x51652,x51651,x51652)),
% 59.47/59.60 inference(rename_variables,[],[5019])).
% 59.47/59.60 cnf(5168,plain,
% 59.47/59.60 (P3(x51681,x51682,x51681,x51682)),
% 59.47/59.60 inference(rename_variables,[],[5019])).
% 59.47/59.60 cnf(5171,plain,
% 59.47/59.60 (P3(x51711,x51712,x51711,x51712)),
% 59.47/59.60 inference(rename_variables,[],[5019])).
% 59.47/59.60 cnf(5174,plain,
% 59.47/59.60 (P3(x51741,x51742,x51741,x51742)),
% 59.47/59.60 inference(rename_variables,[],[5019])).
% 59.47/59.60 cnf(5176,plain,
% 59.47/59.60 (P7(f6(a17,a17,a17),a15,a15)),
% 59.47/59.60 inference(scs_inference,[],[5019,5165,5168,5171,5112,5118,4816,277,319,373,356,949])).
% 59.47/59.60 cnf(5181,plain,
% 59.47/59.60 (P8(a17,a15,a15,a17,a15,a17,a17,a15)),
% 59.47/59.60 inference(scs_inference,[],[5019,5165,5168,5171,5112,5005,4995,5118,4816,277,319,373,356,949,168,261])).
% 59.47/59.60 cnf(5183,plain,
% 59.47/59.60 (P5(f30(x51831,x51831,x51831,x51831,x51831,x51831),x51831,f30(x51831,x51831,x51831,x51831,x51831,x51831),x51831)),
% 59.47/59.60 inference(scs_inference,[],[5019,5165,5168,5171,5112,5005,4995,5110,5118,4816,277,319,373,356,949,168,261,161])).
% 59.47/59.60 cnf(5185,plain,
% 59.47/59.60 (P5(a15,x51851,x51851,a15)),
% 59.47/59.60 inference(scs_inference,[],[5019,5165,5168,5171,5112,5005,4997,4995,5110,5118,4816,277,319,373,356,949,168,261,161,172])).
% 59.47/59.60 cnf(5191,plain,
% 59.47/59.60 (P9(a19,a1,x51911,x51912,a15,a2,x51911,x51912)),
% 59.47/59.60 inference(scs_inference,[],[5019,5165,5168,5171,5112,5005,4997,4991,4995,5110,5118,4993,4816,277,319,373,356,949,168,261,161,172,173,262,230])).
% 59.47/59.60 cnf(5193,plain,
% 59.47/59.60 (P8(a15,a15,a15,a15,a15,a17,a15,a17)),
% 59.47/59.60 inference(scs_inference,[],[5019,5165,5168,5171,5112,5005,4997,4830,4991,4995,5110,5118,4993,4816,277,319,373,356,949,168,261,161,172,173,262,230,264])).
% 59.47/59.60 cnf(5195,plain,
% 59.47/59.60 (P8(a15,a17,a17,a15,a15,a17,a15,a17)),
% 59.47/59.60 inference(scs_inference,[],[5019,5165,5168,5171,5112,5005,4997,4830,4985,4991,4995,5110,5118,4993,4816,277,319,373,356,949,168,261,161,172,173,262,230,264,263])).
% 59.47/59.60 cnf(5199,plain,
% 59.47/59.60 (P9(x51991,x51992,a19,a1,x51991,x51992,a2,a15)),
% 59.47/59.60 inference(scs_inference,[],[5019,5165,5168,5171,5112,5005,4997,4999,4830,4985,4991,4995,5110,5118,4993,4816,277,319,373,356,949,168,261,161,172,173,262,230,264,263,257,258])).
% 59.47/59.60 cnf(5209,plain,
% 59.47/59.60 (P10(a15,a15,x52091,a15)),
% 59.47/59.60 inference(scs_inference,[],[5019,5165,5168,5171,5112,5005,4997,4999,5080,4830,4985,4991,4995,5021,5110,5118,5137,5139,4768,4993,4816,277,319,373,356,949,168,261,161,172,173,262,230,264,263,257,258,156,158,229,231,169])).
% 59.47/59.60 cnf(5213,plain,
% 59.47/59.60 (P3(a19,a22,a17,a15)),
% 59.47/59.60 inference(scs_inference,[],[5019,5165,5168,5171,5112,5005,4997,4999,5080,5106,4830,4985,4991,4995,5021,5023,5110,5118,5137,5139,4768,4993,4816,277,319,373,356,949,168,261,161,172,173,262,230,264,263,257,258,156,158,229,231,169,192,171])).
% 59.47/59.60 cnf(5219,plain,
% 59.47/59.60 (P3(x52191,x52191,a15,x52191)),
% 59.47/59.60 inference(scs_inference,[],[5019,5165,5168,5171,5112,5005,5122,4997,4999,5080,5106,4830,4985,4991,4995,5021,5023,5025,5110,5118,5137,5139,4768,4993,4934,4816,277,319,373,356,949,168,261,161,172,173,262,230,264,263,257,258,156,158,229,231,169,192,171,157,174,170])).
% 59.47/59.60 cnf(5223,plain,
% 59.47/59.60 (P4(x52231,x52232,x52233,x52232)),
% 59.47/59.60 inference(scs_inference,[],[5019,5165,5168,5171,5112,5163,5005,5122,4997,4999,5080,5106,4830,4985,4991,4995,5021,5023,5025,5110,5118,5137,5139,4768,4993,4934,4816,277,319,373,356,949,168,261,161,172,173,262,230,264,263,257,258,156,158,229,231,169,192,171,157,174,170,176,175])).
% 59.47/59.60 cnf(5232,plain,
% 59.47/59.60 (~E(a19,a24)),
% 59.47/59.60 inference(scs_inference,[],[5019,5165,5168,5171,5112,5163,4850,5005,5122,4997,4999,5080,5106,4830,4985,4991,4995,5021,5023,5025,5110,5118,5137,5139,4768,4993,4934,4909,386,4717,4816,277,319,373,356,949,168,261,161,172,173,262,230,264,263,257,258,156,158,229,231,169,192,171,157,174,170,176,175,260,259,181,133])).
% 59.47/59.60 cnf(5233,plain,
% 59.47/59.60 (P1(f5(x52331,x52331,x52332),x52332,x52331)),
% 59.47/59.60 inference(scs_inference,[],[5019,5165,5168,5171,5174,5112,5163,4850,5005,5122,4997,4999,5080,5106,4830,4985,4991,4995,5021,5023,5025,5110,5118,5137,5139,4768,4993,4934,4909,386,4717,4816,277,319,373,356,949,168,261,161,172,173,262,230,264,263,257,258,156,158,229,231,169,192,171,157,174,170,176,175,260,259,181,133,183])).
% 59.47/59.60 cnf(5238,plain,
% 59.47/59.60 (P5(x52381,x52381,x52381,f32(x52381,x52381,x52381,x52381,x52381))),
% 59.47/59.60 inference(scs_inference,[],[5019,5165,5168,5171,5174,5112,5163,4850,5005,5122,4997,4999,5080,5106,4830,4985,4991,4995,5021,5023,5025,5110,5118,5137,5139,4768,4993,4934,4733,4909,386,4790,4717,4816,277,319,373,356,949,168,261,161,172,173,262,230,264,263,257,258,156,158,229,231,169,192,171,157,174,170,176,175,260,259,181,133,183,245,204])).
% 59.47/59.60 cnf(5239,plain,
% 59.47/59.60 (P5(x52391,x52391,x52391,x52391)),
% 59.47/59.60 inference(rename_variables,[],[4790])).
% 59.47/59.60 cnf(5240,plain,
% 59.47/59.60 (P3(x52401,x52402,x52401,x52402)),
% 59.47/59.60 inference(rename_variables,[],[5019])).
% 59.47/59.60 cnf(5242,plain,
% 59.47/59.60 (P3(a19,a1,a15,a2)),
% 59.47/59.60 inference(scs_inference,[],[5019,5165,5168,5171,5174,5240,5112,5163,4850,5005,5122,4997,4999,5080,5106,4830,4985,4991,4995,5021,5023,5025,5110,5118,5137,5139,4768,4993,4934,4733,4909,386,4790,4717,4816,277,319,373,356,949,168,261,161,172,173,262,230,264,263,257,258,156,158,229,231,169,192,171,157,174,170,176,175,260,259,181,133,183,245,204,187])).
% 59.47/59.60 cnf(5243,plain,
% 59.47/59.60 (P3(x52431,x52432,x52431,x52432)),
% 59.47/59.60 inference(rename_variables,[],[5019])).
% 59.47/59.60 cnf(5246,plain,
% 59.47/59.60 (P5(x52461,x52461,x52461,x52461)),
% 59.47/59.60 inference(rename_variables,[],[4790])).
% 59.47/59.60 cnf(5247,plain,
% 59.47/59.60 (P3(x52471,x52472,x52471,x52472)),
% 59.47/59.60 inference(rename_variables,[],[5019])).
% 59.47/59.60 cnf(5249,plain,
% 59.47/59.60 (P3(x52491,f4(x52491,x52491,x52492),x52492,x52491)),
% 59.47/59.60 inference(scs_inference,[],[5019,5165,5168,5171,5174,5240,5243,5247,5112,5163,4850,5005,5122,4997,4999,5080,5106,4830,4985,4991,4995,5021,5023,5025,5110,5118,5137,5139,4768,4993,4934,4733,4909,386,4790,5239,4717,4816,277,319,373,356,949,168,261,161,172,173,262,230,264,263,257,258,156,158,229,231,169,192,171,157,174,170,176,175,260,259,181,133,183,245,204,187,193,194])).
% 59.47/59.60 cnf(5251,plain,
% 59.47/59.60 (P10(f32(x52511,x52511,x52511,x52511,x52511),x52511,x52511,x52511)),
% 59.47/59.60 inference(scs_inference,[],[5019,5165,5168,5171,5174,5240,5243,5247,5112,5163,4850,5005,5122,4997,4999,5080,5106,4830,4985,4991,4995,5021,5023,5025,5110,5118,5137,5139,4768,4993,4934,4733,4909,386,4790,5239,5246,4717,4816,277,319,373,356,949,168,261,161,172,173,262,230,264,263,257,258,156,158,229,231,169,192,171,157,174,170,176,175,260,259,181,133,183,245,204,187,193,194,206])).
% 59.47/59.60 cnf(5252,plain,
% 59.47/59.60 (P5(x52521,x52521,x52521,x52521)),
% 59.47/59.60 inference(rename_variables,[],[4790])).
% 59.47/59.60 cnf(5253,plain,
% 59.47/59.60 (P3(x52531,x52532,x52531,x52532)),
% 59.47/59.60 inference(rename_variables,[],[5019])).
% 59.47/59.60 cnf(5256,plain,
% 59.47/59.60 (P3(x52561,x52562,x52561,x52562)),
% 59.47/59.60 inference(rename_variables,[],[5019])).
% 59.47/59.60 cnf(5263,plain,
% 59.47/59.60 (P3(x52631,f5(x52631,x52631,x52632),x52632,x52631)),
% 59.47/59.60 inference(scs_inference,[],[5019,5165,5168,5171,5174,5240,5243,5247,5253,5256,5112,5163,4850,5005,5122,4997,4999,5080,5106,4830,4985,4991,4995,5021,5023,5025,5110,5118,5137,5139,4768,4993,4934,4733,4909,386,4790,5239,5246,4377,4717,4816,277,319,373,356,949,168,261,161,172,173,262,230,264,263,257,258,156,158,229,231,169,192,171,157,174,170,176,175,260,259,181,133,183,245,204,187,193,194,206,202,199,182,195])).
% 59.47/59.60 cnf(5265,plain,
% 59.47/59.60 (P8(f30(x52651,x52651,x52651,x52651,x52651,x52651),x52651,x52651,x52651,f30(x52651,x52651,x52651,x52651,x52651,x52651),x52651,x52651,x52651)),
% 59.47/59.60 inference(scs_inference,[],[5019,5165,5168,5171,5174,5240,5243,5247,5253,5256,5112,5163,4850,5005,5122,4997,4999,5080,5106,4830,4985,4991,4995,5021,5023,5025,5110,5118,5137,5139,4768,4993,4934,4733,4909,386,4790,5239,5246,4377,4717,4816,277,319,373,356,949,168,261,161,172,173,262,230,264,263,257,258,156,158,229,231,169,192,171,157,174,170,176,175,260,259,181,133,183,245,204,187,193,194,206,202,199,182,195,228])).
% 59.47/59.60 cnf(5269,plain,
% 59.47/59.60 (P3(x52691,x52692,x52691,x52692)),
% 59.47/59.60 inference(rename_variables,[],[5019])).
% 59.47/59.60 cnf(5274,plain,
% 59.47/59.60 (P2(a15,f3(a15,a15,a15),f3(a15,a15,a15),f3(a15,a15,a15))),
% 59.47/59.60 inference(scs_inference,[],[5019,5165,5168,5171,5174,5240,5243,5247,5253,5256,5112,5163,4850,5005,5122,4997,4999,5080,5102,5106,4830,4985,4991,4995,5021,5023,5025,5110,5118,5137,5139,4768,4993,4934,4733,4909,386,4790,5239,5246,4377,4717,4816,277,319,373,356,949,168,261,161,172,173,262,230,264,263,257,258,156,158,229,231,169,192,171,157,174,170,176,175,260,259,181,133,183,245,204,187,193,194,206,202,199,182,195,228,246,196,189])).
% 59.47/59.60 cnf(5283,plain,
% 59.47/59.60 (P4(a15,a15,f14(a17,a15,a15,a17),a17)),
% 59.47/59.60 inference(scs_inference,[],[5019,5165,5168,5171,5174,5240,5243,5247,5253,5256,5269,5112,5163,4850,5005,5122,4997,4999,5080,5102,5106,4830,4985,4991,4995,5021,5023,5025,5110,5118,5137,5139,5136,4768,4993,4934,4733,4909,4941,386,4790,5239,5246,4377,4717,4635,4816,277,319,373,356,949,168,261,161,172,173,262,230,264,263,257,258,156,158,229,231,169,192,171,157,174,170,176,175,260,259,181,133,183,245,204,187,193,194,206,202,199,182,195,228,246,196,189,203,186,208,241])).
% 59.47/59.60 cnf(5286,plain,
% 59.47/59.60 (P9(a15,a15,a15,a15,x52861,a15,x52861,f30(a15,a15,a15,a15,a15,a15))),
% 59.47/59.60 inference(scs_inference,[],[5019,5165,5168,5171,5174,5240,5243,5247,5253,5256,5269,5112,5163,4850,5005,5122,4997,4999,5080,5102,5106,4830,4985,4991,4995,5021,5023,5025,5110,5118,5137,5139,5136,4768,4993,4934,4733,4909,4941,386,4790,5239,5246,4377,4717,4635,4816,277,319,373,356,949,168,261,161,172,173,262,230,264,263,257,258,156,158,229,231,169,192,171,157,174,170,176,175,260,259,181,133,183,245,204,187,193,194,206,202,199,182,195,228,246,196,189,203,186,208,241,232])).
% 59.47/59.60 cnf(5289,plain,
% 59.47/59.60 (P7(a15,f3(a15,a15,a15),f3(a15,a15,a15))),
% 59.47/59.60 inference(scs_inference,[],[5019,5165,5168,5171,5174,5240,5243,5247,5253,5256,5269,5112,5163,4850,5005,5122,4997,4999,5080,5102,5106,4830,4985,4991,4995,5021,5023,5025,5110,5118,5137,5139,5136,4768,4993,4934,4733,5160,4909,4941,386,4790,5239,5246,4377,4452,4503,4717,4635,4816,277,319,373,356,949,168,261,161,172,173,262,230,264,263,257,258,156,158,229,231,169,192,171,157,174,170,176,175,260,259,181,133,183,245,204,187,193,194,206,202,199,182,195,228,246,196,189,203,186,208,241,232,244])).
% 59.47/59.60 cnf(5297,plain,
% 59.47/59.60 (P5(x52971,x52971,x52972,x52972)),
% 59.47/59.60 inference(scs_inference,[],[5019,5165,5168,5171,5174,5240,5243,5247,5253,5256,5269,5027,5029,5112,5163,4850,5005,5122,4997,4999,5080,5102,5106,4830,4985,4991,4995,5021,5023,5025,5110,5118,5137,5139,5136,4768,4993,4934,4826,4733,5160,4909,4941,386,4790,5239,5246,5252,4377,4452,4503,4860,4717,4635,4816,277,319,373,356,949,168,261,161,172,173,262,230,264,263,257,258,156,158,229,231,169,192,171,157,174,170,176,175,260,259,181,133,183,245,204,187,193,194,206,202,199,182,195,228,246,196,189,203,186,208,241,232,244,200,256])).
% 59.47/59.60 cnf(5327,plain,
% 59.47/59.60 (~E(a24,a20)),
% 59.47/59.60 inference(scs_inference,[],[5223,4433])).
% 59.47/59.60 cnf(5328,plain,
% 59.47/59.60 (P4(x53281,x53282,x53283,x53282)),
% 59.47/59.60 inference(rename_variables,[],[5223])).
% 59.47/59.60 cnf(5330,plain,
% 59.47/59.60 (P3(x53301,f4(x53301,x53301,x53302),x53302,x53301)),
% 59.47/59.60 inference(rename_variables,[],[5249])).
% 59.47/59.60 cnf(5333,plain,
% 59.47/59.60 (P3(x53331,f4(x53331,x53331,x53332),x53332,x53331)),
% 59.47/59.60 inference(rename_variables,[],[5249])).
% 59.47/59.60 cnf(5337,plain,
% 59.47/59.60 (P3(x53371,f4(x53371,x53371,x53372),x53372,x53371)),
% 59.47/59.60 inference(rename_variables,[],[5249])).
% 59.47/59.60 cnf(5340,plain,
% 59.47/59.60 (P3(x53401,f4(x53401,x53401,x53402),x53402,x53401)),
% 59.47/59.60 inference(rename_variables,[],[5249])).
% 59.47/59.60 cnf(5343,plain,
% 59.47/59.60 (P3(x53431,f4(x53431,x53431,x53432),x53432,x53431)),
% 59.47/59.60 inference(rename_variables,[],[5249])).
% 59.47/59.60 cnf(5345,plain,
% 59.47/59.60 (P5(f27(x53451,x53452),x53451,f27(x53451,x53452),x53452)),
% 59.47/59.60 inference(scs_inference,[],[5223,5232,5249,5330,5333,5337,5340,5127,4433,1184,356,2,277,373,319,161])).
% 59.47/59.60 cnf(5347,plain,
% 59.47/59.60 (P5(a15,x53471,a15,x53471)),
% 59.47/59.60 inference(scs_inference,[],[5223,5185,5232,5249,5330,5333,5337,5340,5127,4433,1184,356,2,277,373,319,161,173])).
% 59.47/59.60 cnf(5353,plain,
% 59.47/59.60 (P9(a15,a15,x53531,x53532,x53533,a15,x53531,x53532)),
% 59.47/59.60 inference(scs_inference,[],[5223,5164,5185,5209,5181,5232,5249,5330,5333,5337,5340,5127,4433,1184,356,2,277,373,319,161,173,168,263,230])).
% 59.47/59.60 cnf(5363,plain,
% 59.47/59.60 (P9(x53631,x53632,x53631,x53633,x53633,x53632,x53633,x53633)),
% 59.47/59.60 inference(scs_inference,[],[5223,5328,5164,5185,5209,5181,5195,5232,5183,5238,5249,5330,5333,5337,5340,5127,4433,1184,356,2,277,373,319,161,173,168,263,230,172,264,262,231,229])).
% 59.47/59.60 cnf(5365,plain,
% 59.47/59.60 (P1(x53651,f5(x53652,x53652,x53651),x53652)),
% 59.47/59.60 inference(scs_inference,[],[5223,5328,5164,5185,5209,5181,5195,5232,5183,5238,5249,5330,5333,5337,5340,5233,5127,4433,1184,356,2,277,373,319,161,173,168,263,230,172,264,262,231,229,156])).
% 59.47/59.60 cnf(5371,plain,
% 59.47/59.60 (P9(x53711,x53712,a19,a1,x53711,x53712,a15,a2)),
% 59.47/59.60 inference(scs_inference,[],[5223,5328,5164,5185,5191,5209,4968,5181,5195,5232,5183,5238,5249,5330,5333,5337,5340,5233,5127,4433,1184,356,2,277,373,319,161,173,168,263,230,172,264,262,231,229,156,257,169,258])).
% 59.47/59.60 cnf(5373,plain,
% 59.47/59.60 (P4(x53731,x53732,x53733,x53731)),
% 59.47/59.60 inference(scs_inference,[],[5223,5328,5164,5185,5191,5209,4968,5181,5195,5232,5183,5238,5249,5330,5333,5337,5340,5233,5127,4433,1184,356,2,277,373,319,161,173,168,263,230,172,264,262,231,229,156,257,169,258,174])).
% 59.47/59.60 cnf(5375,plain,
% 59.47/59.60 (P3(x53751,x53751,x53751,a15)),
% 59.47/59.60 inference(scs_inference,[],[5223,5328,5164,5219,5185,5191,5209,4968,5181,5195,5232,5183,5238,5249,5330,5333,5337,5340,5233,5127,4433,1184,356,2,277,373,319,161,173,168,263,230,172,264,262,231,229,156,257,169,258,174,171])).
% 59.47/59.60 cnf(5377,plain,
% 59.47/59.60 (P1(f5(x53771,x53771,x53772),x53771,x53772)),
% 59.47/59.60 inference(scs_inference,[],[5223,5328,5164,5219,5185,5191,5209,4968,5181,5195,5232,5183,5238,5249,5330,5333,5337,5340,5233,5127,4433,1184,356,2,277,373,319,161,173,168,263,230,172,264,262,231,229,156,257,169,258,174,171,157])).
% 59.47/59.60 cnf(5379,plain,
% 59.47/59.60 (P4(x53791,x53792,x53792,x53793)),
% 59.47/59.60 inference(scs_inference,[],[5223,5328,5164,5219,5185,5191,5209,4968,5181,5195,5232,5183,5238,5249,5330,5333,5337,5340,5233,5127,4433,1184,356,2,277,373,319,161,173,168,263,230,172,264,262,231,229,156,257,169,258,174,171,157,176])).
% 59.47/59.60 cnf(5381,plain,
% 59.47/59.60 (P3(a15,a2,a19,a1)),
% 59.47/59.60 inference(scs_inference,[],[5223,5328,5164,5219,5185,5191,5209,4968,5181,5195,5232,5242,5183,5238,5249,5330,5333,5337,5340,5233,5127,4433,1184,356,2,277,373,319,161,173,168,263,230,172,264,262,231,229,156,257,169,258,174,171,157,176,170])).
% 59.47/59.60 cnf(5392,plain,
% 59.47/59.60 (P3(a15,a15,a15,x53921)),
% 59.47/59.60 inference(rename_variables,[],[5102])).
% 59.47/59.60 cnf(5395,plain,
% 59.47/59.60 (P3(a15,a15,a15,x53951)),
% 59.47/59.60 inference(rename_variables,[],[5102])).
% 59.47/59.60 cnf(5396,plain,
% 59.47/59.60 (P5(x53961,x53961,x53962,x53962)),
% 59.47/59.60 inference(rename_variables,[],[5297])).
% 59.47/59.60 cnf(5400,plain,
% 59.47/59.60 (P3(a15,a15,a15,x54001)),
% 59.47/59.60 inference(rename_variables,[],[5102])).
% 59.47/59.60 cnf(5403,plain,
% 59.47/59.60 (P3(a15,a15,a15,x54031)),
% 59.47/59.60 inference(rename_variables,[],[5102])).
% 59.47/59.60 cnf(5404,plain,
% 59.47/59.60 (P5(x54041,x54041,x54042,x54042)),
% 59.47/59.60 inference(rename_variables,[],[5297])).
% 59.47/59.60 cnf(5407,plain,
% 59.47/59.60 (P3(x54071,x54072,x54072,x54071)),
% 59.47/59.60 inference(rename_variables,[],[4909])).
% 59.47/59.60 cnf(5410,plain,
% 59.47/59.60 (P3(a15,a15,a15,x54101)),
% 59.47/59.60 inference(rename_variables,[],[5102])).
% 59.47/59.60 cnf(5411,plain,
% 59.47/59.60 (P5(x54111,x54111,x54112,x54112)),
% 59.47/59.60 inference(rename_variables,[],[5297])).
% 59.47/59.60 cnf(5414,plain,
% 59.47/59.60 (P3(a15,a15,a15,x54141)),
% 59.47/59.60 inference(rename_variables,[],[5102])).
% 59.47/59.60 cnf(5417,plain,
% 59.47/59.60 (P10(a15,a15,x54171,a15)),
% 59.47/59.60 inference(rename_variables,[],[5209])).
% 59.47/59.60 cnf(5418,plain,
% 59.47/59.60 (P9(x54181,x54182,a19,a1,x54181,x54182,a2,a15)),
% 59.47/59.60 inference(rename_variables,[],[5199])).
% 59.47/59.60 cnf(5423,plain,
% 59.47/59.60 (P3(x54231,x54232,x54232,x54231)),
% 59.47/59.60 inference(rename_variables,[],[4909])).
% 59.47/59.60 cnf(5434,plain,
% 59.47/59.60 (P3(a15,a15,a15,x54341)),
% 59.47/59.60 inference(rename_variables,[],[5102])).
% 59.47/59.60 cnf(5435,plain,
% 59.47/59.60 (P4(x54351,x54352,x54353,x54353)),
% 59.47/59.60 inference(rename_variables,[],[5112])).
% 59.47/59.60 cnf(5437,plain,
% 59.47/59.60 (P2(f30(x54371,x54371,x54371,x54371,x54371,x54371),x54371,x54371,x54371)),
% 59.47/59.60 inference(scs_inference,[],[142,5297,5396,5404,5223,5328,5164,5219,5185,5191,5199,5209,4846,4968,5007,5181,5193,5195,5232,5242,5183,5238,5249,5330,5333,5337,5340,5233,5274,5289,5283,5003,4601,5127,5112,5102,5392,5395,5400,5403,5410,5414,4915,4909,5407,5423,5122,394,4433,1184,356,2,277,373,319,161,173,168,263,230,172,264,262,231,229,156,257,169,258,174,171,157,176,170,175,260,259,268,253,205,132,252,204,194,206,202,245,267,195,234,182,228,196,189])).
% 59.47/59.60 cnf(5454,plain,
% 59.47/59.60 (P10(a15,a15,a15,x54541)),
% 59.47/59.60 inference(rename_variables,[],[5080])).
% 59.47/59.60 cnf(5455,plain,
% 59.47/59.60 (P10(a15,a15,x54551,a15)),
% 59.47/59.60 inference(rename_variables,[],[5209])).
% 59.47/59.60 cnf(5456,plain,
% 59.47/59.60 (P1(x54561,x54562,x54562)),
% 59.47/59.60 inference(rename_variables,[],[4452])).
% 59.47/59.60 cnf(5457,plain,
% 59.47/59.60 (P7(x54571,x54571,x54571)),
% 59.47/59.60 inference(rename_variables,[],[4930])).
% 59.47/59.60 cnf(5459,plain,
% 59.47/59.60 (P8(f33(a15,a15,a15,a15,a22,a15),a17,a17,a17,f33(a15,a15,a15,a15,a22,a15),a15,a15,a15)),
% 59.47/59.60 inference(scs_inference,[],[142,5297,5396,5404,5411,5223,5328,5164,5219,5185,5191,5199,5418,5209,5417,5455,4846,4968,5007,5181,5193,5195,5232,5242,5183,5238,5249,5330,5333,5337,5340,5343,5233,5274,5289,5283,5003,4601,5127,5112,5102,5392,5395,5400,5403,5410,5414,5434,5080,5454,4915,4909,5407,5423,5122,394,4452,5456,4717,4930,5457,4433,1184,356,2,277,373,319,161,173,168,263,230,172,264,262,231,229,156,257,169,258,174,171,157,176,170,175,260,259,268,253,205,132,252,204,194,206,202,245,267,195,234,182,228,196,189,203,246,186,232,200,954,959])).
% 59.47/59.60 cnf(5471,plain,
% 59.47/59.60 (P10(f3(a15,a15,a15),a15,f3(a15,a15,a15),f3(a15,a15,a15))),
% 59.47/59.60 inference(scs_inference,[],[142,5297,5396,5404,5411,5223,5328,5164,5219,5185,5191,5199,5418,5209,5417,5455,4846,4968,5007,5181,5193,5195,5232,5242,5183,5238,5249,5330,5333,5337,5340,5343,5233,5274,5289,5286,5283,5003,4601,5127,5112,5435,5102,5392,5395,5400,5403,5410,5414,5434,5027,5080,5454,4915,4909,5407,5423,5122,394,4452,5456,4717,4930,5457,4433,1184,356,2,277,373,319,161,173,168,263,230,172,264,262,231,229,156,257,169,258,174,171,157,176,170,175,260,259,268,253,205,132,252,204,194,206,202,245,267,195,234,182,228,196,189,203,246,186,232,200,954,959,256,238])).
% 59.47/59.60 cnf(5477,plain,
% 59.47/59.60 (P4(a17,a17,f23(a17,a17,a15,a17),a15)),
% 59.47/59.60 inference(scs_inference,[],[142,5297,5396,5404,5411,5223,5328,5164,5219,5185,5191,5199,5418,5209,5417,5455,4846,4968,5007,5181,5193,5195,5213,5232,5242,5183,5238,5249,5330,5333,5337,5340,5343,5233,4807,5274,5289,5286,5283,5003,4601,5127,5112,5435,5102,5392,5395,5400,5403,5410,5414,5434,5027,5080,5454,4915,4909,5407,5423,5122,394,4452,5456,4635,4717,4930,5457,4433,1184,356,2,277,373,319,161,173,168,263,230,172,264,262,231,229,156,257,169,258,174,171,157,176,170,175,260,259,268,253,205,132,252,204,194,206,202,245,267,195,234,182,228,196,189,203,246,186,232,200,954,959,256,238,261,198,241])).
% 59.47/59.60 cnf(5480,plain,
% 59.47/59.60 (P7(f6(a16,a2,a2),a16,a2)),
% 59.47/59.60 inference(scs_inference,[],[142,5297,5396,5404,5411,5223,5328,5164,5219,5185,5191,5199,5418,5209,5417,5455,4846,4968,5007,5181,5193,5195,5213,5232,5242,5183,5238,5249,5330,5333,5337,5340,5343,5233,4807,5274,5289,5286,5283,5003,4601,5127,5019,5112,5435,5102,5392,5395,5400,5403,5410,5414,5434,5027,5080,5454,4915,4909,5407,5423,5122,394,4452,5456,4635,4717,4930,5457,4433,1184,356,2,277,373,319,161,173,168,263,230,172,264,262,231,229,156,257,169,258,174,171,157,176,170,175,260,259,268,253,205,132,252,204,194,206,202,245,267,195,234,182,228,196,189,203,246,186,232,200,954,959,256,238,261,198,241,191])).
% 59.47/59.60 cnf(5508,plain,
% 59.47/59.60 (P3(x55081,f5(x55081,x55081,x55082),x55082,x55081)),
% 59.47/59.60 inference(rename_variables,[],[5263])).
% 59.47/59.60 cnf(5511,plain,
% 59.47/59.60 (P3(x55111,f5(x55111,x55111,x55112),x55112,x55111)),
% 59.47/59.60 inference(rename_variables,[],[5263])).
% 59.47/59.60 cnf(5514,plain,
% 59.47/59.60 (P3(x55141,f5(x55141,x55141,x55142),x55142,x55141)),
% 59.47/59.60 inference(rename_variables,[],[5263])).
% 59.47/59.60 cnf(5517,plain,
% 59.47/59.60 (P3(x55171,f5(x55171,x55171,x55172),x55172,x55171)),
% 59.47/59.60 inference(rename_variables,[],[5263])).
% 59.47/59.60 cnf(5574,plain,
% 59.47/59.60 (P3(x55741,x55742,x55742,x55741)),
% 59.47/59.60 inference(rename_variables,[],[4909])).
% 59.47/59.60 cnf(5578,plain,
% 59.47/59.60 (P4(x55781,x55782,x55782,x55783)),
% 59.47/59.60 inference(rename_variables,[],[5379])).
% 59.47/59.60 cnf(5581,plain,
% 59.47/59.60 (P4(x55811,x55812,x55812,x55813)),
% 59.47/59.60 inference(rename_variables,[],[5379])).
% 59.47/59.60 cnf(5586,plain,
% 59.47/59.60 (P4(x55861,x55861,x55862,x55863)),
% 59.47/59.60 inference(scs_inference,[],[5363,5373,5379,5578,5581,5047,5375,5353,5347,4971,5327,5381,5265,5251,5345,5365,5377,5477,5459,5480,5263,5508,5511,5514,5517,4826,5021,365,4909,1184,356,373,277,319,2,168,173,161,159,172,264,229,230,263,261,169,257,158,231,262,156,258,171,174,157,176,260,170,175,259,181,235,134,188,190])).
% 59.47/59.60 cnf(5588,plain,
% 59.47/59.60 (P4(x55881,x55882,x55883,x55881)),
% 59.47/59.60 inference(rename_variables,[],[5373])).
% 59.47/59.60 cnf(5591,plain,
% 59.47/59.60 (P3(x55911,x55911,x55911,a15)),
% 59.47/59.60 inference(rename_variables,[],[5375])).
% 59.47/59.60 cnf(5598,plain,
% 59.47/59.60 (P3(x55981,x55982,x55982,x55981)),
% 59.47/59.60 inference(rename_variables,[],[4909])).
% 59.47/59.60 cnf(5603,plain,
% 59.47/59.60 (P3(x56031,x56032,x56032,x56031)),
% 59.47/59.60 inference(rename_variables,[],[4909])).
% 59.47/59.60 cnf(5608,plain,
% 59.47/59.60 (P3(x56081,x56082,x56082,x56081)),
% 59.47/59.60 inference(rename_variables,[],[4909])).
% 59.47/59.60 cnf(5614,plain,
% 59.47/59.60 (P9(x56141,x56142,x56141,x56143,x56143,x56142,x56143,x56143)),
% 59.47/59.60 inference(rename_variables,[],[5363])).
% 59.47/59.60 cnf(5623,plain,
% 59.47/59.60 (P4(x56231,x56232,x56233,x56231)),
% 59.47/59.60 inference(rename_variables,[],[5373])).
% 59.47/59.60 cnf(5647,plain,
% 59.47/59.60 (~P4(a19,a19,a21,a24)),
% 59.47/59.60 inference(scs_inference,[],[5363,5614,5373,5588,5623,5379,5578,5581,5047,5375,5591,5353,5347,5371,4971,5327,5381,5265,5437,5251,5345,5365,5377,5471,4906,5477,5459,5480,4840,5263,5508,5511,5514,5517,5176,5089,4765,4846,4826,5021,365,5080,4909,5574,5598,5603,5608,5122,4915,854,4456,1184,356,373,277,319,2,168,173,161,159,172,264,229,230,263,261,169,257,158,231,262,156,258,171,174,157,176,260,170,175,259,181,235,134,188,190,252,204,205,253,206,193,202,194,199,245,247,195,196,228,246,189,203,186,232,197,180,5141])).
% 59.47/59.60 cnf(5669,plain,
% 59.47/59.60 ($false),
% 59.47/59.60 inference(scs_inference,[],[5586,5647]),
% 59.47/59.60 ['proof']).
% 59.47/59.60 % SZS output end Proof
% 59.47/59.60 % Total time :58.760000s
%------------------------------------------------------------------------------