%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SYN520+1 : TPTP v9.3.1. Released v2.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n008.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 02:17:26 PM UTC 2026
% Result : CounterSatisfiable 0.21s 0.33s
% Output : FiniteModel 0.21s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
tff('declare_$i1',type,
'fmb_$i_1': $i ).
tff('declare_$i2',type,
'fmb_$i_2': $i ).
tff('declare_$i3',type,
'fmb_$i_3': $i ).
tff('finite_domain_$i',axiom,
! [X: $i] :
( ( X = 'fmb_$i_1' )
| ( X = 'fmb_$i_2' )
| ( X = 'fmb_$i_3' ) ) ).
tff('distinct_domain_$i',axiom,
( ( 'fmb_$i_1' != 'fmb_$i_2' )
& ( 'fmb_$i_1' != 'fmb_$i_3' )
& ( 'fmb_$i_2' != 'fmb_$i_3' ) ) ).
tff(declare_a1323,type,
a1323: $i ).
tff(a1323_definition,axiom,
a1323 = 'fmb_$i_1' ).
tff(declare_a1324,type,
a1324: $i ).
tff(a1324_definition,axiom,
a1324 = 'fmb_$i_2' ).
tff(declare_a1325,type,
a1325: $i ).
tff(a1325_definition,axiom,
a1325 = 'fmb_$i_1' ).
tff(declare_a1326,type,
a1326: $i ).
tff(a1326_definition,axiom,
a1326 = 'fmb_$i_3' ).
tff(declare_a1327,type,
a1327: $i ).
tff(a1327_definition,axiom,
a1327 = 'fmb_$i_2' ).
tff(declare_a1328,type,
a1328: $i ).
tff(a1328_definition,axiom,
a1328 = 'fmb_$i_3' ).
tff(declare_a1329,type,
a1329: $i ).
tff(a1329_definition,axiom,
a1329 = 'fmb_$i_3' ).
tff(declare_a1330,type,
a1330: $i ).
tff(a1330_definition,axiom,
a1330 = 'fmb_$i_3' ).
tff(declare_a1331,type,
a1331: $i ).
tff(a1331_definition,axiom,
a1331 = 'fmb_$i_3' ).
tff(declare_a1332,type,
a1332: $i ).
tff(a1332_definition,axiom,
a1332 = 'fmb_$i_3' ).
tff(declare_a1333,type,
a1333: $i ).
tff(a1333_definition,axiom,
a1333 = 'fmb_$i_3' ).
tff(declare_a1334,type,
a1334: $i ).
tff(a1334_definition,axiom,
a1334 = 'fmb_$i_3' ).
tff(declare_a1335,type,
a1335: $i ).
tff(a1335_definition,axiom,
a1335 = 'fmb_$i_3' ).
tff(declare_a1336,type,
a1336: $i ).
tff(a1336_definition,axiom,
a1336 = 'fmb_$i_3' ).
tff(declare_a1337,type,
a1337: $i ).
tff(a1337_definition,axiom,
a1337 = 'fmb_$i_2' ).
tff(declare_a1338,type,
a1338: $i ).
tff(a1338_definition,axiom,
a1338 = 'fmb_$i_3' ).
tff(declare_a1339,type,
a1339: $i ).
tff(a1339_definition,axiom,
a1339 = 'fmb_$i_3' ).
tff(declare_a1340,type,
a1340: $i ).
tff(a1340_definition,axiom,
a1340 = 'fmb_$i_3' ).
tff(declare_a1341,type,
a1341: $i ).
tff(a1341_definition,axiom,
a1341 = 'fmb_$i_1' ).
tff(declare_a1342,type,
a1342: $i ).
tff(a1342_definition,axiom,
a1342 = 'fmb_$i_3' ).
tff(declare_a1343,type,
a1343: $i ).
tff(a1343_definition,axiom,
a1343 = 'fmb_$i_3' ).
tff(declare_a1344,type,
a1344: $i ).
tff(a1344_definition,axiom,
a1344 = 'fmb_$i_3' ).
tff(declare_a1345,type,
a1345: $i ).
tff(a1345_definition,axiom,
a1345 = 'fmb_$i_3' ).
tff(declare_a1346,type,
a1346: $i ).
tff(a1346_definition,axiom,
a1346 = 'fmb_$i_3' ).
tff(declare_a1347,type,
a1347: $i ).
tff(a1347_definition,axiom,
a1347 = 'fmb_$i_3' ).
tff(declare_a1348,type,
a1348: $i ).
tff(a1348_definition,axiom,
a1348 = 'fmb_$i_3' ).
tff(declare_a1349,type,
a1349: $i ).
tff(a1349_definition,axiom,
a1349 = 'fmb_$i_3' ).
tff(declare_a1350,type,
a1350: $i ).
tff(a1350_definition,axiom,
a1350 = 'fmb_$i_3' ).
tff(declare_a1351,type,
a1351: $i ).
tff(a1351_definition,axiom,
a1351 = 'fmb_$i_3' ).
tff(declare_a1352,type,
a1352: $i ).
tff(a1352_definition,axiom,
a1352 = 'fmb_$i_3' ).
tff(declare_a1353,type,
a1353: $i ).
tff(a1353_definition,axiom,
a1353 = 'fmb_$i_3' ).
tff(declare_a1354,type,
a1354: $i ).
tff(a1354_definition,axiom,
a1354 = 'fmb_$i_3' ).
tff(declare_a1355,type,
a1355: $i ).
tff(a1355_definition,axiom,
a1355 = 'fmb_$i_3' ).
tff(declare_a1356,type,
a1356: $i ).
tff(a1356_definition,axiom,
a1356 = 'fmb_$i_3' ).
tff(declare_a1357,type,
a1357: $i ).
tff(a1357_definition,axiom,
a1357 = 'fmb_$i_3' ).
tff(declare_a1358,type,
a1358: $i ).
tff(a1358_definition,axiom,
a1358 = 'fmb_$i_1' ).
tff(declare_a1359,type,
a1359: $i ).
tff(a1359_definition,axiom,
a1359 = 'fmb_$i_3' ).
tff(declare_a1360,type,
a1360: $i ).
tff(a1360_definition,axiom,
a1360 = 'fmb_$i_3' ).
tff(declare_a1361,type,
a1361: $i ).
tff(a1361_definition,axiom,
a1361 = 'fmb_$i_1' ).
tff(declare_a1362,type,
a1362: $i ).
tff(a1362_definition,axiom,
a1362 = 'fmb_$i_3' ).
tff(declare_a1363,type,
a1363: $i ).
tff(a1363_definition,axiom,
a1363 = 'fmb_$i_3' ).
tff(declare_a1364,type,
a1364: $i ).
tff(a1364_definition,axiom,
a1364 = 'fmb_$i_1' ).
tff(declare_a1365,type,
a1365: $i ).
tff(a1365_definition,axiom,
a1365 = 'fmb_$i_3' ).
tff(declare_a1366,type,
a1366: $i ).
tff(a1366_definition,axiom,
a1366 = 'fmb_$i_3' ).
tff(declare_a1367,type,
a1367: $i ).
tff(a1367_definition,axiom,
a1367 = 'fmb_$i_3' ).
tff(declare_a1368,type,
a1368: $i ).
tff(a1368_definition,axiom,
a1368 = 'fmb_$i_3' ).
tff(declare_a1369,type,
a1369: $i ).
tff(a1369_definition,axiom,
a1369 = 'fmb_$i_3' ).
tff(declare_a1370,type,
a1370: $i ).
tff(a1370_definition,axiom,
a1370 = 'fmb_$i_3' ).
tff(declare_a1371,type,
a1371: $i ).
tff(a1371_definition,axiom,
a1371 = 'fmb_$i_3' ).
tff(declare_a1372,type,
a1372: $i ).
tff(a1372_definition,axiom,
a1372 = 'fmb_$i_3' ).
tff(declare_a1373,type,
a1373: $i ).
tff(a1373_definition,axiom,
a1373 = 'fmb_$i_3' ).
tff(declare_a1374,type,
a1374: $i ).
tff(a1374_definition,axiom,
a1374 = 'fmb_$i_3' ).
tff(declare_a1375,type,
a1375: $i ).
tff(a1375_definition,axiom,
a1375 = 'fmb_$i_3' ).
tff(declare_a1376,type,
a1376: $i ).
tff(a1376_definition,axiom,
a1376 = 'fmb_$i_3' ).
tff(declare_a1377,type,
a1377: $i ).
tff(a1377_definition,axiom,
a1377 = 'fmb_$i_3' ).
tff(declare_a1378,type,
a1378: $i ).
tff(a1378_definition,axiom,
a1378 = 'fmb_$i_3' ).
tff(declare_a1379,type,
a1379: $i ).
tff(a1379_definition,axiom,
a1379 = 'fmb_$i_3' ).
tff(declare_a1380,type,
a1380: $i ).
tff(a1380_definition,axiom,
a1380 = 'fmb_$i_3' ).
tff(declare_a1381,type,
a1381: $i ).
tff(a1381_definition,axiom,
a1381 = 'fmb_$i_3' ).
tff(declare_a1382,type,
a1382: $i ).
tff(a1382_definition,axiom,
a1382 = 'fmb_$i_3' ).
tff(declare_a1383,type,
a1383: $i ).
tff(a1383_definition,axiom,
a1383 = 'fmb_$i_3' ).
tff(declare_a1384,type,
a1384: $i ).
tff(a1384_definition,axiom,
a1384 = 'fmb_$i_3' ).
tff(declare_a1385,type,
a1385: $i ).
tff(a1385_definition,axiom,
a1385 = 'fmb_$i_3' ).
tff(declare_a1386,type,
a1386: $i ).
tff(a1386_definition,axiom,
a1386 = 'fmb_$i_3' ).
tff(declare_a1387,type,
a1387: $i ).
tff(a1387_definition,axiom,
a1387 = 'fmb_$i_3' ).
tff(declare_a1388,type,
a1388: $i ).
tff(a1388_definition,axiom,
a1388 = 'fmb_$i_3' ).
tff(declare_a1389,type,
a1389: $i ).
tff(a1389_definition,axiom,
a1389 = 'fmb_$i_3' ).
tff(declare_a1390,type,
a1390: $i ).
tff(a1390_definition,axiom,
a1390 = 'fmb_$i_3' ).
tff(declare_a1391,type,
a1391: $i ).
tff(a1391_definition,axiom,
a1391 = 'fmb_$i_3' ).
tff(declare_a1392,type,
a1392: $i ).
tff(a1392_definition,axiom,
a1392 = 'fmb_$i_3' ).
tff(declare_a1393,type,
a1393: $i ).
tff(a1393_definition,axiom,
a1393 = 'fmb_$i_3' ).
tff(declare_a1394,type,
a1394: $i ).
tff(a1394_definition,axiom,
a1394 = 'fmb_$i_3' ).
tff(declare_a1395,type,
a1395: $i ).
tff(a1395_definition,axiom,
a1395 = 'fmb_$i_3' ).
tff(declare_a1396,type,
a1396: $i ).
tff(a1396_definition,axiom,
a1396 = 'fmb_$i_3' ).
tff(declare_a1397,type,
a1397: $i ).
tff(a1397_definition,axiom,
a1397 = 'fmb_$i_3' ).
tff(declare_a1398,type,
a1398: $i ).
tff(a1398_definition,axiom,
a1398 = 'fmb_$i_3' ).
tff(declare_a1399,type,
a1399: $i ).
tff(a1399_definition,axiom,
a1399 = 'fmb_$i_3' ).
tff(declare_a1400,type,
a1400: $i ).
tff(a1400_definition,axiom,
a1400 = 'fmb_$i_3' ).
tff(declare_a1401,type,
a1401: $i ).
tff(a1401_definition,axiom,
a1401 = 'fmb_$i_3' ).
tff(declare_a1402,type,
a1402: $i ).
tff(a1402_definition,axiom,
a1402 = 'fmb_$i_3' ).
tff(declare_a1403,type,
a1403: $i ).
tff(a1403_definition,axiom,
a1403 = 'fmb_$i_3' ).
tff(declare_a1404,type,
a1404: $i ).
tff(a1404_definition,axiom,
a1404 = 'fmb_$i_3' ).
tff(declare_a1405,type,
a1405: $i ).
tff(a1405_definition,axiom,
a1405 = 'fmb_$i_3' ).
tff(declare_a1406,type,
a1406: $i ).
tff(a1406_definition,axiom,
a1406 = 'fmb_$i_3' ).
tff(declare_a1407,type,
a1407: $i ).
tff(a1407_definition,axiom,
a1407 = 'fmb_$i_3' ).
tff(declare_a1408,type,
a1408: $i ).
tff(a1408_definition,axiom,
a1408 = 'fmb_$i_3' ).
tff(declare_a1409,type,
a1409: $i ).
tff(a1409_definition,axiom,
a1409 = 'fmb_$i_3' ).
tff(declare_a1410,type,
a1410: $i ).
tff(a1410_definition,axiom,
a1410 = 'fmb_$i_3' ).
tff(declare_a1411,type,
a1411: $i ).
tff(a1411_definition,axiom,
a1411 = 'fmb_$i_3' ).
tff(declare_a1412,type,
a1412: $i ).
tff(a1412_definition,axiom,
a1412 = 'fmb_$i_3' ).
tff(declare_a1413,type,
a1413: $i ).
tff(a1413_definition,axiom,
a1413 = 'fmb_$i_3' ).
tff(declare_a1414,type,
a1414: $i ).
tff(a1414_definition,axiom,
a1414 = 'fmb_$i_3' ).
tff(declare_a1415,type,
a1415: $i ).
tff(a1415_definition,axiom,
a1415 = 'fmb_$i_3' ).
tff(declare_a1416,type,
a1416: $i ).
tff(a1416_definition,axiom,
a1416 = 'fmb_$i_3' ).
tff(declare_a1417,type,
a1417: $i ).
tff(a1417_definition,axiom,
a1417 = 'fmb_$i_3' ).
tff(declare_a1418,type,
a1418: $i ).
tff(a1418_definition,axiom,
a1418 = 'fmb_$i_3' ).
tff(declare_a1419,type,
a1419: $i ).
tff(a1419_definition,axiom,
a1419 = 'fmb_$i_3' ).
tff(declare_a1420,type,
a1420: $i ).
tff(a1420_definition,axiom,
a1420 = 'fmb_$i_3' ).
tff(declare_a1421,type,
a1421: $i ).
tff(a1421_definition,axiom,
a1421 = 'fmb_$i_3' ).
tff(declare_a1422,type,
a1422: $i ).
tff(a1422_definition,axiom,
a1422 = 'fmb_$i_3' ).
tff(declare_a1423,type,
a1423: $i ).
tff(a1423_definition,axiom,
a1423 = 'fmb_$i_3' ).
tff(declare_a1424,type,
a1424: $i ).
tff(a1424_definition,axiom,
a1424 = 'fmb_$i_1' ).
tff(declare_a1425,type,
a1425: $i ).
tff(a1425_definition,axiom,
a1425 = 'fmb_$i_3' ).
tff(declare_a1426,type,
a1426: $i ).
tff(a1426_definition,axiom,
a1426 = 'fmb_$i_3' ).
tff(declare_a1427,type,
a1427: $i ).
tff(a1427_definition,axiom,
a1427 = 'fmb_$i_3' ).
tff(declare_a1428,type,
a1428: $i ).
tff(a1428_definition,axiom,
a1428 = 'fmb_$i_2' ).
tff(declare_a1429,type,
a1429: $i ).
tff(a1429_definition,axiom,
a1429 = 'fmb_$i_1' ).
tff(declare_a1430,type,
a1430: $i ).
tff(a1430_definition,axiom,
a1430 = 'fmb_$i_2' ).
tff(declare_a1431,type,
a1431: $i ).
tff(a1431_definition,axiom,
a1431 = 'fmb_$i_1' ).
tff(declare_a1432,type,
a1432: $i ).
tff(a1432_definition,axiom,
a1432 = 'fmb_$i_2' ).
tff(declare_a1433,type,
a1433: $i ).
tff(a1433_definition,axiom,
a1433 = 'fmb_$i_3' ).
tff(declare_a1434,type,
a1434: $i ).
tff(a1434_definition,axiom,
a1434 = 'fmb_$i_3' ).
tff(declare_a1435,type,
a1435: $i ).
tff(a1435_definition,axiom,
a1435 = 'fmb_$i_3' ).
tff(declare_a1436,type,
a1436: $i ).
tff(a1436_definition,axiom,
a1436 = 'fmb_$i_3' ).
tff(declare_a1437,type,
a1437: $i ).
tff(a1437_definition,axiom,
a1437 = 'fmb_$i_1' ).
tff(declare_a1438,type,
a1438: $i ).
tff(a1438_definition,axiom,
a1438 = 'fmb_$i_3' ).
tff(declare_a1439,type,
a1439: $i ).
tff(a1439_definition,axiom,
a1439 = 'fmb_$i_3' ).
tff(declare_a1440,type,
a1440: $i ).
tff(a1440_definition,axiom,
a1440 = 'fmb_$i_3' ).
tff(declare_a1441,type,
a1441: $i ).
tff(a1441_definition,axiom,
a1441 = 'fmb_$i_3' ).
tff(declare_a1442,type,
a1442: $i ).
tff(a1442_definition,axiom,
a1442 = 'fmb_$i_1' ).
tff(declare_a1443,type,
a1443: $i ).
tff(a1443_definition,axiom,
a1443 = 'fmb_$i_3' ).
tff(declare_a1444,type,
a1444: $i ).
tff(a1444_definition,axiom,
a1444 = 'fmb_$i_3' ).
tff(declare_a1445,type,
a1445: $i ).
tff(a1445_definition,axiom,
a1445 = 'fmb_$i_3' ).
tff(declare_a1446,type,
a1446: $i ).
tff(a1446_definition,axiom,
a1446 = 'fmb_$i_2' ).
tff(declare_a1447,type,
a1447: $i ).
tff(a1447_definition,axiom,
a1447 = 'fmb_$i_3' ).
tff(declare_a1448,type,
a1448: $i ).
tff(a1448_definition,axiom,
a1448 = 'fmb_$i_3' ).
tff(declare_a1449,type,
a1449: $i ).
tff(a1449_definition,axiom,
a1449 = 'fmb_$i_3' ).
tff(declare_a1450,type,
a1450: $i ).
tff(a1450_definition,axiom,
a1450 = 'fmb_$i_3' ).
tff(declare_a1451,type,
a1451: $i ).
tff(a1451_definition,axiom,
a1451 = 'fmb_$i_3' ).
tff(declare_a1452,type,
a1452: $i ).
tff(a1452_definition,axiom,
a1452 = 'fmb_$i_2' ).
tff(declare_a1453,type,
a1453: $i ).
tff(a1453_definition,axiom,
a1453 = 'fmb_$i_3' ).
tff(declare_a1454,type,
a1454: $i ).
tff(a1454_definition,axiom,
a1454 = 'fmb_$i_2' ).
tff(declare_a1455,type,
a1455: $i ).
tff(a1455_definition,axiom,
a1455 = 'fmb_$i_3' ).
tff(declare_a1456,type,
a1456: $i ).
tff(a1456_definition,axiom,
a1456 = 'fmb_$i_3' ).
tff(declare_a1457,type,
a1457: $i ).
tff(a1457_definition,axiom,
a1457 = 'fmb_$i_3' ).
tff(declare_a1458,type,
a1458: $i ).
tff(a1458_definition,axiom,
a1458 = 'fmb_$i_2' ).
tff(declare_a1459,type,
a1459: $i ).
tff(a1459_definition,axiom,
a1459 = 'fmb_$i_2' ).
tff(declare_a1460,type,
a1460: $i ).
tff(a1460_definition,axiom,
a1460 = 'fmb_$i_3' ).
tff(declare_a1461,type,
a1461: $i ).
tff(a1461_definition,axiom,
a1461 = 'fmb_$i_3' ).
tff(declare_a1462,type,
a1462: $i ).
tff(a1462_definition,axiom,
a1462 = 'fmb_$i_3' ).
tff(declare_a1463,type,
a1463: $i ).
tff(a1463_definition,axiom,
a1463 = 'fmb_$i_3' ).
tff(declare_a1464,type,
a1464: $i ).
tff(a1464_definition,axiom,
a1464 = 'fmb_$i_1' ).
tff(declare_a1465,type,
a1465: $i ).
tff(a1465_definition,axiom,
a1465 = 'fmb_$i_3' ).
tff(declare_a1466,type,
a1466: $i ).
tff(a1466_definition,axiom,
a1466 = 'fmb_$i_3' ).
tff(declare_a1467,type,
a1467: $i ).
tff(a1467_definition,axiom,
a1467 = 'fmb_$i_3' ).
tff(declare_a1468,type,
a1468: $i ).
tff(a1468_definition,axiom,
a1468 = 'fmb_$i_3' ).
tff(declare_a1469,type,
a1469: $i ).
tff(a1469_definition,axiom,
a1469 = 'fmb_$i_3' ).
tff(declare_a1470,type,
a1470: $i ).
tff(a1470_definition,axiom,
a1470 = 'fmb_$i_3' ).
tff(declare_a1471,type,
a1471: $i ).
tff(a1471_definition,axiom,
a1471 = 'fmb_$i_3' ).
tff(declare_a1472,type,
a1472: $i ).
tff(a1472_definition,axiom,
a1472 = 'fmb_$i_3' ).
tff(declare_a1473,type,
a1473: $i ).
tff(a1473_definition,axiom,
a1473 = 'fmb_$i_3' ).
tff(declare_a1474,type,
a1474: $i ).
tff(a1474_definition,axiom,
a1474 = 'fmb_$i_3' ).
tff(declare_a1475,type,
a1475: $i ).
tff(a1475_definition,axiom,
a1475 = 'fmb_$i_1' ).
tff(declare_a1476,type,
a1476: $i ).
tff(a1476_definition,axiom,
a1476 = 'fmb_$i_3' ).
tff(declare_a1477,type,
a1477: $i ).
tff(a1477_definition,axiom,
a1477 = 'fmb_$i_3' ).
tff(declare_a1478,type,
a1478: $i ).
tff(a1478_definition,axiom,
a1478 = 'fmb_$i_3' ).
tff(declare_a1479,type,
a1479: $i ).
tff(a1479_definition,axiom,
a1479 = 'fmb_$i_3' ).
tff(declare_a1480,type,
a1480: $i ).
tff(a1480_definition,axiom,
a1480 = 'fmb_$i_3' ).
tff(declare_a1481,type,
a1481: $i ).
tff(a1481_definition,axiom,
a1481 = 'fmb_$i_3' ).
tff(declare_a1482,type,
a1482: $i ).
tff(a1482_definition,axiom,
a1482 = 'fmb_$i_2' ).
tff(declare_a1483,type,
a1483: $i ).
tff(a1483_definition,axiom,
a1483 = 'fmb_$i_3' ).
tff(declare_a1484,type,
a1484: $i ).
tff(a1484_definition,axiom,
a1484 = 'fmb_$i_3' ).
tff(declare_a1485,type,
a1485: $i ).
tff(a1485_definition,axiom,
a1485 = 'fmb_$i_3' ).
tff(declare_a1486,type,
a1486: $i ).
tff(a1486_definition,axiom,
a1486 = 'fmb_$i_3' ).
tff(declare_a1487,type,
a1487: $i ).
tff(a1487_definition,axiom,
a1487 = 'fmb_$i_3' ).
tff(declare_a1488,type,
a1488: $i ).
tff(a1488_definition,axiom,
a1488 = 'fmb_$i_3' ).
tff(declare_a1489,type,
a1489: $i ).
tff(a1489_definition,axiom,
a1489 = 'fmb_$i_2' ).
tff(declare_a1490,type,
a1490: $i ).
tff(a1490_definition,axiom,
a1490 = 'fmb_$i_3' ).
tff(declare_a1491,type,
a1491: $i ).
tff(a1491_definition,axiom,
a1491 = 'fmb_$i_3' ).
tff(declare_a1492,type,
a1492: $i ).
tff(a1492_definition,axiom,
a1492 = 'fmb_$i_3' ).
tff(declare_a1493,type,
a1493: $i ).
tff(a1493_definition,axiom,
a1493 = 'fmb_$i_3' ).
tff(declare_a1494,type,
a1494: $i ).
tff(a1494_definition,axiom,
a1494 = 'fmb_$i_3' ).
tff(declare_a1495,type,
a1495: $i ).
tff(a1495_definition,axiom,
a1495 = 'fmb_$i_3' ).
tff(declare_a1496,type,
a1496: $i ).
tff(a1496_definition,axiom,
a1496 = 'fmb_$i_3' ).
tff(declare_a1497,type,
a1497: $i ).
tff(a1497_definition,axiom,
a1497 = 'fmb_$i_3' ).
tff(declare_a1498,type,
a1498: $i ).
tff(a1498_definition,axiom,
a1498 = 'fmb_$i_2' ).
tff(declare_a1499,type,
a1499: $i ).
tff(a1499_definition,axiom,
a1499 = 'fmb_$i_3' ).
tff(declare_a1500,type,
a1500: $i ).
tff(a1500_definition,axiom,
a1500 = 'fmb_$i_3' ).
tff(declare_a1501,type,
a1501: $i ).
tff(a1501_definition,axiom,
a1501 = 'fmb_$i_3' ).
tff(declare_a1502,type,
a1502: $i ).
tff(a1502_definition,axiom,
a1502 = 'fmb_$i_3' ).
tff(declare_a1503,type,
a1503: $i ).
tff(a1503_definition,axiom,
a1503 = 'fmb_$i_2' ).
tff(declare_a1504,type,
a1504: $i ).
tff(a1504_definition,axiom,
a1504 = 'fmb_$i_3' ).
tff(declare_a1505,type,
a1505: $i ).
tff(a1505_definition,axiom,
a1505 = 'fmb_$i_1' ).
tff(declare_a1506,type,
a1506: $i ).
tff(a1506_definition,axiom,
a1506 = 'fmb_$i_3' ).
tff(declare_a1507,type,
a1507: $i ).
tff(a1507_definition,axiom,
a1507 = 'fmb_$i_3' ).
tff(declare_a1508,type,
a1508: $i ).
tff(a1508_definition,axiom,
a1508 = 'fmb_$i_3' ).
tff(declare_a1509,type,
a1509: $i ).
tff(a1509_definition,axiom,
a1509 = 'fmb_$i_3' ).
tff(declare_a1510,type,
a1510: $i ).
tff(a1510_definition,axiom,
a1510 = 'fmb_$i_3' ).
tff(declare_a1511,type,
a1511: $i ).
tff(a1511_definition,axiom,
a1511 = 'fmb_$i_2' ).
tff(declare_a1512,type,
a1512: $i ).
tff(a1512_definition,axiom,
a1512 = 'fmb_$i_3' ).
tff(declare_a1513,type,
a1513: $i ).
tff(a1513_definition,axiom,
a1513 = 'fmb_$i_3' ).
tff(declare_a1514,type,
a1514: $i ).
tff(a1514_definition,axiom,
a1514 = 'fmb_$i_3' ).
tff(declare_a1515,type,
a1515: $i ).
tff(a1515_definition,axiom,
a1515 = 'fmb_$i_3' ).
tff(declare_a1516,type,
a1516: $i ).
tff(a1516_definition,axiom,
a1516 = 'fmb_$i_3' ).
tff(declare_a1517,type,
a1517: $i ).
tff(a1517_definition,axiom,
a1517 = 'fmb_$i_3' ).
tff(declare_a1518,type,
a1518: $i ).
tff(a1518_definition,axiom,
a1518 = 'fmb_$i_3' ).
tff(declare_a1519,type,
a1519: $i ).
tff(a1519_definition,axiom,
a1519 = 'fmb_$i_3' ).
tff(declare_a1520,type,
a1520: $i ).
tff(a1520_definition,axiom,
a1520 = 'fmb_$i_3' ).
tff(declare_a1521,type,
a1521: $i ).
tff(a1521_definition,axiom,
a1521 = 'fmb_$i_3' ).
tff(declare_a1522,type,
a1522: $i ).
tff(a1522_definition,axiom,
a1522 = 'fmb_$i_3' ).
tff(declare_a1523,type,
a1523: $i ).
tff(a1523_definition,axiom,
a1523 = 'fmb_$i_3' ).
tff(declare_a1524,type,
a1524: $i ).
tff(a1524_definition,axiom,
a1524 = 'fmb_$i_2' ).
tff(declare_a1525,type,
a1525: $i ).
tff(a1525_definition,axiom,
a1525 = 'fmb_$i_3' ).
tff(declare_a1526,type,
a1526: $i ).
tff(a1526_definition,axiom,
a1526 = 'fmb_$i_3' ).
tff(declare_ndr1_0,type,
ndr1_0: $o ).
tff(ndr1_0_definition,axiom,
ndr1_0 ).
tff(declare_c5_0,type,
c5_0: $o ).
tff(c5_0_definition,axiom,
~ c5_0 ).
tff(declare_c4_0,type,
c4_0: $o ).
tff(c4_0_definition,axiom,
~ c4_0 ).
tff(declare_c2_0,type,
c2_0: $o ).
tff(c2_0_definition,axiom,
~ c2_0 ).
tff(declare_c3_0,type,
c3_0: $o ).
tff(c3_0_definition,axiom,
c3_0 ).
tff(declare_c1_0,type,
c1_0: $o ).
tff(c1_0_definition,axiom,
~ c1_0 ).
tff(declare_ndr1_1,type,
ndr1_1: $i > $o ).
tff(predicate_ndr1_1,axiom,
( ndr1_1('fmb_$i_1')
& ndr1_1('fmb_$i_2')
& ndr1_1('fmb_$i_3') ) ).
tff(declare_c5_2,type,
c5_2: ( $i * $i ) > $o ).
tff(predicate_c5_2,axiom,
( ~ c5_2('fmb_$i_1','fmb_$i_1')
& ~ c5_2('fmb_$i_1','fmb_$i_2')
& ~ c5_2('fmb_$i_1','fmb_$i_3')
& c5_2('fmb_$i_2','fmb_$i_1')
& c5_2('fmb_$i_2','fmb_$i_2')
& c5_2('fmb_$i_2','fmb_$i_3')
& c5_2('fmb_$i_3','fmb_$i_1')
& c5_2('fmb_$i_3','fmb_$i_2')
& c5_2('fmb_$i_3','fmb_$i_3') ) ).
tff(declare_c1_2,type,
c1_2: ( $i * $i ) > $o ).
tff(predicate_c1_2,axiom,
( c1_2('fmb_$i_1','fmb_$i_1')
& ~ c1_2('fmb_$i_1','fmb_$i_2')
& ~ c1_2('fmb_$i_1','fmb_$i_3')
& c1_2('fmb_$i_2','fmb_$i_1')
& ~ c1_2('fmb_$i_2','fmb_$i_2')
& ~ c1_2('fmb_$i_2','fmb_$i_3')
& c1_2('fmb_$i_3','fmb_$i_1')
& ~ c1_2('fmb_$i_3','fmb_$i_2')
& ~ c1_2('fmb_$i_3','fmb_$i_3') ) ).
tff(declare_c2_2,type,
c2_2: ( $i * $i ) > $o ).
tff(predicate_c2_2,axiom,
( c2_2('fmb_$i_1','fmb_$i_1')
& c2_2('fmb_$i_1','fmb_$i_2')
& c2_2('fmb_$i_1','fmb_$i_3')
& c2_2('fmb_$i_2','fmb_$i_1')
& ~ c2_2('fmb_$i_2','fmb_$i_2')
& c2_2('fmb_$i_2','fmb_$i_3')
& ~ c2_2('fmb_$i_3','fmb_$i_1')
& c2_2('fmb_$i_3','fmb_$i_2')
& c2_2('fmb_$i_3','fmb_$i_3') ) ).
tff(declare_c4_2,type,
c4_2: ( $i * $i ) > $o ).
tff(predicate_c4_2,axiom,
( c4_2('fmb_$i_1','fmb_$i_1')
& c4_2('fmb_$i_1','fmb_$i_2')
& c4_2('fmb_$i_1','fmb_$i_3')
& ~ c4_2('fmb_$i_2','fmb_$i_1')
& ~ c4_2('fmb_$i_2','fmb_$i_2')
& ~ c4_2('fmb_$i_2','fmb_$i_3')
& ~ c4_2('fmb_$i_3','fmb_$i_1')
& c4_2('fmb_$i_3','fmb_$i_2')
& c4_2('fmb_$i_3','fmb_$i_3') ) ).
tff(declare_c3_2,type,
c3_2: ( $i * $i ) > $o ).
tff(predicate_c3_2,axiom,
( c3_2('fmb_$i_1','fmb_$i_1')
& c3_2('fmb_$i_1','fmb_$i_2')
& c3_2('fmb_$i_1','fmb_$i_3')
& c3_2('fmb_$i_2','fmb_$i_1')
& c3_2('fmb_$i_2','fmb_$i_2')
& ~ c3_2('fmb_$i_2','fmb_$i_3')
& ~ c3_2('fmb_$i_3','fmb_$i_1')
& c3_2('fmb_$i_3','fmb_$i_2')
& c3_2('fmb_$i_3','fmb_$i_3') ) ).
tff(declare_c2_1,type,
c2_1: $i > $o ).
tff(predicate_c2_1,axiom,
( c2_1('fmb_$i_1')
& c2_1('fmb_$i_2')
& ~ c2_1('fmb_$i_3') ) ).
tff(declare_c4_1,type,
c4_1: $i > $o ).
tff(predicate_c4_1,axiom,
( c4_1('fmb_$i_1')
& ~ c4_1('fmb_$i_2')
& ~ c4_1('fmb_$i_3') ) ).
tff(declare_c3_1,type,
c3_1: $i > $o ).
tff(predicate_c3_1,axiom,
( c3_1('fmb_$i_1')
& ~ c3_1('fmb_$i_2')
& ~ c3_1('fmb_$i_3') ) ).
tff(declare_c1_1,type,
c1_1: $i > $o ).
tff(predicate_c1_1,axiom,
( ~ c1_1('fmb_$i_1')
& c1_1('fmb_$i_2')
& c1_1('fmb_$i_3') ) ).
tff(declare_c5_1,type,
c5_1: $i > $o ).
tff(predicate_c5_1,axiom,
( ~ c5_1('fmb_$i_1')
& ~ c5_1('fmb_$i_2')
& c5_1('fmb_$i_3') ) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SYN520+1 : TPTP v9.3.1. Released v2.1.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.09/0.18 % Computer : n008.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 16:25:54 UTC 2026
% 0.09/0.18 % CPUTime :
% 0.09/0.18 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.09/0.21 Running first-order model finding
% 0.09/0.22 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.21/0.33 % (2377621)Will run a generic schedule for satisfiability detection.
% 0.21/0.33 % (2377628)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=4043969903:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 0.21/0.33 % (2377627)% WARNING: option uhcvi not known.
% 0.21/0.33 % (2377626)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2069451060_2999 on theBenchmark for (2999ds/0Mi)
% 0.21/0.33 % (2377627)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1682980781:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 0.21/0.33 % (2377629)dis+10_1_sil=32000:sp=arity:random_seed=3532284430:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 0.21/0.33 % (2377630)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3610324240:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 0.21/0.33 % (2377632)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3738936436:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 0.21/0.33 % (2377631)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=4290362745:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 0.21/0.33 % Detected minimum model sizes of [1]
% 0.21/0.33 % Detected maximum model sizes of [204]
% 0.21/0.33 % TRYING [1]
% 0.21/0.33 % TRYING [2]
% 0.21/0.33 % TRYING [3]
% 0.21/0.33 % (2377630)Instruction limit reached!
% 0.21/0.33 % (2377630)------------------------------
% 0.21/0.33 % (2377630)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.21/0.33 % (2377630)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.21/0.33 % (2377630)CaDiCaL version: 2.1.3
% 0.21/0.33 % (2377630)Termination reason: Instruction limit
% 0.21/0.33 % (2377630)Termination phase: Blocked clause elimination
% 0.21/0.33 % (2377630)Time elapsed: 0.055 s
% 0.21/0.33 % (2377630)Peak memory usage: 12 MB
% 0.21/0.33 % (2377630)Instructions burned: 118 (million)
% 0.21/0.33 % Finite Model Found!
% 0.21/0.33 % SZS status CounterSatisfiable for theBenchmark
% 0.21/0.33 % (2377629)Instruction limit reached!
% 0.21/0.33 % (2377629)------------------------------
% 0.21/0.33 % (2377629)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.21/0.33 % (2377629)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.21/0.33 % (2377629)CaDiCaL version: 2.1.3
% 0.21/0.33 % (2377629)Termination reason: Instruction limit
% 0.21/0.33 % (2377629)Termination phase: Saturation
% 0.21/0.33 % (2377629)Time elapsed: 0.061 s
% 0.21/0.33 % (2377629)Peak memory usage: 15 MB
% 0.21/0.33 % (2377629)Instructions burned: 104 (million)
% 0.21/0.33 % (2377626) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-2377621-2377626"...
% 0.21/0.33 % (2377626)...printing done.
% 0.21/0.33 % SZS output start FiniteModel for theBenchmark
% See solution above
% 0.21/0.34 % (2377626)------------------------------
% 0.21/0.34 % (2377626)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.21/0.34 % (2377626)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.21/0.34 % (2377626)CaDiCaL version: 2.1.3
% 0.21/0.34 % (2377626)Termination reason: Satisfiable
% 0.21/0.34 % (2377626)Time elapsed: 0.063 s
% 0.21/0.34 % (2377626)Peak memory usage: 15 MB
% 0.21/0.34 % (2377626)Instructions burned: 131 (million)
% 0.21/0.34 % (2377621)Success in time 0.109 s
% 0.21/0.34 % Vampire exiting
%------------------------------------------------------------------------------