%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SWV497-1.050 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n002.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:04 PM UTC 2026
% Result : Satisfiable 6.72s 1.52s
% Output : Saturation 8.09s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(u1332,negated_conjecture,
a_1749 != a_1799 ).
cnf(u1337,hypothesis,
i1 != i2 ).
cnf(u1342,hypothesis,
i1 != i3 ).
cnf(u1347,hypothesis,
i1 != i4 ).
cnf(u1352,hypothesis,
i1 != i5 ).
cnf(u1357,hypothesis,
i1 != i6 ).
cnf(u1362,hypothesis,
i1 != i7 ).
cnf(u1367,hypothesis,
i1 != i8 ).
cnf(u1372,hypothesis,
i1 != i9 ).
cnf(u1377,hypothesis,
i1 != i10 ).
cnf(u1382,hypothesis,
i1 != i11 ).
cnf(u1387,hypothesis,
i1 != i12 ).
cnf(u1392,hypothesis,
i1 != i13 ).
cnf(u1397,hypothesis,
i1 != i14 ).
cnf(u1402,hypothesis,
i1 != i15 ).
cnf(u1407,hypothesis,
i1 != i16 ).
cnf(u1412,hypothesis,
i1 != i17 ).
cnf(u1417,hypothesis,
i1 != i18 ).
cnf(u1422,hypothesis,
i1 != i19 ).
cnf(u1427,hypothesis,
i1 != i20 ).
cnf(u1432,hypothesis,
i1 != i21 ).
cnf(u1437,hypothesis,
i1 != i22 ).
cnf(u1442,hypothesis,
i1 != i23 ).
cnf(u1447,hypothesis,
i1 != i24 ).
cnf(u1452,hypothesis,
i1 != i25 ).
cnf(u1457,hypothesis,
i1 != i26 ).
cnf(u1462,hypothesis,
i1 != i27 ).
cnf(u1467,hypothesis,
i1 != i28 ).
cnf(u1472,hypothesis,
i1 != i29 ).
cnf(u1477,hypothesis,
i1 != i30 ).
cnf(u1482,hypothesis,
i1 != i31 ).
cnf(u1487,hypothesis,
i1 != i32 ).
cnf(u1492,hypothesis,
i1 != i33 ).
cnf(u1497,hypothesis,
i1 != i34 ).
cnf(u1502,hypothesis,
i1 != i35 ).
cnf(u1507,hypothesis,
i1 != i36 ).
cnf(u1512,hypothesis,
i1 != i37 ).
cnf(u1517,hypothesis,
i1 != i38 ).
cnf(u1522,hypothesis,
i1 != i39 ).
cnf(u1527,hypothesis,
i1 != i40 ).
cnf(u1532,hypothesis,
i1 != i41 ).
cnf(u1537,hypothesis,
i1 != i42 ).
cnf(u1542,hypothesis,
i1 != i43 ).
cnf(u1547,hypothesis,
i1 != i44 ).
cnf(u1552,hypothesis,
i1 != i45 ).
cnf(u1557,hypothesis,
i1 != i46 ).
cnf(u1562,hypothesis,
i1 != i47 ).
cnf(u1567,hypothesis,
i1 != i48 ).
cnf(u1572,hypothesis,
i1 != i49 ).
cnf(u1577,hypothesis,
i1 != i50 ).
cnf(u1582,hypothesis,
i2 != i3 ).
cnf(u1587,hypothesis,
i2 != i4 ).
cnf(u1592,hypothesis,
i2 != i5 ).
cnf(u1597,hypothesis,
i2 != i6 ).
cnf(u1602,hypothesis,
i2 != i7 ).
cnf(u1607,hypothesis,
i2 != i8 ).
cnf(u1612,hypothesis,
i2 != i9 ).
cnf(u1617,hypothesis,
i2 != i10 ).
cnf(u1622,hypothesis,
i2 != i11 ).
cnf(u1627,hypothesis,
i2 != i12 ).
cnf(u1632,hypothesis,
i2 != i13 ).
cnf(u1637,hypothesis,
i2 != i14 ).
cnf(u1642,hypothesis,
i2 != i15 ).
cnf(u1647,hypothesis,
i2 != i16 ).
cnf(u1652,hypothesis,
i2 != i17 ).
cnf(u1657,hypothesis,
i2 != i18 ).
cnf(u1662,hypothesis,
i2 != i19 ).
cnf(u1667,hypothesis,
i2 != i20 ).
cnf(u1672,hypothesis,
i2 != i21 ).
cnf(u1677,hypothesis,
i2 != i22 ).
cnf(u1682,hypothesis,
i2 != i23 ).
cnf(u1687,hypothesis,
i2 != i24 ).
cnf(u1692,hypothesis,
i2 != i25 ).
cnf(u1697,hypothesis,
i2 != i26 ).
cnf(u1702,hypothesis,
i2 != i27 ).
cnf(u1707,hypothesis,
i2 != i28 ).
cnf(u1712,hypothesis,
i2 != i29 ).
cnf(u1717,hypothesis,
i2 != i30 ).
cnf(u1722,hypothesis,
i2 != i31 ).
cnf(u1727,hypothesis,
i2 != i32 ).
cnf(u1732,hypothesis,
i2 != i33 ).
cnf(u1737,hypothesis,
i2 != i34 ).
cnf(u1742,hypothesis,
i2 != i35 ).
cnf(u1747,hypothesis,
i2 != i36 ).
cnf(u1752,hypothesis,
i2 != i37 ).
cnf(u1757,hypothesis,
i2 != i38 ).
cnf(u1762,hypothesis,
i2 != i39 ).
cnf(u1767,hypothesis,
i2 != i40 ).
cnf(u1772,hypothesis,
i2 != i41 ).
cnf(u1777,hypothesis,
i2 != i42 ).
cnf(u1782,hypothesis,
i2 != i43 ).
cnf(u1787,hypothesis,
i2 != i44 ).
cnf(u1792,hypothesis,
i2 != i45 ).
cnf(u1797,hypothesis,
i2 != i46 ).
cnf(u1802,hypothesis,
i2 != i47 ).
cnf(u1807,hypothesis,
i2 != i48 ).
cnf(u1812,hypothesis,
i2 != i49 ).
cnf(u1817,hypothesis,
i2 != i50 ).
cnf(u1822,hypothesis,
i3 != i4 ).
cnf(u1827,hypothesis,
i3 != i5 ).
cnf(u1832,hypothesis,
i3 != i6 ).
cnf(u1837,hypothesis,
i3 != i7 ).
cnf(u1842,hypothesis,
i3 != i8 ).
cnf(u1847,hypothesis,
i3 != i9 ).
cnf(u1852,hypothesis,
i3 != i10 ).
cnf(u1857,hypothesis,
i3 != i11 ).
cnf(u1862,hypothesis,
i3 != i12 ).
cnf(u1867,hypothesis,
i3 != i13 ).
cnf(u1872,hypothesis,
i3 != i14 ).
cnf(u1877,hypothesis,
i3 != i15 ).
cnf(u1882,hypothesis,
i3 != i16 ).
cnf(u1887,hypothesis,
i3 != i17 ).
cnf(u1892,hypothesis,
i3 != i18 ).
cnf(u1897,hypothesis,
i3 != i19 ).
cnf(u1902,hypothesis,
i3 != i20 ).
cnf(u1907,hypothesis,
i3 != i21 ).
cnf(u1912,hypothesis,
i3 != i22 ).
cnf(u1917,hypothesis,
i3 != i23 ).
cnf(u1922,hypothesis,
i3 != i24 ).
cnf(u1927,hypothesis,
i3 != i25 ).
cnf(u1932,hypothesis,
i3 != i26 ).
cnf(u1937,hypothesis,
i3 != i27 ).
cnf(u1942,hypothesis,
i3 != i28 ).
cnf(u1947,hypothesis,
i3 != i29 ).
cnf(u1952,hypothesis,
i3 != i30 ).
cnf(u1957,hypothesis,
i3 != i31 ).
cnf(u1962,hypothesis,
i3 != i32 ).
cnf(u1967,hypothesis,
i3 != i33 ).
cnf(u1972,hypothesis,
i3 != i34 ).
cnf(u1977,hypothesis,
i3 != i35 ).
cnf(u1982,hypothesis,
i3 != i36 ).
cnf(u1987,hypothesis,
i3 != i37 ).
cnf(u1992,hypothesis,
i3 != i38 ).
cnf(u1997,hypothesis,
i3 != i39 ).
cnf(u2002,hypothesis,
i3 != i40 ).
cnf(u2007,hypothesis,
i3 != i41 ).
cnf(u2012,hypothesis,
i3 != i42 ).
cnf(u2017,hypothesis,
i3 != i43 ).
cnf(u2022,hypothesis,
i3 != i44 ).
cnf(u2027,hypothesis,
i3 != i45 ).
cnf(u2032,hypothesis,
i3 != i46 ).
cnf(u2037,hypothesis,
i3 != i47 ).
cnf(u2042,hypothesis,
i3 != i48 ).
cnf(u2047,hypothesis,
i3 != i49 ).
cnf(u2052,hypothesis,
i3 != i50 ).
cnf(u2057,hypothesis,
i4 != i5 ).
cnf(u2062,hypothesis,
i4 != i6 ).
cnf(u2067,hypothesis,
i4 != i7 ).
cnf(u2072,hypothesis,
i4 != i8 ).
cnf(u2077,hypothesis,
i4 != i9 ).
cnf(u2082,hypothesis,
i4 != i10 ).
cnf(u2087,hypothesis,
i4 != i11 ).
cnf(u2092,hypothesis,
i4 != i12 ).
cnf(u2097,hypothesis,
i4 != i13 ).
cnf(u2102,hypothesis,
i4 != i14 ).
cnf(u2107,hypothesis,
i4 != i15 ).
cnf(u2112,hypothesis,
i4 != i16 ).
cnf(u2117,hypothesis,
i4 != i17 ).
cnf(u2122,hypothesis,
i4 != i18 ).
cnf(u2127,hypothesis,
i4 != i19 ).
cnf(u2132,hypothesis,
i4 != i20 ).
cnf(u2137,hypothesis,
i4 != i21 ).
cnf(u2142,hypothesis,
i4 != i22 ).
cnf(u2147,hypothesis,
i4 != i23 ).
cnf(u2152,hypothesis,
i4 != i24 ).
cnf(u2157,hypothesis,
i4 != i25 ).
cnf(u2162,hypothesis,
i4 != i26 ).
cnf(u2167,hypothesis,
i4 != i27 ).
cnf(u2172,hypothesis,
i4 != i28 ).
cnf(u2177,hypothesis,
i4 != i29 ).
cnf(u2182,hypothesis,
i4 != i30 ).
cnf(u2187,hypothesis,
i4 != i31 ).
cnf(u2192,hypothesis,
i4 != i32 ).
cnf(u2197,hypothesis,
i4 != i33 ).
cnf(u2202,hypothesis,
i4 != i34 ).
cnf(u2207,hypothesis,
i4 != i35 ).
cnf(u2212,hypothesis,
i4 != i36 ).
cnf(u2217,hypothesis,
i4 != i37 ).
cnf(u2222,hypothesis,
i4 != i38 ).
cnf(u2227,hypothesis,
i4 != i39 ).
cnf(u2232,hypothesis,
i4 != i40 ).
cnf(u2237,hypothesis,
i4 != i41 ).
cnf(u2242,hypothesis,
i4 != i42 ).
cnf(u2247,hypothesis,
i4 != i43 ).
cnf(u2252,hypothesis,
i4 != i44 ).
cnf(u2257,hypothesis,
i4 != i45 ).
cnf(u2262,hypothesis,
i4 != i46 ).
cnf(u2267,hypothesis,
i4 != i47 ).
cnf(u2272,hypothesis,
i4 != i48 ).
cnf(u2277,hypothesis,
i4 != i49 ).
cnf(u2282,hypothesis,
i4 != i50 ).
cnf(u2287,hypothesis,
i5 != i6 ).
cnf(u2292,hypothesis,
i5 != i7 ).
cnf(u2297,hypothesis,
i5 != i8 ).
cnf(u2302,hypothesis,
i5 != i9 ).
cnf(u2307,hypothesis,
i5 != i10 ).
cnf(u2312,hypothesis,
i5 != i11 ).
cnf(u2317,hypothesis,
i5 != i12 ).
cnf(u2322,hypothesis,
i5 != i13 ).
cnf(u2327,hypothesis,
i5 != i14 ).
cnf(u2332,hypothesis,
i5 != i15 ).
cnf(u2337,hypothesis,
i5 != i16 ).
cnf(u2342,hypothesis,
i5 != i17 ).
cnf(u2347,hypothesis,
i5 != i18 ).
cnf(u2352,hypothesis,
i5 != i19 ).
cnf(u2357,hypothesis,
i5 != i20 ).
cnf(u2362,hypothesis,
i5 != i21 ).
cnf(u2367,hypothesis,
i5 != i22 ).
cnf(u2372,hypothesis,
i5 != i23 ).
cnf(u2377,hypothesis,
i5 != i24 ).
cnf(u2382,hypothesis,
i5 != i25 ).
cnf(u2387,hypothesis,
i5 != i26 ).
cnf(u2392,hypothesis,
i5 != i27 ).
cnf(u2397,hypothesis,
i5 != i28 ).
cnf(u2402,hypothesis,
i5 != i29 ).
cnf(u2407,hypothesis,
i5 != i30 ).
cnf(u2412,hypothesis,
i5 != i31 ).
cnf(u2417,hypothesis,
i5 != i32 ).
cnf(u2422,hypothesis,
i5 != i33 ).
cnf(u2427,hypothesis,
i5 != i34 ).
cnf(u2432,hypothesis,
i5 != i35 ).
cnf(u2437,hypothesis,
i5 != i36 ).
cnf(u2442,hypothesis,
i5 != i37 ).
cnf(u2447,hypothesis,
i5 != i38 ).
cnf(u2452,hypothesis,
i5 != i39 ).
cnf(u2457,hypothesis,
i5 != i40 ).
cnf(u2462,hypothesis,
i5 != i41 ).
cnf(u2467,hypothesis,
i5 != i42 ).
cnf(u2472,hypothesis,
i5 != i43 ).
cnf(u2477,hypothesis,
i5 != i44 ).
cnf(u2482,hypothesis,
i5 != i45 ).
cnf(u2487,hypothesis,
i5 != i46 ).
cnf(u2492,hypothesis,
i5 != i47 ).
cnf(u2497,hypothesis,
i5 != i48 ).
cnf(u2502,hypothesis,
i5 != i49 ).
cnf(u2507,hypothesis,
i5 != i50 ).
cnf(u2512,hypothesis,
i6 != i7 ).
cnf(u2517,hypothesis,
i6 != i8 ).
cnf(u2522,hypothesis,
i6 != i9 ).
cnf(u2527,hypothesis,
i6 != i10 ).
cnf(u2532,hypothesis,
i6 != i11 ).
cnf(u2537,hypothesis,
i6 != i12 ).
cnf(u2542,hypothesis,
i6 != i13 ).
cnf(u2547,hypothesis,
i6 != i14 ).
cnf(u2552,hypothesis,
i6 != i15 ).
cnf(u2557,hypothesis,
i6 != i16 ).
cnf(u2562,hypothesis,
i6 != i17 ).
cnf(u2567,hypothesis,
i6 != i18 ).
cnf(u2572,hypothesis,
i6 != i19 ).
cnf(u2577,hypothesis,
i6 != i20 ).
cnf(u2582,hypothesis,
i6 != i21 ).
cnf(u2587,hypothesis,
i6 != i22 ).
cnf(u2592,hypothesis,
i6 != i23 ).
cnf(u2597,hypothesis,
i6 != i24 ).
cnf(u2602,hypothesis,
i6 != i25 ).
cnf(u2607,hypothesis,
i6 != i26 ).
cnf(u2612,hypothesis,
i6 != i27 ).
cnf(u2617,hypothesis,
i6 != i28 ).
cnf(u2622,hypothesis,
i6 != i29 ).
cnf(u2627,hypothesis,
i6 != i30 ).
cnf(u2632,hypothesis,
i6 != i31 ).
cnf(u2637,hypothesis,
i6 != i32 ).
cnf(u2642,hypothesis,
i6 != i33 ).
cnf(u2647,hypothesis,
i6 != i34 ).
cnf(u2652,hypothesis,
i6 != i35 ).
cnf(u2657,hypothesis,
i6 != i36 ).
cnf(u2662,hypothesis,
i6 != i37 ).
cnf(u2667,hypothesis,
i6 != i38 ).
cnf(u2672,hypothesis,
i6 != i39 ).
cnf(u2677,hypothesis,
i6 != i40 ).
cnf(u2682,hypothesis,
i6 != i41 ).
cnf(u2687,hypothesis,
i6 != i42 ).
cnf(u2692,hypothesis,
i6 != i43 ).
cnf(u2697,hypothesis,
i6 != i44 ).
cnf(u2702,hypothesis,
i6 != i45 ).
cnf(u2707,hypothesis,
i6 != i46 ).
cnf(u2712,hypothesis,
i6 != i47 ).
cnf(u2717,hypothesis,
i6 != i48 ).
cnf(u2722,hypothesis,
i6 != i49 ).
cnf(u2727,hypothesis,
i6 != i50 ).
cnf(u2732,hypothesis,
i7 != i8 ).
cnf(u2737,hypothesis,
i7 != i9 ).
cnf(u2742,hypothesis,
i7 != i10 ).
cnf(u2747,hypothesis,
i7 != i11 ).
cnf(u2752,hypothesis,
i7 != i12 ).
cnf(u2757,hypothesis,
i7 != i13 ).
cnf(u2762,hypothesis,
i7 != i14 ).
cnf(u2767,hypothesis,
i7 != i15 ).
cnf(u2772,hypothesis,
i7 != i16 ).
cnf(u2777,hypothesis,
i7 != i17 ).
cnf(u2782,hypothesis,
i7 != i18 ).
cnf(u2787,hypothesis,
i7 != i19 ).
cnf(u2792,hypothesis,
i7 != i20 ).
cnf(u2797,hypothesis,
i7 != i21 ).
cnf(u2802,hypothesis,
i7 != i22 ).
cnf(u2807,hypothesis,
i7 != i23 ).
cnf(u2812,hypothesis,
i7 != i24 ).
cnf(u2817,hypothesis,
i7 != i25 ).
cnf(u2822,hypothesis,
i7 != i26 ).
cnf(u2827,hypothesis,
i7 != i27 ).
cnf(u2832,hypothesis,
i7 != i28 ).
cnf(u2837,hypothesis,
i7 != i29 ).
cnf(u2842,hypothesis,
i7 != i30 ).
cnf(u2847,hypothesis,
i7 != i31 ).
cnf(u2852,hypothesis,
i7 != i32 ).
cnf(u2857,hypothesis,
i7 != i33 ).
cnf(u2862,hypothesis,
i7 != i34 ).
cnf(u2867,hypothesis,
i7 != i35 ).
cnf(u2872,hypothesis,
i7 != i36 ).
cnf(u2877,hypothesis,
i7 != i37 ).
cnf(u2882,hypothesis,
i7 != i38 ).
cnf(u2887,hypothesis,
i7 != i39 ).
cnf(u2892,hypothesis,
i7 != i40 ).
cnf(u2897,hypothesis,
i7 != i41 ).
cnf(u2902,hypothesis,
i7 != i42 ).
cnf(u2907,hypothesis,
i7 != i43 ).
cnf(u2912,hypothesis,
i7 != i44 ).
cnf(u2917,hypothesis,
i7 != i45 ).
cnf(u2922,hypothesis,
i7 != i46 ).
cnf(u2927,hypothesis,
i7 != i47 ).
cnf(u2932,hypothesis,
i7 != i48 ).
cnf(u2937,hypothesis,
i7 != i49 ).
cnf(u2942,hypothesis,
i7 != i50 ).
cnf(u2947,hypothesis,
i8 != i9 ).
cnf(u2952,hypothesis,
i8 != i10 ).
cnf(u2957,hypothesis,
i8 != i11 ).
cnf(u2962,hypothesis,
i8 != i12 ).
cnf(u2967,hypothesis,
i8 != i13 ).
cnf(u2972,hypothesis,
i8 != i14 ).
cnf(u2977,hypothesis,
i8 != i15 ).
cnf(u2982,hypothesis,
i8 != i16 ).
cnf(u2987,hypothesis,
i8 != i17 ).
cnf(u2992,hypothesis,
i8 != i18 ).
cnf(u2997,hypothesis,
i8 != i19 ).
cnf(u3002,hypothesis,
i8 != i20 ).
cnf(u3007,hypothesis,
i8 != i21 ).
cnf(u3012,hypothesis,
i8 != i22 ).
cnf(u3017,hypothesis,
i8 != i23 ).
cnf(u3022,hypothesis,
i8 != i24 ).
cnf(u3027,hypothesis,
i8 != i25 ).
cnf(u3032,hypothesis,
i8 != i26 ).
cnf(u3037,hypothesis,
i8 != i27 ).
cnf(u3042,hypothesis,
i8 != i28 ).
cnf(u3047,hypothesis,
i8 != i29 ).
cnf(u3052,hypothesis,
i8 != i30 ).
cnf(u3057,hypothesis,
i8 != i31 ).
cnf(u3062,hypothesis,
i8 != i32 ).
cnf(u3067,hypothesis,
i8 != i33 ).
cnf(u3072,hypothesis,
i8 != i34 ).
cnf(u3077,hypothesis,
i8 != i35 ).
cnf(u3082,hypothesis,
i8 != i36 ).
cnf(u3087,hypothesis,
i8 != i37 ).
cnf(u3092,hypothesis,
i8 != i38 ).
cnf(u3097,hypothesis,
i8 != i39 ).
cnf(u3102,hypothesis,
i8 != i40 ).
cnf(u3107,hypothesis,
i8 != i41 ).
cnf(u3112,hypothesis,
i8 != i42 ).
cnf(u3117,hypothesis,
i8 != i43 ).
cnf(u3122,hypothesis,
i8 != i44 ).
cnf(u3127,hypothesis,
i8 != i45 ).
cnf(u3132,hypothesis,
i8 != i46 ).
cnf(u3137,hypothesis,
i8 != i47 ).
cnf(u3142,hypothesis,
i8 != i48 ).
cnf(u3147,hypothesis,
i8 != i49 ).
cnf(u3152,hypothesis,
i8 != i50 ).
cnf(u3157,hypothesis,
i9 != i10 ).
cnf(u3162,hypothesis,
i9 != i11 ).
cnf(u3167,hypothesis,
i9 != i12 ).
cnf(u3172,hypothesis,
i9 != i13 ).
cnf(u3177,hypothesis,
i9 != i14 ).
cnf(u3182,hypothesis,
i9 != i15 ).
cnf(u3187,hypothesis,
i9 != i16 ).
cnf(u3192,hypothesis,
i9 != i17 ).
cnf(u3197,hypothesis,
i9 != i18 ).
cnf(u3202,hypothesis,
i9 != i19 ).
cnf(u3207,hypothesis,
i9 != i20 ).
cnf(u3212,hypothesis,
i9 != i21 ).
cnf(u3217,hypothesis,
i9 != i22 ).
cnf(u3222,hypothesis,
i9 != i23 ).
cnf(u3227,hypothesis,
i9 != i24 ).
cnf(u3232,hypothesis,
i9 != i25 ).
cnf(u3237,hypothesis,
i9 != i26 ).
cnf(u3242,hypothesis,
i9 != i27 ).
cnf(u3247,hypothesis,
i9 != i28 ).
cnf(u3252,hypothesis,
i9 != i29 ).
cnf(u3257,hypothesis,
i9 != i30 ).
cnf(u3262,hypothesis,
i9 != i31 ).
cnf(u3267,hypothesis,
i9 != i32 ).
cnf(u3272,hypothesis,
i9 != i33 ).
cnf(u3277,hypothesis,
i9 != i34 ).
cnf(u3282,hypothesis,
i9 != i35 ).
cnf(u3287,hypothesis,
i9 != i36 ).
cnf(u3292,hypothesis,
i9 != i37 ).
cnf(u3297,hypothesis,
i9 != i38 ).
cnf(u3302,hypothesis,
i9 != i39 ).
cnf(u3307,hypothesis,
i9 != i40 ).
cnf(u3312,hypothesis,
i9 != i41 ).
cnf(u3317,hypothesis,
i9 != i42 ).
cnf(u3322,hypothesis,
i9 != i43 ).
cnf(u3327,hypothesis,
i9 != i44 ).
cnf(u3332,hypothesis,
i9 != i45 ).
cnf(u3337,hypothesis,
i9 != i46 ).
cnf(u3342,hypothesis,
i9 != i47 ).
cnf(u3347,hypothesis,
i9 != i48 ).
cnf(u3352,hypothesis,
i9 != i49 ).
cnf(u3357,hypothesis,
i9 != i50 ).
cnf(u3362,hypothesis,
i10 != i11 ).
cnf(u3367,hypothesis,
i10 != i12 ).
cnf(u3372,hypothesis,
i10 != i13 ).
cnf(u3377,hypothesis,
i10 != i14 ).
cnf(u3382,hypothesis,
i10 != i15 ).
cnf(u3387,hypothesis,
i10 != i16 ).
cnf(u3392,hypothesis,
i10 != i17 ).
cnf(u3397,hypothesis,
i10 != i18 ).
cnf(u3402,hypothesis,
i10 != i19 ).
cnf(u3407,hypothesis,
i10 != i20 ).
cnf(u3412,hypothesis,
i10 != i21 ).
cnf(u3417,hypothesis,
i10 != i22 ).
cnf(u3422,hypothesis,
i10 != i23 ).
cnf(u3427,hypothesis,
i10 != i24 ).
cnf(u3432,hypothesis,
i10 != i25 ).
cnf(u3437,hypothesis,
i10 != i26 ).
cnf(u3442,hypothesis,
i10 != i27 ).
cnf(u3447,hypothesis,
i10 != i28 ).
cnf(u3452,hypothesis,
i10 != i29 ).
cnf(u3457,hypothesis,
i10 != i30 ).
cnf(u3462,hypothesis,
i10 != i31 ).
cnf(u3467,hypothesis,
i10 != i32 ).
cnf(u3472,hypothesis,
i10 != i33 ).
cnf(u3477,hypothesis,
i10 != i34 ).
cnf(u3482,hypothesis,
i10 != i35 ).
cnf(u3487,hypothesis,
i10 != i36 ).
cnf(u3492,hypothesis,
i10 != i37 ).
cnf(u3497,hypothesis,
i10 != i38 ).
cnf(u3502,hypothesis,
i10 != i39 ).
cnf(u3507,hypothesis,
i10 != i40 ).
cnf(u3512,hypothesis,
i10 != i41 ).
cnf(u3517,hypothesis,
i10 != i42 ).
cnf(u3522,hypothesis,
i10 != i43 ).
cnf(u3527,hypothesis,
i10 != i44 ).
cnf(u3532,hypothesis,
i10 != i45 ).
cnf(u3537,hypothesis,
i10 != i46 ).
cnf(u3542,hypothesis,
i10 != i47 ).
cnf(u3547,hypothesis,
i10 != i48 ).
cnf(u3552,hypothesis,
i10 != i49 ).
cnf(u3557,hypothesis,
i10 != i50 ).
cnf(u3562,hypothesis,
i11 != i12 ).
cnf(u3567,hypothesis,
i11 != i13 ).
cnf(u3572,hypothesis,
i11 != i14 ).
cnf(u3577,hypothesis,
i11 != i15 ).
cnf(u3582,hypothesis,
i11 != i16 ).
cnf(u3587,hypothesis,
i11 != i17 ).
cnf(u3592,hypothesis,
i11 != i18 ).
cnf(u3597,hypothesis,
i11 != i19 ).
cnf(u3602,hypothesis,
i11 != i20 ).
cnf(u3607,hypothesis,
i11 != i21 ).
cnf(u3612,hypothesis,
i11 != i22 ).
cnf(u3617,hypothesis,
i11 != i23 ).
cnf(u3622,hypothesis,
i11 != i24 ).
cnf(u3627,hypothesis,
i11 != i25 ).
cnf(u3632,hypothesis,
i11 != i26 ).
cnf(u3637,hypothesis,
i11 != i27 ).
cnf(u3642,hypothesis,
i11 != i28 ).
cnf(u3647,hypothesis,
i11 != i29 ).
cnf(u3652,hypothesis,
i11 != i30 ).
cnf(u3657,hypothesis,
i11 != i31 ).
cnf(u3662,hypothesis,
i11 != i32 ).
cnf(u3667,hypothesis,
i11 != i33 ).
cnf(u3672,hypothesis,
i11 != i34 ).
cnf(u3677,hypothesis,
i11 != i35 ).
cnf(u3682,hypothesis,
i11 != i36 ).
cnf(u3687,hypothesis,
i11 != i37 ).
cnf(u3692,hypothesis,
i11 != i38 ).
cnf(u3697,hypothesis,
i11 != i39 ).
cnf(u3702,hypothesis,
i11 != i40 ).
cnf(u3707,hypothesis,
i11 != i41 ).
cnf(u3712,hypothesis,
i11 != i42 ).
cnf(u3717,hypothesis,
i11 != i43 ).
cnf(u3722,hypothesis,
i11 != i44 ).
cnf(u3727,hypothesis,
i11 != i45 ).
cnf(u3732,hypothesis,
i11 != i46 ).
cnf(u3737,hypothesis,
i11 != i47 ).
cnf(u3742,hypothesis,
i11 != i48 ).
cnf(u3747,hypothesis,
i11 != i49 ).
cnf(u3752,hypothesis,
i11 != i50 ).
cnf(u3757,hypothesis,
i12 != i13 ).
cnf(u3762,hypothesis,
i12 != i14 ).
cnf(u3767,hypothesis,
i12 != i15 ).
cnf(u3772,hypothesis,
i12 != i16 ).
cnf(u3777,hypothesis,
i12 != i17 ).
cnf(u3782,hypothesis,
i12 != i18 ).
cnf(u3787,hypothesis,
i12 != i19 ).
cnf(u3792,hypothesis,
i12 != i20 ).
cnf(u3797,hypothesis,
i12 != i21 ).
cnf(u3802,hypothesis,
i12 != i22 ).
cnf(u3807,hypothesis,
i12 != i23 ).
cnf(u3812,hypothesis,
i12 != i24 ).
cnf(u3817,hypothesis,
i12 != i25 ).
cnf(u3822,hypothesis,
i12 != i26 ).
cnf(u3827,hypothesis,
i12 != i27 ).
cnf(u3832,hypothesis,
i12 != i28 ).
cnf(u3837,hypothesis,
i12 != i29 ).
cnf(u3842,hypothesis,
i12 != i30 ).
cnf(u3847,hypothesis,
i12 != i31 ).
cnf(u3852,hypothesis,
i12 != i32 ).
cnf(u3857,hypothesis,
i12 != i33 ).
cnf(u3862,hypothesis,
i12 != i34 ).
cnf(u3867,hypothesis,
i12 != i35 ).
cnf(u3872,hypothesis,
i12 != i36 ).
cnf(u3877,hypothesis,
i12 != i37 ).
cnf(u3882,hypothesis,
i12 != i38 ).
cnf(u3887,hypothesis,
i12 != i39 ).
cnf(u3892,hypothesis,
i12 != i40 ).
cnf(u3897,hypothesis,
i12 != i41 ).
cnf(u3902,hypothesis,
i12 != i42 ).
cnf(u3907,hypothesis,
i12 != i43 ).
cnf(u3912,hypothesis,
i12 != i44 ).
cnf(u3917,hypothesis,
i12 != i45 ).
cnf(u3922,hypothesis,
i12 != i46 ).
cnf(u3927,hypothesis,
i12 != i47 ).
cnf(u3932,hypothesis,
i12 != i48 ).
cnf(u3937,hypothesis,
i12 != i49 ).
cnf(u3942,hypothesis,
i12 != i50 ).
cnf(u3947,hypothesis,
i13 != i14 ).
cnf(u3952,hypothesis,
i13 != i15 ).
cnf(u3957,hypothesis,
i13 != i16 ).
cnf(u3962,hypothesis,
i13 != i17 ).
cnf(u3967,hypothesis,
i13 != i18 ).
cnf(u3972,hypothesis,
i13 != i19 ).
cnf(u3977,hypothesis,
i13 != i20 ).
cnf(u3982,hypothesis,
i13 != i21 ).
cnf(u3987,hypothesis,
i13 != i22 ).
cnf(u3992,hypothesis,
i13 != i23 ).
cnf(u3997,hypothesis,
i13 != i24 ).
cnf(u4002,hypothesis,
i13 != i25 ).
cnf(u4007,hypothesis,
i13 != i26 ).
cnf(u4012,hypothesis,
i13 != i27 ).
cnf(u4017,hypothesis,
i13 != i28 ).
cnf(u4022,hypothesis,
i13 != i29 ).
cnf(u4027,hypothesis,
i13 != i30 ).
cnf(u4032,hypothesis,
i13 != i31 ).
cnf(u4037,hypothesis,
i13 != i32 ).
cnf(u4042,hypothesis,
i13 != i33 ).
cnf(u4047,hypothesis,
i13 != i34 ).
cnf(u4052,hypothesis,
i13 != i35 ).
cnf(u4057,hypothesis,
i13 != i36 ).
cnf(u4062,hypothesis,
i13 != i37 ).
cnf(u4067,hypothesis,
i13 != i38 ).
cnf(u4072,hypothesis,
i13 != i39 ).
cnf(u4077,hypothesis,
i13 != i40 ).
cnf(u4082,hypothesis,
i13 != i41 ).
cnf(u4087,hypothesis,
i13 != i42 ).
cnf(u4092,hypothesis,
i13 != i43 ).
cnf(u4097,hypothesis,
i13 != i44 ).
cnf(u4102,hypothesis,
i13 != i45 ).
cnf(u4107,hypothesis,
i13 != i46 ).
cnf(u4112,hypothesis,
i13 != i47 ).
cnf(u4117,hypothesis,
i13 != i48 ).
cnf(u4122,hypothesis,
i13 != i49 ).
cnf(u4127,hypothesis,
i13 != i50 ).
cnf(u4132,hypothesis,
i14 != i15 ).
cnf(u4137,hypothesis,
i14 != i16 ).
cnf(u4142,hypothesis,
i14 != i17 ).
cnf(u4147,hypothesis,
i14 != i18 ).
cnf(u4152,hypothesis,
i14 != i19 ).
cnf(u4157,hypothesis,
i14 != i20 ).
cnf(u4162,hypothesis,
i14 != i21 ).
cnf(u4167,hypothesis,
i14 != i22 ).
cnf(u4172,hypothesis,
i14 != i23 ).
cnf(u4177,hypothesis,
i14 != i24 ).
cnf(u4182,hypothesis,
i14 != i25 ).
cnf(u4187,hypothesis,
i14 != i26 ).
cnf(u4192,hypothesis,
i14 != i27 ).
cnf(u4197,hypothesis,
i14 != i28 ).
cnf(u4202,hypothesis,
i14 != i29 ).
cnf(u4207,hypothesis,
i14 != i30 ).
cnf(u4212,hypothesis,
i14 != i31 ).
cnf(u4217,hypothesis,
i14 != i32 ).
cnf(u4222,hypothesis,
i14 != i33 ).
cnf(u4227,hypothesis,
i14 != i34 ).
cnf(u4232,hypothesis,
i14 != i35 ).
cnf(u4237,hypothesis,
i14 != i36 ).
cnf(u4242,hypothesis,
i14 != i37 ).
cnf(u4247,hypothesis,
i14 != i38 ).
cnf(u4252,hypothesis,
i14 != i39 ).
cnf(u4257,hypothesis,
i14 != i40 ).
cnf(u4262,hypothesis,
i14 != i41 ).
cnf(u4267,hypothesis,
i14 != i42 ).
cnf(u4272,hypothesis,
i14 != i43 ).
cnf(u4277,hypothesis,
i14 != i44 ).
cnf(u4282,hypothesis,
i14 != i45 ).
cnf(u4287,hypothesis,
i14 != i46 ).
cnf(u4292,hypothesis,
i14 != i47 ).
cnf(u4297,hypothesis,
i14 != i48 ).
cnf(u4302,hypothesis,
i14 != i49 ).
cnf(u4307,hypothesis,
i14 != i50 ).
cnf(u4312,hypothesis,
i15 != i16 ).
cnf(u4317,hypothesis,
i15 != i17 ).
cnf(u4322,hypothesis,
i15 != i18 ).
cnf(u4327,hypothesis,
i15 != i19 ).
cnf(u4332,hypothesis,
i15 != i20 ).
cnf(u4337,hypothesis,
i15 != i21 ).
cnf(u4342,hypothesis,
i15 != i22 ).
cnf(u4347,hypothesis,
i15 != i23 ).
cnf(u4352,hypothesis,
i15 != i24 ).
cnf(u4357,hypothesis,
i15 != i25 ).
cnf(u4362,hypothesis,
i15 != i26 ).
cnf(u4367,hypothesis,
i15 != i27 ).
cnf(u4372,hypothesis,
i15 != i28 ).
cnf(u4377,hypothesis,
i15 != i29 ).
cnf(u4382,hypothesis,
i15 != i30 ).
cnf(u4387,hypothesis,
i15 != i31 ).
cnf(u4392,hypothesis,
i15 != i32 ).
cnf(u4397,hypothesis,
i15 != i33 ).
cnf(u4402,hypothesis,
i15 != i34 ).
cnf(u4407,hypothesis,
i15 != i35 ).
cnf(u4412,hypothesis,
i15 != i36 ).
cnf(u4417,hypothesis,
i15 != i37 ).
cnf(u4422,hypothesis,
i15 != i38 ).
cnf(u4427,hypothesis,
i15 != i39 ).
cnf(u4432,hypothesis,
i15 != i40 ).
cnf(u4437,hypothesis,
i15 != i41 ).
cnf(u4442,hypothesis,
i15 != i42 ).
cnf(u4447,hypothesis,
i15 != i43 ).
cnf(u4452,hypothesis,
i15 != i44 ).
cnf(u4457,hypothesis,
i15 != i45 ).
cnf(u4462,hypothesis,
i15 != i46 ).
cnf(u4467,hypothesis,
i15 != i47 ).
cnf(u4472,hypothesis,
i15 != i48 ).
cnf(u4477,hypothesis,
i15 != i49 ).
cnf(u4482,hypothesis,
i15 != i50 ).
cnf(u4487,hypothesis,
i16 != i17 ).
cnf(u4492,hypothesis,
i16 != i18 ).
cnf(u4497,hypothesis,
i16 != i19 ).
cnf(u4502,hypothesis,
i16 != i20 ).
cnf(u4507,hypothesis,
i16 != i21 ).
cnf(u4512,hypothesis,
i16 != i22 ).
cnf(u4517,hypothesis,
i16 != i23 ).
cnf(u4522,hypothesis,
i16 != i24 ).
cnf(u4527,hypothesis,
i16 != i25 ).
cnf(u4532,hypothesis,
i16 != i26 ).
cnf(u4537,hypothesis,
i16 != i27 ).
cnf(u4542,hypothesis,
i16 != i28 ).
cnf(u4547,hypothesis,
i16 != i29 ).
cnf(u4552,hypothesis,
i16 != i30 ).
cnf(u4557,hypothesis,
i16 != i31 ).
cnf(u4562,hypothesis,
i16 != i32 ).
cnf(u4567,hypothesis,
i16 != i33 ).
cnf(u4572,hypothesis,
i16 != i34 ).
cnf(u4577,hypothesis,
i16 != i35 ).
cnf(u4582,hypothesis,
i16 != i36 ).
cnf(u4587,hypothesis,
i16 != i37 ).
cnf(u4592,hypothesis,
i16 != i38 ).
cnf(u4597,hypothesis,
i16 != i39 ).
cnf(u4602,hypothesis,
i16 != i40 ).
cnf(u4607,hypothesis,
i16 != i41 ).
cnf(u4612,hypothesis,
i16 != i42 ).
cnf(u4617,hypothesis,
i16 != i43 ).
cnf(u4622,hypothesis,
i16 != i44 ).
cnf(u4627,hypothesis,
i16 != i45 ).
cnf(u4632,hypothesis,
i16 != i46 ).
cnf(u4637,hypothesis,
i16 != i47 ).
cnf(u4642,hypothesis,
i16 != i48 ).
cnf(u4647,hypothesis,
i16 != i49 ).
cnf(u4652,hypothesis,
i16 != i50 ).
cnf(u4657,hypothesis,
i17 != i18 ).
cnf(u4662,hypothesis,
i17 != i19 ).
cnf(u4667,hypothesis,
i17 != i20 ).
cnf(u4672,hypothesis,
i17 != i21 ).
cnf(u4677,hypothesis,
i17 != i22 ).
cnf(u4682,hypothesis,
i17 != i23 ).
cnf(u4687,hypothesis,
i17 != i24 ).
cnf(u4692,hypothesis,
i17 != i25 ).
cnf(u4697,hypothesis,
i17 != i26 ).
cnf(u4702,hypothesis,
i17 != i27 ).
cnf(u4707,hypothesis,
i17 != i28 ).
cnf(u4712,hypothesis,
i17 != i29 ).
cnf(u4717,hypothesis,
i17 != i30 ).
cnf(u4722,hypothesis,
i17 != i31 ).
cnf(u4727,hypothesis,
i17 != i32 ).
cnf(u4732,hypothesis,
i17 != i33 ).
cnf(u4737,hypothesis,
i17 != i34 ).
cnf(u4742,hypothesis,
i17 != i35 ).
cnf(u4747,hypothesis,
i17 != i36 ).
cnf(u4752,hypothesis,
i17 != i37 ).
cnf(u4757,hypothesis,
i17 != i38 ).
cnf(u4762,hypothesis,
i17 != i39 ).
cnf(u4767,hypothesis,
i17 != i40 ).
cnf(u4772,hypothesis,
i17 != i41 ).
cnf(u4777,hypothesis,
i17 != i42 ).
cnf(u4782,hypothesis,
i17 != i43 ).
cnf(u4787,hypothesis,
i17 != i44 ).
cnf(u4792,hypothesis,
i17 != i45 ).
cnf(u4797,hypothesis,
i17 != i46 ).
cnf(u4802,hypothesis,
i17 != i47 ).
cnf(u4807,hypothesis,
i17 != i48 ).
cnf(u4812,hypothesis,
i17 != i49 ).
cnf(u4817,hypothesis,
i17 != i50 ).
cnf(u4822,hypothesis,
i18 != i19 ).
cnf(u4827,hypothesis,
i18 != i20 ).
cnf(u4832,hypothesis,
i18 != i21 ).
cnf(u4837,hypothesis,
i18 != i22 ).
cnf(u4842,hypothesis,
i18 != i23 ).
cnf(u4847,hypothesis,
i18 != i24 ).
cnf(u4852,hypothesis,
i18 != i25 ).
cnf(u4857,hypothesis,
i18 != i26 ).
cnf(u4862,hypothesis,
i18 != i27 ).
cnf(u4867,hypothesis,
i18 != i28 ).
cnf(u4872,hypothesis,
i18 != i29 ).
cnf(u4877,hypothesis,
i18 != i30 ).
cnf(u4882,hypothesis,
i18 != i31 ).
cnf(u4887,hypothesis,
i18 != i32 ).
cnf(u4892,hypothesis,
i18 != i33 ).
cnf(u4897,hypothesis,
i18 != i34 ).
cnf(u4902,hypothesis,
i18 != i35 ).
cnf(u4907,hypothesis,
i18 != i36 ).
cnf(u4912,hypothesis,
i18 != i37 ).
cnf(u4917,hypothesis,
i18 != i38 ).
cnf(u4922,hypothesis,
i18 != i39 ).
cnf(u4927,hypothesis,
i18 != i40 ).
cnf(u4932,hypothesis,
i18 != i41 ).
cnf(u4937,hypothesis,
i18 != i42 ).
cnf(u4942,hypothesis,
i18 != i43 ).
cnf(u4947,hypothesis,
i18 != i44 ).
cnf(u4952,hypothesis,
i18 != i45 ).
cnf(u4957,hypothesis,
i18 != i46 ).
cnf(u4962,hypothesis,
i18 != i47 ).
cnf(u4967,hypothesis,
i18 != i48 ).
cnf(u4972,hypothesis,
i18 != i49 ).
cnf(u4977,hypothesis,
i18 != i50 ).
cnf(u4982,hypothesis,
i19 != i20 ).
cnf(u4987,hypothesis,
i19 != i21 ).
cnf(u4992,hypothesis,
i19 != i22 ).
cnf(u4997,hypothesis,
i19 != i23 ).
cnf(u5002,hypothesis,
i19 != i24 ).
cnf(u5007,hypothesis,
i19 != i25 ).
cnf(u5012,hypothesis,
i19 != i26 ).
cnf(u5017,hypothesis,
i19 != i27 ).
cnf(u5022,hypothesis,
i19 != i28 ).
cnf(u5027,hypothesis,
i19 != i29 ).
cnf(u5032,hypothesis,
i19 != i30 ).
cnf(u5037,hypothesis,
i19 != i31 ).
cnf(u5042,hypothesis,
i19 != i32 ).
cnf(u5047,hypothesis,
i19 != i33 ).
cnf(u5052,hypothesis,
i19 != i34 ).
cnf(u5057,hypothesis,
i19 != i35 ).
cnf(u5062,hypothesis,
i19 != i36 ).
cnf(u5067,hypothesis,
i19 != i37 ).
cnf(u5072,hypothesis,
i19 != i38 ).
cnf(u5077,hypothesis,
i19 != i39 ).
cnf(u5082,hypothesis,
i19 != i40 ).
cnf(u5087,hypothesis,
i19 != i41 ).
cnf(u5092,hypothesis,
i19 != i42 ).
cnf(u5097,hypothesis,
i19 != i43 ).
cnf(u5102,hypothesis,
i19 != i44 ).
cnf(u5107,hypothesis,
i19 != i45 ).
cnf(u5112,hypothesis,
i19 != i46 ).
cnf(u5117,hypothesis,
i19 != i47 ).
cnf(u5122,hypothesis,
i19 != i48 ).
cnf(u5127,hypothesis,
i19 != i49 ).
cnf(u5132,hypothesis,
i19 != i50 ).
cnf(u5137,hypothesis,
i20 != i21 ).
cnf(u5142,hypothesis,
i20 != i22 ).
cnf(u5147,hypothesis,
i20 != i23 ).
cnf(u5152,hypothesis,
i20 != i24 ).
cnf(u5157,hypothesis,
i20 != i25 ).
cnf(u5162,hypothesis,
i20 != i26 ).
cnf(u5167,hypothesis,
i20 != i27 ).
cnf(u5172,hypothesis,
i20 != i28 ).
cnf(u5177,hypothesis,
i20 != i29 ).
cnf(u5182,hypothesis,
i20 != i30 ).
cnf(u5187,hypothesis,
i20 != i31 ).
cnf(u5192,hypothesis,
i20 != i32 ).
cnf(u5197,hypothesis,
i20 != i33 ).
cnf(u5202,hypothesis,
i20 != i34 ).
cnf(u5207,hypothesis,
i20 != i35 ).
cnf(u5212,hypothesis,
i20 != i36 ).
cnf(u5217,hypothesis,
i20 != i37 ).
cnf(u5222,hypothesis,
i20 != i38 ).
cnf(u5227,hypothesis,
i20 != i39 ).
cnf(u5232,hypothesis,
i20 != i40 ).
cnf(u5237,hypothesis,
i20 != i41 ).
cnf(u5242,hypothesis,
i20 != i42 ).
cnf(u5247,hypothesis,
i20 != i43 ).
cnf(u5252,hypothesis,
i20 != i44 ).
cnf(u5257,hypothesis,
i20 != i45 ).
cnf(u5262,hypothesis,
i20 != i46 ).
cnf(u5267,hypothesis,
i20 != i47 ).
cnf(u5272,hypothesis,
i20 != i48 ).
cnf(u5277,hypothesis,
i20 != i49 ).
cnf(u5282,hypothesis,
i20 != i50 ).
cnf(u5287,hypothesis,
i21 != i22 ).
cnf(u5292,hypothesis,
i21 != i23 ).
cnf(u5297,hypothesis,
i21 != i24 ).
cnf(u5302,hypothesis,
i21 != i25 ).
cnf(u5307,hypothesis,
i21 != i26 ).
cnf(u5312,hypothesis,
i21 != i27 ).
cnf(u5317,hypothesis,
i21 != i28 ).
cnf(u5322,hypothesis,
i21 != i29 ).
cnf(u5327,hypothesis,
i21 != i30 ).
cnf(u5332,hypothesis,
i21 != i31 ).
cnf(u5337,hypothesis,
i21 != i32 ).
cnf(u5342,hypothesis,
i21 != i33 ).
cnf(u5347,hypothesis,
i21 != i34 ).
cnf(u5352,hypothesis,
i21 != i35 ).
cnf(u5357,hypothesis,
i21 != i36 ).
cnf(u5362,hypothesis,
i21 != i37 ).
cnf(u5367,hypothesis,
i21 != i38 ).
cnf(u5372,hypothesis,
i21 != i39 ).
cnf(u5377,hypothesis,
i21 != i40 ).
cnf(u5382,hypothesis,
i21 != i41 ).
cnf(u5387,hypothesis,
i21 != i42 ).
cnf(u5392,hypothesis,
i21 != i43 ).
cnf(u5397,hypothesis,
i21 != i44 ).
cnf(u5402,hypothesis,
i21 != i45 ).
cnf(u5407,hypothesis,
i21 != i46 ).
cnf(u5412,hypothesis,
i21 != i47 ).
cnf(u5417,hypothesis,
i21 != i48 ).
cnf(u5422,hypothesis,
i21 != i49 ).
cnf(u5427,hypothesis,
i21 != i50 ).
cnf(u5432,hypothesis,
i22 != i23 ).
cnf(u5437,hypothesis,
i22 != i24 ).
cnf(u5442,hypothesis,
i22 != i25 ).
cnf(u5447,hypothesis,
i22 != i26 ).
cnf(u5452,hypothesis,
i22 != i27 ).
cnf(u5457,hypothesis,
i22 != i28 ).
cnf(u5462,hypothesis,
i22 != i29 ).
cnf(u5467,hypothesis,
i22 != i30 ).
cnf(u5472,hypothesis,
i22 != i31 ).
cnf(u5477,hypothesis,
i22 != i32 ).
cnf(u5482,hypothesis,
i22 != i33 ).
cnf(u5487,hypothesis,
i22 != i34 ).
cnf(u5492,hypothesis,
i22 != i35 ).
cnf(u5497,hypothesis,
i22 != i36 ).
cnf(u5502,hypothesis,
i22 != i37 ).
cnf(u5507,hypothesis,
i22 != i38 ).
cnf(u5512,hypothesis,
i22 != i39 ).
cnf(u5517,hypothesis,
i22 != i40 ).
cnf(u5522,hypothesis,
i22 != i41 ).
cnf(u5527,hypothesis,
i22 != i42 ).
cnf(u5532,hypothesis,
i22 != i43 ).
cnf(u5537,hypothesis,
i22 != i44 ).
cnf(u5542,hypothesis,
i22 != i45 ).
cnf(u5547,hypothesis,
i22 != i46 ).
cnf(u5552,hypothesis,
i22 != i47 ).
cnf(u5557,hypothesis,
i22 != i48 ).
cnf(u5562,hypothesis,
i22 != i49 ).
cnf(u5567,hypothesis,
i22 != i50 ).
cnf(u5572,hypothesis,
i23 != i24 ).
cnf(u5577,hypothesis,
i23 != i25 ).
cnf(u5582,hypothesis,
i23 != i26 ).
cnf(u5587,hypothesis,
i23 != i27 ).
cnf(u5592,hypothesis,
i23 != i28 ).
cnf(u5597,hypothesis,
i23 != i29 ).
cnf(u5602,hypothesis,
i23 != i30 ).
cnf(u5607,hypothesis,
i23 != i31 ).
cnf(u5612,hypothesis,
i23 != i32 ).
cnf(u5617,hypothesis,
i23 != i33 ).
cnf(u5622,hypothesis,
i23 != i34 ).
cnf(u5627,hypothesis,
i23 != i35 ).
cnf(u5632,hypothesis,
i23 != i36 ).
cnf(u5637,hypothesis,
i23 != i37 ).
cnf(u5642,hypothesis,
i23 != i38 ).
cnf(u5647,hypothesis,
i23 != i39 ).
cnf(u5652,hypothesis,
i23 != i40 ).
cnf(u5657,hypothesis,
i23 != i41 ).
cnf(u5662,hypothesis,
i23 != i42 ).
cnf(u5667,hypothesis,
i23 != i43 ).
cnf(u5672,hypothesis,
i23 != i44 ).
cnf(u5677,hypothesis,
i23 != i45 ).
cnf(u5682,hypothesis,
i23 != i46 ).
cnf(u5687,hypothesis,
i23 != i47 ).
cnf(u5692,hypothesis,
i23 != i48 ).
cnf(u5697,hypothesis,
i23 != i49 ).
cnf(u5702,hypothesis,
i23 != i50 ).
cnf(u5707,hypothesis,
i24 != i25 ).
cnf(u5712,hypothesis,
i24 != i26 ).
cnf(u5717,hypothesis,
i24 != i27 ).
cnf(u5722,hypothesis,
i24 != i28 ).
cnf(u5727,hypothesis,
i24 != i29 ).
cnf(u5732,hypothesis,
i24 != i30 ).
cnf(u5737,hypothesis,
i24 != i31 ).
cnf(u5742,hypothesis,
i24 != i32 ).
cnf(u5747,hypothesis,
i24 != i33 ).
cnf(u5752,hypothesis,
i24 != i34 ).
cnf(u5757,hypothesis,
i24 != i35 ).
cnf(u5762,hypothesis,
i24 != i36 ).
cnf(u5767,hypothesis,
i24 != i37 ).
cnf(u5772,hypothesis,
i24 != i38 ).
cnf(u5777,hypothesis,
i24 != i39 ).
cnf(u5782,hypothesis,
i24 != i40 ).
cnf(u5787,hypothesis,
i24 != i41 ).
cnf(u5792,hypothesis,
i24 != i42 ).
cnf(u5797,hypothesis,
i24 != i43 ).
cnf(u5802,hypothesis,
i24 != i44 ).
cnf(u5807,hypothesis,
i24 != i45 ).
cnf(u5812,hypothesis,
i24 != i46 ).
cnf(u5817,hypothesis,
i24 != i47 ).
cnf(u5822,hypothesis,
i24 != i48 ).
cnf(u5827,hypothesis,
i24 != i49 ).
cnf(u5832,hypothesis,
i24 != i50 ).
cnf(u5837,hypothesis,
i25 != i26 ).
cnf(u5842,hypothesis,
i25 != i27 ).
cnf(u5847,hypothesis,
i25 != i28 ).
cnf(u5852,hypothesis,
i25 != i29 ).
cnf(u5857,hypothesis,
i25 != i30 ).
cnf(u5862,hypothesis,
i25 != i31 ).
cnf(u5867,hypothesis,
i25 != i32 ).
cnf(u5872,hypothesis,
i25 != i33 ).
cnf(u5877,hypothesis,
i25 != i34 ).
cnf(u5882,hypothesis,
i25 != i35 ).
cnf(u5887,hypothesis,
i25 != i36 ).
cnf(u5892,hypothesis,
i25 != i37 ).
cnf(u5897,hypothesis,
i25 != i38 ).
cnf(u5902,hypothesis,
i25 != i39 ).
cnf(u5907,hypothesis,
i25 != i40 ).
cnf(u5912,hypothesis,
i25 != i41 ).
cnf(u5917,hypothesis,
i25 != i42 ).
cnf(u5922,hypothesis,
i25 != i43 ).
cnf(u5927,hypothesis,
i25 != i44 ).
cnf(u5932,hypothesis,
i25 != i45 ).
cnf(u5937,hypothesis,
i25 != i46 ).
cnf(u5942,hypothesis,
i25 != i47 ).
cnf(u5947,hypothesis,
i25 != i48 ).
cnf(u5952,hypothesis,
i25 != i49 ).
cnf(u5957,hypothesis,
i25 != i50 ).
cnf(u5962,hypothesis,
i26 != i27 ).
cnf(u5967,hypothesis,
i26 != i28 ).
cnf(u5972,hypothesis,
i26 != i29 ).
cnf(u5977,hypothesis,
i26 != i30 ).
cnf(u5982,hypothesis,
i26 != i31 ).
cnf(u5987,hypothesis,
i26 != i32 ).
cnf(u5992,hypothesis,
i26 != i33 ).
cnf(u5997,hypothesis,
i26 != i34 ).
cnf(u6002,hypothesis,
i26 != i35 ).
cnf(u6007,hypothesis,
i26 != i36 ).
cnf(u6012,hypothesis,
i26 != i37 ).
cnf(u6017,hypothesis,
i26 != i38 ).
cnf(u6022,hypothesis,
i26 != i39 ).
cnf(u6027,hypothesis,
i26 != i40 ).
cnf(u6032,hypothesis,
i26 != i41 ).
cnf(u6037,hypothesis,
i26 != i42 ).
cnf(u6042,hypothesis,
i26 != i43 ).
cnf(u6047,hypothesis,
i26 != i44 ).
cnf(u6052,hypothesis,
i26 != i45 ).
cnf(u6057,hypothesis,
i26 != i46 ).
cnf(u6062,hypothesis,
i26 != i47 ).
cnf(u6067,hypothesis,
i26 != i48 ).
cnf(u6072,hypothesis,
i26 != i49 ).
cnf(u6077,hypothesis,
i26 != i50 ).
cnf(u6082,hypothesis,
i27 != i28 ).
cnf(u6087,hypothesis,
i27 != i29 ).
cnf(u6092,hypothesis,
i27 != i30 ).
cnf(u6097,hypothesis,
i27 != i31 ).
cnf(u6102,hypothesis,
i27 != i32 ).
cnf(u6107,hypothesis,
i27 != i33 ).
cnf(u6112,hypothesis,
i27 != i34 ).
cnf(u6117,hypothesis,
i27 != i35 ).
cnf(u6122,hypothesis,
i27 != i36 ).
cnf(u6127,hypothesis,
i27 != i37 ).
cnf(u6132,hypothesis,
i27 != i38 ).
cnf(u6137,hypothesis,
i27 != i39 ).
cnf(u6142,hypothesis,
i27 != i40 ).
cnf(u6147,hypothesis,
i27 != i41 ).
cnf(u6152,hypothesis,
i27 != i42 ).
cnf(u6157,hypothesis,
i27 != i43 ).
cnf(u6162,hypothesis,
i27 != i44 ).
cnf(u6167,hypothesis,
i27 != i45 ).
cnf(u6172,hypothesis,
i27 != i46 ).
cnf(u6177,hypothesis,
i27 != i47 ).
cnf(u6182,hypothesis,
i27 != i48 ).
cnf(u6187,hypothesis,
i27 != i49 ).
cnf(u6192,hypothesis,
i27 != i50 ).
cnf(u6197,hypothesis,
i28 != i29 ).
cnf(u6202,hypothesis,
i28 != i30 ).
cnf(u6207,hypothesis,
i28 != i31 ).
cnf(u6212,hypothesis,
i28 != i32 ).
cnf(u6217,hypothesis,
i28 != i33 ).
cnf(u6222,hypothesis,
i28 != i34 ).
cnf(u6227,hypothesis,
i28 != i35 ).
cnf(u6232,hypothesis,
i28 != i36 ).
cnf(u6237,hypothesis,
i28 != i37 ).
cnf(u6242,hypothesis,
i28 != i38 ).
cnf(u6247,hypothesis,
i28 != i39 ).
cnf(u6252,hypothesis,
i28 != i40 ).
cnf(u6257,hypothesis,
i28 != i41 ).
cnf(u6262,hypothesis,
i28 != i42 ).
cnf(u6267,hypothesis,
i28 != i43 ).
cnf(u6272,hypothesis,
i28 != i44 ).
cnf(u6277,hypothesis,
i28 != i45 ).
cnf(u6282,hypothesis,
i28 != i46 ).
cnf(u6287,hypothesis,
i28 != i47 ).
cnf(u6292,hypothesis,
i28 != i48 ).
cnf(u6297,hypothesis,
i28 != i49 ).
cnf(u6302,hypothesis,
i28 != i50 ).
cnf(u6307,hypothesis,
i29 != i30 ).
cnf(u6312,hypothesis,
i29 != i31 ).
cnf(u6317,hypothesis,
i29 != i32 ).
cnf(u6322,hypothesis,
i29 != i33 ).
cnf(u6327,hypothesis,
i29 != i34 ).
cnf(u6332,hypothesis,
i29 != i35 ).
cnf(u6337,hypothesis,
i29 != i36 ).
cnf(u6342,hypothesis,
i29 != i37 ).
cnf(u6347,hypothesis,
i29 != i38 ).
cnf(u6352,hypothesis,
i29 != i39 ).
cnf(u6357,hypothesis,
i29 != i40 ).
cnf(u6362,hypothesis,
i29 != i41 ).
cnf(u6367,hypothesis,
i29 != i42 ).
cnf(u6372,hypothesis,
i29 != i43 ).
cnf(u6377,hypothesis,
i29 != i44 ).
cnf(u6382,hypothesis,
i29 != i45 ).
cnf(u6387,hypothesis,
i29 != i46 ).
cnf(u6392,hypothesis,
i29 != i47 ).
cnf(u6397,hypothesis,
i29 != i48 ).
cnf(u6402,hypothesis,
i29 != i49 ).
cnf(u6407,hypothesis,
i29 != i50 ).
cnf(u6412,hypothesis,
i30 != i31 ).
cnf(u6417,hypothesis,
i30 != i32 ).
cnf(u6422,hypothesis,
i30 != i33 ).
cnf(u6427,hypothesis,
i30 != i34 ).
cnf(u6432,hypothesis,
i30 != i35 ).
cnf(u6437,hypothesis,
i30 != i36 ).
cnf(u6442,hypothesis,
i30 != i37 ).
cnf(u6447,hypothesis,
i30 != i38 ).
cnf(u6452,hypothesis,
i30 != i39 ).
cnf(u6457,hypothesis,
i30 != i40 ).
cnf(u6462,hypothesis,
i30 != i41 ).
cnf(u6467,hypothesis,
i30 != i42 ).
cnf(u6472,hypothesis,
i30 != i43 ).
cnf(u6477,hypothesis,
i30 != i44 ).
cnf(u6482,hypothesis,
i30 != i45 ).
cnf(u6487,hypothesis,
i30 != i46 ).
cnf(u6492,hypothesis,
i30 != i47 ).
cnf(u6497,hypothesis,
i30 != i48 ).
cnf(u6502,hypothesis,
i30 != i49 ).
cnf(u6507,hypothesis,
i30 != i50 ).
cnf(u6512,hypothesis,
i31 != i32 ).
cnf(u6517,hypothesis,
i31 != i33 ).
cnf(u6522,hypothesis,
i31 != i34 ).
cnf(u6527,hypothesis,
i31 != i35 ).
cnf(u6532,hypothesis,
i31 != i36 ).
cnf(u6537,hypothesis,
i31 != i37 ).
cnf(u6542,hypothesis,
i31 != i38 ).
cnf(u6547,hypothesis,
i31 != i39 ).
cnf(u6552,hypothesis,
i31 != i40 ).
cnf(u6557,hypothesis,
i31 != i41 ).
cnf(u6562,hypothesis,
i31 != i42 ).
cnf(u6567,hypothesis,
i31 != i43 ).
cnf(u6572,hypothesis,
i31 != i44 ).
cnf(u6577,hypothesis,
i31 != i45 ).
cnf(u6582,hypothesis,
i31 != i46 ).
cnf(u6587,hypothesis,
i31 != i47 ).
cnf(u6592,hypothesis,
i31 != i48 ).
cnf(u6597,hypothesis,
i31 != i49 ).
cnf(u6602,hypothesis,
i31 != i50 ).
cnf(u6607,hypothesis,
i32 != i33 ).
cnf(u6612,hypothesis,
i32 != i34 ).
cnf(u6617,hypothesis,
i32 != i35 ).
cnf(u6622,hypothesis,
i32 != i36 ).
cnf(u6627,hypothesis,
i32 != i37 ).
cnf(u6632,hypothesis,
i32 != i38 ).
cnf(u6637,hypothesis,
i32 != i39 ).
cnf(u6642,hypothesis,
i32 != i40 ).
cnf(u6647,hypothesis,
i32 != i41 ).
cnf(u6652,hypothesis,
i32 != i42 ).
cnf(u6657,hypothesis,
i32 != i43 ).
cnf(u6662,hypothesis,
i32 != i44 ).
cnf(u6667,hypothesis,
i32 != i45 ).
cnf(u6672,hypothesis,
i32 != i46 ).
cnf(u6677,hypothesis,
i32 != i47 ).
cnf(u6682,hypothesis,
i32 != i48 ).
cnf(u6687,hypothesis,
i32 != i49 ).
cnf(u6692,hypothesis,
i32 != i50 ).
cnf(u6697,hypothesis,
i33 != i34 ).
cnf(u6702,hypothesis,
i33 != i35 ).
cnf(u6707,hypothesis,
i33 != i36 ).
cnf(u6712,hypothesis,
i33 != i37 ).
cnf(u6717,hypothesis,
i33 != i38 ).
cnf(u6722,hypothesis,
i33 != i39 ).
cnf(u6727,hypothesis,
i33 != i40 ).
cnf(u6732,hypothesis,
i33 != i41 ).
cnf(u6737,hypothesis,
i33 != i42 ).
cnf(u6742,hypothesis,
i33 != i43 ).
cnf(u6747,hypothesis,
i33 != i44 ).
cnf(u6752,hypothesis,
i33 != i45 ).
cnf(u6757,hypothesis,
i33 != i46 ).
cnf(u6762,hypothesis,
i33 != i47 ).
cnf(u6767,hypothesis,
i33 != i48 ).
cnf(u6772,hypothesis,
i33 != i49 ).
cnf(u6777,hypothesis,
i33 != i50 ).
cnf(u6782,hypothesis,
i34 != i35 ).
cnf(u6787,hypothesis,
i34 != i36 ).
cnf(u6792,hypothesis,
i34 != i37 ).
cnf(u6797,hypothesis,
i34 != i38 ).
cnf(u6802,hypothesis,
i34 != i39 ).
cnf(u6807,hypothesis,
i34 != i40 ).
cnf(u6812,hypothesis,
i34 != i41 ).
cnf(u6817,hypothesis,
i34 != i42 ).
cnf(u6822,hypothesis,
i34 != i43 ).
cnf(u6827,hypothesis,
i34 != i44 ).
cnf(u6832,hypothesis,
i34 != i45 ).
cnf(u6837,hypothesis,
i34 != i46 ).
cnf(u6842,hypothesis,
i34 != i47 ).
cnf(u6847,hypothesis,
i34 != i48 ).
cnf(u6852,hypothesis,
i34 != i49 ).
cnf(u6857,hypothesis,
i34 != i50 ).
cnf(u6862,hypothesis,
i35 != i36 ).
cnf(u6867,hypothesis,
i35 != i37 ).
cnf(u6872,hypothesis,
i35 != i38 ).
cnf(u6877,hypothesis,
i35 != i39 ).
cnf(u6882,hypothesis,
i35 != i40 ).
cnf(u6887,hypothesis,
i35 != i41 ).
cnf(u6892,hypothesis,
i35 != i42 ).
cnf(u6897,hypothesis,
i35 != i43 ).
cnf(u6902,hypothesis,
i35 != i44 ).
cnf(u6907,hypothesis,
i35 != i45 ).
cnf(u6912,hypothesis,
i35 != i46 ).
cnf(u6917,hypothesis,
i35 != i47 ).
cnf(u6922,hypothesis,
i35 != i48 ).
cnf(u6927,hypothesis,
i35 != i49 ).
cnf(u6932,hypothesis,
i35 != i50 ).
cnf(u6937,hypothesis,
i36 != i37 ).
cnf(u6942,hypothesis,
i36 != i38 ).
cnf(u6947,hypothesis,
i36 != i39 ).
cnf(u6952,hypothesis,
i36 != i40 ).
cnf(u6957,hypothesis,
i36 != i41 ).
cnf(u6962,hypothesis,
i36 != i42 ).
cnf(u6967,hypothesis,
i36 != i43 ).
cnf(u6972,hypothesis,
i36 != i44 ).
cnf(u6977,hypothesis,
i36 != i45 ).
cnf(u6982,hypothesis,
i36 != i46 ).
cnf(u6987,hypothesis,
i36 != i47 ).
cnf(u6992,hypothesis,
i36 != i48 ).
cnf(u6997,hypothesis,
i36 != i49 ).
cnf(u7002,hypothesis,
i36 != i50 ).
cnf(u7007,hypothesis,
i37 != i38 ).
cnf(u7012,hypothesis,
i37 != i39 ).
cnf(u7017,hypothesis,
i37 != i40 ).
cnf(u7022,hypothesis,
i37 != i41 ).
cnf(u7027,hypothesis,
i37 != i42 ).
cnf(u7032,hypothesis,
i37 != i43 ).
cnf(u7037,hypothesis,
i37 != i44 ).
cnf(u7042,hypothesis,
i37 != i45 ).
cnf(u7047,hypothesis,
i37 != i46 ).
cnf(u7052,hypothesis,
i37 != i47 ).
cnf(u7057,hypothesis,
i37 != i48 ).
cnf(u7062,hypothesis,
i37 != i49 ).
cnf(u7067,hypothesis,
i37 != i50 ).
cnf(u7072,hypothesis,
i38 != i39 ).
cnf(u7077,hypothesis,
i38 != i40 ).
cnf(u7082,hypothesis,
i38 != i41 ).
cnf(u7087,hypothesis,
i38 != i42 ).
cnf(u7092,hypothesis,
i38 != i43 ).
cnf(u7097,hypothesis,
i38 != i44 ).
cnf(u7102,hypothesis,
i38 != i45 ).
cnf(u7107,hypothesis,
i38 != i46 ).
cnf(u7112,hypothesis,
i38 != i47 ).
cnf(u7117,hypothesis,
i38 != i48 ).
cnf(u7122,hypothesis,
i38 != i49 ).
cnf(u7127,hypothesis,
i38 != i50 ).
cnf(u7132,hypothesis,
i39 != i40 ).
cnf(u7137,hypothesis,
i39 != i41 ).
cnf(u7142,hypothesis,
i39 != i42 ).
cnf(u7147,hypothesis,
i39 != i43 ).
cnf(u7152,hypothesis,
i39 != i44 ).
cnf(u7157,hypothesis,
i39 != i45 ).
cnf(u7162,hypothesis,
i39 != i46 ).
cnf(u7167,hypothesis,
i39 != i47 ).
cnf(u7172,hypothesis,
i39 != i48 ).
cnf(u7177,hypothesis,
i39 != i49 ).
cnf(u7182,hypothesis,
i39 != i50 ).
cnf(u7187,hypothesis,
i40 != i41 ).
cnf(u7192,hypothesis,
i40 != i42 ).
cnf(u7197,hypothesis,
i40 != i43 ).
cnf(u7202,hypothesis,
i40 != i44 ).
cnf(u7207,hypothesis,
i40 != i45 ).
cnf(u7212,hypothesis,
i40 != i46 ).
cnf(u7217,hypothesis,
i40 != i47 ).
cnf(u7222,hypothesis,
i40 != i48 ).
cnf(u7227,hypothesis,
i40 != i49 ).
cnf(u7232,hypothesis,
i40 != i50 ).
cnf(u7237,hypothesis,
i41 != i42 ).
cnf(u7242,hypothesis,
i41 != i43 ).
cnf(u7247,hypothesis,
i41 != i44 ).
cnf(u7252,hypothesis,
i41 != i45 ).
cnf(u7257,hypothesis,
i41 != i46 ).
cnf(u7262,hypothesis,
i41 != i47 ).
cnf(u7267,hypothesis,
i41 != i48 ).
cnf(u7272,hypothesis,
i41 != i49 ).
cnf(u7277,hypothesis,
i41 != i50 ).
cnf(u7282,hypothesis,
i42 != i43 ).
cnf(u7287,hypothesis,
i42 != i44 ).
cnf(u7292,hypothesis,
i42 != i45 ).
cnf(u7297,hypothesis,
i42 != i46 ).
cnf(u7302,hypothesis,
i42 != i47 ).
cnf(u7307,hypothesis,
i42 != i48 ).
cnf(u7312,hypothesis,
i42 != i49 ).
cnf(u7317,hypothesis,
i42 != i50 ).
cnf(u7322,hypothesis,
i43 != i44 ).
cnf(u7327,hypothesis,
i43 != i45 ).
cnf(u7332,hypothesis,
i43 != i46 ).
cnf(u7337,hypothesis,
i43 != i47 ).
cnf(u7342,hypothesis,
i43 != i48 ).
cnf(u7347,hypothesis,
i43 != i49 ).
cnf(u7352,hypothesis,
i43 != i50 ).
cnf(u7357,hypothesis,
i44 != i45 ).
cnf(u7362,hypothesis,
i44 != i46 ).
cnf(u7367,hypothesis,
i44 != i47 ).
cnf(u7372,hypothesis,
i44 != i48 ).
cnf(u7377,hypothesis,
i44 != i49 ).
cnf(u7382,hypothesis,
i44 != i50 ).
cnf(u7387,hypothesis,
i45 != i46 ).
cnf(u7392,hypothesis,
i45 != i47 ).
cnf(u7397,hypothesis,
i45 != i48 ).
cnf(u7402,hypothesis,
i45 != i49 ).
cnf(u7407,hypothesis,
i45 != i50 ).
cnf(u7412,hypothesis,
i46 != i47 ).
cnf(u7417,hypothesis,
i46 != i48 ).
cnf(u7422,hypothesis,
i46 != i49 ).
cnf(u7427,hypothesis,
i46 != i50 ).
cnf(u7432,hypothesis,
i47 != i48 ).
cnf(u7437,hypothesis,
i47 != i49 ).
cnf(u7442,hypothesis,
i47 != i50 ).
cnf(u7447,hypothesis,
i48 != i49 ).
cnf(u7452,hypothesis,
i48 != i50 ).
cnf(u7457,hypothesis,
i49 != i50 ).
cnf(u7462,hypothesis,
a_1799 = store(a_1798,i1,e1) ).
cnf(u7467,hypothesis,
a_1798 = store(a_1797,i31,e31) ).
cnf(u7472,hypothesis,
a_1797 = store(a_1796,i21,e21) ).
cnf(u7477,hypothesis,
a_1796 = store(a_1795,i24,e24) ).
cnf(u7482,hypothesis,
a_1795 = store(a_1794,i4,e4) ).
cnf(u7487,hypothesis,
a_1794 = store(a_1793,i32,e32) ).
cnf(u7492,hypothesis,
a_1793 = store(a_1792,i5,e5) ).
cnf(u7497,hypothesis,
a_1792 = store(a_1791,i12,e12) ).
cnf(u7502,hypothesis,
a_1791 = store(a_1790,i37,e37) ).
cnf(u7507,hypothesis,
a_1790 = store(a_1789,i3,e3) ).
cnf(u7512,hypothesis,
a_1789 = store(a_1788,i29,e29) ).
cnf(u7517,hypothesis,
a_1788 = store(a_1787,i48,e48) ).
cnf(u7522,hypothesis,
a_1787 = store(a_1786,i10,e10) ).
cnf(u7527,hypothesis,
a_1786 = store(a_1785,i2,e2) ).
cnf(u7532,hypothesis,
a_1785 = store(a_1784,i50,e50) ).
cnf(u7537,hypothesis,
a_1784 = store(a_1783,i35,e35) ).
cnf(u7542,hypothesis,
a_1783 = store(a_1782,i46,e46) ).
cnf(u7547,hypothesis,
a_1782 = store(a_1781,i25,e25) ).
cnf(u7552,hypothesis,
a_1781 = store(a_1780,i23,e23) ).
cnf(u7557,hypothesis,
a_1780 = store(a_1779,i38,e38) ).
cnf(u7562,hypothesis,
a_1779 = store(a_1778,i44,e44) ).
cnf(u7567,hypothesis,
a_1778 = store(a_1777,i36,e36) ).
cnf(u7572,hypothesis,
a_1777 = store(a_1776,i11,e11) ).
cnf(u7577,hypothesis,
a_1776 = store(a_1775,i34,e34) ).
cnf(u7582,hypothesis,
a_1775 = store(a_1774,i26,e26) ).
cnf(u7587,hypothesis,
a_1774 = store(a_1773,i18,e18) ).
cnf(u7592,hypothesis,
a_1773 = store(a_1772,i47,e47) ).
cnf(u7597,hypothesis,
a_1772 = store(a_1771,i42,e42) ).
cnf(u7602,hypothesis,
a_1771 = store(a_1770,i17,e17) ).
cnf(u7607,hypothesis,
a_1770 = store(a_1769,i9,e9) ).
cnf(u7612,hypothesis,
a_1769 = store(a_1768,i33,e33) ).
cnf(u7617,hypothesis,
a_1768 = store(a_1767,i7,e7) ).
cnf(u7622,hypothesis,
a_1767 = store(a_1766,i15,e15) ).
cnf(u7627,hypothesis,
a_1766 = store(a_1765,i27,e27) ).
cnf(u7632,hypothesis,
a_1765 = store(a_1764,i6,e6) ).
cnf(u7637,hypothesis,
a_1764 = store(a_1763,i13,e13) ).
cnf(u7642,hypothesis,
a_1763 = store(a_1762,i14,e14) ).
cnf(u7647,hypothesis,
a_1762 = store(a_1761,i49,e49) ).
cnf(u7652,hypothesis,
a_1761 = store(a_1760,i8,e8) ).
cnf(u7657,hypothesis,
a_1760 = store(a_1759,i16,e16) ).
cnf(u7662,hypothesis,
a_1759 = store(a_1758,i40,e40) ).
cnf(u7667,hypothesis,
a_1758 = store(a_1757,i20,e20) ).
cnf(u7672,hypothesis,
a_1757 = store(a_1756,i39,e39) ).
cnf(u7677,hypothesis,
a_1756 = store(a_1755,i22,e22) ).
cnf(u7682,hypothesis,
a_1755 = store(a_1754,i19,e19) ).
cnf(u7687,hypothesis,
a_1754 = store(a_1753,i28,e28) ).
cnf(u7692,hypothesis,
a_1753 = store(a_1752,i43,e43) ).
cnf(u7697,hypothesis,
a_1752 = store(a_1751,i45,e45) ).
cnf(u7702,hypothesis,
a_1751 = store(a_1750,i30,e30) ).
cnf(u7707,hypothesis,
a_1750 = store(a1,i41,e41) ).
cnf(u7712,hypothesis,
a_1749 = store(a_1748,i50,e50) ).
cnf(u7717,hypothesis,
a_1748 = store(a_1747,i49,e49) ).
cnf(u7722,hypothesis,
a_1747 = store(a_1746,i48,e48) ).
cnf(u7727,hypothesis,
a_1746 = store(a_1745,i47,e47) ).
cnf(u7732,hypothesis,
a_1745 = store(a_1744,i46,e46) ).
cnf(u7737,hypothesis,
a_1744 = store(a_1743,i45,e45) ).
cnf(u7742,hypothesis,
a_1743 = store(a_1742,i44,e44) ).
cnf(u7747,hypothesis,
a_1742 = store(a_1741,i43,e43) ).
cnf(u7752,hypothesis,
a_1741 = store(a_1740,i42,e42) ).
cnf(u7757,hypothesis,
a_1740 = store(a_1739,i41,e41) ).
cnf(u7762,hypothesis,
a_1739 = store(a_1738,i40,e40) ).
cnf(u7767,hypothesis,
a_1738 = store(a_1737,i39,e39) ).
cnf(u7772,hypothesis,
a_1737 = store(a_1736,i38,e38) ).
cnf(u7777,hypothesis,
a_1736 = store(a_1735,i37,e37) ).
cnf(u7782,hypothesis,
a_1735 = store(a_1734,i36,e36) ).
cnf(u7787,hypothesis,
a_1734 = store(a_1733,i35,e35) ).
cnf(u7792,hypothesis,
a_1733 = store(a_1732,i34,e34) ).
cnf(u7797,hypothesis,
a_1732 = store(a_1731,i33,e33) ).
cnf(u7802,hypothesis,
a_1731 = store(a_1730,i32,e32) ).
cnf(u7807,hypothesis,
a_1730 = store(a_1729,i31,e31) ).
cnf(u7812,hypothesis,
a_1729 = store(a_1728,i30,e30) ).
cnf(u7817,hypothesis,
a_1728 = store(a_1727,i29,e29) ).
cnf(u7822,hypothesis,
a_1727 = store(a_1726,i28,e28) ).
cnf(u7827,hypothesis,
a_1726 = store(a_1725,i27,e27) ).
cnf(u7832,hypothesis,
a_1725 = store(a_1724,i26,e26) ).
cnf(u7837,hypothesis,
a_1724 = store(a_1723,i25,e25) ).
cnf(u7842,hypothesis,
a_1723 = store(a_1722,i24,e24) ).
cnf(u7847,hypothesis,
a_1722 = store(a_1721,i23,e23) ).
cnf(u7852,hypothesis,
a_1721 = store(a_1720,i22,e22) ).
cnf(u7857,hypothesis,
a_1720 = store(a_1719,i21,e21) ).
cnf(u7862,hypothesis,
a_1719 = store(a_1718,i20,e20) ).
cnf(u7867,hypothesis,
a_1718 = store(a_1717,i19,e19) ).
cnf(u7872,hypothesis,
a_1717 = store(a_1716,i18,e18) ).
cnf(u7877,hypothesis,
a_1716 = store(a_1715,i17,e17) ).
cnf(u7882,hypothesis,
a_1715 = store(a_1714,i16,e16) ).
cnf(u7887,hypothesis,
a_1714 = store(a_1713,i15,e15) ).
cnf(u7892,hypothesis,
a_1713 = store(a_1712,i14,e14) ).
cnf(u7897,hypothesis,
a_1712 = store(a_1711,i13,e13) ).
cnf(u7902,hypothesis,
a_1711 = store(a_1710,i12,e12) ).
cnf(u7907,hypothesis,
a_1710 = store(a_1709,i11,e11) ).
cnf(u7912,hypothesis,
a_1709 = store(a_1708,i10,e10) ).
cnf(u7917,hypothesis,
a_1708 = store(a_1707,i9,e9) ).
cnf(u7922,hypothesis,
a_1707 = store(a_1706,i8,e8) ).
cnf(u7927,hypothesis,
a_1706 = store(a_1705,i7,e7) ).
cnf(u7932,hypothesis,
a_1705 = store(a_1704,i6,e6) ).
cnf(u7937,hypothesis,
a_1704 = store(a_1703,i5,e5) ).
cnf(u7942,hypothesis,
a_1703 = store(a_1702,i4,e4) ).
cnf(u7947,hypothesis,
a_1702 = store(a_1701,i3,e3) ).
cnf(u7952,hypothesis,
a_1701 = store(a_1700,i2,e2) ).
cnf(u7957,hypothesis,
a_1700 = store(a1,i1,e1) ).
cnf(u8062,hypothesis,
e1 = select(a_1799,i1) ).
cnf(u8067,hypothesis,
e31 = select(a_1798,i31) ).
cnf(u8072,hypothesis,
e21 = select(a_1797,i21) ).
cnf(u8077,hypothesis,
e24 = select(a_1796,i24) ).
cnf(u8082,hypothesis,
e4 = select(a_1795,i4) ).
cnf(u8087,hypothesis,
e32 = select(a_1794,i32) ).
cnf(u8092,hypothesis,
e5 = select(a_1793,i5) ).
cnf(u8097,hypothesis,
e12 = select(a_1792,i12) ).
cnf(u8102,hypothesis,
e37 = select(a_1791,i37) ).
cnf(u8107,hypothesis,
e3 = select(a_1790,i3) ).
cnf(u8112,hypothesis,
e29 = select(a_1789,i29) ).
cnf(u8117,hypothesis,
e48 = select(a_1788,i48) ).
cnf(u8122,hypothesis,
e10 = select(a_1787,i10) ).
cnf(u8127,hypothesis,
e2 = select(a_1786,i2) ).
cnf(u8132,hypothesis,
e50 = select(a_1785,i50) ).
cnf(u8137,hypothesis,
e35 = select(a_1784,i35) ).
cnf(u8142,hypothesis,
e46 = select(a_1783,i46) ).
cnf(u8147,hypothesis,
e25 = select(a_1782,i25) ).
cnf(u8152,hypothesis,
e23 = select(a_1781,i23) ).
cnf(u8157,hypothesis,
e38 = select(a_1780,i38) ).
cnf(u8162,hypothesis,
e44 = select(a_1779,i44) ).
cnf(u8167,hypothesis,
e36 = select(a_1778,i36) ).
cnf(u8172,hypothesis,
e11 = select(a_1777,i11) ).
cnf(u8177,hypothesis,
e34 = select(a_1776,i34) ).
cnf(u8182,hypothesis,
e26 = select(a_1775,i26) ).
cnf(u8187,hypothesis,
e18 = select(a_1774,i18) ).
cnf(u8192,hypothesis,
e47 = select(a_1773,i47) ).
cnf(u8197,hypothesis,
e42 = select(a_1772,i42) ).
cnf(u8202,hypothesis,
e17 = select(a_1771,i17) ).
cnf(u8207,hypothesis,
e9 = select(a_1770,i9) ).
cnf(u8212,hypothesis,
e33 = select(a_1769,i33) ).
cnf(u8217,hypothesis,
e7 = select(a_1768,i7) ).
cnf(u8222,hypothesis,
e15 = select(a_1767,i15) ).
cnf(u8227,hypothesis,
e27 = select(a_1766,i27) ).
cnf(u8232,hypothesis,
e6 = select(a_1765,i6) ).
cnf(u8237,hypothesis,
e13 = select(a_1764,i13) ).
cnf(u8242,hypothesis,
e14 = select(a_1763,i14) ).
cnf(u8247,hypothesis,
e49 = select(a_1762,i49) ).
cnf(u8252,hypothesis,
e8 = select(a_1761,i8) ).
cnf(u8257,hypothesis,
e16 = select(a_1760,i16) ).
cnf(u8262,hypothesis,
e40 = select(a_1759,i40) ).
cnf(u8267,hypothesis,
e20 = select(a_1758,i20) ).
cnf(u8272,hypothesis,
e39 = select(a_1757,i39) ).
cnf(u8277,hypothesis,
e22 = select(a_1756,i22) ).
cnf(u8282,hypothesis,
e19 = select(a_1755,i19) ).
cnf(u8287,hypothesis,
e28 = select(a_1754,i28) ).
cnf(u8292,hypothesis,
e43 = select(a_1753,i43) ).
cnf(u8297,hypothesis,
e45 = select(a_1752,i45) ).
cnf(u8302,hypothesis,
e30 = select(a_1751,i30) ).
cnf(u8307,hypothesis,
e50 = select(a_1749,i50) ).
cnf(u8312,hypothesis,
e49 = select(a_1748,i49) ).
cnf(u8317,hypothesis,
e48 = select(a_1747,i48) ).
cnf(u8322,hypothesis,
e47 = select(a_1746,i47) ).
cnf(u8327,hypothesis,
e46 = select(a_1745,i46) ).
cnf(u8332,hypothesis,
e45 = select(a_1744,i45) ).
cnf(u8337,hypothesis,
e44 = select(a_1743,i44) ).
cnf(u8342,hypothesis,
e43 = select(a_1742,i43) ).
cnf(u8347,hypothesis,
e42 = select(a_1741,i42) ).
cnf(u8352,hypothesis,
e41 = select(a_1740,i41) ).
cnf(u8357,hypothesis,
e40 = select(a_1739,i40) ).
cnf(u8362,hypothesis,
e39 = select(a_1738,i39) ).
cnf(u8367,hypothesis,
e38 = select(a_1737,i38) ).
cnf(u8372,hypothesis,
e37 = select(a_1736,i37) ).
cnf(u8377,hypothesis,
e36 = select(a_1735,i36) ).
cnf(u8382,hypothesis,
e35 = select(a_1734,i35) ).
cnf(u8387,hypothesis,
e34 = select(a_1733,i34) ).
cnf(u8392,hypothesis,
e33 = select(a_1732,i33) ).
cnf(u8397,hypothesis,
e32 = select(a_1731,i32) ).
cnf(u8402,hypothesis,
e31 = select(a_1730,i31) ).
cnf(u8407,hypothesis,
e30 = select(a_1729,i30) ).
cnf(u8412,hypothesis,
e29 = select(a_1728,i29) ).
cnf(u8417,hypothesis,
e28 = select(a_1727,i28) ).
cnf(u8422,hypothesis,
e27 = select(a_1726,i27) ).
cnf(u8427,hypothesis,
e26 = select(a_1725,i26) ).
cnf(u8432,hypothesis,
e25 = select(a_1724,i25) ).
cnf(u8437,hypothesis,
e24 = select(a_1723,i24) ).
cnf(u8442,hypothesis,
e23 = select(a_1722,i23) ).
cnf(u8447,hypothesis,
e22 = select(a_1721,i22) ).
cnf(u8452,hypothesis,
e21 = select(a_1720,i21) ).
cnf(u8457,hypothesis,
e20 = select(a_1719,i20) ).
cnf(u8462,hypothesis,
e19 = select(a_1718,i19) ).
cnf(u8467,hypothesis,
e18 = select(a_1717,i18) ).
cnf(u8472,hypothesis,
e17 = select(a_1716,i17) ).
cnf(u8477,hypothesis,
e16 = select(a_1715,i16) ).
cnf(u8482,hypothesis,
e15 = select(a_1714,i15) ).
cnf(u8487,hypothesis,
e14 = select(a_1713,i14) ).
cnf(u8492,hypothesis,
e13 = select(a_1712,i13) ).
cnf(u8497,hypothesis,
e12 = select(a_1711,i12) ).
cnf(u8502,hypothesis,
e11 = select(a_1710,i11) ).
cnf(u8507,hypothesis,
e10 = select(a_1709,i10) ).
cnf(u8512,hypothesis,
e9 = select(a_1708,i9) ).
cnf(u8517,hypothesis,
e8 = select(a_1707,i8) ).
cnf(u8522,hypothesis,
e7 = select(a_1706,i7) ).
cnf(u8527,hypothesis,
e6 = select(a_1705,i6) ).
cnf(u8532,hypothesis,
e5 = select(a_1704,i5) ).
cnf(u8537,hypothesis,
e4 = select(a_1703,i4) ).
cnf(u8542,hypothesis,
e3 = select(a_1702,i3) ).
cnf(u8547,hypothesis,
e1 = select(a_1700,i1) ).
cnf(u8552,hypothesis,
e41 = select(a_1750,i41) ).
cnf(u8557,hypothesis,
e2 = select(a_1701,i2) ).
cnf(u8606,hypothesis,
( select(a_1745,X0) = select(a_1746,X0)
| i47 = X0 ) ).
cnf(u8620,hypothesis,
( select(a_1760,X0) = select(a_1761,X0)
| i8 = X0 ) ).
cnf(u8598,hypothesis,
( select(a_1737,X0) = select(a_1738,X0)
| i39 = X0 ) ).
cnf(u8571,hypothesis,
( select(a_1710,X0) = select(a_1711,X0)
| i12 = X0 ) ).
cnf(u8594,hypothesis,
( select(a_1733,X0) = select(a_1734,X0)
| i35 = X0 ) ).
cnf(u8608,hypothesis,
( select(a_1747,X0) = select(a_1748,X0)
| i49 = X0 ) ).
cnf(u8579,hypothesis,
( select(a_1718,X0) = select(a_1719,X0)
| i20 = X0 ) ).
cnf(u8656,hypothesis,
( select(a_1796,X0) = select(a_1797,X0)
| i21 = X0 ) ).
cnf(u8580,hypothesis,
( select(a_1719,X0) = select(a_1720,X0)
| i21 = X0 ) ).
cnf(u8648,hypothesis,
( select(a_1788,X0) = select(a_1789,X0)
| i29 = X0 ) ).
cnf(u8655,hypothesis,
( select(a_1795,X0) = select(a_1796,X0)
| i24 = X0 ) ).
cnf(u8565,hypothesis,
( select(a_1704,X0) = select(a_1705,X0)
| i6 = X0 ) ).
cnf(u8602,hypothesis,
( select(a_1741,X0) = select(a_1742,X0)
| i43 = X0 ) ).
cnf(u8611,hypothesis,
( select(a_1751,X0) = select(a_1752,X0)
| i45 = X0 ) ).
cnf(u8625,hypothesis,
( select(a_1765,X0) = select(a_1766,X0)
| i27 = X0 ) ).
cnf(u8645,hypothesis,
( select(a_1785,X0) = select(a_1786,X0)
| i2 = X0 ) ).
cnf(u8576,hypothesis,
( select(a_1715,X0) = select(a_1716,X0)
| i17 = X0 ) ).
cnf(u8578,hypothesis,
( select(a_1717,X0) = select(a_1718,X0)
| i19 = X0 ) ).
cnf(u8641,hypothesis,
( select(a_1781,X0) = select(a_1782,X0)
| i25 = X0 ) ).
cnf(u8568,hypothesis,
( select(a_1707,X0) = select(a_1708,X0)
| i9 = X0 ) ).
cnf(u8560,hypothesis,
( select(a1,X0) = select(a_1750,X0)
| i41 = X0 ) ).
cnf(u8572,hypothesis,
( select(a_1711,X0) = select(a_1712,X0)
| i13 = X0 ) ).
cnf(u8637,hypothesis,
( select(a_1777,X0) = select(a_1778,X0)
| i36 = X0 ) ).
cnf(u8630,hypothesis,
( select(a_1770,X0) = select(a_1771,X0)
| i17 = X0 ) ).
cnf(u8633,hypothesis,
( select(a_1773,X0) = select(a_1774,X0)
| i18 = X0 ) ).
cnf(u8615,hypothesis,
( select(a_1755,X0) = select(a_1756,X0)
| i22 = X0 ) ).
cnf(u8652,hypothesis,
( select(a_1792,X0) = select(a_1793,X0)
| i5 = X0 ) ).
cnf(u8603,hypothesis,
( select(a_1742,X0) = select(a_1743,X0)
| i44 = X0 ) ).
cnf(u8577,hypothesis,
( select(a_1716,X0) = select(a_1717,X0)
| i18 = X0 ) ).
cnf(u8647,hypothesis,
( select(a_1787,X0) = select(a_1788,X0)
| i48 = X0 ) ).
cnf(u8623,hypothesis,
( select(a_1763,X0) = select(a_1764,X0)
| i13 = X0 ) ).
cnf(u8589,hypothesis,
( select(a_1728,X0) = select(a_1729,X0)
| i30 = X0 ) ).
cnf(u8622,hypothesis,
( select(a_1762,X0) = select(a_1763,X0)
| i14 = X0 ) ).
cnf(u8585,hypothesis,
( select(a_1724,X0) = select(a_1725,X0)
| i26 = X0 ) ).
cnf(u8626,hypothesis,
( select(a_1766,X0) = select(a_1767,X0)
| i15 = X0 ) ).
cnf(u8618,hypothesis,
( select(a_1758,X0) = select(a_1759,X0)
| i40 = X0 ) ).
cnf(u8604,hypothesis,
( select(a_1743,X0) = select(a_1744,X0)
| i45 = X0 ) ).
cnf(u8635,hypothesis,
( select(a_1775,X0) = select(a_1776,X0)
| i34 = X0 ) ).
cnf(u8586,hypothesis,
( select(a_1725,X0) = select(a_1726,X0)
| i27 = X0 ) ).
cnf(u8563,hypothesis,
( select(a_1702,X0) = select(a_1703,X0)
| i4 = X0 ) ).
cnf(u8657,hypothesis,
( select(a_1797,X0) = select(a_1798,X0)
| i31 = X0 ) ).
cnf(u8575,hypothesis,
( select(a_1714,X0) = select(a_1715,X0)
| i16 = X0 ) ).
cnf(u8600,hypothesis,
( select(a_1739,X0) = select(a_1740,X0)
| i41 = X0 ) ).
cnf(u8567,hypothesis,
( select(a_1706,X0) = select(a_1707,X0)
| i8 = X0 ) ).
cnf(u8612,hypothesis,
( select(a_1752,X0) = select(a_1753,X0)
| i43 = X0 ) ).
cnf(u8595,hypothesis,
( select(a_1734,X0) = select(a_1735,X0)
| i36 = X0 ) ).
cnf(u8590,hypothesis,
( select(a_1729,X0) = select(a_1730,X0)
| i31 = X0 ) ).
cnf(u8629,hypothesis,
( select(a_1769,X0) = select(a_1770,X0)
| i9 = X0 ) ).
cnf(a2,axiom,
( select(store(X2,X0,X3),X1) = select(X2,X1)
| X0 = X1 ) ).
cnf(u8582,hypothesis,
( select(a_1721,X0) = select(a_1722,X0)
| i23 = X0 ) ).
cnf(u8658,hypothesis,
( select(a_1798,X0) = select(a_1799,X0)
| i1 = X0 ) ).
cnf(u8574,hypothesis,
( select(a_1713,X0) = select(a_1714,X0)
| i15 = X0 ) ).
cnf(u8643,hypothesis,
( select(a_1783,X0) = select(a_1784,X0)
| i35 = X0 ) ).
cnf(u8570,hypothesis,
( select(a_1709,X0) = select(a_1710,X0)
| i11 = X0 ) ).
cnf(u8613,hypothesis,
( select(a_1753,X0) = select(a_1754,X0)
| i28 = X0 ) ).
cnf(u8617,hypothesis,
( select(a_1757,X0) = select(a_1758,X0)
| i20 = X0 ) ).
cnf(u8609,hypothesis,
( select(a_1748,X0) = select(a_1749,X0)
| i50 = X0 ) ).
cnf(u8621,hypothesis,
( select(a_1761,X0) = select(a_1762,X0)
| i49 = X0 ) ).
cnf(u8587,hypothesis,
( select(a_1726,X0) = select(a_1727,X0)
| i28 = X0 ) ).
cnf(u8614,hypothesis,
( select(a_1754,X0) = select(a_1755,X0)
| i19 = X0 ) ).
cnf(u8564,hypothesis,
( select(a_1703,X0) = select(a_1704,X0)
| i5 = X0 ) ).
cnf(u8599,hypothesis,
( select(a_1738,X0) = select(a_1739,X0)
| i40 = X0 ) ).
cnf(u8591,hypothesis,
( select(a_1730,X0) = select(a_1731,X0)
| i32 = X0 ) ).
cnf(u8644,hypothesis,
( select(a_1784,X0) = select(a_1785,X0)
| i50 = X0 ) ).
cnf(u8640,hypothesis,
( select(a_1780,X0) = select(a_1781,X0)
| i23 = X0 ) ).
cnf(u8653,hypothesis,
( select(a_1793,X0) = select(a_1794,X0)
| i32 = X0 ) ).
cnf(u8632,hypothesis,
( select(a_1772,X0) = select(a_1773,X0)
| i47 = X0 ) ).
cnf(u8624,hypothesis,
( select(a_1764,X0) = select(a_1765,X0)
| i6 = X0 ) ).
cnf(u8569,hypothesis,
( select(a_1708,X0) = select(a_1709,X0)
| i10 = X0 ) ).
cnf(u8636,hypothesis,
( select(a_1776,X0) = select(a_1777,X0)
| i11 = X0 ) ).
cnf(u8561,hypothesis,
( select(a_1700,X0) = select(a1,X0)
| i1 = X0 ) ).
cnf(u8581,hypothesis,
( select(a_1720,X0) = select(a_1721,X0)
| i22 = X0 ) ).
cnf(u8631,hypothesis,
( select(a_1771,X0) = select(a_1772,X0)
| i42 = X0 ) ).
cnf(u8649,hypothesis,
( select(a_1789,X0) = select(a_1790,X0)
| i3 = X0 ) ).
cnf(u8605,hypothesis,
( select(a_1744,X0) = select(a_1745,X0)
| i46 = X0 ) ).
cnf(u8654,hypothesis,
( select(a_1794,X0) = select(a_1795,X0)
| i4 = X0 ) ).
cnf(u8646,hypothesis,
( select(a_1786,X0) = select(a_1787,X0)
| i10 = X0 ) ).
cnf(u8573,hypothesis,
( select(a_1712,X0) = select(a_1713,X0)
| i14 = X0 ) ).
cnf(u8610,hypothesis,
( select(a_1750,X0) = select(a_1751,X0)
| i30 = X0 ) ).
cnf(u8596,hypothesis,
( select(a_1735,X0) = select(a_1736,X0)
| i37 = X0 ) ).
cnf(u8627,hypothesis,
( select(a_1767,X0) = select(a_1768,X0)
| i7 = X0 ) ).
cnf(u8588,hypothesis,
( select(a_1727,X0) = select(a_1728,X0)
| i29 = X0 ) ).
cnf(u8592,hypothesis,
( select(a_1731,X0) = select(a_1732,X0)
| i33 = X0 ) ).
cnf(u8559,hypothesis,
( select(a_1700,X0) = select(a_1701,X0)
| i2 = X0 ) ).
cnf(u8584,hypothesis,
( select(a_1723,X0) = select(a_1724,X0)
| i25 = X0 ) ).
cnf(a1,axiom,
select(store(X0,X1,X2),X1) = X2 ).
cnf(u8607,hypothesis,
( select(a_1746,X0) = select(a_1747,X0)
| i48 = X0 ) ).
cnf(u8650,hypothesis,
( select(a_1790,X0) = select(a_1791,X0)
| i37 = X0 ) ).
cnf(u8566,hypothesis,
( select(a_1705,X0) = select(a_1706,X0)
| i7 = X0 ) ).
cnf(u8562,hypothesis,
( select(a_1701,X0) = select(a_1702,X0)
| i3 = X0 ) ).
cnf(u8619,hypothesis,
( select(a_1759,X0) = select(a_1760,X0)
| i16 = X0 ) ).
cnf(u8639,hypothesis,
( select(a_1779,X0) = select(a_1780,X0)
| i38 = X0 ) ).
cnf(u8616,hypothesis,
( select(a_1756,X0) = select(a_1757,X0)
| i39 = X0 ) ).
cnf(u8583,hypothesis,
( select(a_1722,X0) = select(a_1723,X0)
| i24 = X0 ) ).
cnf(u8597,hypothesis,
( select(a_1736,X0) = select(a_1737,X0)
| i38 = X0 ) ).
cnf(u8642,hypothesis,
( select(a_1782,X0) = select(a_1783,X0)
| i46 = X0 ) ).
cnf(u8601,hypothesis,
( select(a_1740,X0) = select(a_1741,X0)
| i42 = X0 ) ).
cnf(u8593,hypothesis,
( select(a_1732,X0) = select(a_1733,X0)
| i34 = X0 ) ).
cnf(u8651,hypothesis,
( select(a_1791,X0) = select(a_1792,X0)
| i12 = X0 ) ).
cnf(u8638,hypothesis,
( select(a_1778,X0) = select(a_1779,X0)
| i44 = X0 ) ).
cnf(u8628,hypothesis,
( select(a_1768,X0) = select(a_1769,X0)
| i33 = X0 ) ).
cnf(u8634,hypothesis,
( select(a_1774,X0) = select(a_1775,X0)
| i26 = X0 ) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWV497-1.050 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.09/0.19 % Computer : n002.cluster.edu
% 0.09/0.19 % Model : x86_64 x86_64
% 0.09/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.19 % Memory : 8046.5625MB
% 0.09/0.19 % OS : Linux 6.8.0-71-generic
% 0.09/0.19 % CPULimit : 300
% 0.09/0.19 % WCLimit : 300
% 0.09/0.19 % DateTime : Mon Sep 28 11:19:13 UTC 2026
% 0.09/0.19 % CPUTime :
% 0.09/0.19 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.09/0.22 Running first-order theorem proving
% 0.09/0.22 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 6.72/1.52 % (293226)Input is clausal, will run a generic CNF schedule.
% 6.72/1.52 % (293237)dis-21_1_sil=8000:lcm=predicate:random_seed=3317785861: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)
% 6.72/1.52 % (293237)Refutation not found, incomplete strategy
% 6.72/1.52 % (293237)------------------------------
% 6.72/1.52 % (293237)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.72/1.52 % (293237)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.72/1.52 % (293237)CaDiCaL version: 2.1.3
% 6.72/1.52 % (293237)Termination reason: Refutation not found, incomplete strategy
% 6.72/1.52 % (293237)Time elapsed: 0.018 s
% 6.72/1.52 % (293237)Peak memory usage: 89 MB
% 6.72/1.52 % (293237)Instructions burned: 65 (million)
% 6.72/1.52 % (293234)lrs+10_1_sil=8000:sp=occurrence:random_seed=3547211049:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 6.72/1.52 % (293232)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=333672483:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 6.72/1.52 % (293233)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=24597678:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 6.72/1.52 % (293235)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=2035325328:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 6.72/1.52 % (293231)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=3474270137:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 6.72/1.52 % (293236)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=350803113:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 6.72/1.52 % (293234)Refutation not found, incomplete strategy
% 6.72/1.52 % (293234)------------------------------
% 6.72/1.52 % (293234)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.72/1.52 % (293234)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.72/1.52 % (293234)CaDiCaL version: 2.1.3
% 6.72/1.52 % (293234)Termination reason: Refutation not found, incomplete strategy
% 6.72/1.52 % (293234)Time elapsed: 0.019 s
% 6.72/1.52 % (293234)Peak memory usage: 88 MB
% 6.72/1.52 % (293234)Instructions burned: 42 (million)
% 6.72/1.52 % (293236)Refutation not found, incomplete strategy
% 6.72/1.52 % (293236)------------------------------
% 6.72/1.52 % (293236)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.72/1.52 % (293236)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.72/1.52 % (293236)CaDiCaL version: 2.1.3
% 6.72/1.52 % (293236)Termination reason: Refutation not found, incomplete strategy
% 6.72/1.52 % (293236)Time elapsed: 0.042 s
% 6.72/1.52 % (293236)Peak memory usage: 89 MB
% 6.72/1.52 % (293236)Instructions burned: 84 (million)
% 6.72/1.52 % (293235)Refutation not found, incomplete strategy
% 6.72/1.52 % (293235)------------------------------
% 6.72/1.52 % (293235)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.72/1.52 % (293235)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.72/1.52 % (293235)CaDiCaL version: 2.1.3
% 6.72/1.52 % (293235)Termination reason: Refutation not found, incomplete strategy
% 6.72/1.52 % (293235)Time elapsed: 0.052 s
% 6.72/1.52 % (293235)Peak memory usage: 89 MB
% 6.72/1.52 % (293235)Instructions burned: 109 (million)
% 6.72/1.52 % (293237)------------------------------
% 6.72/1.52 % (293237)------------------------------
% 6.72/1.52 % (293245)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=542759227:i=143:sd=2:aac=none:ss=axioms:sgt=16_2997 on theBenchmark for (2997ds/143Mi)
% 6.72/1.52 % (293245)Refutation not found, incomplete strategy
% 6.72/1.52 % (293245)------------------------------
% 6.72/1.52 % (293245)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.72/1.52 % (293245)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.72/1.52 % (293245)CaDiCaL version: 2.1.3
% 6.72/1.52 % (293245)Termination reason: Refutation not found, incomplete strategy
% 6.72/1.52 % (293245)Time elapsed: 0.014 s
% 6.72/1.52 % (293245)Peak memory usage: 88 MB
% 6.72/1.52 % (293245)Instructions burned: 51 (million)
% 6.72/1.52 % (293234)------------------------------
% 6.72/1.52 % (293234)------------------------------
% 6.72/1.52 % (293236)------------------------------
% 6.72/1.52 % (293236)------------------------------
% 6.72/1.52 % (293235)------------------------------
% 6.72/1.52 % (293235)------------------------------
% 6.72/1.52 % (293245)------------------------------
% 6.72/1.52 % (293245)------------------------------
% 6.72/1.52 % (293247)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=2721981022:st=3:avsq=on:s2a=on:i=189:s2at=1.2:avsqr=1,16:sd=2:bd=all:nm=64:ss=axioms:sgt=30_2995 on theBenchmark for (2995ds/189Mi)
% 6.72/1.52 % (293248)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=3354766879:st=4:i=219:sd=3:ss=axioms_2995 on theBenchmark for (2995ds/219Mi)
% 6.72/1.52 % (293249)lrs+10_64_to=lpo:sil=8000:random_seed=525055359:i=126:bd=preordered_2995 on theBenchmark for (2995ds/126Mi)
% 6.72/1.52 % (293248)Refutation not found, incomplete strategy
% 6.72/1.52 % (293248)------------------------------
% 6.72/1.52 % (293248)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.72/1.52 % (293248)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.72/1.52 % (293248)CaDiCaL version: 2.1.3
% 6.72/1.52 % (293248)Termination reason: Refutation not found, incomplete strategy
% 6.72/1.52 % (293248)Time elapsed: 0.024 s
% 6.72/1.52 % (293248)Peak memory usage: 89 MB
% 6.72/1.52 % (293248)Instructions burned: 53 (million)
% 6.72/1.52 % (293247)Refutation not found, incomplete strategy
% 6.72/1.52 % (293247)------------------------------
% 6.72/1.52 % (293247)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.72/1.52 % (293247)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.72/1.52 % (293247)CaDiCaL version: 2.1.3
% 6.72/1.52 % (293247)Termination reason: Refutation not found, incomplete strategy
% 6.72/1.52 % (293247)Time elapsed: 0.063 s
% 6.72/1.52 % (293247)Peak memory usage: 90 MB
% 6.72/1.52 % (293247)Instructions burned: 135 (million)
% 6.72/1.52 % (293249)Instruction limit reached!
% 6.72/1.52 % (293249)------------------------------
% 6.72/1.52 % (293249)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.72/1.52 % (293249)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.72/1.52 % (293249)CaDiCaL version: 2.1.3
% 6.72/1.52 % (293249)Termination reason: Instruction limit
% 6.72/1.52 % (293249)Termination phase: Saturation
% 6.72/1.52 % (293249)Time elapsed: 0.058 s
% 6.72/1.52 % (293249)Peak memory usage: 89 MB
% 6.72/1.52 % (293249)Instructions burned: 128 (million)
% 6.72/1.52 % (293251)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=898722686:avsq=on:i=194:fgj=on:bd=preordered_2994 on theBenchmark for (2994ds/194Mi)
% 6.72/1.52 % (293251)Refutation not found, incomplete strategy
% 6.72/1.52 % (293251)------------------------------
% 6.72/1.52 % (293251)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.72/1.52 % (293251)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.72/1.52 % (293251)CaDiCaL version: 2.1.3
% 6.72/1.52 % (293251)Termination reason: Refutation not found, incomplete strategy
% 6.72/1.52 % (293251)Time elapsed: 0.020 s
% 6.72/1.52 % (293251)Peak memory usage: 89 MB
% 6.72/1.52 % (293251)Instructions burned: 75 (million)
% 6.72/1.52 % (293254)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=1942547187:i=157:gtg=all_2993 on theBenchmark for (2993ds/157Mi)
% 6.72/1.52 % (293251)------------------------------
% 6.72/1.52 % (293251)------------------------------
% 6.72/1.52 % (293248)------------------------------
% 6.72/1.52 % (293248)------------------------------
% 6.72/1.52 % (293254)First to succeed.
% 6.72/1.52 % (293254)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-293226"
% 6.72/1.52 % (293247)------------------------------
% 6.72/1.52 % (293247)------------------------------
% 6.72/1.52 % (293257)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=344039305:i=3394:sd=4:ss=included:sgt=64_2991 on theBenchmark for (2991ds/3394Mi)
% 6.72/1.52 % (293258)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=2467077426:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2991 on theBenchmark for (2991ds/106Mi)
% 6.72/1.52 % (293231)Refutation not found, incomplete strategy
% 6.72/1.52 % (293231)------------------------------
% 6.72/1.52 % (293231)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.72/1.52 % (293231)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.72/1.52 % (293231)CaDiCaL version: 2.1.3
% 6.72/1.52 % (293231)Termination reason: Refutation not found, incomplete strategy
% 6.72/1.52 % (293231)Time elapsed: 0.845 s
% 6.72/1.52 % (293231)Peak memory usage: 139 MB
% 6.72/1.52 % (293231)Instructions burned: 1303 (million)
% 6.72/1.52 % (293259)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=102466297:i=107_2991 on theBenchmark for (2991ds/107Mi)
% 6.72/1.52 % (293233)Refutation not found, incomplete strategy
% 6.72/1.52 % (293233)------------------------------
% 6.72/1.52 % (293233)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.72/1.52 % (293233)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.72/1.52 % (293233)CaDiCaL version: 2.1.3
% 6.72/1.52 % (293233)Termination reason: Refutation not found, incomplete strategy
% 6.72/1.52 % (293233)Time elapsed: 0.852 s
% 6.72/1.52 % (293233)Peak memory usage: 138 MB
% 6.72/1.52 % (293233)Instructions burned: 1322 (million)
% 6.72/1.52 % (293258)Refutation not found, incomplete strategy
% 6.72/1.52 % (293258)------------------------------
% 6.72/1.52 % (293258)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.72/1.52 % (293258)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.72/1.52 % (293258)CaDiCaL version: 2.1.3
% 6.72/1.52 % (293258)Termination reason: Refutation not found, incomplete strategy
% 6.72/1.52 % (293258)Time elapsed: 0.034 s
% 6.72/1.52 % (293258)Peak memory usage: 89 MB
% 6.72/1.52 % (293258)Instructions burned: 70 (million)
% 6.72/1.52 % (293259)Refutation not found, incomplete strategy
% 6.72/1.52 % (293259)------------------------------
% 6.72/1.52 % (293259)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.72/1.52 % (293259)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.72/1.52 % (293259)CaDiCaL version: 2.1.3
% 6.72/1.52 % (293259)Termination reason: Refutation not found, incomplete strategy
% 6.72/1.52 % (293259)Time elapsed: 0.032 s
% 6.72/1.52 % (293259)Peak memory usage: 89 MB
% 6.72/1.52 % (293259)Instructions burned: 64 (million)
% 6.72/1.52 % SZS status Satisfiable for theBenchmark
% 6.72/1.52 % SZS output start Saturation.
% See solution above
% 8.09/1.62 % SZS output start Definitions and Model Updates.
% 8.09/1.62 % SZS output end Definitions and Model Updates.
% 8.09/1.62 % (293254)------------------------------
% 8.09/1.62 % (293254)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.09/1.62 % (293254)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.09/1.62 % (293254)CaDiCaL version: 2.1.3
% 8.09/1.62 % (293254)Termination reason: Satisfiable
% 8.09/1.62 % (293254)Time elapsed: 0.059 s
% 8.09/1.62 % (293254)Peak memory usage: 92 MB
% 8.09/1.62 % (293254)Instructions burned: 104 (million)
% 8.09/1.62 % (293254)------------------------------
% 8.09/1.62 % (293254)------------------------------
% 8.09/1.62 % (293226)Success in time 1.105 s
% 8.09/1.62 % Vampire exiting
%------------------------------------------------------------------------------