%------------------------------------------------------------------------------ % File : Crossbow---0.1 % Problem : SYN427+1 : TPTP v8.1.0. Released v2.1.0. % Transfm : none % Format : tptp:raw % Command : do_Crossbow---0.1 %s % Computer : n012.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 600s % DateTime : Thu Jul 21 03:02:14 EDT 2022 % Result : CounterSatisfiable 5.66s 5.89s % Output : FiniteModel 5.66s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : SYN427+1 : TPTP v8.1.0. Released v2.1.0. % 0.07/0.13 % Command : do_Crossbow---0.1 %s % 0.13/0.34 % Computer : n012.cluster.edu % 0.13/0.34 % Model : x86_64 x86_64 % 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.34 % Memory : 8042.1875MB % 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.34 % CPULimit : 300 % 0.13/0.34 % WCLimit : 600 % 0.13/0.34 % DateTime : Mon Jul 11 22:00:13 EDT 2022 % 0.13/0.34 % CPUTime : % 0.13/0.34 /export/starexec/sandbox2/solver/bin % 0.13/0.35 crossbow.opt % 0.13/0.35 do_Crossbow---0.1 % 0.13/0.35 eprover % 0.13/0.35 runsolver % 0.13/0.35 starexec_run_Crossbow---0.1 % 5.66/5.89 % SZS status CounterSatisfiable for theBenchmark.p % 5.66/5.89 % SZS output start FiniteModel for theBenchmark.p % 5.66/5.89 % domain size: 2 % 5.66/5.89 fof(interp, fi_domain, ![X] : (X = 0 | X = 1)). % 5.66/5.89 fof(interp, fi_functors, a1581 = 0). % 5.66/5.89 fof(interp, fi_functors, a1582 = 0). % 5.66/5.89 fof(interp, fi_functors, a1583 = 0). % 5.66/5.89 fof(interp, fi_functors, a1584 = 0). % 5.66/5.89 fof(interp, fi_functors, a1585 = 0). % 5.66/5.89 fof(interp, fi_functors, a1586 = 0). % 5.66/5.89 fof(interp, fi_functors, a1587 = 0). % 5.66/5.89 fof(interp, fi_functors, a1588 = 1). % 5.66/5.89 fof(interp, fi_functors, a1589 = 1). % 5.66/5.89 fof(interp, fi_functors, a1590 = 0). % 5.66/5.89 fof(interp, fi_functors, a1591 = 0). % 5.66/5.89 fof(interp, fi_functors, a1592 = 0). % 5.66/5.89 fof(interp, fi_functors, a1593 = 0). % 5.66/5.89 fof(interp, fi_functors, a1594 = 1). % 5.66/5.89 fof(interp, fi_functors, a1595 = 1). % 5.66/5.89 fof(interp, fi_functors, a1596 = 0). % 5.66/5.89 fof(interp, fi_functors, a1597 = 0). % 5.66/5.89 fof(interp, fi_functors, a1598 = 0). % 5.66/5.89 fof(interp, fi_functors, a1599 = 1). % 5.66/5.89 fof(interp, fi_functors, a1600 = 1). % 5.66/5.89 fof(interp, fi_functors, a1601 = 0). % 5.66/5.89 fof(interp, fi_functors, a1602 = 1). % 5.66/5.89 fof(interp, fi_functors, a1603 = 0). % 5.66/5.89 fof(interp, fi_functors, a1604 = 0). % 5.66/5.89 fof(interp, fi_functors, a1605 = 1). % 5.66/5.89 fof(interp, fi_functors, a1606 = 0). % 5.66/5.89 fof(interp, fi_functors, a1607 = 0). % 5.66/5.89 fof(interp, fi_functors, a1608 = 0). % 5.66/5.89 fof(interp, fi_functors, a1609 = 1). % 5.66/5.89 fof(interp, fi_functors, a1610 = 0). % 5.66/5.89 fof(interp, fi_functors, a1611 = 0). % 5.66/5.89 fof(interp, fi_functors, a1612 = 1). % 5.66/5.89 fof(interp, fi_functors, a1613 = 0). % 5.66/5.89 fof(interp, fi_functors, a1614 = 0). % 5.66/5.89 fof(interp, fi_functors, a1615 = 0). % 5.66/5.89 fof(interp, fi_functors, a1616 = 0). % 5.66/5.89 fof(interp, fi_functors, a1617 = 0). % 5.66/5.89 fof(interp, fi_functors, a1618 = 1). % 5.66/5.89 fof(interp, fi_functors, a1619 = 1). % 5.66/5.89 fof(interp, fi_functors, a1620 = 0). % 5.66/5.89 fof(interp, fi_functors, a1621 = 1). % 5.66/5.89 fof(interp, fi_functors, a1622 = 0). % 5.66/5.89 fof(interp, fi_functors, a1623 = 1). % 5.66/5.89 fof(interp, fi_functors, a1624 = 1). % 5.66/5.89 fof(interp, fi_functors, a1625 = 0). % 5.66/5.89 fof(interp, fi_functors, a1626 = 0). % 5.66/5.89 fof(interp, fi_functors, a1627 = 0). % 5.66/5.89 fof(interp, fi_functors, a1628 = 0). % 5.66/5.89 fof(interp, fi_functors, a1629 = 1). % 5.66/5.89 fof(interp, fi_functors, a1630 = 1). % 5.66/5.89 fof(interp, fi_functors, a1631 = 0). % 5.66/5.89 fof(interp, fi_functors, a1632 = 1). % 5.66/5.89 fof(interp, fi_functors, a1633 = 0). % 5.66/5.89 fof(interp, fi_functors, a1634 = 0). % 5.66/5.89 fof(interp, fi_functors, a1635 = 0). % 5.66/5.89 fof(interp, fi_functors, a1636 = 0). % 5.66/5.89 fof(interp, fi_functors, a1637 = 0). % 5.66/5.89 fof(interp, fi_functors, a1638 = 0). % 5.66/5.89 fof(interp, fi_functors, a1639 = 0). % 5.66/5.89 fof(interp, fi_functors, a1640 = 0). % 5.66/5.89 fof(interp, fi_functors, a1641 = 0). % 5.66/5.89 fof(interp, fi_functors, a1642 = 0). % 5.66/5.89 fof(interp, fi_functors, a1643 = 1). % 5.66/5.89 fof(interp, fi_functors, a1644 = 1). % 5.66/5.89 fof(interp, fi_functors, a1645 = 0). % 5.66/5.89 fof(interp, fi_functors, a1646 = 1). % 5.66/5.89 fof(interp, fi_functors, a1647 = 1). % 5.66/5.89 fof(interp, fi_functors, a1648 = 0). % 5.66/5.89 fof(interp, fi_functors, a1649 = 0). % 5.66/5.89 fof(interp, fi_functors, a1650 = 0). % 5.66/5.89 fof(interp, fi_functors, a1651 = 0). % 5.66/5.89 fof(interp, fi_functors, a1652 = 0). % 5.66/5.89 fof(interp, fi_functors, a1653 = 1). % 5.66/5.89 fof(interp, fi_functors, a1654 = 0). % 5.66/5.89 fof(interp, fi_functors, a1655 = 1). % 5.66/5.89 fof(interp, fi_functors, a1656 = 1). % 5.66/5.89 fof(interp, fi_functors, a1657 = 0). % 5.66/5.89 fof(interp, fi_functors, a1658 = 1). % 5.66/5.89 fof(interp, fi_functors, a1659 = 1). % 5.66/5.89 fof(interp, fi_functors, a1660 = 1). % 5.66/5.89 fof(interp, fi_functors, a1661 = 1). % 5.66/5.89 fof(interp, fi_functors, a1662 = 1). % 5.66/5.89 fof(interp, fi_functors, a1663 = 1). % 5.66/5.89 fof(interp, fi_functors, a1664 = 0). % 5.66/5.89 fof(interp, fi_functors, a1665 = 0). % 5.66/5.89 fof(interp, fi_functors, a1666 = 0). % 5.66/5.89 fof(interp, fi_functors, a1667 = 1). % 5.66/5.89 fof(interp, fi_functors, a1668 = 1). % 5.66/5.89 fof(interp, fi_functors, a1669 = 0). % 5.66/5.89 fof(interp, fi_functors, a1670 = 0). % 5.66/5.89 fof(interp, fi_functors, a1671 = 0). % 5.66/5.89 fof(interp, fi_functors, a1672 = 0). % 5.66/5.89 fof(interp, fi_functors, a1673 = 0). % 5.66/5.89 fof(interp, fi_functors, a1674 = 0). % 5.66/5.89 fof(interp, fi_functors, a1675 = 0). % 5.66/5.89 fof(interp, fi_functors, a1676 = 0). % 5.66/5.89 fof(interp, fi_functors, a1677 = 0). % 5.66/5.89 fof(interp, fi_functors, a1678 = 0). % 5.66/5.89 fof(interp, fi_functors, a1679 = 1). % 5.66/5.89 fof(interp, fi_functors, a1680 = 1). % 5.66/5.89 fof(interp, fi_functors, a1681 = 0). % 5.66/5.89 fof(interp, fi_functors, a1682 = 1). % 5.66/5.89 fof(interp, fi_functors, a1683 = 1). % 5.66/5.89 fof(interp, fi_functors, a1684 = 1). % 5.66/5.89 fof(interp, fi_functors, a1685 = 0). % 5.66/5.89 fof(interp, fi_functors, a1686 = 0). % 5.66/5.89 fof(interp, fi_functors, a1687 = 0). % 5.66/5.89 fof(interp, fi_functors, a1688 = 1). % 5.66/5.89 fof(interp, fi_functors, a1689 = 0). % 5.66/5.89 fof(interp, fi_functors, a1690 = 0). % 5.66/5.89 fof(interp, fi_functors, a1691 = 0). % 5.66/5.89 fof(interp, fi_functors, a1692 = 1). % 5.66/5.89 fof(interp, fi_functors, a1693 = 1). % 5.66/5.89 fof(interp, fi_functors, a1694 = 0). % 5.66/5.89 fof(interp, fi_functors, a1695 = 0). % 5.66/5.89 fof(interp, fi_functors, a1696 = 0). % 5.66/5.89 fof(interp, fi_functors, a1697 = 0). % 5.66/5.89 fof(interp, fi_functors, a1698 = 1). % 5.66/5.89 fof(interp, fi_functors, a1699 = 0). % 5.66/5.89 fof(interp, fi_functors, a1700 = 1). % 5.66/5.89 fof(interp, fi_functors, a1701 = 0). % 5.66/5.89 fof(interp, fi_functors, a1702 = 0). % 5.66/5.89 fof(interp, fi_functors, a1703 = 1). % 5.66/5.89 fof(interp, fi_functors, a1704 = 1). % 5.66/5.89 fof(interp, fi_functors, a1705 = 1). % 5.66/5.89 fof(interp, fi_functors, a1706 = 1). % 5.66/5.89 fof(interp, fi_functors, a1707 = 1). % 5.66/5.89 fof(interp, fi_functors, a1708 = 0). % 5.66/5.89 fof(interp, fi_functors, a1709 = 0). % 5.66/5.89 fof(interp, fi_functors, a1710 = 0). % 5.66/5.89 fof(interp, fi_functors, a1711 = 0). % 5.66/5.89 fof(interp, fi_functors, a1712 = 0). % 5.66/5.89 fof(interp, fi_functors, a1713 = 0). % 5.66/5.89 fof(interp, fi_functors, a1714 = 0). % 5.66/5.89 fof(interp, fi_functors, a1715 = 0). % 5.66/5.89 fof(interp, fi_functors, a1716 = 0). % 5.66/5.89 fof(interp, fi_functors, a1717 = 0). % 5.66/5.89 fof(interp, fi_functors, a1718 = 0). % 5.66/5.89 fof(interp, fi_functors, a1719 = 1). % 5.66/5.89 fof(interp, fi_functors, a1720 = 0). % 5.66/5.89 fof(interp, fi_functors, a1721 = 1). % 5.66/5.89 fof(interp, fi_functors, a1722 = 1). % 5.66/5.89 fof(interp, fi_functors, a1723 = 0). % 5.66/5.89 fof(interp, fi_functors, a1724 = 1). % 5.66/5.89 fof(interp, fi_functors, a1725 = 0). % 5.66/5.89 fof(interp, fi_functors, a1726 = 1). % 5.66/5.89 fof(interp, fi_functors, a1727 = 1). % 5.66/5.89 fof(interp, fi_functors, a1728 = 0). % 5.66/5.89 fof(interp, fi_functors, a1729 = 1). % 5.66/5.89 fof(interp, fi_functors, a1730 = 0). % 5.66/5.89 fof(interp, fi_functors, a1731 = 0). % 5.66/5.89 fof(interp, fi_functors, a1732 = 0). % 5.66/5.89 fof(interp, fi_functors, a1733 = 1). % 5.66/5.89 fof(interp, fi_functors, a1734 = 0). % 5.66/5.89 fof(interp, fi_functors, a1735 = 1). % 5.66/5.89 fof(interp, fi_functors, a1736 = 1). % 5.66/5.89 fof(interp, fi_functors, a1737 = 0). % 5.66/5.89 fof(interp, fi_functors, a1738 = 1). % 5.66/5.89 fof(interp, fi_functors, a1739 = 0). % 5.66/5.89 fof(interp, fi_functors, a1740 = 0). % 5.66/5.89 fof(interp, fi_functors, a1741 = 1). % 5.66/5.89 fof(interp, fi_functors, a1742 = 0). % 5.66/5.89 fof(interp, fi_functors, a1743 = 0). % 5.66/5.89 fof(interp, fi_functors, a1744 = 0). % 5.66/5.89 fof(interp, fi_functors, a1745 = 1). % 5.66/5.89 fof(interp, fi_functors, a1746 = 0). % 5.66/5.89 fof(interp, fi_functors, a1747 = 1). % 5.66/5.89 fof(interp, fi_functors, a1748 = 1). % 5.66/5.89 fof(interp, fi_functors, a1749 = 0). % 5.66/5.89 fof(interp, fi_functors, a1750 = 0). % 5.66/5.89 fof(interp, fi_functors, a1751 = 1). % 5.66/5.89 fof(interp, fi_functors, a1752 = 0). % 5.66/5.89 fof(interp, fi_functors, a1753 = 0). % 5.66/5.89 fof(interp, fi_functors, a1754 = 0). % 5.66/5.89 fof(interp, fi_functors, a1755 = 0). % 5.66/5.89 fof(interp, fi_functors, a1756 = 0). % 5.66/5.89 fof(interp, fi_functors, a1757 = 0). % 5.66/5.89 fof(interp, fi_functors, a1758 = 0). % 5.66/5.89 fof(interp, fi_functors, a1759 = 0). % 5.66/5.89 fof(interp, fi_functors, a1760 = 0). % 5.66/5.89 fof(interp, fi_functors, a1761 = 0). % 5.66/5.89 fof(interp, fi_functors, a1762 = 0). % 5.66/5.89 fof(interp, fi_functors, a1763 = 0). % 5.66/5.89 fof(interp, fi_functors, a1764 = 1). % 5.66/5.89 fof(interp, fi_functors, a1765 = 0). % 5.66/5.89 fof(interp, fi_functors, a1766 = 0). % 5.66/5.89 fof(interp, fi_functors, a1767 = 0). % 5.66/5.89 fof(interp, fi_functors, a1768 = 0). % 5.66/5.89 fof(interp, fi_functors, a1769 = 0). % 5.66/5.89 fof(interp, fi_functors, a1770 = 0). % 5.66/5.89 fof(interp, fi_functors, a1771 = 0). % 5.66/5.89 fof(interp, fi_functors, a1772 = 0). % 5.66/5.89 fof(interp, fi_functors, a1773 = 1). % 5.66/5.89 fof(interp, fi_functors, a1774 = 1). % 5.66/5.89 fof(interp, fi_functors, a1775 = 1). % 5.66/5.89 fof(interp, fi_functors, a1776 = 1). % 5.66/5.89 fof(interp, fi_functors, a1777 = 0). % 5.66/5.89 fof(interp, fi_functors, a1778 = 0). % 5.66/5.89 fof(interp, fi_functors, a1779 = 0). % 5.66/5.89 fof(interp, fi_functors, a1780 = 0). % 5.66/5.89 fof(interp, fi_functors, a1781 = 0). % 5.66/5.89 fof(interp, fi_functors, a1782 = 0). % 5.66/5.89 fof(interp, fi_functors, a1783 = 0). % 5.66/5.89 fof(interp, fi_functors, a1784 = 1). % 5.66/5.89 fof(interp, fi_functors, a1785 = 1). % 5.66/5.89 fof(interp, fi_functors, a1786 = 0). % 5.66/5.89 fof(interp, fi_functors, a1787 = 0). % 5.66/5.89 fof(interp, fi_functors, a1788 = 0). % 5.66/5.89 fof(interp, fi_functors, a1789 = 0). % 5.66/5.89 fof(interp, fi_functors, a1790 = 0). % 5.66/5.89 fof(interp, fi_functors, a1791 = 0). % 5.66/5.89 fof(interp, fi_functors, a1792 = 0). % 5.66/5.89 fof(interp, fi_functors, a1793 = 1). % 5.66/5.89 fof(interp, fi_functors, a1794 = 1). % 5.66/5.89 fof(interp, fi_functors, a1795 = 0). % 5.66/5.89 fof(interp, fi_functors, a1796 = 1). % 5.66/5.89 fof(interp, fi_functors, a1797 = 1). % 5.66/5.89 fof(interp, fi_functors, a1798 = 1). % 5.66/5.89 fof(interp, fi_functors, a1799 = 0). % 5.66/5.89 fof(interp, fi_functors, a1800 = 0). % 5.66/5.89 fof(interp, fi_functors, a1801 = 1). % 5.66/5.89 fof(interp, fi_functors, a1802 = 1). % 5.66/5.89 fof(interp, fi_functors, a1803 = 0). % 5.66/5.89 fof(interp, fi_functors, a1804 = 1). % 5.66/5.89 fof(interp, fi_functors, a1805 = 0). % 5.66/5.89 fof(interp, fi_functors, a1806 = 1). % 5.66/5.89 fof(interp, fi_functors, a1807 = 0). % 5.66/5.89 fof(interp, fi_functors, a1808 = 1). % 5.66/5.89 fof(interp, fi_functors, a1809 = 0). % 5.66/5.89 fof(interp, fi_functors, a1810 = 1). % 5.66/5.89 fof(interp, fi_functors, a1811 = 0). % 5.66/5.89 fof(interp, fi_functors, a1812 = 1). % 5.66/5.89 fof(interp, fi_functors, a1813 = 1). % 5.66/5.89 fof(interp, fi_functors, a1814 = 0). % 5.66/5.89 fof(interp, fi_functors, a1815 = 0). % 5.66/5.89 fof(interp, fi_functors, a1816 = 0). % 5.66/5.89 fof(interp, fi_functors, a1817 = 1). % 5.66/5.89 fof(interp, fi_functors, a1818 = 0). % 5.66/5.89 fof(interp, fi_functors, a1819 = 1). % 5.66/5.89 fof(interp, fi_functors, a1820 = 0). % 5.66/5.89 fof(interp, fi_functors, a1821 = 0). % 5.66/5.89 fof(interp, fi_functors, a1822 = 0). % 5.66/5.89 fof(interp, fi_functors, a1823 = 0). % 5.66/5.89 fof(interp, fi_functors, a1824 = 0). % 5.66/5.89 fof(interp, fi_functors, a1825 = 0). % 5.66/5.89 fof(interp, fi_functors, a1826 = 0). % 5.66/5.89 fof(interp, fi_functors, a1827 = 0). % 5.66/5.89 fof(interp, fi_functors, a1828 = 0). % 5.66/5.89 fof(interp, fi_functors, a1829 = 0). % 5.66/5.89 fof(interp, fi_functors, a1830 = 0). % 5.66/5.89 fof(interp, fi_functors, a1831 = 1). % 5.66/5.89 fof(interp, fi_functors, a1832 = 0). % 5.66/5.89 fof(interp, fi_functors, a1833 = 0). % 5.66/5.89 fof(interp, fi_predicates, c10_0). % 5.66/5.89 fof(interp, fi_predicates, c10_1(0) & ~c10_1(1)). % 5.66/5.89 fof(interp, fi_predicates, ~c10_2(0, 0) & c10_2(0, 1) & c10_2(1, 0) & % 5.66/5.89 ~c10_2(1, 1)). % 5.66/5.89 fof(interp, fi_predicates, c1_0). % 5.66/5.89 fof(interp, fi_predicates, ~c1_1(0) & ~c1_1(1)). % 5.66/5.89 fof(interp, fi_predicates, ~c1_2(0, 0) & c1_2(0, 1) & c1_2(1, 0) & ~c1_2(1, 1)). % 5.66/5.89 fof(interp, fi_predicates, c2_0). % 5.66/5.89 fof(interp, fi_predicates, c2_1(0) & ~c2_1(1)). % 5.66/5.89 fof(interp, fi_predicates, c2_2(0, 0) & c2_2(0, 1) & c2_2(1, 0) & c2_2(1, 1)). % 5.66/5.89 fof(interp, fi_predicates, c3_0). % 5.66/5.89 fof(interp, fi_predicates, c3_1(0) & ~c3_1(1)). % 5.66/5.89 fof(interp, fi_predicates, c3_2(0, 0) & c3_2(0, 1) & c3_2(1, 0) & c3_2(1, 1)). % 5.66/5.89 fof(interp, fi_predicates, ~c4_0). % 5.66/5.89 fof(interp, fi_predicates, ~c4_1(0) & c4_1(1)). % 5.66/5.89 fof(interp, fi_predicates, ~c4_2(0, 0) & ~c4_2(0, 1) & c4_2(1, 0) & ~c4_2(1, 1)). % 5.66/5.89 fof(interp, fi_predicates, c5_0). % 5.66/5.89 fof(interp, fi_predicates, ~c5_1(0) & c5_1(1)). % 5.66/5.89 fof(interp, fi_predicates, c5_2(0, 0) & ~c5_2(0, 1) & c5_2(1, 0) & c5_2(1, 1)). % 5.66/5.89 fof(interp, fi_predicates, ~c6_0). % 5.66/5.89 fof(interp, fi_predicates, ~c6_1(0) & ~c6_1(1)). % 5.66/5.89 fof(interp, fi_predicates, ~c6_2(0, 0) & c6_2(0, 1) & c6_2(1, 0) & ~c6_2(1, 1)). % 5.66/5.89 fof(interp, fi_predicates, c7_0). % 5.66/5.89 fof(interp, fi_predicates, ~c7_1(0) & ~c7_1(1)). % 5.66/5.89 fof(interp, fi_predicates, c7_2(0, 0) & c7_2(0, 1) & c7_2(1, 0) & ~c7_2(1, 1)). % 5.66/5.89 fof(interp, fi_predicates, ~c8_0). % 5.66/5.89 fof(interp, fi_predicates, c8_1(0) & c8_1(1)). % 5.66/5.89 fof(interp, fi_predicates, c8_2(0, 0) & ~c8_2(0, 1) & ~c8_2(1, 0) & ~c8_2(1, 1)). % 5.66/5.89 fof(interp, fi_predicates, c9_0). % 5.66/5.89 fof(interp, fi_predicates, c9_1(0) & ~c9_1(1)). % 5.66/5.89 fof(interp, fi_predicates, ~c9_2(0, 0) & c9_2(0, 1) & ~c9_2(1, 0) & ~c9_2(1, 1)). % 5.66/5.89 fof(interp, fi_predicates, ~epred10_0). % 5.66/5.89 fof(interp, fi_predicates, epred11_0). % 5.66/5.89 fof(interp, fi_predicates, ~epred12_0). % 5.66/5.89 fof(interp, fi_predicates, ~epred13_0). % 5.66/5.89 fof(interp, fi_predicates, epred14_0). % 5.66/5.89 fof(interp, fi_predicates, epred15_0). % 5.66/5.89 fof(interp, fi_predicates, ~epred16_0). % 5.66/5.89 fof(interp, fi_predicates, epred17_0). % 5.66/5.89 fof(interp, fi_predicates, epred1_0). % 5.66/5.89 fof(interp, fi_predicates, epred2_0). % 5.66/5.89 fof(interp, fi_predicates, epred3_0). % 5.66/5.89 fof(interp, fi_predicates, epred4_0). % 5.66/5.89 fof(interp, fi_predicates, epred5_0). % 5.66/5.89 fof(interp, fi_predicates, epred6_0). % 5.66/5.89 fof(interp, fi_predicates, ~epred7_0). % 5.66/5.89 fof(interp, fi_predicates, epred8_0). % 5.66/5.89 fof(interp, fi_predicates, ~epred9_0). % 5.66/5.89 fof(interp, fi_predicates, ndr1_0). % 5.66/5.89 fof(interp, fi_predicates, ndr1_1(0) & ndr1_1(1)). % 5.66/5.89 % SZS output end FiniteModel for theBenchmark.p % 5.66/5.89 % 0 lemma(s) from E % 5.66/5.89 % 2053 pred(s) % 5.66/5.89 % 253 func(s) % 5.66/5.89 % 2 sort(s) % 5.66/5.89 % 4234 clause(s) % 5.66/5.89 % Instantiating 1 (5374 ms) % 5.66/5.89 % Solving (5378 ms) % 5.66/5.89 % Instantiating 2 (5379 ms) % 5.66/5.89 % Solving (5390 ms) % 5.66/5.89 % % 5.66/5.89 % 1 model found (5404 ms) %------------------------------------------------------------------------------