%------------------------------------------------------------------------------ % File : Beagle---0.9.52 % Problem : SWV499-1.050 : TPTP v9.0.0. Released v4.0.0. % Transfm : none % Format : tptp:raw % Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s % Computer : n004.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 : 300s % DateTime : Thu Apr 10 02:51:32 AM UTC 2025 % Result : Satisfiable 7.59s 2.88s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.13 % Problem : SWV499-1.050 : TPTP v9.0.0. Released v4.0.0. % 0.03/0.13 % Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s % 0.14/0.35 % Computer : n004.cluster.edu % 0.14/0.35 % Model : x86_64 x86_64 % 0.14/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.14/0.35 % Memory : 8042.1875MB % 0.14/0.35 % OS : Linux 3.10.0-693.el7.x86_64 % 0.14/0.35 % CPULimit : 300 % 0.14/0.35 % WCLimit : 300 % 0.14/0.35 % DateTime : Wed Apr 9 22:24:52 EDT 2025 % 0.14/0.35 % CPUTime : % 7.59/2.88 % 7.59/2.88 % SZS status Satisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p % 7.59/2.88 % 7.59/2.88 % SZS output start Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 7.59/2.89 %$ store > select > #nlpp > n9 > n8 > n7 > n6 > n50 > n5 > n49 > n48 > n47 > n46 > n45 > n44 > n43 > n42 > n41 > n40 > n4 > n39 > n38 > n37 > n36 > n35 > n34 > n33 > n32 > n31 > n30 > n3 > n29 > n28 > n27 > n26 > n25 > n24 > n23 > n22 > n21 > n20 > n2 > n19 > n18 > n17 > n16 > n15 > n14 > n13 > n12 > n11 > n10 > n1 > e9 > e8 > e7 > e6 > e50 > e5 > e49 > e48 > e47 > e46 > e45 > e44 > e43 > e42 > e41 > e40 > e4 > e39 > e38 > e37 > e36 > e35 > e34 > e33 > e32 > e31 > e30 > e3 > e29 > e28 > e27 > e26 > e25 > e24 > e23 > e22 > e21 > e20 > e2 > e19 > e18 > e17 > e16 > e15 > e14 > e13 > e12 > e11 > e10 > e1 > a_1799 > a_1798 > a_1797 > a_1796 > a_1795 > a_1794 > a_1793 > a_1792 > a_1791 > a_1790 > a_1789 > a_1788 > a_1787 > a_1786 > a_1785 > a_1784 > a_1783 > a_1782 > a_1781 > a_1780 > a_1779 > a_1778 > a_1777 > a_1776 > a_1775 > a_1774 > a_1773 > a_1772 > a_1771 > a_1770 > a_1769 > a_1768 > a_1767 > a_1766 > a_1765 > a_1764 > a_1763 > a_1762 > a_1761 > a_1760 > a_1759 > a_1758 > a_1757 > a_1756 > a_1755 > a_1754 > a_1753 > a_1752 > a_1751 > a_1750 > a_1749 > a_1748 > a_1747 > a_1746 > a_1745 > a_1744 > a_1743 > a_1742 > a_1741 > a_1740 > a_1739 > a_1738 > a_1737 > a_1736 > a_1735 > a_1734 > a_1733 > a_1732 > a_1731 > a_1730 > a_1729 > a_1728 > a_1727 > a_1726 > a_1725 > a_1724 > a_1723 > a_1722 > a_1721 > a_1720 > a_1719 > a_1718 > a_1717 > a_1716 > a_1715 > a_1714 > a_1713 > a_1712 > a_1711 > a_1710 > a_1709 > a_1708 > a_1707 > a_1706 > a_1705 > a_1704 > a_1703 > a_1702 > a_1701 > a_1700 > a1 % 7.59/2.89 % 7.59/2.89 %Foreground sorts: % 7.59/2.89 % 7.59/2.89 % 7.59/2.89 %Background operators: % 7.59/2.89 % 7.59/2.89 % 7.59/2.89 %Foreground operators: % 7.59/2.89 tff(e29, type, e29: $i). % 7.59/2.89 tff(a_1742, type, a_1742: $i). % 7.59/2.89 tff(a_1789, type, a_1789: $i). % 7.59/2.89 tff(a1, type, a1: $i). % 7.59/2.89 tff(e43, type, e43: $i). % 7.59/2.89 tff(a_1772, type, a_1772: $i). % 7.59/2.89 tff(n22, type, n22: $i). % 7.59/2.89 tff(a_1737, type, a_1737: $i). % 7.59/2.89 tff(n27, type, n27: $i). % 7.59/2.89 tff(n16, type, n16: $i). % 7.59/2.89 tff(a_1769, type, a_1769: $i). % 7.59/2.89 tff(n12, type, n12: $i). % 7.59/2.89 tff(e1, type, e1: $i). % 7.59/2.89 tff(a_1725, type, a_1725: $i). % 7.59/2.89 tff(a_1760, type, a_1760: $i). % 7.59/2.89 tff(a_1723, type, a_1723: $i). % 7.59/2.89 tff(e8, type, e8: $i). % 7.59/2.89 tff(a_1706, type, a_1706: $i). % 7.59/2.89 tff(a_1775, type, a_1775: $i). % 7.59/2.89 tff(e21, type, e21: $i). % 7.59/2.89 tff(n24, type, n24: $i). % 7.59/2.89 tff(a_1741, type, a_1741: $i). % 7.59/2.89 tff(a_1715, type, a_1715: $i). % 7.59/2.89 tff(a_1758, type, a_1758: $i). % 7.59/2.89 tff(a_1768, type, a_1768: $i). % 7.59/2.89 tff(e15, type, e15: $i). % 7.59/2.89 tff(a_1774, type, a_1774: $i). % 7.59/2.89 tff(n42, type, n42: $i). % 7.59/2.89 tff(a_1712, type, a_1712: $i). % 7.59/2.89 tff(a_1776, type, a_1776: $i). % 7.59/2.89 tff(e33, type, e33: $i). % 7.59/2.89 tff(a_1752, type, a_1752: $i). % 7.59/2.89 tff(n35, type, n35: $i). % 7.59/2.89 tff(e50, type, e50: $i). % 7.59/2.89 tff(a_1786, type, a_1786: $i). % 7.59/2.89 tff(a_1765, type, a_1765: $i). % 7.59/2.89 tff(a_1707, type, a_1707: $i). % 7.59/2.89 tff(e40, type, e40: $i). % 7.59/2.89 tff(a_1730, type, a_1730: $i). % 7.59/2.89 tff(e18, type, e18: $i). % 7.59/2.89 tff(a_1756, type, a_1756: $i). % 7.59/2.89 tff(e38, type, e38: $i). % 7.59/2.89 tff(e24, type, e24: $i). % 7.59/2.89 tff(e31, type, e31: $i). % 7.59/2.89 tff(n33, type, n33: $i). % 7.59/2.89 tff(n36, type, n36: $i). % 7.59/2.89 tff(e39, type, e39: $i). % 7.59/2.89 tff(e48, type, e48: $i). % 7.59/2.89 tff(a_1762, type, a_1762: $i). % 7.59/2.89 tff(a_1749, type, a_1749: $i). % 7.59/2.89 tff(store, type, store: ($i * $i * $i) > $i). % 7.59/2.89 tff(a_1782, type, a_1782: $i). % 7.59/2.89 tff(n23, type, n23: $i). % 7.59/2.89 tff(n8, type, n8: $i). % 7.59/2.89 tff(a_1793, type, a_1793: $i). % 7.59/2.89 tff(e20, type, e20: $i). % 7.59/2.89 tff(e41, type, e41: $i). % 7.59/2.89 tff(e19, type, e19: $i). % 7.59/2.89 tff(a_1746, type, a_1746: $i). % 7.59/2.89 tff(e16, type, e16: $i). % 7.59/2.89 tff(n30, type, n30: $i). % 7.59/2.89 tff(a_1744, type, a_1744: $i). % 7.59/2.89 tff(e35, type, e35: $i). % 7.59/2.89 tff(a_1797, type, a_1797: $i). % 7.59/2.89 tff(e2, type, e2: $i). % 7.59/2.89 tff(n28, type, n28: $i). % 7.59/2.89 tff(n9, type, n9: $i). % 7.59/2.89 tff(a_1703, type, a_1703: $i). % 7.59/2.89 tff(a_1792, type, a_1792: $i). % 7.59/2.89 tff(a_1781, type, a_1781: $i). % 7.59/2.89 tff(a_1770, type, a_1770: $i). % 7.59/2.89 tff(e42, type, e42: $i). % 7.59/2.89 tff(a_1713, type, a_1713: $i). % 7.59/2.89 tff(e37, type, e37: $i). % 7.59/2.89 tff(e13, type, e13: $i). % 7.59/2.89 tff(n3, type, n3: $i). % 7.59/2.89 tff(e32, type, e32: $i). % 7.59/2.89 tff(e22, type, e22: $i). % 7.59/2.89 tff(a_1720, type, a_1720: $i). % 7.59/2.89 tff(n46, type, n46: $i). % 7.59/2.89 tff(a_1796, type, a_1796: $i). % 7.59/2.89 tff(n48, type, n48: $i). % 7.59/2.89 tff(n39, type, n39: $i). % 7.59/2.89 tff(a_1754, type, a_1754: $i). % 7.59/2.89 tff(e34, type, e34: $i). % 7.59/2.89 tff(a_1729, type, a_1729: $i). % 7.59/2.89 tff(n1, type, n1: $i). % 7.59/2.89 tff(a_1764, type, a_1764: $i). % 7.59/2.89 tff(n29, type, n29: $i). % 7.59/2.89 tff(e9, type, e9: $i). % 7.59/2.89 tff(a_1704, type, a_1704: $i). % 7.59/2.89 tff(n37, type, n37: $i). % 7.59/2.89 tff(a_1710, type, a_1710: $i). % 7.59/2.89 tff(n44, type, n44: $i). % 7.59/2.89 tff(n50, type, n50: $i). % 7.59/2.89 tff(a_1717, type, a_1717: $i). % 7.59/2.89 tff(n7, type, n7: $i). % 7.59/2.89 tff(e25, type, e25: $i). % 7.59/2.89 tff(a_1714, type, a_1714: $i). % 7.59/2.89 tff(e26, type, e26: $i). % 7.59/2.89 tff(n6, type, n6: $i). % 7.59/2.89 tff(a_1753, type, a_1753: $i). % 7.59/2.89 tff(a_1784, type, a_1784: $i). % 7.59/2.89 tff(e17, type, e17: $i). % 7.59/2.89 tff(n26, type, n26: $i). % 7.59/2.89 tff(e27, type, e27: $i). % 7.59/2.89 tff(a_1750, type, a_1750: $i). % 7.59/2.89 tff(a_1731, type, a_1731: $i). % 7.59/2.89 tff(a_1757, type, a_1757: $i). % 7.59/2.89 tff(e10, type, e10: $i). % 7.59/2.89 tff(e7, type, e7: $i). % 7.59/2.89 tff(a_1773, type, a_1773: $i). % 7.59/2.89 tff(a_1767, type, a_1767: $i). % 7.59/2.89 tff(n13, type, n13: $i). % 7.59/2.89 tff(a_1738, type, a_1738: $i). % 7.59/2.89 tff(a_1787, type, a_1787: $i). % 7.59/2.89 tff(a_1709, type, a_1709: $i). % 7.59/2.89 tff(a_1771, type, a_1771: $i). % 7.59/2.89 tff(a_1728, type, a_1728: $i). % 7.59/2.89 tff(a_1785, type, a_1785: $i). % 7.59/2.89 tff(a_1727, type, a_1727: $i). % 7.59/2.89 tff(a_1778, type, a_1778: $i). % 7.59/2.89 tff(e36, type, e36: $i). % 7.59/2.89 tff(a_1795, type, a_1795: $i). % 7.59/2.89 tff(a_1718, type, a_1718: $i). % 7.59/2.89 tff(a_1761, type, a_1761: $i). % 7.59/2.89 tff(a_1745, type, a_1745: $i). % 7.59/2.89 tff(n4, type, n4: $i). % 7.59/2.89 tff(n10, type, n10: $i). % 7.59/2.89 tff(n14, type, n14: $i). % 7.59/2.89 tff(a_1719, type, a_1719: $i). % 7.59/2.89 tff(a_1777, type, a_1777: $i). % 7.59/2.89 tff(e45, type, e45: $i). % 7.59/2.89 tff(a_1726, type, a_1726: $i). % 7.59/2.89 tff(a_1755, type, a_1755: $i). % 7.59/2.89 tff(n15, type, n15: $i). % 7.59/2.89 tff(a_1759, type, a_1759: $i). % 7.59/2.89 tff(a_1700, type, a_1700: $i). % 7.59/2.89 tff(n17, type, n17: $i). % 7.59/2.89 tff(n40, type, n40: $i). % 7.59/2.89 tff(a_1763, type, a_1763: $i). % 7.59/2.89 tff(e30, type, e30: $i). % 7.59/2.89 tff(select, type, select: ($i * $i) > $i). % 7.59/2.89 tff(a_1734, type, a_1734: $i). % 7.59/2.89 tff(a_1780, type, a_1780: $i). % 7.59/2.89 tff(e49, type, e49: $i). % 7.59/2.89 tff(a_1779, type, a_1779: $i). % 7.59/2.89 tff(a_1705, type, a_1705: $i). % 7.59/2.89 tff(a_1794, type, a_1794: $i). % 7.59/2.89 tff(n31, type, n31: $i). % 7.59/2.89 tff(a_1722, type, a_1722: $i). % 7.59/2.89 tff(e47, type, e47: $i). % 7.59/2.89 tff(n49, type, n49: $i). % 7.59/2.89 tff(a_1740, type, a_1740: $i). % 7.59/2.89 tff(a_1798, type, a_1798: $i). % 7.59/2.89 tff(n47, type, n47: $i). % 7.59/2.89 tff(n32, type, n32: $i). % 7.59/2.89 tff(a_1751, type, a_1751: $i). % 7.59/2.89 tff(a_1735, type, a_1735: $i). % 7.59/2.89 tff(n20, type, n20: $i). % 7.59/2.89 tff(e23, type, e23: $i). % 7.59/2.89 tff(n18, type, n18: $i). % 7.59/2.89 tff(n38, type, n38: $i). % 7.59/2.89 tff(e14, type, e14: $i). % 7.59/2.89 tff(n11, type, n11: $i). % 7.59/2.89 tff(e12, type, e12: $i). % 7.59/2.89 tff(e4, type, e4: $i). % 7.59/2.89 tff(n45, type, n45: $i). % 7.59/2.89 tff(a_1747, type, a_1747: $i). % 7.59/2.89 tff(n34, type, n34: $i). % 7.59/2.89 tff(a_1739, type, a_1739: $i). % 7.59/2.89 tff(a_1766, type, a_1766: $i). % 7.59/2.89 tff(a_1748, type, a_1748: $i). % 7.59/2.89 tff(a_1716, type, a_1716: $i). % 7.59/2.89 tff(a_1799, type, a_1799: $i). % 7.59/2.89 tff(a_1732, type, a_1732: $i). % 7.59/2.89 tff(a_1788, type, a_1788: $i). % 7.59/2.89 tff(e6, type, e6: $i). % 7.59/2.89 tff(e46, type, e46: $i). % 7.59/2.89 tff(a_1711, type, a_1711: $i). % 7.59/2.89 tff(a_1724, type, a_1724: $i). % 7.59/2.89 tff(n19, type, n19: $i). % 7.59/2.89 tff(n2, type, n2: $i). % 7.59/2.89 tff(e11, type, e11: $i). % 7.59/2.89 tff(e28, type, e28: $i). % 7.59/2.89 tff(n5, type, n5: $i). % 7.59/2.89 tff(e44, type, e44: $i). % 7.59/2.89 tff(e3, type, e3: $i). % 7.59/2.89 tff(n43, type, n43: $i). % 7.59/2.89 tff(a_1736, type, a_1736: $i). % 7.59/2.89 tff(a_1721, type, a_1721: $i). % 7.59/2.89 tff(n25, type, n25: $i). % 7.59/2.89 tff(a_1708, type, a_1708: $i). % 7.59/2.89 tff(a_1702, type, a_1702: $i). % 7.59/2.89 tff(e5, type, e5: $i). % 7.59/2.89 tff(a_1701, type, a_1701: $i). % 7.59/2.89 tff(a_1743, type, a_1743: $i). % 7.59/2.89 tff(a_1791, type, a_1791: $i). % 7.59/2.89 tff(n21, type, n21: $i). % 7.59/2.89 tff(a_1790, type, a_1790: $i). % 7.59/2.89 tff(n41, type, n41: $i). % 7.59/2.89 tff(a_1783, type, a_1783: $i). % 7.59/2.89 tff(a_1733, type, a_1733: $i). % 7.59/2.89 % 7.59/2.89 %Saturated clause set: % 7.59/2.89 tff(c_1071, plain, (![J_14]: (select(a_1744, J_14)=select(a_1743, J_14) | n45=J_14))). % 7.59/2.89 tff(c_1155, plain, (![J_14]: (select(a_1790, J_14)=select(a_1789, J_14) | n3=J_14))). % 7.59/2.89 tff(c_1116, plain, (![J_14]: (select(a_1732, J_14)=select(a_1731, J_14) | n33=J_14))). % 7.59/2.90 tff(c_1110, plain, (![J_14]: (select(a_1734, J_14)=select(a_1733, J_14) | n35=J_14))). % 7.59/2.90 tff(c_1239, plain, (![J_14]: (select(a_1797, J_14)=select(a_1796, J_14) | n21=J_14))). % 7.59/2.90 tff(c_1005, plain, (![J_14]: (select(a_1763, J_14)=select(a_1762, J_14) | n14=J_14))). % 7.59/2.90 tff(c_1143, plain, (![J_14]: (select(a_1725, J_14)=select(a_1724, J_14) | n26=J_14))). % 7.59/2.90 tff(c_1089, plain, (![J_14]: (select(a_1739, J_14)=select(a_1738, J_14) | n40=J_14))). % 7.59/2.90 tff(c_1158, plain, (![J_14]: (select(a_1721, J_14)=select(a_1720, J_14) | n22=J_14))). % 7.59/2.90 tff(c_1182, plain, (![J_14]: (select(a_1714, J_14)=select(a_1713, J_14) | n15=J_14))). % 7.59/2.90 tff(c_1008, plain, (![J_14]: (select(a_1729, J_14)=select(a_1728, J_14) | n30=J_14))). % 7.59/2.90 tff(c_1038, plain, (![J_14]: (select(a_1753, J_14)=select(a_1752, J_14) | n43=J_14))). % 7.59/2.90 tff(c_1230, plain, (![J_14]: (select(a_1702, J_14)=select(a_1701, J_14) | n3=J_14))). % 7.59/2.90 tff(c_1020, plain, (![J_14]: (select(a_1776, J_14)=select(a_1775, J_14) | n34=J_14))). % 7.59/2.90 tff(c_969, plain, (![J_14]: (select(a_1754, J_14)=select(a_1753, J_14) | n28=J_14))). % 7.59/2.90 tff(c_1017, plain, (![J_14]: (select(a_1764, J_14)=select(a_1763, J_14) | n13=J_14))). % 7.59/2.90 tff(c_1065, plain, (![J_14]: (select(a_1767, J_14)=select(a_1766, J_14) | n15=J_14))). % 7.59/2.90 tff(c_972, plain, (![J_14]: (select(a_1772, J_14)=select(a_1771, J_14) | n42=J_14))). % 7.59/2.90 tff(c_1242, plain, (![J_14]: (select(a_1799, J_14)=select(a_1798, J_14) | n1=J_14))). % 7.59/2.90 tff(c_1203, plain, (![J_14]: (select(a_1709, J_14)=select(a_1708, J_14) | n10=J_14))). % 7.59/2.90 tff(c_1029, plain, (![J_14]: (select(a_1773, J_14)=select(a_1772, J_14) | n47=J_14))). % 7.59/2.90 tff(c_1194, plain, (![J_14]: (select(a_1711, J_14)=select(a_1710, J_14) | n12=J_14))). % 7.59/2.90 tff(c_1221, plain, (![J_14]: (select(a_1704, J_14)=select(a_1703, J_14) | n5=J_14))). % 7.59/2.90 tff(c_1191, plain, (![J_14]: (select(a_1712, J_14)=select(a_1711, J_14) | n13=J_14))). % 7.75/2.90 tff(c_1137, plain, (![J_14]: (select(a_1789, J_14)=select(a_1788, J_14) | n29=J_14))). % 7.75/2.90 tff(c_1200, plain, (![J_14]: (select(a_1710, J_14)=select(a_1709, J_14) | n11=J_14))). % 7.75/2.90 tff(c_1185, plain, (![J_14]: (select(a_1792, J_14)=select(a_1791, J_14) | n12=J_14))). % 7.75/2.90 tff(c_1107, plain, (![J_14]: (select(a_1787, J_14)=select(a_1786, J_14) | n10=J_14))). % 7.75/2.90 tff(c_999, plain, (![J_14]: (select(a_1780, J_14)=select(a_1779, J_14) | n38=J_14))). % 7.75/2.90 tff(c_1062, plain, (![J_14]: (select(a_1746, J_14)=select(a_1745, J_14) | n47=J_14))). % 7.75/2.90 tff(c_1128, plain, (![J_14]: (select(a_1778, J_14)=select(a_1777, J_14) | n36=J_14))). % 7.75/2.90 tff(c_1170, plain, (![J_14]: (select(a_1718, J_14)=select(a_1717, J_14) | n19=J_14))). % 7.75/2.90 tff(c_1119, plain, (![J_14]: (select(a_1731, J_14)=select(a_1730, J_14) | n32=J_14))). % 7.75/2.90 tff(c_1080, plain, (![J_14]: (select(a_1742, J_14)=select(a_1741, J_14) | n43=J_14))). % 7.75/2.90 tff(c_1023, plain, (![J_14]: (select(a_1775, J_14)=select(a_1774, J_14) | n26=J_14))). % 7.75/2.90 tff(c_1098, plain, (![J_14]: (select(a_1785, J_14)=select(a_1784, J_14) | n50=J_14))). % 7.75/2.90 tff(c_1125, plain, (![J_14]: (select(a_1788, J_14)=select(a_1787, J_14) | n48=J_14))). % 7.75/2.90 tff(c_1131, plain, (![J_14]: (select(a_1728, J_14)=select(a_1727, J_14) | n29=J_14))). % 7.75/2.90 tff(c_1044, plain, (![J_14]: (select(a_1751, J_14)=select(a_1750, J_14) | n30=J_14))). % 7.75/2.90 tff(c_1050, plain, (![J_14]: (select(a_1750, J_14)=select(a1, J_14) | n41=J_14))). % 7.75/2.90 tff(c_1167, plain, (![J_14]: (select(a_1791, J_14)=select(a_1790, J_14) | n37=J_14))). % 7.75/2.90 tff(c_1176, plain, (![J_14]: (select(a_1716, J_14)=select(a_1715, J_14) | n17=J_14))). % 7.75/2.90 tff(c_1104, plain, (![J_14]: (select(a_1735, J_14)=select(a_1734, J_14) | n36=J_14))). % 7.75/2.90 tff(c_1122, plain, (![J_14]: (select(a_1730, J_14)=select(a_1729, J_14) | n31=J_14))). % 7.75/2.90 tff(c_1206, plain, (![J_14]: (select(a_1708, J_14)=select(a_1707, J_14) | n9=J_14))). % 7.75/2.90 tff(c_1053, plain, (![J_14]: (select(a_1749, J_14)=select(a_1748, J_14) | n50=J_14))). % 7.75/2.90 tff(c_1209, plain, (![J_14]: (select(a_1707, J_14)=select(a_1706, J_14) | n8=J_14))). % 7.75/2.90 tff(c_1164, plain, (![J_14]: (select(a_1719, J_14)=select(a_1718, J_14) | n20=J_14))). % 7.75/2.90 tff(c_1083, plain, (![J_14]: (select(a_1741, J_14)=select(a_1740, J_14) | n42=J_14))). % 7.75/2.90 tff(c_1161, plain, (![J_14]: (select(a_1720, J_14)=select(a_1719, J_14) | n21=J_14))). % 7.75/2.90 tff(c_1215, plain, (![J_14]: (select(a_1795, J_14)=select(a_1794, J_14) | n4=J_14))). % 7.75/2.90 tff(c_1173, plain, (![J_14]: (select(a_1717, J_14)=select(a_1716, J_14) | n18=J_14))). % 7.75/2.90 tff(c_984, plain, (![J_14]: (select(a_1793, J_14)=select(a_1792, J_14) | n5=J_14))). % 7.75/2.90 tff(c_1101, plain, (![J_14]: (select(a_1736, J_14)=select(a_1735, J_14) | n37=J_14))). % 7.75/2.90 tff(c_1074, plain, (![J_14]: (select(a_1743, J_14)=select(a_1742, J_14) | n44=J_14))). % 7.75/2.90 tff(c_1134, plain, (![J_14]: (select(a_1727, J_14)=select(a_1726, J_14) | n28=J_14))). % 7.75/2.90 tff(c_1026, plain, (![J_14]: (select(a_1774, J_14)=select(a_1773, J_14) | n18=J_14))). % 7.75/2.90 tff(c_1086, plain, (![J_14]: (select(a_1740, J_14)=select(a_1739, J_14) | n41=J_14))). % 7.75/2.90 tff(c_1149, plain, (![J_14]: (select(a_1723, J_14)=select(a_1722, J_14) | n24=J_14))). % 7.75/2.90 tff(c_1188, plain, (![J_14]: (select(a_1713, J_14)=select(a_1712, J_14) | n14=J_14))). % 7.75/2.90 tff(c_1140, plain, (![J_14]: (select(a_1726, J_14)=select(a_1725, J_14) | n27=J_14))). % 7.75/2.91 tff(c_1146, plain, (![J_14]: (select(a_1724, J_14)=select(a_1723, J_14) | n25=J_14))). % 7.75/2.91 tff(c_957, plain, (![J_14]: (select(a_1760, J_14)=select(a_1759, J_14) | n16=J_14))). % 7.75/2.91 tff(c_990, plain, (![J_14]: (select(a_1783, J_14)=select(a_1782, J_14) | n46=J_14))). % 7.75/2.91 tff(c_1227, plain, (![J_14]: (select(a_1796, J_14)=select(a_1795, J_14) | n24=J_14))). % 7.75/2.91 tff(c_960, plain, (![J_14]: (select(a_1784, J_14)=select(a_1783, J_14) | n35=J_14))). % 7.75/2.91 tff(c_1236, plain, (![J_14]: (select(a_1700, J_14)=select(a1, J_14) | n1=J_14))). % 7.75/2.91 tff(c_1113, plain, (![J_14]: (select(a_1733, J_14)=select(a_1732, J_14) | n34=J_14))). % 7.75/2.91 tff(c_1179, plain, (![J_14]: (select(a_1715, J_14)=select(a_1714, J_14) | n16=J_14))). % 7.75/2.91 tff(c_1218, plain, (![J_14]: (select(a_1705, J_14)=select(a_1704, J_14) | n6=J_14))). % 7.75/2.91 tff(c_1032, plain, (![J_14]: (select(a_1771, J_14)=select(a_1770, J_14) | n17=J_14))). % 7.75/2.91 tff(c_945, plain, (![J_14]: (select(a_1798, J_14)=select(a_1797, J_14) | n31=J_14))). % 7.75/2.91 tff(c_1212, plain, (![J_14]: (select(a_1706, J_14)=select(a_1705, J_14) | n7=J_14))). % 7.75/2.91 tff(c_948, plain, (![J_14]: (select(a_1759, J_14)=select(a_1758, J_14) | n40=J_14))). % 7.75/2.91 tff(c_951, plain, (![J_14]: (select(a_1758, J_14)=select(a_1757, J_14) | n20=J_14))). % 7.75/2.91 tff(c_954, plain, (![J_14]: (select(a_1757, J_14)=select(a_1756, J_14) | n39=J_14))). % 7.75/2.91 tff(c_1092, plain, (![J_14]: (select(a_1738, J_14)=select(a_1737, J_14) | n39=J_14))). % 7.75/2.91 tff(c_1035, plain, (![J_14]: (select(a_1765, J_14)=select(a_1764, J_14) | n6=J_14))). % 7.75/2.91 tff(c_1233, plain, (![J_14]: (select(a_1701, J_14)=select(a_1700, J_14) | n2=J_14))). % 7.75/2.91 tff(c_1152, plain, (![J_14]: (select(a_1722, J_14)=select(a_1721, J_14) | n23=J_14))). % 7.75/2.91 tff(c_975, plain, (![J_14]: (select(a_1761, J_14)=select(a_1760, J_14) | n8=J_14))). % 7.75/2.91 tff(c_1014, plain, (![J_14]: (select(a_1777, J_14)=select(a_1776, J_14) | n11=J_14))). % 7.75/2.91 tff(c_1002, plain, (![J_14]: (select(a_1779, J_14)=select(a_1778, J_14) | n44=J_14))). % 7.75/2.91 tff(c_978, plain, (![J_14]: (select(a_1770, J_14)=select(a_1769, J_14) | n9=J_14))). % 7.75/2.91 tff(c_996, plain, (![J_14]: (select(a_1781, J_14)=select(a_1780, J_14) | n23=J_14))). % 7.75/2.91 tff(c_993, plain, (![J_14]: (select(a_1782, J_14)=select(a_1781, J_14) | n25=J_14))). % 7.75/2.91 tff(c_1056, plain, (![J_14]: (select(a_1748, J_14)=select(a_1747, J_14) | n49=J_14))). % 7.75/2.91 tff(c_987, plain, (![J_14]: (select(a_1762, J_14)=select(a_1761, J_14) | n49=J_14))). % 7.75/2.91 tff(c_966, plain, (![J_14]: (select(a_1755, J_14)=select(a_1754, J_14) | n19=J_14))). % 7.75/2.91 tff(c_1011, plain, (![J_14]: (select(a_1769, J_14)=select(a_1768, J_14) | n33=J_14))). % 7.75/2.91 tff(c_981, plain, (![J_14]: (select(a_1737, J_14)=select(a_1736, J_14) | n38=J_14))). % 7.75/2.91 tff(c_1224, plain, (![J_14]: (select(a_1703, J_14)=select(a_1702, J_14) | n4=J_14))). % 7.75/2.91 tff(c_1077, plain, (![J_14]: (select(a_1768, J_14)=select(a_1767, J_14) | n7=J_14))). % 7.75/2.91 tff(c_1047, plain, (![J_14]: (select(a_1766, J_14)=select(a_1765, J_14) | n27=J_14))). % 7.75/2.91 tff(c_1041, plain, (![J_14]: (select(a_1752, J_14)=select(a_1751, J_14) | n45=J_14))). % 7.75/2.91 tff(c_1059, plain, (![J_14]: (select(a_1747, J_14)=select(a_1746, J_14) | n48=J_14))). % 7.75/2.91 tff(c_1068, plain, (![J_14]: (select(a_1745, J_14)=select(a_1744, J_14) | n46=J_14))). % 7.75/2.91 tff(c_1197, plain, (![J_14]: (select(a_1794, J_14)=select(a_1793, J_14) | n32=J_14))). % 7.75/2.91 tff(c_1095, plain, (![J_14]: (select(a_1786, J_14)=select(a_1785, J_14) | n2=J_14))). % 7.75/2.91 tff(c_963, plain, (![J_14]: (select(a_1756, J_14)=select(a_1755, J_14) | n22=J_14))). % 7.75/2.91 tff(c_697, plain, (select(a_1774, n18)=e18)). % 7.75/2.91 tff(c_781, plain, (select(a_1734, n35)=e35)). % 7.75/2.91 tff(c_784, plain, (select(a_1733, n34)=e34)). % 7.75/2.91 tff(c_655, plain, (select(a_1793, n5)=e5)). % 7.75/2.91 tff(c_778, plain, (select(a_1787, n10)=e10)). % 7.75/2.91 tff(c_700, plain, (select(a_1773, n47)=e47)). % 7.75/2.91 tff(c_775, plain, (select(a_1735, n36)=e36)). % 7.75/2.91 tff(c_787, plain, (select(a_1732, n33)=e33)). % 7.75/2.91 tff(c_790, plain, (select(a_1731, n32)=e32)). % 7.75/2.91 tff(c_706, plain, (select(a_1765, n6)=e6)). % 7.75/2.91 tff(c_772, plain, (select(a_1736, n37)=e37)). % 7.75/2.91 tff(c_703, plain, (select(a_1771, n17)=e17)). % 7.75/2.91 tff(c_793, plain, (select(a_1730, n31)=e31)). % 7.75/2.91 tff(c_658, plain, (select(a_1762, n49)=e49)). % 7.75/2.91 tff(c_769, plain, (select(a_1785, n50)=e50)). % 7.75/2.91 tff(c_691, plain, (select(a_1776, n34)=e34)). % 7.75/2.91 tff(c_796, plain, (select(a_1788, n48)=e48)). % 7.75/2.91 tff(c_694, plain, (select(a_1775, n26)=e26)). % 7.75/2.91 tff(c_766, plain, (select(a_1786, n2)=e2)). % 7.75/2.91 tff(c_634, plain, (select(a_1756, n22)=e22)). % 7.75/2.91 tff(c_799, plain, (select(a_1778, n36)=e36)). % 7.75/2.91 tff(c_652, plain, (select(a_1737, n38)=e38)). % 7.75/2.91 tff(c_904, plain, (select(a_1701, n2)=e2)). % 7.75/2.91 tff(c_763, plain, (select(a_1738, n39)=e39)). % 7.75/2.91 tff(c_688, plain, (select(a_1764, n13)=e13)). % 7.75/2.91 tff(c_622, plain, (select(a_1758, n20)=e20)). % 7.75/2.91 tff(c_760, plain, (select(a_1739, n40)=e40)). % 7.75/2.91 tff(c_859, plain, (select(a_1713, n14)=e14)). % 7.75/2.91 tff(c_850, plain, (select(a_1715, n16)=e16)). % 7.75/2.91 tff(c_862, plain, (select(a_1712, n13)=e13)). % 7.75/2.91 tff(c_643, plain, (select(a_1772, n42)=e42)). % 7.75/2.91 tff(c_673, plain, (select(a_1779, n44)=e44)). % 7.75/2.91 tff(c_733, plain, (select(a_1746, n47)=e47)). % 7.75/2.91 tff(c_844, plain, (select(a_1717, n18)=e18)). % 7.75/2.91 tff(c_865, plain, (select(a_1711, n12)=e12)). % 7.75/2.91 tff(c_838, plain, (select(a_1791, n37)=e37)). % 7.75/2.91 tff(c_853, plain, (select(a_1714, n15)=e15)). % 7.75/2.91 tff(c_736, plain, (select(a_1767, n15)=e15)). % 7.75/2.91 tff(c_856, plain, (select(a_1792, n12)=e12)). % 7.75/2.91 tff(c_676, plain, (select(a_1763, n14)=e14)). % 7.75/2.91 tff(c_739, plain, (select(a_1745, n46)=e46)). % 7.75/2.91 tff(c_628, plain, (select(a_1760, n16)=e16)). % 7.75/2.91 tff(c_841, plain, (select(a_1718, n19)=e19)). % 7.75/2.91 tff(c_724, plain, (select(a_1749, n50)=e50)). % 7.75/2.92 tff(c_847, plain, (select(a_1716, n17)=e17)). % 7.75/2.92 tff(c_871, plain, (select(a_1710, n11)=e11)). % 7.75/2.92 tff(c_667, plain, (select(a_1781, n23)=e23)). % 7.75/2.92 tff(c_868, plain, (select(a_1794, n32)=e32)). % 7.75/2.92 tff(c_742, plain, (select(a_1744, n45)=e45)). % 7.75/2.92 tff(c_829, plain, (select(a_1721, n22)=e22)). % 7.75/2.92 tff(c_874, plain, (select(a_1709, n10)=e10)). % 7.75/2.92 tff(c_730, plain, (select(a_1747, n48)=e48)). % 7.75/2.92 tff(c_646, plain, (select(a_1761, n8)=e8)). % 7.75/2.92 tff(c_727, plain, (select(a_1748, n49)=e49)). % 7.75/2.92 tff(c_670, plain, (select(a_1780, n38)=e38)). % 7.75/2.92 tff(c_748, plain, (select(a_1768, n7)=e7)). % 7.75/2.92 tff(c_823, plain, (select(a_1722, n23)=e23)). % 7.75/2.92 tff(c_745, plain, (select(a_1743, n44)=e44)). % 7.75/2.92 tff(c_679, plain, (select(a_1729, n30)=e30)). % 7.75/2.92 tff(c_835, plain, (select(a_1719, n20)=e20)). % 7.75/2.92 tff(c_877, plain, (select(a_1708, n9)=e9)). % 7.75/2.92 tff(c_880, plain, (select(a_1707, n8)=e8)). % 7.75/2.92 tff(c_640, plain, (select(a_1754, n28)=e28)). % 7.75/2.92 tff(c_832, plain, (select(a_1720, n21)=e21)). % 7.75/2.92 tff(c_817, plain, (select(a_1724, n25)=e25)). % 7.75/2.92 tff(c_721, plain, (select(a_1750, n41)=e41)). % 7.75/2.92 tff(c_715, plain, (select(a_1751, n30)=e30)). % 7.75/2.92 tff(c_883, plain, (select(a_1706, n7)=e7)). % 7.75/2.92 tff(c_886, plain, (select(a_1795, n4)=e4)). % 7.75/2.92 tff(c_718, plain, (select(a_1766, n27)=e27)). % 7.75/2.92 tff(c_826, plain, (select(a_1790, n3)=e3)). % 7.75/2.92 tff(c_751, plain, (select(a_1742, n43)=e43)). % 7.75/2.92 tff(c_889, plain, (select(a_1705, n6)=e6)). % 7.75/2.92 tff(c_682, plain, (select(a_1769, n33)=e33)). % 7.75/2.92 tff(c_664, plain, (select(a_1782, n25)=e25)). % 7.75/2.92 tff(c_811, plain, (select(a_1726, n27)=e27)). % 7.75/2.92 tff(c_754, plain, (select(a_1741, n42)=e42)). % 7.75/2.92 tff(c_892, plain, (select(a_1704, n5)=e5)). % 7.75/2.92 tff(c_820, plain, (select(a_1723, n24)=e24)). % 7.75/2.92 tff(c_895, plain, (select(a_1703, n4)=e4)). % 7.75/2.92 tff(c_898, plain, (select(a_1796, n24)=e24)). % 7.75/2.92 tff(c_712, plain, (select(a_1752, n45)=e45)). % 7.75/2.92 tff(c_814, plain, (select(a_1725, n26)=e26)). % 7.75/2.92 tff(c_808, plain, (select(a_1789, n29)=e29)). % 7.75/2.92 tff(c_709, plain, (select(a_1753, n43)=e43)). % 7.75/2.92 tff(c_802, plain, (select(a_1728, n29)=e29)). % 7.75/2.92 tff(c_661, plain, (select(a_1783, n46)=e46)). % 7.75/2.92 tff(c_631, plain, (select(a_1784, n35)=e35)). % 7.75/2.92 tff(c_649, plain, (select(a_1770, n9)=e9)). % 7.75/2.92 tff(c_805, plain, (select(a_1727, n28)=e28)). % 7.75/2.92 tff(c_685, plain, (select(a_1777, n11)=e11)). % 7.75/2.92 tff(c_757, plain, (select(a_1740, n41)=e41)). % 7.75/2.92 tff(c_901, plain, (select(a_1702, n3)=e3)). % 7.75/2.92 tff(c_637, plain, (select(a_1755, n19)=e19)). % 7.75/2.92 tff(c_625, plain, (select(a_1757, n39)=e39)). % 7.75/2.92 tff(c_619, plain, (select(a_1759, n40)=e40)). % 7.75/2.92 tff(c_907, plain, (select(a_1700, n1)=e1)). % 7.75/2.92 tff(c_4, plain, (![A_6, I_4, E_7, J_5]: (select(store(A_6, I_4, E_7), J_5)=select(A_6, J_5) | J_5=I_4))). % 7.75/2.92 tff(c_910, plain, (select(a_1797, n21)=e21)). % 7.75/2.92 tff(c_913, plain, (select(a_1799, n1)=e1)). % 7.75/2.92 tff(c_616, plain, (select(a_1798, n31)=e31)). % 7.75/2.92 tff(c_2, plain, (![A_1, I_2, E_3]: (select(store(A_1, I_2, E_3), I_2)=E_3))). % 7.75/2.92 tff(c_202, plain, (store(a_1797, n31, e31)=a_1798)). % 7.75/2.92 tff(c_124, plain, (store(a_1758, n40, e40)=a_1759)). % 7.75/2.92 tff(c_122, plain, (store(a_1757, n20, e20)=a_1758)). % 7.75/2.92 tff(c_120, plain, (store(a_1756, n39, e39)=a_1757)). % 7.75/2.92 tff(c_126, plain, (store(a_1759, n16, e16)=a_1760)). % 7.75/2.92 tff(c_174, plain, (store(a_1783, n35, e35)=a_1784)). % 7.75/2.92 tff(c_118, plain, (store(a_1755, n22, e22)=a_1756)). % 7.75/2.92 tff(c_116, plain, (store(a_1754, n19, e19)=a_1755)). % 7.75/2.92 tff(c_114, plain, (store(a_1753, n28, e28)=a_1754)). % 7.75/2.92 tff(c_150, plain, (store(a_1771, n42, e42)=a_1772)). % 7.75/2.92 tff(c_128, plain, (store(a_1760, n8, e8)=a_1761)). % 7.75/2.92 tff(c_146, plain, (store(a_1769, n9, e9)=a_1770)). % 7.75/2.92 tff(c_80, plain, (store(a_1736, n38, e38)=a_1737)). % 7.75/2.92 tff(c_192, plain, (store(a_1792, n5, e5)=a_1793)). % 7.75/2.92 tff(c_130, plain, (store(a_1761, n49, e49)=a_1762)). % 7.75/2.92 tff(c_172, plain, (store(a_1782, n46, e46)=a_1783)). % 7.75/2.92 tff(c_170, plain, (store(a_1781, n25, e25)=a_1782)). % 7.75/2.92 tff(c_168, plain, (store(a_1780, n23, e23)=a_1781)). % 7.75/2.92 tff(c_166, plain, (store(a_1779, n38, e38)=a_1780)). % 7.75/2.92 tff(c_164, plain, (store(a_1778, n44, e44)=a_1779)). % 7.75/2.92 tff(c_132, plain, (store(a_1762, n14, e14)=a_1763)). % 7.75/2.92 tff(c_64, plain, (store(a_1728, n30, e30)=a_1729)). % 7.75/2.92 tff(c_144, plain, (store(a_1768, n33, e33)=a_1769)). % 7.75/2.92 tff(c_160, plain, (store(a_1776, n11, e11)=a_1777)). % 7.75/2.92 tff(c_134, plain, (store(a_1763, n13, e13)=a_1764)). % 7.75/2.92 tff(c_158, plain, (store(a_1775, n34, e34)=a_1776)). % 7.75/2.92 tff(c_156, plain, (store(a_1774, n26, e26)=a_1775)). % 7.75/2.92 tff(c_154, plain, (store(a_1773, n18, e18)=a_1774)). % 7.75/2.92 tff(c_152, plain, (store(a_1772, n47, e47)=a_1773)). % 7.75/2.92 tff(c_148, plain, (store(a_1770, n17, e17)=a_1771)). % 7.75/2.92 tff(c_136, plain, (store(a_1764, n6, e6)=a_1765)). % 7.75/2.92 tff(c_112, plain, (store(a_1752, n43, e43)=a_1753)). % 7.75/2.92 tff(c_110, plain, (store(a_1751, n45, e45)=a_1752)). % 7.75/2.92 tff(c_108, plain, (store(a_1750, n30, e30)=a_1751)). % 7.75/2.92 tff(c_138, plain, (store(a_1765, n27, e27)=a_1766)). % 7.75/2.92 tff(c_106, plain, (store(a1, n41, e41)=a_1750)). % 7.75/2.92 tff(c_104, plain, (store(a_1748, n50, e50)=a_1749)). % 7.75/2.92 tff(c_102, plain, (store(a_1747, n49, e49)=a_1748)). % 7.75/2.92 tff(c_100, plain, (store(a_1746, n48, e48)=a_1747)). % 7.75/2.92 tff(c_98, plain, (store(a_1745, n47, e47)=a_1746)). % 7.75/2.92 tff(c_140, plain, (store(a_1766, n15, e15)=a_1767)). % 7.75/2.92 tff(c_96, plain, (store(a_1744, n46, e46)=a_1745)). % 7.75/2.92 tff(c_94, plain, (store(a_1743, n45, e45)=a_1744)). % 7.75/2.92 tff(c_92, plain, (store(a_1742, n44, e44)=a_1743)). % 7.75/2.92 tff(c_142, plain, (store(a_1767, n7, e7)=a_1768)). % 7.75/2.92 tff(c_90, plain, (store(a_1741, n43, e43)=a_1742)). % 7.75/2.92 tff(c_88, plain, (store(a_1740, n42, e42)=a_1741)). % 7.75/2.92 tff(c_86, plain, (store(a_1739, n41, e41)=a_1740)). % 7.75/2.92 tff(c_84, plain, (store(a_1738, n40, e40)=a_1739)). % 7.75/2.92 tff(c_82, plain, (store(a_1737, n39, e39)=a_1738)). % 7.75/2.92 tff(c_178, plain, (store(a_1785, n2, e2)=a_1786)). % 7.75/2.92 tff(c_176, plain, (store(a_1784, n50, e50)=a_1785)). % 7.75/2.93 tff(c_78, plain, (store(a_1735, n37, e37)=a_1736)). % 7.75/2.93 tff(c_76, plain, (store(a_1734, n36, e36)=a_1735)). % 7.75/2.93 tff(c_180, plain, (store(a_1786, n10, e10)=a_1787)). % 7.75/2.93 tff(c_74, plain, (store(a_1733, n35, e35)=a_1734)). % 7.75/2.93 tff(c_72, plain, (store(a_1732, n34, e34)=a_1733)). % 7.75/2.93 tff(c_70, plain, (store(a_1731, n33, e33)=a_1732)). % 7.75/2.93 tff(c_68, plain, (store(a_1730, n32, e32)=a_1731)). % 7.75/2.93 tff(c_66, plain, (store(a_1729, n31, e31)=a_1730)). % 7.75/2.93 tff(c_182, plain, (store(a_1787, n48, e48)=a_1788)). % 7.75/2.93 tff(c_162, plain, (store(a_1777, n36, e36)=a_1778)). % 7.75/2.93 tff(c_62, plain, (store(a_1727, n29, e29)=a_1728)). % 7.75/2.93 tff(c_60, plain, (store(a_1726, n28, e28)=a_1727)). % 7.75/2.93 tff(c_184, plain, (store(a_1788, n29, e29)=a_1789)). % 7.75/2.93 tff(c_58, plain, (store(a_1725, n27, e27)=a_1726)). % 7.75/2.93 tff(c_56, plain, (store(a_1724, n26, e26)=a_1725)). % 7.75/2.93 tff(c_54, plain, (store(a_1723, n25, e25)=a_1724)). % 7.75/2.93 tff(c_52, plain, (store(a_1722, n24, e24)=a_1723)). % 7.75/2.93 tff(c_50, plain, (store(a_1721, n23, e23)=a_1722)). % 7.75/2.93 tff(c_186, plain, (store(a_1789, n3, e3)=a_1790)). % 7.75/2.93 tff(c_48, plain, (store(a_1720, n22, e22)=a_1721)). % 7.75/2.93 tff(c_46, plain, (store(a_1719, n21, e21)=a_1720)). % 7.75/2.93 tff(c_44, plain, (store(a_1718, n20, e20)=a_1719)). % 7.75/2.93 tff(c_188, plain, (store(a_1790, n37, e37)=a_1791)). % 7.75/2.93 tff(c_42, plain, (store(a_1717, n19, e19)=a_1718)). % 7.75/2.93 tff(c_40, plain, (store(a_1716, n18, e18)=a_1717)). % 7.75/2.93 tff(c_38, plain, (store(a_1715, n17, e17)=a_1716)). % 7.75/2.93 tff(c_36, plain, (store(a_1714, n16, e16)=a_1715)). % 7.75/2.93 tff(c_34, plain, (store(a_1713, n15, e15)=a_1714)). % 7.75/2.93 tff(c_190, plain, (store(a_1791, n12, e12)=a_1792)). % 7.75/2.93 tff(c_32, plain, (store(a_1712, n14, e14)=a_1713)). % 7.75/2.93 tff(c_30, plain, (store(a_1711, n13, e13)=a_1712)). % 7.75/2.93 tff(c_28, plain, (store(a_1710, n12, e12)=a_1711)). % 7.75/2.93 tff(c_194, plain, (store(a_1793, n32, e32)=a_1794)). % 7.75/2.93 tff(c_26, plain, (store(a_1709, n11, e11)=a_1710)). % 7.75/2.93 tff(c_24, plain, (store(a_1708, n10, e10)=a_1709)). % 7.75/2.93 tff(c_22, plain, (store(a_1707, n9, e9)=a_1708)). % 7.75/2.93 tff(c_20, plain, (store(a_1706, n8, e8)=a_1707)). % 7.75/2.93 tff(c_18, plain, (store(a_1705, n7, e7)=a_1706)). % 7.75/2.93 tff(c_196, plain, (store(a_1794, n4, e4)=a_1795)). % 7.75/2.93 tff(c_16, plain, (store(a_1704, n6, e6)=a_1705)). % 7.75/2.93 tff(c_14, plain, (store(a_1703, n5, e5)=a_1704)). % 7.75/2.93 tff(c_12, plain, (store(a_1702, n4, e4)=a_1703)). % 7.75/2.93 tff(c_198, plain, (store(a_1795, n24, e24)=a_1796)). % 7.75/2.93 tff(c_10, plain, (store(a_1701, n3, e3)=a_1702)). % 7.75/2.93 tff(c_8, plain, (store(a_1700, n2, e2)=a_1701)). % 7.75/2.93 tff(c_6, plain, (store(a1, n1, e1)=a_1700)). % 7.75/2.93 tff(c_200, plain, (store(a_1796, n21, e21)=a_1797)). % 7.75/2.93 tff(c_204, plain, (store(a_1798, n1, e1)=a_1799)). % 7.75/2.93 tff(c_206, plain, (a_1799!=a_1749)). % 7.75/2.93 % SZS output end Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 7.75/2.93 %------------------------------------------------------------------------------