%------------------------------------------------------------------------------
% File : FMB4J---0.1
% Problem : SYN427+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 : n019.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:43 PM UTC 2026
% Result : CounterSatisfiable 2.76s 1.41s
% Output : FiniteModel 2.76s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
fof(domain,interpretation-domains,
! [X] :
( X = "d1"
| X = "d0" ) ).
fof(mappings,interpretation-mappings,
( a1655 = "d0"
& a1656 = "d0"
& a1653 = "d0"
& a1654 = "d0"
& a1651 = "d0"
& a1652 = "d0"
& a1650 = "d0"
& a1659 = "d0"
& a1657 = "d0"
& a1658 = "d0"
& a1645 = "d0"
& a1644 = "d1"
& a1643 = "d1"
& a1642 = "d0"
& a1640 = "d0"
& a1641 = "d0"
& a1648 = "d0"
& a1649 = "d0"
& a1647 = "d1"
& a1646 = "d0"
& a1633 = "d1"
& a1634 = "d0"
& a1632 = "d0"
& a1631 = "d1"
& a1630 = "d1"
& a1639 = "d0"
& a1637 = "d0"
& a1638 = "d0"
& a1635 = "d0"
& a1636 = "d0"
& a1623 = "d0"
& a1622 = "d1"
& a1621 = "d1"
& a1620 = "d1"
& a1628 = "d0"
& a1629 = "d1"
& a1626 = "d0"
& a1627 = "d0"
& a1624 = "d0"
& a1625 = "d0"
& a1699 = "d1"
& a1697 = "d0"
& a1698 = "d0"
& a1696 = "d0"
& a1695 = "d1"
& a1693 = "d0"
& a1694 = "d0"
& a1688 = "d0"
& a1689 = "d0"
& a1686 = "d0"
& a1687 = "d0"
& a1685 = "d0"
& a1684 = "d1"
& a1683 = "d0"
& a1682 = "d1"
& a1692 = "d1"
& a1691 = "d0"
& a1690 = "d1"
& a1677 = "d0"
& a1678 = "d0"
& a1675 = "d0"
& a1676 = "d0"
& a1673 = "d0"
& a1674 = "d0"
& a1671 = "d0"
& a1672 = "d0"
& a1679 = "d0"
& a1681 = "d1"
& a1680 = "d0"
& a1666 = "d1"
& a1667 = "d0"
& a1664 = "d0"
& a1665 = "d0"
& a1662 = "d0"
& a1663 = "d0"
& a1660 = "d0"
& a1661 = "d0"
& a1668 = "d1"
& a1669 = "d0"
& a1670 = "d0"
& a1810 = "d0"
& a1816 = "d0"
& a1815 = "d0"
& a1818 = "d0"
& a1817 = "d0"
& a1812 = "d1"
& a1811 = "d0"
& a1814 = "d0"
& a1813 = "d1"
& a1819 = "d0"
& a1805 = "d0"
& a1804 = "d0"
& a1807 = "d0"
& a1806 = "d0"
& a1801 = "d0"
& a1800 = "d0"
& a1803 = "d0"
& a1802 = "d1"
& a1809 = "d0"
& a1808 = "d0"
& a1612 = "d1"
& a1611 = "d0"
& a1610 = "d1"
& a1619 = "d0"
& a1617 = "d0"
& a1618 = "d0"
& a1615 = "d0"
& a1616 = "d0"
& a1614 = "d1"
& a1613 = "d1"
& a1601 = "d1"
& a1600 = "d1"
& a1609 = "d1"
& a1608 = "d0"
& a1607 = "d1"
& a1606 = "d0"
& a1604 = "d0"
& a1605 = "d0"
& a1603 = "d1"
& a1602 = "d0"
& a1830 = "d0"
& a1831 = "d0"
& a1832 = "d1"
& a1833 = "d0"
& a1821 = "d0"
& a1820 = "d0"
& a1827 = "d0"
& a1826 = "d0"
& a1829 = "d0"
& a1828 = "d0"
& a1823 = "d0"
& a1822 = "d1"
& a1825 = "d0"
& a1824 = "d0"
& a1598 = "d0"
& a1599 = "d0"
& a1596 = "d0"
& a1597 = "d0"
& a1594 = "d0"
& a1595 = "d0"
& a1589 = "d0"
& a1588 = "d1"
& a1587 = "d1"
& a1585 = "d0"
& a1586 = "d0"
& a1583 = "d0"
& a1584 = "d0"
& a1592 = "d0"
& a1593 = "d1"
& a1590 = "d0"
& a1591 = "d0"
& a1775 = "d0"
& a1774 = "d0"
& a1776 = "d0"
& a1777 = "d1"
& a1771 = "d0"
& a1770 = "d0"
& a1773 = "d0"
& a1772 = "d0"
& a1779 = "d0"
& a1778 = "d0"
& a1780 = "d0"
& a1764 = "d0"
& a1763 = "d0"
& a1766 = "d0"
& a1765 = "d0"
& a1760 = "d0"
& a1762 = "d0"
& a1761 = "d0"
& a1768 = "d0"
& a1767 = "d0"
& a1769 = "d0"
& a1753 = "d0"
& a1752 = "d0"
& a1755 = "d0"
& a1754 = "d0"
& a1751 = "d0"
& a1750 = "d0"
& a1757 = "d0"
& a1756 = "d0"
& a1759 = "d0"
& a1758 = "d0"
& a1742 = "d0"
& a1741 = "d0"
& a1744 = "d0"
& a1743 = "d0"
& a1740 = "d0"
& a1749 = "d0"
& a1746 = "d0"
& a1745 = "d1"
& a1748 = "d0"
& a1747 = "d0"
& a1582 = "d1"
& a1581 = "d0"
& a1797 = "d1"
& a1796 = "d0"
& a1799 = "d0"
& a1798 = "d0"
& a1792 = "d0"
& a1793 = "d1"
& a1795 = "d0"
& a1794 = "d1"
& a1785 = "d1"
& a1786 = "d1"
& a1788 = "d0"
& a1787 = "d0"
& a1781 = "d1"
& a1782 = "d0"
& a1784 = "d0"
& a1783 = "d0"
& a1789 = "d0"
& a1790 = "d1"
& a1791 = "d1"
& a1730 = "d1"
& a1731 = "d1"
& a1733 = "d0"
& a1732 = "d0"
& a1739 = "d0"
& a1738 = "d0"
& a1735 = "d0"
& a1734 = "d0"
& a1737 = "d0"
& a1736 = "d0"
& a1720 = "d0"
& a1722 = "d0"
& a1721 = "d0"
& a1728 = "d0"
& a1727 = "d0"
& a1729 = "d1"
& a1724 = "d0"
& a1723 = "d0"
& a1725 = "d0"
& a1726 = "d1"
& a1711 = "d0"
& a1710 = "d0"
& a1717 = "d0"
& a1716 = "d0"
& a1719 = "d0"
& a1718 = "d0"
& a1713 = "d0"
& a1712 = "d0"
& a1715 = "d0"
& a1714 = "d0"
& a1700 = "d0"
& a1706 = "d0"
& a1705 = "d0"
& a1708 = "d0"
& a1707 = "d0"
& a1702 = "d0"
& a1701 = "d0"
& a1704 = "d0"
& a1703 = "d0"
& a1709 = "d0" ) ).
fof(predicate_mappings,interpretation-mappings,
( c6_1("d0")
& ~ c6_1("d1")
& ~ c5_2("d1","d1")
& ~ c5_2("d0","d0")
& c5_2("d0","d1")
& c5_2("d1","d0")
& c5_0
& c4_1("d0")
& ~ c4_1("d1")
& c3_0
& ~ c3_2("d1","d1")
& c3_2("d0","d0")
& ~ c3_2("d0","d1")
& c3_2("d1","d0")
& c9_2("d1","d1")
& c9_2("d0","d0")
& c9_2("d0","d1")
& ~ c9_2("d1","d0")
& c9_0
& c8_1("d0")
& c8_1("d1")
& c7_0
& c7_2("d1","d1")
& c7_2("d0","d0")
& ~ c7_2("d0","d1")
& ~ c7_2("d1","d0")
& c10_0
& c10_2("d0","d1")
& ~ c10_2("d1","d0")
& c10_2("d1","d1")
& ~ c10_2("d0","d0")
& ndr1_0
& ~ c1_1("d1")
& ~ c1_1("d0")
& c2_0
& ~ c2_2("d0","d1")
& ~ c2_2("d1","d0")
& c2_2("d1","d1")
& c2_2("d0","d0")
& c5_1("d1")
& ~ c5_1("d0")
& ~ c6_0
& ~ c6_2("d0","d1")
& ~ c6_2("d1","d0")
& ~ c6_2("d1","d1")
& c6_2("d0","d0")
& c3_1("d1")
& ~ c3_1("d0")
& ~ c4_2("d0","d1")
& c4_2("d1","d0")
& ~ c4_2("d1","d1")
& c4_2("d0","d0")
& ~ c4_0
& ~ c9_1("d1")
& ~ c9_1("d0")
& ~ c8_2("d0","d1")
& c8_2("d1","d0")
& ~ c8_2("d1","d1")
& c8_2("d0","d0")
& ~ c7_1("d1")
& ~ c7_1("d0")
& ~ c8_0
& c10_1("d0")
& c10_1("d1")
& ndr1_1("d1")
& ndr1_1("d0")
& c1_0
& ~ c2_1("d0")
& ~ c2_1("d1")
& c1_2("d1","d1")
& ~ c1_2("d0","d0")
& ~ c1_2("d0","d1")
& ~ c1_2("d1","d0") ) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYN427+1 : TPTP v9.3.1. Released v2.1.0.
% 0.00/0.04 % Command : run_fmb4j /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.10/0.53 % Computer : n019.cluster.edu
% 0.10/0.53 % Model : x86_64 x86_64
% 0.10/0.53 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.53 % Memory : 8046.5625MB
% 0.10/0.53 % OS : Linux 6.8.0-71-generic
% 0.10/0.53 % CPULimit : 300
% 0.10/0.53 % WCLimit : 300
% 0.10/0.53 % DateTime : Fri Sep 25 01:09:19 UTC 2026
% 0.10/0.54 % CPUTime :
% 0.10/0.54 Running run_fmb4j /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.14/0.64 Running: java -jar /export/starexec/sandbox/solver/bin/FMB4J.jar /export/starexec/sandbox/tmp/tmp.6m63rcknbU/theBenchmark.cnf 300
% 1.09/1.06 % domain size: 1
% 1.90/1.24 % domain size: 2
% 2.76/1.40 % model found for domain size 2
% 2.76/1.41 % SZS status CounterSatisfiable for theBenchmark
% 2.76/1.41 % SZS output start FiniteModel for theBenchmark
% See solution above
% 2.76/1.49 % FMB4L exiting
%------------------------------------------------------------------------------