%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SYN427-1 : TPTP v9.3.1. Released v2.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n014.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:07:51 PM UTC 2026
% Result : Satisfiable 0.53s 0.33s
% Output : FiniteModel 0.53s
% 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('finite_domain_$i',axiom,
! [X: $i] :
( ( X = 'fmb_$i_1' )
| ( X = 'fmb_$i_2' ) ) ).
tff('distinct_domain_$i',axiom,
'fmb_$i_1' != 'fmb_$i_2' ).
tff(declare_a1770,type,
a1770: $i ).
tff(a1770_definition,axiom,
a1770 = 'fmb_$i_1' ).
tff(declare_a1767,type,
a1767: $i ).
tff(a1767_definition,axiom,
a1767 = 'fmb_$i_2' ).
tff(declare_a1685,type,
a1685: $i ).
tff(a1685_definition,axiom,
a1685 = 'fmb_$i_2' ).
tff(declare_a1659,type,
a1659: $i ).
tff(a1659_definition,axiom,
a1659 = 'fmb_$i_2' ).
tff(declare_a1824,type,
a1824: $i ).
tff(a1824_definition,axiom,
a1824 = 'fmb_$i_2' ).
tff(declare_a1820,type,
a1820: $i ).
tff(a1820_definition,axiom,
a1820 = 'fmb_$i_2' ).
tff(declare_a1817,type,
a1817: $i ).
tff(a1817_definition,axiom,
a1817 = 'fmb_$i_2' ).
tff(declare_a1811,type,
a1811: $i ).
tff(a1811_definition,axiom,
a1811 = 'fmb_$i_2' ).
tff(declare_a1807,type,
a1807: $i ).
tff(a1807_definition,axiom,
a1807 = 'fmb_$i_2' ).
tff(declare_a1795,type,
a1795: $i ).
tff(a1795_definition,axiom,
a1795 = 'fmb_$i_2' ).
tff(declare_a1785,type,
a1785: $i ).
tff(a1785_definition,axiom,
a1785 = 'fmb_$i_2' ).
tff(declare_a1756,type,
a1756: $i ).
tff(a1756_definition,axiom,
a1756 = 'fmb_$i_2' ).
tff(declare_a1743,type,
a1743: $i ).
tff(a1743_definition,axiom,
a1743 = 'fmb_$i_2' ).
tff(declare_a1740,type,
a1740: $i ).
tff(a1740_definition,axiom,
a1740 = 'fmb_$i_2' ).
tff(declare_a1736,type,
a1736: $i ).
tff(a1736_definition,axiom,
a1736 = 'fmb_$i_2' ).
tff(declare_a1733,type,
a1733: $i ).
tff(a1733_definition,axiom,
a1733 = 'fmb_$i_2' ).
tff(declare_a1729,type,
a1729: $i ).
tff(a1729_definition,axiom,
a1729 = 'fmb_$i_2' ).
tff(declare_a1721,type,
a1721: $i ).
tff(a1721_definition,axiom,
a1721 = 'fmb_$i_2' ).
tff(declare_a1712,type,
a1712: $i ).
tff(a1712_definition,axiom,
a1712 = 'fmb_$i_2' ).
tff(declare_a1706,type,
a1706: $i ).
tff(a1706_definition,axiom,
a1706 = 'fmb_$i_2' ).
tff(declare_a1694,type,
a1694: $i ).
tff(a1694_definition,axiom,
a1694 = 'fmb_$i_2' ).
tff(declare_a1692,type,
a1692: $i ).
tff(a1692_definition,axiom,
a1692 = 'fmb_$i_2' ).
tff(declare_a1672,type,
a1672: $i ).
tff(a1672_definition,axiom,
a1672 = 'fmb_$i_2' ).
tff(declare_a1662,type,
a1662: $i ).
tff(a1662_definition,axiom,
a1662 = 'fmb_$i_2' ).
tff(declare_a1635,type,
a1635: $i ).
tff(a1635_definition,axiom,
a1635 = 'fmb_$i_2' ).
tff(declare_a1631,type,
a1631: $i ).
tff(a1631_definition,axiom,
a1631 = 'fmb_$i_2' ).
tff(declare_a1618,type,
a1618: $i ).
tff(a1618_definition,axiom,
a1618 = 'fmb_$i_2' ).
tff(declare_a1610,type,
a1610: $i ).
tff(a1610_definition,axiom,
a1610 = 'fmb_$i_2' ).
tff(declare_a1593,type,
a1593: $i ).
tff(a1593_definition,axiom,
a1593 = 'fmb_$i_2' ).
tff(declare_a1587,type,
a1587: $i ).
tff(a1587_definition,axiom,
a1587 = 'fmb_$i_2' ).
tff(declare_a1582,type,
a1582: $i ).
tff(a1582_definition,axiom,
a1582 = 'fmb_$i_2' ).
tff(declare_a1826,type,
a1826: $i ).
tff(a1826_definition,axiom,
a1826 = 'fmb_$i_2' ).
tff(declare_a1822,type,
a1822: $i ).
tff(a1822_definition,axiom,
a1822 = 'fmb_$i_2' ).
tff(declare_a1802,type,
a1802: $i ).
tff(a1802_definition,axiom,
a1802 = 'fmb_$i_2' ).
tff(declare_a1787,type,
a1787: $i ).
tff(a1787_definition,axiom,
a1787 = 'fmb_$i_2' ).
tff(declare_a1771,type,
a1771: $i ).
tff(a1771_definition,axiom,
a1771 = 'fmb_$i_1' ).
tff(declare_a1758,type,
a1758: $i ).
tff(a1758_definition,axiom,
a1758 = 'fmb_$i_2' ).
tff(declare_a1730,type,
a1730: $i ).
tff(a1730_definition,axiom,
a1730 = 'fmb_$i_2' ).
tff(declare_a1723,type,
a1723: $i ).
tff(a1723_definition,axiom,
a1723 = 'fmb_$i_2' ).
tff(declare_a1711,type,
a1711: $i ).
tff(a1711_definition,axiom,
a1711 = 'fmb_$i_2' ).
tff(declare_a1704,type,
a1704: $i ).
tff(a1704_definition,axiom,
a1704 = 'fmb_$i_2' ).
tff(declare_a1695,type,
a1695: $i ).
tff(a1695_definition,axiom,
a1695 = 'fmb_$i_2' ).
tff(declare_a1686,type,
a1686: $i ).
tff(a1686_definition,axiom,
a1686 = 'fmb_$i_2' ).
tff(declare_a1668,type,
a1668: $i ).
tff(a1668_definition,axiom,
a1668 = 'fmb_$i_2' ).
tff(declare_a1661,type,
a1661: $i ).
tff(a1661_definition,axiom,
a1661 = 'fmb_$i_2' ).
tff(declare_a1660,type,
a1660: $i ).
tff(a1660_definition,axiom,
a1660 = 'fmb_$i_2' ).
tff(declare_a1655,type,
a1655: $i ).
tff(a1655_definition,axiom,
a1655 = 'fmb_$i_2' ).
tff(declare_a1650,type,
a1650: $i ).
tff(a1650_definition,axiom,
a1650 = 'fmb_$i_2' ).
tff(declare_a1645,type,
a1645: $i ).
tff(a1645_definition,axiom,
a1645 = 'fmb_$i_2' ).
tff(declare_a1639,type,
a1639: $i ).
tff(a1639_definition,axiom,
a1639 = 'fmb_$i_2' ).
tff(declare_a1626,type,
a1626: $i ).
tff(a1626_definition,axiom,
a1626 = 'fmb_$i_2' ).
tff(declare_a1609,type,
a1609: $i ).
tff(a1609_definition,axiom,
a1609 = 'fmb_$i_2' ).
tff(declare_a1601,type,
a1601: $i ).
tff(a1601_definition,axiom,
a1601 = 'fmb_$i_2' ).
tff(declare_a1597,type,
a1597: $i ).
tff(a1597_definition,axiom,
a1597 = 'fmb_$i_2' ).
tff(declare_a1588,type,
a1588: $i ).
tff(a1588_definition,axiom,
a1588 = 'fmb_$i_2' ).
tff(declare_a1832,type,
a1832: $i ).
tff(a1832_definition,axiom,
a1832 = 'fmb_$i_2' ).
tff(declare_a1829,type,
a1829: $i ).
tff(a1829_definition,axiom,
a1829 = 'fmb_$i_2' ).
tff(declare_a1825,type,
a1825: $i ).
tff(a1825_definition,axiom,
a1825 = 'fmb_$i_2' ).
tff(declare_a1821,type,
a1821: $i ).
tff(a1821_definition,axiom,
a1821 = 'fmb_$i_2' ).
tff(declare_a1819,type,
a1819: $i ).
tff(a1819_definition,axiom,
a1819 = 'fmb_$i_2' ).
tff(declare_a1818,type,
a1818: $i ).
tff(a1818_definition,axiom,
a1818 = 'fmb_$i_2' ).
tff(declare_a1812,type,
a1812: $i ).
tff(a1812_definition,axiom,
a1812 = 'fmb_$i_2' ).
tff(declare_a1808,type,
a1808: $i ).
tff(a1808_definition,axiom,
a1808 = 'fmb_$i_2' ).
tff(declare_a1800,type,
a1800: $i ).
tff(a1800_definition,axiom,
a1800 = 'fmb_$i_2' ).
tff(declare_a1797,type,
a1797: $i ).
tff(a1797_definition,axiom,
a1797 = 'fmb_$i_2' ).
tff(declare_a1796,type,
a1796: $i ).
tff(a1796_definition,axiom,
a1796 = 'fmb_$i_2' ).
tff(declare_a1793,type,
a1793: $i ).
tff(a1793_definition,axiom,
a1793 = 'fmb_$i_2' ).
tff(declare_a1786,type,
a1786: $i ).
tff(a1786_definition,axiom,
a1786 = 'fmb_$i_2' ).
tff(declare_a1784,type,
a1784: $i ).
tff(a1784_definition,axiom,
a1784 = 'fmb_$i_2' ).
tff(declare_a1777,type,
a1777: $i ).
tff(a1777_definition,axiom,
a1777 = 'fmb_$i_2' ).
tff(declare_a1773,type,
a1773: $i ).
tff(a1773_definition,axiom,
a1773 = 'fmb_$i_2' ).
tff(declare_a1764,type,
a1764: $i ).
tff(a1764_definition,axiom,
a1764 = 'fmb_$i_2' ).
tff(declare_a1762,type,
a1762: $i ).
tff(a1762_definition,axiom,
a1762 = 'fmb_$i_2' ).
tff(declare_a1757,type,
a1757: $i ).
tff(a1757_definition,axiom,
a1757 = 'fmb_$i_2' ).
tff(declare_a1754,type,
a1754: $i ).
tff(a1754_definition,axiom,
a1754 = 'fmb_$i_2' ).
tff(declare_a1744,type,
a1744: $i ).
tff(a1744_definition,axiom,
a1744 = 'fmb_$i_2' ).
tff(declare_a1741,type,
a1741: $i ).
tff(a1741_definition,axiom,
a1741 = 'fmb_$i_2' ).
tff(declare_a1737,type,
a1737: $i ).
tff(a1737_definition,axiom,
a1737 = 'fmb_$i_2' ).
tff(declare_a1735,type,
a1735: $i ).
tff(a1735_definition,axiom,
a1735 = 'fmb_$i_2' ).
tff(declare_a1734,type,
a1734: $i ).
tff(a1734_definition,axiom,
a1734 = 'fmb_$i_2' ).
tff(declare_a1713,type,
a1713: $i ).
tff(a1713_definition,axiom,
a1713 = 'fmb_$i_2' ).
tff(declare_a1707,type,
a1707: $i ).
tff(a1707_definition,axiom,
a1707 = 'fmb_$i_2' ).
tff(declare_a1698,type,
a1698: $i ).
tff(a1698_definition,axiom,
a1698 = 'fmb_$i_2' ).
tff(declare_a1693,type,
a1693: $i ).
tff(a1693_definition,axiom,
a1693 = 'fmb_$i_2' ).
tff(declare_a1689,type,
a1689: $i ).
tff(a1689_definition,axiom,
a1689 = 'fmb_$i_2' ).
tff(declare_a1674,type,
a1674: $i ).
tff(a1674_definition,axiom,
a1674 = 'fmb_$i_2' ).
tff(declare_a1673,type,
a1673: $i ).
tff(a1673_definition,axiom,
a1673 = 'fmb_$i_2' ).
tff(declare_a1664,type,
a1664: $i ).
tff(a1664_definition,axiom,
a1664 = 'fmb_$i_2' ).
tff(declare_a1663,type,
a1663: $i ).
tff(a1663_definition,axiom,
a1663 = 'fmb_$i_2' ).
tff(declare_a1648,type,
a1648: $i ).
tff(a1648_definition,axiom,
a1648 = 'fmb_$i_2' ).
tff(declare_a1647,type,
a1647: $i ).
tff(a1647_definition,axiom,
a1647 = 'fmb_$i_2' ).
tff(declare_a1644,type,
a1644: $i ).
tff(a1644_definition,axiom,
a1644 = 'fmb_$i_2' ).
tff(declare_a1638,type,
a1638: $i ).
tff(a1638_definition,axiom,
a1638 = 'fmb_$i_2' ).
tff(declare_a1637,type,
a1637: $i ).
tff(a1637_definition,axiom,
a1637 = 'fmb_$i_2' ).
tff(declare_a1636,type,
a1636: $i ).
tff(a1636_definition,axiom,
a1636 = 'fmb_$i_2' ).
tff(declare_a1633,type,
a1633: $i ).
tff(a1633_definition,axiom,
a1633 = 'fmb_$i_2' ).
tff(declare_a1632,type,
a1632: $i ).
tff(a1632_definition,axiom,
a1632 = 'fmb_$i_2' ).
tff(declare_a1619,type,
a1619: $i ).
tff(a1619_definition,axiom,
a1619 = 'fmb_$i_2' ).
tff(declare_a1613,type,
a1613: $i ).
tff(a1613_definition,axiom,
a1613 = 'fmb_$i_2' ).
tff(declare_a1595,type,
a1595: $i ).
tff(a1595_definition,axiom,
a1595 = 'fmb_$i_2' ).
tff(declare_a1583,type,
a1583: $i ).
tff(a1583_definition,axiom,
a1583 = 'fmb_$i_2' ).
tff(declare_a1827,type,
a1827: $i ).
tff(a1827_definition,axiom,
a1827 = 'fmb_$i_2' ).
tff(declare_a1823,type,
a1823: $i ).
tff(a1823_definition,axiom,
a1823 = 'fmb_$i_2' ).
tff(declare_a1814,type,
a1814: $i ).
tff(a1814_definition,axiom,
a1814 = 'fmb_$i_2' ).
tff(declare_a1813,type,
a1813: $i ).
tff(a1813_definition,axiom,
a1813 = 'fmb_$i_2' ).
tff(declare_a1809,type,
a1809: $i ).
tff(a1809_definition,axiom,
a1809 = 'fmb_$i_2' ).
tff(declare_a1805,type,
a1805: $i ).
tff(a1805_definition,axiom,
a1805 = 'fmb_$i_2' ).
tff(declare_a1804,type,
a1804: $i ).
tff(a1804_definition,axiom,
a1804 = 'fmb_$i_2' ).
tff(declare_a1803,type,
a1803: $i ).
tff(a1803_definition,axiom,
a1803 = 'fmb_$i_2' ).
tff(declare_a1798,type,
a1798: $i ).
tff(a1798_definition,axiom,
a1798 = 'fmb_$i_2' ).
tff(declare_a1789,type,
a1789: $i ).
tff(a1789_definition,axiom,
a1789 = 'fmb_$i_2' ).
tff(declare_a1788,type,
a1788: $i ).
tff(a1788_definition,axiom,
a1788 = 'fmb_$i_2' ).
tff(declare_a1759,type,
a1759: $i ).
tff(a1759_definition,axiom,
a1759 = 'fmb_$i_2' ).
tff(declare_a1750,type,
a1750: $i ).
tff(a1750_definition,axiom,
a1750 = 'fmb_$i_2' ).
tff(declare_a1748,type,
a1748: $i ).
tff(a1748_definition,axiom,
a1748 = 'fmb_$i_2' ).
tff(declare_a1745,type,
a1745: $i ).
tff(a1745_definition,axiom,
a1745 = 'fmb_$i_2' ).
tff(declare_a1739,type,
a1739: $i ).
tff(a1739_definition,axiom,
a1739 = 'fmb_$i_2' ).
tff(declare_a1731,type,
a1731: $i ).
tff(a1731_definition,axiom,
a1731 = 'fmb_$i_2' ).
tff(declare_a1724,type,
a1724: $i ).
tff(a1724_definition,axiom,
a1724 = 'fmb_$i_2' ).
tff(declare_a1718,type,
a1718: $i ).
tff(a1718_definition,axiom,
a1718 = 'fmb_$i_2' ).
tff(declare_a1700,type,
a1700: $i ).
tff(a1700_definition,axiom,
a1700 = 'fmb_$i_2' ).
tff(declare_a1697,type,
a1697: $i ).
tff(a1697_definition,axiom,
a1697 = 'fmb_$i_1' ).
tff(declare_a1696,type,
a1696: $i ).
tff(a1696_definition,axiom,
a1696 = 'fmb_$i_2' ).
tff(declare_a1677,type,
a1677: $i ).
tff(a1677_definition,axiom,
a1677 = 'fmb_$i_2' ).
tff(declare_a1667,type,
a1667: $i ).
tff(a1667_definition,axiom,
a1667 = 'fmb_$i_1' ).
tff(declare_a1656,type,
a1656: $i ).
tff(a1656_definition,axiom,
a1656 = 'fmb_$i_2' ).
tff(declare_a1651,type,
a1651: $i ).
tff(a1651_definition,axiom,
a1651 = 'fmb_$i_2' ).
tff(declare_a1646,type,
a1646: $i ).
tff(a1646_definition,axiom,
a1646 = 'fmb_$i_2' ).
tff(declare_a1641,type,
a1641: $i ).
tff(a1641_definition,axiom,
a1641 = 'fmb_$i_2' ).
tff(declare_a1640,type,
a1640: $i ).
tff(a1640_definition,axiom,
a1640 = 'fmb_$i_2' ).
tff(declare_a1620,type,
a1620: $i ).
tff(a1620_definition,axiom,
a1620 = 'fmb_$i_1' ).
tff(declare_a1616,type,
a1616: $i ).
tff(a1616_definition,axiom,
a1616 = 'fmb_$i_2' ).
tff(declare_a1611,type,
a1611: $i ).
tff(a1611_definition,axiom,
a1611 = 'fmb_$i_1' ).
tff(declare_a1598,type,
a1598: $i ).
tff(a1598_definition,axiom,
a1598 = 'fmb_$i_2' ).
tff(declare_a1590,type,
a1590: $i ).
tff(a1590_definition,axiom,
a1590 = 'fmb_$i_2' ).
tff(declare_a1589,type,
a1589: $i ).
tff(a1589_definition,axiom,
a1589 = 'fmb_$i_2' ).
tff(declare_a1584,type,
a1584: $i ).
tff(a1584_definition,axiom,
a1584 = 'fmb_$i_2' ).
tff(declare_a1775,type,
a1775: $i ).
tff(a1775_definition,axiom,
a1775 = 'fmb_$i_2' ).
tff(declare_a1722,type,
a1722: $i ).
tff(a1722_definition,axiom,
a1722 = 'fmb_$i_2' ).
tff(declare_a1627,type,
a1627: $i ).
tff(a1627_definition,axiom,
a1627 = 'fmb_$i_2' ).
tff(declare_a1623,type,
a1623: $i ).
tff(a1623_definition,axiom,
a1623 = 'fmb_$i_2' ).
tff(declare_a1594,type,
a1594: $i ).
tff(a1594_definition,axiom,
a1594 = 'fmb_$i_2' ).
tff(declare_a1815,type,
a1815: $i ).
tff(a1815_definition,axiom,
a1815 = 'fmb_$i_2' ).
tff(declare_a1799,type,
a1799: $i ).
tff(a1799_definition,axiom,
a1799 = 'fmb_$i_2' ).
tff(declare_a1779,type,
a1779: $i ).
tff(a1779_definition,axiom,
a1779 = 'fmb_$i_2' ).
tff(declare_a1752,type,
a1752: $i ).
tff(a1752_definition,axiom,
a1752 = 'fmb_$i_2' ).
tff(declare_a1746,type,
a1746: $i ).
tff(a1746_definition,axiom,
a1746 = 'fmb_$i_2' ).
tff(declare_a1719,type,
a1719: $i ).
tff(a1719_definition,axiom,
a1719 = 'fmb_$i_2' ).
tff(declare_a1702,type,
a1702: $i ).
tff(a1702_definition,axiom,
a1702 = 'fmb_$i_2' ).
tff(declare_a1701,type,
a1701: $i ).
tff(a1701_definition,axiom,
a1701 = 'fmb_$i_2' ).
tff(declare_a1688,type,
a1688: $i ).
tff(a1688_definition,axiom,
a1688 = 'fmb_$i_2' ).
tff(declare_a1683,type,
a1683: $i ).
tff(a1683_definition,axiom,
a1683 = 'fmb_$i_1' ).
tff(declare_a1681,type,
a1681: $i ).
tff(a1681_definition,axiom,
a1681 = 'fmb_$i_1' ).
tff(declare_a1679,type,
a1679: $i ).
tff(a1679_definition,axiom,
a1679 = 'fmb_$i_2' ).
tff(declare_a1678,type,
a1678: $i ).
tff(a1678_definition,axiom,
a1678 = 'fmb_$i_2' ).
tff(declare_a1652,type,
a1652: $i ).
tff(a1652_definition,axiom,
a1652 = 'fmb_$i_2' ).
tff(declare_a1621,type,
a1621: $i ).
tff(a1621_definition,axiom,
a1621 = 'fmb_$i_1' ).
tff(declare_a1617,type,
a1617: $i ).
tff(a1617_definition,axiom,
a1617 = 'fmb_$i_2' ).
tff(declare_a1612,type,
a1612: $i ).
tff(a1612_definition,axiom,
a1612 = 'fmb_$i_1' ).
tff(declare_a1585,type,
a1585: $i ).
tff(a1585_definition,axiom,
a1585 = 'fmb_$i_2' ).
tff(declare_a1806,type,
a1806: $i ).
tff(a1806_definition,axiom,
a1806 = 'fmb_$i_2' ).
tff(declare_a1705,type,
a1705: $i ).
tff(a1705_definition,axiom,
a1705 = 'fmb_$i_2' ).
tff(declare_a1703,type,
a1703: $i ).
tff(a1703_definition,axiom,
a1703 = 'fmb_$i_2' ).
tff(declare_a1684,type,
a1684: $i ).
tff(a1684_definition,axiom,
a1684 = 'fmb_$i_1' ).
tff(declare_a1680,type,
a1680: $i ).
tff(a1680_definition,axiom,
a1680 = 'fmb_$i_2' ).
tff(declare_a1649,type,
a1649: $i ).
tff(a1649_definition,axiom,
a1649 = 'fmb_$i_2' ).
tff(declare_a1690,type,
a1690: $i ).
tff(a1690_definition,axiom,
a1690 = 'fmb_$i_2' ).
tff(declare_a1769,type,
a1769: $i ).
tff(a1769_definition,axiom,
a1769 = 'fmb_$i_2' ).
tff(declare_a1675,type,
a1675: $i ).
tff(a1675_definition,axiom,
a1675 = 'fmb_$i_2' ).
tff(declare_a1801,type,
a1801: $i ).
tff(a1801_definition,axiom,
a1801 = 'fmb_$i_1' ).
tff(declare_a1710,type,
a1710: $i ).
tff(a1710_definition,axiom,
a1710 = 'fmb_$i_1' ).
tff(declare_a1709,type,
a1709: $i ).
tff(a1709_definition,axiom,
a1709 = 'fmb_$i_2' ).
tff(declare_a1599,type,
a1599: $i ).
tff(a1599_definition,axiom,
a1599 = 'fmb_$i_2' ).
tff(declare_a1676,type,
a1676: $i ).
tff(a1676_definition,axiom,
a1676 = 'fmb_$i_2' ).
tff(declare_a1666,type,
a1666: $i ).
tff(a1666_definition,axiom,
a1666 = 'fmb_$i_2' ).
tff(declare_a1643,type,
a1643: $i ).
tff(a1643_definition,axiom,
a1643 = 'fmb_$i_2' ).
tff(declare_a1624,type,
a1624: $i ).
tff(a1624_definition,axiom,
a1624 = 'fmb_$i_2' ).
tff(declare_a1607,type,
a1607: $i ).
tff(a1607_definition,axiom,
a1607 = 'fmb_$i_2' ).
tff(declare_a1586,type,
a1586: $i ).
tff(a1586_definition,axiom,
a1586 = 'fmb_$i_2' ).
tff(declare_a1794,type,
a1794: $i ).
tff(a1794_definition,axiom,
a1794 = 'fmb_$i_2' ).
tff(declare_a1776,type,
a1776: $i ).
tff(a1776_definition,axiom,
a1776 = 'fmb_$i_2' ).
tff(declare_a1738,type,
a1738: $i ).
tff(a1738_definition,axiom,
a1738 = 'fmb_$i_2' ).
tff(declare_a1726,type,
a1726: $i ).
tff(a1726_definition,axiom,
a1726 = 'fmb_$i_2' ).
tff(declare_a1725,type,
a1725: $i ).
tff(a1725_definition,axiom,
a1725 = 'fmb_$i_2' ).
tff(declare_a1665,type,
a1665: $i ).
tff(a1665_definition,axiom,
a1665 = 'fmb_$i_1' ).
tff(declare_a1628,type,
a1628: $i ).
tff(a1628_definition,axiom,
a1628 = 'fmb_$i_2' ).
tff(declare_a1615,type,
a1615: $i ).
tff(a1615_definition,axiom,
a1615 = 'fmb_$i_2' ).
tff(declare_a1596,type,
a1596: $i ).
tff(a1596_definition,axiom,
a1596 = 'fmb_$i_2' ).
tff(declare_a1783,type,
a1783: $i ).
tff(a1783_definition,axiom,
a1783 = 'fmb_$i_2' ).
tff(declare_a1810,type,
a1810: $i ).
tff(a1810_definition,axiom,
a1810 = 'fmb_$i_2' ).
tff(declare_a1747,type,
a1747: $i ).
tff(a1747_definition,axiom,
a1747 = 'fmb_$i_2' ).
tff(declare_a1727,type,
a1727: $i ).
tff(a1727_definition,axiom,
a1727 = 'fmb_$i_2' ).
tff(declare_a1714,type,
a1714: $i ).
tff(a1714_definition,axiom,
a1714 = 'fmb_$i_2' ).
tff(declare_a1629,type,
a1629: $i ).
tff(a1629_definition,axiom,
a1629 = 'fmb_$i_2' ).
tff(declare_a1742,type,
a1742: $i ).
tff(a1742_definition,axiom,
a1742 = 'fmb_$i_2' ).
tff(declare_a1708,type,
a1708: $i ).
tff(a1708_definition,axiom,
a1708 = 'fmb_$i_2' ).
tff(declare_a1630,type,
a1630: $i ).
tff(a1630_definition,axiom,
a1630 = 'fmb_$i_2' ).
tff(declare_a1614,type,
a1614: $i ).
tff(a1614_definition,axiom,
a1614 = 'fmb_$i_2' ).
tff(declare_a1760,type,
a1760: $i ).
tff(a1760_definition,axiom,
a1760 = 'fmb_$i_2' ).
tff(declare_a1653,type,
a1653: $i ).
tff(a1653_definition,axiom,
a1653 = 'fmb_$i_2' ).
tff(declare_a1768,type,
a1768: $i ).
tff(a1768_definition,axiom,
a1768 = 'fmb_$i_2' ).
tff(declare_a1634,type,
a1634: $i ).
tff(a1634_definition,axiom,
a1634 = 'fmb_$i_2' ).
tff(declare_a1658,type,
a1658: $i ).
tff(a1658_definition,axiom,
a1658 = 'fmb_$i_2' ).
tff(declare_a1763,type,
a1763: $i ).
tff(a1763_definition,axiom,
a1763 = 'fmb_$i_2' ).
tff(declare_a1603,type,
a1603: $i ).
tff(a1603_definition,axiom,
a1603 = 'fmb_$i_2' ).
tff(declare_a1830,type,
a1830: $i ).
tff(a1830_definition,axiom,
a1830 = 'fmb_$i_2' ).
tff(declare_a1749,type,
a1749: $i ).
tff(a1749_definition,axiom,
a1749 = 'fmb_$i_2' ).
tff(declare_a1720,type,
a1720: $i ).
tff(a1720_definition,axiom,
a1720 = 'fmb_$i_2' ).
tff(declare_a1716,type,
a1716: $i ).
tff(a1716_definition,axiom,
a1716 = 'fmb_$i_2' ).
tff(declare_a1606,type,
a1606: $i ).
tff(a1606_definition,axiom,
a1606 = 'fmb_$i_2' ).
tff(declare_a1605,type,
a1605: $i ).
tff(a1605_definition,axiom,
a1605 = 'fmb_$i_2' ).
tff(declare_a1604,type,
a1604: $i ).
tff(a1604_definition,axiom,
a1604 = 'fmb_$i_1' ).
tff(declare_a1600,type,
a1600: $i ).
tff(a1600_definition,axiom,
a1600 = 'fmb_$i_2' ).
tff(declare_a1755,type,
a1755: $i ).
tff(a1755_definition,axiom,
a1755 = 'fmb_$i_2' ).
tff(declare_a1774,type,
a1774: $i ).
tff(a1774_definition,axiom,
a1774 = 'fmb_$i_2' ).
tff(declare_a1728,type,
a1728: $i ).
tff(a1728_definition,axiom,
a1728 = 'fmb_$i_2' ).
tff(declare_a1625,type,
a1625: $i ).
tff(a1625_definition,axiom,
a1625 = 'fmb_$i_2' ).
tff(declare_a1792,type,
a1792: $i ).
tff(a1792_definition,axiom,
a1792 = 'fmb_$i_2' ).
tff(declare_a1691,type,
a1691: $i ).
tff(a1691_definition,axiom,
a1691 = 'fmb_$i_2' ).
tff(declare_a1831,type,
a1831: $i ).
tff(a1831_definition,axiom,
a1831 = 'fmb_$i_2' ).
tff(declare_a1753,type,
a1753: $i ).
tff(a1753_definition,axiom,
a1753 = 'fmb_$i_2' ).
tff(declare_a1602,type,
a1602: $i ).
tff(a1602_definition,axiom,
a1602 = 'fmb_$i_2' ).
tff(declare_a1780,type,
a1780: $i ).
tff(a1780_definition,axiom,
a1780 = 'fmb_$i_1' ).
tff(declare_a1751,type,
a1751: $i ).
tff(a1751_definition,axiom,
a1751 = 'fmb_$i_2' ).
tff(declare_a1732,type,
a1732: $i ).
tff(a1732_definition,axiom,
a1732 = 'fmb_$i_2' ).
tff(declare_a1581,type,
a1581: $i ).
tff(a1581_definition,axiom,
a1581 = 'fmb_$i_2' ).
tff(declare_a1717,type,
a1717: $i ).
tff(a1717_definition,axiom,
a1717 = 'fmb_$i_2' ).
tff(declare_a1654,type,
a1654: $i ).
tff(a1654_definition,axiom,
a1654 = 'fmb_$i_2' ).
tff(declare_a1761,type,
a1761: $i ).
tff(a1761_definition,axiom,
a1761 = 'fmb_$i_2' ).
tff(declare_a1765,type,
a1765: $i ).
tff(a1765_definition,axiom,
a1765 = 'fmb_$i_1' ).
tff(declare_a1772,type,
a1772: $i ).
tff(a1772_definition,axiom,
a1772 = 'fmb_$i_2' ).
tff(declare_a1833,type,
a1833: $i ).
tff(a1833_definition,axiom,
a1833 = 'fmb_$i_2' ).
tff(declare_a1699,type,
a1699: $i ).
tff(a1699_definition,axiom,
a1699 = 'fmb_$i_2' ).
tff(declare_a1715,type,
a1715: $i ).
tff(a1715_definition,axiom,
a1715 = 'fmb_$i_2' ).
tff(declare_a1608,type,
a1608: $i ).
tff(a1608_definition,axiom,
a1608 = 'fmb_$i_2' ).
tff(declare_a1778,type,
a1778: $i ).
tff(a1778_definition,axiom,
a1778 = 'fmb_$i_2' ).
tff(declare_a1682,type,
a1682: $i ).
tff(a1682_definition,axiom,
a1682 = 'fmb_$i_2' ).
tff(declare_a1790,type,
a1790: $i ).
tff(a1790_definition,axiom,
a1790 = 'fmb_$i_2' ).
tff(declare_a1791,type,
a1791: $i ).
tff(a1791_definition,axiom,
a1791 = 'fmb_$i_2' ).
tff(declare_a1781,type,
a1781: $i ).
tff(a1781_definition,axiom,
a1781 = 'fmb_$i_2' ).
tff(declare_a1782,type,
a1782: $i ).
tff(a1782_definition,axiom,
a1782 = 'fmb_$i_2' ).
tff(declare_a1642,type,
a1642: $i ).
tff(a1642_definition,axiom,
a1642 = 'fmb_$i_2' ).
tff(declare_a1657,type,
a1657: $i ).
tff(a1657_definition,axiom,
a1657 = 'fmb_$i_2' ).
tff(declare_a1622,type,
a1622: $i ).
tff(a1622_definition,axiom,
a1622 = 'fmb_$i_2' ).
tff(declare_ndr1_0,type,
ndr1_0: $o ).
tff(ndr1_0_definition,axiom,
ndr1_0 ).
tff(declare_c7_0,type,
c7_0: $o ).
tff(c7_0_definition,axiom,
c7_0 ).
tff(declare_c9_0,type,
c9_0: $o ).
tff(c9_0_definition,axiom,
c9_0 ).
tff(declare_c6_0,type,
c6_0: $o ).
tff(c6_0_definition,axiom,
~ c6_0 ).
tff(declare_c8_0,type,
c8_0: $o ).
tff(c8_0_definition,axiom,
~ c8_0 ).
tff(declare_c2_0,type,
c2_0: $o ).
tff(c2_0_definition,axiom,
c2_0 ).
tff(declare_c3_0,type,
c3_0: $o ).
tff(c3_0_definition,axiom,
c3_0 ).
tff(declare_ssSkC19,type,
ssSkC19: $o ).
tff(ssSkC19_definition,axiom,
~ ssSkC19 ).
tff(declare_c10_0,type,
c10_0: $o ).
tff(c10_0_definition,axiom,
c10_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_ssSkC57,type,
ssSkC57: $o ).
tff(ssSkC57_definition,axiom,
ssSkC57 ).
tff(declare_ssSkC56,type,
ssSkC56: $o ).
tff(ssSkC56_definition,axiom,
~ ssSkC56 ).
tff(declare_ssSkC55,type,
ssSkC55: $o ).
tff(ssSkC55_definition,axiom,
ssSkC55 ).
tff(declare_ssSkC54,type,
ssSkC54: $o ).
tff(ssSkC54_definition,axiom,
ssSkC54 ).
tff(declare_ssSkC52,type,
ssSkC52: $o ).
tff(ssSkC52_definition,axiom,
ssSkC52 ).
tff(declare_ssSkC50,type,
ssSkC50: $o ).
tff(ssSkC50_definition,axiom,
ssSkC50 ).
tff(declare_ssSkC48,type,
ssSkC48: $o ).
tff(ssSkC48_definition,axiom,
ssSkC48 ).
tff(declare_ssSkC43,type,
ssSkC43: $o ).
tff(ssSkC43_definition,axiom,
ssSkC43 ).
tff(declare_ssSkC39,type,
ssSkC39: $o ).
tff(ssSkC39_definition,axiom,
~ ssSkC39 ).
tff(declare_ssSkC38,type,
ssSkC38: $o ).
tff(ssSkC38_definition,axiom,
ssSkC38 ).
tff(declare_ssSkC37,type,
ssSkC37: $o ).
tff(ssSkC37_definition,axiom,
ssSkC37 ).
tff(declare_ssSkC36,type,
ssSkC36: $o ).
tff(ssSkC36_definition,axiom,
ssSkC36 ).
tff(declare_ssSkC35,type,
ssSkC35: $o ).
tff(ssSkC35_definition,axiom,
ssSkC35 ).
tff(declare_ssSkC33,type,
ssSkC33: $o ).
tff(ssSkC33_definition,axiom,
ssSkC33 ).
tff(declare_ssSkC30,type,
ssSkC30: $o ).
tff(ssSkC30_definition,axiom,
ssSkC30 ).
tff(declare_ssSkC27,type,
ssSkC27: $o ).
tff(ssSkC27_definition,axiom,
ssSkC27 ).
tff(declare_ssSkC25,type,
ssSkC25: $o ).
tff(ssSkC25_definition,axiom,
ssSkC25 ).
tff(declare_ssSkC24,type,
ssSkC24: $o ).
tff(ssSkC24_definition,axiom,
ssSkC24 ).
tff(declare_ssSkC22,type,
ssSkC22: $o ).
tff(ssSkC22_definition,axiom,
ssSkC22 ).
tff(declare_ssSkC20,type,
ssSkC20: $o ).
tff(ssSkC20_definition,axiom,
ssSkC20 ).
tff(declare_ssSkC14,type,
ssSkC14: $o ).
tff(ssSkC14_definition,axiom,
ssSkC14 ).
tff(declare_ssSkC13,type,
ssSkC13: $o ).
tff(ssSkC13_definition,axiom,
ssSkC13 ).
tff(declare_ssSkC10,type,
ssSkC10: $o ).
tff(ssSkC10_definition,axiom,
ssSkC10 ).
tff(declare_ssSkC9,type,
ssSkC9: $o ).
tff(ssSkC9_definition,axiom,
ssSkC9 ).
tff(declare_ssSkC3,type,
ssSkC3: $o ).
tff(ssSkC3_definition,axiom,
ssSkC3 ).
tff(declare_ssSkC2,type,
ssSkC2: $o ).
tff(ssSkC2_definition,axiom,
ssSkC2 ).
tff(declare_ssSkC0,type,
ssSkC0: $o ).
tff(ssSkC0_definition,axiom,
ssSkC0 ).
tff(declare_ssSkC51,type,
ssSkC51: $o ).
tff(ssSkC51_definition,axiom,
~ ssSkC51 ).
tff(declare_ssSkC47,type,
ssSkC47: $o ).
tff(ssSkC47_definition,axiom,
~ ssSkC47 ).
tff(declare_ssSkC34,type,
ssSkC34: $o ).
tff(ssSkC34_definition,axiom,
~ ssSkC34 ).
tff(declare_ssSkC32,type,
ssSkC32: $o ).
tff(ssSkC32_definition,axiom,
~ ssSkC32 ).
tff(declare_ssSkC28,type,
ssSkC28: $o ).
tff(ssSkC28_definition,axiom,
ssSkC28 ).
tff(declare_ssSkC29,type,
ssSkC29: $o ).
tff(ssSkC29_definition,axiom,
~ ssSkC29 ).
tff(declare_c1_0,type,
c1_0: $o ).
tff(c1_0_definition,axiom,
c1_0 ).
tff(declare_ssSkC17,type,
ssSkC17: $o ).
tff(ssSkC17_definition,axiom,
ssSkC17 ).
tff(declare_ssSkC18,type,
ssSkC18: $o ).
tff(ssSkC18_definition,axiom,
~ ssSkC18 ).
tff(declare_ssSkC15,type,
ssSkC15: $o ).
tff(ssSkC15_definition,axiom,
~ ssSkC15 ).
tff(declare_ssSkC16,type,
ssSkC16: $o ).
tff(ssSkC16_definition,axiom,
ssSkC16 ).
tff(declare_ssSkC11,type,
ssSkC11: $o ).
tff(ssSkC11_definition,axiom,
~ ssSkC11 ).
tff(declare_ssSkC12,type,
ssSkC12: $o ).
tff(ssSkC12_definition,axiom,
ssSkC12 ).
tff(declare_ssSkC7,type,
ssSkC7: $o ).
tff(ssSkC7_definition,axiom,
ssSkC7 ).
tff(declare_ssSkC8,type,
ssSkC8: $o ).
tff(ssSkC8_definition,axiom,
~ ssSkC8 ).
tff(declare_ssSkC4,type,
ssSkC4: $o ).
tff(ssSkC4_definition,axiom,
ssSkC4 ).
tff(declare_ssSkC5,type,
ssSkC5: $o ).
tff(ssSkC5_definition,axiom,
~ ssSkC5 ).
tff(declare_ssSkC1,type,
ssSkC1: $o ).
tff(ssSkC1_definition,axiom,
~ ssSkC1 ).
tff(declare_ssSkC26,type,
ssSkC26: $o ).
tff(ssSkC26_definition,axiom,
ssSkC26 ).
tff(declare_ssSkC53,type,
ssSkC53: $o ).
tff(ssSkC53_definition,axiom,
~ ssSkC53 ).
tff(declare_ssSkC41,type,
ssSkC41: $o ).
tff(ssSkC41_definition,axiom,
~ ssSkC41 ).
tff(declare_ssSkC40,type,
ssSkC40: $o ).
tff(ssSkC40_definition,axiom,
~ ssSkC40 ).
tff(declare_ssSkC23,type,
ssSkC23: $o ).
tff(ssSkC23_definition,axiom,
~ ssSkC23 ).
tff(declare_ssSkC21,type,
ssSkC21: $o ).
tff(ssSkC21_definition,axiom,
ssSkC21 ).
tff(declare_ssSkC49,type,
ssSkC49: $o ).
tff(ssSkC49_definition,axiom,
~ ssSkC49 ).
tff(declare_ssSkC45,type,
ssSkC45: $o ).
tff(ssSkC45_definition,axiom,
~ ssSkC45 ).
tff(declare_ssSkC46,type,
ssSkC46: $o ).
tff(ssSkC46_definition,axiom,
~ ssSkC46 ).
tff(declare_ssSkC44,type,
ssSkC44: $o ).
tff(ssSkC44_definition,axiom,
ssSkC44 ).
tff(declare_ssSkC6,type,
ssSkC6: $o ).
tff(ssSkC6_definition,axiom,
~ ssSkC6 ).
tff(declare_ssSkC42,type,
ssSkC42: $o ).
tff(ssSkC42_definition,axiom,
ssSkC42 ).
tff(declare_ssSkC58,type,
ssSkC58: $o ).
tff(ssSkC58_definition,axiom,
ssSkC58 ).
tff(declare_ssSkC31,type,
ssSkC31: $o ).
tff(ssSkC31_definition,axiom,
~ ssSkC31 ).
tff(declare_ndr1_1,type,
ndr1_1: $i > $o ).
tff(predicate_ndr1_1,axiom,
( ndr1_1('fmb_$i_1')
& ndr1_1('fmb_$i_2') ) ).
tff(declare_c7_1,type,
c7_1: $i > $o ).
tff(predicate_c7_1,axiom,
( ~ c7_1('fmb_$i_1')
& ~ c7_1('fmb_$i_2') ) ).
tff(declare_c5_1,type,
c5_1: $i > $o ).
tff(predicate_c5_1,axiom,
( ~ c5_1('fmb_$i_1')
& ~ c5_1('fmb_$i_2') ) ).
tff(declare_ssSkP16,type,
ssSkP16: $i > $o ).
tff(predicate_ssSkP16,axiom,
( ssSkP16('fmb_$i_1')
& ssSkP16('fmb_$i_2') ) ).
tff(declare_ssSkP15,type,
ssSkP15: $i > $o ).
tff(predicate_ssSkP15,axiom,
( ssSkP15('fmb_$i_1')
& ssSkP15('fmb_$i_2') ) ).
tff(declare_c8_1,type,
c8_1: $i > $o ).
tff(predicate_c8_1,axiom,
( c8_1('fmb_$i_1')
& c8_1('fmb_$i_2') ) ).
tff(declare_c10_1,type,
c10_1: $i > $o ).
tff(predicate_c10_1,axiom,
( c10_1('fmb_$i_1')
& ~ c10_1('fmb_$i_2') ) ).
tff(declare_c3_1,type,
c3_1: $i > $o ).
tff(predicate_c3_1,axiom,
( c3_1('fmb_$i_1')
& ~ c3_1('fmb_$i_2') ) ).
tff(declare_c9_1,type,
c9_1: $i > $o ).
tff(predicate_c9_1,axiom,
( ~ c9_1('fmb_$i_1')
& ~ c9_1('fmb_$i_2') ) ).
tff(declare_ssSkP14,type,
ssSkP14: $i > $o ).
tff(predicate_ssSkP14,axiom,
( ~ ssSkP14('fmb_$i_1')
& ssSkP14('fmb_$i_2') ) ).
tff(declare_ssSkP13,type,
ssSkP13: $i > $o ).
tff(predicate_ssSkP13,axiom,
( ssSkP13('fmb_$i_1')
& ssSkP13('fmb_$i_2') ) ).
tff(declare_ssSkP12,type,
ssSkP12: $i > $o ).
tff(predicate_ssSkP12,axiom,
( ssSkP12('fmb_$i_1')
& ssSkP12('fmb_$i_2') ) ).
tff(declare_ssSkP11,type,
ssSkP11: $i > $o ).
tff(predicate_ssSkP11,axiom,
( ssSkP11('fmb_$i_1')
& ssSkP11('fmb_$i_2') ) ).
tff(declare_ssSkP10,type,
ssSkP10: $i > $o ).
tff(predicate_ssSkP10,axiom,
( ssSkP10('fmb_$i_1')
& ssSkP10('fmb_$i_2') ) ).
tff(declare_ssSkP9,type,
ssSkP9: $i > $o ).
tff(predicate_ssSkP9,axiom,
( ssSkP9('fmb_$i_1')
& ssSkP9('fmb_$i_2') ) ).
tff(declare_ssSkP8,type,
ssSkP8: $i > $o ).
tff(predicate_ssSkP8,axiom,
( ssSkP8('fmb_$i_1')
& ssSkP8('fmb_$i_2') ) ).
tff(declare_c4_1,type,
c4_1: $i > $o ).
tff(predicate_c4_1,axiom,
( c4_1('fmb_$i_1')
& ~ c4_1('fmb_$i_2') ) ).
tff(declare_c2_1,type,
c2_1: $i > $o ).
tff(predicate_c2_1,axiom,
( ~ c2_1('fmb_$i_1')
& ~ c2_1('fmb_$i_2') ) ).
tff(declare_ssSkP7,type,
ssSkP7: $i > $o ).
tff(predicate_ssSkP7,axiom,
( ssSkP7('fmb_$i_1')
& ssSkP7('fmb_$i_2') ) ).
tff(declare_ssSkP6,type,
ssSkP6: $i > $o ).
tff(predicate_ssSkP6,axiom,
( ~ ssSkP6('fmb_$i_1')
& ssSkP6('fmb_$i_2') ) ).
tff(declare_c6_1,type,
c6_1: $i > $o ).
tff(predicate_c6_1,axiom,
( c6_1('fmb_$i_1')
& ~ c6_1('fmb_$i_2') ) ).
tff(declare_ssSkP5,type,
ssSkP5: $i > $o ).
tff(predicate_ssSkP5,axiom,
( ssSkP5('fmb_$i_1')
& ssSkP5('fmb_$i_2') ) ).
tff(declare_ssSkP4,type,
ssSkP4: $i > $o ).
tff(predicate_ssSkP4,axiom,
( ssSkP4('fmb_$i_1')
& ~ ssSkP4('fmb_$i_2') ) ).
tff(declare_ssSkP3,type,
ssSkP3: $i > $o ).
tff(predicate_ssSkP3,axiom,
( ssSkP3('fmb_$i_1')
& ssSkP3('fmb_$i_2') ) ).
tff(declare_ssSkP2,type,
ssSkP2: $i > $o ).
tff(predicate_ssSkP2,axiom,
( ssSkP2('fmb_$i_1')
& ssSkP2('fmb_$i_2') ) ).
tff(declare_ssSkP1,type,
ssSkP1: $i > $o ).
tff(predicate_ssSkP1,axiom,
( ssSkP1('fmb_$i_1')
& ssSkP1('fmb_$i_2') ) ).
tff(declare_ssSkP0,type,
ssSkP0: $i > $o ).
tff(predicate_ssSkP0,axiom,
( ssSkP0('fmb_$i_1')
& ssSkP0('fmb_$i_2') ) ).
tff(declare_c1_1,type,
c1_1: $i > $o ).
tff(predicate_c1_1,axiom,
( ~ c1_1('fmb_$i_1')
& ~ c1_1('fmb_$i_2') ) ).
tff(declare_c9_2,type,
c9_2: ( $i * $i ) > $o ).
tff(predicate_c9_2,axiom,
( c9_2('fmb_$i_1','fmb_$i_1')
& c9_2('fmb_$i_1','fmb_$i_2')
& ~ c9_2('fmb_$i_2','fmb_$i_1')
& ~ c9_2('fmb_$i_2','fmb_$i_2') ) ).
tff(declare_c8_2,type,
c8_2: ( $i * $i ) > $o ).
tff(predicate_c8_2,axiom,
( ~ c8_2('fmb_$i_1','fmb_$i_1')
& c8_2('fmb_$i_1','fmb_$i_2')
& c8_2('fmb_$i_2','fmb_$i_1')
& c8_2('fmb_$i_2','fmb_$i_2') ) ).
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_2','fmb_$i_1')
& ~ c4_2('fmb_$i_2','fmb_$i_2') ) ).
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_2','fmb_$i_1')
& c5_2('fmb_$i_2','fmb_$i_2') ) ).
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_2','fmb_$i_1')
& c3_2('fmb_$i_2','fmb_$i_2') ) ).
tff(declare_c7_2,type,
c7_2: ( $i * $i ) > $o ).
tff(predicate_c7_2,axiom,
( c7_2('fmb_$i_1','fmb_$i_1')
& c7_2('fmb_$i_1','fmb_$i_2')
& c7_2('fmb_$i_2','fmb_$i_1')
& ~ c7_2('fmb_$i_2','fmb_$i_2') ) ).
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_2','fmb_$i_1')
& ~ c1_2('fmb_$i_2','fmb_$i_2') ) ).
tff(declare_c6_2,type,
c6_2: ( $i * $i ) > $o ).
tff(predicate_c6_2,axiom,
( ~ c6_2('fmb_$i_1','fmb_$i_1')
& ~ c6_2('fmb_$i_1','fmb_$i_2')
& c6_2('fmb_$i_2','fmb_$i_1')
& ~ c6_2('fmb_$i_2','fmb_$i_2') ) ).
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_2','fmb_$i_1')
& c2_2('fmb_$i_2','fmb_$i_2') ) ).
tff(declare_c10_2,type,
c10_2: ( $i * $i ) > $o ).
tff(predicate_c10_2,axiom,
( c10_2('fmb_$i_1','fmb_$i_1')
& ~ c10_2('fmb_$i_1','fmb_$i_2')
& ~ c10_2('fmb_$i_2','fmb_$i_1')
& c10_2('fmb_$i_2','fmb_$i_2') ) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SYN427-1 : TPTP v9.3.1. Released v2.1.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.11/0.17 % Computer : n014.cluster.edu
% 0.11/0.17 % Model : x86_64 x86_64
% 0.11/0.17 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.17 % Memory : 8046.5625MB
% 0.11/0.17 % OS : Linux 6.8.0-71-generic
% 0.11/0.17 % CPULimit : 300
% 0.11/0.17 % WCLimit : 300
% 0.11/0.17 % DateTime : Mon Sep 28 15:55:45 UTC 2026
% 0.11/0.18 % CPUTime :
% 0.11/0.18 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.11/0.21 Running first-order model finding
% 0.11/0.21 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.53/0.33 % (1894646)Will run a generic schedule for satisfiability detection.
% 0.53/0.33 % (1894655)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2369059429:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 0.53/0.33 % (1894652)% WARNING: option uhcvi not known.
% 0.53/0.33 % (1894651)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=146392291_2999 on theBenchmark for (2999ds/0Mi)
% 0.53/0.33 % (1894653)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3579568419:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 0.53/0.33 % (1894654)dis+10_1_sil=32000:sp=arity:random_seed=912200129:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 0.53/0.33 % (1894652)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=6349338:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 0.53/0.33 % (1894656)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2192980348:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 0.53/0.33 % (1894657)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=4245488263:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 0.53/0.33 % (1894655)Instruction limit reached!
% 0.53/0.33 % (1894655)------------------------------
% 0.53/0.33 % (1894655)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.53/0.33 % (1894655)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.53/0.33 % (1894655)CaDiCaL version: 2.1.3
% 0.53/0.33 % (1894655)Termination reason: Instruction limit
% 0.53/0.33 % (1894655)Termination phase: Saturation
% 0.53/0.33 % (1894655)Time elapsed: 0.036 s
% 0.53/0.33 % (1894655)Peak memory usage: 15 MB
% 0.53/0.33 % (1894655)Instructions burned: 117 (million)
% 0.53/0.33 % Detected minimum model sizes of [1]
% 0.53/0.33 % Detected maximum model sizes of [244]
% 0.53/0.33 % TRYING [1]
% 0.53/0.33 % TRYING [2]
% 0.53/0.33 % (1894665)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=1049552125:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 0.53/0.33 % Finite Model Found!
% 0.53/0.33 % SZS status Satisfiable for theBenchmark
% 0.53/0.33 % (1894651) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-1894646-1894651"...
% 0.53/0.33 % (1894651)...printing done.
% 0.53/0.33 % SZS output start FiniteModel for theBenchmark
% See solution above
% 0.53/0.33 % (1894651)------------------------------
% 0.53/0.33 % (1894651)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.53/0.33 % (1894651)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.53/0.33 % (1894651)CaDiCaL version: 2.1.3
% 0.53/0.33 % (1894651)Termination reason: Satisfiable
% 0.53/0.33 % (1894651)Time elapsed: 0.049 s
% 0.53/0.33 % (1894651)Peak memory usage: 14 MB
% 0.53/0.33 % (1894651)Instructions burned: 100 (million)
% 0.53/0.33 % (1894646)Success in time 0.11 s
% 0.53/0.33 % Vampire exiting
%------------------------------------------------------------------------------