Otter---3.3.UNK-Non.f

%------------------------------------------------------------------------------
% File     : Otter---3.3
% Problem  : SWV520-1.050 : TPTP v8.1.0. Released v4.0.0.
% Transfm  : none
% Format   : tptp:raw
% Command  : otter-tptp-script %s

% Computer : n006.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 Jul 27 13:21:02 EDT 2022

% Result   : Unknown 4.99s 5.09s
% Output   : None 
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.11  % Problem  : SWV520-1.050 : TPTP v8.1.0. Released v4.0.0.
% 0.11/0.12  % Command  : otter-tptp-script %s
% 0.13/0.33  % Computer : n006.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 Jul 27 05:41:02 EDT 2022
% 0.13/0.33  % CPUTime  : 
% 3.83/3.91  ----- Otter 3.3f, August 2004 -----
% 3.83/3.91  The process was started by sandbox2 on n006.cluster.edu,
% 3.83/3.91  Wed Jul 27 05:41:02 2022
% 3.83/3.91  The command was "./otter".  The process ID is 2995.
% 3.83/3.91  
% 3.83/3.91  set(prolog_style_variables).
% 3.83/3.91  set(auto).
% 3.83/3.91     dependent: set(auto1).
% 3.83/3.91     dependent: set(process_input).
% 3.83/3.91     dependent: clear(print_kept).
% 3.83/3.91     dependent: clear(print_new_demod).
% 3.83/3.91     dependent: clear(print_back_demod).
% 3.83/3.91     dependent: clear(print_back_sub).
% 3.83/3.91     dependent: set(control_memory).
% 3.83/3.91     dependent: assign(max_mem, 12000).
% 3.83/3.91     dependent: assign(pick_given_ratio, 4).
% 3.83/3.91     dependent: assign(stats_level, 1).
% 3.83/3.91     dependent: assign(max_seconds, 10800).
% 3.83/3.91  clear(print_given).
% 3.83/3.91  
% 3.83/3.91  list(usable).
% 3.83/3.91  0 [] A=A.
% 3.83/3.91  0 [] select(store(A,I,E),I)=E.
% 3.83/3.91  0 [] I=J|select(store(A,I,E),J)=select(A,J).
% 3.83/3.91  0 [] store(store(A,I,select(A,J)),J,select(A,I))=store(store(A,J,select(A,I)),I,select(A,J)).
% 3.83/3.91  0 [] a_1700=store(a1,i1,e1).
% 3.83/3.91  0 [] a_1701=store(a_1700,i2,e2).
% 3.83/3.91  0 [] a_1702=store(a_1701,i3,e3).
% 3.83/3.91  0 [] a_1703=store(a_1702,i4,e4).
% 3.83/3.91  0 [] a_1704=store(a_1703,i5,e5).
% 3.83/3.91  0 [] a_1705=store(a_1704,i6,e6).
% 3.83/3.91  0 [] a_1706=store(a_1705,i7,e7).
% 3.83/3.91  0 [] a_1707=store(a_1706,i8,e8).
% 3.83/3.91  0 [] a_1708=store(a_1707,i9,e9).
% 3.83/3.91  0 [] a_1709=store(a_1708,i10,e10).
% 3.83/3.91  0 [] a_1710=store(a_1709,i11,e11).
% 3.83/3.91  0 [] a_1711=store(a_1710,i12,e12).
% 3.83/3.91  0 [] a_1712=store(a_1711,i13,e13).
% 3.83/3.91  0 [] a_1713=store(a_1712,i14,e14).
% 3.83/3.91  0 [] a_1714=store(a_1713,i15,e15).
% 3.83/3.91  0 [] a_1715=store(a_1714,i16,e16).
% 3.83/3.91  0 [] a_1716=store(a_1715,i17,e17).
% 3.83/3.91  0 [] a_1717=store(a_1716,i18,e18).
% 3.83/3.91  0 [] a_1718=store(a_1717,i19,e19).
% 3.83/3.91  0 [] a_1719=store(a_1718,i20,e20).
% 3.83/3.91  0 [] a_1720=store(a_1719,i21,e21).
% 3.83/3.91  0 [] a_1721=store(a_1720,i22,e22).
% 3.83/3.91  0 [] a_1722=store(a_1721,i23,e23).
% 3.83/3.91  0 [] a_1723=store(a_1722,i24,e24).
% 3.83/3.91  0 [] a_1724=store(a_1723,i25,e25).
% 3.83/3.91  0 [] a_1725=store(a_1724,i26,e26).
% 3.83/3.91  0 [] a_1726=store(a_1725,i27,e27).
% 3.83/3.91  0 [] a_1727=store(a_1726,i28,e28).
% 3.83/3.91  0 [] a_1728=store(a_1727,i29,e29).
% 3.83/3.91  0 [] a_1729=store(a_1728,i30,e30).
% 3.83/3.91  0 [] a_1730=store(a_1729,i31,e31).
% 3.83/3.91  0 [] a_1731=store(a_1730,i32,e32).
% 3.83/3.91  0 [] a_1732=store(a_1731,i33,e33).
% 3.83/3.91  0 [] a_1733=store(a_1732,i34,e34).
% 3.83/3.91  0 [] a_1734=store(a_1733,i35,e35).
% 3.83/3.91  0 [] a_1735=store(a_1734,i36,e36).
% 3.83/3.91  0 [] a_1736=store(a_1735,i37,e37).
% 3.83/3.91  0 [] a_1737=store(a_1736,i38,e38).
% 3.83/3.91  0 [] a_1738=store(a_1737,i39,e39).
% 3.83/3.91  0 [] a_1739=store(a_1738,i40,e40).
% 3.83/3.91  0 [] a_1740=store(a_1739,i41,e41).
% 3.83/3.91  0 [] a_1741=store(a_1740,i42,e42).
% 3.83/3.91  0 [] a_1742=store(a_1741,i43,e43).
% 3.83/3.91  0 [] a_1743=store(a_1742,i44,e44).
% 3.83/3.91  0 [] a_1744=store(a_1743,i45,e45).
% 3.83/3.91  0 [] a_1745=store(a_1744,i46,e46).
% 3.83/3.91  0 [] a_1746=store(a_1745,i47,e47).
% 3.83/3.91  0 [] a_1747=store(a_1746,i48,e48).
% 3.83/3.91  0 [] a_1748=store(a_1747,i49,e49).
% 3.83/3.91  0 [] a_1749=store(a_1748,i1,e1).
% 3.83/3.91  0 [] a_1750=store(a1,i41,e41).
% 3.83/3.91  0 [] a_1751=store(a_1750,i30,e30).
% 3.83/3.91  0 [] a_1752=store(a_1751,i45,e45).
% 3.83/3.91  0 [] a_1753=store(a_1752,i43,e43).
% 3.83/3.91  0 [] a_1754=store(a_1753,i28,e28).
% 3.83/3.91  0 [] a_1755=store(a_1754,i19,e19).
% 3.83/3.91  0 [] a_1756=store(a_1755,i22,e22).
% 3.83/3.91  0 [] a_1757=store(a_1756,i39,e39).
% 3.83/3.91  0 [] a_1758=store(a_1757,i20,e20).
% 3.83/3.91  0 [] a_1759=store(a_1758,i40,e40).
% 3.83/3.91  0 [] a_1760=store(a_1759,i16,e16).
% 3.83/3.91  0 [] a_1761=store(a_1760,i8,e8).
% 3.83/3.91  0 [] a_1762=store(a_1761,i49,e49).
% 3.83/3.91  0 [] a_1763=store(a_1762,i14,e14).
% 3.83/3.91  0 [] a_1764=store(a_1763,i13,e13).
% 3.83/3.91  0 [] a_1765=store(a_1764,i6,e6).
% 3.83/3.91  0 [] a_1766=store(a_1765,i27,e27).
% 3.83/3.91  0 [] a_1767=store(a_1766,i15,e15).
% 3.83/3.91  0 [] a_1768=store(a_1767,i7,e7).
% 3.83/3.91  0 [] a_1769=store(a_1768,i33,e33).
% 3.83/3.91  0 [] a_1770=store(a_1769,i9,e9).
% 3.83/3.91  0 [] a_1771=store(a_1770,i17,e17).
% 3.83/3.91  0 [] a_1772=store(a_1771,i42,e42).
% 3.83/3.91  0 [] a_1773=store(a_1772,i47,e47).
% 3.83/3.91  0 [] a_1774=store(a_1773,i18,e18).
% 3.83/3.91  0 [] a_1775=store(a_1774,i26,e26).
% 3.83/3.91  0 [] a_1776=store(a_1775,i34,e34).
% 3.83/3.91  0 [] a_1777=store(a_1776,i11,e11).
% 3.83/3.91  0 [] a_1778=store(a_1777,i36,e36).
% 3.83/3.91  0 [] a_1779=store(a_1778,i44,e44).
% 3.83/3.91  0 [] a_1780=store(a_1779,i38,e38).
% 3.83/3.91  0 [] a_1781=store(a_1780,i23,e23).
% 3.83/3.91  0 [] a_1782=store(a_1781,i25,e25).
% 3.83/3.91  0 [] a_1783=store(a_1782,i46,e46).
% 3.83/3.91  0 [] a_1784=store(a_1783,i35,e35).
% 3.83/3.91  0 [] a_1785=store(a_1784,i50,e50).
% 3.83/3.91  0 [] a_1786=store(a_1785,i2,e2).
% 3.83/3.91  0 [] a_1787=store(a_1786,i10,e10).
% 3.83/3.91  0 [] a_1788=store(a_1787,i48,e48).
% 3.83/3.91  0 [] a_1789=store(a_1788,i29,e29).
% 3.83/3.91  0 [] a_1790=store(a_1789,i3,e3).
% 3.83/3.91  0 [] a_1791=store(a_1790,i37,e37).
% 3.83/3.91  0 [] a_1792=store(a_1791,i12,e12).
% 3.83/3.91  0 [] a_1793=store(a_1792,i5,e5).
% 3.83/3.91  0 [] a_1794=store(a_1793,i32,e32).
% 3.83/3.91  0 [] a_1795=store(a_1794,i4,e4).
% 3.83/3.91  0 [] a_1796=store(a_1795,i24,e24).
% 3.83/3.91  0 [] a_1797=store(a_1796,i21,e21).
% 3.83/3.91  0 [] a_1798=store(a_1797,i31,e31).
% 3.83/3.91  0 [] a_1799=store(a_1798,i1,e1).
% 3.83/3.91  0 [] i49!=i50.
% 3.83/3.91  0 [] i48!=i50.
% 3.83/3.91  0 [] i48!=i49.
% 3.83/3.91  0 [] i47!=i50.
% 3.83/3.91  0 [] i47!=i49.
% 3.83/3.91  0 [] i47!=i48.
% 3.83/3.91  0 [] i46!=i50.
% 3.83/3.91  0 [] i46!=i49.
% 3.83/3.91  0 [] i46!=i48.
% 3.83/3.91  0 [] i46!=i47.
% 3.83/3.91  0 [] i45!=i50.
% 3.83/3.91  0 [] i45!=i49.
% 3.83/3.91  0 [] i45!=i48.
% 3.83/3.91  0 [] i45!=i47.
% 3.83/3.91  0 [] i45!=i46.
% 3.83/3.91  0 [] i44!=i50.
% 3.83/3.91  0 [] i44!=i49.
% 3.83/3.91  0 [] i44!=i48.
% 3.83/3.91  0 [] i44!=i47.
% 3.83/3.91  0 [] i44!=i46.
% 3.83/3.91  0 [] i44!=i45.
% 3.83/3.91  0 [] i43!=i50.
% 3.83/3.91  0 [] i43!=i49.
% 3.83/3.91  0 [] i43!=i48.
% 3.83/3.91  0 [] i43!=i47.
% 3.83/3.91  0 [] i43!=i46.
% 3.83/3.91  0 [] i43!=i45.
% 3.83/3.91  0 [] i43!=i44.
% 3.83/3.91  0 [] i42!=i50.
% 3.83/3.91  0 [] i42!=i49.
% 3.83/3.91  0 [] i42!=i48.
% 3.83/3.91  0 [] i42!=i47.
% 3.83/3.91  0 [] i42!=i46.
% 3.83/3.91  0 [] i42!=i45.
% 3.83/3.91  0 [] i42!=i44.
% 3.83/3.91  0 [] i42!=i43.
% 3.83/3.91  0 [] i41!=i50.
% 3.83/3.91  0 [] i41!=i49.
% 3.83/3.91  0 [] i41!=i48.
% 3.83/3.91  0 [] i41!=i47.
% 3.83/3.91  0 [] i41!=i46.
% 3.83/3.91  0 [] i41!=i45.
% 3.83/3.91  0 [] i41!=i44.
% 3.83/3.91  0 [] i41!=i43.
% 3.83/3.91  0 [] i41!=i42.
% 3.83/3.91  0 [] i40!=i50.
% 3.83/3.91  0 [] i40!=i49.
% 3.83/3.91  0 [] i40!=i48.
% 3.83/3.91  0 [] i40!=i47.
% 3.83/3.91  0 [] i40!=i46.
% 3.83/3.91  0 [] i40!=i45.
% 3.83/3.91  0 [] i40!=i44.
% 3.83/3.91  0 [] i40!=i43.
% 3.83/3.91  0 [] i40!=i42.
% 3.83/3.91  0 [] i40!=i41.
% 3.83/3.91  0 [] i39!=i50.
% 3.83/3.91  0 [] i39!=i49.
% 3.83/3.91  0 [] i39!=i48.
% 3.83/3.91  0 [] i39!=i47.
% 3.83/3.91  0 [] i39!=i46.
% 3.83/3.91  0 [] i39!=i45.
% 3.83/3.91  0 [] i39!=i44.
% 3.83/3.91  0 [] i39!=i43.
% 3.83/3.91  0 [] i39!=i42.
% 3.83/3.91  0 [] i39!=i41.
% 3.83/3.91  0 [] i39!=i40.
% 3.83/3.91  0 [] i38!=i50.
% 3.83/3.91  0 [] i38!=i49.
% 3.83/3.91  0 [] i38!=i48.
% 3.83/3.91  0 [] i38!=i47.
% 3.83/3.91  0 [] i38!=i46.
% 3.83/3.91  0 [] i38!=i45.
% 3.83/3.91  0 [] i38!=i44.
% 3.83/3.91  0 [] i38!=i43.
% 3.83/3.91  0 [] i38!=i42.
% 3.83/3.91  0 [] i38!=i41.
% 3.83/3.91  0 [] i38!=i40.
% 3.83/3.91  0 [] i38!=i39.
% 3.83/3.91  0 [] i37!=i50.
% 3.83/3.91  0 [] i37!=i49.
% 3.83/3.91  0 [] i37!=i48.
% 3.83/3.91  0 [] i37!=i47.
% 3.83/3.91  0 [] i37!=i46.
% 3.83/3.91  0 [] i37!=i45.
% 3.83/3.91  0 [] i37!=i44.
% 3.83/3.91  0 [] i37!=i43.
% 3.83/3.91  0 [] i37!=i42.
% 3.83/3.91  0 [] i37!=i41.
% 3.83/3.91  0 [] i37!=i40.
% 3.83/3.91  0 [] i37!=i39.
% 3.83/3.91  0 [] i37!=i38.
% 3.83/3.91  0 [] i36!=i50.
% 3.83/3.91  0 [] i36!=i49.
% 3.83/3.91  0 [] i36!=i48.
% 3.83/3.91  0 [] i36!=i47.
% 3.83/3.91  0 [] i36!=i46.
% 3.83/3.91  0 [] i36!=i45.
% 3.83/3.91  0 [] i36!=i44.
% 3.83/3.91  0 [] i36!=i43.
% 3.83/3.91  0 [] i36!=i42.
% 3.83/3.91  0 [] i36!=i41.
% 3.83/3.91  0 [] i36!=i40.
% 3.83/3.91  0 [] i36!=i39.
% 3.83/3.91  0 [] i36!=i38.
% 3.83/3.91  0 [] i36!=i37.
% 3.83/3.91  0 [] i35!=i50.
% 3.83/3.91  0 [] i35!=i49.
% 3.83/3.91  0 [] i35!=i48.
% 3.83/3.91  0 [] i35!=i47.
% 3.83/3.91  0 [] i35!=i46.
% 3.83/3.91  0 [] i35!=i45.
% 3.83/3.91  0 [] i35!=i44.
% 3.83/3.91  0 [] i35!=i43.
% 3.83/3.91  0 [] i35!=i42.
% 3.83/3.91  0 [] i35!=i41.
% 3.83/3.91  0 [] i35!=i40.
% 3.83/3.91  0 [] i35!=i39.
% 3.83/3.91  0 [] i35!=i38.
% 3.83/3.91  0 [] i35!=i37.
% 3.83/3.91  0 [] i35!=i36.
% 3.83/3.91  0 [] i34!=i50.
% 3.83/3.91  0 [] i34!=i49.
% 3.83/3.91  0 [] i34!=i48.
% 3.83/3.91  0 [] i34!=i47.
% 3.83/3.91  0 [] i34!=i46.
% 3.83/3.91  0 [] i34!=i45.
% 3.83/3.91  0 [] i34!=i44.
% 3.83/3.91  0 [] i34!=i43.
% 3.83/3.91  0 [] i34!=i42.
% 3.83/3.91  0 [] i34!=i41.
% 3.83/3.91  0 [] i34!=i40.
% 3.83/3.91  0 [] i34!=i39.
% 3.83/3.91  0 [] i34!=i38.
% 3.83/3.91  0 [] i34!=i37.
% 3.83/3.91  0 [] i34!=i36.
% 3.83/3.91  0 [] i34!=i35.
% 3.83/3.91  0 [] i33!=i50.
% 3.83/3.91  0 [] i33!=i49.
% 3.83/3.91  0 [] i33!=i48.
% 3.83/3.91  0 [] i33!=i47.
% 3.83/3.91  0 [] i33!=i46.
% 3.83/3.91  0 [] i33!=i45.
% 3.83/3.91  0 [] i33!=i44.
% 3.83/3.91  0 [] i33!=i43.
% 3.83/3.91  0 [] i33!=i42.
% 3.83/3.91  0 [] i33!=i41.
% 3.83/3.91  0 [] i33!=i40.
% 3.83/3.91  0 [] i33!=i39.
% 3.83/3.91  0 [] i33!=i38.
% 3.83/3.91  0 [] i33!=i37.
% 3.83/3.91  0 [] i33!=i36.
% 3.83/3.91  0 [] i33!=i35.
% 3.83/3.91  0 [] i33!=i34.
% 3.83/3.91  0 [] i32!=i50.
% 3.83/3.91  0 [] i32!=i49.
% 3.83/3.91  0 [] i32!=i48.
% 3.83/3.91  0 [] i32!=i47.
% 3.83/3.91  0 [] i32!=i46.
% 3.83/3.91  0 [] i32!=i45.
% 3.83/3.91  0 [] i32!=i44.
% 3.83/3.91  0 [] i32!=i43.
% 3.83/3.91  0 [] i32!=i42.
% 3.83/3.91  0 [] i32!=i41.
% 3.83/3.91  0 [] i32!=i40.
% 3.83/3.91  0 [] i32!=i39.
% 3.83/3.91  0 [] i32!=i38.
% 3.83/3.91  0 [] i32!=i37.
% 3.83/3.91  0 [] i32!=i36.
% 3.83/3.91  0 [] i32!=i35.
% 3.83/3.91  0 [] i32!=i34.
% 3.83/3.91  0 [] i32!=i33.
% 3.83/3.91  0 [] i31!=i50.
% 3.83/3.91  0 [] i31!=i49.
% 3.83/3.91  0 [] i31!=i48.
% 3.83/3.91  0 [] i31!=i47.
% 3.83/3.91  0 [] i31!=i46.
% 3.83/3.91  0 [] i31!=i45.
% 3.83/3.91  0 [] i31!=i44.
% 3.83/3.91  0 [] i31!=i43.
% 3.83/3.91  0 [] i31!=i42.
% 3.83/3.91  0 [] i31!=i41.
% 3.83/3.91  0 [] i31!=i40.
% 3.83/3.91  0 [] i31!=i39.
% 3.83/3.91  0 [] i31!=i38.
% 3.83/3.91  0 [] i31!=i37.
% 3.83/3.91  0 [] i31!=i36.
% 3.83/3.91  0 [] i31!=i35.
% 3.83/3.91  0 [] i31!=i34.
% 3.83/3.91  0 [] i31!=i33.
% 3.83/3.91  0 [] i31!=i32.
% 3.83/3.91  0 [] i30!=i50.
% 3.83/3.91  0 [] i30!=i49.
% 3.83/3.91  0 [] i30!=i48.
% 3.83/3.91  0 [] i30!=i47.
% 3.83/3.91  0 [] i30!=i46.
% 3.83/3.91  0 [] i30!=i45.
% 3.83/3.91  0 [] i30!=i44.
% 3.83/3.91  0 [] i30!=i43.
% 3.83/3.91  0 [] i30!=i42.
% 3.83/3.91  0 [] i30!=i41.
% 3.83/3.91  0 [] i30!=i40.
% 3.83/3.91  0 [] i30!=i39.
% 3.83/3.91  0 [] i30!=i38.
% 3.83/3.91  0 [] i30!=i37.
% 3.83/3.91  0 [] i30!=i36.
% 3.83/3.91  0 [] i30!=i35.
% 3.83/3.91  0 [] i30!=i34.
% 3.83/3.91  0 [] i30!=i33.
% 3.83/3.91  0 [] i30!=i32.
% 3.83/3.91  0 [] i30!=i31.
% 3.83/3.91  0 [] i29!=i50.
% 3.83/3.91  0 [] i29!=i49.
% 3.83/3.91  0 [] i29!=i48.
% 3.83/3.91  0 [] i29!=i47.
% 3.83/3.91  0 [] i29!=i46.
% 3.83/3.91  0 [] i29!=i45.
% 3.83/3.91  0 [] i29!=i44.
% 3.83/3.91  0 [] i29!=i43.
% 3.83/3.91  0 [] i29!=i42.
% 3.83/3.91  0 [] i29!=i41.
% 3.83/3.91  0 [] i29!=i40.
% 3.83/3.91  0 [] i29!=i39.
% 3.83/3.91  0 [] i29!=i38.
% 3.83/3.91  0 [] i29!=i37.
% 3.83/3.91  0 [] i29!=i36.
% 3.83/3.91  0 [] i29!=i35.
% 3.83/3.91  0 [] i29!=i34.
% 3.83/3.91  0 [] i29!=i33.
% 3.83/3.91  0 [] i29!=i32.
% 3.83/3.91  0 [] i29!=i31.
% 3.83/3.91  0 [] i29!=i30.
% 3.83/3.91  0 [] i28!=i50.
% 3.83/3.91  0 [] i28!=i49.
% 3.83/3.91  0 [] i28!=i48.
% 3.83/3.91  0 [] i28!=i47.
% 3.83/3.91  0 [] i28!=i46.
% 3.83/3.91  0 [] i28!=i45.
% 3.83/3.91  0 [] i28!=i44.
% 3.83/3.91  0 [] i28!=i43.
% 3.83/3.91  0 [] i28!=i42.
% 3.83/3.91  0 [] i28!=i41.
% 3.83/3.91  0 [] i28!=i40.
% 3.83/3.91  0 [] i28!=i39.
% 3.83/3.91  0 [] i28!=i38.
% 3.83/3.91  0 [] i28!=i37.
% 3.83/3.91  0 [] i28!=i36.
% 3.83/3.91  0 [] i28!=i35.
% 3.83/3.91  0 [] i28!=i34.
% 3.83/3.91  0 [] i28!=i33.
% 3.83/3.91  0 [] i28!=i32.
% 3.83/3.91  0 [] i28!=i31.
% 3.83/3.91  0 [] i28!=i30.
% 3.83/3.91  0 [] i28!=i29.
% 3.83/3.91  0 [] i27!=i50.
% 3.83/3.91  0 [] i27!=i49.
% 3.83/3.91  0 [] i27!=i48.
% 3.83/3.91  0 [] i27!=i47.
% 3.83/3.91  0 [] i27!=i46.
% 3.83/3.91  0 [] i27!=i45.
% 3.83/3.91  0 [] i27!=i44.
% 3.83/3.91  0 [] i27!=i43.
% 3.83/3.91  0 [] i27!=i42.
% 3.83/3.91  0 [] i27!=i41.
% 3.83/3.91  0 [] i27!=i40.
% 3.83/3.91  0 [] i27!=i39.
% 3.83/3.91  0 [] i27!=i38.
% 3.83/3.91  0 [] i27!=i37.
% 3.83/3.91  0 [] i27!=i36.
% 3.83/3.91  0 [] i27!=i35.
% 3.83/3.91  0 [] i27!=i34.
% 3.83/3.91  0 [] i27!=i33.
% 3.83/3.91  0 [] i27!=i32.
% 3.83/3.91  0 [] i27!=i31.
% 3.83/3.91  0 [] i27!=i30.
% 3.83/3.91  0 [] i27!=i29.
% 3.83/3.91  0 [] i27!=i28.
% 3.83/3.91  0 [] i26!=i50.
% 3.83/3.91  0 [] i26!=i49.
% 3.83/3.91  0 [] i26!=i48.
% 3.83/3.91  0 [] i26!=i47.
% 3.83/3.91  0 [] i26!=i46.
% 3.83/3.91  0 [] i26!=i45.
% 3.83/3.91  0 [] i26!=i44.
% 3.83/3.91  0 [] i26!=i43.
% 3.83/3.91  0 [] i26!=i42.
% 3.83/3.91  0 [] i26!=i41.
% 3.83/3.91  0 [] i26!=i40.
% 3.83/3.91  0 [] i26!=i39.
% 3.83/3.91  0 [] i26!=i38.
% 3.83/3.91  0 [] i26!=i37.
% 3.83/3.91  0 [] i26!=i36.
% 3.83/3.91  0 [] i26!=i35.
% 3.83/3.91  0 [] i26!=i34.
% 3.83/3.91  0 [] i26!=i33.
% 3.83/3.91  0 [] i26!=i32.
% 3.83/3.91  0 [] i26!=i31.
% 3.83/3.91  0 [] i26!=i30.
% 3.83/3.91  0 [] i26!=i29.
% 3.83/3.91  0 [] i26!=i28.
% 3.83/3.91  0 [] i26!=i27.
% 3.83/3.91  0 [] i25!=i50.
% 3.83/3.91  0 [] i25!=i49.
% 3.83/3.91  0 [] i25!=i48.
% 3.83/3.91  0 [] i25!=i47.
% 3.83/3.91  0 [] i25!=i46.
% 3.83/3.91  0 [] i25!=i45.
% 3.83/3.91  0 [] i25!=i44.
% 3.83/3.91  0 [] i25!=i43.
% 3.83/3.91  0 [] i25!=i42.
% 3.83/3.91  0 [] i25!=i41.
% 3.83/3.91  0 [] i25!=i40.
% 3.83/3.91  0 [] i25!=i39.
% 3.83/3.91  0 [] i25!=i38.
% 3.83/3.91  0 [] i25!=i37.
% 3.83/3.91  0 [] i25!=i36.
% 3.83/3.91  0 [] i25!=i35.
% 3.83/3.91  0 [] i25!=i34.
% 3.83/3.91  0 [] i25!=i33.
% 3.83/3.91  0 [] i25!=i32.
% 3.83/3.91  0 [] i25!=i31.
% 3.83/3.91  0 [] i25!=i30.
% 3.83/3.91  0 [] i25!=i29.
% 3.83/3.91  0 [] i25!=i28.
% 3.83/3.91  0 [] i25!=i27.
% 3.83/3.91  0 [] i25!=i26.
% 3.83/3.91  0 [] i24!=i50.
% 3.83/3.91  0 [] i24!=i49.
% 3.83/3.91  0 [] i24!=i48.
% 3.83/3.91  0 [] i24!=i47.
% 3.83/3.91  0 [] i24!=i46.
% 3.83/3.91  0 [] i24!=i45.
% 3.83/3.91  0 [] i24!=i44.
% 3.83/3.91  0 [] i24!=i43.
% 3.83/3.91  0 [] i24!=i42.
% 3.83/3.91  0 [] i24!=i41.
% 3.83/3.91  0 [] i24!=i40.
% 3.83/3.91  0 [] i24!=i39.
% 3.83/3.91  0 [] i24!=i38.
% 3.83/3.91  0 [] i24!=i37.
% 3.83/3.91  0 [] i24!=i36.
% 3.83/3.91  0 [] i24!=i35.
% 3.83/3.91  0 [] i24!=i34.
% 3.83/3.91  0 [] i24!=i33.
% 3.83/3.91  0 [] i24!=i32.
% 3.83/3.91  0 [] i24!=i31.
% 3.83/3.91  0 [] i24!=i30.
% 3.83/3.91  0 [] i24!=i29.
% 3.83/3.91  0 [] i24!=i28.
% 3.83/3.91  0 [] i24!=i27.
% 3.83/3.91  0 [] i24!=i26.
% 3.83/3.91  0 [] i24!=i25.
% 3.83/3.91  0 [] i23!=i50.
% 3.83/3.91  0 [] i23!=i49.
% 3.83/3.91  0 [] i23!=i48.
% 3.83/3.91  0 [] i23!=i47.
% 3.83/3.91  0 [] i23!=i46.
% 3.83/3.91  0 [] i23!=i45.
% 3.83/3.91  0 [] i23!=i44.
% 3.83/3.91  0 [] i23!=i43.
% 3.83/3.91  0 [] i23!=i42.
% 3.83/3.91  0 [] i23!=i41.
% 3.83/3.91  0 [] i23!=i40.
% 3.83/3.91  0 [] i23!=i39.
% 3.83/3.91  0 [] i23!=i38.
% 3.83/3.91  0 [] i23!=i37.
% 3.83/3.91  0 [] i23!=i36.
% 3.83/3.91  0 [] i23!=i35.
% 3.83/3.91  0 [] i23!=i34.
% 3.83/3.91  0 [] i23!=i33.
% 3.83/3.91  0 [] i23!=i32.
% 3.83/3.91  0 [] i23!=i31.
% 3.83/3.91  0 [] i23!=i30.
% 3.83/3.91  0 [] i23!=i29.
% 3.83/3.91  0 [] i23!=i28.
% 3.83/3.91  0 [] i23!=i27.
% 3.83/3.91  0 [] i23!=i26.
% 3.83/3.91  0 [] i23!=i25.
% 3.83/3.91  0 [] i23!=i24.
% 3.83/3.91  0 [] i22!=i50.
% 3.83/3.91  0 [] i22!=i49.
% 3.83/3.91  0 [] i22!=i48.
% 3.83/3.91  0 [] i22!=i47.
% 3.83/3.91  0 [] i22!=i46.
% 3.83/3.91  0 [] i22!=i45.
% 3.83/3.91  0 [] i22!=i44.
% 3.83/3.91  0 [] i22!=i43.
% 3.83/3.91  0 [] i22!=i42.
% 3.83/3.91  0 [] i22!=i41.
% 3.83/3.91  0 [] i22!=i40.
% 3.83/3.91  0 [] i22!=i39.
% 3.83/3.91  0 [] i22!=i38.
% 3.83/3.91  0 [] i22!=i37.
% 3.83/3.91  0 [] i22!=i36.
% 3.83/3.91  0 [] i22!=i35.
% 3.83/3.91  0 [] i22!=i34.
% 3.83/3.91  0 [] i22!=i33.
% 3.83/3.91  0 [] i22!=i32.
% 3.83/3.91  0 [] i22!=i31.
% 3.83/3.91  0 [] i22!=i30.
% 3.83/3.91  0 [] i22!=i29.
% 3.83/3.91  0 [] i22!=i28.
% 3.83/3.91  0 [] i22!=i27.
% 3.83/3.91  0 [] i22!=i26.
% 3.83/3.91  0 [] i22!=i25.
% 3.83/3.91  0 [] i22!=i24.
% 3.83/3.91  0 [] i22!=i23.
% 3.83/3.91  0 [] i21!=i50.
% 3.83/3.91  0 [] i21!=i49.
% 3.83/3.91  0 [] i21!=i48.
% 3.83/3.91  0 [] i21!=i47.
% 3.83/3.91  0 [] i21!=i46.
% 3.83/3.91  0 [] i21!=i45.
% 3.83/3.91  0 [] i21!=i44.
% 3.83/3.91  0 [] i21!=i43.
% 3.83/3.91  0 [] i21!=i42.
% 3.83/3.91  0 [] i21!=i41.
% 3.83/3.91  0 [] i21!=i40.
% 3.83/3.91  0 [] i21!=i39.
% 3.83/3.91  0 [] i21!=i38.
% 3.83/3.91  0 [] i21!=i37.
% 3.83/3.91  0 [] i21!=i36.
% 3.83/3.91  0 [] i21!=i35.
% 3.83/3.91  0 [] i21!=i34.
% 3.83/3.91  0 [] i21!=i33.
% 3.83/3.91  0 [] i21!=i32.
% 3.83/3.91  0 [] i21!=i31.
% 3.83/3.91  0 [] i21!=i30.
% 3.83/3.91  0 [] i21!=i29.
% 3.83/3.91  0 [] i21!=i28.
% 3.83/3.91  0 [] i21!=i27.
% 3.83/3.91  0 [] i21!=i26.
% 3.83/3.91  0 [] i21!=i25.
% 3.83/3.91  0 [] i21!=i24.
% 3.83/3.91  0 [] i21!=i23.
% 3.83/3.91  0 [] i21!=i22.
% 3.83/3.91  0 [] i20!=i50.
% 3.83/3.91  0 [] i20!=i49.
% 3.83/3.91  0 [] i20!=i48.
% 3.83/3.91  0 [] i20!=i47.
% 3.83/3.91  0 [] i20!=i46.
% 3.83/3.91  0 [] i20!=i45.
% 3.83/3.91  0 [] i20!=i44.
% 3.83/3.91  0 [] i20!=i43.
% 3.83/3.91  0 [] i20!=i42.
% 3.83/3.91  0 [] i20!=i41.
% 3.83/3.91  0 [] i20!=i40.
% 3.83/3.91  0 [] i20!=i39.
% 3.83/3.91  0 [] i20!=i38.
% 3.83/3.91  0 [] i20!=i37.
% 3.83/3.91  0 [] i20!=i36.
% 3.83/3.91  0 [] i20!=i35.
% 3.83/3.91  0 [] i20!=i34.
% 3.83/3.91  0 [] i20!=i33.
% 3.83/3.91  0 [] i20!=i32.
% 3.83/3.91  0 [] i20!=i31.
% 3.83/3.91  0 [] i20!=i30.
% 3.83/3.91  0 [] i20!=i29.
% 3.83/3.91  0 [] i20!=i28.
% 3.83/3.91  0 [] i20!=i27.
% 3.83/3.91  0 [] i20!=i26.
% 3.83/3.91  0 [] i20!=i25.
% 3.83/3.91  0 [] i20!=i24.
% 3.83/3.91  0 [] i20!=i23.
% 3.83/3.91  0 [] i20!=i22.
% 3.83/3.91  0 [] i20!=i21.
% 3.83/3.91  0 [] i19!=i50.
% 3.83/3.91  0 [] i19!=i49.
% 3.83/3.91  0 [] i19!=i48.
% 3.83/3.91  0 [] i19!=i47.
% 3.83/3.91  0 [] i19!=i46.
% 3.83/3.91  0 [] i19!=i45.
% 3.83/3.91  0 [] i19!=i44.
% 3.83/3.91  0 [] i19!=i43.
% 3.83/3.91  0 [] i19!=i42.
% 3.83/3.91  0 [] i19!=i41.
% 3.83/3.91  0 [] i19!=i40.
% 3.83/3.91  0 [] i19!=i39.
% 3.83/3.91  0 [] i19!=i38.
% 3.83/3.91  0 [] i19!=i37.
% 3.83/3.91  0 [] i19!=i36.
% 3.83/3.91  0 [] i19!=i35.
% 3.83/3.91  0 [] i19!=i34.
% 3.83/3.91  0 [] i19!=i33.
% 3.83/3.91  0 [] i19!=i32.
% 3.83/3.91  0 [] i19!=i31.
% 3.83/3.91  0 [] i19!=i30.
% 3.83/3.91  0 [] i19!=i29.
% 3.83/3.91  0 [] i19!=i28.
% 3.83/3.91  0 [] i19!=i27.
% 3.83/3.91  0 [] i19!=i26.
% 3.83/3.91  0 [] i19!=i25.
% 3.83/3.91  0 [] i19!=i24.
% 3.83/3.91  0 [] i19!=i23.
% 3.83/3.91  0 [] i19!=i22.
% 3.83/3.91  0 [] i19!=i21.
% 3.83/3.91  0 [] i19!=i20.
% 3.83/3.91  0 [] i18!=i50.
% 3.83/3.91  0 [] i18!=i49.
% 3.83/3.91  0 [] i18!=i48.
% 3.83/3.91  0 [] i18!=i47.
% 3.83/3.91  0 [] i18!=i46.
% 3.83/3.91  0 [] i18!=i45.
% 3.83/3.91  0 [] i18!=i44.
% 3.83/3.91  0 [] i18!=i43.
% 3.83/3.91  0 [] i18!=i42.
% 3.83/3.91  0 [] i18!=i41.
% 3.83/3.91  0 [] i18!=i40.
% 3.83/3.91  0 [] i18!=i39.
% 3.83/3.91  0 [] i18!=i38.
% 3.83/3.91  0 [] i18!=i37.
% 3.83/3.91  0 [] i18!=i36.
% 3.83/3.91  0 [] i18!=i35.
% 3.83/3.91  0 [] i18!=i34.
% 3.83/3.91  0 [] i18!=i33.
% 3.83/3.91  0 [] i18!=i32.
% 3.83/3.91  0 [] i18!=i31.
% 3.83/3.91  0 [] i18!=i30.
% 3.83/3.91  0 [] i18!=i29.
% 3.83/3.91  0 [] i18!=i28.
% 3.83/3.91  0 [] i18!=i27.
% 3.83/3.91  0 [] i18!=i26.
% 3.83/3.91  0 [] i18!=i25.
% 3.83/3.91  0 [] i18!=i24.
% 3.83/3.91  0 [] i18!=i23.
% 3.83/3.91  0 [] i18!=i22.
% 3.83/3.91  0 [] i18!=i21.
% 3.83/3.91  0 [] i18!=i20.
% 3.83/3.91  0 [] i18!=i19.
% 3.83/3.91  0 [] i17!=i50.
% 3.83/3.91  0 [] i17!=i49.
% 3.83/3.91  0 [] i17!=i48.
% 3.83/3.91  0 [] i17!=i47.
% 3.83/3.91  0 [] i17!=i46.
% 3.83/3.91  0 [] i17!=i45.
% 3.83/3.91  0 [] i17!=i44.
% 3.83/3.91  0 [] i17!=i43.
% 3.83/3.91  0 [] i17!=i42.
% 3.83/3.91  0 [] i17!=i41.
% 3.83/3.91  0 [] i17!=i40.
% 3.83/3.91  0 [] i17!=i39.
% 3.83/3.91  0 [] i17!=i38.
% 3.83/3.91  0 [] i17!=i37.
% 3.83/3.91  0 [] i17!=i36.
% 3.83/3.91  0 [] i17!=i35.
% 3.83/3.91  0 [] i17!=i34.
% 3.83/3.91  0 [] i17!=i33.
% 3.83/3.91  0 [] i17!=i32.
% 3.83/3.91  0 [] i17!=i31.
% 3.83/3.91  0 [] i17!=i30.
% 3.83/3.91  0 [] i17!=i29.
% 3.83/3.91  0 [] i17!=i28.
% 3.83/3.91  0 [] i17!=i27.
% 3.83/3.91  0 [] i17!=i26.
% 3.83/3.91  0 [] i17!=i25.
% 3.83/3.91  0 [] i17!=i24.
% 3.83/3.91  0 [] i17!=i23.
% 3.83/3.91  0 [] i17!=i22.
% 3.83/3.91  0 [] i17!=i21.
% 3.83/3.91  0 [] i17!=i20.
% 3.83/3.91  0 [] i17!=i19.
% 3.83/3.91  0 [] i17!=i18.
% 3.83/3.91  0 [] i16!=i50.
% 3.83/3.91  0 [] i16!=i49.
% 3.83/3.91  0 [] i16!=i48.
% 3.83/3.91  0 [] i16!=i47.
% 3.83/3.91  0 [] i16!=i46.
% 3.83/3.91  0 [] i16!=i45.
% 3.83/3.91  0 [] i16!=i44.
% 3.83/3.91  0 [] i16!=i43.
% 3.83/3.91  0 [] i16!=i42.
% 3.83/3.91  0 [] i16!=i41.
% 3.83/3.91  0 [] i16!=i40.
% 3.83/3.91  0 [] i16!=i39.
% 3.83/3.91  0 [] i16!=i38.
% 3.83/3.91  0 [] i16!=i37.
% 3.83/3.91  0 [] i16!=i36.
% 3.83/3.91  0 [] i16!=i35.
% 3.83/3.91  0 [] i16!=i34.
% 3.83/3.91  0 [] i16!=i33.
% 3.83/3.91  0 [] i16!=i32.
% 3.83/3.91  0 [] i16!=i31.
% 3.83/3.91  0 [] i16!=i30.
% 3.83/3.91  0 [] i16!=i29.
% 3.83/3.91  0 [] i16!=i28.
% 3.83/3.91  0 [] i16!=i27.
% 3.83/3.91  0 [] i16!=i26.
% 3.83/3.91  0 [] i16!=i25.
% 3.83/3.91  0 [] i16!=i24.
% 3.83/3.91  0 [] i16!=i23.
% 3.83/3.91  0 [] i16!=i22.
% 3.83/3.91  0 [] i16!=i21.
% 3.83/3.91  0 [] i16!=i20.
% 3.83/3.91  0 [] i16!=i19.
% 3.83/3.91  0 [] i16!=i18.
% 3.83/3.91  0 [] i16!=i17.
% 3.83/3.91  0 [] i15!=i50.
% 3.83/3.91  0 [] i15!=i49.
% 3.83/3.91  0 [] i15!=i48.
% 3.83/3.91  0 [] i15!=i47.
% 3.83/3.91  0 [] i15!=i46.
% 3.83/3.91  0 [] i15!=i45.
% 3.83/3.91  0 [] i15!=i44.
% 3.83/3.91  0 [] i15!=i43.
% 3.83/3.91  0 [] i15!=i42.
% 3.83/3.91  0 [] i15!=i41.
% 3.83/3.91  0 [] i15!=i40.
% 3.83/3.91  0 [] i15!=i39.
% 3.83/3.91  0 [] i15!=i38.
% 3.83/3.91  0 [] i15!=i37.
% 3.83/3.91  0 [] i15!=i36.
% 3.83/3.91  0 [] i15!=i35.
% 3.83/3.91  0 [] i15!=i34.
% 3.83/3.91  0 [] i15!=i33.
% 3.83/3.91  0 [] i15!=i32.
% 3.83/3.91  0 [] i15!=i31.
% 3.83/3.91  0 [] i15!=i30.
% 3.83/3.91  0 [] i15!=i29.
% 3.83/3.91  0 [] i15!=i28.
% 3.83/3.91  0 [] i15!=i27.
% 3.83/3.91  0 [] i15!=i26.
% 3.83/3.91  0 [] i15!=i25.
% 3.83/3.91  0 [] i15!=i24.
% 3.83/3.91  0 [] i15!=i23.
% 3.83/3.91  0 [] i15!=i22.
% 3.83/3.91  0 [] i15!=i21.
% 3.83/3.91  0 [] i15!=i20.
% 3.83/3.91  0 [] i15!=i19.
% 3.83/3.91  0 [] i15!=i18.
% 3.83/3.91  0 [] i15!=i17.
% 3.83/3.91  0 [] i15!=i16.
% 3.83/3.91  0 [] i14!=i50.
% 3.83/3.91  0 [] i14!=i49.
% 3.83/3.91  0 [] i14!=i48.
% 3.83/3.91  0 [] i14!=i47.
% 3.83/3.91  0 [] i14!=i46.
% 3.83/3.91  0 [] i14!=i45.
% 3.83/3.91  0 [] i14!=i44.
% 3.83/3.91  0 [] i14!=i43.
% 3.83/3.91  0 [] i14!=i42.
% 3.83/3.91  0 [] i14!=i41.
% 3.83/3.91  0 [] i14!=i40.
% 3.83/3.91  0 [] i14!=i39.
% 3.83/3.91  0 [] i14!=i38.
% 3.83/3.91  0 [] i14!=i37.
% 3.83/3.91  0 [] i14!=i36.
% 3.83/3.91  0 [] i14!=i35.
% 3.83/3.91  0 [] i14!=i34.
% 3.83/3.91  0 [] i14!=i33.
% 3.83/3.91  0 [] i14!=i32.
% 3.83/3.91  0 [] i14!=i31.
% 3.83/3.91  0 [] i14!=i30.
% 3.83/3.91  0 [] i14!=i29.
% 3.83/3.91  0 [] i14!=i28.
% 3.83/3.91  0 [] i14!=i27.
% 3.83/3.91  0 [] i14!=i26.
% 3.83/3.91  0 [] i14!=i25.
% 3.83/3.91  0 [] i14!=i24.
% 3.83/3.91  0 [] i14!=i23.
% 3.83/3.91  0 [] i14!=i22.
% 3.83/3.91  0 [] i14!=i21.
% 3.83/3.91  0 [] i14!=i20.
% 3.83/3.91  0 [] i14!=i19.
% 3.83/3.91  0 [] i14!=i18.
% 3.83/3.91  0 [] i14!=i17.
% 3.83/3.91  0 [] i14!=i16.
% 3.83/3.91  0 [] i14!=i15.
% 3.83/3.91  0 [] i13!=i50.
% 3.83/3.91  0 [] i13!=i49.
% 3.83/3.91  0 [] i13!=i48.
% 3.83/3.91  0 [] i13!=i47.
% 3.83/3.91  0 [] i13!=i46.
% 3.83/3.91  0 [] i13!=i45.
% 3.83/3.91  0 [] i13!=i44.
% 3.83/3.91  0 [] i13!=i43.
% 3.83/3.91  0 [] i13!=i42.
% 3.83/3.91  0 [] i13!=i41.
% 3.83/3.91  0 [] i13!=i40.
% 3.83/3.91  0 [] i13!=i39.
% 3.83/3.91  0 [] i13!=i38.
% 3.83/3.91  0 [] i13!=i37.
% 3.83/3.91  0 [] i13!=i36.
% 3.83/3.91  0 [] i13!=i35.
% 3.83/3.91  0 [] i13!=i34.
% 3.83/3.91  0 [] i13!=i33.
% 3.83/3.91  0 [] i13!=i32.
% 3.83/3.91  0 [] i13!=i31.
% 3.83/3.91  0 [] i13!=i30.
% 3.83/3.91  0 [] i13!=i29.
% 3.83/3.91  0 [] i13!=i28.
% 3.83/3.91  0 [] i13!=i27.
% 3.83/3.91  0 [] i13!=i26.
% 3.83/3.91  0 [] i13!=i25.
% 3.83/3.91  0 [] i13!=i24.
% 3.83/3.91  0 [] i13!=i23.
% 3.83/3.91  0 [] i13!=i22.
% 3.83/3.91  0 [] i13!=i21.
% 3.83/3.91  0 [] i13!=i20.
% 3.83/3.91  0 [] i13!=i19.
% 3.83/3.91  0 [] i13!=i18.
% 3.83/3.91  0 [] i13!=i17.
% 3.83/3.91  0 [] i13!=i16.
% 3.83/3.91  0 [] i13!=i15.
% 3.83/3.91  0 [] i13!=i14.
% 3.83/3.91  0 [] i12!=i50.
% 3.83/3.91  0 [] i12!=i49.
% 3.83/3.91  0 [] i12!=i48.
% 3.83/3.91  0 [] i12!=i47.
% 3.83/3.91  0 [] i12!=i46.
% 3.83/3.91  0 [] i12!=i45.
% 3.83/3.91  0 [] i12!=i44.
% 3.83/3.91  0 [] i12!=i43.
% 3.83/3.91  0 [] i12!=i42.
% 3.83/3.91  0 [] i12!=i41.
% 3.83/3.91  0 [] i12!=i40.
% 3.83/3.91  0 [] i12!=i39.
% 3.83/3.91  0 [] i12!=i38.
% 3.83/3.91  0 [] i12!=i37.
% 3.83/3.91  0 [] i12!=i36.
% 3.83/3.91  0 [] i12!=i35.
% 3.83/3.91  0 [] i12!=i34.
% 3.83/3.91  0 [] i12!=i33.
% 3.83/3.91  0 [] i12!=i32.
% 3.83/3.91  0 [] i12!=i31.
% 3.83/3.91  0 [] i12!=i30.
% 3.83/3.91  0 [] i12!=i29.
% 3.83/3.91  0 [] i12!=i28.
% 3.83/3.91  0 [] i12!=i27.
% 3.83/3.91  0 [] i12!=i26.
% 3.83/3.91  0 [] i12!=i25.
% 3.83/3.91  0 [] i12!=i24.
% 3.83/3.91  0 [] i12!=i23.
% 3.83/3.91  0 [] i12!=i22.
% 3.83/3.91  0 [] i12!=i21.
% 3.83/3.91  0 [] i12!=i20.
% 3.83/3.91  0 [] i12!=i19.
% 3.83/3.91  0 [] i12!=i18.
% 3.83/3.91  0 [] i12!=i17.
% 3.83/3.91  0 [] i12!=i16.
% 3.83/3.91  0 [] i12!=i15.
% 3.83/3.91  0 [] i12!=i14.
% 3.83/3.91  0 [] i12!=i13.
% 3.83/3.91  0 [] i11!=i50.
% 3.83/3.91  0 [] i11!=i49.
% 3.83/3.91  0 [] i11!=i48.
% 3.83/3.91  0 [] i11!=i47.
% 3.83/3.91  0 [] i11!=i46.
% 3.83/3.91  0 [] i11!=i45.
% 3.83/3.91  0 [] i11!=i44.
% 3.83/3.91  0 [] i11!=i43.
% 3.83/3.91  0 [] i11!=i42.
% 3.83/3.91  0 [] i11!=i41.
% 3.83/3.91  0 [] i11!=i40.
% 3.83/3.91  0 [] i11!=i39.
% 3.83/3.91  0 [] i11!=i38.
% 3.83/3.91  0 [] i11!=i37.
% 3.83/3.91  0 [] i11!=i36.
% 3.83/3.91  0 [] i11!=i35.
% 3.83/3.91  0 [] i11!=i34.
% 3.83/3.91  0 [] i11!=i33.
% 3.83/3.91  0 [] i11!=i32.
% 3.83/3.91  0 [] i11!=i31.
% 3.83/3.91  0 [] i11!=i30.
% 3.83/3.91  0 [] i11!=i29.
% 3.83/3.91  0 [] i11!=i28.
% 3.83/3.91  0 [] i11!=i27.
% 3.83/3.91  0 [] i11!=i26.
% 3.83/3.91  0 [] i11!=i25.
% 3.83/3.91  0 [] i11!=i24.
% 3.83/3.91  0 [] i11!=i23.
% 3.83/3.91  0 [] i11!=i22.
% 3.83/3.91  0 [] i11!=i21.
% 3.83/3.91  0 [] i11!=i20.
% 3.83/3.91  0 [] i11!=i19.
% 3.83/3.91  0 [] i11!=i18.
% 3.83/3.91  0 [] i11!=i17.
% 3.83/3.91  0 [] i11!=i16.
% 3.83/3.91  0 [] i11!=i15.
% 3.83/3.91  0 [] i11!=i14.
% 3.83/3.91  0 [] i11!=i13.
% 3.83/3.91  0 [] i11!=i12.
% 3.83/3.91  0 [] i10!=i50.
% 3.83/3.91  0 [] i10!=i49.
% 3.83/3.91  0 [] i10!=i48.
% 3.83/3.91  0 [] i10!=i47.
% 3.83/3.91  0 [] i10!=i46.
% 3.83/3.91  0 [] i10!=i45.
% 3.83/3.91  0 [] i10!=i44.
% 3.83/3.91  0 [] i10!=i43.
% 3.83/3.91  0 [] i10!=i42.
% 3.83/3.91  0 [] i10!=i41.
% 3.83/3.91  0 [] i10!=i40.
% 3.83/3.91  0 [] i10!=i39.
% 3.83/3.91  0 [] i10!=i38.
% 3.83/3.91  0 [] i10!=i37.
% 3.83/3.91  0 [] i10!=i36.
% 3.83/3.91  0 [] i10!=i35.
% 3.83/3.91  0 [] i10!=i34.
% 3.83/3.91  0 [] i10!=i33.
% 3.83/3.91  0 [] i10!=i32.
% 3.83/3.91  0 [] i10!=i31.
% 3.83/3.91  0 [] i10!=i30.
% 3.83/3.91  0 [] i10!=i29.
% 3.83/3.91  0 [] i10!=i28.
% 3.83/3.91  0 [] i10!=i27.
% 3.83/3.91  0 [] i10!=i26.
% 3.83/3.91  0 [] i10!=i25.
% 3.83/3.91  0 [] i10!=i24.
% 3.83/3.92  0 [] i10!=i23.
% 3.83/3.92  0 [] i10!=i22.
% 3.83/3.92  0 [] i10!=i21.
% 3.83/3.92  0 [] i10!=i20.
% 3.83/3.92  0 [] i10!=i19.
% 3.83/3.92  0 [] i10!=i18.
% 3.83/3.92  0 [] i10!=i17.
% 3.83/3.92  0 [] i10!=i16.
% 3.83/3.92  0 [] i10!=i15.
% 3.83/3.92  0 [] i10!=i14.
% 3.83/3.92  0 [] i10!=i13.
% 3.83/3.92  0 [] i10!=i12.
% 3.83/3.92  0 [] i10!=i11.
% 3.83/3.92  0 [] i9!=i50.
% 3.83/3.92  0 [] i9!=i49.
% 3.83/3.92  0 [] i9!=i48.
% 3.83/3.92  0 [] i9!=i47.
% 3.83/3.92  0 [] i9!=i46.
% 3.83/3.92  0 [] i9!=i45.
% 3.83/3.92  0 [] i9!=i44.
% 3.83/3.92  0 [] i9!=i43.
% 3.83/3.92  0 [] i9!=i42.
% 3.83/3.92  0 [] i9!=i41.
% 3.83/3.92  0 [] i9!=i40.
% 3.83/3.92  0 [] i9!=i39.
% 3.83/3.92  0 [] i9!=i38.
% 3.83/3.92  0 [] i9!=i37.
% 3.83/3.92  0 [] i9!=i36.
% 3.83/3.92  0 [] i9!=i35.
% 3.83/3.92  0 [] i9!=i34.
% 3.83/3.92  0 [] i9!=i33.
% 3.83/3.92  0 [] i9!=i32.
% 3.83/3.92  0 [] i9!=i31.
% 3.83/3.92  0 [] i9!=i30.
% 3.83/3.92  0 [] i9!=i29.
% 3.83/3.92  0 [] i9!=i28.
% 3.83/3.92  0 [] i9!=i27.
% 3.83/3.92  0 [] i9!=i26.
% 3.83/3.92  0 [] i9!=i25.
% 3.83/3.92  0 [] i9!=i24.
% 3.83/3.92  0 [] i9!=i23.
% 3.83/3.92  0 [] i9!=i22.
% 3.83/3.92  0 [] i9!=i21.
% 3.83/3.92  0 [] i9!=i20.
% 3.83/3.92  0 [] i9!=i19.
% 3.83/3.92  0 [] i9!=i18.
% 3.83/3.92  0 [] i9!=i17.
% 3.83/3.92  0 [] i9!=i16.
% 3.83/3.92  0 [] i9!=i15.
% 3.83/3.92  0 [] i9!=i14.
% 3.83/3.92  0 [] i9!=i13.
% 3.83/3.92  0 [] i9!=i12.
% 3.83/3.92  0 [] i9!=i11.
% 3.83/3.92  0 [] i9!=i10.
% 3.83/3.92  0 [] i8!=i50.
% 3.83/3.92  0 [] i8!=i49.
% 3.83/3.92  0 [] i8!=i48.
% 3.83/3.92  0 [] i8!=i47.
% 3.83/3.92  0 [] i8!=i46.
% 3.83/3.92  0 [] i8!=i45.
% 3.83/3.92  0 [] i8!=i44.
% 3.83/3.92  0 [] i8!=i43.
% 3.83/3.92  0 [] i8!=i42.
% 3.83/3.92  0 [] i8!=i41.
% 3.83/3.92  0 [] i8!=i40.
% 3.83/3.92  0 [] i8!=i39.
% 3.83/3.92  0 [] i8!=i38.
% 3.83/3.92  0 [] i8!=i37.
% 3.83/3.92  0 [] i8!=i36.
% 3.83/3.92  0 [] i8!=i35.
% 3.83/3.92  0 [] i8!=i34.
% 3.83/3.92  0 [] i8!=i33.
% 3.83/3.92  0 [] i8!=i32.
% 3.83/3.92  0 [] i8!=i31.
% 3.83/3.92  0 [] i8!=i30.
% 3.83/3.92  0 [] i8!=i29.
% 3.83/3.92  0 [] i8!=i28.
% 3.83/3.92  0 [] i8!=i27.
% 3.83/3.92  0 [] i8!=i26.
% 3.83/3.92  0 [] i8!=i25.
% 3.83/3.92  0 [] i8!=i24.
% 3.83/3.92  0 [] i8!=i23.
% 3.83/3.92  0 [] i8!=i22.
% 3.83/3.92  0 [] i8!=i21.
% 3.83/3.92  0 [] i8!=i20.
% 3.83/3.92  0 [] i8!=i19.
% 3.83/3.92  0 [] i8!=i18.
% 3.83/3.92  0 [] i8!=i17.
% 3.83/3.92  0 [] i8!=i16.
% 3.83/3.92  0 [] i8!=i15.
% 3.83/3.92  0 [] i8!=i14.
% 3.83/3.92  0 [] i8!=i13.
% 3.83/3.92  0 [] i8!=i12.
% 3.83/3.92  0 [] i8!=i11.
% 3.83/3.92  0 [] i8!=i10.
% 3.83/3.92  0 [] i8!=i9.
% 3.83/3.92  0 [] i7!=i50.
% 3.83/3.92  0 [] i7!=i49.
% 3.83/3.92  0 [] i7!=i48.
% 3.83/3.92  0 [] i7!=i47.
% 3.83/3.92  0 [] i7!=i46.
% 3.83/3.92  0 [] i7!=i45.
% 3.83/3.92  0 [] i7!=i44.
% 3.83/3.92  0 [] i7!=i43.
% 3.83/3.92  0 [] i7!=i42.
% 3.83/3.92  0 [] i7!=i41.
% 3.83/3.92  0 [] i7!=i40.
% 3.83/3.92  0 [] i7!=i39.
% 3.83/3.92  0 [] i7!=i38.
% 3.83/3.92  0 [] i7!=i37.
% 3.83/3.92  0 [] i7!=i36.
% 3.83/3.92  0 [] i7!=i35.
% 3.83/3.92  0 [] i7!=i34.
% 3.83/3.92  0 [] i7!=i33.
% 3.83/3.92  0 [] i7!=i32.
% 3.83/3.92  0 [] i7!=i31.
% 3.83/3.92  0 [] i7!=i30.
% 3.83/3.92  0 [] i7!=i29.
% 3.83/3.92  0 [] i7!=i28.
% 3.83/3.92  0 [] i7!=i27.
% 3.83/3.92  0 [] i7!=i26.
% 3.83/3.92  0 [] i7!=i25.
% 3.83/3.92  0 [] i7!=i24.
% 3.83/3.92  0 [] i7!=i23.
% 3.83/3.92  0 [] i7!=i22.
% 3.83/3.92  0 [] i7!=i21.
% 3.83/3.92  0 [] i7!=i20.
% 3.83/3.92  0 [] i7!=i19.
% 3.83/3.92  0 [] i7!=i18.
% 3.83/3.92  0 [] i7!=i17.
% 3.83/3.92  0 [] i7!=i16.
% 3.83/3.92  0 [] i7!=i15.
% 3.83/3.92  0 [] i7!=i14.
% 3.83/3.92  0 [] i7!=i13.
% 3.83/3.92  0 [] i7!=i12.
% 3.83/3.92  0 [] i7!=i11.
% 3.83/3.92  0 [] i7!=i10.
% 3.83/3.92  0 [] i7!=i9.
% 3.83/3.92  0 [] i7!=i8.
% 3.83/3.92  0 [] i6!=i50.
% 3.83/3.92  0 [] i6!=i49.
% 3.83/3.92  0 [] i6!=i48.
% 3.83/3.92  0 [] i6!=i47.
% 3.83/3.92  0 [] i6!=i46.
% 3.83/3.92  0 [] i6!=i45.
% 3.83/3.92  0 [] i6!=i44.
% 3.83/3.92  0 [] i6!=i43.
% 3.83/3.92  0 [] i6!=i42.
% 3.83/3.92  0 [] i6!=i41.
% 3.83/3.92  0 [] i6!=i40.
% 3.83/3.92  0 [] i6!=i39.
% 3.83/3.92  0 [] i6!=i38.
% 3.83/3.92  0 [] i6!=i37.
% 3.83/3.92  0 [] i6!=i36.
% 3.83/3.92  0 [] i6!=i35.
% 3.83/3.92  0 [] i6!=i34.
% 3.83/3.92  0 [] i6!=i33.
% 3.83/3.92  0 [] i6!=i32.
% 3.83/3.92  0 [] i6!=i31.
% 3.83/3.92  0 [] i6!=i30.
% 3.83/3.92  0 [] i6!=i29.
% 3.83/3.92  0 [] i6!=i28.
% 3.83/3.92  0 [] i6!=i27.
% 3.83/3.92  0 [] i6!=i26.
% 3.83/3.92  0 [] i6!=i25.
% 3.83/3.92  0 [] i6!=i24.
% 3.83/3.92  0 [] i6!=i23.
% 3.83/3.92  0 [] i6!=i22.
% 3.83/3.92  0 [] i6!=i21.
% 3.83/3.92  0 [] i6!=i20.
% 3.83/3.92  0 [] i6!=i19.
% 3.83/3.92  0 [] i6!=i18.
% 3.83/3.92  0 [] i6!=i17.
% 3.83/3.92  0 [] i6!=i16.
% 3.83/3.92  0 [] i6!=i15.
% 3.83/3.92  0 [] i6!=i14.
% 3.83/3.92  0 [] i6!=i13.
% 3.83/3.92  0 [] i6!=i12.
% 3.83/3.92  0 [] i6!=i11.
% 3.83/3.92  0 [] i6!=i10.
% 3.83/3.92  0 [] i6!=i9.
% 3.83/3.92  0 [] i6!=i8.
% 3.83/3.92  0 [] i6!=i7.
% 3.83/3.92  0 [] i5!=i50.
% 3.83/3.92  0 [] i5!=i49.
% 3.83/3.92  0 [] i5!=i48.
% 3.83/3.92  0 [] i5!=i47.
% 3.83/3.92  0 [] i5!=i46.
% 3.83/3.92  0 [] i5!=i45.
% 3.83/3.92  0 [] i5!=i44.
% 3.83/3.92  0 [] i5!=i43.
% 3.83/3.92  0 [] i5!=i42.
% 3.83/3.92  0 [] i5!=i41.
% 3.83/3.92  0 [] i5!=i40.
% 3.83/3.92  0 [] i5!=i39.
% 3.83/3.92  0 [] i5!=i38.
% 3.83/3.92  0 [] i5!=i37.
% 3.83/3.92  0 [] i5!=i36.
% 3.83/3.92  0 [] i5!=i35.
% 3.83/3.92  0 [] i5!=i34.
% 3.83/3.92  0 [] i5!=i33.
% 3.83/3.92  0 [] i5!=i32.
% 3.83/3.92  0 [] i5!=i31.
% 3.83/3.92  0 [] i5!=i30.
% 3.83/3.92  0 [] i5!=i29.
% 3.83/3.92  0 [] i5!=i28.
% 3.83/3.92  0 [] i5!=i27.
% 3.83/3.92  0 [] i5!=i26.
% 3.83/3.92  0 [] i5!=i25.
% 3.83/3.92  0 [] i5!=i24.
% 3.83/3.92  0 [] i5!=i23.
% 3.83/3.92  0 [] i5!=i22.
% 3.83/3.92  0 [] i5!=i21.
% 3.83/3.92  0 [] i5!=i20.
% 3.83/3.92  0 [] i5!=i19.
% 3.83/3.92  0 [] i5!=i18.
% 3.83/3.92  0 [] i5!=i17.
% 3.83/3.92  0 [] i5!=i16.
% 3.83/3.92  0 [] i5!=i15.
% 3.83/3.92  0 [] i5!=i14.
% 3.83/3.92  0 [] i5!=i13.
% 3.83/3.92  0 [] i5!=i12.
% 3.83/3.92  0 [] i5!=i11.
% 3.83/3.92  0 [] i5!=i10.
% 3.83/3.92  0 [] i5!=i9.
% 3.83/3.92  0 [] i5!=i8.
% 3.83/3.92  0 [] i5!=i7.
% 3.83/3.92  0 [] i5!=i6.
% 3.83/3.92  0 [] i4!=i50.
% 3.83/3.92  0 [] i4!=i49.
% 3.83/3.92  0 [] i4!=i48.
% 3.83/3.92  0 [] i4!=i47.
% 3.83/3.92  0 [] i4!=i46.
% 3.83/3.92  0 [] i4!=i45.
% 3.83/3.92  0 [] i4!=i44.
% 3.83/3.92  0 [] i4!=i43.
% 3.83/3.92  0 [] i4!=i42.
% 3.83/3.92  0 [] i4!=i41.
% 3.83/3.92  0 [] i4!=i40.
% 3.83/3.92  0 [] i4!=i39.
% 3.83/3.92  0 [] i4!=i38.
% 3.83/3.92  0 [] i4!=i37.
% 3.83/3.92  0 [] i4!=i36.
% 3.83/3.92  0 [] i4!=i35.
% 3.83/3.92  0 [] i4!=i34.
% 3.83/3.92  0 [] i4!=i33.
% 3.83/3.92  0 [] i4!=i32.
% 3.83/3.92  0 [] i4!=i31.
% 3.83/3.92  0 [] i4!=i30.
% 3.83/3.92  0 [] i4!=i29.
% 3.83/3.92  0 [] i4!=i28.
% 3.83/3.92  0 [] i4!=i27.
% 3.83/3.92  0 [] i4!=i26.
% 3.83/3.92  0 [] i4!=i25.
% 3.83/3.92  0 [] i4!=i24.
% 3.83/3.92  0 [] i4!=i23.
% 3.83/3.92  0 [] i4!=i22.
% 3.83/3.92  0 [] i4!=i21.
% 3.83/3.92  0 [] i4!=i20.
% 3.83/3.92  0 [] i4!=i19.
% 3.83/3.92  0 [] i4!=i18.
% 3.83/3.92  0 [] i4!=i17.
% 3.83/3.92  0 [] i4!=i16.
% 3.83/3.92  0 [] i4!=i15.
% 3.83/3.92  0 [] i4!=i14.
% 3.83/3.92  0 [] i4!=i13.
% 3.83/3.92  0 [] i4!=i12.
% 3.83/3.92  0 [] i4!=i11.
% 3.83/3.92  0 [] i4!=i10.
% 3.83/3.92  0 [] i4!=i9.
% 3.83/3.92  0 [] i4!=i8.
% 3.83/3.92  0 [] i4!=i7.
% 3.83/3.92  0 [] i4!=i6.
% 3.83/3.92  0 [] i4!=i5.
% 3.83/3.92  0 [] i3!=i50.
% 3.83/3.92  0 [] i3!=i49.
% 3.83/3.92  0 [] i3!=i48.
% 3.83/3.92  0 [] i3!=i47.
% 3.83/3.92  0 [] i3!=i46.
% 3.83/3.92  0 [] i3!=i45.
% 3.83/3.92  0 [] i3!=i44.
% 3.83/3.92  0 [] i3!=i43.
% 3.83/3.92  0 [] i3!=i42.
% 3.83/3.92  0 [] i3!=i41.
% 3.83/3.92  0 [] i3!=i40.
% 3.83/3.92  0 [] i3!=i39.
% 3.83/3.92  0 [] i3!=i38.
% 3.83/3.92  0 [] i3!=i37.
% 3.83/3.92  0 [] i3!=i36.
% 3.83/3.92  0 [] i3!=i35.
% 3.83/3.92  0 [] i3!=i34.
% 3.83/3.92  0 [] i3!=i33.
% 3.83/3.92  0 [] i3!=i32.
% 3.83/3.92  0 [] i3!=i31.
% 3.83/3.92  0 [] i3!=i30.
% 3.83/3.92  0 [] i3!=i29.
% 3.83/3.92  0 [] i3!=i28.
% 3.83/3.92  0 [] i3!=i27.
% 3.83/3.92  0 [] i3!=i26.
% 3.83/3.92  0 [] i3!=i25.
% 3.83/3.92  0 [] i3!=i24.
% 3.83/3.92  0 [] i3!=i23.
% 3.83/3.92  0 [] i3!=i22.
% 3.83/3.92  0 [] i3!=i21.
% 3.83/3.92  0 [] i3!=i20.
% 3.83/3.92  0 [] i3!=i19.
% 3.83/3.92  0 [] i3!=i18.
% 3.83/3.92  0 [] i3!=i17.
% 3.83/3.92  0 [] i3!=i16.
% 3.83/3.92  0 [] i3!=i15.
% 3.83/3.92  0 [] i3!=i14.
% 3.83/3.92  0 [] i3!=i13.
% 3.83/3.92  0 [] i3!=i12.
% 3.83/3.92  0 [] i3!=i11.
% 3.83/3.92  0 [] i3!=i10.
% 3.83/3.92  0 [] i3!=i9.
% 3.83/3.92  0 [] i3!=i8.
% 3.83/3.92  0 [] i3!=i7.
% 3.83/3.92  0 [] i3!=i6.
% 3.83/3.92  0 [] i3!=i5.
% 3.83/3.92  0 [] i3!=i4.
% 3.83/3.92  0 [] i2!=i50.
% 3.83/3.92  0 [] i2!=i49.
% 3.83/3.92  0 [] i2!=i48.
% 3.83/3.92  0 [] i2!=i47.
% 3.83/3.92  0 [] i2!=i46.
% 3.83/3.92  0 [] i2!=i45.
% 3.83/3.92  0 [] i2!=i44.
% 3.83/3.92  0 [] i2!=i43.
% 3.83/3.92  0 [] i2!=i42.
% 3.83/3.92  0 [] i2!=i41.
% 3.83/3.92  0 [] i2!=i40.
% 3.83/3.92  0 [] i2!=i39.
% 3.83/3.92  0 [] i2!=i38.
% 3.83/3.92  0 [] i2!=i37.
% 3.83/3.92  0 [] i2!=i36.
% 3.83/3.92  0 [] i2!=i35.
% 3.83/3.92  0 [] i2!=i34.
% 3.83/3.92  0 [] i2!=i33.
% 3.83/3.92  0 [] i2!=i32.
% 3.83/3.92  0 [] i2!=i31.
% 3.83/3.92  0 [] i2!=i30.
% 3.83/3.92  0 [] i2!=i29.
% 3.83/3.92  0 [] i2!=i28.
% 3.83/3.92  0 [] i2!=i27.
% 3.83/3.92  0 [] i2!=i26.
% 3.83/3.92  0 [] i2!=i25.
% 3.83/3.92  0 [] i2!=i24.
% 3.83/3.92  0 [] i2!=i23.
% 3.83/3.92  0 [] i2!=i22.
% 3.83/3.92  0 [] i2!=i21.
% 3.83/3.92  0 [] i2!=i20.
% 3.83/3.92  0 [] i2!=i19.
% 3.83/3.92  0 [] i2!=i18.
% 3.83/3.92  0 [] i2!=i17.
% 3.83/3.92  0 [] i2!=i16.
% 3.83/3.92  0 [] i2!=i15.
% 3.83/3.92  0 [] i2!=i14.
% 3.83/3.92  0 [] i2!=i13.
% 3.83/3.92  0 [] i2!=i12.
% 3.83/3.92  0 [] i2!=i11.
% 3.83/3.92  0 [] i2!=i10.
% 3.83/3.92  0 [] i2!=i9.
% 3.83/3.92  0 [] i2!=i8.
% 3.83/3.92  0 [] i2!=i7.
% 3.83/3.92  0 [] i2!=i6.
% 3.83/3.92  0 [] i2!=i5.
% 3.83/3.92  0 [] i2!=i4.
% 3.83/3.92  0 [] i2!=i3.
% 3.83/3.92  0 [] i1!=i50.
% 3.83/3.92  0 [] i1!=i49.
% 3.83/3.92  0 [] i1!=i48.
% 3.83/3.92  0 [] i1!=i47.
% 3.83/3.92  0 [] i1!=i46.
% 3.83/3.92  0 [] i1!=i45.
% 3.83/3.92  0 [] i1!=i44.
% 3.83/3.92  0 [] i1!=i43.
% 3.83/3.92  0 [] i1!=i42.
% 3.83/3.92  0 [] i1!=i41.
% 3.83/3.92  0 [] i1!=i40.
% 3.83/3.92  0 [] i1!=i39.
% 3.83/3.92  0 [] i1!=i38.
% 3.83/3.92  0 [] i1!=i37.
% 3.83/3.92  0 [] i1!=i36.
% 3.83/3.92  0 [] i1!=i35.
% 3.83/3.92  0 [] i1!=i34.
% 3.83/3.92  0 [] i1!=i33.
% 3.83/3.92  0 [] i1!=i32.
% 3.83/3.92  0 [] i1!=i31.
% 3.83/3.92  0 [] i1!=i30.
% 3.83/3.92  0 [] i1!=i29.
% 3.83/3.92  0 [] i1!=i28.
% 3.83/3.92  0 [] i1!=i27.
% 3.83/3.92  0 [] i1!=i26.
% 3.83/3.92  0 [] i1!=i25.
% 3.83/3.92  0 [] i1!=i24.
% 3.83/3.92  0 [] i1!=i23.
% 3.83/3.92  0 [] i1!=i22.
% 3.83/3.92  0 [] i1!=i21.
% 3.83/3.92  0 [] i1!=i20.
% 3.83/3.92  0 [] i1!=i19.
% 3.83/3.92  0 [] i1!=i18.
% 3.83/3.92  0 [] i1!=i17.
% 3.83/3.92  0 [] i1!=i16.
% 3.83/3.92  0 [] i1!=i15.
% 3.83/3.92  0 [] i1!=i14.
% 3.83/3.92  0 [] i1!=i13.
% 3.83/3.92  0 [] i1!=i12.
% 3.83/3.92  0 [] i1!=i11.
% 3.83/3.92  0 [] i1!=i10.
% 3.83/3.92  0 [] i1!=i9.
% 3.83/3.92  0 [] i1!=i8.
% 3.83/3.92  0 [] i1!=i7.
% 3.83/3.92  0 [] i1!=i6.
% 3.83/3.92  0 [] i1!=i5.
% 3.83/3.92  0 [] i1!=i4.
% 3.83/3.92  0 [] i1!=i3.
% 3.83/3.92  0 [] i1!=i2.
% 3.83/3.92  0 [] a_1749!=a_1799.
% 3.83/3.92  end_of_list.
% 3.83/3.92  
% 3.83/3.92  SCAN INPUT: prop=0, horn=0, equality=1, symmetry=0, max_lits=2.
% 3.83/3.92  
% 3.83/3.92  This ia a non-Horn set with equality.  The strategy will be
% 3.83/3.92  Knuth-Bendix, ordered hyper_res, factoring, and unit
% 3.83/3.92  deletion, with positive clauses in sos and nonpositive
% 3.83/3.92  clauses in usable.
% 3.83/3.92  
% 3.83/3.92     dependent: set(knuth_bendix).
% 3.83/3.92     dependent: set(anl_eq).
% 3.83/3.92     dependent: set(para_from).
% 3.83/3.92     dependent: set(para_into).
% 3.83/3.92     dependent: clear(para_from_right).
% 3.83/3.92     dependent: clear(para_into_right).
% 3.83/3.92     dependent: set(para_from_vars).
% 3.83/3.92     dependent: set(eq_units_both_ways).
% 3.83/3.92     dependent: set(dynamic_demod_all).
% 3.83/3.92     dependent: set(dynamic_demod).
% 3.83/3.92     dependent: set(order_eq).
% 3.83/3.92     dependent: set(back_demod).
% 3.83/3.92     dependent: set(lrpo).
% 3.83/3.92     dependent: set(hyper_res).
% 3.83/3.92     dependent: set(unit_deletion).
% 3.83/3.92     dependent: set(factor).
% 3.83/3.92  
% 3.83/3.92  ------------> process usable:
% 3.83/3.92  ** KEPT (pick-wt=3): 2 [copy,1,flip.1] i50!=i49.
% 3.83/3.92  ** KEPT (pick-wt=3): 4 [copy,3,flip.1] i50!=i48.
% 3.83/3.92  ** KEPT (pick-wt=3): 6 [copy,5,flip.1] i49!=i48.
% 3.83/3.92  ** KEPT (pick-wt=3): 8 [copy,7,flip.1] i50!=i47.
% 3.83/3.92  ** KEPT (pick-wt=3): 10 [copy,9,flip.1] i49!=i47.
% 3.83/3.92  ** KEPT (pick-wt=3): 12 [copy,11,flip.1] i48!=i47.
% 3.83/3.92  ** KEPT (pick-wt=3): 14 [copy,13,flip.1] i50!=i46.
% 3.83/3.92  ** KEPT (pick-wt=3): 16 [copy,15,flip.1] i49!=i46.
% 3.83/3.92  ** KEPT (pick-wt=3): 18 [copy,17,flip.1] i48!=i46.
% 3.83/3.92  ** KEPT (pick-wt=3): 20 [copy,19,flip.1] i47!=i46.
% 3.83/3.92  ** KEPT (pick-wt=3): 22 [copy,21,flip.1] i50!=i45.
% 3.83/3.92  ** KEPT (pick-wt=3): 24 [copy,23,flip.1] i49!=i45.
% 3.83/3.92  ** KEPT (pick-wt=3): 26 [copy,25,flip.1] i48!=i45.
% 3.83/3.92  ** KEPT (pick-wt=3): 28 [copy,27,flip.1] i47!=i45.
% 3.83/3.92  ** KEPT (pick-wt=3): 30 [copy,29,flip.1] i46!=i45.
% 3.83/3.92  ** KEPT (pick-wt=3): 32 [copy,31,flip.1] i50!=i44.
% 3.83/3.92  ** KEPT (pick-wt=3): 34 [copy,33,flip.1] i49!=i44.
% 3.83/3.92  ** KEPT (pick-wt=3): 36 [copy,35,flip.1] i48!=i44.
% 3.83/3.92  ** KEPT (pick-wt=3): 38 [copy,37,flip.1] i47!=i44.
% 3.83/3.92  ** KEPT (pick-wt=3): 40 [copy,39,flip.1] i46!=i44.
% 3.83/3.92  ** KEPT (pick-wt=3): 42 [copy,41,flip.1] i45!=i44.
% 3.83/3.92  ** KEPT (pick-wt=3): 44 [copy,43,flip.1] i50!=i43.
% 3.83/3.92  ** KEPT (pick-wt=3): 46 [copy,45,flip.1] i49!=i43.
% 3.83/3.92  ** KEPT (pick-wt=3): 48 [copy,47,flip.1] i48!=i43.
% 3.83/3.92  ** KEPT (pick-wt=3): 50 [copy,49,flip.1] i47!=i43.
% 3.83/3.92  ** KEPT (pick-wt=3): 52 [copy,51,flip.1] i46!=i43.
% 3.83/3.92  ** KEPT (pick-wt=3): 54 [copy,53,flip.1] i45!=i43.
% 3.83/3.92  ** KEPT (pick-wt=3): 56 [copy,55,flip.1] i44!=i43.
% 3.83/3.92  ** KEPT (pick-wt=3): 58 [copy,57,flip.1] i50!=i42.
% 3.83/3.92  ** KEPT (pick-wt=3): 60 [copy,59,flip.1] i49!=i42.
% 3.83/3.92  ** KEPT (pick-wt=3): 62 [copy,61,flip.1] i48!=i42.
% 3.83/3.92  ** KEPT (pick-wt=3): 64 [copy,63,flip.1] i47!=i42.
% 3.83/3.92  ** KEPT (pick-wt=3): 66 [copy,65,flip.1] i46!=i42.
% 3.83/3.92  ** KEPT (pick-wt=3): 68 [copy,67,flip.1] i45!=i42.
% 3.83/3.92  ** KEPT (pick-wt=3): 70 [copy,69,flip.1] i44!=i42.
% 3.83/3.92  ** KEPT (pick-wt=3): 72 [copy,71,flip.1] i43!=i42.
% 3.83/3.92  ** KEPT (pick-wt=3): 74 [copy,73,flip.1] i50!=i41.
% 3.83/3.92  ** KEPT (pick-wt=3): 76 [copy,75,flip.1] i49!=i41.
% 3.83/3.92  ** KEPT (pick-wt=3): 78 [copy,77,flip.1] i48!=i41.
% 3.83/3.92  ** KEPT (pick-wt=3): 80 [copy,79,flip.1] i47!=i41.
% 3.83/3.92  ** KEPT (pick-wt=3): 82 [copy,81,flip.1] i46!=i41.
% 3.83/3.92  ** KEPT (pick-wt=3): 84 [copy,83,flip.1] i45!=i41.
% 3.83/3.92  ** KEPT (pick-wt=3): 86 [copy,85,flip.1] i44!=i41.
% 3.83/3.92  ** KEPT (pick-wt=3): 88 [copy,87,flip.1] i43!=i41.
% 3.83/3.92  ** KEPT (pick-wt=3): 90 [copy,89,flip.1] i42!=i41.
% 3.83/3.92  ** KEPT (pick-wt=3): 92 [copy,91,flip.1] i50!=i40.
% 3.83/3.92  ** KEPT (pick-wt=3): 94 [copy,93,flip.1] i49!=i40.
% 3.83/3.92  ** KEPT (pick-wt=3): 96 [copy,95,flip.1] i48!=i40.
% 3.83/3.92  ** KEPT (pick-wt=3): 98 [copy,97,flip.1] i47!=i40.
% 3.83/3.92  ** KEPT (pick-wt=3): 100 [copy,99,flip.1] i46!=i40.
% 3.83/3.92  ** KEPT (pick-wt=3): 102 [copy,101,flip.1] i45!=i40.
% 3.83/3.92  ** KEPT (pick-wt=3): 104 [copy,103,flip.1] i44!=i40.
% 3.83/3.92  ** KEPT (pick-wt=3): 106 [copy,105,flip.1] i43!=i40.
% 3.83/3.92  ** KEPT (pick-wt=3): 108 [copy,107,flip.1] i42!=i40.
% 3.83/3.92  ** KEPT (pick-wt=3): 110 [copy,109,flip.1] i41!=i40.
% 3.83/3.92  ** KEPT (pick-wt=3): 112 [copy,111,flip.1] i50!=i39.
% 3.83/3.92  ** KEPT (pick-wt=3): 114 [copy,113,flip.1] i49!=i39.
% 3.83/3.92  ** KEPT (pick-wt=3): 116 [copy,115,flip.1] i48!=i39.
% 3.83/3.92  ** KEPT (pick-wt=3): 118 [copy,117,flip.1] i47!=i39.
% 3.83/3.92  ** KEPT (pick-wt=3): 120 [copy,119,flip.1] i46!=i39.
% 3.83/3.92  ** KEPT (pick-wt=3): 122 [copy,121,flip.1] i45!=i39.
% 3.83/3.92  ** KEPT (pick-wt=3): 124 [copy,123,flip.1] i44!=i39.
% 3.83/3.92  ** KEPT (pick-wt=3): 126 [copy,125,flip.1] i43!=i39.
% 3.83/3.92  ** KEPT (pick-wt=3): 128 [copy,127,flip.1] i42!=i39.
% 3.83/3.92  ** KEPT (pick-wt=3): 130 [copy,129,flip.1] i41!=i39.
% 3.83/3.92  ** KEPT (pick-wt=3): 132 [copy,131,flip.1] i40!=i39.
% 3.83/3.92  ** KEPT (pick-wt=3): 134 [copy,133,flip.1] i50!=i38.
% 3.83/3.92  ** KEPT (pick-wt=3): 136 [copy,135,flip.1] i49!=i38.
% 3.83/3.92  ** KEPT (pick-wt=3): 138 [copy,137,flip.1] i48!=i38.
% 3.83/3.92  ** KEPT (pick-wt=3): 140 [copy,139,flip.1] i47!=i38.
% 3.83/3.92  ** KEPT (pick-wt=3): 142 [copy,141,flip.1] i46!=i38.
% 3.83/3.92  ** KEPT (pick-wt=3): 144 [copy,143,flip.1] i45!=i38.
% 3.83/3.92  ** KEPT (pick-wt=3): 146 [copy,145,flip.1] i44!=i38.
% 3.83/3.92  ** KEPT (pick-wt=3): 148 [copy,147,flip.1] i43!=i38.
% 3.83/3.92  ** KEPT (pick-wt=3): 150 [copy,149,flip.1] i42!=i38.
% 3.83/3.92  ** KEPT (pick-wt=3): 152 [copy,151,flip.1] i41!=i38.
% 3.83/3.92  ** KEPT (pick-wt=3): 154 [copy,153,flip.1] i40!=i38.
% 3.83/3.92  ** KEPT (pick-wt=3): 156 [copy,155,flip.1] i39!=i38.
% 3.83/3.92  ** KEPT (pick-wt=3): 158 [copy,157,flip.1] i50!=i37.
% 3.83/3.92  ** KEPT (pick-wt=3): 160 [copy,159,flip.1] i49!=i37.
% 3.83/3.92  ** KEPT (pick-wt=3): 162 [copy,161,flip.1] i48!=i37.
% 3.83/3.92  ** KEPT (pick-wt=3): 164 [copy,163,flip.1] i47!=i37.
% 3.83/3.92  ** KEPT (pick-wt=3): 166 [copy,165,flip.1] i46!=i37.
% 3.83/3.92  ** KEPT (pick-wt=3): 168 [copy,167,flip.1] i45!=i37.
% 3.83/3.92  ** KEPT (pick-wt=3): 170 [copy,169,flip.1] i44!=i37.
% 3.83/3.92  ** KEPT (pick-wt=3): 172 [copy,171,flip.1] i43!=i37.
% 3.83/3.92  ** KEPT (pick-wt=3): 174 [copy,173,flip.1] i42!=i37.
% 3.83/3.92  ** KEPT (pick-wt=3): 176 [copy,175,flip.1] i41!=i37.
% 3.83/3.92  ** KEPT (pick-wt=3): 178 [copy,177,flip.1] i40!=i37.
% 3.83/3.92  ** KEPT (pick-wt=3): 180 [copy,179,flip.1] i39!=i37.
% 3.83/3.92  ** KEPT (pick-wt=3): 182 [copy,181,flip.1] i38!=i37.
% 3.83/3.92  ** KEPT (pick-wt=3): 184 [copy,183,flip.1] i50!=i36.
% 3.83/3.92  ** KEPT (pick-wt=3): 186 [copy,185,flip.1] i49!=i36.
% 3.83/3.92  ** KEPT (pick-wt=3): 188 [copy,187,flip.1] i48!=i36.
% 3.83/3.92  ** KEPT (pick-wt=3): 190 [copy,189,flip.1] i47!=i36.
% 3.83/3.92  ** KEPT (pick-wt=3): 192 [copy,191,flip.1] i46!=i36.
% 3.83/3.92  ** KEPT (pick-wt=3): 194 [copy,193,flip.1] i45!=i36.
% 3.83/3.92  ** KEPT (pick-wt=3): 196 [copy,195,flip.1] i44!=i36.
% 3.83/3.92  ** KEPT (pick-wt=3): 198 [copy,197,flip.1] i43!=i36.
% 3.83/3.92  ** KEPT (pick-wt=3): 200 [copy,199,flip.1] i42!=i36.
% 3.83/3.92  ** KEPT (pick-wt=3): 202 [copy,201,flip.1] i41!=i36.
% 3.83/3.92  ** KEPT (pick-wt=3): 204 [copy,203,flip.1] i40!=i36.
% 3.83/3.92  ** KEPT (pick-wt=3): 206 [copy,205,flip.1] i39!=i36.
% 3.83/3.92  ** KEPT (pick-wt=3): 208 [copy,207,flip.1] i38!=i36.
% 3.83/3.92  ** KEPT (pick-wt=3): 210 [copy,209,flip.1] i37!=i36.
% 3.83/3.92  ** KEPT (pick-wt=3): 212 [copy,211,flip.1] i50!=i35.
% 3.83/3.92  ** KEPT (pick-wt=3): 214 [copy,213,flip.1] i49!=i35.
% 3.83/3.92  ** KEPT (pick-wt=3): 216 [copy,215,flip.1] i48!=i35.
% 3.83/3.92  ** KEPT (pick-wt=3): 218 [copy,217,flip.1] i47!=i35.
% 3.83/3.92  ** KEPT (pick-wt=3): 220 [copy,219,flip.1] i46!=i35.
% 3.83/3.92  ** KEPT (pick-wt=3): 222 [copy,221,flip.1] i45!=i35.
% 3.83/3.92  ** KEPT (pick-wt=3): 224 [copy,223,flip.1] i44!=i35.
% 3.83/3.92  ** KEPT (pick-wt=3): 226 [copy,225,flip.1] i43!=i35.
% 3.83/3.92  ** KEPT (pick-wt=3): 228 [copy,227,flip.1] i42!=i35.
% 3.83/3.92  ** KEPT (pick-wt=3): 230 [copy,229,flip.1] i41!=i35.
% 3.83/3.92  ** KEPT (pick-wt=3): 232 [copy,231,flip.1] i40!=i35.
% 3.83/3.92  ** KEPT (pick-wt=3): 234 [copy,233,flip.1] i39!=i35.
% 3.83/3.92  ** KEPT (pick-wt=3): 236 [copy,235,flip.1] i38!=i35.
% 3.83/3.92  ** KEPT (pick-wt=3): 238 [copy,237,flip.1] i37!=i35.
% 3.83/3.92  ** KEPT (pick-wt=3): 240 [copy,239,flip.1] i36!=i35.
% 3.83/3.92  ** KEPT (pick-wt=3): 242 [copy,241,flip.1] i50!=i34.
% 3.83/3.92  ** KEPT (pick-wt=3): 244 [copy,243,flip.1] i49!=i34.
% 3.83/3.92  ** KEPT (pick-wt=3): 246 [copy,245,flip.1] i48!=i34.
% 3.83/3.92  ** KEPT (pick-wt=3): 248 [copy,247,flip.1] i47!=i34.
% 3.83/3.92  ** KEPT (pick-wt=3): 250 [copy,249,flip.1] i46!=i34.
% 3.83/3.92  ** KEPT (pick-wt=3): 252 [copy,251,flip.1] i45!=i34.
% 3.83/3.92  ** KEPT (pick-wt=3): 254 [copy,253,flip.1] i44!=i34.
% 3.83/3.92  ** KEPT (pick-wt=3): 256 [copy,255,flip.1] i43!=i34.
% 3.83/3.92  ** KEPT (pick-wt=3): 258 [copy,257,flip.1] i42!=i34.
% 3.83/3.92  ** KEPT (pick-wt=3): 260 [copy,259,flip.1] i41!=i34.
% 3.83/3.92  ** KEPT (pick-wt=3): 262 [copy,261,flip.1] i40!=i34.
% 3.83/3.92  ** KEPT (pick-wt=3): 264 [copy,263,flip.1] i39!=i34.
% 3.83/3.92  ** KEPT (pick-wt=3): 266 [copy,265,flip.1] i38!=i34.
% 3.83/3.92  ** KEPT (pick-wt=3): 268 [copy,267,flip.1] i37!=i34.
% 3.83/3.92  ** KEPT (pick-wt=3): 270 [copy,269,flip.1] i36!=i34.
% 3.83/3.92  ** KEPT (pick-wt=3): 272 [copy,271,flip.1] i35!=i34.
% 3.83/3.92  ** KEPT (pick-wt=3): 274 [copy,273,flip.1] i50!=i33.
% 3.83/3.92  ** KEPT (pick-wt=3): 276 [copy,275,flip.1] i49!=i33.
% 3.83/3.92  ** KEPT (pick-wt=3): 278 [copy,277,flip.1] i48!=i33.
% 3.83/3.92  ** KEPT (pick-wt=3): 280 [copy,279,flip.1] i47!=i33.
% 3.83/3.92  ** KEPT (pick-wt=3): 282 [copy,281,flip.1] i46!=i33.
% 3.83/3.92  ** KEPT (pick-wt=3): 284 [copy,283,flip.1] i45!=i33.
% 3.83/3.92  ** KEPT (pick-wt=3): 286 [copy,285,flip.1] i44!=i33.
% 3.83/3.92  ** KEPT (pick-wt=3): 288 [copy,287,flip.1] i43!=i33.
% 3.83/3.92  ** KEPT (pick-wt=3): 290 [copy,289,flip.1] i42!=i33.
% 3.83/3.92  ** KEPT (pick-wt=3): 292 [copy,291,flip.1] i41!=i33.
% 3.83/3.92  ** KEPT (pick-wt=3): 294 [copy,293,flip.1] i40!=i33.
% 3.83/3.92  ** KEPT (pick-wt=3): 296 [copy,295,flip.1] i39!=i33.
% 3.83/3.92  ** KEPT (pick-wt=3): 298 [copy,297,flip.1] i38!=i33.
% 3.83/3.92  ** KEPT (pick-wt=3): 300 [copy,299,flip.1] i37!=i33.
% 3.83/3.92  ** KEPT (pick-wt=3): 302 [copy,301,flip.1] i36!=i33.
% 3.83/3.92  ** KEPT (pick-wt=3): 304 [copy,303,flip.1] i35!=i33.
% 3.83/3.92  ** KEPT (pick-wt=3): 306 [copy,305,flip.1] i34!=i33.
% 3.83/3.92  ** KEPT (pick-wt=3): 308 [copy,307,flip.1] i50!=i32.
% 3.83/3.92  ** KEPT (pick-wt=3): 310 [copy,309,flip.1] i49!=i32.
% 3.83/3.92  ** KEPT (pick-wt=3): 312 [copy,311,flip.1] i48!=i32.
% 3.83/3.92  ** KEPT (pick-wt=3): 314 [copy,313,flip.1] i47!=i32.
% 3.83/3.92  ** KEPT (pick-wt=3): 316 [copy,315,flip.1] i46!=i32.
% 3.83/3.92  ** KEPT (pick-wt=3): 318 [copy,317,flip.1] i45!=i32.
% 3.83/3.92  ** KEPT (pick-wt=3): 320 [copy,319,flip.1] i44!=i32.
% 3.83/3.92  ** KEPT (pick-wt=3): 322 [copy,321,flip.1] i43!=i32.
% 3.83/3.92  ** KEPT (pick-wt=3): 324 [copy,323,flip.1] i42!=i32.
% 3.83/3.92  ** KEPT (pick-wt=3): 326 [copy,325,flip.1] i41!=i32.
% 3.83/3.92  ** KEPT (pick-wt=3): 328 [copy,327,flip.1] i40!=i32.
% 3.83/3.92  ** KEPT (pick-wt=3): 330 [copy,329,flip.1] i39!=i32.
% 3.83/3.92  ** KEPT (pick-wt=3): 332 [copy,331,flip.1] i38!=i32.
% 3.83/3.92  ** KEPT (pick-wt=3): 334 [copy,333,flip.1] i37!=i32.
% 3.83/3.92  ** KEPT (pick-wt=3): 336 [copy,335,flip.1] i36!=i32.
% 3.83/3.92  ** KEPT (pick-wt=3): 338 [copy,337,flip.1] i35!=i32.
% 3.83/3.92  ** KEPT (pick-wt=3): 340 [copy,339,flip.1] i34!=i32.
% 3.83/3.92  ** KEPT (pick-wt=3): 342 [copy,341,flip.1] i33!=i32.
% 3.83/3.92  ** KEPT (pick-wt=3): 344 [copy,343,flip.1] i50!=i31.
% 3.83/3.92  ** KEPT (pick-wt=3): 346 [copy,345,flip.1] i49!=i31.
% 3.83/3.92  ** KEPT (pick-wt=3): 348 [copy,347,flip.1] i48!=i31.
% 3.83/3.92  ** KEPT (pick-wt=3): 350 [copy,349,flip.1] i47!=i31.
% 3.83/3.92  ** KEPT (pick-wt=3): 352 [copy,351,flip.1] i46!=i31.
% 3.83/3.92  ** KEPT (pick-wt=3): 354 [copy,353,flip.1] i45!=i31.
% 3.83/3.92  ** KEPT (pick-wt=3): 356 [copy,355,flip.1] i44!=i31.
% 3.83/3.92  ** KEPT (pick-wt=3): 358 [copy,357,flip.1] i43!=i31.
% 3.83/3.92  ** KEPT (pick-wt=3): 360 [copy,359,flip.1] i42!=i31.
% 3.83/3.92  ** KEPT (pick-wt=3): 362 [copy,361,flip.1] i41!=i31.
% 3.83/3.92  ** KEPT (pick-wt=3): 364 [copy,363,flip.1] i40!=i31.
% 3.83/3.92  ** KEPT (pick-wt=3): 366 [copy,365,flip.1] i39!=i31.
% 3.83/3.92  ** KEPT (pick-wt=3): 368 [copy,367,flip.1] i38!=i31.
% 3.83/3.92  ** KEPT (pick-wt=3): 370 [copy,369,flip.1] i37!=i31.
% 3.83/3.92  ** KEPT (pick-wt=3): 372 [copy,371,flip.1] i36!=i31.
% 3.83/3.92  ** KEPT (pick-wt=3): 374 [copy,373,flip.1] i35!=i31.
% 3.83/3.92  ** KEPT (pick-wt=3): 376 [copy,375,flip.1] i34!=i31.
% 3.83/3.92  ** KEPT (pick-wt=3): 378 [copy,377,flip.1] i33!=i31.
% 3.83/3.92  ** KEPT (pick-wt=3): 380 [copy,379,flip.1] i32!=i31.
% 3.83/3.92  ** KEPT (pick-wt=3): 382 [copy,381,flip.1] i50!=i30.
% 3.83/3.92  ** KEPT (pick-wt=3): 384 [copy,383,flip.1] i49!=i30.
% 3.83/3.92  ** KEPT (pick-wt=3): 386 [copy,385,flip.1] i48!=i30.
% 3.83/3.92  ** KEPT (pick-wt=3): 388 [copy,387,flip.1] i47!=i30.
% 3.83/3.92  ** KEPT (pick-wt=3): 390 [copy,389,flip.1] i46!=i30.
% 3.83/3.92  ** KEPT (pick-wt=3): 392 [copy,391,flip.1] i45!=i30.
% 3.83/3.92  ** KEPT (pick-wt=3): 394 [copy,393,flip.1] i44!=i30.
% 3.83/3.92  ** KEPT (pick-wt=3): 396 [copy,395,flip.1] i43!=i30.
% 3.83/3.92  ** KEPT (pick-wt=3): 398 [copy,397,flip.1] i42!=i30.
% 3.83/3.92  ** KEPT (pick-wt=3): 400 [copy,399,flip.1] i41!=i30.
% 3.83/3.92  ** KEPT (pick-wt=3): 402 [copy,401,flip.1] i40!=i30.
% 3.83/3.92  ** KEPT (pick-wt=3): 404 [copy,403,flip.1] i39!=i30.
% 3.83/3.92  ** KEPT (pick-wt=3): 406 [copy,405,flip.1] i38!=i30.
% 3.83/3.92  ** KEPT (pick-wt=3): 408 [copy,407,flip.1] i37!=i30.
% 3.83/3.92  ** KEPT (pick-wt=3): 410 [copy,409,flip.1] i36!=i30.
% 3.83/3.92  ** KEPT (pick-wt=3): 412 [copy,411,flip.1] i35!=i30.
% 3.83/3.92  ** KEPT (pick-wt=3): 414 [copy,413,flip.1] i34!=i30.
% 3.83/3.92  ** KEPT (pick-wt=3): 416 [copy,415,flip.1] i33!=i30.
% 3.83/3.92  ** KEPT (pick-wt=3): 418 [copy,417,flip.1] i32!=i30.
% 3.83/3.92  ** KEPT (pick-wt=3): 420 [copy,419,flip.1] i31!=i30.
% 3.83/3.92  ** KEPT (pick-wt=3): 422 [copy,421,flip.1] i50!=i29.
% 3.83/3.92  ** KEPT (pick-wt=3): 424 [copy,423,flip.1] i49!=i29.
% 3.83/3.92  ** KEPT (pick-wt=3): 426 [copy,425,flip.1] i48!=i29.
% 3.83/3.92  ** KEPT (pick-wt=3): 428 [copy,427,flip.1] i47!=i29.
% 3.83/3.92  ** KEPT (pick-wt=3): 430 [copy,429,flip.1] i46!=i29.
% 3.83/3.92  ** KEPT (pick-wt=3): 432 [copy,431,flip.1] i45!=i29.
% 3.83/3.92  ** KEPT (pick-wt=3): 434 [copy,433,flip.1] i44!=i29.
% 3.83/3.92  ** KEPT (pick-wt=3): 436 [copy,435,flip.1] i43!=i29.
% 3.83/3.92  ** KEPT (pick-wt=3): 438 [copy,437,flip.1] i42!=i29.
% 3.83/3.92  ** KEPT (pick-wt=3): 440 [copy,439,flip.1] i41!=i29.
% 3.83/3.92  ** KEPT (pick-wt=3): 442 [copy,441,flip.1] i40!=i29.
% 3.83/3.92  ** KEPT (pick-wt=3): 444 [copy,443,flip.1] i39!=i29.
% 3.83/3.92  ** KEPT (pick-wt=3): 446 [copy,445,flip.1] i38!=i29.
% 3.83/3.92  ** KEPT (pick-wt=3): 448 [copy,447,flip.1] i37!=i29.
% 3.83/3.92  ** KEPT (pick-wt=3): 450 [copy,449,flip.1] i36!=i29.
% 3.83/3.92  ** KEPT (pick-wt=3): 452 [copy,451,flip.1] i35!=i29.
% 3.83/3.92  ** KEPT (pick-wt=3): 454 [copy,453,flip.1] i34!=i29.
% 3.83/3.92  ** KEPT (pick-wt=3): 456 [copy,455,flip.1] i33!=i29.
% 3.83/3.92  ** KEPT (pick-wt=3): 458 [copy,457,flip.1] i32!=i29.
% 3.83/3.92  ** KEPT (pick-wt=3): 460 [copy,459,flip.1] i31!=i29.
% 3.83/3.92  ** KEPT (pick-wt=3): 462 [copy,461,flip.1] i30!=i29.
% 3.83/3.92  ** KEPT (pick-wt=3): 464 [copy,463,flip.1] i50!=i28.
% 3.83/3.92  ** KEPT (pick-wt=3): 466 [copy,465,flip.1] i49!=i28.
% 3.83/3.92  ** KEPT (pick-wt=3): 468 [copy,467,flip.1] i48!=i28.
% 3.83/3.92  ** KEPT (pick-wt=3): 470 [copy,469,flip.1] i47!=i28.
% 3.83/3.92  ** KEPT (pick-wt=3): 472 [copy,471,flip.1] i46!=i28.
% 3.83/3.92  ** KEPT (pick-wt=3): 474 [copy,473,flip.1] i45!=i28.
% 3.83/3.92  ** KEPT (pick-wt=3): 476 [copy,475,flip.1] i44!=i28.
% 3.83/3.92  ** KEPT (pick-wt=3): 478 [copy,477,flip.1] i43!=i28.
% 3.83/3.92  ** KEPT (pick-wt=3): 480 [copy,479,flip.1] i42!=i28.
% 3.83/3.92  ** KEPT (pick-wt=3): 482 [copy,481,flip.1] i41!=i28.
% 3.83/3.92  ** KEPT (pick-wt=3): 484 [copy,483,flip.1] i40!=i28.
% 3.83/3.92  ** KEPT (pick-wt=3): 486 [copy,485,flip.1] i39!=i28.
% 3.83/3.92  ** KEPT (pick-wt=3): 488 [copy,487,flip.1] i38!=i28.
% 3.83/3.92  ** KEPT (pick-wt=3): 490 [copy,489,flip.1] i37!=i28.
% 3.83/3.92  ** KEPT (pick-wt=3): 492 [copy,491,flip.1] i36!=i28.
% 3.83/3.92  ** KEPT (pick-wt=3): 494 [copy,493,flip.1] i35!=i28.
% 3.83/3.92  ** KEPT (pick-wt=3): 496 [copy,495,flip.1] i34!=i28.
% 3.83/3.92  ** KEPT (pick-wt=3): 498 [copy,497,flip.1] i33!=i28.
% 3.83/3.92  ** KEPT (pick-wt=3): 500 [copy,499,flip.1] i32!=i28.
% 3.83/3.92  ** KEPT (pick-wt=3): 502 [copy,501,flip.1] i31!=i28.
% 3.83/3.92  ** KEPT (pick-wt=3): 504 [copy,503,flip.1] i30!=i28.
% 3.83/3.92  ** KEPT (pick-wt=3): 506 [copy,505,flip.1] i29!=i28.
% 3.83/3.92  ** KEPT (pick-wt=3): 508 [copy,507,flip.1] i50!=i27.
% 3.83/3.92  ** KEPT (pick-wt=3): 510 [copy,509,flip.1] i49!=i27.
% 3.83/3.92  ** KEPT (pick-wt=3): 512 [copy,511,flip.1] i48!=i27.
% 3.83/3.92  ** KEPT (pick-wt=3): 514 [copy,513,flip.1] i47!=i27.
% 3.83/3.92  ** KEPT (pick-wt=3): 516 [copy,515,flip.1] i46!=i27.
% 3.83/3.92  ** KEPT (pick-wt=3): 518 [copy,517,flip.1] i45!=i27.
% 3.83/3.92  ** KEPT (pick-wt=3): 520 [copy,519,flip.1] i44!=i27.
% 3.83/3.92  ** KEPT (pick-wt=3): 522 [copy,521,flip.1] i43!=i27.
% 3.83/3.92  ** KEPT (pick-wt=3): 524 [copy,523,flip.1] i42!=i27.
% 3.83/3.92  ** KEPT (pick-wt=3): 526 [copy,525,flip.1] i41!=i27.
% 3.83/3.92  ** KEPT (pick-wt=3): 528 [copy,527,flip.1] i40!=i27.
% 3.83/3.92  ** KEPT (pick-wt=3): 530 [copy,529,flip.1] i39!=i27.
% 3.83/3.92  ** KEPT (pick-wt=3): 532 [copy,531,flip.1] i38!=i27.
% 3.83/3.92  ** KEPT (pick-wt=3): 534 [copy,533,flip.1] i37!=i27.
% 3.83/3.92  ** KEPT (pick-wt=3): 536 [copy,535,flip.1] i36!=i27.
% 3.83/3.92  ** KEPT (pick-wt=3): 538 [copy,537,flip.1] i35!=i27.
% 3.83/3.92  ** KEPT (pick-wt=3): 540 [copy,539,flip.1] i34!=i27.
% 3.83/3.92  ** KEPT (pick-wt=3): 542 [copy,541,flip.1] i33!=i27.
% 3.83/3.92  ** KEPT (pick-wt=3): 544 [copy,543,flip.1] i32!=i27.
% 3.83/3.92  ** KEPT (pick-wt=3): 546 [copy,545,flip.1] i31!=i27.
% 3.83/3.92  ** KEPT (pick-wt=3): 548 [copy,547,flip.1] i30!=i27.
% 3.83/3.92  ** KEPT (pick-wt=3): 550 [copy,549,flip.1] i29!=i27.
% 3.83/3.92  ** KEPT (pick-wt=3): 552 [copy,551,flip.1] i28!=i27.
% 3.83/3.92  ** KEPT (pick-wt=3): 554 [copy,553,flip.1] i50!=i26.
% 3.83/3.92  ** KEPT (pick-wt=3): 556 [copy,555,flip.1] i49!=i26.
% 3.83/3.92  ** KEPT (pick-wt=3): 558 [copy,557,flip.1] i48!=i26.
% 3.83/3.92  ** KEPT (pick-wt=3): 560 [copy,559,flip.1] i47!=i26.
% 3.83/3.92  ** KEPT (pick-wt=3): 562 [copy,561,flip.1] i46!=i26.
% 3.83/3.92  ** KEPT (pick-wt=3): 564 [copy,563,flip.1] i45!=i26.
% 3.83/3.92  ** KEPT (pick-wt=3): 566 [copy,565,flip.1] i44!=i26.
% 3.83/3.92  ** KEPT (pick-wt=3): 568 [copy,567,flip.1] i43!=i26.
% 3.83/3.92  ** KEPT (pick-wt=3): 570 [copy,569,flip.1] i42!=i26.
% 3.83/3.92  ** KEPT (pick-wt=3): 572 [copy,571,flip.1] i41!=i26.
% 3.83/3.92  ** KEPT (pick-wt=3): 574 [copy,573,flip.1] i40!=i26.
% 3.83/3.92  ** KEPT (pick-wt=3): 576 [copy,575,flip.1] i39!=i26.
% 3.83/3.92  ** KEPT (pick-wt=3): 578 [copy,577,flip.1] i38!=i26.
% 3.83/3.92  ** KEPT (pick-wt=3): 580 [copy,579,flip.1] i37!=i26.
% 3.83/3.92  ** KEPT (pick-wt=3): 582 [copy,581,flip.1] i36!=i26.
% 3.83/3.92  ** KEPT (pick-wt=3): 584 [copy,583,flip.1] i35!=i26.
% 3.83/3.92  ** KEPT (pick-wt=3): 586 [copy,585,flip.1] i34!=i26.
% 3.83/3.92  ** KEPT (pick-wt=3): 588 [copy,587,flip.1] i33!=i26.
% 3.83/3.92  ** KEPT (pick-wt=3): 590 [copy,589,flip.1] i32!=i26.
% 3.83/3.92  ** KEPT (pick-wt=3): 592 [copy,591,flip.1] i31!=i26.
% 3.83/3.92  ** KEPT (pick-wt=3): 594 [copy,593,flip.1] i30!=i26.
% 3.83/3.92  ** KEPT (pick-wt=3): 596 [copy,595,flip.1] i29!=i26.
% 3.83/3.92  ** KEPT (pick-wt=3): 598 [copy,597,flip.1] i28!=i26.
% 3.83/3.92  ** KEPT (pick-wt=3): 600 [copy,599,flip.1] i27!=i26.
% 3.83/3.92  ** KEPT (pick-wt=3): 602 [copy,601,flip.1] i50!=i25.
% 3.83/3.92  ** KEPT (pick-wt=3): 604 [copy,603,flip.1] i49!=i25.
% 3.83/3.92  ** KEPT (pick-wt=3): 606 [copy,605,flip.1] i48!=i25.
% 3.83/3.92  ** KEPT (pick-wt=3): 608 [copy,607,flip.1] i47!=i25.
% 3.83/3.92  ** KEPT (pick-wt=3): 610 [copy,609,flip.1] i46!=i25.
% 3.83/3.92  ** KEPT (pick-wt=3): 612 [copy,611,flip.1] i45!=i25.
% 3.83/3.92  ** KEPT (pick-wt=3): 614 [copy,613,flip.1] i44!=i25.
% 3.83/3.92  ** KEPT (pick-wt=3): 616 [copy,615,flip.1] i43!=i25.
% 3.83/3.92  ** KEPT (pick-wt=3): 618 [copy,617,flip.1] i42!=i25.
% 3.83/3.92  ** KEPT (pick-wt=3): 620 [copy,619,flip.1] i41!=i25.
% 3.83/3.92  ** KEPT (pick-wt=3): 622 [copy,621,flip.1] i40!=i25.
% 3.83/3.92  ** KEPT (pick-wt=3): 624 [copy,623,flip.1] i39!=i25.
% 3.83/3.92  ** KEPT (pick-wt=3): 626 [copy,625,flip.1] i38!=i25.
% 3.83/3.92  ** KEPT (pick-wt=3): 628 [copy,627,flip.1] i37!=i25.
% 3.83/3.92  ** KEPT (pick-wt=3): 630 [copy,629,flip.1] i36!=i25.
% 3.83/3.92  ** KEPT (pick-wt=3): 632 [copy,631,flip.1] i35!=i25.
% 3.83/3.92  ** KEPT (pick-wt=3): 634 [copy,633,flip.1] i34!=i25.
% 3.83/3.92  ** KEPT (pick-wt=3): 636 [copy,635,flip.1] i33!=i25.
% 3.83/3.92  ** KEPT (pick-wt=3): 638 [copy,637,flip.1] i32!=i25.
% 3.83/3.92  ** KEPT (pick-wt=3): 640 [copy,639,flip.1] i31!=i25.
% 3.83/3.92  ** KEPT (pick-wt=3): 642 [copy,641,flip.1] i30!=i25.
% 3.83/3.92  ** KEPT (pick-wt=3): 644 [copy,643,flip.1] i29!=i25.
% 3.83/3.92  ** KEPT (pick-wt=3): 646 [copy,645,flip.1] i28!=i25.
% 3.83/3.92  ** KEPT (pick-wt=3): 648 [copy,647,flip.1] i27!=i25.
% 3.83/3.92  ** KEPT (pick-wt=3): 650 [copy,649,flip.1] i26!=i25.
% 3.83/3.92  ** KEPT (pick-wt=3): 652 [copy,651,flip.1] i50!=i24.
% 3.83/3.92  ** KEPT (pick-wt=3): 654 [copy,653,flip.1] i49!=i24.
% 3.83/3.92  ** KEPT (pick-wt=3): 656 [copy,655,flip.1] i48!=i24.
% 3.83/3.92  ** KEPT (pick-wt=3): 658 [copy,657,flip.1] i47!=i24.
% 3.83/3.92  ** KEPT (pick-wt=3): 660 [copy,659,flip.1] i46!=i24.
% 3.83/3.92  ** KEPT (pick-wt=3): 662 [copy,661,flip.1] i45!=i24.
% 3.83/3.92  ** KEPT (pick-wt=3): 664 [copy,663,flip.1] i44!=i24.
% 3.83/3.92  ** KEPT (pick-wt=3): 666 [copy,665,flip.1] i43!=i24.
% 3.83/3.92  ** KEPT (pick-wt=3): 668 [copy,667,flip.1] i42!=i24.
% 3.83/3.92  ** KEPT (pick-wt=3): 670 [copy,669,flip.1] i41!=i24.
% 3.83/3.92  ** KEPT (pick-wt=3): 672 [copy,671,flip.1] i40!=i24.
% 3.83/3.92  ** KEPT (pick-wt=3): 674 [copy,673,flip.1] i39!=i24.
% 3.83/3.92  ** KEPT (pick-wt=3): 676 [copy,675,flip.1] i38!=i24.
% 3.83/3.92  ** KEPT (pick-wt=3): 678 [copy,677,flip.1] i37!=i24.
% 3.83/3.92  ** KEPT (pick-wt=3): 680 [copy,679,flip.1] i36!=i24.
% 3.83/3.92  ** KEPT (pick-wt=3): 682 [copy,681,flip.1] i35!=i24.
% 3.83/3.92  ** KEPT (pick-wt=3): 684 [copy,683,flip.1] i34!=i24.
% 3.83/3.92  ** KEPT (pick-wt=3): 686 [copy,685,flip.1] i33!=i24.
% 3.83/3.92  ** KEPT (pick-wt=3): 688 [copy,687,flip.1] i32!=i24.
% 3.83/3.92  ** KEPT (pick-wt=3): 690 [copy,689,flip.1] i31!=i24.
% 3.83/3.92  ** KEPT (pick-wt=3): 692 [copy,691,flip.1] i30!=i24.
% 3.83/3.92  ** KEPT (pick-wt=3): 694 [copy,693,flip.1] i29!=i24.
% 3.83/3.92  ** KEPT (pick-wt=3): 696 [copy,695,flip.1] i28!=i24.
% 3.83/3.92  ** KEPT (pick-wt=3): 698 [copy,697,flip.1] i27!=i24.
% 3.83/3.92  ** KEPT (pick-wt=3): 700 [copy,699,flip.1] i26!=i24.
% 3.83/3.92  ** KEPT (pick-wt=3): 702 [copy,701,flip.1] i25!=i24.
% 3.83/3.92  ** KEPT (pick-wt=3): 704 [copy,703,flip.1] i50!=i23.
% 3.83/3.92  ** KEPT (pick-wt=3): 706 [copy,705,flip.1] i49!=i23.
% 3.83/3.92  ** KEPT (pick-wt=3): 708 [copy,707,flip.1] i48!=i23.
% 3.83/3.92  ** KEPT (pick-wt=3): 710 [copy,709,flip.1] i47!=i23.
% 3.83/3.92  ** KEPT (pick-wt=3): 712 [copy,711,flip.1] i46!=i23.
% 3.83/3.92  ** KEPT (pick-wt=3): 714 [copy,713,flip.1] i45!=i23.
% 3.83/3.92  ** KEPT (pick-wt=3): 716 [copy,715,flip.1] i44!=i23.
% 3.83/3.92  ** KEPT (pick-wt=3): 718 [copy,717,flip.1] i43!=i23.
% 3.83/3.92  ** KEPT (pick-wt=3): 720 [copy,719,flip.1] i42!=i23.
% 3.83/3.92  ** KEPT (pick-wt=3): 722 [copy,721,flip.1] i41!=i23.
% 3.83/3.92  ** KEPT (pick-wt=3): 724 [copy,723,flip.1] i40!=i23.
% 3.83/3.92  ** KEPT (pick-wt=3): 726 [copy,725,flip.1] i39!=i23.
% 3.83/3.92  ** KEPT (pick-wt=3): 728 [copy,727,flip.1] i38!=i23.
% 3.83/3.92  ** KEPT (pick-wt=3): 730 [copy,729,flip.1] i37!=i23.
% 3.83/3.92  ** KEPT (pick-wt=3): 732 [copy,731,flip.1] i36!=i23.
% 3.83/3.92  ** KEPT (pick-wt=3): 734 [copy,733,flip.1] i35!=i23.
% 3.83/3.92  ** KEPT (pick-wt=3): 736 [copy,735,flip.1] i34!=i23.
% 3.83/3.92  ** KEPT (pick-wt=3): 738 [copy,737,flip.1] i33!=i23.
% 3.83/3.92  ** KEPT (pick-wt=3): 740 [copy,739,flip.1] i32!=i23.
% 3.83/3.92  ** KEPT (pick-wt=3): 742 [copy,741,flip.1] i31!=i23.
% 3.83/3.92  ** KEPT (pick-wt=3): 744 [copy,743,flip.1] i30!=i23.
% 3.83/3.92  ** KEPT (pick-wt=3): 746 [copy,745,flip.1] i29!=i23.
% 3.83/3.92  ** KEPT (pick-wt=3): 748 [copy,747,flip.1] i28!=i23.
% 3.83/3.92  ** KEPT (pick-wt=3): 750 [copy,749,flip.1] i27!=i23.
% 3.83/3.92  ** KEPT (pick-wt=3): 752 [copy,751,flip.1] i26!=i23.
% 3.83/3.92  ** KEPT (pick-wt=3): 754 [copy,753,flip.1] i25!=i23.
% 3.83/3.92  ** KEPT (pick-wt=3): 756 [copy,755,flip.1] i24!=i23.
% 3.83/3.92  ** KEPT (pick-wt=3): 758 [copy,757,flip.1] i50!=i22.
% 3.83/3.92  ** KEPT (pick-wt=3): 760 [copy,759,flip.1] i49!=i22.
% 3.83/3.92  ** KEPT (pick-wt=3): 762 [copy,761,flip.1] i48!=i22.
% 3.83/3.92  ** KEPT (pick-wt=3): 764 [copy,763,flip.1] i47!=i22.
% 3.83/3.92  ** KEPT (pick-wt=3): 766 [copy,765,flip.1] i46!=i22.
% 3.83/3.92  ** KEPT (pick-wt=3): 768 [copy,767,flip.1] i45!=i22.
% 3.83/3.92  ** KEPT (pick-wt=3): 770 [copy,769,flip.1] i44!=i22.
% 3.83/3.92  ** KEPT (pick-wt=3): 772 [copy,771,flip.1] i43!=i22.
% 3.83/3.92  ** KEPT (pick-wt=3): 774 [copy,773,flip.1] i42!=i22.
% 3.83/3.92  ** KEPT (pick-wt=3): 776 [copy,775,flip.1] i41!=i22.
% 3.83/3.92  ** KEPT (pick-wt=3): 778 [copy,777,flip.1] i40!=i22.
% 3.83/3.92  ** KEPT (pick-wt=3): 780 [copy,779,flip.1] i39!=i22.
% 3.83/3.92  ** KEPT (pick-wt=3): 782 [copy,781,flip.1] i38!=i22.
% 3.83/3.92  ** KEPT (pick-wt=3): 784 [copy,783,flip.1] i37!=i22.
% 3.83/3.92  ** KEPT (pick-wt=3): 786 [copy,785,flip.1] i36!=i22.
% 3.83/3.92  ** KEPT (pick-wt=3): 788 [copy,787,flip.1] i35!=i22.
% 3.83/3.92  ** KEPT (pick-wt=3): 790 [copy,789,flip.1] i34!=i22.
% 3.83/3.92  ** KEPT (pick-wt=3): 792 [copy,791,flip.1] i33!=i22.
% 3.83/3.92  ** KEPT (pick-wt=3): 794 [copy,793,flip.1] i32!=i22.
% 3.83/3.92  ** KEPT (pick-wt=3): 796 [copy,795,flip.1] i31!=i22.
% 3.83/3.92  ** KEPT (pick-wt=3): 798 [copy,797,flip.1] i30!=i22.
% 3.83/3.92  ** KEPT (pick-wt=3): 800 [copy,799,flip.1] i29!=i22.
% 3.83/3.92  ** KEPT (pick-wt=3): 802 [copy,801,flip.1] i28!=i22.
% 3.83/3.92  ** KEPT (pick-wt=3): 804 [copy,803,flip.1] i27!=i22.
% 3.83/3.92  ** KEPT (pick-wt=3): 806 [copy,805,flip.1] i26!=i22.
% 3.83/3.92  ** KEPT (pick-wt=3): 808 [copy,807,flip.1] i25!=i22.
% 3.83/3.92  ** KEPT (pick-wt=3): 810 [copy,809,flip.1] i24!=i22.
% 3.83/3.92  ** KEPT (pick-wt=3): 812 [copy,811,flip.1] i23!=i22.
% 3.83/3.92  ** KEPT (pick-wt=3): 814 [copy,813,flip.1] i50!=i21.
% 3.83/3.92  ** KEPT (pick-wt=3): 816 [copy,815,flip.1] i49!=i21.
% 3.83/3.92  ** KEPT (pick-wt=3): 818 [copy,817,flip.1] i48!=i21.
% 3.83/3.92  ** KEPT (pick-wt=3): 820 [copy,819,flip.1] i47!=i21.
% 3.83/3.92  ** KEPT (pick-wt=3): 822 [copy,821,flip.1] i46!=i21.
% 3.83/3.92  ** KEPT (pick-wt=3): 824 [copy,823,flip.1] i45!=i21.
% 3.83/3.92  ** KEPT (pick-wt=3): 826 [copy,825,flip.1] i44!=i21.
% 3.83/3.92  ** KEPT (pick-wt=3): 828 [copy,827,flip.1] i43!=i21.
% 3.83/3.92  ** KEPT (pick-wt=3): 830 [copy,829,flip.1] i42!=i21.
% 3.83/3.92  ** KEPT (pick-wt=3): 832 [copy,831,flip.1] i41!=i21.
% 3.83/3.92  ** KEPT (pick-wt=3): 834 [copy,833,flip.1] i40!=i21.
% 3.83/3.92  ** KEPT (pick-wt=3): 836 [copy,835,flip.1] i39!=i21.
% 3.83/3.92  ** KEPT (pick-wt=3): 838 [copy,837,flip.1] i38!=i21.
% 3.83/3.92  ** KEPT (pick-wt=3): 840 [copy,839,flip.1] i37!=i21.
% 3.83/3.92  ** KEPT (pick-wt=3): 842 [copy,841,flip.1] i36!=i21.
% 3.83/3.92  ** KEPT (pick-wt=3): 844 [copy,843,flip.1] i35!=i21.
% 3.83/3.92  ** KEPT (pick-wt=3): 846 [copy,845,flip.1] i34!=i21.
% 3.83/3.92  ** KEPT (pick-wt=3): 848 [copy,847,flip.1] i33!=i21.
% 3.83/3.92  ** KEPT (pick-wt=3): 850 [copy,849,flip.1] i32!=i21.
% 3.83/3.92  ** KEPT (pick-wt=3): 852 [copy,851,flip.1] i31!=i21.
% 3.83/3.92  ** KEPT (pick-wt=3): 854 [copy,853,flip.1] i30!=i21.
% 3.83/3.92  ** KEPT (pick-wt=3): 856 [copy,855,flip.1] i29!=i21.
% 3.83/3.92  ** KEPT (pick-wt=3): 858 [copy,857,flip.1] i28!=i21.
% 3.83/3.92  ** KEPT (pick-wt=3): 860 [copy,859,flip.1] i27!=i21.
% 3.83/3.92  ** KEPT (pick-wt=3): 862 [copy,861,flip.1] i26!=i21.
% 3.83/3.92  ** KEPT (pick-wt=3): 864 [copy,863,flip.1] i25!=i21.
% 3.83/3.92  ** KEPT (pick-wt=3): 866 [copy,865,flip.1] i24!=i21.
% 3.83/3.92  ** KEPT (pick-wt=3): 868 [copy,867,flip.1] i23!=i21.
% 3.83/3.92  ** KEPT (pick-wt=3): 870 [copy,869,flip.1] i22!=i21.
% 3.83/3.92  ** KEPT (pick-wt=3): 872 [copy,871,flip.1] i50!=i20.
% 3.83/3.92  ** KEPT (pick-wt=3): 874 [copy,873,flip.1] i49!=i20.
% 3.83/3.92  ** KEPT (pick-wt=3): 876 [copy,875,flip.1] i48!=i20.
% 3.83/3.92  ** KEPT (pick-wt=3): 878 [copy,877,flip.1] i47!=i20.
% 3.83/3.92  ** KEPT (pick-wt=3): 880 [copy,879,flip.1] i46!=i20.
% 3.83/3.92  ** KEPT (pick-wt=3): 882 [copy,881,flip.1] i45!=i20.
% 3.83/3.92  ** KEPT (pick-wt=3): 884 [copy,883,flip.1] i44!=i20.
% 3.83/3.92  ** KEPT (pick-wt=3): 886 [copy,885,flip.1] i43!=i20.
% 3.83/3.92  ** KEPT (pick-wt=3): 888 [copy,887,flip.1] i42!=i20.
% 3.83/3.92  ** KEPT (pick-wt=3): 890 [copy,889,flip.1] i41!=i20.
% 3.83/3.92  ** KEPT (pick-wt=3): 892 [copy,891,flip.1] i40!=i20.
% 3.83/3.92  ** KEPT (pick-wt=3): 894 [copy,893,flip.1] i39!=i20.
% 3.83/3.92  ** KEPT (pick-wt=3): 896 [copy,895,flip.1] i38!=i20.
% 3.83/3.92  ** KEPT (pick-wt=3): 898 [copy,897,flip.1] i37!=i20.
% 3.83/3.92  ** KEPT (pick-wt=3): 900 [copy,899,flip.1] i36!=i20.
% 3.83/3.92  ** KEPT (pick-wt=3): 902 [copy,901,flip.1] i35!=i20.
% 3.83/3.92  ** KEPT (pick-wt=3): 904 [copy,903,flip.1] i34!=i20.
% 3.83/3.92  ** KEPT (pick-wt=3): 906 [copy,905,flip.1] i33!=i20.
% 3.83/3.92  ** KEPT (pick-wt=3): 908 [copy,907,flip.1] i32!=i20.
% 3.83/3.92  ** KEPT (pick-wt=3): 910 [copy,909,flip.1] i31!=i20.
% 3.83/3.92  ** KEPT (pick-wt=3): 912 [copy,911,flip.1] i30!=i20.
% 3.83/3.92  ** KEPT (pick-wt=3): 914 [copy,913,flip.1] i29!=i20.
% 3.83/3.92  ** KEPT (pick-wt=3): 916 [copy,915,flip.1] i28!=i20.
% 3.83/3.92  ** KEPT (pick-wt=3): 918 [copy,917,flip.1] i27!=i20.
% 3.83/3.92  ** KEPT (pick-wt=3): 920 [copy,919,flip.1] i26!=i20.
% 3.83/3.92  ** KEPT (pick-wt=3): 922 [copy,921,flip.1] i25!=i20.
% 3.83/3.92  ** KEPT (pick-wt=3): 924 [copy,923,flip.1] i24!=i20.
% 3.83/3.92  ** KEPT (pick-wt=3): 926 [copy,925,flip.1] i23!=i20.
% 3.83/3.92  ** KEPT (pick-wt=3): 928 [copy,927,flip.1] i22!=i20.
% 3.83/3.92  ** KEPT (pick-wt=3): 930 [copy,929,flip.1] i21!=i20.
% 3.83/3.92  ** KEPT (pick-wt=3): 932 [copy,931,flip.1] i50!=i19.
% 3.83/3.92  ** KEPT (pick-wt=3): 934 [copy,933,flip.1] i49!=i19.
% 3.83/3.92  ** KEPT (pick-wt=3): 936 [copy,935,flip.1] i48!=i19.
% 3.83/3.92  ** KEPT (pick-wt=3): 938 [copy,937,flip.1] i47!=i19.
% 3.83/3.92  ** KEPT (pick-wt=3): 940 [copy,939,flip.1] i46!=i19.
% 3.83/3.92  ** KEPT (pick-wt=3): 942 [copy,941,flip.1] i45!=i19.
% 3.83/3.92  ** KEPT (pick-wt=3): 944 [copy,943,flip.1] i44!=i19.
% 3.83/3.92  ** KEPT (pick-wt=3): 946 [copy,945,flip.1] i43!=i19.
% 3.83/3.92  ** KEPT (pick-wt=3): 948 [copy,947,flip.1] i42!=i19.
% 3.83/3.92  ** KEPT (pick-wt=3): 950 [copy,949,flip.1] i41!=i19.
% 3.83/3.92  ** KEPT (pick-wt=3): 952 [copy,951,flip.1] i40!=i19.
% 3.83/3.92  ** KEPT (pick-wt=3): 954 [copy,953,flip.1] i39!=i19.
% 3.83/3.92  ** KEPT (pick-wt=3): 956 [copy,955,flip.1] i38!=i19.
% 3.83/3.92  ** KEPT (pick-wt=3): 958 [copy,957,flip.1] i37!=i19.
% 3.83/3.92  ** KEPT (pick-wt=3): 960 [copy,959,flip.1] i36!=i19.
% 3.83/3.92  ** KEPT (pick-wt=3): 962 [copy,961,flip.1] i35!=i19.
% 3.83/3.92  ** KEPT (pick-wt=3): 964 [copy,963,flip.1] i34!=i19.
% 3.83/3.92  ** KEPT (pick-wt=3): 966 [copy,965,flip.1] i33!=i19.
% 3.83/3.92  ** KEPT (pick-wt=3): 968 [copy,967,flip.1] i32!=i19.
% 3.83/3.92  ** KEPT (pick-wt=3): 970 [copy,969,flip.1] i31!=i19.
% 3.83/3.92  ** KEPT (pick-wt=3): 972 [copy,971,flip.1] i30!=i19.
% 3.83/3.92  ** KEPT (pick-wt=3): 974 [copy,973,flip.1] i29!=i19.
% 3.83/3.92  ** KEPT (pick-wt=3): 976 [copy,975,flip.1] i28!=i19.
% 3.83/3.92  ** KEPT (pick-wt=3): 978 [copy,977,flip.1] i27!=i19.
% 3.83/3.92  ** KEPT (pick-wt=3): 980 [copy,979,flip.1] i26!=i19.
% 3.83/3.92  ** KEPT (pick-wt=3): 982 [copy,981,flip.1] i25!=i19.
% 3.83/3.92  ** KEPT (pick-wt=3): 984 [copy,983,flip.1] i24!=i19.
% 3.83/3.92  ** KEPT (pick-wt=3): 986 [copy,985,flip.1] i23!=i19.
% 3.83/3.92  ** KEPT (pick-wt=3): 988 [copy,987,flip.1] i22!=i19.
% 3.83/3.92  ** KEPT (pick-wt=3): 990 [copy,989,flip.1] i21!=i19.
% 3.83/3.92  ** KEPT (pick-wt=3): 992 [copy,991,flip.1] i20!=i19.
% 3.83/3.92  ** KEPT (pick-wt=3): 994 [copy,993,flip.1] i50!=i18.
% 3.83/3.92  ** KEPT (pick-wt=3): 996 [copy,995,flip.1] i49!=i18.
% 3.83/3.92  ** KEPT (pick-wt=3): 998 [copy,997,flip.1] i48!=i18.
% 3.83/3.92  ** KEPT (pick-wt=3): 1000 [copy,999,flip.1] i47!=i18.
% 3.83/3.92  ** KEPT (pick-wt=3): 1002 [copy,1001,flip.1] i46!=i18.
% 3.83/3.92  ** KEPT (pick-wt=3): 1004 [copy,1003,flip.1] i45!=i18.
% 3.83/3.92  ** KEPT (pick-wt=3): 1006 [copy,1005,flip.1] i44!=i18.
% 3.83/3.92  ** KEPT (pick-wt=3): 1008 [copy,1007,flip.1] i43!=i18.
% 3.83/3.92  ** KEPT (pick-wt=3): 1010 [copy,1009,flip.1] i42!=i18.
% 3.83/3.92  ** KEPT (pick-wt=3): 1012 [copy,1011,flip.1] i41!=i18.
% 3.83/3.92  ** KEPT (pick-wt=3): 1014 [copy,1013,flip.1] i40!=i18.
% 3.83/3.92  ** KEPT (pick-wt=3): 1016 [copy,1015,flip.1] i39!=i18.
% 3.83/3.92  ** KEPT (pick-wt=3): 1018 [copy,1017,flip.1] i38!=i18.
% 3.83/3.92  ** KEPT (pick-wt=3): 1020 [copy,1019,flip.1] i37!=i18.
% 3.83/3.92  ** KEPT (pick-wt=3): 1022 [copy,1021,flip.1] i36!=i18.
% 3.83/3.92  ** KEPT (pick-wt=3): 1024 [copy,1023,flip.1] i35!=i18.
% 3.83/3.92  ** KEPT (pick-wt=3): 1026 [copy,1025,flip.1] i34!=i18.
% 3.83/3.92  ** KEPT (pick-wt=3): 1028 [copy,1027,flip.1] i33!=i18.
% 3.83/3.92  ** KEPT (pick-wt=3): 1030 [copy,1029,flip.1] i32!=i18.
% 3.83/3.92  ** KEPT (pick-wt=3): 1032 [copy,1031,flip.1] i31!=i18.
% 3.83/3.92  ** KEPT (pick-wt=3): 1034 [copy,1033,flip.1] i30!=i18.
% 3.83/3.92  ** KEPT (pick-wt=3): 1036 [copy,1035,flip.1] i29!=i18.
% 3.83/3.92  ** KEPT (pick-wt=3): 1038 [copy,1037,flip.1] i28!=i18.
% 3.83/3.92  ** KEPT (pick-wt=3): 1040 [copy,1039,flip.1] i27!=i18.
% 3.83/3.92  ** KEPT (pick-wt=3): 1042 [copy,1041,flip.1] i26!=i18.
% 3.83/3.92  ** KEPT (pick-wt=3): 1044 [copy,1043,flip.1] i25!=i18.
% 3.83/3.92  ** KEPT (pick-wt=3): 1046 [copy,1045,flip.1] i24!=i18.
% 3.83/3.92  ** KEPT (pick-wt=3): 1048 [copy,1047,flip.1] i23!=i18.
% 3.83/3.92  ** KEPT (pick-wt=3): 1050 [copy,1049,flip.1] i22!=i18.
% 3.83/3.92  ** KEPT (pick-wt=3): 1052 [copy,1051,flip.1] i21!=i18.
% 3.83/3.92  ** KEPT (pick-wt=3): 1054 [copy,1053,flip.1] i20!=i18.
% 3.83/3.92  ** KEPT (pick-wt=3): 1056 [copy,1055,flip.1] i19!=i18.
% 3.83/3.92  ** KEPT (pick-wt=3): 1058 [copy,1057,flip.1] i50!=i17.
% 3.83/3.92  ** KEPT (pick-wt=3): 1060 [copy,1059,flip.1] i49!=i17.
% 3.83/3.92  ** KEPT (pick-wt=3): 1062 [copy,1061,flip.1] i48!=i17.
% 3.83/3.92  ** KEPT (pick-wt=3): 1064 [copy,1063,flip.1] i47!=i17.
% 3.83/3.92  ** KEPT (pick-wt=3): 1066 [copy,1065,flip.1] i46!=i17.
% 3.83/3.92  ** KEPT (pick-wt=3): 1068 [copy,1067,flip.1] i45!=i17.
% 3.83/3.92  ** KEPT (pick-wt=3): 1070 [copy,1069,flip.1] i44!=i17.
% 3.83/3.92  ** KEPT (pick-wt=3): 1072 [copy,1071,flip.1] i43!=i17.
% 3.83/3.92  ** KEPT (pick-wt=3): 1074 [copy,1073,flip.1] i42!=i17.
% 3.83/3.92  ** KEPT (pick-wt=3): 1076 [copy,1075,flip.1] i41!=i17.
% 3.83/3.92  ** KEPT (pick-wt=3): 1078 [copy,1077,flip.1] i40!=i17.
% 3.83/3.92  ** KEPT (pick-wt=3): 1080 [copy,1079,flip.1] i39!=i17.
% 3.83/3.92  ** KEPT (pick-wt=3): 1082 [copy,1081,flip.1] i38!=i17.
% 3.83/3.92  ** KEPT (pick-wt=3): 1084 [copy,1083,flip.1] i37!=i17.
% 3.83/3.92  ** KEPT (pick-wt=3): 1086 [copy,1085,flip.1] i36!=i17.
% 3.83/3.92  ** KEPT (pick-wt=3): 1088 [copy,1087,flip.1] i35!=i17.
% 3.83/3.92  ** KEPT (pick-wt=3): 1090 [copy,1089,flip.1] i34!=i17.
% 3.83/3.92  ** KEPT (pick-wt=3): 1092 [copy,1091,flip.1] i33!=i17.
% 3.83/3.92  ** KEPT (pick-wt=3): 1094 [copy,1093,flip.1] i32!=i17.
% 3.83/3.92  ** KEPT (pick-wt=3): 1096 [copy,1095,flip.1] i31!=i17.
% 3.83/3.92  ** KEPT (pick-wt=3): 1098 [copy,1097,flip.1] i30!=i17.
% 3.83/3.92  ** KEPT (pick-wt=3): 1100 [copy,1099,flip.1] i29!=i17.
% 3.83/3.92  ** KEPT (pick-wt=3): 1102 [copy,1101,flip.1] i28!=i17.
% 3.83/3.92  ** KEPT (pick-wt=3): 1104 [copy,1103,flip.1] i27!=i17.
% 3.83/3.92  ** KEPT (pick-wt=3): 1106 [copy,1105,flip.1] i26!=i17.
% 3.83/3.92  ** KEPT (pick-wt=3): 1108 [copy,1107,flip.1] i25!=i17.
% 3.83/3.92  ** KEPT (pick-wt=3): 1110 [copy,1109,flip.1] i24!=i17.
% 3.83/3.92  ** KEPT (pick-wt=3): 1112 [copy,1111,flip.1] i23!=i17.
% 3.83/3.92  ** KEPT (pick-wt=3): 1114 [copy,1113,flip.1] i22!=i17.
% 3.83/3.92  ** KEPT (pick-wt=3): 1116 [copy,1115,flip.1] i21!=i17.
% 3.83/3.92  ** KEPT (pick-wt=3): 1118 [copy,1117,flip.1] i20!=i17.
% 3.83/3.92  ** KEPT (pick-wt=3): 1120 [copy,1119,flip.1] i19!=i17.
% 3.83/3.92  ** KEPT (pick-wt=3): 1122 [copy,1121,flip.1] i18!=i17.
% 3.83/3.92  ** KEPT (pick-wt=3): 1124 [copy,1123,flip.1] i50!=i16.
% 3.83/3.92  ** KEPT (pick-wt=3): 1126 [copy,1125,flip.1] i49!=i16.
% 3.83/3.92  ** KEPT (pick-wt=3): 1128 [copy,1127,flip.1] i48!=i16.
% 3.83/3.92  ** KEPT (pick-wt=3): 1130 [copy,1129,flip.1] i47!=i16.
% 3.83/3.92  ** KEPT (pick-wt=3): 1132 [copy,1131,flip.1] i46!=i16.
% 3.83/3.92  ** KEPT (pick-wt=3): 1134 [copy,1133,flip.1] i45!=i16.
% 3.83/3.92  ** KEPT (pick-wt=3): 1136 [copy,1135,flip.1] i44!=i16.
% 3.83/3.92  ** KEPT (pick-wt=3): 1138 [copy,1137,flip.1] i43!=i16.
% 3.83/3.92  ** KEPT (pick-wt=3): 1140 [copy,1139,flip.1] i42!=i16.
% 3.83/3.92  ** KEPT (pick-wt=3): 1142 [copy,1141,flip.1] i41!=i16.
% 3.83/3.92  ** KEPT (pick-wt=3): 1144 [copy,1143,flip.1] i40!=i16.
% 3.83/3.92  ** KEPT (pick-wt=3): 1146 [copy,1145,flip.1] i39!=i16.
% 3.83/3.92  ** KEPT (pick-wt=3): 1148 [copy,1147,flip.1] i38!=i16.
% 3.83/3.92  ** KEPT (pick-wt=3): 1150 [copy,1149,flip.1] i37!=i16.
% 3.83/3.92  ** KEPT (pick-wt=3): 1152 [copy,1151,flip.1] i36!=i16.
% 3.83/3.92  ** KEPT (pick-wt=3): 1154 [copy,1153,flip.1] i35!=i16.
% 3.83/3.92  ** KEPT (pick-wt=3): 1156 [copy,1155,flip.1] i34!=i16.
% 3.83/3.92  ** KEPT (pick-wt=3): 1158 [copy,1157,flip.1] i33!=i16.
% 3.83/3.92  ** KEPT (pick-wt=3): 1160 [copy,1159,flip.1] i32!=i16.
% 3.83/3.92  ** KEPT (pick-wt=3): 1162 [copy,1161,flip.1] i31!=i16.
% 3.83/3.92  ** KEPT (pick-wt=3): 1164 [copy,1163,flip.1] i30!=i16.
% 3.83/3.92  ** KEPT (pick-wt=3): 1166 [copy,1165,flip.1] i29!=i16.
% 3.83/3.92  ** KEPT (pick-wt=3): 1168 [copy,1167,flip.1] i28!=i16.
% 3.83/3.92  ** KEPT (pick-wt=3): 1170 [copy,1169,flip.1] i27!=i16.
% 3.83/3.92  ** KEPT (pick-wt=3): 1172 [copy,1171,flip.1] i26!=i16.
% 3.83/3.92  ** KEPT (pick-wt=3): 1174 [copy,1173,flip.1] i25!=i16.
% 3.83/3.92  ** KEPT (pick-wt=3): 1176 [copy,1175,flip.1] i24!=i16.
% 3.83/3.92  ** KEPT (pick-wt=3): 1178 [copy,1177,flip.1] i23!=i16.
% 3.83/3.92  ** KEPT (pick-wt=3): 1180 [copy,1179,flip.1] i22!=i16.
% 3.83/3.92  ** KEPT (pick-wt=3): 1182 [copy,1181,flip.1] i21!=i16.
% 3.83/3.92  ** KEPT (pick-wt=3): 1184 [copy,1183,flip.1] i20!=i16.
% 3.83/3.92  ** KEPT (pick-wt=3): 1186 [copy,1185,flip.1] i19!=i16.
% 3.83/3.92  ** KEPT (pick-wt=3): 1188 [copy,1187,flip.1] i18!=i16.
% 3.83/3.92  ** KEPT (pick-wt=3): 1190 [copy,1189,flip.1] i17!=i16.
% 3.83/3.92  ** KEPT (pick-wt=3): 1192 [copy,1191,flip.1] i50!=i15.
% 3.83/3.92  ** KEPT (pick-wt=3): 1194 [copy,1193,flip.1] i49!=i15.
% 3.83/3.92  ** KEPT (pick-wt=3): 1196 [copy,1195,flip.1] i48!=i15.
% 3.83/3.92  ** KEPT (pick-wt=3): 1198 [copy,1197,flip.1] i47!=i15.
% 3.83/3.92  ** KEPT (pick-wt=3): 1200 [copy,1199,flip.1] i46!=i15.
% 3.83/3.92  ** KEPT (pick-wt=3): 1202 [copy,1201,flip.1] i45!=i15.
% 3.83/3.92  ** KEPT (pick-wt=3): 1204 [copy,1203,flip.1] i44!=i15.
% 3.83/3.92  ** KEPT (pick-wt=3): 1206 [copy,1205,flip.1] i43!=i15.
% 3.83/3.92  ** KEPT (pick-wt=3): 1208 [copy,1207,flip.1] i42!=i15.
% 3.83/3.92  ** KEPT (pick-wt=3): 1210 [copy,1209,flip.1] i41!=i15.
% 3.83/3.92  ** KEPT (pick-wt=3): 1212 [copy,1211,flip.1] i40!=i15.
% 3.83/3.92  ** KEPT (pick-wt=3): 1214 [copy,1213,flip.1] i39!=i15.
% 3.83/3.92  ** KEPT (pick-wt=3): 1216 [copy,1215,flip.1] i38!=i15.
% 3.83/3.92  ** KEPT (pick-wt=3): 1218 [copy,1217,flip.1] i37!=i15.
% 3.83/3.92  ** KEPT (pick-wt=3): 1220 [copy,1219,flip.1] i36!=i15.
% 3.83/3.92  ** KEPT (pick-wt=3): 1222 [copy,1221,flip.1] i35!=i15.
% 3.83/3.92  ** KEPT (pick-wt=3): 1224 [copy,1223,flip.1] i34!=i15.
% 3.83/3.92  ** KEPT (pick-wt=3): 1226 [copy,1225,flip.1] i33!=i15.
% 3.83/3.92  ** KEPT (pick-wt=3): 1228 [copy,1227,flip.1] i32!=i15.
% 3.83/3.92  ** KEPT (pick-wt=3): 1230 [copy,1229,flip.1] i31!=i15.
% 3.83/3.92  ** KEPT (pick-wt=3): 1232 [copy,1231,flip.1] i30!=i15.
% 3.83/3.92  ** KEPT (pick-wt=3): 1234 [copy,1233,flip.1] i29!=i15.
% 3.83/3.92  ** KEPT (pick-wt=3): 1236 [copy,1235,flip.1] i28!=i15.
% 3.83/3.92  ** KEPT (pick-wt=3): 1238 [copy,1237,flip.1] i27!=i15.
% 3.83/3.92  ** KEPT (pick-wt=3): 1240 [copy,1239,flip.1] i26!=i15.
% 3.83/3.92  ** KEPT (pick-wt=3): 1242 [copy,1241,flip.1] i25!=i15.
% 3.83/3.92  ** KEPT (pick-wt=3): 1244 [copy,1243,flip.1] i24!=i15.
% 3.83/3.92  ** KEPT (pick-wt=3): 1246 [copy,1245,flip.1] i23!=i15.
% 3.83/3.92  ** KEPT (pick-wt=3): 1248 [copy,1247,flip.1] i22!=i15.
% 3.83/3.92  ** KEPT (pick-wt=3): 1250 [copy,1249,flip.1] i21!=i15.
% 3.83/3.92  ** KEPT (pick-wt=3): 1252 [copy,1251,flip.1] i20!=i15.
% 3.83/3.92  ** KEPT (pick-wt=3): 1254 [copy,1253,flip.1] i19!=i15.
% 3.83/3.92  ** KEPT (pick-wt=3): 1256 [copy,1255,flip.1] i18!=i15.
% 3.83/3.92  ** KEPT (pick-wt=3): 1258 [copy,1257,flip.1] i17!=i15.
% 3.83/3.92  ** KEPT (pick-wt=3): 1260 [copy,1259,flip.1] i16!=i15.
% 3.83/3.92  ** KEPT (pick-wt=3): 1262 [copy,1261,flip.1] i50!=i14.
% 3.83/3.92  ** KEPT (pick-wt=3): 1264 [copy,1263,flip.1] i49!=i14.
% 3.83/3.92  ** KEPT (pick-wt=3): 1266 [copy,1265,flip.1] i48!=i14.
% 3.83/3.92  ** KEPT (pick-wt=3): 1268 [copy,1267,flip.1] i47!=i14.
% 3.83/3.92  ** KEPT (pick-wt=3): 1270 [copy,1269,flip.1] i46!=i14.
% 3.83/3.92  ** KEPT (pick-wt=3): 1272 [copy,1271,flip.1] i45!=i14.
% 3.83/3.92  ** KEPT (pick-wt=3): 1274 [copy,1273,flip.1] i44!=i14.
% 3.83/3.92  ** KEPT (pick-wt=3): 1276 [copy,1275,flip.1] i43!=i14.
% 3.83/3.92  ** KEPT (pick-wt=3): 1278 [copy,1277,flip.1] i42!=i14.
% 3.83/3.92  ** KEPT (pick-wt=3): 1280 [copy,1279,flip.1] i41!=i14.
% 3.83/3.92  ** KEPT (pick-wt=3): 1282 [copy,1281,flip.1] i40!=i14.
% 3.83/3.92  ** KEPT (pick-wt=3): 1284 [copy,1283,flip.1] i39!=i14.
% 3.83/3.92  ** KEPT (pick-wt=3): 1286 [copy,1285,flip.1] i38!=i14.
% 3.83/3.92  ** KEPT (pick-wt=3): 1288 [copy,1287,flip.1] i37!=i14.
% 3.83/3.92  ** KEPT (pick-wt=3): 1290 [copy,1289,flip.1] i36!=i14.
% 3.83/3.92  ** KEPT (pick-wt=3): 1292 [copy,1291,flip.1] i35!=i14.
% 3.83/3.92  ** KEPT (pick-wt=3): 1294 [copy,1293,flip.1] i34!=i14.
% 3.83/3.92  ** KEPT (pick-wt=3): 1296 [copy,1295,flip.1] i33!=i14.
% 3.83/3.92  ** KEPT (pick-wt=3): 1298 [copy,1297,flip.1] i32!=i14.
% 3.83/3.92  ** KEPT (pick-wt=3): 1300 [copy,1299,flip.1] i31!=i14.
% 3.83/3.92  ** KEPT (pick-wt=3): 1302 [copy,1301,flip.1] i30!=i14.
% 3.83/3.92  ** KEPT (pick-wt=3): 1304 [copy,1303,flip.1] i29!=i14.
% 3.83/3.92  ** KEPT (pick-wt=3): 1306 [copy,1305,flip.1] i28!=i14.
% 3.83/3.92  ** KEPT (pick-wt=3): 1308 [copy,1307,flip.1] i27!=i14.
% 3.83/3.92  ** KEPT (pick-wt=3): 1310 [copy,1309,flip.1] i26!=i14.
% 3.83/3.92  ** KEPT (pick-wt=3): 1312 [copy,1311,flip.1] i25!=i14.
% 3.83/3.92  ** KEPT (pick-wt=3): 1314 [copy,1313,flip.1] i24!=i14.
% 3.83/3.92  ** KEPT (pick-wt=3): 1316 [copy,1315,flip.1] i23!=i14.
% 3.83/3.92  ** KEPT (pick-wt=3): 1318 [copy,1317,flip.1] i22!=i14.
% 3.83/3.92  ** KEPT (pick-wt=3): 1320 [copy,1319,flip.1] i21!=i14.
% 3.83/3.92  ** KEPT (pick-wt=3): 1322 [copy,1321,flip.1] i20!=i14.
% 3.83/3.92  ** KEPT (pick-wt=3): 1324 [copy,1323,flip.1] i19!=i14.
% 3.83/3.92  ** KEPT (pick-wt=3): 1326 [copy,1325,flip.1] i18!=i14.
% 3.83/3.92  ** KEPT (pick-wt=3): 1328 [copy,1327,flip.1] i17!=i14.
% 3.83/3.92  ** KEPT (pick-wt=3): 1330 [copy,1329,flip.1] i16!=i14.
% 3.83/3.92  ** KEPT (pick-wt=3): 1332 [copy,1331,flip.1] i15!=i14.
% 3.83/3.92  ** KEPT (pick-wt=3): 1334 [copy,1333,flip.1] i50!=i13.
% 3.83/3.92  ** KEPT (pick-wt=3): 1336 [copy,1335,flip.1] i49!=i13.
% 3.83/3.92  ** KEPT (pick-wt=3): 1338 [copy,1337,flip.1] i48!=i13.
% 3.83/3.92  ** KEPT (pick-wt=3): 1340 [copy,1339,flip.1] i47!=i13.
% 3.83/3.92  ** KEPT (pick-wt=3): 1342 [copy,1341,flip.1] i46!=i13.
% 3.83/3.92  ** KEPT (pick-wt=3): 1344 [copy,1343,flip.1] i45!=i13.
% 3.83/3.92  ** KEPT (pick-wt=3): 1346 [copy,1345,flip.1] i44!=i13.
% 3.83/3.92  ** KEPT (pick-wt=3): 1348 [copy,1347,flip.1] i43!=i13.
% 3.83/3.92  ** KEPT (pick-wt=3): 1350 [copy,1349,flip.1] i42!=i13.
% 3.83/3.92  ** KEPT (pick-wt=3): 1352 [copy,1351,flip.1] i41!=i13.
% 3.83/3.92  ** KEPT (pick-wt=3): 1354 [copy,1353,flip.1] i40!=i13.
% 3.83/3.92  ** KEPT (pick-wt=3): 1356 [copy,1355,flip.1] i39!=i13.
% 3.83/3.92  ** KEPT (pick-wt=3): 1358 [copy,1357,flip.1] i38!=i13.
% 3.83/3.92  ** KEPT (pick-wt=3): 1360 [copy,1359,flip.1] i37!=i13.
% 3.83/3.92  ** KEPT (pick-wt=3): 1362 [copy,1361,flip.1] i36!=i13.
% 3.83/3.92  ** KEPT (pick-wt=3): 1364 [copy,1363,flip.1] i35!=i13.
% 3.83/3.92  ** KEPT (pick-wt=3): 1366 [copy,1365,flip.1] i34!=i13.
% 3.83/3.92  ** KEPT (pick-wt=3): 1368 [copy,1367,flip.1] i33!=i13.
% 3.83/3.92  ** KEPT (pick-wt=3): 1370 [copy,1369,flip.1] i32!=i13.
% 3.83/3.92  ** KEPT (pick-wt=3): 1372 [copy,1371,flip.1] i31!=i13.
% 3.83/3.92  ** KEPT (pick-wt=3): 1374 [copy,1373,flip.1] i30!=i13.
% 3.83/3.92  ** KEPT (pick-wt=3): 1376 [copy,1375,flip.1] i29!=i13.
% 3.83/3.92  ** KEPT (pick-wt=3): 1378 [copy,1377,flip.1] i28!=i13.
% 3.83/3.92  ** KEPT (pick-wt=3): 1380 [copy,1379,flip.1] i27!=i13.
% 3.83/3.92  ** KEPT (pick-wt=3): 1382 [copy,1381,flip.1] i26!=i13.
% 3.83/3.92  ** KEPT (pick-wt=3): 1384 [copy,1383,flip.1] i25!=i13.
% 3.83/3.92  ** KEPT (pick-wt=3): 1386 [copy,1385,flip.1] i24!=i13.
% 3.83/3.92  ** KEPT (pick-wt=3): 1388 [copy,1387,flip.1] i23!=i13.
% 3.83/3.92  ** KEPT (pick-wt=3): 1390 [copy,1389,flip.1] i22!=i13.
% 3.83/3.92  ** KEPT (pick-wt=3): 1392 [copy,1391,flip.1] i21!=i13.
% 3.83/3.92  ** KEPT (pick-wt=3): 1394 [copy,1393,flip.1] i20!=i13.
% 3.83/3.92  ** KEPT (pick-wt=3): 1396 [copy,1395,flip.1] i19!=i13.
% 3.83/3.92  ** KEPT (pick-wt=3): 1398 [copy,1397,flip.1] i18!=i13.
% 3.83/3.92  ** KEPT (pick-wt=3): 1400 [copy,1399,flip.1] i17!=i13.
% 3.83/3.92  ** KEPT (pick-wt=3): 1402 [copy,1401,flip.1] i16!=i13.
% 3.83/3.92  ** KEPT (pick-wt=3): 1404 [copy,1403,flip.1] i15!=i13.
% 3.83/3.92  ** KEPT (pick-wt=3): 1406 [copy,1405,flip.1] i14!=i13.
% 3.83/3.92  ** KEPT (pick-wt=3): 1408 [copy,1407,flip.1] i50!=i12.
% 3.83/3.92  ** KEPT (pick-wt=3): 1410 [copy,1409,flip.1] i49!=i12.
% 3.83/3.92  ** KEPT (pick-wt=3): 1412 [copy,1411,flip.1] i48!=i12.
% 3.83/3.92  ** KEPT (pick-wt=3): 1414 [copy,1413,flip.1] i47!=i12.
% 3.83/3.92  ** KEPT (pick-wt=3): 1416 [copy,1415,flip.1] i46!=i12.
% 3.83/3.92  ** KEPT (pick-wt=3): 1418 [copy,1417,flip.1] i45!=i12.
% 3.83/3.92  ** KEPT (pick-wt=3): 1420 [copy,1419,flip.1] i44!=i12.
% 3.83/3.92  ** KEPT (pick-wt=3): 1422 [copy,1421,flip.1] i43!=i12.
% 3.83/3.92  ** KEPT (pick-wt=3): 1424 [copy,1423,flip.1] i42!=i12.
% 3.83/3.92  ** KEPT (pick-wt=3): 1426 [copy,1425,flip.1] i41!=i12.
% 3.83/3.92  ** KEPT (pick-wt=3): 1428 [copy,1427,flip.1] i40!=i12.
% 3.83/3.92  ** KEPT (pick-wt=3): 1430 [copy,1429,flip.1] i39!=i12.
% 3.83/3.92  ** KEPT (pick-wt=3): 1432 [copy,1431,flip.1] i38!=i12.
% 3.83/3.92  ** KEPT (pick-wt=3): 1434 [copy,1433,flip.1] i37!=i12.
% 3.83/3.92  ** KEPT (pick-wt=3): 1436 [copy,1435,flip.1] i36!=i12.
% 3.83/3.92  ** KEPT (pick-wt=3): 1438 [copy,1437,flip.1] i35!=i12.
% 3.83/3.92  ** KEPT (pick-wt=3): 1440 [copy,1439,flip.1] i34!=i12.
% 3.83/3.92  ** KEPT (pick-wt=3): 1442 [copy,1441,flip.1] i33!=i12.
% 3.83/3.92  ** KEPT (pick-wt=3): 1444 [copy,1443,flip.1] i32!=i12.
% 3.83/3.92  ** KEPT (pick-wt=3): 1446 [copy,1445,flip.1] i31!=i12.
% 3.83/3.92  ** KEPT (pick-wt=3): 1448 [copy,1447,flip.1] i30!=i12.
% 3.83/3.92  ** KEPT (pick-wt=3): 1450 [copy,1449,flip.1] i29!=i12.
% 3.83/3.92  ** KEPT (pick-wt=3): 1452 [copy,1451,flip.1] i28!=i12.
% 3.83/3.92  ** KEPT (pick-wt=3): 1454 [copy,1453,flip.1] i27!=i12.
% 3.83/3.92  ** KEPT (pick-wt=3): 1456 [copy,1455,flip.1] i26!=i12.
% 3.83/3.92  ** KEPT (pick-wt=3): 1458 [copy,1457,flip.1] i25!=i12.
% 3.83/3.92  ** KEPT (pick-wt=3): 1460 [copy,1459,flip.1] i24!=i12.
% 3.83/3.92  ** KEPT (pick-wt=3): 1462 [copy,1461,flip.1] i23!=i12.
% 3.83/3.92  ** KEPT (pick-wt=3): 1464 [copy,1463,flip.1] i22!=i12.
% 3.83/3.92  ** KEPT (pick-wt=3): 1466 [copy,1465,flip.1] i21!=i12.
% 3.83/3.92  ** KEPT (pick-wt=3): 1468 [copy,1467,flip.1] i20!=i12.
% 3.83/3.92  ** KEPT (pick-wt=3): 1470 [copy,1469,flip.1] i19!=i12.
% 3.83/3.92  ** KEPT (pick-wt=3): 1472 [copy,1471,flip.1] i18!=i12.
% 3.83/3.92  ** KEPT (pick-wt=3): 1474 [copy,1473,flip.1] i17!=i12.
% 3.83/3.92  ** KEPT (pick-wt=3): 1476 [copy,1475,flip.1] i16!=i12.
% 3.83/3.92  ** KEPT (pick-wt=3): 1478 [copy,1477,flip.1] i15!=i12.
% 3.83/3.92  ** KEPT (pick-wt=3): 1480 [copy,1479,flip.1] i14!=i12.
% 3.83/3.92  ** KEPT (pick-wt=3): 1482 [copy,1481,flip.1] i13!=i12.
% 3.83/3.92  ** KEPT (pick-wt=3): 1484 [copy,1483,flip.1] i50!=i11.
% 3.83/3.92  ** KEPT (pick-wt=3): 1486 [copy,1485,flip.1] i49!=i11.
% 3.83/3.92  ** KEPT (pick-wt=3): 1488 [copy,1487,flip.1] i48!=i11.
% 3.83/3.92  ** KEPT (pick-wt=3): 1490 [copy,1489,flip.1] i47!=i11.
% 3.83/3.92  ** KEPT (pick-wt=3): 1492 [copy,1491,flip.1] i46!=i11.
% 3.83/3.92  ** KEPT (pick-wt=3): 1494 [copy,1493,flip.1] i45!=i11.
% 3.83/3.92  ** KEPT (pick-wt=3): 1496 [copy,1495,flip.1] i44!=i11.
% 3.83/3.92  ** KEPT (pick-wt=3): 1498 [copy,1497,flip.1] i43!=i11.
% 3.83/3.92  ** KEPT (pick-wt=3): 1500 [copy,1499,flip.1] i42!=i11.
% 3.83/3.92  ** KEPT (pick-wt=3): 1502 [copy,1501,flip.1] i41!=i11.
% 3.83/3.92  ** KEPT (pick-wt=3): 1504 [copy,1503,flip.1] i40!=i11.
% 3.83/3.92  ** KEPT (pick-wt=3): 1506 [copy,1505,flip.1] i39!=i11.
% 3.83/3.92  ** KEPT (pick-wt=3): 1508 [copy,1507,flip.1] i38!=i11.
% 3.83/3.92  ** KEPT (pick-wt=3): 1510 [copy,1509,flip.1] i37!=i11.
% 3.83/3.92  ** KEPT (pick-wt=3): 1512 [copy,1511,flip.1] i36!=i11.
% 3.83/3.92  ** KEPT (pick-wt=3): 1514 [copy,1513,flip.1] i35!=i11.
% 3.83/3.92  ** KEPT (pick-wt=3): 1516 [copy,1515,flip.1] i34!=i11.
% 3.83/3.92  ** KEPT (pick-wt=3): 1518 [copy,1517,flip.1] i33!=i11.
% 3.83/3.92  ** KEPT (pick-wt=3): 1520 [copy,1519,flip.1] i32!=i11.
% 3.83/3.92  ** KEPT (pick-wt=3): 1522 [copy,1521,flip.1] i31!=i11.
% 3.83/3.92  ** KEPT (pick-wt=3): 1524 [copy,1523,flip.1] i30!=i11.
% 3.83/3.92  ** KEPT (pick-wt=3): 1526 [copy,1525,flip.1] i29!=i11.
% 3.83/3.92  ** KEPT (pick-wt=3): 1528 [copy,1527,flip.1] i28!=i11.
% 3.83/3.92  ** KEPT (pick-wt=3): 1530 [copy,1529,flip.1] i27!=i11.
% 3.83/3.92  ** KEPT (pick-wt=3): 1532 [copy,1531,flip.1] i26!=i11.
% 3.83/3.92  ** KEPT (pick-wt=3): 1534 [copy,1533,flip.1] i25!=i11.
% 3.83/3.92  ** KEPT (pick-wt=3): 1536 [copy,1535,flip.1] i24!=i11.
% 3.83/3.92  ** KEPT (pick-wt=3): 1538 [copy,1537,flip.1] i23!=i11.
% 3.83/3.92  ** KEPT (pick-wt=3): 1540 [copy,1539,flip.1] i22!=i11.
% 3.83/3.92  ** KEPT (pick-wt=3): 1542 [copy,1541,flip.1] i21!=i11.
% 3.83/3.92  ** KEPT (pick-wt=3): 1544 [copy,1543,flip.1] i20!=i11.
% 3.83/3.92  ** KEPT (pick-wt=3): 1546 [copy,1545,flip.1] i19!=i11.
% 3.83/3.92  ** KEPT (pick-wt=3): 1548 [copy,1547,flip.1] i18!=i11.
% 3.83/3.92  ** KEPT (pick-wt=3): 1550 [copy,1549,flip.1] i17!=i11.
% 3.83/3.92  ** KEPT (pick-wt=3): 1552 [copy,1551,flip.1] i16!=i11.
% 3.83/3.92  ** KEPT (pick-wt=3): 1554 [copy,1553,flip.1] i15!=i11.
% 3.83/3.92  ** KEPT (pick-wt=3): 1556 [copy,1555,flip.1] i14!=i11.
% 3.83/3.92  ** KEPT (pick-wt=3): 1558 [copy,1557,flip.1] i13!=i11.
% 3.83/3.92  ** KEPT (pick-wt=3): 1560 [copy,1559,flip.1] i12!=i11.
% 3.83/3.92  ** KEPT (pick-wt=3): 1562 [copy,1561,flip.1] i50!=i10.
% 3.83/3.92  ** KEPT (pick-wt=3): 1564 [copy,1563,flip.1] i49!=i10.
% 3.83/3.92  ** KEPT (pick-wt=3): 1566 [copy,1565,flip.1] i48!=i10.
% 3.83/3.92  ** KEPT (pick-wt=3): 1568 [copy,1567,flip.1] i47!=i10.
% 3.83/3.92  ** KEPT (pick-wt=3): 1570 [copy,1569,flip.1] i46!=i10.
% 3.83/3.92  ** KEPT (pick-wt=3): 1572 [copy,1571,flip.1] i45!=i10.
% 3.83/3.92  ** KEPT (pick-wt=3): 1574 [copy,1573,flip.1] i44!=i10.
% 3.83/3.92  ** KEPT (pick-wt=3): 1576 [copy,1575,flip.1] i43!=i10.
% 3.83/3.92  ** KEPT (pick-wt=3): 1578 [copy,1577,flip.1] i42!=i10.
% 3.83/3.92  ** KEPT (pick-wt=3): 1580 [copy,1579,flip.1] i41!=i10.
% 3.83/3.92  ** KEPT (pick-wt=3): 1582 [copy,1581,flip.1] i40!=i10.
% 3.83/3.92  ** KEPT (pick-wt=3): 1584 [copy,1583,flip.1] i39!=i10.
% 3.83/3.92  ** KEPT (pick-wt=3): 1586 [copy,1585,flip.1] i38!=i10.
% 3.83/3.93  ** KEPT (pick-wt=3): 1588 [copy,1587,flip.1] i37!=i10.
% 3.83/3.93  ** KEPT (pick-wt=3): 1590 [copy,1589,flip.1] i36!=i10.
% 3.83/3.93  ** KEPT (pick-wt=3): 1592 [copy,1591,flip.1] i35!=i10.
% 3.83/3.93  ** KEPT (pick-wt=3): 1594 [copy,1593,flip.1] i34!=i10.
% 3.83/3.93  ** KEPT (pick-wt=3): 1596 [copy,1595,flip.1] i33!=i10.
% 3.83/3.93  ** KEPT (pick-wt=3): 1598 [copy,1597,flip.1] i32!=i10.
% 3.83/3.93  ** KEPT (pick-wt=3): 1600 [copy,1599,flip.1] i31!=i10.
% 3.83/3.93  ** KEPT (pick-wt=3): 1602 [copy,1601,flip.1] i30!=i10.
% 3.83/3.93  ** KEPT (pick-wt=3): 1604 [copy,1603,flip.1] i29!=i10.
% 3.83/3.93  ** KEPT (pick-wt=3): 1606 [copy,1605,flip.1] i28!=i10.
% 3.83/3.93  ** KEPT (pick-wt=3): 1608 [copy,1607,flip.1] i27!=i10.
% 3.83/3.93  ** KEPT (pick-wt=3): 1610 [copy,1609,flip.1] i26!=i10.
% 3.83/3.93  ** KEPT (pick-wt=3): 1612 [copy,1611,flip.1] i25!=i10.
% 3.83/3.93  ** KEPT (pick-wt=3): 1614 [copy,1613,flip.1] i24!=i10.
% 3.83/3.93  ** KEPT (pick-wt=3): 1616 [copy,1615,flip.1] i23!=i10.
% 3.83/3.93  ** KEPT (pick-wt=3): 1618 [copy,1617,flip.1] i22!=i10.
% 3.83/3.93  ** KEPT (pick-wt=3): 1620 [copy,1619,flip.1] i21!=i10.
% 3.83/3.93  ** KEPT (pick-wt=3): 1622 [copy,1621,flip.1] i20!=i10.
% 3.83/3.93  ** KEPT (pick-wt=3): 1624 [copy,1623,flip.1] i19!=i10.
% 3.83/3.93  ** KEPT (pick-wt=3): 1626 [copy,1625,flip.1] i18!=i10.
% 3.83/3.93  ** KEPT (pick-wt=3): 1628 [copy,1627,flip.1] i17!=i10.
% 3.83/3.93  ** KEPT (pick-wt=3): 1630 [copy,1629,flip.1] i16!=i10.
% 3.83/3.93  ** KEPT (pick-wt=3): 1632 [copy,1631,flip.1] i15!=i10.
% 3.83/3.93  ** KEPT (pick-wt=3): 1634 [copy,1633,flip.1] i14!=i10.
% 3.83/3.93  ** KEPT (pick-wt=3): 1636 [copy,1635,flip.1] i13!=i10.
% 3.83/3.93  ** KEPT (pick-wt=3): 1638 [copy,1637,flip.1] i12!=i10.
% 3.83/3.93  ** KEPT (pick-wt=3): 1640 [copy,1639,flip.1] i11!=i10.
% 3.83/3.93  ** KEPT (pick-wt=3): 1641 [] i9!=i50.
% 3.83/3.93  ** KEPT (pick-wt=3): 1642 [] i9!=i49.
% 3.83/3.93  ** KEPT (pick-wt=3): 1643 [] i9!=i48.
% 3.83/3.93  ** KEPT (pick-wt=3): 1644 [] i9!=i47.
% 3.83/3.93  ** KEPT (pick-wt=3): 1645 [] i9!=i46.
% 3.83/3.93  ** KEPT (pick-wt=3): 1646 [] i9!=i45.
% 3.83/3.93  ** KEPT (pick-wt=3): 1647 [] i9!=i44.
% 3.83/3.93  ** KEPT (pick-wt=3): 1648 [] i9!=i43.
% 3.83/3.93  ** KEPT (pick-wt=3): 1649 [] i9!=i42.
% 3.83/3.93  ** KEPT (pick-wt=3): 1650 [] i9!=i41.
% 3.83/3.93  ** KEPT (pick-wt=3): 1651 [] i9!=i40.
% 3.83/3.93  ** KEPT (pick-wt=3): 1652 [] i9!=i39.
% 3.83/3.93  ** KEPT (pick-wt=3): 1653 [] i9!=i38.
% 3.83/3.93  ** KEPT (pick-wt=3): 1654 [] i9!=i37.
% 3.83/3.93  ** KEPT (pick-wt=3): 1655 [] i9!=i36.
% 3.83/3.93  ** KEPT (pick-wt=3): 1656 [] i9!=i35.
% 3.83/3.93  ** KEPT (pick-wt=3): 1657 [] i9!=i34.
% 3.83/3.93  ** KEPT (pick-wt=3): 1658 [] i9!=i33.
% 3.83/3.93  ** KEPT (pick-wt=3): 1659 [] i9!=i32.
% 3.83/3.93  ** KEPT (pick-wt=3): 1660 [] i9!=i31.
% 3.83/3.93  ** KEPT (pick-wt=3): 1661 [] i9!=i30.
% 3.83/3.93  ** KEPT (pick-wt=3): 1662 [] i9!=i29.
% 3.83/3.93  ** KEPT (pick-wt=3): 1663 [] i9!=i28.
% 3.83/3.93  ** KEPT (pick-wt=3): 1664 [] i9!=i27.
% 3.83/3.93  ** KEPT (pick-wt=3): 1665 [] i9!=i26.
% 3.83/3.93  ** KEPT (pick-wt=3): 1666 [] i9!=i25.
% 3.83/3.93  ** KEPT (pick-wt=3): 1667 [] i9!=i24.
% 3.83/3.93  ** KEPT (pick-wt=3): 1668 [] i9!=i23.
% 3.83/3.93  ** KEPT (pick-wt=3): 1669 [] i9!=i22.
% 3.83/3.93  ** KEPT (pick-wt=3): 1670 [] i9!=i21.
% 3.83/3.93  ** KEPT (pick-wt=3): 1671 [] i9!=i20.
% 3.83/3.93  ** KEPT (pick-wt=3): 1672 [] i9!=i19.
% 3.83/3.93  ** KEPT (pick-wt=3): 1673 [] i9!=i18.
% 3.83/3.93  ** KEPT (pick-wt=3): 1674 [] i9!=i17.
% 3.83/3.93  ** KEPT (pick-wt=3): 1675 [] i9!=i16.
% 3.83/3.93  ** KEPT (pick-wt=3): 1676 [] i9!=i15.
% 3.83/3.93  ** KEPT (pick-wt=3): 1677 [] i9!=i14.
% 3.83/3.93  ** KEPT (pick-wt=3): 1678 [] i9!=i13.
% 3.83/3.93  ** KEPT (pick-wt=3): 1679 [] i9!=i12.
% 3.83/3.93  ** KEPT (pick-wt=3): 1680 [] i9!=i11.
% 3.83/3.93  ** KEPT (pick-wt=3): 1681 [] i9!=i10.
% 3.83/3.93  ** KEPT (pick-wt=3): 1682 [] i8!=i50.
% 3.83/3.93  ** KEPT (pick-wt=3): 1683 [] i8!=i49.
% 3.83/3.93  ** KEPT (pick-wt=3): 1684 [] i8!=i48.
% 3.83/3.93  ** KEPT (pick-wt=3): 1685 [] i8!=i47.
% 3.83/3.93  ** KEPT (pick-wt=3): 1686 [] i8!=i46.
% 3.83/3.93  ** KEPT (pick-wt=3): 1687 [] i8!=i45.
% 3.83/3.93  ** KEPT (pick-wt=3): 1688 [] i8!=i44.
% 3.83/3.93  ** KEPT (pick-wt=3): 1689 [] i8!=i43.
% 3.83/3.93  ** KEPT (pick-wt=3): 1690 [] i8!=i42.
% 3.83/3.93  ** KEPT (pick-wt=3): 1691 [] i8!=i41.
% 3.83/3.93  ** KEPT (pick-wt=3): 1692 [] i8!=i40.
% 3.83/3.93  ** KEPT (pick-wt=3): 1693 [] i8!=i39.
% 3.83/3.93  ** KEPT (pick-wt=3): 1694 [] i8!=i38.
% 3.83/3.93  ** KEPT (pick-wt=3): 1695 [] i8!=i37.
% 3.83/3.93  ** KEPT (pick-wt=3): 1696 [] i8!=i36.
% 3.83/3.93  ** KEPT (pick-wt=3): 1697 [] i8!=i35.
% 3.83/3.93  ** KEPT (pick-wt=3): 1698 [] i8!=i34.
% 3.83/3.93  ** KEPT (pick-wt=3): 1699 [] i8!=i33.
% 3.83/3.93  ** KEPT (pick-wt=3): 1700 [] i8!=i32.
% 3.83/3.93  ** KEPT (pick-wt=3): 1701 [] i8!=i31.
% 3.83/3.93  ** KEPT (pick-wt=3): 1702 [] i8!=i30.
% 3.83/3.93  ** KEPT (pick-wt=3): 1703 [] i8!=i29.
% 3.83/3.93  ** KEPT (pick-wt=3): 1704 [] i8!=i28.
% 3.83/3.93  ** KEPT (pick-wt=3): 1705 [] i8!=i27.
% 3.83/3.93  ** KEPT (pick-wt=3): 1706 [] i8!=i26.
% 3.83/3.93  ** KEPT (pick-wt=3): 1707 [] i8!=i25.
% 3.83/3.93  ** KEPT (pick-wt=3): 1708 [] i8!=i24.
% 3.83/3.93  ** KEPT (pick-wt=3): 1709 [] i8!=i23.
% 3.83/3.93  ** KEPT (pick-wt=3): 1710 [] i8!=i22.
% 3.83/3.93  ** KEPT (pick-wt=3): 1711 [] i8!=i21.
% 3.83/3.93  ** KEPT (pick-wt=3): 1712 [] i8!=i20.
% 3.83/3.93  ** KEPT (pick-wt=3): 1713 [] i8!=i19.
% 3.83/3.93  ** KEPT (pick-wt=3): 1714 [] i8!=i18.
% 3.83/3.93  ** KEPT (pick-wt=3): 1715 [] i8!=i17.
% 3.83/3.93  ** KEPT (pick-wt=3): 1716 [] i8!=i16.
% 3.83/3.93  ** KEPT (pick-wt=3): 1717 [] i8!=i15.
% 3.83/3.93  ** KEPT (pick-wt=3): 1718 [] i8!=i14.
% 3.83/3.93  ** KEPT (pick-wt=3): 1719 [] i8!=i13.
% 3.83/3.93  ** KEPT (pick-wt=3): 1720 [] i8!=i12.
% 3.83/3.93  ** KEPT (pick-wt=3): 1721 [] i8!=i11.
% 3.83/3.93  ** KEPT (pick-wt=3): 1722 [] i8!=i10.
% 3.83/3.93  ** KEPT (pick-wt=3): 1724 [copy,1723,flip.1] i9!=i8.
% 3.83/3.93  ** KEPT (pick-wt=3): 1725 [] i7!=i50.
% 3.83/3.93  ** KEPT (pick-wt=3): 1726 [] i7!=i49.
% 3.83/3.93  ** KEPT (pick-wt=3): 1727 [] i7!=i48.
% 3.83/3.93  ** KEPT (pick-wt=3): 1728 [] i7!=i47.
% 3.83/3.93  ** KEPT (pick-wt=3): 1729 [] i7!=i46.
% 3.83/3.93  ** KEPT (pick-wt=3): 1730 [] i7!=i45.
% 3.83/3.93  ** KEPT (pick-wt=3): 1731 [] i7!=i44.
% 3.83/3.93  ** KEPT (pick-wt=3): 1732 [] i7!=i43.
% 3.83/3.93  ** KEPT (pick-wt=3): 1733 [] i7!=i42.
% 3.83/3.93  ** KEPT (pick-wt=3): 1734 [] i7!=i41.
% 3.83/3.93  ** KEPT (pick-wt=3): 1735 [] i7!=i40.
% 3.83/3.93  ** KEPT (pick-wt=3): 1736 [] i7!=i39.
% 3.83/3.93  ** KEPT (pick-wt=3): 1737 [] i7!=i38.
% 3.83/3.93  ** KEPT (pick-wt=3): 1738 [] i7!=i37.
% 3.83/3.93  ** KEPT (pick-wt=3): 1739 [] i7!=i36.
% 3.83/3.93  ** KEPT (pick-wt=3): 1740 [] i7!=i35.
% 3.83/3.93  ** KEPT (pick-wt=3): 1741 [] i7!=i34.
% 3.83/3.93  ** KEPT (pick-wt=3): 1742 [] i7!=i33.
% 3.83/3.93  ** KEPT (pick-wt=3): 1743 [] i7!=i32.
% 3.83/3.93  ** KEPT (pick-wt=3): 1744 [] i7!=i31.
% 3.83/3.93  ** KEPT (pick-wt=3): 1745 [] i7!=i30.
% 3.83/3.93  ** KEPT (pick-wt=3): 1746 [] i7!=i29.
% 3.83/3.93  ** KEPT (pick-wt=3): 1747 [] i7!=i28.
% 3.83/3.93  ** KEPT (pick-wt=3): 1748 [] i7!=i27.
% 3.83/3.93  ** KEPT (pick-wt=3): 1749 [] i7!=i26.
% 3.83/3.93  ** KEPT (pick-wt=3): 1750 [] i7!=i25.
% 3.83/3.93  ** KEPT (pick-wt=3): 1751 [] i7!=i24.
% 3.83/3.93  ** KEPT (pick-wt=3): 1752 [] i7!=i23.
% 3.83/3.93  ** KEPT (pick-wt=3): 1753 [] i7!=i22.
% 3.83/3.93  ** KEPT (pick-wt=3): 1754 [] i7!=i21.
% 3.83/3.93  ** KEPT (pick-wt=3): 1755 [] i7!=i20.
% 3.83/3.93  ** KEPT (pick-wt=3): 1756 [] i7!=i19.
% 3.83/3.93  ** KEPT (pick-wt=3): 1757 [] i7!=i18.
% 3.83/3.93  ** KEPT (pick-wt=3): 1758 [] i7!=i17.
% 3.83/3.93  ** KEPT (pick-wt=3): 1759 [] i7!=i16.
% 3.83/3.93  ** KEPT (pick-wt=3): 1760 [] i7!=i15.
% 3.83/3.93  ** KEPT (pick-wt=3): 1761 [] i7!=i14.
% 3.83/3.93  ** KEPT (pick-wt=3): 1762 [] i7!=i13.
% 3.83/3.93  ** KEPT (pick-wt=3): 1763 [] i7!=i12.
% 3.83/3.93  ** KEPT (pick-wt=3): 1764 [] i7!=i11.
% 3.83/3.93  ** KEPT (pick-wt=3): 1765 [] i7!=i10.
% 3.83/3.93  ** KEPT (pick-wt=3): 1767 [copy,1766,flip.1] i9!=i7.
% 3.83/3.93  ** KEPT (pick-wt=3): 1769 [copy,1768,flip.1] i8!=i7.
% 3.83/3.93  ** KEPT (pick-wt=3): 1770 [] i6!=i50.
% 3.83/3.93  ** KEPT (pick-wt=3): 1771 [] i6!=i49.
% 3.83/3.93  ** KEPT (pick-wt=3): 1772 [] i6!=i48.
% 3.83/3.93  ** KEPT (pick-wt=3): 1773 [] i6!=i47.
% 3.83/3.93  ** KEPT (pick-wt=3): 1774 [] i6!=i46.
% 3.83/3.93  ** KEPT (pick-wt=3): 1775 [] i6!=i45.
% 3.83/3.93  ** KEPT (pick-wt=3): 1776 [] i6!=i44.
% 3.83/3.93  ** KEPT (pick-wt=3): 1777 [] i6!=i43.
% 3.83/3.93  ** KEPT (pick-wt=3): 1778 [] i6!=i42.
% 3.83/3.93  ** KEPT (pick-wt=3): 1779 [] i6!=i41.
% 3.83/3.93  ** KEPT (pick-wt=3): 1780 [] i6!=i40.
% 3.83/3.93  ** KEPT (pick-wt=3): 1781 [] i6!=i39.
% 3.83/3.93  ** KEPT (pick-wt=3): 1782 [] i6!=i38.
% 3.83/3.93  ** KEPT (pick-wt=3): 1783 [] i6!=i37.
% 3.83/3.93  ** KEPT (pick-wt=3): 1784 [] i6!=i36.
% 3.83/3.93  ** KEPT (pick-wt=3): 1785 [] i6!=i35.
% 3.83/3.93  ** KEPT (pick-wt=3): 1786 [] i6!=i34.
% 3.83/3.93  ** KEPT (pick-wt=3): 1787 [] i6!=i33.
% 3.83/3.93  ** KEPT (pick-wt=3): 1788 [] i6!=i32.
% 3.83/3.93  ** KEPT (pick-wt=3): 1789 [] i6!=i31.
% 3.83/3.93  ** KEPT (pick-wt=3): 1790 [] i6!=i30.
% 3.83/3.93  ** KEPT (pick-wt=3): 1791 [] i6!=i29.
% 3.83/3.93  ** KEPT (pick-wt=3): 1792 [] i6!=i28.
% 3.83/3.93  ** KEPT (pick-wt=3): 1793 [] i6!=i27.
% 3.83/3.93  ** KEPT (pick-wt=3): 1794 [] i6!=i26.
% 3.83/3.93  ** KEPT (pick-wt=3): 1795 [] i6!=i25.
% 3.83/3.93  ** KEPT (pick-wt=3): 1796 [] i6!=i24.
% 3.83/3.93  ** KEPT (pick-wt=3): 1797 [] i6!=i23.
% 3.83/3.93  ** KEPT (pick-wt=3): 1798 [] i6!=i22.
% 3.83/3.93  ** KEPT (pick-wt=3): 1799 [] i6!=i21.
% 3.83/3.93  ** KEPT (pick-wt=3): 1800 [] i6!=i20.
% 3.83/3.93  ** KEPT (pick-wt=3): 1801 [] i6!=i19.
% 3.83/3.93  ** KEPT (pick-wt=3): 1802 [] i6!=i18.
% 3.83/3.93  ** KEPT (pick-wt=3): 1803 [] i6!=i17.
% 3.83/3.93  ** KEPT (pick-wt=3): 1804 [] i6!=i16.
% 3.83/3.93  ** KEPT (pick-wt=3): 1805 [] i6!=i15.
% 3.83/3.93  ** KEPT (pick-wt=3): 1806 [] i6!=i14.
% 3.83/3.93  ** KEPT (pick-wt=3): 1807 [] i6!=i13.
% 3.83/3.93  ** KEPT (pick-wt=3): 1808 [] i6!=i12.
% 3.83/3.93  ** KEPT (pick-wt=3): 1809 [] i6!=i11.
% 3.83/3.93  ** KEPT (pick-wt=3): 1810 [] i6!=i10.
% 3.83/3.93  ** KEPT (pick-wt=3): 1812 [copy,1811,flip.1] i9!=i6.
% 3.83/3.93  ** KEPT (pick-wt=3): 1814 [copy,1813,flip.1] i8!=i6.
% 3.83/3.93  ** KEPT (pick-wt=3): 1816 [copy,1815,flip.1] i7!=i6.
% 3.83/3.93  ** KEPT (pick-wt=3): 1818 [copy,1817,flip.1] i50!=i5.
% 3.83/3.93  ** KEPT (pick-wt=3): 1819 [] i5!=i49.
% 3.83/3.93  ** KEPT (pick-wt=3): 1820 [] i5!=i48.
% 3.83/3.93  ** KEPT (pick-wt=3): 1821 [] i5!=i47.
% 3.83/3.93  ** KEPT (pick-wt=3): 1822 [] i5!=i46.
% 3.83/3.93  ** KEPT (pick-wt=3): 1823 [] i5!=i45.
% 3.83/3.93  ** KEPT (pick-wt=3): 1824 [] i5!=i44.
% 3.83/3.93  ** KEPT (pick-wt=3): 1825 [] i5!=i43.
% 3.83/3.93  ** KEPT (pick-wt=3): 1826 [] i5!=i42.
% 3.83/3.93  ** KEPT (pick-wt=3): 1827 [] i5!=i41.
% 3.83/3.93  ** KEPT (pick-wt=3): 1828 [] i5!=i40.
% 3.83/3.93  ** KEPT (pick-wt=3): 1829 [] i5!=i39.
% 3.83/3.93  ** KEPT (pick-wt=3): 1830 [] i5!=i38.
% 3.83/3.93  ** KEPT (pick-wt=3): 1831 [] i5!=i37.
% 3.83/3.93  ** KEPT (pick-wt=3): 1832 [] i5!=i36.
% 3.83/3.93  ** KEPT (pick-wt=3): 1833 [] i5!=i35.
% 3.83/3.93  ** KEPT (pick-wt=3): 1834 [] i5!=i34.
% 3.83/3.93  ** KEPT (pick-wt=3): 1835 [] i5!=i33.
% 3.83/3.93  ** KEPT (pick-wt=3): 1836 [] i5!=i32.
% 3.83/3.93  ** KEPT (pick-wt=3): 1837 [] i5!=i31.
% 3.83/3.93  ** KEPT (pick-wt=3): 1838 [] i5!=i30.
% 3.83/3.93  ** KEPT (pick-wt=3): 1839 [] i5!=i29.
% 3.83/3.93  ** KEPT (pick-wt=3): 1840 [] i5!=i28.
% 3.83/3.93  ** KEPT (pick-wt=3): 1841 [] i5!=i27.
% 3.83/3.93  ** KEPT (pick-wt=3): 1842 [] i5!=i26.
% 3.83/3.93  ** KEPT (pick-wt=3): 1843 [] i5!=i25.
% 3.83/3.93  ** KEPT (pick-wt=3): 1844 [] i5!=i24.
% 3.83/3.93  ** KEPT (pick-wt=3): 1845 [] i5!=i23.
% 3.83/3.93  ** KEPT (pick-wt=3): 1846 [] i5!=i22.
% 3.83/3.93  ** KEPT (pick-wt=3): 1847 [] i5!=i21.
% 3.83/3.93  ** KEPT (pick-wt=3): 1848 [] i5!=i20.
% 3.83/3.93  ** KEPT (pick-wt=3): 1849 [] i5!=i19.
% 3.83/3.93  ** KEPT (pick-wt=3): 1850 [] i5!=i18.
% 3.83/3.93  ** KEPT (pick-wt=3): 1851 [] i5!=i17.
% 3.83/3.93  ** KEPT (pick-wt=3): 1852 [] i5!=i16.
% 3.83/3.93  ** KEPT (pick-wt=3): 1853 [] i5!=i15.
% 3.83/3.93  ** KEPT (pick-wt=3): 1854 [] i5!=i14.
% 3.83/3.93  ** KEPT (pick-wt=3): 1855 [] i5!=i13.
% 3.83/3.93  ** KEPT (pick-wt=3): 1856 [] i5!=i12.
% 3.83/3.93  ** KEPT (pick-wt=3): 1857 [] i5!=i11.
% 3.83/3.93  ** KEPT (pick-wt=3): 1858 [] i5!=i10.
% 3.83/3.93  ** KEPT (pick-wt=3): 1860 [copy,1859,flip.1] i9!=i5.
% 3.83/3.93  ** KEPT (pick-wt=3): 1862 [copy,1861,flip.1] i8!=i5.
% 3.83/3.93  ** KEPT (pick-wt=3): 1864 [copy,1863,flip.1] i7!=i5.
% 3.83/3.93  ** KEPT (pick-wt=3): 1866 [copy,1865,flip.1] i6!=i5.
% 3.83/3.93  ** KEPT (pick-wt=3): 1868 [copy,1867,flip.1] i50!=i4.
% 3.83/3.93  ** KEPT (pick-wt=3): 1870 [copy,1869,flip.1] i49!=i4.
% 3.83/3.93  ** KEPT (pick-wt=3): 1872 [copy,1871,flip.1] i48!=i4.
% 3.83/3.93  ** KEPT (pick-wt=3): 1874 [copy,1873,flip.1] i47!=i4.
% 3.83/3.93  ** KEPT (pick-wt=3): 1876 [copy,1875,flip.1] i46!=i4.
% 3.83/3.93  ** KEPT (pick-wt=3): 1878 [copy,1877,flip.1] i45!=i4.
% 3.83/3.93  ** KEPT (pick-wt=3): 1880 [copy,1879,flip.1] i44!=i4.
% 3.83/3.93  ** KEPT (pick-wt=3): 1882 [copy,1881,flip.1] i43!=i4.
% 3.83/3.93  ** KEPT (pick-wt=3): 1884 [copy,1883,flip.1] i42!=i4.
% 3.83/3.93  ** KEPT (pick-wt=3): 1886 [copy,1885,flip.1] i41!=i4.
% 3.83/3.93  ** KEPT (pick-wt=3): 1888 [copy,1887,flip.1] i40!=i4.
% 3.83/3.93  ** KEPT (pick-wt=3): 1889 [] i4!=i39.
% 3.83/3.93  ** KEPT (pick-wt=3): 1890 [] i4!=i38.
% 3.83/3.93  ** KEPT (pick-wt=3): 1891 [] i4!=i37.
% 3.83/3.93  ** KEPT (pick-wt=3): 1892 [] i4!=i36.
% 3.83/3.93  ** KEPT (pick-wt=3): 1893 [] i4!=i35.
% 3.83/3.93  ** KEPT (pick-wt=3): 1894 [] i4!=i34.
% 3.83/3.93  ** KEPT (pick-wt=3): 1895 [] i4!=i33.
% 3.83/3.93  ** KEPT (pick-wt=3): 1896 [] i4!=i32.
% 3.83/3.93  ** KEPT (pick-wt=3): 1897 [] i4!=i31.
% 3.83/3.93  ** KEPT (pick-wt=3): 1898 [] i4!=i30.
% 3.83/3.93  ** KEPT (pick-wt=3): 1899 [] i4!=i29.
% 3.83/3.93  ** KEPT (pick-wt=3): 1900 [] i4!=i28.
% 3.83/3.93  ** KEPT (pick-wt=3): 1901 [] i4!=i27.
% 3.83/3.93  ** KEPT (pick-wt=3): 1902 [] i4!=i26.
% 3.83/3.93  ** KEPT (pick-wt=3): 1903 [] i4!=i25.
% 3.83/3.93  ** KEPT (pick-wt=3): 1904 [] i4!=i24.
% 3.83/3.93  ** KEPT (pick-wt=3): 1905 [] i4!=i23.
% 3.83/3.93  ** KEPT (pick-wt=3): 1906 [] i4!=i22.
% 3.83/3.93  ** KEPT (pick-wt=3): 1907 [] i4!=i21.
% 3.83/3.93  ** KEPT (pick-wt=3): 1908 [] i4!=i20.
% 3.83/3.93  ** KEPT (pick-wt=3): 1909 [] i4!=i19.
% 3.83/3.93  ** KEPT (pick-wt=3): 1910 [] i4!=i18.
% 3.83/3.93  ** KEPT (pick-wt=3): 1911 [] i4!=i17.
% 3.83/3.93  ** KEPT (pick-wt=3): 1912 [] i4!=i16.
% 3.83/3.93  ** KEPT (pick-wt=3): 1913 [] i4!=i15.
% 3.83/3.93  ** KEPT (pick-wt=3): 1914 [] i4!=i14.
% 3.83/3.93  ** KEPT (pick-wt=3): 1915 [] i4!=i13.
% 3.83/3.93  ** KEPT (pick-wt=3): 1916 [] i4!=i12.
% 3.83/3.93  ** KEPT (pick-wt=3): 1917 [] i4!=i11.
% 3.83/3.93  ** KEPT (pick-wt=3): 1918 [] i4!=i10.
% 3.83/3.93  ** KEPT (pick-wt=3): 1920 [copy,1919,flip.1] i9!=i4.
% 3.83/3.93  ** KEPT (pick-wt=3): 1922 [copy,1921,flip.1] i8!=i4.
% 3.83/3.93  ** KEPT (pick-wt=3): 1924 [copy,1923,flip.1] i7!=i4.
% 3.83/3.93  ** KEPT (pick-wt=3): 1926 [copy,1925,flip.1] i6!=i4.
% 3.83/3.93  ** KEPT (pick-wt=3): 1928 [copy,1927,flip.1] i5!=i4.
% 3.83/3.93  ** KEPT (pick-wt=3): 1930 [copy,1929,flip.1] i50!=i3.
% 3.83/3.93  ** KEPT (pick-wt=3): 1932 [copy,1931,flip.1] i49!=i3.
% 3.83/3.93  ** KEPT (pick-wt=3): 1934 [copy,1933,flip.1] i48!=i3.
% 3.83/3.93  ** KEPT (pick-wt=3): 1936 [copy,1935,flip.1] i47!=i3.
% 3.83/3.93  ** KEPT (pick-wt=3): 1938 [copy,1937,flip.1] i46!=i3.
% 3.83/3.93  ** KEPT (pick-wt=3): 1940 [copy,1939,flip.1] i45!=i3.
% 3.83/3.93  ** KEPT (pick-wt=3): 1942 [copy,1941,flip.1] i44!=i3.
% 3.83/3.93  ** KEPT (pick-wt=3): 1944 [copy,1943,flip.1] i43!=i3.
% 3.83/3.93  ** KEPT (pick-wt=3): 1946 [copy,1945,flip.1] i42!=i3.
% 3.83/3.93  ** KEPT (pick-wt=3): 1948 [copy,1947,flip.1] i41!=i3.
% 3.83/3.93  ** KEPT (pick-wt=3): 1950 [copy,1949,flip.1] i40!=i3.
% 3.83/3.93  ** KEPT (pick-wt=3): 1952 [copy,1951,flip.1] i39!=i3.
% 3.83/3.93  ** KEPT (pick-wt=3): 1954 [copy,1953,flip.1] i38!=i3.
% 3.83/3.93  ** KEPT (pick-wt=3): 1956 [copy,1955,flip.1] i37!=i3.
% 3.83/3.93  ** KEPT (pick-wt=3): 1958 [copy,1957,flip.1] i36!=i3.
% 3.83/3.93  ** KEPT (pick-wt=3): 1960 [copy,1959,flip.1] i35!=i3.
% 3.83/3.93  ** KEPT (pick-wt=3): 1962 [copy,1961,flip.1] i34!=i3.
% 3.83/3.93  ** KEPT (pick-wt=3): 1964 [copy,1963,flip.1] i33!=i3.
% 3.83/3.93  ** KEPT (pick-wt=3): 1966 [copy,1965,flip.1] i32!=i3.
% 3.83/3.93  ** KEPT (pick-wt=3): 1968 [copy,1967,flip.1] i31!=i3.
% 3.83/3.93  ** KEPT (pick-wt=3): 1970 [copy,1969,flip.1] i30!=i3.
% 3.83/3.93  ** KEPT (pick-wt=3): 1971 [] i3!=i29.
% 3.83/3.93  ** KEPT (pick-wt=3): 1972 [] i3!=i28.
% 3.83/3.93  ** KEPT (pick-wt=3): 1973 [] i3!=i27.
% 3.83/3.93  ** KEPT (pick-wt=3): 1974 [] i3!=i26.
% 3.83/3.93  ** KEPT (pick-wt=3): 1975 [] i3!=i25.
% 3.83/3.93  ** KEPT (pick-wt=3): 1976 [] i3!=i24.
% 3.83/3.93  ** KEPT (pick-wt=3): 1977 [] i3!=i23.
% 3.83/3.93  ** KEPT (pick-wt=3): 1978 [] i3!=i22.
% 3.83/3.93  ** KEPT (pick-wt=3): 1979 [] i3!=i21.
% 3.83/3.93  ** KEPT (pick-wt=3): 1980 [] i3!=i20.
% 3.83/3.93  ** KEPT (pick-wt=3): 1981 [] i3!=i19.
% 3.83/3.93  ** KEPT (pick-wt=3): 1982 [] i3!=i18.
% 3.83/3.93  ** KEPT (pick-wt=3): 1983 [] i3!=i17.
% 3.83/3.93  ** KEPT (pick-wt=3): 1984 [] i3!=i16.
% 3.83/3.93  ** KEPT (pick-wt=3): 1985 [] i3!=i15.
% 3.83/3.93  ** KEPT (pick-wt=3): 1986 [] i3!=i14.
% 3.83/3.93  ** KEPT (pick-wt=3): 1987 [] i3!=i13.
% 3.83/3.93  ** KEPT (pick-wt=3): 1988 [] i3!=i12.
% 3.83/3.93  ** KEPT (pick-wt=3): 1989 [] i3!=i11.
% 3.83/3.93  ** KEPT (pick-wt=3): 1990 [] i3!=i10.
% 3.83/3.93  ** KEPT (pick-wt=3): 1992 [copy,1991,flip.1] i9!=i3.
% 3.83/3.93  ** KEPT (pick-wt=3): 1994 [copy,1993,flip.1] i8!=i3.
% 3.83/3.93  ** KEPT (pick-wt=3): 1996 [copy,1995,flip.1] i7!=i3.
% 3.83/3.93  ** KEPT (pick-wt=3): 1998 [copy,1997,flip.1] i6!=i3.
% 3.83/3.93  ** KEPT (pick-wt=3): 2000 [copy,1999,flip.1] i5!=i3.
% 3.83/3.93  ** KEPT (pick-wt=3): 2002 [copy,2001,flip.1] i4!=i3.
% 3.83/3.93  ** KEPT (pick-wt=3): 2004 [copy,2003,flip.1] i50!=i2.
% 3.83/3.93  ** KEPT (pick-wt=3): 2006 [copy,2005,flip.1] i49!=i2.
% 3.83/3.93  ** KEPT (pick-wt=3): 2008 [copy,2007,flip.1] i48!=i2.
% 3.83/3.93  ** KEPT (pick-wt=3): 2010 [copy,2009,flip.1] i47!=i2.
% 3.83/3.93  ** KEPT (pick-wt=3): 2012 [copy,2011,flip.1] i46!=i2.
% 3.83/3.93  ** KEPT (pick-wt=3): 2014 [copy,2013,flip.1] i45!=i2.
% 3.83/3.93  ** KEPT (pick-wt=3): 2016 [copy,2015,flip.1] i44!=i2.
% 3.83/3.93  ** KEPT (pick-wt=3): 2018 [copy,2017,flip.1] i43!=i2.
% 3.83/3.93  ** KEPT (pick-wt=3): 2020 [copy,2019,flip.1] i42!=i2.
% 3.83/3.93  ** KEPT (pick-wt=3): 2022 [copy,2021,flip.1] i41!=i2.
% 3.83/3.93  ** KEPT (pick-wt=3): 2024 [copy,2023,flip.1] i40!=i2.
% 3.83/3.93  ** KEPT (pick-wt=3): 2026 [copy,2025,flip.1] i39!=i2.
% 3.83/3.93  ** KEPT (pick-wt=3): 2028 [copy,2027,flip.1] i38!=i2.
% 3.83/3.93  ** KEPT (pick-wt=3): 2030 [copy,2029,flip.1] i37!=i2.
% 3.83/3.93  ** KEPT (pick-wt=3): 2032 [copy,2031,flip.1] i36!=i2.
% 3.83/3.93  ** KEPT (pick-wt=3): 2034 [copy,2033,flip.1] i35!=i2.
% 3.83/3.93  ** KEPT (pick-wt=3): 2036 [copy,2035,flip.1] i34!=i2.
% 3.83/3.93  ** KEPT (pick-wt=3): 2038 [copy,2037,flip.1] i33!=i2.
% 3.83/3.93  ** KEPT (pick-wt=3): 2040 [copy,2039,flip.1] i32!=i2.
% 3.83/3.93  ** KEPT (pick-wt=3): 2042 [copy,2041,flip.1] i31!=i2.
% 3.83/3.93  ** KEPT (pick-wt=3): 2044 [copy,2043,flip.1] i30!=i2.
% 3.83/3.93  ** KEPT (pick-wt=3): 2046 [copy,2045,flip.1] i29!=i2.
% 3.83/3.93  ** KEPT (pick-wt=3): 2048 [copy,2047,flip.1] i28!=i2.
% 3.83/3.93  ** KEPT (pick-wt=3): 2050 [copy,2049,flip.1] i27!=i2.
% 3.83/3.93  ** KEPT (pick-wt=3): 2052 [copy,2051,flip.1] i26!=i2.
% 3.83/3.93  ** KEPT (pick-wt=3): 2054 [copy,2053,flip.1] i25!=i2.
% 3.83/3.93  ** KEPT (pick-wt=3): 2056 [copy,2055,flip.1] i24!=i2.
% 3.83/3.93  ** KEPT (pick-wt=3): 2058 [copy,2057,flip.1] i23!=i2.
% 3.83/3.93  ** KEPT (pick-wt=3): 2060 [copy,2059,flip.1] i22!=i2.
% 3.83/3.93  ** KEPT (pick-wt=3): 2062 [copy,2061,flip.1] i21!=i2.
% 3.83/3.93  ** KEPT (pick-wt=3): 2064 [copy,2063,flip.1] i20!=i2.
% 3.83/3.93  ** KEPT (pick-wt=3): 2065 [] i2!=i19.
% 3.83/3.93  ** KEPT (pick-wt=3): 2066 [] i2!=i18.
% 3.83/3.93  ** KEPT (pick-wt=3): 2067 [] i2!=i17.
% 3.83/3.93  ** KEPT (pick-wt=3): 2068 [] i2!=i16.
% 3.83/3.93  ** KEPT (pick-wt=3): 2069 [] i2!=i15.
% 3.83/3.93  ** KEPT (pick-wt=3): 2070 [] i2!=i14.
% 3.83/3.93  ** KEPT (pick-wt=3): 2071 [] i2!=i13.
% 3.83/3.93  ** KEPT (pick-wt=3): 2072 [] i2!=i12.
% 3.83/3.93  ** KEPT (pick-wt=3): 2073 [] i2!=i11.
% 3.83/3.93  ** KEPT (pick-wt=3): 2074 [] i2!=i10.
% 3.83/3.93  ** KEPT (pick-wt=3): 2076 [copy,2075,flip.1] i9!=i2.
% 3.83/3.93  ** KEPT (pick-wt=3): 2078 [copy,2077,flip.1] i8!=i2.
% 3.83/3.93  ** KEPT (pick-wt=3): 2080 [copy,2079,flip.1] i7!=i2.
% 3.83/3.93  ** KEPT (pick-wt=3): 2082 [copy,2081,flip.1] i6!=i2.
% 3.83/3.93  ** KEPT (pick-wt=3): 2084 [copy,2083,flip.1] i5!=i2.
% 3.83/3.93  ** KEPT (pick-wt=3): 2086 [copy,2085,flip.1] i4!=i2.
% 3.83/3.93  ** KEPT (pick-wt=3): 2088 [copy,2087,flip.1] i3!=i2.
% 3.83/3.93  ** KEPT (pick-wt=3): 2090 [copy,2089,flip.1] i50!=i1.
% 3.83/3.93  ** KEPT (pick-wt=3): 2092 [copy,2091,flip.1] i49!=i1.
% 3.83/3.93  ** KEPT (pick-wt=3): 2094 [copy,2093,flip.1] i48!=i1.
% 3.83/3.93  ** KEPT (pick-wt=3): 2096 [copy,2095,flip.1] i47!=i1.
% 3.83/3.93  ** KEPT (pick-wt=3): 2098 [copy,2097,flip.1] i46!=i1.
% 3.83/3.93  ** KEPT (pick-wt=3): 2100 [copy,2099,flip.1] i45!=i1.
% 3.83/3.93  ** KEPT (pick-wt=3): 2102 [copy,2101,flip.1] i44!=i1.
% 3.83/3.93  ** KEPT (pick-wt=3): 2104 [copy,2103,flip.1] i43!=i1.
% 3.83/3.93  ** KEPT (pick-wt=3): 2106 [copy,2105,flip.1] i42!=i1.
% 3.83/3.93  ** KEPT (pick-wt=3): 2108 [copy,2107,flip.1] i41!=i1.
% 3.83/3.93  ** KEPT (pick-wt=3): 2110 [copy,2109,flip.1] i40!=i1.
% 3.83/3.93  ** KEPT (pick-wt=3): 2112 [copy,2111,flip.1] i39!=i1.
% 3.83/3.93  ** KEPT (pick-wt=3): 2114 [copy,2113,flip.1] i38!=i1.
% 3.83/3.93  ** KEPT (pick-wt=3): 2116 [copy,2115,flip.1] i37!=i1.
% 3.83/3.93  ** KEPT (pick-wt=3): 2118 [copy,2117,flip.1] i36!=i1.
% 3.83/3.93  ** KEPT (pick-wt=3): 2120 [copy,2119,flip.1] i35!=i1.
% 3.83/3.93  ** KEPT (pick-wt=3): 2122 [copy,2121,flip.1] i34!=i1.
% 3.83/3.93  ** KEPT (pick-wt=3): 2124 [copy,2123,flip.1] i33!=i1.
% 3.83/3.93  ** KEPT (pick-wt=3): 2126 [copy,2125,flip.1] i32!=i1.
% 3.83/3.93  ** KEPT (pick-wt=3): 2128 [copy,2127,flip.1] i31!=i1.
% 3.83/3.93  ** KEPT (pick-wt=3): 2130 [copy,2129,flip.1] i30!=i1.
% 3.83/3.93  ** KEPT (pick-wt=3): 2132 [copy,2131,flip.1] i29!=i1.
% 3.83/3.93  ** KEPT (pick-wt=3): 2134 [copy,2133,flip.1] i28!=i1.
% 3.83/3.93  ** KEPT (pick-wt=3): 2136 [copy,2135,flip.1] i27!=i1.
% 3.83/3.93  ** KEPT (pick-wt=3): 2138 [copy,2137,flip.1] i26!=i1.
% 3.83/3.93  ** KEPT (pick-wt=3): 2140 [copy,2139,flip.1] i25!=i1.
% 3.83/3.93  ** KEPT (pick-wt=3): 2142 [copy,2141,flip.1] i24!=i1.
% 3.83/3.93  ** KEPT (pick-wt=3): 2144 [copy,2143,flip.1] i23!=i1.
% 3.83/3.93  ** KEPT (pick-wt=3): 2146 [copy,2145,flip.1] i22!=i1.
% 3.83/3.93  ** KEPT (pick-wt=3): 2148 [copy,2147,flip.1] i21!=i1.
% 3.83/3.93  ** KEPT (pick-wt=3): 2150 [copy,2149,flip.1] i20!=i1.
% 3.83/3.93  ** KEPT (pick-wt=3): 2152 [copy,2151,flip.1] i19!=i1.
% 3.83/3.93  ** KEPT (pick-wt=3): 2154 [copy,2153,flip.1] i18!=i1.
% 3.83/3.93  ** KEPT (pick-wt=3): 2156 [copy,2155,flip.1] i17!=i1.
% 3.83/3.93  ** KEPT (pick-wt=3): 2158 [copy,2157,flip.1] i16!=i1.
% 3.83/3.93  ** KEPT (pick-wt=3): 2160 [copy,2159,flip.1] i15!=i1.
% 3.83/3.93  ** KEPT (pick-wt=3): 2162 [copy,2161,flip.1] i14!=i1.
% 3.83/3.93  ** KEPT (pick-wt=3): 2164 [copy,2163,flip.1] i13!=i1.
% 3.83/3.93  ** KEPT (pick-wt=3): 2166 [copy,2165,flip.1] i12!=i1.
% 3.83/3.93  ** KEPT (pick-wt=3): 2168 [copy,2167,flip.1] i11!=i1.
% 3.83/3.93  ** KEPT (pick-wt=3): 2170 [copy,2169,flip.1] i10!=i1.
% 3.83/3.93  ** KEPT (pick-wt=3): 2172 [copy,2171,flip.1] i9!=i1.
% 3.83/3.93  ** KEPT (pick-wt=3): 2174 [copy,2173,flip.1] i8!=i1.
% 3.83/3.93  ** KEPT (pick-wt=3): 2176 [copy,2175,flip.1] i7!=i1.
% 3.83/3.93  ** KEPT (pick-wt=3): 2178 [copy,2177,flip.1] i6!=i1.
% 3.83/3.93  ** KEPT (pick-wt=3): 2180 [copy,2179,flip.1] i5!=i1.
% 3.83/3.93  ** KEPT (pick-wt=3): 2182 [copy,2181,flip.1] i4!=i1.
% 3.83/3.93  ** KEPT (pick-wt=3): 2184 [copy,2183,flip.1] i3!=i1.
% 3.83/3.93  ** KEPT (pick-wt=3): 2186 [copy,2185,flip.1] i2!=i1.
% 3.83/3.93  ** KEPT (pick-wt=3): 2188 [copy,2187,flip.1] a_1799!=a_1749.
% 3.83/3.93  
% 3.83/3.93  ------------> process sos:
% 3.83/3.93  ** KEPT (pick-wt=3): 2189 [] A=A.
% 3.83/3.93  ** KEPT (pick-wt=8): 2190 [] select(store(A,B,C),B)=C.
% 3.83/3.93  ---> New Demodulator: 2191 [new_demod,2190] select(store(A,B,C),B)=C.
% 3.83/3.93  ** KEPT (pick-wt=13): 2192 [] A=B|select(store(C,A,D),B)=select(C,B).
% 3.83/3.93  ** KEPT (pick-wt=23): 2193 [] store(store(A,B,select(A,C)),C,select(A,B))=store(store(A,C,select(A,B)),B,select(A,C)).
% 3.83/3.93  ** KEPT (pick-wt=6): 2195 [copy,2194,flip.1] store(a1,i1,e1)=a_1700.
% 3.83/3.93  ---> New Demodulator: 2196 [new_demod,2195] store(a1,i1,e1)=a_1700.
% 3.83/3.93  ** KEPT (pick-wt=6): 2198 [copy,2197,flip.1] store(a_1700,i2,e2)=a_1701.
% 3.83/3.93  ---> New Demodulator: 2199 [new_demod,2198] store(a_1700,i2,e2)=a_1701.
% 3.83/3.93  ** KEPT (pick-wt=6): 2201 [copy,2200,flip.1] store(a_1701,i3,e3)=a_1702.
% 3.83/3.93  ---> New Demodulator: 2202 [new_demod,2201] store(a_1701,i3,e3)=a_1702.
% 3.83/3.93  ** KEPT (pick-wt=6): 2204 [copy,2203,flip.1] store(a_1702,i4,e4)=a_1703.
% 3.83/3.93  ---> New Demodulator: 2205 [new_demod,2204] store(a_1702,i4,e4)=a_1703.
% 3.83/3.93  ** KEPT (pick-wt=6): 2207 [copy,2206,flip.1] store(a_1703,i5,e5)=a_1704.
% 3.83/3.93  ---> New Demodulator: 2208 [new_demod,2207] store(a_1703,i5,e5)=a_1704.
% 3.83/3.93  ** KEPT (pick-wt=6): 2210 [copy,2209,flip.1] store(a_1704,i6,e6)=a_1705.
% 3.83/3.93  ---> New Demodulator: 2211 [new_demod,2210] store(a_1704,i6,e6)=a_1705.
% 3.83/3.93  ** KEPT (pick-wt=6): 2213 [copy,2212,flip.1] store(a_1705,i7,e7)=a_1706.
% 3.83/3.93  ---> New Demodulator: 2214 [new_demod,2213] store(a_1705,i7,e7)=a_1706.
% 3.83/3.93  ** KEPT (pick-wt=6): 2216 [copy,2215,flip.1] store(a_1706,i8,e8)=a_1707.
% 3.83/3.93  ---> New Demodulator: 2217 [new_demod,2216] store(a_1706,i8,e8)=a_1707.
% 3.83/3.93  ** KEPT (pick-wt=6): 2219 [copy,2218,flip.1] store(a_1707,i9,e9)=a_1708.
% 3.83/3.93  ---> New Demodulator: 2220 [new_demod,2219] store(a_1707,i9,e9)=a_1708.
% 3.83/3.93  ** KEPT (pick-wt=6): 2222 [copy,2221,flip.1] store(a_1708,i10,e10)=a_1709.
% 3.83/3.93  ---> New Demodulator: 2223 [new_demod,2222] store(a_1708,i10,e10)=a_1709.
% 3.83/3.93  ** KEPT (pick-wt=6): 2225 [copy,2224,flip.1] store(a_1709,i11,e11)=a_1710.
% 3.83/3.93  ---> New Demodulator: 2226 [new_demod,2225] store(a_1709,i11,e11)=a_1710.
% 3.83/3.93  ** KEPT (pick-wt=6): 2228 [copy,2227,flip.1] store(a_1710,i12,e12)=a_1711.
% 3.83/3.93  ---> New Demodulator: 2229 [new_demod,2228] store(a_1710,i12,e12)=a_1711.
% 3.83/3.93  ** KEPT (pick-wt=6): 2231 [copy,2230,flip.1] store(a_1711,i13,e13)=a_1712.
% 3.83/3.93  ---> New Demodulator: 2232 [new_demod,2231] store(a_1711,i13,e13)=a_1712.
% 3.83/3.93  ** KEPT (pick-wt=6): 2234 [copy,2233,flip.1] store(a_1712,i14,e14)=a_1713.
% 3.83/3.93  ---> New Demodulator: 2235 [new_demod,2234] store(a_1712,i14,e14)=a_1713.
% 3.83/3.93  ** KEPT (pick-wt=6): 2237 [copy,2236,flip.1] store(a_1713,i15,e15)=a_1714.
% 3.83/3.93  ---> New Demodulator: 2238 [new_demod,2237] store(a_1713,i15,e15)=a_1714.
% 3.83/3.93  ** KEPT (pick-wt=6): 2240 [copy,2239,flip.1] store(a_1714,i16,e16)=a_1715.
% 3.83/3.93  ---> New Demodulator: 2241 [new_demod,2240] store(a_1714,i16,e16)=a_1715.
% 3.83/3.93  ** KEPT (pick-wt=6): 2243 [copy,2242,flip.1] store(a_1715,i17,e17)=a_1716.
% 3.83/3.93  ---> New Demodulator: 2244 [new_demod,2243] store(a_1715,i17,e17)=a_1716.
% 3.83/3.93  ** KEPT (pick-wt=6): 2246 [copy,2245,flip.1] store(a_1716,i18,e18)=a_1717.
% 3.83/3.93  ---> New Demodulator: 2247 [new_demod,2246] store(a_1716,i18,e18)=a_1717.
% 3.83/3.93  ** KEPT (pick-wt=6): 2249 [copy,2248,flip.1] store(a_1717,i19,e19)=a_1718.
% 3.83/3.93  ---> New Demodulator: 2250 [new_demod,2249] store(a_1717,i19,e19)=a_1718.
% 3.83/3.93  ** KEPT (pick-wt=6): 2252 [copy,2251,flip.1] store(a_1718,i20,e20)=a_1719.
% 3.83/3.93  ---> New Demodulator: 2253 [new_demod,2252] store(a_1718,i20,e20)=a_1719.
% 3.83/3.93  ** KEPT (pick-wt=6): 2255 [copy,2254,flip.1] store(a_1719,i21,e21)=a_1720.
% 3.83/3.93  ---> New Demodulator: 2256 [new_demod,2255] store(a_1719,i21,e21)=a_1720.
% 3.83/3.93  ** KEPT (pick-wt=6): 2258 [copy,2257,flip.1] store(a_1720,i22,e22)=a_1721.
% 3.83/3.93  ---> New Demodulator: 2259 [new_demod,2258] store(a_1720,i22,e22)=a_1721.
% 3.83/3.93  ** KEPT (pick-wt=6): 2261 [copy,2260,flip.1] store(a_1721,i23,e23)=a_1722.
% 3.83/3.93  ---> New Demodulator: 2262 [new_demod,2261] store(a_1721,i23,e23)=a_1722.
% 3.83/3.93  ** KEPT (pick-wt=6): 2264 [copy,2263,flip.1] store(a_1722,i24,e24)=a_1723.
% 3.83/3.93  ---> New Demodulator: 2265 [new_demod,2264] store(a_1722,i24,e24)=a_1723.
% 3.83/3.93  ** KEPT (pick-wt=6): 2267 [copy,2266,flip.1] store(a_1723,i25,e25)=a_1724.
% 3.83/3.93  ---> New Demodulator: 2268 [new_demod,2267] store(a_1723,i25,e25)=a_1724.
% 3.83/3.93  ** KEPT (pick-wt=6): 2270 [copy,2269,flip.1] store(a_1724,i26,e26)=a_1725.
% 3.83/3.93  ---> New Demodulator: 2271 [new_demod,2270] store(a_1724,i26,e26)=a_1725.
% 3.83/3.93  ** KEPT (pick-wt=6): 2273 [copy,2272,flip.1] store(a_1725,i27,e27)=a_1726.
% 3.83/3.93  ---> New Demodulator: 2274 [new_demod,2273] store(a_1725,i27,e27)=a_1726.
% 3.83/3.93  ** KEPT (pick-wt=6): 2276 [copy,2275,flip.1] store(a_1726,i28,e28)=a_1727.
% 3.83/3.93  ---> New Demodulator: 2277 [new_demod,2276] store(a_1726,i28,e28)=a_1727.
% 3.83/3.93  ** KEPT (pick-wt=6): 2279 [copy,2278,flip.1] store(a_1727,i29,e29)=a_1728.
% 3.83/3.93  ---> New Demodulator: 2280 [new_demod,2279] store(a_1727,i29,e29)=a_1728.
% 3.83/3.93  ** KEPT (pick-wt=6): 2282 [copy,2281,flip.1] store(a_1728,i30,e30)=a_1729.
% 3.83/3.93  ---> New Demodulator: 2283 [new_demod,2282] store(a_1728,i30,e30)=a_1729.
% 3.83/3.93  ** KEPT (pick-wt=6): 2285 [copy,2284,flip.1] store(a_1729,i31,e31)=a_1730.
% 3.83/3.93  ---> New Demodulator: 2286 [new_demod,2285] store(a_1729,i31,e31)=a_1730.
% 3.83/3.93  ** KEPT (pick-wt=6): 2288 [copy,2287,flip.1] store(a_1730,i32,e32)=a_1731.
% 3.83/3.93  ---> New Demodulator: 2289 [new_demod,2288] store(a_1730,i32,e32)=a_1731.
% 3.83/3.93  ** KEPT (pick-wt=6): 2291 [copy,2290,flip.1] store(a_1731,i33,e33)=a_1732.
% 3.83/3.93  ---> New Demodulator: 2292 [new_demod,2291] store(a_1731,i33,e33)=a_1732.
% 3.83/3.93  ** KEPT (pick-wt=6): 2294 [copy,2293,flip.1] store(a_1732,i34,e34)=a_1733.
% 3.83/3.93  ---> New Demodulator: 2295 [new_demod,2294] store(a_1732,i34,e34)=a_1733.
% 3.83/3.93  ** KEPT (pick-wt=6): 2297 [copy,2296,flip.1] store(a_1733,i35,e35)=a_1734.
% 3.83/3.93  ---> New Demodulator: 2298 [new_demod,2297] store(a_1733,i35,e35)=a_1734.
% 3.83/3.93  ** KEPT (pick-wt=6): 2300 [copy,2299,flip.1] store(a_1734,i36,e36)=a_1735.
% 3.83/3.93  ---> New Demodulator: 2301 [new_demod,2300] store(a_1734,i36,e36)=a_1735.
% 3.83/3.93  ** KEPT (pick-wt=6): 2303 [copy,2302,flip.1] store(a_1735,i37,e37)=a_1736.
% 3.83/3.93  ---> New Demodulator: 2304 [new_demod,2303] store(a_1735,i37,e37)=a_1736.
% 3.83/3.93  ** KEPT (pick-wt=6): 2306 [copy,2305,flip.1] store(a_1736,i38,e38)=a_1737.
% 3.83/3.93  ---> New Demodulator: 2307 [new_demod,2306] store(a_1736,i38,e38)=a_1737.
% 3.83/3.93  ** KEPT (pick-wt=6): 2309 [copy,2308,flip.1] store(a_1737,i39,e39)=a_1738.
% 3.83/3.93  ---> New Demodulator: 2310 [new_demod,2309] store(a_1737,i39,e39)=a_1738.
% 3.83/3.93  ** KEPT (pick-wt=6): 2312 [copy,2311,flip.1] store(a_1738,i40,e40)=a_1739.
% 3.83/3.93  ---> New Demodulator: 2313 [new_demod,2312] store(a_1738,i40,e40)=a_1739.
% 3.83/3.93  ** KEPT (pick-wt=6): 2315 [copy,2314,flip.1] store(a_1739,i41,e41)=a_1740.
% 3.83/3.93  ---> New Demodulator: 2316 [new_demod,2315] store(a_1739,i41,e41)=a_1740.
% 3.83/3.93  ** KEPT (pick-wt=6): 2318 [copy,2317,flip.1] store(a_1740,i42,e42)=a_1741.
% 3.83/3.93  ---> New Demodulator: 2319 [new_demod,2318] store(a_1740,i42,e42)=a_1741.
% 3.83/3.93  ** KEPT (pick-wt=6): 2321 [copy,2320,flip.1] store(a_1741,i43,e43)=a_1742.
% 3.83/3.93  ---> New Demodulator: 2322 [new_demod,2321] store(a_1741,i43,e43)=a_1742.
% 3.83/3.93  ** KEPT (pick-wt=6): 2324 [copy,2323,flip.1] store(a_1742,i44,e44)=a_1743.
% 3.83/3.93  ---> New Demodulator: 2325 [new_demod,2324] store(a_1742,i44,e44)=a_1743.
% 3.83/3.93  ** KEPT (pick-wt=6): 2327 [copy,2326,flip.1] store(a_1743,i45,e45)=a_1744.
% 3.83/3.93  ---> New Demodulator: 2328 [new_demod,2327] store(a_1743,i45,e45)=a_1744.
% 3.83/3.93  ** KEPT (pick-wt=6): 2330 [copy,2329,flip.1] store(a_1744,i46,e46)=a_1745.
% 3.83/3.93  ---> New Demodulator: 2331 [new_demod,2330] store(a_1744,i46,e46)=a_1745.
% 3.83/3.93  ** KEPT (pick-wt=6): 2333 [copy,2332,flip.1] store(a_1745,i47,e47)=a_1746.
% 3.83/3.93  ---> New Demodulator: 2334 [new_demod,2333] store(a_1745,i47,e47)=a_1746.
% 3.83/3.93  ** KEPT (pick-wt=6): 2336 [copy,2335,flip.1] store(a_1746,i48,e48)=a_1747.
% 3.83/3.93  ---> New Demodulator: 2337 [new_demod,2336] store(a_1746,i48,e48)=a_1747.
% 3.83/3.93  ** KEPT (pick-wt=6): 2339 [copy,2338,flip.1] store(a_1747,i49,e49)=a_1748.
% 3.83/3.93  ---> New Demodulator: 2340 [new_demod,2339] store(a_1747,i49,e49)=a_1748.
% 3.83/3.93  ** KEPT (pick-wt=6): 2342 [copy,2341,flip.1] store(a_1748,i1,e1)=a_1749.
% 3.83/3.93  ---> New Demodulator: 2343 [new_demod,2342] store(a_1748,i1,e1)=a_1749.
% 3.83/3.93  ** KEPT (pick-wt=6): 2345 [copy,2344,flip.1] store(a1,i41,e41)=a_1750.
% 3.83/3.93  ---> New Demodulator: 2346 [new_demod,2345] store(a1,i41,e41)=a_1750.
% 3.83/3.93  ** KEPT (pick-wt=6): 2348 [copy,2347,flip.1] store(a_1750,i30,e30)=a_1751.
% 3.83/3.93  ---> New Demodulator: 2349 [new_demod,2348] store(a_1750,i30,e30)=a_1751.
% 3.83/3.93  ** KEPT (pick-wt=6): 2351 [copy,2350,flip.1] store(a_1751,i45,e45)=a_1752.
% 3.83/3.93  ---> New Demodulator: 2352 [new_demod,2351] store(a_1751,i45,e45)=a_1752.
% 3.83/3.93  ** KEPT (pick-wt=6): 2354 [copy,2353,flip.1] store(a_1752,i43,e43)=a_1753.
% 3.83/3.93  ---> New Demodulator: 2355 [new_demod,2354] store(a_1752,i43,e43)=a_1753.
% 3.83/3.93  ** KEPT (pick-wt=6): 2357 [copy,2356,flip.1] store(a_1753,i28,e28)=a_1754.
% 3.83/3.93  ---> New Demodulator: 2358 [new_demod,2357] store(a_1753,i28,e28)=a_1754.
% 3.83/3.93  ** KEPT (pick-wt=6): 2360 [copy,2359,flip.1] store(a_1754,i19,e19)=a_1755.
% 3.83/3.93  ---> New Demodulator: 2361 [new_demod,2360] store(a_1754,i19,e19)=a_1755.
% 3.83/3.93  ** KEPT (pick-wt=6): 2363 [copy,2362,flip.1] store(a_1755,i22,e22)=a_1756.
% 3.83/3.93  ---> New Demodulator: 2364 [new_demod,2363] store(a_1755,i22,e22)=a_1756.
% 3.83/3.93  ** KEPT (pick-wt=6): 2366 [copy,2365,flip.1] store(a_1756,i39,e39)=a_1757.
% 3.83/3.93  ---> New Demodulator: 2367 [new_demod,2366] store(a_1756,i39,e39)=a_1757.
% 3.83/3.93  ** KEPT (pick-wt=6): 2369 [copy,2368,flip.1] store(a_1757,i20,e20)=a_1758.
% 3.83/3.93  ---> New Demodulator: 2370 [new_demod,2369] store(a_1757,i20,e20)=a_1758.
% 3.83/3.93  ** KEPT (pick-wt=6): 2372 [copy,2371,flip.1] store(a_1758,i40,e40)=a_1759.
% 3.83/3.93  ---> New Demodulator: 2373 [new_demod,2372] store(a_1758,i40,e40)=a_1759.
% 3.83/3.93  ** KEPT (pick-wt=6): 2375 [copy,2374,flip.1] store(a_1759,i16,e16)=a_1760.
% 3.83/3.93  ---> New Demodulator: 2376 [new_demod,2375] store(a_1759,i16,e16)=a_1760.
% 3.83/3.93  ** KEPT (pick-wt=6): 2378 [copy,2377,flip.1] store(a_1760,i8,e8)=a_1761.
% 3.83/3.93  ---> New Demodulator: 2379 [new_demod,2378] store(a_1760,i8,e8)=a_1761.
% 3.83/3.93  ** KEPT (pick-wt=6): 2381 [copy,2380,flip.1] store(a_1761,i49,e49)=a_1762.
% 3.83/3.93  ---> New Demodulator: 2382 [new_demod,2381] store(a_1761,i49,e49)=a_1762.
% 3.83/3.93  ** KEPT (pick-wt=6): 2384 [copy,2383,flip.1] store(a_1762,i14,e14)=a_1763.
% 3.83/3.93  ---> New Demodulator: 2385 [new_demod,2384] store(a_1762,i14,e14)=a_1763.
% 3.83/3.93  ** KEPT (pick-wt=6): 2387 [copy,2386,flip.1] store(a_1763,i13,e13)=a_1764.
% 3.83/3.93  ---> New Demodulator: 2388 [new_demod,2387] store(a_1763,i13,e13)=a_1764.
% 3.83/3.93  ** KEPT (pick-wt=6): 2390 [copy,2389,flip.1] store(a_1764,i6,e6)=a_1765.
% 3.83/3.93  ---> New Demodulator: 2391 [new_demod,2390] store(a_1764,i6,e6)=a_1765.
% 3.83/3.93  ** KEPT (pick-wt=6): 2393 [copy,2392,flip.1] store(a_1765,i27,e27)=a_1766.
% 3.83/3.93  ---> New Demodulator: 2394 [new_demod,2393] store(a_1765,i27,e27)=a_1766.
% 3.83/3.93  ** KEPT (pick-wt=6): 2396 [copy,2395,flip.1] store(a_1766,i15,e15)=a_1767.
% 3.83/3.93  ---> New Demodulator: 2397 [new_demod,2396] store(a_1766,i15,e15)=a_1767.
% 3.83/3.93  ** KEPT (pick-wt=6): 2399 [copy,2398,flip.1] store(a_1767,i7,e7)=a_1768.
% 3.83/3.93  ---> New Demodulator: 2400 [new_demod,2399] store(a_1767,i7,e7)=a_1768.
% 3.83/3.93  ** KEPT (pick-wt=6): 2402 [copy,2401,flip.1] store(a_1768,i33,e33)=a_1769.
% 3.83/3.93  ---> New Demodulator: 2403 [new_demod,2402] store(a_1768,i33,e33)=a_1769.
% 3.83/3.93  ** KEPT (pick-wt=6): 2405 [copy,2404,flip.1] store(a_1769,i9,e9)=a_1770.
% 3.83/3.93  ---> New Demodulator: 2406 [new_demod,2405] store(a_1769,i9,e9)=a_1770.
% 3.83/3.93  ** KEPT (pick-wt=6): 2408 [copy,2407,flip.1] store(a_1770,i17,e17)=a_1771.
% 3.83/3.93  ---> New Demodulator: 2409 [new_demod,2408] store(a_1770,i17,e17)=a_1771.
% 3.83/3.93  ** KEPT (pick-wt=6): 2411 [copy,2410,flip.1] store(a_1771,i42,e42)=a_1772.
% 3.83/3.93  ---> New Demodulator: 2412 [new_demod,2411] store(a_1771,i42,e42)=a_1772.
% 3.83/3.93  ** KEPT (pick-wt=6): 2414 [copy,2413,flip.1] store(a_1772,i47,e47)=a_1773.
% 3.83/3.93  ---> New Demodulator: 2415 [new_demod,2414] store(a_1772,i47,e47)=a_1773.
% 3.83/3.93  ** KEPT (pick-wt=6): 2417 [copy,2416,flip.1] store(a_1773,i18,e18)=a_1774.
% 3.83/3.93  ---> New Demodulator: 2418 [new_demod,2417] store(a_1773,i18,e18)=a_1774.
% 3.83/3.93  ** KEPT (pick-wt=6): 2420 [copy,2419,flip.1] store(a_1774,i26,e26)=a_1775.
% 3.83/3.93  ---> New Demodulator: 2421 [new_demod,2420] store(a_1774,i26,e26)=a_1775.
% 3.83/3.93  ** KEPT (pick-wt=6): 2423 [copy,2422,flip.1] store(a_1775,i34,e34)=a_1776.
% 3.83/3.93  ---> New Demodulator: 2424 [new_demod,2423] store(a_1775,i34,e34)=a_1776.
% 3.83/3.93  ** KEPT (pick-wt=6): 2426 [copy,2425,flip.1] store(a_1776,i11,e11)=a_1777.
% 3.83/3.93  ---> New Demodulator: 2427 [new_demod,2426] store(a_1776,i11,e11)=a_1777.
% 3.83/3.93  ** KEPT (pick-wt=6): 2429 [copy,2428,flip.1] store(a_1777,i36,e36)=a_1778.
% 3.83/3.93  ---> New Demodulator: 2430 [new_demod,2429] store(a_1777,i36,e36)=a_1778.
% 3.83/3.93  ** KEPT (pick-wt=6): 2432 [copy,2431,flip.1] store(a_1778,i44,e44)=a_1779.
% 3.83/3.93  ---> New Demodulator: 2433 [new_demod,2432] store(a_1778,i44,e44)=a_1779.
% 3.83/3.93  ** KEPT (pick-wt=6): 2435 [copy,2434,flip.1] store(a_1779,i38,e38)=a_1780.
% 3.83/3.93  ---> New Demodulator: 2436 [new_demod,2435] store(a_1779,i38,e38)=a_1780.
% 3.83/3.93  ** KEPT (pick-wt=6): 2438 [copy,2437,flip.1] store(a_1780,i23,e23)=a_1781.
% 3.83/3.93  ---> New Demodulator: 2439 [new_demod,2438] store(a_1780,i23,e23)=a_1781.
% 3.83/3.93  ** KEPT (pick-wt=6): 2441 [copy,2440,flip.1] store(a_1781,i25,e25)=a_1782.
% 3.83/3.93  ---> New Demodulator: 2442 [new_demod,2441] store(a_1781,i25,e25)=a_1782.
% 3.83/3.93  ** KEPT (pick-wt=6): 2444 [copy,2443,flip.1] store(a_1782,i46,e46)=a_1783.
% 3.83/3.93  ---> New Demodulator: 2445 [new_demod,2444] store(a_1782,i46,e46)=a_1783.
% 3.83/3.93  ** KEPT (pick-wt=6): 2447 [copy,2446,flip.1] store(a_1783,i35,e35)=a_1784.
% 3.83/3.93  ---> New Demodulator: 2448 [new_demod,2447] store(a_1783,i35,e35)=a_1784.
% 3.83/3.93  ** KEPT (pick-wt=6): 2450 [copy,2449,flip.1] store(a_1784,i50,e50)=a_1785.
% 3.83/3.93  ---> New Demodulator: 2451 [new_demod,2450] store(a_1784,i50,e50)=a_1785.
% 3.83/3.93  ** KEPT (pick-wt=6): 2453 [copy,2452,flip.1] store(a_1785,i2,e2)=a_1786.
% 3.83/3.93  ---> New Demodulator: 2454 [new_demod,2453] store(a_1785,i2,e2)=a_1786.
% 3.83/3.93  ** KEPT (pick-wt=6): 2456 [copy,2455,flip.1] store(a_1786,i10,e10)=a_1787.
% 3.83/3.93  ---> New Demodulator: 2457 [new_demod,2456] store(a_1786,i10,e10)=a_1787.
% 3.83/3.93  ** KEPT (pick-wt=6): 2459 [copy,2458,flip.1] store(a_1787,i48,e48)=a_1788.
% 3.83/3.93  ---> New Demodulator: 2460 [new_demod,2459] store(a_1787,i48,e48)=a_1788.
% 3.83/3.93  ** KEPT (pick-wt=6): 2462 [copy,2461,flip.1] store(a_1788,i29,e29)=a_1789.
% 3.83/3.93  ---> New Demodulator: 2463 [new_demod,2462] store(a_1788,i29,e29)=a_1789.
% 3.83/3.93  ** KEPT (pick-wt=6): 2465 [copy,2464,flip.1] store(a_1789,i3,e3)=a_1790.
% 3.83/3.93  ---> New Demodulator: 2466 [new_demod,2465] store(a_1789,i3,e3)=a_1790.
% 3.83/3.93  ** KEPT (pick-wt=6): 2468 [copy,2467,flip.1] store(a_1790,i37,e37)=a_1791.
% 3.83/3.93  ---> New Demodulator: 2469 [new_demod,2468] store(a_1790,i37,e37)=a_1791.
% 3.83/3.93  ** KEPT (pick-wt=6): 2471 [copy,2470,flip.1] store(a_1791,i12,e12)=a_1792.
% 3.83/3.93  ---> New Demodulator: 2472 [new_demod,2471] store(a_1791,i12,e12)=a_1792.
% 3.83/3.93  ** KEPT (pick-wt=6): 2474 [copy,2473,flip.1] store(a_1792,i5,e5)=a_1793.
% 3.83/3.93  ---> New Demodulator: 2475 [new_demod,2474] store(a_1792,i5,e5)=a_1793.
% 3.83/3.93  ** KEPT (pick-wt=6): 2477 [copy,2476,flip.1] store(a_1793,i32,e32)=a_1794.
% 3.83/3.93  ---> New Demodulator: 2478 [new_demod,2477] store(a_1793,i32,e32)=a_1794.
% 3.83/3.93  ** KEPT (pick-wt=6): 2480 [copy,2479,flip.1] store(a_1794,i4,e4)=a_1795.
% 3.83/3.93  ---> New Demodulator: 2481 [new_demod,2480] store(a_1794,i4,e4)=a_1795.
% 3.83/3.93  ** KEPT (pick-wt=6): 2483 [copy,2482,flip.1] store(a_1795,i24,e24)=a_1796.
% 3.83/3.93  ---> New Demodulator: 2484 [new_demod,2483] store(a_1795,i24,e24)=a_1796.
% 3.83/3.93  ** KEPT (pick-wt=6): 2486 [copy,2485,flip.1] store(a_1796,i21,e21)=a_1797.
% 3.83/3.93  ---> New Demodulator: 2487 [new_demod,2486] store(a_1796,i21,e21)=a_1797.
% 3.83/3.93  ** KEPT (pick-wt=6): 2489 [copy,2488,flip.1] store(a_1797,i31,e31)=a_1798.
% 3.83/3.93  ---> New Demodulator: 2490 [new_demod,2489] store(a_1797,i31,e31)=a_1798.
% 3.83/3.93  ** KEPT (pick-wt=6): 2492 [copy,2491,flip.1] store(a_1798,i1,e1)=a_1799.
% 3.83/3.93  ---> New Demodulator: 2493 [new_demod,2492] store(a_1798,i1,e1)=a_1799.
% 3.83/3.93    Following clause subsumed by 2189 during input processing: 0 [copy,2189,flip.1] A=A.
% 3.83/3.93  >>>> Starting back demodulation with 2191.
% 3.83/3.93    Following clause subsumed by 2193 during input processing: 0 [copy,2193,flip.1] store(store(A,B,select(A,C)),C,select(A,B))=store(store(A,C,select(A,B)),B,select(A,C)).
% 3.83/3.93  >>>> Starting back demodulation with 2196.
% 3.83/3.93  >>>> Starting back demodulation with 2199.
% 3.83/3.93  >>>> Starting back demodulation with 2202.
% 3.83/3.93  >>>> Starting back demodulation with 2205.
% 3.83/3.93  >>>> Starting back demodulation with 2208.
% 3.83/3.93  >>>> Starting back demodulation with 2211.
% 3.83/3.93  >>>> Starting back demodulation with 2214.
% 3.83/3.93  >>>> Starting back demodulation with 2217.
% 3.83/3.93  >>>> Starting back demodulation with 2220.
% 3.83/3.93  >>>> Starting back demodulation with 2223.
% 3.83/3.93  >>>> Starting back demodulation with 2226.
% 3.83/3.93  >>>> Starting back demodulation with 2229.
% 3.83/3.93  >>>> Starting back demodulation with 2232.
% 3.83/3.93  >>>> Starting back demodulation with 2235.
% 3.83/3.93  >>>> Starting back demodulation with 2238.
% 3.83/3.93  >>>> Starting back demodulation with 2241.
% 3.83/3.93  >>>> Starting back demodulation with 2244.
% 3.83/3.93  >>>> Starting back demodulation with 2247.
% 3.83/3.93  >>>> Starting back demodulation with 2250.
% 3.83/3.93  >>>> Starting back demodulation with 2253.
% 3.83/3.93  >>>> Starting back demodulation with 2256.
% 3.83/3.93  >>>> Starting back demodulation with 2259.
% 3.83/3.93  >>>> Starting back demodulation with 2262.
% 3.83/3.93  >>>> Starting back demodulation with 2265.
% 3.83/3.93  >>>> Starting back demodulation with 2268.
% 3.83/3.93  >>>> Starting back demodulation with 2271.
% 3.83/3.93  >>>> Starting back demodulation with 2274.
% 3.83/3.93  >>>> Starting back demodulation with 2277.
% 3.83/3.93  >>>> Starting back demodulation with 2280.
% 3.83/3.93  >>>> Starting back demodulation with 2283.
% 3.83/3.93  >>>> Starting back demodulation with 2286.
% 3.83/3.93  >>>> Starting back demodulation with 2289.
% 3.83/3.93  >>>> Starting back demodulation with 2292.
% 3.83/3.93  >>>> Starting back demodulation with 2295.
% 3.83/3.93  >>>> Starting back demodulation with 2298.
% 3.83/3.93  >>>> Starting back demodulation with 2301.
% 3.83/3.93  >>>> Starting back demodulation with 2304.
% 3.83/3.93  >>>> Starting back demodulation with 2307.
% 3.83/3.93  >>>> Starting back demodulation with 2310.
% 3.83/3.93  >>>> Starting back demodulation with 2313.
% 3.83/3.93  >>>> Starting back demodulation with 2316.
% 3.83/3.93  >>>> Starting back demodulation with 2319.
% 3.83/3.93  >>>> Starting back demodulation with 2322.
% 3.83/3.93  >>>> Starting back demodulation with 2325.
% 3.83/3.93  >>>> Starting back demodulation with 2328.
% 3.83/3.93  >>>> Starting back demodulation with 2331.
% 3.83/3.93  >>>> Starting back demodulation with 2334.
% 3.83/3.93  >>>> Starting back demodulation with 2337.
% 3.83/3.93  >>>> Starting back demodulation with 2340.
% 3.83/3.93  >>>> Starting back demodulation with 2343.
% 3.83/3.93  >>>> Starting back demodulation with 2346.
% 3.83/3.93  >>>> Starting back demodulation with 2349.
% 4.99/5.09  >>>> Starting back demodulation with 2352.
% 4.99/5.09  >>>> Starting back demodulation with 2355.
% 4.99/5.09  >>>> Starting back demodulation with 2358.
% 4.99/5.09  >>>> Starting back demodulation with 2361.
% 4.99/5.09  >>>> Starting back demodulation with 2364.
% 4.99/5.09  >>>> Starting back demodulation with 2367.
% 4.99/5.09  >>>> Starting back demodulation with 2370.
% 4.99/5.09  >>>> Starting back demodulation with 2373.
% 4.99/5.09  >>>> Starting back demodulation with 2376.
% 4.99/5.09  >>>> Starting back demodulation with 2379.
% 4.99/5.09  >>>> Starting back demodulation with 2382.
% 4.99/5.09  >>>> Starting back demodulation with 2385.
% 4.99/5.09  >>>> Starting back demodulation with 2388.
% 4.99/5.09  >>>> Starting back demodulation with 2391.
% 4.99/5.09  >>>> Starting back demodulation with 2394.
% 4.99/5.09  >>>> Starting back demodulation with 2397.
% 4.99/5.09  >>>> Starting back demodulation with 2400.
% 4.99/5.09  >>>> Starting back demodulation with 2403.
% 4.99/5.09  >>>> Starting back demodulation with 2406.
% 4.99/5.09  >>>> Starting back demodulation with 2409.
% 4.99/5.09  >>>> Starting back demodulation with 2412.
% 4.99/5.09  >>>> Starting back demodulation with 2415.
% 4.99/5.09  >>>> Starting back demodulation with 2418.
% 4.99/5.09  >>>> Starting back demodulation with 2421.
% 4.99/5.09  >>>> Starting back demodulation with 2424.
% 4.99/5.09  >>>> Starting back demodulation with 2427.
% 4.99/5.09  >>>> Starting back demodulation with 2430.
% 4.99/5.09  >>>> Starting back demodulation with 2433.
% 4.99/5.09  >>>> Starting back demodulation with 2436.
% 4.99/5.09  >>>> Starting back demodulation with 2439.
% 4.99/5.09  >>>> Starting back demodulation with 2442.
% 4.99/5.09  >>>> Starting back demodulation with 2445.
% 4.99/5.09  >>>> Starting back demodulation with 2448.
% 4.99/5.09  >>>> Starting back demodulation with 2451.
% 4.99/5.09  >>>> Starting back demodulation with 2454.
% 4.99/5.09  >>>> Starting back demodulation with 2457.
% 4.99/5.09  >>>> Starting back demodulation with 2460.
% 4.99/5.09  >>>> Starting back demodulation with 2463.
% 4.99/5.09  >>>> Starting back demodulation with 2466.
% 4.99/5.09  >>>> Starting back demodulation with 2469.
% 4.99/5.09  >>>> Starting back demodulation with 2472.
% 4.99/5.09  >>>> Starting back demodulation with 2475.
% 4.99/5.09  >>>> Starting back demodulation with 2478.
% 4.99/5.09  >>>> Starting back demodulation with 2481.
% 4.99/5.09  >>>> Starting back demodulation with 2484.
% 4.99/5.09  >>>> Starting back demodulation with 2487.
% 4.99/5.09  >>>> Starting back demodulation with 2490.
% 4.99/5.09  >>>> Starting back demodulation with 2493.
% 4.99/5.09  
% 4.99/5.09  ======= end of input processing =======
% 4.99/5.09  
% 4.99/5.09  =========== start of search ===========
% 4.99/5.09  
% 4.99/5.09  
% 4.99/5.09  Resetting weight limit to 10.
% 4.99/5.09  
% 4.99/5.09  
% 4.99/5.09  Resetting weight limit to 10.
% 4.99/5.09  
% 4.99/5.09  sos_size=2577
% 4.99/5.09  
% 4.99/5.09  Search stopped in tp_alloc by max_mem option.
% 4.99/5.09  
% 4.99/5.09  Search stopped in tp_alloc by max_mem option.
% 4.99/5.09  
% 4.99/5.09  ============ end of search ============
% 4.99/5.09  
% 4.99/5.09  -------------- statistics -------------
% 4.99/5.09  clauses given               4631
% 4.99/5.09  clauses generated         122468
% 4.99/5.09  clauses kept                9902
% 4.99/5.09  clauses forward subsumed   17106
% 4.99/5.09  clauses back subsumed          8
% 4.99/5.09  Kbytes malloced            11718
% 4.99/5.09  
% 4.99/5.09  ----------- times (seconds) -----------
% 4.99/5.09  user CPU time          1.19          (0 hr, 0 min, 1 sec)
% 4.99/5.09  system CPU time        0.01          (0 hr, 0 min, 0 sec)
% 4.99/5.09  wall-clock time        4             (0 hr, 0 min, 4 sec)
% 4.99/5.09  
% 4.99/5.09  Process 2995 finished Wed Jul 27 05:41:06 2022
% 4.99/5.09  Otter interrupted
% 4.99/5.09  PROOF NOT FOUND
%------------------------------------------------------------------------------