%------------------------------------------------------------------------------ % File : Beagle---0.9.52 % Problem : SWV507-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 : n018.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 : Wed Apr 9 09:30:56 PM UTC 2025 % Result : Satisfiable 9.19s 3.16s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.11 % Problem : SWV507-1.050 : TPTP v9.0.0. Released v4.0.0. % 0.07/0.12 % 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.11/0.33 % Computer : n018.cluster.edu % 0.11/0.33 % Model : x86_64 x86_64 % 0.11/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.11/0.33 % Memory : 8042.1875MB % 0.11/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.11/0.33 % CPULimit : 300 % 0.11/0.33 % WCLimit : 300 % 0.11/0.33 % DateTime : Wed Apr 9 03:40:02 EDT 2025 % 0.11/0.33 % CPUTime : % 9.19/3.16 % 9.19/3.16 % SZS status Satisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p % 9.19/3.16 % 9.19/3.16 % SZS output start Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 9.19/3.18 %$ store > sk > 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 > i_1851 > e_1853 > e_1852 > 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_1850 > a_1849 > a_1848 > a_1847 > a_1846 > a_1845 > a_1844 > a_1843 > a_1842 > a_1841 > a_1840 > a_1839 > a_1838 > a_1837 > a_1836 > a_1835 > a_1834 > a_1833 > a_1832 > a_1831 > a_1830 > a_1829 > a_1828 > a_1827 > a_1826 > a_1825 > a_1824 > a_1823 > a_1822 > a_1821 > a_1820 > a_1819 > a_1818 > a_1817 > a_1816 > a_1815 > a_1814 > a_1813 > a_1812 > a_1811 > a_1810 > a_1809 > a_1808 > a_1807 > a_1806 > a_1805 > a_1804 > a_1803 > a_1802 > a_1801 > a_1800 > 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 > a1 % 9.19/3.18 % 9.19/3.18 %Foreground sorts: % 9.19/3.18 % 9.19/3.18 % 9.19/3.18 %Background operators: % 9.19/3.18 % 9.19/3.18 % 9.19/3.18 %Foreground operators: % 9.19/3.18 tff(e29, type, e29: $i). % 9.19/3.18 tff(a_1789, type, a_1789: $i). % 9.19/3.18 tff(a1, type, a1: $i). % 9.19/3.18 tff(e43, type, e43: $i). % 9.19/3.18 tff(a_1772, type, a_1772: $i). % 9.19/3.18 tff(n22, type, n22: $i). % 9.19/3.18 tff(n27, type, n27: $i). % 9.19/3.18 tff(e_1852, type, e_1852: $i). % 9.19/3.18 tff(a_1848, type, a_1848: $i). % 9.19/3.18 tff(n16, type, n16: $i). % 9.19/3.18 tff(a_1769, type, a_1769: $i). % 9.19/3.18 tff(n12, type, n12: $i). % 9.19/3.18 tff(e1, type, e1: $i). % 9.19/3.18 tff(a_1760, type, a_1760: $i). % 9.19/3.18 tff(i_1851, type, i_1851: $i). % 9.19/3.18 tff(e8, type, e8: $i). % 9.19/3.18 tff(a_1821, type, a_1821: $i). % 9.19/3.18 tff(a_1775, type, a_1775: $i). % 9.19/3.18 tff(a_1819, type, a_1819: $i). % 9.19/3.18 tff(a_1818, type, a_1818: $i). % 9.19/3.18 tff(e21, type, e21: $i). % 9.19/3.18 tff(n24, type, n24: $i). % 9.19/3.18 tff(a_1758, type, a_1758: $i). % 9.19/3.18 tff(a_1768, type, a_1768: $i). % 9.19/3.18 tff(e15, type, e15: $i). % 9.19/3.18 tff(a_1808, type, a_1808: $i). % 9.19/3.18 tff(a_1774, type, a_1774: $i). % 9.19/3.18 tff(n42, type, n42: $i). % 9.19/3.18 tff(a_1776, type, a_1776: $i). % 9.19/3.18 tff(e33, type, e33: $i). % 9.19/3.18 tff(a_1752, type, a_1752: $i). % 9.19/3.18 tff(n35, type, n35: $i). % 9.19/3.18 tff(e50, type, e50: $i). % 9.19/3.18 tff(a_1786, type, a_1786: $i). % 9.19/3.18 tff(a_1765, type, a_1765: $i). % 9.19/3.18 tff(e40, type, e40: $i). % 9.19/3.18 tff(a_1836, type, a_1836: $i). % 9.19/3.18 tff(a_1829, type, a_1829: $i). % 9.19/3.18 tff(e18, type, e18: $i). % 9.19/3.18 tff(a_1834, type, a_1834: $i). % 9.19/3.18 tff(a_1816, type, a_1816: $i). % 9.19/3.18 tff(a_1756, type, a_1756: $i). % 9.19/3.18 tff(e38, type, e38: $i). % 9.19/3.18 tff(e24, type, e24: $i). % 9.19/3.18 tff(e31, type, e31: $i). % 9.19/3.18 tff(n33, type, n33: $i). % 9.19/3.18 tff(n36, type, n36: $i). % 9.19/3.18 tff(e39, type, e39: $i). % 9.19/3.18 tff(e48, type, e48: $i). % 9.19/3.18 tff(a_1762, type, a_1762: $i). % 9.19/3.18 tff(a_1807, type, a_1807: $i). % 9.19/3.18 tff(store, type, store: ($i * $i * $i) > $i). % 9.19/3.18 tff(a_1782, type, a_1782: $i). % 9.19/3.18 tff(n23, type, n23: $i). % 9.19/3.18 tff(n8, type, n8: $i). % 9.19/3.18 tff(a_1793, type, a_1793: $i). % 9.19/3.18 tff(a_1838, type, a_1838: $i). % 9.19/3.18 tff(e20, type, e20: $i). % 9.19/3.18 tff(e41, type, e41: $i). % 9.19/3.18 tff(e19, type, e19: $i). % 9.19/3.18 tff(e16, type, e16: $i). % 9.19/3.18 tff(n30, type, n30: $i). % 9.19/3.18 tff(e35, type, e35: $i). % 9.19/3.18 tff(e_1853, type, e_1853: $i). % 9.19/3.18 tff(a_1797, type, a_1797: $i). % 9.19/3.18 tff(a_1840, type, a_1840: $i). % 9.19/3.18 tff(e2, type, e2: $i). % 9.19/3.18 tff(n28, type, n28: $i). % 9.19/3.18 tff(n9, type, n9: $i). % 9.19/3.18 tff(a_1847, type, a_1847: $i). % 9.19/3.18 tff(a_1792, type, a_1792: $i). % 9.19/3.18 tff(a_1781, type, a_1781: $i). % 9.19/3.18 tff(a_1770, type, a_1770: $i). % 9.19/3.18 tff(e42, type, e42: $i). % 9.19/3.18 tff(a_1817, type, a_1817: $i). % 9.19/3.18 tff(e37, type, e37: $i). % 9.19/3.18 tff(a_1832, type, a_1832: $i). % 9.19/3.18 tff(e13, type, e13: $i). % 9.19/3.18 tff(n3, type, n3: $i). % 9.19/3.18 tff(a_1806, type, a_1806: $i). % 9.19/3.18 tff(e32, type, e32: $i). % 9.19/3.18 tff(e22, type, e22: $i). % 9.19/3.18 tff(n46, type, n46: $i). % 9.19/3.18 tff(a_1796, type, a_1796: $i). % 9.19/3.18 tff(n48, type, n48: $i). % 9.19/3.18 tff(n39, type, n39: $i). % 9.19/3.18 tff(a_1754, type, a_1754: $i). % 9.19/3.18 tff(a_1812, type, a_1812: $i). % 9.19/3.18 tff(a_1809, type, a_1809: $i). % 9.19/3.18 tff(e34, type, e34: $i). % 9.19/3.18 tff(n1, type, n1: $i). % 9.19/3.18 tff(a_1842, type, a_1842: $i). % 9.19/3.18 tff(a_1764, type, a_1764: $i). % 9.19/3.18 tff(n29, type, n29: $i). % 9.19/3.18 tff(e9, type, e9: $i). % 9.19/3.18 tff(n37, type, n37: $i). % 9.19/3.18 tff(n44, type, n44: $i). % 9.19/3.18 tff(n50, type, n50: $i). % 9.19/3.18 tff(a_1805, type, a_1805: $i). % 9.19/3.18 tff(n7, type, n7: $i). % 9.19/3.18 tff(a_1810, type, a_1810: $i). % 9.19/3.18 tff(a_1846, type, a_1846: $i). % 9.19/3.18 tff(a_1813, type, a_1813: $i). % 9.19/3.18 tff(e25, type, e25: $i). % 9.19/3.18 tff(e26, type, e26: $i). % 9.19/3.18 tff(a_1839, type, a_1839: $i). % 9.19/3.18 tff(n6, type, n6: $i). % 9.19/3.18 tff(a_1753, type, a_1753: $i). % 9.19/3.18 tff(a_1784, type, a_1784: $i). % 9.19/3.18 tff(e17, type, e17: $i). % 9.19/3.18 tff(n26, type, n26: $i). % 9.19/3.18 tff(e27, type, e27: $i). % 9.19/3.18 tff(a_1831, type, a_1831: $i). % 9.19/3.18 tff(a_1757, type, a_1757: $i). % 9.19/3.18 tff(e10, type, e10: $i). % 9.19/3.18 tff(e7, type, e7: $i). % 9.19/3.18 tff(a_1773, type, a_1773: $i). % 9.19/3.18 tff(a_1767, type, a_1767: $i). % 9.19/3.18 tff(n13, type, n13: $i). % 9.19/3.18 tff(a_1823, type, a_1823: $i). % 9.19/3.18 tff(a_1787, type, a_1787: $i). % 9.19/3.18 tff(a_1771, type, a_1771: $i). % 9.19/3.18 tff(a_1822, type, a_1822: $i). % 9.19/3.18 tff(a_1785, type, a_1785: $i). % 9.19/3.18 tff(sk, type, sk: ($i * $i) > $i). % 9.19/3.18 tff(a_1778, type, a_1778: $i). % 9.19/3.18 tff(e36, type, e36: $i). % 9.19/3.18 tff(a_1795, type, a_1795: $i). % 9.19/3.18 tff(a_1761, type, a_1761: $i). % 9.19/3.18 tff(a_1841, type, a_1841: $i). % 9.19/3.18 tff(a_1801, type, a_1801: $i). % 9.19/3.18 tff(a_1814, type, a_1814: $i). % 9.19/3.18 tff(n4, type, n4: $i). % 9.19/3.18 tff(a_1827, type, a_1827: $i). % 9.19/3.18 tff(n10, type, n10: $i). % 9.19/3.18 tff(n14, type, n14: $i). % 9.19/3.18 tff(a_1777, type, a_1777: $i). % 9.19/3.18 tff(e45, type, e45: $i). % 9.19/3.18 tff(a_1837, type, a_1837: $i). % 9.19/3.18 tff(a_1755, type, a_1755: $i). % 9.19/3.18 tff(a_1815, type, a_1815: $i). % 9.19/3.18 tff(n15, type, n15: $i). % 9.19/3.18 tff(a_1759, type, a_1759: $i). % 9.19/3.18 tff(n17, type, n17: $i). % 9.19/3.18 tff(n40, type, n40: $i). % 9.19/3.18 tff(a_1763, type, a_1763: $i). % 9.19/3.18 tff(e30, type, e30: $i). % 9.19/3.18 tff(select, type, select: ($i * $i) > $i). % 9.19/3.18 tff(a_1833, type, a_1833: $i). % 9.19/3.18 tff(a_1780, type, a_1780: $i). % 9.19/3.18 tff(a_1800, type, a_1800: $i). % 9.19/3.18 tff(a_1835, type, a_1835: $i). % 9.19/3.18 tff(e49, type, e49: $i). % 9.19/3.18 tff(a_1779, type, a_1779: $i). % 9.19/3.18 tff(a_1794, type, a_1794: $i). % 9.19/3.18 tff(n31, type, n31: $i). % 9.19/3.18 tff(a_1844, type, a_1844: $i). % 9.19/3.18 tff(e47, type, e47: $i). % 9.19/3.18 tff(n49, type, n49: $i). % 9.19/3.18 tff(a_1798, type, a_1798: $i). % 9.19/3.18 tff(n47, type, n47: $i). % 9.19/3.18 tff(n32, type, n32: $i). % 9.19/3.18 tff(a_1751, type, a_1751: $i). % 9.19/3.18 tff(n20, type, n20: $i). % 9.19/3.18 tff(e23, type, e23: $i). % 9.19/3.18 tff(n18, type, n18: $i). % 9.19/3.18 tff(n38, type, n38: $i). % 9.19/3.18 tff(e14, type, e14: $i). % 9.19/3.18 tff(a_1850, type, a_1850: $i). % 9.19/3.18 tff(n11, type, n11: $i). % 9.19/3.18 tff(a_1849, type, a_1849: $i). % 9.19/3.18 tff(e12, type, e12: $i). % 9.19/3.18 tff(e4, type, e4: $i). % 9.19/3.18 tff(n45, type, n45: $i). % 9.19/3.18 tff(a_1811, type, a_1811: $i). % 9.19/3.18 tff(n34, type, n34: $i). % 9.19/3.18 tff(a_1826, type, a_1826: $i). % 9.19/3.18 tff(a_1766, type, a_1766: $i). % 9.19/3.18 tff(a_1843, type, a_1843: $i). % 9.19/3.18 tff(a_1799, type, a_1799: $i). % 9.19/3.18 tff(a_1830, type, a_1830: $i). % 9.19/3.18 tff(a_1788, type, a_1788: $i). % 9.19/3.18 tff(e6, type, e6: $i). % 9.19/3.18 tff(e46, type, e46: $i). % 9.19/3.18 tff(n19, type, n19: $i). % 9.19/3.18 tff(a_1804, type, a_1804: $i). % 9.19/3.18 tff(n2, type, n2: $i). % 9.19/3.18 tff(e11, type, e11: $i). % 9.19/3.18 tff(a_1828, type, a_1828: $i). % 9.19/3.18 tff(a_1803, type, a_1803: $i). % 9.19/3.18 tff(e28, type, e28: $i). % 9.19/3.18 tff(n5, type, n5: $i). % 9.19/3.18 tff(e44, type, e44: $i). % 9.19/3.18 tff(e3, type, e3: $i). % 9.19/3.18 tff(n43, type, n43: $i). % 9.19/3.18 tff(n25, type, n25: $i). % 9.19/3.18 tff(a_1824, type, a_1824: $i). % 9.19/3.18 tff(e5, type, e5: $i). % 9.19/3.18 tff(a_1802, type, a_1802: $i). % 9.19/3.18 tff(a_1791, type, a_1791: $i). % 9.19/3.18 tff(a_1820, type, a_1820: $i). % 9.19/3.18 tff(n21, type, n21: $i). % 9.19/3.18 tff(a_1790, type, a_1790: $i). % 9.19/3.18 tff(n41, type, n41: $i). % 9.19/3.18 tff(a_1783, type, a_1783: $i). % 9.19/3.18 tff(a_1845, type, a_1845: $i). % 9.19/3.18 tff(a_1825, type, a_1825: $i). % 9.19/3.18 % 9.19/3.18 %Saturated clause set: % 9.19/3.18 tff(c_3093, plain, (![J_14]: (select(a_1751, J_14)=select(a1, J_14) | i_1851=J_14))). % 9.19/3.18 tff(c_3092, plain, (![J_14]: (select(a_1850, J_14)=select(a_1849, J_14) | i_1851=J_14))). % 9.19/3.18 tff(c_1695, plain, (![J_14]: (select(a_1800, J_14)=select(a_1799, J_14) | i_1851=J_14))). % 9.19/3.18 tff(c_1170, plain, (![J_14]: (select(a_1844, J_14)=select(a_1843, J_14) | n5=J_14))). % 9.19/3.18 tff(c_1050, plain, (![J_14]: (select(a_1819, J_14)=select(a_1818, J_14) | n7=J_14))). % 9.19/3.18 tff(c_954, plain, (![J_14]: (select(a_1812, J_14)=select(a_1811, J_14) | n8=J_14))). % 9.19/3.18 tff(c_1041, plain, (![J_14]: (select(a_1807, J_14)=select(a_1806, J_14) | n22=J_14))). % 9.19/3.18 tff(c_1194, plain, (![J_14]: (select(a_1766, J_14)=select(a_1765, J_14) | n16=J_14))). % 9.19/3.18 tff(c_987, plain, (![J_14]: (select(a_1838, J_14)=select(a_1837, J_14) | n10=J_14))). % 9.19/3.18 tff(c_1224, plain, (![J_14]: (select(a_1758, J_14)=select(a_1757, J_14) | n8=J_14))). % 9.19/3.18 tff(c_1074, plain, (![J_14]: (select(a_1798, J_14)=select(a_1797, J_14) | n48=J_14))). % 9.19/3.18 tff(c_1191, plain, (![J_14]: (select(a_1767, J_14)=select(a_1766, J_14) | n17=J_14))). % 9.19/3.18 tff(c_1128, plain, (![J_14]: (select(a_1784, J_14)=select(a_1783, J_14) | n34=J_14))). % 9.19/3.18 tff(c_1119, plain, (![J_14]: (select(a_1786, J_14)=select(a_1785, J_14) | n36=J_14))). % 9.19/3.18 tff(c_1155, plain, (![J_14]: (select(a_1777, J_14)=select(a_1776, J_14) | n27=J_14))). % 9.19/3.18 tff(c_1107, plain, (![J_14]: (select(a_1789, J_14)=select(a_1788, J_14) | n39=J_14))). % 9.19/3.18 tff(c_1092, plain, (![J_14]: (select(a_1822, J_14)=select(a_1821, J_14) | n17=J_14))). % 9.19/3.18 tff(c_1167, plain, (![J_14]: (select(a_1773, J_14)=select(a_1772, J_14) | n23=J_14))). % 9.19/3.18 tff(c_1206, plain, (![J_14]: (select(a_1763, J_14)=select(a_1762, J_14) | n13=J_14))). % 9.19/3.18 tff(c_1065, plain, (![J_14]: (select(a_1801, J_14)=select(a1, J_14) | n41=J_14))). % 9.19/3.18 tff(c_1173, plain, (![J_14]: (select(a_1772, J_14)=select(a_1771, J_14) | n22=J_14))). % 9.19/3.18 tff(c_3097, plain, (store(a_1849, i_1851, e1)=a_1850)). % 9.19/3.18 tff(c_1110, plain, (![J_14]: (select(a_1840, J_14)=select(a_1839, J_14) | n29=J_14))). % 9.19/3.18 tff(c_3095, plain, (select(a_1751, i_1851)=e1)). % 9.19/3.18 tff(c_3117, plain, (e50!=e1)). % 9.19/3.18 tff(c_3112, plain, (e_1853=e1)). % 9.19/3.18 tff(c_3094, plain, (select(a_1850, i_1851)=e1)). % 9.19/3.18 tff(c_3096, plain, (store(a1, i_1851, e1)=a_1751)). % 9.19/3.18 tff(c_3091, plain, (n1=i_1851)). % 9.19/3.18 tff(c_1182, plain, (![J_14]: (select(a_1845, J_14)=select(a_1844, J_14) | n32=J_14))). % 9.19/3.18 tff(c_1101, plain, (![J_14]: (select(a_1839, J_14)=select(a_1838, J_14) | n48=J_14))). % 9.19/3.18 tff(c_1218, plain, (![J_14]: (select(a_1760, J_14)=select(a_1759, J_14) | n10=J_14))). % 9.19/3.18 tff(c_1122, plain, (![J_14]: (select(a_1841, J_14)=select(a_1840, J_14) | n3=J_14))). % 9.19/3.18 tff(c_1146, plain, (![J_14]: (select(a_1779, J_14)=select(a_1778, J_14) | n29=J_14))). % 9.19/3.18 tff(c_1056, plain, (![J_14]: (select(a_1803, J_14)=select(a_1802, J_14) | n45=J_14))). % 9.19/3.18 tff(c_1053, plain, (![J_14]: (select(a_1804, J_14)=select(a_1803, J_14) | n43=J_14))). % 9.19/3.18 tff(c_1227, plain, (![J_14]: (select(a_1757, J_14)=select(a_1756, J_14) | n7=J_14))). % 9.19/3.18 tff(c_1062, plain, (![J_14]: (select(a_1820, J_14)=select(a_1819, J_14) | n33=J_14))). % 9.19/3.18 tff(c_1212, plain, (![J_14]: (select(a_1848, J_14)=select(a_1847, J_14) | n21=J_14))). % 9.19/3.18 tff(c_1203, plain, (![J_14]: (select(a_1764, J_14)=select(a_1763, J_14) | n14=J_14))). % 9.19/3.19 tff(c_960, plain, (![J_14]: (select(a_1813, J_14)=select(a_1812, J_14) | n49=J_14))). % 9.19/3.19 tff(c_1002, plain, (![J_14]: (select(a_1816, J_14)=select(a_1815, J_14) | n6=J_14))). % 9.19/3.19 tff(c_1248, plain, (![J_14]: (select(a_1752, J_14)=select(a_1751, J_14) | n2=J_14))). % 9.19/3.19 tff(c_1245, plain, (![J_14]: (select(a_1753, J_14)=select(a_1752, J_14) | n3=J_14))). % 9.19/3.19 tff(c_1197, plain, (![J_14]: (select(a_1765, J_14)=select(a_1764, J_14) | n15=J_14))). % 9.19/3.19 tff(c_1143, plain, (![J_14]: (select(a_1780, J_14)=select(a_1779, J_14) | n30=J_14))). % 9.19/3.19 tff(c_1059, plain, (![J_14]: (select(a_1802, J_14)=select(a_1801, J_14) | n30=J_14))). % 9.19/3.19 tff(c_1080, plain, (![J_14]: (select(a_1821, J_14)=select(a_1820, J_14) | n9=J_14))). % 9.19/3.19 tff(c_1116, plain, (![J_14]: (select(a_1787, J_14)=select(a_1786, J_14) | n37=J_14))). % 9.19/3.19 tff(c_1221, plain, (![J_14]: (select(a_1759, J_14)=select(a_1758, J_14) | n9=J_14))). % 9.19/3.19 tff(c_1017, plain, (![J_14]: (select(a_1823, J_14)=select(a_1822, J_14) | n42=J_14))). % 9.19/3.19 tff(c_966, plain, (![J_14]: (select(a_1847, J_14)=select(a_1846, J_14) | n24=J_14))). % 9.19/3.19 tff(c_1023, plain, (![J_14]: (select(a_1830, J_14)=select(a_1829, J_14) | n44=J_14))). % 9.19/3.19 tff(c_1098, plain, (![J_14]: (select(a_1792, J_14)=select(a_1791, J_14) | n42=J_14))). % 9.19/3.19 tff(c_1083, plain, (![J_14]: (select(a_1796, J_14)=select(a_1795, J_14) | n46=J_14))). % 9.19/3.19 tff(c_1149, plain, (![J_14]: (select(a_1778, J_14)=select(a_1777, J_14) | n28=J_14))). % 9.19/3.19 tff(c_1086, plain, (![J_14]: (select(a_1795, J_14)=select(a_1794, J_14) | n45=J_14))). % 9.19/3.19 tff(c_2574, plain, (![J_14]: (select(a_1836, J_14)=select(a_1835, J_14) | i_1851=J_14))). % 9.19/3.19 tff(c_1179, plain, (![J_14]: (select(a_1770, J_14)=select(a_1769, J_14) | n20=J_14))). % 9.19/3.19 tff(c_969, plain, (![J_14]: (select(a_1809, J_14)=select(a_1808, J_14) | n20=J_14))). % 9.19/3.19 tff(c_1176, plain, (![J_14]: (select(a_1771, J_14)=select(a_1770, J_14) | n21=J_14))). % 9.19/3.19 tff(c_1209, plain, (![J_14]: (select(a_1762, J_14)=select(a_1761, J_14) | n12=J_14))). % 9.19/3.19 tff(c_1089, plain, (![J_14]: (select(a_1794, J_14)=select(a_1793, J_14) | n44=J_14))). % 9.19/3.19 tff(c_1200, plain, (![J_14]: (select(a_1846, J_14)=select(a_1845, J_14) | n4=J_14))). % 9.19/3.19 tff(c_1188, plain, (![J_14]: (select(a_1768, J_14)=select(a_1767, J_14) | n18=J_14))). % 9.19/3.19 tff(c_1164, plain, (![J_14]: (select(a_1774, J_14)=select(a_1773, J_14) | n24=J_14))). % 9.19/3.19 tff(c_1077, plain, (![J_14]: (select(a_1797, J_14)=select(a_1796, J_14) | n47=J_14))). % 9.19/3.19 tff(c_1137, plain, (![J_14]: (select(a_1781, J_14)=select(a_1780, J_14) | n31=J_14))). % 9.19/3.19 tff(c_1005, plain, (![J_14]: (select(a_1834, J_14)=select(a_1833, J_14) | n46=J_14))). % 9.19/3.19 tff(c_1140, plain, (![J_14]: (select(a_1842, J_14)=select(a_1841, J_14) | n37=J_14))). % 9.19/3.19 tff(c_1233, plain, (![J_14]: (select(a_1756, J_14)=select(a_1755, J_14) | n6=J_14))). % 9.19/3.19 tff(c_1104, plain, (![J_14]: (select(a_1790, J_14)=select(a_1789, J_14) | n40=J_14))). % 9.19/3.19 tff(c_1185, plain, (![J_14]: (select(a_1769, J_14)=select(a_1768, J_14) | n19=J_14))). % 9.19/3.19 tff(c_957, plain, (![J_14]: (select(a_1811, J_14)=select(a_1810, J_14) | n16=J_14))). % 9.19/3.19 tff(c_1152, plain, (![J_14]: (select(a_1843, J_14)=select(a_1842, J_14) | n12=J_14))). % 9.19/3.19 tff(c_1035, plain, (![J_14]: (select(a_1827, J_14)=select(a_1826, J_14) | n34=J_14))). % 9.19/3.19 tff(c_1038, plain, (![J_14]: (select(a_1825, J_14)=select(a_1824, J_14) | n18=J_14))). % 9.19/3.19 tff(c_1134, plain, (![J_14]: (select(a_1831, J_14)=select(a_1830, J_14) | n38=J_14))). % 9.19/3.19 tff(c_1032, plain, (![J_14]: (select(a_1818, J_14)=select(a_1817, J_14) | n15=J_14))). % 9.19/3.19 tff(c_1239, plain, (![J_14]: (select(a_1754, J_14)=select(a_1753, J_14) | n4=J_14))). % 9.19/3.19 tff(c_1161, plain, (![J_14]: (select(a_1775, J_14)=select(a_1774, J_14) | n25=J_14))). % 9.19/3.19 tff(c_972, plain, (![J_14]: (select(a_1814, J_14)=select(a_1813, J_14) | n14=J_14))). % 9.19/3.19 tff(c_1011, plain, (![J_14]: (select(a_1832, J_14)=select(a_1831, J_14) | n23=J_14))). % 9.19/3.19 tff(c_1071, plain, (![J_14]: (select(a_1799, J_14)=select(a_1798, J_14) | n49=J_14))). % 9.19/3.19 tff(c_975, plain, (![J_14]: (select(a_1808, J_14)=select(a_1807, J_14) | n39=J_14))). % 9.19/3.19 tff(c_993, plain, (![J_14]: (select(a_1837, J_14)=select(a_1836, J_14) | n2=J_14))). % 9.19/3.19 tff(c_990, plain, (![J_14]: (select(a_1815, J_14)=select(a_1814, J_14) | n13=J_14))). % 9.19/3.19 tff(c_1131, plain, (![J_14]: (select(a_1783, J_14)=select(a_1782, J_14) | n33=J_14))). % 9.19/3.19 tff(c_984, plain, (![J_14]: (select(a_1791, J_14)=select(a_1790, J_14) | n41=J_14))). % 9.19/3.19 tff(c_963, plain, (![J_14]: (select(a_1810, J_14)=select(a_1809, J_14) | n40=J_14))). % 9.19/3.19 tff(c_1008, plain, (![J_14]: (select(a_1833, J_14)=select(a_1832, J_14) | n25=J_14))). % 9.19/3.19 tff(c_978, plain, (![J_14]: (select(a_1826, J_14)=select(a_1825, J_14) | n26=J_14))). % 9.19/3.19 tff(c_1230, plain, (![J_14]: (select(a_1849, J_14)=select(a_1848, J_14) | n31=J_14))). % 9.19/3.19 tff(c_1029, plain, (![J_14]: (select(a_1828, J_14)=select(a_1827, J_14) | n11=J_14))). % 9.19/3.19 tff(c_1044, plain, (![J_14]: (select(a_1806, J_14)=select(a_1805, J_14) | n19=J_14))). % 9.19/3.19 tff(c_1215, plain, (![J_14]: (select(a_1761, J_14)=select(a_1760, J_14) | n11=J_14))). % 9.19/3.19 tff(c_1236, plain, (![J_14]: (select(a_1755, J_14)=select(a_1754, J_14) | n5=J_14))). % 9.19/3.19 tff(c_1014, plain, (![J_14]: (select(a_1782, J_14)=select(a_1781, J_14) | n32=J_14))). % 9.19/3.19 tff(c_981, plain, (![J_14]: (select(a_1824, J_14)=select(a_1823, J_14) | n47=J_14))). % 9.19/3.19 tff(c_999, plain, (![J_14]: (select(a_1835, J_14)=select(a_1834, J_14) | n35=J_14))). % 9.19/3.19 tff(c_1125, plain, (![J_14]: (select(a_1785, J_14)=select(a_1784, J_14) | n35=J_14))). % 9.19/3.19 tff(c_1095, plain, (![J_14]: (select(a_1793, J_14)=select(a_1792, J_14) | n43=J_14))). % 9.19/3.20 tff(c_1047, plain, (![J_14]: (select(a_1805, J_14)=select(a_1804, J_14) | n28=J_14))). % 9.19/3.20 tff(c_1113, plain, (![J_14]: (select(a_1788, J_14)=select(a_1787, J_14) | n38=J_14))). % 9.19/3.20 tff(c_1158, plain, (![J_14]: (select(a_1776, J_14)=select(a_1775, J_14) | n26=J_14))). % 9.19/3.20 tff(c_1698, plain, (store(a_1835, i_1851, e50)=a_1836)). % 9.19/3.20 tff(c_1699, plain, (store(a_1799, i_1851, e50)=a_1800)). % 9.19/3.20 tff(c_1697, plain, (select(a_1836, i_1851)=e50)). % 9.19/3.20 tff(c_1020, plain, (![J_14]: (select(a_1817, J_14)=select(a_1816, J_14) | n27=J_14))). % 9.19/3.20 tff(c_1705, plain, (e_1852=e50)). % 9.19/3.20 tff(c_1696, plain, (select(a_1800, i_1851)=e50)). % 9.19/3.20 tff(c_1693, plain, (n50=i_1851)). % 9.46/3.20 tff(c_1026, plain, (![J_14]: (select(a_1829, J_14)=select(a_1828, J_14) | n36=J_14))). % 9.46/3.20 tff(c_793, plain, (select(a_1840, n29)=e29)). % 9.46/3.20 tff(c_796, plain, (select(a_1788, n38)=e38)). % 9.46/3.20 tff(c_724, plain, (select(a_1807, n22)=e22)). % 9.46/3.20 tff(c_673, plain, (select(a_1815, n13)=e13)). % 9.46/3.20 tff(c_715, plain, (select(a_1818, n15)=e15)). % 9.46/3.20 tff(c_799, plain, (select(a_1787, n37)=e37)). % 9.46/3.20 tff(c_676, plain, (select(a_1837, n2)=e2)). % 9.46/3.20 tff(c_787, plain, (select(a_1790, n40)=e40)). % 9.46/3.20 tff(c_709, plain, (select(a_1829, n36)=e36)). % 9.46/3.20 tff(c_814, plain, (select(a_1783, n33)=e33)). % 9.46/3.20 tff(c_802, plain, (select(a_1786, n36)=e36)). % 9.46/3.20 tff(c_718, plain, (select(a_1827, n34)=e34)). % 9.46/3.20 tff(c_805, plain, (select(a_1841, n3)=e3)). % 9.46/3.20 tff(c_808, plain, (select(a_1785, n35)=e35)). % 9.46/3.20 tff(c_712, plain, (select(a_1828, n11)=e11)). % 9.46/3.20 tff(c_721, plain, (select(a_1825, n18)=e18)). % 9.46/3.20 tff(c_931, plain, (select(a_1752, n2)=e2)). % 9.46/3.20 tff(c_790, plain, (select(a_1789, n39)=e39)). % 9.46/3.20 tff(c_781, plain, (select(a_1792, n42)=e42)). % 9.46/3.20 tff(c_640, plain, (select(a_1811, n16)=e16)). % 9.46/3.20 tff(c_811, plain, (select(a_1784, n34)=e34)). % 9.46/3.20 tff(c_670, plain, (select(a_1838, n10)=e10)). % 9.46/3.20 tff(c_784, plain, (select(a_1839, n48)=e48)). % 9.46/3.20 tff(c_652, plain, (select(a_1809, n20)=e20)). % 9.46/3.20 tff(c_817, plain, (select(a_1831, n38)=e38)). % 9.46/3.20 tff(c_928, plain, (select(a_1753, n3)=e3)). % 9.46/3.20 tff(c_706, plain, (select(a_1830, n44)=e44)). % 9.46/3.20 tff(c_865, plain, (select(a_1845, n32)=e32)). % 9.46/3.20 tff(c_883, plain, (select(a_1846, n4)=e4)). % 9.46/3.20 tff(c_877, plain, (select(a_1766, n16)=e16)). % 9.46/3.20 tff(c_694, plain, (select(a_1832, n23)=e23)). % 9.46/3.20 tff(c_691, plain, (select(a_1833, n25)=e25)). % 9.46/3.20 tff(c_871, plain, (select(a_1768, n18)=e18)). % 9.46/3.20 tff(c_874, plain, (select(a_1767, n17)=e17)). % 9.46/3.20 tff(c_754, plain, (select(a_1799, n49)=e49)). % 9.46/3.20 tff(c_757, plain, (select(a_1798, n48)=e48)). % 9.46/3.20 tff(c_892, plain, (select(a_1762, n12)=e12)). % 9.46/3.20 tff(c_880, plain, (select(a_1765, n15)=e15)). % 9.46/3.20 tff(c_688, plain, (select(a_1834, n46)=e46)). % 9.46/3.20 tff(c_661, plain, (select(a_1826, n26)=e26)). % 9.46/3.20 tff(c_886, plain, (select(a_1764, n14)=e14)). % 9.46/3.20 tff(c_868, plain, (select(a_1769, n19)=e19)). % 9.46/3.20 tff(c_760, plain, (select(a_1797, n47)=e47)). % 9.46/3.20 tff(c_889, plain, (select(a_1763, n13)=e13)). % 9.46/3.20 tff(c_646, plain, (select(a_1810, n40)=e40)). % 9.46/3.20 tff(c_763, plain, (select(a_1821, n9)=e9)). % 9.46/3.20 tff(c_850, plain, (select(a_1773, n23)=e23)). % 9.46/3.20 tff(c_748, plain, (select(a_1801, n41)=e41)). % 9.46/3.20 tff(c_766, plain, (select(a_1796, n46)=e46)). % 9.46/3.20 tff(c_859, plain, (select(a_1771, n21)=e21)). % 9.46/3.20 tff(c_664, plain, (select(a_1824, n47)=e47)). % 9.46/3.20 tff(c_697, plain, (select(a_1782, n32)=e32)). % 9.46/3.20 tff(c_862, plain, (select(a_1770, n20)=e20)). % 9.46/3.20 tff(c_853, plain, (select(a_1844, n5)=e5)). % 9.46/3.20 tff(c_895, plain, (select(a_1848, n21)=e21)). % 9.46/3.20 tff(c_685, plain, (select(a_1816, n6)=e6)). % 9.46/3.20 tff(c_745, plain, (select(a_1820, n33)=e33)). % 9.46/3.20 tff(c_856, plain, (select(a_1772, n22)=e22)). % 9.46/3.20 tff(c_901, plain, (select(a_1760, n10)=e10)). % 9.46/3.20 tff(c_898, plain, (select(a_1761, n11)=e11)). % 9.46/3.20 tff(c_742, plain, (select(a_1802, n30)=e30)). % 9.46/3.20 tff(c_847, plain, (select(a_1774, n24)=e24)). % 9.46/3.20 tff(c_904, plain, (select(a_1759, n9)=e9)). % 9.46/3.20 tff(c_739, plain, (select(a_1803, n45)=e45)). % 9.46/3.20 tff(c_658, plain, (select(a_1808, n39)=e39)). % 9.46/3.20 tff(c_841, plain, (select(a_1776, n26)=e26)). % 9.46/3.20 tff(c_736, plain, (select(a_1804, n43)=e43)). % 9.46/3.20 tff(c_700, plain, (select(a_1823, n42)=e42)). % 9.46/3.20 tff(c_733, plain, (select(a_1819, n7)=e7)). % 9.46/3.20 tff(c_769, plain, (select(a_1795, n45)=e45)). % 9.46/3.20 tff(c_907, plain, (select(a_1758, n8)=e8)). % 9.46/3.20 tff(c_910, plain, (select(a_1757, n7)=e7)). % 9.46/3.20 tff(c_838, plain, (select(a_1777, n27)=e27)). % 9.46/3.20 tff(c_844, plain, (select(a_1775, n25)=e25)). % 9.46/3.20 tff(c_913, plain, (select(a_1849, n31)=e31)). % 9.46/3.20 tff(c_772, plain, (select(a_1794, n44)=e44)). % 9.46/3.20 tff(c_832, plain, (select(a_1778, n28)=e28)). % 9.46/3.20 tff(c_730, plain, (select(a_1805, n28)=e28)). % 9.46/3.20 tff(c_820, plain, (select(a_1781, n31)=e31)). % 9.46/3.20 tff(c_916, plain, (select(a_1756, n6)=e6)). % 9.46/3.20 tff(c_682, plain, (select(a_1835, n35)=e35)). % 9.46/3.20 tff(c_835, plain, (select(a_1843, n12)=e12)). % 9.46/3.21 tff(c_649, plain, (select(a_1847, n24)=e24)). % 9.46/3.21 tff(c_667, plain, (select(a_1791, n41)=e41)). % 9.46/3.21 tff(c_829, plain, (select(a_1779, n29)=e29)). % 9.46/3.21 tff(c_826, plain, (select(a_1780, n30)=e30)). % 9.46/3.21 tff(c_823, plain, (select(a_1842, n37)=e37)). % 9.46/3.21 tff(c_727, plain, (select(a_1806, n19)=e19)). % 9.46/3.21 tff(c_703, plain, (select(a_1817, n27)=e27)). % 9.46/3.21 tff(c_775, plain, (select(a_1822, n17)=e17)). % 9.46/3.21 tff(c_919, plain, (select(a_1755, n5)=e5)). % 9.46/3.21 tff(c_922, plain, (select(a_1754, n4)=e4)). % 9.46/3.21 tff(c_778, plain, (select(a_1793, n43)=e43)). % 9.46/3.21 tff(c_655, plain, (select(a_1814, n14)=e14)). % 9.46/3.21 tff(c_643, plain, (select(a_1813, n49)=e49)). % 9.46/3.21 tff(c_637, plain, (select(a_1812, n8)=e8)). % 9.46/3.21 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))). % 9.46/3.21 tff(c_2, plain, (![A_1, I_2, E_3]: (select(store(A_1, I_2, E_3), I_2)=E_3))). % 9.46/3.21 tff(c_128, plain, (store(a_1811, n8, e8)=a_1812)). % 9.46/3.21 tff(c_126, plain, (store(a_1810, n16, e16)=a_1811)). % 9.46/3.21 tff(c_130, plain, (store(a_1812, n49, e49)=a_1813)). % 9.46/3.21 tff(c_124, plain, (store(a_1809, n40, e40)=a_1810)). % 9.46/3.21 tff(c_198, plain, (store(a_1846, n24, e24)=a_1847)). % 9.46/3.21 tff(c_122, plain, (store(a_1808, n20, e20)=a_1809)). % 9.46/3.21 tff(c_132, plain, (store(a_1813, n14, e14)=a_1814)). % 9.46/3.21 tff(c_120, plain, (store(a_1807, n39, e39)=a_1808)). % 9.46/3.21 tff(c_156, plain, (store(a_1825, n26, e26)=a_1826)). % 9.46/3.21 tff(c_152, plain, (store(a_1823, n47, e47)=a_1824)). % 9.46/3.21 tff(c_86, plain, (store(a_1790, n41, e41)=a_1791)). % 9.46/3.21 tff(c_180, plain, (store(a_1837, n10, e10)=a_1838)). % 9.46/3.21 tff(c_134, plain, (store(a_1814, n13, e13)=a_1815)). % 9.46/3.21 tff(c_178, plain, (store(a_1836, n2, e2)=a_1837)). % 9.46/3.21 tff(c_174, plain, (store(a_1834, n35, e35)=a_1835)). % 9.46/3.21 tff(c_136, plain, (store(a_1815, n6, e6)=a_1816)). % 9.46/3.21 tff(c_172, plain, (store(a_1833, n46, e46)=a_1834)). % 9.46/3.21 tff(c_170, plain, (store(a_1832, n25, e25)=a_1833)). % 9.46/3.21 tff(c_168, plain, (store(a_1831, n23, e23)=a_1832)). % 9.46/3.21 tff(c_68, plain, (store(a_1781, n32, e32)=a_1782)). % 9.46/3.21 tff(c_150, plain, (store(a_1822, n42, e42)=a_1823)). % 9.46/3.21 tff(c_138, plain, (store(a_1816, n27, e27)=a_1817)). % 9.46/3.21 tff(c_164, plain, (store(a_1829, n44, e44)=a_1830)). % 9.46/3.21 tff(c_162, plain, (store(a_1828, n36, e36)=a_1829)). % 9.46/3.21 tff(c_160, plain, (store(a_1827, n11, e11)=a_1828)). % 9.46/3.21 tff(c_140, plain, (store(a_1817, n15, e15)=a_1818)). % 9.46/3.21 tff(c_158, plain, (store(a_1826, n34, e34)=a_1827)). % 9.46/3.21 tff(c_154, plain, (store(a_1824, n18, e18)=a_1825)). % 9.46/3.21 tff(c_118, plain, (store(a_1806, n22, e22)=a_1807)). % 9.46/3.21 tff(c_116, plain, (store(a_1805, n19, e19)=a_1806)). % 9.46/3.21 tff(c_114, plain, (store(a_1804, n28, e28)=a_1805)). % 9.46/3.21 tff(c_142, plain, (store(a_1818, n7, e7)=a_1819)). % 9.46/3.21 tff(c_112, plain, (store(a_1803, n43, e43)=a_1804)). % 9.46/3.21 tff(c_110, plain, (store(a_1802, n45, e45)=a_1803)). % 9.46/3.21 tff(c_108, plain, (store(a_1801, n30, e30)=a_1802)). % 9.46/3.21 tff(c_144, plain, (store(a_1819, n33, e33)=a_1820)). % 9.46/3.21 tff(c_106, plain, (store(a1, n41, e41)=a_1801)). % 9.46/3.21 tff(c_102, plain, (store(a_1798, n49, e49)=a_1799)). % 9.46/3.21 tff(c_100, plain, (store(a_1797, n48, e48)=a_1798)). % 9.46/3.21 tff(c_98, plain, (store(a_1796, n47, e47)=a_1797)). % 9.46/3.21 tff(c_146, plain, (store(a_1820, n9, e9)=a_1821)). % 9.46/3.21 tff(c_96, plain, (store(a_1795, n46, e46)=a_1796)). % 9.46/3.21 tff(c_94, plain, (store(a_1794, n45, e45)=a_1795)). % 9.46/3.21 tff(c_92, plain, (store(a_1793, n44, e44)=a_1794)). % 9.46/3.21 tff(c_148, plain, (store(a_1821, n17, e17)=a_1822)). % 9.46/3.21 tff(c_90, plain, (store(a_1792, n43, e43)=a_1793)). % 9.46/3.21 tff(c_88, plain, (store(a_1791, n42, e42)=a_1792)). % 9.46/3.21 tff(c_182, plain, (store(a_1838, n48, e48)=a_1839)). % 9.46/3.21 tff(c_84, plain, (store(a_1789, n40, e40)=a_1790)). % 9.46/3.21 tff(c_82, plain, (store(a_1788, n39, e39)=a_1789)). % 9.46/3.21 tff(c_184, plain, (store(a_1839, n29, e29)=a_1840)). % 9.46/3.21 tff(c_80, plain, (store(a_1787, n38, e38)=a_1788)). % 9.46/3.21 tff(c_78, plain, (store(a_1786, n37, e37)=a_1787)). % 9.46/3.21 tff(c_76, plain, (store(a_1785, n36, e36)=a_1786)). % 9.46/3.21 tff(c_186, plain, (store(a_1840, n3, e3)=a_1841)). % 9.46/3.21 tff(c_74, plain, (store(a_1784, n35, e35)=a_1785)). % 9.46/3.21 tff(c_72, plain, (store(a_1783, n34, e34)=a_1784)). % 9.46/3.21 tff(c_70, plain, (store(a_1782, n33, e33)=a_1783)). % 9.46/3.21 tff(c_166, plain, (store(a_1830, n38, e38)=a_1831)). % 9.46/3.21 tff(c_66, plain, (store(a_1780, n31, e31)=a_1781)). % 9.46/3.21 tff(c_188, plain, (store(a_1841, n37, e37)=a_1842)). % 9.46/3.21 tff(c_64, plain, (store(a_1779, n30, e30)=a_1780)). % 9.46/3.21 tff(c_62, plain, (store(a_1778, n29, e29)=a_1779)). % 9.46/3.21 tff(c_60, plain, (store(a_1777, n28, e28)=a_1778)). % 9.46/3.21 tff(c_190, plain, (store(a_1842, n12, e12)=a_1843)). % 9.46/3.21 tff(c_58, plain, (store(a_1776, n27, e27)=a_1777)). % 9.46/3.21 tff(c_56, plain, (store(a_1775, n26, e26)=a_1776)). % 9.46/3.21 tff(c_54, plain, (store(a_1774, n25, e25)=a_1775)). % 9.46/3.21 tff(c_52, plain, (store(a_1773, n24, e24)=a_1774)). % 9.46/3.21 tff(c_50, plain, (store(a_1772, n23, e23)=a_1773)). % 9.46/3.21 tff(c_192, plain, (store(a_1843, n5, e5)=a_1844)). % 9.46/3.21 tff(c_48, plain, (store(a_1771, n22, e22)=a_1772)). % 9.46/3.21 tff(c_46, plain, (store(a_1770, n21, e21)=a_1771)). % 9.46/3.21 tff(c_44, plain, (store(a_1769, n20, e20)=a_1770)). % 9.46/3.21 tff(c_194, plain, (store(a_1844, n32, e32)=a_1845)). % 9.46/3.21 tff(c_42, plain, (store(a_1768, n19, e19)=a_1769)). % 9.46/3.21 tff(c_40, plain, (store(a_1767, n18, e18)=a_1768)). % 9.46/3.21 tff(c_38, plain, (store(a_1766, n17, e17)=a_1767)). % 9.46/3.21 tff(c_36, plain, (store(a_1765, n16, e16)=a_1766)). % 9.46/3.21 tff(c_34, plain, (store(a_1764, n15, e15)=a_1765)). % 9.46/3.21 tff(c_196, plain, (store(a_1845, n4, e4)=a_1846)). % 9.46/3.21 tff(c_32, plain, (store(a_1763, n14, e14)=a_1764)). % 9.46/3.21 tff(c_30, plain, (store(a_1762, n13, e13)=a_1763)). % 9.46/3.21 tff(c_28, plain, (store(a_1761, n12, e12)=a_1762)). % 9.46/3.21 tff(c_200, plain, (store(a_1847, n21, e21)=a_1848)). % 9.46/3.22 tff(c_26, plain, (store(a_1760, n11, e11)=a_1761)). % 9.46/3.22 tff(c_24, plain, (store(a_1759, n10, e10)=a_1760)). % 9.46/3.22 tff(c_22, plain, (store(a_1758, n9, e9)=a_1759)). % 9.46/3.22 tff(c_20, plain, (store(a_1757, n8, e8)=a_1758)). % 9.46/3.22 tff(c_18, plain, (store(a_1756, n7, e7)=a_1757)). % 9.46/3.22 tff(c_202, plain, (store(a_1848, n31, e31)=a_1849)). % 9.46/3.22 tff(c_16, plain, (store(a_1755, n6, e6)=a_1756)). % 9.46/3.22 tff(c_14, plain, (store(a_1754, n5, e5)=a_1755)). % 9.46/3.22 tff(c_12, plain, (store(a_1753, n4, e4)=a_1754)). % 9.46/3.22 tff(c_10, plain, (store(a_1752, n3, e3)=a_1753)). % 9.46/3.22 tff(c_8, plain, (store(a_1751, n2, e2)=a_1752)). % 9.46/3.22 tff(c_210, plain, (sk(a_1800, a_1850)=i_1851)). % 9.46/3.22 % SZS output end Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 9.46/3.22 %------------------------------------------------------------------------------