%------------------------------------------------------------------------------
% File : FMB4J---0.1
% Problem : SYN520+1 : TPTP v9.3.1. Released v2.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_fmb4j /export/starexec/sandbox/benchmark/theBenchmark.p 300
% Computer : n003.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 : Fri Sep 25 03:37:59 PM UTC 2026
% Result : CounterSatisfiable 3.44s 16.42s
% Output : FiniteModel 3.44s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
fof(domain,interpretation-domains,
! [X] :
( X = "d2"
| X = "d1"
| X = "d0" ) ).
fof(mappings,interpretation-mappings,
( a1413 = "d0"
& a1414 = "d0"
& a1411 = "d0"
& a1412 = "d0"
& a1410 = "d1"
& a1419 = "d0"
& a1417 = "d0"
& a1415 = "d0"
& a1416 = "d0"
& a1418 = "d2"
& a1402 = "d1"
& a1403 = "d2"
& a1401 = "d0"
& a1400 = "d1"
& a1408 = "d2"
& a1409 = "d2"
& a1407 = "d1"
& a1406 = "d1"
& a1404 = "d0"
& a1405 = "d0"
& a1457 = "d0"
& a1455 = "d0"
& a1458 = "d2"
& a1456 = "d0"
& a1454 = "d0"
& a1453 = "d2"
& a1451 = "d0"
& a1452 = "d0"
& a1459 = "d0"
& a1460 = "d0"
& a1461 = "d0"
& a1447 = "d0"
& a1446 = "d2"
& a1444 = "d0"
& a1445 = "d0"
& a1442 = "d0"
& a1440 = "d0"
& a1441 = "d0"
& a1443 = "d2"
& a1448 = "d0"
& a1449 = "d0"
& a1450 = "d0"
& a1436 = "d1"
& a1435 = "d0"
& a1433 = "d1"
& a1434 = "d0"
& a1432 = "d0"
& a1431 = "d1"
& a1430 = "d2"
& a1437 = "d2"
& a1439 = "d0"
& a1438 = "d2"
& a1424 = "d0"
& a1425 = "d0"
& a1422 = "d0"
& a1423 = "d0"
& a1420 = "d0"
& a1421 = "d0"
& a1428 = "d2"
& a1426 = "d0"
& a1429 = "d2"
& a1427 = "d0"
& a1378 = "d2"
& a1379 = "d1"
& a1374 = "d2"
& a1375 = "d2"
& a1376 = "d2"
& a1377 = "d2"
& a1383 = "d0"
& a1384 = "d0"
& a1381 = "d0"
& a1382 = "d0"
& a1380 = "d0"
& a1369 = "d0"
& a1367 = "d0"
& a1368 = "d0"
& a1366 = "d0"
& a1364 = "d2"
& a1365 = "d2"
& a1363 = "d1"
& a1371 = "d2"
& a1370 = "d0"
& a1372 = "d2"
& a1373 = "d2"
& a1359 = "d1"
& a1358 = "d1"
& a1356 = "d0"
& a1357 = "d1"
& a1354 = "d0"
& a1355 = "d0"
& a1352 = "d0"
& a1353 = "d0"
& a1361 = "d0"
& a1362 = "d0"
& a1360 = "d2"
& a1348 = "d0"
& a1345 = "d0"
& a1347 = "d2"
& a1346 = "d0"
& a1344 = "d1"
& a1343 = "d0"
& a1341 = "d2"
& a1342 = "d0"
& a1349 = "d0"
& a1351 = "d0"
& a1350 = "d1"
& a1398 = "d0"
& a1399 = "d0"
& a1396 = "d0"
& a1397 = "d0"
& a1389 = "d2"
& a1387 = "d0"
& a1388 = "d0"
& a1385 = "d0"
& a1386 = "d0"
& a1395 = "d1"
& a1394 = "d2"
& a1393 = "d1"
& a1392 = "d0"
& a1390 = "d0"
& a1391 = "d0"
& a1523 = "d0"
& a1524 = "d0"
& a1521 = "d0"
& a1522 = "d0"
& a1520 = "d0"
& a1526 = "d2"
& a1525 = "d0"
& a1512 = "d0"
& a1513 = "d0"
& a1510 = "d0"
& a1511 = "d0"
& a1518 = "d0"
& a1519 = "d0"
& a1517 = "d0"
& a1516 = "d1"
& a1514 = "d0"
& a1515 = "d0"
& a1502 = "d0"
& a1501 = "d1"
& a1500 = "d2"
& a1509 = "d0"
& a1507 = "d0"
& a1508 = "d0"
& a1505 = "d0"
& a1503 = "d2"
& a1506 = "d0"
& a1504 = "d2"
& a1335 = "d2"
& a1334 = "d0"
& a1336 = "d2"
& a1337 = "d2"
& a1333 = "d1"
& a1332 = "d0"
& a1330 = "d0"
& a1331 = "d0"
& a1338 = "d0"
& a1339 = "d0"
& a1340 = "d0"
& a1326 = "d0"
& a1324 = "d2"
& a1325 = "d1"
& a1323 = "d0"
& a1329 = "d0"
& a1327 = "d0"
& a1328 = "d0"
& a1499 = "d0"
& a1498 = "d0"
& a1497 = "d1"
& a1495 = "d0"
& a1496 = "d0"
& a1488 = "d0"
& a1489 = "d0"
& a1486 = "d0"
& a1487 = "d1"
& a1485 = "d1"
& a1484 = "d0"
& a1494 = "d1"
& a1493 = "d0"
& a1491 = "d0"
& a1492 = "d0"
& a1490 = "d0"
& a1479 = "d0"
& a1477 = "d0"
& a1478 = "d0"
& a1475 = "d0"
& a1476 = "d0"
& a1473 = "d0"
& a1474 = "d0"
& a1483 = "d0"
& a1480 = "d0"
& a1482 = "d2"
& a1481 = "d0"
& a1468 = "d0"
& a1469 = "d0"
& a1466 = "d0"
& a1467 = "d0"
& a1465 = "d0"
& a1464 = "d2"
& a1462 = "d0"
& a1463 = "d0"
& a1471 = "d0"
& a1472 = "d0"
& a1470 = "d0" ) ).
fof(predicate_mappings,interpretation-mappings,
( ~ c5_2("d2","d2")
& ~ c5_2("d1","d1")
& c5_2("d0","d0")
& c5_2("d0","d1")
& c5_2("d1","d0")
& c5_2("d0","d2")
& ~ c5_2("d2","d0")
& c5_2("d1","d2")
& ~ c5_2("d2","d1")
& ~ c5_0
& ~ c4_1("d2")
& c4_1("d0")
& ~ c4_1("d1")
& c3_0
& c3_2("d0","d2")
& c3_2("d2","d0")
& ~ c3_2("d1","d2")
& ~ c3_2("d2","d1")
& ~ c3_2("d2","d2")
& c3_2("d1","d1")
& c3_2("d0","d0")
& ~ c3_2("d0","d1")
& c3_2("d1","d0")
& ndr1_0
& c1_1("d1")
& ~ c1_1("d0")
& c1_1("d2")
& ~ c2_2("d1","d2")
& c2_2("d2","d1")
& c2_2("d0","d2")
& c2_2("d2","d0")
& ~ c2_0
& ~ c2_2("d0","d1")
& c2_2("d1","d0")
& c2_2("d2","d2")
& c2_2("d1","d1")
& c2_2("d0","d0")
& c5_1("d1")
& ~ c5_1("d0")
& ~ c5_1("d2")
& ~ c3_1("d2")
& c3_1("d1")
& c3_1("d0")
& ~ c4_2("d0","d1")
& c4_2("d1","d0")
& c4_2("d2","d2")
& c4_2("d1","d1")
& c4_2("d0","d0")
& ~ c4_2("d1","d2")
& ~ c4_2("d2","d1")
& c4_2("d0","d2")
& ~ c4_2("d2","d0")
& ~ c4_0
& ndr1_1("d1")
& ndr1_1("d0")
& ndr1_1("d2")
& ~ c1_0
& c2_1("d0")
& ~ c2_1("d1")
& c2_1("d2")
& c1_2("d2","d2")
& c1_2("d1","d1")
& ~ c1_2("d0","d0")
& c1_2("d0","d1")
& ~ c1_2("d1","d0")
& ~ c1_2("d0","d2")
& c1_2("d2","d0")
& c1_2("d1","d2")
& c1_2("d2","d1") ) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SYN520+1 : TPTP v9.3.1. Released v2.1.0.
% 0.00/0.03 % Command : run_fmb4j /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.09/15.37 % Computer : n003.cluster.edu
% 0.09/15.37 % Model : x86_64 x86_64
% 0.09/15.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/15.37 % Memory : 8046.5625MB
% 0.09/15.37 % OS : Linux 6.8.0-71-generic
% 0.09/15.37 % CPULimit : 300
% 0.09/15.37 % WCLimit : 300
% 0.09/15.37 % DateTime : Fri Sep 25 01:42:52 UTC 2026
% 0.09/15.37 % CPUTime :
% 0.09/15.37 Running run_fmb4j /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.12/15.47 Running: java -jar /export/starexec/sandbox/solver/bin/FMB4J.jar /export/starexec/sandbox/tmp/tmp.ydvab9rS6v/theBenchmark.cnf 300
% 0.12/15.85 % domain size: 1
% 0.12/15.97 % domain size: 2
% 1.91/16.04 % domain size: 3
% 3.44/16.41 % model found for domain size 3
% 3.44/16.42 % SZS status CounterSatisfiable for theBenchmark
% 3.44/16.42 % SZS output start FiniteModel for theBenchmark
% See solution above
% 0.18/16.52 % FMB4L exiting
%------------------------------------------------------------------------------