%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SWV538-1.010 : 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 : n026.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:17:27 PM UTC 2026
% Result : Satisfiable 3.02s 1.12s
% Output : Saturation 3.86s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(u178,hypothesis,
i7 != i6 ).
cnf(u183,hypothesis,
e_1302 = select(a_1297,i6) ).
cnf(u190,hypothesis,
i8 != i7 ).
cnf(u195,hypothesis,
e_1296 = e_1300 ).
cnf(u222,hypothesis,
i8 != i5 ).
cnf(u227,hypothesis,
e_1304 = select(a_1301,i5) ).
cnf(u265,hypothesis,
e_1308 = select(a_1305,i9) ).
cnf(u269,hypothesis,
i8 = i9 ).
cnf(u274,hypothesis,
e_1310 = select(a_1305,i4) ).
cnf(u278,hypothesis,
i8 = i4 ).
cnf(u308,hypothesis,
i9 = i1 ).
cnf(u312,hypothesis,
e_1312 = select(a_1309,i1) ).
cnf(u394,hypothesis,
i5 != i0 ).
cnf(u399,hypothesis,
e_1320 = select(a_1317,i0) ).
cnf(u435,hypothesis,
e_1323 = select(a_1321,i2) ).
cnf(u439,hypothesis,
i5 = i2 ).
cnf(u459,hypothesis,
e_1325 = select(a_1321,i8) ).
cnf(u463,hypothesis,
i8 = i0 ).
cnf(u470,hypothesis,
i5 != i1 ).
cnf(u475,hypothesis,
e_1316 = select(a_1313,i5) ).
cnf(u482,hypothesis,
i1 = i0 ).
cnf(u535,hypothesis,
i2 = i3 ).
cnf(u606,hypothesis,
i5 = i_1372 ).
cnf(u625,hypothesis,
i8 = i6 ).
cnf(u761,hypothesis,
i7 = i5 ).
cnf(u98,hypothesis,
e_1323 = select(a_1324,i1) ).
cnf(u1783,hypothesis,
e_1296 = e_1341 ).
cnf(u97,hypothesis,
e_1320 = select(a_1322,i0) ).
cnf(u857,hypothesis,
e_1296 = select(a_1342,i7) ).
cnf(u890,hypothesis,
e_1360 = e_1366 ).
cnf(u1576,hypothesis,
e_1298 = e_1368 ).
cnf(u702,hypothesis,
e_1368 = e_1370 ).
cnf(u377,hypothesis,
e_1308 = select(a_1309,i8) ).
cnf(u1505,hypothesis,
a_1346 = store(a_1344,i8,e_1298) ).
cnf(hyp53,hypothesis,
e_1323 = select(a_1322,i2) ).
cnf(u100,hypothesis,
e_1327 = select(a_1328,i3) ).
cnf(hyp60,hypothesis,
e_1339 = select(a_1336,i6) ).
cnf(u593,hypothesis,
a_1328 = store(a_1326,i5,e_1327) ).
cnf(hyp47,hypothesis,
e_1310 = select(a_1307,i4) ).
cnf(u1131,hypothesis,
e_1343 = e_1351 ).
cnf(u1556,hypothesis,
( select(a_1363,X0) = select(a_1365,X0)
| i7 = X0 ) ).
cnf(u2027,hypothesis,
e_1298 = e_1366 ).
cnf(u798,hypothesis,
e_1327 = e_1331 ).
cnf(u94,hypothesis,
e_1316 = select(a_1317,i4) ).
cnf(u1547,hypothesis,
a_1328 = store(a_1326,i7,e_1296) ).
cnf(u1133,hypothesis,
a_1324 = store(a_1322,i8,e_1296) ).
cnf(u334,hypothesis,
e_1310 = select(a_1311,i8) ).
cnf(u1887,hypothesis,
e_1298 = select(a_1367,i8) ).
cnf(u1155,hypothesis,
a_1358 = store(a_1356,i8,e_1343) ).
cnf(u1495,hypothesis,
( select(a_1352,X0) = select(a_1354,X0)
| i8 = X0 ) ).
cnf(u1139,hypothesis,
a_1319 = store(a_1317,i7,e_1296) ).
cnf(u833,hypothesis,
e_1323 = select(a_1326,i1) ).
cnf(u1157,hypothesis,
a_1352 = store(a_1350,i7,e_1343) ).
cnf(u1130,hypothesis,
e_1296 = select(a_1324,i8) ).
cnf(hyp77,hypothesis,
e_1374 = select(a_1371,i_1372) ).
cnf(u1762,hypothesis,
e_1298 = e_1370 ).
cnf(u957,hypothesis,
e_1298 = e_1310 ).
cnf(u1110,hypothesis,
e_1360 = select(a_1359,i8) ).
cnf(u696,hypothesis,
e_1368 = select(a_1369,i8) ).
cnf(u1433,hypothesis,
( select(a_1330,X0) = select(a_1332,X0)
| i8 = X0 ) ).
cnf(u1741,hypothesis,
e_1298 = e_1347 ).
cnf(u846,hypothesis,
e_1318 = select(a_1319,i7) ).
cnf(u879,hypothesis,
a_1328 = store(a_1326,i7,e_1323) ).
cnf(u820,hypothesis,
e_1320 = select(a_1319,i1) ).
cnf(u1294,hypothesis,
e_1296 = select(a_1326,i8) ).
cnf(u123,hypothesis,
( select(a_1297,X0) = select(a_1299,X0)
| i7 = X0 ) ).
cnf(hyp49,hypothesis,
e_1314 = select(a_1311,i7) ).
cnf(u139,hypothesis,
( select(a_1324,X0) = select(a_1326,X0)
| i2 = X0 ) ).
cnf(u952,hypothesis,
a_1365 = store(a_1363,i7,e_1362) ).
cnf(u330,hypothesis,
e_1308 = select(a_1307,i8) ).
cnf(u1105,hypothesis,
a_1350 = store(a_1348,i8,e_1349) ).
cnf(u142,hypothesis,
( select(a_1330,X0) = select(a_1332,X0)
| i9 = X0 ) ).
cnf(u683,hypothesis,
e_1343 = select(a_1338,i5) ).
cnf(u1339,hypothesis,
a_1321 = store(a_1319,i8,e_1298) ).
cnf(u141,hypothesis,
( select(a_1328,X0) = select(a_1330,X0)
| i0 = X0 ) ).
cnf(u1662,hypothesis,
( select(a_1317,X0) = select(a_1319,X0)
| i7 = X0 ) ).
cnf(u876,hypothesis,
a_1332 = store(a_1330,i8,e_1323) ).
cnf(u135,hypothesis,
( select(a_1317,X0) = select(a_1319,X0)
| i5 = X0 ) ).
cnf(u326,hypothesis,
a_1311 = store(a_1309,i8,e_1310) ).
cnf(u91,hypothesis,
e_1310 = select(a_1311,i9) ).
cnf(u987,hypothesis,
e_1323 = select(a_1321,i7) ).
cnf(u859,hypothesis,
e_1323 = select(a_1330,i7) ).
cnf(u1690,hypothesis,
e_1296 = e_1323 ).
cnf(u93,hypothesis,
e_1314 = select(a_1315,i1) ).
cnf(u1658,hypothesis,
e_1298 = e_1351 ).
cnf(u1645,hypothesis,
e_1298 = e_1353 ).
cnf(u2452,hypothesis,
e_1298 = select(a_1369,i8) ).
cnf(hyp46,hypothesis,
e_1308 = select(a_1307,i9) ).
cnf(u828,hypothesis,
e_1357 = select(a_1359,i1) ).
cnf(u87,hypothesis,
e_1302 = select(a_1303,i8) ).
cnf(hyp71,hypothesis,
e_1362 = select(a_1359,i2) ).
cnf(hyp40,hypothesis,
e_1296 = select(a1,i7) ).
cnf(u1759,hypothesis,
e_1296 = select(a_1303,i8) ).
cnf(hyp70,hypothesis,
e_1360 = select(a_1359,i1) ).
cnf(u706,hypothesis,
a_1301 = store(a_1299,i8,e_1296) ).
cnf(hyp43,hypothesis,
e_1302 = select(a_1299,i6) ).
cnf(hyp73,hypothesis,
e_1366 = select(a_1363,i3) ).
cnf(u705,hypothesis,
a_1338 = store(a_1336,i8,e_1296) ).
cnf(hyp42,hypothesis,
e_1300 = select(a_1299,i8) ).
cnf(u849,hypothesis,
e_1355 = select(a_1356,i7) ).
cnf(hyp64,hypothesis,
e_1347 = select(a_1344,i4) ).
cnf(hyp29,hypothesis,
a_1352 = store(a_1350,i7,e_1351) ).
cnf(u160,hypothesis,
( select(a_1365,X0) = select(a_1367,X0)
| i0 = X0 ) ).
cnf(hyp67,hypothesis,
e_1353 = select(a_1352,i5) ).
cnf(hyp36,hypothesis,
a_1365 = store(a_1363,i3,e_1364) ).
cnf(hyp66,hypothesis,
e_1351 = select(a_1348,i1) ).
cnf(hyp23,hypothesis,
a_1340 = store(a_1338,i8,e_1339) ).
cnf(u1711,hypothesis,
e_1296 = e_1327 ).
cnf(hyp22,hypothesis,
a_1338 = store(a_1336,i6,e_1337) ).
cnf(u376,hypothesis,
e_1355 = select(a_1352,i8) ).
cnf(u1651,hypothesis,
( select(a_1328,X0) = select(a_1330,X0)
| i8 = X0 ) ).
cnf(hyp25,hypothesis,
a_1344 = store(a_1342,i8,e_1343) ).
cnf(u981,hypothesis,
a_1309 = store(a_1307,i8,e_1298) ).
cnf(hyp16,hypothesis,
a_1328 = store(a_1326,i3,e_1327) ).
cnf(hyp19,hypothesis,
a_1334 = store(a_1332,i5,e_1333) ).
cnf(u853,hypothesis,
e_1351 = e_1353 ).
cnf(u370,hypothesis,
a_1317 = store(a_1315,i8,e_1316) ).
cnf(u1261,hypothesis,
a_1326 = store(a_1324,i7,e_1320) ).
cnf(hyp18,hypothesis,
a_1332 = store(a_1330,i9,e_1331) ).
cnf(u329,hypothesis,
a_1371 = store(a_1369,i8,e_1370) ).
cnf(hyp5,hypothesis,
a_1307 = store(a_1305,i5,e_1306) ).
cnf(u1490,hypothesis,
( select(a_1315,X0) = select(a_1317,X0)
| i8 = X0 ) ).
cnf(u829,hypothesis,
e_1366 = select(a_1367,i1) ).
cnf(u1868,negated_conjecture,
i7 = i3 ).
cnf(hyp12,hypothesis,
a_1321 = store(a_1319,i0,e_1320) ).
cnf(u2404,hypothesis,
e_1298 = select(a_1330,i8) ).
cnf(a2,axiom,
( select(store(X2,X0,X3),X1) = select(X2,X1)
| X0 = X1 ) ).
cnf(u1211,hypothesis,
e_1325 = select(a_1326,i7) ).
cnf(a1,axiom,
select(store(X0,X1,X2),X1) = X2 ).
cnf(u1257,hypothesis,
e_1320 = e_1325 ).
cnf(u325,hypothesis,
i8 = i1 ).
cnf(u794,hypothesis,
e_1366 = select(a_1363,i7) ).
cnf(u1426,hypothesis,
( select(a_1309,X0) = select(a_1311,X0)
| i8 = X0 ) ).
cnf(u1095,hypothesis,
e_1296 = e_1318 ).
cnf(u1632,hypothesis,
a_1359 = store(a_1358,i8,e_1298) ).
cnf(u112,hypothesis,
e_1351 = select(a_1352,i7) ).
cnf(u1560,hypothesis,
a_1365 = store(a_1363,i7,e_1296) ).
cnf(u1639,hypothesis,
( select(a_1365,X0) = select(a_1367,X0)
| i8 = X0 ) ).
cnf(u1375,hypothesis,
a_1356 = store(a_1354,i7,e_1296) ).
cnf(u1517,hypothesis,
( select(a_1324,X0) = select(a_1326,X0)
| i7 = X0 ) ).
cnf(u1673,hypothesis,
( select(a_1340,X0) = select(a_1342,X0)
| i7 = X0 ) ).
cnf(u558,hypothesis,
e_1360 = select(a_1361,i5) ).
cnf(u2030,hypothesis,
e_1298 = e_1329 ).
cnf(u959,hypothesis,
a_1354 = store(a_1352,i8,e_1351) ).
cnf(u1361,hypothesis,
a_1350 = store(a_1348,i8,e_1296) ).
cnf(u557,hypothesis,
e_1325 = select(a_1326,i5) ).
cnf(u327,hypothesis,
a_1332 = store(a_1330,i8,e_1331) ).
cnf(u1033,hypothesis,
e_1349 = select(a_1344,i7) ).
cnf(u1666,hypothesis,
a_1352 = store(a_1350,i7,e_1298) ).
cnf(u1622,hypothesis,
a_1358 = store(a_1356,i8,e_1298) ).
cnf(u832,hypothesis,
e_1362 = e_1364 ).
cnf(u101,hypothesis,
e_1329 = select(a_1330,i0) ).
cnf(u1351,hypothesis,
e_1298 = e_1343 ).
cnf(u817,hypothesis,
a_1358 = store(a_1356,i1,e_1357) ).
cnf(u2089,hypothesis,
e_1298 = select(a_1361,i7) ).
cnf(u1144,hypothesis,
e_1374 = select(a_1367,i7) ).
cnf(u915,hypothesis,
a_1371 = store(a_1369,i8,e_1368) ).
cnf(u95,hypothesis,
e_1318 = select(a_1319,i5) ).
cnf(u1617,hypothesis,
( select(a_1356,X0) = select(a_1358,X0)
| i8 = X0 ) ).
cnf(u171,hypothesis,
a_1342 = store(a_1340,i5,e_1339) ).
cnf(u1445,hypothesis,
( select(a_1346,X0) = select(a_1348,X0)
| i8 = X0 ) ).
cnf(u552,hypothesis,
i5 = i3 ).
cnf(u1289,hypothesis,
e_1320 = select(a_1330,i8) ).
cnf(u386,hypothesis,
a_1346 = store(a_1344,i8,e_1343) ).
cnf(u167,hypothesis,
e_1296 = e_1337 ).
cnf(hyp1,hypothesis,
a_1299 = store(a_1297,i7,e_1298) ).
cnf(u1569,hypothesis,
( select(a_1336,X0) = select(a_1338,X0)
| i8 = X0 ) ).
cnf(u154,hypothesis,
( select(a_1354,X0) = select(a_1356,X0)
| i5 = X0 ) ).
cnf(u701,hypothesis,
e_1296 = select(a_1301,i8) ).
cnf(u2059,hypothesis,
e_1298 = e_1325 ).
cnf(u153,hypothesis,
( select(a_1352,X0) = select(a_1354,X0)
| i4 = X0 ) ).
cnf(u126,hypothesis,
( select(a_1299,X0) = select(a_1301,X0)
| i6 = X0 ) ).
cnf(u615,hypothesis,
e_1333 = e_1373 ).
cnf(u156,hypothesis,
( select(a_1358,X0) = select(a_1359,X0)
| i0 = X0 ) ).
cnf(u125,hypothesis,
( select(a1,X0) = select(a_1335,X0)
| i7 = X0 ) ).
cnf(u147,hypothesis,
( select(a_1340,X0) = select(a_1342,X0)
| i5 = X0 ) ).
cnf(u338,hypothesis,
e_1343 = e_1345 ).
cnf(u819,hypothesis,
a_1367 = store(a_1365,i1,e_1366) ).
cnf(u150,hypothesis,
( select(a_1346,X0) = select(a_1348,X0)
| i9 = X0 ) ).
cnf(u119,hypothesis,
e_1364 = select(a_1365,i3) ).
cnf(u149,hypothesis,
( select(a_1344,X0) = select(a_1346,X0)
| i4 = X0 ) ).
cnf(u106,hypothesis,
e_1339 = select(a_1340,i8) ).
cnf(u136,hypothesis,
( select(a_1319,X0) = select(a_1321,X0)
| i0 = X0 ) ).
cnf(u105,hypothesis,
e_1337 = select(a_1338,i6) ).
cnf(u143,hypothesis,
( select(a_1332,X0) = select(a_1334,X0)
| i5 = X0 ) ).
cnf(u108,hypothesis,
e_1343 = select(a_1344,i8) ).
cnf(u815,hypothesis,
a_1322 = store(a_1321,i1,e_1320) ).
cnf(u130,hypothesis,
( select(a_1307,X0) = select(a_1309,X0)
| i4 = X0 ) ).
cnf(u99,hypothesis,
e_1325 = select(a_1326,i2) ).
cnf(u966,hypothesis,
a_1305 = store(a_1303,i8,e_1298) ).
cnf(u129,hypothesis,
( select(a_1305,X0) = select(a_1307,X0)
| i5 = X0 ) ).
cnf(u102,hypothesis,
e_1331 = select(a_1332,i9) ).
cnf(u1017,hypothesis,
e_1343 = select(a_1338,i7) ).
cnf(u132,hypothesis,
( select(a_1311,X0) = select(a_1313,X0)
| i7 = X0 ) ).
cnf(u818,hypothesis,
a_1359 = store(a_1358,i1,e_1357) ).
cnf(u734,hypothesis,
e_1349 = select(a_1346,i7) ).
cnf(hyp55,hypothesis,
e_1327 = select(a_1326,i0) ).
cnf(u613,hypothesis,
e_1374 = select(a_1371,i5) ).
cnf(u88,hypothesis,
e_1304 = select(a_1305,i8) ).
cnf(hyp54,hypothesis,
e_1325 = select(a_1322,i1) ).
cnf(u690,hypothesis,
a_1369 = store(a_1367,i8,e_1368) ).
cnf(u381,hypothesis,
e_1343 = select(a_1346,i8) ).
cnf(hyp57,hypothesis,
e_1331 = select(a_1330,i5) ).
cnf(u597,hypothesis,
e_1327 = select(a_1328,i5) ).
cnf(goal,negated_conjecture,
e_1373 != e_1374 ).
cnf(u1013,hypothesis,
e_1296 = e_1314 ).
cnf(hyp48,hypothesis,
e_1312 = select(a_1311,i1) ).
cnf(hyp78,hypothesis,
i_1372 = sk(a_1334,a_1371) ).
cnf(u1503,hypothesis,
e_1298 = e_1316 ).
cnf(hyp51,hypothesis,
e_1318 = select(a_1315,i4) ).
cnf(u841,hypothesis,
e_1316 = select(a_1315,i7) ).
cnf(u814,hypothesis,
a_1321 = store(a_1319,i1,e_1320) ).
cnf(hyp50,hypothesis,
e_1316 = select(a_1315,i5) ).
cnf(hyp37,hypothesis,
a_1367 = store(a_1365,i0,e_1366) ).
cnf(u1731,hypothesis,
a_1348 = store(a_1346,i8,e_1298) ).
cnf(hyp44,hypothesis,
e_1304 = select(a_1303,i5) ).
cnf(hyp31,hypothesis,
a_1356 = store(a_1354,i5,e_1355) ).
cnf(u837,hypothesis,
a_1334 = store(a_1332,i7,e_1333) ).
cnf(u1785,hypothesis,
e_1298 = select(a_1305,i8) ).
cnf(u1543,hypothesis,
( select(a_1326,X0) = select(a_1328,X0)
| i7 = X0 ) ).
cnf(u1815,hypothesis,
e_1298 = select(a_1317,i8) ).
cnf(u861,hypothesis,
a_1307 = store(a_1305,i7,e_1296) ).
cnf(u1120,hypothesis,
e_1355 = select(a_1363,i8) ).
cnf(u1127,hypothesis,
a_1315 = store(a_1313,i8,e_1296) ).
cnf(u2284,hypothesis,
e_1296 = select(a_1356,i7) ).
cnf(u1460,hypothesis,
( select(a_1369,X0) = select(a_1371,X0)
| i8 = X0 ) ).
cnf(u822,hypothesis,
e_1357 = select(a_1356,i1) ).
cnf(u700,hypothesis,
e_1296 = select(a_1338,i8) ).
cnf(u1113,hypothesis,
e_1349 = select(a_1350,i8) ).
cnf(u1746,hypothesis,
e_1298 = select(a_1371,i8) ).
cnf(u1607,hypothesis,
( select(a_1321,X0) = select(a_1322,X0)
| i8 = X0 ) ).
cnf(u1581,hypothesis,
( select(a_1299,X0) = select(a_1301,X0)
| i8 = X0 ) ).
cnf(u1266,hypothesis,
e_1343 = select(a_1358,i8) ).
cnf(u724,hypothesis,
a_1311 = store(a_1309,i8,e_1308) ).
cnf(u1583,hypothesis,
a_1369 = store(a_1367,i8,e_1298) ).
cnf(u769,hypothesis,
e_1355 = select(a_1350,i8) ).
cnf(u715,hypothesis,
e_1296 = e_1302 ).
cnf(u2124,negated_conjecture,
i7 = i2 ).
cnf(u1243,hypothesis,
e_1320 = select(a_1319,i8) ).
cnf(u1128,hypothesis,
e_1351 = e_1357 ).
cnf(u839,hypothesis,
a_1356 = store(a_1354,i7,e_1355) ).
cnf(u893,hypothesis,
a_1367 = store(a_1365,i1,e_1360) ).
cnf(u1525,hypothesis,
e_1298 = select(a_1354,i8) ).
cnf(u1835,hypothesis,
e_1298 = select(a_1313,i7) ).
cnf(u1016,hypothesis,
a_1317 = store(a_1315,i8,e_1312) ).
cnf(u2252,hypothesis,
e_1296 = select(a_1350,i8) ).
cnf(u860,hypothesis,
a_1342 = store(a_1340,i7,e_1296) ).
cnf(u84,hypothesis,
e_1296 = select(a_1297,i8) ).
cnf(hyp72,hypothesis,
e_1364 = select(a_1363,i0) ).
cnf(u1612,hypothesis,
a_1334 = store(a_1332,i7,e_1298) ).
cnf(hyp75,hypothesis,
e_1370 = select(a_1367,i6) ).
cnf(hyp74,hypothesis,
e_1368 = select(a_1367,i9) ).
cnf(hyp7,hypothesis,
a_1311 = store(a_1309,i9,e_1310) ).
cnf(u385,hypothesis,
e_1308 = e_1310 ).
cnf(hyp61,hypothesis,
e_1341 = select(a_1340,i8) ).
cnf(u709,hypothesis,
e_1296 = e_1339 ).
cnf(hyp30,hypothesis,
a_1354 = store(a_1352,i4,e_1353) ).
cnf(u812,hypothesis,
e_1357 = select(a_1354,i1) ).
cnf(hyp68,hypothesis,
e_1355 = select(a_1352,i4) ).
cnf(hyp33,hypothesis,
a_1359 = store(a_1358,i0,e_1357) ).
cnf(u967,hypothesis,
e_1320 = select(a_1317,i1) ).
cnf(u941,hypothesis,
e_1298 = e_1304 ).
cnf(hyp24,hypothesis,
a_1342 = store(a_1340,i5,e_1341) ).
cnf(u1743,hypothesis,
a_1371 = store(a_1369,i8,e_1298) ).
cnf(u1642,hypothesis,
a_1367 = store(a_1365,i8,e_1298) ).
cnf(hyp27,hypothesis,
a_1348 = store(a_1346,i9,e_1347) ).
cnf(hyp26,hypothesis,
a_1346 = store(a_1344,i4,e_1345) ).
cnf(u337,hypothesis,
e_1370 = select(a_1371,i8) ).
cnf(u157,hypothesis,
( select(a_1359,X0) = select(a_1361,X0)
| i2 = X0 ) ).
cnf(hyp13,hypothesis,
a_1322 = store(a_1321,i0,e_1320) ).
cnf(u661,hypothesis,
e_1314 = select(a_1309,i7) ).
cnf(u1520,hypothesis,
a_1326 = store(a_1324,i7,e_1298) ).
cnf(u2273,hypothesis,
e_1296 = select(a_1358,i7) ).
cnf(hyp20,hypothesis,
a_1335 = store(a1,i7,e_1298) ).
cnf(u331,hypothesis,
e_1333 = select(a_1330,i8) ).
cnf(u374,hypothesis,
e_1318 = select(a_1315,i8) ).
cnf(u372,hypothesis,
a_1354 = store(a_1352,i8,e_1353) ).
cnf(u168,hypothesis,
a_1338 = store(a_1336,i6,e_1296) ).
cnf(hyp6,hypothesis,
a_1309 = store(a_1307,i4,e_1308) ).
cnf(u2028,hypothesis,
e_1298 = e_1357 ).
cnf(u333,hypothesis,
e_1368 = select(a_1367,i8) ).
cnf(hyp9,hypothesis,
a_1315 = store(a_1313,i1,e_1314) ).
cnf(u1563,hypothesis,
( select(a_1367,X0) = select(a_1369,X0)
| i8 = X0 ) ).
cnf(u162,hypothesis,
( select(a_1369,X0) = select(a_1371,X0)
| i9 = X0 ) ).
cnf(hyp0,hypothesis,
a_1297 = store(a1,i8,e_1296) ).
cnf(u1668,hypothesis,
( select(a_1332,X0) = select(a_1334,X0)
| i7 = X0 ) ).
cnf(u161,hypothesis,
( select(a_1367,X0) = select(a_1369,X0)
| i6 = X0 ) ).
cnf(hyp3,hypothesis,
a_1303 = store(a_1301,i8,e_1302) ).
cnf(u2230,hypothesis,
e_1296 = select(a_1321,i7) ).
cnf(u164,hypothesis,
e_1302 = e_1306 ).
cnf(hyp2,hypothesis,
a_1301 = store(a_1299,i6,e_1300) ).
cnf(u1598,hypothesis,
e_1298 = e_1333 ).
cnf(u2198,hypothesis,
e_1298 = select(a_1344,i8) ).
cnf(u120,hypothesis,
e_1366 = select(a_1367,i0) ).
cnf(u827,hypothesis,
e_1357 = select(a_1358,i1) ).
cnf(u594,hypothesis,
a_1365 = store(a_1363,i5,e_1364) ).
cnf(u127,hypothesis,
( select(a_1301,X0) = select(a_1303,X0)
| i8 = X0 ) ).
cnf(u1871,hypothesis,
e_1298 = select(a_1359,i8) ).
cnf(u1791,hypothesis,
e_1298 = select(a_1309,i8) ).
cnf(u114,hypothesis,
e_1355 = select(a_1356,i5) ).
cnf(u795,hypothesis,
e_1325 = e_1329 ).
cnf(u113,hypothesis,
e_1353 = select(a_1354,i4) ).
cnf(u1847,hypothesis,
e_1298 = select(a_1352,i7) ).
cnf(u2148,hypothesis,
e_1298 = select(a_1321,i8) ).
cnf(u1228,hypothesis,
e_1374 = select(a_1371,i7) ).
cnf(u110,hypothesis,
e_1347 = select(a_1348,i9) ).
cnf(u1222,hypothesis,
e_1296 = select(a_1328,i7) ).
cnf(u1627,hypothesis,
( select(a_1358,X0) = select(a_1359,X0)
| i8 = X0 ) ).
cnf(u1028,hypothesis,
a_1315 = store(a_1313,i1,e_1296) ).
cnf(u109,hypothesis,
e_1345 = select(a_1346,i4) ).
cnf(u1725,hypothesis,
( select(a_1361,X0) = select(a_1363,X0)
| i8 = X0 ) ).
cnf(u840,hypothesis,
e_1304 = select(a_1303,i7) ).
cnf(u825,hypothesis,
e_1320 = select(a_1322,i1) ).
cnf(u1534,hypothesis,
a_1361 = store(a_1359,i7,e_1298) ).
cnf(u1340,hypothesis,
a_1322 = store(a_1321,i8,e_1298) ).
cnf(u992,hypothesis,
e_1318 = e_1323 ).
cnf(u1724,hypothesis,
a_1363 = store(a_1361,i8,e_1296) ).
cnf(u1214,hypothesis,
e_1360 = select(a_1361,i7) ).
cnf(u836,hypothesis,
a_1319 = store(a_1317,i7,e_1318) ).
cnf(u1334,hypothesis,
e_1298 = e_1320 ).
cnf(u1146,hypothesis,
a_1313 = store(a_1311,i7,e_1298) ).
cnf(u1358,hypothesis,
e_1296 = e_1349 ).
cnf(u89,hypothesis,
e_1306 = select(a_1307,i5) ).
cnf(u1372,hypothesis,
e_1296 = e_1355 ).
cnf(u1855,hypothesis,
e_1298 = select(a_1358,i8) ).
cnf(u1920,hypothesis,
e_1298 = e_1360 ).
cnf(u2458,hypothesis,
e_1298 = select(a_1334,i7) ).
cnf(u1156,hypothesis,
a_1359 = store(a_1358,i8,e_1343) ).
cnf(u1125,hypothesis,
a_1363 = store(a_1361,i8,e_1355) ).
cnf(u1285,hypothesis,
a_1361 = store(a_1359,i7,e_1343) ).
cnf(u83,hypothesis,
e_1298 = select(a_1299,i7) ).
cnf(u1275,hypothesis,
e_1343 = e_1360 ).
cnf(u556,hypothesis,
e_1362 = select(a_1359,i5) ).
cnf(u1405,negated_conjecture,
e_1296 != e_1333 ).
cnf(u1738,hypothesis,
e_1298 = select(a_1311,i8) ).
cnf(hyp59,hypothesis,
e_1337 = select(a_1336,i8) ).
cnf(u1122,hypothesis,
e_1296 = select(a_1315,i8) ).
cnf(u155,hypothesis,
( select(a_1356,X0) = select(a_1358,X0)
| i0 = X0 ) ).
cnf(u158,hypothesis,
( select(a_1361,X0) = select(a_1363,X0)
| i1 = X0 ) ).
cnf(u1727,hypothesis,
( select(a_1313,X0) = select(a_1315,X0)
| i8 = X0 ) ).
cnf(u1108,hypothesis,
e_1325 = select(a_1322,i8) ).
cnf(u843,hypothesis,
e_1343 = select(a_1340,i7) ).
cnf(u144,hypothesis,
( select(a_1335,X0) = select(a_1336,X0)
| i8 = X0 ) ).
cnf(u151,hypothesis,
( select(a_1348,X0) = select(a_1350,X0)
| i1 = X0 ) ).
cnf(u116,hypothesis,
e_1357 = select(a_1359,i0) ).
cnf(u138,hypothesis,
( select(a_1322,X0) = select(a_1324,X0)
| i1 = X0 ) ).
cnf(u107,hypothesis,
e_1341 = select(a_1342,i5) ).
cnf(u137,hypothesis,
( select(a_1321,X0) = select(a_1322,X0)
| i0 = X0 ) ).
cnf(u2362,hypothesis,
e_1298 = select(a_1346,i8) ).
cnf(u328,hypothesis,
a_1348 = store(a_1346,i8,e_1347) ).
cnf(u1885,negated_conjecture,
e_1296 = e_1364 ).
cnf(u140,hypothesis,
( select(a_1326,X0) = select(a_1328,X0)
| i3 = X0 ) ).
cnf(u847,hypothesis,
e_1333 = select(a_1334,i7) ).
cnf(u131,hypothesis,
( select(a_1309,X0) = select(a_1311,X0)
| i9 = X0 ) ).
cnf(u96,hypothesis,
e_1320 = select(a_1321,i0) ).
cnf(u134,hypothesis,
( select(a_1315,X0) = select(a_1317,X0)
| i4 = X0 ) ).
cnf(u103,hypothesis,
e_1333 = select(a_1334,i5) ).
cnf(u133,hypothesis,
( select(a_1313,X0) = select(a_1315,X0)
| i1 = X0 ) ).
cnf(u90,hypothesis,
e_1308 = select(a_1309,i4) ).
cnf(hyp56,hypothesis,
e_1329 = select(a_1326,i3) ).
cnf(u383,hypothesis,
e_1343 = e_1347 ).
cnf(u722,hypothesis,
a_1348 = store(a_1346,i8,e_1343) ).
cnf(u336,hypothesis,
e_1347 = select(a_1348,i8) ).
cnf(u1715,hypothesis,
( select(a_1348,X0) = select(a_1350,X0)
| i8 = X0 ) ).
cnf(u92,hypothesis,
e_1312 = select(a_1313,i7) ).
cnf(hyp58,hypothesis,
e_1333 = select(a_1330,i9) ).
cnf(u369,hypothesis,
a_1309 = store(a_1307,i8,e_1308) ).
cnf(u1853,hypothesis,
e_1296 = select(a_1365,i7) ).
cnf(hyp45,hypothesis,
e_1306 = select(a_1303,i8) ).
cnf(u86,hypothesis,
e_1300 = select(a_1301,i6) ).
cnf(u1001,hypothesis,
e_1312 = e_1316 ).
cnf(hyp52,hypothesis,
e_1320 = select(a_1319,i0) ).
cnf(u1829,hypothesis,
e_1296 = select(a_1319,i7) ).
cnf(u85,hypothesis,
e_1298 = select(a_1335,i7) ).
cnf(hyp39,hypothesis,
a_1371 = store(a_1369,i9,e_1370) ).
cnf(hyp69,hypothesis,
e_1357 = select(a_1356,i0) ).
cnf(hyp38,hypothesis,
a_1369 = store(a_1367,i6,e_1368) ).
cnf(hyp76,hypothesis,
e_1373 = select(a_1334,i_1372) ).
cnf(hyp41,hypothesis,
e_1298 = select(a1,i8) ).
cnf(hyp63,hypothesis,
e_1345 = select(a_1344,i9) ).
cnf(u997,hypothesis,
a_1311 = store(a_1309,i8,e_1298) ).
cnf(hyp32,hypothesis,
a_1358 = store(a_1356,i0,e_1357) ).
cnf(hyp62,hypothesis,
e_1343 = select(a_1340,i5) ).
cnf(hyp35,hypothesis,
a_1363 = store(a_1361,i1,e_1362) ).
cnf(u165,hypothesis,
a_1307 = store(a_1305,i5,e_1302) ).
cnf(hyp65,hypothesis,
e_1349 = select(a_1348,i7) ).
cnf(u1277,hypothesis,
e_1343 = select(a_1359,i8) ).
cnf(hyp34,hypothesis,
a_1361 = store(a_1359,i2,e_1360) ).
cnf(u598,hypothesis,
e_1364 = select(a_1365,i5) ).
cnf(u1473,hypothesis,
( select(a_1307,X0) = select(a_1309,X0)
| i8 = X0 ) ).
cnf(hyp21,hypothesis,
a_1336 = store(a_1335,i8,e_1296) ).
cnf(u1506,hypothesis,
( select(a_1344,X0) = select(a_1346,X0)
| i8 = X0 ) ).
cnf(hyp28,hypothesis,
a_1350 = store(a_1348,i1,e_1349) ).
cnf(hyp15,hypothesis,
a_1326 = store(a_1324,i2,e_1325) ).
cnf(u949,hypothesis,
e_1298 = e_1308 ).
cnf(hyp14,hypothesis,
a_1324 = store(a_1322,i1,e_1323) ).
cnf(u930,hypothesis,
e_1304 = select(a_1301,i7) ).
cnf(u1101,hypothesis,
e_1355 = e_1362 ).
cnf(u1734,hypothesis,
e_1298 = select(a_1348,i8) ).
cnf(u1251,hypothesis,
e_1320 = select(a_1321,i8) ).
cnf(u1795,hypothesis,
e_1296 = e_1306 ).
cnf(u1254,hypothesis,
e_1320 = select(a_1322,i8) ).
cnf(u916,hypothesis,
a_1340 = store(a_1338,i8,e_1296) ).
cnf(u148,hypothesis,
( select(a_1342,X0) = select(a_1344,X0)
| i8 = X0 ) ).
cnf(u1531,hypothesis,
( select(a_1359,X0) = select(a_1361,X0)
| i7 = X0 ) ).
cnf(u1098,hypothesis,
e_1298 = e_1312 ).
cnf(u806,hypothesis,
e_1323 = e_1327 ).
cnf(u1890,negated_conjecture,
e_1296 = e_1362 ).
cnf(u1729,hypothesis,
( select(a_1322,X0) = select(a_1324,X0)
| i8 = X0 ) ).
cnf(u1250,hypothesis,
e_1343 = select(a_1356,i8) ).
cnf(u1685,hypothesis,
e_1296 = e_1331 ).
cnf(u1282,hypothesis,
e_1343 = select(a_1367,i8) ).
cnf(u1654,hypothesis,
a_1330 = store(a_1328,i8,e_1298) ).
cnf(u1227,hypothesis,
e_1355 = select(a_1365,i7) ).
cnf(u824,hypothesis,
e_1320 = select(a_1321,i1) ).
cnf(u1208,hypothesis,
e_1355 = select(a_1359,i7) ).
cnf(u554,hypothesis,
a_1361 = store(a_1359,i5,e_1360) ).
cnf(u1682,hypothesis,
e_1296 = select(a_1332,i8) ).
cnf(u1681,hypothesis,
a_1332 = store(a_1330,i8,e_1296) ).
cnf(u1202,hypothesis,
e_1296 = select(a_1322,i7) ).
cnf(u111,hypothesis,
e_1349 = select(a_1350,i1) ).
cnf(u1509,hypothesis,
a_1317 = store(a_1315,i8,e_1298) ).
cnf(u1394,hypothesis,
e_1296 = e_1374 ).
cnf(u1657,hypothesis,
a_1354 = store(a_1352,i8,e_1298) ).
cnf(u1353,hypothesis,
a_1344 = store(a_1342,i8,e_1298) ).
cnf(u553,hypothesis,
a_1326 = store(a_1324,i5,e_1325) ).
cnf(u640,hypothesis,
e_1296 = select(a_1297,i7) ).
cnf(u1590,hypothesis,
( select(a_1319,X0) = select(a_1321,X0)
| i8 = X0 ) ).
cnf(u1026,hypothesis,
e_1343 = select(a_1336,i7) ).
cnf(u1974,hypothesis,
e_1298 = select(a_1326,i7) ).
cnf(u1675,hypothesis,
( select(a_1305,X0) = select(a_1307,X0)
| i7 = X0 ) ).
cnf(u378,hypothesis,
e_1316 = select(a_1317,i8) ).
cnf(u2440,hypothesis,
e_1296 = select(a_1363,i8) ).
cnf(u927,hypothesis,
e_1374 = select(a_1369,i7) ).
cnf(u380,hypothesis,
e_1353 = select(a_1354,i8) ).
cnf(u929,hypothesis,
a_1303 = store(a_1301,i8,e_1296) ).
cnf(hyp11,hypothesis,
a_1319 = store(a_1317,i5,e_1318) ).
cnf(hyp17,hypothesis,
a_1330 = store(a_1328,i0,e_1329) ).
cnf(u170,hypothesis,
e_1339 = e_1341 ).
cnf(hyp8,hypothesis,
a_1313 = store(a_1311,i7,e_1312) ).
cnf(u1006,hypothesis,
a_1324 = store(a_1322,i1,e_1318) ).
cnf(u335,hypothesis,
e_1331 = select(a_1332,i8) ).
cnf(u1610,negated_conjecture,
e_1296 != e_1298 ).
cnf(u555,hypothesis,
e_1323 = select(a_1322,i5) ).
cnf(u834,hypothesis,
a_1330 = store(a_1328,i1,e_1325) ).
cnf(hyp10,hypothesis,
a_1317 = store(a_1315,i4,e_1316) ).
cnf(hyp4,hypothesis,
a_1305 = store(a_1303,i8,e_1304) ).
cnf(u858,hypothesis,
e_1296 = select(a_1307,i7) ).
cnf(u122,hypothesis,
e_1370 = select(a_1371,i9) ).
cnf(u152,hypothesis,
( select(a_1350,X0) = select(a_1352,X0)
| i7 = X0 ) ).
cnf(u121,hypothesis,
e_1368 = select(a_1369,i6) ).
cnf(u159,hypothesis,
( select(a_1363,X0) = select(a_1365,X0)
| i3 = X0 ) ).
cnf(u124,hypothesis,
( select(a_1297,X0) = select(a1,X0)
| i8 = X0 ) ).
cnf(u1671,hypothesis,
( select(a_1354,X0) = select(a_1356,X0)
| i7 = X0 ) ).
cnf(u831,hypothesis,
e_1325 = select(a_1330,i1) ).
cnf(u146,hypothesis,
( select(a_1338,X0) = select(a_1340,X0)
| i8 = X0 ) ).
cnf(u115,hypothesis,
e_1357 = select(a_1358,i0) ).
cnf(u145,hypothesis,
( select(a_1336,X0) = select(a_1338,X0)
| i6 = X0 ) ).
cnf(u2164,hypothesis,
e_1298 = select(a_1322,i8) ).
cnf(u118,hypothesis,
e_1362 = select(a_1363,i1) ).
cnf(u128,hypothesis,
( select(a_1303,X0) = select(a_1305,X0)
| i8 = X0 ) ).
cnf(u117,hypothesis,
e_1360 = select(a_1361,i2) ).
cnf(u872,hypothesis,
e_1362 = select(a_1358,i7) ).
cnf(u104,hypothesis,
e_1296 = select(a_1336,i8) ).
cnf(u1753,hypothesis,
e_1296 = select(a_1340,i8) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWV538-1.010 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.07/0.19 % Computer : n026.cluster.edu
% 0.07/0.19 % Model : x86_64 x86_64
% 0.07/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.19 % Memory : 8046.5625MB
% 0.07/0.19 % OS : Linux 6.8.0-71-generic
% 0.07/0.19 % CPULimit : 300
% 0.07/0.19 % WCLimit : 300
% 0.07/0.19 % DateTime : Mon Sep 28 11:40:57 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
% 3.02/1.12 % (3799238)Input is clausal, will run a generic CNF schedule.
% 3.02/1.12 % (3799244)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=4170561264:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 3.02/1.12 % (3799243)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=932494208:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 3.02/1.12 % (3799248)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=918035314:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 3.02/1.12 % (3799249)dis-21_1_sil=8000:lcm=predicate:random_seed=89441793: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)
% 3.02/1.12 % (3799246)lrs+10_1_sil=8000:sp=occurrence:random_seed=482123366:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 3.02/1.12 % (3799245)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=3071016913:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 3.02/1.12 % (3799247)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=2992984997:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 3.02/1.12 % (3799249)Refutation not found, incomplete strategy
% 3.02/1.12 % (3799249)------------------------------
% 3.02/1.12 % (3799249)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.02/1.12 % (3799249)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.02/1.12 % (3799249)CaDiCaL version: 2.1.3
% 3.02/1.12 % (3799249)Termination reason: Refutation not found, incomplete strategy
% 3.02/1.12 % (3799249)Time elapsed: 0.002 s
% 3.02/1.12 % (3799249)Peak memory usage: 88 MB
% 3.02/1.12 % (3799249)Instructions burned: 2 (million)
% 3.02/1.12 % (3799246)First to succeed.
% 3.02/1.12 % (3799246)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-3799238"
% 3.02/1.12 % (3799247)Instruction limit reached!
% 3.02/1.12 % (3799247)------------------------------
% 3.02/1.12 % (3799247)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.02/1.12 % (3799247)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.02/1.12 % (3799247)CaDiCaL version: 2.1.3
% 3.02/1.12 % (3799247)Termination reason: Instruction limit
% 3.02/1.12 % (3799247)Termination phase: Saturation
% 3.02/1.12 % (3799247)Time elapsed: 0.066 s
% 3.02/1.12 % (3799247)Peak memory usage: 89 MB
% 3.02/1.12 % (3799247)Instructions burned: 114 (million)
% 3.02/1.12 % (3799248)Refutation not found, incomplete strategy
% 3.02/1.12 % (3799248)------------------------------
% 3.02/1.12 % (3799248)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.02/1.12 % (3799248)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.02/1.12 % (3799248)CaDiCaL version: 2.1.3
% 3.02/1.12 % (3799248)Termination reason: Refutation not found, incomplete strategy
% 3.02/1.12 % (3799248)Time elapsed: 0.067 s
% 3.02/1.12 % (3799248)Peak memory usage: 89 MB
% 3.02/1.12 % (3799248)Instructions burned: 114 (million)
% 3.02/1.12 % (3799257)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=2795804258:i=143:sd=2:aac=none:ss=axioms:sgt=16_2997 on theBenchmark for (2997ds/143Mi)
% 3.02/1.12 % (3799249)------------------------------
% 3.02/1.12 % (3799249)------------------------------
% 3.02/1.12 % SZS status Satisfiable for theBenchmark
% 3.02/1.12 % SZS output start Saturation.
% See solution above
% 3.86/1.32 % SZS output start Definitions and Model Updates.
% 3.86/1.32 % SZS output end Definitions and Model Updates.
% 3.86/1.32 % (3799246)------------------------------
% 3.86/1.32 % (3799246)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.86/1.32 % (3799246)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.86/1.32 % (3799246)CaDiCaL version: 2.1.3
% 3.86/1.32 % (3799246)Termination reason: Satisfiable
% 3.86/1.32 % (3799246)Time elapsed: 0.048 s
% 3.86/1.32 % (3799246)Peak memory usage: 89 MB
% 3.86/1.32 % (3799246)Instructions burned: 82 (million)
% 3.86/1.32 % (3799246)------------------------------
% 3.86/1.32 % (3799246)------------------------------
% 3.86/1.32 % (3799238)Success in time 0.456 s
% 3.86/1.32 % Vampire exiting
%------------------------------------------------------------------------------