%------------------------------------------------------------------------------ % File : Nitpick---2016 % Problem : SYN427+1 : TPTP v6.4.0. Released v2.1.0. % Transfm : none % Format : tptp:raw % Command : isabelle tptp_nitpick %d %s % Computer : n095.star.cs.uiowa.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2609 0 2.40GHz % Memory : 32218.75MB % OS : Linux 3.10.0-327.36.3.el7.x86_64 % CPULimit : 300s % DateTime : Wed Jan 18 18:47:17 EST 2017 % Result : CounterSatisfiable 34.09s % Output : FiniteModel 34.09s % Verified : % SZS Type : None (Parsing solution fails) % Syntax : Number of formulae : 0 % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : SYN427+1 : TPTP v6.4.0. Released v2.1.0. % 0.00/0.04 % Command : isabelle tptp_nitpick %d %s % 0.03/0.23 % Computer : n095.star.cs.uiowa.edu % 0.03/0.23 % Model : x86_64 x86_64 % 0.03/0.23 % CPU : Intel(R) Xeon(R) CPU E5-2609 0 @ 2.40GHz % 0.03/0.23 % Memory : 32218.75MB % 0.03/0.23 % OS : Linux 3.10.0-327.36.3.el7.x86_64 % 0.03/0.23 % CPULimit : 300 % 0.03/0.23 % DateTime : Mon Jan 16 01:41:33 CST 2017 % 0.03/0.24 % CPUTime: % 34.09/17.42 Nitpicking formula... % 34.09/17.42 Timestamp: 01:41:42 % 34.09/17.42 Using SAT solver "Lingeling_JNI" The following solvers are configured: % 34.09/17.42 "Lingeling_JNI", "CryptoMiniSat_JNI", "MiniSat_JNI", "SAT4J", "SAT4J_Light" % 34.09/17.42 Batch 1 of 20: Trying 5 scopes: % 34.09/17.42 card TPTP_Interpret.ind = 1 % 34.09/17.42 card TPTP_Interpret.ind = 2 % 34.09/17.42 card TPTP_Interpret.ind = 3 % 34.09/17.42 card TPTP_Interpret.ind = 4 % 34.09/17.42 card TPTP_Interpret.ind = 5 % 34.09/17.42 % SZS status CounterSatisfiable % SZS output start FiniteModel % 34.09/17.42 Nitpick found a counterexample for card TPTP_Interpret.ind = 2: % 34.09/17.42 % 34.09/17.42 Constants: % 34.09/17.42 bnd_a1581 = i1 % 34.09/17.42 bnd_a1582 = i1 % 34.09/17.42 bnd_a1583 = i1 % 34.09/17.42 bnd_a1584 = i1 % 34.09/17.42 bnd_a1585 = i1 % 34.09/17.42 bnd_a1586 = i1 % 34.09/17.42 bnd_a1587 = i1 % 34.09/17.42 bnd_a1588 = i1 % 34.09/17.42 bnd_a1589 = i2 % 34.09/17.42 bnd_a1590 = i1 % 34.09/17.42 bnd_a1591 = i1 % 34.09/17.42 bnd_a1592 = i1 % 34.09/17.42 bnd_a1593 = i1 % 34.09/17.42 bnd_a1594 = i2 % 34.09/17.42 bnd_a1595 = i2 % 34.09/17.42 bnd_a1596 = i1 % 34.09/17.42 bnd_a1597 = i1 % 34.09/17.42 bnd_a1598 = i1 % 34.09/17.42 bnd_a1599 = i1 % 34.09/17.42 bnd_a1600 = i1 % 34.09/17.42 bnd_a1601 = i1 % 34.09/17.42 bnd_a1602 = i1 % 34.09/17.42 bnd_a1603 = i1 % 34.09/17.42 bnd_a1604 = i1 % 34.09/17.42 bnd_a1605 = i2 % 34.09/17.42 bnd_a1606 = i1 % 34.09/17.42 bnd_a1607 = i1 % 34.09/17.42 bnd_a1608 = i1 % 34.09/17.42 bnd_a1609 = i1 % 34.09/17.42 bnd_a1610 = i2 % 34.09/17.42 bnd_a1611 = i2 % 34.09/17.42 bnd_a1612 = i2 % 34.09/17.42 bnd_a1613 = i1 % 34.09/17.42 bnd_a1614 = i1 % 34.09/17.42 bnd_a1615 = i1 % 34.09/17.42 bnd_a1616 = i1 % 34.09/17.42 bnd_a1617 = i1 % 34.09/17.42 bnd_a1618 = i1 % 34.09/17.42 bnd_a1619 = i1 % 34.09/17.42 bnd_a1620 = i1 % 34.09/17.42 bnd_a1621 = i1 % 34.09/17.42 bnd_a1622 = i1 % 34.09/17.42 bnd_a1623 = i1 % 34.09/17.42 bnd_a1624 = i1 % 34.09/17.42 bnd_a1625 = i1 % 34.09/17.42 bnd_a1626 = i1 % 34.09/17.42 bnd_a1627 = i1 % 34.09/17.42 bnd_a1628 = i1 % 34.09/17.42 bnd_a1629 = i1 % 34.09/17.42 bnd_a1630 = i2 % 34.09/17.42 bnd_a1631 = i1 % 34.09/17.42 bnd_a1632 = i1 % 34.09/17.42 bnd_a1633 = i1 % 34.09/17.42 bnd_a1634 = i2 % 34.09/17.42 bnd_a1635 = i1 % 34.09/17.42 bnd_a1636 = i1 % 34.09/17.42 bnd_a1637 = i1 % 34.09/17.42 bnd_a1638 = i1 % 34.09/17.42 bnd_a1639 = i1 % 34.09/17.42 bnd_a1640 = i1 % 34.09/17.42 bnd_a1641 = i1 % 34.09/17.42 bnd_a1642 = i1 % 34.09/17.42 bnd_a1643 = i2 % 34.09/17.42 bnd_a1644 = i2 % 34.09/17.42 bnd_a1645 = i1 % 34.09/17.42 bnd_a1646 = i2 % 34.09/17.42 bnd_a1647 = i2 % 34.09/17.42 bnd_a1648 = i2 % 34.09/17.42 bnd_a1649 = i2 % 34.09/17.42 bnd_a1650 = i2 % 34.09/17.42 bnd_a1651 = i1 % 34.09/17.42 bnd_a1652 = i1 % 34.09/17.42 bnd_a1653 = i1 % 34.09/17.42 bnd_a1654 = i1 % 34.09/17.42 bnd_a1655 = i2 % 34.09/17.42 bnd_a1656 = i1 % 34.09/17.42 bnd_a1657 = i1 % 34.09/17.42 bnd_a1658 = i1 % 34.09/17.42 bnd_a1659 = i2 % 34.09/17.42 bnd_a1660 = i1 % 34.09/17.42 bnd_a1661 = i1 % 34.09/17.42 bnd_a1662 = i1 % 34.09/17.42 bnd_a1663 = i1 % 34.09/17.42 bnd_a1664 = i1 % 34.09/17.42 bnd_a1665 = i1 % 34.09/17.42 bnd_a1666 = i2 % 34.09/17.42 bnd_a1667 = i1 % 34.09/17.42 bnd_a1668 = i1 % 34.09/17.42 bnd_a1669 = i1 % 34.09/17.42 bnd_a1670 = i1 % 34.09/17.42 bnd_a1671 = i1 % 34.09/17.42 bnd_a1672 = i1 % 34.09/17.42 bnd_a1673 = i1 % 34.09/17.42 bnd_a1674 = i1 % 34.09/17.42 bnd_a1675 = i1 % 34.09/17.42 bnd_a1676 = i2 % 34.09/17.42 bnd_a1677 = i1 % 34.09/17.42 bnd_a1678 = i1 % 34.09/17.42 bnd_a1679 = i2 % 34.09/17.42 bnd_a1680 = i1 % 34.09/17.42 bnd_a1681 = i1 % 34.09/17.42 bnd_a1682 = i1 % 34.09/17.42 bnd_a1683 = i2 % 34.09/17.42 bnd_a1684 = i2 % 34.09/17.42 bnd_a1685 = i1 % 34.09/17.42 bnd_a1686 = i1 % 34.09/17.42 bnd_a1687 = i1 % 34.09/17.42 bnd_a1688 = i1 % 34.09/17.42 bnd_a1689 = i2 % 34.09/17.42 bnd_a1690 = i1 % 34.09/17.42 bnd_a1691 = i1 % 34.09/17.42 bnd_a1692 = i1 % 34.09/17.42 bnd_a1693 = i1 % 34.09/17.42 bnd_a1694 = i1 % 34.09/17.42 bnd_a1695 = i1 % 34.09/17.42 bnd_a1696 = i1 % 34.09/17.42 bnd_a1697 = i1 % 34.09/17.42 bnd_a1698 = i2 % 34.09/17.42 bnd_a1699 = i1 % 34.09/17.42 bnd_a1700 = i1 % 34.09/17.42 bnd_a1701 = i1 % 34.09/17.42 bnd_a1702 = i2 % 34.09/17.42 bnd_a1703 = i2 % 34.09/17.42 bnd_a1704 = i1 % 34.09/17.42 bnd_a1705 = i2 % 34.09/17.42 bnd_a1706 = i1 % 34.09/17.42 bnd_a1707 = i1 % 34.09/17.42 bnd_a1708 = i1 % 34.09/17.42 bnd_a1709 = i1 % 34.09/17.42 bnd_a1710 = i1 % 34.09/17.42 bnd_a1711 = i1 % 34.09/17.42 bnd_a1712 = i1 % 34.09/17.42 bnd_a1713 = i2 % 34.09/17.42 bnd_a1714 = i1 % 34.09/17.42 bnd_a1715 = i1 % 34.09/17.42 bnd_a1716 = i1 % 34.09/17.42 bnd_a1717 = i1 % 34.09/17.42 bnd_a1718 = i1 % 34.09/17.42 bnd_a1719 = i1 % 34.09/17.42 bnd_a1720 = i1 % 34.09/17.42 bnd_a1721 = i1 % 34.09/17.42 bnd_a1722 = i1 % 34.09/17.42 bnd_a1723 = i1 % 34.09/17.42 bnd_a1724 = i1 % 34.09/17.42 bnd_a1725 = i1 % 34.09/17.42 bnd_a1726 = i1 % 34.09/17.42 bnd_a1727 = i1 % 34.09/17.42 bnd_a1728 = i1 % 34.09/17.42 bnd_a1729 = i1 % 34.09/17.42 bnd_a1730 = i1 % 34.09/17.42 bnd_a1731 = i1 % 34.09/17.42 bnd_a1732 = i1 % 34.09/17.42 bnd_a1733 = i1 % 34.09/17.42 bnd_a1734 = i1 % 34.09/17.42 bnd_a1735 = i1 % 34.09/17.42 bnd_a1736 = i1 % 34.09/17.42 bnd_a1737 = i2 % 34.09/17.42 bnd_a1738 = i2 % 34.09/17.42 bnd_a1739 = i2 % 34.09/17.42 bnd_a1740 = i1 % 34.09/17.42 bnd_a1741 = i1 % 34.09/17.42 bnd_a1742 = i1 % 34.09/17.42 bnd_a1743 = i2 % 34.09/17.42 bnd_a1744 = i1 % 34.09/17.42 bnd_a1745 = i1 % 34.09/17.42 bnd_a1746 = i1 % 34.09/17.42 bnd_a1747 = i2 % 34.09/17.42 bnd_a1748 = i1 % 34.09/17.42 bnd_a1749 = i1 % 34.09/17.42 bnd_a1750 = i1 % 34.09/17.42 bnd_a1751 = i1 % 34.09/17.42 bnd_a1752 = i2 % 34.09/17.42 bnd_a1753 = i1 % 34.09/17.42 bnd_a1754 = i1 % 34.09/17.42 bnd_a1755 = i1 % 34.09/17.42 bnd_a1756 = i1 % 34.09/17.42 bnd_a1757 = i1 % 34.09/17.42 bnd_a1758 = i1 % 34.09/17.42 bnd_a1759 = i1 % 34.09/17.42 bnd_a1760 = i1 % 34.09/17.42 bnd_a1761 = i1 % 34.09/17.42 bnd_a1762 = i1 % 34.09/17.42 bnd_a1763 = i1 % 34.09/17.42 bnd_a1764 = i2 % 34.09/17.42 bnd_a1765 = i1 % 34.09/17.42 bnd_a1766 = i1 % 34.09/17.42 bnd_a1767 = i1 % 34.09/17.42 bnd_a1768 = i1 % 34.09/17.42 bnd_a1769 = i1 % 34.09/17.42 bnd_a1770 = i1 % 34.09/17.42 bnd_a1771 = i1 % 34.09/17.42 bnd_a1772 = i1 % 34.09/17.42 bnd_a1773 = i1 % 34.09/17.42 bnd_a1774 = i1 % 34.09/17.42 bnd_a1775 = i1 % 34.09/17.42 bnd_a1776 = i1 % 34.09/17.42 bnd_a1777 = i1 % 34.09/17.42 bnd_a1778 = i1 % 34.09/17.42 bnd_a1779 = i1 % 34.09/17.42 bnd_a1780 = i1 % 34.09/17.42 bnd_a1781 = i1 % 34.09/17.42 bnd_a1782 = i1 % 34.09/17.42 bnd_a1783 = i1 % 34.09/17.42 bnd_a1784 = i2 % 34.09/17.42 bnd_a1785 = i2 % 34.09/17.42 bnd_a1786 = i2 % 34.09/17.42 bnd_a1787 = i2 % 34.09/17.42 bnd_a1788 = i1 % 34.09/17.42 bnd_a1789 = i1 % 34.09/17.42 bnd_a1790 = i1 % 34.09/17.42 bnd_a1791 = i1 % 34.09/17.42 bnd_a1792 = i1 % 34.09/17.42 bnd_a1793 = i1 % 34.09/17.42 bnd_a1794 = i1 % 34.09/17.42 bnd_a1795 = i2 % 34.09/17.42 bnd_a1796 = i1 % 34.09/17.42 bnd_a1797 = i2 % 34.09/17.42 bnd_a1798 = i2 % 34.09/17.42 bnd_a1799 = i2 % 34.09/17.42 bnd_a1800 = i1 % 34.09/17.42 bnd_a1801 = i1 % 34.09/17.42 bnd_a1802 = i1 % 34.09/17.42 bnd_a1803 = i1 % 34.09/17.42 bnd_a1804 = i1 % 34.09/17.42 bnd_a1805 = i1 % 34.09/17.42 bnd_a1806 = i2 % 34.09/17.42 bnd_a1807 = i1 % 34.09/17.42 bnd_a1808 = i1 % 34.09/17.42 bnd_a1809 = i1 % 34.09/17.42 bnd_a1810 = i1 % 34.09/17.42 bnd_a1811 = i1 % 34.09/17.42 bnd_a1812 = i2 % 34.09/17.42 bnd_a1813 = i2 % 34.09/17.42 bnd_a1814 = i1 % 34.09/17.42 bnd_a1815 = i1 % 34.09/17.42 bnd_a1816 = i1 % 34.09/17.42 bnd_a1817 = i1 % 34.09/17.42 bnd_a1818 = i1 % 34.09/17.42 bnd_a1819 = i2 % 34.09/17.42 bnd_a1820 = i1 % 34.09/17.42 bnd_a1821 = i2 % 34.09/17.42 bnd_a1822 = i1 % 34.09/17.42 bnd_a1823 = i2 % 34.09/17.42 bnd_a1824 = i1 % 34.09/17.42 bnd_a1825 = i1 % 34.09/17.42 bnd_a1826 = i1 % 34.09/17.42 bnd_a1827 = i1 % 34.09/17.42 bnd_a1828 = i1 % 34.09/17.42 bnd_a1829 = i1 % 34.09/17.42 bnd_a1830 = i2 % 34.09/17.42 bnd_a1831 = i1 % 34.09/17.42 bnd_a1832 = i1 % 34.09/17.42 bnd_a1833 = i1 % 34.09/17.42 bnd_c10_0 = True % 34.09/17.42 bnd_c10_1 = (\<lambda>x. _)(i1 := True, i2 := False) % 34.09/17.42 bnd_c10_2 = % 34.09/17.42 (\<lambda>x. _) % 34.09/17.42 (i1 := (\<lambda>x. _)(i1 := False, i2 := False), % 34.09/17.42 i2 := (\<lambda>x. _)(i1 := False, i2 := True)) % 34.09/17.42 bnd_c1_0 = True % 34.09/17.42 bnd_c1_1 = (\<lambda>x. _)(i1 := True, i2 := False) % 34.09/17.42 bnd_c1_2 = % 34.09/17.42 (\<lambda>x. _) % 34.09/17.42 (i1 := (\<lambda>x. _)(i1 := True, i2 := False), % 34.09/17.42 i2 := (\<lambda>x. _)(i1 := False, i2 := False)) % 34.09/17.42 bnd_c2_0 = True % 34.09/17.42 bnd_c2_1 = (\<lambda>x. _)(i1 := True, i2 := False) % 34.09/17.42 bnd_c2_2 = % 34.09/17.42 (\<lambda>x. _) % 34.09/17.42 (i1 := (\<lambda>x. _)(i1 := False, i2 := True), % 34.09/17.42 i2 := (\<lambda>x. _)(i1 := True, i2 := False)) % 34.09/17.42 bnd_c3_0 = True % 34.09/17.42 bnd_c3_1 = (\<lambda>x. _)(i1 := True, i2 := False) % 34.09/17.42 bnd_c3_2 = % 34.09/17.42 (\<lambda>x. _) % 34.09/17.42 (i1 := (\<lambda>x. _)(i1 := True, i2 := True), % 34.09/17.42 i2 := (\<lambda>x. _)(i1 := False, i2 := True)) % 34.09/17.42 bnd_c4_0 = False % 34.09/17.42 bnd_c4_1 = (\<lambda>x. _)(i1 := False, i2 := False) % 34.09/17.42 bnd_c4_2 = % 34.09/17.42 (\<lambda>x. _) % 34.09/17.42 (i1 := (\<lambda>x. _)(i1 := False, i2 := False), % 34.09/17.42 i2 := (\<lambda>x. _)(i1 := True, i2 := True)) % 34.09/17.42 bnd_c5_0 = True % 34.09/17.42 bnd_c5_1 = (\<lambda>x. _)(i1 := False, i2 := False) % 34.09/17.42 bnd_c5_2 = % 34.09/17.42 (\<lambda>x. _) % 34.09/17.42 (i1 := (\<lambda>x. _)(i1 := True, i2 := False), % 34.09/17.42 i2 := (\<lambda>x. _)(i1 := False, i2 := True)) % 34.09/17.42 bnd_c6_0 = False % 34.09/17.42 bnd_c6_1 = (\<lambda>x. _)(i1 := False, i2 := True) % 34.09/17.42 bnd_c6_2 = % 34.09/17.42 (\<lambda>x. _) % 34.09/17.42 (i1 := (\<lambda>x. _)(i1 := True, i2 := False), % 34.09/17.42 i2 := (\<lambda>x. _)(i1 := True, i2 := False)) % 34.09/17.42 bnd_c7_0 = True % 34.09/17.42 bnd_c7_1 = (\<lambda>x. _)(i1 := False, i2 := True) % 34.09/17.42 bnd_c7_2 = % 34.09/17.42 (\<lambda>x. _) % 34.09/17.42 (i1 := (\<lambda>x. _)(i1 := True, i2 := True), % 34.09/17.42 i2 := (\<lambda>x. _)(i1 := False, i2 := False)) % 34.09/17.42 bnd_c8_0 = False % 34.09/17.42 bnd_c8_1 = (\<lambda>x. _)(i1 := True, i2 := True) % 34.09/17.42 bnd_c8_2 = % 34.09/17.42 (\<lambda>x. _) % 34.09/17.42 (i1 := (\<lambda>x. _)(i1 := False, i2 := True), % 34.09/17.42 i2 := (\<lambda>x. _)(i1 := True, i2 := False)) % 34.09/17.42 bnd_c9_0 = True % 34.09/17.42 bnd_c9_1 = (\<lambda>x. _)(i1 := True, i2 := False) % 34.09/17.42 bnd_c9_2 = % 34.09/17.42 (\<lambda>x. _) % 34.09/17.42 (i1 := (\<lambda>x. _)(i1 := False, i2 := False), % 34.09/17.42 i2 := (\<lambda>x. _)(i1 := True, i2 := True)) % 34.09/17.42 bnd_ndr1_0 = True % 34.09/17.42 bnd_ndr1_1 = (\<lambda>x. _)(i1 := True, i2 := True) % 34.09/17.42 % SZS output end FiniteModel % 34.09/17.42 Total time: 7.7 s %------------------------------------------------------------------------------