%------------------------------------------------------------------------------ % File : Beagle---0.9.52 % Problem : SWV498-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/sandbox2/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox2/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s % Computer : n026.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:43 PM UTC 2025 % Result : Satisfiable 19.97s 8.80s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.11/0.12 % Problem : SWV498-1.050 : TPTP v9.0.0. Released v4.0.0. % 0.11/0.13 % Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox2/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox2/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s % 0.13/0.33 % Computer : n026.cluster.edu % 0.13/0.33 % Model : x86_64 x86_64 % 0.13/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.33 % Memory : 8042.1875MB % 0.13/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.33 % CPULimit : 300 % 0.13/0.33 % WCLimit : 300 % 0.13/0.33 % DateTime : Wed Apr 9 03:36:08 EDT 2025 % 0.13/0.34 % CPUTime : % 19.97/8.79 % 19.97/8.80 % SZS status Satisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p % 19.97/8.80 % 19.97/8.80 % SZS output start Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 20.15/8.82 %$ store > select > #nlpp > i9 > i8 > i7 > i6 > i50 > i5 > i49 > i48 > i47 > i46 > i45 > i44 > i43 > i42 > i41 > i40 > i4 > i39 > i38 > i37 > i36 > i35 > i34 > i33 > i32 > i31 > i30 > i3 > i29 > i28 > i27 > i26 > i25 > i24 > i23 > i22 > i21 > i20 > i2 > i19 > i18 > i17 > i16 > i15 > i14 > i13 > i12 > i11 > i10 > i1 > 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 % 20.15/8.82 % 20.15/8.82 %Foreground sorts: % 20.15/8.82 % 20.15/8.82 % 20.15/8.82 %Background operators: % 20.15/8.82 % 20.15/8.82 % 20.15/8.82 %Foreground operators: % 20.15/8.82 tff(e29, type, e29: $i). % 20.15/8.82 tff(i34, type, i34: $i). % 20.15/8.82 tff(a_1742, type, a_1742: $i). % 20.15/8.82 tff(a_1789, type, a_1789: $i). % 20.15/8.82 tff(a1, type, a1: $i). % 20.15/8.82 tff(e43, type, e43: $i). % 20.15/8.82 tff(a_1772, type, a_1772: $i). % 20.15/8.82 tff(a_1737, type, a_1737: $i). % 20.15/8.82 tff(a_1769, type, a_1769: $i). % 20.15/8.82 tff(e1, type, e1: $i). % 20.15/8.82 tff(a_1725, type, a_1725: $i). % 20.15/8.82 tff(a_1760, type, a_1760: $i). % 20.15/8.82 tff(a_1723, type, a_1723: $i). % 20.15/8.82 tff(e8, type, e8: $i). % 20.15/8.82 tff(i50, type, i50: $i). % 20.15/8.82 tff(a_1706, type, a_1706: $i). % 20.15/8.82 tff(a_1775, type, a_1775: $i). % 20.15/8.82 tff(e21, type, e21: $i). % 20.15/8.82 tff(i16, type, i16: $i). % 20.15/8.82 tff(i32, type, i32: $i). % 20.15/8.82 tff(i33, type, i33: $i). % 20.15/8.82 tff(a_1741, type, a_1741: $i). % 20.15/8.82 tff(a_1715, type, a_1715: $i). % 20.15/8.82 tff(a_1758, type, a_1758: $i). % 20.15/8.82 tff(i45, type, i45: $i). % 20.15/8.82 tff(a_1768, type, a_1768: $i). % 20.15/8.82 tff(e15, type, e15: $i). % 20.15/8.82 tff(i14, type, i14: $i). % 20.15/8.82 tff(a_1774, type, a_1774: $i). % 20.15/8.82 tff(a_1712, type, a_1712: $i). % 20.15/8.82 tff(a_1776, type, a_1776: $i). % 20.15/8.82 tff(e33, type, e33: $i). % 20.15/8.82 tff(a_1752, type, a_1752: $i). % 20.15/8.82 tff(e50, type, e50: $i). % 20.15/8.82 tff(a_1786, type, a_1786: $i). % 20.15/8.82 tff(i11, type, i11: $i). % 20.15/8.82 tff(a_1765, type, a_1765: $i). % 20.15/8.82 tff(a_1707, type, a_1707: $i). % 20.15/8.82 tff(e40, type, e40: $i). % 20.15/8.82 tff(a_1730, type, a_1730: $i). % 20.15/8.82 tff(e18, type, e18: $i). % 20.15/8.82 tff(a_1756, type, a_1756: $i). % 20.15/8.82 tff(e38, type, e38: $i). % 20.15/8.82 tff(i48, type, i48: $i). % 20.15/8.82 tff(e24, type, e24: $i). % 20.15/8.82 tff(e31, type, e31: $i). % 20.15/8.82 tff(i44, type, i44: $i). % 20.15/8.82 tff(e39, type, e39: $i). % 20.15/8.82 tff(i23, type, i23: $i). % 20.15/8.82 tff(e48, type, e48: $i). % 20.15/8.82 tff(a_1762, type, a_1762: $i). % 20.15/8.82 tff(a_1749, type, a_1749: $i). % 20.15/8.82 tff(i30, type, i30: $i). % 20.15/8.82 tff(store, type, store: ($i * $i * $i) > $i). % 20.15/8.82 tff(a_1782, type, a_1782: $i). % 20.15/8.82 tff(a_1793, type, a_1793: $i). % 20.15/8.82 tff(e20, type, e20: $i). % 20.15/8.82 tff(e41, type, e41: $i). % 20.15/8.82 tff(e19, type, e19: $i). % 20.15/8.82 tff(a_1746, type, a_1746: $i). % 20.15/8.82 tff(e16, type, e16: $i). % 20.15/8.82 tff(i20, type, i20: $i). % 20.15/8.82 tff(a_1744, type, a_1744: $i). % 20.15/8.82 tff(e35, type, e35: $i). % 20.15/8.82 tff(i38, type, i38: $i). % 20.15/8.82 tff(a_1797, type, a_1797: $i). % 20.15/8.82 tff(e2, type, e2: $i). % 20.15/8.82 tff(i18, type, i18: $i). % 20.15/8.82 tff(i27, type, i27: $i). % 20.15/8.82 tff(a_1703, type, a_1703: $i). % 20.15/8.82 tff(a_1792, type, a_1792: $i). % 20.15/8.82 tff(i26, type, i26: $i). % 20.15/8.82 tff(a_1781, type, a_1781: $i). % 20.15/8.82 tff(a_1770, type, a_1770: $i). % 20.15/8.82 tff(e42, type, e42: $i). % 20.15/8.82 tff(a_1713, type, a_1713: $i). % 20.15/8.82 tff(e37, type, e37: $i). % 20.15/8.82 tff(e13, type, e13: $i). % 20.15/8.82 tff(i22, type, i22: $i). % 20.15/8.82 tff(e32, type, e32: $i). % 20.15/8.82 tff(e22, type, e22: $i). % 20.15/8.82 tff(i12, type, i12: $i). % 20.15/8.82 tff(a_1720, type, a_1720: $i). % 20.15/8.82 tff(a_1796, type, a_1796: $i). % 20.15/8.82 tff(i15, type, i15: $i). % 20.15/8.82 tff(a_1754, type, a_1754: $i). % 20.15/8.82 tff(i17, type, i17: $i). % 20.15/8.82 tff(i19, type, i19: $i). % 20.15/8.82 tff(e34, type, e34: $i). % 20.15/8.82 tff(a_1729, type, a_1729: $i). % 20.15/8.82 tff(a_1764, type, a_1764: $i). % 20.15/8.82 tff(i21, type, i21: $i). % 20.15/8.82 tff(e9, type, e9: $i). % 20.15/8.82 tff(a_1704, type, a_1704: $i). % 20.15/8.82 tff(i25, type, i25: $i). % 20.15/8.82 tff(i40, type, i40: $i). % 20.15/8.82 tff(i28, type, i28: $i). % 20.15/8.82 tff(a_1710, type, a_1710: $i). % 20.15/8.82 tff(a_1717, type, a_1717: $i). % 20.15/8.82 tff(i31, type, i31: $i). % 20.15/8.82 tff(e25, type, e25: $i). % 20.15/8.82 tff(a_1714, type, a_1714: $i). % 20.15/8.82 tff(e26, type, e26: $i). % 20.15/8.82 tff(i10, type, i10: $i). % 20.15/8.82 tff(a_1753, type, a_1753: $i). % 20.15/8.82 tff(a_1784, type, a_1784: $i). % 20.15/8.82 tff(e17, type, e17: $i). % 20.15/8.82 tff(i35, type, i35: $i). % 20.15/8.82 tff(e27, type, e27: $i). % 20.15/8.82 tff(a_1750, type, a_1750: $i). % 20.15/8.82 tff(a_1731, type, a_1731: $i). % 20.15/8.82 tff(a_1757, type, a_1757: $i). % 20.15/8.82 tff(e10, type, e10: $i). % 20.15/8.82 tff(e7, type, e7: $i). % 20.15/8.82 tff(i39, type, i39: $i). % 20.15/8.82 tff(i42, type, i42: $i). % 20.15/8.82 tff(a_1773, type, a_1773: $i). % 20.15/8.82 tff(a_1767, type, a_1767: $i). % 20.15/8.82 tff(i8, type, i8: $i). % 20.15/8.82 tff(i46, type, i46: $i). % 20.15/8.82 tff(a_1738, type, a_1738: $i). % 20.15/8.82 tff(a_1787, type, a_1787: $i). % 20.15/8.82 tff(a_1709, type, a_1709: $i). % 20.15/8.82 tff(a_1771, type, a_1771: $i). % 20.15/8.82 tff(a_1728, type, a_1728: $i). % 20.15/8.82 tff(i9, type, i9: $i). % 20.15/8.82 tff(a_1785, type, a_1785: $i). % 20.15/8.82 tff(a_1727, type, a_1727: $i). % 20.15/8.82 tff(a_1778, type, a_1778: $i). % 20.15/8.82 tff(i29, type, i29: $i). % 20.15/8.82 tff(e36, type, e36: $i). % 20.15/8.82 tff(a_1795, type, a_1795: $i). % 20.15/8.82 tff(a_1718, type, a_1718: $i). % 20.15/8.82 tff(a_1761, type, a_1761: $i). % 20.15/8.82 tff(a_1745, type, a_1745: $i). % 20.15/8.82 tff(i7, type, i7: $i). % 20.15/8.82 tff(i1, type, i1: $i). % 20.15/8.82 tff(i2, type, i2: $i). % 20.15/8.82 tff(a_1719, type, a_1719: $i). % 20.15/8.82 tff(a_1777, type, a_1777: $i). % 20.15/8.82 tff(e45, type, e45: $i). % 20.15/8.82 tff(a_1726, type, a_1726: $i). % 20.15/8.82 tff(a_1755, type, a_1755: $i). % 20.15/8.82 tff(a_1759, type, a_1759: $i). % 20.15/8.82 tff(a_1700, type, a_1700: $i). % 20.15/8.82 tff(i37, type, i37: $i). % 20.15/8.82 tff(a_1763, type, a_1763: $i). % 20.15/8.82 tff(e30, type, e30: $i). % 20.15/8.82 tff(select, type, select: ($i * $i) > $i). % 20.15/8.82 tff(a_1734, type, a_1734: $i). % 20.15/8.82 tff(a_1780, type, a_1780: $i). % 20.15/8.82 tff(e49, type, e49: $i). % 20.15/8.82 tff(a_1779, type, a_1779: $i). % 20.15/8.82 tff(a_1705, type, a_1705: $i). % 20.15/8.82 tff(a_1794, type, a_1794: $i). % 20.15/8.82 tff(i41, type, i41: $i). % 20.15/8.82 tff(i43, type, i43: $i). % 20.15/8.82 tff(a_1722, type, a_1722: $i). % 20.15/8.82 tff(e47, type, e47: $i). % 20.15/8.82 tff(a_1740, type, a_1740: $i). % 20.15/8.82 tff(a_1798, type, a_1798: $i). % 20.15/8.82 tff(a_1751, type, a_1751: $i). % 20.15/8.82 tff(a_1735, type, a_1735: $i). % 20.15/8.82 tff(e23, type, e23: $i). % 20.15/8.82 tff(e14, type, e14: $i). % 20.15/8.82 tff(e12, type, e12: $i). % 20.15/8.82 tff(e4, type, e4: $i). % 20.15/8.82 tff(a_1747, type, a_1747: $i). % 20.15/8.82 tff(i13, type, i13: $i). % 20.15/8.82 tff(i49, type, i49: $i). % 20.15/8.82 tff(a_1739, type, a_1739: $i). % 20.15/8.82 tff(a_1766, type, a_1766: $i). % 20.15/8.82 tff(a_1748, type, a_1748: $i). % 20.15/8.82 tff(a_1716, type, a_1716: $i). % 20.15/8.82 tff(a_1799, type, a_1799: $i). % 20.15/8.82 tff(a_1732, type, a_1732: $i). % 20.15/8.82 tff(a_1788, type, a_1788: $i). % 20.15/8.82 tff(e6, type, e6: $i). % 20.15/8.82 tff(i5, type, i5: $i). % 20.15/8.82 tff(e46, type, e46: $i). % 20.15/8.82 tff(a_1711, type, a_1711: $i). % 20.15/8.82 tff(a_1724, type, a_1724: $i). % 20.15/8.82 tff(e11, type, e11: $i). % 20.15/8.82 tff(e28, type, e28: $i). % 20.15/8.82 tff(i4, type, i4: $i). % 20.15/8.82 tff(i36, type, i36: $i). % 20.15/8.82 tff(e44, type, e44: $i). % 20.15/8.82 tff(e3, type, e3: $i). % 20.15/8.82 tff(a_1736, type, a_1736: $i). % 20.15/8.82 tff(a_1721, type, a_1721: $i). % 20.15/8.82 tff(i47, type, i47: $i). % 20.15/8.82 tff(i24, type, i24: $i). % 20.15/8.82 tff(a_1708, type, a_1708: $i). % 20.15/8.82 tff(a_1702, type, a_1702: $i). % 20.15/8.82 tff(e5, type, e5: $i). % 20.15/8.82 tff(a_1701, type, a_1701: $i). % 20.15/8.82 tff(a_1743, type, a_1743: $i). % 20.15/8.82 tff(i3, type, i3: $i). % 20.15/8.82 tff(a_1791, type, a_1791: $i). % 20.15/8.82 tff(a_1790, type, a_1790: $i). % 20.15/8.82 tff(a_1783, type, a_1783: $i). % 20.15/8.82 tff(a_1733, type, a_1733: $i). % 20.15/8.82 tff(i6, type, i6: $i). % 20.15/8.82 % 20.15/8.82 %Saturated clause set: % 20.15/8.82 tff(c_3685, plain, (![J_14]: (select(a_1720, J_14)=select(a_1719, J_14) | i21=J_14))). % 20.15/8.82 tff(c_3682, plain, (![J_14]: (select(a_1779, J_14)=select(a_1778, J_14) | i44=J_14))). % 20.15/8.82 tff(c_3592, plain, (![J_14]: (select(a_1760, J_14)=select(a_1759, J_14) | i16=J_14))). % 20.15/8.82 tff(c_3628, plain, (![J_14]: (select(a_1740, J_14)=select(a_1739, J_14) | i41=J_14))). % 20.15/8.83 tff(c_3574, plain, (![J_14]: (select(a_1757, J_14)=select(a_1756, J_14) | i39=J_14))). % 20.15/8.83 tff(c_3577, plain, (![J_14]: (select(a_1795, J_14)=select(a_1794, J_14) | i4=J_14))). % 20.15/8.83 tff(c_3562, plain, (![J_14]: (select(a_1759, J_14)=select(a_1758, J_14) | i40=J_14))). % 20.15/8.83 tff(c_3514, plain, (![J_14]: (select(a_1788, J_14)=select(a_1787, J_14) | i48=J_14))). % 20.15/8.83 tff(c_3664, plain, (![J_14]: (select(a_1737, J_14)=select(a_1736, J_14) | i38=J_14))). % 20.15/8.83 tff(c_3589, plain, (![J_14]: (select(a_1747, J_14)=select(a_1746, J_14) | i48=J_14))). % 20.15/8.83 tff(c_3526, plain, (![J_14]: (select(a_1767, J_14)=select(a_1766, J_14) | i15=J_14))). % 20.15/8.83 tff(c_3568, plain, (![J_14]: (select(a_1719, J_14)=select(a_1718, J_14) | i20=J_14))). % 20.15/8.83 tff(c_3481, plain, (![J_14]: (select(a_1794, J_14)=select(a_1793, J_14) | i32=J_14))). % 20.15/8.83 tff(c_3463, plain, (![J_14]: (select(a_1739, J_14)=select(a_1738, J_14) | i40=J_14))). % 20.15/8.83 tff(c_3412, plain, (![J_14]: (select(a_1713, J_14)=select(a_1712, J_14) | i14=J_14))). % 20.15/8.83 tff(c_3460, plain, (![J_14]: (select(a_1735, J_14)=select(a_1734, J_14) | i36=J_14))). % 20.15/8.83 tff(c_3415, plain, (![J_14]: (select(a_1743, J_14)=select(a_1742, J_14) | i44=J_14))). % 20.15/8.83 tff(c_3448, plain, (![J_14]: (select(a_1729, J_14)=select(a_1728, J_14) | i30=J_14))). % 20.15/8.83 tff(c_3688, plain, (![J_14]: (select(a_1780, J_14)=select(a_1779, J_14) | i38=J_14))). % 20.15/8.83 tff(c_3649, plain, (![J_14]: (select(a_1784, J_14)=select(a_1783, J_14) | i35=J_14))). % 20.15/8.83 tff(c_3541, plain, (![J_14]: (select(a_1796, J_14)=select(a_1795, J_14) | i24=J_14))). % 20.15/8.83 tff(c_3523, plain, (![J_14]: (select(a_1703, J_14)=select(a_1702, J_14) | i4=J_14))). % 20.15/8.83 tff(c_3511, plain, (![J_14]: (select(a_1727, J_14)=select(a_1726, J_14) | i28=J_14))). % 20.15/8.83 tff(c_3547, plain, (![J_14]: (select(a_1775, J_14)=select(a_1774, J_14) | i26=J_14))). % 20.15/8.83 tff(c_3604, plain, (![J_14]: (select(a_1770, J_14)=select(a_1769, J_14) | i9=J_14))). % 20.15/8.83 tff(c_3484, plain, (![J_14]: (select(a_1732, J_14)=select(a_1731, J_14) | i33=J_14))). % 20.15/8.83 tff(c_3442, plain, (![J_14]: (select(a_1768, J_14)=select(a_1767, J_14) | i7=J_14))). % 20.15/8.83 tff(c_3433, plain, (![J_14]: (select(a_1777, J_14)=select(a_1776, J_14) | i11=J_14))). % 20.15/8.83 tff(c_3610, plain, (![J_14]: (select(a_1756, J_14)=select(a_1755, J_14) | i22=J_14))). % 20.15/8.83 tff(c_3520, plain, (![J_14]: (select(a_1774, J_14)=select(a_1773, J_14) | i18=J_14))). % 20.15/8.83 tff(c_3502, plain, (![J_14]: (select(a_1793, J_14)=select(a_1792, J_14) | i5=J_14))). % 20.15/8.83 tff(c_3472, plain, (![J_14]: (select(a_1723, J_14)=select(a_1722, J_14) | i24=J_14))). % 20.15/8.83 tff(c_3637, plain, (![J_14]: (select(a_1758, J_14)=select(a_1757, J_14) | i20=J_14))). % 20.15/8.83 tff(c_3535, plain, (![J_14]: (select(a_1715, J_14)=select(a_1714, J_14) | i16=J_14))). % 20.15/8.83 tff(c_3529, plain, (![J_14]: (select(a_1751, J_14)=select(a_1750, J_14) | i30=J_14))). % 20.15/8.83 tff(c_3655, plain, (![J_14]: (select(a_1733, J_14)=select(a_1732, J_14) | i34=J_14))). % 20.15/8.83 tff(c_3466, plain, (![J_14]: (select(a_1716, J_14)=select(a_1715, J_14) | i17=J_14))). % 20.15/8.84 tff(c_3538, plain, (![J_14]: (select(a_1753, J_14)=select(a_1752, J_14) | i43=J_14))). % 20.15/8.84 tff(c_3559, plain, (![J_14]: (select(a_1710, J_14)=select(a_1709, J_14) | i11=J_14))). % 20.15/8.84 tff(c_3553, plain, (![J_14]: (select(a_1718, J_14)=select(a_1717, J_14) | i19=J_14))). % 20.15/8.84 tff(c_3493, plain, (![J_14]: (select(a_1787, J_14)=select(a_1786, J_14) | i10=J_14))). % 20.15/8.84 tff(c_3595, plain, (![J_14]: (select(a_1785, J_14)=select(a_1784, J_14) | i50=J_14))). % 20.15/8.84 tff(c_3676, plain, (![J_14]: (select(a_1772, J_14)=select(a_1771, J_14) | i42=J_14))). % 20.15/8.84 tff(c_3607, plain, (![J_14]: (select(a_1781, J_14)=select(a_1780, J_14) | i23=J_14))). % 20.15/8.84 tff(c_3667, plain, (![J_14]: (select(a_1762, J_14)=select(a_1761, J_14) | i49=J_14))). % 20.15/8.84 tff(c_3580, plain, (![J_14]: (select(a_1790, J_14)=select(a_1789, J_14) | i3=J_14))). % 20.15/8.84 tff(c_3646, plain, (![J_14]: (select(a_1750, J_14)=select(a1, J_14) | i41=J_14))). % 20.15/8.84 tff(c_3406, plain, (![J_14]: (select(a_1746, J_14)=select(a_1745, J_14) | i47=J_14))). % 20.15/8.84 tff(c_3634, plain, (![J_14]: (select(a_1776, J_14)=select(a_1775, J_14) | i34=J_14))). % 20.15/8.84 tff(c_3619, plain, (![J_14]: (select(a_1798, J_14)=select(a_1797, J_14) | i31=J_14))). % 20.15/8.84 tff(c_3625, plain, (![J_14]: (select(a_1765, J_14)=select(a_1764, J_14) | i6=J_14))). % 20.15/8.84 tff(c_3427, plain, (![J_14]: (select(a_1783, J_14)=select(a_1782, J_14) | i46=J_14))). % 20.15/8.84 tff(c_3631, plain, (![J_14]: (select(a_1799, J_14)=select(a_1798, J_14) | i1=J_14))). % 20.15/8.84 tff(c_3583, plain, (![J_14]: (select(a_1755, J_14)=select(a_1754, J_14) | i19=J_14))). % 20.15/8.84 tff(c_3508, plain, (![J_14]: (select(a_1706, J_14)=select(a_1705, J_14) | i7=J_14))). % 20.15/8.84 tff(c_3451, plain, (![J_14]: (select(a_1745, J_14)=select(a_1744, J_14) | i46=J_14))). % 20.15/8.84 tff(c_3661, plain, (![J_14]: (select(a_1791, J_14)=select(a_1790, J_14) | i37=J_14))). % 20.15/8.84 tff(c_3469, plain, (![J_14]: (select(a_1778, J_14)=select(a_1777, J_14) | i36=J_14))). % 20.15/8.84 tff(c_3556, plain, (![J_14]: (select(a_1714, J_14)=select(a_1713, J_14) | i15=J_14))). % 20.15/8.84 tff(c_3679, plain, (![J_14]: (select(a_1728, J_14)=select(a_1727, J_14) | i29=J_14))). % 20.15/8.84 tff(c_3544, plain, (![J_14]: (select(a_1748, J_14)=select(a_1747, J_14) | i49=J_14))). % 20.15/8.84 tff(c_3400, plain, (![J_14]: (select(a_1717, J_14)=select(a_1716, J_14) | i18=J_14))). % 20.15/8.84 tff(c_3586, plain, (![J_14]: (select(a_1722, J_14)=select(a_1721, J_14) | i23=J_14))). % 20.15/8.84 tff(c_3550, plain, (![J_14]: (select(a_1700, J_14)=select(a1, J_14) | i1=J_14))). % 20.15/8.84 tff(c_3673, plain, (![J_14]: (select(a_1742, J_14)=select(a_1741, J_14) | i43=J_14))). % 20.15/8.84 tff(c_3601, plain, (![J_14]: (select(a_1782, J_14)=select(a_1781, J_14) | i25=J_14))). % 20.15/8.84 tff(c_3571, plain, (![J_14]: (select(a_1730, J_14)=select(a_1729, J_14) | i31=J_14))). % 20.15/8.84 tff(c_3622, plain, (![J_14]: (select(a_1712, J_14)=select(a_1711, J_14) | i13=J_14))). % 20.15/8.84 tff(c_3496, plain, (![J_14]: (select(a_1709, J_14)=select(a_1708, J_14) | i10=J_14))). % 20.15/8.84 tff(c_3475, plain, (![J_14]: (select(a_1741, J_14)=select(a_1740, J_14) | i42=J_14))). % 20.15/8.84 tff(c_3487, plain, (![J_14]: (select(a_1797, J_14)=select(a_1796, J_14) | i21=J_14))). % 20.15/8.84 tff(c_3613, plain, (![J_14]: (select(a_1763, J_14)=select(a_1762, J_14) | i14=J_14))). % 20.15/8.84 tff(c_3490, plain, (![J_14]: (select(a_1736, J_14)=select(a_1735, J_14) | i37=J_14))). % 20.15/8.84 tff(c_3391, plain, (![J_14]: (select(a_1786, J_14)=select(a_1785, J_14) | i2=J_14))). % 20.15/8.85 tff(c_3394, plain, (![J_14]: (select(a_1761, J_14)=select(a_1760, J_14) | i8=J_14))). % 20.15/8.85 tff(c_3397, plain, (![J_14]: (select(a_1734, J_14)=select(a_1733, J_14) | i35=J_14))). % 20.15/8.85 tff(c_3478, plain, (![J_14]: (select(a_1708, J_14)=select(a_1707, J_14) | i9=J_14))). % 20.15/8.85 tff(c_3643, plain, (![J_14]: (select(a_1789, J_14)=select(a_1788, J_14) | i29=J_14))). % 20.15/8.85 tff(c_3598, plain, (![J_14]: (select(a_1701, J_14)=select(a_1700, J_14) | i2=J_14))). % 20.15/8.85 tff(c_3403, plain, (![J_14]: (select(a_1721, J_14)=select(a_1720, J_14) | i22=J_14))). % 20.15/8.85 tff(c_3418, plain, (![J_14]: (select(a_1711, J_14)=select(a_1710, J_14) | i12=J_14))). % 20.15/8.85 tff(c_3640, plain, (![J_14]: (select(a_1731, J_14)=select(a_1730, J_14) | i32=J_14))). % 20.15/8.85 tff(c_3457, plain, (![J_14]: (select(a_1754, J_14)=select(a_1753, J_14) | i28=J_14))). % 20.15/8.85 tff(c_3421, plain, (![J_14]: (select(a_1725, J_14)=select(a_1724, J_14) | i26=J_14))). % 20.15/8.85 tff(c_3439, plain, (![J_14]: (select(a_1744, J_14)=select(a_1743, J_14) | i45=J_14))). % 20.15/8.85 tff(c_3436, plain, (![J_14]: (select(a_1764, J_14)=select(a_1763, J_14) | i13=J_14))). % 20.15/8.85 tff(c_3430, plain, (![J_14]: (select(a_1792, J_14)=select(a_1791, J_14) | i12=J_14))). % 20.15/8.85 tff(c_3565, plain, (![J_14]: (select(a_1773, J_14)=select(a_1772, J_14) | i47=J_14))). % 20.15/8.85 tff(c_3409, plain, (![J_14]: (select(a_1704, J_14)=select(a_1703, J_14) | i5=J_14))). % 20.15/8.85 tff(c_3454, plain, (![J_14]: (select(a_1726, J_14)=select(a_1725, J_14) | i27=J_14))). % 20.15/8.85 tff(c_3424, plain, (![J_14]: (select(a_1769, J_14)=select(a_1768, J_14) | i33=J_14))). % 20.15/8.85 tff(c_3532, plain, (![J_14]: (select(a_1702, J_14)=select(a_1701, J_14) | i3=J_14))). % 20.15/8.85 tff(c_3670, plain, (![J_14]: (select(a_1724, J_14)=select(a_1723, J_14) | i25=J_14))). % 20.15/8.85 tff(c_3517, plain, (![J_14]: (select(a_1738, J_14)=select(a_1737, J_14) | i39=J_14))). % 20.15/8.85 tff(c_3658, plain, (![J_14]: (select(a_1771, J_14)=select(a_1770, J_14) | i17=J_14))). % 20.15/8.85 tff(c_3505, plain, (![J_14]: (select(a_1705, J_14)=select(a_1704, J_14) | i6=J_14))). % 20.15/8.85 tff(c_3499, plain, (![J_14]: (select(a_1749, J_14)=select(a_1748, J_14) | i1=J_14))). % 20.15/8.85 tff(c_3652, plain, (![J_14]: (select(a_1752, J_14)=select(a_1751, J_14) | i45=J_14))). % 20.15/8.85 tff(c_3616, plain, (![J_14]: (select(a_1707, J_14)=select(a_1706, J_14) | i8=J_14))). % 20.15/8.85 tff(c_3445, plain, (![J_14]: (select(a_1766, J_14)=select(a_1765, J_14) | i27=J_14))). % 20.15/8.85 tff(c_3240, plain, (select(a_1773, i47)=e47)). % 20.15/8.85 tff(c_3222, plain, (select(a_1775, i26)=e26)). % 20.15/8.85 tff(c_3237, plain, (select(a_1759, i40)=e40)). % 20.15/8.85 tff(c_3150, plain, (select(a_1741, i42)=e42)). % 20.15/8.85 tff(c_3234, plain, (select(a_1710, i11)=e11)). % 20.15/8.85 tff(c_3231, plain, (select(a_1714, i15)=e15)). % 20.15/8.85 tff(c_3147, plain, (select(a_1723, i24)=e24)). % 20.15/8.85 tff(c_3156, plain, (select(a_1794, i32)=e32)). % 20.15/8.85 tff(c_3153, plain, (select(a_1708, i9)=e9)). % 20.15/8.85 tff(c_3105, plain, (select(a_1792, i12)=e12)). % 20.15/8.85 tff(c_3243, plain, (select(a_1719, i20)=e20)). % 20.15/8.85 tff(c_3144, plain, (select(a_1778, i36)=e36)). % 20.15/8.85 tff(c_3228, plain, (select(a_1718, i19)=e19)). % 20.15/8.85 tff(c_3225, plain, (select(a_1700, i1)=e1)). % 20.15/8.85 tff(c_3108, plain, (select(a_1777, i11)=e11)). % 20.15/8.85 tff(c_3219, plain, (select(a_1748, i49)=e49)). % 20.15/8.85 tff(c_3141, plain, (select(a_1716, i17)=e17)). % 20.15/8.85 tff(c_3246, plain, (select(a_1730, i31)=e31)). % 20.15/8.85 tff(c_3216, plain, (select(a_1796, i24)=e24)). % 20.15/8.85 tff(c_3084, plain, (select(a_1704, i5)=e5)). % 20.15/8.85 tff(c_3249, plain, (select(a_1757, i39)=e39)). % 20.15/8.86 tff(c_3210, plain, (select(a_1715, i16)=e16)). % 20.15/8.86 tff(c_3102, plain, (select(a_1783, i46)=e46)). % 20.15/8.86 tff(c_3213, plain, (select(a_1753, i43)=e43)). % 20.15/8.86 tff(c_3138, plain, (select(a_1739, i40)=e40)). % 20.15/8.86 tff(c_3072, plain, (select(a_1734, i35)=e35)). % 20.15/8.86 tff(c_3357, plain, (select(a_1779, i44)=e44)). % 20.15/8.86 tff(c_3183, plain, (select(a_1706, i7)=e7)). % 20.15/8.86 tff(c_3324, plain, (select(a_1784, i35)=e35)). % 20.15/8.86 tff(c_3186, plain, (select(a_1727, i28)=e28)). % 20.15/8.86 tff(c_3297, plain, (select(a_1712, i13)=e13)). % 20.15/8.86 tff(c_3309, plain, (select(a_1776, i34)=e34)). % 20.15/8.86 tff(c_3318, plain, (select(a_1789, i29)=e29)). % 20.15/8.86 tff(c_3126, plain, (select(a_1745, i46)=e46)). % 20.15/8.86 tff(c_3312, plain, (select(a_1758, i20)=e20)). % 20.15/8.86 tff(c_3306, plain, (select(a_1799, i1)=e1)). % 20.15/8.86 tff(c_3303, plain, (select(a_1740, i41)=e41)). % 20.15/8.86 tff(c_3123, plain, (select(a_1729, i30)=e30)). % 20.15/8.86 tff(c_3315, plain, (select(a_1731, i32)=e32)). % 20.15/8.86 tff(c_3300, plain, (select(a_1765, i6)=e6)). % 20.15/8.86 tff(c_3177, plain, (select(a_1793, i5)=e5)). % 20.15/8.86 tff(c_3321, plain, (select(a_1750, i41)=e41)). % 20.15/8.86 tff(c_3189, plain, (select(a_1788, i48)=e48)). % 20.15/8.86 tff(c_3192, plain, (select(a_1738, i39)=e39)). % 20.15/8.86 tff(c_3093, plain, (select(a_1711, i12)=e12)). % 20.15/8.86 tff(c_3078, plain, (select(a_1721, i22)=e22)). % 20.15/8.86 tff(c_3195, plain, (select(a_1774, i18)=e18)). % 20.15/8.86 tff(c_3180, plain, (select(a_1705, i6)=e6)). % 20.15/8.86 tff(c_3333, plain, (select(a_1771, i17)=e17)). % 20.15/8.86 tff(c_3096, plain, (select(a_1725, i26)=e26)). % 20.15/8.86 tff(c_3174, plain, (select(a_1749, i1)=e1)). % 20.15/8.86 tff(c_3129, plain, (select(a_1726, i27)=e27)). % 20.15/8.86 tff(c_3294, plain, (select(a_1798, i31)=e31)). % 20.15/8.86 tff(c_3291, plain, (select(a_1707, i8)=e8)). % 20.15/8.86 tff(c_3327, plain, (select(a_1752, i45)=e45)). % 20.15/8.86 tff(c_3120, plain, (select(a_1766, i27)=e27)). % 20.15/8.86 tff(c_3288, plain, (select(a_1763, i14)=e14)). % 20.15/8.86 tff(c_3330, plain, (select(a_1733, i34)=e34)). % 20.15/8.86 tff(c_3285, plain, (select(a_1756, i22)=e22)). % 20.15/8.86 tff(c_3201, plain, (select(a_1767, i15)=e15)). % 20.15/8.86 tff(c_3282, plain, (select(a_1781, i23)=e23)). % 20.15/8.86 tff(c_3171, plain, (select(a_1709, i10)=e10)). % 20.15/8.86 tff(c_3198, plain, (select(a_1703, i4)=e4)). % 20.15/8.86 tff(c_3279, plain, (select(a_1770, i9)=e9)). % 20.15/8.86 tff(c_3336, plain, (select(a_1791, i37)=e37)). % 20.15/8.86 tff(c_3339, plain, (select(a_1737, i38)=e38)). % 20.15/8.86 tff(c_3132, plain, (select(a_1754, i28)=e28)). % 20.15/8.86 tff(c_3090, plain, (select(a_1743, i44)=e44)). % 20.15/8.86 tff(c_3204, plain, (select(a_1751, i30)=e30)). % 20.15/8.86 tff(c_3117, plain, (select(a_1768, i7)=e7)). % 20.15/8.86 tff(c_3345, plain, (select(a_1724, i25)=e25)). % 20.15/8.86 tff(c_3168, plain, (select(a_1787, i10)=e10)). % 20.15/8.86 tff(c_3276, plain, (select(a_1782, i25)=e25)). % 20.15/8.86 tff(c_3342, plain, (select(a_1762, i49)=e49)). % 20.15/8.86 tff(c_3273, plain, (select(a_1701, i2)=e2)). % 20.15/8.86 tff(c_3270, plain, (select(a_1785, i50)=e50)). % 20.15/8.86 tff(c_3267, plain, (select(a_1760, i16)=e16)). % 20.15/8.86 tff(c_3348, plain, (select(a_1742, i43)=e43)). % 20.15/8.86 tff(c_3252, plain, (select(a_1795, i4)=e4)). % 20.15/8.86 tff(c_3081, plain, (select(a_1746, i47)=e47)). % 20.15/8.86 tff(c_3114, plain, (select(a_1744, i45)=e45)). % 20.15/8.86 tff(c_3135, plain, (select(a_1735, i36)=e36)). % 20.15/8.86 tff(c_3165, plain, (select(a_1736, i37)=e37)). % 20.15/8.86 tff(c_3264, plain, (select(a_1747, i48)=e48)). % 20.15/8.86 tff(c_3261, plain, (select(a_1722, i23)=e23)). % 20.15/8.86 tff(c_3099, plain, (select(a_1769, i33)=e33)). % 20.15/8.86 tff(c_3162, plain, (select(a_1797, i21)=e21)). % 20.15/8.86 tff(c_3255, plain, (select(a_1790, i3)=e3)). % 20.15/8.87 tff(c_3207, plain, (select(a_1702, i3)=e3)). % 20.15/8.87 tff(c_3258, plain, (select(a_1755, i19)=e19)). % 20.15/8.87 tff(c_3351, plain, (select(a_1772, i42)=e42)). % 20.15/8.87 tff(c_3354, plain, (select(a_1728, i29)=e29)). % 20.15/8.87 tff(c_3159, plain, (select(a_1732, i33)=e33)). % 20.15/8.87 tff(c_3111, plain, (select(a_1764, i13)=e13)). % 20.15/8.87 tff(c_3087, plain, (select(a_1713, i14)=e14)). % 20.15/8.87 tff(c_3075, plain, (select(a_1717, i18)=e18)). % 20.15/8.87 tff(c_3069, plain, (select(a_1761, i8)=e8)). % 20.15/8.87 tff(c_3360, plain, (select(a_1720, i21)=e21)). % 20.15/8.87 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))). % 20.15/8.87 tff(c_3363, plain, (select(a_1780, i38)=e38)). % 20.15/8.87 tff(c_3066, plain, (select(a_1786, i2)=e2)). % 20.15/8.87 tff(c_2, plain, (![A_1, I_2, E_3]: (select(store(A_1, I_2, E_3), I_2)=E_3))). % 20.15/8.87 tff(c_178, plain, (store(a_1785, i2, e2)=a_1786)). % 20.15/8.87 tff(c_128, plain, (store(a_1760, i8, e8)=a_1761)). % 20.15/8.87 tff(c_74, plain, (store(a_1733, i35, e35)=a_1734)). % 20.15/8.87 tff(c_40, plain, (store(a_1716, i18, e18)=a_1717)). % 20.15/8.87 tff(c_48, plain, (store(a_1720, i22, e22)=a_1721)). % 20.15/8.87 tff(c_98, plain, (store(a_1745, i47, e47)=a_1746)). % 20.15/8.87 tff(c_14, plain, (store(a_1703, i5, e5)=a_1704)). % 20.15/8.87 tff(c_32, plain, (store(a_1712, i14, e14)=a_1713)). % 20.15/8.87 tff(c_92, plain, (store(a_1742, i44, e44)=a_1743)). % 20.15/8.87 tff(c_28, plain, (store(a_1710, i12, e12)=a_1711)). % 20.15/8.87 tff(c_56, plain, (store(a_1724, i26, e26)=a_1725)). % 20.15/8.87 tff(c_144, plain, (store(a_1768, i33, e33)=a_1769)). % 20.15/8.87 tff(c_172, plain, (store(a_1782, i46, e46)=a_1783)). % 20.15/8.87 tff(c_190, plain, (store(a_1791, i12, e12)=a_1792)). % 20.15/8.87 tff(c_160, plain, (store(a_1776, i11, e11)=a_1777)). % 20.15/8.87 tff(c_134, plain, (store(a_1763, i13, e13)=a_1764)). % 20.15/8.87 tff(c_94, plain, (store(a_1743, i45, e45)=a_1744)). % 20.15/8.87 tff(c_142, plain, (store(a_1767, i7, e7)=a_1768)). % 20.15/8.87 tff(c_138, plain, (store(a_1765, i27, e27)=a_1766)). % 20.15/8.87 tff(c_64, plain, (store(a_1728, i30, e30)=a_1729)). % 20.15/8.87 tff(c_96, plain, (store(a_1744, i46, e46)=a_1745)). % 20.15/8.87 tff(c_58, plain, (store(a_1725, i27, e27)=a_1726)). % 20.15/8.87 tff(c_114, plain, (store(a_1753, i28, e28)=a_1754)). % 20.15/8.87 tff(c_76, plain, (store(a_1734, i36, e36)=a_1735)). % 20.15/8.87 tff(c_84, plain, (store(a_1738, i40, e40)=a_1739)). % 20.15/8.87 tff(c_38, plain, (store(a_1715, i17, e17)=a_1716)). % 20.15/8.87 tff(c_162, plain, (store(a_1777, i36, e36)=a_1778)). % 20.15/8.87 tff(c_52, plain, (store(a_1722, i24, e24)=a_1723)). % 20.15/8.87 tff(c_88, plain, (store(a_1740, i42, e42)=a_1741)). % 20.15/8.87 tff(c_22, plain, (store(a_1707, i9, e9)=a_1708)). % 20.15/8.87 tff(c_194, plain, (store(a_1793, i32, e32)=a_1794)). % 20.15/8.87 tff(c_70, plain, (store(a_1731, i33, e33)=a_1732)). % 20.15/8.87 tff(c_200, plain, (store(a_1796, i21, e21)=a_1797)). % 20.15/8.87 tff(c_78, plain, (store(a_1735, i37, e37)=a_1736)). % 20.15/8.87 tff(c_180, plain, (store(a_1786, i10, e10)=a_1787)). % 20.15/8.87 tff(c_24, plain, (store(a_1708, i10, e10)=a_1709)). % 20.15/8.87 tff(c_104, plain, (store(a_1748, i1, e1)=a_1749)). % 20.15/8.87 tff(c_192, plain, (store(a_1792, i5, e5)=a_1793)). % 20.15/8.87 tff(c_16, plain, (store(a_1704, i6, e6)=a_1705)). % 20.15/8.87 tff(c_18, plain, (store(a_1705, i7, e7)=a_1706)). % 20.15/8.87 tff(c_60, plain, (store(a_1726, i28, e28)=a_1727)). % 20.15/8.87 tff(c_182, plain, (store(a_1787, i48, e48)=a_1788)). % 20.15/8.87 tff(c_82, plain, (store(a_1737, i39, e39)=a_1738)). % 20.15/8.87 tff(c_154, plain, (store(a_1773, i18, e18)=a_1774)). % 20.15/8.87 tff(c_12, plain, (store(a_1702, i4, e4)=a_1703)). % 20.15/8.87 tff(c_140, plain, (store(a_1766, i15, e15)=a_1767)). % 20.15/8.87 tff(c_108, plain, (store(a_1750, i30, e30)=a_1751)). % 20.15/8.87 tff(c_10, plain, (store(a_1701, i3, e3)=a_1702)). % 20.15/8.87 tff(c_36, plain, (store(a_1714, i16, e16)=a_1715)). % 20.15/8.87 tff(c_112, plain, (store(a_1752, i43, e43)=a_1753)). % 20.15/8.87 tff(c_198, plain, (store(a_1795, i24, e24)=a_1796)). % 20.15/8.87 tff(c_102, plain, (store(a_1747, i49, e49)=a_1748)). % 20.15/8.87 tff(c_156, plain, (store(a_1774, i26, e26)=a_1775)). % 20.15/8.87 tff(c_6, plain, (store(a1, i1, e1)=a_1700)). % 20.15/8.87 tff(c_42, plain, (store(a_1717, i19, e19)=a_1718)). % 20.15/8.87 tff(c_34, plain, (store(a_1713, i15, e15)=a_1714)). % 20.15/8.87 tff(c_26, plain, (store(a_1709, i11, e11)=a_1710)). % 20.15/8.87 tff(c_124, plain, (store(a_1758, i40, e40)=a_1759)). % 20.15/8.87 tff(c_152, plain, (store(a_1772, i47, e47)=a_1773)). % 20.15/8.88 tff(c_44, plain, (store(a_1718, i20, e20)=a_1719)). % 20.15/8.88 tff(c_66, plain, (store(a_1729, i31, e31)=a_1730)). % 20.15/8.88 tff(c_120, plain, (store(a_1756, i39, e39)=a_1757)). % 20.15/8.88 tff(c_196, plain, (store(a_1794, i4, e4)=a_1795)). % 20.15/8.88 tff(c_186, plain, (store(a_1789, i3, e3)=a_1790)). % 20.15/8.88 tff(c_116, plain, (store(a_1754, i19, e19)=a_1755)). % 20.15/8.88 tff(c_50, plain, (store(a_1721, i23, e23)=a_1722)). % 20.15/8.88 tff(c_100, plain, (store(a_1746, i48, e48)=a_1747)). % 20.15/8.88 tff(c_126, plain, (store(a_1759, i16, e16)=a_1760)). % 20.15/8.88 tff(c_176, plain, (store(a_1784, i50, e50)=a_1785)). % 20.15/8.88 tff(c_8, plain, (store(a_1700, i2, e2)=a_1701)). % 20.15/8.88 tff(c_170, plain, (store(a_1781, i25, e25)=a_1782)). % 20.15/8.88 tff(c_146, plain, (store(a_1769, i9, e9)=a_1770)). % 20.15/8.88 tff(c_168, plain, (store(a_1780, i23, e23)=a_1781)). % 20.15/8.88 tff(c_118, plain, (store(a_1755, i22, e22)=a_1756)). % 20.15/8.88 tff(c_132, plain, (store(a_1762, i14, e14)=a_1763)). % 20.15/8.88 tff(c_20, plain, (store(a_1706, i8, e8)=a_1707)). % 20.15/8.88 tff(c_202, plain, (store(a_1797, i31, e31)=a_1798)). % 20.15/8.88 tff(c_30, plain, (store(a_1711, i13, e13)=a_1712)). % 20.15/8.88 tff(c_136, plain, (store(a_1764, i6, e6)=a_1765)). % 20.15/8.88 tff(c_86, plain, (store(a_1739, i41, e41)=a_1740)). % 20.15/8.88 tff(c_204, plain, (store(a_1798, i1, e1)=a_1799)). % 20.15/8.88 tff(c_158, plain, (store(a_1775, i34, e34)=a_1776)). % 20.15/8.88 tff(c_122, plain, (store(a_1757, i20, e20)=a_1758)). % 20.15/8.88 tff(c_68, plain, (store(a_1730, i32, e32)=a_1731)). % 20.15/8.88 tff(c_184, plain, (store(a_1788, i29, e29)=a_1789)). % 20.15/8.88 tff(c_106, plain, (store(a1, i41, e41)=a_1750)). % 20.15/8.88 tff(c_174, plain, (store(a_1783, i35, e35)=a_1784)). % 20.15/8.88 tff(c_110, plain, (store(a_1751, i45, e45)=a_1752)). % 20.15/8.88 tff(c_72, plain, (store(a_1732, i34, e34)=a_1733)). % 20.15/8.88 tff(c_148, plain, (store(a_1770, i17, e17)=a_1771)). % 20.15/8.88 tff(c_188, plain, (store(a_1790, i37, e37)=a_1791)). % 20.15/8.88 tff(c_80, plain, (store(a_1736, i38, e38)=a_1737)). % 20.15/8.88 tff(c_130, plain, (store(a_1761, i49, e49)=a_1762)). % 20.15/8.88 tff(c_54, plain, (store(a_1723, i25, e25)=a_1724)). % 20.15/8.88 tff(c_90, plain, (store(a_1741, i43, e43)=a_1742)). % 20.15/8.88 tff(c_150, plain, (store(a_1771, i42, e42)=a_1772)). % 20.15/8.88 tff(c_62, plain, (store(a_1727, i29, e29)=a_1728)). % 20.15/8.88 tff(c_164, plain, (store(a_1778, i44, e44)=a_1779)). % 20.15/8.88 tff(c_46, plain, (store(a_1719, i21, e21)=a_1720)). % 20.15/8.88 tff(c_166, plain, (store(a_1779, i38, e38)=a_1780)). % 20.15/8.88 tff(c_400, plain, (i44!=i36)). % 20.15/8.88 tff(c_742, plain, (i35!=i27)). % 20.15/8.88 tff(c_2240, plain, (i5!=i23)). % 20.15/8.88 tff(c_1014, plain, (i24!=i22)). % 20.15/8.88 tff(c_222, plain, (i48!=i46)). % 20.15/8.88 tff(c_206, plain, (i50!=i49)). % 20.15/8.88 tff(c_1712, plain, (i38!=i11)). % 20.15/8.88 tff(c_426, plain, (i45!=i35)). % 20.15/8.88 tff(c_2024, plain, (i7!=i44)). % 20.15/8.88 tff(c_1068, plain, (i25!=i21)). % 20.15/8.88 tff(c_1812, plain, (i27!=i10)). % 20.15/8.88 tff(c_1206, plain, (i46!=i18)). % 20.15/8.88 tff(c_1110, plain, (i33!=i20)). % 20.15/8.88 tff(c_1290, plain, (i36!=i17)). % 20.15/8.88 tff(c_1486, plain, (i40!=i14)). % 20.15/8.88 tff(c_2542, plain, (i2!=i10)). % 20.15/8.88 tff(c_1790, plain, (i38!=i10)). % 20.15/8.88 tff(c_1390, plain, (i19!=i16)). % 20.15/8.88 tff(c_794, plain, (i32!=i26)). % 20.15/8.88 tff(c_652, plain, (i37!=i29)). % 20.15/8.88 tff(c_1996, plain, (i8!=i16)). % 20.15/8.88 tff(c_342, plain, (i48!=i38)). % 20.15/8.88 tff(c_864, plain, (i46!=i24)). % 20.15/8.88 tff(c_1934, plain, (i8!=i47)). % 20.15/8.88 tff(c_2560, plain, (i49!=i1)). % 20.15/8.88 tff(c_1524, plain, (i21!=i14)). % 20.15/8.88 tff(c_1852, plain, (i9!=i47)). % 20.15/8.88 tff(c_1118, plain, (i29!=i20)). % 20.15/8.88 tff(c_2076, plain, (i7!=i18)). % 20.15/8.88 tff(c_434, plain, (i41!=i35)). % 20.15/8.88 tff(c_1034, plain, (i42!=i21)). % 20.15/8.88 tff(c_2108, plain, (i6!=i45)). % 20.15/8.88 tff(c_442, plain, (i37!=i35)). % 20.15/8.88 tff(c_1752, plain, (i18!=i11)). % 20.15/8.88 tff(c_1106, plain, (i35!=i20)). % 20.15/8.88 tff(c_1254, plain, (i22!=i18)). % 20.15/8.88 tff(c_1730, plain, (i29!=i11)). % 20.15/8.88 tff(c_2006, plain, (i8!=i11)). % 20.15/8.88 tff(c_208, plain, (i50!=i48)). % 20.15/8.88 tff(c_2588, plain, (i35!=i1)). % 20.15/8.88 tff(c_1432, plain, (i32!=i15)). % 20.15/8.88 tff(c_784, plain, (i37!=i26)). % 20.15/8.88 tff(c_508, plain, (i35!=i33)). % 20.15/8.88 tff(c_540, plain, (i36!=i32)). % 20.15/8.88 tff(c_376, plain, (i43!=i37)). % 20.15/8.88 tff(c_1468, plain, (i49!=i14)). % 20.15/8.88 tff(c_1508, plain, (i29!=i14)). % 20.15/8.88 tff(c_1716, plain, (i36!=i11)). % 20.15/8.88 tff(c_440, plain, (i38!=i35)). % 20.15/8.88 tff(c_2544, plain, (i9!=i2)). % 20.15/8.88 tff(c_838, plain, (i34!=i25)). % 20.15/8.88 tff(c_1414, plain, (i41!=i15)). % 20.15/8.88 tff(c_938, plain, (i35!=i23)). % 20.15/8.89 tff(c_504, plain, (i37!=i33)). % 20.15/8.89 tff(c_380, plain, (i41!=i37)). % 20.15/8.89 tff(c_396, plain, (i46!=i36)). % 20.15/8.89 tff(c_2470, plain, (i46!=i2)). % 20.15/8.89 tff(c_2050, plain, (i7!=i31)). % 20.15/8.89 tff(c_1426, plain, (i35!=i15)). % 20.15/8.89 tff(c_2070, plain, (i7!=i21)). % 20.15/8.89 tff(c_2284, plain, (i46!=i4)). % 20.15/8.89 tff(c_2314, plain, (i4!=i31)). % 20.15/8.89 tff(c_578, plain, (i35!=i31)). % 20.15/8.89 tff(c_2448, plain, (i3!=i10)). % 20.15/8.89 tff(c_2494, plain, (i34!=i2)). % 20.15/8.89 tff(c_830, plain, (i38!=i25)). % 20.15/8.89 tff(c_682, plain, (i43!=i28)). % 20.15/8.89 tff(c_1884, plain, (i9!=i31)). % 20.15/8.89 tff(c_1528, plain, (i19!=i14)). % 20.15/8.89 tff(c_1266, plain, (i48!=i17)). % 20.15/8.89 tff(c_1384, plain, (i22!=i16)). % 20.15/8.89 tff(c_1108, plain, (i34!=i20)). % 20.15/8.89 tff(c_832, plain, (i37!=i25)). % 20.15/8.89 tff(c_1072, plain, (i23!=i21)). % 20.15/8.89 tff(c_1678, plain, (i17!=i12)). % 20.15/8.89 tff(c_1646, plain, (i33!=i12)). % 20.15/8.89 tff(c_1858, plain, (i9!=i44)). % 20.15/8.89 tff(c_694, plain, (i37!=i28)). % 20.15/8.89 tff(c_1460, plain, (i18!=i15)). % 20.15/8.89 tff(c_1978, plain, (i8!=i25)). % 20.15/8.89 tff(c_280, plain, (i49!=i41)). % 20.15/8.89 tff(c_702, plain, (i33!=i28)). % 20.15/8.89 tff(c_1984, plain, (i8!=i22)). % 20.15/8.89 tff(c_1102, plain, (i37!=i20)). % 20.15/8.89 tff(c_1850, plain, (i9!=i48)). % 20.15/8.89 tff(c_1608, plain, (i15!=i13)). % 20.15/8.89 tff(c_1936, plain, (i8!=i46)). % 20.15/8.89 tff(c_2352, plain, (i4!=i12)). % 20.15/8.89 tff(c_2498, plain, (i32!=i2)). % 20.15/8.89 tff(c_1074, plain, (i22!=i21)). % 20.15/8.89 tff(c_1258, plain, (i20!=i18)). % 20.15/8.89 tff(c_1920, plain, (i9!=i13)). % 20.15/8.89 tff(c_1368, plain, (i30!=i16)). % 20.15/8.89 tff(c_532, plain, (i40!=i32)). % 20.15/8.89 tff(c_1166, plain, (i35!=i19)). % 20.15/8.89 tff(c_1636, plain, (i38!=i12)). % 20.15/8.89 tff(c_2064, plain, (i7!=i24)). % 20.15/8.89 tff(c_394, plain, (i47!=i36)). % 20.15/8.89 tff(c_2406, plain, (i31!=i3)). % 20.15/8.89 tff(c_1104, plain, (i36!=i20)). % 20.15/8.89 tff(c_1624, plain, (i44!=i12)). % 20.15/8.89 tff(c_2096, plain, (i8!=i7)). % 20.15/8.89 tff(c_1818, plain, (i24!=i10)). % 20.15/8.89 tff(c_518, plain, (i47!=i32)). % 20.15/8.89 tff(c_1746, plain, (i21!=i11)). % 20.15/8.89 tff(c_1590, plain, (i24!=i13)). % 20.15/8.89 tff(c_2574, plain, (i42!=i1)). % 20.15/8.89 tff(c_2590, plain, (i34!=i1)). % 20.15/8.89 tff(c_1894, plain, (i9!=i26)). % 20.15/8.89 tff(c_556, plain, (i46!=i31)). % 20.15/8.89 tff(c_2312, plain, (i4!=i32)). % 20.15/8.89 tff(c_264, plain, (i49!=i42)). % 20.15/8.89 tff(c_854, plain, (i26!=i25)). % 20.15/8.89 tff(c_2258, plain, (i5!=i14)). % 20.15/8.89 tff(c_2244, plain, (i5!=i21)). % 20.15/8.89 tff(c_1938, plain, (i8!=i45)). % 20.15/8.89 tff(c_1320, plain, (i21!=i17)). % 20.15/8.89 tff(c_1152, plain, (i42!=i19)). % 20.15/8.89 tff(c_522, plain, (i45!=i32)). % 20.15/8.89 tff(c_2286, plain, (i45!=i4)). % 20.15/8.89 tff(c_692, plain, (i38!=i28)). % 20.15/8.89 tff(c_1332, plain, (i48!=i16)). % 20.15/8.89 tff(c_2228, plain, (i5!=i29)). % 20.15/8.89 tff(c_2468, plain, (i47!=i2)). % 20.15/8.89 tff(c_306, plain, (i45!=i40)). % 20.15/8.89 tff(c_384, plain, (i39!=i37)). % 20.15/8.89 tff(c_1956, plain, (i8!=i36)). % 20.15/8.89 tff(c_1890, plain, (i9!=i28)). % 20.15/8.89 tff(c_1674, plain, (i19!=i12)). % 20.15/8.89 tff(c_1734, plain, (i27!=i11)). % 20.15/8.89 tff(c_510, plain, (i34!=i33)). % 20.15/8.89 tff(c_1172, plain, (i32!=i19)). % 20.15/8.89 tff(c_2002, plain, (i8!=i13)). % 20.15/8.89 tff(c_1190, plain, (i23!=i19)). % 20.15/8.89 tff(c_1536, plain, (i15!=i14)). % 20.15/8.89 tff(c_2318, plain, (i4!=i29)). % 20.15/8.89 tff(c_1004, plain, (i29!=i22)). % 20.15/8.89 tff(c_266, plain, (i48!=i42)). % 20.15/8.89 tff(c_502, plain, (i38!=i33)). % 20.15/8.89 tff(c_2216, plain, (i5!=i35)). % 20.15/8.89 tff(c_2438, plain, (i3!=i15)). % 20.15/8.89 tff(c_390, plain, (i49!=i36)). % 20.15/8.89 tff(c_676, plain, (i46!=i28)). % 20.15/8.89 tff(c_298, plain, (i49!=i40)). % 20.15/8.89 tff(c_2514, plain, (i24!=i2)). % 20.15/8.89 tff(c_878, plain, (i39!=i24)). % 20.15/8.89 tff(c_920, plain, (i44!=i23)). % 20.15/8.89 tff(c_1360, plain, (i34!=i16)). % 20.15/8.89 tff(c_2048, plain, (i7!=i32)). % 20.15/8.89 tff(c_1560, plain, (i39!=i13)). % 20.15/8.89 tff(c_858, plain, (i49!=i24)). % 20.15/8.89 tff(c_392, plain, (i48!=i36)). % 20.15/8.89 tff(c_616, plain, (i35!=i30)). % 20.15/8.89 tff(c_330, plain, (i43!=i39)). % 20.15/8.89 tff(c_470, plain, (i38!=i34)). % 20.15/8.89 tff(c_2170, plain, (i6!=i14)). % 20.15/8.89 tff(c_2362, plain, (i7!=i4)). % 20.15/8.89 tff(c_1970, plain, (i8!=i29)). % 20.15/8.89 tff(c_560, plain, (i44!=i31)). % 20.15/8.89 tff(c_2622, plain, (i18!=i1)). % 20.15/8.89 tff(c_1706, plain, (i41!=i11)). % 20.15/8.89 tff(c_2056, plain, (i7!=i28)). % 20.15/8.89 tff(c_1982, plain, (i8!=i23)). % 20.15/8.89 tff(c_506, plain, (i36!=i33)). % 20.15/8.89 tff(c_410, plain, (i39!=i36)). % 20.15/8.89 tff(c_790, plain, (i34!=i26)). % 20.15/8.89 tff(c_2612, plain, (i23!=i1)). % 20.15/8.89 tff(c_1926, plain, (i9!=i10)). % 20.15/8.89 tff(c_688, plain, (i40!=i28)). % 20.15/8.89 tff(c_808, plain, (i49!=i25)). % 20.15/8.90 tff(c_768, plain, (i45!=i26)). % 20.15/8.90 tff(c_450, plain, (i48!=i34)). % 20.15/8.90 tff(c_228, plain, (i49!=i45)). % 20.15/8.90 tff(c_1548, plain, (i45!=i13)). % 20.15/8.90 tff(c_1404, plain, (i46!=i15)). % 20.15/8.90 tff(c_2260, plain, (i5!=i13)). % 20.15/8.90 tff(c_1860, plain, (i9!=i43)). % 20.15/8.90 tff(c_2490, plain, (i36!=i2)). % 20.15/8.90 tff(c_1196, plain, (i20!=i19)). % 20.15/8.90 tff(c_1272, plain, (i45!=i17)). % 20.15/8.90 tff(c_2176, plain, (i6!=i11)). % 20.15/8.90 tff(c_2134, plain, (i6!=i32)). % 20.15/8.90 tff(c_1768, plain, (i49!=i10)). % 20.15/8.90 tff(c_1090, plain, (i43!=i20)). % 20.15/8.90 tff(c_1582, plain, (i28!=i13)). % 20.15/8.90 tff(c_2230, plain, (i5!=i28)). % 20.15/8.90 tff(c_1238, plain, (i30!=i18)). % 20.15/8.90 tff(c_252, plain, (i48!=i43)). % 20.15/8.90 tff(c_1846, plain, (i9!=i50)). % 20.15/8.90 tff(c_418, plain, (i49!=i35)). % 20.15/8.90 tff(c_1774, plain, (i46!=i10)). % 20.15/8.90 tff(c_1962, plain, (i8!=i33)). % 20.15/8.90 tff(c_1808, plain, (i29!=i10)). % 20.15/8.90 tff(c_486, plain, (i46!=i33)). % 20.15/8.90 tff(c_1652, plain, (i30!=i12)). % 20.15/8.90 tff(c_890, plain, (i33!=i24)). % 20.15/8.90 tff(c_1064, plain, (i27!=i21)). % 20.15/8.90 tff(c_2474, plain, (i44!=i2)). % 20.15/8.90 tff(c_1762, plain, (i13!=i11)). % 20.15/8.90 tff(c_230, plain, (i48!=i45)). % 20.15/8.90 tff(c_236, plain, (i50!=i44)). % 20.15/8.90 tff(c_1534, plain, (i16!=i14)). % 20.15/8.90 tff(c_2524, plain, (i2!=i19)). % 20.15/8.90 tff(c_1578, plain, (i30!=i13)). % 20.15/8.90 tff(c_2088, plain, (i7!=i12)). % 20.15/8.90 tff(c_542, plain, (i35!=i32)). % 20.15/8.90 tff(c_884, plain, (i36!=i24)). % 20.15/8.90 tff(c_874, plain, (i41!=i24)). % 20.15/8.90 tff(c_276, plain, (i43!=i42)). % 20.15/8.90 tff(c_2500, plain, (i31!=i2)). % 20.15/8.90 tff(c_1028, plain, (i45!=i21)). % 20.15/8.90 tff(c_1922, plain, (i9!=i12)). % 20.15/8.90 tff(c_1918, plain, (i9!=i14)). % 20.15/8.90 tff(c_1694, plain, (i47!=i11)). % 20.15/8.90 tff(c_1354, plain, (i37!=i16)). % 20.15/8.90 tff(c_338, plain, (i50!=i38)). % 20.15/8.90 tff(c_1820, plain, (i23!=i10)). % 20.15/8.90 tff(c_2030, plain, (i7!=i41)). % 20.15/8.90 tff(c_690, plain, (i39!=i28)). % 20.15/8.90 tff(c_1770, plain, (i48!=i10)). % 20.15/8.90 tff(c_1874, plain, (i9!=i36)). % 20.15/8.90 tff(c_1554, plain, (i42!=i13)). % 20.15/8.90 tff(c_1676, plain, (i18!=i12)). % 20.15/8.90 tff(c_1130, plain, (i23!=i20)). % 20.15/8.90 tff(c_1672, plain, (i20!=i12)). % 20.15/8.90 tff(c_1148, plain, (i44!=i19)). % 20.15/8.90 tff(c_1758, plain, (i15!=i11)). % 20.15/8.90 tff(c_1802, plain, (i32!=i10)). % 20.15/8.90 tff(c_748, plain, (i32!=i27)). % 20.15/8.90 tff(c_1604, plain, (i17!=i13)). % 20.15/8.90 tff(c_2138, plain, (i6!=i30)). % 20.15/8.90 tff(c_806, plain, (i50!=i25)). % 20.15/8.90 tff(c_234, plain, (i46!=i45)). % 20.15/8.90 tff(c_984, plain, (i39!=i22)). % 20.15/8.90 tff(c_1288, plain, (i37!=i17)). % 20.15/8.90 tff(c_1942, plain, (i8!=i43)). % 20.15/8.90 tff(c_1718, plain, (i35!=i11)). % 20.15/8.90 tff(c_2548, plain, (i7!=i2)). % 20.15/8.90 tff(c_1622, plain, (i45!=i12)). % 20.15/8.90 tff(c_612, plain, (i37!=i30)). % 20.15/8.90 tff(c_1082, plain, (i47!=i20)). % 20.15/8.90 tff(c_828, plain, (i39!=i25)). % 20.15/8.90 tff(c_628, plain, (i49!=i29)). % 20.15/8.90 tff(c_630, plain, (i48!=i29)). % 20.15/8.90 tff(c_436, plain, (i40!=i35)). % 20.15/8.90 tff(c_1164, plain, (i36!=i19)). % 20.15/8.90 tff(c_2532, plain, (i2!=i15)). % 20.15/8.90 tff(c_994, plain, (i34!=i22)). % 20.15/8.90 tff(c_2388, plain, (i40!=i3)). % 20.15/8.90 tff(c_2204, plain, (i5!=i41)). % 20.15/8.90 tff(c_2350, plain, (i4!=i13)). % 20.15/8.90 tff(c_2114, plain, (i6!=i42)). % 20.15/8.90 tff(c_2380, plain, (i44!=i3)). % 20.15/8.90 tff(c_316, plain, (i50!=i39)). % 20.15/8.90 tff(c_1328, plain, (i50!=i16)). % 20.15/8.90 tff(c_2522, plain, (i20!=i2)). % 20.15/8.90 tff(c_2212, plain, (i5!=i37)). % 20.15/8.90 tff(c_2074, plain, (i7!=i19)). % 20.15/8.90 tff(c_1998, plain, (i8!=i15)). % 20.15/8.90 tff(c_2124, plain, (i6!=i37)). % 20.15/8.90 tff(c_360, plain, (i39!=i38)). % 20.15/8.90 tff(c_512, plain, (i50!=i32)). % 20.15/8.90 tff(c_2466, plain, (i48!=i2)). % 20.15/8.90 tff(c_1964, plain, (i8!=i32)). % 20.15/8.90 tff(c_1026, plain, (i46!=i21)). % 20.15/8.90 tff(c_1568, plain, (i35!=i13)). % 20.15/8.90 tff(c_1372, plain, (i28!=i16)). % 20.15/8.90 tff(c_2198, plain, (i5!=i44)). % 20.15/8.90 tff(c_1724, plain, (i32!=i11)). % 20.15/8.90 tff(c_1766, plain, (i50!=i10)). % 20.48/8.90 tff(c_474, plain, (i36!=i34)). % 20.48/8.90 tff(c_300, plain, (i48!=i40)). % 20.48/8.90 tff(c_2358, plain, (i9!=i4)). % 20.48/8.90 tff(c_2152, plain, (i6!=i23)). % 20.48/8.90 tff(c_2222, plain, (i5!=i32)). % 20.48/8.90 tff(c_2492, plain, (i35!=i2)). % 20.48/8.90 tff(c_2242, plain, (i5!=i22)). % 20.48/8.90 tff(c_1058, plain, (i30!=i21)). % 20.48/8.90 tff(c_1764, plain, (i12!=i11)). % 20.48/8.90 tff(c_478, plain, (i50!=i33)). % 20.48/8.90 tff(c_1552, plain, (i43!=i13)). % 20.48/8.90 tff(c_340, plain, (i49!=i38)). % 20.48/8.90 tff(c_1080, plain, (i48!=i20)). % 20.48/8.90 tff(c_424, plain, (i46!=i35)). % 20.48/8.90 tff(c_620, plain, (i33!=i30)). % 20.48/8.90 tff(c_916, plain, (i46!=i23)). % 20.48/8.90 tff(c_350, plain, (i44!=i38)). % 20.48/8.90 tff(c_1350, plain, (i39!=i16)). % 20.48/8.90 tff(c_2308, plain, (i4!=i34)). % 20.48/8.90 tff(c_1126, plain, (i25!=i20)). % 20.48/8.90 tff(c_998, plain, (i32!=i22)). % 20.48/8.90 tff(c_2278, plain, (i49!=i4)). % 20.48/8.90 tff(c_2158, plain, (i6!=i20)). % 20.48/8.90 tff(c_1900, plain, (i9!=i23)). % 20.48/8.90 tff(c_2316, plain, (i4!=i30)). % 20.48/8.90 tff(c_314, plain, (i41!=i40)). % 20.48/8.90 tff(c_1256, plain, (i21!=i18)). % 20.48/8.90 tff(c_254, plain, (i47!=i43)). % 20.48/8.90 tff(c_860, plain, (i48!=i24)). % 20.48/8.90 tff(c_2478, plain, (i42!=i2)). % 20.48/8.90 tff(c_2028, plain, (i7!=i42)). % 20.48/8.90 tff(c_2116, plain, (i6!=i41)). % 20.48/8.90 tff(c_1430, plain, (i33!=i15)). % 20.48/8.90 tff(c_618, plain, (i34!=i30)). % 20.48/8.90 tff(c_662, plain, (i32!=i29)). % 20.48/8.90 tff(c_1340, plain, (i44!=i16)). % 20.48/8.90 tff(c_250, plain, (i49!=i43)). % 20.48/8.90 tff(c_996, plain, (i33!=i22)). % 20.48/8.90 tff(c_2394, plain, (i37!=i3)). % 20.48/8.90 tff(c_2340, plain, (i4!=i18)). % 20.48/8.90 tff(c_2082, plain, (i7!=i15)). % 20.48/8.90 tff(c_2072, plain, (i7!=i20)). % 20.48/8.90 tff(c_1824, plain, (i21!=i10)). % 20.48/8.90 tff(c_1492, plain, (i37!=i14)). % 20.48/8.90 tff(c_924, plain, (i42!=i23)). % 20.48/8.90 tff(c_1388, plain, (i20!=i16)). % 20.48/8.90 tff(c_1910, plain, (i9!=i18)). % 20.48/8.90 tff(c_210, plain, (i49!=i48)). % 20.48/8.90 tff(c_960, plain, (i24!=i23)). % 20.48/8.90 tff(c_888, plain, (i34!=i24)). % 20.48/8.91 tff(c_1210, plain, (i44!=i18)). % 20.48/8.91 tff(c_2264, plain, (i5!=i11)). % 20.48/8.91 tff(c_944, plain, (i32!=i23)). % 20.48/8.91 tff(c_422, plain, (i47!=i35)). % 20.48/8.91 tff(c_1262, plain, (i50!=i17)). % 20.48/8.91 tff(c_1178, plain, (i29!=i19)). % 20.48/8.91 tff(c_2366, plain, (i5!=i4)). % 20.48/8.91 tff(c_1908, plain, (i9!=i19)). % 20.48/8.91 tff(c_2046, plain, (i7!=i33)). % 20.48/8.91 tff(c_1348, plain, (i40!=i16)). % 20.48/8.91 tff(c_990, plain, (i36!=i22)). % 20.48/8.91 tff(c_2262, plain, (i5!=i12)). % 20.48/8.91 tff(c_2558, plain, (i50!=i1)). % 20.48/8.91 tff(c_2508, plain, (i27!=i2)). % 20.48/8.91 tff(c_1610, plain, (i14!=i13)). % 20.48/8.91 tff(c_940, plain, (i34!=i23)). % 20.48/8.91 tff(c_928, plain, (i40!=i23)). % 20.48/8.91 tff(c_258, plain, (i45!=i43)). % 20.48/8.91 tff(c_1550, plain, (i44!=i13)). % 20.48/8.91 tff(c_1066, plain, (i26!=i21)). % 20.48/8.91 tff(c_2100, plain, (i6!=i49)). % 20.48/8.91 tff(c_358, plain, (i40!=i38)). % 20.48/8.91 tff(c_372, plain, (i45!=i37)). % 20.48/8.91 tff(c_666, plain, (i30!=i29)). % 20.48/8.91 tff(c_1654, plain, (i29!=i12)). % 20.48/8.91 tff(c_926, plain, (i41!=i23)). % 20.48/8.91 tff(c_1396, plain, (i50!=i15)). % 20.48/8.91 tff(c_1760, plain, (i14!=i11)). % 20.48/8.91 tff(c_1438, plain, (i29!=i15)). % 20.48/8.91 tff(c_664, plain, (i31!=i29)). % 20.48/8.91 tff(c_654, plain, (i36!=i29)). % 20.48/8.91 tff(c_1940, plain, (i8!=i44)). % 20.48/8.91 tff(c_2648, plain, (i5!=i1)). % 20.48/8.91 tff(c_308, plain, (i44!=i40)). % 20.48/8.91 tff(c_644, plain, (i41!=i29)). % 20.48/8.91 tff(c_1252, plain, (i23!=i18)). % 20.48/8.91 tff(c_544, plain, (i34!=i32)). % 20.48/8.91 tff(c_356, plain, (i41!=i38)). % 20.48/8.91 tff(c_1062, plain, (i28!=i21)). % 20.48/8.91 tff(c_1896, plain, (i9!=i25)). % 20.48/8.91 tff(c_430, plain, (i43!=i35)). % 20.48/8.91 tff(c_2540, plain, (i2!=i11)). % 20.48/8.91 tff(c_2054, plain, (i7!=i29)). % 20.48/8.91 tff(c_2018, plain, (i7!=i47)). % 20.48/8.91 tff(c_1684, plain, (i14!=i12)). % 20.48/8.91 tff(c_292, plain, (i43!=i41)). % 20.48/8.91 tff(c_2640, plain, (i9!=i1)). % 20.48/8.91 tff(c_1078, plain, (i49!=i20)). % 20.48/8.91 tff(c_2294, plain, (i41!=i4)). % 20.48/8.91 tff(c_2446, plain, (i3!=i11)). % 20.48/8.91 tff(c_1412, plain, (i42!=i15)). % 20.48/8.91 tff(c_294, plain, (i42!=i41)). % 20.48/8.91 tff(c_514, plain, (i49!=i32)). % 20.48/8.91 tff(c_500, plain, (i39!=i33)). % 20.48/8.91 tff(c_238, plain, (i49!=i44)). % 20.48/8.91 tff(c_604, plain, (i41!=i30)). % 20.48/8.91 tff(c_974, plain, (i44!=i22)). % 20.48/8.91 tff(c_1792, plain, (i37!=i10)). % 20.48/8.91 tff(c_1912, plain, (i9!=i17)). % 20.48/8.91 tff(c_498, plain, (i40!=i33)). % 20.48/8.91 tff(c_1546, plain, (i46!=i13)). % 20.48/8.91 tff(c_772, plain, (i43!=i26)). % 20.48/8.91 tff(c_2364, plain, (i6!=i4)). % 20.48/8.91 tff(c_2430, plain, (i3!=i19)). % 20.48/8.91 tff(c_914, plain, (i47!=i23)). % 20.48/8.91 tff(c_2022, plain, (i7!=i45)). % 20.48/8.91 tff(c_1754, plain, (i17!=i11)). % 20.48/8.91 tff(c_848, plain, (i29!=i25)). % 20.48/8.91 tff(c_1856, plain, (i9!=i45)). % 20.48/8.91 tff(c_1702, plain, (i43!=i11)). % 20.48/8.91 tff(c_952, plain, (i28!=i23)). % 20.48/8.91 tff(c_1292, plain, (i35!=i17)). % 20.48/8.91 tff(c_334, plain, (i41!=i39)). % 20.48/8.91 tff(c_1744, plain, (i22!=i11)). % 20.48/8.91 tff(c_1382, plain, (i23!=i16)). % 20.48/8.91 tff(c_1958, plain, (i8!=i35)). % 20.48/8.91 tff(c_1084, plain, (i46!=i20)). % 20.48/8.91 tff(c_1924, plain, (i9!=i11)). % 20.48/8.91 tff(c_1114, plain, (i31!=i20)). % 20.48/8.91 tff(c_640, plain, (i43!=i29)). % 20.48/8.91 tff(c_948, plain, (i30!=i23)). % 20.48/8.91 tff(c_1864, plain, (i9!=i41)). % 20.48/8.91 tff(c_1782, plain, (i42!=i10)). % 20.48/8.91 tff(c_820, plain, (i43!=i25)). % 20.48/8.91 tff(c_1688, plain, (i50!=i11)). % 20.48/8.91 tff(c_2652, plain, (i3!=i1)). % 20.48/8.91 tff(c_2128, plain, (i6!=i35)). % 20.48/8.91 tff(c_1656, plain, (i28!=i12)). % 20.48/8.91 tff(c_778, plain, (i40!=i26)). % 20.48/8.91 tff(c_894, plain, (i31!=i24)). % 20.48/8.91 tff(c_1514, plain, (i26!=i14)). % 20.48/8.91 tff(c_1270, plain, (i46!=i17)). % 20.48/8.91 tff(c_2538, plain, (i2!=i12)). % 20.48/8.91 tff(c_2332, plain, (i4!=i22)). % 20.48/8.91 tff(c_2280, plain, (i48!=i4)). % 20.48/8.91 tff(c_896, plain, (i30!=i24)). % 20.48/8.91 tff(c_1168, plain, (i34!=i19)). % 20.48/8.91 tff(c_1974, plain, (i8!=i27)). % 20.48/8.91 tff(c_918, plain, (i45!=i23)). % 20.48/8.91 tff(c_2058, plain, (i7!=i27)). % 20.48/8.91 tff(c_2086, plain, (i7!=i13)). % 20.48/8.91 tff(c_2458, plain, (i5!=i3)). % 20.48/8.91 tff(c_1264, plain, (i49!=i17)). % 20.48/8.91 tff(c_1882, plain, (i9!=i32)). % 20.48/8.91 tff(c_1342, plain, (i43!=i16)). % 20.48/8.91 tff(c_2144, plain, (i6!=i27)). % 20.48/8.91 tff(c_1986, plain, (i8!=i21)). % 20.48/8.91 tff(c_1566, plain, (i36!=i13)). % 20.48/8.91 tff(c_1318, plain, (i22!=i17)). % 20.48/8.91 tff(c_922, plain, (i43!=i23)). % 20.48/8.91 tff(c_932, plain, (i38!=i23)). % 20.48/8.91 tff(c_476, plain, (i35!=i34)). % 20.48/8.91 tff(c_1120, plain, (i28!=i20)). % 20.48/8.91 tff(c_2140, plain, (i6!=i29)). % 20.48/8.91 tff(c_1204, plain, (i47!=i18)). % 20.48/8.91 tff(c_1344, plain, (i42!=i16)). % 20.48/8.91 tff(c_1664, plain, (i24!=i12)). % 20.48/8.91 tff(c_1192, plain, (i22!=i19)). % 20.48/8.91 tff(c_220, plain, (i49!=i46)). % 20.48/8.91 tff(c_1374, plain, (i27!=i16)). % 20.48/8.91 tff(c_570, plain, (i39!=i31)). % 20.48/8.91 tff(c_2246, plain, (i5!=i20)). % 20.48/8.91 tff(c_2368, plain, (i50!=i3)). % 20.48/8.91 tff(c_1780, plain, (i43!=i10)). % 20.48/8.91 tff(c_2156, plain, (i6!=i21)). % 20.48/8.91 tff(c_1370, plain, (i29!=i16)). % 20.48/8.91 tff(c_1032, plain, (i43!=i21)). % 20.48/8.91 tff(c_2014, plain, (i7!=i49)). % 20.48/8.91 tff(c_684, plain, (i42!=i28)). % 20.48/8.91 tff(c_1240, plain, (i29!=i18)). % 20.48/8.91 tff(c_1228, plain, (i35!=i18)). % 20.48/8.91 tff(c_448, plain, (i49!=i34)). % 20.48/8.91 tff(c_246, plain, (i45!=i44)). % 20.48/8.91 tff(c_1194, plain, (i21!=i19)). % 20.48/8.91 tff(c_1316, plain, (i23!=i17)). % 20.48/8.91 tff(c_466, plain, (i40!=i34)). % 20.48/8.91 tff(c_1362, plain, (i33!=i16)). % 20.48/8.91 tff(c_2296, plain, (i40!=i4)). % 20.48/8.91 tff(c_774, plain, (i42!=i26)). % 20.48/8.91 tff(c_414, plain, (i37!=i36)). % 20.48/8.91 tff(c_686, plain, (i41!=i28)). % 20.48/8.91 tff(c_2248, plain, (i5!=i19)). % 20.48/8.91 tff(c_840, plain, (i33!=i25)). % 20.48/8.91 tff(c_2320, plain, (i4!=i28)). % 20.48/8.91 tff(c_270, plain, (i46!=i42)). % 20.48/8.91 tff(c_420, plain, (i48!=i35)). % 20.48/8.91 tff(c_626, plain, (i50!=i29)). % 20.48/8.91 tff(c_2632, plain, (i13!=i1)). % 20.48/8.91 tff(c_836, plain, (i35!=i25)). % 20.48/8.91 tff(c_1200, plain, (i49!=i18)). % 20.48/8.91 tff(c_406, plain, (i41!=i36)). % 20.48/8.91 tff(c_1056, plain, (i31!=i21)). % 20.48/8.91 tff(c_412, plain, (i38!=i36)). % 20.48/8.91 tff(c_1876, plain, (i9!=i35)). % 20.48/8.91 tff(c_562, plain, (i43!=i31)). % 20.48/8.91 tff(c_674, plain, (i47!=i28)). % 20.48/8.91 tff(c_2092, plain, (i7!=i10)). % 20.48/8.91 tff(c_2324, plain, (i4!=i26)). % 20.48/8.91 tff(c_2026, plain, (i7!=i43)). % 20.48/8.91 tff(c_1722, plain, (i33!=i11)). % 20.48/8.91 tff(c_1728, plain, (i30!=i11)). % 20.48/8.91 tff(c_2440, plain, (i3!=i14)). % 20.48/8.91 tff(c_792, plain, (i33!=i26)). % 20.48/8.91 tff(c_1544, plain, (i47!=i13)). % 20.48/8.91 tff(c_870, plain, (i43!=i24)). % 20.48/8.91 tff(c_1928, plain, (i8!=i50)). % 20.48/8.91 tff(c_534, plain, (i39!=i32)). % 20.48/8.91 tff(c_1502, plain, (i32!=i14)). % 20.48/8.91 tff(c_736, plain, (i38!=i27)). % 20.48/8.91 tff(c_1076, plain, (i50!=i20)). % 20.48/8.91 tff(c_2336, plain, (i4!=i20)). % 20.48/8.91 tff(c_1748, plain, (i20!=i11)). % 20.48/8.91 tff(c_776, plain, (i41!=i26)). % 20.48/8.91 tff(c_2210, plain, (i5!=i38)). % 20.48/8.91 tff(c_2610, plain, (i24!=i1)). % 20.48/8.91 tff(c_218, plain, (i50!=i46)). % 20.48/8.91 tff(c_216, plain, (i48!=i47)). % 20.48/8.91 tff(c_1666, plain, (i23!=i12)). % 20.48/8.91 tff(c_2592, plain, (i33!=i1)). % 20.48/8.91 tff(c_2288, plain, (i44!=i4)). % 20.48/8.91 tff(c_1132, plain, (i22!=i20)). % 20.48/8.91 tff(c_1892, plain, (i9!=i27)). % 20.48/8.91 tff(c_472, plain, (i37!=i34)). % 20.48/8.91 tff(c_322, plain, (i47!=i39)). % 20.48/8.91 tff(c_1422, plain, (i37!=i15)). % 20.48/8.91 tff(c_464, plain, (i41!=i34)). % 20.48/8.91 tff(c_880, plain, (i38!=i24)). % 20.48/8.91 tff(c_590, plain, (i48!=i30)). % 20.48/8.91 tff(c_1932, plain, (i8!=i48)). % 20.48/8.91 tff(c_2464, plain, (i49!=i2)). % 20.48/8.91 tff(c_1738, plain, (i25!=i11)). % 20.48/8.91 tff(c_1658, plain, (i27!=i12)). % 20.48/8.91 tff(c_278, plain, (i50!=i41)). % 20.48/8.91 tff(c_1798, plain, (i34!=i10)). % 20.48/8.91 tff(c_2010, plain, (i9!=i8)). % 20.48/8.91 tff(c_1742, plain, (i23!=i11)). % 20.48/8.91 tff(c_2042, plain, (i7!=i35)). % 20.48/8.91 tff(c_1710, plain, (i39!=i11)). % 20.48/8.91 tff(c_1268, plain, (i47!=i17)). % 20.48/8.91 tff(c_2462, plain, (i50!=i2)). % 20.48/8.91 tff(c_954, plain, (i27!=i23)). % 20.48/8.92 tff(c_1176, plain, (i30!=i19)). % 20.48/8.92 tff(c_1668, plain, (i22!=i12)). % 20.48/8.92 tff(c_2290, plain, (i43!=i4)). % 20.48/8.92 tff(c_550, plain, (i49!=i31)). % 20.48/8.92 tff(c_2534, plain, (i2!=i14)). % 20.48/8.92 tff(c_2068, plain, (i7!=i22)). % 20.48/8.92 tff(c_1358, plain, (i35!=i16)). % 20.48/8.92 tff(c_1556, plain, (i41!=i13)). % 20.48/8.92 tff(c_2404, plain, (i32!=i3)). % 20.48/8.92 tff(c_242, plain, (i47!=i44)). % 20.48/8.92 tff(c_248, plain, (i50!=i43)). % 20.48/8.92 tff(c_1496, plain, (i35!=i14)). % 20.48/8.92 tff(c_760, plain, (i49!=i26)). % 20.48/8.92 tff(c_494, plain, (i42!=i33)). % 20.48/8.92 tff(c_1364, plain, (i32!=i16)). % 20.48/8.92 tff(c_1826, plain, (i20!=i10)). % 20.48/8.92 tff(c_2094, plain, (i9!=i7)). % 20.48/8.92 tff(c_572, plain, (i38!=i31)). % 20.48/8.92 tff(c_1704, plain, (i42!=i11)). % 20.48/8.92 tff(c_898, plain, (i29!=i24)). % 20.48/8.92 tff(c_304, plain, (i46!=i40)). % 20.48/8.92 tff(c_622, plain, (i32!=i30)). % 20.48/8.92 tff(c_1848, plain, (i9!=i49)). % 20.48/8.92 tff(c_1160, plain, (i38!=i19)). % 20.48/8.92 tff(c_1504, plain, (i31!=i14)). % 20.48/8.92 tff(c_2624, plain, (i17!=i1)). % 20.48/8.92 tff(c_1138, plain, (i49!=i19)). % 20.48/8.92 tff(c_2426, plain, (i3!=i21)). % 20.48/8.92 tff(c_516, plain, (i48!=i32)). % 20.48/8.92 tff(c_2646, plain, (i6!=i1)). % 20.48/8.92 tff(c_1376, plain, (i26!=i16)). % 20.48/8.92 tff(c_2194, plain, (i5!=i46)). % 20.48/8.92 tff(c_2004, plain, (i8!=i12)). % 20.48/8.92 tff(c_332, plain, (i42!=i39)). % 20.48/8.92 tff(c_1398, plain, (i49!=i15)). % 20.48/8.92 tff(c_1346, plain, (i41!=i16)). % 20.48/8.92 tff(c_1944, plain, (i8!=i42)). % 20.48/8.92 tff(c_1862, plain, (i9!=i42)). % 20.48/8.92 tff(c_1248, plain, (i25!=i18)). % 20.48/8.92 tff(c_1498, plain, (i34!=i14)). % 20.48/8.92 tff(c_1406, plain, (i45!=i15)). % 20.48/8.92 tff(c_1518, plain, (i24!=i14)). % 20.48/8.92 tff(c_766, plain, (i46!=i26)). % 20.48/8.92 tff(c_2496, plain, (i33!=i2)). % 20.48/8.92 tff(c_756, plain, (i28!=i27)). % 20.48/8.92 tff(c_2282, plain, (i47!=i4)). % 20.48/8.92 tff(c_586, plain, (i50!=i30)). % 20.48/8.92 tff(c_986, plain, (i38!=i22)). % 20.48/8.92 tff(c_1810, plain, (i28!=i10)). % 20.48/8.92 tff(c_1844, plain, (i11!=i10)). % 20.48/8.92 tff(c_2206, plain, (i5!=i40)). % 20.48/8.92 tff(c_2196, plain, (i5!=i45)). % 20.48/8.92 tff(c_1670, plain, (i21!=i12)). % 20.48/8.92 tff(c_548, plain, (i50!=i31)). % 20.48/8.92 tff(c_1630, plain, (i41!=i12)). % 20.48/8.92 tff(c_2408, plain, (i30!=i3)). % 20.48/8.92 tff(c_558, plain, (i45!=i31)). % 20.48/8.92 tff(c_588, plain, (i49!=i30)). % 20.48/8.92 tff(c_1950, plain, (i8!=i39)). % 20.48/8.92 tff(c_408, plain, (i40!=i36)). % 20.48/8.92 tff(c_700, plain, (i34!=i28)). % 20.48/8.92 tff(c_1558, plain, (i40!=i13)). % 20.48/8.92 tff(c_1304, plain, (i29!=i17)). % 20.48/8.92 tff(c_1112, plain, (i32!=i20)). % 20.48/8.92 tff(c_1576, plain, (i31!=i13)). % 20.48/8.92 tff(c_1474, plain, (i46!=i14)). % 20.48/8.92 tff(c_2328, plain, (i4!=i24)). % 20.48/8.92 tff(c_2060, plain, (i7!=i26)). % 20.48/8.92 tff(c_2602, plain, (i28!=i1)). % 20.48/8.92 tff(c_1124, plain, (i26!=i20)). % 20.48/8.92 tff(c_1424, plain, (i36!=i15)). % 20.48/8.92 tff(c_1458, plain, (i19!=i15)). % 20.48/8.92 tff(c_1392, plain, (i18!=i16)). % 20.48/8.92 tff(c_1324, plain, (i19!=i17)). % 20.48/8.92 tff(c_1208, plain, (i45!=i18)). % 20.48/8.92 tff(c_328, plain, (i44!=i39)). % 20.48/8.92 tff(c_2344, plain, (i4!=i16)). % 20.48/8.92 tff(c_1990, plain, (i8!=i19)). % 20.48/8.92 tff(c_646, plain, (i40!=i29)). % 20.48/8.92 tff(c_1030, plain, (i44!=i21)). % 20.48/8.92 tff(c_2012, plain, (i7!=i50)). % 20.48/8.92 tff(c_2476, plain, (i43!=i2)). % 20.48/8.92 tff(c_1588, plain, (i25!=i13)). % 20.48/8.92 tff(c_1308, plain, (i27!=i17)). % 20.48/8.92 tff(c_1286, plain, (i38!=i17)). % 20.48/8.92 tff(c_2390, plain, (i39!=i3)). % 20.48/8.92 tff(c_1878, plain, (i9!=i34)). % 20.48/8.92 tff(c_770, plain, (i44!=i26)). % 20.48/8.92 tff(c_788, plain, (i35!=i26)). % 20.48/8.92 tff(c_348, plain, (i45!=i38)). % 20.48/8.92 tff(c_1302, plain, (i30!=i17)). % 20.48/8.92 tff(c_2172, plain, (i6!=i13)). % 20.48/8.92 tff(c_1454, plain, (i21!=i15)). % 20.48/8.92 tff(c_2512, plain, (i25!=i2)). % 20.48/8.92 tff(c_1366, plain, (i31!=i16)). % 20.48/8.92 tff(c_1150, plain, (i43!=i19)). % 20.48/8.92 tff(c_256, plain, (i46!=i43)). % 20.48/8.92 tff(c_1182, plain, (i27!=i19)). % 20.48/8.92 tff(c_1452, plain, (i22!=i15)). % 20.48/8.92 tff(c_1570, plain, (i34!=i13)). % 20.48/8.92 tff(c_2214, plain, (i5!=i36)). % 20.48/8.92 tff(c_2016, plain, (i7!=i48)). % 20.48/8.92 tff(c_402, plain, (i43!=i36)). % 20.48/8.92 tff(c_468, plain, (i39!=i34)). % 20.48/8.92 tff(c_268, plain, (i47!=i42)). % 20.48/8.92 tff(c_1640, plain, (i36!=i12)). % 20.48/8.92 tff(c_2342, plain, (i4!=i17)). % 20.48/8.92 tff(c_2572, plain, (i43!=i1)). % 20.48/8.92 tff(c_868, plain, (i44!=i24)). % 20.48/8.92 tff(c_2376, plain, (i46!=i3)). % 20.48/8.92 tff(c_1750, plain, (i19!=i11)). % 20.48/8.92 tff(c_1356, plain, (i36!=i16)). % 20.48/8.92 tff(c_1778, plain, (i44!=i10)). % 20.48/8.92 tff(c_462, plain, (i42!=i34)). % 20.48/8.92 tff(c_1020, plain, (i49!=i21)). % 20.48/8.92 tff(c_2386, plain, (i41!=i3)). % 20.48/8.92 tff(c_1280, plain, (i41!=i17)). % 20.48/8.92 tff(c_1300, plain, (i31!=i17)). % 20.48/8.92 tff(c_1416, plain, (i40!=i15)). % 20.48/8.92 tff(c_958, plain, (i25!=i23)). % 20.48/8.92 tff(c_1512, plain, (i27!=i14)). % 20.48/8.92 tff(c_1250, plain, (i24!=i18)). % 20.48/8.92 tff(c_802, plain, (i28!=i26)). % 20.48/8.92 tff(c_670, plain, (i49!=i28)). % 20.48/8.92 tff(c_936, plain, (i36!=i23)). % 20.48/8.92 tff(c_2306, plain, (i4!=i35)). % 20.48/8.92 tff(c_2346, plain, (i4!=i15)). % 20.48/8.92 tff(c_658, plain, (i34!=i29)). % 20.48/8.92 tff(c_744, plain, (i34!=i27)). % 20.48/8.92 tff(c_2636, plain, (i11!=i1)). % 20.48/8.92 tff(c_1212, plain, (i43!=i18)). % 20.48/8.92 tff(c_1092, plain, (i42!=i20)). % 20.48/8.92 tff(c_1122, plain, (i27!=i20)). % 20.48/8.92 tff(c_344, plain, (i47!=i38)). % 20.48/8.92 tff(c_1968, plain, (i8!=i30)). % 20.48/8.92 tff(c_1494, plain, (i36!=i14)). % 20.48/8.92 tff(c_364, plain, (i49!=i37)). % 20.48/8.92 tff(c_2254, plain, (i5!=i16)). % 20.48/8.92 tff(c_834, plain, (i36!=i25)). % 20.48/8.92 tff(c_2110, plain, (i6!=i44)). % 20.48/8.92 tff(c_1428, plain, (i34!=i15)). % 20.48/8.92 tff(c_386, plain, (i38!=i37)). % 20.48/8.92 tff(c_1434, plain, (i31!=i15)). % 20.48/8.92 tff(c_2644, plain, (i7!=i1)). % 20.48/8.92 tff(c_2164, plain, (i6!=i17)). % 20.48/8.92 tff(c_1772, plain, (i47!=i10)). % 20.48/8.92 tff(c_1596, plain, (i21!=i13)). % 20.48/8.92 tff(c_1282, plain, (i40!=i17)). % 20.48/8.92 tff(c_1418, plain, (i39!=i15)). % 20.48/8.92 tff(c_782, plain, (i38!=i26)). % 20.48/8.92 tff(c_668, plain, (i50!=i28)). % 20.48/8.92 tff(c_2582, plain, (i38!=i1)). % 20.48/8.92 tff(c_1198, plain, (i50!=i18)). % 20.48/8.92 tff(c_296, plain, (i50!=i40)). % 20.48/8.92 tff(c_318, plain, (i49!=i39)). % 20.48/8.92 tff(c_1394, plain, (i17!=i16)). % 20.48/8.92 tff(c_224, plain, (i47!=i46)). % 20.48/8.92 tff(c_1184, plain, (i26!=i19)). % 20.48/8.92 tff(c_2570, plain, (i44!=i1)). % 20.48/8.92 tff(c_2518, plain, (i22!=i2)). % 20.48/8.92 tff(c_2226, plain, (i5!=i30)). % 20.48/8.92 tff(c_2436, plain, (i3!=i16)). % 20.48/8.92 tff(c_2520, plain, (i21!=i2)). % 20.48/8.92 tff(c_1444, plain, (i26!=i15)). % 20.48/8.92 tff(c_362, plain, (i50!=i37)). % 20.48/8.92 tff(c_2546, plain, (i8!=i2)). % 20.48/8.92 tff(c_2160, plain, (i6!=i19)). % 20.48/8.92 tff(c_2374, plain, (i47!=i3)). % 20.48/8.92 tff(c_1736, plain, (i26!=i11)). % 20.48/8.92 tff(c_1868, plain, (i9!=i39)). % 20.48/8.92 tff(c_856, plain, (i50!=i24)). % 20.48/8.92 tff(c_2102, plain, (i6!=i48)). % 20.48/8.92 tff(c_2224, plain, (i5!=i31)). % 20.48/8.92 tff(c_1046, plain, (i36!=i21)). % 20.48/8.92 tff(c_382, plain, (i40!=i37)). % 20.48/8.92 tff(c_2020, plain, (i7!=i46)). % 20.48/8.92 tff(c_428, plain, (i44!=i35)). % 20.48/8.92 tff(c_1992, plain, (i8!=i18)). % 20.48/8.92 tff(c_1010, plain, (i26!=i22)). % 20.48/8.92 tff(c_1960, plain, (i8!=i34)). % 20.48/8.92 tff(c_1580, plain, (i29!=i13)). % 20.48/8.92 tff(c_1480, plain, (i43!=i14)). % 20.48/8.92 tff(c_2192, plain, (i5!=i47)). % 20.48/8.92 tff(c_312, plain, (i42!=i40)). % 20.48/8.92 tff(c_1094, plain, (i41!=i20)). % 20.48/8.92 tff(c_872, plain, (i42!=i24)). % 20.48/8.92 tff(c_2300, plain, (i4!=i38)). % 20.48/8.92 tff(c_2292, plain, (i42!=i4)). % 20.48/8.92 tff(c_1284, plain, (i39!=i17)). % 20.48/8.92 tff(c_1954, plain, (i8!=i37)). % 20.48/8.92 tff(c_1456, plain, (i20!=i15)). % 20.48/8.92 tff(c_2418, plain, (i3!=i25)). % 20.48/8.92 tff(c_1400, plain, (i48!=i15)). % 20.48/8.92 tff(c_1490, plain, (i38!=i14)). % 20.48/8.92 tff(c_962, plain, (i50!=i22)). % 20.48/8.92 tff(c_1100, plain, (i38!=i20)). % 20.48/8.92 tff(c_2334, plain, (i4!=i21)). % 20.48/8.92 tff(c_2450, plain, (i9!=i3)). % 20.48/8.92 tff(c_964, plain, (i49!=i22)). % 20.48/8.92 tff(c_2384, plain, (i42!=i3)). % 20.48/8.92 tff(c_2398, plain, (i35!=i3)). % 20.48/8.92 tff(c_1530, plain, (i18!=i14)). % 20.48/8.92 tff(c_1888, plain, (i9!=i29)). % 20.48/8.92 tff(c_352, plain, (i43!=i38)). % 20.48/8.92 tff(c_966, plain, (i48!=i22)). % 20.48/8.92 tff(c_2428, plain, (i3!=i20)). % 20.48/8.92 tff(c_930, plain, (i39!=i23)). % 20.48/8.92 tff(c_290, plain, (i44!=i41)). % 20.48/8.92 tff(c_2410, plain, (i3!=i29)). % 20.48/8.92 tff(c_1510, plain, (i28!=i14)). % 20.48/8.92 tff(c_2232, plain, (i5!=i27)). % 20.48/8.92 tff(c_520, plain, (i46!=i32)). % 20.48/8.92 tff(c_1144, plain, (i46!=i19)). % 20.48/8.92 tff(c_2516, plain, (i23!=i2)). % 20.48/8.92 tff(c_1726, plain, (i31!=i11)). % 20.48/8.92 tff(c_1380, plain, (i24!=i16)). % 20.48/8.92 tff(c_1312, plain, (i25!=i17)). % 20.48/8.92 tff(c_2040, plain, (i7!=i36)). % 20.48/8.92 tff(c_1854, plain, (i9!=i46)). % 20.48/8.92 tff(c_2084, plain, (i7!=i14)). % 20.48/8.92 tff(c_1352, plain, (i38!=i16)). % 20.48/8.92 tff(c_2454, plain, (i7!=i3)). % 20.48/8.92 tff(c_946, plain, (i31!=i23)). % 20.48/8.92 tff(c_1202, plain, (i48!=i18)). % 20.48/8.92 tff(c_942, plain, (i33!=i23)). % 20.48/8.92 tff(c_1060, plain, (i29!=i21)). % 20.48/8.92 tff(c_1440, plain, (i28!=i15)). % 20.48/8.92 tff(c_2274, plain, (i6!=i5)). % 20.48/8.92 tff(c_912, plain, (i48!=i23)). % 20.48/8.92 tff(c_2322, plain, (i4!=i27)). % 20.48/8.92 tff(c_988, plain, (i37!=i22)). % 20.48/8.92 tff(c_1532, plain, (i17!=i14)). % 20.48/8.92 tff(c_2396, plain, (i36!=i3)). % 20.48/8.92 tff(c_624, plain, (i31!=i30)). % 20.48/8.92 tff(c_810, plain, (i48!=i25)). % 20.48/8.92 tff(c_812, plain, (i47!=i25)). % 20.48/8.92 tff(c_446, plain, (i50!=i34)). % 20.48/8.92 tff(c_1788, plain, (i39!=i10)). % 20.48/8.92 tff(c_2580, plain, (i39!=i1)). % 20.48/8.92 tff(c_2472, plain, (i45!=i2)). % 20.48/8.92 tff(c_1314, plain, (i24!=i17)). % 20.48/8.92 tff(c_1338, plain, (i45!=i16)). % 20.48/8.92 tff(c_956, plain, (i26!=i23)). % 20.48/8.92 tff(c_480, plain, (i49!=i33)). % 20.48/8.92 tff(c_1698, plain, (i45!=i11)). % 20.48/8.92 tff(c_862, plain, (i47!=i24)). % 20.48/8.92 tff(c_826, plain, (i40!=i25)). % 20.48/8.92 tff(c_2536, plain, (i2!=i13)). % 20.48/8.92 tff(c_1700, plain, (i44!=i11)). % 20.48/8.92 tff(c_346, plain, (i46!=i38)). % 20.48/8.92 tff(c_2526, plain, (i2!=i18)). % 20.48/8.92 tff(c_2174, plain, (i6!=i12)). % 20.48/8.92 tff(c_642, plain, (i42!=i29)). % 20.48/8.92 tff(c_1526, plain, (i20!=i14)). % 20.48/8.92 tff(c_754, plain, (i29!=i27)). % 20.48/8.92 tff(c_1008, plain, (i27!=i22)). % 20.48/8.92 tff(c_2044, plain, (i7!=i34)). % 20.48/8.92 tff(c_1784, plain, (i41!=i10)). % 20.48/8.92 tff(c_934, plain, (i37!=i23)). % 20.48/8.92 tff(c_2598, plain, (i30!=i1)). % 20.48/8.92 tff(c_2136, plain, (i6!=i31)). % 20.48/8.92 tff(c_800, plain, (i29!=i26)). % 20.48/8.92 tff(c_2112, plain, (i6!=i43)). % 20.48/8.92 tff(c_302, plain, (i47!=i40)). % 20.48/8.92 tff(c_1336, plain, (i46!=i16)). % 20.48/8.92 tff(c_416, plain, (i50!=i35)). % 20.48/8.92 tff(c_1002, plain, (i30!=i22)). % 20.48/8.92 tff(c_1644, plain, (i34!=i12)). % 20.48/8.92 tff(c_1472, plain, (i47!=i14)). % 20.48/8.92 tff(c_310, plain, (i43!=i40)). % 20.48/8.92 tff(c_1616, plain, (i48!=i12)). % 20.48/8.92 tff(c_1520, plain, (i23!=i14)). % 20.48/8.92 tff(c_1136, plain, (i50!=i19)). % 20.48/8.92 tff(c_746, plain, (i33!=i27)). % 20.48/8.92 tff(c_482, plain, (i48!=i33)). % 20.48/8.92 tff(c_992, plain, (i35!=i22)). % 20.48/8.92 tff(c_2304, plain, (i4!=i36)). % 20.48/8.92 tff(c_1870, plain, (i9!=i38)). % 20.48/8.92 tff(c_1146, plain, (i45!=i19)). % 20.48/8.92 tff(c_886, plain, (i35!=i24)). % 20.48/8.92 tff(c_1000, plain, (i31!=i22)). % 20.48/8.92 tff(c_632, plain, (i47!=i29)). % 20.48/8.92 tff(c_1042, plain, (i38!=i21)). % 20.48/8.92 tff(c_1086, plain, (i45!=i20)). % 20.48/8.92 tff(c_1988, plain, (i8!=i20)). % 20.48/8.92 tff(c_214, plain, (i49!=i47)). % 20.48/8.92 tff(c_2066, plain, (i7!=i23)). % 20.48/8.92 tff(c_818, plain, (i44!=i25)). % 20.48/8.92 tff(c_438, plain, (i39!=i35)). % 20.48/8.92 tff(c_374, plain, (i44!=i37)). % 20.48/8.92 tff(c_226, plain, (i50!=i45)). % 20.48/8.92 tff(c_492, plain, (i43!=i33)). % 20.48/8.92 tff(c_1402, plain, (i47!=i15)). % 20.48/8.92 tff(c_1234, plain, (i32!=i18)). % 20.48/8.92 tff(c_1334, plain, (i47!=i16)). % 20.48/8.92 tff(c_1916, plain, (i9!=i15)). % 20.48/8.92 tff(c_262, plain, (i50!=i42)). % 20.48/8.92 tff(c_1326, plain, (i18!=i17)). % 20.48/8.92 tff(c_1386, plain, (i21!=i16)). % 20.48/8.92 tff(c_1686, plain, (i13!=i12)). % 20.48/8.92 tff(c_1098, plain, (i39!=i20)). % 20.48/8.92 tff(c_2270, plain, (i8!=i5)). % 20.48/8.92 tff(c_1880, plain, (i9!=i33)). % 20.48/8.92 tff(c_2120, plain, (i6!=i39)). % 20.48/8.92 tff(c_1614, plain, (i49!=i12)). % 20.48/8.92 tff(c_698, plain, (i35!=i28)). % 20.48/8.92 tff(c_1840, plain, (i13!=i10)). % 20.48/8.92 tff(c_2202, plain, (i5!=i42)). % 20.48/8.92 tff(c_672, plain, (i48!=i28)). % 20.48/8.92 tff(c_1296, plain, (i33!=i17)). % 20.48/8.92 tff(c_1886, plain, (i9!=i30)). % 20.48/8.92 tff(c_1906, plain, (i9!=i20)). % 20.48/8.92 tff(c_1586, plain, (i26!=i13)). % 20.48/8.92 tff(c_368, plain, (i47!=i37)). % 20.48/8.92 tff(c_2444, plain, (i3!=i12)). % 20.48/8.92 tff(c_1914, plain, (i9!=i16)). % 20.48/8.92 tff(c_2150, plain, (i6!=i24)). % 20.48/8.92 tff(c_1024, plain, (i47!=i21)). % 20.48/8.92 tff(c_1420, plain, (i38!=i15)). % 20.48/8.92 tff(c_2118, plain, (i6!=i40)). % 20.48/8.92 tff(c_822, plain, (i42!=i25)). % 20.48/8.92 tff(c_2090, plain, (i7!=i11)). % 20.48/8.92 tff(c_2330, plain, (i4!=i23)). % 20.48/8.92 tff(c_1506, plain, (i30!=i14)). % 20.48/8.92 tff(c_1170, plain, (i33!=i19)). % 20.48/8.92 tff(c_1156, plain, (i40!=i19)). % 20.48/8.92 tff(c_882, plain, (i37!=i24)). % 20.48/8.92 tff(c_1538, plain, (i50!=i13)). % 20.48/8.92 tff(c_614, plain, (i36!=i30)). % 20.48/8.92 tff(c_804, plain, (i27!=i26)). % 20.48/8.92 tff(c_678, plain, (i45!=i28)). % 20.48/8.92 tff(c_680, plain, (i44!=i28)). % 20.48/8.92 tff(c_824, plain, (i41!=i25)). % 20.48/8.92 tff(c_740, plain, (i36!=i27)). % 20.48/8.92 tff(c_1214, plain, (i42!=i18)). % 20.48/8.92 tff(c_752, plain, (i30!=i27)). % 20.48/8.92 tff(c_1128, plain, (i24!=i20)). % 20.48/8.92 tff(c_1142, plain, (i47!=i19)). % 20.48/8.92 tff(c_2356, plain, (i4!=i10)). % 20.48/8.92 tff(c_1310, plain, (i26!=i17)). % 20.48/8.92 tff(c_638, plain, (i44!=i29)). % 20.48/8.92 tff(c_1330, plain, (i49!=i16)). % 20.48/8.92 tff(c_634, plain, (i46!=i29)). % 20.48/8.92 tff(c_1044, plain, (i37!=i21)). % 20.48/8.92 tff(c_1980, plain, (i8!=i24)). % 20.48/8.92 tff(c_908, plain, (i50!=i23)). % 20.48/8.92 tff(c_2310, plain, (i4!=i33)). % 20.48/8.92 tff(c_1902, plain, (i9!=i22)). % 20.48/8.92 tff(c_398, plain, (i45!=i36)). % 20.48/8.92 tff(c_1116, plain, (i30!=i20)). % 20.48/8.92 tff(c_2370, plain, (i49!=i3)). % 20.48/8.92 tff(c_1278, plain, (i42!=i17)). % 20.48/8.92 tff(c_1500, plain, (i33!=i14)). % 20.48/8.92 tff(c_452, plain, (i47!=i34)). % 20.48/8.92 tff(c_1410, plain, (i43!=i15)). % 20.48/8.92 tff(c_2098, plain, (i6!=i50)). % 20.48/8.92 tff(c_2420, plain, (i3!=i24)). % 20.48/8.92 tff(c_404, plain, (i42!=i36)). % 20.48/8.92 tff(c_1050, plain, (i34!=i21)). % 20.48/8.92 tff(c_750, plain, (i31!=i27)). % 20.48/8.92 tff(c_2190, plain, (i5!=i48)). % 20.48/8.92 tff(c_2188, plain, (i5!=i49)). % 20.48/8.92 tff(c_2186, plain, (i50!=i5)). % 20.48/8.92 tff(c_2062, plain, (i7!=i25)). % 20.48/8.92 tff(c_1052, plain, (i33!=i21)). % 20.48/8.92 tff(c_2616, plain, (i21!=i1)). % 20.48/8.92 tff(c_906, plain, (i25!=i24)). % 20.48/8.92 tff(c_1584, plain, (i27!=i13)). % 20.48/8.92 tff(c_366, plain, (i48!=i37)). % 20.48/8.92 tff(c_2566, plain, (i46!=i1)). % 20.48/8.92 tff(c_244, plain, (i46!=i44)). % 20.48/8.92 tff(c_1562, plain, (i38!=i13)). % 20.48/8.92 tff(c_2220, plain, (i5!=i33)). % 20.48/8.92 tff(c_796, plain, (i31!=i26)). % 20.48/8.92 tff(c_576, plain, (i36!=i31)). % 20.48/8.92 tff(c_950, plain, (i29!=i23)). % 20.48/8.92 tff(c_1898, plain, (i9!=i24)). % 20.48/8.92 tff(c_524, plain, (i44!=i32)). % 20.48/8.92 tff(c_370, plain, (i46!=i37)). % 20.48/8.92 tff(c_526, plain, (i43!=i32)). % 20.48/8.92 tff(c_1594, plain, (i22!=i13)). % 20.48/8.92 tff(c_2126, plain, (i6!=i36)). % 20.48/8.92 tff(c_2392, plain, (i38!=i3)). % 20.48/8.92 tff(c_2486, plain, (i38!=i2)). % 20.48/8.92 tff(c_968, plain, (i47!=i22)). % 20.48/8.92 tff(c_1650, plain, (i31!=i12)). % 20.48/8.92 tff(c_2506, plain, (i28!=i2)). % 20.48/8.92 tff(c_1054, plain, (i32!=i21)). % 20.48/8.92 tff(c_970, plain, (i46!=i22)). % 20.48/8.92 tff(c_240, plain, (i48!=i44)). % 20.48/8.92 tff(c_2326, plain, (i4!=i25)). % 20.48/8.92 tff(c_284, plain, (i47!=i41)). % 20.48/8.92 tff(c_2578, plain, (i40!=i1)). % 20.48/8.92 tff(c_1732, plain, (i28!=i11)). % 20.48/8.92 tff(c_972, plain, (i45!=i22)). % 20.48/8.92 tff(c_814, plain, (i46!=i25)). % 20.48/8.92 tff(c_704, plain, (i32!=i28)). % 20.48/8.92 tff(c_1516, plain, (i25!=i14)). % 20.48/8.92 tff(c_786, plain, (i36!=i26)). % 20.48/8.92 tff(c_454, plain, (i46!=i34)). % 20.48/8.92 tff(c_1436, plain, (i30!=i15)). % 20.48/8.92 tff(c_1786, plain, (i40!=i10)). % 20.48/8.92 tff(c_1866, plain, (i9!=i40)). % 20.48/8.92 tff(c_1690, plain, (i49!=i11)). % 20.48/8.92 tff(c_1276, plain, (i43!=i17)). % 20.48/8.92 tff(c_762, plain, (i48!=i26)). % 20.48/8.92 tff(c_2442, plain, (i3!=i13)). % 20.48/8.92 tff(c_1598, plain, (i20!=i13)). % 20.48/8.92 tff(c_1378, plain, (i25!=i16)). % 20.48/8.92 tff(c_1306, plain, (i28!=i17)). % 20.48/8.92 tff(c_1966, plain, (i8!=i31)). % 20.48/8.92 tff(c_354, plain, (i42!=i38)). % 20.48/8.92 tff(c_1930, plain, (i8!=i49)). % 20.48/8.92 tff(c_2154, plain, (i6!=i22)). % 20.48/8.92 tff(c_876, plain, (i40!=i24)). % 20.48/8.92 tff(c_288, plain, (i45!=i41)). % 20.48/8.92 tff(c_1720, plain, (i34!=i11)). % 20.48/8.92 tff(c_552, plain, (i48!=i31)). % 20.48/8.92 tff(c_2162, plain, (i6!=i18)). % 20.48/8.92 tff(c_554, plain, (i47!=i31)). % 20.48/8.92 tff(c_336, plain, (i40!=i39)). % 20.48/8.92 tff(c_1994, plain, (i8!=i17)). % 20.48/8.92 tff(c_2200, plain, (i5!=i43)). % 20.48/8.92 tff(c_2272, plain, (i7!=i5)). % 20.48/8.92 tff(c_2488, plain, (i37!=i2)). % 20.48/8.92 tff(c_2412, plain, (i3!=i28)). % 20.48/8.92 tff(c_1012, plain, (i25!=i22)). % 20.48/8.92 tff(c_636, plain, (i45!=i29)). % 20.48/8.92 tff(c_2460, plain, (i4!=i3)). % 20.48/8.92 tff(c_2372, plain, (i48!=i3)). % 20.48/8.92 tff(c_1682, plain, (i15!=i12)). % 20.48/8.92 tff(c_798, plain, (i30!=i26)). % 20.48/8.92 tff(c_656, plain, (i35!=i29)). % 20.48/8.92 tff(c_2104, plain, (i6!=i47)). % 20.48/8.92 tff(c_2360, plain, (i8!=i4)). % 20.48/8.92 tff(c_2008, plain, (i8!=i10)). % 20.48/8.92 tff(c_1070, plain, (i24!=i21)). % 20.48/8.92 tff(c_1642, plain, (i35!=i12)). % 20.48/8.92 tff(c_1542, plain, (i48!=i13)). % 20.48/8.92 tff(c_1450, plain, (i23!=i15)). % 20.48/8.92 tff(c_2584, plain, (i37!=i1)). % 20.48/8.92 tff(c_1618, plain, (i47!=i12)). % 20.48/8.92 tff(c_1134, plain, (i21!=i20)). % 20.48/8.92 tff(c_260, plain, (i44!=i43)). % 20.48/8.92 tff(c_536, plain, (i38!=i32)). % 20.48/8.92 tff(c_1476, plain, (i45!=i14)). % 20.48/8.92 tff(c_2252, plain, (i5!=i17)). % 20.48/8.92 tff(c_1236, plain, (i31!=i18)). % 20.48/8.92 tff(c_900, plain, (i28!=i24)). % 20.48/8.92 tff(c_574, plain, (i37!=i31)). % 20.48/8.92 tff(c_490, plain, (i44!=i33)). % 20.48/8.92 tff(c_1600, plain, (i19!=i13)). % 20.48/8.92 tff(c_866, plain, (i45!=i24)). % 20.48/8.92 tff(c_650, plain, (i38!=i29)). % 20.48/8.92 tff(c_902, plain, (i27!=i24)). % 20.48/8.92 tff(c_648, plain, (i39!=i29)). % 20.48/8.93 tff(c_212, plain, (i50!=i47)). % 20.48/8.93 tff(c_1822, plain, (i22!=i10)). % 20.48/8.93 tff(c_904, plain, (i26!=i24)). % 20.48/8.93 tff(c_852, plain, (i27!=i25)). % 20.48/8.93 tff(c_282, plain, (i48!=i41)). % 20.48/8.93 tff(c_1756, plain, (i16!=i11)). % 20.48/8.93 tff(c_1244, plain, (i27!=i18)). % 20.48/8.93 tff(c_1478, plain, (i44!=i14)). % 20.48/8.93 tff(c_1242, plain, (i28!=i18)). % 20.48/8.93 tff(c_1740, plain, (i24!=i11)). % 20.48/8.93 tff(c_738, plain, (i37!=i27)). % 20.48/8.93 tff(c_660, plain, (i33!=i29)). % 20.48/8.93 tff(c_2434, plain, (i3!=i17)). % 20.48/8.93 tff(c_2618, plain, (i20!=i1)). % 20.48/8.93 tff(c_2554, plain, (i4!=i2)). % 20.48/8.93 tff(c_850, plain, (i28!=i25)). % 20.48/8.93 tff(c_2132, plain, (i6!=i33)). % 20.48/8.93 tff(c_546, plain, (i33!=i32)). % 20.48/8.93 tff(c_910, plain, (i49!=i23)). % 20.48/8.93 tff(c_1602, plain, (i18!=i13)). % 20.48/8.93 tff(c_2276, plain, (i50!=i4)). % 20.48/8.93 tff(c_1298, plain, (i32!=i17)). % 20.48/8.93 tff(c_530, plain, (i41!=i32)). % 20.48/8.93 tff(c_1574, plain, (i32!=i13)). % 20.48/8.93 tff(c_1466, plain, (i50!=i14)). % 20.48/8.93 tff(c_1606, plain, (i16!=i13)). % 20.48/8.93 tff(c_976, plain, (i43!=i22)). % 20.48/8.93 tff(c_1904, plain, (i9!=i21)). % 20.48/8.93 tff(c_528, plain, (i42!=i32)). % 20.48/8.93 tff(c_1180, plain, (i28!=i19)). % 20.48/8.93 tff(c_484, plain, (i47!=i33)). % 20.48/8.93 tff(c_378, plain, (i42!=i37)). % 20.48/8.93 tff(c_1592, plain, (i23!=i13)). % 20.48/8.93 tff(c_2130, plain, (i6!=i34)). % 20.48/8.93 tff(c_1048, plain, (i35!=i21)). % 20.48/8.93 tff(c_2032, plain, (i7!=i40)). % 20.48/8.93 tff(c_2218, plain, (i5!=i34)). % 20.48/8.93 tff(c_1776, plain, (i45!=i10)). % 20.48/8.93 tff(c_488, plain, (i45!=i33)). % 20.48/8.93 tff(c_1140, plain, (i48!=i19)). % 20.48/8.93 tff(c_2628, plain, (i15!=i1)). % 20.48/8.93 tff(c_232, plain, (i47!=i45)). % 20.48/8.93 tff(c_2302, plain, (i4!=i37)). % 20.48/8.93 tff(c_1408, plain, (i44!=i15)). % 20.48/8.93 tff(c_1294, plain, (i34!=i17)). % 20.48/8.93 tff(c_388, plain, (i50!=i36)). % 20.48/8.93 tff(c_2614, plain, (i22!=i1)). % 20.48/8.93 tff(c_1952, plain, (i8!=i38)). % 20.48/8.93 tff(c_2480, plain, (i41!=i2)). % 20.48/8.93 tff(c_2052, plain, (i7!=i30)). % 20.48/8.93 tff(c_696, plain, (i36!=i28)). % 20.48/8.93 tff(c_1976, plain, (i8!=i26)). % 20.48/8.93 tff(c_274, plain, (i44!=i42)). % 20.48/8.93 tff(c_1680, plain, (i16!=i12)). % 20.48/8.93 tff(c_432, plain, (i42!=i35)). % 20.48/8.93 tff(c_816, plain, (i45!=i25)). % 20.48/8.93 tff(c_1274, plain, (i44!=i17)). % 20.48/8.93 tff(c_2148, plain, (i6!=i25)). % 20.48/8.93 tff(c_1260, plain, (i19!=i18)). % 20.48/8.93 tff(c_2550, plain, (i6!=i2)). % 20.48/8.93 tff(c_780, plain, (i39!=i26)). % 20.48/8.93 tff(c_1018, plain, (i50!=i21)). % 20.48/8.93 tff(c_1564, plain, (i37!=i13)). % 20.48/8.93 tff(c_1016, plain, (i23!=i22)). % 20.48/8.93 tff(c_892, plain, (i32!=i24)). % 20.48/8.93 tff(c_1154, plain, (i41!=i19)). % 20.48/8.93 tff(c_2586, plain, (i36!=i1)). % 20.48/8.93 tff(c_758, plain, (i50!=i26)). % 20.48/8.93 tff(c_1462, plain, (i17!=i15)). % 20.48/8.93 tff(c_1006, plain, (i28!=i22)). % 20.48/8.93 tff(c_2452, plain, (i8!=i3)). % 20.48/8.93 tff(c_2556, plain, (i3!=i2)). % 20.48/8.93 tff(c_1660, plain, (i26!=i12)). % 20.48/8.93 tff(c_272, plain, (i45!=i42)). % 20.48/8.93 tff(c_1448, plain, (i24!=i15)). % 20.48/8.93 tff(c_1446, plain, (i25!=i15)). % 20.48/8.93 tff(c_1464, plain, (i16!=i15)). % 20.48/8.93 tff(c_1482, plain, (i42!=i14)). % 20.48/8.93 tff(c_1662, plain, (i25!=i12)). % 20.48/8.93 tff(c_1162, plain, (i37!=i19)). % 20.48/8.93 tff(c_1022, plain, (i48!=i21)). % 20.48/8.93 tff(c_1158, plain, (i39!=i19)). % 20.48/8.93 tff(c_286, plain, (i46!=i41)). % 20.48/8.93 tff(c_764, plain, (i47!=i26)). % 20.48/8.93 tff(c_1522, plain, (i22!=i14)). % 20.48/8.93 tff(c_1322, plain, (i20!=i17)). % 20.48/8.93 tff(c_1648, plain, (i32!=i12)). % 20.48/8.93 tff(c_1096, plain, (i40!=i20)). % 20.48/8.93 tff(c_1174, plain, (i31!=i19)). % 20.48/8.93 tff(c_1040, plain, (i39!=i21)). % 20.48/8.93 tff(c_2106, plain, (i6!=i46)). % 20.48/8.93 tff(c_2382, plain, (i43!=i3)). % 20.48/8.93 tff(c_1814, plain, (i26!=i10)). % 20.48/8.93 tff(c_1484, plain, (i41!=i14)). % 20.48/8.93 tff(c_496, plain, (i41!=i33)). % 20.48/8.93 tff(c_1714, plain, (i37!=i11)). % 20.48/8.93 tff(c_1088, plain, (i44!=i20)). % 20.48/8.93 tff(c_1442, plain, (i27!=i15)). % 20.48/8.93 tff(c_1816, plain, (i25!=i10)). % 20.48/8.93 tff(c_1828, plain, (i19!=i10)). % 20.48/8.93 tff(c_326, plain, (i45!=i39)). % 20.48/8.93 tff(c_324, plain, (i46!=i39)). % 20.48/8.93 tff(c_1872, plain, (i9!=i37)). % 20.48/8.93 tff(c_1638, plain, (i37!=i12)). % 20.48/8.93 tff(c_320, plain, (i48!=i39)). % 20.48/8.93 tff(c_1188, plain, (i24!=i19)). % 20.48/8.93 tff(c_1186, plain, (i25!=i19)). % 20.48/8.93 tff(c_1972, plain, (i8!=i28)). % 20.48/8.93 tff(c_2568, plain, (i45!=i1)). % 20.48/8.93 tff(c_2576, plain, (i41!=i1)). % 20.48/8.93 tff(c_1038, plain, (i40!=i21)). % 20.48/8.93 tff(c_1036, plain, (i41!=i21)). % 20.48/8.93 tff(c_1470, plain, (i48!=i14)). % 20.48/8.93 tff(c_444, plain, (i36!=i35)). % 20.48/8.93 tff(c_2238, plain, (i5!=i24)). % 20.48/8.93 tff(c_2236, plain, (i5!=i25)). % 20.48/8.93 tff(c_458, plain, (i44!=i34)). % 20.48/8.93 tff(c_456, plain, (i45!=i34)). % 20.48/8.93 tff(c_1572, plain, (i33!=i13)). % 20.48/8.93 tff(c_1708, plain, (i40!=i11)). % 20.48/8.93 tff(c_2606, plain, (i26!=i1)). % 20.48/8.93 tff(c_2504, plain, (i29!=i2)). % 20.48/8.93 tff(c_2638, plain, (i10!=i1)). % 20.48/8.93 tff(c_2256, plain, (i5!=i15)). % 20.48/8.93 tff(c_2078, plain, (i7!=i17)). % 20.48/8.93 tff(c_2338, plain, (i4!=i19)). % 20.48/8.93 tff(c_2596, plain, (i31!=i1)). % 20.48/8.93 tff(c_1226, plain, (i36!=i18)). % 20.48/8.93 tff(c_2510, plain, (i26!=i2)). % 20.48/8.93 tff(c_2122, plain, (i6!=i38)). % 20.48/8.93 tff(c_2634, plain, (i12!=i1)). % 20.48/8.93 tff(c_2604, plain, (i27!=i1)). % 20.48/8.93 tff(c_706, plain, (i31!=i28)). % 20.48/8.93 tff(c_982, plain, (i40!=i22)). % 20.48/8.93 tff(c_980, plain, (i41!=i22)). % 20.48/8.93 tff(c_978, plain, (i42!=i22)). % 20.48/8.93 tff(c_460, plain, (i43!=i34)). % 20.48/8.93 tff(c_1692, plain, (i48!=i11)). % 20.48/8.93 tff(c_708, plain, (i30!=i28)). % 20.48/8.93 tff(c_2502, plain, (i30!=i2)). % 20.48/8.93 tff(c_1804, plain, (i31!=i10)). % 20.48/8.93 tff(c_2208, plain, (i5!=i39)). % 20.48/8.93 tff(c_710, plain, (i29!=i28)). % 20.48/8.93 tff(c_1800, plain, (i33!=i10)). % 20.48/8.93 tff(c_842, plain, (i32!=i25)). % 20.48/8.93 tff(c_1796, plain, (i35!=i10)). % 20.48/8.93 tff(c_1794, plain, (i36!=i10)). % 20.48/8.93 tff(c_538, plain, (i37!=i32)). % 20.48/8.93 tff(c_712, plain, (i50!=i27)). % 20.48/8.93 tff(c_2168, plain, (i6!=i15)). % 20.48/8.93 tff(c_2166, plain, (i6!=i16)). % 20.48/8.93 tff(c_2250, plain, (i5!=i18)). % 20.48/8.93 tff(c_714, plain, (i49!=i27)). % 20.48/8.93 tff(c_2564, plain, (i47!=i1)). % 20.48/8.93 tff(c_2000, plain, (i8!=i14)). % 20.48/8.93 tff(c_1696, plain, (i46!=i11)). % 20.48/8.93 tff(c_2234, plain, (i5!=i26)). % 20.48/8.93 tff(c_2620, plain, (i19!=i1)). % 20.48/8.93 tff(c_716, plain, (i48!=i27)). % 20.48/8.93 tff(c_1806, plain, (i30!=i10)). % 20.48/8.93 tff(c_2562, plain, (i48!=i1)). % 20.48/8.93 tff(c_846, plain, (i30!=i25)). % 20.48/8.93 tff(c_718, plain, (i47!=i27)). % 20.48/8.93 tff(c_844, plain, (i31!=i25)). % 20.48/8.93 tff(c_2038, plain, (i7!=i37)). % 20.48/8.93 tff(c_2036, plain, (i7!=i38)). % 20.48/8.93 tff(c_2034, plain, (i7!=i39)). % 20.48/8.93 tff(c_2414, plain, (i3!=i27)). % 20.48/8.93 tff(c_720, plain, (i46!=i27)). % 20.48/8.93 tff(c_2482, plain, (i40!=i2)). % 20.48/8.93 tff(c_1246, plain, (i26!=i18)). % 20.48/8.93 tff(c_2298, plain, (i4!=i39)). % 20.48/8.93 tff(c_722, plain, (i45!=i27)). % 20.48/8.93 tff(c_1216, plain, (i41!=i18)). % 20.48/8.93 tff(c_2268, plain, (i9!=i5)). % 20.48/8.93 tff(c_2266, plain, (i5!=i10)). % 20.48/8.93 tff(c_1832, plain, (i17!=i10)). % 20.48/8.93 tff(c_1830, plain, (i18!=i10)). % 20.48/8.93 tff(c_724, plain, (i44!=i27)). % 20.48/8.93 tff(c_2552, plain, (i5!=i2)). % 20.48/8.93 tff(c_1222, plain, (i38!=i18)). % 20.48/8.93 tff(c_1220, plain, (i39!=i18)). % 20.48/8.93 tff(c_726, plain, (i43!=i27)). % 20.48/8.93 tff(c_1218, plain, (i40!=i18)). % 20.48/8.93 tff(c_564, plain, (i42!=i31)). % 20.48/8.93 tff(c_566, plain, (i41!=i31)). % 20.48/8.93 tff(c_1612, plain, (i50!=i12)). % 20.48/8.93 tff(c_568, plain, (i40!=i31)). % 20.48/8.93 tff(c_728, plain, (i42!=i27)). % 20.48/8.93 tff(c_1540, plain, (i49!=i13)). % 20.48/8.93 tff(c_2484, plain, (i39!=i2)). % 20.48/8.93 tff(c_1488, plain, (i39!=i14)). % 20.48/8.93 tff(c_730, plain, (i41!=i27)). % 20.48/8.93 tff(c_1838, plain, (i14!=i10)). % 20.48/8.93 tff(c_1836, plain, (i15!=i10)). % 20.48/8.93 tff(c_1834, plain, (i16!=i10)). % 20.48/8.93 tff(c_2416, plain, (i3!=i26)). % 20.48/8.93 tff(c_2080, plain, (i7!=i16)). % 20.48/8.93 tff(c_732, plain, (i40!=i27)). % 20.48/8.93 tff(c_2456, plain, (i6!=i3)). % 20.48/8.93 tff(c_1842, plain, (i12!=i10)). % 20.48/8.93 tff(c_1224, plain, (i37!=i18)). % 20.48/8.93 tff(c_734, plain, (i39!=i27)). % 20.48/8.93 tff(c_2528, plain, (i2!=i17)). % 20.48/8.93 tff(c_580, plain, (i34!=i31)). % 20.48/8.93 tff(c_582, plain, (i33!=i31)). % 20.48/8.93 tff(c_1620, plain, (i46!=i12)). % 20.48/8.93 tff(c_584, plain, (i32!=i31)). % 20.48/8.93 tff(c_2178, plain, (i6!=i10)). % 20.48/8.93 tff(c_2378, plain, (i45!=i3)). % 20.48/8.93 tff(c_2630, plain, (i14!=i1)). % 20.48/8.93 tff(c_2608, plain, (i25!=i1)). % 20.48/8.93 tff(c_2180, plain, (i9!=i6)). % 20.48/8.93 tff(c_1946, plain, (i8!=i41)). % 20.48/8.93 tff(c_1232, plain, (i33!=i18)). % 20.48/8.93 tff(c_1230, plain, (i34!=i18)). % 20.48/8.93 tff(c_592, plain, (i47!=i30)). % 20.48/8.93 tff(c_594, plain, (i46!=i30)). % 20.48/8.93 tff(c_2182, plain, (i8!=i6)). % 20.48/8.93 tff(c_1626, plain, (i43!=i12)). % 20.48/8.93 tff(c_2142, plain, (i6!=i28)). % 20.48/8.93 tff(c_2400, plain, (i34!=i3)). % 20.48/8.93 tff(c_2184, plain, (i7!=i6)). % 20.48/8.93 tff(c_596, plain, (i45!=i30)). % 20.48/8.93 tff(c_598, plain, (i44!=i30)). % 20.48/8.93 tff(c_1628, plain, (i42!=i12)). % 20.48/8.93 tff(c_600, plain, (i43!=i30)). % 20.48/8.93 tff(c_602, plain, (i42!=i30)). % 20.48/8.93 tff(c_2422, plain, (i3!=i23)). % 20.48/8.93 tff(c_2354, plain, (i4!=i11)). % 20.48/8.93 tff(c_2348, plain, (i4!=i14)). % 20.48/8.93 tff(c_1948, plain, (i8!=i40)). % 20.48/8.93 tff(c_2424, plain, (i3!=i22)). % 20.48/8.93 tff(c_606, plain, (i40!=i30)). % 20.48/8.93 tff(c_1632, plain, (i40!=i12)). % 20.48/8.93 tff(c_608, plain, (i39!=i30)). % 20.48/8.93 tff(c_610, plain, (i38!=i30)). % 20.48/8.93 tff(c_1634, plain, (i39!=i12)). % 20.48/8.93 tff(c_2600, plain, (i29!=i1)). % 20.48/8.93 tff(c_2146, plain, (i6!=i26)). % 20.48/8.93 tff(c_2402, plain, (i33!=i3)). % 20.48/8.93 tff(c_2530, plain, (i2!=i16)). % 20.48/8.93 tff(c_2432, plain, (i3!=i18)). % 20.48/8.93 tff(c_2594, plain, (i32!=i1)). % 20.48/8.93 tff(c_2626, plain, (i16!=i1)). % 20.48/8.93 tff(c_2642, plain, (i8!=i1)). % 20.48/8.93 tff(c_2650, plain, (i4!=i1)). % 20.48/8.93 tff(c_2654, plain, (i2!=i1)). % 20.48/8.93 tff(c_2656, plain, (a_1799!=a_1749)). % 20.48/8.93 % SZS output end Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 20.48/8.93 %------------------------------------------------------------------------------