%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SWV497-1.030 : 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 : n004.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.31s 1.69s
% Output : Saturation 7.84s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(u502,negated_conjecture,
a_1047 != a_1077 ).
cnf(u507,hypothesis,
i1 != i2 ).
cnf(u512,hypothesis,
i1 != i3 ).
cnf(u517,hypothesis,
i1 != i4 ).
cnf(u522,hypothesis,
i1 != i5 ).
cnf(u527,hypothesis,
i1 != i6 ).
cnf(u532,hypothesis,
i1 != i7 ).
cnf(u537,hypothesis,
i1 != i8 ).
cnf(u542,hypothesis,
i1 != i9 ).
cnf(u547,hypothesis,
i1 != i10 ).
cnf(u552,hypothesis,
i1 != i11 ).
cnf(u557,hypothesis,
i1 != i12 ).
cnf(u562,hypothesis,
i1 != i13 ).
cnf(u567,hypothesis,
i1 != i14 ).
cnf(u572,hypothesis,
i1 != i15 ).
cnf(u577,hypothesis,
i1 != i16 ).
cnf(u582,hypothesis,
i1 != i17 ).
cnf(u587,hypothesis,
i1 != i18 ).
cnf(u592,hypothesis,
i1 != i19 ).
cnf(u597,hypothesis,
i1 != i20 ).
cnf(u602,hypothesis,
i1 != i21 ).
cnf(u607,hypothesis,
i1 != i22 ).
cnf(u612,hypothesis,
i1 != i23 ).
cnf(u617,hypothesis,
i1 != i24 ).
cnf(u622,hypothesis,
i1 != i25 ).
cnf(u627,hypothesis,
i1 != i26 ).
cnf(u632,hypothesis,
i1 != i27 ).
cnf(u637,hypothesis,
i1 != i28 ).
cnf(u642,hypothesis,
i1 != i29 ).
cnf(u647,hypothesis,
i1 != i30 ).
cnf(u652,hypothesis,
i2 != i3 ).
cnf(u657,hypothesis,
i2 != i4 ).
cnf(u662,hypothesis,
i2 != i5 ).
cnf(u667,hypothesis,
i2 != i6 ).
cnf(u672,hypothesis,
i2 != i7 ).
cnf(u677,hypothesis,
i2 != i8 ).
cnf(u682,hypothesis,
i2 != i9 ).
cnf(u687,hypothesis,
i2 != i10 ).
cnf(u692,hypothesis,
i2 != i11 ).
cnf(u697,hypothesis,
i2 != i12 ).
cnf(u702,hypothesis,
i2 != i13 ).
cnf(u707,hypothesis,
i2 != i14 ).
cnf(u712,hypothesis,
i2 != i15 ).
cnf(u717,hypothesis,
i2 != i16 ).
cnf(u722,hypothesis,
i2 != i17 ).
cnf(u727,hypothesis,
i2 != i18 ).
cnf(u732,hypothesis,
i2 != i19 ).
cnf(u737,hypothesis,
i2 != i20 ).
cnf(u742,hypothesis,
i2 != i21 ).
cnf(u747,hypothesis,
i2 != i22 ).
cnf(u752,hypothesis,
i2 != i23 ).
cnf(u757,hypothesis,
i2 != i24 ).
cnf(u762,hypothesis,
i2 != i25 ).
cnf(u767,hypothesis,
i2 != i26 ).
cnf(u772,hypothesis,
i2 != i27 ).
cnf(u777,hypothesis,
i2 != i28 ).
cnf(u782,hypothesis,
i2 != i29 ).
cnf(u787,hypothesis,
i2 != i30 ).
cnf(u792,hypothesis,
i3 != i4 ).
cnf(u797,hypothesis,
i3 != i5 ).
cnf(u802,hypothesis,
i3 != i6 ).
cnf(u807,hypothesis,
i3 != i7 ).
cnf(u812,hypothesis,
i3 != i8 ).
cnf(u817,hypothesis,
i3 != i9 ).
cnf(u822,hypothesis,
i3 != i10 ).
cnf(u827,hypothesis,
i3 != i11 ).
cnf(u832,hypothesis,
i3 != i12 ).
cnf(u837,hypothesis,
i3 != i13 ).
cnf(u842,hypothesis,
i3 != i14 ).
cnf(u847,hypothesis,
i3 != i15 ).
cnf(u852,hypothesis,
i3 != i16 ).
cnf(u857,hypothesis,
i3 != i17 ).
cnf(u862,hypothesis,
i3 != i18 ).
cnf(u867,hypothesis,
i3 != i19 ).
cnf(u872,hypothesis,
i3 != i20 ).
cnf(u877,hypothesis,
i3 != i21 ).
cnf(u882,hypothesis,
i3 != i22 ).
cnf(u887,hypothesis,
i3 != i23 ).
cnf(u892,hypothesis,
i3 != i24 ).
cnf(u897,hypothesis,
i3 != i25 ).
cnf(u902,hypothesis,
i3 != i26 ).
cnf(u907,hypothesis,
i3 != i27 ).
cnf(u912,hypothesis,
i3 != i28 ).
cnf(u917,hypothesis,
i3 != i29 ).
cnf(u922,hypothesis,
i3 != i30 ).
cnf(u927,hypothesis,
i4 != i5 ).
cnf(u932,hypothesis,
i4 != i6 ).
cnf(u937,hypothesis,
i4 != i7 ).
cnf(u942,hypothesis,
i4 != i8 ).
cnf(u947,hypothesis,
i4 != i9 ).
cnf(u952,hypothesis,
i4 != i10 ).
cnf(u957,hypothesis,
i4 != i11 ).
cnf(u962,hypothesis,
i4 != i12 ).
cnf(u967,hypothesis,
i4 != i13 ).
cnf(u972,hypothesis,
i4 != i14 ).
cnf(u977,hypothesis,
i4 != i15 ).
cnf(u982,hypothesis,
i4 != i16 ).
cnf(u987,hypothesis,
i4 != i17 ).
cnf(u992,hypothesis,
i4 != i18 ).
cnf(u997,hypothesis,
i4 != i19 ).
cnf(u1002,hypothesis,
i4 != i20 ).
cnf(u1007,hypothesis,
i4 != i21 ).
cnf(u1012,hypothesis,
i4 != i22 ).
cnf(u1017,hypothesis,
i4 != i23 ).
cnf(u1022,hypothesis,
i4 != i24 ).
cnf(u1027,hypothesis,
i4 != i25 ).
cnf(u1032,hypothesis,
i4 != i26 ).
cnf(u1037,hypothesis,
i4 != i27 ).
cnf(u1042,hypothesis,
i4 != i28 ).
cnf(u1047,hypothesis,
i4 != i29 ).
cnf(u1052,hypothesis,
i4 != i30 ).
cnf(u1057,hypothesis,
i5 != i6 ).
cnf(u1062,hypothesis,
i5 != i7 ).
cnf(u1067,hypothesis,
i5 != i8 ).
cnf(u1072,hypothesis,
i5 != i9 ).
cnf(u1077,hypothesis,
i5 != i10 ).
cnf(u1082,hypothesis,
i5 != i11 ).
cnf(u1087,hypothesis,
i5 != i12 ).
cnf(u1092,hypothesis,
i5 != i13 ).
cnf(u1097,hypothesis,
i5 != i14 ).
cnf(u1102,hypothesis,
i5 != i15 ).
cnf(u1107,hypothesis,
i5 != i16 ).
cnf(u1112,hypothesis,
i5 != i17 ).
cnf(u1117,hypothesis,
i5 != i18 ).
cnf(u1122,hypothesis,
i5 != i19 ).
cnf(u1127,hypothesis,
i5 != i20 ).
cnf(u1132,hypothesis,
i5 != i21 ).
cnf(u1137,hypothesis,
i5 != i22 ).
cnf(u1142,hypothesis,
i5 != i23 ).
cnf(u1147,hypothesis,
i5 != i24 ).
cnf(u1152,hypothesis,
i5 != i25 ).
cnf(u1157,hypothesis,
i5 != i26 ).
cnf(u1162,hypothesis,
i5 != i27 ).
cnf(u1167,hypothesis,
i5 != i28 ).
cnf(u1172,hypothesis,
i5 != i29 ).
cnf(u1177,hypothesis,
i5 != i30 ).
cnf(u1182,hypothesis,
i6 != i7 ).
cnf(u1187,hypothesis,
i6 != i8 ).
cnf(u1192,hypothesis,
i6 != i9 ).
cnf(u1197,hypothesis,
i6 != i10 ).
cnf(u1202,hypothesis,
i6 != i11 ).
cnf(u1207,hypothesis,
i6 != i12 ).
cnf(u1212,hypothesis,
i6 != i13 ).
cnf(u1217,hypothesis,
i6 != i14 ).
cnf(u1222,hypothesis,
i6 != i15 ).
cnf(u1227,hypothesis,
i6 != i16 ).
cnf(u1232,hypothesis,
i6 != i17 ).
cnf(u1237,hypothesis,
i6 != i18 ).
cnf(u1242,hypothesis,
i6 != i19 ).
cnf(u1247,hypothesis,
i6 != i20 ).
cnf(u1252,hypothesis,
i6 != i21 ).
cnf(u1257,hypothesis,
i6 != i22 ).
cnf(u1262,hypothesis,
i6 != i23 ).
cnf(u1267,hypothesis,
i6 != i24 ).
cnf(u1272,hypothesis,
i6 != i25 ).
cnf(u1277,hypothesis,
i6 != i26 ).
cnf(u1282,hypothesis,
i6 != i27 ).
cnf(u1287,hypothesis,
i6 != i28 ).
cnf(u1292,hypothesis,
i6 != i29 ).
cnf(u1297,hypothesis,
i6 != i30 ).
cnf(u1302,hypothesis,
i7 != i8 ).
cnf(u1307,hypothesis,
i7 != i9 ).
cnf(u1312,hypothesis,
i7 != i10 ).
cnf(u1317,hypothesis,
i7 != i11 ).
cnf(u1322,hypothesis,
i7 != i12 ).
cnf(u1327,hypothesis,
i7 != i13 ).
cnf(u1332,hypothesis,
i7 != i14 ).
cnf(u1337,hypothesis,
i7 != i15 ).
cnf(u1342,hypothesis,
i7 != i16 ).
cnf(u1347,hypothesis,
i7 != i17 ).
cnf(u1352,hypothesis,
i7 != i18 ).
cnf(u1357,hypothesis,
i7 != i19 ).
cnf(u1362,hypothesis,
i7 != i20 ).
cnf(u1367,hypothesis,
i7 != i21 ).
cnf(u1372,hypothesis,
i7 != i22 ).
cnf(u1377,hypothesis,
i7 != i23 ).
cnf(u1382,hypothesis,
i7 != i24 ).
cnf(u1387,hypothesis,
i7 != i25 ).
cnf(u1392,hypothesis,
i7 != i26 ).
cnf(u1397,hypothesis,
i7 != i27 ).
cnf(u1402,hypothesis,
i7 != i28 ).
cnf(u1407,hypothesis,
i7 != i29 ).
cnf(u1412,hypothesis,
i7 != i30 ).
cnf(u1417,hypothesis,
i8 != i9 ).
cnf(u1422,hypothesis,
i8 != i10 ).
cnf(u1427,hypothesis,
i8 != i11 ).
cnf(u1432,hypothesis,
i8 != i12 ).
cnf(u1437,hypothesis,
i8 != i13 ).
cnf(u1442,hypothesis,
i8 != i14 ).
cnf(u1447,hypothesis,
i8 != i15 ).
cnf(u1452,hypothesis,
i8 != i16 ).
cnf(u1457,hypothesis,
i8 != i17 ).
cnf(u1462,hypothesis,
i8 != i18 ).
cnf(u1467,hypothesis,
i8 != i19 ).
cnf(u1472,hypothesis,
i8 != i20 ).
cnf(u1477,hypothesis,
i8 != i21 ).
cnf(u1482,hypothesis,
i8 != i22 ).
cnf(u1487,hypothesis,
i8 != i23 ).
cnf(u1492,hypothesis,
i8 != i24 ).
cnf(u1497,hypothesis,
i8 != i25 ).
cnf(u1502,hypothesis,
i8 != i26 ).
cnf(u1507,hypothesis,
i8 != i27 ).
cnf(u1512,hypothesis,
i8 != i28 ).
cnf(u1517,hypothesis,
i8 != i29 ).
cnf(u1522,hypothesis,
i8 != i30 ).
cnf(u1527,hypothesis,
i9 != i10 ).
cnf(u1532,hypothesis,
i9 != i11 ).
cnf(u1537,hypothesis,
i9 != i12 ).
cnf(u1542,hypothesis,
i9 != i13 ).
cnf(u1547,hypothesis,
i9 != i14 ).
cnf(u1552,hypothesis,
i9 != i15 ).
cnf(u1557,hypothesis,
i9 != i16 ).
cnf(u1562,hypothesis,
i9 != i17 ).
cnf(u1567,hypothesis,
i9 != i18 ).
cnf(u1572,hypothesis,
i9 != i19 ).
cnf(u1577,hypothesis,
i9 != i20 ).
cnf(u1582,hypothesis,
i9 != i21 ).
cnf(u1587,hypothesis,
i9 != i22 ).
cnf(u1592,hypothesis,
i9 != i23 ).
cnf(u1597,hypothesis,
i9 != i24 ).
cnf(u1602,hypothesis,
i9 != i25 ).
cnf(u1607,hypothesis,
i9 != i26 ).
cnf(u1612,hypothesis,
i9 != i27 ).
cnf(u1617,hypothesis,
i9 != i28 ).
cnf(u1622,hypothesis,
i9 != i29 ).
cnf(u1627,hypothesis,
i9 != i30 ).
cnf(u1632,hypothesis,
i10 != i11 ).
cnf(u1637,hypothesis,
i10 != i12 ).
cnf(u1642,hypothesis,
i10 != i13 ).
cnf(u1647,hypothesis,
i10 != i14 ).
cnf(u1652,hypothesis,
i10 != i15 ).
cnf(u1657,hypothesis,
i10 != i16 ).
cnf(u1662,hypothesis,
i10 != i17 ).
cnf(u1667,hypothesis,
i10 != i18 ).
cnf(u1672,hypothesis,
i10 != i19 ).
cnf(u1677,hypothesis,
i10 != i20 ).
cnf(u1682,hypothesis,
i10 != i21 ).
cnf(u1687,hypothesis,
i10 != i22 ).
cnf(u1692,hypothesis,
i10 != i23 ).
cnf(u1697,hypothesis,
i10 != i24 ).
cnf(u1702,hypothesis,
i10 != i25 ).
cnf(u1707,hypothesis,
i10 != i26 ).
cnf(u1712,hypothesis,
i10 != i27 ).
cnf(u1717,hypothesis,
i10 != i28 ).
cnf(u1722,hypothesis,
i10 != i29 ).
cnf(u1727,hypothesis,
i10 != i30 ).
cnf(u1732,hypothesis,
i11 != i12 ).
cnf(u1737,hypothesis,
i11 != i13 ).
cnf(u1742,hypothesis,
i11 != i14 ).
cnf(u1747,hypothesis,
i11 != i15 ).
cnf(u1752,hypothesis,
i11 != i16 ).
cnf(u1757,hypothesis,
i11 != i17 ).
cnf(u1762,hypothesis,
i11 != i18 ).
cnf(u1767,hypothesis,
i11 != i19 ).
cnf(u1772,hypothesis,
i11 != i20 ).
cnf(u1777,hypothesis,
i11 != i21 ).
cnf(u1782,hypothesis,
i11 != i22 ).
cnf(u1787,hypothesis,
i11 != i23 ).
cnf(u1792,hypothesis,
i11 != i24 ).
cnf(u1797,hypothesis,
i11 != i25 ).
cnf(u1802,hypothesis,
i11 != i26 ).
cnf(u1807,hypothesis,
i11 != i27 ).
cnf(u1812,hypothesis,
i11 != i28 ).
cnf(u1817,hypothesis,
i11 != i29 ).
cnf(u1822,hypothesis,
i11 != i30 ).
cnf(u1827,hypothesis,
i12 != i13 ).
cnf(u1832,hypothesis,
i12 != i14 ).
cnf(u1837,hypothesis,
i12 != i15 ).
cnf(u1842,hypothesis,
i12 != i16 ).
cnf(u1847,hypothesis,
i12 != i17 ).
cnf(u1852,hypothesis,
i12 != i18 ).
cnf(u1857,hypothesis,
i12 != i19 ).
cnf(u1862,hypothesis,
i12 != i20 ).
cnf(u1867,hypothesis,
i12 != i21 ).
cnf(u1872,hypothesis,
i12 != i22 ).
cnf(u1877,hypothesis,
i12 != i23 ).
cnf(u1882,hypothesis,
i12 != i24 ).
cnf(u1887,hypothesis,
i12 != i25 ).
cnf(u1892,hypothesis,
i12 != i26 ).
cnf(u1897,hypothesis,
i12 != i27 ).
cnf(u1902,hypothesis,
i12 != i28 ).
cnf(u1907,hypothesis,
i12 != i29 ).
cnf(u1912,hypothesis,
i12 != i30 ).
cnf(u1917,hypothesis,
i13 != i14 ).
cnf(u1922,hypothesis,
i13 != i15 ).
cnf(u1927,hypothesis,
i13 != i16 ).
cnf(u1932,hypothesis,
i13 != i17 ).
cnf(u1937,hypothesis,
i13 != i18 ).
cnf(u1942,hypothesis,
i13 != i19 ).
cnf(u1947,hypothesis,
i13 != i20 ).
cnf(u1952,hypothesis,
i13 != i21 ).
cnf(u1957,hypothesis,
i13 != i22 ).
cnf(u1962,hypothesis,
i13 != i23 ).
cnf(u1967,hypothesis,
i13 != i24 ).
cnf(u1972,hypothesis,
i13 != i25 ).
cnf(u1977,hypothesis,
i13 != i26 ).
cnf(u1982,hypothesis,
i13 != i27 ).
cnf(u1987,hypothesis,
i13 != i28 ).
cnf(u1992,hypothesis,
i13 != i29 ).
cnf(u1997,hypothesis,
i13 != i30 ).
cnf(u2002,hypothesis,
i14 != i15 ).
cnf(u2007,hypothesis,
i14 != i16 ).
cnf(u2012,hypothesis,
i14 != i17 ).
cnf(u2017,hypothesis,
i14 != i18 ).
cnf(u2022,hypothesis,
i14 != i19 ).
cnf(u2027,hypothesis,
i14 != i20 ).
cnf(u2032,hypothesis,
i14 != i21 ).
cnf(u2037,hypothesis,
i14 != i22 ).
cnf(u2042,hypothesis,
i14 != i23 ).
cnf(u2047,hypothesis,
i14 != i24 ).
cnf(u2052,hypothesis,
i14 != i25 ).
cnf(u2057,hypothesis,
i14 != i26 ).
cnf(u2062,hypothesis,
i14 != i27 ).
cnf(u2067,hypothesis,
i14 != i28 ).
cnf(u2072,hypothesis,
i14 != i29 ).
cnf(u2077,hypothesis,
i14 != i30 ).
cnf(u2082,hypothesis,
i15 != i16 ).
cnf(u2087,hypothesis,
i15 != i17 ).
cnf(u2092,hypothesis,
i15 != i18 ).
cnf(u2097,hypothesis,
i15 != i19 ).
cnf(u2102,hypothesis,
i15 != i20 ).
cnf(u2107,hypothesis,
i15 != i21 ).
cnf(u2112,hypothesis,
i15 != i22 ).
cnf(u2117,hypothesis,
i15 != i23 ).
cnf(u2122,hypothesis,
i15 != i24 ).
cnf(u2127,hypothesis,
i15 != i25 ).
cnf(u2132,hypothesis,
i15 != i26 ).
cnf(u2137,hypothesis,
i15 != i27 ).
cnf(u2142,hypothesis,
i15 != i28 ).
cnf(u2147,hypothesis,
i15 != i29 ).
cnf(u2152,hypothesis,
i15 != i30 ).
cnf(u2157,hypothesis,
i16 != i17 ).
cnf(u2162,hypothesis,
i16 != i18 ).
cnf(u2167,hypothesis,
i16 != i19 ).
cnf(u2172,hypothesis,
i16 != i20 ).
cnf(u2177,hypothesis,
i16 != i21 ).
cnf(u2182,hypothesis,
i16 != i22 ).
cnf(u2187,hypothesis,
i16 != i23 ).
cnf(u2192,hypothesis,
i16 != i24 ).
cnf(u2197,hypothesis,
i16 != i25 ).
cnf(u2202,hypothesis,
i16 != i26 ).
cnf(u2207,hypothesis,
i16 != i27 ).
cnf(u2212,hypothesis,
i16 != i28 ).
cnf(u2217,hypothesis,
i16 != i29 ).
cnf(u2222,hypothesis,
i16 != i30 ).
cnf(u2227,hypothesis,
i17 != i18 ).
cnf(u2232,hypothesis,
i17 != i19 ).
cnf(u2237,hypothesis,
i17 != i20 ).
cnf(u2242,hypothesis,
i17 != i21 ).
cnf(u2247,hypothesis,
i17 != i22 ).
cnf(u2252,hypothesis,
i17 != i23 ).
cnf(u2257,hypothesis,
i17 != i24 ).
cnf(u2262,hypothesis,
i17 != i25 ).
cnf(u2267,hypothesis,
i17 != i26 ).
cnf(u2272,hypothesis,
i17 != i27 ).
cnf(u2277,hypothesis,
i17 != i28 ).
cnf(u2282,hypothesis,
i17 != i29 ).
cnf(u2287,hypothesis,
i17 != i30 ).
cnf(u2292,hypothesis,
i18 != i19 ).
cnf(u2297,hypothesis,
i18 != i20 ).
cnf(u2302,hypothesis,
i18 != i21 ).
cnf(u2307,hypothesis,
i18 != i22 ).
cnf(u2312,hypothesis,
i18 != i23 ).
cnf(u2317,hypothesis,
i18 != i24 ).
cnf(u2322,hypothesis,
i18 != i25 ).
cnf(u2327,hypothesis,
i18 != i26 ).
cnf(u2332,hypothesis,
i18 != i27 ).
cnf(u2337,hypothesis,
i18 != i28 ).
cnf(u2342,hypothesis,
i18 != i29 ).
cnf(u2347,hypothesis,
i18 != i30 ).
cnf(u2352,hypothesis,
i19 != i20 ).
cnf(u2357,hypothesis,
i19 != i21 ).
cnf(u2362,hypothesis,
i19 != i22 ).
cnf(u2367,hypothesis,
i19 != i23 ).
cnf(u2372,hypothesis,
i19 != i24 ).
cnf(u2377,hypothesis,
i19 != i25 ).
cnf(u2382,hypothesis,
i19 != i26 ).
cnf(u2387,hypothesis,
i19 != i27 ).
cnf(u2392,hypothesis,
i19 != i28 ).
cnf(u2397,hypothesis,
i19 != i29 ).
cnf(u2402,hypothesis,
i19 != i30 ).
cnf(u2407,hypothesis,
i20 != i21 ).
cnf(u2412,hypothesis,
i20 != i22 ).
cnf(u2417,hypothesis,
i20 != i23 ).
cnf(u2422,hypothesis,
i20 != i24 ).
cnf(u2427,hypothesis,
i20 != i25 ).
cnf(u2432,hypothesis,
i20 != i26 ).
cnf(u2437,hypothesis,
i20 != i27 ).
cnf(u2442,hypothesis,
i20 != i28 ).
cnf(u2447,hypothesis,
i20 != i29 ).
cnf(u2452,hypothesis,
i20 != i30 ).
cnf(u2457,hypothesis,
i21 != i22 ).
cnf(u2462,hypothesis,
i21 != i23 ).
cnf(u2467,hypothesis,
i21 != i24 ).
cnf(u2472,hypothesis,
i21 != i25 ).
cnf(u2477,hypothesis,
i21 != i26 ).
cnf(u2482,hypothesis,
i21 != i27 ).
cnf(u2487,hypothesis,
i21 != i28 ).
cnf(u2492,hypothesis,
i21 != i29 ).
cnf(u2497,hypothesis,
i21 != i30 ).
cnf(u2502,hypothesis,
i22 != i23 ).
cnf(u2507,hypothesis,
i22 != i24 ).
cnf(u2512,hypothesis,
i22 != i25 ).
cnf(u2517,hypothesis,
i22 != i26 ).
cnf(u2522,hypothesis,
i22 != i27 ).
cnf(u2527,hypothesis,
i22 != i28 ).
cnf(u2532,hypothesis,
i22 != i29 ).
cnf(u2537,hypothesis,
i22 != i30 ).
cnf(u2542,hypothesis,
i23 != i24 ).
cnf(u2547,hypothesis,
i23 != i25 ).
cnf(u2552,hypothesis,
i23 != i26 ).
cnf(u2557,hypothesis,
i23 != i27 ).
cnf(u2562,hypothesis,
i23 != i28 ).
cnf(u2567,hypothesis,
i23 != i29 ).
cnf(u2572,hypothesis,
i23 != i30 ).
cnf(u2577,hypothesis,
i24 != i25 ).
cnf(u2582,hypothesis,
i24 != i26 ).
cnf(u2587,hypothesis,
i24 != i27 ).
cnf(u2592,hypothesis,
i24 != i28 ).
cnf(u2597,hypothesis,
i24 != i29 ).
cnf(u2602,hypothesis,
i24 != i30 ).
cnf(u2607,hypothesis,
i25 != i26 ).
cnf(u2612,hypothesis,
i25 != i27 ).
cnf(u2617,hypothesis,
i25 != i28 ).
cnf(u2622,hypothesis,
i25 != i29 ).
cnf(u2627,hypothesis,
i25 != i30 ).
cnf(u2632,hypothesis,
i26 != i27 ).
cnf(u2637,hypothesis,
i26 != i28 ).
cnf(u2642,hypothesis,
i26 != i29 ).
cnf(u2647,hypothesis,
i26 != i30 ).
cnf(u2652,hypothesis,
i27 != i28 ).
cnf(u2657,hypothesis,
i27 != i29 ).
cnf(u2662,hypothesis,
i27 != i30 ).
cnf(u2667,hypothesis,
i28 != i29 ).
cnf(u2672,hypothesis,
i28 != i30 ).
cnf(u2677,hypothesis,
i29 != i30 ).
cnf(u2682,hypothesis,
a_1077 = store(a_1076,i10,e10) ).
cnf(u2687,hypothesis,
a_1076 = store(a_1075,i7,e7) ).
cnf(u2692,hypothesis,
a_1075 = store(a_1074,i24,e24) ).
cnf(u2697,hypothesis,
a_1074 = store(a_1073,i23,e23) ).
cnf(u2702,hypothesis,
a_1073 = store(a_1072,i17,e17) ).
cnf(u2707,hypothesis,
a_1072 = store(a_1071,i28,e28) ).
cnf(u2712,hypothesis,
a_1071 = store(a_1070,i16,e16) ).
cnf(u2717,hypothesis,
a_1070 = store(a_1069,i12,e12) ).
cnf(u2722,hypothesis,
a_1069 = store(a_1068,i3,e3) ).
cnf(u2727,hypothesis,
a_1068 = store(a_1067,i27,e27) ).
cnf(u2732,hypothesis,
a_1067 = store(a_1066,i22,e22) ).
cnf(u2737,hypothesis,
a_1066 = store(a_1065,i26,e26) ).
cnf(u2742,hypothesis,
a_1065 = store(a_1064,i5,e5) ).
cnf(u2747,hypothesis,
a_1064 = store(a_1063,i29,e29) ).
cnf(u2752,hypothesis,
a_1063 = store(a_1062,i14,e14) ).
cnf(u2757,hypothesis,
a_1062 = store(a_1061,i11,e11) ).
cnf(u2762,hypothesis,
a_1061 = store(a_1060,i6,e6) ).
cnf(u2767,hypothesis,
a_1060 = store(a_1059,i21,e21) ).
cnf(u2772,hypothesis,
a_1059 = store(a_1058,i8,e8) ).
cnf(u2777,hypothesis,
a_1058 = store(a_1057,i20,e20) ).
cnf(u2782,hypothesis,
a_1057 = store(a_1056,i18,e18) ).
cnf(u2787,hypothesis,
a_1056 = store(a_1055,i25,e25) ).
cnf(u2792,hypothesis,
a_1055 = store(a_1054,i15,e15) ).
cnf(u2797,hypothesis,
a_1054 = store(a_1053,i2,e2) ).
cnf(u2802,hypothesis,
a_1053 = store(a_1052,i30,e30) ).
cnf(u2807,hypothesis,
a_1052 = store(a_1051,i9,e9) ).
cnf(u2812,hypothesis,
a_1051 = store(a_1050,i4,e4) ).
cnf(u2817,hypothesis,
a_1050 = store(a_1049,i19,e19) ).
cnf(u2822,hypothesis,
a_1049 = store(a_1048,i1,e1) ).
cnf(u2827,hypothesis,
a_1048 = store(a1,i13,e13) ).
cnf(u2832,hypothesis,
a_1047 = store(a_1046,i30,e30) ).
cnf(u2837,hypothesis,
a_1046 = store(a_1045,i29,e29) ).
cnf(u2842,hypothesis,
a_1045 = store(a_1044,i28,e28) ).
cnf(u2847,hypothesis,
a_1044 = store(a_1043,i27,e27) ).
cnf(u2852,hypothesis,
a_1043 = store(a_1042,i26,e26) ).
cnf(u2857,hypothesis,
a_1042 = store(a_1041,i25,e25) ).
cnf(u2862,hypothesis,
a_1041 = store(a_1040,i24,e24) ).
cnf(u2867,hypothesis,
a_1040 = store(a_1039,i23,e23) ).
cnf(u2872,hypothesis,
a_1039 = store(a_1038,i22,e22) ).
cnf(u2877,hypothesis,
a_1038 = store(a_1037,i21,e21) ).
cnf(u2882,hypothesis,
a_1037 = store(a_1036,i20,e20) ).
cnf(u2887,hypothesis,
a_1036 = store(a_1035,i19,e19) ).
cnf(u2892,hypothesis,
a_1035 = store(a_1034,i18,e18) ).
cnf(u2897,hypothesis,
a_1034 = store(a_1033,i17,e17) ).
cnf(u2902,hypothesis,
a_1033 = store(a_1032,i16,e16) ).
cnf(u2907,hypothesis,
a_1032 = store(a_1031,i15,e15) ).
cnf(u2912,hypothesis,
a_1031 = store(a_1030,i14,e14) ).
cnf(u2917,hypothesis,
a_1030 = store(a_1029,i13,e13) ).
cnf(u2922,hypothesis,
a_1029 = store(a_1028,i12,e12) ).
cnf(u2927,hypothesis,
a_1028 = store(a_1027,i11,e11) ).
cnf(u2932,hypothesis,
a_1027 = store(a_1026,i10,e10) ).
cnf(u2937,hypothesis,
a_1026 = store(a_1025,i9,e9) ).
cnf(u2942,hypothesis,
a_1025 = store(a_1024,i8,e8) ).
cnf(u2947,hypothesis,
a_1024 = store(a_1023,i7,e7) ).
cnf(u2952,hypothesis,
a_1023 = store(a_1022,i6,e6) ).
cnf(u2957,hypothesis,
a_1022 = store(a_1021,i5,e5) ).
cnf(u2962,hypothesis,
a_1021 = store(a_1020,i4,e4) ).
cnf(u2967,hypothesis,
a_1020 = store(a_1019,i3,e3) ).
cnf(u2972,hypothesis,
a_1019 = store(a_1018,i2,e2) ).
cnf(u2977,hypothesis,
a_1018 = store(a1,i1,e1) ).
cnf(u3042,hypothesis,
e10 = select(a_1077,i10) ).
cnf(u3047,hypothesis,
e7 = select(a_1076,i7) ).
cnf(u3052,hypothesis,
e24 = select(a_1075,i24) ).
cnf(u3057,hypothesis,
e23 = select(a_1074,i23) ).
cnf(u3062,hypothesis,
e17 = select(a_1073,i17) ).
cnf(u3067,hypothesis,
e28 = select(a_1072,i28) ).
cnf(u3072,hypothesis,
e16 = select(a_1071,i16) ).
cnf(u3077,hypothesis,
e12 = select(a_1070,i12) ).
cnf(u3082,hypothesis,
e3 = select(a_1069,i3) ).
cnf(u3087,hypothesis,
e27 = select(a_1068,i27) ).
cnf(u3092,hypothesis,
e22 = select(a_1067,i22) ).
cnf(u3097,hypothesis,
e26 = select(a_1066,i26) ).
cnf(u3102,hypothesis,
e5 = select(a_1065,i5) ).
cnf(u3107,hypothesis,
e29 = select(a_1064,i29) ).
cnf(u3112,hypothesis,
e14 = select(a_1063,i14) ).
cnf(u3117,hypothesis,
e11 = select(a_1062,i11) ).
cnf(u3122,hypothesis,
e6 = select(a_1061,i6) ).
cnf(u3127,hypothesis,
e21 = select(a_1060,i21) ).
cnf(u3132,hypothesis,
e8 = select(a_1059,i8) ).
cnf(u3137,hypothesis,
e20 = select(a_1058,i20) ).
cnf(u3142,hypothesis,
e18 = select(a_1057,i18) ).
cnf(u3147,hypothesis,
e25 = select(a_1056,i25) ).
cnf(u3152,hypothesis,
e15 = select(a_1055,i15) ).
cnf(u3157,hypothesis,
e2 = select(a_1054,i2) ).
cnf(u3162,hypothesis,
e30 = select(a_1053,i30) ).
cnf(u3167,hypothesis,
e9 = select(a_1052,i9) ).
cnf(u3172,hypothesis,
e4 = select(a_1051,i4) ).
cnf(u3177,hypothesis,
e19 = select(a_1050,i19) ).
cnf(u3182,hypothesis,
e1 = select(a_1049,i1) ).
cnf(u3187,hypothesis,
e30 = select(a_1047,i30) ).
cnf(u3192,hypothesis,
e29 = select(a_1046,i29) ).
cnf(u3197,hypothesis,
e28 = select(a_1045,i28) ).
cnf(u3202,hypothesis,
e27 = select(a_1044,i27) ).
cnf(u3207,hypothesis,
e26 = select(a_1043,i26) ).
cnf(u3212,hypothesis,
e25 = select(a_1042,i25) ).
cnf(u3217,hypothesis,
e24 = select(a_1041,i24) ).
cnf(u3222,hypothesis,
e23 = select(a_1040,i23) ).
cnf(u3227,hypothesis,
e22 = select(a_1039,i22) ).
cnf(u3232,hypothesis,
e21 = select(a_1038,i21) ).
cnf(u3237,hypothesis,
e20 = select(a_1037,i20) ).
cnf(u3242,hypothesis,
e19 = select(a_1036,i19) ).
cnf(u3247,hypothesis,
e18 = select(a_1035,i18) ).
cnf(u3252,hypothesis,
e17 = select(a_1034,i17) ).
cnf(u3257,hypothesis,
e16 = select(a_1033,i16) ).
cnf(u3262,hypothesis,
e15 = select(a_1032,i15) ).
cnf(u3267,hypothesis,
e14 = select(a_1031,i14) ).
cnf(u3272,hypothesis,
e13 = select(a_1030,i13) ).
cnf(u3277,hypothesis,
e12 = select(a_1029,i12) ).
cnf(u3282,hypothesis,
e11 = select(a_1028,i11) ).
cnf(u3287,hypothesis,
e10 = select(a_1027,i10) ).
cnf(u3292,hypothesis,
e9 = select(a_1026,i9) ).
cnf(u3297,hypothesis,
e8 = select(a_1025,i8) ).
cnf(u3302,hypothesis,
e7 = select(a_1024,i7) ).
cnf(u3307,hypothesis,
e6 = select(a_1023,i6) ).
cnf(u3312,hypothesis,
e5 = select(a_1022,i5) ).
cnf(u3317,hypothesis,
e4 = select(a_1021,i4) ).
cnf(u3322,hypothesis,
e3 = select(a_1020,i3) ).
cnf(u3327,hypothesis,
e1 = select(a_1018,i1) ).
cnf(u3332,hypothesis,
e13 = select(a_1048,i13) ).
cnf(u3337,hypothesis,
e2 = select(a_1019,i2) ).
cnf(u3359,hypothesis,
( select(a_1036,X0) = select(a_1037,X0)
| i20 = X0 ) ).
cnf(u3346,hypothesis,
( select(a_1023,X0) = select(a_1024,X0)
| i7 = X0 ) ).
cnf(u3345,hypothesis,
( select(a_1022,X0) = select(a_1023,X0)
| i6 = X0 ) ).
cnf(u3385,hypothesis,
( select(a_1063,X0) = select(a_1064,X0)
| i29 = X0 ) ).
cnf(u3379,hypothesis,
( select(a_1057,X0) = select(a_1058,X0)
| i20 = X0 ) ).
cnf(u3383,hypothesis,
( select(a_1061,X0) = select(a_1062,X0)
| i11 = X0 ) ).
cnf(u3372,hypothesis,
( select(a_1050,X0) = select(a_1051,X0)
| i4 = X0 ) ).
cnf(u3349,hypothesis,
( select(a_1026,X0) = select(a_1027,X0)
| i10 = X0 ) ).
cnf(u3365,hypothesis,
( select(a_1042,X0) = select(a_1043,X0)
| i26 = X0 ) ).
cnf(u3382,hypothesis,
( select(a_1060,X0) = select(a_1061,X0)
| i6 = X0 ) ).
cnf(u3360,hypothesis,
( select(a_1037,X0) = select(a_1038,X0)
| i21 = X0 ) ).
cnf(a2,axiom,
( select(store(X2,X0,X3),X1) = select(X2,X1)
| X0 = X1 ) ).
cnf(a1,axiom,
select(store(X0,X1,X2),X1) = X2 ).
cnf(u3354,hypothesis,
( select(a_1031,X0) = select(a_1032,X0)
| i15 = X0 ) ).
cnf(u3340,hypothesis,
( select(a1,X0) = select(a_1048,X0)
| i13 = X0 ) ).
cnf(u3363,hypothesis,
( select(a_1040,X0) = select(a_1041,X0)
| i24 = X0 ) ).
cnf(u3378,hypothesis,
( select(a_1056,X0) = select(a_1057,X0)
| i18 = X0 ) ).
cnf(u3377,hypothesis,
( select(a_1055,X0) = select(a_1056,X0)
| i25 = X0 ) ).
cnf(u3364,hypothesis,
( select(a_1041,X0) = select(a_1042,X0)
| i25 = X0 ) ).
cnf(u3358,hypothesis,
( select(a_1035,X0) = select(a_1036,X0)
| i19 = X0 ) ).
cnf(u3394,hypothesis,
( select(a_1072,X0) = select(a_1073,X0)
| i17 = X0 ) ).
cnf(u3388,hypothesis,
( select(a_1066,X0) = select(a_1067,X0)
| i22 = X0 ) ).
cnf(u3342,hypothesis,
( select(a_1019,X0) = select(a_1020,X0)
| i3 = X0 ) ).
cnf(u3386,hypothesis,
( select(a_1064,X0) = select(a_1065,X0)
| i5 = X0 ) ).
cnf(u3366,hypothesis,
( select(a_1043,X0) = select(a_1044,X0)
| i27 = X0 ) ).
cnf(u3395,hypothesis,
( select(a_1073,X0) = select(a_1074,X0)
| i23 = X0 ) ).
cnf(u3352,hypothesis,
( select(a_1029,X0) = select(a_1030,X0)
| i13 = X0 ) ).
cnf(u3387,hypothesis,
( select(a_1065,X0) = select(a_1066,X0)
| i26 = X0 ) ).
cnf(u3344,hypothesis,
( select(a_1021,X0) = select(a_1022,X0)
| i5 = X0 ) ).
cnf(u3376,hypothesis,
( select(a_1054,X0) = select(a_1055,X0)
| i15 = X0 ) ).
cnf(u3390,hypothesis,
( select(a_1068,X0) = select(a_1069,X0)
| i3 = X0 ) ).
cnf(u3389,hypothesis,
( select(a_1067,X0) = select(a_1068,X0)
| i27 = X0 ) ).
cnf(u3367,hypothesis,
( select(a_1044,X0) = select(a_1045,X0)
| i28 = X0 ) ).
cnf(u3353,hypothesis,
( select(a_1030,X0) = select(a_1031,X0)
| i14 = X0 ) ).
cnf(u3341,hypothesis,
( select(a_1018,X0) = select(a1,X0)
| i1 = X0 ) ).
cnf(u3392,hypothesis,
( select(a_1070,X0) = select(a_1071,X0)
| i16 = X0 ) ).
cnf(u3351,hypothesis,
( select(a_1028,X0) = select(a_1029,X0)
| i12 = X0 ) ).
cnf(u3396,hypothesis,
( select(a_1074,X0) = select(a_1075,X0)
| i24 = X0 ) ).
cnf(u3375,hypothesis,
( select(a_1053,X0) = select(a_1054,X0)
| i2 = X0 ) ).
cnf(u3361,hypothesis,
( select(a_1038,X0) = select(a_1039,X0)
| i22 = X0 ) ).
cnf(u3355,hypothesis,
( select(a_1032,X0) = select(a_1033,X0)
| i16 = X0 ) ).
cnf(u3393,hypothesis,
( select(a_1071,X0) = select(a_1072,X0)
| i28 = X0 ) ).
cnf(u3381,hypothesis,
( select(a_1059,X0) = select(a_1060,X0)
| i21 = X0 ) ).
cnf(u3368,hypothesis,
( select(a_1045,X0) = select(a_1046,X0)
| i29 = X0 ) ).
cnf(u3362,hypothesis,
( select(a_1039,X0) = select(a_1040,X0)
| i23 = X0 ) ).
cnf(u3397,hypothesis,
( select(a_1075,X0) = select(a_1076,X0)
| i7 = X0 ) ).
cnf(u3398,hypothesis,
( select(a_1076,X0) = select(a_1077,X0)
| i10 = X0 ) ).
cnf(u3370,hypothesis,
( select(a_1048,X0) = select(a_1049,X0)
| i1 = X0 ) ).
cnf(u3356,hypothesis,
( select(a_1033,X0) = select(a_1034,X0)
| i17 = X0 ) ).
cnf(u3369,hypothesis,
( select(a_1046,X0) = select(a_1047,X0)
| i30 = X0 ) ).
cnf(u3350,hypothesis,
( select(a_1027,X0) = select(a_1028,X0)
| i11 = X0 ) ).
cnf(u3348,hypothesis,
( select(a_1025,X0) = select(a_1026,X0)
| i9 = X0 ) ).
cnf(u3357,hypothesis,
( select(a_1034,X0) = select(a_1035,X0)
| i18 = X0 ) ).
cnf(u3347,hypothesis,
( select(a_1024,X0) = select(a_1025,X0)
| i8 = X0 ) ).
cnf(u3339,hypothesis,
( select(a_1018,X0) = select(a_1019,X0)
| i2 = X0 ) ).
cnf(u3371,hypothesis,
( select(a_1049,X0) = select(a_1050,X0)
| i19 = X0 ) ).
cnf(u3374,hypothesis,
( select(a_1052,X0) = select(a_1053,X0)
| i30 = X0 ) ).
cnf(u3343,hypothesis,
( select(a_1020,X0) = select(a_1021,X0)
| i4 = X0 ) ).
cnf(u3391,hypothesis,
( select(a_1069,X0) = select(a_1070,X0)
| i12 = X0 ) ).
cnf(u3384,hypothesis,
( select(a_1062,X0) = select(a_1063,X0)
| i14 = X0 ) ).
cnf(u3380,hypothesis,
( select(a_1058,X0) = select(a_1059,X0)
| i8 = X0 ) ).
cnf(u3373,hypothesis,
( select(a_1051,X0) = select(a_1052,X0)
| i9 = X0 ) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWV497-1.030 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.07/0.18 % Computer : n004.cluster.edu
% 0.07/0.18 % Model : x86_64 x86_64
% 0.07/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.18 % Memory : 8046.5625MB
% 0.07/0.18 % OS : Linux 6.8.0-71-generic
% 0.07/0.18 % CPULimit : 300
% 0.07/0.18 % WCLimit : 300
% 0.07/0.18 % DateTime : Mon Sep 28 11:16:22 UTC 2026
% 0.07/0.19 % CPUTime :
% 0.07/0.19 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.07/0.22 Running first-order theorem proving
% 0.07/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.31/1.69 % (290790)Input is clausal, will run a generic CNF schedule.
% 6.31/1.69 % (290799)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=1675014827:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 6.31/1.69 % (290799)Refutation not found, incomplete strategy
% 6.31/1.69 % (290799)------------------------------
% 6.31/1.69 % (290799)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.31/1.69 % (290799)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.31/1.69 % (290799)CaDiCaL version: 2.1.3
% 6.31/1.69 % (290799)Termination reason: Refutation not found, incomplete strategy
% 6.31/1.69 % (290799)Time elapsed: 0.010 s
% 6.31/1.69 % (290799)Peak memory usage: 88 MB
% 6.31/1.69 % (290799)Instructions burned: 37 (million)
% 6.31/1.69 % (290798)lrs+10_1_sil=8000:sp=occurrence:random_seed=3816856827:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 6.31/1.69 % (290796)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=3469940328:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 6.31/1.69 % (290795)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=3350534285:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 6.31/1.69 % (290797)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=1133289795:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 6.31/1.69 % (290798)Refutation not found, incomplete strategy
% 6.31/1.69 % (290798)------------------------------
% 6.31/1.69 % (290798)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.31/1.69 % (290798)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.31/1.69 % (290798)CaDiCaL version: 2.1.3
% 6.31/1.69 % (290798)Termination reason: Refutation not found, incomplete strategy
% 6.31/1.69 % (290798)Time elapsed: 0.009 s
% 6.31/1.69 % (290798)Peak memory usage: 88 MB
% 6.31/1.69 % (290798)Instructions burned: 17 (million)
% 6.31/1.69 % (290800)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=75638902:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 6.31/1.69 % (290801)dis-21_1_sil=8000:lcm=predicate:random_seed=2719153051: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.31/1.69 % (290801)Refutation not found, incomplete strategy
% 6.31/1.69 % (290801)------------------------------
% 6.31/1.69 % (290801)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.31/1.69 % (290801)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.31/1.69 % (290801)CaDiCaL version: 2.1.3
% 6.31/1.69 % (290801)Termination reason: Refutation not found, incomplete strategy
% 6.31/1.69 % (290801)Time elapsed: 0.012 s
% 6.31/1.69 % (290801)Peak memory usage: 88 MB
% 6.31/1.69 % (290801)Instructions burned: 23 (million)
% 6.31/1.69 % (290800)Refutation not found, incomplete strategy
% 6.31/1.69 % (290800)------------------------------
% 6.31/1.69 % (290800)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.31/1.69 % (290800)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.31/1.69 % (290800)CaDiCaL version: 2.1.3
% 6.31/1.69 % (290800)Termination reason: Refutation not found, incomplete strategy
% 6.31/1.69 % (290800)Time elapsed: 0.021 s
% 6.31/1.69 % (290800)Peak memory usage: 88 MB
% 6.31/1.69 % (290800)Instructions burned: 39 (million)
% 6.31/1.69 % (290799)------------------------------
% 6.31/1.69 % (290799)------------------------------
% 6.31/1.69 % (290809)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=580532605:i=143:sd=2:aac=none:ss=axioms:sgt=16_2997 on theBenchmark for (2997ds/143Mi)
% 6.31/1.69 % (290809)Refutation not found, incomplete strategy
% 6.31/1.69 % (290809)------------------------------
% 6.31/1.69 % (290809)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.31/1.69 % (290809)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.31/1.69 % (290809)CaDiCaL version: 2.1.3
% 6.31/1.69 % (290809)Termination reason: Refutation not found, incomplete strategy
% 6.31/1.69 % (290809)Time elapsed: 0.006 s
% 6.31/1.69 % (290809)Peak memory usage: 88 MB
% 6.31/1.69 % (290809)Instructions burned: 20 (million)
% 6.31/1.69 % (290798)------------------------------
% 6.31/1.69 % (290798)------------------------------
% 6.31/1.69 % (290801)------------------------------
% 6.31/1.69 % (290801)------------------------------
% 6.31/1.69 % (290800)------------------------------
% 6.31/1.69 % (290800)------------------------------
% 6.31/1.69 % (290811)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=18692827:st=3:avsq=on:s2a=on:i=189:s2at=1.2:avsqr=1,16:sd=2:bd=all:nm=64:ss=axioms:sgt=30_2996 on theBenchmark for (2996ds/189Mi)
% 6.31/1.69 % (290809)------------------------------
% 6.31/1.69 % (290809)------------------------------
% 6.31/1.69 % (290811)Refutation not found, incomplete strategy
% 6.31/1.69 % (290811)------------------------------
% 6.31/1.69 % (290811)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.31/1.69 % (290811)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.31/1.69 % (290811)CaDiCaL version: 2.1.3
% 6.31/1.69 % (290811)Termination reason: Refutation not found, incomplete strategy
% 6.31/1.69 % (290811)Time elapsed: 0.025 s
% 6.31/1.69 % (290811)Peak memory usage: 89 MB
% 6.31/1.69 % (290811)Instructions burned: 52 (million)
% 6.31/1.69 % (290813)lrs+10_64_to=lpo:sil=8000:random_seed=1167230683:i=126:bd=preordered_2995 on theBenchmark for (2995ds/126Mi)
% 6.31/1.69 % (290812)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=3509111445:st=4:i=219:sd=3:ss=axioms_2995 on theBenchmark for (2995ds/219Mi)
% 6.31/1.69 % (290812)Refutation not found, incomplete strategy
% 6.31/1.69 % (290812)------------------------------
% 6.31/1.69 % (290812)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.31/1.69 % (290812)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.31/1.69 % (290812)CaDiCaL version: 2.1.3
% 6.31/1.69 % (290812)Termination reason: Refutation not found, incomplete strategy
% 6.31/1.69 % (290812)Time elapsed: 0.010 s
% 6.31/1.69 % (290812)Peak memory usage: 88 MB
% 6.31/1.69 % (290812)Instructions burned: 21 (million)
% 6.31/1.69 % (290815)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=3597380226:avsq=on:i=194:fgj=on:bd=preordered_2994 on theBenchmark for (2994ds/194Mi)
% 6.31/1.69 % (290813)Instruction limit reached!
% 6.31/1.69 % (290813)------------------------------
% 6.31/1.69 % (290813)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.31/1.69 % (290813)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.31/1.69 % (290813)CaDiCaL version: 2.1.3
% 6.31/1.69 % (290813)Termination reason: Instruction limit
% 6.31/1.69 % (290813)Termination phase: Saturation
% 6.31/1.69 % (290813)Time elapsed: 0.056 s
% 6.31/1.69 % (290813)Peak memory usage: 88 MB
% 6.31/1.69 % (290813)Instructions burned: 126 (million)
% 6.31/1.69 % (290815)Refutation not found, incomplete strategy
% 6.31/1.69 % (290815)------------------------------
% 6.31/1.69 % (290815)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.31/1.69 % (290815)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.31/1.69 % (290815)CaDiCaL version: 2.1.3
% 6.31/1.69 % (290815)Termination reason: Refutation not found, incomplete strategy
% 6.31/1.69 % (290815)Time elapsed: 0.010 s
% 6.31/1.69 % (290815)Peak memory usage: 88 MB
% 6.31/1.69 % (290815)Instructions burned: 36 (million)
% 6.31/1.69 % (290819)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=707913171:i=157:gtg=all_2993 on theBenchmark for (2993ds/157Mi)
% 6.31/1.69 % (290815)------------------------------
% 6.31/1.69 % (290815)------------------------------
% 6.31/1.69 % (290819)First to succeed.
% 6.31/1.69 % (290819)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-290790"
% 6.31/1.69 % (290811)------------------------------
% 6.31/1.69 % (290811)------------------------------
% 6.31/1.69 % (290812)------------------------------
% 6.31/1.69 % (290812)------------------------------
% 6.31/1.69 % (290821)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=510303734:i=3394:sd=4:ss=included:sgt=64_2992 on theBenchmark for (2992ds/3394Mi)
% 6.31/1.69 % (290795)Refutation not found, incomplete strategy
% 6.31/1.69 % (290795)------------------------------
% 6.31/1.69 % (290795)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.31/1.69 % (290795)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.31/1.69 % (290795)CaDiCaL version: 2.1.3
% 6.31/1.69 % (290795)Termination reason: Refutation not found, incomplete strategy
% 6.31/1.69 % (290795)Time elapsed: 0.718 s
% 6.31/1.69 % (290795)Peak memory usage: 131 MB
% 6.31/1.69 % (290795)Instructions burned: 1083 (million)
% 6.31/1.69 % (290797)Refutation not found, incomplete strategy
% 6.31/1.69 % (290797)------------------------------
% 6.31/1.69 % (290797)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.31/1.69 % (290797)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.31/1.69 % (290797)CaDiCaL version: 2.1.3
% 6.31/1.69 % (290797)Termination reason: Refutation not found, incomplete strategy
% 6.31/1.69 % (290797)Time elapsed: 0.720 s
% 6.31/1.69 % (290797)Peak memory usage: 131 MB
% 6.31/1.69 % (290797)Instructions burned: 1091 (million)
% 6.31/1.69 % (290822)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=1322999457:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2992 on theBenchmark for (2992ds/106Mi)
% 6.31/1.69 % (290822)Refutation not found, incomplete strategy
% 6.31/1.69 % (290822)------------------------------
% 6.31/1.69 % (290822)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.31/1.69 % (290822)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.31/1.69 % (290822)CaDiCaL version: 2.1.3
% 6.31/1.69 % (290822)Termination reason: Refutation not found, incomplete strategy
% 6.31/1.69 % (290822)Time elapsed: 0.014 s
% 6.31/1.69 % (290822)Peak memory usage: 88 MB
% 6.31/1.69 % (290822)Instructions burned: 27 (million)
% 6.31/1.69 % (290823)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=1535268437:i=107_2991 on theBenchmark for (2991ds/107Mi)
% 6.31/1.69 % (290823)Refutation not found, incomplete strategy
% 6.31/1.69 % (290823)------------------------------
% 6.31/1.69 % (290823)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.31/1.69 % (290823)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.31/1.69 % (290823)CaDiCaL version: 2.1.3
% 6.31/1.69 % (290823)Termination reason: Refutation not found, incomplete strategy
% 6.31/1.69 % (290823)Time elapsed: 0.016 s
% 6.31/1.69 % (290823)Peak memory usage: 88 MB
% 6.31/1.69 % (290823)Instructions burned: 30 (million)
% 6.31/1.69 % SZS status Satisfiable for theBenchmark
% 6.31/1.69 % SZS output start Saturation.
% See solution above
% 7.84/1.89 % SZS output start Definitions and Model Updates.
% 7.84/1.89 % SZS output end Definitions and Model Updates.
% 7.84/1.89 % (290819)------------------------------
% 7.84/1.89 % (290819)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.84/1.89 % (290819)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.84/1.89 % (290819)CaDiCaL version: 2.1.3
% 7.84/1.89 % (290819)Termination reason: Satisfiable
% 7.84/1.89 % (290819)Time elapsed: 0.026 s
% 7.84/1.89 % (290819)Peak memory usage: 90 MB
% 7.84/1.89 % (290819)Instructions burned: 47 (million)
% 7.84/1.89 % (290819)------------------------------
% 7.84/1.89 % (290819)------------------------------
% 7.84/1.89 % (290790)Success in time 1.039 s
% 7.84/1.89 % Vampire exiting
%------------------------------------------------------------------------------