%------------------------------------------------------------------------------ % 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 : n117.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 : Satisfiable 34.01s % Output : FiniteModel 34.05s % 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 : n117.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:03 CST 2017 % 0.03/0.24 % CPUTime: % 34.01/18.19 Nitpicking formula... % 34.01/18.19 Timestamp: 01:41:12 % 34.01/18.19 Using SAT solver "Lingeling_JNI" The following solvers are configured: % 34.01/18.19 "Lingeling_JNI", "CryptoMiniSat_JNI", "MiniSat_JNI", "SAT4J", "SAT4J_Light" % 34.01/18.19 Batch 1 of 20: Trying 5 scopes: % 34.01/18.19 card TPTP_Interpret.ind = 1 % 34.01/18.19 card TPTP_Interpret.ind = 2 % 34.01/18.19 card TPTP_Interpret.ind = 3 % 34.01/18.19 card TPTP_Interpret.ind = 4 % 34.01/18.19 card TPTP_Interpret.ind = 5 % 34.01/18.19 % SZS status Satisfiable % SZS output start FiniteModel % 34.01/18.19 Nitpick found a model for card TPTP_Interpret.ind = 2: % 34.01/18.19 % 34.01/18.19 Constants: % 34.01/18.19 bnd_a1581 = i1 % 34.01/18.19 bnd_a1582 = i1 % 34.01/18.19 bnd_a1583 = i1 % 34.01/18.19 bnd_a1584 = i1 % 34.01/18.19 bnd_a1585 = i1 % 34.01/18.19 bnd_a1586 = i2 % 34.01/18.19 bnd_a1587 = i1 % 34.01/18.19 bnd_a1588 = i2 % 34.01/18.19 bnd_a1589 = i2 % 34.01/18.19 bnd_a1590 = i1 % 34.01/18.19 bnd_a1593 = i1 % 34.01/18.19 bnd_a1594 = i1 % 34.01/18.19 bnd_a1595 = i1 % 34.01/18.19 bnd_a1596 = i1 % 34.01/18.19 bnd_a1597 = i1 % 34.01/18.19 bnd_a1598 = i1 % 34.01/18.19 bnd_a1599 = i1 % 34.01/18.19 bnd_a1600 = i1 % 34.01/18.19 bnd_a1601 = i1 % 34.01/18.19 bnd_a1602 = i1 % 34.01/18.19 bnd_a1603 = i1 % 34.01/18.19 bnd_a1604 = i1 % 34.01/18.19 bnd_a1605 = i1 % 34.01/18.19 bnd_a1606 = i1 % 34.01/18.19 bnd_a1607 = i1 % 34.01/18.19 bnd_a1608 = i1 % 34.01/18.19 bnd_a1609 = i1 % 34.01/18.19 bnd_a1610 = i1 % 34.01/18.19 bnd_a1611 = i1 % 34.01/18.19 bnd_a1612 = i1 % 34.01/18.19 bnd_a1613 = i1 % 34.01/18.19 bnd_a1614 = i2 % 34.01/18.19 bnd_a1615 = i2 % 34.01/18.19 bnd_a1616 = i1 % 34.01/18.19 bnd_a1617 = i1 % 34.01/18.19 bnd_a1618 = i2 % 34.01/18.19 bnd_a1619 = i1 % 34.01/18.19 bnd_a1620 = i2 % 34.01/18.19 bnd_a1621 = i2 % 34.01/18.19 bnd_a1622 = i1 % 34.01/18.19 bnd_a1623 = i1 % 34.01/18.19 bnd_a1624 = i1 % 34.01/18.19 bnd_a1625 = i2 % 34.01/18.19 bnd_a1626 = i1 % 34.01/18.19 bnd_a1627 = i1 % 34.01/18.19 bnd_a1628 = i1 % 34.01/18.19 bnd_a1629 = i1 % 34.01/18.19 bnd_a1630 = i1 % 34.01/18.19 bnd_a1631 = i1 % 34.01/18.19 bnd_a1632 = i1 % 34.01/18.19 bnd_a1633 = i1 % 34.01/18.19 bnd_a1634 = i1 % 34.01/18.19 bnd_a1635 = i1 % 34.01/18.19 bnd_a1636 = i1 % 34.01/18.19 bnd_a1637 = i2 % 34.01/18.19 bnd_a1638 = i1 % 34.01/18.19 bnd_a1639 = i1 % 34.01/18.19 bnd_a1640 = i2 % 34.01/18.19 bnd_a1641 = i1 % 34.01/18.19 bnd_a1642 = i1 % 34.01/18.19 bnd_a1643 = i2 % 34.01/18.19 bnd_a1644 = i2 % 34.01/18.19 bnd_a1645 = i1 % 34.01/18.19 bnd_a1646 = i1 % 34.01/18.19 bnd_a1647 = i2 % 34.01/18.19 bnd_a1648 = i1 % 34.01/18.19 bnd_a1649 = i1 % 34.01/18.19 bnd_a1650 = i2 % 34.01/18.19 bnd_a1651 = i2 % 34.01/18.19 bnd_a1652 = i2 % 34.01/18.19 bnd_a1653 = i1 % 34.01/18.19 bnd_a1654 = i1 % 34.01/18.19 bnd_a1655 = i1 % 34.01/18.19 bnd_a1656 = i1 % 34.01/18.19 bnd_a1657 = i2 % 34.01/18.19 bnd_a1658 = i2 % 34.01/18.19 bnd_a1659 = i2 % 34.01/18.19 bnd_a1660 = i1 % 34.01/18.19 bnd_a1661 = i1 % 34.01/18.19 bnd_a1662 = i1 % 34.01/18.19 bnd_a1663 = i1 % 34.01/18.19 bnd_a1664 = i1 % 34.01/18.19 bnd_a1665 = i1 % 34.01/18.19 bnd_a1666 = i2 % 34.01/18.19 bnd_a1667 = i2 % 34.01/18.19 bnd_a1668 = i2 % 34.01/18.19 bnd_a1672 = i1 % 34.01/18.19 bnd_a1673 = i1 % 34.01/18.19 bnd_a1674 = i1 % 34.01/18.19 bnd_a1675 = i2 % 34.01/18.19 bnd_a1676 = i1 % 34.01/18.19 bnd_a1677 = i1 % 34.01/18.19 bnd_a1678 = i2 % 34.01/18.19 bnd_a1679 = i2 % 34.01/18.19 bnd_a1680 = i2 % 34.01/18.19 bnd_a1681 = i1 % 34.01/18.19 bnd_a1682 = i1 % 34.01/18.19 bnd_a1683 = i1 % 34.01/18.19 bnd_a1684 = i1 % 34.01/18.19 bnd_a1685 = i2 % 34.01/18.19 bnd_a1686 = i1 % 34.01/18.19 bnd_a1688 = i1 % 34.01/18.19 bnd_a1689 = i2 % 34.01/18.19 bnd_a1690 = i2 % 34.01/18.19 bnd_a1691 = i2 % 34.01/18.19 bnd_a1692 = i1 % 34.01/18.19 bnd_a1693 = i1 % 34.01/18.19 bnd_a1694 = i1 % 34.01/18.19 bnd_a1695 = i1 % 34.01/18.19 bnd_a1696 = i2 % 34.01/18.19 bnd_a1697 = i1 % 34.01/18.19 bnd_a1698 = i2 % 34.01/18.19 bnd_a1699 = i1 % 34.01/18.19 bnd_a1700 = i1 % 34.01/18.19 bnd_a1701 = i1 % 34.01/18.19 bnd_a1702 = i1 % 34.01/18.19 bnd_a1703 = i1 % 34.01/18.19 bnd_a1704 = i1 % 34.01/18.19 bnd_a1705 = i1 % 34.01/18.19 bnd_a1706 = i2 % 34.01/18.19 bnd_a1707 = i1 % 34.01/18.19 bnd_a1708 = i1 % 34.01/18.19 bnd_a1709 = i1 % 34.01/18.19 bnd_a1710 = i1 % 34.01/18.19 bnd_a1711 = i1 % 34.01/18.19 bnd_a1712 = i1 % 34.01/18.19 bnd_a1713 = i1 % 34.01/18.19 bnd_a1714 = i1 % 34.01/18.19 bnd_a1715 = i2 % 34.01/18.19 bnd_a1716 = i1 % 34.01/18.19 bnd_a1717 = i1 % 34.01/18.19 bnd_a1718 = i1 % 34.01/18.19 bnd_a1719 = i1 % 34.01/18.19 bnd_a1720 = i1 % 34.01/18.19 bnd_a1721 = i2 % 34.01/18.19 bnd_a1722 = i2 % 34.01/18.19 bnd_a1723 = i1 % 34.01/18.19 bnd_a1724 = i2 % 34.01/18.19 bnd_a1725 = i1 % 34.01/18.19 bnd_a1726 = i1 % 34.01/18.19 bnd_a1727 = i1 % 34.01/18.19 bnd_a1728 = i1 % 34.01/18.19 bnd_a1729 = i1 % 34.01/18.19 bnd_a1730 = i1 % 34.01/18.19 bnd_a1731 = i1 % 34.01/18.19 bnd_a1732 = i2 % 34.01/18.19 bnd_a1733 = i1 % 34.01/18.19 bnd_a1734 = i1 % 34.01/18.19 bnd_a1735 = i1 % 34.01/18.19 bnd_a1736 = i1 % 34.01/18.19 bnd_a1737 = i1 % 34.01/18.19 bnd_a1738 = i2 % 34.01/18.19 bnd_a1739 = i1 % 34.01/18.19 bnd_a1740 = i1 % 34.01/18.19 bnd_a1741 = i1 % 34.01/18.19 bnd_a1742 = i1 % 34.01/18.19 bnd_a1743 = i1 % 34.01/18.19 bnd_a1744 = i1 % 34.01/18.19 bnd_a1745 = i1 % 34.01/18.19 bnd_a1746 = i1 % 34.01/18.19 bnd_a1747 = i1 % 34.01/18.19 bnd_a1748 = i2 % 34.01/18.19 bnd_a1749 = i1 % 34.01/18.19 bnd_a1750 = i1 % 34.01/18.19 bnd_a1751 = i1 % 34.01/18.19 bnd_a1752 = i1 % 34.01/18.19 bnd_a1753 = i1 % 34.01/18.19 bnd_a1754 = i1 % 34.01/18.19 bnd_a1755 = i1 % 34.01/18.19 bnd_a1756 = i1 % 34.01/18.19 bnd_a1757 = i1 % 34.01/18.19 bnd_a1758 = i1 % 34.01/18.19 bnd_a1759 = i1 % 34.01/18.19 bnd_a1760 = i2 % 34.01/18.19 bnd_a1761 = i1 % 34.01/18.19 bnd_a1762 = i1 % 34.01/18.19 bnd_a1763 = i1 % 34.01/18.19 bnd_a1764 = i1 % 34.01/18.19 bnd_a1765 = i1 % 34.01/18.19 bnd_a1767 = i2 % 34.01/18.19 bnd_a1768 = i1 % 34.01/18.19 bnd_a1769 = i1 % 34.01/18.19 bnd_a1770 = i1 % 34.01/18.19 bnd_a1771 = i1 % 34.01/18.19 bnd_a1772 = i1 % 34.01/18.19 bnd_a1773 = i1 % 34.01/18.19 bnd_a1774 = i1 % 34.01/18.19 bnd_a1775 = i1 % 34.01/18.19 bnd_a1776 = i1 % 34.01/18.19 bnd_a1777 = i1 % 34.01/18.19 bnd_a1778 = i1 % 34.01/18.19 bnd_a1779 = i2 % 34.01/18.19 bnd_a1780 = i1 % 34.01/18.19 bnd_a1781 = i1 % 34.01/18.19 bnd_a1782 = i1 % 34.01/18.19 bnd_a1783 = i1 % 34.01/18.19 bnd_a1784 = i2 % 34.01/18.19 bnd_a1785 = i2 % 34.01/18.19 bnd_a1786 = i2 % 34.01/18.19 bnd_a1787 = i2 % 34.01/18.19 bnd_a1788 = i2 % 34.01/18.19 bnd_a1789 = i2 % 34.01/18.19 bnd_a1790 = i1 % 34.01/18.19 bnd_a1791 = i1 % 34.01/18.19 bnd_a1792 = i1 % 34.01/18.19 bnd_a1793 = i1 % 34.01/18.19 bnd_a1794 = i1 % 34.01/18.19 bnd_a1795 = i1 % 34.01/18.19 bnd_a1796 = i1 % 34.01/18.19 bnd_a1797 = i1 % 34.01/18.19 bnd_a1798 = i1 % 34.01/18.19 bnd_a1799 = i1 % 34.01/18.19 bnd_a1800 = i1 % 34.01/18.19 bnd_a1801 = i2 % 34.01/18.19 bnd_a1802 = i1 % 34.01/18.19 bnd_a1803 = i1 % 34.01/18.19 bnd_a1804 = i1 % 34.01/18.19 bnd_a1805 = i2 % 34.01/18.19 bnd_a1806 = i2 % 34.01/18.19 bnd_a1807 = i1 % 34.01/18.19 bnd_a1808 = i1 % 34.01/18.19 bnd_a1809 = i1 % 34.01/18.19 bnd_a1810 = i1 % 34.01/18.19 bnd_a1811 = i2 % 34.01/18.19 bnd_a1812 = i2 % 34.01/18.19 bnd_a1813 = i2 % 34.01/18.19 bnd_a1814 = i1 % 34.01/18.19 bnd_a1815 = i1 % 34.01/18.19 bnd_a1817 = i1 % 34.01/18.19 bnd_a1818 = i1 % 34.01/18.19 bnd_a1819 = i2 % 34.01/18.19 bnd_a1820 = i2 % 34.01/18.19 bnd_a1821 = i2 % 34.01/18.19 bnd_a1822 = i1 % 34.01/18.19 bnd_a1823 = i1 % 34.01/18.19 bnd_a1824 = i1 % 34.01/18.19 bnd_a1825 = i1 % 34.01/18.19 bnd_a1826 = i1 % 34.01/18.19 bnd_a1827 = i2 % 34.01/18.19 bnd_a1829 = i1 % 34.01/18.19 bnd_a1830 = i1 % 34.01/18.19 bnd_a1831 = i2 % 34.01/18.19 bnd_a1832 = i2 % 34.01/18.19 bnd_a1833 = i1 % 34.01/18.19 bnd_c10_0 = False % 34.01/18.19 bnd_c10_1 = (\<lambda>x. _)(i1 := True, i2 := False) % 34.01/18.19 bnd_c10_2 = % 34.01/18.19 (\<lambda>x. _) % 34.01/18.19 (i1 := (\<lambda>x. _)(i1 := True, i2 := True), % 34.01/18.19 i2 := (\<lambda>x. _)(i1 := True, i2 := False)) % 34.01/18.19 bnd_c1_0 = False % 34.01/18.19 bnd_c1_1 = (\<lambda>x. _)(i1 := True, i2 := False) % 34.01/18.19 bnd_c1_2 = % 34.01/18.19 (\<lambda>x. _) % 34.01/18.19 (i1 := (\<lambda>x. _)(i1 := True, i2 := True), % 34.01/18.19 i2 := (\<lambda>x. _)(i1 := False, i2 := True)) % 34.01/18.19 bnd_c2_0 = True % 34.01/18.19 bnd_c2_1 = (\<lambda>x. _)(i1 := True, i2 := True) % 34.01/18.19 bnd_c2_2 = % 34.01/18.19 (\<lambda>x. _) % 34.01/18.19 (i1 := (\<lambda>x. _)(i1 := True, i2 := False), % 34.01/18.19 i2 := (\<lambda>x. _)(i1 := True, i2 := True)) % 34.01/18.19 bnd_c3_0 = False % 34.01/18.19 bnd_c3_1 = (\<lambda>x. _)(i1 := True, i2 := True) % 34.01/18.19 bnd_c3_2 = % 34.01/18.19 (\<lambda>x. _) % 34.01/18.19 (i1 := (\<lambda>x. _)(i1 := True, i2 := False), % 34.01/18.19 i2 := (\<lambda>x. _)(i1 := True, i2 := False)) % 34.01/18.19 bnd_c4_0 = False % 34.01/18.19 bnd_c4_1 = (\<lambda>x. _)(i1 := False, i2 := True) % 34.01/18.19 bnd_c4_2 = % 34.01/18.19 (\<lambda>x. _) % 34.01/18.19 (i1 := (\<lambda>x. _)(i1 := True, i2 := False), % 34.01/18.19 i2 := (\<lambda>x. _)(i1 := True, i2 := False)) % 34.01/18.19 bnd_c5_0 = False % 34.01/18.19 bnd_c5_1 = (\<lambda>x. _)(i1 := True, i2 := False) % 34.01/18.19 bnd_c5_2 = % 34.01/18.19 (\<lambda>x. _) % 34.01/18.19 (i1 := (\<lambda>x. _)(i1 := True, i2 := False), % 34.01/18.19 i2 := (\<lambda>x. _)(i1 := True, i2 := False)) % 34.01/18.19 bnd_c6_0 = False % 34.01/18.19 bnd_c6_1 = (\<lambda>x. _)(i1 := True, i2 := False) % 34.01/18.19 bnd_c6_2 = % 34.01/18.19 (\<lambda>x. _) % 34.01/18.19 (i1 := (\<lambda>x. _)(i1 := True, i2 := True), % 34.01/18.19 i2 := (\<lambda>x. _)(i1 := False, i2 := True)) % 34.01/18.19 bnd_c7_0 = True % 34.01/18.19 bnd_c7_1 = (\<lambda>x. _)(i1 := True, i2 := False) % 34.01/18.19 bnd_c7_2 = % 34.01/18.19 (\<lambda>x. _) % 34.01/18.19 (i1 := (\<lambda>x. _)(i1 := False, i2 := True), % 34.01/18.19 i2 := (\<lambda>x. _)(i1 := False, i2 := True)) % 34.01/18.19 bnd_c8_0 = False % 34.01/18.19 bnd_c8_1 = (\<lambda>x. _)(i1 := False, i2 := False) % 34.01/18.19 bnd_c8_2 = % 34.01/18.19 (\<lambda>x. _) % 34.01/18.19 (i1 := (\<lambda>x. _)(i1 := True, i2 := True), % 34.01/18.19 i2 := (\<lambda>x. _)(i1 := True, i2 := False)) % 34.01/18.19 bnd_c9_0 = True % 34.01/18.19 bnd_c9_1 = (\<lambda>x. _)(i1 := True, i2 := False) % 34.01/18.19 bnd_c9_2 = % 34.01/18.19 (\<lambda>x. _) % 34.01/18.19 (i1 := (\<lambda>x. _)(i1 := False, i2 := True), % 34.01/18.19 i2 := (\<lambda>x. _)(i1 := True, i2 := False)) % 34.01/18.19 bnd_ndr1_0 = True % 34.01/18.19 bnd_ndr1_1 = (\<lambda>x. _)(i1 := True, i2 := True) % 34.01/18.19 bnd_ssSkC0 = True % 34.01/18.19 bnd_ssSkC1 = False % 34.01/18.19 bnd_ssSkC10 = True % 34.01/18.19 bnd_ssSkC11 = False % 34.01/18.19 bnd_ssSkC12 = True % 34.01/18.19 bnd_ssSkC13 = True % 34.01/18.19 bnd_ssSkC14 = True % 34.01/18.19 bnd_ssSkC15 = False % 34.01/18.19 bnd_ssSkC16 = False % 34.01/18.19 bnd_ssSkC17 = True % 34.01/18.19 bnd_ssSkC18 = True % 34.01/18.19 bnd_ssSkC19 = True % 34.01/18.19 bnd_ssSkC2 = True % 34.01/18.19 bnd_ssSkC20 = True % 34.01/18.19 bnd_ssSkC21 = False % 34.01/18.19 bnd_ssSkC22 = True % 34.01/18.19 bnd_ssSkC23 = False % 34.01/18.19 bnd_ssSkC24 = False % 34.01/18.19 bnd_ssSkC25 = True % 34.01/18.19 bnd_ssSkC26 = True % 34.01/18.19 bnd_ssSkC27 = True % 34.01/18.19 bnd_ssSkC28 = True % 34.01/18.19 bnd_ssSkC29 = False % 34.01/18.19 bnd_ssSkC3 = True % 34.01/18.19 bnd_ssSkC30 = True % 34.01/18.19 bnd_ssSkC31 = True % 34.01/18.19 bnd_ssSkC32 = False % 34.01/18.19 bnd_ssSkC33 = True % 34.01/18.19 bnd_ssSkC34 = False % 34.01/18.19 bnd_ssSkC35 = True % 34.01/18.19 bnd_ssSkC36 = True % 34.01/18.19 bnd_ssSkC37 = True % 34.01/18.19 bnd_ssSkC38 = True % 34.01/18.19 bnd_ssSkC39 = True % 34.01/18.19 bnd_ssSkC4 = True % 34.01/18.19 bnd_ssSkC40 = True % 34.01/18.19 bnd_ssSkC41 = False % 34.01/18.19 bnd_ssSkC42 = False % 34.01/18.19 bnd_ssSkC43 = True % 34.01/18.19 bnd_ssSkC44 = False % 34.01/18.19 bnd_ssSkC45 = False % 34.01/18.19 bnd_ssSkC46 = False % 34.01/18.19 bnd_ssSkC47 = True % 34.01/18.19 bnd_ssSkC48 = True % 34.01/18.19 bnd_ssSkC49 = False % 34.01/18.19 bnd_ssSkC5 = True % 34.01/18.19 bnd_ssSkC50 = True % 34.01/18.19 bnd_ssSkC51 = False % 34.01/18.19 bnd_ssSkC52 = True % 34.01/18.19 bnd_ssSkC53 = True % 34.01/18.19 bnd_ssSkC54 = False % 34.01/18.19 bnd_ssSkC55 = True % 34.01/18.19 bnd_ssSkC56 = True % 34.01/18.19 bnd_ssSkC57 = True % 34.01/18.19 bnd_ssSkC58 = True % 34.01/18.19 bnd_ssSkC6 = False % 34.01/18.19 bnd_ssSkC7 = True % 34.01/18.19 bnd_ssSkC8 = False % 34.01/18.19 bnd_ssSkC9 = False % 34.01/18.19 bnd_ssSkP0 = (\<lambda>x. _)(i1 := True, i2 := True) % 34.01/18.19 bnd_ssSkP1 = (\<lambda>x. _)(i1 := True, i2 := True) % 34.01/18.19 bnd_ssSkP10 = (\<lambda>x. _)(i1 := True, i2 := True) % 34.01/18.19 bnd_ssSkP11 = (\<lambda>x. _)(i1 := True, i2 := True) % 34.01/18.19 bnd_ssSkP12 = (\<lambda>x. _)(i1 := True, i2 := True) % 34.01/18.19 bnd_ssSkP13 = (\<lambda>x. _)(i1 := True, i2 := True) % 34.01/18.19 bnd_ssSkP14 = (\<lambda>x. _)(i1 := True, i2 := True) % 34.05/18.19 bnd_ssSkP15 = (\<lambda>x. _)(i1 := True, i2 := True) % 34.05/18.19 bnd_ssSkP16 = (\<lambda>x. _)(i1 := True, i2 := True) % 34.05/18.19 bnd_ssSkP2 = (\<lambda>x. _)(i1 := True, i2 := True) % 34.05/18.19 bnd_ssSkP3 = (\<lambda>x. _)(i1 := True, i2 := True) % 34.05/18.19 bnd_ssSkP4 = (\<lambda>x. _)(i1 := True, i2 := True) % 34.05/18.19 bnd_ssSkP5 = (\<lambda>x. _)(i1 := True, i2 := False) % 34.05/18.19 bnd_ssSkP6 = (\<lambda>x. _)(i1 := True, i2 := True) % 34.05/18.19 bnd_ssSkP7 = (\<lambda>x. _)(i1 := True, i2 := True) % 34.05/18.19 bnd_ssSkP8 = (\<lambda>x. _)(i1 := True, i2 := True) % 34.05/18.19 bnd_ssSkP9 = (\<lambda>x. _)(i1 := True, i2 := True) % 34.05/18.19 % SZS output end FiniteModel % 34.05/18.19 Total time: 8.5 s %------------------------------------------------------------------------------