%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SWV497-1.040 : 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 : n011.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.45s 1.76s
% Output : Saturation 8.31s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(u867,negated_conjecture,
a_1398 != a_1438 ).
cnf(u872,hypothesis,
i1 != i2 ).
cnf(u877,hypothesis,
i1 != i3 ).
cnf(u882,hypothesis,
i1 != i4 ).
cnf(u887,hypothesis,
i1 != i5 ).
cnf(u892,hypothesis,
i1 != i6 ).
cnf(u897,hypothesis,
i1 != i7 ).
cnf(u902,hypothesis,
i1 != i8 ).
cnf(u907,hypothesis,
i1 != i9 ).
cnf(u912,hypothesis,
i1 != i10 ).
cnf(u917,hypothesis,
i1 != i11 ).
cnf(u922,hypothesis,
i1 != i12 ).
cnf(u927,hypothesis,
i1 != i13 ).
cnf(u932,hypothesis,
i1 != i14 ).
cnf(u937,hypothesis,
i1 != i15 ).
cnf(u942,hypothesis,
i1 != i16 ).
cnf(u947,hypothesis,
i1 != i17 ).
cnf(u952,hypothesis,
i1 != i18 ).
cnf(u957,hypothesis,
i1 != i19 ).
cnf(u962,hypothesis,
i1 != i20 ).
cnf(u967,hypothesis,
i1 != i21 ).
cnf(u972,hypothesis,
i1 != i22 ).
cnf(u977,hypothesis,
i1 != i23 ).
cnf(u982,hypothesis,
i1 != i24 ).
cnf(u987,hypothesis,
i1 != i25 ).
cnf(u992,hypothesis,
i1 != i26 ).
cnf(u997,hypothesis,
i1 != i27 ).
cnf(u1002,hypothesis,
i1 != i28 ).
cnf(u1007,hypothesis,
i1 != i29 ).
cnf(u1012,hypothesis,
i1 != i30 ).
cnf(u1017,hypothesis,
i1 != i31 ).
cnf(u1022,hypothesis,
i1 != i32 ).
cnf(u1027,hypothesis,
i1 != i33 ).
cnf(u1032,hypothesis,
i1 != i34 ).
cnf(u1037,hypothesis,
i1 != i35 ).
cnf(u1042,hypothesis,
i1 != i36 ).
cnf(u1047,hypothesis,
i1 != i37 ).
cnf(u1052,hypothesis,
i1 != i38 ).
cnf(u1057,hypothesis,
i1 != i39 ).
cnf(u1062,hypothesis,
i1 != i40 ).
cnf(u1067,hypothesis,
i2 != i3 ).
cnf(u1072,hypothesis,
i2 != i4 ).
cnf(u1077,hypothesis,
i2 != i5 ).
cnf(u1082,hypothesis,
i2 != i6 ).
cnf(u1087,hypothesis,
i2 != i7 ).
cnf(u1092,hypothesis,
i2 != i8 ).
cnf(u1097,hypothesis,
i2 != i9 ).
cnf(u1102,hypothesis,
i2 != i10 ).
cnf(u1107,hypothesis,
i2 != i11 ).
cnf(u1112,hypothesis,
i2 != i12 ).
cnf(u1117,hypothesis,
i2 != i13 ).
cnf(u1122,hypothesis,
i2 != i14 ).
cnf(u1127,hypothesis,
i2 != i15 ).
cnf(u1132,hypothesis,
i2 != i16 ).
cnf(u1137,hypothesis,
i2 != i17 ).
cnf(u1142,hypothesis,
i2 != i18 ).
cnf(u1147,hypothesis,
i2 != i19 ).
cnf(u1152,hypothesis,
i2 != i20 ).
cnf(u1157,hypothesis,
i2 != i21 ).
cnf(u1162,hypothesis,
i2 != i22 ).
cnf(u1167,hypothesis,
i2 != i23 ).
cnf(u1172,hypothesis,
i2 != i24 ).
cnf(u1177,hypothesis,
i2 != i25 ).
cnf(u1182,hypothesis,
i2 != i26 ).
cnf(u1187,hypothesis,
i2 != i27 ).
cnf(u1192,hypothesis,
i2 != i28 ).
cnf(u1197,hypothesis,
i2 != i29 ).
cnf(u1202,hypothesis,
i2 != i30 ).
cnf(u1207,hypothesis,
i2 != i31 ).
cnf(u1212,hypothesis,
i2 != i32 ).
cnf(u1217,hypothesis,
i2 != i33 ).
cnf(u1222,hypothesis,
i2 != i34 ).
cnf(u1227,hypothesis,
i2 != i35 ).
cnf(u1232,hypothesis,
i2 != i36 ).
cnf(u1237,hypothesis,
i2 != i37 ).
cnf(u1242,hypothesis,
i2 != i38 ).
cnf(u1247,hypothesis,
i2 != i39 ).
cnf(u1252,hypothesis,
i2 != i40 ).
cnf(u1257,hypothesis,
i3 != i4 ).
cnf(u1262,hypothesis,
i3 != i5 ).
cnf(u1267,hypothesis,
i3 != i6 ).
cnf(u1272,hypothesis,
i3 != i7 ).
cnf(u1277,hypothesis,
i3 != i8 ).
cnf(u1282,hypothesis,
i3 != i9 ).
cnf(u1287,hypothesis,
i3 != i10 ).
cnf(u1292,hypothesis,
i3 != i11 ).
cnf(u1297,hypothesis,
i3 != i12 ).
cnf(u1302,hypothesis,
i3 != i13 ).
cnf(u1307,hypothesis,
i3 != i14 ).
cnf(u1312,hypothesis,
i3 != i15 ).
cnf(u1317,hypothesis,
i3 != i16 ).
cnf(u1322,hypothesis,
i3 != i17 ).
cnf(u1327,hypothesis,
i3 != i18 ).
cnf(u1332,hypothesis,
i3 != i19 ).
cnf(u1337,hypothesis,
i3 != i20 ).
cnf(u1342,hypothesis,
i3 != i21 ).
cnf(u1347,hypothesis,
i3 != i22 ).
cnf(u1352,hypothesis,
i3 != i23 ).
cnf(u1357,hypothesis,
i3 != i24 ).
cnf(u1362,hypothesis,
i3 != i25 ).
cnf(u1367,hypothesis,
i3 != i26 ).
cnf(u1372,hypothesis,
i3 != i27 ).
cnf(u1377,hypothesis,
i3 != i28 ).
cnf(u1382,hypothesis,
i3 != i29 ).
cnf(u1387,hypothesis,
i3 != i30 ).
cnf(u1392,hypothesis,
i3 != i31 ).
cnf(u1397,hypothesis,
i3 != i32 ).
cnf(u1402,hypothesis,
i3 != i33 ).
cnf(u1407,hypothesis,
i3 != i34 ).
cnf(u1412,hypothesis,
i3 != i35 ).
cnf(u1417,hypothesis,
i3 != i36 ).
cnf(u1422,hypothesis,
i3 != i37 ).
cnf(u1427,hypothesis,
i3 != i38 ).
cnf(u1432,hypothesis,
i3 != i39 ).
cnf(u1437,hypothesis,
i3 != i40 ).
cnf(u1442,hypothesis,
i4 != i5 ).
cnf(u1447,hypothesis,
i4 != i6 ).
cnf(u1452,hypothesis,
i4 != i7 ).
cnf(u1457,hypothesis,
i4 != i8 ).
cnf(u1462,hypothesis,
i4 != i9 ).
cnf(u1467,hypothesis,
i4 != i10 ).
cnf(u1472,hypothesis,
i4 != i11 ).
cnf(u1477,hypothesis,
i4 != i12 ).
cnf(u1482,hypothesis,
i4 != i13 ).
cnf(u1487,hypothesis,
i4 != i14 ).
cnf(u1492,hypothesis,
i4 != i15 ).
cnf(u1497,hypothesis,
i4 != i16 ).
cnf(u1502,hypothesis,
i4 != i17 ).
cnf(u1507,hypothesis,
i4 != i18 ).
cnf(u1512,hypothesis,
i4 != i19 ).
cnf(u1517,hypothesis,
i4 != i20 ).
cnf(u1522,hypothesis,
i4 != i21 ).
cnf(u1527,hypothesis,
i4 != i22 ).
cnf(u1532,hypothesis,
i4 != i23 ).
cnf(u1537,hypothesis,
i4 != i24 ).
cnf(u1542,hypothesis,
i4 != i25 ).
cnf(u1547,hypothesis,
i4 != i26 ).
cnf(u1552,hypothesis,
i4 != i27 ).
cnf(u1557,hypothesis,
i4 != i28 ).
cnf(u1562,hypothesis,
i4 != i29 ).
cnf(u1567,hypothesis,
i4 != i30 ).
cnf(u1572,hypothesis,
i4 != i31 ).
cnf(u1577,hypothesis,
i4 != i32 ).
cnf(u1582,hypothesis,
i4 != i33 ).
cnf(u1587,hypothesis,
i4 != i34 ).
cnf(u1592,hypothesis,
i4 != i35 ).
cnf(u1597,hypothesis,
i4 != i36 ).
cnf(u1602,hypothesis,
i4 != i37 ).
cnf(u1607,hypothesis,
i4 != i38 ).
cnf(u1612,hypothesis,
i4 != i39 ).
cnf(u1617,hypothesis,
i4 != i40 ).
cnf(u1622,hypothesis,
i5 != i6 ).
cnf(u1627,hypothesis,
i5 != i7 ).
cnf(u1632,hypothesis,
i5 != i8 ).
cnf(u1637,hypothesis,
i5 != i9 ).
cnf(u1642,hypothesis,
i5 != i10 ).
cnf(u1647,hypothesis,
i5 != i11 ).
cnf(u1652,hypothesis,
i5 != i12 ).
cnf(u1657,hypothesis,
i5 != i13 ).
cnf(u1662,hypothesis,
i5 != i14 ).
cnf(u1667,hypothesis,
i5 != i15 ).
cnf(u1672,hypothesis,
i5 != i16 ).
cnf(u1677,hypothesis,
i5 != i17 ).
cnf(u1682,hypothesis,
i5 != i18 ).
cnf(u1687,hypothesis,
i5 != i19 ).
cnf(u1692,hypothesis,
i5 != i20 ).
cnf(u1697,hypothesis,
i5 != i21 ).
cnf(u1702,hypothesis,
i5 != i22 ).
cnf(u1707,hypothesis,
i5 != i23 ).
cnf(u1712,hypothesis,
i5 != i24 ).
cnf(u1717,hypothesis,
i5 != i25 ).
cnf(u1722,hypothesis,
i5 != i26 ).
cnf(u1727,hypothesis,
i5 != i27 ).
cnf(u1732,hypothesis,
i5 != i28 ).
cnf(u1737,hypothesis,
i5 != i29 ).
cnf(u1742,hypothesis,
i5 != i30 ).
cnf(u1747,hypothesis,
i5 != i31 ).
cnf(u1752,hypothesis,
i5 != i32 ).
cnf(u1757,hypothesis,
i5 != i33 ).
cnf(u1762,hypothesis,
i5 != i34 ).
cnf(u1767,hypothesis,
i5 != i35 ).
cnf(u1772,hypothesis,
i5 != i36 ).
cnf(u1777,hypothesis,
i5 != i37 ).
cnf(u1782,hypothesis,
i5 != i38 ).
cnf(u1787,hypothesis,
i5 != i39 ).
cnf(u1792,hypothesis,
i5 != i40 ).
cnf(u1797,hypothesis,
i6 != i7 ).
cnf(u1802,hypothesis,
i6 != i8 ).
cnf(u1807,hypothesis,
i6 != i9 ).
cnf(u1812,hypothesis,
i6 != i10 ).
cnf(u1817,hypothesis,
i6 != i11 ).
cnf(u1822,hypothesis,
i6 != i12 ).
cnf(u1827,hypothesis,
i6 != i13 ).
cnf(u1832,hypothesis,
i6 != i14 ).
cnf(u1837,hypothesis,
i6 != i15 ).
cnf(u1842,hypothesis,
i6 != i16 ).
cnf(u1847,hypothesis,
i6 != i17 ).
cnf(u1852,hypothesis,
i6 != i18 ).
cnf(u1857,hypothesis,
i6 != i19 ).
cnf(u1862,hypothesis,
i6 != i20 ).
cnf(u1867,hypothesis,
i6 != i21 ).
cnf(u1872,hypothesis,
i6 != i22 ).
cnf(u1877,hypothesis,
i6 != i23 ).
cnf(u1882,hypothesis,
i6 != i24 ).
cnf(u1887,hypothesis,
i6 != i25 ).
cnf(u1892,hypothesis,
i6 != i26 ).
cnf(u1897,hypothesis,
i6 != i27 ).
cnf(u1902,hypothesis,
i6 != i28 ).
cnf(u1907,hypothesis,
i6 != i29 ).
cnf(u1912,hypothesis,
i6 != i30 ).
cnf(u1917,hypothesis,
i6 != i31 ).
cnf(u1922,hypothesis,
i6 != i32 ).
cnf(u1927,hypothesis,
i6 != i33 ).
cnf(u1932,hypothesis,
i6 != i34 ).
cnf(u1937,hypothesis,
i6 != i35 ).
cnf(u1942,hypothesis,
i6 != i36 ).
cnf(u1947,hypothesis,
i6 != i37 ).
cnf(u1952,hypothesis,
i6 != i38 ).
cnf(u1957,hypothesis,
i6 != i39 ).
cnf(u1962,hypothesis,
i6 != i40 ).
cnf(u1967,hypothesis,
i7 != i8 ).
cnf(u1972,hypothesis,
i7 != i9 ).
cnf(u1977,hypothesis,
i7 != i10 ).
cnf(u1982,hypothesis,
i7 != i11 ).
cnf(u1987,hypothesis,
i7 != i12 ).
cnf(u1992,hypothesis,
i7 != i13 ).
cnf(u1997,hypothesis,
i7 != i14 ).
cnf(u2002,hypothesis,
i7 != i15 ).
cnf(u2007,hypothesis,
i7 != i16 ).
cnf(u2012,hypothesis,
i7 != i17 ).
cnf(u2017,hypothesis,
i7 != i18 ).
cnf(u2022,hypothesis,
i7 != i19 ).
cnf(u2027,hypothesis,
i7 != i20 ).
cnf(u2032,hypothesis,
i7 != i21 ).
cnf(u2037,hypothesis,
i7 != i22 ).
cnf(u2042,hypothesis,
i7 != i23 ).
cnf(u2047,hypothesis,
i7 != i24 ).
cnf(u2052,hypothesis,
i7 != i25 ).
cnf(u2057,hypothesis,
i7 != i26 ).
cnf(u2062,hypothesis,
i7 != i27 ).
cnf(u2067,hypothesis,
i7 != i28 ).
cnf(u2072,hypothesis,
i7 != i29 ).
cnf(u2077,hypothesis,
i7 != i30 ).
cnf(u2082,hypothesis,
i7 != i31 ).
cnf(u2087,hypothesis,
i7 != i32 ).
cnf(u2092,hypothesis,
i7 != i33 ).
cnf(u2097,hypothesis,
i7 != i34 ).
cnf(u2102,hypothesis,
i7 != i35 ).
cnf(u2107,hypothesis,
i7 != i36 ).
cnf(u2112,hypothesis,
i7 != i37 ).
cnf(u2117,hypothesis,
i7 != i38 ).
cnf(u2122,hypothesis,
i7 != i39 ).
cnf(u2127,hypothesis,
i7 != i40 ).
cnf(u2132,hypothesis,
i8 != i9 ).
cnf(u2137,hypothesis,
i8 != i10 ).
cnf(u2142,hypothesis,
i8 != i11 ).
cnf(u2147,hypothesis,
i8 != i12 ).
cnf(u2152,hypothesis,
i8 != i13 ).
cnf(u2157,hypothesis,
i8 != i14 ).
cnf(u2162,hypothesis,
i8 != i15 ).
cnf(u2167,hypothesis,
i8 != i16 ).
cnf(u2172,hypothesis,
i8 != i17 ).
cnf(u2177,hypothesis,
i8 != i18 ).
cnf(u2182,hypothesis,
i8 != i19 ).
cnf(u2187,hypothesis,
i8 != i20 ).
cnf(u2192,hypothesis,
i8 != i21 ).
cnf(u2197,hypothesis,
i8 != i22 ).
cnf(u2202,hypothesis,
i8 != i23 ).
cnf(u2207,hypothesis,
i8 != i24 ).
cnf(u2212,hypothesis,
i8 != i25 ).
cnf(u2217,hypothesis,
i8 != i26 ).
cnf(u2222,hypothesis,
i8 != i27 ).
cnf(u2227,hypothesis,
i8 != i28 ).
cnf(u2232,hypothesis,
i8 != i29 ).
cnf(u2237,hypothesis,
i8 != i30 ).
cnf(u2242,hypothesis,
i8 != i31 ).
cnf(u2247,hypothesis,
i8 != i32 ).
cnf(u2252,hypothesis,
i8 != i33 ).
cnf(u2257,hypothesis,
i8 != i34 ).
cnf(u2262,hypothesis,
i8 != i35 ).
cnf(u2267,hypothesis,
i8 != i36 ).
cnf(u2272,hypothesis,
i8 != i37 ).
cnf(u2277,hypothesis,
i8 != i38 ).
cnf(u2282,hypothesis,
i8 != i39 ).
cnf(u2287,hypothesis,
i8 != i40 ).
cnf(u2292,hypothesis,
i9 != i10 ).
cnf(u2297,hypothesis,
i9 != i11 ).
cnf(u2302,hypothesis,
i9 != i12 ).
cnf(u2307,hypothesis,
i9 != i13 ).
cnf(u2312,hypothesis,
i9 != i14 ).
cnf(u2317,hypothesis,
i9 != i15 ).
cnf(u2322,hypothesis,
i9 != i16 ).
cnf(u2327,hypothesis,
i9 != i17 ).
cnf(u2332,hypothesis,
i9 != i18 ).
cnf(u2337,hypothesis,
i9 != i19 ).
cnf(u2342,hypothesis,
i9 != i20 ).
cnf(u2347,hypothesis,
i9 != i21 ).
cnf(u2352,hypothesis,
i9 != i22 ).
cnf(u2357,hypothesis,
i9 != i23 ).
cnf(u2362,hypothesis,
i9 != i24 ).
cnf(u2367,hypothesis,
i9 != i25 ).
cnf(u2372,hypothesis,
i9 != i26 ).
cnf(u2377,hypothesis,
i9 != i27 ).
cnf(u2382,hypothesis,
i9 != i28 ).
cnf(u2387,hypothesis,
i9 != i29 ).
cnf(u2392,hypothesis,
i9 != i30 ).
cnf(u2397,hypothesis,
i9 != i31 ).
cnf(u2402,hypothesis,
i9 != i32 ).
cnf(u2407,hypothesis,
i9 != i33 ).
cnf(u2412,hypothesis,
i9 != i34 ).
cnf(u2417,hypothesis,
i9 != i35 ).
cnf(u2422,hypothesis,
i9 != i36 ).
cnf(u2427,hypothesis,
i9 != i37 ).
cnf(u2432,hypothesis,
i9 != i38 ).
cnf(u2437,hypothesis,
i9 != i39 ).
cnf(u2442,hypothesis,
i9 != i40 ).
cnf(u2447,hypothesis,
i10 != i11 ).
cnf(u2452,hypothesis,
i10 != i12 ).
cnf(u2457,hypothesis,
i10 != i13 ).
cnf(u2462,hypothesis,
i10 != i14 ).
cnf(u2467,hypothesis,
i10 != i15 ).
cnf(u2472,hypothesis,
i10 != i16 ).
cnf(u2477,hypothesis,
i10 != i17 ).
cnf(u2482,hypothesis,
i10 != i18 ).
cnf(u2487,hypothesis,
i10 != i19 ).
cnf(u2492,hypothesis,
i10 != i20 ).
cnf(u2497,hypothesis,
i10 != i21 ).
cnf(u2502,hypothesis,
i10 != i22 ).
cnf(u2507,hypothesis,
i10 != i23 ).
cnf(u2512,hypothesis,
i10 != i24 ).
cnf(u2517,hypothesis,
i10 != i25 ).
cnf(u2522,hypothesis,
i10 != i26 ).
cnf(u2527,hypothesis,
i10 != i27 ).
cnf(u2532,hypothesis,
i10 != i28 ).
cnf(u2537,hypothesis,
i10 != i29 ).
cnf(u2542,hypothesis,
i10 != i30 ).
cnf(u2547,hypothesis,
i10 != i31 ).
cnf(u2552,hypothesis,
i10 != i32 ).
cnf(u2557,hypothesis,
i10 != i33 ).
cnf(u2562,hypothesis,
i10 != i34 ).
cnf(u2567,hypothesis,
i10 != i35 ).
cnf(u2572,hypothesis,
i10 != i36 ).
cnf(u2577,hypothesis,
i10 != i37 ).
cnf(u2582,hypothesis,
i10 != i38 ).
cnf(u2587,hypothesis,
i10 != i39 ).
cnf(u2592,hypothesis,
i10 != i40 ).
cnf(u2597,hypothesis,
i11 != i12 ).
cnf(u2602,hypothesis,
i11 != i13 ).
cnf(u2607,hypothesis,
i11 != i14 ).
cnf(u2612,hypothesis,
i11 != i15 ).
cnf(u2617,hypothesis,
i11 != i16 ).
cnf(u2622,hypothesis,
i11 != i17 ).
cnf(u2627,hypothesis,
i11 != i18 ).
cnf(u2632,hypothesis,
i11 != i19 ).
cnf(u2637,hypothesis,
i11 != i20 ).
cnf(u2642,hypothesis,
i11 != i21 ).
cnf(u2647,hypothesis,
i11 != i22 ).
cnf(u2652,hypothesis,
i11 != i23 ).
cnf(u2657,hypothesis,
i11 != i24 ).
cnf(u2662,hypothesis,
i11 != i25 ).
cnf(u2667,hypothesis,
i11 != i26 ).
cnf(u2672,hypothesis,
i11 != i27 ).
cnf(u2677,hypothesis,
i11 != i28 ).
cnf(u2682,hypothesis,
i11 != i29 ).
cnf(u2687,hypothesis,
i11 != i30 ).
cnf(u2692,hypothesis,
i11 != i31 ).
cnf(u2697,hypothesis,
i11 != i32 ).
cnf(u2702,hypothesis,
i11 != i33 ).
cnf(u2707,hypothesis,
i11 != i34 ).
cnf(u2712,hypothesis,
i11 != i35 ).
cnf(u2717,hypothesis,
i11 != i36 ).
cnf(u2722,hypothesis,
i11 != i37 ).
cnf(u2727,hypothesis,
i11 != i38 ).
cnf(u2732,hypothesis,
i11 != i39 ).
cnf(u2737,hypothesis,
i11 != i40 ).
cnf(u2742,hypothesis,
i12 != i13 ).
cnf(u2747,hypothesis,
i12 != i14 ).
cnf(u2752,hypothesis,
i12 != i15 ).
cnf(u2757,hypothesis,
i12 != i16 ).
cnf(u2762,hypothesis,
i12 != i17 ).
cnf(u2767,hypothesis,
i12 != i18 ).
cnf(u2772,hypothesis,
i12 != i19 ).
cnf(u2777,hypothesis,
i12 != i20 ).
cnf(u2782,hypothesis,
i12 != i21 ).
cnf(u2787,hypothesis,
i12 != i22 ).
cnf(u2792,hypothesis,
i12 != i23 ).
cnf(u2797,hypothesis,
i12 != i24 ).
cnf(u2802,hypothesis,
i12 != i25 ).
cnf(u2807,hypothesis,
i12 != i26 ).
cnf(u2812,hypothesis,
i12 != i27 ).
cnf(u2817,hypothesis,
i12 != i28 ).
cnf(u2822,hypothesis,
i12 != i29 ).
cnf(u2827,hypothesis,
i12 != i30 ).
cnf(u2832,hypothesis,
i12 != i31 ).
cnf(u2837,hypothesis,
i12 != i32 ).
cnf(u2842,hypothesis,
i12 != i33 ).
cnf(u2847,hypothesis,
i12 != i34 ).
cnf(u2852,hypothesis,
i12 != i35 ).
cnf(u2857,hypothesis,
i12 != i36 ).
cnf(u2862,hypothesis,
i12 != i37 ).
cnf(u2867,hypothesis,
i12 != i38 ).
cnf(u2872,hypothesis,
i12 != i39 ).
cnf(u2877,hypothesis,
i12 != i40 ).
cnf(u2882,hypothesis,
i13 != i14 ).
cnf(u2887,hypothesis,
i13 != i15 ).
cnf(u2892,hypothesis,
i13 != i16 ).
cnf(u2897,hypothesis,
i13 != i17 ).
cnf(u2902,hypothesis,
i13 != i18 ).
cnf(u2907,hypothesis,
i13 != i19 ).
cnf(u2912,hypothesis,
i13 != i20 ).
cnf(u2917,hypothesis,
i13 != i21 ).
cnf(u2922,hypothesis,
i13 != i22 ).
cnf(u2927,hypothesis,
i13 != i23 ).
cnf(u2932,hypothesis,
i13 != i24 ).
cnf(u2937,hypothesis,
i13 != i25 ).
cnf(u2942,hypothesis,
i13 != i26 ).
cnf(u2947,hypothesis,
i13 != i27 ).
cnf(u2952,hypothesis,
i13 != i28 ).
cnf(u2957,hypothesis,
i13 != i29 ).
cnf(u2962,hypothesis,
i13 != i30 ).
cnf(u2967,hypothesis,
i13 != i31 ).
cnf(u2972,hypothesis,
i13 != i32 ).
cnf(u2977,hypothesis,
i13 != i33 ).
cnf(u2982,hypothesis,
i13 != i34 ).
cnf(u2987,hypothesis,
i13 != i35 ).
cnf(u2992,hypothesis,
i13 != i36 ).
cnf(u2997,hypothesis,
i13 != i37 ).
cnf(u3002,hypothesis,
i13 != i38 ).
cnf(u3007,hypothesis,
i13 != i39 ).
cnf(u3012,hypothesis,
i13 != i40 ).
cnf(u3017,hypothesis,
i14 != i15 ).
cnf(u3022,hypothesis,
i14 != i16 ).
cnf(u3027,hypothesis,
i14 != i17 ).
cnf(u3032,hypothesis,
i14 != i18 ).
cnf(u3037,hypothesis,
i14 != i19 ).
cnf(u3042,hypothesis,
i14 != i20 ).
cnf(u3047,hypothesis,
i14 != i21 ).
cnf(u3052,hypothesis,
i14 != i22 ).
cnf(u3057,hypothesis,
i14 != i23 ).
cnf(u3062,hypothesis,
i14 != i24 ).
cnf(u3067,hypothesis,
i14 != i25 ).
cnf(u3072,hypothesis,
i14 != i26 ).
cnf(u3077,hypothesis,
i14 != i27 ).
cnf(u3082,hypothesis,
i14 != i28 ).
cnf(u3087,hypothesis,
i14 != i29 ).
cnf(u3092,hypothesis,
i14 != i30 ).
cnf(u3097,hypothesis,
i14 != i31 ).
cnf(u3102,hypothesis,
i14 != i32 ).
cnf(u3107,hypothesis,
i14 != i33 ).
cnf(u3112,hypothesis,
i14 != i34 ).
cnf(u3117,hypothesis,
i14 != i35 ).
cnf(u3122,hypothesis,
i14 != i36 ).
cnf(u3127,hypothesis,
i14 != i37 ).
cnf(u3132,hypothesis,
i14 != i38 ).
cnf(u3137,hypothesis,
i14 != i39 ).
cnf(u3142,hypothesis,
i14 != i40 ).
cnf(u3147,hypothesis,
i15 != i16 ).
cnf(u3152,hypothesis,
i15 != i17 ).
cnf(u3157,hypothesis,
i15 != i18 ).
cnf(u3162,hypothesis,
i15 != i19 ).
cnf(u3167,hypothesis,
i15 != i20 ).
cnf(u3172,hypothesis,
i15 != i21 ).
cnf(u3177,hypothesis,
i15 != i22 ).
cnf(u3182,hypothesis,
i15 != i23 ).
cnf(u3187,hypothesis,
i15 != i24 ).
cnf(u3192,hypothesis,
i15 != i25 ).
cnf(u3197,hypothesis,
i15 != i26 ).
cnf(u3202,hypothesis,
i15 != i27 ).
cnf(u3207,hypothesis,
i15 != i28 ).
cnf(u3212,hypothesis,
i15 != i29 ).
cnf(u3217,hypothesis,
i15 != i30 ).
cnf(u3222,hypothesis,
i15 != i31 ).
cnf(u3227,hypothesis,
i15 != i32 ).
cnf(u3232,hypothesis,
i15 != i33 ).
cnf(u3237,hypothesis,
i15 != i34 ).
cnf(u3242,hypothesis,
i15 != i35 ).
cnf(u3247,hypothesis,
i15 != i36 ).
cnf(u3252,hypothesis,
i15 != i37 ).
cnf(u3257,hypothesis,
i15 != i38 ).
cnf(u3262,hypothesis,
i15 != i39 ).
cnf(u3267,hypothesis,
i15 != i40 ).
cnf(u3272,hypothesis,
i16 != i17 ).
cnf(u3277,hypothesis,
i16 != i18 ).
cnf(u3282,hypothesis,
i16 != i19 ).
cnf(u3287,hypothesis,
i16 != i20 ).
cnf(u3292,hypothesis,
i16 != i21 ).
cnf(u3297,hypothesis,
i16 != i22 ).
cnf(u3302,hypothesis,
i16 != i23 ).
cnf(u3307,hypothesis,
i16 != i24 ).
cnf(u3312,hypothesis,
i16 != i25 ).
cnf(u3317,hypothesis,
i16 != i26 ).
cnf(u3322,hypothesis,
i16 != i27 ).
cnf(u3327,hypothesis,
i16 != i28 ).
cnf(u3332,hypothesis,
i16 != i29 ).
cnf(u3337,hypothesis,
i16 != i30 ).
cnf(u3342,hypothesis,
i16 != i31 ).
cnf(u3347,hypothesis,
i16 != i32 ).
cnf(u3352,hypothesis,
i16 != i33 ).
cnf(u3357,hypothesis,
i16 != i34 ).
cnf(u3362,hypothesis,
i16 != i35 ).
cnf(u3367,hypothesis,
i16 != i36 ).
cnf(u3372,hypothesis,
i16 != i37 ).
cnf(u3377,hypothesis,
i16 != i38 ).
cnf(u3382,hypothesis,
i16 != i39 ).
cnf(u3387,hypothesis,
i16 != i40 ).
cnf(u3392,hypothesis,
i17 != i18 ).
cnf(u3397,hypothesis,
i17 != i19 ).
cnf(u3402,hypothesis,
i17 != i20 ).
cnf(u3407,hypothesis,
i17 != i21 ).
cnf(u3412,hypothesis,
i17 != i22 ).
cnf(u3417,hypothesis,
i17 != i23 ).
cnf(u3422,hypothesis,
i17 != i24 ).
cnf(u3427,hypothesis,
i17 != i25 ).
cnf(u3432,hypothesis,
i17 != i26 ).
cnf(u3437,hypothesis,
i17 != i27 ).
cnf(u3442,hypothesis,
i17 != i28 ).
cnf(u3447,hypothesis,
i17 != i29 ).
cnf(u3452,hypothesis,
i17 != i30 ).
cnf(u3457,hypothesis,
i17 != i31 ).
cnf(u3462,hypothesis,
i17 != i32 ).
cnf(u3467,hypothesis,
i17 != i33 ).
cnf(u3472,hypothesis,
i17 != i34 ).
cnf(u3477,hypothesis,
i17 != i35 ).
cnf(u3482,hypothesis,
i17 != i36 ).
cnf(u3487,hypothesis,
i17 != i37 ).
cnf(u3492,hypothesis,
i17 != i38 ).
cnf(u3497,hypothesis,
i17 != i39 ).
cnf(u3502,hypothesis,
i17 != i40 ).
cnf(u3507,hypothesis,
i18 != i19 ).
cnf(u3512,hypothesis,
i18 != i20 ).
cnf(u3517,hypothesis,
i18 != i21 ).
cnf(u3522,hypothesis,
i18 != i22 ).
cnf(u3527,hypothesis,
i18 != i23 ).
cnf(u3532,hypothesis,
i18 != i24 ).
cnf(u3537,hypothesis,
i18 != i25 ).
cnf(u3542,hypothesis,
i18 != i26 ).
cnf(u3547,hypothesis,
i18 != i27 ).
cnf(u3552,hypothesis,
i18 != i28 ).
cnf(u3557,hypothesis,
i18 != i29 ).
cnf(u3562,hypothesis,
i18 != i30 ).
cnf(u3567,hypothesis,
i18 != i31 ).
cnf(u3572,hypothesis,
i18 != i32 ).
cnf(u3577,hypothesis,
i18 != i33 ).
cnf(u3582,hypothesis,
i18 != i34 ).
cnf(u3587,hypothesis,
i18 != i35 ).
cnf(u3592,hypothesis,
i18 != i36 ).
cnf(u3597,hypothesis,
i18 != i37 ).
cnf(u3602,hypothesis,
i18 != i38 ).
cnf(u3607,hypothesis,
i18 != i39 ).
cnf(u3612,hypothesis,
i18 != i40 ).
cnf(u3617,hypothesis,
i19 != i20 ).
cnf(u3622,hypothesis,
i19 != i21 ).
cnf(u3627,hypothesis,
i19 != i22 ).
cnf(u3632,hypothesis,
i19 != i23 ).
cnf(u3637,hypothesis,
i19 != i24 ).
cnf(u3642,hypothesis,
i19 != i25 ).
cnf(u3647,hypothesis,
i19 != i26 ).
cnf(u3652,hypothesis,
i19 != i27 ).
cnf(u3657,hypothesis,
i19 != i28 ).
cnf(u3662,hypothesis,
i19 != i29 ).
cnf(u3667,hypothesis,
i19 != i30 ).
cnf(u3672,hypothesis,
i19 != i31 ).
cnf(u3677,hypothesis,
i19 != i32 ).
cnf(u3682,hypothesis,
i19 != i33 ).
cnf(u3687,hypothesis,
i19 != i34 ).
cnf(u3692,hypothesis,
i19 != i35 ).
cnf(u3697,hypothesis,
i19 != i36 ).
cnf(u3702,hypothesis,
i19 != i37 ).
cnf(u3707,hypothesis,
i19 != i38 ).
cnf(u3712,hypothesis,
i19 != i39 ).
cnf(u3717,hypothesis,
i19 != i40 ).
cnf(u3722,hypothesis,
i20 != i21 ).
cnf(u3727,hypothesis,
i20 != i22 ).
cnf(u3732,hypothesis,
i20 != i23 ).
cnf(u3737,hypothesis,
i20 != i24 ).
cnf(u3742,hypothesis,
i20 != i25 ).
cnf(u3747,hypothesis,
i20 != i26 ).
cnf(u3752,hypothesis,
i20 != i27 ).
cnf(u3757,hypothesis,
i20 != i28 ).
cnf(u3762,hypothesis,
i20 != i29 ).
cnf(u3767,hypothesis,
i20 != i30 ).
cnf(u3772,hypothesis,
i20 != i31 ).
cnf(u3777,hypothesis,
i20 != i32 ).
cnf(u3782,hypothesis,
i20 != i33 ).
cnf(u3787,hypothesis,
i20 != i34 ).
cnf(u3792,hypothesis,
i20 != i35 ).
cnf(u3797,hypothesis,
i20 != i36 ).
cnf(u3802,hypothesis,
i20 != i37 ).
cnf(u3807,hypothesis,
i20 != i38 ).
cnf(u3812,hypothesis,
i20 != i39 ).
cnf(u3817,hypothesis,
i20 != i40 ).
cnf(u3822,hypothesis,
i21 != i22 ).
cnf(u3827,hypothesis,
i21 != i23 ).
cnf(u3832,hypothesis,
i21 != i24 ).
cnf(u3837,hypothesis,
i21 != i25 ).
cnf(u3842,hypothesis,
i21 != i26 ).
cnf(u3847,hypothesis,
i21 != i27 ).
cnf(u3852,hypothesis,
i21 != i28 ).
cnf(u3857,hypothesis,
i21 != i29 ).
cnf(u3862,hypothesis,
i21 != i30 ).
cnf(u3867,hypothesis,
i21 != i31 ).
cnf(u3872,hypothesis,
i21 != i32 ).
cnf(u3877,hypothesis,
i21 != i33 ).
cnf(u3882,hypothesis,
i21 != i34 ).
cnf(u3887,hypothesis,
i21 != i35 ).
cnf(u3892,hypothesis,
i21 != i36 ).
cnf(u3897,hypothesis,
i21 != i37 ).
cnf(u3902,hypothesis,
i21 != i38 ).
cnf(u3907,hypothesis,
i21 != i39 ).
cnf(u3912,hypothesis,
i21 != i40 ).
cnf(u3917,hypothesis,
i22 != i23 ).
cnf(u3922,hypothesis,
i22 != i24 ).
cnf(u3927,hypothesis,
i22 != i25 ).
cnf(u3932,hypothesis,
i22 != i26 ).
cnf(u3937,hypothesis,
i22 != i27 ).
cnf(u3942,hypothesis,
i22 != i28 ).
cnf(u3947,hypothesis,
i22 != i29 ).
cnf(u3952,hypothesis,
i22 != i30 ).
cnf(u3957,hypothesis,
i22 != i31 ).
cnf(u3962,hypothesis,
i22 != i32 ).
cnf(u3967,hypothesis,
i22 != i33 ).
cnf(u3972,hypothesis,
i22 != i34 ).
cnf(u3977,hypothesis,
i22 != i35 ).
cnf(u3982,hypothesis,
i22 != i36 ).
cnf(u3987,hypothesis,
i22 != i37 ).
cnf(u3992,hypothesis,
i22 != i38 ).
cnf(u3997,hypothesis,
i22 != i39 ).
cnf(u4002,hypothesis,
i22 != i40 ).
cnf(u4007,hypothesis,
i23 != i24 ).
cnf(u4012,hypothesis,
i23 != i25 ).
cnf(u4017,hypothesis,
i23 != i26 ).
cnf(u4022,hypothesis,
i23 != i27 ).
cnf(u4027,hypothesis,
i23 != i28 ).
cnf(u4032,hypothesis,
i23 != i29 ).
cnf(u4037,hypothesis,
i23 != i30 ).
cnf(u4042,hypothesis,
i23 != i31 ).
cnf(u4047,hypothesis,
i23 != i32 ).
cnf(u4052,hypothesis,
i23 != i33 ).
cnf(u4057,hypothesis,
i23 != i34 ).
cnf(u4062,hypothesis,
i23 != i35 ).
cnf(u4067,hypothesis,
i23 != i36 ).
cnf(u4072,hypothesis,
i23 != i37 ).
cnf(u4077,hypothesis,
i23 != i38 ).
cnf(u4082,hypothesis,
i23 != i39 ).
cnf(u4087,hypothesis,
i23 != i40 ).
cnf(u4092,hypothesis,
i24 != i25 ).
cnf(u4097,hypothesis,
i24 != i26 ).
cnf(u4102,hypothesis,
i24 != i27 ).
cnf(u4107,hypothesis,
i24 != i28 ).
cnf(u4112,hypothesis,
i24 != i29 ).
cnf(u4117,hypothesis,
i24 != i30 ).
cnf(u4122,hypothesis,
i24 != i31 ).
cnf(u4127,hypothesis,
i24 != i32 ).
cnf(u4132,hypothesis,
i24 != i33 ).
cnf(u4137,hypothesis,
i24 != i34 ).
cnf(u4142,hypothesis,
i24 != i35 ).
cnf(u4147,hypothesis,
i24 != i36 ).
cnf(u4152,hypothesis,
i24 != i37 ).
cnf(u4157,hypothesis,
i24 != i38 ).
cnf(u4162,hypothesis,
i24 != i39 ).
cnf(u4167,hypothesis,
i24 != i40 ).
cnf(u4172,hypothesis,
i25 != i26 ).
cnf(u4177,hypothesis,
i25 != i27 ).
cnf(u4182,hypothesis,
i25 != i28 ).
cnf(u4187,hypothesis,
i25 != i29 ).
cnf(u4192,hypothesis,
i25 != i30 ).
cnf(u4197,hypothesis,
i25 != i31 ).
cnf(u4202,hypothesis,
i25 != i32 ).
cnf(u4207,hypothesis,
i25 != i33 ).
cnf(u4212,hypothesis,
i25 != i34 ).
cnf(u4217,hypothesis,
i25 != i35 ).
cnf(u4222,hypothesis,
i25 != i36 ).
cnf(u4227,hypothesis,
i25 != i37 ).
cnf(u4232,hypothesis,
i25 != i38 ).
cnf(u4237,hypothesis,
i25 != i39 ).
cnf(u4242,hypothesis,
i25 != i40 ).
cnf(u4247,hypothesis,
i26 != i27 ).
cnf(u4252,hypothesis,
i26 != i28 ).
cnf(u4257,hypothesis,
i26 != i29 ).
cnf(u4262,hypothesis,
i26 != i30 ).
cnf(u4267,hypothesis,
i26 != i31 ).
cnf(u4272,hypothesis,
i26 != i32 ).
cnf(u4277,hypothesis,
i26 != i33 ).
cnf(u4282,hypothesis,
i26 != i34 ).
cnf(u4287,hypothesis,
i26 != i35 ).
cnf(u4292,hypothesis,
i26 != i36 ).
cnf(u4297,hypothesis,
i26 != i37 ).
cnf(u4302,hypothesis,
i26 != i38 ).
cnf(u4307,hypothesis,
i26 != i39 ).
cnf(u4312,hypothesis,
i26 != i40 ).
cnf(u4317,hypothesis,
i27 != i28 ).
cnf(u4322,hypothesis,
i27 != i29 ).
cnf(u4327,hypothesis,
i27 != i30 ).
cnf(u4332,hypothesis,
i27 != i31 ).
cnf(u4337,hypothesis,
i27 != i32 ).
cnf(u4342,hypothesis,
i27 != i33 ).
cnf(u4347,hypothesis,
i27 != i34 ).
cnf(u4352,hypothesis,
i27 != i35 ).
cnf(u4357,hypothesis,
i27 != i36 ).
cnf(u4362,hypothesis,
i27 != i37 ).
cnf(u4367,hypothesis,
i27 != i38 ).
cnf(u4372,hypothesis,
i27 != i39 ).
cnf(u4377,hypothesis,
i27 != i40 ).
cnf(u4382,hypothesis,
i28 != i29 ).
cnf(u4387,hypothesis,
i28 != i30 ).
cnf(u4392,hypothesis,
i28 != i31 ).
cnf(u4397,hypothesis,
i28 != i32 ).
cnf(u4402,hypothesis,
i28 != i33 ).
cnf(u4407,hypothesis,
i28 != i34 ).
cnf(u4412,hypothesis,
i28 != i35 ).
cnf(u4417,hypothesis,
i28 != i36 ).
cnf(u4422,hypothesis,
i28 != i37 ).
cnf(u4427,hypothesis,
i28 != i38 ).
cnf(u4432,hypothesis,
i28 != i39 ).
cnf(u4437,hypothesis,
i28 != i40 ).
cnf(u4442,hypothesis,
i29 != i30 ).
cnf(u4447,hypothesis,
i29 != i31 ).
cnf(u4452,hypothesis,
i29 != i32 ).
cnf(u4457,hypothesis,
i29 != i33 ).
cnf(u4462,hypothesis,
i29 != i34 ).
cnf(u4467,hypothesis,
i29 != i35 ).
cnf(u4472,hypothesis,
i29 != i36 ).
cnf(u4477,hypothesis,
i29 != i37 ).
cnf(u4482,hypothesis,
i29 != i38 ).
cnf(u4487,hypothesis,
i29 != i39 ).
cnf(u4492,hypothesis,
i29 != i40 ).
cnf(u4497,hypothesis,
i30 != i31 ).
cnf(u4502,hypothesis,
i30 != i32 ).
cnf(u4507,hypothesis,
i30 != i33 ).
cnf(u4512,hypothesis,
i30 != i34 ).
cnf(u4517,hypothesis,
i30 != i35 ).
cnf(u4522,hypothesis,
i30 != i36 ).
cnf(u4527,hypothesis,
i30 != i37 ).
cnf(u4532,hypothesis,
i30 != i38 ).
cnf(u4537,hypothesis,
i30 != i39 ).
cnf(u4542,hypothesis,
i30 != i40 ).
cnf(u4547,hypothesis,
i31 != i32 ).
cnf(u4552,hypothesis,
i31 != i33 ).
cnf(u4557,hypothesis,
i31 != i34 ).
cnf(u4562,hypothesis,
i31 != i35 ).
cnf(u4567,hypothesis,
i31 != i36 ).
cnf(u4572,hypothesis,
i31 != i37 ).
cnf(u4577,hypothesis,
i31 != i38 ).
cnf(u4582,hypothesis,
i31 != i39 ).
cnf(u4587,hypothesis,
i31 != i40 ).
cnf(u4592,hypothesis,
i32 != i33 ).
cnf(u4597,hypothesis,
i32 != i34 ).
cnf(u4602,hypothesis,
i32 != i35 ).
cnf(u4607,hypothesis,
i32 != i36 ).
cnf(u4612,hypothesis,
i32 != i37 ).
cnf(u4617,hypothesis,
i32 != i38 ).
cnf(u4622,hypothesis,
i32 != i39 ).
cnf(u4627,hypothesis,
i32 != i40 ).
cnf(u4632,hypothesis,
i33 != i34 ).
cnf(u4637,hypothesis,
i33 != i35 ).
cnf(u4642,hypothesis,
i33 != i36 ).
cnf(u4647,hypothesis,
i33 != i37 ).
cnf(u4652,hypothesis,
i33 != i38 ).
cnf(u4657,hypothesis,
i33 != i39 ).
cnf(u4662,hypothesis,
i33 != i40 ).
cnf(u4667,hypothesis,
i34 != i35 ).
cnf(u4672,hypothesis,
i34 != i36 ).
cnf(u4677,hypothesis,
i34 != i37 ).
cnf(u4682,hypothesis,
i34 != i38 ).
cnf(u4687,hypothesis,
i34 != i39 ).
cnf(u4692,hypothesis,
i34 != i40 ).
cnf(u4697,hypothesis,
i35 != i36 ).
cnf(u4702,hypothesis,
i35 != i37 ).
cnf(u4707,hypothesis,
i35 != i38 ).
cnf(u4712,hypothesis,
i35 != i39 ).
cnf(u4717,hypothesis,
i35 != i40 ).
cnf(u4722,hypothesis,
i36 != i37 ).
cnf(u4727,hypothesis,
i36 != i38 ).
cnf(u4732,hypothesis,
i36 != i39 ).
cnf(u4737,hypothesis,
i36 != i40 ).
cnf(u4742,hypothesis,
i37 != i38 ).
cnf(u4747,hypothesis,
i37 != i39 ).
cnf(u4752,hypothesis,
i37 != i40 ).
cnf(u4757,hypothesis,
i38 != i39 ).
cnf(u4762,hypothesis,
i38 != i40 ).
cnf(u4767,hypothesis,
i39 != i40 ).
cnf(u4772,hypothesis,
a_1438 = store(a_1437,i19,e19) ).
cnf(u4777,hypothesis,
a_1437 = store(a_1436,i29,e29) ).
cnf(u4782,hypothesis,
a_1436 = store(a_1435,i28,e28) ).
cnf(u4787,hypothesis,
a_1435 = store(a_1434,i34,e34) ).
cnf(u4792,hypothesis,
a_1434 = store(a_1433,i15,e15) ).
cnf(u4797,hypothesis,
a_1433 = store(a_1432,i30,e30) ).
cnf(u4802,hypothesis,
a_1432 = store(a_1431,i4,e4) ).
cnf(u4807,hypothesis,
a_1431 = store(a_1430,i5,e5) ).
cnf(u4812,hypothesis,
a_1430 = store(a_1429,i3,e3) ).
cnf(u4817,hypothesis,
a_1429 = store(a_1428,i9,e9) ).
cnf(u4822,hypothesis,
a_1428 = store(a_1427,i1,e1) ).
cnf(u4827,hypothesis,
a_1427 = store(a_1426,i39,e39) ).
cnf(u4832,hypothesis,
a_1426 = store(a_1425,i38,e38) ).
cnf(u4837,hypothesis,
a_1425 = store(a_1424,i40,e40) ).
cnf(u4842,hypothesis,
a_1424 = store(a_1423,i2,e2) ).
cnf(u4847,hypothesis,
a_1423 = store(a_1422,i33,e33) ).
cnf(u4852,hypothesis,
a_1422 = store(a_1421,i8,e8) ).
cnf(u4857,hypothesis,
a_1421 = store(a_1420,i22,e22) ).
cnf(u4862,hypothesis,
a_1420 = store(a_1419,i10,e10) ).
cnf(u4867,hypothesis,
a_1419 = store(a_1418,i27,e27) ).
cnf(u4872,hypothesis,
a_1418 = store(a_1417,i21,e21) ).
cnf(u4877,hypothesis,
a_1417 = store(a_1416,i26,e26) ).
cnf(u4882,hypothesis,
a_1416 = store(a_1415,i23,e23) ).
cnf(u4887,hypothesis,
a_1415 = store(a_1414,i35,e35) ).
cnf(u4892,hypothesis,
a_1414 = store(a_1413,i20,e20) ).
cnf(u4897,hypothesis,
a_1413 = store(a_1412,i36,e36) ).
cnf(u4902,hypothesis,
a_1412 = store(a_1411,i12,e12) ).
cnf(u4907,hypothesis,
a_1411 = store(a_1410,i13,e13) ).
cnf(u4912,hypothesis,
a_1410 = store(a_1409,i31,e31) ).
cnf(u4917,hypothesis,
a_1409 = store(a_1408,i37,e37) ).
cnf(u4922,hypothesis,
a_1408 = store(a_1407,i18,e18) ).
cnf(u4927,hypothesis,
a_1407 = store(a_1406,i6,e6) ).
cnf(u4932,hypothesis,
a_1406 = store(a_1405,i32,e32) ).
cnf(u4937,hypothesis,
a_1405 = store(a_1404,i7,e7) ).
cnf(u4942,hypothesis,
a_1404 = store(a_1403,i17,e17) ).
cnf(u4947,hypothesis,
a_1403 = store(a_1402,i25,e25) ).
cnf(u4952,hypothesis,
a_1402 = store(a_1401,i11,e11) ).
cnf(u4957,hypothesis,
a_1401 = store(a_1400,i24,e24) ).
cnf(u4962,hypothesis,
a_1400 = store(a_1399,i14,e14) ).
cnf(u4967,hypothesis,
a_1399 = store(a1,i16,e16) ).
cnf(u4972,hypothesis,
a_1398 = store(a_1397,i40,e40) ).
cnf(u4977,hypothesis,
a_1397 = store(a_1396,i39,e39) ).
cnf(u4982,hypothesis,
a_1396 = store(a_1395,i38,e38) ).
cnf(u4987,hypothesis,
a_1395 = store(a_1394,i37,e37) ).
cnf(u4992,hypothesis,
a_1394 = store(a_1393,i36,e36) ).
cnf(u4997,hypothesis,
a_1393 = store(a_1392,i35,e35) ).
cnf(u5002,hypothesis,
a_1392 = store(a_1391,i34,e34) ).
cnf(u5007,hypothesis,
a_1391 = store(a_1390,i33,e33) ).
cnf(u5012,hypothesis,
a_1390 = store(a_1389,i32,e32) ).
cnf(u5017,hypothesis,
a_1389 = store(a_1388,i31,e31) ).
cnf(u5022,hypothesis,
a_1388 = store(a_1387,i30,e30) ).
cnf(u5027,hypothesis,
a_1387 = store(a_1386,i29,e29) ).
cnf(u5032,hypothesis,
a_1386 = store(a_1385,i28,e28) ).
cnf(u5037,hypothesis,
a_1385 = store(a_1384,i27,e27) ).
cnf(u5042,hypothesis,
a_1384 = store(a_1383,i26,e26) ).
cnf(u5047,hypothesis,
a_1383 = store(a_1382,i25,e25) ).
cnf(u5052,hypothesis,
a_1382 = store(a_1381,i24,e24) ).
cnf(u5057,hypothesis,
a_1381 = store(a_1380,i23,e23) ).
cnf(u5062,hypothesis,
a_1380 = store(a_1379,i22,e22) ).
cnf(u5067,hypothesis,
a_1379 = store(a_1378,i21,e21) ).
cnf(u5072,hypothesis,
a_1378 = store(a_1377,i20,e20) ).
cnf(u5077,hypothesis,
a_1377 = store(a_1376,i19,e19) ).
cnf(u5082,hypothesis,
a_1376 = store(a_1375,i18,e18) ).
cnf(u5087,hypothesis,
a_1375 = store(a_1374,i17,e17) ).
cnf(u5092,hypothesis,
a_1374 = store(a_1373,i16,e16) ).
cnf(u5097,hypothesis,
a_1373 = store(a_1372,i15,e15) ).
cnf(u5102,hypothesis,
a_1372 = store(a_1371,i14,e14) ).
cnf(u5107,hypothesis,
a_1371 = store(a_1370,i13,e13) ).
cnf(u5112,hypothesis,
a_1370 = store(a_1369,i12,e12) ).
cnf(u5117,hypothesis,
a_1369 = store(a_1368,i11,e11) ).
cnf(u5122,hypothesis,
a_1368 = store(a_1367,i10,e10) ).
cnf(u5127,hypothesis,
a_1367 = store(a_1366,i9,e9) ).
cnf(u5132,hypothesis,
a_1366 = store(a_1365,i8,e8) ).
cnf(u5137,hypothesis,
a_1365 = store(a_1364,i7,e7) ).
cnf(u5142,hypothesis,
a_1364 = store(a_1363,i6,e6) ).
cnf(u5147,hypothesis,
a_1363 = store(a_1362,i5,e5) ).
cnf(u5152,hypothesis,
a_1362 = store(a_1361,i4,e4) ).
cnf(u5157,hypothesis,
a_1361 = store(a_1360,i3,e3) ).
cnf(u5162,hypothesis,
a_1360 = store(a_1359,i2,e2) ).
cnf(u5167,hypothesis,
a_1359 = store(a1,i1,e1) ).
cnf(u5252,hypothesis,
e19 = select(a_1438,i19) ).
cnf(u5257,hypothesis,
e29 = select(a_1437,i29) ).
cnf(u5262,hypothesis,
e28 = select(a_1436,i28) ).
cnf(u5267,hypothesis,
e34 = select(a_1435,i34) ).
cnf(u5272,hypothesis,
e15 = select(a_1434,i15) ).
cnf(u5277,hypothesis,
e30 = select(a_1433,i30) ).
cnf(u5282,hypothesis,
e4 = select(a_1432,i4) ).
cnf(u5287,hypothesis,
e5 = select(a_1431,i5) ).
cnf(u5292,hypothesis,
e3 = select(a_1430,i3) ).
cnf(u5297,hypothesis,
e9 = select(a_1429,i9) ).
cnf(u5302,hypothesis,
e1 = select(a_1428,i1) ).
cnf(u5307,hypothesis,
e39 = select(a_1427,i39) ).
cnf(u5312,hypothesis,
e38 = select(a_1426,i38) ).
cnf(u5317,hypothesis,
e40 = select(a_1425,i40) ).
cnf(u5322,hypothesis,
e2 = select(a_1424,i2) ).
cnf(u5327,hypothesis,
e33 = select(a_1423,i33) ).
cnf(u5332,hypothesis,
e8 = select(a_1422,i8) ).
cnf(u5337,hypothesis,
e22 = select(a_1421,i22) ).
cnf(u5342,hypothesis,
e10 = select(a_1420,i10) ).
cnf(u5347,hypothesis,
e27 = select(a_1419,i27) ).
cnf(u5352,hypothesis,
e21 = select(a_1418,i21) ).
cnf(u5357,hypothesis,
e26 = select(a_1417,i26) ).
cnf(u5362,hypothesis,
e23 = select(a_1416,i23) ).
cnf(u5367,hypothesis,
e35 = select(a_1415,i35) ).
cnf(u5372,hypothesis,
e20 = select(a_1414,i20) ).
cnf(u5377,hypothesis,
e36 = select(a_1413,i36) ).
cnf(u5382,hypothesis,
e12 = select(a_1412,i12) ).
cnf(u5387,hypothesis,
e13 = select(a_1411,i13) ).
cnf(u5392,hypothesis,
e31 = select(a_1410,i31) ).
cnf(u5397,hypothesis,
e37 = select(a_1409,i37) ).
cnf(u5402,hypothesis,
e18 = select(a_1408,i18) ).
cnf(u5407,hypothesis,
e6 = select(a_1407,i6) ).
cnf(u5412,hypothesis,
e32 = select(a_1406,i32) ).
cnf(u5417,hypothesis,
e7 = select(a_1405,i7) ).
cnf(u5422,hypothesis,
e17 = select(a_1404,i17) ).
cnf(u5427,hypothesis,
e25 = select(a_1403,i25) ).
cnf(u5432,hypothesis,
e11 = select(a_1402,i11) ).
cnf(u5437,hypothesis,
e24 = select(a_1401,i24) ).
cnf(u5442,hypothesis,
e14 = select(a_1400,i14) ).
cnf(u5447,hypothesis,
e40 = select(a_1398,i40) ).
cnf(u5452,hypothesis,
e39 = select(a_1397,i39) ).
cnf(u5457,hypothesis,
e38 = select(a_1396,i38) ).
cnf(u5462,hypothesis,
e37 = select(a_1395,i37) ).
cnf(u5467,hypothesis,
e36 = select(a_1394,i36) ).
cnf(u5472,hypothesis,
e35 = select(a_1393,i35) ).
cnf(u5477,hypothesis,
e34 = select(a_1392,i34) ).
cnf(u5482,hypothesis,
e33 = select(a_1391,i33) ).
cnf(u5487,hypothesis,
e32 = select(a_1390,i32) ).
cnf(u5492,hypothesis,
e31 = select(a_1389,i31) ).
cnf(u5497,hypothesis,
e30 = select(a_1388,i30) ).
cnf(u5502,hypothesis,
e29 = select(a_1387,i29) ).
cnf(u5507,hypothesis,
e28 = select(a_1386,i28) ).
cnf(u5512,hypothesis,
e27 = select(a_1385,i27) ).
cnf(u5517,hypothesis,
e26 = select(a_1384,i26) ).
cnf(u5522,hypothesis,
e25 = select(a_1383,i25) ).
cnf(u5527,hypothesis,
e24 = select(a_1382,i24) ).
cnf(u5532,hypothesis,
e23 = select(a_1381,i23) ).
cnf(u5537,hypothesis,
e22 = select(a_1380,i22) ).
cnf(u5542,hypothesis,
e21 = select(a_1379,i21) ).
cnf(u5547,hypothesis,
e20 = select(a_1378,i20) ).
cnf(u5552,hypothesis,
e19 = select(a_1377,i19) ).
cnf(u5557,hypothesis,
e18 = select(a_1376,i18) ).
cnf(u5562,hypothesis,
e17 = select(a_1375,i17) ).
cnf(u5567,hypothesis,
e16 = select(a_1374,i16) ).
cnf(u5572,hypothesis,
e15 = select(a_1373,i15) ).
cnf(u5577,hypothesis,
e14 = select(a_1372,i14) ).
cnf(u5582,hypothesis,
e13 = select(a_1371,i13) ).
cnf(u5587,hypothesis,
e12 = select(a_1370,i12) ).
cnf(u5592,hypothesis,
e11 = select(a_1369,i11) ).
cnf(u5597,hypothesis,
e10 = select(a_1368,i10) ).
cnf(u5602,hypothesis,
e9 = select(a_1367,i9) ).
cnf(u5607,hypothesis,
e8 = select(a_1366,i8) ).
cnf(u5612,hypothesis,
e7 = select(a_1365,i7) ).
cnf(u5617,hypothesis,
e6 = select(a_1364,i6) ).
cnf(u5622,hypothesis,
e5 = select(a_1363,i5) ).
cnf(u5627,hypothesis,
e4 = select(a_1362,i4) ).
cnf(u5632,hypothesis,
e3 = select(a_1361,i3) ).
cnf(u5637,hypothesis,
e1 = select(a_1359,i1) ).
cnf(u5642,hypothesis,
e16 = select(a_1399,i16) ).
cnf(u5647,hypothesis,
e2 = select(a_1360,i2) ).
cnf(u5665,hypothesis,
( select(a_1373,X0) = select(a_1374,X0)
| i16 = X0 ) ).
cnf(u5650,hypothesis,
( select(a1,X0) = select(a_1399,X0)
| i16 = X0 ) ).
cnf(u5684,hypothesis,
( select(a_1392,X0) = select(a_1393,X0)
| i35 = X0 ) ).
cnf(u5692,hypothesis,
( select(a_1401,X0) = select(a_1402,X0)
| i11 = X0 ) ).
cnf(u5690,hypothesis,
( select(a_1399,X0) = select(a_1400,X0)
| i14 = X0 ) ).
cnf(u5718,hypothesis,
( select(a_1427,X0) = select(a_1428,X0)
| i1 = X0 ) ).
cnf(u5675,hypothesis,
( select(a_1383,X0) = select(a_1384,X0)
| i26 = X0 ) ).
cnf(u5694,hypothesis,
( select(a_1403,X0) = select(a_1404,X0)
| i17 = X0 ) ).
cnf(u5672,hypothesis,
( select(a_1380,X0) = select(a_1381,X0)
| i23 = X0 ) ).
cnf(u5728,hypothesis,
( select(a_1437,X0) = select(a_1438,X0)
| i19 = X0 ) ).
cnf(u5653,hypothesis,
( select(a_1361,X0) = select(a_1362,X0)
| i4 = X0 ) ).
cnf(u5663,hypothesis,
( select(a_1371,X0) = select(a_1372,X0)
| i14 = X0 ) ).
cnf(u5657,hypothesis,
( select(a_1365,X0) = select(a_1366,X0)
| i8 = X0 ) ).
cnf(u5666,hypothesis,
( select(a_1374,X0) = select(a_1375,X0)
| i17 = X0 ) ).
cnf(u5683,hypothesis,
( select(a_1391,X0) = select(a_1392,X0)
| i34 = X0 ) ).
cnf(u5670,hypothesis,
( select(a_1378,X0) = select(a_1379,X0)
| i21 = X0 ) ).
cnf(u5676,hypothesis,
( select(a_1384,X0) = select(a_1385,X0)
| i27 = X0 ) ).
cnf(u5715,hypothesis,
( select(a_1424,X0) = select(a_1425,X0)
| i40 = X0 ) ).
cnf(u5721,hypothesis,
( select(a_1430,X0) = select(a_1431,X0)
| i5 = X0 ) ).
cnf(u5701,hypothesis,
( select(a_1410,X0) = select(a_1411,X0)
| i13 = X0 ) ).
cnf(u5723,hypothesis,
( select(a_1432,X0) = select(a_1433,X0)
| i30 = X0 ) ).
cnf(u5652,hypothesis,
( select(a_1360,X0) = select(a_1361,X0)
| i3 = X0 ) ).
cnf(u5669,hypothesis,
( select(a_1377,X0) = select(a_1378,X0)
| i20 = X0 ) ).
cnf(u5656,hypothesis,
( select(a_1364,X0) = select(a_1365,X0)
| i7 = X0 ) ).
cnf(u5660,hypothesis,
( select(a_1368,X0) = select(a_1369,X0)
| i11 = X0 ) ).
cnf(u5687,hypothesis,
( select(a_1395,X0) = select(a_1396,X0)
| i38 = X0 ) ).
cnf(u5705,hypothesis,
( select(a_1414,X0) = select(a_1415,X0)
| i35 = X0 ) ).
cnf(u5709,hypothesis,
( select(a_1418,X0) = select(a_1419,X0)
| i27 = X0 ) ).
cnf(u5696,hypothesis,
( select(a_1405,X0) = select(a_1406,X0)
| i32 = X0 ) ).
cnf(u5674,hypothesis,
( select(a_1382,X0) = select(a_1383,X0)
| i25 = X0 ) ).
cnf(u5682,hypothesis,
( select(a_1390,X0) = select(a_1391,X0)
| i33 = X0 ) ).
cnf(u5651,hypothesis,
( select(a_1359,X0) = select(a1,X0)
| i1 = X0 ) ).
cnf(u5659,hypothesis,
( select(a_1367,X0) = select(a_1368,X0)
| i10 = X0 ) ).
cnf(a1,axiom,
select(store(X0,X1,X2),X1) = X2 ).
cnf(u5661,hypothesis,
( select(a_1369,X0) = select(a_1370,X0)
| i12 = X0 ) ).
cnf(u5688,hypothesis,
( select(a_1396,X0) = select(a_1397,X0)
| i39 = X0 ) ).
cnf(u5667,hypothesis,
( select(a_1375,X0) = select(a_1376,X0)
| i18 = X0 ) ).
cnf(u5691,hypothesis,
( select(a_1400,X0) = select(a_1401,X0)
| i24 = X0 ) ).
cnf(u5703,hypothesis,
( select(a_1412,X0) = select(a_1413,X0)
| i36 = X0 ) ).
cnf(u5725,hypothesis,
( select(a_1434,X0) = select(a_1435,X0)
| i34 = X0 ) ).
cnf(u5711,hypothesis,
( select(a_1420,X0) = select(a_1421,X0)
| i22 = X0 ) ).
cnf(u5710,hypothesis,
( select(a_1419,X0) = select(a_1420,X0)
| i10 = X0 ) ).
cnf(u5712,hypothesis,
( select(a_1421,X0) = select(a_1422,X0)
| i8 = X0 ) ).
cnf(a2,axiom,
( select(store(X2,X0,X3),X1) = select(X2,X1)
| X0 = X1 ) ).
cnf(u5655,hypothesis,
( select(a_1363,X0) = select(a_1364,X0)
| i6 = X0 ) ).
cnf(u5677,hypothesis,
( select(a_1385,X0) = select(a_1386,X0)
| i28 = X0 ) ).
cnf(u5664,hypothesis,
( select(a_1372,X0) = select(a_1373,X0)
| i15 = X0 ) ).
cnf(u5681,hypothesis,
( select(a_1389,X0) = select(a_1390,X0)
| i32 = X0 ) ).
cnf(u5707,hypothesis,
( select(a_1416,X0) = select(a_1417,X0)
| i26 = X0 ) ).
cnf(u5700,hypothesis,
( select(a_1409,X0) = select(a_1410,X0)
| i31 = X0 ) ).
cnf(u5727,hypothesis,
( select(a_1436,X0) = select(a_1437,X0)
| i29 = X0 ) ).
cnf(u5706,hypothesis,
( select(a_1415,X0) = select(a_1416,X0)
| i23 = X0 ) ).
cnf(u5726,hypothesis,
( select(a_1435,X0) = select(a_1436,X0)
| i28 = X0 ) ).
cnf(u5704,hypothesis,
( select(a_1413,X0) = select(a_1414,X0)
| i20 = X0 ) ).
cnf(u5719,hypothesis,
( select(a_1428,X0) = select(a_1429,X0)
| i9 = X0 ) ).
cnf(u5708,hypothesis,
( select(a_1417,X0) = select(a_1418,X0)
| i21 = X0 ) ).
cnf(u5662,hypothesis,
( select(a_1370,X0) = select(a_1371,X0)
| i13 = X0 ) ).
cnf(u5686,hypothesis,
( select(a_1394,X0) = select(a_1395,X0)
| i37 = X0 ) ).
cnf(u5671,hypothesis,
( select(a_1379,X0) = select(a_1380,X0)
| i22 = X0 ) ).
cnf(u5693,hypothesis,
( select(a_1402,X0) = select(a_1403,X0)
| i25 = X0 ) ).
cnf(u5678,hypothesis,
( select(a_1386,X0) = select(a_1387,X0)
| i29 = X0 ) ).
cnf(u5680,hypothesis,
( select(a_1388,X0) = select(a_1389,X0)
| i31 = X0 ) ).
cnf(u5697,hypothesis,
( select(a_1406,X0) = select(a_1407,X0)
| i6 = X0 ) ).
cnf(u5654,hypothesis,
( select(a_1362,X0) = select(a_1363,X0)
| i5 = X0 ) ).
cnf(u5713,hypothesis,
( select(a_1422,X0) = select(a_1423,X0)
| i33 = X0 ) ).
cnf(u5699,hypothesis,
( select(a_1408,X0) = select(a_1409,X0)
| i37 = X0 ) ).
cnf(u5716,hypothesis,
( select(a_1425,X0) = select(a_1426,X0)
| i38 = X0 ) ).
cnf(u5720,hypothesis,
( select(a_1429,X0) = select(a_1430,X0)
| i3 = X0 ) ).
cnf(u5724,hypothesis,
( select(a_1433,X0) = select(a_1434,X0)
| i15 = X0 ) ).
cnf(u5673,hypothesis,
( select(a_1381,X0) = select(a_1382,X0)
| i24 = X0 ) ).
cnf(u5717,hypothesis,
( select(a_1426,X0) = select(a_1427,X0)
| i39 = X0 ) ).
cnf(u5649,hypothesis,
( select(a_1359,X0) = select(a_1360,X0)
| i2 = X0 ) ).
cnf(u5658,hypothesis,
( select(a_1366,X0) = select(a_1367,X0)
| i9 = X0 ) ).
cnf(u5668,hypothesis,
( select(a_1376,X0) = select(a_1377,X0)
| i19 = X0 ) ).
cnf(u5685,hypothesis,
( select(a_1393,X0) = select(a_1394,X0)
| i36 = X0 ) ).
cnf(u5695,hypothesis,
( select(a_1404,X0) = select(a_1405,X0)
| i7 = X0 ) ).
cnf(u5689,hypothesis,
( select(a_1397,X0) = select(a_1398,X0)
| i40 = X0 ) ).
cnf(u5702,hypothesis,
( select(a_1411,X0) = select(a_1412,X0)
| i12 = X0 ) ).
cnf(u5714,hypothesis,
( select(a_1423,X0) = select(a_1424,X0)
| i2 = X0 ) ).
cnf(u5698,hypothesis,
( select(a_1407,X0) = select(a_1408,X0)
| i18 = X0 ) ).
cnf(u5722,hypothesis,
( select(a_1431,X0) = select(a_1432,X0)
| i4 = X0 ) ).
cnf(u5679,hypothesis,
( select(a_1387,X0) = select(a_1388,X0)
| i30 = X0 ) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWV497-1.040 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.08/0.18 % Computer : n011.cluster.edu
% 0.08/0.18 % Model : x86_64 x86_64
% 0.08/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.18 % Memory : 8046.5625MB
% 0.08/0.18 % OS : Linux 6.8.0-71-generic
% 0.08/0.18 % CPULimit : 300
% 0.08/0.18 % WCLimit : 300
% 0.08/0.18 % DateTime : Mon Sep 28 11:16:37 UTC 2026
% 0.08/0.19 % CPUTime :
% 0.08/0.19 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.08/0.22 Running first-order theorem proving
% 0.08/0.22 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
% 6.45/1.76 % (3330877)Input is clausal, will run a generic CNF schedule.
% 6.45/1.76 % (3330884)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=1267676733:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 6.45/1.76 % (3330883)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=2669025283:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 6.45/1.76 % (3330882)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=477407043:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 6.45/1.76 % (3330887)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=4274138051:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 6.45/1.76 % (3330885)lrs+10_1_sil=8000:sp=occurrence:random_seed=3627344928:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 6.45/1.76 % (3330886)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=2099340706:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 6.45/1.76 % (3330888)dis-21_1_sil=8000:lcm=predicate:random_seed=186192555: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.45/1.76 % (3330885)Refutation not found, incomplete strategy
% 6.45/1.76 % (3330885)------------------------------
% 6.45/1.76 % (3330885)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.45/1.76 % (3330885)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.45/1.76 % (3330885)CaDiCaL version: 2.1.3
% 6.45/1.76 % (3330885)Termination reason: Refutation not found, incomplete strategy
% 6.45/1.76 % (3330885)Time elapsed: 0.013 s
% 6.45/1.76 % (3330885)Peak memory usage: 88 MB
% 6.45/1.76 % (3330885)Instructions burned: 28 (million)
% 6.45/1.76 % (3330888)Refutation not found, incomplete strategy
% 6.45/1.76 % (3330888)------------------------------
% 6.45/1.76 % (3330888)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.45/1.76 % (3330888)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.45/1.76 % (3330888)CaDiCaL version: 2.1.3
% 6.45/1.76 % (3330888)Termination reason: Refutation not found, incomplete strategy
% 6.45/1.76 % (3330888)Time elapsed: 0.021 s
% 6.45/1.76 % (3330888)Peak memory usage: 89 MB
% 6.45/1.76 % (3330888)Instructions burned: 42 (million)
% 6.45/1.76 % (3330887)Refutation not found, incomplete strategy
% 6.45/1.76 % (3330887)------------------------------
% 6.45/1.76 % (3330887)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.45/1.76 % (3330887)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.45/1.76 % (3330887)CaDiCaL version: 2.1.3
% 6.45/1.76 % (3330887)Termination reason: Refutation not found, incomplete strategy
% 6.45/1.76 % (3330887)Time elapsed: 0.029 s
% 6.45/1.76 % (3330887)Peak memory usage: 88 MB
% 6.45/1.76 % (3330887)Instructions burned: 59 (million)
% 6.45/1.76 % (3330886)Refutation not found, incomplete strategy
% 6.45/1.76 % (3330886)------------------------------
% 6.45/1.76 % (3330886)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.45/1.76 % (3330886)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.45/1.76 % (3330886)CaDiCaL version: 2.1.3
% 6.45/1.76 % (3330886)Termination reason: Refutation not found, incomplete strategy
% 6.45/1.76 % (3330886)Time elapsed: 0.032 s
% 6.45/1.76 % (3330886)Peak memory usage: 88 MB
% 6.45/1.76 % (3330886)Instructions burned: 67 (million)
% 6.45/1.76 % (3330885)------------------------------
% 6.45/1.76 % (3330885)------------------------------
% 6.45/1.76 % (3330888)------------------------------
% 6.45/1.76 % (3330888)------------------------------
% 6.45/1.76 % (3330887)------------------------------
% 6.45/1.76 % (3330887)------------------------------
% 6.45/1.76 % (3330886)------------------------------
% 6.45/1.76 % (3330886)------------------------------
% 6.45/1.76 % (3330897)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=2398317222: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.45/1.76 % (3330896)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=2561869268:i=143:sd=2:aac=none:ss=axioms:sgt=16_2995 on theBenchmark for (2995ds/143Mi)
% 6.45/1.76 % (3330896)Refutation not found, incomplete strategy
% 6.45/1.76 % (3330896)------------------------------
% 6.45/1.76 % (3330896)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.45/1.76 % (3330896)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.45/1.76 % (3330896)CaDiCaL version: 2.1.3
% 6.45/1.76 % (3330896)Termination reason: Refutation not found, incomplete strategy
% 6.45/1.76 % (3330896)Time elapsed: 0.018 s
% 6.45/1.76 % (3330896)Peak memory usage: 88 MB
% 6.45/1.76 % (3330896)Instructions burned: 34 (million)
% 6.45/1.76 % (3330898)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=2275710731:st=4:i=219:sd=3:ss=axioms_2995 on theBenchmark for (2995ds/219Mi)
% 6.45/1.76 % (3330899)lrs+10_64_to=lpo:sil=8000:random_seed=922771629:i=126:bd=preordered_2995 on theBenchmark for (2995ds/126Mi)
% 6.45/1.76 % (3330898)Refutation not found, incomplete strategy
% 6.45/1.76 % (3330898)------------------------------
% 6.45/1.76 % (3330898)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.45/1.76 % (3330898)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.45/1.76 % (3330898)CaDiCaL version: 2.1.3
% 6.45/1.76 % (3330898)Termination reason: Refutation not found, incomplete strategy
% 6.45/1.76 % (3330898)Time elapsed: 0.016 s
% 6.45/1.76 % (3330898)Peak memory usage: 88 MB
% 6.45/1.76 % (3330898)Instructions burned: 35 (million)
% 6.45/1.76 % (3330897)Refutation not found, incomplete strategy
% 6.45/1.76 % (3330897)------------------------------
% 6.45/1.76 % (3330897)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.45/1.76 % (3330897)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.45/1.76 % (3330897)CaDiCaL version: 2.1.3
% 6.45/1.76 % (3330897)Termination reason: Refutation not found, incomplete strategy
% 6.45/1.76 % (3330897)Time elapsed: 0.041 s
% 6.45/1.76 % (3330897)Peak memory usage: 89 MB
% 6.45/1.76 % (3330897)Instructions burned: 88 (million)
% 6.45/1.76 % (3330884)Refutation not found, incomplete strategy
% 6.45/1.76 % (3330884)------------------------------
% 6.45/1.76 % (3330884)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.45/1.76 % (3330884)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.45/1.76 % (3330884)CaDiCaL version: 2.1.3
% 6.45/1.76 % (3330884)Termination reason: Refutation not found, incomplete strategy
% 6.45/1.76 % (3330884)Time elapsed: 0.493 s
% 6.45/1.76 % (3330884)Peak memory usage: 136 MB
% 6.45/1.76 % (3330884)Instructions burned: 1197 (million)
% 6.45/1.76 % (3330899)Instruction limit reached!
% 6.45/1.76 % (3330899)------------------------------
% 6.45/1.76 % (3330899)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.45/1.76 % (3330899)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.45/1.76 % (3330899)CaDiCaL version: 2.1.3
% 6.45/1.76 % (3330899)Termination reason: Instruction limit
% 6.45/1.76 % (3330899)Termination phase: Saturation
% 6.45/1.76 % (3330899)Time elapsed: 0.058 s
% 6.45/1.76 % (3330899)Peak memory usage: 88 MB
% 6.45/1.76 % (3330899)Instructions burned: 128 (million)
% 6.45/1.76 % (3330884)------------------------------
% 6.45/1.76 % (3330884)------------------------------
% 6.45/1.76 % (3330904)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=3075617973:avsq=on:i=194:fgj=on:bd=preordered_2993 on theBenchmark for (2993ds/194Mi)
% 6.45/1.76 % (3330904)Refutation not found, incomplete strategy
% 6.45/1.76 % (3330904)------------------------------
% 6.45/1.76 % (3330904)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.45/1.76 % (3330904)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.45/1.76 % (3330904)CaDiCaL version: 2.1.3
% 6.45/1.76 % (3330904)Termination reason: Refutation not found, incomplete strategy
% 6.45/1.76 % (3330904)Time elapsed: 0.026 s
% 6.45/1.76 % (3330904)Peak memory usage: 88 MB
% 6.45/1.76 % (3330904)Instructions burned: 54 (million)
% 6.45/1.76 % (3330896)------------------------------
% 6.45/1.76 % (3330896)------------------------------
% 6.45/1.76 % (3330897)------------------------------
% 6.45/1.76 % (3330897)------------------------------
% 6.45/1.76 % (3330898)------------------------------
% 6.45/1.76 % (3330898)------------------------------
% 6.45/1.76 % (3330905)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=822349434:i=157:gtg=all_2992 on theBenchmark for (2992ds/157Mi)
% 6.45/1.76 % (3330882)Refutation not found, incomplete strategy
% 6.45/1.76 % (3330882)------------------------------
% 6.45/1.76 % (3330882)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.45/1.76 % (3330882)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.45/1.76 % (3330882)CaDiCaL version: 2.1.3
% 6.45/1.76 % (3330882)Termination reason: Refutation not found, incomplete strategy
% 6.45/1.76 % (3330882)Time elapsed: 0.759 s
% 6.45/1.76 % (3330882)Peak memory usage: 135 MB
% 6.45/1.76 % (3330882)Instructions burned: 1185 (million)
% 6.45/1.76 % (3330905)First to succeed.
% 6.45/1.76 % (3330905)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-3330877"
% 6.45/1.76 % (3330907)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=2066982621:i=3394:sd=4:ss=included:sgt=64_2991 on theBenchmark for (2991ds/3394Mi)
% 6.45/1.76 % (3330908)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=3251963829:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2991 on theBenchmark for (2991ds/106Mi)
% 6.45/1.76 % (3330909)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=265716928:i=107_2991 on theBenchmark for (2991ds/107Mi)
% 6.45/1.76 % (3330908)Refutation not found, incomplete strategy
% 6.45/1.76 % (3330908)------------------------------
% 6.45/1.76 % (3330908)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.45/1.76 % (3330908)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.45/1.76 % (3330908)CaDiCaL version: 2.1.3
% 6.45/1.76 % (3330908)Termination reason: Refutation not found, incomplete strategy
% 6.45/1.76 % (3330908)Time elapsed: 0.023 s
% 6.45/1.76 % (3330908)Peak memory usage: 88 MB
% 6.45/1.76 % (3330908)Instructions burned: 46 (million)
% 6.45/1.76 % (3330909)Refutation not found, incomplete strategy
% 6.45/1.76 % (3330909)------------------------------
% 6.45/1.76 % (3330909)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.45/1.76 % (3330909)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.45/1.76 % (3330909)CaDiCaL version: 2.1.3
% 6.45/1.76 % (3330909)Termination reason: Refutation not found, incomplete strategy
% 6.45/1.76 % (3330909)Time elapsed: 0.023 s
% 6.45/1.76 % (3330909)Peak memory usage: 88 MB
% 6.45/1.76 % (3330909)Instructions burned: 46 (million)
% 6.45/1.76 % (3330904)------------------------------
% 6.45/1.76 % (3330904)------------------------------
% 6.45/1.76 % SZS status Satisfiable for theBenchmark
% 6.45/1.76 % SZS output start Saturation.
% See solution above
% 8.31/1.96 % SZS output start Definitions and Model Updates.
% 8.31/1.96 % SZS output end Definitions and Model Updates.
% 8.31/1.96 % (3330905)------------------------------
% 8.31/1.96 % (3330905)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.31/1.96 % (3330905)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.31/1.96 % (3330905)CaDiCaL version: 2.1.3
% 8.31/1.96 % (3330905)Termination reason: Satisfiable
% 8.31/1.96 % (3330905)Time elapsed: 0.040 s
% 8.31/1.96 % (3330905)Peak memory usage: 91 MB
% 8.31/1.96 % (3330905)Instructions burned: 73 (million)
% 8.31/1.96 % (3330905)------------------------------
% 8.31/1.96 % (3330905)------------------------------
% 8.31/1.96 % (3330877)Success in time 1.1 s
% 8.31/1.96 % Vampire exiting
%------------------------------------------------------------------------------