%------------------------------------------------------------------------------
% File : FMB4J---0.1
% Problem : SYN912-1 : TPTP v9.3.1. Released v2.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_fmb4j /export/starexec/sandbox/benchmark/theBenchmark.p 300
% Computer : n005.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:39 PM UTC 2026
% Result : Satisfiable 1.03s 0.96s
% Output : FiniteModel 1.46s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
fof(domain,interpretation-domains,
! [X] :
( X = "d1"
| X = "d0" ) ).
fof(mappings,interpretation-mappings,
( skf81("d0") = "d0"
& skf80("d1") = "d0"
& skf81("d1") = "d0"
& skf80("d0") = "d0"
& skf83("d0") = "d0"
& skf82("d1") = "d0"
& skf83("d1") = "d0"
& skf82("d0") = "d0"
& skf85("d0") = "d0"
& skf84("d1") = "d0"
& skf85("d1") = "d0"
& skf84("d0") = "d0"
& skf86("d1") = "d0"
& skf87("d1") = "d1"
& skf87("d0") = "d0"
& skf86("d0") = "d0"
& skf89("d1") = "d1"
& skf89("d0") = "d0"
& skf88("d1") = "d1"
& skf88("d0") = "d0"
& skf90("d1") = "d1"
& skf90("d0") = "d0"
& skf92("d1") = "d1"
& skf92("d0") = "d0"
& skf91("d1") = "d1"
& skf91("d0") = "d0"
& skf94("d1") = "d1"
& skf94("d0") = "d0"
& skf93("d1") = "d1"
& skf93("d0") = "d0"
& skf96("d1") = "d1"
& skf96("d0") = "d0"
& skf95("d1") = "d1"
& skf95("d0") = "d0"
& skf98("d1") = "d1"
& skf98("d0") = "d0"
& skf97("d1") = "d1"
& skf97("d0") = "d0"
& skf99("d1") = "d1"
& skf99("d0") = "d0"
& skf70("d1") = "d1"
& skf70("d0") = "d1"
& skf72("d0") = "d0"
& skf71("d0") = "d1"
& skf71("d1") = "d0"
& skf72("d1") = "d0"
& skf74("d0") = "d0"
& skf73("d1") = "d0"
& skf74("d1") = "d0"
& skf73("d0") = "d0"
& skf76("d0") = "d0"
& skf75("d1") = "d0"
& skf76("d1") = "d0"
& skf75("d0") = "d0"
& skf78("d0") = "d0"
& skf77("d1") = "d0"
& skf78("d1") = "d0"
& skf77("d0") = "d0"
& skf79("d1") = "d0"
& skf79("d0") = "d0"
& skc81 = "d0"
& skf104("d1") = "d1"
& skf103("d0") = "d1"
& skf104("d0") = "d1"
& skf103("d1") = "d1"
& skf102("d1") = "d1"
& skf102("d0") = "d0"
& skf101("d1") = "d1"
& skf101("d0") = "d0"
& skf100("d1") = "d1"
& skf100("d0") = "d0"
& skf109("d0") = "d1"
& skf109("d1") = "d1"
& skf108("d1") = "d1"
& skf107("d0") = "d1"
& skf108("d0") = "d1"
& skf107("d1") = "d1"
& skf106("d1") = "d1"
& skf105("d0") = "d1"
& skf106("d0") = "d1"
& skf105("d1") = "d1"
& skf115("d1") = "d1"
& skf114("d0") = "d1"
& skf115("d0") = "d1"
& skf114("d1") = "d1"
& skf113("d1") = "d1"
& skf112("d0") = "d1"
& skf113("d0") = "d1"
& skf112("d1") = "d1"
& skf111("d1") = "d1"
& skf110("d0") = "d1"
& skf111("d0") = "d1"
& skf110("d1") = "d1"
& skf119("d1") = "d1"
& skf118("d0") = "d1"
& skf119("d0") = "d1"
& skf118("d1") = "d1"
& skf117("d1") = "d1"
& skf116("d0") = "d1"
& skf117("d0") = "d1"
& skf116("d1") = "d1"
& skf126("d1") = "d1"
& skf125("d0") = "d1"
& skf126("d0") = "d1"
& skf125("d1") = "d1"
& skf124("d1") = "d1"
& skf123("d0") = "d1"
& skf124("d0") = "d1"
& skf123("d1") = "d1"
& skf122("d1") = "d1"
& skf121("d0") = "d1"
& skf122("d0") = "d1"
& skf121("d1") = "d1"
& skf120("d1") = "d1"
& skf120("d0") = "d1"
& skf129("d0") = "d1"
& skf129("d1") = "d1"
& skf128("d1") = "d1"
& skf127("d0") = "d1"
& skf128("d0") = "d1"
& skf127("d1") = "d1"
& skf137("d1") = "d1"
& skf136("d0") = "d1"
& skf137("d0") = "d1"
& skf136("d1") = "d1"
& skf135("d1") = "d1"
& skf134("d0") = "d1"
& skf135("d0") = "d1"
& skf134("d1") = "d1"
& skf133("d1") = "d1"
& skf132("d0") = "d1"
& skf133("d0") = "d1"
& skf132("d1") = "d1"
& skf131("d1") = "d1"
& skf130("d0") = "d1"
& skf131("d0") = "d1"
& skf130("d1") = "d1"
& skf139("d1") = "d1"
& skf138("d0") = "d1"
& skf139("d0") = "d1"
& skf138("d1") = "d1" ) ).
fof(predicate_mappings,interpretation-mappings,
( ssSkP1529("d0")
& ssSkP1528("d1")
& ssSkP1529("d1")
& ssSkP1528("d0")
& ssSkP1527("d0")
& ssSkP1526("d1")
& ssSkP1527("d1")
& ssSkP1526("d0")
& ssSkP1531("d1")
& ssSkP1532("d0")
& ssSkP1531("d0")
& ssSkP1532("d1")
& ssSkP1530("d0")
& ssSkP1530("d1")
& ssSkP1535("d1")
& ssSkP1536("d0")
& ssSkP1535("d0")
& ssSkP1536("d1")
& ssSkP1533("d1")
& ssSkP1534("d0")
& ssSkP1533("d0")
& ssSkP1534("d1")
& ssSkP1517("d1")
& ssSkP1518("d0")
& ssSkP1517("d0")
& ssSkP1518("d1")
& ssSkP1515("d1")
& ssSkP1516("d0")
& ssSkP1515("d0")
& ssSkP1516("d1")
& ssSkP1519("d1")
& ssSkP1519("d0")
& ssSkP1520("d1")
& ssSkP1521("d0")
& ssSkP1520("d0")
& ssSkP1521("d1")
& ssSkP1525("d0")
& ssSkP1524("d1")
& ssSkP1525("d1")
& ssSkP1524("d0")
& ssSkP1523("d0")
& ssSkP1522("d1")
& ssSkP1523("d1")
& ssSkP1522("d0")
& ssSkP1506("d1")
& ssSkP1507("d0")
& ssSkP1506("d0")
& ssSkP1507("d1")
& ssSkP1504("d1")
& ssSkP1505("d0")
& ~ ssSkP1504("d0")
& ssSkP1505("d1")
& ssSkP1508("d1")
& ssSkP1509("d0")
& ssSkP1508("d0")
& ssSkP1509("d1")
& ssSkP1510("d0")
& ssSkP1510("d1")
& ssSkP1513("d1")
& ssSkP1514("d0")
& ssSkP1513("d0")
& ssSkP1514("d1")
& ssSkP1511("d1")
& ssSkP1512("d0")
& ssSkP1511("d0")
& ssSkP1512("d1")
& ~ ssSkP1503("d0")
& ssSkP1502("d1")
& ssSkP1503("d1")
& ~ ssSkP1502("d0")
& ~ ssSkP1501("d0")
& ssSkP1500("d1")
& ssSkP1501("d1")
& ~ ssSkP1500("d0")
& ssPv26("d1")
& ~ ssPv27("d0")
& ~ ssPv26("d0")
& ssPv27("d1")
& ~ ssPv25("d0")
& ssPv25("d1")
& ssPv28("d1")
& ~ ssPv29("d0")
& ~ ssPv28("d0")
& ssPv29("d1")
& ~ ssPv30("d0")
& ssPv30("d1")
& ssPv31("d1")
& ~ ssPv32("d0")
& ~ ssPv31("d0")
& ssPv32("d1")
& ~ ssPv16("d0")
& ssPv15("d1")
& ssPv16("d1")
& ~ ssPv15("d0")
& ssPv13("d1")
& ~ ssPv14("d0")
& ~ ssPv13("d0")
& ssPv14("d1")
& ~ ssPv12("d0")
& ssPv11("d1")
& ssPv12("d1")
& ~ ssPv11("d0")
& ~ ssPv10("d0")
& ssPv10("d1")
& ~ ssSkC40
& ssPv9("d1")
& ~ ssPv9("d0")
& ~ ssSkP1491("d0")
& ssSkP1490("d1")
& ssSkP1491("d1")
& ~ ssSkP1490("d0")
& ~ ssSkP1495("d0")
& ssSkP1494("d1")
& ssSkP1495("d1")
& ~ ssSkP1494("d0")
& ~ ssSkP1493("d0")
& ssSkP1492("d1")
& ssSkP1493("d1")
& ~ ssSkP1492("d0")
& ~ ssSkP1499("d0")
& ssSkP1498("d1")
& ssSkP1499("d1")
& ~ ssSkP1498("d0")
& ssSkP1471("d1","d1")
& ssSkP1471("d0","d0")
& ~ ssSkP1497("d0")
& ssSkP1496("d1")
& ssSkP1471("d0","d1")
& ssSkP1471("d1","d0")
& ssSkP1497("d1")
& ~ ssSkP1496("d0")
& ~ ssSkP1480("d0")
& ssSkP1480("d1")
& ssSkP1483("d1")
& ~ ssSkP1484("d0")
& ~ ssSkP1483("d0")
& ssSkP1484("d1")
& ~ ssSkP1482("d0")
& ssSkP1481("d1")
& ssSkP1482("d1")
& ~ ssSkP1481("d0")
& ssSkP1487("d1")
& ~ ssSkP1488("d0")
& ~ ssSkP1487("d0")
& ssSkP1488("d1")
& ssSkP1485("d1")
& ~ ssSkP1486("d0")
& ~ ssSkP1485("d0")
& ssSkP1486("d1")
& ssSkP1489("d1")
& ssSkP1489("d0")
& ssSkP1590("d0")
& ssSkP1590("d1")
& ssSkP1594("d0")
& ssSkP1593("d1")
& ~ ssSkP1473("d0")
& ssSkP1472("d1")
& ~ ssSkP1594("d1")
& ssSkP1593("d0")
& ssSkP1473("d1")
& ~ ssSkP1472("d0")
& ssSkP1470("d1")
& ssSkP1592("d0")
& ssSkP1591("d1")
& ~ ssSkP1470("d0")
& ssSkP1592("d1")
& ssSkP1591("d0")
& ssSkP1476("d1")
& ~ ssSkP1477("d0")
& ~ ssSkP1476("d0")
& ssSkP1477("d1")
& ssSkP1474("d1")
& ~ ssSkP1475("d0")
& ~ ssSkP1595("d1")
& ~ ssSkP1474("d0")
& ssSkP1475("d1")
& ssSkP1595("d0")
& ~ ssSkP1479("d0")
& ssSkP1478("d1")
& ssSkP1479("d1")
& ~ ssSkP1478("d0")
& ssSkP1461("d1")
& ~ ssSkP1462("d0")
& ssSkP1583("d0")
& ssSkP1582("d1")
& ~ ssSkP1461("d0")
& ssSkP1462("d1")
& ssSkP1583("d1")
& ssSkP1582("d0")
& ~ ssSkP1460("d0")
& ssSkP1581("d0")
& ssSkP1580("d1")
& ssSkP1460("d1")
& ssSkP1581("d1")
& ssSkP1580("d0")
& ssSkP1465("d1")
& ~ ssSkP1466("d0")
& ssSkP1587("d0")
& ssSkP1586("d1")
& ~ ssSkP1465("d0")
& ssSkP1466("d1")
& ssSkP1587("d1")
& ssSkP1586("d0")
& ~ ssSkP1464("d0")
& ssSkP1463("d1")
& ssSkP1585("d0")
& ssSkP1584("d1")
& ssSkP1464("d1")
& ~ ssSkP1463("d0")
& ssSkP1585("d1")
& ssSkP1584("d0")
& ssSkP1469("d1")
& ~ ssSkP1469("d0")
& ssSkP1467("d1")
& ~ ssSkP1468("d0")
& ssSkP1589("d0")
& ssSkP1588("d1")
& ~ ssSkP1467("d0")
& ssSkP1468("d1")
& ssSkP1589("d1")
& ssSkP1588("d0")
& ssSkP1571("d1")
& ssSkP1572("d0")
& ssSkP1571("d0")
& ssSkP1572("d1")
& ssSkP1570("d0")
& ssSkP1570("d1")
& ~ ssSkP1455("d0")
& ssSkP1575("d1")
& ssSkP1576("d0")
& ssSkP1455("d1")
& ssSkP1575("d0")
& ssSkP1576("d1")
& ssSkP1573("d1")
& ssSkP1574("d0")
& ssSkP1453("d0")
& ssSkP1573("d0")
& ssSkP1574("d1")
& ssSkP1453("d1")
& ssSkP1458("d1")
& ~ ssSkP1459("d0")
& ssSkP1579("d1")
& ~ ssSkP1458("d0")
& ssSkP1459("d1")
& ssSkP1579("d0")
& ssSkP1456("d1")
& ~ ssSkP1457("d0")
& ssSkP1577("d1")
& ssSkP1578("d0")
& ~ ssSkP1456("d0")
& ssSkP1457("d1")
& ssSkP1577("d0")
& ssSkP1578("d1")
& ssSkP1559("d1")
& ssSkP1559("d0")
& ssSkP1561("d0")
& ssSkP1560("d1")
& ssSkP1561("d1")
& ssSkP1560("d0")
& ssSkP1565("d0")
& ssSkP1564("d1")
& ssSkP1565("d1")
& ssSkP1564("d0")
& ssSkP1563("d0")
& ssSkP1562("d1")
& ssSkP1563("d1")
& ssSkP1562("d0")
& ssSkP1569("d0")
& ssSkP1568("d1")
& ssSkP1569("d1")
& ssSkP1568("d0")
& ssSkP1567("d0")
& ssSkP1566("d1")
& ssSkP1567("d1")
& ssSkP1566("d0")
& ssSkP1549("d0")
& ssSkP1548("d1")
& ssSkP1549("d1")
& ssSkP1548("d0")
& ssRr("d1","d1")
& ~ ssRr("d0","d0")
& ssRr("d0","d1")
& ssRr("d1","d0")
& ssSkP1454("d1","d0")
& ssSkP1454("d0","d1")
& ssSkP1550("d0")
& ssSkP1454("d1","d1")
& ssSkP1454("d0","d0")
& ssSkP1550("d1")
& ssSkP1553("d1")
& ssSkP1554("d0")
& ssSkP1553("d0")
& ssSkP1554("d1")
& ssSkP1551("d1")
& ssSkP1552("d0")
& ssSkP1551("d0")
& ssSkP1552("d1")
& ssSkP1557("d1")
& ssSkP1558("d0")
& ssSkP1557("d0")
& ssSkP1558("d1")
& ssSkP1555("d1")
& ssSkP1556("d0")
& ssSkP1555("d0")
& ssSkP1556("d1")
& ssSkP1539("d1")
& ssSkP1539("d0")
& ssSkP1537("d1")
& ssSkP1538("d0")
& ssSkP1537("d0")
& ssSkP1538("d1")
& ssSkP1543("d0")
& ssSkP1542("d1")
& ssSkP1543("d1")
& ssSkP1542("d0")
& ssSkP1541("d0")
& ssSkP1540("d1")
& ssSkP1541("d1")
& ssSkP1540("d0")
& ssSkP1547("d0")
& ssSkP1546("d1")
& ssSkP1547("d1")
& ssSkP1546("d0")
& ssSkP1545("d0")
& ssSkP1544("d1")
& ssSkP1545("d1")
& ssSkP1544("d0") ) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYN912-1 : TPTP v9.3.1. Released v2.5.0.
% 0.00/0.04 % Command : run_fmb4j /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.10/0.36 % Computer : n005.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.37 % CPULimit : 300
% 0.10/0.37 % WCLimit : 300
% 0.10/0.37 % DateTime : Fri Sep 25 02:33:02 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.37 Running run_fmb4j /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.10/0.46 Running: java -jar /export/starexec/sandbox/solver/bin/FMB4J.jar /export/starexec/sandbox/tmp/tmp.lJQzlXTjef/theBenchmark.cnf 300
% 0.80/0.80 % domain size: 1
% 1.03/0.90 % domain size: 2
% 1.03/0.94 % model found for domain size 2
% 1.03/0.96 % SZS status CounterSatisfiable for theBenchmark
% 1.03/0.96 % SZS output start FiniteModel for theBenchmark
% See solution above
% 1.46/1.05 % FMB4L exiting
%------------------------------------------------------------------------------