%------------------------------------------------------------------------------
% File : Vampire-SAT---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/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n017.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:25:08 PM UTC 2026
% Result : Satisfiable 0.94s 0.46s
% Output : Saturation 0.94s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(u187,hypothesis,
i8 != i7 ).
cnf(u192,hypothesis,
e_1296 = e_1300 ).
cnf(u300,hypothesis,
i8 != i6 ).
cnf(u377,hypothesis,
i8 != i5 ).
cnf(u382,hypothesis,
e_1304 = select(a_1307,i8) ).
cnf(u522,hypothesis,
e_1308 = select(a_1311,i4) ).
cnf(u595,hypothesis,
i8 != i1 ).
cnf(u733,hypothesis,
e_1327 = select(a_1330,i3) ).
cnf(u1841,hypothesis,
i8 != i_1372 ).
cnf(u2170,hypothesis,
e_1364 = select(a_1367,i3) ).
cnf(u2180,hypothesis,
e_1323 = select(a_1326,i1) ).
cnf(u2190,hypothesis,
e_1318 = select(a_1322,i5) ).
cnf(u2196,hypothesis,
e_1300 = select(a_1303,i6) ).
cnf(u2206,hypothesis,
e_1312 = select(a_1315,i7) ).
cnf(u2230,hypothesis,
e_1316 = select(a_1319,i4) ).
cnf(u2242,hypothesis,
e_1316 = select(a_1322,i4) ).
cnf(u2258,hypothesis,
e_1331 = select(a_1334,i9) ).
cnf(u2286,hypothesis,
e_1345 = select(a_1348,i4) ).
cnf(u2296,hypothesis,
e_1349 = select(a_1352,i1) ).
cnf(u2306,hypothesis,
e_1353 = select(a_1356,i4) ).
cnf(u2316,hypothesis,
e_1360 = select(a_1363,i2) ).
cnf(u2332,hypothesis,
e_1368 = select(a_1371,i6) ).
cnf(u2342,hypothesis,
e_1353 = select(a_1359,i4) ).
cnf(u2347,hypothesis,
e_1355 = select(a_1359,i5) ).
cnf(u2362,hypothesis,
e_1302 = select(a1,i6) ).
cnf(u2376,hypothesis,
e_1304 = select(a_1299,i5) ).
cnf(u2390,hypothesis,
e_1304 = select(a1,i5) ).
cnf(u2404,hypothesis,
e_1308 = select(a_1303,i9) ).
cnf(u2409,hypothesis,
e_1310 = select(a_1303,i4) ).
cnf(u2418,hypothesis,
e_1308 = select(a_1299,i9) ).
cnf(u2430,hypothesis,
e_1310 = select(a_1299,i4) ).
cnf(u2442,hypothesis,
e_1308 = select(a1,i9) ).
cnf(u2454,hypothesis,
e_1310 = select(a1,i4) ).
cnf(u2472,hypothesis,
e_1312 = select(a_1307,i1) ).
cnf(u2477,hypothesis,
e_1314 = select(a_1307,i7) ).
cnf(u2492,hypothesis,
e_1312 = select(a_1303,i1) ).
cnf(u2502,hypothesis,
e_1314 = select(a_1303,i7) ).
cnf(u2516,hypothesis,
e_1312 = select(a_1299,i1) ).
cnf(u2528,hypothesis,
e_1298 = e_1314 ).
cnf(u2539,hypothesis,
e_1312 = select(a1,i1) ).
cnf(u2561,hypothesis,
e_1333 = select(a_1326,i9) ).
cnf(u2570,hypothesis,
e_1331 = select(a_1326,i5) ).
cnf(u2582,hypothesis,
e_1316 = select(a_1311,i5) ).
cnf(u2589,hypothesis,
e_1308 = e_1318 ).
cnf(u2600,hypothesis,
e_1302 = e_1316 ).
cnf(u2627,hypothesis,
e_1320 = select(a_1315,i0) ).
cnf(u2643,hypothesis,
e_1320 = select(a_1311,i0) ).
cnf(u2651,hypothesis,
e_1320 = select(a_1307,i0) ).
cnf(u2659,hypothesis,
e_1320 = select(a_1303,i0) ).
cnf(u2671,hypothesis,
e_1320 = select(a_1299,i0) ).
cnf(u2679,hypothesis,
e_1320 = select(a1,i0) ).
cnf(u2701,hypothesis,
e_1329 = select(a_1322,i3) ).
cnf(u2711,hypothesis,
e_1333 = select(a_1322,i9) ).
cnf(u2725,hypothesis,
e_1320 = e_1327 ).
cnf(u2737,hypothesis,
e_1308 = e_1331 ).
cnf(u2767,hypothesis,
i5 = i_1372 ).
cnf(u2783,hypothesis,
e_1302 = e_1339 ).
cnf(u2814,hypothesis,
e_1343 = select(a_1336,i5) ).
cnf(u2826,hypothesis,
e_1304 = e_1343 ).
cnf(u2841,hypothesis,
e_1345 = select(a_1340,i9) ).
cnf(u2846,hypothesis,
e_1347 = select(a_1340,i4) ).
cnf(u2855,hypothesis,
e_1345 = select(a_1336,i9) ).
cnf(u2863,hypothesis,
e_1347 = select(a_1336,i4) ).
cnf(u2873,hypothesis,
e_1308 = e_1345 ).
cnf(u2884,hypothesis,
e_1310 = e_1347 ).
cnf(u2907,hypothesis,
e_1351 = select(a_1344,i1) ).
cnf(u2912,hypothesis,
e_1349 = select(a_1344,i7) ).
cnf(u2923,hypothesis,
e_1351 = select(a_1340,i1) ).
cnf(u2933,hypothesis,
e_1349 = select(a_1340,i7) ).
cnf(u2943,hypothesis,
e_1351 = select(a_1336,i1) ).
cnf(u2955,hypothesis,
e_1298 = e_1349 ).
cnf(u2968,hypothesis,
e_1312 = e_1351 ).
cnf(u2992,hypothesis,
e_1353 = select(a_1348,i5) ).
cnf(u3001,hypothesis,
e_1308 = e_1355 ).
cnf(u3014,hypothesis,
e_1302 = e_1353 ).
cnf(u3041,hypothesis,
e_1357 = select(a_1352,i0) ).
cnf(u3049,hypothesis,
e_1357 = select(a_1348,i0) ).
cnf(u3057,hypothesis,
e_1357 = select(a_1344,i0) ).
cnf(u3065,hypothesis,
e_1357 = select(a_1340,i0) ).
cnf(u3073,hypothesis,
e_1357 = select(a_1336,i0) ).
cnf(u3083,hypothesis,
e_1320 = e_1357 ).
cnf(u3103,hypothesis,
e_1366 = select(a_1359,i3) ).
cnf(u3113,hypothesis,
e_1320 = e_1364 ).
cnf(u3132,hypothesis,
e_1368 = select(a_1363,i9) ).
cnf(u3141,hypothesis,
e_1370 = select(a_1363,i6) ).
cnf(u3150,hypothesis,
e_1368 = select(a_1359,i9) ).
cnf(u3162,hypothesis,
e_1370 = select(a_1359,i6) ).
cnf(u3173,hypothesis,
e_1374 = select(a_1367,i5) ).
cnf(u3188,hypothesis,
e_1374 = select(a_1363,i5) ).
cnf(u3200,hypothesis,
e_1308 = e_1374 ).
cnf(u3220,hypothesis,
e_1329 = select(a_1315,i3) ).
cnf(u3229,hypothesis,
e_1323 = select(a_1315,i2) ).
cnf(u3235,hypothesis,
e_1333 = select(a_1315,i9) ).
cnf(u3246,hypothesis,
e_1298 = e_1325 ).
cnf(u3259,hypothesis,
e_1329 = select(a_1311,i3) ).
cnf(u3271,hypothesis,
e_1323 = select(a_1311,i2) ).
cnf(u3281,hypothesis,
e_1310 = e_1333 ).
cnf(u3291,hypothesis,
e_1329 = select(a_1307,i3) ).
cnf(u3299,hypothesis,
e_1323 = select(a_1307,i2) ).
cnf(u3311,hypothesis,
e_1329 = select(a_1303,i3) ).
cnf(u3319,hypothesis,
e_1323 = select(a_1303,i2) ).
cnf(u3327,hypothesis,
e_1329 = select(a_1299,i3) ).
cnf(u3335,hypothesis,
e_1323 = select(a_1299,i2) ).
cnf(u3343,hypothesis,
e_1329 = select(a1,i3) ).
cnf(u3351,hypothesis,
e_1323 = select(a1,i2) ).
cnf(u3367,hypothesis,
e_1366 = select(a_1352,i3) ).
cnf(u3372,hypothesis,
e_1362 = select(a_1352,i2) ).
cnf(u3378,hypothesis,
e_1368 = select(a_1352,i9) ).
cnf(u3383,hypothesis,
e_1370 = select(a_1352,i6) ).
cnf(u3395,hypothesis,
e_1298 = e_1360 ).
cnf(u3404,hypothesis,
e_1366 = select(a_1348,i3) ).
cnf(u3412,hypothesis,
e_1362 = select(a_1348,i2) ).
cnf(u3424,hypothesis,
e_1310 = e_1368 ).
cnf(u3433,hypothesis,
e_1370 = select(a_1348,i6) ).
cnf(u3441,hypothesis,
e_1366 = select(a_1344,i3) ).
cnf(u3449,hypothesis,
e_1362 = select(a_1344,i2) ).
cnf(u3457,hypothesis,
e_1370 = select(a_1344,i6) ).
cnf(u3465,hypothesis,
e_1366 = select(a_1340,i3) ).
cnf(u3473,hypothesis,
e_1362 = select(a_1340,i2) ).
cnf(u3485,hypothesis,
e_1296 = e_1370 ).
cnf(u3494,hypothesis,
e_1366 = select(a_1336,i3) ).
cnf(u3502,hypothesis,
e_1362 = select(a_1336,i2) ).
cnf(u3512,hypothesis,
e_1329 = e_1366 ).
cnf(u3523,hypothesis,
e_1323 = e_1362 ).
cnf(u98,hypothesis,
e_1323 = select(a_1324,i1) ).
cnf(u3118,hypothesis,
e_1320 = select(a_1365,i3) ).
cnf(u160,hypothesis,
( select(a_1359,X0) = select(a_1361,X0)
| i2 = X0 ) ).
cnf(u2740,hypothesis,
a_1328 = store(a_1326,i3,e_1320) ).
cnf(hyp53,hypothesis,
e_1323 = select(a_1322,i2) ).
cnf(hyp60,hypothesis,
e_1339 = select(a_1336,i6) ).
cnf(u2212,hypothesis,
e_1296 = select(a_1301,i6) ).
cnf(hyp47,hypothesis,
e_1310 = select(a_1307,i4) ).
cnf(u2971,hypothesis,
a_1352 = store(a_1350,i7,e_1312) ).
cnf(u156,hypothesis,
( select(a_1352,X0) = select(a_1354,X0)
| i4 = X0 ) ).
cnf(u2897,hypothesis,
e_1310 = select(a_1348,i9) ).
cnf(u2829,hypothesis,
a_1344 = store(a_1342,i8,e_1304) ).
cnf(hyp77,hypothesis,
e_1374 = select(a_1371,i_1372) ).
cnf(hyp46,hypothesis,
e_1308 = select(a_1307,i9) ).
cnf(u2268,hypothesis,
( select(a_1336,X0) = select(a_1340,X0)
| i8 = X0
| i6 = X0 ) ).
cnf(u139,hypothesis,
( select(a_1319,X0) = select(a_1321,X0)
| i0 = X0 ) ).
cnf(u2322,hypothesis,
( select(a_1367,X0) = select(a_1371,X0)
| i9 = X0
| i6 = X0 ) ).
cnf(u142,hypothesis,
( select(a_1324,X0) = select(a_1326,X0)
| i2 = X0 ) ).
cnf(u2605,hypothesis,
e_1308 = select(a_1319,i5) ).
cnf(u3093,hypothesis,
e_1320 = select(a_1359,i0) ).
cnf(u164,hypothesis,
( select(a_1367,X0) = select(a_1369,X0)
| i6 = X0 ) ).
cnf(u135,hypothesis,
( select(a_1311,X0) = select(a_1313,X0)
| i7 = X0 ) ).
cnf(u100,hypothesis,
e_1327 = select(a_1328,i3) ).
cnf(u91,hypothesis,
e_1310 = select(a_1311,i9) ).
cnf(u93,hypothesis,
e_1314 = select(a_1315,i1) ).
cnf(u87,hypothesis,
e_1302 = select(a_1303,i8) ).
cnf(u2277,hypothesis,
e_1339 = select(a_1344,i5) ).
cnf(hyp49,hypothesis,
e_1314 = select(a_1311,i7) ).
cnf(hyp71,hypothesis,
e_1362 = select(a_1359,i2) ).
cnf(hyp23,hypothesis,
a_1340 = store(a_1338,i8,e_1339) ).
cnf(hyp40,hypothesis,
e_1296 = select(a1,i7) ).
cnf(hyp70,hypothesis,
e_1360 = select(a_1359,i1) ).
cnf(hyp43,hypothesis,
e_1302 = select(a_1299,i6) ).
cnf(hyp73,hypothesis,
e_1366 = select(a_1363,i3) ).
cnf(hyp42,hypothesis,
e_1300 = select(a_1299,i8) ).
cnf(hyp64,hypothesis,
e_1347 = select(a_1344,i4) ).
cnf(hyp29,hypothesis,
a_1352 = store(a_1350,i7,e_1351) ).
cnf(u3017,hypothesis,
a_1354 = store(a_1352,i4,e_1302) ).
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(hyp22,hypothesis,
a_1338 = store(a_1336,i6,e_1337) ).
cnf(u2531,hypothesis,
a_1315 = store(a_1313,i1,e_1298) ).
cnf(hyp25,hypothesis,
a_1344 = store(a_1342,i8,e_1343) ).
cnf(u2210,hypothesis,
e_1296 = select(a_1303,i6) ).
cnf(u153,hypothesis,
( select(a_1346,X0) = select(a_1348,X0)
| i9 = X0 ) ).
cnf(hyp16,hypothesis,
a_1328 = store(a_1326,i3,e_1327) ).
cnf(u3528,hypothesis,
e_1298 = select(a_1326,i2) ).
cnf(hyp19,hypothesis,
a_1334 = store(a_1332,i5,e_1333) ).
cnf(hyp18,hypothesis,
a_1332 = store(a_1330,i9,e_1331) ).
cnf(u2592,hypothesis,
a_1319 = store(a_1317,i5,e_1308) ).
cnf(hyp5,hypothesis,
a_1307 = store(a_1305,i5,e_1306) ).
cnf(hyp12,hypothesis,
a_1321 = store(a_1319,i0,e_1320) ).
cnf(a2,axiom,
( select(store(X2,X0,X3),X1) = select(X2,X1)
| X0 = X1 ) ).
cnf(u2543,hypothesis,
e_1298 = select(a_1315,i1) ).
cnf(a1,axiom,
select(store(X0,X1,X2),X1) = X2 ).
cnf(u143,hypothesis,
( select(a_1326,X0) = select(a_1328,X0)
| i3 = X0 ) ).
cnf(goal,negated_conjecture,
e_1373 != e_1374 ).
cnf(u112,hypothesis,
e_1351 = select(a_1352,i7) ).
cnf(u155,hypothesis,
( select(a_1350,X0) = select(a_1352,X0)
| i7 = X0 ) ).
cnf(u512,hypothesis,
( select(a_1307,X0) = select(a_1311,X0)
| i9 = X0
| i4 = X0 ) ).
cnf(u129,hypothesis,
( select(a_1299,X0) = select(a_1301,X0)
| i6 = X0 ) ).
cnf(u2973,hypothesis,
e_1298 = select(a_1350,i1) ).
cnf(u3427,hypothesis,
a_1369 = store(a_1367,i6,e_1310) ).
cnf(u2887,hypothesis,
a_1348 = store(a_1346,i9,e_1310) ).
cnf(u3204,negated_conjecture,
e_1308 != e_1333 ).
cnf(u3249,hypothesis,
a_1326 = store(a_1324,i2,e_1298) ).
cnf(u2247,hypothesis,
( select(a_1330,X0) = select(a_1334,X0)
| i5 = X0
| i9 = X0 ) ).
cnf(hyp48,hypothesis,
e_1312 = select(a_1311,i1) ).
cnf(u88,hypothesis,
e_1304 = select(a_1305,i8) ).
cnf(u3087,hypothesis,
a_1359 = store(a_1358,i0,e_1320) ).
cnf(u723,hypothesis,
( select(a_1326,X0) = select(a_1330,X0)
| i0 = X0
| i3 = X0 ) ).
cnf(u171,hypothesis,
e_1339 = e_1341 ).
cnf(u174,hypothesis,
e_1339 = select(a_1342,i5) ).
cnf(u173,hypothesis,
a_1342 = store(a_1340,i5,e_1339) ).
cnf(u2741,hypothesis,
a_1332 = store(a_1330,i9,e_1308) ).
cnf(u167,hypothesis,
e_1296 = e_1337 ).
cnf(hyp1,hypothesis,
a_1299 = store(a_1297,i7,e_1298) ).
cnf(u154,hypothesis,
( select(a_1348,X0) = select(a_1350,X0)
| i1 = X0 ) ).
cnf(u123,hypothesis,
e_1302 = e_1306 ).
cnf(u126,hypothesis,
( select(a_1297,X0) = select(a_1299,X0)
| i7 = X0 ) ).
cnf(u125,hypothesis,
a_1307 = store(a_1305,i5,e_1302) ).
cnf(u147,hypothesis,
( select(a_1335,X0) = select(a_1336,X0)
| i8 = X0 ) ).
cnf(u2789,hypothesis,
e_1302 = select(a_1342,i5) ).
cnf(u150,hypothesis,
( select(a_1340,X0) = select(a_1342,X0)
| i5 = X0 ) ).
cnf(u119,hypothesis,
e_1364 = select(a_1365,i3) ).
cnf(u149,hypothesis,
( select(a_1338,X0) = select(a_1340,X0)
| i8 = X0 ) ).
cnf(u106,hypothesis,
e_1339 = select(a_1340,i8) ).
cnf(u136,hypothesis,
( select(a_1313,X0) = select(a_1315,X0)
| i1 = X0 ) ).
cnf(u3552,hypothesis,
e_1296 = select(a_1371,i9) ).
cnf(u108,hypothesis,
e_1343 = select(a_1344,i8) ).
cnf(u130,hypothesis,
( select(a_1301,X0) = select(a_1303,X0)
| i8 = X0 ) ).
cnf(u99,hypothesis,
e_1325 = select(a_1326,i2) ).
cnf(u2217,hypothesis,
( select(a_1311,X0) = select(a_1315,X0)
| i7 = X0
| i1 = X0 ) ).
cnf(u102,hypothesis,
e_1331 = select(a_1332,i9) ).
cnf(u132,hypothesis,
( select(a_1305,X0) = select(a_1307,X0)
| i5 = X0 ) ).
cnf(u101,hypothesis,
e_1329 = select(a_1330,i0) ).
cnf(hyp55,hypothesis,
e_1327 = select(a_1326,i0) ).
cnf(hyp54,hypothesis,
e_1325 = select(a_1322,i1) ).
cnf(u2797,hypothesis,
e_1302 = select(a_1340,i8) ).
cnf(u95,hypothesis,
e_1318 = select(a_1319,i5) ).
cnf(hyp57,hypothesis,
e_1331 = select(a_1330,i5) ).
cnf(u158,hypothesis,
( select(a_1356,X0) = select(a_1358,X0)
| i0 = X0 ) ).
cnf(hyp78,hypothesis,
i_1372 = sk(a_1334,a_1371) ).
cnf(hyp51,hypothesis,
e_1318 = select(a_1315,i4) ).
cnf(hyp50,hypothesis,
e_1316 = select(a_1315,i5) ).
cnf(hyp37,hypothesis,
a_1367 = store(a_1365,i0,e_1366) ).
cnf(u141,hypothesis,
( select(a_1322,X0) = select(a_1324,X0)
| i1 = X0 ) ).
cnf(hyp44,hypothesis,
e_1304 = select(a_1303,i5) ).
cnf(u3540,hypothesis,
e_1310 = select(a_1334,i5) ).
cnf(u162,hypothesis,
( select(a_1363,X0) = select(a_1365,X0)
| i3 = X0 ) ).
cnf(hyp31,hypothesis,
a_1356 = store(a_1354,i5,e_1355) ).
cnf(u161,hypothesis,
( select(a_1361,X0) = select(a_1363,X0)
| i1 = X0 ) ).
cnf(hyp75,hypothesis,
e_1370 = select(a_1367,i6) ).
cnf(u2262,hypothesis,
( select(a1,X0) = select(a_1336,X0)
| i8 = X0
| i7 = X0 ) ).
cnf(u3284,negated_conjecture,
e_1308 != e_1310 ).
cnf(u3027,hypothesis,
e_1302 = select(a_1354,i4) ).
cnf(u2751,hypothesis,
e_1308 = select(a_1332,i9) ).
cnf(u3116,hypothesis,
a_1365 = store(a_1363,i3,e_1320) ).
cnf(u2319,hypothesis,
( select(a_1363,X0) = select(a_1367,X0)
| i3 = X0
| i0 = X0 ) ).
cnf(u114,hypothesis,
e_1355 = select(a_1356,i5) ).
cnf(u3034,hypothesis,
( select(a_1352,X0) = select(a_1359,X0)
| i5 = X0
| i4 = X0
| i0 = X0 ) ).
cnf(u84,hypothesis,
e_1296 = select(a_1297,i8) ).
cnf(u2300,hypothesis,
( select(a_1352,X0) = select(a_1356,X0)
| i5 = X0
| i4 = X0 ) ).
cnf(hyp72,hypothesis,
e_1364 = select(a_1363,i0) ).
cnf(u2265,hypothesis,
e_1298 = select(a_1336,i7) ).
cnf(hyp74,hypothesis,
e_1368 = select(a_1367,i9) ).
cnf(hyp61,hypothesis,
e_1341 = select(a_1340,i8) ).
cnf(hyp30,hypothesis,
a_1354 = store(a_1352,i4,e_1353) ).
cnf(hyp68,hypothesis,
e_1355 = select(a_1352,i4) ).
cnf(u785,hypothesis,
( select(a_1356,X0) = select(a_1359,X0)
| i0 = X0 ) ).
cnf(hyp33,hypothesis,
a_1359 = store(a_1358,i0,e_1357) ).
cnf(u3556,hypothesis,
e_1329 = select(a_1367,i0) ).
cnf(hyp24,hypothesis,
a_1342 = store(a_1340,i5,e_1341) ).
cnf(hyp27,hypothesis,
a_1348 = store(a_1346,i9,e_1347) ).
cnf(hyp26,hypothesis,
a_1346 = store(a_1344,i4,e_1345) ).
cnf(u2831,hypothesis,
e_1304 = select(a_1344,i8) ).
cnf(u157,hypothesis,
( select(a_1354,X0) = select(a_1356,X0)
| i5 = X0 ) ).
cnf(hyp13,hypothesis,
a_1322 = store(a_1321,i0,e_1320) ).
cnf(hyp20,hypothesis,
a_1335 = store(a1,i7,e_1298) ).
cnf(hyp7,hypothesis,
a_1311 = store(a_1309,i9,e_1310) ).
cnf(hyp6,hypothesis,
a_1309 = store(a_1307,i4,e_1308) ).
cnf(u144,hypothesis,
( select(a_1328,X0) = select(a_1330,X0)
| i0 = X0 ) ).
cnf(hyp9,hypothesis,
a_1315 = store(a_1313,i1,e_1314) ).
cnf(hyp0,hypothesis,
a_1297 = store(a1,i8,e_1296) ).
cnf(hyp3,hypothesis,
a_1303 = store(a_1301,i8,e_1302) ).
cnf(hyp2,hypothesis,
a_1301 = store(a_1299,i6,e_1300) ).
cnf(u120,hypothesis,
e_1366 = select(a_1367,i0) ).
cnf(u127,hypothesis,
( select(a_1297,X0) = select(a1,X0)
| i8 = X0 ) ).
cnf(u2771,hypothesis,
e_1374 = select(a_1371,i5) ).
cnf(u113,hypothesis,
e_1353 = select(a_1354,i4) ).
cnf(u134,hypothesis,
( select(a_1309,X0) = select(a_1311,X0)
| i9 = X0 ) ).
cnf(u3285,hypothesis,
a_1334 = store(a_1332,i5,e_1310) ).
cnf(u165,hypothesis,
( select(a_1369,X0) = select(a_1371,X0)
| i9 = X0 ) ).
cnf(u2743,hypothesis,
e_1320 = select(a_1328,i3) ).
cnf(u96,hypothesis,
e_1320 = select(a_1321,i0) ).
cnf(u2613,hypothesis,
e_1302 = select(a_1317,i4) ).
cnf(u3515,hypothesis,
a_1367 = store(a_1365,i0,e_1329) ).
cnf(u206,hypothesis,
( select(a_1299,X0) = select(a1,X0)
| i8 = X0
| i7 = X0 ) ).
cnf(u86,hypothesis,
e_1300 = select(a_1301,i6) ).
cnf(u2620,hypothesis,
( select(a_1315,X0) = select(a_1322,X0)
| i5 = X0
| i4 = X0
| i0 = X0 ) ).
cnf(u85,hypothesis,
e_1298 = select(a_1335,i7) ).
cnf(hyp59,hypothesis,
e_1337 = select(a_1336,i8) ).
cnf(u3488,hypothesis,
a_1371 = store(a_1369,i9,e_1296) ).
cnf(hyp76,hypothesis,
e_1373 = select(a_1334,i_1372) ).
cnf(hyp69,hypothesis,
e_1357 = select(a_1356,i0) ).
cnf(u2799,hypothesis,
e_1302 = e_1341 ).
cnf(u151,hypothesis,
( select(a_1342,X0) = select(a_1344,X0)
| i8 = X0 ) ).
cnf(u2271,hypothesis,
e_1296 = select(a_1340,i6) ).
cnf(u116,hypothesis,
e_1357 = select(a_1359,i0) ).
cnf(u138,hypothesis,
( select(a_1317,X0) = select(a_1319,X0)
| i5 = X0 ) ).
cnf(hyp63,hypothesis,
e_1345 = select(a_1344,i9) ).
cnf(u137,hypothesis,
( select(a_1315,X0) = select(a_1317,X0)
| i4 = X0 ) ).
cnf(u110,hypothesis,
e_1347 = select(a_1348,i9) ).
cnf(u140,hypothesis,
( select(a_1321,X0) = select(a_1322,X0)
| i0 = X0 ) ).
cnf(u109,hypothesis,
e_1345 = select(a_1346,i4) ).
cnf(u131,hypothesis,
( select(a_1303,X0) = select(a_1305,X0)
| i8 = X0 ) ).
cnf(u2773,hypothesis,
e_1333 = e_1373 ).
cnf(u103,hypothesis,
e_1333 = select(a_1334,i5) ).
cnf(u133,hypothesis,
( select(a_1307,X0) = select(a_1309,X0)
| i4 = X0 ) ).
cnf(u90,hypothesis,
e_1308 = select(a_1309,i4) ).
cnf(u2280,hypothesis,
( select(a_1344,X0) = select(a_1348,X0)
| i9 = X0
| i4 = X0 ) ).
cnf(hyp56,hypothesis,
e_1329 = select(a_1326,i3) ).
cnf(u92,hypothesis,
e_1312 = select(a_1313,i7) ).
cnf(u2274,hypothesis,
( select(a_1340,X0) = select(a_1344,X0)
| i8 = X0
| i5 = X0 ) ).
cnf(hyp58,hypothesis,
e_1333 = select(a_1330,i9) ).
cnf(u83,hypothesis,
e_1298 = select(a_1299,i7) ).
cnf(hyp45,hypothesis,
e_1306 = select(a_1303,i8) ).
cnf(hyp52,hypothesis,
e_1320 = select(a_1319,i0) ).
cnf(hyp39,hypothesis,
a_1371 = store(a_1369,i9,e_1370) ).
cnf(u3086,hypothesis,
a_1358 = store(a_1356,i0,e_1320) ).
cnf(hyp38,hypothesis,
a_1369 = store(a_1367,i6,e_1368) ).
cnf(hyp41,hypothesis,
e_1298 = select(a1,i8) ).
cnf(u2603,hypothesis,
a_1317 = store(a_1315,i4,e_1302) ).
cnf(hyp32,hypothesis,
a_1358 = store(a_1356,i0,e_1357) ).
cnf(hyp62,hypothesis,
e_1343 = select(a_1340,i5) ).
cnf(u3544,hypothesis,
e_1310 = select(a_1369,i6) ).
cnf(hyp35,hypothesis,
a_1363 = store(a_1361,i1,e_1362) ).
cnf(u2794,hypothesis,
e_1302 = select(a_1344,i5) ).
cnf(hyp65,hypothesis,
e_1349 = select(a_1348,i7) ).
cnf(hyp34,hypothesis,
a_1361 = store(a_1359,i2,e_1360) ).
cnf(hyp21,hypothesis,
a_1336 = store(a_1335,i8,e_1296) ).
cnf(hyp28,hypothesis,
a_1350 = store(a_1348,i1,e_1349) ).
cnf(u3398,hypothesis,
a_1361 = store(a_1359,i2,e_1298) ).
cnf(u152,hypothesis,
( select(a_1344,X0) = select(a_1346,X0)
| i4 = X0 ) ).
cnf(hyp15,hypothesis,
a_1326 = store(a_1324,i2,e_1325) ).
cnf(u2209,hypothesis,
a_1301 = store(a_1299,i6,e_1296) ).
cnf(u2220,hypothesis,
( select(a_1315,X0) = select(a_1319,X0)
| i5 = X0
| i4 = X0 ) ).
cnf(hyp14,hypothesis,
a_1324 = store(a_1322,i1,e_1323) ).
cnf(u372,hypothesis,
( select(a_1303,X0) = select(a_1307,X0)
| i5 = X0
| i8 = X0 ) ).
cnf(u148,hypothesis,
( select(a_1336,X0) = select(a_1338,X0)
| i6 = X0 ) ).
cnf(u94,hypothesis,
e_1316 = select(a_1317,i4) ).
cnf(u293,hypothesis,
( select(a_1299,X0) = select(a_1303,X0)
| i8 = X0
| i6 = X0 ) ).
cnf(u675,hypothesis,
( select(a_1319,X0) = select(a_1322,X0)
| i0 = X0 ) ).
cnf(u2958,hypothesis,
a_1350 = store(a_1348,i1,e_1298) ).
cnf(u2889,hypothesis,
e_1308 = select(a_1346,i4) ).
cnf(u3004,hypothesis,
a_1356 = store(a_1354,i5,e_1308) ).
cnf(u2290,hypothesis,
( select(a_1348,X0) = select(a_1352,X0)
| i7 = X0
| i1 = X0 ) ).
cnf(u3526,hypothesis,
a_1363 = store(a_1361,i1,e_1323) ).
cnf(u2981,hypothesis,
e_1312 = select(a_1352,i7) ).
cnf(u2876,hypothesis,
a_1346 = store(a_1344,i4,e_1308) ).
cnf(u97,hypothesis,
e_1320 = select(a_1322,i0) ).
cnf(u3019,hypothesis,
e_1308 = select(a_1356,i5) ).
cnf(hyp8,hypothesis,
a_1313 = store(a_1311,i7,e_1312) ).
cnf(u2787,hypothesis,
a_1340 = store(a_1338,i8,e_1302) ).
cnf(u2245,hypothesis,
( select(a_1322,X0) = select(a_1326,X0)
| i1 = X0
| i2 = X0 ) ).
cnf(hyp17,hypothesis,
a_1330 = store(a_1328,i0,e_1329) ).
cnf(u2310,hypothesis,
( select(a_1359,X0) = select(a_1363,X0)
| i1 = X0
| i2 = X0 ) ).
cnf(u170,hypothesis,
e_1296 = select(a_1338,i6) ).
cnf(u169,hypothesis,
a_1338 = store(a_1336,i6,e_1296) ).
cnf(u3560,hypothesis,
e_1323 = select(a_1363,i1) ).
cnf(hyp11,hypothesis,
a_1319 = store(a_1317,i5,e_1318) ).
cnf(hyp10,hypothesis,
a_1317 = store(a_1315,i4,e_1316) ).
cnf(u163,hypothesis,
( select(a_1365,X0) = select(a_1367,X0)
| i0 = X0 ) ).
cnf(u166,hypothesis,
e_1302 = select(a_1307,i5) ).
cnf(hyp4,hypothesis,
a_1305 = store(a_1303,i8,e_1304) ).
cnf(u122,hypothesis,
e_1370 = select(a_1371,i9) ).
cnf(u3532,hypothesis,
e_1298 = select(a_1361,i2) ).
cnf(u2786,hypothesis,
a_1342 = store(a_1340,i5,e_1302) ).
cnf(u121,hypothesis,
e_1368 = select(a_1369,i6) ).
cnf(u159,hypothesis,
( select(a_1358,X0) = select(a_1359,X0)
| i0 = X0 ) ).
cnf(u146,hypothesis,
( select(a_1332,X0) = select(a_1334,X0)
| i5 = X0 ) ).
cnf(u115,hypothesis,
e_1357 = select(a_1358,i0) ).
cnf(u145,hypothesis,
( select(a_1330,X0) = select(a_1332,X0)
| i9 = X0 ) ).
cnf(u118,hypothesis,
e_1362 = select(a_1363,i1) ).
cnf(u128,hypothesis,
( select(a1,X0) = select(a_1335,X0)
| i7 = X0 ) ).
cnf(u117,hypothesis,
e_1360 = select(a_1361,i2) ).
cnf(u104,hypothesis,
e_1296 = select(a_1336,i8) ).
cnf(u111,hypothesis,
e_1349 = select(a_1350,i1) ).
cnf(u3089,hypothesis,
e_1320 = select(a_1358,i0) ).
%------------------------------------------------------------------------------
%----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/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.09/0.18 % Computer : n017.cluster.edu
% 0.09/0.18 % Model : x86_64 x86_64
% 0.09/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.18 % Memory : 8046.5625MB
% 0.09/0.18 % OS : Linux 6.8.0-71-generic
% 0.09/0.18 % CPULimit : 300
% 0.09/0.18 % WCLimit : 300
% 0.09/0.18 % DateTime : Mon Sep 28 11:33:36 UTC 2026
% 0.09/0.18 % CPUTime :
% 0.09/0.18 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.09/0.22 Running first-order model finding
% 0.09/0.22 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.94/0.45 % (3491251)Will run a generic schedule for satisfiability detection.
% 0.94/0.45 % (3491258)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3324347810:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 0.94/0.45 % (3491257)% WARNING: option uhcvi not known.
% 0.94/0.45 % (3491256)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1373985660_2999 on theBenchmark for (2999ds/0Mi)
% 0.94/0.45 % (3491257)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3399272013:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 0.94/0.45 % (3491259)dis+10_1_sil=32000:sp=arity:random_seed=258348822:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 0.94/0.45 % (3491260)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3539200113:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 0.94/0.45 % (3491261)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2361216292:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 0.94/0.45 % (3491262)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2170182382:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 0.94/0.45 % TRYING [1]
% 0.94/0.45 % TRYING [2]
% 0.94/0.45 % TRYING [3]
% 0.94/0.45 % TRYING [4]
% 0.94/0.45 % TRYING [5]
% 0.94/0.45 % (3491259)Instruction limit reached!
% 0.94/0.45 % (3491259)------------------------------
% 0.94/0.45 % (3491259)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.94/0.45 % (3491259)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.94/0.45 % (3491259)CaDiCaL version: 2.1.3
% 0.94/0.45 % (3491259)Termination reason: Instruction limit
% 0.94/0.45 % (3491259)Termination phase: Saturation
% 0.94/0.45 % (3491259)Time elapsed: 0.058 s
% 0.94/0.45 % (3491259)Peak memory usage: 12 MB
% 0.94/0.45 % (3491259)Instructions burned: 104 (million)
% 0.94/0.45 % (3491260)Instruction limit reached!
% 0.94/0.45 % (3491260)------------------------------
% 0.94/0.45 % (3491260)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.94/0.45 % (3491260)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.94/0.45 % (3491260)CaDiCaL version: 2.1.3
% 0.94/0.45 % (3491260)Termination reason: Instruction limit
% 0.94/0.45 % (3491260)Termination phase: Saturation
% 0.94/0.45 % (3491260)Time elapsed: 0.063 s
% 0.94/0.45 % (3491260)Peak memory usage: 12 MB
% 0.94/0.45 % (3491260)Instructions burned: 116 (million)
% 0.94/0.45 % (3491261)Instruction limit reached!
% 0.94/0.45 % (3491261)------------------------------
% 0.94/0.45 % (3491261)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.94/0.45 % (3491261)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.94/0.45 % (3491261)CaDiCaL version: 2.1.3
% 0.94/0.45 % (3491261)Termination reason: Instruction limit
% 0.94/0.45 % (3491261)Termination phase: Saturation
% 0.94/0.45 % (3491261)Time elapsed: 0.076 s
% 0.94/0.45 % (3491261)Peak memory usage: 13 MB
% 0.94/0.45 % (3491261)Instructions burned: 132 (million)
% 0.94/0.45 % (3491270)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=2098854159:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 0.94/0.45 % (3491271)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=1301978865:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 0.94/0.45 % TRYING [1]
% 0.94/0.45 % TRYING [2]
% 0.94/0.45 % TRYING [6]
% 0.94/0.45 % TRYING [3]
% 0.94/0.45 % (3491262)Instruction limit reached!
% 0.94/0.45 % (3491262)------------------------------
% 0.94/0.45 % (3491262)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.94/0.45 % (3491262)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.94/0.45 % (3491262)CaDiCaL version: 2.1.3
% 0.94/0.45 % (3491262)Termination reason: Instruction limit
% 0.94/0.45 % (3491262)Termination phase: Saturation
% 0.94/0.45 % (3491262)Time elapsed: 0.096 s
% 0.94/0.45 % (3491262)Peak memory usage: 13 MB
% 0.94/0.45 % (3491262)Instructions burned: 160 (million)
% 0.94/0.45 % TRYING [4]
% 0.94/0.45 % (3491273)dis+11_32_anc=none:slsqr=2,1:sil=64000:sas=cadical:lma=off:lsd=50:s2agt=8:slsqc=1:kmz=on:newcnf=on:slsq=on:random_seed=63427038:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 0.94/0.45 % (3491276)ott-21_1_sil=16000:fs=off:random_seed=1420545727:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 0.94/0.45 % TRYING [5]
% 0.94/0.45 % (3491271)Instruction limit reached!
% 0.94/0.45 % (3491271)------------------------------
% 0.94/0.45 % (3491271)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.94/0.46 % (3491271)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.94/0.46 % (3491271)CaDiCaL version: 2.1.3
% 0.94/0.46 % (3491271)Termination reason: Instruction limit
% 0.94/0.46 % (3491271)Termination phase: Saturation
% 0.94/0.46 % (3491271)Time elapsed: 0.073 s
% 0.94/0.46 % (3491271)Peak memory usage: 12 MB
% 0.94/0.46 % (3491271)Instructions burned: 132 (million)
% 0.94/0.46 % (3491278)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=960301556:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 0.94/0.46 % (3491273) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-3491251-3491273"...
% 0.94/0.46 % (3491273)...printing done.
% 0.94/0.46 % SZS status Satisfiable for theBenchmark
% 0.94/0.46 % SZS output start Saturation.
% See solution above
% 0.94/0.46 % SZS output start Definitions and Model Updates.
% 0.94/0.46 % SZS output end Definitions and Model Updates.
% 0.94/0.46 % (3491273)------------------------------
% 0.94/0.46 % (3491273)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.94/0.46 % (3491273)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.94/0.46 % (3491273)CaDiCaL version: 2.1.3
% 0.94/0.46 % (3491273)Termination reason: Satisfiable
% 0.94/0.46 % (3491273)Time elapsed: 0.088 s
% 0.94/0.46 % (3491273)Peak memory usage: 14 MB
% 0.94/0.46 % (3491273)Instructions burned: 149 (million)
% 0.94/0.46 % (3491251)Success in time 0.23 s
% 0.94/0.46 % Vampire exiting
%------------------------------------------------------------------------------