%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : GEO640+1 : TPTP v8.2.0. Released v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% Computer : n025.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:02 EDT 2024
% Result : Theorem 59.63s 59.71s
% Output : CNFRefutation 59.77s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : GEO640+1 : TPTP v8.2.0. Released v7.5.0.
% 0.07/0.12 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% 0.12/0.33 % Computer : n025.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:45:54 EDT 2024
% 0.12/0.33 % CPUTime :
% 0.46/0.58 start to proof:theBenchmark
% 59.63/59.69 %-------------------------------------------
% 59.63/59.69 % File :CSE---1.7
% 59.63/59.69 % Problem :theBenchmark
% 59.63/59.69 % Transform :cnf
% 59.63/59.69 % Format :tptp:raw
% 59.63/59.69 % Command :java -jar mcs_scs.jar %d %s
% 59.63/59.69
% 59.63/59.69 % Result :Theorem 59.030000s
% 59.63/59.69 % Output :CNFRefutation 59.030000s
% 59.63/59.69 %-------------------------------------------
% 59.63/59.70 %------------------------------------------------------------------------------
% 59.63/59.70 % File : GEO640+1 : TPTP v8.2.0. Released v7.5.0.
% 59.63/59.70 % Domain : Geometry
% 59.63/59.70 % Problem : JGEX problem 106
% 59.63/59.70 % Version : [CGZ00] axioms.
% 59.63/59.70 % English :
% 59.63/59.70
% 59.63/59.70 % Refs : [CGZ00] Chou et al. (2000), A Deductive Database Approach to A
% 59.63/59.70 % : [YCG08] Ye et al. (2008), An Introduction to Java Geometry Exp
% 59.63/59.70 % : [Qua20] Quaresma (2020), Email to Geoff Sutcliffe
% 59.63/59.70 % Source : [Qua20]
% 59.63/59.70 % Names : 106.p [Qua20]
% 59.63/59.70
% 59.63/59.70 % Status : Theorem
% 59.63/59.70 % Rating : 0.50 v7.5.0
% 59.63/59.70 % Syntax : Number of formulae : 95 ( 0 unt; 0 def)
% 59.63/59.70 % Number of atoms : 309 ( 1 equ)
% 59.63/59.71 % Maximal formula atoms : 26 ( 3 avg)
% 59.63/59.71 % Number of connectives : 221 ( 7 ~; 0 |; 119 &)
% 59.63/59.71 % ( 0 <=>; 95 =>; 0 <=; 0 <~>)
% 59.63/59.71 % Maximal formula depth : 56 ( 9 avg)
% 59.63/59.71 % Maximal term depth : 1 ( 1 avg)
% 59.63/59.71 % Number of predicates : 12 ( 11 usr; 0 prp; 2-8 aty)
% 59.63/59.71 % Number of functors : 0 ( 0 usr; 0 con; --- aty)
% 59.63/59.71 % Number of variables : 552 ( 532 !; 20 ?)
% 59.63/59.71 % SPC : FOF_THM_RFO_SEQ
% 59.63/59.71
% 59.63/59.71 % Comments : Taken from JGEX [YCG08], converted by Pedro Quaresma.
% 59.63/59.71 %------------------------------------------------------------------------------
% 59.63/59.71 include('Axioms/GEO012+0.ax').
% 59.63/59.71 %------------------------------------------------------------------------------
% 59.63/59.71 fof(exemplo6GDDFULL81109106,conjecture,
% 59.63/59.71 ! [Q4,Q1,Q3,Q0,Q2,P0,P1,P2,P3,P4,O0,O4,O3,O2,O1,M0,M4,M3,M2,M1,NWPNT1,NWPNT2,NWPNT3,NWPNT4,NWPNT5,NWPNT6,NWPNT7,NWPNT8,NWPNT9,NWPNT01] :
% 59.63/59.71 ( ( coll(P0,Q4,Q1)
% 59.63/59.71 & coll(P0,Q0,Q2)
% 59.63/59.71 & coll(P1,Q1,Q3)
% 59.63/59.71 & coll(P1,Q0,Q2)
% 59.63/59.71 & coll(P2,Q1,Q3)
% 59.63/59.71 & coll(P2,Q4,Q2)
% 59.63/59.71 & coll(P3,Q3,Q0)
% 59.63/59.71 & coll(P3,Q4,Q2)
% 59.63/59.71 & coll(P4,Q4,Q1)
% 59.63/59.71 & coll(P4,Q3,Q0)
% 59.63/59.71 & circle(O0,Q0,P0,P4)
% 59.63/59.71 & circle(O4,P4,P3,Q4)
% 59.63/59.71 & circle(O3,P3,P2,Q3)
% 59.63/59.71 & circle(O2,P1,P2,Q2)
% 59.63/59.71 & circle(O1,P1,Q1,P0)
% 59.63/59.71 & circle(O0,Q0,M0,NWPNT1)
% 59.63/59.71 & circle(O1,Q1,M0,NWPNT2)
% 59.63/59.71 & circle(O0,Q0,M4,NWPNT3)
% 59.63/59.71 & circle(O4,Q4,M4,NWPNT4)
% 59.63/59.71 & circle(O4,Q4,M3,NWPNT5)
% 59.63/59.71 & circle(O3,Q3,M3,NWPNT6)
% 59.63/59.71 & circle(O3,Q3,M2,NWPNT7)
% 59.63/59.71 & circle(O2,Q2,M2,NWPNT8)
% 59.63/59.71 & circle(O2,Q2,M1,NWPNT9)
% 59.63/59.71 & circle(O1,Q1,M1,NWPNT01) )
% 59.63/59.71 => cyclic(M4,M3,M2,M1) ) ).
% 59.63/59.71
% 59.63/59.71 %------------------------------------------------------------------------------
% 59.63/59.71 %-------------------------------------------
% 59.63/59.71 % Proof found
% 59.63/59.71 % SZS status Theorem for theBenchmark
% 59.63/59.71 % SZS output start Proof
% 59.63/59.71 %ClaNum:280(EqnAxiom:141)
% 59.63/59.71 %VarNum:1613(SingletonVarNum:590)
% 59.63/59.71 %MaxLitNum:5
% 59.63/59.71 %MaxfuncDepth:1
% 59.63/59.71 %SharedTerms:56
% 59.63/59.71 %goalClause: 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167
% 59.63/59.71 %singleGoalClaCount:26
% 59.63/59.71 [142]P1(a1,a2,a15)
% 59.63/59.71 [143]P1(a1,a16,a18)
% 59.63/59.71 [144]P1(a19,a15,a17)
% 59.63/59.71 [145]P1(a19,a16,a18)
% 59.63/59.71 [146]P1(a20,a2,a18)
% 59.63/59.71 [147]P1(a20,a15,a17)
% 59.63/59.71 [148]P1(a21,a2,a18)
% 59.63/59.71 [149]P1(a21,a17,a16)
% 59.63/59.71 [150]P1(a22,a2,a15)
% 59.63/59.71 [151]P1(a22,a17,a16)
% 59.63/59.71 [152]P2(a24,a16,a1,a22)
% 59.63/59.71 [153]P2(a24,a16,a25,a30)
% 59.63/59.71 [154]P2(a24,a16,a31,a36)
% 59.63/59.71 [155]P2(a26,a2,a31,a38)
% 59.63/59.71 [156]P2(a26,a2,a32,a39)
% 59.63/59.71 [157]P2(a26,a22,a21,a2)
% 59.63/59.71 [158]P2(a27,a17,a32,a40)
% 59.63/59.71 [159]P2(a27,a17,a33,a41)
% 59.63/59.71 [160]P2(a27,a21,a20,a17)
% 59.63/59.71 [161]P2(a28,a18,a33,a42)
% 59.63/59.71 [162]P2(a28,a18,a34,a43)
% 59.63/59.71 [163]P2(a28,a19,a20,a18)
% 59.63/59.71 [164]P2(a29,a15,a25,a37)
% 59.63/59.71 [165]P2(a29,a15,a34,a44)
% 59.63/59.72 [166]P2(a29,a19,a15,a1)
% 59.63/59.72 [167]~P3(a31,a32,a33,a34)
% 59.63/59.72 [168]~P1(x1682,x1681,x1683)+P1(x1681,x1682,x1683)
% 59.63/59.72 [169]~P1(x1691,x1693,x1692)+P1(x1691,x1692,x1693)
% 59.63/59.72 [170]~P6(x1701,x1702,x1703)+P1(x1701,x1702,x1703)
% 59.63/59.72 [171]~P6(x1711,x1713,x1712)+P6(x1711,x1712,x1713)
% 59.63/59.72 [173]~P6(x1731,x1732,x1733)+P4(x1731,x1732,x1731,x1733)
% 59.63/59.72 [177]~P9(x1771,x1772,x1771,x1773)+P1(x1771,x1772,x1773)
% 59.63/59.72 [243]~P4(x2431,x2432,x2431,x2433)+P8(x2431,x2432,x2432,x2433,x2432,x2433,x2431,x2433)
% 59.63/59.72 [180]~P9(x1803,x1804,x1801,x1802)+P9(x1801,x1802,x1803,x1804)
% 59.63/59.72 [181]~P9(x1811,x1812,x1814,x1813)+P9(x1811,x1812,x1813,x1814)
% 59.63/59.72 [182]~P10(x1823,x1824,x1821,x1822)+P10(x1821,x1822,x1823,x1824)
% 59.63/59.72 [183]~P10(x1831,x1832,x1834,x1833)+P10(x1831,x1832,x1833,x1834)
% 59.63/59.72 [184]~P4(x1843,x1844,x1841,x1842)+P4(x1841,x1842,x1843,x1844)
% 59.63/59.72 [185]~P4(x1851,x1852,x1854,x1853)+P4(x1851,x1852,x1853,x1854)
% 59.63/59.72 [186]~P3(x1862,x1861,x1863,x1864)+P3(x1861,x1862,x1863,x1864)
% 59.63/59.72 [187]~P3(x1871,x1873,x1872,x1874)+P3(x1871,x1872,x1873,x1874)
% 59.63/59.72 [188]~P3(x1881,x1882,x1884,x1883)+P3(x1881,x1882,x1883,x1884)
% 59.63/59.72 [241]~P3(x2412,x2413,x2411,x2414)+P8(x2411,x2412,x2411,x2413,x2414,x2412,x2414,x2413)
% 59.63/59.72 [204]~P2(x2044,x2041,x2042,x2043)+P10(f7(x2041,x2042,x2043,x2044),x2041,x2041,x2044)
% 59.63/59.72 [219]P4(x2191,x2192,x2193,x2194)+~P5(x2191,x2192,x2195,x2193,x2194,x2196)
% 59.63/59.72 [231]~P11(x2314,x2315,x2316,x2311,x2312,x2313)+P11(x2311,x2312,x2313,x2314,x2315,x2316)
% 59.63/59.72 [232]~P11(x2322,x2321,x2323,x2325,x2324,x2326)+P11(x2321,x2322,x2323,x2324,x2325,x2326)
% 59.63/59.72 [233]~P11(x2331,x2333,x2332,x2334,x2336,x2335)+P11(x2331,x2332,x2333,x2334,x2335,x2336)
% 59.63/59.72 [234]~P5(x2344,x2345,x2346,x2341,x2342,x2343)+P5(x2341,x2342,x2343,x2344,x2345,x2346)
% 59.63/59.72 [235]~P5(x2352,x2351,x2353,x2355,x2354,x2356)+P5(x2351,x2352,x2353,x2354,x2355,x2356)
% 59.63/59.72 [236]~P5(x2361,x2363,x2362,x2364,x2366,x2365)+P5(x2361,x2362,x2363,x2364,x2365,x2366)
% 59.63/59.72 [242]~P9(x2421,x2422,x2425,x2426)+P8(x2421,x2422,x2423,x2424,x2425,x2426,x2423,x2424)
% 59.63/59.72 [248]~P11(x2481,x2482,x2483,x2484,x2485,x2486)+P8(x2481,x2482,x2482,x2483,x2484,x2485,x2485,x2486)
% 59.63/59.72 [249]~P11(x2491,x2492,x2493,x2494,x2495,x2496)+P7(x2491,x2492,x2491,x2493,x2494,x2495,x2494,x2496)
% 59.63/59.72 [250]~P8(x2501,x2502,x2505,x2506,x2503,x2504,x2505,x2506)+P9(x2501,x2502,x2503,x2504)
% 59.63/59.72 [269]~P8(x2695,x2696,x2697,x2698,x2691,x2692,x2693,x2694)+P8(x2691,x2692,x2693,x2694,x2695,x2696,x2697,x2698)
% 59.63/59.72 [270]~P8(x2703,x2704,x2701,x2702,x2707,x2708,x2705,x2706)+P8(x2701,x2702,x2703,x2704,x2705,x2706,x2707,x2708)
% 59.63/59.72 [271]~P8(x2712,x2711,x2713,x2714,x2715,x2716,x2717,x2718)+P8(x2711,x2712,x2713,x2714,x2715,x2716,x2717,x2718)
% 59.63/59.72 [272]~P8(x2721,x2722,x2725,x2726,x2723,x2724,x2727,x2728)+P8(x2721,x2722,x2723,x2724,x2725,x2726,x2727,x2728)
% 59.63/59.72 [273]~P7(x2735,x2736,x2737,x2738,x2731,x2732,x2733,x2734)+P7(x2731,x2732,x2733,x2734,x2735,x2736,x2737,x2738)
% 59.63/59.72 [274]~P7(x2743,x2744,x2741,x2742,x2747,x2748,x2745,x2746)+P7(x2741,x2742,x2743,x2744,x2745,x2746,x2747,x2748)
% 59.63/59.72 [275]~P7(x2752,x2751,x2753,x2754,x2755,x2756,x2757,x2758)+P7(x2751,x2752,x2753,x2754,x2755,x2756,x2757,x2758)
% 59.63/59.72 [276]~P7(x2761,x2762,x2765,x2766,x2763,x2764,x2767,x2768)+P7(x2761,x2762,x2763,x2764,x2765,x2766,x2767,x2768)
% 59.63/59.72 [178]~P1(x1781,x1782,x1783)+~P4(x1781,x1782,x1781,x1783)+P6(x1781,x1782,x1783)
% 59.63/59.72 [252]P4(x2521,x2522,x2521,x2523)+~P8(x2521,x2522,x2522,x2523,x2522,x2523,x2521,x2523)+P1(x2521,x2522,x2523)
% 59.63/59.72 [193]~P10(x1931,x1932,x1932,x1933)+~P4(x1932,x1931,x1932,x1933)+P1(x1931,x1932,f3(x1931,x1933,x1932))
% 59.63/59.72 [205]~P10(x2052,x2051,x2051,x2053)+~P4(x2051,x2052,x2051,x2053)+P4(x2051,x2052,x2051,f3(x2052,x2053,x2051))
% 59.63/59.72 [172]~P1(x1723,x1724,x1721)+P1(x1721,x1722,x1723)+~P1(x1723,x1724,x1722)
% 59.63/59.72 [189]~P2(x1894,x1891,x1892,x1893)+P10(x1891,x1892,x1892,x1893)+~P1(x1894,x1891,x1893)
% 59.63/59.72 [190]~P10(x1901,x1904,x1902,x1903)+P4(x1901,x1902,x1901,x1903)+~P6(x1904,x1902,x1903)
% 59.63/59.72 [191]~P10(x1911,x1913,x1913,x1914)+P4(x1911,x1912,x1913,x1912)+~P6(x1912,x1911,x1914)
% 59.63/59.72 [198]~P4(x1981,x1984,x1982,x1984)+~P4(x1981,x1983,x1982,x1983)+P10(x1981,x1982,x1983,x1984)
% 59.63/59.72 [201]~P4(x2011,x2012,x2011,x2014)+~P4(x2011,x2012,x2011,x2013)+P2(x2011,x2012,x2013,x2014)
% 59.63/59.72 [247]~P9(x2471,x2474,x2473,x2472)+~P3(x2471,x2474,x2473,x2472)+P8(x2471,x2472,x2473,x2472,x2473,x2472,x2473,x2474)
% 59.63/59.72 [251]~P8(x2511,x2513,x2511,x2514,x2512,x2513,x2512,x2514)+P1(x2511,x2512,x2513)+P3(x2513,x2514,x2511,x2512)
% 59.63/59.72 [253]~P1(x2533,x2534,x2532)+~P8(x2533,x2531,x2533,x2532,x2534,x2531,x2534,x2532)+P3(x2531,x2532,x2533,x2534)
% 59.63/59.72 [255]P10(x2551,x2552,x2553,x2554)+~P8(x2551,x2552,x2553,x2554,x2553,x2554,x2551,x2552)+P9(x2551,x2552,x2553,x2554)
% 59.63/59.72 [194]~P10(x1941,x1944,x1942,x1943)+~P10(x1942,x1944,x1941,x1943)+P1(f4(x1941,x1942,x1943),x1943,x1942)
% 59.63/59.72 [195]~P10(x1951,x1954,x1952,x1953)+~P10(x1952,x1954,x1951,x1953)+P1(f5(x1951,x1952,x1953),x1953,x1951)
% 59.63/59.72 [206]~P10(x2061,x2064,x2062,x2063)+~P10(x2062,x2064,x2061,x2063)+P10(x2061,f4(x2061,x2062,x2063),x2063,x2062)
% 59.63/59.72 [207]~P10(x2071,x2074,x2072,x2073)+~P10(x2072,x2074,x2071,x2073)+P10(x2071,f5(x2072,x2071,x2073),x2073,x2072)
% 59.63/59.72 [208]~P10(x2081,x2083,x2083,x2082)+~P3(x2081,x2082,x2083,x2084)+P2(f8(x2081,x2082,x2083),x2081,x2082,x2083)
% 59.63/59.72 [210]~P10(x2103,x2104,x2102,x2101)+~P4(x2103,x2102,x2103,x2101)+P1(x2101,x2102,f45(x2102,x2101,x2103,x2104))
% 59.63/59.72 [211]~P10(x2113,x2114,x2111,x2112)+~P4(x2113,x2111,x2113,x2112)+P1(f45(x2111,x2112,x2113,x2114),x2113,x2114)
% 59.63/59.72 [262]~P4(x2623,x2622,x2623,x2621)+~P8(x2622,x2623,x2623,x2624,x2623,x2624,x2623,x2621)+P1(x2621,x2622,f23(x2622,x2621,x2623,x2624))
% 59.63/59.72 [263]~P10(x2633,x2634,x2632,x2631)+~P8(x2632,x2633,x2633,x2634,x2633,x2634,x2633,x2631)+P1(x2631,x2632,f35(x2632,x2631,x2633,x2634))
% 59.63/59.72 [264]~P10(x2643,x2642,x2642,x2641)+~P8(x2644,x2643,x2642,x2643,x2642,x2643,x2641,x2643)+P1(f14(x2641,x2642,x2643,x2644),x2643,x2644)
% 59.63/59.72 [265]~P10(x2653,x2652,x2652,x2651)+~P8(x2654,x2653,x2652,x2653,x2652,x2653,x2651,x2653)+P1(f14(x2651,x2652,x2653,x2654),x2651,x2652)
% 59.63/59.72 [266]~P4(x2663,x2661,x2663,x2662)+~P8(x2661,x2663,x2663,x2664,x2663,x2664,x2663,x2662)+P1(f23(x2661,x2662,x2663,x2664),x2663,x2664)
% 59.63/59.72 [267]~P10(x2673,x2674,x2671,x2672)+~P8(x2671,x2673,x2673,x2674,x2673,x2674,x2673,x2672)+P1(f35(x2671,x2672,x2673,x2674),x2673,x2674)
% 59.63/59.72 [174]~P6(x1745,x1741,x1743)+P9(x1741,x1742,x1743,x1744)+~P6(x1745,x1742,x1744)
% 59.63/59.72 [175]~P6(x1751,x1755,x1753)+P9(x1751,x1752,x1753,x1754)+~P6(x1752,x1755,x1754)
% 59.63/59.72 [202]~P3(x2025,x2021,x2022,x2023)+P3(x2021,x2022,x2023,x2024)+~P3(x2025,x2021,x2022,x2024)
% 59.63/59.72 [244]~P6(x2445,x2442,x2443)+~P2(x2444,x2441,x2442,x2443)+P8(x2441,x2442,x2441,x2443,x2444,x2442,x2444,x2445)
% 59.63/59.72 [246]~P2(x2465,x2461,x2463,x2464)+P8(x2461,x2462,x2461,x2463,x2464,x2461,x2464,x2463)+~P10(x2465,x2461,x2461,x2462)
% 59.63/59.72 [259]~P8(x2592,x2593,x2592,x2594,x2595,x2592,x2595,x2594)+P10(x2591,x2592,x2592,x2593)+~P2(x2591,x2592,x2594,x2595)
% 59.63/59.72 [214]~P1(x2142,x2144,x2145)+~P10(x2141,x2143,x2143,x2142)+P1(f12(x2141,x2142,x2143,x2144,x2145),x2144,x2145)
% 59.63/59.72 [215]~P1(x2152,x2154,x2155)+~P10(x2151,x2153,x2153,x2152)+P10(f12(x2151,x2152,x2153,x2154,x2155),x2151,x2154,x2155)
% 59.63/59.72 [216]~P10(x2163,x2164,x2164,x2161)+~P4(x2161,x2162,x2161,x2165)+P4(x2161,x2162,x2161,f49(x2163,x2164,x2162,x2165,x2161))
% 59.63/59.72 [217]~P10(x2173,x2171,x2171,x2175)+~P4(x2175,x2172,x2175,x2174)+P4(x2171,x2172,x2171,f49(x2173,x2171,x2172,x2174,x2175))
% 59.63/59.72 [218]~P10(x2181,x2182,x2182,x2185)+~P4(x2185,x2183,x2185,x2184)+P9(f49(x2181,x2182,x2183,x2184,x2185),x2183,x2181,x2182)
% 59.63/59.72 [261]~P8(x2611,x2613,x2612,x2613,x2611,x2614,x2612,x2615)+P1(x2611,x2612,x2613)+P3(x2614,x2612,x2613,f48(x2611,x2612,x2613,x2614))
% 59.63/59.72 [277]~P8(x2771,x2773,x2772,x2773,x2771,x2774,x2772,x2775)+P1(x2771,x2772,x2773)+P8(x2771,x2773,x2772,x2773,x2771,f48(x2771,x2772,x2773,x2774),x2772,f48(x2771,x2772,x2773,x2774))
% 59.63/59.72 [196]~P9(x1961,x1962,x1965,x1966)+P9(x1961,x1962,x1963,x1964)+~P9(x1965,x1966,x1963,x1964)
% 59.63/59.72 [197]~P10(x1971,x1972,x1975,x1976)+P9(x1971,x1972,x1973,x1974)+~P10(x1975,x1976,x1973,x1974)
% 59.63/59.72 [199]~P10(x1995,x1996,x1993,x1994)+P10(x1991,x1992,x1993,x1994)+~P9(x1991,x1992,x1995,x1996)
% 59.63/59.72 [200]~P4(x2001,x2002,x2005,x2006)+P4(x2001,x2002,x2003,x2004)+~P4(x2005,x2006,x2003,x2004)
% 59.63/59.72 [237]~P4(x2371,x2372,x2374,x2375)+~P11(x2371,x2372,x2373,x2374,x2375,x2376)+P5(x2371,x2372,x2373,x2374,x2375,x2376)
% 59.63/59.72 [240]~P6(x2404,x2405,x2406)+~P6(x2401,x2402,x2403)+P7(x2401,x2402,x2402,x2403,x2404,x2405,x2405,x2406)
% 59.63/59.72 [220]~P6(x2206,x2203,x2204)+~P6(x2205,x2201,x2202)+P6(f47(x2201,x2202,x2203,x2204,x2205,x2206),x2201,x2204)
% 59.63/59.72 [221]~P6(x2216,x2213,x2214)+~P6(x2215,x2211,x2212)+P9(f47(x2211,x2212,x2213,x2214,x2215,x2216),x2216,x2211,x2213)
% 59.63/59.72 [222]~P6(x2226,x2223,x2224)+~P6(x2225,x2221,x2222)+P9(f47(x2221,x2222,x2223,x2224,x2225,x2226),x2225,x2222,x2224)
% 59.63/59.72 [257]~P8(x2571,x2572,x2573,x2574,x2575,x2576,x2577,x2578)+P9(x2571,x2572,x2573,x2574)+~P9(x2575,x2576,x2577,x2578)
% 59.63/59.72 [258]~P8(x2581,x2582,x2583,x2584,x2585,x2586,x2587,x2588)+P10(x2581,x2582,x2583,x2584)+~P10(x2585,x2586,x2587,x2588)
% 59.63/59.72 [260]~P7(x2601,x2602,x2603,x2604,x2605,x2606,x2607,x2608)+P4(x2601,x2602,x2603,x2604)+~P4(x2605,x2606,x2607,x2608)
% 59.63/59.72 [238]~P11(x2381,x2382,x2383,x2387,x2388,x2389)+P11(x2381,x2382,x2383,x2384,x2385,x2386)+~P11(x2387,x2388,x2389,x2384,x2385,x2386)
% 59.63/59.72 [239]~P5(x2391,x2392,x2393,x2397,x2398,x2399)+P5(x2391,x2392,x2393,x2394,x2395,x2396)+~P5(x2397,x2398,x2399,x2394,x2395,x2396)
% 59.63/59.72 [279]~P8(x2791,x2792,x2793,x2794,x2799,x27910,x27911,x27912)+P8(x2791,x2792,x2793,x2794,x2795,x2796,x2797,x2798)+~P8(x2799,x27910,x27911,x27912,x2795,x2796,x2797,x2798)
% 59.63/59.72 [280]~P7(x2801,x2802,x2803,x2804,x2809,x28010,x28011,x28012)+P7(x2801,x2802,x2803,x2804,x2805,x2806,x2807,x2808)+~P7(x2809,x28010,x28011,x28012,x2805,x2806,x2807,x2808)
% 59.63/59.72 [212]~P4(x2122,x2121,x2124,x2121)+~P3(x2122,x2124,x2121,x2123)+P10(x2121,x2122,x2122,x2123)+~P4(x2122,x2123,x2124,x2123)
% 59.63/59.72 [179]~P1(x1791,x1792,x1793)+~P9(x1794,x1791,x1795,x1793)+P6(x1791,x1792,x1793)+~P6(x1794,x1792,x1795)
% 59.63/59.72 [192]~P9(x1924,x1923,x1925,x1922)+~P9(x1924,x1922,x1925,x1923)+P6(x1921,x1922,x1923)+~P6(x1921,x1924,x1925)
% 59.63/59.72 [213]~P4(x2135,x2131,x2135,x2133)+~P4(x2135,x2131,x2135,x2132)+P3(x2131,x2132,x2133,x2134)+~P4(x2135,x2131,x2135,x2134)
% 59.63/59.72 [245]~P1(x2451,x2454,x2455)+~P1(x2451,x2452,x2453)+~P9(x2452,x2454,x2453,x2455)+P7(x2451,x2452,x2452,x2453,x2451,x2454,x2454,x2455)
% 59.63/59.72 [256]~P1(x2561,x2562,x2563)+~P8(x2565,x2562,x2565,x2563,x2564,x2562,x2564,x2561)+P6(x2561,x2562,x2563)+~P2(x2564,x2565,x2562,x2563)
% 59.63/59.72 [203]~P10(x2033,x2031,x2033,x2035)+~P10(x2031,x2032,x2031,x2033)+~P6(x2034,x2032,x2035)+P6(f6(x2031,x2032,x2033),x2031,x2033)
% 59.63/59.72 [209]~P3(x2091,x2092,x2093,x2095)+~P9(x2091,x2092,x2093,x2095)+~P6(x2094,x2091,x2092)+P2(f9(x2091,x2092,x2093),x2091,x2092,x2093)
% 59.63/59.72 [278]~P8(x2781,x2783,x2782,x2783,x2784,x2786,x2785,x2786)+~P8(x2781,x2782,x2782,x2783,x2784,x2785,x2785,x2786)+P1(x2781,x2782,x2783)+P11(x2781,x2782,x2783,x2784,x2785,x2786)
% 59.63/59.72 [268]~P3(x2681,x2682,x2685,x2684)+~P3(x2681,x2682,x2685,x2683)+~P8(x2685,x2681,x2685,x2682,x2686,x2683,x2686,x2684)+P4(x2681,x2682,x2683,x2684)+~P3(x2681,x2682,x2685,x2686)
% 59.63/59.72 [223]~P1(x2232,x2233,x2234)+~P1(x2231,x2234,x2236)+~P1(x2231,x2233,x2235)+~P9(x2233,x2234,x2235,x2236)+P1(x2231,x2232,f13(x2233,x2234,x2235,x2236,x2231,x2232))
% 59.63/59.72 [224]~P1(x2246,x2241,x2242)+~P1(x2245,x2242,x2244)+~P1(x2245,x2241,x2243)+~P9(x2241,x2242,x2243,x2244)+P1(f13(x2241,x2242,x2243,x2244,x2245,x2246),x2243,x2244)
% 59.63/59.72 [225]~P1(x2253,x2254,x2255)+~P6(x2256,x2251,x2252)+~P9(x2251,x2253,x2255,x2256)+~P9(x2251,x2253,x2252,x2254)+P1(f50(x2251,x2252,x2253,x2254,x2255,x2256),x2256,x2255)
% 59.63/59.72 [226]~P1(x2263,x2264,x2265)+~P6(x2266,x2261,x2262)+~P9(x2261,x2263,x2265,x2266)+~P9(x2261,x2263,x2262,x2264)+P1(f50(x2261,x2262,x2263,x2264,x2265,x2266),x2261,x2264)
% 59.63/59.72 [227]~P4(x2272,x2273,x2272,x2274)+~P4(x2271,x2273,x2271,x2276)+~P2(x2271,x2273,x2274,x2275)+E(x2271,x2272)+P1(f10(x2273,x2274,x2275,x2276,x2271,x2272),x2273,x2275)
% 59.63/59.72 [228]~P4(x2282,x2283,x2282,x2284)+~P4(x2281,x2283,x2281,x2286)+~P2(x2281,x2283,x2284,x2285)+E(x2281,x2282)+P1(f11(x2283,x2284,x2285,x2286,x2281,x2282),x2284,x2286)
% 59.63/59.72 [229]~P4(x2292,x2293,x2292,x2294)+~P4(x2291,x2293,x2291,x2296)+~P2(x2291,x2293,x2294,x2295)+E(x2291,x2292)+P4(f10(x2293,x2294,x2295,x2296,x2291,x2292),x2292,x2292,x2293)
% 59.63/59.72 [230]~P4(x2302,x2303,x2302,x2304)+~P4(x2301,x2303,x2301,x2306)+~P2(x2301,x2303,x2304,x2305)+E(x2301,x2302)+P4(f11(x2303,x2304,x2305,x2306,x2301,x2302),x2302,x2302,x2303)
% 59.63/59.72 [176]~P1(x1763,x1761,x1764)+~P1(x1765,x1761,x1764)+~P6(x1766,x1765,x1763)+~P6(x1767,x1761,x1764)+P6(f46(x1761,x1762),x1761,x1762)
% 59.63/59.72 %EqnAxiom
% 59.63/59.72 [1]E(x11,x11)
% 59.63/59.72 [2]E(x22,x21)+~E(x21,x22)
% 59.63/59.72 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 59.63/59.72 [4]~E(x41,x42)+E(f46(x41,x43),f46(x42,x43))
% 59.63/59.72 [5]~E(x51,x52)+E(f46(x53,x51),f46(x53,x52))
% 59.63/59.72 [6]~E(x61,x62)+E(f3(x61,x63,x64),f3(x62,x63,x64))
% 59.63/59.72 [7]~E(x71,x72)+E(f3(x73,x71,x74),f3(x73,x72,x74))
% 59.63/59.72 [8]~E(x81,x82)+E(f3(x83,x84,x81),f3(x83,x84,x82))
% 59.63/59.72 [9]~E(x91,x92)+E(f4(x91,x93,x94),f4(x92,x93,x94))
% 59.63/59.72 [10]~E(x101,x102)+E(f4(x103,x101,x104),f4(x103,x102,x104))
% 59.63/59.72 [11]~E(x111,x112)+E(f4(x113,x114,x111),f4(x113,x114,x112))
% 59.63/59.72 [12]~E(x121,x122)+E(f5(x121,x123,x124),f5(x122,x123,x124))
% 59.63/59.72 [13]~E(x131,x132)+E(f5(x133,x131,x134),f5(x133,x132,x134))
% 59.63/59.72 [14]~E(x141,x142)+E(f5(x143,x144,x141),f5(x143,x144,x142))
% 59.63/59.72 [15]~E(x151,x152)+E(f6(x151,x153,x154),f6(x152,x153,x154))
% 59.63/59.72 [16]~E(x161,x162)+E(f6(x163,x161,x164),f6(x163,x162,x164))
% 59.63/59.72 [17]~E(x171,x172)+E(f6(x173,x174,x171),f6(x173,x174,x172))
% 59.63/59.72 [18]~E(x181,x182)+E(f7(x181,x183,x184,x185),f7(x182,x183,x184,x185))
% 59.63/59.72 [19]~E(x191,x192)+E(f7(x193,x191,x194,x195),f7(x193,x192,x194,x195))
% 59.63/59.72 [20]~E(x201,x202)+E(f7(x203,x204,x201,x205),f7(x203,x204,x202,x205))
% 59.63/59.72 [21]~E(x211,x212)+E(f7(x213,x214,x215,x211),f7(x213,x214,x215,x212))
% 59.63/59.72 [22]~E(x221,x222)+E(f48(x221,x223,x224,x225),f48(x222,x223,x224,x225))
% 59.63/59.72 [23]~E(x231,x232)+E(f48(x233,x231,x234,x235),f48(x233,x232,x234,x235))
% 59.63/59.72 [24]~E(x241,x242)+E(f48(x243,x244,x241,x245),f48(x243,x244,x242,x245))
% 59.63/59.72 [25]~E(x251,x252)+E(f48(x253,x254,x255,x251),f48(x253,x254,x255,x252))
% 59.63/59.72 [26]~E(x261,x262)+E(f23(x261,x263,x264,x265),f23(x262,x263,x264,x265))
% 59.63/59.72 [27]~E(x271,x272)+E(f23(x273,x271,x274,x275),f23(x273,x272,x274,x275))
% 59.63/59.72 [28]~E(x281,x282)+E(f23(x283,x284,x281,x285),f23(x283,x284,x282,x285))
% 59.63/59.72 [29]~E(x291,x292)+E(f23(x293,x294,x295,x291),f23(x293,x294,x295,x292))
% 59.63/59.72 [30]~E(x301,x302)+E(f35(x301,x303,x304,x305),f35(x302,x303,x304,x305))
% 59.63/59.72 [31]~E(x311,x312)+E(f35(x313,x311,x314,x315),f35(x313,x312,x314,x315))
% 59.63/59.72 [32]~E(x321,x322)+E(f35(x323,x324,x321,x325),f35(x323,x324,x322,x325))
% 59.63/59.72 [33]~E(x331,x332)+E(f35(x333,x334,x335,x331),f35(x333,x334,x335,x332))
% 59.63/59.72 [34]~E(x341,x342)+E(f8(x341,x343,x344),f8(x342,x343,x344))
% 59.63/59.72 [35]~E(x351,x352)+E(f8(x353,x351,x354),f8(x353,x352,x354))
% 59.63/59.72 [36]~E(x361,x362)+E(f8(x363,x364,x361),f8(x363,x364,x362))
% 59.63/59.72 [37]~E(x371,x372)+E(f9(x371,x373,x374),f9(x372,x373,x374))
% 59.63/59.72 [38]~E(x381,x382)+E(f9(x383,x381,x384),f9(x383,x382,x384))
% 59.63/59.72 [39]~E(x391,x392)+E(f9(x393,x394,x391),f9(x393,x394,x392))
% 59.63/59.72 [40]~E(x401,x402)+E(f45(x401,x403,x404,x405),f45(x402,x403,x404,x405))
% 59.63/59.72 [41]~E(x411,x412)+E(f45(x413,x411,x414,x415),f45(x413,x412,x414,x415))
% 59.63/59.72 [42]~E(x421,x422)+E(f45(x423,x424,x421,x425),f45(x423,x424,x422,x425))
% 59.63/59.72 [43]~E(x431,x432)+E(f45(x433,x434,x435,x431),f45(x433,x434,x435,x432))
% 59.63/59.72 [44]~E(x441,x442)+E(f14(x441,x443,x444,x445),f14(x442,x443,x444,x445))
% 59.63/59.72 [45]~E(x451,x452)+E(f14(x453,x451,x454,x455),f14(x453,x452,x454,x455))
% 59.63/59.72 [46]~E(x461,x462)+E(f14(x463,x464,x461,x465),f14(x463,x464,x462,x465))
% 59.63/59.72 [47]~E(x471,x472)+E(f14(x473,x474,x475,x471),f14(x473,x474,x475,x472))
% 59.63/59.72 [48]~E(x481,x482)+E(f12(x481,x483,x484,x485,x486),f12(x482,x483,x484,x485,x486))
% 59.63/59.72 [49]~E(x491,x492)+E(f12(x493,x491,x494,x495,x496),f12(x493,x492,x494,x495,x496))
% 59.63/59.72 [50]~E(x501,x502)+E(f12(x503,x504,x501,x505,x506),f12(x503,x504,x502,x505,x506))
% 59.63/59.72 [51]~E(x511,x512)+E(f12(x513,x514,x515,x511,x516),f12(x513,x514,x515,x512,x516))
% 59.63/59.72 [52]~E(x521,x522)+E(f12(x523,x524,x525,x526,x521),f12(x523,x524,x525,x526,x522))
% 59.63/59.72 [53]~E(x531,x532)+E(f11(x531,x533,x534,x535,x536,x537),f11(x532,x533,x534,x535,x536,x537))
% 59.63/59.72 [54]~E(x541,x542)+E(f11(x543,x541,x544,x545,x546,x547),f11(x543,x542,x544,x545,x546,x547))
% 59.63/59.72 [55]~E(x551,x552)+E(f11(x553,x554,x551,x555,x556,x557),f11(x553,x554,x552,x555,x556,x557))
% 59.63/59.72 [56]~E(x561,x562)+E(f11(x563,x564,x565,x561,x566,x567),f11(x563,x564,x565,x562,x566,x567))
% 59.63/59.72 [57]~E(x571,x572)+E(f11(x573,x574,x575,x576,x571,x577),f11(x573,x574,x575,x576,x572,x577))
% 59.63/59.72 [58]~E(x581,x582)+E(f11(x583,x584,x585,x586,x587,x581),f11(x583,x584,x585,x586,x587,x582))
% 59.63/59.72 [59]~E(x591,x592)+E(f49(x591,x593,x594,x595,x596),f49(x592,x593,x594,x595,x596))
% 59.63/59.72 [60]~E(x601,x602)+E(f49(x603,x601,x604,x605,x606),f49(x603,x602,x604,x605,x606))
% 59.63/59.72 [61]~E(x611,x612)+E(f49(x613,x614,x611,x615,x616),f49(x613,x614,x612,x615,x616))
% 59.63/59.72 [62]~E(x621,x622)+E(f49(x623,x624,x625,x621,x626),f49(x623,x624,x625,x622,x626))
% 59.63/59.72 [63]~E(x631,x632)+E(f49(x633,x634,x635,x636,x631),f49(x633,x634,x635,x636,x632))
% 59.63/59.72 [64]~E(x641,x642)+E(f10(x641,x643,x644,x645,x646,x647),f10(x642,x643,x644,x645,x646,x647))
% 59.63/59.72 [65]~E(x651,x652)+E(f10(x653,x651,x654,x655,x656,x657),f10(x653,x652,x654,x655,x656,x657))
% 59.63/59.72 [66]~E(x661,x662)+E(f10(x663,x664,x661,x665,x666,x667),f10(x663,x664,x662,x665,x666,x667))
% 59.63/59.72 [67]~E(x671,x672)+E(f10(x673,x674,x675,x671,x676,x677),f10(x673,x674,x675,x672,x676,x677))
% 59.63/59.72 [68]~E(x681,x682)+E(f10(x683,x684,x685,x686,x681,x687),f10(x683,x684,x685,x686,x682,x687))
% 59.63/59.72 [69]~E(x691,x692)+E(f10(x693,x694,x695,x696,x697,x691),f10(x693,x694,x695,x696,x697,x692))
% 59.63/59.72 [70]~E(x701,x702)+E(f50(x701,x703,x704,x705,x706,x707),f50(x702,x703,x704,x705,x706,x707))
% 59.63/59.72 [71]~E(x711,x712)+E(f50(x713,x711,x714,x715,x716,x717),f50(x713,x712,x714,x715,x716,x717))
% 59.63/59.72 [72]~E(x721,x722)+E(f50(x723,x724,x721,x725,x726,x727),f50(x723,x724,x722,x725,x726,x727))
% 59.63/59.72 [73]~E(x731,x732)+E(f50(x733,x734,x735,x731,x736,x737),f50(x733,x734,x735,x732,x736,x737))
% 59.63/59.72 [74]~E(x741,x742)+E(f50(x743,x744,x745,x746,x741,x747),f50(x743,x744,x745,x746,x742,x747))
% 59.63/59.72 [75]~E(x751,x752)+E(f50(x753,x754,x755,x756,x757,x751),f50(x753,x754,x755,x756,x757,x752))
% 59.63/59.72 [76]~E(x761,x762)+E(f47(x761,x763,x764,x765,x766,x767),f47(x762,x763,x764,x765,x766,x767))
% 59.63/59.72 [77]~E(x771,x772)+E(f47(x773,x771,x774,x775,x776,x777),f47(x773,x772,x774,x775,x776,x777))
% 59.63/59.72 [78]~E(x781,x782)+E(f47(x783,x784,x781,x785,x786,x787),f47(x783,x784,x782,x785,x786,x787))
% 59.63/59.72 [79]~E(x791,x792)+E(f47(x793,x794,x795,x791,x796,x797),f47(x793,x794,x795,x792,x796,x797))
% 59.63/59.72 [80]~E(x801,x802)+E(f47(x803,x804,x805,x806,x801,x807),f47(x803,x804,x805,x806,x802,x807))
% 59.63/59.72 [81]~E(x811,x812)+E(f47(x813,x814,x815,x816,x817,x811),f47(x813,x814,x815,x816,x817,x812))
% 59.63/59.72 [82]~E(x821,x822)+E(f13(x821,x823,x824,x825,x826,x827),f13(x822,x823,x824,x825,x826,x827))
% 59.63/59.72 [83]~E(x831,x832)+E(f13(x833,x831,x834,x835,x836,x837),f13(x833,x832,x834,x835,x836,x837))
% 59.63/59.72 [84]~E(x841,x842)+E(f13(x843,x844,x841,x845,x846,x847),f13(x843,x844,x842,x845,x846,x847))
% 59.63/59.72 [85]~E(x851,x852)+E(f13(x853,x854,x855,x851,x856,x857),f13(x853,x854,x855,x852,x856,x857))
% 59.63/59.72 [86]~E(x861,x862)+E(f13(x863,x864,x865,x866,x861,x867),f13(x863,x864,x865,x866,x862,x867))
% 59.63/59.72 [87]~E(x871,x872)+E(f13(x873,x874,x875,x876,x877,x871),f13(x873,x874,x875,x876,x877,x872))
% 59.63/59.72 [88]P1(x882,x883,x884)+~E(x881,x882)+~P1(x881,x883,x884)
% 59.63/59.72 [89]P1(x893,x892,x894)+~E(x891,x892)+~P1(x893,x891,x894)
% 59.63/59.72 [90]P1(x903,x904,x902)+~E(x901,x902)+~P1(x903,x904,x901)
% 59.63/59.72 [91]P7(x912,x913,x914,x915,x916,x917,x918,x919)+~E(x911,x912)+~P7(x911,x913,x914,x915,x916,x917,x918,x919)
% 59.63/59.72 [92]P7(x923,x922,x924,x925,x926,x927,x928,x929)+~E(x921,x922)+~P7(x923,x921,x924,x925,x926,x927,x928,x929)
% 59.63/59.72 [93]P7(x933,x934,x932,x935,x936,x937,x938,x939)+~E(x931,x932)+~P7(x933,x934,x931,x935,x936,x937,x938,x939)
% 59.63/59.72 [94]P7(x943,x944,x945,x942,x946,x947,x948,x949)+~E(x941,x942)+~P7(x943,x944,x945,x941,x946,x947,x948,x949)
% 59.63/59.72 [95]P7(x953,x954,x955,x956,x952,x957,x958,x959)+~E(x951,x952)+~P7(x953,x954,x955,x956,x951,x957,x958,x959)
% 59.63/59.72 [96]P7(x963,x964,x965,x966,x967,x962,x968,x969)+~E(x961,x962)+~P7(x963,x964,x965,x966,x967,x961,x968,x969)
% 59.63/59.72 [97]P7(x973,x974,x975,x976,x977,x978,x972,x979)+~E(x971,x972)+~P7(x973,x974,x975,x976,x977,x978,x971,x979)
% 59.63/59.72 [98]P7(x983,x984,x985,x986,x987,x988,x989,x982)+~E(x981,x982)+~P7(x983,x984,x985,x986,x987,x988,x989,x981)
% 59.63/59.72 [99]P10(x992,x993,x994,x995)+~E(x991,x992)+~P10(x991,x993,x994,x995)
% 59.63/59.72 [100]P10(x1003,x1002,x1004,x1005)+~E(x1001,x1002)+~P10(x1003,x1001,x1004,x1005)
% 59.63/59.72 [101]P10(x1013,x1014,x1012,x1015)+~E(x1011,x1012)+~P10(x1013,x1014,x1011,x1015)
% 59.63/59.72 [102]P10(x1023,x1024,x1025,x1022)+~E(x1021,x1022)+~P10(x1023,x1024,x1025,x1021)
% 59.63/59.72 [103]P8(x1032,x1033,x1034,x1035,x1036,x1037,x1038,x1039)+~E(x1031,x1032)+~P8(x1031,x1033,x1034,x1035,x1036,x1037,x1038,x1039)
% 59.63/59.72 [104]P8(x1043,x1042,x1044,x1045,x1046,x1047,x1048,x1049)+~E(x1041,x1042)+~P8(x1043,x1041,x1044,x1045,x1046,x1047,x1048,x1049)
% 59.63/59.72 [105]P8(x1053,x1054,x1052,x1055,x1056,x1057,x1058,x1059)+~E(x1051,x1052)+~P8(x1053,x1054,x1051,x1055,x1056,x1057,x1058,x1059)
% 59.63/59.72 [106]P8(x1063,x1064,x1065,x1062,x1066,x1067,x1068,x1069)+~E(x1061,x1062)+~P8(x1063,x1064,x1065,x1061,x1066,x1067,x1068,x1069)
% 59.63/59.73 [107]P8(x1073,x1074,x1075,x1076,x1072,x1077,x1078,x1079)+~E(x1071,x1072)+~P8(x1073,x1074,x1075,x1076,x1071,x1077,x1078,x1079)
% 59.63/59.73 [108]P8(x1083,x1084,x1085,x1086,x1087,x1082,x1088,x1089)+~E(x1081,x1082)+~P8(x1083,x1084,x1085,x1086,x1087,x1081,x1088,x1089)
% 59.63/59.73 [109]P8(x1093,x1094,x1095,x1096,x1097,x1098,x1092,x1099)+~E(x1091,x1092)+~P8(x1093,x1094,x1095,x1096,x1097,x1098,x1091,x1099)
% 59.63/59.73 [110]P8(x1103,x1104,x1105,x1106,x1107,x1108,x1109,x1102)+~E(x1101,x1102)+~P8(x1103,x1104,x1105,x1106,x1107,x1108,x1109,x1101)
% 59.63/59.73 [111]P11(x1112,x1113,x1114,x1115,x1116,x1117)+~E(x1111,x1112)+~P11(x1111,x1113,x1114,x1115,x1116,x1117)
% 59.63/59.73 [112]P11(x1123,x1122,x1124,x1125,x1126,x1127)+~E(x1121,x1122)+~P11(x1123,x1121,x1124,x1125,x1126,x1127)
% 59.63/59.73 [113]P11(x1133,x1134,x1132,x1135,x1136,x1137)+~E(x1131,x1132)+~P11(x1133,x1134,x1131,x1135,x1136,x1137)
% 59.63/59.73 [114]P11(x1143,x1144,x1145,x1142,x1146,x1147)+~E(x1141,x1142)+~P11(x1143,x1144,x1145,x1141,x1146,x1147)
% 59.63/59.73 [115]P11(x1153,x1154,x1155,x1156,x1152,x1157)+~E(x1151,x1152)+~P11(x1153,x1154,x1155,x1156,x1151,x1157)
% 59.63/59.73 [116]P11(x1163,x1164,x1165,x1166,x1167,x1162)+~E(x1161,x1162)+~P11(x1163,x1164,x1165,x1166,x1167,x1161)
% 59.63/59.73 [117]P4(x1172,x1173,x1174,x1175)+~E(x1171,x1172)+~P4(x1171,x1173,x1174,x1175)
% 59.63/59.73 [118]P4(x1183,x1182,x1184,x1185)+~E(x1181,x1182)+~P4(x1183,x1181,x1184,x1185)
% 59.63/59.73 [119]P4(x1193,x1194,x1192,x1195)+~E(x1191,x1192)+~P4(x1193,x1194,x1191,x1195)
% 59.63/59.73 [120]P4(x1203,x1204,x1205,x1202)+~E(x1201,x1202)+~P4(x1203,x1204,x1205,x1201)
% 59.63/59.73 [121]P5(x1212,x1213,x1214,x1215,x1216,x1217)+~E(x1211,x1212)+~P5(x1211,x1213,x1214,x1215,x1216,x1217)
% 59.63/59.73 [122]P5(x1223,x1222,x1224,x1225,x1226,x1227)+~E(x1221,x1222)+~P5(x1223,x1221,x1224,x1225,x1226,x1227)
% 59.63/59.73 [123]P5(x1233,x1234,x1232,x1235,x1236,x1237)+~E(x1231,x1232)+~P5(x1233,x1234,x1231,x1235,x1236,x1237)
% 59.63/59.73 [124]P5(x1243,x1244,x1245,x1242,x1246,x1247)+~E(x1241,x1242)+~P5(x1243,x1244,x1245,x1241,x1246,x1247)
% 59.63/59.73 [125]P5(x1253,x1254,x1255,x1256,x1252,x1257)+~E(x1251,x1252)+~P5(x1253,x1254,x1255,x1256,x1251,x1257)
% 59.63/59.73 [126]P5(x1263,x1264,x1265,x1266,x1267,x1262)+~E(x1261,x1262)+~P5(x1263,x1264,x1265,x1266,x1267,x1261)
% 59.63/59.73 [127]P2(x1272,x1273,x1274,x1275)+~E(x1271,x1272)+~P2(x1271,x1273,x1274,x1275)
% 59.63/59.73 [128]P2(x1283,x1282,x1284,x1285)+~E(x1281,x1282)+~P2(x1283,x1281,x1284,x1285)
% 59.63/59.73 [129]P2(x1293,x1294,x1292,x1295)+~E(x1291,x1292)+~P2(x1293,x1294,x1291,x1295)
% 59.63/59.73 [130]P2(x1303,x1304,x1305,x1302)+~E(x1301,x1302)+~P2(x1303,x1304,x1305,x1301)
% 59.63/59.73 [131]P6(x1312,x1313,x1314)+~E(x1311,x1312)+~P6(x1311,x1313,x1314)
% 59.63/59.73 [132]P6(x1323,x1322,x1324)+~E(x1321,x1322)+~P6(x1323,x1321,x1324)
% 59.63/59.73 [133]P6(x1333,x1334,x1332)+~E(x1331,x1332)+~P6(x1333,x1334,x1331)
% 59.63/59.73 [134]P9(x1342,x1343,x1344,x1345)+~E(x1341,x1342)+~P9(x1341,x1343,x1344,x1345)
% 59.63/59.73 [135]P9(x1353,x1352,x1354,x1355)+~E(x1351,x1352)+~P9(x1353,x1351,x1354,x1355)
% 59.63/59.73 [136]P9(x1363,x1364,x1362,x1365)+~E(x1361,x1362)+~P9(x1363,x1364,x1361,x1365)
% 59.63/59.73 [137]P9(x1373,x1374,x1375,x1372)+~E(x1371,x1372)+~P9(x1373,x1374,x1375,x1371)
% 59.63/59.73 [138]P3(x1382,x1383,x1384,x1385)+~E(x1381,x1382)+~P3(x1381,x1383,x1384,x1385)
% 59.63/59.73 [139]P3(x1393,x1392,x1394,x1395)+~E(x1391,x1392)+~P3(x1393,x1391,x1394,x1395)
% 59.63/59.73 [140]P3(x1403,x1404,x1402,x1405)+~E(x1401,x1402)+~P3(x1403,x1404,x1401,x1405)
% 59.63/59.73 [141]P3(x1413,x1414,x1415,x1412)+~E(x1411,x1412)+~P3(x1413,x1414,x1415,x1411)
% 59.63/59.73
% 59.63/59.73 %-------------------------------------------
% 59.63/59.73 cnf(281,plain,
% 59.63/59.73 (~P3(a32,a31,a33,a34)),
% 59.63/59.73 inference(scs_inference,[],[167,186])).
% 59.63/59.73 cnf(283,plain,
% 59.63/59.73 (~P3(a31,a33,a32,a34)),
% 59.63/59.73 inference(scs_inference,[],[167,186,187])).
% 59.63/59.73 cnf(285,plain,
% 59.63/59.73 (~P3(a31,a32,a34,a33)),
% 59.63/59.73 inference(scs_inference,[],[167,186,187,188])).
% 59.63/59.73 cnf(287,plain,
% 59.63/59.73 (P1(a15,a15,a1)),
% 59.63/59.73 inference(scs_inference,[],[142,167,186,187,188,172])).
% 59.63/59.73 cnf(301,plain,
% 59.63/59.73 (~P3(a33,a31,a32,a34)),
% 59.63/59.73 inference(scs_inference,[],[283,186])).
% 59.63/59.73 cnf(303,plain,
% 59.63/59.73 (~P3(a32,a33,a31,a34)),
% 59.63/59.73 inference(scs_inference,[],[281,283,186,187])).
% 59.63/59.73 cnf(305,plain,
% 59.63/59.73 (~P3(a32,a31,a34,a33)),
% 59.63/59.73 inference(scs_inference,[],[281,283,186,187,188])).
% 59.63/59.73 cnf(309,plain,
% 59.63/59.73 (P2(x3091,a16,a25,a30)+~E(a24,x3091)),
% 59.63/59.73 inference(scs_inference,[],[143,153,281,283,186,187,188,172,127])).
% 59.63/59.73 cnf(321,plain,
% 59.63/59.73 (~P3(a33,a32,a31,a34)),
% 59.63/59.73 inference(scs_inference,[],[303,186])).
% 59.63/59.73 cnf(323,plain,
% 59.63/59.73 (~P3(a31,a34,a32,a33)),
% 59.63/59.73 inference(scs_inference,[],[285,303,186,187])).
% 59.63/59.73 cnf(325,plain,
% 59.63/59.73 (~P3(a33,a31,a34,a32)),
% 59.63/59.73 inference(scs_inference,[],[285,301,303,186,187,188])).
% 59.63/59.73 cnf(341,plain,
% 59.63/59.73 (~P3(a34,a31,a32,a33)),
% 59.63/59.73 inference(scs_inference,[],[323,186])).
% 59.63/59.73 cnf(343,plain,
% 59.63/59.73 (~P3(a32,a34,a31,a33)),
% 59.63/59.73 inference(scs_inference,[],[305,323,186,187])).
% 59.63/59.73 cnf(345,plain,
% 59.63/59.73 (~P3(a33,a32,a34,a31)),
% 59.63/59.73 inference(scs_inference,[],[305,321,323,186,187,188])).
% 59.63/59.73 cnf(363,plain,
% 59.63/59.73 (~P3(a33,a34,a31,a32)),
% 59.63/59.73 inference(scs_inference,[],[325,186,187])).
% 59.63/59.73 cnf(365,plain,
% 59.63/59.73 (~P3(a34,a31,a33,a32)),
% 59.63/59.73 inference(scs_inference,[],[325,341,186,187,188])).
% 59.63/59.73 cnf(383,plain,
% 59.63/59.73 (~P3(a33,a34,a32,a31)),
% 59.63/59.73 inference(scs_inference,[],[343,345,186,187])).
% 59.63/59.73 cnf(385,plain,
% 59.63/59.73 (~P3(a32,a34,a33,a31)),
% 59.63/59.73 inference(scs_inference,[],[343,345,186,187,188])).
% 59.63/59.73 cnf(401,plain,
% 59.63/59.73 (~P3(a34,a33,a31,a32)),
% 59.63/59.73 inference(scs_inference,[],[363,186])).
% 59.63/59.73 cnf(421,plain,
% 59.63/59.73 (~P3(a34,a33,a32,a31)),
% 59.63/59.73 inference(scs_inference,[],[383,186])).
% 59.63/59.73 cnf(423,plain,
% 59.63/59.73 (~P3(a32,a33,a34,a31)),
% 59.63/59.73 inference(scs_inference,[],[383,385,186,187])).
% 59.63/59.73 cnf(425,plain,
% 59.63/59.73 (P1(a16,a16,a21)),
% 59.63/59.73 inference(scs_inference,[],[149,383,385,186,187,172])).
% 59.63/59.73 cnf(454,plain,
% 59.63/59.73 (P1(a16,a16,a22)),
% 59.63/59.73 inference(scs_inference,[],[151,172])).
% 59.63/59.73 cnf(473,plain,
% 59.63/59.73 (~P3(a34,a18,a18,a43)+P10(a28,a18,a18,a18)),
% 59.63/59.73 inference(scs_inference,[],[162,287,172,259,241,186])).
% 59.63/59.73 cnf(954,plain,
% 59.63/59.73 (P10(x9541,x9542,x9543,x9544)+~P10(x9544,x9543,x9541,x9542)),
% 59.63/59.73 inference(scs_inference,[],[182,183])).
% 59.63/59.73 cnf(959,plain,
% 59.63/59.73 (P10(a18,a18,a28,a18)+~P3(a34,a18,a18,a43)),
% 59.63/59.73 inference(scs_inference,[],[473,182])).
% 59.63/59.73 cnf(966,plain,
% 59.63/59.73 (P10(a18,a18,a18,a28)+~P3(a34,a18,a18,a43)),
% 59.63/59.73 inference(scs_inference,[],[959,183])).
% 59.63/59.73 cnf(974,plain,
% 59.63/59.73 (P10(a18,a28,a18,a18)+~P3(a34,a18,a18,a43)),
% 59.63/59.73 inference(scs_inference,[],[966,954])).
% 59.63/59.73 cnf(1427,plain,
% 59.63/59.73 (P10(f7(a16,a25,a30,x14271),a16,a16,x14271)+~E(a24,x14271)),
% 59.63/59.73 inference(scs_inference,[],[204,309])).
% 59.63/59.73 cnf(1428,plain,
% 59.63/59.73 (P10(f7(a16,a25,a30,a24),a16,a16,a24)),
% 59.63/59.73 inference(equality_inference,[],[1427])).
% 59.63/59.73 cnf(1429,plain,
% 59.63/59.73 (P10(a16,a24,a16,f7(a16,a25,a30,a24))),
% 59.63/59.73 inference(scs_inference,[],[1428,954])).
% 59.63/59.73 cnf(1431,plain,
% 59.63/59.73 (P9(f7(a16,a25,a30,a24),a16,a16,f7(a16,a25,a30,a24))),
% 59.63/59.73 inference(scs_inference,[],[1428,954,197])).
% 59.63/59.73 cnf(1439,plain,
% 59.63/59.73 (P10(a16,f7(a16,a25,a30,a24),a24,a16)),
% 59.63/59.73 inference(scs_inference,[],[1429,954])).
% 59.63/59.73 cnf(1441,plain,
% 59.63/59.73 (P10(f7(a16,a25,a30,a24),a16,a24,a16)),
% 59.63/59.73 inference(scs_inference,[],[1431,1429,954,199])).
% 59.63/59.73 cnf(1443,plain,
% 59.63/59.73 (P9(a16,a24,a24,a16)),
% 59.63/59.73 inference(scs_inference,[],[1431,1429,954,199,197])).
% 59.63/59.73 cnf(1450,plain,
% 59.63/59.73 (P10(a24,a16,f7(a16,a25,a30,a24),a16)),
% 59.63/59.73 inference(scs_inference,[],[1439,954])).
% 59.63/59.73 cnf(1454,plain,
% 59.63/59.73 (P9(a24,a16,a16,a24)),
% 59.63/59.73 inference(scs_inference,[],[1428,1439,1443,954,199,197])).
% 59.63/59.73 cnf(1456,plain,
% 59.63/59.73 (P9(a24,a16,a24,a16)),
% 59.63/59.73 inference(scs_inference,[],[1428,1439,1443,954,199,197,196])).
% 59.63/59.73 cnf(1462,plain,
% 59.63/59.73 (P10(a24,a16,a16,f7(a16,a25,a30,a24))),
% 59.63/59.73 inference(scs_inference,[],[1441,954])).
% 59.63/59.73 cnf(1468,plain,
% 59.63/59.73 (~P8(x14681,x14682,x14683,x14684,a16,f7(a16,a25,a30,a24),a16,a25)+P8(x14681,x14682,x14683,x14684,a30,a16,a30,a25)),
% 59.63/59.73 inference(scs_inference,[],[153,1441,1450,954,246,197,279])).
% 59.63/59.73 cnf(1473,plain,
% 59.63/59.73 (P10(a16,f7(a16,a25,a30,a24),a16,a24)),
% 59.63/59.73 inference(scs_inference,[],[1462,954])).
% 59.63/59.73 cnf(1475,plain,
% 59.63/59.73 (P9(a16,a24,a16,a24)),
% 59.63/59.73 inference(scs_inference,[],[1443,1454,1462,954,196])).
% 59.63/59.73 cnf(1511,plain,
% 59.63/59.73 (P9(a16,f7(a16,a25,a30,a24),f7(a16,a25,a30,a24),a16)),
% 59.63/59.73 inference(scs_inference,[],[1450,1439,197])).
% 59.63/59.73 cnf(1688,plain,
% 59.63/59.73 (~P6(x16881,a24,a24)+P6(x16881,a16,a16)),
% 59.63/59.73 inference(scs_inference,[],[1456,192])).
% 59.63/59.73 cnf(1694,plain,
% 59.63/59.73 (~P6(x16941,a16,a16)+P6(x16941,a24,a24)),
% 59.63/59.73 inference(scs_inference,[],[1475,192])).
% 59.63/59.73 cnf(1705,plain,
% 59.63/59.73 (P4(x17051,a24,x17051,a24)+~P6(x17051,a16,a16)),
% 59.63/59.73 inference(scs_inference,[],[1694,173])).
% 59.63/59.73 cnf(1721,plain,
% 59.63/59.73 (P4(x17211,a24,a24,x17211)+~P6(x17211,a16,a16)),
% 59.63/59.73 inference(scs_inference,[],[1705,185])).
% 59.63/59.73 cnf(1732,plain,
% 59.63/59.73 (~P8(x17321,x17322,x17323,x17324,a16,f7(a16,a25,a30,a24),a16,a1)+P8(x17321,x17322,x17323,x17324,a22,a16,a22,a1)),
% 59.63/59.73 inference(scs_inference,[],[152,1462,246,279])).
% 59.63/59.73 cnf(1765,plain,
% 59.63/59.73 (P4(a24,x17651,x17651,a24)+~P6(x17651,a16,a16)),
% 59.63/59.73 inference(scs_inference,[],[1721,184])).
% 59.63/59.73 cnf(1780,plain,
% 59.63/59.73 (P8(a16,f7(a16,a25,a30,a24),a16,a31,a36,a16,a36,a31)),
% 59.63/59.73 inference(scs_inference,[],[154,1462,246])).
% 59.63/59.73 cnf(1782,plain,
% 59.63/59.73 (~P8(x17821,x17822,x17823,x17824,a16,f7(a16,a25,a30,a24),a16,a31)+P8(x17821,x17822,x17823,x17824,a36,a16,a36,a31)),
% 59.63/59.73 inference(scs_inference,[],[154,1462,246,279])).
% 59.63/59.73 cnf(1815,plain,
% 59.63/59.73 (P8(a24,a24,a24,a24,a24,a24,a24,a24)+~P6(a24,a16,a16)),
% 59.63/59.73 inference(scs_inference,[],[1765,243])).
% 59.63/59.73 cnf(1837,plain,
% 59.63/59.73 (P9(a24,a24,a24,a24)+~P6(a24,a16,a16)),
% 59.63/59.73 inference(scs_inference,[],[1815,250])).
% 59.63/59.73 cnf(1853,plain,
% 59.63/59.73 (P8(a24,a24,x18531,x18532,a24,a24,x18531,x18532)+~P6(a24,a16,a16)),
% 59.63/59.73 inference(scs_inference,[],[1837,242])).
% 59.63/59.73 cnf(1869,plain,
% 59.63/59.73 (P8(a24,a24,a24,a24,x18691,x18692,x18691,x18692)+~P6(a24,a16,a16)),
% 59.63/59.73 inference(scs_inference,[],[1853,272])).
% 59.63/59.73 cnf(1885,plain,
% 59.63/59.73 (P8(x18851,x18852,x18851,x18852,a24,a24,a24,a24)+~P6(a24,a16,a16)),
% 59.63/59.73 inference(scs_inference,[],[1869,269])).
% 59.63/59.73 cnf(1901,plain,
% 59.63/59.73 (P8(x19011,x19012,x19012,x19011,a24,a24,a24,a24)+~P6(a24,a16,a16)),
% 59.63/59.73 inference(scs_inference,[],[1885,271])).
% 59.63/59.73 cnf(3828,plain,
% 59.63/59.73 (P1(a2,a1,a15)),
% 59.63/59.73 inference(scs_inference,[],[142,168])).
% 59.63/59.73 cnf(3830,plain,
% 59.63/59.73 (P1(a1,a15,a2)),
% 59.63/59.73 inference(scs_inference,[],[142,168,169])).
% 59.63/59.73 cnf(3832,plain,
% 59.63/59.73 (P1(a16,a24,a24)),
% 59.63/59.73 inference(scs_inference,[],[142,1475,168,169,177])).
% 59.63/59.73 cnf(3834,plain,
% 59.63/59.73 (P8(a16,a24,x38341,x38342,a16,a24,x38341,x38342)),
% 59.63/59.73 inference(scs_inference,[],[142,1475,168,169,177,242])).
% 59.63/59.73 cnf(3846,plain,
% 59.63/59.73 (P1(f4(a16,a16,a24),a24,a16)),
% 59.63/59.73 inference(scs_inference,[],[142,1475,160,1780,1473,168,169,177,242,204,271,270,272,269,194])).
% 59.63/59.73 cnf(3848,plain,
% 59.63/59.73 (P1(f5(a16,a16,a24),a24,a16)),
% 59.63/59.73 inference(scs_inference,[],[142,1475,160,1780,1473,168,169,177,242,204,271,270,272,269,194,195])).
% 59.63/59.73 cnf(3850,plain,
% 59.63/59.73 (P10(a16,f4(a16,a16,a24),a24,a16)),
% 59.63/59.73 inference(scs_inference,[],[142,1475,160,1780,1473,168,169,177,242,204,271,270,272,269,194,195,206])).
% 59.63/59.73 cnf(3852,plain,
% 59.63/59.73 (P10(a16,f5(a16,a16,a24),a24,a16)),
% 59.63/59.73 inference(scs_inference,[],[142,1475,160,1780,1473,168,169,177,242,204,271,270,272,269,194,195,206,207])).
% 59.63/59.73 cnf(3856,plain,
% 59.63/59.73 (P9(a16,f4(a16,a16,a24),a16,f7(a16,a25,a30,a24))),
% 59.63/59.73 inference(scs_inference,[],[142,1475,160,1462,1780,1473,168,169,177,242,204,271,270,272,269,194,195,206,207,279,197])).
% 59.63/59.73 cnf(3858,plain,
% 59.63/59.73 (P9(a16,f4(a16,a16,a24),f7(a16,a25,a30,a24),a16)),
% 59.63/59.73 inference(scs_inference,[],[142,1475,160,1462,1780,1511,1473,168,169,177,242,204,271,270,272,269,194,195,206,207,279,197,196])).
% 59.63/59.73 cnf(3860,plain,
% 59.63/59.73 (P3(a24,a21,a16,a16)),
% 59.63/59.73 inference(scs_inference,[],[142,425,1475,160,1462,1780,1511,1473,168,169,177,242,204,271,270,272,269,194,195,206,207,279,197,196,253])).
% 59.63/59.73 cnf(3862,plain,
% 59.63/59.73 (P9(a16,f7(a16,a25,a30,a24),a16,f4(a16,a16,a24))),
% 59.63/59.73 inference(scs_inference,[],[142,425,1475,160,1462,1780,1511,1473,168,169,177,242,204,271,270,272,269,194,195,206,207,279,197,196,253,180])).
% 59.63/59.73 cnf(3864,plain,
% 59.63/59.73 (P9(a16,f7(a16,a25,a30,a24),f4(a16,a16,a24),a16)),
% 59.63/59.73 inference(scs_inference,[],[142,425,1475,160,1462,1780,1511,1473,168,169,177,242,204,271,270,272,269,194,195,206,207,279,197,196,253,180,181])).
% 59.63/59.73 cnf(3866,plain,
% 59.63/59.73 (P10(a21,a27,f7(a21,a20,a17,a27),a21)),
% 59.63/59.73 inference(scs_inference,[],[142,425,1475,160,1462,1780,1511,1473,168,169,177,242,204,271,270,272,269,194,195,206,207,279,197,196,253,180,181,182])).
% 59.63/59.73 cnf(3868,plain,
% 59.63/59.73 (P10(f7(a21,a20,a17,a27),a21,a27,a21)),
% 59.63/59.73 inference(scs_inference,[],[142,425,1475,160,1462,1780,1511,1473,168,169,177,242,204,271,270,272,269,194,195,206,207,279,197,196,253,180,181,182,183])).
% 59.63/59.73 cnf(3870,plain,
% 59.63/59.73 (P8(a36,a16,a36,a31,a36,a16,a36,a31)),
% 59.63/59.73 inference(scs_inference,[],[142,425,1475,160,1462,1780,1511,1473,168,169,177,242,204,271,270,272,269,194,195,206,207,279,197,196,253,180,181,182,183,1782])).
% 59.63/59.73 cnf(3872,plain,
% 59.63/59.73 (P3(a24,a16,a21,a16)),
% 59.63/59.73 inference(scs_inference,[],[142,425,1475,160,1462,1780,1511,1473,168,169,177,242,204,271,270,272,269,194,195,206,207,279,197,196,253,180,181,182,183,1782,187])).
% 59.63/59.73 cnf(3874,plain,
% 59.63/59.73 (P8(a21,a24,a21,a16,a16,a24,a16,a16)),
% 59.63/59.73 inference(scs_inference,[],[142,425,1475,160,1462,1780,1511,1473,168,169,177,242,204,271,270,272,269,194,195,206,207,279,197,196,253,180,181,182,183,1782,187,241])).
% 59.63/59.73 cnf(3876,plain,
% 59.63/59.73 (P3(a21,a24,a16,a16)),
% 59.63/59.73 inference(scs_inference,[],[142,425,1475,160,1462,1780,1511,1473,168,169,177,242,204,271,270,272,269,194,195,206,207,279,197,196,253,180,181,182,183,1782,187,241,186])).
% 59.63/59.73 cnf(3918,plain,
% 59.63/59.73 (P9(f7(a16,a25,a30,a24),a16,f4(a16,a16,a24),a16)),
% 59.63/59.73 inference(scs_inference,[],[3858,3856,3866,3846,180,169,183,177,181])).
% 59.63/59.73 cnf(3922,plain,
% 59.63/59.73 (P9(a36,a16,a36,a16)),
% 59.63/59.73 inference(scs_inference,[],[3870,3858,3856,3866,3846,165,180,169,183,177,181,204,250])).
% 59.63/59.73 cnf(3928,plain,
% 59.63/59.73 (P1(a15,a1,a2)),
% 59.63/59.73 inference(scs_inference,[],[3830,3870,3858,3856,3868,3866,3846,165,180,169,183,177,181,204,250,182,242,168])).
% 59.63/59.73 cnf(3930,plain,
% 59.63/59.73 (P3(a21,a16,a24,a16)),
% 59.63/59.73 inference(scs_inference,[],[3830,3870,3876,3858,3856,3868,3866,3846,165,180,169,183,177,181,204,250,182,242,168,187])).
% 59.63/59.73 cnf(3932,plain,
% 59.63/59.73 (P8(a24,a16,x39321,x39322,a16,a24,x39321,x39322)),
% 59.63/59.73 inference(scs_inference,[],[3834,3830,3870,3876,3858,3856,3868,3866,3846,165,180,169,183,177,181,204,250,182,242,168,187,271])).
% 59.63/59.73 cnf(3936,plain,
% 59.63/59.73 (P3(a24,a16,a16,a21)),
% 59.63/59.73 inference(scs_inference,[],[3834,3830,3870,3872,3876,3858,3856,3868,3866,3846,165,180,169,183,177,181,204,250,182,242,168,187,271,241,188])).
% 59.63/59.73 cnf(3938,plain,
% 59.63/59.73 (P8(a16,a24,a16,a24,x39381,x39382,x39381,x39382)),
% 59.63/59.73 inference(scs_inference,[],[3834,3830,3870,3872,3876,3858,3856,3868,3866,3846,165,180,169,183,177,181,204,250,182,242,168,187,271,241,188,272])).
% 59.63/59.73 cnf(3940,plain,
% 59.63/59.73 (P8(x39401,x39402,a16,a24,x39401,x39402,a16,a24)),
% 59.63/59.73 inference(scs_inference,[],[3834,3830,3870,3872,3876,3858,3856,3868,3866,3846,165,180,169,183,177,181,204,250,182,242,168,187,271,241,188,272,270])).
% 59.63/59.73 cnf(3942,plain,
% 59.63/59.73 (P8(a16,a24,a16,a16,a21,a24,a21,a16)),
% 59.63/59.73 inference(scs_inference,[],[3834,3830,3870,3872,3874,3876,3858,3856,3868,3866,3846,165,180,169,183,177,181,204,250,182,242,168,187,271,241,188,272,270,269])).
% 59.63/59.73 cnf(3944,plain,
% 59.63/59.73 (P3(a16,a24,a21,a16)),
% 59.63/59.73 inference(scs_inference,[],[3834,3830,3870,3872,3874,3876,3858,3856,3868,3866,3846,165,180,169,183,177,181,204,250,182,242,168,187,271,241,188,272,270,269,186])).
% 59.63/59.73 cnf(3946,plain,
% 59.63/59.73 (P3(a21,a16,a16,a16)),
% 59.63/59.73 inference(scs_inference,[],[3834,3830,3860,3870,3872,3874,3876,3858,3856,3868,3866,3846,165,180,169,183,177,181,204,250,182,242,168,187,271,241,188,272,270,269,186,202])).
% 59.63/59.73 cnf(3950,plain,
% 59.63/59.73 (P1(a15,a15,a2)),
% 59.63/59.73 inference(scs_inference,[],[3828,3834,3830,3860,3870,3872,3874,3876,3858,3856,3868,3866,3846,165,180,169,183,177,181,204,250,182,242,168,187,271,241,188,272,270,269,186,202,257,172])).
% 59.63/59.73 cnf(3954,plain,
% 59.63/59.73 (P3(a24,a24,a16,a24)),
% 59.63/59.73 inference(scs_inference,[],[3828,3834,3830,3832,3860,3870,3872,3874,3876,3858,3856,3868,3866,3846,165,1428,180,169,183,177,181,204,250,182,242,168,187,271,241,188,272,270,269,186,202,257,172,199,253])).
% 59.63/59.73 cnf(3956,plain,
% 59.63/59.73 (P4(a24,a24,a24,a24)),
% 59.63/59.73 inference(scs_inference,[],[3828,3834,3830,3832,3860,3870,3872,3874,3876,3858,3856,3868,3866,3846,165,1428,180,169,183,177,181,204,250,182,242,168,187,271,241,188,272,270,269,186,202,257,172,199,253,268])).
% 59.63/59.73 cnf(3958,plain,
% 59.63/59.73 (P8(a24,a24,a24,a24,a24,a24,a24,a24)),
% 59.63/59.73 inference(scs_inference,[],[3828,3834,3830,3832,3860,3870,3872,3874,3876,3858,3856,3868,3866,3846,165,1428,180,169,183,177,181,204,250,182,242,168,187,271,241,188,272,270,269,186,202,257,172,199,253,268,243])).
% 59.63/59.73 cnf(3962,plain,
% 59.63/59.73 (P10(a24,a24,a24,a24)),
% 59.63/59.73 inference(scs_inference,[],[3828,3834,3830,3832,3860,3870,3872,3874,3876,3858,3856,3868,3866,3846,165,1428,180,169,183,177,181,204,250,182,242,168,187,271,241,188,272,270,269,186,202,257,172,199,253,268,243,189,198])).
% 59.63/59.73 cnf(3964,plain,
% 59.63/59.73 (P2(a24,a24,a24,a24)),
% 59.63/59.73 inference(scs_inference,[],[3828,3834,3830,3832,3860,3870,3872,3874,3876,3858,3856,3868,3866,3846,165,1428,180,169,183,177,181,204,250,182,242,168,187,271,241,188,272,270,269,186,202,257,172,199,253,268,243,189,198,201])).
% 59.63/59.73 cnf(3966,plain,
% 59.63/59.73 (P1(a24,a24,f3(a24,a24,a24))),
% 59.63/59.73 inference(scs_inference,[],[3828,3834,3830,3832,3860,3870,3872,3874,3876,3858,3856,3868,3866,3846,165,1428,180,169,183,177,181,204,250,182,242,168,187,271,241,188,272,270,269,186,202,257,172,199,253,268,243,189,198,201,193])).
% 59.63/59.73 cnf(3968,plain,
% 59.63/59.73 (P4(a24,a24,a24,f3(a24,a24,a24))),
% 59.63/59.73 inference(scs_inference,[],[3828,3834,3830,3832,3860,3870,3872,3874,3876,3858,3856,3868,3866,3846,165,1428,180,169,183,177,181,204,250,182,242,168,187,271,241,188,272,270,269,186,202,257,172,199,253,268,243,189,198,201,193,205])).
% 59.63/59.73 cnf(3974,plain,
% 59.63/59.73 (P10(a16,a24,a16,a24)),
% 59.63/59.73 inference(scs_inference,[],[3828,3834,3830,3832,3860,3870,3872,3874,3876,3858,3856,3868,3866,3846,165,1428,180,169,183,177,181,204,250,182,242,168,187,271,241,188,272,270,269,186,202,257,172,199,253,268,243,189,198,201,193,205,210,211,258])).
% 59.63/59.73 cnf(3980,plain,
% 59.63/59.73 (P1(f14(a24,a24,a24,a24),a24,a24)),
% 59.63/59.73 inference(scs_inference,[],[3828,3834,3830,3832,3860,3870,3872,3874,3876,3858,3856,3868,3866,3846,165,1428,180,169,183,177,181,204,250,182,242,168,187,271,241,188,272,270,269,186,202,257,172,199,253,268,243,189,198,201,193,205,210,211,258,262,263,264])).
% 59.63/59.73 cnf(3994,plain,
% 59.63/59.73 (P3(a24,a24,a24,a24)),
% 59.63/59.73 inference(scs_inference,[],[3828,3834,3830,3832,3860,3870,3872,3874,3876,3858,3856,3868,3866,3846,165,1428,180,169,183,177,181,204,250,182,242,168,187,271,241,188,272,270,269,186,202,257,172,199,253,268,243,189,198,201,193,205,210,211,258,262,263,264,266,267,195,194,206,207,213])).
% 59.63/59.73 cnf(3996,plain,
% 59.63/59.73 (P4(a24,f3(a24,a24,a24),a24,a24)),
% 59.63/59.73 inference(scs_inference,[],[3828,3834,3830,3832,3860,3870,3872,3874,3876,3858,3856,3868,3866,3846,165,1428,180,169,183,177,181,204,250,182,242,168,187,271,241,188,272,270,269,186,202,257,172,199,253,268,243,189,198,201,193,205,210,211,258,262,263,264,266,267,195,194,206,207,213,184])).
% 59.63/59.73 cnf(3998,plain,
% 59.63/59.73 (P4(a24,a24,f3(a24,a24,a24),a24)),
% 59.63/59.73 inference(scs_inference,[],[3828,3834,3830,3832,3860,3870,3872,3874,3876,3858,3856,3868,3866,3846,165,1428,180,169,183,177,181,204,250,182,242,168,187,271,241,188,272,270,269,186,202,257,172,199,253,268,243,189,198,201,193,205,210,211,258,262,263,264,266,267,195,194,206,207,213,184,185])).
% 59.63/59.73 cnf(4004,plain,
% 59.63/59.73 (P4(f3(a24,a24,a24),a24,a24,a24)),
% 59.63/59.73 inference(scs_inference,[],[3998,3996,243,184])).
% 59.63/59.73 cnf(4012,plain,
% 59.63/59.73 (P10(a16,a24,a24,a16)),
% 59.63/59.73 inference(scs_inference,[],[3958,3974,3950,3850,3998,3996,243,184,169,182,250,183])).
% 59.63/59.73 cnf(4018,plain,
% 59.63/59.73 (P8(a36,a16,x40181,x40182,a36,a16,x40181,x40182)),
% 59.63/59.73 inference(scs_inference,[],[3958,3922,3974,3950,3850,3864,3998,3996,243,184,169,182,250,183,180,181,242])).
% 59.63/59.73 cnf(4020,plain,
% 59.63/59.73 (P1(a36,a16,a16)),
% 59.63/59.73 inference(scs_inference,[],[3958,3922,3974,3950,3850,3864,3998,3996,243,184,169,182,250,183,180,181,242,177])).
% 59.63/59.73 cnf(4022,plain,
% 59.63/59.73 (P10(f7(a24,a24,a24,a24),a24,a24,a24)),
% 59.63/59.73 inference(scs_inference,[],[3958,3922,3974,3950,3964,3850,3864,3998,3996,243,184,169,182,250,183,180,181,242,177,204])).
% 59.63/59.73 cnf(4026,plain,
% 59.63/59.73 (P3(a16,a21,a24,a16)),
% 59.63/59.73 inference(scs_inference,[],[3958,3922,3974,3944,3950,3964,3850,3848,3864,3998,3996,243,184,169,182,250,183,180,181,242,177,204,168,187])).
% 59.63/59.73 cnf(4028,plain,
% 59.63/59.73 (P3(a21,a16,a16,a24)),
% 59.63/59.73 inference(scs_inference,[],[3958,3922,3974,3930,3944,3950,3964,3850,3848,3864,3998,3996,243,184,169,182,250,183,180,181,242,177,204,168,187,188])).
% 59.63/59.73 cnf(4030,plain,
% 59.63/59.73 (P8(a24,a16,a16,a24,x40301,x40302,x40301,x40302)),
% 59.63/59.73 inference(scs_inference,[],[3958,3922,3974,3938,3930,3944,3950,3964,3850,3848,3864,3998,3996,243,184,169,182,250,183,180,181,242,177,204,168,187,188,271])).
% 59.63/59.73 cnf(4032,plain,
% 59.63/59.73 (P8(a24,a21,a24,a16,a16,a21,a16,a16)),
% 59.63/59.73 inference(scs_inference,[],[3958,3922,3974,3938,3930,3944,3950,3964,3850,3848,3864,3998,3996,243,184,169,182,250,183,180,181,242,177,204,168,187,188,271,241])).
% 59.63/59.73 cnf(4036,plain,
% 59.63/59.73 (P8(x40361,x40362,x40361,x40362,a16,a24,a16,a24)),
% 59.63/59.73 inference(scs_inference,[],[3958,3922,3974,3932,3938,3940,3930,3944,3950,3964,3850,3848,3864,3998,3996,243,184,169,182,250,183,180,181,242,177,204,168,187,188,271,241,270,272])).
% 59.63/59.73 cnf(4038,plain,
% 59.63/59.73 (P8(a16,a24,x40381,x40382,a24,a16,x40381,x40382)),
% 59.63/59.73 inference(scs_inference,[],[3958,3922,3974,3932,3938,3940,3930,3944,3950,3964,3850,3848,3864,3998,3996,243,184,169,182,250,183,180,181,242,177,204,168,187,188,271,241,270,272,269])).
% 59.63/59.73 cnf(4040,plain,
% 59.63/59.73 (P3(a16,a24,a16,a21)),
% 59.63/59.73 inference(scs_inference,[],[3958,3922,3936,3974,3932,3938,3940,3930,3944,3950,3964,3850,3848,3864,3998,3996,243,184,169,182,250,183,180,181,242,177,204,168,187,188,271,241,270,272,269,186])).
% 59.63/59.73 cnf(4042,plain,
% 59.63/59.73 (P2(f8(a24,a24,a24),a24,a24,a24)),
% 59.63/59.73 inference(scs_inference,[],[3958,3922,3936,3974,3932,3938,3940,3930,3944,3950,3962,3964,3994,3850,3848,3864,3998,3996,243,184,169,182,250,183,180,181,242,177,204,168,187,188,271,241,270,272,269,186,208])).
% 59.63/59.73 cnf(4046,plain,
% 59.63/59.73 (P4(a24,a24,a24,f49(a24,a24,a24,a24,a24))),
% 59.63/59.73 inference(scs_inference,[],[3958,3922,3936,3974,3932,3938,3940,3930,3944,3950,3956,3962,3964,3994,3850,3848,3864,3998,3996,3832,243,184,169,182,250,183,180,181,242,177,204,168,187,188,271,241,270,272,269,186,208,215,216])).
% 59.63/59.73 cnf(4048,plain,
% 59.63/59.73 (P9(f49(a24,a24,a24,a24,a24),a24,a24,a24)),
% 59.63/59.73 inference(scs_inference,[],[3958,3922,3936,3974,3932,3938,3940,3930,3944,3950,3956,3962,3964,3994,3850,3848,3864,3998,3996,3832,243,184,169,182,250,183,180,181,242,177,204,168,187,188,271,241,270,272,269,186,208,215,216,218])).
% 59.63/59.73 cnf(4050,plain,
% 59.63/59.73 (P10(a24,a16,a16,a24)),
% 59.63/59.73 inference(scs_inference,[],[3958,3922,3936,3974,3932,3938,3940,3930,3944,3950,3956,3962,3964,3994,3850,3848,3864,3998,3996,3832,243,184,169,182,250,183,180,181,242,177,204,168,187,188,271,241,270,272,269,186,208,215,216,218,258])).
% 59.63/59.73 cnf(4053,plain,
% 59.63/59.73 (P2(a24,f3(a24,a24,a24),a24,a24)),
% 59.63/59.73 inference(scs_inference,[],[3958,3922,3936,3974,3932,3938,3940,3930,3944,3950,3956,3962,3964,3994,3850,3848,3864,3998,3996,3832,243,184,169,182,250,183,180,181,242,177,204,168,187,188,271,241,270,272,269,186,208,215,216,218,258,201])).
% 59.63/59.73 cnf(4055,plain,
% 59.63/59.73 (P9(x40551,x40552,x40551,x40552)),
% 59.63/59.73 inference(scs_inference,[],[3958,3922,3936,3974,3932,3938,3940,3930,3944,3950,3956,3962,3964,3994,3850,3848,3864,3998,3996,3832,1475,243,184,169,182,250,183,180,181,242,177,204,168,187,188,271,241,270,272,269,186,208,215,216,218,258,201,257])).
% 59.63/59.73 cnf(4059,plain,
% 59.63/59.73 (P3(a24,a22,a16,a16)),
% 59.63/59.73 inference(scs_inference,[],[3958,3922,3936,3974,3932,3938,3940,3930,3944,3950,3956,3962,3964,3994,3850,3848,3864,3998,3996,3832,3834,454,1475,243,184,169,182,250,183,180,181,242,177,204,168,187,188,271,241,270,272,269,186,208,215,216,218,258,201,257,198,253])).
% 59.63/59.73 cnf(4066,plain,
% 59.63/59.73 (P7(f14(a24,a24,a24,a24),a24,f14(a24,a24,a24,a24),a24,a24,a24,a24,a24)),
% 59.63/59.73 inference(scs_inference,[],[3958,3922,3936,3974,3932,3938,3940,3930,3944,3950,3956,3962,3964,3994,3850,3848,3864,3980,3998,3996,3832,3834,454,1475,243,184,169,182,250,183,180,181,242,177,204,168,187,188,271,241,270,272,269,186,208,215,216,218,258,201,257,198,253,213,245,276])).
% 59.63/59.73 cnf(4068,plain,
% 59.63/59.73 (P7(a24,f14(a24,a24,a24,a24),a24,a24,f14(a24,a24,a24,a24),a24,a24,a24)),
% 59.63/59.73 inference(scs_inference,[],[3958,3922,3936,3974,3932,3938,3940,3930,3944,3950,3956,3962,3964,3994,3850,3848,3864,3980,3998,3996,3832,3834,454,1475,243,184,169,182,250,183,180,181,242,177,204,168,187,188,271,241,270,272,269,186,208,215,216,218,258,201,257,198,253,213,245,276,275])).
% 59.63/59.73 cnf(4070,plain,
% 59.63/59.73 (P4(a24,a24,f49(a24,a24,a24,a24,a24),a24)),
% 59.63/59.73 inference(scs_inference,[],[3958,3922,3936,3974,3932,3938,3940,3930,3944,3950,3956,3962,3964,3994,3850,3848,3864,3980,3998,3996,3832,3834,454,1475,243,184,169,182,250,183,180,181,242,177,204,168,187,188,271,241,270,272,269,186,208,215,216,218,258,201,257,198,253,213,245,276,275,185])).
% 59.63/59.73 cnf(4078,plain,
% 59.63/59.73 (P4(f14(a24,a24,a24,a24),a24,f14(a24,a24,a24,a24),a24)),
% 59.63/59.73 inference(scs_inference,[],[3958,3922,3936,3974,3932,3938,3940,3930,3944,3950,3956,3962,3964,3994,3850,3848,3864,3980,3998,3996,3832,3834,454,1475,243,184,169,182,250,183,180,181,242,177,204,168,187,188,271,241,270,272,269,186,208,215,216,218,258,201,257,198,253,213,245,276,275,185,274,190,214,260])).
% 59.63/59.73 cnf(4080,plain,
% 59.63/59.73 (P10(a24,f3(a24,a24,a24),f3(a24,a24,a24),a24)),
% 59.63/59.73 inference(scs_inference,[],[3958,3922,3936,3974,3932,3938,3940,3930,3944,3950,3956,3962,3964,3994,3850,3848,3864,3980,3998,3996,3832,3834,454,1475,243,184,169,182,250,183,180,181,242,177,204,168,187,188,271,241,270,272,269,186,208,215,216,218,258,201,257,198,253,213,245,276,275,185,274,190,214,260,212])).
% 59.63/59.73 cnf(4086,plain,
% 59.63/59.73 (P7(a24,a24,a24,a24,f14(a24,a24,a24,a24),a24,f14(a24,a24,a24,a24),a24)),
% 59.63/59.73 inference(scs_inference,[],[3958,3922,3936,3974,3932,3938,3940,3930,3944,3950,3956,3962,3964,3994,3850,3848,3864,3980,3998,3996,3832,3834,454,1475,243,184,169,182,250,183,180,181,242,177,204,168,187,188,271,241,270,272,269,186,208,215,216,218,258,201,257,198,253,213,245,276,275,185,274,190,214,260,212,223,224,273])).
% 59.63/59.73 cnf(4092,plain,
% 59.63/59.73 (P7(a24,f14(a24,a24,a24,a24),f14(a24,a24,a24,a24),a24,a24,a24,a24,a24)),
% 59.63/59.73 inference(scs_inference,[],[4046,4066,184,275])).
% 59.63/59.73 cnf(4098,plain,
% 59.63/59.73 (P8(a24,a24,a24,f3(a24,a24,a24),a24,f3(a24,a24,a24),a24,f3(a24,a24,a24))),
% 59.63/59.73 inference(scs_inference,[],[3968,4046,3966,4066,4068,184,275,273,169,243])).
% 59.63/59.73 cnf(4100,plain,
% 59.63/59.73 (P9(x41001,x41002,x41002,x41001)),
% 59.63/59.73 inference(scs_inference,[],[4055,3968,4046,3966,4066,4068,184,275,273,169,243,181])).
% 59.63/59.73 cnf(4106,plain,
% 59.63/59.73 (P4(f14(a24,a24,a24,a24),a24,a24,f14(a24,a24,a24,a24))),
% 59.63/59.73 inference(scs_inference,[],[4055,3968,4046,3966,4078,3918,4066,4068,184,275,273,169,243,181,276,180,185])).
% 59.63/59.73 cnf(4108,plain,
% 59.63/59.73 (P9(a24,a24,a24,f3(a24,a24,a24))),
% 59.63/59.73 inference(scs_inference,[],[4055,3968,4046,3966,4078,3918,4066,4068,184,275,273,169,243,181,276,180,185,250])).
% 59.63/59.73 cnf(4110,plain,
% 59.63/59.73 (P8(x41101,x41102,x41103,x41104,x41101,x41102,x41103,x41104)),
% 59.63/59.73 inference(scs_inference,[],[4055,3968,4046,3966,4078,3918,4066,4068,184,275,273,169,243,181,276,180,185,250,242])).
% 59.63/59.73 cnf(4120,plain,
% 59.63/59.73 (P1(x41201,x41202,x41202)),
% 59.63/59.73 inference(scs_inference,[],[4055,4050,3852,3968,4046,3966,4078,3918,4066,4068,164,184,275,273,169,243,181,276,180,185,250,242,182,183,274,204,177])).
% 59.63/59.73 cnf(4122,plain,
% 59.63/59.73 (P1(a16,a36,a16)),
% 59.63/59.73 inference(scs_inference,[],[4055,4050,4020,3852,3968,4046,3966,4078,3918,4066,4068,164,184,275,273,169,243,181,276,180,185,250,242,182,183,274,204,177,168])).
% 59.63/59.73 cnf(4124,plain,
% 59.63/59.73 (P3(a16,a21,a16,a24)),
% 59.63/59.73 inference(scs_inference,[],[4055,4050,4020,4026,3852,3968,4046,3966,4078,3918,4066,4068,164,184,275,273,169,243,181,276,180,185,250,242,182,183,274,204,177,168,188])).
% 59.63/59.73 cnf(4126,plain,
% 59.63/59.73 (P3(a16,a16,a24,a21)),
% 59.63/59.73 inference(scs_inference,[],[4055,4050,4020,4026,4040,3852,3968,4046,3966,4078,3918,4066,4068,164,184,275,273,169,243,181,276,180,185,250,242,182,183,274,204,177,168,188,187])).
% 59.63/59.73 cnf(4128,plain,
% 59.63/59.73 (P8(a24,a16,a16,a16,a21,a24,a21,a16)),
% 59.77/59.73 inference(scs_inference,[],[4055,4050,3942,4020,4026,4040,3852,3968,4046,3966,4078,3918,4066,4068,164,184,275,273,169,243,181,276,180,185,250,242,182,183,274,204,177,168,188,187,271])).
% 59.77/59.73 cnf(4130,plain,
% 59.77/59.73 (P8(a16,a16,a16,a24,a21,a16,a21,a24)),
% 59.77/59.73 inference(scs_inference,[],[4055,4050,3942,4020,4026,4040,3852,3968,4046,3966,4078,3918,4066,4068,164,184,275,273,169,243,181,276,180,185,250,242,182,183,274,204,177,168,188,187,271,270])).
% 59.77/59.73 cnf(4132,plain,
% 59.77/59.73 (P8(a24,a16,a24,a21,a16,a16,a16,a21)),
% 59.77/59.73 inference(scs_inference,[],[4055,4050,3942,4020,4026,4040,3852,3968,4046,3966,4078,3918,4066,4068,164,184,275,273,169,243,181,276,180,185,250,242,182,183,274,204,177,168,188,187,271,270,241])).
% 59.77/59.73 cnf(4134,plain,
% 59.77/59.74 (P8(a16,a24,a21,a24,a16,a16,a21,a16)),
% 59.77/59.74 inference(scs_inference,[],[4055,4050,3942,4020,4026,4040,3852,3968,4046,3966,4078,3918,4066,4068,164,184,275,273,169,243,181,276,180,185,250,242,182,183,274,204,177,168,188,187,271,270,241,272])).
% 59.77/59.74 cnf(4136,plain,
% 59.77/59.74 (P8(x41361,x41362,x41361,x41362,a24,a16,a16,a24)),
% 59.77/59.74 inference(scs_inference,[],[4055,4050,3942,4030,4020,4026,4040,3852,3968,4046,3966,4078,3918,4066,4068,164,184,275,273,169,243,181,276,180,185,250,242,182,183,274,204,177,168,188,187,271,270,241,272,269])).
% 59.77/59.74 cnf(4138,plain,
% 59.77/59.74 (P3(a16,a21,a16,a16)),
% 59.77/59.74 inference(scs_inference,[],[4055,4050,3942,4030,3946,4020,4026,4040,3852,3968,4046,3966,4078,3918,4066,4068,164,184,275,273,169,243,181,276,180,185,250,242,182,183,274,204,177,168,188,187,271,270,241,272,269,186])).
% 59.77/59.74 cnf(4142,plain,
% 59.77/59.74 (P4(f3(a24,a24,a24),a24,a24,f3(a24,a24,a24))),
% 59.77/59.74 inference(scs_inference,[],[4055,4050,3942,4030,3946,4020,4026,4040,3852,3968,4046,3966,4004,4078,3918,4086,4066,4068,164,184,275,273,169,243,181,276,180,185,250,242,182,183,274,204,177,168,188,187,271,270,241,272,269,186,280,200])).
% 59.77/59.74 cnf(4144,plain,
% 59.77/59.74 (P10(f3(a24,a24,a24),a24,a24,a24)),
% 59.77/59.74 inference(scs_inference,[],[4055,4050,3942,4030,3946,4020,4026,4040,3852,3968,4046,3966,4004,4078,3918,4053,4086,4066,4068,164,184,275,273,169,243,181,276,180,185,250,242,182,183,274,204,177,168,188,187,271,270,241,272,269,186,280,200,189])).
% 59.77/59.74 cnf(4148,plain,
% 59.77/59.74 (P10(x41481,x41482,x41481,x41482)),
% 59.77/59.74 inference(scs_inference,[],[4055,4050,3942,4030,4036,3946,4020,4026,4040,3852,3968,4046,3966,4004,4078,3918,4053,4086,4066,4068,3974,3956,164,184,275,273,169,243,181,276,180,185,250,242,182,183,274,204,177,168,188,187,271,270,241,272,269,186,280,200,189,216,258])).
% 59.77/59.74 cnf(4158,plain,
% 59.77/59.74 (P2(a24,a24,f3(a24,a24,a24),f3(a24,a24,a24))),
% 59.77/59.74 inference(scs_inference,[],[142,4055,4050,3942,4030,4036,3946,4020,4026,4040,3852,3968,4046,3966,4004,4078,3918,4053,4086,4066,4068,3954,3974,3956,164,184,275,273,169,243,181,276,180,185,250,242,182,183,274,204,177,168,188,187,271,270,241,272,269,186,280,200,189,216,258,214,208,218,215,201])).
% 59.77/59.74 cnf(4177,plain,
% 59.77/59.74 (P9(x41771,x41772,x41771,x41772)),
% 59.77/59.74 inference(rename_variables,[],[4055])).
% 59.77/59.74 cnf(4181,plain,
% 59.77/59.74 (P6(a24,x41811,x41811)),
% 59.77/59.74 inference(scs_inference,[],[142,4055,4177,4050,3942,4030,4036,3946,4020,4026,4040,3852,3968,4046,3966,4004,4078,3918,4053,4086,4066,4068,4042,3954,3964,3994,3958,3974,3956,3962,164,184,275,273,169,243,181,276,180,185,250,242,182,183,274,204,177,168,188,187,271,270,241,272,269,186,280,200,189,216,258,214,208,218,215,201,195,206,194,198,259,207,253,256,209,203,192])).
% 59.77/59.74 cnf(4183,plain,
% 59.77/59.74 (P9(x41831,x41832,x41831,x41832)),
% 59.77/59.74 inference(rename_variables,[],[4055])).
% 59.77/59.74 cnf(4185,plain,
% 59.77/59.74 (P7(a36,a16,a16,a16,a36,a16,a16,a16)),
% 59.77/59.74 inference(scs_inference,[],[142,4055,4177,4183,4050,3942,4030,4036,3946,4020,4026,4040,3852,3968,4046,3966,4004,4078,3918,4053,4086,4066,4068,4042,3954,3964,3994,3958,3974,3956,3962,164,184,275,273,169,243,181,276,180,185,250,242,182,183,274,204,177,168,188,187,271,270,241,272,269,186,280,200,189,216,258,214,208,218,215,201,195,206,194,198,259,207,253,256,209,203,192,245])).
% 59.77/59.74 cnf(4186,plain,
% 59.77/59.74 (P9(x41861,x41862,x41861,x41862)),
% 59.77/59.74 inference(rename_variables,[],[4055])).
% 59.77/59.74 cnf(4191,plain,
% 59.77/59.74 (P6(f46(a24,x41911),a24,x41911)),
% 59.77/59.74 inference(scs_inference,[],[142,4055,4177,4183,4186,4050,3942,4030,4036,3946,4020,4026,4040,3852,3968,4046,3966,4004,4078,3918,4053,4086,4066,4068,4042,3954,3964,3994,3958,3974,3956,3962,164,184,275,273,169,243,181,276,180,185,250,242,182,183,274,204,177,168,188,187,271,270,241,272,269,186,280,200,189,216,258,214,208,218,215,201,195,206,194,198,259,207,253,256,209,203,192,245,223,176])).
% 59.77/59.74 cnf(4199,plain,
% 59.77/59.74 (P6(f46(a24,x41991),x41991,a24)),
% 59.77/59.74 inference(scs_inference,[],[142,4055,4177,4183,4186,4050,3942,4030,4036,3946,4020,4026,4040,3852,3968,4046,3966,4004,4078,3918,4053,4086,4066,4068,4042,3954,3964,3994,3958,3974,3956,3962,164,184,275,273,169,243,181,276,180,185,250,242,182,183,274,204,177,168,188,187,271,270,241,272,269,186,280,200,189,216,258,214,208,218,215,201,195,206,194,198,259,207,253,256,209,203,192,245,223,176,173,170,1688,171])).
% 59.77/59.74 cnf(4208,plain,
% 59.77/59.74 (P4(f7(a24,a24,a24,a24),a24,f7(a24,a24,a24,a24),a24)),
% 59.77/59.74 inference(scs_inference,[],[142,4055,4177,4183,4186,4050,3942,4018,4030,4036,3946,4020,4026,4040,3852,3968,4046,3966,4004,4078,3918,4053,4086,4066,4068,4022,4042,3954,3964,3994,3958,3974,3956,3962,164,184,275,273,169,243,181,276,180,185,250,242,182,183,274,204,177,168,188,187,271,270,241,272,269,186,280,200,189,216,258,214,208,218,215,201,195,206,194,198,259,207,253,256,209,203,192,245,223,176,173,170,1688,171,251,217,222,190])).
% 59.77/59.74 cnf(4210,plain,
% 59.77/59.74 (P9(f47(a24,a24,x42101,x42101,a24,a24),a24,a24,x42101)),
% 59.77/59.74 inference(scs_inference,[],[142,4055,4177,4183,4186,4050,3942,4018,4030,4036,3946,4020,4026,4040,3852,3968,4046,3966,4004,4078,3918,4053,4086,4066,4068,4022,4042,3954,3964,3994,3958,3974,3956,3962,164,184,275,273,169,243,181,276,180,185,250,242,182,183,274,204,177,168,188,187,271,270,241,272,269,186,280,200,189,216,258,214,208,218,215,201,195,206,194,198,259,207,253,256,209,203,192,245,223,176,173,170,1688,171,251,217,222,190,221])).
% 59.77/59.74 cnf(4220,plain,
% 59.77/59.74 (P6(a24,a24,f3(a24,a24,a24))),
% 59.77/59.74 inference(scs_inference,[],[142,4055,4177,4183,4186,4050,3942,4018,4030,4036,3946,4020,4026,4040,3852,3968,4046,3966,4004,4080,4078,3918,4053,4086,4066,4068,4022,4042,3954,3964,3994,3958,3974,3956,3962,164,184,275,273,169,243,181,276,180,185,250,242,182,183,274,204,177,168,188,187,271,270,241,272,269,186,280,200,189,216,258,214,208,218,215,201,195,206,194,198,259,207,253,256,209,203,192,245,223,176,173,170,1688,171,251,217,222,190,221,240,244,220,246,179])).
% 59.77/59.74 cnf(4222,plain,
% 59.77/59.74 (~P3(a34,a31,x42221,a32)+~E(x42221,a33)),
% 59.77/59.74 inference(scs_inference,[],[142,4055,4177,4183,4186,4050,3942,4018,4030,4036,3946,4020,4026,4040,3852,3968,4046,3966,4004,4080,4078,3918,4053,4086,4066,4068,4022,4042,3954,3964,3994,3958,365,3974,3956,3962,164,184,275,273,169,243,181,276,180,185,250,242,182,183,274,204,177,168,188,187,271,270,241,272,269,186,280,200,189,216,258,214,208,218,215,201,195,206,194,198,259,207,253,256,209,203,192,245,223,176,173,170,1688,171,251,217,222,190,221,240,244,220,246,179,140])).
% 59.77/59.74 cnf(4230,plain,
% 59.77/59.74 (P8(x42301,x42302,x42302,x42301,a24,a24,a24,a24)),
% 59.77/59.74 inference(scs_inference,[],[4181,1901])).
% 59.77/59.74 cnf(4234,plain,
% 59.77/59.74 (P4(a24,x42341,a24,x42341)),
% 59.77/59.74 inference(scs_inference,[],[4181,173])).
% 59.77/59.74 cnf(4241,plain,
% 59.77/59.74 (P7(a16,a36,a16,a16,a36,a16,a16,a16)),
% 59.77/59.74 inference(scs_inference,[],[4181,4185,4191,4199,173,1688,170,275])).
% 59.77/59.74 cnf(4243,plain,
% 59.77/59.74 (P7(a24,a24,a24,a24,a24,f14(a24,a24,a24,a24),f14(a24,a24,a24,a24),a24)),
% 59.77/59.74 inference(scs_inference,[],[4181,4185,4092,4191,4199,173,1688,170,275,273])).
% 59.77/59.74 cnf(4245,plain,
% 59.77/59.74 (P9(a24,f3(a24,a24,a24),a24,a24)),
% 59.77/59.74 inference(scs_inference,[],[4181,4185,4108,4092,4191,4199,173,1688,170,275,273,180])).
% 59.77/59.74 cnf(4249,plain,
% 59.77/59.74 (P7(a36,a16,a36,a16,a16,a16,a16,a16)),
% 59.77/59.74 inference(scs_inference,[],[4181,4185,4108,4092,4070,4191,4199,173,1688,170,275,273,180,184,276])).
% 59.77/59.74 cnf(4251,plain,
% 59.77/59.74 (P6(a24,f3(a24,a24,a24),a24)),
% 59.77/59.74 inference(scs_inference,[],[4181,4185,4108,4092,4070,4191,4199,4220,173,1688,170,275,273,180,184,276,171])).
% 59.77/59.74 cnf(4259,plain,
% 59.77/59.74 (P8(x42591,x42592,x42593,x42594,x42592,x42591,x42593,x42594)),
% 59.77/59.74 inference(scs_inference,[],[4100,4181,4122,4185,4108,4092,4070,4191,4199,4142,4208,4220,173,1688,170,275,273,180,184,276,171,185,243,169,242])).
% 59.77/59.74 cnf(4261,plain,
% 59.77/59.74 (P7(a16,a16,a36,a16,a16,a16,a36,a16)),
% 59.77/59.74 inference(scs_inference,[],[4100,4181,4122,4185,4108,4092,4070,4191,4199,4142,4208,4220,173,1688,170,275,273,180,184,276,171,185,243,169,242,274])).
% 59.77/59.74 cnf(4263,plain,
% 59.77/59.74 (P9(a24,a24,f3(a24,a24,a24),a24)),
% 59.77/59.74 inference(scs_inference,[],[4100,4181,4122,4185,4108,4092,4070,4191,4199,4142,4208,4220,173,1688,170,275,273,180,184,276,171,185,243,169,242,274,181])).
% 59.77/59.74 cnf(4265,plain,
% 59.77/59.74 (P1(a16,f7(a16,a25,a30,a24),f4(a16,a16,a24))),
% 59.77/59.74 inference(scs_inference,[],[4100,4181,4122,4185,4108,4092,3862,4070,4191,4199,4142,4208,4220,173,1688,170,275,273,180,184,276,171,185,243,169,242,274,181,177])).
% 59.77/59.74 cnf(4269,plain,
% 59.77/59.74 (P1(x42691,x42692,x42691)),
% 59.77/59.74 inference(scs_inference,[],[4100,4120,4181,4122,4185,4108,4092,3862,4144,4070,4191,4199,4142,4208,4220,173,1688,170,275,273,180,184,276,171,185,243,169,242,274,181,177,182,168])).
% 59.77/59.74 cnf(4273,plain,
% 59.77/59.74 (P3(a16,a16,a21,a24)),
% 59.77/59.74 inference(scs_inference,[],[4100,4120,4181,4122,4126,4185,4108,4092,3862,4144,4070,4191,4199,4142,4208,4220,166,173,1688,170,275,273,180,184,276,171,185,243,169,242,274,181,177,182,168,204,188])).
% 59.77/59.74 cnf(4275,plain,
% 59.77/59.74 (P10(x42751,x42752,x42752,x42751)),
% 59.77/59.74 inference(scs_inference,[],[4100,4148,4120,4181,4122,4126,4185,4108,4092,3862,4144,4070,4191,4199,4142,4208,4220,166,173,1688,170,275,273,180,184,276,171,185,243,169,242,274,181,177,182,168,204,188,183])).
% 59.77/59.74 cnf(4277,plain,
% 59.77/59.74 (P3(a24,a16,a22,a16)),
% 59.77/59.74 inference(scs_inference,[],[4100,4148,4120,4181,4059,4122,4126,4185,4108,4092,3862,4144,4070,4191,4199,4142,4208,4220,166,173,1688,170,275,273,180,184,276,171,185,243,169,242,274,181,177,182,168,204,188,183,187])).
% 59.77/59.74 cnf(4281,plain,
% 59.77/59.74 (P8(x42811,x42812,x42811,x42812,x42813,x42814,x42813,x42814)),
% 59.77/59.74 inference(scs_inference,[],[4100,4110,4148,4120,4181,4136,4059,4122,4126,4185,4108,4092,3862,4144,4070,4191,4199,4142,4208,4220,166,173,1688,170,275,273,180,184,276,171,185,243,169,242,274,181,177,182,168,204,188,183,187,270,272])).
% 59.77/59.74 cnf(4285,plain,
% 59.77/59.74 (P8(a16,a21,a16,a16,a24,a21,a24,a16)),
% 59.77/59.74 inference(scs_inference,[],[4100,4110,4148,4120,4181,4136,4028,4059,4122,4126,4185,4108,4092,3862,4144,4070,4191,4199,4142,4208,4220,166,173,1688,170,275,273,180,184,276,171,185,243,169,242,274,181,177,182,168,204,188,183,187,270,272,271,241])).
% 59.77/59.74 cnf(4289,plain,
% 59.77/59.74 (P8(a21,a24,a21,a16,a24,a16,a16,a16)),
% 59.77/59.74 inference(scs_inference,[],[4100,4110,4148,4120,4181,4136,4028,4059,4122,4126,4128,4185,4108,4092,3862,4144,4070,4191,4199,4142,4208,4220,166,173,1688,170,275,273,180,184,276,171,185,243,169,242,274,181,177,182,168,204,188,183,187,270,272,271,241,186,269])).
% 59.77/59.74 cnf(4291,plain,
% 59.77/59.74 (P4(x42911,a24,x42911,a24)),
% 59.77/59.74 inference(scs_inference,[],[4100,4110,4148,4120,4181,4136,4028,4059,4122,4126,4128,4185,4108,4092,3862,4144,4070,4191,4199,4142,4208,4220,166,173,1688,170,275,273,180,184,276,171,185,243,169,242,274,181,177,182,168,204,188,183,187,270,272,271,241,186,269,191])).
% 59.77/59.74 cnf(4292,plain,
% 59.77/59.74 (P10(x42921,x42922,x42921,x42922)),
% 59.77/59.74 inference(rename_variables,[],[4148])).
% 59.77/59.74 cnf(4295,plain,
% 59.77/59.74 (P8(a16,a24,x42951,x42952,a24,a16,x42951,x42952)),
% 59.77/59.74 inference(rename_variables,[],[4038])).
% 59.77/59.74 cnf(4298,plain,
% 59.77/59.74 (P10(x42981,x42982,x42981,x42982)),
% 59.77/59.74 inference(rename_variables,[],[4148])).
% 59.77/59.74 cnf(4303,plain,
% 59.77/59.74 (P10(a24,f3(a24,a24,a24),f3(a24,a24,a24),f3(a24,a24,a24))),
% 59.77/59.74 inference(scs_inference,[],[4100,4110,4148,4292,4120,4181,4136,3928,4028,4059,4122,4126,4128,4185,4108,4092,3862,4144,4070,4191,4199,4142,4158,4208,4220,4038,4295,3966,166,173,1688,170,275,273,180,184,276,171,185,243,169,242,274,181,177,182,168,204,188,183,187,270,272,271,241,186,269,191,266,214,262,189])).
% 59.77/59.74 cnf(4306,plain,
% 59.77/59.74 (P6(a24,x43061,x43061)),
% 59.77/59.74 inference(rename_variables,[],[4181])).
% 59.77/59.74 cnf(4308,plain,
% 59.77/59.74 (P9(f47(x43081,x43081,x43081,x43081,a24,a24),a24,x43081,x43081)),
% 59.77/59.74 inference(scs_inference,[],[4100,4110,4148,4292,4120,4181,4306,4136,3928,4028,4059,4122,4126,4128,4185,4108,4092,3862,4144,4070,4191,4199,4142,4158,4208,4220,4038,4295,3966,166,173,1688,170,275,273,180,184,276,171,185,243,169,242,274,181,177,182,168,204,188,183,187,270,272,271,241,186,269,191,266,214,262,189,222,221])).
% 59.77/59.74 cnf(4311,plain,
% 59.77/59.74 (P8(x43111,x43112,x43113,x43114,x43111,x43112,x43113,x43114)),
% 59.77/59.74 inference(rename_variables,[],[4110])).
% 59.77/59.74 cnf(4312,plain,
% 59.77/59.74 (P10(x43121,x43122,x43121,x43122)),
% 59.77/59.74 inference(rename_variables,[],[4148])).
% 59.77/59.74 cnf(4314,plain,
% 59.77/59.74 (P7(a24,x43141,x43141,x43141,a24,x43141,x43141,x43141)),
% 59.77/59.74 inference(scs_inference,[],[4100,4110,4148,4292,4298,4120,4181,4306,4136,3928,4028,4059,4122,4126,4128,4185,4108,4092,3862,4144,4070,4191,4199,4142,4158,4208,4220,4038,4295,3966,166,173,1688,170,275,273,180,184,276,171,185,243,169,242,274,181,177,182,168,204,188,183,187,270,272,271,241,186,269,191,266,214,262,189,222,221,263,240])).
% 59.77/59.74 cnf(4316,plain,
% 59.77/59.74 (P10(f12(x43161,x43161,x43161,x43162,x43162),x43161,x43162,x43162)),
% 59.77/59.74 inference(scs_inference,[],[4100,4110,4148,4292,4298,4312,4120,4181,4306,4136,3928,4028,4059,4122,4126,4128,4185,4108,4092,3862,4144,4070,4191,4199,4142,4158,4208,4220,4038,4295,3966,166,173,1688,170,275,273,180,184,276,171,185,243,169,242,274,181,177,182,168,204,188,183,187,270,272,271,241,186,269,191,266,214,262,189,222,221,263,240,215])).
% 59.77/59.74 cnf(4317,plain,
% 59.77/59.74 (P1(x43171,x43172,x43172)),
% 59.77/59.74 inference(rename_variables,[],[4120])).
% 59.77/59.74 cnf(4318,plain,
% 59.77/59.74 (P10(x43181,x43182,x43181,x43182)),
% 59.77/59.74 inference(rename_variables,[],[4148])).
% 59.77/59.74 cnf(4322,plain,
% 59.77/59.74 (P10(x43221,f4(x43221,x43221,x43222),x43222,x43221)),
% 59.77/59.74 inference(scs_inference,[],[4100,4110,4148,4292,4298,4312,4318,4120,4012,4181,4306,4136,3928,4028,4059,4122,4126,4128,4185,4108,4092,3862,4144,4070,4191,4199,4142,4158,4208,4220,4038,4295,3966,166,173,1688,170,275,273,180,184,276,171,185,243,169,242,274,181,177,182,168,204,188,183,187,270,272,271,241,186,269,191,266,214,262,189,222,221,263,240,215,208,206])).
% 59.77/59.74 cnf(4324,plain,
% 59.77/59.74 (P1(f5(x43241,x43241,x43242),x43242,x43241)),
% 59.77/59.74 inference(scs_inference,[],[4100,4110,4148,4292,4298,4312,4318,4120,4012,4181,4306,4136,3928,4028,4059,4122,4126,4128,4185,4108,4092,3862,4144,4070,4191,4199,4142,4158,4208,4220,4038,4295,3966,166,173,1688,170,275,273,180,184,276,171,185,243,169,242,274,181,177,182,168,204,188,183,187,270,272,271,241,186,269,191,266,214,262,189,222,221,263,240,215,208,206,195])).
% 59.77/59.74 cnf(4326,plain,
% 59.77/59.74 (P2(f7(a24,a24,a24,a24),a24,a24,a24)),
% 59.77/59.74 inference(scs_inference,[],[4100,4110,4148,4292,4298,4312,4318,4120,4012,4181,4306,4136,3928,4028,4059,4122,4126,4128,4185,4108,4092,3862,4144,4070,4191,4199,4142,4158,4208,4220,4038,4295,3966,166,173,1688,170,275,273,180,184,276,171,185,243,169,242,274,181,177,182,168,204,188,183,187,270,272,271,241,186,269,191,266,214,262,189,222,221,263,240,215,208,206,195,201])).
% 59.77/59.74 cnf(4329,plain,
% 59.77/59.74 (P6(a24,x43291,x43291)),
% 59.77/59.74 inference(rename_variables,[],[4181])).
% 59.77/59.74 cnf(4335,plain,
% 59.77/59.74 (P1(f4(x43351,x43351,x43352),x43352,x43351)),
% 59.77/59.74 inference(scs_inference,[],[4100,4110,4148,4292,4298,4312,4318,4120,4012,4181,4306,4136,3928,4028,4059,4122,4126,4128,4185,4108,4092,3862,4144,4070,4191,4199,4142,4158,4208,4220,4038,4295,3966,166,173,1688,170,275,273,180,184,276,171,185,243,169,242,274,181,177,182,168,204,188,183,187,270,272,271,241,186,269,191,266,214,262,189,222,221,263,240,215,208,206,195,201,244,207,198,194])).
% 59.77/59.74 cnf(4337,plain,
% 59.77/59.74 (P6(f47(x43371,x43371,x43371,x43371,a24,a24),x43371,x43371)),
% 59.77/59.74 inference(scs_inference,[],[4100,4110,4148,4292,4298,4312,4318,4120,4012,4181,4306,4329,4136,3928,4028,4059,4122,4126,4128,4185,4108,4092,3862,4144,4070,4191,4199,4142,4158,4208,4220,4038,4295,3966,166,173,1688,170,275,273,180,184,276,171,185,243,169,242,274,181,177,182,168,204,188,183,187,270,272,271,241,186,269,191,266,214,262,189,222,221,263,240,215,208,206,195,201,244,207,198,194,220])).
% 59.77/59.74 cnf(4339,plain,
% 59.77/59.74 (P3(x43391,x43392,x43392,x43392)),
% 59.77/59.74 inference(scs_inference,[],[4100,4110,4311,4148,4292,4298,4312,4318,4120,4317,4012,4181,4306,4329,4136,3928,4028,4059,4122,4126,4128,4185,4108,4092,3862,4144,4070,4191,4199,4142,4158,4208,4220,4038,4295,3966,166,173,1688,170,275,273,180,184,276,171,185,243,169,242,274,181,177,182,168,204,188,183,187,270,272,271,241,186,269,191,266,214,262,189,222,221,263,240,215,208,206,195,201,244,207,198,194,220,253])).
% 59.77/59.74 cnf(4340,plain,
% 59.77/59.74 (P8(x43401,x43402,x43403,x43404,x43401,x43402,x43403,x43404)),
% 59.77/59.74 inference(rename_variables,[],[4110])).
% 59.77/59.74 cnf(4341,plain,
% 59.77/59.74 (P1(x43411,x43412,x43412)),
% 59.77/59.74 inference(rename_variables,[],[4120])).
% 59.77/59.74 cnf(4343,plain,
% 59.77/59.74 (P2(f9(x43431,x43431,x43431),x43431,x43431,x43431)),
% 59.77/59.74 inference(scs_inference,[],[4100,4110,4311,4148,4292,4298,4312,4318,4120,4317,4012,4181,4306,4329,4136,3928,4028,4059,4122,4126,4128,4185,4108,4092,3862,4144,4070,4191,4199,4142,4158,4208,4220,4038,4295,3966,166,173,1688,170,275,273,180,184,276,171,185,243,169,242,274,181,177,182,168,204,188,183,187,270,272,271,241,186,269,191,266,214,262,189,222,221,263,240,215,208,206,195,201,244,207,198,194,220,253,209])).
% 59.77/59.74 cnf(4344,plain,
% 59.77/59.74 (P6(a24,x43441,x43441)),
% 59.77/59.74 inference(rename_variables,[],[4181])).
% 59.77/59.74 cnf(4345,plain,
% 59.77/59.74 (P9(x43451,x43452,x43452,x43451)),
% 59.77/59.74 inference(rename_variables,[],[4100])).
% 59.77/59.74 cnf(4347,plain,
% 59.77/59.74 (P6(f3(a24,a24,a24),f3(a24,a24,a24),f3(a24,a24,a24))),
% 59.77/59.74 inference(scs_inference,[],[4100,4110,4311,4340,4148,4292,4298,4312,4318,4120,4317,4341,4012,4181,4306,4329,4136,3928,4028,4059,4122,4126,4128,4185,4108,4092,3862,4144,4070,4191,4199,4142,4158,4208,4220,4038,4295,3966,166,173,1688,170,275,273,180,184,276,171,185,243,169,242,274,181,177,182,168,204,188,183,187,270,272,271,241,186,269,191,266,214,262,189,222,221,263,240,215,208,206,195,201,244,207,198,194,220,253,209,256])).
% 59.77/59.74 cnf(4349,plain,
% 59.77/59.74 (P1(x43491,x43492,x43492)),
% 59.77/59.74 inference(rename_variables,[],[4120])).
% 59.77/59.74 cnf(4351,plain,
% 59.77/59.74 (P6(f3(a24,a24,a24),a24,a24)),
% 59.77/59.74 inference(scs_inference,[],[4100,4110,4311,4340,4148,4292,4298,4312,4318,4120,4317,4341,4349,4012,4181,4306,4329,4344,4136,3928,4028,4059,4122,4126,4128,4185,4108,4092,3862,4144,4070,4191,4199,4142,4158,4208,4220,4038,4295,3966,166,173,1688,170,275,273,180,184,276,171,185,243,169,242,274,181,177,182,168,204,188,183,187,270,272,271,241,186,269,191,266,214,262,189,222,221,263,240,215,208,206,195,201,244,207,198,194,220,253,209,256,179])).
% 59.77/59.74 cnf(4352,plain,
% 59.77/59.74 (P6(a24,x43521,x43521)),
% 59.77/59.74 inference(rename_variables,[],[4181])).
% 59.77/59.74 cnf(4353,plain,
% 59.77/59.74 (P1(x43531,x43532,x43532)),
% 59.77/59.74 inference(rename_variables,[],[4120])).
% 59.77/59.74 cnf(4355,plain,
% 59.77/59.74 (P6(f6(x43551,x43551,x43551),x43551,x43551)),
% 59.77/59.74 inference(scs_inference,[],[4100,4110,4311,4340,4148,4292,4298,4312,4318,4120,4317,4341,4349,4012,4181,4306,4329,4344,4352,4136,3928,4028,4059,4122,4126,4128,4185,4108,4092,3862,4144,4070,4191,4199,4142,4158,4208,4220,4038,4295,3966,166,173,1688,170,275,273,180,184,276,171,185,243,169,242,274,181,177,182,168,204,188,183,187,270,272,271,241,186,269,191,266,214,262,189,222,221,263,240,215,208,206,195,201,244,207,198,194,220,253,209,256,179,203])).
% 59.77/59.74 cnf(4357,plain,
% 59.77/59.74 (P6(a24,x43571,x43571)),
% 59.77/59.74 inference(rename_variables,[],[4181])).
% 59.77/59.74 cnf(4358,plain,
% 59.77/59.74 (P10(x43581,x43582,x43581,x43582)),
% 59.77/59.74 inference(rename_variables,[],[4148])).
% 59.77/59.74 cnf(4360,plain,
% 59.77/59.74 (P6(a24,f4(a16,a16,a24),f7(a16,a25,a30,a24))),
% 59.77/59.74 inference(scs_inference,[],[4100,4110,4311,4340,4148,4292,4298,4312,4318,4120,4317,4341,4349,4012,4181,4306,4329,4344,4352,4357,4136,3928,4028,4059,4122,4126,4128,4185,4108,4092,3862,4144,4070,4191,4199,4142,4158,4208,4220,4038,4295,3856,3966,166,173,1688,170,275,273,180,184,276,171,185,243,169,242,274,181,177,182,168,204,188,183,187,270,272,271,241,186,269,191,266,214,262,189,222,221,263,240,215,208,206,195,201,244,207,198,194,220,253,209,256,179,203,192])).
% 59.77/59.74 cnf(4361,plain,
% 59.77/59.74 (P6(a24,x43611,x43611)),
% 59.77/59.74 inference(rename_variables,[],[4181])).
% 59.77/59.74 cnf(4364,plain,
% 59.77/59.74 (P9(x43641,x43642,x43642,x43641)),
% 59.77/59.74 inference(rename_variables,[],[4100])).
% 59.77/59.74 cnf(4367,plain,
% 59.77/59.74 (P9(x43671,x43672,x43672,x43671)),
% 59.77/59.74 inference(rename_variables,[],[4100])).
% 59.77/59.74 cnf(4369,plain,
% 59.77/59.74 (P6(f46(x43691,x43692),x43691,x43692)),
% 59.77/59.74 inference(scs_inference,[],[142,4100,4345,4364,4110,4311,4340,4148,4292,4298,4312,4318,4120,4317,4341,4349,4353,4012,4181,4306,4329,4344,4352,4357,4361,4136,3928,4028,4059,4122,4126,4128,4185,4108,4092,3862,4144,4070,4191,4199,4142,4158,4208,4220,4038,4295,3830,3856,3966,166,173,1688,170,275,273,180,184,276,171,185,243,169,242,274,181,177,182,168,204,188,183,187,270,272,271,241,186,269,191,266,214,262,189,222,221,263,240,215,208,206,195,201,244,207,198,194,220,253,209,256,179,203,192,224,223,176])).
% 59.77/59.74 cnf(4372,plain,
% 59.77/59.74 (P1(x43721,x43722,x43722)),
% 59.77/59.74 inference(rename_variables,[],[4120])).
% 59.77/59.74 cnf(4373,plain,
% 59.77/59.74 (P6(a24,x43731,x43731)),
% 59.77/59.74 inference(rename_variables,[],[4181])).
% 59.77/59.74 cnf(4383,plain,
% 59.77/59.74 (P6(f7(a24,a24,a24,a24),a24,a24)),
% 59.77/59.74 inference(scs_inference,[],[142,4100,4345,4364,4110,4311,4340,4148,4292,4298,4312,4318,4120,4317,4341,4349,4353,4372,4012,4181,4306,4329,4344,4352,4357,4361,4136,3928,4028,4059,4122,4126,4128,4185,4108,4092,3862,4144,4070,4191,4199,4142,4158,4208,4220,4038,4295,3830,3856,3966,166,173,1688,170,275,273,180,184,276,171,185,243,169,242,274,181,177,182,168,204,188,183,187,270,272,271,241,186,269,191,266,214,262,189,222,221,263,240,215,208,206,195,201,244,207,198,194,220,253,209,256,179,203,192,224,223,176,1694,247,193,205,178])).
% 59.77/59.74 cnf(4384,plain,
% 59.77/59.74 (P1(x43841,x43842,x43842)),
% 59.77/59.74 inference(rename_variables,[],[4120])).
% 59.77/59.74 cnf(4387,plain,
% 59.77/59.74 (P10(x43871,x43872,x43871,x43872)),
% 59.77/59.74 inference(rename_variables,[],[4148])).
% 59.77/59.74 cnf(4400,plain,
% 59.77/59.74 (~P3(a34,a33,a31,x44001)+~E(x44001,a32)),
% 59.77/59.74 inference(scs_inference,[],[142,4100,4345,4364,4367,4110,4311,4340,4148,4292,4298,4312,4318,4358,4387,4120,4317,4341,4349,4353,4372,4384,4012,4181,4306,4329,4344,4352,4357,4361,4373,4136,3928,4028,4059,4122,4126,4128,4185,4108,4092,3862,4144,4070,4191,4199,4142,4158,4208,4220,4038,4295,3830,3856,401,3966,4055,166,173,1688,170,275,273,180,184,276,171,185,243,169,242,274,181,177,182,168,204,188,183,187,270,272,271,241,186,269,191,266,214,262,189,222,221,263,240,215,208,206,195,201,244,207,198,194,220,253,209,256,179,203,192,224,223,176,1694,247,193,205,178,216,218,190,225,141])).
% 59.77/59.74 cnf(4403,plain,
% 59.77/59.74 (P8(x44031,x44032,x44033,x44034,x44032,x44031,x44033,x44034)),
% 59.77/59.74 inference(rename_variables,[],[4259])).
% 59.77/59.74 cnf(4406,plain,
% 59.77/59.74 (P8(x44061,x44062,x44063,x44064,x44062,x44061,x44063,x44064)),
% 59.77/59.74 inference(rename_variables,[],[4259])).
% 59.77/59.74 cnf(4409,plain,
% 59.77/59.74 (P6(f6(x44091,x44091,x44091),x44091,x44091)),
% 59.77/59.74 inference(rename_variables,[],[4355])).
% 59.77/59.74 cnf(4416,plain,
% 59.77/59.74 (P4(f6(x44161,x44161,x44161),x44161,f6(x44161,x44161,x44161),x44161)),
% 59.77/59.74 inference(scs_inference,[],[4259,4403,4355,4409,4369,4337,1468,1732,1694,1688,170,173])).
% 59.77/59.74 cnf(4418,plain,
% 59.77/59.74 (P7(a24,x44181,a24,x44181,x44181,x44181,x44181,x44181)),
% 59.77/59.74 inference(scs_inference,[],[4259,4403,4314,4355,4409,4369,4337,1468,1732,1694,1688,170,173,276])).
% 59.77/59.74 cnf(4422,plain,
% 59.77/59.74 (P7(x44221,a24,x44221,x44221,a24,x44221,x44221,x44221)),
% 59.77/59.74 inference(scs_inference,[],[4259,4403,4314,4355,4409,4369,4337,4106,1468,1732,1694,1688,170,173,276,184,275])).
% 59.77/59.74 cnf(4424,plain,
% 59.77/59.74 (P6(f46(x44241,x44242),x44242,x44241)),
% 59.77/59.74 inference(scs_inference,[],[4259,4403,4314,4355,4409,4369,4337,4106,1468,1732,1694,1688,170,173,276,184,275,171])).
% 59.77/59.74 cnf(4426,plain,
% 59.77/59.74 (P7(a36,a16,a16,a16,a16,a36,a16,a16)),
% 59.77/59.74 inference(scs_inference,[],[4259,4403,4314,4241,4355,4409,4369,4337,4106,1468,1732,1694,1688,170,173,276,184,275,171,273])).
% 59.77/59.74 cnf(4430,plain,
% 59.77/59.74 (P8(a24,x44301,x44301,x44301,x44301,x44301,a24,x44301)),
% 59.77/59.74 inference(scs_inference,[],[4259,4403,4314,4234,4241,4355,4409,4369,4337,4106,1468,1732,1694,1688,170,173,276,184,275,171,273,274,243])).
% 59.77/59.74 cnf(4434,plain,
% 59.77/59.74 (P4(a24,x44341,x44341,a24)),
% 59.77/59.74 inference(scs_inference,[],[4259,4403,4314,4234,4241,4355,4409,4369,4337,4048,4106,1468,1732,1694,1688,170,173,276,184,275,171,273,274,243,180,185])).
% 59.77/59.74 cnf(4436,plain,
% 59.77/59.74 (P10(x44361,x44361,f12(x44362,x44362,x44362,x44361,x44361),x44362)),
% 59.77/59.74 inference(scs_inference,[],[4259,4403,4314,4234,4241,4355,4409,4316,4369,4337,4048,4106,1468,1732,1694,1688,170,173,276,184,275,171,273,274,243,180,185,182])).
% 59.77/59.74 cnf(4438,plain,
% 59.77/59.74 (P1(x44381,x44381,x44382)),
% 59.77/59.74 inference(scs_inference,[],[4259,4403,4269,4314,4234,4241,4355,4409,4316,4369,4337,4048,4106,1468,1732,1694,1688,170,173,276,184,275,171,273,274,243,180,185,182,169])).
% 59.77/59.74 cnf(4440,plain,
% 59.77/59.74 (P1(x44401,f5(x44402,x44402,x44401),x44402)),
% 59.77/59.74 inference(scs_inference,[],[4259,4403,4269,4314,4234,4241,4355,4409,4316,4324,4369,4337,4048,4106,1468,1732,1694,1688,170,173,276,184,275,171,273,274,243,180,185,182,169,168])).
% 59.77/59.74 cnf(4444,plain,
% 59.77/59.74 (P8(f49(a24,a24,a24,a24,a24),a24,x44441,x44442,a24,a24,x44441,x44442)),
% 59.77/59.74 inference(scs_inference,[],[4259,4403,4269,4314,4234,4241,4355,4409,4316,4324,4369,4337,4048,4106,4210,1468,1732,1694,1688,170,173,276,184,275,171,273,274,243,180,185,182,169,168,181,242])).
% 59.77/59.74 cnf(4450,plain,
% 59.77/59.74 (P3(a24,a16,a16,a22)),
% 59.77/59.74 inference(scs_inference,[],[4259,4403,4269,4314,4234,4241,4277,4355,4409,4316,4322,4324,4369,4337,4048,4106,4210,163,1468,1732,1694,1688,170,173,276,184,275,171,273,274,243,180,185,182,169,168,181,242,204,183,188])).
% 59.77/59.74 cnf(4452,plain,
% 59.77/59.74 (P8(x44521,x44522,x44523,x44524,x44521,x44522,x44524,x44523)),
% 59.77/59.74 inference(scs_inference,[],[4259,4403,4406,4269,4314,4234,4241,4277,4355,4409,4316,4322,4324,4369,4337,4048,4106,4210,163,1468,1732,1694,1688,170,173,276,184,275,171,273,274,243,180,185,182,169,168,181,242,204,183,188,270])).
% 59.77/59.74 cnf(4454,plain,
% 59.77/59.74 (P8(x44541,x44542,x44542,x44541,x44543,x44544,x44543,x44544)),
% 59.77/59.74 inference(scs_inference,[],[4259,4403,4406,4281,4269,4314,4234,4241,4277,4355,4409,4316,4322,4324,4369,4337,4048,4106,4210,163,1468,1732,1694,1688,170,173,276,184,275,171,273,274,243,180,185,182,169,168,181,242,204,183,188,270,271])).
% 59.77/59.74 cnf(4456,plain,
% 59.77/59.74 (P8(a16,a21,a24,a21,a16,a16,a24,a16)),
% 59.77/59.74 inference(scs_inference,[],[4259,4403,4406,4281,4269,4285,4314,4234,4241,4277,4355,4409,4316,4322,4324,4369,4337,4048,4106,4210,163,1468,1732,1694,1688,170,173,276,184,275,171,273,274,243,180,185,182,169,168,181,242,204,183,188,270,271,272])).
% 59.77/59.74 cnf(4458,plain,
% 59.77/59.74 (P8(a16,a16,a16,a21,a24,a16,a24,a21)),
% 59.77/59.74 inference(scs_inference,[],[4259,4403,4406,4281,4269,4285,4124,4314,4234,4241,4277,4355,4409,4316,4322,4324,4369,4337,4048,4106,4210,163,1468,1732,1694,1688,170,173,276,184,275,171,273,274,243,180,185,182,169,168,181,242,204,183,188,270,271,272,241])).
% 59.77/59.74 cnf(4464,plain,
% 59.77/59.74 (P3(x44641,x44642,x44641,x44641)),
% 59.77/59.74 inference(scs_inference,[],[4259,4403,4406,4281,4339,4269,4285,4124,4314,4230,4234,4138,4241,4277,4355,4409,4316,4322,4324,4369,4337,4048,4106,4210,163,1468,1732,1694,1688,170,173,276,184,275,171,273,274,243,180,185,182,169,168,181,242,204,183,188,270,271,272,241,187,269,186])).
% 59.77/59.74 cnf(4466,plain,
% 59.77/59.74 (P1(x44661,a24,f3(x44661,x44661,a24))),
% 59.77/59.74 inference(scs_inference,[],[4259,4403,4406,4275,4281,4339,4269,4285,4124,4314,4230,4234,4138,4241,4277,4355,4409,4316,4322,4324,4369,4337,4048,4106,4210,163,1468,1732,1694,1688,170,173,276,184,275,171,273,274,243,180,185,182,169,168,181,242,204,183,188,270,271,272,241,187,269,186,193])).
% 59.77/59.74 cnf(4467,plain,
% 59.77/59.74 (P10(x44671,x44672,x44672,x44671)),
% 59.77/59.74 inference(rename_variables,[],[4275])).
% 59.77/59.74 cnf(4471,plain,
% 59.77/59.74 (P8(x44711,x44712,x44713,x44714,x44712,x44711,x44713,x44714)),
% 59.77/59.74 inference(rename_variables,[],[4259])).
% 59.77/59.74 cnf(4473,plain,
% 59.77/59.74 (P4(x44731,x44732,x44731,f49(a24,x44731,x44732,x44732,a24))),
% 59.77/59.74 inference(scs_inference,[],[4259,4403,4406,4275,4467,4281,4339,4269,4285,4124,4314,4230,4234,4138,4241,4277,4355,4409,4316,4322,4324,4369,4337,4048,4106,4210,163,1468,1732,1694,1688,170,173,276,184,275,171,273,274,243,180,185,182,169,168,181,242,204,183,188,270,271,272,241,187,269,186,193,258,217])).
% 59.77/59.74 cnf(4474,plain,
% 59.77/59.74 (P10(x44741,x44742,x44742,x44741)),
% 59.77/59.74 inference(rename_variables,[],[4275])).
% 59.77/59.74 cnf(4476,plain,
% 59.77/59.74 (P1(f23(x44761,x44761,a24,x44761),a24,x44761)),
% 59.77/59.74 inference(scs_inference,[],[4259,4403,4406,4471,4275,4467,4281,4339,4269,4285,4124,4314,4230,4234,4138,4241,4277,4355,4409,4316,4322,4324,4369,4337,4048,4106,4210,163,1468,1732,1694,1688,170,173,276,184,275,171,273,274,243,180,185,182,169,168,181,242,204,183,188,270,271,272,241,187,269,186,193,258,217,266])).
% 59.77/59.74 cnf(4477,plain,
% 59.77/59.74 (P4(a24,x44771,a24,x44771)),
% 59.77/59.74 inference(rename_variables,[],[4234])).
% 59.77/59.74 cnf(4478,plain,
% 59.77/59.74 (P8(x44781,x44782,x44783,x44784,x44782,x44781,x44783,x44784)),
% 59.77/59.74 inference(rename_variables,[],[4259])).
% 59.77/59.74 cnf(4481,plain,
% 59.77/59.74 (P10(x44811,x44812,x44812,x44811)),
% 59.77/59.74 inference(rename_variables,[],[4275])).
% 59.77/59.74 cnf(4484,plain,
% 59.77/59.74 (P10(x44841,x44842,x44842,x44841)),
% 59.77/59.74 inference(rename_variables,[],[4275])).
% 59.77/59.74 cnf(4487,plain,
% 59.77/59.74 (P10(x44871,x44872,x44872,x44871)),
% 59.77/59.74 inference(rename_variables,[],[4275])).
% 59.77/59.74 cnf(4489,plain,
% 59.77/59.74 (P9(f49(a24,x44891,x44892,x44892,a24),x44892,a24,x44891)),
% 59.77/59.74 inference(scs_inference,[],[142,4259,4403,4406,4471,4275,4467,4474,4481,4484,4487,4281,4339,4269,4285,4124,4314,4230,4234,4477,4138,4241,4277,4355,4409,4316,4322,4324,4369,4337,4048,4106,4210,163,1468,1732,1694,1688,170,173,276,184,275,171,273,274,243,180,185,182,169,168,181,242,204,183,188,270,271,272,241,187,269,186,193,258,217,266,216,205,214,218])).
% 59.77/59.74 cnf(4490,plain,
% 59.77/59.74 (P10(x44901,x44902,x44902,x44901)),
% 59.77/59.74 inference(rename_variables,[],[4275])).
% 59.77/59.74 cnf(4495,plain,
% 59.77/59.74 (P10(x44951,x44952,x44952,x44951)),
% 59.77/59.74 inference(rename_variables,[],[4275])).
% 59.77/59.74 cnf(4497,plain,
% 59.77/59.74 (P9(a24,f49(a24,a24,a24,a24,a24),a24,a24)),
% 59.77/59.74 inference(scs_inference,[],[142,4259,4403,4406,4471,4478,4275,4467,4474,4481,4484,4487,4490,4281,4339,4269,4285,4124,4314,4230,4234,4477,4138,4241,4277,4355,4409,4316,4322,4324,4369,4347,4337,4048,4106,4210,163,1468,1732,1694,1688,170,173,276,184,275,171,273,274,243,180,185,182,169,168,181,242,204,183,188,270,271,272,241,187,269,186,193,258,217,266,216,205,214,218,240,190,257])).
% 59.77/59.74 cnf(4498,plain,
% 59.77/59.74 (P8(x44981,x44982,x44983,x44984,x44982,x44981,x44983,x44984)),
% 59.77/59.74 inference(rename_variables,[],[4259])).
% 59.77/59.74 cnf(4501,plain,
% 59.77/59.74 (P3(x45011,x45012,x45012,x45012)),
% 59.77/59.74 inference(rename_variables,[],[4339])).
% 59.77/59.74 cnf(4502,plain,
% 59.77/59.74 (P10(x45021,x45022,x45022,x45021)),
% 59.77/59.74 inference(rename_variables,[],[4275])).
% 59.77/59.74 cnf(4505,plain,
% 59.77/59.74 (P2(f9(x45051,x45051,x45051),x45051,x45051,x45051)),
% 59.77/59.74 inference(rename_variables,[],[4343])).
% 59.77/59.74 cnf(4508,plain,
% 59.77/59.74 (P10(x45081,x45082,x45082,x45081)),
% 59.77/59.74 inference(rename_variables,[],[4275])).
% 59.77/59.74 cnf(4510,plain,
% 59.77/59.74 (P2(a24,x45101,x45101,x45101)),
% 59.77/59.74 inference(scs_inference,[],[142,4259,4403,4406,4471,4478,4275,4467,4474,4481,4484,4487,4490,4495,4502,4281,4339,4269,4285,4124,4314,4230,4234,4477,4138,4241,4277,4343,4355,4409,4316,4322,4324,4369,4347,4337,4048,4106,4210,163,1468,1732,1694,1688,170,173,276,184,275,171,273,274,243,180,185,182,169,168,181,242,204,183,188,270,271,272,241,187,269,186,193,258,217,266,216,205,214,218,240,190,257,208,244,215,201])).
% 59.77/59.74 cnf(4512,plain,
% 59.77/59.74 (P10(a24,a24,x45121,x45121)),
% 59.77/59.74 inference(scs_inference,[],[142,4259,4403,4406,4471,4478,4275,4467,4474,4481,4484,4487,4490,4495,4502,4281,4339,4269,4285,4124,4314,4230,4234,4477,4138,4241,4277,4343,4355,4409,4316,4322,4324,4369,4347,4337,4048,4106,4210,163,1468,1732,1694,1688,170,173,276,184,275,171,273,274,243,180,185,182,169,168,181,242,204,183,188,270,271,272,241,187,269,186,193,258,217,266,216,205,214,218,240,190,257,208,244,215,201,198])).
% 59.77/59.74 cnf(4517,plain,
% 59.77/59.74 (P3(a15,a15,a1,a2)),
% 59.77/59.74 inference(scs_inference,[],[142,4259,4403,4406,4471,4478,4275,4467,4474,4481,4484,4487,4490,4495,4502,4508,4281,4339,4269,4285,4124,4314,4230,4234,4477,4138,4241,4277,4343,4355,4409,4316,4322,4324,4369,4347,4337,4048,4106,4210,163,1468,1732,1694,1688,170,173,276,184,275,171,273,274,243,180,185,182,169,168,181,242,204,183,188,270,271,272,241,187,269,186,193,258,217,266,216,205,214,218,240,190,257,208,244,215,201,198,194,253])).
% 59.77/59.74 cnf(4518,plain,
% 59.77/59.74 (P8(x45181,x45182,x45181,x45182,x45183,x45184,x45183,x45184)),
% 59.77/59.74 inference(rename_variables,[],[4281])).
% 59.77/59.74 cnf(4520,plain,
% 59.77/59.74 (P6(x45201,x45201,x45201)),
% 59.77/59.74 inference(scs_inference,[],[142,4259,4403,4406,4471,4478,4275,4467,4474,4481,4484,4487,4490,4495,4502,4508,4281,4518,4339,4269,4285,4124,4314,4230,4234,4477,4138,4241,4277,4343,4505,4355,4409,4316,4322,4324,4369,4347,4337,4048,4106,4210,163,1468,1732,1694,1688,170,173,276,184,275,171,273,274,243,180,185,182,169,168,181,242,204,183,188,270,271,272,241,187,269,186,193,258,217,266,216,205,214,218,240,190,257,208,244,215,201,198,194,253,256])).
% 59.77/59.74 cnf(4525,plain,
% 59.77/59.74 (P4(x45251,x45251,x45251,x45251)),
% 59.77/59.74 inference(scs_inference,[],[142,4259,4403,4406,4471,4478,4498,4275,4467,4474,4481,4484,4487,4490,4495,4502,4508,4281,4518,4339,4501,4269,4285,4124,4314,4230,4234,4477,4138,4241,4277,4343,4505,4355,4409,4316,4322,4324,4369,4347,4337,4048,4106,4210,163,1468,1732,1694,1688,170,173,276,184,275,171,273,274,243,180,185,182,169,168,181,242,204,183,188,270,271,272,241,187,269,186,193,258,217,266,216,205,214,218,240,190,257,208,244,215,201,198,194,253,256,268])).
% 59.77/59.74 cnf(4557,plain,
% 59.77/59.74 (P8(x45571,x45572,x45573,x45574,x45571,x45572,x45574,x45573)),
% 59.77/59.74 inference(rename_variables,[],[4452])).
% 59.77/59.74 cnf(4560,plain,
% 59.77/59.74 (P8(x45601,x45602,x45603,x45604,x45601,x45602,x45604,x45603)),
% 59.77/59.74 inference(rename_variables,[],[4452])).
% 59.77/59.74 cnf(4563,plain,
% 59.77/59.74 (P8(x45631,x45632,x45633,x45634,x45631,x45632,x45634,x45633)),
% 59.77/59.74 inference(rename_variables,[],[4452])).
% 59.77/59.74 cnf(4565,plain,
% 59.77/59.74 (P6(a16,a24,a24)),
% 59.77/59.74 inference(scs_inference,[],[4520,4452,4557,4560,1732,1782,1468,1694])).
% 59.77/59.74 cnf(4566,plain,
% 59.77/59.74 (P6(x45661,x45661,x45661)),
% 59.77/59.74 inference(rename_variables,[],[4520])).
% 59.77/59.74 cnf(4570,plain,
% 59.77/59.74 (P6(f3(a24,a24,a24),a16,a16)),
% 59.77/59.74 inference(scs_inference,[],[4520,4452,4557,4560,4434,4351,1732,1782,1468,1694,184,1688])).
% 59.77/59.74 cnf(4574,plain,
% 59.77/59.74 (P7(x45741,a24,a24,x45741,x45741,x45741,x45741,x45741)),
% 59.77/59.74 inference(scs_inference,[],[4520,4452,4557,4560,4422,4434,4424,4351,1732,1782,1468,1694,184,1688,170,276])).
% 59.77/59.74 cnf(4578,plain,
% 59.77/59.74 (P7(a16,a36,a36,a16,a16,a16,a16,a16)),
% 59.77/59.74 inference(scs_inference,[],[4520,4452,4557,4560,4422,4434,4249,4424,4351,1732,1782,1468,1694,184,1688,170,276,173,275])).
% 59.77/59.74 cnf(4584,plain,
% 59.77/59.74 (P6(a24,f7(a16,a25,a30,a24),f4(a16,a16,a24))),
% 59.77/59.74 inference(scs_inference,[],[4520,4452,4557,4560,4418,4422,4434,4249,4424,4308,4360,4351,1732,1782,1468,1694,184,1688,170,276,173,275,273,180,171])).
% 59.77/59.74 cnf(4586,plain,
% 59.77/59.74 (P1(f4(x45861,x45861,x45862),x45861,x45862)),
% 59.77/59.74 inference(scs_inference,[],[4520,4452,4557,4560,4418,4422,4434,4249,4335,4424,4308,4360,4351,1732,1782,1468,1694,184,1688,170,276,173,275,273,180,171,169])).
% 59.77/59.74 cnf(4588,plain,
% 59.77/59.74 (P7(x45881,x45881,x45881,a24,x45881,x45881,a24,x45881)),
% 59.77/59.74 inference(scs_inference,[],[4520,4452,4557,4560,4418,4422,4434,4249,4335,4424,4308,4360,4351,1732,1782,1468,1694,184,1688,170,276,173,275,273,180,171,169,274])).
% 59.77/59.74 cnf(4590,plain,
% 59.77/59.74 (P1(x45901,f4(x45902,x45902,x45901),x45902)),
% 59.77/59.74 inference(scs_inference,[],[4520,4452,4557,4560,4418,4422,4434,4249,4335,4424,4308,4360,4351,1732,1782,1468,1694,184,1688,170,276,173,275,273,180,171,169,274,168])).
% 59.77/59.74 cnf(4592,plain,
% 59.77/59.74 (P10(x45921,x45921,a24,a24)),
% 59.77/59.74 inference(scs_inference,[],[4520,4452,4557,4560,4418,4422,4434,4512,4249,4335,4424,4308,4360,4351,1732,1782,1468,1694,184,1688,170,276,173,275,273,180,171,169,274,168,182])).
% 59.77/59.74 cnf(4600,plain,
% 59.77/59.74 (P10(f7(x46001,x46001,x46001,a24),x46001,x46001,a24)),
% 59.77/59.74 inference(scs_inference,[],[4520,4452,4557,4560,4418,4422,4510,4434,4512,4249,4416,4335,4424,4308,4489,4360,4351,1732,1782,1468,1694,184,1688,170,276,173,275,273,180,171,169,274,168,182,185,243,181,204])).
% 59.77/59.74 cnf(4604,plain,
% 59.77/59.74 (P3(a15,a15,a2,a1)),
% 59.77/59.74 inference(scs_inference,[],[4520,4452,4557,4560,4418,4422,4510,4517,4434,4512,4249,4416,4335,4424,4308,4489,4360,4351,1732,1782,1468,1694,184,1688,170,276,173,275,273,180,171,169,274,168,182,185,243,181,204,242,188])).
% 59.77/59.74 cnf(4608,plain,
% 59.77/59.74 (P8(x46081,x46082,x46083,x46084,x46082,x46081,x46084,x46083)),
% 59.77/59.74 inference(scs_inference,[],[4520,4452,4557,4560,4563,4418,4422,4510,4517,4434,4512,4249,4416,4436,4335,4424,4308,4489,4360,4351,1732,1782,1468,1694,184,1688,170,276,173,275,273,180,171,169,274,168,182,185,243,181,204,242,188,183,271])).
% 59.77/59.74 cnf(4610,plain,
% 59.77/59.74 (P8(x46101,x46102,x46101,x46102,x46103,x46104,x46104,x46103)),
% 59.77/59.74 inference(scs_inference,[],[4520,4452,4557,4560,4563,4418,4422,4510,4517,4434,4512,4249,4416,4436,4335,4424,4308,4489,4360,4351,1732,1782,1468,1694,184,1688,170,276,173,275,273,180,171,169,274,168,182,185,243,181,204,242,188,183,271,272])).
% 59.77/59.74 cnf(4614,plain,
% 59.77/59.74 (P3(x46141,x46141,x46142,x46141)),
% 59.77/59.74 inference(scs_inference,[],[4520,4452,4557,4560,4563,4464,4418,4422,4430,4510,4517,4434,4512,4249,4416,4436,4335,4424,4308,4489,4360,4351,1732,1782,1468,1694,184,1688,170,276,173,275,273,180,171,169,274,168,182,185,243,181,204,242,188,183,271,272,270,187])).
% 59.77/59.74 cnf(4616,plain,
% 59.77/59.74 (P8(a21,a16,a21,a24,a16,a16,a16,a24)),
% 59.77/59.74 inference(scs_inference,[],[4520,4452,4557,4560,4563,4464,4418,4422,4430,4510,4517,4434,4512,4130,4249,4416,4436,4335,4424,4308,4489,4360,4351,1732,1782,1468,1694,184,1688,170,276,173,275,273,180,171,169,274,168,182,185,243,181,204,242,188,183,271,272,270,187,269])).
% 59.77/59.74 cnf(4618,plain,
% 59.77/59.74 (P8(a16,a24,a16,a16,a22,a24,a22,a16)),
% 59.77/59.74 inference(scs_inference,[],[4520,4452,4557,4560,4563,4464,4418,4422,4430,4510,4517,4434,4512,4130,4249,4450,4416,4436,4335,4424,4308,4489,4360,4351,1732,1782,1468,1694,184,1688,170,276,173,275,273,180,171,169,274,168,182,185,243,181,204,242,188,183,271,272,270,187,269,241])).
% 59.77/59.74 cnf(4620,plain,
% 59.77/59.74 (P3(a16,a24,a16,a22)),
% 59.77/59.74 inference(scs_inference,[],[4520,4452,4557,4560,4563,4464,4418,4422,4430,4510,4517,4434,4512,4130,4249,4450,4416,4436,4335,4424,4308,4489,4360,4351,1732,1782,1468,1694,184,1688,170,276,173,275,273,180,171,169,274,168,182,185,243,181,204,242,188,183,271,272,270,187,269,241,186])).
% 59.77/59.74 cnf(4626,plain,
% 59.77/59.74 (P9(x46261,f46(x46262,x46261),x46262,f46(x46262,x46261))),
% 59.77/59.74 inference(scs_inference,[],[4520,4566,4452,4557,4560,4563,4454,4464,4418,4422,4430,4510,4517,4434,4512,4130,4249,4450,4416,4436,4335,4424,4308,4489,4360,4351,1732,1782,1468,1694,184,1688,170,276,173,275,273,180,171,169,274,168,182,185,243,181,204,242,188,183,271,272,270,187,269,241,186,279,174])).
% 59.77/59.74 cnf(4627,plain,
% 59.77/59.74 (P6(x46271,x46271,x46271)),
% 59.77/59.74 inference(rename_variables,[],[4520])).
% 59.77/59.74 cnf(4629,plain,
% 59.77/59.74 (P9(f46(x46291,x46292),x46292,x46291,x46292)),
% 59.77/59.74 inference(scs_inference,[],[4520,4566,4627,4452,4557,4560,4563,4454,4464,4418,4422,4430,4510,4517,4434,4512,4130,4249,4450,4416,4436,4335,4424,4308,4489,4360,4351,1732,1782,1468,1694,184,1688,170,276,173,275,273,180,171,169,274,168,182,185,243,181,204,242,188,183,271,272,270,187,269,241,186,279,174,175])).
% 59.77/59.74 cnf(4630,plain,
% 59.77/59.74 (P6(f46(x46301,x46302),x46302,x46301)),
% 59.77/59.74 inference(rename_variables,[],[4424])).
% 59.77/59.74 cnf(4633,plain,
% 59.77/59.74 (P1(x46331,x46331,x46332)),
% 59.77/59.74 inference(rename_variables,[],[4438])).
% 59.77/59.74 cnf(4634,plain,
% 59.77/59.74 (P10(a24,a24,x46341,x46341)),
% 59.77/59.74 inference(rename_variables,[],[4512])).
% 59.77/59.74 cnf(4637,plain,
% 59.77/59.74 (P8(f49(a24,a24,a24,a24,a24),a24,x46371,x46372,a24,a24,x46371,x46372)),
% 59.77/59.74 inference(rename_variables,[],[4444])).
% 59.77/59.74 cnf(4639,plain,
% 59.77/59.74 (P9(f47(x46391,x46391,x46391,x46391,x46391,x46391),x46391,x46391,x46391)),
% 59.77/59.74 inference(scs_inference,[],[4520,4566,4627,4452,4557,4560,4563,4454,4464,4438,4418,4422,4430,4510,4517,4434,4512,4634,4130,4249,4450,4416,4436,4335,4424,4308,4489,4444,4360,4351,1732,1782,1468,1694,184,1688,170,276,173,275,273,180,171,169,274,168,182,185,243,181,204,242,188,183,271,272,270,187,269,241,186,279,174,175,214,258,222])).
% 59.77/59.74 cnf(4648,plain,
% 59.77/59.74 (P4(f12(x46481,x46481,x46481,x46481,x46481),x46481,f12(x46481,x46481,x46481,x46481,x46481),x46481)),
% 59.77/59.74 inference(scs_inference,[],[4520,4566,4627,4452,4557,4560,4563,4454,4464,4438,4418,4422,4430,4510,4517,4434,4512,4634,4130,4249,4450,4416,4436,4335,4424,4308,4489,4444,4637,4360,4263,4351,4316,4181,1732,1782,1468,1694,184,1688,170,276,173,275,273,180,171,169,274,168,182,185,243,181,204,242,188,183,271,272,270,187,269,241,186,279,174,175,214,258,222,221,257,240,190])).
% 59.77/59.74 cnf(4655,plain,
% 59.77/59.74 (P1(x46551,x46551,x46552)),
% 59.77/59.74 inference(rename_variables,[],[4438])).
% 59.77/59.74 cnf(4658,plain,
% 59.77/59.74 (P2(x46581,x46581,x46581,x46581)),
% 59.77/59.74 inference(scs_inference,[],[4525,4520,4566,4627,4452,4557,4560,4563,4454,4464,4438,4633,4418,4422,4430,4510,4517,4434,4512,4634,4130,4249,4450,4416,4436,4335,4424,4630,4308,4489,4444,4637,4360,4263,4351,4316,4181,1732,1782,1468,1694,184,1688,170,276,173,275,273,180,171,169,274,168,182,185,243,181,204,242,188,183,271,272,270,187,269,241,186,279,174,175,214,258,222,221,257,240,190,244,215,201])).
% 59.77/59.74 cnf(4660,plain,
% 59.77/59.74 (P10(f6(x46601,x46601,x46601),f6(x46601,x46601,x46601),f6(x46601,x46601,x46601),x46601)),
% 59.77/59.74 inference(scs_inference,[],[4525,4520,4566,4627,4452,4557,4560,4563,4454,4464,4438,4633,4418,4422,4430,4510,4517,4434,4512,4634,4130,4249,4450,4416,4436,4335,4424,4630,4308,4489,4444,4637,4360,4263,4351,4316,4181,1732,1782,1468,1694,184,1688,170,276,173,275,273,180,171,169,274,168,182,185,243,181,204,242,188,183,271,272,270,187,269,241,186,279,174,175,214,258,222,221,257,240,190,244,215,201,198])).
% 59.77/59.74 cnf(4661,plain,
% 59.77/59.74 (P4(x46611,x46611,x46611,x46611)),
% 59.77/59.74 inference(rename_variables,[],[4525])).
% 59.77/59.74 cnf(4663,plain,
% 59.77/59.74 (P6(f47(x46631,x46631,x46631,x46631,x46631,x46631),x46631,x46631)),
% 59.77/59.74 inference(scs_inference,[],[4525,4520,4566,4627,4452,4557,4560,4563,4454,4464,4438,4633,4418,4422,4430,4510,4517,4434,4512,4634,4130,4249,4450,4416,4436,4335,4424,4630,4308,4489,4444,4637,4360,4263,4351,4316,4181,1732,1782,1468,1694,184,1688,170,276,173,275,273,180,171,169,274,168,182,185,243,181,204,242,188,183,271,272,270,187,269,241,186,279,174,175,214,258,222,221,257,240,190,244,215,201,198,220])).
% 59.77/59.74 cnf(4665,plain,
% 59.77/59.74 (P9(x46651,x46651,x46652,f12(x46652,x46652,x46652,x46651,x46651))),
% 59.77/59.74 inference(scs_inference,[],[4525,4520,4566,4627,4452,4557,4560,4563,4454,4464,4438,4633,4418,4422,4430,4510,4517,4434,4512,4634,4130,4249,4450,4416,4436,4335,4424,4630,4308,4489,4444,4637,4360,4263,4351,4275,4316,4181,1732,1782,1468,1694,184,1688,170,276,173,275,273,180,171,169,274,168,182,185,243,181,204,242,188,183,271,272,270,187,269,241,186,279,174,175,214,258,222,221,257,240,190,244,215,201,198,220,197])).
% 59.77/59.74 cnf(4667,plain,
% 59.77/59.74 (P10(x46671,x46672,x46672,x46671)),
% 59.77/59.74 inference(rename_variables,[],[4275])).
% 59.77/59.74 cnf(4672,plain,
% 59.77/59.74 (P3(x46721,x46722,x46723,x46723)),
% 59.77/59.74 inference(scs_inference,[],[4525,4520,4566,4627,4452,4557,4560,4563,4454,4464,4438,4633,4655,4418,4422,4430,4510,4517,4434,4512,4634,4130,4249,4450,4416,4436,4335,4424,4630,4308,4489,4444,4637,4360,4263,4351,4275,4316,4110,4181,1732,1782,1468,1694,184,1688,170,276,173,275,273,180,171,169,274,168,182,185,243,181,204,242,188,183,271,272,270,187,269,241,186,279,174,175,214,258,222,221,257,240,190,244,215,201,198,220,197,196,253])).
% 59.77/59.74 cnf(4675,plain,
% 59.77/59.74 (P6(f3(a24,a24,a24),f3(a24,a24,a24),a24)),
% 59.77/59.74 inference(scs_inference,[],[4525,4520,4566,4627,4452,4557,4560,4563,4454,4464,4438,4633,4655,4418,4422,4430,4510,4517,4434,4512,4634,4130,4249,4450,4416,4436,4335,4424,4630,4251,4308,4489,4444,4637,4360,4263,4351,4245,4275,4316,4110,4181,1732,1782,1468,1694,184,1688,170,276,173,275,273,180,171,169,274,168,182,185,243,181,204,242,188,183,271,272,270,187,269,241,186,279,174,175,214,258,222,221,257,240,190,244,215,201,198,220,197,196,253,179])).
% 59.77/59.74 cnf(4676,plain,
% 59.77/59.74 (P1(x46761,x46761,x46762)),
% 59.77/59.74 inference(rename_variables,[],[4438])).
% 59.77/59.74 cnf(4678,plain,
% 59.77/59.74 (P4(a16,a16,a24,a24)),
% 59.77/59.74 inference(scs_inference,[],[4525,4520,4566,4627,4452,4557,4560,4563,4454,4464,4438,4633,4655,4273,4418,4422,4430,4510,4517,4434,4512,4634,4130,4249,4450,4416,4436,4335,4424,4630,4251,4308,4489,4444,4637,4360,4263,4351,4245,4275,4281,4316,4110,4181,1732,1782,1468,1694,184,1688,170,276,173,275,273,180,171,169,274,168,182,185,243,181,204,242,188,183,271,272,270,187,269,241,186,279,174,175,214,258,222,221,257,240,190,244,215,201,198,220,197,196,253,179,268])).
% 59.77/59.74 cnf(4689,plain,
% 59.77/59.74 (P10(x46891,x46892,x46892,x46891)),
% 59.77/59.74 inference(rename_variables,[],[4275])).
% 59.77/59.74 cnf(4691,plain,
% 59.77/59.74 (P9(f49(x46911,x46912,x46911,x46911,x46911),x46911,x46911,x46912)),
% 59.77/59.74 inference(scs_inference,[],[142,4525,4661,4520,4566,4627,4452,4557,4560,4563,4454,4464,4438,4633,4655,4676,4273,4418,4422,4430,4510,4517,4434,4512,4634,4130,4134,4249,4450,4416,4436,4335,4424,4630,4251,4308,4489,4444,4637,4360,4263,4351,4245,4275,4667,4689,4281,4269,4316,4100,4110,4181,1732,1782,1468,1694,184,1688,170,276,173,275,273,180,171,169,274,168,182,185,243,181,204,242,188,183,271,272,270,187,269,241,186,279,174,175,214,258,222,221,257,240,190,244,215,201,198,220,197,196,253,179,268,223,261,216,218])).
% 59.77/59.74 cnf(4692,plain,
% 59.77/59.74 (P10(x46921,x46922,x46922,x46921)),
% 59.77/59.74 inference(rename_variables,[],[4275])).
% 59.77/59.74 cnf(4697,plain,
% 59.77/59.74 (P10(x46971,f6(x46971,x46971,x46971),f6(x46971,x46971,x46971),f6(x46971,x46971,x46971))),
% 59.77/59.74 inference(scs_inference,[],[142,4525,4661,4520,4566,4627,4452,4557,4560,4563,4454,4464,4438,4633,4655,4676,4273,4418,4422,4430,4510,4517,4434,4512,4634,4130,4134,4249,4450,4416,4436,4335,4424,4630,4251,4308,4489,4444,4637,4360,4263,4351,4245,4275,4667,4689,4692,4281,4269,4316,4100,4110,4181,1732,1782,1468,1694,184,1688,170,276,173,275,273,180,171,169,274,168,182,185,243,181,204,242,188,183,271,272,270,187,269,241,186,279,174,175,214,258,222,221,257,240,190,244,215,201,198,220,197,196,253,179,268,223,261,216,218,208,212])).
% 59.77/59.74 cnf(4705,plain,
% 59.77/59.74 (P3(x47051,x47052,x47053,x47053)),
% 59.77/59.74 inference(rename_variables,[],[4672])).
% 59.77/59.74 cnf(4707,plain,
% 59.77/59.74 (P8(x47071,x47072,x47073,x47074,x47072,x47071,x47074,x47073)),
% 59.77/59.74 inference(rename_variables,[],[4608])).
% 59.77/59.74 cnf(4710,plain,
% 59.77/59.74 (P8(x47101,x47102,x47103,x47104,x47102,x47101,x47104,x47103)),
% 59.77/59.74 inference(rename_variables,[],[4608])).
% 59.77/59.74 cnf(4713,plain,
% 59.77/59.74 (P8(x47131,x47132,x47133,x47134,x47132,x47131,x47134,x47133)),
% 59.77/59.74 inference(rename_variables,[],[4608])).
% 59.77/59.74 cnf(4720,plain,
% 59.77/59.74 (P6(f47(x47201,x47201,x47201,x47201,x47201,x47201),x47201,x47201)),
% 59.77/59.74 inference(rename_variables,[],[4663])).
% 59.77/59.74 cnf(4724,plain,
% 59.77/59.74 (P4(f47(x47241,x47241,x47241,x47241,x47241,x47241),x47241,f47(x47241,x47241,x47241,x47241,x47241,x47241),x47241)),
% 59.77/59.74 inference(scs_inference,[],[4608,4707,4710,4672,4588,4678,4663,4720,4584,4400,1782,1732,1468,276,170,1694,184,173])).
% 59.77/59.74 cnf(4728,plain,
% 59.77/59.74 (P7(x47281,x47281,a24,x47281,x47281,x47281,x47281,a24)),
% 59.77/59.74 inference(scs_inference,[],[4608,4707,4710,4672,4588,4678,4663,4720,4584,4383,4400,1782,1732,1468,276,170,1694,184,173,1688,273])).
% 59.77/59.74 cnf(4730,plain,
% 59.77/59.74 (P7(a16,a36,a16,a16,a16,a36,a16,a16)),
% 59.77/59.74 inference(scs_inference,[],[4608,4707,4710,4672,4588,4426,4678,4663,4720,4584,4383,4400,1782,1732,1468,276,170,1694,184,173,1688,273,275])).
% 59.77/59.74 cnf(4732,plain,
% 59.77/59.74 (P1(x47321,x47322,f5(x47322,x47322,x47321))),
% 59.77/59.74 inference(scs_inference,[],[4608,4707,4710,4672,4588,4426,4678,4663,4720,4440,4584,4383,4400,1782,1732,1468,276,170,1694,184,173,1688,273,275,169])).
% 59.77/59.74 cnf(4736,plain,
% 59.77/59.74 (P4(f12(x47361,x47361,x47361,x47361,x47361),x47361,x47361,f12(x47361,x47361,x47361,x47361,x47361))),
% 59.77/59.74 inference(scs_inference,[],[4608,4707,4710,4672,4588,4426,4678,4648,4660,4663,4720,4440,4584,4383,4400,1782,1732,1468,276,170,1694,184,173,1688,273,275,169,182,185])).
% 59.77/59.74 cnf(4740,plain,
% 59.77/59.74 (P9(x47401,x47401,f47(x47401,x47401,x47401,x47401,x47401,x47401),x47401)),
% 59.77/59.74 inference(scs_inference,[],[4608,4707,4710,4672,4588,4426,4678,4648,4660,4639,4663,4720,4440,4586,4584,4383,4400,1782,1732,1468,276,170,1694,184,173,1688,273,275,169,182,185,168,180])).
% 59.77/59.74 cnf(4742,plain,
% 59.77/59.74 (P7(a24,x47421,x47421,a24,x47421,x47421,x47421,x47421)),
% 59.77/59.74 inference(scs_inference,[],[4608,4707,4710,4672,4574,4588,4426,4678,4648,4660,4639,4663,4720,4440,4586,4584,4383,4400,1782,1732,1468,276,170,1694,184,173,1688,273,275,169,182,185,168,180,274])).
% 59.77/59.74 cnf(4746,plain,
% 59.77/59.74 (P8(f12(x47461,x47461,x47461,x47461,x47461),x47461,x47461,x47461,x47461,x47461,f12(x47461,x47461,x47461,x47461,x47461),x47461)),
% 59.77/59.74 inference(scs_inference,[],[4608,4707,4710,4672,4574,4588,4426,4678,4648,4660,4639,4663,4720,4440,4586,4675,4584,4383,4400,1782,1732,1468,276,170,1694,184,173,1688,273,275,169,182,185,168,180,274,171,243])).
% 59.77/59.74 cnf(4750,plain,
% 59.77/59.74 (P3(x47501,x47501,x47501,x47502)),
% 59.77/59.74 inference(scs_inference,[],[4658,4608,4707,4710,4614,4672,4574,4588,4426,4678,4648,4660,4639,4663,4720,4440,4586,4675,4584,4383,4400,1782,1732,1468,276,170,1694,184,173,1688,273,275,169,182,185,168,180,274,171,243,204,188])).
% 59.77/59.74 cnf(4752,plain,
% 59.77/59.74 (P9(x47521,x47521,f12(x47522,x47522,x47522,x47521,x47521),x47522)),
% 59.77/59.74 inference(scs_inference,[],[4658,4608,4707,4710,4614,4672,4574,4588,4426,4678,4648,4660,4639,4663,4720,4665,4440,4586,4675,4584,4383,4400,1782,1732,1468,276,170,1694,184,173,1688,273,275,169,182,185,168,180,274,171,243,204,188,181])).
% 59.77/59.74 cnf(4754,plain,
% 59.77/59.74 (P8(a21,a24,a24,a16,a16,a21,a16,a16)),
% 59.77/59.74 inference(scs_inference,[],[4658,4608,4707,4710,4614,4672,4032,4574,4588,4426,4678,4648,4660,4639,4663,4720,4665,4440,4586,4675,4584,4383,4400,1782,1732,1468,276,170,1694,184,173,1688,273,275,169,182,185,168,180,274,171,243,204,188,181,271])).
% 59.77/59.74 cnf(4756,plain,
% 59.77/59.74 (P8(f47(x47561,x47561,x47561,x47561,x47561,x47561),x47561,x47562,x47563,x47561,x47561,x47562,x47563)),
% 59.77/59.74 inference(scs_inference,[],[4658,4608,4707,4710,4614,4672,4032,4574,4588,4426,4678,4648,4660,4639,4663,4720,4665,4440,4586,4675,4584,4383,4400,1782,1732,1468,276,170,1694,184,173,1688,273,275,169,182,185,168,180,274,171,243,204,188,181,271,242])).
% 59.77/59.74 cnf(4764,plain,
% 59.77/59.74 (P8(a16,a16,a16,a24,a22,a16,a22,a24)),
% 59.77/59.74 inference(scs_inference,[],[4658,4608,4707,4710,4614,4672,4032,4574,4588,4426,4456,4620,4678,4648,4660,4639,4663,4720,4665,4440,4586,4675,4584,4383,4400,1782,1732,1468,276,170,1694,184,173,1688,273,275,169,182,185,168,180,274,171,243,204,188,181,271,242,183,272,269,241])).
% 59.77/59.74 cnf(4770,plain,
% 59.77/59.74 (P3(x47701,x47702,x47703,x47702)),
% 59.77/59.74 inference(scs_inference,[],[4658,4608,4707,4710,4614,4672,4705,4032,4574,4588,4289,4426,4456,4620,4678,4648,4660,4639,4663,4720,4665,4440,4586,4675,4584,4383,4277,4400,1782,1732,1468,276,170,1694,184,173,1688,273,275,169,182,185,168,180,274,171,243,204,188,181,271,242,183,272,269,241,270,186,187])).
% 59.77/59.74 cnf(4772,plain,
% 59.77/59.74 (P3(x47721,x47722,x47722,x47721)),
% 59.77/59.74 inference(scs_inference,[],[4658,4608,4707,4710,4614,4672,4705,4032,4574,4588,4289,4426,4456,4620,4678,4648,4660,4639,4663,4720,4665,4440,4586,4675,4584,4383,4277,4400,1782,1732,1468,276,170,1694,184,173,1688,273,275,169,182,185,168,180,274,171,243,204,188,181,271,242,183,272,269,241,270,186,187,202])).
% 59.77/59.74 cnf(4773,plain,
% 59.77/59.74 (P3(x47731,x47732,x47733,x47733)),
% 59.77/59.74 inference(rename_variables,[],[4672])).
% 59.77/59.74 cnf(4778,plain,
% 59.77/59.74 (P8(x47781,x47782,x47783,x47784,x47782,x47781,x47784,x47783)),
% 59.77/59.74 inference(rename_variables,[],[4608])).
% 59.77/59.74 cnf(4780,plain,
% 59.77/59.74 (P1(x47801,f3(a24,a24,a24),a24)),
% 59.77/59.74 inference(scs_inference,[],[4658,4608,4707,4710,4713,4614,4672,4705,4032,4574,4588,4289,4426,4456,4565,4620,4678,4648,4660,4639,4663,4720,4665,4440,4586,4303,4675,4584,4466,4383,4438,4277,4400,1782,1732,1468,276,170,1694,184,173,1688,273,275,169,182,185,168,180,274,171,243,204,188,181,271,242,183,272,269,241,270,186,187,202,222,258,172])).
% 59.77/59.74 cnf(4781,plain,
% 59.77/59.74 (P1(x47811,x47811,x47812)),
% 59.77/59.74 inference(rename_variables,[],[4438])).
% 59.77/59.74 cnf(4785,plain,
% 59.77/59.74 (P10(x47851,x47852,x47852,x47851)),
% 59.77/59.74 inference(rename_variables,[],[4275])).
% 59.77/59.74 cnf(4787,plain,
% 59.77/59.74 (P9(x47871,f47(x47871,x47871,x47871,x47871,x47871,x47871),x47871,x47871)),
% 59.77/59.74 inference(scs_inference,[],[4658,4608,4707,4710,4713,4778,4614,4672,4705,4032,4574,4588,4592,4289,4426,4456,4565,4620,4678,4648,4660,4639,4663,4720,4665,4440,4586,4303,4675,4584,4466,4383,4438,4277,4275,4400,1782,1732,1468,276,170,1694,184,173,1688,273,275,169,182,185,168,180,274,171,243,204,188,181,271,242,183,272,269,241,270,186,187,202,222,258,172,195,257])).
% 59.77/59.74 cnf(4788,plain,
% 59.77/59.74 (P9(f47(x47881,x47881,x47881,x47881,x47881,x47881),x47881,x47881,x47881)),
% 59.77/59.74 inference(rename_variables,[],[4639])).
% 59.77/59.74 cnf(4791,plain,
% 59.77/59.74 (P7(a16,a24,a24,a24,a16,a24,a24,a24)),
% 59.77/59.74 inference(scs_inference,[],[4658,4608,4707,4710,4713,4778,4614,4672,4705,4032,4574,4588,4592,4289,4426,4456,4565,4620,4678,4648,4660,4639,4663,4720,4665,4440,4586,4303,4675,4584,4466,4383,4438,4277,4275,4400,1782,1732,1468,276,170,1694,184,173,1688,273,275,169,182,185,168,180,274,171,243,204,188,181,271,242,183,272,269,241,270,186,187,202,222,258,172,195,257,240])).
% 59.77/59.74 cnf(4796,plain,
% 59.77/59.74 (P10(x47961,x47961,a24,a24)),
% 59.77/59.74 inference(rename_variables,[],[4592])).
% 59.77/59.74 cnf(4799,plain,
% 59.77/59.74 (P10(x47991,x47992,x47992,x47991)),
% 59.77/59.74 inference(rename_variables,[],[4275])).
% 59.77/59.74 cnf(4802,plain,
% 59.77/59.74 (P10(x48021,x48022,x48022,x48021)),
% 59.77/59.74 inference(rename_variables,[],[4275])).
% 59.77/59.74 cnf(4804,plain,
% 59.77/59.74 (P8(a24,a24,a24,a24,a24,a24,a24,a16)),
% 59.77/59.74 inference(scs_inference,[],[4658,4608,4707,4710,4713,4778,4614,4672,4705,4032,4574,4588,4592,4796,4289,4426,4456,4565,4620,4678,4648,4660,4639,4788,4663,4720,4665,4440,4586,4303,4675,4584,4466,4383,4520,4438,4277,4275,4785,4799,4400,1782,1732,1468,276,170,1694,184,173,1688,273,275,169,182,185,168,180,274,171,243,204,188,181,271,242,183,272,269,241,270,186,187,202,222,258,172,195,257,240,221,199,206,207,244])).
% 59.77/59.74 cnf(4807,plain,
% 59.77/59.74 (P2(f12(x48071,x48071,x48071,x48071,x48071),x48071,x48071,x48071)),
% 59.77/59.74 inference(scs_inference,[],[4658,4608,4707,4710,4713,4778,4614,4672,4705,4032,4574,4588,4592,4796,4289,4426,4456,4565,4620,4678,4648,4660,4639,4788,4663,4720,4665,4440,4586,4303,4675,4584,4466,4383,4520,4438,4277,4275,4785,4799,4400,1782,1732,1468,276,170,1694,184,173,1688,273,275,169,182,185,168,180,274,171,243,204,188,181,271,242,183,272,269,241,270,186,187,202,222,258,172,195,257,240,221,199,206,207,244,201])).
% 59.77/59.74 cnf(4810,plain,
% 59.77/59.74 (P10(x48101,x48102,x48102,x48101)),
% 59.77/59.74 inference(rename_variables,[],[4275])).
% 59.77/59.74 cnf(4812,plain,
% 59.77/59.74 (P2(f8(x48121,x48121,x48122),x48121,x48121,x48122)),
% 59.77/59.74 inference(scs_inference,[],[4658,4608,4707,4710,4713,4778,4614,4672,4705,4032,4574,4588,4592,4796,4289,4426,4456,4565,4620,4678,4648,4660,4639,4788,4663,4720,4665,4440,4586,4303,4675,4584,4466,4383,4520,4438,4277,4275,4785,4799,4802,4810,4400,1782,1732,1468,276,170,1694,184,173,1688,273,275,169,182,185,168,180,274,171,243,204,188,181,271,242,183,272,269,241,270,186,187,202,222,258,172,195,257,240,221,199,206,207,244,201,194,208])).
% 59.77/59.74 cnf(4813,plain,
% 59.77/59.74 (P10(x48131,x48132,x48132,x48131)),
% 59.77/59.74 inference(rename_variables,[],[4275])).
% 59.77/59.74 cnf(4817,plain,
% 59.77/59.74 (P6(f47(a24,a24,a24,a24,a16,a16),a24,a24)),
% 59.77/59.74 inference(scs_inference,[],[4658,4608,4707,4710,4713,4778,4614,4672,4705,4032,4574,4588,4592,4796,4289,4426,4456,4565,4620,4678,4648,4660,4639,4788,4663,4720,4665,4440,4586,4303,4675,4584,4466,4383,4520,4438,4277,4275,4785,4799,4802,4810,4400,1782,1732,1468,276,170,1694,184,173,1688,273,275,169,182,185,168,180,274,171,243,204,188,181,271,242,183,272,269,241,270,186,187,202,222,258,172,195,257,240,221,199,206,207,244,201,194,208,198,220])).
% 59.77/59.74 cnf(4825,plain,
% 59.77/59.74 (P9(x48251,x48252,x48251,x48252)),
% 59.77/59.74 inference(rename_variables,[],[4055])).
% 59.77/59.74 cnf(4827,plain,
% 59.77/59.74 (P4(a16,a21,a16,a21)),
% 59.77/59.74 inference(scs_inference,[],[4658,4608,4707,4710,4713,4778,4614,4672,4705,4773,4032,4574,4588,4592,4796,4289,4426,4456,4458,4565,4620,4678,4648,4660,4639,4788,4663,4720,4665,4440,4586,4303,4265,4675,4584,4466,4383,4520,4438,4781,4124,4277,4275,4785,4799,4802,4810,4281,4055,4400,1782,1732,1468,276,170,1694,184,173,1688,273,275,169,182,185,168,180,274,171,243,204,188,181,271,242,183,272,269,241,270,186,187,202,222,258,172,195,257,240,221,199,206,207,244,201,194,208,198,220,253,226,268])).
% 59.77/59.74 cnf(4828,plain,
% 59.77/59.74 (P3(x48281,x48282,x48283,x48283)),
% 59.77/59.74 inference(rename_variables,[],[4672])).
% 59.77/59.74 cnf(4831,plain,
% 59.77/59.74 (~E(a32,a33)),
% 59.77/59.74 inference(scs_inference,[],[4658,4608,4707,4710,4713,4778,4614,4672,4705,4773,4828,4032,4574,4588,4592,4796,4289,4426,4456,4458,4565,4620,4678,4648,4660,4639,4788,4663,4720,4665,4440,4586,4303,4265,4675,4584,4466,4383,4520,4438,4781,4124,4277,4275,4785,4799,4802,4810,4281,4055,4400,1782,1732,1468,276,170,1694,184,173,1688,273,275,169,182,185,168,180,274,171,243,204,188,181,271,242,183,272,269,241,270,186,187,202,222,258,172,195,257,240,221,199,206,207,244,201,194,208,198,220,253,226,268,2,4222])).
% 59.77/59.74 cnf(4834,plain,
% 59.77/59.74 (P1(a21,a16,f3(a21,a21,a16))),
% 59.77/59.74 inference(scs_inference,[],[4658,4608,4707,4710,4713,4778,4614,4672,4705,4773,4828,4032,4574,4588,4592,4796,4289,4426,4456,4458,4565,4620,4678,4648,4660,4639,4788,4663,4720,4665,4440,4586,4303,4265,4675,4584,4466,4383,4520,4438,4781,4124,4277,4275,4785,4799,4802,4810,4813,4281,4055,4400,1782,1732,1468,276,170,1694,184,173,1688,273,275,169,182,185,168,180,274,171,243,204,188,181,271,242,183,272,269,241,270,186,187,202,222,258,172,195,257,240,221,199,206,207,244,201,194,208,198,220,253,226,268,2,4222,3,193])).
% 59.77/59.74 cnf(4835,plain,
% 59.77/59.74 (P10(x48351,x48352,x48352,x48351)),
% 59.77/59.74 inference(rename_variables,[],[4275])).
% 59.77/59.74 cnf(4840,plain,
% 59.77/59.74 (P6(x48401,f5(x48401,x48401,x48401),x48401)),
% 59.77/59.74 inference(scs_inference,[],[4658,4608,4707,4710,4713,4778,4614,4672,4705,4773,4828,4032,4574,4588,4592,4796,4289,4426,4456,4458,4565,4620,4678,4648,4660,4639,4788,4663,4720,4665,4440,4586,4303,4265,4675,4584,4466,4383,4520,4438,4781,4124,4277,4275,4785,4799,4802,4810,4813,4835,4281,4055,4825,4400,1782,1732,1468,276,170,1694,184,173,1688,273,275,169,182,185,168,180,274,171,243,204,188,181,271,242,183,272,269,241,270,186,187,202,222,258,172,195,257,240,221,199,206,207,244,201,194,208,198,220,253,226,268,2,4222,3,193,205,179])).
% 59.77/59.74 cnf(4845,plain,
% 59.77/59.74 (P10(a21,a16,a16,a16)),
% 59.77/59.74 inference(scs_inference,[],[4658,4608,4707,4710,4713,4778,4614,4672,4705,4773,4828,4032,4574,4588,4592,4796,4289,4426,4456,4458,4565,4620,4678,4648,4660,4639,4788,4663,4720,4665,4440,4586,4303,4265,4675,4584,4466,4383,4520,4438,4781,4124,4277,4275,4785,4799,4802,4810,4813,4835,4525,4281,4055,4825,4400,1782,1732,1468,276,170,1694,184,173,1688,273,275,169,182,185,168,180,274,171,243,204,188,181,271,242,183,272,269,241,270,186,187,202,222,258,172,195,257,240,221,199,206,207,244,201,194,208,198,220,253,226,268,2,4222,3,193,205,179,212])).
% 59.77/59.74 cnf(4855,plain,
% 59.77/59.74 (P6(f46(a16,a16),a24,a24)),
% 59.77/59.74 inference(scs_inference,[],[4831,4736,4369,2,184,1694])).
% 59.77/59.74 cnf(4866,plain,
% 59.77/59.74 (P10(a16,a16,a21,a16)),
% 59.77/59.74 inference(scs_inference,[],[4728,4578,4831,4845,4736,4840,4360,4369,2,184,1694,276,173,170,273,182])).
% 59.77/59.74 cnf(4868,plain,
% 59.77/59.74 (P9(x48681,x48681,x48681,f47(x48681,x48681,x48681,x48681,x48681,x48681))),
% 59.77/59.74 inference(scs_inference,[],[4728,4578,4831,4845,4736,4787,4840,4360,4369,2,184,1694,276,173,170,273,182,180])).
% 59.77/59.74 cnf(4872,plain,
% 59.77/59.74 (P1(x48721,x48722,f5(x48721,x48721,x48722))),
% 59.77/59.74 inference(scs_inference,[],[4728,4578,4831,4845,4736,4787,4840,4732,4817,4360,4369,2,184,1694,276,173,170,273,182,180,1688,168])).
% 59.77/59.74 cnf(4876,plain,
% 59.77/59.74 (P7(x48761,a24,x48761,a24,x48761,x48761,x48761,x48761)),
% 59.77/59.74 inference(scs_inference,[],[4728,4742,4578,4831,4845,4736,4787,4840,4732,4817,4360,4369,2,184,1694,276,173,170,273,182,180,1688,168,274,275])).
% 59.77/59.74 cnf(4878,plain,
% 59.77/59.74 (P1(x48781,x48782,f4(x48782,x48782,x48781))),
% 59.77/59.74 inference(scs_inference,[],[4728,4742,4578,4831,4845,4736,4787,4840,4590,4732,4817,4360,4369,2,184,1694,276,173,170,273,182,180,1688,168,274,275,169])).
% 59.77/59.74 cnf(4880,plain,
% 59.77/59.74 (P4(a16,a21,a21,a16)),
% 59.77/59.74 inference(scs_inference,[],[4728,4742,4578,4827,4831,4845,4736,4787,4840,4590,4732,4817,4360,4369,2,184,1694,276,173,170,273,182,180,1688,168,274,275,169,185])).
% 59.77/59.74 cnf(4882,plain,
% 59.77/59.74 (P6(x48821,x48821,f5(x48821,x48821,x48821))),
% 59.77/59.74 inference(scs_inference,[],[4728,4742,4578,4827,4831,4845,4736,4787,4840,4590,4732,4817,4360,4369,2,184,1694,276,173,170,273,182,180,1688,168,274,275,169,185,171])).
% 59.77/59.74 cnf(4886,plain,
% 59.77/59.74 (P9(f49(x48861,x48862,x48861,x48861,x48861),x48861,x48862,x48861)),
% 59.77/59.74 inference(scs_inference,[],[4728,4742,4578,4827,4831,4845,4736,4787,4840,4691,4590,4732,4817,4360,4369,152,2,184,1694,276,173,170,273,182,180,1688,168,274,275,169,185,171,204,181])).
% 59.77/59.74 cnf(4896,plain,
% 59.77/59.74 (P3(x48961,x48962,x48962,x48963)),
% 59.77/59.74 inference(scs_inference,[],[4770,4132,4728,4742,4578,4827,4831,4845,4736,4740,4787,4840,4691,4590,4732,4600,4817,4360,4369,152,2,184,1694,276,173,170,273,182,180,1688,168,274,275,169,185,171,204,181,243,242,183,271,188])).
% 59.77/59.74 cnf(4898,plain,
% 59.77/59.74 (P8(x48981,x48982,x48981,x48981,x48982,x48982,x48982,x48981)),
% 59.77/59.74 inference(scs_inference,[],[4772,4770,4132,4728,4742,4578,4827,4831,4845,4736,4740,4787,4840,4691,4590,4732,4600,4817,4360,4369,152,2,184,1694,276,173,170,273,182,180,1688,168,274,275,169,185,171,204,181,243,242,183,271,188,241])).
% 59.77/59.74 cnf(4906,plain,
% 59.77/59.74 (P3(x49061,x49062,x49063,x49061)),
% 59.77/59.74 inference(scs_inference,[],[4772,4770,4132,4728,4742,4578,4618,4754,4827,4831,4845,4736,4740,4787,4840,4691,4590,4732,4600,4817,4360,4369,152,2,184,1694,276,173,170,273,182,180,1688,168,274,275,169,185,171,204,181,243,242,183,271,188,241,270,272,269,186])).
% 59.77/59.74 cnf(4915,plain,
% 59.77/59.74 (~E(a31,a34)),
% 59.77/59.74 inference(scs_inference,[],[4772,4770,4132,4728,4742,4578,4604,4618,4754,4827,4831,4845,4736,4740,4787,4840,4691,4590,4732,4600,4817,4360,421,4369,4110,152,2,184,1694,276,173,170,273,182,180,1688,168,274,275,169,185,171,204,181,243,242,183,271,188,241,270,272,269,186,187,217,264,138])).
% 59.77/59.74 cnf(4920,plain,
% 59.77/59.74 (P4(a16,a36,a36,a16)),
% 59.77/59.74 inference(scs_inference,[],[4772,4770,4132,4728,4742,4578,4604,4618,4754,4827,4831,4845,4736,4740,4787,4840,4691,4812,4590,4732,4600,4780,4817,4360,421,4369,4110,4525,152,2,184,1694,276,173,170,273,182,180,1688,168,274,275,169,185,171,204,181,243,242,183,271,188,241,270,272,269,186,187,217,264,138,189,260])).
% 59.77/59.74 cnf(4924,plain,
% 59.77/59.74 (P8(x49241,x49242,x49242,x49241,x49243,x49244,x49243,x49244)),
% 59.77/59.74 inference(rename_variables,[],[4454])).
% 59.77/59.74 cnf(4930,plain,
% 59.77/59.74 (P4(x49301,a24,x49301,a24)),
% 59.77/59.74 inference(rename_variables,[],[4291])).
% 59.77/59.74 cnf(4932,plain,
% 59.77/59.74 (P4(f5(x49321,x49321,x49321),f5(x49321,x49321,x49321),f5(x49321,x49321,x49321),x49321)),
% 59.77/59.74 inference(scs_inference,[],[4772,4770,4132,4728,4742,4578,4604,4618,4754,4827,4831,4845,4736,4740,4787,4840,4691,4812,4590,4732,4600,4780,4817,4291,4360,4454,4924,421,4148,4369,4110,4525,152,2,184,1694,276,173,170,273,182,180,1688,168,274,275,169,185,171,204,181,243,242,183,271,188,241,270,272,269,186,187,217,264,138,189,260,267,266,216,190])).
% 59.77/59.74 cnf(4933,plain,
% 59.77/59.74 (P6(x49331,f5(x49331,x49331,x49331),x49331)),
% 59.77/59.74 inference(rename_variables,[],[4840])).
% 59.77/59.74 cnf(4934,plain,
% 59.77/59.74 (P10(x49341,x49342,x49341,x49342)),
% 59.77/59.74 inference(rename_variables,[],[4148])).
% 59.77/59.74 cnf(4945,plain,
% 59.77/59.74 (P7(x49451,f5(x49451,x49451,x49451),f5(x49451,x49451,x49451),x49451,x49451,f5(x49451,x49451,x49451),f5(x49451,x49451,x49451),x49451)),
% 59.77/59.74 inference(scs_inference,[],[4772,4770,4132,4728,4742,4578,4604,4618,4754,4827,4831,4845,4736,4740,4787,4840,4933,4691,4812,4590,4732,4600,4780,4817,4098,4291,4360,4454,4924,421,4148,4934,4369,4110,4525,152,2,184,1694,276,173,170,273,182,180,1688,168,274,275,169,185,171,204,181,243,242,183,271,188,241,270,272,269,186,187,217,264,138,189,260,267,266,216,190,218,195,258,207,240])).
% 59.77/59.74 cnf(4959,plain,
% 59.77/59.74 (P2(a16,a21,a21,a21)),
% 59.77/59.74 inference(scs_inference,[],[4772,4770,4132,4728,4742,4578,4604,4618,4754,4827,4831,4845,4746,4736,4740,4787,4807,4840,4933,4691,4752,4812,4590,4732,4600,4780,4570,4817,4098,4291,4360,4454,4924,421,4148,4934,4369,4110,4525,152,2,184,1694,276,173,170,273,182,180,1688,168,274,275,169,185,171,204,181,243,242,183,271,188,241,270,272,269,186,187,217,264,138,189,260,267,266,216,190,218,195,258,207,240,244,257,206,208,201])).
% 59.77/59.74 cnf(4963,plain,
% 59.77/59.74 (P10(a16,a16,a21,a21)),
% 59.77/59.74 inference(scs_inference,[],[4772,4770,4132,4728,4742,4578,4604,4618,4754,4827,4831,4845,4746,4736,4740,4787,4807,4840,4933,4691,4752,4812,4590,4732,4600,4780,4570,4817,4098,4291,4360,4454,4924,421,4148,4934,4369,4110,4525,152,2,184,1694,276,173,170,273,182,180,1688,168,274,275,169,185,171,204,181,243,242,183,271,188,241,270,272,269,186,187,217,264,138,189,260,267,266,216,190,218,195,258,207,240,244,257,206,208,201,194,198])).
% 59.77/59.74 cnf(4965,plain,
% 59.77/59.74 (P6(f46(x49651,x49651),f5(x49651,x49651,x49651),f46(x49651,x49651))),
% 59.77/59.74 inference(scs_inference,[],[4772,4770,4132,4728,4742,4578,4604,4618,4754,4827,4831,4845,4746,4736,4740,4787,4807,4840,4933,4691,4752,4812,4590,4732,4600,4780,4570,4817,4626,4098,4291,4360,4454,4924,421,4148,4934,4269,4369,4110,4525,152,2,184,1694,276,173,170,273,182,180,1688,168,274,275,169,185,171,204,181,243,242,183,271,188,241,270,272,269,186,187,217,264,138,189,260,267,266,216,190,218,195,258,207,240,244,257,206,208,201,194,198,179])).
% 59.77/59.74 cnf(4970,plain,
% 59.77/59.74 (P10(a24,a16,a16,a21)),
% 59.77/59.74 inference(scs_inference,[],[4772,4770,4132,4728,4742,4578,4604,4618,4754,4827,4831,4845,4746,4736,4740,4787,4807,4840,4933,4691,4752,4812,4590,4732,4600,4780,4570,4817,4626,4098,4291,4930,4360,4454,4924,421,4126,4148,4934,4269,4369,4110,4525,152,2,184,1694,276,173,170,273,182,180,1688,168,274,275,169,185,171,204,181,243,242,183,271,188,241,270,272,269,186,187,217,264,138,189,260,267,266,216,190,218,195,258,207,240,244,257,206,208,201,194,198,179,212])).
% 59.77/59.74 cnf(4973,plain,
% 59.77/59.74 (P4(x49731,x49731,x49732,x49732)),
% 59.77/59.74 inference(scs_inference,[],[4750,4772,4770,4132,4728,4742,4578,4604,4618,4754,4827,4831,4845,4746,4736,4740,4787,4807,4840,4933,4691,4752,4812,4590,4732,4600,4780,4570,4817,4626,4098,4610,4291,4930,4360,4454,4924,421,4126,4148,4934,4269,4369,4110,4525,152,2,184,1694,276,173,170,273,182,180,1688,168,274,275,169,185,171,204,181,243,242,183,271,188,241,270,272,269,186,187,217,264,138,189,260,267,266,216,190,218,195,258,207,240,244,257,206,208,201,194,198,179,212,268])).
% 59.77/59.74 cnf(4988,plain,
% 59.77/59.74 (P10(a28,a18,a18,a18)),
% 59.77/59.74 inference(scs_inference,[],[4896,473])).
% 59.77/59.74 cnf(4991,plain,
% 59.77/59.74 (P10(a18,a18,a28,a18)),
% 59.77/59.74 inference(scs_inference,[],[4896,959])).
% 59.77/59.74 cnf(4994,plain,
% 59.77/59.74 (P10(a18,a18,a18,a28)),
% 59.77/59.74 inference(scs_inference,[],[4896,966])).
% 59.77/59.74 cnf(4997,plain,
% 59.77/59.74 (P10(a18,a28,a18,a18)),
% 59.77/59.74 inference(scs_inference,[],[4896,974])).
% 59.77/59.74 cnf(5004,plain,
% 59.77/59.74 (P4(f46(x50041,x50041),f5(x50041,x50041,x50041),f46(x50041,x50041),f46(x50041,x50041))),
% 59.77/59.74 inference(scs_inference,[],[4915,4965,2,173])).
% 59.77/59.74 cnf(5006,plain,
% 59.77/59.74 (P4(a21,a16,a16,a21)),
% 59.77/59.74 inference(scs_inference,[],[4915,4880,4965,2,173,184])).
% 59.77/59.74 cnf(5012,plain,
% 59.77/59.74 (P7(x50121,a24,x50121,x50121,x50121,a24,x50121,x50121)),
% 59.77/59.74 inference(scs_inference,[],[4876,4915,4880,4963,4965,2,173,184,273,182,276])).
% 59.77/59.74 cnf(5014,plain,
% 59.77/59.74 (P9(x50141,x50142,f49(x50142,x50141,x50142,x50142,x50142),x50142)),
% 59.77/59.74 inference(scs_inference,[],[4876,4915,4880,4963,4965,4886,2,173,184,273,182,276,180])).
% 59.77/59.74 cnf(5016,plain,
% 59.77/59.74 (P7(a24,a16,a24,a24,a16,a24,a24,a24)),
% 59.77/59.74 inference(scs_inference,[],[4876,4915,4791,4880,4963,4965,4886,2,173,184,273,182,276,180,275])).
% 59.77/59.74 cnf(5018,plain,
% 59.77/59.74 (P4(a16,a36,a16,a36)),
% 59.77/59.74 inference(scs_inference,[],[4876,4915,4791,4880,4920,4963,4965,4886,2,173,184,273,182,276,180,275,185])).
% 59.77/59.74 cnf(5020,plain,
% 59.77/59.74 (P6(f46(x50201,x50201),f46(x50201,x50201),f5(x50201,x50201,x50201))),
% 59.77/59.74 inference(scs_inference,[],[4876,4915,4791,4880,4920,4963,4965,4886,2,173,184,273,182,276,180,275,185,171])).
% 59.77/59.74 cnf(5028,plain,
% 59.77/59.74 (P1(x50281,f5(x50281,x50281,x50282),x50282)),
% 59.77/59.74 inference(scs_inference,[],[4876,4915,4730,4791,4880,4920,4963,4965,4886,4629,4872,4878,2,173,184,273,182,276,180,275,185,171,274,181,168,169])).
% 59.77/59.74 cnf(5036,plain,
% 59.77/59.74 (P3(x50361,x50362,x50361,x50363)),
% 59.77/59.74 inference(scs_inference,[],[4906,4876,4915,4730,4791,4880,4920,4959,4963,4932,4868,4965,4886,4629,4872,4878,2,173,184,273,182,276,180,275,185,171,274,181,168,169,242,243,204,188])).
% 59.77/59.74 cnf(5038,plain,
% 59.77/59.74 (P10(a16,a16,a16,a21)),
% 59.77/59.74 inference(scs_inference,[],[4906,4876,4915,4730,4791,4866,4880,4920,4959,4963,4932,4868,4965,4886,4629,4872,4878,2,173,184,273,182,276,180,275,185,171,274,181,168,169,242,243,204,188,183])).
% 59.77/59.74 cnf(5040,plain,
% 59.77/59.74 (P8(x50401,x50401,x50401,x50402,x50402,x50401,x50402,x50402)),
% 59.77/59.74 inference(scs_inference,[],[4898,4906,4876,4915,4730,4791,4866,4880,4920,4959,4963,4932,4868,4965,4886,4629,4872,4878,2,173,184,273,182,276,180,275,185,171,274,181,168,169,242,243,204,188,183,270])).
% 59.77/59.74 cnf(5042,plain,
% 59.77/59.74 (P8(x50421,x50422,x50422,x50422,x50421,x50421,x50422,x50421)),
% 59.77/59.74 inference(scs_inference,[],[4898,4906,4876,4915,4730,4791,4866,4880,4920,4959,4963,4932,4868,4965,4886,4629,4872,4878,2,173,184,273,182,276,180,275,185,171,274,181,168,169,242,243,204,188,183,270,272])).
% 59.77/59.74 cnf(5044,plain,
% 59.77/59.74 (P8(x50441,x50442,x50441,x50441,x50443,x50442,x50443,x50441)),
% 59.77/59.74 inference(scs_inference,[],[4898,4896,4906,4876,4915,4730,4791,4866,4880,4920,4959,4963,4932,4868,4965,4886,4629,4872,4878,2,173,184,273,182,276,180,275,185,171,274,181,168,169,242,243,204,188,183,270,272,241])).
% 59.77/59.74 cnf(5048,plain,
% 59.77/59.74 (P8(x50481,x50482,x50482,x50482,x50481,x50481,x50481,x50482)),
% 59.77/59.74 inference(scs_inference,[],[4898,4896,4906,4764,4876,4915,4730,4791,4866,4880,4920,4959,4963,4932,4868,4965,4886,4629,4872,4878,2,173,184,273,182,276,180,275,185,171,274,181,168,169,242,243,204,188,183,270,272,241,269,271])).
% 59.77/59.74 cnf(5050,plain,
% 59.77/59.74 (P3(a16,a16,a24,a22)),
% 59.77/59.74 inference(scs_inference,[],[4898,4896,4906,4764,4876,4915,4730,4791,4866,4880,4920,4959,4963,4932,4868,4965,4886,4629,4872,4878,4620,2,173,184,273,182,276,180,275,185,171,274,181,168,169,242,243,204,188,183,270,272,241,269,271,187])).
% 59.77/59.74 cnf(5056,plain,
% 59.77/59.74 (P4(x50561,x50561,x50562,x50562)),
% 59.77/59.74 inference(rename_variables,[],[4973])).
% 59.77/59.74 cnf(5059,plain,
% 59.77/59.74 (P3(x50591,x50592,x50592,x50593)),
% 59.77/59.74 inference(rename_variables,[],[4896])).
% 59.77/59.74 cnf(5069,plain,
% 59.77/59.74 (P4(f5(x50691,x50691,x50691),f5(x50691,x50691,x50691),f5(x50691,x50691,x50691),x50691)),
% 59.77/59.74 inference(rename_variables,[],[4932])).
% 59.77/59.74 cnf(5073,plain,
% 59.77/59.74 (P8(x50731,x50732,x50731,x50731,x50732,x50732,x50732,x50731)),
% 59.77/59.74 inference(rename_variables,[],[4898])).
% 59.77/59.74 cnf(5076,plain,
% 59.77/59.74 (P10(x50761,x50762,x50762,x50761)),
% 59.77/59.74 inference(rename_variables,[],[4275])).
% 59.77/59.74 cnf(5077,plain,
% 59.77/59.74 (P4(x50771,x50771,x50772,x50772)),
% 59.77/59.74 inference(rename_variables,[],[4973])).
% 59.77/59.74 cnf(5080,plain,
% 59.77/59.74 (P4(x50801,x50801,x50802,x50802)),
% 59.77/59.74 inference(rename_variables,[],[4973])).
% 59.77/59.74 cnf(5086,plain,
% 59.77/59.74 (P4(x50861,x50861,x50862,x50862)),
% 59.77/59.74 inference(rename_variables,[],[4973])).
% 59.77/59.74 cnf(5092,plain,
% 59.77/59.74 (P10(x50921,x50922,x50922,x50921)),
% 59.77/59.74 inference(rename_variables,[],[4275])).
% 59.77/59.74 cnf(5099,plain,
% 59.77/59.74 (P8(a21,a16,a21,a21,a21,a21,a21,a21)),
% 59.77/59.74 inference(scs_inference,[],[4898,4973,5056,5077,5080,4896,5059,4906,4764,4876,4915,4730,4791,4866,4880,4920,4959,4963,4970,4697,4932,4868,4965,4882,4886,4629,4872,4878,4243,4756,4473,4742,4620,4663,4259,423,4728,4520,4275,5076,5092,2,173,184,273,182,276,180,275,185,171,274,181,168,169,242,243,204,188,183,270,272,241,269,271,187,280,217,140,200,266,139,260,259,205,218,258,216,190,195,244,240,246])).
% 59.77/59.74 cnf(5100,plain,
% 59.77/59.74 (P10(x51001,x51002,x51002,x51001)),
% 59.77/59.74 inference(rename_variables,[],[4275])).
% 59.77/59.74 cnf(5103,plain,
% 59.77/59.74 (P10(x51031,x51032,x51032,x51031)),
% 59.77/59.74 inference(rename_variables,[],[4275])).
% 59.77/59.74 cnf(5105,plain,
% 59.77/59.74 (P9(f47(x51051,x51051,x51051,x51051,x51051,x51051),x51051,f47(x51051,x51051,x51051,x51051,x51051,x51051),f47(x51051,x51051,x51051,x51051,x51051,x51051))),
% 59.77/59.74 inference(scs_inference,[],[4898,5073,4973,5056,5077,5080,4896,5059,4906,4764,4876,4915,4730,4791,4866,4880,4920,4959,4963,4970,4697,4932,4868,4965,4882,4886,4629,4872,4878,4243,4756,4473,4742,4620,4663,4259,423,4728,4520,4275,5076,5092,5100,2,173,184,273,182,276,180,275,185,171,274,181,168,169,242,243,204,188,183,270,272,241,269,271,187,280,217,140,200,266,139,260,259,205,218,258,216,190,195,244,240,246,206,257])).
% 59.77/59.74 cnf(5110,plain,
% 59.77/59.74 (P10(x51101,x51102,x51102,x51101)),
% 59.77/59.74 inference(rename_variables,[],[4275])).
% 59.77/59.74 cnf(5119,plain,
% 59.77/59.74 (P4(x51191,x51191,x51192,x51192)),
% 59.77/59.74 inference(rename_variables,[],[4973])).
% 59.77/59.74 cnf(5121,plain,
% 59.77/59.74 (P10(f47(x51211,x51211,x51211,x51211,x51211,x51211),f47(x51211,x51211,x51211,x51211,x51211,x51211),x51211,f47(x51211,x51211,x51211,x51211,x51211,x51211))),
% 59.77/59.74 inference(scs_inference,[],[4898,5073,4973,5056,5077,5080,5086,5119,4896,5059,4906,4764,4876,4915,4730,4791,4866,4880,4920,4959,4963,4970,4697,4932,5069,4868,4965,4882,4886,4629,4872,4878,4243,4724,4756,4473,4742,4620,4663,4259,423,4728,4520,4275,5076,5092,5100,5103,5110,2,173,184,273,182,276,180,275,185,171,274,181,168,169,242,243,204,188,183,270,272,241,269,271,187,280,217,140,200,266,139,260,259,205,218,258,216,190,195,244,240,246,206,257,207,208,194,201,198])).
% 59.77/59.74 cnf(5124,plain,
% 59.77/59.74 (P6(f5(x51241,x51241,x51241),x51241,f5(x51241,x51241,x51241))),
% 59.77/59.74 inference(scs_inference,[],[4898,5073,4973,5056,5077,5080,5086,5119,4896,5059,4906,4764,4876,4915,4730,4791,4866,4880,4920,4959,4963,4970,4697,4932,5069,4868,4965,4882,4886,4629,4872,4878,4243,4724,4756,4473,4742,4620,4663,4452,4259,423,4728,4520,4275,5076,5092,5100,5103,5110,4269,2,173,184,273,182,276,180,275,185,171,274,181,168,169,242,243,204,188,183,270,272,241,269,271,187,280,217,140,200,266,139,260,259,205,218,258,216,190,195,244,240,246,206,257,207,208,194,201,198,256])).
% 59.77/59.74 cnf(5169,plain,
% 59.77/59.74 (P8(x51691,x51692,x51691,x51691,x51693,x51692,x51693,x51691)),
% 59.77/59.74 inference(rename_variables,[],[5044])).
% 59.77/59.74 cnf(5172,plain,
% 59.77/59.74 (P8(x51721,x51722,x51721,x51721,x51723,x51722,x51723,x51721)),
% 59.77/59.74 inference(rename_variables,[],[5044])).
% 59.77/59.74 cnf(5177,plain,
% 59.77/59.74 (P8(x51771,x51772,x51771,x51771,x51773,x51772,x51773,x51771)),
% 59.77/59.75 inference(rename_variables,[],[5044])).
% 59.77/59.75 cnf(5228,plain,
% 59.77/59.75 (P6(f46(x52281,x52282),x52282,x52281)),
% 59.77/59.75 inference(rename_variables,[],[4424])).
% 59.77/59.75 cnf(5232,plain,
% 59.77/59.75 (P3(x52321,x52322,x52321,x52323)),
% 59.77/59.75 inference(rename_variables,[],[5036])).
% 59.77/59.75 cnf(5236,plain,
% 59.77/59.75 (P4(x52361,a24,x52361,a24)),
% 59.77/59.75 inference(rename_variables,[],[4291])).
% 59.77/59.75 cnf(5239,plain,
% 59.77/59.75 (P4(x52391,x52391,x52392,x52392)),
% 59.77/59.75 inference(rename_variables,[],[4973])).
% 59.77/59.75 cnf(5242,plain,
% 59.77/59.75 (P3(x52421,x52422,x52421,x52423)),
% 59.77/59.75 inference(rename_variables,[],[5036])).
% 59.77/59.75 cnf(5247,plain,
% 59.77/59.75 (P4(x52471,x52471,x52472,x52472)),
% 59.77/59.75 inference(rename_variables,[],[4973])).
% 59.77/59.75 cnf(5250,plain,
% 59.77/59.75 (P10(x52501,x52502,x52502,x52501)),
% 59.77/59.75 inference(rename_variables,[],[4275])).
% 59.77/59.75 cnf(5259,plain,
% 59.77/59.75 (P8(x52591,x52591,x52591,x52592,x52592,x52591,x52592,x52592)),
% 59.77/59.75 inference(rename_variables,[],[5040])).
% 59.77/59.75 cnf(5262,plain,
% 59.77/59.75 (P4(x52621,x52621,x52622,x52622)),
% 59.77/59.75 inference(rename_variables,[],[4973])).
% 59.77/59.75 cnf(5265,plain,
% 59.77/59.75 (P10(x52651,x52652,x52652,x52651)),
% 59.77/59.75 inference(rename_variables,[],[4275])).
% 59.77/59.75 cnf(5271,plain,
% 59.77/59.75 (P4(x52711,x52711,x52712,x52712)),
% 59.77/59.75 inference(rename_variables,[],[4973])).
% 59.77/59.75 cnf(5292,plain,
% 59.77/59.75 (P3(x52921,x52922,x52921,x52923)),
% 59.77/59.75 inference(rename_variables,[],[5036])).
% 59.77/59.75 cnf(5303,plain,
% 59.77/59.75 (P3(x53031,x53032,x53031,x53033)),
% 59.77/59.75 inference(rename_variables,[],[5036])).
% 59.77/59.75 cnf(5314,plain,
% 59.77/59.75 (P3(x53141,x53142,x53141,x53143)),
% 59.77/59.75 inference(rename_variables,[],[5036])).
% 59.77/59.75 cnf(5321,plain,
% 59.77/59.75 (P3(x53211,x53212,x53212,x53213)),
% 59.77/59.75 inference(rename_variables,[],[4896])).
% 59.77/59.75 cnf(5328,plain,
% 59.77/59.75 ($false),
% 59.77/59.75 inference(scs_inference,[],[4988,5040,5259,5042,5048,5044,5169,5172,5177,5036,5232,5242,5292,5303,5314,4991,4994,4997,4261,5012,4616,4804,5006,5016,5018,5038,5050,5099,5105,5121,4945,5004,5020,5124,5014,5028,4834,4476,4326,4855,4497,4973,5239,5247,5262,5271,4249,4672,4355,4291,5236,4896,5321,4658,4454,283,4120,4275,5250,5265,4424,5228,4110,161,1782,1732,250,1468,182,180,276,184,173,275,185,273,168,171,243,242,181,274,204,188,169,183,270,269,271,272,241,187,191,247,178,217,202,141,211,193,267,264,279,260,205,258,218,216,190,240,195,257,244,206,208,194,207,198,201,209,256,203,212,192,268,2,170,1688,186]),
% 59.77/59.75 ['proof']).
% 59.77/59.75 % SZS output end Proof
% 59.77/59.75 % Total time :59.030000s
%------------------------------------------------------------------------------