%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SWV498-1.050 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n012.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 01:16:05 PM UTC 2026
% Result : Satisfiable 5.97s 1.23s
% Output : Saturation 6.53s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(u1335,negated_conjecture,
a_1749 != a_1799 ).
cnf(u1340,hypothesis,
i1 != i2 ).
cnf(u1345,hypothesis,
i1 != i3 ).
cnf(u1350,hypothesis,
i1 != i4 ).
cnf(u1355,hypothesis,
i1 != i5 ).
cnf(u1360,hypothesis,
i1 != i6 ).
cnf(u1365,hypothesis,
i1 != i7 ).
cnf(u1370,hypothesis,
i1 != i8 ).
cnf(u1375,hypothesis,
i1 != i9 ).
cnf(u1380,hypothesis,
i1 != i10 ).
cnf(u1385,hypothesis,
i1 != i11 ).
cnf(u1390,hypothesis,
i1 != i12 ).
cnf(u1395,hypothesis,
i1 != i13 ).
cnf(u1400,hypothesis,
i1 != i14 ).
cnf(u1405,hypothesis,
i1 != i15 ).
cnf(u1410,hypothesis,
i1 != i16 ).
cnf(u1415,hypothesis,
i1 != i17 ).
cnf(u1420,hypothesis,
i1 != i18 ).
cnf(u1425,hypothesis,
i1 != i19 ).
cnf(u1430,hypothesis,
i1 != i20 ).
cnf(u1435,hypothesis,
i1 != i21 ).
cnf(u1440,hypothesis,
i1 != i22 ).
cnf(u1445,hypothesis,
i1 != i23 ).
cnf(u1450,hypothesis,
i1 != i24 ).
cnf(u1455,hypothesis,
i1 != i25 ).
cnf(u1460,hypothesis,
i1 != i26 ).
cnf(u1465,hypothesis,
i1 != i27 ).
cnf(u1470,hypothesis,
i1 != i28 ).
cnf(u1475,hypothesis,
i1 != i29 ).
cnf(u1480,hypothesis,
i1 != i30 ).
cnf(u1485,hypothesis,
i1 != i31 ).
cnf(u1490,hypothesis,
i1 != i32 ).
cnf(u1495,hypothesis,
i1 != i33 ).
cnf(u1500,hypothesis,
i1 != i34 ).
cnf(u1505,hypothesis,
i1 != i35 ).
cnf(u1510,hypothesis,
i1 != i36 ).
cnf(u1515,hypothesis,
i1 != i37 ).
cnf(u1520,hypothesis,
i1 != i38 ).
cnf(u1525,hypothesis,
i1 != i39 ).
cnf(u1530,hypothesis,
i1 != i40 ).
cnf(u1535,hypothesis,
i1 != i41 ).
cnf(u1540,hypothesis,
i1 != i42 ).
cnf(u1545,hypothesis,
i1 != i43 ).
cnf(u1550,hypothesis,
i1 != i44 ).
cnf(u1555,hypothesis,
i1 != i45 ).
cnf(u1560,hypothesis,
i1 != i46 ).
cnf(u1565,hypothesis,
i1 != i47 ).
cnf(u1570,hypothesis,
i1 != i48 ).
cnf(u1575,hypothesis,
i1 != i49 ).
cnf(u1580,hypothesis,
i1 != i50 ).
cnf(u1585,hypothesis,
i2 != i3 ).
cnf(u1590,hypothesis,
i2 != i4 ).
cnf(u1595,hypothesis,
i2 != i5 ).
cnf(u1600,hypothesis,
i2 != i6 ).
cnf(u1605,hypothesis,
i2 != i7 ).
cnf(u1610,hypothesis,
i2 != i8 ).
cnf(u1615,hypothesis,
i2 != i9 ).
cnf(u1620,hypothesis,
i2 != i10 ).
cnf(u1625,hypothesis,
i2 != i11 ).
cnf(u1630,hypothesis,
i2 != i12 ).
cnf(u1635,hypothesis,
i2 != i13 ).
cnf(u1640,hypothesis,
i2 != i14 ).
cnf(u1645,hypothesis,
i2 != i15 ).
cnf(u1650,hypothesis,
i2 != i16 ).
cnf(u1655,hypothesis,
i2 != i17 ).
cnf(u1660,hypothesis,
i2 != i18 ).
cnf(u1665,hypothesis,
i2 != i19 ).
cnf(u1670,hypothesis,
i2 != i20 ).
cnf(u1675,hypothesis,
i2 != i21 ).
cnf(u1680,hypothesis,
i2 != i22 ).
cnf(u1685,hypothesis,
i2 != i23 ).
cnf(u1690,hypothesis,
i2 != i24 ).
cnf(u1695,hypothesis,
i2 != i25 ).
cnf(u1700,hypothesis,
i2 != i26 ).
cnf(u1705,hypothesis,
i2 != i27 ).
cnf(u1710,hypothesis,
i2 != i28 ).
cnf(u1715,hypothesis,
i2 != i29 ).
cnf(u1720,hypothesis,
i2 != i30 ).
cnf(u1725,hypothesis,
i2 != i31 ).
cnf(u1730,hypothesis,
i2 != i32 ).
cnf(u1735,hypothesis,
i2 != i33 ).
cnf(u1740,hypothesis,
i2 != i34 ).
cnf(u1745,hypothesis,
i2 != i35 ).
cnf(u1750,hypothesis,
i2 != i36 ).
cnf(u1755,hypothesis,
i2 != i37 ).
cnf(u1760,hypothesis,
i2 != i38 ).
cnf(u1765,hypothesis,
i2 != i39 ).
cnf(u1770,hypothesis,
i2 != i40 ).
cnf(u1775,hypothesis,
i2 != i41 ).
cnf(u1780,hypothesis,
i2 != i42 ).
cnf(u1785,hypothesis,
i2 != i43 ).
cnf(u1790,hypothesis,
i2 != i44 ).
cnf(u1795,hypothesis,
i2 != i45 ).
cnf(u1800,hypothesis,
i2 != i46 ).
cnf(u1805,hypothesis,
i2 != i47 ).
cnf(u1810,hypothesis,
i2 != i48 ).
cnf(u1815,hypothesis,
i2 != i49 ).
cnf(u1820,hypothesis,
i2 != i50 ).
cnf(u1825,hypothesis,
i3 != i4 ).
cnf(u1830,hypothesis,
i3 != i5 ).
cnf(u1835,hypothesis,
i3 != i6 ).
cnf(u1840,hypothesis,
i3 != i7 ).
cnf(u1845,hypothesis,
i3 != i8 ).
cnf(u1850,hypothesis,
i3 != i9 ).
cnf(u1855,hypothesis,
i3 != i10 ).
cnf(u1860,hypothesis,
i3 != i11 ).
cnf(u1865,hypothesis,
i3 != i12 ).
cnf(u1870,hypothesis,
i3 != i13 ).
cnf(u1875,hypothesis,
i3 != i14 ).
cnf(u1880,hypothesis,
i3 != i15 ).
cnf(u1885,hypothesis,
i3 != i16 ).
cnf(u1890,hypothesis,
i3 != i17 ).
cnf(u1895,hypothesis,
i3 != i18 ).
cnf(u1900,hypothesis,
i3 != i19 ).
cnf(u1905,hypothesis,
i3 != i20 ).
cnf(u1910,hypothesis,
i3 != i21 ).
cnf(u1915,hypothesis,
i3 != i22 ).
cnf(u1920,hypothesis,
i3 != i23 ).
cnf(u1925,hypothesis,
i3 != i24 ).
cnf(u1930,hypothesis,
i3 != i25 ).
cnf(u1935,hypothesis,
i3 != i26 ).
cnf(u1940,hypothesis,
i3 != i27 ).
cnf(u1945,hypothesis,
i3 != i28 ).
cnf(u1950,hypothesis,
i3 != i29 ).
cnf(u1955,hypothesis,
i3 != i30 ).
cnf(u1960,hypothesis,
i3 != i31 ).
cnf(u1965,hypothesis,
i3 != i32 ).
cnf(u1970,hypothesis,
i3 != i33 ).
cnf(u1975,hypothesis,
i3 != i34 ).
cnf(u1980,hypothesis,
i3 != i35 ).
cnf(u1985,hypothesis,
i3 != i36 ).
cnf(u1990,hypothesis,
i3 != i37 ).
cnf(u1995,hypothesis,
i3 != i38 ).
cnf(u2000,hypothesis,
i3 != i39 ).
cnf(u2005,hypothesis,
i3 != i40 ).
cnf(u2010,hypothesis,
i3 != i41 ).
cnf(u2015,hypothesis,
i3 != i42 ).
cnf(u2020,hypothesis,
i3 != i43 ).
cnf(u2025,hypothesis,
i3 != i44 ).
cnf(u2030,hypothesis,
i3 != i45 ).
cnf(u2035,hypothesis,
i3 != i46 ).
cnf(u2040,hypothesis,
i3 != i47 ).
cnf(u2045,hypothesis,
i3 != i48 ).
cnf(u2050,hypothesis,
i3 != i49 ).
cnf(u2055,hypothesis,
i3 != i50 ).
cnf(u2060,hypothesis,
i4 != i5 ).
cnf(u2065,hypothesis,
i4 != i6 ).
cnf(u2070,hypothesis,
i4 != i7 ).
cnf(u2075,hypothesis,
i4 != i8 ).
cnf(u2080,hypothesis,
i4 != i9 ).
cnf(u2085,hypothesis,
i4 != i10 ).
cnf(u2090,hypothesis,
i4 != i11 ).
cnf(u2095,hypothesis,
i4 != i12 ).
cnf(u2100,hypothesis,
i4 != i13 ).
cnf(u2105,hypothesis,
i4 != i14 ).
cnf(u2110,hypothesis,
i4 != i15 ).
cnf(u2115,hypothesis,
i4 != i16 ).
cnf(u2120,hypothesis,
i4 != i17 ).
cnf(u2125,hypothesis,
i4 != i18 ).
cnf(u2130,hypothesis,
i4 != i19 ).
cnf(u2135,hypothesis,
i4 != i20 ).
cnf(u2140,hypothesis,
i4 != i21 ).
cnf(u2145,hypothesis,
i4 != i22 ).
cnf(u2150,hypothesis,
i4 != i23 ).
cnf(u2155,hypothesis,
i4 != i24 ).
cnf(u2160,hypothesis,
i4 != i25 ).
cnf(u2165,hypothesis,
i4 != i26 ).
cnf(u2170,hypothesis,
i4 != i27 ).
cnf(u2175,hypothesis,
i4 != i28 ).
cnf(u2180,hypothesis,
i4 != i29 ).
cnf(u2185,hypothesis,
i4 != i30 ).
cnf(u2190,hypothesis,
i4 != i31 ).
cnf(u2195,hypothesis,
i4 != i32 ).
cnf(u2200,hypothesis,
i4 != i33 ).
cnf(u2205,hypothesis,
i4 != i34 ).
cnf(u2210,hypothesis,
i4 != i35 ).
cnf(u2215,hypothesis,
i4 != i36 ).
cnf(u2220,hypothesis,
i4 != i37 ).
cnf(u2225,hypothesis,
i4 != i38 ).
cnf(u2230,hypothesis,
i4 != i39 ).
cnf(u2235,hypothesis,
i4 != i40 ).
cnf(u2240,hypothesis,
i4 != i41 ).
cnf(u2245,hypothesis,
i4 != i42 ).
cnf(u2250,hypothesis,
i4 != i43 ).
cnf(u2255,hypothesis,
i4 != i44 ).
cnf(u2260,hypothesis,
i4 != i45 ).
cnf(u2265,hypothesis,
i4 != i46 ).
cnf(u2270,hypothesis,
i4 != i47 ).
cnf(u2275,hypothesis,
i4 != i48 ).
cnf(u2280,hypothesis,
i4 != i49 ).
cnf(u2285,hypothesis,
i4 != i50 ).
cnf(u2290,hypothesis,
i5 != i6 ).
cnf(u2295,hypothesis,
i5 != i7 ).
cnf(u2300,hypothesis,
i5 != i8 ).
cnf(u2305,hypothesis,
i5 != i9 ).
cnf(u2310,hypothesis,
i5 != i10 ).
cnf(u2315,hypothesis,
i5 != i11 ).
cnf(u2320,hypothesis,
i5 != i12 ).
cnf(u2325,hypothesis,
i5 != i13 ).
cnf(u2330,hypothesis,
i5 != i14 ).
cnf(u2335,hypothesis,
i5 != i15 ).
cnf(u2340,hypothesis,
i5 != i16 ).
cnf(u2345,hypothesis,
i5 != i17 ).
cnf(u2350,hypothesis,
i5 != i18 ).
cnf(u2355,hypothesis,
i5 != i19 ).
cnf(u2360,hypothesis,
i5 != i20 ).
cnf(u2365,hypothesis,
i5 != i21 ).
cnf(u2370,hypothesis,
i5 != i22 ).
cnf(u2375,hypothesis,
i5 != i23 ).
cnf(u2380,hypothesis,
i5 != i24 ).
cnf(u2385,hypothesis,
i5 != i25 ).
cnf(u2390,hypothesis,
i5 != i26 ).
cnf(u2395,hypothesis,
i5 != i27 ).
cnf(u2400,hypothesis,
i5 != i28 ).
cnf(u2405,hypothesis,
i5 != i29 ).
cnf(u2410,hypothesis,
i5 != i30 ).
cnf(u2415,hypothesis,
i5 != i31 ).
cnf(u2420,hypothesis,
i5 != i32 ).
cnf(u2425,hypothesis,
i5 != i33 ).
cnf(u2430,hypothesis,
i5 != i34 ).
cnf(u2435,hypothesis,
i5 != i35 ).
cnf(u2440,hypothesis,
i5 != i36 ).
cnf(u2445,hypothesis,
i5 != i37 ).
cnf(u2450,hypothesis,
i5 != i38 ).
cnf(u2455,hypothesis,
i5 != i39 ).
cnf(u2460,hypothesis,
i5 != i40 ).
cnf(u2465,hypothesis,
i5 != i41 ).
cnf(u2470,hypothesis,
i5 != i42 ).
cnf(u2475,hypothesis,
i5 != i43 ).
cnf(u2480,hypothesis,
i5 != i44 ).
cnf(u2485,hypothesis,
i5 != i45 ).
cnf(u2490,hypothesis,
i5 != i46 ).
cnf(u2495,hypothesis,
i5 != i47 ).
cnf(u2500,hypothesis,
i5 != i48 ).
cnf(u2505,hypothesis,
i5 != i49 ).
cnf(u2510,hypothesis,
i5 != i50 ).
cnf(u2515,hypothesis,
i6 != i7 ).
cnf(u2520,hypothesis,
i6 != i8 ).
cnf(u2525,hypothesis,
i6 != i9 ).
cnf(u2530,hypothesis,
i6 != i10 ).
cnf(u2535,hypothesis,
i6 != i11 ).
cnf(u2540,hypothesis,
i6 != i12 ).
cnf(u2545,hypothesis,
i6 != i13 ).
cnf(u2550,hypothesis,
i6 != i14 ).
cnf(u2555,hypothesis,
i6 != i15 ).
cnf(u2560,hypothesis,
i6 != i16 ).
cnf(u2565,hypothesis,
i6 != i17 ).
cnf(u2570,hypothesis,
i6 != i18 ).
cnf(u2575,hypothesis,
i6 != i19 ).
cnf(u2580,hypothesis,
i6 != i20 ).
cnf(u2585,hypothesis,
i6 != i21 ).
cnf(u2590,hypothesis,
i6 != i22 ).
cnf(u2595,hypothesis,
i6 != i23 ).
cnf(u2600,hypothesis,
i6 != i24 ).
cnf(u2605,hypothesis,
i6 != i25 ).
cnf(u2610,hypothesis,
i6 != i26 ).
cnf(u2615,hypothesis,
i6 != i27 ).
cnf(u2620,hypothesis,
i6 != i28 ).
cnf(u2625,hypothesis,
i6 != i29 ).
cnf(u2630,hypothesis,
i6 != i30 ).
cnf(u2635,hypothesis,
i6 != i31 ).
cnf(u2640,hypothesis,
i6 != i32 ).
cnf(u2645,hypothesis,
i6 != i33 ).
cnf(u2650,hypothesis,
i6 != i34 ).
cnf(u2655,hypothesis,
i6 != i35 ).
cnf(u2660,hypothesis,
i6 != i36 ).
cnf(u2665,hypothesis,
i6 != i37 ).
cnf(u2670,hypothesis,
i6 != i38 ).
cnf(u2675,hypothesis,
i6 != i39 ).
cnf(u2680,hypothesis,
i6 != i40 ).
cnf(u2685,hypothesis,
i6 != i41 ).
cnf(u2690,hypothesis,
i6 != i42 ).
cnf(u2695,hypothesis,
i6 != i43 ).
cnf(u2700,hypothesis,
i6 != i44 ).
cnf(u2705,hypothesis,
i6 != i45 ).
cnf(u2710,hypothesis,
i6 != i46 ).
cnf(u2715,hypothesis,
i6 != i47 ).
cnf(u2720,hypothesis,
i6 != i48 ).
cnf(u2725,hypothesis,
i6 != i49 ).
cnf(u2730,hypothesis,
i6 != i50 ).
cnf(u2735,hypothesis,
i7 != i8 ).
cnf(u2740,hypothesis,
i7 != i9 ).
cnf(u2745,hypothesis,
i7 != i10 ).
cnf(u2750,hypothesis,
i7 != i11 ).
cnf(u2755,hypothesis,
i7 != i12 ).
cnf(u2760,hypothesis,
i7 != i13 ).
cnf(u2765,hypothesis,
i7 != i14 ).
cnf(u2770,hypothesis,
i7 != i15 ).
cnf(u2775,hypothesis,
i7 != i16 ).
cnf(u2780,hypothesis,
i7 != i17 ).
cnf(u2785,hypothesis,
i7 != i18 ).
cnf(u2790,hypothesis,
i7 != i19 ).
cnf(u2795,hypothesis,
i7 != i20 ).
cnf(u2800,hypothesis,
i7 != i21 ).
cnf(u2805,hypothesis,
i7 != i22 ).
cnf(u2810,hypothesis,
i7 != i23 ).
cnf(u2815,hypothesis,
i7 != i24 ).
cnf(u2820,hypothesis,
i7 != i25 ).
cnf(u2825,hypothesis,
i7 != i26 ).
cnf(u2830,hypothesis,
i7 != i27 ).
cnf(u2835,hypothesis,
i7 != i28 ).
cnf(u2840,hypothesis,
i7 != i29 ).
cnf(u2845,hypothesis,
i7 != i30 ).
cnf(u2850,hypothesis,
i7 != i31 ).
cnf(u2855,hypothesis,
i7 != i32 ).
cnf(u2860,hypothesis,
i7 != i33 ).
cnf(u2865,hypothesis,
i7 != i34 ).
cnf(u2870,hypothesis,
i7 != i35 ).
cnf(u2875,hypothesis,
i7 != i36 ).
cnf(u2880,hypothesis,
i7 != i37 ).
cnf(u2885,hypothesis,
i7 != i38 ).
cnf(u2890,hypothesis,
i7 != i39 ).
cnf(u2895,hypothesis,
i7 != i40 ).
cnf(u2900,hypothesis,
i7 != i41 ).
cnf(u2905,hypothesis,
i7 != i42 ).
cnf(u2910,hypothesis,
i7 != i43 ).
cnf(u2915,hypothesis,
i7 != i44 ).
cnf(u2920,hypothesis,
i7 != i45 ).
cnf(u2925,hypothesis,
i7 != i46 ).
cnf(u2930,hypothesis,
i7 != i47 ).
cnf(u2935,hypothesis,
i7 != i48 ).
cnf(u2940,hypothesis,
i7 != i49 ).
cnf(u2945,hypothesis,
i7 != i50 ).
cnf(u2950,hypothesis,
i8 != i9 ).
cnf(u2955,hypothesis,
i8 != i10 ).
cnf(u2960,hypothesis,
i8 != i11 ).
cnf(u2965,hypothesis,
i8 != i12 ).
cnf(u2970,hypothesis,
i8 != i13 ).
cnf(u2975,hypothesis,
i8 != i14 ).
cnf(u2980,hypothesis,
i8 != i15 ).
cnf(u2985,hypothesis,
i8 != i16 ).
cnf(u2990,hypothesis,
i8 != i17 ).
cnf(u2995,hypothesis,
i8 != i18 ).
cnf(u3000,hypothesis,
i8 != i19 ).
cnf(u3005,hypothesis,
i8 != i20 ).
cnf(u3010,hypothesis,
i8 != i21 ).
cnf(u3015,hypothesis,
i8 != i22 ).
cnf(u3020,hypothesis,
i8 != i23 ).
cnf(u3025,hypothesis,
i8 != i24 ).
cnf(u3030,hypothesis,
i8 != i25 ).
cnf(u3035,hypothesis,
i8 != i26 ).
cnf(u3040,hypothesis,
i8 != i27 ).
cnf(u3045,hypothesis,
i8 != i28 ).
cnf(u3050,hypothesis,
i8 != i29 ).
cnf(u3055,hypothesis,
i8 != i30 ).
cnf(u3060,hypothesis,
i8 != i31 ).
cnf(u3065,hypothesis,
i8 != i32 ).
cnf(u3070,hypothesis,
i8 != i33 ).
cnf(u3075,hypothesis,
i8 != i34 ).
cnf(u3080,hypothesis,
i8 != i35 ).
cnf(u3085,hypothesis,
i8 != i36 ).
cnf(u3090,hypothesis,
i8 != i37 ).
cnf(u3095,hypothesis,
i8 != i38 ).
cnf(u3100,hypothesis,
i8 != i39 ).
cnf(u3105,hypothesis,
i8 != i40 ).
cnf(u3110,hypothesis,
i8 != i41 ).
cnf(u3115,hypothesis,
i8 != i42 ).
cnf(u3120,hypothesis,
i8 != i43 ).
cnf(u3125,hypothesis,
i8 != i44 ).
cnf(u3130,hypothesis,
i8 != i45 ).
cnf(u3135,hypothesis,
i8 != i46 ).
cnf(u3140,hypothesis,
i8 != i47 ).
cnf(u3145,hypothesis,
i8 != i48 ).
cnf(u3150,hypothesis,
i8 != i49 ).
cnf(u3155,hypothesis,
i8 != i50 ).
cnf(u3160,hypothesis,
i9 != i10 ).
cnf(u3165,hypothesis,
i9 != i11 ).
cnf(u3170,hypothesis,
i9 != i12 ).
cnf(u3175,hypothesis,
i9 != i13 ).
cnf(u3180,hypothesis,
i9 != i14 ).
cnf(u3185,hypothesis,
i9 != i15 ).
cnf(u3190,hypothesis,
i9 != i16 ).
cnf(u3195,hypothesis,
i9 != i17 ).
cnf(u3200,hypothesis,
i9 != i18 ).
cnf(u3205,hypothesis,
i9 != i19 ).
cnf(u3210,hypothesis,
i9 != i20 ).
cnf(u3215,hypothesis,
i9 != i21 ).
cnf(u3220,hypothesis,
i9 != i22 ).
cnf(u3225,hypothesis,
i9 != i23 ).
cnf(u3230,hypothesis,
i9 != i24 ).
cnf(u3235,hypothesis,
i9 != i25 ).
cnf(u3240,hypothesis,
i9 != i26 ).
cnf(u3245,hypothesis,
i9 != i27 ).
cnf(u3250,hypothesis,
i9 != i28 ).
cnf(u3255,hypothesis,
i9 != i29 ).
cnf(u3260,hypothesis,
i9 != i30 ).
cnf(u3265,hypothesis,
i9 != i31 ).
cnf(u3270,hypothesis,
i9 != i32 ).
cnf(u3275,hypothesis,
i9 != i33 ).
cnf(u3280,hypothesis,
i9 != i34 ).
cnf(u3285,hypothesis,
i9 != i35 ).
cnf(u3290,hypothesis,
i9 != i36 ).
cnf(u3295,hypothesis,
i9 != i37 ).
cnf(u3300,hypothesis,
i9 != i38 ).
cnf(u3305,hypothesis,
i9 != i39 ).
cnf(u3310,hypothesis,
i9 != i40 ).
cnf(u3315,hypothesis,
i9 != i41 ).
cnf(u3320,hypothesis,
i9 != i42 ).
cnf(u3325,hypothesis,
i9 != i43 ).
cnf(u3330,hypothesis,
i9 != i44 ).
cnf(u3335,hypothesis,
i9 != i45 ).
cnf(u3340,hypothesis,
i9 != i46 ).
cnf(u3345,hypothesis,
i9 != i47 ).
cnf(u3350,hypothesis,
i9 != i48 ).
cnf(u3355,hypothesis,
i9 != i49 ).
cnf(u3360,hypothesis,
i9 != i50 ).
cnf(u3365,hypothesis,
i10 != i11 ).
cnf(u3370,hypothesis,
i10 != i12 ).
cnf(u3375,hypothesis,
i10 != i13 ).
cnf(u3380,hypothesis,
i10 != i14 ).
cnf(u3385,hypothesis,
i10 != i15 ).
cnf(u3390,hypothesis,
i10 != i16 ).
cnf(u3395,hypothesis,
i10 != i17 ).
cnf(u3400,hypothesis,
i10 != i18 ).
cnf(u3405,hypothesis,
i10 != i19 ).
cnf(u3410,hypothesis,
i10 != i20 ).
cnf(u3415,hypothesis,
i10 != i21 ).
cnf(u3420,hypothesis,
i10 != i22 ).
cnf(u3425,hypothesis,
i10 != i23 ).
cnf(u3430,hypothesis,
i10 != i24 ).
cnf(u3435,hypothesis,
i10 != i25 ).
cnf(u3440,hypothesis,
i10 != i26 ).
cnf(u3445,hypothesis,
i10 != i27 ).
cnf(u3450,hypothesis,
i10 != i28 ).
cnf(u3455,hypothesis,
i10 != i29 ).
cnf(u3460,hypothesis,
i10 != i30 ).
cnf(u3465,hypothesis,
i10 != i31 ).
cnf(u3470,hypothesis,
i10 != i32 ).
cnf(u3475,hypothesis,
i10 != i33 ).
cnf(u3480,hypothesis,
i10 != i34 ).
cnf(u3485,hypothesis,
i10 != i35 ).
cnf(u3490,hypothesis,
i10 != i36 ).
cnf(u3495,hypothesis,
i10 != i37 ).
cnf(u3500,hypothesis,
i10 != i38 ).
cnf(u3505,hypothesis,
i10 != i39 ).
cnf(u3510,hypothesis,
i10 != i40 ).
cnf(u3515,hypothesis,
i10 != i41 ).
cnf(u3520,hypothesis,
i10 != i42 ).
cnf(u3525,hypothesis,
i10 != i43 ).
cnf(u3530,hypothesis,
i10 != i44 ).
cnf(u3535,hypothesis,
i10 != i45 ).
cnf(u3540,hypothesis,
i10 != i46 ).
cnf(u3545,hypothesis,
i10 != i47 ).
cnf(u3550,hypothesis,
i10 != i48 ).
cnf(u3555,hypothesis,
i10 != i49 ).
cnf(u3560,hypothesis,
i10 != i50 ).
cnf(u3565,hypothesis,
i11 != i12 ).
cnf(u3570,hypothesis,
i11 != i13 ).
cnf(u3575,hypothesis,
i11 != i14 ).
cnf(u3580,hypothesis,
i11 != i15 ).
cnf(u3585,hypothesis,
i11 != i16 ).
cnf(u3590,hypothesis,
i11 != i17 ).
cnf(u3595,hypothesis,
i11 != i18 ).
cnf(u3600,hypothesis,
i11 != i19 ).
cnf(u3605,hypothesis,
i11 != i20 ).
cnf(u3610,hypothesis,
i11 != i21 ).
cnf(u3615,hypothesis,
i11 != i22 ).
cnf(u3620,hypothesis,
i11 != i23 ).
cnf(u3625,hypothesis,
i11 != i24 ).
cnf(u3630,hypothesis,
i11 != i25 ).
cnf(u3635,hypothesis,
i11 != i26 ).
cnf(u3640,hypothesis,
i11 != i27 ).
cnf(u3645,hypothesis,
i11 != i28 ).
cnf(u3650,hypothesis,
i11 != i29 ).
cnf(u3655,hypothesis,
i11 != i30 ).
cnf(u3660,hypothesis,
i11 != i31 ).
cnf(u3665,hypothesis,
i11 != i32 ).
cnf(u3670,hypothesis,
i11 != i33 ).
cnf(u3675,hypothesis,
i11 != i34 ).
cnf(u3680,hypothesis,
i11 != i35 ).
cnf(u3685,hypothesis,
i11 != i36 ).
cnf(u3690,hypothesis,
i11 != i37 ).
cnf(u3695,hypothesis,
i11 != i38 ).
cnf(u3700,hypothesis,
i11 != i39 ).
cnf(u3705,hypothesis,
i11 != i40 ).
cnf(u3710,hypothesis,
i11 != i41 ).
cnf(u3715,hypothesis,
i11 != i42 ).
cnf(u3720,hypothesis,
i11 != i43 ).
cnf(u3725,hypothesis,
i11 != i44 ).
cnf(u3730,hypothesis,
i11 != i45 ).
cnf(u3735,hypothesis,
i11 != i46 ).
cnf(u3740,hypothesis,
i11 != i47 ).
cnf(u3745,hypothesis,
i11 != i48 ).
cnf(u3750,hypothesis,
i11 != i49 ).
cnf(u3755,hypothesis,
i11 != i50 ).
cnf(u3760,hypothesis,
i12 != i13 ).
cnf(u3765,hypothesis,
i12 != i14 ).
cnf(u3770,hypothesis,
i12 != i15 ).
cnf(u3775,hypothesis,
i12 != i16 ).
cnf(u3780,hypothesis,
i12 != i17 ).
cnf(u3785,hypothesis,
i12 != i18 ).
cnf(u3790,hypothesis,
i12 != i19 ).
cnf(u3795,hypothesis,
i12 != i20 ).
cnf(u3800,hypothesis,
i12 != i21 ).
cnf(u3805,hypothesis,
i12 != i22 ).
cnf(u3810,hypothesis,
i12 != i23 ).
cnf(u3815,hypothesis,
i12 != i24 ).
cnf(u3820,hypothesis,
i12 != i25 ).
cnf(u3825,hypothesis,
i12 != i26 ).
cnf(u3830,hypothesis,
i12 != i27 ).
cnf(u3835,hypothesis,
i12 != i28 ).
cnf(u3840,hypothesis,
i12 != i29 ).
cnf(u3845,hypothesis,
i12 != i30 ).
cnf(u3850,hypothesis,
i12 != i31 ).
cnf(u3855,hypothesis,
i12 != i32 ).
cnf(u3860,hypothesis,
i12 != i33 ).
cnf(u3865,hypothesis,
i12 != i34 ).
cnf(u3870,hypothesis,
i12 != i35 ).
cnf(u3875,hypothesis,
i12 != i36 ).
cnf(u3880,hypothesis,
i12 != i37 ).
cnf(u3885,hypothesis,
i12 != i38 ).
cnf(u3890,hypothesis,
i12 != i39 ).
cnf(u3895,hypothesis,
i12 != i40 ).
cnf(u3900,hypothesis,
i12 != i41 ).
cnf(u3905,hypothesis,
i12 != i42 ).
cnf(u3910,hypothesis,
i12 != i43 ).
cnf(u3915,hypothesis,
i12 != i44 ).
cnf(u3920,hypothesis,
i12 != i45 ).
cnf(u3925,hypothesis,
i12 != i46 ).
cnf(u3930,hypothesis,
i12 != i47 ).
cnf(u3935,hypothesis,
i12 != i48 ).
cnf(u3940,hypothesis,
i12 != i49 ).
cnf(u3945,hypothesis,
i12 != i50 ).
cnf(u3950,hypothesis,
i13 != i14 ).
cnf(u3955,hypothesis,
i13 != i15 ).
cnf(u3960,hypothesis,
i13 != i16 ).
cnf(u3965,hypothesis,
i13 != i17 ).
cnf(u3970,hypothesis,
i13 != i18 ).
cnf(u3975,hypothesis,
i13 != i19 ).
cnf(u3980,hypothesis,
i13 != i20 ).
cnf(u3985,hypothesis,
i13 != i21 ).
cnf(u3990,hypothesis,
i13 != i22 ).
cnf(u3995,hypothesis,
i13 != i23 ).
cnf(u4000,hypothesis,
i13 != i24 ).
cnf(u4005,hypothesis,
i13 != i25 ).
cnf(u4010,hypothesis,
i13 != i26 ).
cnf(u4015,hypothesis,
i13 != i27 ).
cnf(u4020,hypothesis,
i13 != i28 ).
cnf(u4025,hypothesis,
i13 != i29 ).
cnf(u4030,hypothesis,
i13 != i30 ).
cnf(u4035,hypothesis,
i13 != i31 ).
cnf(u4040,hypothesis,
i13 != i32 ).
cnf(u4045,hypothesis,
i13 != i33 ).
cnf(u4050,hypothesis,
i13 != i34 ).
cnf(u4055,hypothesis,
i13 != i35 ).
cnf(u4060,hypothesis,
i13 != i36 ).
cnf(u4065,hypothesis,
i13 != i37 ).
cnf(u4070,hypothesis,
i13 != i38 ).
cnf(u4075,hypothesis,
i13 != i39 ).
cnf(u4080,hypothesis,
i13 != i40 ).
cnf(u4085,hypothesis,
i13 != i41 ).
cnf(u4090,hypothesis,
i13 != i42 ).
cnf(u4095,hypothesis,
i13 != i43 ).
cnf(u4100,hypothesis,
i13 != i44 ).
cnf(u4105,hypothesis,
i13 != i45 ).
cnf(u4110,hypothesis,
i13 != i46 ).
cnf(u4115,hypothesis,
i13 != i47 ).
cnf(u4120,hypothesis,
i13 != i48 ).
cnf(u4125,hypothesis,
i13 != i49 ).
cnf(u4130,hypothesis,
i13 != i50 ).
cnf(u4135,hypothesis,
i14 != i15 ).
cnf(u4140,hypothesis,
i14 != i16 ).
cnf(u4145,hypothesis,
i14 != i17 ).
cnf(u4150,hypothesis,
i14 != i18 ).
cnf(u4155,hypothesis,
i14 != i19 ).
cnf(u4160,hypothesis,
i14 != i20 ).
cnf(u4165,hypothesis,
i14 != i21 ).
cnf(u4170,hypothesis,
i14 != i22 ).
cnf(u4175,hypothesis,
i14 != i23 ).
cnf(u4180,hypothesis,
i14 != i24 ).
cnf(u4185,hypothesis,
i14 != i25 ).
cnf(u4190,hypothesis,
i14 != i26 ).
cnf(u4195,hypothesis,
i14 != i27 ).
cnf(u4200,hypothesis,
i14 != i28 ).
cnf(u4205,hypothesis,
i14 != i29 ).
cnf(u4210,hypothesis,
i14 != i30 ).
cnf(u4215,hypothesis,
i14 != i31 ).
cnf(u4220,hypothesis,
i14 != i32 ).
cnf(u4225,hypothesis,
i14 != i33 ).
cnf(u4230,hypothesis,
i14 != i34 ).
cnf(u4235,hypothesis,
i14 != i35 ).
cnf(u4240,hypothesis,
i14 != i36 ).
cnf(u4245,hypothesis,
i14 != i37 ).
cnf(u4250,hypothesis,
i14 != i38 ).
cnf(u4255,hypothesis,
i14 != i39 ).
cnf(u4260,hypothesis,
i14 != i40 ).
cnf(u4265,hypothesis,
i14 != i41 ).
cnf(u4270,hypothesis,
i14 != i42 ).
cnf(u4275,hypothesis,
i14 != i43 ).
cnf(u4280,hypothesis,
i14 != i44 ).
cnf(u4285,hypothesis,
i14 != i45 ).
cnf(u4290,hypothesis,
i14 != i46 ).
cnf(u4295,hypothesis,
i14 != i47 ).
cnf(u4300,hypothesis,
i14 != i48 ).
cnf(u4305,hypothesis,
i14 != i49 ).
cnf(u4310,hypothesis,
i14 != i50 ).
cnf(u4315,hypothesis,
i15 != i16 ).
cnf(u4320,hypothesis,
i15 != i17 ).
cnf(u4325,hypothesis,
i15 != i18 ).
cnf(u4330,hypothesis,
i15 != i19 ).
cnf(u4335,hypothesis,
i15 != i20 ).
cnf(u4340,hypothesis,
i15 != i21 ).
cnf(u4345,hypothesis,
i15 != i22 ).
cnf(u4350,hypothesis,
i15 != i23 ).
cnf(u4355,hypothesis,
i15 != i24 ).
cnf(u4360,hypothesis,
i15 != i25 ).
cnf(u4365,hypothesis,
i15 != i26 ).
cnf(u4370,hypothesis,
i15 != i27 ).
cnf(u4375,hypothesis,
i15 != i28 ).
cnf(u4380,hypothesis,
i15 != i29 ).
cnf(u4385,hypothesis,
i15 != i30 ).
cnf(u4390,hypothesis,
i15 != i31 ).
cnf(u4395,hypothesis,
i15 != i32 ).
cnf(u4400,hypothesis,
i15 != i33 ).
cnf(u4405,hypothesis,
i15 != i34 ).
cnf(u4410,hypothesis,
i15 != i35 ).
cnf(u4415,hypothesis,
i15 != i36 ).
cnf(u4420,hypothesis,
i15 != i37 ).
cnf(u4425,hypothesis,
i15 != i38 ).
cnf(u4430,hypothesis,
i15 != i39 ).
cnf(u4435,hypothesis,
i15 != i40 ).
cnf(u4440,hypothesis,
i15 != i41 ).
cnf(u4445,hypothesis,
i15 != i42 ).
cnf(u4450,hypothesis,
i15 != i43 ).
cnf(u4455,hypothesis,
i15 != i44 ).
cnf(u4460,hypothesis,
i15 != i45 ).
cnf(u4465,hypothesis,
i15 != i46 ).
cnf(u4470,hypothesis,
i15 != i47 ).
cnf(u4475,hypothesis,
i15 != i48 ).
cnf(u4480,hypothesis,
i15 != i49 ).
cnf(u4485,hypothesis,
i15 != i50 ).
cnf(u4490,hypothesis,
i16 != i17 ).
cnf(u4495,hypothesis,
i16 != i18 ).
cnf(u4500,hypothesis,
i16 != i19 ).
cnf(u4505,hypothesis,
i16 != i20 ).
cnf(u4510,hypothesis,
i16 != i21 ).
cnf(u4515,hypothesis,
i16 != i22 ).
cnf(u4520,hypothesis,
i16 != i23 ).
cnf(u4525,hypothesis,
i16 != i24 ).
cnf(u4530,hypothesis,
i16 != i25 ).
cnf(u4535,hypothesis,
i16 != i26 ).
cnf(u4540,hypothesis,
i16 != i27 ).
cnf(u4545,hypothesis,
i16 != i28 ).
cnf(u4550,hypothesis,
i16 != i29 ).
cnf(u4555,hypothesis,
i16 != i30 ).
cnf(u4560,hypothesis,
i16 != i31 ).
cnf(u4565,hypothesis,
i16 != i32 ).
cnf(u4570,hypothesis,
i16 != i33 ).
cnf(u4575,hypothesis,
i16 != i34 ).
cnf(u4580,hypothesis,
i16 != i35 ).
cnf(u4585,hypothesis,
i16 != i36 ).
cnf(u4590,hypothesis,
i16 != i37 ).
cnf(u4595,hypothesis,
i16 != i38 ).
cnf(u4600,hypothesis,
i16 != i39 ).
cnf(u4605,hypothesis,
i16 != i40 ).
cnf(u4610,hypothesis,
i16 != i41 ).
cnf(u4615,hypothesis,
i16 != i42 ).
cnf(u4620,hypothesis,
i16 != i43 ).
cnf(u4625,hypothesis,
i16 != i44 ).
cnf(u4630,hypothesis,
i16 != i45 ).
cnf(u4635,hypothesis,
i16 != i46 ).
cnf(u4640,hypothesis,
i16 != i47 ).
cnf(u4645,hypothesis,
i16 != i48 ).
cnf(u4650,hypothesis,
i16 != i49 ).
cnf(u4655,hypothesis,
i16 != i50 ).
cnf(u4660,hypothesis,
i17 != i18 ).
cnf(u4665,hypothesis,
i17 != i19 ).
cnf(u4670,hypothesis,
i17 != i20 ).
cnf(u4675,hypothesis,
i17 != i21 ).
cnf(u4680,hypothesis,
i17 != i22 ).
cnf(u4685,hypothesis,
i17 != i23 ).
cnf(u4690,hypothesis,
i17 != i24 ).
cnf(u4695,hypothesis,
i17 != i25 ).
cnf(u4700,hypothesis,
i17 != i26 ).
cnf(u4705,hypothesis,
i17 != i27 ).
cnf(u4710,hypothesis,
i17 != i28 ).
cnf(u4715,hypothesis,
i17 != i29 ).
cnf(u4720,hypothesis,
i17 != i30 ).
cnf(u4725,hypothesis,
i17 != i31 ).
cnf(u4730,hypothesis,
i17 != i32 ).
cnf(u4735,hypothesis,
i17 != i33 ).
cnf(u4740,hypothesis,
i17 != i34 ).
cnf(u4745,hypothesis,
i17 != i35 ).
cnf(u4750,hypothesis,
i17 != i36 ).
cnf(u4755,hypothesis,
i17 != i37 ).
cnf(u4760,hypothesis,
i17 != i38 ).
cnf(u4765,hypothesis,
i17 != i39 ).
cnf(u4770,hypothesis,
i17 != i40 ).
cnf(u4775,hypothesis,
i17 != i41 ).
cnf(u4780,hypothesis,
i17 != i42 ).
cnf(u4785,hypothesis,
i17 != i43 ).
cnf(u4790,hypothesis,
i17 != i44 ).
cnf(u4795,hypothesis,
i17 != i45 ).
cnf(u4800,hypothesis,
i17 != i46 ).
cnf(u4805,hypothesis,
i17 != i47 ).
cnf(u4810,hypothesis,
i17 != i48 ).
cnf(u4815,hypothesis,
i17 != i49 ).
cnf(u4820,hypothesis,
i17 != i50 ).
cnf(u4825,hypothesis,
i18 != i19 ).
cnf(u4830,hypothesis,
i18 != i20 ).
cnf(u4835,hypothesis,
i18 != i21 ).
cnf(u4840,hypothesis,
i18 != i22 ).
cnf(u4845,hypothesis,
i18 != i23 ).
cnf(u4850,hypothesis,
i18 != i24 ).
cnf(u4855,hypothesis,
i18 != i25 ).
cnf(u4860,hypothesis,
i18 != i26 ).
cnf(u4865,hypothesis,
i18 != i27 ).
cnf(u4870,hypothesis,
i18 != i28 ).
cnf(u4875,hypothesis,
i18 != i29 ).
cnf(u4880,hypothesis,
i18 != i30 ).
cnf(u4885,hypothesis,
i18 != i31 ).
cnf(u4890,hypothesis,
i18 != i32 ).
cnf(u4895,hypothesis,
i18 != i33 ).
cnf(u4900,hypothesis,
i18 != i34 ).
cnf(u4905,hypothesis,
i18 != i35 ).
cnf(u4910,hypothesis,
i18 != i36 ).
cnf(u4915,hypothesis,
i18 != i37 ).
cnf(u4920,hypothesis,
i18 != i38 ).
cnf(u4925,hypothesis,
i18 != i39 ).
cnf(u4930,hypothesis,
i18 != i40 ).
cnf(u4935,hypothesis,
i18 != i41 ).
cnf(u4940,hypothesis,
i18 != i42 ).
cnf(u4945,hypothesis,
i18 != i43 ).
cnf(u4950,hypothesis,
i18 != i44 ).
cnf(u4955,hypothesis,
i18 != i45 ).
cnf(u4960,hypothesis,
i18 != i46 ).
cnf(u4965,hypothesis,
i18 != i47 ).
cnf(u4970,hypothesis,
i18 != i48 ).
cnf(u4975,hypothesis,
i18 != i49 ).
cnf(u4980,hypothesis,
i18 != i50 ).
cnf(u4985,hypothesis,
i19 != i20 ).
cnf(u4990,hypothesis,
i19 != i21 ).
cnf(u4995,hypothesis,
i19 != i22 ).
cnf(u5000,hypothesis,
i19 != i23 ).
cnf(u5005,hypothesis,
i19 != i24 ).
cnf(u5010,hypothesis,
i19 != i25 ).
cnf(u5015,hypothesis,
i19 != i26 ).
cnf(u5020,hypothesis,
i19 != i27 ).
cnf(u5025,hypothesis,
i19 != i28 ).
cnf(u5030,hypothesis,
i19 != i29 ).
cnf(u5035,hypothesis,
i19 != i30 ).
cnf(u5040,hypothesis,
i19 != i31 ).
cnf(u5045,hypothesis,
i19 != i32 ).
cnf(u5050,hypothesis,
i19 != i33 ).
cnf(u5055,hypothesis,
i19 != i34 ).
cnf(u5060,hypothesis,
i19 != i35 ).
cnf(u5065,hypothesis,
i19 != i36 ).
cnf(u5070,hypothesis,
i19 != i37 ).
cnf(u5075,hypothesis,
i19 != i38 ).
cnf(u5080,hypothesis,
i19 != i39 ).
cnf(u5085,hypothesis,
i19 != i40 ).
cnf(u5090,hypothesis,
i19 != i41 ).
cnf(u5095,hypothesis,
i19 != i42 ).
cnf(u5100,hypothesis,
i19 != i43 ).
cnf(u5105,hypothesis,
i19 != i44 ).
cnf(u5110,hypothesis,
i19 != i45 ).
cnf(u5115,hypothesis,
i19 != i46 ).
cnf(u5120,hypothesis,
i19 != i47 ).
cnf(u5125,hypothesis,
i19 != i48 ).
cnf(u5130,hypothesis,
i19 != i49 ).
cnf(u5135,hypothesis,
i19 != i50 ).
cnf(u5140,hypothesis,
i20 != i21 ).
cnf(u5145,hypothesis,
i20 != i22 ).
cnf(u5150,hypothesis,
i20 != i23 ).
cnf(u5155,hypothesis,
i20 != i24 ).
cnf(u5160,hypothesis,
i20 != i25 ).
cnf(u5165,hypothesis,
i20 != i26 ).
cnf(u5170,hypothesis,
i20 != i27 ).
cnf(u5175,hypothesis,
i20 != i28 ).
cnf(u5180,hypothesis,
i20 != i29 ).
cnf(u5185,hypothesis,
i20 != i30 ).
cnf(u5190,hypothesis,
i20 != i31 ).
cnf(u5195,hypothesis,
i20 != i32 ).
cnf(u5200,hypothesis,
i20 != i33 ).
cnf(u5205,hypothesis,
i20 != i34 ).
cnf(u5210,hypothesis,
i20 != i35 ).
cnf(u5215,hypothesis,
i20 != i36 ).
cnf(u5220,hypothesis,
i20 != i37 ).
cnf(u5225,hypothesis,
i20 != i38 ).
cnf(u5230,hypothesis,
i20 != i39 ).
cnf(u5235,hypothesis,
i20 != i40 ).
cnf(u5240,hypothesis,
i20 != i41 ).
cnf(u5245,hypothesis,
i20 != i42 ).
cnf(u5250,hypothesis,
i20 != i43 ).
cnf(u5255,hypothesis,
i20 != i44 ).
cnf(u5260,hypothesis,
i20 != i45 ).
cnf(u5265,hypothesis,
i20 != i46 ).
cnf(u5270,hypothesis,
i20 != i47 ).
cnf(u5275,hypothesis,
i20 != i48 ).
cnf(u5280,hypothesis,
i20 != i49 ).
cnf(u5285,hypothesis,
i20 != i50 ).
cnf(u5290,hypothesis,
i21 != i22 ).
cnf(u5295,hypothesis,
i21 != i23 ).
cnf(u5300,hypothesis,
i21 != i24 ).
cnf(u5305,hypothesis,
i21 != i25 ).
cnf(u5310,hypothesis,
i21 != i26 ).
cnf(u5315,hypothesis,
i21 != i27 ).
cnf(u5320,hypothesis,
i21 != i28 ).
cnf(u5325,hypothesis,
i21 != i29 ).
cnf(u5330,hypothesis,
i21 != i30 ).
cnf(u5335,hypothesis,
i21 != i31 ).
cnf(u5340,hypothesis,
i21 != i32 ).
cnf(u5345,hypothesis,
i21 != i33 ).
cnf(u5350,hypothesis,
i21 != i34 ).
cnf(u5355,hypothesis,
i21 != i35 ).
cnf(u5360,hypothesis,
i21 != i36 ).
cnf(u5365,hypothesis,
i21 != i37 ).
cnf(u5370,hypothesis,
i21 != i38 ).
cnf(u5375,hypothesis,
i21 != i39 ).
cnf(u5380,hypothesis,
i21 != i40 ).
cnf(u5385,hypothesis,
i21 != i41 ).
cnf(u5390,hypothesis,
i21 != i42 ).
cnf(u5395,hypothesis,
i21 != i43 ).
cnf(u5400,hypothesis,
i21 != i44 ).
cnf(u5405,hypothesis,
i21 != i45 ).
cnf(u5410,hypothesis,
i21 != i46 ).
cnf(u5415,hypothesis,
i21 != i47 ).
cnf(u5420,hypothesis,
i21 != i48 ).
cnf(u5425,hypothesis,
i21 != i49 ).
cnf(u5430,hypothesis,
i21 != i50 ).
cnf(u5435,hypothesis,
i22 != i23 ).
cnf(u5440,hypothesis,
i22 != i24 ).
cnf(u5445,hypothesis,
i22 != i25 ).
cnf(u5450,hypothesis,
i22 != i26 ).
cnf(u5455,hypothesis,
i22 != i27 ).
cnf(u5460,hypothesis,
i22 != i28 ).
cnf(u5465,hypothesis,
i22 != i29 ).
cnf(u5470,hypothesis,
i22 != i30 ).
cnf(u5475,hypothesis,
i22 != i31 ).
cnf(u5480,hypothesis,
i22 != i32 ).
cnf(u5485,hypothesis,
i22 != i33 ).
cnf(u5490,hypothesis,
i22 != i34 ).
cnf(u5495,hypothesis,
i22 != i35 ).
cnf(u5500,hypothesis,
i22 != i36 ).
cnf(u5505,hypothesis,
i22 != i37 ).
cnf(u5510,hypothesis,
i22 != i38 ).
cnf(u5515,hypothesis,
i22 != i39 ).
cnf(u5520,hypothesis,
i22 != i40 ).
cnf(u5525,hypothesis,
i22 != i41 ).
cnf(u5530,hypothesis,
i22 != i42 ).
cnf(u5535,hypothesis,
i22 != i43 ).
cnf(u5540,hypothesis,
i22 != i44 ).
cnf(u5545,hypothesis,
i22 != i45 ).
cnf(u5550,hypothesis,
i22 != i46 ).
cnf(u5555,hypothesis,
i22 != i47 ).
cnf(u5560,hypothesis,
i22 != i48 ).
cnf(u5565,hypothesis,
i22 != i49 ).
cnf(u5570,hypothesis,
i22 != i50 ).
cnf(u5575,hypothesis,
i23 != i24 ).
cnf(u5580,hypothesis,
i23 != i25 ).
cnf(u5585,hypothesis,
i23 != i26 ).
cnf(u5590,hypothesis,
i23 != i27 ).
cnf(u5595,hypothesis,
i23 != i28 ).
cnf(u5600,hypothesis,
i23 != i29 ).
cnf(u5605,hypothesis,
i23 != i30 ).
cnf(u5610,hypothesis,
i23 != i31 ).
cnf(u5615,hypothesis,
i23 != i32 ).
cnf(u5620,hypothesis,
i23 != i33 ).
cnf(u5625,hypothesis,
i23 != i34 ).
cnf(u5630,hypothesis,
i23 != i35 ).
cnf(u5635,hypothesis,
i23 != i36 ).
cnf(u5640,hypothesis,
i23 != i37 ).
cnf(u5645,hypothesis,
i23 != i38 ).
cnf(u5650,hypothesis,
i23 != i39 ).
cnf(u5655,hypothesis,
i23 != i40 ).
cnf(u5660,hypothesis,
i23 != i41 ).
cnf(u5665,hypothesis,
i23 != i42 ).
cnf(u5670,hypothesis,
i23 != i43 ).
cnf(u5675,hypothesis,
i23 != i44 ).
cnf(u5680,hypothesis,
i23 != i45 ).
cnf(u5685,hypothesis,
i23 != i46 ).
cnf(u5690,hypothesis,
i23 != i47 ).
cnf(u5695,hypothesis,
i23 != i48 ).
cnf(u5700,hypothesis,
i23 != i49 ).
cnf(u5705,hypothesis,
i23 != i50 ).
cnf(u5710,hypothesis,
i24 != i25 ).
cnf(u5715,hypothesis,
i24 != i26 ).
cnf(u5720,hypothesis,
i24 != i27 ).
cnf(u5725,hypothesis,
i24 != i28 ).
cnf(u5730,hypothesis,
i24 != i29 ).
cnf(u5735,hypothesis,
i24 != i30 ).
cnf(u5740,hypothesis,
i24 != i31 ).
cnf(u5745,hypothesis,
i24 != i32 ).
cnf(u5750,hypothesis,
i24 != i33 ).
cnf(u5755,hypothesis,
i24 != i34 ).
cnf(u5760,hypothesis,
i24 != i35 ).
cnf(u5765,hypothesis,
i24 != i36 ).
cnf(u5770,hypothesis,
i24 != i37 ).
cnf(u5775,hypothesis,
i24 != i38 ).
cnf(u5780,hypothesis,
i24 != i39 ).
cnf(u5785,hypothesis,
i24 != i40 ).
cnf(u5790,hypothesis,
i24 != i41 ).
cnf(u5795,hypothesis,
i24 != i42 ).
cnf(u5800,hypothesis,
i24 != i43 ).
cnf(u5805,hypothesis,
i24 != i44 ).
cnf(u5810,hypothesis,
i24 != i45 ).
cnf(u5815,hypothesis,
i24 != i46 ).
cnf(u5820,hypothesis,
i24 != i47 ).
cnf(u5825,hypothesis,
i24 != i48 ).
cnf(u5830,hypothesis,
i24 != i49 ).
cnf(u5835,hypothesis,
i24 != i50 ).
cnf(u5840,hypothesis,
i25 != i26 ).
cnf(u5845,hypothesis,
i25 != i27 ).
cnf(u5850,hypothesis,
i25 != i28 ).
cnf(u5855,hypothesis,
i25 != i29 ).
cnf(u5860,hypothesis,
i25 != i30 ).
cnf(u5865,hypothesis,
i25 != i31 ).
cnf(u5870,hypothesis,
i25 != i32 ).
cnf(u5875,hypothesis,
i25 != i33 ).
cnf(u5880,hypothesis,
i25 != i34 ).
cnf(u5885,hypothesis,
i25 != i35 ).
cnf(u5890,hypothesis,
i25 != i36 ).
cnf(u5895,hypothesis,
i25 != i37 ).
cnf(u5900,hypothesis,
i25 != i38 ).
cnf(u5905,hypothesis,
i25 != i39 ).
cnf(u5910,hypothesis,
i25 != i40 ).
cnf(u5915,hypothesis,
i25 != i41 ).
cnf(u5920,hypothesis,
i25 != i42 ).
cnf(u5925,hypothesis,
i25 != i43 ).
cnf(u5930,hypothesis,
i25 != i44 ).
cnf(u5935,hypothesis,
i25 != i45 ).
cnf(u5940,hypothesis,
i25 != i46 ).
cnf(u5945,hypothesis,
i25 != i47 ).
cnf(u5950,hypothesis,
i25 != i48 ).
cnf(u5955,hypothesis,
i25 != i49 ).
cnf(u5960,hypothesis,
i25 != i50 ).
cnf(u5965,hypothesis,
i26 != i27 ).
cnf(u5970,hypothesis,
i26 != i28 ).
cnf(u5975,hypothesis,
i26 != i29 ).
cnf(u5980,hypothesis,
i26 != i30 ).
cnf(u5985,hypothesis,
i26 != i31 ).
cnf(u5990,hypothesis,
i26 != i32 ).
cnf(u5995,hypothesis,
i26 != i33 ).
cnf(u6000,hypothesis,
i26 != i34 ).
cnf(u6005,hypothesis,
i26 != i35 ).
cnf(u6010,hypothesis,
i26 != i36 ).
cnf(u6015,hypothesis,
i26 != i37 ).
cnf(u6020,hypothesis,
i26 != i38 ).
cnf(u6025,hypothesis,
i26 != i39 ).
cnf(u6030,hypothesis,
i26 != i40 ).
cnf(u6035,hypothesis,
i26 != i41 ).
cnf(u6040,hypothesis,
i26 != i42 ).
cnf(u6045,hypothesis,
i26 != i43 ).
cnf(u6050,hypothesis,
i26 != i44 ).
cnf(u6055,hypothesis,
i26 != i45 ).
cnf(u6060,hypothesis,
i26 != i46 ).
cnf(u6065,hypothesis,
i26 != i47 ).
cnf(u6070,hypothesis,
i26 != i48 ).
cnf(u6075,hypothesis,
i26 != i49 ).
cnf(u6080,hypothesis,
i26 != i50 ).
cnf(u6085,hypothesis,
i27 != i28 ).
cnf(u6090,hypothesis,
i27 != i29 ).
cnf(u6095,hypothesis,
i27 != i30 ).
cnf(u6100,hypothesis,
i27 != i31 ).
cnf(u6105,hypothesis,
i27 != i32 ).
cnf(u6110,hypothesis,
i27 != i33 ).
cnf(u6115,hypothesis,
i27 != i34 ).
cnf(u6120,hypothesis,
i27 != i35 ).
cnf(u6125,hypothesis,
i27 != i36 ).
cnf(u6130,hypothesis,
i27 != i37 ).
cnf(u6135,hypothesis,
i27 != i38 ).
cnf(u6140,hypothesis,
i27 != i39 ).
cnf(u6145,hypothesis,
i27 != i40 ).
cnf(u6150,hypothesis,
i27 != i41 ).
cnf(u6155,hypothesis,
i27 != i42 ).
cnf(u6160,hypothesis,
i27 != i43 ).
cnf(u6165,hypothesis,
i27 != i44 ).
cnf(u6170,hypothesis,
i27 != i45 ).
cnf(u6175,hypothesis,
i27 != i46 ).
cnf(u6180,hypothesis,
i27 != i47 ).
cnf(u6185,hypothesis,
i27 != i48 ).
cnf(u6190,hypothesis,
i27 != i49 ).
cnf(u6195,hypothesis,
i27 != i50 ).
cnf(u6200,hypothesis,
i28 != i29 ).
cnf(u6205,hypothesis,
i28 != i30 ).
cnf(u6210,hypothesis,
i28 != i31 ).
cnf(u6215,hypothesis,
i28 != i32 ).
cnf(u6220,hypothesis,
i28 != i33 ).
cnf(u6225,hypothesis,
i28 != i34 ).
cnf(u6230,hypothesis,
i28 != i35 ).
cnf(u6235,hypothesis,
i28 != i36 ).
cnf(u6240,hypothesis,
i28 != i37 ).
cnf(u6245,hypothesis,
i28 != i38 ).
cnf(u6250,hypothesis,
i28 != i39 ).
cnf(u6255,hypothesis,
i28 != i40 ).
cnf(u6260,hypothesis,
i28 != i41 ).
cnf(u6265,hypothesis,
i28 != i42 ).
cnf(u6270,hypothesis,
i28 != i43 ).
cnf(u6275,hypothesis,
i28 != i44 ).
cnf(u6280,hypothesis,
i28 != i45 ).
cnf(u6285,hypothesis,
i28 != i46 ).
cnf(u6290,hypothesis,
i28 != i47 ).
cnf(u6295,hypothesis,
i28 != i48 ).
cnf(u6300,hypothesis,
i28 != i49 ).
cnf(u6305,hypothesis,
i28 != i50 ).
cnf(u6310,hypothesis,
i29 != i30 ).
cnf(u6315,hypothesis,
i29 != i31 ).
cnf(u6320,hypothesis,
i29 != i32 ).
cnf(u6325,hypothesis,
i29 != i33 ).
cnf(u6330,hypothesis,
i29 != i34 ).
cnf(u6335,hypothesis,
i29 != i35 ).
cnf(u6340,hypothesis,
i29 != i36 ).
cnf(u6345,hypothesis,
i29 != i37 ).
cnf(u6350,hypothesis,
i29 != i38 ).
cnf(u6355,hypothesis,
i29 != i39 ).
cnf(u6360,hypothesis,
i29 != i40 ).
cnf(u6365,hypothesis,
i29 != i41 ).
cnf(u6370,hypothesis,
i29 != i42 ).
cnf(u6375,hypothesis,
i29 != i43 ).
cnf(u6380,hypothesis,
i29 != i44 ).
cnf(u6385,hypothesis,
i29 != i45 ).
cnf(u6390,hypothesis,
i29 != i46 ).
cnf(u6395,hypothesis,
i29 != i47 ).
cnf(u6400,hypothesis,
i29 != i48 ).
cnf(u6405,hypothesis,
i29 != i49 ).
cnf(u6410,hypothesis,
i29 != i50 ).
cnf(u6415,hypothesis,
i30 != i31 ).
cnf(u6420,hypothesis,
i30 != i32 ).
cnf(u6425,hypothesis,
i30 != i33 ).
cnf(u6430,hypothesis,
i30 != i34 ).
cnf(u6435,hypothesis,
i30 != i35 ).
cnf(u6440,hypothesis,
i30 != i36 ).
cnf(u6445,hypothesis,
i30 != i37 ).
cnf(u6450,hypothesis,
i30 != i38 ).
cnf(u6455,hypothesis,
i30 != i39 ).
cnf(u6460,hypothesis,
i30 != i40 ).
cnf(u6465,hypothesis,
i30 != i41 ).
cnf(u6470,hypothesis,
i30 != i42 ).
cnf(u6475,hypothesis,
i30 != i43 ).
cnf(u6480,hypothesis,
i30 != i44 ).
cnf(u6485,hypothesis,
i30 != i45 ).
cnf(u6490,hypothesis,
i30 != i46 ).
cnf(u6495,hypothesis,
i30 != i47 ).
cnf(u6500,hypothesis,
i30 != i48 ).
cnf(u6505,hypothesis,
i30 != i49 ).
cnf(u6510,hypothesis,
i30 != i50 ).
cnf(u6515,hypothesis,
i31 != i32 ).
cnf(u6520,hypothesis,
i31 != i33 ).
cnf(u6525,hypothesis,
i31 != i34 ).
cnf(u6530,hypothesis,
i31 != i35 ).
cnf(u6535,hypothesis,
i31 != i36 ).
cnf(u6540,hypothesis,
i31 != i37 ).
cnf(u6545,hypothesis,
i31 != i38 ).
cnf(u6550,hypothesis,
i31 != i39 ).
cnf(u6555,hypothesis,
i31 != i40 ).
cnf(u6560,hypothesis,
i31 != i41 ).
cnf(u6565,hypothesis,
i31 != i42 ).
cnf(u6570,hypothesis,
i31 != i43 ).
cnf(u6575,hypothesis,
i31 != i44 ).
cnf(u6580,hypothesis,
i31 != i45 ).
cnf(u6585,hypothesis,
i31 != i46 ).
cnf(u6590,hypothesis,
i31 != i47 ).
cnf(u6595,hypothesis,
i31 != i48 ).
cnf(u6600,hypothesis,
i31 != i49 ).
cnf(u6605,hypothesis,
i31 != i50 ).
cnf(u6610,hypothesis,
i32 != i33 ).
cnf(u6615,hypothesis,
i32 != i34 ).
cnf(u6620,hypothesis,
i32 != i35 ).
cnf(u6625,hypothesis,
i32 != i36 ).
cnf(u6630,hypothesis,
i32 != i37 ).
cnf(u6635,hypothesis,
i32 != i38 ).
cnf(u6640,hypothesis,
i32 != i39 ).
cnf(u6645,hypothesis,
i32 != i40 ).
cnf(u6650,hypothesis,
i32 != i41 ).
cnf(u6655,hypothesis,
i32 != i42 ).
cnf(u6660,hypothesis,
i32 != i43 ).
cnf(u6665,hypothesis,
i32 != i44 ).
cnf(u6670,hypothesis,
i32 != i45 ).
cnf(u6675,hypothesis,
i32 != i46 ).
cnf(u6680,hypothesis,
i32 != i47 ).
cnf(u6685,hypothesis,
i32 != i48 ).
cnf(u6690,hypothesis,
i32 != i49 ).
cnf(u6695,hypothesis,
i32 != i50 ).
cnf(u6700,hypothesis,
i33 != i34 ).
cnf(u6705,hypothesis,
i33 != i35 ).
cnf(u6710,hypothesis,
i33 != i36 ).
cnf(u6715,hypothesis,
i33 != i37 ).
cnf(u6720,hypothesis,
i33 != i38 ).
cnf(u6725,hypothesis,
i33 != i39 ).
cnf(u6730,hypothesis,
i33 != i40 ).
cnf(u6735,hypothesis,
i33 != i41 ).
cnf(u6740,hypothesis,
i33 != i42 ).
cnf(u6745,hypothesis,
i33 != i43 ).
cnf(u6750,hypothesis,
i33 != i44 ).
cnf(u6755,hypothesis,
i33 != i45 ).
cnf(u6760,hypothesis,
i33 != i46 ).
cnf(u6765,hypothesis,
i33 != i47 ).
cnf(u6770,hypothesis,
i33 != i48 ).
cnf(u6775,hypothesis,
i33 != i49 ).
cnf(u6780,hypothesis,
i33 != i50 ).
cnf(u6785,hypothesis,
i34 != i35 ).
cnf(u6790,hypothesis,
i34 != i36 ).
cnf(u6795,hypothesis,
i34 != i37 ).
cnf(u6800,hypothesis,
i34 != i38 ).
cnf(u6805,hypothesis,
i34 != i39 ).
cnf(u6810,hypothesis,
i34 != i40 ).
cnf(u6815,hypothesis,
i34 != i41 ).
cnf(u6820,hypothesis,
i34 != i42 ).
cnf(u6825,hypothesis,
i34 != i43 ).
cnf(u6830,hypothesis,
i34 != i44 ).
cnf(u6835,hypothesis,
i34 != i45 ).
cnf(u6840,hypothesis,
i34 != i46 ).
cnf(u6845,hypothesis,
i34 != i47 ).
cnf(u6850,hypothesis,
i34 != i48 ).
cnf(u6855,hypothesis,
i34 != i49 ).
cnf(u6860,hypothesis,
i34 != i50 ).
cnf(u6865,hypothesis,
i35 != i36 ).
cnf(u6870,hypothesis,
i35 != i37 ).
cnf(u6875,hypothesis,
i35 != i38 ).
cnf(u6880,hypothesis,
i35 != i39 ).
cnf(u6885,hypothesis,
i35 != i40 ).
cnf(u6890,hypothesis,
i35 != i41 ).
cnf(u6895,hypothesis,
i35 != i42 ).
cnf(u6900,hypothesis,
i35 != i43 ).
cnf(u6905,hypothesis,
i35 != i44 ).
cnf(u6910,hypothesis,
i35 != i45 ).
cnf(u6915,hypothesis,
i35 != i46 ).
cnf(u6920,hypothesis,
i35 != i47 ).
cnf(u6925,hypothesis,
i35 != i48 ).
cnf(u6930,hypothesis,
i35 != i49 ).
cnf(u6935,hypothesis,
i35 != i50 ).
cnf(u6940,hypothesis,
i36 != i37 ).
cnf(u6945,hypothesis,
i36 != i38 ).
cnf(u6950,hypothesis,
i36 != i39 ).
cnf(u6955,hypothesis,
i36 != i40 ).
cnf(u6960,hypothesis,
i36 != i41 ).
cnf(u6965,hypothesis,
i36 != i42 ).
cnf(u6970,hypothesis,
i36 != i43 ).
cnf(u6975,hypothesis,
i36 != i44 ).
cnf(u6980,hypothesis,
i36 != i45 ).
cnf(u6985,hypothesis,
i36 != i46 ).
cnf(u6990,hypothesis,
i36 != i47 ).
cnf(u6995,hypothesis,
i36 != i48 ).
cnf(u7000,hypothesis,
i36 != i49 ).
cnf(u7005,hypothesis,
i36 != i50 ).
cnf(u7010,hypothesis,
i37 != i38 ).
cnf(u7015,hypothesis,
i37 != i39 ).
cnf(u7020,hypothesis,
i37 != i40 ).
cnf(u7025,hypothesis,
i37 != i41 ).
cnf(u7030,hypothesis,
i37 != i42 ).
cnf(u7035,hypothesis,
i37 != i43 ).
cnf(u7040,hypothesis,
i37 != i44 ).
cnf(u7045,hypothesis,
i37 != i45 ).
cnf(u7050,hypothesis,
i37 != i46 ).
cnf(u7055,hypothesis,
i37 != i47 ).
cnf(u7060,hypothesis,
i37 != i48 ).
cnf(u7065,hypothesis,
i37 != i49 ).
cnf(u7070,hypothesis,
i37 != i50 ).
cnf(u7075,hypothesis,
i38 != i39 ).
cnf(u7080,hypothesis,
i38 != i40 ).
cnf(u7085,hypothesis,
i38 != i41 ).
cnf(u7090,hypothesis,
i38 != i42 ).
cnf(u7095,hypothesis,
i38 != i43 ).
cnf(u7100,hypothesis,
i38 != i44 ).
cnf(u7105,hypothesis,
i38 != i45 ).
cnf(u7110,hypothesis,
i38 != i46 ).
cnf(u7115,hypothesis,
i38 != i47 ).
cnf(u7120,hypothesis,
i38 != i48 ).
cnf(u7125,hypothesis,
i38 != i49 ).
cnf(u7130,hypothesis,
i38 != i50 ).
cnf(u7135,hypothesis,
i39 != i40 ).
cnf(u7140,hypothesis,
i39 != i41 ).
cnf(u7145,hypothesis,
i39 != i42 ).
cnf(u7150,hypothesis,
i39 != i43 ).
cnf(u7155,hypothesis,
i39 != i44 ).
cnf(u7160,hypothesis,
i39 != i45 ).
cnf(u7165,hypothesis,
i39 != i46 ).
cnf(u7170,hypothesis,
i39 != i47 ).
cnf(u7175,hypothesis,
i39 != i48 ).
cnf(u7180,hypothesis,
i39 != i49 ).
cnf(u7185,hypothesis,
i39 != i50 ).
cnf(u7190,hypothesis,
i40 != i41 ).
cnf(u7195,hypothesis,
i40 != i42 ).
cnf(u7200,hypothesis,
i40 != i43 ).
cnf(u7205,hypothesis,
i40 != i44 ).
cnf(u7210,hypothesis,
i40 != i45 ).
cnf(u7215,hypothesis,
i40 != i46 ).
cnf(u7220,hypothesis,
i40 != i47 ).
cnf(u7225,hypothesis,
i40 != i48 ).
cnf(u7230,hypothesis,
i40 != i49 ).
cnf(u7235,hypothesis,
i40 != i50 ).
cnf(u7240,hypothesis,
i41 != i42 ).
cnf(u7245,hypothesis,
i41 != i43 ).
cnf(u7250,hypothesis,
i41 != i44 ).
cnf(u7255,hypothesis,
i41 != i45 ).
cnf(u7260,hypothesis,
i41 != i46 ).
cnf(u7265,hypothesis,
i41 != i47 ).
cnf(u7270,hypothesis,
i41 != i48 ).
cnf(u7275,hypothesis,
i41 != i49 ).
cnf(u7280,hypothesis,
i41 != i50 ).
cnf(u7285,hypothesis,
i42 != i43 ).
cnf(u7290,hypothesis,
i42 != i44 ).
cnf(u7295,hypothesis,
i42 != i45 ).
cnf(u7300,hypothesis,
i42 != i46 ).
cnf(u7305,hypothesis,
i42 != i47 ).
cnf(u7310,hypothesis,
i42 != i48 ).
cnf(u7315,hypothesis,
i42 != i49 ).
cnf(u7320,hypothesis,
i42 != i50 ).
cnf(u7325,hypothesis,
i43 != i44 ).
cnf(u7330,hypothesis,
i43 != i45 ).
cnf(u7335,hypothesis,
i43 != i46 ).
cnf(u7340,hypothesis,
i43 != i47 ).
cnf(u7345,hypothesis,
i43 != i48 ).
cnf(u7350,hypothesis,
i43 != i49 ).
cnf(u7355,hypothesis,
i43 != i50 ).
cnf(u7360,hypothesis,
i44 != i45 ).
cnf(u7365,hypothesis,
i44 != i46 ).
cnf(u7370,hypothesis,
i44 != i47 ).
cnf(u7375,hypothesis,
i44 != i48 ).
cnf(u7380,hypothesis,
i44 != i49 ).
cnf(u7385,hypothesis,
i44 != i50 ).
cnf(u7390,hypothesis,
i45 != i46 ).
cnf(u7395,hypothesis,
i45 != i47 ).
cnf(u7400,hypothesis,
i45 != i48 ).
cnf(u7405,hypothesis,
i45 != i49 ).
cnf(u7410,hypothesis,
i45 != i50 ).
cnf(u7415,hypothesis,
i46 != i47 ).
cnf(u7420,hypothesis,
i46 != i48 ).
cnf(u7425,hypothesis,
i46 != i49 ).
cnf(u7430,hypothesis,
i46 != i50 ).
cnf(u7435,hypothesis,
i47 != i48 ).
cnf(u7440,hypothesis,
i47 != i49 ).
cnf(u7445,hypothesis,
i47 != i50 ).
cnf(u7450,hypothesis,
i48 != i49 ).
cnf(u7455,hypothesis,
i48 != i50 ).
cnf(u7460,hypothesis,
i49 != i50 ).
cnf(u7465,hypothesis,
a_1799 = store(a_1798,i1,e1) ).
cnf(u7470,hypothesis,
a_1798 = store(a_1797,i31,e31) ).
cnf(u7475,hypothesis,
a_1797 = store(a_1796,i21,e21) ).
cnf(u7480,hypothesis,
a_1796 = store(a_1795,i24,e24) ).
cnf(u7485,hypothesis,
a_1795 = store(a_1794,i4,e4) ).
cnf(u7490,hypothesis,
a_1794 = store(a_1793,i32,e32) ).
cnf(u7495,hypothesis,
a_1793 = store(a_1792,i5,e5) ).
cnf(u7500,hypothesis,
a_1792 = store(a_1791,i12,e12) ).
cnf(u7505,hypothesis,
a_1791 = store(a_1790,i37,e37) ).
cnf(u7510,hypothesis,
a_1790 = store(a_1789,i3,e3) ).
cnf(u7515,hypothesis,
a_1789 = store(a_1788,i29,e29) ).
cnf(u7520,hypothesis,
a_1788 = store(a_1787,i48,e48) ).
cnf(u7525,hypothesis,
a_1787 = store(a_1786,i10,e10) ).
cnf(u7530,hypothesis,
a_1786 = store(a_1785,i2,e2) ).
cnf(u7535,negated_conjecture,
a_1785 = sF0 ).
cnf(u7540,hypothesis,
a_1784 = store(a_1783,i35,e35) ).
cnf(u7545,hypothesis,
a_1783 = store(a_1782,i46,e46) ).
cnf(u7550,hypothesis,
a_1782 = store(a_1781,i25,e25) ).
cnf(u7555,hypothesis,
a_1781 = store(a_1780,i23,e23) ).
cnf(u7560,hypothesis,
a_1780 = store(a_1779,i38,e38) ).
cnf(u7565,hypothesis,
a_1779 = store(a_1778,i44,e44) ).
cnf(u7570,hypothesis,
a_1778 = store(a_1777,i36,e36) ).
cnf(u7575,hypothesis,
a_1777 = store(a_1776,i11,e11) ).
cnf(u7580,hypothesis,
a_1776 = store(a_1775,i34,e34) ).
cnf(u7585,hypothesis,
a_1775 = store(a_1774,i26,e26) ).
cnf(u7590,hypothesis,
a_1774 = store(a_1773,i18,e18) ).
cnf(u7595,hypothesis,
a_1773 = store(a_1772,i47,e47) ).
cnf(u7600,hypothesis,
a_1772 = store(a_1771,i42,e42) ).
cnf(u7605,hypothesis,
a_1771 = store(a_1770,i17,e17) ).
cnf(u7610,hypothesis,
a_1770 = store(a_1769,i9,e9) ).
cnf(u7615,hypothesis,
a_1769 = store(a_1768,i33,e33) ).
cnf(u7620,hypothesis,
a_1768 = store(a_1767,i7,e7) ).
cnf(u7625,hypothesis,
a_1767 = store(a_1766,i15,e15) ).
cnf(u7630,hypothesis,
a_1766 = store(a_1765,i27,e27) ).
cnf(u7635,hypothesis,
a_1765 = store(a_1764,i6,e6) ).
cnf(u7640,hypothesis,
a_1764 = store(a_1763,i13,e13) ).
cnf(u7645,hypothesis,
a_1763 = store(a_1762,i14,e14) ).
cnf(u7650,hypothesis,
a_1762 = store(a_1761,i49,e49) ).
cnf(u7655,hypothesis,
a_1761 = store(a_1760,i8,e8) ).
cnf(u7660,hypothesis,
a_1760 = store(a_1759,i16,e16) ).
cnf(u7665,hypothesis,
a_1759 = store(a_1758,i40,e40) ).
cnf(u7670,hypothesis,
a_1758 = store(a_1757,i20,e20) ).
cnf(u7675,hypothesis,
a_1757 = store(a_1756,i39,e39) ).
cnf(u7680,hypothesis,
a_1756 = store(a_1755,i22,e22) ).
cnf(u7685,hypothesis,
a_1755 = store(a_1754,i19,e19) ).
cnf(u7690,hypothesis,
a_1754 = store(a_1753,i28,e28) ).
cnf(u7695,hypothesis,
a_1753 = store(a_1752,i43,e43) ).
cnf(u7700,hypothesis,
a_1752 = store(a_1751,i45,e45) ).
cnf(u7705,hypothesis,
a_1751 = store(a_1750,i30,e30) ).
cnf(u7710,hypothesis,
a_1750 = store(a1,i41,e41) ).
cnf(u7715,hypothesis,
a_1749 = store(a_1748,i1,e1) ).
cnf(u7720,hypothesis,
a_1748 = store(a_1747,i49,e49) ).
cnf(u7725,hypothesis,
a_1747 = store(a_1746,i48,e48) ).
cnf(u7730,hypothesis,
a_1746 = store(a_1745,i47,e47) ).
cnf(u7735,hypothesis,
a_1745 = store(a_1744,i46,e46) ).
cnf(u7740,hypothesis,
a_1744 = store(a_1743,i45,e45) ).
cnf(u7745,hypothesis,
a_1743 = store(a_1742,i44,e44) ).
cnf(u7750,hypothesis,
a_1742 = store(a_1741,i43,e43) ).
cnf(u7755,hypothesis,
a_1741 = store(a_1740,i42,e42) ).
cnf(u7760,hypothesis,
a_1740 = store(a_1739,i41,e41) ).
cnf(u7765,hypothesis,
a_1739 = store(a_1738,i40,e40) ).
cnf(u7770,hypothesis,
a_1738 = store(a_1737,i39,e39) ).
cnf(u7775,hypothesis,
a_1737 = store(a_1736,i38,e38) ).
cnf(u7780,hypothesis,
a_1736 = store(a_1735,i37,e37) ).
cnf(u7785,hypothesis,
a_1735 = store(a_1734,i36,e36) ).
cnf(u7790,hypothesis,
a_1734 = store(a_1733,i35,e35) ).
cnf(u7795,hypothesis,
a_1733 = store(a_1732,i34,e34) ).
cnf(u7800,hypothesis,
a_1732 = store(a_1731,i33,e33) ).
cnf(u7805,hypothesis,
a_1731 = store(a_1730,i32,e32) ).
cnf(u7810,hypothesis,
a_1730 = store(a_1729,i31,e31) ).
cnf(u7815,hypothesis,
a_1729 = store(a_1728,i30,e30) ).
cnf(u7820,hypothesis,
a_1728 = store(a_1727,i29,e29) ).
cnf(u7825,hypothesis,
a_1727 = store(a_1726,i28,e28) ).
cnf(u7830,hypothesis,
a_1726 = store(a_1725,i27,e27) ).
cnf(u7835,hypothesis,
a_1725 = store(a_1724,i26,e26) ).
cnf(u7840,hypothesis,
a_1724 = store(a_1723,i25,e25) ).
cnf(u7845,hypothesis,
a_1723 = store(a_1722,i24,e24) ).
cnf(u7850,hypothesis,
a_1722 = store(a_1721,i23,e23) ).
cnf(u7855,hypothesis,
a_1721 = store(a_1720,i22,e22) ).
cnf(u7860,hypothesis,
a_1720 = store(a_1719,i21,e21) ).
cnf(u7865,hypothesis,
a_1719 = store(a_1718,i20,e20) ).
cnf(u7870,hypothesis,
a_1718 = store(a_1717,i19,e19) ).
cnf(u7875,hypothesis,
a_1717 = store(a_1716,i18,e18) ).
cnf(u7880,hypothesis,
a_1716 = store(a_1715,i17,e17) ).
cnf(u7885,hypothesis,
a_1715 = store(a_1714,i16,e16) ).
cnf(u7890,hypothesis,
a_1714 = store(a_1713,i15,e15) ).
cnf(u7895,hypothesis,
a_1713 = store(a_1712,i14,e14) ).
cnf(u7900,hypothesis,
a_1712 = store(a_1711,i13,e13) ).
cnf(u7905,hypothesis,
a_1711 = store(a_1710,i12,e12) ).
cnf(u7910,hypothesis,
a_1710 = store(a_1709,i11,e11) ).
cnf(u7915,hypothesis,
a_1709 = store(a_1708,i10,e10) ).
cnf(u7920,hypothesis,
a_1708 = store(a_1707,i9,e9) ).
cnf(u7925,hypothesis,
a_1707 = store(a_1706,i8,e8) ).
cnf(u7930,hypothesis,
a_1706 = store(a_1705,i7,e7) ).
cnf(u7935,hypothesis,
a_1705 = store(a_1704,i6,e6) ).
cnf(u7940,hypothesis,
a_1704 = store(a_1703,i5,e5) ).
cnf(u7945,hypothesis,
a_1703 = store(a_1702,i4,e4) ).
cnf(u7950,hypothesis,
a_1702 = store(a_1701,i3,e3) ).
cnf(u7955,hypothesis,
a_1701 = store(a_1700,i2,e2) ).
cnf(u7960,hypothesis,
a_1700 = store(a1,i1,e1) ).
cnf(u7965,axiom,
store(a_1784,i50,e50) = sF0 ).
cnf(u7971,negated_conjecture,
a_1785 = store(a_1784,i50,e50) ).
cnf(u8076,hypothesis,
e1 = select(a_1799,i1) ).
cnf(u8081,hypothesis,
e31 = select(a_1798,i31) ).
cnf(u8086,hypothesis,
e21 = select(a_1797,i21) ).
cnf(u8091,hypothesis,
e24 = select(a_1796,i24) ).
cnf(u8096,hypothesis,
e4 = select(a_1795,i4) ).
cnf(u8101,hypothesis,
e32 = select(a_1794,i32) ).
cnf(u8106,hypothesis,
e5 = select(a_1793,i5) ).
cnf(u8111,hypothesis,
e12 = select(a_1792,i12) ).
cnf(u8116,hypothesis,
e37 = select(a_1791,i37) ).
cnf(u8121,hypothesis,
e3 = select(a_1790,i3) ).
cnf(u8126,hypothesis,
e29 = select(a_1789,i29) ).
cnf(u8131,hypothesis,
e48 = select(a_1788,i48) ).
cnf(u8136,hypothesis,
e10 = select(a_1787,i10) ).
cnf(u8141,hypothesis,
e2 = select(a_1786,i2) ).
cnf(u8146,negated_conjecture,
e50 = select(a_1785,i50) ).
cnf(u8151,hypothesis,
e35 = select(a_1784,i35) ).
cnf(u8156,hypothesis,
e46 = select(a_1783,i46) ).
cnf(u8161,hypothesis,
e25 = select(a_1782,i25) ).
cnf(u8166,hypothesis,
e23 = select(a_1781,i23) ).
cnf(u8171,hypothesis,
e38 = select(a_1780,i38) ).
cnf(u8176,hypothesis,
e44 = select(a_1779,i44) ).
cnf(u8181,hypothesis,
e36 = select(a_1778,i36) ).
cnf(u8186,hypothesis,
e11 = select(a_1777,i11) ).
cnf(u8191,hypothesis,
e34 = select(a_1776,i34) ).
cnf(u8196,hypothesis,
e26 = select(a_1775,i26) ).
cnf(u8201,hypothesis,
e18 = select(a_1774,i18) ).
cnf(u8206,hypothesis,
e47 = select(a_1773,i47) ).
cnf(u8211,hypothesis,
e42 = select(a_1772,i42) ).
cnf(u8216,hypothesis,
e17 = select(a_1771,i17) ).
cnf(u8221,hypothesis,
e9 = select(a_1770,i9) ).
cnf(u8226,hypothesis,
e33 = select(a_1769,i33) ).
cnf(u8231,hypothesis,
e7 = select(a_1768,i7) ).
cnf(u8236,hypothesis,
e15 = select(a_1767,i15) ).
cnf(u8241,hypothesis,
e27 = select(a_1766,i27) ).
cnf(u8246,hypothesis,
e6 = select(a_1765,i6) ).
cnf(u8251,hypothesis,
e13 = select(a_1764,i13) ).
cnf(u8256,hypothesis,
e14 = select(a_1763,i14) ).
cnf(u8261,hypothesis,
e49 = select(a_1762,i49) ).
cnf(u8266,hypothesis,
e8 = select(a_1761,i8) ).
cnf(u8271,hypothesis,
e16 = select(a_1760,i16) ).
cnf(u8276,hypothesis,
e40 = select(a_1759,i40) ).
cnf(u8281,hypothesis,
e20 = select(a_1758,i20) ).
cnf(u8286,hypothesis,
e39 = select(a_1757,i39) ).
cnf(u8291,hypothesis,
e22 = select(a_1756,i22) ).
cnf(u8296,hypothesis,
e19 = select(a_1755,i19) ).
cnf(u8301,hypothesis,
e28 = select(a_1754,i28) ).
cnf(u8306,hypothesis,
e43 = select(a_1753,i43) ).
cnf(u8311,hypothesis,
e45 = select(a_1752,i45) ).
cnf(u8316,hypothesis,
e30 = select(a_1751,i30) ).
cnf(u8321,hypothesis,
e1 = select(a_1749,i1) ).
cnf(u8326,hypothesis,
e49 = select(a_1748,i49) ).
cnf(u8331,hypothesis,
e48 = select(a_1747,i48) ).
cnf(u8336,hypothesis,
e47 = select(a_1746,i47) ).
cnf(u8341,hypothesis,
e46 = select(a_1745,i46) ).
cnf(u8346,hypothesis,
e45 = select(a_1744,i45) ).
cnf(u8351,hypothesis,
e44 = select(a_1743,i44) ).
cnf(u8356,hypothesis,
e43 = select(a_1742,i43) ).
cnf(u8361,hypothesis,
e42 = select(a_1741,i42) ).
cnf(u8366,hypothesis,
e41 = select(a_1740,i41) ).
cnf(u8371,hypothesis,
e40 = select(a_1739,i40) ).
cnf(u8376,hypothesis,
e39 = select(a_1738,i39) ).
cnf(u8381,hypothesis,
e38 = select(a_1737,i38) ).
cnf(u8386,hypothesis,
e37 = select(a_1736,i37) ).
cnf(u8391,hypothesis,
e36 = select(a_1735,i36) ).
cnf(u8396,hypothesis,
e35 = select(a_1734,i35) ).
cnf(u8401,hypothesis,
e34 = select(a_1733,i34) ).
cnf(u8406,hypothesis,
e33 = select(a_1732,i33) ).
cnf(u8411,hypothesis,
e32 = select(a_1731,i32) ).
cnf(u8416,hypothesis,
e31 = select(a_1730,i31) ).
cnf(u8421,hypothesis,
e30 = select(a_1729,i30) ).
cnf(u8426,hypothesis,
e29 = select(a_1728,i29) ).
cnf(u8431,hypothesis,
e28 = select(a_1727,i28) ).
cnf(u8436,hypothesis,
e27 = select(a_1726,i27) ).
cnf(u8441,hypothesis,
e26 = select(a_1725,i26) ).
cnf(u8446,hypothesis,
e25 = select(a_1724,i25) ).
cnf(u8451,hypothesis,
e24 = select(a_1723,i24) ).
cnf(u8456,hypothesis,
e23 = select(a_1722,i23) ).
cnf(u8461,hypothesis,
e22 = select(a_1721,i22) ).
cnf(u8466,hypothesis,
e21 = select(a_1720,i21) ).
cnf(u8471,hypothesis,
e20 = select(a_1719,i20) ).
cnf(u8476,hypothesis,
e19 = select(a_1718,i19) ).
cnf(u8481,hypothesis,
e18 = select(a_1717,i18) ).
cnf(u8486,hypothesis,
e17 = select(a_1716,i17) ).
cnf(u8491,hypothesis,
e16 = select(a_1715,i16) ).
cnf(u8496,hypothesis,
e15 = select(a_1714,i15) ).
cnf(u8501,hypothesis,
e14 = select(a_1713,i14) ).
cnf(u8506,hypothesis,
e13 = select(a_1712,i13) ).
cnf(u8511,hypothesis,
e12 = select(a_1711,i12) ).
cnf(u8516,hypothesis,
e11 = select(a_1710,i11) ).
cnf(u8521,hypothesis,
e10 = select(a_1709,i10) ).
cnf(u8526,hypothesis,
e9 = select(a_1708,i9) ).
cnf(u8531,hypothesis,
e8 = select(a_1707,i8) ).
cnf(u8536,hypothesis,
e7 = select(a_1706,i7) ).
cnf(u8541,hypothesis,
e6 = select(a_1705,i6) ).
cnf(u8546,hypothesis,
e5 = select(a_1704,i5) ).
cnf(u8551,hypothesis,
e4 = select(a_1703,i4) ).
cnf(u8556,hypothesis,
e3 = select(a_1702,i3) ).
cnf(u8561,hypothesis,
e1 = select(a_1700,i1) ).
cnf(u8566,hypothesis,
e41 = select(a_1750,i41) ).
cnf(u8571,hypothesis,
e2 = select(a_1701,i2) ).
cnf(u8606,hypothesis,
( select(a_1731,X0) = select(a_1732,X0)
| i33 = X0 ) ).
cnf(u8583,hypothesis,
( select(a_1708,X0) = select(a_1709,X0)
| i10 = X0 ) ).
cnf(u8616,hypothesis,
( select(a_1741,X0) = select(a_1742,X0)
| i43 = X0 ) ).
cnf(u8608,hypothesis,
( select(a_1733,X0) = select(a_1734,X0)
| i35 = X0 ) ).
cnf(u8669,hypothesis,
( select(a_1795,X0) = select(a_1796,X0)
| i24 = X0 ) ).
cnf(u8579,hypothesis,
( select(a_1704,X0) = select(a_1705,X0)
| i6 = X0 ) ).
cnf(u8580,hypothesis,
( select(a_1705,X0) = select(a_1706,X0)
| i7 = X0 ) ).
cnf(u8628,hypothesis,
( select(a_1754,X0) = select(a_1755,X0)
| i19 = X0 ) ).
cnf(u8655,hypothesis,
( select(a_1781,X0) = select(a_1782,X0)
| i25 = X0 ) ).
cnf(u8637,hypothesis,
( select(a_1763,X0) = select(a_1764,X0)
| i13 = X0 ) ).
cnf(u8602,hypothesis,
( select(a_1727,X0) = select(a_1728,X0)
| i29 = X0 ) ).
cnf(u8622,hypothesis,
( select(a_1747,X0) = select(a_1748,X0)
| i49 = X0 ) ).
cnf(u8594,hypothesis,
( select(a_1719,X0) = select(a_1720,X0)
| i21 = X0 ) ).
cnf(u8649,hypothesis,
( select(a_1775,X0) = select(a_1776,X0)
| i34 = X0 ) ).
cnf(u8659,hypothesis,
( select(a_1785,X0) = select(a_1786,X0)
| i2 = X0 ) ).
cnf(u8656,hypothesis,
( select(a_1782,X0) = select(a_1783,X0)
| i46 = X0 ) ).
cnf(u8625,hypothesis,
( select(a_1751,X0) = select(a_1752,X0)
| i45 = X0 ) ).
cnf(u8645,hypothesis,
( select(a_1771,X0) = select(a_1772,X0)
| i42 = X0 ) ).
cnf(u8604,hypothesis,
( select(a_1729,X0) = select(a_1730,X0)
| i31 = X0 ) ).
cnf(u8665,hypothesis,
( select(a_1791,X0) = select(a_1792,X0)
| i12 = X0 ) ).
cnf(u8641,hypothesis,
( select(a_1767,X0) = select(a_1768,X0)
| i7 = X0 ) ).
cnf(u8589,hypothesis,
( select(a_1714,X0) = select(a_1715,X0)
| i16 = X0 ) ).
cnf(u8600,hypothesis,
( select(a_1725,X0) = select(a_1726,X0)
| i27 = X0 ) ).
cnf(u8633,hypothesis,
( select(a_1759,X0) = select(a_1760,X0)
| i16 = X0 ) ).
cnf(u8626,hypothesis,
( select(a_1752,X0) = select(a_1753,X0)
| i43 = X0 ) ).
cnf(u8607,hypothesis,
( select(a_1732,X0) = select(a_1733,X0)
| i34 = X0 ) ).
cnf(u8660,hypothesis,
( select(a_1786,X0) = select(a_1787,X0)
| i10 = X0 ) ).
cnf(u8611,hypothesis,
( select(a_1736,X0) = select(a_1737,X0)
| i38 = X0 ) ).
cnf(u8652,hypothesis,
( select(a_1778,X0) = select(a_1779,X0)
| i44 = X0 ) ).
cnf(u8603,hypothesis,
( select(a_1728,X0) = select(a_1729,X0)
| i30 = X0 ) ).
cnf(u8577,hypothesis,
( select(a_1702,X0) = select(a_1703,X0)
| i4 = X0 ) ).
cnf(u8623,hypothesis,
( select(a_1748,X0) = select(a_1749,X0)
| i1 = X0 ) ).
cnf(u8648,hypothesis,
( select(a_1774,X0) = select(a_1775,X0)
| i26 = X0 ) ).
cnf(u8630,hypothesis,
( select(a_1756,X0) = select(a_1757,X0)
| i39 = X0 ) ).
cnf(u8624,hypothesis,
( select(a_1750,X0) = select(a_1751,X0)
| i30 = X0 ) ).
cnf(u8585,hypothesis,
( select(a_1710,X0) = select(a_1711,X0)
| i12 = X0 ) ).
cnf(u8618,hypothesis,
( select(a_1743,X0) = select(a_1744,X0)
| i45 = X0 ) ).
cnf(u8672,hypothesis,
( select(a_1798,X0) = select(a_1799,X0)
| i1 = X0 ) ).
cnf(u8643,hypothesis,
( select(a_1769,X0) = select(a_1770,X0)
| i9 = X0 ) ).
cnf(u8574,hypothesis,
( select(a1,X0) = select(a_1750,X0)
| i41 = X0 ) ).
cnf(u8657,hypothesis,
( select(a_1783,X0) = select(a_1784,X0)
| i35 = X0 ) ).
cnf(u8575,hypothesis,
( select(a_1700,X0) = select(a1,X0)
| i1 = X0 ) ).
cnf(u8612,hypothesis,
( select(a_1737,X0) = select(a_1738,X0)
| i39 = X0 ) ).
cnf(u8578,hypothesis,
( select(a_1703,X0) = select(a_1704,X0)
| i5 = X0 ) ).
cnf(u8609,hypothesis,
( select(a_1734,X0) = select(a_1735,X0)
| i36 = X0 ) ).
cnf(u8590,hypothesis,
( select(a_1715,X0) = select(a_1716,X0)
| i17 = X0 ) ).
cnf(a2,axiom,
( select(store(X2,X0,X3),X1) = select(X2,X1)
| X0 = X1 ) ).
cnf(u8582,hypothesis,
( select(a_1707,X0) = select(a_1708,X0)
| i9 = X0 ) ).
cnf(u8621,hypothesis,
( select(a_1746,X0) = select(a_1747,X0)
| i48 = X0 ) ).
cnf(u8635,hypothesis,
( select(a_1761,X0) = select(a_1762,X0)
| i49 = X0 ) ).
cnf(u8586,hypothesis,
( select(a_1711,X0) = select(a_1712,X0)
| i13 = X0 ) ).
cnf(u8647,hypothesis,
( select(a_1773,X0) = select(a_1774,X0)
| i18 = X0 ) ).
cnf(u8599,hypothesis,
( select(a_1724,X0) = select(a_1725,X0)
| i26 = X0 ) ).
cnf(u8640,hypothesis,
( select(a_1766,X0) = select(a_1767,X0)
| i15 = X0 ) ).
cnf(u8613,hypothesis,
( select(a_1738,X0) = select(a_1739,X0)
| i40 = X0 ) ).
cnf(u8617,hypothesis,
( select(a_1742,X0) = select(a_1743,X0)
| i44 = X0 ) ).
cnf(u8670,hypothesis,
( select(a_1796,X0) = select(a_1797,X0)
| i21 = X0 ) ).
cnf(u8629,hypothesis,
( select(a_1755,X0) = select(a_1756,X0)
| i22 = X0 ) ).
cnf(u8662,hypothesis,
( select(a_1788,X0) = select(a_1789,X0)
| i29 = X0 ) ).
cnf(u8587,hypothesis,
( select(a_1712,X0) = select(a_1713,X0)
| i14 = X0 ) ).
cnf(u8666,hypothesis,
( select(a_1792,X0) = select(a_1793,X0)
| i5 = X0 ) ).
cnf(u8658,negated_conjecture,
( select(a_1784,X0) = select(a_1785,X0)
| i50 = X0 ) ).
cnf(u8671,hypothesis,
( select(a_1797,X0) = select(a_1798,X0)
| i31 = X0 ) ).
cnf(u8591,hypothesis,
( select(a_1716,X0) = select(a_1717,X0)
| i18 = X0 ) ).
cnf(u8644,hypothesis,
( select(a_1770,X0) = select(a_1771,X0)
| i17 = X0 ) ).
cnf(u8632,hypothesis,
( select(a_1758,X0) = select(a_1759,X0)
| i40 = X0 ) ).
cnf(u8595,hypothesis,
( select(a_1720,X0) = select(a_1721,X0)
| i22 = X0 ) ).
cnf(u8627,hypothesis,
( select(a_1753,X0) = select(a_1754,X0)
| i28 = X0 ) ).
cnf(u8636,hypothesis,
( select(a_1762,X0) = select(a_1763,X0)
| i14 = X0 ) ).
cnf(u8639,hypothesis,
( select(a_1765,X0) = select(a_1766,X0)
| i27 = X0 ) ).
cnf(u8581,hypothesis,
( select(a_1706,X0) = select(a_1707,X0)
| i8 = X0 ) ).
cnf(u8631,hypothesis,
( select(a_1757,X0) = select(a_1758,X0)
| i20 = X0 ) ).
cnf(u8614,hypothesis,
( select(a_1739,X0) = select(a_1740,X0)
| i41 = X0 ) ).
cnf(u8661,hypothesis,
( select(a_1787,X0) = select(a_1788,X0)
| i48 = X0 ) ).
cnf(u8668,hypothesis,
( select(a_1794,X0) = select(a_1795,X0)
| i4 = X0 ) ).
cnf(u8667,hypothesis,
( select(a_1793,X0) = select(a_1794,X0)
| i32 = X0 ) ).
cnf(u8573,hypothesis,
( select(a_1700,X0) = select(a_1701,X0)
| i2 = X0 ) ).
cnf(u8610,hypothesis,
( select(a_1735,X0) = select(a_1736,X0)
| i37 = X0 ) ).
cnf(u8653,hypothesis,
( select(a_1779,X0) = select(a_1780,X0)
| i38 = X0 ) ).
cnf(u8634,hypothesis,
( select(a_1760,X0) = select(a_1761,X0)
| i8 = X0 ) ).
cnf(u8596,hypothesis,
( select(a_1721,X0) = select(a_1722,X0)
| i23 = X0 ) ).
cnf(u8588,hypothesis,
( select(a_1713,X0) = select(a_1714,X0)
| i15 = X0 ) ).
cnf(u8619,hypothesis,
( select(a_1744,X0) = select(a_1745,X0)
| i46 = X0 ) ).
cnf(u8592,hypothesis,
( select(a_1717,X0) = select(a_1718,X0)
| i19 = X0 ) ).
cnf(u8584,hypothesis,
( select(a_1709,X0) = select(a_1710,X0)
| i11 = X0 ) ).
cnf(u8598,hypothesis,
( select(a_1723,X0) = select(a_1724,X0)
| i25 = X0 ) ).
cnf(a1,axiom,
select(store(X0,X1,X2),X1) = X2 ).
cnf(u8601,hypothesis,
( select(a_1726,X0) = select(a_1727,X0)
| i28 = X0 ) ).
cnf(u8651,hypothesis,
( select(a_1777,X0) = select(a_1778,X0)
| i36 = X0 ) ).
cnf(u8646,hypothesis,
( select(a_1772,X0) = select(a_1773,X0)
| i47 = X0 ) ).
cnf(u8576,hypothesis,
( select(a_1701,X0) = select(a_1702,X0)
| i3 = X0 ) ).
cnf(u8620,hypothesis,
( select(a_1745,X0) = select(a_1746,X0)
| i47 = X0 ) ).
cnf(u8664,hypothesis,
( select(a_1790,X0) = select(a_1791,X0)
| i37 = X0 ) ).
cnf(u8605,hypothesis,
( select(a_1730,X0) = select(a_1731,X0)
| i32 = X0 ) ).
cnf(u8597,hypothesis,
( select(a_1722,X0) = select(a_1723,X0)
| i24 = X0 ) ).
cnf(u8615,hypothesis,
( select(a_1740,X0) = select(a_1741,X0)
| i42 = X0 ) ).
cnf(u8642,hypothesis,
( select(a_1768,X0) = select(a_1769,X0)
| i33 = X0 ) ).
cnf(u8593,hypothesis,
( select(a_1718,X0) = select(a_1719,X0)
| i20 = X0 ) ).
cnf(u8654,hypothesis,
( select(a_1780,X0) = select(a_1781,X0)
| i23 = X0 ) ).
cnf(u8650,hypothesis,
( select(a_1776,X0) = select(a_1777,X0)
| i11 = X0 ) ).
cnf(u8663,hypothesis,
( select(a_1789,X0) = select(a_1790,X0)
| i3 = X0 ) ).
cnf(u8638,hypothesis,
( select(a_1764,X0) = select(a_1765,X0)
| i6 = X0 ) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : SWV498-1.050 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.03 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.00/0.10 % Computer : n012.cluster.edu
% 0.00/0.10 % Model : x86_64 x86_64
% 0.00/0.10 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.00/0.10 % Memory : 8046.5625MB
% 0.00/0.10 % OS : Linux 6.8.0-71-generic
% 0.00/0.10 % CPULimit : 300
% 0.00/0.10 % WCLimit : 300
% 0.00/0.10 % DateTime : Mon Sep 28 11:16:49 UTC 2026
% 0.00/0.11 % CPUTime :
% 0.00/0.11 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.08/0.12 Running first-order theorem proving
% 0.08/0.12 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 5.97/1.23 % (3319572)Input is clausal, will run a generic CNF schedule.
% 5.97/1.23 % (3319611)lrs+10_1_sil=8000:sp=occurrence:random_seed=4087202041:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 5.97/1.23 % (3319609)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=2131126206:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 5.97/1.23 % (3319614)dis-21_1_sil=8000:lcm=predicate:random_seed=256596091:st=5:avsq=on:i=117:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/117Mi)
% 5.97/1.23 % (3319612)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=2401952119:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 5.97/1.23 % (3319608)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=goal:fd=preordered:foolp=on:random_seed=861694806:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 5.97/1.23 % (3319613)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=822318823:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 5.97/1.23 % (3319610)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=1648581646:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 5.97/1.23 % (3319611)Refutation not found, incomplete strategy
% 5.97/1.23 % (3319611)------------------------------
% 5.97/1.23 % (3319611)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.97/1.23 % (3319611)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.97/1.23 % (3319611)CaDiCaL version: 2.1.3
% 5.97/1.23 % (3319611)Termination reason: Refutation not found, incomplete strategy
% 5.97/1.23 % (3319611)Time elapsed: 0.010 s
% 5.97/1.23 % (3319611)Peak memory usage: 88 MB
% 5.97/1.23 % (3319611)Instructions burned: 42 (million)
% 5.97/1.23 % (3319614)Refutation not found, incomplete strategy
% 5.97/1.23 % (3319614)------------------------------
% 5.97/1.23 % (3319614)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.97/1.23 % (3319614)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.97/1.23 % (3319614)CaDiCaL version: 2.1.3
% 5.97/1.23 % (3319614)Termination reason: Refutation not found, incomplete strategy
% 5.97/1.23 % (3319614)Time elapsed: 0.017 s
% 5.97/1.23 % (3319614)Peak memory usage: 89 MB
% 5.97/1.23 % (3319614)Instructions burned: 65 (million)
% 5.97/1.23 % (3319613)Refutation not found, incomplete strategy
% 5.97/1.23 % (3319613)------------------------------
% 5.97/1.23 % (3319613)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.97/1.23 % (3319613)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.97/1.23 % (3319613)CaDiCaL version: 2.1.3
% 5.97/1.23 % (3319613)Termination reason: Refutation not found, incomplete strategy
% 5.97/1.23 % (3319613)Time elapsed: 0.022 s
% 5.97/1.23 % (3319613)Peak memory usage: 89 MB
% 5.97/1.23 % (3319613)Instructions burned: 84 (million)
% 5.97/1.23 % (3319612)Refutation not found, incomplete strategy
% 5.97/1.23 % (3319612)------------------------------
% 5.97/1.23 % (3319612)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.97/1.23 % (3319612)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.97/1.23 % (3319612)CaDiCaL version: 2.1.3
% 5.97/1.23 % (3319612)Termination reason: Refutation not found, incomplete strategy
% 5.97/1.23 % (3319612)Time elapsed: 0.024 s
% 5.97/1.23 % (3319612)Peak memory usage: 89 MB
% 5.97/1.23 % (3319612)Instructions burned: 93 (million)
% 5.97/1.23 % (3319611)------------------------------
% 5.97/1.23 % (3319611)------------------------------
% 5.97/1.23 % (3319614)------------------------------
% 5.97/1.23 % (3319614)------------------------------
% 5.97/1.23 % (3319613)------------------------------
% 5.97/1.23 % (3319613)------------------------------
% 5.97/1.23 % (3319612)------------------------------
% 5.97/1.23 % (3319612)------------------------------
% 5.97/1.23 % (3319622)dis+1010_3_sil=8000:plsq=on:drc=off:fde=none:plsqc=1:bsd=on:plsqr=7,2:sos=on:spb=goal_then_units:random_seed=3473565417:i=143:sd=2:aac=none:ss=axioms:sgt=16_2997 on theBenchmark for (2997ds/143Mi)
% 5.97/1.23 % (3319623)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=15970036:st=3:avsq=on:s2a=on:i=189:s2at=1.2:avsqr=1,16:sd=2:bd=all:nm=64:ss=axioms:sgt=30_2996 on theBenchmark for (2996ds/189Mi)
% 5.97/1.23 % (3319622)Refutation not found, incomplete strategy
% 5.97/1.23 % (3319622)------------------------------
% 5.97/1.23 % (3319622)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.97/1.23 % (3319622)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.97/1.23 % (3319622)CaDiCaL version: 2.1.3
% 5.97/1.23 % (3319622)Termination reason: Refutation not found, incomplete strategy
% 5.97/1.23 % (3319622)Time elapsed: 0.014 s
% 5.97/1.23 % (3319622)Peak memory usage: 89 MB
% 5.97/1.23 % (3319622)Instructions burned: 51 (million)
% 5.97/1.23 % (3319625)lrs+10_64_to=lpo:sil=8000:random_seed=1536999417:i=126:bd=preordered_2996 on theBenchmark for (2996ds/126Mi)
% 5.97/1.23 % (3319624)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=4196922234:st=4:i=219:sd=3:ss=axioms_2996 on theBenchmark for (2996ds/219Mi)
% 5.97/1.23 % (3319623)Refutation not found, incomplete strategy
% 5.97/1.23 % (3319623)------------------------------
% 5.97/1.23 % (3319623)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.97/1.23 % (3319623)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.97/1.23 % (3319623)CaDiCaL version: 2.1.3
% 5.97/1.23 % (3319623)Termination reason: Refutation not found, incomplete strategy
% 5.97/1.23 % (3319623)Time elapsed: 0.028 s
% 5.97/1.23 % (3319623)Peak memory usage: 89 MB
% 5.97/1.23 % (3319623)Instructions burned: 105 (million)
% 5.97/1.23 % (3319624)Refutation not found, incomplete strategy
% 5.97/1.23 % (3319624)------------------------------
% 5.97/1.23 % (3319624)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.97/1.23 % (3319624)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.97/1.23 % (3319624)CaDiCaL version: 2.1.3
% 5.97/1.23 % (3319624)Termination reason: Refutation not found, incomplete strategy
% 5.97/1.23 % (3319624)Time elapsed: 0.012 s
% 5.97/1.23 % (3319624)Peak memory usage: 88 MB
% 5.97/1.23 % (3319624)Instructions burned: 49 (million)
% 5.97/1.23 % (3319625)Instruction limit reached!
% 5.97/1.23 % (3319625)------------------------------
% 5.97/1.23 % (3319625)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.97/1.23 % (3319625)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.97/1.23 % (3319625)CaDiCaL version: 2.1.3
% 5.97/1.23 % (3319625)Termination reason: Instruction limit
% 5.97/1.23 % (3319625)Termination phase: Saturation
% 5.97/1.23 % (3319625)Time elapsed: 0.033 s
% 5.97/1.23 % (3319625)Peak memory usage: 88 MB
% 5.97/1.23 % (3319625)Instructions burned: 130 (million)
% 5.97/1.23 % (3319622)------------------------------
% 5.97/1.23 % (3319622)------------------------------
% 5.97/1.23 % (3319623)------------------------------
% 5.97/1.23 % (3319623)------------------------------
% 5.97/1.23 % (3319608)Refutation not found, incomplete strategy
% 5.97/1.23 % (3319608)------------------------------
% 5.97/1.23 % (3319608)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.97/1.23 % (3319608)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.97/1.23 % (3319608)CaDiCaL version: 2.1.3
% 5.97/1.23 % (3319608)Termination reason: Refutation not found, incomplete strategy
% 5.97/1.23 % (3319608)Time elapsed: 0.471 s
% 5.97/1.23 % (3319608)Peak memory usage: 137 MB
% 5.97/1.23 % (3319608)Instructions burned: 1306 (million)
% 5.97/1.23 % (3319630)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=2710294989:avsq=on:i=194:fgj=on:bd=preordered_2995 on theBenchmark for (2995ds/194Mi)
% 5.97/1.23 % (3319610)Refutation not found, incomplete strategy
% 5.97/1.23 % (3319610)------------------------------
% 5.97/1.23 % (3319610)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.97/1.23 % (3319610)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.97/1.23 % (3319610)CaDiCaL version: 2.1.3
% 5.97/1.23 % (3319610)Termination reason: Refutation not found, incomplete strategy
% 5.97/1.23 % (3319610)Time elapsed: 0.475 s
% 5.97/1.23 % (3319610)Peak memory usage: 136 MB
% 5.97/1.23 % (3319610)Instructions burned: 1322 (million)
% 5.97/1.23 % (3319624)------------------------------
% 5.97/1.23 % (3319624)------------------------------
% 5.97/1.23 % (3319630)Refutation not found, incomplete strategy
% 5.97/1.23 % (3319630)------------------------------
% 5.97/1.23 % (3319630)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.97/1.23 % (3319630)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.97/1.23 % (3319630)CaDiCaL version: 2.1.3
% 5.97/1.23 % (3319630)Termination reason: Refutation not found, incomplete strategy
% 5.97/1.23 % (3319630)Time elapsed: 0.020 s
% 5.97/1.23 % (3319630)Peak memory usage: 89 MB
% 5.97/1.23 % (3319630)Instructions burned: 75 (million)
% 5.97/1.23 % (3319631)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=4251383037:i=157:gtg=all_2994 on theBenchmark for (2994ds/157Mi)
% 5.97/1.23 % (3319631)First to succeed.
% 5.97/1.23 % (3319632)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=2488534718:i=3394:sd=4:ss=included:sgt=64_2994 on theBenchmark for (2994ds/3394Mi)
% 5.97/1.23 % (3319631)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-3319572"
% 5.97/1.23 % (3319634)lrs+1011_5_to=lpo:sil=8000:tgt=full:plsq=on:prc=on:drc=off:plsqr=31,4:sp=occurrence:urr=on:nwc=0.8:s2agt=16:br=off:random_seed=1937028375:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2993 on theBenchmark for (2993ds/106Mi)
% 5.97/1.23 % (3319634)Refutation not found, incomplete strategy
% 5.97/1.23 % (3319634)------------------------------
% 5.97/1.23 % (3319634)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.97/1.23 % (3319634)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.97/1.23 % (3319634)CaDiCaL version: 2.1.3
% 5.97/1.23 % (3319634)Termination reason: Refutation not found, incomplete strategy
% 5.97/1.23 % (3319634)Time elapsed: 0.018 s
% 5.97/1.23 % (3319634)Peak memory usage: 89 MB
% 5.97/1.23 % (3319634)Instructions burned: 67 (million)
% 5.97/1.23 % (3319608)------------------------------
% 5.97/1.23 % (3319608)------------------------------
% 5.97/1.23 % (3319610)------------------------------
% 5.97/1.23 % (3319610)------------------------------
% 5.97/1.23 % (3319630)------------------------------
% 5.97/1.23 % (3319630)------------------------------
% 5.97/1.23 % (3319638)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=3038180257:i=107_2992 on theBenchmark for (2992ds/107Mi)
% 5.97/1.23 % SZS status Satisfiable for theBenchmark
% 5.97/1.23 % SZS output start Saturation.
% See solution above
% 6.53/1.33 % SZS output start Definitions and Model Updates.
% 6.53/1.33 % SZS output end Definitions and Model Updates.
% 6.53/1.33 % (3319631)------------------------------
% 6.53/1.33 % (3319631)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.53/1.33 % (3319631)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.53/1.33 % (3319631)CaDiCaL version: 2.1.3
% 6.53/1.33 % (3319631)Termination reason: Satisfiable
% 6.53/1.33 % (3319631)Time elapsed: 0.037 s
% 6.53/1.33 % (3319631)Peak memory usage: 93 MB
% 6.53/1.33 % (3319631)Instructions burned: 119 (million)
% 6.53/1.33 % (3319631)------------------------------
% 6.53/1.33 % (3319631)------------------------------
% 6.53/1.33 % (3319572)Success in time 0.898 s
% 6.53/1.33 % Vampire exiting
%------------------------------------------------------------------------------