%------------------------------------------------------------------------------
% 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 : 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 : Fri Sep 25 03:38:00 PM UTC 2026
% Result : Satisfiable 2.98s 11.31s
% Output : FiniteModel 2.98s
% 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"
& a1410 = "d0"
& a1416 = "d0"
& a1523 = "d0"
& a1521 = "d0"
& a1400 = "d0"
& a1401 = "d0"
& a1522 = "d0"
& a1524 = "d2"
& a1520 = "d0"
& a1409 = "d2"
& a1408 = "d0"
& a1406 = "d0"
& a1407 = "d0"
& a1525 = "d0"
& a1526 = "d0"
& a1512 = "d0"
& a1513 = "d0"
& a1510 = "d0"
& a1511 = "d0"
& a1518 = "d0"
& a1519 = "d0"
& a1516 = "d0"
& a1517 = "d0"
& a1514 = "d0"
& a1515 = "d1"
& a1501 = "d1"
& a1502 = "d0"
& a1500 = "d2"
& a1509 = "d0"
& a1507 = "d0"
& a1508 = "d0"
& a1505 = "d0"
& a1506 = "d0"
& a1503 = "d0"
& a1504 = "d1"
& a1457 = "d0"
& a1336 = "d0"
& a1335 = "d2"
& a1334 = "d0"
& a1455 = "d0"
& a1337 = "d2"
& a1456 = "d0"
& a1458 = "d2"
& a1332 = "d0"
& a1333 = "d1"
& a1452 = "d2"
& a1451 = "d0"
& a1453 = "d2"
& a1454 = "d2"
& a1459 = "d0"
& a1338 = "d0"
& a1339 = "d0"
& a1340 = "d1"
& a1461 = "d0"
& a1460 = "d1"
& a1325 = "d0"
& a1326 = "d0"
& a1446 = "d2"
& a1444 = "d0"
& a1324 = "d0"
& a1445 = "d0"
& a1447 = "d2"
& a1442 = "d0"
& a1443 = "d0"
& a1440 = "d0"
& a1441 = "d0"
& a1449 = "d1"
& a1448 = "d0"
& a1450 = "d0"
& a1435 = "d0"
& a1433 = "d2"
& a1436 = "d1"
& a1434 = "d0"
& a1430 = "d2"
& a1431 = "d2"
& a1432 = "d2"
& a1439 = "d0"
& a1438 = "d1"
& a1437 = "d1"
& a1424 = "d0"
& a1425 = "d0"
& a1423 = "d0"
& a1429 = "d1"
& a1426 = "d0"
& a1428 = "d2"
& a1427 = "d0"
& a1378 = "d2"
& a1499 = "d2"
& a1379 = "d2"
& a1377 = "d1"
& a1376 = "d0"
& a1497 = "d0"
& a1374 = "d0"
& a1498 = "d2"
& a1375 = "d0"
& a1496 = "d0"
& a1495 = "d1"
& a1384 = "d0"
& a1488 = "d0"
& a1489 = "d0"
& a1486 = "d0"
& a1487 = "d1"
& a1365 = "d0"
& a1366 = "d0"
& a1364 = "d1"
& a1484 = "d0"
& a1363 = "d1"
& a1485 = "d0"
& a1493 = "d0"
& a1373 = "d1"
& a1494 = "d1"
& a1491 = "d2"
& a1492 = "d0"
& a1490 = "d0"
& a1479 = "d0"
& a1358 = "d0"
& a1359 = "d0"
& a1477 = "d0"
& a1478 = "d0"
& a1357 = "d0"
& a1354 = "d0"
& a1475 = "d0"
& a1476 = "d0"
& a1355 = "d0"
& a1473 = "d0"
& a1352 = "d0"
& a1474 = "d0"
& a1353 = "d0"
& a1482 = "d0"
& a1480 = "d2"
& a1361 = "d0"
& a1362 = "d0"
& a1481 = "d2"
& a1360 = "d0"
& a1483 = "d2"
& a1468 = "d0"
& a1347 = "d0"
& a1469 = "d0"
& a1466 = "d0"
& a1346 = "d0"
& a1467 = "d0"
& a1465 = "d1"
& a1464 = "d0"
& a1341 = "d0"
& a1462 = "d0"
& a1463 = "d0"
& a1471 = "d0"
& a1472 = "d0"
& a1350 = "d1"
& a1470 = "d0"
& a1398 = "d0"
& a1399 = "d0"
& a1397 = "d0"
& a1396 = "d1"
& a1389 = "d0"
& a1388 = "d0"
& a1385 = "d0"
& a1386 = "d0"
& a1394 = "d0"
& a1395 = "d0"
& a1392 = "d0"
& a1393 = "d0"
& a1390 = "d0"
& a1391 = "d0" ) ).
fof(predicate_mappings,interpretation-mappings,
( c5_1("d1")
& ~ c5_1("d0")
& ~ c5_1("d2")
& 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
& ~ 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
& ~ 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")
& ssSkP9("d0")
& ssSkP9("d1")
& ssSkP9("d2")
& ssSkC35
& ssSkC34
& ssSkC31
& ssSkC30
& ~ ssSkC33
& ~ ssSkC32
& ~ ssSkP5("d0")
& ssSkP7("d2")
& ssSkP5("d1")
& ssSkP6("d2")
& ssSkP5("d2")
& ssSkP6("d1")
& ssSkP7("d0")
& ssSkP6("d0")
& ssSkP7("d1")
& ssSkP3("d2")
& ssSkP2("d2")
& ~ ssSkP2("d1")
& ssSkP3("d0")
& ssSkP2("d0")
& ssSkP3("d1")
& ssSkP10("d2")
& ssSkP10("d0")
& ssSkP10("d1")
& ssSkP11("d1")
& ssSkP12("d0")
& ssSkP13("d2")
& ssSkP11("d0")
& ~ ssSkP12("d1")
& ssSkP13("d1")
& ssSkP12("d2")
& ssSkP13("d0")
& ssSkP11("d2")
& ssSkC17
& ssSkC16
& ~ ssSkC19
& ssSkC18
& ~ ssSkC14
& ssSkC11
& ssSkC10
& ssSkC4
& ssSkC6
& ssSkC5
& ssSkC8
& ssSkC9
& ~ ssSkC0
& ssSkC28
& ssSkC27
& ssSkC2
& ~ ssSkC29
& ssSkC24
& ndr1_1("d1")
& ~ ssSkC23
& ndr1_1("d0")
& ssSkC26
& ssSkC25
& ndr1_1("d2")
& ~ ssSkC20
& ssSkC22
& ~ ssSkC21
& ndr1_0
& c1_1("d1")
& ~ c1_1("d0")
& c1_1("d2")
& ~ c2_2("d1","d2")
& c2_2("d2","d1")
& ~ c2_0
& ~ c2_2("d0","d2")
& c2_2("d2","d0")
& c2_2("d0","d1")
& c2_2("d1","d0")
& c2_2("d2","d2")
& ~ c2_2("d1","d1")
& c2_2("d0","d0")
& ~ 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.03 % Problem : SYN520-1 : TPTP v9.3.1. Released v2.1.0.
% 0.00/0.04 % Command : run_fmb4j /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.11/10.38 % Computer : n008.cluster.edu
% 0.11/10.38 % Model : x86_64 x86_64
% 0.11/10.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/10.38 % Memory : 8046.5625MB
% 0.11/10.38 % OS : Linux 6.8.0-71-generic
% 0.11/10.38 % CPULimit : 300
% 0.11/10.38 % WCLimit : 300
% 0.11/10.38 % DateTime : Fri Sep 25 01:41:51 UTC 2026
% 0.11/10.39 % CPUTime :
% 0.11/10.39 Running run_fmb4j /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.16/10.46 Running: java -jar /export/starexec/sandbox/solver/bin/FMB4J.jar /export/starexec/sandbox/tmp/tmp.RZABBQWe4x/theBenchmark.cnf 300
% 0.16/10.84 % domain size: 1
% 0.16/10.96 % domain size: 2
% 0.16/11.03 % domain size: 3
% 2.55/11.30 % model found for domain size 3
% 2.98/11.31 % SZS status CounterSatisfiable for theBenchmark
% 2.98/11.31 % SZS output start FiniteModel for theBenchmark
% See solution above
% 0.21/11.40 % FMB4L exiting
%------------------------------------------------------------------------------