%------------------------------------------------------------------------------
% 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/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n020.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 : Satisfiable 0.44s 0.30s
% Output : FiniteModel 0.44s
% 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_a1494,type,
a1494: $i ).
tff(a1494_definition,axiom,
a1494 = 'fmb_$i_1' ).
tff(declare_a1464,type,
a1464: $i ).
tff(a1464_definition,axiom,
a1464 = 'fmb_$i_2' ).
tff(declare_a1458,type,
a1458: $i ).
tff(a1458_definition,axiom,
a1458 = 'fmb_$i_3' ).
tff(declare_a1475,type,
a1475: $i ).
tff(a1475_definition,axiom,
a1475 = 'fmb_$i_3' ).
tff(declare_a1466,type,
a1466: $i ).
tff(a1466_definition,axiom,
a1466 = 'fmb_$i_1' ).
tff(declare_a1465,type,
a1465: $i ).
tff(a1465_definition,axiom,
a1465 = 'fmb_$i_2' ).
tff(declare_a1424,type,
a1424: $i ).
tff(a1424_definition,axiom,
a1424 = 'fmb_$i_2' ).
tff(declare_a1350,type,
a1350: $i ).
tff(a1350_definition,axiom,
a1350 = 'fmb_$i_1' ).
tff(declare_a1325,type,
a1325: $i ).
tff(a1325_definition,axiom,
a1325 = 'fmb_$i_3' ).
tff(declare_a1515,type,
a1515: $i ).
tff(a1515_definition,axiom,
a1515 = 'fmb_$i_3' ).
tff(declare_a1500,type,
a1500: $i ).
tff(a1500_definition,axiom,
a1500 = 'fmb_$i_3' ).
tff(declare_a1495,type,
a1495: $i ).
tff(a1495_definition,axiom,
a1495 = 'fmb_$i_3' ).
tff(declare_a1484,type,
a1484: $i ).
tff(a1484_definition,axiom,
a1484 = 'fmb_$i_3' ).
tff(declare_a1483,type,
a1483: $i ).
tff(a1483_definition,axiom,
a1483 = 'fmb_$i_3' ).
tff(declare_a1460,type,
a1460: $i ).
tff(a1460_definition,axiom,
a1460 = 'fmb_$i_3' ).
tff(declare_a1454,type,
a1454: $i ).
tff(a1454_definition,axiom,
a1454 = 'fmb_$i_3' ).
tff(declare_a1447,type,
a1447: $i ).
tff(a1447_definition,axiom,
a1447 = 'fmb_$i_3' ).
tff(declare_a1438,type,
a1438: $i ).
tff(a1438_definition,axiom,
a1438 = 'fmb_$i_1' ).
tff(declare_a1434,type,
a1434: $i ).
tff(a1434_definition,axiom,
a1434 = 'fmb_$i_3' ).
tff(declare_a1430,type,
a1430: $i ).
tff(a1430_definition,axiom,
a1430 = 'fmb_$i_3' ).
tff(declare_a1428,type,
a1428: $i ).
tff(a1428_definition,axiom,
a1428 = 'fmb_$i_2' ).
tff(declare_a1402,type,
a1402: $i ).
tff(a1402_definition,axiom,
a1402 = 'fmb_$i_1' ).
tff(declare_a1370,type,
a1370: $i ).
tff(a1370_definition,axiom,
a1370 = 'fmb_$i_1' ).
tff(declare_a1365,type,
a1365: $i ).
tff(a1365_definition,axiom,
a1365 = 'fmb_$i_3' ).
tff(declare_a1359,type,
a1359: $i ).
tff(a1359_definition,axiom,
a1359 = 'fmb_$i_3' ).
tff(declare_a1352,type,
a1352: $i ).
tff(a1352_definition,axiom,
a1352 = 'fmb_$i_3' ).
tff(declare_a1342,type,
a1342: $i ).
tff(a1342_definition,axiom,
a1342 = 'fmb_$i_1' ).
tff(declare_a1335,type,
a1335: $i ).
tff(a1335_definition,axiom,
a1335 = 'fmb_$i_3' ).
tff(declare_a1327,type,
a1327: $i ).
tff(a1327_definition,axiom,
a1327 = 'fmb_$i_1' ).
tff(declare_a1524,type,
a1524: $i ).
tff(a1524_definition,axiom,
a1524 = 'fmb_$i_3' ).
tff(declare_a1516,type,
a1516: $i ).
tff(a1516_definition,axiom,
a1516 = 'fmb_$i_1' ).
tff(declare_a1509,type,
a1509: $i ).
tff(a1509_definition,axiom,
a1509 = 'fmb_$i_3' ).
tff(declare_a1506,type,
a1506: $i ).
tff(a1506_definition,axiom,
a1506 = 'fmb_$i_3' ).
tff(declare_a1487,type,
a1487: $i ).
tff(a1487_definition,axiom,
a1487 = 'fmb_$i_1' ).
tff(declare_a1455,type,
a1455: $i ).
tff(a1455_definition,axiom,
a1455 = 'fmb_$i_3' ).
tff(declare_a1446,type,
a1446: $i ).
tff(a1446_definition,axiom,
a1446 = 'fmb_$i_3' ).
tff(declare_a1442,type,
a1442: $i ).
tff(a1442_definition,axiom,
a1442 = 'fmb_$i_2' ).
tff(declare_a1436,type,
a1436: $i ).
tff(a1436_definition,axiom,
a1436 = 'fmb_$i_1' ).
tff(declare_a1409,type,
a1409: $i ).
tff(a1409_definition,axiom,
a1409 = 'fmb_$i_1' ).
tff(declare_a1361,type,
a1361: $i ).
tff(a1361_definition,axiom,
a1361 = 'fmb_$i_2' ).
tff(declare_a1339,type,
a1339: $i ).
tff(a1339_definition,axiom,
a1339 = 'fmb_$i_3' ).
tff(declare_a1517,type,
a1517: $i ).
tff(a1517_definition,axiom,
a1517 = 'fmb_$i_3' ).
tff(declare_a1513,type,
a1513: $i ).
tff(a1513_definition,axiom,
a1513 = 'fmb_$i_3' ).
tff(declare_a1502,type,
a1502: $i ).
tff(a1502_definition,axiom,
a1502 = 'fmb_$i_3' ).
tff(declare_a1501,type,
a1501: $i ).
tff(a1501_definition,axiom,
a1501 = 'fmb_$i_3' ).
tff(declare_a1499,type,
a1499: $i ).
tff(a1499_definition,axiom,
a1499 = 'fmb_$i_3' ).
tff(declare_a1496,type,
a1496: $i ).
tff(a1496_definition,axiom,
a1496 = 'fmb_$i_3' ).
tff(declare_a1486,type,
a1486: $i ).
tff(a1486_definition,axiom,
a1486 = 'fmb_$i_3' ).
tff(declare_a1485,type,
a1485: $i ).
tff(a1485_definition,axiom,
a1485 = 'fmb_$i_1' ).
tff(declare_a1480,type,
a1480: $i ).
tff(a1480_definition,axiom,
a1480 = 'fmb_$i_3' ).
tff(declare_a1462,type,
a1462: $i ).
tff(a1462_definition,axiom,
a1462 = 'fmb_$i_3' ).
tff(declare_a1461,type,
a1461: $i ).
tff(a1461_definition,axiom,
a1461 = 'fmb_$i_3' ).
tff(declare_a1448,type,
a1448: $i ).
tff(a1448_definition,axiom,
a1448 = 'fmb_$i_3' ).
tff(declare_a1431,type,
a1431: $i ).
tff(a1431_definition,axiom,
a1431 = 'fmb_$i_3' ).
tff(declare_a1429,type,
a1429: $i ).
tff(a1429_definition,axiom,
a1429 = 'fmb_$i_1' ).
tff(declare_a1404,type,
a1404: $i ).
tff(a1404_definition,axiom,
a1404 = 'fmb_$i_1' ).
tff(declare_a1388,type,
a1388: $i ).
tff(a1388_definition,axiom,
a1388 = 'fmb_$i_3' ).
tff(declare_a1381,type,
a1381: $i ).
tff(a1381_definition,axiom,
a1381 = 'fmb_$i_1' ).
tff(declare_a1376,type,
a1376: $i ).
tff(a1376_definition,axiom,
a1376 = 'fmb_$i_3' ).
tff(declare_a1375,type,
a1375: $i ).
tff(a1375_definition,axiom,
a1375 = 'fmb_$i_3' ).
tff(declare_a1373,type,
a1373: $i ).
tff(a1373_definition,axiom,
a1373 = 'fmb_$i_3' ).
tff(declare_a1371,type,
a1371: $i ).
tff(a1371_definition,axiom,
a1371 = 'fmb_$i_1' ).
tff(declare_a1357,type,
a1357: $i ).
tff(a1357_definition,axiom,
a1357 = 'fmb_$i_3' ).
tff(declare_a1353,type,
a1353: $i ).
tff(a1353_definition,axiom,
a1353 = 'fmb_$i_3' ).
tff(declare_a1344,type,
a1344: $i ).
tff(a1344_definition,axiom,
a1344 = 'fmb_$i_1' ).
tff(declare_a1343,type,
a1343: $i ).
tff(a1343_definition,axiom,
a1343 = 'fmb_$i_1' ).
tff(declare_a1336,type,
a1336: $i ).
tff(a1336_definition,axiom,
a1336 = 'fmb_$i_3' ).
tff(declare_a1330,type,
a1330: $i ).
tff(a1330_definition,axiom,
a1330 = 'fmb_$i_1' ).
tff(declare_a1329,type,
a1329: $i ).
tff(a1329_definition,axiom,
a1329 = 'fmb_$i_1' ).
tff(declare_a1328,type,
a1328: $i ).
tff(a1328_definition,axiom,
a1328 = 'fmb_$i_1' ).
tff(declare_a1525,type,
a1525: $i ).
tff(a1525_definition,axiom,
a1525 = 'fmb_$i_3' ).
tff(declare_a1520,type,
a1520: $i ).
tff(a1520_definition,axiom,
a1520 = 'fmb_$i_3' ).
tff(declare_a1507,type,
a1507: $i ).
tff(a1507_definition,axiom,
a1507 = 'fmb_$i_3' ).
tff(declare_a1503,type,
a1503: $i ).
tff(a1503_definition,axiom,
a1503 = 'fmb_$i_3' ).
tff(declare_a1498,type,
a1498: $i ).
tff(a1498_definition,axiom,
a1498 = 'fmb_$i_3' ).
tff(declare_a1493,type,
a1493: $i ).
tff(a1493_definition,axiom,
a1493 = 'fmb_$i_1' ).
tff(declare_a1488,type,
a1488: $i ).
tff(a1488_definition,axiom,
a1488 = 'fmb_$i_2' ).
tff(declare_a1482,type,
a1482: $i ).
tff(a1482_definition,axiom,
a1482 = 'fmb_$i_3' ).
tff(declare_a1478,type,
a1478: $i ).
tff(a1478_definition,axiom,
a1478 = 'fmb_$i_3' ).
tff(declare_a1457,type,
a1457: $i ).
tff(a1457_definition,axiom,
a1457 = 'fmb_$i_3' ).
tff(declare_a1456,type,
a1456: $i ).
tff(a1456_definition,axiom,
a1456 = 'fmb_$i_3' ).
tff(declare_a1452,type,
a1452: $i ).
tff(a1452_definition,axiom,
a1452 = 'fmb_$i_2' ).
tff(declare_a1450,type,
a1450: $i ).
tff(a1450_definition,axiom,
a1450 = 'fmb_$i_3' ).
tff(declare_a1439,type,
a1439: $i ).
tff(a1439_definition,axiom,
a1439 = 'fmb_$i_1' ).
tff(declare_a1437,type,
a1437: $i ).
tff(a1437_definition,axiom,
a1437 = 'fmb_$i_3' ).
tff(declare_a1425,type,
a1425: $i ).
tff(a1425_definition,axiom,
a1425 = 'fmb_$i_3' ).
tff(declare_a1423,type,
a1423: $i ).
tff(a1423_definition,axiom,
a1423 = 'fmb_$i_3' ).
tff(declare_a1416,type,
a1416: $i ).
tff(a1416_definition,axiom,
a1416 = 'fmb_$i_3' ).
tff(declare_a1406,type,
a1406: $i ).
tff(a1406_definition,axiom,
a1406 = 'fmb_$i_3' ).
tff(declare_a1400,type,
a1400: $i ).
tff(a1400_definition,axiom,
a1400 = 'fmb_$i_3' ).
tff(declare_a1390,type,
a1390: $i ).
tff(a1390_definition,axiom,
a1390 = 'fmb_$i_3' ).
tff(declare_a1378,type,
a1378: $i ).
tff(a1378_definition,axiom,
a1378 = 'fmb_$i_3' ).
tff(declare_a1363,type,
a1363: $i ).
tff(a1363_definition,axiom,
a1363 = 'fmb_$i_1' ).
tff(declare_a1338,type,
a1338: $i ).
tff(a1338_definition,axiom,
a1338 = 'fmb_$i_3' ).
tff(declare_a1333,type,
a1333: $i ).
tff(a1333_definition,axiom,
a1333 = 'fmb_$i_1' ).
tff(declare_a1332,type,
a1332: $i ).
tff(a1332_definition,axiom,
a1332 = 'fmb_$i_3' ).
tff(declare_a1512,type,
a1512: $i ).
tff(a1512_definition,axiom,
a1512 = 'fmb_$i_3' ).
tff(declare_a1449,type,
a1449: $i ).
tff(a1449_definition,axiom,
a1449 = 'fmb_$i_3' ).
tff(declare_a1432,type,
a1432: $i ).
tff(a1432_definition,axiom,
a1432 = 'fmb_$i_3' ).
tff(declare_a1403,type,
a1403: $i ).
tff(a1403_definition,axiom,
a1403 = 'fmb_$i_1' ).
tff(declare_a1360,type,
a1360: $i ).
tff(a1360_definition,axiom,
a1360 = 'fmb_$i_3' ).
tff(declare_a1340,type,
a1340: $i ).
tff(a1340_definition,axiom,
a1340 = 'fmb_$i_3' ).
tff(declare_a1522,type,
a1522: $i ).
tff(a1522_definition,axiom,
a1522 = 'fmb_$i_3' ).
tff(declare_a1479,type,
a1479: $i ).
tff(a1479_definition,axiom,
a1479 = 'fmb_$i_3' ).
tff(declare_a1467,type,
a1467: $i ).
tff(a1467_definition,axiom,
a1467 = 'fmb_$i_3' ).
tff(declare_a1453,type,
a1453: $i ).
tff(a1453_definition,axiom,
a1453 = 'fmb_$i_3' ).
tff(declare_a1441,type,
a1441: $i ).
tff(a1441_definition,axiom,
a1441 = 'fmb_$i_2' ).
tff(declare_a1427,type,
a1427: $i ).
tff(a1427_definition,axiom,
a1427 = 'fmb_$i_3' ).
tff(declare_a1408,type,
a1408: $i ).
tff(a1408_definition,axiom,
a1408 = 'fmb_$i_3' ).
tff(declare_a1407,type,
a1407: $i ).
tff(a1407_definition,axiom,
a1407 = 'fmb_$i_3' ).
tff(declare_a1401,type,
a1401: $i ).
tff(a1401_definition,axiom,
a1401 = 'fmb_$i_3' ).
tff(declare_a1391,type,
a1391: $i ).
tff(a1391_definition,axiom,
a1391 = 'fmb_$i_3' ).
tff(declare_a1389,type,
a1389: $i ).
tff(a1389_definition,axiom,
a1389 = 'fmb_$i_3' ).
tff(declare_a1366,type,
a1366: $i ).
tff(a1366_definition,axiom,
a1366 = 'fmb_$i_3' ).
tff(declare_a1364,type,
a1364: $i ).
tff(a1364_definition,axiom,
a1364 = 'fmb_$i_3' ).
tff(declare_a1337,type,
a1337: $i ).
tff(a1337_definition,axiom,
a1337 = 'fmb_$i_2' ).
tff(declare_a1334,type,
a1334: $i ).
tff(a1334_definition,axiom,
a1334 = 'fmb_$i_1' ).
tff(declare_a1521,type,
a1521: $i ).
tff(a1521_definition,axiom,
a1521 = 'fmb_$i_3' ).
tff(declare_a1469,type,
a1469: $i ).
tff(a1469_definition,axiom,
a1469 = 'fmb_$i_3' ).
tff(declare_a1468,type,
a1468: $i ).
tff(a1468_definition,axiom,
a1468 = 'fmb_$i_3' ).
tff(declare_a1451,type,
a1451: $i ).
tff(a1451_definition,axiom,
a1451 = 'fmb_$i_3' ).
tff(declare_a1445,type,
a1445: $i ).
tff(a1445_definition,axiom,
a1445 = 'fmb_$i_3' ).
tff(declare_a1440,type,
a1440: $i ).
tff(a1440_definition,axiom,
a1440 = 'fmb_$i_3' ).
tff(declare_a1426,type,
a1426: $i ).
tff(a1426_definition,axiom,
a1426 = 'fmb_$i_3' ).
tff(declare_a1481,type,
a1481: $i ).
tff(a1481_definition,axiom,
a1481 = 'fmb_$i_3' ).
tff(declare_a1433,type,
a1433: $i ).
tff(a1433_definition,axiom,
a1433 = 'fmb_$i_3' ).
tff(declare_a1384,type,
a1384: $i ).
tff(a1384_definition,axiom,
a1384 = 'fmb_$i_3' ).
tff(declare_a1377,type,
a1377: $i ).
tff(a1377_definition,axiom,
a1377 = 'fmb_$i_3' ).
tff(declare_a1414,type,
a1414: $i ).
tff(a1414_definition,axiom,
a1414 = 'fmb_$i_1' ).
tff(declare_a1410,type,
a1410: $i ).
tff(a1410_definition,axiom,
a1410 = 'fmb_$i_3' ).
tff(declare_a1374,type,
a1374: $i ).
tff(a1374_definition,axiom,
a1374 = 'fmb_$i_3' ).
tff(declare_a1508,type,
a1508: $i ).
tff(a1508_definition,axiom,
a1508 = 'fmb_$i_3' ).
tff(declare_a1398,type,
a1398: $i ).
tff(a1398_definition,axiom,
a1398 = 'fmb_$i_3' ).
tff(declare_a1477,type,
a1477: $i ).
tff(a1477_definition,axiom,
a1477 = 'fmb_$i_3' ).
tff(declare_a1417,type,
a1417: $i ).
tff(a1417_definition,axiom,
a1417 = 'fmb_$i_1' ).
tff(declare_a1324,type,
a1324: $i ).
tff(a1324_definition,axiom,
a1324 = 'fmb_$i_2' ).
tff(declare_a1514,type,
a1514: $i ).
tff(a1514_definition,axiom,
a1514 = 'fmb_$i_3' ).
tff(declare_a1510,type,
a1510: $i ).
tff(a1510_definition,axiom,
a1510 = 'fmb_$i_3' ).
tff(declare_a1463,type,
a1463: $i ).
tff(a1463_definition,axiom,
a1463 = 'fmb_$i_3' ).
tff(declare_a1341,type,
a1341: $i ).
tff(a1341_definition,axiom,
a1341 = 'fmb_$i_3' ).
tff(declare_a1326,type,
a1326: $i ).
tff(a1326_definition,axiom,
a1326 = 'fmb_$i_3' ).
tff(declare_a1399,type,
a1399: $i ).
tff(a1399_definition,axiom,
a1399 = 'fmb_$i_3' ).
tff(declare_a1490,type,
a1490: $i ).
tff(a1490_definition,axiom,
a1490 = 'fmb_$i_3' ).
tff(declare_a1511,type,
a1511: $i ).
tff(a1511_definition,axiom,
a1511 = 'fmb_$i_3' ).
tff(declare_a1354,type,
a1354: $i ).
tff(a1354_definition,axiom,
a1354 = 'fmb_$i_3' ).
tff(declare_a1411,type,
a1411: $i ).
tff(a1411_definition,axiom,
a1411 = 'fmb_$i_1' ).
tff(declare_a1489,type,
a1489: $i ).
tff(a1489_definition,axiom,
a1489 = 'fmb_$i_1' ).
tff(declare_a1519,type,
a1519: $i ).
tff(a1519_definition,axiom,
a1519 = 'fmb_$i_3' ).
tff(declare_a1526,type,
a1526: $i ).
tff(a1526_definition,axiom,
a1526 = 'fmb_$i_3' ).
tff(declare_a1492,type,
a1492: $i ).
tff(a1492_definition,axiom,
a1492 = 'fmb_$i_3' ).
tff(declare_a1518,type,
a1518: $i ).
tff(a1518_definition,axiom,
a1518 = 'fmb_$i_3' ).
tff(declare_a1476,type,
a1476: $i ).
tff(a1476_definition,axiom,
a1476 = 'fmb_$i_3' ).
tff(declare_a1474,type,
a1474: $i ).
tff(a1474_definition,axiom,
a1474 = 'fmb_$i_3' ).
tff(declare_a1435,type,
a1435: $i ).
tff(a1435_definition,axiom,
a1435 = 'fmb_$i_3' ).
tff(declare_a1346,type,
a1346: $i ).
tff(a1346_definition,axiom,
a1346 = 'fmb_$i_3' ).
tff(declare_a1505,type,
a1505: $i ).
tff(a1505_definition,axiom,
a1505 = 'fmb_$i_1' ).
tff(declare_a1473,type,
a1473: $i ).
tff(a1473_definition,axiom,
a1473 = 'fmb_$i_3' ).
tff(declare_a1459,type,
a1459: $i ).
tff(a1459_definition,axiom,
a1459 = 'fmb_$i_3' ).
tff(declare_a1385,type,
a1385: $i ).
tff(a1385_definition,axiom,
a1385 = 'fmb_$i_3' ).
tff(declare_a1523,type,
a1523: $i ).
tff(a1523_definition,axiom,
a1523 = 'fmb_$i_3' ).
tff(declare_a1413,type,
a1413: $i ).
tff(a1413_definition,axiom,
a1413 = 'fmb_$i_3' ).
tff(declare_a1397,type,
a1397: $i ).
tff(a1397_definition,axiom,
a1397 = 'fmb_$i_3' ).
tff(declare_a1386,type,
a1386: $i ).
tff(a1386_definition,axiom,
a1386 = 'fmb_$i_3' ).
tff(declare_a1362,type,
a1362: $i ).
tff(a1362_definition,axiom,
a1362 = 'fmb_$i_3' ).
tff(declare_a1355,type,
a1355: $i ).
tff(a1355_definition,axiom,
a1355 = 'fmb_$i_3' ).
tff(declare_a1504,type,
a1504: $i ).
tff(a1504_definition,axiom,
a1504 = 'fmb_$i_3' ).
tff(declare_a1470,type,
a1470: $i ).
tff(a1470_definition,axiom,
a1470 = 'fmb_$i_3' ).
tff(declare_a1358,type,
a1358: $i ).
tff(a1358_definition,axiom,
a1358 = 'fmb_$i_2' ).
tff(declare_a1491,type,
a1491: $i ).
tff(a1491_definition,axiom,
a1491 = 'fmb_$i_3' ).
tff(declare_a1472,type,
a1472: $i ).
tff(a1472_definition,axiom,
a1472 = 'fmb_$i_3' ).
tff(declare_a1471,type,
a1471: $i ).
tff(a1471_definition,axiom,
a1471 = 'fmb_$i_3' ).
tff(declare_a1392,type,
a1392: $i ).
tff(a1392_definition,axiom,
a1392 = 'fmb_$i_3' ).
tff(declare_a1379,type,
a1379: $i ).
tff(a1379_definition,axiom,
a1379 = 'fmb_$i_2' ).
tff(declare_a1497,type,
a1497: $i ).
tff(a1497_definition,axiom,
a1497 = 'fmb_$i_3' ).
tff(declare_a1394,type,
a1394: $i ).
tff(a1394_definition,axiom,
a1394 = 'fmb_$i_3' ).
tff(declare_a1393,type,
a1393: $i ).
tff(a1393_definition,axiom,
a1393 = 'fmb_$i_3' ).
tff(declare_a1347,type,
a1347: $i ).
tff(a1347_definition,axiom,
a1347 = 'fmb_$i_3' ).
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_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_ndr1_0,type,
ndr1_0: $o ).
tff(ndr1_0_definition,axiom,
ndr1_0 ).
tff(declare_c3_0,type,
c3_0: $o ).
tff(c3_0_definition,axiom,
c3_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_ssSkC0,type,
ssSkC0: $o ).
tff(ssSkC0_definition,axiom,
~ ssSkC0 ).
tff(declare_c1_0,type,
c1_0: $o ).
tff(c1_0_definition,axiom,
~ c1_0 ).
tff(declare_ssSkC33,type,
ssSkC33: $o ).
tff(ssSkC33_definition,axiom,
ssSkC33 ).
tff(declare_ssSkC32,type,
ssSkC32: $o ).
tff(ssSkC32_definition,axiom,
ssSkC32 ).
tff(declare_ssSkC30,type,
ssSkC30: $o ).
tff(ssSkC30_definition,axiom,
ssSkC30 ).
tff(declare_ssSkC27,type,
ssSkC27: $o ).
tff(ssSkC27_definition,axiom,
ssSkC27 ).
tff(declare_ssSkC26,type,
ssSkC26: $o ).
tff(ssSkC26_definition,axiom,
~ ssSkC26 ).
tff(declare_ssSkC22,type,
ssSkC22: $o ).
tff(ssSkC22_definition,axiom,
ssSkC22 ).
tff(declare_ssSkC21,type,
ssSkC21: $o ).
tff(ssSkC21_definition,axiom,
~ ssSkC21 ).
tff(declare_ssSkC20,type,
ssSkC20: $o ).
tff(ssSkC20_definition,axiom,
ssSkC20 ).
tff(declare_ssSkC19,type,
ssSkC19: $o ).
tff(ssSkC19_definition,axiom,
~ ssSkC19 ).
tff(declare_ssSkC18,type,
ssSkC18: $o ).
tff(ssSkC18_definition,axiom,
ssSkC18 ).
tff(declare_ssSkC17,type,
ssSkC17: $o ).
tff(ssSkC17_definition,axiom,
ssSkC17 ).
tff(declare_ssSkC16,type,
ssSkC16: $o ).
tff(ssSkC16_definition,axiom,
~ ssSkC16 ).
tff(declare_ssSkC12,type,
ssSkC12: $o ).
tff(ssSkC12_definition,axiom,
ssSkC12 ).
tff(declare_ssSkC7,type,
ssSkC7: $o ).
tff(ssSkC7_definition,axiom,
ssSkC7 ).
tff(declare_ssSkC6,type,
ssSkC6: $o ).
tff(ssSkC6_definition,axiom,
ssSkC6 ).
tff(declare_ssSkC5,type,
ssSkC5: $o ).
tff(ssSkC5_definition,axiom,
ssSkC5 ).
tff(declare_ssSkC4,type,
ssSkC4: $o ).
tff(ssSkC4_definition,axiom,
ssSkC4 ).
tff(declare_ssSkC3,type,
ssSkC3: $o ).
tff(ssSkC3_definition,axiom,
ssSkC3 ).
tff(declare_ssSkC2,type,
ssSkC2: $o ).
tff(ssSkC2_definition,axiom,
~ ssSkC2 ).
tff(declare_ssSkC1,type,
ssSkC1: $o ).
tff(ssSkC1_definition,axiom,
ssSkC1 ).
tff(declare_ssSkC35,type,
ssSkC35: $o ).
tff(ssSkC35_definition,axiom,
ssSkC35 ).
tff(declare_ssSkC31,type,
ssSkC31: $o ).
tff(ssSkC31_definition,axiom,
ssSkC31 ).
tff(declare_ssSkC9,type,
ssSkC9: $o ).
tff(ssSkC9_definition,axiom,
ssSkC9 ).
tff(declare_ssSkC34,type,
ssSkC34: $o ).
tff(ssSkC34_definition,axiom,
ssSkC34 ).
tff(declare_ssSkC29,type,
ssSkC29: $o ).
tff(ssSkC29_definition,axiom,
ssSkC29 ).
tff(declare_ssSkC25,type,
ssSkC25: $o ).
tff(ssSkC25_definition,axiom,
ssSkC25 ).
tff(declare_ssSkC24,type,
ssSkC24: $o ).
tff(ssSkC24_definition,axiom,
ssSkC24 ).
tff(declare_ssSkC11,type,
ssSkC11: $o ).
tff(ssSkC11_definition,axiom,
ssSkC11 ).
tff(declare_ssSkC8,type,
ssSkC8: $o ).
tff(ssSkC8_definition,axiom,
ssSkC8 ).
tff(declare_ssSkC10,type,
ssSkC10: $o ).
tff(ssSkC10_definition,axiom,
ssSkC10 ).
tff(declare_ssSkC14,type,
ssSkC14: $o ).
tff(ssSkC14_definition,axiom,
ssSkC14 ).
tff(declare_ssSkC15,type,
ssSkC15: $o ).
tff(ssSkC15_definition,axiom,
ssSkC15 ).
tff(declare_ssSkC28,type,
ssSkC28: $o ).
tff(ssSkC28_definition,axiom,
ssSkC28 ).
tff(declare_ssSkC13,type,
ssSkC13: $o ).
tff(ssSkC13_definition,axiom,
ssSkC13 ).
tff(declare_ssSkC23,type,
ssSkC23: $o ).
tff(ssSkC23_definition,axiom,
~ ssSkC23 ).
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') ) ).
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_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_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_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_ssSkP13,type,
ssSkP13: $i > $o ).
tff(predicate_ssSkP13,axiom,
( ~ ssSkP13('fmb_$i_1')
& ssSkP13('fmb_$i_2')
& ssSkP13('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_ssSkP12,type,
ssSkP12: $i > $o ).
tff(predicate_ssSkP12,axiom,
( ssSkP12('fmb_$i_1')
& ssSkP12('fmb_$i_2')
& ssSkP12('fmb_$i_3') ) ).
tff(declare_ssSkP11,type,
ssSkP11: $i > $o ).
tff(predicate_ssSkP11,axiom,
( ssSkP11('fmb_$i_1')
& ssSkP11('fmb_$i_2')
& ssSkP11('fmb_$i_3') ) ).
tff(declare_ssSkP10,type,
ssSkP10: $i > $o ).
tff(predicate_ssSkP10,axiom,
( ssSkP10('fmb_$i_1')
& ssSkP10('fmb_$i_2')
& ssSkP10('fmb_$i_3') ) ).
tff(declare_ssSkP9,type,
ssSkP9: $i > $o ).
tff(predicate_ssSkP9,axiom,
( ssSkP9('fmb_$i_1')
& ssSkP9('fmb_$i_2')
& ssSkP9('fmb_$i_3') ) ).
tff(declare_ssSkP8,type,
ssSkP8: $i > $o ).
tff(predicate_ssSkP8,axiom,
( ssSkP8('fmb_$i_1')
& ssSkP8('fmb_$i_2')
& ssSkP8('fmb_$i_3') ) ).
tff(declare_ssSkP7,type,
ssSkP7: $i > $o ).
tff(predicate_ssSkP7,axiom,
( ssSkP7('fmb_$i_1')
& ssSkP7('fmb_$i_2')
& ssSkP7('fmb_$i_3') ) ).
tff(declare_ssSkP6,type,
ssSkP6: $i > $o ).
tff(predicate_ssSkP6,axiom,
( ssSkP6('fmb_$i_1')
& ssSkP6('fmb_$i_2')
& ssSkP6('fmb_$i_3') ) ).
tff(declare_ssSkP5,type,
ssSkP5: $i > $o ).
tff(predicate_ssSkP5,axiom,
( ssSkP5('fmb_$i_1')
& ssSkP5('fmb_$i_2')
& ssSkP5('fmb_$i_3') ) ).
tff(declare_ssSkP4,type,
ssSkP4: $i > $o ).
tff(predicate_ssSkP4,axiom,
( ssSkP4('fmb_$i_1')
& ssSkP4('fmb_$i_2')
& ssSkP4('fmb_$i_3') ) ).
tff(declare_ssSkP3,type,
ssSkP3: $i > $o ).
tff(predicate_ssSkP3,axiom,
( ssSkP3('fmb_$i_1')
& ssSkP3('fmb_$i_2')
& ssSkP3('fmb_$i_3') ) ).
tff(declare_ssSkP2,type,
ssSkP2: $i > $o ).
tff(predicate_ssSkP2,axiom,
( ~ ssSkP2('fmb_$i_1')
& ssSkP2('fmb_$i_2')
& ssSkP2('fmb_$i_3') ) ).
tff(declare_ssSkP1,type,
ssSkP1: $i > $o ).
tff(predicate_ssSkP1,axiom,
( ssSkP1('fmb_$i_1')
& ssSkP1('fmb_$i_2')
& ssSkP1('fmb_$i_3') ) ).
tff(declare_ssSkP0,type,
ssSkP0: $i > $o ).
tff(predicate_ssSkP0,axiom,
( ssSkP0('fmb_$i_1')
& ssSkP0('fmb_$i_2')
& ssSkP0('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_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') ) ).
%------------------------------------------------------------------------------
%----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/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.10/0.17 % Computer : n020.cluster.edu
% 0.10/0.17 % Model : x86_64 x86_64
% 0.10/0.17 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.17 % Memory : 8046.5625MB
% 0.10/0.17 % OS : Linux 6.8.0-71-generic
% 0.10/0.17 % CPULimit : 300
% 0.10/0.17 % WCLimit : 300
% 0.10/0.17 % DateTime : Mon Sep 28 16:26:05 UTC 2026
% 0.10/0.18 % CPUTime :
% 0.10/0.18 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.10/0.20 Running first-order model finding
% 0.10/0.20 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.44/0.30 % (283218)Will run a generic schedule for satisfiability detection.
% 0.44/0.30 % (283225)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2737356191:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 0.44/0.30 % (283224)% WARNING: option uhcvi not known.
% 0.44/0.30 % (283223)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2039854452_2999 on theBenchmark for (2999ds/0Mi)
% 0.44/0.30 % (283226)dis+10_1_sil=32000:sp=arity:random_seed=2779158816:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 0.44/0.30 % (283227)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2321545584:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 0.44/0.30 % (283228)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2296441908:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 0.44/0.30 % (283229)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3879325365:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 0.44/0.30 % (283224)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2186579627:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 0.44/0.30 % Detected minimum model sizes of [1]
% 0.44/0.30 % Detected maximum model sizes of [166]
% 0.44/0.30 % TRYING [1]
% 0.44/0.30 % TRYING [2]
% 0.44/0.30 % TRYING [3]
% 0.44/0.30 % Finite Model Found!
% 0.44/0.30 % SZS status Satisfiable for theBenchmark
% 0.44/0.30 % (283223) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-283218-283223"...
% 0.44/0.30 % (283223)...printing done.
% 0.44/0.30 % SZS output start FiniteModel for theBenchmark
% See solution above
% 0.44/0.30 % (283223)------------------------------
% 0.44/0.30 % (283223)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.44/0.30 % (283223)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.44/0.30 % (283223)CaDiCaL version: 2.1.3
% 0.44/0.30 % (283223)Termination reason: Satisfiable
% 0.44/0.30 % (283223)Time elapsed: 0.044 s
% 0.44/0.30 % (283223)Peak memory usage: 14 MB
% 0.44/0.30 % (283223)Instructions burned: 92 (million)
% 0.44/0.30 % (283218)Success in time 0.088 s
% 0.44/0.30 % Vampire exiting
%------------------------------------------------------------------------------