Otter---3.3.UNK-Non.f

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

% Computer : n010.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:13 EDT 2022

% Result   : Unknown 27.54s 27.74s
% Output   : None 
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.10/0.12  % Problem  : SWV568-1.030 : TPTP v8.1.0. Released v4.0.0.
% 0.10/0.12  % Command  : otter-tptp-script %s
% 0.12/0.33  % Computer : n010.cluster.edu
% 0.12/0.33  % Model    : x86_64 x86_64
% 0.12/0.33  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33  % Memory   : 8042.1875MB
% 0.12/0.33  % OS       : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33  % CPULimit : 300
% 0.12/0.33  % WCLimit  : 300
% 0.12/0.33  % DateTime : Wed Jul 27 06:04:54 EDT 2022
% 0.12/0.33  % CPUTime  : 
% 2.42/2.64  ----- Otter 3.3f, August 2004 -----
% 2.42/2.64  The process was started by sandbox on n010.cluster.edu,
% 2.42/2.64  Wed Jul 27 06:04:55 2022
% 2.42/2.64  The command was "./otter".  The process ID is 15662.
% 2.42/2.64  
% 2.42/2.64  set(prolog_style_variables).
% 2.42/2.64  set(auto).
% 2.42/2.64     dependent: set(auto1).
% 2.42/2.64     dependent: set(process_input).
% 2.42/2.64     dependent: clear(print_kept).
% 2.42/2.64     dependent: clear(print_new_demod).
% 2.42/2.64     dependent: clear(print_back_demod).
% 2.42/2.64     dependent: clear(print_back_sub).
% 2.42/2.64     dependent: set(control_memory).
% 2.42/2.64     dependent: assign(max_mem, 12000).
% 2.42/2.64     dependent: assign(pick_given_ratio, 4).
% 2.42/2.64     dependent: assign(stats_level, 1).
% 2.42/2.64     dependent: assign(max_seconds, 10800).
% 2.42/2.64  clear(print_given).
% 2.42/2.64  
% 2.42/2.64  list(usable).
% 2.42/2.64  0 [] A=A.
% 2.42/2.64  0 [] select(store(A,I,E),I)=E.
% 2.42/2.64  0 [] I=J|select(store(A,I,E),J)=select(A,J).
% 2.42/2.64  0 [] rselect_se_q(rstore_se_q(A,E))=E.
% 2.42/2.64  0 [] rselect_head(rstore_head(A,E))=E.
% 2.42/2.64  0 [] rselect_tail(rstore_tail(A,E))=E.
% 2.42/2.64  0 [] rselect_se_q(rstore_head(A,E))=rselect_se_q(A).
% 2.42/2.64  0 [] rselect_se_q(rstore_tail(A,E))=rselect_se_q(A).
% 2.42/2.64  0 [] rselect_head(rstore_tail(A,E))=rselect_head(A).
% 2.42/2.64  0 [] rselect_head(rstore_se_q(A,E))=rselect_head(A).
% 2.42/2.64  0 [] rselect_tail(rstore_se_q(A,E))=rselect_tail(A).
% 2.42/2.64  0 [] rselect_tail(rstore_head(A,E))=rselect_tail(A).
% 2.42/2.64  0 [] s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X))))))))))))))))))))))))))))))))))))))))))))))))))!=X.
% 2.42/2.64  0 [] s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X)))))))))))))))))))))))))))))))))))))))))))))))))!=X.
% 2.42/2.64  0 [] s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X))))))))))))))))))))))))))))))))))))))))))))))))!=X.
% 2.42/2.64  0 [] s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X)))))))))))))))))))))))))))))))))))))))))))))))!=X.
% 2.42/2.64  0 [] s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X))))))))))))))))))))))))))))))))))))))))))))))!=X.
% 2.42/2.64  0 [] s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X)))))))))))))))))))))))))))))))))))))))))))))!=X.
% 2.42/2.64  0 [] s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X))))))))))))))))))))))))))))))))))))))))))))!=X.
% 2.42/2.64  0 [] s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X)))))))))))))))))))))))))))))))))))))))))))!=X.
% 2.42/2.64  0 [] s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X))))))))))))))))))))))))))))))))))))))))))!=X.
% 2.42/2.64  0 [] s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X)))))))))))))))))))))))))))))))))))))))))!=X.
% 2.42/2.64  0 [] s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X))))))))))))))))))))))))))))))))))))))))!=X.
% 2.42/2.64  0 [] s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X)))))))))))))))))))))))))))))))))))))))!=X.
% 2.42/2.64  0 [] s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X))))))))))))))))))))))))))))))))))))))!=X.
% 2.42/2.64  0 [] s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X)))))))))))))))))))))))))))))))))))))!=X.
% 2.42/2.64  0 [] s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X))))))))))))))))))))))))))))))))))))!=X.
% 2.42/2.64  0 [] s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X)))))))))))))))))))))))))))))))))))!=X.
% 2.42/2.64  0 [] s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X))))))))))))))))))))))))))))))))))!=X.
% 2.42/2.64  0 [] s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X)))))))))))))))))))))))))))))))))!=X.
% 2.42/2.64  0 [] s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X))))))))))))))))))))))))))))))))!=X.
% 2.42/2.64  0 [] s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X)))))))))))))))))))))))))))))))!=X.
% 2.42/2.64  0 [] s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X))))))))))))))))))))))))))))))!=X.
% 2.42/2.64  0 [] s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X)))))))))))))))))))))))))))))!=X.
% 2.42/2.64  0 [] s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X))))))))))))))))))))))))))))!=X.
% 2.42/2.64  0 [] s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X)))))))))))))))))))))))))))!=X.
% 2.42/2.64  0 [] s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X))))))))))))))))))))))))))!=X.
% 2.42/2.64  0 [] s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X)))))))))))))))))))))))))!=X.
% 2.42/2.64  0 [] s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X))))))))))))))))))))))))!=X.
% 2.42/2.64  0 [] s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X)))))))))))))))))))))))!=X.
% 2.42/2.64  0 [] s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X))))))))))))))))))))))!=X.
% 2.42/2.64  0 [] s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X)))))))))))))))))))))!=X.
% 2.42/2.64  0 [] s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X))))))))))))))))))))!=X.
% 2.42/2.64  0 [] s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X)))))))))))))))))))!=X.
% 2.42/2.64  0 [] s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X))))))))))))))))))!=X.
% 2.42/2.64  0 [] s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X)))))))))))))))))!=X.
% 2.42/2.64  0 [] s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X))))))))))))))))!=X.
% 2.42/2.64  0 [] s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X)))))))))))))))!=X.
% 2.42/2.64  0 [] s(s(s(s(s(s(s(s(s(s(s(s(s(s(X))))))))))))))!=X.
% 2.42/2.64  0 [] s(s(s(s(s(s(s(s(s(s(s(s(s(X)))))))))))))!=X.
% 2.42/2.64  0 [] s(s(s(s(s(s(s(s(s(s(s(s(X))))))))))))!=X.
% 2.42/2.64  0 [] s(s(s(s(s(s(s(s(s(s(s(X)))))))))))!=X.
% 2.42/2.64  0 [] s(s(s(s(s(s(s(s(s(s(X))))))))))!=X.
% 2.42/2.64  0 [] s(s(s(s(s(s(s(s(s(X)))))))))!=X.
% 2.42/2.64  0 [] s(s(s(s(s(s(s(s(X))))))))!=X.
% 2.42/2.64  0 [] s(s(s(s(s(s(s(X)))))))!=X.
% 2.42/2.64  0 [] s(s(s(s(s(s(X))))))!=X.
% 2.42/2.64  0 [] s(s(s(s(s(X)))))!=X.
% 2.42/2.64  0 [] s(s(s(s(X))))!=X.
% 2.42/2.64  0 [] s(s(s(X)))!=X.
% 2.42/2.64  0 [] s(s(X))!=X.
% 2.42/2.64  0 [] s(X)!=X.
% 2.42/2.64  0 [] earray_10=store(earray_8,index_9,e9).
% 2.42/2.64  0 [] earray_100=store(earray_98,index_99,e21).
% 2.42/2.64  0 [] earray_104=rselect_se_q(q22).
% 2.42/2.64  0 [] earray_106=store(earray_104,index_105,e22).
% 2.42/2.64  0 [] earray_110=rselect_se_q(q23).
% 2.42/2.64  0 [] earray_112=store(earray_110,index_111,e23).
% 2.42/2.64  0 [] earray_119=rselect_se_q(q24).
% 2.42/2.64  0 [] earray_121=store(earray_119,index_120,e24).
% 2.42/2.64  0 [] earray_125=rselect_se_q(q25).
% 2.42/2.64  0 [] earray_127=store(earray_125,index_126,e25).
% 2.42/2.64  0 [] earray_131=rselect_se_q(q26).
% 2.42/2.64  0 [] earray_133=store(earray_131,index_132,e26).
% 2.42/2.64  0 [] earray_14=rselect_se_q(q10).
% 2.42/2.64  0 [] earray_140=rselect_se_q(q27).
% 2.42/2.64  0 [] earray_142=store(earray_140,index_141,e27).
% 2.42/2.64  0 [] earray_146=rselect_se_q(q28).
% 2.42/2.64  0 [] earray_148=store(earray_146,index_147,e28).
% 2.42/2.64  0 [] earray_152=rselect_se_q(q2).
% 2.42/2.64  0 [] earray_154=store(earray_152,index_153,e2).
% 2.42/2.64  0 [] earray_16=store(earray_14,index_15,e10).
% 2.42/2.64  0 [] earray_161=rselect_se_q(q29).
% 2.42/2.64  0 [] earray_163=store(earray_161,index_162,e29).
% 2.42/2.64  0 [] earray_170=rselect_se_q(q3).
% 2.42/2.64  0 [] earray_172=store(earray_170,index_171,e3).
% 2.42/2.64  0 [] earray_176=rselect_se_q(q4).
% 2.42/2.64  0 [] earray_178=store(earray_176,index_177,e4).
% 2.42/2.64  0 [] earray_182=rselect_se_q(q5).
% 2.42/2.64  0 [] earray_184=store(earray_182,index_183,e5).
% 2.42/2.64  0 [] earray_191=rselect_se_q(q6).
% 2.42/2.64  0 [] earray_193=store(earray_191,index_192,e6).
% 2.42/2.64  0 [] earray_197=rselect_se_q(q7).
% 2.42/2.64  0 [] earray_199=store(earray_197,index_198,e7).
% 2.42/2.64  0 [] earray_2=rselect_se_q(q0).
% 2.42/2.64  0 [] earray_20=rselect_se_q(q11).
% 2.42/2.64  0 [] earray_203=rselect_se_q(q8).
% 2.42/2.64  0 [] earray_205=store(earray_203,index_204,e8).
% 2.42/2.64  0 [] earray_212=rselect_se_q(q30).
% 2.42/2.64  0 [] earray_22=store(earray_20,index_21,e11).
% 2.42/2.64  0 [] earray_29=rselect_se_q(q12).
% 2.42/2.64  0 [] earray_31=store(earray_29,index_30,e12).
% 2.42/2.64  0 [] earray_35=rselect_se_q(q13).
% 2.42/2.64  0 [] earray_37=store(earray_35,index_36,e13).
% 2.42/2.64  0 [] earray_4=store(earray_2,index_3,e0).
% 2.42/2.64  0 [] earray_41=rselect_se_q(q14).
% 2.42/2.64  0 [] earray_43=store(earray_41,index_42,e14).
% 2.42/2.64  0 [] earray_50=rselect_se_q(q15).
% 2.42/2.64  0 [] earray_52=store(earray_50,index_51,e15).
% 2.42/2.64  0 [] earray_56=rselect_se_q(q16).
% 2.42/2.64  0 [] earray_58=store(earray_56,index_57,e16).
% 2.42/2.64  0 [] earray_62=rselect_se_q(q17).
% 2.42/2.64  0 [] earray_64=store(earray_62,index_63,e17).
% 2.42/2.64  0 [] earray_71=rselect_se_q(q18).
% 2.42/2.64  0 [] earray_73=store(earray_71,index_72,e18).
% 2.42/2.64  0 [] earray_77=rselect_se_q(q1).
% 2.42/2.64  0 [] earray_79=store(earray_77,index_78,e1).
% 2.42/2.64  0 [] earray_8=rselect_se_q(q9).
% 2.42/2.64  0 [] earray_83=rselect_se_q(q19).
% 2.42/2.64  0 [] earray_85=store(earray_83,index_84,e19).
% 2.42/2.64  0 [] earray_89=rselect_se_q(q20).
% 2.42/2.64  0 [] earray_91=store(earray_89,index_90,e20).
% 2.42/2.64  0 [] earray_98=rselect_se_q(q21).
% 2.42/2.64  0 [] elem_214=select(earray_212,index_213).
% 2.42/2.64  0 [] index_0=rselect_tail(q).
% 2.42/2.64  0 [] index_102=s(index_99).
% 2.42/2.64  0 [] index_105=rselect_tail(q22).
% 2.42/2.64  0 [] index_108=s(index_105).
% 2.42/2.64  0 [] index_111=rselect_tail(q23).
% 2.42/2.64  0 [] index_114=s(index_111).
% 2.42/2.64  0 [] index_116=rselect_head(queue_115).
% 2.42/2.64  0 [] index_117=s(index_116).
% 2.42/2.64  0 [] index_12=s(index_9).
% 2.42/2.64  0 [] index_120=rselect_tail(q24).
% 2.42/2.64  0 [] index_123=s(index_120).
% 2.42/2.64  0 [] index_126=rselect_tail(q25).
% 2.42/2.64  0 [] index_129=s(index_126).
% 2.42/2.64  0 [] index_132=rselect_tail(q26).
% 2.42/2.64  0 [] index_135=s(index_132).
% 2.42/2.64  0 [] index_137=rselect_head(queue_136).
% 2.42/2.64  0 [] index_138=s(index_137).
% 2.42/2.64  0 [] index_141=rselect_tail(q27).
% 2.42/2.64  0 [] index_144=s(index_141).
% 2.42/2.64  0 [] index_147=rselect_tail(q28).
% 2.42/2.64  0 [] index_15=rselect_tail(q10).
% 2.42/2.64  0 [] index_150=s(index_147).
% 2.42/2.64  0 [] index_153=rselect_tail(q2).
% 2.42/2.64  0 [] index_156=s(index_153).
% 2.42/2.64  0 [] index_158=rselect_head(queue_157).
% 2.42/2.64  0 [] index_159=s(index_158).
% 2.42/2.64  0 [] index_162=rselect_tail(q29).
% 2.42/2.64  0 [] index_165=s(index_162).
% 2.42/2.64  0 [] index_167=rselect_head(queue_166).
% 2.42/2.64  0 [] index_168=s(index_167).
% 2.42/2.64  0 [] index_171=rselect_tail(q3).
% 2.42/2.64  0 [] index_174=s(index_171).
% 2.42/2.64  0 [] index_177=rselect_tail(q4).
% 2.42/2.64  0 [] index_18=s(index_15).
% 2.42/2.64  0 [] index_180=s(index_177).
% 2.42/2.64  0 [] index_183=rselect_tail(q5).
% 2.42/2.64  0 [] index_186=s(index_183).
% 2.42/2.64  0 [] index_188=rselect_head(queue_187).
% 2.42/2.64  0 [] index_189=s(index_188).
% 2.42/2.64  0 [] index_192=rselect_tail(q6).
% 2.42/2.64  0 [] index_195=s(index_192).
% 2.42/2.64  0 [] index_198=rselect_tail(q7).
% 2.42/2.64  0 [] index_201=s(index_198).
% 2.42/2.64  0 [] index_204=rselect_tail(q8).
% 2.42/2.64  0 [] index_207=s(index_204).
% 2.42/2.64  0 [] index_209=rselect_head(queue_208).
% 2.42/2.64  0 [] index_21=rselect_tail(q11).
% 2.42/2.64  0 [] index_210=s(index_209).
% 2.42/2.64  0 [] index_213=rselect_head(q30).
% 2.42/2.64  0 [] index_24=s(index_21).
% 2.42/2.64  0 [] index_26=rselect_head(queue_25).
% 2.42/2.64  0 [] index_27=s(index_26).
% 2.42/2.64  0 [] index_3=rselect_tail(q0).
% 2.42/2.64  0 [] index_30=rselect_tail(q12).
% 2.42/2.64  0 [] index_33=s(index_30).
% 2.42/2.64  0 [] index_36=rselect_tail(q13).
% 2.42/2.64  0 [] index_39=s(index_36).
% 2.42/2.64  0 [] index_42=rselect_tail(q14).
% 2.42/2.64  0 [] index_45=s(index_42).
% 2.42/2.64  0 [] index_47=rselect_head(queue_46).
% 2.42/2.64  0 [] index_48=s(index_47).
% 2.42/2.64  0 [] index_51=rselect_tail(q15).
% 2.42/2.64  0 [] index_54=s(index_51).
% 2.42/2.64  0 [] index_57=rselect_tail(q16).
% 2.42/2.64  0 [] index_6=s(index_3).
% 2.42/2.64  0 [] index_60=s(index_57).
% 2.42/2.64  0 [] index_63=rselect_tail(q17).
% 2.42/2.64  0 [] index_66=s(index_63).
% 2.42/2.64  0 [] index_68=rselect_head(queue_67).
% 2.42/2.64  0 [] index_69=s(index_68).
% 2.42/2.64  0 [] index_72=rselect_tail(q18).
% 2.42/2.64  0 [] index_75=s(index_72).
% 2.42/2.64  0 [] index_78=rselect_tail(q1).
% 2.42/2.64  0 [] index_81=s(index_78).
% 2.42/2.64  0 [] index_84=rselect_tail(q19).
% 2.42/2.64  0 [] index_87=s(index_84).
% 2.42/2.64  0 [] index_9=rselect_tail(q9).
% 2.42/2.64  0 [] index_90=rselect_tail(q20).
% 2.42/2.64  0 [] index_93=s(index_90).
% 2.42/2.64  0 [] index_95=rselect_head(queue_94).
% 2.42/2.64  0 [] index_96=s(index_95).
% 2.42/2.64  0 [] index_99=rselect_tail(q21).
% 2.42/2.64  0 [] queue_1=rstore_head(q,index_0).
% 2.42/2.64  0 [] queue_101=rstore_se_q(q21,earray_100).
% 2.42/2.64  0 [] queue_103=rstore_tail(queue_101,index_102).
% 2.42/2.64  0 [] queue_107=rstore_se_q(q22,earray_106).
% 2.42/2.64  0 [] queue_109=rstore_tail(queue_107,index_108).
% 2.42/2.64  0 [] queue_11=rstore_se_q(q9,earray_10).
% 2.42/2.64  0 [] queue_113=rstore_se_q(q23,earray_112).
% 2.42/2.64  0 [] queue_115=rstore_tail(queue_113,index_114).
% 2.42/2.64  0 [] queue_118=rstore_head(queue_115,index_117).
% 2.42/2.64  0 [] queue_122=rstore_se_q(q24,earray_121).
% 2.42/2.64  0 [] queue_124=rstore_tail(queue_122,index_123).
% 2.42/2.64  0 [] queue_128=rstore_se_q(q25,earray_127).
% 2.42/2.64  0 [] queue_13=rstore_tail(queue_11,index_12).
% 2.42/2.64  0 [] queue_130=rstore_tail(queue_128,index_129).
% 2.42/2.64  0 [] queue_134=rstore_se_q(q26,earray_133).
% 2.42/2.64  0 [] queue_136=rstore_tail(queue_134,index_135).
% 2.42/2.64  0 [] queue_139=rstore_head(queue_136,index_138).
% 2.42/2.64  0 [] queue_143=rstore_se_q(q27,earray_142).
% 2.42/2.64  0 [] queue_145=rstore_tail(queue_143,index_144).
% 2.42/2.64  0 [] queue_149=rstore_se_q(q28,earray_148).
% 2.42/2.64  0 [] queue_151=rstore_tail(queue_149,index_150).
% 2.42/2.64  0 [] queue_155=rstore_se_q(q2,earray_154).
% 2.42/2.64  0 [] queue_157=rstore_tail(queue_155,index_156).
% 2.42/2.64  0 [] queue_160=rstore_head(queue_157,index_159).
% 2.42/2.64  0 [] queue_164=rstore_se_q(q29,earray_163).
% 2.42/2.64  0 [] queue_166=rstore_tail(queue_164,index_165).
% 2.42/2.64  0 [] queue_169=rstore_head(queue_166,index_168).
% 2.42/2.64  0 [] queue_17=rstore_se_q(q10,earray_16).
% 2.42/2.64  0 [] queue_173=rstore_se_q(q3,earray_172).
% 2.42/2.64  0 [] queue_175=rstore_tail(queue_173,index_174).
% 2.42/2.64  0 [] queue_179=rstore_se_q(q4,earray_178).
% 2.42/2.64  0 [] queue_181=rstore_tail(queue_179,index_180).
% 2.42/2.64  0 [] queue_185=rstore_se_q(q5,earray_184).
% 2.42/2.64  0 [] queue_187=rstore_tail(queue_185,index_186).
% 2.42/2.64  0 [] queue_19=rstore_tail(queue_17,index_18).
% 2.42/2.64  0 [] queue_190=rstore_head(queue_187,index_189).
% 2.42/2.64  0 [] queue_194=rstore_se_q(q6,earray_193).
% 2.42/2.64  0 [] queue_196=rstore_tail(queue_194,index_195).
% 2.42/2.64  0 [] queue_200=rstore_se_q(q7,earray_199).
% 2.42/2.64  0 [] queue_202=rstore_tail(queue_200,index_201).
% 2.42/2.64  0 [] queue_206=rstore_se_q(q8,earray_205).
% 2.42/2.64  0 [] queue_208=rstore_tail(queue_206,index_207).
% 2.42/2.64  0 [] queue_211=rstore_head(queue_208,index_210).
% 2.42/2.64  0 [] queue_23=rstore_se_q(q11,earray_22).
% 2.42/2.64  0 [] queue_25=rstore_tail(queue_23,index_24).
% 2.42/2.64  0 [] queue_28=rstore_head(queue_25,index_27).
% 2.42/2.64  0 [] queue_32=rstore_se_q(q12,earray_31).
% 2.42/2.64  0 [] queue_34=rstore_tail(queue_32,index_33).
% 2.42/2.64  0 [] queue_38=rstore_se_q(q13,earray_37).
% 2.42/2.64  0 [] queue_40=rstore_tail(queue_38,index_39).
% 2.42/2.64  0 [] queue_44=rstore_se_q(q14,earray_43).
% 2.42/2.64  0 [] queue_46=rstore_tail(queue_44,index_45).
% 2.42/2.64  0 [] queue_49=rstore_head(queue_46,index_48).
% 2.42/2.64  0 [] queue_5=rstore_se_q(q0,earray_4).
% 2.42/2.64  0 [] queue_53=rstore_se_q(q15,earray_52).
% 2.42/2.64  0 [] queue_55=rstore_tail(queue_53,index_54).
% 2.42/2.64  0 [] queue_59=rstore_se_q(q16,earray_58).
% 2.42/2.64  0 [] queue_61=rstore_tail(queue_59,index_60).
% 2.42/2.64  0 [] queue_65=rstore_se_q(q17,earray_64).
% 2.42/2.64  0 [] queue_67=rstore_tail(queue_65,index_66).
% 2.42/2.64  0 [] queue_7=rstore_tail(queue_5,index_6).
% 2.42/2.64  0 [] queue_70=rstore_head(queue_67,index_69).
% 2.42/2.64  0 [] queue_74=rstore_se_q(q18,earray_73).
% 2.42/2.64  0 [] queue_76=rstore_tail(queue_74,index_75).
% 2.42/2.64  0 [] queue_80=rstore_se_q(q1,earray_79).
% 2.42/2.64  0 [] queue_82=rstore_tail(queue_80,index_81).
% 2.42/2.64  0 [] queue_86=rstore_se_q(q19,earray_85).
% 2.42/2.64  0 [] queue_88=rstore_tail(queue_86,index_87).
% 2.42/2.64  0 [] queue_92=rstore_se_q(q20,earray_91).
% 2.42/2.64  0 [] queue_94=rstore_tail(queue_92,index_93).
% 2.42/2.64  0 [] queue_97=rstore_head(queue_94,index_96).
% 2.42/2.64  0 [] q0=queue_1.
% 2.42/2.64  0 [] q1=queue_7.
% 2.42/2.64  0 [] q10=queue_13.
% 2.42/2.64  0 [] q11=queue_19.
% 2.42/2.64  0 [] q12=queue_28.
% 2.42/2.64  0 [] q13=queue_34.
% 2.42/2.64  0 [] q14=queue_40.
% 2.42/2.64  0 [] q15=queue_49.
% 2.42/2.64  0 [] q16=queue_55.
% 2.42/2.64  0 [] q17=queue_61.
% 2.42/2.64  0 [] q18=queue_70.
% 2.42/2.64  0 [] q19=queue_76.
% 2.42/2.64  0 [] q2=queue_82.
% 2.42/2.64  0 [] q20=queue_88.
% 2.42/2.64  0 [] q21=queue_97.
% 2.42/2.64  0 [] q22=queue_103.
% 2.42/2.64  0 [] q23=queue_109.
% 2.42/2.64  0 [] q24=queue_118.
% 2.42/2.64  0 [] q25=queue_124.
% 2.42/2.64  0 [] q26=queue_130.
% 2.42/2.64  0 [] q27=queue_139.
% 2.42/2.64  0 [] q28=queue_145.
% 2.42/2.64  0 [] q29=queue_151.
% 2.42/2.64  0 [] q3=queue_160.
% 2.42/2.64  0 [] q30=queue_169.
% 2.42/2.64  0 [] q4=queue_175.
% 2.42/2.64  0 [] q5=queue_181.
% 2.42/2.64  0 [] q6=queue_190.
% 2.42/2.64  0 [] q7=queue_196.
% 2.42/2.64  0 [] q8=queue_202.
% 2.42/2.64  0 [] q9=queue_211.
% 2.42/2.64  0 [] elem_214!=e10.
% 2.42/2.64  end_of_list.
% 2.42/2.64  
% 2.42/2.64  SCAN INPUT: prop=0, horn=0, equality=1, symmetry=0, max_lits=2.
% 2.42/2.64  
% 2.42/2.64  This ia a non-Horn set with equality.  The strategy will be
% 2.42/2.64  Knuth-Bendix, ordered hyper_res, factoring, and unit
% 2.42/2.64  deletion, with positive clauses in sos and nonpositive
% 2.42/2.64  clauses in usable.
% 2.42/2.64  
% 2.42/2.64     dependent: set(knuth_bendix).
% 2.42/2.64     dependent: set(anl_eq).
% 2.42/2.64     dependent: set(para_from).
% 2.42/2.64     dependent: set(para_into).
% 2.42/2.64     dependent: clear(para_from_right).
% 2.42/2.64     dependent: clear(para_into_right).
% 2.42/2.64     dependent: set(para_from_vars).
% 2.42/2.64     dependent: set(eq_units_both_ways).
% 2.42/2.64     dependent: set(dynamic_demod_all).
% 2.42/2.64     dependent: set(dynamic_demod).
% 2.42/2.64     dependent: set(order_eq).
% 2.42/2.64     dependent: set(back_demod).
% 2.42/2.64     dependent: set(lrpo).
% 2.42/2.64     dependent: set(hyper_res).
% 2.42/2.64     dependent: set(unit_deletion).
% 2.42/2.64     dependent: set(factor).
% 2.42/2.64  
% 2.42/2.64  ------------> process usable:
% 2.42/2.64  ** KEPT (pick-wt=53): 1 [] s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(A))))))))))))))))))))))))))))))))))))))))))))))))))!=A.
% 2.42/2.64  ** KEPT (pick-wt=52): 2 [] s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(A)))))))))))))))))))))))))))))))))))))))))))))))))!=A.
% 2.42/2.64  ** KEPT (pick-wt=51): 3 [] s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(A))))))))))))))))))))))))))))))))))))))))))))))))!=A.
% 2.42/2.64  ** KEPT (pick-wt=50): 4 [] s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(A)))))))))))))))))))))))))))))))))))))))))))))))!=A.
% 2.42/2.64  ** KEPT (pick-wt=49): 5 [] s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(A))))))))))))))))))))))))))))))))))))))))))))))!=A.
% 2.42/2.64  ** KEPT (pick-wt=48): 6 [] s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(A)))))))))))))))))))))))))))))))))))))))))))))!=A.
% 2.42/2.64  ** KEPT (pick-wt=47): 7 [] s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(A))))))))))))))))))))))))))))))))))))))))))))!=A.
% 2.42/2.64  ** KEPT (pick-wt=46): 8 [] s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(A)))))))))))))))))))))))))))))))))))))))))))!=A.
% 2.42/2.64  ** KEPT (pick-wt=45): 9 [] s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(A))))))))))))))))))))))))))))))))))))))))))!=A.
% 2.42/2.64  ** KEPT (pick-wt=44): 10 [] s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(A)))))))))))))))))))))))))))))))))))))))))!=A.
% 2.42/2.64  ** KEPT (pick-wt=43): 11 [] s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(A))))))))))))))))))))))))))))))))))))))))!=A.
% 2.42/2.64  ** KEPT (pick-wt=42): 12 [] s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(A)))))))))))))))))))))))))))))))))))))))!=A.
% 2.42/2.64  ** KEPT (pick-wt=41): 13 [] s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(A))))))))))))))))))))))))))))))))))))))!=A.
% 2.42/2.64  ** KEPT (pick-wt=40): 14 [] s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(A)))))))))))))))))))))))))))))))))))))!=A.
% 2.42/2.64  ** KEPT (pick-wt=39): 15 [] s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(A))))))))))))))))))))))))))))))))))))!=A.
% 2.42/2.64  ** KEPT (pick-wt=38): 16 [] s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(A)))))))))))))))))))))))))))))))))))!=A.
% 2.42/2.64  ** KEPT (pick-wt=37): 17 [] s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(A))))))))))))))))))))))))))))))))))!=A.
% 2.42/2.64  ** KEPT (pick-wt=36): 18 [] s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(A)))))))))))))))))))))))))))))))))!=A.
% 2.42/2.64  ** KEPT (pick-wt=35): 19 [] s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(A))))))))))))))))))))))))))))))))!=A.
% 2.42/2.64  ** KEPT (pick-wt=34): 20 [] s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(A)))))))))))))))))))))))))))))))!=A.
% 2.42/2.64  ** KEPT (pick-wt=33): 21 [] s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(A))))))))))))))))))))))))))))))!=A.
% 2.42/2.64  ** KEPT (pick-wt=32): 22 [] s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(A)))))))))))))))))))))))))))))!=A.
% 2.42/2.64  ** KEPT (pick-wt=31): 23 [] s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(A))))))))))))))))))))))))))))!=A.
% 2.42/2.64  ** KEPT (pick-wt=30): 24 [] s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(A)))))))))))))))))))))))))))!=A.
% 2.42/2.64  ** KEPT (pick-wt=29): 25 [] s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(A))))))))))))))))))))))))))!=A.
% 2.42/2.64  ** KEPT (pick-wt=28): 26 [] s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(A)))))))))))))))))))))))))!=A.
% 2.42/2.64  ** KEPT (pick-wt=27): 27 [] s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(A))))))))))))))))))))))))!=A.
% 2.42/2.64  ** KEPT (pick-wt=26): 28 [] s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(A)))))))))))))))))))))))!=A.
% 2.42/2.64  ** KEPT (pick-wt=25): 29 [] s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(A))))))))))))))))))))))!=A.
% 2.42/2.64  ** KEPT (pick-wt=24): 30 [] s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(A)))))))))))))))))))))!=A.
% 2.42/2.64  ** KEPT (pick-wt=23): 31 [] s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(A))))))))))))))))))))!=A.
% 2.42/2.64  ** KEPT (pick-wt=22): 32 [] s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(A)))))))))))))))))))!=A.
% 2.42/2.64  ** KEPT (pick-wt=21): 33 [] s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(A))))))))))))))))))!=A.
% 2.42/2.64  ** KEPT (pick-wt=20): 34 [] s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(A)))))))))))))))))!=A.
% 2.42/2.64  ** KEPT (pick-wt=19): 35 [] s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(A))))))))))))))))!=A.
% 2.42/2.64  ** KEPT (pick-wt=18): 36 [] s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(A)))))))))))))))!=A.
% 2.42/2.64  ** KEPT (pick-wt=17): 37 [] s(s(s(s(s(s(s(s(s(s(s(s(s(s(A))))))))))))))!=A.
% 2.42/2.64  ** KEPT (pick-wt=16): 38 [] s(s(s(s(s(s(s(s(s(s(s(s(s(A)))))))))))))!=A.
% 2.42/2.64  ** KEPT (pick-wt=15): 39 [] s(s(s(s(s(s(s(s(s(s(s(s(A))))))))))))!=A.
% 2.42/2.64  ** KEPT (pick-wt=14): 40 [] s(s(s(s(s(s(s(s(s(s(s(A)))))))))))!=A.
% 2.42/2.64  ** KEPT (pick-wt=13): 41 [] s(s(s(s(s(s(s(s(s(s(A))))))))))!=A.
% 2.42/2.64  ** KEPT (pick-wt=12): 42 [] s(s(s(s(s(s(s(s(s(A)))))))))!=A.
% 2.42/2.64  ** KEPT (pick-wt=11): 43 [] s(s(s(s(s(s(s(s(A))))))))!=A.
% 2.42/2.64  ** KEPT (pick-wt=10): 44 [] s(s(s(s(s(s(s(A)))))))!=A.
% 2.42/2.64  ** KEPT (pick-wt=9): 45 [] s(s(s(s(s(s(A))))))!=A.
% 2.42/2.64  ** KEPT (pick-wt=8): 46 [] s(s(s(s(s(A)))))!=A.
% 2.42/2.64  ** KEPT (pick-wt=7): 47 [] s(s(s(s(A))))!=A.
% 2.42/2.64  ** KEPT (pick-wt=6): 48 [] s(s(s(A)))!=A.
% 2.42/2.64  ** KEPT (pick-wt=5): 49 [] s(s(A))!=A.
% 2.42/2.64  ** KEPT (pick-wt=4): 50 [] s(A)!=A.
% 2.42/2.64  ** KEPT (pick-wt=3): 51 [] elem_214!=e10.
% 2.42/2.64  
% 2.42/2.64  ------------> process sos:
% 2.42/2.64  ** KEPT (pick-wt=3): 52 [] A=A.
% 2.42/2.64  ** KEPT (pick-wt=8): 53 [] select(store(A,B,C),B)=C.
% 2.42/2.64  ---> New Demodulator: 54 [new_demod,53] select(store(A,B,C),B)=C.
% 2.42/2.64  ** KEPT (pick-wt=13): 55 [] A=B|select(store(C,A,D),B)=select(C,B).
% 2.42/2.64  ** KEPT (pick-wt=6): 56 [] rselect_se_q(rstore_se_q(A,B))=B.
% 2.42/2.64  ---> New Demodulator: 57 [new_demod,56] rselect_se_q(rstore_se_q(A,B))=B.
% 2.42/2.64  ** KEPT (pick-wt=6): 58 [] rselect_head(rstore_head(A,B))=B.
% 2.42/2.64  ---> New Demodulator: 59 [new_demod,58] rselect_head(rstore_head(A,B))=B.
% 2.42/2.64  ** KEPT (pick-wt=6): 60 [] rselect_tail(rstore_tail(A,B))=B.
% 2.42/2.64  ---> New Demodulator: 61 [new_demod,60] rselect_tail(rstore_tail(A,B))=B.
% 2.42/2.64  ** KEPT (pick-wt=7): 62 [] rselect_se_q(rstore_head(A,B))=rselect_se_q(A).
% 2.42/2.64  ---> New Demodulator: 63 [new_demod,62] rselect_se_q(rstore_head(A,B))=rselect_se_q(A).
% 2.42/2.64  ** KEPT (pick-wt=7): 64 [] rselect_se_q(rstore_tail(A,B))=rselect_se_q(A).
% 2.42/2.64  ---> New Demodulator: 65 [new_demod,64] rselect_se_q(rstore_tail(A,B))=rselect_se_q(A).
% 2.42/2.64  ** KEPT (pick-wt=7): 66 [] rselect_head(rstore_tail(A,B))=rselect_head(A).
% 2.42/2.64  ---> New Demodulator: 67 [new_demod,66] rselect_head(rstore_tail(A,B))=rselect_head(A).
% 2.42/2.64  ** KEPT (pick-wt=7): 68 [] rselect_head(rstore_se_q(A,B))=rselect_head(A).
% 2.42/2.64  ---> New Demodulator: 69 [new_demod,68] rselect_head(rstore_se_q(A,B))=rselect_head(A).
% 2.42/2.64  ** KEPT (pick-wt=7): 70 [] rselect_tail(rstore_se_q(A,B))=rselect_tail(A).
% 2.42/2.64  ---> New Demodulator: 71 [new_demod,70] rselect_tail(rstore_se_q(A,B))=rselect_tail(A).
% 2.42/2.64  ** KEPT (pick-wt=7): 72 [] rselect_tail(rstore_head(A,B))=rselect_tail(A).
% 2.42/2.64  ---> New Demodulator: 73 [new_demod,72] rselect_tail(rstore_head(A,B))=rselect_tail(A).
% 2.42/2.64  ** KEPT (pick-wt=6): 75 [copy,74,flip.1] store(earray_8,index_9,e9)=earray_10.
% 2.42/2.64  ---> New Demodulator: 76 [new_demod,75] store(earray_8,index_9,e9)=earray_10.
% 2.42/2.64  ** KEPT (pick-wt=6): 78 [copy,77,flip.1] store(earray_98,index_99,e21)=earray_100.
% 2.42/2.64  ---> New Demodulator: 79 [new_demod,78] store(earray_98,index_99,e21)=earray_100.
% 2.42/2.64  ** KEPT (pick-wt=4): 81 [copy,80,flip.1] rselect_se_q(q22)=earray_104.
% 2.42/2.64  ---> New Demodulator: 82 [new_demod,81] rselect_se_q(q22)=earray_104.
% 2.42/2.64  ** KEPT (pick-wt=6): 84 [copy,83,flip.1] store(earray_104,index_105,e22)=earray_106.
% 2.42/2.64  ---> New Demodulator: 85 [new_demod,84] store(earray_104,index_105,e22)=earray_106.
% 2.42/2.64  ** KEPT (pick-wt=4): 87 [copy,86,flip.1] rselect_se_q(q23)=earray_110.
% 2.42/2.64  ---> New Demodulator: 88 [new_demod,87] rselect_se_q(q23)=earray_110.
% 2.42/2.64  ** KEPT (pick-wt=6): 90 [copy,89,flip.1] store(earray_110,index_111,e23)=earray_112.
% 2.42/2.64  ---> New Demodulator: 91 [new_demod,90] store(earray_110,index_111,e23)=earray_112.
% 2.42/2.64  ** KEPT (pick-wt=4): 93 [copy,92,flip.1] rselect_se_q(q24)=earray_119.
% 2.42/2.64  ---> New Demodulator: 94 [new_demod,93] rselect_se_q(q24)=earray_119.
% 2.42/2.64  ** KEPT (pick-wt=6): 96 [copy,95,flip.1] store(earray_119,index_120,e24)=earray_121.
% 2.42/2.64  ---> New Demodulator: 97 [new_demod,96] store(earray_119,index_120,e24)=earray_121.
% 2.42/2.64  ** KEPT (pick-wt=4): 99 [copy,98,flip.1] rselect_se_q(q25)=earray_125.
% 2.42/2.64  ---> New Demodulator: 100 [new_demod,99] rselect_se_q(q25)=earray_125.
% 2.42/2.64  ** KEPT (pick-wt=6): 102 [copy,101,flip.1] store(earray_125,index_126,e25)=earray_127.
% 2.42/2.64  ---> New Demodulator: 103 [new_demod,102] store(earray_125,index_126,e25)=earray_127.
% 2.42/2.64  ** KEPT (pick-wt=4): 105 [copy,104,flip.1] rselect_se_q(q26)=earray_131.
% 2.42/2.64  ---> New Demodulator: 106 [new_demod,105] rselect_se_q(q26)=earray_131.
% 2.42/2.64  ** KEPT (pick-wt=6): 108 [copy,107,flip.1] store(earray_131,index_132,e26)=earray_133.
% 2.42/2.64  ---> New Demodulator: 109 [new_demod,108] store(earray_131,index_132,e26)=earray_133.
% 2.42/2.64  ** KEPT (pick-wt=4): 111 [copy,110,flip.1] rselect_se_q(q10)=earray_14.
% 2.42/2.64  ---> New Demodulator: 112 [new_demod,111] rselect_se_q(q10)=earray_14.
% 2.42/2.64  ** KEPT (pick-wt=4): 114 [copy,113,flip.1] rselect_se_q(q27)=earray_140.
% 2.42/2.64  ---> New Demodulator: 115 [new_demod,114] rselect_se_q(q27)=earray_140.
% 2.42/2.64  ** KEPT (pick-wt=6): 117 [copy,116,flip.1] store(earray_140,index_141,e27)=earray_142.
% 2.42/2.64  ---> New Demodulator: 118 [new_demod,117] store(earray_140,index_141,e27)=earray_142.
% 2.42/2.64  ** KEPT (pick-wt=4): 120 [copy,119,flip.1] rselect_se_q(q28)=earray_146.
% 2.42/2.64  ---> New Demodulator: 121 [new_demod,120] rselect_se_q(q28)=earray_146.
% 2.42/2.64  ** KEPT (pick-wt=6): 123 [copy,122,flip.1] store(earray_146,index_147,e28)=earray_148.
% 2.42/2.64  ---> New Demodulator: 124 [new_demod,123] store(earray_146,index_147,e28)=earray_148.
% 2.42/2.64  ** KEPT (pick-wt=4): 126 [copy,125,flip.1] rselect_se_q(q2)=earray_152.
% 2.42/2.64  ---> New Demodulator: 127 [new_demod,126] rselect_se_q(q2)=earray_152.
% 2.42/2.64  ** KEPT (pick-wt=6): 129 [copy,128,flip.1] store(earray_152,index_153,e2)=earray_154.
% 2.42/2.64  ---> New Demodulator: 130 [new_demod,129] store(earray_152,index_153,e2)=earray_154.
% 2.42/2.64  ** KEPT (pick-wt=6): 132 [copy,131,flip.1] store(earray_14,index_15,e10)=earray_16.
% 2.42/2.64  ---> New Demodulator: 133 [new_demod,132] store(earray_14,index_15,e10)=earray_16.
% 2.42/2.64  ** KEPT (pick-wt=4): 135 [copy,134,flip.1] rselect_se_q(q29)=earray_161.
% 2.42/2.64  ---> New Demodulator: 136 [new_demod,135] rselect_se_q(q29)=earray_161.
% 2.42/2.64  ** KEPT (pick-wt=6): 138 [copy,137,flip.1] store(earray_161,index_162,e29)=earray_163.
% 2.42/2.64  ---> New Demodulator: 139 [new_demod,138] store(earray_161,index_162,e29)=earray_163.
% 2.42/2.64  ** KEPT (pick-wt=4): 141 [copy,140,flip.1] rselect_se_q(q3)=earray_170.
% 2.42/2.64  ---> New Demodulator: 142 [new_demod,141] rselect_se_q(q3)=earray_170.
% 2.42/2.64  ** KEPT (pick-wt=6): 144 [copy,143,flip.1] store(earray_170,index_171,e3)=earray_172.
% 2.42/2.64  ---> New Demodulator: 145 [new_demod,144] store(earray_170,index_171,e3)=earray_172.
% 2.42/2.64  ** KEPT (pick-wt=4): 147 [copy,146,flip.1] rselect_se_q(q4)=earray_176.
% 2.42/2.64  ---> New Demodulator: 148 [new_demod,147] rselect_se_q(q4)=earray_176.
% 2.42/2.64  ** KEPT (pick-wt=6): 150 [copy,149,flip.1] store(earray_176,index_177,e4)=earray_178.
% 2.42/2.64  ---> New Demodulator: 151 [new_demod,150] store(earray_176,index_177,e4)=earray_178.
% 2.42/2.64  ** KEPT (pick-wt=4): 153 [copy,152,flip.1] rselect_se_q(q5)=earray_182.
% 2.42/2.64  ---> New Demodulator: 154 [new_demod,153] rselect_se_q(q5)=earray_182.
% 2.42/2.64  ** KEPT (pick-wt=6): 156 [copy,155,flip.1] store(earray_182,index_183,e5)=earray_184.
% 2.42/2.64  ---> New Demodulator: 157 [new_demod,156] store(earray_182,index_183,e5)=earray_184.
% 2.42/2.64  ** KEPT (pick-wt=4): 159 [copy,158,flip.1] rselect_se_q(q6)=earray_191.
% 2.42/2.64  ---> New Demodulator: 160 [new_demod,159] rselect_se_q(q6)=earray_191.
% 2.42/2.64  ** KEPT (pick-wt=6): 162 [copy,161,flip.1] store(earray_191,index_192,e6)=earray_193.
% 2.42/2.64  ---> New Demodulator: 163 [new_demod,162] store(earray_191,index_192,e6)=earray_193.
% 2.42/2.64  ** KEPT (pick-wt=4): 165 [copy,164,flip.1] rselect_se_q(q7)=earray_197.
% 2.42/2.64  ---> New Demodulator: 166 [new_demod,165] rselect_se_q(q7)=earray_197.
% 2.42/2.64  ** KEPT (pick-wt=6): 168 [copy,167,flip.1] store(earray_197,index_198,e7)=earray_199.
% 2.42/2.64  ---> New Demodulator: 169 [new_demod,168] store(earray_197,index_198,e7)=earray_199.
% 2.42/2.64  ** KEPT (pick-wt=4): 171 [copy,170,flip.1] rselect_se_q(q0)=earray_2.
% 2.42/2.64  ---> New Demodulator: 172 [new_demod,171] rselect_se_q(q0)=earray_2.
% 2.42/2.64  ** KEPT (pick-wt=4): 174 [copy,173,flip.1] rselect_se_q(q11)=earray_20.
% 2.42/2.64  ---> New Demodulator: 175 [new_demod,174] rselect_se_q(q11)=earray_20.
% 2.42/2.64  ** KEPT (pick-wt=4): 177 [copy,176,flip.1] rselect_se_q(q8)=earray_203.
% 2.42/2.64  ---> New Demodulator: 178 [new_demod,177] rselect_se_q(q8)=earray_203.
% 2.42/2.64  ** KEPT (pick-wt=6): 180 [copy,179,flip.1] store(earray_203,index_204,e8)=earray_205.
% 2.42/2.64  ---> New Demodulator: 181 [new_demod,180] store(earray_203,index_204,e8)=earray_205.
% 2.42/2.64  ** KEPT (pick-wt=4): 183 [copy,182,flip.1] rselect_se_q(q30)=earray_212.
% 2.42/2.64  ---> New Demodulator: 184 [new_demod,183] rselect_se_q(q30)=earray_212.
% 2.42/2.64  ** KEPT (pick-wt=6): 186 [copy,185,flip.1] store(earray_20,index_21,e11)=earray_22.
% 2.42/2.64  ---> New Demodulator: 187 [new_demod,186] store(earray_20,index_21,e11)=earray_22.
% 2.42/2.64  ** KEPT (pick-wt=4): 189 [copy,188,flip.1] rselect_se_q(q12)=earray_29.
% 2.42/2.64  ---> New Demodulator: 190 [new_demod,189] rselect_se_q(q12)=earray_29.
% 2.42/2.64  ** KEPT (pick-wt=6): 192 [copy,191,flip.1] store(earray_29,index_30,e12)=earray_31.
% 2.42/2.64  ---> New Demodulator: 193 [new_demod,192] store(earray_29,index_30,e12)=earray_31.
% 2.42/2.64  ** KEPT (pick-wt=4): 195 [copy,194,flip.1] rselect_se_q(q13)=earray_35.
% 2.42/2.64  ---> New Demodulator: 196 [new_demod,195] rselect_se_q(q13)=earray_35.
% 2.42/2.64  ** KEPT (pick-wt=6): 198 [copy,197,flip.1] store(earray_35,index_36,e13)=earray_37.
% 2.42/2.64  ---> New Demodulator: 199 [new_demod,198] store(earray_35,index_36,e13)=earray_37.
% 2.42/2.64  ** KEPT (pick-wt=6): 201 [copy,200,flip.1] store(earray_2,index_3,e0)=earray_4.
% 2.42/2.64  ---> New Demodulator: 202 [new_demod,201] store(earray_2,index_3,e0)=earray_4.
% 2.42/2.64  ** KEPT (pick-wt=4): 204 [copy,203,flip.1] rselect_se_q(q14)=earray_41.
% 2.42/2.64  ---> New Demodulator: 205 [new_demod,204] rselect_se_q(q14)=earray_41.
% 2.42/2.64  ** KEPT (pick-wt=6): 207 [copy,206,flip.1] store(earray_41,index_42,e14)=earray_43.
% 2.42/2.64  ---> New Demodulator: 208 [new_demod,207] store(earray_41,index_42,e14)=earray_43.
% 2.42/2.64  ** KEPT (pick-wt=4): 210 [copy,209,flip.1] rselect_se_q(q15)=earray_50.
% 2.42/2.64  ---> New Demodulator: 211 [new_demod,210] rselect_se_q(q15)=earray_50.
% 2.42/2.64  ** KEPT (pick-wt=6): 213 [copy,212,flip.1] store(earray_50,index_51,e15)=earray_52.
% 2.42/2.64  ---> New Demodulator: 214 [new_demod,213] store(earray_50,index_51,e15)=earray_52.
% 2.42/2.64  ** KEPT (pick-wt=4): 216 [copy,215,flip.1] rselect_se_q(q16)=earray_56.
% 2.42/2.64  ---> New Demodulator: 217 [new_demod,216] rselect_se_q(q16)=earray_56.
% 2.42/2.64  ** KEPT (pick-wt=6): 219 [copy,218,flip.1] store(earray_56,index_57,e16)=earray_58.
% 2.42/2.64  ---> New Demodulator: 220 [new_demod,219] store(earray_56,index_57,e16)=earray_58.
% 2.42/2.64  ** KEPT (pick-wt=4): 222 [copy,221,flip.1] rselect_se_q(q17)=earray_62.
% 2.42/2.64  ---> New Demodulator: 223 [new_demod,222] rselect_se_q(q17)=earray_62.
% 2.42/2.64  ** KEPT (pick-wt=6): 225 [copy,224,flip.1] store(earray_62,index_63,e17)=earray_64.
% 2.42/2.64  ---> New Demodulator: 226 [new_demod,225] store(earray_62,index_63,e17)=earray_64.
% 2.42/2.64  ** KEPT (pick-wt=4): 228 [copy,227,flip.1] rselect_se_q(q18)=earray_71.
% 2.42/2.64  ---> New Demodulator: 229 [new_demod,228] rselect_se_q(q18)=earray_71.
% 2.42/2.64  ** KEPT (pick-wt=6): 231 [copy,230,flip.1] store(earray_71,index_72,e18)=earray_73.
% 2.42/2.64  ---> New Demodulator: 232 [new_demod,231] store(earray_71,index_72,e18)=earray_73.
% 2.42/2.64  ** KEPT (pick-wt=4): 234 [copy,233,flip.1] rselect_se_q(q1)=earray_77.
% 2.42/2.64  ---> New Demodulator: 235 [new_demod,234] rselect_se_q(q1)=earray_77.
% 2.42/2.64  ** KEPT (pick-wt=6): 237 [copy,236,flip.1] store(earray_77,index_78,e1)=earray_79.
% 2.42/2.64  ---> New Demodulator: 238 [new_demod,237] store(earray_77,index_78,e1)=earray_79.
% 2.42/2.64  ** KEPT (pick-wt=4): 240 [copy,239,flip.1] rselect_se_q(q9)=earray_8.
% 2.42/2.64  ---> New Demodulator: 241 [new_demod,240] rselect_se_q(q9)=earray_8.
% 2.42/2.64  ** KEPT (pick-wt=4): 243 [copy,242,flip.1] rselect_se_q(q19)=earray_83.
% 2.42/2.64  ---> New Demodulator: 244 [new_demod,243] rselect_se_q(q19)=earray_83.
% 2.42/2.64  ** KEPT (pick-wt=6): 246 [copy,245,flip.1] store(earray_83,index_84,e19)=earray_85.
% 2.42/2.64  ---> New Demodulator: 247 [new_demod,246] store(earray_83,index_84,e19)=earray_85.
% 2.42/2.64  ** KEPT (pick-wt=4): 249 [copy,248,flip.1] rselect_se_q(q20)=earray_89.
% 2.42/2.64  ---> New Demodulator: 250 [new_demod,249] rselect_se_q(q20)=earray_89.
% 2.42/2.64  ** KEPT (pick-wt=6): 252 [copy,251,flip.1] store(earray_89,index_90,e20)=earray_91.
% 2.42/2.64  ---> New Demodulator: 253 [new_demod,252] store(earray_89,index_90,e20)=earray_91.
% 2.42/2.64  ** KEPT (pick-wt=4): 255 [copy,254,flip.1] rselect_se_q(q21)=earray_98.
% 2.42/2.64  ---> New Demodulator: 256 [new_demod,255] rselect_se_q(q21)=earray_98.
% 2.42/2.64  ** KEPT (pick-wt=5): 258 [copy,257,flip.1] select(earray_212,index_213)=elem_214.
% 2.42/2.64  ---> New Demodulator: 259 [new_demod,258] select(earray_212,index_213)=elem_214.
% 2.42/2.64  ** KEPT (pick-wt=4): 261 [copy,260,flip.1] rselect_tail(q)=index_0.
% 2.42/2.64  ---> New Demodulator: 262 [new_demod,261] rselect_tail(q)=index_0.
% 2.42/2.64  ** KEPT (pick-wt=4): 264 [copy,263,flip.1] s(index_99)=index_102.
% 2.42/2.64  ---> New Demodulator: 265 [new_demod,264] s(index_99)=index_102.
% 2.42/2.64  ** KEPT (pick-wt=4): 267 [copy,266,flip.1] rselect_tail(q22)=index_105.
% 2.42/2.64  ---> New Demodulator: 268 [new_demod,267] rselect_tail(q22)=index_105.
% 2.42/2.64  ** KEPT (pick-wt=4): 270 [copy,269,flip.1] s(index_105)=index_108.
% 2.42/2.64  ---> New Demodulator: 271 [new_demod,270] s(index_105)=index_108.
% 2.42/2.64  ** KEPT (pick-wt=4): 273 [copy,272,flip.1] rselect_tail(q23)=index_111.
% 2.42/2.64  ---> New Demodulator: 274 [new_demod,273] rselect_tail(q23)=index_111.
% 2.42/2.64  ** KEPT (pick-wt=4): 276 [copy,275,flip.1] s(index_111)=index_114.
% 2.42/2.64  ---> New Demodulator: 277 [new_demod,276] s(index_111)=index_114.
% 2.42/2.64  ** KEPT (pick-wt=4): 279 [copy,278,flip.1] rselect_head(queue_115)=index_116.
% 2.42/2.64  ---> New Demodulator: 280 [new_demod,279] rselect_head(queue_115)=index_116.
% 2.42/2.64  ** KEPT (pick-wt=4): 282 [copy,281,flip.1] s(index_116)=index_117.
% 2.42/2.64  ---> New Demodulator: 283 [new_demod,282] s(index_116)=index_117.
% 2.42/2.64  ** KEPT (pick-wt=4): 285 [copy,284,flip.1] s(index_9)=index_12.
% 2.42/2.64  ---> New Demodulator: 286 [new_demod,285] s(index_9)=index_12.
% 2.42/2.64  ** KEPT (pick-wt=4): 288 [copy,287,flip.1] rselect_tail(q24)=index_120.
% 2.42/2.64  ---> New Demodulator: 289 [new_demod,288] rselect_tail(q24)=index_120.
% 2.42/2.64  ** KEPT (pick-wt=4): 291 [copy,290,flip.1] s(index_120)=index_123.
% 2.42/2.64  ---> New Demodulator: 292 [new_demod,291] s(index_120)=index_123.
% 2.42/2.64  ** KEPT (pick-wt=4): 294 [copy,293,flip.1] rselect_tail(q25)=index_126.
% 2.42/2.64  ---> New Demodulator: 295 [new_demod,294] rselect_tail(q25)=index_126.
% 2.42/2.64  ** KEPT (pick-wt=4): 297 [copy,296,flip.1] s(index_126)=index_129.
% 2.42/2.64  ---> New Demodulator: 298 [new_demod,297] s(index_126)=index_129.
% 2.42/2.64  ** KEPT (pick-wt=4): 300 [copy,299,flip.1] rselect_tail(q26)=index_132.
% 2.42/2.64  ---> New Demodulator: 301 [new_demod,300] rselect_tail(q26)=index_132.
% 2.42/2.64  ** KEPT (pick-wt=4): 303 [copy,302,flip.1] s(index_132)=index_135.
% 2.42/2.64  ---> New Demodulator: 304 [new_demod,303] s(index_132)=index_135.
% 2.42/2.64  ** KEPT (pick-wt=4): 306 [copy,305,flip.1] rselect_head(queue_136)=index_137.
% 2.42/2.64  ---> New Demodulator: 307 [new_demod,306] rselect_head(queue_136)=index_137.
% 2.42/2.64  ** KEPT (pick-wt=4): 309 [copy,308,flip.1] s(index_137)=index_138.
% 2.42/2.64  ---> New Demodulator: 310 [new_demod,309] s(index_137)=index_138.
% 2.42/2.64  ** KEPT (pick-wt=4): 312 [copy,311,flip.1] rselect_tail(q27)=index_141.
% 2.42/2.64  ---> New Demodulator: 313 [new_demod,312] rselect_tail(q27)=index_141.
% 2.42/2.64  ** KEPT (pick-wt=4): 315 [copy,314,flip.1] s(index_141)=index_144.
% 2.42/2.64  ---> New Demodulator: 316 [new_demod,315] s(index_141)=index_144.
% 2.42/2.64  ** KEPT (pick-wt=4): 318 [copy,317,flip.1] rselect_tail(q28)=index_147.
% 2.42/2.64  ---> New Demodulator: 319 [new_demod,318] rselect_tail(q28)=index_147.
% 2.42/2.64  ** KEPT (pick-wt=4): 321 [copy,320,flip.1] rselect_tail(q10)=index_15.
% 2.42/2.64  ---> New Demodulator: 322 [new_demod,321] rselect_tail(q10)=index_15.
% 2.42/2.64  ** KEPT (pick-wt=4): 324 [copy,323,flip.1] s(index_147)=index_150.
% 2.42/2.64  ---> New Demodulator: 325 [new_demod,324] s(index_147)=index_150.
% 2.42/2.64  ** KEPT (pick-wt=4): 327 [copy,326,flip.1] rselect_tail(q2)=index_153.
% 2.42/2.64  ---> New Demodulator: 328 [new_demod,327] rselect_tail(q2)=index_153.
% 2.42/2.64  ** KEPT (pick-wt=4): 330 [copy,329,flip.1] s(index_153)=index_156.
% 2.42/2.64  ---> New Demodulator: 331 [new_demod,330] s(index_153)=index_156.
% 2.42/2.64  ** KEPT (pick-wt=4): 333 [copy,332,flip.1] rselect_head(queue_157)=index_158.
% 2.42/2.64  ---> New Demodulator: 334 [new_demod,333] rselect_head(queue_157)=index_158.
% 2.42/2.64  ** KEPT (pick-wt=4): 336 [copy,335,flip.1] s(index_158)=index_159.
% 2.42/2.64  ---> New Demodulator: 337 [new_demod,336] s(index_158)=index_159.
% 2.42/2.64  ** KEPT (pick-wt=4): 339 [copy,338,flip.1] rselect_tail(q29)=index_162.
% 2.42/2.64  ---> New Demodulator: 340 [new_demod,339] rselect_tail(q29)=index_162.
% 2.42/2.64  ** KEPT (pick-wt=4): 342 [copy,341,flip.1] s(index_162)=index_165.
% 2.42/2.64  ---> New Demodulator: 343 [new_demod,342] s(index_162)=index_165.
% 2.42/2.64  ** KEPT (pick-wt=4): 345 [copy,344,flip.1] rselect_head(queue_166)=index_167.
% 2.42/2.64  ---> New Demodulator: 346 [new_demod,345] rselect_head(queue_166)=index_167.
% 2.42/2.64  ** KEPT (pick-wt=4): 348 [copy,347,flip.1] s(index_167)=index_168.
% 2.42/2.64  ---> New Demodulator: 349 [new_demod,348] s(index_167)=index_168.
% 2.42/2.64  ** KEPT (pick-wt=4): 351 [copy,350,flip.1] rselect_tail(q3)=index_171.
% 2.42/2.64  ---> New Demodulator: 352 [new_demod,351] rselect_tail(q3)=index_171.
% 2.42/2.64  ** KEPT (pick-wt=4): 354 [copy,353,flip.1] s(index_171)=index_174.
% 2.42/2.64  ---> New Demodulator: 355 [new_demod,354] s(index_171)=index_174.
% 2.42/2.64  ** KEPT (pick-wt=4): 357 [copy,356,flip.1] rselect_tail(q4)=index_177.
% 2.42/2.64  ---> New Demodulator: 358 [new_demod,357] rselect_tail(q4)=index_177.
% 2.42/2.64  ** KEPT (pick-wt=4): 360 [copy,359,flip.1] s(index_15)=index_18.
% 2.42/2.64  ---> New Demodulator: 361 [new_demod,360] s(index_15)=index_18.
% 2.42/2.64  ** KEPT (pick-wt=4): 363 [copy,362,flip.1] s(index_177)=index_180.
% 2.42/2.64  ---> New Demodulator: 364 [new_demod,363] s(index_177)=index_180.
% 2.42/2.64  ** KEPT (pick-wt=4): 366 [copy,365,flip.1] rselect_tail(q5)=index_183.
% 2.42/2.64  ---> New Demodulator: 367 [new_demod,366] rselect_tail(q5)=index_183.
% 2.42/2.64  ** KEPT (pick-wt=4): 369 [copy,368,flip.1] s(index_183)=index_186.
% 2.42/2.64  ---> New Demodulator: 370 [new_demod,369] s(index_183)=index_186.
% 2.42/2.64  ** KEPT (pick-wt=4): 372 [copy,371,flip.1] rselect_head(queue_187)=index_188.
% 2.42/2.64  ---> New Demodulator: 373 [new_demod,372] rselect_head(queue_187)=index_188.
% 2.42/2.64  ** KEPT (pick-wt=4): 375 [copy,374,flip.1] s(index_188)=index_189.
% 2.42/2.64  ---> New Demodulator: 376 [new_demod,375] s(index_188)=index_189.
% 2.42/2.64  ** KEPT (pick-wt=4): 378 [copy,377,flip.1] rselect_tail(q6)=index_192.
% 2.42/2.64  ---> New Demodulator: 379 [new_demod,378] rselect_tail(q6)=index_192.
% 2.42/2.64  ** KEPT (pick-wt=4): 381 [copy,380,flip.1] s(index_192)=index_195.
% 2.42/2.64  ---> New Demodulator: 382 [new_demod,381] s(index_192)=index_195.
% 2.42/2.64  ** KEPT (pick-wt=4): 384 [copy,383,flip.1] rselect_tail(q7)=index_198.
% 2.42/2.64  ---> New Demodulator: 385 [new_demod,384] rselect_tail(q7)=index_198.
% 2.42/2.64  ** KEPT (pick-wt=4): 387 [copy,386,flip.1] s(index_198)=index_201.
% 2.42/2.64  ---> New Demodulator: 388 [new_demod,387] s(index_198)=index_201.
% 2.42/2.64  ** KEPT (pick-wt=4): 390 [copy,389,flip.1] rselect_tail(q8)=index_204.
% 2.42/2.64  ---> New Demodulator: 391 [new_demod,390] rselect_tail(q8)=index_204.
% 2.42/2.64  ** KEPT (pick-wt=4): 393 [copy,392,flip.1] s(index_204)=index_207.
% 2.42/2.64  ---> New Demodulator: 394 [new_demod,393] s(index_204)=index_207.
% 2.42/2.64  ** KEPT (pick-wt=4): 396 [copy,395,flip.1] rselect_head(queue_208)=index_209.
% 2.42/2.64  ---> New Demodulator: 397 [new_demod,396] rselect_head(queue_208)=index_209.
% 2.42/2.64  ** KEPT (pick-wt=4): 399 [copy,398,flip.1] rselect_tail(q11)=index_21.
% 2.42/2.64  ---> New Demodulator: 400 [new_demod,399] rselect_tail(q11)=index_21.
% 2.42/2.64  ** KEPT (pick-wt=4): 402 [copy,401,flip.1] s(index_209)=index_210.
% 2.42/2.64  ---> New Demodulator: 403 [new_demod,402] s(index_209)=index_210.
% 2.42/2.64  ** KEPT (pick-wt=4): 405 [copy,404,flip.1] rselect_head(q30)=index_213.
% 2.42/2.64  ---> New Demodulator: 406 [new_demod,405] rselect_head(q30)=index_213.
% 2.42/2.64  ** KEPT (pick-wt=4): 408 [copy,407,flip.1] s(index_21)=index_24.
% 2.42/2.64  ---> New Demodulator: 409 [new_demod,408] s(index_21)=index_24.
% 2.42/2.64  ** KEPT (pick-wt=4): 411 [copy,410,flip.1] rselect_head(queue_25)=index_26.
% 2.42/2.64  ---> New Demodulator: 412 [new_demod,411] rselect_head(queue_25)=index_26.
% 2.42/2.64  ** KEPT (pick-wt=4): 414 [copy,413,flip.1] s(index_26)=index_27.
% 2.42/2.64  ---> New Demodulator: 415 [new_demod,414] s(index_26)=index_27.
% 2.42/2.64  ** KEPT (pick-wt=4): 417 [copy,416,flip.1] rselect_tail(q0)=index_3.
% 2.42/2.64  ---> New Demodulator: 418 [new_demod,417] rselect_tail(q0)=index_3.
% 2.42/2.64  ** KEPT (pick-wt=4): 420 [copy,419,flip.1] rselect_tail(q12)=index_30.
% 2.42/2.64  ---> New Demodulator: 421 [new_demod,420] rselect_tail(q12)=index_30.
% 2.42/2.64  ** KEPT (pick-wt=4): 423 [copy,422,flip.1] s(index_30)=index_33.
% 2.42/2.64  ---> New Demodulator: 424 [new_demod,423] s(index_30)=index_33.
% 2.42/2.64  ** KEPT (pick-wt=4): 426 [copy,425,flip.1] rselect_tail(q13)=index_36.
% 2.42/2.64  ---> New Demodulator: 427 [new_demod,426] rselect_tail(q13)=index_36.
% 2.42/2.64  ** KEPT (pick-wt=4): 429 [copy,428,flip.1] s(index_36)=index_39.
% 2.42/2.64  ---> New Demodulator: 430 [new_demod,429] s(index_36)=index_39.
% 2.42/2.64  ** KEPT (pick-wt=4): 432 [copy,431,flip.1] rselect_tail(q14)=index_42.
% 2.42/2.64  ---> New Demodulator: 433 [new_demod,432] rselect_tail(q14)=index_42.
% 2.42/2.64  ** KEPT (pick-wt=4): 435 [copy,434,flip.1] s(index_42)=index_45.
% 2.42/2.64  ---> New Demodulator: 436 [new_demod,435] s(index_42)=index_45.
% 2.42/2.64  ** KEPT (pick-wt=4): 438 [copy,437,flip.1] rselect_head(queue_46)=index_47.
% 2.42/2.64  ---> New Demodulator: 439 [new_demod,438] rselect_head(queue_46)=index_47.
% 2.42/2.64  ** KEPT (pick-wt=4): 441 [copy,440,flip.1] s(index_47)=index_48.
% 2.42/2.64  ---> New Demodulator: 442 [new_demod,441] s(index_47)=index_48.
% 2.42/2.64  ** KEPT (pick-wt=4): 444 [copy,443,flip.1] rselect_tail(q15)=index_51.
% 2.42/2.64  ---> New Demodulator: 445 [new_demod,444] rselect_tail(q15)=index_51.
% 2.42/2.64  ** KEPT (pick-wt=4): 447 [copy,446,flip.1] s(index_51)=index_54.
% 2.42/2.64  ---> New Demodulator: 448 [new_demod,447] s(index_51)=index_54.
% 2.42/2.64  ** KEPT (pick-wt=4): 450 [copy,449,flip.1] rselect_tail(q16)=index_57.
% 2.42/2.64  ---> New Demodulator: 451 [new_demod,450] rselect_tail(q16)=index_57.
% 2.42/2.64  ** KEPT (pick-wt=4): 453 [copy,452,flip.1] s(index_3)=index_6.
% 2.42/2.64  ---> New Demodulator: 454 [new_demod,453] s(index_3)=index_6.
% 2.42/2.64  ** KEPT (pick-wt=4): 456 [copy,455,flip.1] s(index_57)=index_60.
% 2.42/2.64  ---> New Demodulator: 457 [new_demod,456] s(index_57)=index_60.
% 2.42/2.64  ** KEPT (pick-wt=4): 459 [copy,458,flip.1] rselect_tail(q17)=index_63.
% 2.42/2.64  ---> New Demodulator: 460 [new_demod,459] rselect_tail(q17)=index_63.
% 2.42/2.64  ** KEPT (pick-wt=4): 462 [copy,461,flip.1] s(index_63)=index_66.
% 2.42/2.64  ---> New Demodulator: 463 [new_demod,462] s(index_63)=index_66.
% 2.42/2.64  ** KEPT (pick-wt=4): 465 [copy,464,flip.1] rselect_head(queue_67)=index_68.
% 2.42/2.64  ---> New Demodulator: 466 [new_demod,465] rselect_head(queue_67)=index_68.
% 2.42/2.64  ** KEPT (pick-wt=4): 468 [copy,467,flip.1] s(index_68)=index_69.
% 2.42/2.64  ---> New Demodulator: 469 [new_demod,468] s(index_68)=index_69.
% 2.42/2.64  ** KEPT (pick-wt=4): 471 [copy,470,flip.1] rselect_tail(q18)=index_72.
% 2.42/2.64  ---> New Demodulator: 472 [new_demod,471] rselect_tail(q18)=index_72.
% 2.42/2.64  ** KEPT (pick-wt=4): 474 [copy,473,flip.1] s(index_72)=index_75.
% 2.42/2.64  ---> New Demodulator: 475 [new_demod,474] s(index_72)=index_75.
% 2.42/2.64  ** KEPT (pick-wt=4): 477 [copy,476,flip.1] rselect_tail(q1)=index_78.
% 2.42/2.64  ---> New Demodulator: 478 [new_demod,477] rselect_tail(q1)=index_78.
% 2.42/2.64  ** KEPT (pick-wt=4): 480 [copy,479,flip.1] s(index_78)=index_81.
% 2.42/2.64  ---> New Demodulator: 481 [new_demod,480] s(index_78)=index_81.
% 2.42/2.64  ** KEPT (pick-wt=4): 483 [copy,482,flip.1] rselect_tail(q19)=index_84.
% 2.42/2.64  ---> New Demodulator: 484 [new_demod,483] rselect_tail(q19)=index_84.
% 2.42/2.64  ** KEPT (pick-wt=4): 486 [copy,485,flip.1] s(index_84)=index_87.
% 2.42/2.64  ---> New Demodulator: 487 [new_demod,486] s(index_84)=index_87.
% 2.42/2.64  ** KEPT (pick-wt=4): 489 [copy,488,flip.1] rselect_tail(q9)=index_9.
% 2.42/2.64  ---> New Demodulator: 490 [new_demod,489] rselect_tail(q9)=index_9.
% 2.42/2.64  ** KEPT (pick-wt=4): 492 [copy,491,flip.1] rselect_tail(q20)=index_90.
% 2.42/2.64  ---> New Demodulator: 493 [new_demod,492] rselect_tail(q20)=index_90.
% 2.42/2.64  ** KEPT (pick-wt=4): 495 [copy,494,flip.1] s(index_90)=index_93.
% 2.42/2.64  ---> New Demodulator: 496 [new_demod,495] s(index_90)=index_93.
% 2.42/2.64  ** KEPT (pick-wt=4): 498 [copy,497,flip.1] rselect_head(queue_94)=index_95.
% 2.42/2.64  ---> New Demodulator: 499 [new_demod,498] rselect_head(queue_94)=index_95.
% 2.42/2.64  ** KEPT (pick-wt=4): 501 [copy,500,flip.1] s(index_95)=index_96.
% 2.42/2.64  ---> New Demodulator: 502 [new_demod,501] s(index_95)=index_96.
% 2.42/2.64  ** KEPT (pick-wt=4): 504 [copy,503,flip.1] rselect_tail(q21)=index_99.
% 2.42/2.64  ---> New Demodulator: 505 [new_demod,504] rselect_tail(q21)=index_99.
% 2.42/2.64  ** KEPT (pick-wt=5): 507 [copy,506,flip.1] rstore_head(q,index_0)=queue_1.
% 2.42/2.64  ---> New Demodulator: 508 [new_demod,507] rstore_head(q,index_0)=queue_1.
% 2.42/2.64  ** KEPT (pick-wt=5): 510 [copy,509,flip.1] rstore_se_q(q21,earray_100)=queue_101.
% 2.42/2.64  ---> New Demodulator: 511 [new_demod,510] rstore_se_q(q21,earray_100)=queue_101.
% 2.42/2.64  ** KEPT (pick-wt=5): 513 [copy,512,flip.1] rstore_tail(queue_101,index_102)=queue_103.
% 2.42/2.64  ---> New Demodulator: 514 [new_demod,513] rstore_tail(queue_101,index_102)=queue_103.
% 2.42/2.64  ** KEPT (pick-wt=5): 516 [copy,515,flip.1] rstore_se_q(q22,earray_106)=queue_107.
% 2.42/2.64  ---> New Demodulator: 517 [new_demod,516] rstore_se_q(q22,earray_106)=queue_107.
% 2.42/2.64  ** KEPT (pick-wt=5): 519 [copy,518,flip.1] rstore_tail(queue_107,index_108)=queue_109.
% 2.42/2.64  ---> New Demodulator: 520 [new_demod,519] rstore_tail(queue_107,index_108)=queue_109.
% 2.42/2.64  ** KEPT (pick-wt=5): 522 [copy,521,flip.1] rstore_se_q(q9,earray_10)=queue_11.
% 2.42/2.64  ---> New Demodulator: 523 [new_demod,522] rstore_se_q(q9,earray_10)=queue_11.
% 2.42/2.64  ** KEPT (pick-wt=5): 525 [copy,524,flip.1] rstore_se_q(q23,earray_112)=queue_113.
% 2.42/2.64  ---> New Demodulator: 526 [new_demod,525] rstore_se_q(q23,earray_112)=queue_113.
% 2.42/2.64  ** KEPT (pick-wt=5): 528 [copy,527,flip.1] rstore_tail(queue_113,index_114)=queue_115.
% 2.42/2.64  ---> New Demodulator: 529 [new_demod,528] rstore_tail(queue_113,index_114)=queue_115.
% 2.42/2.64  ** KEPT (pick-wt=5): 531 [copy,530,flip.1] rstore_head(queue_115,index_117)=queue_118.
% 2.42/2.64  ---> New Demodulator: 532 [new_demod,531] rstore_head(queue_115,index_117)=queue_118.
% 2.42/2.64  ** KEPT (pick-wt=5): 534 [copy,533,flip.1] rstore_se_q(q24,earray_121)=queue_122.
% 2.42/2.64  ---> New Demodulator: 535 [new_demod,534] rstore_se_q(q24,earray_121)=queue_122.
% 2.42/2.64  ** KEPT (pick-wt=5): 537 [copy,536,flip.1] rstore_tail(queue_122,index_123)=queue_124.
% 2.42/2.64  ---> New Demodulator: 538 [new_demod,537] rstore_tail(queue_122,index_123)=queue_124.
% 2.42/2.64  ** KEPT (pick-wt=5): 540 [copy,539,flip.1] rstore_se_q(q25,earray_127)=queue_128.
% 2.42/2.64  ---> New Demodulator: 541 [new_demod,540] rstore_se_q(q25,earray_127)=queue_128.
% 2.42/2.64  ** KEPT (pick-wt=5): 543 [copy,542,flip.1] rstore_tail(queue_11,index_12)=queue_13.
% 2.42/2.64  ---> New Demodulator: 544 [new_demod,543] rstore_tail(queue_11,index_12)=queue_13.
% 2.42/2.64  ** KEPT (pick-wt=5): 546 [copy,545,flip.1] rstore_tail(queue_128,index_129)=queue_130.
% 2.42/2.64  ---> New Demodulator: 547 [new_demod,546] rstore_tail(queue_128,index_129)=queue_130.
% 2.42/2.64  ** KEPT (pick-wt=5): 549 [copy,548,flip.1] rstore_se_q(q26,earray_133)=queue_134.
% 2.42/2.64  ---> New Demodulator: 550 [new_demod,549] rstore_se_q(q26,earray_133)=queue_134.
% 2.42/2.64  ** KEPT (pick-wt=5): 552 [copy,551,flip.1] rstore_tail(queue_134,index_135)=queue_136.
% 2.42/2.64  ---> New Demodulator: 553 [new_demod,552] rstore_tail(queue_134,index_135)=queue_136.
% 2.42/2.64  ** KEPT (pick-wt=5): 555 [copy,554,flip.1] rstore_head(queue_136,index_138)=queue_139.
% 2.42/2.64  ---> New Demodulator: 556 [new_demod,555] rstore_head(queue_136,index_138)=queue_139.
% 2.42/2.64  ** KEPT (pick-wt=5): 558 [copy,557,flip.1] rstore_se_q(q27,earray_142)=queue_143.
% 2.42/2.64  ---> New Demodulator: 559 [new_demod,558] rstore_se_q(q27,earray_142)=queue_143.
% 2.42/2.64  ** KEPT (pick-wt=5): 561 [copy,560,flip.1] rstore_tail(queue_143,index_144)=queue_145.
% 2.42/2.64  ---> New Demodulator: 562 [new_demod,561] rstore_tail(queue_143,index_144)=queue_145.
% 2.42/2.64  ** KEPT (pick-wt=5): 564 [copy,563,flip.1] rstore_se_q(q28,earray_148)=queue_149.
% 2.42/2.64  ---> New Demodulator: 565 [new_demod,564] rstore_se_q(q28,earray_148)=queue_149.
% 2.42/2.64  ** KEPT (pick-wt=5): 567 [copy,566,flip.1] rstore_tail(queue_149,index_150)=queue_151.
% 2.42/2.64  ---> New Demodulator: 568 [new_demod,567] rstore_tail(queue_149,index_150)=queue_151.
% 2.42/2.64  ** KEPT (pick-wt=5): 570 [copy,569,flip.1] rstore_se_q(q2,earray_154)=queue_155.
% 2.42/2.64  ---> New Demodulator: 571 [new_demod,570] rstore_se_q(q2,earray_154)=queue_155.
% 2.42/2.64  ** KEPT (pick-wt=5): 573 [copy,572,flip.1] rstore_tail(queue_155,index_156)=queue_157.
% 2.42/2.64  ---> New Demodulator: 574 [new_demod,573] rstore_tail(queue_155,index_156)=queue_157.
% 2.42/2.64  ** KEPT (pick-wt=5): 576 [copy,575,flip.1] rstore_head(queue_157,index_159)=queue_160.
% 2.42/2.64  ---> New Demodulator: 577 [new_demod,576] rstore_head(queue_157,index_159)=queue_160.
% 2.42/2.64  ** KEPT (pick-wt=5): 579 [copy,578,flip.1] rstore_se_q(q29,earray_163)=queue_164.
% 2.42/2.64  ---> New Demodulator: 580 [new_demod,579] rstore_se_q(q29,earray_163)=queue_164.
% 2.42/2.64  ** KEPT (pick-wt=5): 582 [copy,581,flip.1] rstore_tail(queue_164,index_165)=queue_166.
% 2.42/2.64  ---> New Demodulator: 583 [new_demod,582] rstore_tail(queue_164,index_165)=queue_166.
% 2.42/2.64  ** KEPT (pick-wt=5): 585 [copy,584,flip.1] rstore_head(queue_166,index_168)=queue_169.
% 2.42/2.64  ---> New Demodulator: 586 [new_demod,585] rstore_head(queue_166,index_168)=queue_169.
% 2.42/2.64  ** KEPT (pick-wt=5): 588 [copy,587,flip.1] rstore_se_q(q10,earray_16)=queue_17.
% 2.42/2.64  ---> New Demodulator: 589 [new_demod,588] rstore_se_q(q10,earray_16)=queue_17.
% 2.42/2.64  ** KEPT (pick-wt=5): 591 [copy,590,flip.1] rstore_se_q(q3,earray_172)=queue_173.
% 2.42/2.64  ---> New Demodulator: 592 [new_demod,591] rstore_se_q(q3,earray_172)=queue_173.
% 2.42/2.64  ** KEPT (pick-wt=5): 594 [copy,593,flip.1] rstore_tail(queue_173,index_174)=queue_175.
% 2.42/2.64  ---> New Demodulator: 595 [new_demod,594] rstore_tail(queue_173,index_174)=queue_175.
% 2.42/2.64  ** KEPT (pick-wt=5): 597 [copy,596,flip.1] rstore_se_q(q4,earray_178)=queue_179.
% 2.42/2.64  ---> New Demodulator: 598 [new_demod,597] rstore_se_q(q4,earray_178)=queue_179.
% 2.42/2.64  ** KEPT (pick-wt=5): 600 [copy,599,flip.1] rstore_tail(queue_179,index_180)=queue_181.
% 2.42/2.64  ---> New Demodulator: 601 [new_demod,600] rstore_tail(queue_179,index_180)=queue_181.
% 2.42/2.64  ** KEPT (pick-wt=5): 603 [copy,602,flip.1] rstore_se_q(q5,earray_184)=queue_185.
% 2.42/2.64  ---> New Demodulator: 604 [new_demod,603] rstore_se_q(q5,earray_184)=queue_185.
% 2.42/2.64  ** KEPT (pick-wt=5): 606 [copy,605,flip.1] rstore_tail(queue_185,index_186)=queue_187.
% 2.42/2.64  ---> New Demodulator: 607 [new_demod,606] rstore_tail(queue_185,index_186)=queue_187.
% 2.42/2.64  ** KEPT (pick-wt=5): 609 [copy,608,flip.1] rstore_tail(queue_17,index_18)=queue_19.
% 2.42/2.65  ---> New Demodulator: 610 [new_demod,609] rstore_tail(queue_17,index_18)=queue_19.
% 2.42/2.65  ** KEPT (pick-wt=5): 612 [copy,611,flip.1] rstore_head(queue_187,index_189)=queue_190.
% 2.42/2.65  ---> New Demodulator: 613 [new_demod,612] rstore_head(queue_187,index_189)=queue_190.
% 2.42/2.65  ** KEPT (pick-wt=5): 615 [copy,614,flip.1] rstore_se_q(q6,earray_193)=queue_194.
% 2.42/2.65  ---> New Demodulator: 616 [new_demod,615] rstore_se_q(q6,earray_193)=queue_194.
% 2.42/2.65  ** KEPT (pick-wt=5): 618 [copy,617,flip.1] rstore_tail(queue_194,index_195)=queue_196.
% 2.42/2.65  ---> New Demodulator: 619 [new_demod,618] rstore_tail(queue_194,index_195)=queue_196.
% 2.42/2.65  ** KEPT (pick-wt=5): 621 [copy,620,flip.1] rstore_se_q(q7,earray_199)=queue_200.
% 2.42/2.65  ---> New Demodulator: 622 [new_demod,621] rstore_se_q(q7,earray_199)=queue_200.
% 2.42/2.65  ** KEPT (pick-wt=5): 624 [copy,623,flip.1] rstore_tail(queue_200,index_201)=queue_202.
% 2.42/2.65  ---> New Demodulator: 625 [new_demod,624] rstore_tail(queue_200,index_201)=queue_202.
% 2.42/2.65  ** KEPT (pick-wt=5): 627 [copy,626,flip.1] rstore_se_q(q8,earray_205)=queue_206.
% 2.42/2.65  ---> New Demodulator: 628 [new_demod,627] rstore_se_q(q8,earray_205)=queue_206.
% 2.42/2.65  ** KEPT (pick-wt=5): 630 [copy,629,flip.1] rstore_tail(queue_206,index_207)=queue_208.
% 2.42/2.65  ---> New Demodulator: 631 [new_demod,630] rstore_tail(queue_206,index_207)=queue_208.
% 2.42/2.65  ** KEPT (pick-wt=5): 633 [copy,632,flip.1] rstore_head(queue_208,index_210)=queue_211.
% 2.42/2.65  ---> New Demodulator: 634 [new_demod,633] rstore_head(queue_208,index_210)=queue_211.
% 2.42/2.65  ** KEPT (pick-wt=5): 636 [copy,635,flip.1] rstore_se_q(q11,earray_22)=queue_23.
% 2.42/2.65  ---> New Demodulator: 637 [new_demod,636] rstore_se_q(q11,earray_22)=queue_23.
% 2.42/2.65  ** KEPT (pick-wt=5): 639 [copy,638,flip.1] rstore_tail(queue_23,index_24)=queue_25.
% 2.42/2.65  ---> New Demodulator: 640 [new_demod,639] rstore_tail(queue_23,index_24)=queue_25.
% 2.42/2.65  ** KEPT (pick-wt=5): 642 [copy,641,flip.1] rstore_head(queue_25,index_27)=queue_28.
% 2.42/2.65  ---> New Demodulator: 643 [new_demod,642] rstore_head(queue_25,index_27)=queue_28.
% 2.42/2.65  ** KEPT (pick-wt=5): 645 [copy,644,flip.1] rstore_se_q(q12,earray_31)=queue_32.
% 2.42/2.65  ---> New Demodulator: 646 [new_demod,645] rstore_se_q(q12,earray_31)=queue_32.
% 2.42/2.65  ** KEPT (pick-wt=5): 648 [copy,647,flip.1] rstore_tail(queue_32,index_33)=queue_34.
% 2.42/2.65  ---> New Demodulator: 649 [new_demod,648] rstore_tail(queue_32,index_33)=queue_34.
% 2.42/2.65  ** KEPT (pick-wt=5): 651 [copy,650,flip.1] rstore_se_q(q13,earray_37)=queue_38.
% 2.42/2.65  ---> New Demodulator: 652 [new_demod,651] rstore_se_q(q13,earray_37)=queue_38.
% 2.42/2.65  ** KEPT (pick-wt=5): 654 [copy,653,flip.1] rstore_tail(queue_38,index_39)=queue_40.
% 2.42/2.65  ---> New Demodulator: 655 [new_demod,654] rstore_tail(queue_38,index_39)=queue_40.
% 2.42/2.65  ** KEPT (pick-wt=5): 657 [copy,656,flip.1] rstore_se_q(q14,earray_43)=queue_44.
% 2.42/2.65  ---> New Demodulator: 658 [new_demod,657] rstore_se_q(q14,earray_43)=queue_44.
% 2.42/2.65  ** KEPT (pick-wt=5): 660 [copy,659,flip.1] rstore_tail(queue_44,index_45)=queue_46.
% 2.42/2.65  ---> New Demodulator: 661 [new_demod,660] rstore_tail(queue_44,index_45)=queue_46.
% 2.42/2.65  ** KEPT (pick-wt=5): 663 [copy,662,flip.1] rstore_head(queue_46,index_48)=queue_49.
% 2.42/2.65  ---> New Demodulator: 664 [new_demod,663] rstore_head(queue_46,index_48)=queue_49.
% 2.42/2.65  ** KEPT (pick-wt=5): 666 [copy,665,flip.1] rstore_se_q(q0,earray_4)=queue_5.
% 2.42/2.65  ---> New Demodulator: 667 [new_demod,666] rstore_se_q(q0,earray_4)=queue_5.
% 2.42/2.65  ** KEPT (pick-wt=5): 669 [copy,668,flip.1] rstore_se_q(q15,earray_52)=queue_53.
% 2.42/2.65  ---> New Demodulator: 670 [new_demod,669] rstore_se_q(q15,earray_52)=queue_53.
% 2.42/2.65  ** KEPT (pick-wt=5): 672 [copy,671,flip.1] rstore_tail(queue_53,index_54)=queue_55.
% 2.42/2.65  ---> New Demodulator: 673 [new_demod,672] rstore_tail(queue_53,index_54)=queue_55.
% 2.42/2.65  ** KEPT (pick-wt=5): 675 [copy,674,flip.1] rstore_se_q(q16,earray_58)=queue_59.
% 2.42/2.65  ---> New Demodulator: 676 [new_demod,675] rstore_se_q(q16,earray_58)=queue_59.
% 2.42/2.65  ** KEPT (pick-wt=5): 678 [copy,677,flip.1] rstore_tail(queue_59,index_60)=queue_61.
% 2.42/2.65  ---> New Demodulator: 679 [new_demod,678] rstore_tail(queue_59,index_60)=queue_61.
% 2.42/2.65  ** KEPT (pick-wt=5): 681 [copy,680,flip.1] rstore_se_q(q17,earray_64)=queue_65.
% 2.42/2.65  ---> New Demodulator: 682 [new_demod,681] rstore_se_q(q17,earray_64)=queue_65.
% 2.42/2.65  ** KEPT (pick-wt=5): 684 [copy,683,flip.1] rstore_tail(queue_65,index_66)=queue_67.
% 2.42/2.65  ---> New Demodulator: 685 [new_demod,684] rstore_tail(queue_65,index_66)=queue_67.
% 2.42/2.65  ** KEPT (pick-wt=5): 687 [copy,686,flip.1] rstore_tail(queue_5,index_6)=queue_7.
% 2.42/2.65  ---> New Demodulator: 688 [new_demod,687] rstore_tail(queue_5,index_6)=queue_7.
% 2.42/2.65  ** KEPT (pick-wt=5): 690 [copy,689,flip.1] rstore_head(queue_67,index_69)=queue_70.
% 2.42/2.65  ---> New Demodulator: 691 [new_demod,690] rstore_head(queue_67,index_69)=queue_70.
% 2.42/2.65  ** KEPT (pick-wt=5): 693 [copy,692,flip.1] rstore_se_q(q18,earray_73)=queue_74.
% 2.42/2.65  ---> New Demodulator: 694 [new_demod,693] rstore_se_q(q18,earray_73)=queue_74.
% 2.42/2.65  ** KEPT (pick-wt=5): 696 [copy,695,flip.1] rstore_tail(queue_74,index_75)=queue_76.
% 2.42/2.65  ---> New Demodulator: 697 [new_demod,696] rstore_tail(queue_74,index_75)=queue_76.
% 2.42/2.65  ** KEPT (pick-wt=5): 699 [copy,698,flip.1] rstore_se_q(q1,earray_79)=queue_80.
% 2.42/2.65  ---> New Demodulator: 700 [new_demod,699] rstore_se_q(q1,earray_79)=queue_80.
% 2.42/2.65  ** KEPT (pick-wt=5): 702 [copy,701,flip.1] rstore_tail(queue_80,index_81)=queue_82.
% 2.42/2.65  ---> New Demodulator: 703 [new_demod,702] rstore_tail(queue_80,index_81)=queue_82.
% 2.42/2.65  ** KEPT (pick-wt=5): 705 [copy,704,flip.1] rstore_se_q(q19,earray_85)=queue_86.
% 2.42/2.65  ---> New Demodulator: 706 [new_demod,705] rstore_se_q(q19,earray_85)=queue_86.
% 2.42/2.65  ** KEPT (pick-wt=5): 708 [copy,707,flip.1] rstore_tail(queue_86,index_87)=queue_88.
% 2.42/2.65  ---> New Demodulator: 709 [new_demod,708] rstore_tail(queue_86,index_87)=queue_88.
% 2.42/2.65  ** KEPT (pick-wt=5): 711 [copy,710,flip.1] rstore_se_q(q20,earray_91)=queue_92.
% 2.42/2.65  ---> New Demodulator: 712 [new_demod,711] rstore_se_q(q20,earray_91)=queue_92.
% 2.42/2.65  ** KEPT (pick-wt=5): 714 [copy,713,flip.1] rstore_tail(queue_92,index_93)=queue_94.
% 2.42/2.65  ---> New Demodulator: 715 [new_demod,714] rstore_tail(queue_92,index_93)=queue_94.
% 2.42/2.65  ** KEPT (pick-wt=5): 717 [copy,716,flip.1] rstore_head(queue_94,index_96)=queue_97.
% 2.42/2.65  ---> New Demodulator: 718 [new_demod,717] rstore_head(queue_94,index_96)=queue_97.
% 2.42/2.65  ** KEPT (pick-wt=3): 720 [copy,719,flip.1] queue_1=q0.
% 2.42/2.65  ---> New Demodulator: 721 [new_demod,720] queue_1=q0.
% 2.42/2.65  ** KEPT (pick-wt=3): 723 [copy,722,flip.1] queue_7=q1.
% 2.42/2.65  ---> New Demodulator: 724 [new_demod,723] queue_7=q1.
% 2.42/2.65  ** KEPT (pick-wt=3): 726 [copy,725,flip.1] queue_13=q10.
% 2.42/2.65  ---> New Demodulator: 727 [new_demod,726] queue_13=q10.
% 2.42/2.65  ** KEPT (pick-wt=3): 729 [copy,728,flip.1] queue_19=q11.
% 2.42/2.65  ---> New Demodulator: 730 [new_demod,729] queue_19=q11.
% 2.42/2.65  ** KEPT (pick-wt=3): 732 [copy,731,flip.1] queue_28=q12.
% 2.42/2.65  ---> New Demodulator: 733 [new_demod,732] queue_28=q12.
% 2.42/2.65  ** KEPT (pick-wt=3): 735 [copy,734,flip.1] queue_34=q13.
% 2.42/2.65  ---> New Demodulator: 736 [new_demod,735] queue_34=q13.
% 2.42/2.65  ** KEPT (pick-wt=3): 738 [copy,737,flip.1] queue_40=q14.
% 2.42/2.65  ---> New Demodulator: 739 [new_demod,738] queue_40=q14.
% 2.42/2.65  ** KEPT (pick-wt=3): 741 [copy,740,flip.1] queue_49=q15.
% 2.42/2.65  ---> New Demodulator: 742 [new_demod,741] queue_49=q15.
% 2.42/2.65  ** KEPT (pick-wt=3): 744 [copy,743,flip.1] queue_55=q16.
% 2.42/2.65  ---> New Demodulator: 745 [new_demod,744] queue_55=q16.
% 2.42/2.65  ** KEPT (pick-wt=3): 747 [copy,746,flip.1] queue_61=q17.
% 2.42/2.65  ---> New Demodulator: 748 [new_demod,747] queue_61=q17.
% 2.42/2.65  ** KEPT (pick-wt=3): 750 [copy,749,flip.1] queue_70=q18.
% 2.42/2.65  ---> New Demodulator: 751 [new_demod,750] queue_70=q18.
% 2.42/2.65  ** KEPT (pick-wt=3): 753 [copy,752,flip.1] queue_76=q19.
% 2.42/2.65  ---> New Demodulator: 754 [new_demod,753] queue_76=q19.
% 2.42/2.65  ** KEPT (pick-wt=3): 756 [copy,755,flip.1] queue_82=q2.
% 2.42/2.65  ---> New Demodulator: 757 [new_demod,756] queue_82=q2.
% 2.42/2.65  ** KEPT (pick-wt=3): 759 [copy,758,flip.1] queue_88=q20.
% 2.42/2.65  ---> New Demodulator: 760 [new_demod,759] queue_88=q20.
% 2.42/2.65  ** KEPT (pick-wt=3): 762 [copy,761,flip.1] queue_97=q21.
% 2.42/2.65  ---> New Demodulator: 763 [new_demod,762] queue_97=q21.
% 2.42/2.65  ** KEPT (pick-wt=3): 765 [copy,764,flip.1] queue_103=q22.
% 2.42/2.65  ---> New Demodulator: 766 [new_demod,765] queue_103=q22.
% 2.42/2.65  ** KEPT (pick-wt=3): 768 [copy,767,flip.1] queue_109=q23.
% 2.42/2.65  ---> New Demodulator: 769 [new_demod,768] queue_109=q23.
% 2.42/2.65  ** KEPT (pick-wt=3): 771 [copy,770,flip.1] queue_118=q24.
% 2.42/2.65  ---> New Demodulator: 772 [new_demod,771] queue_118=q24.
% 2.42/2.65  ** KEPT (pick-wt=3): 774 [copy,773,flip.1] queue_124=q25.
% 2.42/2.65  ---> New Demodulator: 775 [new_demod,774] queue_124=q25.
% 2.42/2.65  ** KEPT (pick-wt=3): 777 [copy,776,flip.1] queue_130=q26.
% 2.42/2.65  ---> New Demodulator: 778 [new_demod,777] queue_130=q26.
% 2.42/2.65  ** KEPT (pick-wt=3): 780 [copy,779,flip.1] queue_139=q27.
% 2.42/2.65  ---> New Demodulator: 781 [new_demod,780] queue_139=q27.
% 2.42/2.65  ** KEPT (pick-wt=3): 783 [copy,782,flip.1] queue_145=q28.
% 2.42/2.65  ---> New Demodulator: 784 [new_demod,783] queue_145=q28.
% 2.42/2.65  ** KEPT (pick-wt=3): 786 [copy,785,flip.1] queue_151=q29.
% 2.42/2.65  ---> New Demodulator: 787 [new_demod,786] queue_151=q29.
% 2.42/2.65  ** KEPT (pick-wt=3): 789 [copy,788,flip.1] queue_160=q3.
% 2.42/2.65  ---> New Demodulator: 790 [new_demod,789] queue_160=q3.
% 2.42/2.65  ** KEPT (pick-wt=3): 792 [copy,791,flip.1] queue_169=q30.
% 2.42/2.65  ---> New Demodulator: 793 [new_demod,792] queue_169=q30.
% 2.42/2.65  ** KEPT (pick-wt=3): 795 [copy,794,flip.1] queue_175=q4.
% 2.42/2.65  ---> New Demodulator: 796 [new_demod,795] queue_175=q4.
% 2.42/2.65  ** KEPT (pick-wt=3): 798 [copy,797,flip.1] queue_181=q5.
% 2.42/2.65  ---> New Demodulator: 799 [new_demod,798] queue_181=q5.
% 2.42/2.65  ** KEPT (pick-wt=3): 801 [copy,800,flip.1] queue_190=q6.
% 2.42/2.65  ---> New Demodulator: 802 [new_demod,801] queue_190=q6.
% 2.42/2.65  ** KEPT (pick-wt=3): 804 [copy,803,flip.1] queue_196=q7.
% 2.42/2.65  ---> New Demodulator: 805 [new_demod,804] queue_196=q7.
% 2.42/2.65  ** KEPT (pick-wt=3): 807 [copy,806,flip.1] queue_202=q8.
% 2.42/2.65  ---> New Demodulator: 808 [new_demod,807] queue_202=q8.
% 2.42/2.65  ** KEPT (pick-wt=3): 810 [copy,809,flip.1] queue_211=q9.
% 2.42/2.65  ---> New Demodulator: 811 [new_demod,810] queue_211=q9.
% 2.42/2.65    Following clause subsumed by 52 during input processing: 0 [copy,52,flip.1] A=A.
% 2.42/2.65  >>>> Starting back demodulation with 54.
% 2.42/2.65  >>>> Starting back demodulation with 57.
% 2.42/2.65  >>>> Starting back demodulation with 59.
% 2.42/2.65  >>>> Starting back demodulation with 61.
% 2.42/2.65  >>>> Starting back demodulation with 63.
% 2.42/2.65  >>>> Starting back demodulation with 65.
% 2.42/2.65  >>>> Starting back demodulation with 67.
% 2.42/2.65  >>>> Starting back demodulation with 69.
% 2.42/2.65  >>>> Starting back demodulation with 71.
% 2.42/2.65  >>>> Starting back demodulation with 73.
% 2.42/2.65  >>>> Starting back demodulation with 76.
% 2.42/2.65  >>>> Starting back demodulation with 79.
% 2.42/2.65  >>>> Starting back demodulation with 82.
% 2.42/2.65  >>>> Starting back demodulation with 85.
% 2.42/2.65  >>>> Starting back demodulation with 88.
% 2.42/2.65  >>>> Starting back demodulation with 91.
% 2.42/2.65  >>>> Starting back demodulation with 94.
% 2.42/2.65  >>>> Starting back demodulation with 97.
% 2.42/2.65  >>>> Starting back demodulation with 100.
% 2.42/2.65  >>>> Starting back demodulation with 103.
% 2.42/2.65  >>>> Starting back demodulation with 106.
% 2.42/2.65  >>>> Starting back demodulation with 109.
% 2.42/2.65  >>>> Starting back demodulation with 112.
% 2.42/2.65  >>>> Starting back demodulation with 115.
% 2.42/2.65  >>>> Starting back demodulation with 118.
% 2.42/2.65  >>>> Starting back demodulation with 121.
% 2.42/2.65  >>>> Starting back demodulation with 124.
% 2.42/2.65  >>>> Starting back demodulation with 127.
% 2.42/2.65  >>>> Starting back demodulation with 130.
% 2.42/2.65  >>>> Starting back demodulation with 133.
% 2.42/2.65  >>>> Starting back demodulation with 136.
% 2.42/2.65  >>>> Starting back demodulation with 139.
% 2.42/2.65  >>>> Starting back demodulation with 142.
% 2.42/2.65  >>>> Starting back demodulation with 145.
% 2.42/2.65  >>>> Starting back demodulation with 148.
% 2.42/2.65  >>>> Starting back demodulation with 151.
% 2.42/2.65  >>>> Starting back demodulation with 154.
% 2.42/2.65  >>>> Starting back demodulation with 157.
% 2.42/2.65  >>>> Starting back demodulation with 160.
% 2.42/2.65  >>>> Starting back demodulation with 163.
% 2.42/2.65  >>>> Starting back demodulation with 166.
% 2.42/2.65  >>>> Starting back demodulation with 169.
% 2.42/2.65  >>>> Starting back demodulation with 172.
% 2.42/2.65  >>>> Starting back demodulation with 175.
% 2.42/2.65  >>>> Starting back demodulation with 178.
% 2.42/2.65  >>>> Starting back demodulation with 181.
% 2.42/2.65  >>>> Starting back demodulation with 184.
% 2.42/2.65  >>>> Starting back demodulation with 187.
% 2.42/2.65  >>>> Starting back demodulation with 190.
% 2.42/2.65  >>>> Starting back demodulation with 193.
% 2.42/2.65  >>>> Starting back demodulation with 196.
% 2.42/2.65  >>>> Starting back demodulation with 199.
% 2.42/2.65  >>>> Starting back demodulation with 202.
% 2.42/2.65  >>>> Starting back demodulation with 205.
% 2.42/2.65  >>>> Starting back demodulation with 208.
% 2.42/2.65  >>>> Starting back demodulation with 211.
% 2.42/2.65  >>>> Starting back demodulation with 214.
% 2.42/2.65  >>>> Starting back demodulation with 217.
% 2.42/2.65  >>>> Starting back demodulation with 220.
% 2.42/2.65  >>>> Starting back demodulation with 223.
% 2.42/2.65  >>>> Starting back demodulation with 226.
% 2.42/2.65  >>>> Starting back demodulation with 229.
% 2.42/2.65  >>>> Starting back demodulation with 232.
% 2.42/2.65  >>>> Starting back demodulation with 235.
% 2.42/2.65  >>>> Starting back demodulation with 238.
% 2.42/2.65  >>>> Starting back demodulation with 241.
% 2.42/2.65  >>>> Starting back demodulation with 244.
% 2.42/2.65  >>>> Starting back demodulation with 247.
% 2.42/2.65  >>>> Starting back demodulation with 250.
% 2.42/2.65  >>>> Starting back demodulation with 253.
% 2.42/2.65  >>>> Starting back demodulation with 256.
% 2.42/2.65  >>>> Starting back demodulation with 259.
% 2.42/2.65  >>>> Starting back demodulation with 262.
% 2.42/2.65  >>>> Starting back demodulation with 265.
% 2.42/2.65  >>>> Starting back demodulation with 268.
% 2.42/2.65  >>>> Starting back demodulation with 271.
% 2.42/2.65  >>>> Starting back demodulation with 274.
% 2.42/2.65  >>>> Starting back demodulation with 277.
% 2.42/2.65  >>>> Starting back demodulation with 280.
% 2.42/2.65  >>>> Starting back demodulation with 283.
% 2.42/2.65  >>>> Starting back demodulation with 286.
% 2.42/2.65  >>>> Starting back demodulation with 289.
% 2.42/2.65  >>>> Starting back demodulation with 292.
% 2.42/2.65  >>>> Starting back demodulation with 295.
% 2.42/2.65  >>>> Starting back demodulation with 298.
% 2.42/2.65  >>>> Starting back demodulation with 301.
% 2.42/2.65  >>>> Starting back demodulation with 304.
% 2.42/2.65  >>>> Starting back demodulation with 307.
% 2.42/2.65  >>>> Starting back demodulation with 310.
% 2.42/2.65  >>>> Starting back demodulation with 313.
% 2.42/2.65  >>>> Starting back demodulation with 316.
% 2.42/2.65  >>>> Starting back demodulation with 319.
% 2.42/2.65  >>>> Starting back demodulation with 322.
% 2.42/2.65  >>>> Starting back demodulation with 325.
% 2.42/2.65  >>>> Starting back demodulation with 328.
% 2.42/2.65  >>>> Starting back demodulation with 331.
% 2.42/2.65  >>>> Starting back demodulation with 334.
% 2.42/2.65  >>>> Starting back demodulation with 337.
% 2.42/2.65  >>>> Starting back demodulation with 340.
% 2.42/2.65  >>>> Starting back demodulation with 343.
% 2.42/2.65  >>>> Starting back demodulation with 346.
% 2.42/2.65  >>>> Starting back demodulation with 349.
% 2.42/2.65  >>>> Starting back demodulation with 352.
% 2.42/2.65  >>>> Starting back demodulation with 355.
% 2.42/2.65  >>>> Starting back demodulation with 358.
% 2.42/2.65  >>>> Starting back demodulation with 361.
% 2.42/2.65  >>>> Starting back demodulation with 364.
% 2.42/2.65  >>>> Starting back demodulation with 367.
% 2.42/2.65  >>>> Starting back demodulation with 370.
% 2.42/2.65  >>>> Starting back demodulation with 373.
% 2.42/2.65  >>>> Starting back demodulation with 376.
% 2.42/2.65  >>>> Starting back demodulation with 379.
% 2.42/2.65  >>>> Starting back demodulation with 382.
% 2.42/2.65  >>>> Starting back demodulation with 385.
% 2.42/2.65  >>>> Starting back demodulation with 388.
% 2.42/2.65  >>>> Starting back demodulation with 391.
% 2.42/2.65  >>>> Starting back demodulation with 394.
% 2.42/2.65  >>>> Starting back demodulation with 397.
% 2.42/2.65  >>>> Starting back demodulation with 400.
% 2.42/2.65  >>>> Starting back demodulation with 403.
% 2.42/2.65  >>>> Starting back demodulation with 406.
% 2.42/2.65  >>>> Starting back demodulation with 409.
% 2.42/2.65  >>>> Starting back demodulation with 412.
% 2.42/2.65  >>>> Starting back demodulation with 415.
% 2.42/2.65  >>>> Starting back demodulation with 418.
% 2.42/2.65  >>>> Starting back demodulation with 421.
% 2.42/2.65  >>>> Starting back demodulation with 424.
% 2.42/2.65  >>>> Starting back demodulation with 427.
% 2.42/2.65  >>>> Starting back demodulation with 430.
% 2.42/2.65  >>>> Starting back demodulation with 433.
% 2.42/2.65  >>>> Starting back demodulation with 436.
% 2.42/2.65  >>>> Starting back demodulation with 439.
% 2.42/2.65  >>>> Starting back demodulation with 442.
% 2.42/2.65  >>>> Starting back demodulation with 445.
% 2.42/2.65  >>>> Starting back demodulation with 448.
% 2.42/2.65  >>>> Starting back demodulation with 451.
% 2.42/2.65  >>>> Starting back demodulation with 454.
% 2.42/2.65  >>>> Starting back demodulation with 457.
% 2.42/2.65  >>>> Starting back demodulation with 460.
% 2.42/2.65  >>>> Starting back demodulation with 463.
% 2.42/2.65  >>>> Starting back demodulation with 466.
% 2.42/2.65  >>>> Starting back demodulation with 469.
% 2.42/2.65  >>>> Starting back demodulation with 472.
% 2.42/2.65  >>>> Starting back demodulation with 475.
% 2.42/2.65  >>>> Starting back demodulation with 478.
% 2.42/2.65  >>>> Starting back demodulation with 481.
% 2.42/2.65  >>>> Starting back demodulation with 484.
% 2.42/2.65  >>>> Starting back demodulation with 487.
% 2.42/2.65  >>>> Starting back demodulation with 490.
% 2.42/2.65  >>>> Starting back demodulation with 493.
% 2.42/2.65  >>>> Starting back demodulation with 496.
% 2.42/2.65  >>>> Starting back demodulation with 499.
% 2.42/2.65  >>>> Starting back demodulation with 502.
% 2.42/2.65  >>>> Starting back demodulation with 505.
% 2.42/2.65  >>>> Starting back demodulation with 508.
% 2.42/2.65  >>>> Starting back demodulation with 511.
% 2.42/2.65  >>>> Starting back demodulation with 514.
% 2.42/2.65  >>>> Starting back demodulation with 517.
% 2.42/2.65  >>>> Starting back demodulation with 520.
% 2.42/2.65  >>>> Starting back demodulation with 523.
% 2.42/2.65  >>>> Starting back demodulation with 526.
% 2.42/2.65  >>>> Starting back demodulation with 529.
% 2.42/2.65  >>>> Starting back demodulation with 532.
% 2.42/2.65  >>>> Starting back demodulation with 535.
% 2.42/2.65  >>>> Starting back demodulation with 538.
% 2.42/2.65  >>>> Starting back demodulation with 541.
% 2.42/2.65  >>>> Starting back demodulation with 544.
% 2.42/2.65  >>>> Starting back demodulation with 547.
% 2.42/2.65  >>>> Starting back demodulation with 550.
% 2.42/2.65  >>>> Starting back demodulation with 553.
% 2.42/2.65  >>>> Starting back demodulation with 556.
% 2.42/2.65  >>>> Starting back demodulation with 559.
% 2.42/2.65  >>>> Starting back demodulation with 562.
% 2.42/2.65  >>>> Starting back demodulation with 565.
% 2.42/2.65  >>>> Starting back demodulation with 568.
% 2.42/2.65  >>>> Starting back demodulation with 571.
% 2.42/2.65  >>>> Starting back demodulation with 574.
% 2.42/2.65  >>>> Starting back demodulation with 577.
% 2.42/2.65  >>>> Starting back demodulation with 580.
% 2.42/2.65  >>>> Starting back demodulation with 583.
% 2.42/2.65  >>>> Starting back demodulation with 586.
% 2.42/2.65  >>>> Starting back demodulation with 589.
% 2.42/2.65  >>>> Starting back demodulation with 592.
% 2.42/2.65  >>>> Starting back demodulation with 595.
% 2.42/2.65  >>>> Starting back demodulation with 598.
% 2.42/2.65  >>>> Starting back demodulation with 601.
% 2.42/2.65  >>>> Starting back demodulation with 604.
% 2.42/2.65  >>>> Starting back demodulation with 607.
% 2.42/2.65  >>>> Starting back demodulation with 610.
% 2.42/2.65  >>>> Starting back demodulation with 613.
% 2.42/2.65  >>>> Starting back demodulation with 616.
% 2.42/2.65  >>>> Starting back demodulation with 619.
% 2.42/2.65  >>>> Starting back demodulation with 622.
% 2.42/2.65  >>>> Starting back demodulation with 625.
% 2.42/2.65  >>>> Starting back demodulation with 628.
% 2.42/2.65  >>>> Starting back demodulation with 631.
% 2.42/2.65  >>>> Starting back demodulation with 634.
% 2.42/2.65  >>>> Starting back demodulation with 637.
% 2.42/2.65  >>>> Starting back demodulation with 640.
% 2.42/2.65  >>>> Starting back demodulation with 643.
% 2.42/2.65  >>>> Starting back demodulation with 646.
% 2.42/2.65  >>>> Starting back demodulation with 649.
% 2.42/2.65  >>>> Starting back demodulation with 652.
% 2.42/2.65  >>>> Starting back demodulation with 655.
% 2.42/2.65  >>>> Starting back demodulation with 658.
% 2.42/2.65  >>>> Starting back demodulation with 661.
% 2.42/2.65  >>>> Starting back demodulation with 664.
% 2.42/2.65  >>>> Starting back demodulation with 667.
% 2.42/2.65  >>>> Starting back demodulation with 670.
% 2.42/2.65  >>>> Starting back demodulation with 673.
% 2.42/2.65  >>>> Starting back demodulation with 676.
% 2.42/2.65  >>>> Starting back demodulation with 679.
% 2.42/2.65  >>>> Starting back demodulation with 682.
% 2.42/2.65  >>>> Starting back demodulation with 685.
% 2.42/2.65  >>>> Starting back demodulation with 688.
% 2.42/2.65  >>>> Starting back demodulation with 691.
% 2.42/2.65  >>>> Starting back demodulation with 694.
% 2.42/2.65  >>>> Starting back demodulation with 697.
% 2.42/2.65  >>>> Starting back demodulation with 700.
% 2.42/2.65  >>>> Starting back demodulation with 703.
% 2.42/2.65  >>>> Starting back demodulation with 706.
% 2.42/2.65  >>>> Starting back demodulation with 709.
% 2.42/2.65  >>>> Starting back demodulation with 712.
% 2.42/2.65  >>>> Starting back demodulation with 715.
% 2.42/2.65  >>>> Starting back demodulation with 718.
% 2.42/2.65  >>>> Starting back demodulation with 721.
% 2.42/2.65      >> back demodulating 507 with 721.
% 2.42/2.65  >>>> Starting back demodulation with 724.
% 2.42/2.65      >> back demodulating 687 with 724.
% 2.42/2.65  >>>> Starting back demodulation with 727.
% 2.42/2.65      >> back demodulating 543 with 727.
% 2.42/2.65  >>>> Starting back demodulation with 730.
% 2.42/2.65      >> back demodulating 609 with 730.
% 2.42/2.65  >>>> Starting back demodulation with 733.
% 2.42/2.65      >> back demodulating 642 with 733.
% 2.42/2.65  >>>> Starting back demodulation with 736.
% 2.42/2.65      >> back demodulating 648 with 736.
% 2.42/2.65  >>>> Starting back demodulation with 739.
% 2.42/2.65      >> back demodulating 654 with 739.
% 2.42/2.65  >>>> Starting back demodulation with 742.
% 2.42/2.65      >> back demodulating 663 with 742.
% 2.42/2.65  >>>> Starting back demodulation with 745.
% 2.42/2.65      >> back demodulating 672 with 745.
% 2.42/2.65  >>>> Starting back demodulation with 748.
% 2.42/2.65      >> back demodulating 678 with 748.
% 2.42/2.65  >>>> Starting back demodulation with 751.
% 2.42/2.65      >> back demodulating 690 with 751.
% 2.42/2.65  >>>> Starting back demodulation with 754.
% 2.42/2.65      >> back demodulating 696 with 754.
% 2.42/2.65  >>>> Starting back demodulation with 757.
% 2.42/2.65      >> back demodulating 702 with 757.
% 2.42/2.65  >>>> Starting back demodulation with 760.
% 2.42/2.65      >> back demodulating 708 with 760.
% 2.42/2.65  >>>> Starting back demodulation with 763.
% 2.42/2.65      >> back demodulating 717 with 763.
% 2.42/2.65  >>>> Starting back demodulation with 766.
% 2.42/2.65      >> back demodulating 513 with 766.
% 2.42/2.65  >>>> Starting back demodulation with 769.
% 2.42/2.65      >> back demodulating 519 with 769.
% 2.42/2.65  >>>> Starting back demodulation with 772.
% 2.42/2.65      >> back demodulating 531 with 772.
% 27.54/27.74  >>>> Starting back demodulation with 775.
% 27.54/27.74      >> back demodulating 537 with 775.
% 27.54/27.74  >>>> Starting back demodulation with 778.
% 27.54/27.74      >> back demodulating 546 with 778.
% 27.54/27.74  >>>> Starting back demodulation with 781.
% 27.54/27.74      >> back demodulating 555 with 781.
% 27.54/27.74  >>>> Starting back demodulation with 784.
% 27.54/27.74      >> back demodulating 561 with 784.
% 27.54/27.74  >>>> Starting back demodulation with 787.
% 27.54/27.74      >> back demodulating 567 with 787.
% 27.54/27.74  >>>> Starting back demodulation with 790.
% 27.54/27.74      >> back demodulating 576 with 790.
% 27.54/27.74  >>>> Starting back demodulation with 793.
% 27.54/27.74      >> back demodulating 585 with 793.
% 27.54/27.74  >>>> Starting back demodulation with 796.
% 27.54/27.74      >> back demodulating 594 with 796.
% 27.54/27.74  >>>> Starting back demodulation with 799.
% 27.54/27.74      >> back demodulating 600 with 799.
% 27.54/27.74  >>>> Starting back demodulation with 802.
% 27.54/27.74      >> back demodulating 612 with 802.
% 27.54/27.74  >>>> Starting back demodulation with 805.
% 27.54/27.74      >> back demodulating 618 with 805.
% 27.54/27.74  >>>> Starting back demodulation with 808.
% 27.54/27.74      >> back demodulating 624 with 808.
% 27.54/27.74  >>>> Starting back demodulation with 811.
% 27.54/27.74      >> back demodulating 633 with 811.
% 27.54/27.74  >>>> Starting back demodulation with 813.
% 27.54/27.74  >>>> Starting back demodulation with 815.
% 27.54/27.74  >>>> Starting back demodulation with 817.
% 27.54/27.74  >>>> Starting back demodulation with 819.
% 27.54/27.74  >>>> Starting back demodulation with 821.
% 27.54/27.74  >>>> Starting back demodulation with 823.
% 27.54/27.74  >>>> Starting back demodulation with 825.
% 27.54/27.74  >>>> Starting back demodulation with 827.
% 27.54/27.74  >>>> Starting back demodulation with 829.
% 27.54/27.74  >>>> Starting back demodulation with 831.
% 27.54/27.74  >>>> Starting back demodulation with 833.
% 27.54/27.74  >>>> Starting back demodulation with 835.
% 27.54/27.74  >>>> Starting back demodulation with 837.
% 27.54/27.74  >>>> Starting back demodulation with 839.
% 27.54/27.74  >>>> Starting back demodulation with 841.
% 27.54/27.74  >>>> Starting back demodulation with 843.
% 27.54/27.74  >>>> Starting back demodulation with 845.
% 27.54/27.74  >>>> Starting back demodulation with 847.
% 27.54/27.74  >>>> Starting back demodulation with 849.
% 27.54/27.74  >>>> Starting back demodulation with 851.
% 27.54/27.74  >>>> Starting back demodulation with 853.
% 27.54/27.74  >>>> Starting back demodulation with 855.
% 27.54/27.74  >>>> Starting back demodulation with 857.
% 27.54/27.74  >>>> Starting back demodulation with 859.
% 27.54/27.74  >>>> Starting back demodulation with 861.
% 27.54/27.74  >>>> Starting back demodulation with 863.
% 27.54/27.74  >>>> Starting back demodulation with 865.
% 27.54/27.74  >>>> Starting back demodulation with 867.
% 27.54/27.74  >>>> Starting back demodulation with 869.
% 27.54/27.74  >>>> Starting back demodulation with 871.
% 27.54/27.74  >>>> Starting back demodulation with 873.
% 27.54/27.74  
% 27.54/27.74  ======= end of input processing =======
% 27.54/27.74  
% 27.54/27.74  =========== start of search ===========
% 27.54/27.74  
% 27.54/27.74  
% 27.54/27.74  Resetting weight limit to 4.
% 27.54/27.74  
% 27.54/27.74  
% 27.54/27.74  Resetting weight limit to 4.
% 27.54/27.74  
% 27.54/27.74  sos_size=1574
% 27.54/27.74  
% 27.54/27.74  Search stopped because sos empty.
% 27.54/27.74  
% 27.54/27.74  
% 27.54/27.74  Search stopped because sos empty.
% 27.54/27.74  
% 27.54/27.74  ============ end of search ============
% 27.54/27.74  
% 27.54/27.74  -------------- statistics -------------
% 27.54/27.74  clauses given               2421
% 27.54/27.74  clauses generated        2157808
% 27.54/27.74  clauses kept                2539
% 27.54/27.74  clauses forward subsumed    1131
% 27.54/27.74  clauses back subsumed          8
% 27.54/27.74  Kbytes malloced             8789
% 27.54/27.74  
% 27.54/27.74  ----------- times (seconds) -----------
% 27.54/27.74  user CPU time         25.10          (0 hr, 0 min, 25 sec)
% 27.54/27.74  system CPU time        0.01          (0 hr, 0 min, 0 sec)
% 27.54/27.74  wall-clock time       27             (0 hr, 0 min, 27 sec)
% 27.54/27.74  
% 27.54/27.74  Process 15662 finished Wed Jul 27 06:05:22 2022
% 27.54/27.74  Otter interrupted
% 27.54/27.74  PROOF NOT FOUND
%------------------------------------------------------------------------------