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