%------------------------------------------------------------------------------
% File : Paradox---4.0
% Problem : SYN427-1 : TPTP v8.1.0. Released v2.1.0.
% Transfm : none
% Format : tptp:short
% Command : paradox --no-progress --time %d --tstp --model %s
% Computer : n024.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 09:47:17 EDT 2022
% Result : Satisfiable 0.62s 0.79s
% Output : FiniteModel 0.62s
% Verified :
% SZS Type : FiniteModel
% Domain size : 2
% Comments :
%------------------------------------------------------------------------------
% domain size is 2
fof(domain,fi_domain,
! [X] :
( X = "1"
| X = "2" ) ).
fof(a1581,fi_functors,
a1581 = "1" ).
fof(a1582,fi_functors,
a1582 = "1" ).
fof(a1583,fi_functors,
a1583 = "1" ).
fof(a1584,fi_functors,
a1584 = "1" ).
fof(a1585,fi_functors,
a1585 = "1" ).
fof(a1586,fi_functors,
a1586 = "2" ).
fof(a1587,fi_functors,
a1587 = "1" ).
fof(a1588,fi_functors,
a1588 = "2" ).
fof(a1589,fi_functors,
a1589 = "1" ).
fof(a1590,fi_functors,
a1590 = "1" ).
fof(a1593,fi_functors,
a1593 = "2" ).
fof(a1594,fi_functors,
a1594 = "2" ).
fof(a1595,fi_functors,
a1595 = "1" ).
fof(a1596,fi_functors,
a1596 = "2" ).
fof(a1597,fi_functors,
a1597 = "1" ).
fof(a1598,fi_functors,
a1598 = "1" ).
fof(a1599,fi_functors,
a1599 = "1" ).
fof(a1600,fi_functors,
a1600 = "1" ).
fof(a1601,fi_functors,
a1601 = "1" ).
fof(a1602,fi_functors,
a1602 = "1" ).
fof(a1603,fi_functors,
a1603 = "1" ).
fof(a1604,fi_functors,
a1604 = "1" ).
fof(a1605,fi_functors,
a1605 = "1" ).
fof(a1606,fi_functors,
a1606 = "1" ).
fof(a1607,fi_functors,
a1607 = "2" ).
fof(a1608,fi_functors,
a1608 = "2" ).
fof(a1609,fi_functors,
a1609 = "1" ).
fof(a1610,fi_functors,
a1610 = "2" ).
fof(a1611,fi_functors,
a1611 = "1" ).
fof(a1612,fi_functors,
a1612 = "2" ).
fof(a1613,fi_functors,
a1613 = "1" ).
fof(a1614,fi_functors,
a1614 = "1" ).
fof(a1615,fi_functors,
a1615 = "1" ).
fof(a1616,fi_functors,
a1616 = "1" ).
fof(a1617,fi_functors,
a1617 = "1" ).
fof(a1618,fi_functors,
a1618 = "2" ).
fof(a1619,fi_functors,
a1619 = "2" ).
fof(a1620,fi_functors,
a1620 = "2" ).
fof(a1621,fi_functors,
a1621 = "2" ).
fof(a1622,fi_functors,
a1622 = "1" ).
fof(a1623,fi_functors,
a1623 = "1" ).
fof(a1624,fi_functors,
a1624 = "1" ).
fof(a1625,fi_functors,
a1625 = "1" ).
fof(a1626,fi_functors,
a1626 = "1" ).
fof(a1627,fi_functors,
a1627 = "1" ).
fof(a1628,fi_functors,
a1628 = "1" ).
fof(a1629,fi_functors,
a1629 = "2" ).
fof(a1630,fi_functors,
a1630 = "2" ).
fof(a1631,fi_functors,
a1631 = "1" ).
fof(a1632,fi_functors,
a1632 = "2" ).
fof(a1633,fi_functors,
a1633 = "1" ).
fof(a1634,fi_functors,
a1634 = "1" ).
fof(a1635,fi_functors,
a1635 = "1" ).
fof(a1636,fi_functors,
a1636 = "1" ).
fof(a1637,fi_functors,
a1637 = "1" ).
fof(a1638,fi_functors,
a1638 = "1" ).
fof(a1639,fi_functors,
a1639 = "1" ).
fof(a1640,fi_functors,
a1640 = "1" ).
fof(a1641,fi_functors,
a1641 = "1" ).
fof(a1642,fi_functors,
a1642 = "1" ).
fof(a1643,fi_functors,
a1643 = "2" ).
fof(a1644,fi_functors,
a1644 = "1" ).
fof(a1645,fi_functors,
a1645 = "2" ).
fof(a1646,fi_functors,
a1646 = "2" ).
fof(a1647,fi_functors,
a1647 = "2" ).
fof(a1648,fi_functors,
a1648 = "1" ).
fof(a1649,fi_functors,
a1649 = "2" ).
fof(a1650,fi_functors,
a1650 = "2" ).
fof(a1651,fi_functors,
a1651 = "1" ).
fof(a1652,fi_functors,
a1652 = "1" ).
fof(a1653,fi_functors,
a1653 = "2" ).
fof(a1654,fi_functors,
a1654 = "1" ).
fof(a1655,fi_functors,
a1655 = "1" ).
fof(a1656,fi_functors,
a1656 = "1" ).
fof(a1657,fi_functors,
a1657 = "1" ).
fof(a1658,fi_functors,
a1658 = "2" ).
fof(a1659,fi_functors,
a1659 = "2" ).
fof(a1660,fi_functors,
a1660 = "2" ).
fof(a1661,fi_functors,
a1661 = "1" ).
fof(a1662,fi_functors,
a1662 = "1" ).
fof(a1663,fi_functors,
a1663 = "1" ).
fof(a1664,fi_functors,
a1664 = "1" ).
fof(a1665,fi_functors,
a1665 = "1" ).
fof(a1666,fi_functors,
a1666 = "2" ).
fof(a1667,fi_functors,
a1667 = "1" ).
fof(a1668,fi_functors,
a1668 = "2" ).
fof(a1672,fi_functors,
a1672 = "1" ).
fof(a1673,fi_functors,
a1673 = "1" ).
fof(a1674,fi_functors,
a1674 = "1" ).
fof(a1675,fi_functors,
a1675 = "1" ).
fof(a1676,fi_functors,
a1676 = "2" ).
fof(a1677,fi_functors,
a1677 = "2" ).
fof(a1678,fi_functors,
a1678 = "2" ).
fof(a1679,fi_functors,
a1679 = "1" ).
fof(a1680,fi_functors,
a1680 = "2" ).
fof(a1681,fi_functors,
a1681 = "2" ).
fof(a1682,fi_functors,
a1682 = "2" ).
fof(a1683,fi_functors,
a1683 = "1" ).
fof(a1684,fi_functors,
a1684 = "2" ).
fof(a1685,fi_functors,
a1685 = "1" ).
fof(a1686,fi_functors,
a1686 = "1" ).
fof(a1688,fi_functors,
a1688 = "2" ).
fof(a1689,fi_functors,
a1689 = "1" ).
fof(a1690,fi_functors,
a1690 = "2" ).
fof(a1691,fi_functors,
a1691 = "2" ).
fof(a1692,fi_functors,
a1692 = "2" ).
fof(a1693,fi_functors,
a1693 = "1" ).
fof(a1694,fi_functors,
a1694 = "2" ).
fof(a1695,fi_functors,
a1695 = "2" ).
fof(a1696,fi_functors,
a1696 = "1" ).
fof(a1697,fi_functors,
a1697 = "1" ).
fof(a1698,fi_functors,
a1698 = "1" ).
fof(a1699,fi_functors,
a1699 = "1" ).
fof(a1700,fi_functors,
a1700 = "1" ).
fof(a1701,fi_functors,
a1701 = "1" ).
fof(a1702,fi_functors,
a1702 = "1" ).
fof(a1703,fi_functors,
a1703 = "2" ).
fof(a1704,fi_functors,
a1704 = "2" ).
fof(a1705,fi_functors,
a1705 = "1" ).
fof(a1706,fi_functors,
a1706 = "1" ).
fof(a1707,fi_functors,
a1707 = "1" ).
fof(a1708,fi_functors,
a1708 = "1" ).
fof(a1709,fi_functors,
a1709 = "1" ).
fof(a1710,fi_functors,
a1710 = "1" ).
fof(a1711,fi_functors,
a1711 = "1" ).
fof(a1712,fi_functors,
a1712 = "1" ).
fof(a1713,fi_functors,
a1713 = "1" ).
fof(a1714,fi_functors,
a1714 = "1" ).
fof(a1715,fi_functors,
a1715 = "1" ).
fof(a1716,fi_functors,
a1716 = "1" ).
fof(a1717,fi_functors,
a1717 = "2" ).
fof(a1718,fi_functors,
a1718 = "1" ).
fof(a1719,fi_functors,
a1719 = "1" ).
fof(a1720,fi_functors,
a1720 = "1" ).
fof(a1721,fi_functors,
a1721 = "1" ).
fof(a1722,fi_functors,
a1722 = "1" ).
fof(a1723,fi_functors,
a1723 = "1" ).
fof(a1724,fi_functors,
a1724 = "1" ).
fof(a1725,fi_functors,
a1725 = "1" ).
fof(a1726,fi_functors,
a1726 = "1" ).
fof(a1727,fi_functors,
a1727 = "2" ).
fof(a1728,fi_functors,
a1728 = "1" ).
fof(a1729,fi_functors,
a1729 = "2" ).
fof(a1730,fi_functors,
a1730 = "2" ).
fof(a1731,fi_functors,
a1731 = "1" ).
fof(a1732,fi_functors,
a1732 = "1" ).
fof(a1733,fi_functors,
a1733 = "1" ).
fof(a1734,fi_functors,
a1734 = "1" ).
fof(a1735,fi_functors,
a1735 = "1" ).
fof(a1736,fi_functors,
a1736 = "2" ).
fof(a1737,fi_functors,
a1737 = "1" ).
fof(a1738,fi_functors,
a1738 = "1" ).
fof(a1739,fi_functors,
a1739 = "1" ).
fof(a1740,fi_functors,
a1740 = "1" ).
fof(a1741,fi_functors,
a1741 = "2" ).
fof(a1742,fi_functors,
a1742 = "1" ).
fof(a1743,fi_functors,
a1743 = "1" ).
fof(a1744,fi_functors,
a1744 = "1" ).
fof(a1745,fi_functors,
a1745 = "1" ).
fof(a1746,fi_functors,
a1746 = "2" ).
fof(a1747,fi_functors,
a1747 = "1" ).
fof(a1748,fi_functors,
a1748 = "1" ).
fof(a1749,fi_functors,
a1749 = "2" ).
fof(a1750,fi_functors,
a1750 = "1" ).
fof(a1751,fi_functors,
a1751 = "2" ).
fof(a1752,fi_functors,
a1752 = "1" ).
fof(a1753,fi_functors,
a1753 = "1" ).
fof(a1754,fi_functors,
a1754 = "1" ).
fof(a1755,fi_functors,
a1755 = "2" ).
fof(a1756,fi_functors,
a1756 = "1" ).
fof(a1757,fi_functors,
a1757 = "1" ).
fof(a1758,fi_functors,
a1758 = "1" ).
fof(a1759,fi_functors,
a1759 = "1" ).
fof(a1760,fi_functors,
a1760 = "1" ).
fof(a1761,fi_functors,
a1761 = "2" ).
fof(a1762,fi_functors,
a1762 = "1" ).
fof(a1763,fi_functors,
a1763 = "1" ).
fof(a1764,fi_functors,
a1764 = "1" ).
fof(a1765,fi_functors,
a1765 = "1" ).
fof(a1767,fi_functors,
a1767 = "1" ).
fof(a1768,fi_functors,
a1768 = "1" ).
fof(a1769,fi_functors,
a1769 = "1" ).
fof(a1770,fi_functors,
a1770 = "1" ).
fof(a1771,fi_functors,
a1771 = "1" ).
fof(a1772,fi_functors,
a1772 = "1" ).
fof(a1773,fi_functors,
a1773 = "1" ).
fof(a1774,fi_functors,
a1774 = "1" ).
fof(a1775,fi_functors,
a1775 = "1" ).
fof(a1776,fi_functors,
a1776 = "1" ).
fof(a1777,fi_functors,
a1777 = "1" ).
fof(a1778,fi_functors,
a1778 = "1" ).
fof(a1779,fi_functors,
a1779 = "1" ).
fof(a1780,fi_functors,
a1780 = "2" ).
fof(a1781,fi_functors,
a1781 = "1" ).
fof(a1782,fi_functors,
a1782 = "1" ).
fof(a1783,fi_functors,
a1783 = "1" ).
fof(a1784,fi_functors,
a1784 = "2" ).
fof(a1785,fi_functors,
a1785 = "2" ).
fof(a1786,fi_functors,
a1786 = "2" ).
fof(a1787,fi_functors,
a1787 = "2" ).
fof(a1788,fi_functors,
a1788 = "2" ).
fof(a1789,fi_functors,
a1789 = "1" ).
fof(a1790,fi_functors,
a1790 = "1" ).
fof(a1791,fi_functors,
a1791 = "1" ).
fof(a1792,fi_functors,
a1792 = "2" ).
fof(a1793,fi_functors,
a1793 = "2" ).
fof(a1794,fi_functors,
a1794 = "2" ).
fof(a1795,fi_functors,
a1795 = "1" ).
fof(a1796,fi_functors,
a1796 = "1" ).
fof(a1797,fi_functors,
a1797 = "2" ).
fof(a1798,fi_functors,
a1798 = "2" ).
fof(a1799,fi_functors,
a1799 = "1" ).
fof(a1800,fi_functors,
a1800 = "1" ).
fof(a1801,fi_functors,
a1801 = "2" ).
fof(a1802,fi_functors,
a1802 = "1" ).
fof(a1803,fi_functors,
a1803 = "1" ).
fof(a1804,fi_functors,
a1804 = "1" ).
fof(a1805,fi_functors,
a1805 = "1" ).
fof(a1806,fi_functors,
a1806 = "1" ).
fof(a1807,fi_functors,
a1807 = "1" ).
fof(a1808,fi_functors,
a1808 = "1" ).
fof(a1809,fi_functors,
a1809 = "1" ).
fof(a1810,fi_functors,
a1810 = "1" ).
fof(a1811,fi_functors,
a1811 = "1" ).
fof(a1812,fi_functors,
a1812 = "1" ).
fof(a1813,fi_functors,
a1813 = "2" ).
fof(a1814,fi_functors,
a1814 = "1" ).
fof(a1815,fi_functors,
a1815 = "1" ).
fof(a1817,fi_functors,
a1817 = "2" ).
fof(a1818,fi_functors,
a1818 = "1" ).
fof(a1819,fi_functors,
a1819 = "2" ).
fof(a1820,fi_functors,
a1820 = "2" ).
fof(a1821,fi_functors,
a1821 = "2" ).
fof(a1822,fi_functors,
a1822 = "1" ).
fof(a1823,fi_functors,
a1823 = "2" ).
fof(a1824,fi_functors,
a1824 = "1" ).
fof(a1825,fi_functors,
a1825 = "1" ).
fof(a1826,fi_functors,
a1826 = "1" ).
fof(a1827,fi_functors,
a1827 = "1" ).
fof(a1829,fi_functors,
a1829 = "1" ).
fof(a1830,fi_functors,
a1830 = "1" ).
fof(a1831,fi_functors,
a1831 = "1" ).
fof(a1832,fi_functors,
a1832 = "1" ).
fof(a1833,fi_functors,
a1833 = "1" ).
fof(c10_0,fi_predicates,
( c10_0
<=> $true ) ).
fof(c10_1,fi_predicates,
( ( c10_1("1")
<=> $true )
& ( c10_1("2")
<=> $true ) ) ).
fof(c10_2,fi_predicates,
( ( c10_2("1","1")
<=> $false )
& ( c10_2("1","2")
<=> $true )
& ( c10_2("2","1")
<=> $false )
& ( c10_2("2","2")
<=> $true ) ) ).
fof(c1_0,fi_predicates,
( c1_0
<=> $true ) ).
fof(c1_1,fi_predicates,
( ( c1_1("1")
<=> $false )
& ( c1_1("2")
<=> $false ) ) ).
fof(c1_2,fi_predicates,
( ( c1_2("1","1")
<=> $false )
& ( c1_2("1","2")
<=> $false )
& ( c1_2("2","1")
<=> $true )
& ( c1_2("2","2")
<=> $true ) ) ).
fof(c2_0,fi_predicates,
( c2_0
<=> $true ) ).
fof(c2_1,fi_predicates,
( ( c2_1("1")
<=> $false )
& ( c2_1("2")
<=> $false ) ) ).
fof(c2_2,fi_predicates,
( ( c2_2("1","1")
<=> $true )
& ( c2_2("1","2")
<=> $false )
& ( c2_2("2","1")
<=> $false )
& ( c2_2("2","2")
<=> $true ) ) ).
fof(c3_0,fi_predicates,
( c3_0
<=> $true ) ).
fof(c3_1,fi_predicates,
( ( c3_1("1")
<=> $false )
& ( c3_1("2")
<=> $true ) ) ).
fof(c3_2,fi_predicates,
( ( c3_2("1","1")
<=> $false )
& ( c3_2("1","2")
<=> $true )
& ( c3_2("2","1")
<=> $true )
& ( c3_2("2","2")
<=> $false ) ) ).
fof(c4_0,fi_predicates,
( c4_0
<=> $false ) ).
fof(c4_1,fi_predicates,
( ( c4_1("1")
<=> $true )
& ( c4_1("2")
<=> $false ) ) ).
fof(c4_2,fi_predicates,
( ( c4_2("1","1")
<=> $false )
& ( c4_2("1","2")
<=> $true )
& ( c4_2("2","1")
<=> $true )
& ( c4_2("2","2")
<=> $false ) ) ).
fof(c5_0,fi_predicates,
( c5_0
<=> $true ) ).
fof(c5_1,fi_predicates,
( ( c5_1("1")
<=> $false )
& ( c5_1("2")
<=> $true ) ) ).
fof(c5_2,fi_predicates,
( ( c5_2("1","1")
<=> $false )
& ( c5_2("1","2")
<=> $true )
& ( c5_2("2","1")
<=> $true )
& ( c5_2("2","2")
<=> $false ) ) ).
fof(c6_0,fi_predicates,
( c6_0
<=> $false ) ).
fof(c6_1,fi_predicates,
( ( c6_1("1")
<=> $true )
& ( c6_1("2")
<=> $false ) ) ).
fof(c6_2,fi_predicates,
( ( c6_2("1","1")
<=> $true )
& ( c6_2("1","2")
<=> $false )
& ( c6_2("2","1")
<=> $true )
& ( c6_2("2","2")
<=> $true ) ) ).
fof(c7_0,fi_predicates,
( c7_0
<=> $true ) ).
fof(c7_1,fi_predicates,
( ( c7_1("1")
<=> $false )
& ( c7_1("2")
<=> $true ) ) ).
fof(c7_2,fi_predicates,
( ( c7_2("1","1")
<=> $true )
& ( c7_2("1","2")
<=> $false )
& ( c7_2("2","1")
<=> $true )
& ( c7_2("2","2")
<=> $true ) ) ).
fof(c8_0,fi_predicates,
( c8_0
<=> $false ) ).
fof(c8_1,fi_predicates,
( ( c8_1("1")
<=> $true )
& ( c8_1("2")
<=> $true ) ) ).
fof(c8_2,fi_predicates,
( ( c8_2("1","1")
<=> $true )
& ( c8_2("1","2")
<=> $false )
& ( c8_2("2","1")
<=> $true )
& ( c8_2("2","2")
<=> $false ) ) ).
fof(c9_0,fi_predicates,
( c9_0
<=> $true ) ).
fof(c9_1,fi_predicates,
( ( c9_1("1")
<=> $false )
& ( c9_1("2")
<=> $true ) ) ).
fof(c9_2,fi_predicates,
( ( c9_2("1","1")
<=> $true )
& ( c9_2("1","2")
<=> $false )
& ( c9_2("2","1")
<=> $false )
& ( c9_2("2","2")
<=> $true ) ) ).
fof(ndr1_0,fi_predicates,
( ndr1_0
<=> $true ) ).
fof(ndr1_1,fi_predicates,
( ( ndr1_1("1")
<=> $true )
& ( ndr1_1("2")
<=> $true ) ) ).
fof(ssSkC0,fi_predicates,
( ssSkC0
<=> $true ) ).
fof(ssSkC1,fi_predicates,
( ssSkC1
<=> $false ) ).
fof(ssSkC10,fi_predicates,
( ssSkC10
<=> $true ) ).
fof(ssSkC11,fi_predicates,
( ssSkC11
<=> $true ) ).
fof(ssSkC12,fi_predicates,
( ssSkC12
<=> $false ) ).
fof(ssSkC13,fi_predicates,
( ssSkC13
<=> $true ) ).
fof(ssSkC14,fi_predicates,
( ssSkC14
<=> $true ) ).
fof(ssSkC15,fi_predicates,
( ssSkC15
<=> $false ) ).
fof(ssSkC16,fi_predicates,
( ssSkC16
<=> $true ) ).
fof(ssSkC17,fi_predicates,
( ssSkC17
<=> $false ) ).
fof(ssSkC18,fi_predicates,
( ssSkC18
<=> $true ) ).
fof(ssSkC19,fi_predicates,
( ssSkC19
<=> $false ) ).
fof(ssSkC2,fi_predicates,
( ssSkC2
<=> $true ) ).
fof(ssSkC20,fi_predicates,
( ssSkC20
<=> $true ) ).
fof(ssSkC21,fi_predicates,
( ssSkC21
<=> $true ) ).
fof(ssSkC22,fi_predicates,
( ssSkC22
<=> $true ) ).
fof(ssSkC23,fi_predicates,
( ssSkC23
<=> $true ) ).
fof(ssSkC24,fi_predicates,
( ssSkC24
<=> $true ) ).
fof(ssSkC25,fi_predicates,
( ssSkC25
<=> $false ) ).
fof(ssSkC26,fi_predicates,
( ssSkC26
<=> $true ) ).
fof(ssSkC27,fi_predicates,
( ssSkC27
<=> $true ) ).
fof(ssSkC28,fi_predicates,
( ssSkC28
<=> $false ) ).
fof(ssSkC29,fi_predicates,
( ssSkC29
<=> $false ) ).
fof(ssSkC3,fi_predicates,
( ssSkC3
<=> $true ) ).
fof(ssSkC30,fi_predicates,
( ssSkC30
<=> $true ) ).
fof(ssSkC31,fi_predicates,
( ssSkC31
<=> $true ) ).
fof(ssSkC32,fi_predicates,
( ssSkC32
<=> $false ) ).
fof(ssSkC33,fi_predicates,
( ssSkC33
<=> $true ) ).
fof(ssSkC34,fi_predicates,
( ssSkC34
<=> $false ) ).
fof(ssSkC35,fi_predicates,
( ssSkC35
<=> $true ) ).
fof(ssSkC36,fi_predicates,
( ssSkC36
<=> $true ) ).
fof(ssSkC37,fi_predicates,
( ssSkC37
<=> $true ) ).
fof(ssSkC38,fi_predicates,
( ssSkC38
<=> $true ) ).
fof(ssSkC39,fi_predicates,
( ssSkC39
<=> $false ) ).
fof(ssSkC4,fi_predicates,
( ssSkC4
<=> $false ) ).
fof(ssSkC40,fi_predicates,
( ssSkC40
<=> $false ) ).
fof(ssSkC41,fi_predicates,
( ssSkC41
<=> $true ) ).
fof(ssSkC42,fi_predicates,
( ssSkC42
<=> $true ) ).
fof(ssSkC43,fi_predicates,
( ssSkC43
<=> $true ) ).
fof(ssSkC44,fi_predicates,
( ssSkC44
<=> $false ) ).
fof(ssSkC45,fi_predicates,
( ssSkC45
<=> $false ) ).
fof(ssSkC46,fi_predicates,
( ssSkC46
<=> $true ) ).
fof(ssSkC47,fi_predicates,
( ssSkC47
<=> $true ) ).
fof(ssSkC48,fi_predicates,
( ssSkC48
<=> $false ) ).
fof(ssSkC49,fi_predicates,
( ssSkC49
<=> $true ) ).
fof(ssSkC5,fi_predicates,
( ssSkC5
<=> $true ) ).
fof(ssSkC50,fi_predicates,
( ssSkC50
<=> $false ) ).
fof(ssSkC51,fi_predicates,
( ssSkC51
<=> $false ) ).
fof(ssSkC52,fi_predicates,
( ssSkC52
<=> $true ) ).
fof(ssSkC53,fi_predicates,
( ssSkC53
<=> $false ) ).
fof(ssSkC54,fi_predicates,
( ssSkC54
<=> $true ) ).
fof(ssSkC55,fi_predicates,
( ssSkC55
<=> $false ) ).
fof(ssSkC56,fi_predicates,
( ssSkC56
<=> $true ) ).
fof(ssSkC57,fi_predicates,
( ssSkC57
<=> $true ) ).
fof(ssSkC58,fi_predicates,
( ssSkC58
<=> $true ) ).
fof(ssSkC6,fi_predicates,
( ssSkC6
<=> $true ) ).
fof(ssSkC7,fi_predicates,
( ssSkC7
<=> $true ) ).
fof(ssSkC8,fi_predicates,
( ssSkC8
<=> $false ) ).
fof(ssSkC9,fi_predicates,
( ssSkC9
<=> $false ) ).
fof(ssSkP0,fi_predicates,
( ( ssSkP0("1")
<=> $true )
& ( ssSkP0("2")
<=> $true ) ) ).
fof(ssSkP1,fi_predicates,
( ( ssSkP1("1")
<=> $true )
& ( ssSkP1("2")
<=> $true ) ) ).
fof(ssSkP10,fi_predicates,
( ( ssSkP10("1")
<=> $true )
& ( ssSkP10("2")
<=> $true ) ) ).
fof(ssSkP11,fi_predicates,
( ( ssSkP11("1")
<=> $true )
& ( ssSkP11("2")
<=> $true ) ) ).
fof(ssSkP12,fi_predicates,
( ( ssSkP12("1")
<=> $true )
& ( ssSkP12("2")
<=> $true ) ) ).
fof(ssSkP13,fi_predicates,
( ( ssSkP13("1")
<=> $true )
& ( ssSkP13("2")
<=> $false ) ) ).
fof(ssSkP14,fi_predicates,
( ( ssSkP14("1")
<=> $false )
& ( ssSkP14("2")
<=> $true ) ) ).
fof(ssSkP15,fi_predicates,
( ( ssSkP15("1")
<=> $true )
& ( ssSkP15("2")
<=> $true ) ) ).
fof(ssSkP16,fi_predicates,
( ( ssSkP16("1")
<=> $true )
& ( ssSkP16("2")
<=> $true ) ) ).
fof(ssSkP2,fi_predicates,
( ( ssSkP2("1")
<=> $true )
& ( ssSkP2("2")
<=> $true ) ) ).
fof(ssSkP3,fi_predicates,
( ( ssSkP3("1")
<=> $true )
& ( ssSkP3("2")
<=> $true ) ) ).
fof(ssSkP4,fi_predicates,
( ( ssSkP4("1")
<=> $true )
& ( ssSkP4("2")
<=> $true ) ) ).
fof(ssSkP5,fi_predicates,
( ( ssSkP5("1")
<=> $true )
& ( ssSkP5("2")
<=> $true ) ) ).
fof(ssSkP6,fi_predicates,
( ( ssSkP6("1")
<=> $false )
& ( ssSkP6("2")
<=> $false ) ) ).
fof(ssSkP7,fi_predicates,
( ( ssSkP7("1")
<=> $true )
& ( ssSkP7("2")
<=> $true ) ) ).
fof(ssSkP8,fi_predicates,
( ( ssSkP8("1")
<=> $true )
& ( ssSkP8("2")
<=> $true ) ) ).
fof(ssSkP9,fi_predicates,
( ( ssSkP9("1")
<=> $true )
& ( ssSkP9("2")
<=> $true ) ) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.13 % Problem : SYN427-1 : TPTP v8.1.0. Released v2.1.0.
% 0.07/0.13 % Command : paradox --no-progress --time %d --tstp --model %s
% 0.13/0.35 % Computer : n024.cluster.edu
% 0.13/0.35 % Model : x86_64 x86_64
% 0.13/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.35 % Memory : 8042.1875MB
% 0.13/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.35 % CPULimit : 300
% 0.13/0.35 % WCLimit : 600
% 0.13/0.35 % DateTime : Mon Jul 11 19:21:13 EDT 2022
% 0.13/0.35 % CPUTime :
% 0.13/0.35 Paradox, version 4.0, 2010-06-29.
% 0.13/0.35 +++ PROBLEM: /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.13/0.35 Reading '/export/starexec/sandbox/benchmark/theBenchmark.p' ... OK
% 0.21/0.50 +++ SOLVING: /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.62/0.78 +++ BEGIN MODEL
% 0.62/0.78 SZS output start FiniteModel for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
% 0.62/0.79 +++ END MODEL
% 0.62/0.79 +++ RESULT: Satisfiable
% 0.62/0.79 SZS status Satisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------